; @origtpdbfilename ./TRS/SchneiderKamp/trs/thiemann05.trs
; @xtcfilename "./TRS_Standard/AProVE_07/thiemann05.xml"
(format TRS)
(fun isLeaf 1)
(fun leaf 0)
(fun true 0)
(fun cons 2)
(fun false 0)
(fun left 1)
(fun right 1)
(fun concat 2)
(fun less_leaves 2)
(fun if1 4)
(fun if2 3)
(rule (isLeaf leaf) true)
(rule (isLeaf (cons u v)) false)
(rule (left (cons u v)) u)
(rule (right (cons u v)) v)
(rule (concat leaf y) y)
(rule (concat (cons u v) y) (cons u (concat v y)))
(rule (less_leaves u v) (if1 (isLeaf u) (isLeaf v) u v))
(rule (if1 b true u v) false)
(rule (if1 b false u v) (if2 b u v))
(rule (if2 true u v) true)
(rule (if2 false u v) (less_leaves (concat (left u) (right u)) (concat (left v) (right v))))