let X be non empty disjoint_with_NAT set ; ( 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)
card X = card (FreeGenSetNSG (ECIW-signature,X))proof
thus
ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,X)) c= FreeGenSetNSG (
ECIW-signature,
X)
XBOOLE_0:def 10 FreeGenSetNSG (ECIW-signature,X) c= ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,X))
let x be
object ;
TARSKI:def 3 ( x nin FreeGenSetNSG (ECIW-signature,X) or not x nin ElementaryInstructions (FreeUnivAlgNSG (ECIW-signature,X)) )
assume A3:
x in FreeGenSetNSG (
ECIW-signature,
X)
;
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))
;
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;
end;
end;
deffunc H1( object ) -> set = root-tree $1;
consider f being Function such that
A12:
( dom f = X & ( for x being Element of X holds f . x = H1(x) ) )
from FUNCT_1:sch 4();
A13:
rng f = FreeGenSetNSG (ECIW-signature,X)
f is one-to-one
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; verum