A1:
not (intloc (3 + 1)) := (intloc (2 + 1)) destroys intloc (1 + 1)
by SCMFSA7B:6, SCMFSA_2:101;
A2:
not SubFrom ((intloc (2 + 1)),(intloc 0)) destroys intloc (1 + 1)
by SCMFSA7B:8, SCMFSA_2:101;
A3:
not (intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1))) destroys intloc (1 + 1)
by SCMFSA7B:14, SCMFSA_2:101;
A4:
not (intloc (5 + 1)) := ((fsloc 0),(intloc (3 + 1))) destroys intloc (1 + 1)
by SCMFSA7B:14, SCMFSA_2:101;
A5:
not ((fsloc 0),(intloc (2 + 1))) := (intloc (5 + 1)) destroys intloc (1 + 1)
by SCMFSA7B:15;
A6:
not ((fsloc 0),(intloc (3 + 1))) := (intloc (4 + 1)) destroys intloc (1 + 1)
by SCMFSA7B:15;
A7:
not Stop SCM+FSA destroys intloc (1 + 1)
by SCMFSA8C:56;
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 (1 + 1)
by A4, A5, A6, SCMFSA8C:54, SCMFSA8C:55;
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 (1 + 1)
by A7, SCMFSA8C:88;
not (((intloc (3 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),(intloc 0)))) ";" ((intloc (4 + 1)) := ((fsloc 0),(intloc (2 + 1)))) destroys intloc (1 + 1)
by A1, A2, A3, SCMFSA8C:54, SCMFSA8C:55;
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 (1 + 1)
by Lm13, SCMFSA7B:14, SCMFSA8C:54;
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 (1 + 1)
by Lm13, SCMFSA7B:8, SCMFSA8C:54;
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 (1 + 1)
by A8, SCMFSA8C:52; verum