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



PROLOG
  ↳ PrologToPiTRSProof

right2(tree3(X, XS1, XS2), XS2).
flat2(niltree0, nil0).
flat2(tree3(X, niltree0, XS), cons2(X, YS)) :- right2(tree3(X, niltree0, XS), ZS), flat2(ZS, YS).
flat2(tree3(X, tree3(Y, YS1, YS2), XS), ZS) :- flat2(tree3(Y, YS1, tree3(X, YS2, XS)), ZS).


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


flat_2_in_ga2(niltree_0, nil_0) -> flat_2_out_ga2(niltree_0, nil_0)
flat_2_in_ga2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> if_flat_2_in_1_ga4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
right_2_in_ga2(tree_33(X, XS1, XS2), XS2) -> right_2_out_ga2(tree_33(X, XS1, XS2), XS2)
if_flat_2_in_1_ga4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_ga5(X, XS, YS, ZS, flat_2_in_ga2(ZS, YS))
flat_2_in_ga2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_ga7(X, Y, YS1, YS2, XS, ZS, flat_2_in_ga2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
if_flat_2_in_3_ga7(X, Y, YS1, YS2, XS, ZS, flat_2_out_ga2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)) -> flat_2_out_ga2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS)
if_flat_2_in_2_ga5(X, XS, YS, ZS, flat_2_out_ga2(ZS, YS)) -> flat_2_out_ga2(tree_33(X, niltree_0, XS), cons_22(X, YS))

The argument filtering Pi contains the following mapping:
flat_2_in_ga2(x1, x2)  =  flat_2_in_ga1(x1)
tree_33(x1, x2, x3)  =  tree_33(x1, x2, x3)
niltree_0  =  niltree_0
nil_0  =  nil_0
cons_22(x1, x2)  =  cons_22(x1, x2)
flat_2_out_ga2(x1, x2)  =  flat_2_out_ga1(x2)
if_flat_2_in_1_ga4(x1, x2, x3, x4)  =  if_flat_2_in_1_ga2(x1, x4)
right_2_in_ga2(x1, x2)  =  right_2_in_ga1(x1)
right_2_out_ga2(x1, x2)  =  right_2_out_ga1(x2)
if_flat_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_flat_2_in_2_ga2(x1, x5)
if_flat_2_in_3_ga7(x1, x2, x3, x4, x5, x6, x7)  =  if_flat_2_in_3_ga1(x7)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG



↳ PROLOG
  ↳ PrologToPiTRSProof
PiTRS
      ↳ DependencyPairsProof

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

flat_2_in_ga2(niltree_0, nil_0) -> flat_2_out_ga2(niltree_0, nil_0)
flat_2_in_ga2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> if_flat_2_in_1_ga4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
right_2_in_ga2(tree_33(X, XS1, XS2), XS2) -> right_2_out_ga2(tree_33(X, XS1, XS2), XS2)
if_flat_2_in_1_ga4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_ga5(X, XS, YS, ZS, flat_2_in_ga2(ZS, YS))
flat_2_in_ga2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_ga7(X, Y, YS1, YS2, XS, ZS, flat_2_in_ga2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
if_flat_2_in_3_ga7(X, Y, YS1, YS2, XS, ZS, flat_2_out_ga2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)) -> flat_2_out_ga2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS)
if_flat_2_in_2_ga5(X, XS, YS, ZS, flat_2_out_ga2(ZS, YS)) -> flat_2_out_ga2(tree_33(X, niltree_0, XS), cons_22(X, YS))

The argument filtering Pi contains the following mapping:
flat_2_in_ga2(x1, x2)  =  flat_2_in_ga1(x1)
tree_33(x1, x2, x3)  =  tree_33(x1, x2, x3)
niltree_0  =  niltree_0
nil_0  =  nil_0
cons_22(x1, x2)  =  cons_22(x1, x2)
flat_2_out_ga2(x1, x2)  =  flat_2_out_ga1(x2)
if_flat_2_in_1_ga4(x1, x2, x3, x4)  =  if_flat_2_in_1_ga2(x1, x4)
right_2_in_ga2(x1, x2)  =  right_2_in_ga1(x1)
right_2_out_ga2(x1, x2)  =  right_2_out_ga1(x2)
if_flat_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_flat_2_in_2_ga2(x1, x5)
if_flat_2_in_3_ga7(x1, x2, x3, x4, x5, x6, x7)  =  if_flat_2_in_3_ga1(x7)


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

FLAT_2_IN_GA2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> IF_FLAT_2_IN_1_GA4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
FLAT_2_IN_GA2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> RIGHT_2_IN_GA2(tree_33(X, niltree_0, XS), ZS)
IF_FLAT_2_IN_1_GA4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> IF_FLAT_2_IN_2_GA5(X, XS, YS, ZS, flat_2_in_ga2(ZS, YS))
IF_FLAT_2_IN_1_GA4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> FLAT_2_IN_GA2(ZS, YS)
FLAT_2_IN_GA2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> IF_FLAT_2_IN_3_GA7(X, Y, YS1, YS2, XS, ZS, flat_2_in_ga2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
FLAT_2_IN_GA2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GA2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)

The TRS R consists of the following rules:

flat_2_in_ga2(niltree_0, nil_0) -> flat_2_out_ga2(niltree_0, nil_0)
flat_2_in_ga2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> if_flat_2_in_1_ga4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
right_2_in_ga2(tree_33(X, XS1, XS2), XS2) -> right_2_out_ga2(tree_33(X, XS1, XS2), XS2)
if_flat_2_in_1_ga4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_ga5(X, XS, YS, ZS, flat_2_in_ga2(ZS, YS))
flat_2_in_ga2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_ga7(X, Y, YS1, YS2, XS, ZS, flat_2_in_ga2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
if_flat_2_in_3_ga7(X, Y, YS1, YS2, XS, ZS, flat_2_out_ga2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)) -> flat_2_out_ga2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS)
if_flat_2_in_2_ga5(X, XS, YS, ZS, flat_2_out_ga2(ZS, YS)) -> flat_2_out_ga2(tree_33(X, niltree_0, XS), cons_22(X, YS))

The argument filtering Pi contains the following mapping:
flat_2_in_ga2(x1, x2)  =  flat_2_in_ga1(x1)
tree_33(x1, x2, x3)  =  tree_33(x1, x2, x3)
niltree_0  =  niltree_0
nil_0  =  nil_0
cons_22(x1, x2)  =  cons_22(x1, x2)
flat_2_out_ga2(x1, x2)  =  flat_2_out_ga1(x2)
if_flat_2_in_1_ga4(x1, x2, x3, x4)  =  if_flat_2_in_1_ga2(x1, x4)
right_2_in_ga2(x1, x2)  =  right_2_in_ga1(x1)
right_2_out_ga2(x1, x2)  =  right_2_out_ga1(x2)
if_flat_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_flat_2_in_2_ga2(x1, x5)
if_flat_2_in_3_ga7(x1, x2, x3, x4, x5, x6, x7)  =  if_flat_2_in_3_ga1(x7)
FLAT_2_IN_GA2(x1, x2)  =  FLAT_2_IN_GA1(x1)
IF_FLAT_2_IN_1_GA4(x1, x2, x3, x4)  =  IF_FLAT_2_IN_1_GA2(x1, x4)
IF_FLAT_2_IN_3_GA7(x1, x2, x3, x4, x5, x6, x7)  =  IF_FLAT_2_IN_3_GA1(x7)
RIGHT_2_IN_GA2(x1, x2)  =  RIGHT_2_IN_GA1(x1)
IF_FLAT_2_IN_2_GA5(x1, x2, x3, x4, x5)  =  IF_FLAT_2_IN_2_GA2(x1, x5)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
PiDP
          ↳ DependencyGraphProof

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

FLAT_2_IN_GA2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> IF_FLAT_2_IN_1_GA4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
FLAT_2_IN_GA2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> RIGHT_2_IN_GA2(tree_33(X, niltree_0, XS), ZS)
IF_FLAT_2_IN_1_GA4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> IF_FLAT_2_IN_2_GA5(X, XS, YS, ZS, flat_2_in_ga2(ZS, YS))
IF_FLAT_2_IN_1_GA4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> FLAT_2_IN_GA2(ZS, YS)
FLAT_2_IN_GA2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> IF_FLAT_2_IN_3_GA7(X, Y, YS1, YS2, XS, ZS, flat_2_in_ga2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
FLAT_2_IN_GA2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GA2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)

The TRS R consists of the following rules:

flat_2_in_ga2(niltree_0, nil_0) -> flat_2_out_ga2(niltree_0, nil_0)
flat_2_in_ga2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> if_flat_2_in_1_ga4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
right_2_in_ga2(tree_33(X, XS1, XS2), XS2) -> right_2_out_ga2(tree_33(X, XS1, XS2), XS2)
if_flat_2_in_1_ga4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_ga5(X, XS, YS, ZS, flat_2_in_ga2(ZS, YS))
flat_2_in_ga2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_ga7(X, Y, YS1, YS2, XS, ZS, flat_2_in_ga2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
if_flat_2_in_3_ga7(X, Y, YS1, YS2, XS, ZS, flat_2_out_ga2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)) -> flat_2_out_ga2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS)
if_flat_2_in_2_ga5(X, XS, YS, ZS, flat_2_out_ga2(ZS, YS)) -> flat_2_out_ga2(tree_33(X, niltree_0, XS), cons_22(X, YS))

The argument filtering Pi contains the following mapping:
flat_2_in_ga2(x1, x2)  =  flat_2_in_ga1(x1)
tree_33(x1, x2, x3)  =  tree_33(x1, x2, x3)
niltree_0  =  niltree_0
nil_0  =  nil_0
cons_22(x1, x2)  =  cons_22(x1, x2)
flat_2_out_ga2(x1, x2)  =  flat_2_out_ga1(x2)
if_flat_2_in_1_ga4(x1, x2, x3, x4)  =  if_flat_2_in_1_ga2(x1, x4)
right_2_in_ga2(x1, x2)  =  right_2_in_ga1(x1)
right_2_out_ga2(x1, x2)  =  right_2_out_ga1(x2)
if_flat_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_flat_2_in_2_ga2(x1, x5)
if_flat_2_in_3_ga7(x1, x2, x3, x4, x5, x6, x7)  =  if_flat_2_in_3_ga1(x7)
FLAT_2_IN_GA2(x1, x2)  =  FLAT_2_IN_GA1(x1)
IF_FLAT_2_IN_1_GA4(x1, x2, x3, x4)  =  IF_FLAT_2_IN_1_GA2(x1, x4)
IF_FLAT_2_IN_3_GA7(x1, x2, x3, x4, x5, x6, x7)  =  IF_FLAT_2_IN_3_GA1(x7)
RIGHT_2_IN_GA2(x1, x2)  =  RIGHT_2_IN_GA1(x1)
IF_FLAT_2_IN_2_GA5(x1, x2, x3, x4, x5)  =  IF_FLAT_2_IN_2_GA2(x1, x5)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph contains 1 SCC with 3 less nodes.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
PiDP
              ↳ UsableRulesProof

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

FLAT_2_IN_GA2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> IF_FLAT_2_IN_1_GA4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
IF_FLAT_2_IN_1_GA4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> FLAT_2_IN_GA2(ZS, YS)
FLAT_2_IN_GA2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GA2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)

The TRS R consists of the following rules:

flat_2_in_ga2(niltree_0, nil_0) -> flat_2_out_ga2(niltree_0, nil_0)
flat_2_in_ga2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> if_flat_2_in_1_ga4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
right_2_in_ga2(tree_33(X, XS1, XS2), XS2) -> right_2_out_ga2(tree_33(X, XS1, XS2), XS2)
if_flat_2_in_1_ga4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_ga5(X, XS, YS, ZS, flat_2_in_ga2(ZS, YS))
flat_2_in_ga2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_ga7(X, Y, YS1, YS2, XS, ZS, flat_2_in_ga2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS))
if_flat_2_in_3_ga7(X, Y, YS1, YS2, XS, ZS, flat_2_out_ga2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)) -> flat_2_out_ga2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS)
if_flat_2_in_2_ga5(X, XS, YS, ZS, flat_2_out_ga2(ZS, YS)) -> flat_2_out_ga2(tree_33(X, niltree_0, XS), cons_22(X, YS))

The argument filtering Pi contains the following mapping:
flat_2_in_ga2(x1, x2)  =  flat_2_in_ga1(x1)
tree_33(x1, x2, x3)  =  tree_33(x1, x2, x3)
niltree_0  =  niltree_0
nil_0  =  nil_0
cons_22(x1, x2)  =  cons_22(x1, x2)
flat_2_out_ga2(x1, x2)  =  flat_2_out_ga1(x2)
if_flat_2_in_1_ga4(x1, x2, x3, x4)  =  if_flat_2_in_1_ga2(x1, x4)
right_2_in_ga2(x1, x2)  =  right_2_in_ga1(x1)
right_2_out_ga2(x1, x2)  =  right_2_out_ga1(x2)
if_flat_2_in_2_ga5(x1, x2, x3, x4, x5)  =  if_flat_2_in_2_ga2(x1, x5)
if_flat_2_in_3_ga7(x1, x2, x3, x4, x5, x6, x7)  =  if_flat_2_in_3_ga1(x7)
FLAT_2_IN_GA2(x1, x2)  =  FLAT_2_IN_GA1(x1)
IF_FLAT_2_IN_1_GA4(x1, x2, x3, x4)  =  IF_FLAT_2_IN_1_GA2(x1, x4)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
PiDP
                  ↳ PiDPToQDPProof

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

FLAT_2_IN_GA2(tree_33(X, niltree_0, XS), cons_22(X, YS)) -> IF_FLAT_2_IN_1_GA4(X, XS, YS, right_2_in_ga2(tree_33(X, niltree_0, XS), ZS))
IF_FLAT_2_IN_1_GA4(X, XS, YS, right_2_out_ga2(tree_33(X, niltree_0, XS), ZS)) -> FLAT_2_IN_GA2(ZS, YS)
FLAT_2_IN_GA2(tree_33(X, tree_33(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GA2(tree_33(Y, YS1, tree_33(X, YS2, XS)), ZS)

The TRS R consists of the following rules:

right_2_in_ga2(tree_33(X, XS1, XS2), XS2) -> right_2_out_ga2(tree_33(X, XS1, XS2), XS2)

The argument filtering Pi contains the following mapping:
tree_33(x1, x2, x3)  =  tree_33(x1, x2, x3)
niltree_0  =  niltree_0
cons_22(x1, x2)  =  cons_22(x1, x2)
right_2_in_ga2(x1, x2)  =  right_2_in_ga1(x1)
right_2_out_ga2(x1, x2)  =  right_2_out_ga1(x2)
FLAT_2_IN_GA2(x1, x2)  =  FLAT_2_IN_GA1(x1)
IF_FLAT_2_IN_1_GA4(x1, x2, x3, x4)  =  IF_FLAT_2_IN_1_GA2(x1, x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
QDP
                      ↳ QDPPoloProof

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

FLAT_2_IN_GA1(tree_33(X, niltree_0, XS)) -> IF_FLAT_2_IN_1_GA2(X, right_2_in_ga1(tree_33(X, niltree_0, XS)))
IF_FLAT_2_IN_1_GA2(X, right_2_out_ga1(ZS)) -> FLAT_2_IN_GA1(ZS)
FLAT_2_IN_GA1(tree_33(X, tree_33(Y, YS1, YS2), XS)) -> FLAT_2_IN_GA1(tree_33(Y, YS1, tree_33(X, YS2, XS)))

The TRS R consists of the following rules:

right_2_in_ga1(tree_33(X, XS1, XS2)) -> right_2_out_ga1(XS2)

The set Q consists of the following terms:

right_2_in_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_FLAT_2_IN_1_GA2, FLAT_2_IN_GA1}.
By using a polynomial ordering, the following set of Dependency Pairs of this DP problem can be strictly oriented.

IF_FLAT_2_IN_1_GA2(X, right_2_out_ga1(ZS)) -> FLAT_2_IN_GA1(ZS)
The remaining Dependency Pairs were at least non-strictly be oriented.

FLAT_2_IN_GA1(tree_33(X, niltree_0, XS)) -> IF_FLAT_2_IN_1_GA2(X, right_2_in_ga1(tree_33(X, niltree_0, XS)))
FLAT_2_IN_GA1(tree_33(X, tree_33(Y, YS1, YS2), XS)) -> FLAT_2_IN_GA1(tree_33(Y, YS1, tree_33(X, YS2, XS)))
With the implicit AFS we had to orient the following set of usable rules non-strictly.

right_2_in_ga1(tree_33(X, XS1, XS2)) -> right_2_out_ga1(XS2)
Used ordering: POLO with Polynomial interpretation:

POL(niltree_0) = 0   
POL(FLAT_2_IN_GA1(x1)) = x1   
POL(right_2_out_ga1(x1)) = 1 + x1   
POL(IF_FLAT_2_IN_1_GA2(x1, x2)) = x2   
POL(right_2_in_ga1(x1)) = x1   
POL(tree_33(x1, x2, x3)) = 1 + x2 + x3   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ QDPPoloProof
QDP
                          ↳ DependencyGraphProof

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

FLAT_2_IN_GA1(tree_33(X, niltree_0, XS)) -> IF_FLAT_2_IN_1_GA2(X, right_2_in_ga1(tree_33(X, niltree_0, XS)))
FLAT_2_IN_GA1(tree_33(X, tree_33(Y, YS1, YS2), XS)) -> FLAT_2_IN_GA1(tree_33(Y, YS1, tree_33(X, YS2, XS)))

The TRS R consists of the following rules:

right_2_in_ga1(tree_33(X, XS1, XS2)) -> right_2_out_ga1(XS2)

The set Q consists of the following terms:

right_2_in_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_FLAT_2_IN_1_GA2, FLAT_2_IN_GA1}.
The approximation of the Dependency Graph contains 1 SCC with 1 less node.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ QDPPoloProof
                        ↳ QDP
                          ↳ DependencyGraphProof
QDP
                              ↳ UsableRulesProof

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

FLAT_2_IN_GA1(tree_33(X, tree_33(Y, YS1, YS2), XS)) -> FLAT_2_IN_GA1(tree_33(Y, YS1, tree_33(X, YS2, XS)))

The TRS R consists of the following rules:

right_2_in_ga1(tree_33(X, XS1, XS2)) -> right_2_out_ga1(XS2)

The set Q consists of the following terms:

right_2_in_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {FLAT_2_IN_GA1}.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ PiDP
              ↳ UsableRulesProof
                ↳ PiDP
                  ↳ PiDPToQDPProof
                    ↳ QDP
                      ↳ QDPPoloProof
                        ↳ QDP
                          ↳ DependencyGraphProof
                            ↳ QDP
                              ↳ UsableRulesProof
QDP
                                  ↳ QDPSizeChangeProof

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

FLAT_2_IN_GA1(tree_33(X, tree_33(Y, YS1, YS2), XS)) -> FLAT_2_IN_GA1(tree_33(Y, YS1, tree_33(X, YS2, XS)))

R is empty.
The set Q consists of the following terms:

right_2_in_ga1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {FLAT_2_IN_GA1}.
We used the following order and afs together with the size-change analysis to show that there are no infinite chains for this DP problem.

Order:Homeomorphic Embedding Order

AFS:
tree_33(x1, x2, x3)  =  tree_31(x2)

From the DPs we obtained the following set of size-change graphs:

We oriented the following set of usable rules. none