let I be Program of SCM+FSA ; :: thesis: for n being Element of NAT
for s, t being State of SCM+FSA st I +* (Start-At (insloc 0 )) c= s & I +* (Start-At (insloc 0 )) 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 (Computation s,m) in dom I ) holds
( ( for m being Element of NAT st m < n holds
IC (Computation t,m) in dom I ) & ( for m being Element of NAT st m <= n holds
( IC (Computation s,m) = IC (Computation t,m) & ( for a being Int-Location st a in UsedIntLoc I holds
(Computation s,m) . a = (Computation t,m) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Computation s,m) . f = (Computation t,m) . f ) ) ) )
let n be Element of NAT ; :: thesis: for s, t being State of SCM+FSA st I +* (Start-At (insloc 0 )) c= s & I +* (Start-At (insloc 0 )) 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 (Computation s,m) in dom I ) holds
( ( for m being Element of NAT st m < n holds
IC (Computation t,m) in dom I ) & ( for m being Element of NAT st m <= n holds
( IC (Computation s,m) = IC (Computation t,m) & ( for a being Int-Location st a in UsedIntLoc I holds
(Computation s,m) . a = (Computation t,m) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Computation s,m) . f = (Computation t,m) . f ) ) ) )
let s, t be State of SCM+FSA ; :: thesis: ( I +* (Start-At (insloc 0 )) c= s & I +* (Start-At (insloc 0 )) 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 (Computation s,m) in dom I ) implies ( ( for m being Element of NAT st m < n holds
IC (Computation t,m) in dom I ) & ( for m being Element of NAT st m <= n holds
( IC (Computation s,m) = IC (Computation t,m) & ( for a being Int-Location st a in UsedIntLoc I holds
(Computation s,m) . a = (Computation t,m) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Computation s,m) . f = (Computation t,m) . f ) ) ) ) )
assume that
A1:
( I +* (Start-At (insloc 0 )) c= s & I +* (Start-At (insloc 0 )) c= t )
and
A2:
( s | (UsedIntLoc I) = t | (UsedIntLoc I) & s | (UsedInt*Loc I) = t | (UsedInt*Loc I) )
and
A3:
for m being Element of NAT st m < n holds
IC (Computation s,m) in dom I
; :: thesis: ( ( for m being Element of NAT st m < n holds
IC (Computation t,m) in dom I ) & ( for m being Element of NAT st m <= n holds
( IC (Computation s,m) = IC (Computation t,m) & ( for a being Int-Location st a in UsedIntLoc I holds
(Computation s,m) . a = (Computation t,m) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Computation s,m) . f = (Computation t,m) . f ) ) ) )
defpred S1[ Element of NAT ] means ( $1 < n implies ( IC (Computation t,$1) in dom I & IC (Computation s,$1) = IC (Computation t,$1) & ( for a being Int-Location st a in UsedIntLoc I holds
(Computation s,$1) . a = (Computation t,$1) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Computation s,$1) . f = (Computation t,$1) . f ) ) );
A4:
S1[ 0 ]
proof
assume A5:
0 < n
;
:: thesis: ( IC (Computation t,0 ) in dom I & IC (Computation s,0 ) = IC (Computation t,0 ) & ( for a being Int-Location st a in UsedIntLoc I holds
(Computation s,0 ) . a = (Computation t,0 ) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Computation s,0 ) . f = (Computation t,0 ) . f ) )
A6:
IC (Computation s,0 ) =
IC s
by AMI_1:13
.=
insloc 0
by A1, Th67
;
A7:
IC (Computation t,0 ) =
IC t
by AMI_1:13
.=
insloc 0
by A1, Th67
;
hence
IC (Computation t,0 ) in dom I
by A3, A5, A6;
:: thesis: ( IC (Computation s,0 ) = IC (Computation t,0 ) & ( for a being Int-Location st a in UsedIntLoc I holds
(Computation s,0 ) . a = (Computation t,0 ) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Computation s,0 ) . f = (Computation t,0 ) . f ) )
thus
IC (Computation s,0 ) = IC (Computation t,0 )
by A6, A7;
:: thesis: ( ( for a being Int-Location st a in UsedIntLoc I holds
(Computation s,0 ) . a = (Computation t,0 ) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Computation s,0 ) . f = (Computation t,0 ) . f ) )
let f be
FinSeq-Location ;
:: thesis: ( f in UsedInt*Loc I implies (Computation s,0 ) . f = (Computation t,0 ) . f )
assume A9:
f in UsedInt*Loc I
;
:: thesis: (Computation s,0 ) . f = (Computation t,0 ) . f
thus (Computation s,0 ) . f =
s . f
by AMI_1:13
.=
(s | (UsedInt*Loc I)) . f
by A9, FUNCT_1:72
.=
t . f
by A2, A9, FUNCT_1:72
.=
(Computation t,0 ) . f
by AMI_1:13
;
:: thesis: verum
end;
A10:
now let m be
Element of
NAT ;
:: thesis: ( S1[m] implies S1[m + 1] )assume A11:
S1[
m]
;
:: thesis: S1[m + 1]thus
S1[
m + 1]
:: thesis: verumproof
set m1 =
m + 1;
assume A12:
m + 1
< n
;
:: thesis: ( IC (Computation t,(m + 1)) in dom I & IC (Computation s,(m + 1)) = IC (Computation t,(m + 1)) & ( for a being Int-Location st a in UsedIntLoc I holds
(Computation s,(m + 1)) . a = (Computation t,(m + 1)) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Computation s,(m + 1)) . f = (Computation t,(m + 1)) . f ) )
then A13:
m < n
by NAT_1:13;
A14:
Computation s,
(m + 1) =
Following (Computation s,m)
by AMI_1:14
.=
Exec ((Computation s,m) . (IC (Computation s,m))),
(Computation s,m)
;
A15:
Computation t,
(m + 1) =
Following (Computation t,m)
by AMI_1:14
.=
Exec ((Computation t,m) . (IC (Computation t,m))),
(Computation t,m)
;
dom I misses dom (Start-At (insloc 0 ))
by Th64;
then
I c= I +* (Start-At (insloc 0 ))
by FUNCT_4:33;
then
(
I c= s &
I c= t )
by A1, XBOOLE_1:1;
then A16:
(
I c= Computation s,
m &
I c= Computation t,
m )
by AMI_1:81;
then A17:
(Computation s,m) . (IC (Computation s,m)) = I . (IC (Computation s,m))
by A11, A12, GRFUNC_1:8, NAT_1:13;
then A18:
(Computation s,m) . (IC (Computation s,m)) = (Computation t,m) . (IC (Computation t,m))
by A11, A12, A16, GRFUNC_1:8, NAT_1:13;
set i =
(Computation s,m) . (IC (Computation s,m));
IC (Computation s,m) in dom I
by A3, A13;
then A19:
(Computation s,m) . (IC (Computation s,m)) in rng I
by A17, FUNCT_1:def 5;
now thus dom ((Computation s,m) | (UsedIntLoc I)) =
(dom (Computation s,m)) /\ (UsedIntLoc I)
by RELAT_1:90
.=
(dom the Object-Kind of SCM+FSA ) /\ (UsedIntLoc I)
by CARD_3:18
.=
(dom (Computation t,m)) /\ (UsedIntLoc I)
by CARD_3:18
;
:: thesis: for x being set st x in dom ((Computation s,m) | (UsedIntLoc I)) holds
((Computation s,m) | (UsedIntLoc I)) . x = (Computation t,m) . xlet x be
set ;
:: thesis: ( x in dom ((Computation s,m) | (UsedIntLoc I)) implies ((Computation s,m) | (UsedIntLoc I)) . x = (Computation t,m) . x )assume
x in dom ((Computation s,m) | (UsedIntLoc I))
;
:: thesis: ((Computation s,m) | (UsedIntLoc I)) . x = (Computation t,m) . xthen A20:
x in UsedIntLoc I
by RELAT_1:86;
then reconsider x' =
x as
Int-Location by SCMFSA_2:11;
thus ((Computation s,m) | (UsedIntLoc I)) . x =
(Computation s,m) . x'
by A20, FUNCT_1:72
.=
(Computation t,m) . x
by A11, A12, A20, NAT_1:13
;
:: thesis: verum end;
then A21:
(Computation s,m) | (UsedIntLoc I) = (Computation t,m) | (UsedIntLoc I)
by FUNCT_1:68;
A22:
(Computation s,m) | (UsedIntLoc ((Computation s,m) . (IC (Computation s,m)))) =
((Computation s,m) | (UsedIntLoc I)) | (UsedIntLoc ((Computation s,m) . (IC (Computation s,m))))
by A19, Th23, RELAT_1:103
.=
(Computation t,m) | (UsedIntLoc ((Computation s,m) . (IC (Computation s,m))))
by A19, A21, Th23, RELAT_1:103
;
now thus dom ((Computation s,m) | (UsedInt*Loc I)) =
(dom (Computation s,m)) /\ (UsedInt*Loc I)
by RELAT_1:90
.=
(dom the Object-Kind of SCM+FSA ) /\ (UsedInt*Loc I)
by CARD_3:18
.=
(dom (Computation t,m)) /\ (UsedInt*Loc I)
by CARD_3:18
;
:: thesis: for x being set st x in dom ((Computation s,m) | (UsedInt*Loc I)) holds
((Computation s,m) | (UsedInt*Loc I)) . x = (Computation t,m) . xlet x be
set ;
:: thesis: ( x in dom ((Computation s,m) | (UsedInt*Loc I)) implies ((Computation s,m) | (UsedInt*Loc I)) . x = (Computation t,m) . x )assume
x in dom ((Computation s,m) | (UsedInt*Loc I))
;
:: thesis: ((Computation s,m) | (UsedInt*Loc I)) . x = (Computation t,m) . xthen A23:
x in UsedInt*Loc I
by RELAT_1:86;
then reconsider x' =
x as
FinSeq-Location by SCMFSA_2:12;
thus ((Computation s,m) | (UsedInt*Loc I)) . x =
(Computation s,m) . x'
by A23, FUNCT_1:72
.=
(Computation t,m) . x
by A11, A12, A23, NAT_1:13
;
:: thesis: verum end;
then A24:
(Computation s,m) | (UsedInt*Loc I) = (Computation t,m) | (UsedInt*Loc I)
by FUNCT_1:68;
(Computation s,m) | (UsedInt*Loc ((Computation s,m) . (IC (Computation s,m)))) =
((Computation s,m) | (UsedInt*Loc I)) | (UsedInt*Loc ((Computation s,m) . (IC (Computation s,m))))
by A19, Th39, RELAT_1:103
.=
(Computation t,m) | (UsedInt*Loc ((Computation s,m) . (IC (Computation s,m))))
by A19, A24, Th39, RELAT_1:103
;
then A25:
(
(Exec ((Computation s,m) . (IC (Computation s,m))),(Computation s,m)) | (UsedIntLoc ((Computation s,m) . (IC (Computation s,m)))) = (Exec ((Computation s,m) . (IC (Computation s,m))),(Computation t,m)) | (UsedIntLoc ((Computation s,m) . (IC (Computation s,m)))) &
(Exec ((Computation s,m) . (IC (Computation s,m))),(Computation s,m)) | (UsedInt*Loc ((Computation s,m) . (IC (Computation s,m)))) = (Exec ((Computation s,m) . (IC (Computation s,m))),(Computation t,m)) | (UsedInt*Loc ((Computation s,m) . (IC (Computation s,m)))) &
IC (Exec ((Computation s,m) . (IC (Computation s,m))),(Computation s,m)) = IC (Exec ((Computation s,m) . (IC (Computation s,m))),(Computation t,m)) )
by A11, A12, A22, Th72, NAT_1:13;
hence
IC (Computation t,(m + 1)) in dom I
by A3, A12, A14, A15, A18;
:: thesis: ( IC (Computation s,(m + 1)) = IC (Computation t,(m + 1)) & ( for a being Int-Location st a in UsedIntLoc I holds
(Computation s,(m + 1)) . a = (Computation t,(m + 1)) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Computation s,(m + 1)) . f = (Computation t,(m + 1)) . f ) )
thus
IC (Computation s,(m + 1)) = IC (Computation t,(m + 1))
by A11, A12, A14, A15, A16, A17, A25, GRFUNC_1:8, NAT_1:13;
:: thesis: ( ( for a being Int-Location st a in UsedIntLoc I holds
(Computation s,(m + 1)) . a = (Computation t,(m + 1)) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Computation s,(m + 1)) . f = (Computation t,(m + 1)) . f ) )
hereby :: thesis: for f being FinSeq-Location st f in UsedInt*Loc I holds
(Computation s,(m + 1)) . f = (Computation t,(m + 1)) . f
let a be
Int-Location ;
:: thesis: ( a in UsedIntLoc I implies (Computation s,(m + 1)) . b1 = (Computation t,(m + 1)) . b1 )assume A26:
a in UsedIntLoc I
;
:: thesis: (Computation s,(m + 1)) . b1 = (Computation t,(m + 1)) . b1per cases
( a in UsedIntLoc ((Computation s,m) . (IC (Computation s,m))) or not a in UsedIntLoc ((Computation s,m) . (IC (Computation s,m))) )
;
suppose A27:
a in UsedIntLoc ((Computation s,m) . (IC (Computation s,m)))
;
:: thesis: (Computation s,(m + 1)) . b1 = (Computation t,(m + 1)) . b1hence (Computation s,(m + 1)) . a =
((Exec ((Computation s,m) . (IC (Computation s,m))),(Computation s,m)) | (UsedIntLoc ((Computation s,m) . (IC (Computation s,m))))) . a
by A14, FUNCT_1:72
.=
(Computation t,(m + 1)) . a
by A15, A18, A25, A27, FUNCT_1:72
;
:: thesis: verum end; suppose A28:
not
a in UsedIntLoc ((Computation s,m) . (IC (Computation s,m)))
;
:: thesis: (Computation s,(m + 1)) . b1 = (Computation t,(m + 1)) . b1hence (Computation s,(m + 1)) . a =
(Computation s,m) . a
by A14, Th68
.=
(Computation t,m) . a
by A11, A12, A26, NAT_1:13
.=
(Computation t,(m + 1)) . a
by A15, A18, A28, Th68
;
:: thesis: verum end;
end;
let f be
FinSeq-Location ;
:: thesis: ( f in UsedInt*Loc I implies (Computation s,(m + 1)) . f = (Computation t,(m + 1)) . f )
assume A29:
f in UsedInt*Loc I
;
:: thesis: (Computation s,(m + 1)) . f = (Computation t,(m + 1)) . f
per cases
( f in UsedInt*Loc ((Computation s,m) . (IC (Computation s,m))) or not f in UsedInt*Loc ((Computation s,m) . (IC (Computation s,m))) )
;
suppose A30:
f in UsedInt*Loc ((Computation s,m) . (IC (Computation s,m)))
;
:: thesis: (Computation s,(m + 1)) . f = (Computation t,(m + 1)) . fhence (Computation s,(m + 1)) . f =
((Exec ((Computation s,m) . (IC (Computation s,m))),(Computation s,m)) | (UsedInt*Loc ((Computation s,m) . (IC (Computation s,m))))) . f
by A14, FUNCT_1:72
.=
(Computation t,(m + 1)) . f
by A15, A18, A25, A30, FUNCT_1:72
;
:: thesis: verum end; suppose A31:
not
f in UsedInt*Loc ((Computation s,m) . (IC (Computation s,m)))
;
:: thesis: (Computation s,(m + 1)) . f = (Computation t,(m + 1)) . fhence (Computation s,(m + 1)) . f =
(Computation s,m) . f
by A14, Th70
.=
(Computation t,m) . f
by A11, A12, A29, NAT_1:13
.=
(Computation t,(m + 1)) . f
by A15, A18, A31, Th70
;
:: thesis: verum end;
end; end;
A32:
for m being Element of NAT holds S1[m]
from NAT_1:sch 1(A4, A10);
hence
for m being Element of NAT st m < n holds
IC (Computation t,m) in dom I
; :: thesis: for m being Element of NAT st m <= n holds
( IC (Computation s,m) = IC (Computation t,m) & ( for a being Int-Location st a in UsedIntLoc I holds
(Computation s,m) . a = (Computation t,m) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Computation s,m) . f = (Computation t,m) . f ) )
let m be Element of NAT ; :: thesis: ( m <= n implies ( IC (Computation s,m) = IC (Computation t,m) & ( for a being Int-Location st a in UsedIntLoc I holds
(Computation s,m) . a = (Computation t,m) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Computation s,m) . f = (Computation t,m) . f ) ) )
assume A33:
m <= n
; :: thesis: ( IC (Computation s,m) = IC (Computation t,m) & ( for a being Int-Location st a in UsedIntLoc I holds
(Computation s,m) . a = (Computation t,m) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Computation s,m) . f = (Computation t,m) . f ) )
per cases
( m = 0 or ex p being Nat st m = p + 1 )
by NAT_1:6;
suppose A34:
m = 0
;
:: thesis: ( IC (Computation s,m) = IC (Computation t,m) & ( for a being Int-Location st a in UsedIntLoc I holds
(Computation s,m) . a = (Computation t,m) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Computation s,m) . f = (Computation t,m) . f ) )A35:
IC (Computation s,0 ) =
IC s
by AMI_1:13
.=
insloc 0
by A1, Th67
;
IC (Computation t,0 ) =
IC t
by AMI_1:13
.=
insloc 0
by A1, Th67
;
hence
IC (Computation s,m) = IC (Computation t,m)
by A34, A35;
:: thesis: ( ( for a being Int-Location st a in UsedIntLoc I holds
(Computation s,m) . a = (Computation t,m) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Computation s,m) . f = (Computation t,m) . f ) )hereby :: thesis: for f being FinSeq-Location st f in UsedInt*Loc I holds
(Computation s,m) . f = (Computation t,m) . f
let a be
Int-Location ;
:: thesis: ( a in UsedIntLoc I implies (Computation s,m) . a = (Computation t,m) . a )assume A36:
a in UsedIntLoc I
;
:: thesis: (Computation s,m) . a = (Computation t,m) . athus (Computation s,m) . a =
s . a
by A34, AMI_1:13
.=
(s | (UsedIntLoc I)) . a
by A36, FUNCT_1:72
.=
t . a
by A2, A36, FUNCT_1:72
.=
(Computation t,m) . a
by A34, AMI_1:13
;
:: thesis: verum
end; let f be
FinSeq-Location ;
:: thesis: ( f in UsedInt*Loc I implies (Computation s,m) . f = (Computation t,m) . f )assume A37:
f in UsedInt*Loc I
;
:: thesis: (Computation s,m) . f = (Computation t,m) . fthus (Computation s,m) . f =
s . f
by A34, AMI_1:13
.=
(s | (UsedInt*Loc I)) . f
by A37, FUNCT_1:72
.=
t . f
by A2, A37, FUNCT_1:72
.=
(Computation t,m) . f
by A34, AMI_1:13
;
:: thesis: verum end; suppose
ex
p being
Nat st
m = p + 1
;
:: thesis: ( IC (Computation s,m) = IC (Computation t,m) & ( for a being Int-Location st a in UsedIntLoc I holds
(Computation s,m) . a = (Computation t,m) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Computation s,m) . f = (Computation t,m) . f ) )then consider p being
Nat such that A38:
m = p + 1
;
reconsider p =
p as
Element of
NAT by ORDINAL1:def 13;
set p1 =
p + 1;
A39:
p < n
by A33, A38, NAT_1:13;
A40:
Computation s,
(p + 1) =
Following (Computation s,p)
by AMI_1:14
.=
Exec ((Computation s,p) . (IC (Computation s,p))),
(Computation s,p)
;
A41:
Computation t,
(p + 1) =
Following (Computation t,p)
by AMI_1:14
.=
Exec ((Computation t,p) . (IC (Computation t,p))),
(Computation t,p)
;
A42:
(
IC (Computation s,p) = IC (Computation t,p) &
IC (Computation s,p) in dom I )
by A3, A32, A39;
dom I misses dom (Start-At (insloc 0 ))
by Th64;
then
I c= I +* (Start-At (insloc 0 ))
by FUNCT_4:33;
then
(
I c= s &
I c= t )
by A1, XBOOLE_1:1;
then A43:
(
I c= Computation s,
p &
I c= Computation t,
p )
by AMI_1:81;
then A44:
(Computation s,p) . (IC (Computation s,p)) = I . (IC (Computation s,p))
by A42, GRFUNC_1:8;
then A45:
(Computation s,p) . (IC (Computation s,p)) = (Computation t,p) . (IC (Computation t,p))
by A42, A43, GRFUNC_1:8;
set i =
(Computation s,p) . (IC (Computation s,p));
IC (Computation s,p) in dom I
by A3, A39;
then A46:
(Computation s,p) . (IC (Computation s,p)) in rng I
by A44, FUNCT_1:def 5;
now thus dom ((Computation s,p) | (UsedIntLoc I)) =
(dom (Computation s,p)) /\ (UsedIntLoc I)
by RELAT_1:90
.=
(dom the Object-Kind of SCM+FSA ) /\ (UsedIntLoc I)
by CARD_3:18
.=
(dom (Computation t,p)) /\ (UsedIntLoc I)
by CARD_3:18
;
:: thesis: for x being set st x in dom ((Computation s,p) | (UsedIntLoc I)) holds
((Computation s,p) | (UsedIntLoc I)) . x = (Computation t,p) . xlet x be
set ;
:: thesis: ( x in dom ((Computation s,p) | (UsedIntLoc I)) implies ((Computation s,p) | (UsedIntLoc I)) . x = (Computation t,p) . x )assume
x in dom ((Computation s,p) | (UsedIntLoc I))
;
:: thesis: ((Computation s,p) | (UsedIntLoc I)) . x = (Computation t,p) . xthen A47:
x in UsedIntLoc I
by RELAT_1:86;
then reconsider x' =
x as
Int-Location by SCMFSA_2:11;
thus ((Computation s,p) | (UsedIntLoc I)) . x =
(Computation s,p) . x'
by A47, FUNCT_1:72
.=
(Computation t,p) . x
by A32, A39, A47
;
:: thesis: verum end; then A48:
(Computation s,p) | (UsedIntLoc I) = (Computation t,p) | (UsedIntLoc I)
by FUNCT_1:68;
A49:
(Computation s,p) | (UsedIntLoc ((Computation s,p) . (IC (Computation s,p)))) =
((Computation s,p) | (UsedIntLoc I)) | (UsedIntLoc ((Computation s,p) . (IC (Computation s,p))))
by A46, Th23, RELAT_1:103
.=
(Computation t,p) | (UsedIntLoc ((Computation s,p) . (IC (Computation s,p))))
by A46, A48, Th23, RELAT_1:103
;
now thus dom ((Computation s,p) | (UsedInt*Loc I)) =
(dom (Computation s,p)) /\ (UsedInt*Loc I)
by RELAT_1:90
.=
(dom the Object-Kind of SCM+FSA ) /\ (UsedInt*Loc I)
by CARD_3:18
.=
(dom (Computation t,p)) /\ (UsedInt*Loc I)
by CARD_3:18
;
:: thesis: for x being set st x in dom ((Computation s,p) | (UsedInt*Loc I)) holds
((Computation s,p) | (UsedInt*Loc I)) . x = (Computation t,p) . xlet x be
set ;
:: thesis: ( x in dom ((Computation s,p) | (UsedInt*Loc I)) implies ((Computation s,p) | (UsedInt*Loc I)) . x = (Computation t,p) . x )assume
x in dom ((Computation s,p) | (UsedInt*Loc I))
;
:: thesis: ((Computation s,p) | (UsedInt*Loc I)) . x = (Computation t,p) . xthen A50:
x in UsedInt*Loc I
by RELAT_1:86;
then reconsider x' =
x as
FinSeq-Location by SCMFSA_2:12;
thus ((Computation s,p) | (UsedInt*Loc I)) . x =
(Computation s,p) . x'
by A50, FUNCT_1:72
.=
(Computation t,p) . x
by A32, A39, A50
;
:: thesis: verum end; then A51:
(Computation s,p) | (UsedInt*Loc I) = (Computation t,p) | (UsedInt*Loc I)
by FUNCT_1:68;
A52:
(Computation s,p) | (UsedInt*Loc ((Computation s,p) . (IC (Computation s,p)))) =
((Computation s,p) | (UsedInt*Loc I)) | (UsedInt*Loc ((Computation s,p) . (IC (Computation s,p))))
by A46, Th39, RELAT_1:103
.=
(Computation t,p) | (UsedInt*Loc ((Computation s,p) . (IC (Computation s,p))))
by A46, A51, Th39, RELAT_1:103
;
then A53:
(
(Exec ((Computation s,p) . (IC (Computation s,p))),(Computation s,p)) | (UsedIntLoc ((Computation s,p) . (IC (Computation s,p)))) = (Exec ((Computation s,p) . (IC (Computation s,p))),(Computation t,p)) | (UsedIntLoc ((Computation s,p) . (IC (Computation s,p)))) &
(Exec ((Computation s,p) . (IC (Computation s,p))),(Computation s,p)) | (UsedInt*Loc ((Computation s,p) . (IC (Computation s,p)))) = (Exec ((Computation s,p) . (IC (Computation s,p))),(Computation t,p)) | (UsedInt*Loc ((Computation s,p) . (IC (Computation s,p)))) &
IC (Exec ((Computation s,p) . (IC (Computation s,p))),(Computation s,p)) = IC (Exec ((Computation s,p) . (IC (Computation s,p))),(Computation t,p)) )
by A42, A49, Th72;
thus
IC (Computation s,m) = IC (Computation t,m)
by A38, A40, A41, A42, A45, A49, A52, Th72;
:: thesis: ( ( for a being Int-Location st a in UsedIntLoc I holds
(Computation s,m) . a = (Computation t,m) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Computation s,m) . f = (Computation t,m) . f ) )hereby :: thesis: for f being FinSeq-Location st f in UsedInt*Loc I holds
(Computation s,m) . f = (Computation t,m) . f
let a be
Int-Location ;
:: thesis: ( a in UsedIntLoc I implies (Computation s,m) . b1 = (Computation t,m) . b1 )assume A54:
a in UsedIntLoc I
;
:: thesis: (Computation s,m) . b1 = (Computation t,m) . b1per cases
( a in UsedIntLoc ((Computation s,p) . (IC (Computation s,p))) or not a in UsedIntLoc ((Computation s,p) . (IC (Computation s,p))) )
;
suppose A55:
a in UsedIntLoc ((Computation s,p) . (IC (Computation s,p)))
;
:: thesis: (Computation s,m) . b1 = (Computation t,m) . b1hence (Computation s,m) . a =
((Exec ((Computation s,p) . (IC (Computation s,p))),(Computation s,p)) | (UsedIntLoc ((Computation s,p) . (IC (Computation s,p))))) . a
by A38, A40, FUNCT_1:72
.=
(Computation t,m) . a
by A38, A41, A45, A53, A55, FUNCT_1:72
;
:: thesis: verum end; suppose A56:
not
a in UsedIntLoc ((Computation s,p) . (IC (Computation s,p)))
;
:: thesis: (Computation s,m) . b1 = (Computation t,m) . b1hence (Computation s,m) . a =
(Computation s,p) . a
by A38, A40, Th68
.=
(Computation t,p) . a
by A32, A39, A54
.=
(Computation t,m) . a
by A38, A41, A45, A56, Th68
;
:: thesis: verum end;
end; hereby :: thesis: verum
let f be
FinSeq-Location ;
:: thesis: ( f in UsedInt*Loc I implies (Computation s,m) . b1 = (Computation t,m) . b1 )assume A57:
f in UsedInt*Loc I
;
:: thesis: (Computation s,m) . b1 = (Computation t,m) . b1per cases
( f in UsedInt*Loc ((Computation s,p) . (IC (Computation s,p))) or not f in UsedInt*Loc ((Computation s,p) . (IC (Computation s,p))) )
;
suppose A58:
f in UsedInt*Loc ((Computation s,p) . (IC (Computation s,p)))
;
:: thesis: (Computation s,m) . b1 = (Computation t,m) . b1hence (Computation s,m) . f =
((Exec ((Computation s,p) . (IC (Computation s,p))),(Computation s,p)) | (UsedInt*Loc ((Computation s,p) . (IC (Computation s,p))))) . f
by A38, A40, FUNCT_1:72
.=
(Computation t,m) . f
by A38, A41, A45, A53, A58, FUNCT_1:72
;
:: thesis: verum end; suppose A59:
not
f in UsedInt*Loc ((Computation s,p) . (IC (Computation s,p)))
;
:: thesis: (Computation s,m) . b1 = (Computation t,m) . b1hence (Computation s,m) . f =
(Computation s,p) . f
by A38, A40, Th70
.=
(Computation t,p) . f
by A32, A39, A57
.=
(Computation t,m) . f
by A38, A41, A45, A59, Th70
;
:: thesis: verum end;
end; end;