YES Problem: h(x,c(y,z)) -> h(c(s(y),x),z) h(c(s(x),c(s(0()),y)),z) -> h(y,c(s(0()),c(x,z))) Proof: DP Processor: DPs: h#(x,c(y,z)) -> h#(c(s(y),x),z) h#(c(s(x),c(s(0()),y)),z) -> h#(y,c(s(0()),c(x,z))) TRS: h(x,c(y,z)) -> h(c(s(y),x),z) h(c(s(x),c(s(0()),y)),z) -> h(y,c(s(0()),c(x,z))) CDG Processor: DPs: h#(x,c(y,z)) -> h#(c(s(y),x),z) h#(c(s(x),c(s(0()),y)),z) -> h#(y,c(s(0()),c(x,z))) TRS: h(x,c(y,z)) -> h(c(s(y),x),z) h(c(s(x),c(s(0()),y)),z) -> h(y,c(s(0()),c(x,z))) graph: h#(c(s(x),c(s(0()),y)),z) -> h#(y,c(s(0()),c(x,z))) -> h#(x,c(y,z)) -> h#(c(s(y),x),z) h#(x,c(y,z)) -> h#(c(s(y),x),z) -> h#(x,c(y,z)) -> h#(c(s(y),x),z) SCC Processor: #sccs: 1 #rules: 1 #arcs: 2/4 DPs: h#(x,c(y,z)) -> h#(c(s(y),x),z) TRS: h(x,c(y,z)) -> h(c(s(y),x),z) h(c(s(x),c(s(0()),y)),z) -> h(y,c(s(0()),c(x,z))) KBO Processor: argument filtering: pi(c) = [1] pi(h) = [] pi(s) = 0 pi(0) = [] pi(h#) = 1 weight function: w0 = 1 w(h#) = w(0) = w(s) = w(h) = w(c) = 1 precedence: h# ~ 0 ~ s ~ h ~ c problem: DPs: TRS: h(x,c(y,z)) -> h(c(s(y),x),z) h(c(s(x),c(s(0()),y)),z) -> h(y,c(s(0()),c(x,z))) Qed