0 QTRS
↳1 Overlay + Local Confluence (⇔)
↳2 QTRS
↳3 DependencyPairsProof (⇔)
↳4 QDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 QDP
↳8 UsableRulesProof (⇔)
↳9 QDP
↳10 QReductionProof (⇔)
↳11 QDP
↳12 QDPOrderProof (⇔)
↳13 QDP
↳14 PisEmptyProof (⇔)
↳15 TRUE
↳16 QDP
↳17 UsableRulesProof (⇔)
↳18 QDP
↳19 QReductionProof (⇔)
↳20 QDP
↳21 QDPOrderProof (⇔)
↳22 QDP
↳23 DependencyGraphProof (⇔)
↳24 TRUE
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
last(x, l) → if(empty(l), x, l)
if(true, x, l) → x
if(false, x, l) → last(head(l), tail(l))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
last(x, l) → if(empty(l), x, l)
if(true, x, l) → x
if(false, x, l) → last(head(l), tail(l))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
rev(nil)
rev(cons(x0, x1))
last(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
rev2(x0, nil)
rev2(x0, cons(x1, x2))
REV(cons(x, l)) → REV2(x, l)
LAST(x, l) → IF(empty(l), x, l)
LAST(x, l) → EMPTY(l)
IF(false, x, l) → LAST(head(l), tail(l))
IF(false, x, l) → HEAD(l)
IF(false, x, l) → TAIL(l)
REV2(x, cons(y, l)) → REV(cons(x, rev2(y, l)))
REV2(x, cons(y, l)) → REV2(y, l)
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
last(x, l) → if(empty(l), x, l)
if(true, x, l) → x
if(false, x, l) → last(head(l), tail(l))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
rev(nil)
rev(cons(x0, x1))
last(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
rev2(x0, nil)
rev2(x0, cons(x1, x2))
IF(false, x, l) → LAST(head(l), tail(l))
LAST(x, l) → IF(empty(l), x, l)
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
last(x, l) → if(empty(l), x, l)
if(true, x, l) → x
if(false, x, l) → last(head(l), tail(l))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
rev(nil)
rev(cons(x0, x1))
last(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
rev2(x0, nil)
rev2(x0, cons(x1, x2))
IF(false, x, l) → LAST(head(l), tail(l))
LAST(x, l) → IF(empty(l), x, l)
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
rev(nil)
rev(cons(x0, x1))
last(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
rev2(x0, nil)
rev2(x0, cons(x1, x2))
rev(nil)
rev(cons(x0, x1))
last(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
rev2(x0, nil)
rev2(x0, cons(x1, x2))
IF(false, x, l) → LAST(head(l), tail(l))
LAST(x, l) → IF(empty(l), x, l)
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IF(false, x, l) → LAST(head(l), tail(l))
LAST(x, l) → IF(empty(l), x, l)
The value of delta used in the strict ordering is 1/4.
POL(IF(x1, x2, x3)) = (11/4)x1 + (1/2)x2 + x3
POL(false) = 3/4
POL(LAST(x1, x2)) = 1 + (1/2)x1 + (7/4)x2
POL(head(x1)) = 3/4 + x1
POL(tail(x1)) = 1/4 + (1/4)x1
POL(empty(x1)) = (1/4)x1
POL(cons(x1, x2)) = 4 + x1 + (4)x2
POL(nil) = 0
POL(true) = 0
tail(cons(x, l)) → l
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
REV2(x, cons(y, l)) → REV(cons(x, rev2(y, l)))
REV(cons(x, l)) → REV2(x, l)
REV2(x, cons(y, l)) → REV2(y, l)
empty(nil) → true
empty(cons(x, l)) → false
head(cons(x, l)) → x
tail(nil) → nil
tail(cons(x, l)) → l
rev(nil) → nil
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
last(x, l) → if(empty(l), x, l)
if(true, x, l) → x
if(false, x, l) → last(head(l), tail(l))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
rev(nil)
rev(cons(x0, x1))
last(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
rev2(x0, nil)
rev2(x0, cons(x1, x2))
REV2(x, cons(y, l)) → REV(cons(x, rev2(y, l)))
REV(cons(x, l)) → REV2(x, l)
REV2(x, cons(y, l)) → REV2(y, l)
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
rev(nil)
rev(cons(x0, x1))
last(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
rev2(x0, nil)
rev2(x0, cons(x1, x2))
empty(nil)
empty(cons(x0, x1))
head(cons(x0, x1))
tail(nil)
tail(cons(x0, x1))
last(x0, x1)
if(true, x0, x1)
if(false, x0, x1)
REV2(x, cons(y, l)) → REV(cons(x, rev2(y, l)))
REV(cons(x, l)) → REV2(x, l)
REV2(x, cons(y, l)) → REV2(y, l)
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
rev(nil)
rev(cons(x0, x1))
rev2(x0, nil)
rev2(x0, cons(x1, x2))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
REV(cons(x, l)) → REV2(x, l)
REV2(x, cons(y, l)) → REV2(y, l)
POL(REV(x1)) = x1
POL(REV2(x1, x2)) = x1 + x2
POL(cons(x1, x2)) = 1 + x1 + x2
POL(nil) = 0
POL(rev(x1)) = x1
POL(rev1(x1, x2)) = 0
POL(rev2(x1, x2)) = x1 + x2
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
rev2(x, nil) → nil
REV2(x, cons(y, l)) → REV(cons(x, rev2(y, l)))
rev2(x, nil) → nil
rev2(x, cons(y, l)) → rev(cons(x, rev2(y, l)))
rev(cons(x, l)) → cons(rev1(x, l), rev2(x, l))
rev(nil)
rev(cons(x0, x1))
rev2(x0, nil)
rev2(x0, cons(x1, x2))