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 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)) | (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 ) )
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;
then A13: (Comput (P,s,m)) | (UsedI*Loc I) = (Comput (Q,t,m)) | (UsedI*Loc I) by FUNCT_1:46;
A14: P . (IC (Comput (P,s,m))) = I . (IC (Comput (P,s,m))) by A8, A11, A1, GRFUNC_1:2, NAT_1:13;
then A15: P . (IC (Comput (P,s,m))) = Q . (IC (Comput (Q,t,m))) by A8, A11, A1, GRFUNC_1:2, NAT_1:13;
now :: thesis: ( 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 ) )
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;
then A17: (Comput (P,s,m)) | (UsedILoc I) = (Comput (Q,t,m)) | (UsedILoc I) by FUNCT_1:46;
dom Q = NAT by PARTFUN1:def 2;
then A18: Q /. (IC (Comput (Q,t,m))) = Q . (IC (Comput (Q,t,m))) by PARTFUN1:def 6;
A19: Comput (Q,t,(m + 1)) = Following (Q,(Comput (Q,t,m))) by EXTPRO_1:3
.= Exec ((Q . (IC (Comput (Q,t,m)))),(Comput (Q,t,m))) by A18 ;
m < n by A11, NAT_1:13;
then IC (Comput (P,s,m)) in dom I by A6;
then A20: P . (IC (Comput (P,s,m))) in rng I by A14, FUNCT_1:def 3;
then A21: (Comput (P,s,m)) | (UsedInt*Loc (P . (IC (Comput (P,s,m))))) = ((Comput (P,s,m)) | (UsedI*Loc I)) | (UsedInt*Loc (P . (IC (Comput (P,s,m))))) by Th35, RELAT_1:74
.= (Comput (Q,t,m)) | (UsedInt*Loc (P . (IC (Comput (P,s,m))))) by A20, A13, Th35, RELAT_1:74 ;
A22: (Comput (P,s,m)) | (UsedIntLoc (P . (IC (Comput (P,s,m))))) = ((Comput (P,s,m)) | (UsedILoc I)) | (UsedIntLoc (P . (IC (Comput (P,s,m))))) by A20, Th19, RELAT_1:74
.= (Comput (Q,t,m)) | (UsedIntLoc (P . (IC (Comput (P,s,m))))) by A20, A17, Th19, RELAT_1:74 ;
then A23: (Exec ((P . (IC (Comput (P,s,m)))),(Comput (P,s,m)))) | (UsedInt*Loc (P . (IC (Comput (P,s,m))))) = (Exec ((P . (IC (Comput (P,s,m)))),(Comput (Q,t,m)))) | (UsedInt*Loc (P . (IC (Comput (P,s,m))))) by A8, A11, A21, Th64, NAT_1:13;
A24: IC (Exec ((P . (IC (Comput (P,s,m)))),(Comput (P,s,m)))) = IC (Exec ((P . (IC (Comput (P,s,m)))),(Comput (Q,t,m)))) by A8, A11, A22, A21, Th64, NAT_1:13;
hence IC (Comput (Q,t,(m + 1))) in dom I by A6, A11, A10, A19, A15; :: thesis: ( 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 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 A10, FUNCT_1:49
.= (Comput (Q,t,(m + 1))) . a by A19, A15, A25, A27, FUNCT_1:49 ;
:: 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 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;
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 A10, FUNCT_1:49
.= (Comput (Q,t,(m + 1))) . f by A19, A15, A23, A30, FUNCT_1:49 ;
:: 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 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;
end;
end;
end;
A32: S1[ 0 ]
proof
A33: IC (Comput (Q,t,0)) = IC t
.= 0 by A3, MEMSTR_0:39 ;
A34: IC (Comput (P,s,0)) = IC s
.= 0 by A2, MEMSTR_0:39 ;
assume 0 < n ; :: thesis: ( 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 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;
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 | (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;
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 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 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;
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 | (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;
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 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 ) )
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;
then A47: (Comput (P,s,p)) | (UsedI*Loc I) = (Comput (Q,t,p)) | (UsedI*Loc I) by FUNCT_1:46;
set i = P . (IC (Comput (P,s,p)));
set p1 = p + 1;
dom P = NAT by PARTFUN1:def 2;
then A48: P /. (IC (Comput (P,s,p))) = P . (IC (Comput (P,s,p))) by PARTFUN1:def 6;
A49: Comput (P,s,(p + 1)) = Following (P,(Comput (P,s,p))) by EXTPRO_1:3
.= Exec ((P . (IC (Comput (P,s,p)))),(Comput (P,s,p))) by A48 ;
now :: thesis: ( 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 ) )
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;
then A51: (Comput (P,s,p)) | (UsedILoc I) = (Comput (Q,t,p)) | (UsedILoc I) by FUNCT_1:46;
A52: IC (Comput (P,s,p)) = IC (Comput (Q,t,p)) by A37, A44;
A53: P . (IC (Comput (P,s,p))) = I . (IC (Comput (P,s,p))) by A45, A1, GRFUNC_1:2;
dom Q = NAT by PARTFUN1:def 2;
then A54: Q /. (IC (Comput (Q,t,p))) = Q . (IC (Comput (Q,t,p))) by PARTFUN1:def 6;
A55: Comput (Q,t,(p + 1)) = Following (Q,(Comput (Q,t,p))) by EXTPRO_1:3
.= Exec ((Q . (IC (Comput (Q,t,p)))),(Comput (Q,t,p))) by A54 ;
A56: P . (IC (Comput (P,s,p))) = Q . (IC (Comput (Q,t,p))) by A52, A45, A53, A1, GRFUNC_1:2;
IC (Comput (P,s,p)) in dom I by A6, A44;
then A57: P . (IC (Comput (P,s,p))) in rng I by A53, FUNCT_1:def 3;
then A58: (Comput (P,s,p)) | (UsedInt*Loc (P . (IC (Comput (P,s,p))))) = ((Comput (P,s,p)) | (UsedI*Loc I)) | (UsedInt*Loc (P . (IC (Comput (P,s,p))))) by Th35, RELAT_1:74
.= (Comput (Q,t,p)) | (UsedInt*Loc (P . (IC (Comput (P,s,p))))) by A57, A47, Th35, RELAT_1:74 ;
A59: (Comput (P,s,p)) | (UsedIntLoc (P . (IC (Comput (P,s,p))))) = ((Comput (P,s,p)) | (UsedILoc I)) | (UsedIntLoc (P . (IC (Comput (P,s,p))))) by A57, Th19, RELAT_1:74
.= (Comput (Q,t,p)) | (UsedIntLoc (P . (IC (Comput (P,s,p))))) by A57, A51, Th19, RELAT_1:74 ;
hence IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) by A43, A49, A55, A52, A56, A58, Th64; :: thesis: ( ( 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
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 A43, A49, FUNCT_1:49
.= (Comput (Q,t,m)) . a by A43, A55, A56, A60, A62, FUNCT_1:49 ;
:: 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 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;
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 A52, A59, A58, Th64;
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 A43, A49, FUNCT_1:49
.= (Comput (Q,t,m)) . f by A43, A55, A56, A64, A66, FUNCT_1:49 ;
:: 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 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;
end;
end;
end;
end;