Left Termination proof of /tmp/tmp3KS7

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

↳ PROLOG

  ↳ PrologToPiTRSProof

perm₂({}₀, {}₀).
perm₂(L, .₂(H, T)) :- append2₃(V, .₂(H, U), L), append1₃(V, U, W), perm₂(W, T).
append1₃({}₀, L, L).
append1₃(.₂(H, L1), L2, .₂(H, L3)) :- append1₃(L1, L2, L3).
append2₃({}₀, L, L).
append2₃(.₂(H, L1), L2, .₂(H, L3)) :- append2₃(L1, L2, L3).

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

perm_2_in_ga₂([]_0, []_0) -> perm_2_out_ga₂([]_0, []_0)
perm_2_in_ga₂(L, ._2₂(H, T)) -> if_perm_2_in_1_ga₄(L, H, T, append2_3_in_aag₃(V, ._2₂(H, U), L))
append2_3_in_aag₃([]_0, L, L) -> append2_3_out_aag₃([]_0, L, L)
append2_3_in_aag₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> if_append2_3_in_1_aag₅(H, L1, L2, L3, append2_3_in_aag₃(L1, L2, L3))
if_append2_3_in_1_aag₅(H, L1, L2, L3, append2_3_out_aag₃(L1, L2, L3)) -> append2_3_out_aag₃(._2₂(H, L1), L2, ._2₂(H, L3))
if_perm_2_in_1_ga₄(L, H, T, append2_3_out_aag₃(V, ._2₂(H, U), L)) -> if_perm_2_in_2_ga₆(L, H, T, V, U, append1_3_in_gga₃(V, U, W))
append1_3_in_gga₃([]_0, L, L) -> append1_3_out_gga₃([]_0, L, L)
append1_3_in_gga₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> if_append1_3_in_1_gga₅(H, L1, L2, L3, append1_3_in_gga₃(L1, L2, L3))
if_append1_3_in_1_gga₅(H, L1, L2, L3, append1_3_out_gga₃(L1, L2, L3)) -> append1_3_out_gga₃(._2₂(H, L1), L2, ._2₂(H, L3))
if_perm_2_in_2_ga₆(L, H, T, V, U, append1_3_out_gga₃(V, U, W)) -> if_perm_2_in_3_ga₅(L, H, T, W, perm_2_in_ga₂(W, T))
if_perm_2_in_3_ga₅(L, H, T, W, perm_2_out_ga₂(W, T)) -> perm_2_out_ga₂(L, ._2₂(H, T))

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:

perm_2_in_ga₂([]_0, []_0) -> perm_2_out_ga₂([]_0, []_0)
perm_2_in_ga₂(L, ._2₂(H, T)) -> if_perm_2_in_1_ga₄(L, H, T, append2_3_in_aag₃(V, ._2₂(H, U), L))
append2_3_in_aag₃([]_0, L, L) -> append2_3_out_aag₃([]_0, L, L)
append2_3_in_aag₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> if_append2_3_in_1_aag₅(H, L1, L2, L3, append2_3_in_aag₃(L1, L2, L3))
if_append2_3_in_1_aag₅(H, L1, L2, L3, append2_3_out_aag₃(L1, L2, L3)) -> append2_3_out_aag₃(._2₂(H, L1), L2, ._2₂(H, L3))
if_perm_2_in_1_ga₄(L, H, T, append2_3_out_aag₃(V, ._2₂(H, U), L)) -> if_perm_2_in_2_ga₆(L, H, T, V, U, append1_3_in_gga₃(V, U, W))
append1_3_in_gga₃([]_0, L, L) -> append1_3_out_gga₃([]_0, L, L)
append1_3_in_gga₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> if_append1_3_in_1_gga₅(H, L1, L2, L3, append1_3_in_gga₃(L1, L2, L3))
if_append1_3_in_1_gga₅(H, L1, L2, L3, append1_3_out_gga₃(L1, L2, L3)) -> append1_3_out_gga₃(._2₂(H, L1), L2, ._2₂(H, L3))
if_perm_2_in_2_ga₆(L, H, T, V, U, append1_3_out_gga₃(V, U, W)) -> if_perm_2_in_3_ga₅(L, H, T, W, perm_2_in_ga₂(W, T))
if_perm_2_in_3_ga₅(L, H, T, W, perm_2_out_ga₂(W, T)) -> perm_2_out_ga₂(L, ._2₂(H, T))

PERM_2_IN_GA₂(L, ._2₂(H, T)) -> IF_PERM_2_IN_1_GA₄(L, H, T, append2_3_in_aag₃(V, ._2₂(H, U), L))
PERM_2_IN_GA₂(L, ._2₂(H, T)) -> APPEND2_3_IN_AAG₃(V, ._2₂(H, U), L)
APPEND2_3_IN_AAG₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> IF_APPEND2_3_IN_1_AAG₅(H, L1, L2, L3, append2_3_in_aag₃(L1, L2, L3))
APPEND2_3_IN_AAG₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> APPEND2_3_IN_AAG₃(L1, L2, L3)
IF_PERM_2_IN_1_GA₄(L, H, T, append2_3_out_aag₃(V, ._2₂(H, U), L)) -> IF_PERM_2_IN_2_GA₆(L, H, T, V, U, append1_3_in_gga₃(V, U, W))
IF_PERM_2_IN_1_GA₄(L, H, T, append2_3_out_aag₃(V, ._2₂(H, U), L)) -> APPEND1_3_IN_GGA₃(V, U, W)
APPEND1_3_IN_GGA₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> IF_APPEND1_3_IN_1_GGA₅(H, L1, L2, L3, append1_3_in_gga₃(L1, L2, L3))
APPEND1_3_IN_GGA₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> APPEND1_3_IN_GGA₃(L1, L2, L3)
IF_PERM_2_IN_2_GA₆(L, H, T, V, U, append1_3_out_gga₃(V, U, W)) -> IF_PERM_2_IN_3_GA₅(L, H, T, W, perm_2_in_ga₂(W, T))
IF_PERM_2_IN_2_GA₆(L, H, T, V, U, append1_3_out_gga₃(V, U, W)) -> PERM_2_IN_GA₂(W, T)

The TRS R consists of the following rules:

perm_2_in_ga₂([]_0, []_0) -> perm_2_out_ga₂([]_0, []_0)
perm_2_in_ga₂(L, ._2₂(H, T)) -> if_perm_2_in_1_ga₄(L, H, T, append2_3_in_aag₃(V, ._2₂(H, U), L))
append2_3_in_aag₃([]_0, L, L) -> append2_3_out_aag₃([]_0, L, L)
append2_3_in_aag₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> if_append2_3_in_1_aag₅(H, L1, L2, L3, append2_3_in_aag₃(L1, L2, L3))
if_append2_3_in_1_aag₅(H, L1, L2, L3, append2_3_out_aag₃(L1, L2, L3)) -> append2_3_out_aag₃(._2₂(H, L1), L2, ._2₂(H, L3))
if_perm_2_in_1_ga₄(L, H, T, append2_3_out_aag₃(V, ._2₂(H, U), L)) -> if_perm_2_in_2_ga₆(L, H, T, V, U, append1_3_in_gga₃(V, U, W))
append1_3_in_gga₃([]_0, L, L) -> append1_3_out_gga₃([]_0, L, L)
append1_3_in_gga₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> if_append1_3_in_1_gga₅(H, L1, L2, L3, append1_3_in_gga₃(L1, L2, L3))
if_append1_3_in_1_gga₅(H, L1, L2, L3, append1_3_out_gga₃(L1, L2, L3)) -> append1_3_out_gga₃(._2₂(H, L1), L2, ._2₂(H, L3))
if_perm_2_in_2_ga₆(L, H, T, V, U, append1_3_out_gga₃(V, U, W)) -> if_perm_2_in_3_ga₅(L, H, T, W, perm_2_in_ga₂(W, T))
if_perm_2_in_3_ga₅(L, H, T, W, perm_2_out_ga₂(W, T)) -> perm_2_out_ga₂(L, ._2₂(H, T))

The argument filtering Pi contains the following mapping:
perm_2_in_ga₂(x1, x2) = perm_2_in_ga₁(x1)
[]_0 = []_0
._2₂(x1, x2) = ._2₂(x1, x2)
perm_2_out_ga₂(x1, x2) = perm_2_out_ga₁(x2)
if_perm_2_in_1_ga₄(x1, x2, x3, x4) = if_perm_2_in_1_ga₁(x4)
append2_3_in_aag₃(x1, x2, x3) = append2_3_in_aag₁(x3)
append2_3_out_aag₃(x1, x2, x3) = append2_3_out_aag₂(x1, x2)
if_append2_3_in_1_aag₅(x1, x2, x3, x4, x5) = if_append2_3_in_1_aag₂(x1, x5)
if_perm_2_in_2_ga₆(x1, x2, x3, x4, x5, x6) = if_perm_2_in_2_ga₂(x2, x6)
append1_3_in_gga₃(x1, x2, x3) = append1_3_in_gga₂(x1, x2)
append1_3_out_gga₃(x1, x2, x3) = append1_3_out_gga₁(x3)
if_append1_3_in_1_gga₅(x1, x2, x3, x4, x5) = if_append1_3_in_1_gga₂(x1, x5)
if_perm_2_in_3_ga₅(x1, x2, x3, x4, x5) = if_perm_2_in_3_ga₂(x2, x5)
IF_APPEND1_3_IN_1_GGA₅(x1, x2, x3, x4, x5) = IF_APPEND1_3_IN_1_GGA₂(x1, x5)
APPEND1_3_IN_GGA₃(x1, x2, x3) = APPEND1_3_IN_GGA₂(x1, x2)
APPEND2_3_IN_AAG₃(x1, x2, x3) = APPEND2_3_IN_AAG₁(x3)
IF_PERM_2_IN_3_GA₅(x1, x2, x3, x4, x5) = IF_PERM_2_IN_3_GA₂(x2, x5)
PERM_2_IN_GA₂(x1, x2) = PERM_2_IN_GA₁(x1)
IF_APPEND2_3_IN_1_AAG₅(x1, x2, x3, x4, x5) = IF_APPEND2_3_IN_1_AAG₂(x1, x5)
IF_PERM_2_IN_2_GA₆(x1, x2, x3, x4, x5, x6) = IF_PERM_2_IN_2_GA₂(x2, x6)
IF_PERM_2_IN_1_GA₄(x1, x2, x3, x4) = IF_PERM_2_IN_1_GA₁(x4)

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:

PERM_2_IN_GA₂(L, ._2₂(H, T)) -> IF_PERM_2_IN_1_GA₄(L, H, T, append2_3_in_aag₃(V, ._2₂(H, U), L))
PERM_2_IN_GA₂(L, ._2₂(H, T)) -> APPEND2_3_IN_AAG₃(V, ._2₂(H, U), L)
APPEND2_3_IN_AAG₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> IF_APPEND2_3_IN_1_AAG₅(H, L1, L2, L3, append2_3_in_aag₃(L1, L2, L3))
APPEND2_3_IN_AAG₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> APPEND2_3_IN_AAG₃(L1, L2, L3)
IF_PERM_2_IN_1_GA₄(L, H, T, append2_3_out_aag₃(V, ._2₂(H, U), L)) -> IF_PERM_2_IN_2_GA₆(L, H, T, V, U, append1_3_in_gga₃(V, U, W))
IF_PERM_2_IN_1_GA₄(L, H, T, append2_3_out_aag₃(V, ._2₂(H, U), L)) -> APPEND1_3_IN_GGA₃(V, U, W)
APPEND1_3_IN_GGA₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> IF_APPEND1_3_IN_1_GGA₅(H, L1, L2, L3, append1_3_in_gga₃(L1, L2, L3))
APPEND1_3_IN_GGA₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> APPEND1_3_IN_GGA₃(L1, L2, L3)
IF_PERM_2_IN_2_GA₆(L, H, T, V, U, append1_3_out_gga₃(V, U, W)) -> IF_PERM_2_IN_3_GA₅(L, H, T, W, perm_2_in_ga₂(W, T))
IF_PERM_2_IN_2_GA₆(L, H, T, V, U, append1_3_out_gga₃(V, U, W)) -> PERM_2_IN_GA₂(W, T)

The TRS R consists of the following rules:

perm_2_in_ga₂([]_0, []_0) -> perm_2_out_ga₂([]_0, []_0)
perm_2_in_ga₂(L, ._2₂(H, T)) -> if_perm_2_in_1_ga₄(L, H, T, append2_3_in_aag₃(V, ._2₂(H, U), L))
append2_3_in_aag₃([]_0, L, L) -> append2_3_out_aag₃([]_0, L, L)
append2_3_in_aag₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> if_append2_3_in_1_aag₅(H, L1, L2, L3, append2_3_in_aag₃(L1, L2, L3))
if_append2_3_in_1_aag₅(H, L1, L2, L3, append2_3_out_aag₃(L1, L2, L3)) -> append2_3_out_aag₃(._2₂(H, L1), L2, ._2₂(H, L3))
if_perm_2_in_1_ga₄(L, H, T, append2_3_out_aag₃(V, ._2₂(H, U), L)) -> if_perm_2_in_2_ga₆(L, H, T, V, U, append1_3_in_gga₃(V, U, W))
append1_3_in_gga₃([]_0, L, L) -> append1_3_out_gga₃([]_0, L, L)
append1_3_in_gga₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> if_append1_3_in_1_gga₅(H, L1, L2, L3, append1_3_in_gga₃(L1, L2, L3))
if_append1_3_in_1_gga₅(H, L1, L2, L3, append1_3_out_gga₃(L1, L2, L3)) -> append1_3_out_gga₃(._2₂(H, L1), L2, ._2₂(H, L3))
if_perm_2_in_2_ga₆(L, H, T, V, U, append1_3_out_gga₃(V, U, W)) -> if_perm_2_in_3_ga₅(L, H, T, W, perm_2_in_ga₂(W, T))
if_perm_2_in_3_ga₅(L, H, T, W, perm_2_out_ga₂(W, T)) -> perm_2_out_ga₂(L, ._2₂(H, T))

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

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

APPEND1_3_IN_GGA₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> APPEND1_3_IN_GGA₃(L1, L2, L3)

The TRS R consists of the following rules:

perm_2_in_ga₂([]_0, []_0) -> perm_2_out_ga₂([]_0, []_0)
perm_2_in_ga₂(L, ._2₂(H, T)) -> if_perm_2_in_1_ga₄(L, H, T, append2_3_in_aag₃(V, ._2₂(H, U), L))
append2_3_in_aag₃([]_0, L, L) -> append2_3_out_aag₃([]_0, L, L)
append2_3_in_aag₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> if_append2_3_in_1_aag₅(H, L1, L2, L3, append2_3_in_aag₃(L1, L2, L3))
if_append2_3_in_1_aag₅(H, L1, L2, L3, append2_3_out_aag₃(L1, L2, L3)) -> append2_3_out_aag₃(._2₂(H, L1), L2, ._2₂(H, L3))
if_perm_2_in_1_ga₄(L, H, T, append2_3_out_aag₃(V, ._2₂(H, U), L)) -> if_perm_2_in_2_ga₆(L, H, T, V, U, append1_3_in_gga₃(V, U, W))
append1_3_in_gga₃([]_0, L, L) -> append1_3_out_gga₃([]_0, L, L)
append1_3_in_gga₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> if_append1_3_in_1_gga₅(H, L1, L2, L3, append1_3_in_gga₃(L1, L2, L3))
if_append1_3_in_1_gga₅(H, L1, L2, L3, append1_3_out_gga₃(L1, L2, L3)) -> append1_3_out_gga₃(._2₂(H, L1), L2, ._2₂(H, L3))
if_perm_2_in_2_ga₆(L, H, T, V, U, append1_3_out_gga₃(V, U, W)) -> if_perm_2_in_3_ga₅(L, H, T, W, perm_2_in_ga₂(W, T))
if_perm_2_in_3_ga₅(L, H, T, W, perm_2_out_ga₂(W, T)) -> perm_2_out_ga₂(L, ._2₂(H, T))

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

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

APPEND1_3_IN_GGA₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> APPEND1_3_IN_GGA₃(L1, L2, L3)

R is empty.
The argument filtering Pi contains the following mapping:
._2₂(x1, x2) = ._2₂(x1, x2)
APPEND1_3_IN_GGA₃(x1, x2, x3) = APPEND1_3_IN_GGA₂(x1, 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

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

              ↳ PiDP

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

APPEND1_3_IN_GGA₂(._2₂(H, L1), L2) -> APPEND1_3_IN_GGA₂(L1, L2)

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_GGA₂}.
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:

APPEND1_3_IN_GGA₂(._2₂(H, L1), L2) -> APPEND1_3_IN_GGA₂(L1, L2)
The graph contains the following edges 1 > 1, 2 >= 2

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

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

APPEND2_3_IN_AAG₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> APPEND2_3_IN_AAG₃(L1, L2, L3)

The TRS R consists of the following rules:

perm_2_in_ga₂([]_0, []_0) -> perm_2_out_ga₂([]_0, []_0)
perm_2_in_ga₂(L, ._2₂(H, T)) -> if_perm_2_in_1_ga₄(L, H, T, append2_3_in_aag₃(V, ._2₂(H, U), L))
append2_3_in_aag₃([]_0, L, L) -> append2_3_out_aag₃([]_0, L, L)
append2_3_in_aag₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> if_append2_3_in_1_aag₅(H, L1, L2, L3, append2_3_in_aag₃(L1, L2, L3))
if_append2_3_in_1_aag₅(H, L1, L2, L3, append2_3_out_aag₃(L1, L2, L3)) -> append2_3_out_aag₃(._2₂(H, L1), L2, ._2₂(H, L3))
if_perm_2_in_1_ga₄(L, H, T, append2_3_out_aag₃(V, ._2₂(H, U), L)) -> if_perm_2_in_2_ga₆(L, H, T, V, U, append1_3_in_gga₃(V, U, W))
append1_3_in_gga₃([]_0, L, L) -> append1_3_out_gga₃([]_0, L, L)
append1_3_in_gga₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> if_append1_3_in_1_gga₅(H, L1, L2, L3, append1_3_in_gga₃(L1, L2, L3))
if_append1_3_in_1_gga₅(H, L1, L2, L3, append1_3_out_gga₃(L1, L2, L3)) -> append1_3_out_gga₃(._2₂(H, L1), L2, ._2₂(H, L3))
if_perm_2_in_2_ga₆(L, H, T, V, U, append1_3_out_gga₃(V, U, W)) -> if_perm_2_in_3_ga₅(L, H, T, W, perm_2_in_ga₂(W, T))
if_perm_2_in_3_ga₅(L, H, T, W, perm_2_out_ga₂(W, T)) -> perm_2_out_ga₂(L, ._2₂(H, T))

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

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

APPEND2_3_IN_AAG₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> APPEND2_3_IN_AAG₃(L1, L2, L3)

R is empty.
The argument filtering Pi contains the following mapping:
._2₂(x1, x2) = ._2₂(x1, x2)
APPEND2_3_IN_AAG₃(x1, x2, x3) = APPEND2_3_IN_AAG₁(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

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

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

APPEND2_3_IN_AAG₁(._2₂(H, L3)) -> APPEND2_3_IN_AAG₁(L3)

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_AAG₁}.
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_AAG₁(._2₂(H, L3)) -> APPEND2_3_IN_AAG₁(L3)
The graph contains the following edges 1 > 1

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

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

PERM_2_IN_GA₂(L, ._2₂(H, T)) -> IF_PERM_2_IN_1_GA₄(L, H, T, append2_3_in_aag₃(V, ._2₂(H, U), L))
IF_PERM_2_IN_2_GA₆(L, H, T, V, U, append1_3_out_gga₃(V, U, W)) -> PERM_2_IN_GA₂(W, T)
IF_PERM_2_IN_1_GA₄(L, H, T, append2_3_out_aag₃(V, ._2₂(H, U), L)) -> IF_PERM_2_IN_2_GA₆(L, H, T, V, U, append1_3_in_gga₃(V, U, W))

The TRS R consists of the following rules:

perm_2_in_ga₂([]_0, []_0) -> perm_2_out_ga₂([]_0, []_0)
perm_2_in_ga₂(L, ._2₂(H, T)) -> if_perm_2_in_1_ga₄(L, H, T, append2_3_in_aag₃(V, ._2₂(H, U), L))
append2_3_in_aag₃([]_0, L, L) -> append2_3_out_aag₃([]_0, L, L)
append2_3_in_aag₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> if_append2_3_in_1_aag₅(H, L1, L2, L3, append2_3_in_aag₃(L1, L2, L3))
if_append2_3_in_1_aag₅(H, L1, L2, L3, append2_3_out_aag₃(L1, L2, L3)) -> append2_3_out_aag₃(._2₂(H, L1), L2, ._2₂(H, L3))
if_perm_2_in_1_ga₄(L, H, T, append2_3_out_aag₃(V, ._2₂(H, U), L)) -> if_perm_2_in_2_ga₆(L, H, T, V, U, append1_3_in_gga₃(V, U, W))
append1_3_in_gga₃([]_0, L, L) -> append1_3_out_gga₃([]_0, L, L)
append1_3_in_gga₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> if_append1_3_in_1_gga₅(H, L1, L2, L3, append1_3_in_gga₃(L1, L2, L3))
if_append1_3_in_1_gga₅(H, L1, L2, L3, append1_3_out_gga₃(L1, L2, L3)) -> append1_3_out_gga₃(._2₂(H, L1), L2, ._2₂(H, L3))
if_perm_2_in_2_ga₆(L, H, T, V, U, append1_3_out_gga₃(V, U, W)) -> if_perm_2_in_3_ga₅(L, H, T, W, perm_2_in_ga₂(W, T))
if_perm_2_in_3_ga₅(L, H, T, W, perm_2_out_ga₂(W, T)) -> perm_2_out_ga₂(L, ._2₂(H, T))

The argument filtering Pi contains the following mapping:
perm_2_in_ga₂(x1, x2) = perm_2_in_ga₁(x1)
[]_0 = []_0
._2₂(x1, x2) = ._2₂(x1, x2)
perm_2_out_ga₂(x1, x2) = perm_2_out_ga₁(x2)
if_perm_2_in_1_ga₄(x1, x2, x3, x4) = if_perm_2_in_1_ga₁(x4)
append2_3_in_aag₃(x1, x2, x3) = append2_3_in_aag₁(x3)
append2_3_out_aag₃(x1, x2, x3) = append2_3_out_aag₂(x1, x2)
if_append2_3_in_1_aag₅(x1, x2, x3, x4, x5) = if_append2_3_in_1_aag₂(x1, x5)
if_perm_2_in_2_ga₆(x1, x2, x3, x4, x5, x6) = if_perm_2_in_2_ga₂(x2, x6)
append1_3_in_gga₃(x1, x2, x3) = append1_3_in_gga₂(x1, x2)
append1_3_out_gga₃(x1, x2, x3) = append1_3_out_gga₁(x3)
if_append1_3_in_1_gga₅(x1, x2, x3, x4, x5) = if_append1_3_in_1_gga₂(x1, x5)
if_perm_2_in_3_ga₅(x1, x2, x3, x4, x5) = if_perm_2_in_3_ga₂(x2, x5)
PERM_2_IN_GA₂(x1, x2) = PERM_2_IN_GA₁(x1)
IF_PERM_2_IN_2_GA₆(x1, x2, x3, x4, x5, x6) = IF_PERM_2_IN_2_GA₂(x2, x6)
IF_PERM_2_IN_1_GA₄(x1, x2, x3, x4) = IF_PERM_2_IN_1_GA₁(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

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

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

PERM_2_IN_GA₂(L, ._2₂(H, T)) -> IF_PERM_2_IN_1_GA₄(L, H, T, append2_3_in_aag₃(V, ._2₂(H, U), L))
IF_PERM_2_IN_2_GA₆(L, H, T, V, U, append1_3_out_gga₃(V, U, W)) -> PERM_2_IN_GA₂(W, T)
IF_PERM_2_IN_1_GA₄(L, H, T, append2_3_out_aag₃(V, ._2₂(H, U), L)) -> IF_PERM_2_IN_2_GA₆(L, H, T, V, U, append1_3_in_gga₃(V, U, W))

The TRS R consists of the following rules:

append2_3_in_aag₃([]_0, L, L) -> append2_3_out_aag₃([]_0, L, L)
append2_3_in_aag₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> if_append2_3_in_1_aag₅(H, L1, L2, L3, append2_3_in_aag₃(L1, L2, L3))
append1_3_in_gga₃([]_0, L, L) -> append1_3_out_gga₃([]_0, L, L)
append1_3_in_gga₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> if_append1_3_in_1_gga₅(H, L1, L2, L3, append1_3_in_gga₃(L1, L2, L3))
if_append2_3_in_1_aag₅(H, L1, L2, L3, append2_3_out_aag₃(L1, L2, L3)) -> append2_3_out_aag₃(._2₂(H, L1), L2, ._2₂(H, L3))
if_append1_3_in_1_gga₅(H, L1, L2, L3, append1_3_out_gga₃(L1, L2, L3)) -> append1_3_out_gga₃(._2₂(H, L1), L2, ._2₂(H, L3))

The argument filtering Pi contains the following mapping:
[]_0 = []_0
._2₂(x1, x2) = ._2₂(x1, x2)
append2_3_in_aag₃(x1, x2, x3) = append2_3_in_aag₁(x3)
append2_3_out_aag₃(x1, x2, x3) = append2_3_out_aag₂(x1, x2)
if_append2_3_in_1_aag₅(x1, x2, x3, x4, x5) = if_append2_3_in_1_aag₂(x1, x5)
append1_3_in_gga₃(x1, x2, x3) = append1_3_in_gga₂(x1, x2)
append1_3_out_gga₃(x1, x2, x3) = append1_3_out_gga₁(x3)
if_append1_3_in_1_gga₅(x1, x2, x3, x4, x5) = if_append1_3_in_1_gga₂(x1, x5)
PERM_2_IN_GA₂(x1, x2) = PERM_2_IN_GA₁(x1)
IF_PERM_2_IN_2_GA₆(x1, x2, x3, x4, x5, x6) = IF_PERM_2_IN_2_GA₂(x2, x6)
IF_PERM_2_IN_1_GA₄(x1, x2, x3, x4) = IF_PERM_2_IN_1_GA₁(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

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ RuleRemovalProof

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

PERM_2_IN_GA₁(L) -> IF_PERM_2_IN_1_GA₁(append2_3_in_aag₁(L))
IF_PERM_2_IN_2_GA₂(H, append1_3_out_gga₁(W)) -> PERM_2_IN_GA₁(W)
IF_PERM_2_IN_1_GA₁(append2_3_out_aag₂(V, ._2₂(H, U))) -> IF_PERM_2_IN_2_GA₂(H, append1_3_in_gga₂(V, U))

The TRS R consists of the following rules:

append2_3_in_aag₁(L) -> append2_3_out_aag₂([]_0, L)
append2_3_in_aag₁(._2₂(H, L3)) -> if_append2_3_in_1_aag₂(H, append2_3_in_aag₁(L3))
append1_3_in_gga₂([]_0, L) -> append1_3_out_gga₁(L)
append1_3_in_gga₂(._2₂(H, L1), L2) -> if_append1_3_in_1_gga₂(H, append1_3_in_gga₂(L1, L2))
if_append2_3_in_1_aag₂(H, append2_3_out_aag₂(L1, L2)) -> append2_3_out_aag₂(._2₂(H, L1), L2)
if_append1_3_in_1_gga₂(H, append1_3_out_gga₁(L3)) -> append1_3_out_gga₁(._2₂(H, L3))

The set Q consists of the following terms:

append2_3_in_aag₁(x0)
append1_3_in_gga₂(x0, x1)
if_append2_3_in_1_aag₂(x0, x1)
if_append1_3_in_1_gga₂(x0, x1)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_PERM_2_IN_1_GA₁, PERM_2_IN_GA₁, IF_PERM_2_IN_2_GA₂}.
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:

append1_3_in_gga₂([]_0, L) -> append1_3_out_gga₁(L)

Used ordering: POLO with Polynomial interpretation:

POL(append2_3_in_aag₁(x₁)) = 2 + x₁
POL(._2₂(x₁, x₂)) = 1 + x₁ + x₂
POL(IF_PERM_2_IN_2_GA₂(x₁, x₂)) = 1 + x₁ + x₂
POL(append2_3_out_aag₂(x₁, x₂)) = x₁ + x₂
POL(append1_3_in_gga₂(x₁, x₂)) = x₁ + x₂
POL(IF_PERM_2_IN_1_GA₁(x₁)) = x₁
POL(if_append1_3_in_1_gga₂(x₁, x₂)) = 1 + x₁ + x₂
POL(if_append2_3_in_1_aag₂(x₁, x₂)) = 1 + x₁ + x₂
POL([]_0) = 2
POL(append1_3_out_gga₁(x₁)) = 1 + x₁
POL(PERM_2_IN_GA₁(x₁)) = 2 + x₁

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ RuleRemovalProof

                          ↳ QDP

                            ↳ QDPPoloProof

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

PERM_2_IN_GA₁(L) -> IF_PERM_2_IN_1_GA₁(append2_3_in_aag₁(L))
IF_PERM_2_IN_2_GA₂(H, append1_3_out_gga₁(W)) -> PERM_2_IN_GA₁(W)
IF_PERM_2_IN_1_GA₁(append2_3_out_aag₂(V, ._2₂(H, U))) -> IF_PERM_2_IN_2_GA₂(H, append1_3_in_gga₂(V, U))

The TRS R consists of the following rules:

append2_3_in_aag₁(L) -> append2_3_out_aag₂([]_0, L)
append2_3_in_aag₁(._2₂(H, L3)) -> if_append2_3_in_1_aag₂(H, append2_3_in_aag₁(L3))
append1_3_in_gga₂(._2₂(H, L1), L2) -> if_append1_3_in_1_gga₂(H, append1_3_in_gga₂(L1, L2))
if_append2_3_in_1_aag₂(H, append2_3_out_aag₂(L1, L2)) -> append2_3_out_aag₂(._2₂(H, L1), L2)
if_append1_3_in_1_gga₂(H, append1_3_out_gga₁(L3)) -> append1_3_out_gga₁(._2₂(H, L3))

The set Q consists of the following terms:

append2_3_in_aag₁(x0)
append1_3_in_gga₂(x0, x1)
if_append2_3_in_1_aag₂(x0, x1)
if_append1_3_in_1_gga₂(x0, x1)

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

IF_PERM_2_IN_2_GA₂(H, append1_3_out_gga₁(W)) -> PERM_2_IN_GA₁(W)

The remaining Dependency Pairs were at least non-strictly be oriented.

PERM_2_IN_GA₁(L) -> IF_PERM_2_IN_1_GA₁(append2_3_in_aag₁(L))
IF_PERM_2_IN_1_GA₁(append2_3_out_aag₂(V, ._2₂(H, U))) -> IF_PERM_2_IN_2_GA₂(H, append1_3_in_gga₂(V, U))

With the implicit AFS we had to orient the following set of usable rules non-strictly.

append1_3_in_gga₂(._2₂(H, L1), L2) -> if_append1_3_in_1_gga₂(H, append1_3_in_gga₂(L1, L2))
if_append1_3_in_1_gga₂(H, append1_3_out_gga₁(L3)) -> append1_3_out_gga₁(._2₂(H, L3))

Used ordering: POLO with Polynomial interpretation:

POL(._2₂(x₁, x₂)) = 0
POL(append2_3_in_aag₁(x₁)) = 0
POL(IF_PERM_2_IN_2_GA₂(x₁, x₂)) = x₂
POL(append2_3_out_aag₂(x₁, x₂)) = 0
POL(append1_3_in_gga₂(x₁, x₂)) = 0
POL(IF_PERM_2_IN_1_GA₁(x₁)) = 0
POL(if_append1_3_in_1_gga₂(x₁, x₂)) = x₂
POL(if_append2_3_in_1_aag₂(x₁, x₂)) = 0
POL([]_0) = 0
POL(append1_3_out_gga₁(x₁)) = 1
POL(PERM_2_IN_GA₁(x₁)) = 0

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ RuleRemovalProof

                          ↳ QDP

                            ↳ QDPPoloProof

                              ↳ QDP

                                ↳ DependencyGraphProof

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

PERM_2_IN_GA₁(L) -> IF_PERM_2_IN_1_GA₁(append2_3_in_aag₁(L))
IF_PERM_2_IN_1_GA₁(append2_3_out_aag₂(V, ._2₂(H, U))) -> IF_PERM_2_IN_2_GA₂(H, append1_3_in_gga₂(V, U))

The TRS R consists of the following rules:

append2_3_in_aag₁(L) -> append2_3_out_aag₂([]_0, L)
append2_3_in_aag₁(._2₂(H, L3)) -> if_append2_3_in_1_aag₂(H, append2_3_in_aag₁(L3))
append1_3_in_gga₂(._2₂(H, L1), L2) -> if_append1_3_in_1_gga₂(H, append1_3_in_gga₂(L1, L2))
if_append2_3_in_1_aag₂(H, append2_3_out_aag₂(L1, L2)) -> append2_3_out_aag₂(._2₂(H, L1), L2)
if_append1_3_in_1_gga₂(H, append1_3_out_gga₁(L3)) -> append1_3_out_gga₁(._2₂(H, L3))

The set Q consists of the following terms:

append2_3_in_aag₁(x0)
append1_3_in_gga₂(x0, x1)
if_append2_3_in_1_aag₂(x0, x1)
if_append1_3_in_1_gga₂(x0, x1)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_PERM_2_IN_1_GA₁, PERM_2_IN_GA₁, IF_PERM_2_IN_2_GA₂}.
The approximation of the Dependency Graph contains 0 SCCs with 2 less nodes.