/* 

This defines natural numbers with a partial predecessor
function and exercises partial congruences.

*/


predicates([eq,nat]).
partial_congruence(eq).

nat(X) -> eq(X,X).
eq(X,X) -> nat(X).

nat(0).
nat(X) -> nat(s(X)).
nat(s(X)) -> nat(X).
nat(X),eq(0,s(X)) -> [].

nat(p(X)) -> eq(s(p(X)),X).
nat(X) -> eq(p(s(X)),X).


%nat(p(0)).       % p(0) is not a natural number, hence this can be refuted.


precedence( [nat,eq,s,p,0] ).
:-sarp([1-4,6,7,10-13]).