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;

(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;

end;

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;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

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

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;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

then A29:
s2 = IncIC ((s2 +* v),((card (Macro (goto l))) -' 1))
by A23, A24, FUNCT_1:2;
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 )} ;

end;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 )
;

end;

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;.= ((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

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;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

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