MAYBE Problem: +(x,+(y,z)) -> +(+(x,y),z) *(x,+(y,z)) -> +(*(x,y),*(x,z)) +(+(x,*(y,z)),*(y,u)) -> +(x,*(y,+(z,u))) Proof: DP Processor: DPs: +#(x,+(y,z)) -> +#(x,y) +#(x,+(y,z)) -> +#(+(x,y),z) *#(x,+(y,z)) -> *#(x,z) *#(x,+(y,z)) -> *#(x,y) *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) +#(+(x,*(y,z)),*(y,u)) -> +#(z,u) +#(+(x,*(y,z)),*(y,u)) -> *#(y,+(z,u)) +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u))) TRS: +(x,+(y,z)) -> +(+(x,y),z) *(x,+(y,z)) -> +(*(x,y),*(x,z)) +(+(x,*(y,z)),*(y,u)) -> +(x,*(y,+(z,u))) TDG Processor: DPs: +#(x,+(y,z)) -> +#(x,y) +#(x,+(y,z)) -> +#(+(x,y),z) *#(x,+(y,z)) -> *#(x,z) *#(x,+(y,z)) -> *#(x,y) *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) +#(+(x,*(y,z)),*(y,u)) -> +#(z,u) +#(+(x,*(y,z)),*(y,u)) -> *#(y,+(z,u)) +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u))) TRS: +(x,+(y,z)) -> +(+(x,y),z) *(x,+(y,z)) -> +(*(x,y),*(x,z)) +(+(x,*(y,z)),*(y,u)) -> +(x,*(y,+(z,u))) graph: *#(x,+(y,z)) -> *#(x,z) -> *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) *#(x,+(y,z)) -> *#(x,z) -> *#(x,+(y,z)) -> *#(x,y) *#(x,+(y,z)) -> *#(x,z) -> *#(x,+(y,z)) -> *#(x,z) *#(x,+(y,z)) -> *#(x,y) -> *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) *#(x,+(y,z)) -> *#(x,y) -> *#(x,+(y,z)) -> *#(x,y) *#(x,+(y,z)) -> *#(x,y) -> *#(x,+(y,z)) -> *#(x,z) *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) -> +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u))) *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) -> +#(+(x,*(y,z)),*(y,u)) -> *#(y,+(z,u)) *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) -> +#(+(x,*(y,z)),*(y,u)) -> +#(z,u) *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) -> +#(x,+(y,z)) -> +#(+(x,y),z) *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) -> +#(x,+(y,z)) -> +#(x,y) +#(+(x,*(y,z)),*(y,u)) -> *#(y,+(z,u)) -> *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) +#(+(x,*(y,z)),*(y,u)) -> *#(y,+(z,u)) -> *#(x,+(y,z)) -> *#(x,y) +#(+(x,*(y,z)),*(y,u)) -> *#(y,+(z,u)) -> *#(x,+(y,z)) -> *#(x,z) +#(+(x,*(y,z)),*(y,u)) -> +#(z,u) -> +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u))) +#(+(x,*(y,z)),*(y,u)) -> +#(z,u) -> +#(+(x,*(y,z)),*(y,u)) -> *#(y,+(z,u)) +#(+(x,*(y,z)),*(y,u)) -> +#(z,u) -> +#(+(x,*(y,z)),*(y,u)) -> +#(z,u) +#(+(x,*(y,z)),*(y,u)) -> +#(z,u) -> +#(x,+(y,z)) -> +#(+(x,y),z) +#(+(x,*(y,z)),*(y,u)) -> +#(z,u) -> +#(x,+(y,z)) -> +#(x,y) +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u))) -> +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u))) +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u))) -> +#(+(x,*(y,z)),*(y,u)) -> *#(y,+(z,u)) +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u))) -> +#(+(x,*(y,z)),*(y,u)) -> +#(z,u) +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u))) -> +#(x,+(y,z)) -> +#(+(x,y),z) +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u))) -> +#(x,+(y,z)) -> +#(x,y) +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u))) +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(+(x,*(y,z)),*(y,u)) -> *#(y,+(z,u)) +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(+(x,*(y,z)),*(y,u)) -> +#(z,u) +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(x,y) +#(x,+(y,z)) -> +#(x,y) -> +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u))) +#(x,+(y,z)) -> +#(x,y) -> +#(+(x,*(y,z)),*(y,u)) -> *#(y,+(z,u)) +#(x,+(y,z)) -> +#(x,y) -> +#(+(x,*(y,z)),*(y,u)) -> +#(z,u) +#(x,+(y,z)) -> +#(x,y) -> +#(x,+(y,z)) -> +#(+(x,y),z) +#(x,+(y,z)) -> +#(x,y) -> +#(x,+(y,z)) -> +#(x,y) Arctic Interpretation Processor: dimension: 1 interpretation: [*#](x0, x1) = 2x1 + 2, [+#](x0, x1) = 1x0 + 1x1 + 0, [*](x0, x1) = 1x1 + 1, [+](x0, x1) = x0 + x1 orientation: +#(x,+(y,z)) = 1x + 1y + 1z + 0 >= 1x + 1y + 0 = +#(x,y) +#(x,+(y,z)) = 1x + 1y + 1z + 0 >= 1x + 1y + 1z + 0 = +#(+(x,y),z) *#(x,+(y,z)) = 2y + 2z + 2 >= 2z + 2 = *#(x,z) *#(x,+(y,z)) = 2y + 2z + 2 >= 2y + 2 = *#(x,y) *#(x,+(y,z)) = 2y + 2z + 2 >= 2y + 2z + 2 = +#(*(x,y),*(x,z)) +#(+(x,*(y,z)),*(y,u)) = 2u + 1x + 2z + 2 >= 1u + 1z + 0 = +#(z,u) +#(+(x,*(y,z)),*(y,u)) = 2u + 1x + 2z + 2 >= 2u + 2z + 2 = *#(y,+(z,u)) +#(+(x,*(y,z)),*(y,u)) = 2u + 1x + 2z + 2 >= 2u + 1x + 2z + 2 = +#(x,*(y,+(z,u))) +(x,+(y,z)) = x + y + z >= x + y + z = +(+(x,y),z) *(x,+(y,z)) = 1y + 1z + 1 >= 1y + 1z + 1 = +(*(x,y),*(x,z)) +(+(x,*(y,z)),*(y,u)) = 1u + x + 1z + 1 >= 1u + x + 1z + 1 = +(x,*(y,+(z,u))) problem: DPs: +#(x,+(y,z)) -> +#(x,y) +#(x,+(y,z)) -> +#(+(x,y),z) *#(x,+(y,z)) -> *#(x,z) *#(x,+(y,z)) -> *#(x,y) *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) +#(+(x,*(y,z)),*(y,u)) -> *#(y,+(z,u)) +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u))) TRS: +(x,+(y,z)) -> +(+(x,y),z) *(x,+(y,z)) -> +(*(x,y),*(x,z)) +(+(x,*(y,z)),*(y,u)) -> +(x,*(y,+(z,u))) Matrix Interpretation Processor: dim=1 interpretation: [*#](x0, x1) = x1 + 1, [+#](x0, x1) = x0 + x1 + 2, [*](x0, x1) = x1, [+](x0, x1) = x0 + x1 + 1 orientation: +#(x,+(y,z)) = x + y + z + 3 >= x + y + 2 = +#(x,y) +#(x,+(y,z)) = x + y + z + 3 >= x + y + z + 3 = +#(+(x,y),z) *#(x,+(y,z)) = y + z + 2 >= z + 1 = *#(x,z) *#(x,+(y,z)) = y + z + 2 >= y + 1 = *#(x,y) *#(x,+(y,z)) = y + z + 2 >= y + z + 2 = +#(*(x,y),*(x,z)) +#(+(x,*(y,z)),*(y,u)) = u + x + z + 3 >= u + z + 2 = *#(y,+(z,u)) +#(+(x,*(y,z)),*(y,u)) = u + x + z + 3 >= u + x + z + 3 = +#(x,*(y,+(z,u))) +(x,+(y,z)) = x + y + z + 2 >= x + y + z + 2 = +(+(x,y),z) *(x,+(y,z)) = y + z + 1 >= y + z + 1 = +(*(x,y),*(x,z)) +(+(x,*(y,z)),*(y,u)) = u + x + z + 2 >= u + x + z + 2 = +(x,*(y,+(z,u))) problem: DPs: +#(x,+(y,z)) -> +#(+(x,y),z) *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u))) TRS: +(x,+(y,z)) -> +(+(x,y),z) *(x,+(y,z)) -> +(*(x,y),*(x,z)) +(+(x,*(y,z)),*(y,u)) -> +(x,*(y,+(z,u))) SCC Processor: #sccs: 1 #rules: 2 #arcs: 34/9 DPs: +#(x,+(y,z)) -> +#(+(x,y),z) +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u))) TRS: +(x,+(y,z)) -> +(+(x,y),z) *(x,+(y,z)) -> +(*(x,y),*(x,z)) +(+(x,*(y,z)),*(y,u)) -> +(x,*(y,+(z,u))) Open