A1: (intloc (1 + 1)) := (intloc (2 + 1)) does_not_destroy intloc (3 + 1) by AMI_3:52, SCMFSA7B:12;
A2: SubFrom (intloc (2 + 1)),(intloc 0 ) does_not_destroy intloc (3 + 1) by AMI_3:52, SCMFSA7B:14;
A3: (intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)) does_not_destroy intloc (3 + 1) by AMI_3:52, SCMFSA7B:20;
A4: intloc (3 + 1) <> intloc (5 + 1) by AMI_3:52;
(((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) does_not_destroy intloc (3 + 1) by A1, A2, A3, SCMFSA8C:83, SCMFSA8C:84;
then ((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1))) does_not_destroy intloc (3 + 1) by A4, SCMFSA7B:20, SCMFSA8C:83;
then (((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((fsloc 0 ),(intloc (1 + 1)) := (intloc (5 + 1))) does_not_destroy intloc (3 + 1) by SCMFSA7B:21, SCMFSA8C:83;
hence ((((((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)))) ';' ((intloc (5 + 1)) := (fsloc 0 ),(intloc (2 + 1)))) ';' ((fsloc 0 ),(intloc (1 + 1)) := (intloc (5 + 1)))) ';' ((fsloc 0 ),(intloc (2 + 1)) := (intloc (4 + 1))) does_not_destroy intloc (3 + 1) by SCMFSA7B:21, SCMFSA8C:83; :: thesis: verum