A1:
not (intloc (1 + 1)) := (intloc (0 + 1)) destroys intloc (0 + 1)
by SCMFSA7B:12, SCMFSA_2:128;
A2:
not SubFrom ((intloc (1 + 1)),(intloc 0)) destroys intloc (0 + 1)
by SCMFSA7B:14, SCMFSA_2:128;
A3:
not (intloc (2 + 1)) :=len (fsloc 0) destroys intloc (0 + 1)
by SCMFSA7B:22, SCMFSA_2:128;
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, Th3, SCMFSA_2:128;
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:83, SCMFSA8C:84;
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:81; verum