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

(0) Obligation:

Clauses:

test_snake(Pattern, C, R) :- ','(s2l(C, Cols), ','(s2l(R, Rows), snake(Pattern, Cols, Rows))).
s2l(0, nil).
s2l(s(X), cons(X1, 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, X2, X3, nil).
produce_snake(cons(X4, 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(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) :- part_of_snake(R, Rings, RestSnake, RestRings).
coil_it(nil, X6).
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).

Queries:

test_snake(g,g,g).

(1) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
test_snake_in: (b,b,b)
s2l_in: (b,f)
snake_in: (b,f,f)
infinite_snake_in: (b,f,f)
produce_snake_in: (f,f,f,f)
part_of_snake_in: (f,f,f,f)
coil_it_in: (f,b)
reverse2_in: (f,f)
reverse_in: (f,b,f) (f,f,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, nil) → s2l_out_ga(0, nil)
s2l_in_ga(s(X), cons(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), cons(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_gaa(Pattern, Cols, Rows))
snake_in_gaa(Pattern, Cols, Rows) → U5_gaa(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa(nil, S, S) → infinite_snake_out_gaa(nil, S, S)
infinite_snake_in_gaa(cons(A, R), cons(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(cons(A, R), cons(A, T), S)
U5_gaa(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_gaa(Pattern, Cols, Rows, produce_snake_in_aaaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_aaaa(nil, X2, X3, nil) → produce_snake_out_aaaa(nil, X2, X3, nil)
produce_snake_in_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_aaaa(nil, RestSnake, RestSnake, nil) → part_of_snake_out_aaaa(nil, RestSnake, RestSnake, nil)
part_of_snake_in_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_aaaa(R, Rings, RestSnake, RestRings))
U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_aaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings))
U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_aaaa(Rows, Cols, NewInfSnake, Tail))
U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_aaaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail))
U6_gaa(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → U7_gaa(Pattern, Cols, Rows, coil_it_in_ag(Snake, odd))
coil_it_in_ag(nil, X6) → coil_it_out_ag(nil, X6)
coil_it_in_ag(cons(Line, Lines), odd) → U12_ag(Line, Lines, coil_it_in_ag(Lines, even))
coil_it_in_ag(cons(Line, Lines), even) → U13_ag(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, nil, Reversed))
reverse_in_aga(nil, Reversed, Reversed) → reverse_out_aga(nil, Reversed, Reversed)
reverse_in_aga(cons(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
reverse_in_aaa(nil, Reversed, Reversed) → reverse_out_aaa(nil, Reversed, Reversed)
reverse_in_aaa(cons(Head, Tail), SoFar, Reversed) → U16_aaa(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
U16_aaa(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aaa(cons(Head, Tail), SoFar, Reversed)
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aga(cons(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, nil, Reversed)) → reverse2_out_aa(List, Reversed)
U13_ag(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_ag(Line, Lines, coil_it_in_ag(Lines, odd))
U14_ag(Line, Lines, coil_it_out_ag(Lines, odd)) → coil_it_out_ag(cons(Line, Lines), even)
U12_ag(Line, Lines, coil_it_out_ag(Lines, even)) → coil_it_out_ag(cons(Line, Lines), odd)
U7_gaa(Pattern, Cols, Rows, coil_it_out_ag(Snake, odd)) → snake_out_gaa(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_gaa(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x2, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x1)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x1, x4)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x2, x3, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x1, x2, x3, x4)
snake_in_gaa(x1, x2, x3)  =  snake_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
nil  =  nil
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa(x1)
cons(x1, x2)  =  cons(x1, x2)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x1, x2, x5)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x1, x4)
produce_snake_in_aaaa(x1, x2, x3, x4)  =  produce_snake_in_aaaa
produce_snake_out_aaaa(x1, x2, x3, x4)  =  produce_snake_out_aaaa
U9_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_aaaa(x7)
part_of_snake_in_aaaa(x1, x2, x3, x4)  =  part_of_snake_in_aaaa
part_of_snake_out_aaaa(x1, x2, x3, x4)  =  part_of_snake_out_aaaa
U11_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_aaaa(x7)
U10_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_aaaa(x7)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x1, x4)
coil_it_in_ag(x1, x2)  =  coil_it_in_ag(x2)
coil_it_out_ag(x1, x2)  =  coil_it_out_ag(x2)
odd  =  odd
U12_ag(x1, x2, x3)  =  U12_ag(x3)
even  =  even
U13_ag(x1, x2, x3)  =  U13_ag(x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x2)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x3, x5)
reverse_in_aaa(x1, x2, x3)  =  reverse_in_aaa
reverse_out_aaa(x1, x2, x3)  =  reverse_out_aaa
U16_aaa(x1, x2, x3, x4, x5)  =  U16_aaa(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa
U14_ag(x1, x2, x3)  =  U14_ag(x3)
snake_out_gaa(x1, x2, x3)  =  snake_out_gaa(x1)
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg(x1, x2, x3)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(2) Obligation:

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

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, nil) → s2l_out_ga(0, nil)
s2l_in_ga(s(X), cons(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), cons(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_gaa(Pattern, Cols, Rows))
snake_in_gaa(Pattern, Cols, Rows) → U5_gaa(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa(nil, S, S) → infinite_snake_out_gaa(nil, S, S)
infinite_snake_in_gaa(cons(A, R), cons(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(cons(A, R), cons(A, T), S)
U5_gaa(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_gaa(Pattern, Cols, Rows, produce_snake_in_aaaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_aaaa(nil, X2, X3, nil) → produce_snake_out_aaaa(nil, X2, X3, nil)
produce_snake_in_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_aaaa(nil, RestSnake, RestSnake, nil) → part_of_snake_out_aaaa(nil, RestSnake, RestSnake, nil)
part_of_snake_in_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_aaaa(R, Rings, RestSnake, RestRings))
U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_aaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings))
U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_aaaa(Rows, Cols, NewInfSnake, Tail))
U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_aaaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail))
U6_gaa(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → U7_gaa(Pattern, Cols, Rows, coil_it_in_ag(Snake, odd))
coil_it_in_ag(nil, X6) → coil_it_out_ag(nil, X6)
coil_it_in_ag(cons(Line, Lines), odd) → U12_ag(Line, Lines, coil_it_in_ag(Lines, even))
coil_it_in_ag(cons(Line, Lines), even) → U13_ag(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, nil, Reversed))
reverse_in_aga(nil, Reversed, Reversed) → reverse_out_aga(nil, Reversed, Reversed)
reverse_in_aga(cons(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
reverse_in_aaa(nil, Reversed, Reversed) → reverse_out_aaa(nil, Reversed, Reversed)
reverse_in_aaa(cons(Head, Tail), SoFar, Reversed) → U16_aaa(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
U16_aaa(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aaa(cons(Head, Tail), SoFar, Reversed)
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aga(cons(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, nil, Reversed)) → reverse2_out_aa(List, Reversed)
U13_ag(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_ag(Line, Lines, coil_it_in_ag(Lines, odd))
U14_ag(Line, Lines, coil_it_out_ag(Lines, odd)) → coil_it_out_ag(cons(Line, Lines), even)
U12_ag(Line, Lines, coil_it_out_ag(Lines, even)) → coil_it_out_ag(cons(Line, Lines), odd)
U7_gaa(Pattern, Cols, Rows, coil_it_out_ag(Snake, odd)) → snake_out_gaa(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_gaa(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x2, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x1)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x1, x4)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x2, x3, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x1, x2, x3, x4)
snake_in_gaa(x1, x2, x3)  =  snake_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
nil  =  nil
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa(x1)
cons(x1, x2)  =  cons(x1, x2)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x1, x2, x5)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x1, x4)
produce_snake_in_aaaa(x1, x2, x3, x4)  =  produce_snake_in_aaaa
produce_snake_out_aaaa(x1, x2, x3, x4)  =  produce_snake_out_aaaa
U9_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_aaaa(x7)
part_of_snake_in_aaaa(x1, x2, x3, x4)  =  part_of_snake_in_aaaa
part_of_snake_out_aaaa(x1, x2, x3, x4)  =  part_of_snake_out_aaaa
U11_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_aaaa(x7)
U10_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_aaaa(x7)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x1, x4)
coil_it_in_ag(x1, x2)  =  coil_it_in_ag(x2)
coil_it_out_ag(x1, x2)  =  coil_it_out_ag(x2)
odd  =  odd
U12_ag(x1, x2, x3)  =  U12_ag(x3)
even  =  even
U13_ag(x1, x2, x3)  =  U13_ag(x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x2)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x3, x5)
reverse_in_aaa(x1, x2, x3)  =  reverse_in_aaa
reverse_out_aaa(x1, x2, x3)  =  reverse_out_aaa
U16_aaa(x1, x2, x3, x4, x5)  =  U16_aaa(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa
U14_ag(x1, x2, x3)  =  U14_ag(x3)
snake_out_gaa(x1, x2, x3)  =  snake_out_gaa(x1)
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg(x1, x2, x3)

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

TEST_SNAKE_IN_GGG(Pattern, C, R) → U1_GGG(Pattern, C, R, s2l_in_ga(C, Cols))
TEST_SNAKE_IN_GGG(Pattern, C, R) → S2L_IN_GA(C, Cols)
S2L_IN_GA(s(X), cons(X1, Y)) → U4_GA(X, X1, Y, s2l_in_ga(X, Y))
S2L_IN_GA(s(X), cons(X1, Y)) → S2L_IN_GA(X, Y)
U1_GGG(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_GGG(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U1_GGG(Pattern, C, R, s2l_out_ga(C, Cols)) → S2L_IN_GA(R, Rows)
U2_GGG(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_GGG(Pattern, C, R, snake_in_gaa(Pattern, Cols, Rows))
U2_GGG(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → SNAKE_IN_GAA(Pattern, Cols, Rows)
SNAKE_IN_GAA(Pattern, Cols, Rows) → U5_GAA(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
SNAKE_IN_GAA(Pattern, Cols, Rows) → INFINITE_SNAKE_IN_GAA(Pattern, InfSnake, InfSnake)
INFINITE_SNAKE_IN_GAA(cons(A, R), cons(A, T), S) → U8_GAA(A, R, T, S, infinite_snake_in_gaa(R, T, S))
INFINITE_SNAKE_IN_GAA(cons(A, R), cons(A, T), S) → INFINITE_SNAKE_IN_GAA(R, T, S)
U5_GAA(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_GAA(Pattern, Cols, Rows, produce_snake_in_aaaa(Rows, Cols, InfSnake, Snake))
U5_GAA(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → PRODUCE_SNAKE_IN_AAAA(Rows, Cols, InfSnake, Snake)
PRODUCE_SNAKE_IN_AAAA(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_AAAA(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))
PRODUCE_SNAKE_IN_AAAA(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → PART_OF_SNAKE_IN_AAAA(Cols, InfSnake, NewInfSnake, Part)
PART_OF_SNAKE_IN_AAAA(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → U11_AAAA(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_aaaa(R, Rings, RestSnake, RestRings))
PART_OF_SNAKE_IN_AAAA(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → PART_OF_SNAKE_IN_AAAA(R, Rings, RestSnake, RestRings)
U9_AAAA(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_AAAA(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_aaaa(Rows, Cols, NewInfSnake, Tail))
U9_AAAA(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → PRODUCE_SNAKE_IN_AAAA(Rows, Cols, NewInfSnake, Tail)
U6_GAA(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → U7_GAA(Pattern, Cols, Rows, coil_it_in_ag(Snake, odd))
U6_GAA(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → COIL_IT_IN_AG(Snake, odd)
COIL_IT_IN_AG(cons(Line, Lines), odd) → U12_AG(Line, Lines, coil_it_in_ag(Lines, even))
COIL_IT_IN_AG(cons(Line, Lines), odd) → COIL_IT_IN_AG(Lines, even)
COIL_IT_IN_AG(cons(Line, Lines), even) → U13_AG(Line, Lines, reverse2_in_aa(Line, Line1))
COIL_IT_IN_AG(cons(Line, Lines), even) → REVERSE2_IN_AA(Line, Line1)
REVERSE2_IN_AA(List, Reversed) → U15_AA(List, Reversed, reverse_in_aga(List, nil, Reversed))
REVERSE2_IN_AA(List, Reversed) → REVERSE_IN_AGA(List, nil, Reversed)
REVERSE_IN_AGA(cons(Head, Tail), SoFar, Reversed) → U16_AGA(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
REVERSE_IN_AGA(cons(Head, Tail), SoFar, Reversed) → REVERSE_IN_AAA(Tail, cons(Head, SoFar), Reversed)
REVERSE_IN_AAA(cons(Head, Tail), SoFar, Reversed) → U16_AAA(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
REVERSE_IN_AAA(cons(Head, Tail), SoFar, Reversed) → REVERSE_IN_AAA(Tail, cons(Head, SoFar), Reversed)
U13_AG(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_AG(Line, Lines, coil_it_in_ag(Lines, odd))
U13_AG(Line, Lines, reverse2_out_aa(Line, Line1)) → COIL_IT_IN_AG(Lines, odd)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, nil) → s2l_out_ga(0, nil)
s2l_in_ga(s(X), cons(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), cons(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_gaa(Pattern, Cols, Rows))
snake_in_gaa(Pattern, Cols, Rows) → U5_gaa(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa(nil, S, S) → infinite_snake_out_gaa(nil, S, S)
infinite_snake_in_gaa(cons(A, R), cons(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(cons(A, R), cons(A, T), S)
U5_gaa(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_gaa(Pattern, Cols, Rows, produce_snake_in_aaaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_aaaa(nil, X2, X3, nil) → produce_snake_out_aaaa(nil, X2, X3, nil)
produce_snake_in_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_aaaa(nil, RestSnake, RestSnake, nil) → part_of_snake_out_aaaa(nil, RestSnake, RestSnake, nil)
part_of_snake_in_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_aaaa(R, Rings, RestSnake, RestRings))
U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_aaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings))
U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_aaaa(Rows, Cols, NewInfSnake, Tail))
U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_aaaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail))
U6_gaa(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → U7_gaa(Pattern, Cols, Rows, coil_it_in_ag(Snake, odd))
coil_it_in_ag(nil, X6) → coil_it_out_ag(nil, X6)
coil_it_in_ag(cons(Line, Lines), odd) → U12_ag(Line, Lines, coil_it_in_ag(Lines, even))
coil_it_in_ag(cons(Line, Lines), even) → U13_ag(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, nil, Reversed))
reverse_in_aga(nil, Reversed, Reversed) → reverse_out_aga(nil, Reversed, Reversed)
reverse_in_aga(cons(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
reverse_in_aaa(nil, Reversed, Reversed) → reverse_out_aaa(nil, Reversed, Reversed)
reverse_in_aaa(cons(Head, Tail), SoFar, Reversed) → U16_aaa(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
U16_aaa(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aaa(cons(Head, Tail), SoFar, Reversed)
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aga(cons(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, nil, Reversed)) → reverse2_out_aa(List, Reversed)
U13_ag(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_ag(Line, Lines, coil_it_in_ag(Lines, odd))
U14_ag(Line, Lines, coil_it_out_ag(Lines, odd)) → coil_it_out_ag(cons(Line, Lines), even)
U12_ag(Line, Lines, coil_it_out_ag(Lines, even)) → coil_it_out_ag(cons(Line, Lines), odd)
U7_gaa(Pattern, Cols, Rows, coil_it_out_ag(Snake, odd)) → snake_out_gaa(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_gaa(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x2, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x1)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x1, x4)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x2, x3, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x1, x2, x3, x4)
snake_in_gaa(x1, x2, x3)  =  snake_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
nil  =  nil
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa(x1)
cons(x1, x2)  =  cons(x1, x2)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x1, x2, x5)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x1, x4)
produce_snake_in_aaaa(x1, x2, x3, x4)  =  produce_snake_in_aaaa
produce_snake_out_aaaa(x1, x2, x3, x4)  =  produce_snake_out_aaaa
U9_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_aaaa(x7)
part_of_snake_in_aaaa(x1, x2, x3, x4)  =  part_of_snake_in_aaaa
part_of_snake_out_aaaa(x1, x2, x3, x4)  =  part_of_snake_out_aaaa
U11_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_aaaa(x7)
U10_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_aaaa(x7)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x1, x4)
coil_it_in_ag(x1, x2)  =  coil_it_in_ag(x2)
coil_it_out_ag(x1, x2)  =  coil_it_out_ag(x2)
odd  =  odd
U12_ag(x1, x2, x3)  =  U12_ag(x3)
even  =  even
U13_ag(x1, x2, x3)  =  U13_ag(x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x2)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x3, x5)
reverse_in_aaa(x1, x2, x3)  =  reverse_in_aaa
reverse_out_aaa(x1, x2, x3)  =  reverse_out_aaa
U16_aaa(x1, x2, x3, x4, x5)  =  U16_aaa(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa
U14_ag(x1, x2, x3)  =  U14_ag(x3)
snake_out_gaa(x1, x2, x3)  =  snake_out_gaa(x1)
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg(x1, x2, x3)
TEST_SNAKE_IN_GGG(x1, x2, x3)  =  TEST_SNAKE_IN_GGG(x1, x2, x3)
U1_GGG(x1, x2, x3, x4)  =  U1_GGG(x1, x2, x3, x4)
S2L_IN_GA(x1, x2)  =  S2L_IN_GA(x1)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x1, x4)
U2_GGG(x1, x2, x3, x4, x5)  =  U2_GGG(x1, x2, x3, x5)
U3_GGG(x1, x2, x3, x4)  =  U3_GGG(x1, x2, x3, x4)
SNAKE_IN_GAA(x1, x2, x3)  =  SNAKE_IN_GAA(x1)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x4)
INFINITE_SNAKE_IN_GAA(x1, x2, x3)  =  INFINITE_SNAKE_IN_GAA(x1)
U8_GAA(x1, x2, x3, x4, x5)  =  U8_GAA(x1, x2, x5)
U6_GAA(x1, x2, x3, x4)  =  U6_GAA(x1, x4)
PRODUCE_SNAKE_IN_AAAA(x1, x2, x3, x4)  =  PRODUCE_SNAKE_IN_AAAA
U9_AAAA(x1, x2, x3, x4, x5, x6, x7)  =  U9_AAAA(x7)
PART_OF_SNAKE_IN_AAAA(x1, x2, x3, x4)  =  PART_OF_SNAKE_IN_AAAA
U11_AAAA(x1, x2, x3, x4, x5, x6, x7)  =  U11_AAAA(x7)
U10_AAAA(x1, x2, x3, x4, x5, x6, x7)  =  U10_AAAA(x7)
U7_GAA(x1, x2, x3, x4)  =  U7_GAA(x1, x4)
COIL_IT_IN_AG(x1, x2)  =  COIL_IT_IN_AG(x2)
U12_AG(x1, x2, x3)  =  U12_AG(x3)
U13_AG(x1, x2, x3)  =  U13_AG(x3)
REVERSE2_IN_AA(x1, x2)  =  REVERSE2_IN_AA
U15_AA(x1, x2, x3)  =  U15_AA(x3)
REVERSE_IN_AGA(x1, x2, x3)  =  REVERSE_IN_AGA(x2)
U16_AGA(x1, x2, x3, x4, x5)  =  U16_AGA(x3, x5)
REVERSE_IN_AAA(x1, x2, x3)  =  REVERSE_IN_AAA
U16_AAA(x1, x2, x3, x4, x5)  =  U16_AAA(x5)
U14_AG(x1, x2, x3)  =  U14_AG(x3)

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

(4) Obligation:

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

TEST_SNAKE_IN_GGG(Pattern, C, R) → U1_GGG(Pattern, C, R, s2l_in_ga(C, Cols))
TEST_SNAKE_IN_GGG(Pattern, C, R) → S2L_IN_GA(C, Cols)
S2L_IN_GA(s(X), cons(X1, Y)) → U4_GA(X, X1, Y, s2l_in_ga(X, Y))
S2L_IN_GA(s(X), cons(X1, Y)) → S2L_IN_GA(X, Y)
U1_GGG(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_GGG(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U1_GGG(Pattern, C, R, s2l_out_ga(C, Cols)) → S2L_IN_GA(R, Rows)
U2_GGG(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_GGG(Pattern, C, R, snake_in_gaa(Pattern, Cols, Rows))
U2_GGG(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → SNAKE_IN_GAA(Pattern, Cols, Rows)
SNAKE_IN_GAA(Pattern, Cols, Rows) → U5_GAA(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
SNAKE_IN_GAA(Pattern, Cols, Rows) → INFINITE_SNAKE_IN_GAA(Pattern, InfSnake, InfSnake)
INFINITE_SNAKE_IN_GAA(cons(A, R), cons(A, T), S) → U8_GAA(A, R, T, S, infinite_snake_in_gaa(R, T, S))
INFINITE_SNAKE_IN_GAA(cons(A, R), cons(A, T), S) → INFINITE_SNAKE_IN_GAA(R, T, S)
U5_GAA(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_GAA(Pattern, Cols, Rows, produce_snake_in_aaaa(Rows, Cols, InfSnake, Snake))
U5_GAA(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → PRODUCE_SNAKE_IN_AAAA(Rows, Cols, InfSnake, Snake)
PRODUCE_SNAKE_IN_AAAA(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_AAAA(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))
PRODUCE_SNAKE_IN_AAAA(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → PART_OF_SNAKE_IN_AAAA(Cols, InfSnake, NewInfSnake, Part)
PART_OF_SNAKE_IN_AAAA(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → U11_AAAA(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_aaaa(R, Rings, RestSnake, RestRings))
PART_OF_SNAKE_IN_AAAA(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → PART_OF_SNAKE_IN_AAAA(R, Rings, RestSnake, RestRings)
U9_AAAA(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_AAAA(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_aaaa(Rows, Cols, NewInfSnake, Tail))
U9_AAAA(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → PRODUCE_SNAKE_IN_AAAA(Rows, Cols, NewInfSnake, Tail)
U6_GAA(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → U7_GAA(Pattern, Cols, Rows, coil_it_in_ag(Snake, odd))
U6_GAA(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → COIL_IT_IN_AG(Snake, odd)
COIL_IT_IN_AG(cons(Line, Lines), odd) → U12_AG(Line, Lines, coil_it_in_ag(Lines, even))
COIL_IT_IN_AG(cons(Line, Lines), odd) → COIL_IT_IN_AG(Lines, even)
COIL_IT_IN_AG(cons(Line, Lines), even) → U13_AG(Line, Lines, reverse2_in_aa(Line, Line1))
COIL_IT_IN_AG(cons(Line, Lines), even) → REVERSE2_IN_AA(Line, Line1)
REVERSE2_IN_AA(List, Reversed) → U15_AA(List, Reversed, reverse_in_aga(List, nil, Reversed))
REVERSE2_IN_AA(List, Reversed) → REVERSE_IN_AGA(List, nil, Reversed)
REVERSE_IN_AGA(cons(Head, Tail), SoFar, Reversed) → U16_AGA(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
REVERSE_IN_AGA(cons(Head, Tail), SoFar, Reversed) → REVERSE_IN_AAA(Tail, cons(Head, SoFar), Reversed)
REVERSE_IN_AAA(cons(Head, Tail), SoFar, Reversed) → U16_AAA(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
REVERSE_IN_AAA(cons(Head, Tail), SoFar, Reversed) → REVERSE_IN_AAA(Tail, cons(Head, SoFar), Reversed)
U13_AG(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_AG(Line, Lines, coil_it_in_ag(Lines, odd))
U13_AG(Line, Lines, reverse2_out_aa(Line, Line1)) → COIL_IT_IN_AG(Lines, odd)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, nil) → s2l_out_ga(0, nil)
s2l_in_ga(s(X), cons(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), cons(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_gaa(Pattern, Cols, Rows))
snake_in_gaa(Pattern, Cols, Rows) → U5_gaa(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa(nil, S, S) → infinite_snake_out_gaa(nil, S, S)
infinite_snake_in_gaa(cons(A, R), cons(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(cons(A, R), cons(A, T), S)
U5_gaa(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_gaa(Pattern, Cols, Rows, produce_snake_in_aaaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_aaaa(nil, X2, X3, nil) → produce_snake_out_aaaa(nil, X2, X3, nil)
produce_snake_in_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_aaaa(nil, RestSnake, RestSnake, nil) → part_of_snake_out_aaaa(nil, RestSnake, RestSnake, nil)
part_of_snake_in_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_aaaa(R, Rings, RestSnake, RestRings))
U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_aaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings))
U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_aaaa(Rows, Cols, NewInfSnake, Tail))
U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_aaaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail))
U6_gaa(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → U7_gaa(Pattern, Cols, Rows, coil_it_in_ag(Snake, odd))
coil_it_in_ag(nil, X6) → coil_it_out_ag(nil, X6)
coil_it_in_ag(cons(Line, Lines), odd) → U12_ag(Line, Lines, coil_it_in_ag(Lines, even))
coil_it_in_ag(cons(Line, Lines), even) → U13_ag(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, nil, Reversed))
reverse_in_aga(nil, Reversed, Reversed) → reverse_out_aga(nil, Reversed, Reversed)
reverse_in_aga(cons(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
reverse_in_aaa(nil, Reversed, Reversed) → reverse_out_aaa(nil, Reversed, Reversed)
reverse_in_aaa(cons(Head, Tail), SoFar, Reversed) → U16_aaa(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
U16_aaa(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aaa(cons(Head, Tail), SoFar, Reversed)
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aga(cons(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, nil, Reversed)) → reverse2_out_aa(List, Reversed)
U13_ag(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_ag(Line, Lines, coil_it_in_ag(Lines, odd))
U14_ag(Line, Lines, coil_it_out_ag(Lines, odd)) → coil_it_out_ag(cons(Line, Lines), even)
U12_ag(Line, Lines, coil_it_out_ag(Lines, even)) → coil_it_out_ag(cons(Line, Lines), odd)
U7_gaa(Pattern, Cols, Rows, coil_it_out_ag(Snake, odd)) → snake_out_gaa(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_gaa(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x2, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x1)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x1, x4)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x2, x3, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x1, x2, x3, x4)
snake_in_gaa(x1, x2, x3)  =  snake_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
nil  =  nil
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa(x1)
cons(x1, x2)  =  cons(x1, x2)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x1, x2, x5)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x1, x4)
produce_snake_in_aaaa(x1, x2, x3, x4)  =  produce_snake_in_aaaa
produce_snake_out_aaaa(x1, x2, x3, x4)  =  produce_snake_out_aaaa
U9_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_aaaa(x7)
part_of_snake_in_aaaa(x1, x2, x3, x4)  =  part_of_snake_in_aaaa
part_of_snake_out_aaaa(x1, x2, x3, x4)  =  part_of_snake_out_aaaa
U11_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_aaaa(x7)
U10_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_aaaa(x7)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x1, x4)
coil_it_in_ag(x1, x2)  =  coil_it_in_ag(x2)
coil_it_out_ag(x1, x2)  =  coil_it_out_ag(x2)
odd  =  odd
U12_ag(x1, x2, x3)  =  U12_ag(x3)
even  =  even
U13_ag(x1, x2, x3)  =  U13_ag(x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x2)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x3, x5)
reverse_in_aaa(x1, x2, x3)  =  reverse_in_aaa
reverse_out_aaa(x1, x2, x3)  =  reverse_out_aaa
U16_aaa(x1, x2, x3, x4, x5)  =  U16_aaa(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa
U14_ag(x1, x2, x3)  =  U14_ag(x3)
snake_out_gaa(x1, x2, x3)  =  snake_out_gaa(x1)
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg(x1, x2, x3)
TEST_SNAKE_IN_GGG(x1, x2, x3)  =  TEST_SNAKE_IN_GGG(x1, x2, x3)
U1_GGG(x1, x2, x3, x4)  =  U1_GGG(x1, x2, x3, x4)
S2L_IN_GA(x1, x2)  =  S2L_IN_GA(x1)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x1, x4)
U2_GGG(x1, x2, x3, x4, x5)  =  U2_GGG(x1, x2, x3, x5)
U3_GGG(x1, x2, x3, x4)  =  U3_GGG(x1, x2, x3, x4)
SNAKE_IN_GAA(x1, x2, x3)  =  SNAKE_IN_GAA(x1)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x4)
INFINITE_SNAKE_IN_GAA(x1, x2, x3)  =  INFINITE_SNAKE_IN_GAA(x1)
U8_GAA(x1, x2, x3, x4, x5)  =  U8_GAA(x1, x2, x5)
U6_GAA(x1, x2, x3, x4)  =  U6_GAA(x1, x4)
PRODUCE_SNAKE_IN_AAAA(x1, x2, x3, x4)  =  PRODUCE_SNAKE_IN_AAAA
U9_AAAA(x1, x2, x3, x4, x5, x6, x7)  =  U9_AAAA(x7)
PART_OF_SNAKE_IN_AAAA(x1, x2, x3, x4)  =  PART_OF_SNAKE_IN_AAAA
U11_AAAA(x1, x2, x3, x4, x5, x6, x7)  =  U11_AAAA(x7)
U10_AAAA(x1, x2, x3, x4, x5, x6, x7)  =  U10_AAAA(x7)
U7_GAA(x1, x2, x3, x4)  =  U7_GAA(x1, x4)
COIL_IT_IN_AG(x1, x2)  =  COIL_IT_IN_AG(x2)
U12_AG(x1, x2, x3)  =  U12_AG(x3)
U13_AG(x1, x2, x3)  =  U13_AG(x3)
REVERSE2_IN_AA(x1, x2)  =  REVERSE2_IN_AA
U15_AA(x1, x2, x3)  =  U15_AA(x3)
REVERSE_IN_AGA(x1, x2, x3)  =  REVERSE_IN_AGA(x2)
U16_AGA(x1, x2, x3, x4, x5)  =  U16_AGA(x3, x5)
REVERSE_IN_AAA(x1, x2, x3)  =  REVERSE_IN_AAA
U16_AAA(x1, x2, x3, x4, x5)  =  U16_AAA(x5)
U14_AG(x1, x2, x3)  =  U14_AG(x3)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 6 SCCs with 25 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

REVERSE_IN_AAA(cons(Head, Tail), SoFar, Reversed) → REVERSE_IN_AAA(Tail, cons(Head, SoFar), Reversed)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, nil) → s2l_out_ga(0, nil)
s2l_in_ga(s(X), cons(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), cons(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_gaa(Pattern, Cols, Rows))
snake_in_gaa(Pattern, Cols, Rows) → U5_gaa(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa(nil, S, S) → infinite_snake_out_gaa(nil, S, S)
infinite_snake_in_gaa(cons(A, R), cons(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(cons(A, R), cons(A, T), S)
U5_gaa(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_gaa(Pattern, Cols, Rows, produce_snake_in_aaaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_aaaa(nil, X2, X3, nil) → produce_snake_out_aaaa(nil, X2, X3, nil)
produce_snake_in_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_aaaa(nil, RestSnake, RestSnake, nil) → part_of_snake_out_aaaa(nil, RestSnake, RestSnake, nil)
part_of_snake_in_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_aaaa(R, Rings, RestSnake, RestRings))
U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_aaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings))
U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_aaaa(Rows, Cols, NewInfSnake, Tail))
U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_aaaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail))
U6_gaa(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → U7_gaa(Pattern, Cols, Rows, coil_it_in_ag(Snake, odd))
coil_it_in_ag(nil, X6) → coil_it_out_ag(nil, X6)
coil_it_in_ag(cons(Line, Lines), odd) → U12_ag(Line, Lines, coil_it_in_ag(Lines, even))
coil_it_in_ag(cons(Line, Lines), even) → U13_ag(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, nil, Reversed))
reverse_in_aga(nil, Reversed, Reversed) → reverse_out_aga(nil, Reversed, Reversed)
reverse_in_aga(cons(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
reverse_in_aaa(nil, Reversed, Reversed) → reverse_out_aaa(nil, Reversed, Reversed)
reverse_in_aaa(cons(Head, Tail), SoFar, Reversed) → U16_aaa(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
U16_aaa(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aaa(cons(Head, Tail), SoFar, Reversed)
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aga(cons(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, nil, Reversed)) → reverse2_out_aa(List, Reversed)
U13_ag(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_ag(Line, Lines, coil_it_in_ag(Lines, odd))
U14_ag(Line, Lines, coil_it_out_ag(Lines, odd)) → coil_it_out_ag(cons(Line, Lines), even)
U12_ag(Line, Lines, coil_it_out_ag(Lines, even)) → coil_it_out_ag(cons(Line, Lines), odd)
U7_gaa(Pattern, Cols, Rows, coil_it_out_ag(Snake, odd)) → snake_out_gaa(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_gaa(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x2, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x1)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x1, x4)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x2, x3, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x1, x2, x3, x4)
snake_in_gaa(x1, x2, x3)  =  snake_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
nil  =  nil
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa(x1)
cons(x1, x2)  =  cons(x1, x2)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x1, x2, x5)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x1, x4)
produce_snake_in_aaaa(x1, x2, x3, x4)  =  produce_snake_in_aaaa
produce_snake_out_aaaa(x1, x2, x3, x4)  =  produce_snake_out_aaaa
U9_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_aaaa(x7)
part_of_snake_in_aaaa(x1, x2, x3, x4)  =  part_of_snake_in_aaaa
part_of_snake_out_aaaa(x1, x2, x3, x4)  =  part_of_snake_out_aaaa
U11_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_aaaa(x7)
U10_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_aaaa(x7)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x1, x4)
coil_it_in_ag(x1, x2)  =  coil_it_in_ag(x2)
coil_it_out_ag(x1, x2)  =  coil_it_out_ag(x2)
odd  =  odd
U12_ag(x1, x2, x3)  =  U12_ag(x3)
even  =  even
U13_ag(x1, x2, x3)  =  U13_ag(x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x2)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x3, x5)
reverse_in_aaa(x1, x2, x3)  =  reverse_in_aaa
reverse_out_aaa(x1, x2, x3)  =  reverse_out_aaa
U16_aaa(x1, x2, x3, x4, x5)  =  U16_aaa(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa
U14_ag(x1, x2, x3)  =  U14_ag(x3)
snake_out_gaa(x1, x2, x3)  =  snake_out_gaa(x1)
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg(x1, x2, x3)
REVERSE_IN_AAA(x1, x2, x3)  =  REVERSE_IN_AAA

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

(8) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(9) Obligation:

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

REVERSE_IN_AAA(cons(Head, Tail), SoFar, Reversed) → REVERSE_IN_AAA(Tail, cons(Head, SoFar), Reversed)

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

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

(10) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(11) Obligation:

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

REVERSE_IN_AAA → REVERSE_IN_AAA

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(12) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = REVERSE_IN_AAA evaluates to t =REVERSE_IN_AAA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Semiunifier: [ ]
• Matcher: [ ]

---

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from REVERSE_IN_AAA to REVERSE_IN_AAA.

(13) FALSE

(14) Obligation:

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

COIL_IT_IN_AG(cons(Line, Lines), odd) → COIL_IT_IN_AG(Lines, even)
COIL_IT_IN_AG(cons(Line, Lines), even) → U13_AG(Line, Lines, reverse2_in_aa(Line, Line1))
U13_AG(Line, Lines, reverse2_out_aa(Line, Line1)) → COIL_IT_IN_AG(Lines, odd)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, nil) → s2l_out_ga(0, nil)
s2l_in_ga(s(X), cons(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), cons(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_gaa(Pattern, Cols, Rows))
snake_in_gaa(Pattern, Cols, Rows) → U5_gaa(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa(nil, S, S) → infinite_snake_out_gaa(nil, S, S)
infinite_snake_in_gaa(cons(A, R), cons(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(cons(A, R), cons(A, T), S)
U5_gaa(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_gaa(Pattern, Cols, Rows, produce_snake_in_aaaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_aaaa(nil, X2, X3, nil) → produce_snake_out_aaaa(nil, X2, X3, nil)
produce_snake_in_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_aaaa(nil, RestSnake, RestSnake, nil) → part_of_snake_out_aaaa(nil, RestSnake, RestSnake, nil)
part_of_snake_in_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_aaaa(R, Rings, RestSnake, RestRings))
U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_aaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings))
U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_aaaa(Rows, Cols, NewInfSnake, Tail))
U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_aaaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail))
U6_gaa(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → U7_gaa(Pattern, Cols, Rows, coil_it_in_ag(Snake, odd))
coil_it_in_ag(nil, X6) → coil_it_out_ag(nil, X6)
coil_it_in_ag(cons(Line, Lines), odd) → U12_ag(Line, Lines, coil_it_in_ag(Lines, even))
coil_it_in_ag(cons(Line, Lines), even) → U13_ag(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, nil, Reversed))
reverse_in_aga(nil, Reversed, Reversed) → reverse_out_aga(nil, Reversed, Reversed)
reverse_in_aga(cons(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
reverse_in_aaa(nil, Reversed, Reversed) → reverse_out_aaa(nil, Reversed, Reversed)
reverse_in_aaa(cons(Head, Tail), SoFar, Reversed) → U16_aaa(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
U16_aaa(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aaa(cons(Head, Tail), SoFar, Reversed)
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aga(cons(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, nil, Reversed)) → reverse2_out_aa(List, Reversed)
U13_ag(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_ag(Line, Lines, coil_it_in_ag(Lines, odd))
U14_ag(Line, Lines, coil_it_out_ag(Lines, odd)) → coil_it_out_ag(cons(Line, Lines), even)
U12_ag(Line, Lines, coil_it_out_ag(Lines, even)) → coil_it_out_ag(cons(Line, Lines), odd)
U7_gaa(Pattern, Cols, Rows, coil_it_out_ag(Snake, odd)) → snake_out_gaa(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_gaa(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x2, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x1)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x1, x4)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x2, x3, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x1, x2, x3, x4)
snake_in_gaa(x1, x2, x3)  =  snake_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
nil  =  nil
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa(x1)
cons(x1, x2)  =  cons(x1, x2)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x1, x2, x5)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x1, x4)
produce_snake_in_aaaa(x1, x2, x3, x4)  =  produce_snake_in_aaaa
produce_snake_out_aaaa(x1, x2, x3, x4)  =  produce_snake_out_aaaa
U9_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_aaaa(x7)
part_of_snake_in_aaaa(x1, x2, x3, x4)  =  part_of_snake_in_aaaa
part_of_snake_out_aaaa(x1, x2, x3, x4)  =  part_of_snake_out_aaaa
U11_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_aaaa(x7)
U10_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_aaaa(x7)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x1, x4)
coil_it_in_ag(x1, x2)  =  coil_it_in_ag(x2)
coil_it_out_ag(x1, x2)  =  coil_it_out_ag(x2)
odd  =  odd
U12_ag(x1, x2, x3)  =  U12_ag(x3)
even  =  even
U13_ag(x1, x2, x3)  =  U13_ag(x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x2)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x3, x5)
reverse_in_aaa(x1, x2, x3)  =  reverse_in_aaa
reverse_out_aaa(x1, x2, x3)  =  reverse_out_aaa
U16_aaa(x1, x2, x3, x4, x5)  =  U16_aaa(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa
U14_ag(x1, x2, x3)  =  U14_ag(x3)
snake_out_gaa(x1, x2, x3)  =  snake_out_gaa(x1)
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg(x1, x2, x3)
COIL_IT_IN_AG(x1, x2)  =  COIL_IT_IN_AG(x2)
U13_AG(x1, x2, x3)  =  U13_AG(x3)

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

(15) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(16) Obligation:

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

COIL_IT_IN_AG(cons(Line, Lines), odd) → COIL_IT_IN_AG(Lines, even)
COIL_IT_IN_AG(cons(Line, Lines), even) → U13_AG(Line, Lines, reverse2_in_aa(Line, Line1))
U13_AG(Line, Lines, reverse2_out_aa(Line, Line1)) → COIL_IT_IN_AG(Lines, odd)

The TRS R consists of the following rules:

reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, nil, Reversed))
U15_aa(List, Reversed, reverse_out_aga(List, nil, Reversed)) → reverse2_out_aa(List, Reversed)
reverse_in_aga(nil, Reversed, Reversed) → reverse_out_aga(nil, Reversed, Reversed)
reverse_in_aga(cons(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aga(cons(Head, Tail), SoFar, Reversed)
reverse_in_aaa(nil, Reversed, Reversed) → reverse_out_aaa(nil, Reversed, Reversed)
reverse_in_aaa(cons(Head, Tail), SoFar, Reversed) → U16_aaa(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
U16_aaa(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aaa(cons(Head, Tail), SoFar, Reversed)

The argument filtering Pi contains the following mapping:
nil  =  nil
cons(x1, x2)  =  cons(x1, x2)
odd  =  odd
even  =  even
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x2)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x3, x5)
reverse_in_aaa(x1, x2, x3)  =  reverse_in_aaa
reverse_out_aaa(x1, x2, x3)  =  reverse_out_aaa
U16_aaa(x1, x2, x3, x4, x5)  =  U16_aaa(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa
COIL_IT_IN_AG(x1, x2)  =  COIL_IT_IN_AG(x2)
U13_AG(x1, x2, x3)  =  U13_AG(x3)

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

(17) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(18) Obligation:

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

COIL_IT_IN_AG(odd) → COIL_IT_IN_AG(even)
COIL_IT_IN_AG(even) → U13_AG(reverse2_in_aa)
U13_AG(reverse2_out_aa) → COIL_IT_IN_AG(odd)

The TRS R consists of the following rules:

reverse2_in_aa → U15_aa(reverse_in_aga(nil))
U15_aa(reverse_out_aga(nil)) → reverse2_out_aa
reverse_in_aga(Reversed) → reverse_out_aga(Reversed)
reverse_in_aga(SoFar) → U16_aga(SoFar, reverse_in_aaa)
U16_aga(SoFar, reverse_out_aaa) → reverse_out_aga(SoFar)
reverse_in_aaa → reverse_out_aaa
reverse_in_aaa → U16_aaa(reverse_in_aaa)
U16_aaa(reverse_out_aaa) → reverse_out_aaa

The set Q consists of the following terms:

reverse2_in_aa
U15_aa(x0)
reverse_in_aga(x0)
U16_aga(x0, x1)
reverse_in_aaa
U16_aaa(x0)

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

(19) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule COIL_IT_IN_AG(even) → U13_AG(reverse2_in_aa) at position [0] we obtained the following new rules [LPAR04]:

COIL_IT_IN_AG(even) → U13_AG(U15_aa(reverse_in_aga(nil)))

(20) Obligation:

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

COIL_IT_IN_AG(odd) → COIL_IT_IN_AG(even)
U13_AG(reverse2_out_aa) → COIL_IT_IN_AG(odd)
COIL_IT_IN_AG(even) → U13_AG(U15_aa(reverse_in_aga(nil)))

The TRS R consists of the following rules:

reverse2_in_aa → U15_aa(reverse_in_aga(nil))
U15_aa(reverse_out_aga(nil)) → reverse2_out_aa
reverse_in_aga(Reversed) → reverse_out_aga(Reversed)
reverse_in_aga(SoFar) → U16_aga(SoFar, reverse_in_aaa)
U16_aga(SoFar, reverse_out_aaa) → reverse_out_aga(SoFar)
reverse_in_aaa → reverse_out_aaa
reverse_in_aaa → U16_aaa(reverse_in_aaa)
U16_aaa(reverse_out_aaa) → reverse_out_aaa

The set Q consists of the following terms:

reverse2_in_aa
U15_aa(x0)
reverse_in_aga(x0)
U16_aga(x0, x1)
reverse_in_aaa
U16_aaa(x0)

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

(21) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(22) Obligation:

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

COIL_IT_IN_AG(odd) → COIL_IT_IN_AG(even)
U13_AG(reverse2_out_aa) → COIL_IT_IN_AG(odd)
COIL_IT_IN_AG(even) → U13_AG(U15_aa(reverse_in_aga(nil)))

The TRS R consists of the following rules:

reverse_in_aga(Reversed) → reverse_out_aga(Reversed)
reverse_in_aga(SoFar) → U16_aga(SoFar, reverse_in_aaa)
U15_aa(reverse_out_aga(nil)) → reverse2_out_aa
reverse_in_aaa → reverse_out_aaa
reverse_in_aaa → U16_aaa(reverse_in_aaa)
U16_aga(SoFar, reverse_out_aaa) → reverse_out_aga(SoFar)
U16_aaa(reverse_out_aaa) → reverse_out_aaa

The set Q consists of the following terms:

reverse2_in_aa
U15_aa(x0)
reverse_in_aga(x0)
U16_aga(x0, x1)
reverse_in_aaa
U16_aaa(x0)

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

(23) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

reverse2_in_aa

(24) Obligation:

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

COIL_IT_IN_AG(odd) → COIL_IT_IN_AG(even)
U13_AG(reverse2_out_aa) → COIL_IT_IN_AG(odd)
COIL_IT_IN_AG(even) → U13_AG(U15_aa(reverse_in_aga(nil)))

The TRS R consists of the following rules:

reverse_in_aga(Reversed) → reverse_out_aga(Reversed)
reverse_in_aga(SoFar) → U16_aga(SoFar, reverse_in_aaa)
U15_aa(reverse_out_aga(nil)) → reverse2_out_aa
reverse_in_aaa → reverse_out_aaa
reverse_in_aaa → U16_aaa(reverse_in_aaa)
U16_aga(SoFar, reverse_out_aaa) → reverse_out_aga(SoFar)
U16_aaa(reverse_out_aaa) → reverse_out_aaa

The set Q consists of the following terms:

U15_aa(x0)
reverse_in_aga(x0)
U16_aga(x0, x1)
reverse_in_aaa
U16_aaa(x0)

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

(25) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = U13_AG(U15_aa(reverse_in_aga(nil))) evaluates to t =U13_AG(U15_aa(reverse_in_aga(nil)))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Semiunifier: [ ]
• Matcher: [ ]

---

Rewriting sequence

U13_AG(U15_aa(reverse_in_aga(nil))) → U13_AG(U15_aa(reverse_out_aga(nil)))
with rule reverse_in_aga(Reversed) → reverse_out_aga(Reversed) at position [0,0] and matcher [Reversed / nil]

U13_AG(U15_aa(reverse_out_aga(nil))) → U13_AG(reverse2_out_aa)
with rule U15_aa(reverse_out_aga(nil)) → reverse2_out_aa at position [0] and matcher [ ]

U13_AG(reverse2_out_aa) → COIL_IT_IN_AG(odd)
with rule U13_AG(reverse2_out_aa) → COIL_IT_IN_AG(odd) at position [] and matcher [ ]

COIL_IT_IN_AG(odd) → COIL_IT_IN_AG(even)
with rule COIL_IT_IN_AG(odd) → COIL_IT_IN_AG(even) at position [] and matcher [ ]

COIL_IT_IN_AG(even) → U13_AG(U15_aa(reverse_in_aga(nil)))
with rule COIL_IT_IN_AG(even) → U13_AG(U15_aa(reverse_in_aga(nil)))

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.

(26) FALSE

(27) Obligation:

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

PART_OF_SNAKE_IN_AAAA(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → PART_OF_SNAKE_IN_AAAA(R, Rings, RestSnake, RestRings)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, nil) → s2l_out_ga(0, nil)
s2l_in_ga(s(X), cons(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), cons(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_gaa(Pattern, Cols, Rows))
snake_in_gaa(Pattern, Cols, Rows) → U5_gaa(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa(nil, S, S) → infinite_snake_out_gaa(nil, S, S)
infinite_snake_in_gaa(cons(A, R), cons(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(cons(A, R), cons(A, T), S)
U5_gaa(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_gaa(Pattern, Cols, Rows, produce_snake_in_aaaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_aaaa(nil, X2, X3, nil) → produce_snake_out_aaaa(nil, X2, X3, nil)
produce_snake_in_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_aaaa(nil, RestSnake, RestSnake, nil) → part_of_snake_out_aaaa(nil, RestSnake, RestSnake, nil)
part_of_snake_in_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_aaaa(R, Rings, RestSnake, RestRings))
U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_aaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings))
U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_aaaa(Rows, Cols, NewInfSnake, Tail))
U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_aaaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail))
U6_gaa(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → U7_gaa(Pattern, Cols, Rows, coil_it_in_ag(Snake, odd))
coil_it_in_ag(nil, X6) → coil_it_out_ag(nil, X6)
coil_it_in_ag(cons(Line, Lines), odd) → U12_ag(Line, Lines, coil_it_in_ag(Lines, even))
coil_it_in_ag(cons(Line, Lines), even) → U13_ag(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, nil, Reversed))
reverse_in_aga(nil, Reversed, Reversed) → reverse_out_aga(nil, Reversed, Reversed)
reverse_in_aga(cons(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
reverse_in_aaa(nil, Reversed, Reversed) → reverse_out_aaa(nil, Reversed, Reversed)
reverse_in_aaa(cons(Head, Tail), SoFar, Reversed) → U16_aaa(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
U16_aaa(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aaa(cons(Head, Tail), SoFar, Reversed)
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aga(cons(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, nil, Reversed)) → reverse2_out_aa(List, Reversed)
U13_ag(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_ag(Line, Lines, coil_it_in_ag(Lines, odd))
U14_ag(Line, Lines, coil_it_out_ag(Lines, odd)) → coil_it_out_ag(cons(Line, Lines), even)
U12_ag(Line, Lines, coil_it_out_ag(Lines, even)) → coil_it_out_ag(cons(Line, Lines), odd)
U7_gaa(Pattern, Cols, Rows, coil_it_out_ag(Snake, odd)) → snake_out_gaa(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_gaa(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x2, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x1)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x1, x4)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x2, x3, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x1, x2, x3, x4)
snake_in_gaa(x1, x2, x3)  =  snake_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
nil  =  nil
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa(x1)
cons(x1, x2)  =  cons(x1, x2)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x1, x2, x5)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x1, x4)
produce_snake_in_aaaa(x1, x2, x3, x4)  =  produce_snake_in_aaaa
produce_snake_out_aaaa(x1, x2, x3, x4)  =  produce_snake_out_aaaa
U9_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_aaaa(x7)
part_of_snake_in_aaaa(x1, x2, x3, x4)  =  part_of_snake_in_aaaa
part_of_snake_out_aaaa(x1, x2, x3, x4)  =  part_of_snake_out_aaaa
U11_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_aaaa(x7)
U10_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_aaaa(x7)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x1, x4)
coil_it_in_ag(x1, x2)  =  coil_it_in_ag(x2)
coil_it_out_ag(x1, x2)  =  coil_it_out_ag(x2)
odd  =  odd
U12_ag(x1, x2, x3)  =  U12_ag(x3)
even  =  even
U13_ag(x1, x2, x3)  =  U13_ag(x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x2)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x3, x5)
reverse_in_aaa(x1, x2, x3)  =  reverse_in_aaa
reverse_out_aaa(x1, x2, x3)  =  reverse_out_aaa
U16_aaa(x1, x2, x3, x4, x5)  =  U16_aaa(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa
U14_ag(x1, x2, x3)  =  U14_ag(x3)
snake_out_gaa(x1, x2, x3)  =  snake_out_gaa(x1)
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg(x1, x2, x3)
PART_OF_SNAKE_IN_AAAA(x1, x2, x3, x4)  =  PART_OF_SNAKE_IN_AAAA

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

(28) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(29) Obligation:

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

PART_OF_SNAKE_IN_AAAA(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → PART_OF_SNAKE_IN_AAAA(R, Rings, RestSnake, RestRings)

R is empty.
The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
PART_OF_SNAKE_IN_AAAA(x1, x2, x3, x4)  =  PART_OF_SNAKE_IN_AAAA

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

(30) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(31) Obligation:

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

PART_OF_SNAKE_IN_AAAA → PART_OF_SNAKE_IN_AAAA

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(32) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = PART_OF_SNAKE_IN_AAAA evaluates to t =PART_OF_SNAKE_IN_AAAA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Semiunifier: [ ]
• Matcher: [ ]

---

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from PART_OF_SNAKE_IN_AAAA to PART_OF_SNAKE_IN_AAAA.

(33) FALSE

(34) Obligation:

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

U9_AAAA(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → PRODUCE_SNAKE_IN_AAAA(Rows, Cols, NewInfSnake, Tail)
PRODUCE_SNAKE_IN_AAAA(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_AAAA(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, nil) → s2l_out_ga(0, nil)
s2l_in_ga(s(X), cons(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), cons(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_gaa(Pattern, Cols, Rows))
snake_in_gaa(Pattern, Cols, Rows) → U5_gaa(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa(nil, S, S) → infinite_snake_out_gaa(nil, S, S)
infinite_snake_in_gaa(cons(A, R), cons(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(cons(A, R), cons(A, T), S)
U5_gaa(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_gaa(Pattern, Cols, Rows, produce_snake_in_aaaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_aaaa(nil, X2, X3, nil) → produce_snake_out_aaaa(nil, X2, X3, nil)
produce_snake_in_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_aaaa(nil, RestSnake, RestSnake, nil) → part_of_snake_out_aaaa(nil, RestSnake, RestSnake, nil)
part_of_snake_in_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_aaaa(R, Rings, RestSnake, RestRings))
U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_aaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings))
U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_aaaa(Rows, Cols, NewInfSnake, Tail))
U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_aaaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail))
U6_gaa(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → U7_gaa(Pattern, Cols, Rows, coil_it_in_ag(Snake, odd))
coil_it_in_ag(nil, X6) → coil_it_out_ag(nil, X6)
coil_it_in_ag(cons(Line, Lines), odd) → U12_ag(Line, Lines, coil_it_in_ag(Lines, even))
coil_it_in_ag(cons(Line, Lines), even) → U13_ag(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, nil, Reversed))
reverse_in_aga(nil, Reversed, Reversed) → reverse_out_aga(nil, Reversed, Reversed)
reverse_in_aga(cons(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
reverse_in_aaa(nil, Reversed, Reversed) → reverse_out_aaa(nil, Reversed, Reversed)
reverse_in_aaa(cons(Head, Tail), SoFar, Reversed) → U16_aaa(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
U16_aaa(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aaa(cons(Head, Tail), SoFar, Reversed)
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aga(cons(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, nil, Reversed)) → reverse2_out_aa(List, Reversed)
U13_ag(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_ag(Line, Lines, coil_it_in_ag(Lines, odd))
U14_ag(Line, Lines, coil_it_out_ag(Lines, odd)) → coil_it_out_ag(cons(Line, Lines), even)
U12_ag(Line, Lines, coil_it_out_ag(Lines, even)) → coil_it_out_ag(cons(Line, Lines), odd)
U7_gaa(Pattern, Cols, Rows, coil_it_out_ag(Snake, odd)) → snake_out_gaa(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_gaa(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x2, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x1)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x1, x4)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x2, x3, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x1, x2, x3, x4)
snake_in_gaa(x1, x2, x3)  =  snake_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
nil  =  nil
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa(x1)
cons(x1, x2)  =  cons(x1, x2)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x1, x2, x5)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x1, x4)
produce_snake_in_aaaa(x1, x2, x3, x4)  =  produce_snake_in_aaaa
produce_snake_out_aaaa(x1, x2, x3, x4)  =  produce_snake_out_aaaa
U9_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_aaaa(x7)
part_of_snake_in_aaaa(x1, x2, x3, x4)  =  part_of_snake_in_aaaa
part_of_snake_out_aaaa(x1, x2, x3, x4)  =  part_of_snake_out_aaaa
U11_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_aaaa(x7)
U10_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_aaaa(x7)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x1, x4)
coil_it_in_ag(x1, x2)  =  coil_it_in_ag(x2)
coil_it_out_ag(x1, x2)  =  coil_it_out_ag(x2)
odd  =  odd
U12_ag(x1, x2, x3)  =  U12_ag(x3)
even  =  even
U13_ag(x1, x2, x3)  =  U13_ag(x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x2)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x3, x5)
reverse_in_aaa(x1, x2, x3)  =  reverse_in_aaa
reverse_out_aaa(x1, x2, x3)  =  reverse_out_aaa
U16_aaa(x1, x2, x3, x4, x5)  =  U16_aaa(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa
U14_ag(x1, x2, x3)  =  U14_ag(x3)
snake_out_gaa(x1, x2, x3)  =  snake_out_gaa(x1)
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg(x1, x2, x3)
PRODUCE_SNAKE_IN_AAAA(x1, x2, x3, x4)  =  PRODUCE_SNAKE_IN_AAAA
U9_AAAA(x1, x2, x3, x4, x5, x6, x7)  =  U9_AAAA(x7)

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

(35) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(36) Obligation:

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

U9_AAAA(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → PRODUCE_SNAKE_IN_AAAA(Rows, Cols, NewInfSnake, Tail)
PRODUCE_SNAKE_IN_AAAA(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_AAAA(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))

The TRS R consists of the following rules:

part_of_snake_in_aaaa(nil, RestSnake, RestSnake, nil) → part_of_snake_out_aaaa(nil, RestSnake, RestSnake, nil)
part_of_snake_in_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_aaaa(R, Rings, RestSnake, RestRings))
U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_aaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings))

The argument filtering Pi contains the following mapping:
nil  =  nil
cons(x1, x2)  =  cons(x1, x2)
part_of_snake_in_aaaa(x1, x2, x3, x4)  =  part_of_snake_in_aaaa
part_of_snake_out_aaaa(x1, x2, x3, x4)  =  part_of_snake_out_aaaa
U11_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_aaaa(x7)
PRODUCE_SNAKE_IN_AAAA(x1, x2, x3, x4)  =  PRODUCE_SNAKE_IN_AAAA
U9_AAAA(x1, x2, x3, x4, x5, x6, x7)  =  U9_AAAA(x7)

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

(37) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(38) Obligation:

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

U9_AAAA(part_of_snake_out_aaaa) → PRODUCE_SNAKE_IN_AAAA
PRODUCE_SNAKE_IN_AAAA → U9_AAAA(part_of_snake_in_aaaa)

The TRS R consists of the following rules:

part_of_snake_in_aaaa → part_of_snake_out_aaaa
part_of_snake_in_aaaa → U11_aaaa(part_of_snake_in_aaaa)
U11_aaaa(part_of_snake_out_aaaa) → part_of_snake_out_aaaa

The set Q consists of the following terms:

part_of_snake_in_aaaa
U11_aaaa(x0)

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

(39) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule PRODUCE_SNAKE_IN_AAAA → U9_AAAA(part_of_snake_in_aaaa) at position [0] we obtained the following new rules [LPAR04]:

PRODUCE_SNAKE_IN_AAAA → U9_AAAA(part_of_snake_out_aaaa)
PRODUCE_SNAKE_IN_AAAA → U9_AAAA(U11_aaaa(part_of_snake_in_aaaa))

(40) Obligation:

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

U9_AAAA(part_of_snake_out_aaaa) → PRODUCE_SNAKE_IN_AAAA
PRODUCE_SNAKE_IN_AAAA → U9_AAAA(part_of_snake_out_aaaa)
PRODUCE_SNAKE_IN_AAAA → U9_AAAA(U11_aaaa(part_of_snake_in_aaaa))

The TRS R consists of the following rules:

part_of_snake_in_aaaa → part_of_snake_out_aaaa
part_of_snake_in_aaaa → U11_aaaa(part_of_snake_in_aaaa)
U11_aaaa(part_of_snake_out_aaaa) → part_of_snake_out_aaaa

The set Q consists of the following terms:

part_of_snake_in_aaaa
U11_aaaa(x0)

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

(41) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = PRODUCE_SNAKE_IN_AAAA evaluates to t =PRODUCE_SNAKE_IN_AAAA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Semiunifier: [ ]
• Matcher: [ ]

---

Rewriting sequence

PRODUCE_SNAKE_IN_AAAA → U9_AAAA(part_of_snake_out_aaaa)
with rule PRODUCE_SNAKE_IN_AAAA → U9_AAAA(part_of_snake_out_aaaa) at position [] and matcher [ ]

U9_AAAA(part_of_snake_out_aaaa) → PRODUCE_SNAKE_IN_AAAA
with rule U9_AAAA(part_of_snake_out_aaaa) → PRODUCE_SNAKE_IN_AAAA

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.

(42) FALSE

(43) Obligation:

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

INFINITE_SNAKE_IN_GAA(cons(A, R), cons(A, T), S) → INFINITE_SNAKE_IN_GAA(R, T, S)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, nil) → s2l_out_ga(0, nil)
s2l_in_ga(s(X), cons(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), cons(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_gaa(Pattern, Cols, Rows))
snake_in_gaa(Pattern, Cols, Rows) → U5_gaa(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa(nil, S, S) → infinite_snake_out_gaa(nil, S, S)
infinite_snake_in_gaa(cons(A, R), cons(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(cons(A, R), cons(A, T), S)
U5_gaa(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_gaa(Pattern, Cols, Rows, produce_snake_in_aaaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_aaaa(nil, X2, X3, nil) → produce_snake_out_aaaa(nil, X2, X3, nil)
produce_snake_in_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_aaaa(nil, RestSnake, RestSnake, nil) → part_of_snake_out_aaaa(nil, RestSnake, RestSnake, nil)
part_of_snake_in_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_aaaa(R, Rings, RestSnake, RestRings))
U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_aaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings))
U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_aaaa(Rows, Cols, NewInfSnake, Tail))
U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_aaaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail))
U6_gaa(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → U7_gaa(Pattern, Cols, Rows, coil_it_in_ag(Snake, odd))
coil_it_in_ag(nil, X6) → coil_it_out_ag(nil, X6)
coil_it_in_ag(cons(Line, Lines), odd) → U12_ag(Line, Lines, coil_it_in_ag(Lines, even))
coil_it_in_ag(cons(Line, Lines), even) → U13_ag(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, nil, Reversed))
reverse_in_aga(nil, Reversed, Reversed) → reverse_out_aga(nil, Reversed, Reversed)
reverse_in_aga(cons(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
reverse_in_aaa(nil, Reversed, Reversed) → reverse_out_aaa(nil, Reversed, Reversed)
reverse_in_aaa(cons(Head, Tail), SoFar, Reversed) → U16_aaa(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
U16_aaa(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aaa(cons(Head, Tail), SoFar, Reversed)
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aga(cons(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, nil, Reversed)) → reverse2_out_aa(List, Reversed)
U13_ag(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_ag(Line, Lines, coil_it_in_ag(Lines, odd))
U14_ag(Line, Lines, coil_it_out_ag(Lines, odd)) → coil_it_out_ag(cons(Line, Lines), even)
U12_ag(Line, Lines, coil_it_out_ag(Lines, even)) → coil_it_out_ag(cons(Line, Lines), odd)
U7_gaa(Pattern, Cols, Rows, coil_it_out_ag(Snake, odd)) → snake_out_gaa(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_gaa(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x2, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x1)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x1, x4)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x2, x3, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x1, x2, x3, x4)
snake_in_gaa(x1, x2, x3)  =  snake_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
nil  =  nil
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa(x1)
cons(x1, x2)  =  cons(x1, x2)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x1, x2, x5)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x1, x4)
produce_snake_in_aaaa(x1, x2, x3, x4)  =  produce_snake_in_aaaa
produce_snake_out_aaaa(x1, x2, x3, x4)  =  produce_snake_out_aaaa
U9_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_aaaa(x7)
part_of_snake_in_aaaa(x1, x2, x3, x4)  =  part_of_snake_in_aaaa
part_of_snake_out_aaaa(x1, x2, x3, x4)  =  part_of_snake_out_aaaa
U11_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_aaaa(x7)
U10_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_aaaa(x7)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x1, x4)
coil_it_in_ag(x1, x2)  =  coil_it_in_ag(x2)
coil_it_out_ag(x1, x2)  =  coil_it_out_ag(x2)
odd  =  odd
U12_ag(x1, x2, x3)  =  U12_ag(x3)
even  =  even
U13_ag(x1, x2, x3)  =  U13_ag(x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x2)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x3, x5)
reverse_in_aaa(x1, x2, x3)  =  reverse_in_aaa
reverse_out_aaa(x1, x2, x3)  =  reverse_out_aaa
U16_aaa(x1, x2, x3, x4, x5)  =  U16_aaa(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa
U14_ag(x1, x2, x3)  =  U14_ag(x3)
snake_out_gaa(x1, x2, x3)  =  snake_out_gaa(x1)
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg(x1, x2, x3)
INFINITE_SNAKE_IN_GAA(x1, x2, x3)  =  INFINITE_SNAKE_IN_GAA(x1)

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

(44) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(45) Obligation:

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

INFINITE_SNAKE_IN_GAA(cons(A, R), cons(A, T), S) → INFINITE_SNAKE_IN_GAA(R, T, S)

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

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

(46) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(47) Obligation:

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

INFINITE_SNAKE_IN_GAA(cons(A, R)) → INFINITE_SNAKE_IN_GAA(R)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(48) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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_IN_GAA(cons(A, R)) → INFINITE_SNAKE_IN_GAA(R)
  The graph contains the following edges 1 > 1

(49) TRUE

(50) Obligation:

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

S2L_IN_GA(s(X), cons(X1, Y)) → S2L_IN_GA(X, Y)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, nil) → s2l_out_ga(0, nil)
s2l_in_ga(s(X), cons(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), cons(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_gaa(Pattern, Cols, Rows))
snake_in_gaa(Pattern, Cols, Rows) → U5_gaa(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa(nil, S, S) → infinite_snake_out_gaa(nil, S, S)
infinite_snake_in_gaa(cons(A, R), cons(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(cons(A, R), cons(A, T), S)
U5_gaa(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_gaa(Pattern, Cols, Rows, produce_snake_in_aaaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_aaaa(nil, X2, X3, nil) → produce_snake_out_aaaa(nil, X2, X3, nil)
produce_snake_in_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_aaaa(nil, RestSnake, RestSnake, nil) → part_of_snake_out_aaaa(nil, RestSnake, RestSnake, nil)
part_of_snake_in_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_aaaa(R, Rings, RestSnake, RestRings))
U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_aaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings))
U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_aaaa(Rows, Cols, NewInfSnake, Tail))
U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_aaaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail))
U6_gaa(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → U7_gaa(Pattern, Cols, Rows, coil_it_in_ag(Snake, odd))
coil_it_in_ag(nil, X6) → coil_it_out_ag(nil, X6)
coil_it_in_ag(cons(Line, Lines), odd) → U12_ag(Line, Lines, coil_it_in_ag(Lines, even))
coil_it_in_ag(cons(Line, Lines), even) → U13_ag(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, nil, Reversed))
reverse_in_aga(nil, Reversed, Reversed) → reverse_out_aga(nil, Reversed, Reversed)
reverse_in_aga(cons(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
reverse_in_aaa(nil, Reversed, Reversed) → reverse_out_aaa(nil, Reversed, Reversed)
reverse_in_aaa(cons(Head, Tail), SoFar, Reversed) → U16_aaa(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
U16_aaa(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aaa(cons(Head, Tail), SoFar, Reversed)
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aga(cons(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, nil, Reversed)) → reverse2_out_aa(List, Reversed)
U13_ag(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_ag(Line, Lines, coil_it_in_ag(Lines, odd))
U14_ag(Line, Lines, coil_it_out_ag(Lines, odd)) → coil_it_out_ag(cons(Line, Lines), even)
U12_ag(Line, Lines, coil_it_out_ag(Lines, even)) → coil_it_out_ag(cons(Line, Lines), odd)
U7_gaa(Pattern, Cols, Rows, coil_it_out_ag(Snake, odd)) → snake_out_gaa(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_gaa(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x2, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga(x1)
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x1, x4)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x2, x3, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x1, x2, x3, x4)
snake_in_gaa(x1, x2, x3)  =  snake_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
nil  =  nil
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa(x1)
cons(x1, x2)  =  cons(x1, x2)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x1, x2, x5)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x1, x4)
produce_snake_in_aaaa(x1, x2, x3, x4)  =  produce_snake_in_aaaa
produce_snake_out_aaaa(x1, x2, x3, x4)  =  produce_snake_out_aaaa
U9_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_aaaa(x7)
part_of_snake_in_aaaa(x1, x2, x3, x4)  =  part_of_snake_in_aaaa
part_of_snake_out_aaaa(x1, x2, x3, x4)  =  part_of_snake_out_aaaa
U11_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_aaaa(x7)
U10_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_aaaa(x7)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x1, x4)
coil_it_in_ag(x1, x2)  =  coil_it_in_ag(x2)
coil_it_out_ag(x1, x2)  =  coil_it_out_ag(x2)
odd  =  odd
U12_ag(x1, x2, x3)  =  U12_ag(x3)
even  =  even
U13_ag(x1, x2, x3)  =  U13_ag(x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga(x2)
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x3, x5)
reverse_in_aaa(x1, x2, x3)  =  reverse_in_aaa
reverse_out_aaa(x1, x2, x3)  =  reverse_out_aaa
U16_aaa(x1, x2, x3, x4, x5)  =  U16_aaa(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa
U14_ag(x1, x2, x3)  =  U14_ag(x3)
snake_out_gaa(x1, x2, x3)  =  snake_out_gaa(x1)
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg(x1, x2, x3)
S2L_IN_GA(x1, x2)  =  S2L_IN_GA(x1)

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

(51) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(52) Obligation:

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

S2L_IN_GA(s(X), cons(X1, Y)) → S2L_IN_GA(X, Y)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
cons(x1, x2)  =  cons(x1, x2)
S2L_IN_GA(x1, x2)  =  S2L_IN_GA(x1)

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

(53) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(54) Obligation:

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

S2L_IN_GA(s(X)) → S2L_IN_GA(X)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(55) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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_IN_GA(s(X)) → S2L_IN_GA(X)
  The graph contains the following edges 1 > 1

(56) TRUE

(57) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
test_snake_in: (b,b,b)
s2l_in: (b,f)
snake_in: (b,f,f)
infinite_snake_in: (b,f,f)
produce_snake_in: (f,f,f,f)
part_of_snake_in: (f,f,f,f)
coil_it_in: (f,b)
reverse2_in: (f,f)
reverse_in: (f,b,f) (f,f,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, nil) → s2l_out_ga(0, nil)
s2l_in_ga(s(X), cons(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), cons(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_gaa(Pattern, Cols, Rows))
snake_in_gaa(Pattern, Cols, Rows) → U5_gaa(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa(nil, S, S) → infinite_snake_out_gaa(nil, S, S)
infinite_snake_in_gaa(cons(A, R), cons(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(cons(A, R), cons(A, T), S)
U5_gaa(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_gaa(Pattern, Cols, Rows, produce_snake_in_aaaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_aaaa(nil, X2, X3, nil) → produce_snake_out_aaaa(nil, X2, X3, nil)
produce_snake_in_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_aaaa(nil, RestSnake, RestSnake, nil) → part_of_snake_out_aaaa(nil, RestSnake, RestSnake, nil)
part_of_snake_in_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_aaaa(R, Rings, RestSnake, RestRings))
U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_aaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings))
U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_aaaa(Rows, Cols, NewInfSnake, Tail))
U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_aaaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail))
U6_gaa(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → U7_gaa(Pattern, Cols, Rows, coil_it_in_ag(Snake, odd))
coil_it_in_ag(nil, X6) → coil_it_out_ag(nil, X6)
coil_it_in_ag(cons(Line, Lines), odd) → U12_ag(Line, Lines, coil_it_in_ag(Lines, even))
coil_it_in_ag(cons(Line, Lines), even) → U13_ag(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, nil, Reversed))
reverse_in_aga(nil, Reversed, Reversed) → reverse_out_aga(nil, Reversed, Reversed)
reverse_in_aga(cons(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
reverse_in_aaa(nil, Reversed, Reversed) → reverse_out_aaa(nil, Reversed, Reversed)
reverse_in_aaa(cons(Head, Tail), SoFar, Reversed) → U16_aaa(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
U16_aaa(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aaa(cons(Head, Tail), SoFar, Reversed)
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aga(cons(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, nil, Reversed)) → reverse2_out_aa(List, Reversed)
U13_ag(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_ag(Line, Lines, coil_it_in_ag(Lines, odd))
U14_ag(Line, Lines, coil_it_out_ag(Lines, odd)) → coil_it_out_ag(cons(Line, Lines), even)
U12_ag(Line, Lines, coil_it_out_ag(Lines, even)) → coil_it_out_ag(cons(Line, Lines), odd)
U7_gaa(Pattern, Cols, Rows, coil_it_out_ag(Snake, odd)) → snake_out_gaa(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_gaa(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x4)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x4)
snake_in_gaa(x1, x2, x3)  =  snake_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
nil  =  nil
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa
cons(x1, x2)  =  cons(x1, x2)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x4)
produce_snake_in_aaaa(x1, x2, x3, x4)  =  produce_snake_in_aaaa
produce_snake_out_aaaa(x1, x2, x3, x4)  =  produce_snake_out_aaaa
U9_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_aaaa(x7)
part_of_snake_in_aaaa(x1, x2, x3, x4)  =  part_of_snake_in_aaaa
part_of_snake_out_aaaa(x1, x2, x3, x4)  =  part_of_snake_out_aaaa
U11_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_aaaa(x7)
U10_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_aaaa(x7)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x4)
coil_it_in_ag(x1, x2)  =  coil_it_in_ag(x2)
coil_it_out_ag(x1, x2)  =  coil_it_out_ag
odd  =  odd
U12_ag(x1, x2, x3)  =  U12_ag(x3)
even  =  even
U13_ag(x1, x2, x3)  =  U13_ag(x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x5)
reverse_in_aaa(x1, x2, x3)  =  reverse_in_aaa
reverse_out_aaa(x1, x2, x3)  =  reverse_out_aaa
U16_aaa(x1, x2, x3, x4, x5)  =  U16_aaa(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa
U14_ag(x1, x2, x3)  =  U14_ag(x3)
snake_out_gaa(x1, x2, x3)  =  snake_out_gaa
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(58) Obligation:

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

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, nil) → s2l_out_ga(0, nil)
s2l_in_ga(s(X), cons(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), cons(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_gaa(Pattern, Cols, Rows))
snake_in_gaa(Pattern, Cols, Rows) → U5_gaa(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa(nil, S, S) → infinite_snake_out_gaa(nil, S, S)
infinite_snake_in_gaa(cons(A, R), cons(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(cons(A, R), cons(A, T), S)
U5_gaa(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_gaa(Pattern, Cols, Rows, produce_snake_in_aaaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_aaaa(nil, X2, X3, nil) → produce_snake_out_aaaa(nil, X2, X3, nil)
produce_snake_in_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_aaaa(nil, RestSnake, RestSnake, nil) → part_of_snake_out_aaaa(nil, RestSnake, RestSnake, nil)
part_of_snake_in_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_aaaa(R, Rings, RestSnake, RestRings))
U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_aaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings))
U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_aaaa(Rows, Cols, NewInfSnake, Tail))
U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_aaaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail))
U6_gaa(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → U7_gaa(Pattern, Cols, Rows, coil_it_in_ag(Snake, odd))
coil_it_in_ag(nil, X6) → coil_it_out_ag(nil, X6)
coil_it_in_ag(cons(Line, Lines), odd) → U12_ag(Line, Lines, coil_it_in_ag(Lines, even))
coil_it_in_ag(cons(Line, Lines), even) → U13_ag(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, nil, Reversed))
reverse_in_aga(nil, Reversed, Reversed) → reverse_out_aga(nil, Reversed, Reversed)
reverse_in_aga(cons(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
reverse_in_aaa(nil, Reversed, Reversed) → reverse_out_aaa(nil, Reversed, Reversed)
reverse_in_aaa(cons(Head, Tail), SoFar, Reversed) → U16_aaa(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
U16_aaa(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aaa(cons(Head, Tail), SoFar, Reversed)
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aga(cons(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, nil, Reversed)) → reverse2_out_aa(List, Reversed)
U13_ag(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_ag(Line, Lines, coil_it_in_ag(Lines, odd))
U14_ag(Line, Lines, coil_it_out_ag(Lines, odd)) → coil_it_out_ag(cons(Line, Lines), even)
U12_ag(Line, Lines, coil_it_out_ag(Lines, even)) → coil_it_out_ag(cons(Line, Lines), odd)
U7_gaa(Pattern, Cols, Rows, coil_it_out_ag(Snake, odd)) → snake_out_gaa(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_gaa(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x4)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x4)
snake_in_gaa(x1, x2, x3)  =  snake_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
nil  =  nil
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa
cons(x1, x2)  =  cons(x1, x2)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x4)
produce_snake_in_aaaa(x1, x2, x3, x4)  =  produce_snake_in_aaaa
produce_snake_out_aaaa(x1, x2, x3, x4)  =  produce_snake_out_aaaa
U9_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_aaaa(x7)
part_of_snake_in_aaaa(x1, x2, x3, x4)  =  part_of_snake_in_aaaa
part_of_snake_out_aaaa(x1, x2, x3, x4)  =  part_of_snake_out_aaaa
U11_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_aaaa(x7)
U10_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_aaaa(x7)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x4)
coil_it_in_ag(x1, x2)  =  coil_it_in_ag(x2)
coil_it_out_ag(x1, x2)  =  coil_it_out_ag
odd  =  odd
U12_ag(x1, x2, x3)  =  U12_ag(x3)
even  =  even
U13_ag(x1, x2, x3)  =  U13_ag(x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x5)
reverse_in_aaa(x1, x2, x3)  =  reverse_in_aaa
reverse_out_aaa(x1, x2, x3)  =  reverse_out_aaa
U16_aaa(x1, x2, x3, x4, x5)  =  U16_aaa(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa
U14_ag(x1, x2, x3)  =  U14_ag(x3)
snake_out_gaa(x1, x2, x3)  =  snake_out_gaa
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg

(59) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

TEST_SNAKE_IN_GGG(Pattern, C, R) → U1_GGG(Pattern, C, R, s2l_in_ga(C, Cols))
TEST_SNAKE_IN_GGG(Pattern, C, R) → S2L_IN_GA(C, Cols)
S2L_IN_GA(s(X), cons(X1, Y)) → U4_GA(X, X1, Y, s2l_in_ga(X, Y))
S2L_IN_GA(s(X), cons(X1, Y)) → S2L_IN_GA(X, Y)
U1_GGG(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_GGG(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U1_GGG(Pattern, C, R, s2l_out_ga(C, Cols)) → S2L_IN_GA(R, Rows)
U2_GGG(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_GGG(Pattern, C, R, snake_in_gaa(Pattern, Cols, Rows))
U2_GGG(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → SNAKE_IN_GAA(Pattern, Cols, Rows)
SNAKE_IN_GAA(Pattern, Cols, Rows) → U5_GAA(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
SNAKE_IN_GAA(Pattern, Cols, Rows) → INFINITE_SNAKE_IN_GAA(Pattern, InfSnake, InfSnake)
INFINITE_SNAKE_IN_GAA(cons(A, R), cons(A, T), S) → U8_GAA(A, R, T, S, infinite_snake_in_gaa(R, T, S))
INFINITE_SNAKE_IN_GAA(cons(A, R), cons(A, T), S) → INFINITE_SNAKE_IN_GAA(R, T, S)
U5_GAA(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_GAA(Pattern, Cols, Rows, produce_snake_in_aaaa(Rows, Cols, InfSnake, Snake))
U5_GAA(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → PRODUCE_SNAKE_IN_AAAA(Rows, Cols, InfSnake, Snake)
PRODUCE_SNAKE_IN_AAAA(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_AAAA(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))
PRODUCE_SNAKE_IN_AAAA(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → PART_OF_SNAKE_IN_AAAA(Cols, InfSnake, NewInfSnake, Part)
PART_OF_SNAKE_IN_AAAA(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → U11_AAAA(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_aaaa(R, Rings, RestSnake, RestRings))
PART_OF_SNAKE_IN_AAAA(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → PART_OF_SNAKE_IN_AAAA(R, Rings, RestSnake, RestRings)
U9_AAAA(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_AAAA(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_aaaa(Rows, Cols, NewInfSnake, Tail))
U9_AAAA(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → PRODUCE_SNAKE_IN_AAAA(Rows, Cols, NewInfSnake, Tail)
U6_GAA(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → U7_GAA(Pattern, Cols, Rows, coil_it_in_ag(Snake, odd))
U6_GAA(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → COIL_IT_IN_AG(Snake, odd)
COIL_IT_IN_AG(cons(Line, Lines), odd) → U12_AG(Line, Lines, coil_it_in_ag(Lines, even))
COIL_IT_IN_AG(cons(Line, Lines), odd) → COIL_IT_IN_AG(Lines, even)
COIL_IT_IN_AG(cons(Line, Lines), even) → U13_AG(Line, Lines, reverse2_in_aa(Line, Line1))
COIL_IT_IN_AG(cons(Line, Lines), even) → REVERSE2_IN_AA(Line, Line1)
REVERSE2_IN_AA(List, Reversed) → U15_AA(List, Reversed, reverse_in_aga(List, nil, Reversed))
REVERSE2_IN_AA(List, Reversed) → REVERSE_IN_AGA(List, nil, Reversed)
REVERSE_IN_AGA(cons(Head, Tail), SoFar, Reversed) → U16_AGA(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
REVERSE_IN_AGA(cons(Head, Tail), SoFar, Reversed) → REVERSE_IN_AAA(Tail, cons(Head, SoFar), Reversed)
REVERSE_IN_AAA(cons(Head, Tail), SoFar, Reversed) → U16_AAA(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
REVERSE_IN_AAA(cons(Head, Tail), SoFar, Reversed) → REVERSE_IN_AAA(Tail, cons(Head, SoFar), Reversed)
U13_AG(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_AG(Line, Lines, coil_it_in_ag(Lines, odd))
U13_AG(Line, Lines, reverse2_out_aa(Line, Line1)) → COIL_IT_IN_AG(Lines, odd)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, nil) → s2l_out_ga(0, nil)
s2l_in_ga(s(X), cons(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), cons(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_gaa(Pattern, Cols, Rows))
snake_in_gaa(Pattern, Cols, Rows) → U5_gaa(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa(nil, S, S) → infinite_snake_out_gaa(nil, S, S)
infinite_snake_in_gaa(cons(A, R), cons(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(cons(A, R), cons(A, T), S)
U5_gaa(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_gaa(Pattern, Cols, Rows, produce_snake_in_aaaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_aaaa(nil, X2, X3, nil) → produce_snake_out_aaaa(nil, X2, X3, nil)
produce_snake_in_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_aaaa(nil, RestSnake, RestSnake, nil) → part_of_snake_out_aaaa(nil, RestSnake, RestSnake, nil)
part_of_snake_in_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_aaaa(R, Rings, RestSnake, RestRings))
U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_aaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings))
U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_aaaa(Rows, Cols, NewInfSnake, Tail))
U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_aaaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail))
U6_gaa(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → U7_gaa(Pattern, Cols, Rows, coil_it_in_ag(Snake, odd))
coil_it_in_ag(nil, X6) → coil_it_out_ag(nil, X6)
coil_it_in_ag(cons(Line, Lines), odd) → U12_ag(Line, Lines, coil_it_in_ag(Lines, even))
coil_it_in_ag(cons(Line, Lines), even) → U13_ag(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, nil, Reversed))
reverse_in_aga(nil, Reversed, Reversed) → reverse_out_aga(nil, Reversed, Reversed)
reverse_in_aga(cons(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
reverse_in_aaa(nil, Reversed, Reversed) → reverse_out_aaa(nil, Reversed, Reversed)
reverse_in_aaa(cons(Head, Tail), SoFar, Reversed) → U16_aaa(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
U16_aaa(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aaa(cons(Head, Tail), SoFar, Reversed)
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aga(cons(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, nil, Reversed)) → reverse2_out_aa(List, Reversed)
U13_ag(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_ag(Line, Lines, coil_it_in_ag(Lines, odd))
U14_ag(Line, Lines, coil_it_out_ag(Lines, odd)) → coil_it_out_ag(cons(Line, Lines), even)
U12_ag(Line, Lines, coil_it_out_ag(Lines, even)) → coil_it_out_ag(cons(Line, Lines), odd)
U7_gaa(Pattern, Cols, Rows, coil_it_out_ag(Snake, odd)) → snake_out_gaa(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_gaa(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x4)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x4)
snake_in_gaa(x1, x2, x3)  =  snake_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
nil  =  nil
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa
cons(x1, x2)  =  cons(x1, x2)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x4)
produce_snake_in_aaaa(x1, x2, x3, x4)  =  produce_snake_in_aaaa
produce_snake_out_aaaa(x1, x2, x3, x4)  =  produce_snake_out_aaaa
U9_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_aaaa(x7)
part_of_snake_in_aaaa(x1, x2, x3, x4)  =  part_of_snake_in_aaaa
part_of_snake_out_aaaa(x1, x2, x3, x4)  =  part_of_snake_out_aaaa
U11_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_aaaa(x7)
U10_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_aaaa(x7)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x4)
coil_it_in_ag(x1, x2)  =  coil_it_in_ag(x2)
coil_it_out_ag(x1, x2)  =  coil_it_out_ag
odd  =  odd
U12_ag(x1, x2, x3)  =  U12_ag(x3)
even  =  even
U13_ag(x1, x2, x3)  =  U13_ag(x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x5)
reverse_in_aaa(x1, x2, x3)  =  reverse_in_aaa
reverse_out_aaa(x1, x2, x3)  =  reverse_out_aaa
U16_aaa(x1, x2, x3, x4, x5)  =  U16_aaa(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa
U14_ag(x1, x2, x3)  =  U14_ag(x3)
snake_out_gaa(x1, x2, x3)  =  snake_out_gaa
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg
TEST_SNAKE_IN_GGG(x1, x2, x3)  =  TEST_SNAKE_IN_GGG(x1, x2, x3)
U1_GGG(x1, x2, x3, x4)  =  U1_GGG(x1, x3, x4)
S2L_IN_GA(x1, x2)  =  S2L_IN_GA(x1)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x4)
U2_GGG(x1, x2, x3, x4, x5)  =  U2_GGG(x1, x5)
U3_GGG(x1, x2, x3, x4)  =  U3_GGG(x4)
SNAKE_IN_GAA(x1, x2, x3)  =  SNAKE_IN_GAA(x1)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x4)
INFINITE_SNAKE_IN_GAA(x1, x2, x3)  =  INFINITE_SNAKE_IN_GAA(x1)
U8_GAA(x1, x2, x3, x4, x5)  =  U8_GAA(x5)
U6_GAA(x1, x2, x3, x4)  =  U6_GAA(x4)
PRODUCE_SNAKE_IN_AAAA(x1, x2, x3, x4)  =  PRODUCE_SNAKE_IN_AAAA
U9_AAAA(x1, x2, x3, x4, x5, x6, x7)  =  U9_AAAA(x7)
PART_OF_SNAKE_IN_AAAA(x1, x2, x3, x4)  =  PART_OF_SNAKE_IN_AAAA
U11_AAAA(x1, x2, x3, x4, x5, x6, x7)  =  U11_AAAA(x7)
U10_AAAA(x1, x2, x3, x4, x5, x6, x7)  =  U10_AAAA(x7)
U7_GAA(x1, x2, x3, x4)  =  U7_GAA(x4)
COIL_IT_IN_AG(x1, x2)  =  COIL_IT_IN_AG(x2)
U12_AG(x1, x2, x3)  =  U12_AG(x3)
U13_AG(x1, x2, x3)  =  U13_AG(x3)
REVERSE2_IN_AA(x1, x2)  =  REVERSE2_IN_AA
U15_AA(x1, x2, x3)  =  U15_AA(x3)
REVERSE_IN_AGA(x1, x2, x3)  =  REVERSE_IN_AGA(x2)
U16_AGA(x1, x2, x3, x4, x5)  =  U16_AGA(x5)
REVERSE_IN_AAA(x1, x2, x3)  =  REVERSE_IN_AAA
U16_AAA(x1, x2, x3, x4, x5)  =  U16_AAA(x5)
U14_AG(x1, x2, x3)  =  U14_AG(x3)

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

(60) Obligation:

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

TEST_SNAKE_IN_GGG(Pattern, C, R) → U1_GGG(Pattern, C, R, s2l_in_ga(C, Cols))
TEST_SNAKE_IN_GGG(Pattern, C, R) → S2L_IN_GA(C, Cols)
S2L_IN_GA(s(X), cons(X1, Y)) → U4_GA(X, X1, Y, s2l_in_ga(X, Y))
S2L_IN_GA(s(X), cons(X1, Y)) → S2L_IN_GA(X, Y)
U1_GGG(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_GGG(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U1_GGG(Pattern, C, R, s2l_out_ga(C, Cols)) → S2L_IN_GA(R, Rows)
U2_GGG(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_GGG(Pattern, C, R, snake_in_gaa(Pattern, Cols, Rows))
U2_GGG(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → SNAKE_IN_GAA(Pattern, Cols, Rows)
SNAKE_IN_GAA(Pattern, Cols, Rows) → U5_GAA(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
SNAKE_IN_GAA(Pattern, Cols, Rows) → INFINITE_SNAKE_IN_GAA(Pattern, InfSnake, InfSnake)
INFINITE_SNAKE_IN_GAA(cons(A, R), cons(A, T), S) → U8_GAA(A, R, T, S, infinite_snake_in_gaa(R, T, S))
INFINITE_SNAKE_IN_GAA(cons(A, R), cons(A, T), S) → INFINITE_SNAKE_IN_GAA(R, T, S)
U5_GAA(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_GAA(Pattern, Cols, Rows, produce_snake_in_aaaa(Rows, Cols, InfSnake, Snake))
U5_GAA(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → PRODUCE_SNAKE_IN_AAAA(Rows, Cols, InfSnake, Snake)
PRODUCE_SNAKE_IN_AAAA(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_AAAA(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))
PRODUCE_SNAKE_IN_AAAA(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → PART_OF_SNAKE_IN_AAAA(Cols, InfSnake, NewInfSnake, Part)
PART_OF_SNAKE_IN_AAAA(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → U11_AAAA(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_aaaa(R, Rings, RestSnake, RestRings))
PART_OF_SNAKE_IN_AAAA(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → PART_OF_SNAKE_IN_AAAA(R, Rings, RestSnake, RestRings)
U9_AAAA(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_AAAA(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_aaaa(Rows, Cols, NewInfSnake, Tail))
U9_AAAA(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → PRODUCE_SNAKE_IN_AAAA(Rows, Cols, NewInfSnake, Tail)
U6_GAA(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → U7_GAA(Pattern, Cols, Rows, coil_it_in_ag(Snake, odd))
U6_GAA(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → COIL_IT_IN_AG(Snake, odd)
COIL_IT_IN_AG(cons(Line, Lines), odd) → U12_AG(Line, Lines, coil_it_in_ag(Lines, even))
COIL_IT_IN_AG(cons(Line, Lines), odd) → COIL_IT_IN_AG(Lines, even)
COIL_IT_IN_AG(cons(Line, Lines), even) → U13_AG(Line, Lines, reverse2_in_aa(Line, Line1))
COIL_IT_IN_AG(cons(Line, Lines), even) → REVERSE2_IN_AA(Line, Line1)
REVERSE2_IN_AA(List, Reversed) → U15_AA(List, Reversed, reverse_in_aga(List, nil, Reversed))
REVERSE2_IN_AA(List, Reversed) → REVERSE_IN_AGA(List, nil, Reversed)
REVERSE_IN_AGA(cons(Head, Tail), SoFar, Reversed) → U16_AGA(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
REVERSE_IN_AGA(cons(Head, Tail), SoFar, Reversed) → REVERSE_IN_AAA(Tail, cons(Head, SoFar), Reversed)
REVERSE_IN_AAA(cons(Head, Tail), SoFar, Reversed) → U16_AAA(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
REVERSE_IN_AAA(cons(Head, Tail), SoFar, Reversed) → REVERSE_IN_AAA(Tail, cons(Head, SoFar), Reversed)
U13_AG(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_AG(Line, Lines, coil_it_in_ag(Lines, odd))
U13_AG(Line, Lines, reverse2_out_aa(Line, Line1)) → COIL_IT_IN_AG(Lines, odd)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, nil) → s2l_out_ga(0, nil)
s2l_in_ga(s(X), cons(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), cons(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_gaa(Pattern, Cols, Rows))
snake_in_gaa(Pattern, Cols, Rows) → U5_gaa(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa(nil, S, S) → infinite_snake_out_gaa(nil, S, S)
infinite_snake_in_gaa(cons(A, R), cons(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(cons(A, R), cons(A, T), S)
U5_gaa(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_gaa(Pattern, Cols, Rows, produce_snake_in_aaaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_aaaa(nil, X2, X3, nil) → produce_snake_out_aaaa(nil, X2, X3, nil)
produce_snake_in_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_aaaa(nil, RestSnake, RestSnake, nil) → part_of_snake_out_aaaa(nil, RestSnake, RestSnake, nil)
part_of_snake_in_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_aaaa(R, Rings, RestSnake, RestRings))
U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_aaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings))
U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_aaaa(Rows, Cols, NewInfSnake, Tail))
U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_aaaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail))
U6_gaa(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → U7_gaa(Pattern, Cols, Rows, coil_it_in_ag(Snake, odd))
coil_it_in_ag(nil, X6) → coil_it_out_ag(nil, X6)
coil_it_in_ag(cons(Line, Lines), odd) → U12_ag(Line, Lines, coil_it_in_ag(Lines, even))
coil_it_in_ag(cons(Line, Lines), even) → U13_ag(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, nil, Reversed))
reverse_in_aga(nil, Reversed, Reversed) → reverse_out_aga(nil, Reversed, Reversed)
reverse_in_aga(cons(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
reverse_in_aaa(nil, Reversed, Reversed) → reverse_out_aaa(nil, Reversed, Reversed)
reverse_in_aaa(cons(Head, Tail), SoFar, Reversed) → U16_aaa(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
U16_aaa(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aaa(cons(Head, Tail), SoFar, Reversed)
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aga(cons(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, nil, Reversed)) → reverse2_out_aa(List, Reversed)
U13_ag(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_ag(Line, Lines, coil_it_in_ag(Lines, odd))
U14_ag(Line, Lines, coil_it_out_ag(Lines, odd)) → coil_it_out_ag(cons(Line, Lines), even)
U12_ag(Line, Lines, coil_it_out_ag(Lines, even)) → coil_it_out_ag(cons(Line, Lines), odd)
U7_gaa(Pattern, Cols, Rows, coil_it_out_ag(Snake, odd)) → snake_out_gaa(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_gaa(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x4)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x4)
snake_in_gaa(x1, x2, x3)  =  snake_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
nil  =  nil
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa
cons(x1, x2)  =  cons(x1, x2)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x4)
produce_snake_in_aaaa(x1, x2, x3, x4)  =  produce_snake_in_aaaa
produce_snake_out_aaaa(x1, x2, x3, x4)  =  produce_snake_out_aaaa
U9_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_aaaa(x7)
part_of_snake_in_aaaa(x1, x2, x3, x4)  =  part_of_snake_in_aaaa
part_of_snake_out_aaaa(x1, x2, x3, x4)  =  part_of_snake_out_aaaa
U11_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_aaaa(x7)
U10_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_aaaa(x7)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x4)
coil_it_in_ag(x1, x2)  =  coil_it_in_ag(x2)
coil_it_out_ag(x1, x2)  =  coil_it_out_ag
odd  =  odd
U12_ag(x1, x2, x3)  =  U12_ag(x3)
even  =  even
U13_ag(x1, x2, x3)  =  U13_ag(x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x5)
reverse_in_aaa(x1, x2, x3)  =  reverse_in_aaa
reverse_out_aaa(x1, x2, x3)  =  reverse_out_aaa
U16_aaa(x1, x2, x3, x4, x5)  =  U16_aaa(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa
U14_ag(x1, x2, x3)  =  U14_ag(x3)
snake_out_gaa(x1, x2, x3)  =  snake_out_gaa
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg
TEST_SNAKE_IN_GGG(x1, x2, x3)  =  TEST_SNAKE_IN_GGG(x1, x2, x3)
U1_GGG(x1, x2, x3, x4)  =  U1_GGG(x1, x3, x4)
S2L_IN_GA(x1, x2)  =  S2L_IN_GA(x1)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x4)
U2_GGG(x1, x2, x3, x4, x5)  =  U2_GGG(x1, x5)
U3_GGG(x1, x2, x3, x4)  =  U3_GGG(x4)
SNAKE_IN_GAA(x1, x2, x3)  =  SNAKE_IN_GAA(x1)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x4)
INFINITE_SNAKE_IN_GAA(x1, x2, x3)  =  INFINITE_SNAKE_IN_GAA(x1)
U8_GAA(x1, x2, x3, x4, x5)  =  U8_GAA(x5)
U6_GAA(x1, x2, x3, x4)  =  U6_GAA(x4)
PRODUCE_SNAKE_IN_AAAA(x1, x2, x3, x4)  =  PRODUCE_SNAKE_IN_AAAA
U9_AAAA(x1, x2, x3, x4, x5, x6, x7)  =  U9_AAAA(x7)
PART_OF_SNAKE_IN_AAAA(x1, x2, x3, x4)  =  PART_OF_SNAKE_IN_AAAA
U11_AAAA(x1, x2, x3, x4, x5, x6, x7)  =  U11_AAAA(x7)
U10_AAAA(x1, x2, x3, x4, x5, x6, x7)  =  U10_AAAA(x7)
U7_GAA(x1, x2, x3, x4)  =  U7_GAA(x4)
COIL_IT_IN_AG(x1, x2)  =  COIL_IT_IN_AG(x2)
U12_AG(x1, x2, x3)  =  U12_AG(x3)
U13_AG(x1, x2, x3)  =  U13_AG(x3)
REVERSE2_IN_AA(x1, x2)  =  REVERSE2_IN_AA
U15_AA(x1, x2, x3)  =  U15_AA(x3)
REVERSE_IN_AGA(x1, x2, x3)  =  REVERSE_IN_AGA(x2)
U16_AGA(x1, x2, x3, x4, x5)  =  U16_AGA(x5)
REVERSE_IN_AAA(x1, x2, x3)  =  REVERSE_IN_AAA
U16_AAA(x1, x2, x3, x4, x5)  =  U16_AAA(x5)
U14_AG(x1, x2, x3)  =  U14_AG(x3)

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

(61) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 6 SCCs with 25 less nodes.

(62) Complex Obligation (AND)

(63) Obligation:

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

REVERSE_IN_AAA(cons(Head, Tail), SoFar, Reversed) → REVERSE_IN_AAA(Tail, cons(Head, SoFar), Reversed)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, nil) → s2l_out_ga(0, nil)
s2l_in_ga(s(X), cons(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), cons(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_gaa(Pattern, Cols, Rows))
snake_in_gaa(Pattern, Cols, Rows) → U5_gaa(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa(nil, S, S) → infinite_snake_out_gaa(nil, S, S)
infinite_snake_in_gaa(cons(A, R), cons(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(cons(A, R), cons(A, T), S)
U5_gaa(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_gaa(Pattern, Cols, Rows, produce_snake_in_aaaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_aaaa(nil, X2, X3, nil) → produce_snake_out_aaaa(nil, X2, X3, nil)
produce_snake_in_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_aaaa(nil, RestSnake, RestSnake, nil) → part_of_snake_out_aaaa(nil, RestSnake, RestSnake, nil)
part_of_snake_in_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_aaaa(R, Rings, RestSnake, RestRings))
U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_aaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings))
U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_aaaa(Rows, Cols, NewInfSnake, Tail))
U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_aaaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail))
U6_gaa(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → U7_gaa(Pattern, Cols, Rows, coil_it_in_ag(Snake, odd))
coil_it_in_ag(nil, X6) → coil_it_out_ag(nil, X6)
coil_it_in_ag(cons(Line, Lines), odd) → U12_ag(Line, Lines, coil_it_in_ag(Lines, even))
coil_it_in_ag(cons(Line, Lines), even) → U13_ag(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, nil, Reversed))
reverse_in_aga(nil, Reversed, Reversed) → reverse_out_aga(nil, Reversed, Reversed)
reverse_in_aga(cons(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
reverse_in_aaa(nil, Reversed, Reversed) → reverse_out_aaa(nil, Reversed, Reversed)
reverse_in_aaa(cons(Head, Tail), SoFar, Reversed) → U16_aaa(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
U16_aaa(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aaa(cons(Head, Tail), SoFar, Reversed)
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aga(cons(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, nil, Reversed)) → reverse2_out_aa(List, Reversed)
U13_ag(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_ag(Line, Lines, coil_it_in_ag(Lines, odd))
U14_ag(Line, Lines, coil_it_out_ag(Lines, odd)) → coil_it_out_ag(cons(Line, Lines), even)
U12_ag(Line, Lines, coil_it_out_ag(Lines, even)) → coil_it_out_ag(cons(Line, Lines), odd)
U7_gaa(Pattern, Cols, Rows, coil_it_out_ag(Snake, odd)) → snake_out_gaa(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_gaa(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x4)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x4)
snake_in_gaa(x1, x2, x3)  =  snake_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
nil  =  nil
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa
cons(x1, x2)  =  cons(x1, x2)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x4)
produce_snake_in_aaaa(x1, x2, x3, x4)  =  produce_snake_in_aaaa
produce_snake_out_aaaa(x1, x2, x3, x4)  =  produce_snake_out_aaaa
U9_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_aaaa(x7)
part_of_snake_in_aaaa(x1, x2, x3, x4)  =  part_of_snake_in_aaaa
part_of_snake_out_aaaa(x1, x2, x3, x4)  =  part_of_snake_out_aaaa
U11_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_aaaa(x7)
U10_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_aaaa(x7)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x4)
coil_it_in_ag(x1, x2)  =  coil_it_in_ag(x2)
coil_it_out_ag(x1, x2)  =  coil_it_out_ag
odd  =  odd
U12_ag(x1, x2, x3)  =  U12_ag(x3)
even  =  even
U13_ag(x1, x2, x3)  =  U13_ag(x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x5)
reverse_in_aaa(x1, x2, x3)  =  reverse_in_aaa
reverse_out_aaa(x1, x2, x3)  =  reverse_out_aaa
U16_aaa(x1, x2, x3, x4, x5)  =  U16_aaa(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa
U14_ag(x1, x2, x3)  =  U14_ag(x3)
snake_out_gaa(x1, x2, x3)  =  snake_out_gaa
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg
REVERSE_IN_AAA(x1, x2, x3)  =  REVERSE_IN_AAA

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

(64) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(65) Obligation:

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

REVERSE_IN_AAA(cons(Head, Tail), SoFar, Reversed) → REVERSE_IN_AAA(Tail, cons(Head, SoFar), Reversed)

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

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

(66) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(67) Obligation:

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

REVERSE_IN_AAA → REVERSE_IN_AAA

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(68) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = REVERSE_IN_AAA evaluates to t =REVERSE_IN_AAA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Semiunifier: [ ]
• Matcher: [ ]

---

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from REVERSE_IN_AAA to REVERSE_IN_AAA.

(69) FALSE

(70) Obligation:

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

COIL_IT_IN_AG(cons(Line, Lines), odd) → COIL_IT_IN_AG(Lines, even)
COIL_IT_IN_AG(cons(Line, Lines), even) → U13_AG(Line, Lines, reverse2_in_aa(Line, Line1))
U13_AG(Line, Lines, reverse2_out_aa(Line, Line1)) → COIL_IT_IN_AG(Lines, odd)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, nil) → s2l_out_ga(0, nil)
s2l_in_ga(s(X), cons(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), cons(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_gaa(Pattern, Cols, Rows))
snake_in_gaa(Pattern, Cols, Rows) → U5_gaa(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa(nil, S, S) → infinite_snake_out_gaa(nil, S, S)
infinite_snake_in_gaa(cons(A, R), cons(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(cons(A, R), cons(A, T), S)
U5_gaa(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_gaa(Pattern, Cols, Rows, produce_snake_in_aaaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_aaaa(nil, X2, X3, nil) → produce_snake_out_aaaa(nil, X2, X3, nil)
produce_snake_in_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_aaaa(nil, RestSnake, RestSnake, nil) → part_of_snake_out_aaaa(nil, RestSnake, RestSnake, nil)
part_of_snake_in_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_aaaa(R, Rings, RestSnake, RestRings))
U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_aaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings))
U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_aaaa(Rows, Cols, NewInfSnake, Tail))
U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_aaaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail))
U6_gaa(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → U7_gaa(Pattern, Cols, Rows, coil_it_in_ag(Snake, odd))
coil_it_in_ag(nil, X6) → coil_it_out_ag(nil, X6)
coil_it_in_ag(cons(Line, Lines), odd) → U12_ag(Line, Lines, coil_it_in_ag(Lines, even))
coil_it_in_ag(cons(Line, Lines), even) → U13_ag(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, nil, Reversed))
reverse_in_aga(nil, Reversed, Reversed) → reverse_out_aga(nil, Reversed, Reversed)
reverse_in_aga(cons(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
reverse_in_aaa(nil, Reversed, Reversed) → reverse_out_aaa(nil, Reversed, Reversed)
reverse_in_aaa(cons(Head, Tail), SoFar, Reversed) → U16_aaa(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
U16_aaa(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aaa(cons(Head, Tail), SoFar, Reversed)
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aga(cons(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, nil, Reversed)) → reverse2_out_aa(List, Reversed)
U13_ag(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_ag(Line, Lines, coil_it_in_ag(Lines, odd))
U14_ag(Line, Lines, coil_it_out_ag(Lines, odd)) → coil_it_out_ag(cons(Line, Lines), even)
U12_ag(Line, Lines, coil_it_out_ag(Lines, even)) → coil_it_out_ag(cons(Line, Lines), odd)
U7_gaa(Pattern, Cols, Rows, coil_it_out_ag(Snake, odd)) → snake_out_gaa(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_gaa(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x4)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x4)
snake_in_gaa(x1, x2, x3)  =  snake_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
nil  =  nil
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa
cons(x1, x2)  =  cons(x1, x2)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x4)
produce_snake_in_aaaa(x1, x2, x3, x4)  =  produce_snake_in_aaaa
produce_snake_out_aaaa(x1, x2, x3, x4)  =  produce_snake_out_aaaa
U9_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_aaaa(x7)
part_of_snake_in_aaaa(x1, x2, x3, x4)  =  part_of_snake_in_aaaa
part_of_snake_out_aaaa(x1, x2, x3, x4)  =  part_of_snake_out_aaaa
U11_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_aaaa(x7)
U10_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_aaaa(x7)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x4)
coil_it_in_ag(x1, x2)  =  coil_it_in_ag(x2)
coil_it_out_ag(x1, x2)  =  coil_it_out_ag
odd  =  odd
U12_ag(x1, x2, x3)  =  U12_ag(x3)
even  =  even
U13_ag(x1, x2, x3)  =  U13_ag(x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x5)
reverse_in_aaa(x1, x2, x3)  =  reverse_in_aaa
reverse_out_aaa(x1, x2, x3)  =  reverse_out_aaa
U16_aaa(x1, x2, x3, x4, x5)  =  U16_aaa(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa
U14_ag(x1, x2, x3)  =  U14_ag(x3)
snake_out_gaa(x1, x2, x3)  =  snake_out_gaa
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg
COIL_IT_IN_AG(x1, x2)  =  COIL_IT_IN_AG(x2)
U13_AG(x1, x2, x3)  =  U13_AG(x3)

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

(71) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(72) Obligation:

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

COIL_IT_IN_AG(cons(Line, Lines), odd) → COIL_IT_IN_AG(Lines, even)
COIL_IT_IN_AG(cons(Line, Lines), even) → U13_AG(Line, Lines, reverse2_in_aa(Line, Line1))
U13_AG(Line, Lines, reverse2_out_aa(Line, Line1)) → COIL_IT_IN_AG(Lines, odd)

The TRS R consists of the following rules:

reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, nil, Reversed))
U15_aa(List, Reversed, reverse_out_aga(List, nil, Reversed)) → reverse2_out_aa(List, Reversed)
reverse_in_aga(nil, Reversed, Reversed) → reverse_out_aga(nil, Reversed, Reversed)
reverse_in_aga(cons(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aga(cons(Head, Tail), SoFar, Reversed)
reverse_in_aaa(nil, Reversed, Reversed) → reverse_out_aaa(nil, Reversed, Reversed)
reverse_in_aaa(cons(Head, Tail), SoFar, Reversed) → U16_aaa(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
U16_aaa(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aaa(cons(Head, Tail), SoFar, Reversed)

The argument filtering Pi contains the following mapping:
nil  =  nil
cons(x1, x2)  =  cons(x1, x2)
odd  =  odd
even  =  even
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x5)
reverse_in_aaa(x1, x2, x3)  =  reverse_in_aaa
reverse_out_aaa(x1, x2, x3)  =  reverse_out_aaa
U16_aaa(x1, x2, x3, x4, x5)  =  U16_aaa(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa
COIL_IT_IN_AG(x1, x2)  =  COIL_IT_IN_AG(x2)
U13_AG(x1, x2, x3)  =  U13_AG(x3)

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

(73) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(74) Obligation:

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

COIL_IT_IN_AG(odd) → COIL_IT_IN_AG(even)
COIL_IT_IN_AG(even) → U13_AG(reverse2_in_aa)
U13_AG(reverse2_out_aa) → COIL_IT_IN_AG(odd)

The TRS R consists of the following rules:

reverse2_in_aa → U15_aa(reverse_in_aga(nil))
U15_aa(reverse_out_aga) → reverse2_out_aa
reverse_in_aga(Reversed) → reverse_out_aga
reverse_in_aga(SoFar) → U16_aga(reverse_in_aaa)
U16_aga(reverse_out_aaa) → reverse_out_aga
reverse_in_aaa → reverse_out_aaa
reverse_in_aaa → U16_aaa(reverse_in_aaa)
U16_aaa(reverse_out_aaa) → reverse_out_aaa

The set Q consists of the following terms:

reverse2_in_aa
U15_aa(x0)
reverse_in_aga(x0)
U16_aga(x0)
reverse_in_aaa
U16_aaa(x0)

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

(75) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule COIL_IT_IN_AG(even) → U13_AG(reverse2_in_aa) at position [0] we obtained the following new rules [LPAR04]:

COIL_IT_IN_AG(even) → U13_AG(U15_aa(reverse_in_aga(nil)))

(76) Obligation:

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

COIL_IT_IN_AG(odd) → COIL_IT_IN_AG(even)
U13_AG(reverse2_out_aa) → COIL_IT_IN_AG(odd)
COIL_IT_IN_AG(even) → U13_AG(U15_aa(reverse_in_aga(nil)))

The TRS R consists of the following rules:

reverse2_in_aa → U15_aa(reverse_in_aga(nil))
U15_aa(reverse_out_aga) → reverse2_out_aa
reverse_in_aga(Reversed) → reverse_out_aga
reverse_in_aga(SoFar) → U16_aga(reverse_in_aaa)
U16_aga(reverse_out_aaa) → reverse_out_aga
reverse_in_aaa → reverse_out_aaa
reverse_in_aaa → U16_aaa(reverse_in_aaa)
U16_aaa(reverse_out_aaa) → reverse_out_aaa

The set Q consists of the following terms:

reverse2_in_aa
U15_aa(x0)
reverse_in_aga(x0)
U16_aga(x0)
reverse_in_aaa
U16_aaa(x0)

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

(77) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(78) Obligation:

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

COIL_IT_IN_AG(odd) → COIL_IT_IN_AG(even)
U13_AG(reverse2_out_aa) → COIL_IT_IN_AG(odd)
COIL_IT_IN_AG(even) → U13_AG(U15_aa(reverse_in_aga(nil)))

The TRS R consists of the following rules:

reverse_in_aga(Reversed) → reverse_out_aga
reverse_in_aga(SoFar) → U16_aga(reverse_in_aaa)
U15_aa(reverse_out_aga) → reverse2_out_aa
reverse_in_aaa → reverse_out_aaa
reverse_in_aaa → U16_aaa(reverse_in_aaa)
U16_aga(reverse_out_aaa) → reverse_out_aga
U16_aaa(reverse_out_aaa) → reverse_out_aaa

The set Q consists of the following terms:

reverse2_in_aa
U15_aa(x0)
reverse_in_aga(x0)
U16_aga(x0)
reverse_in_aaa
U16_aaa(x0)

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

(79) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

reverse2_in_aa

(80) Obligation:

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

COIL_IT_IN_AG(odd) → COIL_IT_IN_AG(even)
U13_AG(reverse2_out_aa) → COIL_IT_IN_AG(odd)
COIL_IT_IN_AG(even) → U13_AG(U15_aa(reverse_in_aga(nil)))

The TRS R consists of the following rules:

reverse_in_aga(Reversed) → reverse_out_aga
reverse_in_aga(SoFar) → U16_aga(reverse_in_aaa)
U15_aa(reverse_out_aga) → reverse2_out_aa
reverse_in_aaa → reverse_out_aaa
reverse_in_aaa → U16_aaa(reverse_in_aaa)
U16_aga(reverse_out_aaa) → reverse_out_aga
U16_aaa(reverse_out_aaa) → reverse_out_aaa

The set Q consists of the following terms:

U15_aa(x0)
reverse_in_aga(x0)
U16_aga(x0)
reverse_in_aaa
U16_aaa(x0)

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

(81) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = U13_AG(U15_aa(reverse_in_aga(Reversed))) evaluates to t =U13_AG(U15_aa(reverse_in_aga(nil)))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Matcher: [Reversed / nil]
• Semiunifier: [ ]

---

Rewriting sequence

U13_AG(U15_aa(reverse_in_aga(Reversed))) → U13_AG(U15_aa(reverse_out_aga))
with rule reverse_in_aga(Reversed') → reverse_out_aga at position [0,0] and matcher [Reversed' / Reversed]

U13_AG(U15_aa(reverse_out_aga)) → U13_AG(reverse2_out_aa)
with rule U15_aa(reverse_out_aga) → reverse2_out_aa at position [0] and matcher [ ]

U13_AG(reverse2_out_aa) → COIL_IT_IN_AG(odd)
with rule U13_AG(reverse2_out_aa) → COIL_IT_IN_AG(odd) at position [] and matcher [ ]

COIL_IT_IN_AG(odd) → COIL_IT_IN_AG(even)
with rule COIL_IT_IN_AG(odd) → COIL_IT_IN_AG(even) at position [] and matcher [ ]

COIL_IT_IN_AG(even) → U13_AG(U15_aa(reverse_in_aga(nil)))
with rule COIL_IT_IN_AG(even) → U13_AG(U15_aa(reverse_in_aga(nil)))

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.

(82) FALSE

(83) Obligation:

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

PART_OF_SNAKE_IN_AAAA(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → PART_OF_SNAKE_IN_AAAA(R, Rings, RestSnake, RestRings)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, nil) → s2l_out_ga(0, nil)
s2l_in_ga(s(X), cons(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), cons(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_gaa(Pattern, Cols, Rows))
snake_in_gaa(Pattern, Cols, Rows) → U5_gaa(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa(nil, S, S) → infinite_snake_out_gaa(nil, S, S)
infinite_snake_in_gaa(cons(A, R), cons(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(cons(A, R), cons(A, T), S)
U5_gaa(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_gaa(Pattern, Cols, Rows, produce_snake_in_aaaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_aaaa(nil, X2, X3, nil) → produce_snake_out_aaaa(nil, X2, X3, nil)
produce_snake_in_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_aaaa(nil, RestSnake, RestSnake, nil) → part_of_snake_out_aaaa(nil, RestSnake, RestSnake, nil)
part_of_snake_in_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_aaaa(R, Rings, RestSnake, RestRings))
U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_aaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings))
U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_aaaa(Rows, Cols, NewInfSnake, Tail))
U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_aaaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail))
U6_gaa(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → U7_gaa(Pattern, Cols, Rows, coil_it_in_ag(Snake, odd))
coil_it_in_ag(nil, X6) → coil_it_out_ag(nil, X6)
coil_it_in_ag(cons(Line, Lines), odd) → U12_ag(Line, Lines, coil_it_in_ag(Lines, even))
coil_it_in_ag(cons(Line, Lines), even) → U13_ag(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, nil, Reversed))
reverse_in_aga(nil, Reversed, Reversed) → reverse_out_aga(nil, Reversed, Reversed)
reverse_in_aga(cons(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
reverse_in_aaa(nil, Reversed, Reversed) → reverse_out_aaa(nil, Reversed, Reversed)
reverse_in_aaa(cons(Head, Tail), SoFar, Reversed) → U16_aaa(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
U16_aaa(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aaa(cons(Head, Tail), SoFar, Reversed)
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aga(cons(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, nil, Reversed)) → reverse2_out_aa(List, Reversed)
U13_ag(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_ag(Line, Lines, coil_it_in_ag(Lines, odd))
U14_ag(Line, Lines, coil_it_out_ag(Lines, odd)) → coil_it_out_ag(cons(Line, Lines), even)
U12_ag(Line, Lines, coil_it_out_ag(Lines, even)) → coil_it_out_ag(cons(Line, Lines), odd)
U7_gaa(Pattern, Cols, Rows, coil_it_out_ag(Snake, odd)) → snake_out_gaa(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_gaa(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x4)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x4)
snake_in_gaa(x1, x2, x3)  =  snake_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
nil  =  nil
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa
cons(x1, x2)  =  cons(x1, x2)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x4)
produce_snake_in_aaaa(x1, x2, x3, x4)  =  produce_snake_in_aaaa
produce_snake_out_aaaa(x1, x2, x3, x4)  =  produce_snake_out_aaaa
U9_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_aaaa(x7)
part_of_snake_in_aaaa(x1, x2, x3, x4)  =  part_of_snake_in_aaaa
part_of_snake_out_aaaa(x1, x2, x3, x4)  =  part_of_snake_out_aaaa
U11_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_aaaa(x7)
U10_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_aaaa(x7)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x4)
coil_it_in_ag(x1, x2)  =  coil_it_in_ag(x2)
coil_it_out_ag(x1, x2)  =  coil_it_out_ag
odd  =  odd
U12_ag(x1, x2, x3)  =  U12_ag(x3)
even  =  even
U13_ag(x1, x2, x3)  =  U13_ag(x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x5)
reverse_in_aaa(x1, x2, x3)  =  reverse_in_aaa
reverse_out_aaa(x1, x2, x3)  =  reverse_out_aaa
U16_aaa(x1, x2, x3, x4, x5)  =  U16_aaa(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa
U14_ag(x1, x2, x3)  =  U14_ag(x3)
snake_out_gaa(x1, x2, x3)  =  snake_out_gaa
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg
PART_OF_SNAKE_IN_AAAA(x1, x2, x3, x4)  =  PART_OF_SNAKE_IN_AAAA

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

(84) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(85) Obligation:

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

PART_OF_SNAKE_IN_AAAA(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → PART_OF_SNAKE_IN_AAAA(R, Rings, RestSnake, RestRings)

R is empty.
The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
PART_OF_SNAKE_IN_AAAA(x1, x2, x3, x4)  =  PART_OF_SNAKE_IN_AAAA

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

(86) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(87) Obligation:

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

PART_OF_SNAKE_IN_AAAA → PART_OF_SNAKE_IN_AAAA

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(88) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = PART_OF_SNAKE_IN_AAAA evaluates to t =PART_OF_SNAKE_IN_AAAA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Semiunifier: [ ]
• Matcher: [ ]

---

Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from PART_OF_SNAKE_IN_AAAA to PART_OF_SNAKE_IN_AAAA.

(89) FALSE

(90) Obligation:

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

U9_AAAA(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → PRODUCE_SNAKE_IN_AAAA(Rows, Cols, NewInfSnake, Tail)
PRODUCE_SNAKE_IN_AAAA(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_AAAA(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, nil) → s2l_out_ga(0, nil)
s2l_in_ga(s(X), cons(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), cons(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_gaa(Pattern, Cols, Rows))
snake_in_gaa(Pattern, Cols, Rows) → U5_gaa(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa(nil, S, S) → infinite_snake_out_gaa(nil, S, S)
infinite_snake_in_gaa(cons(A, R), cons(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(cons(A, R), cons(A, T), S)
U5_gaa(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_gaa(Pattern, Cols, Rows, produce_snake_in_aaaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_aaaa(nil, X2, X3, nil) → produce_snake_out_aaaa(nil, X2, X3, nil)
produce_snake_in_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_aaaa(nil, RestSnake, RestSnake, nil) → part_of_snake_out_aaaa(nil, RestSnake, RestSnake, nil)
part_of_snake_in_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_aaaa(R, Rings, RestSnake, RestRings))
U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_aaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings))
U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_aaaa(Rows, Cols, NewInfSnake, Tail))
U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_aaaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail))
U6_gaa(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → U7_gaa(Pattern, Cols, Rows, coil_it_in_ag(Snake, odd))
coil_it_in_ag(nil, X6) → coil_it_out_ag(nil, X6)
coil_it_in_ag(cons(Line, Lines), odd) → U12_ag(Line, Lines, coil_it_in_ag(Lines, even))
coil_it_in_ag(cons(Line, Lines), even) → U13_ag(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, nil, Reversed))
reverse_in_aga(nil, Reversed, Reversed) → reverse_out_aga(nil, Reversed, Reversed)
reverse_in_aga(cons(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
reverse_in_aaa(nil, Reversed, Reversed) → reverse_out_aaa(nil, Reversed, Reversed)
reverse_in_aaa(cons(Head, Tail), SoFar, Reversed) → U16_aaa(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
U16_aaa(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aaa(cons(Head, Tail), SoFar, Reversed)
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aga(cons(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, nil, Reversed)) → reverse2_out_aa(List, Reversed)
U13_ag(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_ag(Line, Lines, coil_it_in_ag(Lines, odd))
U14_ag(Line, Lines, coil_it_out_ag(Lines, odd)) → coil_it_out_ag(cons(Line, Lines), even)
U12_ag(Line, Lines, coil_it_out_ag(Lines, even)) → coil_it_out_ag(cons(Line, Lines), odd)
U7_gaa(Pattern, Cols, Rows, coil_it_out_ag(Snake, odd)) → snake_out_gaa(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_gaa(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x4)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x4)
snake_in_gaa(x1, x2, x3)  =  snake_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
nil  =  nil
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa
cons(x1, x2)  =  cons(x1, x2)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x4)
produce_snake_in_aaaa(x1, x2, x3, x4)  =  produce_snake_in_aaaa
produce_snake_out_aaaa(x1, x2, x3, x4)  =  produce_snake_out_aaaa
U9_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_aaaa(x7)
part_of_snake_in_aaaa(x1, x2, x3, x4)  =  part_of_snake_in_aaaa
part_of_snake_out_aaaa(x1, x2, x3, x4)  =  part_of_snake_out_aaaa
U11_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_aaaa(x7)
U10_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_aaaa(x7)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x4)
coil_it_in_ag(x1, x2)  =  coil_it_in_ag(x2)
coil_it_out_ag(x1, x2)  =  coil_it_out_ag
odd  =  odd
U12_ag(x1, x2, x3)  =  U12_ag(x3)
even  =  even
U13_ag(x1, x2, x3)  =  U13_ag(x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x5)
reverse_in_aaa(x1, x2, x3)  =  reverse_in_aaa
reverse_out_aaa(x1, x2, x3)  =  reverse_out_aaa
U16_aaa(x1, x2, x3, x4, x5)  =  U16_aaa(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa
U14_ag(x1, x2, x3)  =  U14_ag(x3)
snake_out_gaa(x1, x2, x3)  =  snake_out_gaa
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg
PRODUCE_SNAKE_IN_AAAA(x1, x2, x3, x4)  =  PRODUCE_SNAKE_IN_AAAA
U9_AAAA(x1, x2, x3, x4, x5, x6, x7)  =  U9_AAAA(x7)

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

(91) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(92) Obligation:

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

U9_AAAA(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → PRODUCE_SNAKE_IN_AAAA(Rows, Cols, NewInfSnake, Tail)
PRODUCE_SNAKE_IN_AAAA(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_AAAA(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))

The TRS R consists of the following rules:

part_of_snake_in_aaaa(nil, RestSnake, RestSnake, nil) → part_of_snake_out_aaaa(nil, RestSnake, RestSnake, nil)
part_of_snake_in_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_aaaa(R, Rings, RestSnake, RestRings))
U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_aaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings))

The argument filtering Pi contains the following mapping:
nil  =  nil
cons(x1, x2)  =  cons(x1, x2)
part_of_snake_in_aaaa(x1, x2, x3, x4)  =  part_of_snake_in_aaaa
part_of_snake_out_aaaa(x1, x2, x3, x4)  =  part_of_snake_out_aaaa
U11_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_aaaa(x7)
PRODUCE_SNAKE_IN_AAAA(x1, x2, x3, x4)  =  PRODUCE_SNAKE_IN_AAAA
U9_AAAA(x1, x2, x3, x4, x5, x6, x7)  =  U9_AAAA(x7)

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

(93) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(94) Obligation:

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

U9_AAAA(part_of_snake_out_aaaa) → PRODUCE_SNAKE_IN_AAAA
PRODUCE_SNAKE_IN_AAAA → U9_AAAA(part_of_snake_in_aaaa)

The TRS R consists of the following rules:

part_of_snake_in_aaaa → part_of_snake_out_aaaa
part_of_snake_in_aaaa → U11_aaaa(part_of_snake_in_aaaa)
U11_aaaa(part_of_snake_out_aaaa) → part_of_snake_out_aaaa

The set Q consists of the following terms:

part_of_snake_in_aaaa
U11_aaaa(x0)

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

(95) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule PRODUCE_SNAKE_IN_AAAA → U9_AAAA(part_of_snake_in_aaaa) at position [0] we obtained the following new rules [LPAR04]:

PRODUCE_SNAKE_IN_AAAA → U9_AAAA(part_of_snake_out_aaaa)
PRODUCE_SNAKE_IN_AAAA → U9_AAAA(U11_aaaa(part_of_snake_in_aaaa))

(96) Obligation:

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

U9_AAAA(part_of_snake_out_aaaa) → PRODUCE_SNAKE_IN_AAAA
PRODUCE_SNAKE_IN_AAAA → U9_AAAA(part_of_snake_out_aaaa)
PRODUCE_SNAKE_IN_AAAA → U9_AAAA(U11_aaaa(part_of_snake_in_aaaa))

The TRS R consists of the following rules:

part_of_snake_in_aaaa → part_of_snake_out_aaaa
part_of_snake_in_aaaa → U11_aaaa(part_of_snake_in_aaaa)
U11_aaaa(part_of_snake_out_aaaa) → part_of_snake_out_aaaa

The set Q consists of the following terms:

part_of_snake_in_aaaa
U11_aaaa(x0)

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

(97) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = PRODUCE_SNAKE_IN_AAAA evaluates to t =PRODUCE_SNAKE_IN_AAAA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Matcher: [ ]
• Semiunifier: [ ]

---

Rewriting sequence

PRODUCE_SNAKE_IN_AAAA → U9_AAAA(part_of_snake_out_aaaa)
with rule PRODUCE_SNAKE_IN_AAAA → U9_AAAA(part_of_snake_out_aaaa) at position [] and matcher [ ]

U9_AAAA(part_of_snake_out_aaaa) → PRODUCE_SNAKE_IN_AAAA
with rule U9_AAAA(part_of_snake_out_aaaa) → PRODUCE_SNAKE_IN_AAAA

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.

(98) FALSE

(99) Obligation:

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

INFINITE_SNAKE_IN_GAA(cons(A, R), cons(A, T), S) → INFINITE_SNAKE_IN_GAA(R, T, S)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, nil) → s2l_out_ga(0, nil)
s2l_in_ga(s(X), cons(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), cons(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_gaa(Pattern, Cols, Rows))
snake_in_gaa(Pattern, Cols, Rows) → U5_gaa(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa(nil, S, S) → infinite_snake_out_gaa(nil, S, S)
infinite_snake_in_gaa(cons(A, R), cons(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(cons(A, R), cons(A, T), S)
U5_gaa(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_gaa(Pattern, Cols, Rows, produce_snake_in_aaaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_aaaa(nil, X2, X3, nil) → produce_snake_out_aaaa(nil, X2, X3, nil)
produce_snake_in_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_aaaa(nil, RestSnake, RestSnake, nil) → part_of_snake_out_aaaa(nil, RestSnake, RestSnake, nil)
part_of_snake_in_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_aaaa(R, Rings, RestSnake, RestRings))
U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_aaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings))
U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_aaaa(Rows, Cols, NewInfSnake, Tail))
U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_aaaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail))
U6_gaa(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → U7_gaa(Pattern, Cols, Rows, coil_it_in_ag(Snake, odd))
coil_it_in_ag(nil, X6) → coil_it_out_ag(nil, X6)
coil_it_in_ag(cons(Line, Lines), odd) → U12_ag(Line, Lines, coil_it_in_ag(Lines, even))
coil_it_in_ag(cons(Line, Lines), even) → U13_ag(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, nil, Reversed))
reverse_in_aga(nil, Reversed, Reversed) → reverse_out_aga(nil, Reversed, Reversed)
reverse_in_aga(cons(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
reverse_in_aaa(nil, Reversed, Reversed) → reverse_out_aaa(nil, Reversed, Reversed)
reverse_in_aaa(cons(Head, Tail), SoFar, Reversed) → U16_aaa(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
U16_aaa(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aaa(cons(Head, Tail), SoFar, Reversed)
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aga(cons(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, nil, Reversed)) → reverse2_out_aa(List, Reversed)
U13_ag(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_ag(Line, Lines, coil_it_in_ag(Lines, odd))
U14_ag(Line, Lines, coil_it_out_ag(Lines, odd)) → coil_it_out_ag(cons(Line, Lines), even)
U12_ag(Line, Lines, coil_it_out_ag(Lines, even)) → coil_it_out_ag(cons(Line, Lines), odd)
U7_gaa(Pattern, Cols, Rows, coil_it_out_ag(Snake, odd)) → snake_out_gaa(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_gaa(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x4)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x4)
snake_in_gaa(x1, x2, x3)  =  snake_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
nil  =  nil
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa
cons(x1, x2)  =  cons(x1, x2)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x4)
produce_snake_in_aaaa(x1, x2, x3, x4)  =  produce_snake_in_aaaa
produce_snake_out_aaaa(x1, x2, x3, x4)  =  produce_snake_out_aaaa
U9_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_aaaa(x7)
part_of_snake_in_aaaa(x1, x2, x3, x4)  =  part_of_snake_in_aaaa
part_of_snake_out_aaaa(x1, x2, x3, x4)  =  part_of_snake_out_aaaa
U11_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_aaaa(x7)
U10_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_aaaa(x7)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x4)
coil_it_in_ag(x1, x2)  =  coil_it_in_ag(x2)
coil_it_out_ag(x1, x2)  =  coil_it_out_ag
odd  =  odd
U12_ag(x1, x2, x3)  =  U12_ag(x3)
even  =  even
U13_ag(x1, x2, x3)  =  U13_ag(x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x5)
reverse_in_aaa(x1, x2, x3)  =  reverse_in_aaa
reverse_out_aaa(x1, x2, x3)  =  reverse_out_aaa
U16_aaa(x1, x2, x3, x4, x5)  =  U16_aaa(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa
U14_ag(x1, x2, x3)  =  U14_ag(x3)
snake_out_gaa(x1, x2, x3)  =  snake_out_gaa
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg
INFINITE_SNAKE_IN_GAA(x1, x2, x3)  =  INFINITE_SNAKE_IN_GAA(x1)

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

(100) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(101) Obligation:

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

INFINITE_SNAKE_IN_GAA(cons(A, R), cons(A, T), S) → INFINITE_SNAKE_IN_GAA(R, T, S)

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

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

(102) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(103) Obligation:

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

INFINITE_SNAKE_IN_GAA(cons(A, R)) → INFINITE_SNAKE_IN_GAA(R)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(104) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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_IN_GAA(cons(A, R)) → INFINITE_SNAKE_IN_GAA(R)
  The graph contains the following edges 1 > 1

(105) TRUE

(106) Obligation:

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

S2L_IN_GA(s(X), cons(X1, Y)) → S2L_IN_GA(X, Y)

The TRS R consists of the following rules:

test_snake_in_ggg(Pattern, C, R) → U1_ggg(Pattern, C, R, s2l_in_ga(C, Cols))
s2l_in_ga(0, nil) → s2l_out_ga(0, nil)
s2l_in_ga(s(X), cons(X1, Y)) → U4_ga(X, X1, Y, s2l_in_ga(X, Y))
U4_ga(X, X1, Y, s2l_out_ga(X, Y)) → s2l_out_ga(s(X), cons(X1, Y))
U1_ggg(Pattern, C, R, s2l_out_ga(C, Cols)) → U2_ggg(Pattern, C, R, Cols, s2l_in_ga(R, Rows))
U2_ggg(Pattern, C, R, Cols, s2l_out_ga(R, Rows)) → U3_ggg(Pattern, C, R, snake_in_gaa(Pattern, Cols, Rows))
snake_in_gaa(Pattern, Cols, Rows) → U5_gaa(Pattern, Cols, Rows, infinite_snake_in_gaa(Pattern, InfSnake, InfSnake))
infinite_snake_in_gaa(nil, S, S) → infinite_snake_out_gaa(nil, S, S)
infinite_snake_in_gaa(cons(A, R), cons(A, T), S) → U8_gaa(A, R, T, S, infinite_snake_in_gaa(R, T, S))
U8_gaa(A, R, T, S, infinite_snake_out_gaa(R, T, S)) → infinite_snake_out_gaa(cons(A, R), cons(A, T), S)
U5_gaa(Pattern, Cols, Rows, infinite_snake_out_gaa(Pattern, InfSnake, InfSnake)) → U6_gaa(Pattern, Cols, Rows, produce_snake_in_aaaa(Rows, Cols, InfSnake, Snake))
produce_snake_in_aaaa(nil, X2, X3, nil) → produce_snake_out_aaaa(nil, X2, X3, nil)
produce_snake_in_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail)) → U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_in_aaaa(Cols, InfSnake, NewInfSnake, Part))
part_of_snake_in_aaaa(nil, RestSnake, RestSnake, nil) → part_of_snake_out_aaaa(nil, RestSnake, RestSnake, nil)
part_of_snake_in_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings)) → U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_in_aaaa(R, Rings, RestSnake, RestRings))
U11_aaaa(X5, R, Ring, Rings, RestSnake, RestRings, part_of_snake_out_aaaa(R, Rings, RestSnake, RestRings)) → part_of_snake_out_aaaa(cons(X5, R), cons(Ring, Rings), RestSnake, cons(Ring, RestRings))
U9_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, part_of_snake_out_aaaa(Cols, InfSnake, NewInfSnake, Part)) → U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_in_aaaa(Rows, Cols, NewInfSnake, Tail))
U10_aaaa(X4, Rows, Cols, InfSnake, Part, Tail, produce_snake_out_aaaa(Rows, Cols, NewInfSnake, Tail)) → produce_snake_out_aaaa(cons(X4, Rows), Cols, InfSnake, cons(Part, Tail))
U6_gaa(Pattern, Cols, Rows, produce_snake_out_aaaa(Rows, Cols, InfSnake, Snake)) → U7_gaa(Pattern, Cols, Rows, coil_it_in_ag(Snake, odd))
coil_it_in_ag(nil, X6) → coil_it_out_ag(nil, X6)
coil_it_in_ag(cons(Line, Lines), odd) → U12_ag(Line, Lines, coil_it_in_ag(Lines, even))
coil_it_in_ag(cons(Line, Lines), even) → U13_ag(Line, Lines, reverse2_in_aa(Line, Line1))
reverse2_in_aa(List, Reversed) → U15_aa(List, Reversed, reverse_in_aga(List, nil, Reversed))
reverse_in_aga(nil, Reversed, Reversed) → reverse_out_aga(nil, Reversed, Reversed)
reverse_in_aga(cons(Head, Tail), SoFar, Reversed) → U16_aga(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
reverse_in_aaa(nil, Reversed, Reversed) → reverse_out_aaa(nil, Reversed, Reversed)
reverse_in_aaa(cons(Head, Tail), SoFar, Reversed) → U16_aaa(Head, Tail, SoFar, Reversed, reverse_in_aaa(Tail, cons(Head, SoFar), Reversed))
U16_aaa(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aaa(cons(Head, Tail), SoFar, Reversed)
U16_aga(Head, Tail, SoFar, Reversed, reverse_out_aaa(Tail, cons(Head, SoFar), Reversed)) → reverse_out_aga(cons(Head, Tail), SoFar, Reversed)
U15_aa(List, Reversed, reverse_out_aga(List, nil, Reversed)) → reverse2_out_aa(List, Reversed)
U13_ag(Line, Lines, reverse2_out_aa(Line, Line1)) → U14_ag(Line, Lines, coil_it_in_ag(Lines, odd))
U14_ag(Line, Lines, coil_it_out_ag(Lines, odd)) → coil_it_out_ag(cons(Line, Lines), even)
U12_ag(Line, Lines, coil_it_out_ag(Lines, even)) → coil_it_out_ag(cons(Line, Lines), odd)
U7_gaa(Pattern, Cols, Rows, coil_it_out_ag(Snake, odd)) → snake_out_gaa(Pattern, Cols, Rows)
U3_ggg(Pattern, C, R, snake_out_gaa(Pattern, Cols, Rows)) → test_snake_out_ggg(Pattern, C, R)

The argument filtering Pi contains the following mapping:
test_snake_in_ggg(x1, x2, x3)  =  test_snake_in_ggg(x1, x2, x3)
U1_ggg(x1, x2, x3, x4)  =  U1_ggg(x1, x3, x4)
s2l_in_ga(x1, x2)  =  s2l_in_ga(x1)
0  =  0
s2l_out_ga(x1, x2)  =  s2l_out_ga
s(x1)  =  s(x1)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x4)
U2_ggg(x1, x2, x3, x4, x5)  =  U2_ggg(x1, x5)
U3_ggg(x1, x2, x3, x4)  =  U3_ggg(x4)
snake_in_gaa(x1, x2, x3)  =  snake_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
infinite_snake_in_gaa(x1, x2, x3)  =  infinite_snake_in_gaa(x1)
nil  =  nil
infinite_snake_out_gaa(x1, x2, x3)  =  infinite_snake_out_gaa
cons(x1, x2)  =  cons(x1, x2)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
U6_gaa(x1, x2, x3, x4)  =  U6_gaa(x4)
produce_snake_in_aaaa(x1, x2, x3, x4)  =  produce_snake_in_aaaa
produce_snake_out_aaaa(x1, x2, x3, x4)  =  produce_snake_out_aaaa
U9_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U9_aaaa(x7)
part_of_snake_in_aaaa(x1, x2, x3, x4)  =  part_of_snake_in_aaaa
part_of_snake_out_aaaa(x1, x2, x3, x4)  =  part_of_snake_out_aaaa
U11_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_aaaa(x7)
U10_aaaa(x1, x2, x3, x4, x5, x6, x7)  =  U10_aaaa(x7)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x4)
coil_it_in_ag(x1, x2)  =  coil_it_in_ag(x2)
coil_it_out_ag(x1, x2)  =  coil_it_out_ag
odd  =  odd
U12_ag(x1, x2, x3)  =  U12_ag(x3)
even  =  even
U13_ag(x1, x2, x3)  =  U13_ag(x3)
reverse2_in_aa(x1, x2)  =  reverse2_in_aa
U15_aa(x1, x2, x3)  =  U15_aa(x3)
reverse_in_aga(x1, x2, x3)  =  reverse_in_aga(x2)
reverse_out_aga(x1, x2, x3)  =  reverse_out_aga
U16_aga(x1, x2, x3, x4, x5)  =  U16_aga(x5)
reverse_in_aaa(x1, x2, x3)  =  reverse_in_aaa
reverse_out_aaa(x1, x2, x3)  =  reverse_out_aaa
U16_aaa(x1, x2, x3, x4, x5)  =  U16_aaa(x5)
reverse2_out_aa(x1, x2)  =  reverse2_out_aa
U14_ag(x1, x2, x3)  =  U14_ag(x3)
snake_out_gaa(x1, x2, x3)  =  snake_out_gaa
test_snake_out_ggg(x1, x2, x3)  =  test_snake_out_ggg
S2L_IN_GA(x1, x2)  =  S2L_IN_GA(x1)

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

(107) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(108) Obligation:

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

S2L_IN_GA(s(X), cons(X1, Y)) → S2L_IN_GA(X, Y)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
cons(x1, x2)  =  cons(x1, x2)
S2L_IN_GA(x1, x2)  =  S2L_IN_GA(x1)

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

(109) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(110) Obligation:

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

S2L_IN_GA(s(X)) → S2L_IN_GA(X)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(111) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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_IN_GA(s(X)) → S2L_IN_GA(X)
  The graph contains the following edges 1 > 1

(112) TRUE