let I be Program of SCM+FSA ; :: thesis: for a, b being Int-Location st not I destroysdestroy b & a <> b holds
not Times a,I destroysdestroy b
let a, b be Int-Location ; :: thesis: ( not I destroysdestroy b & a <> b implies not Times a,I destroysdestroy b )
assume that
A1: not I destroysdestroy b and
A2: a <> b ; :: thesis: not Times a,I destroysdestroy b
set Gi = Goto 2;
set Si = SubFrom a,(intloc 0 );
set SS = Stop SCM+FSA ;
set if0 = if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )));
A3: not Goto 2 destroysdestroy b by SCMFSA8C:86;
not I ';' (SubFrom a,(intloc 0 )) destroysdestroy b by A1, A2, SCMFSA7B:14, SCMFSA8C:83;
then not if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 ))) destroysdestroy b by A3, SCMFSA8C:121;
then A4: not loop (if=0 a,(Goto 2),(I ';' (SubFrom a,(intloc 0 )))) destroysdestroy b by SCMFSA8C:105;
not Stop SCM+FSA destroysdestroy b by SCMFSA8C:85;
hence not Times a,I destroysdestroy b by A4, SCMFSA8C:121; :: thesis: verum