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



↳ PROLOG
  ↳ PrologToPiTRSProof

palindrome1(L) :- halves4(L, X1s, X2s, EvenOdd), eq2(EvenOdd, even0), eq2(X1s, X2s).
palindrome1(L) :- halves4(L, X1s, X2s, EvenOdd), eq2(EvenOdd, odd0), last3(X1s, underscore, X2s).
halves4({}0, {}0, {}0, even0).
halves4(.2(X, {}0), .2(X, {}0), {}0, odd0).
halves4(.2(T, .2(Y, Xs)), .2(T, Ts), .2(R, Rs), EvenOdd) :- last3(.2(Y, Xs), R, Rests), halves4(Rests, Ts, Rs, EvenOdd).
last3(.2(T, {}0), T, {}0).
last3(.2(H, T), X, .2(H, M)) :- last3(T, X, M).
eq2(X, X).


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


palindrome_1_in_g1(L) -> if_palindrome_1_in_1_g2(L, halves_4_in_gaaa4(L, X1s, X2s, EvenOdd))
halves_4_in_gaaa4([]_0, []_0, []_0, even_0) -> halves_4_out_gaaa4([]_0, []_0, []_0, even_0)
halves_4_in_gaaa4(._22(X, []_0), ._22(X, []_0), []_0, odd_0) -> halves_4_out_gaaa4(._22(X, []_0), ._22(X, []_0), []_0, odd_0)
halves_4_in_gaaa4(._22(T, ._22(Y, Xs)), ._22(T, Ts), ._22(R, Rs), EvenOdd) -> if_halves_4_in_1_gaaa8(T, Y, Xs, Ts, R, Rs, EvenOdd, last_3_in_gaa3(._22(Y, Xs), R, Rests))
last_3_in_gaa3(._22(T, []_0), T, []_0) -> last_3_out_gaa3(._22(T, []_0), T, []_0)
last_3_in_gaa3(._22(H, T), X, ._22(H, M)) -> if_last_3_in_1_gaa5(H, T, X, M, last_3_in_gaa3(T, X, M))
if_last_3_in_1_gaa5(H, T, X, M, last_3_out_gaa3(T, X, M)) -> last_3_out_gaa3(._22(H, T), X, ._22(H, M))
if_halves_4_in_1_gaaa8(T, Y, Xs, Ts, R, Rs, EvenOdd, last_3_out_gaa3(._22(Y, Xs), R, Rests)) -> if_halves_4_in_2_gaaa9(T, Y, Xs, Ts, R, Rs, EvenOdd, Rests, halves_4_in_gaaa4(Rests, Ts, Rs, EvenOdd))
if_halves_4_in_2_gaaa9(T, Y, Xs, Ts, R, Rs, EvenOdd, Rests, halves_4_out_gaaa4(Rests, Ts, Rs, EvenOdd)) -> halves_4_out_gaaa4(._22(T, ._22(Y, Xs)), ._22(T, Ts), ._22(R, Rs), EvenOdd)
if_palindrome_1_in_1_g2(L, halves_4_out_gaaa4(L, X1s, X2s, EvenOdd)) -> if_palindrome_1_in_2_g5(L, X1s, X2s, EvenOdd, eq_2_in_gg2(EvenOdd, even_0))
eq_2_in_gg2(X, X) -> eq_2_out_gg2(X, X)
if_palindrome_1_in_2_g5(L, X1s, X2s, EvenOdd, eq_2_out_gg2(EvenOdd, even_0)) -> if_palindrome_1_in_3_g4(L, X1s, X2s, eq_2_in_gg2(X1s, X2s))
if_palindrome_1_in_3_g4(L, X1s, X2s, eq_2_out_gg2(X1s, X2s)) -> palindrome_1_out_g1(L)
if_palindrome_1_in_1_g2(L, halves_4_out_gaaa4(L, X1s, X2s, EvenOdd)) -> if_palindrome_1_in_4_g5(L, X1s, X2s, EvenOdd, eq_2_in_gg2(EvenOdd, odd_0))
if_palindrome_1_in_4_g5(L, X1s, X2s, EvenOdd, eq_2_out_gg2(EvenOdd, odd_0)) -> if_palindrome_1_in_5_g4(L, X1s, X2s, last_3_in_gag3(X1s, underscore, X2s))
last_3_in_gag3(._22(T, []_0), T, []_0) -> last_3_out_gag3(._22(T, []_0), T, []_0)
last_3_in_gag3(._22(H, T), X, ._22(H, M)) -> if_last_3_in_1_gag5(H, T, X, M, last_3_in_gag3(T, X, M))
if_last_3_in_1_gag5(H, T, X, M, last_3_out_gag3(T, X, M)) -> last_3_out_gag3(._22(H, T), X, ._22(H, M))
if_palindrome_1_in_5_g4(L, X1s, X2s, last_3_out_gag3(X1s, underscore, X2s)) -> palindrome_1_out_g1(L)

The argument filtering Pi contains the following mapping:
palindrome_1_in_g1(x1)  =  palindrome_1_in_g1(x1)
even_0  =  even_0
odd_0  =  odd_0
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
if_palindrome_1_in_1_g2(x1, x2)  =  if_palindrome_1_in_1_g1(x2)
halves_4_in_gaaa4(x1, x2, x3, x4)  =  halves_4_in_gaaa1(x1)
halves_4_out_gaaa4(x1, x2, x3, x4)  =  halves_4_out_gaaa3(x2, x3, x4)
if_halves_4_in_1_gaaa8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_halves_4_in_1_gaaa2(x1, x8)
last_3_in_gaa3(x1, x2, x3)  =  last_3_in_gaa1(x1)
last_3_out_gaa3(x1, x2, x3)  =  last_3_out_gaa2(x2, x3)
if_last_3_in_1_gaa5(x1, x2, x3, x4, x5)  =  if_last_3_in_1_gaa2(x1, x5)
if_halves_4_in_2_gaaa9(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  if_halves_4_in_2_gaaa3(x1, x5, x9)
if_palindrome_1_in_2_g5(x1, x2, x3, x4, x5)  =  if_palindrome_1_in_2_g3(x2, x3, x5)
eq_2_in_gg2(x1, x2)  =  eq_2_in_gg2(x1, x2)
eq_2_out_gg2(x1, x2)  =  eq_2_out_gg
if_palindrome_1_in_3_g4(x1, x2, x3, x4)  =  if_palindrome_1_in_3_g1(x4)
palindrome_1_out_g1(x1)  =  palindrome_1_out_g
if_palindrome_1_in_4_g5(x1, x2, x3, x4, x5)  =  if_palindrome_1_in_4_g3(x2, x3, x5)
if_palindrome_1_in_5_g4(x1, x2, x3, x4)  =  if_palindrome_1_in_5_g1(x4)
last_3_in_gag3(x1, x2, x3)  =  last_3_in_gag2(x1, x3)
last_3_out_gag3(x1, x2, x3)  =  last_3_out_gag1(x2)
if_last_3_in_1_gag5(x1, x2, x3, x4, x5)  =  if_last_3_in_1_gag1(x5)

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_g1(L) -> if_palindrome_1_in_1_g2(L, halves_4_in_gaaa4(L, X1s, X2s, EvenOdd))
halves_4_in_gaaa4([]_0, []_0, []_0, even_0) -> halves_4_out_gaaa4([]_0, []_0, []_0, even_0)
halves_4_in_gaaa4(._22(X, []_0), ._22(X, []_0), []_0, odd_0) -> halves_4_out_gaaa4(._22(X, []_0), ._22(X, []_0), []_0, odd_0)
halves_4_in_gaaa4(._22(T, ._22(Y, Xs)), ._22(T, Ts), ._22(R, Rs), EvenOdd) -> if_halves_4_in_1_gaaa8(T, Y, Xs, Ts, R, Rs, EvenOdd, last_3_in_gaa3(._22(Y, Xs), R, Rests))
last_3_in_gaa3(._22(T, []_0), T, []_0) -> last_3_out_gaa3(._22(T, []_0), T, []_0)
last_3_in_gaa3(._22(H, T), X, ._22(H, M)) -> if_last_3_in_1_gaa5(H, T, X, M, last_3_in_gaa3(T, X, M))
if_last_3_in_1_gaa5(H, T, X, M, last_3_out_gaa3(T, X, M)) -> last_3_out_gaa3(._22(H, T), X, ._22(H, M))
if_halves_4_in_1_gaaa8(T, Y, Xs, Ts, R, Rs, EvenOdd, last_3_out_gaa3(._22(Y, Xs), R, Rests)) -> if_halves_4_in_2_gaaa9(T, Y, Xs, Ts, R, Rs, EvenOdd, Rests, halves_4_in_gaaa4(Rests, Ts, Rs, EvenOdd))
if_halves_4_in_2_gaaa9(T, Y, Xs, Ts, R, Rs, EvenOdd, Rests, halves_4_out_gaaa4(Rests, Ts, Rs, EvenOdd)) -> halves_4_out_gaaa4(._22(T, ._22(Y, Xs)), ._22(T, Ts), ._22(R, Rs), EvenOdd)
if_palindrome_1_in_1_g2(L, halves_4_out_gaaa4(L, X1s, X2s, EvenOdd)) -> if_palindrome_1_in_2_g5(L, X1s, X2s, EvenOdd, eq_2_in_gg2(EvenOdd, even_0))
eq_2_in_gg2(X, X) -> eq_2_out_gg2(X, X)
if_palindrome_1_in_2_g5(L, X1s, X2s, EvenOdd, eq_2_out_gg2(EvenOdd, even_0)) -> if_palindrome_1_in_3_g4(L, X1s, X2s, eq_2_in_gg2(X1s, X2s))
if_palindrome_1_in_3_g4(L, X1s, X2s, eq_2_out_gg2(X1s, X2s)) -> palindrome_1_out_g1(L)
if_palindrome_1_in_1_g2(L, halves_4_out_gaaa4(L, X1s, X2s, EvenOdd)) -> if_palindrome_1_in_4_g5(L, X1s, X2s, EvenOdd, eq_2_in_gg2(EvenOdd, odd_0))
if_palindrome_1_in_4_g5(L, X1s, X2s, EvenOdd, eq_2_out_gg2(EvenOdd, odd_0)) -> if_palindrome_1_in_5_g4(L, X1s, X2s, last_3_in_gag3(X1s, underscore, X2s))
last_3_in_gag3(._22(T, []_0), T, []_0) -> last_3_out_gag3(._22(T, []_0), T, []_0)
last_3_in_gag3(._22(H, T), X, ._22(H, M)) -> if_last_3_in_1_gag5(H, T, X, M, last_3_in_gag3(T, X, M))
if_last_3_in_1_gag5(H, T, X, M, last_3_out_gag3(T, X, M)) -> last_3_out_gag3(._22(H, T), X, ._22(H, M))
if_palindrome_1_in_5_g4(L, X1s, X2s, last_3_out_gag3(X1s, underscore, X2s)) -> palindrome_1_out_g1(L)

The argument filtering Pi contains the following mapping:
palindrome_1_in_g1(x1)  =  palindrome_1_in_g1(x1)
even_0  =  even_0
odd_0  =  odd_0
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
if_palindrome_1_in_1_g2(x1, x2)  =  if_palindrome_1_in_1_g1(x2)
halves_4_in_gaaa4(x1, x2, x3, x4)  =  halves_4_in_gaaa1(x1)
halves_4_out_gaaa4(x1, x2, x3, x4)  =  halves_4_out_gaaa3(x2, x3, x4)
if_halves_4_in_1_gaaa8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_halves_4_in_1_gaaa2(x1, x8)
last_3_in_gaa3(x1, x2, x3)  =  last_3_in_gaa1(x1)
last_3_out_gaa3(x1, x2, x3)  =  last_3_out_gaa2(x2, x3)
if_last_3_in_1_gaa5(x1, x2, x3, x4, x5)  =  if_last_3_in_1_gaa2(x1, x5)
if_halves_4_in_2_gaaa9(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  if_halves_4_in_2_gaaa3(x1, x5, x9)
if_palindrome_1_in_2_g5(x1, x2, x3, x4, x5)  =  if_palindrome_1_in_2_g3(x2, x3, x5)
eq_2_in_gg2(x1, x2)  =  eq_2_in_gg2(x1, x2)
eq_2_out_gg2(x1, x2)  =  eq_2_out_gg
if_palindrome_1_in_3_g4(x1, x2, x3, x4)  =  if_palindrome_1_in_3_g1(x4)
palindrome_1_out_g1(x1)  =  palindrome_1_out_g
if_palindrome_1_in_4_g5(x1, x2, x3, x4, x5)  =  if_palindrome_1_in_4_g3(x2, x3, x5)
if_palindrome_1_in_5_g4(x1, x2, x3, x4)  =  if_palindrome_1_in_5_g1(x4)
last_3_in_gag3(x1, x2, x3)  =  last_3_in_gag2(x1, x3)
last_3_out_gag3(x1, x2, x3)  =  last_3_out_gag1(x2)
if_last_3_in_1_gag5(x1, x2, x3, x4, x5)  =  if_last_3_in_1_gag1(x5)


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

PALINDROME_1_IN_G1(L) -> IF_PALINDROME_1_IN_1_G2(L, halves_4_in_gaaa4(L, X1s, X2s, EvenOdd))
PALINDROME_1_IN_G1(L) -> HALVES_4_IN_GAAA4(L, X1s, X2s, EvenOdd)
HALVES_4_IN_GAAA4(._22(T, ._22(Y, Xs)), ._22(T, Ts), ._22(R, Rs), EvenOdd) -> IF_HALVES_4_IN_1_GAAA8(T, Y, Xs, Ts, R, Rs, EvenOdd, last_3_in_gaa3(._22(Y, Xs), R, Rests))
HALVES_4_IN_GAAA4(._22(T, ._22(Y, Xs)), ._22(T, Ts), ._22(R, Rs), EvenOdd) -> LAST_3_IN_GAA3(._22(Y, Xs), R, Rests)
LAST_3_IN_GAA3(._22(H, T), X, ._22(H, M)) -> IF_LAST_3_IN_1_GAA5(H, T, X, M, last_3_in_gaa3(T, X, M))
LAST_3_IN_GAA3(._22(H, T), X, ._22(H, M)) -> LAST_3_IN_GAA3(T, X, M)
IF_HALVES_4_IN_1_GAAA8(T, Y, Xs, Ts, R, Rs, EvenOdd, last_3_out_gaa3(._22(Y, Xs), R, Rests)) -> IF_HALVES_4_IN_2_GAAA9(T, Y, Xs, Ts, R, Rs, EvenOdd, Rests, halves_4_in_gaaa4(Rests, Ts, Rs, EvenOdd))
IF_HALVES_4_IN_1_GAAA8(T, Y, Xs, Ts, R, Rs, EvenOdd, last_3_out_gaa3(._22(Y, Xs), R, Rests)) -> HALVES_4_IN_GAAA4(Rests, Ts, Rs, EvenOdd)
IF_PALINDROME_1_IN_1_G2(L, halves_4_out_gaaa4(L, X1s, X2s, EvenOdd)) -> IF_PALINDROME_1_IN_2_G5(L, X1s, X2s, EvenOdd, eq_2_in_gg2(EvenOdd, even_0))
IF_PALINDROME_1_IN_1_G2(L, halves_4_out_gaaa4(L, X1s, X2s, EvenOdd)) -> EQ_2_IN_GG2(EvenOdd, even_0)
IF_PALINDROME_1_IN_2_G5(L, X1s, X2s, EvenOdd, eq_2_out_gg2(EvenOdd, even_0)) -> IF_PALINDROME_1_IN_3_G4(L, X1s, X2s, eq_2_in_gg2(X1s, X2s))
IF_PALINDROME_1_IN_2_G5(L, X1s, X2s, EvenOdd, eq_2_out_gg2(EvenOdd, even_0)) -> EQ_2_IN_GG2(X1s, X2s)
IF_PALINDROME_1_IN_1_G2(L, halves_4_out_gaaa4(L, X1s, X2s, EvenOdd)) -> IF_PALINDROME_1_IN_4_G5(L, X1s, X2s, EvenOdd, eq_2_in_gg2(EvenOdd, odd_0))
IF_PALINDROME_1_IN_1_G2(L, halves_4_out_gaaa4(L, X1s, X2s, EvenOdd)) -> EQ_2_IN_GG2(EvenOdd, odd_0)
IF_PALINDROME_1_IN_4_G5(L, X1s, X2s, EvenOdd, eq_2_out_gg2(EvenOdd, odd_0)) -> IF_PALINDROME_1_IN_5_G4(L, X1s, X2s, last_3_in_gag3(X1s, underscore, X2s))
IF_PALINDROME_1_IN_4_G5(L, X1s, X2s, EvenOdd, eq_2_out_gg2(EvenOdd, odd_0)) -> LAST_3_IN_GAG3(X1s, underscore, X2s)
LAST_3_IN_GAG3(._22(H, T), X, ._22(H, M)) -> IF_LAST_3_IN_1_GAG5(H, T, X, M, last_3_in_gag3(T, X, M))
LAST_3_IN_GAG3(._22(H, T), X, ._22(H, M)) -> LAST_3_IN_GAG3(T, X, M)

The TRS R consists of the following rules:

palindrome_1_in_g1(L) -> if_palindrome_1_in_1_g2(L, halves_4_in_gaaa4(L, X1s, X2s, EvenOdd))
halves_4_in_gaaa4([]_0, []_0, []_0, even_0) -> halves_4_out_gaaa4([]_0, []_0, []_0, even_0)
halves_4_in_gaaa4(._22(X, []_0), ._22(X, []_0), []_0, odd_0) -> halves_4_out_gaaa4(._22(X, []_0), ._22(X, []_0), []_0, odd_0)
halves_4_in_gaaa4(._22(T, ._22(Y, Xs)), ._22(T, Ts), ._22(R, Rs), EvenOdd) -> if_halves_4_in_1_gaaa8(T, Y, Xs, Ts, R, Rs, EvenOdd, last_3_in_gaa3(._22(Y, Xs), R, Rests))
last_3_in_gaa3(._22(T, []_0), T, []_0) -> last_3_out_gaa3(._22(T, []_0), T, []_0)
last_3_in_gaa3(._22(H, T), X, ._22(H, M)) -> if_last_3_in_1_gaa5(H, T, X, M, last_3_in_gaa3(T, X, M))
if_last_3_in_1_gaa5(H, T, X, M, last_3_out_gaa3(T, X, M)) -> last_3_out_gaa3(._22(H, T), X, ._22(H, M))
if_halves_4_in_1_gaaa8(T, Y, Xs, Ts, R, Rs, EvenOdd, last_3_out_gaa3(._22(Y, Xs), R, Rests)) -> if_halves_4_in_2_gaaa9(T, Y, Xs, Ts, R, Rs, EvenOdd, Rests, halves_4_in_gaaa4(Rests, Ts, Rs, EvenOdd))
if_halves_4_in_2_gaaa9(T, Y, Xs, Ts, R, Rs, EvenOdd, Rests, halves_4_out_gaaa4(Rests, Ts, Rs, EvenOdd)) -> halves_4_out_gaaa4(._22(T, ._22(Y, Xs)), ._22(T, Ts), ._22(R, Rs), EvenOdd)
if_palindrome_1_in_1_g2(L, halves_4_out_gaaa4(L, X1s, X2s, EvenOdd)) -> if_palindrome_1_in_2_g5(L, X1s, X2s, EvenOdd, eq_2_in_gg2(EvenOdd, even_0))
eq_2_in_gg2(X, X) -> eq_2_out_gg2(X, X)
if_palindrome_1_in_2_g5(L, X1s, X2s, EvenOdd, eq_2_out_gg2(EvenOdd, even_0)) -> if_palindrome_1_in_3_g4(L, X1s, X2s, eq_2_in_gg2(X1s, X2s))
if_palindrome_1_in_3_g4(L, X1s, X2s, eq_2_out_gg2(X1s, X2s)) -> palindrome_1_out_g1(L)
if_palindrome_1_in_1_g2(L, halves_4_out_gaaa4(L, X1s, X2s, EvenOdd)) -> if_palindrome_1_in_4_g5(L, X1s, X2s, EvenOdd, eq_2_in_gg2(EvenOdd, odd_0))
if_palindrome_1_in_4_g5(L, X1s, X2s, EvenOdd, eq_2_out_gg2(EvenOdd, odd_0)) -> if_palindrome_1_in_5_g4(L, X1s, X2s, last_3_in_gag3(X1s, underscore, X2s))
last_3_in_gag3(._22(T, []_0), T, []_0) -> last_3_out_gag3(._22(T, []_0), T, []_0)
last_3_in_gag3(._22(H, T), X, ._22(H, M)) -> if_last_3_in_1_gag5(H, T, X, M, last_3_in_gag3(T, X, M))
if_last_3_in_1_gag5(H, T, X, M, last_3_out_gag3(T, X, M)) -> last_3_out_gag3(._22(H, T), X, ._22(H, M))
if_palindrome_1_in_5_g4(L, X1s, X2s, last_3_out_gag3(X1s, underscore, X2s)) -> palindrome_1_out_g1(L)

The argument filtering Pi contains the following mapping:
palindrome_1_in_g1(x1)  =  palindrome_1_in_g1(x1)
even_0  =  even_0
odd_0  =  odd_0
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
if_palindrome_1_in_1_g2(x1, x2)  =  if_palindrome_1_in_1_g1(x2)
halves_4_in_gaaa4(x1, x2, x3, x4)  =  halves_4_in_gaaa1(x1)
halves_4_out_gaaa4(x1, x2, x3, x4)  =  halves_4_out_gaaa3(x2, x3, x4)
if_halves_4_in_1_gaaa8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_halves_4_in_1_gaaa2(x1, x8)
last_3_in_gaa3(x1, x2, x3)  =  last_3_in_gaa1(x1)
last_3_out_gaa3(x1, x2, x3)  =  last_3_out_gaa2(x2, x3)
if_last_3_in_1_gaa5(x1, x2, x3, x4, x5)  =  if_last_3_in_1_gaa2(x1, x5)
if_halves_4_in_2_gaaa9(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  if_halves_4_in_2_gaaa3(x1, x5, x9)
if_palindrome_1_in_2_g5(x1, x2, x3, x4, x5)  =  if_palindrome_1_in_2_g3(x2, x3, x5)
eq_2_in_gg2(x1, x2)  =  eq_2_in_gg2(x1, x2)
eq_2_out_gg2(x1, x2)  =  eq_2_out_gg
if_palindrome_1_in_3_g4(x1, x2, x3, x4)  =  if_palindrome_1_in_3_g1(x4)
palindrome_1_out_g1(x1)  =  palindrome_1_out_g
if_palindrome_1_in_4_g5(x1, x2, x3, x4, x5)  =  if_palindrome_1_in_4_g3(x2, x3, x5)
if_palindrome_1_in_5_g4(x1, x2, x3, x4)  =  if_palindrome_1_in_5_g1(x4)
last_3_in_gag3(x1, x2, x3)  =  last_3_in_gag2(x1, x3)
last_3_out_gag3(x1, x2, x3)  =  last_3_out_gag1(x2)
if_last_3_in_1_gag5(x1, x2, x3, x4, x5)  =  if_last_3_in_1_gag1(x5)
IF_PALINDROME_1_IN_1_G2(x1, x2)  =  IF_PALINDROME_1_IN_1_G1(x2)
LAST_3_IN_GAA3(x1, x2, x3)  =  LAST_3_IN_GAA1(x1)
IF_PALINDROME_1_IN_3_G4(x1, x2, x3, x4)  =  IF_PALINDROME_1_IN_3_G1(x4)
IF_LAST_3_IN_1_GAG5(x1, x2, x3, x4, x5)  =  IF_LAST_3_IN_1_GAG1(x5)
EQ_2_IN_GG2(x1, x2)  =  EQ_2_IN_GG2(x1, x2)
IF_PALINDROME_1_IN_4_G5(x1, x2, x3, x4, x5)  =  IF_PALINDROME_1_IN_4_G3(x2, x3, x5)
IF_LAST_3_IN_1_GAA5(x1, x2, x3, x4, x5)  =  IF_LAST_3_IN_1_GAA2(x1, x5)
LAST_3_IN_GAG3(x1, x2, x3)  =  LAST_3_IN_GAG2(x1, x3)
IF_PALINDROME_1_IN_5_G4(x1, x2, x3, x4)  =  IF_PALINDROME_1_IN_5_G1(x4)
HALVES_4_IN_GAAA4(x1, x2, x3, x4)  =  HALVES_4_IN_GAAA1(x1)
IF_PALINDROME_1_IN_2_G5(x1, x2, x3, x4, x5)  =  IF_PALINDROME_1_IN_2_G3(x2, x3, x5)
IF_HALVES_4_IN_2_GAAA9(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  IF_HALVES_4_IN_2_GAAA3(x1, x5, x9)
IF_HALVES_4_IN_1_GAAA8(x1, x2, x3, x4, x5, x6, x7, x8)  =  IF_HALVES_4_IN_1_GAAA2(x1, x8)
PALINDROME_1_IN_G1(x1)  =  PALINDROME_1_IN_G1(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_G1(L) -> IF_PALINDROME_1_IN_1_G2(L, halves_4_in_gaaa4(L, X1s, X2s, EvenOdd))
PALINDROME_1_IN_G1(L) -> HALVES_4_IN_GAAA4(L, X1s, X2s, EvenOdd)
HALVES_4_IN_GAAA4(._22(T, ._22(Y, Xs)), ._22(T, Ts), ._22(R, Rs), EvenOdd) -> IF_HALVES_4_IN_1_GAAA8(T, Y, Xs, Ts, R, Rs, EvenOdd, last_3_in_gaa3(._22(Y, Xs), R, Rests))
HALVES_4_IN_GAAA4(._22(T, ._22(Y, Xs)), ._22(T, Ts), ._22(R, Rs), EvenOdd) -> LAST_3_IN_GAA3(._22(Y, Xs), R, Rests)
LAST_3_IN_GAA3(._22(H, T), X, ._22(H, M)) -> IF_LAST_3_IN_1_GAA5(H, T, X, M, last_3_in_gaa3(T, X, M))
LAST_3_IN_GAA3(._22(H, T), X, ._22(H, M)) -> LAST_3_IN_GAA3(T, X, M)
IF_HALVES_4_IN_1_GAAA8(T, Y, Xs, Ts, R, Rs, EvenOdd, last_3_out_gaa3(._22(Y, Xs), R, Rests)) -> IF_HALVES_4_IN_2_GAAA9(T, Y, Xs, Ts, R, Rs, EvenOdd, Rests, halves_4_in_gaaa4(Rests, Ts, Rs, EvenOdd))
IF_HALVES_4_IN_1_GAAA8(T, Y, Xs, Ts, R, Rs, EvenOdd, last_3_out_gaa3(._22(Y, Xs), R, Rests)) -> HALVES_4_IN_GAAA4(Rests, Ts, Rs, EvenOdd)
IF_PALINDROME_1_IN_1_G2(L, halves_4_out_gaaa4(L, X1s, X2s, EvenOdd)) -> IF_PALINDROME_1_IN_2_G5(L, X1s, X2s, EvenOdd, eq_2_in_gg2(EvenOdd, even_0))
IF_PALINDROME_1_IN_1_G2(L, halves_4_out_gaaa4(L, X1s, X2s, EvenOdd)) -> EQ_2_IN_GG2(EvenOdd, even_0)
IF_PALINDROME_1_IN_2_G5(L, X1s, X2s, EvenOdd, eq_2_out_gg2(EvenOdd, even_0)) -> IF_PALINDROME_1_IN_3_G4(L, X1s, X2s, eq_2_in_gg2(X1s, X2s))
IF_PALINDROME_1_IN_2_G5(L, X1s, X2s, EvenOdd, eq_2_out_gg2(EvenOdd, even_0)) -> EQ_2_IN_GG2(X1s, X2s)
IF_PALINDROME_1_IN_1_G2(L, halves_4_out_gaaa4(L, X1s, X2s, EvenOdd)) -> IF_PALINDROME_1_IN_4_G5(L, X1s, X2s, EvenOdd, eq_2_in_gg2(EvenOdd, odd_0))
IF_PALINDROME_1_IN_1_G2(L, halves_4_out_gaaa4(L, X1s, X2s, EvenOdd)) -> EQ_2_IN_GG2(EvenOdd, odd_0)
IF_PALINDROME_1_IN_4_G5(L, X1s, X2s, EvenOdd, eq_2_out_gg2(EvenOdd, odd_0)) -> IF_PALINDROME_1_IN_5_G4(L, X1s, X2s, last_3_in_gag3(X1s, underscore, X2s))
IF_PALINDROME_1_IN_4_G5(L, X1s, X2s, EvenOdd, eq_2_out_gg2(EvenOdd, odd_0)) -> LAST_3_IN_GAG3(X1s, underscore, X2s)
LAST_3_IN_GAG3(._22(H, T), X, ._22(H, M)) -> IF_LAST_3_IN_1_GAG5(H, T, X, M, last_3_in_gag3(T, X, M))
LAST_3_IN_GAG3(._22(H, T), X, ._22(H, M)) -> LAST_3_IN_GAG3(T, X, M)

The TRS R consists of the following rules:

palindrome_1_in_g1(L) -> if_palindrome_1_in_1_g2(L, halves_4_in_gaaa4(L, X1s, X2s, EvenOdd))
halves_4_in_gaaa4([]_0, []_0, []_0, even_0) -> halves_4_out_gaaa4([]_0, []_0, []_0, even_0)
halves_4_in_gaaa4(._22(X, []_0), ._22(X, []_0), []_0, odd_0) -> halves_4_out_gaaa4(._22(X, []_0), ._22(X, []_0), []_0, odd_0)
halves_4_in_gaaa4(._22(T, ._22(Y, Xs)), ._22(T, Ts), ._22(R, Rs), EvenOdd) -> if_halves_4_in_1_gaaa8(T, Y, Xs, Ts, R, Rs, EvenOdd, last_3_in_gaa3(._22(Y, Xs), R, Rests))
last_3_in_gaa3(._22(T, []_0), T, []_0) -> last_3_out_gaa3(._22(T, []_0), T, []_0)
last_3_in_gaa3(._22(H, T), X, ._22(H, M)) -> if_last_3_in_1_gaa5(H, T, X, M, last_3_in_gaa3(T, X, M))
if_last_3_in_1_gaa5(H, T, X, M, last_3_out_gaa3(T, X, M)) -> last_3_out_gaa3(._22(H, T), X, ._22(H, M))
if_halves_4_in_1_gaaa8(T, Y, Xs, Ts, R, Rs, EvenOdd, last_3_out_gaa3(._22(Y, Xs), R, Rests)) -> if_halves_4_in_2_gaaa9(T, Y, Xs, Ts, R, Rs, EvenOdd, Rests, halves_4_in_gaaa4(Rests, Ts, Rs, EvenOdd))
if_halves_4_in_2_gaaa9(T, Y, Xs, Ts, R, Rs, EvenOdd, Rests, halves_4_out_gaaa4(Rests, Ts, Rs, EvenOdd)) -> halves_4_out_gaaa4(._22(T, ._22(Y, Xs)), ._22(T, Ts), ._22(R, Rs), EvenOdd)
if_palindrome_1_in_1_g2(L, halves_4_out_gaaa4(L, X1s, X2s, EvenOdd)) -> if_palindrome_1_in_2_g5(L, X1s, X2s, EvenOdd, eq_2_in_gg2(EvenOdd, even_0))
eq_2_in_gg2(X, X) -> eq_2_out_gg2(X, X)
if_palindrome_1_in_2_g5(L, X1s, X2s, EvenOdd, eq_2_out_gg2(EvenOdd, even_0)) -> if_palindrome_1_in_3_g4(L, X1s, X2s, eq_2_in_gg2(X1s, X2s))
if_palindrome_1_in_3_g4(L, X1s, X2s, eq_2_out_gg2(X1s, X2s)) -> palindrome_1_out_g1(L)
if_palindrome_1_in_1_g2(L, halves_4_out_gaaa4(L, X1s, X2s, EvenOdd)) -> if_palindrome_1_in_4_g5(L, X1s, X2s, EvenOdd, eq_2_in_gg2(EvenOdd, odd_0))
if_palindrome_1_in_4_g5(L, X1s, X2s, EvenOdd, eq_2_out_gg2(EvenOdd, odd_0)) -> if_palindrome_1_in_5_g4(L, X1s, X2s, last_3_in_gag3(X1s, underscore, X2s))
last_3_in_gag3(._22(T, []_0), T, []_0) -> last_3_out_gag3(._22(T, []_0), T, []_0)
last_3_in_gag3(._22(H, T), X, ._22(H, M)) -> if_last_3_in_1_gag5(H, T, X, M, last_3_in_gag3(T, X, M))
if_last_3_in_1_gag5(H, T, X, M, last_3_out_gag3(T, X, M)) -> last_3_out_gag3(._22(H, T), X, ._22(H, M))
if_palindrome_1_in_5_g4(L, X1s, X2s, last_3_out_gag3(X1s, underscore, X2s)) -> palindrome_1_out_g1(L)

The argument filtering Pi contains the following mapping:
palindrome_1_in_g1(x1)  =  palindrome_1_in_g1(x1)
even_0  =  even_0
odd_0  =  odd_0
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
if_palindrome_1_in_1_g2(x1, x2)  =  if_palindrome_1_in_1_g1(x2)
halves_4_in_gaaa4(x1, x2, x3, x4)  =  halves_4_in_gaaa1(x1)
halves_4_out_gaaa4(x1, x2, x3, x4)  =  halves_4_out_gaaa3(x2, x3, x4)
if_halves_4_in_1_gaaa8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_halves_4_in_1_gaaa2(x1, x8)
last_3_in_gaa3(x1, x2, x3)  =  last_3_in_gaa1(x1)
last_3_out_gaa3(x1, x2, x3)  =  last_3_out_gaa2(x2, x3)
if_last_3_in_1_gaa5(x1, x2, x3, x4, x5)  =  if_last_3_in_1_gaa2(x1, x5)
if_halves_4_in_2_gaaa9(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  if_halves_4_in_2_gaaa3(x1, x5, x9)
if_palindrome_1_in_2_g5(x1, x2, x3, x4, x5)  =  if_palindrome_1_in_2_g3(x2, x3, x5)
eq_2_in_gg2(x1, x2)  =  eq_2_in_gg2(x1, x2)
eq_2_out_gg2(x1, x2)  =  eq_2_out_gg
if_palindrome_1_in_3_g4(x1, x2, x3, x4)  =  if_palindrome_1_in_3_g1(x4)
palindrome_1_out_g1(x1)  =  palindrome_1_out_g
if_palindrome_1_in_4_g5(x1, x2, x3, x4, x5)  =  if_palindrome_1_in_4_g3(x2, x3, x5)
if_palindrome_1_in_5_g4(x1, x2, x3, x4)  =  if_palindrome_1_in_5_g1(x4)
last_3_in_gag3(x1, x2, x3)  =  last_3_in_gag2(x1, x3)
last_3_out_gag3(x1, x2, x3)  =  last_3_out_gag1(x2)
if_last_3_in_1_gag5(x1, x2, x3, x4, x5)  =  if_last_3_in_1_gag1(x5)
IF_PALINDROME_1_IN_1_G2(x1, x2)  =  IF_PALINDROME_1_IN_1_G1(x2)
LAST_3_IN_GAA3(x1, x2, x3)  =  LAST_3_IN_GAA1(x1)
IF_PALINDROME_1_IN_3_G4(x1, x2, x3, x4)  =  IF_PALINDROME_1_IN_3_G1(x4)
IF_LAST_3_IN_1_GAG5(x1, x2, x3, x4, x5)  =  IF_LAST_3_IN_1_GAG1(x5)
EQ_2_IN_GG2(x1, x2)  =  EQ_2_IN_GG2(x1, x2)
IF_PALINDROME_1_IN_4_G5(x1, x2, x3, x4, x5)  =  IF_PALINDROME_1_IN_4_G3(x2, x3, x5)
IF_LAST_3_IN_1_GAA5(x1, x2, x3, x4, x5)  =  IF_LAST_3_IN_1_GAA2(x1, x5)
LAST_3_IN_GAG3(x1, x2, x3)  =  LAST_3_IN_GAG2(x1, x3)
IF_PALINDROME_1_IN_5_G4(x1, x2, x3, x4)  =  IF_PALINDROME_1_IN_5_G1(x4)
HALVES_4_IN_GAAA4(x1, x2, x3, x4)  =  HALVES_4_IN_GAAA1(x1)
IF_PALINDROME_1_IN_2_G5(x1, x2, x3, x4, x5)  =  IF_PALINDROME_1_IN_2_G3(x2, x3, x5)
IF_HALVES_4_IN_2_GAAA9(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  IF_HALVES_4_IN_2_GAAA3(x1, x5, x9)
IF_HALVES_4_IN_1_GAAA8(x1, x2, x3, x4, x5, x6, x7, x8)  =  IF_HALVES_4_IN_1_GAAA2(x1, x8)
PALINDROME_1_IN_G1(x1)  =  PALINDROME_1_IN_G1(x1)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph contains 3 SCCs with 14 less nodes.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP

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

LAST_3_IN_GAG3(._22(H, T), X, ._22(H, M)) -> LAST_3_IN_GAG3(T, X, M)

The TRS R consists of the following rules:

palindrome_1_in_g1(L) -> if_palindrome_1_in_1_g2(L, halves_4_in_gaaa4(L, X1s, X2s, EvenOdd))
halves_4_in_gaaa4([]_0, []_0, []_0, even_0) -> halves_4_out_gaaa4([]_0, []_0, []_0, even_0)
halves_4_in_gaaa4(._22(X, []_0), ._22(X, []_0), []_0, odd_0) -> halves_4_out_gaaa4(._22(X, []_0), ._22(X, []_0), []_0, odd_0)
halves_4_in_gaaa4(._22(T, ._22(Y, Xs)), ._22(T, Ts), ._22(R, Rs), EvenOdd) -> if_halves_4_in_1_gaaa8(T, Y, Xs, Ts, R, Rs, EvenOdd, last_3_in_gaa3(._22(Y, Xs), R, Rests))
last_3_in_gaa3(._22(T, []_0), T, []_0) -> last_3_out_gaa3(._22(T, []_0), T, []_0)
last_3_in_gaa3(._22(H, T), X, ._22(H, M)) -> if_last_3_in_1_gaa5(H, T, X, M, last_3_in_gaa3(T, X, M))
if_last_3_in_1_gaa5(H, T, X, M, last_3_out_gaa3(T, X, M)) -> last_3_out_gaa3(._22(H, T), X, ._22(H, M))
if_halves_4_in_1_gaaa8(T, Y, Xs, Ts, R, Rs, EvenOdd, last_3_out_gaa3(._22(Y, Xs), R, Rests)) -> if_halves_4_in_2_gaaa9(T, Y, Xs, Ts, R, Rs, EvenOdd, Rests, halves_4_in_gaaa4(Rests, Ts, Rs, EvenOdd))
if_halves_4_in_2_gaaa9(T, Y, Xs, Ts, R, Rs, EvenOdd, Rests, halves_4_out_gaaa4(Rests, Ts, Rs, EvenOdd)) -> halves_4_out_gaaa4(._22(T, ._22(Y, Xs)), ._22(T, Ts), ._22(R, Rs), EvenOdd)
if_palindrome_1_in_1_g2(L, halves_4_out_gaaa4(L, X1s, X2s, EvenOdd)) -> if_palindrome_1_in_2_g5(L, X1s, X2s, EvenOdd, eq_2_in_gg2(EvenOdd, even_0))
eq_2_in_gg2(X, X) -> eq_2_out_gg2(X, X)
if_palindrome_1_in_2_g5(L, X1s, X2s, EvenOdd, eq_2_out_gg2(EvenOdd, even_0)) -> if_palindrome_1_in_3_g4(L, X1s, X2s, eq_2_in_gg2(X1s, X2s))
if_palindrome_1_in_3_g4(L, X1s, X2s, eq_2_out_gg2(X1s, X2s)) -> palindrome_1_out_g1(L)
if_palindrome_1_in_1_g2(L, halves_4_out_gaaa4(L, X1s, X2s, EvenOdd)) -> if_palindrome_1_in_4_g5(L, X1s, X2s, EvenOdd, eq_2_in_gg2(EvenOdd, odd_0))
if_palindrome_1_in_4_g5(L, X1s, X2s, EvenOdd, eq_2_out_gg2(EvenOdd, odd_0)) -> if_palindrome_1_in_5_g4(L, X1s, X2s, last_3_in_gag3(X1s, underscore, X2s))
last_3_in_gag3(._22(T, []_0), T, []_0) -> last_3_out_gag3(._22(T, []_0), T, []_0)
last_3_in_gag3(._22(H, T), X, ._22(H, M)) -> if_last_3_in_1_gag5(H, T, X, M, last_3_in_gag3(T, X, M))
if_last_3_in_1_gag5(H, T, X, M, last_3_out_gag3(T, X, M)) -> last_3_out_gag3(._22(H, T), X, ._22(H, M))
if_palindrome_1_in_5_g4(L, X1s, X2s, last_3_out_gag3(X1s, underscore, X2s)) -> palindrome_1_out_g1(L)

The argument filtering Pi contains the following mapping:
palindrome_1_in_g1(x1)  =  palindrome_1_in_g1(x1)
even_0  =  even_0
odd_0  =  odd_0
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
if_palindrome_1_in_1_g2(x1, x2)  =  if_palindrome_1_in_1_g1(x2)
halves_4_in_gaaa4(x1, x2, x3, x4)  =  halves_4_in_gaaa1(x1)
halves_4_out_gaaa4(x1, x2, x3, x4)  =  halves_4_out_gaaa3(x2, x3, x4)
if_halves_4_in_1_gaaa8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_halves_4_in_1_gaaa2(x1, x8)
last_3_in_gaa3(x1, x2, x3)  =  last_3_in_gaa1(x1)
last_3_out_gaa3(x1, x2, x3)  =  last_3_out_gaa2(x2, x3)
if_last_3_in_1_gaa5(x1, x2, x3, x4, x5)  =  if_last_3_in_1_gaa2(x1, x5)
if_halves_4_in_2_gaaa9(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  if_halves_4_in_2_gaaa3(x1, x5, x9)
if_palindrome_1_in_2_g5(x1, x2, x3, x4, x5)  =  if_palindrome_1_in_2_g3(x2, x3, x5)
eq_2_in_gg2(x1, x2)  =  eq_2_in_gg2(x1, x2)
eq_2_out_gg2(x1, x2)  =  eq_2_out_gg
if_palindrome_1_in_3_g4(x1, x2, x3, x4)  =  if_palindrome_1_in_3_g1(x4)
palindrome_1_out_g1(x1)  =  palindrome_1_out_g
if_palindrome_1_in_4_g5(x1, x2, x3, x4, x5)  =  if_palindrome_1_in_4_g3(x2, x3, x5)
if_palindrome_1_in_5_g4(x1, x2, x3, x4)  =  if_palindrome_1_in_5_g1(x4)
last_3_in_gag3(x1, x2, x3)  =  last_3_in_gag2(x1, x3)
last_3_out_gag3(x1, x2, x3)  =  last_3_out_gag1(x2)
if_last_3_in_1_gag5(x1, x2, x3, x4, x5)  =  if_last_3_in_1_gag1(x5)
LAST_3_IN_GAG3(x1, x2, x3)  =  LAST_3_IN_GAG2(x1, 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
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP

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

LAST_3_IN_GAG3(._22(H, T), X, ._22(H, M)) -> LAST_3_IN_GAG3(T, X, M)

R is empty.
The argument filtering Pi contains the following mapping:
._22(x1, x2)  =  ._22(x1, x2)
LAST_3_IN_GAG3(x1, x2, x3)  =  LAST_3_IN_GAG2(x1, x3)

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
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP

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

LAST_3_IN_GAG2(._22(H, T), ._22(H, M)) -> LAST_3_IN_GAG2(T, M)

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



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
              ↳ PiDP

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

LAST_3_IN_GAA3(._22(H, T), X, ._22(H, M)) -> LAST_3_IN_GAA3(T, X, M)

The TRS R consists of the following rules:

palindrome_1_in_g1(L) -> if_palindrome_1_in_1_g2(L, halves_4_in_gaaa4(L, X1s, X2s, EvenOdd))
halves_4_in_gaaa4([]_0, []_0, []_0, even_0) -> halves_4_out_gaaa4([]_0, []_0, []_0, even_0)
halves_4_in_gaaa4(._22(X, []_0), ._22(X, []_0), []_0, odd_0) -> halves_4_out_gaaa4(._22(X, []_0), ._22(X, []_0), []_0, odd_0)
halves_4_in_gaaa4(._22(T, ._22(Y, Xs)), ._22(T, Ts), ._22(R, Rs), EvenOdd) -> if_halves_4_in_1_gaaa8(T, Y, Xs, Ts, R, Rs, EvenOdd, last_3_in_gaa3(._22(Y, Xs), R, Rests))
last_3_in_gaa3(._22(T, []_0), T, []_0) -> last_3_out_gaa3(._22(T, []_0), T, []_0)
last_3_in_gaa3(._22(H, T), X, ._22(H, M)) -> if_last_3_in_1_gaa5(H, T, X, M, last_3_in_gaa3(T, X, M))
if_last_3_in_1_gaa5(H, T, X, M, last_3_out_gaa3(T, X, M)) -> last_3_out_gaa3(._22(H, T), X, ._22(H, M))
if_halves_4_in_1_gaaa8(T, Y, Xs, Ts, R, Rs, EvenOdd, last_3_out_gaa3(._22(Y, Xs), R, Rests)) -> if_halves_4_in_2_gaaa9(T, Y, Xs, Ts, R, Rs, EvenOdd, Rests, halves_4_in_gaaa4(Rests, Ts, Rs, EvenOdd))
if_halves_4_in_2_gaaa9(T, Y, Xs, Ts, R, Rs, EvenOdd, Rests, halves_4_out_gaaa4(Rests, Ts, Rs, EvenOdd)) -> halves_4_out_gaaa4(._22(T, ._22(Y, Xs)), ._22(T, Ts), ._22(R, Rs), EvenOdd)
if_palindrome_1_in_1_g2(L, halves_4_out_gaaa4(L, X1s, X2s, EvenOdd)) -> if_palindrome_1_in_2_g5(L, X1s, X2s, EvenOdd, eq_2_in_gg2(EvenOdd, even_0))
eq_2_in_gg2(X, X) -> eq_2_out_gg2(X, X)
if_palindrome_1_in_2_g5(L, X1s, X2s, EvenOdd, eq_2_out_gg2(EvenOdd, even_0)) -> if_palindrome_1_in_3_g4(L, X1s, X2s, eq_2_in_gg2(X1s, X2s))
if_palindrome_1_in_3_g4(L, X1s, X2s, eq_2_out_gg2(X1s, X2s)) -> palindrome_1_out_g1(L)
if_palindrome_1_in_1_g2(L, halves_4_out_gaaa4(L, X1s, X2s, EvenOdd)) -> if_palindrome_1_in_4_g5(L, X1s, X2s, EvenOdd, eq_2_in_gg2(EvenOdd, odd_0))
if_palindrome_1_in_4_g5(L, X1s, X2s, EvenOdd, eq_2_out_gg2(EvenOdd, odd_0)) -> if_palindrome_1_in_5_g4(L, X1s, X2s, last_3_in_gag3(X1s, underscore, X2s))
last_3_in_gag3(._22(T, []_0), T, []_0) -> last_3_out_gag3(._22(T, []_0), T, []_0)
last_3_in_gag3(._22(H, T), X, ._22(H, M)) -> if_last_3_in_1_gag5(H, T, X, M, last_3_in_gag3(T, X, M))
if_last_3_in_1_gag5(H, T, X, M, last_3_out_gag3(T, X, M)) -> last_3_out_gag3(._22(H, T), X, ._22(H, M))
if_palindrome_1_in_5_g4(L, X1s, X2s, last_3_out_gag3(X1s, underscore, X2s)) -> palindrome_1_out_g1(L)

The argument filtering Pi contains the following mapping:
palindrome_1_in_g1(x1)  =  palindrome_1_in_g1(x1)
even_0  =  even_0
odd_0  =  odd_0
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
if_palindrome_1_in_1_g2(x1, x2)  =  if_palindrome_1_in_1_g1(x2)
halves_4_in_gaaa4(x1, x2, x3, x4)  =  halves_4_in_gaaa1(x1)
halves_4_out_gaaa4(x1, x2, x3, x4)  =  halves_4_out_gaaa3(x2, x3, x4)
if_halves_4_in_1_gaaa8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_halves_4_in_1_gaaa2(x1, x8)
last_3_in_gaa3(x1, x2, x3)  =  last_3_in_gaa1(x1)
last_3_out_gaa3(x1, x2, x3)  =  last_3_out_gaa2(x2, x3)
if_last_3_in_1_gaa5(x1, x2, x3, x4, x5)  =  if_last_3_in_1_gaa2(x1, x5)
if_halves_4_in_2_gaaa9(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  if_halves_4_in_2_gaaa3(x1, x5, x9)
if_palindrome_1_in_2_g5(x1, x2, x3, x4, x5)  =  if_palindrome_1_in_2_g3(x2, x3, x5)
eq_2_in_gg2(x1, x2)  =  eq_2_in_gg2(x1, x2)
eq_2_out_gg2(x1, x2)  =  eq_2_out_gg
if_palindrome_1_in_3_g4(x1, x2, x3, x4)  =  if_palindrome_1_in_3_g1(x4)
palindrome_1_out_g1(x1)  =  palindrome_1_out_g
if_palindrome_1_in_4_g5(x1, x2, x3, x4, x5)  =  if_palindrome_1_in_4_g3(x2, x3, x5)
if_palindrome_1_in_5_g4(x1, x2, x3, x4)  =  if_palindrome_1_in_5_g1(x4)
last_3_in_gag3(x1, x2, x3)  =  last_3_in_gag2(x1, x3)
last_3_out_gag3(x1, x2, x3)  =  last_3_out_gag1(x2)
if_last_3_in_1_gag5(x1, x2, x3, x4, x5)  =  if_last_3_in_1_gag1(x5)
LAST_3_IN_GAA3(x1, x2, x3)  =  LAST_3_IN_GAA1(x1)

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
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

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

LAST_3_IN_GAA3(._22(H, T), X, ._22(H, M)) -> LAST_3_IN_GAA3(T, X, M)

R is empty.
The argument filtering Pi contains the following mapping:
._22(x1, x2)  =  ._22(x1, x2)
LAST_3_IN_GAA3(x1, x2, x3)  =  LAST_3_IN_GAA1(x1)

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
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP

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

LAST_3_IN_GAA1(._22(H, T)) -> LAST_3_IN_GAA1(T)

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



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof

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

HALVES_4_IN_GAAA4(._22(T, ._22(Y, Xs)), ._22(T, Ts), ._22(R, Rs), EvenOdd) -> IF_HALVES_4_IN_1_GAAA8(T, Y, Xs, Ts, R, Rs, EvenOdd, last_3_in_gaa3(._22(Y, Xs), R, Rests))
IF_HALVES_4_IN_1_GAAA8(T, Y, Xs, Ts, R, Rs, EvenOdd, last_3_out_gaa3(._22(Y, Xs), R, Rests)) -> HALVES_4_IN_GAAA4(Rests, Ts, Rs, EvenOdd)

The TRS R consists of the following rules:

palindrome_1_in_g1(L) -> if_palindrome_1_in_1_g2(L, halves_4_in_gaaa4(L, X1s, X2s, EvenOdd))
halves_4_in_gaaa4([]_0, []_0, []_0, even_0) -> halves_4_out_gaaa4([]_0, []_0, []_0, even_0)
halves_4_in_gaaa4(._22(X, []_0), ._22(X, []_0), []_0, odd_0) -> halves_4_out_gaaa4(._22(X, []_0), ._22(X, []_0), []_0, odd_0)
halves_4_in_gaaa4(._22(T, ._22(Y, Xs)), ._22(T, Ts), ._22(R, Rs), EvenOdd) -> if_halves_4_in_1_gaaa8(T, Y, Xs, Ts, R, Rs, EvenOdd, last_3_in_gaa3(._22(Y, Xs), R, Rests))
last_3_in_gaa3(._22(T, []_0), T, []_0) -> last_3_out_gaa3(._22(T, []_0), T, []_0)
last_3_in_gaa3(._22(H, T), X, ._22(H, M)) -> if_last_3_in_1_gaa5(H, T, X, M, last_3_in_gaa3(T, X, M))
if_last_3_in_1_gaa5(H, T, X, M, last_3_out_gaa3(T, X, M)) -> last_3_out_gaa3(._22(H, T), X, ._22(H, M))
if_halves_4_in_1_gaaa8(T, Y, Xs, Ts, R, Rs, EvenOdd, last_3_out_gaa3(._22(Y, Xs), R, Rests)) -> if_halves_4_in_2_gaaa9(T, Y, Xs, Ts, R, Rs, EvenOdd, Rests, halves_4_in_gaaa4(Rests, Ts, Rs, EvenOdd))
if_halves_4_in_2_gaaa9(T, Y, Xs, Ts, R, Rs, EvenOdd, Rests, halves_4_out_gaaa4(Rests, Ts, Rs, EvenOdd)) -> halves_4_out_gaaa4(._22(T, ._22(Y, Xs)), ._22(T, Ts), ._22(R, Rs), EvenOdd)
if_palindrome_1_in_1_g2(L, halves_4_out_gaaa4(L, X1s, X2s, EvenOdd)) -> if_palindrome_1_in_2_g5(L, X1s, X2s, EvenOdd, eq_2_in_gg2(EvenOdd, even_0))
eq_2_in_gg2(X, X) -> eq_2_out_gg2(X, X)
if_palindrome_1_in_2_g5(L, X1s, X2s, EvenOdd, eq_2_out_gg2(EvenOdd, even_0)) -> if_palindrome_1_in_3_g4(L, X1s, X2s, eq_2_in_gg2(X1s, X2s))
if_palindrome_1_in_3_g4(L, X1s, X2s, eq_2_out_gg2(X1s, X2s)) -> palindrome_1_out_g1(L)
if_palindrome_1_in_1_g2(L, halves_4_out_gaaa4(L, X1s, X2s, EvenOdd)) -> if_palindrome_1_in_4_g5(L, X1s, X2s, EvenOdd, eq_2_in_gg2(EvenOdd, odd_0))
if_palindrome_1_in_4_g5(L, X1s, X2s, EvenOdd, eq_2_out_gg2(EvenOdd, odd_0)) -> if_palindrome_1_in_5_g4(L, X1s, X2s, last_3_in_gag3(X1s, underscore, X2s))
last_3_in_gag3(._22(T, []_0), T, []_0) -> last_3_out_gag3(._22(T, []_0), T, []_0)
last_3_in_gag3(._22(H, T), X, ._22(H, M)) -> if_last_3_in_1_gag5(H, T, X, M, last_3_in_gag3(T, X, M))
if_last_3_in_1_gag5(H, T, X, M, last_3_out_gag3(T, X, M)) -> last_3_out_gag3(._22(H, T), X, ._22(H, M))
if_palindrome_1_in_5_g4(L, X1s, X2s, last_3_out_gag3(X1s, underscore, X2s)) -> palindrome_1_out_g1(L)

The argument filtering Pi contains the following mapping:
palindrome_1_in_g1(x1)  =  palindrome_1_in_g1(x1)
even_0  =  even_0
odd_0  =  odd_0
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
if_palindrome_1_in_1_g2(x1, x2)  =  if_palindrome_1_in_1_g1(x2)
halves_4_in_gaaa4(x1, x2, x3, x4)  =  halves_4_in_gaaa1(x1)
halves_4_out_gaaa4(x1, x2, x3, x4)  =  halves_4_out_gaaa3(x2, x3, x4)
if_halves_4_in_1_gaaa8(x1, x2, x3, x4, x5, x6, x7, x8)  =  if_halves_4_in_1_gaaa2(x1, x8)
last_3_in_gaa3(x1, x2, x3)  =  last_3_in_gaa1(x1)
last_3_out_gaa3(x1, x2, x3)  =  last_3_out_gaa2(x2, x3)
if_last_3_in_1_gaa5(x1, x2, x3, x4, x5)  =  if_last_3_in_1_gaa2(x1, x5)
if_halves_4_in_2_gaaa9(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  if_halves_4_in_2_gaaa3(x1, x5, x9)
if_palindrome_1_in_2_g5(x1, x2, x3, x4, x5)  =  if_palindrome_1_in_2_g3(x2, x3, x5)
eq_2_in_gg2(x1, x2)  =  eq_2_in_gg2(x1, x2)
eq_2_out_gg2(x1, x2)  =  eq_2_out_gg
if_palindrome_1_in_3_g4(x1, x2, x3, x4)  =  if_palindrome_1_in_3_g1(x4)
palindrome_1_out_g1(x1)  =  palindrome_1_out_g
if_palindrome_1_in_4_g5(x1, x2, x3, x4, x5)  =  if_palindrome_1_in_4_g3(x2, x3, x5)
if_palindrome_1_in_5_g4(x1, x2, x3, x4)  =  if_palindrome_1_in_5_g1(x4)
last_3_in_gag3(x1, x2, x3)  =  last_3_in_gag2(x1, x3)
last_3_out_gag3(x1, x2, x3)  =  last_3_out_gag1(x2)
if_last_3_in_1_gag5(x1, x2, x3, x4, x5)  =  if_last_3_in_1_gag1(x5)
HALVES_4_IN_GAAA4(x1, x2, x3, x4)  =  HALVES_4_IN_GAAA1(x1)
IF_HALVES_4_IN_1_GAAA8(x1, x2, x3, x4, x5, x6, x7, x8)  =  IF_HALVES_4_IN_1_GAAA2(x1, x8)

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
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof

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

HALVES_4_IN_GAAA4(._22(T, ._22(Y, Xs)), ._22(T, Ts), ._22(R, Rs), EvenOdd) -> IF_HALVES_4_IN_1_GAAA8(T, Y, Xs, Ts, R, Rs, EvenOdd, last_3_in_gaa3(._22(Y, Xs), R, Rests))
IF_HALVES_4_IN_1_GAAA8(T, Y, Xs, Ts, R, Rs, EvenOdd, last_3_out_gaa3(._22(Y, Xs), R, Rests)) -> HALVES_4_IN_GAAA4(Rests, Ts, Rs, EvenOdd)

The TRS R consists of the following rules:

last_3_in_gaa3(._22(T, []_0), T, []_0) -> last_3_out_gaa3(._22(T, []_0), T, []_0)
last_3_in_gaa3(._22(H, T), X, ._22(H, M)) -> if_last_3_in_1_gaa5(H, T, X, M, last_3_in_gaa3(T, X, M))
if_last_3_in_1_gaa5(H, T, X, M, last_3_out_gaa3(T, X, M)) -> last_3_out_gaa3(._22(H, T), X, ._22(H, M))

The argument filtering Pi contains the following mapping:
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
last_3_in_gaa3(x1, x2, x3)  =  last_3_in_gaa1(x1)
last_3_out_gaa3(x1, x2, x3)  =  last_3_out_gaa2(x2, x3)
if_last_3_in_1_gaa5(x1, x2, x3, x4, x5)  =  if_last_3_in_1_gaa2(x1, x5)
HALVES_4_IN_GAAA4(x1, x2, x3, x4)  =  HALVES_4_IN_GAAA1(x1)
IF_HALVES_4_IN_1_GAAA8(x1, x2, x3, x4, x5, x6, x7, x8)  =  IF_HALVES_4_IN_1_GAAA2(x1, x8)

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
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPPoloProof

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

HALVES_4_IN_GAAA1(._22(T, ._22(Y, Xs))) -> IF_HALVES_4_IN_1_GAAA2(T, last_3_in_gaa1(._22(Y, Xs)))
IF_HALVES_4_IN_1_GAAA2(T, last_3_out_gaa2(R, Rests)) -> HALVES_4_IN_GAAA1(Rests)

The TRS R consists of the following rules:

last_3_in_gaa1(._22(T, []_0)) -> last_3_out_gaa2(T, []_0)
last_3_in_gaa1(._22(H, T)) -> if_last_3_in_1_gaa2(H, last_3_in_gaa1(T))
if_last_3_in_1_gaa2(H, last_3_out_gaa2(X, M)) -> last_3_out_gaa2(X, ._22(H, M))

The set Q consists of the following terms:

last_3_in_gaa1(x0)
if_last_3_in_1_gaa2(x0, x1)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_HALVES_4_IN_1_GAAA2, HALVES_4_IN_GAAA1}.
By using a polynomial ordering, the following set of Dependency Pairs of this DP problem can be strictly oriented.

HALVES_4_IN_GAAA1(._22(T, ._22(Y, Xs))) -> IF_HALVES_4_IN_1_GAAA2(T, last_3_in_gaa1(._22(Y, Xs)))
The remaining Dependency Pairs were at least non-strictly be oriented.

IF_HALVES_4_IN_1_GAAA2(T, last_3_out_gaa2(R, Rests)) -> HALVES_4_IN_GAAA1(Rests)
With the implicit AFS we had to orient the following set of usable rules non-strictly.

last_3_in_gaa1(._22(H, T)) -> if_last_3_in_1_gaa2(H, last_3_in_gaa1(T))
last_3_in_gaa1(._22(T, []_0)) -> last_3_out_gaa2(T, []_0)
if_last_3_in_1_gaa2(H, last_3_out_gaa2(X, M)) -> last_3_out_gaa2(X, ._22(H, M))
Used ordering: POLO with Polynomial interpretation:

POL(if_last_3_in_1_gaa2(x1, x2)) = 1 + x2   
POL(._22(x1, x2)) = 1 + x2   
POL(last_3_in_gaa1(x1)) = x1   
POL(IF_HALVES_4_IN_1_GAAA2(x1, x2)) = x2   
POL([]_0) = 0   
POL(HALVES_4_IN_GAAA1(x1)) = x1   
POL(last_3_out_gaa2(x1, x2)) = x2   



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
                      ↳ QDP
                        ↳ QDPPoloProof
                          ↳ QDP
                            ↳ DependencyGraphProof

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

IF_HALVES_4_IN_1_GAAA2(T, last_3_out_gaa2(R, Rests)) -> HALVES_4_IN_GAAA1(Rests)

The TRS R consists of the following rules:

last_3_in_gaa1(._22(T, []_0)) -> last_3_out_gaa2(T, []_0)
last_3_in_gaa1(._22(H, T)) -> if_last_3_in_1_gaa2(H, last_3_in_gaa1(T))
if_last_3_in_1_gaa2(H, last_3_out_gaa2(X, M)) -> last_3_out_gaa2(X, ._22(H, M))

The set Q consists of the following terms:

last_3_in_gaa1(x0)
if_last_3_in_1_gaa2(x0, x1)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {HALVES_4_IN_GAAA1, IF_HALVES_4_IN_1_GAAA2}.
The approximation of the Dependency Graph contains 0 SCCs with 1 less node.