Error Number: 834

Mizar Message:

Description

Typical example

environ

vocabularies BOOLE,FUNCT_1,RELAT_1;
notations FUNCT_1,NAT_1,RELAT_1,TARSKI,XBOOLE_0,XXREAL_0,ZFMISC_1;
constructors FUNCT_1,NAT_1,RELAT_1,TARSKI,XBOOLE_0,XXREAL_0,ZFMISC_1;
requirements ARITHM,BOOLE,NUMERALS,REAL,SUBSET;

:: notations BINOP_1;              :: uncomment these two lines to correct
:: constructors BINOP_1;         :: this example error

schemes FUNCT_3;
::>                      *834

begin

    reserve X for set;
    reserve x,y,z,z1 for set;

:: The absence of BINOP_1 causes f.(x,y) to be undefined, and this
:: triggers error 834

definition
    let X;
    defpred P[set,set,set] means $3 = $1 \/ $2;
    L1: for x,y,z,z1 st x in X & y in X &
        P[x,y,z] & P[x,y,z1] holds z=z1;
    L2: for x,y st x in X & y in X ex z st P[x,y,z];
    ex f being Function st dom f = [: X,X :] &
     for x,y st x in X & y in X holds
        P[x,y,f.(x,y)] from FUNCT_3:sch 1(L1,L2);    :: this justification triggers the error
end;