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 object ; :: 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 object ; :: 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₁( object ) -> 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 object ; :: 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 object such that
A14: x in X and
A15: a = f . x by A12, FUNCT_1: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 object ; :: 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 3; :: thesis: verum

end;

f is one-to-one

proof

let a, b be object ; :: according to FUNCT_1:def 4 :: thesis: ( a nin dom f or b nin dom 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:5; :: thesis: verum