; @origtpdbfilename ./TRS/SchneiderKamp/trs/thiemann10.trs
; @xtcfilename "./TRS_Standard/AProVE_07/thiemann10.xml"
(format TRS)
(fun half 1)
(fun |0| 0)
(fun s 1)
(fun lastbit 1)
(fun zero 1)
(fun true 0)
(fun false 0)
(fun conv 1)
(fun conviter 2)
(fun cons 2)
(fun nil 0)
(fun if 3)
(rule (half |0|) |0|)
(rule (half (s |0|)) |0|)
(rule (half (s (s x))) (s (half x)))
(rule (lastbit |0|) |0|)
(rule (lastbit (s |0|)) (s |0|))
(rule (lastbit (s (s x))) (lastbit x))
(rule (zero |0|) true)
(rule (zero (s x)) false)
(rule (conv x) (conviter x (cons |0| nil)))
(rule (conviter x l) (if (zero x) x l))
(rule (if true x l) l)
(rule (if false x l) (conviter (half x) (cons (lastbit x) l)))