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 Th6, FUNCT_7:30;

hence (while=0 (a,I)) . ((card I) + 2) = goto 0 by FUNCT_7:31; :: thesis: verum

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 Th6, FUNCT_7:30;

hence (while=0 (a,I)) . ((card I) + 2) = goto 0 by FUNCT_7:31; :: thesis: verum