MAYBE Problem: cond(true(),x,y) -> cond(gr(x,y),y,x) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) Proof: DP Processor: DPs: cond#(true(),x,y) -> gr#(x,y) cond#(true(),x,y) -> cond#(gr(x,y),y,x) gr#(s(x),s(y)) -> gr#(x,y) TRS: cond(true(),x,y) -> cond(gr(x,y),y,x) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) Usable Rule Processor: DPs: cond#(true(),x,y) -> gr#(x,y) cond#(true(),x,y) -> cond#(gr(x,y),y,x) gr#(s(x),s(y)) -> gr#(x,y) TRS: f8(x,y) -> x f8(x,y) -> y gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) ADG Processor: DPs: cond#(true(),x,y) -> gr#(x,y) cond#(true(),x,y) -> cond#(gr(x,y),y,x) gr#(s(x),s(y)) -> gr#(x,y) TRS: f8(x,y) -> x f8(x,y) -> y gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) graph: gr#(s(x),s(y)) -> gr#(x,y) -> gr#(s(x),s(y)) -> gr#(x,y) cond#(true(),x,y) -> gr#(x,y) -> gr#(s(x),s(y)) -> gr#(x,y) cond#(true(),x,y) -> cond#(gr(x,y),y,x) -> cond#(true(),x,y) -> gr#(x,y) cond#(true(),x,y) -> cond#(gr(x,y),y,x) -> cond#(true(),x,y) -> cond#(gr(x,y),y,x) Restore Modifier: DPs: cond#(true(),x,y) -> gr#(x,y) cond#(true(),x,y) -> cond#(gr(x,y),y,x) gr#(s(x),s(y)) -> gr#(x,y) TRS: cond(true(),x,y) -> cond(gr(x,y),y,x) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) SCC Processor: #sccs: 2 #rules: 2 #arcs: 4/9 DPs: cond#(true(),x,y) -> cond#(gr(x,y),y,x) TRS: cond(true(),x,y) -> cond(gr(x,y),y,x) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) Open DPs: gr#(s(x),s(y)) -> gr#(x,y) TRS: cond(true(),x,y) -> cond(gr(x,y),y,x) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) Matrix Interpretation Processor: dimension: 1 interpretation: [gr#](x0, x1) = x0 + x1, [s](x0) = x0 + 1, [false] = 0, [0] = 0, [gr](x0, x1) = 0, [cond](x0, x1, x2) = 0, [true] = 0 orientation: gr#(s(x),s(y)) = x + y + 2 >= x + y = gr#(x,y) cond(true(),x,y) = 0 >= 0 = cond(gr(x,y),y,x) gr(0(),x) = 0 >= 0 = false() gr(s(x),0()) = 0 >= 0 = true() gr(s(x),s(y)) = 0 >= 0 = gr(x,y) problem: DPs: TRS: cond(true(),x,y) -> cond(gr(x,y),y,x) gr(0(),x) -> false() gr(s(x),0()) -> true() gr(s(x),s(y)) -> gr(x,y) Qed