; @origtpdbfilename ./TRS/secret07/aprove/aprove10.trs
; @xtcfilename "./TRS_Standard/Secret_07_TRS/aprove10.xml"
(format TRS)
(fun lessElements 2)
(fun lessE 3)
(fun |0| 0)
(fun if 5)
(fun le 2)
(fun length 1)
(fun toList 1)
(fun true 0)
(fun false 0)
(fun s 1)
(fun nil 0)
(fun cons 2)
(fun leaf 0)
(fun node 3)
(fun append 2)
(fun a 0)
(fun c 0)
(fun d 0)
(rule (lessElements l t) (lessE l t |0|))
(rule (lessE l t n) (if (le (length l) n) (le (length (toList t)) n) l t n))
(rule (if true b l t n) l)
(rule (if false true l t n) t)
(rule (if false false l t n) (lessE l t (s n)))
(rule (length nil) |0|)
(rule (length (cons n l)) (s (length l)))
(rule (toList leaf) nil)
(rule (toList (node t1 n t2)) (append (toList t1) (cons n (toList t2))))
(rule (append nil l2) l2)
(rule (append (cons n l1) l2) (cons n (append l1 l2)))
(rule (le (s n) |0|) false)
(rule (le |0| m) true)
(rule (le (s n) (s m)) (le n m))
(rule a c)
(rule a d)