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

(0) Obligation:

Clauses:

delete(X, tree(X, void, Right), Right).
delete(X, tree(X, Left, void), Left).
delete(X, tree(X, Left, Right), tree(Y, Left, Right1)) :- delmin(Right, Y, Right1).
delete(X, tree(Y, Left, Right), tree(Y, Left1, Right)) :- ','(less(X, Y), delete(X, Left, Left1)).
delete(X, tree(Y, Left, Right), tree(Y, Left, Right1)) :- ','(less(Y, X), delete(X, Right, Right1)).
delmin(tree(Y, void, Right), Y, Right).
delmin(tree(X, Left, X1), Y, tree(X, Left1, X2)) :- delmin(Left, Y, Left1).
less(0, s(X3)).
less(s(X), s(Y)) :- less(X, Y).

Query: delete(a,g,a)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="3: delete(T1, T2, T3)\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 0\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: delmin(T46, T49, T50)\n\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: delmin(T46, T49, T50), SCOPE: 2, CLAUSE: 5 | delmin(T46, T49, T50), SCOPE: 2, CLAUSE: 6\n\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: delmin(T46, T49, T50), SCOPE: 2, CLAUSE: 5\n\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: delmin(T46, T49, T50), SCOPE: 2, CLAUSE: 6\n\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: delmin(T78, T83, T84)\n\nT78 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: ','(less(T114, T110), delete(T114, T111, T115))\n\nT110 is ground\nT111 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: less(T114, T110)\n\nT110 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: delete(T118, T111, T119)\n\nT111 is ground\nT118 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: less(T114, T110), SCOPE: 3, CLAUSE: 7 | less(T114, T110), SCOPE: 3, CLAUSE: 8\n\nT110 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: less(T114, T110), SCOPE: 3, CLAUSE: 7\n\nT110 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: less(T114, T110), SCOPE: 3, CLAUSE: 8\n\nT110 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: less(T133, T132)\n\nT132 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: delete(T118, T111, T119), SCOPE: 4, CLAUSE: 0 | delete(T118, T111, T119), SCOPE: 4, CLAUSE: 1 | delete(T118, T111, T119), SCOPE: 4, CLAUSE: 2 | delete(T118, T111, T119), SCOPE: 4, CLAUSE: 3 | delete(T118, T111, T119), SCOPE: 4, CLAUSE: 4\n\nT111 is ground\nT118 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: delete(T118, T111, T119), SCOPE: 4, CLAUSE: 0\n\nT111 is ground\nT118 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: delete(T118, T111, T119), SCOPE: 4, CLAUSE: 1 | delete(T118, T111, T119), SCOPE: 4, CLAUSE: 2 | delete(T118, T111, T119), SCOPE: 4, CLAUSE: 3 | delete(T118, T111, T119), SCOPE: 4, CLAUSE: 4\n\nT111 is ground\nT118 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: delete(T118, T111, T119), SCOPE: 4, CLAUSE: 1\n\nT111 is ground\nT118 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: delete(T118, T111, T119), SCOPE: 4, CLAUSE: 2 | delete(T118, T111, T119), SCOPE: 4, CLAUSE: 3 | delete(T118, T111, T119), SCOPE: 4, CLAUSE: 4\n\nT111 is ground\nT118 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: delete(T118, T111, T119), SCOPE: 4, CLAUSE: 2\n\nT111 is ground\nT118 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: delete(T118, T111, T119), SCOPE: 4, CLAUSE: 3 | delete(T118, T111, T119), SCOPE: 4, CLAUSE: 4\n\nT111 is ground\nT118 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: delmin(T182, T185, T186)\n\nT182 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: delete(T118, T111, T119), SCOPE: 4, CLAUSE: 3\n\nT111 is ground\nT118 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: delete(T118, T111, T119), SCOPE: 4, CLAUSE: 4\n\nT111 is ground\nT118 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="191: ','(less(T211, T212), delete(T211, T213, T216))\n\nT211 is ground\nT212 is ground\nT213 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: less(T211, T212)\n\nT211 is ground\nT212 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: delete(T211, T213, T216)\n\nT211 is ground\nT213 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: less(T211, T212), SCOPE: 5, CLAUSE: 7 | less(T211, T212), SCOPE: 5, CLAUSE: 8\n\nT211 is ground\nT212 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: less(T211, T212), SCOPE: 5, CLAUSE: 7\n\nT211 is ground\nT212 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: less(T211, T212), SCOPE: 5, CLAUSE: 8\n\nT211 is ground\nT212 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: less(T230, T231)\n\nT230 is ground\nT231 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: ','(less(T249, T248), delete(T248, T251, T253))\n\nT248 is ground\nT249 is ground\nT251 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: less(T249, T248)\n\nT248 is ground\nT249 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: delete(T248, T251, T253)\n\nT248 is ground\nT251 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
230 [label="230: ','(less(T273, T277), delete(T277, T275, T278))\n\nT273 is ground\nT275 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="231: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
242 [label="242: less(T273, T277)\n\nT273 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
243 [label="243: delete(T281, T275, T282)\n\nT275 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
245 [label="245: less(T273, T277), SCOPE: 6, CLAUSE: 7 | less(T273, T277), SCOPE: 6, CLAUSE: 8\n\nT273 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
248 [label="248: less(T273, T277), SCOPE: 6, CLAUSE: 7\n\nT273 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
249 [label="249: less(T273, T277), SCOPE: 6, CLAUSE: 8\n\nT273 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
251 [label="251: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
253 [label="253: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
254 [label="254: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
263 [label="263: less(T294, T296)\n\nT294 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
264 [label="264: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
265 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 265 [arrowhead = none ];
265 -> 6;

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

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

268 [label="EVAL with clause\ndelete(X12, tree(X12, void, X13), X13).\nand substitutionT1 -> T12,\nX12 -> T12,\nX13 -> T13,\nT2 -> tree(T12, void, T13),\nT3 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 268 [arrowhead = none ];
268 -> 11;

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

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

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

272 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
11 -> 272 [arrowhead = none ];
272 -> 15;

273 [label="EVAL with clause\ndelete(X22, tree(X22, X23, void), X23).\nand substitutionT1 -> T22,\nX22 -> T22,\nX23 -> T23,\nT2 -> tree(T22, T23, void),\nT3 -> T23", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 273 [arrowhead = none ];
273 -> 26;

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

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

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

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

278 [label="EVAL with clause\ndelete(X44, tree(X44, X45, X46), tree(X47, X45, X48)) :- delmin(X46, X47, X48).\nand substitutionT1 -> T44,\nX44 -> T44,\nX45 -> T45,\nX46 -> T46,\nT2 -> tree(T44, T45, T46),\nX47 -> T49,\nX48 -> T50,\nT3 -> tree(T49, T45, T50),\nT47 -> T49,\nT48 -> T50", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 278 [arrowhead = none ];
278 -> 51;

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

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

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

282 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
51 -> 282 [arrowhead = none ];
282 -> 56;

283 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
56 -> 283 [arrowhead = none ];
283 -> 78;

284 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
56 -> 284 [arrowhead = none ];
284 -> 79;

285 [label="EVAL with clause\ndelmin(tree(X61, void, X62), X61, X62).\nand substitutionX61 -> T63,\nX62 -> T64,\nT46 -> tree(T63, void, T64),\nT49 -> T63,\nT50 -> T64", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 285 [arrowhead = none ];
285 -> 82;

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

287 [label="EVAL with clause\ndelmin(tree(X75, X76, X77), X78, tree(X75, X79, X80)) :- delmin(X76, X78, X79).\nand substitutionX75 -> T77,\nX76 -> T78,\nX77 -> T79,\nT46 -> tree(T77, T78, T79),\nT49 -> T83,\nX78 -> T83,\nX79 -> T84,\nX80 -> T82,\nT50 -> tree(T77, T84, T82),\nT80 -> T83,\nT81 -> T84", fontsize=14, style = filled, fillcolor = lightblue];
79 -> 287 [arrowhead = none ];
287 -> 105;

288 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
79 -> 288 [arrowhead = none ];
288 -> 106;

289 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
82 -> 289 [arrowhead = none ];
289 -> 84;

290 [label="INSTANCE with matching:\nT46 -> T78\nT49 -> T83\nT50 -> T84", fontsize=14, style = filled, fillcolor = lightgrey];
105 -> 290 [arrowhead = none , style=dashed];
290 -> 51[style=dashed];

291 [label="EVAL with clause\ndelete(X105, tree(X106, X107, X108), tree(X106, X109, X108)) :- ','(less(X105, X106), delete(X105, X107, X109)).\nand substitutionT1 -> T114,\nX105 -> T114,\nX106 -> T110,\nX107 -> T111,\nX108 -> T112,\nT2 -> tree(T110, T111, T112),\nX109 -> T115,\nT3 -> tree(T110, T115, T112),\nT109 -> T114,\nT113 -> T115", fontsize=14, style = filled, fillcolor = lightblue];
114 -> 291 [arrowhead = none ];
291 -> 135;

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

293 [label="EVAL with clause\ndelete(X259, tree(X260, X261, X262), tree(X260, X261, X263)) :- ','(less(X260, X259), delete(X259, X262, X263)).\nand substitutionT1 -> T277,\nX259 -> T277,\nX260 -> T273,\nX261 -> T274,\nX262 -> T275,\nT2 -> tree(T273, T274, T275),\nX263 -> T278,\nT3 -> tree(T273, T274, T278),\nT272 -> T277,\nT276 -> T278", fontsize=14, style = filled, fillcolor = lightblue];
116 -> 293 [arrowhead = none ];
293 -> 230;

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

295 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
135 -> 295 [arrowhead = none ];
295 -> 139;

296 [label="SPLIT 2\nnew knowledge:\nT118 is ground\nT110 is ground\nreplacements:T114 -> T118,\nT115 -> T119", fontsize=14, style = filled, fillcolor = violet];
135 -> 296 [arrowhead = none ];
296 -> 140;

297 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
139 -> 297 [arrowhead = none ];
297 -> 148;

298 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
140 -> 298 [arrowhead = none ];
298 -> 161;

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

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

301 [label="EVAL with clause\nless(0, s(X118)).\nand substitutionT114 -> 0,\nX118 -> T126,\nT110 -> s(T126)", fontsize=14, style = filled, fillcolor = lightblue];
149 -> 301 [arrowhead = none ];
301 -> 152;

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

303 [label="EVAL with clause\nless(s(X123), s(X124)) :- less(X123, X124).\nand substitutionX123 -> T133,\nT114 -> s(T133),\nX124 -> T132,\nT110 -> s(T132),\nT131 -> T133", fontsize=14, style = filled, fillcolor = lightblue];
150 -> 303 [arrowhead = none ];
303 -> 156;

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

305 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
152 -> 305 [arrowhead = none ];
305 -> 155;

306 [label="INSTANCE with matching:\nT114 -> T133\nT110 -> T132", fontsize=14, style = filled, fillcolor = lightgrey];
156 -> 306 [arrowhead = none , style=dashed];
306 -> 139[style=dashed];

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

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

309 [label="EVAL with clause\ndelete(X139, tree(X139, void, X140), X140).\nand substitutionT118 -> T148,\nX139 -> T148,\nX140 -> T149,\nT111 -> tree(T148, void, T149),\nT119 -> T149", fontsize=14, style = filled, fillcolor = lightblue];
162 -> 309 [arrowhead = none ];
309 -> 165;

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

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

312 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
163 -> 312 [arrowhead = none ];
312 -> 169;

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

314 [label="EVAL with clause\ndelete(X149, tree(X149, X150, void), X150).\nand substitutionT118 -> T158,\nX149 -> T158,\nX150 -> T159,\nT111 -> tree(T158, T159, void),\nT119 -> T159", fontsize=14, style = filled, fillcolor = lightblue];
168 -> 314 [arrowhead = none ];
314 -> 172;

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

316 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
169 -> 316 [arrowhead = none ];
316 -> 177;

317 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
169 -> 317 [arrowhead = none ];
317 -> 178;

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

319 [label="EVAL with clause\ndelete(X171, tree(X171, X172, X173), tree(X174, X172, X175)) :- delmin(X173, X174, X175).\nand substitutionT118 -> T180,\nX171 -> T180,\nX172 -> T181,\nX173 -> T182,\nT111 -> tree(T180, T181, T182),\nX174 -> T185,\nX175 -> T186,\nT119 -> tree(T185, T181, T186),\nT183 -> T185,\nT184 -> T186", fontsize=14, style = filled, fillcolor = lightblue];
177 -> 319 [arrowhead = none ];
319 -> 181;

320 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
177 -> 320 [arrowhead = none ];
320 -> 183;

321 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
178 -> 321 [arrowhead = none ];
321 -> 187;

322 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
178 -> 322 [arrowhead = none ];
322 -> 188;

323 [label="INSTANCE with matching:\nT46 -> T182\nT49 -> T185\nT50 -> T186", fontsize=14, style = filled, fillcolor = lightgrey];
181 -> 323 [arrowhead = none , style=dashed];
323 -> 51[style=dashed];

324 [label="EVAL with clause\ndelete(X200, tree(X201, X202, X203), tree(X201, X204, X203)) :- ','(less(X200, X201), delete(X200, X202, X204)).\nand substitutionT118 -> T211,\nX200 -> T211,\nX201 -> T212,\nX202 -> T213,\nX203 -> T214,\nT111 -> tree(T212, T213, T214),\nX204 -> T216,\nT119 -> tree(T212, T216, T214),\nT215 -> T216", fontsize=14, style = filled, fillcolor = lightblue];
187 -> 324 [arrowhead = none ];
324 -> 191;

325 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
187 -> 325 [arrowhead = none ];
325 -> 192;

326 [label="EVAL with clause\ndelete(X236, tree(X237, X238, X239), tree(X237, X238, X240)) :- ','(less(X237, X236), delete(X236, X239, X240)).\nand substitutionT118 -> T248,\nX236 -> T248,\nX237 -> T249,\nX238 -> T250,\nX239 -> T251,\nT111 -> tree(T249, T250, T251),\nX240 -> T253,\nT119 -> tree(T249, T250, T253),\nT252 -> T253", fontsize=14, style = filled, fillcolor = lightblue];
188 -> 326 [arrowhead = none ];
326 -> 209;

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

328 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
191 -> 328 [arrowhead = none ];
328 -> 193;

329 [label="SPLIT 2\nnew knowledge:\nT211 is ground\nT212 is ground", fontsize=14, style = filled, fillcolor = violet];
191 -> 329 [arrowhead = none ];
329 -> 194;

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

331 [label="INSTANCE with matching:\nT118 -> T211\nT111 -> T213\nT119 -> T216", fontsize=14, style = filled, fillcolor = lightgrey];
194 -> 331 [arrowhead = none , style=dashed];
331 -> 140[style=dashed];

332 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
195 -> 332 [arrowhead = none ];
332 -> 197;

333 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
195 -> 333 [arrowhead = none ];
333 -> 198;

334 [label="EVAL with clause\nless(0, s(X213)).\nand substitutionT211 -> 0,\nX213 -> T225,\nT212 -> s(T225)", fontsize=14, style = filled, fillcolor = lightblue];
197 -> 334 [arrowhead = none ];
334 -> 199;

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

336 [label="EVAL with clause\nless(s(X218), s(X219)) :- less(X218, X219).\nand substitutionX218 -> T230,\nT211 -> s(T230),\nX219 -> T231,\nT212 -> s(T231)", fontsize=14, style = filled, fillcolor = lightblue];
198 -> 336 [arrowhead = none ];
336 -> 205;

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

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

339 [label="INSTANCE with matching:\nT211 -> T230\nT212 -> T231", fontsize=14, style = filled, fillcolor = lightgrey];
205 -> 339 [arrowhead = none , style=dashed];
339 -> 193[style=dashed];

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

341 [label="SPLIT 2\nnew knowledge:\nT249 is ground\nT248 is ground", fontsize=14, style = filled, fillcolor = violet];
209 -> 341 [arrowhead = none ];
341 -> 214;

342 [label="INSTANCE with matching:\nT211 -> T249\nT212 -> T248", fontsize=14, style = filled, fillcolor = lightgrey];
213 -> 342 [arrowhead = none , style=dashed];
342 -> 193[style=dashed];

343 [label="INSTANCE with matching:\nT118 -> T248\nT111 -> T251\nT119 -> T253", fontsize=14, style = filled, fillcolor = lightgrey];
214 -> 343 [arrowhead = none , style=dashed];
343 -> 140[style=dashed];

344 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
230 -> 344 [arrowhead = none ];
344 -> 242;

345 [label="SPLIT 2\nnew knowledge:\nT273 is ground\nreplacements:T277 -> T281,\nT278 -> T282", fontsize=14, style = filled, fillcolor = violet];
230 -> 345 [arrowhead = none ];
345 -> 243;

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

347 [label="INSTANCE with matching:\nT1 -> T281\nT2 -> T275\nT3 -> T282", fontsize=14, style = filled, fillcolor = lightgrey];
243 -> 347 [arrowhead = none , style=dashed];
347 -> 3[style=dashed];

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

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

350 [label="EVAL with clause\nless(0, s(X272)).\nand substitutionT273 -> 0,\nX272 -> T289,\nT277 -> s(T289)", fontsize=14, style = filled, fillcolor = lightblue];
248 -> 350 [arrowhead = none ];
350 -> 251;

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

352 [label="EVAL with clause\nless(s(X277), s(X278)) :- less(X277, X278).\nand substitutionX277 -> T294,\nT273 -> s(T294),\nX278 -> T296,\nT277 -> s(T296),\nT295 -> T296", fontsize=14, style = filled, fillcolor = lightblue];
249 -> 352 [arrowhead = none ];
352 -> 263;

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

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

355 [label="INSTANCE with matching:\nT273 -> T294\nT277 -> T296", fontsize=14, style = filled, fillcolor = lightgrey];
263 -> 355 [arrowhead = none , style=dashed];
355 -> 242[style=dashed];

}

(2) Obligation:

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

f3_in(tree(T12, void, T13)) → f3_out1(T12)
f3_in(tree(T22, T23, void)) → f3_out1(T22)
f3_in(tree(T44, T45, T46)) → U1(f51_in(T46), tree(T44, T45, T46))
U1(f51_out1(T49), tree(T44, T45, T46)) → f3_out1(T44)
f3_in(tree(T110, T111, T112)) → U2(f135_in(T110, T111), tree(T110, T111, T112))
U2(f135_out1(T114), tree(T110, T111, T112)) → f3_out1(T114)
f3_in(tree(T273, T274, T275)) → U3(f230_in(T273, T275), tree(T273, T274, T275))
U3(f230_out1(T277), tree(T273, T274, T275)) → f3_out1(T277)
f51_in(tree(T63, void, T64)) → f51_out1(T63)
f51_in(tree(T77, T78, T79)) → U4(f51_in(T78), tree(T77, T78, T79))
U4(f51_out1(T83), tree(T77, T78, T79)) → f51_out1(T83)
f139_in(s(T126)) → f139_out1(0)
f139_in(s(T132)) → U5(f139_in(T132), s(T132))
U5(f139_out1(T133), s(T132)) → f139_out1(s(T133))
f140_in(T148, tree(T148, void, T149)) → f140_out1
f140_in(T158, tree(T158, T159, void)) → f140_out1
f140_in(T180, tree(T180, T181, T182)) → U6(f51_in(T182), T180, tree(T180, T181, T182))
U6(f51_out1(T185), T180, tree(T180, T181, T182)) → f140_out1
f140_in(T211, tree(T212, T213, T214)) → U7(f191_in(T211, T212, T213), T211, tree(T212, T213, T214))
U7(f191_out1, T211, tree(T212, T213, T214)) → f140_out1
f140_in(T248, tree(T249, T250, T251)) → U8(f209_in(T249, T248, T251), T248, tree(T249, T250, T251))
U8(f209_out1, T248, tree(T249, T250, T251)) → f140_out1
f193_in(0, s(T225)) → f193_out1
f193_in(s(T230), s(T231)) → U9(f193_in(T230, T231), s(T230), s(T231))
U9(f193_out1, s(T230), s(T231)) → f193_out1
f242_in(0) → f242_out1
f242_in(s(T294)) → U10(f242_in(T294), s(T294))
U10(f242_out1, s(T294)) → f242_out1
f135_in(T110, T111) → U11(f139_in(T110), T110, T111)
U11(f139_out1(T118), T110, T111) → U12(f140_in(T118, T111), T110, T111, T118)
U12(f140_out1, T110, T111, T118) → f135_out1(T118)
f191_in(T211, T212, T213) → U13(f193_in(T211, T212), T211, T212, T213)
U13(f193_out1, T211, T212, T213) → U14(f140_in(T211, T213), T211, T212, T213)
U14(f140_out1, T211, T212, T213) → f191_out1
f209_in(T249, T248, T251) → U15(f193_in(T249, T248), T249, T248, T251)
U15(f193_out1, T249, T248, T251) → U16(f140_in(T248, T251), T249, T248, T251)
U16(f140_out1, T249, T248, T251) → f209_out1
f230_in(T273, T275) → U17(f242_in(T273), T273, T275)
U17(f242_out1, T273, T275) → U18(f3_in(T275), T273, T275)
U18(f3_out1(T281), T273, T275) → f230_out1(T281)

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(T44, T45, T46)) → U1¹(f51_in(T46), tree(T44, T45, T46))
F3_IN(tree(T44, T45, T46)) → F51_IN(T46)
F3_IN(tree(T110, T111, T112)) → U2¹(f135_in(T110, T111), tree(T110, T111, T112))
F3_IN(tree(T110, T111, T112)) → F135_IN(T110, T111)
F3_IN(tree(T273, T274, T275)) → U3¹(f230_in(T273, T275), tree(T273, T274, T275))
F3_IN(tree(T273, T274, T275)) → F230_IN(T273, T275)
F51_IN(tree(T77, T78, T79)) → U4¹(f51_in(T78), tree(T77, T78, T79))
F51_IN(tree(T77, T78, T79)) → F51_IN(T78)
F139_IN(s(T132)) → U5¹(f139_in(T132), s(T132))
F139_IN(s(T132)) → F139_IN(T132)
F140_IN(T180, tree(T180, T181, T182)) → U6¹(f51_in(T182), T180, tree(T180, T181, T182))
F140_IN(T180, tree(T180, T181, T182)) → F51_IN(T182)
F140_IN(T211, tree(T212, T213, T214)) → U7¹(f191_in(T211, T212, T213), T211, tree(T212, T213, T214))
F140_IN(T211, tree(T212, T213, T214)) → F191_IN(T211, T212, T213)
F140_IN(T248, tree(T249, T250, T251)) → U8¹(f209_in(T249, T248, T251), T248, tree(T249, T250, T251))
F140_IN(T248, tree(T249, T250, T251)) → F209_IN(T249, T248, T251)
F193_IN(s(T230), s(T231)) → U9¹(f193_in(T230, T231), s(T230), s(T231))
F193_IN(s(T230), s(T231)) → F193_IN(T230, T231)
F242_IN(s(T294)) → U10¹(f242_in(T294), s(T294))
F242_IN(s(T294)) → F242_IN(T294)
F135_IN(T110, T111) → U11¹(f139_in(T110), T110, T111)
F135_IN(T110, T111) → F139_IN(T110)
U11¹(f139_out1(T118), T110, T111) → U12¹(f140_in(T118, T111), T110, T111, T118)
U11¹(f139_out1(T118), T110, T111) → F140_IN(T118, T111)
F191_IN(T211, T212, T213) → U13¹(f193_in(T211, T212), T211, T212, T213)
F191_IN(T211, T212, T213) → F193_IN(T211, T212)
U13¹(f193_out1, T211, T212, T213) → U14¹(f140_in(T211, T213), T211, T212, T213)
U13¹(f193_out1, T211, T212, T213) → F140_IN(T211, T213)
F209_IN(T249, T248, T251) → U15¹(f193_in(T249, T248), T249, T248, T251)
F209_IN(T249, T248, T251) → F193_IN(T249, T248)
U15¹(f193_out1, T249, T248, T251) → U16¹(f140_in(T248, T251), T249, T248, T251)
U15¹(f193_out1, T249, T248, T251) → F140_IN(T248, T251)
F230_IN(T273, T275) → U17¹(f242_in(T273), T273, T275)
F230_IN(T273, T275) → F242_IN(T273)
U17¹(f242_out1, T273, T275) → U18¹(f3_in(T275), T273, T275)
U17¹(f242_out1, T273, T275) → F3_IN(T275)

The TRS R consists of the following rules:

f3_in(tree(T12, void, T13)) → f3_out1(T12)
f3_in(tree(T22, T23, void)) → f3_out1(T22)
f3_in(tree(T44, T45, T46)) → U1(f51_in(T46), tree(T44, T45, T46))
U1(f51_out1(T49), tree(T44, T45, T46)) → f3_out1(T44)
f3_in(tree(T110, T111, T112)) → U2(f135_in(T110, T111), tree(T110, T111, T112))
U2(f135_out1(T114), tree(T110, T111, T112)) → f3_out1(T114)
f3_in(tree(T273, T274, T275)) → U3(f230_in(T273, T275), tree(T273, T274, T275))
U3(f230_out1(T277), tree(T273, T274, T275)) → f3_out1(T277)
f51_in(tree(T63, void, T64)) → f51_out1(T63)
f51_in(tree(T77, T78, T79)) → U4(f51_in(T78), tree(T77, T78, T79))
U4(f51_out1(T83), tree(T77, T78, T79)) → f51_out1(T83)
f139_in(s(T126)) → f139_out1(0)
f139_in(s(T132)) → U5(f139_in(T132), s(T132))
U5(f139_out1(T133), s(T132)) → f139_out1(s(T133))
f140_in(T148, tree(T148, void, T149)) → f140_out1
f140_in(T158, tree(T158, T159, void)) → f140_out1
f140_in(T180, tree(T180, T181, T182)) → U6(f51_in(T182), T180, tree(T180, T181, T182))
U6(f51_out1(T185), T180, tree(T180, T181, T182)) → f140_out1
f140_in(T211, tree(T212, T213, T214)) → U7(f191_in(T211, T212, T213), T211, tree(T212, T213, T214))
U7(f191_out1, T211, tree(T212, T213, T214)) → f140_out1
f140_in(T248, tree(T249, T250, T251)) → U8(f209_in(T249, T248, T251), T248, tree(T249, T250, T251))
U8(f209_out1, T248, tree(T249, T250, T251)) → f140_out1
f193_in(0, s(T225)) → f193_out1
f193_in(s(T230), s(T231)) → U9(f193_in(T230, T231), s(T230), s(T231))
U9(f193_out1, s(T230), s(T231)) → f193_out1
f242_in(0) → f242_out1
f242_in(s(T294)) → U10(f242_in(T294), s(T294))
U10(f242_out1, s(T294)) → f242_out1
f135_in(T110, T111) → U11(f139_in(T110), T110, T111)
U11(f139_out1(T118), T110, T111) → U12(f140_in(T118, T111), T110, T111, T118)
U12(f140_out1, T110, T111, T118) → f135_out1(T118)
f191_in(T211, T212, T213) → U13(f193_in(T211, T212), T211, T212, T213)
U13(f193_out1, T211, T212, T213) → U14(f140_in(T211, T213), T211, T212, T213)
U14(f140_out1, T211, T212, T213) → f191_out1
f209_in(T249, T248, T251) → U15(f193_in(T249, T248), T249, T248, T251)
U15(f193_out1, T249, T248, T251) → U16(f140_in(T248, T251), T249, T248, T251)
U16(f140_out1, T249, T248, T251) → f209_out1
f230_in(T273, T275) → U17(f242_in(T273), T273, T275)
U17(f242_out1, T273, T275) → U18(f3_in(T275), T273, T275)
U18(f3_out1(T281), T273, T275) → f230_out1(T281)

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 6 SCCs with 23 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

F242_IN(s(T294)) → F242_IN(T294)

The TRS R consists of the following rules:

f3_in(tree(T12, void, T13)) → f3_out1(T12)
f3_in(tree(T22, T23, void)) → f3_out1(T22)
f3_in(tree(T44, T45, T46)) → U1(f51_in(T46), tree(T44, T45, T46))
U1(f51_out1(T49), tree(T44, T45, T46)) → f3_out1(T44)
f3_in(tree(T110, T111, T112)) → U2(f135_in(T110, T111), tree(T110, T111, T112))
U2(f135_out1(T114), tree(T110, T111, T112)) → f3_out1(T114)
f3_in(tree(T273, T274, T275)) → U3(f230_in(T273, T275), tree(T273, T274, T275))
U3(f230_out1(T277), tree(T273, T274, T275)) → f3_out1(T277)
f51_in(tree(T63, void, T64)) → f51_out1(T63)
f51_in(tree(T77, T78, T79)) → U4(f51_in(T78), tree(T77, T78, T79))
U4(f51_out1(T83), tree(T77, T78, T79)) → f51_out1(T83)
f139_in(s(T126)) → f139_out1(0)
f139_in(s(T132)) → U5(f139_in(T132), s(T132))
U5(f139_out1(T133), s(T132)) → f139_out1(s(T133))
f140_in(T148, tree(T148, void, T149)) → f140_out1
f140_in(T158, tree(T158, T159, void)) → f140_out1
f140_in(T180, tree(T180, T181, T182)) → U6(f51_in(T182), T180, tree(T180, T181, T182))
U6(f51_out1(T185), T180, tree(T180, T181, T182)) → f140_out1
f140_in(T211, tree(T212, T213, T214)) → U7(f191_in(T211, T212, T213), T211, tree(T212, T213, T214))
U7(f191_out1, T211, tree(T212, T213, T214)) → f140_out1
f140_in(T248, tree(T249, T250, T251)) → U8(f209_in(T249, T248, T251), T248, tree(T249, T250, T251))
U8(f209_out1, T248, tree(T249, T250, T251)) → f140_out1
f193_in(0, s(T225)) → f193_out1
f193_in(s(T230), s(T231)) → U9(f193_in(T230, T231), s(T230), s(T231))
U9(f193_out1, s(T230), s(T231)) → f193_out1
f242_in(0) → f242_out1
f242_in(s(T294)) → U10(f242_in(T294), s(T294))
U10(f242_out1, s(T294)) → f242_out1
f135_in(T110, T111) → U11(f139_in(T110), T110, T111)
U11(f139_out1(T118), T110, T111) → U12(f140_in(T118, T111), T110, T111, T118)
U12(f140_out1, T110, T111, T118) → f135_out1(T118)
f191_in(T211, T212, T213) → U13(f193_in(T211, T212), T211, T212, T213)
U13(f193_out1, T211, T212, T213) → U14(f140_in(T211, T213), T211, T212, T213)
U14(f140_out1, T211, T212, T213) → f191_out1
f209_in(T249, T248, T251) → U15(f193_in(T249, T248), T249, T248, T251)
U15(f193_out1, T249, T248, T251) → U16(f140_in(T248, T251), T249, T248, T251)
U16(f140_out1, T249, T248, T251) → f209_out1
f230_in(T273, T275) → U17(f242_in(T273), T273, T275)
U17(f242_out1, T273, T275) → U18(f3_in(T275), T273, T275)
U18(f3_out1(T281), T273, T275) → f230_out1(T281)

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:

F242_IN(s(T294)) → F242_IN(T294)

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:

• F242_IN(s(T294)) → F242_IN(T294)
  The graph contains the following edges 1 > 1

(11) YES

(12) Obligation:

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

F193_IN(s(T230), s(T231)) → F193_IN(T230, T231)

The TRS R consists of the following rules:

f3_in(tree(T12, void, T13)) → f3_out1(T12)
f3_in(tree(T22, T23, void)) → f3_out1(T22)
f3_in(tree(T44, T45, T46)) → U1(f51_in(T46), tree(T44, T45, T46))
U1(f51_out1(T49), tree(T44, T45, T46)) → f3_out1(T44)
f3_in(tree(T110, T111, T112)) → U2(f135_in(T110, T111), tree(T110, T111, T112))
U2(f135_out1(T114), tree(T110, T111, T112)) → f3_out1(T114)
f3_in(tree(T273, T274, T275)) → U3(f230_in(T273, T275), tree(T273, T274, T275))
U3(f230_out1(T277), tree(T273, T274, T275)) → f3_out1(T277)
f51_in(tree(T63, void, T64)) → f51_out1(T63)
f51_in(tree(T77, T78, T79)) → U4(f51_in(T78), tree(T77, T78, T79))
U4(f51_out1(T83), tree(T77, T78, T79)) → f51_out1(T83)
f139_in(s(T126)) → f139_out1(0)
f139_in(s(T132)) → U5(f139_in(T132), s(T132))
U5(f139_out1(T133), s(T132)) → f139_out1(s(T133))
f140_in(T148, tree(T148, void, T149)) → f140_out1
f140_in(T158, tree(T158, T159, void)) → f140_out1
f140_in(T180, tree(T180, T181, T182)) → U6(f51_in(T182), T180, tree(T180, T181, T182))
U6(f51_out1(T185), T180, tree(T180, T181, T182)) → f140_out1
f140_in(T211, tree(T212, T213, T214)) → U7(f191_in(T211, T212, T213), T211, tree(T212, T213, T214))
U7(f191_out1, T211, tree(T212, T213, T214)) → f140_out1
f140_in(T248, tree(T249, T250, T251)) → U8(f209_in(T249, T248, T251), T248, tree(T249, T250, T251))
U8(f209_out1, T248, tree(T249, T250, T251)) → f140_out1
f193_in(0, s(T225)) → f193_out1
f193_in(s(T230), s(T231)) → U9(f193_in(T230, T231), s(T230), s(T231))
U9(f193_out1, s(T230), s(T231)) → f193_out1
f242_in(0) → f242_out1
f242_in(s(T294)) → U10(f242_in(T294), s(T294))
U10(f242_out1, s(T294)) → f242_out1
f135_in(T110, T111) → U11(f139_in(T110), T110, T111)
U11(f139_out1(T118), T110, T111) → U12(f140_in(T118, T111), T110, T111, T118)
U12(f140_out1, T110, T111, T118) → f135_out1(T118)
f191_in(T211, T212, T213) → U13(f193_in(T211, T212), T211, T212, T213)
U13(f193_out1, T211, T212, T213) → U14(f140_in(T211, T213), T211, T212, T213)
U14(f140_out1, T211, T212, T213) → f191_out1
f209_in(T249, T248, T251) → U15(f193_in(T249, T248), T249, T248, T251)
U15(f193_out1, T249, T248, T251) → U16(f140_in(T248, T251), T249, T248, T251)
U16(f140_out1, T249, T248, T251) → f209_out1
f230_in(T273, T275) → U17(f242_in(T273), T273, T275)
U17(f242_out1, T273, T275) → U18(f3_in(T275), T273, T275)
U18(f3_out1(T281), T273, T275) → f230_out1(T281)

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:

F193_IN(s(T230), s(T231)) → F193_IN(T230, T231)

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:

• F193_IN(s(T230), s(T231)) → F193_IN(T230, T231)
  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:

F139_IN(s(T132)) → F139_IN(T132)

The TRS R consists of the following rules:

f3_in(tree(T12, void, T13)) → f3_out1(T12)
f3_in(tree(T22, T23, void)) → f3_out1(T22)
f3_in(tree(T44, T45, T46)) → U1(f51_in(T46), tree(T44, T45, T46))
U1(f51_out1(T49), tree(T44, T45, T46)) → f3_out1(T44)
f3_in(tree(T110, T111, T112)) → U2(f135_in(T110, T111), tree(T110, T111, T112))
U2(f135_out1(T114), tree(T110, T111, T112)) → f3_out1(T114)
f3_in(tree(T273, T274, T275)) → U3(f230_in(T273, T275), tree(T273, T274, T275))
U3(f230_out1(T277), tree(T273, T274, T275)) → f3_out1(T277)
f51_in(tree(T63, void, T64)) → f51_out1(T63)
f51_in(tree(T77, T78, T79)) → U4(f51_in(T78), tree(T77, T78, T79))
U4(f51_out1(T83), tree(T77, T78, T79)) → f51_out1(T83)
f139_in(s(T126)) → f139_out1(0)
f139_in(s(T132)) → U5(f139_in(T132), s(T132))
U5(f139_out1(T133), s(T132)) → f139_out1(s(T133))
f140_in(T148, tree(T148, void, T149)) → f140_out1
f140_in(T158, tree(T158, T159, void)) → f140_out1
f140_in(T180, tree(T180, T181, T182)) → U6(f51_in(T182), T180, tree(T180, T181, T182))
U6(f51_out1(T185), T180, tree(T180, T181, T182)) → f140_out1
f140_in(T211, tree(T212, T213, T214)) → U7(f191_in(T211, T212, T213), T211, tree(T212, T213, T214))
U7(f191_out1, T211, tree(T212, T213, T214)) → f140_out1
f140_in(T248, tree(T249, T250, T251)) → U8(f209_in(T249, T248, T251), T248, tree(T249, T250, T251))
U8(f209_out1, T248, tree(T249, T250, T251)) → f140_out1
f193_in(0, s(T225)) → f193_out1
f193_in(s(T230), s(T231)) → U9(f193_in(T230, T231), s(T230), s(T231))
U9(f193_out1, s(T230), s(T231)) → f193_out1
f242_in(0) → f242_out1
f242_in(s(T294)) → U10(f242_in(T294), s(T294))
U10(f242_out1, s(T294)) → f242_out1
f135_in(T110, T111) → U11(f139_in(T110), T110, T111)
U11(f139_out1(T118), T110, T111) → U12(f140_in(T118, T111), T110, T111, T118)
U12(f140_out1, T110, T111, T118) → f135_out1(T118)
f191_in(T211, T212, T213) → U13(f193_in(T211, T212), T211, T212, T213)
U13(f193_out1, T211, T212, T213) → U14(f140_in(T211, T213), T211, T212, T213)
U14(f140_out1, T211, T212, T213) → f191_out1
f209_in(T249, T248, T251) → U15(f193_in(T249, T248), T249, T248, T251)
U15(f193_out1, T249, T248, T251) → U16(f140_in(T248, T251), T249, T248, T251)
U16(f140_out1, T249, T248, T251) → f209_out1
f230_in(T273, T275) → U17(f242_in(T273), T273, T275)
U17(f242_out1, T273, T275) → U18(f3_in(T275), T273, T275)
U18(f3_out1(T281), T273, T275) → f230_out1(T281)

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

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

(19) Obligation:

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

F139_IN(s(T132)) → F139_IN(T132)

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

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

• F139_IN(s(T132)) → F139_IN(T132)
  The graph contains the following edges 1 > 1

(21) YES

(22) Obligation:

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

F51_IN(tree(T77, T78, T79)) → F51_IN(T78)

The TRS R consists of the following rules:

f3_in(tree(T12, void, T13)) → f3_out1(T12)
f3_in(tree(T22, T23, void)) → f3_out1(T22)
f3_in(tree(T44, T45, T46)) → U1(f51_in(T46), tree(T44, T45, T46))
U1(f51_out1(T49), tree(T44, T45, T46)) → f3_out1(T44)
f3_in(tree(T110, T111, T112)) → U2(f135_in(T110, T111), tree(T110, T111, T112))
U2(f135_out1(T114), tree(T110, T111, T112)) → f3_out1(T114)
f3_in(tree(T273, T274, T275)) → U3(f230_in(T273, T275), tree(T273, T274, T275))
U3(f230_out1(T277), tree(T273, T274, T275)) → f3_out1(T277)
f51_in(tree(T63, void, T64)) → f51_out1(T63)
f51_in(tree(T77, T78, T79)) → U4(f51_in(T78), tree(T77, T78, T79))
U4(f51_out1(T83), tree(T77, T78, T79)) → f51_out1(T83)
f139_in(s(T126)) → f139_out1(0)
f139_in(s(T132)) → U5(f139_in(T132), s(T132))
U5(f139_out1(T133), s(T132)) → f139_out1(s(T133))
f140_in(T148, tree(T148, void, T149)) → f140_out1
f140_in(T158, tree(T158, T159, void)) → f140_out1
f140_in(T180, tree(T180, T181, T182)) → U6(f51_in(T182), T180, tree(T180, T181, T182))
U6(f51_out1(T185), T180, tree(T180, T181, T182)) → f140_out1
f140_in(T211, tree(T212, T213, T214)) → U7(f191_in(T211, T212, T213), T211, tree(T212, T213, T214))
U7(f191_out1, T211, tree(T212, T213, T214)) → f140_out1
f140_in(T248, tree(T249, T250, T251)) → U8(f209_in(T249, T248, T251), T248, tree(T249, T250, T251))
U8(f209_out1, T248, tree(T249, T250, T251)) → f140_out1
f193_in(0, s(T225)) → f193_out1
f193_in(s(T230), s(T231)) → U9(f193_in(T230, T231), s(T230), s(T231))
U9(f193_out1, s(T230), s(T231)) → f193_out1
f242_in(0) → f242_out1
f242_in(s(T294)) → U10(f242_in(T294), s(T294))
U10(f242_out1, s(T294)) → f242_out1
f135_in(T110, T111) → U11(f139_in(T110), T110, T111)
U11(f139_out1(T118), T110, T111) → U12(f140_in(T118, T111), T110, T111, T118)
U12(f140_out1, T110, T111, T118) → f135_out1(T118)
f191_in(T211, T212, T213) → U13(f193_in(T211, T212), T211, T212, T213)
U13(f193_out1, T211, T212, T213) → U14(f140_in(T211, T213), T211, T212, T213)
U14(f140_out1, T211, T212, T213) → f191_out1
f209_in(T249, T248, T251) → U15(f193_in(T249, T248), T249, T248, T251)
U15(f193_out1, T249, T248, T251) → U16(f140_in(T248, T251), T249, T248, T251)
U16(f140_out1, T249, T248, T251) → f209_out1
f230_in(T273, T275) → U17(f242_in(T273), T273, T275)
U17(f242_out1, T273, T275) → U18(f3_in(T275), T273, T275)
U18(f3_out1(T281), T273, T275) → f230_out1(T281)

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

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

(24) Obligation:

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

F51_IN(tree(T77, T78, T79)) → F51_IN(T78)

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

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

• F51_IN(tree(T77, T78, T79)) → F51_IN(T78)
  The graph contains the following edges 1 > 1

(26) YES

(27) Obligation:

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

F140_IN(T211, tree(T212, T213, T214)) → F191_IN(T211, T212, T213)
F191_IN(T211, T212, T213) → U13¹(f193_in(T211, T212), T211, T212, T213)
U13¹(f193_out1, T211, T212, T213) → F140_IN(T211, T213)
F140_IN(T248, tree(T249, T250, T251)) → F209_IN(T249, T248, T251)
F209_IN(T249, T248, T251) → U15¹(f193_in(T249, T248), T249, T248, T251)
U15¹(f193_out1, T249, T248, T251) → F140_IN(T248, T251)

The TRS R consists of the following rules:

f3_in(tree(T12, void, T13)) → f3_out1(T12)
f3_in(tree(T22, T23, void)) → f3_out1(T22)
f3_in(tree(T44, T45, T46)) → U1(f51_in(T46), tree(T44, T45, T46))
U1(f51_out1(T49), tree(T44, T45, T46)) → f3_out1(T44)
f3_in(tree(T110, T111, T112)) → U2(f135_in(T110, T111), tree(T110, T111, T112))
U2(f135_out1(T114), tree(T110, T111, T112)) → f3_out1(T114)
f3_in(tree(T273, T274, T275)) → U3(f230_in(T273, T275), tree(T273, T274, T275))
U3(f230_out1(T277), tree(T273, T274, T275)) → f3_out1(T277)
f51_in(tree(T63, void, T64)) → f51_out1(T63)
f51_in(tree(T77, T78, T79)) → U4(f51_in(T78), tree(T77, T78, T79))
U4(f51_out1(T83), tree(T77, T78, T79)) → f51_out1(T83)
f139_in(s(T126)) → f139_out1(0)
f139_in(s(T132)) → U5(f139_in(T132), s(T132))
U5(f139_out1(T133), s(T132)) → f139_out1(s(T133))
f140_in(T148, tree(T148, void, T149)) → f140_out1
f140_in(T158, tree(T158, T159, void)) → f140_out1
f140_in(T180, tree(T180, T181, T182)) → U6(f51_in(T182), T180, tree(T180, T181, T182))
U6(f51_out1(T185), T180, tree(T180, T181, T182)) → f140_out1
f140_in(T211, tree(T212, T213, T214)) → U7(f191_in(T211, T212, T213), T211, tree(T212, T213, T214))
U7(f191_out1, T211, tree(T212, T213, T214)) → f140_out1
f140_in(T248, tree(T249, T250, T251)) → U8(f209_in(T249, T248, T251), T248, tree(T249, T250, T251))
U8(f209_out1, T248, tree(T249, T250, T251)) → f140_out1
f193_in(0, s(T225)) → f193_out1
f193_in(s(T230), s(T231)) → U9(f193_in(T230, T231), s(T230), s(T231))
U9(f193_out1, s(T230), s(T231)) → f193_out1
f242_in(0) → f242_out1
f242_in(s(T294)) → U10(f242_in(T294), s(T294))
U10(f242_out1, s(T294)) → f242_out1
f135_in(T110, T111) → U11(f139_in(T110), T110, T111)
U11(f139_out1(T118), T110, T111) → U12(f140_in(T118, T111), T110, T111, T118)
U12(f140_out1, T110, T111, T118) → f135_out1(T118)
f191_in(T211, T212, T213) → U13(f193_in(T211, T212), T211, T212, T213)
U13(f193_out1, T211, T212, T213) → U14(f140_in(T211, T213), T211, T212, T213)
U14(f140_out1, T211, T212, T213) → f191_out1
f209_in(T249, T248, T251) → U15(f193_in(T249, T248), T249, T248, T251)
U15(f193_out1, T249, T248, T251) → U16(f140_in(T248, T251), T249, T248, T251)
U16(f140_out1, T249, T248, T251) → f209_out1
f230_in(T273, T275) → U17(f242_in(T273), T273, T275)
U17(f242_out1, T273, T275) → U18(f3_in(T275), T273, T275)
U18(f3_out1(T281), T273, T275) → f230_out1(T281)

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

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

• F191_IN(T211, T212, T213) → U13¹(f193_in(T211, T212), T211, T212, T213)
  The graph contains the following edges 1 >= 2, 2 >= 3, 3 >= 4

• U13¹(f193_out1, T211, T212, T213) → F140_IN(T211, T213)
  The graph contains the following edges 2 >= 1, 4 >= 2

• U15¹(f193_out1, T249, T248, T251) → F140_IN(T248, T251)
  The graph contains the following edges 3 >= 1, 4 >= 2

• F140_IN(T211, tree(T212, T213, T214)) → F191_IN(T211, T212, T213)
  The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

• F140_IN(T248, tree(T249, T250, T251)) → F209_IN(T249, T248, T251)
  The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3

• F209_IN(T249, T248, T251) → U15¹(f193_in(T249, T248), T249, T248, T251)
  The graph contains the following edges 1 >= 2, 2 >= 3, 3 >= 4

(29) YES

(30) Obligation:

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

F3_IN(tree(T273, T274, T275)) → F230_IN(T273, T275)
F230_IN(T273, T275) → U17¹(f242_in(T273), T273, T275)
U17¹(f242_out1, T273, T275) → F3_IN(T275)

The TRS R consists of the following rules:

f3_in(tree(T12, void, T13)) → f3_out1(T12)
f3_in(tree(T22, T23, void)) → f3_out1(T22)
f3_in(tree(T44, T45, T46)) → U1(f51_in(T46), tree(T44, T45, T46))
U1(f51_out1(T49), tree(T44, T45, T46)) → f3_out1(T44)
f3_in(tree(T110, T111, T112)) → U2(f135_in(T110, T111), tree(T110, T111, T112))
U2(f135_out1(T114), tree(T110, T111, T112)) → f3_out1(T114)
f3_in(tree(T273, T274, T275)) → U3(f230_in(T273, T275), tree(T273, T274, T275))
U3(f230_out1(T277), tree(T273, T274, T275)) → f3_out1(T277)
f51_in(tree(T63, void, T64)) → f51_out1(T63)
f51_in(tree(T77, T78, T79)) → U4(f51_in(T78), tree(T77, T78, T79))
U4(f51_out1(T83), tree(T77, T78, T79)) → f51_out1(T83)
f139_in(s(T126)) → f139_out1(0)
f139_in(s(T132)) → U5(f139_in(T132), s(T132))
U5(f139_out1(T133), s(T132)) → f139_out1(s(T133))
f140_in(T148, tree(T148, void, T149)) → f140_out1
f140_in(T158, tree(T158, T159, void)) → f140_out1
f140_in(T180, tree(T180, T181, T182)) → U6(f51_in(T182), T180, tree(T180, T181, T182))
U6(f51_out1(T185), T180, tree(T180, T181, T182)) → f140_out1
f140_in(T211, tree(T212, T213, T214)) → U7(f191_in(T211, T212, T213), T211, tree(T212, T213, T214))
U7(f191_out1, T211, tree(T212, T213, T214)) → f140_out1
f140_in(T248, tree(T249, T250, T251)) → U8(f209_in(T249, T248, T251), T248, tree(T249, T250, T251))
U8(f209_out1, T248, tree(T249, T250, T251)) → f140_out1
f193_in(0, s(T225)) → f193_out1
f193_in(s(T230), s(T231)) → U9(f193_in(T230, T231), s(T230), s(T231))
U9(f193_out1, s(T230), s(T231)) → f193_out1
f242_in(0) → f242_out1
f242_in(s(T294)) → U10(f242_in(T294), s(T294))
U10(f242_out1, s(T294)) → f242_out1
f135_in(T110, T111) → U11(f139_in(T110), T110, T111)
U11(f139_out1(T118), T110, T111) → U12(f140_in(T118, T111), T110, T111, T118)
U12(f140_out1, T110, T111, T118) → f135_out1(T118)
f191_in(T211, T212, T213) → U13(f193_in(T211, T212), T211, T212, T213)
U13(f193_out1, T211, T212, T213) → U14(f140_in(T211, T213), T211, T212, T213)
U14(f140_out1, T211, T212, T213) → f191_out1
f209_in(T249, T248, T251) → U15(f193_in(T249, T248), T249, T248, T251)
U15(f193_out1, T249, T248, T251) → U16(f140_in(T248, T251), T249, T248, T251)
U16(f140_out1, T249, T248, T251) → f209_out1
f230_in(T273, T275) → U17(f242_in(T273), T273, T275)
U17(f242_out1, T273, T275) → U18(f3_in(T275), T273, T275)
U18(f3_out1(T281), T273, T275) → f230_out1(T281)

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

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

• F230_IN(T273, T275) → U17¹(f242_in(T273), T273, T275)
  The graph contains the following edges 1 >= 2, 2 >= 3

• U17¹(f242_out1, T273, T275) → F3_IN(T275)
  The graph contains the following edges 3 >= 1

• F3_IN(tree(T273, T274, T275)) → F230_IN(T273, T275)
  The graph contains the following edges 1 > 1, 1 > 2

(32) YES