MAYBE 5.48/2.03 MAYBE 5.48/2.06 5.48/2.06 5.48/2.06
5.48/2.06 5.48/2.060 CpxTRS5.48/2.06
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))5.48/2.06
↳2 CdtProblem5.48/2.06
↳3 CdtLeafRemovalProof (ComplexityIfPolyImplication)5.48/2.06
↳4 CdtProblem5.48/2.06
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))5.48/2.06
↳6 CdtProblem5.48/2.06
↳7 CdtNarrowingProof (BOTH BOUNDS(ID, ID))5.48/2.06
↳8 CdtProblem5.48/2.06
↳9 CdtNarrowingProof (BOTH BOUNDS(ID, ID))5.48/2.06
↳10 CdtProblem5.48/2.06
↳11 CdtRewritingProof (BOTH BOUNDS(ID, ID))5.48/2.06
↳12 CdtProblem5.48/2.06
↳13 CdtRewritingProof (BOTH BOUNDS(ID, ID))5.48/2.06
↳14 CdtProblem5.48/2.06
nesteql(Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
nesteql(Cons(x, xs)) → nesteql(eql(Cons(x, xs))) 5.48/2.06
eql(Nil) → Nil 5.48/2.06
eql(Cons(x, xs)) → eql(Cons(x, xs)) 5.48/2.06
number17(n) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
goal(x) → nesteql(x)
Tuples:
nesteql(Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
nesteql(Cons(z0, z1)) → nesteql(eql(Cons(z0, z1))) 5.48/2.06
eql(Nil) → Nil 5.48/2.06
eql(Cons(z0, z1)) → eql(Cons(z0, z1)) 5.48/2.06
number17(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
goal(z0) → nesteql(z0)
S tuples:
NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1))) 5.48/2.06
EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1))) 5.48/2.06
GOAL(z0) → c5(NESTEQL(z0))
K tuples:none
NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1))) 5.48/2.06
EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1))) 5.48/2.06
GOAL(z0) → c5(NESTEQL(z0))
nesteql, eql, number17, goal
NESTEQL, EQL, GOAL
c1, c3, c5
GOAL(z0) → c5(NESTEQL(z0))
Tuples:
nesteql(Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
nesteql(Cons(z0, z1)) → nesteql(eql(Cons(z0, z1))) 5.48/2.06
eql(Nil) → Nil 5.48/2.06
eql(Cons(z0, z1)) → eql(Cons(z0, z1)) 5.48/2.06
number17(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
goal(z0) → nesteql(z0)
S tuples:
NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1))) 5.48/2.06
EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1)))
K tuples:none
NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1))) 5.48/2.06
EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1)))
nesteql, eql, number17, goal
NESTEQL, EQL
c1, c3
We considered the (Usable) Rules:
NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1)))
And the Tuples:
eql(Cons(z0, z1)) → eql(Cons(z0, z1))
The order we found is given by the following interpretation:
NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1))) 5.48/2.06
EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1)))
POL(Cons(x1, x2)) = [4] 5.48/2.06
POL(EQL(x1)) = [1] 5.48/2.06
POL(NESTEQL(x1)) = [4]x1 5.48/2.06
POL(c1(x1, x2)) = x1 + x2 5.48/2.06
POL(c3(x1)) = x1 5.48/2.06
POL(eql(x1)) = 0
Tuples:
nesteql(Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
nesteql(Cons(z0, z1)) → nesteql(eql(Cons(z0, z1))) 5.48/2.06
eql(Nil) → Nil 5.48/2.06
eql(Cons(z0, z1)) → eql(Cons(z0, z1)) 5.48/2.06
number17(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
goal(z0) → nesteql(z0)
S tuples:
NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1))) 5.48/2.06
EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1)))
K tuples:
EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1)))
Defined Rule Symbols:
NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1)))
nesteql, eql, number17, goal
NESTEQL, EQL
c1, c3
NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1)))
Tuples:
nesteql(Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
nesteql(Cons(z0, z1)) → nesteql(eql(Cons(z0, z1))) 5.48/2.06
eql(Nil) → Nil 5.48/2.06
eql(Cons(z0, z1)) → eql(Cons(z0, z1)) 5.48/2.06
number17(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
goal(z0) → nesteql(z0)
S tuples:
EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1))) 5.48/2.06
NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1)))
K tuples:
EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1)))
Defined Rule Symbols:
NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1)))
nesteql, eql, number17, goal
EQL, NESTEQL
c3, c1
NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1)))
Tuples:
nesteql(Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
nesteql(Cons(z0, z1)) → nesteql(eql(Cons(z0, z1))) 5.48/2.06
eql(Nil) → Nil 5.48/2.06
eql(Cons(z0, z1)) → eql(Cons(z0, z1)) 5.48/2.06
number17(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
goal(z0) → nesteql(z0)
S tuples:
EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1))) 5.48/2.06
NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1)))
K tuples:
EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1)))
Defined Rule Symbols:
NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1)))
nesteql, eql, number17, goal
EQL, NESTEQL
c3, c1
Tuples:
nesteql(Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
nesteql(Cons(z0, z1)) → nesteql(eql(Cons(z0, z1))) 5.48/2.06
eql(Nil) → Nil 5.48/2.06
eql(Cons(z0, z1)) → eql(Cons(z0, z1)) 5.48/2.06
number17(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
goal(z0) → nesteql(z0)
S tuples:
EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1))) 5.48/2.06
NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1)))
K tuples:
EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1)))
Defined Rule Symbols:
NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1)))
nesteql, eql, number17, goal
EQL, NESTEQL
c3, c1
Tuples:
nesteql(Nil) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
nesteql(Cons(z0, z1)) → nesteql(eql(Cons(z0, z1))) 5.48/2.06
eql(Nil) → Nil 5.48/2.06
eql(Cons(z0, z1)) → eql(Cons(z0, z1)) 5.48/2.06
number17(z0) → Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Cons(Nil, Nil))))))))))))))))) 5.48/2.06
goal(z0) → nesteql(z0)
S tuples:
EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1))) 5.48/2.06
NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1)))
K tuples:
EQL(Cons(z0, z1)) → c3(EQL(Cons(z0, z1)))
Defined Rule Symbols:
NESTEQL(Cons(z0, z1)) → c1(NESTEQL(eql(Cons(z0, z1))), EQL(Cons(z0, z1)))
nesteql, eql, number17, goal
EQL, NESTEQL
c3, c1