; @origtpdbfilename ./TRS/various/14.trs
; @xtcfilename "./TRS_Standard/Various_04/14.xml"
(format TRS)
(fun O 1)
(fun |0| 0)
(fun + 2)
(fun I 1)
(fun - 2)
(fun |1| 0)
(fun not 1)
(fun true 0)
(fun false 0)
(fun and 2)
(fun if 3)
(fun ge 2)
(fun |Log'| 1)
(fun Log 1)
(fun Val 1)
(fun L 1)
(fun N 3)
(fun l 0)
(fun r 0)
(fun Min 1)
(fun Max 1)
(fun BS 1)
(fun Size 1)
(fun WB 1)
(rule (O |0|) |0|)
(rule (+ |0| x) x)
(rule (+ x |0|) x)
(rule (+ (O x) (O y)) (O (+ x y)))
(rule (+ (O x) (I y)) (I (+ x y)))
(rule (+ (I x) (O y)) (I (+ x y)))
(rule (+ (I x) (I y)) (O (+ (+ x y) (I |0|))))
(rule (+ x (+ y z)) (+ (+ x y) z))
(rule (- x |0|) x)
(rule (- |0| x) |0|)
(rule (- (O x) (O y)) (O (- x y)))
(rule (- (O x) (I y)) (I (- (- x y) (I |1|))))
(rule (- (I x) (O y)) (I (- x y)))
(rule (- (I x) (I y)) (O (- x y)))
(rule (not true) false)
(rule (not false) true)
(rule (and x true) x)
(rule (and x false) false)
(rule (if true x y) x)
(rule (if false x y) y)
(rule (ge (O x) (O y)) (ge x y))
(rule (ge (O x) (I y)) (not (ge y x)))
(rule (ge (I x) (O y)) (ge x y))
(rule (ge (I x) (I y)) (ge x y))
(rule (ge x |0|) true)
(rule (ge |0| (O x)) (ge |0| x))
(rule (ge |0| (I x)) false)
(rule (|Log'| |0|) |0|)
(rule (|Log'| (I x)) (+ (|Log'| x) (I |0|)))
(rule (|Log'| (O x)) (if (ge x (I |0|)) (+ (|Log'| x) (I |0|)) |0|))
(rule (Log x) (- (|Log'| x) (I |0|)))
(rule (Val (L x)) x)
(rule (Val (N x l r)) x)
(rule (Min (L x)) x)
(rule (Min (N x l r)) (Min l))
(rule (Max (L x)) x)
(rule (Max (N x l r)) (Max r))
(rule (BS (L x)) true)
(rule (BS (N x l r)) (and (and (ge x (Max l)) (ge (Min r) x)) (and (BS l) (BS r))))
(rule (Size (L x)) (I |0|))
(rule (Size (N x l r)) (+ (+ (Size l) (Size r)) (I |1|)))
(rule (WB (L x)) true)
(rule (WB (N x l r)) (and (if (ge (Size l) (Size r)) (ge (I |0|) (- (Size l) (Size r))) (ge (I |0|) (- (Size r) (Size l)))) (and (WB l) (WB r))))