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
and
A2:
I +* (Start-At (insloc 0 )) c= t
and
A3:
s | (UsedIntLoc I) = t | (UsedIntLoc I)
and
A4:
s | (UsedInt*Loc I) = t | (UsedInt*Loc I)
and
A5:
for m being Element of NAT st m < n holds
IC (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 ) ) );
A6:
now let m be
Element of
NAT ;
:: thesis: ( S1[m] implies S1[m + 1] )assume A7:
S1[
m]
;
:: thesis: S1[m + 1]thus
S1[
m + 1]
:: thesis: verumproof
dom I misses dom (Start-At (insloc 0 ))
by Th64;
then A8:
I c= I +* (Start-At (insloc 0 ))
by FUNCT_4:33;
then
I c= t
by A2, XBOOLE_1:1;
then A9:
I c= Computation t,
m
by AMI_1:81;
set i =
(Computation s,m) . (IC (Computation s,m));
set m1 =
m + 1;
A10:
Computation s,
(m + 1) =
Following (Computation s,m)
by AMI_1:14
.=
Exec ((Computation s,m) . (IC (Computation s,m))),
(Computation s,m)
;
assume A11:
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 ) )
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 A12:
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 A12, FUNCT_1:72
.=
(Computation t,m) . x
by A7, A11, A12, NAT_1:13
;
:: thesis: verum end;
then A13:
(Computation s,m) | (UsedInt*Loc I) = (Computation t,m) | (UsedInt*Loc I)
by FUNCT_1:68;
I c= s
by A1, A8, XBOOLE_1:1;
then
I c= Computation s,
m
by AMI_1:81;
then A14:
(Computation s,m) . (IC (Computation s,m)) = I . (IC (Computation s,m))
by A7, A11, GRFUNC_1:8, NAT_1:13;
then A15:
(Computation s,m) . (IC (Computation s,m)) = (Computation t,m) . (IC (Computation t,m))
by A7, A11, A9, GRFUNC_1:8, NAT_1:13;
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 A16:
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 A16, FUNCT_1:72
.=
(Computation t,m) . x
by A7, A11, A16, NAT_1:13
;
:: thesis: verum end;
then A17:
(Computation s,m) | (UsedIntLoc I) = (Computation t,m) | (UsedIntLoc I)
by FUNCT_1:68;
A18:
Computation t,
(m + 1) =
Following (Computation t,m)
by AMI_1:14
.=
Exec ((Computation t,m) . (IC (Computation t,m))),
(Computation t,m)
;
m < n
by A11, NAT_1:13;
then
IC (Computation s,m) in dom I
by A5;
then A19:
(Computation s,m) . (IC (Computation s,m)) in rng I
by A14, FUNCT_1:def 5;
then A20:
(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 Th39, RELAT_1:103
.=
(Computation t,m) | (UsedInt*Loc ((Computation s,m) . (IC (Computation s,m))))
by A19, A13, Th39, RELAT_1:103
;
A21:
(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, A17, Th23, RELAT_1:103
;
then A22:
(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))))
by A7, A11, A20, Th72, NAT_1:13;
A23:
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 A7, A11, A21, A20, Th72, NAT_1:13;
hence
IC (Computation t,(m + 1)) in dom I
by A5, A11, A10, A18, A15;
:: 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 A7, A11, A10, A18, A9, A14, A23, GRFUNC_1:8, NAT_1:13;
:: thesis: ( ( for a being Int-Location st a in UsedIntLoc I holds
(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 ) )
A24:
(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))))
by A7, A11, A21, A20, Th72, NAT_1:13;
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 A25:
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 A26:
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 A10, FUNCT_1:72
.=
(Computation t,(m + 1)) . a
by A18, A15, A24, A26, FUNCT_1:72
;
:: thesis: verum end; suppose A27:
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 A10, Th68
.=
(Computation t,m) . a
by A7, A11, A25, NAT_1:13
.=
(Computation t,(m + 1)) . a
by A18, A15, A27, 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 A28:
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 A29:
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 A10, FUNCT_1:72
.=
(Computation t,(m + 1)) . f
by A18, A15, A22, A29, FUNCT_1:72
;
:: thesis: verum end; suppose A30:
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 A10, Th70
.=
(Computation t,m) . f
by A7, A11, A28, NAT_1:13
.=
(Computation t,(m + 1)) . f
by A18, A15, A30, Th70
;
:: thesis: verum end;
end; end;
A31:
S1[ 0 ]
proof
A32:
IC (Computation t,0 ) =
IC t
by AMI_1:13
.=
insloc 0
by A2, Th67
;
A33:
IC (Computation s,0 ) =
IC s
by AMI_1:13
.=
insloc 0
by A1, Th67
;
assume
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 ) )
hence
IC (Computation t,0 ) in dom I
by A5, A33, A32;
:: 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 A33, A32;
:: 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 A35:
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 A35, FUNCT_1:72
.=
t . f
by A4, A35, FUNCT_1:72
.=
(Computation t,0 ) . f
by AMI_1:13
;
:: thesis: verum
end;
A36:
for m being Element of NAT holds S1[m]
from NAT_1:sch 1(A31, A6);
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 A37:
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 A38:
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 ) )A39:
IC (Computation t,0 ) =
IC t
by AMI_1:13
.=
insloc 0
by A2, Th67
;
IC (Computation s,0 ) =
IC s
by AMI_1:13
.=
insloc 0
by A1, Th67
;
hence
IC (Computation s,m) = IC (Computation t,m)
by A38, A39;
:: 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 A40:
a in UsedIntLoc I
;
:: thesis: (Computation s,m) . a = (Computation t,m) . athus (Computation s,m) . a =
s . a
by A38, AMI_1:13
.=
(s | (UsedIntLoc I)) . a
by A40, FUNCT_1:72
.=
t . a
by A3, A40, FUNCT_1:72
.=
(Computation t,m) . a
by A38, 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 A41:
f in UsedInt*Loc I
;
:: thesis: (Computation s,m) . f = (Computation t,m) . fthus (Computation s,m) . f =
s . f
by A38, AMI_1:13
.=
(s | (UsedInt*Loc I)) . f
by A41, FUNCT_1:72
.=
t . f
by A4, A41, FUNCT_1:72
.=
(Computation t,m) . f
by A38, 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 A42:
m = p + 1
;
reconsider p =
p as
Element of
NAT by ORDINAL1:def 13;
A43:
p < n
by A37, A42, NAT_1:13;
then A44:
IC (Computation s,p) in dom I
by A5;
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 A45:
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 A45, FUNCT_1:72
.=
(Computation t,p) . x
by A36, A43, A45
;
:: thesis: verum end; then A46:
(Computation s,p) | (UsedInt*Loc I) = (Computation t,p) | (UsedInt*Loc I)
by FUNCT_1:68;
set i =
(Computation s,p) . (IC (Computation s,p));
set p1 =
p + 1;
A47:
Computation s,
(p + 1) =
Following (Computation s,p)
by AMI_1:14
.=
Exec ((Computation s,p) . (IC (Computation s,p))),
(Computation s,p)
;
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 A48:
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 A48, FUNCT_1:72
.=
(Computation t,p) . x
by A36, A43, A48
;
:: thesis: verum end; then A49:
(Computation s,p) | (UsedIntLoc I) = (Computation t,p) | (UsedIntLoc I)
by FUNCT_1:68;
A50:
IC (Computation s,p) = IC (Computation t,p)
by A36, A43;
dom I misses dom (Start-At (insloc 0 ))
by Th64;
then A51:
I c= I +* (Start-At (insloc 0 ))
by FUNCT_4:33;
then
I c= s
by A1, XBOOLE_1:1;
then
I c= Computation s,
p
by AMI_1:81;
then A52:
(Computation s,p) . (IC (Computation s,p)) = I . (IC (Computation s,p))
by A44, GRFUNC_1:8;
A53:
Computation t,
(p + 1) =
Following (Computation t,p)
by AMI_1:14
.=
Exec ((Computation t,p) . (IC (Computation t,p))),
(Computation t,p)
;
I c= t
by A2, A51, XBOOLE_1:1;
then
I c= Computation t,
p
by AMI_1:81;
then A54:
(Computation s,p) . (IC (Computation s,p)) = (Computation t,p) . (IC (Computation t,p))
by A50, A44, A52, GRFUNC_1:8;
IC (Computation s,p) in dom I
by A5, A43;
then A55:
(Computation s,p) . (IC (Computation s,p)) in rng I
by A52, FUNCT_1:def 5;
then A56:
(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 Th39, RELAT_1:103
.=
(Computation t,p) | (UsedInt*Loc ((Computation s,p) . (IC (Computation s,p))))
by A55, A46, Th39, RELAT_1:103
;
A57:
(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 A55, Th23, RELAT_1:103
.=
(Computation t,p) | (UsedIntLoc ((Computation s,p) . (IC (Computation s,p))))
by A55, A49, Th23, RELAT_1:103
;
hence
IC (Computation s,m) = IC (Computation t,m)
by A42, A47, A53, A50, A54, A56, 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 ) )A58:
(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))))
by A50, A57, A56, Th72;
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 A59:
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 A60:
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 A42, A47, FUNCT_1:72
.=
(Computation t,m) . a
by A42, A53, A54, A58, A60, FUNCT_1:72
;
:: thesis: verum end; suppose A61:
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 A42, A47, Th68
.=
(Computation t,p) . a
by A36, A43, A59
.=
(Computation t,m) . a
by A42, A53, A54, A61, Th68
;
:: thesis: verum end;
end; A62:
(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))))
by A50, A57, A56, Th72;
hereby :: thesis: verum
let f be
FinSeq-Location ;
:: thesis: ( f in UsedInt*Loc I implies (Computation s,m) . b1 = (Computation t,m) . b1 )assume A63:
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 A64:
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 A42, A47, FUNCT_1:72
.=
(Computation t,m) . f
by A42, A53, A54, A62, A64, FUNCT_1:72
;
:: thesis: verum end; suppose A65:
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 A42, A47, Th70
.=
(Computation t,p) . f
by A36, A43, A63
.=
(Computation t,m) . f
by A42, A53, A54, A65, Th70
;
:: thesis: verum end;
end; end;