let I be Program of ; :: thesis: for n being Nat
for s, t being State of SCM+FSA
for P, Q being Instruction-Sequence of SCM+FSA st I c= P & I c= Q & Start-At (0,SCM+FSA) c= s & Start-At (0,SCM+FSA) c= t & s | () = t | () & s | () = t | () & ( for m being Nat st m < n holds
IC (Comput (P,s,m)) in dom I ) holds
( ( for m being Nat st m < n holds
IC (Comput (Q,t,m)) in dom I ) & ( for m being Nat st m <= n holds
( IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) & ( for a being Int-Location st a in UsedILoc I holds
(Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedI*Loc I holds
(Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) ) ) )

let n be Nat; :: thesis: for s, t being State of SCM+FSA
for P, Q being Instruction-Sequence of SCM+FSA st I c= P & I c= Q & Start-At (0,SCM+FSA) c= s & Start-At (0,SCM+FSA) c= t & s | () = t | () & s | () = t | () & ( for m being Nat st m < n holds
IC (Comput (P,s,m)) in dom I ) holds
( ( for m being Nat st m < n holds
IC (Comput (Q,t,m)) in dom I ) & ( for m being Nat st m <= n holds
( IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) & ( for a being Int-Location st a in UsedILoc I holds
(Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedI*Loc I holds
(Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) ) ) )

let s, t be State of SCM+FSA; :: thesis: for P, Q being Instruction-Sequence of SCM+FSA st I c= P & I c= Q & Start-At (0,SCM+FSA) c= s & Start-At (0,SCM+FSA) c= t & s | () = t | () & s | () = t | () & ( for m being Nat st m < n holds
IC (Comput (P,s,m)) in dom I ) holds
( ( for m being Nat st m < n holds
IC (Comput (Q,t,m)) in dom I ) & ( for m being Nat st m <= n holds
( IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) & ( for a being Int-Location st a in UsedILoc I holds
(Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedI*Loc I holds
(Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) ) ) )

let P, Q be Instruction-Sequence of SCM+FSA; :: thesis: ( I c= P & I c= Q & Start-At (0,SCM+FSA) c= s & Start-At (0,SCM+FSA) c= t & s | () = t | () & s | () = t | () & ( for m being Nat st m < n holds
IC (Comput (P,s,m)) in dom I ) implies ( ( for m being Nat st m < n holds
IC (Comput (Q,t,m)) in dom I ) & ( for m being Nat st m <= n holds
( IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) & ( for a being Int-Location st a in UsedILoc I holds
(Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedI*Loc I holds
(Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) ) ) ) )

assume A1: ( I c= P & I c= Q ) ; :: thesis: ( not Start-At (0,SCM+FSA) c= s or not Start-At (0,SCM+FSA) c= t or not s | () = t | () or not s | () = t | () or ex m being Nat st
( m < n & not IC (Comput (P,s,m)) in dom I ) or ( ( for m being Nat st m < n holds
IC (Comput (Q,t,m)) in dom I ) & ( for m being Nat st m <= n holds
( IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) & ( for a being Int-Location st a in UsedILoc I holds
(Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedI*Loc I holds
(Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) ) ) ) )

assume that
A2: Start-At (0,SCM+FSA) c= s and
A3: Start-At (0,SCM+FSA) c= t and
A4: s | () = t | () and
A5: s | () = t | () and
A6: for m being Nat st m < n holds
IC (Comput (P,s,m)) in dom I ; :: thesis: ( ( for m being Nat st m < n holds
IC (Comput (Q,t,m)) in dom I ) & ( for m being Nat st m <= n holds
( IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) & ( for a being Int-Location st a in UsedILoc I holds
(Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedI*Loc I holds
(Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) ) ) )

defpred S1[ 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: for m being Nat st S1[m] holds
S1[m + 1]
let m be Nat; :: thesis: ( S1[m] implies S1[m + 1] )
assume A8: S1[m] ; :: thesis: S1[m + 1]
thus S1[m + 1] :: thesis: verum
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: ( IC (Comput (Q,t,(m + 1))) in dom I & IC (Comput (P,s,(m + 1))) = IC (Comput (Q,t,(m + 1))) & ( for a being Int-Location st a in UsedILoc I holds
(Comput (P,s,(m + 1))) . a = (Comput (Q,t,(m + 1))) . a ) & ( for f being FinSeq-Location st f in UsedI*Loc I holds
(Comput (P,s,(m + 1))) . f = (Comput (Q,t,(m + 1))) . f ) )

now :: thesis: ( dom ((Comput (P,s,m)) | ()) = (dom (Comput (Q,t,m))) /\ () & ( for x being object st x in dom ((Comput (P,s,m)) | ()) holds
((Comput (P,s,m)) | ()) . x = (Comput (Q,t,m)) . x ) )
thus dom ((Comput (P,s,m)) | ()) = (dom (Comput (P,s,m))) /\ () by RELAT_1:61
.= the carrier of SCM+FSA /\ () by PARTFUN1:def 2
.= (dom (Comput (Q,t,m))) /\ () by PARTFUN1:def 2 ; :: thesis: for x being object st x in dom ((Comput (P,s,m)) | ()) holds
((Comput (P,s,m)) | ()) . x = (Comput (Q,t,m)) . x

let x be object ; :: thesis: ( x in dom ((Comput (P,s,m)) | ()) implies ((Comput (P,s,m)) | ()) . x = (Comput (Q,t,m)) . x )
assume x in dom ((Comput (P,s,m)) | ()) ; :: thesis: ((Comput (P,s,m)) | ()) . x = (Comput (Q,t,m)) . x
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)) | ()) . x = (Comput (P,s,m)) . x9 by
.= (Comput (Q,t,m)) . x by ; :: thesis: verum
end;
then A13: (Comput (P,s,m)) | () = (Comput (Q,t,m)) | () by FUNCT_1:46;
A14: P . (IC (Comput (P,s,m))) = I . (IC (Comput (P,s,m))) by ;
then A15: P . (IC (Comput (P,s,m))) = Q . (IC (Comput (Q,t,m))) by ;
now :: thesis: ( dom ((Comput (P,s,m)) | ()) = (dom (Comput (Q,t,m))) /\ () & ( for x being object st x in dom ((Comput (P,s,m)) | ()) holds
((Comput (P,s,m)) | ()) . x = (Comput (Q,t,m)) . x ) )
thus dom ((Comput (P,s,m)) | ()) = (dom (Comput (P,s,m))) /\ () by RELAT_1:61
.= the carrier of SCM+FSA /\ () by PARTFUN1:def 2
.= (dom (Comput (Q,t,m))) /\ () by PARTFUN1:def 2 ; :: thesis: for x being object st x in dom ((Comput (P,s,m)) | ()) holds
((Comput (P,s,m)) | ()) . x = (Comput (Q,t,m)) . x

let x be object ; :: thesis: ( x in dom ((Comput (P,s,m)) | ()) implies ((Comput (P,s,m)) | ()) . x = (Comput (Q,t,m)) . x )
assume x in dom ((Comput (P,s,m)) | ()) ; :: thesis: ((Comput (P,s,m)) | ()) . x = (Comput (Q,t,m)) . x
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)) | ()) . x = (Comput (P,s,m)) . x9 by
.= (Comput (Q,t,m)) . x by ; :: thesis: verum
end;
then A17: (Comput (P,s,m)) | () = (Comput (Q,t,m)) | () 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 ;
then IC (Comput (P,s,m)) in dom I by A6;
then A20: P . (IC (Comput (P,s,m))) in rng I by ;
then A21: (Comput (P,s,m)) | (UsedInt*Loc (P . (IC (Comput (P,s,m))))) = ((Comput (P,s,m)) | ()) | (UsedInt*Loc (P . (IC (Comput (P,s,m))))) by
.= (Comput (Q,t,m)) | (UsedInt*Loc (P . (IC (Comput (P,s,m))))) by ;
A22: (Comput (P,s,m)) | (UsedIntLoc (P . (IC (Comput (P,s,m))))) = ((Comput (P,s,m)) | ()) | (UsedIntLoc (P . (IC (Comput (P,s,m))))) by
.= (Comput (Q,t,m)) | (UsedIntLoc (P . (IC (Comput (P,s,m))))) by ;
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 ;
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 ;
hence IC (Comput (Q,t,(m + 1))) in dom I by A6, A11, A10, A19, A15; :: thesis: ( IC (Comput (P,s,(m + 1))) = IC (Comput (Q,t,(m + 1))) & ( for a being Int-Location st a in UsedILoc I holds
(Comput (P,s,(m + 1))) . a = (Comput (Q,t,(m + 1))) . a ) & ( for f being FinSeq-Location st f in UsedI*Loc I holds
(Comput (P,s,(m + 1))) . f = (Comput (Q,t,(m + 1))) . f ) )

thus IC (Comput (P,s,(m + 1))) = IC (Comput (Q,t,(m + 1))) by ; :: thesis: ( ( for a being Int-Location st a in UsedILoc I holds
(Comput (P,s,(m + 1))) . a = (Comput (Q,t,(m + 1))) . a ) & ( for f being FinSeq-Location st f in UsedI*Loc I holds
(Comput (P,s,(m + 1))) . f = (Comput (Q,t,(m + 1))) . f ) )

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 ;
hereby :: thesis: for f being FinSeq-Location st f in UsedI*Loc I holds
(Comput (P,s,(m + 1))) . f = (Comput (Q,t,(m + 1))) . f
let a be Int-Location; :: thesis: ( a in UsedILoc I implies (Comput (P,s,(m + 1))) . b1 = (Comput (Q,t,(m + 1))) . b1 )
assume A26: a in UsedILoc I ; :: thesis: (Comput (P,s,(m + 1))) . b1 = (Comput (Q,t,(m + 1))) . b1
per cases ( a in UsedIntLoc (P . (IC (Comput (P,s,m)))) or not a in UsedIntLoc (P . (IC (Comput (P,s,m)))) ) ;
suppose A27: a in UsedIntLoc (P . (IC (Comput (P,s,m)))) ; :: thesis: (Comput (P,s,(m + 1))) . b1 = (Comput (Q,t,(m + 1))) . b1
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
.= (Comput (Q,t,(m + 1))) . a by ;
:: thesis: verum
end;
suppose A28: not a in UsedIntLoc (P . (IC (Comput (P,s,m)))) ; :: thesis: (Comput (P,s,(m + 1))) . b1 = (Comput (Q,t,(m + 1))) . b1
hence (Comput (P,s,(m + 1))) . a = (Comput (P,s,m)) . a by
.= (Comput (Q,t,m)) . a by
.= (Comput (Q,t,(m + 1))) . a by ;
:: thesis: verum
end;
end;
end;
let f be FinSeq-Location ; :: thesis: ( f in UsedI*Loc I implies (Comput (P,s,(m + 1))) . f = (Comput (Q,t,(m + 1))) . f )
assume A29: f in UsedI*Loc I ; :: thesis: (Comput (P,s,(m + 1))) . f = (Comput (Q,t,(m + 1))) . f
per cases ( f in UsedInt*Loc (P . (IC (Comput (P,s,m)))) or not f in UsedInt*Loc (P . (IC (Comput (P,s,m)))) ) ;
suppose A30: f in UsedInt*Loc (P . (IC (Comput (P,s,m)))) ; :: thesis: (Comput (P,s,(m + 1))) . f = (Comput (Q,t,(m + 1))) . f
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
.= (Comput (Q,t,(m + 1))) . f by ;
:: thesis: verum
end;
suppose A31: not f in UsedInt*Loc (P . (IC (Comput (P,s,m)))) ; :: thesis: (Comput (P,s,(m + 1))) . f = (Comput (Q,t,(m + 1))) . f
hence (Comput (P,s,(m + 1))) . f = (Comput (P,s,m)) . f by
.= (Comput (Q,t,m)) . f by
.= (Comput (Q,t,(m + 1))) . f by ;
:: thesis: verum
end;
end;
end;
end;
A32: S1[ 0 ]
proof
A33: IC (Comput (Q,t,0)) = IC t
.= 0 by ;
A34: IC (Comput (P,s,0)) = IC s
.= 0 by ;
assume 0 < n ; :: thesis: ( IC (Comput (Q,t,0)) in dom I & IC (Comput (P,s,0)) = IC (Comput (Q,t,0)) & ( for a being Int-Location st a in UsedILoc I holds
(Comput (P,s,0)) . a = (Comput (Q,t,0)) . a ) & ( for f being FinSeq-Location st f in UsedI*Loc I holds
(Comput (P,s,0)) . f = (Comput (Q,t,0)) . f ) )

hence IC (Comput (Q,t,0)) in dom I by A6, A34, A33; :: thesis: ( IC (Comput (P,s,0)) = IC (Comput (Q,t,0)) & ( for a being Int-Location st a in UsedILoc I holds
(Comput (P,s,0)) . a = (Comput (Q,t,0)) . a ) & ( for f being FinSeq-Location st f in UsedI*Loc I holds
(Comput (P,s,0)) . f = (Comput (Q,t,0)) . f ) )

thus IC (Comput (P,s,0)) = IC (Comput (Q,t,0)) by ; :: thesis: ( ( for a being Int-Location st a in UsedILoc I holds
(Comput (P,s,0)) . a = (Comput (Q,t,0)) . a ) & ( for f being FinSeq-Location st f in UsedI*Loc I holds
(Comput (P,s,0)) . f = (Comput (Q,t,0)) . f ) )

hereby :: thesis: for f being FinSeq-Location st f in UsedI*Loc I holds
(Comput (P,s,0)) . f = (Comput (Q,t,0)) . f
let a be Int-Location; :: thesis: ( a in UsedILoc I implies (Comput (P,s,0)) . a = (Comput (Q,t,0)) . a )
assume A35: a in UsedILoc I ; :: thesis: (Comput (P,s,0)) . a = (Comput (Q,t,0)) . a
thus (Comput (P,s,0)) . a = s . a
.= (s | ()) . a by
.= t . a by
.= (Comput (Q,t,0)) . a ; :: thesis: verum
end;
let f be FinSeq-Location ; :: thesis: ( f in UsedI*Loc I implies (Comput (P,s,0)) . f = (Comput (Q,t,0)) . f )
assume A36: f in UsedI*Loc I ; :: thesis: (Comput (P,s,0)) . f = (Comput (Q,t,0)) . f
thus (Comput (P,s,0)) . f = s . f
.= (s | ()) . f by
.= t . f by
.= (Comput (Q,t,0)) . f ; :: thesis: verum
end;
A37: for m being Nat holds S1[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: for m being Nat st m <= n holds
( IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) & ( for a being Int-Location st a in UsedILoc I holds
(Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedI*Loc I holds
(Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) )

let m be Nat; :: thesis: ( m <= n implies ( IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) & ( for a being Int-Location st a in UsedILoc I holds
(Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedI*Loc I holds
(Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) ) )

assume A38: m <= n ; :: thesis: ( IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) & ( for a being Int-Location st a in UsedILoc I holds
(Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedI*Loc I holds
(Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) )

per cases ( m = 0 or ex p being Nat st m = p + 1 ) by NAT_1:6;
suppose A39: m = 0 ; :: thesis: ( IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) & ( for a being Int-Location st a in UsedILoc I holds
(Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedI*Loc I holds
(Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) )

A40: IC (Comput (Q,t,0)) = IC t
.= 0 by ;
IC (Comput (P,s,0)) = IC s
.= 0 by ;
hence IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) by ; :: thesis: ( ( for a being Int-Location st a in UsedILoc I holds
(Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedI*Loc I holds
(Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) )

hereby :: thesis: for f being FinSeq-Location st f in UsedI*Loc I holds
(Comput (P,s,m)) . f = (Comput (Q,t,m)) . f
let a be Int-Location; :: thesis: ( a in UsedILoc I implies (Comput (P,s,m)) . a = (Comput (Q,t,m)) . a )
assume A41: a in UsedILoc I ; :: thesis: (Comput (P,s,m)) . a = (Comput (Q,t,m)) . a
thus (Comput (P,s,m)) . a = s . a by A39
.= (s | ()) . a by
.= t . a by
.= (Comput (Q,t,m)) . a by A39 ; :: thesis: verum
end;
let f be FinSeq-Location ; :: thesis: ( f in UsedI*Loc I implies (Comput (P,s,m)) . f = (Comput (Q,t,m)) . f )
assume A42: f in UsedI*Loc I ; :: thesis: (Comput (P,s,m)) . f = (Comput (Q,t,m)) . f
thus (Comput (P,s,m)) . f = s . f by A39
.= (s | ()) . f by
.= t . f by
.= (Comput (Q,t,m)) . f by A39 ; :: thesis: verum
end;
suppose ex p being Nat st m = p + 1 ; :: thesis: ( IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) & ( for a being Int-Location st a in UsedILoc I holds
(Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedI*Loc I holds
(Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) )

then consider p being Nat such that
A43: m = p + 1 ;
reconsider p = p as Nat ;
A44: p < n by ;
then A45: IC (Comput (P,s,p)) in dom I by A6;
now :: thesis: ( dom ((Comput (P,s,p)) | ()) = (dom (Comput (Q,t,p))) /\ () & ( for x being object st x in dom ((Comput (P,s,p)) | ()) holds
((Comput (P,s,p)) | ()) . x = (Comput (Q,t,p)) . x ) )
thus dom ((Comput (P,s,p)) | ()) = (dom (Comput (P,s,p))) /\ () by RELAT_1:61
.= the carrier of SCM+FSA /\ () by PARTFUN1:def 2
.= (dom (Comput (Q,t,p))) /\ () by PARTFUN1:def 2 ; :: thesis: for x being object st x in dom ((Comput (P,s,p)) | ()) holds
((Comput (P,s,p)) | ()) . x = (Comput (Q,t,p)) . x

let x be object ; :: thesis: ( x in dom ((Comput (P,s,p)) | ()) implies ((Comput (P,s,p)) | ()) . x = (Comput (Q,t,p)) . x )
assume x in dom ((Comput (P,s,p)) | ()) ; :: thesis: ((Comput (P,s,p)) | ()) . x = (Comput (Q,t,p)) . x
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)) | ()) . x = (Comput (P,s,p)) . x9 by
.= (Comput (Q,t,p)) . x by ; :: thesis: verum
end;
then A47: (Comput (P,s,p)) | () = (Comput (Q,t,p)) | () 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: ( dom ((Comput (P,s,p)) | ()) = (dom (Comput (Q,t,p))) /\ () & ( for x being object st x in dom ((Comput (P,s,p)) | ()) holds
((Comput (P,s,p)) | ()) . x = (Comput (Q,t,p)) . x ) )
thus dom ((Comput (P,s,p)) | ()) = (dom (Comput (P,s,p))) /\ () by RELAT_1:61
.= the carrier of SCM+FSA /\ () by PARTFUN1:def 2
.= (dom (Comput (Q,t,p))) /\ () by PARTFUN1:def 2 ; :: thesis: for x being object st x in dom ((Comput (P,s,p)) | ()) holds
((Comput (P,s,p)) | ()) . x = (Comput (Q,t,p)) . x

let x be object ; :: thesis: ( x in dom ((Comput (P,s,p)) | ()) implies ((Comput (P,s,p)) | ()) . x = (Comput (Q,t,p)) . x )
assume x in dom ((Comput (P,s,p)) | ()) ; :: thesis: ((Comput (P,s,p)) | ()) . x = (Comput (Q,t,p)) . x
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)) | ()) . x = (Comput (P,s,p)) . x9 by
.= (Comput (Q,t,p)) . x by ; :: thesis: verum
end;
then A51: (Comput (P,s,p)) | () = (Comput (Q,t,p)) | () by FUNCT_1:46;
A52: IC (Comput (P,s,p)) = IC (Comput (Q,t,p)) by ;
A53: P . (IC (Comput (P,s,p))) = I . (IC (Comput (P,s,p))) by ;
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 ;
IC (Comput (P,s,p)) in dom I by ;
then A57: P . (IC (Comput (P,s,p))) in rng I by ;
then A58: (Comput (P,s,p)) | (UsedInt*Loc (P . (IC (Comput (P,s,p))))) = ((Comput (P,s,p)) | ()) | (UsedInt*Loc (P . (IC (Comput (P,s,p))))) by
.= (Comput (Q,t,p)) | (UsedInt*Loc (P . (IC (Comput (P,s,p))))) by ;
A59: (Comput (P,s,p)) | (UsedIntLoc (P . (IC (Comput (P,s,p))))) = ((Comput (P,s,p)) | ()) | (UsedIntLoc (P . (IC (Comput (P,s,p))))) by
.= (Comput (Q,t,p)) | (UsedIntLoc (P . (IC (Comput (P,s,p))))) by ;
hence IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) by A43, A49, A55, A52, A56, A58, Th64; :: thesis: ( ( for a being Int-Location st a in UsedILoc I holds
(Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedI*Loc I holds
(Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) )

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 ;
hereby :: thesis: for f being FinSeq-Location st f in UsedI*Loc I holds
(Comput (P,s,m)) . f = (Comput (Q,t,m)) . f
let a be Int-Location; :: thesis: ( a in UsedILoc I implies (Comput (P,s,m)) . b1 = (Comput (Q,t,m)) . b1 )
assume A61: a in UsedILoc I ; :: thesis: (Comput (P,s,m)) . b1 = (Comput (Q,t,m)) . b1
per cases ( a in UsedIntLoc (P . (IC (Comput (P,s,p)))) or not a in UsedIntLoc (P . (IC (Comput (P,s,p)))) ) ;
suppose A62: a in UsedIntLoc (P . (IC (Comput (P,s,p)))) ; :: thesis: (Comput (P,s,m)) . b1 = (Comput (Q,t,m)) . b1
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
.= (Comput (Q,t,m)) . a by ;
:: thesis: verum
end;
suppose A63: not a in UsedIntLoc (P . (IC (Comput (P,s,p)))) ; :: thesis: (Comput (P,s,m)) . b1 = (Comput (Q,t,m)) . b1
hence (Comput (P,s,m)) . a = (Comput (P,s,p)) . a by
.= (Comput (Q,t,p)) . a by
.= (Comput (Q,t,m)) . a by A43, A55, A56, A63, Th60 ;
:: thesis: verum
end;
end;
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 ;
hereby :: thesis: verum
let f be FinSeq-Location ; :: thesis: ( f in UsedI*Loc I implies (Comput (P,s,m)) . b1 = (Comput (Q,t,m)) . b1 )
assume A65: f in UsedI*Loc I ; :: thesis: (Comput (P,s,m)) . b1 = (Comput (Q,t,m)) . b1
per cases ( f in UsedInt*Loc (P . (IC (Comput (P,s,p)))) or not f in UsedInt*Loc (P . (IC (Comput (P,s,p)))) ) ;
suppose A66: f in UsedInt*Loc (P . (IC (Comput (P,s,p)))) ; :: thesis: (Comput (P,s,m)) . b1 = (Comput (Q,t,m)) . b1
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
.= (Comput (Q,t,m)) . f by ;
:: thesis: verum
end;
suppose A67: not f in UsedInt*Loc (P . (IC (Comput (P,s,p)))) ; :: thesis: (Comput (P,s,m)) . b1 = (Comput (Q,t,m)) . b1
hence (Comput (P,s,m)) . f = (Comput (P,s,p)) . f by
.= (Comput (Q,t,p)) . f by
.= (Comput (Q,t,m)) . f by A43, A55, A56, A67, Th62 ;
:: thesis: verum
end;
end;
end;
end;
end;