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 CdtLeafRemovalProof (ComplexityIfPolyImplication)0.00/0.71
↳4 CdtProblem0.00/0.71
↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.71
↳6 CdtProblem0.00/0.71
↳7 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.71
↳8 BOUNDS(O(1), O(1))0.00/0.71
append(Cons(x, xs), ys) → Cons(x, append(xs, ys)) 0.00/0.71
append(Nil, ys) → ys 0.00/0.71
goal(x, y) → append(x, y)
Tuples:
append(Cons(z0, z1), z2) → Cons(z0, append(z1, z2)) 0.00/0.71
append(Nil, z0) → z0 0.00/0.71
goal(z0, z1) → append(z0, z1)
S tuples:
APPEND(Cons(z0, z1), z2) → c(APPEND(z1, z2)) 0.00/0.71
GOAL(z0, z1) → c2(APPEND(z0, z1))
K tuples:none
APPEND(Cons(z0, z1), z2) → c(APPEND(z1, z2)) 0.00/0.71
GOAL(z0, z1) → c2(APPEND(z0, z1))
append, goal
APPEND, GOAL
c, c2
GOAL(z0, z1) → c2(APPEND(z0, z1))
Tuples:
append(Cons(z0, z1), z2) → Cons(z0, append(z1, z2)) 0.00/0.71
append(Nil, z0) → z0 0.00/0.71
goal(z0, z1) → append(z0, z1)
S tuples:
APPEND(Cons(z0, z1), z2) → c(APPEND(z1, z2))
K tuples:none
APPEND(Cons(z0, z1), z2) → c(APPEND(z1, z2))
append, goal
APPEND
c
We considered the (Usable) Rules:none
APPEND(Cons(z0, z1), z2) → c(APPEND(z1, z2))
The order we found is given by the following interpretation:
APPEND(Cons(z0, z1), z2) → c(APPEND(z1, z2))
POL(APPEND(x1, x2)) = [3]x1 0.00/0.71
POL(Cons(x1, x2)) = [1] + x2 0.00/0.71
POL(c(x1)) = x1
Tuples:
append(Cons(z0, z1), z2) → Cons(z0, append(z1, z2)) 0.00/0.71
append(Nil, z0) → z0 0.00/0.71
goal(z0, z1) → append(z0, z1)
S tuples:none
APPEND(Cons(z0, z1), z2) → c(APPEND(z1, z2))
Defined Rule Symbols:
APPEND(Cons(z0, z1), z2) → c(APPEND(z1, z2))
append, goal
APPEND
c