A1: intloc (0 + 1) <> intloc (5 + 1) by SCMFSA_2:101;
A2: not (intloc (4 + 1)) := ((),(intloc (1 + 1))) destroys intloc (0 + 1) by ;
A3: not SubFrom ((intloc (2 + 1)),()) destroys intloc (0 + 1) by ;
not (intloc (1 + 1)) := (intloc (2 + 1)) destroys intloc (0 + 1) by ;
then not (((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1)))) destroys intloc (0 + 1) by ;
then not ((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1)))) destroys intloc (0 + 1) by ;
then not (((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1))) destroys intloc (0 + 1) by ;
hence not ((((((intloc (1 + 1)) := (intloc (2 + 1))) ";" (SubFrom ((intloc (2 + 1)),()))) ";" ((intloc (4 + 1)) := ((),(intloc (1 + 1))))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (((),(intloc (1 + 1))) := (intloc (5 + 1)))) ";" (((),(intloc (2 + 1))) := (intloc (4 + 1))) destroys intloc (0 + 1) by ; :: thesis: verum