Left Termination proof of /tmp/tmpSOJ2uS/NJ2.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), X, RES) :- g₄(Tail, X, .₂(Head, Tail), RES).
g₄(A, B, C, RES) :- f₃(A, .₂(B, C), RES).

With regard to the inferred argument filtering the predicates were used in the following modes:
f₃: (b,b,f)
g₄: (b,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₃([]_0, RES, RES) -> f_3_out_gga₃([]_0, RES, RES)
f_3_in_gga₃(._2₂(Head, Tail), X, RES) -> if_f_3_in_1_gga₅(Head, Tail, X, RES, g_4_in_ggga₄(Tail, X, ._2₂(Head, Tail), RES))
g_4_in_ggga₄(A, B, C, RES) -> if_g_4_in_1_ggga₅(A, B, C, RES, f_3_in_gga₃(A, ._2₂(B, C), RES))
if_g_4_in_1_ggga₅(A, B, C, RES, f_3_out_gga₃(A, ._2₂(B, C), RES)) -> g_4_out_ggga₄(A, B, C, RES)
if_f_3_in_1_gga₅(Head, Tail, X, RES, g_4_out_ggga₄(Tail, X, ._2₂(Head, Tail), RES)) -> f_3_out_gga₃(._2₂(Head, Tail), X, 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₃([]_0, RES, RES) -> f_3_out_gga₃([]_0, RES, RES)
f_3_in_gga₃(._2₂(Head, Tail), X, RES) -> if_f_3_in_1_gga₅(Head, Tail, X, RES, g_4_in_ggga₄(Tail, X, ._2₂(Head, Tail), RES))
g_4_in_ggga₄(A, B, C, RES) -> if_g_4_in_1_ggga₅(A, B, C, RES, f_3_in_gga₃(A, ._2₂(B, C), RES))
if_g_4_in_1_ggga₅(A, B, C, RES, f_3_out_gga₃(A, ._2₂(B, C), RES)) -> g_4_out_ggga₄(A, B, C, RES)
if_f_3_in_1_gga₅(Head, Tail, X, RES, g_4_out_ggga₄(Tail, X, ._2₂(Head, Tail), RES)) -> f_3_out_gga₃(._2₂(Head, Tail), X, RES)

F_3_IN_GGA₃(._2₂(Head, Tail), X, RES) -> IF_F_3_IN_1_GGA₅(Head, Tail, X, RES, g_4_in_ggga₄(Tail, X, ._2₂(Head, Tail), RES))
F_3_IN_GGA₃(._2₂(Head, Tail), X, RES) -> G_4_IN_GGGA₄(Tail, X, ._2₂(Head, Tail), RES)
G_4_IN_GGGA₄(A, B, C, RES) -> IF_G_4_IN_1_GGGA₅(A, B, C, RES, f_3_in_gga₃(A, ._2₂(B, C), RES))
G_4_IN_GGGA₄(A, B, C, RES) -> F_3_IN_GGA₃(A, ._2₂(B, C), RES)

The TRS R consists of the following rules:

f_3_in_gga₃([]_0, RES, RES) -> f_3_out_gga₃([]_0, RES, RES)
f_3_in_gga₃(._2₂(Head, Tail), X, RES) -> if_f_3_in_1_gga₅(Head, Tail, X, RES, g_4_in_ggga₄(Tail, X, ._2₂(Head, Tail), RES))
g_4_in_ggga₄(A, B, C, RES) -> if_g_4_in_1_ggga₅(A, B, C, RES, f_3_in_gga₃(A, ._2₂(B, C), RES))
if_g_4_in_1_ggga₅(A, B, C, RES, f_3_out_gga₃(A, ._2₂(B, C), RES)) -> g_4_out_ggga₄(A, B, C, RES)
if_f_3_in_1_gga₅(Head, Tail, X, RES, g_4_out_ggga₄(Tail, X, ._2₂(Head, Tail), RES)) -> f_3_out_gga₃(._2₂(Head, Tail), X, 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, x5) = if_f_3_in_1_gga₁(x5)
g_4_in_ggga₄(x1, x2, x3, x4) = g_4_in_ggga₃(x1, x2, x3)
if_g_4_in_1_ggga₅(x1, x2, x3, x4, x5) = if_g_4_in_1_ggga₁(x5)
g_4_out_ggga₄(x1, x2, x3, x4) = g_4_out_ggga₁(x4)
G_4_IN_GGGA₄(x1, x2, x3, x4) = G_4_IN_GGGA₃(x1, x2, x3)
F_3_IN_GGA₃(x1, x2, x3) = F_3_IN_GGA₂(x1, x2)
IF_F_3_IN_1_GGA₅(x1, x2, x3, x4, x5) = IF_F_3_IN_1_GGA₁(x5)
IF_G_4_IN_1_GGGA₅(x1, x2, x3, x4, x5) = IF_G_4_IN_1_GGGA₁(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₃(._2₂(Head, Tail), X, RES) -> IF_F_3_IN_1_GGA₅(Head, Tail, X, RES, g_4_in_ggga₄(Tail, X, ._2₂(Head, Tail), RES))
F_3_IN_GGA₃(._2₂(Head, Tail), X, RES) -> G_4_IN_GGGA₄(Tail, X, ._2₂(Head, Tail), RES)
G_4_IN_GGGA₄(A, B, C, RES) -> IF_G_4_IN_1_GGGA₅(A, B, C, RES, f_3_in_gga₃(A, ._2₂(B, C), RES))
G_4_IN_GGGA₄(A, B, C, RES) -> F_3_IN_GGA₃(A, ._2₂(B, C), RES)

The TRS R consists of the following rules:

f_3_in_gga₃([]_0, RES, RES) -> f_3_out_gga₃([]_0, RES, RES)
f_3_in_gga₃(._2₂(Head, Tail), X, RES) -> if_f_3_in_1_gga₅(Head, Tail, X, RES, g_4_in_ggga₄(Tail, X, ._2₂(Head, Tail), RES))
g_4_in_ggga₄(A, B, C, RES) -> if_g_4_in_1_ggga₅(A, B, C, RES, f_3_in_gga₃(A, ._2₂(B, C), RES))
if_g_4_in_1_ggga₅(A, B, C, RES, f_3_out_gga₃(A, ._2₂(B, C), RES)) -> g_4_out_ggga₄(A, B, C, RES)
if_f_3_in_1_gga₅(Head, Tail, X, RES, g_4_out_ggga₄(Tail, X, ._2₂(Head, Tail), RES)) -> f_3_out_gga₃(._2₂(Head, Tail), X, RES)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

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

F_3_IN_GGA₃(._2₂(Head, Tail), X, RES) -> G_4_IN_GGGA₄(Tail, X, ._2₂(Head, Tail), RES)
G_4_IN_GGGA₄(A, B, C, RES) -> F_3_IN_GGA₃(A, ._2₂(B, C), RES)

The TRS R consists of the following rules:

f_3_in_gga₃([]_0, RES, RES) -> f_3_out_gga₃([]_0, RES, RES)
f_3_in_gga₃(._2₂(Head, Tail), X, RES) -> if_f_3_in_1_gga₅(Head, Tail, X, RES, g_4_in_ggga₄(Tail, X, ._2₂(Head, Tail), RES))
g_4_in_ggga₄(A, B, C, RES) -> if_g_4_in_1_ggga₅(A, B, C, RES, f_3_in_gga₃(A, ._2₂(B, C), RES))
if_g_4_in_1_ggga₅(A, B, C, RES, f_3_out_gga₃(A, ._2₂(B, C), RES)) -> g_4_out_ggga₄(A, B, C, RES)
if_f_3_in_1_gga₅(Head, Tail, X, RES, g_4_out_ggga₄(Tail, X, ._2₂(Head, Tail), RES)) -> f_3_out_gga₃(._2₂(Head, Tail), X, 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, x5) = if_f_3_in_1_gga₁(x5)
g_4_in_ggga₄(x1, x2, x3, x4) = g_4_in_ggga₃(x1, x2, x3)
if_g_4_in_1_ggga₅(x1, x2, x3, x4, x5) = if_g_4_in_1_ggga₁(x5)
g_4_out_ggga₄(x1, x2, x3, x4) = g_4_out_ggga₁(x4)
G_4_IN_GGGA₄(x1, x2, x3, x4) = G_4_IN_GGGA₃(x1, x2, x3)
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₃(._2₂(Head, Tail), X, RES) -> G_4_IN_GGGA₄(Tail, X, ._2₂(Head, Tail), RES)
G_4_IN_GGGA₄(A, B, C, RES) -> F_3_IN_GGA₃(A, ._2₂(B, C), RES)

R is empty.
The argument filtering Pi contains the following mapping:
._2₂(x1, x2) = ._2₂(x1, x2)
G_4_IN_GGGA₄(x1, x2, x3, x4) = G_4_IN_GGGA₃(x1, x2, x3)
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₂(._2₂(Head, Tail), X) -> G_4_IN_GGGA₃(Tail, X, ._2₂(Head, Tail))
G_4_IN_GGGA₃(A, B, C) -> F_3_IN_GGA₂(A, ._2₂(B, C))

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

G_4_IN_GGGA₃(A, B, C) -> F_3_IN_GGA₂(A, ._2₂(B, C))
The graph contains the following edges 1 >= 1
F_3_IN_GGA₂(._2₂(Head, Tail), X) -> G_4_IN_GGGA₃(Tail, X, ._2₂(Head, Tail))
The graph contains the following edges 1 > 1, 2 >= 2, 1 >= 3