; @origtpdbfilename ./TRS/secret06/aprove/toList.trs
; @xtcfilename "./TRS_Standard/Secret_06_TRS/toList.xml"
(format TRS)
(fun isEmpty 1)
(fun empty 0)
(fun true 0)
(fun node 3)
(fun false 0)
(fun left 1)
(fun right 1)
(fun elem 1)
(fun append 2)
(fun nil 0)
(fun cons 2)
(fun y 0)
(fun listify 2)
(fun if 6)
(fun toList 1)
(rule (isEmpty empty) true)
(rule (isEmpty (node l x r)) false)
(rule (left empty) empty)
(rule (left (node l x r)) l)
(rule (right empty) empty)
(rule (right (node l x r)) r)
(rule (elem (node l x r)) x)
(rule (append nil x) (cons x nil))
(rule (append (cons y ys) x) (cons y (append ys x)))
(rule (listify n xs) (if (isEmpty n) (isEmpty (left n)) (right n) (node (left (left n)) (elem (left n)) (node (right (left n)) (elem n) (right n))) xs (append xs n)))
(rule (if true b n m xs ys) xs)
(rule (if false false n m xs ys) (listify m xs))
(rule (if false true n m xs ys) (listify n ys))
(rule (toList n) (listify n nil))