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))) CDG 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,z) *#(x,+(y,z)) -> *#(x,z) -> *#(x,+(y,z)) -> *#(x,y) *#(x,+(y,z)) -> *#(x,z) -> *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) *#(x,+(y,z)) -> *#(x,y) -> *#(x,+(y,z)) -> *#(x,z) *#(x,+(y,z)) -> *#(x,y) -> *#(x,+(y,z)) -> *#(x,y) *#(x,+(y,z)) -> *#(x,y) -> *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) -> +#(x,+(y,z)) -> +#(x,y) *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) -> +#(x,+(y,z)) -> +#(+(x,y),z) *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) -> +#(+(x,*(y,z)),*(y,u)) -> +#(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)) -> +#(x,*(y,+(z,u))) +#(+(x,*(y,z)),*(y,u)) -> *#(y,+(z,u)) -> *#(x,+(y,z)) -> *#(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,y),*(x,z)) +#(+(x,*(y,z)),*(y,u)) -> +#(z,u) -> +#(x,+(y,z)) -> +#(x,y) +#(+(x,*(y,z)),*(y,u)) -> +#(z,u) -> +#(x,+(y,z)) -> +#(+(x,y),z) +#(+(x,*(y,z)),*(y,u)) -> +#(z,u) -> +#(+(x,*(y,z)),*(y,u)) -> +#(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)) -> +#(x,*(y,+(z,u))) +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u))) -> +#(x,+(y,z)) -> +#(x,y) +#(+(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)),*(y,u)) -> +#(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)) -> +#(x,*(y,+(z,u))) +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(x,y) +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(+(x,*(y,z)),*(y,u)) -> +#(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)) -> +#(x,*(y,+(z,u))) +#(x,+(y,z)) -> +#(x,y) -> +#(x,+(y,z)) -> +#(x,y) +#(x,+(y,z)) -> +#(x,y) -> +#(x,+(y,z)) -> +#(+(x,y),z) +#(x,+(y,z)) -> +#(x,y) -> +#(+(x,*(y,z)),*(y,u)) -> +#(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)) -> +#(x,*(y,+(z,u))) Restore Modifier: 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))) SCC Processor: #sccs: 1 #rules: 8 #arcs: 34/64 DPs: *#(x,+(y,z)) -> *#(x,z) *#(x,+(y,z)) -> +#(*(x,y),*(x,z)) +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u))) +#(+(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),z) +#(x,+(y,z)) -> +#(x,y) 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: dimension: 1 interpretation: [*#](x0, x1) = x1, [+#](x0, x1) = x0 + x1, [*](x0, x1) = x1, [+](x0, x1) = x0 + x1 + 1 orientation: *#(x,+(y,z)) = y + z + 1 >= z = *#(x,z) *#(x,+(y,z)) = y + z + 1 >= y + z = +#(*(x,y),*(x,z)) +#(+(x,*(y,z)),*(y,u)) = u + x + z + 1 >= u + x + z + 1 = +#(x,*(y,+(z,u))) +#(+(x,*(y,z)),*(y,u)) = u + x + z + 1 >= u + z + 1 = *#(y,+(z,u)) *#(x,+(y,z)) = y + z + 1 >= y = *#(x,y) +#(+(x,*(y,z)),*(y,u)) = u + x + z + 1 >= u + z = +#(z,u) +#(x,+(y,z)) = x + y + z + 1 >= x + y + z + 1 = +#(+(x,y),z) +#(x,+(y,z)) = x + y + z + 1 >= x + y = +#(x,y) +(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)),*(y,u)) -> +#(x,*(y,+(z,u))) +#(+(x,*(y,z)),*(y,u)) -> *#(y,+(z,u)) +#(x,+(y,z)) -> +#(+(x,y),z) 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: dimension: 1 interpretation: [*#](x0, x1) = 0, [+#](x0, x1) = x1, [*](x0, x1) = 1, [+](x0, x1) = x1 orientation: +#(+(x,*(y,z)),*(y,u)) = 1 >= 1 = +#(x,*(y,+(z,u))) +#(+(x,*(y,z)),*(y,u)) = 1 >= 0 = *#(y,+(z,u)) +#(x,+(y,z)) = z >= z = +#(+(x,y),z) +(x,+(y,z)) = z >= z = +(+(x,y),z) *(x,+(y,z)) = 1 >= 1 = +(*(x,y),*(x,z)) +(+(x,*(y,z)),*(y,u)) = 1 >= 1 = +(x,*(y,+(z,u))) problem: DPs: +#(+(x,*(y,z)),*(y,u)) -> +#(x,*(y,+(z,u))) +#(x,+(y,z)) -> +#(+(x,y),z) TRS: +(x,+(y,z)) -> +(+(x,y),z) *(x,+(y,z)) -> +(*(x,y),*(x,z)) +(+(x,*(y,z)),*(y,u)) -> +(x,*(y,+(z,u))) Open