(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 x n) (RULES g(A) -> A g(B) -> A g(B) -> B g(C) -> A g(C) -> B g(C) -> C foldB(t,0) -> t foldB(t,s(n)) -> f(foldB(t,n),B) foldC(t,0) -> t foldC(t,s(n)) -> f(foldC(t,n),C) f(t,x) -> f'(t,g(x)) f'(triple(a,b,c),C) -> triple(a,b,s(c)) f'(triple(a,b,c),B) -> f(triple(a,b,c),A) f'(triple(a,b,c),A) -> f''(foldB(triple(s(a),0,c),b)) f''(triple(a,b,c)) -> foldC(triple(a,b,0),c) )