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

(0) Obligation:

Clauses:

preorder(X, Y) :- pdl(X, -(Y, [])).
pdl(nil, Y) :- ','(!, eq(Y, -(X, X))).
pdl(T, -(.(X, Xs), Zs)) :- ','(value(T, X), ','(left(T, L), ','(right(T, R), ','(pdl(L, -(Xs, Ys)), pdl(R, -(Ys, Zs)))))).
left(nil, nil).
left(tree(L, X1, X2), L).
right(nil, nil).
right(tree(X3, X4, R), R).
value(nil, X5).
value(tree(X6, X, X7), X).
eq(X, X).

Queries:

preorder(g,a).

(1) CutEliminatorProof (SOUND transformation)

Eliminated all cuts by simply ignoring them[PROLOG].

(2) Obligation:

Clauses:

preorder(X, Y) :- pdl(X, -(Y, [])).
pdl(nil, Y) :- eq(Y, -(X, X)).
pdl(T, -(.(X, Xs), Zs)) :- ','(value(T, X), ','(left(T, L), ','(right(T, R), ','(pdl(L, -(Xs, Ys)), pdl(R, -(Ys, Zs)))))).
left(nil, nil).
left(tree(L, X1, X2), L).
right(nil, nil).
right(tree(X3, X4, R), R).
value(nil, X5).
value(tree(X6, X, X7), X).
eq(X, X).

Queries:

preorder(g,a).

(3) PrologToPiTRSProof (SOUND transformation)

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

preorder_in_ga(X, Y) → U1_ga(X, Y, pdl_in_ga(X, -(Y, [])))
pdl_in_ga(nil, Y) → U2_ga(Y, eq_in_aa(Y, -(X, X)))
eq_in_aa(X, X) → eq_out_aa(X, X)
U2_ga(Y, eq_out_aa(Y, -(X, X))) → pdl_out_ga(nil, Y)
pdl_in_ga(T, -(.(X, Xs), Zs)) → U3_ga(T, X, Xs, Zs, value_in_ga(T, X))
value_in_ga(nil, X5) → value_out_ga(nil, X5)
value_in_ga(tree(X6, X, X7), X) → value_out_ga(tree(X6, X, X7), X)
U3_ga(T, X, Xs, Zs, value_out_ga(T, X)) → U4_ga(T, X, Xs, Zs, left_in_ga(T, L))
left_in_ga(nil, nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2), L) → left_out_ga(tree(L, X1, X2), L)
U4_ga(T, X, Xs, Zs, left_out_ga(T, L)) → U5_ga(T, X, Xs, Zs, L, right_in_ga(T, R))
right_in_ga(nil, nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R), R) → right_out_ga(tree(X3, X4, R), R)
U5_ga(T, X, Xs, Zs, L, right_out_ga(T, R)) → U6_ga(T, X, Xs, Zs, L, R, pdl_in_ga(L, -(Xs, Ys)))
U6_ga(T, X, Xs, Zs, L, R, pdl_out_ga(L, -(Xs, Ys))) → U7_ga(T, X, Xs, Zs, pdl_in_ga(R, -(Ys, Zs)))
U7_ga(T, X, Xs, Zs, pdl_out_ga(R, -(Ys, Zs))) → pdl_out_ga(T, -(.(X, Xs), Zs))
U1_ga(X, Y, pdl_out_ga(X, -(Y, []))) → preorder_out_ga(X, Y)

The argument filtering Pi contains the following mapping:
preorder_in_ga(x1, x2)  =  preorder_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
pdl_in_ga(x1, x2)  =  pdl_in_ga(x1)
nil  =  nil
U2_ga(x1, x2)  =  U2_ga(x2)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
pdl_out_ga(x1, x2)  =  pdl_out_ga
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x5)
value_in_ga(x1, x2)  =  value_in_ga(x1)
value_out_ga(x1, x2)  =  value_out_ga
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x5)
left_in_ga(x1, x2)  =  left_in_ga(x1)
left_out_ga(x1, x2)  =  left_out_ga(x2)
U5_ga(x1, x2, x3, x4, x5, x6)  =  U5_ga(x5, x6)
right_in_ga(x1, x2)  =  right_in_ga(x1)
right_out_ga(x1, x2)  =  right_out_ga(x2)
U6_ga(x1, x2, x3, x4, x5, x6, x7)  =  U6_ga(x6, x7)
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x5)
preorder_out_ga(x1, x2)  =  preorder_out_ga

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

preorder_in_ga(X, Y) → U1_ga(X, Y, pdl_in_ga(X, -(Y, [])))
pdl_in_ga(nil, Y) → U2_ga(Y, eq_in_aa(Y, -(X, X)))
eq_in_aa(X, X) → eq_out_aa(X, X)
U2_ga(Y, eq_out_aa(Y, -(X, X))) → pdl_out_ga(nil, Y)
pdl_in_ga(T, -(.(X, Xs), Zs)) → U3_ga(T, X, Xs, Zs, value_in_ga(T, X))
value_in_ga(nil, X5) → value_out_ga(nil, X5)
value_in_ga(tree(X6, X, X7), X) → value_out_ga(tree(X6, X, X7), X)
U3_ga(T, X, Xs, Zs, value_out_ga(T, X)) → U4_ga(T, X, Xs, Zs, left_in_ga(T, L))
left_in_ga(nil, nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2), L) → left_out_ga(tree(L, X1, X2), L)
U4_ga(T, X, Xs, Zs, left_out_ga(T, L)) → U5_ga(T, X, Xs, Zs, L, right_in_ga(T, R))
right_in_ga(nil, nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R), R) → right_out_ga(tree(X3, X4, R), R)
U5_ga(T, X, Xs, Zs, L, right_out_ga(T, R)) → U6_ga(T, X, Xs, Zs, L, R, pdl_in_ga(L, -(Xs, Ys)))
U6_ga(T, X, Xs, Zs, L, R, pdl_out_ga(L, -(Xs, Ys))) → U7_ga(T, X, Xs, Zs, pdl_in_ga(R, -(Ys, Zs)))
U7_ga(T, X, Xs, Zs, pdl_out_ga(R, -(Ys, Zs))) → pdl_out_ga(T, -(.(X, Xs), Zs))
U1_ga(X, Y, pdl_out_ga(X, -(Y, []))) → preorder_out_ga(X, Y)

The argument filtering Pi contains the following mapping:
preorder_in_ga(x1, x2)  =  preorder_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
pdl_in_ga(x1, x2)  =  pdl_in_ga(x1)
nil  =  nil
U2_ga(x1, x2)  =  U2_ga(x2)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
pdl_out_ga(x1, x2)  =  pdl_out_ga
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x5)
value_in_ga(x1, x2)  =  value_in_ga(x1)
value_out_ga(x1, x2)  =  value_out_ga
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x5)
left_in_ga(x1, x2)  =  left_in_ga(x1)
left_out_ga(x1, x2)  =  left_out_ga(x2)
U5_ga(x1, x2, x3, x4, x5, x6)  =  U5_ga(x5, x6)
right_in_ga(x1, x2)  =  right_in_ga(x1)
right_out_ga(x1, x2)  =  right_out_ga(x2)
U6_ga(x1, x2, x3, x4, x5, x6, x7)  =  U6_ga(x6, x7)
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x5)
preorder_out_ga(x1, x2)  =  preorder_out_ga

(5) 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:

PREORDER_IN_GA(X, Y) → U1_GA(X, Y, pdl_in_ga(X, -(Y, [])))
PREORDER_IN_GA(X, Y) → PDL_IN_GA(X, -(Y, []))
PDL_IN_GA(nil, Y) → U2_GA(Y, eq_in_aa(Y, -(X, X)))
PDL_IN_GA(nil, Y) → EQ_IN_AA(Y, -(X, X))
PDL_IN_GA(T, -(.(X, Xs), Zs)) → U3_GA(T, X, Xs, Zs, value_in_ga(T, X))
PDL_IN_GA(T, -(.(X, Xs), Zs)) → VALUE_IN_GA(T, X)
U3_GA(T, X, Xs, Zs, value_out_ga(T, X)) → U4_GA(T, X, Xs, Zs, left_in_ga(T, L))
U3_GA(T, X, Xs, Zs, value_out_ga(T, X)) → LEFT_IN_GA(T, L)
U4_GA(T, X, Xs, Zs, left_out_ga(T, L)) → U5_GA(T, X, Xs, Zs, L, right_in_ga(T, R))
U4_GA(T, X, Xs, Zs, left_out_ga(T, L)) → RIGHT_IN_GA(T, R)
U5_GA(T, X, Xs, Zs, L, right_out_ga(T, R)) → U6_GA(T, X, Xs, Zs, L, R, pdl_in_ga(L, -(Xs, Ys)))
U5_GA(T, X, Xs, Zs, L, right_out_ga(T, R)) → PDL_IN_GA(L, -(Xs, Ys))
U6_GA(T, X, Xs, Zs, L, R, pdl_out_ga(L, -(Xs, Ys))) → U7_GA(T, X, Xs, Zs, pdl_in_ga(R, -(Ys, Zs)))
U6_GA(T, X, Xs, Zs, L, R, pdl_out_ga(L, -(Xs, Ys))) → PDL_IN_GA(R, -(Ys, Zs))

The TRS R consists of the following rules:

preorder_in_ga(X, Y) → U1_ga(X, Y, pdl_in_ga(X, -(Y, [])))
pdl_in_ga(nil, Y) → U2_ga(Y, eq_in_aa(Y, -(X, X)))
eq_in_aa(X, X) → eq_out_aa(X, X)
U2_ga(Y, eq_out_aa(Y, -(X, X))) → pdl_out_ga(nil, Y)
pdl_in_ga(T, -(.(X, Xs), Zs)) → U3_ga(T, X, Xs, Zs, value_in_ga(T, X))
value_in_ga(nil, X5) → value_out_ga(nil, X5)
value_in_ga(tree(X6, X, X7), X) → value_out_ga(tree(X6, X, X7), X)
U3_ga(T, X, Xs, Zs, value_out_ga(T, X)) → U4_ga(T, X, Xs, Zs, left_in_ga(T, L))
left_in_ga(nil, nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2), L) → left_out_ga(tree(L, X1, X2), L)
U4_ga(T, X, Xs, Zs, left_out_ga(T, L)) → U5_ga(T, X, Xs, Zs, L, right_in_ga(T, R))
right_in_ga(nil, nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R), R) → right_out_ga(tree(X3, X4, R), R)
U5_ga(T, X, Xs, Zs, L, right_out_ga(T, R)) → U6_ga(T, X, Xs, Zs, L, R, pdl_in_ga(L, -(Xs, Ys)))
U6_ga(T, X, Xs, Zs, L, R, pdl_out_ga(L, -(Xs, Ys))) → U7_ga(T, X, Xs, Zs, pdl_in_ga(R, -(Ys, Zs)))
U7_ga(T, X, Xs, Zs, pdl_out_ga(R, -(Ys, Zs))) → pdl_out_ga(T, -(.(X, Xs), Zs))
U1_ga(X, Y, pdl_out_ga(X, -(Y, []))) → preorder_out_ga(X, Y)

The argument filtering Pi contains the following mapping:
preorder_in_ga(x1, x2)  =  preorder_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
pdl_in_ga(x1, x2)  =  pdl_in_ga(x1)
nil  =  nil
U2_ga(x1, x2)  =  U2_ga(x2)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
pdl_out_ga(x1, x2)  =  pdl_out_ga
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x5)
value_in_ga(x1, x2)  =  value_in_ga(x1)
value_out_ga(x1, x2)  =  value_out_ga
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x5)
left_in_ga(x1, x2)  =  left_in_ga(x1)
left_out_ga(x1, x2)  =  left_out_ga(x2)
U5_ga(x1, x2, x3, x4, x5, x6)  =  U5_ga(x5, x6)
right_in_ga(x1, x2)  =  right_in_ga(x1)
right_out_ga(x1, x2)  =  right_out_ga(x2)
U6_ga(x1, x2, x3, x4, x5, x6, x7)  =  U6_ga(x6, x7)
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x5)
preorder_out_ga(x1, x2)  =  preorder_out_ga
PREORDER_IN_GA(x1, x2)  =  PREORDER_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
PDL_IN_GA(x1, x2)  =  PDL_IN_GA(x1)
U2_GA(x1, x2)  =  U2_GA(x2)
EQ_IN_AA(x1, x2)  =  EQ_IN_AA
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x1, x5)
VALUE_IN_GA(x1, x2)  =  VALUE_IN_GA(x1)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x1, x5)
LEFT_IN_GA(x1, x2)  =  LEFT_IN_GA(x1)
U5_GA(x1, x2, x3, x4, x5, x6)  =  U5_GA(x5, x6)
RIGHT_IN_GA(x1, x2)  =  RIGHT_IN_GA(x1)
U6_GA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GA(x6, x7)
U7_GA(x1, x2, x3, x4, x5)  =  U7_GA(x5)

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

(6) Obligation:

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

PREORDER_IN_GA(X, Y) → U1_GA(X, Y, pdl_in_ga(X, -(Y, [])))
PREORDER_IN_GA(X, Y) → PDL_IN_GA(X, -(Y, []))
PDL_IN_GA(nil, Y) → U2_GA(Y, eq_in_aa(Y, -(X, X)))
PDL_IN_GA(nil, Y) → EQ_IN_AA(Y, -(X, X))
PDL_IN_GA(T, -(.(X, Xs), Zs)) → U3_GA(T, X, Xs, Zs, value_in_ga(T, X))
PDL_IN_GA(T, -(.(X, Xs), Zs)) → VALUE_IN_GA(T, X)
U3_GA(T, X, Xs, Zs, value_out_ga(T, X)) → U4_GA(T, X, Xs, Zs, left_in_ga(T, L))
U3_GA(T, X, Xs, Zs, value_out_ga(T, X)) → LEFT_IN_GA(T, L)
U4_GA(T, X, Xs, Zs, left_out_ga(T, L)) → U5_GA(T, X, Xs, Zs, L, right_in_ga(T, R))
U4_GA(T, X, Xs, Zs, left_out_ga(T, L)) → RIGHT_IN_GA(T, R)
U5_GA(T, X, Xs, Zs, L, right_out_ga(T, R)) → U6_GA(T, X, Xs, Zs, L, R, pdl_in_ga(L, -(Xs, Ys)))
U5_GA(T, X, Xs, Zs, L, right_out_ga(T, R)) → PDL_IN_GA(L, -(Xs, Ys))
U6_GA(T, X, Xs, Zs, L, R, pdl_out_ga(L, -(Xs, Ys))) → U7_GA(T, X, Xs, Zs, pdl_in_ga(R, -(Ys, Zs)))
U6_GA(T, X, Xs, Zs, L, R, pdl_out_ga(L, -(Xs, Ys))) → PDL_IN_GA(R, -(Ys, Zs))

The TRS R consists of the following rules:

preorder_in_ga(X, Y) → U1_ga(X, Y, pdl_in_ga(X, -(Y, [])))
pdl_in_ga(nil, Y) → U2_ga(Y, eq_in_aa(Y, -(X, X)))
eq_in_aa(X, X) → eq_out_aa(X, X)
U2_ga(Y, eq_out_aa(Y, -(X, X))) → pdl_out_ga(nil, Y)
pdl_in_ga(T, -(.(X, Xs), Zs)) → U3_ga(T, X, Xs, Zs, value_in_ga(T, X))
value_in_ga(nil, X5) → value_out_ga(nil, X5)
value_in_ga(tree(X6, X, X7), X) → value_out_ga(tree(X6, X, X7), X)
U3_ga(T, X, Xs, Zs, value_out_ga(T, X)) → U4_ga(T, X, Xs, Zs, left_in_ga(T, L))
left_in_ga(nil, nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2), L) → left_out_ga(tree(L, X1, X2), L)
U4_ga(T, X, Xs, Zs, left_out_ga(T, L)) → U5_ga(T, X, Xs, Zs, L, right_in_ga(T, R))
right_in_ga(nil, nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R), R) → right_out_ga(tree(X3, X4, R), R)
U5_ga(T, X, Xs, Zs, L, right_out_ga(T, R)) → U6_ga(T, X, Xs, Zs, L, R, pdl_in_ga(L, -(Xs, Ys)))
U6_ga(T, X, Xs, Zs, L, R, pdl_out_ga(L, -(Xs, Ys))) → U7_ga(T, X, Xs, Zs, pdl_in_ga(R, -(Ys, Zs)))
U7_ga(T, X, Xs, Zs, pdl_out_ga(R, -(Ys, Zs))) → pdl_out_ga(T, -(.(X, Xs), Zs))
U1_ga(X, Y, pdl_out_ga(X, -(Y, []))) → preorder_out_ga(X, Y)

The argument filtering Pi contains the following mapping:
preorder_in_ga(x1, x2)  =  preorder_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
pdl_in_ga(x1, x2)  =  pdl_in_ga(x1)
nil  =  nil
U2_ga(x1, x2)  =  U2_ga(x2)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
pdl_out_ga(x1, x2)  =  pdl_out_ga
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x5)
value_in_ga(x1, x2)  =  value_in_ga(x1)
value_out_ga(x1, x2)  =  value_out_ga
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x5)
left_in_ga(x1, x2)  =  left_in_ga(x1)
left_out_ga(x1, x2)  =  left_out_ga(x2)
U5_ga(x1, x2, x3, x4, x5, x6)  =  U5_ga(x5, x6)
right_in_ga(x1, x2)  =  right_in_ga(x1)
right_out_ga(x1, x2)  =  right_out_ga(x2)
U6_ga(x1, x2, x3, x4, x5, x6, x7)  =  U6_ga(x6, x7)
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x5)
preorder_out_ga(x1, x2)  =  preorder_out_ga
PREORDER_IN_GA(x1, x2)  =  PREORDER_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
PDL_IN_GA(x1, x2)  =  PDL_IN_GA(x1)
U2_GA(x1, x2)  =  U2_GA(x2)
EQ_IN_AA(x1, x2)  =  EQ_IN_AA
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x1, x5)
VALUE_IN_GA(x1, x2)  =  VALUE_IN_GA(x1)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x1, x5)
LEFT_IN_GA(x1, x2)  =  LEFT_IN_GA(x1)
U5_GA(x1, x2, x3, x4, x5, x6)  =  U5_GA(x5, x6)
RIGHT_IN_GA(x1, x2)  =  RIGHT_IN_GA(x1)
U6_GA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GA(x6, x7)
U7_GA(x1, x2, x3, x4, x5)  =  U7_GA(x5)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Obligation:

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

PDL_IN_GA(T, -(.(X, Xs), Zs)) → U3_GA(T, X, Xs, Zs, value_in_ga(T, X))
U3_GA(T, X, Xs, Zs, value_out_ga(T, X)) → U4_GA(T, X, Xs, Zs, left_in_ga(T, L))
U4_GA(T, X, Xs, Zs, left_out_ga(T, L)) → U5_GA(T, X, Xs, Zs, L, right_in_ga(T, R))
U5_GA(T, X, Xs, Zs, L, right_out_ga(T, R)) → U6_GA(T, X, Xs, Zs, L, R, pdl_in_ga(L, -(Xs, Ys)))
U6_GA(T, X, Xs, Zs, L, R, pdl_out_ga(L, -(Xs, Ys))) → PDL_IN_GA(R, -(Ys, Zs))
U5_GA(T, X, Xs, Zs, L, right_out_ga(T, R)) → PDL_IN_GA(L, -(Xs, Ys))

The TRS R consists of the following rules:

preorder_in_ga(X, Y) → U1_ga(X, Y, pdl_in_ga(X, -(Y, [])))
pdl_in_ga(nil, Y) → U2_ga(Y, eq_in_aa(Y, -(X, X)))
eq_in_aa(X, X) → eq_out_aa(X, X)
U2_ga(Y, eq_out_aa(Y, -(X, X))) → pdl_out_ga(nil, Y)
pdl_in_ga(T, -(.(X, Xs), Zs)) → U3_ga(T, X, Xs, Zs, value_in_ga(T, X))
value_in_ga(nil, X5) → value_out_ga(nil, X5)
value_in_ga(tree(X6, X, X7), X) → value_out_ga(tree(X6, X, X7), X)
U3_ga(T, X, Xs, Zs, value_out_ga(T, X)) → U4_ga(T, X, Xs, Zs, left_in_ga(T, L))
left_in_ga(nil, nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2), L) → left_out_ga(tree(L, X1, X2), L)
U4_ga(T, X, Xs, Zs, left_out_ga(T, L)) → U5_ga(T, X, Xs, Zs, L, right_in_ga(T, R))
right_in_ga(nil, nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R), R) → right_out_ga(tree(X3, X4, R), R)
U5_ga(T, X, Xs, Zs, L, right_out_ga(T, R)) → U6_ga(T, X, Xs, Zs, L, R, pdl_in_ga(L, -(Xs, Ys)))
U6_ga(T, X, Xs, Zs, L, R, pdl_out_ga(L, -(Xs, Ys))) → U7_ga(T, X, Xs, Zs, pdl_in_ga(R, -(Ys, Zs)))
U7_ga(T, X, Xs, Zs, pdl_out_ga(R, -(Ys, Zs))) → pdl_out_ga(T, -(.(X, Xs), Zs))
U1_ga(X, Y, pdl_out_ga(X, -(Y, []))) → preorder_out_ga(X, Y)

The argument filtering Pi contains the following mapping:
preorder_in_ga(x1, x2)  =  preorder_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
pdl_in_ga(x1, x2)  =  pdl_in_ga(x1)
nil  =  nil
U2_ga(x1, x2)  =  U2_ga(x2)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
pdl_out_ga(x1, x2)  =  pdl_out_ga
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x5)
value_in_ga(x1, x2)  =  value_in_ga(x1)
value_out_ga(x1, x2)  =  value_out_ga
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x5)
left_in_ga(x1, x2)  =  left_in_ga(x1)
left_out_ga(x1, x2)  =  left_out_ga(x2)
U5_ga(x1, x2, x3, x4, x5, x6)  =  U5_ga(x5, x6)
right_in_ga(x1, x2)  =  right_in_ga(x1)
right_out_ga(x1, x2)  =  right_out_ga(x2)
U6_ga(x1, x2, x3, x4, x5, x6, x7)  =  U6_ga(x6, x7)
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x5)
preorder_out_ga(x1, x2)  =  preorder_out_ga
PDL_IN_GA(x1, x2)  =  PDL_IN_GA(x1)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x1, x5)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x1, x5)
U5_GA(x1, x2, x3, x4, x5, x6)  =  U5_GA(x5, x6)
U6_GA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GA(x6, x7)

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

(9) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(10) Obligation:

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

PDL_IN_GA(T, -(.(X, Xs), Zs)) → U3_GA(T, X, Xs, Zs, value_in_ga(T, X))
U3_GA(T, X, Xs, Zs, value_out_ga(T, X)) → U4_GA(T, X, Xs, Zs, left_in_ga(T, L))
U4_GA(T, X, Xs, Zs, left_out_ga(T, L)) → U5_GA(T, X, Xs, Zs, L, right_in_ga(T, R))
U5_GA(T, X, Xs, Zs, L, right_out_ga(T, R)) → U6_GA(T, X, Xs, Zs, L, R, pdl_in_ga(L, -(Xs, Ys)))
U6_GA(T, X, Xs, Zs, L, R, pdl_out_ga(L, -(Xs, Ys))) → PDL_IN_GA(R, -(Ys, Zs))
U5_GA(T, X, Xs, Zs, L, right_out_ga(T, R)) → PDL_IN_GA(L, -(Xs, Ys))

The TRS R consists of the following rules:

value_in_ga(nil, X5) → value_out_ga(nil, X5)
value_in_ga(tree(X6, X, X7), X) → value_out_ga(tree(X6, X, X7), X)
left_in_ga(nil, nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2), L) → left_out_ga(tree(L, X1, X2), L)
right_in_ga(nil, nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R), R) → right_out_ga(tree(X3, X4, R), R)
pdl_in_ga(nil, Y) → U2_ga(Y, eq_in_aa(Y, -(X, X)))
pdl_in_ga(T, -(.(X, Xs), Zs)) → U3_ga(T, X, Xs, Zs, value_in_ga(T, X))
U2_ga(Y, eq_out_aa(Y, -(X, X))) → pdl_out_ga(nil, Y)
U3_ga(T, X, Xs, Zs, value_out_ga(T, X)) → U4_ga(T, X, Xs, Zs, left_in_ga(T, L))
eq_in_aa(X, X) → eq_out_aa(X, X)
U4_ga(T, X, Xs, Zs, left_out_ga(T, L)) → U5_ga(T, X, Xs, Zs, L, right_in_ga(T, R))
U5_ga(T, X, Xs, Zs, L, right_out_ga(T, R)) → U6_ga(T, X, Xs, Zs, L, R, pdl_in_ga(L, -(Xs, Ys)))
U6_ga(T, X, Xs, Zs, L, R, pdl_out_ga(L, -(Xs, Ys))) → U7_ga(T, X, Xs, Zs, pdl_in_ga(R, -(Ys, Zs)))
U7_ga(T, X, Xs, Zs, pdl_out_ga(R, -(Ys, Zs))) → pdl_out_ga(T, -(.(X, Xs), Zs))

The argument filtering Pi contains the following mapping:
pdl_in_ga(x1, x2)  =  pdl_in_ga(x1)
nil  =  nil
U2_ga(x1, x2)  =  U2_ga(x2)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
pdl_out_ga(x1, x2)  =  pdl_out_ga
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x5)
value_in_ga(x1, x2)  =  value_in_ga(x1)
value_out_ga(x1, x2)  =  value_out_ga
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x5)
left_in_ga(x1, x2)  =  left_in_ga(x1)
left_out_ga(x1, x2)  =  left_out_ga(x2)
U5_ga(x1, x2, x3, x4, x5, x6)  =  U5_ga(x5, x6)
right_in_ga(x1, x2)  =  right_in_ga(x1)
right_out_ga(x1, x2)  =  right_out_ga(x2)
U6_ga(x1, x2, x3, x4, x5, x6, x7)  =  U6_ga(x6, x7)
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x5)
PDL_IN_GA(x1, x2)  =  PDL_IN_GA(x1)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x1, x5)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x1, x5)
U5_GA(x1, x2, x3, x4, x5, x6)  =  U5_GA(x5, x6)
U6_GA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GA(x6, x7)

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:

PDL_IN_GA(T) → U3_GA(T, value_in_ga(T))
U3_GA(T, value_out_ga) → U4_GA(T, left_in_ga(T))
U4_GA(T, left_out_ga(L)) → U5_GA(L, right_in_ga(T))
U5_GA(L, right_out_ga(R)) → U6_GA(R, pdl_in_ga(L))
U6_GA(R, pdl_out_ga) → PDL_IN_GA(R)
U5_GA(L, right_out_ga(R)) → PDL_IN_GA(L)

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga
value_in_ga(tree(X6, X, X7)) → value_out_ga
left_in_ga(nil) → left_out_ga(nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(L)
right_in_ga(nil) → right_out_ga(nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga
U3_ga(T, value_out_ga) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(L)) → U5_ga(L, right_in_ga(T))
U5_ga(L, right_out_ga(R)) → U6_ga(R, pdl_in_ga(L))
U6_ga(R, pdl_out_ga) → U7_ga(pdl_in_ga(R))
U7_ga(pdl_out_ga) → pdl_out_ga

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1)
U6_ga(x0, x1)
U7_ga(x0)

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

(13) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule PDL_IN_GA(T) → U3_GA(T, value_in_ga(T)) at position [1] we obtained the following new rules [LPAR04]:

PDL_IN_GA(nil) → U3_GA(nil, value_out_ga)
PDL_IN_GA(tree(x0, x1, x2)) → U3_GA(tree(x0, x1, x2), value_out_ga)

(14) Obligation:

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

U3_GA(T, value_out_ga) → U4_GA(T, left_in_ga(T))
U4_GA(T, left_out_ga(L)) → U5_GA(L, right_in_ga(T))
U5_GA(L, right_out_ga(R)) → U6_GA(R, pdl_in_ga(L))
U6_GA(R, pdl_out_ga) → PDL_IN_GA(R)
U5_GA(L, right_out_ga(R)) → PDL_IN_GA(L)
PDL_IN_GA(nil) → U3_GA(nil, value_out_ga)
PDL_IN_GA(tree(x0, x1, x2)) → U3_GA(tree(x0, x1, x2), value_out_ga)

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga
value_in_ga(tree(X6, X, X7)) → value_out_ga
left_in_ga(nil) → left_out_ga(nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(L)
right_in_ga(nil) → right_out_ga(nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga
U3_ga(T, value_out_ga) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(L)) → U5_ga(L, right_in_ga(T))
U5_ga(L, right_out_ga(R)) → U6_ga(R, pdl_in_ga(L))
U6_ga(R, pdl_out_ga) → U7_ga(pdl_in_ga(R))
U7_ga(pdl_out_ga) → pdl_out_ga

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1)
U6_ga(x0, x1)
U7_ga(x0)

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

(15) Narrowing (SOUND transformation)

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

U3_GA(nil, value_out_ga) → U4_GA(nil, left_out_ga(nil))
U3_GA(tree(x0, x1, x2), value_out_ga) → U4_GA(tree(x0, x1, x2), left_out_ga(x0))

(16) Obligation:

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

U4_GA(T, left_out_ga(L)) → U5_GA(L, right_in_ga(T))
U5_GA(L, right_out_ga(R)) → U6_GA(R, pdl_in_ga(L))
U6_GA(R, pdl_out_ga) → PDL_IN_GA(R)
U5_GA(L, right_out_ga(R)) → PDL_IN_GA(L)
PDL_IN_GA(nil) → U3_GA(nil, value_out_ga)
PDL_IN_GA(tree(x0, x1, x2)) → U3_GA(tree(x0, x1, x2), value_out_ga)
U3_GA(nil, value_out_ga) → U4_GA(nil, left_out_ga(nil))
U3_GA(tree(x0, x1, x2), value_out_ga) → U4_GA(tree(x0, x1, x2), left_out_ga(x0))

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga
value_in_ga(tree(X6, X, X7)) → value_out_ga
left_in_ga(nil) → left_out_ga(nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(L)
right_in_ga(nil) → right_out_ga(nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga
U3_ga(T, value_out_ga) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(L)) → U5_ga(L, right_in_ga(T))
U5_ga(L, right_out_ga(R)) → U6_ga(R, pdl_in_ga(L))
U6_ga(R, pdl_out_ga) → U7_ga(pdl_in_ga(R))
U7_ga(pdl_out_ga) → pdl_out_ga

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1)
U6_ga(x0, x1)
U7_ga(x0)

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

(17) Narrowing (SOUND transformation)

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

U4_GA(nil, left_out_ga(y1)) → U5_GA(y1, right_out_ga(nil))
U4_GA(tree(x0, x1, x2), left_out_ga(y1)) → U5_GA(y1, right_out_ga(x2))

(18) Obligation:

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

U5_GA(L, right_out_ga(R)) → U6_GA(R, pdl_in_ga(L))
U6_GA(R, pdl_out_ga) → PDL_IN_GA(R)
U5_GA(L, right_out_ga(R)) → PDL_IN_GA(L)
PDL_IN_GA(nil) → U3_GA(nil, value_out_ga)
PDL_IN_GA(tree(x0, x1, x2)) → U3_GA(tree(x0, x1, x2), value_out_ga)
U3_GA(nil, value_out_ga) → U4_GA(nil, left_out_ga(nil))
U3_GA(tree(x0, x1, x2), value_out_ga) → U4_GA(tree(x0, x1, x2), left_out_ga(x0))
U4_GA(nil, left_out_ga(y1)) → U5_GA(y1, right_out_ga(nil))
U4_GA(tree(x0, x1, x2), left_out_ga(y1)) → U5_GA(y1, right_out_ga(x2))

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga
value_in_ga(tree(X6, X, X7)) → value_out_ga
left_in_ga(nil) → left_out_ga(nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(L)
right_in_ga(nil) → right_out_ga(nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga
U3_ga(T, value_out_ga) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(L)) → U5_ga(L, right_in_ga(T))
U5_ga(L, right_out_ga(R)) → U6_ga(R, pdl_in_ga(L))
U6_ga(R, pdl_out_ga) → U7_ga(pdl_in_ga(R))
U7_ga(pdl_out_ga) → pdl_out_ga

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1)
U6_ga(x0, x1)
U7_ga(x0)

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

(19) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U4_GA(nil, left_out_ga(y1)) → U5_GA(y1, right_out_ga(nil)) we obtained the following new rules [LPAR04]:

U4_GA(nil, left_out_ga(nil)) → U5_GA(nil, right_out_ga(nil))

(20) Obligation:

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

U5_GA(L, right_out_ga(R)) → U6_GA(R, pdl_in_ga(L))
U6_GA(R, pdl_out_ga) → PDL_IN_GA(R)
U5_GA(L, right_out_ga(R)) → PDL_IN_GA(L)
PDL_IN_GA(nil) → U3_GA(nil, value_out_ga)
PDL_IN_GA(tree(x0, x1, x2)) → U3_GA(tree(x0, x1, x2), value_out_ga)
U3_GA(nil, value_out_ga) → U4_GA(nil, left_out_ga(nil))
U3_GA(tree(x0, x1, x2), value_out_ga) → U4_GA(tree(x0, x1, x2), left_out_ga(x0))
U4_GA(tree(x0, x1, x2), left_out_ga(y1)) → U5_GA(y1, right_out_ga(x2))
U4_GA(nil, left_out_ga(nil)) → U5_GA(nil, right_out_ga(nil))

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga
value_in_ga(tree(X6, X, X7)) → value_out_ga
left_in_ga(nil) → left_out_ga(nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(L)
right_in_ga(nil) → right_out_ga(nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga
U3_ga(T, value_out_ga) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(L)) → U5_ga(L, right_in_ga(T))
U5_ga(L, right_out_ga(R)) → U6_ga(R, pdl_in_ga(L))
U6_ga(R, pdl_out_ga) → U7_ga(pdl_in_ga(R))
U7_ga(pdl_out_ga) → pdl_out_ga

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1)
U6_ga(x0, x1)
U7_ga(x0)

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

(21) Instantiation (EQUIVALENT transformation)

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

U4_GA(tree(z0, z1, z2), left_out_ga(z0)) → U5_GA(z0, right_out_ga(z2))

(22) Obligation:

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

U5_GA(L, right_out_ga(R)) → U6_GA(R, pdl_in_ga(L))
U6_GA(R, pdl_out_ga) → PDL_IN_GA(R)
U5_GA(L, right_out_ga(R)) → PDL_IN_GA(L)
PDL_IN_GA(nil) → U3_GA(nil, value_out_ga)
PDL_IN_GA(tree(x0, x1, x2)) → U3_GA(tree(x0, x1, x2), value_out_ga)
U3_GA(nil, value_out_ga) → U4_GA(nil, left_out_ga(nil))
U3_GA(tree(x0, x1, x2), value_out_ga) → U4_GA(tree(x0, x1, x2), left_out_ga(x0))
U4_GA(nil, left_out_ga(nil)) → U5_GA(nil, right_out_ga(nil))
U4_GA(tree(z0, z1, z2), left_out_ga(z0)) → U5_GA(z0, right_out_ga(z2))

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga
value_in_ga(tree(X6, X, X7)) → value_out_ga
left_in_ga(nil) → left_out_ga(nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(L)
right_in_ga(nil) → right_out_ga(nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga
U3_ga(T, value_out_ga) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(L)) → U5_ga(L, right_in_ga(T))
U5_ga(L, right_out_ga(R)) → U6_ga(R, pdl_in_ga(L))
U6_ga(R, pdl_out_ga) → U7_ga(pdl_in_ga(R))
U7_ga(pdl_out_ga) → pdl_out_ga

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1)
U6_ga(x0, x1)
U7_ga(x0)

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

(23) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

PDL_IN_GA(tree(x0, x1, x2)) → U3_GA(tree(x0, x1, x2), value_out_ga)

The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(U5_GA(x1, x2)) =

0

+

[ 1, 0 ]

·

x1

+

[ 0, 1 ]

·

x2

POL(right_out_ga(x1)) =

/ 0 \ \ 0 /

+

/ 1 0 \ \ 1 0 /

·

x1

POL(U6_GA(x1, x2)) =

0

+

[ 1, 0 ]

·

x1

+

[ 0, 0 ]

·

x2

POL(pdl_in_ga(x1)) =

/ 0 \ \ 1 /

+

/ 0 0 \ \ 0 0 /

·

x1

POL(pdl_out_ga) =

/ 0 \ \ 1 /

POL(PDL_IN_GA(x1)) =

0

+

[ 1, 0 ]

·

x1

POL(nil) =

/ 0 \ \ 0 /

POL(U3_GA(x1, x2)) =

0

+

[ 0, 1 ]

·

x1

+

[ 0, 0 ]

·

x2

POL(value_out_ga) =

/ 1 \ \ 0 /

POL(tree(x1, x2, x3)) =

/ 1 \ \ 0 /

+

/ 1 0 \ \ 1 0 /

·

x1

+

/ 0 0 \ \ 0 0 /

·

x2

+

/ 1 0 \ \ 1 0 /

·

x3

POL(U4_GA(x1, x2)) =

0

+

[ 0, 1 ]

·

x1

+

[ 0, 0 ]

·

x2

POL(left_out_ga(x1)) =

/ 0 \ \ 0 /

+

/ 1 0 \ \ 1 1 /

·

x1

POL(U2_ga(x1)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 0 0 /

·

x1

POL(eq_in_aa) =

/ 0 \ \ 0 /

POL(U3_ga(x1, x2)) =

/ 1 \ \ 1 /

+

/ 0 0 \ \ 1 1 /

·

x1

+

/ 1 1 \ \ 1 1 /

·

x2

POL(value_in_ga(x1)) =

/ 1 \ \ 1 /

+

/ 0 1 \ \ 0 1 /

·

x1

POL(U4_ga(x1, x2)) =

/ 0 \ \ 0 /

+

/ 1 1 \ \ 0 0 /

·

x1

+

/ 1 0 \ \ 0 0 /

·

x2

POL(left_in_ga(x1)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 1 0 /

·

x1

POL(U5_ga(x1, x2)) =

/ 1 \ \ 0 /

+

/ 0 0 \ \ 1 1 /

·

x1

+

/ 1 1 \ \ 0 0 /

·

x2

POL(right_in_ga(x1)) =

/ 1 \ \ 1 /

+

/ 1 0 \ \ 1 0 /

·

x1

POL(U6_ga(x1, x2)) =

/ 0 \ \ 0 /

+

/ 0 0 \ \ 0 0 /

·

x1

+

/ 0 0 \ \ 0 0 /

·

x2

POL(U7_ga(x1)) =

/ 1 \ \ 0 /

+

/ 0 1 \ \ 0 0 /

·

x1

POL(eq_out_aa) =

/ 1 \ \ 0 /

The following usable rules [FROCOS05] were oriented: none

(24) Obligation:

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

U5_GA(L, right_out_ga(R)) → U6_GA(R, pdl_in_ga(L))
U6_GA(R, pdl_out_ga) → PDL_IN_GA(R)
U5_GA(L, right_out_ga(R)) → PDL_IN_GA(L)
PDL_IN_GA(nil) → U3_GA(nil, value_out_ga)
U3_GA(nil, value_out_ga) → U4_GA(nil, left_out_ga(nil))
U3_GA(tree(x0, x1, x2), value_out_ga) → U4_GA(tree(x0, x1, x2), left_out_ga(x0))
U4_GA(nil, left_out_ga(nil)) → U5_GA(nil, right_out_ga(nil))
U4_GA(tree(z0, z1, z2), left_out_ga(z0)) → U5_GA(z0, right_out_ga(z2))

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga
value_in_ga(tree(X6, X, X7)) → value_out_ga
left_in_ga(nil) → left_out_ga(nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(L)
right_in_ga(nil) → right_out_ga(nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga
U3_ga(T, value_out_ga) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(L)) → U5_ga(L, right_in_ga(T))
U5_ga(L, right_out_ga(R)) → U6_ga(R, pdl_in_ga(L))
U6_ga(R, pdl_out_ga) → U7_ga(pdl_in_ga(R))
U7_ga(pdl_out_ga) → pdl_out_ga

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1)
U6_ga(x0, x1)
U7_ga(x0)

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

(25) DependencyGraphProof (EQUIVALENT transformation)

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

(26) Obligation:

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

U6_GA(R, pdl_out_ga) → PDL_IN_GA(R)
PDL_IN_GA(nil) → U3_GA(nil, value_out_ga)
U3_GA(nil, value_out_ga) → U4_GA(nil, left_out_ga(nil))
U4_GA(nil, left_out_ga(nil)) → U5_GA(nil, right_out_ga(nil))
U5_GA(L, right_out_ga(R)) → U6_GA(R, pdl_in_ga(L))
U5_GA(L, right_out_ga(R)) → PDL_IN_GA(L)

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga
value_in_ga(tree(X6, X, X7)) → value_out_ga
left_in_ga(nil) → left_out_ga(nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(L)
right_in_ga(nil) → right_out_ga(nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga
U3_ga(T, value_out_ga) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(L)) → U5_ga(L, right_in_ga(T))
U5_ga(L, right_out_ga(R)) → U6_ga(R, pdl_in_ga(L))
U6_ga(R, pdl_out_ga) → U7_ga(pdl_in_ga(R))
U7_ga(pdl_out_ga) → pdl_out_ga

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1)
U6_ga(x0, x1)
U7_ga(x0)

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

(27) Instantiation (EQUIVALENT transformation)

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

U5_GA(nil, right_out_ga(nil)) → U6_GA(nil, pdl_in_ga(nil))

(28) Obligation:

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

U6_GA(R, pdl_out_ga) → PDL_IN_GA(R)
PDL_IN_GA(nil) → U3_GA(nil, value_out_ga)
U3_GA(nil, value_out_ga) → U4_GA(nil, left_out_ga(nil))
U4_GA(nil, left_out_ga(nil)) → U5_GA(nil, right_out_ga(nil))
U5_GA(L, right_out_ga(R)) → PDL_IN_GA(L)
U5_GA(nil, right_out_ga(nil)) → U6_GA(nil, pdl_in_ga(nil))

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga
value_in_ga(tree(X6, X, X7)) → value_out_ga
left_in_ga(nil) → left_out_ga(nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(L)
right_in_ga(nil) → right_out_ga(nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga
U3_ga(T, value_out_ga) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(L)) → U5_ga(L, right_in_ga(T))
U5_ga(L, right_out_ga(R)) → U6_ga(R, pdl_in_ga(L))
U6_ga(R, pdl_out_ga) → U7_ga(pdl_in_ga(R))
U7_ga(pdl_out_ga) → pdl_out_ga

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1)
U6_ga(x0, x1)
U7_ga(x0)

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

(29) Instantiation (EQUIVALENT transformation)

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

U5_GA(nil, right_out_ga(nil)) → U6_GA(nil, pdl_in_ga(nil))

(30) Obligation:

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

U6_GA(R, pdl_out_ga) → PDL_IN_GA(R)
PDL_IN_GA(nil) → U3_GA(nil, value_out_ga)
U3_GA(nil, value_out_ga) → U4_GA(nil, left_out_ga(nil))
U4_GA(nil, left_out_ga(nil)) → U5_GA(nil, right_out_ga(nil))
U5_GA(L, right_out_ga(R)) → PDL_IN_GA(L)
U5_GA(nil, right_out_ga(nil)) → U6_GA(nil, pdl_in_ga(nil))

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga
value_in_ga(tree(X6, X, X7)) → value_out_ga
left_in_ga(nil) → left_out_ga(nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(L)
right_in_ga(nil) → right_out_ga(nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga
U3_ga(T, value_out_ga) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(L)) → U5_ga(L, right_in_ga(T))
U5_ga(L, right_out_ga(R)) → U6_ga(R, pdl_in_ga(L))
U6_ga(R, pdl_out_ga) → U7_ga(pdl_in_ga(R))
U7_ga(pdl_out_ga) → pdl_out_ga

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1)
U6_ga(x0, x1)
U7_ga(x0)

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

(31) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U6_GA(R, pdl_out_ga) → PDL_IN_GA(R) we obtained the following new rules [LPAR04]:

U6_GA(nil, pdl_out_ga) → PDL_IN_GA(nil)

(32) Obligation:

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

PDL_IN_GA(nil) → U3_GA(nil, value_out_ga)
U3_GA(nil, value_out_ga) → U4_GA(nil, left_out_ga(nil))
U4_GA(nil, left_out_ga(nil)) → U5_GA(nil, right_out_ga(nil))
U5_GA(L, right_out_ga(R)) → PDL_IN_GA(L)
U5_GA(nil, right_out_ga(nil)) → U6_GA(nil, pdl_in_ga(nil))
U6_GA(nil, pdl_out_ga) → PDL_IN_GA(nil)

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga
value_in_ga(tree(X6, X, X7)) → value_out_ga
left_in_ga(nil) → left_out_ga(nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(L)
right_in_ga(nil) → right_out_ga(nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga
U3_ga(T, value_out_ga) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(L)) → U5_ga(L, right_in_ga(T))
U5_ga(L, right_out_ga(R)) → U6_ga(R, pdl_in_ga(L))
U6_ga(R, pdl_out_ga) → U7_ga(pdl_in_ga(R))
U7_ga(pdl_out_ga) → pdl_out_ga

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1)
U6_ga(x0, x1)
U7_ga(x0)

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

(33) Instantiation (EQUIVALENT transformation)

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

U5_GA(nil, right_out_ga(nil)) → PDL_IN_GA(nil)

(34) Obligation:

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

PDL_IN_GA(nil) → U3_GA(nil, value_out_ga)
U3_GA(nil, value_out_ga) → U4_GA(nil, left_out_ga(nil))
U4_GA(nil, left_out_ga(nil)) → U5_GA(nil, right_out_ga(nil))
U5_GA(nil, right_out_ga(nil)) → U6_GA(nil, pdl_in_ga(nil))
U6_GA(nil, pdl_out_ga) → PDL_IN_GA(nil)
U5_GA(nil, right_out_ga(nil)) → PDL_IN_GA(nil)

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga
value_in_ga(tree(X6, X, X7)) → value_out_ga
left_in_ga(nil) → left_out_ga(nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(L)
right_in_ga(nil) → right_out_ga(nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga
U3_ga(T, value_out_ga) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(L)) → U5_ga(L, right_in_ga(T))
U5_ga(L, right_out_ga(R)) → U6_ga(R, pdl_in_ga(L))
U6_ga(R, pdl_out_ga) → U7_ga(pdl_in_ga(R))
U7_ga(pdl_out_ga) → pdl_out_ga

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1)
U6_ga(x0, x1)
U7_ga(x0)

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

(35) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U5_GA(nil, right_out_ga(nil)) → U6_GA(nil, pdl_in_ga(nil)) at position [1] we obtained the following new rules [LPAR04]:

U5_GA(nil, right_out_ga(nil)) → U6_GA(nil, U2_ga(eq_in_aa))
U5_GA(nil, right_out_ga(nil)) → U6_GA(nil, U3_ga(nil, value_in_ga(nil)))

(36) Obligation:

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

PDL_IN_GA(nil) → U3_GA(nil, value_out_ga)
U3_GA(nil, value_out_ga) → U4_GA(nil, left_out_ga(nil))
U4_GA(nil, left_out_ga(nil)) → U5_GA(nil, right_out_ga(nil))
U6_GA(nil, pdl_out_ga) → PDL_IN_GA(nil)
U5_GA(nil, right_out_ga(nil)) → PDL_IN_GA(nil)
U5_GA(nil, right_out_ga(nil)) → U6_GA(nil, U2_ga(eq_in_aa))
U5_GA(nil, right_out_ga(nil)) → U6_GA(nil, U3_ga(nil, value_in_ga(nil)))

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga
value_in_ga(tree(X6, X, X7)) → value_out_ga
left_in_ga(nil) → left_out_ga(nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(L)
right_in_ga(nil) → right_out_ga(nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga
U3_ga(T, value_out_ga) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(L)) → U5_ga(L, right_in_ga(T))
U5_ga(L, right_out_ga(R)) → U6_ga(R, pdl_in_ga(L))
U6_ga(R, pdl_out_ga) → U7_ga(pdl_in_ga(R))
U7_ga(pdl_out_ga) → pdl_out_ga

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1)
U6_ga(x0, x1)
U7_ga(x0)

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

(37) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U5_GA(nil, right_out_ga(nil)) → U6_GA(nil, U2_ga(eq_in_aa)) at position [1,0] we obtained the following new rules [LPAR04]:

U5_GA(nil, right_out_ga(nil)) → U6_GA(nil, U2_ga(eq_out_aa))

(38) Obligation:

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

PDL_IN_GA(nil) → U3_GA(nil, value_out_ga)
U3_GA(nil, value_out_ga) → U4_GA(nil, left_out_ga(nil))
U4_GA(nil, left_out_ga(nil)) → U5_GA(nil, right_out_ga(nil))
U6_GA(nil, pdl_out_ga) → PDL_IN_GA(nil)
U5_GA(nil, right_out_ga(nil)) → PDL_IN_GA(nil)
U5_GA(nil, right_out_ga(nil)) → U6_GA(nil, U3_ga(nil, value_in_ga(nil)))
U5_GA(nil, right_out_ga(nil)) → U6_GA(nil, U2_ga(eq_out_aa))

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga
value_in_ga(tree(X6, X, X7)) → value_out_ga
left_in_ga(nil) → left_out_ga(nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(L)
right_in_ga(nil) → right_out_ga(nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga
U3_ga(T, value_out_ga) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(L)) → U5_ga(L, right_in_ga(T))
U5_ga(L, right_out_ga(R)) → U6_ga(R, pdl_in_ga(L))
U6_ga(R, pdl_out_ga) → U7_ga(pdl_in_ga(R))
U7_ga(pdl_out_ga) → pdl_out_ga

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1)
U6_ga(x0, x1)
U7_ga(x0)

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

(39) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U5_GA(nil, right_out_ga(nil)) → U6_GA(nil, U3_ga(nil, value_in_ga(nil))) at position [1,1] we obtained the following new rules [LPAR04]:

U5_GA(nil, right_out_ga(nil)) → U6_GA(nil, U3_ga(nil, value_out_ga))

(40) Obligation:

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

PDL_IN_GA(nil) → U3_GA(nil, value_out_ga)
U3_GA(nil, value_out_ga) → U4_GA(nil, left_out_ga(nil))
U4_GA(nil, left_out_ga(nil)) → U5_GA(nil, right_out_ga(nil))
U6_GA(nil, pdl_out_ga) → PDL_IN_GA(nil)
U5_GA(nil, right_out_ga(nil)) → PDL_IN_GA(nil)
U5_GA(nil, right_out_ga(nil)) → U6_GA(nil, U2_ga(eq_out_aa))
U5_GA(nil, right_out_ga(nil)) → U6_GA(nil, U3_ga(nil, value_out_ga))

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga
value_in_ga(tree(X6, X, X7)) → value_out_ga
left_in_ga(nil) → left_out_ga(nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(L)
right_in_ga(nil) → right_out_ga(nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga
U3_ga(T, value_out_ga) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(L)) → U5_ga(L, right_in_ga(T))
U5_ga(L, right_out_ga(R)) → U6_ga(R, pdl_in_ga(L))
U6_ga(R, pdl_out_ga) → U7_ga(pdl_in_ga(R))
U7_ga(pdl_out_ga) → pdl_out_ga

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1)
U6_ga(x0, x1)
U7_ga(x0)

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

(41) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U5_GA(nil, right_out_ga(nil)) → U6_GA(nil, U2_ga(eq_out_aa)) at position [1] we obtained the following new rules [LPAR04]:

U5_GA(nil, right_out_ga(nil)) → U6_GA(nil, pdl_out_ga)

(42) Obligation:

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

PDL_IN_GA(nil) → U3_GA(nil, value_out_ga)
U3_GA(nil, value_out_ga) → U4_GA(nil, left_out_ga(nil))
U4_GA(nil, left_out_ga(nil)) → U5_GA(nil, right_out_ga(nil))
U6_GA(nil, pdl_out_ga) → PDL_IN_GA(nil)
U5_GA(nil, right_out_ga(nil)) → PDL_IN_GA(nil)
U5_GA(nil, right_out_ga(nil)) → U6_GA(nil, U3_ga(nil, value_out_ga))
U5_GA(nil, right_out_ga(nil)) → U6_GA(nil, pdl_out_ga)

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga
value_in_ga(tree(X6, X, X7)) → value_out_ga
left_in_ga(nil) → left_out_ga(nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(L)
right_in_ga(nil) → right_out_ga(nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga
U3_ga(T, value_out_ga) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(L)) → U5_ga(L, right_in_ga(T))
U5_ga(L, right_out_ga(R)) → U6_ga(R, pdl_in_ga(L))
U6_ga(R, pdl_out_ga) → U7_ga(pdl_in_ga(R))
U7_ga(pdl_out_ga) → pdl_out_ga

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1)
U6_ga(x0, x1)
U7_ga(x0)

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

(43) 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 = U3_GA(nil, value_out_ga) evaluates to t =U3_GA(nil, value_out_ga)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Semiunifier: [ ]
• Matcher: [ ]

---

Rewriting sequence

U3_GA(nil, value_out_ga) → U4_GA(nil, left_out_ga(nil))
with rule U3_GA(nil, value_out_ga) → U4_GA(nil, left_out_ga(nil)) at position [] and matcher [ ]

U4_GA(nil, left_out_ga(nil)) → U5_GA(nil, right_out_ga(nil))
with rule U4_GA(nil, left_out_ga(nil)) → U5_GA(nil, right_out_ga(nil)) at position [] and matcher [ ]

U5_GA(nil, right_out_ga(nil)) → PDL_IN_GA(nil)
with rule U5_GA(nil, right_out_ga(nil)) → PDL_IN_GA(nil) at position [] and matcher [ ]

PDL_IN_GA(nil) → U3_GA(nil, value_out_ga)
with rule PDL_IN_GA(nil) → U3_GA(nil, value_out_ga)

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.

(44) FALSE

(45) PrologToPiTRSProof (SOUND transformation)

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

preorder_in_ga(X, Y) → U1_ga(X, Y, pdl_in_ga(X, -(Y, [])))
pdl_in_ga(nil, Y) → U2_ga(Y, eq_in_aa(Y, -(X, X)))
eq_in_aa(X, X) → eq_out_aa(X, X)
U2_ga(Y, eq_out_aa(Y, -(X, X))) → pdl_out_ga(nil, Y)
pdl_in_ga(T, -(.(X, Xs), Zs)) → U3_ga(T, X, Xs, Zs, value_in_ga(T, X))
value_in_ga(nil, X5) → value_out_ga(nil, X5)
value_in_ga(tree(X6, X, X7), X) → value_out_ga(tree(X6, X, X7), X)
U3_ga(T, X, Xs, Zs, value_out_ga(T, X)) → U4_ga(T, X, Xs, Zs, left_in_ga(T, L))
left_in_ga(nil, nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2), L) → left_out_ga(tree(L, X1, X2), L)
U4_ga(T, X, Xs, Zs, left_out_ga(T, L)) → U5_ga(T, X, Xs, Zs, L, right_in_ga(T, R))
right_in_ga(nil, nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R), R) → right_out_ga(tree(X3, X4, R), R)
U5_ga(T, X, Xs, Zs, L, right_out_ga(T, R)) → U6_ga(T, X, Xs, Zs, L, R, pdl_in_ga(L, -(Xs, Ys)))
U6_ga(T, X, Xs, Zs, L, R, pdl_out_ga(L, -(Xs, Ys))) → U7_ga(T, X, Xs, Zs, pdl_in_ga(R, -(Ys, Zs)))
U7_ga(T, X, Xs, Zs, pdl_out_ga(R, -(Ys, Zs))) → pdl_out_ga(T, -(.(X, Xs), Zs))
U1_ga(X, Y, pdl_out_ga(X, -(Y, []))) → preorder_out_ga(X, Y)

The argument filtering Pi contains the following mapping:
preorder_in_ga(x1, x2)  =  preorder_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
pdl_in_ga(x1, x2)  =  pdl_in_ga(x1)
nil  =  nil
U2_ga(x1, x2)  =  U2_ga(x2)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
pdl_out_ga(x1, x2)  =  pdl_out_ga(x1)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x5)
value_in_ga(x1, x2)  =  value_in_ga(x1)
value_out_ga(x1, x2)  =  value_out_ga(x1)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x5)
left_in_ga(x1, x2)  =  left_in_ga(x1)
left_out_ga(x1, x2)  =  left_out_ga(x1, x2)
U5_ga(x1, x2, x3, x4, x5, x6)  =  U5_ga(x1, x5, x6)
right_in_ga(x1, x2)  =  right_in_ga(x1)
right_out_ga(x1, x2)  =  right_out_ga(x1, x2)
U6_ga(x1, x2, x3, x4, x5, x6, x7)  =  U6_ga(x1, x6, x7)
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x1, x5)
preorder_out_ga(x1, x2)  =  preorder_out_ga(x1)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(46) Obligation:

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

preorder_in_ga(X, Y) → U1_ga(X, Y, pdl_in_ga(X, -(Y, [])))
pdl_in_ga(nil, Y) → U2_ga(Y, eq_in_aa(Y, -(X, X)))
eq_in_aa(X, X) → eq_out_aa(X, X)
U2_ga(Y, eq_out_aa(Y, -(X, X))) → pdl_out_ga(nil, Y)
pdl_in_ga(T, -(.(X, Xs), Zs)) → U3_ga(T, X, Xs, Zs, value_in_ga(T, X))
value_in_ga(nil, X5) → value_out_ga(nil, X5)
value_in_ga(tree(X6, X, X7), X) → value_out_ga(tree(X6, X, X7), X)
U3_ga(T, X, Xs, Zs, value_out_ga(T, X)) → U4_ga(T, X, Xs, Zs, left_in_ga(T, L))
left_in_ga(nil, nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2), L) → left_out_ga(tree(L, X1, X2), L)
U4_ga(T, X, Xs, Zs, left_out_ga(T, L)) → U5_ga(T, X, Xs, Zs, L, right_in_ga(T, R))
right_in_ga(nil, nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R), R) → right_out_ga(tree(X3, X4, R), R)
U5_ga(T, X, Xs, Zs, L, right_out_ga(T, R)) → U6_ga(T, X, Xs, Zs, L, R, pdl_in_ga(L, -(Xs, Ys)))
U6_ga(T, X, Xs, Zs, L, R, pdl_out_ga(L, -(Xs, Ys))) → U7_ga(T, X, Xs, Zs, pdl_in_ga(R, -(Ys, Zs)))
U7_ga(T, X, Xs, Zs, pdl_out_ga(R, -(Ys, Zs))) → pdl_out_ga(T, -(.(X, Xs), Zs))
U1_ga(X, Y, pdl_out_ga(X, -(Y, []))) → preorder_out_ga(X, Y)

The argument filtering Pi contains the following mapping:
preorder_in_ga(x1, x2)  =  preorder_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
pdl_in_ga(x1, x2)  =  pdl_in_ga(x1)
nil  =  nil
U2_ga(x1, x2)  =  U2_ga(x2)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
pdl_out_ga(x1, x2)  =  pdl_out_ga(x1)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x5)
value_in_ga(x1, x2)  =  value_in_ga(x1)
value_out_ga(x1, x2)  =  value_out_ga(x1)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x5)
left_in_ga(x1, x2)  =  left_in_ga(x1)
left_out_ga(x1, x2)  =  left_out_ga(x1, x2)
U5_ga(x1, x2, x3, x4, x5, x6)  =  U5_ga(x1, x5, x6)
right_in_ga(x1, x2)  =  right_in_ga(x1)
right_out_ga(x1, x2)  =  right_out_ga(x1, x2)
U6_ga(x1, x2, x3, x4, x5, x6, x7)  =  U6_ga(x1, x6, x7)
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x1, x5)
preorder_out_ga(x1, x2)  =  preorder_out_ga(x1)

(47) 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:

PREORDER_IN_GA(X, Y) → U1_GA(X, Y, pdl_in_ga(X, -(Y, [])))
PREORDER_IN_GA(X, Y) → PDL_IN_GA(X, -(Y, []))
PDL_IN_GA(nil, Y) → U2_GA(Y, eq_in_aa(Y, -(X, X)))
PDL_IN_GA(nil, Y) → EQ_IN_AA(Y, -(X, X))
PDL_IN_GA(T, -(.(X, Xs), Zs)) → U3_GA(T, X, Xs, Zs, value_in_ga(T, X))
PDL_IN_GA(T, -(.(X, Xs), Zs)) → VALUE_IN_GA(T, X)
U3_GA(T, X, Xs, Zs, value_out_ga(T, X)) → U4_GA(T, X, Xs, Zs, left_in_ga(T, L))
U3_GA(T, X, Xs, Zs, value_out_ga(T, X)) → LEFT_IN_GA(T, L)
U4_GA(T, X, Xs, Zs, left_out_ga(T, L)) → U5_GA(T, X, Xs, Zs, L, right_in_ga(T, R))
U4_GA(T, X, Xs, Zs, left_out_ga(T, L)) → RIGHT_IN_GA(T, R)
U5_GA(T, X, Xs, Zs, L, right_out_ga(T, R)) → U6_GA(T, X, Xs, Zs, L, R, pdl_in_ga(L, -(Xs, Ys)))
U5_GA(T, X, Xs, Zs, L, right_out_ga(T, R)) → PDL_IN_GA(L, -(Xs, Ys))
U6_GA(T, X, Xs, Zs, L, R, pdl_out_ga(L, -(Xs, Ys))) → U7_GA(T, X, Xs, Zs, pdl_in_ga(R, -(Ys, Zs)))
U6_GA(T, X, Xs, Zs, L, R, pdl_out_ga(L, -(Xs, Ys))) → PDL_IN_GA(R, -(Ys, Zs))

The TRS R consists of the following rules:

preorder_in_ga(X, Y) → U1_ga(X, Y, pdl_in_ga(X, -(Y, [])))
pdl_in_ga(nil, Y) → U2_ga(Y, eq_in_aa(Y, -(X, X)))
eq_in_aa(X, X) → eq_out_aa(X, X)
U2_ga(Y, eq_out_aa(Y, -(X, X))) → pdl_out_ga(nil, Y)
pdl_in_ga(T, -(.(X, Xs), Zs)) → U3_ga(T, X, Xs, Zs, value_in_ga(T, X))
value_in_ga(nil, X5) → value_out_ga(nil, X5)
value_in_ga(tree(X6, X, X7), X) → value_out_ga(tree(X6, X, X7), X)
U3_ga(T, X, Xs, Zs, value_out_ga(T, X)) → U4_ga(T, X, Xs, Zs, left_in_ga(T, L))
left_in_ga(nil, nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2), L) → left_out_ga(tree(L, X1, X2), L)
U4_ga(T, X, Xs, Zs, left_out_ga(T, L)) → U5_ga(T, X, Xs, Zs, L, right_in_ga(T, R))
right_in_ga(nil, nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R), R) → right_out_ga(tree(X3, X4, R), R)
U5_ga(T, X, Xs, Zs, L, right_out_ga(T, R)) → U6_ga(T, X, Xs, Zs, L, R, pdl_in_ga(L, -(Xs, Ys)))
U6_ga(T, X, Xs, Zs, L, R, pdl_out_ga(L, -(Xs, Ys))) → U7_ga(T, X, Xs, Zs, pdl_in_ga(R, -(Ys, Zs)))
U7_ga(T, X, Xs, Zs, pdl_out_ga(R, -(Ys, Zs))) → pdl_out_ga(T, -(.(X, Xs), Zs))
U1_ga(X, Y, pdl_out_ga(X, -(Y, []))) → preorder_out_ga(X, Y)

The argument filtering Pi contains the following mapping:
preorder_in_ga(x1, x2)  =  preorder_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
pdl_in_ga(x1, x2)  =  pdl_in_ga(x1)
nil  =  nil
U2_ga(x1, x2)  =  U2_ga(x2)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
pdl_out_ga(x1, x2)  =  pdl_out_ga(x1)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x5)
value_in_ga(x1, x2)  =  value_in_ga(x1)
value_out_ga(x1, x2)  =  value_out_ga(x1)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x5)
left_in_ga(x1, x2)  =  left_in_ga(x1)
left_out_ga(x1, x2)  =  left_out_ga(x1, x2)
U5_ga(x1, x2, x3, x4, x5, x6)  =  U5_ga(x1, x5, x6)
right_in_ga(x1, x2)  =  right_in_ga(x1)
right_out_ga(x1, x2)  =  right_out_ga(x1, x2)
U6_ga(x1, x2, x3, x4, x5, x6, x7)  =  U6_ga(x1, x6, x7)
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x1, x5)
preorder_out_ga(x1, x2)  =  preorder_out_ga(x1)
PREORDER_IN_GA(x1, x2)  =  PREORDER_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
PDL_IN_GA(x1, x2)  =  PDL_IN_GA(x1)
U2_GA(x1, x2)  =  U2_GA(x2)
EQ_IN_AA(x1, x2)  =  EQ_IN_AA
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x1, x5)
VALUE_IN_GA(x1, x2)  =  VALUE_IN_GA(x1)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x1, x5)
LEFT_IN_GA(x1, x2)  =  LEFT_IN_GA(x1)
U5_GA(x1, x2, x3, x4, x5, x6)  =  U5_GA(x1, x5, x6)
RIGHT_IN_GA(x1, x2)  =  RIGHT_IN_GA(x1)
U6_GA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GA(x1, x6, x7)
U7_GA(x1, x2, x3, x4, x5)  =  U7_GA(x1, x5)

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

(48) Obligation:

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

PREORDER_IN_GA(X, Y) → U1_GA(X, Y, pdl_in_ga(X, -(Y, [])))
PREORDER_IN_GA(X, Y) → PDL_IN_GA(X, -(Y, []))
PDL_IN_GA(nil, Y) → U2_GA(Y, eq_in_aa(Y, -(X, X)))
PDL_IN_GA(nil, Y) → EQ_IN_AA(Y, -(X, X))
PDL_IN_GA(T, -(.(X, Xs), Zs)) → U3_GA(T, X, Xs, Zs, value_in_ga(T, X))
PDL_IN_GA(T, -(.(X, Xs), Zs)) → VALUE_IN_GA(T, X)
U3_GA(T, X, Xs, Zs, value_out_ga(T, X)) → U4_GA(T, X, Xs, Zs, left_in_ga(T, L))
U3_GA(T, X, Xs, Zs, value_out_ga(T, X)) → LEFT_IN_GA(T, L)
U4_GA(T, X, Xs, Zs, left_out_ga(T, L)) → U5_GA(T, X, Xs, Zs, L, right_in_ga(T, R))
U4_GA(T, X, Xs, Zs, left_out_ga(T, L)) → RIGHT_IN_GA(T, R)
U5_GA(T, X, Xs, Zs, L, right_out_ga(T, R)) → U6_GA(T, X, Xs, Zs, L, R, pdl_in_ga(L, -(Xs, Ys)))
U5_GA(T, X, Xs, Zs, L, right_out_ga(T, R)) → PDL_IN_GA(L, -(Xs, Ys))
U6_GA(T, X, Xs, Zs, L, R, pdl_out_ga(L, -(Xs, Ys))) → U7_GA(T, X, Xs, Zs, pdl_in_ga(R, -(Ys, Zs)))
U6_GA(T, X, Xs, Zs, L, R, pdl_out_ga(L, -(Xs, Ys))) → PDL_IN_GA(R, -(Ys, Zs))

The TRS R consists of the following rules:

preorder_in_ga(X, Y) → U1_ga(X, Y, pdl_in_ga(X, -(Y, [])))
pdl_in_ga(nil, Y) → U2_ga(Y, eq_in_aa(Y, -(X, X)))
eq_in_aa(X, X) → eq_out_aa(X, X)
U2_ga(Y, eq_out_aa(Y, -(X, X))) → pdl_out_ga(nil, Y)
pdl_in_ga(T, -(.(X, Xs), Zs)) → U3_ga(T, X, Xs, Zs, value_in_ga(T, X))
value_in_ga(nil, X5) → value_out_ga(nil, X5)
value_in_ga(tree(X6, X, X7), X) → value_out_ga(tree(X6, X, X7), X)
U3_ga(T, X, Xs, Zs, value_out_ga(T, X)) → U4_ga(T, X, Xs, Zs, left_in_ga(T, L))
left_in_ga(nil, nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2), L) → left_out_ga(tree(L, X1, X2), L)
U4_ga(T, X, Xs, Zs, left_out_ga(T, L)) → U5_ga(T, X, Xs, Zs, L, right_in_ga(T, R))
right_in_ga(nil, nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R), R) → right_out_ga(tree(X3, X4, R), R)
U5_ga(T, X, Xs, Zs, L, right_out_ga(T, R)) → U6_ga(T, X, Xs, Zs, L, R, pdl_in_ga(L, -(Xs, Ys)))
U6_ga(T, X, Xs, Zs, L, R, pdl_out_ga(L, -(Xs, Ys))) → U7_ga(T, X, Xs, Zs, pdl_in_ga(R, -(Ys, Zs)))
U7_ga(T, X, Xs, Zs, pdl_out_ga(R, -(Ys, Zs))) → pdl_out_ga(T, -(.(X, Xs), Zs))
U1_ga(X, Y, pdl_out_ga(X, -(Y, []))) → preorder_out_ga(X, Y)

The argument filtering Pi contains the following mapping:
preorder_in_ga(x1, x2)  =  preorder_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
pdl_in_ga(x1, x2)  =  pdl_in_ga(x1)
nil  =  nil
U2_ga(x1, x2)  =  U2_ga(x2)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
pdl_out_ga(x1, x2)  =  pdl_out_ga(x1)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x5)
value_in_ga(x1, x2)  =  value_in_ga(x1)
value_out_ga(x1, x2)  =  value_out_ga(x1)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x5)
left_in_ga(x1, x2)  =  left_in_ga(x1)
left_out_ga(x1, x2)  =  left_out_ga(x1, x2)
U5_ga(x1, x2, x3, x4, x5, x6)  =  U5_ga(x1, x5, x6)
right_in_ga(x1, x2)  =  right_in_ga(x1)
right_out_ga(x1, x2)  =  right_out_ga(x1, x2)
U6_ga(x1, x2, x3, x4, x5, x6, x7)  =  U6_ga(x1, x6, x7)
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x1, x5)
preorder_out_ga(x1, x2)  =  preorder_out_ga(x1)
PREORDER_IN_GA(x1, x2)  =  PREORDER_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
PDL_IN_GA(x1, x2)  =  PDL_IN_GA(x1)
U2_GA(x1, x2)  =  U2_GA(x2)
EQ_IN_AA(x1, x2)  =  EQ_IN_AA
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x1, x5)
VALUE_IN_GA(x1, x2)  =  VALUE_IN_GA(x1)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x1, x5)
LEFT_IN_GA(x1, x2)  =  LEFT_IN_GA(x1)
U5_GA(x1, x2, x3, x4, x5, x6)  =  U5_GA(x1, x5, x6)
RIGHT_IN_GA(x1, x2)  =  RIGHT_IN_GA(x1)
U6_GA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GA(x1, x6, x7)
U7_GA(x1, x2, x3, x4, x5)  =  U7_GA(x1, x5)

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

(49) DependencyGraphProof (EQUIVALENT transformation)

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

(50) Obligation:

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

PDL_IN_GA(T, -(.(X, Xs), Zs)) → U3_GA(T, X, Xs, Zs, value_in_ga(T, X))
U3_GA(T, X, Xs, Zs, value_out_ga(T, X)) → U4_GA(T, X, Xs, Zs, left_in_ga(T, L))
U4_GA(T, X, Xs, Zs, left_out_ga(T, L)) → U5_GA(T, X, Xs, Zs, L, right_in_ga(T, R))
U5_GA(T, X, Xs, Zs, L, right_out_ga(T, R)) → U6_GA(T, X, Xs, Zs, L, R, pdl_in_ga(L, -(Xs, Ys)))
U6_GA(T, X, Xs, Zs, L, R, pdl_out_ga(L, -(Xs, Ys))) → PDL_IN_GA(R, -(Ys, Zs))
U5_GA(T, X, Xs, Zs, L, right_out_ga(T, R)) → PDL_IN_GA(L, -(Xs, Ys))

The TRS R consists of the following rules:

preorder_in_ga(X, Y) → U1_ga(X, Y, pdl_in_ga(X, -(Y, [])))
pdl_in_ga(nil, Y) → U2_ga(Y, eq_in_aa(Y, -(X, X)))
eq_in_aa(X, X) → eq_out_aa(X, X)
U2_ga(Y, eq_out_aa(Y, -(X, X))) → pdl_out_ga(nil, Y)
pdl_in_ga(T, -(.(X, Xs), Zs)) → U3_ga(T, X, Xs, Zs, value_in_ga(T, X))
value_in_ga(nil, X5) → value_out_ga(nil, X5)
value_in_ga(tree(X6, X, X7), X) → value_out_ga(tree(X6, X, X7), X)
U3_ga(T, X, Xs, Zs, value_out_ga(T, X)) → U4_ga(T, X, Xs, Zs, left_in_ga(T, L))
left_in_ga(nil, nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2), L) → left_out_ga(tree(L, X1, X2), L)
U4_ga(T, X, Xs, Zs, left_out_ga(T, L)) → U5_ga(T, X, Xs, Zs, L, right_in_ga(T, R))
right_in_ga(nil, nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R), R) → right_out_ga(tree(X3, X4, R), R)
U5_ga(T, X, Xs, Zs, L, right_out_ga(T, R)) → U6_ga(T, X, Xs, Zs, L, R, pdl_in_ga(L, -(Xs, Ys)))
U6_ga(T, X, Xs, Zs, L, R, pdl_out_ga(L, -(Xs, Ys))) → U7_ga(T, X, Xs, Zs, pdl_in_ga(R, -(Ys, Zs)))
U7_ga(T, X, Xs, Zs, pdl_out_ga(R, -(Ys, Zs))) → pdl_out_ga(T, -(.(X, Xs), Zs))
U1_ga(X, Y, pdl_out_ga(X, -(Y, []))) → preorder_out_ga(X, Y)

The argument filtering Pi contains the following mapping:
preorder_in_ga(x1, x2)  =  preorder_in_ga(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
pdl_in_ga(x1, x2)  =  pdl_in_ga(x1)
nil  =  nil
U2_ga(x1, x2)  =  U2_ga(x2)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
pdl_out_ga(x1, x2)  =  pdl_out_ga(x1)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x5)
value_in_ga(x1, x2)  =  value_in_ga(x1)
value_out_ga(x1, x2)  =  value_out_ga(x1)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x5)
left_in_ga(x1, x2)  =  left_in_ga(x1)
left_out_ga(x1, x2)  =  left_out_ga(x1, x2)
U5_ga(x1, x2, x3, x4, x5, x6)  =  U5_ga(x1, x5, x6)
right_in_ga(x1, x2)  =  right_in_ga(x1)
right_out_ga(x1, x2)  =  right_out_ga(x1, x2)
U6_ga(x1, x2, x3, x4, x5, x6, x7)  =  U6_ga(x1, x6, x7)
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x1, x5)
preorder_out_ga(x1, x2)  =  preorder_out_ga(x1)
PDL_IN_GA(x1, x2)  =  PDL_IN_GA(x1)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x1, x5)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x1, x5)
U5_GA(x1, x2, x3, x4, x5, x6)  =  U5_GA(x1, x5, x6)
U6_GA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GA(x1, x6, x7)

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

(51) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(52) Obligation:

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

PDL_IN_GA(T, -(.(X, Xs), Zs)) → U3_GA(T, X, Xs, Zs, value_in_ga(T, X))
U3_GA(T, X, Xs, Zs, value_out_ga(T, X)) → U4_GA(T, X, Xs, Zs, left_in_ga(T, L))
U4_GA(T, X, Xs, Zs, left_out_ga(T, L)) → U5_GA(T, X, Xs, Zs, L, right_in_ga(T, R))
U5_GA(T, X, Xs, Zs, L, right_out_ga(T, R)) → U6_GA(T, X, Xs, Zs, L, R, pdl_in_ga(L, -(Xs, Ys)))
U6_GA(T, X, Xs, Zs, L, R, pdl_out_ga(L, -(Xs, Ys))) → PDL_IN_GA(R, -(Ys, Zs))
U5_GA(T, X, Xs, Zs, L, right_out_ga(T, R)) → PDL_IN_GA(L, -(Xs, Ys))

The TRS R consists of the following rules:

value_in_ga(nil, X5) → value_out_ga(nil, X5)
value_in_ga(tree(X6, X, X7), X) → value_out_ga(tree(X6, X, X7), X)
left_in_ga(nil, nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2), L) → left_out_ga(tree(L, X1, X2), L)
right_in_ga(nil, nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R), R) → right_out_ga(tree(X3, X4, R), R)
pdl_in_ga(nil, Y) → U2_ga(Y, eq_in_aa(Y, -(X, X)))
pdl_in_ga(T, -(.(X, Xs), Zs)) → U3_ga(T, X, Xs, Zs, value_in_ga(T, X))
U2_ga(Y, eq_out_aa(Y, -(X, X))) → pdl_out_ga(nil, Y)
U3_ga(T, X, Xs, Zs, value_out_ga(T, X)) → U4_ga(T, X, Xs, Zs, left_in_ga(T, L))
eq_in_aa(X, X) → eq_out_aa(X, X)
U4_ga(T, X, Xs, Zs, left_out_ga(T, L)) → U5_ga(T, X, Xs, Zs, L, right_in_ga(T, R))
U5_ga(T, X, Xs, Zs, L, right_out_ga(T, R)) → U6_ga(T, X, Xs, Zs, L, R, pdl_in_ga(L, -(Xs, Ys)))
U6_ga(T, X, Xs, Zs, L, R, pdl_out_ga(L, -(Xs, Ys))) → U7_ga(T, X, Xs, Zs, pdl_in_ga(R, -(Ys, Zs)))
U7_ga(T, X, Xs, Zs, pdl_out_ga(R, -(Ys, Zs))) → pdl_out_ga(T, -(.(X, Xs), Zs))

The argument filtering Pi contains the following mapping:
pdl_in_ga(x1, x2)  =  pdl_in_ga(x1)
nil  =  nil
U2_ga(x1, x2)  =  U2_ga(x2)
eq_in_aa(x1, x2)  =  eq_in_aa
eq_out_aa(x1, x2)  =  eq_out_aa
pdl_out_ga(x1, x2)  =  pdl_out_ga(x1)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x5)
value_in_ga(x1, x2)  =  value_in_ga(x1)
value_out_ga(x1, x2)  =  value_out_ga(x1)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x5)
left_in_ga(x1, x2)  =  left_in_ga(x1)
left_out_ga(x1, x2)  =  left_out_ga(x1, x2)
U5_ga(x1, x2, x3, x4, x5, x6)  =  U5_ga(x1, x5, x6)
right_in_ga(x1, x2)  =  right_in_ga(x1)
right_out_ga(x1, x2)  =  right_out_ga(x1, x2)
U6_ga(x1, x2, x3, x4, x5, x6, x7)  =  U6_ga(x1, x6, x7)
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x1, x5)
PDL_IN_GA(x1, x2)  =  PDL_IN_GA(x1)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x1, x5)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x1, x5)
U5_GA(x1, x2, x3, x4, x5, x6)  =  U5_GA(x1, x5, x6)
U6_GA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GA(x1, x6, x7)

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

(53) PiDPToQDPProof (SOUND transformation)

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

(54) Obligation:

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

PDL_IN_GA(T) → U3_GA(T, value_in_ga(T))
U3_GA(T, value_out_ga(T)) → U4_GA(T, left_in_ga(T))
U4_GA(T, left_out_ga(T, L)) → U5_GA(T, L, right_in_ga(T))
U5_GA(T, L, right_out_ga(T, R)) → U6_GA(T, R, pdl_in_ga(L))
U6_GA(T, R, pdl_out_ga(L)) → PDL_IN_GA(R)
U5_GA(T, L, right_out_ga(T, R)) → PDL_IN_GA(L)

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga(nil)
value_in_ga(tree(X6, X, X7)) → value_out_ga(tree(X6, X, X7))
left_in_ga(nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(tree(L, X1, X2), L)
right_in_ga(nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga(nil)
U3_ga(T, value_out_ga(T)) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(T, L)) → U5_ga(T, L, right_in_ga(T))
U5_ga(T, L, right_out_ga(T, R)) → U6_ga(T, R, pdl_in_ga(L))
U6_ga(T, R, pdl_out_ga(L)) → U7_ga(T, pdl_in_ga(R))
U7_ga(T, pdl_out_ga(R)) → pdl_out_ga(T)

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1, x2)
U6_ga(x0, x1, x2)
U7_ga(x0, x1)

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

(55) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule PDL_IN_GA(T) → U3_GA(T, value_in_ga(T)) at position [1] we obtained the following new rules [LPAR04]:

PDL_IN_GA(nil) → U3_GA(nil, value_out_ga(nil))
PDL_IN_GA(tree(x0, x1, x2)) → U3_GA(tree(x0, x1, x2), value_out_ga(tree(x0, x1, x2)))

(56) Obligation:

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

U3_GA(T, value_out_ga(T)) → U4_GA(T, left_in_ga(T))
U4_GA(T, left_out_ga(T, L)) → U5_GA(T, L, right_in_ga(T))
U5_GA(T, L, right_out_ga(T, R)) → U6_GA(T, R, pdl_in_ga(L))
U6_GA(T, R, pdl_out_ga(L)) → PDL_IN_GA(R)
U5_GA(T, L, right_out_ga(T, R)) → PDL_IN_GA(L)
PDL_IN_GA(nil) → U3_GA(nil, value_out_ga(nil))
PDL_IN_GA(tree(x0, x1, x2)) → U3_GA(tree(x0, x1, x2), value_out_ga(tree(x0, x1, x2)))

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga(nil)
value_in_ga(tree(X6, X, X7)) → value_out_ga(tree(X6, X, X7))
left_in_ga(nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(tree(L, X1, X2), L)
right_in_ga(nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga(nil)
U3_ga(T, value_out_ga(T)) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(T, L)) → U5_ga(T, L, right_in_ga(T))
U5_ga(T, L, right_out_ga(T, R)) → U6_ga(T, R, pdl_in_ga(L))
U6_ga(T, R, pdl_out_ga(L)) → U7_ga(T, pdl_in_ga(R))
U7_ga(T, pdl_out_ga(R)) → pdl_out_ga(T)

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1, x2)
U6_ga(x0, x1, x2)
U7_ga(x0, x1)

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

(57) Narrowing (SOUND transformation)

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

U3_GA(nil, value_out_ga(nil)) → U4_GA(nil, left_out_ga(nil, nil))
U3_GA(tree(x0, x1, x2), value_out_ga(tree(x0, x1, x2))) → U4_GA(tree(x0, x1, x2), left_out_ga(tree(x0, x1, x2), x0))

(58) Obligation:

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

U4_GA(T, left_out_ga(T, L)) → U5_GA(T, L, right_in_ga(T))
U5_GA(T, L, right_out_ga(T, R)) → U6_GA(T, R, pdl_in_ga(L))
U6_GA(T, R, pdl_out_ga(L)) → PDL_IN_GA(R)
U5_GA(T, L, right_out_ga(T, R)) → PDL_IN_GA(L)
PDL_IN_GA(nil) → U3_GA(nil, value_out_ga(nil))
PDL_IN_GA(tree(x0, x1, x2)) → U3_GA(tree(x0, x1, x2), value_out_ga(tree(x0, x1, x2)))
U3_GA(nil, value_out_ga(nil)) → U4_GA(nil, left_out_ga(nil, nil))
U3_GA(tree(x0, x1, x2), value_out_ga(tree(x0, x1, x2))) → U4_GA(tree(x0, x1, x2), left_out_ga(tree(x0, x1, x2), x0))

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga(nil)
value_in_ga(tree(X6, X, X7)) → value_out_ga(tree(X6, X, X7))
left_in_ga(nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(tree(L, X1, X2), L)
right_in_ga(nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga(nil)
U3_ga(T, value_out_ga(T)) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(T, L)) → U5_ga(T, L, right_in_ga(T))
U5_ga(T, L, right_out_ga(T, R)) → U6_ga(T, R, pdl_in_ga(L))
U6_ga(T, R, pdl_out_ga(L)) → U7_ga(T, pdl_in_ga(R))
U7_ga(T, pdl_out_ga(R)) → pdl_out_ga(T)

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1, x2)
U6_ga(x0, x1, x2)
U7_ga(x0, x1)

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

(59) Narrowing (SOUND transformation)

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

U4_GA(nil, left_out_ga(nil, y1)) → U5_GA(nil, y1, right_out_ga(nil, nil))
U4_GA(tree(x0, x1, x2), left_out_ga(tree(x0, x1, x2), y1)) → U5_GA(tree(x0, x1, x2), y1, right_out_ga(tree(x0, x1, x2), x2))

(60) Obligation:

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

U5_GA(T, L, right_out_ga(T, R)) → U6_GA(T, R, pdl_in_ga(L))
U6_GA(T, R, pdl_out_ga(L)) → PDL_IN_GA(R)
U5_GA(T, L, right_out_ga(T, R)) → PDL_IN_GA(L)
PDL_IN_GA(nil) → U3_GA(nil, value_out_ga(nil))
PDL_IN_GA(tree(x0, x1, x2)) → U3_GA(tree(x0, x1, x2), value_out_ga(tree(x0, x1, x2)))
U3_GA(nil, value_out_ga(nil)) → U4_GA(nil, left_out_ga(nil, nil))
U3_GA(tree(x0, x1, x2), value_out_ga(tree(x0, x1, x2))) → U4_GA(tree(x0, x1, x2), left_out_ga(tree(x0, x1, x2), x0))
U4_GA(nil, left_out_ga(nil, y1)) → U5_GA(nil, y1, right_out_ga(nil, nil))
U4_GA(tree(x0, x1, x2), left_out_ga(tree(x0, x1, x2), y1)) → U5_GA(tree(x0, x1, x2), y1, right_out_ga(tree(x0, x1, x2), x2))

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga(nil)
value_in_ga(tree(X6, X, X7)) → value_out_ga(tree(X6, X, X7))
left_in_ga(nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(tree(L, X1, X2), L)
right_in_ga(nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga(nil)
U3_ga(T, value_out_ga(T)) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(T, L)) → U5_ga(T, L, right_in_ga(T))
U5_ga(T, L, right_out_ga(T, R)) → U6_ga(T, R, pdl_in_ga(L))
U6_ga(T, R, pdl_out_ga(L)) → U7_ga(T, pdl_in_ga(R))
U7_ga(T, pdl_out_ga(R)) → pdl_out_ga(T)

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1, x2)
U6_ga(x0, x1, x2)
U7_ga(x0, x1)

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

(61) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U4_GA(nil, left_out_ga(nil, y1)) → U5_GA(nil, y1, right_out_ga(nil, nil)) we obtained the following new rules [LPAR04]:

U4_GA(nil, left_out_ga(nil, nil)) → U5_GA(nil, nil, right_out_ga(nil, nil))

(62) Obligation:

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

U5_GA(T, L, right_out_ga(T, R)) → U6_GA(T, R, pdl_in_ga(L))
U6_GA(T, R, pdl_out_ga(L)) → PDL_IN_GA(R)
U5_GA(T, L, right_out_ga(T, R)) → PDL_IN_GA(L)
PDL_IN_GA(nil) → U3_GA(nil, value_out_ga(nil))
PDL_IN_GA(tree(x0, x1, x2)) → U3_GA(tree(x0, x1, x2), value_out_ga(tree(x0, x1, x2)))
U3_GA(nil, value_out_ga(nil)) → U4_GA(nil, left_out_ga(nil, nil))
U3_GA(tree(x0, x1, x2), value_out_ga(tree(x0, x1, x2))) → U4_GA(tree(x0, x1, x2), left_out_ga(tree(x0, x1, x2), x0))
U4_GA(tree(x0, x1, x2), left_out_ga(tree(x0, x1, x2), y1)) → U5_GA(tree(x0, x1, x2), y1, right_out_ga(tree(x0, x1, x2), x2))
U4_GA(nil, left_out_ga(nil, nil)) → U5_GA(nil, nil, right_out_ga(nil, nil))

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga(nil)
value_in_ga(tree(X6, X, X7)) → value_out_ga(tree(X6, X, X7))
left_in_ga(nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(tree(L, X1, X2), L)
right_in_ga(nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga(nil)
U3_ga(T, value_out_ga(T)) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(T, L)) → U5_ga(T, L, right_in_ga(T))
U5_ga(T, L, right_out_ga(T, R)) → U6_ga(T, R, pdl_in_ga(L))
U6_ga(T, R, pdl_out_ga(L)) → U7_ga(T, pdl_in_ga(R))
U7_ga(T, pdl_out_ga(R)) → pdl_out_ga(T)

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1, x2)
U6_ga(x0, x1, x2)
U7_ga(x0, x1)

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

(63) Instantiation (EQUIVALENT transformation)

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

U4_GA(tree(z0, z1, z2), left_out_ga(tree(z0, z1, z2), z0)) → U5_GA(tree(z0, z1, z2), z0, right_out_ga(tree(z0, z1, z2), z2))

(64) Obligation:

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

U5_GA(T, L, right_out_ga(T, R)) → U6_GA(T, R, pdl_in_ga(L))
U6_GA(T, R, pdl_out_ga(L)) → PDL_IN_GA(R)
U5_GA(T, L, right_out_ga(T, R)) → PDL_IN_GA(L)
PDL_IN_GA(nil) → U3_GA(nil, value_out_ga(nil))
PDL_IN_GA(tree(x0, x1, x2)) → U3_GA(tree(x0, x1, x2), value_out_ga(tree(x0, x1, x2)))
U3_GA(nil, value_out_ga(nil)) → U4_GA(nil, left_out_ga(nil, nil))
U3_GA(tree(x0, x1, x2), value_out_ga(tree(x0, x1, x2))) → U4_GA(tree(x0, x1, x2), left_out_ga(tree(x0, x1, x2), x0))
U4_GA(nil, left_out_ga(nil, nil)) → U5_GA(nil, nil, right_out_ga(nil, nil))
U4_GA(tree(z0, z1, z2), left_out_ga(tree(z0, z1, z2), z0)) → U5_GA(tree(z0, z1, z2), z0, right_out_ga(tree(z0, z1, z2), z2))

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga(nil)
value_in_ga(tree(X6, X, X7)) → value_out_ga(tree(X6, X, X7))
left_in_ga(nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(tree(L, X1, X2), L)
right_in_ga(nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga(nil)
U3_ga(T, value_out_ga(T)) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(T, L)) → U5_ga(T, L, right_in_ga(T))
U5_ga(T, L, right_out_ga(T, R)) → U6_ga(T, R, pdl_in_ga(L))
U6_ga(T, R, pdl_out_ga(L)) → U7_ga(T, pdl_in_ga(R))
U7_ga(T, pdl_out_ga(R)) → pdl_out_ga(T)

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1, x2)
U6_ga(x0, x1, x2)
U7_ga(x0, x1)

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

(65) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

U4_GA(tree(z0, z1, z2), left_out_ga(tree(z0, z1, z2), z0)) → U5_GA(tree(z0, z1, z2), z0, right_out_ga(tree(z0, z1, z2), z2))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(PDL_IN_GA(x₁)) = x₁   
POL(U2_ga(x₁)) = 0   
POL(U3_GA(x₁, x₂)) = x₁   
POL(U3_ga(x₁, x₂)) = 0   
POL(U4_GA(x₁, x₂)) = x₁   
POL(U4_ga(x₁, x₂)) = 0   
POL(U5_GA(x₁, x₂, x₃)) = x₂ + x₃   
POL(U5_ga(x₁, x₂, x₃)) = 0   
POL(U6_GA(x₁, x₂, x₃)) = x₂   
POL(U6_ga(x₁, x₂, x₃)) = 0   
POL(U7_ga(x₁, x₂)) = 0   
POL(eq_in_aa) = 0   
POL(eq_out_aa) = 0   
POL(left_in_ga(x₁)) = 1   
POL(left_out_ga(x₁, x₂)) = 0   
POL(nil) = 0   
POL(pdl_in_ga(x₁)) = 0   
POL(pdl_out_ga(x₁)) = 0   
POL(right_in_ga(x₁)) = 0   
POL(right_out_ga(x₁, x₂)) = x₂   
POL(tree(x₁, x₂, x₃)) = 1 + x₁ + x₃   
POL(value_in_ga(x₁)) = 0   
POL(value_out_ga(x₁)) = 0   

The following usable rules [FROCOS05] were oriented: none

(66) Obligation:

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

U5_GA(T, L, right_out_ga(T, R)) → U6_GA(T, R, pdl_in_ga(L))
U6_GA(T, R, pdl_out_ga(L)) → PDL_IN_GA(R)
U5_GA(T, L, right_out_ga(T, R)) → PDL_IN_GA(L)
PDL_IN_GA(nil) → U3_GA(nil, value_out_ga(nil))
PDL_IN_GA(tree(x0, x1, x2)) → U3_GA(tree(x0, x1, x2), value_out_ga(tree(x0, x1, x2)))
U3_GA(nil, value_out_ga(nil)) → U4_GA(nil, left_out_ga(nil, nil))
U3_GA(tree(x0, x1, x2), value_out_ga(tree(x0, x1, x2))) → U4_GA(tree(x0, x1, x2), left_out_ga(tree(x0, x1, x2), x0))
U4_GA(nil, left_out_ga(nil, nil)) → U5_GA(nil, nil, right_out_ga(nil, nil))

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga(nil)
value_in_ga(tree(X6, X, X7)) → value_out_ga(tree(X6, X, X7))
left_in_ga(nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(tree(L, X1, X2), L)
right_in_ga(nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga(nil)
U3_ga(T, value_out_ga(T)) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(T, L)) → U5_ga(T, L, right_in_ga(T))
U5_ga(T, L, right_out_ga(T, R)) → U6_ga(T, R, pdl_in_ga(L))
U6_ga(T, R, pdl_out_ga(L)) → U7_ga(T, pdl_in_ga(R))
U7_ga(T, pdl_out_ga(R)) → pdl_out_ga(T)

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1, x2)
U6_ga(x0, x1, x2)
U7_ga(x0, x1)

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

(67) DependencyGraphProof (EQUIVALENT transformation)

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

(68) Obligation:

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

U6_GA(T, R, pdl_out_ga(L)) → PDL_IN_GA(R)
PDL_IN_GA(nil) → U3_GA(nil, value_out_ga(nil))
U3_GA(nil, value_out_ga(nil)) → U4_GA(nil, left_out_ga(nil, nil))
U4_GA(nil, left_out_ga(nil, nil)) → U5_GA(nil, nil, right_out_ga(nil, nil))
U5_GA(T, L, right_out_ga(T, R)) → U6_GA(T, R, pdl_in_ga(L))
U5_GA(T, L, right_out_ga(T, R)) → PDL_IN_GA(L)

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga(nil)
value_in_ga(tree(X6, X, X7)) → value_out_ga(tree(X6, X, X7))
left_in_ga(nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(tree(L, X1, X2), L)
right_in_ga(nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga(nil)
U3_ga(T, value_out_ga(T)) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(T, L)) → U5_ga(T, L, right_in_ga(T))
U5_ga(T, L, right_out_ga(T, R)) → U6_ga(T, R, pdl_in_ga(L))
U6_ga(T, R, pdl_out_ga(L)) → U7_ga(T, pdl_in_ga(R))
U7_ga(T, pdl_out_ga(R)) → pdl_out_ga(T)

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1, x2)
U6_ga(x0, x1, x2)
U7_ga(x0, x1)

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

(69) Instantiation (EQUIVALENT transformation)

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

U5_GA(nil, nil, right_out_ga(nil, nil)) → U6_GA(nil, nil, pdl_in_ga(nil))

(70) Obligation:

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

U6_GA(T, R, pdl_out_ga(L)) → PDL_IN_GA(R)
PDL_IN_GA(nil) → U3_GA(nil, value_out_ga(nil))
U3_GA(nil, value_out_ga(nil)) → U4_GA(nil, left_out_ga(nil, nil))
U4_GA(nil, left_out_ga(nil, nil)) → U5_GA(nil, nil, right_out_ga(nil, nil))
U5_GA(T, L, right_out_ga(T, R)) → PDL_IN_GA(L)
U5_GA(nil, nil, right_out_ga(nil, nil)) → U6_GA(nil, nil, pdl_in_ga(nil))

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga(nil)
value_in_ga(tree(X6, X, X7)) → value_out_ga(tree(X6, X, X7))
left_in_ga(nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(tree(L, X1, X2), L)
right_in_ga(nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga(nil)
U3_ga(T, value_out_ga(T)) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(T, L)) → U5_ga(T, L, right_in_ga(T))
U5_ga(T, L, right_out_ga(T, R)) → U6_ga(T, R, pdl_in_ga(L))
U6_ga(T, R, pdl_out_ga(L)) → U7_ga(T, pdl_in_ga(R))
U7_ga(T, pdl_out_ga(R)) → pdl_out_ga(T)

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1, x2)
U6_ga(x0, x1, x2)
U7_ga(x0, x1)

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

(71) Instantiation (EQUIVALENT transformation)

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

U5_GA(nil, nil, right_out_ga(nil, nil)) → U6_GA(nil, nil, pdl_in_ga(nil))

(72) Obligation:

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

U6_GA(T, R, pdl_out_ga(L)) → PDL_IN_GA(R)
PDL_IN_GA(nil) → U3_GA(nil, value_out_ga(nil))
U3_GA(nil, value_out_ga(nil)) → U4_GA(nil, left_out_ga(nil, nil))
U4_GA(nil, left_out_ga(nil, nil)) → U5_GA(nil, nil, right_out_ga(nil, nil))
U5_GA(T, L, right_out_ga(T, R)) → PDL_IN_GA(L)
U5_GA(nil, nil, right_out_ga(nil, nil)) → U6_GA(nil, nil, pdl_in_ga(nil))

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga(nil)
value_in_ga(tree(X6, X, X7)) → value_out_ga(tree(X6, X, X7))
left_in_ga(nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(tree(L, X1, X2), L)
right_in_ga(nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga(nil)
U3_ga(T, value_out_ga(T)) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(T, L)) → U5_ga(T, L, right_in_ga(T))
U5_ga(T, L, right_out_ga(T, R)) → U6_ga(T, R, pdl_in_ga(L))
U6_ga(T, R, pdl_out_ga(L)) → U7_ga(T, pdl_in_ga(R))
U7_ga(T, pdl_out_ga(R)) → pdl_out_ga(T)

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1, x2)
U6_ga(x0, x1, x2)
U7_ga(x0, x1)

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

(73) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U6_GA(T, R, pdl_out_ga(L)) → PDL_IN_GA(R) we obtained the following new rules [LPAR04]:

U6_GA(nil, nil, pdl_out_ga(x2)) → PDL_IN_GA(nil)

(74) Obligation:

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

PDL_IN_GA(nil) → U3_GA(nil, value_out_ga(nil))
U3_GA(nil, value_out_ga(nil)) → U4_GA(nil, left_out_ga(nil, nil))
U4_GA(nil, left_out_ga(nil, nil)) → U5_GA(nil, nil, right_out_ga(nil, nil))
U5_GA(T, L, right_out_ga(T, R)) → PDL_IN_GA(L)
U5_GA(nil, nil, right_out_ga(nil, nil)) → U6_GA(nil, nil, pdl_in_ga(nil))
U6_GA(nil, nil, pdl_out_ga(x2)) → PDL_IN_GA(nil)

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga(nil)
value_in_ga(tree(X6, X, X7)) → value_out_ga(tree(X6, X, X7))
left_in_ga(nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(tree(L, X1, X2), L)
right_in_ga(nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga(nil)
U3_ga(T, value_out_ga(T)) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(T, L)) → U5_ga(T, L, right_in_ga(T))
U5_ga(T, L, right_out_ga(T, R)) → U6_ga(T, R, pdl_in_ga(L))
U6_ga(T, R, pdl_out_ga(L)) → U7_ga(T, pdl_in_ga(R))
U7_ga(T, pdl_out_ga(R)) → pdl_out_ga(T)

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1, x2)
U6_ga(x0, x1, x2)
U7_ga(x0, x1)

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

(75) Instantiation (EQUIVALENT transformation)

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

U5_GA(nil, nil, right_out_ga(nil, nil)) → PDL_IN_GA(nil)

(76) Obligation:

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

PDL_IN_GA(nil) → U3_GA(nil, value_out_ga(nil))
U3_GA(nil, value_out_ga(nil)) → U4_GA(nil, left_out_ga(nil, nil))
U4_GA(nil, left_out_ga(nil, nil)) → U5_GA(nil, nil, right_out_ga(nil, nil))
U5_GA(nil, nil, right_out_ga(nil, nil)) → U6_GA(nil, nil, pdl_in_ga(nil))
U6_GA(nil, nil, pdl_out_ga(x2)) → PDL_IN_GA(nil)
U5_GA(nil, nil, right_out_ga(nil, nil)) → PDL_IN_GA(nil)

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga(nil)
value_in_ga(tree(X6, X, X7)) → value_out_ga(tree(X6, X, X7))
left_in_ga(nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(tree(L, X1, X2), L)
right_in_ga(nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga(nil)
U3_ga(T, value_out_ga(T)) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(T, L)) → U5_ga(T, L, right_in_ga(T))
U5_ga(T, L, right_out_ga(T, R)) → U6_ga(T, R, pdl_in_ga(L))
U6_ga(T, R, pdl_out_ga(L)) → U7_ga(T, pdl_in_ga(R))
U7_ga(T, pdl_out_ga(R)) → pdl_out_ga(T)

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1, x2)
U6_ga(x0, x1, x2)
U7_ga(x0, x1)

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

(77) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U5_GA(nil, nil, right_out_ga(nil, nil)) → U6_GA(nil, nil, pdl_in_ga(nil)) at position [2] we obtained the following new rules [LPAR04]:

U5_GA(nil, nil, right_out_ga(nil, nil)) → U6_GA(nil, nil, U2_ga(eq_in_aa))
U5_GA(nil, nil, right_out_ga(nil, nil)) → U6_GA(nil, nil, U3_ga(nil, value_in_ga(nil)))

(78) Obligation:

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

PDL_IN_GA(nil) → U3_GA(nil, value_out_ga(nil))
U3_GA(nil, value_out_ga(nil)) → U4_GA(nil, left_out_ga(nil, nil))
U4_GA(nil, left_out_ga(nil, nil)) → U5_GA(nil, nil, right_out_ga(nil, nil))
U6_GA(nil, nil, pdl_out_ga(x2)) → PDL_IN_GA(nil)
U5_GA(nil, nil, right_out_ga(nil, nil)) → PDL_IN_GA(nil)
U5_GA(nil, nil, right_out_ga(nil, nil)) → U6_GA(nil, nil, U2_ga(eq_in_aa))
U5_GA(nil, nil, right_out_ga(nil, nil)) → U6_GA(nil, nil, U3_ga(nil, value_in_ga(nil)))

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga(nil)
value_in_ga(tree(X6, X, X7)) → value_out_ga(tree(X6, X, X7))
left_in_ga(nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(tree(L, X1, X2), L)
right_in_ga(nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga(nil)
U3_ga(T, value_out_ga(T)) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(T, L)) → U5_ga(T, L, right_in_ga(T))
U5_ga(T, L, right_out_ga(T, R)) → U6_ga(T, R, pdl_in_ga(L))
U6_ga(T, R, pdl_out_ga(L)) → U7_ga(T, pdl_in_ga(R))
U7_ga(T, pdl_out_ga(R)) → pdl_out_ga(T)

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1, x2)
U6_ga(x0, x1, x2)
U7_ga(x0, x1)

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

(79) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U5_GA(nil, nil, right_out_ga(nil, nil)) → U6_GA(nil, nil, U2_ga(eq_in_aa)) at position [2,0] we obtained the following new rules [LPAR04]:

U5_GA(nil, nil, right_out_ga(nil, nil)) → U6_GA(nil, nil, U2_ga(eq_out_aa))

(80) Obligation:

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

PDL_IN_GA(nil) → U3_GA(nil, value_out_ga(nil))
U3_GA(nil, value_out_ga(nil)) → U4_GA(nil, left_out_ga(nil, nil))
U4_GA(nil, left_out_ga(nil, nil)) → U5_GA(nil, nil, right_out_ga(nil, nil))
U6_GA(nil, nil, pdl_out_ga(x2)) → PDL_IN_GA(nil)
U5_GA(nil, nil, right_out_ga(nil, nil)) → PDL_IN_GA(nil)
U5_GA(nil, nil, right_out_ga(nil, nil)) → U6_GA(nil, nil, U3_ga(nil, value_in_ga(nil)))
U5_GA(nil, nil, right_out_ga(nil, nil)) → U6_GA(nil, nil, U2_ga(eq_out_aa))

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga(nil)
value_in_ga(tree(X6, X, X7)) → value_out_ga(tree(X6, X, X7))
left_in_ga(nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(tree(L, X1, X2), L)
right_in_ga(nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga(nil)
U3_ga(T, value_out_ga(T)) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(T, L)) → U5_ga(T, L, right_in_ga(T))
U5_ga(T, L, right_out_ga(T, R)) → U6_ga(T, R, pdl_in_ga(L))
U6_ga(T, R, pdl_out_ga(L)) → U7_ga(T, pdl_in_ga(R))
U7_ga(T, pdl_out_ga(R)) → pdl_out_ga(T)

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1, x2)
U6_ga(x0, x1, x2)
U7_ga(x0, x1)

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

(81) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U5_GA(nil, nil, right_out_ga(nil, nil)) → U6_GA(nil, nil, U3_ga(nil, value_in_ga(nil))) at position [2,1] we obtained the following new rules [LPAR04]:

U5_GA(nil, nil, right_out_ga(nil, nil)) → U6_GA(nil, nil, U3_ga(nil, value_out_ga(nil)))

(82) Obligation:

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

PDL_IN_GA(nil) → U3_GA(nil, value_out_ga(nil))
U3_GA(nil, value_out_ga(nil)) → U4_GA(nil, left_out_ga(nil, nil))
U4_GA(nil, left_out_ga(nil, nil)) → U5_GA(nil, nil, right_out_ga(nil, nil))
U6_GA(nil, nil, pdl_out_ga(x2)) → PDL_IN_GA(nil)
U5_GA(nil, nil, right_out_ga(nil, nil)) → PDL_IN_GA(nil)
U5_GA(nil, nil, right_out_ga(nil, nil)) → U6_GA(nil, nil, U2_ga(eq_out_aa))
U5_GA(nil, nil, right_out_ga(nil, nil)) → U6_GA(nil, nil, U3_ga(nil, value_out_ga(nil)))

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga(nil)
value_in_ga(tree(X6, X, X7)) → value_out_ga(tree(X6, X, X7))
left_in_ga(nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(tree(L, X1, X2), L)
right_in_ga(nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga(nil)
U3_ga(T, value_out_ga(T)) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(T, L)) → U5_ga(T, L, right_in_ga(T))
U5_ga(T, L, right_out_ga(T, R)) → U6_ga(T, R, pdl_in_ga(L))
U6_ga(T, R, pdl_out_ga(L)) → U7_ga(T, pdl_in_ga(R))
U7_ga(T, pdl_out_ga(R)) → pdl_out_ga(T)

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1, x2)
U6_ga(x0, x1, x2)
U7_ga(x0, x1)

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

(83) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U5_GA(nil, nil, right_out_ga(nil, nil)) → U6_GA(nil, nil, U2_ga(eq_out_aa)) at position [2] we obtained the following new rules [LPAR04]:

U5_GA(nil, nil, right_out_ga(nil, nil)) → U6_GA(nil, nil, pdl_out_ga(nil))

(84) Obligation:

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

PDL_IN_GA(nil) → U3_GA(nil, value_out_ga(nil))
U3_GA(nil, value_out_ga(nil)) → U4_GA(nil, left_out_ga(nil, nil))
U4_GA(nil, left_out_ga(nil, nil)) → U5_GA(nil, nil, right_out_ga(nil, nil))
U6_GA(nil, nil, pdl_out_ga(x2)) → PDL_IN_GA(nil)
U5_GA(nil, nil, right_out_ga(nil, nil)) → PDL_IN_GA(nil)
U5_GA(nil, nil, right_out_ga(nil, nil)) → U6_GA(nil, nil, U3_ga(nil, value_out_ga(nil)))
U5_GA(nil, nil, right_out_ga(nil, nil)) → U6_GA(nil, nil, pdl_out_ga(nil))

The TRS R consists of the following rules:

value_in_ga(nil) → value_out_ga(nil)
value_in_ga(tree(X6, X, X7)) → value_out_ga(tree(X6, X, X7))
left_in_ga(nil) → left_out_ga(nil, nil)
left_in_ga(tree(L, X1, X2)) → left_out_ga(tree(L, X1, X2), L)
right_in_ga(nil) → right_out_ga(nil, nil)
right_in_ga(tree(X3, X4, R)) → right_out_ga(tree(X3, X4, R), R)
pdl_in_ga(nil) → U2_ga(eq_in_aa)
pdl_in_ga(T) → U3_ga(T, value_in_ga(T))
U2_ga(eq_out_aa) → pdl_out_ga(nil)
U3_ga(T, value_out_ga(T)) → U4_ga(T, left_in_ga(T))
eq_in_aa → eq_out_aa
U4_ga(T, left_out_ga(T, L)) → U5_ga(T, L, right_in_ga(T))
U5_ga(T, L, right_out_ga(T, R)) → U6_ga(T, R, pdl_in_ga(L))
U6_ga(T, R, pdl_out_ga(L)) → U7_ga(T, pdl_in_ga(R))
U7_ga(T, pdl_out_ga(R)) → pdl_out_ga(T)

The set Q consists of the following terms:

value_in_ga(x0)
left_in_ga(x0)
right_in_ga(x0)
pdl_in_ga(x0)
U2_ga(x0)
U3_ga(x0, x1)
eq_in_aa
U4_ga(x0, x1)
U5_ga(x0, x1, x2)
U6_ga(x0, x1, x2)
U7_ga(x0, x1)

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

(85) 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 = U3_GA(nil, value_out_ga(nil)) evaluates to t =U3_GA(nil, value_out_ga(nil))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Matcher: [ ]
• Semiunifier: [ ]

---

Rewriting sequence

U3_GA(nil, value_out_ga(nil)) → U4_GA(nil, left_out_ga(nil, nil))
with rule U3_GA(nil, value_out_ga(nil)) → U4_GA(nil, left_out_ga(nil, nil)) at position [] and matcher [ ]

U4_GA(nil, left_out_ga(nil, nil)) → U5_GA(nil, nil, right_out_ga(nil, nil))
with rule U4_GA(nil, left_out_ga(nil, nil)) → U5_GA(nil, nil, right_out_ga(nil, nil)) at position [] and matcher [ ]

U5_GA(nil, nil, right_out_ga(nil, nil)) → PDL_IN_GA(nil)
with rule U5_GA(nil, nil, right_out_ga(nil, nil)) → PDL_IN_GA(nil) at position [] and matcher [ ]

PDL_IN_GA(nil) → U3_GA(nil, value_out_ga(nil))
with rule PDL_IN_GA(nil) → U3_GA(nil, value_out_ga(nil))

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.

(86) FALSE