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) = x1, [nil] = 1, [0] = 0, [L](x0) = 6, [f](x0, x1) = x0 + x1, [s](x0) = x0 + 1 orientation: f#(x,f(s(s(y)),nil())) = y + 3 >= y + 2 = f#(s(x),f(y,f(s(0()),nil()))) f#(x,f(s(s(y)),f(z,w))) = w + y + z + 2 >= w + y + z + 1 = f#(s(x),f(y,f(s(z),w))) f#(x,f(s(s(y)),f(z,w))) = w + y + z + 2 >= w + z + 1 = f#(y,f(s(z),w)) f#(x,f(s(s(y)),f(z,w))) = w + y + z + 2 >= w = f#(s(z),w) f(x,f(s(s(y)),f(z,w))) = w + x + y + z + 2 >= w + x + y + z + 2 = f(s(x),f(y,f(s(z),w))) L(f(s(s(y)),f(z,w))) = 6 >= 6 = L(f(s(0()),f(y,f(s(z),w)))) f(x,f(s(s(y)),nil())) = x + y + 3 >= x + y + 3 = 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