Termination w.r.t. Q proof of /tmp/tmp

Termination w.r.t. Q of the following Term Rewriting System could be disproven:

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

app(app(f, 0), n) → app(app(hd, app(app(map, f), app(app(cons, 0), nil))), n)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))

The set Q consists of the following terms:

app(app(map, x0), nil)
app(app(x0, 0), x1)
app(app(map, x0), app(app(cons, x1), x2))

↳ QTRS

  ↳ DependencyPairsProof

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

app(app(f, 0), n) → app(app(hd, app(app(map, f), app(app(cons, 0), nil))), n)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))

The set Q consists of the following terms:

app(app(map, x0), nil)
app(app(x0, 0), x1)
app(app(map, x0), app(app(cons, x1), x2))

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

APP(app(f, 0), n) → APP(app(cons, 0), nil)
APP(app(f, 0), n) → APP(map, f)
APP(app(f, 0), n) → APP(app(map, f), app(app(cons, 0), nil))
APP(app(map, f), app(app(cons, x), xs)) → APP(cons, app(f, x))
APP(app(f, 0), n) → APP(hd, app(app(map, f), app(app(cons, 0), nil)))
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(f, 0), n) → APP(app(hd, app(app(map, f), app(app(cons, 0), nil))), n)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
APP(app(f, 0), n) → APP(cons, 0)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(cons, app(f, x)), app(app(map, f), xs))

The TRS R consists of the following rules:

app(app(f, 0), n) → app(app(hd, app(app(map, f), app(app(cons, 0), nil))), n)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))

The set Q consists of the following terms:

app(app(map, x0), nil)
app(app(x0, 0), x1)
app(app(map, x0), app(app(cons, x1), x2))

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

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

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

APP(app(f, 0), n) → APP(app(cons, 0), nil)
APP(app(f, 0), n) → APP(map, f)
APP(app(f, 0), n) → APP(app(map, f), app(app(cons, 0), nil))
APP(app(map, f), app(app(cons, x), xs)) → APP(cons, app(f, x))
APP(app(f, 0), n) → APP(hd, app(app(map, f), app(app(cons, 0), nil)))
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(f, 0), n) → APP(app(hd, app(app(map, f), app(app(cons, 0), nil))), n)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
APP(app(f, 0), n) → APP(cons, 0)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(cons, app(f, x)), app(app(map, f), xs))

The TRS R consists of the following rules:

app(app(f, 0), n) → app(app(hd, app(app(map, f), app(app(cons, 0), nil))), n)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))

The set Q consists of the following terms:

app(app(map, x0), nil)
app(app(x0, 0), x1)
app(app(map, x0), app(app(cons, x1), x2))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 4 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

          ↳ NonTerminationProof

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

APP(app(f, 0), n) → APP(app(cons, 0), nil)
APP(app(f, 0), n) → APP(app(map, f), app(app(cons, 0), nil))
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(f, 0), n) → APP(app(hd, app(app(map, f), app(app(cons, 0), nil))), n)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(cons, app(f, x)), app(app(map, f), xs))

The TRS R consists of the following rules:

app(app(f, 0), n) → app(app(hd, app(app(map, f), app(app(cons, 0), nil))), n)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))

The set Q consists of the following terms:

app(app(map, x0), nil)
app(app(x0, 0), x1)
app(app(map, x0), app(app(cons, x1), x2))

We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule APP(app(f, 0), n) → APP(app(map, f), app(app(cons, 0), nil)) at position [1] we obtained the following new rules:

APP(app(y0, 0), y1) → APP(app(map, y0), app(app(hd, app(app(map, cons), app(app(cons, 0), nil))), nil))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

          ↳ NonTerminationProof

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

APP(app(f, 0), n) → APP(app(cons, 0), nil)
APP(app(y0, 0), y1) → APP(app(map, y0), app(app(hd, app(app(map, cons), app(app(cons, 0), nil))), nil))
APP(app(f, 0), n) → APP(app(hd, app(app(map, f), app(app(cons, 0), nil))), n)
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(cons, app(f, x)), app(app(map, f), xs))

The TRS R consists of the following rules:

app(app(f, 0), n) → app(app(hd, app(app(map, f), app(app(cons, 0), nil))), n)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))

The set Q consists of the following terms:

app(app(map, x0), nil)
app(app(x0, 0), x1)
app(app(map, x0), app(app(cons, x1), x2))

We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule APP(app(f, 0), n) → APP(app(hd, app(app(map, f), app(app(cons, 0), nil))), n) at position [0,1,1] we obtained the following new rules:

APP(app(y0, 0), y1) → APP(app(hd, app(app(map, y0), app(app(hd, app(app(map, cons), app(app(cons, 0), nil))), nil))), y1)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

          ↳ NonTerminationProof

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

APP(app(f, 0), n) → APP(app(cons, 0), nil)
APP(app(y0, 0), y1) → APP(app(hd, app(app(map, y0), app(app(hd, app(app(map, cons), app(app(cons, 0), nil))), nil))), y1)
APP(app(y0, 0), y1) → APP(app(map, y0), app(app(hd, app(app(map, cons), app(app(cons, 0), nil))), nil))
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(cons, app(f, x)), app(app(map, f), xs))

The TRS R consists of the following rules:

app(app(f, 0), n) → app(app(hd, app(app(map, f), app(app(cons, 0), nil))), n)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))

The set Q consists of the following terms:

app(app(map, x0), nil)
app(app(x0, 0), x1)
app(app(map, x0), app(app(cons, x1), x2))

We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule APP(app(map, f), app(app(cons, x), xs)) → APP(app(cons, app(f, x)), app(app(map, f), xs)) at position [0,1] we obtained the following new rules:

APP(app(map, app(x0, 0)), app(app(cons, x1), y2)) → APP(app(cons, app(app(hd, app(app(map, x0), app(app(cons, 0), nil))), x1)), app(app(map, app(x0, 0)), y2))
APP(app(map, app(map, x0)), app(app(cons, nil), y2)) → APP(app(cons, nil), app(app(map, app(map, x0)), y2))
APP(app(map, app(map, x0)), app(app(cons, app(app(cons, x1), x2)), y2)) → APP(app(cons, app(app(cons, app(x0, x1)), app(app(map, x0), x2))), app(app(map, app(map, x0)), y2))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

          ↳ NonTerminationProof

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

APP(app(map, app(x0, 0)), app(app(cons, x1), y2)) → APP(app(cons, app(app(hd, app(app(map, x0), app(app(cons, 0), nil))), x1)), app(app(map, app(x0, 0)), y2))
APP(app(f, 0), n) → APP(app(cons, 0), nil)
APP(app(y0, 0), y1) → APP(app(hd, app(app(map, y0), app(app(hd, app(app(map, cons), app(app(cons, 0), nil))), nil))), y1)
APP(app(map, app(map, x0)), app(app(cons, nil), y2)) → APP(app(cons, nil), app(app(map, app(map, x0)), y2))
APP(app(y0, 0), y1) → APP(app(map, y0), app(app(hd, app(app(map, cons), app(app(cons, 0), nil))), nil))
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(map, app(map, x0)), app(app(cons, app(app(cons, x1), x2)), y2)) → APP(app(cons, app(app(cons, app(x0, x1)), app(app(map, x0), x2))), app(app(map, app(map, x0)), y2))
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)

The TRS R consists of the following rules:

app(app(f, 0), n) → app(app(hd, app(app(map, f), app(app(cons, 0), nil))), n)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))

The set Q consists of the following terms:

app(app(map, x0), nil)
app(app(x0, 0), x1)
app(app(map, x0), app(app(cons, x1), x2))

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 1 less node.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ ForwardInstantiation

          ↳ NonTerminationProof

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

APP(app(map, app(x0, 0)), app(app(cons, x1), y2)) → APP(app(cons, app(app(hd, app(app(map, x0), app(app(cons, 0), nil))), x1)), app(app(map, app(x0, 0)), y2))
APP(app(f, 0), n) → APP(app(cons, 0), nil)
APP(app(y0, 0), y1) → APP(app(hd, app(app(map, y0), app(app(hd, app(app(map, cons), app(app(cons, 0), nil))), nil))), y1)
APP(app(y0, 0), y1) → APP(app(map, y0), app(app(hd, app(app(map, cons), app(app(cons, 0), nil))), nil))
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(map, app(map, x0)), app(app(cons, app(app(cons, x1), x2)), y2)) → APP(app(cons, app(app(cons, app(x0, x1)), app(app(map, x0), x2))), app(app(map, app(map, x0)), y2))
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)

The TRS R consists of the following rules:

app(app(f, 0), n) → app(app(hd, app(app(map, f), app(app(cons, 0), nil))), n)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))

The set Q consists of the following terms:

app(app(map, x0), nil)
app(app(x0, 0), x1)
app(app(map, x0), app(app(cons, x1), x2))

We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule APP(app(map, f), app(app(cons, x), xs)) → APP(f, x) we obtained the following new rules:

APP(app(map, app(map, app(map, y_0))), app(app(cons, app(app(cons, app(app(cons, y_1), y_2)), y_3)), x2)) → APP(app(map, app(map, y_0)), app(app(cons, app(app(cons, y_1), y_2)), y_3))
APP(app(map, app(map, app(y_0, 0))), app(app(cons, app(app(cons, y_1), y_2)), x2)) → APP(app(map, app(y_0, 0)), app(app(cons, y_1), y_2))
APP(app(map, app(map, y_0)), app(app(cons, app(app(cons, y_1), y_2)), x2)) → APP(app(map, y_0), app(app(cons, y_1), y_2))
APP(app(map, app(y_0, 0)), app(app(cons, x1), x2)) → APP(app(y_0, 0), x1)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ ForwardInstantiation

                            ↳ QDP

                              ↳ ForwardInstantiation

          ↳ NonTerminationProof

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

APP(app(map, app(x0, 0)), app(app(cons, x1), y2)) → APP(app(cons, app(app(hd, app(app(map, x0), app(app(cons, 0), nil))), x1)), app(app(map, app(x0, 0)), y2))
APP(app(f, 0), n) → APP(app(cons, 0), nil)
APP(app(map, app(map, app(map, y_0))), app(app(cons, app(app(cons, app(app(cons, y_1), y_2)), y_3)), x2)) → APP(app(map, app(map, y_0)), app(app(cons, app(app(cons, y_1), y_2)), y_3))
APP(app(map, app(map, app(y_0, 0))), app(app(cons, app(app(cons, y_1), y_2)), x2)) → APP(app(map, app(y_0, 0)), app(app(cons, y_1), y_2))
APP(app(y0, 0), y1) → APP(app(hd, app(app(map, y0), app(app(hd, app(app(map, cons), app(app(cons, 0), nil))), nil))), y1)
APP(app(map, app(map, y_0)), app(app(cons, app(app(cons, y_1), y_2)), x2)) → APP(app(map, y_0), app(app(cons, y_1), y_2))
APP(app(y0, 0), y1) → APP(app(map, y0), app(app(hd, app(app(map, cons), app(app(cons, 0), nil))), nil))
APP(app(map, app(y_0, 0)), app(app(cons, x1), x2)) → APP(app(y_0, 0), x1)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
APP(app(map, app(map, x0)), app(app(cons, app(app(cons, x1), x2)), y2)) → APP(app(cons, app(app(cons, app(x0, x1)), app(app(map, x0), x2))), app(app(map, app(map, x0)), y2))

The TRS R consists of the following rules:

app(app(f, 0), n) → app(app(hd, app(app(map, f), app(app(cons, 0), nil))), n)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))

The set Q consists of the following terms:

app(app(map, x0), nil)
app(app(x0, 0), x1)
app(app(map, x0), app(app(cons, x1), x2))

We have to consider all minimal (P,Q,R)-chains.
By forward instantiating [14] the rule APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs) we obtained the following new rules:

APP(app(map, app(map, y_0)), app(app(cons, x1), app(app(cons, app(app(cons, y_1), y_2)), y_3))) → APP(app(map, app(map, y_0)), app(app(cons, app(app(cons, y_1), y_2)), y_3))
APP(app(map, app(map, app(y_0, 0))), app(app(cons, x1), app(app(cons, app(app(cons, y_1), y_2)), y_3))) → APP(app(map, app(map, app(y_0, 0))), app(app(cons, app(app(cons, y_1), y_2)), y_3))
APP(app(map, app(map, app(map, y_0))), app(app(cons, x1), app(app(cons, app(app(cons, app(app(cons, y_1), y_2)), y_3)), y_4))) → APP(app(map, app(map, app(map, y_0))), app(app(cons, app(app(cons, app(app(cons, y_1), y_2)), y_3)), y_4))
APP(app(map, 0), app(app(cons, x1), x2)) → APP(app(map, 0), x2)
APP(app(map, x0), app(app(cons, x1), app(app(cons, y_1), y_2))) → APP(app(map, x0), app(app(cons, y_1), y_2))
APP(app(map, app(y_0, 0)), app(app(cons, x1), app(app(cons, y_1), y_2))) → APP(app(map, app(y_0, 0)), app(app(cons, y_1), y_2))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

          ↳ Narrowing

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ DependencyGraphProof

                        ↳ QDP

                          ↳ ForwardInstantiation

                            ↳ QDP

                              ↳ ForwardInstantiation

                                ↳ QDP

                                  ↳ NonTerminationProof

          ↳ NonTerminationProof

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

APP(app(f, 0), n) → APP(app(cons, 0), nil)
APP(app(map, app(map, app(map, y_0))), app(app(cons, app(app(cons, app(app(cons, y_1), y_2)), y_3)), x2)) → APP(app(map, app(map, y_0)), app(app(cons, app(app(cons, y_1), y_2)), y_3))
APP(app(map, app(map, app(map, y_0))), app(app(cons, x1), app(app(cons, app(app(cons, app(app(cons, y_1), y_2)), y_3)), y_4))) → APP(app(map, app(map, app(map, y_0))), app(app(cons, app(app(cons, app(app(cons, y_1), y_2)), y_3)), y_4))
APP(app(map, 0), app(app(cons, x1), x2)) → APP(app(map, 0), x2)
APP(app(map, app(map, y_0)), app(app(cons, app(app(cons, y_1), y_2)), x2)) → APP(app(map, y_0), app(app(cons, y_1), y_2))
APP(app(map, app(y_0, 0)), app(app(cons, x1), x2)) → APP(app(y_0, 0), x1)
APP(app(map, app(map, x0)), app(app(cons, app(app(cons, x1), x2)), y2)) → APP(app(cons, app(app(cons, app(x0, x1)), app(app(map, x0), x2))), app(app(map, app(map, x0)), y2))
APP(app(map, app(x0, 0)), app(app(cons, x1), y2)) → APP(app(cons, app(app(hd, app(app(map, x0), app(app(cons, 0), nil))), x1)), app(app(map, app(x0, 0)), y2))
APP(app(map, app(map, y_0)), app(app(cons, x1), app(app(cons, app(app(cons, y_1), y_2)), y_3))) → APP(app(map, app(map, y_0)), app(app(cons, app(app(cons, y_1), y_2)), y_3))
APP(app(map, app(map, app(y_0, 0))), app(app(cons, x1), app(app(cons, app(app(cons, y_1), y_2)), y_3))) → APP(app(map, app(map, app(y_0, 0))), app(app(cons, app(app(cons, y_1), y_2)), y_3))
APP(app(map, app(map, app(y_0, 0))), app(app(cons, app(app(cons, y_1), y_2)), x2)) → APP(app(map, app(y_0, 0)), app(app(cons, y_1), y_2))
APP(app(y0, 0), y1) → APP(app(hd, app(app(map, y0), app(app(hd, app(app(map, cons), app(app(cons, 0), nil))), nil))), y1)
APP(app(y0, 0), y1) → APP(app(map, y0), app(app(hd, app(app(map, cons), app(app(cons, 0), nil))), nil))
APP(app(map, x0), app(app(cons, x1), app(app(cons, y_1), y_2))) → APP(app(map, x0), app(app(cons, y_1), y_2))
APP(app(map, app(y_0, 0)), app(app(cons, x1), app(app(cons, y_1), y_2))) → APP(app(map, app(y_0, 0)), app(app(cons, y_1), y_2))

The TRS R consists of the following rules:

app(app(f, 0), n) → app(app(hd, app(app(map, f), app(app(cons, 0), nil))), n)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))

The set Q consists of the following terms:

app(app(map, x0), nil)
app(app(x0, 0), x1)
app(app(map, x0), app(app(cons, x1), x2))

We have to consider all minimal (P,Q,R)-chains.
We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

APP(app(f, 0), n) → APP(app(cons, 0), nil)
APP(app(map, app(map, app(map, y_0))), app(app(cons, app(app(cons, app(app(cons, y_1), y_2)), y_3)), x2)) → APP(app(map, app(map, y_0)), app(app(cons, app(app(cons, y_1), y_2)), y_3))
APP(app(map, app(map, app(map, y_0))), app(app(cons, x1), app(app(cons, app(app(cons, app(app(cons, y_1), y_2)), y_3)), y_4))) → APP(app(map, app(map, app(map, y_0))), app(app(cons, app(app(cons, app(app(cons, y_1), y_2)), y_3)), y_4))
APP(app(map, 0), app(app(cons, x1), x2)) → APP(app(map, 0), x2)
APP(app(map, app(map, y_0)), app(app(cons, app(app(cons, y_1), y_2)), x2)) → APP(app(map, y_0), app(app(cons, y_1), y_2))
APP(app(map, app(y_0, 0)), app(app(cons, x1), x2)) → APP(app(y_0, 0), x1)
APP(app(map, app(map, x0)), app(app(cons, app(app(cons, x1), x2)), y2)) → APP(app(cons, app(app(cons, app(x0, x1)), app(app(map, x0), x2))), app(app(map, app(map, x0)), y2))
APP(app(map, app(x0, 0)), app(app(cons, x1), y2)) → APP(app(cons, app(app(hd, app(app(map, x0), app(app(cons, 0), nil))), x1)), app(app(map, app(x0, 0)), y2))
APP(app(map, app(map, y_0)), app(app(cons, x1), app(app(cons, app(app(cons, y_1), y_2)), y_3))) → APP(app(map, app(map, y_0)), app(app(cons, app(app(cons, y_1), y_2)), y_3))
APP(app(map, app(map, app(y_0, 0))), app(app(cons, x1), app(app(cons, app(app(cons, y_1), y_2)), y_3))) → APP(app(map, app(map, app(y_0, 0))), app(app(cons, app(app(cons, y_1), y_2)), y_3))
APP(app(map, app(map, app(y_0, 0))), app(app(cons, app(app(cons, y_1), y_2)), x2)) → APP(app(map, app(y_0, 0)), app(app(cons, y_1), y_2))
APP(app(y0, 0), y1) → APP(app(hd, app(app(map, y0), app(app(hd, app(app(map, cons), app(app(cons, 0), nil))), nil))), y1)
APP(app(y0, 0), y1) → APP(app(map, y0), app(app(hd, app(app(map, cons), app(app(cons, 0), nil))), nil))
APP(app(map, x0), app(app(cons, x1), app(app(cons, y_1), y_2))) → APP(app(map, x0), app(app(cons, y_1), y_2))
APP(app(map, app(y_0, 0)), app(app(cons, x1), app(app(cons, y_1), y_2))) → APP(app(map, app(y_0, 0)), app(app(cons, y_1), y_2))

The TRS R consists of the following rules:

app(app(f, 0), n) → app(app(hd, app(app(map, f), app(app(cons, 0), nil))), n)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))

s = APP(app(f, 0), n) evaluates to t =APP(app(cons, 0), nil)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [n / nil, f / cons]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from APP(app(f, 0), n) to APP(app(cons, 0), nil).

We used the non-termination processor [17] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

The TRS P consists of the following rules:

APP(app(f, 0), n) → APP(app(cons, 0), nil)
APP(app(f, 0), n) → APP(app(map, f), app(app(cons, 0), nil))
APP(app(map, f), app(app(cons, x), xs)) → APP(f, x)
APP(app(f, 0), n) → APP(app(hd, app(app(map, f), app(app(cons, 0), nil))), n)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(map, f), xs)
APP(app(map, f), app(app(cons, x), xs)) → APP(app(cons, app(f, x)), app(app(map, f), xs))

The TRS R consists of the following rules:

app(app(f, 0), n) → app(app(hd, app(app(map, f), app(app(cons, 0), nil))), n)
app(app(map, f), nil) → nil
app(app(map, f), app(app(cons, x), xs)) → app(app(cons, app(f, x)), app(app(map, f), xs))

s = APP(app(f, 0), n) evaluates to t =APP(app(cons, 0), nil)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

Semiunifier: [ ]
Matcher: [n / nil, f / cons]

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from APP(app(f, 0), n) to APP(app(cons, 0), nil).