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()))) TDG 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()))) 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))) -> 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))) 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(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)),nil())) -> f#(s(x),f(y,f(s(0()),nil()))) L#(f(s(s(y)),f(z,w))) -> f#(s(0()),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#(s(0()),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#(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(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(z),w) 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#(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(0()),nil()) 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)),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(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(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)),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(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(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)),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(z),w) f#(x,f(s(s(y)),nil())) -> 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)),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(0()),nil()) -> f#(x,f(s(s(y)),nil())) -> f#(s(0()),nil()) f#(x,f(s(s(y)),nil())) -> 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)),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#(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)),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)),nil())) -> 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)),nil())) -> 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(x),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#(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) 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()))) f#(x,f(s(s(y)),nil())) -> f#(y,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#(y,f(s(0()),nil())) -> 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)),f(z,w))) -> f#(s(x),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#(y,f(s(0()),nil())) -> 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)),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#(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(0()),nil()) 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)),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(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)),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)),nil())) -> 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)),nil())) -> 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(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(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#(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#(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(0()),nil()) 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)),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(z),w) SCC Processor: #sccs: 2 #rules: 7 #arcs: 58/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(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)),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()))) 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))) 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()))) graph: 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()))) SCC Processor: #sccs: 1 #rules: 4 #arcs: 18/36 DPs: 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#(y,f(s(z),w)) 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()))) Matrix Interpretation Processor: dim=1 interpretation: [f#](x0, x1) = x0 + 2x1, [nil] = 3/2, [0] = 0, [L](x0) = 0, [f](x0, x1) = 1/2x0 + x1, [s](x0) = x0 + 1 orientation: f#(x,f(s(s(y)),nil())) = x + y + 5 >= x + y + 5 = f#(s(x),f(y,f(s(0()),nil()))) f#(x,f(s(s(y)),f(z,w))) = 2w + x + y + z + 2 >= 2w + x + y + z + 2 = f#(s(x),f(y,f(s(z),w))) f#(x,f(s(s(y)),f(z,w))) = 2w + x + y + z + 2 >= 2w + y + z + 1 = f#(y,f(s(z),w)) f#(x,f(s(s(y)),f(z,w))) = 2w + x + y + z + 2 >= 2w + z + 1 = f#(s(z),w) f(x,f(s(s(y)),f(z,w))) = w + 1/2x + 1/2y + 1/2z + 1 >= w + 1/2x + 1/2y + 1/2z + 1 = f(s(x),f(y,f(s(z),w))) L(f(s(s(y)),f(z,w))) = 0 >= 0 = L(f(s(0()),f(y,f(s(z),w)))) f(x,f(s(s(y)),nil())) = 1/2x + 1/2y + 5/2 >= 1/2x + 1/2y + 5/2 = f(s(x),f(y,f(s(0()),nil()))) problem: DPs: 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))) 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: 1 #rules: 1 #arcs: 14/4 DPs: f#(x,f(s(s(y)),f(z,w))) -> f#(s(x),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()))) Matrix Interpretation Processor: dim=1 interpretation: [f#](x0, x1) = x0 + x1 + 6, [nil] = 1, [0] = 0, [L](x0) = 0, [f](x0, x1) = 2x0 + x1, [s](x0) = x0 + 2 orientation: f#(x,f(s(s(y)),f(z,w))) = w + x + 2y + 2z + 14 >= w + x + 2y + 2z + 12 = f#(s(x),f(y,f(s(z),w))) f(x,f(s(s(y)),f(z,w))) = w + 2x + 2y + 2z + 8 >= w + 2x + 2y + 2z + 8 = f(s(x),f(y,f(s(z),w))) L(f(s(s(y)),f(z,w))) = 0 >= 0 = L(f(s(0()),f(y,f(s(z),w)))) f(x,f(s(s(y)),nil())) = 2x + 2y + 9 >= 2x + 2y + 9 = f(s(x),f(y,f(s(0()),nil()))) problem: DPs: 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()))) Qed