; @origtpdbfilename ./TRS/SchneiderKamp/trs/thiemann21.trs
; @xtcfilename "./TRS_Standard/AProVE_07/thiemann21.xml"
(format TRS)
(fun eq 2)
(fun |0| 0)
(fun true 0)
(fun s 1)
(fun false 0)
(fun lt 2)
(fun bin2s 1)
(fun nil 0)
(fun cons 2)
(fun bin2ss 2)
(fun double 1)
(fun |1| 0)
(fun half 1)
(fun log 1)
(fun more 1)
(fun s2bin 1)
(fun s2bin1 3)
(fun if1 4)
(fun s2bin2 2)
(fun bug_list_not 0)
(fun if2 4)
(rule (eq |0| |0|) true)
(rule (eq |0| (s y)) false)
(rule (eq (s x) |0|) false)
(rule (eq (s x) (s y)) (eq x y))
(rule (lt |0| (s y)) true)
(rule (lt x |0|) false)
(rule (lt (s x) (s y)) (lt x y))
(rule (bin2s nil) |0|)
(rule (bin2s (cons x xs)) (bin2ss x xs))
(rule (bin2ss x nil) x)
(rule (bin2ss x (cons |0| xs)) (bin2ss (double x) xs))
(rule (bin2ss x (cons |1| xs)) (bin2ss (s (double x)) xs))
(rule (half |0|) |0|)
(rule (half (s |0|)) |0|)
(rule (half (s (s x))) (s (half x)))
(rule (log |0|) |0|)
(rule (log (s |0|)) |0|)
(rule (log (s (s x))) (s (log (half (s (s x))))))
(rule (more nil) nil)
(rule (more (cons xs ys)) (cons (cons |0| xs) (cons (cons |1| xs) (cons xs ys))))
(rule (s2bin x) (s2bin1 x |0| (cons nil nil)))
(rule (s2bin1 x y lists) (if1 (lt y (log x)) x y lists))
(rule (if1 true x y lists) (s2bin1 x (s y) (more lists)))
(rule (if1 false x y lists) (s2bin2 x lists))
(rule (s2bin2 x nil) bug_list_not)
(rule (s2bin2 x (cons xs ys)) (if2 (eq x (bin2s xs)) x xs ys))
(rule (if2 true x xs ys) xs)
(rule (if2 false x xs ys) (s2bin2 x ys))