/* 

Congruence axioms for lists

*/




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

use(eq).


eq(X,Y), eq(cdr(X),Z) -> eq(cdr(Y),Z).
eq(X,Y), eq(car(X),Z) -> eq(car(Y),Z).
eq(X,Y), eq(U,V), eq(cons(X,U),Z) -> eq(cons(Y,V),Z).

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.


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