The following DP Processors were used

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

Problem 1: DependencyGraph

---

---

Dependency Pair Problem

Dependency Pairs

rev#(cons(x, xs))

→

rev#(cons(x, nil))

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)))

Original Signature

Termination of terms over the following signature is verified: app, append, rev, 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)

---

Problem 2: 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)))

Original Signature

Termination of terms over the following signature is verified: app, append, rev, 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 4: 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)))

Original Signature

Termination of terms over the following signature is verified: append, app, rev, 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 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)))

Original Signature

Termination of terms over the following signature is verified: app, append, rev, 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))

Problem 3: 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)))

Original Signature

Termination of terms over the following signature is verified: app, append, rev, 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)