; @origtpdbfilename ./TRS/Rubio/bintrees.trs./TRS/AG01/#3.14.trs
; @xtcfilename "./TRS_Standard/Rubio_04/bintrees.xml"
(format TRS)
(fun concat 2)
(fun leaf 0)
(fun cons 2)
(fun lessleaves 2)
(fun false 0)
(fun true 0)
(rule (concat leaf Y) Y)
(rule (concat (cons U V) Y) (cons U (concat V Y)))
(rule (lessleaves X leaf) false)
(rule (lessleaves leaf (cons W Z)) true)
(rule (lessleaves (cons U V) (cons W Z)) (lessleaves (concat U V) (concat W Z)))