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