YES Problem: op(i(x),op(y,z)) -> op(x,op(i(i(y)),z)) op(i(x),op(y,op(z,w))) -> op(x,op(z,op(y,w))) i(x) -> 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)) -> op#(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))) -> op#(x,op(z,op(y,w))) TRS: op(i(x),op(y,z)) -> op(x,op(i(i(y)),z)) op(i(x),op(y,op(z,w))) -> op(x,op(z,op(y,w))) i(x) -> 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)) -> op#(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))) -> op#(x,op(z,op(y,w))) TRS: op(i(x),op(y,z)) -> op(x,op(i(i(y)),z)) op(i(x),op(y,op(z,w))) -> op(x,op(z,op(y,w))) i(x) -> x graph: op#(i(x),op(y,op(z,w))) -> op#(z,op(y,w)) -> op#(i(x),op(y,op(z,w))) -> op#(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#(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#(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#(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#(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#(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#(x,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,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,op(z,w))) -> op#(x,op(z,op(y,w))) -> op#(i(x),op(y,op(z,w))) -> op#(x,op(z,op(y,w))) op#(i(x),op(y,op(z,w))) -> op#(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#(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#(x,op(z,op(y,w))) -> op#(i(x),op(y,z)) -> op#(x,op(i(i(y)),z)) op#(i(x),op(y,op(z,w))) -> op#(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#(x,op(z,op(y,w))) -> op#(i(x),op(y,z)) -> i#(i(y)) op#(i(x),op(y,op(z,w))) -> op#(x,op(z,op(y,w))) -> 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#(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#(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#(x,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)) -> 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) op#(i(x),op(y,z)) -> op#(x,op(i(i(y)),z)) -> op#(i(x),op(y,op(z,w))) -> op#(x,op(z,op(y,w))) op#(i(x),op(y,z)) -> op#(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#(x,op(i(i(y)),z)) -> op#(i(x),op(y,op(z,w))) -> op#(y,w) op#(i(x),op(y,z)) -> op#(x,op(i(i(y)),z)) -> op#(i(x),op(y,z)) -> op#(x,op(i(i(y)),z)) op#(i(x),op(y,z)) -> op#(x,op(i(i(y)),z)) -> op#(i(x),op(y,z)) -> op#(i(i(y)),z) op#(i(x),op(y,z)) -> op#(x,op(i(i(y)),z)) -> op#(i(x),op(y,z)) -> i#(i(y)) op#(i(x),op(y,z)) -> op#(x,op(i(i(y)),z)) -> op#(i(x),op(y,z)) -> i#(y) SCC Processor: #sccs: 1 #rules: 5 #arcs: 35/49 DPs: 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,z)) -> op#(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#(x,op(z,op(y,w))) TRS: op(i(x),op(y,z)) -> op(x,op(i(i(y)),z)) op(i(x),op(y,op(z,w))) -> op(x,op(z,op(y,w))) i(x) -> x KBO Processor: argument filtering: pi(i) = [0] pi(op) = [0,1] pi(op#) = [0,1] weight function: w0 = 1 w(op#) = 1 w(op) = w(i) = 0 precedence: op# ~ op ~ i problem: DPs: TRS: op(i(x),op(y,z)) -> op(x,op(i(i(y)),z)) op(i(x),op(y,op(z,w))) -> op(x,op(z,op(y,w))) i(x) -> x Qed