Left Termination proof of /tmp/tmppfiIPU/delmin-ffb.pl

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

↳ PROLOG

  ↳ UnrequestedClauseRemoverProof

delete₃(X, tree₃(X, void₀, Right), Right).
delete₃(X, tree₃(X, Left, void₀), Left).
delete₃(X, tree₃(X, Left, Right), tree₃(Y, Left, Right1)) :- delmin₃(Right, Y, Right1).
delete₃(X, tree₃(Y, Left, Right), tree₃(Y, Left1, Right)) :- less₂(X, Y), delete₃(X, Left, Left1).
delete₃(X, tree₃(Y, Left, Right), tree₃(Y, Left, Right1)) :- less₂(Y, X), delete₃(X, Right, Right1).
delmin₃(tree₃(Y, void₀, Right), Y, Right).
delmin₃(tree₃(X, Left, underscore), Y, tree₃(X, Left1, underscore1)) :- delmin₃(Left, Y, Left1).
less₂(0₀, s₁(underscore2)).
less₂(s₁(X), s₁(Y)) :- less₂(X, Y).

The clauses

delete₃(X, tree₃(X, void₀, Right), Right).
delete₃(X, tree₃(X, Left, void₀), Left).
delete₃(X, tree₃(X, Left, Right), tree₃(Y, Left, Right1)) :- delmin₃(Right, Y, Right1).
delete₃(X, tree₃(Y, Left, Right), tree₃(Y, Left1, Right)) :- less₂(X, Y), delete₃(X, Left, Left1).
delete₃(X, tree₃(Y, Left, Right), tree₃(Y, Left, Right1)) :- less₂(Y, X), delete₃(X, Right, Right1).
less₂(0₀, s₁(underscore2)).
less₂(s₁(X), s₁(Y)) :- less₂(X, Y).

can be ignored, as they are not needed by any of the given querys.

Deleting these clauses results in the following prolog program:

delmin₃(tree₃(Y, void₀, Right), Y, Right).
delmin₃(tree₃(X, Left, underscore), Y, tree₃(X, Left1, underscore1)) :- delmin₃(Left, Y, Left1).

↳ PROLOG

  ↳ UnrequestedClauseRemoverProof

    ↳ PROLOG

      ↳ PrologToPiTRSProof

delmin₃(tree₃(Y, void₀, Right), Y, Right).
delmin₃(tree₃(X, Left, underscore), Y, tree₃(X, Left1, underscore1)) :- delmin₃(Left, Y, Left1).

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

delmin_3_in_aag₃(tree_3₃(Y, void_0, Right), Y, Right) -> delmin_3_out_aag₃(tree_3₃(Y, void_0, Right), Y, Right)
delmin_3_in_aag₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> if_delmin_3_in_1_aag₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_in_aag₃(Left, Y, Left1))
if_delmin_3_in_1_aag₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_out_aag₃(Left, Y, Left1)) -> delmin_3_out_aag₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1))

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ UnrequestedClauseRemoverProof

    ↳ PROLOG

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

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

delmin_3_in_aag₃(tree_3₃(Y, void_0, Right), Y, Right) -> delmin_3_out_aag₃(tree_3₃(Y, void_0, Right), Y, Right)
delmin_3_in_aag₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> if_delmin_3_in_1_aag₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_in_aag₃(Left, Y, Left1))
if_delmin_3_in_1_aag₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_out_aag₃(Left, Y, Left1)) -> delmin_3_out_aag₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1))

DELMIN_3_IN_AAG₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> IF_DELMIN_3_IN_1_AAG₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_in_aag₃(Left, Y, Left1))
DELMIN_3_IN_AAG₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> DELMIN_3_IN_AAG₃(Left, Y, Left1)

The TRS R consists of the following rules:

delmin_3_in_aag₃(tree_3₃(Y, void_0, Right), Y, Right) -> delmin_3_out_aag₃(tree_3₃(Y, void_0, Right), Y, Right)
delmin_3_in_aag₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> if_delmin_3_in_1_aag₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_in_aag₃(Left, Y, Left1))
if_delmin_3_in_1_aag₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_out_aag₃(Left, Y, Left1)) -> delmin_3_out_aag₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1))

The argument filtering Pi contains the following mapping:
delmin_3_in_aag₃(x1, x2, x3) = delmin_3_in_aag₁(x3)
tree_3₃(x1, x2, x3) = tree_3₁(x2)
void_0 = void_0
delmin_3_out_aag₃(x1, x2, x3) = delmin_3_out_aag₁(x1)
if_delmin_3_in_1_aag₇(x1, x2, x3, x4, x5, x6, x7) = if_delmin_3_in_1_aag₁(x7)
DELMIN_3_IN_AAG₃(x1, x2, x3) = DELMIN_3_IN_AAG₁(x3)
IF_DELMIN_3_IN_1_AAG₇(x1, x2, x3, x4, x5, x6, x7) = IF_DELMIN_3_IN_1_AAG₁(x7)

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

↳ PROLOG

  ↳ UnrequestedClauseRemoverProof

    ↳ PROLOG

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

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

DELMIN_3_IN_AAG₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> IF_DELMIN_3_IN_1_AAG₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_in_aag₃(Left, Y, Left1))
DELMIN_3_IN_AAG₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> DELMIN_3_IN_AAG₃(Left, Y, Left1)

The TRS R consists of the following rules:

delmin_3_in_aag₃(tree_3₃(Y, void_0, Right), Y, Right) -> delmin_3_out_aag₃(tree_3₃(Y, void_0, Right), Y, Right)
delmin_3_in_aag₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> if_delmin_3_in_1_aag₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_in_aag₃(Left, Y, Left1))
if_delmin_3_in_1_aag₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_out_aag₃(Left, Y, Left1)) -> delmin_3_out_aag₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1))

↳ PROLOG

  ↳ UnrequestedClauseRemoverProof

    ↳ PROLOG

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ PiDP

                  ↳ UsableRulesProof

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

DELMIN_3_IN_AAG₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> DELMIN_3_IN_AAG₃(Left, Y, Left1)

The TRS R consists of the following rules:

delmin_3_in_aag₃(tree_3₃(Y, void_0, Right), Y, Right) -> delmin_3_out_aag₃(tree_3₃(Y, void_0, Right), Y, Right)
delmin_3_in_aag₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> if_delmin_3_in_1_aag₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_in_aag₃(Left, Y, Left1))
if_delmin_3_in_1_aag₇(X, Left, underscore, Y, Left1, underscore1, delmin_3_out_aag₃(Left, Y, Left1)) -> delmin_3_out_aag₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1))

The argument filtering Pi contains the following mapping:
delmin_3_in_aag₃(x1, x2, x3) = delmin_3_in_aag₁(x3)
tree_3₃(x1, x2, x3) = tree_3₁(x2)
void_0 = void_0
delmin_3_out_aag₃(x1, x2, x3) = delmin_3_out_aag₁(x1)
if_delmin_3_in_1_aag₇(x1, x2, x3, x4, x5, x6, x7) = if_delmin_3_in_1_aag₁(x7)
DELMIN_3_IN_AAG₃(x1, x2, x3) = DELMIN_3_IN_AAG₁(x3)

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

↳ PROLOG

  ↳ UnrequestedClauseRemoverProof

    ↳ PROLOG

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ PiDP

                  ↳ UsableRulesProof

                    ↳ PiDP

                      ↳ PiDPToQDPProof

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

DELMIN_3_IN_AAG₃(tree_3₃(X, Left, underscore), Y, tree_3₃(X, Left1, underscore1)) -> DELMIN_3_IN_AAG₃(Left, Y, Left1)

R is empty.
The argument filtering Pi contains the following mapping:
tree_3₃(x1, x2, x3) = tree_3₁(x2)
DELMIN_3_IN_AAG₃(x1, x2, x3) = DELMIN_3_IN_AAG₁(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

  ↳ UnrequestedClauseRemoverProof

    ↳ PROLOG

      ↳ PrologToPiTRSProof

        ↳ PiTRS

          ↳ DependencyPairsProof

            ↳ PiDP

              ↳ DependencyGraphProof

                ↳ PiDP

                  ↳ UsableRulesProof

                    ↳ PiDP

                      ↳ PiDPToQDPProof

                        ↳ QDP

                          ↳ QDPSizeChangeProof

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

DELMIN_3_IN_AAG₁(tree_3₁(Left1)) -> DELMIN_3_IN_AAG₁(Left1)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {DELMIN_3_IN_AAG₁}.
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:

DELMIN_3_IN_AAG₁(tree_3₁(Left1)) -> DELMIN_3_IN_AAG₁(Left1)
The graph contains the following edges 1 > 1