MAYBE Problem: cond1(true(),x,y) -> cond2(gr(x,y),x,y) cond2(true(),x,y) -> cond3(gr(x,0()),x,y) cond2(false(),x,y) -> cond4(gr(y,0()),x,y) cond3(true(),x,y) -> cond3(gr(x,0()),p(x),y) cond3(false(),x,y) -> cond1(and(gr(x,0()),gr(y,0())),x,y) cond4(true(),x,y) -> cond4(gr(y,0()),x,p(y)) cond4(false(),x,y) -> cond1(and(gr(x,0()),gr(y,0())),x,y) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) and(true(),true()) -> true() and(false(),x) -> false() and(x,false()) -> false() p(0()) -> 0() p(s(x)) -> x Proof: DP Processor: DPs: cond1#(true(),x,y) -> gr#(x,y) cond1#(true(),x,y) -> cond2#(gr(x,y),x,y) cond2#(true(),x,y) -> gr#(x,0()) cond2#(true(),x,y) -> cond3#(gr(x,0()),x,y) cond2#(false(),x,y) -> gr#(y,0()) cond2#(false(),x,y) -> cond4#(gr(y,0()),x,y) cond3#(true(),x,y) -> p#(x) cond3#(true(),x,y) -> gr#(x,0()) cond3#(true(),x,y) -> cond3#(gr(x,0()),p(x),y) cond3#(false(),x,y) -> gr#(y,0()) cond3#(false(),x,y) -> gr#(x,0()) cond3#(false(),x,y) -> and#(gr(x,0()),gr(y,0())) cond3#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) cond4#(true(),x,y) -> p#(y) cond4#(true(),x,y) -> gr#(y,0()) cond4#(true(),x,y) -> cond4#(gr(y,0()),x,p(y)) cond4#(false(),x,y) -> gr#(y,0()) cond4#(false(),x,y) -> gr#(x,0()) cond4#(false(),x,y) -> and#(gr(x,0()),gr(y,0())) cond4#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) gr#(s(x),s(y)) -> gr#(x,y) TRS: cond1(true(),x,y) -> cond2(gr(x,y),x,y) cond2(true(),x,y) -> cond3(gr(x,0()),x,y) cond2(false(),x,y) -> cond4(gr(y,0()),x,y) cond3(true(),x,y) -> cond3(gr(x,0()),p(x),y) cond3(false(),x,y) -> cond1(and(gr(x,0()),gr(y,0())),x,y) cond4(true(),x,y) -> cond4(gr(y,0()),x,p(y)) cond4(false(),x,y) -> cond1(and(gr(x,0()),gr(y,0())),x,y) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) and(true(),true()) -> true() and(false(),x) -> false() and(x,false()) -> false() p(0()) -> 0() p(s(x)) -> x Usable Rule Processor: DPs: cond1#(true(),x,y) -> gr#(x,y) cond1#(true(),x,y) -> cond2#(gr(x,y),x,y) cond2#(true(),x,y) -> gr#(x,0()) cond2#(true(),x,y) -> cond3#(gr(x,0()),x,y) cond2#(false(),x,y) -> gr#(y,0()) cond2#(false(),x,y) -> cond4#(gr(y,0()),x,y) cond3#(true(),x,y) -> p#(x) cond3#(true(),x,y) -> gr#(x,0()) cond3#(true(),x,y) -> cond3#(gr(x,0()),p(x),y) cond3#(false(),x,y) -> gr#(y,0()) cond3#(false(),x,y) -> gr#(x,0()) cond3#(false(),x,y) -> and#(gr(x,0()),gr(y,0())) cond3#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) cond4#(true(),x,y) -> p#(y) cond4#(true(),x,y) -> gr#(y,0()) cond4#(true(),x,y) -> cond4#(gr(y,0()),x,p(y)) cond4#(false(),x,y) -> gr#(y,0()) cond4#(false(),x,y) -> gr#(x,0()) cond4#(false(),x,y) -> and#(gr(x,0()),gr(y,0())) cond4#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) gr#(s(x),s(y)) -> gr#(x,y) TRS: f18(x,y) -> x f18(x,y) -> y gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) p(0()) -> 0() p(s(x)) -> x and(true(),true()) -> true() and(false(),x) -> false() and(x,false()) -> false() TDG Processor: DPs: cond1#(true(),x,y) -> gr#(x,y) cond1#(true(),x,y) -> cond2#(gr(x,y),x,y) cond2#(true(),x,y) -> gr#(x,0()) cond2#(true(),x,y) -> cond3#(gr(x,0()),x,y) cond2#(false(),x,y) -> gr#(y,0()) cond2#(false(),x,y) -> cond4#(gr(y,0()),x,y) cond3#(true(),x,y) -> p#(x) cond3#(true(),x,y) -> gr#(x,0()) cond3#(true(),x,y) -> cond3#(gr(x,0()),p(x),y) cond3#(false(),x,y) -> gr#(y,0()) cond3#(false(),x,y) -> gr#(x,0()) cond3#(false(),x,y) -> and#(gr(x,0()),gr(y,0())) cond3#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) cond4#(true(),x,y) -> p#(y) cond4#(true(),x,y) -> gr#(y,0()) cond4#(true(),x,y) -> cond4#(gr(y,0()),x,p(y)) cond4#(false(),x,y) -> gr#(y,0()) cond4#(false(),x,y) -> gr#(x,0()) cond4#(false(),x,y) -> and#(gr(x,0()),gr(y,0())) cond4#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) gr#(s(x),s(y)) -> gr#(x,y) TRS: f18(x,y) -> x f18(x,y) -> y gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) p(0()) -> 0() p(s(x)) -> x and(true(),true()) -> true() and(false(),x) -> false() and(x,false()) -> false() graph: cond4#(false(),x,y) -> gr#(y,0()) -> gr#(s(x),s(y)) -> gr#(x,y) cond4#(false(),x,y) -> gr#(x,0()) -> gr#(s(x),s(y)) -> gr#(x,y) cond4#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) -> cond1#(true(),x,y) -> cond2#(gr(x,y),x,y) cond4#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) -> cond1#(true(),x,y) -> gr#(x,y) cond4#(true(),x,y) -> cond4#(gr(y,0()),x,p(y)) -> cond4#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) cond4#(true(),x,y) -> cond4#(gr(y,0()),x,p(y)) -> cond4#(false(),x,y) -> and#(gr(x,0()),gr(y,0())) cond4#(true(),x,y) -> cond4#(gr(y,0()),x,p(y)) -> cond4#(false(),x,y) -> gr#(x,0()) cond4#(true(),x,y) -> cond4#(gr(y,0()),x,p(y)) -> cond4#(false(),x,y) -> gr#(y,0()) cond4#(true(),x,y) -> cond4#(gr(y,0()),x,p(y)) -> cond4#(true(),x,y) -> cond4#(gr(y,0()),x,p(y)) cond4#(true(),x,y) -> cond4#(gr(y,0()),x,p(y)) -> cond4#(true(),x,y) -> gr#(y,0()) cond4#(true(),x,y) -> cond4#(gr(y,0()),x,p(y)) -> cond4#(true(),x,y) -> p#(y) cond4#(true(),x,y) -> gr#(y,0()) -> gr#(s(x),s(y)) -> gr#(x,y) cond3#(false(),x,y) -> gr#(y,0()) -> gr#(s(x),s(y)) -> gr#(x,y) cond3#(false(),x,y) -> gr#(x,0()) -> gr#(s(x),s(y)) -> gr#(x,y) cond3#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) -> cond1#(true(),x,y) -> cond2#(gr(x,y),x,y) cond3#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) -> cond1#(true(),x,y) -> gr#(x,y) cond3#(true(),x,y) -> cond3#(gr(x,0()),p(x),y) -> cond3#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) cond3#(true(),x,y) -> cond3#(gr(x,0()),p(x),y) -> cond3#(false(),x,y) -> and#(gr(x,0()),gr(y,0())) cond3#(true(),x,y) -> cond3#(gr(x,0()),p(x),y) -> cond3#(false(),x,y) -> gr#(x,0()) cond3#(true(),x,y) -> cond3#(gr(x,0()),p(x),y) -> cond3#(false(),x,y) -> gr#(y,0()) cond3#(true(),x,y) -> cond3#(gr(x,0()),p(x),y) -> cond3#(true(),x,y) -> cond3#(gr(x,0()),p(x),y) cond3#(true(),x,y) -> cond3#(gr(x,0()),p(x),y) -> cond3#(true(),x,y) -> gr#(x,0()) cond3#(true(),x,y) -> cond3#(gr(x,0()),p(x),y) -> cond3#(true(),x,y) -> p#(x) cond3#(true(),x,y) -> gr#(x,0()) -> gr#(s(x),s(y)) -> gr#(x,y) cond2#(false(),x,y) -> cond4#(gr(y,0()),x,y) -> cond4#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) cond2#(false(),x,y) -> cond4#(gr(y,0()),x,y) -> cond4#(false(),x,y) -> and#(gr(x,0()),gr(y,0())) cond2#(false(),x,y) -> cond4#(gr(y,0()),x,y) -> cond4#(false(),x,y) -> gr#(x,0()) cond2#(false(),x,y) -> cond4#(gr(y,0()),x,y) -> cond4#(false(),x,y) -> gr#(y,0()) cond2#(false(),x,y) -> cond4#(gr(y,0()),x,y) -> cond4#(true(),x,y) -> cond4#(gr(y,0()),x,p(y)) cond2#(false(),x,y) -> cond4#(gr(y,0()),x,y) -> cond4#(true(),x,y) -> gr#(y,0()) cond2#(false(),x,y) -> cond4#(gr(y,0()),x,y) -> cond4#(true(),x,y) -> p#(y) cond2#(false(),x,y) -> gr#(y,0()) -> gr#(s(x),s(y)) -> gr#(x,y) cond2#(true(),x,y) -> cond3#(gr(x,0()),x,y) -> cond3#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) cond2#(true(),x,y) -> cond3#(gr(x,0()),x,y) -> cond3#(false(),x,y) -> and#(gr(x,0()),gr(y,0())) cond2#(true(),x,y) -> cond3#(gr(x,0()),x,y) -> cond3#(false(),x,y) -> gr#(x,0()) cond2#(true(),x,y) -> cond3#(gr(x,0()),x,y) -> cond3#(false(),x,y) -> gr#(y,0()) cond2#(true(),x,y) -> cond3#(gr(x,0()),x,y) -> cond3#(true(),x,y) -> cond3#(gr(x,0()),p(x),y) cond2#(true(),x,y) -> cond3#(gr(x,0()),x,y) -> cond3#(true(),x,y) -> gr#(x,0()) cond2#(true(),x,y) -> cond3#(gr(x,0()),x,y) -> cond3#(true(),x,y) -> p#(x) cond2#(true(),x,y) -> gr#(x,0()) -> gr#(s(x),s(y)) -> gr#(x,y) gr#(s(x),s(y)) -> gr#(x,y) -> gr#(s(x),s(y)) -> gr#(x,y) cond1#(true(),x,y) -> cond2#(gr(x,y),x,y) -> cond2#(false(),x,y) -> cond4#(gr(y,0()),x,y) cond1#(true(),x,y) -> cond2#(gr(x,y),x,y) -> cond2#(false(),x,y) -> gr#(y,0()) cond1#(true(),x,y) -> cond2#(gr(x,y),x,y) -> cond2#(true(),x,y) -> cond3#(gr(x,0()),x,y) cond1#(true(),x,y) -> cond2#(gr(x,y),x,y) -> cond2#(true(),x,y) -> gr#(x,0()) cond1#(true(),x,y) -> gr#(x,y) -> gr#(s(x),s(y)) -> gr#(x,y) EDG Processor: DPs: cond1#(true(),x,y) -> gr#(x,y) cond1#(true(),x,y) -> cond2#(gr(x,y),x,y) cond2#(true(),x,y) -> gr#(x,0()) cond2#(true(),x,y) -> cond3#(gr(x,0()),x,y) cond2#(false(),x,y) -> gr#(y,0()) cond2#(false(),x,y) -> cond4#(gr(y,0()),x,y) cond3#(true(),x,y) -> p#(x) cond3#(true(),x,y) -> gr#(x,0()) cond3#(true(),x,y) -> cond3#(gr(x,0()),p(x),y) cond3#(false(),x,y) -> gr#(y,0()) cond3#(false(),x,y) -> gr#(x,0()) cond3#(false(),x,y) -> and#(gr(x,0()),gr(y,0())) cond3#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) cond4#(true(),x,y) -> p#(y) cond4#(true(),x,y) -> gr#(y,0()) cond4#(true(),x,y) -> cond4#(gr(y,0()),x,p(y)) cond4#(false(),x,y) -> gr#(y,0()) cond4#(false(),x,y) -> gr#(x,0()) cond4#(false(),x,y) -> and#(gr(x,0()),gr(y,0())) cond4#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) gr#(s(x),s(y)) -> gr#(x,y) TRS: f18(x,y) -> x f18(x,y) -> y gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) p(0()) -> 0() p(s(x)) -> x and(true(),true()) -> true() and(false(),x) -> false() and(x,false()) -> false() graph: cond4#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) -> cond1#(true(),x,y) -> gr#(x,y) cond4#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) -> cond1#(true(),x,y) -> cond2#(gr(x,y),x,y) cond4#(true(),x,y) -> cond4#(gr(y,0()),x,p(y)) -> cond4#(true(),x,y) -> p#(y) cond4#(true(),x,y) -> cond4#(gr(y,0()),x,p(y)) -> cond4#(true(),x,y) -> gr#(y,0()) cond4#(true(),x,y) -> cond4#(gr(y,0()),x,p(y)) -> cond4#(true(),x,y) -> cond4#(gr(y,0()),x,p(y)) cond4#(true(),x,y) -> cond4#(gr(y,0()),x,p(y)) -> cond4#(false(),x,y) -> gr#(y,0()) cond4#(true(),x,y) -> cond4#(gr(y,0()),x,p(y)) -> cond4#(false(),x,y) -> gr#(x,0()) cond4#(true(),x,y) -> cond4#(gr(y,0()),x,p(y)) -> cond4#(false(),x,y) -> and#(gr(x,0()),gr(y,0())) cond4#(true(),x,y) -> cond4#(gr(y,0()),x,p(y)) -> cond4#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) cond3#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) -> cond1#(true(),x,y) -> gr#(x,y) cond3#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) -> cond1#(true(),x,y) -> cond2#(gr(x,y),x,y) cond3#(true(),x,y) -> cond3#(gr(x,0()),p(x),y) -> cond3#(true(),x,y) -> p#(x) cond3#(true(),x,y) -> cond3#(gr(x,0()),p(x),y) -> cond3#(true(),x,y) -> gr#(x,0()) cond3#(true(),x,y) -> cond3#(gr(x,0()),p(x),y) -> cond3#(true(),x,y) -> cond3#(gr(x,0()),p(x),y) cond3#(true(),x,y) -> cond3#(gr(x,0()),p(x),y) -> cond3#(false(),x,y) -> gr#(y,0()) cond3#(true(),x,y) -> cond3#(gr(x,0()),p(x),y) -> cond3#(false(),x,y) -> gr#(x,0()) cond3#(true(),x,y) -> cond3#(gr(x,0()),p(x),y) -> cond3#(false(),x,y) -> and#(gr(x,0()),gr(y,0())) cond3#(true(),x,y) -> cond3#(gr(x,0()),p(x),y) -> cond3#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) cond2#(false(),x,y) -> cond4#(gr(y,0()),x,y) -> cond4#(true(),x,y) -> p#(y) cond2#(false(),x,y) -> cond4#(gr(y,0()),x,y) -> cond4#(true(),x,y) -> gr#(y,0()) cond2#(false(),x,y) -> cond4#(gr(y,0()),x,y) -> cond4#(true(),x,y) -> cond4#(gr(y,0()),x,p(y)) cond2#(false(),x,y) -> cond4#(gr(y,0()),x,y) -> cond4#(false(),x,y) -> gr#(y,0()) cond2#(false(),x,y) -> cond4#(gr(y,0()),x,y) -> cond4#(false(),x,y) -> gr#(x,0()) cond2#(false(),x,y) -> cond4#(gr(y,0()),x,y) -> cond4#(false(),x,y) -> and#(gr(x,0()),gr(y,0())) cond2#(false(),x,y) -> cond4#(gr(y,0()),x,y) -> cond4#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) cond2#(true(),x,y) -> cond3#(gr(x,0()),x,y) -> cond3#(true(),x,y) -> p#(x) cond2#(true(),x,y) -> cond3#(gr(x,0()),x,y) -> cond3#(true(),x,y) -> gr#(x,0()) cond2#(true(),x,y) -> cond3#(gr(x,0()),x,y) -> cond3#(true(),x,y) -> cond3#(gr(x,0()),p(x),y) cond2#(true(),x,y) -> cond3#(gr(x,0()),x,y) -> cond3#(false(),x,y) -> gr#(y,0()) cond2#(true(),x,y) -> cond3#(gr(x,0()),x,y) -> cond3#(false(),x,y) -> gr#(x,0()) cond2#(true(),x,y) -> cond3#(gr(x,0()),x,y) -> cond3#(false(),x,y) -> and#(gr(x,0()),gr(y,0())) cond2#(true(),x,y) -> cond3#(gr(x,0()),x,y) -> cond3#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) gr#(s(x),s(y)) -> gr#(x,y) -> gr#(s(x),s(y)) -> gr#(x,y) cond1#(true(),x,y) -> cond2#(gr(x,y),x,y) -> cond2#(true(),x,y) -> gr#(x,0()) cond1#(true(),x,y) -> cond2#(gr(x,y),x,y) -> cond2#(true(),x,y) -> cond3#(gr(x,0()),x,y) cond1#(true(),x,y) -> cond2#(gr(x,y),x,y) -> cond2#(false(),x,y) -> gr#(y,0()) cond1#(true(),x,y) -> cond2#(gr(x,y),x,y) -> cond2#(false(),x,y) -> cond4#(gr(y,0()),x,y) cond1#(true(),x,y) -> gr#(x,y) -> gr#(s(x),s(y)) -> gr#(x,y) Restore Modifier: DPs: cond1#(true(),x,y) -> gr#(x,y) cond1#(true(),x,y) -> cond2#(gr(x,y),x,y) cond2#(true(),x,y) -> gr#(x,0()) cond2#(true(),x,y) -> cond3#(gr(x,0()),x,y) cond2#(false(),x,y) -> gr#(y,0()) cond2#(false(),x,y) -> cond4#(gr(y,0()),x,y) cond3#(true(),x,y) -> p#(x) cond3#(true(),x,y) -> gr#(x,0()) cond3#(true(),x,y) -> cond3#(gr(x,0()),p(x),y) cond3#(false(),x,y) -> gr#(y,0()) cond3#(false(),x,y) -> gr#(x,0()) cond3#(false(),x,y) -> and#(gr(x,0()),gr(y,0())) cond3#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) cond4#(true(),x,y) -> p#(y) cond4#(true(),x,y) -> gr#(y,0()) cond4#(true(),x,y) -> cond4#(gr(y,0()),x,p(y)) cond4#(false(),x,y) -> gr#(y,0()) cond4#(false(),x,y) -> gr#(x,0()) cond4#(false(),x,y) -> and#(gr(x,0()),gr(y,0())) cond4#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) gr#(s(x),s(y)) -> gr#(x,y) TRS: cond1(true(),x,y) -> cond2(gr(x,y),x,y) cond2(true(),x,y) -> cond3(gr(x,0()),x,y) cond2(false(),x,y) -> cond4(gr(y,0()),x,y) cond3(true(),x,y) -> cond3(gr(x,0()),p(x),y) cond3(false(),x,y) -> cond1(and(gr(x,0()),gr(y,0())),x,y) cond4(true(),x,y) -> cond4(gr(y,0()),x,p(y)) cond4(false(),x,y) -> cond1(and(gr(x,0()),gr(y,0())),x,y) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) and(true(),true()) -> true() and(false(),x) -> false() and(x,false()) -> false() p(0()) -> 0() p(s(x)) -> x SCC Processor: #sccs: 2 #rules: 8 #arcs: 38/441 DPs: cond4#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) cond1#(true(),x,y) -> cond2#(gr(x,y),x,y) cond2#(false(),x,y) -> cond4#(gr(y,0()),x,y) cond4#(true(),x,y) -> cond4#(gr(y,0()),x,p(y)) cond2#(true(),x,y) -> cond3#(gr(x,0()),x,y) cond3#(false(),x,y) -> cond1#(and(gr(x,0()),gr(y,0())),x,y) cond3#(true(),x,y) -> cond3#(gr(x,0()),p(x),y) TRS: cond1(true(),x,y) -> cond2(gr(x,y),x,y) cond2(true(),x,y) -> cond3(gr(x,0()),x,y) cond2(false(),x,y) -> cond4(gr(y,0()),x,y) cond3(true(),x,y) -> cond3(gr(x,0()),p(x),y) cond3(false(),x,y) -> cond1(and(gr(x,0()),gr(y,0())),x,y) cond4(true(),x,y) -> cond4(gr(y,0()),x,p(y)) cond4(false(),x,y) -> cond1(and(gr(x,0()),gr(y,0())),x,y) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) and(true(),true()) -> true() and(false(),x) -> false() and(x,false()) -> false() p(0()) -> 0() p(s(x)) -> x Open DPs: gr#(s(x),s(y)) -> gr#(x,y) TRS: cond1(true(),x,y) -> cond2(gr(x,y),x,y) cond2(true(),x,y) -> cond3(gr(x,0()),x,y) cond2(false(),x,y) -> cond4(gr(y,0()),x,y) cond3(true(),x,y) -> cond3(gr(x,0()),p(x),y) cond3(false(),x,y) -> cond1(and(gr(x,0()),gr(y,0())),x,y) cond4(true(),x,y) -> cond4(gr(y,0()),x,p(y)) cond4(false(),x,y) -> cond1(and(gr(x,0()),gr(y,0())),x,y) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) and(true(),true()) -> true() and(false(),x) -> false() and(x,false()) -> false() p(0()) -> 0() p(s(x)) -> x Matrix Interpretation Processor: dimension: 1 interpretation: [gr#](x0, x1) = x1 + 1, [s](x0) = x0 + 1, [and](x0, x1) = 0, [p](x0) = x0, [cond4](x0, x1, x2) = 0, [false] = 0, [cond3](x0, x1, x2) = 0, [0] = 0, [cond2](x0, x1, x2) = 0, [gr](x0, x1) = 0, [cond1](x0, x1, x2) = 0, [true] = 0 orientation: gr#(s(x),s(y)) = y + 2 >= y + 1 = gr#(x,y) cond1(true(),x,y) = 0 >= 0 = cond2(gr(x,y),x,y) cond2(true(),x,y) = 0 >= 0 = cond3(gr(x,0()),x,y) cond2(false(),x,y) = 0 >= 0 = cond4(gr(y,0()),x,y) cond3(true(),x,y) = 0 >= 0 = cond3(gr(x,0()),p(x),y) cond3(false(),x,y) = 0 >= 0 = cond1(and(gr(x,0()),gr(y,0())),x,y) cond4(true(),x,y) = 0 >= 0 = cond4(gr(y,0()),x,p(y)) cond4(false(),x,y) = 0 >= 0 = cond1(and(gr(x,0()),gr(y,0())),x,y) gr(0(),x) = 0 >= 0 = false() gr(s(x),0()) = 0 >= 0 = true() gr(s(x),s(y)) = 0 >= 0 = gr(x,y) and(true(),true()) = 0 >= 0 = true() and(false(),x) = 0 >= 0 = false() and(x,false()) = 0 >= 0 = false() p(0()) = 0 >= 0 = 0() p(s(x)) = x + 1 >= x = x problem: DPs: TRS: cond1(true(),x,y) -> cond2(gr(x,y),x,y) cond2(true(),x,y) -> cond3(gr(x,0()),x,y) cond2(false(),x,y) -> cond4(gr(y,0()),x,y) cond3(true(),x,y) -> cond3(gr(x,0()),p(x),y) cond3(false(),x,y) -> cond1(and(gr(x,0()),gr(y,0())),x,y) cond4(true(),x,y) -> cond4(gr(y,0()),x,p(y)) cond4(false(),x,y) -> cond1(and(gr(x,0()),gr(y,0())),x,y) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) and(true(),true()) -> true() and(false(),x) -> false() and(x,false()) -> false() p(0()) -> 0() p(s(x)) -> x Qed