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

(0) Obligation:

Clauses:

insert(X, void, tree(X, void, void)).
insert(X, tree(X, Left, Right), tree(X, Left, Right)).
insert(X, tree(Y, Left, Right), tree(Y, Left1, Right)) :- ','(less(X, Y), insert(X, Left, Left1)).
insert(X, tree(Y, Left, Right), tree(Y, Left, Right1)) :- ','(less(Y, X), insert(X, Right, Right1)).
less(0, s(X1)).
less(s(X), s(Y)) :- less(X, Y).

Query: insert(a,g,a)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="3: insert(T1, T2, T3)\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 0\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(less(T49, T45), insert(T49, T46, T50))\n\nT45 is ground\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: less(T49, T45)\n\nT45 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: insert(T53, T46, T54)\n\nT46 is ground\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: less(T49, T45), SCOPE: 2, CLAUSE: 4 | less(T49, T45), SCOPE: 2, CLAUSE: 5\n\nT45 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: less(T49, T45), SCOPE: 2, CLAUSE: 4\n\nT45 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: less(T49, T45), SCOPE: 2, CLAUSE: 5\n\nT45 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: less(T68, T67)\n\nT67 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: insert(T53, T46, T54), SCOPE: 3, CLAUSE: 0 | insert(T53, T46, T54), SCOPE: 3, CLAUSE: 1 | insert(T53, T46, T54), SCOPE: 3, CLAUSE: 2 | insert(T53, T46, T54), SCOPE: 3, CLAUSE: 3\n\nT46 is ground\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: insert(T53, T46, T54), SCOPE: 3, CLAUSE: 0\n\nT46 is ground\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: insert(T53, T46, T54), SCOPE: 3, CLAUSE: 1 | insert(T53, T46, T54), SCOPE: 3, CLAUSE: 2 | insert(T53, T46, T54), SCOPE: 3, CLAUSE: 3\n\nT46 is ground\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: insert(T53, T46, T54), SCOPE: 3, CLAUSE: 1\n\nT46 is ground\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: insert(T53, T46, T54), SCOPE: 3, CLAUSE: 2 | insert(T53, T46, T54), SCOPE: 3, CLAUSE: 3\n\nT46 is ground\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: insert(T53, T46, T54), SCOPE: 3, CLAUSE: 2\n\nT46 is ground\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: insert(T53, T46, T54), SCOPE: 3, CLAUSE: 3\n\nT46 is ground\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: ','(less(T113, T114), insert(T113, T115, T118))\n\nT113 is ground\nT114 is ground\nT115 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: less(T113, T114)\n\nT113 is ground\nT114 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: insert(T113, T115, T118)\n\nT113 is ground\nT115 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: less(T113, T114), SCOPE: 4, CLAUSE: 4 | less(T113, T114), SCOPE: 4, CLAUSE: 5\n\nT113 is ground\nT114 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: less(T113, T114), SCOPE: 4, CLAUSE: 4\n\nT113 is ground\nT114 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: less(T113, T114), SCOPE: 4, CLAUSE: 5\n\nT113 is ground\nT114 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: less(T132, T133)\n\nT132 is ground\nT133 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: ','(less(T149, T148), insert(T148, T151, T153))\n\nT148 is ground\nT149 is ground\nT151 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: less(T149, T148)\n\nT148 is ground\nT149 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: insert(T148, T151, T153)\n\nT148 is ground\nT151 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: ','(less(T171, T175), insert(T175, T173, T176))\n\nT171 is ground\nT173 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: less(T171, T175)\n\nT171 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: insert(T179, T173, T180)\n\nT173 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
230 [label="230: less(T171, T175), SCOPE: 5, CLAUSE: 4 | less(T171, T175), SCOPE: 5, CLAUSE: 5\n\nT171 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="231: less(T171, T175), SCOPE: 5, CLAUSE: 4\n\nT171 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: less(T171, T175), SCOPE: 5, CLAUSE: 5\n\nT171 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
236 [label="236: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
237 [label="237: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
240 [label="240: less(T192, T194)\n\nT192 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
241 [label="241: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
242 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 242 [arrowhead = none ];
242 -> 4;

243 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 243 [arrowhead = none ];
243 -> 7;

244 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 244 [arrowhead = none ];
244 -> 8;

245 [label="EVAL with clause\ninsert(X6, void, tree(X6, void, void)).\nand substitutionT1 -> T8,\nX6 -> T8,\nT2 -> void,\nT3 -> tree(T8, void, void)", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 245 [arrowhead = none ];
245 -> 10;

246 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
7 -> 246 [arrowhead = none ];
246 -> 11;

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

248 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
8 -> 248 [arrowhead = none ];
248 -> 17;

249 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 249 [arrowhead = none ];
249 -> 12;

250 [label="EVAL with clause\ninsert(X19, tree(X19, X20, X21), tree(X19, X20, X21)).\nand substitutionT1 -> T21,\nX19 -> T21,\nX20 -> T22,\nX21 -> T23,\nT2 -> tree(T21, T22, T23),\nT3 -> tree(T21, T22, T23)", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 250 [arrowhead = none ];
250 -> 25;

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

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

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

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

255 [label="EVAL with clause\ninsert(X42, tree(X43, X44, X45), tree(X43, X46, X45)) :- ','(less(X42, X43), insert(X42, X44, X46)).\nand substitutionT1 -> T49,\nX42 -> T49,\nX43 -> T45,\nX44 -> T46,\nX45 -> T47,\nT2 -> tree(T45, T46, T47),\nX46 -> T50,\nT3 -> tree(T45, T50, T47),\nT44 -> T49,\nT48 -> T50", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 255 [arrowhead = none ];
255 -> 38;

256 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 256 [arrowhead = none ];
256 -> 40;

257 [label="EVAL with clause\ninsert(X161, tree(X162, X163, X164), tree(X162, X163, X165)) :- ','(less(X162, X161), insert(X161, X164, X165)).\nand substitutionT1 -> T175,\nX161 -> T175,\nX162 -> T171,\nX163 -> T172,\nX164 -> T173,\nT2 -> tree(T171, T172, T173),\nX165 -> T176,\nT3 -> tree(T171, T172, T176),\nT170 -> T175,\nT174 -> T176", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 257 [arrowhead = none ];
257 -> 205;

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

259 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
38 -> 259 [arrowhead = none ];
259 -> 59;

260 [label="SPLIT 2\nnew knowledge:\nT53 is ground\nT45 is ground\nreplacements:T49 -> T53,\nT50 -> T54", fontsize=14, style = filled, fillcolor = violet];
38 -> 260 [arrowhead = none ];
260 -> 60;

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

262 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
60 -> 262 [arrowhead = none ];
262 -> 100;

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

264 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
71 -> 264 [arrowhead = none ];
264 -> 73;

265 [label="EVAL with clause\nless(0, s(X55)).\nand substitutionT49 -> 0,\nX55 -> T61,\nT45 -> s(T61)", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 265 [arrowhead = none ];
265 -> 77;

266 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
72 -> 266 [arrowhead = none ];
266 -> 78;

267 [label="EVAL with clause\nless(s(X60), s(X61)) :- less(X60, X61).\nand substitutionX60 -> T68,\nT49 -> s(T68),\nX61 -> T67,\nT45 -> s(T67),\nT66 -> T68", fontsize=14, style = filled, fillcolor = lightblue];
73 -> 267 [arrowhead = none ];
267 -> 91;

268 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
73 -> 268 [arrowhead = none ];
268 -> 92;

269 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
77 -> 269 [arrowhead = none ];
269 -> 79;

270 [label="INSTANCE with matching:\nT49 -> T68\nT45 -> T67", fontsize=14, style = filled, fillcolor = lightgrey];
91 -> 270 [arrowhead = none , style=dashed];
270 -> 59[style=dashed];

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

272 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
100 -> 272 [arrowhead = none ];
272 -> 102;

273 [label="EVAL with clause\ninsert(X70, void, tree(X70, void, void)).\nand substitutionT53 -> T77,\nX70 -> T77,\nT46 -> void,\nT54 -> tree(T77, void, void)", fontsize=14, style = filled, fillcolor = lightblue];
101 -> 273 [arrowhead = none ];
273 -> 103;

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

275 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
102 -> 275 [arrowhead = none ];
275 -> 107;

276 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
102 -> 276 [arrowhead = none ];
276 -> 108;

277 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
103 -> 277 [arrowhead = none ];
277 -> 105;

278 [label="EVAL with clause\ninsert(X83, tree(X83, X84, X85), tree(X83, X84, X85)).\nand substitutionT53 -> T90,\nX83 -> T90,\nX84 -> T91,\nX85 -> T92,\nT46 -> tree(T90, T91, T92),\nT54 -> tree(T90, T91, T92)", fontsize=14, style = filled, fillcolor = lightblue];
107 -> 278 [arrowhead = none ];
278 -> 112;

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

280 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
108 -> 280 [arrowhead = none ];
280 -> 131;

281 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
108 -> 281 [arrowhead = none ];
281 -> 132;

282 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
112 -> 282 [arrowhead = none ];
282 -> 128;

283 [label="EVAL with clause\ninsert(X106, tree(X107, X108, X109), tree(X107, X110, X109)) :- ','(less(X106, X107), insert(X106, X108, X110)).\nand substitutionT53 -> T113,\nX106 -> T113,\nX107 -> T114,\nX108 -> T115,\nX109 -> T116,\nT46 -> tree(T114, T115, T116),\nX110 -> T118,\nT54 -> tree(T114, T118, T116),\nT117 -> T118", fontsize=14, style = filled, fillcolor = lightblue];
131 -> 283 [arrowhead = none ];
283 -> 137;

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

285 [label="EVAL with clause\ninsert(X140, tree(X141, X142, X143), tree(X141, X142, X144)) :- ','(less(X141, X140), insert(X140, X143, X144)).\nand substitutionT53 -> T148,\nX140 -> T148,\nX141 -> T149,\nX142 -> T150,\nX143 -> T151,\nT46 -> tree(T149, T150, T151),\nX144 -> T153,\nT54 -> tree(T149, T150, T153),\nT152 -> T153", fontsize=14, style = filled, fillcolor = lightblue];
132 -> 285 [arrowhead = none ];
285 -> 167;

286 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
132 -> 286 [arrowhead = none ];
286 -> 168;

287 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
137 -> 287 [arrowhead = none ];
287 -> 141;

288 [label="SPLIT 2\nnew knowledge:\nT113 is ground\nT114 is ground", fontsize=14, style = filled, fillcolor = violet];
137 -> 288 [arrowhead = none ];
288 -> 142;

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

290 [label="INSTANCE with matching:\nT53 -> T113\nT46 -> T115\nT54 -> T118", fontsize=14, style = filled, fillcolor = lightgrey];
142 -> 290 [arrowhead = none , style=dashed];
290 -> 60[style=dashed];

291 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
145 -> 291 [arrowhead = none ];
291 -> 146;

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

293 [label="EVAL with clause\nless(0, s(X119)).\nand substitutionT113 -> 0,\nX119 -> T127,\nT114 -> s(T127)", fontsize=14, style = filled, fillcolor = lightblue];
146 -> 293 [arrowhead = none ];
293 -> 149;

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

295 [label="EVAL with clause\nless(s(X124), s(X125)) :- less(X124, X125).\nand substitutionX124 -> T132,\nT113 -> s(T132),\nX125 -> T133,\nT114 -> s(T133)", fontsize=14, style = filled, fillcolor = lightblue];
148 -> 295 [arrowhead = none ];
295 -> 155;

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

297 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
149 -> 297 [arrowhead = none ];
297 -> 151;

298 [label="INSTANCE with matching:\nT113 -> T132\nT114 -> T133", fontsize=14, style = filled, fillcolor = lightgrey];
155 -> 298 [arrowhead = none , style=dashed];
298 -> 141[style=dashed];

299 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
167 -> 299 [arrowhead = none ];
299 -> 170;

300 [label="SPLIT 2\nnew knowledge:\nT149 is ground\nT148 is ground", fontsize=14, style = filled, fillcolor = violet];
167 -> 300 [arrowhead = none ];
300 -> 171;

301 [label="INSTANCE with matching:\nT113 -> T149\nT114 -> T148", fontsize=14, style = filled, fillcolor = lightgrey];
170 -> 301 [arrowhead = none , style=dashed];
301 -> 141[style=dashed];

302 [label="INSTANCE with matching:\nT53 -> T148\nT46 -> T151\nT54 -> T153", fontsize=14, style = filled, fillcolor = lightgrey];
171 -> 302 [arrowhead = none , style=dashed];
302 -> 60[style=dashed];

303 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
205 -> 303 [arrowhead = none ];
303 -> 213;

304 [label="SPLIT 2\nnew knowledge:\nT171 is ground\nreplacements:T175 -> T179,\nT176 -> T180", fontsize=14, style = filled, fillcolor = violet];
205 -> 304 [arrowhead = none ];
304 -> 214;

305 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
213 -> 305 [arrowhead = none ];
305 -> 230;

306 [label="INSTANCE with matching:\nT1 -> T179\nT2 -> T173\nT3 -> T180", fontsize=14, style = filled, fillcolor = lightgrey];
214 -> 306 [arrowhead = none , style=dashed];
306 -> 3[style=dashed];

307 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
230 -> 307 [arrowhead = none ];
307 -> 231;

308 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
230 -> 308 [arrowhead = none ];
308 -> 232;

309 [label="EVAL with clause\nless(0, s(X174)).\nand substitutionT171 -> 0,\nX174 -> T187,\nT175 -> s(T187)", fontsize=14, style = filled, fillcolor = lightblue];
231 -> 309 [arrowhead = none ];
309 -> 235;

310 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
231 -> 310 [arrowhead = none ];
310 -> 236;

311 [label="EVAL with clause\nless(s(X179), s(X180)) :- less(X179, X180).\nand substitutionX179 -> T192,\nT171 -> s(T192),\nX180 -> T194,\nT175 -> s(T194),\nT193 -> T194", fontsize=14, style = filled, fillcolor = lightblue];
232 -> 311 [arrowhead = none ];
311 -> 240;

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

313 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
235 -> 313 [arrowhead = none ];
313 -> 237;

314 [label="INSTANCE with matching:\nT171 -> T192\nT175 -> T194", fontsize=14, style = filled, fillcolor = lightgrey];
240 -> 314 [arrowhead = none , style=dashed];
314 -> 213[style=dashed];

}

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

f3_in(void) → f3_out1
f3_in(tree(T21, T22, T23)) → f3_out1
f3_in(tree(T45, T46, T47)) → U1(f38_in(T45, T46), tree(T45, T46, T47))
U1(f38_out1(T49, T50), tree(T45, T46, T47)) → f3_out1
f3_in(tree(T171, T172, T173)) → U2(f205_in(T171, T173), tree(T171, T172, T173))
U2(f205_out1, tree(T171, T172, T173)) → f3_out1
f59_in(s(T61)) → f59_out1(0)
f59_in(s(T67)) → U3(f59_in(T67), s(T67))
U3(f59_out1(T68), s(T67)) → f59_out1(s(T68))
f60_in(T77, void) → f60_out1(tree(T77, void, void))
f60_in(T90, tree(T90, T91, T92)) → f60_out1(tree(T90, T91, T92))
f60_in(T113, tree(T114, T115, T116)) → U4(f137_in(T113, T114, T115), T113, tree(T114, T115, T116))
U4(f137_out1(T118), T113, tree(T114, T115, T116)) → f60_out1(tree(T114, T118, T116))
f60_in(T148, tree(T149, T150, T151)) → U5(f167_in(T149, T148, T151), T148, tree(T149, T150, T151))
U5(f167_out1(T153), T148, tree(T149, T150, T151)) → f60_out1(tree(T149, T150, T153))
f141_in(0, s(T127)) → f141_out1
f141_in(s(T132), s(T133)) → U6(f141_in(T132, T133), s(T132), s(T133))
U6(f141_out1, s(T132), s(T133)) → f141_out1
f213_in(0) → f213_out1
f213_in(s(T192)) → U7(f213_in(T192), s(T192))
U7(f213_out1, s(T192)) → f213_out1
f38_in(T45, T46) → U8(f59_in(T45), T45, T46)
U8(f59_out1(T53), T45, T46) → U9(f60_in(T53, T46), T45, T46, T53)
U9(f60_out1(T54), T45, T46, T53) → f38_out1(T53, T54)
f137_in(T113, T114, T115) → U10(f141_in(T113, T114), T113, T114, T115)
U10(f141_out1, T113, T114, T115) → U11(f60_in(T113, T115), T113, T114, T115)
U11(f60_out1(T118), T113, T114, T115) → f137_out1(T118)
f167_in(T149, T148, T151) → U12(f141_in(T149, T148), T149, T148, T151)
U12(f141_out1, T149, T148, T151) → U13(f60_in(T148, T151), T149, T148, T151)
U13(f60_out1(T153), T149, T148, T151) → f167_out1(T153)
f205_in(T171, T173) → U14(f213_in(T171), T171, T173)
U14(f213_out1, T171, T173) → U15(f3_in(T173), T171, T173)
U15(f3_out1, T171, T173) → f205_out1

Q is empty.

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(4) Obligation:

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

F3_IN(tree(T45, T46, T47)) → U1¹(f38_in(T45, T46), tree(T45, T46, T47))
F3_IN(tree(T45, T46, T47)) → F38_IN(T45, T46)
F3_IN(tree(T171, T172, T173)) → U2¹(f205_in(T171, T173), tree(T171, T172, T173))
F3_IN(tree(T171, T172, T173)) → F205_IN(T171, T173)
F59_IN(s(T67)) → U3¹(f59_in(T67), s(T67))
F59_IN(s(T67)) → F59_IN(T67)
F60_IN(T113, tree(T114, T115, T116)) → U4¹(f137_in(T113, T114, T115), T113, tree(T114, T115, T116))
F60_IN(T113, tree(T114, T115, T116)) → F137_IN(T113, T114, T115)
F60_IN(T148, tree(T149, T150, T151)) → U5¹(f167_in(T149, T148, T151), T148, tree(T149, T150, T151))
F60_IN(T148, tree(T149, T150, T151)) → F167_IN(T149, T148, T151)
F141_IN(s(T132), s(T133)) → U6¹(f141_in(T132, T133), s(T132), s(T133))
F141_IN(s(T132), s(T133)) → F141_IN(T132, T133)
F213_IN(s(T192)) → U7¹(f213_in(T192), s(T192))
F213_IN(s(T192)) → F213_IN(T192)
F38_IN(T45, T46) → U8¹(f59_in(T45), T45, T46)
F38_IN(T45, T46) → F59_IN(T45)
U8¹(f59_out1(T53), T45, T46) → U9¹(f60_in(T53, T46), T45, T46, T53)
U8¹(f59_out1(T53), T45, T46) → F60_IN(T53, T46)
F137_IN(T113, T114, T115) → U10¹(f141_in(T113, T114), T113, T114, T115)
F137_IN(T113, T114, T115) → F141_IN(T113, T114)
U10¹(f141_out1, T113, T114, T115) → U11¹(f60_in(T113, T115), T113, T114, T115)
U10¹(f141_out1, T113, T114, T115) → F60_IN(T113, T115)
F167_IN(T149, T148, T151) → U12¹(f141_in(T149, T148), T149, T148, T151)
F167_IN(T149, T148, T151) → F141_IN(T149, T148)
U12¹(f141_out1, T149, T148, T151) → U13¹(f60_in(T148, T151), T149, T148, T151)
U12¹(f141_out1, T149, T148, T151) → F60_IN(T148, T151)
F205_IN(T171, T173) → U14¹(f213_in(T171), T171, T173)
F205_IN(T171, T173) → F213_IN(T171)
U14¹(f213_out1, T171, T173) → U15¹(f3_in(T173), T171, T173)
U14¹(f213_out1, T171, T173) → F3_IN(T173)

The TRS R consists of the following rules:

f3_in(void) → f3_out1
f3_in(tree(T21, T22, T23)) → f3_out1
f3_in(tree(T45, T46, T47)) → U1(f38_in(T45, T46), tree(T45, T46, T47))
U1(f38_out1(T49, T50), tree(T45, T46, T47)) → f3_out1
f3_in(tree(T171, T172, T173)) → U2(f205_in(T171, T173), tree(T171, T172, T173))
U2(f205_out1, tree(T171, T172, T173)) → f3_out1
f59_in(s(T61)) → f59_out1(0)
f59_in(s(T67)) → U3(f59_in(T67), s(T67))
U3(f59_out1(T68), s(T67)) → f59_out1(s(T68))
f60_in(T77, void) → f60_out1(tree(T77, void, void))
f60_in(T90, tree(T90, T91, T92)) → f60_out1(tree(T90, T91, T92))
f60_in(T113, tree(T114, T115, T116)) → U4(f137_in(T113, T114, T115), T113, tree(T114, T115, T116))
U4(f137_out1(T118), T113, tree(T114, T115, T116)) → f60_out1(tree(T114, T118, T116))
f60_in(T148, tree(T149, T150, T151)) → U5(f167_in(T149, T148, T151), T148, tree(T149, T150, T151))
U5(f167_out1(T153), T148, tree(T149, T150, T151)) → f60_out1(tree(T149, T150, T153))
f141_in(0, s(T127)) → f141_out1
f141_in(s(T132), s(T133)) → U6(f141_in(T132, T133), s(T132), s(T133))
U6(f141_out1, s(T132), s(T133)) → f141_out1
f213_in(0) → f213_out1
f213_in(s(T192)) → U7(f213_in(T192), s(T192))
U7(f213_out1, s(T192)) → f213_out1
f38_in(T45, T46) → U8(f59_in(T45), T45, T46)
U8(f59_out1(T53), T45, T46) → U9(f60_in(T53, T46), T45, T46, T53)
U9(f60_out1(T54), T45, T46, T53) → f38_out1(T53, T54)
f137_in(T113, T114, T115) → U10(f141_in(T113, T114), T113, T114, T115)
U10(f141_out1, T113, T114, T115) → U11(f60_in(T113, T115), T113, T114, T115)
U11(f60_out1(T118), T113, T114, T115) → f137_out1(T118)
f167_in(T149, T148, T151) → U12(f141_in(T149, T148), T149, T148, T151)
U12(f141_out1, T149, T148, T151) → U13(f60_in(T148, T151), T149, T148, T151)
U13(f60_out1(T153), T149, T148, T151) → f167_out1(T153)
f205_in(T171, T173) → U14(f213_in(T171), T171, T173)
U14(f213_out1, T171, T173) → U15(f3_in(T173), T171, T173)
U15(f3_out1, T171, T173) → f205_out1

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

F213_IN(s(T192)) → F213_IN(T192)

The TRS R consists of the following rules:

f3_in(void) → f3_out1
f3_in(tree(T21, T22, T23)) → f3_out1
f3_in(tree(T45, T46, T47)) → U1(f38_in(T45, T46), tree(T45, T46, T47))
U1(f38_out1(T49, T50), tree(T45, T46, T47)) → f3_out1
f3_in(tree(T171, T172, T173)) → U2(f205_in(T171, T173), tree(T171, T172, T173))
U2(f205_out1, tree(T171, T172, T173)) → f3_out1
f59_in(s(T61)) → f59_out1(0)
f59_in(s(T67)) → U3(f59_in(T67), s(T67))
U3(f59_out1(T68), s(T67)) → f59_out1(s(T68))
f60_in(T77, void) → f60_out1(tree(T77, void, void))
f60_in(T90, tree(T90, T91, T92)) → f60_out1(tree(T90, T91, T92))
f60_in(T113, tree(T114, T115, T116)) → U4(f137_in(T113, T114, T115), T113, tree(T114, T115, T116))
U4(f137_out1(T118), T113, tree(T114, T115, T116)) → f60_out1(tree(T114, T118, T116))
f60_in(T148, tree(T149, T150, T151)) → U5(f167_in(T149, T148, T151), T148, tree(T149, T150, T151))
U5(f167_out1(T153), T148, tree(T149, T150, T151)) → f60_out1(tree(T149, T150, T153))
f141_in(0, s(T127)) → f141_out1
f141_in(s(T132), s(T133)) → U6(f141_in(T132, T133), s(T132), s(T133))
U6(f141_out1, s(T132), s(T133)) → f141_out1
f213_in(0) → f213_out1
f213_in(s(T192)) → U7(f213_in(T192), s(T192))
U7(f213_out1, s(T192)) → f213_out1
f38_in(T45, T46) → U8(f59_in(T45), T45, T46)
U8(f59_out1(T53), T45, T46) → U9(f60_in(T53, T46), T45, T46, T53)
U9(f60_out1(T54), T45, T46, T53) → f38_out1(T53, T54)
f137_in(T113, T114, T115) → U10(f141_in(T113, T114), T113, T114, T115)
U10(f141_out1, T113, T114, T115) → U11(f60_in(T113, T115), T113, T114, T115)
U11(f60_out1(T118), T113, T114, T115) → f137_out1(T118)
f167_in(T149, T148, T151) → U12(f141_in(T149, T148), T149, T148, T151)
U12(f141_out1, T149, T148, T151) → U13(f60_in(T148, T151), T149, T148, T151)
U13(f60_out1(T153), T149, T148, T151) → f167_out1(T153)
f205_in(T171, T173) → U14(f213_in(T171), T171, T173)
U14(f213_out1, T171, T173) → U15(f3_in(T173), T171, T173)
U15(f3_out1, T171, T173) → f205_out1

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

(8) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(9) Obligation:

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

F213_IN(s(T192)) → F213_IN(T192)

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

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

• F213_IN(s(T192)) → F213_IN(T192)
  The graph contains the following edges 1 > 1

(11) YES

(12) Obligation:

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

F141_IN(s(T132), s(T133)) → F141_IN(T132, T133)

The TRS R consists of the following rules:

f3_in(void) → f3_out1
f3_in(tree(T21, T22, T23)) → f3_out1
f3_in(tree(T45, T46, T47)) → U1(f38_in(T45, T46), tree(T45, T46, T47))
U1(f38_out1(T49, T50), tree(T45, T46, T47)) → f3_out1
f3_in(tree(T171, T172, T173)) → U2(f205_in(T171, T173), tree(T171, T172, T173))
U2(f205_out1, tree(T171, T172, T173)) → f3_out1
f59_in(s(T61)) → f59_out1(0)
f59_in(s(T67)) → U3(f59_in(T67), s(T67))
U3(f59_out1(T68), s(T67)) → f59_out1(s(T68))
f60_in(T77, void) → f60_out1(tree(T77, void, void))
f60_in(T90, tree(T90, T91, T92)) → f60_out1(tree(T90, T91, T92))
f60_in(T113, tree(T114, T115, T116)) → U4(f137_in(T113, T114, T115), T113, tree(T114, T115, T116))
U4(f137_out1(T118), T113, tree(T114, T115, T116)) → f60_out1(tree(T114, T118, T116))
f60_in(T148, tree(T149, T150, T151)) → U5(f167_in(T149, T148, T151), T148, tree(T149, T150, T151))
U5(f167_out1(T153), T148, tree(T149, T150, T151)) → f60_out1(tree(T149, T150, T153))
f141_in(0, s(T127)) → f141_out1
f141_in(s(T132), s(T133)) → U6(f141_in(T132, T133), s(T132), s(T133))
U6(f141_out1, s(T132), s(T133)) → f141_out1
f213_in(0) → f213_out1
f213_in(s(T192)) → U7(f213_in(T192), s(T192))
U7(f213_out1, s(T192)) → f213_out1
f38_in(T45, T46) → U8(f59_in(T45), T45, T46)
U8(f59_out1(T53), T45, T46) → U9(f60_in(T53, T46), T45, T46, T53)
U9(f60_out1(T54), T45, T46, T53) → f38_out1(T53, T54)
f137_in(T113, T114, T115) → U10(f141_in(T113, T114), T113, T114, T115)
U10(f141_out1, T113, T114, T115) → U11(f60_in(T113, T115), T113, T114, T115)
U11(f60_out1(T118), T113, T114, T115) → f137_out1(T118)
f167_in(T149, T148, T151) → U12(f141_in(T149, T148), T149, T148, T151)
U12(f141_out1, T149, T148, T151) → U13(f60_in(T148, T151), T149, T148, T151)
U13(f60_out1(T153), T149, T148, T151) → f167_out1(T153)
f205_in(T171, T173) → U14(f213_in(T171), T171, T173)
U14(f213_out1, T171, T173) → U15(f3_in(T173), T171, T173)
U15(f3_out1, T171, T173) → f205_out1

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

(13) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(14) Obligation:

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

F141_IN(s(T132), s(T133)) → F141_IN(T132, T133)

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

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

• F141_IN(s(T132), s(T133)) → F141_IN(T132, T133)
  The graph contains the following edges 1 > 1, 2 > 2

(16) YES

(17) Obligation:

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

F60_IN(T113, tree(T114, T115, T116)) → F137_IN(T113, T114, T115)
F137_IN(T113, T114, T115) → U10¹(f141_in(T113, T114), T113, T114, T115)
U10¹(f141_out1, T113, T114, T115) → F60_IN(T113, T115)
F60_IN(T148, tree(T149, T150, T151)) → F167_IN(T149, T148, T151)
F167_IN(T149, T148, T151) → U12¹(f141_in(T149, T148), T149, T148, T151)
U12¹(f141_out1, T149, T148, T151) → F60_IN(T148, T151)

The TRS R consists of the following rules:

f3_in(void) → f3_out1
f3_in(tree(T21, T22, T23)) → f3_out1
f3_in(tree(T45, T46, T47)) → U1(f38_in(T45, T46), tree(T45, T46, T47))
U1(f38_out1(T49, T50), tree(T45, T46, T47)) → f3_out1
f3_in(tree(T171, T172, T173)) → U2(f205_in(T171, T173), tree(T171, T172, T173))
U2(f205_out1, tree(T171, T172, T173)) → f3_out1
f59_in(s(T61)) → f59_out1(0)
f59_in(s(T67)) → U3(f59_in(T67), s(T67))
U3(f59_out1(T68), s(T67)) → f59_out1(s(T68))
f60_in(T77, void) → f60_out1(tree(T77, void, void))
f60_in(T90, tree(T90, T91, T92)) → f60_out1(tree(T90, T91, T92))
f60_in(T113, tree(T114, T115, T116)) → U4(f137_in(T113, T114, T115), T113, tree(T114, T115, T116))
U4(f137_out1(T118), T113, tree(T114, T115, T116)) → f60_out1(tree(T114, T118, T116))
f60_in(T148, tree(T149, T150, T151)) → U5(f167_in(T149, T148, T151), T148, tree(T149, T150, T151))
U5(f167_out1(T153), T148, tree(T149, T150, T151)) → f60_out1(tree(T149, T150, T153))
f141_in(0, s(T127)) → f141_out1
f141_in(s(T132), s(T133)) → U6(f141_in(T132, T133), s(T132), s(T133))
U6(f141_out1, s(T132), s(T133)) → f141_out1
f213_in(0) → f213_out1
f213_in(s(T192)) → U7(f213_in(T192), s(T192))
U7(f213_out1, s(T192)) → f213_out1
f38_in(T45, T46) → U8(f59_in(T45), T45, T46)
U8(f59_out1(T53), T45, T46) → U9(f60_in(T53, T46), T45, T46, T53)
U9(f60_out1(T54), T45, T46, T53) → f38_out1(T53, T54)
f137_in(T113, T114, T115) → U10(f141_in(T113, T114), T113, T114, T115)
U10(f141_out1, T113, T114, T115) → U11(f60_in(T113, T115), T113, T114, T115)
U11(f60_out1(T118), T113, T114, T115) → f137_out1(T118)
f167_in(T149, T148, T151) → U12(f141_in(T149, T148), T149, T148, T151)
U12(f141_out1, T149, T148, T151) → U13(f60_in(T148, T151), T149, T148, T151)
U13(f60_out1(T153), T149, T148, T151) → f167_out1(T153)
f205_in(T171, T173) → U14(f213_in(T171), T171, T173)
U14(f213_out1, T171, T173) → U15(f3_in(T173), T171, T173)
U15(f3_out1, T171, T173) → f205_out1

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

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

• F137_IN(T113, T114, T115) → U10¹(f141_in(T113, T114), T113, T114, T115)
  The graph contains the following edges 1 >= 2, 2 >= 3, 3 >= 4

• U10¹(f141_out1, T113, T114, T115) → F60_IN(T113, T115)
  The graph contains the following edges 2 >= 1, 4 >= 2

• U12¹(f141_out1, T149, T148, T151) → F60_IN(T148, T151)
  The graph contains the following edges 3 >= 1, 4 >= 2

• F60_IN(T113, tree(T114, T115, T116)) → F137_IN(T113, T114, T115)
  The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

• F60_IN(T148, tree(T149, T150, T151)) → F167_IN(T149, T148, T151)
  The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3

• F167_IN(T149, T148, T151) → U12¹(f141_in(T149, T148), T149, T148, T151)
  The graph contains the following edges 1 >= 2, 2 >= 3, 3 >= 4

(19) YES

(20) Obligation:

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

F59_IN(s(T67)) → F59_IN(T67)

The TRS R consists of the following rules:

f3_in(void) → f3_out1
f3_in(tree(T21, T22, T23)) → f3_out1
f3_in(tree(T45, T46, T47)) → U1(f38_in(T45, T46), tree(T45, T46, T47))
U1(f38_out1(T49, T50), tree(T45, T46, T47)) → f3_out1
f3_in(tree(T171, T172, T173)) → U2(f205_in(T171, T173), tree(T171, T172, T173))
U2(f205_out1, tree(T171, T172, T173)) → f3_out1
f59_in(s(T61)) → f59_out1(0)
f59_in(s(T67)) → U3(f59_in(T67), s(T67))
U3(f59_out1(T68), s(T67)) → f59_out1(s(T68))
f60_in(T77, void) → f60_out1(tree(T77, void, void))
f60_in(T90, tree(T90, T91, T92)) → f60_out1(tree(T90, T91, T92))
f60_in(T113, tree(T114, T115, T116)) → U4(f137_in(T113, T114, T115), T113, tree(T114, T115, T116))
U4(f137_out1(T118), T113, tree(T114, T115, T116)) → f60_out1(tree(T114, T118, T116))
f60_in(T148, tree(T149, T150, T151)) → U5(f167_in(T149, T148, T151), T148, tree(T149, T150, T151))
U5(f167_out1(T153), T148, tree(T149, T150, T151)) → f60_out1(tree(T149, T150, T153))
f141_in(0, s(T127)) → f141_out1
f141_in(s(T132), s(T133)) → U6(f141_in(T132, T133), s(T132), s(T133))
U6(f141_out1, s(T132), s(T133)) → f141_out1
f213_in(0) → f213_out1
f213_in(s(T192)) → U7(f213_in(T192), s(T192))
U7(f213_out1, s(T192)) → f213_out1
f38_in(T45, T46) → U8(f59_in(T45), T45, T46)
U8(f59_out1(T53), T45, T46) → U9(f60_in(T53, T46), T45, T46, T53)
U9(f60_out1(T54), T45, T46, T53) → f38_out1(T53, T54)
f137_in(T113, T114, T115) → U10(f141_in(T113, T114), T113, T114, T115)
U10(f141_out1, T113, T114, T115) → U11(f60_in(T113, T115), T113, T114, T115)
U11(f60_out1(T118), T113, T114, T115) → f137_out1(T118)
f167_in(T149, T148, T151) → U12(f141_in(T149, T148), T149, T148, T151)
U12(f141_out1, T149, T148, T151) → U13(f60_in(T148, T151), T149, T148, T151)
U13(f60_out1(T153), T149, T148, T151) → f167_out1(T153)
f205_in(T171, T173) → U14(f213_in(T171), T171, T173)
U14(f213_out1, T171, T173) → U15(f3_in(T173), T171, T173)
U15(f3_out1, T171, T173) → f205_out1

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

(21) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(22) Obligation:

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

F59_IN(s(T67)) → F59_IN(T67)

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

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

• F59_IN(s(T67)) → F59_IN(T67)
  The graph contains the following edges 1 > 1

(24) YES

(25) Obligation:

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

F3_IN(tree(T171, T172, T173)) → F205_IN(T171, T173)
F205_IN(T171, T173) → U14¹(f213_in(T171), T171, T173)
U14¹(f213_out1, T171, T173) → F3_IN(T173)

The TRS R consists of the following rules:

f3_in(void) → f3_out1
f3_in(tree(T21, T22, T23)) → f3_out1
f3_in(tree(T45, T46, T47)) → U1(f38_in(T45, T46), tree(T45, T46, T47))
U1(f38_out1(T49, T50), tree(T45, T46, T47)) → f3_out1
f3_in(tree(T171, T172, T173)) → U2(f205_in(T171, T173), tree(T171, T172, T173))
U2(f205_out1, tree(T171, T172, T173)) → f3_out1
f59_in(s(T61)) → f59_out1(0)
f59_in(s(T67)) → U3(f59_in(T67), s(T67))
U3(f59_out1(T68), s(T67)) → f59_out1(s(T68))
f60_in(T77, void) → f60_out1(tree(T77, void, void))
f60_in(T90, tree(T90, T91, T92)) → f60_out1(tree(T90, T91, T92))
f60_in(T113, tree(T114, T115, T116)) → U4(f137_in(T113, T114, T115), T113, tree(T114, T115, T116))
U4(f137_out1(T118), T113, tree(T114, T115, T116)) → f60_out1(tree(T114, T118, T116))
f60_in(T148, tree(T149, T150, T151)) → U5(f167_in(T149, T148, T151), T148, tree(T149, T150, T151))
U5(f167_out1(T153), T148, tree(T149, T150, T151)) → f60_out1(tree(T149, T150, T153))
f141_in(0, s(T127)) → f141_out1
f141_in(s(T132), s(T133)) → U6(f141_in(T132, T133), s(T132), s(T133))
U6(f141_out1, s(T132), s(T133)) → f141_out1
f213_in(0) → f213_out1
f213_in(s(T192)) → U7(f213_in(T192), s(T192))
U7(f213_out1, s(T192)) → f213_out1
f38_in(T45, T46) → U8(f59_in(T45), T45, T46)
U8(f59_out1(T53), T45, T46) → U9(f60_in(T53, T46), T45, T46, T53)
U9(f60_out1(T54), T45, T46, T53) → f38_out1(T53, T54)
f137_in(T113, T114, T115) → U10(f141_in(T113, T114), T113, T114, T115)
U10(f141_out1, T113, T114, T115) → U11(f60_in(T113, T115), T113, T114, T115)
U11(f60_out1(T118), T113, T114, T115) → f137_out1(T118)
f167_in(T149, T148, T151) → U12(f141_in(T149, T148), T149, T148, T151)
U12(f141_out1, T149, T148, T151) → U13(f60_in(T148, T151), T149, T148, T151)
U13(f60_out1(T153), T149, T148, T151) → f167_out1(T153)
f205_in(T171, T173) → U14(f213_in(T171), T171, T173)
U14(f213_out1, T171, T173) → U15(f3_in(T173), T171, T173)
U15(f3_out1, T171, T173) → f205_out1

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

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

• F205_IN(T171, T173) → U14¹(f213_in(T171), T171, T173)
  The graph contains the following edges 1 >= 2, 2 >= 3

• U14¹(f213_out1, T171, T173) → F3_IN(T173)
  The graph contains the following edges 3 >= 1

• F3_IN(tree(T171, T172, T173)) → F205_IN(T171, T173)
  The graph contains the following edges 1 > 1, 1 > 2

(27) YES