/home/nowonder/forschung/aprove/TPDB05/TRS/AProVE/rta1.trs

The program

(VAR x y)
(RULES
  
  plus(s(s(x)),y) -> s(plus(x,s(y)))
  plus(x,s(s(y))) -> s(plus(s(x),y))
  plus(s(0),y) -> s(y)
  plus(0,y) -> y

  ack(0,y) -> s(y)
  ack(s(x),0) -> ack(x,s(0))
  ack(s(x),s(y)) -> ack(x,plus(y,ack(s(x),y)))
)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend