let X be non empty disjoint_with_NAT set ; :: thesis: ( ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,X) = FreeGenSetNSG ECIW-signature ,X & card X = card (FreeGenSetNSG ECIW-signature ,X) )
set S = ECIW-signature ;
set G = DTConUA ECIW-signature ,X;
A1: X = Terminals (DTConUA ECIW-signature ,X) by FREEALG:3;
set A = FreeUnivAlgNSG ECIW-signature ,X;
thus ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,X) = FreeGenSetNSG ECIW-signature ,X :: thesis: card X = card (FreeGenSetNSG ECIW-signature ,X)

proof

thus ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,X) c= FreeGenSetNSG ECIW-signature ,X :: according to XBOOLE_0:def 10 :: thesis: FreeGenSetNSG ECIW-signature ,X c= ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,X)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( x nin ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,X) or not x nin FreeGenSetNSG ECIW-signature ,X )
assume x in ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,X) ; :: thesis: not x nin FreeGenSetNSG ECIW-signature ,X
then consider y being Element of X such that
A2: x = y -tree {} by Th68;
reconsider y = y as Symbol of (DTConUA ECIW-signature ,X) by XBOOLE_0:def 3;
x = root-tree y by A2, TREES_4:20;
hence not x nin FreeGenSetNSG ECIW-signature ,X by A1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( x nin FreeGenSetNSG ECIW-signature ,X or not x nin ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,X) )
assume A3: x in FreeGenSetNSG ECIW-signature ,X ; :: thesis: not x nin ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,X)
then reconsider I = x as Element of (FreeUnivAlgNSG ECIW-signature ,X) ;
consider y being Symbol of (DTConUA ECIW-signature ,X) such that
A4: x = root-tree y and
A5: y in Terminals (DTConUA ECIW-signature ,X) by A3;
A6: x = y -tree {} by A4, TREES_4:20;
assume A7: x nin ElementaryInstructions (FreeUnivAlgNSG ECIW-signature ,X) ; :: thesis: contradiction

per cases ( I = EmptyIns (FreeUnivAlgNSG ECIW-signature ,X) or ex I1, I2 being Element of (FreeUnivAlgNSG ECIW-signature ,X) st
( I = I1 \; I2 & I1 <> I1 \; I2 & I2 <> I1 \; I2 ) or ex C, I1, I2 being Element of (FreeUnivAlgNSG ECIW-signature ,X) st I = if-then-else C,I1,I2 or ex C, J being Element of (FreeUnivAlgNSG ECIW-signature ,X) st I = while C,J ) by A7, Th53;

suppose I = EmptyIns (FreeUnivAlgNSG ECIW-signature ,X) ; :: thesis: contradiction

then x = 1 -tree {} by Th57;
then A8: y = 1 by A6, TREES_4:15;
X misses NAT by FREEALG:def 1;
hence contradiction by A1, A5, A8, XBOOLE_0:3; :: thesis: verum

end;

suppose ex I1, I2 being Element of (FreeUnivAlgNSG ECIW-signature ,X) st
( I = I1 \; I2 & I1 <> I1 \; I2 & I2 <> I1 \; I2 ) ; :: thesis: contradiction

then consider I1, I2 being Element of (FreeUnivAlgNSG ECIW-signature ,X) such that
A9: I = I1 \; I2 ;
x = 2 -tree I1,I2 by A9, Th59
.= 2 -tree <*I1,I2*> ;
hence contradiction by A6, TREES_4:15; :: thesis: verum

end;

suppose ex C, I1, I2 being Element of (FreeUnivAlgNSG ECIW-signature ,X) st I = if-then-else C,I1,I2 ; :: thesis: contradiction

then consider C, I1, I2 being Element of (FreeUnivAlgNSG ECIW-signature ,X) such that
A10: I = if-then-else C,I1,I2 ;
x = 3 -tree <*C,I1,I2*> by A10, Th63;
hence contradiction by A6, TREES_4:15; :: thesis: verum

end;

suppose ex C, J being Element of (FreeUnivAlgNSG ECIW-signature ,X) st I = while C,J ; :: thesis: contradiction

then consider C, J being Element of (FreeUnivAlgNSG ECIW-signature ,X) such that
A11: I = while C,J ;
x = 4 -tree C,J by A11, Th66
.= 4 -tree <*C,J*> ;
hence contradiction by A6, TREES_4:15; :: thesis: verum

end;

end;

end;

deffunc H₁( set ) -> set = root-tree $1;
consider f being Function such that
A12: ( dom f = X & ( for x being Element of X holds f . x = H₁(x) ) ) from FUNCT_1:sch 4();
A13: rng f = FreeGenSetNSG ECIW-signature ,X

proof

thus rng f c= FreeGenSetNSG ECIW-signature ,X :: according to XBOOLE_0:def 10 :: thesis: FreeGenSetNSG ECIW-signature ,X c= rng f

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( a nin rng f or not a nin FreeGenSetNSG ECIW-signature ,X )
assume a in rng f ; :: thesis: not a nin FreeGenSetNSG ECIW-signature ,X
then consider x being set such that
A14: x in X and
A15: a = f . x by A12, FUNCT_1:def 5;
reconsider s = x as Symbol of (DTConUA ECIW-signature ,X) by A14, XBOOLE_0:def 3;
a = H₁(x) by A12, A14, A15;
hence not a nin FreeGenSetNSG ECIW-signature ,X by A1, A14; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( a nin FreeGenSetNSG ECIW-signature ,X or not a nin rng f )
assume a in FreeGenSetNSG ECIW-signature ,X ; :: thesis: not a nin rng f
then consider s being Symbol of (DTConUA ECIW-signature ,X) such that
A16: a = root-tree s and
A17: s in X by A1;
reconsider s = s as Element of X by A17;
f . s = a by A12, A16;
hence not a nin rng f by A12, FUNCT_1:def 5; :: thesis: verum

end;

f is one-to-one

proof

let a, b be set ; :: according to FUNCT_1:def 8 :: thesis: ( a nin proj1 f or b nin proj1 f or not f . a = f . b or a = b )
assume that
A18: a in dom f and
A19: b in dom f ; :: thesis: ( not f . a = f . b or a = b )
reconsider x = a, y = b as Element of X by A12, A18, A19;
assume f . a = f . b ; :: thesis: a = b
then H₁(x) = f . b by A12
.= H₁(y) by A12 ;
hence a = b by TREES_4:4; :: thesis: verum

end;

then X, FreeGenSetNSG ECIW-signature ,X are_equipotent by A12, A13, WELLORD2:def 4;
hence card X = card (FreeGenSetNSG ECIW-signature ,X) by CARD_1:21; :: thesis: verum