Left Termination proof of /tmp/tmpyICdA7/minimum-fb.pl

Left Termination of the query pattern minimum(f,b) w.r.t. the given Prolog program could not be shown:

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

minimum₂(tree₃(X, void₀, underscore), X).
minimum₂(tree₃(underscore1, Left, underscore2), X) :- minimum₂(Left, X).

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

minimum_2_in_ag₂(tree_3₃(X, void_0, underscore), X) -> minimum_2_out_ag₂(tree_3₃(X, void_0, underscore), X)
minimum_2_in_ag₂(tree_3₃(underscore1, Left, underscore2), X) -> if_minimum_2_in_1_ag₅(underscore1, Left, underscore2, X, minimum_2_in_ag₂(Left, X))
if_minimum_2_in_1_ag₅(underscore1, Left, underscore2, X, minimum_2_out_ag₂(Left, X)) -> minimum_2_out_ag₂(tree_3₃(underscore1, Left, underscore2), X)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

  ↳ PrologToPiTRSProof

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

minimum_2_in_ag₂(tree_3₃(X, void_0, underscore), X) -> minimum_2_out_ag₂(tree_3₃(X, void_0, underscore), X)
minimum_2_in_ag₂(tree_3₃(underscore1, Left, underscore2), X) -> if_minimum_2_in_1_ag₅(underscore1, Left, underscore2, X, minimum_2_in_ag₂(Left, X))
if_minimum_2_in_1_ag₅(underscore1, Left, underscore2, X, minimum_2_out_ag₂(Left, X)) -> minimum_2_out_ag₂(tree_3₃(underscore1, Left, underscore2), X)

MINIMUM_2_IN_AG₂(tree_3₃(underscore1, Left, underscore2), X) -> IF_MINIMUM_2_IN_1_AG₅(underscore1, Left, underscore2, X, minimum_2_in_ag₂(Left, X))
MINIMUM_2_IN_AG₂(tree_3₃(underscore1, Left, underscore2), X) -> MINIMUM_2_IN_AG₂(Left, X)

The TRS R consists of the following rules:

minimum_2_in_ag₂(tree_3₃(X, void_0, underscore), X) -> minimum_2_out_ag₂(tree_3₃(X, void_0, underscore), X)
minimum_2_in_ag₂(tree_3₃(underscore1, Left, underscore2), X) -> if_minimum_2_in_1_ag₅(underscore1, Left, underscore2, X, minimum_2_in_ag₂(Left, X))
if_minimum_2_in_1_ag₅(underscore1, Left, underscore2, X, minimum_2_out_ag₂(Left, X)) -> minimum_2_out_ag₂(tree_3₃(underscore1, Left, underscore2), X)

The argument filtering Pi contains the following mapping:
minimum_2_in_ag₂(x1, x2) = minimum_2_in_ag₁(x2)
tree_3₃(x1, x2, x3) = tree_3₁(x2)
void_0 = void_0
minimum_2_out_ag₂(x1, x2) = minimum_2_out_ag₁(x1)
if_minimum_2_in_1_ag₅(x1, x2, x3, x4, x5) = if_minimum_2_in_1_ag₁(x5)
MINIMUM_2_IN_AG₂(x1, x2) = MINIMUM_2_IN_AG₁(x2)
IF_MINIMUM_2_IN_1_AG₅(x1, x2, x3, x4, x5) = IF_MINIMUM_2_IN_1_AG₁(x5)

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

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

  ↳ PrologToPiTRSProof

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

MINIMUM_2_IN_AG₂(tree_3₃(underscore1, Left, underscore2), X) -> IF_MINIMUM_2_IN_1_AG₅(underscore1, Left, underscore2, X, minimum_2_in_ag₂(Left, X))
MINIMUM_2_IN_AG₂(tree_3₃(underscore1, Left, underscore2), X) -> MINIMUM_2_IN_AG₂(Left, X)

The TRS R consists of the following rules:

minimum_2_in_ag₂(tree_3₃(X, void_0, underscore), X) -> minimum_2_out_ag₂(tree_3₃(X, void_0, underscore), X)
minimum_2_in_ag₂(tree_3₃(underscore1, Left, underscore2), X) -> if_minimum_2_in_1_ag₅(underscore1, Left, underscore2, X, minimum_2_in_ag₂(Left, X))
if_minimum_2_in_1_ag₅(underscore1, Left, underscore2, X, minimum_2_out_ag₂(Left, X)) -> minimum_2_out_ag₂(tree_3₃(underscore1, Left, underscore2), X)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

  ↳ PrologToPiTRSProof

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

MINIMUM_2_IN_AG₂(tree_3₃(underscore1, Left, underscore2), X) -> MINIMUM_2_IN_AG₂(Left, X)

The TRS R consists of the following rules:

minimum_2_in_ag₂(tree_3₃(X, void_0, underscore), X) -> minimum_2_out_ag₂(tree_3₃(X, void_0, underscore), X)
minimum_2_in_ag₂(tree_3₃(underscore1, Left, underscore2), X) -> if_minimum_2_in_1_ag₅(underscore1, Left, underscore2, X, minimum_2_in_ag₂(Left, X))
if_minimum_2_in_1_ag₅(underscore1, Left, underscore2, X, minimum_2_out_ag₂(Left, X)) -> minimum_2_out_ag₂(tree_3₃(underscore1, Left, underscore2), X)

The argument filtering Pi contains the following mapping:
minimum_2_in_ag₂(x1, x2) = minimum_2_in_ag₁(x2)
tree_3₃(x1, x2, x3) = tree_3₁(x2)
void_0 = void_0
minimum_2_out_ag₂(x1, x2) = minimum_2_out_ag₁(x1)
if_minimum_2_in_1_ag₅(x1, x2, x3, x4, x5) = if_minimum_2_in_1_ag₁(x5)
MINIMUM_2_IN_AG₂(x1, x2) = MINIMUM_2_IN_AG₁(x2)

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

  ↳ PrologToPiTRSProof

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

MINIMUM_2_IN_AG₂(tree_3₃(underscore1, Left, underscore2), X) -> MINIMUM_2_IN_AG₂(Left, X)

R is empty.
The argument filtering Pi contains the following mapping:
tree_3₃(x1, x2, x3) = tree_3₁(x2)
MINIMUM_2_IN_AG₂(x1, x2) = MINIMUM_2_IN_AG₁(x2)

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

  ↳ PrologToPiTRSProof

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

MINIMUM_2_IN_AG₁(X) -> MINIMUM_2_IN_AG₁(X)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {MINIMUM_2_IN_AG₁}.
With regard to the inferred argument filtering the predicates were used in the following modes:
minimum₂: (f,b)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

minimum_2_in_ag₂(tree_3₃(X, void_0, underscore), X) -> minimum_2_out_ag₂(tree_3₃(X, void_0, underscore), X)
minimum_2_in_ag₂(tree_3₃(underscore1, Left, underscore2), X) -> if_minimum_2_in_1_ag₅(underscore1, Left, underscore2, X, minimum_2_in_ag₂(Left, X))
if_minimum_2_in_1_ag₅(underscore1, Left, underscore2, X, minimum_2_out_ag₂(Left, X)) -> minimum_2_out_ag₂(tree_3₃(underscore1, Left, underscore2), X)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

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

minimum_2_in_ag₂(tree_3₃(X, void_0, underscore), X) -> minimum_2_out_ag₂(tree_3₃(X, void_0, underscore), X)
minimum_2_in_ag₂(tree_3₃(underscore1, Left, underscore2), X) -> if_minimum_2_in_1_ag₅(underscore1, Left, underscore2, X, minimum_2_in_ag₂(Left, X))
if_minimum_2_in_1_ag₅(underscore1, Left, underscore2, X, minimum_2_out_ag₂(Left, X)) -> minimum_2_out_ag₂(tree_3₃(underscore1, Left, underscore2), X)

MINIMUM_2_IN_AG₂(tree_3₃(underscore1, Left, underscore2), X) -> IF_MINIMUM_2_IN_1_AG₅(underscore1, Left, underscore2, X, minimum_2_in_ag₂(Left, X))
MINIMUM_2_IN_AG₂(tree_3₃(underscore1, Left, underscore2), X) -> MINIMUM_2_IN_AG₂(Left, X)

The TRS R consists of the following rules:

minimum_2_in_ag₂(tree_3₃(X, void_0, underscore), X) -> minimum_2_out_ag₂(tree_3₃(X, void_0, underscore), X)
minimum_2_in_ag₂(tree_3₃(underscore1, Left, underscore2), X) -> if_minimum_2_in_1_ag₅(underscore1, Left, underscore2, X, minimum_2_in_ag₂(Left, X))
if_minimum_2_in_1_ag₅(underscore1, Left, underscore2, X, minimum_2_out_ag₂(Left, X)) -> minimum_2_out_ag₂(tree_3₃(underscore1, Left, underscore2), X)

The argument filtering Pi contains the following mapping:
minimum_2_in_ag₂(x1, x2) = minimum_2_in_ag₁(x2)
tree_3₃(x1, x2, x3) = tree_3₁(x2)
void_0 = void_0
minimum_2_out_ag₂(x1, x2) = minimum_2_out_ag₂(x1, x2)
if_minimum_2_in_1_ag₅(x1, x2, x3, x4, x5) = if_minimum_2_in_1_ag₂(x4, x5)
MINIMUM_2_IN_AG₂(x1, x2) = MINIMUM_2_IN_AG₁(x2)
IF_MINIMUM_2_IN_1_AG₅(x1, x2, x3, x4, x5) = IF_MINIMUM_2_IN_1_AG₂(x4, x5)

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

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

MINIMUM_2_IN_AG₂(tree_3₃(underscore1, Left, underscore2), X) -> IF_MINIMUM_2_IN_1_AG₅(underscore1, Left, underscore2, X, minimum_2_in_ag₂(Left, X))
MINIMUM_2_IN_AG₂(tree_3₃(underscore1, Left, underscore2), X) -> MINIMUM_2_IN_AG₂(Left, X)

The TRS R consists of the following rules:

minimum_2_in_ag₂(tree_3₃(X, void_0, underscore), X) -> minimum_2_out_ag₂(tree_3₃(X, void_0, underscore), X)
minimum_2_in_ag₂(tree_3₃(underscore1, Left, underscore2), X) -> if_minimum_2_in_1_ag₅(underscore1, Left, underscore2, X, minimum_2_in_ag₂(Left, X))
if_minimum_2_in_1_ag₅(underscore1, Left, underscore2, X, minimum_2_out_ag₂(Left, X)) -> minimum_2_out_ag₂(tree_3₃(underscore1, Left, underscore2), X)

The argument filtering Pi contains the following mapping:
minimum_2_in_ag₂(x1, x2) = minimum_2_in_ag₁(x2)
tree_3₃(x1, x2, x3) = tree_3₁(x2)
void_0 = void_0
minimum_2_out_ag₂(x1, x2) = minimum_2_out_ag₂(x1, x2)
if_minimum_2_in_1_ag₅(x1, x2, x3, x4, x5) = if_minimum_2_in_1_ag₂(x4, x5)
MINIMUM_2_IN_AG₂(x1, x2) = MINIMUM_2_IN_AG₁(x2)
IF_MINIMUM_2_IN_1_AG₅(x1, x2, x3, x4, x5) = IF_MINIMUM_2_IN_1_AG₂(x4, x5)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph contains 1 SCC with 1 less node.

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

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

MINIMUM_2_IN_AG₂(tree_3₃(underscore1, Left, underscore2), X) -> MINIMUM_2_IN_AG₂(Left, X)

The TRS R consists of the following rules:

minimum_2_in_ag₂(tree_3₃(X, void_0, underscore), X) -> minimum_2_out_ag₂(tree_3₃(X, void_0, underscore), X)
minimum_2_in_ag₂(tree_3₃(underscore1, Left, underscore2), X) -> if_minimum_2_in_1_ag₅(underscore1, Left, underscore2, X, minimum_2_in_ag₂(Left, X))
if_minimum_2_in_1_ag₅(underscore1, Left, underscore2, X, minimum_2_out_ag₂(Left, X)) -> minimum_2_out_ag₂(tree_3₃(underscore1, Left, underscore2), X)

The argument filtering Pi contains the following mapping:
minimum_2_in_ag₂(x1, x2) = minimum_2_in_ag₁(x2)
tree_3₃(x1, x2, x3) = tree_3₁(x2)
void_0 = void_0
minimum_2_out_ag₂(x1, x2) = minimum_2_out_ag₂(x1, x2)
if_minimum_2_in_1_ag₅(x1, x2, x3, x4, x5) = if_minimum_2_in_1_ag₂(x4, x5)
MINIMUM_2_IN_AG₂(x1, x2) = MINIMUM_2_IN_AG₁(x2)

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

                ↳ PiDP

                  ↳ PiDPToQDPProof

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

MINIMUM_2_IN_AG₂(tree_3₃(underscore1, Left, underscore2), X) -> MINIMUM_2_IN_AG₂(Left, X)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

                ↳ PiDP

                  ↳ PiDPToQDPProof

                    ↳ QDP

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

MINIMUM_2_IN_AG₁(X) -> MINIMUM_2_IN_AG₁(X)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {MINIMUM_2_IN_AG₁}.