MAYBE 11.65/6.70 MAYBE 11.65/6.72 11.65/6.72 11.65/6.72
11.65/6.72 11.65/6.730 CpxTRS11.65/6.73
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))11.65/6.73
↳2 CdtProblem11.65/6.73
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))11.65/6.73
↳4 CdtProblem11.65/6.73
↳5 CdtNarrowingProof (BOTH BOUNDS(ID, ID))11.65/6.73
↳6 CdtProblem11.65/6.73
↳7 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))11.65/6.73
↳8 CdtProblem11.65/6.73
↳9 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))11.65/6.73
↳10 CdtProblem11.65/6.73
↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))11.65/6.73
↳12 CdtProblem11.65/6.73
↳13 CdtNarrowingProof (BOTH BOUNDS(ID, ID))11.65/6.73
↳14 CdtProblem11.65/6.73
↳15 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))11.65/6.73
↳16 CdtProblem11.65/6.73
is_empty(nil) → true 11.65/6.73
is_empty(cons(x, l)) → false 11.65/6.73
hd(cons(x, l)) → x 11.65/6.73
tl(cons(x, l)) → cons(x, l) 11.65/6.73
append(l1, l2) → ifappend(l1, l2, is_empty(l1)) 11.65/6.73
ifappend(l1, l2, true) → l2 11.65/6.73
ifappend(l1, l2, false) → cons(hd(l1), append(tl(l1), l2))
Tuples:
is_empty(nil) → true 11.65/6.73
is_empty(cons(z0, z1)) → false 11.65/6.73
hd(cons(z0, z1)) → z0 11.65/6.73
tl(cons(z0, z1)) → cons(z0, z1) 11.65/6.73
append(z0, z1) → ifappend(z0, z1, is_empty(z0)) 11.65/6.73
ifappend(z0, z1, true) → z1 11.65/6.73
ifappend(z0, z1, false) → cons(hd(z0), append(tl(z0), z1))
S tuples:
APPEND(z0, z1) → c4(IFAPPEND(z0, z1, is_empty(z0)), IS_EMPTY(z0)) 11.65/6.73
IFAPPEND(z0, z1, false) → c6(HD(z0), APPEND(tl(z0), z1), TL(z0))
K tuples:none
APPEND(z0, z1) → c4(IFAPPEND(z0, z1, is_empty(z0)), IS_EMPTY(z0)) 11.65/6.73
IFAPPEND(z0, z1, false) → c6(HD(z0), APPEND(tl(z0), z1), TL(z0))
is_empty, hd, tl, append, ifappend
APPEND, IFAPPEND
c4, c6
Tuples:
is_empty(nil) → true 11.65/6.73
is_empty(cons(z0, z1)) → false 11.65/6.73
hd(cons(z0, z1)) → z0 11.65/6.73
tl(cons(z0, z1)) → cons(z0, z1) 11.65/6.73
append(z0, z1) → ifappend(z0, z1, is_empty(z0)) 11.65/6.73
ifappend(z0, z1, true) → z1 11.65/6.73
ifappend(z0, z1, false) → cons(hd(z0), append(tl(z0), z1))
S tuples:
APPEND(z0, z1) → c4(IFAPPEND(z0, z1, is_empty(z0))) 11.65/6.73
IFAPPEND(z0, z1, false) → c6(APPEND(tl(z0), z1))
K tuples:none
APPEND(z0, z1) → c4(IFAPPEND(z0, z1, is_empty(z0))) 11.65/6.73
IFAPPEND(z0, z1, false) → c6(APPEND(tl(z0), z1))
is_empty, hd, tl, append, ifappend
APPEND, IFAPPEND
c4, c6
APPEND(nil, x1) → c4(IFAPPEND(nil, x1, true)) 11.65/6.73
APPEND(cons(z0, z1), x1) → c4(IFAPPEND(cons(z0, z1), x1, false))
Tuples:
is_empty(nil) → true 11.65/6.73
is_empty(cons(z0, z1)) → false 11.65/6.73
hd(cons(z0, z1)) → z0 11.65/6.73
tl(cons(z0, z1)) → cons(z0, z1) 11.65/6.73
append(z0, z1) → ifappend(z0, z1, is_empty(z0)) 11.65/6.73
ifappend(z0, z1, true) → z1 11.65/6.73
ifappend(z0, z1, false) → cons(hd(z0), append(tl(z0), z1))
S tuples:
IFAPPEND(z0, z1, false) → c6(APPEND(tl(z0), z1)) 11.65/6.73
APPEND(nil, x1) → c4(IFAPPEND(nil, x1, true)) 11.65/6.73
APPEND(cons(z0, z1), x1) → c4(IFAPPEND(cons(z0, z1), x1, false))
K tuples:none
IFAPPEND(z0, z1, false) → c6(APPEND(tl(z0), z1)) 11.65/6.73
APPEND(nil, x1) → c4(IFAPPEND(nil, x1, true)) 11.65/6.73
APPEND(cons(z0, z1), x1) → c4(IFAPPEND(cons(z0, z1), x1, false))
is_empty, hd, tl, append, ifappend
IFAPPEND, APPEND
c6, c4
Tuples:
is_empty(nil) → true 11.65/6.73
is_empty(cons(z0, z1)) → false 11.65/6.73
hd(cons(z0, z1)) → z0 11.65/6.73
tl(cons(z0, z1)) → cons(z0, z1) 11.65/6.73
append(z0, z1) → ifappend(z0, z1, is_empty(z0)) 11.65/6.73
ifappend(z0, z1, true) → z1 11.65/6.73
ifappend(z0, z1, false) → cons(hd(z0), append(tl(z0), z1))
S tuples:
IFAPPEND(z0, z1, false) → c6(APPEND(tl(z0), z1)) 11.65/6.73
APPEND(cons(z0, z1), x1) → c4(IFAPPEND(cons(z0, z1), x1, false)) 11.65/6.73
APPEND(nil, x1) → c4
K tuples:none
IFAPPEND(z0, z1, false) → c6(APPEND(tl(z0), z1)) 11.65/6.73
APPEND(cons(z0, z1), x1) → c4(IFAPPEND(cons(z0, z1), x1, false)) 11.65/6.73
APPEND(nil, x1) → c4
is_empty, hd, tl, append, ifappend
IFAPPEND, APPEND
c6, c4, c4
APPEND(nil, x1) → c4
Tuples:
is_empty(nil) → true 11.65/6.73
is_empty(cons(z0, z1)) → false 11.65/6.73
hd(cons(z0, z1)) → z0 11.65/6.73
tl(cons(z0, z1)) → cons(z0, z1) 11.65/6.73
append(z0, z1) → ifappend(z0, z1, is_empty(z0)) 11.65/6.73
ifappend(z0, z1, true) → z1 11.65/6.73
ifappend(z0, z1, false) → cons(hd(z0), append(tl(z0), z1))
S tuples:
IFAPPEND(z0, z1, false) → c6(APPEND(tl(z0), z1)) 11.65/6.73
APPEND(cons(z0, z1), x1) → c4(IFAPPEND(cons(z0, z1), x1, false)) 11.65/6.73
APPEND(nil, x1) → c4
K tuples:none
IFAPPEND(z0, z1, false) → c6(APPEND(tl(z0), z1)) 11.65/6.73
APPEND(cons(z0, z1), x1) → c4(IFAPPEND(cons(z0, z1), x1, false)) 11.65/6.73
APPEND(nil, x1) → c4
is_empty, hd, tl, append, ifappend
IFAPPEND, APPEND
c6, c4, c4
We considered the (Usable) Rules:
APPEND(nil, x1) → c4
And the Tuples:
tl(cons(z0, z1)) → cons(z0, z1)
The order we found is given by the following interpretation:
IFAPPEND(z0, z1, false) → c6(APPEND(tl(z0), z1)) 11.65/6.73
APPEND(cons(z0, z1), x1) → c4(IFAPPEND(cons(z0, z1), x1, false)) 11.65/6.73
APPEND(nil, x1) → c4
POL(APPEND(x1, x2)) = [1] 11.65/6.73
POL(IFAPPEND(x1, x2, x3)) = [1] 11.65/6.73
POL(c4) = 0 11.65/6.73
POL(c4(x1)) = x1 11.65/6.73
POL(c6(x1)) = x1 11.65/6.73
POL(cons(x1, x2)) = [2] 11.65/6.73
POL(false) = [1] 11.65/6.73
POL(nil) = [1] 11.65/6.73
POL(tl(x1)) = [4]
Tuples:
is_empty(nil) → true 11.65/6.73
is_empty(cons(z0, z1)) → false 11.65/6.73
hd(cons(z0, z1)) → z0 11.65/6.73
tl(cons(z0, z1)) → cons(z0, z1) 11.65/6.73
append(z0, z1) → ifappend(z0, z1, is_empty(z0)) 11.65/6.73
ifappend(z0, z1, true) → z1 11.65/6.73
ifappend(z0, z1, false) → cons(hd(z0), append(tl(z0), z1))
S tuples:
IFAPPEND(z0, z1, false) → c6(APPEND(tl(z0), z1)) 11.65/6.73
APPEND(cons(z0, z1), x1) → c4(IFAPPEND(cons(z0, z1), x1, false)) 11.65/6.73
APPEND(nil, x1) → c4
K tuples:
IFAPPEND(z0, z1, false) → c6(APPEND(tl(z0), z1)) 11.65/6.73
APPEND(cons(z0, z1), x1) → c4(IFAPPEND(cons(z0, z1), x1, false))
Defined Rule Symbols:
APPEND(nil, x1) → c4
is_empty, hd, tl, append, ifappend
IFAPPEND, APPEND
c6, c4, c4
IFAPPEND(cons(z0, z1), x1, false) → c6(APPEND(cons(z0, z1), x1))
Tuples:
is_empty(nil) → true 11.65/6.73
is_empty(cons(z0, z1)) → false 11.65/6.73
hd(cons(z0, z1)) → z0 11.65/6.73
tl(cons(z0, z1)) → cons(z0, z1) 11.65/6.73
append(z0, z1) → ifappend(z0, z1, is_empty(z0)) 11.65/6.73
ifappend(z0, z1, true) → z1 11.65/6.73
ifappend(z0, z1, false) → cons(hd(z0), append(tl(z0), z1))
S tuples:
APPEND(cons(z0, z1), x1) → c4(IFAPPEND(cons(z0, z1), x1, false)) 11.65/6.73
APPEND(nil, x1) → c4 11.65/6.73
IFAPPEND(cons(z0, z1), x1, false) → c6(APPEND(cons(z0, z1), x1))
K tuples:
APPEND(cons(z0, z1), x1) → c4(IFAPPEND(cons(z0, z1), x1, false)) 11.65/6.73
IFAPPEND(cons(z0, z1), x1, false) → c6(APPEND(cons(z0, z1), x1))
Defined Rule Symbols:
APPEND(nil, x1) → c4
is_empty, hd, tl, append, ifappend
APPEND, IFAPPEND
c4, c4, c6
APPEND(nil, x1) → c4
Tuples:
is_empty(nil) → true 11.65/6.73
is_empty(cons(z0, z1)) → false 11.65/6.73
hd(cons(z0, z1)) → z0 11.65/6.73
tl(cons(z0, z1)) → cons(z0, z1) 11.65/6.73
append(z0, z1) → ifappend(z0, z1, is_empty(z0)) 11.65/6.73
ifappend(z0, z1, true) → z1 11.65/6.73
ifappend(z0, z1, false) → cons(hd(z0), append(tl(z0), z1))
S tuples:
APPEND(cons(z0, z1), x1) → c4(IFAPPEND(cons(z0, z1), x1, false)) 11.65/6.73
IFAPPEND(cons(z0, z1), x1, false) → c6(APPEND(cons(z0, z1), x1))
K tuples:none
APPEND(cons(z0, z1), x1) → c4(IFAPPEND(cons(z0, z1), x1, false)) 11.65/6.73
IFAPPEND(cons(z0, z1), x1, false) → c6(APPEND(cons(z0, z1), x1))
is_empty, hd, tl, append, ifappend
APPEND, IFAPPEND
c4, c6