YES(O(1), O(n^1)) 0.00/0.71 YES(O(1), O(n^1)) 0.00/0.73 0.00/0.73 0.00/0.73
0.00/0.73 0.00/0.730 CpxTRS0.00/0.73
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.73
↳2 CdtProblem0.00/0.73
↳3 CdtLeafRemovalProof (ComplexityIfPolyImplication)0.00/0.73
↳4 CdtProblem0.00/0.73
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.73
↳6 CdtProblem0.00/0.73
↳7 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.73
↳8 BOUNDS(O(1), O(1))0.00/0.73
f(c(X, s(Y))) → f(c(s(X), Y)) 0.00/0.73
g(c(s(X), Y)) → f(c(X, s(Y)))
Tuples:
f(c(z0, s(z1))) → f(c(s(z0), z1)) 0.00/0.73
g(c(s(z0), z1)) → f(c(z0, s(z1)))
S tuples:
F(c(z0, s(z1))) → c1(F(c(s(z0), z1))) 0.00/0.73
G(c(s(z0), z1)) → c2(F(c(z0, s(z1))))
K tuples:none
F(c(z0, s(z1))) → c1(F(c(s(z0), z1))) 0.00/0.73
G(c(s(z0), z1)) → c2(F(c(z0, s(z1))))
f, g
F, G
c1, c2
G(c(s(z0), z1)) → c2(F(c(z0, s(z1))))
Tuples:
f(c(z0, s(z1))) → f(c(s(z0), z1)) 0.00/0.73
g(c(s(z0), z1)) → f(c(z0, s(z1)))
S tuples:
F(c(z0, s(z1))) → c1(F(c(s(z0), z1)))
K tuples:none
F(c(z0, s(z1))) → c1(F(c(s(z0), z1)))
f, g
F
c1
We considered the (Usable) Rules:none
F(c(z0, s(z1))) → c1(F(c(s(z0), z1)))
The order we found is given by the following interpretation:
F(c(z0, s(z1))) → c1(F(c(s(z0), z1)))
POL(F(x1)) = x1 0.00/0.73
POL(c(x1, x2)) = x2 0.00/0.73
POL(c1(x1)) = x1 0.00/0.73
POL(s(x1)) = [2] + x1
Tuples:
f(c(z0, s(z1))) → f(c(s(z0), z1)) 0.00/0.73
g(c(s(z0), z1)) → f(c(z0, s(z1)))
S tuples:none
F(c(z0, s(z1))) → c1(F(c(s(z0), z1)))
Defined Rule Symbols:
F(c(z0, s(z1))) → c1(F(c(s(z0), z1)))
f, g
F
c1