reconsider i = len p as Nat ;
let s1, s2 be XFinSequence of the InstructionsF of SCM+FSA; ( ex pp being XFinSequence of the InstructionsF of SCM+FSA ^omega st
( len pp = len p & ( for k being Nat st k < len pp holds
ex i being Integer st
( i = p . (k + 1) & pp . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) ) & s1 = FlattenSeq pp ) & ex pp being XFinSequence of the InstructionsF of SCM+FSA ^omega st
( len pp = len p & ( for k being Nat st k < len pp holds
ex i being Integer st
( i = p . (k + 1) & pp . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) ) & s2 = FlattenSeq pp ) implies s1 = s2 )
assume that
A4:
ex pp being XFinSequence of the InstructionsF of SCM+FSA ^omega st
( len pp = len p & ( for k being Nat st k < len pp holds
ex i being Integer st
( i = p . (k + 1) & pp . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) ) & s1 = FlattenSeq pp )
and
A5:
ex pp being XFinSequence of the InstructionsF of SCM+FSA ^omega st
( len pp = len p & ( for k being Nat st k < len pp holds
ex i being Integer st
( i = p . (k + 1) & pp . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) ) & s2 = FlattenSeq pp )
; s1 = s2
consider pp1 being XFinSequence of the InstructionsF of SCM+FSA ^omega such that
A6:
len pp1 = len p
and
A7:
for k being Nat st k < len pp1 holds
ex i being Integer st
( i = p . (k + 1) & pp1 . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> )
and
A8:
s1 = FlattenSeq pp1
by A4;
consider pp2 being XFinSequence of the InstructionsF of SCM+FSA ^omega such that
A9:
len pp2 = len p
and
A10:
for k being Nat st k < len pp2 holds
ex i being Integer st
( i = p . (k + 1) & pp2 . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i))) ^ <%((f,(intloc 1)) := (intloc 2))%> )
and
A11:
s2 = FlattenSeq pp2
by A5;
for k being Nat st k < len pp1 holds
pp1 . k = pp2 . k
proof
let k be
Nat;
( k < len pp1 implies pp1 . k = pp2 . k )
assume A12:
k < len pp1
;
pp1 . k = pp2 . k
( ex
i1 being
Integer st
(
i1 = p . (k + 1) &
pp1 . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i1))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) & ex
i2 being
Integer st
(
i2 = p . (k + 1) &
pp2 . k = ((aSeq ((intloc 1),(k + 1))) ^ (aSeq ((intloc 2),i2))) ^ <%((f,(intloc 1)) := (intloc 2))%> ) )
by A7, A10, A12, A6, A9;
hence
pp1 . k = pp2 . k
;
verum
end;
hence
s1 = s2
by A8, A11, A6, A9, AFINSQ_1:9; verum