(0) Obligation:

Clauses:

bin_tree(void) :- !.
bin_tree(T) :- ','(left(T, L), ','(right(T, R), ','(bin_tree(L), bin_tree(R)))).
left(void, void).
left(tree(X1, L, X2), L).
right(void, void).
right(tree(X3, X4, R), R).

Query: bin_tree(g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

(2) Obligation:

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

bin_treeA_in_g(void) → bin_treeA_out_g(void)
bin_treeA_in_g(tree(T19, T20, T21)) → U1_g(T19, T20, T21, pB_in_gg(T20, T21))
pB_in_gg(T20, T21) → U2_gg(T20, T21, bin_treeA_in_g(T20))
U2_gg(T20, T21, bin_treeA_out_g(T20)) → U3_gg(T20, T21, bin_treeA_in_g(T21))
U3_gg(T20, T21, bin_treeA_out_g(T21)) → pB_out_gg(T20, T21)
U1_g(T19, T20, T21, pB_out_gg(T20, T21)) → bin_treeA_out_g(tree(T19, T20, T21))

Pi is empty.

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

BIN_TREEA_IN_G(tree(T19, T20, T21)) → U1_G(T19, T20, T21, pB_in_gg(T20, T21))
BIN_TREEA_IN_G(tree(T19, T20, T21)) → PB_IN_GG(T20, T21)
PB_IN_GG(T20, T21) → U2_GG(T20, T21, bin_treeA_in_g(T20))
PB_IN_GG(T20, T21) → BIN_TREEA_IN_G(T20)
U2_GG(T20, T21, bin_treeA_out_g(T20)) → U3_GG(T20, T21, bin_treeA_in_g(T21))
U2_GG(T20, T21, bin_treeA_out_g(T20)) → BIN_TREEA_IN_G(T21)

The TRS R consists of the following rules:

bin_treeA_in_g(void) → bin_treeA_out_g(void)
bin_treeA_in_g(tree(T19, T20, T21)) → U1_g(T19, T20, T21, pB_in_gg(T20, T21))
pB_in_gg(T20, T21) → U2_gg(T20, T21, bin_treeA_in_g(T20))
U2_gg(T20, T21, bin_treeA_out_g(T20)) → U3_gg(T20, T21, bin_treeA_in_g(T21))
U3_gg(T20, T21, bin_treeA_out_g(T21)) → pB_out_gg(T20, T21)
U1_g(T19, T20, T21, pB_out_gg(T20, T21)) → bin_treeA_out_g(tree(T19, T20, T21))

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

(4) Obligation:

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

BIN_TREEA_IN_G(tree(T19, T20, T21)) → U1_G(T19, T20, T21, pB_in_gg(T20, T21))
BIN_TREEA_IN_G(tree(T19, T20, T21)) → PB_IN_GG(T20, T21)
PB_IN_GG(T20, T21) → U2_GG(T20, T21, bin_treeA_in_g(T20))
PB_IN_GG(T20, T21) → BIN_TREEA_IN_G(T20)
U2_GG(T20, T21, bin_treeA_out_g(T20)) → U3_GG(T20, T21, bin_treeA_in_g(T21))
U2_GG(T20, T21, bin_treeA_out_g(T20)) → BIN_TREEA_IN_G(T21)

The TRS R consists of the following rules:

bin_treeA_in_g(void) → bin_treeA_out_g(void)
bin_treeA_in_g(tree(T19, T20, T21)) → U1_g(T19, T20, T21, pB_in_gg(T20, T21))
pB_in_gg(T20, T21) → U2_gg(T20, T21, bin_treeA_in_g(T20))
U2_gg(T20, T21, bin_treeA_out_g(T20)) → U3_gg(T20, T21, bin_treeA_in_g(T21))
U3_gg(T20, T21, bin_treeA_out_g(T21)) → pB_out_gg(T20, T21)
U1_g(T19, T20, T21, pB_out_gg(T20, T21)) → bin_treeA_out_g(tree(T19, T20, T21))

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 2 less nodes.

(6) Obligation:

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

BIN_TREEA_IN_G(tree(T19, T20, T21)) → PB_IN_GG(T20, T21)
PB_IN_GG(T20, T21) → U2_GG(T20, T21, bin_treeA_in_g(T20))
U2_GG(T20, T21, bin_treeA_out_g(T20)) → BIN_TREEA_IN_G(T21)
PB_IN_GG(T20, T21) → BIN_TREEA_IN_G(T20)

The TRS R consists of the following rules:

bin_treeA_in_g(void) → bin_treeA_out_g(void)
bin_treeA_in_g(tree(T19, T20, T21)) → U1_g(T19, T20, T21, pB_in_gg(T20, T21))
pB_in_gg(T20, T21) → U2_gg(T20, T21, bin_treeA_in_g(T20))
U2_gg(T20, T21, bin_treeA_out_g(T20)) → U3_gg(T20, T21, bin_treeA_in_g(T21))
U3_gg(T20, T21, bin_treeA_out_g(T21)) → pB_out_gg(T20, T21)
U1_g(T19, T20, T21, pB_out_gg(T20, T21)) → bin_treeA_out_g(tree(T19, T20, T21))

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

(7) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(8) Obligation:

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

BIN_TREEA_IN_G(tree(T19, T20, T21)) → PB_IN_GG(T20, T21)
PB_IN_GG(T20, T21) → U2_GG(T20, T21, bin_treeA_in_g(T20))
U2_GG(T20, T21, bin_treeA_out_g(T20)) → BIN_TREEA_IN_G(T21)
PB_IN_GG(T20, T21) → BIN_TREEA_IN_G(T20)

The TRS R consists of the following rules:

bin_treeA_in_g(void) → bin_treeA_out_g(void)
bin_treeA_in_g(tree(T19, T20, T21)) → U1_g(T19, T20, T21, pB_in_gg(T20, T21))
pB_in_gg(T20, T21) → U2_gg(T20, T21, bin_treeA_in_g(T20))
U2_gg(T20, T21, bin_treeA_out_g(T20)) → U3_gg(T20, T21, bin_treeA_in_g(T21))
U3_gg(T20, T21, bin_treeA_out_g(T21)) → pB_out_gg(T20, T21)
U1_g(T19, T20, T21, pB_out_gg(T20, T21)) → bin_treeA_out_g(tree(T19, T20, T21))

The set Q consists of the following terms:

bin_treeA_in_g(x0)
pB_in_gg(x0, x1)
U2_gg(x0, x1, x2)
U3_gg(x0, x1, x2)
U1_g(x0, x1, x2, x3)

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

(9) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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:

  • PB_IN_GG(T20, T21) → BIN_TREEA_IN_G(T20)
    The graph contains the following edges 1 >= 1

  • PB_IN_GG(T20, T21) → U2_GG(T20, T21, bin_treeA_in_g(T20))
    The graph contains the following edges 1 >= 1, 2 >= 2

  • U2_GG(T20, T21, bin_treeA_out_g(T20)) → BIN_TREEA_IN_G(T21)
    The graph contains the following edges 2 >= 1

  • BIN_TREEA_IN_G(tree(T19, T20, T21)) → PB_IN_GG(T20, T21)
    The graph contains the following edges 1 > 1, 1 > 2

(10) YES