YES Time: 0.368120 TRS: { O 0() -> 0(), +(x, 0()) -> x, +(x, +(y, z)) -> +(+(x, y), z), +(0(), x) -> x, +(O x, O y) -> O +(x, y), +(O x, I y) -> I +(x, y), +(I x, O y) -> I +(x, y), +(I x, I y) -> O +(+(x, y), I 0()), -(x, 0()) -> x, -(0(), x) -> 0(), -(O x, O y) -> O -(x, y), -(O x, I y) -> I -(-(x, y), I 1()), -(I x, O y) -> I -(x, y), -(I x, I y) -> O -(x, y), not false() -> true(), not true() -> false(), and(x, false()) -> false(), and(x, true()) -> x, if(false(), x, y) -> y, if(true(), x, y) -> x, ge(x, 0()) -> true(), ge(0(), O x) -> ge(0(), x), ge(0(), I x) -> false(), ge(O x, O y) -> ge(x, y), ge(O x, I y) -> not ge(y, x), ge(I x, O y) -> ge(x, y), ge(I x, I y) -> ge(x, y), Log' 0() -> 0(), Log' O x -> if(ge(x, I 0()), +(Log' x, I 0()), 0()), Log' I x -> +(Log' x, I 0()), Log x -> -(Log' x, I 0()), Val L x -> x, Val N(x, l(), r()) -> x, Min L x -> x, Min N(x, l(), r()) -> Min l(), Max L x -> x, Max N(x, l(), r()) -> Max r(), BS L x -> true(), BS N(x, l(), r()) -> and(and(ge(x, Max l()), ge(Min r(), x)), and(BS l(), BS r())), Size L x -> I 0(), Size N(x, l(), r()) -> +(+(Size l(), Size r()), I 1()), WB L x -> true(), 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()))} DP: DP: { +#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z), +#(O x, O y) -> O# +(x, y), +#(O x, O y) -> +#(x, y), +#(O x, I y) -> +#(x, y), +#(I x, O y) -> +#(x, y), +#(I x, I y) -> O# +(+(x, y), I 0()), +#(I x, I y) -> +#(x, y), +#(I x, I y) -> +#(+(x, y), I 0()), -#(O x, O y) -> O# -(x, y), -#(O x, O y) -> -#(x, y), -#(O x, I y) -> -#(x, y), -#(O x, I y) -> -#(-(x, y), I 1()), -#(I x, O y) -> -#(x, y), -#(I x, I y) -> O# -(x, y), -#(I x, I y) -> -#(x, y), ge#(0(), O x) -> ge#(0(), x), ge#(O x, O y) -> ge#(x, y), ge#(O x, I y) -> not# ge(y, x), ge#(O x, I y) -> ge#(y, x), ge#(I x, O y) -> ge#(x, y), ge#(I x, I y) -> ge#(x, y), Log'# O x -> +#(Log' x, I 0()), Log'# O x -> if#(ge(x, I 0()), +(Log' x, I 0()), 0()), Log'# O x -> ge#(x, I 0()), Log'# O x -> Log'# x, Log'# I x -> +#(Log' x, I 0()), Log'# I x -> Log'# x, Log# x -> -#(Log' x, I 0()), Log# x -> Log'# x, Min# N(x, l(), r()) -> Min# l(), Max# N(x, l(), r()) -> Max# r(), BS# N(x, l(), r()) -> and#(and(ge(x, Max l()), ge(Min r(), x)), and(BS l(), BS r())), BS# N(x, l(), r()) -> and#(ge(x, Max l()), ge(Min r(), x)), BS# N(x, l(), r()) -> and#(BS l(), BS r()), BS# N(x, l(), r()) -> ge#(x, Max l()), BS# N(x, l(), r()) -> ge#(Min r(), x), BS# N(x, l(), r()) -> Min# r(), BS# N(x, l(), r()) -> Max# l(), BS# N(x, l(), r()) -> BS# l(), BS# N(x, l(), r()) -> BS# r(), Size# N(x, l(), r()) -> +#(+(Size l(), Size r()), I 1()), Size# N(x, l(), r()) -> +#(Size l(), Size r()), Size# N(x, l(), r()) -> Size# l(), Size# N(x, l(), r()) -> Size# r(), WB# N(x, l(), r()) -> -#(Size l(), Size r()), WB# N(x, l(), r()) -> -#(Size r(), Size l()), 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())), WB# N(x, l(), r()) -> and#(WB l(), WB r()), WB# N(x, l(), r()) -> if#(ge(Size l(), Size r()), ge(I 0(), -(Size l(), Size r())), ge(I 0(), -(Size r(), Size l()))), WB# N(x, l(), r()) -> ge#(I 0(), -(Size l(), Size r())), WB# N(x, l(), r()) -> ge#(I 0(), -(Size r(), Size l())), WB# N(x, l(), r()) -> ge#(Size l(), Size r()), WB# N(x, l(), r()) -> Size# l(), WB# N(x, l(), r()) -> Size# r(), WB# N(x, l(), r()) -> WB# l(), WB# N(x, l(), r()) -> WB# r()} TRS: { O 0() -> 0(), +(x, 0()) -> x, +(x, +(y, z)) -> +(+(x, y), z), +(0(), x) -> x, +(O x, O y) -> O +(x, y), +(O x, I y) -> I +(x, y), +(I x, O y) -> I +(x, y), +(I x, I y) -> O +(+(x, y), I 0()), -(x, 0()) -> x, -(0(), x) -> 0(), -(O x, O y) -> O -(x, y), -(O x, I y) -> I -(-(x, y), I 1()), -(I x, O y) -> I -(x, y), -(I x, I y) -> O -(x, y), not false() -> true(), not true() -> false(), and(x, false()) -> false(), and(x, true()) -> x, if(false(), x, y) -> y, if(true(), x, y) -> x, ge(x, 0()) -> true(), ge(0(), O x) -> ge(0(), x), ge(0(), I x) -> false(), ge(O x, O y) -> ge(x, y), ge(O x, I y) -> not ge(y, x), ge(I x, O y) -> ge(x, y), ge(I x, I y) -> ge(x, y), Log' 0() -> 0(), Log' O x -> if(ge(x, I 0()), +(Log' x, I 0()), 0()), Log' I x -> +(Log' x, I 0()), Log x -> -(Log' x, I 0()), Val L x -> x, Val N(x, l(), r()) -> x, Min L x -> x, Min N(x, l(), r()) -> Min l(), Max L x -> x, Max N(x, l(), r()) -> Max r(), BS L x -> true(), BS N(x, l(), r()) -> and(and(ge(x, Max l()), ge(Min r(), x)), and(BS l(), BS r())), Size L x -> I 0(), Size N(x, l(), r()) -> +(+(Size l(), Size r()), I 1()), WB L x -> true(), 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()))} EDG: {(Log'# O x -> Log'# x, Log'# I x -> Log'# x) (Log'# O x -> Log'# x, Log'# I x -> +#(Log' x, I 0())) (Log'# O x -> Log'# x, Log'# O x -> Log'# x) (Log'# O x -> Log'# x, Log'# O x -> ge#(x, I 0())) (Log'# O x -> Log'# x, Log'# O x -> if#(ge(x, I 0()), +(Log' x, I 0()), 0())) (Log'# O x -> Log'# x, Log'# O x -> +#(Log' x, I 0())) (Log# x -> Log'# x, Log'# I x -> Log'# x) (Log# x -> Log'# x, Log'# I x -> +#(Log' x, I 0())) (Log# x -> Log'# x, Log'# O x -> Log'# x) (Log# x -> Log'# x, Log'# O x -> ge#(x, I 0())) (Log# x -> Log'# x, Log'# O x -> if#(ge(x, I 0()), +(Log' x, I 0()), 0())) (Log# x -> Log'# x, Log'# O x -> +#(Log' x, I 0())) (+#(O x, O y) -> +#(x, y), +#(I x, I y) -> +#(+(x, y), I 0())) (+#(O x, O y) -> +#(x, y), +#(I x, I y) -> +#(x, y)) (+#(O x, O y) -> +#(x, y), +#(I x, I y) -> O# +(+(x, y), I 0())) (+#(O x, O y) -> +#(x, y), +#(I x, O y) -> +#(x, y)) (+#(O x, O y) -> +#(x, y), +#(O x, I y) -> +#(x, y)) (+#(O x, O y) -> +#(x, y), +#(O x, O y) -> +#(x, y)) (+#(O x, O y) -> +#(x, y), +#(O x, O y) -> O# +(x, y)) (+#(O x, O y) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z)) (+#(O x, O y) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y)) (+#(I x, O y) -> +#(x, y), +#(I x, I y) -> +#(+(x, y), I 0())) (+#(I x, O y) -> +#(x, y), +#(I x, I y) -> +#(x, y)) (+#(I x, O y) -> +#(x, y), +#(I x, I y) -> O# +(+(x, y), I 0())) (+#(I x, O y) -> +#(x, y), +#(I x, O y) -> +#(x, y)) (+#(I x, O y) -> +#(x, y), +#(O x, I y) -> +#(x, y)) (+#(I x, O y) -> +#(x, y), +#(O x, O y) -> +#(x, y)) (+#(I x, O y) -> +#(x, y), +#(O x, O y) -> O# +(x, y)) (+#(I x, O y) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z)) (+#(I x, O y) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y)) (-#(O x, O y) -> -#(x, y), -#(I x, I y) -> -#(x, y)) (-#(O x, O y) -> -#(x, y), -#(I x, I y) -> O# -(x, y)) (-#(O x, O y) -> -#(x, y), -#(I x, O y) -> -#(x, y)) (-#(O x, O y) -> -#(x, y), -#(O x, I y) -> -#(-(x, y), I 1())) (-#(O x, O y) -> -#(x, y), -#(O x, I y) -> -#(x, y)) (-#(O x, O y) -> -#(x, y), -#(O x, O y) -> -#(x, y)) (-#(O x, O y) -> -#(x, y), -#(O x, O y) -> O# -(x, y)) (-#(I x, O y) -> -#(x, y), -#(I x, I y) -> -#(x, y)) (-#(I x, O y) -> -#(x, y), -#(I x, I y) -> O# -(x, y)) (-#(I x, O y) -> -#(x, y), -#(I x, O y) -> -#(x, y)) (-#(I x, O y) -> -#(x, y), -#(O x, I y) -> -#(-(x, y), I 1())) (-#(I x, O y) -> -#(x, y), -#(O x, I y) -> -#(x, y)) (-#(I x, O y) -> -#(x, y), -#(O x, O y) -> -#(x, y)) (-#(I x, O y) -> -#(x, y), -#(O x, O y) -> O# -(x, y)) (ge#(O x, O y) -> ge#(x, y), ge#(I x, I y) -> ge#(x, y)) (ge#(O x, O y) -> ge#(x, y), ge#(I x, O y) -> ge#(x, y)) (ge#(O x, O y) -> ge#(x, y), ge#(O x, I y) -> ge#(y, x)) (ge#(O x, O y) -> ge#(x, y), ge#(O x, I y) -> not# ge(y, x)) (ge#(O x, O y) -> ge#(x, y), ge#(O x, O y) -> ge#(x, y)) (ge#(O x, O y) -> ge#(x, y), ge#(0(), O x) -> ge#(0(), x)) (ge#(I x, I y) -> ge#(x, y), ge#(I x, I y) -> ge#(x, y)) (ge#(I x, I y) -> ge#(x, y), ge#(I x, O y) -> ge#(x, y)) (ge#(I x, I y) -> ge#(x, y), ge#(O x, I y) -> ge#(y, x)) (ge#(I x, I y) -> ge#(x, y), ge#(O x, I y) -> not# ge(y, x)) (ge#(I x, I y) -> ge#(x, y), ge#(O x, O y) -> ge#(x, y)) (ge#(I x, I y) -> ge#(x, y), ge#(0(), O x) -> ge#(0(), x)) (+#(I x, I y) -> +#(+(x, y), I 0()), +#(I x, I y) -> +#(+(x, y), I 0())) (+#(I x, I y) -> +#(+(x, y), I 0()), +#(I x, I y) -> +#(x, y)) (+#(I x, I y) -> +#(+(x, y), I 0()), +#(I x, I y) -> O# +(+(x, y), I 0())) (+#(I x, I y) -> +#(+(x, y), I 0()), +#(O x, I y) -> +#(x, y)) (Log'# O x -> +#(Log' x, I 0()), +#(I x, I y) -> +#(+(x, y), I 0())) (Log'# O x -> +#(Log' x, I 0()), +#(I x, I y) -> +#(x, y)) (Log'# O x -> +#(Log' x, I 0()), +#(I x, I y) -> O# +(+(x, y), I 0())) (Log'# O x -> +#(Log' x, I 0()), +#(O x, I y) -> +#(x, y)) (Log'# I x -> +#(Log' x, I 0()), +#(I x, I y) -> +#(+(x, y), I 0())) (Log'# I x -> +#(Log' x, I 0()), +#(I x, I y) -> +#(x, y)) (Log'# I x -> +#(Log' x, I 0()), +#(I x, I y) -> O# +(+(x, y), I 0())) (Log'# I x -> +#(Log' x, I 0()), +#(O x, I y) -> +#(x, y)) (Log# x -> -#(Log' x, I 0()), -#(O x, I y) -> -#(x, y)) (Log# x -> -#(Log' x, I 0()), -#(O x, I y) -> -#(-(x, y), I 1())) (Log# x -> -#(Log' x, I 0()), -#(I x, I y) -> O# -(x, y)) (Log# x -> -#(Log' x, I 0()), -#(I x, I y) -> -#(x, y)) (Log'# O x -> ge#(x, I 0()), ge#(O x, I y) -> not# ge(y, x)) (Log'# O x -> ge#(x, I 0()), ge#(O x, I y) -> ge#(y, x)) (Log'# O x -> ge#(x, I 0()), ge#(I x, I y) -> ge#(x, y)) (-#(O x, I y) -> -#(-(x, y), I 1()), -#(O x, I y) -> -#(x, y)) (-#(O x, I y) -> -#(-(x, y), I 1()), -#(O x, I y) -> -#(-(x, y), I 1())) (-#(O x, I y) -> -#(-(x, y), I 1()), -#(I x, I y) -> O# -(x, y)) (-#(O x, I y) -> -#(-(x, y), I 1()), -#(I x, I y) -> -#(x, y)) (ge#(I x, O y) -> ge#(x, y), ge#(0(), O x) -> ge#(0(), x)) (ge#(I x, O y) -> ge#(x, y), ge#(O x, O y) -> ge#(x, y)) (ge#(I x, O y) -> ge#(x, y), ge#(O x, I y) -> not# ge(y, x)) (ge#(I x, O y) -> ge#(x, y), ge#(O x, I y) -> ge#(y, x)) (ge#(I x, O y) -> ge#(x, y), ge#(I x, O y) -> ge#(x, y)) (ge#(I x, O y) -> ge#(x, y), ge#(I x, I y) -> ge#(x, y)) (-#(I x, I y) -> -#(x, y), -#(O x, O y) -> O# -(x, y)) (-#(I x, I y) -> -#(x, y), -#(O x, O y) -> -#(x, y)) (-#(I x, I y) -> -#(x, y), -#(O x, I y) -> -#(x, y)) (-#(I x, I y) -> -#(x, y), -#(O x, I y) -> -#(-(x, y), I 1())) (-#(I x, I y) -> -#(x, y), -#(I x, O y) -> -#(x, y)) (-#(I x, I y) -> -#(x, y), -#(I x, I y) -> O# -(x, y)) (-#(I x, I y) -> -#(x, y), -#(I x, I y) -> -#(x, y)) (-#(O x, I y) -> -#(x, y), -#(O x, O y) -> O# -(x, y)) (-#(O x, I y) -> -#(x, y), -#(O x, O y) -> -#(x, y)) (-#(O x, I y) -> -#(x, y), -#(O x, I y) -> -#(x, y)) (-#(O x, I y) -> -#(x, y), -#(O x, I y) -> -#(-(x, y), I 1())) (-#(O x, I y) -> -#(x, y), -#(I x, O y) -> -#(x, y)) (-#(O x, I y) -> -#(x, y), -#(I x, I y) -> O# -(x, y)) (-#(O x, I y) -> -#(x, y), -#(I x, I y) -> -#(x, y)) (+#(I x, I y) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y)) (+#(I x, I y) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z)) (+#(I x, I y) -> +#(x, y), +#(O x, O y) -> O# +(x, y)) (+#(I x, I y) -> +#(x, y), +#(O x, O y) -> +#(x, y)) (+#(I x, I y) -> +#(x, y), +#(O x, I y) -> +#(x, y)) (+#(I x, I y) -> +#(x, y), +#(I x, O y) -> +#(x, y)) (+#(I x, I y) -> +#(x, y), +#(I x, I y) -> O# +(+(x, y), I 0())) (+#(I x, I y) -> +#(x, y), +#(I x, I y) -> +#(x, y)) (+#(I x, I y) -> +#(x, y), +#(I x, I y) -> +#(+(x, y), I 0())) (+#(O x, I y) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y)) (+#(O x, I y) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z)) (+#(O x, I y) -> +#(x, y), +#(O x, O y) -> O# +(x, y)) (+#(O x, I y) -> +#(x, y), +#(O x, O y) -> +#(x, y)) (+#(O x, I y) -> +#(x, y), +#(O x, I y) -> +#(x, y)) (+#(O x, I y) -> +#(x, y), +#(I x, O y) -> +#(x, y)) (+#(O x, I y) -> +#(x, y), +#(I x, I y) -> O# +(+(x, y), I 0())) (+#(O x, I y) -> +#(x, y), +#(I x, I y) -> +#(x, y)) (+#(O x, I y) -> +#(x, y), +#(I x, I y) -> +#(+(x, y), I 0())) (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y)) (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z)) (+#(x, +(y, z)) -> +#(x, y), +#(O x, O y) -> O# +(x, y)) (+#(x, +(y, z)) -> +#(x, y), +#(O x, O y) -> +#(x, y)) (+#(x, +(y, z)) -> +#(x, y), +#(O x, I y) -> +#(x, y)) (+#(x, +(y, z)) -> +#(x, y), +#(I x, O y) -> +#(x, y)) (+#(x, +(y, z)) -> +#(x, y), +#(I x, I y) -> O# +(+(x, y), I 0())) (+#(x, +(y, z)) -> +#(x, y), +#(I x, I y) -> +#(x, y)) (+#(x, +(y, z)) -> +#(x, y), +#(I x, I y) -> +#(+(x, y), I 0())) (ge#(0(), O x) -> ge#(0(), x), ge#(0(), O x) -> ge#(0(), x)) (+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(x, y)) (+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(+(x, y), z)) (+#(x, +(y, z)) -> +#(+(x, y), z), +#(O x, O y) -> O# +(x, y)) (+#(x, +(y, z)) -> +#(+(x, y), z), +#(O x, O y) -> +#(x, y)) (+#(x, +(y, z)) -> +#(+(x, y), z), +#(O x, I y) -> +#(x, y)) (+#(x, +(y, z)) -> +#(+(x, y), z), +#(I x, O y) -> +#(x, y)) (+#(x, +(y, z)) -> +#(+(x, y), z), +#(I x, I y) -> O# +(+(x, y), I 0())) (+#(x, +(y, z)) -> +#(+(x, y), z), +#(I x, I y) -> +#(x, y)) (+#(x, +(y, z)) -> +#(+(x, y), z), +#(I x, I y) -> +#(+(x, y), I 0())) (Log'# I x -> Log'# x, Log'# O x -> +#(Log' x, I 0())) (Log'# I x -> Log'# x, Log'# O x -> if#(ge(x, I 0()), +(Log' x, I 0()), 0())) (Log'# I x -> Log'# x, Log'# O x -> ge#(x, I 0())) (Log'# I x -> Log'# x, Log'# O x -> Log'# x) (Log'# I x -> Log'# x, Log'# I x -> +#(Log' x, I 0())) (Log'# I x -> Log'# x, Log'# I x -> Log'# x) (ge#(O x, I y) -> ge#(y, x), ge#(0(), O x) -> ge#(0(), x)) (ge#(O x, I y) -> ge#(y, x), ge#(O x, O y) -> ge#(x, y)) (ge#(O x, I y) -> ge#(y, x), ge#(O x, I y) -> not# ge(y, x)) (ge#(O x, I y) -> ge#(y, x), ge#(O x, I y) -> ge#(y, x)) (ge#(O x, I y) -> ge#(y, x), ge#(I x, O y) -> ge#(x, y)) (ge#(O x, I y) -> ge#(y, x), ge#(I x, I y) -> ge#(x, y))} SCCS (5): Scc: {Log'# O x -> Log'# x, Log'# I x -> Log'# x} Scc: {ge#(O x, O y) -> ge#(x, y), ge#(O x, I y) -> ge#(y, x), ge#(I x, O y) -> ge#(x, y), ge#(I x, I y) -> ge#(x, y)} Scc: {ge#(0(), O x) -> ge#(0(), x)} Scc: {-#(O x, O y) -> -#(x, y), -#(O x, I y) -> -#(x, y), -#(O x, I y) -> -#(-(x, y), I 1()), -#(I x, O y) -> -#(x, y), -#(I x, I y) -> -#(x, y)} Scc: {+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z), +#(O x, O y) -> +#(x, y), +#(O x, I y) -> +#(x, y), +#(I x, O y) -> +#(x, y), +#(I x, I y) -> +#(x, y), +#(I x, I y) -> +#(+(x, y), I 0())} SCC (2): Strict: {Log'# O x -> Log'# x, Log'# I x -> Log'# x} Weak: { O 0() -> 0(), +(x, 0()) -> x, +(x, +(y, z)) -> +(+(x, y), z), +(0(), x) -> x, +(O x, O y) -> O +(x, y), +(O x, I y) -> I +(x, y), +(I x, O y) -> I +(x, y), +(I x, I y) -> O +(+(x, y), I 0()), -(x, 0()) -> x, -(0(), x) -> 0(), -(O x, O y) -> O -(x, y), -(O x, I y) -> I -(-(x, y), I 1()), -(I x, O y) -> I -(x, y), -(I x, I y) -> O -(x, y), not false() -> true(), not true() -> false(), and(x, false()) -> false(), and(x, true()) -> x, if(false(), x, y) -> y, if(true(), x, y) -> x, ge(x, 0()) -> true(), ge(0(), O x) -> ge(0(), x), ge(0(), I x) -> false(), ge(O x, O y) -> ge(x, y), ge(O x, I y) -> not ge(y, x), ge(I x, O y) -> ge(x, y), ge(I x, I y) -> ge(x, y), Log' 0() -> 0(), Log' O x -> if(ge(x, I 0()), +(Log' x, I 0()), 0()), Log' I x -> +(Log' x, I 0()), Log x -> -(Log' x, I 0()), Val L x -> x, Val N(x, l(), r()) -> x, Min L x -> x, Min N(x, l(), r()) -> Min l(), Max L x -> x, Max N(x, l(), r()) -> Max r(), BS L x -> true(), BS N(x, l(), r()) -> and(and(ge(x, Max l()), ge(Min r(), x)), and(BS l(), BS r())), Size L x -> I 0(), Size N(x, l(), r()) -> +(+(Size l(), Size r()), I 1()), WB L x -> true(), 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()))} SPSC: Simple Projection: pi(Log'#) = 0 Strict: {Log'# I x -> Log'# x} EDG: {(Log'# I x -> Log'# x, Log'# I x -> Log'# x)} SCCS (1): Scc: {Log'# I x -> Log'# x} SCC (1): Strict: {Log'# I x -> Log'# x} Weak: { O 0() -> 0(), +(x, 0()) -> x, +(x, +(y, z)) -> +(+(x, y), z), +(0(), x) -> x, +(O x, O y) -> O +(x, y), +(O x, I y) -> I +(x, y), +(I x, O y) -> I +(x, y), +(I x, I y) -> O +(+(x, y), I 0()), -(x, 0()) -> x, -(0(), x) -> 0(), -(O x, O y) -> O -(x, y), -(O x, I y) -> I -(-(x, y), I 1()), -(I x, O y) -> I -(x, y), -(I x, I y) -> O -(x, y), not false() -> true(), not true() -> false(), and(x, false()) -> false(), and(x, true()) -> x, if(false(), x, y) -> y, if(true(), x, y) -> x, ge(x, 0()) -> true(), ge(0(), O x) -> ge(0(), x), ge(0(), I x) -> false(), ge(O x, O y) -> ge(x, y), ge(O x, I y) -> not ge(y, x), ge(I x, O y) -> ge(x, y), ge(I x, I y) -> ge(x, y), Log' 0() -> 0(), Log' O x -> if(ge(x, I 0()), +(Log' x, I 0()), 0()), Log' I x -> +(Log' x, I 0()), Log x -> -(Log' x, I 0()), Val L x -> x, Val N(x, l(), r()) -> x, Min L x -> x, Min N(x, l(), r()) -> Min l(), Max L x -> x, Max N(x, l(), r()) -> Max r(), BS L x -> true(), BS N(x, l(), r()) -> and(and(ge(x, Max l()), ge(Min r(), x)), and(BS l(), BS r())), Size L x -> I 0(), Size N(x, l(), r()) -> +(+(Size l(), Size r()), I 1()), WB L x -> true(), 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()))} SPSC: Simple Projection: pi(Log'#) = 0 Strict: {} Qed SCC (4): Strict: {ge#(O x, O y) -> ge#(x, y), ge#(O x, I y) -> ge#(y, x), ge#(I x, O y) -> ge#(x, y), ge#(I x, I y) -> ge#(x, y)} Weak: { O 0() -> 0(), +(x, 0()) -> x, +(x, +(y, z)) -> +(+(x, y), z), +(0(), x) -> x, +(O x, O y) -> O +(x, y), +(O x, I y) -> I +(x, y), +(I x, O y) -> I +(x, y), +(I x, I y) -> O +(+(x, y), I 0()), -(x, 0()) -> x, -(0(), x) -> 0(), -(O x, O y) -> O -(x, y), -(O x, I y) -> I -(-(x, y), I 1()), -(I x, O y) -> I -(x, y), -(I x, I y) -> O -(x, y), not false() -> true(), not true() -> false(), and(x, false()) -> false(), and(x, true()) -> x, if(false(), x, y) -> y, if(true(), x, y) -> x, ge(x, 0()) -> true(), ge(0(), O x) -> ge(0(), x), ge(0(), I x) -> false(), ge(O x, O y) -> ge(x, y), ge(O x, I y) -> not ge(y, x), ge(I x, O y) -> ge(x, y), ge(I x, I y) -> ge(x, y), Log' 0() -> 0(), Log' O x -> if(ge(x, I 0()), +(Log' x, I 0()), 0()), Log' I x -> +(Log' x, I 0()), Log x -> -(Log' x, I 0()), Val L x -> x, Val N(x, l(), r()) -> x, Min L x -> x, Min N(x, l(), r()) -> Min l(), Max L x -> x, Max N(x, l(), r()) -> Max r(), BS L x -> true(), BS N(x, l(), r()) -> and(and(ge(x, Max l()), ge(Min r(), x)), and(BS l(), BS r())), Size L x -> I 0(), Size N(x, l(), r()) -> +(+(Size l(), Size r()), I 1()), WB L x -> true(), 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()))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [N](x0, x1, x2) = 1, [+](x0, x1) = x0 + x1 + 1, [-](x0, x1) = x0 + x1 + 1, [and](x0, x1) = x0 + 1, [ge](x0, x1) = 0, [O](x0) = x0 + 1, [I](x0) = x0 + 1, [not](x0) = x0 + 1, [Log'](x0) = x0 + 1, [Log](x0) = 0, [Val](x0) = x0 + 1, [L](x0) = 1, [Min](x0) = x0 + 1, [Max](x0) = x0 + 1, [BS](x0) = 0, [Size](x0) = x0 + 1, [WB](x0) = 0, [0] = 1, [1] = 1, [false] = 1, [true] = 1, [l] = 1, [r] = 1, [ge#](x0, x1) = x0 + x1 + 1 Strict: ge#(I x, I y) -> ge#(x, y) 3 + 1x + 1y >= 1 + 1x + 1y ge#(I x, O y) -> ge#(x, y) 3 + 1x + 1y >= 1 + 1x + 1y ge#(O x, I y) -> ge#(y, x) 3 + 1x + 1y >= 1 + 1x + 1y ge#(O x, O y) -> ge#(x, y) 3 + 1x + 1y >= 1 + 1x + 1y Weak: Qed SCC (1): Strict: {ge#(0(), O x) -> ge#(0(), x)} Weak: { O 0() -> 0(), +(x, 0()) -> x, +(x, +(y, z)) -> +(+(x, y), z), +(0(), x) -> x, +(O x, O y) -> O +(x, y), +(O x, I y) -> I +(x, y), +(I x, O y) -> I +(x, y), +(I x, I y) -> O +(+(x, y), I 0()), -(x, 0()) -> x, -(0(), x) -> 0(), -(O x, O y) -> O -(x, y), -(O x, I y) -> I -(-(x, y), I 1()), -(I x, O y) -> I -(x, y), -(I x, I y) -> O -(x, y), not false() -> true(), not true() -> false(), and(x, false()) -> false(), and(x, true()) -> x, if(false(), x, y) -> y, if(true(), x, y) -> x, ge(x, 0()) -> true(), ge(0(), O x) -> ge(0(), x), ge(0(), I x) -> false(), ge(O x, O y) -> ge(x, y), ge(O x, I y) -> not ge(y, x), ge(I x, O y) -> ge(x, y), ge(I x, I y) -> ge(x, y), Log' 0() -> 0(), Log' O x -> if(ge(x, I 0()), +(Log' x, I 0()), 0()), Log' I x -> +(Log' x, I 0()), Log x -> -(Log' x, I 0()), Val L x -> x, Val N(x, l(), r()) -> x, Min L x -> x, Min N(x, l(), r()) -> Min l(), Max L x -> x, Max N(x, l(), r()) -> Max r(), BS L x -> true(), BS N(x, l(), r()) -> and(and(ge(x, Max l()), ge(Min r(), x)), and(BS l(), BS r())), Size L x -> I 0(), Size N(x, l(), r()) -> +(+(Size l(), Size r()), I 1()), WB L x -> true(), 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()))} SPSC: Simple Projection: pi(ge#) = 1 Strict: {} Qed SCC (5): Strict: {-#(O x, O y) -> -#(x, y), -#(O x, I y) -> -#(x, y), -#(O x, I y) -> -#(-(x, y), I 1()), -#(I x, O y) -> -#(x, y), -#(I x, I y) -> -#(x, y)} Weak: { O 0() -> 0(), +(x, 0()) -> x, +(x, +(y, z)) -> +(+(x, y), z), +(0(), x) -> x, +(O x, O y) -> O +(x, y), +(O x, I y) -> I +(x, y), +(I x, O y) -> I +(x, y), +(I x, I y) -> O +(+(x, y), I 0()), -(x, 0()) -> x, -(0(), x) -> 0(), -(O x, O y) -> O -(x, y), -(O x, I y) -> I -(-(x, y), I 1()), -(I x, O y) -> I -(x, y), -(I x, I y) -> O -(x, y), not false() -> true(), not true() -> false(), and(x, false()) -> false(), and(x, true()) -> x, if(false(), x, y) -> y, if(true(), x, y) -> x, ge(x, 0()) -> true(), ge(0(), O x) -> ge(0(), x), ge(0(), I x) -> false(), ge(O x, O y) -> ge(x, y), ge(O x, I y) -> not ge(y, x), ge(I x, O y) -> ge(x, y), ge(I x, I y) -> ge(x, y), Log' 0() -> 0(), Log' O x -> if(ge(x, I 0()), +(Log' x, I 0()), 0()), Log' I x -> +(Log' x, I 0()), Log x -> -(Log' x, I 0()), Val L x -> x, Val N(x, l(), r()) -> x, Min L x -> x, Min N(x, l(), r()) -> Min l(), Max L x -> x, Max N(x, l(), r()) -> Max r(), BS L x -> true(), BS N(x, l(), r()) -> and(and(ge(x, Max l()), ge(Min r(), x)), and(BS l(), BS r())), Size L x -> I 0(), Size N(x, l(), r()) -> +(+(Size l(), Size r()), I 1()), WB L x -> true(), 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()))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + 1, [N](x0, x1, x2) = 1, [+](x0, x1) = x0 + x1 + 1, [-](x0, x1) = x0, [and](x0, x1) = x0 + x1 + 1, [ge](x0, x1) = x0 + 1, [O](x0) = x0 + 1, [I](x0) = x0 + 1, [not](x0) = x0 + 1, [Log'](x0) = x0 + 1, [Log](x0) = 0, [Val](x0) = x0 + 1, [L](x0) = 1, [Min](x0) = x0 + 1, [Max](x0) = x0 + 1, [BS](x0) = 0, [Size](x0) = 0, [WB](x0) = 0, [0] = 1, [1] = 0, [false] = 1, [true] = 1, [l] = 1, [r] = 1, [-#](x0, x1) = x0 + 1 Strict: -#(I x, I y) -> -#(x, y) 2 + 1x + 0y >= 1 + 1x + 0y -#(I x, O y) -> -#(x, y) 2 + 1x + 0y >= 1 + 1x + 0y -#(O x, I y) -> -#(-(x, y), I 1()) 2 + 1x + 0y >= 1 + 1x + 0y -#(O x, I y) -> -#(x, y) 2 + 1x + 0y >= 1 + 1x + 0y -#(O x, O y) -> -#(x, y) 2 + 1x + 0y >= 1 + 1x + 0y Weak: Qed SCC (7): Strict: {+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z), +#(O x, O y) -> +#(x, y), +#(O x, I y) -> +#(x, y), +#(I x, O y) -> +#(x, y), +#(I x, I y) -> +#(x, y), +#(I x, I y) -> +#(+(x, y), I 0())} Weak: { O 0() -> 0(), +(x, 0()) -> x, +(x, +(y, z)) -> +(+(x, y), z), +(0(), x) -> x, +(O x, O y) -> O +(x, y), +(O x, I y) -> I +(x, y), +(I x, O y) -> I +(x, y), +(I x, I y) -> O +(+(x, y), I 0()), -(x, 0()) -> x, -(0(), x) -> 0(), -(O x, O y) -> O -(x, y), -(O x, I y) -> I -(-(x, y), I 1()), -(I x, O y) -> I -(x, y), -(I x, I y) -> O -(x, y), not false() -> true(), not true() -> false(), and(x, false()) -> false(), and(x, true()) -> x, if(false(), x, y) -> y, if(true(), x, y) -> x, ge(x, 0()) -> true(), ge(0(), O x) -> ge(0(), x), ge(0(), I x) -> false(), ge(O x, O y) -> ge(x, y), ge(O x, I y) -> not ge(y, x), ge(I x, O y) -> ge(x, y), ge(I x, I y) -> ge(x, y), Log' 0() -> 0(), Log' O x -> if(ge(x, I 0()), +(Log' x, I 0()), 0()), Log' I x -> +(Log' x, I 0()), Log x -> -(Log' x, I 0()), Val L x -> x, Val N(x, l(), r()) -> x, Min L x -> x, Min N(x, l(), r()) -> Min l(), Max L x -> x, Max N(x, l(), r()) -> Max r(), BS L x -> true(), BS N(x, l(), r()) -> and(and(ge(x, Max l()), ge(Min r(), x)), and(BS l(), BS r())), Size L x -> I 0(), Size N(x, l(), r()) -> +(+(Size l(), Size r()), I 1()), WB L x -> true(), 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()))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = 0, [N](x0, x1, x2) = 1, [+](x0, x1) = x0 + x1, [-](x0, x1) = 0, [and](x0, x1) = x0 + 1, [ge](x0, x1) = 0, [O](x0) = x0 + 1, [I](x0) = x0, [not](x0) = x0 + 1, [Log'](x0) = 0, [Log](x0) = 0, [Val](x0) = x0 + 1, [L](x0) = 1, [Min](x0) = x0 + 1, [Max](x0) = x0 + 1, [BS](x0) = x0 + 1, [Size](x0) = x0 + 1, [WB](x0) = x0 + 1, [0] = 0, [1] = 0, [false] = 1, [true] = 1, [l] = 1, [r] = 1, [+#](x0, x1) = x0 Strict: +#(I x, I y) -> +#(+(x, y), I 0()) 0 + 0x + 1y >= 0 + 0x + 0y +#(I x, I y) -> +#(x, y) 0 + 0x + 1y >= 0 + 0x + 1y +#(I x, O y) -> +#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y +#(O x, I y) -> +#(x, y) 0 + 0x + 1y >= 0 + 0x + 1y +#(O x, O y) -> +#(x, y) 1 + 0x + 1y >= 0 + 0x + 1y +#(x, +(y, z)) -> +#(+(x, y), z) 0 + 0x + 1y + 1z >= 0 + 0x + 0y + 1z +#(x, +(y, z)) -> +#(x, y) 0 + 0x + 1y + 1z >= 0 + 0x + 1y Weak: EDG: {(+#(x, +(y, z)) -> +#(x, y), +#(I x, I y) -> +#(+(x, y), I 0())) (+#(x, +(y, z)) -> +#(x, y), +#(I x, I y) -> +#(x, y)) (+#(x, +(y, z)) -> +#(x, y), +#(O x, I y) -> +#(x, y)) (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z)) (+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y)) (+#(I x, I y) -> +#(x, y), +#(I x, I y) -> +#(+(x, y), I 0())) (+#(I x, I y) -> +#(x, y), +#(I x, I y) -> +#(x, y)) (+#(I x, I y) -> +#(x, y), +#(O x, I y) -> +#(x, y)) (+#(I x, I y) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z)) (+#(I x, I y) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y)) (+#(I x, I y) -> +#(+(x, y), I 0()), +#(O x, I y) -> +#(x, y)) (+#(I x, I y) -> +#(+(x, y), I 0()), +#(I x, I y) -> +#(x, y)) (+#(I x, I y) -> +#(+(x, y), I 0()), +#(I x, I y) -> +#(+(x, y), I 0())) (+#(O x, I y) -> +#(x, y), +#(x, +(y, z)) -> +#(x, y)) (+#(O x, I y) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z)) (+#(O x, I y) -> +#(x, y), +#(O x, I y) -> +#(x, y)) (+#(O x, I y) -> +#(x, y), +#(I x, I y) -> +#(x, y)) (+#(O x, I y) -> +#(x, y), +#(I x, I y) -> +#(+(x, y), I 0())) (+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(x, y)) (+#(x, +(y, z)) -> +#(+(x, y), z), +#(x, +(y, z)) -> +#(+(x, y), z)) (+#(x, +(y, z)) -> +#(+(x, y), z), +#(O x, I y) -> +#(x, y)) (+#(x, +(y, z)) -> +#(+(x, y), z), +#(I x, I y) -> +#(x, y)) (+#(x, +(y, z)) -> +#(+(x, y), z), +#(I x, I y) -> +#(+(x, y), I 0()))} SCCS (1): Scc: {+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z), +#(O x, I y) -> +#(x, y), +#(I x, I y) -> +#(x, y), +#(I x, I y) -> +#(+(x, y), I 0())} SCC (5): Strict: {+#(x, +(y, z)) -> +#(x, y), +#(x, +(y, z)) -> +#(+(x, y), z), +#(O x, I y) -> +#(x, y), +#(I x, I y) -> +#(x, y), +#(I x, I y) -> +#(+(x, y), I 0())} Weak: { O 0() -> 0(), +(x, 0()) -> x, +(x, +(y, z)) -> +(+(x, y), z), +(0(), x) -> x, +(O x, O y) -> O +(x, y), +(O x, I y) -> I +(x, y), +(I x, O y) -> I +(x, y), +(I x, I y) -> O +(+(x, y), I 0()), -(x, 0()) -> x, -(0(), x) -> 0(), -(O x, O y) -> O -(x, y), -(O x, I y) -> I -(-(x, y), I 1()), -(I x, O y) -> I -(x, y), -(I x, I y) -> O -(x, y), not false() -> true(), not true() -> false(), and(x, false()) -> false(), and(x, true()) -> x, if(false(), x, y) -> y, if(true(), x, y) -> x, ge(x, 0()) -> true(), ge(0(), O x) -> ge(0(), x), ge(0(), I x) -> false(), ge(O x, O y) -> ge(x, y), ge(O x, I y) -> not ge(y, x), ge(I x, O y) -> ge(x, y), ge(I x, I y) -> ge(x, y), Log' 0() -> 0(), Log' O x -> if(ge(x, I 0()), +(Log' x, I 0()), 0()), Log' I x -> +(Log' x, I 0()), Log x -> -(Log' x, I 0()), Val L x -> x, Val N(x, l(), r()) -> x, Min L x -> x, Min N(x, l(), r()) -> Min l(), Max L x -> x, Max N(x, l(), r()) -> Max r(), BS L x -> true(), BS N(x, l(), r()) -> and(and(ge(x, Max l()), ge(Min r(), x)), and(BS l(), BS r())), Size L x -> I 0(), Size N(x, l(), r()) -> +(+(Size l(), Size r()), I 1()), WB L x -> true(), 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()))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + x1 + 1, [N](x0, x1, x2) = 1, [+](x0, x1) = x0 + x1 + 1, [-](x0, x1) = 0, [and](x0, x1) = x0 + 1, [ge](x0, x1) = 0, [O](x0) = 0, [I](x0) = x0, [not](x0) = x0 + 1, [Log'](x0) = 0, [Log](x0) = 0, [Val](x0) = x0 + 1, [L](x0) = 1, [Min](x0) = x0 + 1, [Max](x0) = x0 + 1, [BS](x0) = 0, [Size](x0) = x0 + 1, [WB](x0) = x0 + 1, [0] = 0, [1] = 0, [false] = 1, [true] = 1, [l] = 1, [r] = 1, [+#](x0, x1) = x0 Strict: +#(I x, I y) -> +#(+(x, y), I 0()) 0 + 0x + 1y >= 0 + 0x + 0y +#(I x, I y) -> +#(x, y) 0 + 0x + 1y >= 0 + 0x + 1y +#(O x, I y) -> +#(x, y) 0 + 0x + 1y >= 0 + 0x + 1y +#(x, +(y, z)) -> +#(+(x, y), z) 1 + 0x + 1y + 1z >= 0 + 0x + 0y + 1z +#(x, +(y, z)) -> +#(x, y) 1 + 0x + 1y + 1z >= 0 + 0x + 1y Weak: EDG: {(+#(I x, I y) -> +#(x, y), +#(I x, I y) -> +#(+(x, y), I 0())) (+#(I x, I y) -> +#(x, y), +#(I x, I y) -> +#(x, y)) (+#(I x, I y) -> +#(x, y), +#(O x, I y) -> +#(x, y)) (+#(I x, I y) -> +#(+(x, y), I 0()), +#(O x, I y) -> +#(x, y)) (+#(I x, I y) -> +#(+(x, y), I 0()), +#(I x, I y) -> +#(x, y)) (+#(I x, I y) -> +#(+(x, y), I 0()), +#(I x, I y) -> +#(+(x, y), I 0())) (+#(O x, I y) -> +#(x, y), +#(O x, I y) -> +#(x, y)) (+#(O x, I y) -> +#(x, y), +#(I x, I y) -> +#(x, y)) (+#(O x, I y) -> +#(x, y), +#(I x, I y) -> +#(+(x, y), I 0()))} SCCS (1): Scc: {+#(O x, I y) -> +#(x, y), +#(I x, I y) -> +#(x, y), +#(I x, I y) -> +#(+(x, y), I 0())} SCC (3): Strict: {+#(O x, I y) -> +#(x, y), +#(I x, I y) -> +#(x, y), +#(I x, I y) -> +#(+(x, y), I 0())} Weak: { O 0() -> 0(), +(x, 0()) -> x, +(x, +(y, z)) -> +(+(x, y), z), +(0(), x) -> x, +(O x, O y) -> O +(x, y), +(O x, I y) -> I +(x, y), +(I x, O y) -> I +(x, y), +(I x, I y) -> O +(+(x, y), I 0()), -(x, 0()) -> x, -(0(), x) -> 0(), -(O x, O y) -> O -(x, y), -(O x, I y) -> I -(-(x, y), I 1()), -(I x, O y) -> I -(x, y), -(I x, I y) -> O -(x, y), not false() -> true(), not true() -> false(), and(x, false()) -> false(), and(x, true()) -> x, if(false(), x, y) -> y, if(true(), x, y) -> x, ge(x, 0()) -> true(), ge(0(), O x) -> ge(0(), x), ge(0(), I x) -> false(), ge(O x, O y) -> ge(x, y), ge(O x, I y) -> not ge(y, x), ge(I x, O y) -> ge(x, y), ge(I x, I y) -> ge(x, y), Log' 0() -> 0(), Log' O x -> if(ge(x, I 0()), +(Log' x, I 0()), 0()), Log' I x -> +(Log' x, I 0()), Log x -> -(Log' x, I 0()), Val L x -> x, Val N(x, l(), r()) -> x, Min L x -> x, Min N(x, l(), r()) -> Min l(), Max L x -> x, Max N(x, l(), r()) -> Max r(), BS L x -> true(), BS N(x, l(), r()) -> and(and(ge(x, Max l()), ge(Min r(), x)), and(BS l(), BS r())), Size L x -> I 0(), Size N(x, l(), r()) -> +(+(Size l(), Size r()), I 1()), WB L x -> true(), 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()))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2) = x0 + x1 + 1, [N](x0, x1, x2) = 1, [+](x0, x1) = x0 + x1, [-](x0, x1) = x0, [and](x0, x1) = x0 + 1, [ge](x0, x1) = 0, [O](x0) = x0, [I](x0) = x0 + 1, [not](x0) = x0 + 1, [Log'](x0) = 0, [Log](x0) = 0, [Val](x0) = x0 + 1, [L](x0) = 1, [Min](x0) = x0 + 1, [Max](x0) = x0 + 1, [BS](x0) = 0, [Size](x0) = 0, [WB](x0) = 0, [0] = 0, [1] = 1, [false] = 1, [true] = 1, [l] = 1, [r] = 1, [+#](x0, x1) = x0 + x1 Strict: +#(I x, I y) -> +#(+(x, y), I 0()) 2 + 1x + 1y >= 1 + 1x + 1y +#(I x, I y) -> +#(x, y) 2 + 1x + 1y >= 0 + 1x + 1y +#(O x, I y) -> +#(x, y) 1 + 1x + 1y >= 0 + 1x + 1y Weak: Qed