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;

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;

end;

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:70, A12;

end;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:70, A12;

per cases then
( x = l or x = (IC s2) + 1 )
;

end;

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

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

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

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

then A32:
s2 = IncIC ((s2 +* v),((card (Macro (a =0_goto l))) -' 1))
by A26, A27, FUNCT_1:2;
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 )} ;

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

end;

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

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

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