intloc (0 + 1) <> intloc (1 + 1)
by SCMFSA_2:101;
then A1:
not Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1)))) destroys intloc (0 + 1)
by SCMFSA7B:8, SCMFSA8C:48;
A2:
not SubFrom ((intloc (1 + 1)),(intloc 0)) destroys intloc (0 + 1)
by SCMFSA7B:8, SCMFSA_2:101;
not AddTo ((intloc (3 + 1)),(intloc 0)) destroys intloc (0 + 1)
by SCMFSA7B:7, SCMFSA_2:101;
then
not (AddTo ((intloc (3 + 1)),(intloc 0))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0))) destroys intloc (0 + 1)
by A2, SCMFSA8C:55;
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:88;
A4:
not SubFrom ((intloc (4 + 1)),(intloc (5 + 1))) destroys intloc (0 + 1)
by SCMFSA7B:8, SCMFSA_2:101;
not (intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1))) destroys intloc (0 + 1)
by SCMFSA7B:14, SCMFSA_2:101;
then
not ((intloc (4 + 1)) := ((fsloc 0),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1)))) destroys intloc (0 + 1)
by A4, SCMFSA8C:55;
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:52; verum