let I be really-closed MacroInstruction of SCM+FSA ; :: thesis: 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; :: thesis: for k being Nat st k <= card I holds
(Macro (a >0_goto k)) ';' I is really-closed

let l be Nat; :: thesis: ( l <= card I implies (Macro (a >0_goto l)) ';' I is really-closed )
assume A1: l <= card I ; :: thesis: (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; :: according to AMISTD_1:def 9 :: thesis: ( 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) ; :: thesis: 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 ; :: according to TARSKI:def 3 :: thesis: ( 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) ; :: thesis: x in K543(NAT,((Macro (a >0_goto l)) ';' I))
then consider s2 being Element of product 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 ;
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 ;
suppose A8: f in dom (CutLastLoc (Macro (a >0_goto l))) ; :: thesis: x in K543(NAT,((Macro (a >0_goto l)) ';' I))
then A9: f < card (CutLastLoc (Macro (a >0_goto l))) by AFINSQ_1:66;
card (CutLastLoc (Macro (a >0_goto l))) = (card (Macro (a >0_goto l))) - 1 by VALUED_1:38
.= 2 - 1 by COMPOS_1:56 ;
then A10: f = 0 by ;
dom (CutLastLoc (Macro (a >0_goto l))) misses dom (Reloc (I,((card (Macro (a >0_goto l))) -' 1))) by COMPOS_1:18;
then A11: not f in dom (Reloc (I,((card (Macro (a >0_goto l))) -' 1))) by ;
((Macro (a >0_goto l)) ';' I) /. f = (CutLastLoc (Macro (a >0_goto l))) . 0 by
.= a >0_goto l ;
then A12: x = IC (Exec ((a >0_goto l),s2)) by A5;
( s2 . a = 0 or s2 . a <> 0 ) ;
then ( x = l or x = (IC s2) + 1 ) by ;
per cases then ( x = l or x = (IC s2) + 1 ) ;
suppose A13: x = l ; :: thesis: x in K543(NAT,((Macro (a >0_goto l)) ';' I))
card ((Macro (a >0_goto l)) ';' I) = ((card (Macro (a >0_goto l))) + (card I)) - 1 by COMPOS_1:20
.= (2 + (card I)) - 1 by COMPOS_1:56
.= (card I) + 1 ;
then card I < card ((Macro (a >0_goto l)) ';' I) by XREAL_1:29;
then l < card ((Macro (a >0_goto l)) ';' I) by ;
hence x in dom ((Macro (a >0_goto l)) ';' I) by ; :: thesis: verum
end;
suppose x = (IC s2) + 1 ; :: thesis: x in K543(NAT,((Macro (a >0_goto l)) ';' I))
then A14: x = f + 1 by A6;
f < (card (Macro (a >0_goto l))) - 1 by ;
then f + 1 < card (Macro (a >0_goto l)) by XREAL_1:20;
then A15: x in dom (Macro (a >0_goto l)) by ;
dom (Macro (a >0_goto l)) c= dom ((Macro (a >0_goto l)) ';' I) by COMPOS_1:21;
hence x in K543(NAT,((Macro (a >0_goto l)) ';' I)) by A15; :: thesis: verum
end;
end;
end;
suppose A16: f in dom (Reloc (I,((card (Macro (a >0_goto l))) -' 1))) ; :: thesis: 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 ;
then A20: NIC ((I /. m),m) c= dom I by AMISTD_1:def 9;
A21: Values () = NAT by MEMSTR_0:def 6;
reconsider m = m as Element of NAT by ORDINAL1:def 12;
reconsider v = () .--> 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
.= (IncAddr (I,((card (Macro (a >0_goto l))) -' 1))) . m by ;
A23: ((IC ) .--> m) . () = m by FUNCOP_1:72;
A24: IC in {()} by TARSKI:def 1;
A25: dom (() .--> m) = {()} ;
reconsider w = () .--> ((IC (s2 +* v)) + ((card (Macro (a >0_goto l))) -' 1)) as PartState of SCM+FSA by A21;
A26: dom ((s2 +* v) +* (() .--> ((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 (s2 +* v)) + ((card (Macro (a >0_goto l))) -' 1)))) . a
proof
let a be object ; :: thesis: ( a in dom s2 implies s2 . a = ((s2 +* v) +* (() .--> ((IC (s2 +* v)) + ((card (Macro (a >0_goto l))) -' 1)))) . a )
assume a in dom s2 ; :: thesis: s2 . a = ((s2 +* v) +* (() .--> ((IC (s2 +* v)) + ((card (Macro (a >0_goto l))) -' 1)))) . a
A28: dom (() .--> ((IC (s2 +* v)) + ((card (Macro (a >0_goto l))) -' 1))) = {()} ;
per cases ( a = IC or a <> IC ) ;
suppose A29: a = IC ; :: thesis: s2 . a = ((s2 +* v) +* (() .--> ((IC (s2 +* v)) + ((card (Macro (a >0_goto l))) -' 1)))) . a
hence s2 . a = (IC (s2 +* v)) + ((card (Macro (a >0_goto l))) -' 1) by
.= (() .--> ((IC (s2 +* v)) + ((card (Macro (a >0_goto l))) -' 1))) . a by
.= ((s2 +* v) +* (() .--> ((IC (s2 +* v)) + ((card (Macro (a >0_goto l))) -' 1)))) . a by ;
:: thesis: verum
end;
suppose A30: a <> IC ; :: thesis: s2 . a = ((s2 +* v) +* (() .--> ((IC (s2 +* v)) + ((card (Macro (a >0_goto l))) -' 1)))) . a
then A31: not a in dom (() .--> ((IC (s2 +* v)) + ((card (Macro (a >0_goto l))) -' 1))) by TARSKI:def 1;
not a in dom (() .--> m) by ;
then (s2 +* v) . a = s2 . a by FUNCT_4:11;
hence s2 . a = ((s2 +* v) +* (() .--> ((IC (s2 +* v)) + ((card (Macro (a >0_goto l))) -' 1)))) . a by ; :: thesis: verum
end;
end;
end;
then A32: s2 = IncIC ((s2 +* v),((card (Macro (a >0_goto l))) -' 1)) by ;
set s3 = s2 +* v;
A33: IC (s2 +* v) = m by ;
reconsider s3 = s2 +* v as Element of product 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
.= (IC (Exec ((I /. m),s3))) + k by ;
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 ;
hence x in K543(NAT,((Macro (a >0_goto l)) ';' I)) by ; :: thesis: verum
end;
end;