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