YES Problem: op(i(x),op(y,z)) -> op(f(x,i(x)),op(i(i(y)),z)) op(i(x),op(y,op(z,w))) -> op(f(x,i(x)),op(z,op(y,w))) i(x) -> x f(x,y) -> x Proof: DP Processor: DPs: op#(i(x),op(y,z)) -> i#(y) op#(i(x),op(y,z)) -> i#(i(y)) op#(i(x),op(y,z)) -> op#(i(i(y)),z) op#(i(x),op(y,z)) -> f#(x,i(x)) op#(i(x),op(y,z)) -> op#(f(x,i(x)),op(i(i(y)),z)) op#(i(x),op(y,op(z,w))) -> op#(y,w) op#(i(x),op(y,op(z,w))) -> op#(z,op(y,w)) op#(i(x),op(y,op(z,w))) -> f#(x,i(x)) op#(i(x),op(y,op(z,w))) -> op#(f(x,i(x)),op(z,op(y,w))) TRS: op(i(x),op(y,z)) -> op(f(x,i(x)),op(i(i(y)),z)) op(i(x),op(y,op(z,w))) -> op(f(x,i(x)),op(z,op(y,w))) i(x) -> x f(x,y) -> x TDG Processor: DPs: op#(i(x),op(y,z)) -> i#(y) op#(i(x),op(y,z)) -> i#(i(y)) op#(i(x),op(y,z)) -> op#(i(i(y)),z) op#(i(x),op(y,z)) -> f#(x,i(x)) op#(i(x),op(y,z)) -> op#(f(x,i(x)),op(i(i(y)),z)) op#(i(x),op(y,op(z,w))) -> op#(y,w) op#(i(x),op(y,op(z,w))) -> op#(z,op(y,w)) op#(i(x),op(y,op(z,w))) -> f#(x,i(x)) op#(i(x),op(y,op(z,w))) -> op#(f(x,i(x)),op(z,op(y,w))) TRS: op(i(x),op(y,z)) -> op(f(x,i(x)),op(i(i(y)),z)) op(i(x),op(y,op(z,w))) -> op(f(x,i(x)),op(z,op(y,w))) i(x) -> x f(x,y) -> x graph: op#(i(x),op(y,op(z,w))) -> op#(f(x,i(x)),op(z,op(y,w))) -> op#(i(x),op(y,op(z,w))) -> op#(f(x,i(x)),op(z,op(y,w))) op#(i(x),op(y,op(z,w))) -> op#(f(x,i(x)),op(z,op(y,w))) -> op#(i(x),op(y,op(z,w))) -> f#(x,i(x)) op#(i(x),op(y,op(z,w))) -> op#(f(x,i(x)),op(z,op(y,w))) -> op#(i(x),op(y,op(z,w))) -> op#(z,op(y,w)) op#(i(x),op(y,op(z,w))) -> op#(f(x,i(x)),op(z,op(y,w))) -> op#(i(x),op(y,op(z,w))) -> op#(y,w) op#(i(x),op(y,op(z,w))) -> op#(f(x,i(x)),op(z,op(y,w))) -> op#(i(x),op(y,z)) -> op#(f(x,i(x)),op(i(i(y)),z)) op#(i(x),op(y,op(z,w))) -> op#(f(x,i(x)),op(z,op(y,w))) -> op#(i(x),op(y,z)) -> f#(x,i(x)) op#(i(x),op(y,op(z,w))) -> op#(f(x,i(x)),op(z,op(y,w))) -> op#(i(x),op(y,z)) -> op#(i(i(y)),z) op#(i(x),op(y,op(z,w))) -> op#(f(x,i(x)),op(z,op(y,w))) -> op#(i(x),op(y,z)) -> i#(i(y)) op#(i(x),op(y,op(z,w))) -> op#(f(x,i(x)),op(z,op(y,w))) -> op#(i(x),op(y,z)) -> i#(y) op#(i(x),op(y,op(z,w))) -> op#(z,op(y,w)) -> op#(i(x),op(y,op(z,w))) -> op#(f(x,i(x)),op(z,op(y,w))) op#(i(x),op(y,op(z,w))) -> op#(z,op(y,w)) -> op#(i(x),op(y,op(z,w))) -> f#(x,i(x)) op#(i(x),op(y,op(z,w))) -> op#(z,op(y,w)) -> op#(i(x),op(y,op(z,w))) -> op#(z,op(y,w)) op#(i(x),op(y,op(z,w))) -> op#(z,op(y,w)) -> op#(i(x),op(y,op(z,w))) -> op#(y,w) op#(i(x),op(y,op(z,w))) -> op#(z,op(y,w)) -> op#(i(x),op(y,z)) -> op#(f(x,i(x)),op(i(i(y)),z)) op#(i(x),op(y,op(z,w))) -> op#(z,op(y,w)) -> op#(i(x),op(y,z)) -> f#(x,i(x)) op#(i(x),op(y,op(z,w))) -> op#(z,op(y,w)) -> op#(i(x),op(y,z)) -> op#(i(i(y)),z) op#(i(x),op(y,op(z,w))) -> op#(z,op(y,w)) -> op#(i(x),op(y,z)) -> i#(i(y)) op#(i(x),op(y,op(z,w))) -> op#(z,op(y,w)) -> op#(i(x),op(y,z)) -> i#(y) op#(i(x),op(y,op(z,w))) -> op#(y,w) -> op#(i(x),op(y,op(z,w))) -> op#(f(x,i(x)),op(z,op(y,w))) op#(i(x),op(y,op(z,w))) -> op#(y,w) -> op#(i(x),op(y,op(z,w))) -> f#(x,i(x)) op#(i(x),op(y,op(z,w))) -> op#(y,w) -> op#(i(x),op(y,op(z,w))) -> op#(z,op(y,w)) op#(i(x),op(y,op(z,w))) -> op#(y,w) -> op#(i(x),op(y,op(z,w))) -> op#(y,w) op#(i(x),op(y,op(z,w))) -> op#(y,w) -> op#(i(x),op(y,z)) -> op#(f(x,i(x)),op(i(i(y)),z)) op#(i(x),op(y,op(z,w))) -> op#(y,w) -> op#(i(x),op(y,z)) -> f#(x,i(x)) op#(i(x),op(y,op(z,w))) -> op#(y,w) -> op#(i(x),op(y,z)) -> op#(i(i(y)),z) op#(i(x),op(y,op(z,w))) -> op#(y,w) -> op#(i(x),op(y,z)) -> i#(i(y)) op#(i(x),op(y,op(z,w))) -> op#(y,w) -> op#(i(x),op(y,z)) -> i#(y) op#(i(x),op(y,z)) -> op#(f(x,i(x)),op(i(i(y)),z)) -> op#(i(x),op(y,op(z,w))) -> op#(f(x,i(x)),op(z,op(y,w))) op#(i(x),op(y,z)) -> op#(f(x,i(x)),op(i(i(y)),z)) -> op#(i(x),op(y,op(z,w))) -> f#(x,i(x)) op#(i(x),op(y,z)) -> op#(f(x,i(x)),op(i(i(y)),z)) -> op#(i(x),op(y,op(z,w))) -> op#(z,op(y,w)) op#(i(x),op(y,z)) -> op#(f(x,i(x)),op(i(i(y)),z)) -> op#(i(x),op(y,op(z,w))) -> op#(y,w) op#(i(x),op(y,z)) -> op#(f(x,i(x)),op(i(i(y)),z)) -> op#(i(x),op(y,z)) -> op#(f(x,i(x)),op(i(i(y)),z)) op#(i(x),op(y,z)) -> op#(f(x,i(x)),op(i(i(y)),z)) -> op#(i(x),op(y,z)) -> f#(x,i(x)) op#(i(x),op(y,z)) -> op#(f(x,i(x)),op(i(i(y)),z)) -> op#(i(x),op(y,z)) -> op#(i(i(y)),z) op#(i(x),op(y,z)) -> op#(f(x,i(x)),op(i(i(y)),z)) -> op#(i(x),op(y,z)) -> i#(i(y)) op#(i(x),op(y,z)) -> op#(f(x,i(x)),op(i(i(y)),z)) -> op#(i(x),op(y,z)) -> i#(y) op#(i(x),op(y,z)) -> op#(i(i(y)),z) -> op#(i(x),op(y,op(z,w))) -> op#(f(x,i(x)),op(z,op(y,w))) op#(i(x),op(y,z)) -> op#(i(i(y)),z) -> op#(i(x),op(y,op(z,w))) -> f#(x,i(x)) op#(i(x),op(y,z)) -> op#(i(i(y)),z) -> op#(i(x),op(y,op(z,w))) -> op#(z,op(y,w)) op#(i(x),op(y,z)) -> op#(i(i(y)),z) -> op#(i(x),op(y,op(z,w))) -> op#(y,w) op#(i(x),op(y,z)) -> op#(i(i(y)),z) -> op#(i(x),op(y,z)) -> op#(f(x,i(x)),op(i(i(y)),z)) op#(i(x),op(y,z)) -> op#(i(i(y)),z) -> op#(i(x),op(y,z)) -> f#(x,i(x)) op#(i(x),op(y,z)) -> op#(i(i(y)),z) -> op#(i(x),op(y,z)) -> op#(i(i(y)),z) op#(i(x),op(y,z)) -> op#(i(i(y)),z) -> op#(i(x),op(y,z)) -> i#(i(y)) op#(i(x),op(y,z)) -> op#(i(i(y)),z) -> op#(i(x),op(y,z)) -> i#(y) SCC Processor: #sccs: 1 #rules: 5 #arcs: 45/81 DPs: op#(i(x),op(y,op(z,w))) -> op#(f(x,i(x)),op(z,op(y,w))) op#(i(x),op(y,z)) -> op#(i(i(y)),z) op#(i(x),op(y,z)) -> op#(f(x,i(x)),op(i(i(y)),z)) op#(i(x),op(y,op(z,w))) -> op#(y,w) op#(i(x),op(y,op(z,w))) -> op#(z,op(y,w)) TRS: op(i(x),op(y,z)) -> op(f(x,i(x)),op(i(i(y)),z)) op(i(x),op(y,op(z,w))) -> op(f(x,i(x)),op(z,op(y,w))) i(x) -> x f(x,y) -> x Arctic Interpretation Processor: dimension: 1 usable rules: op(i(x),op(y,z)) -> op(f(x,i(x)),op(i(i(y)),z)) op(i(x),op(y,op(z,w))) -> op(f(x,i(x)),op(z,op(y,w))) interpretation: [op#](x0, x1) = x1, [f](x0, x1) = 1x1 + 1, [op](x0, x1) = 1x1, [i](x0) = x0 + 4 orientation: op#(i(x),op(y,op(z,w))) = 2w >= 2w = op#(f(x,i(x)),op(z,op(y,w))) op#(i(x),op(y,z)) = 1z >= z = op#(i(i(y)),z) op#(i(x),op(y,z)) = 1z >= 1z = op#(f(x,i(x)),op(i(i(y)),z)) op#(i(x),op(y,op(z,w))) = 2w >= w = op#(y,w) op#(i(x),op(y,op(z,w))) = 2w >= 1w = op#(z,op(y,w)) op(i(x),op(y,z)) = 2z >= 2z = op(f(x,i(x)),op(i(i(y)),z)) op(i(x),op(y,op(z,w))) = 3w >= 3w = op(f(x,i(x)),op(z,op(y,w))) i(x) = x + 4 >= x = x f(x,y) = 1y + 1 >= x = x problem: DPs: op#(i(x),op(y,op(z,w))) -> op#(f(x,i(x)),op(z,op(y,w))) op#(i(x),op(y,z)) -> op#(f(x,i(x)),op(i(i(y)),z)) op#(i(x),op(y,op(z,w))) -> op#(z,op(y,w)) TRS: op(i(x),op(y,z)) -> op(f(x,i(x)),op(i(i(y)),z)) op(i(x),op(y,op(z,w))) -> op(f(x,i(x)),op(z,op(y,w))) i(x) -> x f(x,y) -> x Restore Modifier: DPs: op#(i(x),op(y,op(z,w))) -> op#(f(x,i(x)),op(z,op(y,w))) op#(i(x),op(y,z)) -> op#(f(x,i(x)),op(i(i(y)),z)) op#(i(x),op(y,op(z,w))) -> op#(z,op(y,w)) TRS: op(i(x),op(y,z)) -> op(f(x,i(x)),op(i(i(y)),z)) op(i(x),op(y,op(z,w))) -> op(f(x,i(x)),op(z,op(y,w))) i(x) -> x f(x,y) -> x KBO Processor: argument filtering: pi(i) = [0] pi(op) = [1] pi(f) = 1 pi(op#) = 1 usable rules: op(i(x),op(y,z)) -> op(f(x,i(x)),op(i(i(y)),z)) op(i(x),op(y,op(z,w))) -> op(f(x,i(x)),op(z,op(y,w))) weight function: w0 = 1 w(op#) = w(f) = w(op) = w(i) = 1 precedence: op# ~ f ~ op ~ i problem: DPs: op#(i(x),op(y,op(z,w))) -> op#(f(x,i(x)),op(z,op(y,w))) op#(i(x),op(y,z)) -> op#(f(x,i(x)),op(i(i(y)),z)) TRS: op(i(x),op(y,z)) -> op(f(x,i(x)),op(i(i(y)),z)) op(i(x),op(y,op(z,w))) -> op(f(x,i(x)),op(z,op(y,w))) i(x) -> x f(x,y) -> x Restore Modifier: DPs: op#(i(x),op(y,op(z,w))) -> op#(f(x,i(x)),op(z,op(y,w))) op#(i(x),op(y,z)) -> op#(f(x,i(x)),op(i(i(y)),z)) TRS: op(i(x),op(y,z)) -> op(f(x,i(x)),op(i(i(y)),z)) op(i(x),op(y,op(z,w))) -> op(f(x,i(x)),op(z,op(y,w))) i(x) -> x f(x,y) -> x KBO Processor: argument filtering: pi(i) = [0] pi(op) = [] pi(f) = 0 pi(op#) = 0 usable rules: f(x,y) -> x weight function: w0 = 1 w(op#) = w(f) = w(op) = w(i) = 1 precedence: op# ~ f ~ op ~ i problem: DPs: TRS: op(i(x),op(y,z)) -> op(f(x,i(x)),op(i(i(y)),z)) op(i(x),op(y,op(z,w))) -> op(f(x,i(x)),op(z,op(y,w))) i(x) -> x f(x,y) -> x Qed