let I be really-closed Program of ; :: thesis: for k being Nat st k <= card I holds
(Macro (goto k)) ';' I is really-closed
let l be Nat; :: thesis: ( l <= card I implies (Macro (goto l)) ';' I is really-closed )
assume A1: l <= card I ; :: thesis: (Macro (goto l)) ';' I is really-closed
set F = Macro (goto l);
set G = I;
set S = SCM+FSA ;
set P = (Macro (goto l)) ';' I;
set k = (card (Macro (goto l))) -' 1;
let f be Nat; :: according to AMISTD_1:def 9 :: thesis: ( not f in K543(NAT,((Macro (goto l)) ';' I)) or NIC ((((Macro (goto l)) ';' I) /. f),f) c= K543(NAT,((Macro (goto l)) ';' I)) )
assume A2: f in dom ((Macro (goto l)) ';' I) ; :: thesis: NIC ((((Macro (goto l)) ';' I) /. f),f) c= K543(NAT,((Macro (goto l)) ';' I))
A3: dom ((Macro (goto l)) ';' I) = (dom (CutLastLoc (Macro (goto l)))) \/ (dom (Reloc (I,((card (Macro (goto l))) -' 1)))) by FUNCT_4:def 1;
A4: dom (Reloc (I,((card (Macro (goto l))) -' 1))) = { (m + ((card (Macro (goto l))) -' 1)) where m is Nat : m in dom (IncAddr (I,((card (Macro (goto l))) -' 1))) } by VALUED_1:def 12;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in NIC ((((Macro (goto l)) ';' I) /. f),f) or x in K543(NAT,((Macro (goto l)) ';' I)) )
assume x in NIC ((((Macro (goto l)) ';' I) /. f),f) ; :: thesis: x in K543(NAT,((Macro (goto l)) ';' I))
then consider s2 being Element of product (the_Values_of SCM+FSA) such that
A5: x = IC (Exec ((((Macro (goto l)) ';' I) /. f),s2)) and
A6: IC s2 = f ;
A7: ((Macro (goto l)) ';' I) /. f = ((Macro (goto l)) ';' I) . f by A2, PARTFUN1:def 6;

per cases ( f in dom (CutLastLoc (Macro (goto l))) or f in dom (Reloc (I,((card (Macro (goto l))) -' 1))) ) by A2, A3, XBOOLE_0:def 3;

suppose A8: f in dom (CutLastLoc (Macro (goto l))) ; :: thesis: x in K543(NAT,((Macro (goto l)) ';' I))

then A9: f < card (CutLastLoc (Macro (goto l))) by AFINSQ_1:66;
card (CutLastLoc (Macro (goto l))) = (card (Macro (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 (goto l))) misses dom (Reloc (I,((card (Macro (goto l))) -' 1))) by COMPOS_1:18;
then A11: not f in dom (Reloc (I,((card (Macro (goto l))) -' 1))) by A8, XBOOLE_0:3;
((Macro (goto l)) ';' I) /. f = (CutLastLoc (Macro (goto l))) . 0 by A10, FUNCT_4:11, A11, A7
.= goto l ;
then A12: x = l by SCMFSA_2:69, A5;
card ((Macro (goto l)) ';' I) = ((card (Macro (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 (goto l)) ';' I) by XREAL_1:29;
then l < card ((Macro (goto l)) ';' I) by A1, XXREAL_0:2;
hence x in dom ((Macro (goto l)) ';' I) by AFINSQ_1:66, A12; :: thesis: verum

end;

suppose A13: f in dom (Reloc (I,((card (Macro (goto l))) -' 1))) ; :: thesis: x in K543(NAT,((Macro (goto l)) ';' I))

then consider m being Nat such that
A14: f = m + ((card (Macro (goto l))) -' 1) and
A15: m in dom (IncAddr (I,((card (Macro (goto l))) -' 1))) by A4;
A16: m in dom I by A15, COMPOS_1:def 21;
then A17: NIC ((I /. m),m) c= dom I by AMISTD_1:def 9;
A18: 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 A18;
set s1 = s2 +* v;
A19: ((Macro (goto l)) ';' I) /. f = (Reloc (I,((card (Macro (goto l))) -' 1))) . f by A7, A13, FUNCT_4:13
.= (IncAddr (I,((card (Macro (goto l))) -' 1))) . m by A14, A15, VALUED_1:def 12 ;
A20: ((IC ) .--> m) . (IC ) = m by FUNCOP_1:72;
A21: IC in {(IC )} by TARSKI:def 1;
A22: dom ((IC ) .--> m) = {(IC )} ;
reconsider w = (IC ) .--> ((IC (s2 +* v)) + ((card (Macro (goto l))) -' 1)) as PartState of SCM+FSA by A18;
A23: dom ((s2 +* v) +* ((IC ) .--> ((IC (s2 +* v)) + ((card (Macro (goto l))) -' 1)))) = the carrier of SCM+FSA by PARTFUN1:def 2;
A24: 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 (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 (goto l))) -' 1)))) . a )
assume a in dom s2 ; :: thesis: s2 . a = ((s2 +* v) +* ((IC ) .--> ((IC (s2 +* v)) + ((card (Macro (goto l))) -' 1)))) . a
A25: dom ((IC ) .--> ((IC (s2 +* v)) + ((card (Macro (goto l))) -' 1))) = {(IC )} ;

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

suppose A26: a = IC ; :: thesis: s2 . a = ((s2 +* v) +* ((IC ) .--> ((IC (s2 +* v)) + ((card (Macro (goto l))) -' 1)))) . a

hence s2 . a = (IC (s2 +* v)) + ((card (Macro (goto l))) -' 1) by A6, A14, A22, A20, A21, FUNCT_4:13
.= ((IC ) .--> ((IC (s2 +* v)) + ((card (Macro (goto l))) -' 1))) . a by A26, FUNCOP_1:72
.= ((s2 +* v) +* ((IC ) .--> ((IC (s2 +* v)) + ((card (Macro (goto l))) -' 1)))) . a by A21, A25, A26, FUNCT_4:13 ;
:: thesis: verum

end;

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

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

end;

end;

end;

then A29: s2 = IncIC ((s2 +* v),((card (Macro (goto l))) -' 1)) by A23, A24, FUNCT_1:2;
set s3 = s2 +* v;
A30: IC (s2 +* v) = m by A20, A21, A22, FUNCT_4:13;
reconsider s3 = s2 +* v as Element of product (the_Values_of SCM+FSA) by CARD_3:107;
reconsider k = (card (Macro (goto l))) -' 1, m = m as Element of NAT ;
A31: x = IC (Exec ((IncAddr ((I /. m),k)),s2)) by A5, A16, A19, COMPOS_1:def 21
.= (IC (Exec ((I /. m),s3))) + k by A29, AMISTD_2:7 ;
IC (Exec ((I /. m),s3)) in NIC ((I /. m),m) by A30;
then IC (Exec ((I /. m),s3)) in dom I by A17;
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, A31;
hence x in K543(NAT,((Macro (goto l)) ';' I)) by A3, XBOOLE_0:def 3; :: thesis: verum

end;

end;