Left Termination proof of /tmp/tmpTrXRS5/pl1.2

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

↳ PROLOG

  ↳ PrologToPiTRSProof

append2₂(parts₂({}₀, Y), is₁(sum₁(Y))).
append2₂(parts₂(.₂(H, X), Y), is₁(sum₁(.₂(H, Z)))) :- append2₂(parts₂(X, Y), is₁(sum₁(Z))).
append1₂(parts₂({}₀, Y), is₁(sum₁(Y))).
append1₂(parts₂(.₂(H, X), Y), is₁(sum₁(.₂(H, Z)))) :- append1₂(parts₂(X, Y), is₁(sum₁(Z))).
perm₂({}₀, {}₀).
perm₂(L, .₂(H, T)) :- append2₂(parts₂(V, .₂(H, U)), is₁(sum₁(L))), append1₂(parts₂(V, U), is₁(sum₁(W))), perm₂(W, T).

With regard to the inferred argument filtering the predicates were used in the following modes:
perm₂: (b,f)
append2₂: (f,b)
append1₂: (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_2_in_ag₂(parts_2₂(V, ._2₂(H, U)), is_1₁(sum_1₁(L))))
append2_2_in_ag₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y))) -> append2_2_out_ag₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y)))
append2_2_in_ag₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> if_append2_2_in_1_ag₅(H, X, Y, Z, append2_2_in_ag₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z))))
if_append2_2_in_1_ag₅(H, X, Y, Z, append2_2_out_ag₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z)))) -> append2_2_out_ag₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z))))
if_perm_2_in_1_ga₄(L, H, T, append2_2_out_ag₂(parts_2₂(V, ._2₂(H, U)), is_1₁(sum_1₁(L)))) -> if_perm_2_in_2_ga₆(L, H, T, V, U, append1_2_in_ga₂(parts_2₂(V, U), is_1₁(sum_1₁(W))))
append1_2_in_ga₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y))) -> append1_2_out_ga₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y)))
append1_2_in_ga₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> if_append1_2_in_1_ga₅(H, X, Y, Z, append1_2_in_ga₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z))))
if_append1_2_in_1_ga₅(H, X, Y, Z, append1_2_out_ga₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z)))) -> append1_2_out_ga₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z))))
if_perm_2_in_2_ga₆(L, H, T, V, U, append1_2_out_ga₂(parts_2₂(V, U), is_1₁(sum_1₁(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_2_in_ag₂(parts_2₂(V, ._2₂(H, U)), is_1₁(sum_1₁(L))))
append2_2_in_ag₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y))) -> append2_2_out_ag₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y)))
append2_2_in_ag₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> if_append2_2_in_1_ag₅(H, X, Y, Z, append2_2_in_ag₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z))))
if_append2_2_in_1_ag₅(H, X, Y, Z, append2_2_out_ag₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z)))) -> append2_2_out_ag₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z))))
if_perm_2_in_1_ga₄(L, H, T, append2_2_out_ag₂(parts_2₂(V, ._2₂(H, U)), is_1₁(sum_1₁(L)))) -> if_perm_2_in_2_ga₆(L, H, T, V, U, append1_2_in_ga₂(parts_2₂(V, U), is_1₁(sum_1₁(W))))
append1_2_in_ga₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y))) -> append1_2_out_ga₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y)))
append1_2_in_ga₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> if_append1_2_in_1_ga₅(H, X, Y, Z, append1_2_in_ga₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z))))
if_append1_2_in_1_ga₅(H, X, Y, Z, append1_2_out_ga₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z)))) -> append1_2_out_ga₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z))))
if_perm_2_in_2_ga₆(L, H, T, V, U, append1_2_out_ga₂(parts_2₂(V, U), is_1₁(sum_1₁(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_2_in_ag₂(parts_2₂(V, ._2₂(H, U)), is_1₁(sum_1₁(L))))
PERM_2_IN_GA₂(L, ._2₂(H, T)) -> APPEND2_2_IN_AG₂(parts_2₂(V, ._2₂(H, U)), is_1₁(sum_1₁(L)))
APPEND2_2_IN_AG₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> IF_APPEND2_2_IN_1_AG₅(H, X, Y, Z, append2_2_in_ag₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z))))
APPEND2_2_IN_AG₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> APPEND2_2_IN_AG₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z)))
IF_PERM_2_IN_1_GA₄(L, H, T, append2_2_out_ag₂(parts_2₂(V, ._2₂(H, U)), is_1₁(sum_1₁(L)))) -> IF_PERM_2_IN_2_GA₆(L, H, T, V, U, append1_2_in_ga₂(parts_2₂(V, U), is_1₁(sum_1₁(W))))
IF_PERM_2_IN_1_GA₄(L, H, T, append2_2_out_ag₂(parts_2₂(V, ._2₂(H, U)), is_1₁(sum_1₁(L)))) -> APPEND1_2_IN_GA₂(parts_2₂(V, U), is_1₁(sum_1₁(W)))
APPEND1_2_IN_GA₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> IF_APPEND1_2_IN_1_GA₅(H, X, Y, Z, append1_2_in_ga₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z))))
APPEND1_2_IN_GA₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> APPEND1_2_IN_GA₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z)))
IF_PERM_2_IN_2_GA₆(L, H, T, V, U, append1_2_out_ga₂(parts_2₂(V, U), is_1₁(sum_1₁(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_2_out_ga₂(parts_2₂(V, U), is_1₁(sum_1₁(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_2_in_ag₂(parts_2₂(V, ._2₂(H, U)), is_1₁(sum_1₁(L))))
append2_2_in_ag₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y))) -> append2_2_out_ag₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y)))
append2_2_in_ag₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> if_append2_2_in_1_ag₅(H, X, Y, Z, append2_2_in_ag₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z))))
if_append2_2_in_1_ag₅(H, X, Y, Z, append2_2_out_ag₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z)))) -> append2_2_out_ag₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z))))
if_perm_2_in_1_ga₄(L, H, T, append2_2_out_ag₂(parts_2₂(V, ._2₂(H, U)), is_1₁(sum_1₁(L)))) -> if_perm_2_in_2_ga₆(L, H, T, V, U, append1_2_in_ga₂(parts_2₂(V, U), is_1₁(sum_1₁(W))))
append1_2_in_ga₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y))) -> append1_2_out_ga₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y)))
append1_2_in_ga₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> if_append1_2_in_1_ga₅(H, X, Y, Z, append1_2_in_ga₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z))))
if_append1_2_in_1_ga₅(H, X, Y, Z, append1_2_out_ga₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z)))) -> append1_2_out_ga₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z))))
if_perm_2_in_2_ga₆(L, H, T, V, U, append1_2_out_ga₂(parts_2₂(V, U), is_1₁(sum_1₁(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)
parts_2₂(x1, x2) = parts_2₂(x1, x2)
[]_0 = []_0
is_1₁(x1) = is_1₁(x1)
sum_1₁(x1) = sum_1₁(x1)
._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_2_in_ag₂(x1, x2) = append2_2_in_ag₁(x2)
append2_2_out_ag₂(x1, x2) = append2_2_out_ag₁(x1)
if_append2_2_in_1_ag₅(x1, x2, x3, x4, x5) = if_append2_2_in_1_ag₂(x1, x5)
if_perm_2_in_2_ga₆(x1, x2, x3, x4, x5, x6) = if_perm_2_in_2_ga₂(x2, x6)
append1_2_in_ga₂(x1, x2) = append1_2_in_ga₁(x1)
append1_2_out_ga₂(x1, x2) = append1_2_out_ga₁(x2)
if_append1_2_in_1_ga₅(x1, x2, x3, x4, x5) = if_append1_2_in_1_ga₂(x1, x5)
if_perm_2_in_3_ga₅(x1, x2, x3, x4, x5) = if_perm_2_in_3_ga₂(x2, x5)
APPEND1_2_IN_GA₂(x1, x2) = APPEND1_2_IN_GA₁(x1)
IF_APPEND1_2_IN_1_GA₅(x1, x2, x3, x4, x5) = IF_APPEND1_2_IN_1_GA₂(x1, x5)
IF_APPEND2_2_IN_1_AG₅(x1, x2, x3, x4, x5) = IF_APPEND2_2_IN_1_AG₂(x1, x5)
IF_PERM_2_IN_3_GA₅(x1, x2, x3, x4, x5) = IF_PERM_2_IN_3_GA₂(x2, x5)
APPEND2_2_IN_AG₂(x1, x2) = APPEND2_2_IN_AG₁(x2)
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

↳ 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_2_in_ag₂(parts_2₂(V, ._2₂(H, U)), is_1₁(sum_1₁(L))))
PERM_2_IN_GA₂(L, ._2₂(H, T)) -> APPEND2_2_IN_AG₂(parts_2₂(V, ._2₂(H, U)), is_1₁(sum_1₁(L)))
APPEND2_2_IN_AG₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> IF_APPEND2_2_IN_1_AG₅(H, X, Y, Z, append2_2_in_ag₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z))))
APPEND2_2_IN_AG₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> APPEND2_2_IN_AG₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z)))
IF_PERM_2_IN_1_GA₄(L, H, T, append2_2_out_ag₂(parts_2₂(V, ._2₂(H, U)), is_1₁(sum_1₁(L)))) -> IF_PERM_2_IN_2_GA₆(L, H, T, V, U, append1_2_in_ga₂(parts_2₂(V, U), is_1₁(sum_1₁(W))))
IF_PERM_2_IN_1_GA₄(L, H, T, append2_2_out_ag₂(parts_2₂(V, ._2₂(H, U)), is_1₁(sum_1₁(L)))) -> APPEND1_2_IN_GA₂(parts_2₂(V, U), is_1₁(sum_1₁(W)))
APPEND1_2_IN_GA₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> IF_APPEND1_2_IN_1_GA₅(H, X, Y, Z, append1_2_in_ga₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z))))
APPEND1_2_IN_GA₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> APPEND1_2_IN_GA₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z)))
IF_PERM_2_IN_2_GA₆(L, H, T, V, U, append1_2_out_ga₂(parts_2₂(V, U), is_1₁(sum_1₁(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_2_out_ga₂(parts_2₂(V, U), is_1₁(sum_1₁(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_2_in_ag₂(parts_2₂(V, ._2₂(H, U)), is_1₁(sum_1₁(L))))
append2_2_in_ag₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y))) -> append2_2_out_ag₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y)))
append2_2_in_ag₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> if_append2_2_in_1_ag₅(H, X, Y, Z, append2_2_in_ag₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z))))
if_append2_2_in_1_ag₅(H, X, Y, Z, append2_2_out_ag₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z)))) -> append2_2_out_ag₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z))))
if_perm_2_in_1_ga₄(L, H, T, append2_2_out_ag₂(parts_2₂(V, ._2₂(H, U)), is_1₁(sum_1₁(L)))) -> if_perm_2_in_2_ga₆(L, H, T, V, U, append1_2_in_ga₂(parts_2₂(V, U), is_1₁(sum_1₁(W))))
append1_2_in_ga₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y))) -> append1_2_out_ga₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y)))
append1_2_in_ga₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> if_append1_2_in_1_ga₅(H, X, Y, Z, append1_2_in_ga₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z))))
if_append1_2_in_1_ga₅(H, X, Y, Z, append1_2_out_ga₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z)))) -> append1_2_out_ga₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z))))
if_perm_2_in_2_ga₆(L, H, T, V, U, append1_2_out_ga₂(parts_2₂(V, U), is_1₁(sum_1₁(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_2_IN_GA₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> APPEND1_2_IN_GA₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z)))

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_2_in_ag₂(parts_2₂(V, ._2₂(H, U)), is_1₁(sum_1₁(L))))
append2_2_in_ag₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y))) -> append2_2_out_ag₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y)))
append2_2_in_ag₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> if_append2_2_in_1_ag₅(H, X, Y, Z, append2_2_in_ag₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z))))
if_append2_2_in_1_ag₅(H, X, Y, Z, append2_2_out_ag₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z)))) -> append2_2_out_ag₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z))))
if_perm_2_in_1_ga₄(L, H, T, append2_2_out_ag₂(parts_2₂(V, ._2₂(H, U)), is_1₁(sum_1₁(L)))) -> if_perm_2_in_2_ga₆(L, H, T, V, U, append1_2_in_ga₂(parts_2₂(V, U), is_1₁(sum_1₁(W))))
append1_2_in_ga₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y))) -> append1_2_out_ga₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y)))
append1_2_in_ga₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> if_append1_2_in_1_ga₅(H, X, Y, Z, append1_2_in_ga₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z))))
if_append1_2_in_1_ga₅(H, X, Y, Z, append1_2_out_ga₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z)))) -> append1_2_out_ga₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z))))
if_perm_2_in_2_ga₆(L, H, T, V, U, append1_2_out_ga₂(parts_2₂(V, U), is_1₁(sum_1₁(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_2_IN_GA₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> APPEND1_2_IN_GA₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z)))

R is empty.
The argument filtering Pi contains the following mapping:
parts_2₂(x1, x2) = parts_2₂(x1, x2)
is_1₁(x1) = is_1₁(x1)
sum_1₁(x1) = sum_1₁(x1)
._2₂(x1, x2) = ._2₂(x1, x2)
APPEND1_2_IN_GA₂(x1, x2) = APPEND1_2_IN_GA₁(x1)

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_2_IN_GA₁(parts_2₂(._2₂(H, X), Y)) -> APPEND1_2_IN_GA₁(parts_2₂(X, Y))

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

Order:Homeomorphic Embedding Order

AFS:
._2₂(x1, x2) = ._2₁(x2)
parts_2₂(x1, x2) = x1

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

APPEND1_2_IN_GA₁(parts_2₂(._2₂(H, X), Y)) -> APPEND1_2_IN_GA₁(parts_2₂(X, Y)) (allowed arguments on rhs = {1})
The graph contains the following edges 1 > 1

We oriented the following set of usable rules. none

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

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

APPEND2_2_IN_AG₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> APPEND2_2_IN_AG₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z)))

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_2_in_ag₂(parts_2₂(V, ._2₂(H, U)), is_1₁(sum_1₁(L))))
append2_2_in_ag₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y))) -> append2_2_out_ag₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y)))
append2_2_in_ag₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> if_append2_2_in_1_ag₅(H, X, Y, Z, append2_2_in_ag₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z))))
if_append2_2_in_1_ag₅(H, X, Y, Z, append2_2_out_ag₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z)))) -> append2_2_out_ag₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z))))
if_perm_2_in_1_ga₄(L, H, T, append2_2_out_ag₂(parts_2₂(V, ._2₂(H, U)), is_1₁(sum_1₁(L)))) -> if_perm_2_in_2_ga₆(L, H, T, V, U, append1_2_in_ga₂(parts_2₂(V, U), is_1₁(sum_1₁(W))))
append1_2_in_ga₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y))) -> append1_2_out_ga₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y)))
append1_2_in_ga₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> if_append1_2_in_1_ga₅(H, X, Y, Z, append1_2_in_ga₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z))))
if_append1_2_in_1_ga₅(H, X, Y, Z, append1_2_out_ga₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z)))) -> append1_2_out_ga₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z))))
if_perm_2_in_2_ga₆(L, H, T, V, U, append1_2_out_ga₂(parts_2₂(V, U), is_1₁(sum_1₁(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_2_IN_AG₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> APPEND2_2_IN_AG₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z)))

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

                        ↳ QDPSizeChangeProof

              ↳ PiDP

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

APPEND2_2_IN_AG₁(is_1₁(sum_1₁(._2₂(H, Z)))) -> APPEND2_2_IN_AG₁(is_1₁(sum_1₁(Z)))

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

Order:Homeomorphic Embedding Order

AFS:
is_1₁(x1) = x1
sum_1₁(x1) = x1
._2₂(x1, x2) = ._2₁(x2)

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

APPEND2_2_IN_AG₁(is_1₁(sum_1₁(._2₂(H, Z)))) -> APPEND2_2_IN_AG₁(is_1₁(sum_1₁(Z))) (allowed arguments on rhs = {1})
The graph contains the following edges 1 > 1

We oriented the following set of usable rules. none

↳ 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_2_in_ag₂(parts_2₂(V, ._2₂(H, U)), is_1₁(sum_1₁(L))))
IF_PERM_2_IN_2_GA₆(L, H, T, V, U, append1_2_out_ga₂(parts_2₂(V, U), is_1₁(sum_1₁(W)))) -> PERM_2_IN_GA₂(W, T)
IF_PERM_2_IN_1_GA₄(L, H, T, append2_2_out_ag₂(parts_2₂(V, ._2₂(H, U)), is_1₁(sum_1₁(L)))) -> IF_PERM_2_IN_2_GA₆(L, H, T, V, U, append1_2_in_ga₂(parts_2₂(V, U), is_1₁(sum_1₁(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_2_in_ag₂(parts_2₂(V, ._2₂(H, U)), is_1₁(sum_1₁(L))))
append2_2_in_ag₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y))) -> append2_2_out_ag₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y)))
append2_2_in_ag₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> if_append2_2_in_1_ag₅(H, X, Y, Z, append2_2_in_ag₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z))))
if_append2_2_in_1_ag₅(H, X, Y, Z, append2_2_out_ag₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z)))) -> append2_2_out_ag₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z))))
if_perm_2_in_1_ga₄(L, H, T, append2_2_out_ag₂(parts_2₂(V, ._2₂(H, U)), is_1₁(sum_1₁(L)))) -> if_perm_2_in_2_ga₆(L, H, T, V, U, append1_2_in_ga₂(parts_2₂(V, U), is_1₁(sum_1₁(W))))
append1_2_in_ga₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y))) -> append1_2_out_ga₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y)))
append1_2_in_ga₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> if_append1_2_in_1_ga₅(H, X, Y, Z, append1_2_in_ga₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z))))
if_append1_2_in_1_ga₅(H, X, Y, Z, append1_2_out_ga₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z)))) -> append1_2_out_ga₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z))))
if_perm_2_in_2_ga₆(L, H, T, V, U, append1_2_out_ga₂(parts_2₂(V, U), is_1₁(sum_1₁(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)
parts_2₂(x1, x2) = parts_2₂(x1, x2)
[]_0 = []_0
is_1₁(x1) = is_1₁(x1)
sum_1₁(x1) = sum_1₁(x1)
._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_2_in_ag₂(x1, x2) = append2_2_in_ag₁(x2)
append2_2_out_ag₂(x1, x2) = append2_2_out_ag₁(x1)
if_append2_2_in_1_ag₅(x1, x2, x3, x4, x5) = if_append2_2_in_1_ag₂(x1, x5)
if_perm_2_in_2_ga₆(x1, x2, x3, x4, x5, x6) = if_perm_2_in_2_ga₂(x2, x6)
append1_2_in_ga₂(x1, x2) = append1_2_in_ga₁(x1)
append1_2_out_ga₂(x1, x2) = append1_2_out_ga₁(x2)
if_append1_2_in_1_ga₅(x1, x2, x3, x4, x5) = if_append1_2_in_1_ga₂(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_2_in_ag₂(parts_2₂(V, ._2₂(H, U)), is_1₁(sum_1₁(L))))
IF_PERM_2_IN_2_GA₆(L, H, T, V, U, append1_2_out_ga₂(parts_2₂(V, U), is_1₁(sum_1₁(W)))) -> PERM_2_IN_GA₂(W, T)
IF_PERM_2_IN_1_GA₄(L, H, T, append2_2_out_ag₂(parts_2₂(V, ._2₂(H, U)), is_1₁(sum_1₁(L)))) -> IF_PERM_2_IN_2_GA₆(L, H, T, V, U, append1_2_in_ga₂(parts_2₂(V, U), is_1₁(sum_1₁(W))))

The TRS R consists of the following rules:

append2_2_in_ag₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y))) -> append2_2_out_ag₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y)))
append2_2_in_ag₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> if_append2_2_in_1_ag₅(H, X, Y, Z, append2_2_in_ag₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z))))
append1_2_in_ga₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y))) -> append1_2_out_ga₂(parts_2₂([]_0, Y), is_1₁(sum_1₁(Y)))
append1_2_in_ga₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z)))) -> if_append1_2_in_1_ga₅(H, X, Y, Z, append1_2_in_ga₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z))))
if_append2_2_in_1_ag₅(H, X, Y, Z, append2_2_out_ag₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z)))) -> append2_2_out_ag₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z))))
if_append1_2_in_1_ga₅(H, X, Y, Z, append1_2_out_ga₂(parts_2₂(X, Y), is_1₁(sum_1₁(Z)))) -> append1_2_out_ga₂(parts_2₂(._2₂(H, X), Y), is_1₁(sum_1₁(._2₂(H, Z))))

The argument filtering Pi contains the following mapping:
parts_2₂(x1, x2) = parts_2₂(x1, x2)
[]_0 = []_0
is_1₁(x1) = is_1₁(x1)
sum_1₁(x1) = sum_1₁(x1)
._2₂(x1, x2) = ._2₂(x1, x2)
append2_2_in_ag₂(x1, x2) = append2_2_in_ag₁(x2)
append2_2_out_ag₂(x1, x2) = append2_2_out_ag₁(x1)
if_append2_2_in_1_ag₅(x1, x2, x3, x4, x5) = if_append2_2_in_1_ag₂(x1, x5)
append1_2_in_ga₂(x1, x2) = append1_2_in_ga₁(x1)
append1_2_out_ga₂(x1, x2) = append1_2_out_ga₁(x2)
if_append1_2_in_1_ga₅(x1, x2, x3, x4, x5) = if_append1_2_in_1_ga₂(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

                        ↳ QDPPoloProof

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

PERM_2_IN_GA₁(L) -> IF_PERM_2_IN_1_GA₁(append2_2_in_ag₁(is_1₁(sum_1₁(L))))
IF_PERM_2_IN_2_GA₂(H, append1_2_out_ga₁(is_1₁(sum_1₁(W)))) -> PERM_2_IN_GA₁(W)
IF_PERM_2_IN_1_GA₁(append2_2_out_ag₁(parts_2₂(V, ._2₂(H, U)))) -> IF_PERM_2_IN_2_GA₂(H, append1_2_in_ga₁(parts_2₂(V, U)))

The TRS R consists of the following rules:

append2_2_in_ag₁(is_1₁(sum_1₁(Y))) -> append2_2_out_ag₁(parts_2₂([]_0, Y))
append2_2_in_ag₁(is_1₁(sum_1₁(._2₂(H, Z)))) -> if_append2_2_in_1_ag₂(H, append2_2_in_ag₁(is_1₁(sum_1₁(Z))))
append1_2_in_ga₁(parts_2₂([]_0, Y)) -> append1_2_out_ga₁(is_1₁(sum_1₁(Y)))
append1_2_in_ga₁(parts_2₂(._2₂(H, X), Y)) -> if_append1_2_in_1_ga₂(H, append1_2_in_ga₁(parts_2₂(X, Y)))
if_append2_2_in_1_ag₂(H, append2_2_out_ag₁(parts_2₂(X, Y))) -> append2_2_out_ag₁(parts_2₂(._2₂(H, X), Y))
if_append1_2_in_1_ga₂(H, append1_2_out_ga₁(is_1₁(sum_1₁(Z)))) -> append1_2_out_ga₁(is_1₁(sum_1₁(._2₂(H, Z))))

The set Q consists of the following terms:

append2_2_in_ag₁(x0)
append1_2_in_ga₁(x0)
if_append2_2_in_1_ag₂(x0, x1)
if_append1_2_in_1_ga₂(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_1_GA₁(append2_2_out_ag₁(parts_2₂(V, ._2₂(H, U)))) -> IF_PERM_2_IN_2_GA₂(H, append1_2_in_ga₁(parts_2₂(V, U)))

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

PERM_2_IN_GA₁(L) -> IF_PERM_2_IN_1_GA₁(append2_2_in_ag₁(is_1₁(sum_1₁(L))))
IF_PERM_2_IN_2_GA₂(H, append1_2_out_ga₁(is_1₁(sum_1₁(W)))) -> PERM_2_IN_GA₁(W)

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

append1_2_in_ga₁(parts_2₂(._2₂(H, X), Y)) -> if_append1_2_in_1_ga₂(H, append1_2_in_ga₁(parts_2₂(X, Y)))
if_append1_2_in_1_ga₂(H, append1_2_out_ga₁(is_1₁(sum_1₁(Z)))) -> append1_2_out_ga₁(is_1₁(sum_1₁(._2₂(H, Z))))
append2_2_in_ag₁(is_1₁(sum_1₁(._2₂(H, Z)))) -> if_append2_2_in_1_ag₂(H, append2_2_in_ag₁(is_1₁(sum_1₁(Z))))
if_append2_2_in_1_ag₂(H, append2_2_out_ag₁(parts_2₂(X, Y))) -> append2_2_out_ag₁(parts_2₂(._2₂(H, X), Y))
append2_2_in_ag₁(is_1₁(sum_1₁(Y))) -> append2_2_out_ag₁(parts_2₂([]_0, Y))
append1_2_in_ga₁(parts_2₂([]_0, Y)) -> append1_2_out_ga₁(is_1₁(sum_1₁(Y)))

Used ordering: POLO with Polynomial interpretation:

POL(if_append1_2_in_1_ga₂(x₁, x₂)) = 1 + x₂
POL(if_append2_2_in_1_ag₂(x₁, x₂)) = 1 + x₂
POL(is_1₁(x₁)) = x₁
POL(append2_2_out_ag₁(x₁)) = x₁
POL(IF_PERM_2_IN_1_GA₁(x₁)) = x₁
POL(parts_2₂(x₁, x₂)) = x₁ + x₂
POL(append1_2_in_ga₁(x₁)) = x₁
POL([]_0) = 0
POL(append1_2_out_ga₁(x₁)) = x₁
POL(._2₂(x₁, x₂)) = 1 + x₂
POL(sum_1₁(x₁)) = x₁
POL(IF_PERM_2_IN_2_GA₂(x₁, x₂)) = x₂
POL(append2_2_in_ag₁(x₁)) = x₁
POL(PERM_2_IN_GA₁(x₁)) = x₁

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ 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_2_in_ag₁(is_1₁(sum_1₁(L))))
IF_PERM_2_IN_2_GA₂(H, append1_2_out_ga₁(is_1₁(sum_1₁(W)))) -> PERM_2_IN_GA₁(W)

The TRS R consists of the following rules:

append2_2_in_ag₁(is_1₁(sum_1₁(Y))) -> append2_2_out_ag₁(parts_2₂([]_0, Y))
append2_2_in_ag₁(is_1₁(sum_1₁(._2₂(H, Z)))) -> if_append2_2_in_1_ag₂(H, append2_2_in_ag₁(is_1₁(sum_1₁(Z))))
append1_2_in_ga₁(parts_2₂([]_0, Y)) -> append1_2_out_ga₁(is_1₁(sum_1₁(Y)))
append1_2_in_ga₁(parts_2₂(._2₂(H, X), Y)) -> if_append1_2_in_1_ga₂(H, append1_2_in_ga₁(parts_2₂(X, Y)))
if_append2_2_in_1_ag₂(H, append2_2_out_ag₁(parts_2₂(X, Y))) -> append2_2_out_ag₁(parts_2₂(._2₂(H, X), Y))
if_append1_2_in_1_ga₂(H, append1_2_out_ga₁(is_1₁(sum_1₁(Z)))) -> append1_2_out_ga₁(is_1₁(sum_1₁(._2₂(H, Z))))

The set Q consists of the following terms:

append2_2_in_ag₁(x0)
append1_2_in_ga₁(x0)
if_append2_2_in_1_ag₂(x0, x1)
if_append1_2_in_1_ga₂(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.