MAYBE 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))))) Usable Rule 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: f7(x,y) -> x f7(x,y) -> y 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: f7(x,y) -> x f7(x,y) -> y 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)))) Restore Modifier: 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))))) 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))))) Open 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))))) Matrix Interpretation Processor: dimension: 1 interpretation: [t#](x0) = x0, [0] = 0, [h](x0, x1, x2) = 0, [t](x0) = x0 + 1, [s](x0) = 0, [c](x0, x1) = 0 orientation: t#(t(x)) = x + 1 >= 0 = t#(c(t(x),x)) h(c(x,y),c(s(z),z),t(w)) = 0 >= 0 = h(z,c(y,x),t(t(c(x,c(y,t(w)))))) h(x,c(y,z),t(w)) = 0 >= 0 = h(c(s(y),x),z,t(c(t(w),w))) h(c(s(x),c(s(0()),y)),z,t(x)) = 0 >= 0 = h(y,c(s(0()),c(x,z)),t(t(c(x,s(x))))) t(t(x)) = x + 2 >= 1 = t(c(t(x),x)) t(x) = x + 1 >= x = x t(x) = x + 1 >= 0 = c(0(),c(0(),c(0(),c(0(),c(0(),x))))) 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