Error Number: 20

Mizar Message:

Description

1. A statement Q justified by a scheme does not match the scheme's conclusion, or
2. A statement P justifying a scheme does not match the scheme's premise statement, or
3. A private-functor or private-predicate used in P or Q does not match the corresponding scheme parameter.

Basic examples

    defpred NonNeg[Nat] means $1 >= 0;

:: wrong
::   Although NAT_1:sch 1 specifies parameter P[Nat], the premise and conclusion of the scheme 
::   specify the type Element of NAT: 
::          for k being Element of NAT holds P[k]
::   In this example, n is Nat, hence the error:
    reserve n for Nat;
    A: NonNeg[0];
    B: for n st NonNeg[n] holds NonNeg[n+1];
    for n holds NonNeg[n] from NAT_1:sch 1(A,B);
::>                          *20

:: right 1
:: Here the type of n matches the scheme's expectation
    reserve n for Element of NAT;
    A: NonNeg[0];
    B: for n st NonNeg[n] holds NonNeg[n+1];
    for n holds NonNeg[n] from NAT_1:sch 1(A,B);

:: right 2
::   The statement and premises need not match the scheme's conclusion
::   and premise exactly as long as they are (trivially) logically equivalent.
    reserve n for Element of NAT;
    A: NonNeg[0];
    B: NonNeg[n] implies NonNeg[n+1];
    NonNeg[n] from NAT_1:sch 1(A,B);

Typical examples

:: These are based on scheme MinimalFiniteSet in ABCMIZ_0 and its
:: use by ABCMIZ_0:th 65

:: wrong 2
::   The premise to MinimalFiniteSet requires a 'finite set'
    reserve X for finite set;
    defpred P[set] means $1 c= NAT;
    A: ex a being set st P[a] proof               ::  error here
        take {0};
        thus thesis by ZFMISC_1:37;
    end;
    ex X st P[X] & for Y being set st Y c= X & P[Y] holds Y = X from ABCMIZ_0:sch 1(A);
::>                                                                                 *20

:: right 3
    reserve X for finite set;
    defpred P[set] means $1 c= NAT;
    A: ex a being finite set st P[a] proof      :: fixed
        take {0};
        thus thesis by ZFMISC_1:37;
    end;
    ex X st P[X] & for Y being set st Y c= X & P[Y] holds Y = X from ABCMIZ_0:sch 1(A);

:: right 4 
::   A scheme does not disagree if its conclusion reduces the residual thesis even if
::   they don't match. Here 'consider' is justified by MinimalFiniteSet.
    reserve X for finite set;
    defpred P[set] means $1 c= NAT;
    A: ex a being finite set st P[a] proof
        take {0};
        thus thesis by ZFMISC_1:37;
    end;
    consider X such that P[X] and for Y being set st Y c= X & P[Y] holds Y = X from ABCMIZ_0:sch 1(A);