Left Termination proof of /tmp/tmpTlDdZj/pl3.5.6.pl

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

p₁(X) :- l₁(X), q₁(X).
q₁(.₂(A, {}₀)).
r₁(1₀).
l₁({}₀).
l₁(.₂(H, T)) :- r₁(H), l₁(T).

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

p_1_in_a₁(X) -> if_p_1_in_1_a₂(X, l_1_in_a₁(X))
l_1_in_a₁([]_0) -> l_1_out_a₁([]_0)
l_1_in_a₁(._2₂(H, T)) -> if_l_1_in_1_a₃(H, T, r_1_in_a₁(H))
r_1_in_a₁(1_0) -> r_1_out_a₁(1_0)
if_l_1_in_1_a₃(H, T, r_1_out_a₁(H)) -> if_l_1_in_2_a₃(H, T, l_1_in_a₁(T))
if_l_1_in_2_a₃(H, T, l_1_out_a₁(T)) -> l_1_out_a₁(._2₂(H, T))
if_p_1_in_1_a₂(X, l_1_out_a₁(X)) -> if_p_1_in_2_a₂(X, q_1_in_g₁(X))
q_1_in_g₁(._2₂(A, []_0)) -> q_1_out_g₁(._2₂(A, []_0))
if_p_1_in_2_a₂(X, q_1_out_g₁(X)) -> p_1_out_a₁(X)

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:

p_1_in_a₁(X) -> if_p_1_in_1_a₂(X, l_1_in_a₁(X))
l_1_in_a₁([]_0) -> l_1_out_a₁([]_0)
l_1_in_a₁(._2₂(H, T)) -> if_l_1_in_1_a₃(H, T, r_1_in_a₁(H))
r_1_in_a₁(1_0) -> r_1_out_a₁(1_0)
if_l_1_in_1_a₃(H, T, r_1_out_a₁(H)) -> if_l_1_in_2_a₃(H, T, l_1_in_a₁(T))
if_l_1_in_2_a₃(H, T, l_1_out_a₁(T)) -> l_1_out_a₁(._2₂(H, T))
if_p_1_in_1_a₂(X, l_1_out_a₁(X)) -> if_p_1_in_2_a₂(X, q_1_in_g₁(X))
q_1_in_g₁(._2₂(A, []_0)) -> q_1_out_g₁(._2₂(A, []_0))
if_p_1_in_2_a₂(X, q_1_out_g₁(X)) -> p_1_out_a₁(X)

P_1_IN_A₁(X) -> IF_P_1_IN_1_A₂(X, l_1_in_a₁(X))
P_1_IN_A₁(X) -> L_1_IN_A₁(X)
L_1_IN_A₁(._2₂(H, T)) -> IF_L_1_IN_1_A₃(H, T, r_1_in_a₁(H))
L_1_IN_A₁(._2₂(H, T)) -> R_1_IN_A₁(H)
IF_L_1_IN_1_A₃(H, T, r_1_out_a₁(H)) -> IF_L_1_IN_2_A₃(H, T, l_1_in_a₁(T))
IF_L_1_IN_1_A₃(H, T, r_1_out_a₁(H)) -> L_1_IN_A₁(T)
IF_P_1_IN_1_A₂(X, l_1_out_a₁(X)) -> IF_P_1_IN_2_A₂(X, q_1_in_g₁(X))
IF_P_1_IN_1_A₂(X, l_1_out_a₁(X)) -> Q_1_IN_G₁(X)

The TRS R consists of the following rules:

p_1_in_a₁(X) -> if_p_1_in_1_a₂(X, l_1_in_a₁(X))
l_1_in_a₁([]_0) -> l_1_out_a₁([]_0)
l_1_in_a₁(._2₂(H, T)) -> if_l_1_in_1_a₃(H, T, r_1_in_a₁(H))
r_1_in_a₁(1_0) -> r_1_out_a₁(1_0)
if_l_1_in_1_a₃(H, T, r_1_out_a₁(H)) -> if_l_1_in_2_a₃(H, T, l_1_in_a₁(T))
if_l_1_in_2_a₃(H, T, l_1_out_a₁(T)) -> l_1_out_a₁(._2₂(H, T))
if_p_1_in_1_a₂(X, l_1_out_a₁(X)) -> if_p_1_in_2_a₂(X, q_1_in_g₁(X))
q_1_in_g₁(._2₂(A, []_0)) -> q_1_out_g₁(._2₂(A, []_0))
if_p_1_in_2_a₂(X, q_1_out_g₁(X)) -> p_1_out_a₁(X)

The argument filtering Pi contains the following mapping:
p_1_in_a₁(x1) = p_1_in_a
._2₂(x1, x2) = ._2₂(x1, x2)
[]_0 = []_0
1_0 = 1_0
if_p_1_in_1_a₂(x1, x2) = if_p_1_in_1_a₁(x2)
l_1_in_a₁(x1) = l_1_in_a
l_1_out_a₁(x1) = l_1_out_a₁(x1)
if_l_1_in_1_a₃(x1, x2, x3) = if_l_1_in_1_a₁(x3)
r_1_in_a₁(x1) = r_1_in_a
r_1_out_a₁(x1) = r_1_out_a₁(x1)
if_l_1_in_2_a₃(x1, x2, x3) = if_l_1_in_2_a₂(x1, x3)
if_p_1_in_2_a₂(x1, x2) = if_p_1_in_2_a₂(x1, x2)
q_1_in_g₁(x1) = q_1_in_g₁(x1)
q_1_out_g₁(x1) = q_1_out_g
p_1_out_a₁(x1) = p_1_out_a₁(x1)
L_1_IN_A₁(x1) = L_1_IN_A
Q_1_IN_G₁(x1) = Q_1_IN_G₁(x1)
P_1_IN_A₁(x1) = P_1_IN_A
IF_P_1_IN_2_A₂(x1, x2) = IF_P_1_IN_2_A₂(x1, x2)
IF_L_1_IN_2_A₃(x1, x2, x3) = IF_L_1_IN_2_A₂(x1, x3)
IF_P_1_IN_1_A₂(x1, x2) = IF_P_1_IN_1_A₁(x2)
IF_L_1_IN_1_A₃(x1, x2, x3) = IF_L_1_IN_1_A₁(x3)
R_1_IN_A₁(x1) = R_1_IN_A

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:

P_1_IN_A₁(X) -> IF_P_1_IN_1_A₂(X, l_1_in_a₁(X))
P_1_IN_A₁(X) -> L_1_IN_A₁(X)
L_1_IN_A₁(._2₂(H, T)) -> IF_L_1_IN_1_A₃(H, T, r_1_in_a₁(H))
L_1_IN_A₁(._2₂(H, T)) -> R_1_IN_A₁(H)
IF_L_1_IN_1_A₃(H, T, r_1_out_a₁(H)) -> IF_L_1_IN_2_A₃(H, T, l_1_in_a₁(T))
IF_L_1_IN_1_A₃(H, T, r_1_out_a₁(H)) -> L_1_IN_A₁(T)
IF_P_1_IN_1_A₂(X, l_1_out_a₁(X)) -> IF_P_1_IN_2_A₂(X, q_1_in_g₁(X))
IF_P_1_IN_1_A₂(X, l_1_out_a₁(X)) -> Q_1_IN_G₁(X)

The TRS R consists of the following rules:

p_1_in_a₁(X) -> if_p_1_in_1_a₂(X, l_1_in_a₁(X))
l_1_in_a₁([]_0) -> l_1_out_a₁([]_0)
l_1_in_a₁(._2₂(H, T)) -> if_l_1_in_1_a₃(H, T, r_1_in_a₁(H))
r_1_in_a₁(1_0) -> r_1_out_a₁(1_0)
if_l_1_in_1_a₃(H, T, r_1_out_a₁(H)) -> if_l_1_in_2_a₃(H, T, l_1_in_a₁(T))
if_l_1_in_2_a₃(H, T, l_1_out_a₁(T)) -> l_1_out_a₁(._2₂(H, T))
if_p_1_in_1_a₂(X, l_1_out_a₁(X)) -> if_p_1_in_2_a₂(X, q_1_in_g₁(X))
q_1_in_g₁(._2₂(A, []_0)) -> q_1_out_g₁(._2₂(A, []_0))
if_p_1_in_2_a₂(X, q_1_out_g₁(X)) -> p_1_out_a₁(X)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

  ↳ PrologToPiTRSProof

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

L_1_IN_A₁(._2₂(H, T)) -> IF_L_1_IN_1_A₃(H, T, r_1_in_a₁(H))
IF_L_1_IN_1_A₃(H, T, r_1_out_a₁(H)) -> L_1_IN_A₁(T)

The TRS R consists of the following rules:

p_1_in_a₁(X) -> if_p_1_in_1_a₂(X, l_1_in_a₁(X))
l_1_in_a₁([]_0) -> l_1_out_a₁([]_0)
l_1_in_a₁(._2₂(H, T)) -> if_l_1_in_1_a₃(H, T, r_1_in_a₁(H))
r_1_in_a₁(1_0) -> r_1_out_a₁(1_0)
if_l_1_in_1_a₃(H, T, r_1_out_a₁(H)) -> if_l_1_in_2_a₃(H, T, l_1_in_a₁(T))
if_l_1_in_2_a₃(H, T, l_1_out_a₁(T)) -> l_1_out_a₁(._2₂(H, T))
if_p_1_in_1_a₂(X, l_1_out_a₁(X)) -> if_p_1_in_2_a₂(X, q_1_in_g₁(X))
q_1_in_g₁(._2₂(A, []_0)) -> q_1_out_g₁(._2₂(A, []_0))
if_p_1_in_2_a₂(X, q_1_out_g₁(X)) -> p_1_out_a₁(X)

The argument filtering Pi contains the following mapping:
p_1_in_a₁(x1) = p_1_in_a
._2₂(x1, x2) = ._2₂(x1, x2)
[]_0 = []_0
1_0 = 1_0
if_p_1_in_1_a₂(x1, x2) = if_p_1_in_1_a₁(x2)
l_1_in_a₁(x1) = l_1_in_a
l_1_out_a₁(x1) = l_1_out_a₁(x1)
if_l_1_in_1_a₃(x1, x2, x3) = if_l_1_in_1_a₁(x3)
r_1_in_a₁(x1) = r_1_in_a
r_1_out_a₁(x1) = r_1_out_a₁(x1)
if_l_1_in_2_a₃(x1, x2, x3) = if_l_1_in_2_a₂(x1, x3)
if_p_1_in_2_a₂(x1, x2) = if_p_1_in_2_a₂(x1, x2)
q_1_in_g₁(x1) = q_1_in_g₁(x1)
q_1_out_g₁(x1) = q_1_out_g
p_1_out_a₁(x1) = p_1_out_a₁(x1)
L_1_IN_A₁(x1) = L_1_IN_A
IF_L_1_IN_1_A₃(x1, x2, x3) = IF_L_1_IN_1_A₁(x3)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

                ↳ PiDP

                  ↳ PiDPToQDPProof

  ↳ PrologToPiTRSProof

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

L_1_IN_A₁(._2₂(H, T)) -> IF_L_1_IN_1_A₃(H, T, r_1_in_a₁(H))
IF_L_1_IN_1_A₃(H, T, r_1_out_a₁(H)) -> L_1_IN_A₁(T)

The TRS R consists of the following rules:

r_1_in_a₁(1_0) -> r_1_out_a₁(1_0)

The argument filtering Pi contains the following mapping:
._2₂(x1, x2) = ._2₂(x1, x2)
1_0 = 1_0
r_1_in_a₁(x1) = r_1_in_a
r_1_out_a₁(x1) = r_1_out_a₁(x1)
L_1_IN_A₁(x1) = L_1_IN_A
IF_L_1_IN_1_A₃(x1, x2, x3) = IF_L_1_IN_1_A₁(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

            ↳ PiDP

              ↳ UsableRulesProof

                ↳ PiDP

                  ↳ PiDPToQDPProof

                    ↳ QDP

  ↳ PrologToPiTRSProof

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

L_1_IN_A -> IF_L_1_IN_1_A₁(r_1_in_a)
IF_L_1_IN_1_A₁(r_1_out_a₁(H)) -> L_1_IN_A

The TRS R consists of the following rules:

r_1_in_a -> r_1_out_a₁(1_0)

The set Q consists of the following terms:

r_1_in_a

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

p_1_in_a₁(X) -> if_p_1_in_1_a₂(X, l_1_in_a₁(X))
l_1_in_a₁([]_0) -> l_1_out_a₁([]_0)
l_1_in_a₁(._2₂(H, T)) -> if_l_1_in_1_a₃(H, T, r_1_in_a₁(H))
r_1_in_a₁(1_0) -> r_1_out_a₁(1_0)
if_l_1_in_1_a₃(H, T, r_1_out_a₁(H)) -> if_l_1_in_2_a₃(H, T, l_1_in_a₁(T))
if_l_1_in_2_a₃(H, T, l_1_out_a₁(T)) -> l_1_out_a₁(._2₂(H, T))
if_p_1_in_1_a₂(X, l_1_out_a₁(X)) -> if_p_1_in_2_a₂(X, q_1_in_g₁(X))
q_1_in_g₁(._2₂(A, []_0)) -> q_1_out_g₁(._2₂(A, []_0))
if_p_1_in_2_a₂(X, q_1_out_g₁(X)) -> p_1_out_a₁(X)

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:

p_1_in_a₁(X) -> if_p_1_in_1_a₂(X, l_1_in_a₁(X))
l_1_in_a₁([]_0) -> l_1_out_a₁([]_0)
l_1_in_a₁(._2₂(H, T)) -> if_l_1_in_1_a₃(H, T, r_1_in_a₁(H))
r_1_in_a₁(1_0) -> r_1_out_a₁(1_0)
if_l_1_in_1_a₃(H, T, r_1_out_a₁(H)) -> if_l_1_in_2_a₃(H, T, l_1_in_a₁(T))
if_l_1_in_2_a₃(H, T, l_1_out_a₁(T)) -> l_1_out_a₁(._2₂(H, T))
if_p_1_in_1_a₂(X, l_1_out_a₁(X)) -> if_p_1_in_2_a₂(X, q_1_in_g₁(X))
q_1_in_g₁(._2₂(A, []_0)) -> q_1_out_g₁(._2₂(A, []_0))
if_p_1_in_2_a₂(X, q_1_out_g₁(X)) -> p_1_out_a₁(X)

P_1_IN_A₁(X) -> IF_P_1_IN_1_A₂(X, l_1_in_a₁(X))
P_1_IN_A₁(X) -> L_1_IN_A₁(X)
L_1_IN_A₁(._2₂(H, T)) -> IF_L_1_IN_1_A₃(H, T, r_1_in_a₁(H))
L_1_IN_A₁(._2₂(H, T)) -> R_1_IN_A₁(H)
IF_L_1_IN_1_A₃(H, T, r_1_out_a₁(H)) -> IF_L_1_IN_2_A₃(H, T, l_1_in_a₁(T))
IF_L_1_IN_1_A₃(H, T, r_1_out_a₁(H)) -> L_1_IN_A₁(T)
IF_P_1_IN_1_A₂(X, l_1_out_a₁(X)) -> IF_P_1_IN_2_A₂(X, q_1_in_g₁(X))
IF_P_1_IN_1_A₂(X, l_1_out_a₁(X)) -> Q_1_IN_G₁(X)

The TRS R consists of the following rules:

p_1_in_a₁(X) -> if_p_1_in_1_a₂(X, l_1_in_a₁(X))
l_1_in_a₁([]_0) -> l_1_out_a₁([]_0)
l_1_in_a₁(._2₂(H, T)) -> if_l_1_in_1_a₃(H, T, r_1_in_a₁(H))
r_1_in_a₁(1_0) -> r_1_out_a₁(1_0)
if_l_1_in_1_a₃(H, T, r_1_out_a₁(H)) -> if_l_1_in_2_a₃(H, T, l_1_in_a₁(T))
if_l_1_in_2_a₃(H, T, l_1_out_a₁(T)) -> l_1_out_a₁(._2₂(H, T))
if_p_1_in_1_a₂(X, l_1_out_a₁(X)) -> if_p_1_in_2_a₂(X, q_1_in_g₁(X))
q_1_in_g₁(._2₂(A, []_0)) -> q_1_out_g₁(._2₂(A, []_0))
if_p_1_in_2_a₂(X, q_1_out_g₁(X)) -> p_1_out_a₁(X)

The argument filtering Pi contains the following mapping:
p_1_in_a₁(x1) = p_1_in_a
._2₂(x1, x2) = ._2₂(x1, x2)
[]_0 = []_0
1_0 = 1_0
if_p_1_in_1_a₂(x1, x2) = if_p_1_in_1_a₁(x2)
l_1_in_a₁(x1) = l_1_in_a
l_1_out_a₁(x1) = l_1_out_a₁(x1)
if_l_1_in_1_a₃(x1, x2, x3) = if_l_1_in_1_a₁(x3)
r_1_in_a₁(x1) = r_1_in_a
r_1_out_a₁(x1) = r_1_out_a₁(x1)
if_l_1_in_2_a₃(x1, x2, x3) = if_l_1_in_2_a₂(x1, x3)
if_p_1_in_2_a₂(x1, x2) = if_p_1_in_2_a₂(x1, x2)
q_1_in_g₁(x1) = q_1_in_g₁(x1)
q_1_out_g₁(x1) = q_1_out_g₁(x1)
p_1_out_a₁(x1) = p_1_out_a₁(x1)
L_1_IN_A₁(x1) = L_1_IN_A
Q_1_IN_G₁(x1) = Q_1_IN_G₁(x1)
P_1_IN_A₁(x1) = P_1_IN_A
IF_P_1_IN_2_A₂(x1, x2) = IF_P_1_IN_2_A₂(x1, x2)
IF_L_1_IN_2_A₃(x1, x2, x3) = IF_L_1_IN_2_A₂(x1, x3)
IF_P_1_IN_1_A₂(x1, x2) = IF_P_1_IN_1_A₁(x2)
IF_L_1_IN_1_A₃(x1, x2, x3) = IF_L_1_IN_1_A₁(x3)
R_1_IN_A₁(x1) = R_1_IN_A

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:

P_1_IN_A₁(X) -> IF_P_1_IN_1_A₂(X, l_1_in_a₁(X))
P_1_IN_A₁(X) -> L_1_IN_A₁(X)
L_1_IN_A₁(._2₂(H, T)) -> IF_L_1_IN_1_A₃(H, T, r_1_in_a₁(H))
L_1_IN_A₁(._2₂(H, T)) -> R_1_IN_A₁(H)
IF_L_1_IN_1_A₃(H, T, r_1_out_a₁(H)) -> IF_L_1_IN_2_A₃(H, T, l_1_in_a₁(T))
IF_L_1_IN_1_A₃(H, T, r_1_out_a₁(H)) -> L_1_IN_A₁(T)
IF_P_1_IN_1_A₂(X, l_1_out_a₁(X)) -> IF_P_1_IN_2_A₂(X, q_1_in_g₁(X))
IF_P_1_IN_1_A₂(X, l_1_out_a₁(X)) -> Q_1_IN_G₁(X)

The TRS R consists of the following rules:

p_1_in_a₁(X) -> if_p_1_in_1_a₂(X, l_1_in_a₁(X))
l_1_in_a₁([]_0) -> l_1_out_a₁([]_0)
l_1_in_a₁(._2₂(H, T)) -> if_l_1_in_1_a₃(H, T, r_1_in_a₁(H))
r_1_in_a₁(1_0) -> r_1_out_a₁(1_0)
if_l_1_in_1_a₃(H, T, r_1_out_a₁(H)) -> if_l_1_in_2_a₃(H, T, l_1_in_a₁(T))
if_l_1_in_2_a₃(H, T, l_1_out_a₁(T)) -> l_1_out_a₁(._2₂(H, T))
if_p_1_in_1_a₂(X, l_1_out_a₁(X)) -> if_p_1_in_2_a₂(X, q_1_in_g₁(X))
q_1_in_g₁(._2₂(A, []_0)) -> q_1_out_g₁(._2₂(A, []_0))
if_p_1_in_2_a₂(X, q_1_out_g₁(X)) -> p_1_out_a₁(X)

The argument filtering Pi contains the following mapping:
p_1_in_a₁(x1) = p_1_in_a
._2₂(x1, x2) = ._2₂(x1, x2)
[]_0 = []_0
1_0 = 1_0
if_p_1_in_1_a₂(x1, x2) = if_p_1_in_1_a₁(x2)
l_1_in_a₁(x1) = l_1_in_a
l_1_out_a₁(x1) = l_1_out_a₁(x1)
if_l_1_in_1_a₃(x1, x2, x3) = if_l_1_in_1_a₁(x3)
r_1_in_a₁(x1) = r_1_in_a
r_1_out_a₁(x1) = r_1_out_a₁(x1)
if_l_1_in_2_a₃(x1, x2, x3) = if_l_1_in_2_a₂(x1, x3)
if_p_1_in_2_a₂(x1, x2) = if_p_1_in_2_a₂(x1, x2)
q_1_in_g₁(x1) = q_1_in_g₁(x1)
q_1_out_g₁(x1) = q_1_out_g₁(x1)
p_1_out_a₁(x1) = p_1_out_a₁(x1)
L_1_IN_A₁(x1) = L_1_IN_A
Q_1_IN_G₁(x1) = Q_1_IN_G₁(x1)
P_1_IN_A₁(x1) = P_1_IN_A
IF_P_1_IN_2_A₂(x1, x2) = IF_P_1_IN_2_A₂(x1, x2)
IF_L_1_IN_2_A₃(x1, x2, x3) = IF_L_1_IN_2_A₂(x1, x3)
IF_P_1_IN_1_A₂(x1, x2) = IF_P_1_IN_1_A₁(x2)
IF_L_1_IN_1_A₃(x1, x2, x3) = IF_L_1_IN_1_A₁(x3)
R_1_IN_A₁(x1) = R_1_IN_A

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

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

L_1_IN_A₁(._2₂(H, T)) -> IF_L_1_IN_1_A₃(H, T, r_1_in_a₁(H))
IF_L_1_IN_1_A₃(H, T, r_1_out_a₁(H)) -> L_1_IN_A₁(T)

The TRS R consists of the following rules:

p_1_in_a₁(X) -> if_p_1_in_1_a₂(X, l_1_in_a₁(X))
l_1_in_a₁([]_0) -> l_1_out_a₁([]_0)
l_1_in_a₁(._2₂(H, T)) -> if_l_1_in_1_a₃(H, T, r_1_in_a₁(H))
r_1_in_a₁(1_0) -> r_1_out_a₁(1_0)
if_l_1_in_1_a₃(H, T, r_1_out_a₁(H)) -> if_l_1_in_2_a₃(H, T, l_1_in_a₁(T))
if_l_1_in_2_a₃(H, T, l_1_out_a₁(T)) -> l_1_out_a₁(._2₂(H, T))
if_p_1_in_1_a₂(X, l_1_out_a₁(X)) -> if_p_1_in_2_a₂(X, q_1_in_g₁(X))
q_1_in_g₁(._2₂(A, []_0)) -> q_1_out_g₁(._2₂(A, []_0))
if_p_1_in_2_a₂(X, q_1_out_g₁(X)) -> p_1_out_a₁(X)

The argument filtering Pi contains the following mapping:
p_1_in_a₁(x1) = p_1_in_a
._2₂(x1, x2) = ._2₂(x1, x2)
[]_0 = []_0
1_0 = 1_0
if_p_1_in_1_a₂(x1, x2) = if_p_1_in_1_a₁(x2)
l_1_in_a₁(x1) = l_1_in_a
l_1_out_a₁(x1) = l_1_out_a₁(x1)
if_l_1_in_1_a₃(x1, x2, x3) = if_l_1_in_1_a₁(x3)
r_1_in_a₁(x1) = r_1_in_a
r_1_out_a₁(x1) = r_1_out_a₁(x1)
if_l_1_in_2_a₃(x1, x2, x3) = if_l_1_in_2_a₂(x1, x3)
if_p_1_in_2_a₂(x1, x2) = if_p_1_in_2_a₂(x1, x2)
q_1_in_g₁(x1) = q_1_in_g₁(x1)
q_1_out_g₁(x1) = q_1_out_g₁(x1)
p_1_out_a₁(x1) = p_1_out_a₁(x1)
L_1_IN_A₁(x1) = L_1_IN_A
IF_L_1_IN_1_A₃(x1, x2, x3) = IF_L_1_IN_1_A₁(x3)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

                ↳ PiDP

                  ↳ PiDPToQDPProof

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

L_1_IN_A₁(._2₂(H, T)) -> IF_L_1_IN_1_A₃(H, T, r_1_in_a₁(H))
IF_L_1_IN_1_A₃(H, T, r_1_out_a₁(H)) -> L_1_IN_A₁(T)

The TRS R consists of the following rules:

r_1_in_a₁(1_0) -> r_1_out_a₁(1_0)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

                ↳ PiDP

                  ↳ PiDPToQDPProof

                    ↳ QDP

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

L_1_IN_A -> IF_L_1_IN_1_A₁(r_1_in_a)
IF_L_1_IN_1_A₁(r_1_out_a₁(H)) -> L_1_IN_A

The TRS R consists of the following rules:

r_1_in_a -> r_1_out_a₁(1_0)

The set Q consists of the following terms:

r_1_in_a

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