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

A13: now

let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[b₁ + 1] )
assume A14: S₁[m] ; :: thesis: S₁[b₁ + 1]
set sk1 = Comput (ProgramPart s1),s1,(k + m);
set sk11 = Comput (ProgramPart s1),s1,(k + (m + 1));
set i1 = CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m));
set sk2 = Comput (ProgramPart s2),s2,(k + m);
set sk12 = Comput (ProgramPart s2),s2,(k + (m + 1));
set i2 = CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(k + m))),(Comput (ProgramPart s2),s2,(k + m));
A15: IC (Comput (ProgramPart s1),s1,(k + m)) in dom p by A5;
Y: (ProgramPart (Comput (ProgramPart s2),s2,(k + m))) /. (IC (Comput (ProgramPart s2),s2,(k + m))) = (Comput (ProgramPart s2),s2,(k + m)) . (IC (Comput (ProgramPart s2),s2,(k + m))) by COMPOS_1:38;
Z: (ProgramPart (Comput (ProgramPart s1),s1,(k + m))) /. (IC (Comput (ProgramPart s1),s1,(k + m))) = (Comput (ProgramPart s1),s1,(k + m)) . (IC (Comput (ProgramPart s1),s1,(k + m))) by COMPOS_1:38;
B5: ( IC (Comput (ProgramPart s1),s1,(k + m)) in dom p & IC (Comput (ProgramPart s2),s2,(k + m)) in dom p ) by A5;
A16: CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m)) = ((Comput (ProgramPart s1),s1,(k + m)) | (dom p)) . (IC (Comput (ProgramPart s1),s1,(k + m))) by Z, B5, FUNCT_1:72;
CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m)) = s1 . (IC (Comput (ProgramPart s1),s1,(k + m))) by Z, AMI_1:54
.= p . (IC (Comput (ProgramPart s1),s1,(k + m))) by A2, A15, GRFUNC_1:8 ;
then A17: CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m)) in rng p by A15, FUNCT_1:def 5;
A18: CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(k + m))),(Comput (ProgramPart s2),s2,(k + m)) = ((Comput (ProgramPart s2),s2,(k + m)) | (dom p)) . (IC (Comput (ProgramPart s2),s2,(k + m))) by Y, B5, FUNCT_1:72
.= CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m)) by A2, A3, A14, A16, AMI_1:124 ;
T: ProgramPart s1 = ProgramPart (Comput (ProgramPart s1),s1,(k + m)) by AMI_1:123;
A19: Comput (ProgramPart s1),s1,(k + (m + 1)) = Comput (ProgramPart s1),s1,((k + m) + 1)
.= Following (ProgramPart s1),(Comput (ProgramPart s1),s1,(k + m)) by AMI_1:14
.= Exec (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m)) by T ;
S: ProgramPart s2 = ProgramPart (Comput (ProgramPart s2),s2,(k + m)) by AMI_1:123;
A20: Comput (ProgramPart s2),s2,(k + (m + 1)) = Comput (ProgramPart s2),s2,((k + m) + 1)
.= Following (ProgramPart s2),(Comput (ProgramPart s2),s2,(k + m)) by AMI_1:14
.= Exec (CurInstr (ProgramPart (Comput (ProgramPart s2),s2,(k + m))),(Comput (ProgramPart s2),s2,(k + m))),(Comput (ProgramPart s2),s2,(k + m)) by S ;
A21: dom (Comput (ProgramPart s1),s1,(k + (m + 1))) = the carrier of SCM+FSA by PARTFUN1:def 4
.= dom (Comput (ProgramPart s2),s2,(k + (m + 1))) by PARTFUN1:def 4 ;

per cases ( InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m))) = 0 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m))) = 1 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m))) = 2 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m))) = 3 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m))) = 4 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m))) = 5 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m))) = 6 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m))) = 7 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m))) = 8 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m))) = 9 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m))) = 10 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m))) = 11 or InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m))) = 12 ) by NAT_1:37, SCMFSA_2:35;

suppose InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m))) = 0 ; :: thesis: S₁[b₁ + 1]

then A22: CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m)) = halt SCM+FSA by SCMFSA_2:122;
then Comput (ProgramPart s1),s1,(k + (m + 1)) = Comput (ProgramPart s1),s1,(k + m) by A19, AMI_1:def 8;
hence S₁[m + 1] by A14, A18, A20, A22, AMI_1:def 8; :: thesis: verum

end;

suppose InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m))) = 1 ; :: thesis: S₁[b₁ + 1]

then consider da, db being Int-Location such that
A23: CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m)) = da := db by SCMFSA_2:54;
A24: (Comput (ProgramPart s1),s1,(k + (m + 1))) . (IC SCM+FSA ) = succ (IC (Comput (ProgramPart s1),s1,(k + m))) by A19, A23, SCMFSA_2:89
.= (Comput (ProgramPart s2),s2,(k + (m + 1))) . (IC SCM+FSA ) by A14, A18, A20, A23, SCMFSA_2:89 ;

now

let x be set ; :: thesis: ( x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) implies (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁ )
assume A25: x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

per cases ( x is Int-Location or x is FinSeq-Location ) by A4, A25, Th23;

suppose A26: x is Int-Location ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

now

per cases ( x = da or x <> da ) ;

case A27: x = da ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x

then A28: (Comput (ProgramPart s2),s2,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + m)) . db by A18, A20, A23, SCMFSA_2:89;
A29: db in UsedIntLoc p by A17, A23, Th16;
then (Comput (ProgramPart s1),s1,(k + m)) . db = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . db by A10, A14, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . db by A10, A29, FUNCT_1:72 ;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A19, A23, A27, A28, SCMFSA_2:89; :: thesis: verum

end;

case A30: x <> da ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x

then A31: (Comput (ProgramPart s2),s2,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + m)) . x by A18, A20, A23, A26, SCMFSA_2:89;
(Comput (ProgramPart s1),s1,(k + m)) . x = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A14, A25, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . x by A25, FUNCT_1:72 ;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A19, A23, A26, A30, A31, SCMFSA_2:89; :: thesis: verum

end;

end;

end;

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

end;

suppose A32: x is FinSeq-Location ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

then A33: (Comput (ProgramPart s2),s2,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + m)) . x by A18, A20, A23, SCMFSA_2:89;
(Comput (ProgramPart s1),s1,(k + m)) . x = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A14, A25, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . x by A25, FUNCT_1:72 ;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A19, A23, A32, A33, SCMFSA_2:89; :: thesis: verum

end;

end;

end;

hence S₁[m + 1] by A21, A24, FUNCT_1:166; :: thesis: verum

end;

suppose InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m))) = 2 ; :: thesis: S₁[b₁ + 1]

then consider da, db being Int-Location such that
A34: CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m)) = AddTo da,db by SCMFSA_2:55;
A35: (Comput (ProgramPart s1),s1,(k + (m + 1))) . (IC SCM+FSA ) = succ (IC (Comput (ProgramPart s1),s1,(k + m))) by A19, A34, SCMFSA_2:90
.= (Comput (ProgramPart s2),s2,(k + (m + 1))) . (IC SCM+FSA ) by A14, A18, A20, A34, SCMFSA_2:90 ;

now

let x be set ; :: thesis: ( x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) implies (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁ )
assume A36: x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

per cases ( x is Int-Location or x is FinSeq-Location ) by A4, A36, Th23;

suppose A37: x is Int-Location ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

now

per cases ( x = da or x <> da ) ;

case A38: x = da ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x

then A39: (Comput (ProgramPart s2),s2,(k + (m + 1))) . x = ((Comput (ProgramPart s2),s2,(k + m)) . da) + ((Comput (ProgramPart s2),s2,(k + m)) . db) by A18, A20, A34, SCMFSA_2:90;
A40: da in UsedIntLoc p by A17, A34, Th16;
then A41: (Comput (ProgramPart s1),s1,(k + m)) . da = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . da by A10, A14, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . da by A10, A40, FUNCT_1:72 ;
A42: db in UsedIntLoc p by A17, A34, Th16;
then (Comput (ProgramPart s1),s1,(k + m)) . db = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . db by A10, A14, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . db by A10, A42, FUNCT_1:72 ;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A19, A34, A38, A39, A41, SCMFSA_2:90; :: thesis: verum

end;

case A43: x <> da ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x

then A44: (Comput (ProgramPart s2),s2,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + m)) . x by A18, A20, A34, A37, SCMFSA_2:90;
(Comput (ProgramPart s1),s1,(k + m)) . x = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A14, A36, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . x by A36, FUNCT_1:72 ;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A19, A34, A37, A43, A44, SCMFSA_2:90; :: thesis: verum

end;

end;

end;

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

end;

suppose A45: x is FinSeq-Location ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

then A46: (Comput (ProgramPart s2),s2,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + m)) . x by A18, A20, A34, SCMFSA_2:90;
(Comput (ProgramPart s1),s1,(k + m)) . x = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A14, A36, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . x by A36, FUNCT_1:72 ;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A19, A34, A45, A46, SCMFSA_2:90; :: thesis: verum

end;

end;

end;

hence S₁[m + 1] by A21, A35, FUNCT_1:166; :: thesis: verum

end;

suppose InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m))) = 3 ; :: thesis: S₁[b₁ + 1]

then consider da, db being Int-Location such that
A47: CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m)) = SubFrom da,db by SCMFSA_2:56;
A48: (Comput (ProgramPart s1),s1,(k + (m + 1))) . (IC SCM+FSA ) = succ (IC (Comput (ProgramPart s1),s1,(k + m))) by A19, A47, SCMFSA_2:91
.= (Comput (ProgramPart s2),s2,(k + (m + 1))) . (IC SCM+FSA ) by A14, A18, A20, A47, SCMFSA_2:91 ;

now

let x be set ; :: thesis: ( x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) implies (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁ )
assume A49: x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

per cases ( x is Int-Location or x is FinSeq-Location ) by A4, A49, Th23;

suppose A50: x is Int-Location ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

now

per cases ( x = da or x <> da ) ;

case A51: x = da ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x

then A52: (Comput (ProgramPart s2),s2,(k + (m + 1))) . x = ((Comput (ProgramPart s2),s2,(k + m)) . da) - ((Comput (ProgramPart s2),s2,(k + m)) . db) by A18, A20, A47, SCMFSA_2:91;
A53: da in UsedIntLoc p by A17, A47, Th16;
then A54: (Comput (ProgramPart s1),s1,(k + m)) . da = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . da by A10, A14, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . da by A10, A53, FUNCT_1:72 ;
A55: db in UsedIntLoc p by A17, A47, Th16;
then (Comput (ProgramPart s1),s1,(k + m)) . db = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . db by A10, A14, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . db by A10, A55, FUNCT_1:72 ;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A19, A47, A51, A52, A54, SCMFSA_2:91; :: thesis: verum

end;

case A56: x <> da ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x

then A57: (Comput (ProgramPart s2),s2,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + m)) . x by A18, A20, A47, A50, SCMFSA_2:91;
(Comput (ProgramPart s1),s1,(k + m)) . x = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A14, A49, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . x by A49, FUNCT_1:72 ;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A19, A47, A50, A56, A57, SCMFSA_2:91; :: thesis: verum

end;

end;

end;

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

end;

suppose A58: x is FinSeq-Location ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

then A59: (Comput (ProgramPart s2),s2,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + m)) . x by A18, A20, A47, SCMFSA_2:91;
(Comput (ProgramPart s1),s1,(k + m)) . x = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A14, A49, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . x by A49, FUNCT_1:72 ;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A19, A47, A58, A59, SCMFSA_2:91; :: thesis: verum

end;

end;

end;

hence S₁[m + 1] by A21, A48, FUNCT_1:166; :: thesis: verum

end;

suppose InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m))) = 4 ; :: thesis: S₁[b₁ + 1]

then consider da, db being Int-Location such that
A60: CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m)) = MultBy da,db by SCMFSA_2:57;
A61: (Comput (ProgramPart s1),s1,(k + (m + 1))) . (IC SCM+FSA ) = succ (IC (Comput (ProgramPart s1),s1,(k + m))) by A19, A60, SCMFSA_2:92
.= (Comput (ProgramPart s2),s2,(k + (m + 1))) . (IC SCM+FSA ) by A14, A18, A20, A60, SCMFSA_2:92 ;

now

let x be set ; :: thesis: ( x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) implies (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁ )
assume A62: x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

per cases ( x is Int-Location or x is FinSeq-Location ) by A4, A62, Th23;

suppose A63: x is Int-Location ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

now

per cases ( x = da or x <> da ) ;

case A64: x = da ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x

then A65: (Comput (ProgramPart s2),s2,(k + (m + 1))) . x = ((Comput (ProgramPart s2),s2,(k + m)) . da) * ((Comput (ProgramPart s2),s2,(k + m)) . db) by A18, A20, A60, SCMFSA_2:92;
A66: da in UsedIntLoc p by A17, A60, Th16;
then A67: (Comput (ProgramPart s1),s1,(k + m)) . da = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . da by A10, A14, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . da by A10, A66, FUNCT_1:72 ;
A68: db in UsedIntLoc p by A17, A60, Th16;
then (Comput (ProgramPart s1),s1,(k + m)) . db = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . db by A10, A14, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . db by A10, A68, FUNCT_1:72 ;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A19, A60, A64, A65, A67, SCMFSA_2:92; :: thesis: verum

end;

case A69: x <> da ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x

then A70: (Comput (ProgramPart s2),s2,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + m)) . x by A18, A20, A60, A63, SCMFSA_2:92;
(Comput (ProgramPart s1),s1,(k + m)) . x = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A14, A62, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . x by A62, FUNCT_1:72 ;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A19, A60, A63, A69, A70, SCMFSA_2:92; :: thesis: verum

end;

end;

end;

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

end;

suppose A71: x is FinSeq-Location ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

then A72: (Comput (ProgramPart s2),s2,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + m)) . x by A18, A20, A60, SCMFSA_2:92;
(Comput (ProgramPart s1),s1,(k + m)) . x = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A14, A62, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . x by A62, FUNCT_1:72 ;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A19, A60, A71, A72, SCMFSA_2:92; :: thesis: verum

end;

end;

end;

hence S₁[m + 1] by A21, A61, FUNCT_1:166; :: thesis: verum

end;

suppose InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m))) = 5 ; :: thesis: S₁[b₁ + 1]

then consider da, db being Int-Location such that
A73: CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m)) = Divide da,db by SCMFSA_2:58;
A74: (Comput (ProgramPart s1),s1,(k + (m + 1))) . (IC SCM+FSA ) = succ (IC (Comput (ProgramPart s1),s1,(k + m))) by A19, A73, SCMFSA_2:93
.= (Comput (ProgramPart s2),s2,(k + (m + 1))) . (IC SCM+FSA ) by A14, A18, A20, A73, SCMFSA_2:93 ;

now

let x be set ; :: thesis: ( x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) implies (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁ )
assume A75: x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

per cases ( x is Int-Location or x is FinSeq-Location ) by A4, A75, Th23;

suppose A76: x is Int-Location ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

A77: da in UsedIntLoc p by A17, A73, Th16;
then A78: (Comput (ProgramPart s1),s1,(k + m)) . da = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . da by A10, A14, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . da by A10, A77, FUNCT_1:72 ;
A79: db in UsedIntLoc p by A17, A73, Th16;
then A80: (Comput (ProgramPart s1),s1,(k + m)) . db = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . db by A10, A14, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . db by A10, A79, FUNCT_1:72 ;
A81: (Comput (ProgramPart s1),s1,(k + m)) . x = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A14, A75, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . x by A75, FUNCT_1:72 ;

now

per cases ( da <> db or da = db ) ;

suppose A82: da <> db ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x

now

per cases ( x = da or x = db or ( x <> da & x <> db ) ) ;

suppose A83: x = da ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x

then (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = ((Comput (ProgramPart s1),s1,(k + m)) . da) div ((Comput (ProgramPart s1),s1,(k + m)) . db) by A19, A73, A82, SCMFSA_2:93;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A18, A20, A73, A78, A80, A82, A83, SCMFSA_2:93; :: thesis: verum

end;

suppose A84: x = db ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x

then (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = ((Comput (ProgramPart s1),s1,(k + m)) . da) mod ((Comput (ProgramPart s1),s1,(k + m)) . db) by A19, A73, SCMFSA_2:93;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A18, A20, A73, A78, A80, A84, SCMFSA_2:93; :: thesis: verum

end;

suppose A85: ( x <> da & x <> db ) ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x

then (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s1),s1,(k + m)) . x by A19, A73, A76, SCMFSA_2:93;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A18, A20, A73, A76, A81, A85, SCMFSA_2:93; :: thesis: verum

end;

end;

end;

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

end;

suppose A86: da = db ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x

now

per cases ( x = da or x <> da ) ;

case A87: x = da ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x

then (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = ((Comput (ProgramPart s1),s1,(k + m)) . da) mod ((Comput (ProgramPart s1),s1,(k + m)) . da) by A19, A73, A86, SCMFSA_2:94;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A18, A20, A73, A78, A86, A87, SCMFSA_2:94; :: thesis: verum

end;

case A88: x <> da ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x

then (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s1),s1,(k + m)) . x by A19, A73, A76, A86, SCMFSA_2:94;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A18, A20, A73, A76, A81, A86, A88, SCMFSA_2:94; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

suppose A89: x is FinSeq-Location ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

then A90: (Comput (ProgramPart s2),s2,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + m)) . x by A18, A20, A73, SCMFSA_2:93;
(Comput (ProgramPart s1),s1,(k + m)) . x = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A14, A75, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . x by A75, FUNCT_1:72 ;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A19, A73, A89, A90, SCMFSA_2:93; :: thesis: verum

end;

end;

end;

hence S₁[m + 1] by A21, A74, FUNCT_1:166; :: thesis: verum

end;

suppose InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m))) = 6 ; :: thesis: S₁[b₁ + 1]

then consider lb being Element of NAT such that
A91: CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m)) = goto lb by SCMFSA_2:59;
A92: (Comput (ProgramPart s1),s1,(k + (m + 1))) . (IC SCM+FSA ) = lb by A19, A91, SCMFSA_2:95
.= (Comput (ProgramPart s2),s2,(k + (m + 1))) . (IC SCM+FSA ) by A18, A20, A91, SCMFSA_2:95 ;

now

let x be set ; :: thesis: ( x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) implies (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁ )
assume A93: x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁
then A94: (Comput (ProgramPart s1),s1,(k + m)) . x = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A14, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . x by A93, FUNCT_1:72 ;

per cases ( x is Int-Location or x is FinSeq-Location ) by A4, A93, Th23;

suppose A95: x is Int-Location ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

then (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s1),s1,(k + m)) . x by A19, A91, SCMFSA_2:95;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A18, A20, A91, A94, A95, SCMFSA_2:95; :: thesis: verum

end;

suppose A96: x is FinSeq-Location ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

then (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s1),s1,(k + m)) . x by A19, A91, SCMFSA_2:95;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A18, A20, A91, A94, A96, SCMFSA_2:95; :: thesis: verum

end;

end;

end;

hence S₁[m + 1] by A21, A92, FUNCT_1:166; :: thesis: verum

end;

suppose InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m))) = 7 ; :: thesis: S₁[b₁ + 1]

then consider lb being Element of NAT , da being Int-Location such that
A97: CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m)) = da =0_goto lb by SCMFSA_2:60;
A98: da in UsedIntLoc p by A17, A97, Th17;
then A99: (Comput (ProgramPart s1),s1,(k + m)) . da = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . da by A10, A14, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . da by A10, A98, FUNCT_1:72 ;

A100: now

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

suppose A101: (Comput (ProgramPart s1),s1,(k + m)) . da = 0 ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . (IC SCM+FSA ) = (Comput (ProgramPart s2),s2,(k + (m + 1))) . (IC SCM+FSA )

hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . (IC SCM+FSA ) = lb by A19, A97, SCMFSA_2:96
.= (Comput (ProgramPart s2),s2,(k + (m + 1))) . (IC SCM+FSA ) by A18, A20, A97, A99, A101, SCMFSA_2:96 ;
:: thesis: verum

end;

suppose A102: (Comput (ProgramPart s1),s1,(k + m)) . da <> 0 ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . (IC SCM+FSA ) = (Comput (ProgramPart s2),s2,(k + (m + 1))) . (IC SCM+FSA )

hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . (IC SCM+FSA ) = succ (IC (Comput (ProgramPart s2),s2,(k + m))) by A14, A19, A97, SCMFSA_2:96
.= (Comput (ProgramPart s2),s2,(k + (m + 1))) . (IC SCM+FSA ) by A18, A20, A97, A99, A102, SCMFSA_2:96 ;
:: thesis: verum

end;

end;

end;

now

let x be set ; :: thesis: ( x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) implies (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁ )
assume A103: x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁
then A104: (Comput (ProgramPart s1),s1,(k + m)) . x = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A14, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . x by A103, FUNCT_1:72 ;

per cases ( x is Int-Location or x is FinSeq-Location ) by A4, A103, Th23;

suppose A105: x is Int-Location ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

then (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s1),s1,(k + m)) . x by A19, A97, SCMFSA_2:96;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A18, A20, A97, A104, A105, SCMFSA_2:96; :: thesis: verum

end;

suppose A106: x is FinSeq-Location ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

then (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s1),s1,(k + m)) . x by A19, A97, SCMFSA_2:96;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A18, A20, A97, A104, A106, SCMFSA_2:96; :: thesis: verum

end;

end;

end;

hence S₁[m + 1] by A21, A100, FUNCT_1:166; :: thesis: verum

end;

suppose InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m))) = 8 ; :: thesis: S₁[b₁ + 1]

then consider lb being Element of NAT , da being Int-Location such that
A107: CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m)) = da >0_goto lb by SCMFSA_2:61;
A108: da in UsedIntLoc p by A17, A107, Th17;
then A109: (Comput (ProgramPart s1),s1,(k + m)) . da = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . da by A10, A14, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . da by A10, A108, FUNCT_1:72 ;

A110: now

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

suppose A111: (Comput (ProgramPart s1),s1,(k + m)) . da > 0 ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . (IC SCM+FSA ) = (Comput (ProgramPart s2),s2,(k + (m + 1))) . (IC SCM+FSA )

hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . (IC SCM+FSA ) = lb by A19, A107, SCMFSA_2:97
.= (Comput (ProgramPart s2),s2,(k + (m + 1))) . (IC SCM+FSA ) by A18, A20, A107, A109, A111, SCMFSA_2:97 ;
:: thesis: verum

end;

suppose A112: (Comput (ProgramPart s1),s1,(k + m)) . da <= 0 ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . (IC SCM+FSA ) = (Comput (ProgramPart s2),s2,(k + (m + 1))) . (IC SCM+FSA )

hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . (IC SCM+FSA ) = succ (IC (Comput (ProgramPart s2),s2,(k + m))) by A14, A19, A107, SCMFSA_2:97
.= (Comput (ProgramPart s2),s2,(k + (m + 1))) . (IC SCM+FSA ) by A18, A20, A107, A109, A112, SCMFSA_2:97 ;
:: thesis: verum

end;

end;

end;

now

let x be set ; :: thesis: ( x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) implies (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁ )
assume A113: x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁
then A114: (Comput (ProgramPart s1),s1,(k + m)) . x = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A14, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . x by A113, FUNCT_1:72 ;

per cases ( x is Int-Location or x is FinSeq-Location ) by A4, A113, Th23;

suppose A115: x is Int-Location ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

then (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s1),s1,(k + m)) . x by A19, A107, SCMFSA_2:97;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A18, A20, A107, A114, A115, SCMFSA_2:97; :: thesis: verum

end;

suppose A116: x is FinSeq-Location ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

then (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s1),s1,(k + m)) . x by A19, A107, SCMFSA_2:97;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A18, A20, A107, A114, A116, SCMFSA_2:97; :: thesis: verum

end;

end;

end;

hence S₁[m + 1] by A21, A110, FUNCT_1:166; :: thesis: verum

end;

suppose InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m))) = 9 ; :: thesis: S₁[b₁ + 1]

then consider a, b being Int-Location , fa being FinSeq-Location such that
A117: CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m)) = b := fa,a by SCMFSA_2:62;
A118: (Comput (ProgramPart s1),s1,(k + (m + 1))) . (IC SCM+FSA ) = succ (IC (Comput (ProgramPart s2),s2,(k + m))) by A14, A19, A117, SCMFSA_2:98
.= (Comput (ProgramPart s2),s2,(k + (m + 1))) . (IC SCM+FSA ) by A18, A20, A117, SCMFSA_2:98 ;

now

let x be set ; :: thesis: ( x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) implies (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁ )
assume A119: x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

per cases ( x is Int-Location or x is FinSeq-Location ) by A4, A119, Th23;

suppose A120: x is Int-Location ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

now

per cases ( x = b or x <> b ) ;

case A121: x = b ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x

A122: ex k1 being Element of NAT st
( k1 = abs ((Comput (ProgramPart s1),s1,(k + m)) . a) & (Exec (b := fa,a),(Comput (ProgramPart s1),s1,(k + m))) . b = ((Comput (ProgramPart s1),s1,(k + m)) . fa) /. k1 ) by SCMFSA_2:98;
A123: ex k2 being Element of NAT st
( k2 = abs ((Comput (ProgramPart s2),s2,(k + m)) . a) & (Exec (b := fa,a),(Comput (ProgramPart s2),s2,(k + m))) . b = ((Comput (ProgramPart s2),s2,(k + m)) . fa) /. k2 ) by SCMFSA_2:98;
A124: a in UsedIntLoc p by A17, A117, Th18;
then A125: (Comput (ProgramPart s1),s1,(k + m)) . a = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . a by A10, A14, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . a by A10, A124, FUNCT_1:72 ;
A126: fa in UsedInt*Loc p by A17, A117, Th19;
then (Comput (ProgramPart s1),s1,(k + m)) . fa = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . fa by A11, A14, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . fa by A11, A126, FUNCT_1:72 ;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A18, A19, A20, A117, A121, A122, A123, A125; :: thesis: verum

end;

case A127: x <> b ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x

then A128: (Comput (ProgramPart s2),s2,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + m)) . x by A18, A20, A117, A120, SCMFSA_2:98;
(Comput (ProgramPart s1),s1,(k + m)) . x = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A14, A119, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . x by A119, FUNCT_1:72 ;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A19, A117, A120, A127, A128, SCMFSA_2:98; :: thesis: verum

end;

end;

end;

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

end;

suppose A129: x is FinSeq-Location ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

then A130: (Comput (ProgramPart s2),s2,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + m)) . x by A18, A20, A117, SCMFSA_2:98;
(Comput (ProgramPart s1),s1,(k + m)) . x = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A14, A119, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . x by A119, FUNCT_1:72 ;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A19, A117, A129, A130, SCMFSA_2:98; :: thesis: verum

end;

end;

end;

hence S₁[m + 1] by A21, A118, FUNCT_1:166; :: thesis: verum

end;

suppose InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m))) = 10 ; :: thesis: S₁[b₁ + 1]

then consider a, b being Int-Location , fa being FinSeq-Location such that
A131: CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m)) = fa,a := b by SCMFSA_2:63;
A132: (Comput (ProgramPart s1),s1,(k + (m + 1))) . (IC SCM+FSA ) = succ (IC (Comput (ProgramPart s2),s2,(k + m))) by A14, A19, A131, SCMFSA_2:99
.= (Comput (ProgramPart s2),s2,(k + (m + 1))) . (IC SCM+FSA ) by A18, A20, A131, SCMFSA_2:99 ;

now

let x be set ; :: thesis: ( x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) implies (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁ )
assume A133: x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

per cases ( x is FinSeq-Location or x is Int-Location ) by A4, A133, Th23;

suppose A134: x is FinSeq-Location ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

now

per cases ( x = fa or x <> fa ) ;

case A135: x = fa ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x

A136: ex k1 being Element of NAT st
( k1 = abs ((Comput (ProgramPart s1),s1,(k + m)) . a) & (Exec (fa,a := b),(Comput (ProgramPart s1),s1,(k + m))) . fa = ((Comput (ProgramPart s1),s1,(k + m)) . fa) +* k1,((Comput (ProgramPart s1),s1,(k + m)) . b) ) by SCMFSA_2:99;
A137: ex k2 being Element of NAT st
( k2 = abs ((Comput (ProgramPart s2),s2,(k + m)) . a) & (Exec (fa,a := b),(Comput (ProgramPart s2),s2,(k + m))) . fa = ((Comput (ProgramPart s2),s2,(k + m)) . fa) +* k2,((Comput (ProgramPart s2),s2,(k + m)) . b) ) by SCMFSA_2:99;
A138: a in UsedIntLoc p by A17, A131, Th18;
then A139: (Comput (ProgramPart s1),s1,(k + m)) . a = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . a by A10, A14, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . a by A10, A138, FUNCT_1:72 ;
A140: b in UsedIntLoc p by A17, A131, Th18;
then A141: (Comput (ProgramPart s1),s1,(k + m)) . b = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . b by A10, A14, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . b by A10, A140, FUNCT_1:72 ;
A142: fa in UsedInt*Loc p by A17, A131, Th19;
then (Comput (ProgramPart s1),s1,(k + m)) . fa = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . fa by A11, A14, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . fa by A11, A142, FUNCT_1:72 ;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A18, A19, A20, A131, A135, A136, A137, A139, A141; :: thesis: verum

end;

case A143: x <> fa ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x

then A144: (Comput (ProgramPart s2),s2,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + m)) . x by A18, A20, A131, A134, SCMFSA_2:99;
(Comput (ProgramPart s1),s1,(k + m)) . x = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A14, A133, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . x by A133, FUNCT_1:72 ;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A19, A131, A134, A143, A144, SCMFSA_2:99; :: thesis: verum

end;

end;

end;

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

end;

suppose A145: x is Int-Location ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

then A146: (Comput (ProgramPart s2),s2,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + m)) . x by A18, A20, A131, SCMFSA_2:99;
(Comput (ProgramPart s1),s1,(k + m)) . x = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A14, A133, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . x by A133, FUNCT_1:72 ;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A19, A131, A145, A146, SCMFSA_2:99; :: thesis: verum

end;

end;

end;

hence S₁[m + 1] by A21, A132, FUNCT_1:166; :: thesis: verum

end;

suppose InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m))) = 11 ; :: thesis: S₁[b₁ + 1]

then consider a being Int-Location , fa being FinSeq-Location such that
A147: CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m)) = a :=len fa by SCMFSA_2:64;
A148: (Comput (ProgramPart s1),s1,(k + (m + 1))) . (IC SCM+FSA ) = succ (IC (Comput (ProgramPart s2),s2,(k + m))) by A14, A19, A147, SCMFSA_2:100
.= (Comput (ProgramPart s2),s2,(k + (m + 1))) . (IC SCM+FSA ) by A18, A20, A147, SCMFSA_2:100 ;

now

let x be set ; :: thesis: ( x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) implies (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁ )
assume A149: x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

per cases ( x is Int-Location or x is FinSeq-Location ) by A4, A149, Th23;

suppose A150: x is Int-Location ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

now

per cases ( x = a or x <> a ) ;

case A151: x = a ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x

then A152: (Comput (ProgramPart s2),s2,(k + (m + 1))) . x = len ((Comput (ProgramPart s2),s2,(k + m)) . fa) by A18, A20, A147, SCMFSA_2:100;
A153: fa in UsedInt*Loc p by A17, A147, Th21;
then (Comput (ProgramPart s1),s1,(k + m)) . fa = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . fa by A11, A14, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . fa by A11, A153, FUNCT_1:72 ;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A19, A147, A151, A152, SCMFSA_2:100; :: thesis: verum

end;

case A154: x <> a ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x

then A155: (Comput (ProgramPart s2),s2,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + m)) . x by A18, A20, A147, A150, SCMFSA_2:100;
(Comput (ProgramPart s1),s1,(k + m)) . x = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A14, A149, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . x by A149, FUNCT_1:72 ;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A19, A147, A150, A154, A155, SCMFSA_2:100; :: thesis: verum

end;

end;

end;

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

end;

suppose A156: x is FinSeq-Location ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

then A157: (Comput (ProgramPart s2),s2,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + m)) . x by A18, A20, A147, SCMFSA_2:100;
(Comput (ProgramPart s1),s1,(k + m)) . x = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A14, A149, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . x by A149, FUNCT_1:72 ;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A19, A147, A156, A157, SCMFSA_2:100; :: thesis: verum

end;

end;

end;

hence S₁[m + 1] by A21, A148, FUNCT_1:166; :: thesis: verum

end;

suppose InsCode (CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m))) = 12 ; :: thesis: S₁[b₁ + 1]

then consider a being Int-Location , fa being FinSeq-Location such that
A158: CurInstr (ProgramPart (Comput (ProgramPart s1),s1,(k + m))),(Comput (ProgramPart s1),s1,(k + m)) = fa :=<0,...,0> a by SCMFSA_2:65;
A159: (Comput (ProgramPart s1),s1,(k + (m + 1))) . (IC SCM+FSA ) = succ (IC (Comput (ProgramPart s2),s2,(k + m))) by A14, A19, A158, SCMFSA_2:101
.= (Comput (ProgramPart s2),s2,(k + (m + 1))) . (IC SCM+FSA ) by A18, A20, A158, SCMFSA_2:101 ;

now

let x be set ; :: thesis: ( x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) implies (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁ )
assume A160: x in ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

per cases ( x is FinSeq-Location or x is Int-Location ) by A4, A160, Th23;

suppose A161: x is FinSeq-Location ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

now

per cases ( x = fa or x <> fa ) ;

case A162: x = fa ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x

A163: ex k1 being Element of NAT st
( k1 = abs ((Comput (ProgramPart s1),s1,(k + m)) . a) & (Exec (fa :=<0,...,0> a),(Comput (ProgramPart s1),s1,(k + m))) . fa = k1 |-> 0 ) by SCMFSA_2:101;
A164: ex k2 being Element of NAT st
( k2 = abs ((Comput (ProgramPart s2),s2,(k + m)) . a) & (Exec (fa :=<0,...,0> a),(Comput (ProgramPart s2),s2,(k + m))) . fa = k2 |-> 0 ) by SCMFSA_2:101;
A165: a in UsedIntLoc p by A17, A158, Th20;
then (Comput (ProgramPart s1),s1,(k + m)) . a = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . a by A10, A14, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . a by A10, A165, FUNCT_1:72 ;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A18, A19, A20, A158, A162, A163, A164; :: thesis: verum

end;

case A166: x <> fa ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x

then A167: (Comput (ProgramPart s2),s2,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + m)) . x by A18, A20, A158, A161, SCMFSA_2:101;
(Comput (ProgramPart s1),s1,(k + m)) . x = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A14, A160, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . x by A160, FUNCT_1:72 ;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A19, A158, A161, A166, A167, SCMFSA_2:101; :: thesis: verum

end;

end;

end;

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

end;

suppose A168: x is Int-Location ; :: thesis: (Comput (ProgramPart s1),s1,(k + (m + 1))) . b₁ = (Comput (ProgramPart s2),s2,(k + (m + 1))) . b₁

then A169: (Comput (ProgramPart s2),s2,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + m)) . x by A18, A20, A158, SCMFSA_2:101;
(Comput (ProgramPart s1),s1,(k + m)) . x = ((Comput (ProgramPart s2),s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A14, A160, FUNCT_1:72
.= (Comput (ProgramPart s2),s2,(k + m)) . x by A160, FUNCT_1:72 ;
hence (Comput (ProgramPart s1),s1,(k + (m + 1))) . x = (Comput (ProgramPart s2),s2,(k + (m + 1))) . x by A19, A158, A168, A169, SCMFSA_2:101; :: thesis: verum

end;

end;

end;

hence S₁[m + 1] by A21, A159, FUNCT_1:166; :: thesis: verum

end;

end;

end;

for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A12, A13);
hence ( (Comput (ProgramPart s1),s1,i) . (IC SCM+FSA ) = (Comput (ProgramPart s2),s2,i) . (IC SCM+FSA ) & (Comput (ProgramPart s1),s1,i) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) = (Comput (ProgramPart s2),s2,i) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) ) by A9; :: thesis: verum