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