YES(O(1), O(n^1)) 0.00/0.75 YES(O(1), O(n^1)) 0.00/0.77 0.00/0.77 0.00/0.77
0.00/0.77 0.00/0.770 CpxTRS0.00/0.77
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.77
↳2 CdtProblem0.00/0.77
↳3 CdtUnreachableProof (⇔)0.00/0.77
↳4 CdtProblem0.00/0.77
↳5 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/0.77
↳6 CdtProblem0.00/0.77
↳7 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))0.00/0.77
↳8 CdtProblem0.00/0.77
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.77
↳10 CdtProblem0.00/0.77
↳11 CdtKnowledgeProof (⇔)0.00/0.77
↳12 BOUNDS(O(1), O(1))0.00/0.77
f(f(x)) → f(c(f(x))) 0.00/0.77
f(f(x)) → f(d(f(x))) 0.00/0.77
g(c(x)) → x 0.00/0.77
g(d(x)) → x 0.00/0.77
g(c(h(0))) → g(d(1)) 0.00/0.77
g(c(1)) → g(d(h(0))) 0.00/0.77
g(h(x)) → g(x)
Tuples:
f(f(z0)) → f(c(f(z0))) 0.00/0.77
f(f(z0)) → f(d(f(z0))) 0.00/0.77
g(c(z0)) → z0 0.00/0.77
g(d(z0)) → z0 0.00/0.77
g(c(h(0))) → g(d(1)) 0.00/0.77
g(c(1)) → g(d(h(0))) 0.00/0.77
g(h(z0)) → g(z0)
S tuples:
F(f(z0)) → c1(F(c(f(z0))), F(z0)) 0.00/0.77
F(f(z0)) → c2(F(d(f(z0))), F(z0)) 0.00/0.77
G(c(h(0))) → c5(G(d(1))) 0.00/0.77
G(c(1)) → c6(G(d(h(0)))) 0.00/0.77
G(h(z0)) → c7(G(z0))
K tuples:none
F(f(z0)) → c1(F(c(f(z0))), F(z0)) 0.00/0.77
F(f(z0)) → c2(F(d(f(z0))), F(z0)) 0.00/0.77
G(c(h(0))) → c5(G(d(1))) 0.00/0.77
G(c(1)) → c6(G(d(h(0)))) 0.00/0.77
G(h(z0)) → c7(G(z0))
f, g
F, G
c1, c2, c5, c6, c7
F(f(z0)) → c1(F(c(f(z0))), F(z0)) 0.00/0.77
F(f(z0)) → c2(F(d(f(z0))), F(z0))
Tuples:
f(f(z0)) → f(c(f(z0))) 0.00/0.77
f(f(z0)) → f(d(f(z0))) 0.00/0.77
g(c(z0)) → z0 0.00/0.77
g(d(z0)) → z0 0.00/0.77
g(c(h(0))) → g(d(1)) 0.00/0.77
g(c(1)) → g(d(h(0))) 0.00/0.77
g(h(z0)) → g(z0)
S tuples:
G(c(h(0))) → c5(G(d(1))) 0.00/0.77
G(c(1)) → c6(G(d(h(0)))) 0.00/0.77
G(h(z0)) → c7(G(z0))
K tuples:none
G(c(h(0))) → c5(G(d(1))) 0.00/0.77
G(c(1)) → c6(G(d(h(0)))) 0.00/0.77
G(h(z0)) → c7(G(z0))
f, g
G
c5, c6, c7
Tuples:
f(f(z0)) → f(c(f(z0))) 0.00/0.77
f(f(z0)) → f(d(f(z0))) 0.00/0.77
g(c(z0)) → z0 0.00/0.77
g(d(z0)) → z0 0.00/0.77
g(c(h(0))) → g(d(1)) 0.00/0.77
g(c(1)) → g(d(h(0))) 0.00/0.77
g(h(z0)) → g(z0)
S tuples:
G(h(z0)) → c7(G(z0)) 0.00/0.77
G(c(h(0))) → c5 0.00/0.77
G(c(1)) → c6
K tuples:none
G(h(z0)) → c7(G(z0)) 0.00/0.77
G(c(h(0))) → c5 0.00/0.77
G(c(1)) → c6
f, g
G
c7, c5, c6
G(c(h(0))) → c5 0.00/0.77
G(c(1)) → c6
Tuples:
f(f(z0)) → f(c(f(z0))) 0.00/0.77
f(f(z0)) → f(d(f(z0))) 0.00/0.77
g(c(z0)) → z0 0.00/0.77
g(d(z0)) → z0 0.00/0.77
g(c(h(0))) → g(d(1)) 0.00/0.77
g(c(1)) → g(d(h(0))) 0.00/0.77
g(h(z0)) → g(z0)
S tuples:
G(h(z0)) → c7(G(z0)) 0.00/0.77
G(c(h(0))) → c5 0.00/0.77
G(c(1)) → c6
K tuples:none
G(h(z0)) → c7(G(z0)) 0.00/0.77
G(c(h(0))) → c5 0.00/0.77
G(c(1)) → c6
f, g
G
c7, c5, c6
We considered the (Usable) Rules:none
G(h(z0)) → c7(G(z0))
The order we found is given by the following interpretation:
G(h(z0)) → c7(G(z0)) 0.00/0.77
G(c(h(0))) → c5 0.00/0.77
G(c(1)) → c6
POL(0) = [1] 0.00/0.77
POL(1) = [1] 0.00/0.77
POL(G(x1)) = [2]x1 0.00/0.77
POL(c(x1)) = 0 0.00/0.77
POL(c5) = 0 0.00/0.77
POL(c6) = 0 0.00/0.77
POL(c7(x1)) = x1 0.00/0.77
POL(h(x1)) = [1] + x1
Tuples:
f(f(z0)) → f(c(f(z0))) 0.00/0.77
f(f(z0)) → f(d(f(z0))) 0.00/0.77
g(c(z0)) → z0 0.00/0.77
g(d(z0)) → z0 0.00/0.77
g(c(h(0))) → g(d(1)) 0.00/0.77
g(c(1)) → g(d(h(0))) 0.00/0.77
g(h(z0)) → g(z0)
S tuples:
G(h(z0)) → c7(G(z0)) 0.00/0.77
G(c(h(0))) → c5 0.00/0.77
G(c(1)) → c6
K tuples:
G(c(h(0))) → c5 0.00/0.77
G(c(1)) → c6
Defined Rule Symbols:
G(h(z0)) → c7(G(z0))
f, g
G
c7, c5, c6
Now S is empty
G(c(h(0))) → c5 0.00/0.77
G(c(1)) → c6