A1:
not (intloc (3 + 1)) := (intloc (2 + 1)) destroys intloc (0 + 1)
by SCMFSA7B:12, SCMFSA_2:128;
A2:
not SubFrom ((intloc (2 + 1)),(intloc 0)) destroys intloc (0 + 1)
by SCMFSA7B:14, SCMFSA_2:128;
A3:
not (intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))) destroys intloc (0 + 1)
by SCMFSA7B:20, SCMFSA_2:128;
A4:
not (intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))) destroys intloc (0 + 1)
by SCMFSA7B:20, SCMFSA_2:128;
A5:
not ((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)) destroys intloc (0 + 1)
by SCMFSA7B:21;
A6:
not ((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)) destroys intloc (0 + 1)
by SCMFSA7B:21;
A7:
not Stop SCM+FSA destroys 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))) destroys 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)) destroys 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)))) destroys 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)))) destroys 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)))) destroys 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))) destroys intloc (0 + 1)
by A8, SCMFSA8C:81; verum