; @origtpdbfilename ./TRS/SchneiderKamp/trs/cade16.trs
; @xtcfilename "./TRS_Standard/GTSSK07/cade16.xml"
(format TRS)
(fun nthtail 2)
(fun cond 3)
(fun ge 2)
(fun length 1)
(fun true 0)
(fun false 0)
(fun tail 1)
(fun s 1)
(fun nil 0)
(fun cons 2)
(fun |0| 0)
(rule (nthtail n l) (cond (ge n (length l)) n l))
(rule (cond true n l) l)
(rule (cond false n l) (tail (nthtail (s n) l)))
(rule (tail nil) nil)
(rule (tail (cons x l)) l)
(rule (length nil) |0|)
(rule (length (cons x l)) (s (length l)))
(rule (ge u |0|) true)
(rule (ge |0| (s v)) false)
(rule (ge (s u) (s v)) (ge u v))