Left Termination proof of /tmp/tmpVQss

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

right₂(tree₃(X, XS1, XS2), XS2).
flat₂(niltree₀, nil₀).
flat₂(tree₃(X, niltree₀, XS), cons₂(X, YS)) :- right₂(tree₃(X, niltree₀, XS), ZS), flat₂(ZS, YS).
flat₂(tree₃(X, tree₃(Y, YS1, YS2), XS), ZS) :- flat₂(tree₃(Y, YS1, tree₃(X, YS2, XS)), ZS).

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

flat_2_in_ag₂(niltree_0, nil_0) -> flat_2_out_ag₂(niltree_0, nil_0)
flat_2_in_ag₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> if_flat_2_in_1_ag₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
right_2_in_ga₂(tree_3₃(X, XS1, XS2), XS2) -> right_2_out_ga₂(tree_3₃(X, XS1, XS2), XS2)
if_flat_2_in_1_ag₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_ag₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
flat_2_in_ag₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_ag₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
flat_2_in_gg₂(niltree_0, nil_0) -> flat_2_out_gg₂(niltree_0, nil_0)
flat_2_in_gg₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> if_flat_2_in_1_gg₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
if_flat_2_in_1_gg₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_gg₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
if_flat_2_in_2_gg₅(X, XS, YS, ZS, flat_2_out_ag₂(ZS, YS)) -> flat_2_out_gg₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS))
flat_2_in_gg₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_gg₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
if_flat_2_in_3_gg₇(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)) -> flat_2_out_gg₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS)
if_flat_2_in_3_ag₇(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)) -> flat_2_out_ag₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS)
if_flat_2_in_2_ag₅(X, XS, YS, ZS, flat_2_out_ag₂(ZS, YS)) -> flat_2_out_ag₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS))

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

  ↳ PrologToPiTRSProof

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

flat_2_in_ag₂(niltree_0, nil_0) -> flat_2_out_ag₂(niltree_0, nil_0)
flat_2_in_ag₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> if_flat_2_in_1_ag₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
right_2_in_ga₂(tree_3₃(X, XS1, XS2), XS2) -> right_2_out_ga₂(tree_3₃(X, XS1, XS2), XS2)
if_flat_2_in_1_ag₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_ag₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
flat_2_in_ag₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_ag₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
flat_2_in_gg₂(niltree_0, nil_0) -> flat_2_out_gg₂(niltree_0, nil_0)
flat_2_in_gg₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> if_flat_2_in_1_gg₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
if_flat_2_in_1_gg₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_gg₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
if_flat_2_in_2_gg₅(X, XS, YS, ZS, flat_2_out_ag₂(ZS, YS)) -> flat_2_out_gg₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS))
flat_2_in_gg₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_gg₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
if_flat_2_in_3_gg₇(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)) -> flat_2_out_gg₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS)
if_flat_2_in_3_ag₇(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)) -> flat_2_out_ag₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS)
if_flat_2_in_2_ag₅(X, XS, YS, ZS, flat_2_out_ag₂(ZS, YS)) -> flat_2_out_ag₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS))

FLAT_2_IN_AG₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> IF_FLAT_2_IN_1_AG₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
FLAT_2_IN_AG₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> RIGHT_2_IN_GA₂(tree_3₃(X, niltree_0, XS), ZS)
IF_FLAT_2_IN_1_AG₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> IF_FLAT_2_IN_2_AG₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
IF_FLAT_2_IN_1_AG₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG₂(ZS, YS)
FLAT_2_IN_AG₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> IF_FLAT_2_IN_3_AG₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
FLAT_2_IN_AG₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)
FLAT_2_IN_GG₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> IF_FLAT_2_IN_1_GG₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
FLAT_2_IN_GG₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> RIGHT_2_IN_GA₂(tree_3₃(X, niltree_0, XS), ZS)
IF_FLAT_2_IN_1_GG₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> IF_FLAT_2_IN_2_GG₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
IF_FLAT_2_IN_1_GG₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG₂(ZS, YS)
FLAT_2_IN_GG₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> IF_FLAT_2_IN_3_GG₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
FLAT_2_IN_GG₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)

The TRS R consists of the following rules:

flat_2_in_ag₂(niltree_0, nil_0) -> flat_2_out_ag₂(niltree_0, nil_0)
flat_2_in_ag₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> if_flat_2_in_1_ag₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
right_2_in_ga₂(tree_3₃(X, XS1, XS2), XS2) -> right_2_out_ga₂(tree_3₃(X, XS1, XS2), XS2)
if_flat_2_in_1_ag₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_ag₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
flat_2_in_ag₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_ag₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
flat_2_in_gg₂(niltree_0, nil_0) -> flat_2_out_gg₂(niltree_0, nil_0)
flat_2_in_gg₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> if_flat_2_in_1_gg₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
if_flat_2_in_1_gg₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_gg₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
if_flat_2_in_2_gg₅(X, XS, YS, ZS, flat_2_out_ag₂(ZS, YS)) -> flat_2_out_gg₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS))
flat_2_in_gg₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_gg₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
if_flat_2_in_3_gg₇(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)) -> flat_2_out_gg₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS)
if_flat_2_in_3_ag₇(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)) -> flat_2_out_ag₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS)
if_flat_2_in_2_ag₅(X, XS, YS, ZS, flat_2_out_ag₂(ZS, YS)) -> flat_2_out_ag₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS))

The argument filtering Pi contains the following mapping:
flat_2_in_ag₂(x1, x2) = flat_2_in_ag₁(x2)
tree_3₃(x1, x2, x3) = tree_3
niltree_0 = niltree_0
nil_0 = nil_0
cons_2₂(x1, x2) = cons_2₂(x1, x2)
flat_2_out_ag₂(x1, x2) = flat_2_out_ag₁(x1)
if_flat_2_in_1_ag₄(x1, x2, x3, x4) = if_flat_2_in_1_ag₂(x3, x4)
right_2_in_ga₂(x1, x2) = right_2_in_ga₁(x1)
right_2_out_ga₂(x1, x2) = right_2_out_ga
if_flat_2_in_2_ag₅(x1, x2, x3, x4, x5) = if_flat_2_in_2_ag₁(x5)
if_flat_2_in_3_ag₇(x1, x2, x3, x4, x5, x6, x7) = if_flat_2_in_3_ag₁(x7)
flat_2_in_gg₂(x1, x2) = flat_2_in_gg₂(x1, x2)
flat_2_out_gg₂(x1, x2) = flat_2_out_gg
if_flat_2_in_1_gg₄(x1, x2, x3, x4) = if_flat_2_in_1_gg₂(x3, x4)
if_flat_2_in_2_gg₅(x1, x2, x3, x4, x5) = if_flat_2_in_2_gg₁(x5)
if_flat_2_in_3_gg₇(x1, x2, x3, x4, x5, x6, x7) = if_flat_2_in_3_gg₁(x7)
IF_FLAT_2_IN_3_GG₇(x1, x2, x3, x4, x5, x6, x7) = IF_FLAT_2_IN_3_GG₁(x7)
IF_FLAT_2_IN_3_AG₇(x1, x2, x3, x4, x5, x6, x7) = IF_FLAT_2_IN_3_AG₁(x7)
IF_FLAT_2_IN_2_AG₅(x1, x2, x3, x4, x5) = IF_FLAT_2_IN_2_AG₁(x5)
IF_FLAT_2_IN_2_GG₅(x1, x2, x3, x4, x5) = IF_FLAT_2_IN_2_GG₁(x5)
FLAT_2_IN_GG₂(x1, x2) = FLAT_2_IN_GG₂(x1, x2)
IF_FLAT_2_IN_1_GG₄(x1, x2, x3, x4) = IF_FLAT_2_IN_1_GG₂(x3, x4)
RIGHT_2_IN_GA₂(x1, x2) = RIGHT_2_IN_GA₁(x1)
FLAT_2_IN_AG₂(x1, x2) = FLAT_2_IN_AG₁(x2)
IF_FLAT_2_IN_1_AG₄(x1, x2, x3, x4) = IF_FLAT_2_IN_1_AG₂(x3, x4)

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

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

  ↳ PrologToPiTRSProof

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

FLAT_2_IN_AG₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> IF_FLAT_2_IN_1_AG₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
FLAT_2_IN_AG₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> RIGHT_2_IN_GA₂(tree_3₃(X, niltree_0, XS), ZS)
IF_FLAT_2_IN_1_AG₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> IF_FLAT_2_IN_2_AG₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
IF_FLAT_2_IN_1_AG₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG₂(ZS, YS)
FLAT_2_IN_AG₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> IF_FLAT_2_IN_3_AG₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
FLAT_2_IN_AG₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)
FLAT_2_IN_GG₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> IF_FLAT_2_IN_1_GG₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
FLAT_2_IN_GG₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> RIGHT_2_IN_GA₂(tree_3₃(X, niltree_0, XS), ZS)
IF_FLAT_2_IN_1_GG₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> IF_FLAT_2_IN_2_GG₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
IF_FLAT_2_IN_1_GG₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG₂(ZS, YS)
FLAT_2_IN_GG₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> IF_FLAT_2_IN_3_GG₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
FLAT_2_IN_GG₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)

The TRS R consists of the following rules:

flat_2_in_ag₂(niltree_0, nil_0) -> flat_2_out_ag₂(niltree_0, nil_0)
flat_2_in_ag₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> if_flat_2_in_1_ag₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
right_2_in_ga₂(tree_3₃(X, XS1, XS2), XS2) -> right_2_out_ga₂(tree_3₃(X, XS1, XS2), XS2)
if_flat_2_in_1_ag₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_ag₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
flat_2_in_ag₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_ag₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
flat_2_in_gg₂(niltree_0, nil_0) -> flat_2_out_gg₂(niltree_0, nil_0)
flat_2_in_gg₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> if_flat_2_in_1_gg₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
if_flat_2_in_1_gg₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_gg₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
if_flat_2_in_2_gg₅(X, XS, YS, ZS, flat_2_out_ag₂(ZS, YS)) -> flat_2_out_gg₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS))
flat_2_in_gg₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_gg₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
if_flat_2_in_3_gg₇(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)) -> flat_2_out_gg₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS)
if_flat_2_in_3_ag₇(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)) -> flat_2_out_ag₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS)
if_flat_2_in_2_ag₅(X, XS, YS, ZS, flat_2_out_ag₂(ZS, YS)) -> flat_2_out_ag₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS))

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

  ↳ PrologToPiTRSProof

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

FLAT_2_IN_GG₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> IF_FLAT_2_IN_1_GG₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
FLAT_2_IN_AG₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> IF_FLAT_2_IN_1_AG₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
IF_FLAT_2_IN_1_AG₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG₂(ZS, YS)
FLAT_2_IN_GG₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)
IF_FLAT_2_IN_1_GG₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG₂(ZS, YS)
FLAT_2_IN_AG₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)

The TRS R consists of the following rules:

flat_2_in_ag₂(niltree_0, nil_0) -> flat_2_out_ag₂(niltree_0, nil_0)
flat_2_in_ag₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> if_flat_2_in_1_ag₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
right_2_in_ga₂(tree_3₃(X, XS1, XS2), XS2) -> right_2_out_ga₂(tree_3₃(X, XS1, XS2), XS2)
if_flat_2_in_1_ag₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_ag₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
flat_2_in_ag₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_ag₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
flat_2_in_gg₂(niltree_0, nil_0) -> flat_2_out_gg₂(niltree_0, nil_0)
flat_2_in_gg₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> if_flat_2_in_1_gg₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
if_flat_2_in_1_gg₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_gg₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
if_flat_2_in_2_gg₅(X, XS, YS, ZS, flat_2_out_ag₂(ZS, YS)) -> flat_2_out_gg₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS))
flat_2_in_gg₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_gg₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
if_flat_2_in_3_gg₇(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)) -> flat_2_out_gg₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS)
if_flat_2_in_3_ag₇(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)) -> flat_2_out_ag₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS)
if_flat_2_in_2_ag₅(X, XS, YS, ZS, flat_2_out_ag₂(ZS, YS)) -> flat_2_out_ag₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS))

The argument filtering Pi contains the following mapping:
flat_2_in_ag₂(x1, x2) = flat_2_in_ag₁(x2)
tree_3₃(x1, x2, x3) = tree_3
niltree_0 = niltree_0
nil_0 = nil_0
cons_2₂(x1, x2) = cons_2₂(x1, x2)
flat_2_out_ag₂(x1, x2) = flat_2_out_ag₁(x1)
if_flat_2_in_1_ag₄(x1, x2, x3, x4) = if_flat_2_in_1_ag₂(x3, x4)
right_2_in_ga₂(x1, x2) = right_2_in_ga₁(x1)
right_2_out_ga₂(x1, x2) = right_2_out_ga
if_flat_2_in_2_ag₅(x1, x2, x3, x4, x5) = if_flat_2_in_2_ag₁(x5)
if_flat_2_in_3_ag₇(x1, x2, x3, x4, x5, x6, x7) = if_flat_2_in_3_ag₁(x7)
flat_2_in_gg₂(x1, x2) = flat_2_in_gg₂(x1, x2)
flat_2_out_gg₂(x1, x2) = flat_2_out_gg
if_flat_2_in_1_gg₄(x1, x2, x3, x4) = if_flat_2_in_1_gg₂(x3, x4)
if_flat_2_in_2_gg₅(x1, x2, x3, x4, x5) = if_flat_2_in_2_gg₁(x5)
if_flat_2_in_3_gg₇(x1, x2, x3, x4, x5, x6, x7) = if_flat_2_in_3_gg₁(x7)
FLAT_2_IN_GG₂(x1, x2) = FLAT_2_IN_GG₂(x1, x2)
IF_FLAT_2_IN_1_GG₄(x1, x2, x3, x4) = IF_FLAT_2_IN_1_GG₂(x3, x4)
FLAT_2_IN_AG₂(x1, x2) = FLAT_2_IN_AG₁(x2)
IF_FLAT_2_IN_1_AG₄(x1, x2, x3, x4) = IF_FLAT_2_IN_1_AG₂(x3, 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

  ↳ PrologToPiTRSProof

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

FLAT_2_IN_GG₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> IF_FLAT_2_IN_1_GG₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
FLAT_2_IN_AG₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> IF_FLAT_2_IN_1_AG₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
IF_FLAT_2_IN_1_AG₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG₂(ZS, YS)
FLAT_2_IN_GG₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)
IF_FLAT_2_IN_1_GG₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG₂(ZS, YS)
FLAT_2_IN_AG₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)

The TRS R consists of the following rules:

right_2_in_ga₂(tree_3₃(X, XS1, XS2), XS2) -> right_2_out_ga₂(tree_3₃(X, XS1, XS2), XS2)

The argument filtering Pi contains the following mapping:
tree_3₃(x1, x2, x3) = tree_3
niltree_0 = niltree_0
cons_2₂(x1, x2) = cons_2₂(x1, x2)
right_2_in_ga₂(x1, x2) = right_2_in_ga₁(x1)
right_2_out_ga₂(x1, x2) = right_2_out_ga
FLAT_2_IN_GG₂(x1, x2) = FLAT_2_IN_GG₂(x1, x2)
IF_FLAT_2_IN_1_GG₄(x1, x2, x3, x4) = IF_FLAT_2_IN_1_GG₂(x3, x4)
FLAT_2_IN_AG₂(x1, x2) = FLAT_2_IN_AG₁(x2)
IF_FLAT_2_IN_1_AG₄(x1, x2, x3, x4) = IF_FLAT_2_IN_1_AG₂(x3, x4)

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

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

                ↳ PiDP

                  ↳ PiDPToQDPProof

                    ↳ QDP

                      ↳ RuleRemovalProof

  ↳ PrologToPiTRSProof

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

FLAT_2_IN_GG₂(tree_3, cons_2₂(X, YS)) -> IF_FLAT_2_IN_1_GG₂(YS, right_2_in_ga₁(tree_3))
FLAT_2_IN_AG₁(cons_2₂(X, YS)) -> IF_FLAT_2_IN_1_AG₂(YS, right_2_in_ga₁(tree_3))
IF_FLAT_2_IN_1_AG₂(YS, right_2_out_ga) -> FLAT_2_IN_AG₁(YS)
FLAT_2_IN_GG₂(tree_3, ZS) -> FLAT_2_IN_GG₂(tree_3, ZS)
IF_FLAT_2_IN_1_GG₂(YS, right_2_out_ga) -> FLAT_2_IN_AG₁(YS)
FLAT_2_IN_AG₁(ZS) -> FLAT_2_IN_GG₂(tree_3, ZS)

The TRS R consists of the following rules:

right_2_in_ga₁(tree_3) -> right_2_out_ga

The set Q consists of the following terms:

right_2_in_ga₁(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_FLAT_2_IN_1_GG₂, FLAT_2_IN_GG₂, IF_FLAT_2_IN_1_AG₂, FLAT_2_IN_AG₁}.
By using a polynomial ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.

Strictly oriented rules of the TRS R:

right_2_in_ga₁(tree_3) -> right_2_out_ga

Used ordering: POLO with Polynomial interpretation:

POL(FLAT_2_IN_AG₁(x₁)) = 1 + x₁
POL(FLAT_2_IN_GG₂(x₁, x₂)) = x₁ + x₂
POL(IF_FLAT_2_IN_1_GG₂(x₁, x₂)) = x₁ + x₂
POL(tree_3) = 1
POL(IF_FLAT_2_IN_1_AG₂(x₁, x₂)) = x₁ + x₂
POL(right_2_in_ga₁(x₁)) = 2·x₁
POL(right_2_out_ga) = 1
POL(cons_2₂(x₁, x₂)) = 1 + x₁ + x₂

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

                ↳ PiDP

                  ↳ PiDPToQDPProof

                    ↳ QDP

                      ↳ RuleRemovalProof

                        ↳ QDP

                          ↳ DependencyGraphProof

  ↳ PrologToPiTRSProof

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

FLAT_2_IN_GG₂(tree_3, cons_2₂(X, YS)) -> IF_FLAT_2_IN_1_GG₂(YS, right_2_in_ga₁(tree_3))
FLAT_2_IN_AG₁(cons_2₂(X, YS)) -> IF_FLAT_2_IN_1_AG₂(YS, right_2_in_ga₁(tree_3))
IF_FLAT_2_IN_1_AG₂(YS, right_2_out_ga) -> FLAT_2_IN_AG₁(YS)
FLAT_2_IN_GG₂(tree_3, ZS) -> FLAT_2_IN_GG₂(tree_3, ZS)
IF_FLAT_2_IN_1_GG₂(YS, right_2_out_ga) -> FLAT_2_IN_AG₁(YS)
FLAT_2_IN_AG₁(ZS) -> FLAT_2_IN_GG₂(tree_3, ZS)

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

right_2_in_ga₁(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_FLAT_2_IN_1_GG₂, FLAT_2_IN_GG₂, IF_FLAT_2_IN_1_AG₂, FLAT_2_IN_AG₁}.
The approximation of the Dependency Graph contains 1 SCC with 5 less nodes.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

                ↳ PiDP

                  ↳ PiDPToQDPProof

                    ↳ QDP

                      ↳ RuleRemovalProof

                        ↳ QDP

                          ↳ DependencyGraphProof

                            ↳ QDP

  ↳ PrologToPiTRSProof

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

FLAT_2_IN_GG₂(tree_3, ZS) -> FLAT_2_IN_GG₂(tree_3, ZS)

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

right_2_in_ga₁(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {FLAT_2_IN_GG₂}.
With regard to the inferred argument filtering the predicates were used in the following modes:
flat₂: (f,b) (b,b)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

flat_2_in_ag₂(niltree_0, nil_0) -> flat_2_out_ag₂(niltree_0, nil_0)
flat_2_in_ag₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> if_flat_2_in_1_ag₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
right_2_in_ga₂(tree_3₃(X, XS1, XS2), XS2) -> right_2_out_ga₂(tree_3₃(X, XS1, XS2), XS2)
if_flat_2_in_1_ag₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_ag₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
flat_2_in_ag₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_ag₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
flat_2_in_gg₂(niltree_0, nil_0) -> flat_2_out_gg₂(niltree_0, nil_0)
flat_2_in_gg₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> if_flat_2_in_1_gg₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
if_flat_2_in_1_gg₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_gg₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
if_flat_2_in_2_gg₅(X, XS, YS, ZS, flat_2_out_ag₂(ZS, YS)) -> flat_2_out_gg₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS))
flat_2_in_gg₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_gg₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
if_flat_2_in_3_gg₇(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)) -> flat_2_out_gg₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS)
if_flat_2_in_3_ag₇(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)) -> flat_2_out_ag₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS)
if_flat_2_in_2_ag₅(X, XS, YS, ZS, flat_2_out_ag₂(ZS, YS)) -> flat_2_out_ag₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS))

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

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

flat_2_in_ag₂(niltree_0, nil_0) -> flat_2_out_ag₂(niltree_0, nil_0)
flat_2_in_ag₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> if_flat_2_in_1_ag₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
right_2_in_ga₂(tree_3₃(X, XS1, XS2), XS2) -> right_2_out_ga₂(tree_3₃(X, XS1, XS2), XS2)
if_flat_2_in_1_ag₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_ag₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
flat_2_in_ag₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_ag₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
flat_2_in_gg₂(niltree_0, nil_0) -> flat_2_out_gg₂(niltree_0, nil_0)
flat_2_in_gg₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> if_flat_2_in_1_gg₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
if_flat_2_in_1_gg₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_gg₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
if_flat_2_in_2_gg₅(X, XS, YS, ZS, flat_2_out_ag₂(ZS, YS)) -> flat_2_out_gg₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS))
flat_2_in_gg₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_gg₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
if_flat_2_in_3_gg₇(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)) -> flat_2_out_gg₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS)
if_flat_2_in_3_ag₇(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)) -> flat_2_out_ag₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS)
if_flat_2_in_2_ag₅(X, XS, YS, ZS, flat_2_out_ag₂(ZS, YS)) -> flat_2_out_ag₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS))

FLAT_2_IN_AG₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> IF_FLAT_2_IN_1_AG₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
FLAT_2_IN_AG₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> RIGHT_2_IN_GA₂(tree_3₃(X, niltree_0, XS), ZS)
IF_FLAT_2_IN_1_AG₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> IF_FLAT_2_IN_2_AG₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
IF_FLAT_2_IN_1_AG₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG₂(ZS, YS)
FLAT_2_IN_AG₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> IF_FLAT_2_IN_3_AG₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
FLAT_2_IN_AG₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)
FLAT_2_IN_GG₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> IF_FLAT_2_IN_1_GG₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
FLAT_2_IN_GG₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> RIGHT_2_IN_GA₂(tree_3₃(X, niltree_0, XS), ZS)
IF_FLAT_2_IN_1_GG₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> IF_FLAT_2_IN_2_GG₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
IF_FLAT_2_IN_1_GG₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG₂(ZS, YS)
FLAT_2_IN_GG₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> IF_FLAT_2_IN_3_GG₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
FLAT_2_IN_GG₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)

The TRS R consists of the following rules:

flat_2_in_ag₂(niltree_0, nil_0) -> flat_2_out_ag₂(niltree_0, nil_0)
flat_2_in_ag₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> if_flat_2_in_1_ag₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
right_2_in_ga₂(tree_3₃(X, XS1, XS2), XS2) -> right_2_out_ga₂(tree_3₃(X, XS1, XS2), XS2)
if_flat_2_in_1_ag₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_ag₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
flat_2_in_ag₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_ag₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
flat_2_in_gg₂(niltree_0, nil_0) -> flat_2_out_gg₂(niltree_0, nil_0)
flat_2_in_gg₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> if_flat_2_in_1_gg₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
if_flat_2_in_1_gg₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_gg₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
if_flat_2_in_2_gg₅(X, XS, YS, ZS, flat_2_out_ag₂(ZS, YS)) -> flat_2_out_gg₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS))
flat_2_in_gg₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_gg₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
if_flat_2_in_3_gg₇(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)) -> flat_2_out_gg₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS)
if_flat_2_in_3_ag₇(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)) -> flat_2_out_ag₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS)
if_flat_2_in_2_ag₅(X, XS, YS, ZS, flat_2_out_ag₂(ZS, YS)) -> flat_2_out_ag₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS))

The argument filtering Pi contains the following mapping:
flat_2_in_ag₂(x1, x2) = flat_2_in_ag₁(x2)
tree_3₃(x1, x2, x3) = tree_3
niltree_0 = niltree_0
nil_0 = nil_0
cons_2₂(x1, x2) = cons_2₂(x1, x2)
flat_2_out_ag₂(x1, x2) = flat_2_out_ag₂(x1, x2)
if_flat_2_in_1_ag₄(x1, x2, x3, x4) = if_flat_2_in_1_ag₃(x1, x3, x4)
right_2_in_ga₂(x1, x2) = right_2_in_ga₁(x1)
right_2_out_ga₂(x1, x2) = right_2_out_ga₁(x1)
if_flat_2_in_2_ag₅(x1, x2, x3, x4, x5) = if_flat_2_in_2_ag₃(x1, x3, x5)
if_flat_2_in_3_ag₇(x1, x2, x3, x4, x5, x6, x7) = if_flat_2_in_3_ag₂(x6, x7)
flat_2_in_gg₂(x1, x2) = flat_2_in_gg₂(x1, x2)
flat_2_out_gg₂(x1, x2) = flat_2_out_gg₂(x1, x2)
if_flat_2_in_1_gg₄(x1, x2, x3, x4) = if_flat_2_in_1_gg₃(x1, x3, x4)
if_flat_2_in_2_gg₅(x1, x2, x3, x4, x5) = if_flat_2_in_2_gg₃(x1, x3, x5)
if_flat_2_in_3_gg₇(x1, x2, x3, x4, x5, x6, x7) = if_flat_2_in_3_gg₂(x6, x7)
IF_FLAT_2_IN_3_GG₇(x1, x2, x3, x4, x5, x6, x7) = IF_FLAT_2_IN_3_GG₂(x6, x7)
IF_FLAT_2_IN_3_AG₇(x1, x2, x3, x4, x5, x6, x7) = IF_FLAT_2_IN_3_AG₂(x6, x7)
IF_FLAT_2_IN_2_AG₅(x1, x2, x3, x4, x5) = IF_FLAT_2_IN_2_AG₃(x1, x3, x5)
IF_FLAT_2_IN_2_GG₅(x1, x2, x3, x4, x5) = IF_FLAT_2_IN_2_GG₃(x1, x3, x5)
FLAT_2_IN_GG₂(x1, x2) = FLAT_2_IN_GG₂(x1, x2)
IF_FLAT_2_IN_1_GG₄(x1, x2, x3, x4) = IF_FLAT_2_IN_1_GG₃(x1, x3, x4)
RIGHT_2_IN_GA₂(x1, x2) = RIGHT_2_IN_GA₁(x1)
FLAT_2_IN_AG₂(x1, x2) = FLAT_2_IN_AG₁(x2)
IF_FLAT_2_IN_1_AG₄(x1, x2, x3, x4) = IF_FLAT_2_IN_1_AG₃(x1, x3, x4)

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

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

FLAT_2_IN_AG₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> IF_FLAT_2_IN_1_AG₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
FLAT_2_IN_AG₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> RIGHT_2_IN_GA₂(tree_3₃(X, niltree_0, XS), ZS)
IF_FLAT_2_IN_1_AG₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> IF_FLAT_2_IN_2_AG₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
IF_FLAT_2_IN_1_AG₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG₂(ZS, YS)
FLAT_2_IN_AG₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> IF_FLAT_2_IN_3_AG₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
FLAT_2_IN_AG₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)
FLAT_2_IN_GG₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> IF_FLAT_2_IN_1_GG₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
FLAT_2_IN_GG₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> RIGHT_2_IN_GA₂(tree_3₃(X, niltree_0, XS), ZS)
IF_FLAT_2_IN_1_GG₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> IF_FLAT_2_IN_2_GG₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
IF_FLAT_2_IN_1_GG₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG₂(ZS, YS)
FLAT_2_IN_GG₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> IF_FLAT_2_IN_3_GG₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
FLAT_2_IN_GG₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)

The TRS R consists of the following rules:

flat_2_in_ag₂(niltree_0, nil_0) -> flat_2_out_ag₂(niltree_0, nil_0)
flat_2_in_ag₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> if_flat_2_in_1_ag₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
right_2_in_ga₂(tree_3₃(X, XS1, XS2), XS2) -> right_2_out_ga₂(tree_3₃(X, XS1, XS2), XS2)
if_flat_2_in_1_ag₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_ag₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
flat_2_in_ag₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_ag₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
flat_2_in_gg₂(niltree_0, nil_0) -> flat_2_out_gg₂(niltree_0, nil_0)
flat_2_in_gg₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> if_flat_2_in_1_gg₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
if_flat_2_in_1_gg₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_gg₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
if_flat_2_in_2_gg₅(X, XS, YS, ZS, flat_2_out_ag₂(ZS, YS)) -> flat_2_out_gg₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS))
flat_2_in_gg₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_gg₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
if_flat_2_in_3_gg₇(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)) -> flat_2_out_gg₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS)
if_flat_2_in_3_ag₇(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)) -> flat_2_out_ag₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS)
if_flat_2_in_2_ag₅(X, XS, YS, ZS, flat_2_out_ag₂(ZS, YS)) -> flat_2_out_ag₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS))

The argument filtering Pi contains the following mapping:
flat_2_in_ag₂(x1, x2) = flat_2_in_ag₁(x2)
tree_3₃(x1, x2, x3) = tree_3
niltree_0 = niltree_0
nil_0 = nil_0
cons_2₂(x1, x2) = cons_2₂(x1, x2)
flat_2_out_ag₂(x1, x2) = flat_2_out_ag₂(x1, x2)
if_flat_2_in_1_ag₄(x1, x2, x3, x4) = if_flat_2_in_1_ag₃(x1, x3, x4)
right_2_in_ga₂(x1, x2) = right_2_in_ga₁(x1)
right_2_out_ga₂(x1, x2) = right_2_out_ga₁(x1)
if_flat_2_in_2_ag₅(x1, x2, x3, x4, x5) = if_flat_2_in_2_ag₃(x1, x3, x5)
if_flat_2_in_3_ag₇(x1, x2, x3, x4, x5, x6, x7) = if_flat_2_in_3_ag₂(x6, x7)
flat_2_in_gg₂(x1, x2) = flat_2_in_gg₂(x1, x2)
flat_2_out_gg₂(x1, x2) = flat_2_out_gg₂(x1, x2)
if_flat_2_in_1_gg₄(x1, x2, x3, x4) = if_flat_2_in_1_gg₃(x1, x3, x4)
if_flat_2_in_2_gg₅(x1, x2, x3, x4, x5) = if_flat_2_in_2_gg₃(x1, x3, x5)
if_flat_2_in_3_gg₇(x1, x2, x3, x4, x5, x6, x7) = if_flat_2_in_3_gg₂(x6, x7)
IF_FLAT_2_IN_3_GG₇(x1, x2, x3, x4, x5, x6, x7) = IF_FLAT_2_IN_3_GG₂(x6, x7)
IF_FLAT_2_IN_3_AG₇(x1, x2, x3, x4, x5, x6, x7) = IF_FLAT_2_IN_3_AG₂(x6, x7)
IF_FLAT_2_IN_2_AG₅(x1, x2, x3, x4, x5) = IF_FLAT_2_IN_2_AG₃(x1, x3, x5)
IF_FLAT_2_IN_2_GG₅(x1, x2, x3, x4, x5) = IF_FLAT_2_IN_2_GG₃(x1, x3, x5)
FLAT_2_IN_GG₂(x1, x2) = FLAT_2_IN_GG₂(x1, x2)
IF_FLAT_2_IN_1_GG₄(x1, x2, x3, x4) = IF_FLAT_2_IN_1_GG₃(x1, x3, x4)
RIGHT_2_IN_GA₂(x1, x2) = RIGHT_2_IN_GA₁(x1)
FLAT_2_IN_AG₂(x1, x2) = FLAT_2_IN_AG₁(x2)
IF_FLAT_2_IN_1_AG₄(x1, x2, x3, x4) = IF_FLAT_2_IN_1_AG₃(x1, x3, x4)

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

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

FLAT_2_IN_GG₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> IF_FLAT_2_IN_1_GG₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
FLAT_2_IN_AG₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> IF_FLAT_2_IN_1_AG₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
IF_FLAT_2_IN_1_AG₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG₂(ZS, YS)
FLAT_2_IN_GG₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)
IF_FLAT_2_IN_1_GG₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG₂(ZS, YS)
FLAT_2_IN_AG₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)

The TRS R consists of the following rules:

flat_2_in_ag₂(niltree_0, nil_0) -> flat_2_out_ag₂(niltree_0, nil_0)
flat_2_in_ag₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> if_flat_2_in_1_ag₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
right_2_in_ga₂(tree_3₃(X, XS1, XS2), XS2) -> right_2_out_ga₂(tree_3₃(X, XS1, XS2), XS2)
if_flat_2_in_1_ag₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_ag₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
flat_2_in_ag₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_ag₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
flat_2_in_gg₂(niltree_0, nil_0) -> flat_2_out_gg₂(niltree_0, nil_0)
flat_2_in_gg₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> if_flat_2_in_1_gg₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
if_flat_2_in_1_gg₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> if_flat_2_in_2_gg₅(X, XS, YS, ZS, flat_2_in_ag₂(ZS, YS))
if_flat_2_in_2_gg₅(X, XS, YS, ZS, flat_2_out_ag₂(ZS, YS)) -> flat_2_out_gg₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS))
flat_2_in_gg₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> if_flat_2_in_3_gg₇(X, Y, YS1, YS2, XS, ZS, flat_2_in_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS))
if_flat_2_in_3_gg₇(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)) -> flat_2_out_gg₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS)
if_flat_2_in_3_ag₇(X, Y, YS1, YS2, XS, ZS, flat_2_out_gg₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)) -> flat_2_out_ag₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS)
if_flat_2_in_2_ag₅(X, XS, YS, ZS, flat_2_out_ag₂(ZS, YS)) -> flat_2_out_ag₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS))

The argument filtering Pi contains the following mapping:
flat_2_in_ag₂(x1, x2) = flat_2_in_ag₁(x2)
tree_3₃(x1, x2, x3) = tree_3
niltree_0 = niltree_0
nil_0 = nil_0
cons_2₂(x1, x2) = cons_2₂(x1, x2)
flat_2_out_ag₂(x1, x2) = flat_2_out_ag₂(x1, x2)
if_flat_2_in_1_ag₄(x1, x2, x3, x4) = if_flat_2_in_1_ag₃(x1, x3, x4)
right_2_in_ga₂(x1, x2) = right_2_in_ga₁(x1)
right_2_out_ga₂(x1, x2) = right_2_out_ga₁(x1)
if_flat_2_in_2_ag₅(x1, x2, x3, x4, x5) = if_flat_2_in_2_ag₃(x1, x3, x5)
if_flat_2_in_3_ag₇(x1, x2, x3, x4, x5, x6, x7) = if_flat_2_in_3_ag₂(x6, x7)
flat_2_in_gg₂(x1, x2) = flat_2_in_gg₂(x1, x2)
flat_2_out_gg₂(x1, x2) = flat_2_out_gg₂(x1, x2)
if_flat_2_in_1_gg₄(x1, x2, x3, x4) = if_flat_2_in_1_gg₃(x1, x3, x4)
if_flat_2_in_2_gg₅(x1, x2, x3, x4, x5) = if_flat_2_in_2_gg₃(x1, x3, x5)
if_flat_2_in_3_gg₇(x1, x2, x3, x4, x5, x6, x7) = if_flat_2_in_3_gg₂(x6, x7)
FLAT_2_IN_GG₂(x1, x2) = FLAT_2_IN_GG₂(x1, x2)
IF_FLAT_2_IN_1_GG₄(x1, x2, x3, x4) = IF_FLAT_2_IN_1_GG₃(x1, x3, x4)
FLAT_2_IN_AG₂(x1, x2) = FLAT_2_IN_AG₁(x2)
IF_FLAT_2_IN_1_AG₄(x1, x2, x3, x4) = IF_FLAT_2_IN_1_AG₃(x1, x3, 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

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

                ↳ PiDP

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

FLAT_2_IN_GG₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> IF_FLAT_2_IN_1_GG₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
FLAT_2_IN_AG₂(tree_3₃(X, niltree_0, XS), cons_2₂(X, YS)) -> IF_FLAT_2_IN_1_AG₄(X, XS, YS, right_2_in_ga₂(tree_3₃(X, niltree_0, XS), ZS))
IF_FLAT_2_IN_1_AG₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG₂(ZS, YS)
FLAT_2_IN_GG₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)
IF_FLAT_2_IN_1_GG₄(X, XS, YS, right_2_out_ga₂(tree_3₃(X, niltree_0, XS), ZS)) -> FLAT_2_IN_AG₂(ZS, YS)
FLAT_2_IN_AG₂(tree_3₃(X, tree_3₃(Y, YS1, YS2), XS), ZS) -> FLAT_2_IN_GG₂(tree_3₃(Y, YS1, tree_3₃(X, YS2, XS)), ZS)

The TRS R consists of the following rules:

right_2_in_ga₂(tree_3₃(X, XS1, XS2), XS2) -> right_2_out_ga₂(tree_3₃(X, XS1, XS2), XS2)

The argument filtering Pi contains the following mapping:
tree_3₃(x1, x2, x3) = tree_3
niltree_0 = niltree_0
cons_2₂(x1, x2) = cons_2₂(x1, x2)
right_2_in_ga₂(x1, x2) = right_2_in_ga₁(x1)
right_2_out_ga₂(x1, x2) = right_2_out_ga₁(x1)
FLAT_2_IN_GG₂(x1, x2) = FLAT_2_IN_GG₂(x1, x2)
IF_FLAT_2_IN_1_GG₄(x1, x2, x3, x4) = IF_FLAT_2_IN_1_GG₃(x1, x3, x4)
FLAT_2_IN_AG₂(x1, x2) = FLAT_2_IN_AG₁(x2)
IF_FLAT_2_IN_1_AG₄(x1, x2, x3, x4) = IF_FLAT_2_IN_1_AG₃(x1, x3, x4)

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