Left Termination proof of /tmp/tmpDiEOw6/palindrome.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 214 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 272 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 27 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇒, 32 ms)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔, 0 ms)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇒, 0 ms)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔, 0 ms)

        ↳20 YES

    ↳21 PiDP

        ↳22 UsableRulesProof (⇔, 0 ms)

        ↳23 PiDP

        ↳24 PiDPToQDPProof (⇒, 0 ms)

        ↳25 QDP

        ↳26 QDPOrderProof (⇔, 74 ms)

        ↳27 QDP

        ↳28 DependencyGraphProof (⇔, 0 ms)

        ↳29 TRUE

(0) Obligation:

Clauses:

palindrome(L) :- ','(halves(L, X1s, X2s, EvenOdd), ','(eq(EvenOdd, even), eq(X1s, X2s))).
palindrome(L) :- ','(halves(L, X1s, X2s, EvenOdd), ','(eq(EvenOdd, odd), last(X1s, X1, X2s))).
halves([], [], [], even).
halves(.(X, []), .(X, []), [], odd).
halves(.(T, .(Y, Xs)), .(T, Ts), .(R, Rs), EvenOdd) :- ','(last(.(Y, Xs), R, Rests), halves(Rests, Ts, Rs, EvenOdd)).
last(.(T, []), T, []).
last(.(H, T), X, .(H, M)) :- last(T, X, M).
eq(X, X).

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 | palindrome(T1), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(halves(T3, X4, X5, X6), ','(eq(X6, even), eq(X4, X5))) | palindrome(T3), SCOPE: 1, CLAUSE: 1\n\nT3 is ground\nX4 is free\nX5 is free\nX6 is free", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(halves(T3, X4, X5, X6), ','(eq(X6, even), eq(X4, X5))), SCOPE: 2, CLAUSE: 2 | ','(halves(T3, X4, X5, X6), ','(eq(X6, even), eq(X4, X5))), SCOPE: 2, CLAUSE: 3 | ','(halves(T3, X4, X5, X6), ','(eq(X6, even), eq(X4, X5))), SCOPE: 2, CLAUSE: 4 | ?_2 | palindrome(T3), SCOPE: 1, CLAUSE: 1\n\nT3 is ground\nX4 is free\nX5 is free\nX6 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(halves(T3, X4, X5, X6), ','(eq(X6, even), eq(X4, X5))), SCOPE: 2, CLAUSE: 2\n\nT3 is ground\nX4 is free\nX5 is free\nX6 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(halves(T3, X4, X5, X6), ','(eq(X6, even), eq(X4, X5))), SCOPE: 2, CLAUSE: 3 | ','(halves(T3, X4, X5, X6), ','(eq(X6, even), eq(X4, X5))), SCOPE: 2, CLAUSE: 4 | ?_2 | palindrome(T3), SCOPE: 1, CLAUSE: 1\n\nT3 is ground\nX4 is free\nX5 is free\nX6 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(eq(even, even), eq([], []))\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(eq(even, even), eq([], [])), SCOPE: 3, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: eq([], [])\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: eq([], []), SCOPE: 4, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(halves(T3, X4, X5, X6), ','(eq(X6, even), eq(X4, X5))), SCOPE: 2, CLAUSE: 3\n\nT3 is ground\nX4 is free\nX5 is free\nX6 is free", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(halves(T3, X4, X5, X6), ','(eq(X6, even), eq(X4, X5))), SCOPE: 2, CLAUSE: 4 | ?_2 | palindrome(T3), SCOPE: 1, CLAUSE: 1\n\nT3 is ground\nX4 is free\nX5 is free\nX6 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: ','(eq(odd, even), eq(.(T8, []), []))\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(eq(odd, even), eq(.(T8, []), [])), SCOPE: 5, CLAUSE: 7\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(halves(T3, X4, X5, X6), ','(eq(X6, even), eq(X4, X5))), SCOPE: 2, CLAUSE: 4\n\nT3 is ground\nX4 is free\nX5 is free\nX6 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ?_2 | palindrome(T3), SCOPE: 1, CLAUSE: 1\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="B: ','(','(last(.(T22, T23), X74, X72), halves(X72, X73, X75, X76)), ','(eq(X76, even), eq(.(T21, X73), .(X74, X75))))\n\nT21 is ground\nT22 is ground\nT23 is ground\nX73 is free\nX74 is free\nX75 is free\nX76 is free\nX72 is free", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="E: last(.(T22, T23), X74, X72)\n\nT22 is ground\nT23 is ground\nX74 is free\nX72 is free", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="K: ','(halves(T27, X73, X75, X76), ','(eq(X76, even), eq(.(T21, X73), .(T26, X75))))\n\nT21 is ground\nT26 is ground\nT27 is ground\nX73 is free\nX75 is free\nX76 is free", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: last(.(T22, T23), X74, X72), SCOPE: 6, CLAUSE: 5 | last(.(T22, T23), X74, X72), SCOPE: 6, CLAUSE: 6\n\nT22 is ground\nT23 is ground\nX74 is free\nX72 is free", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: last(.(T22, T23), X74, X72), SCOPE: 6, CLAUSE: 5\n\nT22 is ground\nT23 is ground\nX74 is free\nX72 is free", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: last(.(T22, T23), X74, X72), SCOPE: 6, CLAUSE: 6\n\nT22 is ground\nT23 is ground\nX74 is free\nX72 is free", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="D: last(T42, X104, X105)\n\nT42 is ground\nX104 is free\nX105 is free", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: last(T42, X104, X105), SCOPE: 7, CLAUSE: 5 | last(T42, X104, X105), SCOPE: 7, CLAUSE: 6\n\nT42 is ground\nX104 is free\nX105 is free", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: last(T42, X104, X105), SCOPE: 7, CLAUSE: 5\n\nT42 is ground\nX104 is free\nX105 is free", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: last(T42, X104, X105), SCOPE: 7, CLAUSE: 6\n\nT42 is ground\nX104 is free\nX105 is free", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: last(T55, X129, X130)\n\nT55 is ground\nX129 is free\nX130 is free", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="F: halves(T27, X73, X75, X76)\n\nT27 is ground\nX73 is free\nX75 is free\nX76 is free", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="I: ','(eq(T60, even), eq(.(T21, T58), .(T26, T59)))\n\nT21 is ground\nT26 is ground\nT58 is ground\nT59 is ground\nT60 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: halves(T27, X73, X75, X76), SCOPE: 8, CLAUSE: 2 | halves(T27, X73, X75, X76), SCOPE: 8, CLAUSE: 3 | halves(T27, X73, X75, X76), SCOPE: 8, CLAUSE: 4\n\nT27 is ground\nX73 is free\nX75 is free\nX76 is free", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: halves(T27, X73, X75, X76), SCOPE: 8, CLAUSE: 2\n\nT27 is ground\nX73 is free\nX75 is free\nX76 is free", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: halves(T27, X73, X75, X76), SCOPE: 8, CLAUSE: 3 | halves(T27, X73, X75, X76), SCOPE: 8, CLAUSE: 4\n\nT27 is ground\nX73 is free\nX75 is free\nX76 is free", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: halves(T27, X73, X75, X76), SCOPE: 8, CLAUSE: 3\n\nT27 is ground\nX73 is free\nX75 is free\nX76 is free", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: halves(T27, X73, X75, X76), SCOPE: 8, CLAUSE: 4\n\nT27 is ground\nX73 is free\nX75 is free\nX76 is free", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="G: ','(last(.(T73, T74), X170, X168), halves(X168, X169, X171, X172))\n\nT73 is ground\nT74 is ground\nX169 is free\nX170 is free\nX171 is free\nX172 is free\nX168 is free", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: last(.(T73, T74), X170, X168)\n\nT73 is ground\nT74 is ground\nX170 is free\nX168 is free", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: halves(T78, X169, X171, X172)\n\nT78 is ground\nX169 is free\nX171 is free\nX172 is free", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: ','(eq(T60, even), eq(.(T21, T58), .(T26, T59))), SCOPE: 9, CLAUSE: 7\n\nT21 is ground\nT26 is ground\nT58 is ground\nT59 is ground\nT60 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: eq(.(T21, T58), .(T26, T59))\n\nT21 is ground\nT26 is ground\nT58 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: eq(.(T21, T58), .(T26, T59)), SCOPE: 10, CLAUSE: 7\n\nT21 is ground\nT26 is ground\nT58 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: palindrome(T3), SCOPE: 1, CLAUSE: 1\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="C: ','(halves(T92, X190, X191, X192), ','(eq(X192, odd), last(X190, X193, X191)))\n\nT92 is ground\nX190 is free\nX191 is free\nX192 is free\nX193 is free", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: halves(T92, X190, X191, X192)\n\nT92 is ground\nX190 is free\nX191 is free\nX192 is free", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="J: ','(eq(T95, odd), last(T93, X193, T94))\n\nT93 is ground\nT94 is ground\nT95 is ground\nX193 is free", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: ','(eq(T95, odd), last(T93, X193, T94)), SCOPE: 11, CLAUSE: 7\n\nT93 is ground\nT94 is ground\nT95 is ground\nX193 is free", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="H: last(T93, X193, T94)\n\nT93 is ground\nT94 is ground\nX193 is free", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: last(T93, X193, T94), SCOPE: 12, CLAUSE: 5 | last(T93, X193, T94), SCOPE: 12, CLAUSE: 6\n\nT93 is ground\nT94 is ground\nX193 is free", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: last(T93, X193, T94), SCOPE: 12, CLAUSE: 5\n\nT93 is ground\nT94 is ground\nX193 is free", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: last(T93, X193, T94), SCOPE: 12, CLAUSE: 6\n\nT93 is ground\nT94 is ground\nX193 is free", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: last(T115, X220, T116)\n\nT115 is ground\nT116 is ground\nX220 is free", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 217 [arrowhead = none ];
217 -> 4;

218 [label="ONLY EVAL with clause\npalindrome(X3) :- ','(halves(X3, X4, X5, X6), ','(eq(X6, even), eq(X4, X5))).\nand substitutionT1 -> T3,\nX3 -> T3", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 218 [arrowhead = none ];
218 -> 7;

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

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

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

222 [label="EVAL with clause\nhalves([], [], [], even).\nand substitutionT3 -> [],\nX4 -> [],\nX5 -> [],\nX6 -> even", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 222 [arrowhead = none ];
222 -> 18;

223 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
13 -> 223 [arrowhead = none ];
223 -> 20;

224 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
15 -> 224 [arrowhead = none ];
224 -> 34;

225 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
15 -> 225 [arrowhead = none ];
225 -> 36;

226 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
18 -> 226 [arrowhead = none ];
226 -> 23;

227 [label="ONLY EVAL with clause\neq(X9, X9).\nand substitutionX9 -> even", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 227 [arrowhead = none ];
227 -> 24;

228 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
24 -> 228 [arrowhead = none ];
228 -> 25;

229 [label="ONLY EVAL with clause\neq(X12, X12).\nand substitutionX12 -> []", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 229 [arrowhead = none ];
229 -> 28;

230 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
28 -> 230 [arrowhead = none ];
230 -> 29;

231 [label="EVAL with clause\nhalves(.(X17, []), .(X17, []), [], odd).\nand substitutionX17 -> T8,\nT3 -> .(T8, []),\nX4 -> .(T8, []),\nX5 -> [],\nX6 -> odd", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 231 [arrowhead = none ];
231 -> 47;

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

233 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
36 -> 233 [arrowhead = none ];
233 -> 59;

234 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
36 -> 234 [arrowhead = none ];
234 -> 60;

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

236 [label="BACKTRACK\nfor clause: eq(X, X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
50 -> 236 [arrowhead = none ];
236 -> 52;

237 [label="EVAL with clause\nhalves(.(X65, .(X66, X67)), .(X65, X68), .(X69, X70), X71) :- ','(last(.(X66, X67), X69, X72), halves(X72, X68, X70, X71)).\nand substitutionX65 -> T21,\nX66 -> T22,\nX67 -> T23,\nT3 -> .(T21, .(T22, T23)),\nX68 -> X73,\nX4 -> .(T21, X73),\nX69 -> X74,\nX70 -> X75,\nX5 -> .(X74, X75),\nX6 -> X76,\nX71 -> X76", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 237 [arrowhead = none ];
237 -> 97;

238 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 238 [arrowhead = none ];
238 -> 98;

239 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
60 -> 239 [arrowhead = none ];
239 -> 200;

240 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
97 -> 240 [arrowhead = none ];
240 -> 101;

241 [label="SPLIT 2\nnew knowledge:\nT22 is ground\nT23 is ground\nT26 is ground\nT27 is ground\nreplacements:X74 -> T26,\nX72 -> T27", fontsize=14, style = filled, fillcolor = violet];
97 -> 241 [arrowhead = none ];
241 -> 102;

242 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
101 -> 242 [arrowhead = none ];
242 -> 121;

243 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
102 -> 243 [arrowhead = none ];
243 -> 164;

244 [label="SPLIT 2\nnew knowledge:\nT27 is ground\nT58 is ground\nT59 is ground\nT60 is ground\nreplacements:X73 -> T58,\nX75 -> T59,\nX76 -> T60", fontsize=14, style = filled, fillcolor = violet];
102 -> 244 [arrowhead = none ];
244 -> 165;

245 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
121 -> 245 [arrowhead = none ];
245 -> 123;

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

247 [label="EVAL with clause\nlast(.(X85, []), X85, []).\nand substitutionT22 -> T34,\nX85 -> T34,\nT23 -> [],\nX74 -> T34,\nX72 -> []", fontsize=14, style = filled, fillcolor = lightblue];
123 -> 247 [arrowhead = none ];
247 -> 127;

248 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
123 -> 248 [arrowhead = none ];
248 -> 128;

249 [label="ONLY EVAL with clause\nlast(.(X100, X101), X102, .(X100, X103)) :- last(X101, X102, X103).\nand substitutionT22 -> T41,\nX100 -> T41,\nT23 -> T42,\nX101 -> T42,\nX74 -> X104,\nX102 -> X104,\nX103 -> X105,\nX72 -> .(T41, X105)", fontsize=14, style = filled, fillcolor = lightblue];
124 -> 249 [arrowhead = none ];
249 -> 135;

250 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
127 -> 250 [arrowhead = none ];
250 -> 129;

251 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
135 -> 251 [arrowhead = none ];
251 -> 137;

252 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
137 -> 252 [arrowhead = none ];
252 -> 138;

253 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
137 -> 253 [arrowhead = none ];
253 -> 139;

254 [label="EVAL with clause\nlast(.(X112, []), X112, []).\nand substitutionX112 -> T49,\nT42 -> .(T49, []),\nX104 -> T49,\nX105 -> []", fontsize=14, style = filled, fillcolor = lightblue];
138 -> 254 [arrowhead = none ];
254 -> 148;

255 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
138 -> 255 [arrowhead = none ];
255 -> 149;

256 [label="EVAL with clause\nlast(.(X125, X126), X127, .(X125, X128)) :- last(X126, X127, X128).\nand substitutionX125 -> T54,\nX126 -> T55,\nT42 -> .(T54, T55),\nX104 -> X129,\nX127 -> X129,\nX128 -> X130,\nX105 -> .(T54, X130)", fontsize=14, style = filled, fillcolor = lightblue];
139 -> 256 [arrowhead = none ];
256 -> 154;

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

258 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
148 -> 258 [arrowhead = none ];
258 -> 150;

259 [label="INSTANCE with matching:\nT42 -> T55\nX104 -> X129\nX105 -> X130", fontsize=14, style = filled, fillcolor = lightgrey];
154 -> 259 [arrowhead = none , style=dashed];
259 -> 135[style=dashed];

260 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
164 -> 260 [arrowhead = none ];
260 -> 166;

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

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

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

264 [label="EVAL with clause\nhalves([], [], [], even).\nand substitutionT27 -> [],\nX73 -> [],\nX75 -> [],\nX76 -> even", fontsize=14, style = filled, fillcolor = lightblue];
167 -> 264 [arrowhead = none ];
264 -> 169;

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

266 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
168 -> 266 [arrowhead = none ];
266 -> 172;

267 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
168 -> 267 [arrowhead = none ];
267 -> 173;

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

269 [label="EVAL with clause\nhalves(.(X137, []), .(X137, []), [], odd).\nand substitutionX137 -> T65,\nT27 -> .(T65, []),\nX73 -> .(T65, []),\nX75 -> [],\nX76 -> odd", fontsize=14, style = filled, fillcolor = lightblue];
172 -> 269 [arrowhead = none ];
269 -> 174;

270 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
172 -> 270 [arrowhead = none ];
270 -> 175;

271 [label="EVAL with clause\nhalves(.(X161, .(X162, X163)), .(X161, X164), .(X165, X166), X167) :- ','(last(.(X162, X163), X165, X168), halves(X168, X164, X166, X167)).\nand substitutionX161 -> T72,\nX162 -> T73,\nX163 -> T74,\nT27 -> .(T72, .(T73, T74)),\nX164 -> X169,\nX73 -> .(T72, X169),\nX165 -> X170,\nX166 -> X171,\nX75 -> .(X170, X171),\nX76 -> X172,\nX167 -> X172", fontsize=14, style = filled, fillcolor = lightblue];
173 -> 271 [arrowhead = none ];
271 -> 180;

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

273 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
174 -> 273 [arrowhead = none ];
273 -> 176;

274 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
180 -> 274 [arrowhead = none ];
274 -> 182;

275 [label="SPLIT 2\nnew knowledge:\nT73 is ground\nT74 is ground\nT77 is ground\nT78 is ground\nreplacements:X170 -> T77,\nX168 -> T78", fontsize=14, style = filled, fillcolor = violet];
180 -> 275 [arrowhead = none ];
275 -> 183;

276 [label="INSTANCE with matching:\nT22 -> T73\nT23 -> T74\nX74 -> X170\nX72 -> X168", fontsize=14, style = filled, fillcolor = lightgrey];
182 -> 276 [arrowhead = none , style=dashed];
276 -> 101[style=dashed];

277 [label="INSTANCE with matching:\nT27 -> T78\nX73 -> X169\nX75 -> X171\nX76 -> X172", fontsize=14, style = filled, fillcolor = lightgrey];
183 -> 277 [arrowhead = none , style=dashed];
277 -> 164[style=dashed];

278 [label="EVAL with clause\neq(X179, X179).\nand substitutionT60 -> even,\nX179 -> even,\nT83 -> even", fontsize=14, style = filled, fillcolor = lightblue];
193 -> 278 [arrowhead = none ];
278 -> 194;

279 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
193 -> 279 [arrowhead = none ];
279 -> 195;

280 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
194 -> 280 [arrowhead = none ];
280 -> 196;

281 [label="EVAL with clause\neq(X182, X182).\nand substitutionT21 -> T88,\nT58 -> T89,\nX182 -> .(T88, T89),\nT26 -> T88,\nT59 -> T89", fontsize=14, style = filled, fillcolor = lightblue];
196 -> 281 [arrowhead = none ];
281 -> 197;

282 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
196 -> 282 [arrowhead = none ];
282 -> 198;

283 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
197 -> 283 [arrowhead = none ];
283 -> 199;

284 [label="ONLY EVAL with clause\npalindrome(X189) :- ','(halves(X189, X190, X191, X192), ','(eq(X192, odd), last(X190, X193, X191))).\nand substitutionT3 -> T92,\nX189 -> T92", fontsize=14, style = filled, fillcolor = lightblue];
200 -> 284 [arrowhead = none ];
284 -> 201;

285 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
201 -> 285 [arrowhead = none ];
285 -> 204;

286 [label="SPLIT 2\nnew knowledge:\nT92 is ground\nT93 is ground\nT94 is ground\nT95 is ground\nreplacements:X190 -> T93,\nX191 -> T94,\nX192 -> T95", fontsize=14, style = filled, fillcolor = violet];
201 -> 286 [arrowhead = none ];
286 -> 205;

287 [label="INSTANCE with matching:\nT27 -> T92\nX73 -> X190\nX75 -> X191\nX76 -> X192", fontsize=14, style = filled, fillcolor = lightgrey];
204 -> 287 [arrowhead = none , style=dashed];
287 -> 164[style=dashed];

288 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
205 -> 288 [arrowhead = none ];
288 -> 206;

289 [label="EVAL with clause\neq(X198, X198).\nand substitutionT95 -> odd,\nX198 -> odd,\nT100 -> odd", fontsize=14, style = filled, fillcolor = lightblue];
206 -> 289 [arrowhead = none ];
289 -> 207;

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

291 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
207 -> 291 [arrowhead = none ];
291 -> 209;

292 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
209 -> 292 [arrowhead = none ];
292 -> 210;

293 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
209 -> 293 [arrowhead = none ];
293 -> 211;

294 [label="EVAL with clause\nlast(.(X205, []), X205, []).\nand substitutionX205 -> T107,\nT93 -> .(T107, []),\nX193 -> T107,\nT94 -> []", fontsize=14, style = filled, fillcolor = lightblue];
210 -> 294 [arrowhead = none ];
294 -> 212;

295 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
210 -> 295 [arrowhead = none ];
295 -> 213;

296 [label="EVAL with clause\nlast(.(X216, X217), X218, .(X216, X219)) :- last(X217, X218, X219).\nand substitutionX216 -> T114,\nX217 -> T115,\nT93 -> .(T114, T115),\nX193 -> X220,\nX218 -> X220,\nX219 -> T116,\nT94 -> .(T114, T116)", fontsize=14, style = filled, fillcolor = lightblue];
211 -> 296 [arrowhead = none ];
296 -> 215;

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

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

299 [label="INSTANCE with matching:\nT93 -> T115\nX193 -> X220\nT94 -> T116", fontsize=14, style = filled, fillcolor = lightgrey];
215 -> 299 [arrowhead = none , style=dashed];
299 -> 207[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(.(T21, .(T22, T23))) → U1_g(T21, T22, T23, pB_in_ggaaaaag(T22, T23, X74, X72, X73, X75, X76, T21))
pB_in_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21) → U8_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21, lastE_in_ggaa(T22, T23, T26, T27))
lastE_in_ggaa(T34, [], T34, []) → lastE_out_ggaa(T34, [], T34, [])
lastE_in_ggaa(T41, T42, X104, .(T41, X105)) → U4_ggaa(T41, T42, X104, X105, lastD_in_gaa(T42, X104, X105))
lastD_in_gaa(.(T49, []), T49, []) → lastD_out_gaa(.(T49, []), T49, [])
lastD_in_gaa(.(T54, T55), X129, .(T54, X130)) → U3_gaa(T54, T55, X129, X130, lastD_in_gaa(T55, X129, X130))
U3_gaa(T54, T55, X129, X130, lastD_out_gaa(T55, X129, X130)) → lastD_out_gaa(.(T54, T55), X129, .(T54, X130))
U4_ggaa(T41, T42, X104, X105, lastD_out_gaa(T42, X104, X105)) → lastE_out_ggaa(T41, T42, X104, .(T41, X105))
U8_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21, lastE_out_ggaa(T22, T23, T26, T27)) → U9_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21, pK_in_gaaagg(T27, X73, X75, X76, T21, T26))
pK_in_gaaagg(T27, T58, T59, T60, T21, T26) → U10_gaaagg(T27, T58, T59, T60, T21, T26, halvesF_in_gaaa(T27, T58, T59, T60))
halvesF_in_gaaa([], [], [], even) → halvesF_out_gaaa([], [], [], even)
halvesF_in_gaaa(.(T65, []), .(T65, []), [], odd) → halvesF_out_gaaa(.(T65, []), .(T65, []), [], odd)
halvesF_in_gaaa(.(T72, .(T73, T74)), .(T72, X169), .(X170, X171), X172) → U5_gaaa(T72, T73, T74, X169, X170, X171, X172, pG_in_ggaaaaa(T73, T74, X170, X168, X169, X171, X172))
pG_in_ggaaaaa(T73, T74, T77, T78, X169, X171, X172) → U12_ggaaaaa(T73, T74, T77, T78, X169, X171, X172, lastE_in_ggaa(T73, T74, T77, T78))
U12_ggaaaaa(T73, T74, T77, T78, X169, X171, X172, lastE_out_ggaa(T73, T74, T77, T78)) → U13_ggaaaaa(T73, T74, T77, T78, X169, X171, X172, halvesF_in_gaaa(T78, X169, X171, X172))
U13_ggaaaaa(T73, T74, T77, T78, X169, X171, X172, halvesF_out_gaaa(T78, X169, X171, X172)) → pG_out_ggaaaaa(T73, T74, T77, T78, X169, X171, X172)
U5_gaaa(T72, T73, T74, X169, X170, X171, X172, pG_out_ggaaaaa(T73, T74, X170, X168, X169, X171, X172)) → halvesF_out_gaaa(.(T72, .(T73, T74)), .(T72, X169), .(X170, X171), X172)
U10_gaaagg(T27, T58, T59, T60, T21, T26, halvesF_out_gaaa(T27, T58, T59, T60)) → U11_gaaagg(T27, T58, T59, T60, T21, T26, pI_in_ggggg(T60, T21, T58, T26, T59))
pI_in_ggggg(even, T88, T89, T88, T89) → pI_out_ggggg(even, T88, T89, T88, T89)
U11_gaaagg(T27, T58, T59, T60, T21, T26, pI_out_ggggg(T60, T21, T58, T26, T59)) → pK_out_gaaagg(T27, T58, T59, T60, T21, T26)
U9_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21, pK_out_gaaagg(T27, X73, X75, X76, T21, T26)) → pB_out_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21)
U1_g(T21, T22, T23, pB_out_ggaaaaag(T22, T23, X74, X72, X73, X75, X76, T21)) → palindromeA_out_g(.(T21, .(T22, T23)))
palindromeA_in_g(T92) → U2_g(T92, pC_in_gaaaa(T92, X190, X191, X192, X193))
pC_in_gaaaa(T92, T93, T94, T95, X193) → U14_gaaaa(T92, T93, T94, T95, X193, halvesF_in_gaaa(T92, T93, T94, T95))
U14_gaaaa(T92, T93, T94, T95, X193, halvesF_out_gaaa(T92, T93, T94, T95)) → U15_gaaaa(T92, T93, T94, T95, X193, pJ_in_ggag(T95, T93, X193, T94))
pJ_in_ggag(odd, T93, X193, T94) → U7_ggag(T93, X193, T94, lastH_in_gag(T93, X193, T94))
lastH_in_gag(.(T107, []), T107, []) → lastH_out_gag(.(T107, []), T107, [])
lastH_in_gag(.(T114, T115), X220, .(T114, T116)) → U6_gag(T114, T115, X220, T116, lastH_in_gag(T115, X220, T116))
U6_gag(T114, T115, X220, T116, lastH_out_gag(T115, X220, T116)) → lastH_out_gag(.(T114, T115), X220, .(T114, T116))
U7_ggag(T93, X193, T94, lastH_out_gag(T93, X193, T94)) → pJ_out_ggag(odd, T93, X193, T94)
U15_gaaaa(T92, T93, T94, T95, X193, pJ_out_ggag(T95, T93, X193, T94)) → pC_out_gaaaa(T92, T93, T94, T95, X193)
U2_g(T92, pC_out_gaaaa(T92, X190, X191, X192, X193)) → palindromeA_out_g(T92)

(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(.(T21, .(T22, T23))) → U1_G(T21, T22, T23, pB_in_ggaaaaag(T22, T23, X74, X72, X73, X75, X76, T21))
PALINDROMEA_IN_G(.(T21, .(T22, T23))) → PB_IN_GGAAAAAG(T22, T23, X74, X72, X73, X75, X76, T21)
PB_IN_GGAAAAAG(T22, T23, T26, T27, X73, X75, X76, T21) → U8_GGAAAAAG(T22, T23, T26, T27, X73, X75, X76, T21, lastE_in_ggaa(T22, T23, T26, T27))
PB_IN_GGAAAAAG(T22, T23, T26, T27, X73, X75, X76, T21) → LASTE_IN_GGAA(T22, T23, T26, T27)
LASTE_IN_GGAA(T41, T42, X104, .(T41, X105)) → U4_GGAA(T41, T42, X104, X105, lastD_in_gaa(T42, X104, X105))
LASTE_IN_GGAA(T41, T42, X104, .(T41, X105)) → LASTD_IN_GAA(T42, X104, X105)
LASTD_IN_GAA(.(T54, T55), X129, .(T54, X130)) → U3_GAA(T54, T55, X129, X130, lastD_in_gaa(T55, X129, X130))
LASTD_IN_GAA(.(T54, T55), X129, .(T54, X130)) → LASTD_IN_GAA(T55, X129, X130)
U8_GGAAAAAG(T22, T23, T26, T27, X73, X75, X76, T21, lastE_out_ggaa(T22, T23, T26, T27)) → U9_GGAAAAAG(T22, T23, T26, T27, X73, X75, X76, T21, pK_in_gaaagg(T27, X73, X75, X76, T21, T26))
U8_GGAAAAAG(T22, T23, T26, T27, X73, X75, X76, T21, lastE_out_ggaa(T22, T23, T26, T27)) → PK_IN_GAAAGG(T27, X73, X75, X76, T21, T26)
PK_IN_GAAAGG(T27, T58, T59, T60, T21, T26) → U10_GAAAGG(T27, T58, T59, T60, T21, T26, halvesF_in_gaaa(T27, T58, T59, T60))
PK_IN_GAAAGG(T27, T58, T59, T60, T21, T26) → HALVESF_IN_GAAA(T27, T58, T59, T60)
HALVESF_IN_GAAA(.(T72, .(T73, T74)), .(T72, X169), .(X170, X171), X172) → U5_GAAA(T72, T73, T74, X169, X170, X171, X172, pG_in_ggaaaaa(T73, T74, X170, X168, X169, X171, X172))
HALVESF_IN_GAAA(.(T72, .(T73, T74)), .(T72, X169), .(X170, X171), X172) → PG_IN_GGAAAAA(T73, T74, X170, X168, X169, X171, X172)
PG_IN_GGAAAAA(T73, T74, T77, T78, X169, X171, X172) → U12_GGAAAAA(T73, T74, T77, T78, X169, X171, X172, lastE_in_ggaa(T73, T74, T77, T78))
PG_IN_GGAAAAA(T73, T74, T77, T78, X169, X171, X172) → LASTE_IN_GGAA(T73, T74, T77, T78)
U12_GGAAAAA(T73, T74, T77, T78, X169, X171, X172, lastE_out_ggaa(T73, T74, T77, T78)) → U13_GGAAAAA(T73, T74, T77, T78, X169, X171, X172, halvesF_in_gaaa(T78, X169, X171, X172))
U12_GGAAAAA(T73, T74, T77, T78, X169, X171, X172, lastE_out_ggaa(T73, T74, T77, T78)) → HALVESF_IN_GAAA(T78, X169, X171, X172)
U10_GAAAGG(T27, T58, T59, T60, T21, T26, halvesF_out_gaaa(T27, T58, T59, T60)) → U11_GAAAGG(T27, T58, T59, T60, T21, T26, pI_in_ggggg(T60, T21, T58, T26, T59))
U10_GAAAGG(T27, T58, T59, T60, T21, T26, halvesF_out_gaaa(T27, T58, T59, T60)) → PI_IN_GGGGG(T60, T21, T58, T26, T59)
PALINDROMEA_IN_G(T92) → U2_G(T92, pC_in_gaaaa(T92, X190, X191, X192, X193))
PALINDROMEA_IN_G(T92) → PC_IN_GAAAA(T92, X190, X191, X192, X193)
PC_IN_GAAAA(T92, T93, T94, T95, X193) → U14_GAAAA(T92, T93, T94, T95, X193, halvesF_in_gaaa(T92, T93, T94, T95))
PC_IN_GAAAA(T92, T93, T94, T95, X193) → HALVESF_IN_GAAA(T92, T93, T94, T95)
U14_GAAAA(T92, T93, T94, T95, X193, halvesF_out_gaaa(T92, T93, T94, T95)) → U15_GAAAA(T92, T93, T94, T95, X193, pJ_in_ggag(T95, T93, X193, T94))
U14_GAAAA(T92, T93, T94, T95, X193, halvesF_out_gaaa(T92, T93, T94, T95)) → PJ_IN_GGAG(T95, T93, X193, T94)
PJ_IN_GGAG(odd, T93, X193, T94) → U7_GGAG(T93, X193, T94, lastH_in_gag(T93, X193, T94))
PJ_IN_GGAG(odd, T93, X193, T94) → LASTH_IN_GAG(T93, X193, T94)
LASTH_IN_GAG(.(T114, T115), X220, .(T114, T116)) → U6_GAG(T114, T115, X220, T116, lastH_in_gag(T115, X220, T116))
LASTH_IN_GAG(.(T114, T115), X220, .(T114, T116)) → LASTH_IN_GAG(T115, X220, T116)

The TRS R consists of the following rules:

palindromeA_in_g([]) → palindromeA_out_g([])
palindromeA_in_g(.(T21, .(T22, T23))) → U1_g(T21, T22, T23, pB_in_ggaaaaag(T22, T23, X74, X72, X73, X75, X76, T21))
pB_in_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21) → U8_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21, lastE_in_ggaa(T22, T23, T26, T27))
lastE_in_ggaa(T34, [], T34, []) → lastE_out_ggaa(T34, [], T34, [])
lastE_in_ggaa(T41, T42, X104, .(T41, X105)) → U4_ggaa(T41, T42, X104, X105, lastD_in_gaa(T42, X104, X105))
lastD_in_gaa(.(T49, []), T49, []) → lastD_out_gaa(.(T49, []), T49, [])
lastD_in_gaa(.(T54, T55), X129, .(T54, X130)) → U3_gaa(T54, T55, X129, X130, lastD_in_gaa(T55, X129, X130))
U3_gaa(T54, T55, X129, X130, lastD_out_gaa(T55, X129, X130)) → lastD_out_gaa(.(T54, T55), X129, .(T54, X130))
U4_ggaa(T41, T42, X104, X105, lastD_out_gaa(T42, X104, X105)) → lastE_out_ggaa(T41, T42, X104, .(T41, X105))
U8_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21, lastE_out_ggaa(T22, T23, T26, T27)) → U9_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21, pK_in_gaaagg(T27, X73, X75, X76, T21, T26))
pK_in_gaaagg(T27, T58, T59, T60, T21, T26) → U10_gaaagg(T27, T58, T59, T60, T21, T26, halvesF_in_gaaa(T27, T58, T59, T60))
halvesF_in_gaaa([], [], [], even) → halvesF_out_gaaa([], [], [], even)
halvesF_in_gaaa(.(T65, []), .(T65, []), [], odd) → halvesF_out_gaaa(.(T65, []), .(T65, []), [], odd)
halvesF_in_gaaa(.(T72, .(T73, T74)), .(T72, X169), .(X170, X171), X172) → U5_gaaa(T72, T73, T74, X169, X170, X171, X172, pG_in_ggaaaaa(T73, T74, X170, X168, X169, X171, X172))
pG_in_ggaaaaa(T73, T74, T77, T78, X169, X171, X172) → U12_ggaaaaa(T73, T74, T77, T78, X169, X171, X172, lastE_in_ggaa(T73, T74, T77, T78))
U12_ggaaaaa(T73, T74, T77, T78, X169, X171, X172, lastE_out_ggaa(T73, T74, T77, T78)) → U13_ggaaaaa(T73, T74, T77, T78, X169, X171, X172, halvesF_in_gaaa(T78, X169, X171, X172))
U13_ggaaaaa(T73, T74, T77, T78, X169, X171, X172, halvesF_out_gaaa(T78, X169, X171, X172)) → pG_out_ggaaaaa(T73, T74, T77, T78, X169, X171, X172)
U5_gaaa(T72, T73, T74, X169, X170, X171, X172, pG_out_ggaaaaa(T73, T74, X170, X168, X169, X171, X172)) → halvesF_out_gaaa(.(T72, .(T73, T74)), .(T72, X169), .(X170, X171), X172)
U10_gaaagg(T27, T58, T59, T60, T21, T26, halvesF_out_gaaa(T27, T58, T59, T60)) → U11_gaaagg(T27, T58, T59, T60, T21, T26, pI_in_ggggg(T60, T21, T58, T26, T59))
pI_in_ggggg(even, T88, T89, T88, T89) → pI_out_ggggg(even, T88, T89, T88, T89)
U11_gaaagg(T27, T58, T59, T60, T21, T26, pI_out_ggggg(T60, T21, T58, T26, T59)) → pK_out_gaaagg(T27, T58, T59, T60, T21, T26)
U9_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21, pK_out_gaaagg(T27, X73, X75, X76, T21, T26)) → pB_out_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21)
U1_g(T21, T22, T23, pB_out_ggaaaaag(T22, T23, X74, X72, X73, X75, X76, T21)) → palindromeA_out_g(.(T21, .(T22, T23)))
palindromeA_in_g(T92) → U2_g(T92, pC_in_gaaaa(T92, X190, X191, X192, X193))
pC_in_gaaaa(T92, T93, T94, T95, X193) → U14_gaaaa(T92, T93, T94, T95, X193, halvesF_in_gaaa(T92, T93, T94, T95))
U14_gaaaa(T92, T93, T94, T95, X193, halvesF_out_gaaa(T92, T93, T94, T95)) → U15_gaaaa(T92, T93, T94, T95, X193, pJ_in_ggag(T95, T93, X193, T94))
pJ_in_ggag(odd, T93, X193, T94) → U7_ggag(T93, X193, T94, lastH_in_gag(T93, X193, T94))
lastH_in_gag(.(T107, []), T107, []) → lastH_out_gag(.(T107, []), T107, [])
lastH_in_gag(.(T114, T115), X220, .(T114, T116)) → U6_gag(T114, T115, X220, T116, lastH_in_gag(T115, X220, T116))
U6_gag(T114, T115, X220, T116, lastH_out_gag(T115, X220, T116)) → lastH_out_gag(.(T114, T115), X220, .(T114, T116))
U7_ggag(T93, X193, T94, lastH_out_gag(T93, X193, T94)) → pJ_out_ggag(odd, T93, X193, T94)
U15_gaaaa(T92, T93, T94, T95, X193, pJ_out_ggag(T95, T93, X193, T94)) → pC_out_gaaaa(T92, T93, T94, T95, X193)
U2_g(T92, pC_out_gaaaa(T92, X190, X191, X192, X193)) → palindromeA_out_g(T92)

The argument filtering Pi contains the following mapping:
palindromeA_in_g(x1) = palindromeA_in_g(x1)
[] = []
palindromeA_out_g(x1) = palindromeA_out_g(x1)
.(x1, x2) = .(x1, x2)
U1_g(x1, x2, x3, x4) = U1_g(x1, x2, x3, x4)
pB_in_ggaaaaag(x1, x2, x3, x4, x5, x6, x7, x8) = pB_in_ggaaaaag(x1, x2, x8)
U8_ggaaaaag(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U8_ggaaaaag(x1, x2, x8, x9)
lastE_in_ggaa(x1, x2, x3, x4) = lastE_in_ggaa(x1, x2)
lastE_out_ggaa(x1, x2, x3, x4) = lastE_out_ggaa(x1, x2, x3, x4)
U4_ggaa(x1, x2, x3, x4, x5) = U4_ggaa(x1, x2, x5)
lastD_in_gaa(x1, x2, x3) = lastD_in_gaa(x1)
lastD_out_gaa(x1, x2, x3) = lastD_out_gaa(x1, x2, x3)
U3_gaa(x1, x2, x3, x4, x5) = U3_gaa(x1, x2, x5)
U9_ggaaaaag(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U9_ggaaaaag(x1, x2, x3, x4, x8, x9)
pK_in_gaaagg(x1, x2, x3, x4, x5, x6) = pK_in_gaaagg(x1, x5, x6)
U10_gaaagg(x1, x2, x3, x4, x5, x6, x7) = U10_gaaagg(x1, x5, x6, x7)
halvesF_in_gaaa(x1, x2, x3, x4) = halvesF_in_gaaa(x1)
halvesF_out_gaaa(x1, x2, x3, x4) = halvesF_out_gaaa(x1, x2, x3, x4)
U5_gaaa(x1, x2, x3, x4, x5, x6, x7, x8) = U5_gaaa(x1, x2, x3, x8)
pG_in_ggaaaaa(x1, x2, x3, x4, x5, x6, x7) = pG_in_ggaaaaa(x1, x2)
U12_ggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8) = U12_ggaaaaa(x1, x2, x8)
U13_ggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8) = U13_ggaaaaa(x1, x2, x3, x4, x8)
pG_out_ggaaaaa(x1, x2, x3, x4, x5, x6, x7) = pG_out_ggaaaaa(x1, x2, x3, x4, x5, x6, x7)
U11_gaaagg(x1, x2, x3, x4, x5, x6, x7) = U11_gaaagg(x1, x2, x3, x4, x5, x6, x7)
pI_in_ggggg(x1, x2, x3, x4, x5) = pI_in_ggggg(x1, x2, x3, x4, x5)
even = even
pI_out_ggggg(x1, x2, x3, x4, x5) = pI_out_ggggg(x1, x2, x3, x4, x5)
pK_out_gaaagg(x1, x2, x3, x4, x5, x6) = pK_out_gaaagg(x1, x2, x3, x4, x5, x6)
pB_out_ggaaaaag(x1, x2, x3, x4, x5, x6, x7, x8) = pB_out_ggaaaaag(x1, x2, x3, x4, x5, x6, x7, x8)
U2_g(x1, x2) = U2_g(x1, x2)
pC_in_gaaaa(x1, x2, x3, x4, x5) = pC_in_gaaaa(x1)
U14_gaaaa(x1, x2, x3, x4, x5, x6) = U14_gaaaa(x1, x6)
U15_gaaaa(x1, x2, x3, x4, x5, x6) = U15_gaaaa(x1, x2, x3, x4, x6)
pJ_in_ggag(x1, x2, x3, x4) = pJ_in_ggag(x1, x2, x4)
odd = odd
U7_ggag(x1, x2, x3, x4) = U7_ggag(x1, x3, x4)
lastH_in_gag(x1, x2, x3) = lastH_in_gag(x1, x3)
lastH_out_gag(x1, x2, x3) = lastH_out_gag(x1, x2, x3)
U6_gag(x1, x2, x3, x4, x5) = U6_gag(x1, x2, x4, x5)
pJ_out_ggag(x1, x2, x3, x4) = pJ_out_ggag(x1, x2, x3, x4)
pC_out_gaaaa(x1, x2, x3, x4, x5) = pC_out_gaaaa(x1, x2, x3, x4, x5)
PALINDROMEA_IN_G(x1) = PALINDROMEA_IN_G(x1)
U1_G(x1, x2, x3, x4) = U1_G(x1, x2, x3, x4)
PB_IN_GGAAAAAG(x1, x2, x3, x4, x5, x6, x7, x8) = PB_IN_GGAAAAAG(x1, x2, x8)
U8_GGAAAAAG(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U8_GGAAAAAG(x1, x2, x8, x9)
LASTE_IN_GGAA(x1, x2, x3, x4) = LASTE_IN_GGAA(x1, x2)
U4_GGAA(x1, x2, x3, x4, x5) = U4_GGAA(x1, x2, x5)
LASTD_IN_GAA(x1, x2, x3) = LASTD_IN_GAA(x1)
U3_GAA(x1, x2, x3, x4, x5) = U3_GAA(x1, x2, x5)
U9_GGAAAAAG(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U9_GGAAAAAG(x1, x2, x3, x4, x8, x9)
PK_IN_GAAAGG(x1, x2, x3, x4, x5, x6) = PK_IN_GAAAGG(x1, x5, x6)
U10_GAAAGG(x1, x2, x3, x4, x5, x6, x7) = U10_GAAAGG(x1, x5, x6, x7)
HALVESF_IN_GAAA(x1, x2, x3, x4) = HALVESF_IN_GAAA(x1)
U5_GAAA(x1, x2, x3, x4, x5, x6, x7, x8) = U5_GAAA(x1, x2, x3, x8)
PG_IN_GGAAAAA(x1, x2, x3, x4, x5, x6, x7) = PG_IN_GGAAAAA(x1, x2)
U12_GGAAAAA(x1, x2, x3, x4, x5, x6, x7, x8) = U12_GGAAAAA(x1, x2, x8)
U13_GGAAAAA(x1, x2, x3, x4, x5, x6, x7, x8) = U13_GGAAAAA(x1, x2, x3, x4, x8)
U11_GAAAGG(x1, x2, x3, x4, x5, x6, x7) = U11_GAAAGG(x1, x2, x3, x4, x5, x6, x7)
PI_IN_GGGGG(x1, x2, x3, x4, x5) = PI_IN_GGGGG(x1, x2, x3, x4, x5)
U2_G(x1, x2) = U2_G(x1, x2)
PC_IN_GAAAA(x1, x2, x3, x4, x5) = PC_IN_GAAAA(x1)
U14_GAAAA(x1, x2, x3, x4, x5, x6) = U14_GAAAA(x1, x6)
U15_GAAAA(x1, x2, x3, x4, x5, x6) = U15_GAAAA(x1, x2, x3, x4, x6)
PJ_IN_GGAG(x1, x2, x3, x4) = PJ_IN_GGAG(x1, x2, x4)
U7_GGAG(x1, x2, x3, x4) = U7_GGAG(x1, x3, x4)
LASTH_IN_GAG(x1, x2, x3) = LASTH_IN_GAG(x1, x3)
U6_GAG(x1, x2, x3, x4, x5) = U6_GAG(x1, x2, x4, x5)

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(.(T21, .(T22, T23))) → U1_G(T21, T22, T23, pB_in_ggaaaaag(T22, T23, X74, X72, X73, X75, X76, T21))
PALINDROMEA_IN_G(.(T21, .(T22, T23))) → PB_IN_GGAAAAAG(T22, T23, X74, X72, X73, X75, X76, T21)
PB_IN_GGAAAAAG(T22, T23, T26, T27, X73, X75, X76, T21) → U8_GGAAAAAG(T22, T23, T26, T27, X73, X75, X76, T21, lastE_in_ggaa(T22, T23, T26, T27))
PB_IN_GGAAAAAG(T22, T23, T26, T27, X73, X75, X76, T21) → LASTE_IN_GGAA(T22, T23, T26, T27)
LASTE_IN_GGAA(T41, T42, X104, .(T41, X105)) → U4_GGAA(T41, T42, X104, X105, lastD_in_gaa(T42, X104, X105))
LASTE_IN_GGAA(T41, T42, X104, .(T41, X105)) → LASTD_IN_GAA(T42, X104, X105)
LASTD_IN_GAA(.(T54, T55), X129, .(T54, X130)) → U3_GAA(T54, T55, X129, X130, lastD_in_gaa(T55, X129, X130))
LASTD_IN_GAA(.(T54, T55), X129, .(T54, X130)) → LASTD_IN_GAA(T55, X129, X130)
U8_GGAAAAAG(T22, T23, T26, T27, X73, X75, X76, T21, lastE_out_ggaa(T22, T23, T26, T27)) → U9_GGAAAAAG(T22, T23, T26, T27, X73, X75, X76, T21, pK_in_gaaagg(T27, X73, X75, X76, T21, T26))
U8_GGAAAAAG(T22, T23, T26, T27, X73, X75, X76, T21, lastE_out_ggaa(T22, T23, T26, T27)) → PK_IN_GAAAGG(T27, X73, X75, X76, T21, T26)
PK_IN_GAAAGG(T27, T58, T59, T60, T21, T26) → U10_GAAAGG(T27, T58, T59, T60, T21, T26, halvesF_in_gaaa(T27, T58, T59, T60))
PK_IN_GAAAGG(T27, T58, T59, T60, T21, T26) → HALVESF_IN_GAAA(T27, T58, T59, T60)
HALVESF_IN_GAAA(.(T72, .(T73, T74)), .(T72, X169), .(X170, X171), X172) → U5_GAAA(T72, T73, T74, X169, X170, X171, X172, pG_in_ggaaaaa(T73, T74, X170, X168, X169, X171, X172))
HALVESF_IN_GAAA(.(T72, .(T73, T74)), .(T72, X169), .(X170, X171), X172) → PG_IN_GGAAAAA(T73, T74, X170, X168, X169, X171, X172)
PG_IN_GGAAAAA(T73, T74, T77, T78, X169, X171, X172) → U12_GGAAAAA(T73, T74, T77, T78, X169, X171, X172, lastE_in_ggaa(T73, T74, T77, T78))
PG_IN_GGAAAAA(T73, T74, T77, T78, X169, X171, X172) → LASTE_IN_GGAA(T73, T74, T77, T78)
U12_GGAAAAA(T73, T74, T77, T78, X169, X171, X172, lastE_out_ggaa(T73, T74, T77, T78)) → U13_GGAAAAA(T73, T74, T77, T78, X169, X171, X172, halvesF_in_gaaa(T78, X169, X171, X172))
U12_GGAAAAA(T73, T74, T77, T78, X169, X171, X172, lastE_out_ggaa(T73, T74, T77, T78)) → HALVESF_IN_GAAA(T78, X169, X171, X172)
U10_GAAAGG(T27, T58, T59, T60, T21, T26, halvesF_out_gaaa(T27, T58, T59, T60)) → U11_GAAAGG(T27, T58, T59, T60, T21, T26, pI_in_ggggg(T60, T21, T58, T26, T59))
U10_GAAAGG(T27, T58, T59, T60, T21, T26, halvesF_out_gaaa(T27, T58, T59, T60)) → PI_IN_GGGGG(T60, T21, T58, T26, T59)
PALINDROMEA_IN_G(T92) → U2_G(T92, pC_in_gaaaa(T92, X190, X191, X192, X193))
PALINDROMEA_IN_G(T92) → PC_IN_GAAAA(T92, X190, X191, X192, X193)
PC_IN_GAAAA(T92, T93, T94, T95, X193) → U14_GAAAA(T92, T93, T94, T95, X193, halvesF_in_gaaa(T92, T93, T94, T95))
PC_IN_GAAAA(T92, T93, T94, T95, X193) → HALVESF_IN_GAAA(T92, T93, T94, T95)
U14_GAAAA(T92, T93, T94, T95, X193, halvesF_out_gaaa(T92, T93, T94, T95)) → U15_GAAAA(T92, T93, T94, T95, X193, pJ_in_ggag(T95, T93, X193, T94))
U14_GAAAA(T92, T93, T94, T95, X193, halvesF_out_gaaa(T92, T93, T94, T95)) → PJ_IN_GGAG(T95, T93, X193, T94)
PJ_IN_GGAG(odd, T93, X193, T94) → U7_GGAG(T93, X193, T94, lastH_in_gag(T93, X193, T94))
PJ_IN_GGAG(odd, T93, X193, T94) → LASTH_IN_GAG(T93, X193, T94)
LASTH_IN_GAG(.(T114, T115), X220, .(T114, T116)) → U6_GAG(T114, T115, X220, T116, lastH_in_gag(T115, X220, T116))
LASTH_IN_GAG(.(T114, T115), X220, .(T114, T116)) → LASTH_IN_GAG(T115, X220, T116)

The TRS R consists of the following rules:

palindromeA_in_g([]) → palindromeA_out_g([])
palindromeA_in_g(.(T21, .(T22, T23))) → U1_g(T21, T22, T23, pB_in_ggaaaaag(T22, T23, X74, X72, X73, X75, X76, T21))
pB_in_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21) → U8_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21, lastE_in_ggaa(T22, T23, T26, T27))
lastE_in_ggaa(T34, [], T34, []) → lastE_out_ggaa(T34, [], T34, [])
lastE_in_ggaa(T41, T42, X104, .(T41, X105)) → U4_ggaa(T41, T42, X104, X105, lastD_in_gaa(T42, X104, X105))
lastD_in_gaa(.(T49, []), T49, []) → lastD_out_gaa(.(T49, []), T49, [])
lastD_in_gaa(.(T54, T55), X129, .(T54, X130)) → U3_gaa(T54, T55, X129, X130, lastD_in_gaa(T55, X129, X130))
U3_gaa(T54, T55, X129, X130, lastD_out_gaa(T55, X129, X130)) → lastD_out_gaa(.(T54, T55), X129, .(T54, X130))
U4_ggaa(T41, T42, X104, X105, lastD_out_gaa(T42, X104, X105)) → lastE_out_ggaa(T41, T42, X104, .(T41, X105))
U8_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21, lastE_out_ggaa(T22, T23, T26, T27)) → U9_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21, pK_in_gaaagg(T27, X73, X75, X76, T21, T26))
pK_in_gaaagg(T27, T58, T59, T60, T21, T26) → U10_gaaagg(T27, T58, T59, T60, T21, T26, halvesF_in_gaaa(T27, T58, T59, T60))
halvesF_in_gaaa([], [], [], even) → halvesF_out_gaaa([], [], [], even)
halvesF_in_gaaa(.(T65, []), .(T65, []), [], odd) → halvesF_out_gaaa(.(T65, []), .(T65, []), [], odd)
halvesF_in_gaaa(.(T72, .(T73, T74)), .(T72, X169), .(X170, X171), X172) → U5_gaaa(T72, T73, T74, X169, X170, X171, X172, pG_in_ggaaaaa(T73, T74, X170, X168, X169, X171, X172))
pG_in_ggaaaaa(T73, T74, T77, T78, X169, X171, X172) → U12_ggaaaaa(T73, T74, T77, T78, X169, X171, X172, lastE_in_ggaa(T73, T74, T77, T78))
U12_ggaaaaa(T73, T74, T77, T78, X169, X171, X172, lastE_out_ggaa(T73, T74, T77, T78)) → U13_ggaaaaa(T73, T74, T77, T78, X169, X171, X172, halvesF_in_gaaa(T78, X169, X171, X172))
U13_ggaaaaa(T73, T74, T77, T78, X169, X171, X172, halvesF_out_gaaa(T78, X169, X171, X172)) → pG_out_ggaaaaa(T73, T74, T77, T78, X169, X171, X172)
U5_gaaa(T72, T73, T74, X169, X170, X171, X172, pG_out_ggaaaaa(T73, T74, X170, X168, X169, X171, X172)) → halvesF_out_gaaa(.(T72, .(T73, T74)), .(T72, X169), .(X170, X171), X172)
U10_gaaagg(T27, T58, T59, T60, T21, T26, halvesF_out_gaaa(T27, T58, T59, T60)) → U11_gaaagg(T27, T58, T59, T60, T21, T26, pI_in_ggggg(T60, T21, T58, T26, T59))
pI_in_ggggg(even, T88, T89, T88, T89) → pI_out_ggggg(even, T88, T89, T88, T89)
U11_gaaagg(T27, T58, T59, T60, T21, T26, pI_out_ggggg(T60, T21, T58, T26, T59)) → pK_out_gaaagg(T27, T58, T59, T60, T21, T26)
U9_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21, pK_out_gaaagg(T27, X73, X75, X76, T21, T26)) → pB_out_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21)
U1_g(T21, T22, T23, pB_out_ggaaaaag(T22, T23, X74, X72, X73, X75, X76, T21)) → palindromeA_out_g(.(T21, .(T22, T23)))
palindromeA_in_g(T92) → U2_g(T92, pC_in_gaaaa(T92, X190, X191, X192, X193))
pC_in_gaaaa(T92, T93, T94, T95, X193) → U14_gaaaa(T92, T93, T94, T95, X193, halvesF_in_gaaa(T92, T93, T94, T95))
U14_gaaaa(T92, T93, T94, T95, X193, halvesF_out_gaaa(T92, T93, T94, T95)) → U15_gaaaa(T92, T93, T94, T95, X193, pJ_in_ggag(T95, T93, X193, T94))
pJ_in_ggag(odd, T93, X193, T94) → U7_ggag(T93, X193, T94, lastH_in_gag(T93, X193, T94))
lastH_in_gag(.(T107, []), T107, []) → lastH_out_gag(.(T107, []), T107, [])
lastH_in_gag(.(T114, T115), X220, .(T114, T116)) → U6_gag(T114, T115, X220, T116, lastH_in_gag(T115, X220, T116))
U6_gag(T114, T115, X220, T116, lastH_out_gag(T115, X220, T116)) → lastH_out_gag(.(T114, T115), X220, .(T114, T116))
U7_ggag(T93, X193, T94, lastH_out_gag(T93, X193, T94)) → pJ_out_ggag(odd, T93, X193, T94)
U15_gaaaa(T92, T93, T94, T95, X193, pJ_out_ggag(T95, T93, X193, T94)) → pC_out_gaaaa(T92, T93, T94, T95, X193)
U2_g(T92, pC_out_gaaaa(T92, X190, X191, X192, X193)) → palindromeA_out_g(T92)

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

LASTH_IN_GAG(.(T114, T115), X220, .(T114, T116)) → LASTH_IN_GAG(T115, X220, T116)

The TRS R consists of the following rules:

palindromeA_in_g([]) → palindromeA_out_g([])
palindromeA_in_g(.(T21, .(T22, T23))) → U1_g(T21, T22, T23, pB_in_ggaaaaag(T22, T23, X74, X72, X73, X75, X76, T21))
pB_in_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21) → U8_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21, lastE_in_ggaa(T22, T23, T26, T27))
lastE_in_ggaa(T34, [], T34, []) → lastE_out_ggaa(T34, [], T34, [])
lastE_in_ggaa(T41, T42, X104, .(T41, X105)) → U4_ggaa(T41, T42, X104, X105, lastD_in_gaa(T42, X104, X105))
lastD_in_gaa(.(T49, []), T49, []) → lastD_out_gaa(.(T49, []), T49, [])
lastD_in_gaa(.(T54, T55), X129, .(T54, X130)) → U3_gaa(T54, T55, X129, X130, lastD_in_gaa(T55, X129, X130))
U3_gaa(T54, T55, X129, X130, lastD_out_gaa(T55, X129, X130)) → lastD_out_gaa(.(T54, T55), X129, .(T54, X130))
U4_ggaa(T41, T42, X104, X105, lastD_out_gaa(T42, X104, X105)) → lastE_out_ggaa(T41, T42, X104, .(T41, X105))
U8_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21, lastE_out_ggaa(T22, T23, T26, T27)) → U9_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21, pK_in_gaaagg(T27, X73, X75, X76, T21, T26))
pK_in_gaaagg(T27, T58, T59, T60, T21, T26) → U10_gaaagg(T27, T58, T59, T60, T21, T26, halvesF_in_gaaa(T27, T58, T59, T60))
halvesF_in_gaaa([], [], [], even) → halvesF_out_gaaa([], [], [], even)
halvesF_in_gaaa(.(T65, []), .(T65, []), [], odd) → halvesF_out_gaaa(.(T65, []), .(T65, []), [], odd)
halvesF_in_gaaa(.(T72, .(T73, T74)), .(T72, X169), .(X170, X171), X172) → U5_gaaa(T72, T73, T74, X169, X170, X171, X172, pG_in_ggaaaaa(T73, T74, X170, X168, X169, X171, X172))
pG_in_ggaaaaa(T73, T74, T77, T78, X169, X171, X172) → U12_ggaaaaa(T73, T74, T77, T78, X169, X171, X172, lastE_in_ggaa(T73, T74, T77, T78))
U12_ggaaaaa(T73, T74, T77, T78, X169, X171, X172, lastE_out_ggaa(T73, T74, T77, T78)) → U13_ggaaaaa(T73, T74, T77, T78, X169, X171, X172, halvesF_in_gaaa(T78, X169, X171, X172))
U13_ggaaaaa(T73, T74, T77, T78, X169, X171, X172, halvesF_out_gaaa(T78, X169, X171, X172)) → pG_out_ggaaaaa(T73, T74, T77, T78, X169, X171, X172)
U5_gaaa(T72, T73, T74, X169, X170, X171, X172, pG_out_ggaaaaa(T73, T74, X170, X168, X169, X171, X172)) → halvesF_out_gaaa(.(T72, .(T73, T74)), .(T72, X169), .(X170, X171), X172)
U10_gaaagg(T27, T58, T59, T60, T21, T26, halvesF_out_gaaa(T27, T58, T59, T60)) → U11_gaaagg(T27, T58, T59, T60, T21, T26, pI_in_ggggg(T60, T21, T58, T26, T59))
pI_in_ggggg(even, T88, T89, T88, T89) → pI_out_ggggg(even, T88, T89, T88, T89)
U11_gaaagg(T27, T58, T59, T60, T21, T26, pI_out_ggggg(T60, T21, T58, T26, T59)) → pK_out_gaaagg(T27, T58, T59, T60, T21, T26)
U9_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21, pK_out_gaaagg(T27, X73, X75, X76, T21, T26)) → pB_out_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21)
U1_g(T21, T22, T23, pB_out_ggaaaaag(T22, T23, X74, X72, X73, X75, X76, T21)) → palindromeA_out_g(.(T21, .(T22, T23)))
palindromeA_in_g(T92) → U2_g(T92, pC_in_gaaaa(T92, X190, X191, X192, X193))
pC_in_gaaaa(T92, T93, T94, T95, X193) → U14_gaaaa(T92, T93, T94, T95, X193, halvesF_in_gaaa(T92, T93, T94, T95))
U14_gaaaa(T92, T93, T94, T95, X193, halvesF_out_gaaa(T92, T93, T94, T95)) → U15_gaaaa(T92, T93, T94, T95, X193, pJ_in_ggag(T95, T93, X193, T94))
pJ_in_ggag(odd, T93, X193, T94) → U7_ggag(T93, X193, T94, lastH_in_gag(T93, X193, T94))
lastH_in_gag(.(T107, []), T107, []) → lastH_out_gag(.(T107, []), T107, [])
lastH_in_gag(.(T114, T115), X220, .(T114, T116)) → U6_gag(T114, T115, X220, T116, lastH_in_gag(T115, X220, T116))
U6_gag(T114, T115, X220, T116, lastH_out_gag(T115, X220, T116)) → lastH_out_gag(.(T114, T115), X220, .(T114, T116))
U7_ggag(T93, X193, T94, lastH_out_gag(T93, X193, T94)) → pJ_out_ggag(odd, T93, X193, T94)
U15_gaaaa(T92, T93, T94, T95, X193, pJ_out_ggag(T95, T93, X193, T94)) → pC_out_gaaaa(T92, T93, T94, T95, X193)
U2_g(T92, pC_out_gaaaa(T92, X190, X191, X192, X193)) → palindromeA_out_g(T92)

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

LASTH_IN_GAG(.(T114, T115), X220, .(T114, T116)) → LASTH_IN_GAG(T115, X220, T116)

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

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:

LASTH_IN_GAG(.(T114, T115), .(T114, T116)) → LASTH_IN_GAG(T115, T116)

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

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

LASTH_IN_GAG(.(T114, T115), .(T114, T116)) → LASTH_IN_GAG(T115, T116)
The graph contains the following edges 1 > 1, 2 > 2

(13) YES

(14) Obligation:

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

LASTD_IN_GAA(.(T54, T55), X129, .(T54, X130)) → LASTD_IN_GAA(T55, X129, X130)

The TRS R consists of the following rules:

palindromeA_in_g([]) → palindromeA_out_g([])
palindromeA_in_g(.(T21, .(T22, T23))) → U1_g(T21, T22, T23, pB_in_ggaaaaag(T22, T23, X74, X72, X73, X75, X76, T21))
pB_in_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21) → U8_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21, lastE_in_ggaa(T22, T23, T26, T27))
lastE_in_ggaa(T34, [], T34, []) → lastE_out_ggaa(T34, [], T34, [])
lastE_in_ggaa(T41, T42, X104, .(T41, X105)) → U4_ggaa(T41, T42, X104, X105, lastD_in_gaa(T42, X104, X105))
lastD_in_gaa(.(T49, []), T49, []) → lastD_out_gaa(.(T49, []), T49, [])
lastD_in_gaa(.(T54, T55), X129, .(T54, X130)) → U3_gaa(T54, T55, X129, X130, lastD_in_gaa(T55, X129, X130))
U3_gaa(T54, T55, X129, X130, lastD_out_gaa(T55, X129, X130)) → lastD_out_gaa(.(T54, T55), X129, .(T54, X130))
U4_ggaa(T41, T42, X104, X105, lastD_out_gaa(T42, X104, X105)) → lastE_out_ggaa(T41, T42, X104, .(T41, X105))
U8_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21, lastE_out_ggaa(T22, T23, T26, T27)) → U9_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21, pK_in_gaaagg(T27, X73, X75, X76, T21, T26))
pK_in_gaaagg(T27, T58, T59, T60, T21, T26) → U10_gaaagg(T27, T58, T59, T60, T21, T26, halvesF_in_gaaa(T27, T58, T59, T60))
halvesF_in_gaaa([], [], [], even) → halvesF_out_gaaa([], [], [], even)
halvesF_in_gaaa(.(T65, []), .(T65, []), [], odd) → halvesF_out_gaaa(.(T65, []), .(T65, []), [], odd)
halvesF_in_gaaa(.(T72, .(T73, T74)), .(T72, X169), .(X170, X171), X172) → U5_gaaa(T72, T73, T74, X169, X170, X171, X172, pG_in_ggaaaaa(T73, T74, X170, X168, X169, X171, X172))
pG_in_ggaaaaa(T73, T74, T77, T78, X169, X171, X172) → U12_ggaaaaa(T73, T74, T77, T78, X169, X171, X172, lastE_in_ggaa(T73, T74, T77, T78))
U12_ggaaaaa(T73, T74, T77, T78, X169, X171, X172, lastE_out_ggaa(T73, T74, T77, T78)) → U13_ggaaaaa(T73, T74, T77, T78, X169, X171, X172, halvesF_in_gaaa(T78, X169, X171, X172))
U13_ggaaaaa(T73, T74, T77, T78, X169, X171, X172, halvesF_out_gaaa(T78, X169, X171, X172)) → pG_out_ggaaaaa(T73, T74, T77, T78, X169, X171, X172)
U5_gaaa(T72, T73, T74, X169, X170, X171, X172, pG_out_ggaaaaa(T73, T74, X170, X168, X169, X171, X172)) → halvesF_out_gaaa(.(T72, .(T73, T74)), .(T72, X169), .(X170, X171), X172)
U10_gaaagg(T27, T58, T59, T60, T21, T26, halvesF_out_gaaa(T27, T58, T59, T60)) → U11_gaaagg(T27, T58, T59, T60, T21, T26, pI_in_ggggg(T60, T21, T58, T26, T59))
pI_in_ggggg(even, T88, T89, T88, T89) → pI_out_ggggg(even, T88, T89, T88, T89)
U11_gaaagg(T27, T58, T59, T60, T21, T26, pI_out_ggggg(T60, T21, T58, T26, T59)) → pK_out_gaaagg(T27, T58, T59, T60, T21, T26)
U9_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21, pK_out_gaaagg(T27, X73, X75, X76, T21, T26)) → pB_out_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21)
U1_g(T21, T22, T23, pB_out_ggaaaaag(T22, T23, X74, X72, X73, X75, X76, T21)) → palindromeA_out_g(.(T21, .(T22, T23)))
palindromeA_in_g(T92) → U2_g(T92, pC_in_gaaaa(T92, X190, X191, X192, X193))
pC_in_gaaaa(T92, T93, T94, T95, X193) → U14_gaaaa(T92, T93, T94, T95, X193, halvesF_in_gaaa(T92, T93, T94, T95))
U14_gaaaa(T92, T93, T94, T95, X193, halvesF_out_gaaa(T92, T93, T94, T95)) → U15_gaaaa(T92, T93, T94, T95, X193, pJ_in_ggag(T95, T93, X193, T94))
pJ_in_ggag(odd, T93, X193, T94) → U7_ggag(T93, X193, T94, lastH_in_gag(T93, X193, T94))
lastH_in_gag(.(T107, []), T107, []) → lastH_out_gag(.(T107, []), T107, [])
lastH_in_gag(.(T114, T115), X220, .(T114, T116)) → U6_gag(T114, T115, X220, T116, lastH_in_gag(T115, X220, T116))
U6_gag(T114, T115, X220, T116, lastH_out_gag(T115, X220, T116)) → lastH_out_gag(.(T114, T115), X220, .(T114, T116))
U7_ggag(T93, X193, T94, lastH_out_gag(T93, X193, T94)) → pJ_out_ggag(odd, T93, X193, T94)
U15_gaaaa(T92, T93, T94, T95, X193, pJ_out_ggag(T95, T93, X193, T94)) → pC_out_gaaaa(T92, T93, T94, T95, X193)
U2_g(T92, pC_out_gaaaa(T92, X190, X191, X192, X193)) → palindromeA_out_g(T92)

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

LASTD_IN_GAA(.(T54, T55), X129, .(T54, X130)) → LASTD_IN_GAA(T55, X129, X130)

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

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:

LASTD_IN_GAA(.(T54, T55)) → LASTD_IN_GAA(T55)

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

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

LASTD_IN_GAA(.(T54, T55)) → LASTD_IN_GAA(T55)
The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

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

PG_IN_GGAAAAA(T73, T74, T77, T78, X169, X171, X172) → U12_GGAAAAA(T73, T74, T77, T78, X169, X171, X172, lastE_in_ggaa(T73, T74, T77, T78))
U12_GGAAAAA(T73, T74, T77, T78, X169, X171, X172, lastE_out_ggaa(T73, T74, T77, T78)) → HALVESF_IN_GAAA(T78, X169, X171, X172)
HALVESF_IN_GAAA(.(T72, .(T73, T74)), .(T72, X169), .(X170, X171), X172) → PG_IN_GGAAAAA(T73, T74, X170, X168, X169, X171, X172)

The TRS R consists of the following rules:

palindromeA_in_g([]) → palindromeA_out_g([])
palindromeA_in_g(.(T21, .(T22, T23))) → U1_g(T21, T22, T23, pB_in_ggaaaaag(T22, T23, X74, X72, X73, X75, X76, T21))
pB_in_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21) → U8_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21, lastE_in_ggaa(T22, T23, T26, T27))
lastE_in_ggaa(T34, [], T34, []) → lastE_out_ggaa(T34, [], T34, [])
lastE_in_ggaa(T41, T42, X104, .(T41, X105)) → U4_ggaa(T41, T42, X104, X105, lastD_in_gaa(T42, X104, X105))
lastD_in_gaa(.(T49, []), T49, []) → lastD_out_gaa(.(T49, []), T49, [])
lastD_in_gaa(.(T54, T55), X129, .(T54, X130)) → U3_gaa(T54, T55, X129, X130, lastD_in_gaa(T55, X129, X130))
U3_gaa(T54, T55, X129, X130, lastD_out_gaa(T55, X129, X130)) → lastD_out_gaa(.(T54, T55), X129, .(T54, X130))
U4_ggaa(T41, T42, X104, X105, lastD_out_gaa(T42, X104, X105)) → lastE_out_ggaa(T41, T42, X104, .(T41, X105))
U8_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21, lastE_out_ggaa(T22, T23, T26, T27)) → U9_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21, pK_in_gaaagg(T27, X73, X75, X76, T21, T26))
pK_in_gaaagg(T27, T58, T59, T60, T21, T26) → U10_gaaagg(T27, T58, T59, T60, T21, T26, halvesF_in_gaaa(T27, T58, T59, T60))
halvesF_in_gaaa([], [], [], even) → halvesF_out_gaaa([], [], [], even)
halvesF_in_gaaa(.(T65, []), .(T65, []), [], odd) → halvesF_out_gaaa(.(T65, []), .(T65, []), [], odd)
halvesF_in_gaaa(.(T72, .(T73, T74)), .(T72, X169), .(X170, X171), X172) → U5_gaaa(T72, T73, T74, X169, X170, X171, X172, pG_in_ggaaaaa(T73, T74, X170, X168, X169, X171, X172))
pG_in_ggaaaaa(T73, T74, T77, T78, X169, X171, X172) → U12_ggaaaaa(T73, T74, T77, T78, X169, X171, X172, lastE_in_ggaa(T73, T74, T77, T78))
U12_ggaaaaa(T73, T74, T77, T78, X169, X171, X172, lastE_out_ggaa(T73, T74, T77, T78)) → U13_ggaaaaa(T73, T74, T77, T78, X169, X171, X172, halvesF_in_gaaa(T78, X169, X171, X172))
U13_ggaaaaa(T73, T74, T77, T78, X169, X171, X172, halvesF_out_gaaa(T78, X169, X171, X172)) → pG_out_ggaaaaa(T73, T74, T77, T78, X169, X171, X172)
U5_gaaa(T72, T73, T74, X169, X170, X171, X172, pG_out_ggaaaaa(T73, T74, X170, X168, X169, X171, X172)) → halvesF_out_gaaa(.(T72, .(T73, T74)), .(T72, X169), .(X170, X171), X172)
U10_gaaagg(T27, T58, T59, T60, T21, T26, halvesF_out_gaaa(T27, T58, T59, T60)) → U11_gaaagg(T27, T58, T59, T60, T21, T26, pI_in_ggggg(T60, T21, T58, T26, T59))
pI_in_ggggg(even, T88, T89, T88, T89) → pI_out_ggggg(even, T88, T89, T88, T89)
U11_gaaagg(T27, T58, T59, T60, T21, T26, pI_out_ggggg(T60, T21, T58, T26, T59)) → pK_out_gaaagg(T27, T58, T59, T60, T21, T26)
U9_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21, pK_out_gaaagg(T27, X73, X75, X76, T21, T26)) → pB_out_ggaaaaag(T22, T23, T26, T27, X73, X75, X76, T21)
U1_g(T21, T22, T23, pB_out_ggaaaaag(T22, T23, X74, X72, X73, X75, X76, T21)) → palindromeA_out_g(.(T21, .(T22, T23)))
palindromeA_in_g(T92) → U2_g(T92, pC_in_gaaaa(T92, X190, X191, X192, X193))
pC_in_gaaaa(T92, T93, T94, T95, X193) → U14_gaaaa(T92, T93, T94, T95, X193, halvesF_in_gaaa(T92, T93, T94, T95))
U14_gaaaa(T92, T93, T94, T95, X193, halvesF_out_gaaa(T92, T93, T94, T95)) → U15_gaaaa(T92, T93, T94, T95, X193, pJ_in_ggag(T95, T93, X193, T94))
pJ_in_ggag(odd, T93, X193, T94) → U7_ggag(T93, X193, T94, lastH_in_gag(T93, X193, T94))
lastH_in_gag(.(T107, []), T107, []) → lastH_out_gag(.(T107, []), T107, [])
lastH_in_gag(.(T114, T115), X220, .(T114, T116)) → U6_gag(T114, T115, X220, T116, lastH_in_gag(T115, X220, T116))
U6_gag(T114, T115, X220, T116, lastH_out_gag(T115, X220, T116)) → lastH_out_gag(.(T114, T115), X220, .(T114, T116))
U7_ggag(T93, X193, T94, lastH_out_gag(T93, X193, T94)) → pJ_out_ggag(odd, T93, X193, T94)
U15_gaaaa(T92, T93, T94, T95, X193, pJ_out_ggag(T95, T93, X193, T94)) → pC_out_gaaaa(T92, T93, T94, T95, X193)
U2_g(T92, pC_out_gaaaa(T92, X190, X191, X192, X193)) → palindromeA_out_g(T92)

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

PG_IN_GGAAAAA(T73, T74, T77, T78, X169, X171, X172) → U12_GGAAAAA(T73, T74, T77, T78, X169, X171, X172, lastE_in_ggaa(T73, T74, T77, T78))
U12_GGAAAAA(T73, T74, T77, T78, X169, X171, X172, lastE_out_ggaa(T73, T74, T77, T78)) → HALVESF_IN_GAAA(T78, X169, X171, X172)
HALVESF_IN_GAAA(.(T72, .(T73, T74)), .(T72, X169), .(X170, X171), X172) → PG_IN_GGAAAAA(T73, T74, X170, X168, X169, X171, X172)

The TRS R consists of the following rules:

lastE_in_ggaa(T34, [], T34, []) → lastE_out_ggaa(T34, [], T34, [])
lastE_in_ggaa(T41, T42, X104, .(T41, X105)) → U4_ggaa(T41, T42, X104, X105, lastD_in_gaa(T42, X104, X105))
U4_ggaa(T41, T42, X104, X105, lastD_out_gaa(T42, X104, X105)) → lastE_out_ggaa(T41, T42, X104, .(T41, X105))
lastD_in_gaa(.(T49, []), T49, []) → lastD_out_gaa(.(T49, []), T49, [])
lastD_in_gaa(.(T54, T55), X129, .(T54, X130)) → U3_gaa(T54, T55, X129, X130, lastD_in_gaa(T55, X129, X130))
U3_gaa(T54, T55, X129, X130, lastD_out_gaa(T55, X129, X130)) → lastD_out_gaa(.(T54, T55), X129, .(T54, X130))

The argument filtering Pi contains the following mapping:
[] = []
.(x1, x2) = .(x1, x2)
lastE_in_ggaa(x1, x2, x3, x4) = lastE_in_ggaa(x1, x2)
lastE_out_ggaa(x1, x2, x3, x4) = lastE_out_ggaa(x1, x2, x3, x4)
U4_ggaa(x1, x2, x3, x4, x5) = U4_ggaa(x1, x2, x5)
lastD_in_gaa(x1, x2, x3) = lastD_in_gaa(x1)
lastD_out_gaa(x1, x2, x3) = lastD_out_gaa(x1, x2, x3)
U3_gaa(x1, x2, x3, x4, x5) = U3_gaa(x1, x2, x5)
HALVESF_IN_GAAA(x1, x2, x3, x4) = HALVESF_IN_GAAA(x1)
PG_IN_GGAAAAA(x1, x2, x3, x4, x5, x6, x7) = PG_IN_GGAAAAA(x1, x2)
U12_GGAAAAA(x1, x2, x3, x4, x5, x6, x7, x8) = U12_GGAAAAA(x1, x2, x8)

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

PG_IN_GGAAAAA(T73, T74) → U12_GGAAAAA(T73, T74, lastE_in_ggaa(T73, T74))
U12_GGAAAAA(T73, T74, lastE_out_ggaa(T73, T74, T77, T78)) → HALVESF_IN_GAAA(T78)
HALVESF_IN_GAAA(.(T72, .(T73, T74))) → PG_IN_GGAAAAA(T73, T74)

The TRS R consists of the following rules:

lastE_in_ggaa(T34, []) → lastE_out_ggaa(T34, [], T34, [])
lastE_in_ggaa(T41, T42) → U4_ggaa(T41, T42, lastD_in_gaa(T42))
U4_ggaa(T41, T42, lastD_out_gaa(T42, X104, X105)) → lastE_out_ggaa(T41, T42, X104, .(T41, X105))
lastD_in_gaa(.(T49, [])) → lastD_out_gaa(.(T49, []), T49, [])
lastD_in_gaa(.(T54, T55)) → U3_gaa(T54, T55, lastD_in_gaa(T55))
U3_gaa(T54, T55, lastD_out_gaa(T55, X129, X130)) → lastD_out_gaa(.(T54, T55), X129, .(T54, X130))

The set Q consists of the following terms:

lastE_in_ggaa(x0, x1)
U4_ggaa(x0, x1, x2)
lastD_in_gaa(x0)
U3_gaa(x0, x1, x2)

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

(26) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

HALVESF_IN_GAAA(.(T72, .(T73, T74))) → PG_IN_GGAAAAA(T73, T74)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = 1 + x₂
POL(HALVESF_IN_GAAA(x₁)) = x₁
POL(PG_IN_GGAAAAA(x₁, x₂)) = x₂
POL(U12_GGAAAAA(x₁, x₂, x₃)) = x₃
POL(U3_gaa(x₁, x₂, x₃)) = 1 + x₃
POL(U4_ggaa(x₁, x₂, x₃)) = x₃
POL([]) = 0
POL(lastD_in_gaa(x₁)) = x₁
POL(lastD_out_gaa(x₁, x₂, x₃)) = 1 + x₃
POL(lastE_in_ggaa(x₁, x₂)) = x₂
POL(lastE_out_ggaa(x₁, x₂, x₃, x₄)) = x₄

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

lastE_in_ggaa(T34, []) → lastE_out_ggaa(T34, [], T34, [])
lastE_in_ggaa(T41, T42) → U4_ggaa(T41, T42, lastD_in_gaa(T42))
lastD_in_gaa(.(T49, [])) → lastD_out_gaa(.(T49, []), T49, [])
lastD_in_gaa(.(T54, T55)) → U3_gaa(T54, T55, lastD_in_gaa(T55))
U4_ggaa(T41, T42, lastD_out_gaa(T42, X104, X105)) → lastE_out_ggaa(T41, T42, X104, .(T41, X105))
U3_gaa(T54, T55, lastD_out_gaa(T55, X129, X130)) → lastD_out_gaa(.(T54, T55), X129, .(T54, X130))

(27) Obligation:

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

PG_IN_GGAAAAA(T73, T74) → U12_GGAAAAA(T73, T74, lastE_in_ggaa(T73, T74))
U12_GGAAAAA(T73, T74, lastE_out_ggaa(T73, T74, T77, T78)) → HALVESF_IN_GAAA(T78)

The TRS R consists of the following rules:

lastE_in_ggaa(T34, []) → lastE_out_ggaa(T34, [], T34, [])
lastE_in_ggaa(T41, T42) → U4_ggaa(T41, T42, lastD_in_gaa(T42))
U4_ggaa(T41, T42, lastD_out_gaa(T42, X104, X105)) → lastE_out_ggaa(T41, T42, X104, .(T41, X105))
lastD_in_gaa(.(T49, [])) → lastD_out_gaa(.(T49, []), T49, [])
lastD_in_gaa(.(T54, T55)) → U3_gaa(T54, T55, lastD_in_gaa(T55))
U3_gaa(T54, T55, lastD_out_gaa(T55, X129, X130)) → lastD_out_gaa(.(T54, T55), X129, .(T54, X130))

The set Q consists of the following terms:

lastE_in_ggaa(x0, x1)
U4_ggaa(x0, x1, x2)
lastD_in_gaa(x0)
U3_gaa(x0, x1, x2)

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

(28) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(0) Obligation:

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) PiDPToQDPProof (SOUND transformation)

(11) Obligation:

(12) QDPSizeChangeProof (EQUIVALENT transformation)

(13) YES

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) PiDPToQDPProof (SOUND transformation)

(18) Obligation:

(19) QDPSizeChangeProof (EQUIVALENT transformation)

(20) YES

(21) Obligation:

(22) UsableRulesProof (EQUIVALENT transformation)

(23) Obligation:

(24) PiDPToQDPProof (SOUND transformation)

(25) Obligation:

(26) QDPOrderProof (EQUIVALENT transformation)

(27) Obligation:

(28) DependencyGraphProof (EQUIVALENT transformation)

(29) TRUE