A1:
not (intloc (3 + 1)) := (intloc (2 + 1)) destroysdestroy intloc (0 + 1)
by AMI_3:52, SCMFSA7B:12;
A2:
not SubFrom (intloc (2 + 1)),(intloc 0 ) destroysdestroy intloc (0 + 1)
by AMI_3:52, SCMFSA7B:14;
A3:
not (intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1)) destroysdestroy intloc (0 + 1)
by AMI_3:52, SCMFSA7B:20;
A4:
not (intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1)) destroysdestroy intloc (0 + 1)
by AMI_3:52, SCMFSA7B:20;
A5:
not (fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)) destroysdestroy intloc (0 + 1)
by SCMFSA7B:21;
A6:
not (fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1)) destroysdestroy intloc (0 + 1)
by SCMFSA7B:21;
A7:
not Stop SCM+FSA destroysdestroy intloc (0 + 1)
by SCMFSA8C:85;
not (((intloc (5 + 1)) := (fsloc 0 ),(intloc (3 + 1))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (3 + 1)) := (intloc (4 + 1))) destroysdestroy intloc (0 + 1)
by A4, A5, A6, SCMFSA8C:83, SCMFSA8C:84;
then A8:
not 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 A7, SCMFSA8C:121;
not (((intloc (3 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (2 + 1))) destroysdestroy intloc (0 + 1)
by A1, A2, A3, SCMFSA8C:83, SCMFSA8C:84;
then
not ((((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))) destroysdestroy intloc (0 + 1)
by Lm9, SCMFSA7B:20, SCMFSA8C:83;
then
not (((((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))) destroysdestroy intloc (0 + 1)
by Lm9, SCMFSA7B:14, SCMFSA8C:83;
hence
not ((((((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 A8, SCMFSA8C:81; verum