let aa, bb be Int-Location; :: thesis: for I being MacroInstruction of SCM+FSA st not I destroys aa holds
not if=0 (bb,(I ';' (goto 0))) destroys aa
let I be MacroInstruction of SCM+FSA ; :: thesis: ( not I destroys aa implies not if=0 (bb,(I ';' (goto 0))) destroys aa )
set i = bb =0_goto 3;
set Mi = Macro (bb =0_goto 3);
set IG = I ';' (goto 0);
A1: not Stop SCM+FSA destroys aa by Th47;
assume not I destroys aa ; :: thesis: not if=0 (bb,(I ';' (goto 0))) destroys aa
then A2: not I ';' (goto 0) destroys aa by Lm2;
A3: not Goto ((card (I ';' (goto 0))) + 1) destroys aa by Th48;
not bb =0_goto 3 destroys aa ;
then not (bb =0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1)) destroys aa by A3, Th44;
then not ((bb =0_goto 3) ";" (Goto ((card (I ';' (goto 0))) + 1))) ";" (I ';' (goto 0)) destroys aa by A2, Th43;
hence not if=0 (bb,(I ';' (goto 0))) destroys aa by A1, Th43; :: thesis: verum