Left Termination of the query pattern bin_tree_in_1(g) w.r.t. the given Prolog program could not be shown:

0 Prolog
↳1 CutEliminatorProof (⇐)
↳2 Prolog
↳3 UndefinedPredicateHandlerProof (⇐)
↳4 Prolog
  ↳5 PrologToPiTRSProof (⇐)
    ↳6 PiTRS
    ↳7 DependencyPairsProof (⇔)
    ↳8 PiDP
    ↳9 DependencyGraphProof (⇔)
    ↳10 PiDP
    ↳11 PiDPToQDPProof (⇐)
    ↳12 QDP
    ↳13 UsableRulesReductionPairsProof (⇔)
    ↳14 QDP
    ↳15 Narrowing (⇐)
    ↳16 QDP
    ↳17 Narrowing (⇐)
    ↳18 QDP
    ↳19 Instantiation (⇔)
    ↳20 QDP
    ↳21 Instantiation (⇔)
    ↳22 QDP
    ↳23 Instantiation (⇔)
    ↳24 QDP
    ↳25 Instantiation (⇔)
    ↳26 QDP
    ↳27 Instantiation (⇔)
    ↳28 QDP
    ↳29 Instantiation (⇔)
    ↳30 QDP
    ↳31 Narrowing (⇐)
    ↳32 QDP
    ↳33 Rewriting (⇔)
    ↳34 QDP
    ↳35 Rewriting (⇔)
    ↳36 QDP
    ↳37 Rewriting (⇔)
    ↳38 QDP
    ↳39 NonTerminationProof (⇔)
    ↳40 FALSE
  ↳41 PrologToPiTRSProof (⇐)
    ↳42 PiTRS
    ↳43 DependencyPairsProof (⇔)
    ↳44 PiDP
    ↳45 DependencyGraphProof (⇔)
    ↳46 PiDP
    ↳47 PiDPToQDPProof (⇐)
    ↳48 QDP
    ↳49 Narrowing (⇐)
    ↳50 QDP
    ↳51 Narrowing (⇐)
    ↳52 QDP
    ↳53 Instantiation (⇔)
    ↳54 QDP
    ↳55 Instantiation (⇔)
    ↳56 QDP
    ↳57 QDPOrderProof (⇔)
    ↳58 QDP
    ↳59 DependencyGraphProof (⇔)
    ↳60 QDP
      ↳61 Instantiation (⇔)
        ↳62 QDP
      ↳63 Instantiation (⇔)
        ↳64 QDP
        ↳65 Instantiation (⇔)
        ↳66 QDP
        ↳67 Instantiation (⇔)
        ↳68 QDP
        ↳69 Narrowing (⇐)
        ↳70 QDP
        ↳71 Rewriting (⇔)
        ↳72 QDP
        ↳73 Rewriting (⇔)
        ↳74 QDP
        ↳75 Rewriting (⇔)
        ↳76 QDP
        ↳77 NonTerminationProof (⇔)
        ↳78 FALSE

(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).

Queries:

bin_tree(g).

(1) CutEliminatorProof (SOUND transformation)

Eliminated all cuts by simply ignoring them[PROLOG].

(2) Obligation:

Clauses:

bin_tree(void) :- true.
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).

Queries:

bin_tree(g).

(3) UndefinedPredicateHandlerProof (SOUND transformation)

Added facts for all undefined predicates [PROLOG].

(4) Obligation:

Clauses:

bin_tree(void) :- true.
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).
true.

Queries:

bin_tree(g).

(5) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
bin_tree_in: (b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g(void)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T, L))
left_in_ga(void, void) → left_out_ga(void, void)
left_in_ga(tree(X1, L, X2), L) → left_out_ga(tree(X1, L, X2), L)
U2_g(T, left_out_ga(T, L)) → U3_g(T, L, right_in_ga(T, R))
right_in_ga(void, void) → right_out_ga(void, void)
right_in_ga(tree(X3, X4, R), R) → right_out_ga(tree(X3, X4, R), R)
U3_g(T, L, right_out_ga(T, R)) → U4_g(T, L, R, bin_tree_in_g(L))
U4_g(T, L, R, bin_tree_out_g(L)) → U5_g(T, bin_tree_in_g(R))
U5_g(T, bin_tree_out_g(R)) → bin_tree_out_g(T)

The argument filtering Pi contains the following mapping:
bin_tree_in_g(x1)  =  bin_tree_in_g(x1)
void  =  void
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
bin_tree_out_g(x1)  =  bin_tree_out_g
U2_g(x1, x2)  =  U2_g(x1, x2)
left_in_ga(x1, x2)  =  left_in_ga(x1)
left_out_ga(x1, x2)  =  left_out_ga(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U3_g(x1, x2, x3)  =  U3_g(x2, x3)
right_in_ga(x1, x2)  =  right_in_ga(x1)
right_out_ga(x1, x2)  =  right_out_ga(x2)
U4_g(x1, x2, x3, x4)  =  U4_g(x3, x4)
U5_g(x1, x2)  =  U5_g(x2)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(6) Obligation:

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

bin_tree_in_g(void) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g(void)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T, L))
left_in_ga(void, void) → left_out_ga(void, void)
left_in_ga(tree(X1, L, X2), L) → left_out_ga(tree(X1, L, X2), L)
U2_g(T, left_out_ga(T, L)) → U3_g(T, L, right_in_ga(T, R))
right_in_ga(void, void) → right_out_ga(void, void)
right_in_ga(tree(X3, X4, R), R) → right_out_ga(tree(X3, X4, R), R)
U3_g(T, L, right_out_ga(T, R)) → U4_g(T, L, R, bin_tree_in_g(L))
U4_g(T, L, R, bin_tree_out_g(L)) → U5_g(T, bin_tree_in_g(R))
U5_g(T, bin_tree_out_g(R)) → bin_tree_out_g(T)

The argument filtering Pi contains the following mapping:
bin_tree_in_g(x1)  =  bin_tree_in_g(x1)
void  =  void
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
bin_tree_out_g(x1)  =  bin_tree_out_g
U2_g(x1, x2)  =  U2_g(x1, x2)
left_in_ga(x1, x2)  =  left_in_ga(x1)
left_out_ga(x1, x2)  =  left_out_ga(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U3_g(x1, x2, x3)  =  U3_g(x2, x3)
right_in_ga(x1, x2)  =  right_in_ga(x1)
right_out_ga(x1, x2)  =  right_out_ga(x2)
U4_g(x1, x2, x3, x4)  =  U4_g(x3, x4)
U5_g(x1, x2)  =  U5_g(x2)

(7) 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_TREE_IN_G(void) → U1_G(true_in_)
BIN_TREE_IN_G(void) → TRUE_IN_
BIN_TREE_IN_G(T) → U2_G(T, left_in_ga(T, L))
BIN_TREE_IN_G(T) → LEFT_IN_GA(T, L)
U2_G(T, left_out_ga(T, L)) → U3_G(T, L, right_in_ga(T, R))
U2_G(T, left_out_ga(T, L)) → RIGHT_IN_GA(T, R)
U3_G(T, L, right_out_ga(T, R)) → U4_G(T, L, R, bin_tree_in_g(L))
U3_G(T, L, right_out_ga(T, R)) → BIN_TREE_IN_G(L)
U4_G(T, L, R, bin_tree_out_g(L)) → U5_G(T, bin_tree_in_g(R))
U4_G(T, L, R, bin_tree_out_g(L)) → BIN_TREE_IN_G(R)

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g(void)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T, L))
left_in_ga(void, void) → left_out_ga(void, void)
left_in_ga(tree(X1, L, X2), L) → left_out_ga(tree(X1, L, X2), L)
U2_g(T, left_out_ga(T, L)) → U3_g(T, L, right_in_ga(T, R))
right_in_ga(void, void) → right_out_ga(void, void)
right_in_ga(tree(X3, X4, R), R) → right_out_ga(tree(X3, X4, R), R)
U3_g(T, L, right_out_ga(T, R)) → U4_g(T, L, R, bin_tree_in_g(L))
U4_g(T, L, R, bin_tree_out_g(L)) → U5_g(T, bin_tree_in_g(R))
U5_g(T, bin_tree_out_g(R)) → bin_tree_out_g(T)

The argument filtering Pi contains the following mapping:
bin_tree_in_g(x1)  =  bin_tree_in_g(x1)
void  =  void
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
bin_tree_out_g(x1)  =  bin_tree_out_g
U2_g(x1, x2)  =  U2_g(x1, x2)
left_in_ga(x1, x2)  =  left_in_ga(x1)
left_out_ga(x1, x2)  =  left_out_ga(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U3_g(x1, x2, x3)  =  U3_g(x2, x3)
right_in_ga(x1, x2)  =  right_in_ga(x1)
right_out_ga(x1, x2)  =  right_out_ga(x2)
U4_g(x1, x2, x3, x4)  =  U4_g(x3, x4)
U5_g(x1, x2)  =  U5_g(x2)
BIN_TREE_IN_G(x1)  =  BIN_TREE_IN_G(x1)
U1_G(x1)  =  U1_G(x1)
TRUE_IN_  =  TRUE_IN_
U2_G(x1, x2)  =  U2_G(x1, x2)
LEFT_IN_GA(x1, x2)  =  LEFT_IN_GA(x1)
U3_G(x1, x2, x3)  =  U3_G(x2, x3)
RIGHT_IN_GA(x1, x2)  =  RIGHT_IN_GA(x1)
U4_G(x1, x2, x3, x4)  =  U4_G(x3, x4)
U5_G(x1, x2)  =  U5_G(x2)

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

(8) Obligation:

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

BIN_TREE_IN_G(void) → U1_G(true_in_)
BIN_TREE_IN_G(void) → TRUE_IN_
BIN_TREE_IN_G(T) → U2_G(T, left_in_ga(T, L))
BIN_TREE_IN_G(T) → LEFT_IN_GA(T, L)
U2_G(T, left_out_ga(T, L)) → U3_G(T, L, right_in_ga(T, R))
U2_G(T, left_out_ga(T, L)) → RIGHT_IN_GA(T, R)
U3_G(T, L, right_out_ga(T, R)) → U4_G(T, L, R, bin_tree_in_g(L))
U3_G(T, L, right_out_ga(T, R)) → BIN_TREE_IN_G(L)
U4_G(T, L, R, bin_tree_out_g(L)) → U5_G(T, bin_tree_in_g(R))
U4_G(T, L, R, bin_tree_out_g(L)) → BIN_TREE_IN_G(R)

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g(void)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T, L))
left_in_ga(void, void) → left_out_ga(void, void)
left_in_ga(tree(X1, L, X2), L) → left_out_ga(tree(X1, L, X2), L)
U2_g(T, left_out_ga(T, L)) → U3_g(T, L, right_in_ga(T, R))
right_in_ga(void, void) → right_out_ga(void, void)
right_in_ga(tree(X3, X4, R), R) → right_out_ga(tree(X3, X4, R), R)
U3_g(T, L, right_out_ga(T, R)) → U4_g(T, L, R, bin_tree_in_g(L))
U4_g(T, L, R, bin_tree_out_g(L)) → U5_g(T, bin_tree_in_g(R))
U5_g(T, bin_tree_out_g(R)) → bin_tree_out_g(T)

The argument filtering Pi contains the following mapping:
bin_tree_in_g(x1)  =  bin_tree_in_g(x1)
void  =  void
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
bin_tree_out_g(x1)  =  bin_tree_out_g
U2_g(x1, x2)  =  U2_g(x1, x2)
left_in_ga(x1, x2)  =  left_in_ga(x1)
left_out_ga(x1, x2)  =  left_out_ga(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U3_g(x1, x2, x3)  =  U3_g(x2, x3)
right_in_ga(x1, x2)  =  right_in_ga(x1)
right_out_ga(x1, x2)  =  right_out_ga(x2)
U4_g(x1, x2, x3, x4)  =  U4_g(x3, x4)
U5_g(x1, x2)  =  U5_g(x2)
BIN_TREE_IN_G(x1)  =  BIN_TREE_IN_G(x1)
U1_G(x1)  =  U1_G(x1)
TRUE_IN_  =  TRUE_IN_
U2_G(x1, x2)  =  U2_G(x1, x2)
LEFT_IN_GA(x1, x2)  =  LEFT_IN_GA(x1)
U3_G(x1, x2, x3)  =  U3_G(x2, x3)
RIGHT_IN_GA(x1, x2)  =  RIGHT_IN_GA(x1)
U4_G(x1, x2, x3, x4)  =  U4_G(x3, x4)
U5_G(x1, x2)  =  U5_G(x2)

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

(9) DependencyGraphProof (EQUIVALENT transformation)

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

(10) Obligation:

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

BIN_TREE_IN_G(T) → U2_G(T, left_in_ga(T, L))
U2_G(T, left_out_ga(T, L)) → U3_G(T, L, right_in_ga(T, R))
U3_G(T, L, right_out_ga(T, R)) → U4_G(T, L, R, bin_tree_in_g(L))
U4_G(T, L, R, bin_tree_out_g(L)) → BIN_TREE_IN_G(R)
U3_G(T, L, right_out_ga(T, R)) → BIN_TREE_IN_G(L)

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g(void)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T, L))
left_in_ga(void, void) → left_out_ga(void, void)
left_in_ga(tree(X1, L, X2), L) → left_out_ga(tree(X1, L, X2), L)
U2_g(T, left_out_ga(T, L)) → U3_g(T, L, right_in_ga(T, R))
right_in_ga(void, void) → right_out_ga(void, void)
right_in_ga(tree(X3, X4, R), R) → right_out_ga(tree(X3, X4, R), R)
U3_g(T, L, right_out_ga(T, R)) → U4_g(T, L, R, bin_tree_in_g(L))
U4_g(T, L, R, bin_tree_out_g(L)) → U5_g(T, bin_tree_in_g(R))
U5_g(T, bin_tree_out_g(R)) → bin_tree_out_g(T)

The argument filtering Pi contains the following mapping:
bin_tree_in_g(x1)  =  bin_tree_in_g(x1)
void  =  void
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
bin_tree_out_g(x1)  =  bin_tree_out_g
U2_g(x1, x2)  =  U2_g(x1, x2)
left_in_ga(x1, x2)  =  left_in_ga(x1)
left_out_ga(x1, x2)  =  left_out_ga(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U3_g(x1, x2, x3)  =  U3_g(x2, x3)
right_in_ga(x1, x2)  =  right_in_ga(x1)
right_out_ga(x1, x2)  =  right_out_ga(x2)
U4_g(x1, x2, x3, x4)  =  U4_g(x3, x4)
U5_g(x1, x2)  =  U5_g(x2)
BIN_TREE_IN_G(x1)  =  BIN_TREE_IN_G(x1)
U2_G(x1, x2)  =  U2_G(x1, x2)
U3_G(x1, x2, x3)  =  U3_G(x2, x3)
U4_G(x1, x2, x3, x4)  =  U4_G(x3, x4)

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

(11) PiDPToQDPProof (SOUND transformation)

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

(12) Obligation:

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

BIN_TREE_IN_G(T) → U2_G(T, left_in_ga(T))
U2_G(T, left_out_ga(L)) → U3_G(L, right_in_ga(T))
U3_G(L, right_out_ga(R)) → U4_G(R, bin_tree_in_g(L))
U4_G(R, bin_tree_out_g) → BIN_TREE_IN_G(R)
U3_G(L, right_out_ga(R)) → BIN_TREE_IN_G(L)

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void)
left_in_ga(tree(X1, L, X2)) → left_out_ga(L)
U2_g(T, left_out_ga(L)) → U3_g(L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void)
right_in_ga(tree(X3, X4, R)) → right_out_ga(R)
U3_g(L, right_out_ga(R)) → U4_g(R, bin_tree_in_g(L))
U4_g(R, bin_tree_out_g) → U5_g(bin_tree_in_g(R))
U5_g(bin_tree_out_g) → bin_tree_out_g

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1)
U4_g(x0, x1)
U5_g(x0)

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

(13) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

No dependency pairs are removed.

The following rules are removed from R:

left_in_ga(tree(X1, L, X2)) → left_out_ga(L)
right_in_ga(tree(X3, X4, R)) → right_out_ga(R)
Used ordering: POLO with Polynomial interpretation [POLO]:

POL(BIN_TREE_IN_G(x1)) = 2·x1   
POL(U1_g(x1)) = 2·x1   
POL(U2_G(x1, x2)) = x1 + x2   
POL(U2_g(x1, x2)) = x1 + x2   
POL(U3_G(x1, x2)) = 2·x1 + x2   
POL(U3_g(x1, x2)) = 2·x1 + x2   
POL(U4_G(x1, x2)) = 2·x1 + x2   
POL(U4_g(x1, x2)) = 2·x1 + x2   
POL(U5_g(x1)) = x1   
POL(bin_tree_in_g(x1)) = 2·x1   
POL(bin_tree_out_g) = 0   
POL(left_in_ga(x1)) = x1   
POL(left_out_ga(x1)) = 2·x1   
POL(right_in_ga(x1)) = x1   
POL(right_out_ga(x1)) = 2·x1   
POL(tree(x1, x2, x3)) = x1 + 2·x2 + 2·x3   
POL(true_in_) = 0   
POL(true_out_) = 0   
POL(void) = 0   

(14) Obligation:

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

BIN_TREE_IN_G(T) → U2_G(T, left_in_ga(T))
U2_G(T, left_out_ga(L)) → U3_G(L, right_in_ga(T))
U3_G(L, right_out_ga(R)) → U4_G(R, bin_tree_in_g(L))
U4_G(R, bin_tree_out_g) → BIN_TREE_IN_G(R)
U3_G(L, right_out_ga(R)) → BIN_TREE_IN_G(L)

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void)
U2_g(T, left_out_ga(L)) → U3_g(L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void)
U3_g(L, right_out_ga(R)) → U4_g(R, bin_tree_in_g(L))
U4_g(R, bin_tree_out_g) → U5_g(bin_tree_in_g(R))
U5_g(bin_tree_out_g) → bin_tree_out_g
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1)
U4_g(x0, x1)
U5_g(x0)

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

(15) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule BIN_TREE_IN_G(T) → U2_G(T, left_in_ga(T)) at position [1] we obtained the following new rules [LPAR04]:

BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void))

(16) Obligation:

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

U2_G(T, left_out_ga(L)) → U3_G(L, right_in_ga(T))
U3_G(L, right_out_ga(R)) → U4_G(R, bin_tree_in_g(L))
U4_G(R, bin_tree_out_g) → BIN_TREE_IN_G(R)
U3_G(L, right_out_ga(R)) → BIN_TREE_IN_G(L)
BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void))

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void)
U2_g(T, left_out_ga(L)) → U3_g(L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void)
U3_g(L, right_out_ga(R)) → U4_g(R, bin_tree_in_g(L))
U4_g(R, bin_tree_out_g) → U5_g(bin_tree_in_g(R))
U5_g(bin_tree_out_g) → bin_tree_out_g
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1)
U4_g(x0, x1)
U5_g(x0)

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

(17) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U2_G(T, left_out_ga(L)) → U3_G(L, right_in_ga(T)) at position [1] we obtained the following new rules [LPAR04]:

U2_G(void, left_out_ga(y1)) → U3_G(y1, right_out_ga(void))

(18) Obligation:

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

U3_G(L, right_out_ga(R)) → U4_G(R, bin_tree_in_g(L))
U4_G(R, bin_tree_out_g) → BIN_TREE_IN_G(R)
U3_G(L, right_out_ga(R)) → BIN_TREE_IN_G(L)
BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void))
U2_G(void, left_out_ga(y1)) → U3_G(y1, right_out_ga(void))

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void)
U2_g(T, left_out_ga(L)) → U3_g(L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void)
U3_g(L, right_out_ga(R)) → U4_g(R, bin_tree_in_g(L))
U4_g(R, bin_tree_out_g) → U5_g(bin_tree_in_g(R))
U5_g(bin_tree_out_g) → bin_tree_out_g
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1)
U4_g(x0, x1)
U5_g(x0)

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

(19) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U3_G(L, right_out_ga(R)) → U4_G(R, bin_tree_in_g(L)) we obtained the following new rules [LPAR04]:

U3_G(z0, right_out_ga(void)) → U4_G(void, bin_tree_in_g(z0))

(20) Obligation:

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

U4_G(R, bin_tree_out_g) → BIN_TREE_IN_G(R)
U3_G(L, right_out_ga(R)) → BIN_TREE_IN_G(L)
BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void))
U2_G(void, left_out_ga(y1)) → U3_G(y1, right_out_ga(void))
U3_G(z0, right_out_ga(void)) → U4_G(void, bin_tree_in_g(z0))

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void)
U2_g(T, left_out_ga(L)) → U3_g(L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void)
U3_g(L, right_out_ga(R)) → U4_g(R, bin_tree_in_g(L))
U4_g(R, bin_tree_out_g) → U5_g(bin_tree_in_g(R))
U5_g(bin_tree_out_g) → bin_tree_out_g
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1)
U4_g(x0, x1)
U5_g(x0)

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

(21) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U4_G(R, bin_tree_out_g) → BIN_TREE_IN_G(R) we obtained the following new rules [LPAR04]:

U4_G(void, bin_tree_out_g) → BIN_TREE_IN_G(void)

(22) Obligation:

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

U3_G(L, right_out_ga(R)) → BIN_TREE_IN_G(L)
BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void))
U2_G(void, left_out_ga(y1)) → U3_G(y1, right_out_ga(void))
U3_G(z0, right_out_ga(void)) → U4_G(void, bin_tree_in_g(z0))
U4_G(void, bin_tree_out_g) → BIN_TREE_IN_G(void)

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void)
U2_g(T, left_out_ga(L)) → U3_g(L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void)
U3_g(L, right_out_ga(R)) → U4_g(R, bin_tree_in_g(L))
U4_g(R, bin_tree_out_g) → U5_g(bin_tree_in_g(R))
U5_g(bin_tree_out_g) → bin_tree_out_g
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1)
U4_g(x0, x1)
U5_g(x0)

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

(23) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U3_G(L, right_out_ga(R)) → BIN_TREE_IN_G(L) we obtained the following new rules [LPAR04]:

U3_G(z0, right_out_ga(void)) → BIN_TREE_IN_G(z0)

(24) Obligation:

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

BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void))
U2_G(void, left_out_ga(y1)) → U3_G(y1, right_out_ga(void))
U3_G(z0, right_out_ga(void)) → U4_G(void, bin_tree_in_g(z0))
U4_G(void, bin_tree_out_g) → BIN_TREE_IN_G(void)
U3_G(z0, right_out_ga(void)) → BIN_TREE_IN_G(z0)

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void)
U2_g(T, left_out_ga(L)) → U3_g(L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void)
U3_g(L, right_out_ga(R)) → U4_g(R, bin_tree_in_g(L))
U4_g(R, bin_tree_out_g) → U5_g(bin_tree_in_g(R))
U5_g(bin_tree_out_g) → bin_tree_out_g
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1)
U4_g(x0, x1)
U5_g(x0)

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

(25) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U2_G(void, left_out_ga(y1)) → U3_G(y1, right_out_ga(void)) we obtained the following new rules [LPAR04]:

U2_G(void, left_out_ga(void)) → U3_G(void, right_out_ga(void))

(26) Obligation:

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

BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void))
U3_G(z0, right_out_ga(void)) → U4_G(void, bin_tree_in_g(z0))
U4_G(void, bin_tree_out_g) → BIN_TREE_IN_G(void)
U3_G(z0, right_out_ga(void)) → BIN_TREE_IN_G(z0)
U2_G(void, left_out_ga(void)) → U3_G(void, right_out_ga(void))

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void)
U2_g(T, left_out_ga(L)) → U3_g(L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void)
U3_g(L, right_out_ga(R)) → U4_g(R, bin_tree_in_g(L))
U4_g(R, bin_tree_out_g) → U5_g(bin_tree_in_g(R))
U5_g(bin_tree_out_g) → bin_tree_out_g
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1)
U4_g(x0, x1)
U5_g(x0)

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

(27) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U3_G(z0, right_out_ga(void)) → U4_G(void, bin_tree_in_g(z0)) we obtained the following new rules [LPAR04]:

U3_G(void, right_out_ga(void)) → U4_G(void, bin_tree_in_g(void))

(28) Obligation:

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

BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void))
U4_G(void, bin_tree_out_g) → BIN_TREE_IN_G(void)
U3_G(z0, right_out_ga(void)) → BIN_TREE_IN_G(z0)
U2_G(void, left_out_ga(void)) → U3_G(void, right_out_ga(void))
U3_G(void, right_out_ga(void)) → U4_G(void, bin_tree_in_g(void))

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void)
U2_g(T, left_out_ga(L)) → U3_g(L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void)
U3_g(L, right_out_ga(R)) → U4_g(R, bin_tree_in_g(L))
U4_g(R, bin_tree_out_g) → U5_g(bin_tree_in_g(R))
U5_g(bin_tree_out_g) → bin_tree_out_g
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1)
U4_g(x0, x1)
U5_g(x0)

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

(29) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U3_G(z0, right_out_ga(void)) → BIN_TREE_IN_G(z0) we obtained the following new rules [LPAR04]:

U3_G(void, right_out_ga(void)) → BIN_TREE_IN_G(void)

(30) Obligation:

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

BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void))
U4_G(void, bin_tree_out_g) → BIN_TREE_IN_G(void)
U2_G(void, left_out_ga(void)) → U3_G(void, right_out_ga(void))
U3_G(void, right_out_ga(void)) → U4_G(void, bin_tree_in_g(void))
U3_G(void, right_out_ga(void)) → BIN_TREE_IN_G(void)

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void)
U2_g(T, left_out_ga(L)) → U3_g(L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void)
U3_g(L, right_out_ga(R)) → U4_g(R, bin_tree_in_g(L))
U4_g(R, bin_tree_out_g) → U5_g(bin_tree_in_g(R))
U5_g(bin_tree_out_g) → bin_tree_out_g
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1)
U4_g(x0, x1)
U5_g(x0)

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

(31) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U3_G(void, right_out_ga(void)) → U4_G(void, bin_tree_in_g(void)) at position [1] we obtained the following new rules [LPAR04]:

U3_G(void, right_out_ga(void)) → U4_G(void, U1_g(true_in_))
U3_G(void, right_out_ga(void)) → U4_G(void, U2_g(void, left_in_ga(void)))

(32) Obligation:

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

BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void))
U4_G(void, bin_tree_out_g) → BIN_TREE_IN_G(void)
U2_G(void, left_out_ga(void)) → U3_G(void, right_out_ga(void))
U3_G(void, right_out_ga(void)) → BIN_TREE_IN_G(void)
U3_G(void, right_out_ga(void)) → U4_G(void, U1_g(true_in_))
U3_G(void, right_out_ga(void)) → U4_G(void, U2_g(void, left_in_ga(void)))

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void)
U2_g(T, left_out_ga(L)) → U3_g(L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void)
U3_g(L, right_out_ga(R)) → U4_g(R, bin_tree_in_g(L))
U4_g(R, bin_tree_out_g) → U5_g(bin_tree_in_g(R))
U5_g(bin_tree_out_g) → bin_tree_out_g
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1)
U4_g(x0, x1)
U5_g(x0)

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

(33) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U3_G(void, right_out_ga(void)) → U4_G(void, U1_g(true_in_)) at position [1,0] we obtained the following new rules [LPAR04]:

U3_G(void, right_out_ga(void)) → U4_G(void, U1_g(true_out_))

(34) Obligation:

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

BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void))
U4_G(void, bin_tree_out_g) → BIN_TREE_IN_G(void)
U2_G(void, left_out_ga(void)) → U3_G(void, right_out_ga(void))
U3_G(void, right_out_ga(void)) → BIN_TREE_IN_G(void)
U3_G(void, right_out_ga(void)) → U4_G(void, U2_g(void, left_in_ga(void)))
U3_G(void, right_out_ga(void)) → U4_G(void, U1_g(true_out_))

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void)
U2_g(T, left_out_ga(L)) → U3_g(L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void)
U3_g(L, right_out_ga(R)) → U4_g(R, bin_tree_in_g(L))
U4_g(R, bin_tree_out_g) → U5_g(bin_tree_in_g(R))
U5_g(bin_tree_out_g) → bin_tree_out_g
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1)
U4_g(x0, x1)
U5_g(x0)

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

(35) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U3_G(void, right_out_ga(void)) → U4_G(void, U2_g(void, left_in_ga(void))) at position [1,1] we obtained the following new rules [LPAR04]:

U3_G(void, right_out_ga(void)) → U4_G(void, U2_g(void, left_out_ga(void)))

(36) Obligation:

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

BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void))
U4_G(void, bin_tree_out_g) → BIN_TREE_IN_G(void)
U2_G(void, left_out_ga(void)) → U3_G(void, right_out_ga(void))
U3_G(void, right_out_ga(void)) → BIN_TREE_IN_G(void)
U3_G(void, right_out_ga(void)) → U4_G(void, U1_g(true_out_))
U3_G(void, right_out_ga(void)) → U4_G(void, U2_g(void, left_out_ga(void)))

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void)
U2_g(T, left_out_ga(L)) → U3_g(L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void)
U3_g(L, right_out_ga(R)) → U4_g(R, bin_tree_in_g(L))
U4_g(R, bin_tree_out_g) → U5_g(bin_tree_in_g(R))
U5_g(bin_tree_out_g) → bin_tree_out_g
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1)
U4_g(x0, x1)
U5_g(x0)

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

(37) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U3_G(void, right_out_ga(void)) → U4_G(void, U1_g(true_out_)) at position [1] we obtained the following new rules [LPAR04]:

U3_G(void, right_out_ga(void)) → U4_G(void, bin_tree_out_g)

(38) Obligation:

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

BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void))
U4_G(void, bin_tree_out_g) → BIN_TREE_IN_G(void)
U2_G(void, left_out_ga(void)) → U3_G(void, right_out_ga(void))
U3_G(void, right_out_ga(void)) → BIN_TREE_IN_G(void)
U3_G(void, right_out_ga(void)) → U4_G(void, U2_g(void, left_out_ga(void)))
U3_G(void, right_out_ga(void)) → U4_G(void, bin_tree_out_g)

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void)
U2_g(T, left_out_ga(L)) → U3_g(L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void)
U3_g(L, right_out_ga(R)) → U4_g(R, bin_tree_in_g(L))
U4_g(R, bin_tree_out_g) → U5_g(bin_tree_in_g(R))
U5_g(bin_tree_out_g) → bin_tree_out_g
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1)
U4_g(x0, x1)
U5_g(x0)

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

(39) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = U2_G(void, left_out_ga(void)) evaluates to t =U2_G(void, left_out_ga(void))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Semiunifier: [ ]
  • Matcher: [ ]



Rewriting sequence

U2_G(void, left_out_ga(void)) → U3_G(void, right_out_ga(void))
with rule U2_G(void, left_out_ga(void)) → U3_G(void, right_out_ga(void)) at position [] and matcher [ ]

U3_G(void, right_out_ga(void)) → BIN_TREE_IN_G(void)
with rule U3_G(void, right_out_ga(void)) → BIN_TREE_IN_G(void) at position [] and matcher [ ]

BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void))
with rule BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void))

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.



(40) FALSE

(41) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
bin_tree_in: (b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g(void)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T, L))
left_in_ga(void, void) → left_out_ga(void, void)
left_in_ga(tree(X1, L, X2), L) → left_out_ga(tree(X1, L, X2), L)
U2_g(T, left_out_ga(T, L)) → U3_g(T, L, right_in_ga(T, R))
right_in_ga(void, void) → right_out_ga(void, void)
right_in_ga(tree(X3, X4, R), R) → right_out_ga(tree(X3, X4, R), R)
U3_g(T, L, right_out_ga(T, R)) → U4_g(T, L, R, bin_tree_in_g(L))
U4_g(T, L, R, bin_tree_out_g(L)) → U5_g(T, bin_tree_in_g(R))
U5_g(T, bin_tree_out_g(R)) → bin_tree_out_g(T)

The argument filtering Pi contains the following mapping:
bin_tree_in_g(x1)  =  bin_tree_in_g(x1)
void  =  void
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
bin_tree_out_g(x1)  =  bin_tree_out_g(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
left_in_ga(x1, x2)  =  left_in_ga(x1)
left_out_ga(x1, x2)  =  left_out_ga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U3_g(x1, x2, x3)  =  U3_g(x1, x2, x3)
right_in_ga(x1, x2)  =  right_in_ga(x1)
right_out_ga(x1, x2)  =  right_out_ga(x1, x2)
U4_g(x1, x2, x3, x4)  =  U4_g(x1, x3, x4)
U5_g(x1, x2)  =  U5_g(x1, x2)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(42) Obligation:

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

bin_tree_in_g(void) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g(void)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T, L))
left_in_ga(void, void) → left_out_ga(void, void)
left_in_ga(tree(X1, L, X2), L) → left_out_ga(tree(X1, L, X2), L)
U2_g(T, left_out_ga(T, L)) → U3_g(T, L, right_in_ga(T, R))
right_in_ga(void, void) → right_out_ga(void, void)
right_in_ga(tree(X3, X4, R), R) → right_out_ga(tree(X3, X4, R), R)
U3_g(T, L, right_out_ga(T, R)) → U4_g(T, L, R, bin_tree_in_g(L))
U4_g(T, L, R, bin_tree_out_g(L)) → U5_g(T, bin_tree_in_g(R))
U5_g(T, bin_tree_out_g(R)) → bin_tree_out_g(T)

The argument filtering Pi contains the following mapping:
bin_tree_in_g(x1)  =  bin_tree_in_g(x1)
void  =  void
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
bin_tree_out_g(x1)  =  bin_tree_out_g(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
left_in_ga(x1, x2)  =  left_in_ga(x1)
left_out_ga(x1, x2)  =  left_out_ga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U3_g(x1, x2, x3)  =  U3_g(x1, x2, x3)
right_in_ga(x1, x2)  =  right_in_ga(x1)
right_out_ga(x1, x2)  =  right_out_ga(x1, x2)
U4_g(x1, x2, x3, x4)  =  U4_g(x1, x3, x4)
U5_g(x1, x2)  =  U5_g(x1, x2)

(43) 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_TREE_IN_G(void) → U1_G(true_in_)
BIN_TREE_IN_G(void) → TRUE_IN_
BIN_TREE_IN_G(T) → U2_G(T, left_in_ga(T, L))
BIN_TREE_IN_G(T) → LEFT_IN_GA(T, L)
U2_G(T, left_out_ga(T, L)) → U3_G(T, L, right_in_ga(T, R))
U2_G(T, left_out_ga(T, L)) → RIGHT_IN_GA(T, R)
U3_G(T, L, right_out_ga(T, R)) → U4_G(T, L, R, bin_tree_in_g(L))
U3_G(T, L, right_out_ga(T, R)) → BIN_TREE_IN_G(L)
U4_G(T, L, R, bin_tree_out_g(L)) → U5_G(T, bin_tree_in_g(R))
U4_G(T, L, R, bin_tree_out_g(L)) → BIN_TREE_IN_G(R)

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g(void)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T, L))
left_in_ga(void, void) → left_out_ga(void, void)
left_in_ga(tree(X1, L, X2), L) → left_out_ga(tree(X1, L, X2), L)
U2_g(T, left_out_ga(T, L)) → U3_g(T, L, right_in_ga(T, R))
right_in_ga(void, void) → right_out_ga(void, void)
right_in_ga(tree(X3, X4, R), R) → right_out_ga(tree(X3, X4, R), R)
U3_g(T, L, right_out_ga(T, R)) → U4_g(T, L, R, bin_tree_in_g(L))
U4_g(T, L, R, bin_tree_out_g(L)) → U5_g(T, bin_tree_in_g(R))
U5_g(T, bin_tree_out_g(R)) → bin_tree_out_g(T)

The argument filtering Pi contains the following mapping:
bin_tree_in_g(x1)  =  bin_tree_in_g(x1)
void  =  void
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
bin_tree_out_g(x1)  =  bin_tree_out_g(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
left_in_ga(x1, x2)  =  left_in_ga(x1)
left_out_ga(x1, x2)  =  left_out_ga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U3_g(x1, x2, x3)  =  U3_g(x1, x2, x3)
right_in_ga(x1, x2)  =  right_in_ga(x1)
right_out_ga(x1, x2)  =  right_out_ga(x1, x2)
U4_g(x1, x2, x3, x4)  =  U4_g(x1, x3, x4)
U5_g(x1, x2)  =  U5_g(x1, x2)
BIN_TREE_IN_G(x1)  =  BIN_TREE_IN_G(x1)
U1_G(x1)  =  U1_G(x1)
TRUE_IN_  =  TRUE_IN_
U2_G(x1, x2)  =  U2_G(x1, x2)
LEFT_IN_GA(x1, x2)  =  LEFT_IN_GA(x1)
U3_G(x1, x2, x3)  =  U3_G(x1, x2, x3)
RIGHT_IN_GA(x1, x2)  =  RIGHT_IN_GA(x1)
U4_G(x1, x2, x3, x4)  =  U4_G(x1, x3, x4)
U5_G(x1, x2)  =  U5_G(x1, x2)

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

(44) Obligation:

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

BIN_TREE_IN_G(void) → U1_G(true_in_)
BIN_TREE_IN_G(void) → TRUE_IN_
BIN_TREE_IN_G(T) → U2_G(T, left_in_ga(T, L))
BIN_TREE_IN_G(T) → LEFT_IN_GA(T, L)
U2_G(T, left_out_ga(T, L)) → U3_G(T, L, right_in_ga(T, R))
U2_G(T, left_out_ga(T, L)) → RIGHT_IN_GA(T, R)
U3_G(T, L, right_out_ga(T, R)) → U4_G(T, L, R, bin_tree_in_g(L))
U3_G(T, L, right_out_ga(T, R)) → BIN_TREE_IN_G(L)
U4_G(T, L, R, bin_tree_out_g(L)) → U5_G(T, bin_tree_in_g(R))
U4_G(T, L, R, bin_tree_out_g(L)) → BIN_TREE_IN_G(R)

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g(void)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T, L))
left_in_ga(void, void) → left_out_ga(void, void)
left_in_ga(tree(X1, L, X2), L) → left_out_ga(tree(X1, L, X2), L)
U2_g(T, left_out_ga(T, L)) → U3_g(T, L, right_in_ga(T, R))
right_in_ga(void, void) → right_out_ga(void, void)
right_in_ga(tree(X3, X4, R), R) → right_out_ga(tree(X3, X4, R), R)
U3_g(T, L, right_out_ga(T, R)) → U4_g(T, L, R, bin_tree_in_g(L))
U4_g(T, L, R, bin_tree_out_g(L)) → U5_g(T, bin_tree_in_g(R))
U5_g(T, bin_tree_out_g(R)) → bin_tree_out_g(T)

The argument filtering Pi contains the following mapping:
bin_tree_in_g(x1)  =  bin_tree_in_g(x1)
void  =  void
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
bin_tree_out_g(x1)  =  bin_tree_out_g(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
left_in_ga(x1, x2)  =  left_in_ga(x1)
left_out_ga(x1, x2)  =  left_out_ga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U3_g(x1, x2, x3)  =  U3_g(x1, x2, x3)
right_in_ga(x1, x2)  =  right_in_ga(x1)
right_out_ga(x1, x2)  =  right_out_ga(x1, x2)
U4_g(x1, x2, x3, x4)  =  U4_g(x1, x3, x4)
U5_g(x1, x2)  =  U5_g(x1, x2)
BIN_TREE_IN_G(x1)  =  BIN_TREE_IN_G(x1)
U1_G(x1)  =  U1_G(x1)
TRUE_IN_  =  TRUE_IN_
U2_G(x1, x2)  =  U2_G(x1, x2)
LEFT_IN_GA(x1, x2)  =  LEFT_IN_GA(x1)
U3_G(x1, x2, x3)  =  U3_G(x1, x2, x3)
RIGHT_IN_GA(x1, x2)  =  RIGHT_IN_GA(x1)
U4_G(x1, x2, x3, x4)  =  U4_G(x1, x3, x4)
U5_G(x1, x2)  =  U5_G(x1, x2)

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

(45) DependencyGraphProof (EQUIVALENT transformation)

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

(46) Obligation:

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

BIN_TREE_IN_G(T) → U2_G(T, left_in_ga(T, L))
U2_G(T, left_out_ga(T, L)) → U3_G(T, L, right_in_ga(T, R))
U3_G(T, L, right_out_ga(T, R)) → U4_G(T, L, R, bin_tree_in_g(L))
U4_G(T, L, R, bin_tree_out_g(L)) → BIN_TREE_IN_G(R)
U3_G(T, L, right_out_ga(T, R)) → BIN_TREE_IN_G(L)

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g(void)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T, L))
left_in_ga(void, void) → left_out_ga(void, void)
left_in_ga(tree(X1, L, X2), L) → left_out_ga(tree(X1, L, X2), L)
U2_g(T, left_out_ga(T, L)) → U3_g(T, L, right_in_ga(T, R))
right_in_ga(void, void) → right_out_ga(void, void)
right_in_ga(tree(X3, X4, R), R) → right_out_ga(tree(X3, X4, R), R)
U3_g(T, L, right_out_ga(T, R)) → U4_g(T, L, R, bin_tree_in_g(L))
U4_g(T, L, R, bin_tree_out_g(L)) → U5_g(T, bin_tree_in_g(R))
U5_g(T, bin_tree_out_g(R)) → bin_tree_out_g(T)

The argument filtering Pi contains the following mapping:
bin_tree_in_g(x1)  =  bin_tree_in_g(x1)
void  =  void
U1_g(x1)  =  U1_g(x1)
true_in_  =  true_in_
true_out_  =  true_out_
bin_tree_out_g(x1)  =  bin_tree_out_g(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
left_in_ga(x1, x2)  =  left_in_ga(x1)
left_out_ga(x1, x2)  =  left_out_ga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U3_g(x1, x2, x3)  =  U3_g(x1, x2, x3)
right_in_ga(x1, x2)  =  right_in_ga(x1)
right_out_ga(x1, x2)  =  right_out_ga(x1, x2)
U4_g(x1, x2, x3, x4)  =  U4_g(x1, x3, x4)
U5_g(x1, x2)  =  U5_g(x1, x2)
BIN_TREE_IN_G(x1)  =  BIN_TREE_IN_G(x1)
U2_G(x1, x2)  =  U2_G(x1, x2)
U3_G(x1, x2, x3)  =  U3_G(x1, x2, x3)
U4_G(x1, x2, x3, x4)  =  U4_G(x1, x3, x4)

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

(47) PiDPToQDPProof (SOUND transformation)

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

(48) Obligation:

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

BIN_TREE_IN_G(T) → U2_G(T, left_in_ga(T))
U2_G(T, left_out_ga(T, L)) → U3_G(T, L, right_in_ga(T))
U3_G(T, L, right_out_ga(T, R)) → U4_G(T, R, bin_tree_in_g(L))
U4_G(T, R, bin_tree_out_g(L)) → BIN_TREE_IN_G(R)
U3_G(T, L, right_out_ga(T, R)) → BIN_TREE_IN_G(L)

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g(void)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void, void)
left_in_ga(tree(X1, L, X2)) → left_out_ga(tree(X1, L, X2), L)
U2_g(T, left_out_ga(T, L)) → U3_g(T, L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void, void)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
U3_g(T, L, right_out_ga(T, R)) → U4_g(T, R, bin_tree_in_g(L))
U4_g(T, R, bin_tree_out_g(L)) → U5_g(T, bin_tree_in_g(R))
U5_g(T, bin_tree_out_g(R)) → bin_tree_out_g(T)

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1, x2)
U4_g(x0, x1, x2)
U5_g(x0, x1)

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

(49) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule BIN_TREE_IN_G(T) → U2_G(T, left_in_ga(T)) at position [1] we obtained the following new rules [LPAR04]:

BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void, void))
BIN_TREE_IN_G(tree(x0, x1, x2)) → U2_G(tree(x0, x1, x2), left_out_ga(tree(x0, x1, x2), x1))

(50) Obligation:

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

U2_G(T, left_out_ga(T, L)) → U3_G(T, L, right_in_ga(T))
U3_G(T, L, right_out_ga(T, R)) → U4_G(T, R, bin_tree_in_g(L))
U4_G(T, R, bin_tree_out_g(L)) → BIN_TREE_IN_G(R)
U3_G(T, L, right_out_ga(T, R)) → BIN_TREE_IN_G(L)
BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void, void))
BIN_TREE_IN_G(tree(x0, x1, x2)) → U2_G(tree(x0, x1, x2), left_out_ga(tree(x0, x1, x2), x1))

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g(void)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void, void)
left_in_ga(tree(X1, L, X2)) → left_out_ga(tree(X1, L, X2), L)
U2_g(T, left_out_ga(T, L)) → U3_g(T, L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void, void)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
U3_g(T, L, right_out_ga(T, R)) → U4_g(T, R, bin_tree_in_g(L))
U4_g(T, R, bin_tree_out_g(L)) → U5_g(T, bin_tree_in_g(R))
U5_g(T, bin_tree_out_g(R)) → bin_tree_out_g(T)

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1, x2)
U4_g(x0, x1, x2)
U5_g(x0, x1)

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

(51) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U2_G(T, left_out_ga(T, L)) → U3_G(T, L, right_in_ga(T)) at position [2] we obtained the following new rules [LPAR04]:

U2_G(void, left_out_ga(void, y1)) → U3_G(void, y1, right_out_ga(void, void))
U2_G(tree(x0, x1, x2), left_out_ga(tree(x0, x1, x2), y1)) → U3_G(tree(x0, x1, x2), y1, right_out_ga(tree(x0, x1, x2), x2))

(52) Obligation:

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

U3_G(T, L, right_out_ga(T, R)) → U4_G(T, R, bin_tree_in_g(L))
U4_G(T, R, bin_tree_out_g(L)) → BIN_TREE_IN_G(R)
U3_G(T, L, right_out_ga(T, R)) → BIN_TREE_IN_G(L)
BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void, void))
BIN_TREE_IN_G(tree(x0, x1, x2)) → U2_G(tree(x0, x1, x2), left_out_ga(tree(x0, x1, x2), x1))
U2_G(void, left_out_ga(void, y1)) → U3_G(void, y1, right_out_ga(void, void))
U2_G(tree(x0, x1, x2), left_out_ga(tree(x0, x1, x2), y1)) → U3_G(tree(x0, x1, x2), y1, right_out_ga(tree(x0, x1, x2), x2))

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g(void)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void, void)
left_in_ga(tree(X1, L, X2)) → left_out_ga(tree(X1, L, X2), L)
U2_g(T, left_out_ga(T, L)) → U3_g(T, L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void, void)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
U3_g(T, L, right_out_ga(T, R)) → U4_g(T, R, bin_tree_in_g(L))
U4_g(T, R, bin_tree_out_g(L)) → U5_g(T, bin_tree_in_g(R))
U5_g(T, bin_tree_out_g(R)) → bin_tree_out_g(T)

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1, x2)
U4_g(x0, x1, x2)
U5_g(x0, x1)

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

(53) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U2_G(void, left_out_ga(void, y1)) → U3_G(void, y1, right_out_ga(void, void)) we obtained the following new rules [LPAR04]:

U2_G(void, left_out_ga(void, void)) → U3_G(void, void, right_out_ga(void, void))

(54) Obligation:

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

U3_G(T, L, right_out_ga(T, R)) → U4_G(T, R, bin_tree_in_g(L))
U4_G(T, R, bin_tree_out_g(L)) → BIN_TREE_IN_G(R)
U3_G(T, L, right_out_ga(T, R)) → BIN_TREE_IN_G(L)
BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void, void))
BIN_TREE_IN_G(tree(x0, x1, x2)) → U2_G(tree(x0, x1, x2), left_out_ga(tree(x0, x1, x2), x1))
U2_G(tree(x0, x1, x2), left_out_ga(tree(x0, x1, x2), y1)) → U3_G(tree(x0, x1, x2), y1, right_out_ga(tree(x0, x1, x2), x2))
U2_G(void, left_out_ga(void, void)) → U3_G(void, void, right_out_ga(void, void))

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g(void)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void, void)
left_in_ga(tree(X1, L, X2)) → left_out_ga(tree(X1, L, X2), L)
U2_g(T, left_out_ga(T, L)) → U3_g(T, L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void, void)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
U3_g(T, L, right_out_ga(T, R)) → U4_g(T, R, bin_tree_in_g(L))
U4_g(T, R, bin_tree_out_g(L)) → U5_g(T, bin_tree_in_g(R))
U5_g(T, bin_tree_out_g(R)) → bin_tree_out_g(T)

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1, x2)
U4_g(x0, x1, x2)
U5_g(x0, x1)

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

(55) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U2_G(tree(x0, x1, x2), left_out_ga(tree(x0, x1, x2), y1)) → U3_G(tree(x0, x1, x2), y1, right_out_ga(tree(x0, x1, x2), x2)) we obtained the following new rules [LPAR04]:

U2_G(tree(z0, z1, z2), left_out_ga(tree(z0, z1, z2), z1)) → U3_G(tree(z0, z1, z2), z1, right_out_ga(tree(z0, z1, z2), z2))

(56) Obligation:

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

U3_G(T, L, right_out_ga(T, R)) → U4_G(T, R, bin_tree_in_g(L))
U4_G(T, R, bin_tree_out_g(L)) → BIN_TREE_IN_G(R)
U3_G(T, L, right_out_ga(T, R)) → BIN_TREE_IN_G(L)
BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void, void))
BIN_TREE_IN_G(tree(x0, x1, x2)) → U2_G(tree(x0, x1, x2), left_out_ga(tree(x0, x1, x2), x1))
U2_G(void, left_out_ga(void, void)) → U3_G(void, void, right_out_ga(void, void))
U2_G(tree(z0, z1, z2), left_out_ga(tree(z0, z1, z2), z1)) → U3_G(tree(z0, z1, z2), z1, right_out_ga(tree(z0, z1, z2), z2))

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g(void)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void, void)
left_in_ga(tree(X1, L, X2)) → left_out_ga(tree(X1, L, X2), L)
U2_g(T, left_out_ga(T, L)) → U3_g(T, L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void, void)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
U3_g(T, L, right_out_ga(T, R)) → U4_g(T, R, bin_tree_in_g(L))
U4_g(T, R, bin_tree_out_g(L)) → U5_g(T, bin_tree_in_g(R))
U5_g(T, bin_tree_out_g(R)) → bin_tree_out_g(T)

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1, x2)
U4_g(x0, x1, x2)
U5_g(x0, x1)

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

(57) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


U2_G(tree(z0, z1, z2), left_out_ga(tree(z0, z1, z2), z1)) → U3_G(tree(z0, z1, z2), z1, right_out_ga(tree(z0, z1, z2), z2))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(BIN_TREE_IN_G(x1)) = x1   
POL(U1_g(x1)) = 0   
POL(U2_G(x1, x2)) = x1   
POL(U2_g(x1, x2)) = 0   
POL(U3_G(x1, x2, x3)) = x2 + x3   
POL(U3_g(x1, x2, x3)) = 0   
POL(U4_G(x1, x2, x3)) = x2   
POL(U4_g(x1, x2, x3)) = 0   
POL(U5_g(x1, x2)) = 0   
POL(bin_tree_in_g(x1)) = 0   
POL(bin_tree_out_g(x1)) = 0   
POL(left_in_ga(x1)) = x1   
POL(left_out_ga(x1, x2)) = 0   
POL(right_in_ga(x1)) = 0   
POL(right_out_ga(x1, x2)) = x2   
POL(tree(x1, x2, x3)) = 1 + x2 + x3   
POL(true_in_) = 0   
POL(true_out_) = 0   
POL(void) = 0   

The following usable rules [FROCOS05] were oriented: none

(58) Obligation:

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

U3_G(T, L, right_out_ga(T, R)) → U4_G(T, R, bin_tree_in_g(L))
U4_G(T, R, bin_tree_out_g(L)) → BIN_TREE_IN_G(R)
U3_G(T, L, right_out_ga(T, R)) → BIN_TREE_IN_G(L)
BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void, void))
BIN_TREE_IN_G(tree(x0, x1, x2)) → U2_G(tree(x0, x1, x2), left_out_ga(tree(x0, x1, x2), x1))
U2_G(void, left_out_ga(void, void)) → U3_G(void, void, right_out_ga(void, void))

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g(void)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void, void)
left_in_ga(tree(X1, L, X2)) → left_out_ga(tree(X1, L, X2), L)
U2_g(T, left_out_ga(T, L)) → U3_g(T, L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void, void)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
U3_g(T, L, right_out_ga(T, R)) → U4_g(T, R, bin_tree_in_g(L))
U4_g(T, R, bin_tree_out_g(L)) → U5_g(T, bin_tree_in_g(R))
U5_g(T, bin_tree_out_g(R)) → bin_tree_out_g(T)

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1, x2)
U4_g(x0, x1, x2)
U5_g(x0, x1)

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

(59) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(60) Obligation:

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

U4_G(T, R, bin_tree_out_g(L)) → BIN_TREE_IN_G(R)
BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void, void))
U2_G(void, left_out_ga(void, void)) → U3_G(void, void, right_out_ga(void, void))
U3_G(T, L, right_out_ga(T, R)) → U4_G(T, R, bin_tree_in_g(L))
U3_G(T, L, right_out_ga(T, R)) → BIN_TREE_IN_G(L)

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g(void)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void, void)
left_in_ga(tree(X1, L, X2)) → left_out_ga(tree(X1, L, X2), L)
U2_g(T, left_out_ga(T, L)) → U3_g(T, L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void, void)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
U3_g(T, L, right_out_ga(T, R)) → U4_g(T, R, bin_tree_in_g(L))
U4_g(T, R, bin_tree_out_g(L)) → U5_g(T, bin_tree_in_g(R))
U5_g(T, bin_tree_out_g(R)) → bin_tree_out_g(T)

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1, x2)
U4_g(x0, x1, x2)
U5_g(x0, x1)

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

(61) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U3_G(T, L, right_out_ga(T, R)) → U4_G(T, R, bin_tree_in_g(L)) we obtained the following new rules [LPAR04]:

U3_G(void, void, right_out_ga(void, void)) → U4_G(void, void, bin_tree_in_g(void))

(62) Obligation:

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

U4_G(T, R, bin_tree_out_g(L)) → BIN_TREE_IN_G(R)
BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void, void))
U2_G(void, left_out_ga(void, void)) → U3_G(void, void, right_out_ga(void, void))
U3_G(T, L, right_out_ga(T, R)) → BIN_TREE_IN_G(L)
U3_G(void, void, right_out_ga(void, void)) → U4_G(void, void, bin_tree_in_g(void))

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g(void)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void, void)
left_in_ga(tree(X1, L, X2)) → left_out_ga(tree(X1, L, X2), L)
U2_g(T, left_out_ga(T, L)) → U3_g(T, L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void, void)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
U3_g(T, L, right_out_ga(T, R)) → U4_g(T, R, bin_tree_in_g(L))
U4_g(T, R, bin_tree_out_g(L)) → U5_g(T, bin_tree_in_g(R))
U5_g(T, bin_tree_out_g(R)) → bin_tree_out_g(T)

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1, x2)
U4_g(x0, x1, x2)
U5_g(x0, x1)

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

(63) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U3_G(T, L, right_out_ga(T, R)) → U4_G(T, R, bin_tree_in_g(L)) we obtained the following new rules [LPAR04]:

U3_G(void, void, right_out_ga(void, void)) → U4_G(void, void, bin_tree_in_g(void))

(64) Obligation:

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

U4_G(T, R, bin_tree_out_g(L)) → BIN_TREE_IN_G(R)
BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void, void))
U2_G(void, left_out_ga(void, void)) → U3_G(void, void, right_out_ga(void, void))
U3_G(T, L, right_out_ga(T, R)) → BIN_TREE_IN_G(L)
U3_G(void, void, right_out_ga(void, void)) → U4_G(void, void, bin_tree_in_g(void))

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g(void)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void, void)
left_in_ga(tree(X1, L, X2)) → left_out_ga(tree(X1, L, X2), L)
U2_g(T, left_out_ga(T, L)) → U3_g(T, L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void, void)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
U3_g(T, L, right_out_ga(T, R)) → U4_g(T, R, bin_tree_in_g(L))
U4_g(T, R, bin_tree_out_g(L)) → U5_g(T, bin_tree_in_g(R))
U5_g(T, bin_tree_out_g(R)) → bin_tree_out_g(T)

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1, x2)
U4_g(x0, x1, x2)
U5_g(x0, x1)

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

(65) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U4_G(T, R, bin_tree_out_g(L)) → BIN_TREE_IN_G(R) we obtained the following new rules [LPAR04]:

U4_G(void, void, bin_tree_out_g(x2)) → BIN_TREE_IN_G(void)

(66) Obligation:

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

BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void, void))
U2_G(void, left_out_ga(void, void)) → U3_G(void, void, right_out_ga(void, void))
U3_G(T, L, right_out_ga(T, R)) → BIN_TREE_IN_G(L)
U3_G(void, void, right_out_ga(void, void)) → U4_G(void, void, bin_tree_in_g(void))
U4_G(void, void, bin_tree_out_g(x2)) → BIN_TREE_IN_G(void)

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g(void)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void, void)
left_in_ga(tree(X1, L, X2)) → left_out_ga(tree(X1, L, X2), L)
U2_g(T, left_out_ga(T, L)) → U3_g(T, L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void, void)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
U3_g(T, L, right_out_ga(T, R)) → U4_g(T, R, bin_tree_in_g(L))
U4_g(T, R, bin_tree_out_g(L)) → U5_g(T, bin_tree_in_g(R))
U5_g(T, bin_tree_out_g(R)) → bin_tree_out_g(T)

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1, x2)
U4_g(x0, x1, x2)
U5_g(x0, x1)

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

(67) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U3_G(T, L, right_out_ga(T, R)) → BIN_TREE_IN_G(L) we obtained the following new rules [LPAR04]:

U3_G(void, void, right_out_ga(void, void)) → BIN_TREE_IN_G(void)

(68) Obligation:

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

BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void, void))
U2_G(void, left_out_ga(void, void)) → U3_G(void, void, right_out_ga(void, void))
U3_G(void, void, right_out_ga(void, void)) → U4_G(void, void, bin_tree_in_g(void))
U4_G(void, void, bin_tree_out_g(x2)) → BIN_TREE_IN_G(void)
U3_G(void, void, right_out_ga(void, void)) → BIN_TREE_IN_G(void)

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g(void)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void, void)
left_in_ga(tree(X1, L, X2)) → left_out_ga(tree(X1, L, X2), L)
U2_g(T, left_out_ga(T, L)) → U3_g(T, L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void, void)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
U3_g(T, L, right_out_ga(T, R)) → U4_g(T, R, bin_tree_in_g(L))
U4_g(T, R, bin_tree_out_g(L)) → U5_g(T, bin_tree_in_g(R))
U5_g(T, bin_tree_out_g(R)) → bin_tree_out_g(T)

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1, x2)
U4_g(x0, x1, x2)
U5_g(x0, x1)

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

(69) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U3_G(void, void, right_out_ga(void, void)) → U4_G(void, void, bin_tree_in_g(void)) at position [2] we obtained the following new rules [LPAR04]:

U3_G(void, void, right_out_ga(void, void)) → U4_G(void, void, U1_g(true_in_))
U3_G(void, void, right_out_ga(void, void)) → U4_G(void, void, U2_g(void, left_in_ga(void)))

(70) Obligation:

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

BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void, void))
U2_G(void, left_out_ga(void, void)) → U3_G(void, void, right_out_ga(void, void))
U4_G(void, void, bin_tree_out_g(x2)) → BIN_TREE_IN_G(void)
U3_G(void, void, right_out_ga(void, void)) → BIN_TREE_IN_G(void)
U3_G(void, void, right_out_ga(void, void)) → U4_G(void, void, U1_g(true_in_))
U3_G(void, void, right_out_ga(void, void)) → U4_G(void, void, U2_g(void, left_in_ga(void)))

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g(void)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void, void)
left_in_ga(tree(X1, L, X2)) → left_out_ga(tree(X1, L, X2), L)
U2_g(T, left_out_ga(T, L)) → U3_g(T, L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void, void)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
U3_g(T, L, right_out_ga(T, R)) → U4_g(T, R, bin_tree_in_g(L))
U4_g(T, R, bin_tree_out_g(L)) → U5_g(T, bin_tree_in_g(R))
U5_g(T, bin_tree_out_g(R)) → bin_tree_out_g(T)

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1, x2)
U4_g(x0, x1, x2)
U5_g(x0, x1)

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

(71) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U3_G(void, void, right_out_ga(void, void)) → U4_G(void, void, U1_g(true_in_)) at position [2,0] we obtained the following new rules [LPAR04]:

U3_G(void, void, right_out_ga(void, void)) → U4_G(void, void, U1_g(true_out_))

(72) Obligation:

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

BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void, void))
U2_G(void, left_out_ga(void, void)) → U3_G(void, void, right_out_ga(void, void))
U4_G(void, void, bin_tree_out_g(x2)) → BIN_TREE_IN_G(void)
U3_G(void, void, right_out_ga(void, void)) → BIN_TREE_IN_G(void)
U3_G(void, void, right_out_ga(void, void)) → U4_G(void, void, U2_g(void, left_in_ga(void)))
U3_G(void, void, right_out_ga(void, void)) → U4_G(void, void, U1_g(true_out_))

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g(void)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void, void)
left_in_ga(tree(X1, L, X2)) → left_out_ga(tree(X1, L, X2), L)
U2_g(T, left_out_ga(T, L)) → U3_g(T, L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void, void)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
U3_g(T, L, right_out_ga(T, R)) → U4_g(T, R, bin_tree_in_g(L))
U4_g(T, R, bin_tree_out_g(L)) → U5_g(T, bin_tree_in_g(R))
U5_g(T, bin_tree_out_g(R)) → bin_tree_out_g(T)

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1, x2)
U4_g(x0, x1, x2)
U5_g(x0, x1)

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

(73) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U3_G(void, void, right_out_ga(void, void)) → U4_G(void, void, U2_g(void, left_in_ga(void))) at position [2,1] we obtained the following new rules [LPAR04]:

U3_G(void, void, right_out_ga(void, void)) → U4_G(void, void, U2_g(void, left_out_ga(void, void)))

(74) Obligation:

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

BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void, void))
U2_G(void, left_out_ga(void, void)) → U3_G(void, void, right_out_ga(void, void))
U4_G(void, void, bin_tree_out_g(x2)) → BIN_TREE_IN_G(void)
U3_G(void, void, right_out_ga(void, void)) → BIN_TREE_IN_G(void)
U3_G(void, void, right_out_ga(void, void)) → U4_G(void, void, U1_g(true_out_))
U3_G(void, void, right_out_ga(void, void)) → U4_G(void, void, U2_g(void, left_out_ga(void, void)))

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g(void)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void, void)
left_in_ga(tree(X1, L, X2)) → left_out_ga(tree(X1, L, X2), L)
U2_g(T, left_out_ga(T, L)) → U3_g(T, L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void, void)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
U3_g(T, L, right_out_ga(T, R)) → U4_g(T, R, bin_tree_in_g(L))
U4_g(T, R, bin_tree_out_g(L)) → U5_g(T, bin_tree_in_g(R))
U5_g(T, bin_tree_out_g(R)) → bin_tree_out_g(T)

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1, x2)
U4_g(x0, x1, x2)
U5_g(x0, x1)

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

(75) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U3_G(void, void, right_out_ga(void, void)) → U4_G(void, void, U1_g(true_out_)) at position [2] we obtained the following new rules [LPAR04]:

U3_G(void, void, right_out_ga(void, void)) → U4_G(void, void, bin_tree_out_g(void))

(76) Obligation:

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

BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void, void))
U2_G(void, left_out_ga(void, void)) → U3_G(void, void, right_out_ga(void, void))
U4_G(void, void, bin_tree_out_g(x2)) → BIN_TREE_IN_G(void)
U3_G(void, void, right_out_ga(void, void)) → BIN_TREE_IN_G(void)
U3_G(void, void, right_out_ga(void, void)) → U4_G(void, void, U2_g(void, left_out_ga(void, void)))
U3_G(void, void, right_out_ga(void, void)) → U4_G(void, void, bin_tree_out_g(void))

The TRS R consists of the following rules:

bin_tree_in_g(void) → U1_g(true_in_)
true_in_ → true_out_
U1_g(true_out_) → bin_tree_out_g(void)
bin_tree_in_g(T) → U2_g(T, left_in_ga(T))
left_in_ga(void) → left_out_ga(void, void)
left_in_ga(tree(X1, L, X2)) → left_out_ga(tree(X1, L, X2), L)
U2_g(T, left_out_ga(T, L)) → U3_g(T, L, right_in_ga(T))
right_in_ga(void) → right_out_ga(void, void)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
U3_g(T, L, right_out_ga(T, R)) → U4_g(T, R, bin_tree_in_g(L))
U4_g(T, R, bin_tree_out_g(L)) → U5_g(T, bin_tree_in_g(R))
U5_g(T, bin_tree_out_g(R)) → bin_tree_out_g(T)

The set Q consists of the following terms:

bin_tree_in_g(x0)
true_in_
U1_g(x0)
left_in_ga(x0)
U2_g(x0, x1)
right_in_ga(x0)
U3_g(x0, x1, x2)
U4_g(x0, x1, x2)
U5_g(x0, x1)

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

(77) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = U2_G(void, left_out_ga(void, void)) evaluates to t =U2_G(void, left_out_ga(void, void))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Matcher: [ ]
  • Semiunifier: [ ]



Rewriting sequence

U2_G(void, left_out_ga(void, void)) → U3_G(void, void, right_out_ga(void, void))
with rule U2_G(void, left_out_ga(void, void)) → U3_G(void, void, right_out_ga(void, void)) at position [] and matcher [ ]

U3_G(void, void, right_out_ga(void, void)) → BIN_TREE_IN_G(void)
with rule U3_G(void, void, right_out_ga(void, void)) → BIN_TREE_IN_G(void) at position [] and matcher [ ]

BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void, void))
with rule BIN_TREE_IN_G(void) → U2_G(void, left_out_ga(void, void))

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.



(78) FALSE