YES(O(1), O(n^1)) 0.00/0.73 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
add0(x', Cons(x, xs)) → add0(Cons(Cons(Nil, Nil), x'), xs) 0.00/0.75
notEmpty(Cons(x, xs)) → True 0.00/0.75
notEmpty(Nil) → False 0.00/0.75
add0(x, Nil) → x 0.00/0.75
goal(x, y) → add0(x, y)
Tuples:
add0(z0, Cons(z1, z2)) → add0(Cons(Cons(Nil, Nil), z0), z2) 0.00/0.75
add0(z0, Nil) → z0 0.00/0.75
notEmpty(Cons(z0, z1)) → True 0.00/0.75
notEmpty(Nil) → False 0.00/0.75
goal(z0, z1) → add0(z0, z1)
S tuples:
ADD0(z0, Cons(z1, z2)) → c(ADD0(Cons(Cons(Nil, Nil), z0), z2)) 0.00/0.75
GOAL(z0, z1) → c4(ADD0(z0, z1))
K tuples:none
ADD0(z0, Cons(z1, z2)) → c(ADD0(Cons(Cons(Nil, Nil), z0), z2)) 0.00/0.75
GOAL(z0, z1) → c4(ADD0(z0, z1))
add0, notEmpty, goal
ADD0, GOAL
c, c4
GOAL(z0, z1) → c4(ADD0(z0, z1))
Tuples:
add0(z0, Cons(z1, z2)) → add0(Cons(Cons(Nil, Nil), z0), z2) 0.00/0.75
add0(z0, Nil) → z0 0.00/0.75
notEmpty(Cons(z0, z1)) → True 0.00/0.75
notEmpty(Nil) → False 0.00/0.75
goal(z0, z1) → add0(z0, z1)
S tuples:
ADD0(z0, Cons(z1, z2)) → c(ADD0(Cons(Cons(Nil, Nil), z0), z2))
K tuples:none
ADD0(z0, Cons(z1, z2)) → c(ADD0(Cons(Cons(Nil, Nil), z0), z2))
add0, notEmpty, goal
ADD0
c
We considered the (Usable) Rules:none
ADD0(z0, Cons(z1, z2)) → c(ADD0(Cons(Cons(Nil, Nil), z0), z2))
The order we found is given by the following interpretation:
ADD0(z0, Cons(z1, z2)) → c(ADD0(Cons(Cons(Nil, Nil), z0), z2))
POL(ADD0(x1, x2)) = x2 0.00/0.75
POL(Cons(x1, x2)) = [1] + x2 0.00/0.75
POL(Nil) = 0 0.00/0.75
POL(c(x1)) = x1
Tuples:
add0(z0, Cons(z1, z2)) → add0(Cons(Cons(Nil, Nil), z0), z2) 0.00/0.75
add0(z0, Nil) → z0 0.00/0.75
notEmpty(Cons(z0, z1)) → True 0.00/0.75
notEmpty(Nil) → False 0.00/0.75
goal(z0, z1) → add0(z0, z1)
S tuples:none
ADD0(z0, Cons(z1, z2)) → c(ADD0(Cons(Cons(Nil, Nil), z0), z2))
Defined Rule Symbols:
ADD0(z0, Cons(z1, z2)) → c(ADD0(Cons(Cons(Nil, Nil), z0), z2))
add0, notEmpty, goal
ADD0
c