; @origtpdbfilename ./TRS/SK90/4.28.trs
; @xtcfilename "./TRS_Standard/SK90/4.28.xml"
(format TRS)
(fun f 2)
(fun nil 0)
(fun g 2)
(fun ++ 2)
(fun null 1)
(fun true 0)
(fun false 0)
(fun mem 2)
(fun or 2)
(fun = 2)
(fun max 1)
(fun not 1)
(fun |max'| 2)
(fun u 0)
(rule (f x nil) (g nil x))
(rule (f x (g y z)) (g (f x y) z))
(rule (++ x nil) x)
(rule (++ x (g y z)) (g (++ x y) z))
(rule (null nil) true)
(rule (null (g x y)) false)
(rule (mem nil y) false)
(rule (mem (g x y) z) (or (= y z) (mem x z)))
(rule (mem x (max x)) (not (null x)))
(rule (max (g (g nil x) y)) (|max'| x y))
(rule (max (g (g (g x y) z) u)) (|max'| (max (g (g x y) z)) u))