set J = Stop SCM+FSA;
let a be Int-Location; :: thesis: for I being MacroInstruction of SCM+FSA holds (while>0 (a,I)) . ((card I) + 2) = goto 0
let I be MacroInstruction of SCM+FSA ; :: thesis: (while>0 (a,I)) . ((card I) + 2) = goto 0
set I1 = I ';' (goto 0);
set Lc4 = (card I) + 2;
( (card I) + 2 in dom (while>0 (a,I)) & dom (while>0 (a,I)) = dom (if>0 (a,(I ';' (goto 0)))) ) by Th8, FUNCT_7:30;
hence (while>0 (a,I)) . ((card I) + 2) = goto 0 by FUNCT_7:31; :: thesis: verum