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 (Computation s1,j) in dom p & IC (Computation s2,j) in dom p ) ) & (Computation s1,k) . (IC SCM+FSA ) = (Computation s2,k) . (IC SCM+FSA ) & (Computation s1,k) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) = (Computation s2,k) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) holds
( (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) & (Computation s1,i) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) = (Computation 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 (Computation s1,j) in dom p & IC (Computation s2,j) in dom p ) ) & (Computation s1,k) . (IC SCM+FSA ) = (Computation s2,k) . (IC SCM+FSA ) & (Computation s1,k) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) = (Computation s2,k) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) holds
( (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) & (Computation s1,i) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) = (Computation 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 (Computation s1,j) in dom p & IC (Computation s2,j) in dom p ) ) & (Computation s1,k) . (IC SCM+FSA ) = (Computation s2,k) . (IC SCM+FSA ) & (Computation s1,k) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) = (Computation s2,k) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) holds
( (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) & (Computation s1,i) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) = (Computation 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 (Computation s1,j) in dom p & IC (Computation s2,j) in dom p ) ) & (Computation s1,k) . (IC SCM+FSA ) = (Computation s2,k) . (IC SCM+FSA ) & (Computation s1,k) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) = (Computation s2,k) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) implies ( (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) & (Computation s1,i) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) = (Computation s2,i) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) ) )
set Dloc = ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p);
assume A1: ( k <= i & p c= s1 & p c= s2 & dom t c= Int-Locations \/ FinSeq-Locations & ( for j being Element of NAT holds
( IC (Computation s1,j) in dom p & IC (Computation s2,j) in dom p ) ) & (Computation s1,k) . (IC SCM+FSA ) = (Computation s2,k) . (IC SCM+FSA ) & (Computation s1,k) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) = (Computation s2,k) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) ) ; :: thesis: ( (Computation s1,i) . (IC SCM+FSA ) = (Computation s2,i) . (IC SCM+FSA ) & (Computation s1,i) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) = (Computation s2,i) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) )
then consider m being Nat such that
A2: i = k + m by NAT_1:10;
reconsider m = m as Element of NAT by ORDINAL1:def 13;
A3: i = k + m by A2;
A4: 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 A5: UsedInt*Loc p c= ((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p) by XBOOLE_1:7;
defpred S₁[ Element of NAT ] means ( (Computation s1,(k + $1)) . (IC SCM+FSA ) = (Computation s2,(k + $1)) . (IC SCM+FSA ) & (Computation s1,(k + $1)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) = (Computation s2,(k + $1)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p)) );
A6: S₁[ 0 ] by A1;

A7: now

let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[b₁ + 1] )
assume A8: S₁[m] ; :: thesis: S₁[b₁ + 1]
set sk1 = Computation s1,(k + m);
set sk11 = Computation s1,(k + (m + 1));
set i1 = CurInstr (Computation s1,(k + m));
set sk2 = Computation s2,(k + m);
set sk12 = Computation s2,(k + (m + 1));
set i2 = CurInstr (Computation s2,(k + m));
A9: IC (Computation s1,(k + m)) in dom p by A1;
then A10: CurInstr (Computation s1,(k + m)) = ((Computation s1,(k + m)) | (dom p)) . (IC (Computation s1,(k + m))) by FUNCT_1:72;
CurInstr (Computation s1,(k + m)) = s1 . (IC (Computation s1,(k + m))) by AMI_1:54
.= p . (IC (Computation s1,(k + m))) by A1, A9, GRFUNC_1:8 ;
then A11: CurInstr (Computation s1,(k + m)) in rng p by A9, FUNCT_1:def 5;
IC (Computation s2,(k + m)) in dom p by A1;
then A12: CurInstr (Computation s2,(k + m)) = ((Computation s2,(k + m)) | (dom p)) . (IC (Computation s2,(k + m))) by FUNCT_1:72
.= CurInstr (Computation s1,(k + m)) by A1, A8, A10, AMI_1:124 ;
A13: Computation s1,(k + (m + 1)) = Computation s1,((k + m) + 1)
.= Following (Computation s1,(k + m)) by AMI_1:14
.= Exec (CurInstr (Computation s1,(k + m))),(Computation s1,(k + m)) ;
A14: Computation s2,(k + (m + 1)) = Computation s2,((k + m) + 1)
.= Following (Computation s2,(k + m)) by AMI_1:14
.= Exec (CurInstr (Computation s2,(k + m))),(Computation s2,(k + m)) ;
A15: dom (Computation s1,(k + (m + 1))) = the carrier of SCM+FSA by AMI_1:79
.= dom (Computation s2,(k + (m + 1))) by AMI_1:79 ;

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

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

then A16: CurInstr (Computation s1,(k + m)) = halt SCM+FSA by SCMFSA_2:122;
then Computation s1,(k + (m + 1)) = Computation s1,(k + m) by A13, AMI_1:def 8;
hence S₁[m + 1] by A8, A12, A14, A16, AMI_1:def 8; :: thesis: verum

end;

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

then consider da, db being Int-Location such that
A17: CurInstr (Computation s1,(k + m)) = da := db by SCMFSA_2:54;
A18: (Computation s1,(k + (m + 1))) . (IC SCM+FSA ) = Next (IC (Computation s1,(k + m))) by A13, A17, SCMFSA_2:89
.= (Computation s2,(k + (m + 1))) . (IC SCM+FSA ) by A8, A12, A14, A17, SCMFSA_2:89 ;

now

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

per cases ( x is Int-Location or x is FinSeq-Location ) by A1, A19, Th23;

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

now

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

case A21: x = da ; :: thesis: (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x

then A22: (Computation s2,(k + (m + 1))) . x = (Computation s2,(k + m)) . db by A12, A14, A17, SCMFSA_2:89;
A23: db in UsedIntLoc p by A11, A17, Th16;
then (Computation s1,(k + m)) . db = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . db by A4, A8, FUNCT_1:72
.= (Computation s2,(k + m)) . db by A4, A23, FUNCT_1:72 ;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A13, A17, A21, A22, SCMFSA_2:89; :: thesis: verum

end;

case A24: x <> da ; :: thesis: (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x

then A25: (Computation s2,(k + (m + 1))) . x = (Computation s2,(k + m)) . x by A12, A14, A17, A20, SCMFSA_2:89;
(Computation s1,(k + m)) . x = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A8, A19, FUNCT_1:72
.= (Computation s2,(k + m)) . x by A19, FUNCT_1:72 ;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A13, A17, A20, A24, A25, SCMFSA_2:89; :: thesis: verum

end;

end;

end;

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

end;

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

then A27: (Computation s2,(k + (m + 1))) . x = (Computation s2,(k + m)) . x by A12, A14, A17, SCMFSA_2:89;
(Computation s1,(k + m)) . x = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A8, A19, FUNCT_1:72
.= (Computation s2,(k + m)) . x by A19, FUNCT_1:72 ;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A13, A17, A26, A27, SCMFSA_2:89; :: thesis: verum

end;

end;

end;

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

end;

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

then consider da, db being Int-Location such that
A28: CurInstr (Computation s1,(k + m)) = AddTo da,db by SCMFSA_2:55;
A29: (Computation s1,(k + (m + 1))) . (IC SCM+FSA ) = Next (IC (Computation s1,(k + m))) by A13, A28, SCMFSA_2:90
.= (Computation s2,(k + (m + 1))) . (IC SCM+FSA ) by A8, A12, A14, A28, SCMFSA_2:90 ;

now

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

per cases ( x is Int-Location or x is FinSeq-Location ) by A1, A30, Th23;

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

now

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

case A32: x = da ; :: thesis: (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x

then A33: (Computation s2,(k + (m + 1))) . x = ((Computation s2,(k + m)) . da) + ((Computation s2,(k + m)) . db) by A12, A14, A28, SCMFSA_2:90;
A34: da in UsedIntLoc p by A11, A28, Th16;
then A35: (Computation s1,(k + m)) . da = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . da by A4, A8, FUNCT_1:72
.= (Computation s2,(k + m)) . da by A4, A34, FUNCT_1:72 ;
A36: db in UsedIntLoc p by A11, A28, Th16;
then (Computation s1,(k + m)) . db = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . db by A4, A8, FUNCT_1:72
.= (Computation s2,(k + m)) . db by A4, A36, FUNCT_1:72 ;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A13, A28, A32, A33, A35, SCMFSA_2:90; :: thesis: verum

end;

case A37: x <> da ; :: thesis: (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x

then A38: (Computation s2,(k + (m + 1))) . x = (Computation s2,(k + m)) . x by A12, A14, A28, A31, SCMFSA_2:90;
(Computation s1,(k + m)) . x = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A8, A30, FUNCT_1:72
.= (Computation s2,(k + m)) . x by A30, FUNCT_1:72 ;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A13, A28, A31, A37, A38, SCMFSA_2:90; :: thesis: verum

end;

end;

end;

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

end;

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

then A40: (Computation s2,(k + (m + 1))) . x = (Computation s2,(k + m)) . x by A12, A14, A28, SCMFSA_2:90;
(Computation s1,(k + m)) . x = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A8, A30, FUNCT_1:72
.= (Computation s2,(k + m)) . x by A30, FUNCT_1:72 ;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A13, A28, A39, A40, SCMFSA_2:90; :: thesis: verum

end;

end;

end;

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

end;

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

then consider da, db being Int-Location such that
A41: CurInstr (Computation s1,(k + m)) = SubFrom da,db by SCMFSA_2:56;
A42: (Computation s1,(k + (m + 1))) . (IC SCM+FSA ) = Next (IC (Computation s1,(k + m))) by A13, A41, SCMFSA_2:91
.= (Computation s2,(k + (m + 1))) . (IC SCM+FSA ) by A8, A12, A14, A41, SCMFSA_2:91 ;

now

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

per cases ( x is Int-Location or x is FinSeq-Location ) by A1, A43, Th23;

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

now

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

case A45: x = da ; :: thesis: (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x

then A46: (Computation s2,(k + (m + 1))) . x = ((Computation s2,(k + m)) . da) - ((Computation s2,(k + m)) . db) by A12, A14, A41, SCMFSA_2:91;
A47: da in UsedIntLoc p by A11, A41, Th16;
then A48: (Computation s1,(k + m)) . da = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . da by A4, A8, FUNCT_1:72
.= (Computation s2,(k + m)) . da by A4, A47, FUNCT_1:72 ;
A49: db in UsedIntLoc p by A11, A41, Th16;
then (Computation s1,(k + m)) . db = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . db by A4, A8, FUNCT_1:72
.= (Computation s2,(k + m)) . db by A4, A49, FUNCT_1:72 ;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A13, A41, A45, A46, A48, SCMFSA_2:91; :: thesis: verum

end;

case A50: x <> da ; :: thesis: (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x

then A51: (Computation s2,(k + (m + 1))) . x = (Computation s2,(k + m)) . x by A12, A14, A41, A44, SCMFSA_2:91;
(Computation s1,(k + m)) . x = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A8, A43, FUNCT_1:72
.= (Computation s2,(k + m)) . x by A43, FUNCT_1:72 ;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A13, A41, A44, A50, A51, SCMFSA_2:91; :: thesis: verum

end;

end;

end;

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

end;

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

then A53: (Computation s2,(k + (m + 1))) . x = (Computation s2,(k + m)) . x by A12, A14, A41, SCMFSA_2:91;
(Computation s1,(k + m)) . x = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A8, A43, FUNCT_1:72
.= (Computation s2,(k + m)) . x by A43, FUNCT_1:72 ;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A13, A41, A52, A53, SCMFSA_2:91; :: thesis: verum

end;

end;

end;

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

end;

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

then consider da, db being Int-Location such that
A54: CurInstr (Computation s1,(k + m)) = MultBy da,db by SCMFSA_2:57;
A55: (Computation s1,(k + (m + 1))) . (IC SCM+FSA ) = Next (IC (Computation s1,(k + m))) by A13, A54, SCMFSA_2:92
.= (Computation s2,(k + (m + 1))) . (IC SCM+FSA ) by A8, A12, A14, A54, SCMFSA_2:92 ;

now

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

per cases ( x is Int-Location or x is FinSeq-Location ) by A1, A56, Th23;

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

now

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

case A58: x = da ; :: thesis: (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x

then A59: (Computation s2,(k + (m + 1))) . x = ((Computation s2,(k + m)) . da) * ((Computation s2,(k + m)) . db) by A12, A14, A54, SCMFSA_2:92;
A60: da in UsedIntLoc p by A11, A54, Th16;
then A61: (Computation s1,(k + m)) . da = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . da by A4, A8, FUNCT_1:72
.= (Computation s2,(k + m)) . da by A4, A60, FUNCT_1:72 ;
A62: db in UsedIntLoc p by A11, A54, Th16;
then (Computation s1,(k + m)) . db = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . db by A4, A8, FUNCT_1:72
.= (Computation s2,(k + m)) . db by A4, A62, FUNCT_1:72 ;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A13, A54, A58, A59, A61, SCMFSA_2:92; :: thesis: verum

end;

case A63: x <> da ; :: thesis: (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x

then A64: (Computation s2,(k + (m + 1))) . x = (Computation s2,(k + m)) . x by A12, A14, A54, A57, SCMFSA_2:92;
(Computation s1,(k + m)) . x = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A8, A56, FUNCT_1:72
.= (Computation s2,(k + m)) . x by A56, FUNCT_1:72 ;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A13, A54, A57, A63, A64, SCMFSA_2:92; :: thesis: verum

end;

end;

end;

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

end;

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

then A66: (Computation s2,(k + (m + 1))) . x = (Computation s2,(k + m)) . x by A12, A14, A54, SCMFSA_2:92;
(Computation s1,(k + m)) . x = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A8, A56, FUNCT_1:72
.= (Computation s2,(k + m)) . x by A56, FUNCT_1:72 ;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A13, A54, A65, A66, SCMFSA_2:92; :: thesis: verum

end;

end;

end;

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

end;

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

then consider da, db being Int-Location such that
A67: CurInstr (Computation s1,(k + m)) = Divide da,db by SCMFSA_2:58;
A68: (Computation s1,(k + (m + 1))) . (IC SCM+FSA ) = Next (IC (Computation s1,(k + m))) by A13, A67, SCMFSA_2:93
.= (Computation s2,(k + (m + 1))) . (IC SCM+FSA ) by A8, A12, A14, A67, SCMFSA_2:93 ;

now

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

per cases ( x is Int-Location or x is FinSeq-Location ) by A1, A69, Th23;

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

A71: da in UsedIntLoc p by A11, A67, Th16;
then A72: (Computation s1,(k + m)) . da = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . da by A4, A8, FUNCT_1:72
.= (Computation s2,(k + m)) . da by A4, A71, FUNCT_1:72 ;
A73: db in UsedIntLoc p by A11, A67, Th16;
then A74: (Computation s1,(k + m)) . db = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . db by A4, A8, FUNCT_1:72
.= (Computation s2,(k + m)) . db by A4, A73, FUNCT_1:72 ;
A75: (Computation s1,(k + m)) . x = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A8, A69, FUNCT_1:72
.= (Computation s2,(k + m)) . x by A69, FUNCT_1:72 ;

now

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

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

now

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

suppose A77: x = da ; :: thesis: (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x

then (Computation s1,(k + (m + 1))) . x = ((Computation s1,(k + m)) . da) div ((Computation s1,(k + m)) . db) by A13, A67, A76, SCMFSA_2:93;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A12, A14, A67, A72, A74, A76, A77, SCMFSA_2:93; :: thesis: verum

end;

suppose A78: x = db ; :: thesis: (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x

then (Computation s1,(k + (m + 1))) . x = ((Computation s1,(k + m)) . da) mod ((Computation s1,(k + m)) . db) by A13, A67, SCMFSA_2:93;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A12, A14, A67, A72, A74, A78, SCMFSA_2:93; :: thesis: verum

end;

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

then (Computation s1,(k + (m + 1))) . x = (Computation s1,(k + m)) . x by A13, A67, A70, SCMFSA_2:93;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A12, A14, A67, A70, A75, A79, SCMFSA_2:93; :: thesis: verum

end;

end;

end;

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

end;

suppose A80: da = db ; :: thesis: (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x

now

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

case A81: x = da ; :: thesis: (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x

then (Computation s1,(k + (m + 1))) . x = ((Computation s1,(k + m)) . da) mod ((Computation s1,(k + m)) . da) by A13, A67, A80, SCMFSA_2:94;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A12, A14, A67, A72, A80, A81, SCMFSA_2:94; :: thesis: verum

end;

case A82: x <> da ; :: thesis: (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x

then (Computation s1,(k + (m + 1))) . x = (Computation s1,(k + m)) . x by A13, A67, A70, A80, SCMFSA_2:94;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A12, A14, A67, A70, A75, A80, A82, SCMFSA_2:94; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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

end;

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

then A84: (Computation s2,(k + (m + 1))) . x = (Computation s2,(k + m)) . x by A12, A14, A67, SCMFSA_2:93;
(Computation s1,(k + m)) . x = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A8, A69, FUNCT_1:72
.= (Computation s2,(k + m)) . x by A69, FUNCT_1:72 ;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A13, A67, A83, A84, SCMFSA_2:93; :: thesis: verum

end;

end;

end;

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

end;

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

then consider lb being Instruction-Location of SCM+FSA such that
A85: CurInstr (Computation s1,(k + m)) = goto lb by SCMFSA_2:59;
A86: (Computation s1,(k + (m + 1))) . (IC SCM+FSA ) = lb by A13, A85, SCMFSA_2:95
.= (Computation s2,(k + (m + 1))) . (IC SCM+FSA ) by A12, A14, A85, SCMFSA_2:95 ;

now

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

per cases ( x is Int-Location or x is FinSeq-Location ) by A1, A87, Th23;

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

then (Computation s1,(k + (m + 1))) . x = (Computation s1,(k + m)) . x by A13, A85, SCMFSA_2:95;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A12, A14, A85, A88, A89, SCMFSA_2:95; :: thesis: verum

end;

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

then (Computation s1,(k + (m + 1))) . x = (Computation s1,(k + m)) . x by A13, A85, SCMFSA_2:95;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A12, A14, A85, A88, A90, SCMFSA_2:95; :: thesis: verum

end;

end;

end;

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

end;

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

then consider lb being Instruction-Location of SCM+FSA , da being Int-Location such that
A91: CurInstr (Computation s1,(k + m)) = da =0_goto lb by SCMFSA_2:60;
A92: da in UsedIntLoc p by A11, A91, Th17;
then A93: (Computation s1,(k + m)) . da = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . da by A4, A8, FUNCT_1:72
.= (Computation s2,(k + m)) . da by A4, A92, FUNCT_1:72 ;

A94: now

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

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

hence (Computation s1,(k + (m + 1))) . (IC SCM+FSA ) = lb by A13, A91, SCMFSA_2:96
.= (Computation s2,(k + (m + 1))) . (IC SCM+FSA ) by A12, A14, A91, A93, A95, SCMFSA_2:96 ;
:: thesis: verum

end;

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

hence (Computation s1,(k + (m + 1))) . (IC SCM+FSA ) = Next (IC (Computation s2,(k + m))) by A8, A13, A91, SCMFSA_2:96
.= (Computation s2,(k + (m + 1))) . (IC SCM+FSA ) by A12, A14, A91, A93, A96, SCMFSA_2:96 ;
:: thesis: verum

end;

end;

end;

now

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

per cases ( x is Int-Location or x is FinSeq-Location ) by A1, A97, Th23;

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

then (Computation s1,(k + (m + 1))) . x = (Computation s1,(k + m)) . x by A13, A91, SCMFSA_2:96;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A12, A14, A91, A98, A99, SCMFSA_2:96; :: thesis: verum

end;

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

then (Computation s1,(k + (m + 1))) . x = (Computation s1,(k + m)) . x by A13, A91, SCMFSA_2:96;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A12, A14, A91, A98, A100, SCMFSA_2:96; :: thesis: verum

end;

end;

end;

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

end;

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

then consider lb being Instruction-Location of SCM+FSA , da being Int-Location such that
A101: CurInstr (Computation s1,(k + m)) = da >0_goto lb by SCMFSA_2:61;
A102: da in UsedIntLoc p by A11, A101, Th17;
then A103: (Computation s1,(k + m)) . da = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . da by A4, A8, FUNCT_1:72
.= (Computation s2,(k + m)) . da by A4, A102, FUNCT_1:72 ;

A104: now

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

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

hence (Computation s1,(k + (m + 1))) . (IC SCM+FSA ) = lb by A13, A101, SCMFSA_2:97
.= (Computation s2,(k + (m + 1))) . (IC SCM+FSA ) by A12, A14, A101, A103, A105, SCMFSA_2:97 ;
:: thesis: verum

end;

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

hence (Computation s1,(k + (m + 1))) . (IC SCM+FSA ) = Next (IC (Computation s2,(k + m))) by A8, A13, A101, SCMFSA_2:97
.= (Computation s2,(k + (m + 1))) . (IC SCM+FSA ) by A12, A14, A101, A103, A106, SCMFSA_2:97 ;
:: thesis: verum

end;

end;

end;

now

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

per cases ( x is Int-Location or x is FinSeq-Location ) by A1, A107, Th23;

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

then (Computation s1,(k + (m + 1))) . x = (Computation s1,(k + m)) . x by A13, A101, SCMFSA_2:97;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A12, A14, A101, A108, A109, SCMFSA_2:97; :: thesis: verum

end;

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

then (Computation s1,(k + (m + 1))) . x = (Computation s1,(k + m)) . x by A13, A101, SCMFSA_2:97;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A12, A14, A101, A108, A110, SCMFSA_2:97; :: thesis: verum

end;

end;

end;

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

end;

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

then consider a, b being Int-Location , fa being FinSeq-Location such that
A111: CurInstr (Computation s1,(k + m)) = b := fa,a by SCMFSA_2:62;
A112: (Computation s1,(k + (m + 1))) . (IC SCM+FSA ) = Next (IC (Computation s2,(k + m))) by A8, A13, A111, SCMFSA_2:98
.= (Computation s2,(k + (m + 1))) . (IC SCM+FSA ) by A12, A14, A111, SCMFSA_2:98 ;

now

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

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

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

now

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

case A115: x = b ; :: thesis: (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x

consider k1 being Element of NAT such that
A116: ( k1 = abs ((Computation s1,(k + m)) . a) & (Exec (b := fa,a),(Computation s1,(k + m))) . b = ((Computation s1,(k + m)) . fa) /. k1 ) by SCMFSA_2:98;
consider k2 being Element of NAT such that
A117: ( k2 = abs ((Computation s2,(k + m)) . a) & (Exec (b := fa,a),(Computation s2,(k + m))) . b = ((Computation s2,(k + m)) . fa) /. k2 ) by SCMFSA_2:98;
A118: a in UsedIntLoc p by A11, A111, Th18;
then A119: (Computation s1,(k + m)) . a = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . a by A4, A8, FUNCT_1:72
.= (Computation s2,(k + m)) . a by A4, A118, FUNCT_1:72 ;
A120: fa in UsedInt*Loc p by A11, A111, Th19;
then (Computation s1,(k + m)) . fa = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . fa by A5, A8, FUNCT_1:72
.= (Computation s2,(k + m)) . fa by A5, A120, FUNCT_1:72 ;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A12, A13, A14, A111, A115, A116, A117, A119; :: thesis: verum

end;

case A121: x <> b ; :: thesis: (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x

then A122: (Computation s2,(k + (m + 1))) . x = (Computation s2,(k + m)) . x by A12, A14, A111, A114, SCMFSA_2:98;
(Computation s1,(k + m)) . x = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A8, A113, FUNCT_1:72
.= (Computation s2,(k + m)) . x by A113, FUNCT_1:72 ;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A13, A111, A114, A121, A122, SCMFSA_2:98; :: thesis: verum

end;

end;

end;

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

end;

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

then A124: (Computation s2,(k + (m + 1))) . x = (Computation s2,(k + m)) . x by A12, A14, A111, SCMFSA_2:98;
(Computation s1,(k + m)) . x = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A8, A113, FUNCT_1:72
.= (Computation s2,(k + m)) . x by A113, FUNCT_1:72 ;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A13, A111, A123, A124, SCMFSA_2:98; :: thesis: verum

end;

end;

end;

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

end;

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

then consider a, b being Int-Location , fa being FinSeq-Location such that
A125: CurInstr (Computation s1,(k + m)) = fa,a := b by SCMFSA_2:63;
A126: (Computation s1,(k + (m + 1))) . (IC SCM+FSA ) = Next (IC (Computation s2,(k + m))) by A8, A13, A125, SCMFSA_2:99
.= (Computation s2,(k + (m + 1))) . (IC SCM+FSA ) by A12, A14, A125, SCMFSA_2:99 ;

now

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

per cases ( x is FinSeq-Location or x is Int-Location ) by A1, A127, Th23;

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

now

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

case A129: x = fa ; :: thesis: (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x

consider k1 being Element of NAT such that
A130: ( k1 = abs ((Computation s1,(k + m)) . a) & (Exec (fa,a := b),(Computation s1,(k + m))) . fa = ((Computation s1,(k + m)) . fa) +* k1,((Computation s1,(k + m)) . b) ) by SCMFSA_2:99;
consider k2 being Element of NAT such that
A131: ( k2 = abs ((Computation s2,(k + m)) . a) & (Exec (fa,a := b),(Computation s2,(k + m))) . fa = ((Computation s2,(k + m)) . fa) +* k2,((Computation s2,(k + m)) . b) ) by SCMFSA_2:99;
A132: a in UsedIntLoc p by A11, A125, Th18;
then A133: (Computation s1,(k + m)) . a = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . a by A4, A8, FUNCT_1:72
.= (Computation s2,(k + m)) . a by A4, A132, FUNCT_1:72 ;
A134: b in UsedIntLoc p by A11, A125, Th18;
then A135: (Computation s1,(k + m)) . b = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . b by A4, A8, FUNCT_1:72
.= (Computation s2,(k + m)) . b by A4, A134, FUNCT_1:72 ;
A136: fa in UsedInt*Loc p by A11, A125, Th19;
then (Computation s1,(k + m)) . fa = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . fa by A5, A8, FUNCT_1:72
.= (Computation s2,(k + m)) . fa by A5, A136, FUNCT_1:72 ;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A12, A13, A14, A125, A129, A130, A131, A133, A135; :: thesis: verum

end;

case A137: x <> fa ; :: thesis: (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x

then A138: (Computation s2,(k + (m + 1))) . x = (Computation s2,(k + m)) . x by A12, A14, A125, A128, SCMFSA_2:99;
(Computation s1,(k + m)) . x = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A8, A127, FUNCT_1:72
.= (Computation s2,(k + m)) . x by A127, FUNCT_1:72 ;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A13, A125, A128, A137, A138, SCMFSA_2:99; :: thesis: verum

end;

end;

end;

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

end;

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

then A140: (Computation s2,(k + (m + 1))) . x = (Computation s2,(k + m)) . x by A12, A14, A125, SCMFSA_2:99;
(Computation s1,(k + m)) . x = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A8, A127, FUNCT_1:72
.= (Computation s2,(k + m)) . x by A127, FUNCT_1:72 ;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A13, A125, A139, A140, SCMFSA_2:99; :: thesis: verum

end;

end;

end;

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

end;

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

then consider a being Int-Location , fa being FinSeq-Location such that
A141: CurInstr (Computation s1,(k + m)) = a :=len fa by SCMFSA_2:64;
A142: (Computation s1,(k + (m + 1))) . (IC SCM+FSA ) = Next (IC (Computation s2,(k + m))) by A8, A13, A141, SCMFSA_2:100
.= (Computation s2,(k + (m + 1))) . (IC SCM+FSA ) by A12, A14, A141, SCMFSA_2:100 ;

now

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

per cases ( x is Int-Location or x is FinSeq-Location ) by A1, A143, Th23;

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

now

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

case A145: x = a ; :: thesis: (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x

then A146: (Computation s2,(k + (m + 1))) . x = len ((Computation s2,(k + m)) . fa) by A12, A14, A141, SCMFSA_2:100;
A147: fa in UsedInt*Loc p by A11, A141, Th21;
then (Computation s1,(k + m)) . fa = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . fa by A5, A8, FUNCT_1:72
.= (Computation s2,(k + m)) . fa by A5, A147, FUNCT_1:72 ;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A13, A141, A145, A146, SCMFSA_2:100; :: thesis: verum

end;

case A148: x <> a ; :: thesis: (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x

then A149: (Computation s2,(k + (m + 1))) . x = (Computation s2,(k + m)) . x by A12, A14, A141, A144, SCMFSA_2:100;
(Computation s1,(k + m)) . x = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A8, A143, FUNCT_1:72
.= (Computation s2,(k + m)) . x by A143, FUNCT_1:72 ;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A13, A141, A144, A148, A149, SCMFSA_2:100; :: thesis: verum

end;

end;

end;

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

end;

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

then A151: (Computation s2,(k + (m + 1))) . x = (Computation s2,(k + m)) . x by A12, A14, A141, SCMFSA_2:100;
(Computation s1,(k + m)) . x = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A8, A143, FUNCT_1:72
.= (Computation s2,(k + m)) . x by A143, FUNCT_1:72 ;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A13, A141, A150, A151, SCMFSA_2:100; :: thesis: verum

end;

end;

end;

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

end;

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

then consider a being Int-Location , fa being FinSeq-Location such that
A152: CurInstr (Computation s1,(k + m)) = fa :=<0,...,0> a by SCMFSA_2:65;
A153: (Computation s1,(k + (m + 1))) . (IC SCM+FSA ) = Next (IC (Computation s2,(k + m))) by A8, A13, A152, SCMFSA_2:101
.= (Computation s2,(k + (m + 1))) . (IC SCM+FSA ) by A12, A14, A152, SCMFSA_2:101 ;

now

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

per cases ( x is FinSeq-Location or x is Int-Location ) by A1, A154, Th23;

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

now

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

case A156: x = fa ; :: thesis: (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x

consider k1 being Element of NAT such that
A157: ( k1 = abs ((Computation s1,(k + m)) . a) & (Exec (fa :=<0,...,0> a),(Computation s1,(k + m))) . fa = k1 |-> 0 ) by SCMFSA_2:101;
consider k2 being Element of NAT such that
A158: ( k2 = abs ((Computation s2,(k + m)) . a) & (Exec (fa :=<0,...,0> a),(Computation s2,(k + m))) . fa = k2 |-> 0 ) by SCMFSA_2:101;
A159: a in UsedIntLoc p by A11, A152, Th20;
then (Computation s1,(k + m)) . a = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . a by A4, A8, FUNCT_1:72
.= (Computation s2,(k + m)) . a by A4, A159, FUNCT_1:72 ;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A12, A13, A14, A152, A156, A157, A158; :: thesis: verum

end;

case A160: x <> fa ; :: thesis: (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x

then A161: (Computation s2,(k + (m + 1))) . x = (Computation s2,(k + m)) . x by A12, A14, A152, A155, SCMFSA_2:101;
(Computation s1,(k + m)) . x = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A8, A154, FUNCT_1:72
.= (Computation s2,(k + m)) . x by A154, FUNCT_1:72 ;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A13, A152, A155, A160, A161, SCMFSA_2:101; :: thesis: verum

end;

end;

end;

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

end;

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

then A163: (Computation s2,(k + (m + 1))) . x = (Computation s2,(k + m)) . x by A12, A14, A152, SCMFSA_2:101;
(Computation s1,(k + m)) . x = ((Computation s2,(k + m)) | (((dom t) \/ (UsedInt*Loc p)) \/ (UsedIntLoc p))) . x by A8, A154, FUNCT_1:72
.= (Computation s2,(k + m)) . x by A154, FUNCT_1:72 ;
hence (Computation s1,(k + (m + 1))) . x = (Computation s2,(k + (m + 1))) . x by A13, A152, A162, A163, SCMFSA_2:101; :: thesis: verum

end;

end;

end;

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

end;

end;

end;

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