; @origtpdbfilename ./TRS/various/10.trs
; @xtcfilename "./TRS_Standard/Various_04/10.xml"
(format TRS)
(fun + 2)
(fun |0| 0)
(fun s 1)
(fun ++ 2)
(fun nil 0)
(fun |:| 2)
(fun sum 1)
(fun - 2)
(fun quot 2)
(fun length 1)
(fun hd 1)
(fun avg 1)
(rule (+ |0| y) y)
(rule (+ (s x) y) (s (+ x y)))
(rule (++ nil ys) ys)
(rule (++ (|:| x xs) ys) (|:| x (++ xs ys)))
(rule (sum (|:| x nil)) (|:| x nil))
(rule (sum (|:| x (|:| y xs))) (sum (|:| (+ x y) xs)))
(rule (sum (++ xs (|:| x (|:| y ys)))) (sum (++ xs (sum (|:| x (|:| y ys))))))
(rule (- x |0|) x)
(rule (- |0| (s y)) |0|)
(rule (- (s x) (s y)) (- x y))
(rule (quot |0| (s y)) |0|)
(rule (quot (s x) (s y)) (s (quot (- x y) (s y))))
(rule (length nil) |0|)
(rule (length (|:| x xs)) (s (length xs)))
(rule (hd (|:| x xs)) x)
(rule (avg xs) (quot (hd (sum xs)) (length xs)))