% Proving the Commutative Law of Addition using Induction

set(auto).

formula_list(usable).

all x (s(x) != 0).                                      % Axiom a

all x all y ((s(x) = s(y) -> x = y)).                   % Axiom b

all x (x + 0 = x).                                      % Axiom c

all x all y (x + s(y) = s(x + y)).                      % Axiom d

all x (0 + x = x).                                      % Lemma 1 (proved separately)

all y all x ((s(x) + y = s(x + y))).                    % Lemma 2 (proved separately)

% Below is the Induction axiom specialized to the commutative law of addition

 (
  (all x (x + 0 = 0 + x))                               % basis
 &
  (all y (
      (all x (x + y = y + x))                           % induction step
   -> (all x (x + s(y) = s(y) + x)))
  )
 )

-> (all y all x (x + y = y + x)).                       % induction axiom


% The following is our theorem negated.

-(all y  all x (x + y = y + x)).			% negation of theorem

end_of_list.