/* 
The theory of lists.

*/




:-option(special_relations(off)).      % otherwise trivial

use(listcong).

/*
% system (I)
eq(cons(X,Y),Z) -> eq(car(Z),X).
eq(cons(X,Y),Z) -> eq(cdr(Z),Y).

eq(cons(A,B),X), eq(car(Y),A), eq(cdr(Y),B) -> eq(X,Y).  % (1)
*/

% system (II) (non-flat)
eq(car(cons(X,Y)),X).
eq(cdr(cons(X,Y)),Y).
eq(cons(car(X),cdr(X)),X).



precedence( [eq,car,cdr,cons] ).
:-ordering(sto).
:-sama([]).             % We want saturation by ordered resolution w/o sel.
:-sarp([1-7,10-15]).    % the usual + clausal rewriting  
:-sams([3,19]).      % messages about redundancy proofs by clausal rewrtng.
%:-saci([2]).

:-option([memo_constraints(on),crw_depth(1)]).