YES(O(1), O(n^1)) 0.00/0.82 YES(O(1), O(n^1)) 0.00/0.84 0.00/0.84 0.00/0.84
0.00/0.84 0.00/0.840 CpxTRS0.00/0.84
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.84
↳2 CdtProblem0.00/0.84
↳3 CdtUnreachableProof (⇔)0.00/0.84
↳4 CdtProblem0.00/0.84
↳5 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/0.84
↳6 CdtProblem0.00/0.84
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.84
↳8 CdtProblem0.00/0.84
↳9 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.84
↳10 BOUNDS(O(1), O(1))0.00/0.84
c(c(c(y))) → c(c(a(y, 0))) 0.00/0.84
c(a(a(0, x), y)) → a(c(c(c(0))), y) 0.00/0.84
c(y) → y
Tuples:
c(c(c(z0))) → c(c(a(z0, 0))) 0.00/0.84
c(a(a(0, z0), z1)) → a(c(c(c(0))), z1) 0.00/0.84
c(z0) → z0
S tuples:
C(c(c(z0))) → c1(C(c(a(z0, 0))), C(a(z0, 0))) 0.00/0.84
C(a(a(0, z0), z1)) → c2(C(c(c(0))), C(c(0)), C(0))
K tuples:none
C(c(c(z0))) → c1(C(c(a(z0, 0))), C(a(z0, 0))) 0.00/0.84
C(a(a(0, z0), z1)) → c2(C(c(c(0))), C(c(0)), C(0))
c
C
c1, c2
C(c(c(z0))) → c1(C(c(a(z0, 0))), C(a(z0, 0)))
Tuples:
c(c(c(z0))) → c(c(a(z0, 0))) 0.00/0.84
c(a(a(0, z0), z1)) → a(c(c(c(0))), z1) 0.00/0.84
c(z0) → z0
S tuples:
C(a(a(0, z0), z1)) → c2(C(c(c(0))), C(c(0)), C(0))
K tuples:none
C(a(a(0, z0), z1)) → c2(C(c(c(0))), C(c(0)), C(0))
c
C
c2
Tuples:
c(c(c(z0))) → c(c(a(z0, 0))) 0.00/0.84
c(a(a(0, z0), z1)) → a(c(c(c(0))), z1) 0.00/0.84
c(z0) → z0
S tuples:
C(a(a(0, z0), z1)) → c2(C(c(c(0))), C(c(0)))
K tuples:none
C(a(a(0, z0), z1)) → c2(C(c(c(0))), C(c(0)))
c
C
c2
We considered the (Usable) Rules:
C(a(a(0, z0), z1)) → c2(C(c(c(0))), C(c(0)))
And the Tuples:
c(z0) → z0 0.00/0.84
c(a(a(0, z0), z1)) → a(c(c(c(0))), z1)
The order we found is given by the following interpretation:
C(a(a(0, z0), z1)) → c2(C(c(c(0))), C(c(0)))
POL(0) = 0 0.00/0.84
POL(C(x1)) = [5] + [4]x1 0.00/0.84
POL(a(x1, x2)) = [4] + x1 + x2 0.00/0.84
POL(c(x1)) = [1] + x1 0.00/0.84
POL(c2(x1, x2)) = x1 + x2
Tuples:
c(c(c(z0))) → c(c(a(z0, 0))) 0.00/0.84
c(a(a(0, z0), z1)) → a(c(c(c(0))), z1) 0.00/0.84
c(z0) → z0
S tuples:none
C(a(a(0, z0), z1)) → c2(C(c(c(0))), C(c(0)))
Defined Rule Symbols:
C(a(a(0, z0), z1)) → c2(C(c(c(0))), C(c(0)))
c
C
c2