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

(0) Obligation:

Clauses:

palindrome(Xs) :- reverse(Xs, Xs).
reverse(X1s, X2s) :- reverse(X1s, [], X2s).
reverse([], Xs, Xs).
reverse(.(X, X1s), X2s, Ys) :- reverse(X1s, .(X, X2s), Ys).

Query: palindrome(g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: palindrome(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: palindrome(T1), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: reverse(T3, T3)\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: reverse(T3, T3), SCOPE: 2, CLAUSE: 1\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: reverse(T6, [], T6)\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: reverse(T6, [], T6), SCOPE: 3, CLAUSE: 2 | reverse(T6, [], T6), SCOPE: 3, CLAUSE: 3\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: reverse(T6, [], T6), SCOPE: 3, CLAUSE: 2\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: reverse(T6, [], T6), SCOPE: 3, CLAUSE: 3\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: reverse(T12, .(T11, []), .(T11, T12))\n\nT11 is ground\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: reverse(T12, .(T11, []), .(T11, T12)), SCOPE: 4, CLAUSE: 2 | reverse(T12, .(T11, []), .(T11, T12)), SCOPE: 4, CLAUSE: 3\n\nT11 is ground\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: reverse(T12, .(T11, []), .(T11, T12)), SCOPE: 4, CLAUSE: 2\n\nT11 is ground\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: reverse(T12, .(T11, []), .(T11, T12)), SCOPE: 4, CLAUSE: 3\n\nT11 is ground\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: reverse(T27, .(T26, .(T28, [])), .(T28, .(T26, T27)))\n\nT26 is ground\nT27 is ground\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: reverse(T27, .(T26, .(T28, [])), .(T28, .(T26, T27))), SCOPE: 5, CLAUSE: 2 | reverse(T27, .(T26, .(T28, [])), .(T28, .(T26, T27))), SCOPE: 5, CLAUSE: 3\n\nT26 is ground\nT27 is ground\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: reverse(T27, .(T26, .(T28, [])), .(T28, .(T26, T27))), SCOPE: 5, CLAUSE: 2\n\nT26 is ground\nT27 is ground\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: reverse(T27, .(T26, .(T28, [])), .(T28, .(T26, T27))), SCOPE: 5, CLAUSE: 3\n\nT26 is ground\nT27 is ground\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: reverse(T52, .(T51, .(T53, .(T54, []))), .(T54, .(T53, .(T51, T52))))\n\nT51 is ground\nT52 is ground\nT53 is ground\nT54 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: reverse(T52, .(T51, .(T53, .(T54, []))), .(T54, .(T53, .(T51, T52)))), SCOPE: 6, CLAUSE: 2 | reverse(T52, .(T51, .(T53, .(T54, []))), .(T54, .(T53, .(T51, T52)))), SCOPE: 6, CLAUSE: 3\n\nT51 is ground\nT52 is ground\nT53 is ground\nT54 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: reverse(T52, .(T51, .(T53, .(T54, []))), .(T54, .(T53, .(T51, T52)))), SCOPE: 6, CLAUSE: 2\n\nT51 is ground\nT52 is ground\nT53 is ground\nT54 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: reverse(T52, .(T51, .(T53, .(T54, []))), .(T54, .(T53, .(T51, T52)))), SCOPE: 6, CLAUSE: 3\n\nT51 is ground\nT52 is ground\nT53 is ground\nT54 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: reverse(T87, .(T86, .(T88, .(T89, .(T90, [])))), .(T90, .(T89, .(T88, .(T86, T87)))))\n\nT86 is ground\nT87 is ground\nT88 is ground\nT89 is ground\nT90 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: reverse(T87, .(T86, .(T88, .(T89, .(T90, [])))), .(T90, .(T89, .(T88, .(T86, T87))))), SCOPE: 7, CLAUSE: 2 | reverse(T87, .(T86, .(T88, .(T89, .(T90, [])))), .(T90, .(T89, .(T88, .(T86, T87))))), SCOPE: 7, CLAUSE: 3\n\nT86 is ground\nT87 is ground\nT88 is ground\nT89 is ground\nT90 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: reverse(T87, .(T86, .(T88, .(T89, .(T90, [])))), .(T90, .(T89, .(T88, .(T86, T87))))), SCOPE: 7, CLAUSE: 2\n\nT86 is ground\nT87 is ground\nT88 is ground\nT89 is ground\nT90 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: reverse(T87, .(T86, .(T88, .(T89, .(T90, [])))), .(T90, .(T89, .(T88, .(T86, T87))))), SCOPE: 7, CLAUSE: 3\n\nT86 is ground\nT87 is ground\nT88 is ground\nT89 is ground\nT90 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: reverse(T132, .(T131, .(T133, .(T134, .(T135, .(T136, []))))), .(T136, .(T135, .(T134, .(T133, .(T131, T132))))))\n\nT131 is ground\nT132 is ground\nT133 is ground\nT134 is ground\nT135 is ground\nT136 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: reverse(T132, .(T131, .(T133, .(T134, .(T135, .(T136, []))))), .(T136, .(T135, .(T134, .(T133, .(T131, T132)))))), SCOPE: 8, CLAUSE: 2 | reverse(T132, .(T131, .(T133, .(T134, .(T135, .(T136, []))))), .(T136, .(T135, .(T134, .(T133, .(T131, T132)))))), SCOPE: 8, CLAUSE: 3\n\nT131 is ground\nT132 is ground\nT133 is ground\nT134 is ground\nT135 is ground\nT136 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: reverse(T132, .(T131, .(T133, .(T134, .(T135, .(T136, []))))), .(T136, .(T135, .(T134, .(T133, .(T131, T132)))))), SCOPE: 8, CLAUSE: 2\n\nT131 is ground\nT132 is ground\nT133 is ground\nT134 is ground\nT135 is ground\nT136 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: reverse(T132, .(T131, .(T133, .(T134, .(T135, .(T136, []))))), .(T136, .(T135, .(T134, .(T133, .(T131, T132)))))), SCOPE: 8, CLAUSE: 3\n\nT131 is ground\nT132 is ground\nT133 is ground\nT134 is ground\nT135 is ground\nT136 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: reverse(T187, .(T186, .(T188, .(T189, .(T190, .(T191, .(T192, [])))))), .(T192, .(T191, .(T190, .(T189, .(T188, .(T186, T187)))))))\n\nT186 is ground\nT187 is ground\nT188 is ground\nT189 is ground\nT190 is ground\nT191 is ground\nT192 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: reverse(T187, .(T186, .(T188, .(T189, .(T190, .(T191, .(T192, [])))))), .(T192, .(T191, .(T190, .(T189, .(T188, .(T186, T187))))))), SCOPE: 9, CLAUSE: 2 | reverse(T187, .(T186, .(T188, .(T189, .(T190, .(T191, .(T192, [])))))), .(T192, .(T191, .(T190, .(T189, .(T188, .(T186, T187))))))), SCOPE: 9, CLAUSE: 3\n\nT186 is ground\nT187 is ground\nT188 is ground\nT189 is ground\nT190 is ground\nT191 is ground\nT192 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: reverse(T187, .(T186, .(T188, .(T189, .(T190, .(T191, .(T192, [])))))), .(T192, .(T191, .(T190, .(T189, .(T188, .(T186, T187))))))), SCOPE: 9, CLAUSE: 2\n\nT186 is ground\nT187 is ground\nT188 is ground\nT189 is ground\nT190 is ground\nT191 is ground\nT192 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: reverse(T187, .(T186, .(T188, .(T189, .(T190, .(T191, .(T192, [])))))), .(T192, .(T191, .(T190, .(T189, .(T188, .(T186, T187))))))), SCOPE: 9, CLAUSE: 3\n\nT186 is ground\nT187 is ground\nT188 is ground\nT189 is ground\nT190 is ground\nT191 is ground\nT192 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: reverse(T252, .(T251, .(T253, .(T254, .(T255, .(T256, .(T257, .(T258, []))))))), .(T258, .(T257, .(T256, .(T255, .(T254, .(T253, .(T251, T252))))))))\n\nT251 is ground\nT252 is ground\nT253 is ground\nT254 is ground\nT255 is ground\nT256 is ground\nT257 is ground\nT258 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: reverse(T252, .(T251, .(T253, .(T254, .(T255, .(T256, .(T257, .(T258, []))))))), .(T258, .(T257, .(T256, .(T255, .(T254, .(T253, .(T251, T252)))))))), SCOPE: 10, CLAUSE: 2 | reverse(T252, .(T251, .(T253, .(T254, .(T255, .(T256, .(T257, .(T258, []))))))), .(T258, .(T257, .(T256, .(T255, .(T254, .(T253, .(T251, T252)))))))), SCOPE: 10, CLAUSE: 3\n\nT251 is ground\nT252 is ground\nT253 is ground\nT254 is ground\nT255 is ground\nT256 is ground\nT257 is ground\nT258 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: reverse(T252, .(T251, .(T253, .(T254, .(T255, .(T256, .(T257, .(T258, []))))))), .(T258, .(T257, .(T256, .(T255, .(T254, .(T253, .(T251, T252)))))))), SCOPE: 10, CLAUSE: 2\n\nT251 is ground\nT252 is ground\nT253 is ground\nT254 is ground\nT255 is ground\nT256 is ground\nT257 is ground\nT258 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: reverse(T252, .(T251, .(T253, .(T254, .(T255, .(T256, .(T257, .(T258, []))))))), .(T258, .(T257, .(T256, .(T255, .(T254, .(T253, .(T251, T252)))))))), SCOPE: 10, CLAUSE: 3\n\nT251 is ground\nT252 is ground\nT253 is ground\nT254 is ground\nT255 is ground\nT256 is ground\nT257 is ground\nT258 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: reverse(T327, .(T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, [])))))))), .(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))\n\nT326 is ground\nT327 is ground\nT328 is ground\nT329 is ground\nT330 is ground\nT331 is ground\nT332 is ground\nT333 is ground\nT334 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="B: reverse(T327, .(T326, T351), .(T334, T352))\n\nT326 is ground\nT327 is ground\nT334 is ground\nT351 is ground\nT352 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: reverse(T327, .(T326, T351), .(T334, T352)), SCOPE: 11, CLAUSE: 2 | reverse(T327, .(T326, T351), .(T334, T352)), SCOPE: 11, CLAUSE: 3\n\nT326 is ground\nT327 is ground\nT334 is ground\nT351 is ground\nT352 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
220 [label="220: reverse(T327, .(T326, T351), .(T334, T352)), SCOPE: 11, CLAUSE: 2\n\nT326 is ground\nT327 is ground\nT334 is ground\nT351 is ground\nT352 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="221: reverse(T327, .(T326, T351), .(T334, T352)), SCOPE: 11, CLAUSE: 3\n\nT326 is ground\nT327 is ground\nT334 is ground\nT351 is ground\nT352 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
224 [label="224: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="231: reverse(T380, .(T379, .(T381, T382)), .(T383, T384))\n\nT379 is ground\nT380 is ground\nT381 is ground\nT382 is ground\nT383 is ground\nT384 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
233 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 233 [arrowhead = none ];
233 -> 4;

234 [label="ONLY EVAL with clause\npalindrome(X2) :- reverse(X2, X2).\nand substitutionT1 -> T3,\nX2 -> T3", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 234 [arrowhead = none ];
234 -> 8;

235 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
8 -> 235 [arrowhead = none ];
235 -> 10;

236 [label="ONLY EVAL with clause\nreverse(X9, X10) :- reverse(X9, [], X10).\nand substitutionT3 -> T6,\nX9 -> T6,\nX10 -> T6", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 236 [arrowhead = none ];
236 -> 13;

237 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
13 -> 237 [arrowhead = none ];
237 -> 14;

238 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 238 [arrowhead = none ];
238 -> 18;

239 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
14 -> 239 [arrowhead = none ];
239 -> 19;

240 [label="EVAL with clause\nreverse([], X17, X17).\nand substitutionT6 -> [],\nX17 -> []", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 240 [arrowhead = none ];
240 -> 24;

241 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
18 -> 241 [arrowhead = none ];
241 -> 28;

242 [label="EVAL with clause\nreverse(.(X26, X27), X28, X29) :- reverse(X27, .(X26, X28), X29).\nand substitutionX26 -> T11,\nX27 -> T12,\nT6 -> .(T11, T12),\nX28 -> [],\nX29 -> .(T11, T12)", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 242 [arrowhead = none ];
242 -> 38;

243 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 243 [arrowhead = none ];
243 -> 39;

244 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
24 -> 244 [arrowhead = none ];
244 -> 30;

245 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
38 -> 245 [arrowhead = none ];
245 -> 42;

246 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
42 -> 246 [arrowhead = none ];
246 -> 47;

247 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
42 -> 247 [arrowhead = none ];
247 -> 48;

248 [label="EVAL with clause\nreverse([], X36, X36).\nand substitutionT12 -> [],\nT11 -> T19,\nX36 -> .(T19, [])", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 248 [arrowhead = none ];
248 -> 52;

249 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
47 -> 249 [arrowhead = none ];
249 -> 53;

250 [label="EVAL with clause\nreverse(.(X45, X46), X47, X48) :- reverse(X46, .(X45, X47), X48).\nand substitutionX45 -> T26,\nX46 -> T27,\nT12 -> .(T26, T27),\nT11 -> T28,\nX47 -> .(T28, []),\nX48 -> .(T28, .(T26, T27))", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 250 [arrowhead = none ];
250 -> 61;

251 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
48 -> 251 [arrowhead = none ];
251 -> 62;

252 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
52 -> 252 [arrowhead = none ];
252 -> 54;

253 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
61 -> 253 [arrowhead = none ];
253 -> 74;

254 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
74 -> 254 [arrowhead = none ];
254 -> 77;

255 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
74 -> 255 [arrowhead = none ];
255 -> 80;

256 [label="EVAL with clause\nreverse([], X55, X55).\nand substitutionT27 -> [],\nT26 -> T42,\nT28 -> T42,\nX55 -> .(T42, .(T42, [])),\nT41 -> T42", fontsize=14, style = filled, fillcolor = lightblue];
77 -> 256 [arrowhead = none ];
256 -> 81;

257 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
77 -> 257 [arrowhead = none ];
257 -> 82;

258 [label="EVAL with clause\nreverse(.(X64, X65), X66, X67) :- reverse(X65, .(X64, X66), X67).\nand substitutionX64 -> T51,\nX65 -> T52,\nT27 -> .(T51, T52),\nT26 -> T53,\nT28 -> T54,\nX66 -> .(T53, .(T54, [])),\nX67 -> .(T54, .(T53, .(T51, T52)))", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 258 [arrowhead = none ];
258 -> 92;

259 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
80 -> 259 [arrowhead = none ];
259 -> 93;

260 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
81 -> 260 [arrowhead = none ];
260 -> 83;

261 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
92 -> 261 [arrowhead = none ];
261 -> 95;

262 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
95 -> 262 [arrowhead = none ];
262 -> 104;

263 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
95 -> 263 [arrowhead = none ];
263 -> 105;

264 [label="EVAL with clause\nreverse([], X74, X74).\nand substitutionT52 -> [],\nT51 -> T75,\nT53 -> T74,\nT54 -> T75,\nX74 -> .(T75, .(T74, .(T75, []))),\nT73 -> T75", fontsize=14, style = filled, fillcolor = lightblue];
104 -> 264 [arrowhead = none ];
264 -> 107;

265 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
104 -> 265 [arrowhead = none ];
265 -> 108;

266 [label="EVAL with clause\nreverse(.(X83, X84), X85, X86) :- reverse(X84, .(X83, X85), X86).\nand substitutionX83 -> T86,\nX84 -> T87,\nT52 -> .(T86, T87),\nT51 -> T88,\nT53 -> T89,\nT54 -> T90,\nX85 -> .(T88, .(T89, .(T90, []))),\nX86 -> .(T90, .(T89, .(T88, .(T86, T87))))", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 266 [arrowhead = none ];
266 -> 117;

267 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
105 -> 267 [arrowhead = none ];
267 -> 118;

268 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
107 -> 268 [arrowhead = none ];
268 -> 109;

269 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
117 -> 269 [arrowhead = none ];
269 -> 129;

270 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
129 -> 270 [arrowhead = none ];
270 -> 135;

271 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
129 -> 271 [arrowhead = none ];
271 -> 136;

272 [label="EVAL with clause\nreverse([], X93, X93).\nand substitutionT87 -> [],\nT86 -> T118,\nT88 -> T117,\nT89 -> T117,\nT90 -> T118,\nX93 -> .(T118, .(T117, .(T117, .(T118, [])))),\nT115 -> T118,\nT116 -> T117", fontsize=14, style = filled, fillcolor = lightblue];
135 -> 272 [arrowhead = none ];
272 -> 137;

273 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
135 -> 273 [arrowhead = none ];
273 -> 139;

274 [label="EVAL with clause\nreverse(.(X102, X103), X104, X105) :- reverse(X103, .(X102, X104), X105).\nand substitutionX102 -> T131,\nX103 -> T132,\nT87 -> .(T131, T132),\nT86 -> T133,\nT88 -> T134,\nT89 -> T135,\nT90 -> T136,\nX104 -> .(T133, .(T134, .(T135, .(T136, [])))),\nX105 -> .(T136, .(T135, .(T134, .(T133, .(T131, T132)))))", fontsize=14, style = filled, fillcolor = lightblue];
136 -> 274 [arrowhead = none ];
274 -> 145;

275 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
136 -> 275 [arrowhead = none ];
275 -> 146;

276 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
137 -> 276 [arrowhead = none ];
276 -> 140;

277 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
145 -> 277 [arrowhead = none ];
277 -> 153;

278 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
153 -> 278 [arrowhead = none ];
278 -> 156;

279 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
153 -> 279 [arrowhead = none ];
279 -> 157;

280 [label="EVAL with clause\nreverse([], X112, X112).\nand substitutionT132 -> [],\nT131 -> T171,\nT133 -> T170,\nT134 -> T169,\nT135 -> T170,\nT136 -> T171,\nX112 -> .(T171, .(T170, .(T169, .(T170, .(T171, []))))),\nT167 -> T171,\nT168 -> T170", fontsize=14, style = filled, fillcolor = lightblue];
156 -> 280 [arrowhead = none ];
280 -> 164;

281 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
156 -> 281 [arrowhead = none ];
281 -> 165;

282 [label="EVAL with clause\nreverse(.(X121, X122), X123, X124) :- reverse(X122, .(X121, X123), X124).\nand substitutionX121 -> T186,\nX122 -> T187,\nT132 -> .(T186, T187),\nT131 -> T188,\nT133 -> T189,\nT134 -> T190,\nT135 -> T191,\nT136 -> T192,\nX123 -> .(T188, .(T189, .(T190, .(T191, .(T192, []))))),\nX124 -> .(T192, .(T191, .(T190, .(T189, .(T188, .(T186, T187))))))", fontsize=14, style = filled, fillcolor = lightblue];
157 -> 282 [arrowhead = none ];
282 -> 177;

283 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
157 -> 283 [arrowhead = none ];
283 -> 178;

284 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
164 -> 284 [arrowhead = none ];
284 -> 166;

285 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
177 -> 285 [arrowhead = none ];
285 -> 179;

286 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
179 -> 286 [arrowhead = none ];
286 -> 181;

287 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
179 -> 287 [arrowhead = none ];
287 -> 182;

288 [label="EVAL with clause\nreverse([], X131, X131).\nand substitutionT187 -> [],\nT186 -> T234,\nT188 -> T233,\nT189 -> T232,\nT190 -> T232,\nT191 -> T233,\nT192 -> T234,\nX131 -> .(T234, .(T233, .(T232, .(T232, .(T233, .(T234, [])))))),\nT229 -> T234,\nT230 -> T233,\nT231 -> T232", fontsize=14, style = filled, fillcolor = lightblue];
181 -> 288 [arrowhead = none ];
288 -> 196;

289 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
181 -> 289 [arrowhead = none ];
289 -> 197;

290 [label="EVAL with clause\nreverse(.(X140, X141), X142, X143) :- reverse(X141, .(X140, X142), X143).\nand substitutionX140 -> T251,\nX141 -> T252,\nT187 -> .(T251, T252),\nT186 -> T253,\nT188 -> T254,\nT189 -> T255,\nT190 -> T256,\nT191 -> T257,\nT192 -> T258,\nX142 -> .(T253, .(T254, .(T255, .(T256, .(T257, .(T258, [])))))),\nX143 -> .(T258, .(T257, .(T256, .(T255, .(T254, .(T253, .(T251, T252)))))))", fontsize=14, style = filled, fillcolor = lightblue];
182 -> 290 [arrowhead = none ];
290 -> 199;

291 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
182 -> 291 [arrowhead = none ];
291 -> 200;

292 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
196 -> 292 [arrowhead = none ];
292 -> 198;

293 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
199 -> 293 [arrowhead = none ];
293 -> 204;

294 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
204 -> 294 [arrowhead = none ];
294 -> 205;

295 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
204 -> 295 [arrowhead = none ];
295 -> 206;

296 [label="EVAL with clause\nreverse([], X150, X150).\nand substitutionT252 -> [],\nT251 -> T307,\nT253 -> T306,\nT254 -> T305,\nT255 -> T304,\nT256 -> T305,\nT257 -> T306,\nT258 -> T307,\nX150 -> .(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, []))))))),\nT301 -> T307,\nT302 -> T306,\nT303 -> T305", fontsize=14, style = filled, fillcolor = lightblue];
205 -> 296 [arrowhead = none ];
296 -> 210;

297 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
205 -> 297 [arrowhead = none ];
297 -> 211;

298 [label="EVAL with clause\nreverse(.(X159, X160), X161, X162) :- reverse(X160, .(X159, X161), X162).\nand substitutionX159 -> T326,\nX160 -> T327,\nT252 -> .(T326, T327),\nT251 -> T328,\nT253 -> T329,\nT254 -> T330,\nT255 -> T331,\nT256 -> T332,\nT257 -> T333,\nT258 -> T334,\nX161 -> .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))),\nX162 -> .(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))", fontsize=14, style = filled, fillcolor = lightblue];
206 -> 298 [arrowhead = none ];
298 -> 215;

299 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
206 -> 299 [arrowhead = none ];
299 -> 216;

300 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
210 -> 300 [arrowhead = none ];
300 -> 212;

301 [label="GENERALIZATION\nT351 <-- .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, [])))))))\nT352 <-- .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))\n\nNew Knowledge:\nT351 is ground\nT352 is ground", fontsize=14, style = filled, fillcolor = violet];
215 -> 301 [arrowhead = none ];
301 -> 218;

302 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
218 -> 302 [arrowhead = none ];
302 -> 219;

303 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
219 -> 303 [arrowhead = none ];
303 -> 220;

304 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
219 -> 304 [arrowhead = none ];
304 -> 221;

305 [label="EVAL with clause\nreverse([], X171, X171).\nand substitutionT327 -> [],\nT326 -> T365,\nT351 -> T366,\nX171 -> .(T365, T366),\nT334 -> T365,\nT352 -> T366", fontsize=14, style = filled, fillcolor = lightblue];
220 -> 305 [arrowhead = none ];
305 -> 223;

306 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
220 -> 306 [arrowhead = none ];
306 -> 224;

307 [label="EVAL with clause\nreverse(.(X180, X181), X182, X183) :- reverse(X181, .(X180, X182), X183).\nand substitutionX180 -> T379,\nX181 -> T380,\nT327 -> .(T379, T380),\nT326 -> T381,\nT351 -> T382,\nX182 -> .(T381, T382),\nT334 -> T383,\nT352 -> T384,\nX183 -> .(T383, T384)", fontsize=14, style = filled, fillcolor = lightblue];
221 -> 307 [arrowhead = none ];
307 -> 231;

308 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
221 -> 308 [arrowhead = none ];
308 -> 232;

309 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
223 -> 309 [arrowhead = none ];
309 -> 226;

310 [label="INSTANCE with matching:\nT327 -> T380\nT326 -> T379\nT351 -> .(T381, T382)\nT334 -> T383\nT352 -> T384", fontsize=14, style = filled, fillcolor = lightgrey];
231 -> 310 [arrowhead = none , style=dashed];
310 -> 218[style=dashed];

}

(2) Obligation:

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

palindromeA_in_g([]) → palindromeA_out_g([])
palindromeA_in_g(.(T19, [])) → palindromeA_out_g(.(T19, []))
palindromeA_in_g(.(T42, .(T42, []))) → palindromeA_out_g(.(T42, .(T42, [])))
palindromeA_in_g(.(T75, .(T74, .(T75, [])))) → palindromeA_out_g(.(T75, .(T74, .(T75, []))))
palindromeA_in_g(.(T118, .(T117, .(T117, .(T118, []))))) → palindromeA_out_g(.(T118, .(T117, .(T117, .(T118, [])))))
palindromeA_in_g(.(T171, .(T170, .(T169, .(T170, .(T171, [])))))) → palindromeA_out_g(.(T171, .(T170, .(T169, .(T170, .(T171, []))))))
palindromeA_in_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, []))))))) → palindromeA_out_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, [])))))))
palindromeA_in_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, [])))))))) → palindromeA_out_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, []))))))))
palindromeA_in_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → U1_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverseB_in_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))
reverseB_in_ggggg([], T365, T366, T365, T366) → reverseB_out_ggggg([], T365, T366, T365, T366)
reverseB_in_ggggg(.(T379, T380), T381, T382, T383, T384) → U2_ggggg(T379, T380, T381, T382, T383, T384, reverseB_in_ggggg(T380, T379, .(T381, T382), T383, T384))
U2_ggggg(T379, T380, T381, T382, T383, T384, reverseB_out_ggggg(T380, T379, .(T381, T382), T383, T384)) → reverseB_out_ggggg(.(T379, T380), T381, T382, T383, T384)
U1_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverseB_out_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → palindromeA_out_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))

Pi is empty.

(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:

PALINDROMEA_IN_G(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → U1_G(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverseB_in_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))
PALINDROMEA_IN_G(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → REVERSEB_IN_GGGGG(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))
REVERSEB_IN_GGGGG(.(T379, T380), T381, T382, T383, T384) → U2_GGGGG(T379, T380, T381, T382, T383, T384, reverseB_in_ggggg(T380, T379, .(T381, T382), T383, T384))
REVERSEB_IN_GGGGG(.(T379, T380), T381, T382, T383, T384) → REVERSEB_IN_GGGGG(T380, T379, .(T381, T382), T383, T384)

The TRS R consists of the following rules:

palindromeA_in_g([]) → palindromeA_out_g([])
palindromeA_in_g(.(T19, [])) → palindromeA_out_g(.(T19, []))
palindromeA_in_g(.(T42, .(T42, []))) → palindromeA_out_g(.(T42, .(T42, [])))
palindromeA_in_g(.(T75, .(T74, .(T75, [])))) → palindromeA_out_g(.(T75, .(T74, .(T75, []))))
palindromeA_in_g(.(T118, .(T117, .(T117, .(T118, []))))) → palindromeA_out_g(.(T118, .(T117, .(T117, .(T118, [])))))
palindromeA_in_g(.(T171, .(T170, .(T169, .(T170, .(T171, [])))))) → palindromeA_out_g(.(T171, .(T170, .(T169, .(T170, .(T171, []))))))
palindromeA_in_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, []))))))) → palindromeA_out_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, [])))))))
palindromeA_in_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, [])))))))) → palindromeA_out_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, []))))))))
palindromeA_in_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → U1_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverseB_in_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))
reverseB_in_ggggg([], T365, T366, T365, T366) → reverseB_out_ggggg([], T365, T366, T365, T366)
reverseB_in_ggggg(.(T379, T380), T381, T382, T383, T384) → U2_ggggg(T379, T380, T381, T382, T383, T384, reverseB_in_ggggg(T380, T379, .(T381, T382), T383, T384))
U2_ggggg(T379, T380, T381, T382, T383, T384, reverseB_out_ggggg(T380, T379, .(T381, T382), T383, T384)) → reverseB_out_ggggg(.(T379, T380), T381, T382, T383, T384)
U1_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverseB_out_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → palindromeA_out_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))

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

(4) Obligation:

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

PALINDROMEA_IN_G(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → U1_G(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverseB_in_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))
PALINDROMEA_IN_G(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → REVERSEB_IN_GGGGG(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))
REVERSEB_IN_GGGGG(.(T379, T380), T381, T382, T383, T384) → U2_GGGGG(T379, T380, T381, T382, T383, T384, reverseB_in_ggggg(T380, T379, .(T381, T382), T383, T384))
REVERSEB_IN_GGGGG(.(T379, T380), T381, T382, T383, T384) → REVERSEB_IN_GGGGG(T380, T379, .(T381, T382), T383, T384)

The TRS R consists of the following rules:

palindromeA_in_g([]) → palindromeA_out_g([])
palindromeA_in_g(.(T19, [])) → palindromeA_out_g(.(T19, []))
palindromeA_in_g(.(T42, .(T42, []))) → palindromeA_out_g(.(T42, .(T42, [])))
palindromeA_in_g(.(T75, .(T74, .(T75, [])))) → palindromeA_out_g(.(T75, .(T74, .(T75, []))))
palindromeA_in_g(.(T118, .(T117, .(T117, .(T118, []))))) → palindromeA_out_g(.(T118, .(T117, .(T117, .(T118, [])))))
palindromeA_in_g(.(T171, .(T170, .(T169, .(T170, .(T171, [])))))) → palindromeA_out_g(.(T171, .(T170, .(T169, .(T170, .(T171, []))))))
palindromeA_in_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, []))))))) → palindromeA_out_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, [])))))))
palindromeA_in_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, [])))))))) → palindromeA_out_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, []))))))))
palindromeA_in_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → U1_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverseB_in_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))
reverseB_in_ggggg([], T365, T366, T365, T366) → reverseB_out_ggggg([], T365, T366, T365, T366)
reverseB_in_ggggg(.(T379, T380), T381, T382, T383, T384) → U2_ggggg(T379, T380, T381, T382, T383, T384, reverseB_in_ggggg(T380, T379, .(T381, T382), T383, T384))
U2_ggggg(T379, T380, T381, T382, T383, T384, reverseB_out_ggggg(T380, T379, .(T381, T382), T383, T384)) → reverseB_out_ggggg(.(T379, T380), T381, T382, T383, T384)
U1_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverseB_out_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → palindromeA_out_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 3 less nodes.

(6) Obligation:

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

REVERSEB_IN_GGGGG(.(T379, T380), T381, T382, T383, T384) → REVERSEB_IN_GGGGG(T380, T379, .(T381, T382), T383, T384)

The TRS R consists of the following rules:

palindromeA_in_g([]) → palindromeA_out_g([])
palindromeA_in_g(.(T19, [])) → palindromeA_out_g(.(T19, []))
palindromeA_in_g(.(T42, .(T42, []))) → palindromeA_out_g(.(T42, .(T42, [])))
palindromeA_in_g(.(T75, .(T74, .(T75, [])))) → palindromeA_out_g(.(T75, .(T74, .(T75, []))))
palindromeA_in_g(.(T118, .(T117, .(T117, .(T118, []))))) → palindromeA_out_g(.(T118, .(T117, .(T117, .(T118, [])))))
palindromeA_in_g(.(T171, .(T170, .(T169, .(T170, .(T171, [])))))) → palindromeA_out_g(.(T171, .(T170, .(T169, .(T170, .(T171, []))))))
palindromeA_in_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, []))))))) → palindromeA_out_g(.(T234, .(T233, .(T232, .(T232, .(T233, .(T234, [])))))))
palindromeA_in_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, [])))))))) → palindromeA_out_g(.(T307, .(T306, .(T305, .(T304, .(T305, .(T306, .(T307, []))))))))
palindromeA_in_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → U1_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverseB_in_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))
reverseB_in_ggggg([], T365, T366, T365, T366) → reverseB_out_ggggg([], T365, T366, T365, T366)
reverseB_in_ggggg(.(T379, T380), T381, T382, T383, T384) → U2_ggggg(T379, T380, T381, T382, T383, T384, reverseB_in_ggggg(T380, T379, .(T381, T382), T383, T384))
U2_ggggg(T379, T380, T381, T382, T383, T384, reverseB_out_ggggg(T380, T379, .(T381, T382), T383, T384)) → reverseB_out_ggggg(.(T379, T380), T381, T382, T383, T384)
U1_g(T334, T333, T332, T331, T330, T329, T328, T326, T327, reverseB_out_ggggg(T327, T326, .(T328, .(T329, .(T330, .(T331, .(T332, .(T333, .(T334, []))))))), T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327))))))))) → palindromeA_out_g(.(T334, .(T333, .(T332, .(T331, .(T330, .(T329, .(T328, .(T326, T327)))))))))

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

(7) UsableRulesProof (EQUIVALENT transformation)

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

(8) Obligation:

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

REVERSEB_IN_GGGGG(.(T379, T380), T381, T382, T383, T384) → REVERSEB_IN_GGGGG(T380, T379, .(T381, T382), T383, T384)

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

(9) PiDPToQDPProof (EQUIVALENT transformation)

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

(10) Obligation:

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

REVERSEB_IN_GGGGG(.(T379, T380), T381, T382, T383, T384) → REVERSEB_IN_GGGGG(T380, T379, .(T381, T382), T383, T384)

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

(11) 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:

• REVERSEB_IN_GGGGG(.(T379, T380), T381, T382, T383, T384) → REVERSEB_IN_GGGGG(T380, T379, .(T381, T382), T383, T384)
  The graph contains the following edges 1 > 1, 1 > 2, 4 >= 4, 5 >= 5

(12) YES