let I be really-closed MacroInstruction of SCM+FSA ; :: thesis: for a being Int-Location

for k being Nat st k <= card I holds

(a =0_goto k) ";" I is really-closed

let a be Int-Location; :: thesis: for k being Nat st k <= card I holds

(a =0_goto k) ";" I is really-closed

let k be Nat; :: thesis: ( k <= card I implies (a =0_goto k) ";" I is really-closed )

assume A1: k <= card I ; :: thesis: (a =0_goto k) ";" I is really-closed

A2: (a =0_goto k) ";" I = (stop ((Macro (a =0_goto k)) ';' (Goto 1))) ';' I by Lm4

.= ((Macro (a =0_goto k)) ';' (Macro (goto 1))) ';' I by Lm5

.= (Macro (a =0_goto k)) ';' ((Macro (goto 1)) ';' I) by COMPOS_1:29 ;

A3: card ((Macro (goto 1)) ';' I) = ((card (Macro (goto 1))) + (card I)) - 1 by COMPOS_1:20

.= (2 + (card I)) - 1 by COMPOS_1:56 ;

card I <= (card I) + 1 by NAT_1:11;

then A4: k <= card ((Macro (goto 1)) ';' I) by A3, A1, XXREAL_0:2;

0 + 1 <= card I by NAT_1:13;

then (Macro (goto 1)) ';' I is really-closed by Th24;

hence (a =0_goto k) ";" I is really-closed by A4, A2, Th27; :: thesis: verum

for k being Nat st k <= card I holds

(a =0_goto k) ";" I is really-closed

let a be Int-Location; :: thesis: for k being Nat st k <= card I holds

(a =0_goto k) ";" I is really-closed

let k be Nat; :: thesis: ( k <= card I implies (a =0_goto k) ";" I is really-closed )

assume A1: k <= card I ; :: thesis: (a =0_goto k) ";" I is really-closed

A2: (a =0_goto k) ";" I = (stop ((Macro (a =0_goto k)) ';' (Goto 1))) ';' I by Lm4

.= ((Macro (a =0_goto k)) ';' (Macro (goto 1))) ';' I by Lm5

.= (Macro (a =0_goto k)) ';' ((Macro (goto 1)) ';' I) by COMPOS_1:29 ;

A3: card ((Macro (goto 1)) ';' I) = ((card (Macro (goto 1))) + (card I)) - 1 by COMPOS_1:20

.= (2 + (card I)) - 1 by COMPOS_1:56 ;

card I <= (card I) + 1 by NAT_1:11;

then A4: k <= card ((Macro (goto 1)) ';' I) by A3, A1, XXREAL_0:2;

0 + 1 <= card I by NAT_1:13;

then (Macro (goto 1)) ';' I is really-closed by Th24;

hence (a =0_goto k) ";" I is really-closed by A4, A2, Th27; :: thesis: verum