Left Termination proof of /tmp/tmpu2YqJ1/quot.pl

Left Termination of the query pattern div(b,b,f) w.r.t. the given Prolog program could successfully be proven:

↳ PROLOG

  ↳ PrologToPiTRSProof

div₃(X, Y, Z) :- quot₄(X, Y, Y, Z).
quot₄(0₀, s₁(Y), s₁(Z), 0₀).
quot₄(s₁(X), s₁(Y), Z, U) :- quot₄(X, Y, Z, U).
quot₄(X, 0₀, s₁(Z), s₁(U)) :- quot₄(X, s₁(Z), s₁(Z), U).

With regard to the inferred argument filtering the predicates were used in the following modes:
div₃: (b,b,f)
quot₄: (b,b,b,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

div_3_in_gga₃(X, Y, Z) -> if_div_3_in_1_gga₄(X, Y, Z, quot_4_in_ggga₄(X, Y, Y, Z))
quot_4_in_ggga₄(0_0, s_1₁(Y), s_1₁(Z), 0_0) -> quot_4_out_ggga₄(0_0, s_1₁(Y), s_1₁(Z), 0_0)
quot_4_in_ggga₄(s_1₁(X), s_1₁(Y), Z, U) -> if_quot_4_in_1_ggga₅(X, Y, Z, U, quot_4_in_ggga₄(X, Y, Z, U))
quot_4_in_ggga₄(X, 0_0, s_1₁(Z), s_1₁(U)) -> if_quot_4_in_2_ggga₄(X, Z, U, quot_4_in_ggga₄(X, s_1₁(Z), s_1₁(Z), U))
if_quot_4_in_2_ggga₄(X, Z, U, quot_4_out_ggga₄(X, s_1₁(Z), s_1₁(Z), U)) -> quot_4_out_ggga₄(X, 0_0, s_1₁(Z), s_1₁(U))
if_quot_4_in_1_ggga₅(X, Y, Z, U, quot_4_out_ggga₄(X, Y, Z, U)) -> quot_4_out_ggga₄(s_1₁(X), s_1₁(Y), Z, U)
if_div_3_in_1_gga₄(X, Y, Z, quot_4_out_ggga₄(X, Y, Y, Z)) -> div_3_out_gga₃(X, Y, Z)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

div_3_in_gga₃(X, Y, Z) -> if_div_3_in_1_gga₄(X, Y, Z, quot_4_in_ggga₄(X, Y, Y, Z))
quot_4_in_ggga₄(0_0, s_1₁(Y), s_1₁(Z), 0_0) -> quot_4_out_ggga₄(0_0, s_1₁(Y), s_1₁(Z), 0_0)
quot_4_in_ggga₄(s_1₁(X), s_1₁(Y), Z, U) -> if_quot_4_in_1_ggga₅(X, Y, Z, U, quot_4_in_ggga₄(X, Y, Z, U))
quot_4_in_ggga₄(X, 0_0, s_1₁(Z), s_1₁(U)) -> if_quot_4_in_2_ggga₄(X, Z, U, quot_4_in_ggga₄(X, s_1₁(Z), s_1₁(Z), U))
if_quot_4_in_2_ggga₄(X, Z, U, quot_4_out_ggga₄(X, s_1₁(Z), s_1₁(Z), U)) -> quot_4_out_ggga₄(X, 0_0, s_1₁(Z), s_1₁(U))
if_quot_4_in_1_ggga₅(X, Y, Z, U, quot_4_out_ggga₄(X, Y, Z, U)) -> quot_4_out_ggga₄(s_1₁(X), s_1₁(Y), Z, U)
if_div_3_in_1_gga₄(X, Y, Z, quot_4_out_ggga₄(X, Y, Y, Z)) -> div_3_out_gga₃(X, Y, Z)

DIV_3_IN_GGA₃(X, Y, Z) -> IF_DIV_3_IN_1_GGA₄(X, Y, Z, quot_4_in_ggga₄(X, Y, Y, Z))
DIV_3_IN_GGA₃(X, Y, Z) -> QUOT_4_IN_GGGA₄(X, Y, Y, Z)
QUOT_4_IN_GGGA₄(s_1₁(X), s_1₁(Y), Z, U) -> IF_QUOT_4_IN_1_GGGA₅(X, Y, Z, U, quot_4_in_ggga₄(X, Y, Z, U))
QUOT_4_IN_GGGA₄(s_1₁(X), s_1₁(Y), Z, U) -> QUOT_4_IN_GGGA₄(X, Y, Z, U)
QUOT_4_IN_GGGA₄(X, 0_0, s_1₁(Z), s_1₁(U)) -> IF_QUOT_4_IN_2_GGGA₄(X, Z, U, quot_4_in_ggga₄(X, s_1₁(Z), s_1₁(Z), U))
QUOT_4_IN_GGGA₄(X, 0_0, s_1₁(Z), s_1₁(U)) -> QUOT_4_IN_GGGA₄(X, s_1₁(Z), s_1₁(Z), U)

The TRS R consists of the following rules:

div_3_in_gga₃(X, Y, Z) -> if_div_3_in_1_gga₄(X, Y, Z, quot_4_in_ggga₄(X, Y, Y, Z))
quot_4_in_ggga₄(0_0, s_1₁(Y), s_1₁(Z), 0_0) -> quot_4_out_ggga₄(0_0, s_1₁(Y), s_1₁(Z), 0_0)
quot_4_in_ggga₄(s_1₁(X), s_1₁(Y), Z, U) -> if_quot_4_in_1_ggga₅(X, Y, Z, U, quot_4_in_ggga₄(X, Y, Z, U))
quot_4_in_ggga₄(X, 0_0, s_1₁(Z), s_1₁(U)) -> if_quot_4_in_2_ggga₄(X, Z, U, quot_4_in_ggga₄(X, s_1₁(Z), s_1₁(Z), U))
if_quot_4_in_2_ggga₄(X, Z, U, quot_4_out_ggga₄(X, s_1₁(Z), s_1₁(Z), U)) -> quot_4_out_ggga₄(X, 0_0, s_1₁(Z), s_1₁(U))
if_quot_4_in_1_ggga₅(X, Y, Z, U, quot_4_out_ggga₄(X, Y, Z, U)) -> quot_4_out_ggga₄(s_1₁(X), s_1₁(Y), Z, U)
if_div_3_in_1_gga₄(X, Y, Z, quot_4_out_ggga₄(X, Y, Y, Z)) -> div_3_out_gga₃(X, Y, Z)

The argument filtering Pi contains the following mapping:
div_3_in_gga₃(x1, x2, x3) = div_3_in_gga₂(x1, x2)
0_0 = 0_0
s_1₁(x1) = s_1₁(x1)
if_div_3_in_1_gga₄(x1, x2, x3, x4) = if_div_3_in_1_gga₁(x4)
quot_4_in_ggga₄(x1, x2, x3, x4) = quot_4_in_ggga₃(x1, x2, x3)
quot_4_out_ggga₄(x1, x2, x3, x4) = quot_4_out_ggga₁(x4)
if_quot_4_in_1_ggga₅(x1, x2, x3, x4, x5) = if_quot_4_in_1_ggga₁(x5)
if_quot_4_in_2_ggga₄(x1, x2, x3, x4) = if_quot_4_in_2_ggga₁(x4)
div_3_out_gga₃(x1, x2, x3) = div_3_out_gga₁(x3)
DIV_3_IN_GGA₃(x1, x2, x3) = DIV_3_IN_GGA₂(x1, x2)
QUOT_4_IN_GGGA₄(x1, x2, x3, x4) = QUOT_4_IN_GGGA₃(x1, x2, x3)
IF_DIV_3_IN_1_GGA₄(x1, x2, x3, x4) = IF_DIV_3_IN_1_GGA₁(x4)
IF_QUOT_4_IN_2_GGGA₄(x1, x2, x3, x4) = IF_QUOT_4_IN_2_GGGA₁(x4)
IF_QUOT_4_IN_1_GGGA₅(x1, x2, x3, x4, x5) = IF_QUOT_4_IN_1_GGGA₁(x5)

We have to consider all (P,R,Pi)-chains

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

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

DIV_3_IN_GGA₃(X, Y, Z) -> IF_DIV_3_IN_1_GGA₄(X, Y, Z, quot_4_in_ggga₄(X, Y, Y, Z))
DIV_3_IN_GGA₃(X, Y, Z) -> QUOT_4_IN_GGGA₄(X, Y, Y, Z)
QUOT_4_IN_GGGA₄(s_1₁(X), s_1₁(Y), Z, U) -> IF_QUOT_4_IN_1_GGGA₅(X, Y, Z, U, quot_4_in_ggga₄(X, Y, Z, U))
QUOT_4_IN_GGGA₄(s_1₁(X), s_1₁(Y), Z, U) -> QUOT_4_IN_GGGA₄(X, Y, Z, U)
QUOT_4_IN_GGGA₄(X, 0_0, s_1₁(Z), s_1₁(U)) -> IF_QUOT_4_IN_2_GGGA₄(X, Z, U, quot_4_in_ggga₄(X, s_1₁(Z), s_1₁(Z), U))
QUOT_4_IN_GGGA₄(X, 0_0, s_1₁(Z), s_1₁(U)) -> QUOT_4_IN_GGGA₄(X, s_1₁(Z), s_1₁(Z), U)

The TRS R consists of the following rules:

div_3_in_gga₃(X, Y, Z) -> if_div_3_in_1_gga₄(X, Y, Z, quot_4_in_ggga₄(X, Y, Y, Z))
quot_4_in_ggga₄(0_0, s_1₁(Y), s_1₁(Z), 0_0) -> quot_4_out_ggga₄(0_0, s_1₁(Y), s_1₁(Z), 0_0)
quot_4_in_ggga₄(s_1₁(X), s_1₁(Y), Z, U) -> if_quot_4_in_1_ggga₅(X, Y, Z, U, quot_4_in_ggga₄(X, Y, Z, U))
quot_4_in_ggga₄(X, 0_0, s_1₁(Z), s_1₁(U)) -> if_quot_4_in_2_ggga₄(X, Z, U, quot_4_in_ggga₄(X, s_1₁(Z), s_1₁(Z), U))
if_quot_4_in_2_ggga₄(X, Z, U, quot_4_out_ggga₄(X, s_1₁(Z), s_1₁(Z), U)) -> quot_4_out_ggga₄(X, 0_0, s_1₁(Z), s_1₁(U))
if_quot_4_in_1_ggga₅(X, Y, Z, U, quot_4_out_ggga₄(X, Y, Z, U)) -> quot_4_out_ggga₄(s_1₁(X), s_1₁(Y), Z, U)
if_div_3_in_1_gga₄(X, Y, Z, quot_4_out_ggga₄(X, Y, Y, Z)) -> div_3_out_gga₃(X, Y, Z)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

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

QUOT_4_IN_GGGA₄(X, 0_0, s_1₁(Z), s_1₁(U)) -> QUOT_4_IN_GGGA₄(X, s_1₁(Z), s_1₁(Z), U)
QUOT_4_IN_GGGA₄(s_1₁(X), s_1₁(Y), Z, U) -> QUOT_4_IN_GGGA₄(X, Y, Z, U)

The TRS R consists of the following rules:

div_3_in_gga₃(X, Y, Z) -> if_div_3_in_1_gga₄(X, Y, Z, quot_4_in_ggga₄(X, Y, Y, Z))
quot_4_in_ggga₄(0_0, s_1₁(Y), s_1₁(Z), 0_0) -> quot_4_out_ggga₄(0_0, s_1₁(Y), s_1₁(Z), 0_0)
quot_4_in_ggga₄(s_1₁(X), s_1₁(Y), Z, U) -> if_quot_4_in_1_ggga₅(X, Y, Z, U, quot_4_in_ggga₄(X, Y, Z, U))
quot_4_in_ggga₄(X, 0_0, s_1₁(Z), s_1₁(U)) -> if_quot_4_in_2_ggga₄(X, Z, U, quot_4_in_ggga₄(X, s_1₁(Z), s_1₁(Z), U))
if_quot_4_in_2_ggga₄(X, Z, U, quot_4_out_ggga₄(X, s_1₁(Z), s_1₁(Z), U)) -> quot_4_out_ggga₄(X, 0_0, s_1₁(Z), s_1₁(U))
if_quot_4_in_1_ggga₅(X, Y, Z, U, quot_4_out_ggga₄(X, Y, Z, U)) -> quot_4_out_ggga₄(s_1₁(X), s_1₁(Y), Z, U)
if_div_3_in_1_gga₄(X, Y, Z, quot_4_out_ggga₄(X, Y, Y, Z)) -> div_3_out_gga₃(X, Y, Z)

The argument filtering Pi contains the following mapping:
div_3_in_gga₃(x1, x2, x3) = div_3_in_gga₂(x1, x2)
0_0 = 0_0
s_1₁(x1) = s_1₁(x1)
if_div_3_in_1_gga₄(x1, x2, x3, x4) = if_div_3_in_1_gga₁(x4)
quot_4_in_ggga₄(x1, x2, x3, x4) = quot_4_in_ggga₃(x1, x2, x3)
quot_4_out_ggga₄(x1, x2, x3, x4) = quot_4_out_ggga₁(x4)
if_quot_4_in_1_ggga₅(x1, x2, x3, x4, x5) = if_quot_4_in_1_ggga₁(x5)
if_quot_4_in_2_ggga₄(x1, x2, x3, x4) = if_quot_4_in_2_ggga₁(x4)
div_3_out_gga₃(x1, x2, x3) = div_3_out_gga₁(x3)
QUOT_4_IN_GGGA₄(x1, x2, x3, x4) = QUOT_4_IN_GGGA₃(x1, x2, x3)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

                ↳ PiDP

                  ↳ PiDPToQDPProof

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

QUOT_4_IN_GGGA₄(X, 0_0, s_1₁(Z), s_1₁(U)) -> QUOT_4_IN_GGGA₄(X, s_1₁(Z), s_1₁(Z), U)
QUOT_4_IN_GGGA₄(s_1₁(X), s_1₁(Y), Z, U) -> QUOT_4_IN_GGGA₄(X, Y, Z, U)

R is empty.
The argument filtering Pi contains the following mapping:
0_0 = 0_0
s_1₁(x1) = s_1₁(x1)
QUOT_4_IN_GGGA₄(x1, x2, x3, x4) = QUOT_4_IN_GGGA₃(x1, x2, x3)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

                ↳ PiDP

                  ↳ PiDPToQDPProof

                    ↳ QDP

                      ↳ QDPSizeChangeProof

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

QUOT_4_IN_GGGA₃(X, 0_0, s_1₁(Z)) -> QUOT_4_IN_GGGA₃(X, s_1₁(Z), s_1₁(Z))
QUOT_4_IN_GGGA₃(s_1₁(X), s_1₁(Y), Z) -> QUOT_4_IN_GGGA₃(X, Y, Z)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {QUOT_4_IN_GGGA₃}.
By using the subterm criterion together with the size-change analysis 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:

QUOT_4_IN_GGGA₃(s_1₁(X), s_1₁(Y), Z) -> QUOT_4_IN_GGGA₃(X, Y, Z)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
QUOT_4_IN_GGGA₃(X, 0_0, s_1₁(Z)) -> QUOT_4_IN_GGGA₃(X, s_1₁(Z), s_1₁(Z))
The graph contains the following edges 1 >= 1, 3 >= 2, 3 >= 3