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