Left Termination proof of /tmp/tmpFdropp/NJ1.pl

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

↳ PROLOG

  ↳ PrologToPiTRSProof

rev₂(LS, RES) :- r1₃(LS, {}₀, RES).
r1₃({}₀, RES, RES).
r1₃(.₂(X, Xs), Accm, RES) :- r1₃(Xs, .₂(X, Accm), RES).

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

rev_2_in_ga₂(LS, RES) -> if_rev_2_in_1_ga₃(LS, RES, r1_3_in_gga₃(LS, []_0, RES))
r1_3_in_gga₃([]_0, RES, RES) -> r1_3_out_gga₃([]_0, RES, RES)
r1_3_in_gga₃(._2₂(X, Xs), Accm, RES) -> if_r1_3_in_1_gga₅(X, Xs, Accm, RES, r1_3_in_gga₃(Xs, ._2₂(X, Accm), RES))
if_r1_3_in_1_gga₅(X, Xs, Accm, RES, r1_3_out_gga₃(Xs, ._2₂(X, Accm), RES)) -> r1_3_out_gga₃(._2₂(X, Xs), Accm, RES)
if_rev_2_in_1_ga₃(LS, RES, r1_3_out_gga₃(LS, []_0, RES)) -> rev_2_out_ga₂(LS, RES)

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:

rev_2_in_ga₂(LS, RES) -> if_rev_2_in_1_ga₃(LS, RES, r1_3_in_gga₃(LS, []_0, RES))
r1_3_in_gga₃([]_0, RES, RES) -> r1_3_out_gga₃([]_0, RES, RES)
r1_3_in_gga₃(._2₂(X, Xs), Accm, RES) -> if_r1_3_in_1_gga₅(X, Xs, Accm, RES, r1_3_in_gga₃(Xs, ._2₂(X, Accm), RES))
if_r1_3_in_1_gga₅(X, Xs, Accm, RES, r1_3_out_gga₃(Xs, ._2₂(X, Accm), RES)) -> r1_3_out_gga₃(._2₂(X, Xs), Accm, RES)
if_rev_2_in_1_ga₃(LS, RES, r1_3_out_gga₃(LS, []_0, RES)) -> rev_2_out_ga₂(LS, RES)

REV_2_IN_GA₂(LS, RES) -> IF_REV_2_IN_1_GA₃(LS, RES, r1_3_in_gga₃(LS, []_0, RES))
REV_2_IN_GA₂(LS, RES) -> R1_3_IN_GGA₃(LS, []_0, RES)
R1_3_IN_GGA₃(._2₂(X, Xs), Accm, RES) -> IF_R1_3_IN_1_GGA₅(X, Xs, Accm, RES, r1_3_in_gga₃(Xs, ._2₂(X, Accm), RES))
R1_3_IN_GGA₃(._2₂(X, Xs), Accm, RES) -> R1_3_IN_GGA₃(Xs, ._2₂(X, Accm), RES)

The TRS R consists of the following rules:

rev_2_in_ga₂(LS, RES) -> if_rev_2_in_1_ga₃(LS, RES, r1_3_in_gga₃(LS, []_0, RES))
r1_3_in_gga₃([]_0, RES, RES) -> r1_3_out_gga₃([]_0, RES, RES)
r1_3_in_gga₃(._2₂(X, Xs), Accm, RES) -> if_r1_3_in_1_gga₅(X, Xs, Accm, RES, r1_3_in_gga₃(Xs, ._2₂(X, Accm), RES))
if_r1_3_in_1_gga₅(X, Xs, Accm, RES, r1_3_out_gga₃(Xs, ._2₂(X, Accm), RES)) -> r1_3_out_gga₃(._2₂(X, Xs), Accm, RES)
if_rev_2_in_1_ga₃(LS, RES, r1_3_out_gga₃(LS, []_0, RES)) -> rev_2_out_ga₂(LS, RES)

The argument filtering Pi contains the following mapping:
rev_2_in_ga₂(x1, x2) = rev_2_in_ga₁(x1)
[]_0 = []_0
._2₂(x1, x2) = ._2₂(x1, x2)
if_rev_2_in_1_ga₃(x1, x2, x3) = if_rev_2_in_1_ga₁(x3)
r1_3_in_gga₃(x1, x2, x3) = r1_3_in_gga₂(x1, x2)
r1_3_out_gga₃(x1, x2, x3) = r1_3_out_gga₁(x3)
if_r1_3_in_1_gga₅(x1, x2, x3, x4, x5) = if_r1_3_in_1_gga₁(x5)
rev_2_out_ga₂(x1, x2) = rev_2_out_ga₁(x2)
REV_2_IN_GA₂(x1, x2) = REV_2_IN_GA₁(x1)
IF_REV_2_IN_1_GA₃(x1, x2, x3) = IF_REV_2_IN_1_GA₁(x3)
R1_3_IN_GGA₃(x1, x2, x3) = R1_3_IN_GGA₂(x1, x2)
IF_R1_3_IN_1_GGA₅(x1, x2, x3, x4, x5) = IF_R1_3_IN_1_GGA₁(x5)

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:

REV_2_IN_GA₂(LS, RES) -> IF_REV_2_IN_1_GA₃(LS, RES, r1_3_in_gga₃(LS, []_0, RES))
REV_2_IN_GA₂(LS, RES) -> R1_3_IN_GGA₃(LS, []_0, RES)
R1_3_IN_GGA₃(._2₂(X, Xs), Accm, RES) -> IF_R1_3_IN_1_GGA₅(X, Xs, Accm, RES, r1_3_in_gga₃(Xs, ._2₂(X, Accm), RES))
R1_3_IN_GGA₃(._2₂(X, Xs), Accm, RES) -> R1_3_IN_GGA₃(Xs, ._2₂(X, Accm), RES)

The TRS R consists of the following rules:

rev_2_in_ga₂(LS, RES) -> if_rev_2_in_1_ga₃(LS, RES, r1_3_in_gga₃(LS, []_0, RES))
r1_3_in_gga₃([]_0, RES, RES) -> r1_3_out_gga₃([]_0, RES, RES)
r1_3_in_gga₃(._2₂(X, Xs), Accm, RES) -> if_r1_3_in_1_gga₅(X, Xs, Accm, RES, r1_3_in_gga₃(Xs, ._2₂(X, Accm), RES))
if_r1_3_in_1_gga₅(X, Xs, Accm, RES, r1_3_out_gga₃(Xs, ._2₂(X, Accm), RES)) -> r1_3_out_gga₃(._2₂(X, Xs), Accm, RES)
if_rev_2_in_1_ga₃(LS, RES, r1_3_out_gga₃(LS, []_0, RES)) -> rev_2_out_ga₂(LS, RES)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

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

R1_3_IN_GGA₃(._2₂(X, Xs), Accm, RES) -> R1_3_IN_GGA₃(Xs, ._2₂(X, Accm), RES)

The TRS R consists of the following rules:

rev_2_in_ga₂(LS, RES) -> if_rev_2_in_1_ga₃(LS, RES, r1_3_in_gga₃(LS, []_0, RES))
r1_3_in_gga₃([]_0, RES, RES) -> r1_3_out_gga₃([]_0, RES, RES)
r1_3_in_gga₃(._2₂(X, Xs), Accm, RES) -> if_r1_3_in_1_gga₅(X, Xs, Accm, RES, r1_3_in_gga₃(Xs, ._2₂(X, Accm), RES))
if_r1_3_in_1_gga₅(X, Xs, Accm, RES, r1_3_out_gga₃(Xs, ._2₂(X, Accm), RES)) -> r1_3_out_gga₃(._2₂(X, Xs), Accm, RES)
if_rev_2_in_1_ga₃(LS, RES, r1_3_out_gga₃(LS, []_0, RES)) -> rev_2_out_ga₂(LS, RES)

The argument filtering Pi contains the following mapping:
rev_2_in_ga₂(x1, x2) = rev_2_in_ga₁(x1)
[]_0 = []_0
._2₂(x1, x2) = ._2₂(x1, x2)
if_rev_2_in_1_ga₃(x1, x2, x3) = if_rev_2_in_1_ga₁(x3)
r1_3_in_gga₃(x1, x2, x3) = r1_3_in_gga₂(x1, x2)
r1_3_out_gga₃(x1, x2, x3) = r1_3_out_gga₁(x3)
if_r1_3_in_1_gga₅(x1, x2, x3, x4, x5) = if_r1_3_in_1_gga₁(x5)
rev_2_out_ga₂(x1, x2) = rev_2_out_ga₁(x2)
R1_3_IN_GGA₃(x1, x2, x3) = R1_3_IN_GGA₂(x1, x2)

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

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

R1_3_IN_GGA₃(._2₂(X, Xs), Accm, RES) -> R1_3_IN_GGA₃(Xs, ._2₂(X, Accm), RES)

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

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

                ↳ PiDP

                  ↳ PiDPToQDPProof

                    ↳ QDP

                      ↳ QDPSizeChangeProof

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

R1_3_IN_GGA₂(._2₂(X, Xs), Accm) -> R1_3_IN_GGA₂(Xs, ._2₂(X, Accm))

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {R1_3_IN_GGA₂}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

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

R1_3_IN_GGA₂(._2₂(X, Xs), Accm) -> R1_3_IN_GGA₂(Xs, ._2₂(X, Accm))
The graph contains the following edges 1 > 1