MAYBE Problem: f(x,f(s(s(y)),f(z,w))) -> f(s(x),f(y,f(s(z),w))) L(f(s(s(y)),f(z,w))) -> L(f(s(0()),f(y,f(s(z),w)))) f(x,f(s(s(y)),nil())) -> f(s(x),f(y,f(s(0()),nil()))) Proof: DP Processor: DPs: f#(x,f(s(s(y)),f(z,w))) -> f#(s(z),w) f#(x,f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) f#(x,f(s(s(y)),f(z,w))) -> f#(s(x),f(y,f(s(z),w))) L#(f(s(s(y)),f(z,w))) -> f#(s(z),w) L#(f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) L#(f(s(s(y)),f(z,w))) -> f#(s(0()),f(y,f(s(z),w))) L#(f(s(s(y)),f(z,w))) -> L#(f(s(0()),f(y,f(s(z),w)))) f#(x,f(s(s(y)),nil())) -> f#(s(0()),nil()) f#(x,f(s(s(y)),nil())) -> f#(y,f(s(0()),nil())) f#(x,f(s(s(y)),nil())) -> f#(s(x),f(y,f(s(0()),nil()))) TRS: f(x,f(s(s(y)),f(z,w))) -> f(s(x),f(y,f(s(z),w))) L(f(s(s(y)),f(z,w))) -> L(f(s(0()),f(y,f(s(z),w)))) f(x,f(s(s(y)),nil())) -> f(s(x),f(y,f(s(0()),nil()))) Usable Rule Processor: DPs: f#(x,f(s(s(y)),f(z,w))) -> f#(s(z),w) f#(x,f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) f#(x,f(s(s(y)),f(z,w))) -> f#(s(x),f(y,f(s(z),w))) L#(f(s(s(y)),f(z,w))) -> f#(s(z),w) L#(f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) L#(f(s(s(y)),f(z,w))) -> f#(s(0()),f(y,f(s(z),w))) L#(f(s(s(y)),f(z,w))) -> L#(f(s(0()),f(y,f(s(z),w)))) f#(x,f(s(s(y)),nil())) -> f#(s(0()),nil()) f#(x,f(s(s(y)),nil())) -> f#(y,f(s(0()),nil())) f#(x,f(s(s(y)),nil())) -> f#(s(x),f(y,f(s(0()),nil()))) TRS: f(x,f(s(s(y)),f(z,w))) -> f(s(x),f(y,f(s(z),w))) f(x,f(s(s(y)),nil())) -> f(s(x),f(y,f(s(0()),nil()))) EDG Processor: DPs: f#(x,f(s(s(y)),f(z,w))) -> f#(s(z),w) f#(x,f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) f#(x,f(s(s(y)),f(z,w))) -> f#(s(x),f(y,f(s(z),w))) L#(f(s(s(y)),f(z,w))) -> f#(s(z),w) L#(f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) L#(f(s(s(y)),f(z,w))) -> f#(s(0()),f(y,f(s(z),w))) L#(f(s(s(y)),f(z,w))) -> L#(f(s(0()),f(y,f(s(z),w)))) f#(x,f(s(s(y)),nil())) -> f#(s(0()),nil()) f#(x,f(s(s(y)),nil())) -> f#(y,f(s(0()),nil())) f#(x,f(s(s(y)),nil())) -> f#(s(x),f(y,f(s(0()),nil()))) TRS: f(x,f(s(s(y)),f(z,w))) -> f(s(x),f(y,f(s(z),w))) f(x,f(s(s(y)),nil())) -> f(s(x),f(y,f(s(0()),nil()))) graph: L#(f(s(s(y)),f(z,w))) -> L#(f(s(0()),f(y,f(s(z),w)))) -> L#(f(s(s(y)),f(z,w))) -> f#(s(z),w) L#(f(s(s(y)),f(z,w))) -> L#(f(s(0()),f(y,f(s(z),w)))) -> L#(f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) L#(f(s(s(y)),f(z,w))) -> L#(f(s(0()),f(y,f(s(z),w)))) -> L#(f(s(s(y)),f(z,w))) -> f#(s(0()),f(y,f(s(z),w))) L#(f(s(s(y)),f(z,w))) -> L#(f(s(0()),f(y,f(s(z),w)))) -> L#(f(s(s(y)),f(z,w))) -> L#(f(s(0()),f(y,f(s(z),w)))) L#(f(s(s(y)),f(z,w))) -> f#(s(0()),f(y,f(s(z),w))) -> f#(x,f(s(s(y)),f(z,w))) -> f#(s(z),w) L#(f(s(s(y)),f(z,w))) -> f#(s(0()),f(y,f(s(z),w))) -> f#(x,f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) L#(f(s(s(y)),f(z,w))) -> f#(s(0()),f(y,f(s(z),w))) -> f#(x,f(s(s(y)),f(z,w))) -> f#(s(x),f(y,f(s(z),w))) L#(f(s(s(y)),f(z,w))) -> f#(s(z),w) -> f#(x,f(s(s(y)),f(z,w))) -> f#(s(z),w) L#(f(s(s(y)),f(z,w))) -> f#(s(z),w) -> f#(x,f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) L#(f(s(s(y)),f(z,w))) -> f#(s(z),w) -> f#(x,f(s(s(y)),f(z,w))) -> f#(s(x),f(y,f(s(z),w))) L#(f(s(s(y)),f(z,w))) -> f#(s(z),w) -> f#(x,f(s(s(y)),nil())) -> f#(s(0()),nil()) L#(f(s(s(y)),f(z,w))) -> f#(s(z),w) -> f#(x,f(s(s(y)),nil())) -> f#(y,f(s(0()),nil())) L#(f(s(s(y)),f(z,w))) -> f#(s(z),w) -> f#(x,f(s(s(y)),nil())) -> f#(s(x),f(y,f(s(0()),nil()))) L#(f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) -> f#(x,f(s(s(y)),f(z,w))) -> f#(s(z),w) L#(f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) -> f#(x,f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) L#(f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) -> f#(x,f(s(s(y)),f(z,w))) -> f#(s(x),f(y,f(s(z),w))) L#(f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) -> f#(x,f(s(s(y)),nil())) -> f#(s(0()),nil()) L#(f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) -> f#(x,f(s(s(y)),nil())) -> f#(y,f(s(0()),nil())) L#(f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) -> f#(x,f(s(s(y)),nil())) -> f#(s(x),f(y,f(s(0()),nil()))) f#(x,f(s(s(y)),nil())) -> f#(s(x),f(y,f(s(0()),nil()))) -> f#(x,f(s(s(y)),f(z,w))) -> f#(s(z),w) f#(x,f(s(s(y)),nil())) -> f#(s(x),f(y,f(s(0()),nil()))) -> f#(x,f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) f#(x,f(s(s(y)),nil())) -> f#(s(x),f(y,f(s(0()),nil()))) -> f#(x,f(s(s(y)),f(z,w))) -> f#(s(x),f(y,f(s(z),w))) f#(x,f(s(s(y)),f(z,w))) -> f#(s(z),w) -> f#(x,f(s(s(y)),f(z,w))) -> f#(s(z),w) f#(x,f(s(s(y)),f(z,w))) -> f#(s(z),w) -> f#(x,f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) f#(x,f(s(s(y)),f(z,w))) -> f#(s(z),w) -> f#(x,f(s(s(y)),f(z,w))) -> f#(s(x),f(y,f(s(z),w))) f#(x,f(s(s(y)),f(z,w))) -> f#(s(z),w) -> f#(x,f(s(s(y)),nil())) -> f#(s(0()),nil()) f#(x,f(s(s(y)),f(z,w))) -> f#(s(z),w) -> f#(x,f(s(s(y)),nil())) -> f#(y,f(s(0()),nil())) f#(x,f(s(s(y)),f(z,w))) -> f#(s(z),w) -> f#(x,f(s(s(y)),nil())) -> f#(s(x),f(y,f(s(0()),nil()))) f#(x,f(s(s(y)),f(z,w))) -> f#(s(x),f(y,f(s(z),w))) -> f#(x,f(s(s(y)),f(z,w))) -> f#(s(z),w) f#(x,f(s(s(y)),f(z,w))) -> f#(s(x),f(y,f(s(z),w))) -> f#(x,f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) f#(x,f(s(s(y)),f(z,w))) -> f#(s(x),f(y,f(s(z),w))) -> f#(x,f(s(s(y)),f(z,w))) -> f#(s(x),f(y,f(s(z),w))) f#(x,f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) -> f#(x,f(s(s(y)),f(z,w))) -> f#(s(z),w) f#(x,f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) -> f#(x,f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) f#(x,f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) -> f#(x,f(s(s(y)),f(z,w))) -> f#(s(x),f(y,f(s(z),w))) f#(x,f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) -> f#(x,f(s(s(y)),nil())) -> f#(s(0()),nil()) f#(x,f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) -> f#(x,f(s(s(y)),nil())) -> f#(y,f(s(0()),nil())) f#(x,f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) -> f#(x,f(s(s(y)),nil())) -> f#(s(x),f(y,f(s(0()),nil()))) Restore Modifier: DPs: f#(x,f(s(s(y)),f(z,w))) -> f#(s(z),w) f#(x,f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) f#(x,f(s(s(y)),f(z,w))) -> f#(s(x),f(y,f(s(z),w))) L#(f(s(s(y)),f(z,w))) -> f#(s(z),w) L#(f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) L#(f(s(s(y)),f(z,w))) -> f#(s(0()),f(y,f(s(z),w))) L#(f(s(s(y)),f(z,w))) -> L#(f(s(0()),f(y,f(s(z),w)))) f#(x,f(s(s(y)),nil())) -> f#(s(0()),nil()) f#(x,f(s(s(y)),nil())) -> f#(y,f(s(0()),nil())) f#(x,f(s(s(y)),nil())) -> f#(s(x),f(y,f(s(0()),nil()))) TRS: f(x,f(s(s(y)),f(z,w))) -> f(s(x),f(y,f(s(z),w))) L(f(s(s(y)),f(z,w))) -> L(f(s(0()),f(y,f(s(z),w)))) f(x,f(s(s(y)),nil())) -> f(s(x),f(y,f(s(0()),nil()))) SCC Processor: #sccs: 2 #rules: 5 #arcs: 37/100 DPs: L#(f(s(s(y)),f(z,w))) -> L#(f(s(0()),f(y,f(s(z),w)))) TRS: f(x,f(s(s(y)),f(z,w))) -> f(s(x),f(y,f(s(z),w))) L(f(s(s(y)),f(z,w))) -> L(f(s(0()),f(y,f(s(z),w)))) f(x,f(s(s(y)),nil())) -> f(s(x),f(y,f(s(0()),nil()))) Open DPs: f#(x,f(s(s(y)),f(z,w))) -> f#(s(x),f(y,f(s(z),w))) f#(x,f(s(s(y)),f(z,w))) -> f#(y,f(s(z),w)) f#(x,f(s(s(y)),nil())) -> f#(s(x),f(y,f(s(0()),nil()))) f#(x,f(s(s(y)),f(z,w))) -> f#(s(z),w) TRS: f(x,f(s(s(y)),f(z,w))) -> f(s(x),f(y,f(s(z),w))) L(f(s(s(y)),f(z,w))) -> L(f(s(0()),f(y,f(s(z),w)))) f(x,f(s(s(y)),nil())) -> f(s(x),f(y,f(s(0()),nil()))) Open