Left Termination proof of /tmp/tmp1flso

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₀, nil₀).
s2l₂(s₁(X), cons₂(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₃(nil₀, S, S).
infinite_snake₃(cons₂(A, R), cons₂(A, T), S) :- infinite_snake₃(R, T, S).
produce_snake₄(nil₀, underscore1, underscore2, nil₀).
produce_snake₄(cons₂(underscore3, Rows), Cols, InfSnake, cons₂(Part, Tail)) :- part_{of_snake₄}(Cols, InfSnake, NewInfSnake, Part), produce_snake₄(Rows, Cols, NewInfSnake, Tail).
part_{of_snake₄}(nil₀, RestSnake, RestSnake, nil₀).
part_{of_snake₄}(cons₂(underscore4, R), cons₂(Ring, Rings), RestSnake, cons₂(Ring, RestRings)) :- part_{of_snake₄}(R, Rings, RestSnake, RestRings).
coil_it₂(nil₀, underscore5).
coil_it₂(cons₂(Line, Lines), odd₀) :- coil_it₂(Lines, even₀).
coil_it₂(cons₂(Line, Lines), even₀) :- reverse2₂(Line, Line1), coil_it₂(Lines, odd₀).
reverse2₂(List, Reversed) :- reverse₃(List, nil₀, Reversed).
reverse₃(nil₀, Reversed, Reversed).
reverse₃(cons₂(Head, Tail), SoFar, Reversed) :- reverse₃(Tail, cons₂(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, nil_0) -> s2l_2_out_ga₂(0_0, nil_0)
s2l_2_in_ga₂(s_1₁(X), cons_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), cons_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₃(nil_0, S, S) -> infinite_snake_3_out_gaa₃(nil_0, S, S)
infinite_snake_3_in_gaa₃(cons_2₂(A, R), cons_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₃(cons_2₂(A, R), cons_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₄(nil_0, underscore1, underscore2, nil_0) -> produce_snake_4_out_ggaa₄(nil_0, underscore1, underscore2, nil_0)
produce_snake_4_in_ggaa₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₄(nil_0, RestSnake, RestSnake, nil_0) -> part_of_snake_4_out_gaaa₄(nil_0, RestSnake, RestSnake, nil_0)
part_of_snake_4_in_gaaa₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₂(nil_0, underscore5) -> coil_it_2_out_gg₂(nil_0, underscore5)
coil_it_2_in_gg₂(cons_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₂(cons_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, nil_0, Reversed))
reverse_3_in_aga₃(nil_0, Reversed, Reversed) -> reverse_3_out_aga₃(nil_0, Reversed, Reversed)
reverse_3_in_aga₃(cons_2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, cons_2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, cons_2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(cons_2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, nil_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₂(cons_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₂(cons_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, nil_0) -> s2l_2_out_ga₂(0_0, nil_0)
s2l_2_in_ga₂(s_1₁(X), cons_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), cons_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₃(nil_0, S, S) -> infinite_snake_3_out_gaa₃(nil_0, S, S)
infinite_snake_3_in_gaa₃(cons_2₂(A, R), cons_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₃(cons_2₂(A, R), cons_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₄(nil_0, underscore1, underscore2, nil_0) -> produce_snake_4_out_ggaa₄(nil_0, underscore1, underscore2, nil_0)
produce_snake_4_in_ggaa₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₄(nil_0, RestSnake, RestSnake, nil_0) -> part_of_snake_4_out_gaaa₄(nil_0, RestSnake, RestSnake, nil_0)
part_of_snake_4_in_gaaa₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₂(nil_0, underscore5) -> coil_it_2_out_gg₂(nil_0, underscore5)
coil_it_2_in_gg₂(cons_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₂(cons_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, nil_0, Reversed))
reverse_3_in_aga₃(nil_0, Reversed, Reversed) -> reverse_3_out_aga₃(nil_0, Reversed, Reversed)
reverse_3_in_aga₃(cons_2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, cons_2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, cons_2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(cons_2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, nil_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₂(cons_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₂(cons_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), cons_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), cons_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₃(cons_2₂(A, R), cons_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₃(cons_2₂(A, R), cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_2₂(Part, Tail)) -> PART_OF_SNAKE_4_IN_GAAA₄(Cols, InfSnake, NewInfSnake, Part)
PART_OF_SNAKE_4_IN_GAAA₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₂(cons_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₂(cons_2₂(Line, Lines), odd_0) -> COIL_IT_2_IN_GG₂(Lines, even_0)
COIL_IT_2_IN_GG₂(cons_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₂(cons_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, nil_0, Reversed))
REVERSE2_2_IN_AA₂(List, Reversed) -> REVERSE_3_IN_AGA₃(List, nil_0, Reversed)
REVERSE_3_IN_AGA₃(cons_2₂(Head, Tail), SoFar, Reversed) -> IF_REVERSE_3_IN_1_AGA₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, cons_2₂(Head, SoFar), Reversed))
REVERSE_3_IN_AGA₃(cons_2₂(Head, Tail), SoFar, Reversed) -> REVERSE_3_IN_AGA₃(Tail, cons_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, nil_0) -> s2l_2_out_ga₂(0_0, nil_0)
s2l_2_in_ga₂(s_1₁(X), cons_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), cons_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₃(nil_0, S, S) -> infinite_snake_3_out_gaa₃(nil_0, S, S)
infinite_snake_3_in_gaa₃(cons_2₂(A, R), cons_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₃(cons_2₂(A, R), cons_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₄(nil_0, underscore1, underscore2, nil_0) -> produce_snake_4_out_ggaa₄(nil_0, underscore1, underscore2, nil_0)
produce_snake_4_in_ggaa₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₄(nil_0, RestSnake, RestSnake, nil_0) -> part_of_snake_4_out_gaaa₄(nil_0, RestSnake, RestSnake, nil_0)
part_of_snake_4_in_gaaa₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₂(nil_0, underscore5) -> coil_it_2_out_gg₂(nil_0, underscore5)
coil_it_2_in_gg₂(cons_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₂(cons_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, nil_0, Reversed))
reverse_3_in_aga₃(nil_0, Reversed, Reversed) -> reverse_3_out_aga₃(nil_0, Reversed, Reversed)
reverse_3_in_aga₃(cons_2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, cons_2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, cons_2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(cons_2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, nil_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₂(cons_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₂(cons_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
nil_0 = nil_0
s_1₁(x1) = s_1₁(x1)
cons_2₂(x1, x2) = cons_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), cons_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), cons_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₃(cons_2₂(A, R), cons_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₃(cons_2₂(A, R), cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_2₂(Part, Tail)) -> PART_OF_SNAKE_4_IN_GAAA₄(Cols, InfSnake, NewInfSnake, Part)
PART_OF_SNAKE_4_IN_GAAA₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₂(cons_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₂(cons_2₂(Line, Lines), odd_0) -> COIL_IT_2_IN_GG₂(Lines, even_0)
COIL_IT_2_IN_GG₂(cons_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₂(cons_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, nil_0, Reversed))
REVERSE2_2_IN_AA₂(List, Reversed) -> REVERSE_3_IN_AGA₃(List, nil_0, Reversed)
REVERSE_3_IN_AGA₃(cons_2₂(Head, Tail), SoFar, Reversed) -> IF_REVERSE_3_IN_1_AGA₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, cons_2₂(Head, SoFar), Reversed))
REVERSE_3_IN_AGA₃(cons_2₂(Head, Tail), SoFar, Reversed) -> REVERSE_3_IN_AGA₃(Tail, cons_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, nil_0) -> s2l_2_out_ga₂(0_0, nil_0)
s2l_2_in_ga₂(s_1₁(X), cons_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), cons_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₃(nil_0, S, S) -> infinite_snake_3_out_gaa₃(nil_0, S, S)
infinite_snake_3_in_gaa₃(cons_2₂(A, R), cons_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₃(cons_2₂(A, R), cons_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₄(nil_0, underscore1, underscore2, nil_0) -> produce_snake_4_out_ggaa₄(nil_0, underscore1, underscore2, nil_0)
produce_snake_4_in_ggaa₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₄(nil_0, RestSnake, RestSnake, nil_0) -> part_of_snake_4_out_gaaa₄(nil_0, RestSnake, RestSnake, nil_0)
part_of_snake_4_in_gaaa₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₂(nil_0, underscore5) -> coil_it_2_out_gg₂(nil_0, underscore5)
coil_it_2_in_gg₂(cons_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₂(cons_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, nil_0, Reversed))
reverse_3_in_aga₃(nil_0, Reversed, Reversed) -> reverse_3_out_aga₃(nil_0, Reversed, Reversed)
reverse_3_in_aga₃(cons_2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, cons_2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, cons_2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(cons_2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, nil_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₂(cons_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₂(cons_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₃(cons_2₂(Head, Tail), SoFar, Reversed) -> REVERSE_3_IN_AGA₃(Tail, cons_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, nil_0) -> s2l_2_out_ga₂(0_0, nil_0)
s2l_2_in_ga₂(s_1₁(X), cons_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), cons_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₃(nil_0, S, S) -> infinite_snake_3_out_gaa₃(nil_0, S, S)
infinite_snake_3_in_gaa₃(cons_2₂(A, R), cons_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₃(cons_2₂(A, R), cons_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₄(nil_0, underscore1, underscore2, nil_0) -> produce_snake_4_out_ggaa₄(nil_0, underscore1, underscore2, nil_0)
produce_snake_4_in_ggaa₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₄(nil_0, RestSnake, RestSnake, nil_0) -> part_of_snake_4_out_gaaa₄(nil_0, RestSnake, RestSnake, nil_0)
part_of_snake_4_in_gaaa₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₂(nil_0, underscore5) -> coil_it_2_out_gg₂(nil_0, underscore5)
coil_it_2_in_gg₂(cons_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₂(cons_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, nil_0, Reversed))
reverse_3_in_aga₃(nil_0, Reversed, Reversed) -> reverse_3_out_aga₃(nil_0, Reversed, Reversed)
reverse_3_in_aga₃(cons_2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, cons_2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, cons_2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(cons_2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, nil_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₂(cons_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₂(cons_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₃(cons_2₂(Head, Tail), SoFar, Reversed) -> REVERSE_3_IN_AGA₃(Tail, cons_2₂(Head, SoFar), Reversed)

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

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, nil_0) -> s2l_2_out_ga₂(0_0, nil_0)
s2l_2_in_ga₂(s_1₁(X), cons_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), cons_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₃(nil_0, S, S) -> infinite_snake_3_out_gaa₃(nil_0, S, S)
infinite_snake_3_in_gaa₃(cons_2₂(A, R), cons_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₃(cons_2₂(A, R), cons_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₄(nil_0, underscore1, underscore2, nil_0) -> produce_snake_4_out_ggaa₄(nil_0, underscore1, underscore2, nil_0)
produce_snake_4_in_ggaa₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₄(nil_0, RestSnake, RestSnake, nil_0) -> part_of_snake_4_out_gaaa₄(nil_0, RestSnake, RestSnake, nil_0)
part_of_snake_4_in_gaaa₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₂(nil_0, underscore5) -> coil_it_2_out_gg₂(nil_0, underscore5)
coil_it_2_in_gg₂(cons_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₂(cons_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, nil_0, Reversed))
reverse_3_in_aga₃(nil_0, Reversed, Reversed) -> reverse_3_out_aga₃(nil_0, Reversed, Reversed)
reverse_3_in_aga₃(cons_2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, cons_2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, cons_2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(cons_2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, nil_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₂(cons_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₂(cons_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₂(cons_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₂(cons_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)

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, nil_0, Reversed))
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, nil_0, Reversed)) -> reverse2_2_out_aa₂(List, Reversed)
reverse_3_in_aga₃(nil_0, Reversed, Reversed) -> reverse_3_out_aga₃(nil_0, Reversed, Reversed)
reverse_3_in_aga₃(cons_2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, cons_2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, cons_2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(cons_2₂(Head, Tail), SoFar, Reversed)

The argument filtering Pi contains the following mapping:
nil_0 = nil_0
cons_2₂(x1, x2) = cons_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₂(cons_2₁(Lines), even_0) -> IF_COIL_IT_2_IN_2_GG₂(Lines, reverse2_2_in_aa)
COIL_IT_2_IN_GG₂(cons_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)

The TRS R consists of the following rules:

reverse2_2_in_aa -> if_reverse2_2_in_1_aa₁(reverse_3_in_aga₁(nil_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₂(nil_0, Reversed)
reverse_3_in_aga₁(SoFar) -> if_reverse_3_in_1_aga₁(reverse_3_in_aga₁(cons_2₁(SoFar)))
if_reverse_3_in_1_aga₁(reverse_3_out_aga₂(Tail, Reversed)) -> reverse_3_out_aga₂(cons_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 {IF_COIL_IT_2_IN_2_GG₂, COIL_IT_2_IN_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:

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₂(cons_2₁(Lines), odd_0) -> COIL_IT_2_IN_GG₂(Lines, even_0)
The graph contains the following edges 1 > 1
COIL_IT_2_IN_GG₂(cons_2₁(Lines), even_0) -> IF_COIL_IT_2_IN_2_GG₂(Lines, reverse2_2_in_aa)
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₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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, nil_0) -> s2l_2_out_ga₂(0_0, nil_0)
s2l_2_in_ga₂(s_1₁(X), cons_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), cons_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₃(nil_0, S, S) -> infinite_snake_3_out_gaa₃(nil_0, S, S)
infinite_snake_3_in_gaa₃(cons_2₂(A, R), cons_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₃(cons_2₂(A, R), cons_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₄(nil_0, underscore1, underscore2, nil_0) -> produce_snake_4_out_ggaa₄(nil_0, underscore1, underscore2, nil_0)
produce_snake_4_in_ggaa₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₄(nil_0, RestSnake, RestSnake, nil_0) -> part_of_snake_4_out_gaaa₄(nil_0, RestSnake, RestSnake, nil_0)
part_of_snake_4_in_gaaa₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₂(nil_0, underscore5) -> coil_it_2_out_gg₂(nil_0, underscore5)
coil_it_2_in_gg₂(cons_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₂(cons_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, nil_0, Reversed))
reverse_3_in_aga₃(nil_0, Reversed, Reversed) -> reverse_3_out_aga₃(nil_0, Reversed, Reversed)
reverse_3_in_aga₃(cons_2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, cons_2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, cons_2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(cons_2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, nil_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₂(cons_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₂(cons_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₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_2₂(Ring, RestRings)) -> PART_OF_SNAKE_4_IN_GAAA₄(R, Rings, RestSnake, RestRings)

R is empty.
The argument filtering Pi contains the following mapping:
cons_2₂(x1, x2) = cons_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₁(cons_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₁(cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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, nil_0) -> s2l_2_out_ga₂(0_0, nil_0)
s2l_2_in_ga₂(s_1₁(X), cons_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), cons_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₃(nil_0, S, S) -> infinite_snake_3_out_gaa₃(nil_0, S, S)
infinite_snake_3_in_gaa₃(cons_2₂(A, R), cons_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₃(cons_2₂(A, R), cons_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₄(nil_0, underscore1, underscore2, nil_0) -> produce_snake_4_out_ggaa₄(nil_0, underscore1, underscore2, nil_0)
produce_snake_4_in_ggaa₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₄(nil_0, RestSnake, RestSnake, nil_0) -> part_of_snake_4_out_gaaa₄(nil_0, RestSnake, RestSnake, nil_0)
part_of_snake_4_in_gaaa₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₂(nil_0, underscore5) -> coil_it_2_out_gg₂(nil_0, underscore5)
coil_it_2_in_gg₂(cons_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₂(cons_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, nil_0, Reversed))
reverse_3_in_aga₃(nil_0, Reversed, Reversed) -> reverse_3_out_aga₃(nil_0, Reversed, Reversed)
reverse_3_in_aga₃(cons_2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, cons_2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, cons_2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(cons_2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, nil_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₂(cons_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₂(cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₄(nil_0, RestSnake, RestSnake, nil_0) -> part_of_snake_4_out_gaaa₄(nil_0, RestSnake, RestSnake, nil_0)
part_of_snake_4_in_gaaa₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_2₂(Ring, RestRings))

The argument filtering Pi contains the following mapping:
nil_0 = nil_0
cons_2₂(x1, x2) = cons_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₂(cons_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₁(nil_0) -> part_of_snake_4_out_gaaa₁(nil_0)
part_of_snake_4_in_gaaa₁(cons_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₁(cons_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₂(cons_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₃(cons_2₂(A, R), cons_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, nil_0) -> s2l_2_out_ga₂(0_0, nil_0)
s2l_2_in_ga₂(s_1₁(X), cons_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), cons_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₃(nil_0, S, S) -> infinite_snake_3_out_gaa₃(nil_0, S, S)
infinite_snake_3_in_gaa₃(cons_2₂(A, R), cons_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₃(cons_2₂(A, R), cons_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₄(nil_0, underscore1, underscore2, nil_0) -> produce_snake_4_out_ggaa₄(nil_0, underscore1, underscore2, nil_0)
produce_snake_4_in_ggaa₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₄(nil_0, RestSnake, RestSnake, nil_0) -> part_of_snake_4_out_gaaa₄(nil_0, RestSnake, RestSnake, nil_0)
part_of_snake_4_in_gaaa₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₂(nil_0, underscore5) -> coil_it_2_out_gg₂(nil_0, underscore5)
coil_it_2_in_gg₂(cons_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₂(cons_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, nil_0, Reversed))
reverse_3_in_aga₃(nil_0, Reversed, Reversed) -> reverse_3_out_aga₃(nil_0, Reversed, Reversed)
reverse_3_in_aga₃(cons_2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, cons_2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, cons_2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(cons_2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, nil_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₂(cons_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₂(cons_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₃(cons_2₂(A, R), cons_2₂(A, T), S) -> INFINITE_SNAKE_3_IN_GAA₃(R, T, S)

R is empty.
The argument filtering Pi contains the following mapping:
cons_2₂(x1, x2) = cons_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₁(cons_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₁(cons_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), cons_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, nil_0) -> s2l_2_out_ga₂(0_0, nil_0)
s2l_2_in_ga₂(s_1₁(X), cons_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), cons_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₃(nil_0, S, S) -> infinite_snake_3_out_gaa₃(nil_0, S, S)
infinite_snake_3_in_gaa₃(cons_2₂(A, R), cons_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₃(cons_2₂(A, R), cons_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₄(nil_0, underscore1, underscore2, nil_0) -> produce_snake_4_out_ggaa₄(nil_0, underscore1, underscore2, nil_0)
produce_snake_4_in_ggaa₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₄(nil_0, RestSnake, RestSnake, nil_0) -> part_of_snake_4_out_gaaa₄(nil_0, RestSnake, RestSnake, nil_0)
part_of_snake_4_in_gaaa₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₂(nil_0, underscore5) -> coil_it_2_out_gg₂(nil_0, underscore5)
coil_it_2_in_gg₂(cons_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₂(cons_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, nil_0, Reversed))
reverse_3_in_aga₃(nil_0, Reversed, Reversed) -> reverse_3_out_aga₃(nil_0, Reversed, Reversed)
reverse_3_in_aga₃(cons_2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, cons_2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, cons_2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(cons_2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, nil_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₂(cons_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₂(cons_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), cons_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)
cons_2₂(x1, x2) = cons_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, nil_0) -> s2l_2_out_ga₂(0_0, nil_0)
s2l_2_in_ga₂(s_1₁(X), cons_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), cons_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₃(nil_0, S, S) -> infinite_snake_3_out_gaa₃(nil_0, S, S)
infinite_snake_3_in_gaa₃(cons_2₂(A, R), cons_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₃(cons_2₂(A, R), cons_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₄(nil_0, underscore1, underscore2, nil_0) -> produce_snake_4_out_ggaa₄(nil_0, underscore1, underscore2, nil_0)
produce_snake_4_in_ggaa₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₄(nil_0, RestSnake, RestSnake, nil_0) -> part_of_snake_4_out_gaaa₄(nil_0, RestSnake, RestSnake, nil_0)
part_of_snake_4_in_gaaa₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₂(nil_0, underscore5) -> coil_it_2_out_gg₂(nil_0, underscore5)
coil_it_2_in_gg₂(cons_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₂(cons_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, nil_0, Reversed))
reverse_3_in_aga₃(nil_0, Reversed, Reversed) -> reverse_3_out_aga₃(nil_0, Reversed, Reversed)
reverse_3_in_aga₃(cons_2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, cons_2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, cons_2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(cons_2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, nil_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₂(cons_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₂(cons_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, nil_0) -> s2l_2_out_ga₂(0_0, nil_0)
s2l_2_in_ga₂(s_1₁(X), cons_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), cons_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₃(nil_0, S, S) -> infinite_snake_3_out_gaa₃(nil_0, S, S)
infinite_snake_3_in_gaa₃(cons_2₂(A, R), cons_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₃(cons_2₂(A, R), cons_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₄(nil_0, underscore1, underscore2, nil_0) -> produce_snake_4_out_ggaa₄(nil_0, underscore1, underscore2, nil_0)
produce_snake_4_in_ggaa₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₄(nil_0, RestSnake, RestSnake, nil_0) -> part_of_snake_4_out_gaaa₄(nil_0, RestSnake, RestSnake, nil_0)
part_of_snake_4_in_gaaa₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₂(nil_0, underscore5) -> coil_it_2_out_gg₂(nil_0, underscore5)
coil_it_2_in_gg₂(cons_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₂(cons_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, nil_0, Reversed))
reverse_3_in_aga₃(nil_0, Reversed, Reversed) -> reverse_3_out_aga₃(nil_0, Reversed, Reversed)
reverse_3_in_aga₃(cons_2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, cons_2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, cons_2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(cons_2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, nil_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₂(cons_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₂(cons_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), cons_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), cons_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₃(cons_2₂(A, R), cons_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₃(cons_2₂(A, R), cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_2₂(Part, Tail)) -> PART_OF_SNAKE_4_IN_GAAA₄(Cols, InfSnake, NewInfSnake, Part)
PART_OF_SNAKE_4_IN_GAAA₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₂(cons_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₂(cons_2₂(Line, Lines), odd_0) -> COIL_IT_2_IN_GG₂(Lines, even_0)
COIL_IT_2_IN_GG₂(cons_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₂(cons_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, nil_0, Reversed))
REVERSE2_2_IN_AA₂(List, Reversed) -> REVERSE_3_IN_AGA₃(List, nil_0, Reversed)
REVERSE_3_IN_AGA₃(cons_2₂(Head, Tail), SoFar, Reversed) -> IF_REVERSE_3_IN_1_AGA₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, cons_2₂(Head, SoFar), Reversed))
REVERSE_3_IN_AGA₃(cons_2₂(Head, Tail), SoFar, Reversed) -> REVERSE_3_IN_AGA₃(Tail, cons_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, nil_0) -> s2l_2_out_ga₂(0_0, nil_0)
s2l_2_in_ga₂(s_1₁(X), cons_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), cons_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₃(nil_0, S, S) -> infinite_snake_3_out_gaa₃(nil_0, S, S)
infinite_snake_3_in_gaa₃(cons_2₂(A, R), cons_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₃(cons_2₂(A, R), cons_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₄(nil_0, underscore1, underscore2, nil_0) -> produce_snake_4_out_ggaa₄(nil_0, underscore1, underscore2, nil_0)
produce_snake_4_in_ggaa₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₄(nil_0, RestSnake, RestSnake, nil_0) -> part_of_snake_4_out_gaaa₄(nil_0, RestSnake, RestSnake, nil_0)
part_of_snake_4_in_gaaa₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₂(nil_0, underscore5) -> coil_it_2_out_gg₂(nil_0, underscore5)
coil_it_2_in_gg₂(cons_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₂(cons_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, nil_0, Reversed))
reverse_3_in_aga₃(nil_0, Reversed, Reversed) -> reverse_3_out_aga₃(nil_0, Reversed, Reversed)
reverse_3_in_aga₃(cons_2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, cons_2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, cons_2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(cons_2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, nil_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₂(cons_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₂(cons_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
nil_0 = nil_0
s_1₁(x1) = s_1₁(x1)
cons_2₂(x1, x2) = cons_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), cons_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), cons_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₃(cons_2₂(A, R), cons_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₃(cons_2₂(A, R), cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_2₂(Part, Tail)) -> PART_OF_SNAKE_4_IN_GAAA₄(Cols, InfSnake, NewInfSnake, Part)
PART_OF_SNAKE_4_IN_GAAA₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₂(cons_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₂(cons_2₂(Line, Lines), odd_0) -> COIL_IT_2_IN_GG₂(Lines, even_0)
COIL_IT_2_IN_GG₂(cons_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₂(cons_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, nil_0, Reversed))
REVERSE2_2_IN_AA₂(List, Reversed) -> REVERSE_3_IN_AGA₃(List, nil_0, Reversed)
REVERSE_3_IN_AGA₃(cons_2₂(Head, Tail), SoFar, Reversed) -> IF_REVERSE_3_IN_1_AGA₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, cons_2₂(Head, SoFar), Reversed))
REVERSE_3_IN_AGA₃(cons_2₂(Head, Tail), SoFar, Reversed) -> REVERSE_3_IN_AGA₃(Tail, cons_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, nil_0) -> s2l_2_out_ga₂(0_0, nil_0)
s2l_2_in_ga₂(s_1₁(X), cons_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), cons_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₃(nil_0, S, S) -> infinite_snake_3_out_gaa₃(nil_0, S, S)
infinite_snake_3_in_gaa₃(cons_2₂(A, R), cons_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₃(cons_2₂(A, R), cons_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₄(nil_0, underscore1, underscore2, nil_0) -> produce_snake_4_out_ggaa₄(nil_0, underscore1, underscore2, nil_0)
produce_snake_4_in_ggaa₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₄(nil_0, RestSnake, RestSnake, nil_0) -> part_of_snake_4_out_gaaa₄(nil_0, RestSnake, RestSnake, nil_0)
part_of_snake_4_in_gaaa₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₂(nil_0, underscore5) -> coil_it_2_out_gg₂(nil_0, underscore5)
coil_it_2_in_gg₂(cons_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₂(cons_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, nil_0, Reversed))
reverse_3_in_aga₃(nil_0, Reversed, Reversed) -> reverse_3_out_aga₃(nil_0, Reversed, Reversed)
reverse_3_in_aga₃(cons_2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, cons_2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, cons_2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(cons_2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, nil_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₂(cons_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₂(cons_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
nil_0 = nil_0
s_1₁(x1) = s_1₁(x1)
cons_2₂(x1, x2) = cons_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

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

              ↳ PiDP

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

REVERSE_3_IN_AGA₃(cons_2₂(Head, Tail), SoFar, Reversed) -> REVERSE_3_IN_AGA₃(Tail, cons_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, nil_0) -> s2l_2_out_ga₂(0_0, nil_0)
s2l_2_in_ga₂(s_1₁(X), cons_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), cons_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₃(nil_0, S, S) -> infinite_snake_3_out_gaa₃(nil_0, S, S)
infinite_snake_3_in_gaa₃(cons_2₂(A, R), cons_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₃(cons_2₂(A, R), cons_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₄(nil_0, underscore1, underscore2, nil_0) -> produce_snake_4_out_ggaa₄(nil_0, underscore1, underscore2, nil_0)
produce_snake_4_in_ggaa₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₄(nil_0, RestSnake, RestSnake, nil_0) -> part_of_snake_4_out_gaaa₄(nil_0, RestSnake, RestSnake, nil_0)
part_of_snake_4_in_gaaa₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₂(nil_0, underscore5) -> coil_it_2_out_gg₂(nil_0, underscore5)
coil_it_2_in_gg₂(cons_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₂(cons_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, nil_0, Reversed))
reverse_3_in_aga₃(nil_0, Reversed, Reversed) -> reverse_3_out_aga₃(nil_0, Reversed, Reversed)
reverse_3_in_aga₃(cons_2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, cons_2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, cons_2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(cons_2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, nil_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₂(cons_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₂(cons_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

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

COIL_IT_2_IN_GG₂(cons_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₂(cons_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)

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, nil_0) -> s2l_2_out_ga₂(0_0, nil_0)
s2l_2_in_ga₂(s_1₁(X), cons_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), cons_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₃(nil_0, S, S) -> infinite_snake_3_out_gaa₃(nil_0, S, S)
infinite_snake_3_in_gaa₃(cons_2₂(A, R), cons_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₃(cons_2₂(A, R), cons_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₄(nil_0, underscore1, underscore2, nil_0) -> produce_snake_4_out_ggaa₄(nil_0, underscore1, underscore2, nil_0)
produce_snake_4_in_ggaa₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₄(nil_0, RestSnake, RestSnake, nil_0) -> part_of_snake_4_out_gaaa₄(nil_0, RestSnake, RestSnake, nil_0)
part_of_snake_4_in_gaaa₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₂(nil_0, underscore5) -> coil_it_2_out_gg₂(nil_0, underscore5)
coil_it_2_in_gg₂(cons_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₂(cons_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, nil_0, Reversed))
reverse_3_in_aga₃(nil_0, Reversed, Reversed) -> reverse_3_out_aga₃(nil_0, Reversed, Reversed)
reverse_3_in_aga₃(cons_2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, cons_2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, cons_2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(cons_2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, nil_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₂(cons_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₂(cons_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

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

PART_OF_SNAKE_4_IN_GAAA₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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, nil_0) -> s2l_2_out_ga₂(0_0, nil_0)
s2l_2_in_ga₂(s_1₁(X), cons_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), cons_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₃(nil_0, S, S) -> infinite_snake_3_out_gaa₃(nil_0, S, S)
infinite_snake_3_in_gaa₃(cons_2₂(A, R), cons_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₃(cons_2₂(A, R), cons_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₄(nil_0, underscore1, underscore2, nil_0) -> produce_snake_4_out_ggaa₄(nil_0, underscore1, underscore2, nil_0)
produce_snake_4_in_ggaa₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₄(nil_0, RestSnake, RestSnake, nil_0) -> part_of_snake_4_out_gaaa₄(nil_0, RestSnake, RestSnake, nil_0)
part_of_snake_4_in_gaaa₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₂(nil_0, underscore5) -> coil_it_2_out_gg₂(nil_0, underscore5)
coil_it_2_in_gg₂(cons_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₂(cons_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, nil_0, Reversed))
reverse_3_in_aga₃(nil_0, Reversed, Reversed) -> reverse_3_out_aga₃(nil_0, Reversed, Reversed)
reverse_3_in_aga₃(cons_2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, cons_2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, cons_2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(cons_2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, nil_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₂(cons_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₂(cons_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

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

PRODUCE_SNAKE_4_IN_GGAA₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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, nil_0) -> s2l_2_out_ga₂(0_0, nil_0)
s2l_2_in_ga₂(s_1₁(X), cons_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), cons_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₃(nil_0, S, S) -> infinite_snake_3_out_gaa₃(nil_0, S, S)
infinite_snake_3_in_gaa₃(cons_2₂(A, R), cons_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₃(cons_2₂(A, R), cons_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₄(nil_0, underscore1, underscore2, nil_0) -> produce_snake_4_out_ggaa₄(nil_0, underscore1, underscore2, nil_0)
produce_snake_4_in_ggaa₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₄(nil_0, RestSnake, RestSnake, nil_0) -> part_of_snake_4_out_gaaa₄(nil_0, RestSnake, RestSnake, nil_0)
part_of_snake_4_in_gaaa₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₂(nil_0, underscore5) -> coil_it_2_out_gg₂(nil_0, underscore5)
coil_it_2_in_gg₂(cons_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₂(cons_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, nil_0, Reversed))
reverse_3_in_aga₃(nil_0, Reversed, Reversed) -> reverse_3_out_aga₃(nil_0, Reversed, Reversed)
reverse_3_in_aga₃(cons_2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, cons_2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, cons_2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(cons_2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, nil_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₂(cons_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₂(cons_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

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

INFINITE_SNAKE_3_IN_GAA₃(cons_2₂(A, R), cons_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, nil_0) -> s2l_2_out_ga₂(0_0, nil_0)
s2l_2_in_ga₂(s_1₁(X), cons_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), cons_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₃(nil_0, S, S) -> infinite_snake_3_out_gaa₃(nil_0, S, S)
infinite_snake_3_in_gaa₃(cons_2₂(A, R), cons_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₃(cons_2₂(A, R), cons_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₄(nil_0, underscore1, underscore2, nil_0) -> produce_snake_4_out_ggaa₄(nil_0, underscore1, underscore2, nil_0)
produce_snake_4_in_ggaa₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₄(nil_0, RestSnake, RestSnake, nil_0) -> part_of_snake_4_out_gaaa₄(nil_0, RestSnake, RestSnake, nil_0)
part_of_snake_4_in_gaaa₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₂(nil_0, underscore5) -> coil_it_2_out_gg₂(nil_0, underscore5)
coil_it_2_in_gg₂(cons_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₂(cons_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, nil_0, Reversed))
reverse_3_in_aga₃(nil_0, Reversed, Reversed) -> reverse_3_out_aga₃(nil_0, Reversed, Reversed)
reverse_3_in_aga₃(cons_2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, cons_2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, cons_2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(cons_2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, nil_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₂(cons_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₂(cons_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

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

S2L_2_IN_GA₂(s_1₁(X), cons_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, nil_0) -> s2l_2_out_ga₂(0_0, nil_0)
s2l_2_in_ga₂(s_1₁(X), cons_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), cons_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₃(nil_0, S, S) -> infinite_snake_3_out_gaa₃(nil_0, S, S)
infinite_snake_3_in_gaa₃(cons_2₂(A, R), cons_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₃(cons_2₂(A, R), cons_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₄(nil_0, underscore1, underscore2, nil_0) -> produce_snake_4_out_ggaa₄(nil_0, underscore1, underscore2, nil_0)
produce_snake_4_in_ggaa₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₄(nil_0, RestSnake, RestSnake, nil_0) -> part_of_snake_4_out_gaaa₄(nil_0, RestSnake, RestSnake, nil_0)
part_of_snake_4_in_gaaa₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore4, R), cons_2₂(Ring, Rings), RestSnake, cons_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₄(cons_2₂(underscore3, Rows), Cols, InfSnake, cons_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₂(nil_0, underscore5) -> coil_it_2_out_gg₂(nil_0, underscore5)
coil_it_2_in_gg₂(cons_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₂(cons_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, nil_0, Reversed))
reverse_3_in_aga₃(nil_0, Reversed, Reversed) -> reverse_3_out_aga₃(nil_0, Reversed, Reversed)
reverse_3_in_aga₃(cons_2₂(Head, Tail), SoFar, Reversed) -> if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_in_aga₃(Tail, cons_2₂(Head, SoFar), Reversed))
if_reverse_3_in_1_aga₅(Head, Tail, SoFar, Reversed, reverse_3_out_aga₃(Tail, cons_2₂(Head, SoFar), Reversed)) -> reverse_3_out_aga₃(cons_2₂(Head, Tail), SoFar, Reversed)
if_reverse2_2_in_1_aa₃(List, Reversed, reverse_3_out_aga₃(List, nil_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₂(cons_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₂(cons_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)