A1:
not (intloc (1 + 1)) := (intloc (0 + 1)) destroys intloc (0 + 1)
by SCMFSA7B:6, SCMFSA_2:101;
A2:
not SubFrom ((intloc (1 + 1)),(intloc 0)) destroys intloc (0 + 1)
by SCMFSA7B:8, SCMFSA_2:101;
A3:
not (intloc (2 + 1)) :=len (fsloc 0) destroys intloc (0 + 1)
by SCMFSA7B:16, SCMFSA_2:101;
A4:
not Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA))))) destroys intloc (0 + 1)
by Lm24, SCMFSA8C:93, SCMFSA_2:101;
not (((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))) ";" ((intloc (2 + 1)) :=len (fsloc 0)) destroys intloc (0 + 1)
by A1, A2, A3, SCMFSA8C:54, SCMFSA8C:55;
hence
not ((((intloc (1 + 1)) := (intloc (0 + 1))) ";" (SubFrom ((intloc (1 + 1)),(intloc 0)))) ";" ((intloc (2 + 1)) :=len (fsloc 0))) ";" (Times ((intloc (1 + 1)),(((((((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))))) ";" ((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))))) ";" (SubFrom ((intloc (5 + 1)),(intloc (4 + 1))))) ";" (if>0 ((intloc (5 + 1)),((((intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1)))) ";" (((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)))) ";" (((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)))),(Stop SCM+FSA)))))) destroys intloc (0 + 1)
by A4, SCMFSA8C:52; verum