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