/home/nowonder/forschung/aprove/TPDB05/TRS/uncurried/D33/29.trs

The program

(VAR x y)
(RULES 
ack(0,y) -> succ(y)
ack(succ(x),y) -> ack(x,succ(0))
ack(succ(x),succ(y)) -> ack(x,ack(succ(x),y))
)

(COMMENT Example 29 in \cite{D33})

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend