let A be free preIfWhileAlgebra; for I1, I2 being Element of A
for n being Nat st I1 \; I2 in (ElementaryInstructions A) |^ n holds
ex i being Nat st
( n = i + 1 & I1 in (ElementaryInstructions A) |^ i & I2 in (ElementaryInstructions A) |^ i )
set B = ElementaryInstructions A;
A1:
ElementaryInstructions A is GeneratorSet of A
by Def25;
let I1, I2 be Element of A; for n being Nat st I1 \; I2 in (ElementaryInstructions A) |^ n holds
ex i being Nat st
( n = i + 1 & I1 in (ElementaryInstructions A) |^ i & I2 in (ElementaryInstructions A) |^ i )
A2:
I1 \; I2 <> I1
by Th73;
I1 \; I2 <> I2
by Th73;
then
I1 \; I2 nin ElementaryInstructions A
by A2, Th50;
then A3:
I1 \; I2 nin (ElementaryInstructions A) |^ 0
by Th18;
let n be Nat; ( I1 \; I2 in (ElementaryInstructions A) |^ n implies ex i being Nat st
( n = i + 1 & I1 in (ElementaryInstructions A) |^ i & I2 in (ElementaryInstructions A) |^ i ) )
assume A4:
I1 \; I2 in (ElementaryInstructions A) |^ n
; ex i being Nat st
( n = i + 1 & I1 in (ElementaryInstructions A) |^ i & I2 in (ElementaryInstructions A) |^ i )
then
n > 0
by A3;
then
n >= 0 + 1
by NAT_1:13;
then consider i being Nat such that
A5:
n = 1 + i
by NAT_1:10;
take
i
; ( n = i + 1 & I1 in (ElementaryInstructions A) |^ i & I2 in (ElementaryInstructions A) |^ i )
thus
n = i + 1
by A5; ( I1 in (ElementaryInstructions A) |^ i & I2 in (ElementaryInstructions A) |^ i )
A6:
dom (Den ((In (2,(dom the charact of A))),A)) = 2 -tuples_on the carrier of A
by Th44;
A7:
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 (2,(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 (2,(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 (2,(dom the charact of A)) )
assume that A8:
p in dom (Den (o,A))
and A9:
(Den (o,A)) . p in ElementaryInstructions A
and A10:
o = In (2,
(dom the charact of A))
;
contradiction
consider a,
b being
object such that A11:
a in the
carrier of
A
and A12:
b in the
carrier of
A
and A13:
p = <*a,b*>
by A6, A8, A10, FINSEQ_2:137;
reconsider a =
a,
b =
b as
Element of
A by A11, A12;
A14:
a \; b <> a
by Th73;
a \; b <> b
by Th73;
hence
contradiction
by A9, A10, A13, A14, Th50;
verum
end;
<*I1,I2*> in dom (Den ((In (2,(dom the charact of A))),A))
by A6, FINSEQ_2:137;
then
rng <*I1,I2*> c= (ElementaryInstructions A) |^ i
by A1, A4, A5, A7, Th39;
then
{I1,I2} c= (ElementaryInstructions A) |^ i
by FINSEQ_2:127;
hence
( I1 in (ElementaryInstructions A) |^ i & I2 in (ElementaryInstructions A) |^ i )
by ZFMISC_1:32; verum