; @origtpdbfilename ./TRS/Cime/log2.trs
; @xtcfilename "./TRS_Standard/CiME_04/log2.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 ge 2)
(fun log 1)
(fun |log'| 1)
(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 (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| |#|)) |#|))