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))))) 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))))) 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))))) 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