YES 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: Strict: { +#(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())} 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())))} EDG: {(+#(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)) (ge#(O(x), I(y)) -> ge#(y, x), ge#(I(x), I(y)) -> ge#(x, y)) (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#(O(x), I(y)) -> ge#(y, x)) (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), O(y)) -> ge#(x, y)) (ge#(O(x), I(y)) -> ge#(y, x), ge#(0(), O(x)) -> ge#(0(), x)) (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()))) (ge#(0(), O(x)) -> ge#(0(), x), 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)) (+#(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#(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())))} SCCS: 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: 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: Scc: {Log'#(I(x)) -> Log'#(x)} SCC: 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: 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: Argument Filtering: pi(WB) = [], pi(Size) = [], pi(BS) = [], pi(Max) = [], pi(Min) = [], pi(r) = [], pi(l) = [], pi(N) = [], pi(L) = [], pi(Val) = [], pi(Log) = [], pi(Log') = [], pi(ge#) = [0,1], pi(ge) = [], pi(if) = [], pi(and) = [], pi(true) = [], pi(not) = [], pi(false) = [], pi(1) = [], pi(-) = [], pi(I) = 0, pi(+) = [], pi(O) = [0], pi(0) = [] Usable Rules: {} Interpretation: [ge#](x0, x1) = x0 + x1, [O](x0) = x0 + 1 Strict: {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())))} EDG: {(ge#(I(x), I(y)) -> ge#(x, y), ge#(I(x), I(y)) -> ge#(x, y))} SCCS: Scc: {ge#(I(x), I(y)) -> ge#(x, y)} SCC: Strict: {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())))} SPSC: Simple Projection: pi(ge#) = 0 Strict: {} Qed SCC: 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: 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: Argument Filtering: pi(WB) = [], pi(Size) = [], pi(BS) = [], pi(Max) = [], pi(Min) = [], pi(r) = [], pi(l) = [], pi(N) = [], pi(L) = [], pi(Val) = [], pi(Log) = [], pi(Log') = [], pi(ge) = [], pi(if) = [], pi(and) = [], pi(true) = [], pi(not) = [], pi(false) = [], pi(1) = [], pi(-#) = 1, pi(-) = [], pi(I) = [0], pi(+) = [], pi(O) = 0, pi(0) = [] Usable Rules: {} Interpretation: [I](x0) = x0 + 1, [1] = 0 Strict: {-#(O(x), O(y)) -> -#(x, y), -#(O(x), I(y)) -> -#(-(x, y), I(1())), -#(I(x), O(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())))} EDG: {(-#(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), O(y)) -> -#(x, y)) (-#(O(x), I(y)) -> -#(-(x, y), I(1())), -#(O(x), I(y)) -> -#(-(x, y), I(1()))) (-#(O(x), O(y)) -> -#(x, y), -#(O(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), -#(I(x), O(y)) -> -#(x, y))} SCCS: Scc: {-#(O(x), I(y)) -> -#(-(x, y), I(1()))} Scc: {-#(O(x), O(y)) -> -#(x, y), -#(I(x), O(y)) -> -#(x, y)} SCC: Strict: {-#(O(x), I(y)) -> -#(-(x, y), I(1()))} 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: Argument Filtering: pi(WB) = [], pi(Size) = [], pi(BS) = [], pi(Max) = [], pi(Min) = [], pi(r) = [], pi(l) = [], pi(N) = [], pi(L) = [], pi(Val) = [], pi(Log) = [], pi(Log') = [], pi(ge) = [], pi(if) = [], pi(and) = [], pi(true) = [], pi(not) = [], pi(false) = [], pi(1) = [], pi(-#) = [0], pi(-) = 0, pi(I) = [0], pi(+) = [], pi(O) = [0], pi(0) = [] Usable Rules: {} Interpretation: [-#](x0) = x0 + 1, [O](x0) = x0 + 1 Strict: {} 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())))} Qed SCC: Strict: {-#(O(x), O(y)) -> -#(x, y), -#(I(x), O(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())))} SPSC: Simple Projection: pi(-#) = 0 Strict: {-#(O(x), O(y)) -> -#(x, y)} EDG: {(-#(O(x), O(y)) -> -#(x, y), -#(O(x), O(y)) -> -#(x, y))} SCCS: Scc: {-#(O(x), O(y)) -> -#(x, y)} SCC: Strict: {-#(O(x), O(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())))} SPSC: Simple Projection: pi(-#) = 0 Strict: {} Qed SCC: 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: Argument Filtering: pi(WB) = [], pi(Size) = 0, pi(BS) = [], pi(Max) = [], pi(Min) = [], pi(r) = [], pi(l) = [], pi(N) = [], pi(L) = [], pi(Val) = [], pi(Log) = [], pi(Log') = [], pi(ge) = [], pi(if) = [], pi(and) = [], pi(true) = [], pi(not) = [], pi(false) = [], pi(1) = [], pi(-) = [], pi(I) = 0, pi(+#) = 1, pi(+) = [0,1], pi(O) = 0, pi(0) = [] Usable Rules: {} Interpretation: [+](x0, x1) = x0 + x1 + 1, [0] = 0 Strict: {+#(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())))} EDG: {(+#(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)) (+#(O(x), I(y)) -> +#(x, y), +#(I(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), O(y)) -> +#(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), +#(I(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), 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())), +#(I(x), I(y)) -> +#(x, y)) (+#(I(x), I(y)) -> +#(+(x, y), I(0())), +#(I(x), I(y)) -> +#(+(x, y), I(0()))) (+#(I(x), O(y)) -> +#(x, y), +#(O(x), O(y)) -> +#(x, y)) (+#(I(x), O(y)) -> +#(x, y), +#(O(x), I(y)) -> +#(x, y)) (+#(I(x), O(y)) -> +#(x, y), +#(I(x), O(y)) -> +#(x, y)) (+#(I(x), O(y)) -> +#(x, y), +#(I(x), I(y)) -> +#(x, y)) (+#(I(x), O(y)) -> +#(x, y), +#(I(x), I(y)) -> +#(+(x, y), I(0()))) (+#(O(x), O(y)) -> +#(x, y), +#(O(x), O(y)) -> +#(x, y)) (+#(O(x), O(y)) -> +#(x, y), +#(O(x), I(y)) -> +#(x, y)) (+#(O(x), O(y)) -> +#(x, y), +#(I(x), O(y)) -> +#(x, y)) (+#(O(x), O(y)) -> +#(x, y), +#(I(x), I(y)) -> +#(x, y)) (+#(O(x), O(y)) -> +#(x, y), +#(I(x), I(y)) -> +#(+(x, y), I(0())))} SCCS: Scc: {+#(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: Strict: {+#(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: Argument Filtering: pi(WB) = [], pi(Size) = [], pi(BS) = [], pi(Max) = [], pi(Min) = [], pi(r) = [], pi(l) = [], pi(N) = [], pi(L) = [], pi(Val) = [], pi(Log) = [], pi(Log') = [], pi(ge) = [], pi(if) = [], pi(and) = [], pi(true) = [], pi(not) = [], pi(false) = [], pi(1) = [], pi(-) = [], pi(I) = [0], pi(+#) = 1, pi(+) = [], pi(O) = 0, pi(0) = [] Usable Rules: {} Interpretation: [I](x0) = x0 + 1, [0] = 0 Strict: {+#(O(x), O(y)) -> +#(x, y), +#(I(x), O(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())))} EDG: {(+#(I(x), O(y)) -> +#(x, y), +#(I(x), I(y)) -> +#(+(x, y), I(0()))) (+#(I(x), O(y)) -> +#(x, y), +#(I(x), O(y)) -> +#(x, y)) (+#(I(x), O(y)) -> +#(x, y), +#(O(x), O(y)) -> +#(x, y)) (+#(I(x), I(y)) -> +#(+(x, y), I(0())), +#(I(x), I(y)) -> +#(+(x, y), I(0()))) (+#(O(x), O(y)) -> +#(x, y), +#(O(x), O(y)) -> +#(x, y)) (+#(O(x), O(y)) -> +#(x, y), +#(I(x), O(y)) -> +#(x, y)) (+#(O(x), O(y)) -> +#(x, y), +#(I(x), I(y)) -> +#(+(x, y), I(0())))} SCCS: Scc: {+#(I(x), I(y)) -> +#(+(x, y), I(0()))} Scc: {+#(O(x), O(y)) -> +#(x, y), +#(I(x), O(y)) -> +#(x, y)} SCC: Strict: {+#(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: Argument Filtering: pi(WB) = [], pi(Size) = [], pi(BS) = [], pi(Max) = [], pi(Min) = [], pi(r) = [], pi(l) = [], pi(N) = [], pi(L) = [], pi(Val) = [], pi(Log) = [], pi(Log') = [], pi(ge) = [], pi(if) = [], pi(and) = [], pi(true) = [], pi(not) = [], pi(false) = [], pi(1) = [], pi(-) = [], pi(I) = [0], pi(+#) = [0,1], pi(+) = [0,1], pi(O) = 0, pi(0) = [] Usable Rules: {} Interpretation: [+#](x0, x1) = x0 + x1 + 1, [+](x0, x1) = x0 + x1, [I](x0) = x0 + 1, [0] = 0 Strict: {} 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())))} Qed SCC: Strict: {+#(O(x), O(y)) -> +#(x, y), +#(I(x), O(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())))} SPSC: Simple Projection: pi(+#) = 0 Strict: {+#(O(x), O(y)) -> +#(x, y)} EDG: {(+#(O(x), O(y)) -> +#(x, y), +#(O(x), O(y)) -> +#(x, y))} SCCS: Scc: {+#(O(x), O(y)) -> +#(x, y)} SCC: Strict: {+#(O(x), O(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())))} SPSC: Simple Projection: pi(+#) = 0 Strict: {} Qed