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 | (UsedILoc I) = t | (UsedILoc I) & s | (UsedI*Loc I) = t | (UsedI*Loc I) & ( 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 | (UsedILoc I) = t | (UsedILoc I) & s | (UsedI*Loc I) = t | (UsedI*Loc I) & ( 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 | (UsedILoc I) = t | (UsedILoc I) & s | (UsedI*Loc I) = t | (UsedI*Loc I) & ( 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 | (UsedILoc I) = t | (UsedILoc I) & s | (UsedI*Loc I) = t | (UsedI*Loc I) & ( 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 | (UsedILoc I) = t | (UsedILoc I) or not s | (UsedI*Loc I) = t | (UsedI*Loc I) 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 | (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: ( ( 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 S_{1}[ 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 ) ) );

_{1}[ 0 ]
_{1}[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 ) )

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 | (UsedILoc I) = t | (UsedILoc I) & s | (UsedI*Loc I) = t | (UsedI*Loc I) & ( 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 | (UsedILoc I) = t | (UsedILoc I) & s | (UsedI*Loc I) = t | (UsedI*Loc I) & ( 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 | (UsedILoc I) = t | (UsedILoc I) & s | (UsedI*Loc I) = t | (UsedI*Loc I) & ( 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 | (UsedILoc I) = t | (UsedILoc I) & s | (UsedI*Loc I) = t | (UsedI*Loc I) & ( 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 | (UsedILoc I) = t | (UsedILoc I) or not s | (UsedI*Loc I) = t | (UsedI*Loc I) 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 | (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: ( ( 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 S

(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 S_{1}[m] holds

S_{1}[m + 1]

A32:
SS

let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[m + 1] )

assume A8: S_{1}[m]
; :: thesis: S_{1}[m + 1]

thus S_{1}[m + 1]
:: thesis: verum

end;assume A8: S

thus S

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 ) )

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;

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: ( 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 A8, A11, A10, A19, A14, A24, A1, GRFUNC_1:2, NAT_1:13; :: 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 A8, A11, A22, A21, Th64, NAT_1:13;

assume A29: f in UsedI*Loc I ; :: thesis: (Comput (P,s,(m + 1))) . f = (Comput (Q,t,(m + 1))) . f

end;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)) | (UsedI*Loc I)) = (dom (Comput (Q,t,m))) /\ (UsedI*Loc I) & ( for x being object st x in dom ((Comput (P,s,m)) | (UsedI*Loc I)) holds

((Comput (P,s,m)) | (UsedI*Loc I)) . x = (Comput (Q,t,m)) . x ) )

then A13:
(Comput (P,s,m)) | (UsedI*Loc I) = (Comput (Q,t,m)) | (UsedI*Loc I)
by FUNCT_1:46;((Comput (P,s,m)) | (UsedI*Loc I)) . x = (Comput (Q,t,m)) . x ) )

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: for x being object st x in dom ((Comput (P,s,m)) | (UsedI*Loc I)) holds

((Comput (P,s,m)) | (UsedI*Loc I)) . x = (Comput (Q,t,m)) . x

let x be object ; :: thesis: ( x in dom ((Comput (P,s,m)) | (UsedI*Loc I)) implies ((Comput (P,s,m)) | (UsedI*Loc I)) . x = (Comput (Q,t,m)) . x )

assume x in dom ((Comput (P,s,m)) | (UsedI*Loc I)) ; :: thesis: ((Comput (P,s,m)) | (UsedI*Loc I)) . 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)) | (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: verum

end;.= 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: for x being object st x in dom ((Comput (P,s,m)) | (UsedI*Loc I)) holds

((Comput (P,s,m)) | (UsedI*Loc I)) . x = (Comput (Q,t,m)) . x

let x be object ; :: thesis: ( x in dom ((Comput (P,s,m)) | (UsedI*Loc I)) implies ((Comput (P,s,m)) | (UsedI*Loc I)) . x = (Comput (Q,t,m)) . x )

assume x in dom ((Comput (P,s,m)) | (UsedI*Loc I)) ; :: thesis: ((Comput (P,s,m)) | (UsedI*Loc I)) . 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)) | (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: verum

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: ( dom ((Comput (P,s,m)) | (UsedILoc I)) = (dom (Comput (Q,t,m))) /\ (UsedILoc I) & ( for x being object st x in dom ((Comput (P,s,m)) | (UsedILoc I)) holds

((Comput (P,s,m)) | (UsedILoc I)) . x = (Comput (Q,t,m)) . x ) )

then A17:
(Comput (P,s,m)) | (UsedILoc I) = (Comput (Q,t,m)) | (UsedILoc I)
by FUNCT_1:46;((Comput (P,s,m)) | (UsedILoc I)) . x = (Comput (Q,t,m)) . x ) )

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: for x being object st x in dom ((Comput (P,s,m)) | (UsedILoc I)) holds

((Comput (P,s,m)) | (UsedILoc I)) . x = (Comput (Q,t,m)) . x

let x be object ; :: thesis: ( x in dom ((Comput (P,s,m)) | (UsedILoc I)) implies ((Comput (P,s,m)) | (UsedILoc I)) . x = (Comput (Q,t,m)) . x )

assume x in dom ((Comput (P,s,m)) | (UsedILoc I)) ; :: thesis: ((Comput (P,s,m)) | (UsedILoc I)) . 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)) | (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: verum

end;.= the carrier of SCM+FSA /\ (UsedILoc I) by PARTFUN1:def 2

.= (dom (Comput (Q,t,m))) /\ (UsedILoc I) by PARTFUN1:def 2 ; :: thesis: for x being object st x in dom ((Comput (P,s,m)) | (UsedILoc I)) holds

((Comput (P,s,m)) | (UsedILoc I)) . x = (Comput (Q,t,m)) . x

let x be object ; :: thesis: ( x in dom ((Comput (P,s,m)) | (UsedILoc I)) implies ((Comput (P,s,m)) | (UsedILoc I)) . x = (Comput (Q,t,m)) . x )

assume x in dom ((Comput (P,s,m)) | (UsedILoc I)) ; :: thesis: ((Comput (P,s,m)) | (UsedILoc I)) . 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)) | (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: verum

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: ( 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 A8, A11, A10, A19, A14, A24, A1, GRFUNC_1:2, NAT_1:13; :: 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 A8, A11, A22, A21, Th64, NAT_1:13;

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 f be FinSeq-Location ; :: thesis: ( f in UsedI*Loc I implies (Comput (P,s,(m + 1))) . f = (Comput (Q,t,(m + 1))) . f )(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))) . b_{1} = (Comput (Q,t,(m + 1))) . b_{1} )

assume A26: a in UsedILoc I ; :: thesis: (Comput (P,s,(m + 1))) . b_{1} = (Comput (Q,t,(m + 1))) . b_{1}

end;assume A26: a in UsedILoc I ; :: thesis: (Comput (P,s,(m + 1))) . b

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

end;

suppose A27:
a in UsedIntLoc (P . (IC (Comput (P,s,m))))
; :: thesis: (Comput (P,s,(m + 1))) . b_{1} = (Comput (Q,t,(m + 1))) . b_{1}

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: verum

end;.= (Comput (Q,t,(m + 1))) . a by A19, A15, A25, A27, FUNCT_1:49 ;

:: thesis: verum

suppose A28:
not a in UsedIntLoc (P . (IC (Comput (P,s,m))))
; :: thesis: (Comput (P,s,(m + 1))) . b_{1} = (Comput (Q,t,(m + 1))) . b_{1}

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: verum

end;.= (Comput (Q,t,m)) . a by A8, A11, A26, NAT_1:13

.= (Comput (Q,t,(m + 1))) . a by A19, A15, A28, Th60 ;

:: thesis: verum

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)))) )
;

end;

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 A10, FUNCT_1:49

.= (Comput (Q,t,(m + 1))) . f by A19, A15, A23, A30, FUNCT_1:49 ;

:: thesis: verum

end;.= (Comput (Q,t,(m + 1))) . f by A19, A15, A23, A30, FUNCT_1:49 ;

:: thesis: verum

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 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: verum

end;.= (Comput (Q,t,m)) . f by A8, A11, A29, NAT_1:13

.= (Comput (Q,t,(m + 1))) . f by A19, A15, A31, Th62 ;

:: thesis: verum

proof

A37:
for m being Nat holds S
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: ( 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 A34, A33; :: 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 ) )

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 | (UsedI*Loc I)) . f by A36, FUNCT_1:49

.= t . f by A5, A36, FUNCT_1:49

.= (Comput (Q,t,0)) . f ; :: thesis: verum

end;.= 0 by A3, MEMSTR_0:39 ;

A34: IC (Comput (P,s,0)) = IC s

.= 0 by A2, MEMSTR_0:39 ;

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 A34, A33; :: 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 f be FinSeq-Location ; :: thesis: ( f in UsedI*Loc I implies (Comput (P,s,0)) . f = (Comput (Q,t,0)) . f )(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 | (UsedILoc I)) . a by A35, FUNCT_1:49

.= t . a by A4, A35, FUNCT_1:49

.= (Comput (Q,t,0)) . a ; :: thesis: verum

end;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 | (UsedILoc I)) . a by A35, FUNCT_1:49

.= t . a by A4, A35, FUNCT_1:49

.= (Comput (Q,t,0)) . a ; :: thesis: verum

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 | (UsedI*Loc I)) . f by A36, FUNCT_1:49

.= t . f by A5, A36, FUNCT_1:49

.= (Comput (Q,t,0)) . f ; :: thesis: verum

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;

end;

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 ) )

(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 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: ( ( 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 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 | (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: verum

end;.= 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: ( ( 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 f be FinSeq-Location ; :: thesis: ( f in UsedI*Loc I implies (Comput (P,s,m)) . f = (Comput (Q,t,m)) . f )(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 | (UsedILoc I)) . a by A41, FUNCT_1:49

.= t . a by A4, A41, FUNCT_1:49

.= (Comput (Q,t,m)) . a by A39 ; :: thesis: verum

end;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 | (UsedILoc I)) . a by A41, FUNCT_1:49

.= t . a by A4, A41, FUNCT_1:49

.= (Comput (Q,t,m)) . a by A39 ; :: thesis: verum

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 | (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: verum

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 ) )

(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 A38, A43, NAT_1:13;

then A45: IC (Comput (P,s,p)) in dom I by A6;

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 ;

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: ( ( 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 A52, A59, A58, Th64;

end;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: ( dom ((Comput (P,s,p)) | (UsedI*Loc I)) = (dom (Comput (Q,t,p))) /\ (UsedI*Loc I) & ( for x being object st x in dom ((Comput (P,s,p)) | (UsedI*Loc I)) holds

((Comput (P,s,p)) | (UsedI*Loc I)) . x = (Comput (Q,t,p)) . x ) )

then A47:
(Comput (P,s,p)) | (UsedI*Loc I) = (Comput (Q,t,p)) | (UsedI*Loc I)
by FUNCT_1:46;((Comput (P,s,p)) | (UsedI*Loc I)) . x = (Comput (Q,t,p)) . x ) )

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: for x being object st x in dom ((Comput (P,s,p)) | (UsedI*Loc I)) holds

((Comput (P,s,p)) | (UsedI*Loc I)) . x = (Comput (Q,t,p)) . x

let x be object ; :: thesis: ( x in dom ((Comput (P,s,p)) | (UsedI*Loc I)) implies ((Comput (P,s,p)) | (UsedI*Loc I)) . x = (Comput (Q,t,p)) . x )

assume x in dom ((Comput (P,s,p)) | (UsedI*Loc I)) ; :: thesis: ((Comput (P,s,p)) | (UsedI*Loc I)) . 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)) | (UsedI*Loc I)) . x = (Comput (P,s,p)) . x9 by A46, FUNCT_1:49

.= (Comput (Q,t,p)) . x by A37, A44, A46 ; :: thesis: verum

end;.= 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: for x being object st x in dom ((Comput (P,s,p)) | (UsedI*Loc I)) holds

((Comput (P,s,p)) | (UsedI*Loc I)) . x = (Comput (Q,t,p)) . x

let x be object ; :: thesis: ( x in dom ((Comput (P,s,p)) | (UsedI*Loc I)) implies ((Comput (P,s,p)) | (UsedI*Loc I)) . x = (Comput (Q,t,p)) . x )

assume x in dom ((Comput (P,s,p)) | (UsedI*Loc I)) ; :: thesis: ((Comput (P,s,p)) | (UsedI*Loc I)) . 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)) | (UsedI*Loc I)) . x = (Comput (P,s,p)) . x9 by A46, FUNCT_1:49

.= (Comput (Q,t,p)) . x by A37, A44, A46 ; :: thesis: verum

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)) | (UsedILoc I)) = (dom (Comput (Q,t,p))) /\ (UsedILoc I) & ( for x being object st x in dom ((Comput (P,s,p)) | (UsedILoc I)) holds

((Comput (P,s,p)) | (UsedILoc I)) . x = (Comput (Q,t,p)) . x ) )

then A51:
(Comput (P,s,p)) | (UsedILoc I) = (Comput (Q,t,p)) | (UsedILoc I)
by FUNCT_1:46;((Comput (P,s,p)) | (UsedILoc I)) . x = (Comput (Q,t,p)) . x ) )

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: for x being object st x in dom ((Comput (P,s,p)) | (UsedILoc I)) holds

((Comput (P,s,p)) | (UsedILoc I)) . x = (Comput (Q,t,p)) . x

let x be object ; :: thesis: ( x in dom ((Comput (P,s,p)) | (UsedILoc I)) implies ((Comput (P,s,p)) | (UsedILoc I)) . x = (Comput (Q,t,p)) . x )

assume x in dom ((Comput (P,s,p)) | (UsedILoc I)) ; :: thesis: ((Comput (P,s,p)) | (UsedILoc I)) . 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)) | (UsedILoc I)) . x = (Comput (P,s,p)) . x9 by A50, FUNCT_1:49

.= (Comput (Q,t,p)) . x by A37, A44, A50 ; :: thesis: verum

end;.= the carrier of SCM+FSA /\ (UsedILoc I) by PARTFUN1:def 2

.= (dom (Comput (Q,t,p))) /\ (UsedILoc I) by PARTFUN1:def 2 ; :: thesis: for x being object st x in dom ((Comput (P,s,p)) | (UsedILoc I)) holds

((Comput (P,s,p)) | (UsedILoc I)) . x = (Comput (Q,t,p)) . x

let x be object ; :: thesis: ( x in dom ((Comput (P,s,p)) | (UsedILoc I)) implies ((Comput (P,s,p)) | (UsedILoc I)) . x = (Comput (Q,t,p)) . x )

assume x in dom ((Comput (P,s,p)) | (UsedILoc I)) ; :: thesis: ((Comput (P,s,p)) | (UsedILoc I)) . 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)) | (UsedILoc I)) . x = (Comput (P,s,p)) . x9 by A50, FUNCT_1:49

.= (Comput (Q,t,p)) . x by A37, A44, A50 ; :: thesis: verum

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: ( ( 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 A52, A59, A58, Th64;

hereby :: thesis: for f being FinSeq-Location st f in UsedI*Loc I holds

(Comput (P,s,m)) . f = (Comput (Q,t,m)) . f

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;(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)) . b_{1} = (Comput (Q,t,m)) . b_{1} )

assume A61: a in UsedILoc I ; :: thesis: (Comput (P,s,m)) . b_{1} = (Comput (Q,t,m)) . b_{1}

end;assume A61: a in UsedILoc I ; :: thesis: (Comput (P,s,m)) . b

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

end;

suppose A62:
a in UsedIntLoc (P . (IC (Comput (P,s,p))))
; :: thesis: (Comput (P,s,m)) . b_{1} = (Comput (Q,t,m)) . b_{1}

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: verum

end;.= (Comput (Q,t,m)) . a by A43, A55, A56, A60, A62, FUNCT_1:49 ;

:: thesis: verum

suppose A63:
not a in UsedIntLoc (P . (IC (Comput (P,s,p))))
; :: thesis: (Comput (P,s,m)) . b_{1} = (Comput (Q,t,m)) . b_{1}

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: verum

end;.= (Comput (Q,t,p)) . a by A37, A44, A61

.= (Comput (Q,t,m)) . a by A43, A55, A56, A63, Th60 ;

:: thesis: verum

hereby :: thesis: verum

let f be FinSeq-Location ; :: thesis: ( f in UsedI*Loc I implies (Comput (P,s,m)) . b_{1} = (Comput (Q,t,m)) . b_{1} )

assume A65: f in UsedI*Loc I ; :: thesis: (Comput (P,s,m)) . b_{1} = (Comput (Q,t,m)) . b_{1}

end;assume A65: f in UsedI*Loc I ; :: thesis: (Comput (P,s,m)) . b

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

end;

suppose A66:
f in UsedInt*Loc (P . (IC (Comput (P,s,p))))
; :: thesis: (Comput (P,s,m)) . b_{1} = (Comput (Q,t,m)) . b_{1}

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: verum

end;.= (Comput (Q,t,m)) . f by A43, A55, A56, A64, A66, FUNCT_1:49 ;

:: thesis: verum

suppose A67:
not f in UsedInt*Loc (P . (IC (Comput (P,s,p))))
; :: thesis: (Comput (P,s,m)) . b_{1} = (Comput (Q,t,m)) . b_{1}

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: verum

end;.= (Comput (Q,t,p)) . f by A37, A44, A65

.= (Comput (Q,t,m)) . f by A43, A55, A56, A67, Th62 ;

:: thesis: verum