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.
APPEND(l1, l2) → IFAPPEND(l1, l2, is_empty(l1))
The value of delta used in the strict ordering is 5/8.
POL(IFAPPEND(x1, x2, x3)) = 1/2 + (3/4)x1 + (9/4)x3
POL(false) = 1
POL(APPEND(x1, x2)) = 9/4 + (2)x1
POL(tl(x1)) = 1/4 + (1/4)x1
POL(is_empty(x1)) = 1/2 + (1/2)x1
POL(cons(x1, x2)) = 4 + (4)x2
POL(nil) = 4
POL(true) = 3/4
is_empty(cons(x, l)) → false
tl(cons(x, l)) → l
is_empty(nil) → true
IFAPPEND(l1, l2, false) → APPEND(tl(l1), l2)
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))