Termination w.r.t. Q proof of ../tpdb/TRS/higher-order/Bird/Ex2_8

NO Termination w.r.t. Q proof of ../tpdb/TRS/higher-order/Bird/Ex2_8_1ConstSubstFix.trs
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(const, x), y) → x
app(app(app(subst, f), g), x) → app(app(f, x), app(g, x))
app(app(fix, f), x) → app(app(f, app(fix, f)), x)

Q is empty.

↳ QTRS

  ↳ Overlay + Local Confluence

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

app(app(const, x), y) → x
app(app(app(subst, f), g), x) → app(app(f, x), app(g, x))
app(app(fix, f), x) → app(app(f, app(fix, f)), x)

Q is empty.

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

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

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

app(app(const, x), y) → x
app(app(app(subst, f), g), x) → app(app(f, x), app(g, x))
app(app(fix, f), x) → app(app(f, app(fix, f)), x)

The set Q consists of the following terms:

app(app(const, x0), x1)
app(app(app(subst, x0), x1), x2)
app(app(fix, x0), x1)

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(fix, f), x) → APP(f, app(fix, f))
APP(app(fix, f), x) → APP(app(f, app(fix, f)), x)
APP(app(app(subst, f), g), x) → APP(f, x)
APP(app(app(subst, f), g), x) → APP(app(f, x), app(g, x))
APP(app(app(subst, f), g), x) → APP(g, x)

The TRS R consists of the following rules:

app(app(const, x), y) → x
app(app(app(subst, f), g), x) → app(app(f, x), app(g, x))
app(app(fix, f), x) → app(app(f, app(fix, f)), x)

The set Q consists of the following terms:

app(app(const, x0), x1)
app(app(app(subst, x0), x1), x2)
app(app(fix, x0), x1)

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

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ ForwardInstantiation

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

APP(app(fix, f), x) → APP(f, app(fix, f))
APP(app(fix, f), x) → APP(app(f, app(fix, f)), x)
APP(app(app(subst, f), g), x) → APP(f, x)
APP(app(app(subst, f), g), x) → APP(app(f, x), app(g, x))
APP(app(app(subst, f), g), x) → APP(g, x)

The TRS R consists of the following rules:

app(app(const, x), y) → x
app(app(app(subst, f), g), x) → app(app(f, x), app(g, x))
app(app(fix, f), x) → app(app(f, app(fix, f)), x)

The set Q consists of the following terms:

app(app(const, x0), x1)
app(app(app(subst, x0), x1), x2)
app(app(fix, x0), x1)

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

APP(app(app(subst, app(app(subst, y_0), y_1)), x1), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(app(subst, app(fix, y_0)), x1), x2) → APP(app(fix, y_0), x2)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ ForwardInstantiation

            ↳ QDP

              ↳ ForwardInstantiation

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

APP(app(app(subst, app(app(subst, y_0), y_1)), x1), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(fix, f), x) → APP(app(f, app(fix, f)), x)
APP(app(fix, f), x) → APP(f, app(fix, f))
APP(app(app(subst, f), g), x) → APP(app(f, x), app(g, x))
APP(app(app(subst, app(fix, y_0)), x1), x2) → APP(app(fix, y_0), x2)
APP(app(app(subst, f), g), x) → APP(g, x)

The TRS R consists of the following rules:

app(app(const, x), y) → x
app(app(app(subst, f), g), x) → app(app(f, x), app(g, x))
app(app(fix, f), x) → app(app(f, app(fix, f)), x)

The set Q consists of the following terms:

app(app(const, x0), x1)
app(app(app(subst, x0), x1), x2)
app(app(fix, x0), x1)

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

APP(app(app(subst, x0), app(app(subst, app(app(subst, y_0), y_1)), y_2)), x2) → APP(app(app(subst, app(app(subst, y_0), y_1)), y_2), x2)
APP(app(app(subst, x0), app(fix, y_0)), x2) → APP(app(fix, y_0), x2)
APP(app(app(subst, x0), app(app(subst, y_0), y_1)), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(app(subst, x0), app(app(subst, app(fix, y_0)), y_1)), x2) → APP(app(app(subst, app(fix, y_0)), y_1), x2)

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ ForwardInstantiation

            ↳ QDP

              ↳ ForwardInstantiation

                ↳ QDP

                  ↳ ForwardInstantiation

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

APP(app(app(subst, x0), app(fix, y_0)), x2) → APP(app(fix, y_0), x2)
APP(app(app(subst, x0), app(app(subst, app(app(subst, y_0), y_1)), y_2)), x2) → APP(app(app(subst, app(app(subst, y_0), y_1)), y_2), x2)
APP(app(app(subst, x0), app(app(subst, y_0), y_1)), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(app(subst, app(app(subst, y_0), y_1)), x1), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(fix, f), x) → APP(f, app(fix, f))
APP(app(fix, f), x) → APP(app(f, app(fix, f)), x)
APP(app(app(subst, f), g), x) → APP(app(f, x), app(g, x))
APP(app(app(subst, x0), app(app(subst, app(fix, y_0)), y_1)), x2) → APP(app(app(subst, app(fix, y_0)), y_1), x2)
APP(app(app(subst, app(fix, y_0)), x1), x2) → APP(app(fix, y_0), x2)

The TRS R consists of the following rules:

app(app(const, x), y) → x
app(app(app(subst, f), g), x) → app(app(f, x), app(g, x))
app(app(fix, f), x) → app(app(f, app(fix, f)), x)

The set Q consists of the following terms:

app(app(const, x0), x1)
app(app(app(subst, x0), x1), x2)
app(app(fix, x0), x1)

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

APP(app(fix, app(app(subst, app(fix, y_0)), y_1)), x1) → APP(app(app(subst, app(fix, y_0)), y_1), app(fix, app(app(subst, app(fix, y_0)), y_1)))
APP(app(fix, app(app(subst, app(app(subst, y_0), y_1)), y_2)), x1) → APP(app(app(subst, app(app(subst, y_0), y_1)), y_2), app(fix, app(app(subst, app(app(subst, y_0), y_1)), y_2)))
APP(app(fix, app(fix, y_0)), x1) → APP(app(fix, y_0), app(fix, app(fix, y_0)))
APP(app(fix, app(app(subst, y_0), y_1)), x1) → APP(app(app(subst, y_0), y_1), app(fix, app(app(subst, y_0), y_1)))
APP(app(fix, app(app(subst, y_0), app(fix, y_1))), x1) → APP(app(app(subst, y_0), app(fix, y_1)), app(fix, app(app(subst, y_0), app(fix, y_1))))
APP(app(fix, app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2))), x1) → APP(app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2)), app(fix, app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2))))
APP(app(fix, app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3))), x1) → APP(app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3)), app(fix, app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3))))
APP(app(fix, app(app(subst, y_0), app(app(subst, y_1), y_2))), x1) → APP(app(app(subst, y_0), app(app(subst, y_1), y_2)), app(fix, app(app(subst, y_0), app(app(subst, y_1), y_2))))

↳ QTRS

  ↳ Overlay + Local Confluence

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ ForwardInstantiation

            ↳ QDP

              ↳ ForwardInstantiation

                ↳ QDP

                  ↳ ForwardInstantiation

                    ↳ QDP

                      ↳ NonTerminationProof

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

APP(app(fix, app(app(subst, app(fix, y_0)), y_1)), x1) → APP(app(app(subst, app(fix, y_0)), y_1), app(fix, app(app(subst, app(fix, y_0)), y_1)))
APP(app(app(subst, x0), app(app(subst, y_0), y_1)), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(fix, app(fix, y_0)), x1) → APP(app(fix, y_0), app(fix, app(fix, y_0)))
APP(app(fix, app(app(subst, y_0), app(fix, y_1))), x1) → APP(app(app(subst, y_0), app(fix, y_1)), app(fix, app(app(subst, y_0), app(fix, y_1))))
APP(app(fix, app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3))), x1) → APP(app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3)), app(fix, app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3))))
APP(app(app(subst, x0), app(app(subst, app(fix, y_0)), y_1)), x2) → APP(app(app(subst, app(fix, y_0)), y_1), x2)
APP(app(app(subst, x0), app(fix, y_0)), x2) → APP(app(fix, y_0), x2)
APP(app(app(subst, x0), app(app(subst, app(app(subst, y_0), y_1)), y_2)), x2) → APP(app(app(subst, app(app(subst, y_0), y_1)), y_2), x2)
APP(app(fix, app(app(subst, app(app(subst, y_0), y_1)), y_2)), x1) → APP(app(app(subst, app(app(subst, y_0), y_1)), y_2), app(fix, app(app(subst, app(app(subst, y_0), y_1)), y_2)))
APP(app(app(subst, app(app(subst, y_0), y_1)), x1), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(fix, f), x) → APP(app(f, app(fix, f)), x)
APP(app(fix, app(app(subst, y_0), y_1)), x1) → APP(app(app(subst, y_0), y_1), app(fix, app(app(subst, y_0), y_1)))
APP(app(app(subst, f), g), x) → APP(app(f, x), app(g, x))
APP(app(fix, app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2))), x1) → APP(app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2)), app(fix, app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2))))
APP(app(app(subst, app(fix, y_0)), x1), x2) → APP(app(fix, y_0), x2)
APP(app(fix, app(app(subst, y_0), app(app(subst, y_1), y_2))), x1) → APP(app(app(subst, y_0), app(app(subst, y_1), y_2)), app(fix, app(app(subst, y_0), app(app(subst, y_1), y_2))))

The TRS R consists of the following rules:

app(app(const, x), y) → x
app(app(app(subst, f), g), x) → app(app(f, x), app(g, x))
app(app(fix, f), x) → app(app(f, app(fix, f)), x)

The set Q consists of the following terms:

app(app(const, x0), x1)
app(app(app(subst, x0), x1), x2)
app(app(fix, x0), x1)

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 narrowing to the left:

The TRS P consists of the following rules:

APP(app(fix, app(app(subst, app(fix, y_0)), y_1)), x1) → APP(app(app(subst, app(fix, y_0)), y_1), app(fix, app(app(subst, app(fix, y_0)), y_1)))
APP(app(app(subst, x0), app(app(subst, y_0), y_1)), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(fix, app(fix, y_0)), x1) → APP(app(fix, y_0), app(fix, app(fix, y_0)))
APP(app(fix, app(app(subst, y_0), app(fix, y_1))), x1) → APP(app(app(subst, y_0), app(fix, y_1)), app(fix, app(app(subst, y_0), app(fix, y_1))))
APP(app(fix, app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3))), x1) → APP(app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3)), app(fix, app(app(subst, y_0), app(app(subst, app(app(subst, y_1), y_2)), y_3))))
APP(app(app(subst, x0), app(app(subst, app(fix, y_0)), y_1)), x2) → APP(app(app(subst, app(fix, y_0)), y_1), x2)
APP(app(app(subst, x0), app(fix, y_0)), x2) → APP(app(fix, y_0), x2)
APP(app(app(subst, x0), app(app(subst, app(app(subst, y_0), y_1)), y_2)), x2) → APP(app(app(subst, app(app(subst, y_0), y_1)), y_2), x2)
APP(app(fix, app(app(subst, app(app(subst, y_0), y_1)), y_2)), x1) → APP(app(app(subst, app(app(subst, y_0), y_1)), y_2), app(fix, app(app(subst, app(app(subst, y_0), y_1)), y_2)))
APP(app(app(subst, app(app(subst, y_0), y_1)), x1), x2) → APP(app(app(subst, y_0), y_1), x2)
APP(app(fix, f), x) → APP(app(f, app(fix, f)), x)
APP(app(fix, app(app(subst, y_0), y_1)), x1) → APP(app(app(subst, y_0), y_1), app(fix, app(app(subst, y_0), y_1)))
APP(app(app(subst, f), g), x) → APP(app(f, x), app(g, x))
APP(app(fix, app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2))), x1) → APP(app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2)), app(fix, app(app(subst, y_0), app(app(subst, app(fix, y_1)), y_2))))
APP(app(app(subst, app(fix, y_0)), x1), x2) → APP(app(fix, y_0), x2)
APP(app(fix, app(app(subst, y_0), app(app(subst, y_1), y_2))), x1) → APP(app(app(subst, y_0), app(app(subst, y_1), y_2)), app(fix, app(app(subst, y_0), app(app(subst, y_1), y_2))))

The TRS R consists of the following rules:

app(app(const, x), y) → x
app(app(app(subst, f), g), x) → app(app(f, x), app(g, x))
app(app(fix, f), x) → app(app(f, app(fix, f)), x)

s = APP(app(fix, fix), x) evaluates to t =APP(app(fix, fix), app(fix, app(fix, fix)))

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

Matcher: [x / app(fix, app(fix, fix))]
Semiunifier: [ ]

Rewriting sequence

APP(app(fix, fix), x) → APP(app(fix, app(fix, fix)), x)
with rule APP(app(fix, f), x') → APP(app(f, app(fix, f)), x') at position [] and matcher [x' / x, f / fix]

APP(app(fix, app(fix, fix)), x) → APP(app(fix, fix), app(fix, app(fix, fix)))
with rule APP(app(fix, app(fix, y_0)), x1) → APP(app(fix, y_0), app(fix, app(fix, y_0)))

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence

All these steps are and every following step will be a correct step w.r.t to Q.