let p1, p2 be Instruction-Sequence of SCM+FSA; :: thesis:
let i, k be Nat; :: thesis:
let t be FinPartState of SCM+FSA; :: thesis:
let p be Program of ; :: thesis:
let s1, s2 be State of SCM+FSA; :: thesis:
set Dloc = ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p);
assume that
A1: k <= i and
A2: p c= p1 and
A3: p c= p2 and
A4: dom t c= Int-Locations \/ FinSeq-Locations and
A5: for j being Nat holds
( IC (Comput (p1,s1,j)) in dom p & IC (Comput (p2,s2,j)) in dom p ) and
A6: (Comput (p1,s1,k)) . (IC ) = (Comput (p2,s2,k)) . (IC ) and
A7: (Comput (p1,s1,k)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) = (Comput (p2,s2,k)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) ; :: thesis:
consider m being Nat such that
A8: i = k + m by A1, NAT_1:10;
reconsider m = m as Nat ;
A9: i = k + m by A8;
A10: UsedILoc p c= ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) by XBOOLE_1:7;
((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) = ((dom t) \/ (UsedILoc p)) \/ (UsedI*Loc p) by XBOOLE_1:4;
then A11: UsedI*Loc p c= ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) by XBOOLE_1:7;
defpred S₁[ Nat] means ( (Comput (p1,s1,(k + $1))) . (IC ) = (Comput (p2,s2,(k + $1))) . (IC ) & (Comput (p1,s1,(k + $1))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) = (Comput (p2,s2,(k + $1))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) );
A12: S₁[ 0 ] by A6, A7;

A13: now :: thesis:

let m be Nat; :: thesis:
assume A14: S₁[m] ; :: thesis:
set sk1 = Comput (p1,s1,(k + m));
set sk11 = Comput (p1,s1,(k + (m + 1)));
set i1 = CurInstr (p1,(Comput (p1,s1,(k + m))));
set sk2 = Comput (p2,s2,(k + m));
set sk12 = Comput (p2,s2,(k + (m + 1)));
set i2 = CurInstr (p2,(Comput (p2,s2,(k + m))));
A15: IC (Comput (p1,s1,(k + m))) in dom p by A5;
A16: p2 /. (IC (Comput (p2,s2,(k + m)))) = p2 . (IC (Comput (p2,s2,(k + m)))) by PBOOLE:143;
A17: p1 /. (IC (Comput (p1,s1,(k + m)))) = p1 . (IC (Comput (p1,s1,(k + m)))) by PBOOLE:143;
CurInstr (p1,(Comput (p1,s1,(k + m)))) = p . (IC (Comput (p1,s1,(k + m)))) by A2, A15, A17, GRFUNC_1:2;
then A18: CurInstr (p1,(Comput (p1,s1,(k + m)))) in rng p by A15, FUNCT_1:def 3;
A19: CurInstr (p2,(Comput (p2,s2,(k + m)))) = (p2 | (dom p)) . (IC (Comput (p2,s2,(k + m)))) by A16, A5, FUNCT_1:49
.= (p1 | (dom p)) . (IC (Comput (p1,s1,(k + m)))) by A2, A3, A14, GRFUNC_1:33
.= CurInstr (p1,(Comput (p1,s1,(k + m)))) by A17, A5, FUNCT_1:49 ;
A20: Comput (p1,s1,(k + (m + 1))) = Comput (p1,s1,((k + m) + 1))
.= Following (p1,(Comput (p1,s1,(k + m)))) by EXTPRO_1:3
.= Exec ((CurInstr (p1,(Comput (p1,s1,(k + m))))),(Comput (p1,s1,(k + m)))) ;
A21: Comput (p2,s2,(k + (m + 1))) = Comput (p2,s2,((k + m) + 1))
.= Following (p2,(Comput (p2,s2,(k + m)))) by EXTPRO_1:3
.= Exec ((CurInstr (p2,(Comput (p2,s2,(k + m))))),(Comput (p2,s2,(k + m)))) ;
A22: dom (Comput (p1,s1,(k + (m + 1)))) = the carrier of SCM+FSA by PARTFUN1:def 2
.= dom (Comput (p2,s2,(k + (m + 1)))) by PARTFUN1:def 2 ;
not not InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 0 & ... & not InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 12 by SCMFSA_2:16;

per cases ;

suppose InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 0 ; :: thesis:

then A23: CurInstr (p1,(Comput (p1,s1,(k + m)))) = halt SCM+FSA by SCMFSA_2:95;
then Comput (p1,s1,(k + (m + 1))) = Comput (p1,s1,(k + m)) by A20, EXTPRO_1:def 3;
hence S₁[m + 1] by A14, A19, A21, A23, EXTPRO_1:def 3; :: thesis:

end;

suppose InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 1 ; :: thesis:

then consider da, db being Int-Location such that
A24: CurInstr (p1,(Comput (p1,s1,(k + m)))) = da := db by SCMFSA_2:30;
A25: (Comput (p1,s1,(k + (m + 1)))) . (IC ) = (IC (Comput (p1,s1,(k + m)))) + 1 by A20, A24, SCMFSA_2:63
.= (Comput (p2,s2,(k + (m + 1)))) . (IC ) by A14, A19, A21, A24, SCMFSA_2:63 ;

now :: thesis:

let x be set ; :: thesis:
assume A26: x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) ; :: thesis:

per cases by A4, A26, Th12;

suppose A27: x is Int-Location ; :: thesis:

per cases ;

suppose A28: x = da ; :: thesis:

then A29: (Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . db by A19, A21, A24, SCMFSA_2:63;
A30: db in UsedILoc p by A18, A24, Th6;
then (Comput (p1,s1,(k + m))) . db = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . db by A10, A14, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . db by A10, A30, FUNCT_1:49 ;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A20, A24, A28, A29, SCMFSA_2:63; :: thesis:

end;

suppose A31: x <> da ; :: thesis:

then A32: (Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x by A19, A21, A24, A27, SCMFSA_2:63;
(Comput (p1,s1,(k + m))) . x = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x by A14, A26, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . x by A26, FUNCT_1:49 ;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A20, A24, A27, A31, A32, SCMFSA_2:63; :: thesis:

end;

suppose A33: x is FinSeq-Location ; :: thesis:

then A34: (Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x by A19, A21, A24, SCMFSA_2:63;
(Comput (p1,s1,(k + m))) . x = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x by A14, A26, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . x by A26, FUNCT_1:49 ;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A20, A24, A33, A34, SCMFSA_2:63; :: thesis:

end;

hence S₁[m + 1] by A22, A25, FUNCT_1:96; :: thesis:

end;

suppose InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 2 ; :: thesis:

then consider da, db being Int-Location such that
A35: CurInstr (p1,(Comput (p1,s1,(k + m)))) = AddTo (da,db) by SCMFSA_2:31;
A36: (Comput (p1,s1,(k + (m + 1)))) . (IC ) = (IC (Comput (p1,s1,(k + m)))) + 1 by A20, A35, SCMFSA_2:64
.= (Comput (p2,s2,(k + (m + 1)))) . (IC ) by A14, A19, A21, A35, SCMFSA_2:64 ;

now :: thesis:

let x be set ; :: thesis:
assume A37: x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) ; :: thesis:

per cases by A4, A37, Th12;

suppose A38: x is Int-Location ; :: thesis:

per cases ;

suppose A39: x = da ; :: thesis:

then A40: (Comput (p2,s2,(k + (m + 1)))) . x = ((Comput (p2,s2,(k + m))) . da) + ((Comput (p2,s2,(k + m))) . db) by A19, A21, A35, SCMFSA_2:64;
A41: da in UsedILoc p by A18, A35, Th6;
then A42: (Comput (p1,s1,(k + m))) . da = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . da by A10, A14, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . da by A10, A41, FUNCT_1:49 ;
A43: db in UsedILoc p by A18, A35, Th6;
then (Comput (p1,s1,(k + m))) . db = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . db by A10, A14, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . db by A10, A43, FUNCT_1:49 ;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A20, A35, A39, A40, A42, SCMFSA_2:64; :: thesis:

end;

suppose A44: x <> da ; :: thesis:

then A45: (Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x by A19, A21, A35, A38, SCMFSA_2:64;
(Comput (p1,s1,(k + m))) . x = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x by A14, A37, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . x by A37, FUNCT_1:49 ;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A20, A35, A38, A44, A45, SCMFSA_2:64; :: thesis:

end;

suppose A46: x is FinSeq-Location ; :: thesis:

then A47: (Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x by A19, A21, A35, SCMFSA_2:64;
(Comput (p1,s1,(k + m))) . x = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x by A14, A37, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . x by A37, FUNCT_1:49 ;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A20, A35, A46, A47, SCMFSA_2:64; :: thesis:

end;

hence S₁[m + 1] by A22, A36, FUNCT_1:96; :: thesis:

end;

suppose InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 3 ; :: thesis:

then consider da, db being Int-Location such that
A48: CurInstr (p1,(Comput (p1,s1,(k + m)))) = SubFrom (da,db) by SCMFSA_2:32;
A49: (Comput (p1,s1,(k + (m + 1)))) . (IC ) = (IC (Comput (p1,s1,(k + m)))) + 1 by A20, A48, SCMFSA_2:65
.= (Comput (p2,s2,(k + (m + 1)))) . (IC ) by A14, A19, A21, A48, SCMFSA_2:65 ;

now :: thesis:

let x be set ; :: thesis:
assume A50: x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) ; :: thesis:

per cases by A4, A50, Th12;

suppose A51: x is Int-Location ; :: thesis:

per cases ;

suppose A52: x = da ; :: thesis:

then A53: (Comput (p2,s2,(k + (m + 1)))) . x = ((Comput (p2,s2,(k + m))) . da) - ((Comput (p2,s2,(k + m))) . db) by A19, A21, A48, SCMFSA_2:65;
A54: da in UsedILoc p by A18, A48, Th6;
then A55: (Comput (p1,s1,(k + m))) . da = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . da by A10, A14, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . da by A10, A54, FUNCT_1:49 ;
A56: db in UsedILoc p by A18, A48, Th6;
then (Comput (p1,s1,(k + m))) . db = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . db by A10, A14, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . db by A10, A56, FUNCT_1:49 ;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A20, A48, A52, A53, A55, SCMFSA_2:65; :: thesis:

end;

suppose A57: x <> da ; :: thesis:

then A58: (Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x by A19, A21, A48, A51, SCMFSA_2:65;
(Comput (p1,s1,(k + m))) . x = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x by A14, A50, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . x by A50, FUNCT_1:49 ;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A20, A48, A51, A57, A58, SCMFSA_2:65; :: thesis:

end;

suppose A59: x is FinSeq-Location ; :: thesis:

then A60: (Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x by A19, A21, A48, SCMFSA_2:65;
(Comput (p1,s1,(k + m))) . x = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x by A14, A50, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . x by A50, FUNCT_1:49 ;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A20, A48, A59, A60, SCMFSA_2:65; :: thesis:

end;

hence S₁[m + 1] by A22, A49, FUNCT_1:96; :: thesis:

end;

suppose InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 4 ; :: thesis:

then consider da, db being Int-Location such that
A61: CurInstr (p1,(Comput (p1,s1,(k + m)))) = MultBy (da,db) by SCMFSA_2:33;
A62: (Comput (p1,s1,(k + (m + 1)))) . (IC ) = (IC (Comput (p1,s1,(k + m)))) + 1 by A20, A61, SCMFSA_2:66
.= (Comput (p2,s2,(k + (m + 1)))) . (IC ) by A14, A19, A21, A61, SCMFSA_2:66 ;

now :: thesis:

let x be set ; :: thesis:
assume A63: x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) ; :: thesis:

per cases by A4, A63, Th12;

suppose A64: x is Int-Location ; :: thesis:

per cases ;

suppose A65: x = da ; :: thesis:

then A66: (Comput (p2,s2,(k + (m + 1)))) . x = ((Comput (p2,s2,(k + m))) . da) * ((Comput (p2,s2,(k + m))) . db) by A19, A21, A61, SCMFSA_2:66;
A67: da in UsedILoc p by A18, A61, Th6;
then A68: (Comput (p1,s1,(k + m))) . da = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . da by A10, A14, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . da by A10, A67, FUNCT_1:49 ;
A69: db in UsedILoc p by A18, A61, Th6;
then (Comput (p1,s1,(k + m))) . db = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . db by A10, A14, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . db by A10, A69, FUNCT_1:49 ;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A20, A61, A65, A66, A68, SCMFSA_2:66; :: thesis:

end;

suppose A70: x <> da ; :: thesis:

then A71: (Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x by A19, A21, A61, A64, SCMFSA_2:66;
(Comput (p1,s1,(k + m))) . x = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x by A14, A63, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . x by A63, FUNCT_1:49 ;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A20, A61, A64, A70, A71, SCMFSA_2:66; :: thesis:

end;

suppose A72: x is FinSeq-Location ; :: thesis:

then A73: (Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x by A19, A21, A61, SCMFSA_2:66;
(Comput (p1,s1,(k + m))) . x = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x by A14, A63, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . x by A63, FUNCT_1:49 ;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A20, A61, A72, A73, SCMFSA_2:66; :: thesis:

end;

hence S₁[m + 1] by A22, A62, FUNCT_1:96; :: thesis:

end;

suppose InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 5 ; :: thesis:

then consider da, db being Int-Location such that
A74: CurInstr (p1,(Comput (p1,s1,(k + m)))) = Divide (da,db) by SCMFSA_2:34;
A75: (Comput (p1,s1,(k + (m + 1)))) . (IC ) = (IC (Comput (p1,s1,(k + m)))) + 1 by A20, A74, SCMFSA_2:67
.= (Comput (p2,s2,(k + (m + 1)))) . (IC ) by A14, A19, A21, A74, SCMFSA_2:67 ;

now :: thesis:

let x be set ; :: thesis:
assume A76: x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) ; :: thesis:

per cases by A4, A76, Th12;

suppose A77: x is Int-Location ; :: thesis:

A78: da in UsedILoc p by A18, A74, Th6;
then A79: (Comput (p1,s1,(k + m))) . da = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . da by A10, A14, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . da by A10, A78, FUNCT_1:49 ;
A80: db in UsedILoc p by A18, A74, Th6;
then A81: (Comput (p1,s1,(k + m))) . db = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . db by A10, A14, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . db by A10, A80, FUNCT_1:49 ;
A82: (Comput (p1,s1,(k + m))) . x = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x by A14, A76, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . x by A76, FUNCT_1:49 ;

now :: thesis:

per cases ;

suppose A83: da <> db ; :: thesis:

per cases ;

suppose A84: x = da ; :: thesis:

then (Comput (p1,s1,(k + (m + 1)))) . x = ((Comput (p1,s1,(k + m))) . da) div ((Comput (p1,s1,(k + m))) . db) by A20, A74, A83, SCMFSA_2:67;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A19, A21, A74, A79, A81, A83, A84, SCMFSA_2:67; :: thesis:

end;

suppose A85: x = db ; :: thesis:

then (Comput (p1,s1,(k + (m + 1)))) . x = ((Comput (p1,s1,(k + m))) . da) mod ((Comput (p1,s1,(k + m))) . db) by A20, A74, SCMFSA_2:67;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A19, A21, A74, A79, A81, A85, SCMFSA_2:67; :: thesis:

end;

suppose A86: ( x <> da & x <> db ) ; :: thesis:

then (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p1,s1,(k + m))) . x by A20, A74, A77, SCMFSA_2:67;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A19, A21, A74, A77, A82, A86, SCMFSA_2:67; :: thesis:

end;

suppose A87: da = db ; :: thesis:

now :: thesis:

per cases ;

case A88: x = da ; :: thesis:

then (Comput (p1,s1,(k + (m + 1)))) . x = ((Comput (p1,s1,(k + m))) . da) mod ((Comput (p1,s1,(k + m))) . da) by A20, A74, A87, SCMFSA_2:68;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A19, A21, A74, A79, A87, A88, SCMFSA_2:68; :: thesis:

end;

case A89: x <> da ; :: thesis:

then (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p1,s1,(k + m))) . x by A20, A74, A77, A87, SCMFSA_2:68;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A19, A21, A74, A77, A82, A87, A89, SCMFSA_2:68; :: thesis:

end;

hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x ; :: thesis:

end;

hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x ; :: thesis:

end;

suppose A90: x is FinSeq-Location ; :: thesis:

then A91: (Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x by A19, A21, A74, SCMFSA_2:67;
(Comput (p1,s1,(k + m))) . x = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x by A14, A76, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . x by A76, FUNCT_1:49 ;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A20, A74, A90, A91, SCMFSA_2:67; :: thesis:

end;

hence S₁[m + 1] by A22, A75, FUNCT_1:96; :: thesis:

end;

suppose InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 6 ; :: thesis:

then consider lb being Nat such that
A92: CurInstr (p1,(Comput (p1,s1,(k + m)))) = goto lb by SCMFSA_2:35;
A93: (Comput (p1,s1,(k + (m + 1)))) . (IC ) = lb by A20, A92, SCMFSA_2:69
.= (Comput (p2,s2,(k + (m + 1)))) . (IC ) by A19, A21, A92, SCMFSA_2:69 ;

now :: thesis:

let x be set ; :: thesis:
assume A94: x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) ; :: thesis:
then A95: (Comput (p1,s1,(k + m))) . x = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x by A14, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . x by A94, FUNCT_1:49 ;

per cases by A4, A94, Th12;

suppose A96: x is Int-Location ; :: thesis:

then (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p1,s1,(k + m))) . x by A20, A92, SCMFSA_2:69;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A19, A21, A92, A95, A96, SCMFSA_2:69; :: thesis:

end;

suppose A97: x is FinSeq-Location ; :: thesis:

end;

hence S₁[m + 1] by A22, A93, FUNCT_1:96; :: thesis:

end;

suppose InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 7 ; :: thesis:

then consider lb being Nat, da being Int-Location such that
A98: CurInstr (p1,(Comput (p1,s1,(k + m)))) = da =0_goto lb by SCMFSA_2:36;
A99: da in UsedILoc p by A18, A98, Th7;
then A100: (Comput (p1,s1,(k + m))) . da = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . da by A10, A14, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . da by A10, A99, FUNCT_1:49 ;

A101: now :: thesis:

per cases ) . da = 0 or (Comput (p1,s1,(k + m))) . da <> 0 ) ;

suppose A102: (Comput (p1,s1,(k + m))) . da = 0 ; :: thesis:

hence (Comput (p1,s1,(k + (m + 1)))) . (IC ) = lb by A20, A98, SCMFSA_2:70
.= (Comput (p2,s2,(k + (m + 1)))) . (IC ) by A19, A21, A98, A100, A102, SCMFSA_2:70 ;
:: thesis:

end;

suppose A103: (Comput (p1,s1,(k + m))) . da <> 0 ; :: thesis:

hence (Comput (p1,s1,(k + (m + 1)))) . (IC ) = (IC (Comput (p2,s2,(k + m)))) + 1 by A14, A20, A98, SCMFSA_2:70
.= (Comput (p2,s2,(k + (m + 1)))) . (IC ) by A19, A21, A98, A100, A103, SCMFSA_2:70 ;
:: thesis:

end;

now :: thesis:

let x be set ; :: thesis:
assume A104: x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) ; :: thesis:
then A105: (Comput (p1,s1,(k + m))) . x = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x by A14, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . x by A104, FUNCT_1:49 ;

per cases by A4, A104, Th12;

suppose A106: x is Int-Location ; :: thesis:

then (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p1,s1,(k + m))) . x by A20, A98, SCMFSA_2:70;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A19, A21, A98, A105, A106, SCMFSA_2:70; :: thesis:

end;

suppose A107: x is FinSeq-Location ; :: thesis:

end;

hence S₁[m + 1] by A22, A101, FUNCT_1:96; :: thesis:

end;

suppose InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 8 ; :: thesis:

then consider lb being Nat, da being Int-Location such that
A108: CurInstr (p1,(Comput (p1,s1,(k + m)))) = da >0_goto lb by SCMFSA_2:37;
A109: da in UsedILoc p by A18, A108, Th7;
then A110: (Comput (p1,s1,(k + m))) . da = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . da by A10, A14, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . da by A10, A109, FUNCT_1:49 ;

A111: now :: thesis:

per cases ) . da > 0 or (Comput (p1,s1,(k + m))) . da <= 0 ) ;

suppose A112: (Comput (p1,s1,(k + m))) . da > 0 ; :: thesis:

hence (Comput (p1,s1,(k + (m + 1)))) . (IC ) = lb by A20, A108, SCMFSA_2:71
.= (Comput (p2,s2,(k + (m + 1)))) . (IC ) by A19, A21, A108, A110, A112, SCMFSA_2:71 ;
:: thesis:

end;

suppose A113: (Comput (p1,s1,(k + m))) . da <= 0 ; :: thesis:

hence (Comput (p1,s1,(k + (m + 1)))) . (IC ) = (IC (Comput (p2,s2,(k + m)))) + 1 by A14, A20, A108, SCMFSA_2:71
.= (Comput (p2,s2,(k + (m + 1)))) . (IC ) by A19, A21, A108, A110, A113, SCMFSA_2:71 ;
:: thesis:

end;

now :: thesis:

let x be set ; :: thesis:
assume A114: x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) ; :: thesis:
then A115: (Comput (p1,s1,(k + m))) . x = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x by A14, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . x by A114, FUNCT_1:49 ;

per cases by A4, A114, Th12;

suppose A116: x is Int-Location ; :: thesis:

then (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p1,s1,(k + m))) . x by A20, A108, SCMFSA_2:71;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A19, A21, A108, A115, A116, SCMFSA_2:71; :: thesis:

end;

suppose A117: x is FinSeq-Location ; :: thesis:

end;

hence S₁[m + 1] by A22, A111, FUNCT_1:96; :: thesis:

end;

suppose InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 9 ; :: thesis:

then consider a, b being Int-Location, fa being FinSeq-Location such that
A118: CurInstr (p1,(Comput (p1,s1,(k + m)))) = b := (fa,a) by SCMFSA_2:38;
A119: (Comput (p1,s1,(k + (m + 1)))) . (IC ) = (IC (Comput (p2,s2,(k + m)))) + 1 by A14, A20, A118, SCMFSA_2:72
.= (Comput (p2,s2,(k + (m + 1)))) . (IC ) by A19, A21, A118, SCMFSA_2:72 ;

now :: thesis:

let x be set ; :: thesis:
assume A120: x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) ; :: thesis:

per cases by A4, A120, Th12;

suppose A121: x is Int-Location ; :: thesis:

per cases ;

suppose A122: x = b ; :: thesis:

A123: ex k1 being Nat st
( k1 = |.((Comput (p1,s1,(k + m))) . a).| & (Exec ((b := (fa,a)),(Comput (p1,s1,(k + m))))) . b = ((Comput (p1,s1,(k + m))) . fa) /. k1 ) by SCMFSA_2:72;
A124: ex k2 being Nat st
( k2 = |.((Comput (p2,s2,(k + m))) . a).| & (Exec ((b := (fa,a)),(Comput (p2,s2,(k + m))))) . b = ((Comput (p2,s2,(k + m))) . fa) /. k2 ) by SCMFSA_2:72;
A125: a in UsedILoc p by A18, A118, Th8;
then A126: (Comput (p1,s1,(k + m))) . a = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . a by A10, A14, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . a by A10, A125, FUNCT_1:49 ;
A127: fa in UsedI*Loc p by A18, A118, Th9;
then (Comput (p1,s1,(k + m))) . fa = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . fa by A11, A14, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . fa by A11, A127, FUNCT_1:49 ;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A19, A20, A21, A118, A122, A123, A124, A126; :: thesis:

end;

suppose A128: x <> b ; :: thesis:

then A129: (Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x by A19, A21, A118, A121, SCMFSA_2:72;
(Comput (p1,s1,(k + m))) . x = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x by A14, A120, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . x by A120, FUNCT_1:49 ;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A20, A118, A121, A128, A129, SCMFSA_2:72; :: thesis:

end;

suppose A130: x is FinSeq-Location ; :: thesis:

then A131: (Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x by A19, A21, A118, SCMFSA_2:72;
(Comput (p1,s1,(k + m))) . x = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x by A14, A120, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . x by A120, FUNCT_1:49 ;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A20, A118, A130, A131, SCMFSA_2:72; :: thesis:

end;

hence S₁[m + 1] by A22, A119, FUNCT_1:96; :: thesis:

end;

suppose InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 10 ; :: thesis:

then consider a, b being Int-Location, fa being FinSeq-Location such that
A132: CurInstr (p1,(Comput (p1,s1,(k + m)))) = (fa,a) := b by SCMFSA_2:39;
A133: (Comput (p1,s1,(k + (m + 1)))) . (IC ) = (IC (Comput (p2,s2,(k + m)))) + 1 by A14, A20, A132, SCMFSA_2:73
.= (Comput (p2,s2,(k + (m + 1)))) . (IC ) by A19, A21, A132, SCMFSA_2:73 ;

now :: thesis:

let x be set ; :: thesis:
assume A134: x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) ; :: thesis:

per cases by A4, A134, Th12;

suppose A135: x is FinSeq-Location ; :: thesis:

per cases ;

suppose A136: x = fa ; :: thesis:

A137: ex k1 being Nat st
( k1 = |.((Comput (p1,s1,(k + m))) . a).| & (Exec (((fa,a) := b),(Comput (p1,s1,(k + m))))) . fa = ((Comput (p1,s1,(k + m))) . fa) +* (k1,((Comput (p1,s1,(k + m))) . b)) ) by SCMFSA_2:73;
A138: ex k2 being Nat st
( k2 = |.((Comput (p2,s2,(k + m))) . a).| & (Exec (((fa,a) := b),(Comput (p2,s2,(k + m))))) . fa = ((Comput (p2,s2,(k + m))) . fa) +* (k2,((Comput (p2,s2,(k + m))) . b)) ) by SCMFSA_2:73;
A139: a in UsedILoc p by A18, A132, Th8;
then A140: (Comput (p1,s1,(k + m))) . a = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . a by A10, A14, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . a by A10, A139, FUNCT_1:49 ;
A141: b in UsedILoc p by A18, A132, Th8;
then A142: (Comput (p1,s1,(k + m))) . b = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . b by A10, A14, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . b by A10, A141, FUNCT_1:49 ;
A143: fa in UsedI*Loc p by A18, A132, Th9;
then (Comput (p1,s1,(k + m))) . fa = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . fa by A11, A14, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . fa by A11, A143, FUNCT_1:49 ;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A19, A20, A21, A132, A136, A137, A138, A140, A142; :: thesis:

end;

suppose A144: x <> fa ; :: thesis:

then A145: (Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x by A19, A21, A132, A135, SCMFSA_2:73;
(Comput (p1,s1,(k + m))) . x = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x by A14, A134, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . x by A134, FUNCT_1:49 ;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A20, A132, A135, A144, A145, SCMFSA_2:73; :: thesis:

end;

suppose A146: x is Int-Location ; :: thesis:

then A147: (Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x by A19, A21, A132, SCMFSA_2:73;
(Comput (p1,s1,(k + m))) . x = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x by A14, A134, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . x by A134, FUNCT_1:49 ;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A20, A132, A146, A147, SCMFSA_2:73; :: thesis:

end;

hence S₁[m + 1] by A22, A133, FUNCT_1:96; :: thesis:

end;

suppose InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 11 ; :: thesis:

then consider a being Int-Location, fa being FinSeq-Location such that
A148: CurInstr (p1,(Comput (p1,s1,(k + m)))) = a :=len fa by SCMFSA_2:40;
A149: (Comput (p1,s1,(k + (m + 1)))) . (IC ) = (IC (Comput (p2,s2,(k + m)))) + 1 by A14, A20, A148, SCMFSA_2:74
.= (Comput (p2,s2,(k + (m + 1)))) . (IC ) by A19, A21, A148, SCMFSA_2:74 ;

now :: thesis:

let x be set ; :: thesis:
assume A150: x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) ; :: thesis:

per cases by A4, A150, Th12;

suppose A151: x is Int-Location ; :: thesis:

per cases ;

suppose A152: x = a ; :: thesis:

then A153: (Comput (p2,s2,(k + (m + 1)))) . x = len ((Comput (p2,s2,(k + m))) . fa) by A19, A21, A148, SCMFSA_2:74;
A154: fa in UsedI*Loc p by A18, A148, Th11;
then (Comput (p1,s1,(k + m))) . fa = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . fa by A11, A14, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . fa by A11, A154, FUNCT_1:49 ;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A20, A148, A152, A153, SCMFSA_2:74; :: thesis:

end;

suppose A155: x <> a ; :: thesis:

then A156: (Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x by A19, A21, A148, A151, SCMFSA_2:74;
(Comput (p1,s1,(k + m))) . x = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x by A14, A150, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . x by A150, FUNCT_1:49 ;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A20, A148, A151, A155, A156, SCMFSA_2:74; :: thesis:

end;

suppose A157: x is FinSeq-Location ; :: thesis:

then A158: (Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x by A19, A21, A148, SCMFSA_2:74;
(Comput (p1,s1,(k + m))) . x = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x by A14, A150, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . x by A150, FUNCT_1:49 ;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A20, A148, A157, A158, SCMFSA_2:74; :: thesis:

end;

hence S₁[m + 1] by A22, A149, FUNCT_1:96; :: thesis:

end;

suppose InsCode (CurInstr (p1,(Comput (p1,s1,(k + m))))) = 12 ; :: thesis:

then consider a being Int-Location, fa being FinSeq-Location such that
A159: CurInstr (p1,(Comput (p1,s1,(k + m)))) = fa :=<0,...,0> a by SCMFSA_2:41;
A160: (Comput (p1,s1,(k + (m + 1)))) . (IC ) = (IC (Comput (p2,s2,(k + m)))) + 1 by A14, A20, A159, SCMFSA_2:75
.= (Comput (p2,s2,(k + (m + 1)))) . (IC ) by A19, A21, A159, SCMFSA_2:75 ;

now :: thesis:

let x be set ; :: thesis:
assume A161: x in ((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p) ; :: thesis:

per cases by A4, A161, Th12;

suppose A162: x is FinSeq-Location ; :: thesis:

per cases ;

suppose A163: x = fa ; :: thesis:

A164: ex k1 being Nat st
( k1 = |.((Comput (p1,s1,(k + m))) . a).| & (Exec ((fa :=<0,...,0> a),(Comput (p1,s1,(k + m))))) . fa = k1 |-> 0 ) by SCMFSA_2:75;
A165: ex k2 being Nat st
( k2 = |.((Comput (p2,s2,(k + m))) . a).| & (Exec ((fa :=<0,...,0> a),(Comput (p2,s2,(k + m))))) . fa = k2 |-> 0 ) by SCMFSA_2:75;
A166: a in UsedILoc p by A18, A159, Th10;
then (Comput (p1,s1,(k + m))) . a = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . a by A10, A14, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . a by A10, A166, FUNCT_1:49 ;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A19, A20, A21, A159, A163, A164, A165; :: thesis:

end;

suppose A167: x <> fa ; :: thesis:

then A168: (Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x by A19, A21, A159, A162, SCMFSA_2:75;
(Comput (p1,s1,(k + m))) . x = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x by A14, A161, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . x by A161, FUNCT_1:49 ;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A20, A159, A162, A167, A168, SCMFSA_2:75; :: thesis:

end;

suppose A169: x is Int-Location ; :: thesis:

then A170: (Comput (p2,s2,(k + (m + 1)))) . x = (Comput (p2,s2,(k + m))) . x by A19, A21, A159, SCMFSA_2:75;
(Comput (p1,s1,(k + m))) . x = ((Comput (p2,s2,(k + m))) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p))) . x by A14, A161, FUNCT_1:49
.= (Comput (p2,s2,(k + m))) . x by A161, FUNCT_1:49 ;
hence (Comput (p1,s1,(k + (m + 1)))) . x = (Comput (p2,s2,(k + (m + 1)))) . x by A20, A159, A169, A170, SCMFSA_2:75; :: thesis:

end;

hence S₁[m + 1] by A22, A160, FUNCT_1:96; :: thesis:

end;

for m being Nat holds S₁[m] from NAT_1:sch 2(A12, A13);
hence ( (Comput (p1,s1,i)) . (IC ) = (Comput (p2,s2,i)) . (IC ) & (Comput (p1,s1,i)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) = (Comput (p2,s2,i)) | (((dom t) \/ (UsedI*Loc p)) \/ (UsedILoc p)) ) by A9; :: thesis: