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