intloc (0 + 1) <> intloc (1 + 1)
by AMI_3:52;
then A1:
Macro (SubFrom (intloc (1 + 1)),(intloc (1 + 1))) does_not_destroy intloc (0 + 1)
by SCMFSA7B:14, SCMFSA8C:77;
A2:
SubFrom (intloc (1 + 1)),(intloc 0 ) does_not_destroy intloc (0 + 1)
by AMI_3:52, SCMFSA7B:14;
AddTo (intloc (3 + 1)),(intloc 0 ) does_not_destroy intloc (0 + 1)
by AMI_3:52, SCMFSA7B:13;
then
(AddTo (intloc (3 + 1)),(intloc 0 )) ';' (SubFrom (intloc (1 + 1)),(intloc 0 )) does_not_destroy intloc (0 + 1)
by A2, SCMFSA8C:84;
then A3:
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 ))) does_not_destroy intloc (0 + 1)
by A1, SCMFSA8C:121;
A4:
SubFrom (intloc (4 + 1)),(intloc (5 + 1)) does_not_destroy intloc (0 + 1)
by AMI_3:52, SCMFSA7B:14;
(intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)) does_not_destroy intloc (0 + 1)
by AMI_3:52, SCMFSA7B:20;
then
((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) ';' (SubFrom (intloc (4 + 1)),(intloc (5 + 1))) does_not_destroy intloc (0 + 1)
by A4, SCMFSA8C:84;
hence
(((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 )))) does_not_destroy intloc (0 + 1)
by A3, SCMFSA8C:81; verum