A1: intloc (3 + 1) <> intloc (5 + 1) by AMI_3:52;
A2: not (intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1)) destroysdestroy intloc (3 + 1) by AMI_3:52, SCMFSA7B:20;
A3: not SubFrom (intloc (2 + 1)),(intloc 0 ) destroysdestroy intloc (3 + 1) by AMI_3:52, SCMFSA7B:14;
not (intloc (1 + 1)) := (intloc (2 + 1)) destroysdestroy intloc (3 + 1) by AMI_3:52, SCMFSA7B:12;
then not (((intloc (1 + 1)) := (intloc (2 + 1))) ';' (SubFrom (intloc (2 + 1)),(intloc 0 ))) ';' ((intloc (4 + 1)) := (fsloc 0 ),(intloc (1 + 1))) destroysdestroy intloc (3 + 1) by A3, A2, SCMFSA8C:83, SCMFSA8C:84;
then not ((((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))) destroysdestroy intloc (3 + 1) by A1, SCMFSA7B:20, SCMFSA8C:83;
then not (((((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))) destroysdestroy intloc (3 + 1) by SCMFSA7B:21, SCMFSA8C:83;
hence not ((((((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))) destroysdestroy intloc (3 + 1) by SCMFSA7B:21, SCMFSA8C:83; :: thesis: verum