let I be Program of ; :: thesis:
let n be Nat; :: thesis:
let s, t be State of SCM+FSA; :: thesis:
let P, Q be Instruction-Sequence of SCM+FSA; :: thesis:
assume A1: ( I c= P & I c= Q ) ; :: thesis:
assume that
A2: Start-At (0,SCM+FSA) c= s and
A3: Start-At (0,SCM+FSA) c= t and
A4: s | (UsedILoc I) = t | (UsedILoc I) and
A5: s | (UsedI*Loc I) = t | (UsedI*Loc I) and
A6: for m being Nat st m < n holds
IC (Comput (P,s,m)) in dom I ; :: thesis:
defpred S₁[ Nat] means ( $1 < n implies ( IC (Comput (Q,t,$1)) in dom I & IC (Comput (P,s,$1)) = IC (Comput (Q,t,$1)) & ( for a being Int-Location st a in UsedILoc I holds
(Comput (P,s,$1)) . a = (Comput (Q,t,$1)) . a ) & ( for f being FinSeq-Location st f in UsedI*Loc I holds
(Comput (P,s,$1)) . f = (Comput (Q,t,$1)) . f ) ) );

A7: now :: thesis:

let m be Nat; :: thesis:
assume A8: S₁[m] ; :: thesis:
thus S₁[m + 1] :: thesis:

proof

set i = P . (IC (Comput (P,s,m)));
dom P = NAT by PARTFUN1:def 2;
then A9: P /. (IC (Comput (P,s,m))) = P . (IC (Comput (P,s,m))) by PARTFUN1:def 6;
set m1 = m + 1;
A10: Comput (P,s,(m + 1)) = Following (P,(Comput (P,s,m))) by EXTPRO_1:3
.= Exec ((P . (IC (Comput (P,s,m)))),(Comput (P,s,m))) by A9 ;
assume A11: m + 1 < n ; :: thesis:

now :: thesis:

thus dom ((Comput (P,s,m)) | (UsedI*Loc I)) = (dom (Comput (P,s,m))) /\ (UsedI*Loc I) by RELAT_1:61
.= the carrier of SCM+FSA /\ (UsedI*Loc I) by PARTFUN1:def 2
.= (dom (Comput (Q,t,m))) /\ (UsedI*Loc I) by PARTFUN1:def 2 ; :: thesis:
let x be object ; :: thesis:
assume x in dom ((Comput (P,s,m)) | (UsedI*Loc I)) ; :: thesis:
then A12: x in UsedI*Loc I by RELAT_1:57;
then x in FinSeq-Locations ;
then reconsider x9 = x as FinSeq-Location by SCMFSA_2:def 5;
thus ((Comput (P,s,m)) | (UsedI*Loc I)) . x = (Comput (P,s,m)) . x9 by A12, FUNCT_1:49
.= (Comput (Q,t,m)) . x by A8, A11, A12, NAT_1:13 ; :: thesis:

end;

then A13: (Comput (P,s,m)) | (UsedI*Loc I) = (Comput (Q,t,m)) | (UsedI*Loc I) by FUNCT_1:46;
A14: P . (IC (Comput (P,s,m))) = I . (IC (Comput (P,s,m))) by A8, A11, A1, GRFUNC_1:2, NAT_1:13;
then A15: P . (IC (Comput (P,s,m))) = Q . (IC (Comput (Q,t,m))) by A8, A11, A1, GRFUNC_1:2, NAT_1:13;

now :: thesis:

thus dom ((Comput (P,s,m)) | (UsedILoc I)) = (dom (Comput (P,s,m))) /\ (UsedILoc I) by RELAT_1:61
.= the carrier of SCM+FSA /\ (UsedILoc I) by PARTFUN1:def 2
.= (dom (Comput (Q,t,m))) /\ (UsedILoc I) by PARTFUN1:def 2 ; :: thesis:
let x be object ; :: thesis:
assume x in dom ((Comput (P,s,m)) | (UsedILoc I)) ; :: thesis:
then A16: x in UsedILoc I by RELAT_1:57;
then x in Int-Locations ;
then reconsider x9 = x as Int-Location by AMI_2:def 16;
thus ((Comput (P,s,m)) | (UsedILoc I)) . x = (Comput (P,s,m)) . x9 by A16, FUNCT_1:49
.= (Comput (Q,t,m)) . x by A8, A11, A16, NAT_1:13 ; :: thesis:

end;

then A17: (Comput (P,s,m)) | (UsedILoc I) = (Comput (Q,t,m)) | (UsedILoc I) by FUNCT_1:46;
dom Q = NAT by PARTFUN1:def 2;
then A18: Q /. (IC (Comput (Q,t,m))) = Q . (IC (Comput (Q,t,m))) by PARTFUN1:def 6;
A19: Comput (Q,t,(m + 1)) = Following (Q,(Comput (Q,t,m))) by EXTPRO_1:3
.= Exec ((Q . (IC (Comput (Q,t,m)))),(Comput (Q,t,m))) by A18 ;
m < n by A11, NAT_1:13;
then IC (Comput (P,s,m)) in dom I by A6;
then A20: P . (IC (Comput (P,s,m))) in rng I by A14, FUNCT_1:def 3;
then A21: (Comput (P,s,m)) | (UsedInt*Loc (P . (IC (Comput (P,s,m))))) = ((Comput (P,s,m)) | (UsedI*Loc I)) | (UsedInt*Loc (P . (IC (Comput (P,s,m))))) by Th35, RELAT_1:74
.= (Comput (Q,t,m)) | (UsedInt*Loc (P . (IC (Comput (P,s,m))))) by A20, A13, Th35, RELAT_1:74 ;
A22: (Comput (P,s,m)) | (UsedIntLoc (P . (IC (Comput (P,s,m))))) = ((Comput (P,s,m)) | (UsedILoc I)) | (UsedIntLoc (P . (IC (Comput (P,s,m))))) by A20, Th19, RELAT_1:74
.= (Comput (Q,t,m)) | (UsedIntLoc (P . (IC (Comput (P,s,m))))) by A20, A17, Th19, RELAT_1:74 ;
then A23: (Exec ((P . (IC (Comput (P,s,m)))),(Comput (P,s,m)))) | (UsedInt*Loc (P . (IC (Comput (P,s,m))))) = (Exec ((P . (IC (Comput (P,s,m)))),(Comput (Q,t,m)))) | (UsedInt*Loc (P . (IC (Comput (P,s,m))))) by A8, A11, A21, Th64, NAT_1:13;
A24: IC (Exec ((P . (IC (Comput (P,s,m)))),(Comput (P,s,m)))) = IC (Exec ((P . (IC (Comput (P,s,m)))),(Comput (Q,t,m)))) by A8, A11, A22, A21, Th64, NAT_1:13;
hence IC (Comput (Q,t,(m + 1))) in dom I by A6, A11, A10, A19, A15; :: thesis:
thus IC (Comput (P,s,(m + 1))) = IC (Comput (Q,t,(m + 1))) by A8, A11, A10, A19, A14, A24, A1, GRFUNC_1:2, NAT_1:13; :: thesis:
A25: (Exec ((P . (IC (Comput (P,s,m)))),(Comput (P,s,m)))) | (UsedIntLoc (P . (IC (Comput (P,s,m))))) = (Exec ((P . (IC (Comput (P,s,m)))),(Comput (Q,t,m)))) | (UsedIntLoc (P . (IC (Comput (P,s,m))))) by A8, A11, A22, A21, Th64, NAT_1:13;

hereby :: thesis:

let a be Int-Location; :: thesis:
assume A26: a in UsedILoc I ; :: thesis:

per cases ;

suppose A27: a in UsedIntLoc (P . (IC (Comput (P,s,m)))) ; :: thesis:

hence (Comput (P,s,(m + 1))) . a = ((Exec ((P . (IC (Comput (P,s,m)))),(Comput (P,s,m)))) | (UsedIntLoc (P . (IC (Comput (P,s,m)))))) . a by A10, FUNCT_1:49
.= (Comput (Q,t,(m + 1))) . a by A19, A15, A25, A27, FUNCT_1:49 ;
:: thesis:

end;

suppose A28: not a in UsedIntLoc (P . (IC (Comput (P,s,m)))) ; :: thesis:

hence (Comput (P,s,(m + 1))) . a = (Comput (P,s,m)) . a by A10, Th60
.= (Comput (Q,t,m)) . a by A8, A11, A26, NAT_1:13
.= (Comput (Q,t,(m + 1))) . a by A19, A15, A28, Th60 ;
:: thesis:

end;

let f be FinSeq-Location ; :: thesis:
assume A29: f in UsedI*Loc I ; :: thesis:

per cases ;

suppose A30: f in UsedInt*Loc (P . (IC (Comput (P,s,m)))) ; :: thesis:

hence (Comput (P,s,(m + 1))) . f = ((Exec ((P . (IC (Comput (P,s,m)))),(Comput (P,s,m)))) | (UsedInt*Loc (P . (IC (Comput (P,s,m)))))) . f by A10, FUNCT_1:49
.= (Comput (Q,t,(m + 1))) . f by A19, A15, A23, A30, FUNCT_1:49 ;
:: thesis:

end;

suppose A31: not f in UsedInt*Loc (P . (IC (Comput (P,s,m)))) ; :: thesis:

hence (Comput (P,s,(m + 1))) . f = (Comput (P,s,m)) . f by A10, Th62
.= (Comput (Q,t,m)) . f by A8, A11, A29, NAT_1:13
.= (Comput (Q,t,(m + 1))) . f by A19, A15, A31, Th62 ;
:: thesis:

end;

A32: S₁[ 0 ]

proof

A33: IC (Comput (Q,t,0)) = IC t
.= 0 by A3, MEMSTR_0:39 ;
A34: IC (Comput (P,s,0)) = IC s
.= 0 by A2, MEMSTR_0:39 ;
assume 0 < n ; :: thesis:
hence IC (Comput (Q,t,0)) in dom I by A6, A34, A33; :: thesis:
thus IC (Comput (P,s,0)) = IC (Comput (Q,t,0)) by A34, A33; :: thesis:

hereby :: thesis:

let a be Int-Location; :: thesis:
assume A35: a in UsedILoc I ; :: thesis:
thus (Comput (P,s,0)) . a = s . a
.= (s | (UsedILoc I)) . a by A35, FUNCT_1:49
.= t . a by A4, A35, FUNCT_1:49
.= (Comput (Q,t,0)) . a ; :: thesis:

end;

let f be FinSeq-Location ; :: thesis:
assume A36: f in UsedI*Loc I ; :: thesis:
thus (Comput (P,s,0)) . f = s . f
.= (s | (UsedI*Loc I)) . f by A36, FUNCT_1:49
.= t . f by A5, A36, FUNCT_1:49
.= (Comput (Q,t,0)) . f ; :: thesis:

end;

A37: for m being Nat holds S₁[m] from NAT_1:sch 2(A32, A7);
hence for m being Nat st m < n holds
IC (Comput (Q,t,m)) in dom I ; :: thesis:
let m be Nat; :: thesis:
assume A38: m <= n ; :: thesis:

per cases by NAT_1:6;

suppose A39: m = 0 ; :: thesis:

A40: IC (Comput (Q,t,0)) = IC t
.= 0 by A3, MEMSTR_0:39 ;
IC (Comput (P,s,0)) = IC s
.= 0 by A2, MEMSTR_0:39 ;
hence IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) by A39, A40; :: thesis:

hereby :: thesis:

let a be Int-Location; :: thesis:
assume A41: a in UsedILoc I ; :: thesis:
thus (Comput (P,s,m)) . a = s . a by A39
.= (s | (UsedILoc I)) . a by A41, FUNCT_1:49
.= t . a by A4, A41, FUNCT_1:49
.= (Comput (Q,t,m)) . a by A39 ; :: thesis:

end;

let f be FinSeq-Location ; :: thesis:
assume A42: f in UsedI*Loc I ; :: thesis:
thus (Comput (P,s,m)) . f = s . f by A39
.= (s | (UsedI*Loc I)) . f by A42, FUNCT_1:49
.= t . f by A5, A42, FUNCT_1:49
.= (Comput (Q,t,m)) . f by A39 ; :: thesis:

end;

suppose ex p being Nat st m = p + 1 ; :: thesis:

then consider p being Nat such that
A43: m = p + 1 ;
reconsider p = p as Nat ;
A44: p < n by A38, A43, NAT_1:13;
then A45: IC (Comput (P,s,p)) in dom I by A6;

now :: thesis:

thus dom ((Comput (P,s,p)) | (UsedI*Loc I)) = (dom (Comput (P,s,p))) /\ (UsedI*Loc I) by RELAT_1:61
.= the carrier of SCM+FSA /\ (UsedI*Loc I) by PARTFUN1:def 2
.= (dom (Comput (Q,t,p))) /\ (UsedI*Loc I) by PARTFUN1:def 2 ; :: thesis:
let x be object ; :: thesis:
assume x in dom ((Comput (P,s,p)) | (UsedI*Loc I)) ; :: thesis:
then A46: x in UsedI*Loc I by RELAT_1:57;
then x in FinSeq-Locations ;
then reconsider x9 = x as FinSeq-Location by SCMFSA_2:def 5;
thus ((Comput (P,s,p)) | (UsedI*Loc I)) . x = (Comput (P,s,p)) . x9 by A46, FUNCT_1:49
.= (Comput (Q,t,p)) . x by A37, A44, A46 ; :: thesis:

end;

then A47: (Comput (P,s,p)) | (UsedI*Loc I) = (Comput (Q,t,p)) | (UsedI*Loc I) by FUNCT_1:46;
set i = P . (IC (Comput (P,s,p)));
set p1 = p + 1;
dom P = NAT by PARTFUN1:def 2;
then A48: P /. (IC (Comput (P,s,p))) = P . (IC (Comput (P,s,p))) by PARTFUN1:def 6;
A49: Comput (P,s,(p + 1)) = Following (P,(Comput (P,s,p))) by EXTPRO_1:3
.= Exec ((P . (IC (Comput (P,s,p)))),(Comput (P,s,p))) by A48 ;

now :: thesis:

thus dom ((Comput (P,s,p)) | (UsedILoc I)) = (dom (Comput (P,s,p))) /\ (UsedILoc I) by RELAT_1:61
.= the carrier of SCM+FSA /\ (UsedILoc I) by PARTFUN1:def 2
.= (dom (Comput (Q,t,p))) /\ (UsedILoc I) by PARTFUN1:def 2 ; :: thesis:
let x be object ; :: thesis:
assume x in dom ((Comput (P,s,p)) | (UsedILoc I)) ; :: thesis:
then A50: x in UsedILoc I by RELAT_1:57;
then x in Int-Locations ;
then reconsider x9 = x as Int-Location by AMI_2:def 16;
thus ((Comput (P,s,p)) | (UsedILoc I)) . x = (Comput (P,s,p)) . x9 by A50, FUNCT_1:49
.= (Comput (Q,t,p)) . x by A37, A44, A50 ; :: thesis:

end;

then A51: (Comput (P,s,p)) | (UsedILoc I) = (Comput (Q,t,p)) | (UsedILoc I) by FUNCT_1:46;
A52: IC (Comput (P,s,p)) = IC (Comput (Q,t,p)) by A37, A44;
A53: P . (IC (Comput (P,s,p))) = I . (IC (Comput (P,s,p))) by A45, A1, GRFUNC_1:2;
dom Q = NAT by PARTFUN1:def 2;
then A54: Q /. (IC (Comput (Q,t,p))) = Q . (IC (Comput (Q,t,p))) by PARTFUN1:def 6;
A55: Comput (Q,t,(p + 1)) = Following (Q,(Comput (Q,t,p))) by EXTPRO_1:3
.= Exec ((Q . (IC (Comput (Q,t,p)))),(Comput (Q,t,p))) by A54 ;
A56: P . (IC (Comput (P,s,p))) = Q . (IC (Comput (Q,t,p))) by A52, A45, A53, A1, GRFUNC_1:2;
IC (Comput (P,s,p)) in dom I by A6, A44;
then A57: P . (IC (Comput (P,s,p))) in rng I by A53, FUNCT_1:def 3;
then A58: (Comput (P,s,p)) | (UsedInt*Loc (P . (IC (Comput (P,s,p))))) = ((Comput (P,s,p)) | (UsedI*Loc I)) | (UsedInt*Loc (P . (IC (Comput (P,s,p))))) by Th35, RELAT_1:74
.= (Comput (Q,t,p)) | (UsedInt*Loc (P . (IC (Comput (P,s,p))))) by A57, A47, Th35, RELAT_1:74 ;
A59: (Comput (P,s,p)) | (UsedIntLoc (P . (IC (Comput (P,s,p))))) = ((Comput (P,s,p)) | (UsedILoc I)) | (UsedIntLoc (P . (IC (Comput (P,s,p))))) by A57, Th19, RELAT_1:74
.= (Comput (Q,t,p)) | (UsedIntLoc (P . (IC (Comput (P,s,p))))) by A57, A51, Th19, RELAT_1:74 ;
hence IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) by A43, A49, A55, A52, A56, A58, Th64; :: thesis:
A60: (Exec ((P . (IC (Comput (P,s,p)))),(Comput (P,s,p)))) | (UsedIntLoc (P . (IC (Comput (P,s,p))))) = (Exec ((P . (IC (Comput (P,s,p)))),(Comput (Q,t,p)))) | (UsedIntLoc (P . (IC (Comput (P,s,p))))) by A52, A59, A58, Th64;

hereby :: thesis:

let a be Int-Location; :: thesis:
assume A61: a in UsedILoc I ; :: thesis:

per cases ;

suppose A62: a in UsedIntLoc (P . (IC (Comput (P,s,p)))) ; :: thesis:

hence (Comput (P,s,m)) . a = ((Exec ((P . (IC (Comput (P,s,p)))),(Comput (P,s,p)))) | (UsedIntLoc (P . (IC (Comput (P,s,p)))))) . a by A43, A49, FUNCT_1:49
.= (Comput (Q,t,m)) . a by A43, A55, A56, A60, A62, FUNCT_1:49 ;
:: thesis:

end;

suppose A63: not a in UsedIntLoc (P . (IC (Comput (P,s,p)))) ; :: thesis:

hence (Comput (P,s,m)) . a = (Comput (P,s,p)) . a by A43, A49, Th60
.= (Comput (Q,t,p)) . a by A37, A44, A61
.= (Comput (Q,t,m)) . a by A43, A55, A56, A63, Th60 ;
:: thesis:

end;

A64: (Exec ((P . (IC (Comput (P,s,p)))),(Comput (P,s,p)))) | (UsedInt*Loc (P . (IC (Comput (P,s,p))))) = (Exec ((P . (IC (Comput (P,s,p)))),(Comput (Q,t,p)))) | (UsedInt*Loc (P . (IC (Comput (P,s,p))))) by A52, A59, A58, Th64;

hereby :: thesis:

let f be FinSeq-Location ; :: thesis:
assume A65: f in UsedI*Loc I ; :: thesis:

per cases ;

suppose A66: f in UsedInt*Loc (P . (IC (Comput (P,s,p)))) ; :: thesis:

hence (Comput (P,s,m)) . f = ((Exec ((P . (IC (Comput (P,s,p)))),(Comput (P,s,p)))) | (UsedInt*Loc (P . (IC (Comput (P,s,p)))))) . f by A43, A49, FUNCT_1:49
.= (Comput (Q,t,m)) . f by A43, A55, A56, A64, A66, FUNCT_1:49 ;
:: thesis:

end;

suppose A67: not f in UsedInt*Loc (P . (IC (Comput (P,s,p)))) ; :: thesis:

hence (Comput (P,s,m)) . f = (Comput (P,s,p)) . f by A43, A49, Th62
.= (Comput (Q,t,p)) . f by A37, A44, A65
.= (Comput (Q,t,m)) . f by A43, A55, A56, A67, Th62 ;
:: thesis:

end;