% Proofs by consistency about lists.

set script list2
set log list2
clear
set trace 0
set name list

declare sorts Element, List
declare variables e, e1: Element, x, y, z: List
declare operators
  null   :               -> List
  cons   : Element, List -> List
  append : List, List    -> List
  rev    : List          -> List
  ..

% Axioms

assert 
  sort List generated by null, cons;
  append(null, x) = x;
  append(cons(e, y), z) = cons(e, append(y, z));
  rev(null) = null;
  rev(cons(e, y)) = append(rev(y), cons(e, null));
  cons(e, x) ~= null;
  cons(e1, x) = cons(e, y) <=> e = e1 /\ x = y
  ..
complete


% Theorems

set name theorem
assert rev(rev(x)) = x
complete
statistics

% Notice that the proof generated a lemma about a special case of
%     rev(append(x, y)) = append(rev(y), rev(x)).
% Proving the more general lemma is tricky.  Its proof diverges unless we
% prove the associativity of `append' as another lemma first.  The proof 
% of that lemma requires a critical decision about ordering an equation; 
% furthermore, the proof diverges in the presence of the lemma about the 
% special case of `rev' of `append'.

delete theorem
complete
assert append(append(x, y), z) = append(x, append(y, z))
complete
assert rev(append(x, y)) = append(rev(y), rev(x))
complete
statistics