/home/nowonder/forschung/aprove/TPDB05/TRS/Cime/filliatre3.trs

The program

(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) 
fold(t,x,0) -> t 
fold(t,x,s(n)) -> f(fold(t,x,n),x) 

)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend