let a, b be Int-Location; for s being State of SCM+FSA holds
( (Exec ((SubFrom (a,b)),s)) . (IC ) = (IC s) + 1 & (Exec ((SubFrom (a,b)),s)) . a = (s . a) - (s . b) & ( for c being Int-Location st c <> a holds
(Exec ((SubFrom (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((SubFrom (a,b)),s)) . f = s . f ) )
let s be State of SCM+FSA; ( (Exec ((SubFrom (a,b)),s)) . (IC ) = (IC s) + 1 & (Exec ((SubFrom (a,b)),s)) . a = (s . a) - (s . b) & ( for c being Int-Location st c <> a holds
(Exec ((SubFrom (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((SubFrom (a,b)),s)) . f = s . f ) )
consider A, B being Data-Location such that
A1:
a = A
and
A2:
b = B
and
A3:
SubFrom (a,b) = SubFrom (A,B)
by Def8;
reconsider S = s | SCM-Memory as State of SCM by Th42;
A4:
Exec ((SubFrom (a,b)),s) = s +* (Exec ((SubFrom (A,B)),S))
by A3, Th44;
hence (Exec ((SubFrom (a,b)),s)) . (IC ) =
(Exec ((SubFrom (A,B)),S)) . (IC )
by Th46
.=
(IC S) + 1
by AMI_3:4
.=
(IC s) + 1
by Th55
;
( (Exec ((SubFrom (a,b)),s)) . a = (s . a) - (s . b) & ( for c being Int-Location st c <> a holds
(Exec ((SubFrom (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((SubFrom (a,b)),s)) . f = s . f ) )
thus (Exec ((SubFrom (a,b)),s)) . a =
(Exec ((SubFrom (A,B)),S)) . A
by A1, A4, Th47
.=
(S . A) - (S . B)
by AMI_3:4
.=
(S . A) - (s . b)
by A2, Th48
.=
(s . a) - (s . b)
by A1, Th48
; ( ( for c being Int-Location st c <> a holds
(Exec ((SubFrom (a,b)),s)) . c = s . c ) & ( for f being FinSeq-Location holds (Exec ((SubFrom (a,b)),s)) . f = s . f ) )
hereby for f being FinSeq-Location holds (Exec ((SubFrom (a,b)),s)) . f = s . f
let c be
Int-Location;
( c <> a implies (Exec ((SubFrom (a,b)),s)) . c = s . c )assume A5:
c <> a
;
(Exec ((SubFrom (a,b)),s)) . c = s . creconsider C =
c as
Data-Location by Th5;
thus (Exec ((SubFrom (a,b)),s)) . c =
(Exec ((SubFrom (A,B)),S)) . C
by A4, Th47
.=
S . C
by A1, A5, AMI_3:4
.=
s . c
by Th48
;
verum
end;
let f be FinSeq-Location ; (Exec ((SubFrom (a,b)),s)) . f = s . f
A6:
not f in dom (Exec ((SubFrom (A,B)),S))
by Th37;
thus
(Exec ((SubFrom (a,b)),s)) . f = s . f
by A4, A6, FUNCT_4:11; verum