/* 

The theory of pairs.
The initial presentation is not subterm local,
as otherwise the rules with fst and snd
cound not be used for queries without those
operators.

Saturation produces the essential consequences 44 an 59,
representing the injectivity of cons.

*/


predicates( [eq] ).


:-option(special_relations(off)).  

% equality
eq(X,Y), eq(Y,Z) -> eq(X,Z).
eq(X,X).
eq(X,Y) -> eq(Y,X).
eq(X,Y), eq(U,V) -> eq(cons(X,U),cons(Y,V)).        
eq(X,Y) -> eq(fst(X),fst(Y)).
eq(X,Y) -> eq(snd(X),snd(Y)).

% theory 
eq(fst(cons(X,Y)),X).
eq(snd(cons(X,Y)),Y).





precedence( [f,p] ).

:-option([crw_depth(1),memo_constraints(on)]).
:-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.

:-ordering(sto).  % subterm ordering


/*

20000810

Saturation terminated.

Persisting Clauses:

    1(1) : eq(B,C),eq(C,D) -> eq(B,D)
    2(1) : eq(B,B)
    3(1) : eq(B,C) -> eq(C,B)
    4(1) : eq(B,C),eq(D,E) -> eq(cons(B,D),cons(C,E))
    7(1) : eq(B,C) -> eq(fst(B),fst(C))
    8(1) : eq(B,C) -> eq(snd(B),snd(C))
    9(2) : eq(B,C) -> eq(fst(cons(B,D)),C)
   10(2) : eq(fst(cons(B,C)),D) -> eq(B,D)
   14(2) : eq(B,C) -> eq(snd(cons(D,B)),C)
   15(2) : eq(snd(cons(B,C)),D) -> eq(C,D)
   19(2) : eq(B,C),eq(fst(C),D) -> eq(fst(B),D)
   24(2) : eq(B,C),eq(snd(C),D) -> eq(snd(B),D)
   29(2) : eq(B,C),eq(D,E),eq(cons(C,E),F) -> eq(cons(B,D),F)
   35(3) : eq(cons(B,C),D) -> eq(B,fst(D))
   37(4) : eq(cons(B,C),D),eq(fst(D),E) -> eq(B,E)
   38(4) : eq(cons(B,C),D),eq(B,E) -> eq(fst(D),E)
   44(4) : eq(cons(B,C),cons(D,E)) -> eq(D,B)
   48(3) : eq(cons(B,C),D) -> eq(C,snd(D))
   51(4) : eq(cons(B,C),D),eq(snd(D),E) -> eq(C,E)
   52(4) : eq(cons(B,C),D),eq(C,E) -> eq(snd(D),E)
   59(4) : eq(cons(B,C),cons(D,E)) -> eq(E,C)



Total time: 6005720 milliseconds

Number of forward inferences: 254
Number of tableau inferences: 0
Number of kept clauses: 23

*/