/* 

The theory of lists with lenght function

*/


:-option(special_relations(off)).  


precedence( [<,eq,length,car,cdr,cons,s,0] ).


use(listprims).
use(nat).


eq(X,Y), eq(length(X),Z) -> eq(length(Y),Z).

cons(X,Y)=Z, length(X)=A -> length(Z)=cons(nil,A).
length(nil)=nil.


:-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)]).


/*


*/