; @origtpdbfilename ./TRS/Rubio/enno.trs
; @xtcfilename "./TRS_Standard/Rubio_04/enno.xml"
(format TRS)
(fun lt 2)
(fun |0| 0)
(fun s 1)
(fun true 0)
(fun false 0)
(fun append 2)
(fun nil 0)
(fun add 2)
(fun split 2)
(fun pair 2)
(fun f_1 4)
(fun f_2 6)
(fun qsort 1)
(fun f_3 3)
(rule (lt |0| (s X)) true)
(rule (lt (s X) |0|) false)
(rule (lt (s X) (s Y)) (lt X Y))
(rule (append nil Y) Y)
(rule (append (add N X) Y) (add N (append X Y)))
(rule (split N nil) (pair nil nil))
(rule (split N (add M Y)) (f_1 (split N Y) N M Y))
(rule (f_1 (pair X Z) N M Y) (f_2 (lt N M) N M Y X Z))
(rule (f_2 true N M Y X Z) (pair X (add M Z)))
(rule (f_2 false N M Y X Z) (pair (add M X) Z))
(rule (qsort nil) nil)
(rule (qsort (add N X)) (f_3 (split N X) N X))
(rule (f_3 (pair Y Z) N X) (append (qsort Y) (add X (qsort Z))))