let aa be Int-Location; :: thesis: for I being MacroInstruction of SCM+FSA st not I destroys aa holds
not I ';' (goto 0) destroys aa
let I be MacroInstruction of SCM+FSA ; :: thesis: ( not I destroys aa implies not I ';' (goto 0) destroys aa )
assume A1: not I destroys aa ; :: thesis: not I ';' (goto 0) destroys aa
not goto 0 destroys aa ;
then not Macro (goto 0) destroys aa by Th39;
then not I ';' (Macro (goto 0)) destroys aa by Lm1, A1;
hence not I ';' (goto 0) destroys aa by COMPOS_2:def 2; :: thesis: verum