; @origtpdbfilename ./TRS/Cime/tree.trs
; @xtcfilename "./TRS_Standard/CiME_04/tree.xml"
(format TRS)
(fun |0| 1)
(fun |#| 0)
(fun + 2)
(fun |1| 1)
(fun - 2)
(fun not 1)
(fun false 0)
(fun true 0)
(fun and 2)
(fun if 3)
(fun ge 2)
(fun val 1)
(fun l 1)
(fun n 3)
(fun min 1)
(fun max 1)
(fun bs 1)
(fun size 1)
(fun wb 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 |#|) x)
(rule (- |#| 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 false) true)
(rule (not true) false)
(rule (and x true) x)
(rule (and x false) false)
(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 |#| (|1| x)) false)
(rule (ge |#| (|0| x)) (ge |#| x))
(rule (val (l x)) x)
(rule (val (n x y z)) x)
(rule (min (l x)) x)
(rule (min (n x y z)) (min y))
(rule (max (l x)) x)
(rule (max (n x y z)) (max z))
(rule (bs (l x)) true)
(rule (bs (n x y z)) (and (and (ge x (max y)) (ge (min z) x)) (and (bs y) (bs z))))
(rule (size (l x)) (|1| |#|))
(rule (size (n x y z)) (+ (+ (size x) (size y)) (|1| |#|)))
(rule (wb (l x)) true)
(rule (wb (n x y z)) (and (if (ge (size y) (size z)) (ge (|1| |#|) (- (size y) (size z))) (ge (|1| |#|) (- (size z) (size y)))) (and (wb y) (wb z))))