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

The program

(COMMENT 

  This example is a translation of a logic program for Ackermann's
  function, built by TALP.

    http://bibiserv.techfak.uni-bielefeld.de/talp/

  Enno Ohlebusch, Claus Claves, and Claude Marché

)

(VAR m  n)
(RULES

ack_in(0,n) -> ack_out(s(n)) 
ack_in(s(m),0) -> u11(ack_in(m,s(0))) 
u11(ack_out(n)) -> ack_out(n) 
ack_in(s(m),s(n)) -> u21(ack_in(s(m),n),m) 
u21(ack_out(n),m) -> u22(ack_in(m,n)) 
u22(ack_out(n)) -> ack_out(n) 

)

Submit to AProVE Web Frontend

Edit in AProVE Web Frontend