; @origtpdbfilename ./TRS/SchneiderKamp/trs/thiemann32.trs
; @xtcfilename "./TRS_Standard/AProVE_07/thiemann32.xml"
(format TRS)
(fun table 0)
(fun gen 1)
(fun s 1)
(fun |0| 0)
(fun if1 2)
(fun le 2)
(fun |10| 0)
(fun false 0)
(fun nil 0)
(fun true 0)
(fun if2 2)
(fun if3 3)
(fun cons 2)
(fun entry 3)
(fun times 2)
(fun plus 2)
(rule table (gen (s |0|)))
(rule (gen x) (if1 (le x |10|) x))
(rule (if1 false x) nil)
(rule (if1 true x) (if2 x x))
(rule (if2 x y) (if3 (le y |10|) x y))
(rule (if3 true x y) (cons (entry x y (times x y)) (if2 x (s y))))
(rule (if3 false x y) (gen (s x)))
(rule (le |0| y) true)
(rule (le (s x) |0|) false)
(rule (le (s x) (s y)) (le x y))
(rule (plus |0| y) y)
(rule (plus (s x) y) (s (plus x y)))
(rule (times |0| y) |0|)
(rule (times (s x) y) (plus y (times x y)))
(rule |10| (s (s (s (s (s (s (s (s (s (s |0|)))))))))))