% Equivalence of two definitions of the Fibonacci numbers

set log fib
set script fib
clear
set trace 0

% Axioms for 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 +;
  0 + x = x;
  s(x) + y = s(x + y);
  (x + y) + z = x + (y + z);
  1 = s(0);
  2 = s(1)
  ..


% First definition of the Fibonacci numbers

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


% Second definition

set name dfib
declare operator dfib : Nat, Nat -> Nat
assert
  dfib(0, y) = y;
  dfib(1, y) = y + 1;
  dfib(x+2, y) = dfib(x+1, dfib(x, y))
  ..
make immune dfib

% The proof

set name lemma
prove dfib(x, y) = fib(x) + y by induction on x depth 2
qed

set name theorem
prove fib(x) = dfib(x, 0)
qed
statistics

% It is also possible to prove the lemma by consistency:
%      delete lemma theorem
%      complete
%      assert dfib(x, y) = fib(x) + y
%      complete