let A be free preIfWhileAlgebra; :: thesis: 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; :: thesis: 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 )
( I1 \; I2 <> I1 & I1 \; I2 <> I2 )
by Th73;
then
I1 \; I2 nin ElementaryInstructions A
by Th50;
then A2:
I1 \; I2 nin (ElementaryInstructions A) |^ 0
by Th18;
let n be Nat; :: thesis: ( 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 A3:
I1 \; I2 in (ElementaryInstructions A) |^ n
; :: thesis: ex i being Nat st
( n = i + 1 & I1 in (ElementaryInstructions A) |^ i & I2 in (ElementaryInstructions A) |^ i )
then
n > 0
by A2;
then
n >= 0 + 1
by NAT_1:13;
then consider i being Nat such that
A4:
n = 1 + i
by NAT_1:10;
take
i
; :: thesis: ( n = i + 1 & I1 in (ElementaryInstructions A) |^ i & I2 in (ElementaryInstructions A) |^ i )
thus
n = i + 1
by A4; :: thesis: ( I1 in (ElementaryInstructions A) |^ i & I2 in (ElementaryInstructions A) |^ i )
A5:
dom (Den (In 2,(dom the charact of A)),A) = 2 -tuples_on the carrier of A
by Th44;
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 2,(dom the charact of A)
proof
let o be
OperSymbol of
A;
:: thesis: 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;
:: thesis: ( p in dom (Den o,A) & (Den o,A) . p in ElementaryInstructions A implies o <> In 2,(dom the charact of A) )
assume A7:
(
p in dom (Den o,A) &
(Den o,A) . p in ElementaryInstructions A &
o = In 2,
(dom the charact of A) )
;
:: thesis: contradiction
then consider a,
b being
set such that A8:
(
a in the
carrier of
A &
b in the
carrier of
A &
p = <*a,b*> )
by A5, CATALG_1:10;
reconsider a =
a,
b =
b as
Element of
A by A8;
(
(Den o,A) . p = a \; b &
a \; b <> a &
a \; b <> b )
by A7, A8, Th73;
hence
contradiction
by A7, Th50;
:: thesis: verum
end;
<*I1,I2*> in dom (Den (In 2,(dom the charact of A)),A)
by A5, CATALG_1:10;
then
rng <*I1,I2*> c= (ElementaryInstructions A) |^ i
by A1, A3, A4, A6, Th39;
then
{I1,I2} c= (ElementaryInstructions A) |^ i
by FINSEQ_2:147;
hence
( I1 in (ElementaryInstructions A) |^ i & I2 in (ElementaryInstructions A) |^ i )
by ZFMISC_1:38; :: thesis: verum