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) Usable Rule 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: +(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) O(0()) -> 0() Semantic Labeling Processor: dimension: 1 usable rules: interpretation: [I](x0) = x0 + 1, [+](x0, x1) = x0 + x1 + 1, [O](x0) = x0, [0] = 0 labeled: +# I + usable (for model): +# O I + 0 argument filtering: pi(0) = [] pi(O) = [] pi(+) = 0 pi(I) = [] pi(+#) = [] precedence: +# ~ I ~ + ~ O ~ 0 problem: DPs: +#(O(x),O(y)) -> +#(x,y) +#(I(x),I(y)) -> +#(+(x,y),I(0())) +#(x,+(y,z)) -> +#(+(x,y),z) TRS: +(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) O(0()) -> 0() Restore Modifier: DPs: +#(O(x),O(y)) -> +#(x,y) +#(I(x),I(y)) -> +#(+(x,y),I(0())) +#(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: +#(O(x),O(y)) -> +#(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()))) 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()))) Usable Rule Processor: DPs: +#(I(x),I(y)) -> +#(+(x,y),I(0())) TRS: +(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) O(0()) -> 0() Semantic Labeling Processor: dimension: 1 usable rules: interpretation: [I](x0) = x0 + 1, [+](x0, x1) = x0 + x1, [O](x0) = x0, [0] = 0 labeled: +# + O usable (for model): +# I + 0 O argument filtering: pi(0) = [] pi(O) = [] pi(+) = 1 pi(I) = [] pi(+#) = [] precedence: +# ~ I ~ + ~ O ~ 0 problem: DPs: TRS: +(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) O(0()) -> 0() 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) Usable Rule 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: -(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)) O(0()) -> 0() Semantic Labeling Processor: dimension: 1 usable rules: interpretation: [1] = 1, [-](x0, x1) = x0, [I](x0) = x0 + 1, [O](x0) = x0 + 1, [0] = 0 labeled: -# I - usable (for model): -# O I - 1 0 argument filtering: pi(0) = [] pi(O) = 0 pi(I) = [] pi(-) = 0 pi(1) = [] pi(-#) = [] precedence: -# ~ 1 ~ - ~ I ~ O ~ 0 problem: DPs: TRS: -(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)) O(0()) -> 0() Qed