YES Problem: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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()))) Proof: DP Processor: DPs: +#(O(x),O(y)) -> +#(x,y) +#(O(x),O(y)) -> O#(+(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())) +#(I(x),I(y)) -> O#(+(+(x,y),I(0()))) +#(x,+(y,z)) -> +#(x,y) +#(x,+(y,z)) -> +#(+(x,y),z) -#(O(x),O(y)) -> -#(x,y) -#(O(x),O(y)) -> O#(-(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) -#(I(x),I(y)) -> O#(-(x,y)) ge#(O(x),O(y)) -> ge#(x,y) ge#(O(x),I(y)) -> ge#(y,x) ge#(O(x),I(y)) -> not#(ge(y,x)) ge#(I(x),O(y)) -> ge#(x,y) ge#(I(x),I(y)) -> ge#(x,y) ge#(0(),O(x)) -> ge#(0(),x) Log'#(I(x)) -> Log'#(x) Log'#(I(x)) -> +#(Log'(x),I(0())) Log'#(O(x)) -> Log'#(x) Log'#(O(x)) -> +#(Log'(x),I(0())) Log'#(O(x)) -> ge#(x,I(0())) Log'#(O(x)) -> if#(ge(x,I(0())),+(Log'(x),I(0())),0()) Log#(x) -> Log'#(x) Log#(x) -> -#(Log'(x),I(0())) Min#(N(x,l(),r())) -> Min#(l()) Max#(N(x,l(),r())) -> Max#(r()) BS#(N(x,l(),r())) -> BS#(r()) BS#(N(x,l(),r())) -> BS#(l()) BS#(N(x,l(),r())) -> and#(BS(l()),BS(r())) BS#(N(x,l(),r())) -> Min#(r()) BS#(N(x,l(),r())) -> ge#(Min(r()),x) BS#(N(x,l(),r())) -> Max#(l()) BS#(N(x,l(),r())) -> ge#(x,Max(l())) BS#(N(x,l(),r())) -> and#(ge(x,Max(l())),ge(Min(r()),x)) BS#(N(x,l(),r())) -> and#(and(ge(x,Max(l())),ge(Min(r()),x)),and(BS(l()),BS(r()))) Size#(N(x,l(),r())) -> Size#(r()) Size#(N(x,l(),r())) -> Size#(l()) Size#(N(x,l(),r())) -> +#(Size(l()),Size(r())) Size#(N(x,l(),r())) -> +#(+(Size(l()),Size(r())),I(1())) WB#(N(x,l(),r())) -> WB#(r()) WB#(N(x,l(),r())) -> WB#(l()) WB#(N(x,l(),r())) -> and#(WB(l()),WB(r())) WB#(N(x,l(),r())) -> -#(Size(r()),Size(l())) WB#(N(x,l(),r())) -> ge#(I(0()),-(Size(r()),Size(l()))) WB#(N(x,l(),r())) -> -#(Size(l()),Size(r())) WB#(N(x,l(),r())) -> ge#(I(0()),-(Size(l()),Size(r()))) WB#(N(x,l(),r())) -> Size#(r()) WB#(N(x,l(),r())) -> Size#(l()) WB#(N(x,l(),r())) -> ge#(Size(l()),Size(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())) -> 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()))) TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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()))) TDG Processor: DPs: +#(O(x),O(y)) -> +#(x,y) +#(O(x),O(y)) -> O#(+(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())) +#(I(x),I(y)) -> O#(+(+(x,y),I(0()))) +#(x,+(y,z)) -> +#(x,y) +#(x,+(y,z)) -> +#(+(x,y),z) -#(O(x),O(y)) -> -#(x,y) -#(O(x),O(y)) -> O#(-(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) -#(I(x),I(y)) -> O#(-(x,y)) ge#(O(x),O(y)) -> ge#(x,y) ge#(O(x),I(y)) -> ge#(y,x) ge#(O(x),I(y)) -> not#(ge(y,x)) ge#(I(x),O(y)) -> ge#(x,y) ge#(I(x),I(y)) -> ge#(x,y) ge#(0(),O(x)) -> ge#(0(),x) Log'#(I(x)) -> Log'#(x) Log'#(I(x)) -> +#(Log'(x),I(0())) Log'#(O(x)) -> Log'#(x) Log'#(O(x)) -> +#(Log'(x),I(0())) Log'#(O(x)) -> ge#(x,I(0())) Log'#(O(x)) -> if#(ge(x,I(0())),+(Log'(x),I(0())),0()) Log#(x) -> Log'#(x) Log#(x) -> -#(Log'(x),I(0())) Min#(N(x,l(),r())) -> Min#(l()) Max#(N(x,l(),r())) -> Max#(r()) BS#(N(x,l(),r())) -> BS#(r()) BS#(N(x,l(),r())) -> BS#(l()) BS#(N(x,l(),r())) -> and#(BS(l()),BS(r())) BS#(N(x,l(),r())) -> Min#(r()) BS#(N(x,l(),r())) -> ge#(Min(r()),x) BS#(N(x,l(),r())) -> Max#(l()) BS#(N(x,l(),r())) -> ge#(x,Max(l())) BS#(N(x,l(),r())) -> and#(ge(x,Max(l())),ge(Min(r()),x)) BS#(N(x,l(),r())) -> and#(and(ge(x,Max(l())),ge(Min(r()),x)),and(BS(l()),BS(r()))) Size#(N(x,l(),r())) -> Size#(r()) Size#(N(x,l(),r())) -> Size#(l()) Size#(N(x,l(),r())) -> +#(Size(l()),Size(r())) Size#(N(x,l(),r())) -> +#(+(Size(l()),Size(r())),I(1())) WB#(N(x,l(),r())) -> WB#(r()) WB#(N(x,l(),r())) -> WB#(l()) WB#(N(x,l(),r())) -> and#(WB(l()),WB(r())) WB#(N(x,l(),r())) -> -#(Size(r()),Size(l())) WB#(N(x,l(),r())) -> ge#(I(0()),-(Size(r()),Size(l()))) WB#(N(x,l(),r())) -> -#(Size(l()),Size(r())) WB#(N(x,l(),r())) -> ge#(I(0()),-(Size(l()),Size(r()))) WB#(N(x,l(),r())) -> Size#(r()) WB#(N(x,l(),r())) -> Size#(l()) WB#(N(x,l(),r())) -> ge#(Size(l()),Size(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())) -> 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()))) TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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()))) graph: WB#(N(x,l(),r())) -> WB#(r()) -> WB#(N(x,l(),r())) -> and#(if(ge(Size(l()),Size(r())),ge(I(0()),-(Size(l()),Size(r()))), ge(I(0()),-(Size(r()),Size(l())))),and(WB(l()),WB(r()))) WB#(N(x,l(),r())) -> WB#(r()) -> WB#(N(x,l(),r())) -> if#(ge(Size(l()),Size(r())),ge(I(0()),-(Size(l()),Size(r()))),ge(I(0()),-(Size(r()),Size(l())))) WB#(N(x,l(),r())) -> WB#(r()) -> WB#(N(x,l(),r())) -> ge#(Size(l()),Size(r())) WB#(N(x,l(),r())) -> WB#(r()) -> WB#(N(x,l(),r())) -> Size#(l()) WB#(N(x,l(),r())) -> WB#(r()) -> WB#(N(x,l(),r())) -> Size#(r()) WB#(N(x,l(),r())) -> WB#(r()) -> WB#(N(x,l(),r())) -> ge#(I(0()),-(Size(l()),Size(r()))) WB#(N(x,l(),r())) -> WB#(r()) -> WB#(N(x,l(),r())) -> -#(Size(l()),Size(r())) WB#(N(x,l(),r())) -> WB#(r()) -> WB#(N(x,l(),r())) -> ge#(I(0()),-(Size(r()),Size(l()))) WB#(N(x,l(),r())) -> WB#(r()) -> WB#(N(x,l(),r())) -> -#(Size(r()),Size(l())) WB#(N(x,l(),r())) -> WB#(r()) -> WB#(N(x,l(),r())) -> and#(WB(l()),WB(r())) WB#(N(x,l(),r())) -> WB#(r()) -> WB#(N(x,l(),r())) -> WB#(l()) WB#(N(x,l(),r())) -> WB#(r()) -> WB#(N(x,l(),r())) -> WB#(r()) WB#(N(x,l(),r())) -> WB#(l()) -> WB#(N(x,l(),r())) -> and#(if(ge(Size(l()),Size(r())),ge(I(0()),-(Size(l()),Size(r()))), ge(I(0()),-(Size(r()),Size(l())))),and(WB(l()),WB(r()))) WB#(N(x,l(),r())) -> WB#(l()) -> WB#(N(x,l(),r())) -> if#(ge(Size(l()),Size(r())),ge(I(0()),-(Size(l()),Size(r()))),ge(I(0()),-(Size(r()),Size(l())))) WB#(N(x,l(),r())) -> WB#(l()) -> WB#(N(x,l(),r())) -> ge#(Size(l()),Size(r())) WB#(N(x,l(),r())) -> WB#(l()) -> WB#(N(x,l(),r())) -> Size#(l()) WB#(N(x,l(),r())) -> WB#(l()) -> WB#(N(x,l(),r())) -> Size#(r()) WB#(N(x,l(),r())) -> WB#(l()) -> WB#(N(x,l(),r())) -> ge#(I(0()),-(Size(l()),Size(r()))) WB#(N(x,l(),r())) -> WB#(l()) -> WB#(N(x,l(),r())) -> -#(Size(l()),Size(r())) WB#(N(x,l(),r())) -> WB#(l()) -> WB#(N(x,l(),r())) -> ge#(I(0()),-(Size(r()),Size(l()))) WB#(N(x,l(),r())) -> WB#(l()) -> WB#(N(x,l(),r())) -> -#(Size(r()),Size(l())) WB#(N(x,l(),r())) -> WB#(l()) -> WB#(N(x,l(),r())) -> and#(WB(l()),WB(r())) WB#(N(x,l(),r())) -> WB#(l()) -> WB#(N(x,l(),r())) -> WB#(l()) WB#(N(x,l(),r())) -> WB#(l()) -> WB#(N(x,l(),r())) -> WB#(r()) WB#(N(x,l(),r())) -> Size#(r()) -> Size#(N(x,l(),r())) -> +#(+(Size(l()),Size(r())),I(1())) WB#(N(x,l(),r())) -> Size#(r()) -> Size#(N(x,l(),r())) -> +#(Size(l()),Size(r())) WB#(N(x,l(),r())) -> Size#(r()) -> Size#(N(x,l(),r())) -> Size#(l()) WB#(N(x,l(),r())) -> Size#(r()) -> Size#(N(x,l(),r())) -> Size#(r()) WB#(N(x,l(),r())) -> Size#(l()) -> Size#(N(x,l(),r())) -> +#(+(Size(l()),Size(r())),I(1())) WB#(N(x,l(),r())) -> Size#(l()) -> Size#(N(x,l(),r())) -> +#(Size(l()),Size(r())) WB#(N(x,l(),r())) -> Size#(l()) -> Size#(N(x,l(),r())) -> Size#(l()) WB#(N(x,l(),r())) -> Size#(l()) -> Size#(N(x,l(),r())) -> Size#(r()) WB#(N(x,l(),r())) -> ge#(Size(l()),Size(r())) -> ge#(0(),O(x)) -> ge#(0(),x) WB#(N(x,l(),r())) -> ge#(Size(l()),Size(r())) -> ge#(I(x),I(y)) -> ge#(x,y) WB#(N(x,l(),r())) -> ge#(Size(l()),Size(r())) -> ge#(I(x),O(y)) -> ge#(x,y) WB#(N(x,l(),r())) -> ge#(Size(l()),Size(r())) -> ge#(O(x),I(y)) -> not#(ge(y,x)) WB#(N(x,l(),r())) -> ge#(Size(l()),Size(r())) -> ge#(O(x),I(y)) -> ge#(y,x) WB#(N(x,l(),r())) -> ge#(Size(l()),Size(r())) -> ge#(O(x),O(y)) -> ge#(x,y) WB#(N(x,l(),r())) -> ge#(I(0()),-(Size(r()),Size(l()))) -> ge#(0(),O(x)) -> ge#(0(),x) WB#(N(x,l(),r())) -> ge#(I(0()),-(Size(r()),Size(l()))) -> ge#(I(x),I(y)) -> ge#(x,y) WB#(N(x,l(),r())) -> ge#(I(0()),-(Size(r()),Size(l()))) -> ge#(I(x),O(y)) -> ge#(x,y) WB#(N(x,l(),r())) -> ge#(I(0()),-(Size(r()),Size(l()))) -> ge#(O(x),I(y)) -> not#(ge(y,x)) WB#(N(x,l(),r())) -> ge#(I(0()),-(Size(r()),Size(l()))) -> ge#(O(x),I(y)) -> ge#(y,x) WB#(N(x,l(),r())) -> ge#(I(0()),-(Size(r()),Size(l()))) -> ge#(O(x),O(y)) -> ge#(x,y) WB#(N(x,l(),r())) -> ge#(I(0()),-(Size(l()),Size(r()))) -> ge#(0(),O(x)) -> ge#(0(),x) WB#(N(x,l(),r())) -> ge#(I(0()),-(Size(l()),Size(r()))) -> ge#(I(x),I(y)) -> ge#(x,y) WB#(N(x,l(),r())) -> ge#(I(0()),-(Size(l()),Size(r()))) -> ge#(I(x),O(y)) -> ge#(x,y) WB#(N(x,l(),r())) -> ge#(I(0()),-(Size(l()),Size(r()))) -> ge#(O(x),I(y)) -> not#(ge(y,x)) WB#(N(x,l(),r())) -> ge#(I(0()),-(Size(l()),Size(r()))) -> ge#(O(x),I(y)) -> ge#(y,x) WB#(N(x,l(),r())) -> ge#(I(0()),-(Size(l()),Size(r()))) -> ge#(O(x),O(y)) -> ge#(x,y) WB#(N(x,l(),r())) -> -#(Size(r()),Size(l())) -> -#(I(x),I(y)) -> O#(-(x,y)) WB#(N(x,l(),r())) -> -#(Size(r()),Size(l())) -> -#(I(x),I(y)) -> -#(x,y) WB#(N(x,l(),r())) -> -#(Size(r()),Size(l())) -> -#(I(x),O(y)) -> -#(x,y) WB#(N(x,l(),r())) -> -#(Size(r()),Size(l())) -> -#(O(x),I(y)) -> -#(-(x,y),I(1())) WB#(N(x,l(),r())) -> -#(Size(r()),Size(l())) -> -#(O(x),I(y)) -> -#(x,y) WB#(N(x,l(),r())) -> -#(Size(r()),Size(l())) -> -#(O(x),O(y)) -> O#(-(x,y)) WB#(N(x,l(),r())) -> -#(Size(r()),Size(l())) -> -#(O(x),O(y)) -> -#(x,y) WB#(N(x,l(),r())) -> -#(Size(l()),Size(r())) -> -#(I(x),I(y)) -> O#(-(x,y)) WB#(N(x,l(),r())) -> -#(Size(l()),Size(r())) -> -#(I(x),I(y)) -> -#(x,y) WB#(N(x,l(),r())) -> -#(Size(l()),Size(r())) -> -#(I(x),O(y)) -> -#(x,y) WB#(N(x,l(),r())) -> -#(Size(l()),Size(r())) -> -#(O(x),I(y)) -> -#(-(x,y),I(1())) WB#(N(x,l(),r())) -> -#(Size(l()),Size(r())) -> -#(O(x),I(y)) -> -#(x,y) WB#(N(x,l(),r())) -> -#(Size(l()),Size(r())) -> -#(O(x),O(y)) -> O#(-(x,y)) WB#(N(x,l(),r())) -> -#(Size(l()),Size(r())) -> -#(O(x),O(y)) -> -#(x,y) Size#(N(x,l(),r())) -> Size#(r()) -> Size#(N(x,l(),r())) -> +#(+(Size(l()),Size(r())),I(1())) Size#(N(x,l(),r())) -> Size#(r()) -> Size#(N(x,l(),r())) -> +#(Size(l()),Size(r())) Size#(N(x,l(),r())) -> Size#(r()) -> Size#(N(x,l(),r())) -> Size#(l()) Size#(N(x,l(),r())) -> Size#(r()) -> Size#(N(x,l(),r())) -> Size#(r()) Size#(N(x,l(),r())) -> Size#(l()) -> Size#(N(x,l(),r())) -> +#(+(Size(l()),Size(r())),I(1())) Size#(N(x,l(),r())) -> Size#(l()) -> Size#(N(x,l(),r())) -> +#(Size(l()),Size(r())) Size#(N(x,l(),r())) -> Size#(l()) -> Size#(N(x,l(),r())) -> Size#(l()) Size#(N(x,l(),r())) -> Size#(l()) -> Size#(N(x,l(),r())) -> Size#(r()) Size#(N(x,l(),r())) -> +#(Size(l()),Size(r())) -> +#(x,+(y,z)) -> +#(+(x,y),z) Size#(N(x,l(),r())) -> +#(Size(l()),Size(r())) -> +#(x,+(y,z)) -> +#(x,y) Size#(N(x,l(),r())) -> +#(Size(l()),Size(r())) -> +#(I(x),I(y)) -> O#(+(+(x,y),I(0()))) Size#(N(x,l(),r())) -> +#(Size(l()),Size(r())) -> +#(I(x),I(y)) -> +#(+(x,y),I(0())) Size#(N(x,l(),r())) -> +#(Size(l()),Size(r())) -> +#(I(x),I(y)) -> +#(x,y) Size#(N(x,l(),r())) -> +#(Size(l()),Size(r())) -> +#(I(x),O(y)) -> +#(x,y) Size#(N(x,l(),r())) -> +#(Size(l()),Size(r())) -> +#(O(x),I(y)) -> +#(x,y) Size#(N(x,l(),r())) -> +#(Size(l()),Size(r())) -> +#(O(x),O(y)) -> O#(+(x,y)) Size#(N(x,l(),r())) -> +#(Size(l()),Size(r())) -> +#(O(x),O(y)) -> +#(x,y) Size#(N(x,l(),r())) -> +#(+(Size(l()),Size(r())),I(1())) -> +#(x,+(y,z)) -> +#(+(x,y),z) Size#(N(x,l(),r())) -> +#(+(Size(l()),Size(r())),I(1())) -> +#(x,+(y,z)) -> +#(x,y) Size#(N(x,l(),r())) -> +#(+(Size(l()),Size(r())),I(1())) -> +#(I(x),I(y)) -> O#(+(+(x,y),I(0()))) Size#(N(x,l(),r())) -> +#(+(Size(l()),Size(r())),I(1())) -> +#(I(x),I(y)) -> +#(+(x,y),I(0())) Size#(N(x,l(),r())) -> +#(+(Size(l()),Size(r())),I(1())) -> +#(I(x),I(y)) -> +#(x,y) Size#(N(x,l(),r())) -> +#(+(Size(l()),Size(r())),I(1())) -> +#(I(x),O(y)) -> +#(x,y) Size#(N(x,l(),r())) -> +#(+(Size(l()),Size(r())),I(1())) -> +#(O(x),I(y)) -> +#(x,y) Size#(N(x,l(),r())) -> +#(+(Size(l()),Size(r())),I(1())) -> +#(O(x),O(y)) -> O#(+(x,y)) Size#(N(x,l(),r())) -> +#(+(Size(l()),Size(r())),I(1())) -> +#(O(x),O(y)) -> +#(x,y) BS#(N(x,l(),r())) -> BS#(r()) -> BS#(N(x,l(),r())) -> and#(and(ge(x,Max(l())),ge(Min(r()),x)),and(BS(l()),BS(r()))) BS#(N(x,l(),r())) -> BS#(r()) -> BS#(N(x,l(),r())) -> and#(ge(x,Max(l())),ge(Min(r()),x)) BS#(N(x,l(),r())) -> BS#(r()) -> BS#(N(x,l(),r())) -> ge#(x,Max(l())) BS#(N(x,l(),r())) -> BS#(r()) -> BS#(N(x,l(),r())) -> Max#(l()) BS#(N(x,l(),r())) -> BS#(r()) -> BS#(N(x,l(),r())) -> ge#(Min(r()),x) BS#(N(x,l(),r())) -> BS#(r()) -> BS#(N(x,l(),r())) -> Min#(r()) BS#(N(x,l(),r())) -> BS#(r()) -> BS#(N(x,l(),r())) -> and#(BS(l()),BS(r())) BS#(N(x,l(),r())) -> BS#(r()) -> BS#(N(x,l(),r())) -> BS#(l()) BS#(N(x,l(),r())) -> BS#(r()) -> BS#(N(x,l(),r())) -> BS#(r()) BS#(N(x,l(),r())) -> BS#(l()) -> BS#(N(x,l(),r())) -> and#(and(ge(x,Max(l())),ge(Min(r()),x)),and(BS(l()),BS(r()))) BS#(N(x,l(),r())) -> BS#(l()) -> BS#(N(x,l(),r())) -> and#(ge(x,Max(l())),ge(Min(r()),x)) BS#(N(x,l(),r())) -> BS#(l()) -> BS#(N(x,l(),r())) -> ge#(x,Max(l())) BS#(N(x,l(),r())) -> BS#(l()) -> BS#(N(x,l(),r())) -> Max#(l()) BS#(N(x,l(),r())) -> BS#(l()) -> BS#(N(x,l(),r())) -> ge#(Min(r()),x) BS#(N(x,l(),r())) -> BS#(l()) -> BS#(N(x,l(),r())) -> Min#(r()) BS#(N(x,l(),r())) -> BS#(l()) -> BS#(N(x,l(),r())) -> and#(BS(l()),BS(r())) BS#(N(x,l(),r())) -> BS#(l()) -> BS#(N(x,l(),r())) -> BS#(l()) BS#(N(x,l(),r())) -> BS#(l()) -> BS#(N(x,l(),r())) -> BS#(r()) BS#(N(x,l(),r())) -> Max#(l()) -> Max#(N(x,l(),r())) -> Max#(r()) BS#(N(x,l(),r())) -> Min#(r()) -> Min#(N(x,l(),r())) -> Min#(l()) BS#(N(x,l(),r())) -> ge#(Min(r()),x) -> ge#(0(),O(x)) -> ge#(0(),x) BS#(N(x,l(),r())) -> ge#(Min(r()),x) -> ge#(I(x),I(y)) -> ge#(x,y) BS#(N(x,l(),r())) -> ge#(Min(r()),x) -> ge#(I(x),O(y)) -> ge#(x,y) BS#(N(x,l(),r())) -> ge#(Min(r()),x) -> ge#(O(x),I(y)) -> not#(ge(y,x)) BS#(N(x,l(),r())) -> ge#(Min(r()),x) -> ge#(O(x),I(y)) -> ge#(y,x) BS#(N(x,l(),r())) -> ge#(Min(r()),x) -> ge#(O(x),O(y)) -> ge#(x,y) BS#(N(x,l(),r())) -> ge#(x,Max(l())) -> ge#(0(),O(x)) -> ge#(0(),x) BS#(N(x,l(),r())) -> ge#(x,Max(l())) -> ge#(I(x),I(y)) -> ge#(x,y) BS#(N(x,l(),r())) -> ge#(x,Max(l())) -> ge#(I(x),O(y)) -> ge#(x,y) BS#(N(x,l(),r())) -> ge#(x,Max(l())) -> ge#(O(x),I(y)) -> not#(ge(y,x)) BS#(N(x,l(),r())) -> ge#(x,Max(l())) -> ge#(O(x),I(y)) -> ge#(y,x) BS#(N(x,l(),r())) -> ge#(x,Max(l())) -> ge#(O(x),O(y)) -> ge#(x,y) Max#(N(x,l(),r())) -> Max#(r()) -> Max#(N(x,l(),r())) -> Max#(r()) Min#(N(x,l(),r())) -> Min#(l()) -> Min#(N(x,l(),r())) -> Min#(l()) Log#(x) -> Log'#(x) -> Log'#(O(x)) -> if#(ge(x,I(0())),+(Log'(x),I(0())),0()) Log#(x) -> Log'#(x) -> Log'#(O(x)) -> ge#(x,I(0())) Log#(x) -> Log'#(x) -> Log'#(O(x)) -> +#(Log'(x),I(0())) Log#(x) -> Log'#(x) -> Log'#(O(x)) -> Log'#(x) Log#(x) -> Log'#(x) -> Log'#(I(x)) -> +#(Log'(x),I(0())) Log#(x) -> Log'#(x) -> Log'#(I(x)) -> Log'#(x) 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#(x) -> -#(Log'(x),I(0())) -> -#(I(x),O(y)) -> -#(x,y) Log#(x) -> -#(Log'(x),I(0())) -> -#(O(x),I(y)) -> -#(-(x,y),I(1())) Log#(x) -> -#(Log'(x),I(0())) -> -#(O(x),I(y)) -> -#(x,y) Log#(x) -> -#(Log'(x),I(0())) -> -#(O(x),O(y)) -> O#(-(x,y)) Log#(x) -> -#(Log'(x),I(0())) -> -#(O(x),O(y)) -> -#(x,y) Log'#(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),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) Log'#(I(x)) -> +#(Log'(x),I(0())) -> +#(x,+(y,z)) -> +#(+(x,y),z) Log'#(I(x)) -> +#(Log'(x),I(0())) -> +#(x,+(y,z)) -> +#(x,y) Log'#(I(x)) -> +#(Log'(x),I(0())) -> +#(I(x),I(y)) -> O#(+(+(x,y),I(0()))) Log'#(I(x)) -> +#(Log'(x),I(0())) -> +#(I(x),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),O(y)) -> +#(x,y) Log'#(I(x)) -> +#(Log'(x),I(0())) -> +#(O(x),I(y)) -> +#(x,y) Log'#(I(x)) -> +#(Log'(x),I(0())) -> +#(O(x),O(y)) -> O#(+(x,y)) Log'#(I(x)) -> +#(Log'(x),I(0())) -> +#(O(x),O(y)) -> +#(x,y) 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)) -> ge#(x,I(0())) Log'#(O(x)) -> Log'#(x) -> Log'#(O(x)) -> +#(Log'(x),I(0())) Log'#(O(x)) -> Log'#(x) -> Log'#(O(x)) -> Log'#(x) Log'#(O(x)) -> Log'#(x) -> Log'#(I(x)) -> +#(Log'(x),I(0())) Log'#(O(x)) -> Log'#(x) -> Log'#(I(x)) -> Log'#(x) Log'#(O(x)) -> ge#(x,I(0())) -> ge#(0(),O(x)) -> ge#(0(),x) Log'#(O(x)) -> ge#(x,I(0())) -> ge#(I(x),I(y)) -> ge#(x,y) Log'#(O(x)) -> ge#(x,I(0())) -> ge#(I(x),O(y)) -> ge#(x,y) Log'#(O(x)) -> ge#(x,I(0())) -> ge#(O(x),I(y)) -> not#(ge(y,x)) Log'#(O(x)) -> ge#(x,I(0())) -> ge#(O(x),I(y)) -> ge#(y,x) Log'#(O(x)) -> ge#(x,I(0())) -> ge#(O(x),O(y)) -> ge#(x,y) Log'#(O(x)) -> +#(Log'(x),I(0())) -> +#(x,+(y,z)) -> +#(+(x,y),z) Log'#(O(x)) -> +#(Log'(x),I(0())) -> +#(x,+(y,z)) -> +#(x,y) Log'#(O(x)) -> +#(Log'(x),I(0())) -> +#(I(x),I(y)) -> O#(+(+(x,y),I(0()))) 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),O(y)) -> +#(x,y) Log'#(O(x)) -> +#(Log'(x),I(0())) -> +#(O(x),I(y)) -> +#(x,y) Log'#(O(x)) -> +#(Log'(x),I(0())) -> +#(O(x),O(y)) -> O#(+(x,y)) Log'#(O(x)) -> +#(Log'(x),I(0())) -> +#(O(x),O(y)) -> +#(x,y) ge#(I(x),I(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)) -> not#(ge(y,x)) 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),O(y)) -> ge#(x,y) ge#(I(x),O(y)) -> ge#(x,y) -> ge#(0(),O(x)) -> ge#(0(),x) ge#(I(x),O(y)) -> ge#(x,y) -> ge#(I(x),I(y)) -> ge#(x,y) 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#(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#(O(x),O(y)) -> ge#(x,y) ge#(O(x),I(y)) -> ge#(y,x) -> 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)) -> not#(ge(y,x)) ge#(O(x),I(y)) -> ge#(y,x) -> ge#(O(x),I(y)) -> ge#(y,x) ge#(O(x),I(y)) -> ge#(y,x) -> ge#(O(x),O(y)) -> ge#(x,y) ge#(O(x),O(y)) -> ge#(x,y) -> ge#(0(),O(x)) -> ge#(0(),x) 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)) -> not#(ge(y,x)) 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),O(y)) -> ge#(x,y) ge#(0(),O(x)) -> ge#(0(),x) -> ge#(0(),O(x)) -> ge#(0(),x) ge#(0(),O(x)) -> ge#(0(),x) -> ge#(I(x),I(y)) -> ge#(x,y) ge#(0(),O(x)) -> ge#(0(),x) -> ge#(I(x),O(y)) -> ge#(x,y) ge#(0(),O(x)) -> ge#(0(),x) -> ge#(O(x),I(y)) -> not#(ge(y,x)) ge#(0(),O(x)) -> ge#(0(),x) -> ge#(O(x),I(y)) -> ge#(y,x) ge#(0(),O(x)) -> ge#(0(),x) -> ge#(O(x),O(y)) -> ge#(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) -#(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(1())) -#(I(x),I(y)) -> -#(x,y) -> -#(O(x),I(y)) -> -#(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),O(y)) -> -#(x,y) -> -#(I(x),I(y)) -> O#(-(x,y)) -#(I(x),O(y)) -> -#(x,y) -> -#(I(x),I(y)) -> -#(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)) -> O#(-(x,y)) -#(I(x),O(y)) -> -#(x,y) -> -#(O(x),O(y)) -> -#(x,y) -#(O(x),I(y)) -> -#(-(x,y),I(1())) -> -#(I(x),I(y)) -> O#(-(x,y)) -#(O(x),I(y)) -> -#(-(x,y),I(1())) -> -#(I(x),I(y)) -> -#(x,y) -#(O(x),I(y)) -> -#(-(x,y),I(1())) -> -#(I(x),O(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())) -> -#(O(x),I(y)) -> -#(x,y) -#(O(x),I(y)) -> -#(-(x,y),I(1())) -> -#(O(x),O(y)) -> O#(-(x,y)) -#(O(x),I(y)) -> -#(-(x,y),I(1())) -> -#(O(x),O(y)) -> -#(x,y) -#(O(x),I(y)) -> -#(x,y) -> -#(I(x),I(y)) -> O#(-(x,y)) -#(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),I(1())) -#(O(x),I(y)) -> -#(x,y) -> -#(O(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),O(y)) -> -#(x,y) -> -#(I(x),I(y)) -> O#(-(x,y)) -#(O(x),O(y)) -> -#(x,y) -> -#(I(x),I(y)) -> -#(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)) -> O#(-(x,y)) -#(O(x),O(y)) -> -#(x,y) -> -#(O(x),O(y)) -> -#(x,y) +#(I(x),I(y)) -> +#(+(x,y),I(0())) -> +#(x,+(y,z)) -> +#(+(x,y),z) +#(I(x),I(y)) -> +#(+(x,y),I(0())) -> +#(x,+(y,z)) -> +#(x,y) +#(I(x),I(y)) -> +#(+(x,y),I(0())) -> +#(I(x),I(y)) -> O#(+(+(x,y),I(0()))) +#(I(x),I(y)) -> +#(+(x,y),I(0())) -> +#(I(x),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),O(y)) -> +#(x,y) +#(I(x),I(y)) -> +#(+(x,y),I(0())) -> +#(O(x),I(y)) -> +#(x,y) +#(I(x),I(y)) -> +#(+(x,y),I(0())) -> +#(O(x),O(y)) -> O#(+(x,y)) +#(I(x),I(y)) -> +#(+(x,y),I(0())) -> +#(O(x),O(y)) -> +#(x,y) +#(I(x),I(y)) -> +#(x,y) -> +#(x,+(y,z)) -> +#(+(x,y),z) +#(I(x),I(y)) -> +#(x,y) -> +#(x,+(y,z)) -> +#(x,y) +#(I(x),I(y)) -> +#(x,y) -> +#(I(x),I(y)) -> O#(+(+(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(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)) -> O#(+(x,y)) +#(I(x),I(y)) -> +#(x,y) -> +#(O(x),O(y)) -> +#(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) +#(I(x),O(y)) -> +#(x,y) -> +#(I(x),I(y)) -> O#(+(+(x,y),I(0()))) +#(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),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)) -> O#(+(x,y)) +#(I(x),O(y)) -> +#(x,y) -> +#(O(x),O(y)) -> +#(x,y) +#(O(x),I(y)) -> +#(x,y) -> +#(x,+(y,z)) -> +#(+(x,y),z) +#(O(x),I(y)) -> +#(x,y) -> +#(x,+(y,z)) -> +#(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),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)) -> O#(+(x,y)) +#(O(x),I(y)) -> +#(x,y) -> +#(O(x),O(y)) -> +#(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) +#(O(x),O(y)) -> +#(x,y) -> +#(I(x),I(y)) -> O#(+(+(x,y),I(0()))) +#(O(x),O(y)) -> +#(x,y) -> +#(I(x),I(y)) -> +#(+(x,y),I(0())) +#(O(x),O(y)) -> +#(x,y) -> +#(I(x),I(y)) -> +#(x,y) +#(O(x),O(y)) -> +#(x,y) -> +#(I(x),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)) -> O#(+(x,y)) +#(O(x),O(y)) -> +#(x,y) -> +#(O(x),O(y)) -> +#(x,y) +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(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),I(0())) +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(I(x),I(y)) -> +#(x,y) +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(I(x),O(y)) -> +#(x,y) +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(O(x),I(y)) -> +#(x,y) +#(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) -> +#(x,+(y,z)) -> +#(+(x,y),z) +#(x,+(y,z)) -> +#(x,y) -> +#(x,+(y,z)) -> +#(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),I(0())) +#(x,+(y,z)) -> +#(x,y) -> +#(I(x),I(y)) -> +#(x,y) +#(x,+(y,z)) -> +#(x,y) -> +#(I(x),O(y)) -> +#(x,y) +#(x,+(y,z)) -> +#(x,y) -> +#(O(x),I(y)) -> +#(x,y) +#(x,+(y,z)) -> +#(x,y) -> +#(O(x),O(y)) -> O#(+(x,y)) +#(x,+(y,z)) -> +#(x,y) -> +#(O(x),O(y)) -> +#(x,y) SCC Processor: #sccs: 9 #rules: 27 #arcs: 301/3249 DPs: Log'#(I(x)) -> Log'#(x) Log'#(O(x)) -> Log'#(x) TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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()))) Subterm Criterion Processor: simple projection: pi(Log'#) = 0 problem: DPs: TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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 DPs: BS#(N(x,l(),r())) -> BS#(r()) BS#(N(x,l(),r())) -> BS#(l()) TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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()))) Subterm Criterion Processor: simple projection: pi(BS#) = 0 problem: DPs: TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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 DPs: Max#(N(x,l(),r())) -> Max#(r()) TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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()))) Subterm Criterion Processor: simple projection: pi(Max#) = 0 problem: DPs: TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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 DPs: Min#(N(x,l(),r())) -> Min#(l()) TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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()))) Subterm Criterion Processor: simple projection: pi(Min#) = 0 problem: DPs: TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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 DPs: WB#(N(x,l(),r())) -> WB#(r()) WB#(N(x,l(),r())) -> WB#(l()) TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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()))) Subterm Criterion Processor: simple projection: pi(WB#) = 0 problem: DPs: TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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 DPs: Size#(N(x,l(),r())) -> Size#(r()) Size#(N(x,l(),r())) -> Size#(l()) TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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()))) Subterm Criterion Processor: simple projection: pi(Size#) = 0 problem: DPs: TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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 DPs: +#(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())) +#(x,+(y,z)) -> +#(x,y) +#(x,+(y,z)) -> +#(+(x,y),z) TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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 Processor: DPs: +#(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())) +#(x,+(y,z)) -> +#(x,y) +#(x,+(y,z)) -> +#(+(x,y),z) TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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()))) graph: +#(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),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)) -> +#(x,y) +#(I(x),I(y)) -> +#(x,y) -> +#(I(x),I(y)) -> +#(+(x,y),I(0())) +#(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),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())) +#(I(x),O(y)) -> +#(x,y) -> +#(x,+(y,z)) -> +#(x,y) +#(I(x),O(y)) -> +#(x,y) -> +#(x,+(y,z)) -> +#(+(x,y),z) +#(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)) -> +#(x,y) +#(O(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),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())) +#(O(x),O(y)) -> +#(x,y) -> +#(x,+(y,z)) -> +#(x,y) +#(O(x),O(y)) -> +#(x,y) -> +#(x,+(y,z)) -> +#(+(x,y),z) +#(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)) -> +#(x,y) +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(I(x),I(y)) -> +#(+(x,y),I(0())) +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(x,y) +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) +#(x,+(y,z)) -> +#(x,y) -> +#(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)) -> +#(x,y) +#(x,+(y,z)) -> +#(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) Matrix Interpretation Processor: dim=1 interpretation: [+#](x0, x1) = x1, [WB](x0) = x0, [Size](x0) = x0, [BS](x0) = 0, [Max](x0) = x0, [Min](x0) = x0, [N](x0, x1, x2) = 4x0 + 4x1, [r] = 0, [l] = 4, [Val](x0) = x0 + 4, [L](x0) = 2x0 + 3, [Log](x0) = 6x0 + 4, [Log'](x0) = 6x0 + 4, [ge](x0, x1) = 0, [if](x0, x1, x2) = x1 + 4x2 + 1, [and](x0, x1) = x0 + 2x1, [false] = 0, [not](x0) = 0, [true] = 0, [1] = 0, [-](x0, x1) = x0, [I](x0) = x0 + 3, [+](x0, x1) = x0 + 4x1, [O](x0) = x0 + 3, [0] = 0 orientation: +#(O(x),O(y)) = y + 3 >= y = +#(x,y) +#(O(x),I(y)) = y + 3 >= y = +#(x,y) +#(I(x),O(y)) = y + 3 >= y = +#(x,y) +#(I(x),I(y)) = y + 3 >= y = +#(x,y) +#(I(x),I(y)) = y + 3 >= 3 = +#(+(x,y),I(0())) +#(x,+(y,z)) = y + 4z >= y = +#(x,y) +#(x,+(y,z)) = y + 4z >= z = +#(+(x,y),z) O(0()) = 3 >= 0 = 0() +(0(),x) = 4x >= x = x +(x,0()) = x >= x = x +(O(x),O(y)) = x + 4y + 15 >= x + 4y + 3 = O(+(x,y)) +(O(x),I(y)) = x + 4y + 15 >= x + 4y + 3 = I(+(x,y)) +(I(x),O(y)) = x + 4y + 15 >= x + 4y + 3 = I(+(x,y)) +(I(x),I(y)) = x + 4y + 15 >= x + 4y + 15 = O(+(+(x,y),I(0()))) +(x,+(y,z)) = x + 4y + 16z >= x + 4y + 4z = +(+(x,y),z) -(x,0()) = x >= x = x -(0(),x) = 0 >= 0 = 0() -(O(x),O(y)) = x + 3 >= x + 3 = O(-(x,y)) -(O(x),I(y)) = x + 3 >= x + 3 = I(-(-(x,y),I(1()))) -(I(x),O(y)) = x + 3 >= x + 3 = I(-(x,y)) -(I(x),I(y)) = x + 3 >= x + 3 = O(-(x,y)) not(true()) = 0 >= 0 = false() not(false()) = 0 >= 0 = true() and(x,true()) = x >= x = x and(x,false()) = x >= 0 = false() if(true(),x,y) = x + 4y + 1 >= x = x if(false(),x,y) = x + 4y + 1 >= y = y ge(O(x),O(y)) = 0 >= 0 = ge(x,y) ge(O(x),I(y)) = 0 >= 0 = not(ge(y,x)) ge(I(x),O(y)) = 0 >= 0 = ge(x,y) ge(I(x),I(y)) = 0 >= 0 = ge(x,y) ge(x,0()) = 0 >= 0 = true() ge(0(),O(x)) = 0 >= 0 = ge(0(),x) ge(0(),I(x)) = 0 >= 0 = false() Log'(0()) = 4 >= 0 = 0() Log'(I(x)) = 6x + 22 >= 6x + 16 = +(Log'(x),I(0())) Log'(O(x)) = 6x + 22 >= 6x + 17 = if(ge(x,I(0())),+(Log'(x),I(0())),0()) Log(x) = 6x + 4 >= 6x + 4 = -(Log'(x),I(0())) Val(L(x)) = 2x + 7 >= x = x Val(N(x,l(),r())) = 4x + 20 >= x = x Min(L(x)) = 2x + 3 >= x = x Min(N(x,l(),r())) = 4x + 16 >= 4 = Min(l()) Max(L(x)) = 2x + 3 >= x = x Max(N(x,l(),r())) = 4x + 16 >= 0 = Max(r()) BS(L(x)) = 0 >= 0 = true() BS(N(x,l(),r())) = 0 >= 0 = and(and(ge(x,Max(l())),ge(Min(r()),x)),and(BS(l()),BS(r()))) Size(L(x)) = 2x + 3 >= 3 = I(0()) Size(N(x,l(),r())) = 4x + 16 >= 16 = +(+(Size(l()),Size(r())),I(1())) WB(L(x)) = 2x + 3 >= 0 = true() WB(N(x,l(),r())) = 4x + 16 >= 9 = 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()))) problem: DPs: +#(I(x),I(y)) -> +#(+(x,y),I(0())) +#(x,+(y,z)) -> +#(x,y) +#(x,+(y,z)) -> +#(+(x,y),z) TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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()))) SCC Processor: #sccs: 2 #rules: 3 #arcs: 45/9 DPs: +#(x,+(y,z)) -> +#(+(x,y),z) +#(x,+(y,z)) -> +#(x,y) TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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()))) Subterm Criterion Processor: simple projection: pi(+#) = 1 problem: DPs: TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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 DPs: +#(I(x),I(y)) -> +#(+(x,y),I(0())) TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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()))) Matrix Interpretation Processor: dim=1 interpretation: [+#](x0, x1) = 4x0 + 4x1, [WB](x0) = 4x0, [Size](x0) = 2x0 + 4, [BS](x0) = 4, [Max](x0) = 4x0, [Min](x0) = x0 + 4, [N](x0, x1, x2) = x0 + 6, [r] = 0, [l] = 3, [Val](x0) = x0 + 6, [L](x0) = x0, [Log](x0) = 7x0 + 4, [Log'](x0) = 6x0, [ge](x0, x1) = 2, [if](x0, x1, x2) = 4x0 + x1 + x2 + 1, [and](x0, x1) = x0 + 1, [false] = 0, [not](x0) = 2, [true] = 0, [1] = 0, [-](x0, x1) = x0 + 2x1, [I](x0) = x0 + 2, [+](x0, x1) = x0 + x1, [O](x0) = x0 + 2, [0] = 0 orientation: +#(I(x),I(y)) = 4x + 4y + 16 >= 4x + 4y + 8 = +#(+(x,y),I(0())) O(0()) = 2 >= 0 = 0() +(0(),x) = x >= x = x +(x,0()) = x >= x = x +(O(x),O(y)) = x + y + 4 >= x + y + 2 = O(+(x,y)) +(O(x),I(y)) = x + y + 4 >= x + y + 2 = I(+(x,y)) +(I(x),O(y)) = x + y + 4 >= x + y + 2 = I(+(x,y)) +(I(x),I(y)) = x + y + 4 >= x + y + 4 = O(+(+(x,y),I(0()))) +(x,+(y,z)) = x + y + z >= x + y + z = +(+(x,y),z) -(x,0()) = x >= x = x -(0(),x) = 2x >= 0 = 0() -(O(x),O(y)) = x + 2y + 6 >= x + 2y + 2 = O(-(x,y)) -(O(x),I(y)) = x + 2y + 6 >= x + 2y + 6 = I(-(-(x,y),I(1()))) -(I(x),O(y)) = x + 2y + 6 >= x + 2y + 2 = I(-(x,y)) -(I(x),I(y)) = x + 2y + 6 >= x + 2y + 2 = O(-(x,y)) not(true()) = 2 >= 0 = false() not(false()) = 2 >= 0 = true() and(x,true()) = x + 1 >= x = x and(x,false()) = x + 1 >= 0 = false() if(true(),x,y) = x + y + 1 >= x = x if(false(),x,y) = x + y + 1 >= y = y ge(O(x),O(y)) = 2 >= 2 = ge(x,y) ge(O(x),I(y)) = 2 >= 2 = not(ge(y,x)) ge(I(x),O(y)) = 2 >= 2 = ge(x,y) ge(I(x),I(y)) = 2 >= 2 = ge(x,y) ge(x,0()) = 2 >= 0 = true() ge(0(),O(x)) = 2 >= 2 = ge(0(),x) ge(0(),I(x)) = 2 >= 0 = false() Log'(0()) = 0 >= 0 = 0() Log'(I(x)) = 6x + 12 >= 6x + 2 = +(Log'(x),I(0())) Log'(O(x)) = 6x + 12 >= 6x + 11 = if(ge(x,I(0())),+(Log'(x),I(0())),0()) Log(x) = 7x + 4 >= 6x + 4 = -(Log'(x),I(0())) Val(L(x)) = x + 6 >= x = x Val(N(x,l(),r())) = x + 12 >= x = x Min(L(x)) = x + 4 >= x = x Min(N(x,l(),r())) = x + 10 >= 7 = Min(l()) Max(L(x)) = 4x >= x = x Max(N(x,l(),r())) = 4x + 24 >= 0 = Max(r()) BS(L(x)) = 4 >= 0 = true() BS(N(x,l(),r())) = 4 >= 4 = and(and(ge(x,Max(l())),ge(Min(r()),x)),and(BS(l()),BS(r()))) Size(L(x)) = 2x + 4 >= 2 = I(0()) Size(N(x,l(),r())) = 2x + 16 >= 16 = +(+(Size(l()),Size(r())),I(1())) WB(L(x)) = 4x >= 0 = true() WB(N(x,l(),r())) = 4x + 24 >= 14 = 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()))) problem: DPs: TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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 DPs: 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) ge#(0(),O(x)) -> ge#(0(),x) TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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 Processor: DPs: 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) ge#(0(),O(x)) -> ge#(0(),x) TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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()))) graph: 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#(O(x),I(y)) -> ge#(y,x) 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#(I(x),I(y)) -> ge#(x,y) ge#(I(x),I(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)) -> 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) ge#(I(x),O(y)) -> ge#(x,y) -> ge#(0(),O(x)) -> ge#(0(),x) ge#(O(x),I(y)) -> ge#(y,x) -> ge#(O(x),O(y)) -> ge#(x,y) ge#(O(x),I(y)) -> ge#(y,x) -> ge#(O(x),I(y)) -> ge#(y,x) ge#(O(x),I(y)) -> ge#(y,x) -> ge#(I(x),O(y)) -> ge#(x,y) ge#(O(x),I(y)) -> ge#(y,x) -> ge#(I(x),I(y)) -> ge#(x,y) ge#(O(x),I(y)) -> ge#(y,x) -> ge#(0(),O(x)) -> ge#(0(),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#(O(x),I(y)) -> ge#(y,x) 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#(I(x),I(y)) -> ge#(x,y) ge#(O(x),O(y)) -> ge#(x,y) -> ge#(0(),O(x)) -> ge#(0(),x) ge#(0(),O(x)) -> ge#(0(),x) -> ge#(0(),O(x)) -> ge#(0(),x) SCC Processor: #sccs: 2 #rules: 5 #arcs: 21/25 DPs: ge#(I(x),I(y)) -> ge#(x,y) ge#(I(x),O(y)) -> ge#(x,y) ge#(O(x),I(y)) -> ge#(y,x) ge#(O(x),O(y)) -> ge#(x,y) TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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()))) Size-Change Termination Processor: DPs: TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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()))) The DP: ge#(I(x),I(y)) -> ge#(x,y) has the edges: 0 > 0 1 > 1 The DP: ge#(I(x),O(y)) -> ge#(x,y) has the edges: 0 > 0 1 > 1 The DP: ge#(O(x),I(y)) -> ge#(y,x) has the edges: 0 > 1 1 > 0 The DP: ge#(O(x),O(y)) -> ge#(x,y) has the edges: 0 > 0 1 > 1 Qed DPs: ge#(0(),O(x)) -> ge#(0(),x) TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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()))) Subterm Criterion Processor: simple projection: pi(ge#) = 1 problem: DPs: TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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 DPs: -#(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) TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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 Processor: DPs: -#(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) TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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()))) graph: -#(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)) -> -#(x,y) -#(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) -> -#(O(x),I(y)) -> -#(-(x,y),I(1())) -#(I(x),O(y)) -> -#(x,y) -> -#(I(x),O(y)) -> -#(x,y) -#(I(x),O(y)) -> -#(x,y) -> -#(I(x),I(y)) -> -#(x,y) -#(O(x),I(y)) -> -#(-(x,y),I(1())) -> -#(O(x),I(y)) -> -#(x,y) -#(O(x),I(y)) -> -#(-(x,y),I(1())) -> -#(O(x),I(y)) -> -#(-(x,y),I(1())) -#(O(x),I(y)) -> -#(-(x,y),I(1())) -> -#(I(x),I(y)) -> -#(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)) -> -#(x,y) -#(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) -> -#(O(x),I(y)) -> -#(-(x,y),I(1())) -#(O(x),O(y)) -> -#(x,y) -> -#(I(x),O(y)) -> -#(x,y) -#(O(x),O(y)) -> -#(x,y) -> -#(I(x),I(y)) -> -#(x,y) Matrix Interpretation Processor: dim=1 interpretation: [-#](x0, x1) = 2x0, [WB](x0) = 0, [Size](x0) = 2x0, [BS](x0) = 4x0, [Max](x0) = x0 + 4, [Min](x0) = 3x0 + 4, [N](x0, x1, x2) = x0 + x2 + 1, [r] = 2, [l] = 0, [Val](x0) = 2x0 + 2, [L](x0) = 4x0 + 5, [Log](x0) = 4x0 + 7, [Log'](x0) = x0 + 7, [ge](x0, x1) = 0, [if](x0, x1, x2) = x1 + x2, [and](x0, x1) = x0, [false] = 0, [not](x0) = 0, [true] = 0, [1] = 1, [-](x0, x1) = x0, [I](x0) = x0 + 1, [+](x0, x1) = x0 + x1, [O](x0) = x0 + 1, [0] = 0 orientation: -#(O(x),O(y)) = 2x + 2 >= 2x = -#(x,y) -#(O(x),I(y)) = 2x + 2 >= 2x = -#(x,y) -#(O(x),I(y)) = 2x + 2 >= 2x = -#(-(x,y),I(1())) -#(I(x),O(y)) = 2x + 2 >= 2x = -#(x,y) -#(I(x),I(y)) = 2x + 2 >= 2x = -#(x,y) O(0()) = 1 >= 0 = 0() +(0(),x) = x >= x = x +(x,0()) = x >= x = x +(O(x),O(y)) = x + y + 2 >= x + y + 1 = O(+(x,y)) +(O(x),I(y)) = x + y + 2 >= x + y + 1 = I(+(x,y)) +(I(x),O(y)) = x + y + 2 >= x + y + 1 = I(+(x,y)) +(I(x),I(y)) = x + y + 2 >= x + y + 2 = O(+(+(x,y),I(0()))) +(x,+(y,z)) = x + y + z >= x + y + z = +(+(x,y),z) -(x,0()) = x >= x = x -(0(),x) = 0 >= 0 = 0() -(O(x),O(y)) = x + 1 >= x + 1 = O(-(x,y)) -(O(x),I(y)) = x + 1 >= x + 1 = I(-(-(x,y),I(1()))) -(I(x),O(y)) = x + 1 >= x + 1 = I(-(x,y)) -(I(x),I(y)) = x + 1 >= x + 1 = O(-(x,y)) not(true()) = 0 >= 0 = false() not(false()) = 0 >= 0 = true() and(x,true()) = x >= x = x and(x,false()) = x >= 0 = false() if(true(),x,y) = x + y >= x = x if(false(),x,y) = x + y >= y = y ge(O(x),O(y)) = 0 >= 0 = ge(x,y) ge(O(x),I(y)) = 0 >= 0 = not(ge(y,x)) ge(I(x),O(y)) = 0 >= 0 = ge(x,y) ge(I(x),I(y)) = 0 >= 0 = ge(x,y) ge(x,0()) = 0 >= 0 = true() ge(0(),O(x)) = 0 >= 0 = ge(0(),x) ge(0(),I(x)) = 0 >= 0 = false() Log'(0()) = 7 >= 0 = 0() Log'(I(x)) = x + 8 >= x + 8 = +(Log'(x),I(0())) Log'(O(x)) = x + 8 >= x + 8 = if(ge(x,I(0())),+(Log'(x),I(0())),0()) Log(x) = 4x + 7 >= x + 7 = -(Log'(x),I(0())) Val(L(x)) = 8x + 12 >= x = x Val(N(x,l(),r())) = 2x + 8 >= x = x Min(L(x)) = 12x + 19 >= x = x Min(N(x,l(),r())) = 3x + 13 >= 4 = Min(l()) Max(L(x)) = 4x + 9 >= x = x Max(N(x,l(),r())) = x + 7 >= 6 = Max(r()) BS(L(x)) = 16x + 20 >= 0 = true() BS(N(x,l(),r())) = 4x + 12 >= 0 = and(and(ge(x,Max(l())),ge(Min(r()),x)),and(BS(l()),BS(r()))) Size(L(x)) = 8x + 10 >= 1 = I(0()) Size(N(x,l(),r())) = 2x + 6 >= 6 = +(+(Size(l()),Size(r())),I(1())) WB(L(x)) = 0 >= 0 = true() WB(N(x,l(),r())) = 0 >= 0 = 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()))) problem: DPs: TRS: O(0()) -> 0() +(0(),x) -> x +(x,0()) -> 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,+(y,z)) -> +(+(x,y),z) -(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(true()) -> false() not(false()) -> true() and(x,true()) -> x and(x,false()) -> false() if(true(),x,y) -> x if(false(),x,y) -> y 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) ge(x,0()) -> true() ge(0(),O(x)) -> ge(0(),x) ge(0(),I(x)) -> false() Log'(0()) -> 0() Log'(I(x)) -> +(Log'(x),I(0())) Log'(O(x)) -> if(ge(x,I(0())),+(Log'(x),I(0())),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