let A be free preIfWhileAlgebra; for C, I1, I2 being Element of A
for n being Nat st if-then-else (C,I1,I2) in (ElementaryInstructions A) |^ n holds
ex i being Nat st
( n = i + 1 & C in (ElementaryInstructions A) |^ i & I1 in (ElementaryInstructions A) |^ i & I2 in (ElementaryInstructions A) |^ i )
set B = ElementaryInstructions A;
A1:
ElementaryInstructions A is GeneratorSet of A
by Def25;
let C, I1, I2 be Element of A; for n being Nat st if-then-else (C,I1,I2) in (ElementaryInstructions A) |^ n holds
ex i being Nat st
( n = i + 1 & C in (ElementaryInstructions A) |^ i & I1 in (ElementaryInstructions A) |^ i & I2 in (ElementaryInstructions A) |^ i )
if-then-else (C,I1,I2) nin ElementaryInstructions A
by Th51;
then A2:
if-then-else (C,I1,I2) nin (ElementaryInstructions A) |^ 0
by Th18;
let n be Nat; ( if-then-else (C,I1,I2) in (ElementaryInstructions A) |^ n implies ex i being Nat st
( n = i + 1 & C in (ElementaryInstructions A) |^ i & I1 in (ElementaryInstructions A) |^ i & I2 in (ElementaryInstructions A) |^ i ) )
assume A3:
if-then-else (C,I1,I2) in (ElementaryInstructions A) |^ n
; ex i being Nat st
( n = i + 1 & C in (ElementaryInstructions A) |^ i & I1 in (ElementaryInstructions A) |^ i & I2 in (ElementaryInstructions A) |^ i )
then consider i being Nat such that
A4:
n = i + 1
by A2, NAT_1:6;
take
i
; ( n = i + 1 & C in (ElementaryInstructions A) |^ i & I1 in (ElementaryInstructions A) |^ i & I2 in (ElementaryInstructions A) |^ i )
thus
n = i + 1
by A4; ( C in (ElementaryInstructions A) |^ i & I1 in (ElementaryInstructions A) |^ i & I2 in (ElementaryInstructions A) |^ i )
A5:
dom (Den ((In (3,(dom the charact of A))),A)) = 3 -tuples_on the carrier of A
by Th47;
A6:
for o being OperSymbol of A
for p being FinSequence st p in dom (Den (o,A)) & (Den (o,A)) . p in ElementaryInstructions A holds
o <> In (3,(dom the charact of A))
proof
let o be
OperSymbol of
A;
for p being FinSequence st p in dom (Den (o,A)) & (Den (o,A)) . p in ElementaryInstructions A holds
o <> In (3,(dom the charact of A))let p be
FinSequence;
( p in dom (Den (o,A)) & (Den (o,A)) . p in ElementaryInstructions A implies o <> In (3,(dom the charact of A)) )
assume that A7:
p in dom (Den (o,A))
and A8:
(Den (o,A)) . p in ElementaryInstructions A
and A9:
o = In (3,
(dom the charact of A))
;
contradiction
consider a,
b,
c being
object such that A10:
a in the
carrier of
A
and A11:
b in the
carrier of
A
and A12:
c in the
carrier of
A
and A13:
p = <*a,b,c*>
by A5, A7, A9, FINSEQ_2:139;
reconsider a =
a,
b =
b,
c =
c as
Element of
A by A10, A11, A12;
(Den (o,A)) . p = if-then-else (
a,
b,
c)
by A9, A13;
hence
contradiction
by A8, Th51;
verum
end;
<*C,I1,I2*> in dom (Den ((In (3,(dom the charact of A))),A))
by A5, FINSEQ_2:139;
then
rng <*C,I1,I2*> c= (ElementaryInstructions A) |^ i
by A1, A3, A4, A6, Th39;
then A14:
{C,I1,I2} c= (ElementaryInstructions A) |^ i
by FINSEQ_2:128;
A15:
C in {C,I1,I2}
by ENUMSET1:def 1;
A16:
I1 in {C,I1,I2}
by ENUMSET1:def 1;
I2 in {C,I1,I2}
by ENUMSET1:def 1;
hence
( C in (ElementaryInstructions A) |^ i & I1 in (ElementaryInstructions A) |^ i & I2 in (ElementaryInstructions A) |^ i )
by A14, A15, A16; verum