let I be really-closed MacroInstruction of SCM+FSA ; for a being Int-Location
for k being Nat st k <= card I holds
(Macro (a >0_goto k)) ';' I is really-closed
let a be Int-Location; for k being Nat st k <= card I holds
(Macro (a >0_goto k)) ';' I is really-closed
let l be Nat; ( l <= card I implies (Macro (a >0_goto l)) ';' I is really-closed )
assume A1:
l <= card I
; (Macro (a >0_goto l)) ';' I is really-closed
set F = Macro (a >0_goto l);
set G = I;
set S = SCM+FSA ;
set P = (Macro (a >0_goto l)) ';' I;
set k = (card (Macro (a >0_goto l))) -' 1;
let f be Nat; AMISTD_1:def 9 ( not f in K543(NAT,((Macro (a >0_goto l)) ';' I)) or NIC ((((Macro (a >0_goto l)) ';' I) /. f),f) c= K543(NAT,((Macro (a >0_goto l)) ';' I)) )
assume A2:
f in dom ((Macro (a >0_goto l)) ';' I)
; NIC ((((Macro (a >0_goto l)) ';' I) /. f),f) c= K543(NAT,((Macro (a >0_goto l)) ';' I))
A3:
dom ((Macro (a >0_goto l)) ';' I) = (dom (CutLastLoc (Macro (a >0_goto l)))) \/ (dom (Reloc (I,((card (Macro (a >0_goto l))) -' 1))))
by FUNCT_4:def 1;
A4:
dom (Reloc (I,((card (Macro (a >0_goto l))) -' 1))) = { (m + ((card (Macro (a >0_goto l))) -' 1)) where m is Nat : m in dom (IncAddr (I,((card (Macro (a >0_goto l))) -' 1))) }
by VALUED_1:def 12;
let x be object ; TARSKI:def 3 ( not x in NIC ((((Macro (a >0_goto l)) ';' I) /. f),f) or x in K543(NAT,((Macro (a >0_goto l)) ';' I)) )
assume
x in NIC ((((Macro (a >0_goto l)) ';' I) /. f),f)
; x in K543(NAT,((Macro (a >0_goto l)) ';' I))
then consider s2 being Element of product (the_Values_of SCM+FSA) such that
A5:
x = IC (Exec ((((Macro (a >0_goto l)) ';' I) /. f),s2))
and
A6:
IC s2 = f
;
A7:
((Macro (a >0_goto l)) ';' I) /. f = ((Macro (a >0_goto l)) ';' I) . f
by A2, PARTFUN1:def 6;
per cases
( f in dom (CutLastLoc (Macro (a >0_goto l))) or f in dom (Reloc (I,((card (Macro (a >0_goto l))) -' 1))) )
by A2, A3, XBOOLE_0:def 3;
suppose A16:
f in dom (Reloc (I,((card (Macro (a >0_goto l))) -' 1)))
;
x in K543(NAT,((Macro (a >0_goto l)) ';' I))then consider m being
Nat such that A17:
f = m + ((card (Macro (a >0_goto l))) -' 1)
and A18:
m in dom (IncAddr (I,((card (Macro (a >0_goto l))) -' 1)))
by A4;
A19:
m in dom I
by A18, COMPOS_1:def 21;
then A20:
NIC (
(I /. m),
m)
c= dom I
by AMISTD_1:def 9;
A21:
Values (IC ) = NAT
by MEMSTR_0:def 6;
reconsider m =
m as
Element of
NAT by ORDINAL1:def 12;
reconsider v =
(IC ) .--> m as
PartState of
SCM+FSA by A21;
set s1 =
s2 +* v;
A22:
((Macro (a >0_goto l)) ';' I) /. f =
(Reloc (I,((card (Macro (a >0_goto l))) -' 1))) . f
by A7, A16, FUNCT_4:13
.=
(IncAddr (I,((card (Macro (a >0_goto l))) -' 1))) . m
by A17, A18, VALUED_1:def 12
;
A23:
((IC ) .--> m) . (IC ) = m
by FUNCOP_1:72;
A24:
IC in {(IC )}
by TARSKI:def 1;
A25:
dom ((IC ) .--> m) = {(IC )}
;
reconsider w =
(IC ) .--> ((IC (s2 +* v)) + ((card (Macro (a >0_goto l))) -' 1)) as
PartState of
SCM+FSA by A21;
A26:
dom ((s2 +* v) +* ((IC ) .--> ((IC (s2 +* v)) + ((card (Macro (a >0_goto l))) -' 1)))) = the
carrier of
SCM+FSA
by PARTFUN1:def 2;
A27:
dom s2 = the
carrier of
SCM+FSA
by PARTFUN1:def 2;
for
a being
object st
a in dom s2 holds
s2 . a = ((s2 +* v) +* ((IC ) .--> ((IC (s2 +* v)) + ((card (Macro (a >0_goto l))) -' 1)))) . a
then A32:
s2 = IncIC (
(s2 +* v),
((card (Macro (a >0_goto l))) -' 1))
by A26, A27, FUNCT_1:2;
set s3 =
s2 +* v;
A33:
IC (s2 +* v) = m
by A23, A24, A25, FUNCT_4:13;
reconsider s3 =
s2 +* v as
Element of
product (the_Values_of SCM+FSA) by CARD_3:107;
reconsider k =
(card (Macro (a >0_goto l))) -' 1,
m =
m as
Element of
NAT ;
A34:
x =
IC (Exec ((IncAddr ((I /. m),k)),s2))
by A5, A19, A22, COMPOS_1:def 21
.=
(IC (Exec ((I /. m),s3))) + k
by A32, AMISTD_2:7
;
IC (Exec ((I /. m),s3)) in NIC (
(I /. m),
m)
by A33;
then
IC (Exec ((I /. m),s3)) in dom I
by A20;
then
IC (Exec ((I /. m),s3)) in dom (IncAddr (I,k))
by COMPOS_1:def 21;
then
x in dom (Reloc (I,k))
by A4, A34;
hence
x in K543(
NAT,
((Macro (a >0_goto l)) ';' I))
by A3, XBOOLE_0:def 3;
verum end; end;