Left Termination proof of /tmp/tmp8ZNT2N/bad

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

append1₃({}₀, Ys, Ys).
append1₃(.₂(X, Xs), Ys, .₂(X, Zs)) :- append1₃(Xs, Ys, Zs).
append2₃({}₀, Ys, Ys).
append2₃(.₂(X, Xs), Ys, .₂(X, Zs)) :- append2₃(Xs, Ys, Zs).
sublist₂(X, Y) :- append1₃(U, X, V), append2₃(V, W, Y).

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

sublist_2_in_gg₂(X, Y) -> if_sublist_2_in_1_gg₃(X, Y, append1_3_in_aga₃(U, X, V))
append1_3_in_aga₃([]_0, Ys, Ys) -> append1_3_out_aga₃([]_0, Ys, Ys)
append1_3_in_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_append1_3_in_1_aga₅(X, Xs, Ys, Zs, append1_3_in_aga₃(Xs, Ys, Zs))
if_append1_3_in_1_aga₅(X, Xs, Ys, Zs, append1_3_out_aga₃(Xs, Ys, Zs)) -> append1_3_out_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_sublist_2_in_1_gg₃(X, Y, append1_3_out_aga₃(U, X, V)) -> if_sublist_2_in_2_gg₄(X, Y, V, append2_3_in_gag₃(V, W, Y))
append2_3_in_gag₃([]_0, Ys, Ys) -> append2_3_out_gag₃([]_0, Ys, Ys)
append2_3_in_gag₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_append2_3_in_1_gag₅(X, Xs, Ys, Zs, append2_3_in_gag₃(Xs, Ys, Zs))
if_append2_3_in_1_gag₅(X, Xs, Ys, Zs, append2_3_out_gag₃(Xs, Ys, Zs)) -> append2_3_out_gag₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_sublist_2_in_2_gg₄(X, Y, V, append2_3_out_gag₃(V, W, Y)) -> sublist_2_out_gg₂(X, Y)

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:

sublist_2_in_gg₂(X, Y) -> if_sublist_2_in_1_gg₃(X, Y, append1_3_in_aga₃(U, X, V))
append1_3_in_aga₃([]_0, Ys, Ys) -> append1_3_out_aga₃([]_0, Ys, Ys)
append1_3_in_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_append1_3_in_1_aga₅(X, Xs, Ys, Zs, append1_3_in_aga₃(Xs, Ys, Zs))
if_append1_3_in_1_aga₅(X, Xs, Ys, Zs, append1_3_out_aga₃(Xs, Ys, Zs)) -> append1_3_out_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_sublist_2_in_1_gg₃(X, Y, append1_3_out_aga₃(U, X, V)) -> if_sublist_2_in_2_gg₄(X, Y, V, append2_3_in_gag₃(V, W, Y))
append2_3_in_gag₃([]_0, Ys, Ys) -> append2_3_out_gag₃([]_0, Ys, Ys)
append2_3_in_gag₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_append2_3_in_1_gag₅(X, Xs, Ys, Zs, append2_3_in_gag₃(Xs, Ys, Zs))
if_append2_3_in_1_gag₅(X, Xs, Ys, Zs, append2_3_out_gag₃(Xs, Ys, Zs)) -> append2_3_out_gag₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_sublist_2_in_2_gg₄(X, Y, V, append2_3_out_gag₃(V, W, Y)) -> sublist_2_out_gg₂(X, Y)

SUBLIST_2_IN_GG₂(X, Y) -> IF_SUBLIST_2_IN_1_GG₃(X, Y, append1_3_in_aga₃(U, X, V))
SUBLIST_2_IN_GG₂(X, Y) -> APPEND1_3_IN_AGA₃(U, X, V)
APPEND1_3_IN_AGA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> IF_APPEND1_3_IN_1_AGA₅(X, Xs, Ys, Zs, append1_3_in_aga₃(Xs, Ys, Zs))
APPEND1_3_IN_AGA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> APPEND1_3_IN_AGA₃(Xs, Ys, Zs)
IF_SUBLIST_2_IN_1_GG₃(X, Y, append1_3_out_aga₃(U, X, V)) -> IF_SUBLIST_2_IN_2_GG₄(X, Y, V, append2_3_in_gag₃(V, W, Y))
IF_SUBLIST_2_IN_1_GG₃(X, Y, append1_3_out_aga₃(U, X, V)) -> APPEND2_3_IN_GAG₃(V, W, Y)
APPEND2_3_IN_GAG₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> IF_APPEND2_3_IN_1_GAG₅(X, Xs, Ys, Zs, append2_3_in_gag₃(Xs, Ys, Zs))
APPEND2_3_IN_GAG₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> APPEND2_3_IN_GAG₃(Xs, Ys, Zs)

The TRS R consists of the following rules:

sublist_2_in_gg₂(X, Y) -> if_sublist_2_in_1_gg₃(X, Y, append1_3_in_aga₃(U, X, V))
append1_3_in_aga₃([]_0, Ys, Ys) -> append1_3_out_aga₃([]_0, Ys, Ys)
append1_3_in_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_append1_3_in_1_aga₅(X, Xs, Ys, Zs, append1_3_in_aga₃(Xs, Ys, Zs))
if_append1_3_in_1_aga₅(X, Xs, Ys, Zs, append1_3_out_aga₃(Xs, Ys, Zs)) -> append1_3_out_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_sublist_2_in_1_gg₃(X, Y, append1_3_out_aga₃(U, X, V)) -> if_sublist_2_in_2_gg₄(X, Y, V, append2_3_in_gag₃(V, W, Y))
append2_3_in_gag₃([]_0, Ys, Ys) -> append2_3_out_gag₃([]_0, Ys, Ys)
append2_3_in_gag₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_append2_3_in_1_gag₅(X, Xs, Ys, Zs, append2_3_in_gag₃(Xs, Ys, Zs))
if_append2_3_in_1_gag₅(X, Xs, Ys, Zs, append2_3_out_gag₃(Xs, Ys, Zs)) -> append2_3_out_gag₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_sublist_2_in_2_gg₄(X, Y, V, append2_3_out_gag₃(V, W, Y)) -> sublist_2_out_gg₂(X, Y)

The argument filtering Pi contains the following mapping:
sublist_2_in_gg₂(x1, x2) = sublist_2_in_gg₂(x1, x2)
[]_0 = []_0
._2₂(x1, x2) = ._2₁(x2)
if_sublist_2_in_1_gg₃(x1, x2, x3) = if_sublist_2_in_1_gg₂(x2, x3)
append1_3_in_aga₃(x1, x2, x3) = append1_3_in_aga₁(x2)
append1_3_out_aga₃(x1, x2, x3) = append1_3_out_aga₂(x1, x3)
if_append1_3_in_1_aga₅(x1, x2, x3, x4, x5) = if_append1_3_in_1_aga₁(x5)
if_sublist_2_in_2_gg₄(x1, x2, x3, x4) = if_sublist_2_in_2_gg₁(x4)
append2_3_in_gag₃(x1, x2, x3) = append2_3_in_gag₂(x1, x3)
append2_3_out_gag₃(x1, x2, x3) = append2_3_out_gag₁(x2)
if_append2_3_in_1_gag₅(x1, x2, x3, x4, x5) = if_append2_3_in_1_gag₁(x5)
sublist_2_out_gg₂(x1, x2) = sublist_2_out_gg
IF_APPEND1_3_IN_1_AGA₅(x1, x2, x3, x4, x5) = IF_APPEND1_3_IN_1_AGA₁(x5)
SUBLIST_2_IN_GG₂(x1, x2) = SUBLIST_2_IN_GG₂(x1, x2)
IF_APPEND2_3_IN_1_GAG₅(x1, x2, x3, x4, x5) = IF_APPEND2_3_IN_1_GAG₁(x5)
APPEND1_3_IN_AGA₃(x1, x2, x3) = APPEND1_3_IN_AGA₁(x2)
IF_SUBLIST_2_IN_2_GG₄(x1, x2, x3, x4) = IF_SUBLIST_2_IN_2_GG₁(x4)
APPEND2_3_IN_GAG₃(x1, x2, x3) = APPEND2_3_IN_GAG₂(x1, x3)
IF_SUBLIST_2_IN_1_GG₃(x1, x2, x3) = IF_SUBLIST_2_IN_1_GG₂(x2, x3)

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:

SUBLIST_2_IN_GG₂(X, Y) -> IF_SUBLIST_2_IN_1_GG₃(X, Y, append1_3_in_aga₃(U, X, V))
SUBLIST_2_IN_GG₂(X, Y) -> APPEND1_3_IN_AGA₃(U, X, V)
APPEND1_3_IN_AGA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> IF_APPEND1_3_IN_1_AGA₅(X, Xs, Ys, Zs, append1_3_in_aga₃(Xs, Ys, Zs))
APPEND1_3_IN_AGA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> APPEND1_3_IN_AGA₃(Xs, Ys, Zs)
IF_SUBLIST_2_IN_1_GG₃(X, Y, append1_3_out_aga₃(U, X, V)) -> IF_SUBLIST_2_IN_2_GG₄(X, Y, V, append2_3_in_gag₃(V, W, Y))
IF_SUBLIST_2_IN_1_GG₃(X, Y, append1_3_out_aga₃(U, X, V)) -> APPEND2_3_IN_GAG₃(V, W, Y)
APPEND2_3_IN_GAG₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> IF_APPEND2_3_IN_1_GAG₅(X, Xs, Ys, Zs, append2_3_in_gag₃(Xs, Ys, Zs))
APPEND2_3_IN_GAG₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> APPEND2_3_IN_GAG₃(Xs, Ys, Zs)

The TRS R consists of the following rules:

sublist_2_in_gg₂(X, Y) -> if_sublist_2_in_1_gg₃(X, Y, append1_3_in_aga₃(U, X, V))
append1_3_in_aga₃([]_0, Ys, Ys) -> append1_3_out_aga₃([]_0, Ys, Ys)
append1_3_in_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_append1_3_in_1_aga₅(X, Xs, Ys, Zs, append1_3_in_aga₃(Xs, Ys, Zs))
if_append1_3_in_1_aga₅(X, Xs, Ys, Zs, append1_3_out_aga₃(Xs, Ys, Zs)) -> append1_3_out_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_sublist_2_in_1_gg₃(X, Y, append1_3_out_aga₃(U, X, V)) -> if_sublist_2_in_2_gg₄(X, Y, V, append2_3_in_gag₃(V, W, Y))
append2_3_in_gag₃([]_0, Ys, Ys) -> append2_3_out_gag₃([]_0, Ys, Ys)
append2_3_in_gag₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_append2_3_in_1_gag₅(X, Xs, Ys, Zs, append2_3_in_gag₃(Xs, Ys, Zs))
if_append2_3_in_1_gag₅(X, Xs, Ys, Zs, append2_3_out_gag₃(Xs, Ys, Zs)) -> append2_3_out_gag₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_sublist_2_in_2_gg₄(X, Y, V, append2_3_out_gag₃(V, W, Y)) -> sublist_2_out_gg₂(X, Y)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

APPEND2_3_IN_GAG₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> APPEND2_3_IN_GAG₃(Xs, Ys, Zs)

The TRS R consists of the following rules:

sublist_2_in_gg₂(X, Y) -> if_sublist_2_in_1_gg₃(X, Y, append1_3_in_aga₃(U, X, V))
append1_3_in_aga₃([]_0, Ys, Ys) -> append1_3_out_aga₃([]_0, Ys, Ys)
append1_3_in_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_append1_3_in_1_aga₅(X, Xs, Ys, Zs, append1_3_in_aga₃(Xs, Ys, Zs))
if_append1_3_in_1_aga₅(X, Xs, Ys, Zs, append1_3_out_aga₃(Xs, Ys, Zs)) -> append1_3_out_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_sublist_2_in_1_gg₃(X, Y, append1_3_out_aga₃(U, X, V)) -> if_sublist_2_in_2_gg₄(X, Y, V, append2_3_in_gag₃(V, W, Y))
append2_3_in_gag₃([]_0, Ys, Ys) -> append2_3_out_gag₃([]_0, Ys, Ys)
append2_3_in_gag₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_append2_3_in_1_gag₅(X, Xs, Ys, Zs, append2_3_in_gag₃(Xs, Ys, Zs))
if_append2_3_in_1_gag₅(X, Xs, Ys, Zs, append2_3_out_gag₃(Xs, Ys, Zs)) -> append2_3_out_gag₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_sublist_2_in_2_gg₄(X, Y, V, append2_3_out_gag₃(V, W, Y)) -> sublist_2_out_gg₂(X, Y)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

APPEND2_3_IN_GAG₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> APPEND2_3_IN_GAG₃(Xs, Ys, Zs)

R is empty.
The argument filtering Pi contains the following mapping:
._2₂(x1, x2) = ._2₁(x2)
APPEND2_3_IN_GAG₃(x1, x2, x3) = APPEND2_3_IN_GAG₂(x1, x3)

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

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

APPEND2_3_IN_GAG₂(._2₁(Xs), ._2₁(Zs)) -> APPEND2_3_IN_GAG₂(Xs, Zs)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {APPEND2_3_IN_GAG₂}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

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

APPEND2_3_IN_GAG₂(._2₁(Xs), ._2₁(Zs)) -> APPEND2_3_IN_GAG₂(Xs, Zs)
The graph contains the following edges 1 > 1, 2 > 2

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

  ↳ PrologToPiTRSProof

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

APPEND1_3_IN_AGA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> APPEND1_3_IN_AGA₃(Xs, Ys, Zs)

The TRS R consists of the following rules:

sublist_2_in_gg₂(X, Y) -> if_sublist_2_in_1_gg₃(X, Y, append1_3_in_aga₃(U, X, V))
append1_3_in_aga₃([]_0, Ys, Ys) -> append1_3_out_aga₃([]_0, Ys, Ys)
append1_3_in_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_append1_3_in_1_aga₅(X, Xs, Ys, Zs, append1_3_in_aga₃(Xs, Ys, Zs))
if_append1_3_in_1_aga₅(X, Xs, Ys, Zs, append1_3_out_aga₃(Xs, Ys, Zs)) -> append1_3_out_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_sublist_2_in_1_gg₃(X, Y, append1_3_out_aga₃(U, X, V)) -> if_sublist_2_in_2_gg₄(X, Y, V, append2_3_in_gag₃(V, W, Y))
append2_3_in_gag₃([]_0, Ys, Ys) -> append2_3_out_gag₃([]_0, Ys, Ys)
append2_3_in_gag₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_append2_3_in_1_gag₅(X, Xs, Ys, Zs, append2_3_in_gag₃(Xs, Ys, Zs))
if_append2_3_in_1_gag₅(X, Xs, Ys, Zs, append2_3_out_gag₃(Xs, Ys, Zs)) -> append2_3_out_gag₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_sublist_2_in_2_gg₄(X, Y, V, append2_3_out_gag₃(V, W, Y)) -> sublist_2_out_gg₂(X, Y)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

  ↳ PrologToPiTRSProof

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

APPEND1_3_IN_AGA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> APPEND1_3_IN_AGA₃(Xs, Ys, Zs)

R is empty.
The argument filtering Pi contains the following mapping:
._2₂(x1, x2) = ._2₁(x2)
APPEND1_3_IN_AGA₃(x1, x2, x3) = APPEND1_3_IN_AGA₁(x2)

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

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

  ↳ PrologToPiTRSProof

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

APPEND1_3_IN_AGA₁(Ys) -> APPEND1_3_IN_AGA₁(Ys)

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

sublist_2_in_gg₂(X, Y) -> if_sublist_2_in_1_gg₃(X, Y, append1_3_in_aga₃(U, X, V))
append1_3_in_aga₃([]_0, Ys, Ys) -> append1_3_out_aga₃([]_0, Ys, Ys)
append1_3_in_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_append1_3_in_1_aga₅(X, Xs, Ys, Zs, append1_3_in_aga₃(Xs, Ys, Zs))
if_append1_3_in_1_aga₅(X, Xs, Ys, Zs, append1_3_out_aga₃(Xs, Ys, Zs)) -> append1_3_out_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_sublist_2_in_1_gg₃(X, Y, append1_3_out_aga₃(U, X, V)) -> if_sublist_2_in_2_gg₄(X, Y, V, append2_3_in_gag₃(V, W, Y))
append2_3_in_gag₃([]_0, Ys, Ys) -> append2_3_out_gag₃([]_0, Ys, Ys)
append2_3_in_gag₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_append2_3_in_1_gag₅(X, Xs, Ys, Zs, append2_3_in_gag₃(Xs, Ys, Zs))
if_append2_3_in_1_gag₅(X, Xs, Ys, Zs, append2_3_out_gag₃(Xs, Ys, Zs)) -> append2_3_out_gag₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_sublist_2_in_2_gg₄(X, Y, V, append2_3_out_gag₃(V, W, Y)) -> sublist_2_out_gg₂(X, Y)

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:

sublist_2_in_gg₂(X, Y) -> if_sublist_2_in_1_gg₃(X, Y, append1_3_in_aga₃(U, X, V))
append1_3_in_aga₃([]_0, Ys, Ys) -> append1_3_out_aga₃([]_0, Ys, Ys)
append1_3_in_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_append1_3_in_1_aga₅(X, Xs, Ys, Zs, append1_3_in_aga₃(Xs, Ys, Zs))
if_append1_3_in_1_aga₅(X, Xs, Ys, Zs, append1_3_out_aga₃(Xs, Ys, Zs)) -> append1_3_out_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_sublist_2_in_1_gg₃(X, Y, append1_3_out_aga₃(U, X, V)) -> if_sublist_2_in_2_gg₄(X, Y, V, append2_3_in_gag₃(V, W, Y))
append2_3_in_gag₃([]_0, Ys, Ys) -> append2_3_out_gag₃([]_0, Ys, Ys)
append2_3_in_gag₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_append2_3_in_1_gag₅(X, Xs, Ys, Zs, append2_3_in_gag₃(Xs, Ys, Zs))
if_append2_3_in_1_gag₅(X, Xs, Ys, Zs, append2_3_out_gag₃(Xs, Ys, Zs)) -> append2_3_out_gag₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_sublist_2_in_2_gg₄(X, Y, V, append2_3_out_gag₃(V, W, Y)) -> sublist_2_out_gg₂(X, Y)

SUBLIST_2_IN_GG₂(X, Y) -> IF_SUBLIST_2_IN_1_GG₃(X, Y, append1_3_in_aga₃(U, X, V))
SUBLIST_2_IN_GG₂(X, Y) -> APPEND1_3_IN_AGA₃(U, X, V)
APPEND1_3_IN_AGA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> IF_APPEND1_3_IN_1_AGA₅(X, Xs, Ys, Zs, append1_3_in_aga₃(Xs, Ys, Zs))
APPEND1_3_IN_AGA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> APPEND1_3_IN_AGA₃(Xs, Ys, Zs)
IF_SUBLIST_2_IN_1_GG₃(X, Y, append1_3_out_aga₃(U, X, V)) -> IF_SUBLIST_2_IN_2_GG₄(X, Y, V, append2_3_in_gag₃(V, W, Y))
IF_SUBLIST_2_IN_1_GG₃(X, Y, append1_3_out_aga₃(U, X, V)) -> APPEND2_3_IN_GAG₃(V, W, Y)
APPEND2_3_IN_GAG₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> IF_APPEND2_3_IN_1_GAG₅(X, Xs, Ys, Zs, append2_3_in_gag₃(Xs, Ys, Zs))
APPEND2_3_IN_GAG₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> APPEND2_3_IN_GAG₃(Xs, Ys, Zs)

The TRS R consists of the following rules:

sublist_2_in_gg₂(X, Y) -> if_sublist_2_in_1_gg₃(X, Y, append1_3_in_aga₃(U, X, V))
append1_3_in_aga₃([]_0, Ys, Ys) -> append1_3_out_aga₃([]_0, Ys, Ys)
append1_3_in_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_append1_3_in_1_aga₅(X, Xs, Ys, Zs, append1_3_in_aga₃(Xs, Ys, Zs))
if_append1_3_in_1_aga₅(X, Xs, Ys, Zs, append1_3_out_aga₃(Xs, Ys, Zs)) -> append1_3_out_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_sublist_2_in_1_gg₃(X, Y, append1_3_out_aga₃(U, X, V)) -> if_sublist_2_in_2_gg₄(X, Y, V, append2_3_in_gag₃(V, W, Y))
append2_3_in_gag₃([]_0, Ys, Ys) -> append2_3_out_gag₃([]_0, Ys, Ys)
append2_3_in_gag₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_append2_3_in_1_gag₅(X, Xs, Ys, Zs, append2_3_in_gag₃(Xs, Ys, Zs))
if_append2_3_in_1_gag₅(X, Xs, Ys, Zs, append2_3_out_gag₃(Xs, Ys, Zs)) -> append2_3_out_gag₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_sublist_2_in_2_gg₄(X, Y, V, append2_3_out_gag₃(V, W, Y)) -> sublist_2_out_gg₂(X, Y)

The argument filtering Pi contains the following mapping:
sublist_2_in_gg₂(x1, x2) = sublist_2_in_gg₂(x1, x2)
[]_0 = []_0
._2₂(x1, x2) = ._2₁(x2)
if_sublist_2_in_1_gg₃(x1, x2, x3) = if_sublist_2_in_1_gg₃(x1, x2, x3)
append1_3_in_aga₃(x1, x2, x3) = append1_3_in_aga₁(x2)
append1_3_out_aga₃(x1, x2, x3) = append1_3_out_aga₃(x1, x2, x3)
if_append1_3_in_1_aga₅(x1, x2, x3, x4, x5) = if_append1_3_in_1_aga₂(x3, x5)
if_sublist_2_in_2_gg₄(x1, x2, x3, x4) = if_sublist_2_in_2_gg₃(x1, x2, x4)
append2_3_in_gag₃(x1, x2, x3) = append2_3_in_gag₂(x1, x3)
append2_3_out_gag₃(x1, x2, x3) = append2_3_out_gag₃(x1, x2, x3)
if_append2_3_in_1_gag₅(x1, x2, x3, x4, x5) = if_append2_3_in_1_gag₃(x2, x4, x5)
sublist_2_out_gg₂(x1, x2) = sublist_2_out_gg₂(x1, x2)
IF_APPEND1_3_IN_1_AGA₅(x1, x2, x3, x4, x5) = IF_APPEND1_3_IN_1_AGA₂(x3, x5)
SUBLIST_2_IN_GG₂(x1, x2) = SUBLIST_2_IN_GG₂(x1, x2)
IF_APPEND2_3_IN_1_GAG₅(x1, x2, x3, x4, x5) = IF_APPEND2_3_IN_1_GAG₃(x2, x4, x5)
APPEND1_3_IN_AGA₃(x1, x2, x3) = APPEND1_3_IN_AGA₁(x2)
IF_SUBLIST_2_IN_2_GG₄(x1, x2, x3, x4) = IF_SUBLIST_2_IN_2_GG₃(x1, x2, x4)
APPEND2_3_IN_GAG₃(x1, x2, x3) = APPEND2_3_IN_GAG₂(x1, x3)
IF_SUBLIST_2_IN_1_GG₃(x1, x2, x3) = IF_SUBLIST_2_IN_1_GG₃(x1, x2, x3)

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:

SUBLIST_2_IN_GG₂(X, Y) -> IF_SUBLIST_2_IN_1_GG₃(X, Y, append1_3_in_aga₃(U, X, V))
SUBLIST_2_IN_GG₂(X, Y) -> APPEND1_3_IN_AGA₃(U, X, V)
APPEND1_3_IN_AGA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> IF_APPEND1_3_IN_1_AGA₅(X, Xs, Ys, Zs, append1_3_in_aga₃(Xs, Ys, Zs))
APPEND1_3_IN_AGA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> APPEND1_3_IN_AGA₃(Xs, Ys, Zs)
IF_SUBLIST_2_IN_1_GG₃(X, Y, append1_3_out_aga₃(U, X, V)) -> IF_SUBLIST_2_IN_2_GG₄(X, Y, V, append2_3_in_gag₃(V, W, Y))
IF_SUBLIST_2_IN_1_GG₃(X, Y, append1_3_out_aga₃(U, X, V)) -> APPEND2_3_IN_GAG₃(V, W, Y)
APPEND2_3_IN_GAG₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> IF_APPEND2_3_IN_1_GAG₅(X, Xs, Ys, Zs, append2_3_in_gag₃(Xs, Ys, Zs))
APPEND2_3_IN_GAG₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> APPEND2_3_IN_GAG₃(Xs, Ys, Zs)

The TRS R consists of the following rules:

sublist_2_in_gg₂(X, Y) -> if_sublist_2_in_1_gg₃(X, Y, append1_3_in_aga₃(U, X, V))
append1_3_in_aga₃([]_0, Ys, Ys) -> append1_3_out_aga₃([]_0, Ys, Ys)
append1_3_in_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_append1_3_in_1_aga₅(X, Xs, Ys, Zs, append1_3_in_aga₃(Xs, Ys, Zs))
if_append1_3_in_1_aga₅(X, Xs, Ys, Zs, append1_3_out_aga₃(Xs, Ys, Zs)) -> append1_3_out_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_sublist_2_in_1_gg₃(X, Y, append1_3_out_aga₃(U, X, V)) -> if_sublist_2_in_2_gg₄(X, Y, V, append2_3_in_gag₃(V, W, Y))
append2_3_in_gag₃([]_0, Ys, Ys) -> append2_3_out_gag₃([]_0, Ys, Ys)
append2_3_in_gag₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_append2_3_in_1_gag₅(X, Xs, Ys, Zs, append2_3_in_gag₃(Xs, Ys, Zs))
if_append2_3_in_1_gag₅(X, Xs, Ys, Zs, append2_3_out_gag₃(Xs, Ys, Zs)) -> append2_3_out_gag₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_sublist_2_in_2_gg₄(X, Y, V, append2_3_out_gag₃(V, W, Y)) -> sublist_2_out_gg₂(X, Y)

The argument filtering Pi contains the following mapping:
sublist_2_in_gg₂(x1, x2) = sublist_2_in_gg₂(x1, x2)
[]_0 = []_0
._2₂(x1, x2) = ._2₁(x2)
if_sublist_2_in_1_gg₃(x1, x2, x3) = if_sublist_2_in_1_gg₃(x1, x2, x3)
append1_3_in_aga₃(x1, x2, x3) = append1_3_in_aga₁(x2)
append1_3_out_aga₃(x1, x2, x3) = append1_3_out_aga₃(x1, x2, x3)
if_append1_3_in_1_aga₅(x1, x2, x3, x4, x5) = if_append1_3_in_1_aga₂(x3, x5)
if_sublist_2_in_2_gg₄(x1, x2, x3, x4) = if_sublist_2_in_2_gg₃(x1, x2, x4)
append2_3_in_gag₃(x1, x2, x3) = append2_3_in_gag₂(x1, x3)
append2_3_out_gag₃(x1, x2, x3) = append2_3_out_gag₃(x1, x2, x3)
if_append2_3_in_1_gag₅(x1, x2, x3, x4, x5) = if_append2_3_in_1_gag₃(x2, x4, x5)
sublist_2_out_gg₂(x1, x2) = sublist_2_out_gg₂(x1, x2)
IF_APPEND1_3_IN_1_AGA₅(x1, x2, x3, x4, x5) = IF_APPEND1_3_IN_1_AGA₂(x3, x5)
SUBLIST_2_IN_GG₂(x1, x2) = SUBLIST_2_IN_GG₂(x1, x2)
IF_APPEND2_3_IN_1_GAG₅(x1, x2, x3, x4, x5) = IF_APPEND2_3_IN_1_GAG₃(x2, x4, x5)
APPEND1_3_IN_AGA₃(x1, x2, x3) = APPEND1_3_IN_AGA₁(x2)
IF_SUBLIST_2_IN_2_GG₄(x1, x2, x3, x4) = IF_SUBLIST_2_IN_2_GG₃(x1, x2, x4)
APPEND2_3_IN_GAG₃(x1, x2, x3) = APPEND2_3_IN_GAG₂(x1, x3)
IF_SUBLIST_2_IN_1_GG₃(x1, x2, x3) = IF_SUBLIST_2_IN_1_GG₃(x1, x2, x3)

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

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

APPEND2_3_IN_GAG₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> APPEND2_3_IN_GAG₃(Xs, Ys, Zs)

The TRS R consists of the following rules:

sublist_2_in_gg₂(X, Y) -> if_sublist_2_in_1_gg₃(X, Y, append1_3_in_aga₃(U, X, V))
append1_3_in_aga₃([]_0, Ys, Ys) -> append1_3_out_aga₃([]_0, Ys, Ys)
append1_3_in_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_append1_3_in_1_aga₅(X, Xs, Ys, Zs, append1_3_in_aga₃(Xs, Ys, Zs))
if_append1_3_in_1_aga₅(X, Xs, Ys, Zs, append1_3_out_aga₃(Xs, Ys, Zs)) -> append1_3_out_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_sublist_2_in_1_gg₃(X, Y, append1_3_out_aga₃(U, X, V)) -> if_sublist_2_in_2_gg₄(X, Y, V, append2_3_in_gag₃(V, W, Y))
append2_3_in_gag₃([]_0, Ys, Ys) -> append2_3_out_gag₃([]_0, Ys, Ys)
append2_3_in_gag₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_append2_3_in_1_gag₅(X, Xs, Ys, Zs, append2_3_in_gag₃(Xs, Ys, Zs))
if_append2_3_in_1_gag₅(X, Xs, Ys, Zs, append2_3_out_gag₃(Xs, Ys, Zs)) -> append2_3_out_gag₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_sublist_2_in_2_gg₄(X, Y, V, append2_3_out_gag₃(V, W, Y)) -> sublist_2_out_gg₂(X, Y)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

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

APPEND2_3_IN_GAG₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> APPEND2_3_IN_GAG₃(Xs, Ys, Zs)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

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

APPEND2_3_IN_GAG₂(._2₁(Xs), ._2₁(Zs)) -> APPEND2_3_IN_GAG₂(Xs, Zs)

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

APPEND2_3_IN_GAG₂(._2₁(Xs), ._2₁(Zs)) -> APPEND2_3_IN_GAG₂(Xs, Zs)
The graph contains the following edges 1 > 1, 2 > 2

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

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

APPEND1_3_IN_AGA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> APPEND1_3_IN_AGA₃(Xs, Ys, Zs)

The TRS R consists of the following rules:

sublist_2_in_gg₂(X, Y) -> if_sublist_2_in_1_gg₃(X, Y, append1_3_in_aga₃(U, X, V))
append1_3_in_aga₃([]_0, Ys, Ys) -> append1_3_out_aga₃([]_0, Ys, Ys)
append1_3_in_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_append1_3_in_1_aga₅(X, Xs, Ys, Zs, append1_3_in_aga₃(Xs, Ys, Zs))
if_append1_3_in_1_aga₅(X, Xs, Ys, Zs, append1_3_out_aga₃(Xs, Ys, Zs)) -> append1_3_out_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_sublist_2_in_1_gg₃(X, Y, append1_3_out_aga₃(U, X, V)) -> if_sublist_2_in_2_gg₄(X, Y, V, append2_3_in_gag₃(V, W, Y))
append2_3_in_gag₃([]_0, Ys, Ys) -> append2_3_out_gag₃([]_0, Ys, Ys)
append2_3_in_gag₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_append2_3_in_1_gag₅(X, Xs, Ys, Zs, append2_3_in_gag₃(Xs, Ys, Zs))
if_append2_3_in_1_gag₅(X, Xs, Ys, Zs, append2_3_out_gag₃(Xs, Ys, Zs)) -> append2_3_out_gag₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_sublist_2_in_2_gg₄(X, Y, V, append2_3_out_gag₃(V, W, Y)) -> sublist_2_out_gg₂(X, Y)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

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

APPEND1_3_IN_AGA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> APPEND1_3_IN_AGA₃(Xs, Ys, Zs)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

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

APPEND1_3_IN_AGA₁(Ys) -> APPEND1_3_IN_AGA₁(Ys)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {APPEND1_3_IN_AGA₁}.