A1: not (intloc (2 + 1)) := (intloc (1 + 1)) destroys intloc (0 + 1) by ;
A2: intloc (0 + 1) <> intloc (2 + 1) by SCMFSA_2:101;
A3: not SubFrom ((intloc (1 + 1)),(intloc (0 + 1))) destroys intloc (0 + 1) by ;
not (intloc (1 + 1)) :=len () destroys intloc (0 + 1) by ;
then not (((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1))) destroys intloc (0 + 1) by ;
then A4: not ((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),())) destroys intloc (0 + 1) by ;
A5: intloc (0 + 1) <> intloc (3 + 1) by SCMFSA_2:101;
intloc (0 + 1) <> intloc (5 + 1) by SCMFSA_2:101;
then not (((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1)))) destroys intloc (0 + 1) by ;
then A6: not ((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1)))) destroys intloc (0 + 1) by ;
not while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),()))))))) destroys intloc (0 + 1) by ;
then A7: not (((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))) ";" (while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())))))))) destroys intloc (0 + 1) by ;
not Times ((intloc (3 + 1)),(((((((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 ;
hence not ((((((((intloc (1 + 1)) :=len ()) ";" (SubFrom ((intloc (1 + 1)),(intloc (0 + 1))))) ";" ((intloc (2 + 1)) := (intloc (1 + 1)))) ";" (AddTo ((intloc (2 + 1)),()))) ";" ((intloc (5 + 1)) := ((),(intloc (2 + 1))))) ";" (SubFrom ((intloc (3 + 1)),(intloc (3 + 1))))) ";" (while>0 ((intloc (1 + 1)),((((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1))))) ";" (if>0 ((intloc (4 + 1)),(Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1))))),((AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),()))))))))) ";" (Times ((intloc (3 + 1)),(((((((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