(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
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(nil) → nil
shuffle(add(n, x)) → add(n, shuffle(reverse(x)))
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:
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(nil) → nil
shuffle(add(n, x)) → add(n, shuffle(reverse(x)))
The set Q consists of the following terms:
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(nil)
shuffle(add(x0, x1))
(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(add(n, x)) → SHUFFLE(reverse(x))
SHUFFLE(add(n, x)) → REVERSE(x)
The TRS R consists of the following rules:
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(nil) → nil
shuffle(add(n, x)) → add(n, shuffle(reverse(x)))
The set Q consists of the following terms:
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(nil)
shuffle(add(x0, x1))
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 2 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:
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(nil) → nil
shuffle(add(n, x)) → add(n, shuffle(reverse(x)))
The set Q consists of the following terms:
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(nil)
shuffle(add(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
(8) 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:
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(nil) → nil
shuffle(add(n, x)) → add(n, shuffle(reverse(x)))
The set Q consists of the following terms:
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(nil)
shuffle(add(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
(9) Obligation:
Q DP problem:
The TRS P consists of the following rules:
SHUFFLE(add(n, x)) → SHUFFLE(reverse(x))
The TRS R consists of the following rules:
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(nil) → nil
shuffle(add(n, x)) → add(n, shuffle(reverse(x)))
The set Q consists of the following terms:
app(nil, x0)
app(add(x0, x1), x2)
reverse(nil)
reverse(add(x0, x1))
shuffle(nil)
shuffle(add(x0, x1))
We have to consider all minimal (P,Q,R)-chains.