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

A6: now

let m be Element of NAT ; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume A7: S₁[m] ; :: thesis: S₁[m + 1]
thus S₁[m + 1] :: thesis: verum

proof

dom I misses dom (Start-At 0 ,SCM+FSA ) by Th64;
then A8: I c= I +* (Start-At 0 ,SCM+FSA ) by FUNCT_4:33;
then I c= t by A2, XBOOLE_1:1;
then A9: I c= Comput (ProgramPart t),t,m by AMI_1:81;
set i = (Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m));
Y: (ProgramPart (Comput (ProgramPart s),s,m)) /. (IC (Comput (ProgramPart s),s,m)) = (Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m)) by COMPOS_1:38;
set m1 = m + 1;
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,m) by AMI_1:123;
A10: Comput (ProgramPart s),s,(m + 1) = Following (ProgramPart s),(Comput (ProgramPart s),s,m) by AMI_1:14
.= Exec ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m))),(Comput (ProgramPart s),s,m) by Y, T ;
assume A11: m + 1 < n ; :: thesis: ( IC (Comput (ProgramPart t),t,(m + 1)) in dom I & IC (Comput (ProgramPart s),s,(m + 1)) = IC (Comput (ProgramPart t),t,(m + 1)) & ( for a being Int-Location st a in UsedIntLoc I holds
(Comput (ProgramPart s),s,(m + 1)) . a = (Comput (ProgramPart t),t,(m + 1)) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Comput (ProgramPart s),s,(m + 1)) . f = (Comput (ProgramPart t),t,(m + 1)) . f ) )

now

thus dom ((Comput (ProgramPart s),s,m) | (UsedInt*Loc I)) = (dom (Comput (ProgramPart s),s,m)) /\ (UsedInt*Loc I) by RELAT_1:90
.= the carrier of SCM+FSA /\ (UsedInt*Loc I) by PARTFUN1:def 4
.= (dom (Comput (ProgramPart t),t,m)) /\ (UsedInt*Loc I) by PARTFUN1:def 4 ; :: thesis: for x being set st x in dom ((Comput (ProgramPart s),s,m) | (UsedInt*Loc I)) holds
((Comput (ProgramPart s),s,m) | (UsedInt*Loc I)) . x = (Comput (ProgramPart t),t,m) . x
let x be set ; :: thesis: ( x in dom ((Comput (ProgramPart s),s,m) | (UsedInt*Loc I)) implies ((Comput (ProgramPart s),s,m) | (UsedInt*Loc I)) . x = (Comput (ProgramPart t),t,m) . x )
assume x in dom ((Comput (ProgramPart s),s,m) | (UsedInt*Loc I)) ; :: thesis: ((Comput (ProgramPart s),s,m) | (UsedInt*Loc I)) . x = (Comput (ProgramPart t),t,m) . x
then A12: x in UsedInt*Loc I by RELAT_1:86;
then reconsider x9 = x as FinSeq-Location by SCMFSA_2:12;
thus ((Comput (ProgramPart s),s,m) | (UsedInt*Loc I)) . x = (Comput (ProgramPart s),s,m) . x9 by A12, FUNCT_1:72
.= (Comput (ProgramPart t),t,m) . x by A7, A11, A12, NAT_1:13 ; :: thesis: verum

end;

then A13: (Comput (ProgramPart s),s,m) | (UsedInt*Loc I) = (Comput (ProgramPart t),t,m) | (UsedInt*Loc I) by FUNCT_1:68;
I c= s by A1, A8, XBOOLE_1:1;
then I c= Comput (ProgramPart s),s,m by AMI_1:81;
then A14: (Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m)) = I . (IC (Comput (ProgramPart s),s,m)) by A7, A11, GRFUNC_1:8, NAT_1:13;
then A15: (Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m)) = (Comput (ProgramPart t),t,m) . (IC (Comput (ProgramPart t),t,m)) by A7, A11, A9, GRFUNC_1:8, NAT_1:13;

now

thus dom ((Comput (ProgramPart s),s,m) | (UsedIntLoc I)) = (dom (Comput (ProgramPart s),s,m)) /\ (UsedIntLoc I) by RELAT_1:90
.= the carrier of SCM+FSA /\ (UsedIntLoc I) by PARTFUN1:def 4
.= (dom (Comput (ProgramPart t),t,m)) /\ (UsedIntLoc I) by PARTFUN1:def 4 ; :: thesis: for x being set st x in dom ((Comput (ProgramPart s),s,m) | (UsedIntLoc I)) holds
((Comput (ProgramPart s),s,m) | (UsedIntLoc I)) . x = (Comput (ProgramPart t),t,m) . x
let x be set ; :: thesis: ( x in dom ((Comput (ProgramPart s),s,m) | (UsedIntLoc I)) implies ((Comput (ProgramPart s),s,m) | (UsedIntLoc I)) . x = (Comput (ProgramPart t),t,m) . x )
assume x in dom ((Comput (ProgramPart s),s,m) | (UsedIntLoc I)) ; :: thesis: ((Comput (ProgramPart s),s,m) | (UsedIntLoc I)) . x = (Comput (ProgramPart t),t,m) . x
then A16: x in UsedIntLoc I by RELAT_1:86;
then reconsider x9 = x as Int-Location by SCMFSA_2:11;
thus ((Comput (ProgramPart s),s,m) | (UsedIntLoc I)) . x = (Comput (ProgramPart s),s,m) . x9 by A16, FUNCT_1:72
.= (Comput (ProgramPart t),t,m) . x by A7, A11, A16, NAT_1:13 ; :: thesis: verum

end;

then A17: (Comput (ProgramPart s),s,m) | (UsedIntLoc I) = (Comput (ProgramPart t),t,m) | (UsedIntLoc I) by FUNCT_1:68;
Y: (ProgramPart (Comput (ProgramPart t),t,m)) /. (IC (Comput (ProgramPart t),t,m)) = (Comput (ProgramPart t),t,m) . (IC (Comput (ProgramPart t),t,m)) by COMPOS_1:38;
T: ProgramPart t = ProgramPart (Comput (ProgramPart t),t,m) by AMI_1:123;
A18: Comput (ProgramPart t),t,(m + 1) = Following (ProgramPart t),(Comput (ProgramPart t),t,m) by AMI_1:14
.= Exec ((Comput (ProgramPart t),t,m) . (IC (Comput (ProgramPart t),t,m))),(Comput (ProgramPart t),t,m) by Y, T ;
m < n by A11, NAT_1:13;
then IC (Comput (ProgramPart s),s,m) in dom I by A5;
then A19: (Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m)) in rng I by A14, FUNCT_1:def 5;
then A20: (Comput (ProgramPart s),s,m) | (UsedInt*Loc ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m)))) = ((Comput (ProgramPart s),s,m) | (UsedInt*Loc I)) | (UsedInt*Loc ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m)))) by Th39, RELAT_1:103
.= (Comput (ProgramPart t),t,m) | (UsedInt*Loc ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m)))) by A19, A13, Th39, RELAT_1:103 ;
A21: (Comput (ProgramPart s),s,m) | (UsedIntLoc ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m)))) = ((Comput (ProgramPart s),s,m) | (UsedIntLoc I)) | (UsedIntLoc ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m)))) by A19, Th23, RELAT_1:103
.= (Comput (ProgramPart t),t,m) | (UsedIntLoc ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m)))) by A19, A17, Th23, RELAT_1:103 ;
then A22: (Exec ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m))),(Comput (ProgramPart s),s,m)) | (UsedInt*Loc ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m)))) = (Exec ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m))),(Comput (ProgramPart t),t,m)) | (UsedInt*Loc ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m)))) by A7, A11, A20, Th72, NAT_1:13;
A23: IC (Exec ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m))),(Comput (ProgramPart s),s,m)) = IC (Exec ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m))),(Comput (ProgramPart t),t,m)) by A7, A11, A21, A20, Th72, NAT_1:13;
hence IC (Comput (ProgramPart t),t,(m + 1)) in dom I by A5, A11, A10, A18, A15; :: thesis: ( IC (Comput (ProgramPart s),s,(m + 1)) = IC (Comput (ProgramPart t),t,(m + 1)) & ( for a being Int-Location st a in UsedIntLoc I holds
(Comput (ProgramPart s),s,(m + 1)) . a = (Comput (ProgramPart t),t,(m + 1)) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Comput (ProgramPart s),s,(m + 1)) . f = (Comput (ProgramPart t),t,(m + 1)) . f ) )
thus IC (Comput (ProgramPart s),s,(m + 1)) = IC (Comput (ProgramPart t),t,(m + 1)) by A7, A11, A10, A18, A9, A14, A23, GRFUNC_1:8, NAT_1:13; :: thesis: ( ( for a being Int-Location st a in UsedIntLoc I holds
(Comput (ProgramPart s),s,(m + 1)) . a = (Comput (ProgramPart t),t,(m + 1)) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Comput (ProgramPart s),s,(m + 1)) . f = (Comput (ProgramPart t),t,(m + 1)) . f ) )
A24: (Exec ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m))),(Comput (ProgramPart s),s,m)) | (UsedIntLoc ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m)))) = (Exec ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m))),(Comput (ProgramPart t),t,m)) | (UsedIntLoc ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m)))) by A7, A11, A21, A20, Th72, NAT_1:13;

hereby :: thesis: for f being FinSeq-Location st f in UsedInt*Loc I holds
(Comput (ProgramPart s),s,(m + 1)) . f = (Comput (ProgramPart t),t,(m + 1)) . f

let a be Int-Location ; :: thesis: ( a in UsedIntLoc I implies (Comput (ProgramPart s),s,(m + 1)) . b₁ = (Comput (ProgramPart t),t,(m + 1)) . b₁ )
assume A25: a in UsedIntLoc I ; :: thesis: (Comput (ProgramPart s),s,(m + 1)) . b₁ = (Comput (ProgramPart t),t,(m + 1)) . b₁

per cases ( a in UsedIntLoc ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m))) or not a in UsedIntLoc ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m))) ) ;

suppose A26: a in UsedIntLoc ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m))) ; :: thesis: (Comput (ProgramPart s),s,(m + 1)) . b₁ = (Comput (ProgramPart t),t,(m + 1)) . b₁

hence (Comput (ProgramPart s),s,(m + 1)) . a = ((Exec ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m))),(Comput (ProgramPart s),s,m)) | (UsedIntLoc ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m))))) . a by A10, FUNCT_1:72
.= (Comput (ProgramPart t),t,(m + 1)) . a by A18, A15, A24, A26, FUNCT_1:72 ;
:: thesis: verum

end;

suppose A27: not a in UsedIntLoc ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m))) ; :: thesis: (Comput (ProgramPart s),s,(m + 1)) . b₁ = (Comput (ProgramPart t),t,(m + 1)) . b₁

hence (Comput (ProgramPart s),s,(m + 1)) . a = (Comput (ProgramPart s),s,m) . a by A10, Th68
.= (Comput (ProgramPart t),t,m) . a by A7, A11, A25, NAT_1:13
.= (Comput (ProgramPart t),t,(m + 1)) . a by A18, A15, A27, Th68 ;
:: thesis: verum

end;

end;

end;

let f be FinSeq-Location ; :: thesis: ( f in UsedInt*Loc I implies (Comput (ProgramPart s),s,(m + 1)) . f = (Comput (ProgramPart t),t,(m + 1)) . f )
assume A28: f in UsedInt*Loc I ; :: thesis: (Comput (ProgramPart s),s,(m + 1)) . f = (Comput (ProgramPart t),t,(m + 1)) . f

per cases ( f in UsedInt*Loc ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m))) or not f in UsedInt*Loc ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m))) ) ;

suppose A29: f in UsedInt*Loc ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m))) ; :: thesis: (Comput (ProgramPart s),s,(m + 1)) . f = (Comput (ProgramPart t),t,(m + 1)) . f

hence (Comput (ProgramPart s),s,(m + 1)) . f = ((Exec ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m))),(Comput (ProgramPart s),s,m)) | (UsedInt*Loc ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m))))) . f by A10, FUNCT_1:72
.= (Comput (ProgramPart t),t,(m + 1)) . f by A18, A15, A22, A29, FUNCT_1:72 ;
:: thesis: verum

end;

suppose A30: not f in UsedInt*Loc ((Comput (ProgramPart s),s,m) . (IC (Comput (ProgramPart s),s,m))) ; :: thesis: (Comput (ProgramPart s),s,(m + 1)) . f = (Comput (ProgramPart t),t,(m + 1)) . f

hence (Comput (ProgramPart s),s,(m + 1)) . f = (Comput (ProgramPart s),s,m) . f by A10, Th70
.= (Comput (ProgramPart t),t,m) . f by A7, A11, A28, NAT_1:13
.= (Comput (ProgramPart t),t,(m + 1)) . f by A18, A15, A30, Th70 ;
:: thesis: verum

end;

end;

end;

end;

A31: S₁[ 0 ]

proof

A32: IC (Comput (ProgramPart t),t,0 ) = IC t by AMI_1:13
.= 0 by A2, Th67 ;
A33: IC (Comput (ProgramPart s),s,0 ) = IC s by AMI_1:13
.= 0 by A1, Th67 ;
assume 0 < n ; :: thesis: ( IC (Comput (ProgramPart t),t,0 ) in dom I & IC (Comput (ProgramPart s),s,0 ) = IC (Comput (ProgramPart t),t,0 ) & ( for a being Int-Location st a in UsedIntLoc I holds
(Comput (ProgramPart s),s,0 ) . a = (Comput (ProgramPart t),t,0 ) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Comput (ProgramPart s),s,0 ) . f = (Comput (ProgramPart t),t,0 ) . f ) )
hence IC (Comput (ProgramPart t),t,0 ) in dom I by A5, A33, A32; :: thesis: ( IC (Comput (ProgramPart s),s,0 ) = IC (Comput (ProgramPart t),t,0 ) & ( for a being Int-Location st a in UsedIntLoc I holds
(Comput (ProgramPart s),s,0 ) . a = (Comput (ProgramPart t),t,0 ) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Comput (ProgramPart s),s,0 ) . f = (Comput (ProgramPart t),t,0 ) . f ) )
thus IC (Comput (ProgramPart s),s,0 ) = IC (Comput (ProgramPart t),t,0 ) by A33, A32; :: thesis: ( ( for a being Int-Location st a in UsedIntLoc I holds
(Comput (ProgramPart s),s,0 ) . a = (Comput (ProgramPart t),t,0 ) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Comput (ProgramPart s),s,0 ) . f = (Comput (ProgramPart t),t,0 ) . f ) )

hereby :: thesis: for f being FinSeq-Location st f in UsedInt*Loc I holds
(Comput (ProgramPart s),s,0 ) . f = (Comput (ProgramPart t),t,0 ) . f

let a be Int-Location ; :: thesis: ( a in UsedIntLoc I implies (Comput (ProgramPart s),s,0 ) . a = (Comput (ProgramPart t),t,0 ) . a )
assume A34: a in UsedIntLoc I ; :: thesis: (Comput (ProgramPart s),s,0 ) . a = (Comput (ProgramPart t),t,0 ) . a
thus (Comput (ProgramPart s),s,0 ) . a = s . a by AMI_1:13
.= (s | (UsedIntLoc I)) . a by A34, FUNCT_1:72
.= t . a by A3, A34, FUNCT_1:72
.= (Comput (ProgramPart t),t,0 ) . a by AMI_1:13 ; :: thesis: verum

end;

let f be FinSeq-Location ; :: thesis: ( f in UsedInt*Loc I implies (Comput (ProgramPart s),s,0 ) . f = (Comput (ProgramPart t),t,0 ) . f )
assume A35: f in UsedInt*Loc I ; :: thesis: (Comput (ProgramPart s),s,0 ) . f = (Comput (ProgramPart t),t,0 ) . f
thus (Comput (ProgramPart s),s,0 ) . f = s . f by AMI_1:13
.= (s | (UsedInt*Loc I)) . f by A35, FUNCT_1:72
.= t . f by A4, A35, FUNCT_1:72
.= (Comput (ProgramPart t),t,0 ) . f by AMI_1:13 ; :: thesis: verum

end;

A36: for m being Element of NAT holds S₁[m] from NAT_1:sch 1(A31, A6);
hence for m being Element of NAT st m < n holds
IC (Comput (ProgramPart t),t,m) in dom I ; :: thesis: for m being Element of NAT st m <= n holds
( IC (Comput (ProgramPart s),s,m) = IC (Comput (ProgramPart t),t,m) & ( for a being Int-Location st a in UsedIntLoc I holds
(Comput (ProgramPart s),s,m) . a = (Comput (ProgramPart t),t,m) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Comput (ProgramPart s),s,m) . f = (Comput (ProgramPart t),t,m) . f ) )
let m be Element of NAT ; :: thesis: ( m <= n implies ( IC (Comput (ProgramPart s),s,m) = IC (Comput (ProgramPart t),t,m) & ( for a being Int-Location st a in UsedIntLoc I holds
(Comput (ProgramPart s),s,m) . a = (Comput (ProgramPart t),t,m) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Comput (ProgramPart s),s,m) . f = (Comput (ProgramPart t),t,m) . f ) ) )
assume A37: m <= n ; :: thesis: ( IC (Comput (ProgramPart s),s,m) = IC (Comput (ProgramPart t),t,m) & ( for a being Int-Location st a in UsedIntLoc I holds
(Comput (ProgramPart s),s,m) . a = (Comput (ProgramPart t),t,m) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Comput (ProgramPart s),s,m) . f = (Comput (ProgramPart t),t,m) . f ) )

per cases ( m = 0 or ex p being Nat st m = p + 1 ) by NAT_1:6;

suppose A38: m = 0 ; :: thesis: ( IC (Comput (ProgramPart s),s,m) = IC (Comput (ProgramPart t),t,m) & ( for a being Int-Location st a in UsedIntLoc I holds
(Comput (ProgramPart s),s,m) . a = (Comput (ProgramPart t),t,m) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Comput (ProgramPart s),s,m) . f = (Comput (ProgramPart t),t,m) . f ) )

A39: IC (Comput (ProgramPart t),t,0 ) = IC t by AMI_1:13
.= 0 by A2, Th67 ;
IC (Comput (ProgramPart s),s,0 ) = IC s by AMI_1:13
.= 0 by A1, Th67 ;
hence IC (Comput (ProgramPart s),s,m) = IC (Comput (ProgramPart t),t,m) by A38, A39; :: thesis: ( ( for a being Int-Location st a in UsedIntLoc I holds
(Comput (ProgramPart s),s,m) . a = (Comput (ProgramPart t),t,m) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Comput (ProgramPart s),s,m) . f = (Comput (ProgramPart t),t,m) . f ) )

hereby :: thesis: for f being FinSeq-Location st f in UsedInt*Loc I holds
(Comput (ProgramPart s),s,m) . f = (Comput (ProgramPart t),t,m) . f

let a be Int-Location ; :: thesis: ( a in UsedIntLoc I implies (Comput (ProgramPart s),s,m) . a = (Comput (ProgramPart t),t,m) . a )
assume A40: a in UsedIntLoc I ; :: thesis: (Comput (ProgramPart s),s,m) . a = (Comput (ProgramPart t),t,m) . a
thus (Comput (ProgramPart s),s,m) . a = s . a by A38, AMI_1:13
.= (s | (UsedIntLoc I)) . a by A40, FUNCT_1:72
.= t . a by A3, A40, FUNCT_1:72
.= (Comput (ProgramPart t),t,m) . a by A38, AMI_1:13 ; :: thesis: verum

end;

let f be FinSeq-Location ; :: thesis: ( f in UsedInt*Loc I implies (Comput (ProgramPart s),s,m) . f = (Comput (ProgramPart t),t,m) . f )
assume A41: f in UsedInt*Loc I ; :: thesis: (Comput (ProgramPart s),s,m) . f = (Comput (ProgramPart t),t,m) . f
thus (Comput (ProgramPart s),s,m) . f = s . f by A38, AMI_1:13
.= (s | (UsedInt*Loc I)) . f by A41, FUNCT_1:72
.= t . f by A4, A41, FUNCT_1:72
.= (Comput (ProgramPart t),t,m) . f by A38, AMI_1:13 ; :: thesis: verum

end;

suppose ex p being Nat st m = p + 1 ; :: thesis: ( IC (Comput (ProgramPart s),s,m) = IC (Comput (ProgramPart t),t,m) & ( for a being Int-Location st a in UsedIntLoc I holds
(Comput (ProgramPart s),s,m) . a = (Comput (ProgramPart t),t,m) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Comput (ProgramPart s),s,m) . f = (Comput (ProgramPart t),t,m) . f ) )

then consider p being Nat such that
A42: m = p + 1 ;
reconsider p = p as Element of NAT by ORDINAL1:def 13;
A43: p < n by A37, A42, NAT_1:13;
then A44: IC (Comput (ProgramPart s),s,p) in dom I by A5;

now

thus dom ((Comput (ProgramPart s),s,p) | (UsedInt*Loc I)) = (dom (Comput (ProgramPart s),s,p)) /\ (UsedInt*Loc I) by RELAT_1:90
.= the carrier of SCM+FSA /\ (UsedInt*Loc I) by PARTFUN1:def 4
.= (dom (Comput (ProgramPart t),t,p)) /\ (UsedInt*Loc I) by PARTFUN1:def 4 ; :: thesis: for x being set st x in dom ((Comput (ProgramPart s),s,p) | (UsedInt*Loc I)) holds
((Comput (ProgramPart s),s,p) | (UsedInt*Loc I)) . x = (Comput (ProgramPart t),t,p) . x
let x be set ; :: thesis: ( x in dom ((Comput (ProgramPart s),s,p) | (UsedInt*Loc I)) implies ((Comput (ProgramPart s),s,p) | (UsedInt*Loc I)) . x = (Comput (ProgramPart t),t,p) . x )
assume x in dom ((Comput (ProgramPart s),s,p) | (UsedInt*Loc I)) ; :: thesis: ((Comput (ProgramPart s),s,p) | (UsedInt*Loc I)) . x = (Comput (ProgramPart t),t,p) . x
then A45: x in UsedInt*Loc I by RELAT_1:86;
then reconsider x9 = x as FinSeq-Location by SCMFSA_2:12;
thus ((Comput (ProgramPart s),s,p) | (UsedInt*Loc I)) . x = (Comput (ProgramPart s),s,p) . x9 by A45, FUNCT_1:72
.= (Comput (ProgramPart t),t,p) . x by A36, A43, A45 ; :: thesis: verum

end;

then A46: (Comput (ProgramPart s),s,p) | (UsedInt*Loc I) = (Comput (ProgramPart t),t,p) | (UsedInt*Loc I) by FUNCT_1:68;
set i = (Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p));
set p1 = p + 1;
Y: (ProgramPart (Comput (ProgramPart s),s,p)) /. (IC (Comput (ProgramPart s),s,p)) = (Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p)) by COMPOS_1:38;
T: ProgramPart s = ProgramPart (Comput (ProgramPart s),s,p) by AMI_1:123;
A47: Comput (ProgramPart s),s,(p + 1) = Following (ProgramPart s),(Comput (ProgramPart s),s,p) by AMI_1:14
.= Exec ((Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p))),(Comput (ProgramPart s),s,p) by Y, T ;

now

thus dom ((Comput (ProgramPart s),s,p) | (UsedIntLoc I)) = (dom (Comput (ProgramPart s),s,p)) /\ (UsedIntLoc I) by RELAT_1:90
.= the carrier of SCM+FSA /\ (UsedIntLoc I) by PARTFUN1:def 4
.= (dom (Comput (ProgramPart t),t,p)) /\ (UsedIntLoc I) by PARTFUN1:def 4 ; :: thesis: for x being set st x in dom ((Comput (ProgramPart s),s,p) | (UsedIntLoc I)) holds
((Comput (ProgramPart s),s,p) | (UsedIntLoc I)) . x = (Comput (ProgramPart t),t,p) . x
let x be set ; :: thesis: ( x in dom ((Comput (ProgramPart s),s,p) | (UsedIntLoc I)) implies ((Comput (ProgramPart s),s,p) | (UsedIntLoc I)) . x = (Comput (ProgramPart t),t,p) . x )
assume x in dom ((Comput (ProgramPart s),s,p) | (UsedIntLoc I)) ; :: thesis: ((Comput (ProgramPart s),s,p) | (UsedIntLoc I)) . x = (Comput (ProgramPart t),t,p) . x
then A48: x in UsedIntLoc I by RELAT_1:86;
then reconsider x9 = x as Int-Location by SCMFSA_2:11;
thus ((Comput (ProgramPart s),s,p) | (UsedIntLoc I)) . x = (Comput (ProgramPart s),s,p) . x9 by A48, FUNCT_1:72
.= (Comput (ProgramPart t),t,p) . x by A36, A43, A48 ; :: thesis: verum

end;

then A49: (Comput (ProgramPart s),s,p) | (UsedIntLoc I) = (Comput (ProgramPart t),t,p) | (UsedIntLoc I) by FUNCT_1:68;
A50: IC (Comput (ProgramPart s),s,p) = IC (Comput (ProgramPart t),t,p) by A36, A43;
dom I misses dom (Start-At 0 ,SCM+FSA ) by Th64;
then A51: I c= I +* (Start-At 0 ,SCM+FSA ) by FUNCT_4:33;
then I c= s by A1, XBOOLE_1:1;
then I c= Comput (ProgramPart s),s,p by AMI_1:81;
then A52: (Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p)) = I . (IC (Comput (ProgramPart s),s,p)) by A44, GRFUNC_1:8;
Y: (ProgramPart (Comput (ProgramPart t),t,p)) /. (IC (Comput (ProgramPart t),t,p)) = (Comput (ProgramPart t),t,p) . (IC (Comput (ProgramPart t),t,p)) by COMPOS_1:38;
T: ProgramPart t = ProgramPart (Comput (ProgramPart t),t,p) by AMI_1:123;
A53: Comput (ProgramPart t),t,(p + 1) = Following (ProgramPart t),(Comput (ProgramPart t),t,p) by AMI_1:14
.= Exec ((Comput (ProgramPart t),t,p) . (IC (Comput (ProgramPart t),t,p))),(Comput (ProgramPart t),t,p) by Y, T ;
I c= t by A2, A51, XBOOLE_1:1;
then I c= Comput (ProgramPart t),t,p by AMI_1:81;
then A54: (Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p)) = (Comput (ProgramPart t),t,p) . (IC (Comput (ProgramPart t),t,p)) by A50, A44, A52, GRFUNC_1:8;
IC (Comput (ProgramPart s),s,p) in dom I by A5, A43;
then A55: (Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p)) in rng I by A52, FUNCT_1:def 5;
then A56: (Comput (ProgramPart s),s,p) | (UsedInt*Loc ((Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p)))) = ((Comput (ProgramPart s),s,p) | (UsedInt*Loc I)) | (UsedInt*Loc ((Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p)))) by Th39, RELAT_1:103
.= (Comput (ProgramPart t),t,p) | (UsedInt*Loc ((Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p)))) by A55, A46, Th39, RELAT_1:103 ;
A57: (Comput (ProgramPart s),s,p) | (UsedIntLoc ((Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p)))) = ((Comput (ProgramPart s),s,p) | (UsedIntLoc I)) | (UsedIntLoc ((Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p)))) by A55, Th23, RELAT_1:103
.= (Comput (ProgramPart t),t,p) | (UsedIntLoc ((Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p)))) by A55, A49, Th23, RELAT_1:103 ;
hence IC (Comput (ProgramPart s),s,m) = IC (Comput (ProgramPart t),t,m) by A42, A47, A53, A50, A54, A56, Th72; :: thesis: ( ( for a being Int-Location st a in UsedIntLoc I holds
(Comput (ProgramPart s),s,m) . a = (Comput (ProgramPart t),t,m) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Comput (ProgramPart s),s,m) . f = (Comput (ProgramPart t),t,m) . f ) )
A58: (Exec ((Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p))),(Comput (ProgramPart s),s,p)) | (UsedIntLoc ((Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p)))) = (Exec ((Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p))),(Comput (ProgramPart t),t,p)) | (UsedIntLoc ((Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p)))) by A50, A57, A56, Th72;

hereby :: thesis: for f being FinSeq-Location st f in UsedInt*Loc I holds
(Comput (ProgramPart s),s,m) . f = (Comput (ProgramPart t),t,m) . f

let a be Int-Location ; :: thesis: ( a in UsedIntLoc I implies (Comput (ProgramPart s),s,m) . b₁ = (Comput (ProgramPart t),t,m) . b₁ )
assume A59: a in UsedIntLoc I ; :: thesis: (Comput (ProgramPart s),s,m) . b₁ = (Comput (ProgramPart t),t,m) . b₁

per cases ( a in UsedIntLoc ((Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p))) or not a in UsedIntLoc ((Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p))) ) ;

suppose A60: a in UsedIntLoc ((Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p))) ; :: thesis: (Comput (ProgramPart s),s,m) . b₁ = (Comput (ProgramPart t),t,m) . b₁

hence (Comput (ProgramPart s),s,m) . a = ((Exec ((Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p))),(Comput (ProgramPart s),s,p)) | (UsedIntLoc ((Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p))))) . a by A42, A47, FUNCT_1:72
.= (Comput (ProgramPart t),t,m) . a by A42, A53, A54, A58, A60, FUNCT_1:72 ;
:: thesis: verum

end;

suppose A61: not a in UsedIntLoc ((Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p))) ; :: thesis: (Comput (ProgramPart s),s,m) . b₁ = (Comput (ProgramPart t),t,m) . b₁

hence (Comput (ProgramPart s),s,m) . a = (Comput (ProgramPart s),s,p) . a by A42, A47, Th68
.= (Comput (ProgramPart t),t,p) . a by A36, A43, A59
.= (Comput (ProgramPart t),t,m) . a by A42, A53, A54, A61, Th68 ;
:: thesis: verum

end;

end;

end;

A62: (Exec ((Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p))),(Comput (ProgramPart s),s,p)) | (UsedInt*Loc ((Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p)))) = (Exec ((Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p))),(Comput (ProgramPart t),t,p)) | (UsedInt*Loc ((Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p)))) by A50, A57, A56, Th72;

hereby :: thesis: verum

let f be FinSeq-Location ; :: thesis: ( f in UsedInt*Loc I implies (Comput (ProgramPart s),s,m) . b₁ = (Comput (ProgramPart t),t,m) . b₁ )
assume A63: f in UsedInt*Loc I ; :: thesis: (Comput (ProgramPart s),s,m) . b₁ = (Comput (ProgramPart t),t,m) . b₁

per cases ( f in UsedInt*Loc ((Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p))) or not f in UsedInt*Loc ((Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p))) ) ;

suppose A64: f in UsedInt*Loc ((Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p))) ; :: thesis: (Comput (ProgramPart s),s,m) . b₁ = (Comput (ProgramPart t),t,m) . b₁

hence (Comput (ProgramPart s),s,m) . f = ((Exec ((Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p))),(Comput (ProgramPart s),s,p)) | (UsedInt*Loc ((Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p))))) . f by A42, A47, FUNCT_1:72
.= (Comput (ProgramPart t),t,m) . f by A42, A53, A54, A62, A64, FUNCT_1:72 ;
:: thesis: verum

end;

suppose A65: not f in UsedInt*Loc ((Comput (ProgramPart s),s,p) . (IC (Comput (ProgramPart s),s,p))) ; :: thesis: (Comput (ProgramPart s),s,m) . b₁ = (Comput (ProgramPart t),t,m) . b₁

hence (Comput (ProgramPart s),s,m) . f = (Comput (ProgramPart s),s,p) . f by A42, A47, Th70
.= (Comput (ProgramPart t),t,p) . f by A36, A43, A63
.= (Comput (ProgramPart t),t,m) . f by A42, A53, A54, A65, Th70 ;
:: thesis: verum

end;

end;

end;

end;

end;