0 CpxTRS
↳1 RcToIrcProof (BOTH BOUNDS(ID, ID), 10 ms)
↳2 CpxTRS
↳3 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CdtProblem
↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CdtProblem
↳7 CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)), 167 ms)
↳8 CdtProblem
↳9 CdtRuleRemovalProof (UPPER BOUND(ADD(n^2)), 121 ms)
↳10 CdtProblem
↳11 CdtRuleRemovalProof (UPPER BOUND(ADD(n^3)), 1042 ms)
↳12 CdtProblem
↳13 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)
↳14 BOUNDS(1, 1)
+(0, y) → y
+(s(x), y) → s(+(x, y))
+(p(x), y) → p(+(x, y))
minus(0) → 0
minus(s(x)) → p(minus(x))
minus(p(x)) → s(minus(x))
*(0, y) → 0
*(s(x), y) → +(*(x, y), y)
*(p(x), y) → +(*(x, y), minus(y))
The duplicating contexts are:
*(s(x), [])
*(p(x), [])
The defined contexts are:
+([], x1)
+(x0, [])
As the TRS is an overlay system and the defined contexts and the duplicating contexts don't overlap, we have rc = irc.
+(0, y) → y
+(s(x), y) → s(+(x, y))
+(p(x), y) → p(+(x, y))
minus(0) → 0
minus(s(x)) → p(minus(x))
minus(p(x)) → s(minus(x))
*(0, y) → 0
*(s(x), y) → +(*(x, y), y)
*(p(x), y) → +(*(x, y), minus(y))
Tuples:
+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
+(p(z0), z1) → p(+(z0, z1))
minus(0) → 0
minus(s(z0)) → p(minus(z0))
minus(p(z0)) → s(minus(z0))
*(0, z0) → 0
*(s(z0), z1) → +(*(z0, z1), z1)
*(p(z0), z1) → +(*(z0, z1), minus(z1))
S tuples:
+'(0, z0) → c
+'(s(z0), z1) → c1(+'(z0, z1))
+'(p(z0), z1) → c2(+'(z0, z1))
MINUS(0) → c3
MINUS(s(z0)) → c4(MINUS(z0))
MINUS(p(z0)) → c5(MINUS(z0))
*'(0, z0) → c6
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1))
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
K tuples:none
+'(0, z0) → c
+'(s(z0), z1) → c1(+'(z0, z1))
+'(p(z0), z1) → c2(+'(z0, z1))
MINUS(0) → c3
MINUS(s(z0)) → c4(MINUS(z0))
MINUS(p(z0)) → c5(MINUS(z0))
*'(0, z0) → c6
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1))
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
+, minus, *
+', MINUS, *'
c, c1, c2, c3, c4, c5, c6, c7, c8
+'(0, z0) → c
*'(0, z0) → c6
MINUS(0) → c3
Tuples:
+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
+(p(z0), z1) → p(+(z0, z1))
minus(0) → 0
minus(s(z0)) → p(minus(z0))
minus(p(z0)) → s(minus(z0))
*(0, z0) → 0
*(s(z0), z1) → +(*(z0, z1), z1)
*(p(z0), z1) → +(*(z0, z1), minus(z1))
S tuples:
+'(s(z0), z1) → c1(+'(z0, z1))
+'(p(z0), z1) → c2(+'(z0, z1))
MINUS(s(z0)) → c4(MINUS(z0))
MINUS(p(z0)) → c5(MINUS(z0))
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1))
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
K tuples:none
+'(s(z0), z1) → c1(+'(z0, z1))
+'(p(z0), z1) → c2(+'(z0, z1))
MINUS(s(z0)) → c4(MINUS(z0))
MINUS(p(z0)) → c5(MINUS(z0))
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1))
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
+, minus, *
+', MINUS, *'
c1, c2, c4, c5, c7, c8
We considered the (Usable) Rules:none
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1))
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
The order we found is given by the following interpretation:
+'(s(z0), z1) → c1(+'(z0, z1))
+'(p(z0), z1) → c2(+'(z0, z1))
MINUS(s(z0)) → c4(MINUS(z0))
MINUS(p(z0)) → c5(MINUS(z0))
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1))
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
POL(*(x1, x2)) = 0
POL(*'(x1, x2)) = [2]x1
POL(+(x1, x2)) = 0
POL(+'(x1, x2)) = 0
POL(0) = 0
POL(MINUS(x1)) = [3]
POL(c1(x1)) = x1
POL(c2(x1)) = x1
POL(c4(x1)) = x1
POL(c5(x1)) = x1
POL(c7(x1, x2)) = x1 + x2
POL(c8(x1, x2, x3)) = x1 + x2 + x3
POL(minus(x1)) = 0
POL(p(x1)) = [2] + x1
POL(s(x1)) = [3] + x1
Tuples:
+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
+(p(z0), z1) → p(+(z0, z1))
minus(0) → 0
minus(s(z0)) → p(minus(z0))
minus(p(z0)) → s(minus(z0))
*(0, z0) → 0
*(s(z0), z1) → +(*(z0, z1), z1)
*(p(z0), z1) → +(*(z0, z1), minus(z1))
S tuples:
+'(s(z0), z1) → c1(+'(z0, z1))
+'(p(z0), z1) → c2(+'(z0, z1))
MINUS(s(z0)) → c4(MINUS(z0))
MINUS(p(z0)) → c5(MINUS(z0))
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1))
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
K tuples:
+'(s(z0), z1) → c1(+'(z0, z1))
+'(p(z0), z1) → c2(+'(z0, z1))
MINUS(s(z0)) → c4(MINUS(z0))
MINUS(p(z0)) → c5(MINUS(z0))
Defined Rule Symbols:
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1))
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
+, minus, *
+', MINUS, *'
c1, c2, c4, c5, c7, c8
We considered the (Usable) Rules:none
MINUS(s(z0)) → c4(MINUS(z0))
MINUS(p(z0)) → c5(MINUS(z0))
The order we found is given by the following interpretation:
+'(s(z0), z1) → c1(+'(z0, z1))
+'(p(z0), z1) → c2(+'(z0, z1))
MINUS(s(z0)) → c4(MINUS(z0))
MINUS(p(z0)) → c5(MINUS(z0))
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1))
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
POL(*(x1, x2)) = [2]x22 + [2]x12
POL(*'(x1, x2)) = [2]x1·x2
POL(+(x1, x2)) = [1] + x1 + [2]x2 + [2]x22 + x12
POL(+'(x1, x2)) = 0
POL(0) = [1]
POL(MINUS(x1)) = [2]x1
POL(c1(x1)) = x1
POL(c2(x1)) = x1
POL(c4(x1)) = x1
POL(c5(x1)) = x1
POL(c7(x1, x2)) = x1 + x2
POL(c8(x1, x2, x3)) = x1 + x2 + x3
POL(minus(x1)) = [1] + x1
POL(p(x1)) = [1] + x1
POL(s(x1)) = [2] + x1
Tuples:
+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
+(p(z0), z1) → p(+(z0, z1))
minus(0) → 0
minus(s(z0)) → p(minus(z0))
minus(p(z0)) → s(minus(z0))
*(0, z0) → 0
*(s(z0), z1) → +(*(z0, z1), z1)
*(p(z0), z1) → +(*(z0, z1), minus(z1))
S tuples:
+'(s(z0), z1) → c1(+'(z0, z1))
+'(p(z0), z1) → c2(+'(z0, z1))
MINUS(s(z0)) → c4(MINUS(z0))
MINUS(p(z0)) → c5(MINUS(z0))
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1))
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
K tuples:
+'(s(z0), z1) → c1(+'(z0, z1))
+'(p(z0), z1) → c2(+'(z0, z1))
Defined Rule Symbols:
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1))
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
MINUS(s(z0)) → c4(MINUS(z0))
MINUS(p(z0)) → c5(MINUS(z0))
+, minus, *
+', MINUS, *'
c1, c2, c4, c5, c7, c8
We considered the (Usable) Rules:
+'(s(z0), z1) → c1(+'(z0, z1))
+'(p(z0), z1) → c2(+'(z0, z1))
And the Tuples:
+(s(z0), z1) → s(+(z0, z1))
*(p(z0), z1) → +(*(z0, z1), minus(z1))
minus(0) → 0
*(s(z0), z1) → +(*(z0, z1), z1)
minus(p(z0)) → s(minus(z0))
*(0, z0) → 0
minus(s(z0)) → p(minus(z0))
+(p(z0), z1) → p(+(z0, z1))
+(0, z0) → z0
The order we found is given by the following interpretation:
+'(s(z0), z1) → c1(+'(z0, z1))
+'(p(z0), z1) → c2(+'(z0, z1))
MINUS(s(z0)) → c4(MINUS(z0))
MINUS(p(z0)) → c5(MINUS(z0))
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1))
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
POL(*(x1, x2)) = x1·x2
POL(*'(x1, x2)) = x12·x2
POL(+(x1, x2)) = x1 + x2
POL(+'(x1, x2)) = x1
POL(0) = 0
POL(MINUS(x1)) = 0
POL(c1(x1)) = x1
POL(c2(x1)) = x1
POL(c4(x1)) = x1
POL(c5(x1)) = x1
POL(c7(x1, x2)) = x1 + x2
POL(c8(x1, x2, x3)) = x1 + x2 + x3
POL(minus(x1)) = x1
POL(p(x1)) = [1] + x1
POL(s(x1)) = [1] + x1
Tuples:
+(0, z0) → z0
+(s(z0), z1) → s(+(z0, z1))
+(p(z0), z1) → p(+(z0, z1))
minus(0) → 0
minus(s(z0)) → p(minus(z0))
minus(p(z0)) → s(minus(z0))
*(0, z0) → 0
*(s(z0), z1) → +(*(z0, z1), z1)
*(p(z0), z1) → +(*(z0, z1), minus(z1))
S tuples:none
+'(s(z0), z1) → c1(+'(z0, z1))
+'(p(z0), z1) → c2(+'(z0, z1))
MINUS(s(z0)) → c4(MINUS(z0))
MINUS(p(z0)) → c5(MINUS(z0))
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1))
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
Defined Rule Symbols:
*'(s(z0), z1) → c7(+'(*(z0, z1), z1), *'(z0, z1))
*'(p(z0), z1) → c8(+'(*(z0, z1), minus(z1)), *'(z0, z1), MINUS(z1))
MINUS(s(z0)) → c4(MINUS(z0))
MINUS(p(z0)) → c5(MINUS(z0))
+'(s(z0), z1) → c1(+'(z0, z1))
+'(p(z0), z1) → c2(+'(z0, z1))
+, minus, *
+', MINUS, *'
c1, c2, c4, c5, c7, c8