YES(O(1), O(n^1)) 3.04/1.26 YES(O(1), O(n^1)) 3.04/1.28 3.04/1.28 3.04/1.28
3.04/1.28 3.04/1.280 CpxTRS3.04/1.28
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))3.04/1.28
↳2 CdtProblem3.04/1.28
↳3 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))3.04/1.28
↳4 CdtProblem3.04/1.28
↳5 CdtInstantiationProof (BOTH BOUNDS(ID, ID))3.04/1.28
↳6 CdtProblem3.04/1.28
↳7 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))3.04/1.28
↳8 CdtProblem3.04/1.28
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))3.04/1.28
↳10 CdtProblem3.04/1.28
↳11 SIsEmptyProof (BOTH BOUNDS(ID, ID))3.04/1.28
↳12 BOUNDS(O(1), O(1))3.04/1.28
f(x, c(y)) → f(x, s(f(y, y))) 3.04/1.28
f(s(x), y) → f(x, s(c(y)))
Tuples:
f(z0, c(z1)) → f(z0, s(f(z1, z1))) 3.04/1.28
f(s(z0), z1) → f(z0, s(c(z1)))
S tuples:
F(z0, c(z1)) → c1(F(z0, s(f(z1, z1))), F(z1, z1)) 3.04/1.28
F(s(z0), z1) → c2(F(z0, s(c(z1))))
K tuples:none
F(z0, c(z1)) → c1(F(z0, s(f(z1, z1))), F(z1, z1)) 3.04/1.28
F(s(z0), z1) → c2(F(z0, s(c(z1))))
f
F
c1, c2
We considered the (Usable) Rules:
F(z0, c(z1)) → c1(F(z0, s(f(z1, z1))), F(z1, z1))
And the Tuples:
f(z0, c(z1)) → f(z0, s(f(z1, z1))) 3.04/1.28
f(s(z0), z1) → f(z0, s(c(z1)))
The order we found is given by the following interpretation:
F(z0, c(z1)) → c1(F(z0, s(f(z1, z1))), F(z1, z1)) 3.04/1.28
F(s(z0), z1) → c2(F(z0, s(c(z1))))
POL(F(x1, x2)) = [2]x2 3.04/1.28
POL(c(x1)) = [1] + x1 3.04/1.28
POL(c1(x1, x2)) = x1 + x2 3.04/1.28
POL(c2(x1)) = x1 3.04/1.28
POL(f(x1, x2)) = [5] + x1 3.04/1.28
POL(s(x1)) = 0
Tuples:
f(z0, c(z1)) → f(z0, s(f(z1, z1))) 3.04/1.28
f(s(z0), z1) → f(z0, s(c(z1)))
S tuples:
F(z0, c(z1)) → c1(F(z0, s(f(z1, z1))), F(z1, z1)) 3.04/1.28
F(s(z0), z1) → c2(F(z0, s(c(z1))))
K tuples:
F(s(z0), z1) → c2(F(z0, s(c(z1))))
Defined Rule Symbols:
F(z0, c(z1)) → c1(F(z0, s(f(z1, z1))), F(z1, z1))
f
F
c1, c2
F(c(z1), c(z1)) → c1(F(c(z1), s(f(z1, z1))), F(z1, z1))
Tuples:
f(z0, c(z1)) → f(z0, s(f(z1, z1))) 3.04/1.28
f(s(z0), z1) → f(z0, s(c(z1)))
S tuples:
F(s(z0), z1) → c2(F(z0, s(c(z1)))) 3.04/1.28
F(c(z1), c(z1)) → c1(F(c(z1), s(f(z1, z1))), F(z1, z1))
K tuples:
F(s(z0), z1) → c2(F(z0, s(c(z1))))
Defined Rule Symbols:
F(c(z1), c(z1)) → c1(F(c(z1), s(f(z1, z1))), F(z1, z1))
f
F
c2, c1
Tuples:
f(z0, c(z1)) → f(z0, s(f(z1, z1))) 3.04/1.28
f(s(z0), z1) → f(z0, s(c(z1)))
S tuples:
F(s(z0), z1) → c2(F(z0, s(c(z1)))) 3.04/1.28
F(c(z1), c(z1)) → c1(F(z1, z1))
K tuples:
F(s(z0), z1) → c2(F(z0, s(c(z1))))
Defined Rule Symbols:
F(c(z1), c(z1)) → c1(F(z1, z1))
f
F
c2, c1
We considered the (Usable) Rules:none
F(s(z0), z1) → c2(F(z0, s(c(z1))))
The order we found is given by the following interpretation:
F(s(z0), z1) → c2(F(z0, s(c(z1)))) 3.04/1.28
F(c(z1), c(z1)) → c1(F(z1, z1))
POL(F(x1, x2)) = [4]x1 3.04/1.28
POL(c(x1)) = [1] + x1 3.04/1.28
POL(c1(x1)) = x1 3.04/1.28
POL(c2(x1)) = x1 3.04/1.28
POL(s(x1)) = [4] + x1
Tuples:
f(z0, c(z1)) → f(z0, s(f(z1, z1))) 3.04/1.28
f(s(z0), z1) → f(z0, s(c(z1)))
S tuples:none
F(s(z0), z1) → c2(F(z0, s(c(z1)))) 3.04/1.28
F(c(z1), c(z1)) → c1(F(z1, z1))
Defined Rule Symbols:
F(c(z1), c(z1)) → c1(F(z1, z1)) 3.04/1.28
F(s(z0), z1) → c2(F(z0, s(c(z1))))
f
F
c2, c1