let X be non empty disjoint_with_NAT set ; :: thesis: for I being Element of (FreeUnivAlgNSG (ECIW-signature,X)) st I in ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,X)) holds
ex x being Element of X st I = x -tree {}
set S = ECIW-signature ;
set A = FreeUnivAlgNSG (ECIW-signature,X);
let I be Element of (FreeUnivAlgNSG (ECIW-signature,X)); :: thesis: ( I in ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,X)) implies ex x being Element of X st I = x -tree {} )
assume A1: I in ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,X)) ; :: thesis: ex x being Element of X st I = x -tree {}
per cases ( ex x being Element of X st I = root-tree x or ex n being Nat ex p being FinSequence of (FreeUnivAlgNSG (ECIW-signature,X)) st
( n in Seg 4 & I = n -tree p & len p = ECIW-signature . n ) ) by Th56;
suppose ex x being Element of X st I = root-tree x ; :: thesis: ex x being Element of X st I = x -tree {}
then consider x being Element of X such that
A2: I = root-tree x ;
root-tree x = x -tree {} by TREES_4:20;
hence ex x being Element of X st I = x -tree {} by A2; :: thesis: verum
end;
suppose ex n being Nat ex p being FinSequence of (FreeUnivAlgNSG (ECIW-signature,X)) st
( n in Seg 4 & I = n -tree p & len p = ECIW-signature . n ) ; :: thesis: ex x being Element of X st I = x -tree {}
then consider n being Nat, p being FinSequence of (FreeUnivAlgNSG (ECIW-signature,X)) such that
A3: n in Seg 4 and
A4: I = n -tree p and
len p = ECIW-signature . n ;
per cases ( n = 1 or n = 2 or n = 3 or n = 4 ) by A3, ENUMSET1:def 2, FINSEQ_3:2;
suppose A6: n = 2 ; :: thesis: ex x being Element of X st I = x -tree {}
then consider I1, I2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) such that
A7: p = <*I1,I2*> by A4, Th60;
A8: I = n -tree (I1,I2) by A4, A7
.= I1 \; I2 by A6, Th59 ;
then A9: I <> I1 by Th61;
I <> I2 by A8, Th61;
hence ex x being Element of X st I = x -tree {} by A1, A8, A9, Th50; :: thesis: verum
end;
suppose A10: n = 3 ; :: thesis: ex x being Element of X st I = x -tree {}
then consider C, I1, I2 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) such that
A11: p = <*C,I1,I2*> by A4, Th64;
I = if-then-else (C,I1,I2) by A4, A10, A11, Th63;
hence ex x being Element of X st I = x -tree {} by A1, Th51; :: thesis: verum
end;
suppose A12: n = 4 ; :: thesis: ex x being Element of X st I = x -tree {}
then consider C, I9 being Element of (FreeUnivAlgNSG (ECIW-signature,X)) such that
A13: p = <*C,I9*> by A4, Th67;
I = n -tree (C,I9) by A4, A13
.= while (C,I9) by A12, Th66 ;
hence ex x being Element of X st I = x -tree {} by A1, Th52; :: thesis: verum
end;
end;
end;
end;