let A be preIfWhileAlgebra; for I being Element of A holds
( not I nin ElementaryInstructions A or I = EmptyIns A or ex I1, I2 being Element of A st
( I = I1 \; I2 & I1 <> I1 \; I2 & I2 <> I1 \; I2 ) or ex C, I1, I2 being Element of A st I = if-then-else C,I1,I2 or ex C, J being Element of A st I = while C,J )
let I be Element of A; ( not I nin ElementaryInstructions A or I = EmptyIns A or ex I1, I2 being Element of A st
( I = I1 \; I2 & I1 <> I1 \; I2 & I2 <> I1 \; I2 ) or ex C, I1, I2 being Element of A st I = if-then-else C,I1,I2 or ex C, J being Element of A st I = while C,J )
assume that
A1:
I nin ElementaryInstructions A
and
A2:
I <> EmptyIns A
and
A3:
for I1, I2 being Element of A st I = I1 \; I2 & I1 <> I1 \; I2 holds
I2 = I1 \; I2
and
A4:
for C, I1, I2 being Element of A holds I <> if-then-else C,I1,I2
and
A5:
for C, J being Element of A holds I <> while C,J
; contradiction
A6:
now assume
I in rng (Den (In 3,(dom the charact of A)),A)
;
contradictionthen consider x being
set such that A7:
x in dom (Den (In 3,(dom the charact of A)),A)
and A8:
I = (Den (In 3,(dom the charact of A)),A) . x
by FUNCT_1:def 5;
reconsider f = the
charact of
A . 3 as non
empty homogeneous quasi_total ternary PartFunc of
(the carrier of A * ),the
carrier of
A by Def12;
3
in dom the
charact of
A
by Def12;
then
In 3,
(dom the charact of A) = 3
by FUNCT_7:def 1;
then dom (Den (In 3,(dom the charact of A)),A) =
(arity f) -tuples_on the
carrier of
A
by COMPUT_1:25
.=
3
-tuples_on the
carrier of
A
by COMPUT_1:def 27
;
then consider C,
I1,
I2 being
set such that A9:
C in the
carrier of
A
and A10:
I1 in the
carrier of
A
and A11:
I2 in the
carrier of
A
and A12:
x = <*C,I1,I2*>
by A7, FINSEQ_2:159;
reconsider C =
C,
I1 =
I1,
I2 =
I2 as
Element of
A by A9, A10, A11;
I = if-then-else C,
I1,
I2
by A8, A12;
hence
contradiction
by A4;
verum end;
A13:
now assume
I in rng (Den (In 4,(dom the charact of A)),A)
;
contradictionthen consider x being
set such that A14:
x in dom (Den (In 4,(dom the charact of A)),A)
and A15:
I = (Den (In 4,(dom the charact of A)),A) . x
by FUNCT_1:def 5;
reconsider f = the
charact of
A . 4 as non
empty homogeneous quasi_total binary PartFunc of
(the carrier of A * ),the
carrier of
A by Def13;
4
in dom the
charact of
A
by Def13;
then
In 4,
(dom the charact of A) = 4
by FUNCT_7:def 1;
then dom (Den (In 4,(dom the charact of A)),A) =
(arity f) -tuples_on the
carrier of
A
by COMPUT_1:25
.=
2
-tuples_on the
carrier of
A
by COMPUT_1:def 26
;
then consider C,
J being
set such that A16:
C in the
carrier of
A
and A17:
J in the
carrier of
A
and A18:
x = <*C,J*>
by A14, FINSEQ_2:157;
reconsider C =
C,
J =
J as
Element of
A by A16, A17;
I = while C,
J
by A15, A18;
hence
contradiction
by A5;
verum end;
A19:
I nin { (I1 \; I2) where I1, I2 is Algorithm of A : ( I1 <> I1 \; I2 & I2 <> I1 \; I2 ) }
by A3;
I in the carrier of A \ {(EmptyIns A)}
by A2, ZFMISC_1:64;
then
I in (the carrier of A \ {(EmptyIns A)}) \ (rng (Den (In 3,(dom the charact of A)),A))
by A6, XBOOLE_0:def 5;
then
I in ((the carrier of A \ {(EmptyIns A)}) \ (rng (Den (In 3,(dom the charact of A)),A))) \ (rng (Den (In 4,(dom the charact of A)),A))
by A13, XBOOLE_0:def 5;
hence
contradiction
by A1, A19, XBOOLE_0:def 5; verum