YES Time: 0.642476 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()))} UR: { 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()), a(w, v) -> w, a(w, v) -> v} 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())) (Min# N(x, l(), r()) -> Min# l(), Min# N(x, l(), r()) -> Min# l()) (BS# N(x, l(), r()) -> Min# r(), Min# N(x, l(), r()) -> Min# l()) (BS# N(x, l(), r()) -> BS# l(), BS# N(x, l(), r()) -> BS# r()) (BS# N(x, l(), r()) -> BS# l(), BS# N(x, l(), r()) -> BS# l()) (BS# N(x, l(), r()) -> BS# l(), BS# N(x, l(), r()) -> Max# l()) (BS# N(x, l(), r()) -> BS# l(), BS# N(x, l(), r()) -> Min# r()) (BS# N(x, l(), r()) -> BS# l(), BS# N(x, l(), r()) -> ge#(Min r(), x)) (BS# N(x, l(), r()) -> BS# l(), BS# N(x, l(), r()) -> ge#(x, Max l())) (BS# N(x, l(), r()) -> BS# l(), BS# N(x, l(), r()) -> and#(BS l(), BS r())) (BS# N(x, l(), r()) -> BS# l(), BS# N(x, l(), r()) -> and#(ge(x, Max l()), ge(Min r(), x))) (BS# N(x, l(), r()) -> BS# l(), BS# N(x, l(), r()) -> and#(and(ge(x, Max l()), ge(Min r(), x)), and(BS l(), BS r()))) (Size# N(x, l(), r()) -> Size# l(), Size# N(x, l(), r()) -> Size# r()) (Size# N(x, l(), r()) -> Size# l(), Size# N(x, l(), r()) -> Size# l()) (Size# N(x, l(), r()) -> Size# l(), Size# N(x, l(), r()) -> +#(Size l(), Size r())) (Size# N(x, l(), r()) -> Size# l(), Size# N(x, l(), r()) -> +#(+(Size l(), Size r()), I 1())) (WB# N(x, l(), r()) -> Size# l(), Size# N(x, l(), r()) -> Size# r()) (WB# N(x, l(), r()) -> Size# l(), Size# N(x, l(), r()) -> Size# l()) (WB# N(x, l(), r()) -> Size# l(), Size# N(x, l(), r()) -> +#(Size l(), Size r())) (WB# N(x, l(), r()) -> Size# l(), Size# N(x, l(), r()) -> +#(+(Size l(), Size r()), I 1())) (WB# N(x, l(), r()) -> WB# l(), WB# N(x, l(), r()) -> WB# r()) (WB# N(x, l(), r()) -> WB# l(), WB# N(x, l(), r()) -> WB# l()) (WB# N(x, l(), r()) -> WB# l(), WB# N(x, l(), r()) -> Size# r()) (WB# N(x, l(), r()) -> WB# l(), WB# N(x, l(), r()) -> Size# l()) (WB# N(x, l(), r()) -> WB# l(), WB# N(x, l(), r()) -> ge#(Size l(), Size r())) (WB# N(x, l(), r()) -> WB# l(), WB# N(x, l(), r()) -> ge#(I 0(), -(Size r(), Size l()))) (WB# N(x, l(), r()) -> WB# l(), WB# N(x, l(), r()) -> ge#(I 0(), -(Size l(), Size r()))) (WB# N(x, l(), r()) -> WB# l(), 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()) -> WB# l(), WB# N(x, l(), r()) -> and#(WB l(), WB r())) (WB# N(x, l(), r()) -> WB# 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()) -> WB# l(), WB# N(x, l(), r()) -> -#(Size r(), Size l())) (WB# N(x, l(), r()) -> WB# l(), WB# N(x, l(), r()) -> -#(Size l(), Size r())) (WB# N(x, l(), r()) -> ge#(I 0(), -(Size l(), Size r())), ge#(I x, I y) -> ge#(x, y)) (WB# N(x, l(), r()) -> ge#(I 0(), -(Size l(), Size r())), ge#(I x, O y) -> ge#(x, y)) (WB# N(x, l(), r()) -> ge#(I 0(), -(Size l(), Size r())), ge#(O x, I y) -> ge#(y, x)) (WB# N(x, l(), r()) -> ge#(I 0(), -(Size l(), Size r())), ge#(O x, I y) -> not# ge(y, x)) (WB# N(x, l(), r()) -> ge#(I 0(), -(Size l(), Size r())), ge#(O x, O y) -> ge#(x, y)) (WB# N(x, l(), r()) -> ge#(I 0(), -(Size l(), Size r())), ge#(0(), O x) -> ge#(0(), x)) (+#(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()), +#(I x, O 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()), +#(O x, O y) -> +#(x, y)) (+#(I x, I y) -> +#(+(x, y), I 0()), +#(O x, O y) -> O# +(x, y)) (+#(I x, I y) -> +#(+(x, y), I 0()), +#(x, +(y, z)) -> +#(+(x, y), z)) (+#(I x, I y) -> +#(+(x, y), I 0()), +#(x, +(y, z)) -> +#(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()), +#(I x, O y) -> +#(x, y)) (Log'# O x -> +#(Log' x, I 0()), +#(O x, I y) -> +#(x, y)) (Log'# O x -> +#(Log' x, I 0()), +#(O x, O y) -> +#(x, y)) (Log'# O x -> +#(Log' x, I 0()), +#(O x, O y) -> O# +(x, y)) (Log'# O x -> +#(Log' x, I 0()), +#(x, +(y, z)) -> +#(+(x, y), z)) (Log'# O x -> +#(Log' x, I 0()), +#(x, +(y, z)) -> +#(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()), +#(I x, O y) -> +#(x, y)) (Log'# I x -> +#(Log' x, I 0()), +#(O x, I y) -> +#(x, y)) (Log'# I x -> +#(Log' x, I 0()), +#(O x, O y) -> +#(x, y)) (Log'# I x -> +#(Log' x, I 0()), +#(O x, O y) -> O# +(x, y)) (Log'# I x -> +#(Log' x, I 0()), +#(x, +(y, z)) -> +#(+(x, y), z)) (Log'# I x -> +#(Log' x, I 0()), +#(x, +(y, z)) -> +#(x, y)) (Size# N(x, l(), r()) -> +#(+(Size l(), Size r()), I 1()), +#(I x, I y) -> +#(+(x, y), I 0())) (Size# N(x, l(), r()) -> +#(+(Size l(), Size r()), I 1()), +#(I x, I y) -> +#(x, y)) (Size# N(x, l(), r()) -> +#(+(Size l(), Size r()), I 1()), +#(I x, I y) -> O# +(+(x, y), I 0())) (Size# N(x, l(), r()) -> +#(+(Size l(), Size r()), I 1()), +#(I x, O y) -> +#(x, y)) (Size# N(x, l(), r()) -> +#(+(Size l(), Size r()), I 1()), +#(O x, I y) -> +#(x, y)) (Size# N(x, l(), r()) -> +#(+(Size l(), Size r()), I 1()), +#(O x, O y) -> +#(x, y)) (Size# N(x, l(), r()) -> +#(+(Size l(), Size r()), I 1()), +#(O x, O y) -> O# +(x, y)) (Size# N(x, l(), r()) -> +#(+(Size l(), Size r()), I 1()), +#(x, +(y, z)) -> +#(+(x, y), z)) (Size# N(x, l(), r()) -> +#(+(Size l(), Size r()), I 1()), +#(x, +(y, z)) -> +#(x, y)) (WB# N(x, l(), r()) -> -#(Size l(), Size r()), -#(I x, I y) -> -#(x, y)) (WB# N(x, l(), r()) -> -#(Size l(), Size r()), -#(I x, I y) -> O# -(x, y)) (WB# N(x, l(), r()) -> -#(Size l(), Size r()), -#(I x, O y) -> -#(x, y)) (WB# N(x, l(), r()) -> -#(Size l(), Size r()), -#(O x, I y) -> -#(-(x, y), I 1())) (WB# N(x, l(), r()) -> -#(Size l(), Size r()), -#(O x, I y) -> -#(x, y)) (WB# N(x, l(), r()) -> -#(Size l(), Size r()), -#(O x, O y) -> -#(x, y)) (WB# N(x, l(), r()) -> -#(Size l(), Size r()), -#(O x, O y) -> O# -(x, y)) (WB# N(x, l(), r()) -> ge#(Size l(), Size r()), ge#(0(), O x) -> ge#(0(), x)) (WB# N(x, l(), r()) -> ge#(Size l(), Size r()), ge#(O x, O y) -> ge#(x, y)) (WB# N(x, l(), r()) -> ge#(Size l(), Size r()), ge#(O x, I y) -> not# ge(y, x)) (WB# N(x, l(), r()) -> ge#(Size l(), Size r()), ge#(O x, I y) -> ge#(y, x)) (WB# N(x, l(), r()) -> ge#(Size l(), Size r()), ge#(I x, O y) -> ge#(x, y)) (WB# N(x, l(), r()) -> ge#(Size l(), Size r()), ge#(I x, I y) -> ge#(x, y)) (WB# N(x, l(), r()) -> -#(Size r(), Size l()), -#(O x, O y) -> O# -(x, y)) (WB# N(x, l(), r()) -> -#(Size r(), Size l()), -#(O x, O y) -> -#(x, y)) (WB# N(x, l(), r()) -> -#(Size r(), Size l()), -#(O x, I y) -> -#(x, y)) (WB# N(x, l(), r()) -> -#(Size r(), Size l()), -#(O x, I y) -> -#(-(x, y), I 1())) (WB# N(x, l(), r()) -> -#(Size r(), Size l()), -#(I x, O y) -> -#(x, y)) (WB# N(x, l(), r()) -> -#(Size r(), Size l()), -#(I x, I y) -> O# -(x, y)) (WB# N(x, l(), r()) -> -#(Size r(), Size l()), -#(I x, I y) -> -#(x, y)) (Size# N(x, l(), r()) -> +#(Size l(), Size r()), +#(x, +(y, z)) -> +#(x, y)) (Size# N(x, l(), r()) -> +#(Size l(), Size r()), +#(x, +(y, z)) -> +#(+(x, y), z)) (Size# N(x, l(), r()) -> +#(Size l(), Size r()), +#(O x, O y) -> O# +(x, y)) (Size# N(x, l(), r()) -> +#(Size l(), Size r()), +#(O x, O y) -> +#(x, y)) (Size# N(x, l(), r()) -> +#(Size l(), Size r()), +#(O x, I y) -> +#(x, y)) (Size# N(x, l(), r()) -> +#(Size l(), Size r()), +#(I x, O y) -> +#(x, y)) (Size# N(x, l(), r()) -> +#(Size l(), Size r()), +#(I x, I y) -> O# +(+(x, y), I 0())) (Size# N(x, l(), r()) -> +#(Size l(), Size r()), +#(I x, I y) -> +#(x, y)) (Size# N(x, l(), r()) -> +#(Size l(), Size r()), +#(I x, I y) -> +#(+(x, y), I 0())) (BS# N(x, l(), r()) -> ge#(x, Max l()), ge#(0(), O x) -> ge#(0(), x)) (BS# N(x, l(), r()) -> ge#(x, Max l()), ge#(O x, O y) -> ge#(x, y)) (BS# N(x, l(), r()) -> ge#(x, Max l()), ge#(O x, I y) -> not# ge(y, x)) (BS# N(x, l(), r()) -> ge#(x, Max l()), ge#(O x, I y) -> ge#(y, x)) (BS# N(x, l(), r()) -> ge#(x, Max l()), ge#(I x, O y) -> ge#(x, y)) (BS# N(x, l(), r()) -> ge#(x, Max l()), ge#(I x, I y) -> ge#(x, y)) (Log# x -> -#(Log' x, I 0()), -#(O x, O y) -> O# -(x, y)) (Log# x -> -#(Log' x, I 0()), -#(O x, O 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, O y) -> -#(x, y)) (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#(0(), O x) -> ge#(0(), x)) (Log'# O x -> ge#(x, I 0()), ge#(O x, O y) -> ge#(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, O y) -> ge#(x, y)) (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, O y) -> O# -(x, y)) (-#(O x, I y) -> -#(-(x, y), I 1()), -#(O x, O y) -> -#(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, O y) -> -#(x, y)) (-#(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)) (BS# N(x, l(), r()) -> ge#(Min r(), x), ge#(0(), O x) -> ge#(0(), x)) (BS# N(x, l(), r()) -> ge#(Min r(), x), ge#(O x, O y) -> ge#(x, y)) (BS# N(x, l(), r()) -> ge#(Min r(), x), ge#(O x, I y) -> not# ge(y, x)) (BS# N(x, l(), r()) -> ge#(Min r(), x), ge#(O x, I y) -> ge#(y, x)) (BS# N(x, l(), r()) -> ge#(Min r(), x), ge#(I x, O y) -> ge#(x, y)) (BS# N(x, l(), r()) -> ge#(Min r(), x), ge#(I x, I y) -> ge#(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())) (WB# N(x, l(), r()) -> ge#(I 0(), -(Size r(), Size l())), ge#(0(), O x) -> ge#(0(), x)) (WB# N(x, l(), r()) -> ge#(I 0(), -(Size r(), Size l())), ge#(O x, O y) -> ge#(x, y)) (WB# N(x, l(), r()) -> ge#(I 0(), -(Size r(), Size l())), ge#(O x, I y) -> not# ge(y, x)) (WB# N(x, l(), r()) -> ge#(I 0(), -(Size r(), Size l())), ge#(O x, I y) -> ge#(y, x)) (WB# N(x, l(), r()) -> ge#(I 0(), -(Size r(), Size l())), ge#(I x, O y) -> ge#(x, y)) (WB# N(x, l(), r()) -> ge#(I 0(), -(Size r(), Size l())), ge#(I x, I y) -> ge#(x, y)) (ge#(0(), O x) -> ge#(0(), x), ge#(0(), O x) -> ge#(0(), x)) (ge#(0(), O x) -> ge#(0(), x), ge#(O x, O y) -> ge#(x, y)) (ge#(0(), O x) -> ge#(0(), x), ge#(O x, I y) -> not# ge(y, x)) (ge#(0(), O x) -> ge#(0(), x), ge#(O x, I y) -> ge#(y, x)) (ge#(0(), O x) -> ge#(0(), x), ge#(I x, O y) -> ge#(x, y)) (ge#(0(), O x) -> ge#(0(), x), ge#(I x, I y) -> ge#(x, y)) (+#(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())) (WB# N(x, l(), r()) -> WB# r(), WB# N(x, l(), r()) -> -#(Size l(), Size r())) (WB# N(x, l(), r()) -> WB# r(), WB# N(x, l(), r()) -> -#(Size r(), Size l())) (WB# N(x, l(), r()) -> WB# r(), 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()) -> WB# r(), WB# N(x, l(), r()) -> and#(WB l(), WB r())) (WB# N(x, l(), r()) -> 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()) -> WB# r(), WB# N(x, l(), r()) -> ge#(I 0(), -(Size l(), Size r()))) (WB# N(x, l(), r()) -> WB# r(), WB# N(x, l(), r()) -> ge#(I 0(), -(Size r(), Size l()))) (WB# N(x, l(), r()) -> WB# r(), WB# N(x, l(), r()) -> ge#(Size l(), Size r())) (WB# N(x, l(), r()) -> WB# r(), WB# N(x, l(), r()) -> Size# l()) (WB# N(x, l(), r()) -> WB# r(), WB# N(x, l(), r()) -> Size# r()) (WB# N(x, l(), r()) -> WB# r(), WB# N(x, l(), r()) -> WB# l()) (WB# N(x, l(), r()) -> WB# r(), WB# N(x, l(), r()) -> WB# r()) (WB# N(x, l(), r()) -> Size# r(), Size# N(x, l(), r()) -> +#(+(Size l(), Size r()), I 1())) (WB# N(x, l(), r()) -> Size# r(), Size# N(x, l(), r()) -> +#(Size l(), Size r())) (WB# N(x, l(), r()) -> Size# r(), Size# N(x, l(), r()) -> Size# l()) (WB# N(x, l(), r()) -> Size# r(), Size# N(x, l(), r()) -> Size# r()) (Size# N(x, l(), r()) -> Size# r(), Size# N(x, l(), r()) -> +#(+(Size l(), Size r()), I 1())) (Size# N(x, l(), r()) -> Size# r(), Size# N(x, l(), r()) -> +#(Size l(), Size r())) (Size# N(x, l(), r()) -> Size# r(), Size# N(x, l(), r()) -> Size# l()) (Size# N(x, l(), r()) -> Size# r(), Size# N(x, l(), r()) -> Size# r()) (BS# N(x, l(), r()) -> BS# 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()) -> BS# r(), BS# N(x, l(), r()) -> and#(ge(x, Max l()), ge(Min r(), x))) (BS# N(x, l(), r()) -> BS# r(), BS# N(x, l(), r()) -> and#(BS l(), BS r())) (BS# N(x, l(), r()) -> BS# r(), BS# N(x, l(), r()) -> ge#(x, Max l())) (BS# N(x, l(), r()) -> BS# r(), BS# N(x, l(), r()) -> ge#(Min r(), x)) (BS# N(x, l(), r()) -> BS# r(), BS# N(x, l(), r()) -> Min# r()) (BS# N(x, l(), r()) -> BS# r(), BS# N(x, l(), r()) -> Max# l()) (BS# N(x, l(), r()) -> BS# r(), BS# N(x, l(), r()) -> BS# l()) (BS# N(x, l(), r()) -> BS# r(), BS# N(x, l(), r()) -> BS# r()) (BS# N(x, l(), r()) -> Max# l(), Max# N(x, l(), r()) -> Max# r()) (Max# N(x, l(), r()) -> Max# r(), Max# N(x, l(), r()) -> Max# r()) (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)) } 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))} 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))} 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))} STATUS: arrows: 0.954448 SCCS (5): 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: {Log'# O x -> Log'# x, Log'# I x -> Log'# x} 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: {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 (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: 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())) 0 + 0x >= 4 WB L x -> true() 0 + 0x >= 1 Size N(x, l(), r()) -> +(+(Size l(), Size r()), I 1()) 0 + 0x >= 3 Size L x -> I 0() 0 + 0x >= 2 BS N(x, l(), r()) -> and(and(ge(x, Max l()), ge(Min r(), x)), and(BS l(), BS r())) 0 + 0x >= 7 + 1x BS L x -> true() 0 + 0x >= 1 Max N(x, l(), r()) -> Max r() 2 + 0x >= 2 Max L x -> x 2 + 0x >= 1x Min N(x, l(), r()) -> Min l() 2 + 0x >= 2 Min L x -> x 2 + 0x >= 1x Val N(x, l(), r()) -> x 2 + 0x >= 1x Val L x -> x 2 + 0x >= 1x Log x -> -(Log' x, I 0()) 0 + 0x >= 1 + 1x Log' I x -> +(Log' x, I 0()) 2 + 1x >= 4 + 1x Log' O x -> if(ge(x, I 0()), +(Log' x, I 0()), 0()) 2 + 1x >= 4 + 0x Log' 0() -> 0() 2 >= 1 ge(I x, I y) -> ge(x, y) 2 + 0x + 1y >= 1 + 0x + 1y ge(I x, O y) -> ge(x, y) 2 + 0x + 1y >= 1 + 0x + 1y ge(O x, I y) -> not ge(y, x) 2 + 0x + 1y >= 2 + 1x + 0y ge(O x, O y) -> ge(x, y) 2 + 0x + 1y >= 1 + 0x + 1y ge(0(), I x) -> false() 2 + 1x >= 1 ge(0(), O x) -> ge(0(), x) 2 + 1x >= 1 + 1x ge(x, 0()) -> true() 2 + 0x >= 1 if(true(), x, y) -> x 2 + 0x + 0y >= 1x if(false(), x, y) -> y 2 + 0x + 0y >= 1y and(x, true()) -> x 2 + 1x >= 1x and(x, false()) -> false() 2 + 1x >= 1 not true() -> false() 2 >= 1 not false() -> true() 2 >= 1 -(I x, I y) -> O -(x, y) 1 + 1x + 0y >= 1 + 1x + 0y -(I x, O y) -> I -(x, y) 1 + 1x + 0y >= 1 + 1x + 0y -(O x, I y) -> I -(-(x, y), I 1()) 1 + 1x + 0y >= 1 + 1x + 0y -(O x, O y) -> O -(x, y) 1 + 1x + 0y >= 1 + 1x + 0y -(0(), x) -> 0() 1 + 0x >= 1 -(x, 0()) -> x 0 + 1x >= 1x +(I x, I y) -> O +(+(x, y), I 0()) 3 + 1x + 1y >= 5 + 1x + 1y +(I x, O y) -> I +(x, y) 3 + 1x + 1y >= 2 + 1x + 1y +(O x, I y) -> I +(x, y) 3 + 1x + 1y >= 2 + 1x + 1y +(O x, O y) -> O +(x, y) 3 + 1x + 1y >= 2 + 1x + 1y +(0(), x) -> x 2 + 1x >= 1x +(x, +(y, z)) -> +(+(x, y), z) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +(x, 0()) -> x 2 + 1x >= 1x O 0() -> 0() 2 >= 1 Qed 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()))} 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) = 0, [-](x0, x1) = 0, [and](x0, x1) = 0, [ge](x0, x1) = x0, [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, [Max](x0) = x0, [BS](x0) = x0 + 1, [Size](x0) = 0, [WB](x0) = 0, [0] = 0, [1] = 1, [false] = 1, [true] = 1, [l] = 1, [r] = 1, [Log'#](x0) = x0 Strict: Log'# I x -> Log'# x 0 + 1x >= 0 + 1x Log'# O x -> Log'# x 1 + 1x >= 0 + 1x Weak: 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())) 0 + 0x >= 0 WB L x -> true() 0 + 0x >= 1 Size N(x, l(), r()) -> +(+(Size l(), Size r()), I 1()) 0 + 0x >= 0 Size L x -> I 0() 0 + 0x >= 0 BS N(x, l(), r()) -> and(and(ge(x, Max l()), ge(Min r(), x)), and(BS l(), BS r())) 2 + 0x >= 0 + 0x BS L x -> true() 2 + 0x >= 1 Max N(x, l(), r()) -> Max r() 1 + 0x >= 1 Max L x -> x 1 + 0x >= 1x Min N(x, l(), r()) -> Min l() 1 + 0x >= 1 Min L x -> x 1 + 0x >= 1x Val N(x, l(), r()) -> x 2 + 0x >= 1x Val L x -> x 2 + 0x >= 1x Log x -> -(Log' x, I 0()) 0 + 0x >= 0 + 0x Log' I x -> +(Log' x, I 0()) 0 + 0x >= 0 + 0x Log' O x -> if(ge(x, I 0()), +(Log' x, I 0()), 0()) 0 + 0x >= 0 + 0x Log' 0() -> 0() 0 >= 0 ge(I x, I y) -> ge(x, y) 0 + 1x + 0y >= 0 + 1x + 0y ge(I x, O y) -> ge(x, y) 0 + 1x + 0y >= 0 + 1x + 0y ge(O x, I y) -> not ge(y, x) 1 + 1x + 0y >= 1 + 0x + 1y ge(O x, O y) -> ge(x, y) 1 + 1x + 0y >= 0 + 1x + 0y ge(0(), I x) -> false() 0 + 0x >= 1 ge(0(), O x) -> ge(0(), x) 0 + 0x >= 0 + 0x ge(x, 0()) -> true() 0 + 1x >= 1 if(true(), x, y) -> x 0 + 0x + 0y >= 1x if(false(), x, y) -> y 0 + 0x + 0y >= 1y and(x, true()) -> x 0 + 0x >= 1x and(x, false()) -> false() 0 + 0x >= 1 not true() -> false() 2 >= 1 not false() -> true() 2 >= 1 -(I x, I y) -> O -(x, y) 0 + 0x + 0y >= 1 + 0x + 0y -(I x, O y) -> I -(x, y) 0 + 0x + 0y >= 0 + 0x + 0y -(O x, I y) -> I -(-(x, y), I 1()) 0 + 0x + 0y >= 0 + 0x + 0y -(O x, O y) -> O -(x, y) 0 + 0x + 0y >= 1 + 0x + 0y -(0(), x) -> 0() 0 + 0x >= 0 -(x, 0()) -> x 0 + 0x >= 1x +(I x, I y) -> O +(+(x, y), I 0()) 0 + 0x + 0y >= 1 + 0x + 0y +(I x, O y) -> I +(x, y) 0 + 0x + 0y >= 0 + 0x + 0y +(O x, I y) -> I +(x, y) 0 + 0x + 0y >= 0 + 0x + 0y +(O x, O y) -> O +(x, y) 0 + 0x + 0y >= 1 + 0x + 0y +(0(), x) -> x 0 + 0x >= 1x +(x, +(y, z)) -> +(+(x, y), z) 0 + 0x + 0y + 0z >= 0 + 0x + 0y + 0z +(x, 0()) -> x 0 + 0x >= 1x O 0() -> 0() 1 >= 0 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()))} 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 + x1 + 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) = x0 + 1, [Size](x0) = x0 + 1, [WB](x0) = x0 + 1, [0] = 1, [1] = 1, [false] = 1, [true] = 1, [l] = 1, [r] = 1, [Log'#](x0) = x0 Strict: Log'# I x -> Log'# x 1 + 1x >= 0 + 1x Weak: 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())) 2 + 0x >= 7 WB L x -> true() 2 + 0x >= 1 Size N(x, l(), r()) -> +(+(Size l(), Size r()), I 1()) 2 + 0x >= 8 Size L x -> I 0() 2 + 0x >= 2 BS N(x, l(), r()) -> and(and(ge(x, Max l()), ge(Min r(), x)), and(BS l(), BS r())) 2 + 0x >= 7 + 0x BS L x -> true() 2 + 0x >= 1 Max N(x, l(), r()) -> Max r() 2 + 0x >= 2 Max L x -> x 2 + 0x >= 1x Min N(x, l(), r()) -> Min l() 2 + 0x >= 2 Min L x -> x 2 + 0x >= 1x Val N(x, l(), r()) -> x 2 + 0x >= 1x Val L x -> x 2 + 0x >= 1x Log x -> -(Log' x, I 0()) 0 + 0x >= 4 + 1x Log' I x -> +(Log' x, I 0()) 2 + 1x >= 4 + 1x Log' O x -> if(ge(x, I 0()), +(Log' x, I 0()), 0()) 2 + 1x >= 1 + 0x Log' 0() -> 0() 2 >= 1 ge(I x, I y) -> ge(x, y) 0 + 0x + 0y >= 0 + 0x + 0y ge(I x, O y) -> ge(x, y) 0 + 0x + 0y >= 0 + 0x + 0y ge(O x, I y) -> not ge(y, x) 0 + 0x + 0y >= 1 + 0x + 0y ge(O x, O y) -> ge(x, y) 0 + 0x + 0y >= 0 + 0x + 0y ge(0(), I x) -> false() 0 + 0x >= 1 ge(0(), O x) -> ge(0(), x) 0 + 0x >= 0 + 0x ge(x, 0()) -> true() 0 + 0x >= 1 if(true(), x, y) -> x 2 + 0x + 0y >= 1x if(false(), x, y) -> y 2 + 0x + 0y >= 1y and(x, true()) -> x 2 + 1x >= 1x and(x, false()) -> false() 2 + 1x >= 1 not true() -> false() 2 >= 1 not false() -> true() 2 >= 1 -(I x, I y) -> O -(x, y) 3 + 1x + 1y >= 2 + 1x + 1y -(I x, O y) -> I -(x, y) 3 + 1x + 1y >= 2 + 1x + 1y -(O x, I y) -> I -(-(x, y), I 1()) 3 + 1x + 1y >= 5 + 1x + 1y -(O x, O y) -> O -(x, y) 3 + 1x + 1y >= 2 + 1x + 1y -(0(), x) -> 0() 2 + 1x >= 1 -(x, 0()) -> x 2 + 1x >= 1x +(I x, I y) -> O +(+(x, y), I 0()) 3 + 1x + 1y >= 5 + 1x + 1y +(I x, O y) -> I +(x, y) 3 + 1x + 1y >= 2 + 1x + 1y +(O x, I y) -> I +(x, y) 3 + 1x + 1y >= 2 + 1x + 1y +(O x, O y) -> O +(x, y) 3 + 1x + 1y >= 2 + 1x + 1y +(0(), x) -> x 2 + 1x >= 1x +(x, +(y, z)) -> +(+(x, y), z) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +(x, 0()) -> x 2 + 1x >= 1x O 0() -> 0() 2 >= 1 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: 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())) 2 + 0x >= 4 WB L x -> true() 2 + 0x >= 1 Size N(x, l(), r()) -> +(+(Size l(), Size r()), I 1()) 2 + 0x >= 4 Size L x -> I 0() 2 + 0x >= 0 BS N(x, l(), r()) -> and(and(ge(x, Max l()), ge(Min r(), x)), and(BS l(), BS r())) 2 + 0x >= 4 + 0x BS L x -> true() 2 + 0x >= 1 Max N(x, l(), r()) -> Max r() 2 + 0x >= 2 Max L x -> x 2 + 0x >= 1x Min N(x, l(), r()) -> Min l() 2 + 0x >= 2 Min L x -> x 2 + 0x >= 1x Val N(x, l(), r()) -> x 2 + 0x >= 1x Val L x -> x 2 + 0x >= 1x Log x -> -(Log' x, I 0()) 0 + 0x >= 0 + 0x Log' I x -> +(Log' x, I 0()) 0 + 0x >= 0 + 0x Log' O x -> if(ge(x, I 0()), +(Log' x, I 0()), 0()) 0 + 0x >= 0 + 0x Log' 0() -> 0() 0 >= 0 ge(I x, I y) -> ge(x, y) 0 + 0x + 0y >= 0 + 0x + 0y ge(I x, O y) -> ge(x, y) 0 + 0x + 0y >= 0 + 0x + 0y ge(O x, I y) -> not ge(y, x) 0 + 0x + 0y >= 1 + 0x + 0y ge(O x, O y) -> ge(x, y) 0 + 0x + 0y >= 0 + 0x + 0y ge(0(), I x) -> false() 0 + 0x >= 1 ge(0(), O x) -> ge(0(), x) 0 + 0x >= 0 + 0x ge(x, 0()) -> true() 0 + 0x >= 1 if(true(), x, y) -> x 0 + 0x + 0y >= 1x if(false(), x, y) -> y 0 + 0x + 0y >= 1y and(x, true()) -> x 2 + 0x >= 1x and(x, false()) -> false() 2 + 0x >= 1 not true() -> false() 2 >= 1 not false() -> true() 2 >= 1 -(I x, I y) -> O -(x, y) 0 + 0x + 0y >= 1 + 0x + 0y -(I x, O y) -> I -(x, y) 0 + 0x + 0y >= 0 + 0x + 0y -(O x, I y) -> I -(-(x, y), I 1()) 0 + 0x + 0y >= 0 + 0x + 0y -(O x, O y) -> O -(x, y) 0 + 0x + 0y >= 1 + 0x + 0y -(0(), x) -> 0() 0 + 0x >= 0 -(x, 0()) -> x 0 + 0x >= 1x +(I x, I y) -> O +(+(x, y), I 0()) 0 + 1x + 1y >= 1 + 1x + 1y +(I x, O y) -> I +(x, y) 1 + 1x + 1y >= 0 + 1x + 1y +(O x, I y) -> I +(x, y) 1 + 1x + 1y >= 0 + 1x + 1y +(O x, O y) -> O +(x, y) 2 + 1x + 1y >= 1 + 1x + 1y +(0(), x) -> x 0 + 1x >= 1x +(x, +(y, z)) -> +(+(x, y), z) 0 + 1x + 1y + 1z >= 0 + 1x + 1y + 1z +(x, 0()) -> x 0 + 1x >= 1x O 0() -> 0() 1 >= 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: 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())) 2 + 0x >= 4 WB L x -> true() 2 + 0x >= 1 Size N(x, l(), r()) -> +(+(Size l(), Size r()), I 1()) 2 + 0x >= 6 Size L x -> I 0() 2 + 0x >= 0 BS N(x, l(), r()) -> and(and(ge(x, Max l()), ge(Min r(), x)), and(BS l(), BS r())) 0 + 0x >= 2 + 0x BS L x -> true() 0 + 0x >= 1 Max N(x, l(), r()) -> Max r() 2 + 0x >= 2 Max L x -> x 2 + 0x >= 1x Min N(x, l(), r()) -> Min l() 2 + 0x >= 2 Min L x -> x 2 + 0x >= 1x Val N(x, l(), r()) -> x 2 + 0x >= 1x Val L x -> x 2 + 0x >= 1x Log x -> -(Log' x, I 0()) 0 + 0x >= 0 + 0x Log' I x -> +(Log' x, I 0()) 0 + 0x >= 1 + 0x Log' O x -> if(ge(x, I 0()), +(Log' x, I 0()), 0()) 0 + 0x >= 2 + 0x Log' 0() -> 0() 0 >= 0 ge(I x, I y) -> ge(x, y) 0 + 0x + 0y >= 0 + 0x + 0y ge(I x, O y) -> ge(x, y) 0 + 0x + 0y >= 0 + 0x + 0y ge(O x, I y) -> not ge(y, x) 0 + 0x + 0y >= 1 + 0x + 0y ge(O x, O y) -> ge(x, y) 0 + 0x + 0y >= 0 + 0x + 0y ge(0(), I x) -> false() 0 + 0x >= 1 ge(0(), O x) -> ge(0(), x) 0 + 0x >= 0 + 0x ge(x, 0()) -> true() 0 + 0x >= 1 if(true(), x, y) -> x 2 + 1x + 0y >= 1x if(false(), x, y) -> y 2 + 1x + 0y >= 1y and(x, true()) -> x 2 + 0x >= 1x and(x, false()) -> false() 2 + 0x >= 1 not true() -> false() 2 >= 1 not false() -> true() 2 >= 1 -(I x, I y) -> O -(x, y) 0 + 0x + 0y >= 0 + 0x + 0y -(I x, O y) -> I -(x, y) 0 + 0x + 0y >= 0 + 0x + 0y -(O x, I y) -> I -(-(x, y), I 1()) 0 + 0x + 0y >= 0 + 0x + 0y -(O x, O y) -> O -(x, y) 0 + 0x + 0y >= 0 + 0x + 0y -(0(), x) -> 0() 0 + 0x >= 0 -(x, 0()) -> x 0 + 0x >= 1x +(I x, I y) -> O +(+(x, y), I 0()) 1 + 1x + 1y >= 0 + 0x + 0y +(I x, O y) -> I +(x, y) 1 + 1x + 0y >= 1 + 1x + 1y +(O x, I y) -> I +(x, y) 1 + 0x + 1y >= 1 + 1x + 1y +(O x, O y) -> O +(x, y) 1 + 0x + 0y >= 0 + 0x + 0y +(0(), x) -> x 1 + 1x >= 1x +(x, +(y, z)) -> +(+(x, y), z) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +(x, 0()) -> x 1 + 1x >= 1x O 0() -> 0() 0 >= 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: 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())) 0 + 0x >= 2 WB L x -> true() 0 + 0x >= 1 Size N(x, l(), r()) -> +(+(Size l(), Size r()), I 1()) 0 + 0x >= 2 Size L x -> I 0() 0 + 0x >= 1 BS N(x, l(), r()) -> and(and(ge(x, Max l()), ge(Min r(), x)), and(BS l(), BS r())) 0 + 0x >= 2 + 0x BS L x -> true() 0 + 0x >= 1 Max N(x, l(), r()) -> Max r() 2 + 0x >= 2 Max L x -> x 2 + 0x >= 1x Min N(x, l(), r()) -> Min l() 2 + 0x >= 2 Min L x -> x 2 + 0x >= 1x Val N(x, l(), r()) -> x 2 + 0x >= 1x Val L x -> x 2 + 0x >= 1x Log x -> -(Log' x, I 0()) 0 + 0x >= 1 + 0x Log' I x -> +(Log' x, I 0()) 0 + 0x >= 1 + 0x Log' O x -> if(ge(x, I 0()), +(Log' x, I 0()), 0()) 0 + 0x >= 2 + 0x Log' 0() -> 0() 0 >= 0 ge(I x, I y) -> ge(x, y) 0 + 0x + 0y >= 0 + 0x + 0y ge(I x, O y) -> ge(x, y) 0 + 0x + 0y >= 0 + 0x + 0y ge(O x, I y) -> not ge(y, x) 0 + 0x + 0y >= 1 + 0x + 0y ge(O x, O y) -> ge(x, y) 0 + 0x + 0y >= 0 + 0x + 0y ge(0(), I x) -> false() 0 + 0x >= 1 ge(0(), O x) -> ge(0(), x) 0 + 0x >= 0 + 0x ge(x, 0()) -> true() 0 + 0x >= 1 if(true(), x, y) -> x 2 + 1x + 0y >= 1x if(false(), x, y) -> y 2 + 1x + 0y >= 1y and(x, true()) -> x 2 + 0x >= 1x and(x, false()) -> false() 2 + 0x >= 1 not true() -> false() 2 >= 1 not false() -> true() 2 >= 1 -(I x, I y) -> O -(x, y) 1 + 0x + 1y >= 0 + 0x + 1y -(I x, O y) -> I -(x, y) 0 + 0x + 1y >= 1 + 0x + 1y -(O x, I y) -> I -(-(x, y), I 1()) 1 + 0x + 1y >= 3 + 0x + 0y -(O x, O y) -> O -(x, y) 0 + 0x + 1y >= 0 + 0x + 1y -(0(), x) -> 0() 0 + 1x >= 0 -(x, 0()) -> x 0 + 0x >= 1x +(I x, I y) -> O +(+(x, y), I 0()) 2 + 1x + 1y >= 1 + 1x + 1y +(I x, O y) -> I +(x, y) 1 + 1x + 1y >= 1 + 1x + 1y +(O x, I y) -> I +(x, y) 1 + 1x + 1y >= 1 + 1x + 1y +(O x, O y) -> O +(x, y) 0 + 1x + 1y >= 0 + 1x + 1y +(0(), x) -> x 0 + 1x >= 1x +(x, +(y, z)) -> +(+(x, y), z) 0 + 1x + 1y + 1z >= 0 + 1x + 1y + 1z +(x, 0()) -> x 0 + 1x >= 1x O 0() -> 0() 0 >= 0 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: 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())) 0 + 0x >= 2 WB L x -> true() 0 + 0x >= 1 Size N(x, l(), r()) -> +(+(Size l(), Size r()), I 1()) 2 + 0x >= 8 Size L x -> I 0() 2 + 0x >= 2 BS N(x, l(), r()) -> and(and(ge(x, Max l()), ge(Min r(), x)), and(BS l(), BS r())) 0 + 0x >= 2 + 0x BS L x -> true() 0 + 0x >= 1 Max N(x, l(), r()) -> Max r() 2 + 0x >= 2 Max L x -> x 2 + 0x >= 1x Min N(x, l(), r()) -> Min l() 2 + 0x >= 2 Min L x -> x 2 + 0x >= 1x Val N(x, l(), r()) -> x 2 + 0x >= 1x Val L x -> x 2 + 0x >= 1x Log x -> -(Log' x, I 0()) 0 + 0x >= 4 + 1x Log' I x -> +(Log' x, I 0()) 2 + 1x >= 4 + 1x Log' O x -> if(ge(x, I 0()), +(Log' x, I 0()), 0()) 2 + 1x >= 1 + 0x Log' 0() -> 0() 2 >= 1 ge(I x, I y) -> ge(x, y) 0 + 0x + 0y >= 0 + 0x + 0y ge(I x, O y) -> ge(x, y) 0 + 0x + 0y >= 0 + 0x + 0y ge(O x, I y) -> not ge(y, x) 0 + 0x + 0y >= 1 + 0x + 0y ge(O x, O y) -> ge(x, y) 0 + 0x + 0y >= 0 + 0x + 0y ge(0(), I x) -> false() 0 + 0x >= 1 ge(0(), O x) -> ge(0(), x) 0 + 0x >= 0 + 0x ge(x, 0()) -> true() 0 + 0x >= 1 if(true(), x, y) -> x 2 + 0x + 0y >= 1x if(false(), x, y) -> y 2 + 0x + 0y >= 1y and(x, true()) -> x 2 + 0x >= 1x and(x, false()) -> false() 2 + 0x >= 1 not true() -> false() 2 >= 1 not false() -> true() 2 >= 1 -(I x, I y) -> O -(x, y) 3 + 1x + 1y >= 2 + 1x + 1y -(I x, O y) -> I -(x, y) 3 + 1x + 1y >= 2 + 1x + 1y -(O x, I y) -> I -(-(x, y), I 1()) 3 + 1x + 1y >= 5 + 1x + 1y -(O x, O y) -> O -(x, y) 3 + 1x + 1y >= 2 + 1x + 1y -(0(), x) -> 0() 2 + 1x >= 1 -(x, 0()) -> x 2 + 1x >= 1x +(I x, I y) -> O +(+(x, y), I 0()) 3 + 1x + 1y >= 5 + 1x + 1y +(I x, O y) -> I +(x, y) 3 + 1x + 1y >= 2 + 1x + 1y +(O x, I y) -> I +(x, y) 3 + 1x + 1y >= 2 + 1x + 1y +(O x, O y) -> O +(x, y) 3 + 1x + 1y >= 2 + 1x + 1y +(0(), x) -> x 2 + 1x >= 1x +(x, +(y, z)) -> +(+(x, y), z) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +(x, 0()) -> x 2 + 1x >= 1x O 0() -> 0() 2 >= 1 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()))} 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) = x0 + 1, [O](x0) = x0 + 1, [I](x0) = 0, [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) = x0 + 1, [Size](x0) = x0 + 1, [WB](x0) = x0 + 1, [0] = 1, [1] = 0, [false] = 1, [true] = 1, [l] = 1, [r] = 1, [ge#](x0, x1) = x0 + 1 Strict: ge#(0(), O x) -> ge#(0(), x) 2 + 1x >= 1 + 1x Weak: 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())) 2 + 0x >= 4 WB L x -> true() 2 + 0x >= 1 Size N(x, l(), r()) -> +(+(Size l(), Size r()), I 1()) 2 + 0x >= 6 Size L x -> I 0() 2 + 0x >= 0 BS N(x, l(), r()) -> and(and(ge(x, Max l()), ge(Min r(), x)), and(BS l(), BS r())) 2 + 0x >= 4 + 0x BS L x -> true() 2 + 0x >= 1 Max N(x, l(), r()) -> Max r() 2 + 0x >= 2 Max L x -> x 2 + 0x >= 1x Min N(x, l(), r()) -> Min l() 2 + 0x >= 2 Min L x -> x 2 + 0x >= 1x Val N(x, l(), r()) -> x 2 + 0x >= 1x Val L x -> x 2 + 0x >= 1x Log x -> -(Log' x, I 0()) 0 + 0x >= 2 + 1x Log' I x -> +(Log' x, I 0()) 1 + 0x >= 2 + 1x Log' O x -> if(ge(x, I 0()), +(Log' x, I 0()), 0()) 2 + 1x >= 2 + 0x Log' 0() -> 0() 2 >= 1 ge(I x, I y) -> ge(x, y) 1 + 0x + 0y >= 1 + 0x + 1y ge(I x, O y) -> ge(x, y) 2 + 0x + 1y >= 1 + 0x + 1y ge(O x, I y) -> not ge(y, x) 1 + 0x + 0y >= 2 + 1x + 0y ge(O x, O y) -> ge(x, y) 2 + 0x + 1y >= 1 + 0x + 1y ge(0(), I x) -> false() 1 + 0x >= 1 ge(0(), O x) -> ge(0(), x) 2 + 1x >= 1 + 1x ge(x, 0()) -> true() 2 + 0x >= 1 if(true(), x, y) -> x 2 + 0x + 0y >= 1x if(false(), x, y) -> y 2 + 0x + 0y >= 1y and(x, true()) -> x 2 + 0x >= 1x and(x, false()) -> false() 2 + 0x >= 1 not true() -> false() 2 >= 1 not false() -> true() 2 >= 1 -(I x, I y) -> O -(x, y) 1 + 0x + 0y >= 2 + 1x + 1y -(I x, O y) -> I -(x, y) 2 + 0x + 1y >= 0 + 0x + 0y -(O x, I y) -> I -(-(x, y), I 1()) 2 + 1x + 0y >= 0 + 0x + 0y -(O x, O y) -> O -(x, y) 3 + 1x + 1y >= 2 + 1x + 1y -(0(), x) -> 0() 2 + 1x >= 1 -(x, 0()) -> x 2 + 1x >= 1x +(I x, I y) -> O +(+(x, y), I 0()) 1 + 0x + 0y >= 3 + 1x + 1y +(I x, O y) -> I +(x, y) 2 + 0x + 1y >= 0 + 0x + 0y +(O x, I y) -> I +(x, y) 2 + 1x + 0y >= 0 + 0x + 0y +(O x, O y) -> O +(x, y) 3 + 1x + 1y >= 2 + 1x + 1y +(0(), x) -> x 2 + 1x >= 1x +(x, +(y, z)) -> +(+(x, y), z) 2 + 1x + 1y + 1z >= 2 + 1x + 1y + 1z +(x, 0()) -> x 2 + 1x >= 1x O 0() -> 0() 2 >= 1 Qed