/* 

The theory of lists with lenght function

*/


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

cons(X,Y)=Z -> car(Z)=X.
cons(X,Y)=Z -> cdr(Z)=Y.
cons(X,Y)=cons(U,V) -> X=U.
cons(X,Y)=cons(U,V) -> Y=V.
cons(X,Y)=nil -> [].


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


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


/*


*/