%  Proofs by induction using uncompleted sets of rewrite rules

set log sum
set script sum
clear
set trace 0

% Axioms for the natural numbers

set name nat

declare sort Nat
declare variables x, y, z: Nat
declare operators
  0, 1, 2      :          -> Nat
  s            : Nat      -> Nat
  __+__, __*__ : Nat, Nat -> Nat
  ..
assert 
  sort Nat generated by 0, s;
  ac +;
  ac *;
  x + 0 = x;
  x + s(y) = s(x + y);
  x * 0 = 0;
  x * s(y) = (x * y) + x;
  x * (y + z) = (x * y) + (x * z);
  1 = s(0);
  2 = s(1)
  ..

%  Step 1.  Define the "sum of the first n integers" function.

declare operator sum: Nat -> Nat
assert
  sum(0) = 0;
  sum(x+1) = sum(x) + x + 1
  ..


% Step 2.  Prove a theorem by induction.

set name theorem
prove 2*sum(x) = x*(x+1) by induction
qed

% Step 3.  Introduce notation to restate the theorem.

delete theorem
set name div2

declare operator div2: Nat -> Nat
assert
  div2(0) = 0;
  div2(1) = 0;
  div2(x+2) = div2(x) + 1
  ..

%  Step 4.  Prove the restated theorem by induction.

set name theorem
prove sum(x) = div2(x*(x+1)) by induction

% We need a lemma, which we formulate by brute-force generalization 
% and prove by two-level induction on x.  This could be nicer.

prove x + div2(y+x) = div2(y+x+x+x) by induction on x depth 2
qed

% A more general lemma would have been "x + div2(y) = div2(y+(2*x))", 
% which we can prove by one-level induction on x.

statistics