Left Termination proof of /tmp/tmp3mp4a3/NJ5.pl

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

↳ PROLOG

  ↳ PrologToPiTRSProof

f₃(RES, {}₀, RES).
f₃({}₀, .₂(Head, Tail), RES) :- f₃(.₂(Head, Tail), Tail, RES).
f₃(.₂(Head, Tail), Y, RES) :- f₃(Y, Tail, RES).

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

f_3_in_gga₃(RES, []_0, RES) -> f_3_out_gga₃(RES, []_0, RES)
f_3_in_gga₃([]_0, ._2₂(Head, Tail), RES) -> if_f_3_in_1_gga₄(Head, Tail, RES, f_3_in_gga₃(._2₂(Head, Tail), Tail, RES))
f_3_in_gga₃(._2₂(Head, Tail), Y, RES) -> if_f_3_in_2_gga₅(Head, Tail, Y, RES, f_3_in_gga₃(Y, Tail, RES))
if_f_3_in_2_gga₅(Head, Tail, Y, RES, f_3_out_gga₃(Y, Tail, RES)) -> f_3_out_gga₃(._2₂(Head, Tail), Y, RES)
if_f_3_in_1_gga₄(Head, Tail, RES, f_3_out_gga₃(._2₂(Head, Tail), Tail, RES)) -> f_3_out_gga₃([]_0, ._2₂(Head, Tail), 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:

f_3_in_gga₃(RES, []_0, RES) -> f_3_out_gga₃(RES, []_0, RES)
f_3_in_gga₃([]_0, ._2₂(Head, Tail), RES) -> if_f_3_in_1_gga₄(Head, Tail, RES, f_3_in_gga₃(._2₂(Head, Tail), Tail, RES))
f_3_in_gga₃(._2₂(Head, Tail), Y, RES) -> if_f_3_in_2_gga₅(Head, Tail, Y, RES, f_3_in_gga₃(Y, Tail, RES))
if_f_3_in_2_gga₅(Head, Tail, Y, RES, f_3_out_gga₃(Y, Tail, RES)) -> f_3_out_gga₃(._2₂(Head, Tail), Y, RES)
if_f_3_in_1_gga₄(Head, Tail, RES, f_3_out_gga₃(._2₂(Head, Tail), Tail, RES)) -> f_3_out_gga₃([]_0, ._2₂(Head, Tail), RES)

F_3_IN_GGA₃([]_0, ._2₂(Head, Tail), RES) -> IF_F_3_IN_1_GGA₄(Head, Tail, RES, f_3_in_gga₃(._2₂(Head, Tail), Tail, RES))
F_3_IN_GGA₃([]_0, ._2₂(Head, Tail), RES) -> F_3_IN_GGA₃(._2₂(Head, Tail), Tail, RES)
F_3_IN_GGA₃(._2₂(Head, Tail), Y, RES) -> IF_F_3_IN_2_GGA₅(Head, Tail, Y, RES, f_3_in_gga₃(Y, Tail, RES))
F_3_IN_GGA₃(._2₂(Head, Tail), Y, RES) -> F_3_IN_GGA₃(Y, Tail, RES)

The TRS R consists of the following rules:

f_3_in_gga₃(RES, []_0, RES) -> f_3_out_gga₃(RES, []_0, RES)
f_3_in_gga₃([]_0, ._2₂(Head, Tail), RES) -> if_f_3_in_1_gga₄(Head, Tail, RES, f_3_in_gga₃(._2₂(Head, Tail), Tail, RES))
f_3_in_gga₃(._2₂(Head, Tail), Y, RES) -> if_f_3_in_2_gga₅(Head, Tail, Y, RES, f_3_in_gga₃(Y, Tail, RES))
if_f_3_in_2_gga₅(Head, Tail, Y, RES, f_3_out_gga₃(Y, Tail, RES)) -> f_3_out_gga₃(._2₂(Head, Tail), Y, RES)
if_f_3_in_1_gga₄(Head, Tail, RES, f_3_out_gga₃(._2₂(Head, Tail), Tail, RES)) -> f_3_out_gga₃([]_0, ._2₂(Head, Tail), RES)

The argument filtering Pi contains the following mapping:
f_3_in_gga₃(x1, x2, x3) = f_3_in_gga₂(x1, x2)
[]_0 = []_0
._2₂(x1, x2) = ._2₂(x1, x2)
f_3_out_gga₃(x1, x2, x3) = f_3_out_gga₁(x3)
if_f_3_in_1_gga₄(x1, x2, x3, x4) = if_f_3_in_1_gga₁(x4)
if_f_3_in_2_gga₅(x1, x2, x3, x4, x5) = if_f_3_in_2_gga₁(x5)
F_3_IN_GGA₃(x1, x2, x3) = F_3_IN_GGA₂(x1, x2)
IF_F_3_IN_1_GGA₄(x1, x2, x3, x4) = IF_F_3_IN_1_GGA₁(x4)
IF_F_3_IN_2_GGA₅(x1, x2, x3, x4, x5) = IF_F_3_IN_2_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:

F_3_IN_GGA₃([]_0, ._2₂(Head, Tail), RES) -> IF_F_3_IN_1_GGA₄(Head, Tail, RES, f_3_in_gga₃(._2₂(Head, Tail), Tail, RES))
F_3_IN_GGA₃([]_0, ._2₂(Head, Tail), RES) -> F_3_IN_GGA₃(._2₂(Head, Tail), Tail, RES)
F_3_IN_GGA₃(._2₂(Head, Tail), Y, RES) -> IF_F_3_IN_2_GGA₅(Head, Tail, Y, RES, f_3_in_gga₃(Y, Tail, RES))
F_3_IN_GGA₃(._2₂(Head, Tail), Y, RES) -> F_3_IN_GGA₃(Y, Tail, RES)

The TRS R consists of the following rules:

f_3_in_gga₃(RES, []_0, RES) -> f_3_out_gga₃(RES, []_0, RES)
f_3_in_gga₃([]_0, ._2₂(Head, Tail), RES) -> if_f_3_in_1_gga₄(Head, Tail, RES, f_3_in_gga₃(._2₂(Head, Tail), Tail, RES))
f_3_in_gga₃(._2₂(Head, Tail), Y, RES) -> if_f_3_in_2_gga₅(Head, Tail, Y, RES, f_3_in_gga₃(Y, Tail, RES))
if_f_3_in_2_gga₅(Head, Tail, Y, RES, f_3_out_gga₃(Y, Tail, RES)) -> f_3_out_gga₃(._2₂(Head, Tail), Y, RES)
if_f_3_in_1_gga₄(Head, Tail, RES, f_3_out_gga₃(._2₂(Head, Tail), Tail, RES)) -> f_3_out_gga₃([]_0, ._2₂(Head, Tail), RES)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

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

F_3_IN_GGA₃([]_0, ._2₂(Head, Tail), RES) -> F_3_IN_GGA₃(._2₂(Head, Tail), Tail, RES)
F_3_IN_GGA₃(._2₂(Head, Tail), Y, RES) -> F_3_IN_GGA₃(Y, Tail, RES)

The TRS R consists of the following rules:

f_3_in_gga₃(RES, []_0, RES) -> f_3_out_gga₃(RES, []_0, RES)
f_3_in_gga₃([]_0, ._2₂(Head, Tail), RES) -> if_f_3_in_1_gga₄(Head, Tail, RES, f_3_in_gga₃(._2₂(Head, Tail), Tail, RES))
f_3_in_gga₃(._2₂(Head, Tail), Y, RES) -> if_f_3_in_2_gga₅(Head, Tail, Y, RES, f_3_in_gga₃(Y, Tail, RES))
if_f_3_in_2_gga₅(Head, Tail, Y, RES, f_3_out_gga₃(Y, Tail, RES)) -> f_3_out_gga₃(._2₂(Head, Tail), Y, RES)
if_f_3_in_1_gga₄(Head, Tail, RES, f_3_out_gga₃(._2₂(Head, Tail), Tail, RES)) -> f_3_out_gga₃([]_0, ._2₂(Head, Tail), RES)

The argument filtering Pi contains the following mapping:
f_3_in_gga₃(x1, x2, x3) = f_3_in_gga₂(x1, x2)
[]_0 = []_0
._2₂(x1, x2) = ._2₂(x1, x2)
f_3_out_gga₃(x1, x2, x3) = f_3_out_gga₁(x3)
if_f_3_in_1_gga₄(x1, x2, x3, x4) = if_f_3_in_1_gga₁(x4)
if_f_3_in_2_gga₅(x1, x2, x3, x4, x5) = if_f_3_in_2_gga₁(x5)
F_3_IN_GGA₃(x1, x2, x3) = F_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:

F_3_IN_GGA₃([]_0, ._2₂(Head, Tail), RES) -> F_3_IN_GGA₃(._2₂(Head, Tail), Tail, RES)
F_3_IN_GGA₃(._2₂(Head, Tail), Y, RES) -> F_3_IN_GGA₃(Y, Tail, RES)

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

F_3_IN_GGA₂([]_0, ._2₂(Head, Tail)) -> F_3_IN_GGA₂(._2₂(Head, Tail), Tail)
F_3_IN_GGA₂(._2₂(Head, Tail), Y) -> F_3_IN_GGA₂(Y, Tail)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {F_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:

F_3_IN_GGA₂(._2₂(Head, Tail), Y) -> F_3_IN_GGA₂(Y, Tail)
The graph contains the following edges 2 >= 1, 1 > 2
F_3_IN_GGA₂([]_0, ._2₂(Head, Tail)) -> F_3_IN_GGA₂(._2₂(Head, Tail), Tail)
The graph contains the following edges 2 >= 1, 2 > 2