Left Termination proof of /tmp/tmpwL98wd/tree.pl

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

↳ PROLOG

  ↳ PrologToPiTRSProof

bin_tree₁(void₀).
bin_tree₁(tree₃(underscore, Left, Right)) :- bin_tree₁(Left), bin_tree₁(Right).

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

bin_tree_1_in_g₁(void_0) -> bin_tree_1_out_g₁(void_0)
bin_tree_1_in_g₁(tree_3₃(underscore, Left, Right)) -> if_bin_tree_1_in_1_g₄(underscore, Left, Right, bin_tree_1_in_g₁(Left))
if_bin_tree_1_in_1_g₄(underscore, Left, Right, bin_tree_1_out_g₁(Left)) -> if_bin_tree_1_in_2_g₄(underscore, Left, Right, bin_tree_1_in_g₁(Right))
if_bin_tree_1_in_2_g₄(underscore, Left, Right, bin_tree_1_out_g₁(Right)) -> bin_tree_1_out_g₁(tree_3₃(underscore, Left, Right))

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:

bin_tree_1_in_g₁(void_0) -> bin_tree_1_out_g₁(void_0)
bin_tree_1_in_g₁(tree_3₃(underscore, Left, Right)) -> if_bin_tree_1_in_1_g₄(underscore, Left, Right, bin_tree_1_in_g₁(Left))
if_bin_tree_1_in_1_g₄(underscore, Left, Right, bin_tree_1_out_g₁(Left)) -> if_bin_tree_1_in_2_g₄(underscore, Left, Right, bin_tree_1_in_g₁(Right))
if_bin_tree_1_in_2_g₄(underscore, Left, Right, bin_tree_1_out_g₁(Right)) -> bin_tree_1_out_g₁(tree_3₃(underscore, Left, Right))

BIN_TREE_1_IN_G₁(tree_3₃(underscore, Left, Right)) -> IF_BIN_TREE_1_IN_1_G₄(underscore, Left, Right, bin_tree_1_in_g₁(Left))
BIN_TREE_1_IN_G₁(tree_3₃(underscore, Left, Right)) -> BIN_TREE_1_IN_G₁(Left)
IF_BIN_TREE_1_IN_1_G₄(underscore, Left, Right, bin_tree_1_out_g₁(Left)) -> IF_BIN_TREE_1_IN_2_G₄(underscore, Left, Right, bin_tree_1_in_g₁(Right))
IF_BIN_TREE_1_IN_1_G₄(underscore, Left, Right, bin_tree_1_out_g₁(Left)) -> BIN_TREE_1_IN_G₁(Right)

The TRS R consists of the following rules:

bin_tree_1_in_g₁(void_0) -> bin_tree_1_out_g₁(void_0)
bin_tree_1_in_g₁(tree_3₃(underscore, Left, Right)) -> if_bin_tree_1_in_1_g₄(underscore, Left, Right, bin_tree_1_in_g₁(Left))
if_bin_tree_1_in_1_g₄(underscore, Left, Right, bin_tree_1_out_g₁(Left)) -> if_bin_tree_1_in_2_g₄(underscore, Left, Right, bin_tree_1_in_g₁(Right))
if_bin_tree_1_in_2_g₄(underscore, Left, Right, bin_tree_1_out_g₁(Right)) -> bin_tree_1_out_g₁(tree_3₃(underscore, Left, Right))

The argument filtering Pi contains the following mapping:
bin_tree_1_in_g₁(x1) = bin_tree_1_in_g₁(x1)
void_0 = void_0
tree_3₃(x1, x2, x3) = tree_3₃(x1, x2, x3)
bin_tree_1_out_g₁(x1) = bin_tree_1_out_g
if_bin_tree_1_in_1_g₄(x1, x2, x3, x4) = if_bin_tree_1_in_1_g₂(x3, x4)
if_bin_tree_1_in_2_g₄(x1, x2, x3, x4) = if_bin_tree_1_in_2_g₁(x4)
IF_BIN_TREE_1_IN_2_G₄(x1, x2, x3, x4) = IF_BIN_TREE_1_IN_2_G₁(x4)
BIN_TREE_1_IN_G₁(x1) = BIN_TREE_1_IN_G₁(x1)
IF_BIN_TREE_1_IN_1_G₄(x1, x2, x3, x4) = IF_BIN_TREE_1_IN_1_G₂(x3, x4)

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:

BIN_TREE_1_IN_G₁(tree_3₃(underscore, Left, Right)) -> IF_BIN_TREE_1_IN_1_G₄(underscore, Left, Right, bin_tree_1_in_g₁(Left))
BIN_TREE_1_IN_G₁(tree_3₃(underscore, Left, Right)) -> BIN_TREE_1_IN_G₁(Left)
IF_BIN_TREE_1_IN_1_G₄(underscore, Left, Right, bin_tree_1_out_g₁(Left)) -> IF_BIN_TREE_1_IN_2_G₄(underscore, Left, Right, bin_tree_1_in_g₁(Right))
IF_BIN_TREE_1_IN_1_G₄(underscore, Left, Right, bin_tree_1_out_g₁(Left)) -> BIN_TREE_1_IN_G₁(Right)

The TRS R consists of the following rules:

bin_tree_1_in_g₁(void_0) -> bin_tree_1_out_g₁(void_0)
bin_tree_1_in_g₁(tree_3₃(underscore, Left, Right)) -> if_bin_tree_1_in_1_g₄(underscore, Left, Right, bin_tree_1_in_g₁(Left))
if_bin_tree_1_in_1_g₄(underscore, Left, Right, bin_tree_1_out_g₁(Left)) -> if_bin_tree_1_in_2_g₄(underscore, Left, Right, bin_tree_1_in_g₁(Right))
if_bin_tree_1_in_2_g₄(underscore, Left, Right, bin_tree_1_out_g₁(Right)) -> bin_tree_1_out_g₁(tree_3₃(underscore, Left, Right))

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ PiDPToQDPProof

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

IF_BIN_TREE_1_IN_1_G₄(underscore, Left, Right, bin_tree_1_out_g₁(Left)) -> BIN_TREE_1_IN_G₁(Right)
BIN_TREE_1_IN_G₁(tree_3₃(underscore, Left, Right)) -> BIN_TREE_1_IN_G₁(Left)
BIN_TREE_1_IN_G₁(tree_3₃(underscore, Left, Right)) -> IF_BIN_TREE_1_IN_1_G₄(underscore, Left, Right, bin_tree_1_in_g₁(Left))

The TRS R consists of the following rules:

bin_tree_1_in_g₁(void_0) -> bin_tree_1_out_g₁(void_0)
bin_tree_1_in_g₁(tree_3₃(underscore, Left, Right)) -> if_bin_tree_1_in_1_g₄(underscore, Left, Right, bin_tree_1_in_g₁(Left))
if_bin_tree_1_in_1_g₄(underscore, Left, Right, bin_tree_1_out_g₁(Left)) -> if_bin_tree_1_in_2_g₄(underscore, Left, Right, bin_tree_1_in_g₁(Right))
if_bin_tree_1_in_2_g₄(underscore, Left, Right, bin_tree_1_out_g₁(Right)) -> bin_tree_1_out_g₁(tree_3₃(underscore, Left, Right))

The argument filtering Pi contains the following mapping:
bin_tree_1_in_g₁(x1) = bin_tree_1_in_g₁(x1)
void_0 = void_0
tree_3₃(x1, x2, x3) = tree_3₃(x1, x2, x3)
bin_tree_1_out_g₁(x1) = bin_tree_1_out_g
if_bin_tree_1_in_1_g₄(x1, x2, x3, x4) = if_bin_tree_1_in_1_g₂(x3, x4)
if_bin_tree_1_in_2_g₄(x1, x2, x3, x4) = if_bin_tree_1_in_2_g₁(x4)
BIN_TREE_1_IN_G₁(x1) = BIN_TREE_1_IN_G₁(x1)
IF_BIN_TREE_1_IN_1_G₄(x1, x2, x3, x4) = IF_BIN_TREE_1_IN_1_G₂(x3, x4)

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

              ↳ PiDPToQDPProof

                ↳ QDP

                  ↳ QDPSizeChangeProof

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

IF_BIN_TREE_1_IN_1_G₂(Right, bin_tree_1_out_g) -> BIN_TREE_1_IN_G₁(Right)
BIN_TREE_1_IN_G₁(tree_3₃(underscore, Left, Right)) -> BIN_TREE_1_IN_G₁(Left)
BIN_TREE_1_IN_G₁(tree_3₃(underscore, Left, Right)) -> IF_BIN_TREE_1_IN_1_G₂(Right, bin_tree_1_in_g₁(Left))

The TRS R consists of the following rules:

bin_tree_1_in_g₁(void_0) -> bin_tree_1_out_g
bin_tree_1_in_g₁(tree_3₃(underscore, Left, Right)) -> if_bin_tree_1_in_1_g₂(Right, bin_tree_1_in_g₁(Left))
if_bin_tree_1_in_1_g₂(Right, bin_tree_1_out_g) -> if_bin_tree_1_in_2_g₁(bin_tree_1_in_g₁(Right))
if_bin_tree_1_in_2_g₁(bin_tree_1_out_g) -> bin_tree_1_out_g

The set Q consists of the following terms:

bin_tree_1_in_g₁(x0)
if_bin_tree_1_in_1_g₂(x0, x1)
if_bin_tree_1_in_2_g₁(x0)

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

BIN_TREE_1_IN_G₁(tree_3₃(underscore, Left, Right)) -> IF_BIN_TREE_1_IN_1_G₂(Right, bin_tree_1_in_g₁(Left))
The graph contains the following edges 1 > 1
BIN_TREE_1_IN_G₁(tree_3₃(underscore, Left, Right)) -> BIN_TREE_1_IN_G₁(Left)
The graph contains the following edges 1 > 1
IF_BIN_TREE_1_IN_1_G₂(Right, bin_tree_1_out_g) -> BIN_TREE_1_IN_G₁(Right)
The graph contains the following edges 1 >= 1