A1:
not (intloc (1 + 1)) := (intloc (0 + 1)) destroysdestroy intloc (0 + 1)
by AMI_3:52, SCMFSA7B:12;
A2:
not SubFrom (intloc (1 + 1)),(intloc 0 ) destroysdestroy intloc (0 + 1)
by AMI_3:52, SCMFSA7B:14;
A3:
not (intloc (2 + 1)) :=len (fsloc 0 ) destroysdestroy intloc (0 + 1)
by AMI_3:52, SCMFSA7B:22;
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 ))) destroysdestroy intloc (0 + 1)
by Lm24, Th3, AMI_3:52;
not (((intloc (1 + 1)) := (intloc (0 + 1))) ';' (SubFrom (intloc (1 + 1)),(intloc 0 ))) ';' ((intloc (2 + 1)) :=len (fsloc 0 )) destroysdestroy 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 )))) destroysdestroy intloc (0 + 1)
by A4, SCMFSA8C:81; verum