MAYBE Problem: cond1(true(),x,y) -> cond2(gr(x,0()),x,y) cond2(true(),x,y) -> cond1(gr(add(x,y),0()),p(x),y) cond2(false(),x,y) -> cond3(gr(y,0()),x,y) cond3(true(),x,y) -> cond1(gr(add(x,y),0()),x,p(y)) cond3(false(),x,y) -> cond1(gr(add(x,y),0()),x,y) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) add(0(),x) -> x add(s(x),y) -> s(add(x,y)) p(0()) -> 0() p(s(x)) -> x Proof: DP Processor: DPs: cond1#(true(),x,y) -> gr#(x,0()) cond1#(true(),x,y) -> cond2#(gr(x,0()),x,y) cond2#(true(),x,y) -> p#(x) cond2#(true(),x,y) -> add#(x,y) cond2#(true(),x,y) -> gr#(add(x,y),0()) cond2#(true(),x,y) -> cond1#(gr(add(x,y),0()),p(x),y) cond2#(false(),x,y) -> gr#(y,0()) cond2#(false(),x,y) -> cond3#(gr(y,0()),x,y) cond3#(true(),x,y) -> p#(y) cond3#(true(),x,y) -> add#(x,y) cond3#(true(),x,y) -> gr#(add(x,y),0()) cond3#(true(),x,y) -> cond1#(gr(add(x,y),0()),x,p(y)) cond3#(false(),x,y) -> add#(x,y) cond3#(false(),x,y) -> gr#(add(x,y),0()) cond3#(false(),x,y) -> cond1#(gr(add(x,y),0()),x,y) gr#(s(x),s(y)) -> gr#(x,y) add#(s(x),y) -> add#(x,y) TRS: cond1(true(),x,y) -> cond2(gr(x,0()),x,y) cond2(true(),x,y) -> cond1(gr(add(x,y),0()),p(x),y) cond2(false(),x,y) -> cond3(gr(y,0()),x,y) cond3(true(),x,y) -> cond1(gr(add(x,y),0()),x,p(y)) cond3(false(),x,y) -> cond1(gr(add(x,y),0()),x,y) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) add(0(),x) -> x add(s(x),y) -> s(add(x,y)) p(0()) -> 0() p(s(x)) -> x TDG Processor: DPs: cond1#(true(),x,y) -> gr#(x,0()) cond1#(true(),x,y) -> cond2#(gr(x,0()),x,y) cond2#(true(),x,y) -> p#(x) cond2#(true(),x,y) -> add#(x,y) cond2#(true(),x,y) -> gr#(add(x,y),0()) cond2#(true(),x,y) -> cond1#(gr(add(x,y),0()),p(x),y) cond2#(false(),x,y) -> gr#(y,0()) cond2#(false(),x,y) -> cond3#(gr(y,0()),x,y) cond3#(true(),x,y) -> p#(y) cond3#(true(),x,y) -> add#(x,y) cond3#(true(),x,y) -> gr#(add(x,y),0()) cond3#(true(),x,y) -> cond1#(gr(add(x,y),0()),x,p(y)) cond3#(false(),x,y) -> add#(x,y) cond3#(false(),x,y) -> gr#(add(x,y),0()) cond3#(false(),x,y) -> cond1#(gr(add(x,y),0()),x,y) gr#(s(x),s(y)) -> gr#(x,y) add#(s(x),y) -> add#(x,y) TRS: cond1(true(),x,y) -> cond2(gr(x,0()),x,y) cond2(true(),x,y) -> cond1(gr(add(x,y),0()),p(x),y) cond2(false(),x,y) -> cond3(gr(y,0()),x,y) cond3(true(),x,y) -> cond1(gr(add(x,y),0()),x,p(y)) cond3(false(),x,y) -> cond1(gr(add(x,y),0()),x,y) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) add(0(),x) -> x add(s(x),y) -> s(add(x,y)) p(0()) -> 0() p(s(x)) -> x graph: cond3#(false(),x,y) -> add#(x,y) -> add#(s(x),y) -> add#(x,y) cond3#(false(),x,y) -> gr#(add(x,y),0()) -> gr#(s(x),s(y)) -> gr#(x,y) cond3#(false(),x,y) -> cond1#(gr(add(x,y),0()),x,y) -> cond1#(true(),x,y) -> cond2#(gr(x,0()),x,y) cond3#(false(),x,y) -> cond1#(gr(add(x,y),0()),x,y) -> cond1#(true(),x,y) -> gr#(x,0()) cond3#(true(),x,y) -> add#(x,y) -> add#(s(x),y) -> add#(x,y) cond3#(true(),x,y) -> gr#(add(x,y),0()) -> gr#(s(x),s(y)) -> gr#(x,y) cond3#(true(),x,y) -> cond1#(gr(add(x,y),0()),x,p(y)) -> cond1#(true(),x,y) -> cond2#(gr(x,0()),x,y) cond3#(true(),x,y) -> cond1#(gr(add(x,y),0()),x,p(y)) -> cond1#(true(),x,y) -> gr#(x,0()) add#(s(x),y) -> add#(x,y) -> add#(s(x),y) -> add#(x,y) cond2#(false(),x,y) -> cond3#(gr(y,0()),x,y) -> cond3#(false(),x,y) -> cond1#(gr(add(x,y),0()),x,y) cond2#(false(),x,y) -> cond3#(gr(y,0()),x,y) -> cond3#(false(),x,y) -> gr#(add(x,y),0()) cond2#(false(),x,y) -> cond3#(gr(y,0()),x,y) -> cond3#(false(),x,y) -> add#(x,y) cond2#(false(),x,y) -> cond3#(gr(y,0()),x,y) -> cond3#(true(),x,y) -> cond1#(gr(add(x,y),0()),x,p(y)) cond2#(false(),x,y) -> cond3#(gr(y,0()),x,y) -> cond3#(true(),x,y) -> gr#(add(x,y),0()) cond2#(false(),x,y) -> cond3#(gr(y,0()),x,y) -> cond3#(true(),x,y) -> add#(x,y) cond2#(false(),x,y) -> cond3#(gr(y,0()),x,y) -> cond3#(true(),x,y) -> p#(y) cond2#(false(),x,y) -> gr#(y,0()) -> gr#(s(x),s(y)) -> gr#(x,y) cond2#(true(),x,y) -> add#(x,y) -> add#(s(x),y) -> add#(x,y) cond2#(true(),x,y) -> gr#(add(x,y),0()) -> gr#(s(x),s(y)) -> gr#(x,y) cond2#(true(),x,y) -> cond1#(gr(add(x,y),0()),p(x),y) -> cond1#(true(),x,y) -> cond2#(gr(x,0()),x,y) cond2#(true(),x,y) -> cond1#(gr(add(x,y),0()),p(x),y) -> cond1#(true(),x,y) -> gr#(x,0()) gr#(s(x),s(y)) -> gr#(x,y) -> gr#(s(x),s(y)) -> gr#(x,y) cond1#(true(),x,y) -> cond2#(gr(x,0()),x,y) -> cond2#(false(),x,y) -> cond3#(gr(y,0()),x,y) cond1#(true(),x,y) -> cond2#(gr(x,0()),x,y) -> cond2#(false(),x,y) -> gr#(y,0()) cond1#(true(),x,y) -> cond2#(gr(x,0()),x,y) -> cond2#(true(),x,y) -> cond1#(gr(add(x,y),0()),p(x),y) cond1#(true(),x,y) -> cond2#(gr(x,0()),x,y) -> cond2#(true(),x,y) -> gr#(add(x,y),0()) cond1#(true(),x,y) -> cond2#(gr(x,0()),x,y) -> cond2#(true(),x,y) -> add#(x,y) cond1#(true(),x,y) -> cond2#(gr(x,0()),x,y) -> cond2#(true(),x,y) -> p#(x) cond1#(true(),x,y) -> gr#(x,0()) -> gr#(s(x),s(y)) -> gr#(x,y) EDG Processor: DPs: cond1#(true(),x,y) -> gr#(x,0()) cond1#(true(),x,y) -> cond2#(gr(x,0()),x,y) cond2#(true(),x,y) -> p#(x) cond2#(true(),x,y) -> add#(x,y) cond2#(true(),x,y) -> gr#(add(x,y),0()) cond2#(true(),x,y) -> cond1#(gr(add(x,y),0()),p(x),y) cond2#(false(),x,y) -> gr#(y,0()) cond2#(false(),x,y) -> cond3#(gr(y,0()),x,y) cond3#(true(),x,y) -> p#(y) cond3#(true(),x,y) -> add#(x,y) cond3#(true(),x,y) -> gr#(add(x,y),0()) cond3#(true(),x,y) -> cond1#(gr(add(x,y),0()),x,p(y)) cond3#(false(),x,y) -> add#(x,y) cond3#(false(),x,y) -> gr#(add(x,y),0()) cond3#(false(),x,y) -> cond1#(gr(add(x,y),0()),x,y) gr#(s(x),s(y)) -> gr#(x,y) add#(s(x),y) -> add#(x,y) TRS: cond1(true(),x,y) -> cond2(gr(x,0()),x,y) cond2(true(),x,y) -> cond1(gr(add(x,y),0()),p(x),y) cond2(false(),x,y) -> cond3(gr(y,0()),x,y) cond3(true(),x,y) -> cond1(gr(add(x,y),0()),x,p(y)) cond3(false(),x,y) -> cond1(gr(add(x,y),0()),x,y) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) add(0(),x) -> x add(s(x),y) -> s(add(x,y)) p(0()) -> 0() p(s(x)) -> x graph: cond3#(false(),x,y) -> add#(x,y) -> add#(s(x),y) -> add#(x,y) cond3#(false(),x,y) -> cond1#(gr(add(x,y),0()),x,y) -> cond1#(true(),x,y) -> gr#(x,0()) cond3#(false(),x,y) -> cond1#(gr(add(x,y),0()),x,y) -> cond1#(true(),x,y) -> cond2#(gr(x,0()),x,y) cond3#(true(),x,y) -> add#(x,y) -> add#(s(x),y) -> add#(x,y) cond3#(true(),x,y) -> cond1#(gr(add(x,y),0()),x,p(y)) -> cond1#(true(),x,y) -> gr#(x,0()) cond3#(true(),x,y) -> cond1#(gr(add(x,y),0()),x,p(y)) -> cond1#(true(),x,y) -> cond2#(gr(x,0()),x,y) add#(s(x),y) -> add#(x,y) -> add#(s(x),y) -> add#(x,y) cond2#(false(),x,y) -> cond3#(gr(y,0()),x,y) -> cond3#(true(),x,y) -> p#(y) cond2#(false(),x,y) -> cond3#(gr(y,0()),x,y) -> cond3#(true(),x,y) -> add#(x,y) cond2#(false(),x,y) -> cond3#(gr(y,0()),x,y) -> cond3#(true(),x,y) -> gr#(add(x,y),0()) cond2#(false(),x,y) -> cond3#(gr(y,0()),x,y) -> cond3#(true(),x,y) -> cond1#(gr(add(x,y),0()),x,p(y)) cond2#(false(),x,y) -> cond3#(gr(y,0()),x,y) -> cond3#(false(),x,y) -> add#(x,y) cond2#(false(),x,y) -> cond3#(gr(y,0()),x,y) -> cond3#(false(),x,y) -> gr#(add(x,y),0()) cond2#(false(),x,y) -> cond3#(gr(y,0()),x,y) -> cond3#(false(),x,y) -> cond1#(gr(add(x,y),0()),x,y) cond2#(true(),x,y) -> add#(x,y) -> add#(s(x),y) -> add#(x,y) cond2#(true(),x,y) -> cond1#(gr(add(x,y),0()),p(x),y) -> cond1#(true(),x,y) -> gr#(x,0()) cond2#(true(),x,y) -> cond1#(gr(add(x,y),0()),p(x),y) -> cond1#(true(),x,y) -> cond2#(gr(x,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,0()),x,y) -> cond2#(true(),x,y) -> p#(x) cond1#(true(),x,y) -> cond2#(gr(x,0()),x,y) -> cond2#(true(),x,y) -> add#(x,y) cond1#(true(),x,y) -> cond2#(gr(x,0()),x,y) -> cond2#(true(),x,y) -> gr#(add(x,y),0()) cond1#(true(),x,y) -> cond2#(gr(x,0()),x,y) -> cond2#(true(),x,y) -> cond1#(gr(add(x,y),0()),p(x),y) cond1#(true(),x,y) -> cond2#(gr(x,0()),x,y) -> cond2#(false(),x,y) -> gr#(y,0()) cond1#(true(),x,y) -> cond2#(gr(x,0()),x,y) -> cond2#(false(),x,y) -> cond3#(gr(y,0()),x,y) SCC Processor: #sccs: 3 #rules: 7 #arcs: 24/289 DPs: gr#(s(x),s(y)) -> gr#(x,y) TRS: cond1(true(),x,y) -> cond2(gr(x,0()),x,y) cond2(true(),x,y) -> cond1(gr(add(x,y),0()),p(x),y) cond2(false(),x,y) -> cond3(gr(y,0()),x,y) cond3(true(),x,y) -> cond1(gr(add(x,y),0()),x,p(y)) cond3(false(),x,y) -> cond1(gr(add(x,y),0()),x,y) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) add(0(),x) -> x add(s(x),y) -> s(add(x,y)) p(0()) -> 0() p(s(x)) -> x KBO Processor: argument filtering: pi(true) = [] pi(cond1) = 2 pi(0) = [] pi(gr) = 0 pi(cond2) = 2 pi(add) = [0,1] pi(p) = 0 pi(false) = [] pi(cond3) = 2 pi(s) = [0] pi(gr#) = [0,1] weight function: w0 = 1 w(gr#) = w(s) = w(false) = w(add) = w(cond2) = w(gr) = w(0) = w( true) = 1 w(cond3) = w(p) = w(cond1) = 0 precedence: 0 > add > gr# ~ s ~ cond3 ~ false ~ p ~ cond2 ~ gr ~ cond1 ~ true problem: DPs: TRS: cond1(true(),x,y) -> cond2(gr(x,0()),x,y) cond2(true(),x,y) -> cond1(gr(add(x,y),0()),p(x),y) cond2(false(),x,y) -> cond3(gr(y,0()),x,y) cond3(true(),x,y) -> cond1(gr(add(x,y),0()),x,p(y)) cond3(false(),x,y) -> cond1(gr(add(x,y),0()),x,y) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) add(0(),x) -> x add(s(x),y) -> s(add(x,y)) p(0()) -> 0() p(s(x)) -> x Qed DPs: cond3#(false(),x,y) -> cond1#(gr(add(x,y),0()),x,y) cond1#(true(),x,y) -> cond2#(gr(x,0()),x,y) cond2#(false(),x,y) -> cond3#(gr(y,0()),x,y) cond3#(true(),x,y) -> cond1#(gr(add(x,y),0()),x,p(y)) cond2#(true(),x,y) -> cond1#(gr(add(x,y),0()),p(x),y) TRS: cond1(true(),x,y) -> cond2(gr(x,0()),x,y) cond2(true(),x,y) -> cond1(gr(add(x,y),0()),p(x),y) cond2(false(),x,y) -> cond3(gr(y,0()),x,y) cond3(true(),x,y) -> cond1(gr(add(x,y),0()),x,p(y)) cond3(false(),x,y) -> cond1(gr(add(x,y),0()),x,y) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) add(0(),x) -> x add(s(x),y) -> s(add(x,y)) p(0()) -> 0() p(s(x)) -> x Open DPs: add#(s(x),y) -> add#(x,y) TRS: cond1(true(),x,y) -> cond2(gr(x,0()),x,y) cond2(true(),x,y) -> cond1(gr(add(x,y),0()),p(x),y) cond2(false(),x,y) -> cond3(gr(y,0()),x,y) cond3(true(),x,y) -> cond1(gr(add(x,y),0()),x,p(y)) cond3(false(),x,y) -> cond1(gr(add(x,y),0()),x,y) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) add(0(),x) -> x add(s(x),y) -> s(add(x,y)) p(0()) -> 0() p(s(x)) -> x KBO Processor: argument filtering: pi(true) = [] pi(cond1) = 2 pi(0) = [] pi(gr) = [1] pi(cond2) = 2 pi(add) = [0,1] pi(p) = 0 pi(false) = [] pi(cond3) = 2 pi(s) = [0] pi(add#) = 0 weight function: w0 = 1 w(add#) = w(s) = w(false) = w(p) = w(gr) = w(0) = w(cond1) = w( true) = 1 w(cond3) = w(add) = w(cond2) = 0 precedence: add# ~ add ~ 0 ~ cond1 > s ~ cond3 ~ false ~ p ~ cond2 ~ gr ~ true problem: DPs: TRS: cond1(true(),x,y) -> cond2(gr(x,0()),x,y) cond2(true(),x,y) -> cond1(gr(add(x,y),0()),p(x),y) cond2(false(),x,y) -> cond3(gr(y,0()),x,y) cond3(true(),x,y) -> cond1(gr(add(x,y),0()),x,p(y)) cond3(false(),x,y) -> cond1(gr(add(x,y),0()),x,y) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) add(0(),x) -> x add(s(x),y) -> s(add(x,y)) p(0()) -> 0() p(s(x)) -> x Qed