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