; @origtpdbfilename ./TRS/SchneiderKamp/trs/thiemann09.trs
; @xtcfilename "./TRS_Standard/AProVE_07/thiemann09.xml"
(format TRS)
(fun minus 2)
(fun plus 2)
(fun |0| 0)
(fun s 1)
(fun zero 1)
(fun false 0)
(fun true 0)
(fun p 1)
(fun div 2)
(fun quot 3)
(fun ack 2)
(rule (minus (minus x y) z) (minus x (plus y z)))
(rule (minus |0| y) |0|)
(rule (minus x |0|) x)
(rule (minus (s x) (s y)) (minus x y))
(rule (plus |0| y) y)
(rule (plus (s x) y) (plus x (s y)))
(rule (plus (s x) y) (s (plus y x)))
(rule (zero (s x)) false)
(rule (zero |0|) true)
(rule (p (s x)) x)
(rule (p |0|) |0|)
(rule (div x y) (quot x y |0|))
(rule (quot (s x) (s y) z) (quot (minus (p (ack |0| x)) y) (s y) (s z)))
(rule (quot |0| (s y) z) z)
(rule (ack |0| x) (s x))
(rule (ack |0| x) (plus x (s |0|)))
(rule (ack (s x) |0|) (ack x (s |0|)))
(rule (ack (s x) (s y)) (ack x (ack (s x) y)))