; @origtpdbfilename combination.trs
; @xtcfilename "../xml/combination.trs.xml"
(format TRS)
(fun true 0)
(fun less_leaves 2)
(fun app 2)
(fun divL 2)
(fun concat 2)
(fun leaf 0)
(fun xs 0)
(fun shuffle 1)
(fun nil 0)
(fun false 0)
(fun s 1)
(fun reverse 1)
(fun div 2)
(fun |0| 0)
(fun minus 2)
(fun cons 2)
(rule (minus x |0|) x)
(rule (minus (s x) (s y)) (minus x y))
(rule (div |0| (s y)) |0|)
(rule (div (s x) (s y)) (s (div (minus x y) (s y))))
(rule (divL x nil) x)
(rule (divL x (cons y xs)) (divL (div x y) xs))
(rule (app nil y) y)
(rule (app (cons n x) y) (cons n (app x y)))
(rule (reverse nil) nil)
(rule (reverse (cons n x)) (app (reverse x) (cons n nil)))
(rule (shuffle nil) nil)
(rule (shuffle (cons n x)) (cons n (shuffle (reverse x))))
(rule (concat leaf y) y)
(rule (concat (cons u v) y) (cons u (concat v y)))
(rule (less_leaves x leaf) false)
(rule (less_leaves leaf (cons w z)) true)
(rule (less_leaves (cons u v) (cons w z)) (less_leaves (concat u v) (concat w z)))
(rule (divL z (cons x (cons y xs))) (divL z (cons y (cons x xs))) :cost 0)
(rule (shuffle (cons n (cons m x))) (shuffle (cons m (cons n x))) :cost 0)