reconsider i = len p as Nat ;
let s1, s2 be XFinSequence of the InstructionsF of SCM+FSA; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: ( k < len pp1 implies pp1 . k = pp2 . k )
assume A12: k < len pp1 ; :: thesis: 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 ; :: thesis: verum
end;
hence s1 = s2 by A8, A11, A6, A9, AFINSQ_1:9; :: thesis: verum