let I be Program of {INT,(INT *)}; :: 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 COMPOS_1:140;
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 EXTPRO_1:4
.= 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 EXTPRO_1:4
.= 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 EXTPRO_1:3
.= 0 by A2, COMPOS_1:143 ;
A33: IC (Comput ((ProgramPart s),s,0)) = IC s by EXTPRO_1:3
.= 0 by A1, COMPOS_1:143 ;
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 EXTPRO_1:3
.= (s | (UsedIntLoc I)) . a by A34, FUNCT_1:72
.= t . a by A3, A34, FUNCT_1:72
.= (Comput ((ProgramPart t),t,0)) . a by EXTPRO_1:3 ; :: 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 EXTPRO_1:3
.= (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 EXTPRO_1:3 ; :: 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 EXTPRO_1:3
.= 0 by A2, COMPOS_1:143 ;
IC (Comput ((ProgramPart s),s,0)) = IC s by EXTPRO_1:3
.= 0 by A1, COMPOS_1:143 ;
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, EXTPRO_1:3
.= (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, EXTPRO_1:3 ; :: 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, EXTPRO_1:3
.= (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, EXTPRO_1:3 ; :: 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 EXTPRO_1:4
.= 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 COMPOS_1:140;
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 EXTPRO_1:4
.= 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;