YES(O(1), O(1)) 0.00/0.54 YES(O(1), O(1)) 0.00/0.55 0.00/0.55 0.00/0.55
0.00/0.55 0.00/0.550 CpxTRS0.00/0.55
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.55
↳2 CdtProblem0.00/0.55
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/0.55
↳4 CdtProblem0.00/0.55
↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))0.00/0.55
↳6 CdtProblem0.00/0.55
↳7 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.55
↳8 BOUNDS(O(1), O(1))0.00/0.55
terms(N) → cons(recip(sqr(N))) 0.00/0.55
sqr(0) → 0 0.00/0.55
sqr(s) → s 0.00/0.55
dbl(0) → 0 0.00/0.55
dbl(s) → s 0.00/0.55
add(0, X) → X 0.00/0.55
add(s, Y) → s 0.00/0.55
first(0, X) → nil 0.00/0.55
first(s, cons(Y)) → cons(Y)
Tuples:
terms(z0) → cons(recip(sqr(z0))) 0.00/0.55
sqr(0) → 0 0.00/0.55
sqr(s) → s 0.00/0.55
dbl(0) → 0 0.00/0.55
dbl(s) → s 0.00/0.55
add(0, z0) → z0 0.00/0.55
add(s, z0) → s 0.00/0.55
first(0, z0) → nil 0.00/0.55
first(s, cons(z0)) → cons(z0)
S tuples:
TERMS(z0) → c(SQR(z0))
K tuples:none
TERMS(z0) → c(SQR(z0))
terms, sqr, dbl, add, first
TERMS
c
Tuples:
terms(z0) → cons(recip(sqr(z0))) 0.00/0.55
sqr(0) → 0 0.00/0.55
sqr(s) → s 0.00/0.55
dbl(0) → 0 0.00/0.55
dbl(s) → s 0.00/0.55
add(0, z0) → z0 0.00/0.55
add(s, z0) → s 0.00/0.55
first(0, z0) → nil 0.00/0.55
first(s, cons(z0)) → cons(z0)
S tuples:
TERMS(z0) → c
K tuples:none
TERMS(z0) → c
terms, sqr, dbl, add, first
TERMS
c
TERMS(z0) → c
Tuples:none
terms(z0) → cons(recip(sqr(z0))) 0.00/0.55
sqr(0) → 0 0.00/0.55
sqr(s) → s 0.00/0.55
dbl(0) → 0 0.00/0.55
dbl(s) → s 0.00/0.55
add(0, z0) → z0 0.00/0.55
add(s, z0) → s 0.00/0.55
first(0, z0) → nil 0.00/0.55
first(s, cons(z0)) → cons(z0)
terms, sqr, dbl, add, first