intloc (0 + 1) <> intloc (1 + 1)
by AMI_3:52;
then A1:
not Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1))) destroysdestroy intloc (0 + 1)
by SCMFSA7B:14, SCMFSA8C:77;
A2:
not SubFrom (intloc (1 + 1)),(intloc 0 ) destroysdestroy intloc (0 + 1)
by AMI_3:52, SCMFSA7B:14;
not AddTo (intloc (3 + 1)),(intloc 0 ) destroysdestroy intloc (0 + 1)
by AMI_3:52, SCMFSA7B:13;
then
not (AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )) destroysdestroy intloc (0 + 1)
by A2, SCMFSA8C:84;
then A3:
not if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))) destroysdestroy intloc (0 + 1)
by A1, SCMFSA8C:121;
A4:
not SubFrom (intloc (4 + 1)),(intloc (5 + 1)) destroysdestroy intloc (0 + 1)
by AMI_3:52, SCMFSA7B:14;
not (intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)) destroysdestroy intloc (0 + 1)
by AMI_3:52, SCMFSA7B:20;
then
not ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1))) destroysdestroy intloc (0 + 1)
by A4, SCMFSA8C:84;
hence
not (((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1)))) ';' (if>0 (intloc (4 + 1)),(Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1)))),((AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )))) destroysdestroy intloc (0 + 1)
by A3, SCMFSA8C:81; verum