Termination proof of /tmp/tmpulxDHw/Ex49

Termination of the following Term Rewriting System could be proven:

Context-sensitive rewrite system:
The TRS R consists of the following rules:

minus(0, Y) → 0
minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → true
geq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)
div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) → X
if(false, X, Y) → Y

The replacement map contains the following entries:

minus: empty set
0: empty set
s: {1}
geq: empty set
true: empty set
false: empty set
div: {1}
if: {1}

↳ CSR

  ↳ CSRInnermostProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

minus(0, Y) → 0
minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → true
geq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)
div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) → X
if(false, X, Y) → Y

The replacement map contains the following entries:

minus: empty set
0: empty set
s: {1}
geq: empty set
true: empty set
false: empty set
div: {1}
if: {1}

The CSR is orthogonal. By [10] we can switch to innermost.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

Context-sensitive rewrite system:
The TRS R consists of the following rules:

minus(0, Y) → 0
minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → true
geq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)
div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) → X
if(false, X, Y) → Y

The replacement map contains the following entries:

minus: empty set
0: empty set
s: {1}
geq: empty set
true: empty set
false: empty set
div: {1}
if: {1}

Innermost Strategy.

Using Improved CS-DPs we result in the following initial Q-CSDP problem.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {s} are replacing on all positions.
For all symbols f in {div, if, IF, DIV} we have µ(f) = {1}.
The symbols in {minus, geq, MINUS, GEQ, U} are not replacing on any position.

The ordinary context-sensitive dependency pairs DP_o are:

MINUS(s(X), s(Y)) → MINUS(X, Y)
GEQ(s(X), s(Y)) → GEQ(X, Y)
DIV(s(X), s(Y)) → IF(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
DIV(s(X), s(Y)) → GEQ(X, Y)

The collapsing dependency pairs are DP_c:

IF(true, X, Y) → X
IF(false, X, Y) → Y

The hidden terms of R are:

div(minus(X, Y), s(Y))
minus(X, Y)

Every hiding context is built from:

s on positions {1}
div on positions {1}

Hence, the new unhiding pairs DP_u are :

IF(true, X, Y) → U(X)
IF(false, X, Y) → U(Y)
U(s(x_0)) → U(x_0)
U(div(x_0, x_1)) → U(x_0)
U(div(minus(X, Y), s(Y))) → DIV(minus(X, Y), s(Y))
U(minus(X, Y)) → MINUS(X, Y)

The TRS R consists of the following rules:

minus(0, Y) → 0
minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → true
geq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)
div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) → X
if(false, X, Y) → Y

The set Q consists of the following terms:

minus(0, x0)
minus(s(x0), s(x1))
geq(x0, 0)
geq(0, s(x0))
geq(s(x0), s(x1))
div(0, s(x0))
div(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)

The approximation of the Context-Sensitive Dependency Graph contains 3 SCCs with 6 less nodes.
The rules U(div(minus(x0, x1), s(x1))) → DIV(minus(x0, x1), s(x1)) and DIV(s(z0), s(z1)) → IF(geq(z0, z1), s(div(minus(z0, z1), s(z1))), 0) form no chain, because ECap^µ_R'(DIV(s(z0), s(z1))) = DIV(s(x_1), s(z1)) does not unify with DIV(minus(x0, x1), s(x1)).
R' =

( 0, minus(0, Y))
( minus(X, Y), minus(s(X), s(Y)))

The rules U(div(minus(x0, x1), s(x1))) → DIV(minus(x0, x1), s(x1)) and DIV(s(z0), s(z1)) → GEQ(z0, z1) form no chain, because ECap^µ_R'(DIV(s(z0), s(z1))) = DIV(s(x_1), s(z1)) does not unify with DIV(minus(x0, x1), s(x1)).
R' =

( 0, minus(0, Y))
( minus(X, Y), minus(s(X), s(Y)))

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

                ↳ QCSDPSubtermProof

              ↳ QCSDP

              ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {s} are replacing on all positions.
For all symbols f in {div, if} we have µ(f) = {1}.
The symbols in {minus, geq, GEQ} are not replacing on any position.

The TRS P consists of the following rules:

GEQ(s(X), s(Y)) → GEQ(X, Y)

The TRS R consists of the following rules:

minus(0, Y) → 0
minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → true
geq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)
div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) → X
if(false, X, Y) → Y

The set Q consists of the following terms:

minus(0, x0)
minus(s(x0), s(x1))
geq(x0, 0)
geq(0, s(x0))
geq(s(x0), s(x1))
div(0, s(x0))
div(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

GEQ(s(X), s(Y)) → GEQ(X, Y)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
GEQ(x1, x2) = x1

Subterm Order

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

                ↳ QCSDPSubtermProof

                  ↳ QCSDP

                    ↳ PIsEmptyProof

              ↳ QCSDP

              ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {s} are replacing on all positions.
For all symbols f in {div, if} we have µ(f) = {1}.
The symbols in {minus, geq} are not replacing on any position.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

minus(0, Y) → 0
minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → true
geq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)
div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) → X
if(false, X, Y) → Y

The set Q consists of the following terms:

minus(0, x0)
minus(s(x0), s(x1))
geq(x0, 0)
geq(0, s(x0))
geq(s(x0), s(x1))
div(0, s(x0))
div(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

              ↳ QCSDP

                ↳ QCSDPSubtermProof

              ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {s} are replacing on all positions.
For all symbols f in {div, if} we have µ(f) = {1}.
The symbols in {minus, geq, MINUS} are not replacing on any position.

The TRS P consists of the following rules:

MINUS(s(X), s(Y)) → MINUS(X, Y)

The TRS R consists of the following rules:

minus(0, Y) → 0
minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → true
geq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)
div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) → X
if(false, X, Y) → Y

The set Q consists of the following terms:

minus(0, x0)
minus(s(x0), s(x1))
geq(x0, 0)
geq(0, s(x0))
geq(s(x0), s(x1))
div(0, s(x0))
div(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

MINUS(s(X), s(Y)) → MINUS(X, Y)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
MINUS(x1, x2) = x1

Subterm Order

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

              ↳ QCSDP

                ↳ QCSDPSubtermProof

                  ↳ QCSDP

                    ↳ PIsEmptyProof

              ↳ QCSDP

Q-restricted context-sensitive dependency pair problem:
The symbols in {s} are replacing on all positions.
For all symbols f in {div, if} we have µ(f) = {1}.
The symbols in {minus, geq} are not replacing on any position.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

minus(0, Y) → 0
minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → true
geq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)
div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) → X
if(false, X, Y) → Y

The set Q consists of the following terms:

minus(0, x0)
minus(s(x0), s(x1))
geq(x0, 0)
geq(0, s(x0))
geq(s(x0), s(x1))
div(0, s(x0))
div(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

              ↳ QCSDP

              ↳ QCSDP

                ↳ QCSDPSubtermProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {s} are replacing on all positions.
For all symbols f in {div, if} we have µ(f) = {1}.
The symbols in {minus, geq, U} are not replacing on any position.

The TRS P consists of the following rules:

U(s(x_0)) → U(x_0)
U(div(x_0, x_1)) → U(x_0)

The TRS R consists of the following rules:

minus(0, Y) → 0
minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → true
geq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)
div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) → X
if(false, X, Y) → Y

The set Q consists of the following terms:

minus(0, x0)
minus(s(x0), s(x1))
geq(x0, 0)
geq(0, s(x0))
geq(s(x0), s(x1))
div(0, s(x0))
div(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)

We use the subterm processor [20].

The following pairs can be oriented strictly and are deleted.

U(s(x_0)) → U(x_0)
U(div(x_0, x_1)) → U(x_0)

The remaining pairs can at least be oriented weakly.
none
Used ordering: Combined order from the following AFS and order.
U(x1) = x1

Subterm Order

↳ CSR

  ↳ CSRInnermostProof

    ↳ CSR

      ↳ CSDependencyPairsProof

        ↳ QCSDP

          ↳ QCSDependencyGraphProof

            ↳ AND

              ↳ QCSDP

              ↳ QCSDP

              ↳ QCSDP

                ↳ QCSDPSubtermProof

                  ↳ QCSDP

                    ↳ PIsEmptyProof

Q-restricted context-sensitive dependency pair problem:
The symbols in {s} are replacing on all positions.
For all symbols f in {div, if} we have µ(f) = {1}.
The symbols in {minus, geq} are not replacing on any position.

The TRS P consists of the following rules:
none

The TRS R consists of the following rules:

minus(0, Y) → 0
minus(s(X), s(Y)) → minus(X, Y)
geq(X, 0) → true
geq(0, s(Y)) → false
geq(s(X), s(Y)) → geq(X, Y)
div(0, s(Y)) → 0
div(s(X), s(Y)) → if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) → X
if(false, X, Y) → Y

The set Q consists of the following terms:

minus(0, x0)
minus(s(x0), s(x1))
geq(x0, 0)
geq(0, s(x0))
geq(s(x0), s(x1))
div(0, s(x0))
div(s(x0), s(x1))
if(true, x0, x1)
if(false, x0, x1)

The TRS P is empty. Hence, there is no (P,Q,R,µ)-chain.