; @origtpdbfilename ./TRS/SchneiderKamp/trs/otto02.trs
; @xtcfilename "./TRS_Standard/AProVE_07/otto02.xml"
(format TRS)
(fun app 2)
(fun helpa 4)
(fun |0| 0)
(fun plus 2)
(fun length 1)
(fun s 1)
(fun nil 0)
(fun cons 2)
(fun if 5)
(fun ge 2)
(fun true 0)
(fun false 0)
(fun helpb 4)
(fun take 3)
(fun xs 0)
(rule (app x y) (helpa |0| (plus (length x) (length y)) x y))
(rule (plus x |0|) x)
(rule (plus x (s y)) (s (plus x y)))
(rule (length nil) |0|)
(rule (length (cons x y)) (s (length y)))
(rule (helpa c l ys zs) (if (ge c l) c l ys zs))
(rule (ge x |0|) true)
(rule (ge |0| (s x)) false)
(rule (ge (s x) (s y)) (ge x y))
(rule (if true c l ys zs) nil)
(rule (if false c l ys zs) (helpb c l ys zs))
(rule (take |0| (cons x xs) ys) x)
(rule (take |0| nil (cons y ys)) y)
(rule (take (s c) (cons x xs) ys) (take c xs ys))
(rule (take (s c) nil (cons y ys)) (take c nil ys))
(rule (helpb c l ys zs) (cons (take c ys zs) (helpa (s c) l ys zs)))