let I be Program of ; :: thesis: for a, b being Int-Location st not I destroys b & a <> b holds
not Times (a,I) destroys b
let a, b be Int-Location ; :: thesis: ( not I destroys b & a <> b implies not Times (a,I) destroys b )
assume that
A1: not I destroys b and
A2: a <> b ; :: thesis: not Times (a,I) destroys 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 destroys b by SCMFSA8C:57;
not I ';' (SubFrom (a,(intloc 0))) destroys b by A1, A2, SCMFSA7B:8, SCMFSA8C:54;
then not if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0))))) destroys b by A3, SCMFSA8C:88;
then A4: not loop (if=0 (a,(Goto 2),(I ';' (SubFrom (a,(intloc 0)))))) destroys b by SCMFSA8C:74;
not Stop SCM+FSA destroys b by SCMFSA8C:56;
hence not Times (a,I) destroys b by A4, SCMFSA8C:88; :: thesis: verum