let A be preIfWhileAlgebra; :: thesis: Generators A c= ElementaryInstructions A
let x be object ; :: according to TARSKI:def 3 :: thesis: ( x nin Generators A or not x nin ElementaryInstructions A )
assume that
A1: x in Generators A and
A2: x nin ElementaryInstructions A ; :: thesis: contradiction
reconsider x = x as Element of A by A1;
dom (Den ((In (1,(dom the charact of A))),A)) = {{}} by Th42;
then A3: {} in dom (Den ((In (1,(dom the charact of A))),A)) by TARSKI:def 1;
per cases ( x = EmptyIns A or ex I1, I2 being Element of A st
( x = I1 \; I2 & I1 <> I1 \; I2 & I2 <> I1 \; I2 ) or ex C, I1, I2 being Element of A st x = if-then-else (C,I1,I2) or ex C, J being Element of A st x = while (C,J) ) by A2, Th53;
suppose x = EmptyIns A ; :: thesis: contradiction
then x in rng (Den ((In (1,(dom the charact of A))),A)) by A3, FUNCT_1:3;
hence contradiction by A1, Th26; :: thesis: verum
end;
suppose ex I1, I2 being Element of A st
( x = I1 \; I2 & I1 <> I1 \; I2 & I2 <> I1 \; I2 ) ; :: thesis: contradiction
then consider I1, I2 being Element of A such that
A4: x = I1 \; I2 and
I1 <> I1 \; I2 and
I2 <> I1 \; I2 ;
dom (Den ((In (2,(dom the charact of A))),A)) = 2 -tuples_on the carrier of A by Th44;
then <*I1,I2*> in dom (Den ((In (2,(dom the charact of A))),A)) by FINSEQ_2:137;
then x in rng (Den ((In (2,(dom the charact of A))),A)) by A4, FUNCT_1:3;
hence contradiction by A1, Th26; :: thesis: verum
end;
suppose ex C, I1, I2 being Element of A st x = if-then-else (C,I1,I2) ; :: thesis: contradiction
then consider C, I1, I2 being Element of A such that
A5: x = if-then-else (C,I1,I2) ;
dom (Den ((In (3,(dom the charact of A))),A)) = 3 -tuples_on the carrier of A by Th47;
then <*C,I1,I2*> in dom (Den ((In (3,(dom the charact of A))),A)) by FINSEQ_2:139;
then x in rng (Den ((In (3,(dom the charact of A))),A)) by A5, FUNCT_1:3;
hence contradiction by A1, Th26; :: thesis: verum
end;
suppose ex C, J being Element of A st x = while (C,J) ; :: thesis: contradiction
then consider C, J being Element of A such that
A6: x = while (C,J) ;
dom (Den ((In (4,(dom the charact of A))),A)) = 2 -tuples_on the carrier of A by Th48;
then <*C,J*> in dom (Den ((In (4,(dom the charact of A))),A)) by FINSEQ_2:137;
then x in rng (Den ((In (4,(dom the charact of A))),A)) by A6, FUNCT_1:3;
hence contradiction by A1, Th26; :: thesis: verum
end;
end;