Left Termination proof of /tmp/tmpehJ9oS/pl4.0.1.pl

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

↳ PROLOG

  ↳ PrologToPiTRSProof

append₃({}₀, L, L).
append₃(.₂(H, L1), L2, .₂(H, L3)) :- append₃(L1, L2, L3).
append3₄(A, B, C, D) :- append₃(A, B, E), append₃(E, C, D).

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

append3_4_in_ggga₄(A, B, C, D) -> if_append3_4_in_1_ggga₅(A, B, C, D, append_3_in_gga₃(A, B, E))
append_3_in_gga₃([]_0, L, L) -> append_3_out_gga₃([]_0, L, L)
append_3_in_gga₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> if_append_3_in_1_gga₅(H, L1, L2, L3, append_3_in_gga₃(L1, L2, L3))
if_append_3_in_1_gga₅(H, L1, L2, L3, append_3_out_gga₃(L1, L2, L3)) -> append_3_out_gga₃(._2₂(H, L1), L2, ._2₂(H, L3))
if_append3_4_in_1_ggga₅(A, B, C, D, append_3_out_gga₃(A, B, E)) -> if_append3_4_in_2_ggga₆(A, B, C, D, E, append_3_in_gga₃(E, C, D))
if_append3_4_in_2_ggga₆(A, B, C, D, E, append_3_out_gga₃(E, C, D)) -> append3_4_out_ggga₄(A, B, C, D)

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:

append3_4_in_ggga₄(A, B, C, D) -> if_append3_4_in_1_ggga₅(A, B, C, D, append_3_in_gga₃(A, B, E))
append_3_in_gga₃([]_0, L, L) -> append_3_out_gga₃([]_0, L, L)
append_3_in_gga₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> if_append_3_in_1_gga₅(H, L1, L2, L3, append_3_in_gga₃(L1, L2, L3))
if_append_3_in_1_gga₅(H, L1, L2, L3, append_3_out_gga₃(L1, L2, L3)) -> append_3_out_gga₃(._2₂(H, L1), L2, ._2₂(H, L3))
if_append3_4_in_1_ggga₅(A, B, C, D, append_3_out_gga₃(A, B, E)) -> if_append3_4_in_2_ggga₆(A, B, C, D, E, append_3_in_gga₃(E, C, D))
if_append3_4_in_2_ggga₆(A, B, C, D, E, append_3_out_gga₃(E, C, D)) -> append3_4_out_ggga₄(A, B, C, D)

APPEND3_4_IN_GGGA₄(A, B, C, D) -> IF_APPEND3_4_IN_1_GGGA₅(A, B, C, D, append_3_in_gga₃(A, B, E))
APPEND3_4_IN_GGGA₄(A, B, C, D) -> APPEND_3_IN_GGA₃(A, B, E)
APPEND_3_IN_GGA₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> IF_APPEND_3_IN_1_GGA₅(H, L1, L2, L3, append_3_in_gga₃(L1, L2, L3))
APPEND_3_IN_GGA₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> APPEND_3_IN_GGA₃(L1, L2, L3)
IF_APPEND3_4_IN_1_GGGA₅(A, B, C, D, append_3_out_gga₃(A, B, E)) -> IF_APPEND3_4_IN_2_GGGA₆(A, B, C, D, E, append_3_in_gga₃(E, C, D))
IF_APPEND3_4_IN_1_GGGA₅(A, B, C, D, append_3_out_gga₃(A, B, E)) -> APPEND_3_IN_GGA₃(E, C, D)

The TRS R consists of the following rules:

append3_4_in_ggga₄(A, B, C, D) -> if_append3_4_in_1_ggga₅(A, B, C, D, append_3_in_gga₃(A, B, E))
append_3_in_gga₃([]_0, L, L) -> append_3_out_gga₃([]_0, L, L)
append_3_in_gga₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> if_append_3_in_1_gga₅(H, L1, L2, L3, append_3_in_gga₃(L1, L2, L3))
if_append_3_in_1_gga₅(H, L1, L2, L3, append_3_out_gga₃(L1, L2, L3)) -> append_3_out_gga₃(._2₂(H, L1), L2, ._2₂(H, L3))
if_append3_4_in_1_ggga₅(A, B, C, D, append_3_out_gga₃(A, B, E)) -> if_append3_4_in_2_ggga₆(A, B, C, D, E, append_3_in_gga₃(E, C, D))
if_append3_4_in_2_ggga₆(A, B, C, D, E, append_3_out_gga₃(E, C, D)) -> append3_4_out_ggga₄(A, B, C, D)

The argument filtering Pi contains the following mapping:
append3_4_in_ggga₄(x1, x2, x3, x4) = append3_4_in_ggga₃(x1, x2, x3)
[]_0 = []_0
._2₂(x1, x2) = ._2₂(x1, x2)
if_append3_4_in_1_ggga₅(x1, x2, x3, x4, x5) = if_append3_4_in_1_ggga₂(x3, x5)
append_3_in_gga₃(x1, x2, x3) = append_3_in_gga₂(x1, x2)
append_3_out_gga₃(x1, x2, x3) = append_3_out_gga₁(x3)
if_append_3_in_1_gga₅(x1, x2, x3, x4, x5) = if_append_3_in_1_gga₂(x1, x5)
if_append3_4_in_2_ggga₆(x1, x2, x3, x4, x5, x6) = if_append3_4_in_2_ggga₁(x6)
append3_4_out_ggga₄(x1, x2, x3, x4) = append3_4_out_ggga₁(x4)
IF_APPEND3_4_IN_2_GGGA₆(x1, x2, x3, x4, x5, x6) = IF_APPEND3_4_IN_2_GGGA₁(x6)
IF_APPEND_3_IN_1_GGA₅(x1, x2, x3, x4, x5) = IF_APPEND_3_IN_1_GGA₂(x1, x5)
IF_APPEND3_4_IN_1_GGGA₅(x1, x2, x3, x4, x5) = IF_APPEND3_4_IN_1_GGGA₂(x3, x5)
APPEND3_4_IN_GGGA₄(x1, x2, x3, x4) = APPEND3_4_IN_GGGA₃(x1, x2, x3)
APPEND_3_IN_GGA₃(x1, x2, x3) = APPEND_3_IN_GGA₂(x1, x2)

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:

APPEND3_4_IN_GGGA₄(A, B, C, D) -> IF_APPEND3_4_IN_1_GGGA₅(A, B, C, D, append_3_in_gga₃(A, B, E))
APPEND3_4_IN_GGGA₄(A, B, C, D) -> APPEND_3_IN_GGA₃(A, B, E)
APPEND_3_IN_GGA₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> IF_APPEND_3_IN_1_GGA₅(H, L1, L2, L3, append_3_in_gga₃(L1, L2, L3))
APPEND_3_IN_GGA₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> APPEND_3_IN_GGA₃(L1, L2, L3)
IF_APPEND3_4_IN_1_GGGA₅(A, B, C, D, append_3_out_gga₃(A, B, E)) -> IF_APPEND3_4_IN_2_GGGA₆(A, B, C, D, E, append_3_in_gga₃(E, C, D))
IF_APPEND3_4_IN_1_GGGA₅(A, B, C, D, append_3_out_gga₃(A, B, E)) -> APPEND_3_IN_GGA₃(E, C, D)

The TRS R consists of the following rules:

append3_4_in_ggga₄(A, B, C, D) -> if_append3_4_in_1_ggga₅(A, B, C, D, append_3_in_gga₃(A, B, E))
append_3_in_gga₃([]_0, L, L) -> append_3_out_gga₃([]_0, L, L)
append_3_in_gga₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> if_append_3_in_1_gga₅(H, L1, L2, L3, append_3_in_gga₃(L1, L2, L3))
if_append_3_in_1_gga₅(H, L1, L2, L3, append_3_out_gga₃(L1, L2, L3)) -> append_3_out_gga₃(._2₂(H, L1), L2, ._2₂(H, L3))
if_append3_4_in_1_ggga₅(A, B, C, D, append_3_out_gga₃(A, B, E)) -> if_append3_4_in_2_ggga₆(A, B, C, D, E, append_3_in_gga₃(E, C, D))
if_append3_4_in_2_ggga₆(A, B, C, D, E, append_3_out_gga₃(E, C, D)) -> append3_4_out_ggga₄(A, B, C, D)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

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

APPEND_3_IN_GGA₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> APPEND_3_IN_GGA₃(L1, L2, L3)

The TRS R consists of the following rules:

append3_4_in_ggga₄(A, B, C, D) -> if_append3_4_in_1_ggga₅(A, B, C, D, append_3_in_gga₃(A, B, E))
append_3_in_gga₃([]_0, L, L) -> append_3_out_gga₃([]_0, L, L)
append_3_in_gga₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> if_append_3_in_1_gga₅(H, L1, L2, L3, append_3_in_gga₃(L1, L2, L3))
if_append_3_in_1_gga₅(H, L1, L2, L3, append_3_out_gga₃(L1, L2, L3)) -> append_3_out_gga₃(._2₂(H, L1), L2, ._2₂(H, L3))
if_append3_4_in_1_ggga₅(A, B, C, D, append_3_out_gga₃(A, B, E)) -> if_append3_4_in_2_ggga₆(A, B, C, D, E, append_3_in_gga₃(E, C, D))
if_append3_4_in_2_ggga₆(A, B, C, D, E, append_3_out_gga₃(E, C, D)) -> append3_4_out_ggga₄(A, B, C, D)

The argument filtering Pi contains the following mapping:
append3_4_in_ggga₄(x1, x2, x3, x4) = append3_4_in_ggga₃(x1, x2, x3)
[]_0 = []_0
._2₂(x1, x2) = ._2₂(x1, x2)
if_append3_4_in_1_ggga₅(x1, x2, x3, x4, x5) = if_append3_4_in_1_ggga₂(x3, x5)
append_3_in_gga₃(x1, x2, x3) = append_3_in_gga₂(x1, x2)
append_3_out_gga₃(x1, x2, x3) = append_3_out_gga₁(x3)
if_append_3_in_1_gga₅(x1, x2, x3, x4, x5) = if_append_3_in_1_gga₂(x1, x5)
if_append3_4_in_2_ggga₆(x1, x2, x3, x4, x5, x6) = if_append3_4_in_2_ggga₁(x6)
append3_4_out_ggga₄(x1, x2, x3, x4) = append3_4_out_ggga₁(x4)
APPEND_3_IN_GGA₃(x1, x2, x3) = APPEND_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:

APPEND_3_IN_GGA₃(._2₂(H, L1), L2, ._2₂(H, L3)) -> APPEND_3_IN_GGA₃(L1, L2, L3)

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

APPEND_3_IN_GGA₂(._2₂(H, L1), L2) -> APPEND_3_IN_GGA₂(L1, L2)

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

APPEND_3_IN_GGA₂(._2₂(H, L1), L2) -> APPEND_3_IN_GGA₂(L1, L2)
The graph contains the following edges 1 > 1, 2 >= 2