The following DP Processors were used

Problem 1 was processed with processor DependencyGraph (0ms).
 | – Problem 2 was processed with processor SubtermCriterion (0ms).
 | – Problem 3 was processed with processor PolynomialOrdering (0ms).
 | – Problem 4 was processed with processor BackwardInstantiation (5ms).
 |    | – Problem 5 was processed with processor BackwardInstantiation (3ms).
 |    |    | – Problem 6 was processed with processor BackwardInstantiation (2ms).
 |    |    |    | – Problem 7 remains open; application of the following processors failed [ForwardInstantiation (2ms), Propagation (1ms)].

Problem 1: DependencyGraph

---

---

Dependency Pair Problem

Dependency Pairs

rev#(cons(x, xs))	→	rev#(cons(x, nil))		app#(cons(x, xs), ys)	→	app#(xs, ys)
shuffle#(cons(x, xs))	→	shuffle#(rev(xs))		shuffle#(cons(x, xs))	→	rev#(xs)

Rewrite Rules

app(nil, xs)	→	nil		app(cons(x, xs), ys)	→	cons(x, app(xs, ys))
rev(nil)	→	nil		rev(cons(x, xs))	→	append(xs, rev(cons(x, nil)))
shuffle(nil)	→	nil		shuffle(cons(x, xs))	→	cons(x, shuffle(rev(xs)))

Original Signature

Termination of terms over the following signature is verified: app, append, rev, shuffle, nil, cons

Strategy

---

Parameters

• Use inverse cap function: true
• Use strongly defined symbols: false

---

The following SCCs where found

rev#(cons(x, xs)) → rev#(cons(x, nil))

---

app#(cons(x, xs), ys) → app#(xs, ys)

---

shuffle#(cons(x, xs)) → shuffle#(rev(xs))

---

Problem 2: SubtermCriterion

---

---

Dependency Pair Problem

Dependency Pairs

app#(cons(x, xs), ys)

→

app#(xs, ys)

Rewrite Rules

app(nil, xs)	→	nil		app(cons(x, xs), ys)	→	cons(x, app(xs, ys))
rev(nil)	→	nil		rev(cons(x, xs))	→	append(xs, rev(cons(x, nil)))
shuffle(nil)	→	nil		shuffle(cons(x, xs))	→	cons(x, shuffle(rev(xs)))

Original Signature

Termination of terms over the following signature is verified: app, append, rev, shuffle, nil, cons

Strategy

---

Projection

The following projection was used:

• π (app#): 1

Thus, the following dependency pairs are removed:

app#(cons(x, xs), ys)

→

app#(xs, ys)

Problem 3: PolynomialOrdering

---

---

Dependency Pair Problem

Dependency Pairs

shuffle#(cons(x, xs))

→

shuffle#(rev(xs))

Rewrite Rules

app(nil, xs)	→	nil		app(cons(x, xs), ys)	→	cons(x, app(xs, ys))
rev(nil)	→	nil		rev(cons(x, xs))	→	append(xs, rev(cons(x, nil)))
shuffle(nil)	→	nil		shuffle(cons(x, xs))	→	cons(x, shuffle(rev(xs)))

Original Signature

Termination of terms over the following signature is verified: app, append, rev, shuffle, nil, cons

Strategy

---

Parameters

• Usable Rules: Improved
• Polynomial Degree: Linear
• Use negative constants: false
• Coefficient Range: 4
• Negative Constant Range: 0

---

Polynomial Interpretation

• app(x,y): 0
• append(x,y): 0
• cons(x,y): 2x + 1
• nil: 0
• rev(x): 0
• shuffle(x): 0
• shuffle#(x): 2x

Improved Usable rules

rev(cons(x, xs))

→

append(xs, rev(cons(x, nil)))

rev(nil)

→

nil

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

shuffle#(cons(x, xs))

→

shuffle#(rev(xs))

Problem 4: BackwardInstantiation

---

---

Dependency Pair Problem

Dependency Pairs

rev#(cons(x, xs))

→

rev#(cons(x, nil))

Rewrite Rules

app(nil, xs)	→	nil		app(cons(x, xs), ys)	→	cons(x, app(xs, ys))
rev(nil)	→	nil		rev(cons(x, xs))	→	append(xs, rev(cons(x, nil)))
shuffle(nil)	→	nil		shuffle(cons(x, xs))	→	cons(x, shuffle(rev(xs)))

Original Signature

Termination of terms over the following signature is verified: app, append, rev, shuffle, nil, cons

Strategy

---

Instantiation

For all potential predecessors l → r of the rule rev^#(cons(x, xs)) → rev^#(cons(x, nil)) on dependency pair chains it holds that:

• rev#(cons(x, xs)) matches r,
• all variables of rev#(cons(x, xs)) are embedded in constructor contexts, i.e., each subterm of rev#(cons(x, xs)), containing a variable is rooted by a constructor symbol.

Thus, rev^#(cons(x, xs)) → rev^#(cons(x, nil)) is replaced by instances determined through the above matching. These instances are:

rev#(cons(_x, nil)) → rev#(cons(_x, nil))

Problem 5: BackwardInstantiation

---

---

Dependency Pair Problem

Dependency Pairs

rev#(cons(_x, nil))

→

rev#(cons(_x, nil))

Rewrite Rules

app(nil, xs)	→	nil		app(cons(x, xs), ys)	→	cons(x, app(xs, ys))
rev(nil)	→	nil		rev(cons(x, xs))	→	append(xs, rev(cons(x, nil)))
shuffle(nil)	→	nil		shuffle(cons(x, xs))	→	cons(x, shuffle(rev(xs)))

Original Signature

Termination of terms over the following signature is verified: append, app, rev, shuffle, cons, nil

Strategy

---

Instantiation

For all potential predecessors l → r of the rule rev^#(cons(_x, nil)) → rev^#(cons(_x, nil)) on dependency pair chains it holds that:

• rev#(cons(_x, nil)) matches r,
• all variables of rev#(cons(_x, nil)) are embedded in constructor contexts, i.e., each subterm of rev#(cons(_x, nil)), containing a variable is rooted by a constructor symbol.

Thus, rev^#(cons(_x, nil)) → rev^#(cons(_x, nil)) is replaced by instances determined through the above matching. These instances are:

rev#(cons(__x, nil)) → rev#(cons(__x, nil))

Problem 6: BackwardInstantiation

---

---

Dependency Pair Problem

Dependency Pairs

rev#(cons(__x, nil))

→

rev#(cons(__x, nil))

Rewrite Rules

app(nil, xs)	→	nil		app(cons(x, xs), ys)	→	cons(x, app(xs, ys))
rev(nil)	→	nil		rev(cons(x, xs))	→	append(xs, rev(cons(x, nil)))
shuffle(nil)	→	nil		shuffle(cons(x, xs))	→	cons(x, shuffle(rev(xs)))

Original Signature

Termination of terms over the following signature is verified: app, append, rev, shuffle, nil, cons

Strategy

---

Instantiation

For all potential predecessors l → r of the rule rev^#(cons(__x, nil)) → rev^#(cons(__x, nil)) on dependency pair chains it holds that:

• rev#(cons(__x, nil)) matches r,
• all variables of rev#(cons(__x, nil)) are embedded in constructor contexts, i.e., each subterm of rev#(cons(__x, nil)), containing a variable is rooted by a constructor symbol.

Thus, rev^#(cons(__x, nil)) → rev^#(cons(__x, nil)) is replaced by instances determined through the above matching. These instances are:

rev#(cons(___x, nil)) → rev#(cons(___x, nil))