YES(O(1), O(n^1)) 0.00/0.73 YES(O(1), O(n^1)) 0.00/0.74 0.00/0.74 0.00/0.74
0.00/0.74 0.00/0.740 CpxTRS0.00/0.74
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.74
↳2 CdtProblem0.00/0.74
↳3 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.74
↳4 CdtProblem0.00/0.74
↳5 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.74
↳6 BOUNDS(O(1), O(1))0.00/0.74
p(m, n, s(r)) → p(m, r, n) 0.00/0.74
p(m, s(n), 0) → p(0, n, m) 0.00/0.74
p(m, 0, 0) → m
Tuples:
p(z0, z1, s(z2)) → p(z0, z2, z1) 0.00/0.74
p(z0, s(z1), 0) → p(0, z1, z0) 0.00/0.74
p(z0, 0, 0) → z0
S tuples:
P(z0, z1, s(z2)) → c(P(z0, z2, z1)) 0.00/0.74
P(z0, s(z1), 0) → c1(P(0, z1, z0))
K tuples:none
P(z0, z1, s(z2)) → c(P(z0, z2, z1)) 0.00/0.74
P(z0, s(z1), 0) → c1(P(0, z1, z0))
p
P
c, c1
We considered the (Usable) Rules:none
P(z0, z1, s(z2)) → c(P(z0, z2, z1)) 0.00/0.74
P(z0, s(z1), 0) → c1(P(0, z1, z0))
The order we found is given by the following interpretation:
P(z0, z1, s(z2)) → c(P(z0, z2, z1)) 0.00/0.74
P(z0, s(z1), 0) → c1(P(0, z1, z0))
POL(0) = 0 0.00/0.74
POL(P(x1, x2, x3)) = x1 + x2 + x3 0.00/0.74
POL(c(x1)) = x1 0.00/0.74
POL(c1(x1)) = x1 0.00/0.74
POL(s(x1)) = [1] + x1
Tuples:
p(z0, z1, s(z2)) → p(z0, z2, z1) 0.00/0.74
p(z0, s(z1), 0) → p(0, z1, z0) 0.00/0.74
p(z0, 0, 0) → z0
S tuples:none
P(z0, z1, s(z2)) → c(P(z0, z2, z1)) 0.00/0.74
P(z0, s(z1), 0) → c1(P(0, z1, z0))
Defined Rule Symbols:
P(z0, z1, s(z2)) → c(P(z0, z2, z1)) 0.00/0.74
P(z0, s(z1), 0) → c1(P(0, z1, z0))
p
P
c, c1