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 not I in rng (Den ((In (3,(dom the charact of A))),A))assume
I in rng (Den ((In (3,(dom the charact of A))),A))
;
contradictionthen consider x being
object 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 3;
reconsider f = the
charact of
A . 3 as non
empty homogeneous quasi_total 3
-ary 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 SUBSET_1:def 8;
then dom (Den ((In (3,(dom the charact of A))),A)) =
(arity f) -tuples_on the
carrier of
A
by COMPUT_1:22
.=
3
-tuples_on the
carrier of
A
by COMPUT_1:def 21
;
then consider C,
I1,
I2 being
object 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:139;
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 not I in rng (Den ((In (4,(dom the charact of A))),A))assume
I in rng (Den ((In (4,(dom the charact of A))),A))
;
contradictionthen consider x being
object 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 3;
reconsider f = the
charact of
A . 4 as non
empty homogeneous quasi_total 2
-ary 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 SUBSET_1:def 8;
then dom (Den ((In (4,(dom the charact of A))),A)) =
(arity f) -tuples_on the
carrier of
A
by COMPUT_1:22
.=
2
-tuples_on the
carrier of
A
by COMPUT_1:def 21
;
then consider C,
J being
object 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:137;
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:56;
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