; @origtpdbfilename ./TRS/Cime/big.trs
; @xtcfilename "./TRS_Standard/CiME_04/big.xml"
(format TRS)
(fun |0| 1)
(fun |#| 0)
(fun + 2)
(fun |1| 1)
(fun - 2)
(fun not 1)
(fun true 0)
(fun false 0)
(fun if 3)
(fun eq 2)
(fun ge 2)
(fun log 1)
(fun |log'| 1)
(fun * 2)
(fun app 2)
(fun nil 0)
(fun cons 2)
(fun sum 1)
(fun prod 1)
(fun mem 2)
(fun inter 2)
(fun ifinter 4)
(rule (|0| |#|) |#|)
(rule (+ x |#|) x)
(rule (+ |#| x) x)
(rule (+ (|0| x) (|0| y)) (|0| (+ x y)))
(rule (+ (|0| x) (|1| y)) (|1| (+ x y)))
(rule (+ (|1| x) (|0| y)) (|1| (+ x y)))
(rule (+ (|1| x) (|1| y)) (|0| (+ (+ x y) (|1| |#|))))
(rule (+ (+ x y) z) (+ x (+ y z)))
(rule (- |#| x) |#|)
(rule (- x |#|) x)
(rule (- (|0| x) (|0| y)) (|0| (- x y)))
(rule (- (|0| x) (|1| y)) (|1| (- (- x y) (|1| |#|))))
(rule (- (|1| x) (|0| y)) (|1| (- x y)))
(rule (- (|1| x) (|1| y)) (|0| (- x y)))
(rule (not true) false)
(rule (not false) true)
(rule (if true x y) x)
(rule (if false x y) y)
(rule (eq |#| |#|) true)
(rule (eq |#| (|1| y)) false)
(rule (eq (|1| x) |#|) false)
(rule (eq |#| (|0| y)) (eq |#| y))
(rule (eq (|0| x) |#|) (eq x |#|))
(rule (eq (|1| x) (|1| y)) (eq x y))
(rule (eq (|0| x) (|1| y)) false)
(rule (eq (|1| x) (|0| y)) false)
(rule (eq (|0| x) (|0| y)) (eq x y))
(rule (ge (|0| x) (|0| y)) (ge x y))
(rule (ge (|0| x) (|1| y)) (not (ge y x)))
(rule (ge (|1| x) (|0| y)) (ge x y))
(rule (ge (|1| x) (|1| y)) (ge x y))
(rule (ge x |#|) true)
(rule (ge |#| (|0| x)) (ge |#| x))
(rule (ge |#| (|1| x)) false)
(rule (log x) (- (|log'| x) (|1| |#|)))
(rule (|log'| |#|) |#|)
(rule (|log'| (|1| x)) (+ (|log'| x) (|1| |#|)))
(rule (|log'| (|0| x)) (if (ge x (|1| |#|)) (+ (|log'| x) (|1| |#|)) |#|))
(rule (* |#| x) |#|)
(rule (* (|0| x) y) (|0| (* x y)))
(rule (* (|1| x) y) (+ (|0| (* x y)) y))
(rule (* (* x y) z) (* x (* y z)))
(rule (* x (+ y z)) (+ (* x y) (* x z)))
(rule (app nil l) l)
(rule (app (cons x l1) l2) (cons x (app l1 l2)))
(rule (sum nil) (|0| |#|))
(rule (sum (cons x l)) (+ x (sum l)))
(rule (sum (app l1 l2)) (+ (sum l1) (sum l2)))
(rule (prod nil) (|1| |#|))
(rule (prod (cons x l)) (* x (prod l)))
(rule (prod (app l1 l2)) (* (prod l1) (prod l2)))
(rule (mem x nil) false)
(rule (mem x (cons y l)) (if (eq x y) true (mem x l)))
(rule (inter x nil) nil)
(rule (inter nil x) nil)
(rule (inter (app l1 l2) l3) (app (inter l1 l3) (inter l2 l3)))
(rule (inter l1 (app l2 l3)) (app (inter l1 l2) (inter l1 l3)))
(rule (inter (cons x l1) l2) (ifinter (mem x l2) x l1 l2))
(rule (inter l1 (cons x l2)) (ifinter (mem x l1) x l2 l1))
(rule (ifinter true x l1 l2) (cons x (inter l1 l2)))
(rule (ifinter false x l1 l2) (inter l1 l2))