YES Problem: h(c(x,y),c(s(z),z),t(w)) -> h(z,c(y,x),t(t(c(x,c(y,t(w)))))) h(x,c(y,z),t(w)) -> h(c(s(y),x),z,t(c(t(w),w))) h(c(s(x),c(s(0()),y)),z,t(x)) -> h(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) t(t(x)) -> t(c(t(x),x)) t(x) -> x t(x) -> c(0(),c(0(),c(0(),c(0(),c(0(),x))))) Proof: DP Processor: DPs: h#(c(x,y),c(s(z),z),t(w)) -> t#(c(x,c(y,t(w)))) h#(c(x,y),c(s(z),z),t(w)) -> t#(t(c(x,c(y,t(w))))) h#(c(x,y),c(s(z),z),t(w)) -> h#(z,c(y,x),t(t(c(x,c(y,t(w)))))) h#(x,c(y,z),t(w)) -> t#(c(t(w),w)) h#(x,c(y,z),t(w)) -> h#(c(s(y),x),z,t(c(t(w),w))) h#(c(s(x),c(s(0()),y)),z,t(x)) -> t#(c(x,s(x))) h#(c(s(x),c(s(0()),y)),z,t(x)) -> t#(t(c(x,s(x)))) h#(c(s(x),c(s(0()),y)),z,t(x)) -> h#(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) t#(t(x)) -> t#(c(t(x),x)) TRS: h(c(x,y),c(s(z),z),t(w)) -> h(z,c(y,x),t(t(c(x,c(y,t(w)))))) h(x,c(y,z),t(w)) -> h(c(s(y),x),z,t(c(t(w),w))) h(c(s(x),c(s(0()),y)),z,t(x)) -> h(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) t(t(x)) -> t(c(t(x),x)) t(x) -> x t(x) -> c(0(),c(0(),c(0(),c(0(),c(0(),x))))) TDG Processor: DPs: h#(c(x,y),c(s(z),z),t(w)) -> t#(c(x,c(y,t(w)))) h#(c(x,y),c(s(z),z),t(w)) -> t#(t(c(x,c(y,t(w))))) h#(c(x,y),c(s(z),z),t(w)) -> h#(z,c(y,x),t(t(c(x,c(y,t(w)))))) h#(x,c(y,z),t(w)) -> t#(c(t(w),w)) h#(x,c(y,z),t(w)) -> h#(c(s(y),x),z,t(c(t(w),w))) h#(c(s(x),c(s(0()),y)),z,t(x)) -> t#(c(x,s(x))) h#(c(s(x),c(s(0()),y)),z,t(x)) -> t#(t(c(x,s(x)))) h#(c(s(x),c(s(0()),y)),z,t(x)) -> h#(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) t#(t(x)) -> t#(c(t(x),x)) TRS: h(c(x,y),c(s(z),z),t(w)) -> h(z,c(y,x),t(t(c(x,c(y,t(w)))))) h(x,c(y,z),t(w)) -> h(c(s(y),x),z,t(c(t(w),w))) h(c(s(x),c(s(0()),y)),z,t(x)) -> h(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) t(t(x)) -> t(c(t(x),x)) t(x) -> x t(x) -> c(0(),c(0(),c(0(),c(0(),c(0(),x))))) graph: t#(t(x)) -> t#(c(t(x),x)) -> t#(t(x)) -> t#(c(t(x),x)) h#(c(s(x),c(s(0()),y)),z,t(x)) -> t#(t(c(x,s(x)))) -> t#(t(x)) -> t#(c(t(x),x)) h#(c(s(x),c(s(0()),y)),z,t(x)) -> t#(c(x,s(x))) -> t#(t(x)) -> t#(c(t(x),x)) h#(c(s(x),c(s(0()),y)),z,t(x)) -> h#(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) -> h#(c(s(x),c(s(0()),y)),z,t(x)) -> h#(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) h#(c(s(x),c(s(0()),y)),z,t(x)) -> h#(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) -> h#(c(s(x),c(s(0()),y)),z,t(x)) -> t#(t(c(x,s(x)))) h#(c(s(x),c(s(0()),y)),z,t(x)) -> h#(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) -> h#(c(s(x),c(s(0()),y)),z,t(x)) -> t#(c(x,s(x))) h#(c(s(x),c(s(0()),y)),z,t(x)) -> h#(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) -> h#(x,c(y,z),t(w)) -> h#(c(s(y),x),z,t(c(t(w),w))) h#(c(s(x),c(s(0()),y)),z,t(x)) -> h#(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) -> h#(x,c(y,z),t(w)) -> t#(c(t(w),w)) h#(c(s(x),c(s(0()),y)),z,t(x)) -> h#(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) -> h#(c(x,y),c(s(z),z),t(w)) -> h#(z,c(y,x),t(t(c(x,c(y,t(w)))))) h#(c(s(x),c(s(0()),y)),z,t(x)) -> h#(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) -> h#(c(x,y),c(s(z),z),t(w)) -> t#(t(c(x,c(y,t(w))))) h#(c(s(x),c(s(0()),y)),z,t(x)) -> h#(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) -> h#(c(x,y),c(s(z),z),t(w)) -> t#(c(x,c(y,t(w)))) h#(c(x,y),c(s(z),z),t(w)) -> t#(t(c(x,c(y,t(w))))) -> t#(t(x)) -> t#(c(t(x),x)) h#(c(x,y),c(s(z),z),t(w)) -> t#(c(x,c(y,t(w)))) -> t#(t(x)) -> t#(c(t(x),x)) h#(c(x,y),c(s(z),z),t(w)) -> h#(z,c(y,x),t(t(c(x,c(y,t(w)))))) -> h#(c(s(x),c(s(0()),y)),z,t(x)) -> h#(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) h#(c(x,y),c(s(z),z),t(w)) -> h#(z,c(y,x),t(t(c(x,c(y,t(w)))))) -> h#(c(s(x),c(s(0()),y)),z,t(x)) -> t#(t(c(x,s(x)))) h#(c(x,y),c(s(z),z),t(w)) -> h#(z,c(y,x),t(t(c(x,c(y,t(w)))))) -> h#(c(s(x),c(s(0()),y)),z,t(x)) -> t#(c(x,s(x))) h#(c(x,y),c(s(z),z),t(w)) -> h#(z,c(y,x),t(t(c(x,c(y,t(w)))))) -> h#(x,c(y,z),t(w)) -> h#(c(s(y),x),z,t(c(t(w),w))) h#(c(x,y),c(s(z),z),t(w)) -> h#(z,c(y,x),t(t(c(x,c(y,t(w)))))) -> h#(x,c(y,z),t(w)) -> t#(c(t(w),w)) h#(c(x,y),c(s(z),z),t(w)) -> h#(z,c(y,x),t(t(c(x,c(y,t(w)))))) -> h#(c(x,y),c(s(z),z),t(w)) -> h#(z,c(y,x),t(t(c(x,c(y,t(w)))))) h#(c(x,y),c(s(z),z),t(w)) -> h#(z,c(y,x),t(t(c(x,c(y,t(w)))))) -> h#(c(x,y),c(s(z),z),t(w)) -> t#(t(c(x,c(y,t(w))))) h#(c(x,y),c(s(z),z),t(w)) -> h#(z,c(y,x),t(t(c(x,c(y,t(w)))))) -> h#(c(x,y),c(s(z),z),t(w)) -> t#(c(x,c(y,t(w)))) h#(x,c(y,z),t(w)) -> t#(c(t(w),w)) -> t#(t(x)) -> t#(c(t(x),x)) h#(x,c(y,z),t(w)) -> h#(c(s(y),x),z,t(c(t(w),w))) -> h#(c(s(x),c(s(0()),y)),z,t(x)) -> h#(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) h#(x,c(y,z),t(w)) -> h#(c(s(y),x),z,t(c(t(w),w))) -> h#(c(s(x),c(s(0()),y)),z,t(x)) -> t#(t(c(x,s(x)))) h#(x,c(y,z),t(w)) -> h#(c(s(y),x),z,t(c(t(w),w))) -> h#(c(s(x),c(s(0()),y)),z,t(x)) -> t#(c(x,s(x))) h#(x,c(y,z),t(w)) -> h#(c(s(y),x),z,t(c(t(w),w))) -> h#(x,c(y,z),t(w)) -> h#(c(s(y),x),z,t(c(t(w),w))) h#(x,c(y,z),t(w)) -> h#(c(s(y),x),z,t(c(t(w),w))) -> h#(x,c(y,z),t(w)) -> t#(c(t(w),w)) h#(x,c(y,z),t(w)) -> h#(c(s(y),x),z,t(c(t(w),w))) -> h#(c(x,y),c(s(z),z),t(w)) -> h#(z,c(y,x),t(t(c(x,c(y,t(w)))))) h#(x,c(y,z),t(w)) -> h#(c(s(y),x),z,t(c(t(w),w))) -> h#(c(x,y),c(s(z),z),t(w)) -> t#(t(c(x,c(y,t(w))))) h#(x,c(y,z),t(w)) -> h#(c(s(y),x),z,t(c(t(w),w))) -> h#(c(x,y),c(s(z),z),t(w)) -> t#(c(x,c(y,t(w)))) SCC Processor: #sccs: 2 #rules: 4 #arcs: 30/81 DPs: h#(c(s(x),c(s(0()),y)),z,t(x)) -> h#(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) h#(c(x,y),c(s(z),z),t(w)) -> h#(z,c(y,x),t(t(c(x,c(y,t(w)))))) h#(x,c(y,z),t(w)) -> h#(c(s(y),x),z,t(c(t(w),w))) TRS: h(c(x,y),c(s(z),z),t(w)) -> h(z,c(y,x),t(t(c(x,c(y,t(w)))))) h(x,c(y,z),t(w)) -> h(c(s(y),x),z,t(c(t(w),w))) h(c(s(x),c(s(0()),y)),z,t(x)) -> h(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) t(t(x)) -> t(c(t(x),x)) t(x) -> x t(x) -> c(0(),c(0(),c(0(),c(0(),c(0(),x))))) EDG Processor: DPs: h#(c(s(x),c(s(0()),y)),z,t(x)) -> h#(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) h#(c(x,y),c(s(z),z),t(w)) -> h#(z,c(y,x),t(t(c(x,c(y,t(w)))))) h#(x,c(y,z),t(w)) -> h#(c(s(y),x),z,t(c(t(w),w))) TRS: h(c(x,y),c(s(z),z),t(w)) -> h(z,c(y,x),t(t(c(x,c(y,t(w)))))) h(x,c(y,z),t(w)) -> h(c(s(y),x),z,t(c(t(w),w))) h(c(s(x),c(s(0()),y)),z,t(x)) -> h(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) t(t(x)) -> t(c(t(x),x)) t(x) -> x t(x) -> c(0(),c(0(),c(0(),c(0(),c(0(),x))))) graph: h#(c(s(x),c(s(0()),y)),z,t(x)) -> h#(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) -> h#(x,c(y,z),t(w)) -> h#(c(s(y),x),z,t(c(t(w),w))) h#(c(s(x),c(s(0()),y)),z,t(x)) -> h#(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) -> h#(c(s(x),c(s(0()),y)),z,t(x)) -> h#(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) h#(c(x,y),c(s(z),z),t(w)) -> h#(z,c(y,x),t(t(c(x,c(y,t(w)))))) -> h#(c(x,y),c(s(z),z),t(w)) -> h#(z,c(y,x),t(t(c(x,c(y,t(w)))))) h#(c(x,y),c(s(z),z),t(w)) -> h#(z,c(y,x),t(t(c(x,c(y,t(w)))))) -> h#(x,c(y,z),t(w)) -> h#(c(s(y),x),z,t(c(t(w),w))) h#(c(x,y),c(s(z),z),t(w)) -> h#(z,c(y,x),t(t(c(x,c(y,t(w)))))) -> h#(c(s(x),c(s(0()),y)),z,t(x)) -> h#(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) h#(x,c(y,z),t(w)) -> h#(c(s(y),x),z,t(c(t(w),w))) -> h#(c(x,y),c(s(z),z),t(w)) -> h#(z,c(y,x),t(t(c(x,c(y,t(w)))))) h#(x,c(y,z),t(w)) -> h#(c(s(y),x),z,t(c(t(w),w))) -> h#(x,c(y,z),t(w)) -> h#(c(s(y),x),z,t(c(t(w),w))) h#(x,c(y,z),t(w)) -> h#(c(s(y),x),z,t(c(t(w),w))) -> h#(c(s(x),c(s(0()),y)),z,t(x)) -> h#(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) Usable Rule Processor: DPs: h#(c(s(x),c(s(0()),y)),z,t(x)) -> h#(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) h#(c(x,y),c(s(z),z),t(w)) -> h#(z,c(y,x),t(t(c(x,c(y,t(w)))))) h#(x,c(y,z),t(w)) -> h#(c(s(y),x),z,t(c(t(w),w))) TRS: t(x) -> x t(x) -> c(0(),c(0(),c(0(),c(0(),c(0(),x))))) t(t(x)) -> t(c(t(x),x)) Matrix Interpretation Processor: dim=1 usable rules: interpretation: [h#](x0, x1, x2) = 4x0 + 4x1 + 1, [0] = 0, [t](x0) = 2x0, [s](x0) = x0, [c](x0, x1) = x0 + x1 + 2 orientation: h#(c(s(x),c(s(0()),y)),z,t(x)) = 4x + 4y + 4z + 17 >= 4x + 4y + 4z + 17 = h#(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) h#(c(x,y),c(s(z),z),t(w)) = 4x + 4y + 8z + 17 >= 4x + 4y + 4z + 9 = h#(z,c(y,x),t(t(c(x,c(y,t(w)))))) h#(x,c(y,z),t(w)) = 4x + 4y + 4z + 9 >= 4x + 4y + 4z + 9 = h#(c(s(y),x),z,t(c(t(w),w))) t(x) = 2x >= x = x t(x) = 2x >= x + 10 = c(0(),c(0(),c(0(),c(0(),c(0(),x))))) t(t(x)) = 4x >= 6x + 4 = t(c(t(x),x)) problem: DPs: h#(c(s(x),c(s(0()),y)),z,t(x)) -> h#(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) h#(x,c(y,z),t(w)) -> h#(c(s(y),x),z,t(c(t(w),w))) TRS: t(x) -> x t(x) -> c(0(),c(0(),c(0(),c(0(),c(0(),x))))) t(t(x)) -> t(c(t(x),x)) Restore Modifier: DPs: h#(c(s(x),c(s(0()),y)),z,t(x)) -> h#(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) h#(x,c(y,z),t(w)) -> h#(c(s(y),x),z,t(c(t(w),w))) TRS: h(c(x,y),c(s(z),z),t(w)) -> h(z,c(y,x),t(t(c(x,c(y,t(w)))))) h(x,c(y,z),t(w)) -> h(c(s(y),x),z,t(c(t(w),w))) h(c(s(x),c(s(0()),y)),z,t(x)) -> h(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) t(t(x)) -> t(c(t(x),x)) t(x) -> x t(x) -> c(0(),c(0(),c(0(),c(0(),c(0(),x))))) Usable Rule Processor: DPs: h#(c(s(x),c(s(0()),y)),z,t(x)) -> h#(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) h#(x,c(y,z),t(w)) -> h#(c(s(y),x),z,t(c(t(w),w))) TRS: t(x) -> x t(x) -> c(0(),c(0(),c(0(),c(0(),c(0(),x))))) t(t(x)) -> t(c(t(x),x)) Matrix Interpretation Processor: dim=1 usable rules: interpretation: [h#](x0, x1, x2) = 2x0 + x1, [0] = 1, [t](x0) = 1/2, [s](x0) = 1/2x0, [c](x0, x1) = x0 + x1 orientation: h#(c(s(x),c(s(0()),y)),z,t(x)) = x + 2y + z + 1 >= x + 2y + z + 1/2 = h#(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) h#(x,c(y,z),t(w)) = 2x + y + z >= 2x + y + z = h#(c(s(y),x),z,t(c(t(w),w))) t(x) = 1/2 >= x = x t(x) = 1/2 >= x + 5 = c(0(),c(0(),c(0(),c(0(),c(0(),x))))) t(t(x)) = 1/2 >= 1/2 = t(c(t(x),x)) problem: DPs: h#(x,c(y,z),t(w)) -> h#(c(s(y),x),z,t(c(t(w),w))) TRS: t(x) -> x t(x) -> c(0(),c(0(),c(0(),c(0(),c(0(),x))))) t(t(x)) -> t(c(t(x),x)) Restore Modifier: DPs: h#(x,c(y,z),t(w)) -> h#(c(s(y),x),z,t(c(t(w),w))) TRS: h(c(x,y),c(s(z),z),t(w)) -> h(z,c(y,x),t(t(c(x,c(y,t(w)))))) h(x,c(y,z),t(w)) -> h(c(s(y),x),z,t(c(t(w),w))) h(c(s(x),c(s(0()),y)),z,t(x)) -> h(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) t(t(x)) -> t(c(t(x),x)) t(x) -> x t(x) -> c(0(),c(0(),c(0(),c(0(),c(0(),x))))) Subterm Criterion Processor: simple projection: pi(h#) = 1 problem: DPs: TRS: h(c(x,y),c(s(z),z),t(w)) -> h(z,c(y,x),t(t(c(x,c(y,t(w)))))) h(x,c(y,z),t(w)) -> h(c(s(y),x),z,t(c(t(w),w))) h(c(s(x),c(s(0()),y)),z,t(x)) -> h(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) t(t(x)) -> t(c(t(x),x)) t(x) -> x t(x) -> c(0(),c(0(),c(0(),c(0(),c(0(),x))))) Qed DPs: t#(t(x)) -> t#(c(t(x),x)) TRS: h(c(x,y),c(s(z),z),t(w)) -> h(z,c(y,x),t(t(c(x,c(y,t(w)))))) h(x,c(y,z),t(w)) -> h(c(s(y),x),z,t(c(t(w),w))) h(c(s(x),c(s(0()),y)),z,t(x)) -> h(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) t(t(x)) -> t(c(t(x),x)) t(x) -> x t(x) -> c(0(),c(0(),c(0(),c(0(),c(0(),x))))) EDG Processor: DPs: t#(t(x)) -> t#(c(t(x),x)) TRS: h(c(x,y),c(s(z),z),t(w)) -> h(z,c(y,x),t(t(c(x,c(y,t(w)))))) h(x,c(y,z),t(w)) -> h(c(s(y),x),z,t(c(t(w),w))) h(c(s(x),c(s(0()),y)),z,t(x)) -> h(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) t(t(x)) -> t(c(t(x),x)) t(x) -> x t(x) -> c(0(),c(0(),c(0(),c(0(),c(0(),x))))) graph: Qed