set P = F ';' G;
set k = (card F) -' 1;
let f be Instruction-Location of S; :: according to AMISTD_1:def 17 :: thesis: ( not f in dom (F ';' G) or NIC (pi (F ';' G),f),f c= dom (F ';' G) )
assume A1:
f in dom (F ';' G)
; :: thesis: NIC (pi (F ';' G),f),f c= dom (F ';' G)
A2:
dom (F ';' G) = (dom (CutLastLoc F)) \/ (dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)))
by FUNCT_4:def 1;
dom (CutLastLoc F) misses dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))
by Th50;
then A3:
(dom (CutLastLoc F)) /\ (dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))) = {}
by XBOOLE_0:def 7;
A4:
dom (CutLastLoc F) c= dom F
by GRFUNC_1:8;
A5:
dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) = { (il. S,(m + ((card F) -' 1))) where m is Element of NAT : il. S,m in dom (IncAddr G,((card F) -' 1)) }
by Def16;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in NIC (pi (F ';' G),f),f or x in dom (F ';' G) )
assume
x in NIC (pi (F ';' G),f),f
; :: thesis: x in dom (F ';' G)
then consider s2 being State of S such that
A6:
x = IC (Following s2)
and
A7:
IC s2 = f
and
A8:
s2 . f = pi (F ';' G),f
;
A9:
pi (F ';' G),f = (F ';' G) . f
by A1, AMI_1:def 47;
per cases
( f in dom (CutLastLoc F) or f in dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) )
by A1, A2, XBOOLE_0:def 3;
suppose A10:
f in dom (CutLastLoc F)
;
:: thesis: x in dom (F ';' G)then A11:
NIC (pi F,f),
f c= dom F
by A4, AMISTD_1:def 17;
not
f in dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))
by A3, A10, XBOOLE_0:def 4;
then s2 . f =
(CutLastLoc F) . f
by A8, A9, FUNCT_4:12
.=
F . f
by A10, GRFUNC_1:8
.=
pi F,
f
by A4, A10, AMI_1:def 47
;
then
IC (Following s2) in NIC (pi F,f),
f
by A7;
then A12:
x in dom F
by A6, A11;
dom F c= dom (F ';' G)
by Th53;
hence
x in dom (F ';' G)
by A12;
:: thesis: verum end; suppose A13:
f in dom (Shift (IncAddr G,((card F) -' 1)),((card F) -' 1))
;
:: thesis: x in dom (F ';' G)then consider m being
Element of
NAT such that A14:
f = il. S,
(m + ((card F) -' 1))
and A15:
il. S,
m in dom (IncAddr G,((card F) -' 1))
by A5;
A16:
il. S,
m in dom G
by A15, Def15;
then A17:
NIC (pi G,(il. S,m)),
(il. S,m) c= dom G
by AMISTD_1:def 17;
A18:
ObjectKind (IC S) = NAT
by AMI_1:def 11;
il. S,
m in NAT
by AMI_1:def 4;
then reconsider v =
(IC S) .--> (il. S,m) as
FinPartState of
S by A18, AMI_1:59;
set s1 =
s2 +* v;
A19:
pi (F ';' G),
f =
(Shift (IncAddr G,((card F) -' 1)),((card F) -' 1)) . f
by A9, A13, FUNCT_4:14
.=
(IncAddr G,((card F) -' 1)) . (il. S,m)
by A14, A15, Def16
;
A20:
((IC S) .--> (il. S,m)) . (IC S) = il. S,
m
by FUNCOP_1:87;
A21:
IC S in {(IC S)}
by TARSKI:def 1;
A22:
dom ((IC S) .--> (il. S,m)) = {(IC S)}
by FUNCOP_1:19;
then A23:
IC (s2 +* v) = il. S,
m
by A20, A21, FUNCT_4:14;
(IC (s2 +* v)) + ((card F) -' 1) in NAT
by AMI_1:def 4;
then reconsider w =
(IC S) .--> ((IC (s2 +* v)) + ((card F) -' 1)) as
FinPartState of
S by A18, AMI_1:59;
(s2 +* v) +* w is
State of
S
;
then A25:
dom ((s2 +* v) +* ((IC S) .--> ((IC (s2 +* v)) + ((card F) -' 1)))) = the
carrier of
S
by AMI_1:79;
for
a being
set st
a in dom s2 holds
s2 . a = ((s2 +* v) +* ((IC S) .--> ((IC (s2 +* v)) + ((card F) -' 1)))) . a
then A30:
s2 = (s2 +* v) +* ((IC S) .--> ((IC (s2 +* v)) + ((card F) -' 1)))
by A25, AMI_1:79, FUNCT_1:9;
set s3 =
(s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m)));
A31:
dom ((il. S,m) .--> (pi G,(il. S,m))) = {(il. S,m)}
by FUNCOP_1:19;
then A32:
il. S,
m in dom ((il. S,m) .--> (pi G,(il. S,m)))
by TARSKI:def 1;
then A33:
IC ((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m)))) =
(s2 +* v) . (IC S)
by FUNCT_4:12
.=
il. S,
m
by A20, A21, A22, FUNCT_4:14
;
A34:
((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m)))) . (il. S,m) =
((il. S,m) .--> (pi G,(il. S,m))) . (il. S,m)
by A32, FUNCT_4:14
.=
pi G,
(il. S,m)
by FUNCOP_1:87
;
s2 +* v,
(s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m))) equal_outside NAT
proof
A35:
(
dom (s2 +* v) = the
carrier of
S &
dom ((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m)))) = the
carrier of
S )
by AMI_1:79;
for
x being
set st
x in (dom (s2 +* v)) \ NAT holds
(s2 +* v) . x = ((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m)))) . x
proof
let x be
set ;
:: thesis: ( x in (dom (s2 +* v)) \ NAT implies (s2 +* v) . x = ((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m)))) . x )
A36:
dom ((il. S,m) .--> (pi G,(il. S,m))) c= NAT
by RELAT_1:def 18;
assume
x in (dom (s2 +* v)) \ NAT
;
:: thesis: (s2 +* v) . x = ((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m)))) . x
then
not
x in dom ((il. S,m) .--> (pi G,(il. S,m)))
by A36, XBOOLE_0:def 5;
hence
(s2 +* v) . x = ((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m)))) . x
by FUNCT_4:12;
:: thesis: verum
end;
hence
(s2 +* v) | ((dom (s2 +* v)) \ NAT ) = ((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m)))) | ((dom ((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m))))) \ NAT )
by A35, FUNCT_1:165;
:: according to FUNCT_7:def 2 :: thesis: verum
end; then A37:
Exec (pi G,(il. S,m)),
(s2 +* v),
Exec (pi G,(il. S,m)),
((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m)))) equal_outside NAT
by Def19;
reconsider k =
(card F) -' 1,
m =
m as
Element of
NAT ;
A38:
x =
IC (Exec (IncAddr (pi G,(il. S,m)),k),s2)
by A6, A7, A8, A16, A19, Def15
.=
(IC (Exec (pi G,(il. S,m)),(s2 +* v))) + k
by A30, Def17
.=
il. S,
((locnum (IC (Exec (pi G,(il. S,m)),((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m))))))) + k)
by A37, AMI_1:121
;
IC (Following ((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m))))) = il. S,
(locnum (IC (Exec (pi G,(il. S,m)),((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m)))))))
by A33, A34, AMISTD_1:def 13;
then
il. S,
(locnum (IC (Exec (pi G,(il. S,m)),((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m))))))) in NIC (pi G,(il. S,m)),
(il. S,m)
by A33, A34;
then
il. S,
(locnum (IC (Exec (pi G,(il. S,m)),((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m))))))) in dom G
by A17;
then A39:
il. S,
(locnum (IC (Exec (pi G,(il. S,m)),((s2 +* v) +* ((il. S,m) .--> (pi G,(il. S,m))))))) in dom (IncAddr G,k)
by Def15;
x in dom (Shift (IncAddr G,k),k)
by A5, A38, A39;
hence
x in dom (F ';' G)
by A2, XBOOLE_0:def 3;
:: thesis: verum end;