0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 QDP
↳7 UsableRulesProof (⇔)
↳8 QDP
↳9 QReductionProof (⇔)
↳10 QDP
↳11 QDPOrderProof (⇔)
↳12 QDP
↳13 DependencyGraphProof (⇔)
↳14 TRUE
is_empty(nil) → true
is_empty(cons(x, l)) → false
hd(cons(x, l)) → x
tl(cons(x, l)) → l
append(l1, l2) → ifappend(l1, l2, is_empty(l1))
ifappend(l1, l2, true) → l2
ifappend(l1, l2, false) → cons(hd(l1), append(tl(l1), l2))
is_empty(nil) → true
is_empty(cons(x, l)) → false
hd(cons(x, l)) → x
tl(cons(x, l)) → l
append(l1, l2) → ifappend(l1, l2, is_empty(l1))
ifappend(l1, l2, true) → l2
ifappend(l1, l2, false) → cons(hd(l1), append(tl(l1), l2))
is_empty(nil)
is_empty(cons(x0, x1))
hd(cons(x0, x1))
tl(cons(x0, x1))
append(x0, x1)
ifappend(x0, x1, true)
ifappend(x0, x1, false)
APPEND(l1, l2) → IFAPPEND(l1, l2, is_empty(l1))
APPEND(l1, l2) → IS_EMPTY(l1)
IFAPPEND(l1, l2, false) → HD(l1)
IFAPPEND(l1, l2, false) → APPEND(tl(l1), l2)
IFAPPEND(l1, l2, false) → TL(l1)
is_empty(nil) → true
is_empty(cons(x, l)) → false
hd(cons(x, l)) → x
tl(cons(x, l)) → l
append(l1, l2) → ifappend(l1, l2, is_empty(l1))
ifappend(l1, l2, true) → l2
ifappend(l1, l2, false) → cons(hd(l1), append(tl(l1), l2))
is_empty(nil)
is_empty(cons(x0, x1))
hd(cons(x0, x1))
tl(cons(x0, x1))
append(x0, x1)
ifappend(x0, x1, true)
ifappend(x0, x1, false)
IFAPPEND(l1, l2, false) → APPEND(tl(l1), l2)
APPEND(l1, l2) → IFAPPEND(l1, l2, is_empty(l1))
is_empty(nil) → true
is_empty(cons(x, l)) → false
hd(cons(x, l)) → x
tl(cons(x, l)) → l
append(l1, l2) → ifappend(l1, l2, is_empty(l1))
ifappend(l1, l2, true) → l2
ifappend(l1, l2, false) → cons(hd(l1), append(tl(l1), l2))
is_empty(nil)
is_empty(cons(x0, x1))
hd(cons(x0, x1))
tl(cons(x0, x1))
append(x0, x1)
ifappend(x0, x1, true)
ifappend(x0, x1, false)
IFAPPEND(l1, l2, false) → APPEND(tl(l1), l2)
APPEND(l1, l2) → IFAPPEND(l1, l2, is_empty(l1))
is_empty(nil) → true
is_empty(cons(x, l)) → false
tl(cons(x, l)) → l
is_empty(nil)
is_empty(cons(x0, x1))
hd(cons(x0, x1))
tl(cons(x0, x1))
append(x0, x1)
ifappend(x0, x1, true)
ifappend(x0, x1, false)
hd(cons(x0, x1))
append(x0, x1)
ifappend(x0, x1, true)
ifappend(x0, x1, false)
IFAPPEND(l1, l2, false) → APPEND(tl(l1), l2)
APPEND(l1, l2) → IFAPPEND(l1, l2, is_empty(l1))
is_empty(nil) → true
is_empty(cons(x, l)) → false
tl(cons(x, l)) → l
is_empty(nil)
is_empty(cons(x0, x1))
tl(cons(x0, x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IFAPPEND(l1, l2, false) → APPEND(tl(l1), l2)
The value of delta used in the strict ordering is 9/16.
POL(IFAPPEND(x1, x2, x3)) = (1/2)x1 + (4)x3
POL(false) = 1/4
POL(APPEND(x1, x2)) = (7/4)x1
POL(tl(x1)) = 1/4 + (1/4)x1
POL(is_empty(x1)) = (1/4)x1
POL(cons(x1, x2)) = 1 + (4)x2
POL(nil) = 5/4
POL(true) = 0
tl(cons(x, l)) → l
is_empty(cons(x, l)) → false
is_empty(nil) → true
APPEND(l1, l2) → IFAPPEND(l1, l2, is_empty(l1))
is_empty(nil) → true
is_empty(cons(x, l)) → false
tl(cons(x, l)) → l
is_empty(nil)
is_empty(cons(x0, x1))
tl(cons(x0, x1))