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 QDPSizeChangeProof (⇔)
↳13 TRUE
↳14 QDP
↳15 UsableRulesProof (⇔)
↳16 QDP
↳17 QReductionProof (⇔)
↳18 QDP
↳19 QDPSizeChangeProof (⇔)
↳20 TRUE
↳21 QDP
↳22 UsableRulesProof (⇔)
↳23 QDP
↳24 QReductionProof (⇔)
↳25 QDP
↳26 Narrowing (⇔)
↳27 QDP
↳28 DependencyGraphProof (⇔)
↳29 QDP
↳30 UsableRulesProof (⇔)
↳31 QDP
↳32 QReductionProof (⇔)
↳33 QDP
↳34 Rewriting (⇔)
↳35 QDP
↳36 UsableRulesProof (⇔)
↳37 QDP
↳38 QReductionProof (⇔)
↳39 QDP
↳40 Narrowing (⇔)
↳41 QDP
↳42 DependencyGraphProof (⇔)
↳43 QDP
↳44 UsableRulesProof (⇔)
↳45 QDP
↳46 QReductionProof (⇔)
↳47 QDP
↳48 QDPOrderProof (⇔)
↳49 QDP
↳50 DependencyGraphProof (⇔)
↳51 TRUE
null(nil) → true
null(add(n, x)) → false
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
shuffle(x) → shuff(x, nil)
shuff(x, y) → if(null(x), x, y, app(y, add(head(x), nil)))
if(true, x, y, z) → y
if(false, x, y, z) → shuff(reverse(tail(x)), z)
null(nil) → true
null(add(n, x)) → false
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
shuffle(x) → shuff(x, nil)
shuff(x, y) → if(null(x), x, y, app(y, add(head(x), nil)))
if(true, x, y, z) → y
if(false, x, y, z) → shuff(reverse(tail(x)), z)
null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(x0)
shuff(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
APP(add(n, x), y) → APP(x, y)
REVERSE(add(n, x)) → APP(reverse(x), add(n, nil))
REVERSE(add(n, x)) → REVERSE(x)
SHUFFLE(x) → SHUFF(x, nil)
SHUFF(x, y) → IF(null(x), x, y, app(y, add(head(x), nil)))
SHUFF(x, y) → NULL(x)
SHUFF(x, y) → APP(y, add(head(x), nil))
SHUFF(x, y) → HEAD(x)
IF(false, x, y, z) → SHUFF(reverse(tail(x)), z)
IF(false, x, y, z) → REVERSE(tail(x))
IF(false, x, y, z) → TAIL(x)
null(nil) → true
null(add(n, x)) → false
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
shuffle(x) → shuff(x, nil)
shuff(x, y) → if(null(x), x, y, app(y, add(head(x), nil)))
if(true, x, y, z) → y
if(false, x, y, z) → shuff(reverse(tail(x)), z)
null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(x0)
shuff(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
APP(add(n, x), y) → APP(x, y)
null(nil) → true
null(add(n, x)) → false
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
shuffle(x) → shuff(x, nil)
shuff(x, y) → if(null(x), x, y, app(y, add(head(x), nil)))
if(true, x, y, z) → y
if(false, x, y, z) → shuff(reverse(tail(x)), z)
null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(x0)
shuff(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
APP(add(n, x), y) → APP(x, y)
null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(x0)
shuff(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(x0)
shuff(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
APP(add(n, x), y) → APP(x, y)
From the DPs we obtained the following set of size-change graphs:
REVERSE(add(n, x)) → REVERSE(x)
null(nil) → true
null(add(n, x)) → false
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
shuffle(x) → shuff(x, nil)
shuff(x, y) → if(null(x), x, y, app(y, add(head(x), nil)))
if(true, x, y, z) → y
if(false, x, y, z) → shuff(reverse(tail(x)), z)
null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(x0)
shuff(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
REVERSE(add(n, x)) → REVERSE(x)
null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(x0)
shuff(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(x0)
shuff(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
REVERSE(add(n, x)) → REVERSE(x)
From the DPs we obtained the following set of size-change graphs:
IF(false, x, y, z) → SHUFF(reverse(tail(x)), z)
SHUFF(x, y) → IF(null(x), x, y, app(y, add(head(x), nil)))
null(nil) → true
null(add(n, x)) → false
tail(add(n, x)) → x
tail(nil) → nil
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
shuffle(x) → shuff(x, nil)
shuff(x, y) → if(null(x), x, y, app(y, add(head(x), nil)))
if(true, x, y, z) → y
if(false, x, y, z) → shuff(reverse(tail(x)), z)
null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(x0)
shuff(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
IF(false, x, y, z) → SHUFF(reverse(tail(x)), z)
SHUFF(x, y) → IF(null(x), x, y, app(y, add(head(x), nil)))
null(nil) → true
null(add(n, x)) → false
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
tail(add(n, x)) → x
tail(nil) → nil
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(x0)
shuff(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
shuffle(x0)
shuff(x0, x1)
if(true, x0, x1, x2)
if(false, x0, x1, x2)
IF(false, x, y, z) → SHUFF(reverse(tail(x)), z)
SHUFF(x, y) → IF(null(x), x, y, app(y, add(head(x), nil)))
null(nil) → true
null(add(n, x)) → false
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
tail(add(n, x)) → x
tail(nil) → nil
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
SHUFF(nil, y1) → IF(true, nil, y1, app(y1, add(head(nil), nil)))
SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(head(add(x0, x1)), nil)))
IF(false, x, y, z) → SHUFF(reverse(tail(x)), z)
SHUFF(nil, y1) → IF(true, nil, y1, app(y1, add(head(nil), nil)))
SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(head(add(x0, x1)), nil)))
null(nil) → true
null(add(n, x)) → false
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
tail(add(n, x)) → x
tail(nil) → nil
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(head(add(x0, x1)), nil)))
IF(false, x, y, z) → SHUFF(reverse(tail(x)), z)
null(nil) → true
null(add(n, x)) → false
head(add(n, x)) → n
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
tail(add(n, x)) → x
tail(nil) → nil
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(head(add(x0, x1)), nil)))
IF(false, x, y, z) → SHUFF(reverse(tail(x)), z)
tail(add(n, x)) → x
tail(nil) → nil
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
head(add(n, x)) → n
null(nil)
null(add(x0, x1))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
null(nil)
null(add(x0, x1))
SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(head(add(x0, x1)), nil)))
IF(false, x, y, z) → SHUFF(reverse(tail(x)), z)
tail(add(n, x)) → x
tail(nil) → nil
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
head(add(n, x)) → n
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(x0, nil)))
IF(false, x, y, z) → SHUFF(reverse(tail(x)), z)
SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(x0, nil)))
tail(add(n, x)) → x
tail(nil) → nil
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
head(add(n, x)) → n
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
IF(false, x, y, z) → SHUFF(reverse(tail(x)), z)
SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(x0, nil)))
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
tail(add(n, x)) → x
tail(nil) → nil
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
tail(add(x0, x1))
tail(nil)
head(add(x0, x1))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
head(add(x0, x1))
IF(false, x, y, z) → SHUFF(reverse(tail(x)), z)
SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(x0, nil)))
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
tail(add(n, x)) → x
tail(nil) → nil
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
tail(add(x0, x1))
tail(nil)
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
IF(false, add(x0, x1), y1, y2) → SHUFF(reverse(x1), y2)
IF(false, nil, y1, y2) → SHUFF(reverse(nil), y2)
SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(x0, nil)))
IF(false, add(x0, x1), y1, y2) → SHUFF(reverse(x1), y2)
IF(false, nil, y1, y2) → SHUFF(reverse(nil), y2)
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
tail(add(n, x)) → x
tail(nil) → nil
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
tail(add(x0, x1))
tail(nil)
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
IF(false, add(x0, x1), y1, y2) → SHUFF(reverse(x1), y2)
SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(x0, nil)))
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
tail(add(n, x)) → x
tail(nil) → nil
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
tail(add(x0, x1))
tail(nil)
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
IF(false, add(x0, x1), y1, y2) → SHUFF(reverse(x1), y2)
SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(x0, nil)))
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
tail(add(x0, x1))
tail(nil)
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
tail(add(x0, x1))
tail(nil)
IF(false, add(x0, x1), y1, y2) → SHUFF(reverse(x1), y2)
SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(x0, nil)))
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
IF(false, add(x0, x1), y1, y2) → SHUFF(reverse(x1), y2)
POL(IF(x1, x2, x3, x4)) = x2
POL(SHUFF(x1, x2)) = x1
POL(add(x1, x2)) = 1 + x2
POL(app(x1, x2)) = x1 + x2
POL(false) = 0
POL(nil) = 0
POL(reverse(x1)) = x1
app(nil, y) → y
reverse(nil) → nil
app(add(n, x), y) → add(n, app(x, y))
reverse(add(n, x)) → app(reverse(x), add(n, nil))
SHUFF(add(x0, x1), y1) → IF(false, add(x0, x1), y1, app(y1, add(x0, nil)))
app(nil, y) → y
app(add(n, x), y) → add(n, app(x, y))
reverse(nil) → nil
reverse(add(n, x)) → app(reverse(x), add(n, nil))
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))