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 (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 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 A9, NAT_1:14;
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 A8, XBOOLE_0:3;
((Macro (a >0_goto l)) ';' I) /. f = (CutLastLoc (Macro (a >0_goto l))) . 0 by A10, FUNCT_4:11, A11, A7
.= 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 SCMFSA_2:71, A12;

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 A1, XXREAL_0:2;
hence x in dom ((Macro (a >0_goto l)) ';' I) by AFINSQ_1:66, A13; :: 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 A9, VALUED_1:38;
then f + 1 < card (Macro (a >0_goto l)) by XREAL_1:20;
then A15: x in dom (Macro (a >0_goto l)) by A14, AFINSQ_1:66;
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 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

proof

let a be object ; :: thesis: ( a in dom s2 implies s2 . a = ((s2 +* v) +* ((IC ) .--> ((IC (s2 +* v)) + ((card (Macro (a >0_goto l))) -' 1)))) . a )
assume a in dom s2 ; :: thesis: s2 . a = ((s2 +* v) +* ((IC ) .--> ((IC (s2 +* v)) + ((card (Macro (a >0_goto l))) -' 1)))) . a
A28: dom ((IC ) .--> ((IC (s2 +* v)) + ((card (Macro (a >0_goto l))) -' 1))) = {(IC )} ;

per cases ( a = IC or a <> IC ) ;

suppose A29: a = IC ; :: thesis: s2 . a = ((s2 +* v) +* ((IC ) .--> ((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 A6, A17, A25, A23, A24, FUNCT_4:13
.= ((IC ) .--> ((IC (s2 +* v)) + ((card (Macro (a >0_goto l))) -' 1))) . a by A29, FUNCOP_1:72
.= ((s2 +* v) +* ((IC ) .--> ((IC (s2 +* v)) + ((card (Macro (a >0_goto l))) -' 1)))) . a by A24, A28, A29, FUNCT_4:13 ;
:: thesis: verum

end;

suppose A30: a <> IC ; :: thesis: s2 . a = ((s2 +* v) +* ((IC ) .--> ((IC (s2 +* v)) + ((card (Macro (a >0_goto l))) -' 1)))) . a

then A31: not a in dom ((IC ) .--> ((IC (s2 +* v)) + ((card (Macro (a >0_goto l))) -' 1))) by TARSKI:def 1;
not a in dom ((IC ) .--> m) by A30, TARSKI:def 1;
then (s2 +* v) . a = s2 . a by FUNCT_4:11;
hence s2 . a = ((s2 +* v) +* ((IC ) .--> ((IC (s2 +* v)) + ((card (Macro (a >0_goto l))) -' 1)))) . a by A31, FUNCT_4:11; :: thesis: verum

end;

end;

end;

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; :: thesis: verum

end;

end;