let I be MacroInstruction of SCM+FSA ; :: 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 A1: not I destroys b ; :: thesis: ( not a <> b or not Times (a,I) destroys b )
assume a <> b ; :: thesis: not Times (a,I) destroys b
then not SubFrom (a,(intloc 0)) destroys b by SCMFSA7B:8;
then not I ";" (SubFrom (a,(intloc 0))) destroys b by A1, Th45;
then not while>0 (a,(I ";" (SubFrom (a,(intloc 0))))) destroys b by Th67;
hence not Times (a,I) destroys b ; :: thesis: verum