(COMMENT 

  Claude Marché

  From: J.-C. Filliâtre, S. Owre, H. Rueß, and N. Shankar. Deciding
        propositional combinations of equalities and
	inequalities. http://www.lri.fr/~filliatr/ftp/publis/ics.ps

)

(VAR t  c  b  a  z  y  x)
(RULES

g(A) -> A 
g(B) -> A 
g(B) -> B 
g(C) -> A 
g(C) -> B 
g(C) -> C 
foldf(x,nil) -> x 
foldf(x,cons(y,z)) -> f(foldf(x,z),y) 
f(t,x) -> f'(t,g(x)) 
f'(triple(a,b,c),C) -> triple(a,b,cons(C,c)) 
f'(triple(a,b,c),B) -> f(triple(a,b,c),A) 
f'(triple(a,b,c),A) -> f''(foldf(triple(cons(A,a),nil,c),b)) 
f''(triple(a,b,c)) -> foldf(triple(a,b,nil),c) 

)