Left Termination proof of /tmp/tmp0byZea/reverse-fb.pl

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

reverse₂(X1s, X2s) :- reverse₃(X1s, {}₀, X2s).
reverse₃({}₀, Xs, Xs).
reverse₃(.₂(X, X1s), X2s, Ys) :- reverse₃(X1s, .₂(X, X2s), Ys).

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

reverse_2_in_ag₂(X1s, X2s) -> if_reverse_2_in_1_ag₃(X1s, X2s, reverse_3_in_agg₃(X1s, []_0, X2s))
reverse_3_in_agg₃([]_0, Xs, Xs) -> reverse_3_out_agg₃([]_0, Xs, Xs)
reverse_3_in_agg₃(._2₂(X, X1s), X2s, Ys) -> if_reverse_3_in_1_agg₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
reverse_3_in_aag₃([]_0, Xs, Xs) -> reverse_3_out_aag₃([]_0, Xs, Xs)
reverse_3_in_aag₃(._2₂(X, X1s), X2s, Ys) -> if_reverse_3_in_1_aag₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
if_reverse_3_in_1_aag₅(X, X1s, X2s, Ys, reverse_3_out_aag₃(X1s, ._2₂(X, X2s), Ys)) -> reverse_3_out_aag₃(._2₂(X, X1s), X2s, Ys)
if_reverse_3_in_1_agg₅(X, X1s, X2s, Ys, reverse_3_out_aag₃(X1s, ._2₂(X, X2s), Ys)) -> reverse_3_out_agg₃(._2₂(X, X1s), X2s, Ys)
if_reverse_2_in_1_ag₃(X1s, X2s, reverse_3_out_agg₃(X1s, []_0, X2s)) -> reverse_2_out_ag₂(X1s, X2s)

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:

reverse_2_in_ag₂(X1s, X2s) -> if_reverse_2_in_1_ag₃(X1s, X2s, reverse_3_in_agg₃(X1s, []_0, X2s))
reverse_3_in_agg₃([]_0, Xs, Xs) -> reverse_3_out_agg₃([]_0, Xs, Xs)
reverse_3_in_agg₃(._2₂(X, X1s), X2s, Ys) -> if_reverse_3_in_1_agg₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
reverse_3_in_aag₃([]_0, Xs, Xs) -> reverse_3_out_aag₃([]_0, Xs, Xs)
reverse_3_in_aag₃(._2₂(X, X1s), X2s, Ys) -> if_reverse_3_in_1_aag₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
if_reverse_3_in_1_aag₅(X, X1s, X2s, Ys, reverse_3_out_aag₃(X1s, ._2₂(X, X2s), Ys)) -> reverse_3_out_aag₃(._2₂(X, X1s), X2s, Ys)
if_reverse_3_in_1_agg₅(X, X1s, X2s, Ys, reverse_3_out_aag₃(X1s, ._2₂(X, X2s), Ys)) -> reverse_3_out_agg₃(._2₂(X, X1s), X2s, Ys)
if_reverse_2_in_1_ag₃(X1s, X2s, reverse_3_out_agg₃(X1s, []_0, X2s)) -> reverse_2_out_ag₂(X1s, X2s)

REVERSE_2_IN_AG₂(X1s, X2s) -> IF_REVERSE_2_IN_1_AG₃(X1s, X2s, reverse_3_in_agg₃(X1s, []_0, X2s))
REVERSE_2_IN_AG₂(X1s, X2s) -> REVERSE_3_IN_AGG₃(X1s, []_0, X2s)
REVERSE_3_IN_AGG₃(._2₂(X, X1s), X2s, Ys) -> IF_REVERSE_3_IN_1_AGG₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
REVERSE_3_IN_AGG₃(._2₂(X, X1s), X2s, Ys) -> REVERSE_3_IN_AAG₃(X1s, ._2₂(X, X2s), Ys)
REVERSE_3_IN_AAG₃(._2₂(X, X1s), X2s, Ys) -> IF_REVERSE_3_IN_1_AAG₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
REVERSE_3_IN_AAG₃(._2₂(X, X1s), X2s, Ys) -> REVERSE_3_IN_AAG₃(X1s, ._2₂(X, X2s), Ys)

The TRS R consists of the following rules:

reverse_2_in_ag₂(X1s, X2s) -> if_reverse_2_in_1_ag₃(X1s, X2s, reverse_3_in_agg₃(X1s, []_0, X2s))
reverse_3_in_agg₃([]_0, Xs, Xs) -> reverse_3_out_agg₃([]_0, Xs, Xs)
reverse_3_in_agg₃(._2₂(X, X1s), X2s, Ys) -> if_reverse_3_in_1_agg₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
reverse_3_in_aag₃([]_0, Xs, Xs) -> reverse_3_out_aag₃([]_0, Xs, Xs)
reverse_3_in_aag₃(._2₂(X, X1s), X2s, Ys) -> if_reverse_3_in_1_aag₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
if_reverse_3_in_1_aag₅(X, X1s, X2s, Ys, reverse_3_out_aag₃(X1s, ._2₂(X, X2s), Ys)) -> reverse_3_out_aag₃(._2₂(X, X1s), X2s, Ys)
if_reverse_3_in_1_agg₅(X, X1s, X2s, Ys, reverse_3_out_aag₃(X1s, ._2₂(X, X2s), Ys)) -> reverse_3_out_agg₃(._2₂(X, X1s), X2s, Ys)
if_reverse_2_in_1_ag₃(X1s, X2s, reverse_3_out_agg₃(X1s, []_0, X2s)) -> reverse_2_out_ag₂(X1s, X2s)

The argument filtering Pi contains the following mapping:
reverse_2_in_ag₂(x1, x2) = reverse_2_in_ag₁(x2)
[]_0 = []_0
._2₂(x1, x2) = ._2₂(x1, x2)
if_reverse_2_in_1_ag₃(x1, x2, x3) = if_reverse_2_in_1_ag₁(x3)
reverse_3_in_agg₃(x1, x2, x3) = reverse_3_in_agg₂(x2, x3)
reverse_3_out_agg₃(x1, x2, x3) = reverse_3_out_agg₁(x1)
if_reverse_3_in_1_agg₅(x1, x2, x3, x4, x5) = if_reverse_3_in_1_agg₁(x5)
reverse_3_in_aag₃(x1, x2, x3) = reverse_3_in_aag₁(x3)
reverse_3_out_aag₃(x1, x2, x3) = reverse_3_out_aag₂(x1, x2)
if_reverse_3_in_1_aag₅(x1, x2, x3, x4, x5) = if_reverse_3_in_1_aag₁(x5)
reverse_2_out_ag₂(x1, x2) = reverse_2_out_ag₁(x1)
IF_REVERSE_3_IN_1_AAG₅(x1, x2, x3, x4, x5) = IF_REVERSE_3_IN_1_AAG₁(x5)
REVERSE_3_IN_AAG₃(x1, x2, x3) = REVERSE_3_IN_AAG₁(x3)
IF_REVERSE_3_IN_1_AGG₅(x1, x2, x3, x4, x5) = IF_REVERSE_3_IN_1_AGG₁(x5)
IF_REVERSE_2_IN_1_AG₃(x1, x2, x3) = IF_REVERSE_2_IN_1_AG₁(x3)
REVERSE_3_IN_AGG₃(x1, x2, x3) = REVERSE_3_IN_AGG₂(x2, x3)
REVERSE_2_IN_AG₂(x1, x2) = REVERSE_2_IN_AG₁(x2)

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:

REVERSE_2_IN_AG₂(X1s, X2s) -> IF_REVERSE_2_IN_1_AG₃(X1s, X2s, reverse_3_in_agg₃(X1s, []_0, X2s))
REVERSE_2_IN_AG₂(X1s, X2s) -> REVERSE_3_IN_AGG₃(X1s, []_0, X2s)
REVERSE_3_IN_AGG₃(._2₂(X, X1s), X2s, Ys) -> IF_REVERSE_3_IN_1_AGG₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
REVERSE_3_IN_AGG₃(._2₂(X, X1s), X2s, Ys) -> REVERSE_3_IN_AAG₃(X1s, ._2₂(X, X2s), Ys)
REVERSE_3_IN_AAG₃(._2₂(X, X1s), X2s, Ys) -> IF_REVERSE_3_IN_1_AAG₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
REVERSE_3_IN_AAG₃(._2₂(X, X1s), X2s, Ys) -> REVERSE_3_IN_AAG₃(X1s, ._2₂(X, X2s), Ys)

The TRS R consists of the following rules:

reverse_2_in_ag₂(X1s, X2s) -> if_reverse_2_in_1_ag₃(X1s, X2s, reverse_3_in_agg₃(X1s, []_0, X2s))
reverse_3_in_agg₃([]_0, Xs, Xs) -> reverse_3_out_agg₃([]_0, Xs, Xs)
reverse_3_in_agg₃(._2₂(X, X1s), X2s, Ys) -> if_reverse_3_in_1_agg₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
reverse_3_in_aag₃([]_0, Xs, Xs) -> reverse_3_out_aag₃([]_0, Xs, Xs)
reverse_3_in_aag₃(._2₂(X, X1s), X2s, Ys) -> if_reverse_3_in_1_aag₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
if_reverse_3_in_1_aag₅(X, X1s, X2s, Ys, reverse_3_out_aag₃(X1s, ._2₂(X, X2s), Ys)) -> reverse_3_out_aag₃(._2₂(X, X1s), X2s, Ys)
if_reverse_3_in_1_agg₅(X, X1s, X2s, Ys, reverse_3_out_aag₃(X1s, ._2₂(X, X2s), Ys)) -> reverse_3_out_agg₃(._2₂(X, X1s), X2s, Ys)
if_reverse_2_in_1_ag₃(X1s, X2s, reverse_3_out_agg₃(X1s, []_0, X2s)) -> reverse_2_out_ag₂(X1s, X2s)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

  ↳ PrologToPiTRSProof

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

REVERSE_3_IN_AAG₃(._2₂(X, X1s), X2s, Ys) -> REVERSE_3_IN_AAG₃(X1s, ._2₂(X, X2s), Ys)

The TRS R consists of the following rules:

reverse_2_in_ag₂(X1s, X2s) -> if_reverse_2_in_1_ag₃(X1s, X2s, reverse_3_in_agg₃(X1s, []_0, X2s))
reverse_3_in_agg₃([]_0, Xs, Xs) -> reverse_3_out_agg₃([]_0, Xs, Xs)
reverse_3_in_agg₃(._2₂(X, X1s), X2s, Ys) -> if_reverse_3_in_1_agg₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
reverse_3_in_aag₃([]_0, Xs, Xs) -> reverse_3_out_aag₃([]_0, Xs, Xs)
reverse_3_in_aag₃(._2₂(X, X1s), X2s, Ys) -> if_reverse_3_in_1_aag₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
if_reverse_3_in_1_aag₅(X, X1s, X2s, Ys, reverse_3_out_aag₃(X1s, ._2₂(X, X2s), Ys)) -> reverse_3_out_aag₃(._2₂(X, X1s), X2s, Ys)
if_reverse_3_in_1_agg₅(X, X1s, X2s, Ys, reverse_3_out_aag₃(X1s, ._2₂(X, X2s), Ys)) -> reverse_3_out_agg₃(._2₂(X, X1s), X2s, Ys)
if_reverse_2_in_1_ag₃(X1s, X2s, reverse_3_out_agg₃(X1s, []_0, X2s)) -> reverse_2_out_ag₂(X1s, X2s)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

                ↳ PiDP

                  ↳ PiDPToQDPProof

  ↳ PrologToPiTRSProof

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

REVERSE_3_IN_AAG₃(._2₂(X, X1s), X2s, Ys) -> REVERSE_3_IN_AAG₃(X1s, ._2₂(X, X2s), Ys)

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

            ↳ PiDP

              ↳ UsableRulesProof

                ↳ PiDP

                  ↳ PiDPToQDPProof

                    ↳ QDP

  ↳ PrologToPiTRSProof

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

REVERSE_3_IN_AAG₁(Ys) -> REVERSE_3_IN_AAG₁(Ys)

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

reverse_2_in_ag₂(X1s, X2s) -> if_reverse_2_in_1_ag₃(X1s, X2s, reverse_3_in_agg₃(X1s, []_0, X2s))
reverse_3_in_agg₃([]_0, Xs, Xs) -> reverse_3_out_agg₃([]_0, Xs, Xs)
reverse_3_in_agg₃(._2₂(X, X1s), X2s, Ys) -> if_reverse_3_in_1_agg₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
reverse_3_in_aag₃([]_0, Xs, Xs) -> reverse_3_out_aag₃([]_0, Xs, Xs)
reverse_3_in_aag₃(._2₂(X, X1s), X2s, Ys) -> if_reverse_3_in_1_aag₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
if_reverse_3_in_1_aag₅(X, X1s, X2s, Ys, reverse_3_out_aag₃(X1s, ._2₂(X, X2s), Ys)) -> reverse_3_out_aag₃(._2₂(X, X1s), X2s, Ys)
if_reverse_3_in_1_agg₅(X, X1s, X2s, Ys, reverse_3_out_aag₃(X1s, ._2₂(X, X2s), Ys)) -> reverse_3_out_agg₃(._2₂(X, X1s), X2s, Ys)
if_reverse_2_in_1_ag₃(X1s, X2s, reverse_3_out_agg₃(X1s, []_0, X2s)) -> reverse_2_out_ag₂(X1s, X2s)

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:

reverse_2_in_ag₂(X1s, X2s) -> if_reverse_2_in_1_ag₃(X1s, X2s, reverse_3_in_agg₃(X1s, []_0, X2s))
reverse_3_in_agg₃([]_0, Xs, Xs) -> reverse_3_out_agg₃([]_0, Xs, Xs)
reverse_3_in_agg₃(._2₂(X, X1s), X2s, Ys) -> if_reverse_3_in_1_agg₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
reverse_3_in_aag₃([]_0, Xs, Xs) -> reverse_3_out_aag₃([]_0, Xs, Xs)
reverse_3_in_aag₃(._2₂(X, X1s), X2s, Ys) -> if_reverse_3_in_1_aag₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
if_reverse_3_in_1_aag₅(X, X1s, X2s, Ys, reverse_3_out_aag₃(X1s, ._2₂(X, X2s), Ys)) -> reverse_3_out_aag₃(._2₂(X, X1s), X2s, Ys)
if_reverse_3_in_1_agg₅(X, X1s, X2s, Ys, reverse_3_out_aag₃(X1s, ._2₂(X, X2s), Ys)) -> reverse_3_out_agg₃(._2₂(X, X1s), X2s, Ys)
if_reverse_2_in_1_ag₃(X1s, X2s, reverse_3_out_agg₃(X1s, []_0, X2s)) -> reverse_2_out_ag₂(X1s, X2s)

REVERSE_2_IN_AG₂(X1s, X2s) -> IF_REVERSE_2_IN_1_AG₃(X1s, X2s, reverse_3_in_agg₃(X1s, []_0, X2s))
REVERSE_2_IN_AG₂(X1s, X2s) -> REVERSE_3_IN_AGG₃(X1s, []_0, X2s)
REVERSE_3_IN_AGG₃(._2₂(X, X1s), X2s, Ys) -> IF_REVERSE_3_IN_1_AGG₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
REVERSE_3_IN_AGG₃(._2₂(X, X1s), X2s, Ys) -> REVERSE_3_IN_AAG₃(X1s, ._2₂(X, X2s), Ys)
REVERSE_3_IN_AAG₃(._2₂(X, X1s), X2s, Ys) -> IF_REVERSE_3_IN_1_AAG₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
REVERSE_3_IN_AAG₃(._2₂(X, X1s), X2s, Ys) -> REVERSE_3_IN_AAG₃(X1s, ._2₂(X, X2s), Ys)

The TRS R consists of the following rules:

reverse_2_in_ag₂(X1s, X2s) -> if_reverse_2_in_1_ag₃(X1s, X2s, reverse_3_in_agg₃(X1s, []_0, X2s))
reverse_3_in_agg₃([]_0, Xs, Xs) -> reverse_3_out_agg₃([]_0, Xs, Xs)
reverse_3_in_agg₃(._2₂(X, X1s), X2s, Ys) -> if_reverse_3_in_1_agg₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
reverse_3_in_aag₃([]_0, Xs, Xs) -> reverse_3_out_aag₃([]_0, Xs, Xs)
reverse_3_in_aag₃(._2₂(X, X1s), X2s, Ys) -> if_reverse_3_in_1_aag₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
if_reverse_3_in_1_aag₅(X, X1s, X2s, Ys, reverse_3_out_aag₃(X1s, ._2₂(X, X2s), Ys)) -> reverse_3_out_aag₃(._2₂(X, X1s), X2s, Ys)
if_reverse_3_in_1_agg₅(X, X1s, X2s, Ys, reverse_3_out_aag₃(X1s, ._2₂(X, X2s), Ys)) -> reverse_3_out_agg₃(._2₂(X, X1s), X2s, Ys)
if_reverse_2_in_1_ag₃(X1s, X2s, reverse_3_out_agg₃(X1s, []_0, X2s)) -> reverse_2_out_ag₂(X1s, X2s)

The argument filtering Pi contains the following mapping:
reverse_2_in_ag₂(x1, x2) = reverse_2_in_ag₁(x2)
[]_0 = []_0
._2₂(x1, x2) = ._2₂(x1, x2)
if_reverse_2_in_1_ag₃(x1, x2, x3) = if_reverse_2_in_1_ag₂(x2, x3)
reverse_3_in_agg₃(x1, x2, x3) = reverse_3_in_agg₂(x2, x3)
reverse_3_out_agg₃(x1, x2, x3) = reverse_3_out_agg₃(x1, x2, x3)
if_reverse_3_in_1_agg₅(x1, x2, x3, x4, x5) = if_reverse_3_in_1_agg₃(x3, x4, x5)
reverse_3_in_aag₃(x1, x2, x3) = reverse_3_in_aag₁(x3)
reverse_3_out_aag₃(x1, x2, x3) = reverse_3_out_aag₃(x1, x2, x3)
if_reverse_3_in_1_aag₅(x1, x2, x3, x4, x5) = if_reverse_3_in_1_aag₂(x4, x5)
reverse_2_out_ag₂(x1, x2) = reverse_2_out_ag₂(x1, x2)
IF_REVERSE_3_IN_1_AAG₅(x1, x2, x3, x4, x5) = IF_REVERSE_3_IN_1_AAG₂(x4, x5)
REVERSE_3_IN_AAG₃(x1, x2, x3) = REVERSE_3_IN_AAG₁(x3)
IF_REVERSE_3_IN_1_AGG₅(x1, x2, x3, x4, x5) = IF_REVERSE_3_IN_1_AGG₃(x3, x4, x5)
IF_REVERSE_2_IN_1_AG₃(x1, x2, x3) = IF_REVERSE_2_IN_1_AG₂(x2, x3)
REVERSE_3_IN_AGG₃(x1, x2, x3) = REVERSE_3_IN_AGG₂(x2, x3)
REVERSE_2_IN_AG₂(x1, x2) = REVERSE_2_IN_AG₁(x2)

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:

REVERSE_2_IN_AG₂(X1s, X2s) -> IF_REVERSE_2_IN_1_AG₃(X1s, X2s, reverse_3_in_agg₃(X1s, []_0, X2s))
REVERSE_2_IN_AG₂(X1s, X2s) -> REVERSE_3_IN_AGG₃(X1s, []_0, X2s)
REVERSE_3_IN_AGG₃(._2₂(X, X1s), X2s, Ys) -> IF_REVERSE_3_IN_1_AGG₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
REVERSE_3_IN_AGG₃(._2₂(X, X1s), X2s, Ys) -> REVERSE_3_IN_AAG₃(X1s, ._2₂(X, X2s), Ys)
REVERSE_3_IN_AAG₃(._2₂(X, X1s), X2s, Ys) -> IF_REVERSE_3_IN_1_AAG₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
REVERSE_3_IN_AAG₃(._2₂(X, X1s), X2s, Ys) -> REVERSE_3_IN_AAG₃(X1s, ._2₂(X, X2s), Ys)

The TRS R consists of the following rules:

reverse_2_in_ag₂(X1s, X2s) -> if_reverse_2_in_1_ag₃(X1s, X2s, reverse_3_in_agg₃(X1s, []_0, X2s))
reverse_3_in_agg₃([]_0, Xs, Xs) -> reverse_3_out_agg₃([]_0, Xs, Xs)
reverse_3_in_agg₃(._2₂(X, X1s), X2s, Ys) -> if_reverse_3_in_1_agg₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
reverse_3_in_aag₃([]_0, Xs, Xs) -> reverse_3_out_aag₃([]_0, Xs, Xs)
reverse_3_in_aag₃(._2₂(X, X1s), X2s, Ys) -> if_reverse_3_in_1_aag₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
if_reverse_3_in_1_aag₅(X, X1s, X2s, Ys, reverse_3_out_aag₃(X1s, ._2₂(X, X2s), Ys)) -> reverse_3_out_aag₃(._2₂(X, X1s), X2s, Ys)
if_reverse_3_in_1_agg₅(X, X1s, X2s, Ys, reverse_3_out_aag₃(X1s, ._2₂(X, X2s), Ys)) -> reverse_3_out_agg₃(._2₂(X, X1s), X2s, Ys)
if_reverse_2_in_1_ag₃(X1s, X2s, reverse_3_out_agg₃(X1s, []_0, X2s)) -> reverse_2_out_ag₂(X1s, X2s)

The argument filtering Pi contains the following mapping:
reverse_2_in_ag₂(x1, x2) = reverse_2_in_ag₁(x2)
[]_0 = []_0
._2₂(x1, x2) = ._2₂(x1, x2)
if_reverse_2_in_1_ag₃(x1, x2, x3) = if_reverse_2_in_1_ag₂(x2, x3)
reverse_3_in_agg₃(x1, x2, x3) = reverse_3_in_agg₂(x2, x3)
reverse_3_out_agg₃(x1, x2, x3) = reverse_3_out_agg₃(x1, x2, x3)
if_reverse_3_in_1_agg₅(x1, x2, x3, x4, x5) = if_reverse_3_in_1_agg₃(x3, x4, x5)
reverse_3_in_aag₃(x1, x2, x3) = reverse_3_in_aag₁(x3)
reverse_3_out_aag₃(x1, x2, x3) = reverse_3_out_aag₃(x1, x2, x3)
if_reverse_3_in_1_aag₅(x1, x2, x3, x4, x5) = if_reverse_3_in_1_aag₂(x4, x5)
reverse_2_out_ag₂(x1, x2) = reverse_2_out_ag₂(x1, x2)
IF_REVERSE_3_IN_1_AAG₅(x1, x2, x3, x4, x5) = IF_REVERSE_3_IN_1_AAG₂(x4, x5)
REVERSE_3_IN_AAG₃(x1, x2, x3) = REVERSE_3_IN_AAG₁(x3)
IF_REVERSE_3_IN_1_AGG₅(x1, x2, x3, x4, x5) = IF_REVERSE_3_IN_1_AGG₃(x3, x4, x5)
IF_REVERSE_2_IN_1_AG₃(x1, x2, x3) = IF_REVERSE_2_IN_1_AG₂(x2, x3)
REVERSE_3_IN_AGG₃(x1, x2, x3) = REVERSE_3_IN_AGG₂(x2, x3)
REVERSE_2_IN_AG₂(x1, x2) = REVERSE_2_IN_AG₁(x2)

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

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

REVERSE_3_IN_AAG₃(._2₂(X, X1s), X2s, Ys) -> REVERSE_3_IN_AAG₃(X1s, ._2₂(X, X2s), Ys)

The TRS R consists of the following rules:

reverse_2_in_ag₂(X1s, X2s) -> if_reverse_2_in_1_ag₃(X1s, X2s, reverse_3_in_agg₃(X1s, []_0, X2s))
reverse_3_in_agg₃([]_0, Xs, Xs) -> reverse_3_out_agg₃([]_0, Xs, Xs)
reverse_3_in_agg₃(._2₂(X, X1s), X2s, Ys) -> if_reverse_3_in_1_agg₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
reverse_3_in_aag₃([]_0, Xs, Xs) -> reverse_3_out_aag₃([]_0, Xs, Xs)
reverse_3_in_aag₃(._2₂(X, X1s), X2s, Ys) -> if_reverse_3_in_1_aag₅(X, X1s, X2s, Ys, reverse_3_in_aag₃(X1s, ._2₂(X, X2s), Ys))
if_reverse_3_in_1_aag₅(X, X1s, X2s, Ys, reverse_3_out_aag₃(X1s, ._2₂(X, X2s), Ys)) -> reverse_3_out_aag₃(._2₂(X, X1s), X2s, Ys)
if_reverse_3_in_1_agg₅(X, X1s, X2s, Ys, reverse_3_out_aag₃(X1s, ._2₂(X, X2s), Ys)) -> reverse_3_out_agg₃(._2₂(X, X1s), X2s, Ys)
if_reverse_2_in_1_ag₃(X1s, X2s, reverse_3_out_agg₃(X1s, []_0, X2s)) -> reverse_2_out_ag₂(X1s, X2s)

The argument filtering Pi contains the following mapping:
reverse_2_in_ag₂(x1, x2) = reverse_2_in_ag₁(x2)
[]_0 = []_0
._2₂(x1, x2) = ._2₂(x1, x2)
if_reverse_2_in_1_ag₃(x1, x2, x3) = if_reverse_2_in_1_ag₂(x2, x3)
reverse_3_in_agg₃(x1, x2, x3) = reverse_3_in_agg₂(x2, x3)
reverse_3_out_agg₃(x1, x2, x3) = reverse_3_out_agg₃(x1, x2, x3)
if_reverse_3_in_1_agg₅(x1, x2, x3, x4, x5) = if_reverse_3_in_1_agg₃(x3, x4, x5)
reverse_3_in_aag₃(x1, x2, x3) = reverse_3_in_aag₁(x3)
reverse_3_out_aag₃(x1, x2, x3) = reverse_3_out_aag₃(x1, x2, x3)
if_reverse_3_in_1_aag₅(x1, x2, x3, x4, x5) = if_reverse_3_in_1_aag₂(x4, x5)
reverse_2_out_ag₂(x1, x2) = reverse_2_out_ag₂(x1, x2)
REVERSE_3_IN_AAG₃(x1, x2, x3) = REVERSE_3_IN_AAG₁(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:

REVERSE_3_IN_AAG₃(._2₂(X, X1s), X2s, Ys) -> REVERSE_3_IN_AAG₃(X1s, ._2₂(X, X2s), Ys)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

                ↳ PiDP

                  ↳ PiDPToQDPProof

                    ↳ QDP

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

REVERSE_3_IN_AAG₁(Ys) -> REVERSE_3_IN_AAG₁(Ys)

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