/* 
The theory of arrays.
*/


:-option(special_relations(off)).   

use(eq).

eq(X,Y) -> eq(select(X,I),select(Y,I)).
%eq(X,Y),eq(U,V), eq(A,B) -> eq(store(A,X,U),store(B,Y,V)).
eq(A,B) -> eq(store(A,X,U),store(B,X,U)).


eq(store(A,I,X),AIX) -> eq(select(AIX,I),X).
eq(select(AIX,J),AJ) <- eq(store(A,I,X),AIX), eq(select(A,J),AJ).
eq(select(AIX,J),AJ) <- eq(store(A,I,X),AIX), eq(select(A,J),AJ).



% extensionality 
%  (we don't need a congruence axiom for the 
%   Skolem function i)

%eq(select(A,i(A,B)),select(B,i(A,B))) -> eq(A,B).


precedence( [neq,eq,select,store,i] ).
:-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)]).

/*



*/