Left Termination proof of /tmp/tmpkf1JOj/g.pl

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

g₁(W) :- eq₂(X, .₂(.₂(a₀, {}₀), .₂(.₂(R, {}₀), {}₀))), eq₂(Y, .₂(.₂(S, .₂(c₀, {}₀)), .₂({}₀, {}₀))), app_1₃(X, Y, Z), eq₂(Z, .₂(U, V)), app_2₃(U, U, W).
app_1₃({}₀, X, X).
app_1₃(.₂(X, Xs), Ys, .₂(X, Zs)) :- app_1₃(Xs, Ys, Zs).
app_2₃({}₀, X, X).
app_2₃(.₂(X, Xs), Ys, .₂(X, Zs)) :- app_2₃(Xs, Ys, Zs).
eq₂(X, X).

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

g_1_in_a₁(W) -> if_g_1_in_1_a₂(W, eq_2_in_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0))))
eq_2_in_ag₂(X, X) -> eq_2_out_ag₂(X, X)
if_g_1_in_1_a₂(W, eq_2_out_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0)))) -> if_g_1_in_2_a₃(W, X, eq_2_in_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0))))
if_g_1_in_2_a₃(W, X, eq_2_out_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0)))) -> if_g_1_in_3_a₄(W, X, Y, app_1_3_in_aga₃(X, Y, Z))
app_1_3_in_aga₃([]_0, X, X) -> app_1_3_out_aga₃([]_0, X, X)
app_1_3_in_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_app_1_3_in_1_aga₅(X, Xs, Ys, Zs, app_1_3_in_aga₃(Xs, Ys, Zs))
if_app_1_3_in_1_aga₅(X, Xs, Ys, Zs, app_1_3_out_aga₃(Xs, Ys, Zs)) -> app_1_3_out_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_g_1_in_3_a₄(W, X, Y, app_1_3_out_aga₃(X, Y, Z)) -> if_g_1_in_4_a₃(W, Z, eq_2_in_ga₂(Z, ._2₂(U, V)))
eq_2_in_ga₂(X, X) -> eq_2_out_ga₂(X, X)
if_g_1_in_4_a₃(W, Z, eq_2_out_ga₂(Z, ._2₂(U, V))) -> if_g_1_in_5_a₃(W, U, app_2_3_in_aaa₃(U, U, W))
app_2_3_in_aaa₃([]_0, X, X) -> app_2_3_out_aaa₃([]_0, X, X)
app_2_3_in_aaa₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_app_2_3_in_1_aaa₅(X, Xs, Ys, Zs, app_2_3_in_aaa₃(Xs, Ys, Zs))
if_app_2_3_in_1_aaa₅(X, Xs, Ys, Zs, app_2_3_out_aaa₃(Xs, Ys, Zs)) -> app_2_3_out_aaa₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_g_1_in_5_a₃(W, U, app_2_3_out_aaa₃(U, U, W)) -> g_1_out_a₁(W)

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:

g_1_in_a₁(W) -> if_g_1_in_1_a₂(W, eq_2_in_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0))))
eq_2_in_ag₂(X, X) -> eq_2_out_ag₂(X, X)
if_g_1_in_1_a₂(W, eq_2_out_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0)))) -> if_g_1_in_2_a₃(W, X, eq_2_in_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0))))
if_g_1_in_2_a₃(W, X, eq_2_out_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0)))) -> if_g_1_in_3_a₄(W, X, Y, app_1_3_in_aga₃(X, Y, Z))
app_1_3_in_aga₃([]_0, X, X) -> app_1_3_out_aga₃([]_0, X, X)
app_1_3_in_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_app_1_3_in_1_aga₅(X, Xs, Ys, Zs, app_1_3_in_aga₃(Xs, Ys, Zs))
if_app_1_3_in_1_aga₅(X, Xs, Ys, Zs, app_1_3_out_aga₃(Xs, Ys, Zs)) -> app_1_3_out_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_g_1_in_3_a₄(W, X, Y, app_1_3_out_aga₃(X, Y, Z)) -> if_g_1_in_4_a₃(W, Z, eq_2_in_ga₂(Z, ._2₂(U, V)))
eq_2_in_ga₂(X, X) -> eq_2_out_ga₂(X, X)
if_g_1_in_4_a₃(W, Z, eq_2_out_ga₂(Z, ._2₂(U, V))) -> if_g_1_in_5_a₃(W, U, app_2_3_in_aaa₃(U, U, W))
app_2_3_in_aaa₃([]_0, X, X) -> app_2_3_out_aaa₃([]_0, X, X)
app_2_3_in_aaa₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_app_2_3_in_1_aaa₅(X, Xs, Ys, Zs, app_2_3_in_aaa₃(Xs, Ys, Zs))
if_app_2_3_in_1_aaa₅(X, Xs, Ys, Zs, app_2_3_out_aaa₃(Xs, Ys, Zs)) -> app_2_3_out_aaa₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_g_1_in_5_a₃(W, U, app_2_3_out_aaa₃(U, U, W)) -> g_1_out_a₁(W)

G_1_IN_A₁(W) -> IF_G_1_IN_1_A₂(W, eq_2_in_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0))))
G_1_IN_A₁(W) -> EQ_2_IN_AG₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0)))
IF_G_1_IN_1_A₂(W, eq_2_out_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0)))) -> IF_G_1_IN_2_A₃(W, X, eq_2_in_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0))))
IF_G_1_IN_1_A₂(W, eq_2_out_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0)))) -> EQ_2_IN_AG₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0)))
IF_G_1_IN_2_A₃(W, X, eq_2_out_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0)))) -> IF_G_1_IN_3_A₄(W, X, Y, app_1_3_in_aga₃(X, Y, Z))
IF_G_1_IN_2_A₃(W, X, eq_2_out_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0)))) -> APP_1_3_IN_AGA₃(X, Y, Z)
APP_1_3_IN_AGA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> IF_APP_1_3_IN_1_AGA₅(X, Xs, Ys, Zs, app_1_3_in_aga₃(Xs, Ys, Zs))
APP_1_3_IN_AGA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> APP_1_3_IN_AGA₃(Xs, Ys, Zs)
IF_G_1_IN_3_A₄(W, X, Y, app_1_3_out_aga₃(X, Y, Z)) -> IF_G_1_IN_4_A₃(W, Z, eq_2_in_ga₂(Z, ._2₂(U, V)))
IF_G_1_IN_3_A₄(W, X, Y, app_1_3_out_aga₃(X, Y, Z)) -> EQ_2_IN_GA₂(Z, ._2₂(U, V))
IF_G_1_IN_4_A₃(W, Z, eq_2_out_ga₂(Z, ._2₂(U, V))) -> IF_G_1_IN_5_A₃(W, U, app_2_3_in_aaa₃(U, U, W))
IF_G_1_IN_4_A₃(W, Z, eq_2_out_ga₂(Z, ._2₂(U, V))) -> APP_2_3_IN_AAA₃(U, U, W)
APP_2_3_IN_AAA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> IF_APP_2_3_IN_1_AAA₅(X, Xs, Ys, Zs, app_2_3_in_aaa₃(Xs, Ys, Zs))
APP_2_3_IN_AAA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> APP_2_3_IN_AAA₃(Xs, Ys, Zs)

The TRS R consists of the following rules:

g_1_in_a₁(W) -> if_g_1_in_1_a₂(W, eq_2_in_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0))))
eq_2_in_ag₂(X, X) -> eq_2_out_ag₂(X, X)
if_g_1_in_1_a₂(W, eq_2_out_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0)))) -> if_g_1_in_2_a₃(W, X, eq_2_in_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0))))
if_g_1_in_2_a₃(W, X, eq_2_out_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0)))) -> if_g_1_in_3_a₄(W, X, Y, app_1_3_in_aga₃(X, Y, Z))
app_1_3_in_aga₃([]_0, X, X) -> app_1_3_out_aga₃([]_0, X, X)
app_1_3_in_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_app_1_3_in_1_aga₅(X, Xs, Ys, Zs, app_1_3_in_aga₃(Xs, Ys, Zs))
if_app_1_3_in_1_aga₅(X, Xs, Ys, Zs, app_1_3_out_aga₃(Xs, Ys, Zs)) -> app_1_3_out_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_g_1_in_3_a₄(W, X, Y, app_1_3_out_aga₃(X, Y, Z)) -> if_g_1_in_4_a₃(W, Z, eq_2_in_ga₂(Z, ._2₂(U, V)))
eq_2_in_ga₂(X, X) -> eq_2_out_ga₂(X, X)
if_g_1_in_4_a₃(W, Z, eq_2_out_ga₂(Z, ._2₂(U, V))) -> if_g_1_in_5_a₃(W, U, app_2_3_in_aaa₃(U, U, W))
app_2_3_in_aaa₃([]_0, X, X) -> app_2_3_out_aaa₃([]_0, X, X)
app_2_3_in_aaa₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_app_2_3_in_1_aaa₅(X, Xs, Ys, Zs, app_2_3_in_aaa₃(Xs, Ys, Zs))
if_app_2_3_in_1_aaa₅(X, Xs, Ys, Zs, app_2_3_out_aaa₃(Xs, Ys, Zs)) -> app_2_3_out_aaa₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_g_1_in_5_a₃(W, U, app_2_3_out_aaa₃(U, U, W)) -> g_1_out_a₁(W)

The argument filtering Pi contains the following mapping:
g_1_in_a₁(x1) = g_1_in_a
._2₂(x1, x2) = ._2₁(x2)
a_0 = a_0
[]_0 = []_0
c_0 = c_0
if_g_1_in_1_a₂(x1, x2) = if_g_1_in_1_a₁(x2)
if_g_1_in_2_a₃(x1, x2, x3) = if_g_1_in_2_a₁(x3)
if_g_1_in_3_a₄(x1, x2, x3, x4) = if_g_1_in_3_a₁(x4)
eq_2_in_ag₂(x1, x2) = eq_2_in_ag₁(x2)
eq_2_out_ag₂(x1, x2) = eq_2_out_ag₁(x1)
app_1_3_in_aga₃(x1, x2, x3) = app_1_3_in_aga₁(x2)
app_1_3_out_aga₃(x1, x2, x3) = app_1_3_out_aga₂(x1, x3)
if_app_1_3_in_1_aga₅(x1, x2, x3, x4, x5) = if_app_1_3_in_1_aga₁(x5)
if_g_1_in_4_a₃(x1, x2, x3) = if_g_1_in_4_a₁(x3)
eq_2_in_ga₂(x1, x2) = eq_2_in_ga₁(x1)
eq_2_out_ga₂(x1, x2) = eq_2_out_ga₁(x2)
if_g_1_in_5_a₃(x1, x2, x3) = if_g_1_in_5_a₁(x3)
app_2_3_in_aaa₃(x1, x2, x3) = app_2_3_in_aaa
app_2_3_out_aaa₃(x1, x2, x3) = app_2_3_out_aaa₁(x1)
if_app_2_3_in_1_aaa₅(x1, x2, x3, x4, x5) = if_app_2_3_in_1_aaa₁(x5)
g_1_out_a₁(x1) = g_1_out_a
IF_G_1_IN_1_A₂(x1, x2) = IF_G_1_IN_1_A₁(x2)
IF_G_1_IN_4_A₃(x1, x2, x3) = IF_G_1_IN_4_A₁(x3)
G_1_IN_A₁(x1) = G_1_IN_A
EQ_2_IN_AG₂(x1, x2) = EQ_2_IN_AG₁(x2)
APP_2_3_IN_AAA₃(x1, x2, x3) = APP_2_3_IN_AAA
IF_APP_1_3_IN_1_AGA₅(x1, x2, x3, x4, x5) = IF_APP_1_3_IN_1_AGA₁(x5)
IF_G_1_IN_3_A₄(x1, x2, x3, x4) = IF_G_1_IN_3_A₁(x4)
IF_G_1_IN_2_A₃(x1, x2, x3) = IF_G_1_IN_2_A₁(x3)
IF_G_1_IN_5_A₃(x1, x2, x3) = IF_G_1_IN_5_A₁(x3)
IF_APP_2_3_IN_1_AAA₅(x1, x2, x3, x4, x5) = IF_APP_2_3_IN_1_AAA₁(x5)
APP_1_3_IN_AGA₃(x1, x2, x3) = APP_1_3_IN_AGA₁(x2)
EQ_2_IN_GA₂(x1, x2) = EQ_2_IN_GA₁(x1)

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:

G_1_IN_A₁(W) -> IF_G_1_IN_1_A₂(W, eq_2_in_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0))))
G_1_IN_A₁(W) -> EQ_2_IN_AG₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0)))
IF_G_1_IN_1_A₂(W, eq_2_out_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0)))) -> IF_G_1_IN_2_A₃(W, X, eq_2_in_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0))))
IF_G_1_IN_1_A₂(W, eq_2_out_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0)))) -> EQ_2_IN_AG₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0)))
IF_G_1_IN_2_A₃(W, X, eq_2_out_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0)))) -> IF_G_1_IN_3_A₄(W, X, Y, app_1_3_in_aga₃(X, Y, Z))
IF_G_1_IN_2_A₃(W, X, eq_2_out_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0)))) -> APP_1_3_IN_AGA₃(X, Y, Z)
APP_1_3_IN_AGA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> IF_APP_1_3_IN_1_AGA₅(X, Xs, Ys, Zs, app_1_3_in_aga₃(Xs, Ys, Zs))
APP_1_3_IN_AGA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> APP_1_3_IN_AGA₃(Xs, Ys, Zs)
IF_G_1_IN_3_A₄(W, X, Y, app_1_3_out_aga₃(X, Y, Z)) -> IF_G_1_IN_4_A₃(W, Z, eq_2_in_ga₂(Z, ._2₂(U, V)))
IF_G_1_IN_3_A₄(W, X, Y, app_1_3_out_aga₃(X, Y, Z)) -> EQ_2_IN_GA₂(Z, ._2₂(U, V))
IF_G_1_IN_4_A₃(W, Z, eq_2_out_ga₂(Z, ._2₂(U, V))) -> IF_G_1_IN_5_A₃(W, U, app_2_3_in_aaa₃(U, U, W))
IF_G_1_IN_4_A₃(W, Z, eq_2_out_ga₂(Z, ._2₂(U, V))) -> APP_2_3_IN_AAA₃(U, U, W)
APP_2_3_IN_AAA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> IF_APP_2_3_IN_1_AAA₅(X, Xs, Ys, Zs, app_2_3_in_aaa₃(Xs, Ys, Zs))
APP_2_3_IN_AAA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> APP_2_3_IN_AAA₃(Xs, Ys, Zs)

The TRS R consists of the following rules:

g_1_in_a₁(W) -> if_g_1_in_1_a₂(W, eq_2_in_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0))))
eq_2_in_ag₂(X, X) -> eq_2_out_ag₂(X, X)
if_g_1_in_1_a₂(W, eq_2_out_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0)))) -> if_g_1_in_2_a₃(W, X, eq_2_in_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0))))
if_g_1_in_2_a₃(W, X, eq_2_out_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0)))) -> if_g_1_in_3_a₄(W, X, Y, app_1_3_in_aga₃(X, Y, Z))
app_1_3_in_aga₃([]_0, X, X) -> app_1_3_out_aga₃([]_0, X, X)
app_1_3_in_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_app_1_3_in_1_aga₅(X, Xs, Ys, Zs, app_1_3_in_aga₃(Xs, Ys, Zs))
if_app_1_3_in_1_aga₅(X, Xs, Ys, Zs, app_1_3_out_aga₃(Xs, Ys, Zs)) -> app_1_3_out_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_g_1_in_3_a₄(W, X, Y, app_1_3_out_aga₃(X, Y, Z)) -> if_g_1_in_4_a₃(W, Z, eq_2_in_ga₂(Z, ._2₂(U, V)))
eq_2_in_ga₂(X, X) -> eq_2_out_ga₂(X, X)
if_g_1_in_4_a₃(W, Z, eq_2_out_ga₂(Z, ._2₂(U, V))) -> if_g_1_in_5_a₃(W, U, app_2_3_in_aaa₃(U, U, W))
app_2_3_in_aaa₃([]_0, X, X) -> app_2_3_out_aaa₃([]_0, X, X)
app_2_3_in_aaa₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_app_2_3_in_1_aaa₅(X, Xs, Ys, Zs, app_2_3_in_aaa₃(Xs, Ys, Zs))
if_app_2_3_in_1_aaa₅(X, Xs, Ys, Zs, app_2_3_out_aaa₃(Xs, Ys, Zs)) -> app_2_3_out_aaa₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_g_1_in_5_a₃(W, U, app_2_3_out_aaa₃(U, U, W)) -> g_1_out_a₁(W)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

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

The TRS R consists of the following rules:

g_1_in_a₁(W) -> if_g_1_in_1_a₂(W, eq_2_in_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0))))
eq_2_in_ag₂(X, X) -> eq_2_out_ag₂(X, X)
if_g_1_in_1_a₂(W, eq_2_out_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0)))) -> if_g_1_in_2_a₃(W, X, eq_2_in_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0))))
if_g_1_in_2_a₃(W, X, eq_2_out_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0)))) -> if_g_1_in_3_a₄(W, X, Y, app_1_3_in_aga₃(X, Y, Z))
app_1_3_in_aga₃([]_0, X, X) -> app_1_3_out_aga₃([]_0, X, X)
app_1_3_in_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_app_1_3_in_1_aga₅(X, Xs, Ys, Zs, app_1_3_in_aga₃(Xs, Ys, Zs))
if_app_1_3_in_1_aga₅(X, Xs, Ys, Zs, app_1_3_out_aga₃(Xs, Ys, Zs)) -> app_1_3_out_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_g_1_in_3_a₄(W, X, Y, app_1_3_out_aga₃(X, Y, Z)) -> if_g_1_in_4_a₃(W, Z, eq_2_in_ga₂(Z, ._2₂(U, V)))
eq_2_in_ga₂(X, X) -> eq_2_out_ga₂(X, X)
if_g_1_in_4_a₃(W, Z, eq_2_out_ga₂(Z, ._2₂(U, V))) -> if_g_1_in_5_a₃(W, U, app_2_3_in_aaa₃(U, U, W))
app_2_3_in_aaa₃([]_0, X, X) -> app_2_3_out_aaa₃([]_0, X, X)
app_2_3_in_aaa₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_app_2_3_in_1_aaa₅(X, Xs, Ys, Zs, app_2_3_in_aaa₃(Xs, Ys, Zs))
if_app_2_3_in_1_aaa₅(X, Xs, Ys, Zs, app_2_3_out_aaa₃(Xs, Ys, Zs)) -> app_2_3_out_aaa₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_g_1_in_5_a₃(W, U, app_2_3_out_aaa₃(U, U, W)) -> g_1_out_a₁(W)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

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

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

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

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

APP_2_3_IN_AAA -> APP_2_3_IN_AAA

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

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

  ↳ PrologToPiTRSProof

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

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

The TRS R consists of the following rules:

g_1_in_a₁(W) -> if_g_1_in_1_a₂(W, eq_2_in_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0))))
eq_2_in_ag₂(X, X) -> eq_2_out_ag₂(X, X)
if_g_1_in_1_a₂(W, eq_2_out_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0)))) -> if_g_1_in_2_a₃(W, X, eq_2_in_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0))))
if_g_1_in_2_a₃(W, X, eq_2_out_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0)))) -> if_g_1_in_3_a₄(W, X, Y, app_1_3_in_aga₃(X, Y, Z))
app_1_3_in_aga₃([]_0, X, X) -> app_1_3_out_aga₃([]_0, X, X)
app_1_3_in_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_app_1_3_in_1_aga₅(X, Xs, Ys, Zs, app_1_3_in_aga₃(Xs, Ys, Zs))
if_app_1_3_in_1_aga₅(X, Xs, Ys, Zs, app_1_3_out_aga₃(Xs, Ys, Zs)) -> app_1_3_out_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_g_1_in_3_a₄(W, X, Y, app_1_3_out_aga₃(X, Y, Z)) -> if_g_1_in_4_a₃(W, Z, eq_2_in_ga₂(Z, ._2₂(U, V)))
eq_2_in_ga₂(X, X) -> eq_2_out_ga₂(X, X)
if_g_1_in_4_a₃(W, Z, eq_2_out_ga₂(Z, ._2₂(U, V))) -> if_g_1_in_5_a₃(W, U, app_2_3_in_aaa₃(U, U, W))
app_2_3_in_aaa₃([]_0, X, X) -> app_2_3_out_aaa₃([]_0, X, X)
app_2_3_in_aaa₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_app_2_3_in_1_aaa₅(X, Xs, Ys, Zs, app_2_3_in_aaa₃(Xs, Ys, Zs))
if_app_2_3_in_1_aaa₅(X, Xs, Ys, Zs, app_2_3_out_aaa₃(Xs, Ys, Zs)) -> app_2_3_out_aaa₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_g_1_in_5_a₃(W, U, app_2_3_out_aaa₃(U, U, W)) -> g_1_out_a₁(W)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

  ↳ PrologToPiTRSProof

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

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

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

APP_1_3_IN_AGA₁(Ys) -> APP_1_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 {APP_1_3_IN_AGA₁}.
With regard to the inferred argument filtering the predicates were used in the following modes:
g₁: (f)
app_1₃: (f,b,f)
app_2₃: (f,f,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

g_1_in_a₁(W) -> if_g_1_in_1_a₂(W, eq_2_in_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0))))
eq_2_in_ag₂(X, X) -> eq_2_out_ag₂(X, X)
if_g_1_in_1_a₂(W, eq_2_out_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0)))) -> if_g_1_in_2_a₃(W, X, eq_2_in_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0))))
if_g_1_in_2_a₃(W, X, eq_2_out_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0)))) -> if_g_1_in_3_a₄(W, X, Y, app_1_3_in_aga₃(X, Y, Z))
app_1_3_in_aga₃([]_0, X, X) -> app_1_3_out_aga₃([]_0, X, X)
app_1_3_in_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_app_1_3_in_1_aga₅(X, Xs, Ys, Zs, app_1_3_in_aga₃(Xs, Ys, Zs))
if_app_1_3_in_1_aga₅(X, Xs, Ys, Zs, app_1_3_out_aga₃(Xs, Ys, Zs)) -> app_1_3_out_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_g_1_in_3_a₄(W, X, Y, app_1_3_out_aga₃(X, Y, Z)) -> if_g_1_in_4_a₃(W, Z, eq_2_in_ga₂(Z, ._2₂(U, V)))
eq_2_in_ga₂(X, X) -> eq_2_out_ga₂(X, X)
if_g_1_in_4_a₃(W, Z, eq_2_out_ga₂(Z, ._2₂(U, V))) -> if_g_1_in_5_a₃(W, U, app_2_3_in_aaa₃(U, U, W))
app_2_3_in_aaa₃([]_0, X, X) -> app_2_3_out_aaa₃([]_0, X, X)
app_2_3_in_aaa₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_app_2_3_in_1_aaa₅(X, Xs, Ys, Zs, app_2_3_in_aaa₃(Xs, Ys, Zs))
if_app_2_3_in_1_aaa₅(X, Xs, Ys, Zs, app_2_3_out_aaa₃(Xs, Ys, Zs)) -> app_2_3_out_aaa₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_g_1_in_5_a₃(W, U, app_2_3_out_aaa₃(U, U, W)) -> g_1_out_a₁(W)

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:

g_1_in_a₁(W) -> if_g_1_in_1_a₂(W, eq_2_in_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0))))
eq_2_in_ag₂(X, X) -> eq_2_out_ag₂(X, X)
if_g_1_in_1_a₂(W, eq_2_out_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0)))) -> if_g_1_in_2_a₃(W, X, eq_2_in_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0))))
if_g_1_in_2_a₃(W, X, eq_2_out_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0)))) -> if_g_1_in_3_a₄(W, X, Y, app_1_3_in_aga₃(X, Y, Z))
app_1_3_in_aga₃([]_0, X, X) -> app_1_3_out_aga₃([]_0, X, X)
app_1_3_in_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_app_1_3_in_1_aga₅(X, Xs, Ys, Zs, app_1_3_in_aga₃(Xs, Ys, Zs))
if_app_1_3_in_1_aga₅(X, Xs, Ys, Zs, app_1_3_out_aga₃(Xs, Ys, Zs)) -> app_1_3_out_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_g_1_in_3_a₄(W, X, Y, app_1_3_out_aga₃(X, Y, Z)) -> if_g_1_in_4_a₃(W, Z, eq_2_in_ga₂(Z, ._2₂(U, V)))
eq_2_in_ga₂(X, X) -> eq_2_out_ga₂(X, X)
if_g_1_in_4_a₃(W, Z, eq_2_out_ga₂(Z, ._2₂(U, V))) -> if_g_1_in_5_a₃(W, U, app_2_3_in_aaa₃(U, U, W))
app_2_3_in_aaa₃([]_0, X, X) -> app_2_3_out_aaa₃([]_0, X, X)
app_2_3_in_aaa₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_app_2_3_in_1_aaa₅(X, Xs, Ys, Zs, app_2_3_in_aaa₃(Xs, Ys, Zs))
if_app_2_3_in_1_aaa₅(X, Xs, Ys, Zs, app_2_3_out_aaa₃(Xs, Ys, Zs)) -> app_2_3_out_aaa₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_g_1_in_5_a₃(W, U, app_2_3_out_aaa₃(U, U, W)) -> g_1_out_a₁(W)

G_1_IN_A₁(W) -> IF_G_1_IN_1_A₂(W, eq_2_in_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0))))
G_1_IN_A₁(W) -> EQ_2_IN_AG₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0)))
IF_G_1_IN_1_A₂(W, eq_2_out_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0)))) -> IF_G_1_IN_2_A₃(W, X, eq_2_in_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0))))
IF_G_1_IN_1_A₂(W, eq_2_out_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0)))) -> EQ_2_IN_AG₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0)))
IF_G_1_IN_2_A₃(W, X, eq_2_out_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0)))) -> IF_G_1_IN_3_A₄(W, X, Y, app_1_3_in_aga₃(X, Y, Z))
IF_G_1_IN_2_A₃(W, X, eq_2_out_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0)))) -> APP_1_3_IN_AGA₃(X, Y, Z)
APP_1_3_IN_AGA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> IF_APP_1_3_IN_1_AGA₅(X, Xs, Ys, Zs, app_1_3_in_aga₃(Xs, Ys, Zs))
APP_1_3_IN_AGA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> APP_1_3_IN_AGA₃(Xs, Ys, Zs)
IF_G_1_IN_3_A₄(W, X, Y, app_1_3_out_aga₃(X, Y, Z)) -> IF_G_1_IN_4_A₃(W, Z, eq_2_in_ga₂(Z, ._2₂(U, V)))
IF_G_1_IN_3_A₄(W, X, Y, app_1_3_out_aga₃(X, Y, Z)) -> EQ_2_IN_GA₂(Z, ._2₂(U, V))
IF_G_1_IN_4_A₃(W, Z, eq_2_out_ga₂(Z, ._2₂(U, V))) -> IF_G_1_IN_5_A₃(W, U, app_2_3_in_aaa₃(U, U, W))
IF_G_1_IN_4_A₃(W, Z, eq_2_out_ga₂(Z, ._2₂(U, V))) -> APP_2_3_IN_AAA₃(U, U, W)
APP_2_3_IN_AAA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> IF_APP_2_3_IN_1_AAA₅(X, Xs, Ys, Zs, app_2_3_in_aaa₃(Xs, Ys, Zs))
APP_2_3_IN_AAA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> APP_2_3_IN_AAA₃(Xs, Ys, Zs)

The TRS R consists of the following rules:

g_1_in_a₁(W) -> if_g_1_in_1_a₂(W, eq_2_in_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0))))
eq_2_in_ag₂(X, X) -> eq_2_out_ag₂(X, X)
if_g_1_in_1_a₂(W, eq_2_out_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0)))) -> if_g_1_in_2_a₃(W, X, eq_2_in_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0))))
if_g_1_in_2_a₃(W, X, eq_2_out_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0)))) -> if_g_1_in_3_a₄(W, X, Y, app_1_3_in_aga₃(X, Y, Z))
app_1_3_in_aga₃([]_0, X, X) -> app_1_3_out_aga₃([]_0, X, X)
app_1_3_in_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_app_1_3_in_1_aga₅(X, Xs, Ys, Zs, app_1_3_in_aga₃(Xs, Ys, Zs))
if_app_1_3_in_1_aga₅(X, Xs, Ys, Zs, app_1_3_out_aga₃(Xs, Ys, Zs)) -> app_1_3_out_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_g_1_in_3_a₄(W, X, Y, app_1_3_out_aga₃(X, Y, Z)) -> if_g_1_in_4_a₃(W, Z, eq_2_in_ga₂(Z, ._2₂(U, V)))
eq_2_in_ga₂(X, X) -> eq_2_out_ga₂(X, X)
if_g_1_in_4_a₃(W, Z, eq_2_out_ga₂(Z, ._2₂(U, V))) -> if_g_1_in_5_a₃(W, U, app_2_3_in_aaa₃(U, U, W))
app_2_3_in_aaa₃([]_0, X, X) -> app_2_3_out_aaa₃([]_0, X, X)
app_2_3_in_aaa₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_app_2_3_in_1_aaa₅(X, Xs, Ys, Zs, app_2_3_in_aaa₃(Xs, Ys, Zs))
if_app_2_3_in_1_aaa₅(X, Xs, Ys, Zs, app_2_3_out_aaa₃(Xs, Ys, Zs)) -> app_2_3_out_aaa₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_g_1_in_5_a₃(W, U, app_2_3_out_aaa₃(U, U, W)) -> g_1_out_a₁(W)

The argument filtering Pi contains the following mapping:
g_1_in_a₁(x1) = g_1_in_a
._2₂(x1, x2) = ._2₁(x2)
a_0 = a_0
[]_0 = []_0
c_0 = c_0
if_g_1_in_1_a₂(x1, x2) = if_g_1_in_1_a₁(x2)
if_g_1_in_2_a₃(x1, x2, x3) = if_g_1_in_2_a₁(x3)
if_g_1_in_3_a₄(x1, x2, x3, x4) = if_g_1_in_3_a₁(x4)
eq_2_in_ag₂(x1, x2) = eq_2_in_ag₁(x2)
eq_2_out_ag₂(x1, x2) = eq_2_out_ag₂(x1, x2)
app_1_3_in_aga₃(x1, x2, x3) = app_1_3_in_aga₁(x2)
app_1_3_out_aga₃(x1, x2, x3) = app_1_3_out_aga₃(x1, x2, x3)
if_app_1_3_in_1_aga₅(x1, x2, x3, x4, x5) = if_app_1_3_in_1_aga₂(x3, x5)
if_g_1_in_4_a₃(x1, x2, x3) = if_g_1_in_4_a₁(x3)
eq_2_in_ga₂(x1, x2) = eq_2_in_ga₁(x1)
eq_2_out_ga₂(x1, x2) = eq_2_out_ga₂(x1, x2)
if_g_1_in_5_a₃(x1, x2, x3) = if_g_1_in_5_a₁(x3)
app_2_3_in_aaa₃(x1, x2, x3) = app_2_3_in_aaa
app_2_3_out_aaa₃(x1, x2, x3) = app_2_3_out_aaa₁(x1)
if_app_2_3_in_1_aaa₅(x1, x2, x3, x4, x5) = if_app_2_3_in_1_aaa₁(x5)
g_1_out_a₁(x1) = g_1_out_a
IF_G_1_IN_1_A₂(x1, x2) = IF_G_1_IN_1_A₁(x2)
IF_G_1_IN_4_A₃(x1, x2, x3) = IF_G_1_IN_4_A₁(x3)
G_1_IN_A₁(x1) = G_1_IN_A
EQ_2_IN_AG₂(x1, x2) = EQ_2_IN_AG₁(x2)
APP_2_3_IN_AAA₃(x1, x2, x3) = APP_2_3_IN_AAA
IF_APP_1_3_IN_1_AGA₅(x1, x2, x3, x4, x5) = IF_APP_1_3_IN_1_AGA₂(x3, x5)
IF_G_1_IN_3_A₄(x1, x2, x3, x4) = IF_G_1_IN_3_A₁(x4)
IF_G_1_IN_2_A₃(x1, x2, x3) = IF_G_1_IN_2_A₁(x3)
IF_G_1_IN_5_A₃(x1, x2, x3) = IF_G_1_IN_5_A₁(x3)
IF_APP_2_3_IN_1_AAA₅(x1, x2, x3, x4, x5) = IF_APP_2_3_IN_1_AAA₁(x5)
APP_1_3_IN_AGA₃(x1, x2, x3) = APP_1_3_IN_AGA₁(x2)
EQ_2_IN_GA₂(x1, x2) = EQ_2_IN_GA₁(x1)

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:

G_1_IN_A₁(W) -> IF_G_1_IN_1_A₂(W, eq_2_in_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0))))
G_1_IN_A₁(W) -> EQ_2_IN_AG₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0)))
IF_G_1_IN_1_A₂(W, eq_2_out_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0)))) -> IF_G_1_IN_2_A₃(W, X, eq_2_in_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0))))
IF_G_1_IN_1_A₂(W, eq_2_out_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0)))) -> EQ_2_IN_AG₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0)))
IF_G_1_IN_2_A₃(W, X, eq_2_out_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0)))) -> IF_G_1_IN_3_A₄(W, X, Y, app_1_3_in_aga₃(X, Y, Z))
IF_G_1_IN_2_A₃(W, X, eq_2_out_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0)))) -> APP_1_3_IN_AGA₃(X, Y, Z)
APP_1_3_IN_AGA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> IF_APP_1_3_IN_1_AGA₅(X, Xs, Ys, Zs, app_1_3_in_aga₃(Xs, Ys, Zs))
APP_1_3_IN_AGA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> APP_1_3_IN_AGA₃(Xs, Ys, Zs)
IF_G_1_IN_3_A₄(W, X, Y, app_1_3_out_aga₃(X, Y, Z)) -> IF_G_1_IN_4_A₃(W, Z, eq_2_in_ga₂(Z, ._2₂(U, V)))
IF_G_1_IN_3_A₄(W, X, Y, app_1_3_out_aga₃(X, Y, Z)) -> EQ_2_IN_GA₂(Z, ._2₂(U, V))
IF_G_1_IN_4_A₃(W, Z, eq_2_out_ga₂(Z, ._2₂(U, V))) -> IF_G_1_IN_5_A₃(W, U, app_2_3_in_aaa₃(U, U, W))
IF_G_1_IN_4_A₃(W, Z, eq_2_out_ga₂(Z, ._2₂(U, V))) -> APP_2_3_IN_AAA₃(U, U, W)
APP_2_3_IN_AAA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> IF_APP_2_3_IN_1_AAA₅(X, Xs, Ys, Zs, app_2_3_in_aaa₃(Xs, Ys, Zs))
APP_2_3_IN_AAA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> APP_2_3_IN_AAA₃(Xs, Ys, Zs)

The TRS R consists of the following rules:

g_1_in_a₁(W) -> if_g_1_in_1_a₂(W, eq_2_in_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0))))
eq_2_in_ag₂(X, X) -> eq_2_out_ag₂(X, X)
if_g_1_in_1_a₂(W, eq_2_out_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0)))) -> if_g_1_in_2_a₃(W, X, eq_2_in_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0))))
if_g_1_in_2_a₃(W, X, eq_2_out_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0)))) -> if_g_1_in_3_a₄(W, X, Y, app_1_3_in_aga₃(X, Y, Z))
app_1_3_in_aga₃([]_0, X, X) -> app_1_3_out_aga₃([]_0, X, X)
app_1_3_in_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_app_1_3_in_1_aga₅(X, Xs, Ys, Zs, app_1_3_in_aga₃(Xs, Ys, Zs))
if_app_1_3_in_1_aga₅(X, Xs, Ys, Zs, app_1_3_out_aga₃(Xs, Ys, Zs)) -> app_1_3_out_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_g_1_in_3_a₄(W, X, Y, app_1_3_out_aga₃(X, Y, Z)) -> if_g_1_in_4_a₃(W, Z, eq_2_in_ga₂(Z, ._2₂(U, V)))
eq_2_in_ga₂(X, X) -> eq_2_out_ga₂(X, X)
if_g_1_in_4_a₃(W, Z, eq_2_out_ga₂(Z, ._2₂(U, V))) -> if_g_1_in_5_a₃(W, U, app_2_3_in_aaa₃(U, U, W))
app_2_3_in_aaa₃([]_0, X, X) -> app_2_3_out_aaa₃([]_0, X, X)
app_2_3_in_aaa₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_app_2_3_in_1_aaa₅(X, Xs, Ys, Zs, app_2_3_in_aaa₃(Xs, Ys, Zs))
if_app_2_3_in_1_aaa₅(X, Xs, Ys, Zs, app_2_3_out_aaa₃(Xs, Ys, Zs)) -> app_2_3_out_aaa₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_g_1_in_5_a₃(W, U, app_2_3_out_aaa₃(U, U, W)) -> g_1_out_a₁(W)

The argument filtering Pi contains the following mapping:
g_1_in_a₁(x1) = g_1_in_a
._2₂(x1, x2) = ._2₁(x2)
a_0 = a_0
[]_0 = []_0
c_0 = c_0
if_g_1_in_1_a₂(x1, x2) = if_g_1_in_1_a₁(x2)
if_g_1_in_2_a₃(x1, x2, x3) = if_g_1_in_2_a₁(x3)
if_g_1_in_3_a₄(x1, x2, x3, x4) = if_g_1_in_3_a₁(x4)
eq_2_in_ag₂(x1, x2) = eq_2_in_ag₁(x2)
eq_2_out_ag₂(x1, x2) = eq_2_out_ag₂(x1, x2)
app_1_3_in_aga₃(x1, x2, x3) = app_1_3_in_aga₁(x2)
app_1_3_out_aga₃(x1, x2, x3) = app_1_3_out_aga₃(x1, x2, x3)
if_app_1_3_in_1_aga₅(x1, x2, x3, x4, x5) = if_app_1_3_in_1_aga₂(x3, x5)
if_g_1_in_4_a₃(x1, x2, x3) = if_g_1_in_4_a₁(x3)
eq_2_in_ga₂(x1, x2) = eq_2_in_ga₁(x1)
eq_2_out_ga₂(x1, x2) = eq_2_out_ga₂(x1, x2)
if_g_1_in_5_a₃(x1, x2, x3) = if_g_1_in_5_a₁(x3)
app_2_3_in_aaa₃(x1, x2, x3) = app_2_3_in_aaa
app_2_3_out_aaa₃(x1, x2, x3) = app_2_3_out_aaa₁(x1)
if_app_2_3_in_1_aaa₅(x1, x2, x3, x4, x5) = if_app_2_3_in_1_aaa₁(x5)
g_1_out_a₁(x1) = g_1_out_a
IF_G_1_IN_1_A₂(x1, x2) = IF_G_1_IN_1_A₁(x2)
IF_G_1_IN_4_A₃(x1, x2, x3) = IF_G_1_IN_4_A₁(x3)
G_1_IN_A₁(x1) = G_1_IN_A
EQ_2_IN_AG₂(x1, x2) = EQ_2_IN_AG₁(x2)
APP_2_3_IN_AAA₃(x1, x2, x3) = APP_2_3_IN_AAA
IF_APP_1_3_IN_1_AGA₅(x1, x2, x3, x4, x5) = IF_APP_1_3_IN_1_AGA₂(x3, x5)
IF_G_1_IN_3_A₄(x1, x2, x3, x4) = IF_G_1_IN_3_A₁(x4)
IF_G_1_IN_2_A₃(x1, x2, x3) = IF_G_1_IN_2_A₁(x3)
IF_G_1_IN_5_A₃(x1, x2, x3) = IF_G_1_IN_5_A₁(x3)
IF_APP_2_3_IN_1_AAA₅(x1, x2, x3, x4, x5) = IF_APP_2_3_IN_1_AAA₁(x5)
APP_1_3_IN_AGA₃(x1, x2, x3) = APP_1_3_IN_AGA₁(x2)
EQ_2_IN_GA₂(x1, x2) = EQ_2_IN_GA₁(x1)

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

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

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

The TRS R consists of the following rules:

g_1_in_a₁(W) -> if_g_1_in_1_a₂(W, eq_2_in_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0))))
eq_2_in_ag₂(X, X) -> eq_2_out_ag₂(X, X)
if_g_1_in_1_a₂(W, eq_2_out_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0)))) -> if_g_1_in_2_a₃(W, X, eq_2_in_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0))))
if_g_1_in_2_a₃(W, X, eq_2_out_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0)))) -> if_g_1_in_3_a₄(W, X, Y, app_1_3_in_aga₃(X, Y, Z))
app_1_3_in_aga₃([]_0, X, X) -> app_1_3_out_aga₃([]_0, X, X)
app_1_3_in_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_app_1_3_in_1_aga₅(X, Xs, Ys, Zs, app_1_3_in_aga₃(Xs, Ys, Zs))
if_app_1_3_in_1_aga₅(X, Xs, Ys, Zs, app_1_3_out_aga₃(Xs, Ys, Zs)) -> app_1_3_out_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_g_1_in_3_a₄(W, X, Y, app_1_3_out_aga₃(X, Y, Z)) -> if_g_1_in_4_a₃(W, Z, eq_2_in_ga₂(Z, ._2₂(U, V)))
eq_2_in_ga₂(X, X) -> eq_2_out_ga₂(X, X)
if_g_1_in_4_a₃(W, Z, eq_2_out_ga₂(Z, ._2₂(U, V))) -> if_g_1_in_5_a₃(W, U, app_2_3_in_aaa₃(U, U, W))
app_2_3_in_aaa₃([]_0, X, X) -> app_2_3_out_aaa₃([]_0, X, X)
app_2_3_in_aaa₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_app_2_3_in_1_aaa₅(X, Xs, Ys, Zs, app_2_3_in_aaa₃(Xs, Ys, Zs))
if_app_2_3_in_1_aaa₅(X, Xs, Ys, Zs, app_2_3_out_aaa₃(Xs, Ys, Zs)) -> app_2_3_out_aaa₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_g_1_in_5_a₃(W, U, app_2_3_out_aaa₃(U, U, W)) -> g_1_out_a₁(W)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

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

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

              ↳ PiDP

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

APP_2_3_IN_AAA -> APP_2_3_IN_AAA

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

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

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

The TRS R consists of the following rules:

g_1_in_a₁(W) -> if_g_1_in_1_a₂(W, eq_2_in_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0))))
eq_2_in_ag₂(X, X) -> eq_2_out_ag₂(X, X)
if_g_1_in_1_a₂(W, eq_2_out_ag₂(X, ._2₂(._2₂(a_0, []_0), ._2₂(._2₂(R, []_0), []_0)))) -> if_g_1_in_2_a₃(W, X, eq_2_in_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0))))
if_g_1_in_2_a₃(W, X, eq_2_out_ag₂(Y, ._2₂(._2₂(S, ._2₂(c_0, []_0)), ._2₂([]_0, []_0)))) -> if_g_1_in_3_a₄(W, X, Y, app_1_3_in_aga₃(X, Y, Z))
app_1_3_in_aga₃([]_0, X, X) -> app_1_3_out_aga₃([]_0, X, X)
app_1_3_in_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_app_1_3_in_1_aga₅(X, Xs, Ys, Zs, app_1_3_in_aga₃(Xs, Ys, Zs))
if_app_1_3_in_1_aga₅(X, Xs, Ys, Zs, app_1_3_out_aga₃(Xs, Ys, Zs)) -> app_1_3_out_aga₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_g_1_in_3_a₄(W, X, Y, app_1_3_out_aga₃(X, Y, Z)) -> if_g_1_in_4_a₃(W, Z, eq_2_in_ga₂(Z, ._2₂(U, V)))
eq_2_in_ga₂(X, X) -> eq_2_out_ga₂(X, X)
if_g_1_in_4_a₃(W, Z, eq_2_out_ga₂(Z, ._2₂(U, V))) -> if_g_1_in_5_a₃(W, U, app_2_3_in_aaa₃(U, U, W))
app_2_3_in_aaa₃([]_0, X, X) -> app_2_3_out_aaa₃([]_0, X, X)
app_2_3_in_aaa₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> if_app_2_3_in_1_aaa₅(X, Xs, Ys, Zs, app_2_3_in_aaa₃(Xs, Ys, Zs))
if_app_2_3_in_1_aaa₅(X, Xs, Ys, Zs, app_2_3_out_aaa₃(Xs, Ys, Zs)) -> app_2_3_out_aaa₃(._2₂(X, Xs), Ys, ._2₂(X, Zs))
if_g_1_in_5_a₃(W, U, app_2_3_out_aaa₃(U, U, W)) -> g_1_out_a₁(W)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

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

APP_1_3_IN_AGA₃(._2₂(X, Xs), Ys, ._2₂(X, Zs)) -> APP_1_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:

APP_1_3_IN_AGA₁(Ys) -> APP_1_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 {APP_1_3_IN_AGA₁}.