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

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

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

f(true, x, y) → f(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
plus(plus(n, m), u) → plus(n, plus(m, u))
double(0) → 0
double(s(x)) → s(s(double(x)))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
f(true, x0, x1)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

↳ QTRS

  ↳ DependencyPairsProof

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

f(true, x, y) → f(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
plus(plus(n, m), u) → plus(n, plus(m, u))
double(0) → 0
double(s(x)) → s(s(double(x)))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
f(true, x0, x1)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

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

DOUBLE(s(x)) → DOUBLE(x)
PLUS(plus(n, m), u) → PLUS(n, plus(m, u))
F(true, x, y) → GT(y, s(s(0)))
PLUS(plus(n, m), u) → PLUS(m, u)
F(true, x, y) → F(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))
F(true, x, y) → GT(x, y)
GT(s(u), s(v)) → GT(u, v)
F(true, x, y) → DOUBLE(y)
PLUS(n, s(m)) → PLUS(n, m)
F(true, x, y) → PLUS(s(0), x)
F(true, x, y) → AND(gt(x, y), gt(y, s(s(0))))

The TRS R consists of the following rules:

f(true, x, y) → f(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
plus(plus(n, m), u) → plus(n, plus(m, u))
double(0) → 0
double(s(x)) → s(s(double(x)))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
f(true, x0, x1)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, 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:

DOUBLE(s(x)) → DOUBLE(x)
PLUS(plus(n, m), u) → PLUS(n, plus(m, u))
F(true, x, y) → GT(y, s(s(0)))
PLUS(plus(n, m), u) → PLUS(m, u)
F(true, x, y) → F(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))
F(true, x, y) → GT(x, y)
GT(s(u), s(v)) → GT(u, v)
F(true, x, y) → DOUBLE(y)
PLUS(n, s(m)) → PLUS(n, m)
F(true, x, y) → PLUS(s(0), x)
F(true, x, y) → AND(gt(x, y), gt(y, s(s(0))))

The TRS R consists of the following rules:

f(true, x, y) → f(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
plus(plus(n, m), u) → plus(n, plus(m, u))
double(0) → 0
double(s(x)) → s(s(double(x)))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
f(true, x0, x1)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [13,14,18] contains 4 SCCs with 5 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

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

DOUBLE(s(x)) → DOUBLE(x)

The TRS R consists of the following rules:

f(true, x, y) → f(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
plus(plus(n, m), u) → plus(n, plus(m, u))
double(0) → 0
double(s(x)) → s(s(double(x)))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
f(true, x0, x1)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [13] we can delete all non-usable rules [14] from R.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

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

DOUBLE(s(x)) → DOUBLE(x)

R is empty.
The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
f(true, x0, x1)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
f(true, x0, x1)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

          ↳ QDP

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

DOUBLE(s(x)) → DOUBLE(x)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [16] together with the size-change analysis [27] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

DOUBLE(s(x)) → DOUBLE(x)
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

          ↳ QDP

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

PLUS(plus(n, m), u) → PLUS(n, plus(m, u))
PLUS(plus(n, m), u) → PLUS(m, u)
PLUS(n, s(m)) → PLUS(n, m)

The TRS R consists of the following rules:

f(true, x, y) → f(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
plus(plus(n, m), u) → plus(n, plus(m, u))
double(0) → 0
double(s(x)) → s(s(double(x)))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
f(true, x0, x1)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

          ↳ QDP

          ↳ QDP

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

PLUS(plus(n, m), u) → PLUS(n, plus(m, u))
PLUS(plus(n, m), u) → PLUS(m, u)
PLUS(n, s(m)) → PLUS(n, m)

The TRS R consists of the following rules:

plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
f(true, x0, x1)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

double(0)
gt(0, x0)
gt(s(x0), s(x1))
f(true, x0, x1)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ QDPSizeChangeProof

          ↳ QDP

          ↳ QDP

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

PLUS(plus(n, m), u) → PLUS(n, plus(m, u))
PLUS(plus(n, m), u) → PLUS(m, u)
PLUS(n, s(m)) → PLUS(n, m)

The TRS R consists of the following rules:

plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

plus(x0, s(x1))
plus(x0, 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [16] together with the size-change analysis [27] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

PLUS(n, s(m)) → PLUS(n, m)
The graph contains the following edges 1 >= 1, 2 > 2
PLUS(plus(n, m), u) → PLUS(m, u)
The graph contains the following edges 1 > 1, 2 >= 2
PLUS(plus(n, m), u) → PLUS(n, plus(m, u))
The graph contains the following edges 1 > 1

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

          ↳ QDP

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

GT(s(u), s(v)) → GT(u, v)

The TRS R consists of the following rules:

f(true, x, y) → f(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
plus(plus(n, m), u) → plus(n, plus(m, u))
double(0) → 0
double(s(x)) → s(s(double(x)))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
f(true, x0, x1)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

          ↳ QDP

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

GT(s(u), s(v)) → GT(u, v)

R is empty.
The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
f(true, x0, x1)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
f(true, x0, x1)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ QDPSizeChangeProof

          ↳ QDP

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

GT(s(u), s(v)) → GT(u, v)

From the DPs we obtained the following set of size-change graphs:

GT(s(u), s(v)) → GT(u, v)
The graph contains the following edges 1 > 1, 2 > 2

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

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

F(true, x, y) → F(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))

The TRS R consists of the following rules:

f(true, x, y) → f(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))
gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
plus(plus(n, m), u) → plus(n, plus(m, u))
double(0) → 0
double(s(x)) → s(s(double(x)))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
f(true, x0, x1)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

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

F(true, x, y) → F(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
f(true, x0, x1)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.

f(true, x0, x1)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                    ↳ NonInfProof

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

F(true, x, y) → F(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By narrowing [13] the rule F(true, x, y) → F(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y)) at position [0] we obtained the following new rules:

F(true, y0, s(x0)) → F(and(gt(y0, s(x0)), gt(x0, s(0))), plus(s(0), y0), double(s(x0)))
F(true, s(x0), s(x1)) → F(and(gt(x0, x1), gt(s(x1), s(s(0)))), plus(s(0), s(x0)), double(s(x1)))
F(true, 0, x0) → F(and(false, gt(x0, s(s(0)))), plus(s(0), 0), double(x0))
F(true, y0, 0) → F(and(gt(y0, 0), false), plus(s(0), y0), double(0))
F(true, s(x0), 0) → F(and(true, gt(0, s(s(0)))), plus(s(0), s(x0)), double(0))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                    ↳ NonInfProof

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

F(true, y0, s(x0)) → F(and(gt(y0, s(x0)), gt(x0, s(0))), plus(s(0), y0), double(s(x0)))
F(true, 0, x0) → F(and(false, gt(x0, s(s(0)))), plus(s(0), 0), double(x0))
F(true, s(x0), s(x1)) → F(and(gt(x0, x1), gt(s(x1), s(s(0)))), plus(s(0), s(x0)), double(s(x1)))
F(true, y0, 0) → F(and(gt(y0, 0), false), plus(s(0), y0), double(0))
F(true, s(x0), 0) → F(and(true, gt(0, s(s(0)))), plus(s(0), s(x0)), double(0))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, y0, s(x0)) → F(and(gt(y0, s(x0)), gt(x0, s(0))), plus(s(0), y0), double(s(x0))) at position [2] we obtained the following new rules:

F(true, y0, s(x0)) → F(and(gt(y0, s(x0)), gt(x0, s(0))), plus(s(0), y0), s(s(double(x0))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                    ↳ NonInfProof

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

F(true, 0, x0) → F(and(false, gt(x0, s(s(0)))), plus(s(0), 0), double(x0))
F(true, y0, s(x0)) → F(and(gt(y0, s(x0)), gt(x0, s(0))), plus(s(0), y0), s(s(double(x0))))
F(true, s(x0), s(x1)) → F(and(gt(x0, x1), gt(s(x1), s(s(0)))), plus(s(0), s(x0)), double(s(x1)))
F(true, y0, 0) → F(and(gt(y0, 0), false), plus(s(0), y0), double(0))
F(true, s(x0), 0) → F(and(true, gt(0, s(s(0)))), plus(s(0), s(x0)), double(0))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, s(x0), s(x1)) → F(and(gt(x0, x1), gt(s(x1), s(s(0)))), plus(s(0), s(x0)), double(s(x1))) at position [0,1] we obtained the following new rules:

F(true, s(x0), s(x1)) → F(and(gt(x0, x1), gt(x1, s(0))), plus(s(0), s(x0)), double(s(x1)))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                    ↳ NonInfProof

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

F(true, s(x0), s(x1)) → F(and(gt(x0, x1), gt(x1, s(0))), plus(s(0), s(x0)), double(s(x1)))
F(true, 0, x0) → F(and(false, gt(x0, s(s(0)))), plus(s(0), 0), double(x0))
F(true, y0, s(x0)) → F(and(gt(y0, s(x0)), gt(x0, s(0))), plus(s(0), y0), s(s(double(x0))))
F(true, y0, 0) → F(and(gt(y0, 0), false), plus(s(0), y0), double(0))
F(true, s(x0), 0) → F(and(true, gt(0, s(s(0)))), plus(s(0), s(x0)), double(0))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, 0, x0) → F(and(false, gt(x0, s(s(0)))), plus(s(0), 0), double(x0)) at position [1] we obtained the following new rules:

F(true, 0, x0) → F(and(false, gt(x0, s(s(0)))), s(0), double(x0))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                    ↳ NonInfProof

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

F(true, s(x0), s(x1)) → F(and(gt(x0, x1), gt(x1, s(0))), plus(s(0), s(x0)), double(s(x1)))
F(true, 0, x0) → F(and(false, gt(x0, s(s(0)))), s(0), double(x0))
F(true, y0, s(x0)) → F(and(gt(y0, s(x0)), gt(x0, s(0))), plus(s(0), y0), s(s(double(x0))))
F(true, y0, 0) → F(and(gt(y0, 0), false), plus(s(0), y0), double(0))
F(true, s(x0), 0) → F(and(true, gt(0, s(s(0)))), plus(s(0), s(x0)), double(0))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, y0, 0) → F(and(gt(y0, 0), false), plus(s(0), y0), double(0)) at position [0] we obtained the following new rules:

F(true, y0, 0) → F(false, plus(s(0), y0), double(0))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                    ↳ NonInfProof

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

F(true, s(x0), s(x1)) → F(and(gt(x0, x1), gt(x1, s(0))), plus(s(0), s(x0)), double(s(x1)))
F(true, y0, 0) → F(false, plus(s(0), y0), double(0))
F(true, y0, s(x0)) → F(and(gt(y0, s(x0)), gt(x0, s(0))), plus(s(0), y0), s(s(double(x0))))
F(true, 0, x0) → F(and(false, gt(x0, s(s(0)))), s(0), double(x0))
F(true, s(x0), 0) → F(and(true, gt(0, s(s(0)))), plus(s(0), s(x0)), double(0))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

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

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                    ↳ NonInfProof

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

F(true, s(x0), s(x1)) → F(and(gt(x0, x1), gt(x1, s(0))), plus(s(0), s(x0)), double(s(x1)))
F(true, 0, x0) → F(and(false, gt(x0, s(s(0)))), s(0), double(x0))
F(true, y0, s(x0)) → F(and(gt(y0, s(x0)), gt(x0, s(0))), plus(s(0), y0), s(s(double(x0))))
F(true, s(x0), 0) → F(and(true, gt(0, s(s(0)))), plus(s(0), s(x0)), double(0))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, s(x0), 0) → F(and(true, gt(0, s(s(0)))), plus(s(0), s(x0)), double(0)) at position [0,1] we obtained the following new rules:

F(true, s(x0), 0) → F(and(true, false), plus(s(0), s(x0)), double(0))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                    ↳ NonInfProof

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

F(true, s(x0), s(x1)) → F(and(gt(x0, x1), gt(x1, s(0))), plus(s(0), s(x0)), double(s(x1)))
F(true, s(x0), 0) → F(and(true, false), plus(s(0), s(x0)), double(0))
F(true, y0, s(x0)) → F(and(gt(y0, s(x0)), gt(x0, s(0))), plus(s(0), y0), s(s(double(x0))))
F(true, 0, x0) → F(and(false, gt(x0, s(s(0)))), s(0), double(x0))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, s(x0), s(x1)) → F(and(gt(x0, x1), gt(x1, s(0))), plus(s(0), s(x0)), double(s(x1))) at position [2] we obtained the following new rules:

F(true, s(x0), s(x1)) → F(and(gt(x0, x1), gt(x1, s(0))), plus(s(0), s(x0)), s(s(double(x1))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                    ↳ NonInfProof

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

F(true, s(x0), 0) → F(and(true, false), plus(s(0), s(x0)), double(0))
F(true, 0, x0) → F(and(false, gt(x0, s(s(0)))), s(0), double(x0))
F(true, y0, s(x0)) → F(and(gt(y0, s(x0)), gt(x0, s(0))), plus(s(0), y0), s(s(double(x0))))
F(true, s(x0), s(x1)) → F(and(gt(x0, x1), gt(x1, s(0))), plus(s(0), s(x0)), s(s(double(x1))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, s(x0), 0) → F(and(true, false), plus(s(0), s(x0)), double(0)) at position [0] we obtained the following new rules:

F(true, s(x0), 0) → F(false, plus(s(0), s(x0)), double(0))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                    ↳ NonInfProof

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

F(true, s(x0), 0) → F(false, plus(s(0), s(x0)), double(0))
F(true, y0, s(x0)) → F(and(gt(y0, s(x0)), gt(x0, s(0))), plus(s(0), y0), s(s(double(x0))))
F(true, 0, x0) → F(and(false, gt(x0, s(s(0)))), s(0), double(x0))
F(true, s(x0), s(x1)) → F(and(gt(x0, x1), gt(x1, s(0))), plus(s(0), s(x0)), s(s(double(x1))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

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

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                    ↳ NonInfProof

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

F(true, 0, x0) → F(and(false, gt(x0, s(s(0)))), s(0), double(x0))
F(true, y0, s(x0)) → F(and(gt(y0, s(x0)), gt(x0, s(0))), plus(s(0), y0), s(s(double(x0))))
F(true, s(x0), s(x1)) → F(and(gt(x0, x1), gt(x1, s(0))), plus(s(0), s(x0)), s(s(double(x1))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By narrowing [13] the rule F(true, 0, x0) → F(and(false, gt(x0, s(s(0)))), s(0), double(x0)) at position [2] we obtained the following new rules:

F(true, 0, 0) → F(and(false, gt(0, s(s(0)))), s(0), 0)
F(true, 0, s(x0)) → F(and(false, gt(s(x0), s(s(0)))), s(0), s(s(double(x0))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                    ↳ NonInfProof

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

F(true, y0, s(x0)) → F(and(gt(y0, s(x0)), gt(x0, s(0))), plus(s(0), y0), s(s(double(x0))))
F(true, 0, 0) → F(and(false, gt(0, s(s(0)))), s(0), 0)
F(true, s(x0), s(x1)) → F(and(gt(x0, x1), gt(x1, s(0))), plus(s(0), s(x0)), s(s(double(x1))))
F(true, 0, s(x0)) → F(and(false, gt(s(x0), s(s(0)))), s(0), s(s(double(x0))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

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

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                    ↳ NonInfProof

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

F(true, y0, s(x0)) → F(and(gt(y0, s(x0)), gt(x0, s(0))), plus(s(0), y0), s(s(double(x0))))
F(true, s(x0), s(x1)) → F(and(gt(x0, x1), gt(x1, s(0))), plus(s(0), s(x0)), s(s(double(x1))))
F(true, 0, s(x0)) → F(and(false, gt(s(x0), s(s(0)))), s(0), s(s(double(x0))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, 0, s(x0)) → F(and(false, gt(s(x0), s(s(0)))), s(0), s(s(double(x0)))) at position [0,1] we obtained the following new rules:

F(true, 0, s(x0)) → F(and(false, gt(x0, s(0))), s(0), s(s(double(x0))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                    ↳ NonInfProof

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

F(true, y0, s(x0)) → F(and(gt(y0, s(x0)), gt(x0, s(0))), plus(s(0), y0), s(s(double(x0))))
F(true, s(x0), s(x1)) → F(and(gt(x0, x1), gt(x1, s(0))), plus(s(0), s(x0)), s(s(double(x1))))
F(true, 0, s(x0)) → F(and(false, gt(x0, s(0))), s(0), s(s(double(x0))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By narrowing [13] the rule F(true, s(x0), s(x1)) → F(and(gt(x0, x1), gt(x1, s(0))), plus(s(0), s(x0)), s(s(double(x1)))) at position [1] we obtained the following new rules:

F(true, s(x1), s(y1)) → F(and(gt(x1, y1), gt(y1, s(0))), s(plus(s(0), x1)), s(s(double(y1))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                    ↳ NonInfProof

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

F(true, s(x1), s(y1)) → F(and(gt(x1, y1), gt(y1, s(0))), s(plus(s(0), x1)), s(s(double(y1))))
F(true, y0, s(x0)) → F(and(gt(y0, s(x0)), gt(x0, s(0))), plus(s(0), y0), s(s(double(x0))))
F(true, 0, s(x0)) → F(and(false, gt(x0, s(0))), s(0), s(s(double(x0))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By instantiating [13] the rule F(true, y0, s(x0)) → F(and(gt(y0, s(x0)), gt(x0, s(0))), plus(s(0), y0), s(s(double(x0)))) we obtained the following new rules:

F(true, s(0), s(s(y_2))) → F(and(gt(s(0), s(s(y_2))), gt(s(y_2), s(0))), plus(s(0), s(0)), s(s(double(s(y_2)))))
F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(s(y_4), s(0))), plus(s(0), y_3), s(s(double(s(y_4)))))
F(true, s(y_3), s(s(y_4))) → F(and(gt(s(y_3), s(s(y_4))), gt(s(y_4), s(0))), plus(s(0), s(y_3)), s(s(double(s(y_4)))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                    ↳ NonInfProof

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

F(true, s(x1), s(y1)) → F(and(gt(x1, y1), gt(y1, s(0))), s(plus(s(0), x1)), s(s(double(y1))))
F(true, s(0), s(s(y_2))) → F(and(gt(s(0), s(s(y_2))), gt(s(y_2), s(0))), plus(s(0), s(0)), s(s(double(s(y_2)))))
F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(s(y_4), s(0))), plus(s(0), y_3), s(s(double(s(y_4)))))
F(true, 0, s(x0)) → F(and(false, gt(x0, s(0))), s(0), s(s(double(x0))))
F(true, s(y_3), s(s(y_4))) → F(and(gt(s(y_3), s(s(y_4))), gt(s(y_4), s(0))), plus(s(0), s(y_3)), s(s(double(s(y_4)))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, s(0), s(s(y_2))) → F(and(gt(s(0), s(s(y_2))), gt(s(y_2), s(0))), plus(s(0), s(0)), s(s(double(s(y_2))))) at position [0,0] we obtained the following new rules:

F(true, s(0), s(s(y_2))) → F(and(gt(0, s(y_2)), gt(s(y_2), s(0))), plus(s(0), s(0)), s(s(double(s(y_2)))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                    ↳ NonInfProof

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

F(true, s(0), s(s(y_2))) → F(and(gt(0, s(y_2)), gt(s(y_2), s(0))), plus(s(0), s(0)), s(s(double(s(y_2)))))
F(true, s(x1), s(y1)) → F(and(gt(x1, y1), gt(y1, s(0))), s(plus(s(0), x1)), s(s(double(y1))))
F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(s(y_4), s(0))), plus(s(0), y_3), s(s(double(s(y_4)))))
F(true, 0, s(x0)) → F(and(false, gt(x0, s(0))), s(0), s(s(double(x0))))
F(true, s(y_3), s(s(y_4))) → F(and(gt(s(y_3), s(s(y_4))), gt(s(y_4), s(0))), plus(s(0), s(y_3)), s(s(double(s(y_4)))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(s(y_4), s(0))), plus(s(0), y_3), s(s(double(s(y_4))))) at position [0,1] we obtained the following new rules:

F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(double(s(y_4)))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                    ↳ NonInfProof

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

F(true, s(0), s(s(y_2))) → F(and(gt(0, s(y_2)), gt(s(y_2), s(0))), plus(s(0), s(0)), s(s(double(s(y_2)))))
F(true, s(x1), s(y1)) → F(and(gt(x1, y1), gt(y1, s(0))), s(plus(s(0), x1)), s(s(double(y1))))
F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(double(s(y_4)))))
F(true, 0, s(x0)) → F(and(false, gt(x0, s(0))), s(0), s(s(double(x0))))
F(true, s(y_3), s(s(y_4))) → F(and(gt(s(y_3), s(s(y_4))), gt(s(y_4), s(0))), plus(s(0), s(y_3)), s(s(double(s(y_4)))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, s(y_3), s(s(y_4))) → F(and(gt(s(y_3), s(s(y_4))), gt(s(y_4), s(0))), plus(s(0), s(y_3)), s(s(double(s(y_4))))) at position [0,0] we obtained the following new rules:

F(true, s(y_3), s(s(y_4))) → F(and(gt(y_3, s(y_4)), gt(s(y_4), s(0))), plus(s(0), s(y_3)), s(s(double(s(y_4)))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                    ↳ NonInfProof

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

F(true, s(0), s(s(y_2))) → F(and(gt(0, s(y_2)), gt(s(y_2), s(0))), plus(s(0), s(0)), s(s(double(s(y_2)))))
F(true, s(x1), s(y1)) → F(and(gt(x1, y1), gt(y1, s(0))), s(plus(s(0), x1)), s(s(double(y1))))
F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(double(s(y_4)))))
F(true, 0, s(x0)) → F(and(false, gt(x0, s(0))), s(0), s(s(double(x0))))
F(true, s(y_3), s(s(y_4))) → F(and(gt(y_3, s(y_4)), gt(s(y_4), s(0))), plus(s(0), s(y_3)), s(s(double(s(y_4)))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, s(0), s(s(y_2))) → F(and(gt(0, s(y_2)), gt(s(y_2), s(0))), plus(s(0), s(0)), s(s(double(s(y_2))))) at position [0,0] we obtained the following new rules:

F(true, s(0), s(s(y_2))) → F(and(false, gt(s(y_2), s(0))), plus(s(0), s(0)), s(s(double(s(y_2)))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                    ↳ NonInfProof

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

F(true, s(0), s(s(y_2))) → F(and(false, gt(s(y_2), s(0))), plus(s(0), s(0)), s(s(double(s(y_2)))))
F(true, s(x1), s(y1)) → F(and(gt(x1, y1), gt(y1, s(0))), s(plus(s(0), x1)), s(s(double(y1))))
F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(double(s(y_4)))))
F(true, 0, s(x0)) → F(and(false, gt(x0, s(0))), s(0), s(s(double(x0))))
F(true, s(y_3), s(s(y_4))) → F(and(gt(y_3, s(y_4)), gt(s(y_4), s(0))), plus(s(0), s(y_3)), s(s(double(s(y_4)))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(double(s(y_4))))) at position [2,0,0] we obtained the following new rules:

F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                    ↳ NonInfProof

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

F(true, s(0), s(s(y_2))) → F(and(false, gt(s(y_2), s(0))), plus(s(0), s(0)), s(s(double(s(y_2)))))
F(true, s(x1), s(y1)) → F(and(gt(x1, y1), gt(y1, s(0))), s(plus(s(0), x1)), s(s(double(y1))))
F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, 0, s(x0)) → F(and(false, gt(x0, s(0))), s(0), s(s(double(x0))))
F(true, s(y_3), s(s(y_4))) → F(and(gt(y_3, s(y_4)), gt(s(y_4), s(0))), plus(s(0), s(y_3)), s(s(double(s(y_4)))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, s(y_3), s(s(y_4))) → F(and(gt(y_3, s(y_4)), gt(s(y_4), s(0))), plus(s(0), s(y_3)), s(s(double(s(y_4))))) at position [0,1] we obtained the following new rules:

F(true, s(y_3), s(s(y_4))) → F(and(gt(y_3, s(y_4)), gt(y_4, 0)), plus(s(0), s(y_3)), s(s(double(s(y_4)))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                    ↳ NonInfProof

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

F(true, s(0), s(s(y_2))) → F(and(false, gt(s(y_2), s(0))), plus(s(0), s(0)), s(s(double(s(y_2)))))
F(true, s(x1), s(y1)) → F(and(gt(x1, y1), gt(y1, s(0))), s(plus(s(0), x1)), s(s(double(y1))))
F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, 0, s(x0)) → F(and(false, gt(x0, s(0))), s(0), s(s(double(x0))))
F(true, s(y_3), s(s(y_4))) → F(and(gt(y_3, s(y_4)), gt(y_4, 0)), plus(s(0), s(y_3)), s(s(double(s(y_4)))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, s(0), s(s(y_2))) → F(and(false, gt(s(y_2), s(0))), plus(s(0), s(0)), s(s(double(s(y_2))))) at position [0,1] we obtained the following new rules:

F(true, s(0), s(s(y_2))) → F(and(false, gt(y_2, 0)), plus(s(0), s(0)), s(s(double(s(y_2)))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                    ↳ NonInfProof

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

F(true, s(x1), s(y1)) → F(and(gt(x1, y1), gt(y1, s(0))), s(plus(s(0), x1)), s(s(double(y1))))
F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, s(0), s(s(y_2))) → F(and(false, gt(y_2, 0)), plus(s(0), s(0)), s(s(double(s(y_2)))))
F(true, 0, s(x0)) → F(and(false, gt(x0, s(0))), s(0), s(s(double(x0))))
F(true, s(y_3), s(s(y_4))) → F(and(gt(y_3, s(y_4)), gt(y_4, 0)), plus(s(0), s(y_3)), s(s(double(s(y_4)))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, s(y_3), s(s(y_4))) → F(and(gt(y_3, s(y_4)), gt(y_4, 0)), plus(s(0), s(y_3)), s(s(double(s(y_4))))) at position [2,0,0] we obtained the following new rules:

F(true, s(y_3), s(s(y_4))) → F(and(gt(y_3, s(y_4)), gt(y_4, 0)), plus(s(0), s(y_3)), s(s(s(s(double(y_4))))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                    ↳ NonInfProof

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

F(true, s(x1), s(y1)) → F(and(gt(x1, y1), gt(y1, s(0))), s(plus(s(0), x1)), s(s(double(y1))))
F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, 0, s(x0)) → F(and(false, gt(x0, s(0))), s(0), s(s(double(x0))))
F(true, s(0), s(s(y_2))) → F(and(false, gt(y_2, 0)), plus(s(0), s(0)), s(s(double(s(y_2)))))
F(true, s(y_3), s(s(y_4))) → F(and(gt(y_3, s(y_4)), gt(y_4, 0)), plus(s(0), s(y_3)), s(s(s(s(double(y_4))))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, s(0), s(s(y_2))) → F(and(false, gt(y_2, 0)), plus(s(0), s(0)), s(s(double(s(y_2))))) at position [2,0,0] we obtained the following new rules:

F(true, s(0), s(s(y_2))) → F(and(false, gt(y_2, 0)), plus(s(0), s(0)), s(s(s(s(double(y_2))))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Narrowing

                    ↳ NonInfProof

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

F(true, s(x1), s(y1)) → F(and(gt(x1, y1), gt(y1, s(0))), s(plus(s(0), x1)), s(s(double(y1))))
F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, s(0), s(s(y_2))) → F(and(false, gt(y_2, 0)), plus(s(0), s(0)), s(s(s(s(double(y_2))))))
F(true, 0, s(x0)) → F(and(false, gt(x0, s(0))), s(0), s(s(double(x0))))
F(true, s(y_3), s(s(y_4))) → F(and(gt(y_3, s(y_4)), gt(y_4, 0)), plus(s(0), s(y_3)), s(s(s(s(double(y_4))))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By narrowing [13] the rule F(true, s(y_3), s(s(y_4))) → F(and(gt(y_3, s(y_4)), gt(y_4, 0)), plus(s(0), s(y_3)), s(s(s(s(double(y_4)))))) at position [1] we obtained the following new rules:

F(true, s(x1), s(s(y1))) → F(and(gt(x1, s(y1)), gt(y1, 0)), s(plus(s(0), x1)), s(s(s(s(double(y1))))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Narrowing

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                    ↳ NonInfProof

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

F(true, s(x1), s(y1)) → F(and(gt(x1, y1), gt(y1, s(0))), s(plus(s(0), x1)), s(s(double(y1))))
F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, s(0), s(s(y_2))) → F(and(false, gt(y_2, 0)), plus(s(0), s(0)), s(s(s(s(double(y_2))))))
F(true, 0, s(x0)) → F(and(false, gt(x0, s(0))), s(0), s(s(double(x0))))
F(true, s(x1), s(s(y1))) → F(and(gt(x1, s(y1)), gt(y1, 0)), s(plus(s(0), x1)), s(s(s(s(double(y1))))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By narrowing [13] the rule F(true, s(0), s(s(y_2))) → F(and(false, gt(y_2, 0)), plus(s(0), s(0)), s(s(s(s(double(y_2)))))) at position [1] we obtained the following new rules:

F(true, s(0), s(s(y0))) → F(and(false, gt(y0, 0)), s(plus(s(0), 0)), s(s(s(s(double(y0))))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Narrowing

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                    ↳ NonInfProof

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

F(true, s(x1), s(y1)) → F(and(gt(x1, y1), gt(y1, s(0))), s(plus(s(0), x1)), s(s(double(y1))))
F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, s(0), s(s(y0))) → F(and(false, gt(y0, 0)), s(plus(s(0), 0)), s(s(s(s(double(y0))))))
F(true, 0, s(x0)) → F(and(false, gt(x0, s(0))), s(0), s(s(double(x0))))
F(true, s(x1), s(s(y1))) → F(and(gt(x1, s(y1)), gt(y1, 0)), s(plus(s(0), x1)), s(s(s(s(double(y1))))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, s(0), s(s(y0))) → F(and(false, gt(y0, 0)), s(plus(s(0), 0)), s(s(s(s(double(y0)))))) at position [1,0] we obtained the following new rules:

F(true, s(0), s(s(y0))) → F(and(false, gt(y0, 0)), s(s(0)), s(s(s(s(double(y0))))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Narrowing

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                    ↳ NonInfProof

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

F(true, s(x1), s(y1)) → F(and(gt(x1, y1), gt(y1, s(0))), s(plus(s(0), x1)), s(s(double(y1))))
F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, s(0), s(s(y0))) → F(and(false, gt(y0, 0)), s(s(0)), s(s(s(s(double(y0))))))
F(true, 0, s(x0)) → F(and(false, gt(x0, s(0))), s(0), s(s(double(x0))))
F(true, s(x1), s(s(y1))) → F(and(gt(x1, s(y1)), gt(y1, 0)), s(plus(s(0), x1)), s(s(s(s(double(y1))))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By instantiating [13] the rule F(true, 0, s(x0)) → F(and(false, gt(x0, s(0))), s(0), s(s(double(x0)))) we obtained the following new rules:

F(true, 0, s(s(s(s(y_4))))) → F(and(false, gt(s(s(s(y_4))), s(0))), s(0), s(s(double(s(s(s(y_4)))))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Narrowing

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ Rewriting

                    ↳ NonInfProof

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

F(true, s(x1), s(y1)) → F(and(gt(x1, y1), gt(y1, s(0))), s(plus(s(0), x1)), s(s(double(y1))))
F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, s(0), s(s(y0))) → F(and(false, gt(y0, 0)), s(s(0)), s(s(s(s(double(y0))))))
F(true, 0, s(s(s(s(y_4))))) → F(and(false, gt(s(s(s(y_4))), s(0))), s(0), s(s(double(s(s(s(y_4)))))))
F(true, s(x1), s(s(y1))) → F(and(gt(x1, s(y1)), gt(y1, 0)), s(plus(s(0), x1)), s(s(s(s(double(y1))))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, 0, s(s(s(s(y_4))))) → F(and(false, gt(s(s(s(y_4))), s(0))), s(0), s(s(double(s(s(s(y_4))))))) at position [0,1] we obtained the following new rules:

F(true, 0, s(s(s(s(y_4))))) → F(and(false, gt(s(s(y_4)), 0)), s(0), s(s(double(s(s(s(y_4)))))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Narrowing

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ Rewriting

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ Rewriting

                    ↳ NonInfProof

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

F(true, s(x1), s(y1)) → F(and(gt(x1, y1), gt(y1, s(0))), s(plus(s(0), x1)), s(s(double(y1))))
F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, s(0), s(s(y0))) → F(and(false, gt(y0, 0)), s(s(0)), s(s(s(s(double(y0))))))
F(true, 0, s(s(s(s(y_4))))) → F(and(false, gt(s(s(y_4)), 0)), s(0), s(s(double(s(s(s(y_4)))))))
F(true, s(x1), s(s(y1))) → F(and(gt(x1, s(y1)), gt(y1, 0)), s(plus(s(0), x1)), s(s(s(s(double(y1))))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, 0, s(s(s(s(y_4))))) → F(and(false, gt(s(s(y_4)), 0)), s(0), s(s(double(s(s(s(y_4))))))) at position [0,1] we obtained the following new rules:

F(true, 0, s(s(s(s(y_4))))) → F(and(false, true), s(0), s(s(double(s(s(s(y_4)))))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Narrowing

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ Rewriting

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ Rewriting

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ Rewriting

                    ↳ NonInfProof

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

F(true, 0, s(s(s(s(y_4))))) → F(and(false, true), s(0), s(s(double(s(s(s(y_4)))))))
F(true, s(x1), s(y1)) → F(and(gt(x1, y1), gt(y1, s(0))), s(plus(s(0), x1)), s(s(double(y1))))
F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, s(0), s(s(y0))) → F(and(false, gt(y0, 0)), s(s(0)), s(s(s(s(double(y0))))))
F(true, s(x1), s(s(y1))) → F(and(gt(x1, s(y1)), gt(y1, 0)), s(plus(s(0), x1)), s(s(s(s(double(y1))))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, 0, s(s(s(s(y_4))))) → F(and(false, true), s(0), s(s(double(s(s(s(y_4))))))) at position [0] we obtained the following new rules:

F(true, 0, s(s(s(s(y_4))))) → F(false, s(0), s(s(double(s(s(s(y_4)))))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Narrowing

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ Rewriting

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ Rewriting

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ Rewriting

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ DependencyGraphProof

                    ↳ NonInfProof

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

F(true, s(x1), s(y1)) → F(and(gt(x1, y1), gt(y1, s(0))), s(plus(s(0), x1)), s(s(double(y1))))
F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, s(0), s(s(y0))) → F(and(false, gt(y0, 0)), s(s(0)), s(s(s(s(double(y0))))))
F(true, 0, s(s(s(s(y_4))))) → F(false, s(0), s(s(double(s(s(s(y_4)))))))
F(true, s(x1), s(s(y1))) → F(and(gt(x1, s(y1)), gt(y1, 0)), s(plus(s(0), x1)), s(s(s(s(double(y1))))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

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

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Narrowing

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ Rewriting

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ Rewriting

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ Rewriting

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ DependencyGraphProof

                                                                                                                                                  ↳ QDP

                                                                                                                                                    ↳ Instantiation

                    ↳ NonInfProof

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

F(true, s(x1), s(y1)) → F(and(gt(x1, y1), gt(y1, s(0))), s(plus(s(0), x1)), s(s(double(y1))))
F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, s(0), s(s(y0))) → F(and(false, gt(y0, 0)), s(s(0)), s(s(s(s(double(y0))))))
F(true, s(x1), s(s(y1))) → F(and(gt(x1, s(y1)), gt(y1, 0)), s(plus(s(0), x1)), s(s(s(s(double(y1))))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By instantiating [13] the rule F(true, s(x1), s(y1)) → F(and(gt(x1, y1), gt(y1, s(0))), s(plus(s(0), x1)), s(s(double(y1)))) we obtained the following new rules:

F(true, s(s(0)), s(s(s(s(y_2))))) → F(and(gt(s(0), s(s(s(y_2)))), gt(s(s(s(y_2))), s(0))), s(plus(s(0), s(0))), s(s(double(s(s(s(y_2)))))))
F(true, s(x0), s(s(s(s(y_4))))) → F(and(gt(x0, s(s(s(y_4)))), gt(s(s(s(y_4))), s(0))), s(plus(s(0), x0)), s(s(double(s(s(s(y_4)))))))
F(true, s(y_3), s(s(y_4))) → F(and(gt(y_3, s(y_4)), gt(s(y_4), s(0))), s(plus(s(0), y_3)), s(s(double(s(y_4)))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Narrowing

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ Rewriting

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ Rewriting

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ Rewriting

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ DependencyGraphProof

                                                                                                                                                  ↳ QDP

                                                                                                                                                    ↳ Instantiation

                                                                                                                                                      ↳ QDP

                                                                                                                                                        ↳ Rewriting

                    ↳ NonInfProof

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

F(true, s(s(0)), s(s(s(s(y_2))))) → F(and(gt(s(0), s(s(s(y_2)))), gt(s(s(s(y_2))), s(0))), s(plus(s(0), s(0))), s(s(double(s(s(s(y_2)))))))
F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, s(0), s(s(y0))) → F(and(false, gt(y0, 0)), s(s(0)), s(s(s(s(double(y0))))))
F(true, s(x0), s(s(s(s(y_4))))) → F(and(gt(x0, s(s(s(y_4)))), gt(s(s(s(y_4))), s(0))), s(plus(s(0), x0)), s(s(double(s(s(s(y_4)))))))
F(true, s(y_3), s(s(y_4))) → F(and(gt(y_3, s(y_4)), gt(s(y_4), s(0))), s(plus(s(0), y_3)), s(s(double(s(y_4)))))
F(true, s(x1), s(s(y1))) → F(and(gt(x1, s(y1)), gt(y1, 0)), s(plus(s(0), x1)), s(s(s(s(double(y1))))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, s(s(0)), s(s(s(s(y_2))))) → F(and(gt(s(0), s(s(s(y_2)))), gt(s(s(s(y_2))), s(0))), s(plus(s(0), s(0))), s(s(double(s(s(s(y_2))))))) at position [0,0] we obtained the following new rules:

F(true, s(s(0)), s(s(s(s(y_2))))) → F(and(gt(0, s(s(y_2))), gt(s(s(s(y_2))), s(0))), s(plus(s(0), s(0))), s(s(double(s(s(s(y_2)))))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Narrowing

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ Rewriting

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ Rewriting

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ Rewriting

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ DependencyGraphProof

                                                                                                                                                  ↳ QDP

                                                                                                                                                    ↳ Instantiation

                                                                                                                                                      ↳ QDP

                                                                                                                                                        ↳ Rewriting

                                                                                                                                                          ↳ QDP

                                                                                                                                                            ↳ Rewriting

                    ↳ NonInfProof

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

F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, s(0), s(s(y0))) → F(and(false, gt(y0, 0)), s(s(0)), s(s(s(s(double(y0))))))
F(true, s(x0), s(s(s(s(y_4))))) → F(and(gt(x0, s(s(s(y_4)))), gt(s(s(s(y_4))), s(0))), s(plus(s(0), x0)), s(s(double(s(s(s(y_4)))))))
F(true, s(y_3), s(s(y_4))) → F(and(gt(y_3, s(y_4)), gt(s(y_4), s(0))), s(plus(s(0), y_3)), s(s(double(s(y_4)))))
F(true, s(s(0)), s(s(s(s(y_2))))) → F(and(gt(0, s(s(y_2))), gt(s(s(s(y_2))), s(0))), s(plus(s(0), s(0))), s(s(double(s(s(s(y_2)))))))
F(true, s(x1), s(s(y1))) → F(and(gt(x1, s(y1)), gt(y1, 0)), s(plus(s(0), x1)), s(s(s(s(double(y1))))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, s(x0), s(s(s(s(y_4))))) → F(and(gt(x0, s(s(s(y_4)))), gt(s(s(s(y_4))), s(0))), s(plus(s(0), x0)), s(s(double(s(s(s(y_4))))))) at position [0,1] we obtained the following new rules:

F(true, s(x0), s(s(s(s(y_4))))) → F(and(gt(x0, s(s(s(y_4)))), gt(s(s(y_4)), 0)), s(plus(s(0), x0)), s(s(double(s(s(s(y_4)))))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Narrowing

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ Rewriting

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ Rewriting

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ Rewriting

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ DependencyGraphProof

                                                                                                                                                  ↳ QDP

                                                                                                                                                    ↳ Instantiation

                                                                                                                                                      ↳ QDP

                                                                                                                                                        ↳ Rewriting

                                                                                                                                                          ↳ QDP

                                                                                                                                                            ↳ Rewriting

                                                                                                                                                              ↳ QDP

                                                                                                                                                                ↳ Rewriting

                    ↳ NonInfProof

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

F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, s(0), s(s(y0))) → F(and(false, gt(y0, 0)), s(s(0)), s(s(s(s(double(y0))))))
F(true, s(y_3), s(s(y_4))) → F(and(gt(y_3, s(y_4)), gt(s(y_4), s(0))), s(plus(s(0), y_3)), s(s(double(s(y_4)))))
F(true, s(s(0)), s(s(s(s(y_2))))) → F(and(gt(0, s(s(y_2))), gt(s(s(s(y_2))), s(0))), s(plus(s(0), s(0))), s(s(double(s(s(s(y_2)))))))
F(true, s(x0), s(s(s(s(y_4))))) → F(and(gt(x0, s(s(s(y_4)))), gt(s(s(y_4)), 0)), s(plus(s(0), x0)), s(s(double(s(s(s(y_4)))))))
F(true, s(x1), s(s(y1))) → F(and(gt(x1, s(y1)), gt(y1, 0)), s(plus(s(0), x1)), s(s(s(s(double(y1))))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, s(y_3), s(s(y_4))) → F(and(gt(y_3, s(y_4)), gt(s(y_4), s(0))), s(plus(s(0), y_3)), s(s(double(s(y_4))))) at position [0,1] we obtained the following new rules:

F(true, s(y_3), s(s(y_4))) → F(and(gt(y_3, s(y_4)), gt(y_4, 0)), s(plus(s(0), y_3)), s(s(double(s(y_4)))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Narrowing

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ Rewriting

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ Rewriting

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ Rewriting

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ DependencyGraphProof

                                                                                                                                                  ↳ QDP

                                                                                                                                                    ↳ Instantiation

                                                                                                                                                      ↳ QDP

                                                                                                                                                        ↳ Rewriting

                                                                                                                                                          ↳ QDP

                                                                                                                                                            ↳ Rewriting

                                                                                                                                                              ↳ QDP

                                                                                                                                                                ↳ Rewriting

                                                                                                                                                                  ↳ QDP

                                                                                                                                                                    ↳ Rewriting

                    ↳ NonInfProof

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

F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, s(0), s(s(y0))) → F(and(false, gt(y0, 0)), s(s(0)), s(s(s(s(double(y0))))))
F(true, s(y_3), s(s(y_4))) → F(and(gt(y_3, s(y_4)), gt(y_4, 0)), s(plus(s(0), y_3)), s(s(double(s(y_4)))))
F(true, s(s(0)), s(s(s(s(y_2))))) → F(and(gt(0, s(s(y_2))), gt(s(s(s(y_2))), s(0))), s(plus(s(0), s(0))), s(s(double(s(s(s(y_2)))))))
F(true, s(x1), s(s(y1))) → F(and(gt(x1, s(y1)), gt(y1, 0)), s(plus(s(0), x1)), s(s(s(s(double(y1))))))
F(true, s(x0), s(s(s(s(y_4))))) → F(and(gt(x0, s(s(s(y_4)))), gt(s(s(y_4)), 0)), s(plus(s(0), x0)), s(s(double(s(s(s(y_4)))))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, s(s(0)), s(s(s(s(y_2))))) → F(and(gt(0, s(s(y_2))), gt(s(s(s(y_2))), s(0))), s(plus(s(0), s(0))), s(s(double(s(s(s(y_2))))))) at position [0,0] we obtained the following new rules:

F(true, s(s(0)), s(s(s(s(y_2))))) → F(and(false, gt(s(s(s(y_2))), s(0))), s(plus(s(0), s(0))), s(s(double(s(s(s(y_2)))))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Narrowing

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ Rewriting

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ Rewriting

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ Rewriting

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ DependencyGraphProof

                                                                                                                                                  ↳ QDP

                                                                                                                                                    ↳ Instantiation

                                                                                                                                                      ↳ QDP

                                                                                                                                                        ↳ Rewriting

                                                                                                                                                          ↳ QDP

                                                                                                                                                            ↳ Rewriting

                                                                                                                                                              ↳ QDP

                                                                                                                                                                ↳ Rewriting

                                                                                                                                                                  ↳ QDP

                                                                                                                                                                    ↳ Rewriting

                                                                                                                                                                      ↳ QDP

                                                                                                                                                                        ↳ Rewriting

                    ↳ NonInfProof

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

F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, s(0), s(s(y0))) → F(and(false, gt(y0, 0)), s(s(0)), s(s(s(s(double(y0))))))
F(true, s(y_3), s(s(y_4))) → F(and(gt(y_3, s(y_4)), gt(y_4, 0)), s(plus(s(0), y_3)), s(s(double(s(y_4)))))
F(true, s(s(0)), s(s(s(s(y_2))))) → F(and(false, gt(s(s(s(y_2))), s(0))), s(plus(s(0), s(0))), s(s(double(s(s(s(y_2)))))))
F(true, s(x0), s(s(s(s(y_4))))) → F(and(gt(x0, s(s(s(y_4)))), gt(s(s(y_4)), 0)), s(plus(s(0), x0)), s(s(double(s(s(s(y_4)))))))
F(true, s(x1), s(s(y1))) → F(and(gt(x1, s(y1)), gt(y1, 0)), s(plus(s(0), x1)), s(s(s(s(double(y1))))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, s(x0), s(s(s(s(y_4))))) → F(and(gt(x0, s(s(s(y_4)))), gt(s(s(y_4)), 0)), s(plus(s(0), x0)), s(s(double(s(s(s(y_4))))))) at position [0,1] we obtained the following new rules:

F(true, s(x0), s(s(s(s(y_4))))) → F(and(gt(x0, s(s(s(y_4)))), true), s(plus(s(0), x0)), s(s(double(s(s(s(y_4)))))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Narrowing

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ Rewriting

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ Rewriting

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ Rewriting

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ DependencyGraphProof

                                                                                                                                                  ↳ QDP

                                                                                                                                                    ↳ Instantiation

                                                                                                                                                      ↳ QDP

                                                                                                                                                        ↳ Rewriting

                                                                                                                                                          ↳ QDP

                                                                                                                                                            ↳ Rewriting

                                                                                                                                                              ↳ QDP

                                                                                                                                                                ↳ Rewriting

                                                                                                                                                                  ↳ QDP

                                                                                                                                                                    ↳ Rewriting

                                                                                                                                                                      ↳ QDP

                                                                                                                                                                        ↳ Rewriting

                                                                                                                                                                          ↳ QDP

                                                                                                                                                                            ↳ Rewriting

                    ↳ NonInfProof

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

F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, s(0), s(s(y0))) → F(and(false, gt(y0, 0)), s(s(0)), s(s(s(s(double(y0))))))
F(true, s(x0), s(s(s(s(y_4))))) → F(and(gt(x0, s(s(s(y_4)))), true), s(plus(s(0), x0)), s(s(double(s(s(s(y_4)))))))
F(true, s(y_3), s(s(y_4))) → F(and(gt(y_3, s(y_4)), gt(y_4, 0)), s(plus(s(0), y_3)), s(s(double(s(y_4)))))
F(true, s(s(0)), s(s(s(s(y_2))))) → F(and(false, gt(s(s(s(y_2))), s(0))), s(plus(s(0), s(0))), s(s(double(s(s(s(y_2)))))))
F(true, s(x1), s(s(y1))) → F(and(gt(x1, s(y1)), gt(y1, 0)), s(plus(s(0), x1)), s(s(s(s(double(y1))))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, s(y_3), s(s(y_4))) → F(and(gt(y_3, s(y_4)), gt(y_4, 0)), s(plus(s(0), y_3)), s(s(double(s(y_4))))) at position [2,0,0] we obtained the following new rules:

F(true, s(y_3), s(s(y_4))) → F(and(gt(y_3, s(y_4)), gt(y_4, 0)), s(plus(s(0), y_3)), s(s(s(s(double(y_4))))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Narrowing

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ Rewriting

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ Rewriting

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ Rewriting

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ DependencyGraphProof

                                                                                                                                                  ↳ QDP

                                                                                                                                                    ↳ Instantiation

                                                                                                                                                      ↳ QDP

                                                                                                                                                        ↳ Rewriting

                                                                                                                                                          ↳ QDP

                                                                                                                                                            ↳ Rewriting

                                                                                                                                                              ↳ QDP

                                                                                                                                                                ↳ Rewriting

                                                                                                                                                                  ↳ QDP

                                                                                                                                                                    ↳ Rewriting

                                                                                                                                                                      ↳ QDP

                                                                                                                                                                        ↳ Rewriting

                                                                                                                                                                          ↳ QDP

                                                                                                                                                                            ↳ Rewriting

                                                                                                                                                                              ↳ QDP

                                                                                                                                                                                ↳ Rewriting

                    ↳ NonInfProof

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

F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, s(0), s(s(y0))) → F(and(false, gt(y0, 0)), s(s(0)), s(s(s(s(double(y0))))))
F(true, s(x0), s(s(s(s(y_4))))) → F(and(gt(x0, s(s(s(y_4)))), true), s(plus(s(0), x0)), s(s(double(s(s(s(y_4)))))))
F(true, s(s(0)), s(s(s(s(y_2))))) → F(and(false, gt(s(s(s(y_2))), s(0))), s(plus(s(0), s(0))), s(s(double(s(s(s(y_2)))))))
F(true, s(x1), s(s(y1))) → F(and(gt(x1, s(y1)), gt(y1, 0)), s(plus(s(0), x1)), s(s(s(s(double(y1))))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, s(s(0)), s(s(s(s(y_2))))) → F(and(false, gt(s(s(s(y_2))), s(0))), s(plus(s(0), s(0))), s(s(double(s(s(s(y_2))))))) at position [0,1] we obtained the following new rules:

F(true, s(s(0)), s(s(s(s(y_2))))) → F(and(false, gt(s(s(y_2)), 0)), s(plus(s(0), s(0))), s(s(double(s(s(s(y_2)))))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Narrowing

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ Rewriting

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ Rewriting

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ Rewriting

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ DependencyGraphProof

                                                                                                                                                  ↳ QDP

                                                                                                                                                    ↳ Instantiation

                                                                                                                                                      ↳ QDP

                                                                                                                                                        ↳ Rewriting

                                                                                                                                                          ↳ QDP

                                                                                                                                                            ↳ Rewriting

                                                                                                                                                              ↳ QDP

                                                                                                                                                                ↳ Rewriting

                                                                                                                                                                  ↳ QDP

                                                                                                                                                                    ↳ Rewriting

                                                                                                                                                                      ↳ QDP

                                                                                                                                                                        ↳ Rewriting

                                                                                                                                                                          ↳ QDP

                                                                                                                                                                            ↳ Rewriting

                                                                                                                                                                              ↳ QDP

                                                                                                                                                                                ↳ Rewriting

                                                                                                                                                                                  ↳ QDP

                                                                                                                                                                                    ↳ Rewriting

                    ↳ NonInfProof

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

F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, s(0), s(s(y0))) → F(and(false, gt(y0, 0)), s(s(0)), s(s(s(s(double(y0))))))
F(true, s(x0), s(s(s(s(y_4))))) → F(and(gt(x0, s(s(s(y_4)))), true), s(plus(s(0), x0)), s(s(double(s(s(s(y_4)))))))
F(true, s(s(0)), s(s(s(s(y_2))))) → F(and(false, gt(s(s(y_2)), 0)), s(plus(s(0), s(0))), s(s(double(s(s(s(y_2)))))))
F(true, s(x1), s(s(y1))) → F(and(gt(x1, s(y1)), gt(y1, 0)), s(plus(s(0), x1)), s(s(s(s(double(y1))))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, s(x0), s(s(s(s(y_4))))) → F(and(gt(x0, s(s(s(y_4)))), true), s(plus(s(0), x0)), s(s(double(s(s(s(y_4))))))) at position [0] we obtained the following new rules:

F(true, s(x0), s(s(s(s(y_4))))) → F(gt(x0, s(s(s(y_4)))), s(plus(s(0), x0)), s(s(double(s(s(s(y_4)))))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Narrowing

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ Rewriting

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ Rewriting

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ Rewriting

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ DependencyGraphProof

                                                                                                                                                  ↳ QDP

                                                                                                                                                    ↳ Instantiation

                                                                                                                                                      ↳ QDP

                                                                                                                                                        ↳ Rewriting

                                                                                                                                                          ↳ QDP

                                                                                                                                                            ↳ Rewriting

                                                                                                                                                              ↳ QDP

                                                                                                                                                                ↳ Rewriting

                                                                                                                                                                  ↳ QDP

                                                                                                                                                                    ↳ Rewriting

                                                                                                                                                                      ↳ QDP

                                                                                                                                                                        ↳ Rewriting

                                                                                                                                                                          ↳ QDP

                                                                                                                                                                            ↳ Rewriting

                                                                                                                                                                              ↳ QDP

                                                                                                                                                                                ↳ Rewriting

                                                                                                                                                                                  ↳ QDP

                                                                                                                                                                                    ↳ Rewriting

                                                                                                                                                                                      ↳ QDP

                                                                                                                                                                                        ↳ Rewriting

                    ↳ NonInfProof

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

F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, s(0), s(s(y0))) → F(and(false, gt(y0, 0)), s(s(0)), s(s(s(s(double(y0))))))
F(true, s(x0), s(s(s(s(y_4))))) → F(gt(x0, s(s(s(y_4)))), s(plus(s(0), x0)), s(s(double(s(s(s(y_4)))))))
F(true, s(s(0)), s(s(s(s(y_2))))) → F(and(false, gt(s(s(y_2)), 0)), s(plus(s(0), s(0))), s(s(double(s(s(s(y_2)))))))
F(true, s(x1), s(s(y1))) → F(and(gt(x1, s(y1)), gt(y1, 0)), s(plus(s(0), x1)), s(s(s(s(double(y1))))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, s(s(0)), s(s(s(s(y_2))))) → F(and(false, gt(s(s(y_2)), 0)), s(plus(s(0), s(0))), s(s(double(s(s(s(y_2))))))) at position [0,1] we obtained the following new rules:

F(true, s(s(0)), s(s(s(s(y_2))))) → F(and(false, true), s(plus(s(0), s(0))), s(s(double(s(s(s(y_2)))))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Narrowing

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ Rewriting

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ Rewriting

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ Rewriting

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ DependencyGraphProof

                                                                                                                                                  ↳ QDP

                                                                                                                                                    ↳ Instantiation

                                                                                                                                                      ↳ QDP

                                                                                                                                                        ↳ Rewriting

                                                                                                                                                          ↳ QDP

                                                                                                                                                            ↳ Rewriting

                                                                                                                                                              ↳ QDP

                                                                                                                                                                ↳ Rewriting

                                                                                                                                                                  ↳ QDP

                                                                                                                                                                    ↳ Rewriting

                                                                                                                                                                      ↳ QDP

                                                                                                                                                                        ↳ Rewriting

                                                                                                                                                                          ↳ QDP

                                                                                                                                                                            ↳ Rewriting

                                                                                                                                                                              ↳ QDP

                                                                                                                                                                                ↳ Rewriting

                                                                                                                                                                                  ↳ QDP

                                                                                                                                                                                    ↳ Rewriting

                                                                                                                                                                                      ↳ QDP

                                                                                                                                                                                        ↳ Rewriting

                                                                                                                                                                                          ↳ QDP

                                                                                                                                                                                            ↳ Rewriting

                    ↳ NonInfProof

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

F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, s(0), s(s(y0))) → F(and(false, gt(y0, 0)), s(s(0)), s(s(s(s(double(y0))))))
F(true, s(x0), s(s(s(s(y_4))))) → F(gt(x0, s(s(s(y_4)))), s(plus(s(0), x0)), s(s(double(s(s(s(y_4)))))))
F(true, s(s(0)), s(s(s(s(y_2))))) → F(and(false, true), s(plus(s(0), s(0))), s(s(double(s(s(s(y_2)))))))
F(true, s(x1), s(s(y1))) → F(and(gt(x1, s(y1)), gt(y1, 0)), s(plus(s(0), x1)), s(s(s(s(double(y1))))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, s(x0), s(s(s(s(y_4))))) → F(gt(x0, s(s(s(y_4)))), s(plus(s(0), x0)), s(s(double(s(s(s(y_4))))))) at position [2,0,0] we obtained the following new rules:

F(true, s(x0), s(s(s(s(y_4))))) → F(gt(x0, s(s(s(y_4)))), s(plus(s(0), x0)), s(s(s(s(double(s(s(y_4))))))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Narrowing

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ Rewriting

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ Rewriting

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ Rewriting

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ DependencyGraphProof

                                                                                                                                                  ↳ QDP

                                                                                                                                                    ↳ Instantiation

                                                                                                                                                      ↳ QDP

                                                                                                                                                        ↳ Rewriting

                                                                                                                                                          ↳ QDP

                                                                                                                                                            ↳ Rewriting

                                                                                                                                                              ↳ QDP

                                                                                                                                                                ↳ Rewriting

                                                                                                                                                                  ↳ QDP

                                                                                                                                                                    ↳ Rewriting

                                                                                                                                                                      ↳ QDP

                                                                                                                                                                        ↳ Rewriting

                                                                                                                                                                          ↳ QDP

                                                                                                                                                                            ↳ Rewriting

                                                                                                                                                                              ↳ QDP

                                                                                                                                                                                ↳ Rewriting

                                                                                                                                                                                  ↳ QDP

                                                                                                                                                                                    ↳ Rewriting

                                                                                                                                                                                      ↳ QDP

                                                                                                                                                                                        ↳ Rewriting

                                                                                                                                                                                          ↳ QDP

                                                                                                                                                                                            ↳ Rewriting

                                                                                                                                                                                              ↳ QDP

                                                                                                                                                                                                ↳ Rewriting

                    ↳ NonInfProof

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

F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, s(x0), s(s(s(s(y_4))))) → F(gt(x0, s(s(s(y_4)))), s(plus(s(0), x0)), s(s(s(s(double(s(s(y_4))))))))
F(true, s(0), s(s(y0))) → F(and(false, gt(y0, 0)), s(s(0)), s(s(s(s(double(y0))))))
F(true, s(s(0)), s(s(s(s(y_2))))) → F(and(false, true), s(plus(s(0), s(0))), s(s(double(s(s(s(y_2)))))))
F(true, s(x1), s(s(y1))) → F(and(gt(x1, s(y1)), gt(y1, 0)), s(plus(s(0), x1)), s(s(s(s(double(y1))))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, s(s(0)), s(s(s(s(y_2))))) → F(and(false, true), s(plus(s(0), s(0))), s(s(double(s(s(s(y_2))))))) at position [0] we obtained the following new rules:

F(true, s(s(0)), s(s(s(s(y_2))))) → F(false, s(plus(s(0), s(0))), s(s(double(s(s(s(y_2)))))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Narrowing

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ Rewriting

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ Rewriting

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ Rewriting

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ DependencyGraphProof

                                                                                                                                                  ↳ QDP

                                                                                                                                                    ↳ Instantiation

                                                                                                                                                      ↳ QDP

                                                                                                                                                        ↳ Rewriting

                                                                                                                                                          ↳ QDP

                                                                                                                                                            ↳ Rewriting

                                                                                                                                                              ↳ QDP

                                                                                                                                                                ↳ Rewriting

                                                                                                                                                                  ↳ QDP

                                                                                                                                                                    ↳ Rewriting

                                                                                                                                                                      ↳ QDP

                                                                                                                                                                        ↳ Rewriting

                                                                                                                                                                          ↳ QDP

                                                                                                                                                                            ↳ Rewriting

                                                                                                                                                                              ↳ QDP

                                                                                                                                                                                ↳ Rewriting

                                                                                                                                                                                  ↳ QDP

                                                                                                                                                                                    ↳ Rewriting

                                                                                                                                                                                      ↳ QDP

                                                                                                                                                                                        ↳ Rewriting

                                                                                                                                                                                          ↳ QDP

                                                                                                                                                                                            ↳ Rewriting

                                                                                                                                                                                              ↳ QDP

                                                                                                                                                                                                ↳ Rewriting

                                                                                                                                                                                                  ↳ QDP

                                                                                                                                                                                                    ↳ DependencyGraphProof

                    ↳ NonInfProof

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

F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, s(s(0)), s(s(s(s(y_2))))) → F(false, s(plus(s(0), s(0))), s(s(double(s(s(s(y_2)))))))
F(true, s(0), s(s(y0))) → F(and(false, gt(y0, 0)), s(s(0)), s(s(s(s(double(y0))))))
F(true, s(x0), s(s(s(s(y_4))))) → F(gt(x0, s(s(s(y_4)))), s(plus(s(0), x0)), s(s(s(s(double(s(s(y_4))))))))
F(true, s(x1), s(s(y1))) → F(and(gt(x1, s(y1)), gt(y1, 0)), s(plus(s(0), x1)), s(s(s(s(double(y1))))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

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

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Narrowing

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ Rewriting

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ Rewriting

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ Rewriting

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ DependencyGraphProof

                                                                                                                                                  ↳ QDP

                                                                                                                                                    ↳ Instantiation

                                                                                                                                                      ↳ QDP

                                                                                                                                                        ↳ Rewriting

                                                                                                                                                          ↳ QDP

                                                                                                                                                            ↳ Rewriting

                                                                                                                                                              ↳ QDP

                                                                                                                                                                ↳ Rewriting

                                                                                                                                                                  ↳ QDP

                                                                                                                                                                    ↳ Rewriting

                                                                                                                                                                      ↳ QDP

                                                                                                                                                                        ↳ Rewriting

                                                                                                                                                                          ↳ QDP

                                                                                                                                                                            ↳ Rewriting

                                                                                                                                                                              ↳ QDP

                                                                                                                                                                                ↳ Rewriting

                                                                                                                                                                                  ↳ QDP

                                                                                                                                                                                    ↳ Rewriting

                                                                                                                                                                                      ↳ QDP

                                                                                                                                                                                        ↳ Rewriting

                                                                                                                                                                                          ↳ QDP

                                                                                                                                                                                            ↳ Rewriting

                                                                                                                                                                                              ↳ QDP

                                                                                                                                                                                                ↳ Rewriting

                                                                                                                                                                                                  ↳ QDP

                                                                                                                                                                                                    ↳ DependencyGraphProof

                                                                                                                                                                                                      ↳ QDP

                                                                                                                                                                                                        ↳ Rewriting

                    ↳ NonInfProof

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

F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, s(x0), s(s(s(s(y_4))))) → F(gt(x0, s(s(s(y_4)))), s(plus(s(0), x0)), s(s(s(s(double(s(s(y_4))))))))
F(true, s(0), s(s(y0))) → F(and(false, gt(y0, 0)), s(s(0)), s(s(s(s(double(y0))))))
F(true, s(x1), s(s(y1))) → F(and(gt(x1, s(y1)), gt(y1, 0)), s(plus(s(0), x1)), s(s(s(s(double(y1))))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, s(x0), s(s(s(s(y_4))))) → F(gt(x0, s(s(s(y_4)))), s(plus(s(0), x0)), s(s(s(s(double(s(s(y_4)))))))) at position [2,0,0,0,0] we obtained the following new rules:

F(true, s(x0), s(s(s(s(y_4))))) → F(gt(x0, s(s(s(y_4)))), s(plus(s(0), x0)), s(s(s(s(s(s(double(s(y_4)))))))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Narrowing

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ Rewriting

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ Rewriting

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ Rewriting

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ DependencyGraphProof

                                                                                                                                                  ↳ QDP

                                                                                                                                                    ↳ Instantiation

                                                                                                                                                      ↳ QDP

                                                                                                                                                        ↳ Rewriting

                                                                                                                                                          ↳ QDP

                                                                                                                                                            ↳ Rewriting

                                                                                                                                                              ↳ QDP

                                                                                                                                                                ↳ Rewriting

                                                                                                                                                                  ↳ QDP

                                                                                                                                                                    ↳ Rewriting

                                                                                                                                                                      ↳ QDP

                                                                                                                                                                        ↳ Rewriting

                                                                                                                                                                          ↳ QDP

                                                                                                                                                                            ↳ Rewriting

                                                                                                                                                                              ↳ QDP

                                                                                                                                                                                ↳ Rewriting

                                                                                                                                                                                  ↳ QDP

                                                                                                                                                                                    ↳ Rewriting

                                                                                                                                                                                      ↳ QDP

                                                                                                                                                                                        ↳ Rewriting

                                                                                                                                                                                          ↳ QDP

                                                                                                                                                                                            ↳ Rewriting

                                                                                                                                                                                              ↳ QDP

                                                                                                                                                                                                ↳ Rewriting

                                                                                                                                                                                                  ↳ QDP

                                                                                                                                                                                                    ↳ DependencyGraphProof

                                                                                                                                                                                                      ↳ QDP

                                                                                                                                                                                                        ↳ Rewriting

                                                                                                                                                                                                          ↳ QDP

                                                                                                                                                                                                            ↳ Rewriting

                    ↳ NonInfProof

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

F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, s(x0), s(s(s(s(y_4))))) → F(gt(x0, s(s(s(y_4)))), s(plus(s(0), x0)), s(s(s(s(s(s(double(s(y_4)))))))))
F(true, s(0), s(s(y0))) → F(and(false, gt(y0, 0)), s(s(0)), s(s(s(s(double(y0))))))
F(true, s(x1), s(s(y1))) → F(and(gt(x1, s(y1)), gt(y1, 0)), s(plus(s(0), x1)), s(s(s(s(double(y1))))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
By rewriting [13] the rule F(true, s(x0), s(s(s(s(y_4))))) → F(gt(x0, s(s(s(y_4)))), s(plus(s(0), x0)), s(s(s(s(s(s(double(s(y_4))))))))) at position [2,0,0,0,0,0,0] we obtained the following new rules:

F(true, s(x0), s(s(s(s(y_4))))) → F(gt(x0, s(s(s(y_4)))), s(plus(s(0), x0)), s(s(s(s(s(s(s(s(double(y_4))))))))))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Narrowing

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ Rewriting

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ Rewriting

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ Rewriting

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ DependencyGraphProof

                                                                                                                                                  ↳ QDP

                                                                                                                                                    ↳ Instantiation

                                                                                                                                                      ↳ QDP

                                                                                                                                                        ↳ Rewriting

                                                                                                                                                          ↳ QDP

                                                                                                                                                            ↳ Rewriting

                                                                                                                                                              ↳ QDP

                                                                                                                                                                ↳ Rewriting

                                                                                                                                                                  ↳ QDP

                                                                                                                                                                    ↳ Rewriting

                                                                                                                                                                      ↳ QDP

                                                                                                                                                                        ↳ Rewriting

                                                                                                                                                                          ↳ QDP

                                                                                                                                                                            ↳ Rewriting

                                                                                                                                                                              ↳ QDP

                                                                                                                                                                                ↳ Rewriting

                                                                                                                                                                                  ↳ QDP

                                                                                                                                                                                    ↳ Rewriting

                                                                                                                                                                                      ↳ QDP

                                                                                                                                                                                        ↳ Rewriting

                                                                                                                                                                                          ↳ QDP

                                                                                                                                                                                            ↳ Rewriting

                                                                                                                                                                                              ↳ QDP

                                                                                                                                                                                                ↳ Rewriting

                                                                                                                                                                                                  ↳ QDP

                                                                                                                                                                                                    ↳ DependencyGraphProof

                                                                                                                                                                                                      ↳ QDP

                                                                                                                                                                                                        ↳ Rewriting

                                                                                                                                                                                                          ↳ QDP

                                                                                                                                                                                                            ↳ Rewriting

                                                                                                                                                                                                              ↳ QDP

                                                                                                                                                                                                                ↳ QDPOrderProof

                    ↳ NonInfProof

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

F(true, s(x0), s(s(s(s(y_4))))) → F(gt(x0, s(s(s(y_4)))), s(plus(s(0), x0)), s(s(s(s(s(s(s(s(double(y_4))))))))))
F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, s(0), s(s(y0))) → F(and(false, gt(y0, 0)), s(s(0)), s(s(s(s(double(y0))))))
F(true, s(x1), s(s(y1))) → F(and(gt(x1, s(y1)), gt(y1, 0)), s(plus(s(0), x1)), s(s(s(s(double(y1))))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [13].

The following pairs can be oriented strictly and are deleted.

F(true, s(0), s(s(y0))) → F(and(false, gt(y0, 0)), s(s(0)), s(s(s(s(double(y0))))))

The remaining pairs can at least be oriented weakly.

F(true, s(x0), s(s(s(s(y_4))))) → F(gt(x0, s(s(s(y_4)))), s(plus(s(0), x0)), s(s(s(s(s(s(s(s(double(y_4))))))))))
F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, s(x1), s(s(y1))) → F(and(gt(x1, s(y1)), gt(y1, 0)), s(plus(s(0), x1)), s(s(s(s(double(y1))))))

Used ordering: Polynomial interpretation [21]:

POL(0) = 1
POL(F(x₁, x₂, x₃)) = x₁ + x₃
POL(and(x₁, x₂)) = x₁
POL(double(x₁)) = 1
POL(false) = 0
POL(gt(x₁, x₂)) = 1
POL(plus(x₁, x₂)) = 0
POL(s(x₁)) = 1
POL(true) = 1

The following usable rules [14] were oriented:

gt(0, v) → false
gt(s(u), s(v)) → gt(u, v)
and(x, false) → false
gt(s(u), 0) → true
and(x, true) → x

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                      ↳ QDP

                        ↳ Rewriting

                          ↳ QDP

                            ↳ Rewriting

                              ↳ QDP

                                ↳ Rewriting

                                  ↳ QDP

                                    ↳ Rewriting

                                      ↳ QDP

                                        ↳ DependencyGraphProof

                                          ↳ QDP

                                            ↳ Rewriting

                                              ↳ QDP

                                                ↳ Rewriting

                                                  ↳ QDP

                                                    ↳ Rewriting

                                                      ↳ QDP

                                                        ↳ DependencyGraphProof

                                                          ↳ QDP

                                                            ↳ Narrowing

                                                              ↳ QDP

                                                                ↳ DependencyGraphProof

                                                                  ↳ QDP

                                                                    ↳ Rewriting

                                                                      ↳ QDP

                                                                        ↳ Narrowing

                                                                          ↳ QDP

                                                                            ↳ Instantiation

                                                                              ↳ QDP

                                                                                ↳ Rewriting

                                                                                  ↳ QDP

                                                                                    ↳ Rewriting

                                                                                      ↳ QDP

                                                                                        ↳ Rewriting

                                                                                          ↳ QDP

                                                                                            ↳ Rewriting

                                                                                              ↳ QDP

                                                                                                ↳ Rewriting

                                                                                                  ↳ QDP

                                                                                                    ↳ Rewriting

                                                                                                      ↳ QDP

                                                                                                        ↳ Rewriting

                                                                                                          ↳ QDP

                                                                                                            ↳ Rewriting

                                                                                                              ↳ QDP

                                                                                                                ↳ Rewriting

                                                                                                                  ↳ QDP

                                                                                                                    ↳ Narrowing

                                                                                                                      ↳ QDP

                                                                                                                        ↳ Narrowing

                                                                                                                          ↳ QDP

                                                                                                                            ↳ Rewriting

                                                                                                                              ↳ QDP

                                                                                                                                ↳ Instantiation

                                                                                                                                  ↳ QDP

                                                                                                                                    ↳ Rewriting

                                                                                                                                      ↳ QDP

                                                                                                                                        ↳ Rewriting

                                                                                                                                          ↳ QDP

                                                                                                                                            ↳ Rewriting

                                                                                                                                              ↳ QDP

                                                                                                                                                ↳ DependencyGraphProof

                                                                                                                                                  ↳ QDP

                                                                                                                                                    ↳ Instantiation

                                                                                                                                                      ↳ QDP

                                                                                                                                                        ↳ Rewriting

                                                                                                                                                          ↳ QDP

                                                                                                                                                            ↳ Rewriting

                                                                                                                                                              ↳ QDP

                                                                                                                                                                ↳ Rewriting

                                                                                                                                                                  ↳ QDP

                                                                                                                                                                    ↳ Rewriting

                                                                                                                                                                      ↳ QDP

                                                                                                                                                                        ↳ Rewriting

                                                                                                                                                                          ↳ QDP

                                                                                                                                                                            ↳ Rewriting

                                                                                                                                                                              ↳ QDP

                                                                                                                                                                                ↳ Rewriting

                                                                                                                                                                                  ↳ QDP

                                                                                                                                                                                    ↳ Rewriting

                                                                                                                                                                                      ↳ QDP

                                                                                                                                                                                        ↳ Rewriting

                                                                                                                                                                                          ↳ QDP

                                                                                                                                                                                            ↳ Rewriting

                                                                                                                                                                                              ↳ QDP

                                                                                                                                                                                                ↳ Rewriting

                                                                                                                                                                                                  ↳ QDP

                                                                                                                                                                                                    ↳ DependencyGraphProof

                                                                                                                                                                                                      ↳ QDP

                                                                                                                                                                                                        ↳ Rewriting

                                                                                                                                                                                                          ↳ QDP

                                                                                                                                                                                                            ↳ Rewriting

                                                                                                                                                                                                              ↳ QDP

                                                                                                                                                                                                                ↳ QDPOrderProof

                                                                                                                                                                                                                  ↳ QDP

                    ↳ NonInfProof

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

F(true, s(x0), s(s(s(s(y_4))))) → F(gt(x0, s(s(s(y_4)))), s(plus(s(0), x0)), s(s(s(s(s(s(s(s(double(y_4))))))))))
F(true, y_3, s(s(y_4))) → F(and(gt(y_3, s(s(y_4))), gt(y_4, 0)), plus(s(0), y_3), s(s(s(s(double(y_4))))))
F(true, s(x1), s(s(y1))) → F(and(gt(x1, s(y1)), gt(y1, 0)), s(plus(s(0), x1)), s(s(s(s(double(y1))))))

The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The DP Problem is simplified using the Induction Calculus with the following steps:
Note that final constraints are written in bold face.

For Pair F(true, x, y) → F(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y)) the following chains were created:

We consider the chain F(true, x, y) → F(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y)), F(true, x, y) → F(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y)) which results in the following constraint:
- (1) (F(and(gt(x0, x1), gt(x1, s(s(0)))), plus(s(0), x0), double(x1))=F(true, x2, x3) ⇒ F(true, x0, x1)≥F(and(gt(x0, x1), gt(x1, s(s(0)))), plus(s(0), x0), double(x1)))
We simplified constraint (1) using rules (I), (II), (IV), (VII) which results in the following new constraint:
- (2) (gt(x0, x1)=x4∧s(s(0))=x6∧gt(x1, x6)=x5∧and(x4, x5)=true ⇒ F(true, x0, x1)≥F(and(gt(x0, x1), gt(x1, s(s(0)))), plus(s(0), x0), double(x1)))
We simplified constraint (2) using rule (V) (with possible (I) afterwards) using induction on and(x4, x5)=true which results in the following new constraint:
- (3) (x7=true∧gt(x0, x1)=x7∧s(s(0))=x6∧gt(x1, x6)=true ⇒ F(true, x0, x1)≥F(and(gt(x0, x1), gt(x1, s(s(0)))), plus(s(0), x0), double(x1)))
We simplified constraint (3) using rule (III) which results in the following new constraint:
- (4) (gt(x0, x1)=true∧s(s(0))=x6∧gt(x1, x6)=true ⇒ F(true, x0, x1)≥F(and(gt(x0, x1), gt(x1, s(s(0)))), plus(s(0), x0), double(x1)))
We simplified constraint (4) using rule (V) (with possible (I) afterwards) using induction on gt(x0, x1)=true which results in the following new constraints:
- (5) (true=true∧s(s(0))=x6∧gt(0, x6)=true ⇒ F(true, s(x10), 0)≥F(and(gt(s(x10), 0), gt(0, s(s(0)))), plus(s(0), s(x10)), double(0)))
- (6) (gt(x11, x12)=true∧s(s(0))=x6∧gt(s(x12), x6)=true∧(∀x13:gt(x11, x12)=true∧s(s(0))=x13∧gt(x12, x13)=true ⇒ F(true, x11, x12)≥F(and(gt(x11, x12), gt(x12, s(s(0)))), plus(s(0), x11), double(x12))) ⇒ F(true, s(x11), s(x12))≥F(and(gt(s(x11), s(x12)), gt(s(x12), s(s(0)))), plus(s(0), s(x11)), double(s(x12))))
We simplified constraint (5) using rules (I), (II), (VII) which results in the following new constraint:
- (7) (s(s(0))=x6∧0=x14∧gt(x14, x6)=true ⇒ F(true, s(x10), 0)≥F(and(gt(s(x10), 0), gt(0, s(s(0)))), plus(s(0), s(x10)), double(0)))
We simplified constraint (6) using rule (VII) which results in the following new constraint:
- (8) (gt(x11, x12)=true∧s(s(0))=x6∧s(x12)=x20∧gt(x20, x6)=true∧(∀x13:gt(x11, x12)=true∧s(s(0))=x13∧gt(x12, x13)=true ⇒ F(true, x11, x12)≥F(and(gt(x11, x12), gt(x12, s(s(0)))), plus(s(0), x11), double(x12))) ⇒ F(true, s(x11), s(x12))≥F(and(gt(s(x11), s(x12)), gt(s(x12), s(s(0)))), plus(s(0), s(x11)), double(s(x12))))
We simplified constraint (7) using rule (V) (with possible (I) afterwards) using induction on gt(x14, x6)=true which results in the following new constraints:
- (9) (true=true∧s(s(0))=0∧0=s(x16) ⇒ F(true, s(x10), 0)≥F(and(gt(s(x10), 0), gt(0, s(s(0)))), plus(s(0), s(x10)), double(0)))
- (10) (gt(x17, x18)=true∧s(s(0))=s(x18)∧0=s(x17)∧(∀x19:gt(x17, x18)=true∧s(s(0))=x18∧0=x17 ⇒ F(true, s(x19), 0)≥F(and(gt(s(x19), 0), gt(0, s(s(0)))), plus(s(0), s(x19)), double(0))) ⇒ F(true, s(x10), 0)≥F(and(gt(s(x10), 0), gt(0, s(s(0)))), plus(s(0), s(x10)), double(0)))
We solved constraint (9) using rules (I), (II).We solved constraint (10) using rules (I), (II).We simplified constraint (8) using rule (V) (with possible (I) afterwards) using induction on gt(x20, x6)=true which results in the following new constraints:
- (11) (true=true∧gt(x11, x12)=true∧s(s(0))=0∧s(x12)=s(x22)∧(∀x13:gt(x11, x12)=true∧s(s(0))=x13∧gt(x12, x13)=true ⇒ F(true, x11, x12)≥F(and(gt(x11, x12), gt(x12, s(s(0)))), plus(s(0), x11), double(x12))) ⇒ F(true, s(x11), s(x12))≥F(and(gt(s(x11), s(x12)), gt(s(x12), s(s(0)))), plus(s(0), s(x11)), double(s(x12))))
- (12) (gt(x23, x24)=true∧gt(x11, x12)=true∧s(s(0))=s(x24)∧s(x12)=s(x23)∧(∀x13:gt(x11, x12)=true∧s(s(0))=x13∧gt(x12, x13)=true ⇒ F(true, x11, x12)≥F(and(gt(x11, x12), gt(x12, s(s(0)))), plus(s(0), x11), double(x12)))∧(∀x25,x26,x27:gt(x23, x24)=true∧gt(x25, x26)=true∧s(s(0))=x24∧s(x26)=x23∧(∀x27:gt(x25, x26)=true∧s(s(0))=x27∧gt(x26, x27)=true ⇒ F(true, x25, x26)≥F(and(gt(x25, x26), gt(x26, s(s(0)))), plus(s(0), x25), double(x26))) ⇒ F(true, s(x25), s(x26))≥F(and(gt(s(x25), s(x26)), gt(s(x26), s(s(0)))), plus(s(0), s(x25)), double(s(x26)))) ⇒ F(true, s(x11), s(x12))≥F(and(gt(s(x11), s(x12)), gt(s(x12), s(s(0)))), plus(s(0), s(x11)), double(s(x12))))
We solved constraint (11) using rules (I), (II).We simplified constraint (12) using rules (I), (II), (III), (IV) which results in the following new constraint:
- (13) (gt(x23, x24)=true∧gt(x11, x23)=true∧s(0)=x24∧(∀x13:gt(x11, x23)=true∧s(s(0))=x13∧gt(x23, x13)=true ⇒ F(true, x11, x23)≥F(and(gt(x11, x23), gt(x23, s(s(0)))), plus(s(0), x11), double(x23))) ⇒ F(true, s(x11), s(x23))≥F(and(gt(s(x11), s(x23)), gt(s(x23), s(s(0)))), plus(s(0), s(x11)), double(s(x23))))
We simplified constraint (13) using rule (V) (with possible (I) afterwards) using induction on gt(x23, x24)=true which results in the following new constraints:
- (14) (true=true∧gt(x11, s(x29))=true∧s(0)=0∧(∀x13:gt(x11, s(x29))=true∧s(s(0))=x13∧gt(s(x29), x13)=true ⇒ F(true, x11, s(x29))≥F(and(gt(x11, s(x29)), gt(s(x29), s(s(0)))), plus(s(0), x11), double(s(x29)))) ⇒ F(true, s(x11), s(s(x29)))≥F(and(gt(s(x11), s(s(x29))), gt(s(s(x29)), s(s(0)))), plus(s(0), s(x11)), double(s(s(x29)))))
- (15) (gt(x30, x31)=true∧gt(x11, s(x30))=true∧s(0)=s(x31)∧(∀x13:gt(x11, s(x30))=true∧s(s(0))=x13∧gt(s(x30), x13)=true ⇒ F(true, x11, s(x30))≥F(and(gt(x11, s(x30)), gt(s(x30), s(s(0)))), plus(s(0), x11), double(s(x30))))∧(∀x32,x33:gt(x30, x31)=true∧gt(x32, x30)=true∧s(0)=x31∧(∀x33:gt(x32, x30)=true∧s(s(0))=x33∧gt(x30, x33)=true ⇒ F(true, x32, x30)≥F(and(gt(x32, x30), gt(x30, s(s(0)))), plus(s(0), x32), double(x30))) ⇒ F(true, s(x32), s(x30))≥F(and(gt(s(x32), s(x30)), gt(s(x30), s(s(0)))), plus(s(0), s(x32)), double(s(x30)))) ⇒ F(true, s(x11), s(s(x30)))≥F(and(gt(s(x11), s(s(x30))), gt(s(s(x30)), s(s(0)))), plus(s(0), s(x11)), double(s(s(x30)))))
We solved constraint (14) using rules (I), (II).We simplified constraint (15) using rules (I), (II), (IV), (VII) which results in the following new constraint:
- (16) (gt(x30, x31)=true∧s(x30)=x34∧gt(x11, x34)=true∧0=x31∧(∀x32:gt(x30, x31)=true∧gt(x32, x30)=true∧s(0)=x31 ⇒ F(true, s(x32), s(x30))≥F(and(gt(s(x32), s(x30)), gt(s(x30), s(s(0)))), plus(s(0), s(x32)), double(s(x30)))) ⇒ F(true, s(x11), s(s(x30)))≥F(and(gt(s(x11), s(s(x30))), gt(s(s(x30)), s(s(0)))), plus(s(0), s(x11)), double(s(s(x30)))))
We simplified constraint (16) using rule (V) (with possible (I) afterwards) using induction on gt(x11, x34)=true which results in the following new constraints:
- (17) (true=true∧gt(x30, x31)=true∧s(x30)=0∧0=x31∧(∀x32:gt(x30, x31)=true∧gt(x32, x30)=true∧s(0)=x31 ⇒ F(true, s(x32), s(x30))≥F(and(gt(s(x32), s(x30)), gt(s(x30), s(s(0)))), plus(s(0), s(x32)), double(s(x30)))) ⇒ F(true, s(s(x36)), s(s(x30)))≥F(and(gt(s(s(x36)), s(s(x30))), gt(s(s(x30)), s(s(0)))), plus(s(0), s(s(x36))), double(s(s(x30)))))
- (18) (gt(x37, x38)=true∧gt(x30, x31)=true∧s(x30)=s(x38)∧0=x31∧(∀x32:gt(x30, x31)=true∧gt(x32, x30)=true∧s(0)=x31 ⇒ F(true, s(x32), s(x30))≥F(and(gt(s(x32), s(x30)), gt(s(x30), s(s(0)))), plus(s(0), s(x32)), double(s(x30))))∧(∀x39,x40,x41:gt(x37, x38)=true∧gt(x39, x40)=true∧s(x39)=x38∧0=x40∧(∀x41:gt(x39, x40)=true∧gt(x41, x39)=true∧s(0)=x40 ⇒ F(true, s(x41), s(x39))≥F(and(gt(s(x41), s(x39)), gt(s(x39), s(s(0)))), plus(s(0), s(x41)), double(s(x39)))) ⇒ F(true, s(x37), s(s(x39)))≥F(and(gt(s(x37), s(s(x39))), gt(s(s(x39)), s(s(0)))), plus(s(0), s(x37)), double(s(s(x39))))) ⇒ F(true, s(s(x37)), s(s(x30)))≥F(and(gt(s(s(x37)), s(s(x30))), gt(s(s(x30)), s(s(0)))), plus(s(0), s(s(x37))), double(s(s(x30)))))
We solved constraint (17) using rules (I), (II).We simplified constraint (18) using rules (I), (II), (III), (IV) which results in the following new constraint:
- (19) (gt(x37, x38)=true∧gt(x38, x31)=true∧0=x31∧(∀x32:gt(x38, x31)=true∧gt(x32, x38)=true∧s(0)=x31 ⇒ F(true, s(x32), s(x38))≥F(and(gt(s(x32), s(x38)), gt(s(x38), s(s(0)))), plus(s(0), s(x32)), double(s(x38)))) ⇒ F(true, s(s(x37)), s(s(x38)))≥F(and(gt(s(s(x37)), s(s(x38))), gt(s(s(x38)), s(s(0)))), plus(s(0), s(s(x37))), double(s(s(x38)))))
We simplified constraint (19) using rule (V) (with possible (I) afterwards) using induction on gt(x37, x38)=true which results in the following new constraints:
- (20) (true=true∧gt(0, x31)=true∧0=x31∧(∀x32:gt(0, x31)=true∧gt(x32, 0)=true∧s(0)=x31 ⇒ F(true, s(x32), s(0))≥F(and(gt(s(x32), s(0)), gt(s(0), s(s(0)))), plus(s(0), s(x32)), double(s(0)))) ⇒ F(true, s(s(s(x43))), s(s(0)))≥F(and(gt(s(s(s(x43))), s(s(0))), gt(s(s(0)), s(s(0)))), plus(s(0), s(s(s(x43)))), double(s(s(0)))))
- (21) (gt(x44, x45)=true∧gt(s(x45), x31)=true∧0=x31∧(∀x32:gt(s(x45), x31)=true∧gt(x32, s(x45))=true∧s(0)=x31 ⇒ F(true, s(x32), s(s(x45)))≥F(and(gt(s(x32), s(s(x45))), gt(s(s(x45)), s(s(0)))), plus(s(0), s(x32)), double(s(s(x45)))))∧(∀x46,x47:gt(x44, x45)=true∧gt(x45, x46)=true∧0=x46∧(∀x47:gt(x45, x46)=true∧gt(x47, x45)=true∧s(0)=x46 ⇒ F(true, s(x47), s(x45))≥F(and(gt(s(x47), s(x45)), gt(s(x45), s(s(0)))), plus(s(0), s(x47)), double(s(x45)))) ⇒ F(true, s(s(x44)), s(s(x45)))≥F(and(gt(s(s(x44)), s(s(x45))), gt(s(s(x45)), s(s(0)))), plus(s(0), s(s(x44))), double(s(s(x45))))) ⇒ F(true, s(s(s(x44))), s(s(s(x45))))≥F(and(gt(s(s(s(x44))), s(s(s(x45)))), gt(s(s(s(x45))), s(s(0)))), plus(s(0), s(s(s(x44)))), double(s(s(s(x45))))))
We simplified constraint (20) using rules (I), (II), (IV), (VII) which results in the following new constraint:
- (22) (0=x48∧gt(x48, x31)=true∧0=x31 ⇒ F(true, s(s(s(x43))), s(s(0)))≥F(and(gt(s(s(s(x43))), s(s(0))), gt(s(s(0)), s(s(0)))), plus(s(0), s(s(s(x43)))), double(s(s(0)))))
We simplified constraint (21) using rules (IV), (VII) which results in the following new constraint:
- (23) (gt(x44, x45)=true∧s(x45)=x54∧gt(x54, x31)=true∧0=x31∧(∀x46:gt(x44, x45)=true∧gt(x45, x46)=true∧0=x46 ⇒ F(true, s(s(x44)), s(s(x45)))≥F(and(gt(s(s(x44)), s(s(x45))), gt(s(s(x45)), s(s(0)))), plus(s(0), s(s(x44))), double(s(s(x45))))) ⇒ F(true, s(s(s(x44))), s(s(s(x45))))≥F(and(gt(s(s(s(x44))), s(s(s(x45)))), gt(s(s(s(x45))), s(s(0)))), plus(s(0), s(s(s(x44)))), double(s(s(s(x45))))))
We simplified constraint (22) using rule (V) (with possible (I) afterwards) using induction on gt(x48, x31)=true which results in the following new constraints:
- (24) (true=true∧0=s(x50)∧0=0 ⇒ F(true, s(s(s(x43))), s(s(0)))≥F(and(gt(s(s(s(x43))), s(s(0))), gt(s(s(0)), s(s(0)))), plus(s(0), s(s(s(x43)))), double(s(s(0)))))
- (25) (gt(x51, x52)=true∧0=s(x51)∧0=s(x52)∧(∀x53:gt(x51, x52)=true∧0=x51∧0=x52 ⇒ F(true, s(s(s(x53))), s(s(0)))≥F(and(gt(s(s(s(x53))), s(s(0))), gt(s(s(0)), s(s(0)))), plus(s(0), s(s(s(x53)))), double(s(s(0))))) ⇒ F(true, s(s(s(x43))), s(s(0)))≥F(and(gt(s(s(s(x43))), s(s(0))), gt(s(s(0)), s(s(0)))), plus(s(0), s(s(s(x43)))), double(s(s(0)))))
We solved constraint (24) using rules (I), (II).We solved constraint (25) using rules (I), (II).We simplified constraint (23) using rule (V) (with possible (I) afterwards) using induction on gt(x54, x31)=true which results in the following new constraints:
- (26) (true=true∧gt(x44, x45)=true∧s(x45)=s(x56)∧0=0∧(∀x46:gt(x44, x45)=true∧gt(x45, x46)=true∧0=x46 ⇒ F(true, s(s(x44)), s(s(x45)))≥F(and(gt(s(s(x44)), s(s(x45))), gt(s(s(x45)), s(s(0)))), plus(s(0), s(s(x44))), double(s(s(x45))))) ⇒ F(true, s(s(s(x44))), s(s(s(x45))))≥F(and(gt(s(s(s(x44))), s(s(s(x45)))), gt(s(s(s(x45))), s(s(0)))), plus(s(0), s(s(s(x44)))), double(s(s(s(x45))))))
- (27) (gt(x57, x58)=true∧gt(x44, x45)=true∧s(x45)=s(x57)∧0=s(x58)∧(∀x46:gt(x44, x45)=true∧gt(x45, x46)=true∧0=x46 ⇒ F(true, s(s(x44)), s(s(x45)))≥F(and(gt(s(s(x44)), s(s(x45))), gt(s(s(x45)), s(s(0)))), plus(s(0), s(s(x44))), double(s(s(x45)))))∧(∀x59,x60,x61:gt(x57, x58)=true∧gt(x59, x60)=true∧s(x60)=x57∧0=x58∧(∀x61:gt(x59, x60)=true∧gt(x60, x61)=true∧0=x61 ⇒ F(true, s(s(x59)), s(s(x60)))≥F(and(gt(s(s(x59)), s(s(x60))), gt(s(s(x60)), s(s(0)))), plus(s(0), s(s(x59))), double(s(s(x60))))) ⇒ F(true, s(s(s(x59))), s(s(s(x60))))≥F(and(gt(s(s(s(x59))), s(s(s(x60)))), gt(s(s(s(x60))), s(s(0)))), plus(s(0), s(s(s(x59)))), double(s(s(s(x60)))))) ⇒ F(true, s(s(s(x44))), s(s(s(x45))))≥F(and(gt(s(s(s(x44))), s(s(s(x45)))), gt(s(s(s(x45))), s(s(0)))), plus(s(0), s(s(s(x44)))), double(s(s(s(x45))))))
We simplified constraint (26) using rules (I), (II), (IV) which results in the following new constraint:
- (28) (gt(x44, x45)=true ⇒ F(true, s(s(s(x44))), s(s(s(x45))))≥F(and(gt(s(s(s(x44))), s(s(s(x45)))), gt(s(s(s(x45))), s(s(0)))), plus(s(0), s(s(s(x44)))), double(s(s(s(x45))))))
We solved constraint (27) using rules (I), (II).We simplified constraint (28) using rule (V) (with possible (I) afterwards) using induction on gt(x44, x45)=true which results in the following new constraints:
- (29) (true=true ⇒ F(true, s(s(s(s(x63)))), s(s(s(0))))≥F(and(gt(s(s(s(s(x63)))), s(s(s(0)))), gt(s(s(s(0))), s(s(0)))), plus(s(0), s(s(s(s(x63))))), double(s(s(s(0))))))
- (30) (gt(x64, x65)=true∧(gt(x64, x65)=true ⇒ F(true, s(s(s(x64))), s(s(s(x65))))≥F(and(gt(s(s(s(x64))), s(s(s(x65)))), gt(s(s(s(x65))), s(s(0)))), plus(s(0), s(s(s(x64)))), double(s(s(s(x65)))))) ⇒ F(true, s(s(s(s(x64)))), s(s(s(s(x65)))))≥F(and(gt(s(s(s(s(x64)))), s(s(s(s(x65))))), gt(s(s(s(s(x65)))), s(s(0)))), plus(s(0), s(s(s(s(x64))))), double(s(s(s(s(x65)))))))
We simplified constraint (29) using rules (I), (II) which results in the following new constraint:
- (31) (F(true, s(s(s(s(x63)))), s(s(s(0))))≥F(and(gt(s(s(s(s(x63)))), s(s(s(0)))), gt(s(s(s(0))), s(s(0)))), plus(s(0), s(s(s(s(x63))))), double(s(s(s(0))))))
We simplified constraint (30) using rule (VI) where we applied the induction hypothesis (gt(x64, x65)=true ⇒ F(true, s(s(s(x64))), s(s(s(x65))))≥F(and(gt(s(s(s(x64))), s(s(s(x65)))), gt(s(s(s(x65))), s(s(0)))), plus(s(0), s(s(s(x64)))), double(s(s(s(x65)))))) with σ = [ ] which results in the following new constraint:
- (32) (F(true, s(s(s(x64))), s(s(s(x65))))≥F(and(gt(s(s(s(x64))), s(s(s(x65)))), gt(s(s(s(x65))), s(s(0)))), plus(s(0), s(s(s(x64)))), double(s(s(s(x65))))) ⇒ F(true, s(s(s(s(x64)))), s(s(s(s(x65)))))≥F(and(gt(s(s(s(s(x64)))), s(s(s(s(x65))))), gt(s(s(s(s(x65)))), s(s(0)))), plus(s(0), s(s(s(s(x64))))), double(s(s(s(s(x65)))))))

To summarize, we get the following constraints P_≥ for the following pairs.

F(true, x, y) → F(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))
- (F(true, s(s(s(s(x63)))), s(s(s(0))))≥F(and(gt(s(s(s(s(x63)))), s(s(s(0)))), gt(s(s(s(0))), s(s(0)))), plus(s(0), s(s(s(s(x63))))), double(s(s(s(0))))))
- (F(true, s(s(s(x64))), s(s(s(x65))))≥F(and(gt(s(s(s(x64))), s(s(s(x65)))), gt(s(s(s(x65))), s(s(0)))), plus(s(0), s(s(s(x64)))), double(s(s(s(x65))))) ⇒ F(true, s(s(s(s(x64)))), s(s(s(s(x65)))))≥F(and(gt(s(s(s(s(x64)))), s(s(s(s(x65))))), gt(s(s(s(s(x65)))), s(s(0)))), plus(s(0), s(s(s(s(x64))))), double(s(s(s(s(x65)))))))

The constraints for P_> respective P_bound are constructed from P_≥ where we just replace every occurence of "t ≥ s" in P_≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for P_bound.
Using the following integer polynomial ordering the resulting constraints can be solved.
Polynomial interpretation [21]:

POL(0) = 0
POL(F(x₁, x₂, x₃)) = -1 - x₁ + x₂ - x₃
POL(and(x₁, x₂)) = 0
POL(c) = -1
POL(double(x₁)) = 2·x₁
POL(false) = 0
POL(gt(x₁, x₂)) = 0
POL(plus(x₁, x₂)) = x₁ + x₂
POL(s(x₁)) = 2 + x₁
POL(true) = 1

The following pairs are in P_>:

F(true, x, y) → F(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))

The following pairs are in P_bound:

F(true, x, y) → F(and(gt(x, y), gt(y, s(s(0)))), plus(s(0), x), double(y))

The following rules are usable:

0 → double(0)
false → and(x, false)
plus(plus(n, m), u) → plus(n, plus(m, u))
plus(n, s(m)) → s(plus(n, m))
plus(n, 0) → n
x → and(x, true)
s(s(double(x))) → double(s(x))

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

          ↳ QDP

          ↳ QDP

            ↳ UsableRulesProof

              ↳ QDP

                ↳ QReductionProof

                  ↳ QDP

                    ↳ Narrowing

                    ↳ NonInfProof

                      ↳ QDP

                        ↳ PisEmptyProof

Q DP problem:
P is empty.
The TRS R consists of the following rules:

gt(0, v) → false
gt(s(u), 0) → true
gt(s(u), s(v)) → gt(u, v)
and(x, true) → x
and(x, false) → false
plus(n, 0) → n
plus(n, s(m)) → s(plus(n, m))
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(plus(n, m), u) → plus(n, plus(m, u))

The set Q consists of the following terms:

double(0)
gt(0, x0)
plus(x0, s(x1))
gt(s(x0), s(x1))
plus(x0, 0)
and(x0, false)
and(x0, true)
double(s(x0))
gt(s(x0), 0)
plus(plus(x0, x1), x2)

We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.