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