/*

This example 
shows how commutation can be eliminated
in the presence of certain ordering constraints,
at the expense of a very explicit inferences with an
ordered variant of symmetry.

Applying that symmetry law
orders negative equations
such that the maximal term occurs
on the right side.
This is not needed if intially given negative equations 
are all of the form s=x with constraint s>=x.
This form can always be achieved and is in particular
present for all equations that abstract subterms of nonflat
terms in the initial clauses.


The STC-transformation
transforms a=b
into the two clauses
  a=x -> b=x if [a>=x, b>=x]
  b=x -> a=x if [a>=x, b>=x]


*/


id(X,X).
eq(X,Y) <- id(X,Y).
eq(Z,Y) <- eq(Z,X), eq(Y,X) if [Y>=Z].


eq(Z,Y) <- eq(Y,Z)          if [Z>Y].
/*
eq(X,Z) <- eq(X,f(Z)) if [Z>X].
eq(X,f(Z)) <- eq(X,Z) if [Z>=X,X>=Z].
*/

eq(X,b) <- eq(X,a) if [b>X].
eq(X,a) <- eq(X,b) if [b>=X,X>=b].




precedence([f,a,b]).
top_predicates_precedence([eq,id]).


:-option([crw_depth(2),memo_constraints(on)]).
:-sama([3]).            % We want saturation by ordered resolution w/ sel.
:-sarp([1-7,10-15]).    % the usual + clausal rewriting  
:-sams([3,19]).         % messages about redundancy proofs by clausal rewrtng.


:-saci([2]).

/*


We have the following system:

A) theory axioms 

A.1) reflexivity
x==y
x==y -> x=y

A.2) ordered symmetry

x=y  -> y=x  if x>y

A.3) ordered commutation

y=x, z=x -> y=z  if y>=z


The ``other half'' of the symmetry follows from the
restricted commutation axiom, together with 
reflexivity.
In presence of symmetry, the ordered version of commutation
is sufficient.


B) the STC modification replaces any positive equation
   a=b with a>b by two clauses

x=a  -> x=b  if b>=x
x=b  -> x=a  if b>=x



As the set of clauses 1-7 is saturated up to redundancy,
any resolution inference of a B-clause with a theory clause
is redundant in the presence of the other B-clause.

Resolution between B-clauses which derive a new
equation will always produce both forms
of the equation, hence inferences with theory axioms
will also be redundant.

Since the commutation axiom has a selected literal it
need not occur as positive premise.

If all negative equations are of the form x=s with a constraint s>=x
then no resolution with ordered symmetry is ever possible.
The B-type negative literals have this property.
If x does not occur elsewhere, whenever
s=x needs to be selected, reflexivity resolution
will eliminate it.
If x does occur elsewhere in a term f(x), and if x>s, then s=x is no maximal,
hence need not be selected.
If x occurs in t=x then x has been introduced by positive
(or negative) splitting and, therefore, carries the constraint s>=x
(and t>=x).

In short, if one starts from flat clauses in STC form
and, then, splits negative equations u=v into
u=x, x=v with constraints u,v>=x (this preserves [un]satisfiablity,
all resolution steps with ordered symmetry are redundant.

*/