intloc (0 + 1) <> intloc (1 + 1) by SCMFSA_2:101;
then A1: not Macro (SubFrom ((intloc (1 + 1)),(intloc (1 + 1)))) destroys intloc (0 + 1) by ;
A2: not SubFrom ((intloc (1 + 1)),()) destroys intloc (0 + 1) by ;
not AddTo ((intloc (3 + 1)),()) destroys intloc (0 + 1) by ;
then not (AddTo ((intloc (3 + 1)),())) ";" (SubFrom ((intloc (1 + 1)),())) destroys intloc (0 + 1) by ;
then A3: not 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 ;
A4: not SubFrom ((intloc (4 + 1)),(intloc (5 + 1))) destroys intloc (0 + 1) by ;
not (intloc (4 + 1)) := ((),(intloc (1 + 1))) destroys intloc (0 + 1) by ;
then not ((intloc (4 + 1)) := ((),(intloc (1 + 1)))) ";" (SubFrom ((intloc (4 + 1)),(intloc (5 + 1)))) destroys intloc (0 + 1) by ;
hence not (((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 ; :: thesis: verum