YES(O(1), O(n^1)) 0.00/0.74 YES(O(1), O(n^1)) 0.00/0.75 0.00/0.75 0.00/0.75
0.00/0.75 0.00/0.750 CpxTRS0.00/0.75
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.75
↳2 CdtProblem0.00/0.75
↳3 CdtLeafRemovalProof (ComplexityIfPolyImplication)0.00/0.75
↳4 CdtProblem0.00/0.75
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.75
↳6 CdtProblem0.00/0.75
↳7 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.75
↳8 BOUNDS(O(1), O(1))0.00/0.75
anchored(Cons(x, xs), y) → anchored(xs, Cons(Cons(Nil, Nil), y)) 0.00/0.75
anchored(Nil, y) → y 0.00/0.75
goal(x, y) → anchored(x, y)
Tuples:
anchored(Cons(z0, z1), z2) → anchored(z1, Cons(Cons(Nil, Nil), z2)) 0.00/0.75
anchored(Nil, z0) → z0 0.00/0.75
goal(z0, z1) → anchored(z0, z1)
S tuples:
ANCHORED(Cons(z0, z1), z2) → c(ANCHORED(z1, Cons(Cons(Nil, Nil), z2))) 0.00/0.75
GOAL(z0, z1) → c2(ANCHORED(z0, z1))
K tuples:none
ANCHORED(Cons(z0, z1), z2) → c(ANCHORED(z1, Cons(Cons(Nil, Nil), z2))) 0.00/0.75
GOAL(z0, z1) → c2(ANCHORED(z0, z1))
anchored, goal
ANCHORED, GOAL
c, c2
GOAL(z0, z1) → c2(ANCHORED(z0, z1))
Tuples:
anchored(Cons(z0, z1), z2) → anchored(z1, Cons(Cons(Nil, Nil), z2)) 0.00/0.75
anchored(Nil, z0) → z0 0.00/0.75
goal(z0, z1) → anchored(z0, z1)
S tuples:
ANCHORED(Cons(z0, z1), z2) → c(ANCHORED(z1, Cons(Cons(Nil, Nil), z2)))
K tuples:none
ANCHORED(Cons(z0, z1), z2) → c(ANCHORED(z1, Cons(Cons(Nil, Nil), z2)))
anchored, goal
ANCHORED
c
We considered the (Usable) Rules:none
ANCHORED(Cons(z0, z1), z2) → c(ANCHORED(z1, Cons(Cons(Nil, Nil), z2)))
The order we found is given by the following interpretation:
ANCHORED(Cons(z0, z1), z2) → c(ANCHORED(z1, Cons(Cons(Nil, Nil), z2)))
POL(ANCHORED(x1, x2)) = [4]x1 + [3]x2 0.00/0.75
POL(Cons(x1, x2)) = [4] + x2 0.00/0.75
POL(Nil) = 0 0.00/0.75
POL(c(x1)) = x1
Tuples:
anchored(Cons(z0, z1), z2) → anchored(z1, Cons(Cons(Nil, Nil), z2)) 0.00/0.75
anchored(Nil, z0) → z0 0.00/0.75
goal(z0, z1) → anchored(z0, z1)
S tuples:none
ANCHORED(Cons(z0, z1), z2) → c(ANCHORED(z1, Cons(Cons(Nil, Nil), z2)))
Defined Rule Symbols:
ANCHORED(Cons(z0, z1), z2) → c(ANCHORED(z1, Cons(Cons(Nil, Nil), z2)))
anchored, goal
ANCHORED
c