YES(O(1), O(n^1)) 2.46/1.08 YES(O(1), O(n^1)) 2.46/1.10 2.46/1.10 2.46/1.10
2.46/1.10 2.46/1.100 CpxTRS2.46/1.10
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))2.46/1.10
↳2 CdtProblem2.46/1.10
↳3 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))2.46/1.10
↳4 CdtProblem2.46/1.10
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))2.46/1.10
↳6 CdtProblem2.46/1.10
↳7 SIsEmptyProof (BOTH BOUNDS(ID, ID))2.46/1.10
↳8 BOUNDS(O(1), O(1))2.46/1.10
ackin(s(X), s(Y)) → u21(ackin(s(X), Y), X) 2.46/1.10
u21(ackout(X), Y) → u22(ackin(Y, X))
Tuples:
ackin(s(z0), s(z1)) → u21(ackin(s(z0), z1), z0) 2.46/1.10
u21(ackout(z0), z1) → u22(ackin(z1, z0))
S tuples:
ACKIN(s(z0), s(z1)) → c(U21(ackin(s(z0), z1), z0), ACKIN(s(z0), z1)) 2.46/1.10
U21(ackout(z0), z1) → c1(ACKIN(z1, z0))
K tuples:none
ACKIN(s(z0), s(z1)) → c(U21(ackin(s(z0), z1), z0), ACKIN(s(z0), z1)) 2.46/1.10
U21(ackout(z0), z1) → c1(ACKIN(z1, z0))
ackin, u21
ACKIN, U21
c, c1
We considered the (Usable) Rules:
U21(ackout(z0), z1) → c1(ACKIN(z1, z0))
And the Tuples:
ackin(s(z0), s(z1)) → u21(ackin(s(z0), z1), z0) 2.46/1.10
u21(ackout(z0), z1) → u22(ackin(z1, z0))
The order we found is given by the following interpretation:
ACKIN(s(z0), s(z1)) → c(U21(ackin(s(z0), z1), z0), ACKIN(s(z0), z1)) 2.46/1.10
U21(ackout(z0), z1) → c1(ACKIN(z1, z0))
POL(ACKIN(x1, x2)) = 0 2.46/1.10
POL(U21(x1, x2)) = x1 2.46/1.10
POL(ackin(x1, x2)) = 0 2.46/1.10
POL(ackout(x1)) = [1] 2.46/1.10
POL(c(x1, x2)) = x1 + x2 2.46/1.10
POL(c1(x1)) = x1 2.46/1.10
POL(s(x1)) = 0 2.46/1.10
POL(u21(x1, x2)) = 0 2.46/1.10
POL(u22(x1)) = 0
Tuples:
ackin(s(z0), s(z1)) → u21(ackin(s(z0), z1), z0) 2.46/1.10
u21(ackout(z0), z1) → u22(ackin(z1, z0))
S tuples:
ACKIN(s(z0), s(z1)) → c(U21(ackin(s(z0), z1), z0), ACKIN(s(z0), z1)) 2.46/1.10
U21(ackout(z0), z1) → c1(ACKIN(z1, z0))
K tuples:
ACKIN(s(z0), s(z1)) → c(U21(ackin(s(z0), z1), z0), ACKIN(s(z0), z1))
Defined Rule Symbols:
U21(ackout(z0), z1) → c1(ACKIN(z1, z0))
ackin, u21
ACKIN, U21
c, c1
We considered the (Usable) Rules:
ACKIN(s(z0), s(z1)) → c(U21(ackin(s(z0), z1), z0), ACKIN(s(z0), z1))
And the Tuples:
ackin(s(z0), s(z1)) → u21(ackin(s(z0), z1), z0) 2.46/1.10
u21(ackout(z0), z1) → u22(ackin(z1, z0))
The order we found is given by the following interpretation:
ACKIN(s(z0), s(z1)) → c(U21(ackin(s(z0), z1), z0), ACKIN(s(z0), z1)) 2.46/1.10
U21(ackout(z0), z1) → c1(ACKIN(z1, z0))
POL(ACKIN(x1, x2)) = [3] + [2]x2 2.46/1.10
POL(U21(x1, x2)) = [1] + [2]x1 2.46/1.10
POL(ackin(x1, x2)) = 0 2.46/1.10
POL(ackout(x1)) = [3] + x1 2.46/1.10
POL(c(x1, x2)) = x1 + x2 2.46/1.10
POL(c1(x1)) = x1 2.46/1.10
POL(s(x1)) = [1] + x1 2.46/1.10
POL(u21(x1, x2)) = [4]x1 2.46/1.10
POL(u22(x1)) = [2]
Tuples:
ackin(s(z0), s(z1)) → u21(ackin(s(z0), z1), z0) 2.46/1.10
u21(ackout(z0), z1) → u22(ackin(z1, z0))
S tuples:none
ACKIN(s(z0), s(z1)) → c(U21(ackin(s(z0), z1), z0), ACKIN(s(z0), z1)) 2.46/1.10
U21(ackout(z0), z1) → c1(ACKIN(z1, z0))
Defined Rule Symbols:
U21(ackout(z0), z1) → c1(ACKIN(z1, z0)) 2.46/1.10
ACKIN(s(z0), s(z1)) → c(U21(ackin(s(z0), z1), z0), ACKIN(s(z0), z1))
ackin, u21
ACKIN, U21
c, c1