; @origtpdbfilename ./TRS/Rubio/revlist.trs
; @xtcfilename "./TRS_Standard/Rubio_04/revlist.xml"
(format TRS)
(fun rev1 2)
(fun |0| 0)
(fun nil 0)
(fun s 1)
(fun cons 2)
(fun rev 1)
(fun rev2 2)
(rule (rev1 |0| nil) |0|)
(rule (rev1 (s X) nil) (s X))
(rule (rev1 X (cons Y L)) (rev1 Y L))
(rule (rev nil) nil)
(rule (rev (cons X L)) (cons (rev1 X L) (rev2 X L)))
(rule (rev2 X nil) nil)
(rule (rev2 X (cons Y L)) (rev (cons X (rev (rev2 Y L)))))