Left Termination proof of /tmp/tmpAaDVtC/palindrome.pl

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

↳ PROLOG

  ↳ PrologToPiTRSProof

palindrome₁(Xs) :- reverse₂(Xs, Xs).
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:
palindrome₁: (b)
reverse₂: (b,b)
reverse₃: (b,b,b)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

palindrome_1_in_g₁(Xs) -> if_palindrome_1_in_1_g₂(Xs, reverse_2_in_gg₂(Xs, Xs))
reverse_2_in_gg₂(X1s, X2s) -> if_reverse_2_in_1_gg₃(X1s, X2s, reverse_3_in_ggg₃(X1s, []_0, X2s))
reverse_3_in_ggg₃([]_0, Xs, Xs) -> reverse_3_out_ggg₃([]_0, Xs, Xs)
reverse_3_in_ggg₃(._2₂(X, X1s), X2s, Ys) -> if_reverse_3_in_1_ggg₅(X, X1s, X2s, Ys, reverse_3_in_ggg₃(X1s, ._2₂(X, X2s), Ys))
if_reverse_3_in_1_ggg₅(X, X1s, X2s, Ys, reverse_3_out_ggg₃(X1s, ._2₂(X, X2s), Ys)) -> reverse_3_out_ggg₃(._2₂(X, X1s), X2s, Ys)
if_reverse_2_in_1_gg₃(X1s, X2s, reverse_3_out_ggg₃(X1s, []_0, X2s)) -> reverse_2_out_gg₂(X1s, X2s)
if_palindrome_1_in_1_g₂(Xs, reverse_2_out_gg₂(Xs, Xs)) -> palindrome_1_out_g₁(Xs)

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:

palindrome_1_in_g₁(Xs) -> if_palindrome_1_in_1_g₂(Xs, reverse_2_in_gg₂(Xs, Xs))
reverse_2_in_gg₂(X1s, X2s) -> if_reverse_2_in_1_gg₃(X1s, X2s, reverse_3_in_ggg₃(X1s, []_0, X2s))
reverse_3_in_ggg₃([]_0, Xs, Xs) -> reverse_3_out_ggg₃([]_0, Xs, Xs)
reverse_3_in_ggg₃(._2₂(X, X1s), X2s, Ys) -> if_reverse_3_in_1_ggg₅(X, X1s, X2s, Ys, reverse_3_in_ggg₃(X1s, ._2₂(X, X2s), Ys))
if_reverse_3_in_1_ggg₅(X, X1s, X2s, Ys, reverse_3_out_ggg₃(X1s, ._2₂(X, X2s), Ys)) -> reverse_3_out_ggg₃(._2₂(X, X1s), X2s, Ys)
if_reverse_2_in_1_gg₃(X1s, X2s, reverse_3_out_ggg₃(X1s, []_0, X2s)) -> reverse_2_out_gg₂(X1s, X2s)
if_palindrome_1_in_1_g₂(Xs, reverse_2_out_gg₂(Xs, Xs)) -> palindrome_1_out_g₁(Xs)

PALINDROME_1_IN_G₁(Xs) -> IF_PALINDROME_1_IN_1_G₂(Xs, reverse_2_in_gg₂(Xs, Xs))
PALINDROME_1_IN_G₁(Xs) -> REVERSE_2_IN_GG₂(Xs, Xs)
REVERSE_2_IN_GG₂(X1s, X2s) -> IF_REVERSE_2_IN_1_GG₃(X1s, X2s, reverse_3_in_ggg₃(X1s, []_0, X2s))
REVERSE_2_IN_GG₂(X1s, X2s) -> REVERSE_3_IN_GGG₃(X1s, []_0, X2s)
REVERSE_3_IN_GGG₃(._2₂(X, X1s), X2s, Ys) -> IF_REVERSE_3_IN_1_GGG₅(X, X1s, X2s, Ys, reverse_3_in_ggg₃(X1s, ._2₂(X, X2s), Ys))
REVERSE_3_IN_GGG₃(._2₂(X, X1s), X2s, Ys) -> REVERSE_3_IN_GGG₃(X1s, ._2₂(X, X2s), Ys)

The TRS R consists of the following rules:

palindrome_1_in_g₁(Xs) -> if_palindrome_1_in_1_g₂(Xs, reverse_2_in_gg₂(Xs, Xs))
reverse_2_in_gg₂(X1s, X2s) -> if_reverse_2_in_1_gg₃(X1s, X2s, reverse_3_in_ggg₃(X1s, []_0, X2s))
reverse_3_in_ggg₃([]_0, Xs, Xs) -> reverse_3_out_ggg₃([]_0, Xs, Xs)
reverse_3_in_ggg₃(._2₂(X, X1s), X2s, Ys) -> if_reverse_3_in_1_ggg₅(X, X1s, X2s, Ys, reverse_3_in_ggg₃(X1s, ._2₂(X, X2s), Ys))
if_reverse_3_in_1_ggg₅(X, X1s, X2s, Ys, reverse_3_out_ggg₃(X1s, ._2₂(X, X2s), Ys)) -> reverse_3_out_ggg₃(._2₂(X, X1s), X2s, Ys)
if_reverse_2_in_1_gg₃(X1s, X2s, reverse_3_out_ggg₃(X1s, []_0, X2s)) -> reverse_2_out_gg₂(X1s, X2s)
if_palindrome_1_in_1_g₂(Xs, reverse_2_out_gg₂(Xs, Xs)) -> palindrome_1_out_g₁(Xs)

The argument filtering Pi contains the following mapping:
palindrome_1_in_g₁(x1) = palindrome_1_in_g₁(x1)
[]_0 = []_0
._2₂(x1, x2) = ._2₂(x1, x2)
if_palindrome_1_in_1_g₂(x1, x2) = if_palindrome_1_in_1_g₁(x2)
reverse_2_in_gg₂(x1, x2) = reverse_2_in_gg₂(x1, x2)
if_reverse_2_in_1_gg₃(x1, x2, x3) = if_reverse_2_in_1_gg₁(x3)
reverse_3_in_ggg₃(x1, x2, x3) = reverse_3_in_ggg₃(x1, x2, x3)
reverse_3_out_ggg₃(x1, x2, x3) = reverse_3_out_ggg
if_reverse_3_in_1_ggg₅(x1, x2, x3, x4, x5) = if_reverse_3_in_1_ggg₁(x5)
reverse_2_out_gg₂(x1, x2) = reverse_2_out_gg
palindrome_1_out_g₁(x1) = palindrome_1_out_g
IF_PALINDROME_1_IN_1_G₂(x1, x2) = IF_PALINDROME_1_IN_1_G₁(x2)
REVERSE_2_IN_GG₂(x1, x2) = REVERSE_2_IN_GG₂(x1, x2)
REVERSE_3_IN_GGG₃(x1, x2, x3) = REVERSE_3_IN_GGG₃(x1, x2, x3)
IF_REVERSE_3_IN_1_GGG₅(x1, x2, x3, x4, x5) = IF_REVERSE_3_IN_1_GGG₁(x5)
IF_REVERSE_2_IN_1_GG₃(x1, x2, x3) = IF_REVERSE_2_IN_1_GG₁(x3)
PALINDROME_1_IN_G₁(x1) = PALINDROME_1_IN_G₁(x1)

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:

PALINDROME_1_IN_G₁(Xs) -> IF_PALINDROME_1_IN_1_G₂(Xs, reverse_2_in_gg₂(Xs, Xs))
PALINDROME_1_IN_G₁(Xs) -> REVERSE_2_IN_GG₂(Xs, Xs)
REVERSE_2_IN_GG₂(X1s, X2s) -> IF_REVERSE_2_IN_1_GG₃(X1s, X2s, reverse_3_in_ggg₃(X1s, []_0, X2s))
REVERSE_2_IN_GG₂(X1s, X2s) -> REVERSE_3_IN_GGG₃(X1s, []_0, X2s)
REVERSE_3_IN_GGG₃(._2₂(X, X1s), X2s, Ys) -> IF_REVERSE_3_IN_1_GGG₅(X, X1s, X2s, Ys, reverse_3_in_ggg₃(X1s, ._2₂(X, X2s), Ys))
REVERSE_3_IN_GGG₃(._2₂(X, X1s), X2s, Ys) -> REVERSE_3_IN_GGG₃(X1s, ._2₂(X, X2s), Ys)

The TRS R consists of the following rules:

palindrome_1_in_g₁(Xs) -> if_palindrome_1_in_1_g₂(Xs, reverse_2_in_gg₂(Xs, Xs))
reverse_2_in_gg₂(X1s, X2s) -> if_reverse_2_in_1_gg₃(X1s, X2s, reverse_3_in_ggg₃(X1s, []_0, X2s))
reverse_3_in_ggg₃([]_0, Xs, Xs) -> reverse_3_out_ggg₃([]_0, Xs, Xs)
reverse_3_in_ggg₃(._2₂(X, X1s), X2s, Ys) -> if_reverse_3_in_1_ggg₅(X, X1s, X2s, Ys, reverse_3_in_ggg₃(X1s, ._2₂(X, X2s), Ys))
if_reverse_3_in_1_ggg₅(X, X1s, X2s, Ys, reverse_3_out_ggg₃(X1s, ._2₂(X, X2s), Ys)) -> reverse_3_out_ggg₃(._2₂(X, X1s), X2s, Ys)
if_reverse_2_in_1_gg₃(X1s, X2s, reverse_3_out_ggg₃(X1s, []_0, X2s)) -> reverse_2_out_gg₂(X1s, X2s)
if_palindrome_1_in_1_g₂(Xs, reverse_2_out_gg₂(Xs, Xs)) -> palindrome_1_out_g₁(Xs)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

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

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

The TRS R consists of the following rules:

palindrome_1_in_g₁(Xs) -> if_palindrome_1_in_1_g₂(Xs, reverse_2_in_gg₂(Xs, Xs))
reverse_2_in_gg₂(X1s, X2s) -> if_reverse_2_in_1_gg₃(X1s, X2s, reverse_3_in_ggg₃(X1s, []_0, X2s))
reverse_3_in_ggg₃([]_0, Xs, Xs) -> reverse_3_out_ggg₃([]_0, Xs, Xs)
reverse_3_in_ggg₃(._2₂(X, X1s), X2s, Ys) -> if_reverse_3_in_1_ggg₅(X, X1s, X2s, Ys, reverse_3_in_ggg₃(X1s, ._2₂(X, X2s), Ys))
if_reverse_3_in_1_ggg₅(X, X1s, X2s, Ys, reverse_3_out_ggg₃(X1s, ._2₂(X, X2s), Ys)) -> reverse_3_out_ggg₃(._2₂(X, X1s), X2s, Ys)
if_reverse_2_in_1_gg₃(X1s, X2s, reverse_3_out_ggg₃(X1s, []_0, X2s)) -> reverse_2_out_gg₂(X1s, X2s)
if_palindrome_1_in_1_g₂(Xs, reverse_2_out_gg₂(Xs, Xs)) -> palindrome_1_out_g₁(Xs)

The argument filtering Pi contains the following mapping:
palindrome_1_in_g₁(x1) = palindrome_1_in_g₁(x1)
[]_0 = []_0
._2₂(x1, x2) = ._2₂(x1, x2)
if_palindrome_1_in_1_g₂(x1, x2) = if_palindrome_1_in_1_g₁(x2)
reverse_2_in_gg₂(x1, x2) = reverse_2_in_gg₂(x1, x2)
if_reverse_2_in_1_gg₃(x1, x2, x3) = if_reverse_2_in_1_gg₁(x3)
reverse_3_in_ggg₃(x1, x2, x3) = reverse_3_in_ggg₃(x1, x2, x3)
reverse_3_out_ggg₃(x1, x2, x3) = reverse_3_out_ggg
if_reverse_3_in_1_ggg₅(x1, x2, x3, x4, x5) = if_reverse_3_in_1_ggg₁(x5)
reverse_2_out_gg₂(x1, x2) = reverse_2_out_gg
palindrome_1_out_g₁(x1) = palindrome_1_out_g
REVERSE_3_IN_GGG₃(x1, x2, x3) = REVERSE_3_IN_GGG₃(x1, x2, 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

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ PiDP

              ↳ UsableRulesProof

                ↳ PiDP

                  ↳ PiDPToQDPProof

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

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

R is empty.
Pi is empty.
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:

REVERSE_3_IN_GGG₃(._2₂(X, X1s), X2s, Ys) -> REVERSE_3_IN_GGG₃(X1s, ._2₂(X, X2s), 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_GGG₃}.
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:

REVERSE_3_IN_GGG₃(._2₂(X, X1s), X2s, Ys) -> REVERSE_3_IN_GGG₃(X1s, ._2₂(X, X2s), Ys)
The graph contains the following edges 1 > 1, 3 >= 3