Left Termination proof of /tmp/tmp5WUh0

Left Termination of the query pattern test_snake(b,b,b) w.r.t. the given Prolog program could not be shown:

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

test_snake₃(Pattern, C, R) :- s2l₂(C, Cols), s2l₂(R, Rows), snake₃(Pattern, Cols, Rows).
s2l₂(0₀, {}₀).
s2l₂(s₁(X), .₂(underscore, Y)) :- s2l₂(X, Y).
snake₃(Pattern, Cols, Rows) :- infinite_snake₃(Pattern, InfSnake, InfSnake), produce_snake₄(Rows, Cols, InfSnake, Snake), coil_it₂(Snake, odd₀).
infinite_snake₃({}₀, S, S).
infinite_snake₃(.₂(A, R), .₂(A, T), S) :- infinite_snake₃(R, T, S).
produce_snake₄({}₀, underscore1, underscore2, {}₀).
produce_snake₄(.₂(underscore3, Rows), Cols, InfSnake, .₂(Part, Tail)) :- part_{of_snake₄}(Cols, InfSnake, NewInfSnake, Part), produce_snake₄(Rows, Cols, NewInfSnake, Tail).
part_{of_snake₄}({}₀, RestSnake, RestSnake, {}₀).
part_{of_snake₄}(.₂(underscore4, R), .₂(Ring, Rings), RestSnake, .₂(Ring, RestRings)) :- part_{of_snake₄}(R, Rings, RestSnake, RestRings).
coil_it₂({}₀, underscore5).
coil_it₂(.₂(Line, Lines), odd₀) :- coil_it₂(Lines, even₀).
coil_it₂(.₂(Line, Lines), even₀) :- reverse2₂(Line, Line1), coil_it₂(Lines, odd₀).
reverse2₂(List, Reversed) :- reverse₃(List, {}₀, Reversed).
reverse₃({}₀, Reversed, Reversed).
reverse₃(.₂(Head, Tail), SoFar, Reversed) :- reverse₃(Tail, .₂(Head, SoFar), Reversed).

With regard to the inferred argument filtering the predicates were used in the following modes:
test_snake₃: (b,b,b)
s2l₂: (b,f)
snake₃: (b,b,b)
infinite_snake₃: (b,f,f)
produce_snake₄: (b,b,f,f)
part_of_snake₄: (b,f,f,f)
coil_it₂: (b,b)
reverse2₂: (f,f)
reverse₃: (f,b,f)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

test_snake_3_in_ggg₃(Pattern, C, R) -> if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_in_ga₂(C, Cols))
s2l_2_in_ga₂(0_0, []_0) -> s2l_2_out_ga₂(0_0, []_0)
s2l_2_in_ga₂(s_1₁(X), ._2₂(underscore, Y)) -> if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_in_ga₂(X, Y))
if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_out_ga₂(X, Y)) -> s2l_2_out_ga₂(s_1₁(X), ._2₂(underscore, Y))
if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_in_ga₂(R, Rows))
if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_in_ggg₃(Pattern, Cols, Rows))
snake_3_in_ggg₃(Pattern, Cols, Rows) -> if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_in_gaa₃(Pattern, InfSnake, InfSnake))
infinite_snake_3_in_gaa₃([]_0, S, S) -> infinite_snake_3_out_gaa₃([]_0, S, S)
infinite_snake_3_in_gaa₃(._2₂(A, R), ._2₂(A, T), S) -> if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_in_gaa₃(R, T, S))
if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_out_gaa₃(R, T, S)) -> infinite_snake_3_out_gaa₃(._2₂(A, R), ._2₂(A, T), S)
if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, InfSnake, Snake))
produce_snake_4_in_ggaa₄([]_0, underscore1, underscore2, []_0) -> produce_snake_4_out_ggaa₄([]_0, underscore1, underscore2, []_0)
produce_snake_4_in_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_4_in_gaaa₄([]_0, RestSnake, RestSnake, []_0) -> part_of_snake_4_out_gaaa₄([]_0, RestSnake, RestSnake, []_0)
part_of_snake_4_in_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_in_gaaa₄(R, Rings, RestSnake, RestRings))
if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_out_gaaa₄(R, Rings, RestSnake, RestRings)) -> part_of_snake_4_out_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings))
if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, NewInfSnake, Tail))
if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, NewInfSnake, Tail)) -> produce_snake_4_out_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail))
if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_in_gg₂(Snake, odd_0))
coil_it_2_in_gg₂([]_0, underscore5) -> coil_it_2_out_gg₂([]_0, underscore5)
coil_it_2_in_gg₂(._2₂(Line, Lines), odd_0) -> if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, even_0))
coil_it_2_in_gg₂(._2₂(Line, Lines), even_0) -> if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))
reverse2_2_in_aa₂(List, Reversed) -> if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_in_aga₃(List, []_0, Reversed))
reverse_3_in_aga₃([]_0, Reversed, Reversed) -> reverse_3_out_aga₃([]_0, Reversed, Reversed)
reverse_3_in_aga₃(._2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, ._2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, ._2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(._2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, []_0, Reversed)) -> reverse2_2_out_aa₂(List, Reversed)
if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, odd_0))
if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, odd_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), even_0)
if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, even_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), odd_0)
if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_out_gg₂(Snake, odd_0)) -> snake_3_out_ggg₃(Pattern, Cols, Rows)
if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_out_ggg₃(Pattern, Cols, Rows)) -> test_snake_3_out_ggg₃(Pattern, C, R)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

  ↳ PrologToPiTRSProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

test_snake_3_in_ggg₃(Pattern, C, R) -> if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_in_ga₂(C, Cols))
s2l_2_in_ga₂(0_0, []_0) -> s2l_2_out_ga₂(0_0, []_0)
s2l_2_in_ga₂(s_1₁(X), ._2₂(underscore, Y)) -> if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_in_ga₂(X, Y))
if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_out_ga₂(X, Y)) -> s2l_2_out_ga₂(s_1₁(X), ._2₂(underscore, Y))
if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_in_ga₂(R, Rows))
if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_in_ggg₃(Pattern, Cols, Rows))
snake_3_in_ggg₃(Pattern, Cols, Rows) -> if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_in_gaa₃(Pattern, InfSnake, InfSnake))
infinite_snake_3_in_gaa₃([]_0, S, S) -> infinite_snake_3_out_gaa₃([]_0, S, S)
infinite_snake_3_in_gaa₃(._2₂(A, R), ._2₂(A, T), S) -> if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_in_gaa₃(R, T, S))
if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_out_gaa₃(R, T, S)) -> infinite_snake_3_out_gaa₃(._2₂(A, R), ._2₂(A, T), S)
if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, InfSnake, Snake))
produce_snake_4_in_ggaa₄([]_0, underscore1, underscore2, []_0) -> produce_snake_4_out_ggaa₄([]_0, underscore1, underscore2, []_0)
produce_snake_4_in_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_4_in_gaaa₄([]_0, RestSnake, RestSnake, []_0) -> part_of_snake_4_out_gaaa₄([]_0, RestSnake, RestSnake, []_0)
part_of_snake_4_in_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_in_gaaa₄(R, Rings, RestSnake, RestRings))
if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_out_gaaa₄(R, Rings, RestSnake, RestRings)) -> part_of_snake_4_out_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings))
if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, NewInfSnake, Tail))
if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, NewInfSnake, Tail)) -> produce_snake_4_out_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail))
if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_in_gg₂(Snake, odd_0))
coil_it_2_in_gg₂([]_0, underscore5) -> coil_it_2_out_gg₂([]_0, underscore5)
coil_it_2_in_gg₂(._2₂(Line, Lines), odd_0) -> if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, even_0))
coil_it_2_in_gg₂(._2₂(Line, Lines), even_0) -> if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))
reverse2_2_in_aa₂(List, Reversed) -> if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_in_aga₃(List, []_0, Reversed))
reverse_3_in_aga₃([]_0, Reversed, Reversed) -> reverse_3_out_aga₃([]_0, Reversed, Reversed)
reverse_3_in_aga₃(._2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, ._2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, ._2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(._2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, []_0, Reversed)) -> reverse2_2_out_aa₂(List, Reversed)
if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, odd_0))
if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, odd_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), even_0)
if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, even_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), odd_0)
if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_out_gg₂(Snake, odd_0)) -> snake_3_out_ggg₃(Pattern, Cols, Rows)
if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_out_ggg₃(Pattern, Cols, Rows)) -> test_snake_3_out_ggg₃(Pattern, C, R)

TEST_SNAKE_3_IN_GGG₃(Pattern, C, R) -> IF_TEST_SNAKE_3_IN_1_GGG₄(Pattern, C, R, s2l_2_in_ga₂(C, Cols))
TEST_SNAKE_3_IN_GGG₃(Pattern, C, R) -> S2L_2_IN_GA₂(C, Cols)
S2L_2_IN_GA₂(s_1₁(X), ._2₂(underscore, Y)) -> IF_S2L_2_IN_1_GA₄(X, underscore, Y, s2l_2_in_ga₂(X, Y))
S2L_2_IN_GA₂(s_1₁(X), ._2₂(underscore, Y)) -> S2L_2_IN_GA₂(X, Y)
IF_TEST_SNAKE_3_IN_1_GGG₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> IF_TEST_SNAKE_3_IN_2_GGG₅(Pattern, C, R, Cols, s2l_2_in_ga₂(R, Rows))
IF_TEST_SNAKE_3_IN_1_GGG₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> S2L_2_IN_GA₂(R, Rows)
IF_TEST_SNAKE_3_IN_2_GGG₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> IF_TEST_SNAKE_3_IN_3_GGG₆(Pattern, C, R, Cols, Rows, snake_3_in_ggg₃(Pattern, Cols, Rows))
IF_TEST_SNAKE_3_IN_2_GGG₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> SNAKE_3_IN_GGG₃(Pattern, Cols, Rows)
SNAKE_3_IN_GGG₃(Pattern, Cols, Rows) -> IF_SNAKE_3_IN_1_GGG₄(Pattern, Cols, Rows, infinite_snake_3_in_gaa₃(Pattern, InfSnake, InfSnake))
SNAKE_3_IN_GGG₃(Pattern, Cols, Rows) -> INFINITE_SNAKE_3_IN_GAA₃(Pattern, InfSnake, InfSnake)
INFINITE_SNAKE_3_IN_GAA₃(._2₂(A, R), ._2₂(A, T), S) -> IF_INFINITE_SNAKE_3_IN_1_GAA₅(A, R, T, S, infinite_snake_3_in_gaa₃(R, T, S))
INFINITE_SNAKE_3_IN_GAA₃(._2₂(A, R), ._2₂(A, T), S) -> INFINITE_SNAKE_3_IN_GAA₃(R, T, S)
IF_SNAKE_3_IN_1_GGG₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> IF_SNAKE_3_IN_2_GGG₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, InfSnake, Snake))
IF_SNAKE_3_IN_1_GGG₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> PRODUCE_SNAKE_4_IN_GGAA₄(Rows, Cols, InfSnake, Snake)
PRODUCE_SNAKE_4_IN_GGAA₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> IF_PRODUCE_SNAKE_4_IN_1_GGAA₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
PRODUCE_SNAKE_4_IN_GGAA₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> PART_OF_SNAKE_4_IN_GAAA₄(Cols, InfSnake, NewInfSnake, Part)
PART_OF_SNAKE_4_IN_GAAA₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> IF_PART_OF_SNAKE_4_IN_1_GAAA₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_in_gaaa₄(R, Rings, RestSnake, RestRings))
PART_OF_SNAKE_4_IN_GAAA₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> PART_OF_SNAKE_4_IN_GAAA₄(R, Rings, RestSnake, RestRings)
IF_PRODUCE_SNAKE_4_IN_1_GGAA₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> IF_PRODUCE_SNAKE_4_IN_2_GGAA₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, NewInfSnake, Tail))
IF_PRODUCE_SNAKE_4_IN_1_GGAA₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> PRODUCE_SNAKE_4_IN_GGAA₄(Rows, Cols, NewInfSnake, Tail)
IF_SNAKE_3_IN_2_GGG₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> IF_SNAKE_3_IN_3_GGG₅(Pattern, Cols, Rows, Snake, coil_it_2_in_gg₂(Snake, odd_0))
IF_SNAKE_3_IN_2_GGG₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> COIL_IT_2_IN_GG₂(Snake, odd_0)
COIL_IT_2_IN_GG₂(._2₂(Line, Lines), odd_0) -> IF_COIL_IT_2_IN_1_GG₃(Line, Lines, coil_it_2_in_gg₂(Lines, even_0))
COIL_IT_2_IN_GG₂(._2₂(Line, Lines), odd_0) -> COIL_IT_2_IN_GG₂(Lines, even_0)
COIL_IT_2_IN_GG₂(._2₂(Line, Lines), even_0) -> IF_COIL_IT_2_IN_2_GG₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))
COIL_IT_2_IN_GG₂(._2₂(Line, Lines), even_0) -> REVERSE2_2_IN_AA₂(Line, Line1)
REVERSE2_2_IN_AA₂(List, Reversed) -> IF_REVERSE2_2_IN_1_AA₃(List, Reversed, reverse_3_in_aga₃(List, []_0, Reversed))
REVERSE2_2_IN_AA₂(List, Reversed) -> REVERSE_3_IN_AGA₃(List, []_0, Reversed)
REVERSE_3_IN_AGA₃(._2₂(Head, Tail), SoFar, Reversed) -> IF_REVERSE_3_IN_1_AGA₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, ._2₂(Head, SoFar), Reversed))
REVERSE_3_IN_AGA₃(._2₂(Head, Tail), SoFar, Reversed) -> REVERSE_3_IN_AGA₃(Tail, ._2₂(Head, SoFar), Reversed)
IF_COIL_IT_2_IN_2_GG₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> IF_COIL_IT_2_IN_3_GG₃(Line, Lines, coil_it_2_in_gg₂(Lines, odd_0))
IF_COIL_IT_2_IN_2_GG₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> COIL_IT_2_IN_GG₂(Lines, odd_0)

The TRS R consists of the following rules:

test_snake_3_in_ggg₃(Pattern, C, R) -> if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_in_ga₂(C, Cols))
s2l_2_in_ga₂(0_0, []_0) -> s2l_2_out_ga₂(0_0, []_0)
s2l_2_in_ga₂(s_1₁(X), ._2₂(underscore, Y)) -> if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_in_ga₂(X, Y))
if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_out_ga₂(X, Y)) -> s2l_2_out_ga₂(s_1₁(X), ._2₂(underscore, Y))
if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_in_ga₂(R, Rows))
if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_in_ggg₃(Pattern, Cols, Rows))
snake_3_in_ggg₃(Pattern, Cols, Rows) -> if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_in_gaa₃(Pattern, InfSnake, InfSnake))
infinite_snake_3_in_gaa₃([]_0, S, S) -> infinite_snake_3_out_gaa₃([]_0, S, S)
infinite_snake_3_in_gaa₃(._2₂(A, R), ._2₂(A, T), S) -> if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_in_gaa₃(R, T, S))
if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_out_gaa₃(R, T, S)) -> infinite_snake_3_out_gaa₃(._2₂(A, R), ._2₂(A, T), S)
if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, InfSnake, Snake))
produce_snake_4_in_ggaa₄([]_0, underscore1, underscore2, []_0) -> produce_snake_4_out_ggaa₄([]_0, underscore1, underscore2, []_0)
produce_snake_4_in_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_4_in_gaaa₄([]_0, RestSnake, RestSnake, []_0) -> part_of_snake_4_out_gaaa₄([]_0, RestSnake, RestSnake, []_0)
part_of_snake_4_in_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_in_gaaa₄(R, Rings, RestSnake, RestRings))
if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_out_gaaa₄(R, Rings, RestSnake, RestRings)) -> part_of_snake_4_out_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings))
if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, NewInfSnake, Tail))
if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, NewInfSnake, Tail)) -> produce_snake_4_out_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail))
if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_in_gg₂(Snake, odd_0))
coil_it_2_in_gg₂([]_0, underscore5) -> coil_it_2_out_gg₂([]_0, underscore5)
coil_it_2_in_gg₂(._2₂(Line, Lines), odd_0) -> if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, even_0))
coil_it_2_in_gg₂(._2₂(Line, Lines), even_0) -> if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))
reverse2_2_in_aa₂(List, Reversed) -> if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_in_aga₃(List, []_0, Reversed))
reverse_3_in_aga₃([]_0, Reversed, Reversed) -> reverse_3_out_aga₃([]_0, Reversed, Reversed)
reverse_3_in_aga₃(._2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, ._2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, ._2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(._2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, []_0, Reversed)) -> reverse2_2_out_aa₂(List, Reversed)
if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, odd_0))
if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, odd_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), even_0)
if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, even_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), odd_0)
if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_out_gg₂(Snake, odd_0)) -> snake_3_out_ggg₃(Pattern, Cols, Rows)
if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_out_ggg₃(Pattern, Cols, Rows)) -> test_snake_3_out_ggg₃(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_3_in_ggg₃(x1, x2, x3) = test_snake_3_in_ggg₃(x1, x2, x3)
0_0 = 0_0
[]_0 = []_0
s_1₁(x1) = s_1₁(x1)
._2₂(x1, x2) = ._2₁(x2)
odd_0 = odd_0
even_0 = even_0
if_test_snake_3_in_1_ggg₄(x1, x2, x3, x4) = if_test_snake_3_in_1_ggg₃(x1, x3, x4)
s2l_2_in_ga₂(x1, x2) = s2l_2_in_ga₁(x1)
s2l_2_out_ga₂(x1, x2) = s2l_2_out_ga₁(x2)
if_s2l_2_in_1_ga₄(x1, x2, x3, x4) = if_s2l_2_in_1_ga₁(x4)
if_test_snake_3_in_2_ggg₅(x1, x2, x3, x4, x5) = if_test_snake_3_in_2_ggg₃(x1, x4, x5)
if_test_snake_3_in_3_ggg₆(x1, x2, x3, x4, x5, x6) = if_test_snake_3_in_3_ggg₁(x6)
snake_3_in_ggg₃(x1, x2, x3) = snake_3_in_ggg₃(x1, x2, x3)
if_snake_3_in_1_ggg₄(x1, x2, x3, x4) = if_snake_3_in_1_ggg₃(x2, x3, x4)
infinite_snake_3_in_gaa₃(x1, x2, x3) = infinite_snake_3_in_gaa₁(x1)
infinite_snake_3_out_gaa₃(x1, x2, x3) = infinite_snake_3_out_gaa
if_infinite_snake_3_in_1_gaa₅(x1, x2, x3, x4, x5) = if_infinite_snake_3_in_1_gaa₁(x5)
if_snake_3_in_2_ggg₅(x1, x2, x3, x4, x5) = if_snake_3_in_2_ggg₁(x5)
produce_snake_4_in_ggaa₄(x1, x2, x3, x4) = produce_snake_4_in_ggaa₂(x1, x2)
produce_snake_4_out_ggaa₄(x1, x2, x3, x4) = produce_snake_4_out_ggaa₁(x4)
if_produce_snake_4_in_1_ggaa₇(x1, x2, x3, x4, x5, x6, x7) = if_produce_snake_4_in_1_ggaa₃(x2, x3, x7)
part_of_snake_4_in_gaaa₄(x1, x2, x3, x4) = part_of_snake_4_in_gaaa₁(x1)
part_of_snake_4_out_gaaa₄(x1, x2, x3, x4) = part_of_snake_4_out_gaaa₁(x4)
if_part_of_snake_4_in_1_gaaa₇(x1, x2, x3, x4, x5, x6, x7) = if_part_of_snake_4_in_1_gaaa₁(x7)
if_produce_snake_4_in_2_ggaa₈(x1, x2, x3, x4, x5, x6, x7, x8) = if_produce_snake_4_in_2_ggaa₁(x8)
if_snake_3_in_3_ggg₅(x1, x2, x3, x4, x5) = if_snake_3_in_3_ggg₁(x5)
coil_it_2_in_gg₂(x1, x2) = coil_it_2_in_gg₂(x1, x2)
coil_it_2_out_gg₂(x1, x2) = coil_it_2_out_gg
if_coil_it_2_in_1_gg₃(x1, x2, x3) = if_coil_it_2_in_1_gg₁(x3)
if_coil_it_2_in_2_gg₃(x1, x2, x3) = if_coil_it_2_in_2_gg₂(x2, x3)
reverse2_2_in_aa₂(x1, x2) = reverse2_2_in_aa
if_reverse2_2_in_1_aa₃(x1, x2, x3) = if_reverse2_2_in_1_aa₁(x3)
reverse_3_in_aga₃(x1, x2, x3) = reverse_3_in_aga₁(x2)
reverse_3_out_aga₃(x1, x2, x3) = reverse_3_out_aga₂(x1, x3)
if_reverse_3_in_1_aga₅(x1, x2, x3, x4, x5) = if_reverse_3_in_1_aga₁(x5)
reverse2_2_out_aa₂(x1, x2) = reverse2_2_out_aa₂(x1, x2)
if_coil_it_2_in_3_gg₃(x1, x2, x3) = if_coil_it_2_in_3_gg₁(x3)
snake_3_out_ggg₃(x1, x2, x3) = snake_3_out_ggg
test_snake_3_out_ggg₃(x1, x2, x3) = test_snake_3_out_ggg
TEST_SNAKE_3_IN_GGG₃(x1, x2, x3) = TEST_SNAKE_3_IN_GGG₃(x1, x2, x3)
IF_COIL_IT_2_IN_1_GG₃(x1, x2, x3) = IF_COIL_IT_2_IN_1_GG₁(x3)
IF_REVERSE2_2_IN_1_AA₃(x1, x2, x3) = IF_REVERSE2_2_IN_1_AA₁(x3)
IF_PRODUCE_SNAKE_4_IN_1_GGAA₇(x1, x2, x3, x4, x5, x6, x7) = IF_PRODUCE_SNAKE_4_IN_1_GGAA₃(x2, x3, x7)
IF_REVERSE_3_IN_1_AGA₅(x1, x2, x3, x4, x5) = IF_REVERSE_3_IN_1_AGA₁(x5)
IF_INFINITE_SNAKE_3_IN_1_GAA₅(x1, x2, x3, x4, x5) = IF_INFINITE_SNAKE_3_IN_1_GAA₁(x5)
IF_SNAKE_3_IN_3_GGG₅(x1, x2, x3, x4, x5) = IF_SNAKE_3_IN_3_GGG₁(x5)
S2L_2_IN_GA₂(x1, x2) = S2L_2_IN_GA₁(x1)
IF_TEST_SNAKE_3_IN_3_GGG₆(x1, x2, x3, x4, x5, x6) = IF_TEST_SNAKE_3_IN_3_GGG₁(x6)
IF_COIL_IT_2_IN_2_GG₃(x1, x2, x3) = IF_COIL_IT_2_IN_2_GG₂(x2, x3)
IF_TEST_SNAKE_3_IN_2_GGG₅(x1, x2, x3, x4, x5) = IF_TEST_SNAKE_3_IN_2_GGG₃(x1, x4, x5)
PRODUCE_SNAKE_4_IN_GGAA₄(x1, x2, x3, x4) = PRODUCE_SNAKE_4_IN_GGAA₂(x1, x2)
IF_COIL_IT_2_IN_3_GG₃(x1, x2, x3) = IF_COIL_IT_2_IN_3_GG₁(x3)
IF_PART_OF_SNAKE_4_IN_1_GAAA₇(x1, x2, x3, x4, x5, x6, x7) = IF_PART_OF_SNAKE_4_IN_1_GAAA₁(x7)
REVERSE_3_IN_AGA₃(x1, x2, x3) = REVERSE_3_IN_AGA₁(x2)
IF_PRODUCE_SNAKE_4_IN_2_GGAA₈(x1, x2, x3, x4, x5, x6, x7, x8) = IF_PRODUCE_SNAKE_4_IN_2_GGAA₁(x8)
INFINITE_SNAKE_3_IN_GAA₃(x1, x2, x3) = INFINITE_SNAKE_3_IN_GAA₁(x1)
COIL_IT_2_IN_GG₂(x1, x2) = COIL_IT_2_IN_GG₂(x1, x2)
REVERSE2_2_IN_AA₂(x1, x2) = REVERSE2_2_IN_AA
IF_TEST_SNAKE_3_IN_1_GGG₄(x1, x2, x3, x4) = IF_TEST_SNAKE_3_IN_1_GGG₃(x1, x3, x4)
PART_OF_SNAKE_4_IN_GAAA₄(x1, x2, x3, x4) = PART_OF_SNAKE_4_IN_GAAA₁(x1)
IF_S2L_2_IN_1_GA₄(x1, x2, x3, x4) = IF_S2L_2_IN_1_GA₁(x4)
IF_SNAKE_3_IN_1_GGG₄(x1, x2, x3, x4) = IF_SNAKE_3_IN_1_GGG₃(x2, x3, x4)
SNAKE_3_IN_GGG₃(x1, x2, x3) = SNAKE_3_IN_GGG₃(x1, x2, x3)
IF_SNAKE_3_IN_2_GGG₅(x1, x2, x3, x4, x5) = IF_SNAKE_3_IN_2_GGG₁(x5)

We have to consider all (P,R,Pi)-chains

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

  ↳ PrologToPiTRSProof

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

TEST_SNAKE_3_IN_GGG₃(Pattern, C, R) -> IF_TEST_SNAKE_3_IN_1_GGG₄(Pattern, C, R, s2l_2_in_ga₂(C, Cols))
TEST_SNAKE_3_IN_GGG₃(Pattern, C, R) -> S2L_2_IN_GA₂(C, Cols)
S2L_2_IN_GA₂(s_1₁(X), ._2₂(underscore, Y)) -> IF_S2L_2_IN_1_GA₄(X, underscore, Y, s2l_2_in_ga₂(X, Y))
S2L_2_IN_GA₂(s_1₁(X), ._2₂(underscore, Y)) -> S2L_2_IN_GA₂(X, Y)
IF_TEST_SNAKE_3_IN_1_GGG₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> IF_TEST_SNAKE_3_IN_2_GGG₅(Pattern, C, R, Cols, s2l_2_in_ga₂(R, Rows))
IF_TEST_SNAKE_3_IN_1_GGG₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> S2L_2_IN_GA₂(R, Rows)
IF_TEST_SNAKE_3_IN_2_GGG₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> IF_TEST_SNAKE_3_IN_3_GGG₆(Pattern, C, R, Cols, Rows, snake_3_in_ggg₃(Pattern, Cols, Rows))
IF_TEST_SNAKE_3_IN_2_GGG₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> SNAKE_3_IN_GGG₃(Pattern, Cols, Rows)
SNAKE_3_IN_GGG₃(Pattern, Cols, Rows) -> IF_SNAKE_3_IN_1_GGG₄(Pattern, Cols, Rows, infinite_snake_3_in_gaa₃(Pattern, InfSnake, InfSnake))
SNAKE_3_IN_GGG₃(Pattern, Cols, Rows) -> INFINITE_SNAKE_3_IN_GAA₃(Pattern, InfSnake, InfSnake)
INFINITE_SNAKE_3_IN_GAA₃(._2₂(A, R), ._2₂(A, T), S) -> IF_INFINITE_SNAKE_3_IN_1_GAA₅(A, R, T, S, infinite_snake_3_in_gaa₃(R, T, S))
INFINITE_SNAKE_3_IN_GAA₃(._2₂(A, R), ._2₂(A, T), S) -> INFINITE_SNAKE_3_IN_GAA₃(R, T, S)
IF_SNAKE_3_IN_1_GGG₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> IF_SNAKE_3_IN_2_GGG₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, InfSnake, Snake))
IF_SNAKE_3_IN_1_GGG₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> PRODUCE_SNAKE_4_IN_GGAA₄(Rows, Cols, InfSnake, Snake)
PRODUCE_SNAKE_4_IN_GGAA₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> IF_PRODUCE_SNAKE_4_IN_1_GGAA₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
PRODUCE_SNAKE_4_IN_GGAA₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> PART_OF_SNAKE_4_IN_GAAA₄(Cols, InfSnake, NewInfSnake, Part)
PART_OF_SNAKE_4_IN_GAAA₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> IF_PART_OF_SNAKE_4_IN_1_GAAA₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_in_gaaa₄(R, Rings, RestSnake, RestRings))
PART_OF_SNAKE_4_IN_GAAA₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> PART_OF_SNAKE_4_IN_GAAA₄(R, Rings, RestSnake, RestRings)
IF_PRODUCE_SNAKE_4_IN_1_GGAA₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> IF_PRODUCE_SNAKE_4_IN_2_GGAA₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, NewInfSnake, Tail))
IF_PRODUCE_SNAKE_4_IN_1_GGAA₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> PRODUCE_SNAKE_4_IN_GGAA₄(Rows, Cols, NewInfSnake, Tail)
IF_SNAKE_3_IN_2_GGG₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> IF_SNAKE_3_IN_3_GGG₅(Pattern, Cols, Rows, Snake, coil_it_2_in_gg₂(Snake, odd_0))
IF_SNAKE_3_IN_2_GGG₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> COIL_IT_2_IN_GG₂(Snake, odd_0)
COIL_IT_2_IN_GG₂(._2₂(Line, Lines), odd_0) -> IF_COIL_IT_2_IN_1_GG₃(Line, Lines, coil_it_2_in_gg₂(Lines, even_0))
COIL_IT_2_IN_GG₂(._2₂(Line, Lines), odd_0) -> COIL_IT_2_IN_GG₂(Lines, even_0)
COIL_IT_2_IN_GG₂(._2₂(Line, Lines), even_0) -> IF_COIL_IT_2_IN_2_GG₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))
COIL_IT_2_IN_GG₂(._2₂(Line, Lines), even_0) -> REVERSE2_2_IN_AA₂(Line, Line1)
REVERSE2_2_IN_AA₂(List, Reversed) -> IF_REVERSE2_2_IN_1_AA₃(List, Reversed, reverse_3_in_aga₃(List, []_0, Reversed))
REVERSE2_2_IN_AA₂(List, Reversed) -> REVERSE_3_IN_AGA₃(List, []_0, Reversed)
REVERSE_3_IN_AGA₃(._2₂(Head, Tail), SoFar, Reversed) -> IF_REVERSE_3_IN_1_AGA₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, ._2₂(Head, SoFar), Reversed))
REVERSE_3_IN_AGA₃(._2₂(Head, Tail), SoFar, Reversed) -> REVERSE_3_IN_AGA₃(Tail, ._2₂(Head, SoFar), Reversed)
IF_COIL_IT_2_IN_2_GG₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> IF_COIL_IT_2_IN_3_GG₃(Line, Lines, coil_it_2_in_gg₂(Lines, odd_0))
IF_COIL_IT_2_IN_2_GG₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> COIL_IT_2_IN_GG₂(Lines, odd_0)

The TRS R consists of the following rules:

test_snake_3_in_ggg₃(Pattern, C, R) -> if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_in_ga₂(C, Cols))
s2l_2_in_ga₂(0_0, []_0) -> s2l_2_out_ga₂(0_0, []_0)
s2l_2_in_ga₂(s_1₁(X), ._2₂(underscore, Y)) -> if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_in_ga₂(X, Y))
if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_out_ga₂(X, Y)) -> s2l_2_out_ga₂(s_1₁(X), ._2₂(underscore, Y))
if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_in_ga₂(R, Rows))
if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_in_ggg₃(Pattern, Cols, Rows))
snake_3_in_ggg₃(Pattern, Cols, Rows) -> if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_in_gaa₃(Pattern, InfSnake, InfSnake))
infinite_snake_3_in_gaa₃([]_0, S, S) -> infinite_snake_3_out_gaa₃([]_0, S, S)
infinite_snake_3_in_gaa₃(._2₂(A, R), ._2₂(A, T), S) -> if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_in_gaa₃(R, T, S))
if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_out_gaa₃(R, T, S)) -> infinite_snake_3_out_gaa₃(._2₂(A, R), ._2₂(A, T), S)
if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, InfSnake, Snake))
produce_snake_4_in_ggaa₄([]_0, underscore1, underscore2, []_0) -> produce_snake_4_out_ggaa₄([]_0, underscore1, underscore2, []_0)
produce_snake_4_in_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_4_in_gaaa₄([]_0, RestSnake, RestSnake, []_0) -> part_of_snake_4_out_gaaa₄([]_0, RestSnake, RestSnake, []_0)
part_of_snake_4_in_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_in_gaaa₄(R, Rings, RestSnake, RestRings))
if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_out_gaaa₄(R, Rings, RestSnake, RestRings)) -> part_of_snake_4_out_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings))
if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, NewInfSnake, Tail))
if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, NewInfSnake, Tail)) -> produce_snake_4_out_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail))
if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_in_gg₂(Snake, odd_0))
coil_it_2_in_gg₂([]_0, underscore5) -> coil_it_2_out_gg₂([]_0, underscore5)
coil_it_2_in_gg₂(._2₂(Line, Lines), odd_0) -> if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, even_0))
coil_it_2_in_gg₂(._2₂(Line, Lines), even_0) -> if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))
reverse2_2_in_aa₂(List, Reversed) -> if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_in_aga₃(List, []_0, Reversed))
reverse_3_in_aga₃([]_0, Reversed, Reversed) -> reverse_3_out_aga₃([]_0, Reversed, Reversed)
reverse_3_in_aga₃(._2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, ._2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, ._2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(._2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, []_0, Reversed)) -> reverse2_2_out_aa₂(List, Reversed)
if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, odd_0))
if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, odd_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), even_0)
if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, even_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), odd_0)
if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_out_gg₂(Snake, odd_0)) -> snake_3_out_ggg₃(Pattern, Cols, Rows)
if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_out_ggg₃(Pattern, Cols, Rows)) -> test_snake_3_out_ggg₃(Pattern, C, R)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

REVERSE_3_IN_AGA₃(._2₂(Head, Tail), SoFar, Reversed) -> REVERSE_3_IN_AGA₃(Tail, ._2₂(Head, SoFar), Reversed)

The TRS R consists of the following rules:

test_snake_3_in_ggg₃(Pattern, C, R) -> if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_in_ga₂(C, Cols))
s2l_2_in_ga₂(0_0, []_0) -> s2l_2_out_ga₂(0_0, []_0)
s2l_2_in_ga₂(s_1₁(X), ._2₂(underscore, Y)) -> if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_in_ga₂(X, Y))
if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_out_ga₂(X, Y)) -> s2l_2_out_ga₂(s_1₁(X), ._2₂(underscore, Y))
if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_in_ga₂(R, Rows))
if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_in_ggg₃(Pattern, Cols, Rows))
snake_3_in_ggg₃(Pattern, Cols, Rows) -> if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_in_gaa₃(Pattern, InfSnake, InfSnake))
infinite_snake_3_in_gaa₃([]_0, S, S) -> infinite_snake_3_out_gaa₃([]_0, S, S)
infinite_snake_3_in_gaa₃(._2₂(A, R), ._2₂(A, T), S) -> if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_in_gaa₃(R, T, S))
if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_out_gaa₃(R, T, S)) -> infinite_snake_3_out_gaa₃(._2₂(A, R), ._2₂(A, T), S)
if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, InfSnake, Snake))
produce_snake_4_in_ggaa₄([]_0, underscore1, underscore2, []_0) -> produce_snake_4_out_ggaa₄([]_0, underscore1, underscore2, []_0)
produce_snake_4_in_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_4_in_gaaa₄([]_0, RestSnake, RestSnake, []_0) -> part_of_snake_4_out_gaaa₄([]_0, RestSnake, RestSnake, []_0)
part_of_snake_4_in_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_in_gaaa₄(R, Rings, RestSnake, RestRings))
if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_out_gaaa₄(R, Rings, RestSnake, RestRings)) -> part_of_snake_4_out_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings))
if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, NewInfSnake, Tail))
if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, NewInfSnake, Tail)) -> produce_snake_4_out_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail))
if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_in_gg₂(Snake, odd_0))
coil_it_2_in_gg₂([]_0, underscore5) -> coil_it_2_out_gg₂([]_0, underscore5)
coil_it_2_in_gg₂(._2₂(Line, Lines), odd_0) -> if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, even_0))
coil_it_2_in_gg₂(._2₂(Line, Lines), even_0) -> if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))
reverse2_2_in_aa₂(List, Reversed) -> if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_in_aga₃(List, []_0, Reversed))
reverse_3_in_aga₃([]_0, Reversed, Reversed) -> reverse_3_out_aga₃([]_0, Reversed, Reversed)
reverse_3_in_aga₃(._2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, ._2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, ._2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(._2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, []_0, Reversed)) -> reverse2_2_out_aa₂(List, Reversed)
if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, odd_0))
if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, odd_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), even_0)
if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, even_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), odd_0)
if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_out_gg₂(Snake, odd_0)) -> snake_3_out_ggg₃(Pattern, Cols, Rows)
if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_out_ggg₃(Pattern, Cols, Rows)) -> test_snake_3_out_ggg₃(Pattern, C, R)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

REVERSE_3_IN_AGA₃(._2₂(Head, Tail), SoFar, Reversed) -> REVERSE_3_IN_AGA₃(Tail, ._2₂(Head, SoFar), Reversed)

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

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

REVERSE_3_IN_AGA₁(SoFar) -> REVERSE_3_IN_AGA₁(._2₁(SoFar))

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_AGA₁}.

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

COIL_IT_2_IN_GG₂(._2₂(Line, Lines), odd_0) -> COIL_IT_2_IN_GG₂(Lines, even_0)
IF_COIL_IT_2_IN_2_GG₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> COIL_IT_2_IN_GG₂(Lines, odd_0)
COIL_IT_2_IN_GG₂(._2₂(Line, Lines), even_0) -> IF_COIL_IT_2_IN_2_GG₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))

The TRS R consists of the following rules:

test_snake_3_in_ggg₃(Pattern, C, R) -> if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_in_ga₂(C, Cols))
s2l_2_in_ga₂(0_0, []_0) -> s2l_2_out_ga₂(0_0, []_0)
s2l_2_in_ga₂(s_1₁(X), ._2₂(underscore, Y)) -> if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_in_ga₂(X, Y))
if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_out_ga₂(X, Y)) -> s2l_2_out_ga₂(s_1₁(X), ._2₂(underscore, Y))
if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_in_ga₂(R, Rows))
if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_in_ggg₃(Pattern, Cols, Rows))
snake_3_in_ggg₃(Pattern, Cols, Rows) -> if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_in_gaa₃(Pattern, InfSnake, InfSnake))
infinite_snake_3_in_gaa₃([]_0, S, S) -> infinite_snake_3_out_gaa₃([]_0, S, S)
infinite_snake_3_in_gaa₃(._2₂(A, R), ._2₂(A, T), S) -> if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_in_gaa₃(R, T, S))
if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_out_gaa₃(R, T, S)) -> infinite_snake_3_out_gaa₃(._2₂(A, R), ._2₂(A, T), S)
if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, InfSnake, Snake))
produce_snake_4_in_ggaa₄([]_0, underscore1, underscore2, []_0) -> produce_snake_4_out_ggaa₄([]_0, underscore1, underscore2, []_0)
produce_snake_4_in_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_4_in_gaaa₄([]_0, RestSnake, RestSnake, []_0) -> part_of_snake_4_out_gaaa₄([]_0, RestSnake, RestSnake, []_0)
part_of_snake_4_in_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_in_gaaa₄(R, Rings, RestSnake, RestRings))
if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_out_gaaa₄(R, Rings, RestSnake, RestRings)) -> part_of_snake_4_out_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings))
if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, NewInfSnake, Tail))
if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, NewInfSnake, Tail)) -> produce_snake_4_out_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail))
if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_in_gg₂(Snake, odd_0))
coil_it_2_in_gg₂([]_0, underscore5) -> coil_it_2_out_gg₂([]_0, underscore5)
coil_it_2_in_gg₂(._2₂(Line, Lines), odd_0) -> if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, even_0))
coil_it_2_in_gg₂(._2₂(Line, Lines), even_0) -> if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))
reverse2_2_in_aa₂(List, Reversed) -> if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_in_aga₃(List, []_0, Reversed))
reverse_3_in_aga₃([]_0, Reversed, Reversed) -> reverse_3_out_aga₃([]_0, Reversed, Reversed)
reverse_3_in_aga₃(._2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, ._2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, ._2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(._2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, []_0, Reversed)) -> reverse2_2_out_aa₂(List, Reversed)
if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, odd_0))
if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, odd_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), even_0)
if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, even_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), odd_0)
if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_out_gg₂(Snake, odd_0)) -> snake_3_out_ggg₃(Pattern, Cols, Rows)
if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_out_ggg₃(Pattern, Cols, Rows)) -> test_snake_3_out_ggg₃(Pattern, C, R)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

COIL_IT_2_IN_GG₂(._2₂(Line, Lines), odd_0) -> COIL_IT_2_IN_GG₂(Lines, even_0)
IF_COIL_IT_2_IN_2_GG₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> COIL_IT_2_IN_GG₂(Lines, odd_0)
COIL_IT_2_IN_GG₂(._2₂(Line, Lines), even_0) -> IF_COIL_IT_2_IN_2_GG₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))

The TRS R consists of the following rules:

reverse2_2_in_aa₂(List, Reversed) -> if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_in_aga₃(List, []_0, Reversed))
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, []_0, Reversed)) -> reverse2_2_out_aa₂(List, Reversed)
reverse_3_in_aga₃([]_0, Reversed, Reversed) -> reverse_3_out_aga₃([]_0, Reversed, Reversed)
reverse_3_in_aga₃(._2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, ._2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, ._2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(._2₂(Head, Tail), SoFar, Reversed)

The argument filtering Pi contains the following mapping:
[]_0 = []_0
._2₂(x1, x2) = ._2₁(x2)
odd_0 = odd_0
even_0 = even_0
reverse2_2_in_aa₂(x1, x2) = reverse2_2_in_aa
if_reverse2_2_in_1_aa₃(x1, x2, x3) = if_reverse2_2_in_1_aa₁(x3)
reverse_3_in_aga₃(x1, x2, x3) = reverse_3_in_aga₁(x2)
reverse_3_out_aga₃(x1, x2, x3) = reverse_3_out_aga₂(x1, x3)
if_reverse_3_in_1_aga₅(x1, x2, x3, x4, x5) = if_reverse_3_in_1_aga₁(x5)
reverse2_2_out_aa₂(x1, x2) = reverse2_2_out_aa₂(x1, x2)
IF_COIL_IT_2_IN_2_GG₃(x1, x2, x3) = IF_COIL_IT_2_IN_2_GG₂(x2, x3)
COIL_IT_2_IN_GG₂(x1, x2) = COIL_IT_2_IN_GG₂(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

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

COIL_IT_2_IN_GG₂(._2₁(Lines), odd_0) -> COIL_IT_2_IN_GG₂(Lines, even_0)
IF_COIL_IT_2_IN_2_GG₂(Lines, reverse2_2_out_aa₂(Line, Line1)) -> COIL_IT_2_IN_GG₂(Lines, odd_0)
COIL_IT_2_IN_GG₂(._2₁(Lines), even_0) -> IF_COIL_IT_2_IN_2_GG₂(Lines, reverse2_2_in_aa)

The TRS R consists of the following rules:

reverse2_2_in_aa -> if_reverse2_2_in_1_aa₁(reverse_3_in_aga₁([]_0))
if_reverse2_2_in_1_aa₁(reverse_3_out_aga₂(List, Reversed)) -> reverse2_2_out_aa₂(List, Reversed)
reverse_3_in_aga₁(Reversed) -> reverse_3_out_aga₂([]_0, Reversed)
reverse_3_in_aga₁(SoFar) -> if_reverse_3_in_1_aga₁(reverse_3_in_aga₁(._2₁(SoFar)))
if_reverse_3_in_1_aga₁(reverse_3_out_aga₂(Tail, Reversed)) -> reverse_3_out_aga₂(._2₁(Tail), Reversed)

The set Q consists of the following terms:

reverse2_2_in_aa
if_reverse2_2_in_1_aa₁(x0)
reverse_3_in_aga₁(x0)
if_reverse_3_in_1_aga₁(x0)

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

COIL_IT_2_IN_GG₂(._2₁(Lines), even_0) -> IF_COIL_IT_2_IN_2_GG₂(Lines, reverse2_2_in_aa)
The graph contains the following edges 1 > 1
IF_COIL_IT_2_IN_2_GG₂(Lines, reverse2_2_out_aa₂(Line, Line1)) -> COIL_IT_2_IN_GG₂(Lines, odd_0)
The graph contains the following edges 1 >= 1
COIL_IT_2_IN_GG₂(._2₁(Lines), odd_0) -> COIL_IT_2_IN_GG₂(Lines, even_0)
The graph contains the following edges 1 > 1

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

PART_OF_SNAKE_4_IN_GAAA₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> PART_OF_SNAKE_4_IN_GAAA₄(R, Rings, RestSnake, RestRings)

The TRS R consists of the following rules:

test_snake_3_in_ggg₃(Pattern, C, R) -> if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_in_ga₂(C, Cols))
s2l_2_in_ga₂(0_0, []_0) -> s2l_2_out_ga₂(0_0, []_0)
s2l_2_in_ga₂(s_1₁(X), ._2₂(underscore, Y)) -> if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_in_ga₂(X, Y))
if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_out_ga₂(X, Y)) -> s2l_2_out_ga₂(s_1₁(X), ._2₂(underscore, Y))
if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_in_ga₂(R, Rows))
if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_in_ggg₃(Pattern, Cols, Rows))
snake_3_in_ggg₃(Pattern, Cols, Rows) -> if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_in_gaa₃(Pattern, InfSnake, InfSnake))
infinite_snake_3_in_gaa₃([]_0, S, S) -> infinite_snake_3_out_gaa₃([]_0, S, S)
infinite_snake_3_in_gaa₃(._2₂(A, R), ._2₂(A, T), S) -> if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_in_gaa₃(R, T, S))
if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_out_gaa₃(R, T, S)) -> infinite_snake_3_out_gaa₃(._2₂(A, R), ._2₂(A, T), S)
if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, InfSnake, Snake))
produce_snake_4_in_ggaa₄([]_0, underscore1, underscore2, []_0) -> produce_snake_4_out_ggaa₄([]_0, underscore1, underscore2, []_0)
produce_snake_4_in_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_4_in_gaaa₄([]_0, RestSnake, RestSnake, []_0) -> part_of_snake_4_out_gaaa₄([]_0, RestSnake, RestSnake, []_0)
part_of_snake_4_in_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_in_gaaa₄(R, Rings, RestSnake, RestRings))
if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_out_gaaa₄(R, Rings, RestSnake, RestRings)) -> part_of_snake_4_out_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings))
if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, NewInfSnake, Tail))
if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, NewInfSnake, Tail)) -> produce_snake_4_out_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail))
if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_in_gg₂(Snake, odd_0))
coil_it_2_in_gg₂([]_0, underscore5) -> coil_it_2_out_gg₂([]_0, underscore5)
coil_it_2_in_gg₂(._2₂(Line, Lines), odd_0) -> if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, even_0))
coil_it_2_in_gg₂(._2₂(Line, Lines), even_0) -> if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))
reverse2_2_in_aa₂(List, Reversed) -> if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_in_aga₃(List, []_0, Reversed))
reverse_3_in_aga₃([]_0, Reversed, Reversed) -> reverse_3_out_aga₃([]_0, Reversed, Reversed)
reverse_3_in_aga₃(._2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, ._2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, ._2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(._2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, []_0, Reversed)) -> reverse2_2_out_aa₂(List, Reversed)
if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, odd_0))
if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, odd_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), even_0)
if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, even_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), odd_0)
if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_out_gg₂(Snake, odd_0)) -> snake_3_out_ggg₃(Pattern, Cols, Rows)
if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_out_ggg₃(Pattern, Cols, Rows)) -> test_snake_3_out_ggg₃(Pattern, C, R)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

PART_OF_SNAKE_4_IN_GAAA₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> PART_OF_SNAKE_4_IN_GAAA₄(R, Rings, RestSnake, RestRings)

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

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

PART_OF_SNAKE_4_IN_GAAA₁(._2₁(R)) -> PART_OF_SNAKE_4_IN_GAAA₁(R)

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

PART_OF_SNAKE_4_IN_GAAA₁(._2₁(R)) -> PART_OF_SNAKE_4_IN_GAAA₁(R)
The graph contains the following edges 1 > 1

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

PRODUCE_SNAKE_4_IN_GGAA₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> IF_PRODUCE_SNAKE_4_IN_1_GGAA₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
IF_PRODUCE_SNAKE_4_IN_1_GGAA₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> PRODUCE_SNAKE_4_IN_GGAA₄(Rows, Cols, NewInfSnake, Tail)

The TRS R consists of the following rules:

test_snake_3_in_ggg₃(Pattern, C, R) -> if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_in_ga₂(C, Cols))
s2l_2_in_ga₂(0_0, []_0) -> s2l_2_out_ga₂(0_0, []_0)
s2l_2_in_ga₂(s_1₁(X), ._2₂(underscore, Y)) -> if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_in_ga₂(X, Y))
if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_out_ga₂(X, Y)) -> s2l_2_out_ga₂(s_1₁(X), ._2₂(underscore, Y))
if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_in_ga₂(R, Rows))
if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_in_ggg₃(Pattern, Cols, Rows))
snake_3_in_ggg₃(Pattern, Cols, Rows) -> if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_in_gaa₃(Pattern, InfSnake, InfSnake))
infinite_snake_3_in_gaa₃([]_0, S, S) -> infinite_snake_3_out_gaa₃([]_0, S, S)
infinite_snake_3_in_gaa₃(._2₂(A, R), ._2₂(A, T), S) -> if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_in_gaa₃(R, T, S))
if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_out_gaa₃(R, T, S)) -> infinite_snake_3_out_gaa₃(._2₂(A, R), ._2₂(A, T), S)
if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, InfSnake, Snake))
produce_snake_4_in_ggaa₄([]_0, underscore1, underscore2, []_0) -> produce_snake_4_out_ggaa₄([]_0, underscore1, underscore2, []_0)
produce_snake_4_in_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_4_in_gaaa₄([]_0, RestSnake, RestSnake, []_0) -> part_of_snake_4_out_gaaa₄([]_0, RestSnake, RestSnake, []_0)
part_of_snake_4_in_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_in_gaaa₄(R, Rings, RestSnake, RestRings))
if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_out_gaaa₄(R, Rings, RestSnake, RestRings)) -> part_of_snake_4_out_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings))
if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, NewInfSnake, Tail))
if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, NewInfSnake, Tail)) -> produce_snake_4_out_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail))
if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_in_gg₂(Snake, odd_0))
coil_it_2_in_gg₂([]_0, underscore5) -> coil_it_2_out_gg₂([]_0, underscore5)
coil_it_2_in_gg₂(._2₂(Line, Lines), odd_0) -> if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, even_0))
coil_it_2_in_gg₂(._2₂(Line, Lines), even_0) -> if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))
reverse2_2_in_aa₂(List, Reversed) -> if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_in_aga₃(List, []_0, Reversed))
reverse_3_in_aga₃([]_0, Reversed, Reversed) -> reverse_3_out_aga₃([]_0, Reversed, Reversed)
reverse_3_in_aga₃(._2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, ._2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, ._2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(._2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, []_0, Reversed)) -> reverse2_2_out_aa₂(List, Reversed)
if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, odd_0))
if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, odd_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), even_0)
if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, even_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), odd_0)
if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_out_gg₂(Snake, odd_0)) -> snake_3_out_ggg₃(Pattern, Cols, Rows)
if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_out_ggg₃(Pattern, Cols, Rows)) -> test_snake_3_out_ggg₃(Pattern, C, R)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

PRODUCE_SNAKE_4_IN_GGAA₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> IF_PRODUCE_SNAKE_4_IN_1_GGAA₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
IF_PRODUCE_SNAKE_4_IN_1_GGAA₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> PRODUCE_SNAKE_4_IN_GGAA₄(Rows, Cols, NewInfSnake, Tail)

The TRS R consists of the following rules:

part_of_snake_4_in_gaaa₄([]_0, RestSnake, RestSnake, []_0) -> part_of_snake_4_out_gaaa₄([]_0, RestSnake, RestSnake, []_0)
part_of_snake_4_in_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_in_gaaa₄(R, Rings, RestSnake, RestRings))
if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_out_gaaa₄(R, Rings, RestSnake, RestRings)) -> part_of_snake_4_out_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings))

The argument filtering Pi contains the following mapping:
[]_0 = []_0
._2₂(x1, x2) = ._2₁(x2)
part_of_snake_4_in_gaaa₄(x1, x2, x3, x4) = part_of_snake_4_in_gaaa₁(x1)
part_of_snake_4_out_gaaa₄(x1, x2, x3, x4) = part_of_snake_4_out_gaaa₁(x4)
if_part_of_snake_4_in_1_gaaa₇(x1, x2, x3, x4, x5, x6, x7) = if_part_of_snake_4_in_1_gaaa₁(x7)
IF_PRODUCE_SNAKE_4_IN_1_GGAA₇(x1, x2, x3, x4, x5, x6, x7) = IF_PRODUCE_SNAKE_4_IN_1_GGAA₃(x2, x3, x7)
PRODUCE_SNAKE_4_IN_GGAA₄(x1, x2, x3, x4) = PRODUCE_SNAKE_4_IN_GGAA₂(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

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

PRODUCE_SNAKE_4_IN_GGAA₂(._2₁(Rows), Cols) -> IF_PRODUCE_SNAKE_4_IN_1_GGAA₃(Rows, Cols, part_of_snake_4_in_gaaa₁(Cols))
IF_PRODUCE_SNAKE_4_IN_1_GGAA₃(Rows, Cols, part_of_snake_4_out_gaaa₁(Part)) -> PRODUCE_SNAKE_4_IN_GGAA₂(Rows, Cols)

The TRS R consists of the following rules:

part_of_snake_4_in_gaaa₁([]_0) -> part_of_snake_4_out_gaaa₁([]_0)
part_of_snake_4_in_gaaa₁(._2₁(R)) -> if_part_of_snake_4_in_1_gaaa₁(part_of_snake_4_in_gaaa₁(R))
if_part_of_snake_4_in_1_gaaa₁(part_of_snake_4_out_gaaa₁(RestRings)) -> part_of_snake_4_out_gaaa₁(._2₁(RestRings))

The set Q consists of the following terms:

part_of_snake_4_in_gaaa₁(x0)
if_part_of_snake_4_in_1_gaaa₁(x0)

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

IF_PRODUCE_SNAKE_4_IN_1_GGAA₃(Rows, Cols, part_of_snake_4_out_gaaa₁(Part)) -> PRODUCE_SNAKE_4_IN_GGAA₂(Rows, Cols)
The graph contains the following edges 1 >= 1, 2 >= 2
PRODUCE_SNAKE_4_IN_GGAA₂(._2₁(Rows), Cols) -> IF_PRODUCE_SNAKE_4_IN_1_GGAA₃(Rows, Cols, part_of_snake_4_in_gaaa₁(Cols))
The graph contains the following edges 1 > 1, 2 >= 2

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

INFINITE_SNAKE_3_IN_GAA₃(._2₂(A, R), ._2₂(A, T), S) -> INFINITE_SNAKE_3_IN_GAA₃(R, T, S)

The TRS R consists of the following rules:

test_snake_3_in_ggg₃(Pattern, C, R) -> if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_in_ga₂(C, Cols))
s2l_2_in_ga₂(0_0, []_0) -> s2l_2_out_ga₂(0_0, []_0)
s2l_2_in_ga₂(s_1₁(X), ._2₂(underscore, Y)) -> if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_in_ga₂(X, Y))
if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_out_ga₂(X, Y)) -> s2l_2_out_ga₂(s_1₁(X), ._2₂(underscore, Y))
if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_in_ga₂(R, Rows))
if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_in_ggg₃(Pattern, Cols, Rows))
snake_3_in_ggg₃(Pattern, Cols, Rows) -> if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_in_gaa₃(Pattern, InfSnake, InfSnake))
infinite_snake_3_in_gaa₃([]_0, S, S) -> infinite_snake_3_out_gaa₃([]_0, S, S)
infinite_snake_3_in_gaa₃(._2₂(A, R), ._2₂(A, T), S) -> if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_in_gaa₃(R, T, S))
if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_out_gaa₃(R, T, S)) -> infinite_snake_3_out_gaa₃(._2₂(A, R), ._2₂(A, T), S)
if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, InfSnake, Snake))
produce_snake_4_in_ggaa₄([]_0, underscore1, underscore2, []_0) -> produce_snake_4_out_ggaa₄([]_0, underscore1, underscore2, []_0)
produce_snake_4_in_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_4_in_gaaa₄([]_0, RestSnake, RestSnake, []_0) -> part_of_snake_4_out_gaaa₄([]_0, RestSnake, RestSnake, []_0)
part_of_snake_4_in_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_in_gaaa₄(R, Rings, RestSnake, RestRings))
if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_out_gaaa₄(R, Rings, RestSnake, RestRings)) -> part_of_snake_4_out_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings))
if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, NewInfSnake, Tail))
if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, NewInfSnake, Tail)) -> produce_snake_4_out_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail))
if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_in_gg₂(Snake, odd_0))
coil_it_2_in_gg₂([]_0, underscore5) -> coil_it_2_out_gg₂([]_0, underscore5)
coil_it_2_in_gg₂(._2₂(Line, Lines), odd_0) -> if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, even_0))
coil_it_2_in_gg₂(._2₂(Line, Lines), even_0) -> if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))
reverse2_2_in_aa₂(List, Reversed) -> if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_in_aga₃(List, []_0, Reversed))
reverse_3_in_aga₃([]_0, Reversed, Reversed) -> reverse_3_out_aga₃([]_0, Reversed, Reversed)
reverse_3_in_aga₃(._2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, ._2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, ._2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(._2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, []_0, Reversed)) -> reverse2_2_out_aa₂(List, Reversed)
if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, odd_0))
if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, odd_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), even_0)
if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, even_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), odd_0)
if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_out_gg₂(Snake, odd_0)) -> snake_3_out_ggg₃(Pattern, Cols, Rows)
if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_out_ggg₃(Pattern, Cols, Rows)) -> test_snake_3_out_ggg₃(Pattern, C, R)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

INFINITE_SNAKE_3_IN_GAA₃(._2₂(A, R), ._2₂(A, T), S) -> INFINITE_SNAKE_3_IN_GAA₃(R, T, S)

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

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

  ↳ PrologToPiTRSProof

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

INFINITE_SNAKE_3_IN_GAA₁(._2₁(R)) -> INFINITE_SNAKE_3_IN_GAA₁(R)

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

INFINITE_SNAKE_3_IN_GAA₁(._2₁(R)) -> INFINITE_SNAKE_3_IN_GAA₁(R)
The graph contains the following edges 1 > 1

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

  ↳ PrologToPiTRSProof

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

S2L_2_IN_GA₂(s_1₁(X), ._2₂(underscore, Y)) -> S2L_2_IN_GA₂(X, Y)

The TRS R consists of the following rules:

test_snake_3_in_ggg₃(Pattern, C, R) -> if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_in_ga₂(C, Cols))
s2l_2_in_ga₂(0_0, []_0) -> s2l_2_out_ga₂(0_0, []_0)
s2l_2_in_ga₂(s_1₁(X), ._2₂(underscore, Y)) -> if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_in_ga₂(X, Y))
if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_out_ga₂(X, Y)) -> s2l_2_out_ga₂(s_1₁(X), ._2₂(underscore, Y))
if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_in_ga₂(R, Rows))
if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_in_ggg₃(Pattern, Cols, Rows))
snake_3_in_ggg₃(Pattern, Cols, Rows) -> if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_in_gaa₃(Pattern, InfSnake, InfSnake))
infinite_snake_3_in_gaa₃([]_0, S, S) -> infinite_snake_3_out_gaa₃([]_0, S, S)
infinite_snake_3_in_gaa₃(._2₂(A, R), ._2₂(A, T), S) -> if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_in_gaa₃(R, T, S))
if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_out_gaa₃(R, T, S)) -> infinite_snake_3_out_gaa₃(._2₂(A, R), ._2₂(A, T), S)
if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, InfSnake, Snake))
produce_snake_4_in_ggaa₄([]_0, underscore1, underscore2, []_0) -> produce_snake_4_out_ggaa₄([]_0, underscore1, underscore2, []_0)
produce_snake_4_in_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_4_in_gaaa₄([]_0, RestSnake, RestSnake, []_0) -> part_of_snake_4_out_gaaa₄([]_0, RestSnake, RestSnake, []_0)
part_of_snake_4_in_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_in_gaaa₄(R, Rings, RestSnake, RestRings))
if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_out_gaaa₄(R, Rings, RestSnake, RestRings)) -> part_of_snake_4_out_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings))
if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, NewInfSnake, Tail))
if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, NewInfSnake, Tail)) -> produce_snake_4_out_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail))
if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_in_gg₂(Snake, odd_0))
coil_it_2_in_gg₂([]_0, underscore5) -> coil_it_2_out_gg₂([]_0, underscore5)
coil_it_2_in_gg₂(._2₂(Line, Lines), odd_0) -> if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, even_0))
coil_it_2_in_gg₂(._2₂(Line, Lines), even_0) -> if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))
reverse2_2_in_aa₂(List, Reversed) -> if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_in_aga₃(List, []_0, Reversed))
reverse_3_in_aga₃([]_0, Reversed, Reversed) -> reverse_3_out_aga₃([]_0, Reversed, Reversed)
reverse_3_in_aga₃(._2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, ._2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, ._2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(._2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, []_0, Reversed)) -> reverse2_2_out_aa₂(List, Reversed)
if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, odd_0))
if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, odd_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), even_0)
if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, even_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), odd_0)
if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_out_gg₂(Snake, odd_0)) -> snake_3_out_ggg₃(Pattern, Cols, Rows)
if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_out_ggg₃(Pattern, Cols, Rows)) -> test_snake_3_out_ggg₃(Pattern, C, R)

↳ PROLOG

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

  ↳ PrologToPiTRSProof

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

S2L_2_IN_GA₂(s_1₁(X), ._2₂(underscore, Y)) -> S2L_2_IN_GA₂(X, Y)

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

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

  ↳ PrologToPiTRSProof

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

S2L_2_IN_GA₁(s_1₁(X)) -> S2L_2_IN_GA₁(X)

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

S2L_2_IN_GA₁(s_1₁(X)) -> S2L_2_IN_GA₁(X)
The graph contains the following edges 1 > 1

test_snake_3_in_ggg₃(Pattern, C, R) -> if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_in_ga₂(C, Cols))
s2l_2_in_ga₂(0_0, []_0) -> s2l_2_out_ga₂(0_0, []_0)
s2l_2_in_ga₂(s_1₁(X), ._2₂(underscore, Y)) -> if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_in_ga₂(X, Y))
if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_out_ga₂(X, Y)) -> s2l_2_out_ga₂(s_1₁(X), ._2₂(underscore, Y))
if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_in_ga₂(R, Rows))
if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_in_ggg₃(Pattern, Cols, Rows))
snake_3_in_ggg₃(Pattern, Cols, Rows) -> if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_in_gaa₃(Pattern, InfSnake, InfSnake))
infinite_snake_3_in_gaa₃([]_0, S, S) -> infinite_snake_3_out_gaa₃([]_0, S, S)
infinite_snake_3_in_gaa₃(._2₂(A, R), ._2₂(A, T), S) -> if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_in_gaa₃(R, T, S))
if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_out_gaa₃(R, T, S)) -> infinite_snake_3_out_gaa₃(._2₂(A, R), ._2₂(A, T), S)
if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, InfSnake, Snake))
produce_snake_4_in_ggaa₄([]_0, underscore1, underscore2, []_0) -> produce_snake_4_out_ggaa₄([]_0, underscore1, underscore2, []_0)
produce_snake_4_in_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_4_in_gaaa₄([]_0, RestSnake, RestSnake, []_0) -> part_of_snake_4_out_gaaa₄([]_0, RestSnake, RestSnake, []_0)
part_of_snake_4_in_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_in_gaaa₄(R, Rings, RestSnake, RestRings))
if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_out_gaaa₄(R, Rings, RestSnake, RestRings)) -> part_of_snake_4_out_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings))
if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, NewInfSnake, Tail))
if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, NewInfSnake, Tail)) -> produce_snake_4_out_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail))
if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_in_gg₂(Snake, odd_0))
coil_it_2_in_gg₂([]_0, underscore5) -> coil_it_2_out_gg₂([]_0, underscore5)
coil_it_2_in_gg₂(._2₂(Line, Lines), odd_0) -> if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, even_0))
coil_it_2_in_gg₂(._2₂(Line, Lines), even_0) -> if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))
reverse2_2_in_aa₂(List, Reversed) -> if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_in_aga₃(List, []_0, Reversed))
reverse_3_in_aga₃([]_0, Reversed, Reversed) -> reverse_3_out_aga₃([]_0, Reversed, Reversed)
reverse_3_in_aga₃(._2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, ._2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, ._2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(._2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, []_0, Reversed)) -> reverse2_2_out_aa₂(List, Reversed)
if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, odd_0))
if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, odd_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), even_0)
if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, even_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), odd_0)
if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_out_gg₂(Snake, odd_0)) -> snake_3_out_ggg₃(Pattern, Cols, Rows)
if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_out_ggg₃(Pattern, Cols, Rows)) -> test_snake_3_out_ggg₃(Pattern, C, R)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

test_snake_3_in_ggg₃(Pattern, C, R) -> if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_in_ga₂(C, Cols))
s2l_2_in_ga₂(0_0, []_0) -> s2l_2_out_ga₂(0_0, []_0)
s2l_2_in_ga₂(s_1₁(X), ._2₂(underscore, Y)) -> if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_in_ga₂(X, Y))
if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_out_ga₂(X, Y)) -> s2l_2_out_ga₂(s_1₁(X), ._2₂(underscore, Y))
if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_in_ga₂(R, Rows))
if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_in_ggg₃(Pattern, Cols, Rows))
snake_3_in_ggg₃(Pattern, Cols, Rows) -> if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_in_gaa₃(Pattern, InfSnake, InfSnake))
infinite_snake_3_in_gaa₃([]_0, S, S) -> infinite_snake_3_out_gaa₃([]_0, S, S)
infinite_snake_3_in_gaa₃(._2₂(A, R), ._2₂(A, T), S) -> if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_in_gaa₃(R, T, S))
if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_out_gaa₃(R, T, S)) -> infinite_snake_3_out_gaa₃(._2₂(A, R), ._2₂(A, T), S)
if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, InfSnake, Snake))
produce_snake_4_in_ggaa₄([]_0, underscore1, underscore2, []_0) -> produce_snake_4_out_ggaa₄([]_0, underscore1, underscore2, []_0)
produce_snake_4_in_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_4_in_gaaa₄([]_0, RestSnake, RestSnake, []_0) -> part_of_snake_4_out_gaaa₄([]_0, RestSnake, RestSnake, []_0)
part_of_snake_4_in_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_in_gaaa₄(R, Rings, RestSnake, RestRings))
if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_out_gaaa₄(R, Rings, RestSnake, RestRings)) -> part_of_snake_4_out_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings))
if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, NewInfSnake, Tail))
if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, NewInfSnake, Tail)) -> produce_snake_4_out_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail))
if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_in_gg₂(Snake, odd_0))
coil_it_2_in_gg₂([]_0, underscore5) -> coil_it_2_out_gg₂([]_0, underscore5)
coil_it_2_in_gg₂(._2₂(Line, Lines), odd_0) -> if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, even_0))
coil_it_2_in_gg₂(._2₂(Line, Lines), even_0) -> if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))
reverse2_2_in_aa₂(List, Reversed) -> if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_in_aga₃(List, []_0, Reversed))
reverse_3_in_aga₃([]_0, Reversed, Reversed) -> reverse_3_out_aga₃([]_0, Reversed, Reversed)
reverse_3_in_aga₃(._2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, ._2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, ._2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(._2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, []_0, Reversed)) -> reverse2_2_out_aa₂(List, Reversed)
if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, odd_0))
if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, odd_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), even_0)
if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, even_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), odd_0)
if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_out_gg₂(Snake, odd_0)) -> snake_3_out_ggg₃(Pattern, Cols, Rows)
if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_out_ggg₃(Pattern, Cols, Rows)) -> test_snake_3_out_ggg₃(Pattern, C, R)

TEST_SNAKE_3_IN_GGG₃(Pattern, C, R) -> IF_TEST_SNAKE_3_IN_1_GGG₄(Pattern, C, R, s2l_2_in_ga₂(C, Cols))
TEST_SNAKE_3_IN_GGG₃(Pattern, C, R) -> S2L_2_IN_GA₂(C, Cols)
S2L_2_IN_GA₂(s_1₁(X), ._2₂(underscore, Y)) -> IF_S2L_2_IN_1_GA₄(X, underscore, Y, s2l_2_in_ga₂(X, Y))
S2L_2_IN_GA₂(s_1₁(X), ._2₂(underscore, Y)) -> S2L_2_IN_GA₂(X, Y)
IF_TEST_SNAKE_3_IN_1_GGG₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> IF_TEST_SNAKE_3_IN_2_GGG₅(Pattern, C, R, Cols, s2l_2_in_ga₂(R, Rows))
IF_TEST_SNAKE_3_IN_1_GGG₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> S2L_2_IN_GA₂(R, Rows)
IF_TEST_SNAKE_3_IN_2_GGG₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> IF_TEST_SNAKE_3_IN_3_GGG₆(Pattern, C, R, Cols, Rows, snake_3_in_ggg₃(Pattern, Cols, Rows))
IF_TEST_SNAKE_3_IN_2_GGG₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> SNAKE_3_IN_GGG₃(Pattern, Cols, Rows)
SNAKE_3_IN_GGG₃(Pattern, Cols, Rows) -> IF_SNAKE_3_IN_1_GGG₄(Pattern, Cols, Rows, infinite_snake_3_in_gaa₃(Pattern, InfSnake, InfSnake))
SNAKE_3_IN_GGG₃(Pattern, Cols, Rows) -> INFINITE_SNAKE_3_IN_GAA₃(Pattern, InfSnake, InfSnake)
INFINITE_SNAKE_3_IN_GAA₃(._2₂(A, R), ._2₂(A, T), S) -> IF_INFINITE_SNAKE_3_IN_1_GAA₅(A, R, T, S, infinite_snake_3_in_gaa₃(R, T, S))
INFINITE_SNAKE_3_IN_GAA₃(._2₂(A, R), ._2₂(A, T), S) -> INFINITE_SNAKE_3_IN_GAA₃(R, T, S)
IF_SNAKE_3_IN_1_GGG₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> IF_SNAKE_3_IN_2_GGG₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, InfSnake, Snake))
IF_SNAKE_3_IN_1_GGG₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> PRODUCE_SNAKE_4_IN_GGAA₄(Rows, Cols, InfSnake, Snake)
PRODUCE_SNAKE_4_IN_GGAA₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> IF_PRODUCE_SNAKE_4_IN_1_GGAA₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
PRODUCE_SNAKE_4_IN_GGAA₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> PART_OF_SNAKE_4_IN_GAAA₄(Cols, InfSnake, NewInfSnake, Part)
PART_OF_SNAKE_4_IN_GAAA₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> IF_PART_OF_SNAKE_4_IN_1_GAAA₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_in_gaaa₄(R, Rings, RestSnake, RestRings))
PART_OF_SNAKE_4_IN_GAAA₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> PART_OF_SNAKE_4_IN_GAAA₄(R, Rings, RestSnake, RestRings)
IF_PRODUCE_SNAKE_4_IN_1_GGAA₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> IF_PRODUCE_SNAKE_4_IN_2_GGAA₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, NewInfSnake, Tail))
IF_PRODUCE_SNAKE_4_IN_1_GGAA₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> PRODUCE_SNAKE_4_IN_GGAA₄(Rows, Cols, NewInfSnake, Tail)
IF_SNAKE_3_IN_2_GGG₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> IF_SNAKE_3_IN_3_GGG₅(Pattern, Cols, Rows, Snake, coil_it_2_in_gg₂(Snake, odd_0))
IF_SNAKE_3_IN_2_GGG₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> COIL_IT_2_IN_GG₂(Snake, odd_0)
COIL_IT_2_IN_GG₂(._2₂(Line, Lines), odd_0) -> IF_COIL_IT_2_IN_1_GG₃(Line, Lines, coil_it_2_in_gg₂(Lines, even_0))
COIL_IT_2_IN_GG₂(._2₂(Line, Lines), odd_0) -> COIL_IT_2_IN_GG₂(Lines, even_0)
COIL_IT_2_IN_GG₂(._2₂(Line, Lines), even_0) -> IF_COIL_IT_2_IN_2_GG₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))
COIL_IT_2_IN_GG₂(._2₂(Line, Lines), even_0) -> REVERSE2_2_IN_AA₂(Line, Line1)
REVERSE2_2_IN_AA₂(List, Reversed) -> IF_REVERSE2_2_IN_1_AA₃(List, Reversed, reverse_3_in_aga₃(List, []_0, Reversed))
REVERSE2_2_IN_AA₂(List, Reversed) -> REVERSE_3_IN_AGA₃(List, []_0, Reversed)
REVERSE_3_IN_AGA₃(._2₂(Head, Tail), SoFar, Reversed) -> IF_REVERSE_3_IN_1_AGA₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, ._2₂(Head, SoFar), Reversed))
REVERSE_3_IN_AGA₃(._2₂(Head, Tail), SoFar, Reversed) -> REVERSE_3_IN_AGA₃(Tail, ._2₂(Head, SoFar), Reversed)
IF_COIL_IT_2_IN_2_GG₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> IF_COIL_IT_2_IN_3_GG₃(Line, Lines, coil_it_2_in_gg₂(Lines, odd_0))
IF_COIL_IT_2_IN_2_GG₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> COIL_IT_2_IN_GG₂(Lines, odd_0)

The TRS R consists of the following rules:

test_snake_3_in_ggg₃(Pattern, C, R) -> if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_in_ga₂(C, Cols))
s2l_2_in_ga₂(0_0, []_0) -> s2l_2_out_ga₂(0_0, []_0)
s2l_2_in_ga₂(s_1₁(X), ._2₂(underscore, Y)) -> if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_in_ga₂(X, Y))
if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_out_ga₂(X, Y)) -> s2l_2_out_ga₂(s_1₁(X), ._2₂(underscore, Y))
if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_in_ga₂(R, Rows))
if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_in_ggg₃(Pattern, Cols, Rows))
snake_3_in_ggg₃(Pattern, Cols, Rows) -> if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_in_gaa₃(Pattern, InfSnake, InfSnake))
infinite_snake_3_in_gaa₃([]_0, S, S) -> infinite_snake_3_out_gaa₃([]_0, S, S)
infinite_snake_3_in_gaa₃(._2₂(A, R), ._2₂(A, T), S) -> if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_in_gaa₃(R, T, S))
if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_out_gaa₃(R, T, S)) -> infinite_snake_3_out_gaa₃(._2₂(A, R), ._2₂(A, T), S)
if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, InfSnake, Snake))
produce_snake_4_in_ggaa₄([]_0, underscore1, underscore2, []_0) -> produce_snake_4_out_ggaa₄([]_0, underscore1, underscore2, []_0)
produce_snake_4_in_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_4_in_gaaa₄([]_0, RestSnake, RestSnake, []_0) -> part_of_snake_4_out_gaaa₄([]_0, RestSnake, RestSnake, []_0)
part_of_snake_4_in_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_in_gaaa₄(R, Rings, RestSnake, RestRings))
if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_out_gaaa₄(R, Rings, RestSnake, RestRings)) -> part_of_snake_4_out_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings))
if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, NewInfSnake, Tail))
if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, NewInfSnake, Tail)) -> produce_snake_4_out_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail))
if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_in_gg₂(Snake, odd_0))
coil_it_2_in_gg₂([]_0, underscore5) -> coil_it_2_out_gg₂([]_0, underscore5)
coil_it_2_in_gg₂(._2₂(Line, Lines), odd_0) -> if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, even_0))
coil_it_2_in_gg₂(._2₂(Line, Lines), even_0) -> if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))
reverse2_2_in_aa₂(List, Reversed) -> if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_in_aga₃(List, []_0, Reversed))
reverse_3_in_aga₃([]_0, Reversed, Reversed) -> reverse_3_out_aga₃([]_0, Reversed, Reversed)
reverse_3_in_aga₃(._2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, ._2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, ._2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(._2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, []_0, Reversed)) -> reverse2_2_out_aa₂(List, Reversed)
if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, odd_0))
if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, odd_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), even_0)
if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, even_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), odd_0)
if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_out_gg₂(Snake, odd_0)) -> snake_3_out_ggg₃(Pattern, Cols, Rows)
if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_out_ggg₃(Pattern, Cols, Rows)) -> test_snake_3_out_ggg₃(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_3_in_ggg₃(x1, x2, x3) = test_snake_3_in_ggg₃(x1, x2, x3)
0_0 = 0_0
[]_0 = []_0
s_1₁(x1) = s_1₁(x1)
._2₂(x1, x2) = ._2₁(x2)
odd_0 = odd_0
even_0 = even_0
if_test_snake_3_in_1_ggg₄(x1, x2, x3, x4) = if_test_snake_3_in_1_ggg₄(x1, x2, x3, x4)
s2l_2_in_ga₂(x1, x2) = s2l_2_in_ga₁(x1)
s2l_2_out_ga₂(x1, x2) = s2l_2_out_ga₂(x1, x2)
if_s2l_2_in_1_ga₄(x1, x2, x3, x4) = if_s2l_2_in_1_ga₂(x1, x4)
if_test_snake_3_in_2_ggg₅(x1, x2, x3, x4, x5) = if_test_snake_3_in_2_ggg₅(x1, x2, x3, x4, x5)
if_test_snake_3_in_3_ggg₆(x1, x2, x3, x4, x5, x6) = if_test_snake_3_in_3_ggg₄(x1, x2, x3, x6)
snake_3_in_ggg₃(x1, x2, x3) = snake_3_in_ggg₃(x1, x2, x3)
if_snake_3_in_1_ggg₄(x1, x2, x3, x4) = if_snake_3_in_1_ggg₄(x1, x2, x3, x4)
infinite_snake_3_in_gaa₃(x1, x2, x3) = infinite_snake_3_in_gaa₁(x1)
infinite_snake_3_out_gaa₃(x1, x2, x3) = infinite_snake_3_out_gaa₁(x1)
if_infinite_snake_3_in_1_gaa₅(x1, x2, x3, x4, x5) = if_infinite_snake_3_in_1_gaa₂(x2, x5)
if_snake_3_in_2_ggg₅(x1, x2, x3, x4, x5) = if_snake_3_in_2_ggg₄(x1, x2, x3, x5)
produce_snake_4_in_ggaa₄(x1, x2, x3, x4) = produce_snake_4_in_ggaa₂(x1, x2)
produce_snake_4_out_ggaa₄(x1, x2, x3, x4) = produce_snake_4_out_ggaa₃(x1, x2, x4)
if_produce_snake_4_in_1_ggaa₇(x1, x2, x3, x4, x5, x6, x7) = if_produce_snake_4_in_1_ggaa₃(x2, x3, x7)
part_of_snake_4_in_gaaa₄(x1, x2, x3, x4) = part_of_snake_4_in_gaaa₁(x1)
part_of_snake_4_out_gaaa₄(x1, x2, x3, x4) = part_of_snake_4_out_gaaa₂(x1, x4)
if_part_of_snake_4_in_1_gaaa₇(x1, x2, x3, x4, x5, x6, x7) = if_part_of_snake_4_in_1_gaaa₂(x2, x7)
if_produce_snake_4_in_2_ggaa₈(x1, x2, x3, x4, x5, x6, x7, x8) = if_produce_snake_4_in_2_ggaa₃(x2, x3, x8)
if_snake_3_in_3_ggg₅(x1, x2, x3, x4, x5) = if_snake_3_in_3_ggg₄(x1, x2, x3, x5)
coil_it_2_in_gg₂(x1, x2) = coil_it_2_in_gg₂(x1, x2)
coil_it_2_out_gg₂(x1, x2) = coil_it_2_out_gg₂(x1, x2)
if_coil_it_2_in_1_gg₃(x1, x2, x3) = if_coil_it_2_in_1_gg₂(x2, x3)
if_coil_it_2_in_2_gg₃(x1, x2, x3) = if_coil_it_2_in_2_gg₂(x2, x3)
reverse2_2_in_aa₂(x1, x2) = reverse2_2_in_aa
if_reverse2_2_in_1_aa₃(x1, x2, x3) = if_reverse2_2_in_1_aa₁(x3)
reverse_3_in_aga₃(x1, x2, x3) = reverse_3_in_aga₁(x2)
reverse_3_out_aga₃(x1, x2, x3) = reverse_3_out_aga₃(x1, x2, x3)
if_reverse_3_in_1_aga₅(x1, x2, x3, x4, x5) = if_reverse_3_in_1_aga₂(x3, x5)
reverse2_2_out_aa₂(x1, x2) = reverse2_2_out_aa₂(x1, x2)
if_coil_it_2_in_3_gg₃(x1, x2, x3) = if_coil_it_2_in_3_gg₂(x2, x3)
snake_3_out_ggg₃(x1, x2, x3) = snake_3_out_ggg₃(x1, x2, x3)
test_snake_3_out_ggg₃(x1, x2, x3) = test_snake_3_out_ggg₃(x1, x2, x3)
TEST_SNAKE_3_IN_GGG₃(x1, x2, x3) = TEST_SNAKE_3_IN_GGG₃(x1, x2, x3)
IF_COIL_IT_2_IN_1_GG₃(x1, x2, x3) = IF_COIL_IT_2_IN_1_GG₂(x2, x3)
IF_REVERSE2_2_IN_1_AA₃(x1, x2, x3) = IF_REVERSE2_2_IN_1_AA₁(x3)
IF_PRODUCE_SNAKE_4_IN_1_GGAA₇(x1, x2, x3, x4, x5, x6, x7) = IF_PRODUCE_SNAKE_4_IN_1_GGAA₃(x2, x3, x7)
IF_REVERSE_3_IN_1_AGA₅(x1, x2, x3, x4, x5) = IF_REVERSE_3_IN_1_AGA₂(x3, x5)
IF_INFINITE_SNAKE_3_IN_1_GAA₅(x1, x2, x3, x4, x5) = IF_INFINITE_SNAKE_3_IN_1_GAA₂(x2, x5)
IF_SNAKE_3_IN_3_GGG₅(x1, x2, x3, x4, x5) = IF_SNAKE_3_IN_3_GGG₄(x1, x2, x3, x5)
S2L_2_IN_GA₂(x1, x2) = S2L_2_IN_GA₁(x1)
IF_TEST_SNAKE_3_IN_3_GGG₆(x1, x2, x3, x4, x5, x6) = IF_TEST_SNAKE_3_IN_3_GGG₄(x1, x2, x3, x6)
IF_COIL_IT_2_IN_2_GG₃(x1, x2, x3) = IF_COIL_IT_2_IN_2_GG₂(x2, x3)
IF_TEST_SNAKE_3_IN_2_GGG₅(x1, x2, x3, x4, x5) = IF_TEST_SNAKE_3_IN_2_GGG₅(x1, x2, x3, x4, x5)
PRODUCE_SNAKE_4_IN_GGAA₄(x1, x2, x3, x4) = PRODUCE_SNAKE_4_IN_GGAA₂(x1, x2)
IF_COIL_IT_2_IN_3_GG₃(x1, x2, x3) = IF_COIL_IT_2_IN_3_GG₂(x2, x3)
IF_PART_OF_SNAKE_4_IN_1_GAAA₇(x1, x2, x3, x4, x5, x6, x7) = IF_PART_OF_SNAKE_4_IN_1_GAAA₂(x2, x7)
REVERSE_3_IN_AGA₃(x1, x2, x3) = REVERSE_3_IN_AGA₁(x2)
IF_PRODUCE_SNAKE_4_IN_2_GGAA₈(x1, x2, x3, x4, x5, x6, x7, x8) = IF_PRODUCE_SNAKE_4_IN_2_GGAA₃(x2, x3, x8)
INFINITE_SNAKE_3_IN_GAA₃(x1, x2, x3) = INFINITE_SNAKE_3_IN_GAA₁(x1)
COIL_IT_2_IN_GG₂(x1, x2) = COIL_IT_2_IN_GG₂(x1, x2)
REVERSE2_2_IN_AA₂(x1, x2) = REVERSE2_2_IN_AA
IF_TEST_SNAKE_3_IN_1_GGG₄(x1, x2, x3, x4) = IF_TEST_SNAKE_3_IN_1_GGG₄(x1, x2, x3, x4)
PART_OF_SNAKE_4_IN_GAAA₄(x1, x2, x3, x4) = PART_OF_SNAKE_4_IN_GAAA₁(x1)
IF_S2L_2_IN_1_GA₄(x1, x2, x3, x4) = IF_S2L_2_IN_1_GA₂(x1, x4)
IF_SNAKE_3_IN_1_GGG₄(x1, x2, x3, x4) = IF_SNAKE_3_IN_1_GGG₄(x1, x2, x3, x4)
SNAKE_3_IN_GGG₃(x1, x2, x3) = SNAKE_3_IN_GGG₃(x1, x2, x3)
IF_SNAKE_3_IN_2_GGG₅(x1, x2, x3, x4, x5) = IF_SNAKE_3_IN_2_GGG₄(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

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

TEST_SNAKE_3_IN_GGG₃(Pattern, C, R) -> IF_TEST_SNAKE_3_IN_1_GGG₄(Pattern, C, R, s2l_2_in_ga₂(C, Cols))
TEST_SNAKE_3_IN_GGG₃(Pattern, C, R) -> S2L_2_IN_GA₂(C, Cols)
S2L_2_IN_GA₂(s_1₁(X), ._2₂(underscore, Y)) -> IF_S2L_2_IN_1_GA₄(X, underscore, Y, s2l_2_in_ga₂(X, Y))
S2L_2_IN_GA₂(s_1₁(X), ._2₂(underscore, Y)) -> S2L_2_IN_GA₂(X, Y)
IF_TEST_SNAKE_3_IN_1_GGG₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> IF_TEST_SNAKE_3_IN_2_GGG₅(Pattern, C, R, Cols, s2l_2_in_ga₂(R, Rows))
IF_TEST_SNAKE_3_IN_1_GGG₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> S2L_2_IN_GA₂(R, Rows)
IF_TEST_SNAKE_3_IN_2_GGG₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> IF_TEST_SNAKE_3_IN_3_GGG₆(Pattern, C, R, Cols, Rows, snake_3_in_ggg₃(Pattern, Cols, Rows))
IF_TEST_SNAKE_3_IN_2_GGG₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> SNAKE_3_IN_GGG₃(Pattern, Cols, Rows)
SNAKE_3_IN_GGG₃(Pattern, Cols, Rows) -> IF_SNAKE_3_IN_1_GGG₄(Pattern, Cols, Rows, infinite_snake_3_in_gaa₃(Pattern, InfSnake, InfSnake))
SNAKE_3_IN_GGG₃(Pattern, Cols, Rows) -> INFINITE_SNAKE_3_IN_GAA₃(Pattern, InfSnake, InfSnake)
INFINITE_SNAKE_3_IN_GAA₃(._2₂(A, R), ._2₂(A, T), S) -> IF_INFINITE_SNAKE_3_IN_1_GAA₅(A, R, T, S, infinite_snake_3_in_gaa₃(R, T, S))
INFINITE_SNAKE_3_IN_GAA₃(._2₂(A, R), ._2₂(A, T), S) -> INFINITE_SNAKE_3_IN_GAA₃(R, T, S)
IF_SNAKE_3_IN_1_GGG₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> IF_SNAKE_3_IN_2_GGG₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, InfSnake, Snake))
IF_SNAKE_3_IN_1_GGG₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> PRODUCE_SNAKE_4_IN_GGAA₄(Rows, Cols, InfSnake, Snake)
PRODUCE_SNAKE_4_IN_GGAA₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> IF_PRODUCE_SNAKE_4_IN_1_GGAA₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
PRODUCE_SNAKE_4_IN_GGAA₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> PART_OF_SNAKE_4_IN_GAAA₄(Cols, InfSnake, NewInfSnake, Part)
PART_OF_SNAKE_4_IN_GAAA₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> IF_PART_OF_SNAKE_4_IN_1_GAAA₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_in_gaaa₄(R, Rings, RestSnake, RestRings))
PART_OF_SNAKE_4_IN_GAAA₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> PART_OF_SNAKE_4_IN_GAAA₄(R, Rings, RestSnake, RestRings)
IF_PRODUCE_SNAKE_4_IN_1_GGAA₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> IF_PRODUCE_SNAKE_4_IN_2_GGAA₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, NewInfSnake, Tail))
IF_PRODUCE_SNAKE_4_IN_1_GGAA₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> PRODUCE_SNAKE_4_IN_GGAA₄(Rows, Cols, NewInfSnake, Tail)
IF_SNAKE_3_IN_2_GGG₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> IF_SNAKE_3_IN_3_GGG₅(Pattern, Cols, Rows, Snake, coil_it_2_in_gg₂(Snake, odd_0))
IF_SNAKE_3_IN_2_GGG₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> COIL_IT_2_IN_GG₂(Snake, odd_0)
COIL_IT_2_IN_GG₂(._2₂(Line, Lines), odd_0) -> IF_COIL_IT_2_IN_1_GG₃(Line, Lines, coil_it_2_in_gg₂(Lines, even_0))
COIL_IT_2_IN_GG₂(._2₂(Line, Lines), odd_0) -> COIL_IT_2_IN_GG₂(Lines, even_0)
COIL_IT_2_IN_GG₂(._2₂(Line, Lines), even_0) -> IF_COIL_IT_2_IN_2_GG₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))
COIL_IT_2_IN_GG₂(._2₂(Line, Lines), even_0) -> REVERSE2_2_IN_AA₂(Line, Line1)
REVERSE2_2_IN_AA₂(List, Reversed) -> IF_REVERSE2_2_IN_1_AA₃(List, Reversed, reverse_3_in_aga₃(List, []_0, Reversed))
REVERSE2_2_IN_AA₂(List, Reversed) -> REVERSE_3_IN_AGA₃(List, []_0, Reversed)
REVERSE_3_IN_AGA₃(._2₂(Head, Tail), SoFar, Reversed) -> IF_REVERSE_3_IN_1_AGA₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, ._2₂(Head, SoFar), Reversed))
REVERSE_3_IN_AGA₃(._2₂(Head, Tail), SoFar, Reversed) -> REVERSE_3_IN_AGA₃(Tail, ._2₂(Head, SoFar), Reversed)
IF_COIL_IT_2_IN_2_GG₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> IF_COIL_IT_2_IN_3_GG₃(Line, Lines, coil_it_2_in_gg₂(Lines, odd_0))
IF_COIL_IT_2_IN_2_GG₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> COIL_IT_2_IN_GG₂(Lines, odd_0)

The TRS R consists of the following rules:

test_snake_3_in_ggg₃(Pattern, C, R) -> if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_in_ga₂(C, Cols))
s2l_2_in_ga₂(0_0, []_0) -> s2l_2_out_ga₂(0_0, []_0)
s2l_2_in_ga₂(s_1₁(X), ._2₂(underscore, Y)) -> if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_in_ga₂(X, Y))
if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_out_ga₂(X, Y)) -> s2l_2_out_ga₂(s_1₁(X), ._2₂(underscore, Y))
if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_in_ga₂(R, Rows))
if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_in_ggg₃(Pattern, Cols, Rows))
snake_3_in_ggg₃(Pattern, Cols, Rows) -> if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_in_gaa₃(Pattern, InfSnake, InfSnake))
infinite_snake_3_in_gaa₃([]_0, S, S) -> infinite_snake_3_out_gaa₃([]_0, S, S)
infinite_snake_3_in_gaa₃(._2₂(A, R), ._2₂(A, T), S) -> if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_in_gaa₃(R, T, S))
if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_out_gaa₃(R, T, S)) -> infinite_snake_3_out_gaa₃(._2₂(A, R), ._2₂(A, T), S)
if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, InfSnake, Snake))
produce_snake_4_in_ggaa₄([]_0, underscore1, underscore2, []_0) -> produce_snake_4_out_ggaa₄([]_0, underscore1, underscore2, []_0)
produce_snake_4_in_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_4_in_gaaa₄([]_0, RestSnake, RestSnake, []_0) -> part_of_snake_4_out_gaaa₄([]_0, RestSnake, RestSnake, []_0)
part_of_snake_4_in_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_in_gaaa₄(R, Rings, RestSnake, RestRings))
if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_out_gaaa₄(R, Rings, RestSnake, RestRings)) -> part_of_snake_4_out_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings))
if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, NewInfSnake, Tail))
if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, NewInfSnake, Tail)) -> produce_snake_4_out_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail))
if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_in_gg₂(Snake, odd_0))
coil_it_2_in_gg₂([]_0, underscore5) -> coil_it_2_out_gg₂([]_0, underscore5)
coil_it_2_in_gg₂(._2₂(Line, Lines), odd_0) -> if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, even_0))
coil_it_2_in_gg₂(._2₂(Line, Lines), even_0) -> if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))
reverse2_2_in_aa₂(List, Reversed) -> if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_in_aga₃(List, []_0, Reversed))
reverse_3_in_aga₃([]_0, Reversed, Reversed) -> reverse_3_out_aga₃([]_0, Reversed, Reversed)
reverse_3_in_aga₃(._2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, ._2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, ._2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(._2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, []_0, Reversed)) -> reverse2_2_out_aa₂(List, Reversed)
if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, odd_0))
if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, odd_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), even_0)
if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, even_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), odd_0)
if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_out_gg₂(Snake, odd_0)) -> snake_3_out_ggg₃(Pattern, Cols, Rows)
if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_out_ggg₃(Pattern, Cols, Rows)) -> test_snake_3_out_ggg₃(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_3_in_ggg₃(x1, x2, x3) = test_snake_3_in_ggg₃(x1, x2, x3)
0_0 = 0_0
[]_0 = []_0
s_1₁(x1) = s_1₁(x1)
._2₂(x1, x2) = ._2₁(x2)
odd_0 = odd_0
even_0 = even_0
if_test_snake_3_in_1_ggg₄(x1, x2, x3, x4) = if_test_snake_3_in_1_ggg₄(x1, x2, x3, x4)
s2l_2_in_ga₂(x1, x2) = s2l_2_in_ga₁(x1)
s2l_2_out_ga₂(x1, x2) = s2l_2_out_ga₂(x1, x2)
if_s2l_2_in_1_ga₄(x1, x2, x3, x4) = if_s2l_2_in_1_ga₂(x1, x4)
if_test_snake_3_in_2_ggg₅(x1, x2, x3, x4, x5) = if_test_snake_3_in_2_ggg₅(x1, x2, x3, x4, x5)
if_test_snake_3_in_3_ggg₆(x1, x2, x3, x4, x5, x6) = if_test_snake_3_in_3_ggg₄(x1, x2, x3, x6)
snake_3_in_ggg₃(x1, x2, x3) = snake_3_in_ggg₃(x1, x2, x3)
if_snake_3_in_1_ggg₄(x1, x2, x3, x4) = if_snake_3_in_1_ggg₄(x1, x2, x3, x4)
infinite_snake_3_in_gaa₃(x1, x2, x3) = infinite_snake_3_in_gaa₁(x1)
infinite_snake_3_out_gaa₃(x1, x2, x3) = infinite_snake_3_out_gaa₁(x1)
if_infinite_snake_3_in_1_gaa₅(x1, x2, x3, x4, x5) = if_infinite_snake_3_in_1_gaa₂(x2, x5)
if_snake_3_in_2_ggg₅(x1, x2, x3, x4, x5) = if_snake_3_in_2_ggg₄(x1, x2, x3, x5)
produce_snake_4_in_ggaa₄(x1, x2, x3, x4) = produce_snake_4_in_ggaa₂(x1, x2)
produce_snake_4_out_ggaa₄(x1, x2, x3, x4) = produce_snake_4_out_ggaa₃(x1, x2, x4)
if_produce_snake_4_in_1_ggaa₇(x1, x2, x3, x4, x5, x6, x7) = if_produce_snake_4_in_1_ggaa₃(x2, x3, x7)
part_of_snake_4_in_gaaa₄(x1, x2, x3, x4) = part_of_snake_4_in_gaaa₁(x1)
part_of_snake_4_out_gaaa₄(x1, x2, x3, x4) = part_of_snake_4_out_gaaa₂(x1, x4)
if_part_of_snake_4_in_1_gaaa₇(x1, x2, x3, x4, x5, x6, x7) = if_part_of_snake_4_in_1_gaaa₂(x2, x7)
if_produce_snake_4_in_2_ggaa₈(x1, x2, x3, x4, x5, x6, x7, x8) = if_produce_snake_4_in_2_ggaa₃(x2, x3, x8)
if_snake_3_in_3_ggg₅(x1, x2, x3, x4, x5) = if_snake_3_in_3_ggg₄(x1, x2, x3, x5)
coil_it_2_in_gg₂(x1, x2) = coil_it_2_in_gg₂(x1, x2)
coil_it_2_out_gg₂(x1, x2) = coil_it_2_out_gg₂(x1, x2)
if_coil_it_2_in_1_gg₃(x1, x2, x3) = if_coil_it_2_in_1_gg₂(x2, x3)
if_coil_it_2_in_2_gg₃(x1, x2, x3) = if_coil_it_2_in_2_gg₂(x2, x3)
reverse2_2_in_aa₂(x1, x2) = reverse2_2_in_aa
if_reverse2_2_in_1_aa₃(x1, x2, x3) = if_reverse2_2_in_1_aa₁(x3)
reverse_3_in_aga₃(x1, x2, x3) = reverse_3_in_aga₁(x2)
reverse_3_out_aga₃(x1, x2, x3) = reverse_3_out_aga₃(x1, x2, x3)
if_reverse_3_in_1_aga₅(x1, x2, x3, x4, x5) = if_reverse_3_in_1_aga₂(x3, x5)
reverse2_2_out_aa₂(x1, x2) = reverse2_2_out_aa₂(x1, x2)
if_coil_it_2_in_3_gg₃(x1, x2, x3) = if_coil_it_2_in_3_gg₂(x2, x3)
snake_3_out_ggg₃(x1, x2, x3) = snake_3_out_ggg₃(x1, x2, x3)
test_snake_3_out_ggg₃(x1, x2, x3) = test_snake_3_out_ggg₃(x1, x2, x3)
TEST_SNAKE_3_IN_GGG₃(x1, x2, x3) = TEST_SNAKE_3_IN_GGG₃(x1, x2, x3)
IF_COIL_IT_2_IN_1_GG₃(x1, x2, x3) = IF_COIL_IT_2_IN_1_GG₂(x2, x3)
IF_REVERSE2_2_IN_1_AA₃(x1, x2, x3) = IF_REVERSE2_2_IN_1_AA₁(x3)
IF_PRODUCE_SNAKE_4_IN_1_GGAA₇(x1, x2, x3, x4, x5, x6, x7) = IF_PRODUCE_SNAKE_4_IN_1_GGAA₃(x2, x3, x7)
IF_REVERSE_3_IN_1_AGA₅(x1, x2, x3, x4, x5) = IF_REVERSE_3_IN_1_AGA₂(x3, x5)
IF_INFINITE_SNAKE_3_IN_1_GAA₅(x1, x2, x3, x4, x5) = IF_INFINITE_SNAKE_3_IN_1_GAA₂(x2, x5)
IF_SNAKE_3_IN_3_GGG₅(x1, x2, x3, x4, x5) = IF_SNAKE_3_IN_3_GGG₄(x1, x2, x3, x5)
S2L_2_IN_GA₂(x1, x2) = S2L_2_IN_GA₁(x1)
IF_TEST_SNAKE_3_IN_3_GGG₆(x1, x2, x3, x4, x5, x6) = IF_TEST_SNAKE_3_IN_3_GGG₄(x1, x2, x3, x6)
IF_COIL_IT_2_IN_2_GG₃(x1, x2, x3) = IF_COIL_IT_2_IN_2_GG₂(x2, x3)
IF_TEST_SNAKE_3_IN_2_GGG₅(x1, x2, x3, x4, x5) = IF_TEST_SNAKE_3_IN_2_GGG₅(x1, x2, x3, x4, x5)
PRODUCE_SNAKE_4_IN_GGAA₄(x1, x2, x3, x4) = PRODUCE_SNAKE_4_IN_GGAA₂(x1, x2)
IF_COIL_IT_2_IN_3_GG₃(x1, x2, x3) = IF_COIL_IT_2_IN_3_GG₂(x2, x3)
IF_PART_OF_SNAKE_4_IN_1_GAAA₇(x1, x2, x3, x4, x5, x6, x7) = IF_PART_OF_SNAKE_4_IN_1_GAAA₂(x2, x7)
REVERSE_3_IN_AGA₃(x1, x2, x3) = REVERSE_3_IN_AGA₁(x2)
IF_PRODUCE_SNAKE_4_IN_2_GGAA₈(x1, x2, x3, x4, x5, x6, x7, x8) = IF_PRODUCE_SNAKE_4_IN_2_GGAA₃(x2, x3, x8)
INFINITE_SNAKE_3_IN_GAA₃(x1, x2, x3) = INFINITE_SNAKE_3_IN_GAA₁(x1)
COIL_IT_2_IN_GG₂(x1, x2) = COIL_IT_2_IN_GG₂(x1, x2)
REVERSE2_2_IN_AA₂(x1, x2) = REVERSE2_2_IN_AA
IF_TEST_SNAKE_3_IN_1_GGG₄(x1, x2, x3, x4) = IF_TEST_SNAKE_3_IN_1_GGG₄(x1, x2, x3, x4)
PART_OF_SNAKE_4_IN_GAAA₄(x1, x2, x3, x4) = PART_OF_SNAKE_4_IN_GAAA₁(x1)
IF_S2L_2_IN_1_GA₄(x1, x2, x3, x4) = IF_S2L_2_IN_1_GA₂(x1, x4)
IF_SNAKE_3_IN_1_GGG₄(x1, x2, x3, x4) = IF_SNAKE_3_IN_1_GGG₄(x1, x2, x3, x4)
SNAKE_3_IN_GGG₃(x1, x2, x3) = SNAKE_3_IN_GGG₃(x1, x2, x3)
IF_SNAKE_3_IN_2_GGG₅(x1, x2, x3, x4, x5) = IF_SNAKE_3_IN_2_GGG₄(x1, x2, x3, x5)

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

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

REVERSE_3_IN_AGA₃(._2₂(Head, Tail), SoFar, Reversed) -> REVERSE_3_IN_AGA₃(Tail, ._2₂(Head, SoFar), Reversed)

The TRS R consists of the following rules:

test_snake_3_in_ggg₃(Pattern, C, R) -> if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_in_ga₂(C, Cols))
s2l_2_in_ga₂(0_0, []_0) -> s2l_2_out_ga₂(0_0, []_0)
s2l_2_in_ga₂(s_1₁(X), ._2₂(underscore, Y)) -> if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_in_ga₂(X, Y))
if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_out_ga₂(X, Y)) -> s2l_2_out_ga₂(s_1₁(X), ._2₂(underscore, Y))
if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_in_ga₂(R, Rows))
if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_in_ggg₃(Pattern, Cols, Rows))
snake_3_in_ggg₃(Pattern, Cols, Rows) -> if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_in_gaa₃(Pattern, InfSnake, InfSnake))
infinite_snake_3_in_gaa₃([]_0, S, S) -> infinite_snake_3_out_gaa₃([]_0, S, S)
infinite_snake_3_in_gaa₃(._2₂(A, R), ._2₂(A, T), S) -> if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_in_gaa₃(R, T, S))
if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_out_gaa₃(R, T, S)) -> infinite_snake_3_out_gaa₃(._2₂(A, R), ._2₂(A, T), S)
if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, InfSnake, Snake))
produce_snake_4_in_ggaa₄([]_0, underscore1, underscore2, []_0) -> produce_snake_4_out_ggaa₄([]_0, underscore1, underscore2, []_0)
produce_snake_4_in_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_4_in_gaaa₄([]_0, RestSnake, RestSnake, []_0) -> part_of_snake_4_out_gaaa₄([]_0, RestSnake, RestSnake, []_0)
part_of_snake_4_in_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_in_gaaa₄(R, Rings, RestSnake, RestRings))
if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_out_gaaa₄(R, Rings, RestSnake, RestRings)) -> part_of_snake_4_out_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings))
if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, NewInfSnake, Tail))
if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, NewInfSnake, Tail)) -> produce_snake_4_out_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail))
if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_in_gg₂(Snake, odd_0))
coil_it_2_in_gg₂([]_0, underscore5) -> coil_it_2_out_gg₂([]_0, underscore5)
coil_it_2_in_gg₂(._2₂(Line, Lines), odd_0) -> if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, even_0))
coil_it_2_in_gg₂(._2₂(Line, Lines), even_0) -> if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))
reverse2_2_in_aa₂(List, Reversed) -> if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_in_aga₃(List, []_0, Reversed))
reverse_3_in_aga₃([]_0, Reversed, Reversed) -> reverse_3_out_aga₃([]_0, Reversed, Reversed)
reverse_3_in_aga₃(._2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, ._2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, ._2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(._2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, []_0, Reversed)) -> reverse2_2_out_aa₂(List, Reversed)
if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, odd_0))
if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, odd_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), even_0)
if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, even_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), odd_0)
if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_out_gg₂(Snake, odd_0)) -> snake_3_out_ggg₃(Pattern, Cols, Rows)
if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_out_ggg₃(Pattern, Cols, Rows)) -> test_snake_3_out_ggg₃(Pattern, C, R)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

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

REVERSE_3_IN_AGA₃(._2₂(Head, Tail), SoFar, Reversed) -> REVERSE_3_IN_AGA₃(Tail, ._2₂(Head, SoFar), Reversed)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

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

REVERSE_3_IN_AGA₁(SoFar) -> REVERSE_3_IN_AGA₁(._2₁(SoFar))

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_AGA₁}.

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

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

COIL_IT_2_IN_GG₂(._2₂(Line, Lines), odd_0) -> COIL_IT_2_IN_GG₂(Lines, even_0)
IF_COIL_IT_2_IN_2_GG₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> COIL_IT_2_IN_GG₂(Lines, odd_0)
COIL_IT_2_IN_GG₂(._2₂(Line, Lines), even_0) -> IF_COIL_IT_2_IN_2_GG₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))

The TRS R consists of the following rules:

test_snake_3_in_ggg₃(Pattern, C, R) -> if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_in_ga₂(C, Cols))
s2l_2_in_ga₂(0_0, []_0) -> s2l_2_out_ga₂(0_0, []_0)
s2l_2_in_ga₂(s_1₁(X), ._2₂(underscore, Y)) -> if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_in_ga₂(X, Y))
if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_out_ga₂(X, Y)) -> s2l_2_out_ga₂(s_1₁(X), ._2₂(underscore, Y))
if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_in_ga₂(R, Rows))
if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_in_ggg₃(Pattern, Cols, Rows))
snake_3_in_ggg₃(Pattern, Cols, Rows) -> if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_in_gaa₃(Pattern, InfSnake, InfSnake))
infinite_snake_3_in_gaa₃([]_0, S, S) -> infinite_snake_3_out_gaa₃([]_0, S, S)
infinite_snake_3_in_gaa₃(._2₂(A, R), ._2₂(A, T), S) -> if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_in_gaa₃(R, T, S))
if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_out_gaa₃(R, T, S)) -> infinite_snake_3_out_gaa₃(._2₂(A, R), ._2₂(A, T), S)
if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, InfSnake, Snake))
produce_snake_4_in_ggaa₄([]_0, underscore1, underscore2, []_0) -> produce_snake_4_out_ggaa₄([]_0, underscore1, underscore2, []_0)
produce_snake_4_in_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_4_in_gaaa₄([]_0, RestSnake, RestSnake, []_0) -> part_of_snake_4_out_gaaa₄([]_0, RestSnake, RestSnake, []_0)
part_of_snake_4_in_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_in_gaaa₄(R, Rings, RestSnake, RestRings))
if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_out_gaaa₄(R, Rings, RestSnake, RestRings)) -> part_of_snake_4_out_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings))
if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, NewInfSnake, Tail))
if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, NewInfSnake, Tail)) -> produce_snake_4_out_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail))
if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_in_gg₂(Snake, odd_0))
coil_it_2_in_gg₂([]_0, underscore5) -> coil_it_2_out_gg₂([]_0, underscore5)
coil_it_2_in_gg₂(._2₂(Line, Lines), odd_0) -> if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, even_0))
coil_it_2_in_gg₂(._2₂(Line, Lines), even_0) -> if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))
reverse2_2_in_aa₂(List, Reversed) -> if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_in_aga₃(List, []_0, Reversed))
reverse_3_in_aga₃([]_0, Reversed, Reversed) -> reverse_3_out_aga₃([]_0, Reversed, Reversed)
reverse_3_in_aga₃(._2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, ._2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, ._2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(._2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, []_0, Reversed)) -> reverse2_2_out_aa₂(List, Reversed)
if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, odd_0))
if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, odd_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), even_0)
if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, even_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), odd_0)
if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_out_gg₂(Snake, odd_0)) -> snake_3_out_ggg₃(Pattern, Cols, Rows)
if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_out_ggg₃(Pattern, Cols, Rows)) -> test_snake_3_out_ggg₃(Pattern, C, R)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

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

COIL_IT_2_IN_GG₂(._2₂(Line, Lines), odd_0) -> COIL_IT_2_IN_GG₂(Lines, even_0)
IF_COIL_IT_2_IN_2_GG₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> COIL_IT_2_IN_GG₂(Lines, odd_0)
COIL_IT_2_IN_GG₂(._2₂(Line, Lines), even_0) -> IF_COIL_IT_2_IN_2_GG₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))

The TRS R consists of the following rules:

reverse2_2_in_aa₂(List, Reversed) -> if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_in_aga₃(List, []_0, Reversed))
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, []_0, Reversed)) -> reverse2_2_out_aa₂(List, Reversed)
reverse_3_in_aga₃([]_0, Reversed, Reversed) -> reverse_3_out_aga₃([]_0, Reversed, Reversed)
reverse_3_in_aga₃(._2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, ._2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, ._2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(._2₂(Head, Tail), SoFar, Reversed)

The argument filtering Pi contains the following mapping:
[]_0 = []_0
._2₂(x1, x2) = ._2₁(x2)
odd_0 = odd_0
even_0 = even_0
reverse2_2_in_aa₂(x1, x2) = reverse2_2_in_aa
if_reverse2_2_in_1_aa₃(x1, x2, x3) = if_reverse2_2_in_1_aa₁(x3)
reverse_3_in_aga₃(x1, x2, x3) = reverse_3_in_aga₁(x2)
reverse_3_out_aga₃(x1, x2, x3) = reverse_3_out_aga₃(x1, x2, x3)
if_reverse_3_in_1_aga₅(x1, x2, x3, x4, x5) = if_reverse_3_in_1_aga₂(x3, x5)
reverse2_2_out_aa₂(x1, x2) = reverse2_2_out_aa₂(x1, x2)
IF_COIL_IT_2_IN_2_GG₃(x1, x2, x3) = IF_COIL_IT_2_IN_2_GG₂(x2, x3)
COIL_IT_2_IN_GG₂(x1, x2) = COIL_IT_2_IN_GG₂(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

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

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

COIL_IT_2_IN_GG₂(._2₁(Lines), odd_0) -> COIL_IT_2_IN_GG₂(Lines, even_0)
IF_COIL_IT_2_IN_2_GG₂(Lines, reverse2_2_out_aa₂(Line, Line1)) -> COIL_IT_2_IN_GG₂(Lines, odd_0)
COIL_IT_2_IN_GG₂(._2₁(Lines), even_0) -> IF_COIL_IT_2_IN_2_GG₂(Lines, reverse2_2_in_aa)

The TRS R consists of the following rules:

reverse2_2_in_aa -> if_reverse2_2_in_1_aa₁(reverse_3_in_aga₁([]_0))
if_reverse2_2_in_1_aa₁(reverse_3_out_aga₃(List, []_0, Reversed)) -> reverse2_2_out_aa₂(List, Reversed)
reverse_3_in_aga₁(Reversed) -> reverse_3_out_aga₃([]_0, Reversed, Reversed)
reverse_3_in_aga₁(SoFar) -> if_reverse_3_in_1_aga₂(SoFar, reverse_3_in_aga₁(._2₁(SoFar)))
if_reverse_3_in_1_aga₂(SoFar, reverse_3_out_aga₃(Tail, ._2₁(SoFar), Reversed)) -> reverse_3_out_aga₃(._2₁(Tail), SoFar, Reversed)

The set Q consists of the following terms:

reverse2_2_in_aa
if_reverse2_2_in_1_aa₁(x0)
reverse_3_in_aga₁(x0)
if_reverse_3_in_1_aga₂(x0, x1)

From the DPs we obtained the following set of size-change graphs:

COIL_IT_2_IN_GG₂(._2₁(Lines), even_0) -> IF_COIL_IT_2_IN_2_GG₂(Lines, reverse2_2_in_aa)
The graph contains the following edges 1 > 1
IF_COIL_IT_2_IN_2_GG₂(Lines, reverse2_2_out_aa₂(Line, Line1)) -> COIL_IT_2_IN_GG₂(Lines, odd_0)
The graph contains the following edges 1 >= 1
COIL_IT_2_IN_GG₂(._2₁(Lines), odd_0) -> COIL_IT_2_IN_GG₂(Lines, even_0)
The graph contains the following edges 1 > 1

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

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

PART_OF_SNAKE_4_IN_GAAA₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> PART_OF_SNAKE_4_IN_GAAA₄(R, Rings, RestSnake, RestRings)

The TRS R consists of the following rules:

test_snake_3_in_ggg₃(Pattern, C, R) -> if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_in_ga₂(C, Cols))
s2l_2_in_ga₂(0_0, []_0) -> s2l_2_out_ga₂(0_0, []_0)
s2l_2_in_ga₂(s_1₁(X), ._2₂(underscore, Y)) -> if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_in_ga₂(X, Y))
if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_out_ga₂(X, Y)) -> s2l_2_out_ga₂(s_1₁(X), ._2₂(underscore, Y))
if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_in_ga₂(R, Rows))
if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_in_ggg₃(Pattern, Cols, Rows))
snake_3_in_ggg₃(Pattern, Cols, Rows) -> if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_in_gaa₃(Pattern, InfSnake, InfSnake))
infinite_snake_3_in_gaa₃([]_0, S, S) -> infinite_snake_3_out_gaa₃([]_0, S, S)
infinite_snake_3_in_gaa₃(._2₂(A, R), ._2₂(A, T), S) -> if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_in_gaa₃(R, T, S))
if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_out_gaa₃(R, T, S)) -> infinite_snake_3_out_gaa₃(._2₂(A, R), ._2₂(A, T), S)
if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, InfSnake, Snake))
produce_snake_4_in_ggaa₄([]_0, underscore1, underscore2, []_0) -> produce_snake_4_out_ggaa₄([]_0, underscore1, underscore2, []_0)
produce_snake_4_in_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_4_in_gaaa₄([]_0, RestSnake, RestSnake, []_0) -> part_of_snake_4_out_gaaa₄([]_0, RestSnake, RestSnake, []_0)
part_of_snake_4_in_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_in_gaaa₄(R, Rings, RestSnake, RestRings))
if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_out_gaaa₄(R, Rings, RestSnake, RestRings)) -> part_of_snake_4_out_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings))
if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, NewInfSnake, Tail))
if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, NewInfSnake, Tail)) -> produce_snake_4_out_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail))
if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_in_gg₂(Snake, odd_0))
coil_it_2_in_gg₂([]_0, underscore5) -> coil_it_2_out_gg₂([]_0, underscore5)
coil_it_2_in_gg₂(._2₂(Line, Lines), odd_0) -> if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, even_0))
coil_it_2_in_gg₂(._2₂(Line, Lines), even_0) -> if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))
reverse2_2_in_aa₂(List, Reversed) -> if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_in_aga₃(List, []_0, Reversed))
reverse_3_in_aga₃([]_0, Reversed, Reversed) -> reverse_3_out_aga₃([]_0, Reversed, Reversed)
reverse_3_in_aga₃(._2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, ._2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, ._2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(._2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, []_0, Reversed)) -> reverse2_2_out_aa₂(List, Reversed)
if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, odd_0))
if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, odd_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), even_0)
if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, even_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), odd_0)
if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_out_gg₂(Snake, odd_0)) -> snake_3_out_ggg₃(Pattern, Cols, Rows)
if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_out_ggg₃(Pattern, Cols, Rows)) -> test_snake_3_out_ggg₃(Pattern, C, R)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

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

PART_OF_SNAKE_4_IN_GAAA₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> PART_OF_SNAKE_4_IN_GAAA₄(R, Rings, RestSnake, RestRings)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

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

PART_OF_SNAKE_4_IN_GAAA₁(._2₁(R)) -> PART_OF_SNAKE_4_IN_GAAA₁(R)

From the DPs we obtained the following set of size-change graphs:

PART_OF_SNAKE_4_IN_GAAA₁(._2₁(R)) -> PART_OF_SNAKE_4_IN_GAAA₁(R)
The graph contains the following edges 1 > 1

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

              ↳ PiDP

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

PRODUCE_SNAKE_4_IN_GGAA₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> IF_PRODUCE_SNAKE_4_IN_1_GGAA₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
IF_PRODUCE_SNAKE_4_IN_1_GGAA₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> PRODUCE_SNAKE_4_IN_GGAA₄(Rows, Cols, NewInfSnake, Tail)

The TRS R consists of the following rules:

test_snake_3_in_ggg₃(Pattern, C, R) -> if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_in_ga₂(C, Cols))
s2l_2_in_ga₂(0_0, []_0) -> s2l_2_out_ga₂(0_0, []_0)
s2l_2_in_ga₂(s_1₁(X), ._2₂(underscore, Y)) -> if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_in_ga₂(X, Y))
if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_out_ga₂(X, Y)) -> s2l_2_out_ga₂(s_1₁(X), ._2₂(underscore, Y))
if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_in_ga₂(R, Rows))
if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_in_ggg₃(Pattern, Cols, Rows))
snake_3_in_ggg₃(Pattern, Cols, Rows) -> if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_in_gaa₃(Pattern, InfSnake, InfSnake))
infinite_snake_3_in_gaa₃([]_0, S, S) -> infinite_snake_3_out_gaa₃([]_0, S, S)
infinite_snake_3_in_gaa₃(._2₂(A, R), ._2₂(A, T), S) -> if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_in_gaa₃(R, T, S))
if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_out_gaa₃(R, T, S)) -> infinite_snake_3_out_gaa₃(._2₂(A, R), ._2₂(A, T), S)
if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, InfSnake, Snake))
produce_snake_4_in_ggaa₄([]_0, underscore1, underscore2, []_0) -> produce_snake_4_out_ggaa₄([]_0, underscore1, underscore2, []_0)
produce_snake_4_in_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_4_in_gaaa₄([]_0, RestSnake, RestSnake, []_0) -> part_of_snake_4_out_gaaa₄([]_0, RestSnake, RestSnake, []_0)
part_of_snake_4_in_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_in_gaaa₄(R, Rings, RestSnake, RestRings))
if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_out_gaaa₄(R, Rings, RestSnake, RestRings)) -> part_of_snake_4_out_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings))
if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, NewInfSnake, Tail))
if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, NewInfSnake, Tail)) -> produce_snake_4_out_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail))
if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_in_gg₂(Snake, odd_0))
coil_it_2_in_gg₂([]_0, underscore5) -> coil_it_2_out_gg₂([]_0, underscore5)
coil_it_2_in_gg₂(._2₂(Line, Lines), odd_0) -> if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, even_0))
coil_it_2_in_gg₂(._2₂(Line, Lines), even_0) -> if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))
reverse2_2_in_aa₂(List, Reversed) -> if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_in_aga₃(List, []_0, Reversed))
reverse_3_in_aga₃([]_0, Reversed, Reversed) -> reverse_3_out_aga₃([]_0, Reversed, Reversed)
reverse_3_in_aga₃(._2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, ._2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, ._2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(._2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, []_0, Reversed)) -> reverse2_2_out_aa₂(List, Reversed)
if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, odd_0))
if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, odd_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), even_0)
if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, even_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), odd_0)
if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_out_gg₂(Snake, odd_0)) -> snake_3_out_ggg₃(Pattern, Cols, Rows)
if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_out_ggg₃(Pattern, Cols, Rows)) -> test_snake_3_out_ggg₃(Pattern, C, R)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

              ↳ PiDP

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

PRODUCE_SNAKE_4_IN_GGAA₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> IF_PRODUCE_SNAKE_4_IN_1_GGAA₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
IF_PRODUCE_SNAKE_4_IN_1_GGAA₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> PRODUCE_SNAKE_4_IN_GGAA₄(Rows, Cols, NewInfSnake, Tail)

The TRS R consists of the following rules:

part_of_snake_4_in_gaaa₄([]_0, RestSnake, RestSnake, []_0) -> part_of_snake_4_out_gaaa₄([]_0, RestSnake, RestSnake, []_0)
part_of_snake_4_in_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_in_gaaa₄(R, Rings, RestSnake, RestRings))
if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_out_gaaa₄(R, Rings, RestSnake, RestRings)) -> part_of_snake_4_out_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings))

The argument filtering Pi contains the following mapping:
[]_0 = []_0
._2₂(x1, x2) = ._2₁(x2)
part_of_snake_4_in_gaaa₄(x1, x2, x3, x4) = part_of_snake_4_in_gaaa₁(x1)
part_of_snake_4_out_gaaa₄(x1, x2, x3, x4) = part_of_snake_4_out_gaaa₂(x1, x4)
if_part_of_snake_4_in_1_gaaa₇(x1, x2, x3, x4, x5, x6, x7) = if_part_of_snake_4_in_1_gaaa₂(x2, x7)
IF_PRODUCE_SNAKE_4_IN_1_GGAA₇(x1, x2, x3, x4, x5, x6, x7) = IF_PRODUCE_SNAKE_4_IN_1_GGAA₃(x2, x3, x7)
PRODUCE_SNAKE_4_IN_GGAA₄(x1, x2, x3, x4) = PRODUCE_SNAKE_4_IN_GGAA₂(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

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

              ↳ PiDP

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

PRODUCE_SNAKE_4_IN_GGAA₂(._2₁(Rows), Cols) -> IF_PRODUCE_SNAKE_4_IN_1_GGAA₃(Rows, Cols, part_of_snake_4_in_gaaa₁(Cols))
IF_PRODUCE_SNAKE_4_IN_1_GGAA₃(Rows, Cols, part_of_snake_4_out_gaaa₂(Cols, Part)) -> PRODUCE_SNAKE_4_IN_GGAA₂(Rows, Cols)

The TRS R consists of the following rules:

part_of_snake_4_in_gaaa₁([]_0) -> part_of_snake_4_out_gaaa₂([]_0, []_0)
part_of_snake_4_in_gaaa₁(._2₁(R)) -> if_part_of_snake_4_in_1_gaaa₂(R, part_of_snake_4_in_gaaa₁(R))
if_part_of_snake_4_in_1_gaaa₂(R, part_of_snake_4_out_gaaa₂(R, RestRings)) -> part_of_snake_4_out_gaaa₂(._2₁(R), ._2₁(RestRings))

The set Q consists of the following terms:

part_of_snake_4_in_gaaa₁(x0)
if_part_of_snake_4_in_1_gaaa₂(x0, x1)

From the DPs we obtained the following set of size-change graphs:

IF_PRODUCE_SNAKE_4_IN_1_GGAA₃(Rows, Cols, part_of_snake_4_out_gaaa₂(Cols, Part)) -> PRODUCE_SNAKE_4_IN_GGAA₂(Rows, Cols)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 2
PRODUCE_SNAKE_4_IN_GGAA₂(._2₁(Rows), Cols) -> IF_PRODUCE_SNAKE_4_IN_1_GGAA₃(Rows, Cols, part_of_snake_4_in_gaaa₁(Cols))
The graph contains the following edges 1 > 1, 2 >= 2

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

              ↳ PiDP

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

INFINITE_SNAKE_3_IN_GAA₃(._2₂(A, R), ._2₂(A, T), S) -> INFINITE_SNAKE_3_IN_GAA₃(R, T, S)

The TRS R consists of the following rules:

test_snake_3_in_ggg₃(Pattern, C, R) -> if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_in_ga₂(C, Cols))
s2l_2_in_ga₂(0_0, []_0) -> s2l_2_out_ga₂(0_0, []_0)
s2l_2_in_ga₂(s_1₁(X), ._2₂(underscore, Y)) -> if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_in_ga₂(X, Y))
if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_out_ga₂(X, Y)) -> s2l_2_out_ga₂(s_1₁(X), ._2₂(underscore, Y))
if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_in_ga₂(R, Rows))
if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_in_ggg₃(Pattern, Cols, Rows))
snake_3_in_ggg₃(Pattern, Cols, Rows) -> if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_in_gaa₃(Pattern, InfSnake, InfSnake))
infinite_snake_3_in_gaa₃([]_0, S, S) -> infinite_snake_3_out_gaa₃([]_0, S, S)
infinite_snake_3_in_gaa₃(._2₂(A, R), ._2₂(A, T), S) -> if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_in_gaa₃(R, T, S))
if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_out_gaa₃(R, T, S)) -> infinite_snake_3_out_gaa₃(._2₂(A, R), ._2₂(A, T), S)
if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, InfSnake, Snake))
produce_snake_4_in_ggaa₄([]_0, underscore1, underscore2, []_0) -> produce_snake_4_out_ggaa₄([]_0, underscore1, underscore2, []_0)
produce_snake_4_in_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_4_in_gaaa₄([]_0, RestSnake, RestSnake, []_0) -> part_of_snake_4_out_gaaa₄([]_0, RestSnake, RestSnake, []_0)
part_of_snake_4_in_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_in_gaaa₄(R, Rings, RestSnake, RestRings))
if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_out_gaaa₄(R, Rings, RestSnake, RestRings)) -> part_of_snake_4_out_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings))
if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, NewInfSnake, Tail))
if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, NewInfSnake, Tail)) -> produce_snake_4_out_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail))
if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_in_gg₂(Snake, odd_0))
coil_it_2_in_gg₂([]_0, underscore5) -> coil_it_2_out_gg₂([]_0, underscore5)
coil_it_2_in_gg₂(._2₂(Line, Lines), odd_0) -> if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, even_0))
coil_it_2_in_gg₂(._2₂(Line, Lines), even_0) -> if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))
reverse2_2_in_aa₂(List, Reversed) -> if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_in_aga₃(List, []_0, Reversed))
reverse_3_in_aga₃([]_0, Reversed, Reversed) -> reverse_3_out_aga₃([]_0, Reversed, Reversed)
reverse_3_in_aga₃(._2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, ._2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, ._2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(._2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, []_0, Reversed)) -> reverse2_2_out_aa₂(List, Reversed)
if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, odd_0))
if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, odd_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), even_0)
if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, even_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), odd_0)
if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_out_gg₂(Snake, odd_0)) -> snake_3_out_ggg₃(Pattern, Cols, Rows)
if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_out_ggg₃(Pattern, Cols, Rows)) -> test_snake_3_out_ggg₃(Pattern, C, R)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

              ↳ PiDP

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

INFINITE_SNAKE_3_IN_GAA₃(._2₂(A, R), ._2₂(A, T), S) -> INFINITE_SNAKE_3_IN_GAA₃(R, T, S)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

              ↳ PiDP

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

INFINITE_SNAKE_3_IN_GAA₁(._2₁(R)) -> INFINITE_SNAKE_3_IN_GAA₁(R)

From the DPs we obtained the following set of size-change graphs:

INFINITE_SNAKE_3_IN_GAA₁(._2₁(R)) -> INFINITE_SNAKE_3_IN_GAA₁(R)
The graph contains the following edges 1 > 1

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

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

S2L_2_IN_GA₂(s_1₁(X), ._2₂(underscore, Y)) -> S2L_2_IN_GA₂(X, Y)

The TRS R consists of the following rules:

test_snake_3_in_ggg₃(Pattern, C, R) -> if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_in_ga₂(C, Cols))
s2l_2_in_ga₂(0_0, []_0) -> s2l_2_out_ga₂(0_0, []_0)
s2l_2_in_ga₂(s_1₁(X), ._2₂(underscore, Y)) -> if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_in_ga₂(X, Y))
if_s2l_2_in_1_ga₄(X, underscore, Y, s2l_2_out_ga₂(X, Y)) -> s2l_2_out_ga₂(s_1₁(X), ._2₂(underscore, Y))
if_test_snake_3_in_1_ggg₄(Pattern, C, R, s2l_2_out_ga₂(C, Cols)) -> if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_in_ga₂(R, Rows))
if_test_snake_3_in_2_ggg₅(Pattern, C, R, Cols, s2l_2_out_ga₂(R, Rows)) -> if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_in_ggg₃(Pattern, Cols, Rows))
snake_3_in_ggg₃(Pattern, Cols, Rows) -> if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_in_gaa₃(Pattern, InfSnake, InfSnake))
infinite_snake_3_in_gaa₃([]_0, S, S) -> infinite_snake_3_out_gaa₃([]_0, S, S)
infinite_snake_3_in_gaa₃(._2₂(A, R), ._2₂(A, T), S) -> if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_in_gaa₃(R, T, S))
if_infinite_snake_3_in_1_gaa₅(A, R, T, S, infinite_snake_3_out_gaa₃(R, T, S)) -> infinite_snake_3_out_gaa₃(._2₂(A, R), ._2₂(A, T), S)
if_snake_3_in_1_ggg₄(Pattern, Cols, Rows, infinite_snake_3_out_gaa₃(Pattern, InfSnake, InfSnake)) -> if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, InfSnake, Snake))
produce_snake_4_in_ggaa₄([]_0, underscore1, underscore2, []_0) -> produce_snake_4_out_ggaa₄([]_0, underscore1, underscore2, []_0)
produce_snake_4_in_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail)) -> if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_in_gaaa₄(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_4_in_gaaa₄([]_0, RestSnake, RestSnake, []_0) -> part_of_snake_4_out_gaaa₄([]_0, RestSnake, RestSnake, []_0)
part_of_snake_4_in_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings)) -> if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_in_gaaa₄(R, Rings, RestSnake, RestRings))
if_part_of_snake_4_in_1_gaaa₇(underscore4, R, Ring, Rings, RestSnake, RestRings, part_of_snake_4_out_gaaa₄(R, Rings, RestSnake, RestRings)) -> part_of_snake_4_out_gaaa₄(._2₂(underscore4, R), ._2₂(Ring, Rings), RestSnake, ._2₂(Ring, RestRings))
if_produce_snake_4_in_1_ggaa₇(underscore3, Rows, Cols, InfSnake, Part, Tail, part_of_snake_4_out_gaaa₄(Cols, InfSnake, NewInfSnake, Part)) -> if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_in_ggaa₄(Rows, Cols, NewInfSnake, Tail))
if_produce_snake_4_in_2_ggaa₈(underscore3, Rows, Cols, InfSnake, Part, Tail, NewInfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, NewInfSnake, Tail)) -> produce_snake_4_out_ggaa₄(._2₂(underscore3, Rows), Cols, InfSnake, ._2₂(Part, Tail))
if_snake_3_in_2_ggg₅(Pattern, Cols, Rows, InfSnake, produce_snake_4_out_ggaa₄(Rows, Cols, InfSnake, Snake)) -> if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_in_gg₂(Snake, odd_0))
coil_it_2_in_gg₂([]_0, underscore5) -> coil_it_2_out_gg₂([]_0, underscore5)
coil_it_2_in_gg₂(._2₂(Line, Lines), odd_0) -> if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, even_0))
coil_it_2_in_gg₂(._2₂(Line, Lines), even_0) -> if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_in_aa₂(Line, Line1))
reverse2_2_in_aa₂(List, Reversed) -> if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_in_aga₃(List, []_0, Reversed))
reverse_3_in_aga₃([]_0, Reversed, Reversed) -> reverse_3_out_aga₃([]_0, Reversed, Reversed)
reverse_3_in_aga₃(._2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, ._2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, ._2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(._2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, []_0, Reversed)) -> reverse2_2_out_aa₂(List, Reversed)
if_coil_it_2_in_2_gg₃(Line, Lines, reverse2_2_out_aa₂(Line, Line1)) -> if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_in_gg₂(Lines, odd_0))
if_coil_it_2_in_3_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, odd_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), even_0)
if_coil_it_2_in_1_gg₃(Line, Lines, coil_it_2_out_gg₂(Lines, even_0)) -> coil_it_2_out_gg₂(._2₂(Line, Lines), odd_0)
if_snake_3_in_3_ggg₅(Pattern, Cols, Rows, Snake, coil_it_2_out_gg₂(Snake, odd_0)) -> snake_3_out_ggg₃(Pattern, Cols, Rows)
if_test_snake_3_in_3_ggg₆(Pattern, C, R, Cols, Rows, snake_3_out_ggg₃(Pattern, Cols, Rows)) -> test_snake_3_out_ggg₃(Pattern, C, R)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

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

S2L_2_IN_GA₂(s_1₁(X), ._2₂(underscore, Y)) -> S2L_2_IN_GA₂(X, Y)

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

    ↳ PiTRS

      ↳ DependencyPairsProof

        ↳ PiDP

          ↳ DependencyGraphProof

            ↳ AND

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

                ↳ UsableRulesProof

                  ↳ PiDP

                    ↳ PiDPToQDPProof

                      ↳ QDP

                        ↳ QDPSizeChangeProof

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

S2L_2_IN_GA₁(s_1₁(X)) -> S2L_2_IN_GA₁(X)

From the DPs we obtained the following set of size-change graphs:

S2L_2_IN_GA₁(s_1₁(X)) -> S2L_2_IN_GA₁(X)
The graph contains the following edges 1 > 1