YES Problem: :(x,x) -> e() :(x,e()) -> x i(:(x,y)) -> :(y,x) :(:(x,y),z) -> :(x,:(z,i(y))) :(e(),x) -> i(x) i(i(x)) -> x i(e()) -> e() :(x,:(y,i(x))) -> i(y) :(x,:(y,:(i(x),z))) -> :(i(z),y) :(i(x),:(y,x)) -> i(y) :(i(x),:(y,:(x,z))) -> :(i(z),y) Proof: DP Processor: DPs: i#(:(x,y)) -> :#(y,x) :#(:(x,y),z) -> i#(y) :#(:(x,y),z) -> :#(z,i(y)) :#(:(x,y),z) -> :#(x,:(z,i(y))) :#(e(),x) -> i#(x) :#(x,:(y,i(x))) -> i#(y) :#(x,:(y,:(i(x),z))) -> i#(z) :#(x,:(y,:(i(x),z))) -> :#(i(z),y) :#(i(x),:(y,x)) -> i#(y) :#(i(x),:(y,:(x,z))) -> i#(z) :#(i(x),:(y,:(x,z))) -> :#(i(z),y) TRS: :(x,x) -> e() :(x,e()) -> x i(:(x,y)) -> :(y,x) :(:(x,y),z) -> :(x,:(z,i(y))) :(e(),x) -> i(x) i(i(x)) -> x i(e()) -> e() :(x,:(y,i(x))) -> i(y) :(x,:(y,:(i(x),z))) -> :(i(z),y) :(i(x),:(y,x)) -> i(y) :(i(x),:(y,:(x,z))) -> :(i(z),y) EDG Processor: DPs: i#(:(x,y)) -> :#(y,x) :#(:(x,y),z) -> i#(y) :#(:(x,y),z) -> :#(z,i(y)) :#(:(x,y),z) -> :#(x,:(z,i(y))) :#(e(),x) -> i#(x) :#(x,:(y,i(x))) -> i#(y) :#(x,:(y,:(i(x),z))) -> i#(z) :#(x,:(y,:(i(x),z))) -> :#(i(z),y) :#(i(x),:(y,x)) -> i#(y) :#(i(x),:(y,:(x,z))) -> i#(z) :#(i(x),:(y,:(x,z))) -> :#(i(z),y) TRS: :(x,x) -> e() :(x,e()) -> x i(:(x,y)) -> :(y,x) :(:(x,y),z) -> :(x,:(z,i(y))) :(e(),x) -> i(x) i(i(x)) -> x i(e()) -> e() :(x,:(y,i(x))) -> i(y) :(x,:(y,:(i(x),z))) -> :(i(z),y) :(i(x),:(y,x)) -> i(y) :(i(x),:(y,:(x,z))) -> :(i(z),y) graph: i#(:(x,y)) -> :#(y,x) -> :#(:(x,y),z) -> i#(y) i#(:(x,y)) -> :#(y,x) -> :#(:(x,y),z) -> :#(z,i(y)) i#(:(x,y)) -> :#(y,x) -> :#(:(x,y),z) -> :#(x,:(z,i(y))) i#(:(x,y)) -> :#(y,x) -> :#(e(),x) -> i#(x) i#(:(x,y)) -> :#(y,x) -> :#(x,:(y,i(x))) -> i#(y) i#(:(x,y)) -> :#(y,x) -> :#(x,:(y,:(i(x),z))) -> i#(z) i#(:(x,y)) -> :#(y,x) -> :#(x,:(y,:(i(x),z))) -> :#(i(z),y) i#(:(x,y)) -> :#(y,x) -> :#(i(x),:(y,x)) -> i#(y) i#(:(x,y)) -> :#(y,x) -> :#(i(x),:(y,:(x,z))) -> i#(z) i#(:(x,y)) -> :#(y,x) -> :#(i(x),:(y,:(x,z))) -> :#(i(z),y) :#(i(x),:(y,:(x,z))) -> i#(z) -> i#(:(x,y)) -> :#(y,x) :#(i(x),:(y,:(x,z))) -> :#(i(z),y) -> :#(:(x,y),z) -> i#(y) :#(i(x),:(y,:(x,z))) -> :#(i(z),y) -> :#(:(x,y),z) -> :#(z,i(y)) :#(i(x),:(y,:(x,z))) -> :#(i(z),y) -> :#(:(x,y),z) -> :#(x,:(z,i(y))) :#(i(x),:(y,:(x,z))) -> :#(i(z),y) -> :#(e(),x) -> i#(x) :#(i(x),:(y,:(x,z))) -> :#(i(z),y) -> :#(x,:(y,i(x))) -> i#(y) :#(i(x),:(y,:(x,z))) -> :#(i(z),y) -> :#(x,:(y,:(i(x),z))) -> i#(z) :#(i(x),:(y,:(x,z))) -> :#(i(z),y) -> :#(x,:(y,:(i(x),z))) -> :#(i(z),y) :#(i(x),:(y,:(x,z))) -> :#(i(z),y) -> :#(i(x),:(y,x)) -> i#(y) :#(i(x),:(y,:(x,z))) -> :#(i(z),y) -> :#(i(x),:(y,:(x,z))) -> i#(z) :#(i(x),:(y,:(x,z))) -> :#(i(z),y) -> :#(i(x),:(y,:(x,z))) -> :#(i(z),y) :#(i(x),:(y,x)) -> i#(y) -> i#(:(x,y)) -> :#(y,x) :#(e(),x) -> i#(x) -> i#(:(x,y)) -> :#(y,x) :#(:(x,y),z) -> i#(y) -> i#(:(x,y)) -> :#(y,x) :#(:(x,y),z) -> :#(z,i(y)) -> :#(:(x,y),z) -> i#(y) :#(:(x,y),z) -> :#(z,i(y)) -> :#(:(x,y),z) -> :#(z,i(y)) :#(:(x,y),z) -> :#(z,i(y)) -> :#(:(x,y),z) -> :#(x,:(z,i(y))) :#(:(x,y),z) -> :#(z,i(y)) -> :#(e(),x) -> i#(x) :#(:(x,y),z) -> :#(z,i(y)) -> :#(x,:(y,i(x))) -> i#(y) :#(:(x,y),z) -> :#(z,i(y)) -> :#(x,:(y,:(i(x),z))) -> i#(z) :#(:(x,y),z) -> :#(z,i(y)) -> :#(x,:(y,:(i(x),z))) -> :#(i(z),y) :#(:(x,y),z) -> :#(z,i(y)) -> :#(i(x),:(y,x)) -> i#(y) :#(:(x,y),z) -> :#(z,i(y)) -> :#(i(x),:(y,:(x,z))) -> i#(z) :#(:(x,y),z) -> :#(z,i(y)) -> :#(i(x),:(y,:(x,z))) -> :#(i(z),y) :#(:(x,y),z) -> :#(x,:(z,i(y))) -> :#(:(x,y),z) -> i#(y) :#(:(x,y),z) -> :#(x,:(z,i(y))) -> :#(:(x,y),z) -> :#(z,i(y)) :#(:(x,y),z) -> :#(x,:(z,i(y))) -> :#(:(x,y),z) -> :#(x,:(z,i(y))) :#(:(x,y),z) -> :#(x,:(z,i(y))) -> :#(e(),x) -> i#(x) :#(:(x,y),z) -> :#(x,:(z,i(y))) -> :#(x,:(y,i(x))) -> i#(y) :#(:(x,y),z) -> :#(x,:(z,i(y))) -> :#(x,:(y,:(i(x),z))) -> i#(z) :#(:(x,y),z) -> :#(x,:(z,i(y))) -> :#(x,:(y,:(i(x),z))) -> :#(i(z),y) :#(:(x,y),z) -> :#(x,:(z,i(y))) -> :#(i(x),:(y,x)) -> i#(y) :#(:(x,y),z) -> :#(x,:(z,i(y))) -> :#(i(x),:(y,:(x,z))) -> i#(z) :#(:(x,y),z) -> :#(x,:(z,i(y))) -> :#(i(x),:(y,:(x,z))) -> :#(i(z),y) :#(x,:(y,i(x))) -> i#(y) -> i#(:(x,y)) -> :#(y,x) :#(x,:(y,:(i(x),z))) -> i#(z) -> i#(:(x,y)) -> :#(y,x) :#(x,:(y,:(i(x),z))) -> :#(i(z),y) -> :#(:(x,y),z) -> i#(y) :#(x,:(y,:(i(x),z))) -> :#(i(z),y) -> :#(:(x,y),z) -> :#(z,i(y)) :#(x,:(y,:(i(x),z))) -> :#(i(z),y) -> :#(:(x,y),z) -> :#(x,:(z,i(y))) :#(x,:(y,:(i(x),z))) -> :#(i(z),y) -> :#(e(),x) -> i#(x) :#(x,:(y,:(i(x),z))) -> :#(i(z),y) -> :#(x,:(y,i(x))) -> i#(y) :#(x,:(y,:(i(x),z))) -> :#(i(z),y) -> :#(x,:(y,:(i(x),z))) -> i#(z) :#(x,:(y,:(i(x),z))) -> :#(i(z),y) -> :#(x,:(y,:(i(x),z))) -> :#(i(z),y) :#(x,:(y,:(i(x),z))) -> :#(i(z),y) -> :#(i(x),:(y,x)) -> i#(y) :#(x,:(y,:(i(x),z))) -> :#(i(z),y) -> :#(i(x),:(y,:(x,z))) -> i#(z) :#(x,:(y,:(i(x),z))) -> :#(i(z),y) -> :#(i(x),:(y,:(x,z))) -> :#(i(z),y) Matrix Interpretation Processor: dimension: 1 interpretation: [i#](x0) = x0, [:#](x0, x1) = x0 + x1, [i](x0) = x0, [e] = 0, [:](x0, x1) = x0 + x1 + 1 orientation: i#(:(x,y)) = x + y + 1 >= x + y = :#(y,x) :#(:(x,y),z) = x + y + z + 1 >= y = i#(y) :#(:(x,y),z) = x + y + z + 1 >= y + z = :#(z,i(y)) :#(:(x,y),z) = x + y + z + 1 >= x + y + z + 1 = :#(x,:(z,i(y))) :#(e(),x) = x >= x = i#(x) :#(x,:(y,i(x))) = 2x + y + 1 >= y = i#(y) :#(x,:(y,:(i(x),z))) = 2x + y + z + 2 >= z = i#(z) :#(x,:(y,:(i(x),z))) = 2x + y + z + 2 >= y + z = :#(i(z),y) :#(i(x),:(y,x)) = 2x + y + 1 >= y = i#(y) :#(i(x),:(y,:(x,z))) = 2x + y + z + 2 >= z = i#(z) :#(i(x),:(y,:(x,z))) = 2x + y + z + 2 >= y + z = :#(i(z),y) :(x,x) = 2x + 1 >= 0 = e() :(x,e()) = x + 1 >= x = x i(:(x,y)) = x + y + 1 >= x + y + 1 = :(y,x) :(:(x,y),z) = x + y + z + 2 >= x + y + z + 2 = :(x,:(z,i(y))) :(e(),x) = x + 1 >= x = i(x) i(i(x)) = x >= x = x i(e()) = 0 >= 0 = e() :(x,:(y,i(x))) = 2x + y + 2 >= y = i(y) :(x,:(y,:(i(x),z))) = 2x + y + z + 3 >= y + z + 1 = :(i(z),y) :(i(x),:(y,x)) = 2x + y + 2 >= y = i(y) :(i(x),:(y,:(x,z))) = 2x + y + z + 3 >= y + z + 1 = :(i(z),y) problem: DPs: :#(:(x,y),z) -> :#(x,:(z,i(y))) :#(e(),x) -> i#(x) TRS: :(x,x) -> e() :(x,e()) -> x i(:(x,y)) -> :(y,x) :(:(x,y),z) -> :(x,:(z,i(y))) :(e(),x) -> i(x) i(i(x)) -> x i(e()) -> e() :(x,:(y,i(x))) -> i(y) :(x,:(y,:(i(x),z))) -> :(i(z),y) :(i(x),:(y,x)) -> i(y) :(i(x),:(y,:(x,z))) -> :(i(z),y) Matrix Interpretation Processor: dimension: 1 interpretation: [i#](x0) = 0, [:#](x0, x1) = 1, [i](x0) = x0, [e] = 0, [:](x0, x1) = x0 + x1 orientation: :#(:(x,y),z) = 1 >= 1 = :#(x,:(z,i(y))) :#(e(),x) = 1 >= 0 = i#(x) :(x,x) = 2x >= 0 = e() :(x,e()) = x >= x = x i(:(x,y)) = x + y >= x + y = :(y,x) :(:(x,y),z) = x + y + z >= x + y + z = :(x,:(z,i(y))) :(e(),x) = x >= x = i(x) i(i(x)) = x >= x = x i(e()) = 0 >= 0 = e() :(x,:(y,i(x))) = 2x + y >= y = i(y) :(x,:(y,:(i(x),z))) = 2x + y + z >= y + z = :(i(z),y) :(i(x),:(y,x)) = 2x + y >= y = i(y) :(i(x),:(y,:(x,z))) = 2x + y + z >= y + z = :(i(z),y) problem: DPs: :#(:(x,y),z) -> :#(x,:(z,i(y))) TRS: :(x,x) -> e() :(x,e()) -> x i(:(x,y)) -> :(y,x) :(:(x,y),z) -> :(x,:(z,i(y))) :(e(),x) -> i(x) i(i(x)) -> x i(e()) -> e() :(x,:(y,i(x))) -> i(y) :(x,:(y,:(i(x),z))) -> :(i(z),y) :(i(x),:(y,x)) -> i(y) :(i(x),:(y,:(x,z))) -> :(i(z),y) Subterm Criterion Processor: simple projection: pi(:#) = 0 problem: DPs: TRS: :(x,x) -> e() :(x,e()) -> x i(:(x,y)) -> :(y,x) :(:(x,y),z) -> :(x,:(z,i(y))) :(e(),x) -> i(x) i(i(x)) -> x i(e()) -> e() :(x,:(y,i(x))) -> i(y) :(x,:(y,:(i(x),z))) -> :(i(z),y) :(i(x),:(y,x)) -> i(y) :(i(x),:(y,:(x,z))) -> :(i(z),y) Qed