Termination w.r.t. Q of the given QTRS could not be shown:

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

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)

Q is empty.

(1) Overlay + Local Confluence (EQUIVALENT transformation)

The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

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)

The set Q consists of the following terms:

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)

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(4) Obligation:

Q DP problem:
The TRS P consists of the following rules:

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)

The TRS R consists of the following rules:

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)

The set Q consists of the following terms:

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)

We have to consider all minimal (P,Q,R)-chains.

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 3 SCCs with 7 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Q DP problem:
The TRS P consists of the following rules:

APP(add(n, x), y) → APP(x, y)

The TRS R consists of the following rules:

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)

The set Q consists of the following terms:

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)

We have to consider all minimal (P,Q,R)-chains.

(8) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

APP(add(n, x), y) → APP(x, y)

The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
APP(x1, x2)  =  APP(x1)
add(x1, x2)  =  add(x1, x2)

Lexicographic Path Order [LPO].
Precedence:

add₂ > APP₁

The following usable rules [FROCOS05] were oriented: none

(9) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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)

The set Q consists of the following terms:

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)

We have to consider all minimal (P,Q,R)-chains.

(10) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(11) TRUE

(12) Obligation:

Q DP problem:
The TRS P consists of the following rules:

REVERSE(add(n, x)) → REVERSE(x)

The TRS R consists of the following rules:

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)

The set Q consists of the following terms:

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)

We have to consider all minimal (P,Q,R)-chains.

(13) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

REVERSE(add(n, x)) → REVERSE(x)

The remaining pairs can at least be oriented weakly.
Used ordering: Lexicographic Path Order [LPO].
Precedence:

add₂ > REVERSE₁

The following usable rules [FROCOS05] were oriented: none

(14) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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)

The set Q consists of the following terms:

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)

We have to consider all minimal (P,Q,R)-chains.

(15) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(16) TRUE

(17) Obligation:

Q DP problem:
The TRS P consists of the following rules:

IF(false, x, y, z) → SHUFF(reverse(tail(x)), z)
SHUFF(x, y) → IF(null(x), x, y, app(y, add(head(x), nil)))

The TRS R consists of the following rules:

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)

The set Q consists of the following terms:

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)

We have to consider all minimal (P,Q,R)-chains.