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