YES Problem: +(a(),b()) -> +(b(),a()) +(a(),+(b(),z)) -> +(b(),+(a(),z)) +(+(x,y),z) -> +(x,+(y,z)) f(a(),y) -> a() f(b(),y) -> b() f(+(x,y),z) -> +(f(x,z),f(y,z)) Proof: DP Processor: DPs: +#(a(),b()) -> +#(b(),a()) +#(a(),+(b(),z)) -> +#(a(),z) +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(x,+(y,z)) f#(+(x,y),z) -> f#(y,z) f#(+(x,y),z) -> f#(x,z) f#(+(x,y),z) -> +#(f(x,z),f(y,z)) TRS: +(a(),b()) -> +(b(),a()) +(a(),+(b(),z)) -> +(b(),+(a(),z)) +(+(x,y),z) -> +(x,+(y,z)) f(a(),y) -> a() f(b(),y) -> b() f(+(x,y),z) -> +(f(x,z),f(y,z)) EDG Processor: DPs: +#(a(),b()) -> +#(b(),a()) +#(a(),+(b(),z)) -> +#(a(),z) +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(x,+(y,z)) f#(+(x,y),z) -> f#(y,z) f#(+(x,y),z) -> f#(x,z) f#(+(x,y),z) -> +#(f(x,z),f(y,z)) TRS: +(a(),b()) -> +(b(),a()) +(a(),+(b(),z)) -> +(b(),+(a(),z)) +(+(x,y),z) -> +(x,+(y,z)) f(a(),y) -> a() f(b(),y) -> b() f(+(x,y),z) -> +(f(x,z),f(y,z)) graph: f#(+(x,y),z) -> f#(y,z) -> f#(+(x,y),z) -> f#(y,z) f#(+(x,y),z) -> f#(y,z) -> f#(+(x,y),z) -> f#(x,z) f#(+(x,y),z) -> f#(y,z) -> f#(+(x,y),z) -> +#(f(x,z),f(y,z)) f#(+(x,y),z) -> f#(x,z) -> f#(+(x,y),z) -> f#(y,z) f#(+(x,y),z) -> f#(x,z) -> f#(+(x,y),z) -> f#(x,z) f#(+(x,y),z) -> f#(x,z) -> f#(+(x,y),z) -> +#(f(x,z),f(y,z)) f#(+(x,y),z) -> +#(f(x,z),f(y,z)) -> +#(a(),b()) -> +#(b(),a()) f#(+(x,y),z) -> +#(f(x,z),f(y,z)) -> +#(a(),+(b(),z)) -> +#(a(),z) f#(+(x,y),z) -> +#(f(x,z),f(y,z)) -> +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) f#(+(x,y),z) -> +#(f(x,z),f(y,z)) -> +#(+(x,y),z) -> +#(y,z) f#(+(x,y),z) -> +#(f(x,z),f(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z)) +#(+(x,y),z) -> +#(y,z) -> +#(a(),b()) -> +#(b(),a()) +#(+(x,y),z) -> +#(y,z) -> +#(a(),+(b(),z)) -> +#(a(),z) +#(+(x,y),z) -> +#(y,z) -> +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) +#(+(x,y),z) -> +#(y,z) -> +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(y,z) -> +#(+(x,y),z) -> +#(x,+(y,z)) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(a(),b()) -> +#(b(),a()) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(a(),+(b(),z)) -> +#(a(),z) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z)) +#(a(),+(b(),z)) -> +#(a(),z) -> +#(a(),b()) -> +#(b(),a()) +#(a(),+(b(),z)) -> +#(a(),z) -> +#(a(),+(b(),z)) -> +#(a(),z) +#(a(),+(b(),z)) -> +#(a(),z) -> +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) Restore Modifier: DPs: +#(a(),b()) -> +#(b(),a()) +#(a(),+(b(),z)) -> +#(a(),z) +#(a(),+(b(),z)) -> +#(b(),+(a(),z)) +#(+(x,y),z) -> +#(y,z) +#(+(x,y),z) -> +#(x,+(y,z)) f#(+(x,y),z) -> f#(y,z) f#(+(x,y),z) -> f#(x,z) f#(+(x,y),z) -> +#(f(x,z),f(y,z)) TRS: +(a(),b()) -> +(b(),a()) +(a(),+(b(),z)) -> +(b(),+(a(),z)) +(+(x,y),z) -> +(x,+(y,z)) f(a(),y) -> a() f(b(),y) -> b() f(+(x,y),z) -> +(f(x,z),f(y,z)) SCC Processor: #sccs: 3 #rules: 5 #arcs: 24/64 DPs: f#(+(x,y),z) -> f#(y,z) f#(+(x,y),z) -> f#(x,z) TRS: +(a(),b()) -> +(b(),a()) +(a(),+(b(),z)) -> +(b(),+(a(),z)) +(+(x,y),z) -> +(x,+(y,z)) f(a(),y) -> a() f(b(),y) -> b() f(+(x,y),z) -> +(f(x,z),f(y,z)) Matrix Interpretation Processor: dimension: 1 interpretation: [f#](x0, x1) = x0 + 1, [f](x0, x1) = x0, [+](x0, x1) = x0 + x1 + 1, [b] = 0, [a] = 0 orientation: f#(+(x,y),z) = x + y + 2 >= y + 1 = f#(y,z) f#(+(x,y),z) = x + y + 2 >= x + 1 = f#(x,z) +(a(),b()) = 1 >= 1 = +(b(),a()) +(a(),+(b(),z)) = z + 2 >= z + 2 = +(b(),+(a(),z)) +(+(x,y),z) = x + y + z + 2 >= x + y + z + 2 = +(x,+(y,z)) f(a(),y) = 0 >= 0 = a() f(b(),y) = 0 >= 0 = b() f(+(x,y),z) = x + y + 1 >= x + y + 1 = +(f(x,z),f(y,z)) problem: DPs: TRS: +(a(),b()) -> +(b(),a()) +(a(),+(b(),z)) -> +(b(),+(a(),z)) +(+(x,y),z) -> +(x,+(y,z)) f(a(),y) -> a() f(b(),y) -> b() f(+(x,y),z) -> +(f(x,z),f(y,z)) Qed DPs: +#(+(x,y),z) -> +#(x,+(y,z)) +#(+(x,y),z) -> +#(y,z) TRS: +(a(),b()) -> +(b(),a()) +(a(),+(b(),z)) -> +(b(),+(a(),z)) +(+(x,y),z) -> +(x,+(y,z)) f(a(),y) -> a() f(b(),y) -> b() f(+(x,y),z) -> +(f(x,z),f(y,z)) Matrix Interpretation Processor: dimension: 1 interpretation: [+#](x0, x1) = x0, [f](x0, x1) = x0, [+](x0, x1) = x0 + x1 + 1, [b] = 0, [a] = 1 orientation: +#(+(x,y),z) = x + y + 1 >= x = +#(x,+(y,z)) +#(+(x,y),z) = x + y + 1 >= y = +#(y,z) +(a(),b()) = 2 >= 2 = +(b(),a()) +(a(),+(b(),z)) = z + 3 >= z + 3 = +(b(),+(a(),z)) +(+(x,y),z) = x + y + z + 2 >= x + y + z + 2 = +(x,+(y,z)) f(a(),y) = 1 >= 1 = a() f(b(),y) = 0 >= 0 = b() f(+(x,y),z) = x + y + 1 >= x + y + 1 = +(f(x,z),f(y,z)) problem: DPs: TRS: +(a(),b()) -> +(b(),a()) +(a(),+(b(),z)) -> +(b(),+(a(),z)) +(+(x,y),z) -> +(x,+(y,z)) f(a(),y) -> a() f(b(),y) -> b() f(+(x,y),z) -> +(f(x,z),f(y,z)) Qed DPs: +#(a(),+(b(),z)) -> +#(a(),z) TRS: +(a(),b()) -> +(b(),a()) +(a(),+(b(),z)) -> +(b(),+(a(),z)) +(+(x,y),z) -> +(x,+(y,z)) f(a(),y) -> a() f(b(),y) -> b() f(+(x,y),z) -> +(f(x,z),f(y,z)) Matrix Interpretation Processor: dimension: 1 interpretation: [+#](x0, x1) = x1, [f](x0, x1) = x0, [+](x0, x1) = x0 + x1 + 1, [b] = 1, [a] = 0 orientation: +#(a(),+(b(),z)) = z + 2 >= z = +#(a(),z) +(a(),b()) = 2 >= 2 = +(b(),a()) +(a(),+(b(),z)) = z + 3 >= z + 3 = +(b(),+(a(),z)) +(+(x,y),z) = x + y + z + 2 >= x + y + z + 2 = +(x,+(y,z)) f(a(),y) = 0 >= 0 = a() f(b(),y) = 1 >= 1 = b() f(+(x,y),z) = x + y + 1 >= x + y + 1 = +(f(x,z),f(y,z)) problem: DPs: TRS: +(a(),b()) -> +(b(),a()) +(a(),+(b(),z)) -> +(b(),+(a(),z)) +(+(x,y),z) -> +(x,+(y,z)) f(a(),y) -> a() f(b(),y) -> b() f(+(x,y),z) -> +(f(x,z),f(y,z)) Qed