YES(O(1), O(n^1)) 0.00/0.75 YES(O(1), O(n^1)) 0.00/0.76 0.00/0.76 0.00/0.76
0.00/0.76 0.00/0.760 CpxTRS0.00/0.76
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.76
↳2 CdtProblem0.00/0.76
↳3 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.76
↳4 CdtProblem0.00/0.76
↳5 CdtKnowledgeProof (⇔)0.00/0.76
↳6 BOUNDS(O(1), O(1))0.00/0.76
g(f(x), y) → f(h(x, y)) 0.00/0.76
h(x, y) → g(x, f(y))
Tuples:
g(f(z0), z1) → f(h(z0, z1)) 0.00/0.76
h(z0, z1) → g(z0, f(z1))
S tuples:
G(f(z0), z1) → c(H(z0, z1)) 0.00/0.76
H(z0, z1) → c1(G(z0, f(z1)))
K tuples:none
G(f(z0), z1) → c(H(z0, z1)) 0.00/0.76
H(z0, z1) → c1(G(z0, f(z1)))
g, h
G, H
c, c1
We considered the (Usable) Rules:none
G(f(z0), z1) → c(H(z0, z1))
The order we found is given by the following interpretation:
G(f(z0), z1) → c(H(z0, z1)) 0.00/0.76
H(z0, z1) → c1(G(z0, f(z1)))
POL(G(x1, x2)) = x1 0.00/0.76
POL(H(x1, x2)) = x1 0.00/0.76
POL(c(x1)) = x1 0.00/0.76
POL(c1(x1)) = x1 0.00/0.76
POL(f(x1)) = [1] + x1
Tuples:
g(f(z0), z1) → f(h(z0, z1)) 0.00/0.76
h(z0, z1) → g(z0, f(z1))
S tuples:
G(f(z0), z1) → c(H(z0, z1)) 0.00/0.76
H(z0, z1) → c1(G(z0, f(z1)))
K tuples:
H(z0, z1) → c1(G(z0, f(z1)))
Defined Rule Symbols:
G(f(z0), z1) → c(H(z0, z1))
g, h
G, H
c, c1
Now S is empty
H(z0, z1) → c1(G(z0, f(z1))) 0.00/0.76
G(f(z0), z1) → c(H(z0, z1))