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

(0) Obligation:

Clauses:

log2(X, Y) :- log2(X, 0, Y).
log2(0, I, I).
log2(s(0), I, I).
log2(s(s(X)), I, Y) :- ','(half(s(s(X)), X1), log2(X1, s(I), Y)).
half(0, 0).
half(s(0), 0).
half(s(s(X)), s(Y)) :- half(X, Y).

Query: log2(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: log2(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: log2(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: log2(T5, 0, T7)\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: log2(T5, 0, T7), SCOPE: 2, CLAUSE: 1 | log2(T5, 0, T7), SCOPE: 2, CLAUSE: 2 | log2(T5, 0, T7), SCOPE: 2, CLAUSE: 3\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: log2(T5, 0, T7), SCOPE: 2, CLAUSE: 1\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: log2(T5, 0, T7), SCOPE: 2, CLAUSE: 2 | log2(T5, 0, T7), SCOPE: 2, CLAUSE: 3\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: log2(T5, 0, T7), SCOPE: 2, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: log2(T5, 0, T7), SCOPE: 2, CLAUSE: 3\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="B: ','(half(s(s(T12)), X26), log2(X26, s(0), T14))\n\nT12 is ground\nX26 is free", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="D: half(s(s(T12)), X26)\n\nT12 is ground\nX26 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="E: log2(T15, s(0), T14)\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: half(s(s(T12)), X26), SCOPE: 3, CLAUSE: 4 | half(s(s(T12)), X26), SCOPE: 3, CLAUSE: 5 | half(s(s(T12)), X26), SCOPE: 3, CLAUSE: 6\n\nT12 is ground\nX26 is free", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: half(s(s(T12)), X26), SCOPE: 3, CLAUSE: 5 | half(s(s(T12)), X26), SCOPE: 3, CLAUSE: 6\n\nT12 is ground\nX26 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: half(s(s(T12)), X26), SCOPE: 3, CLAUSE: 6\n\nT12 is ground\nX26 is free", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="C: half(T18, X35)\n\nT18 is ground\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: half(T18, X35), SCOPE: 4, CLAUSE: 4 | half(T18, X35), SCOPE: 4, CLAUSE: 5 | half(T18, X35), SCOPE: 4, CLAUSE: 6\n\nT18 is ground\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: half(T18, X35), SCOPE: 4, CLAUSE: 4\n\nT18 is ground\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: half(T18, X35), SCOPE: 4, CLAUSE: 5 | half(T18, X35), SCOPE: 4, CLAUSE: 6\n\nT18 is ground\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: half(T18, X35), SCOPE: 4, CLAUSE: 5\n\nT18 is ground\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: half(T18, X35), SCOPE: 4, CLAUSE: 6\n\nT18 is ground\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: half(T21, X44)\n\nT21 is ground\nX44 is free", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: log2(T15, s(0), T14), SCOPE: 5, CLAUSE: 1 | log2(T15, s(0), T14), SCOPE: 5, CLAUSE: 2 | log2(T15, s(0), T14), SCOPE: 5, CLAUSE: 3\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: log2(T15, s(0), T14), SCOPE: 5, CLAUSE: 1\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: log2(T15, s(0), T14), SCOPE: 5, CLAUSE: 2 | log2(T15, s(0), T14), SCOPE: 5, CLAUSE: 3\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: log2(T15, s(0), T14), SCOPE: 5, CLAUSE: 2\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: log2(T15, s(0), T14), SCOPE: 5, CLAUSE: 3\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="F: ','(half(s(s(T26)), X67), log2(X67, s(s(0)), T28))\n\nT26 is ground\nX67 is free", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: half(s(s(T26)), X67)\n\nT26 is ground\nX67 is free", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="G: log2(T29, s(s(0)), T28)\n\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: log2(T29, s(s(0)), T28), SCOPE: 6, CLAUSE: 1 | log2(T29, s(s(0)), T28), SCOPE: 6, CLAUSE: 2 | log2(T29, s(s(0)), T28), SCOPE: 6, CLAUSE: 3\n\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: log2(T29, s(s(0)), T28), SCOPE: 6, CLAUSE: 1\n\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: log2(T29, s(s(0)), T28), SCOPE: 6, CLAUSE: 2 | log2(T29, s(s(0)), T28), SCOPE: 6, CLAUSE: 3\n\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: log2(T29, s(s(0)), T28), SCOPE: 6, CLAUSE: 2\n\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="221: log2(T29, s(s(0)), T28), SCOPE: 6, CLAUSE: 3\n\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
228 [label="228: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
250 [label="H: ','(half(s(s(T34)), X90), log2(X90, s(s(s(0))), T36))\n\nT34 is ground\nX90 is free", fontsize=16, style=filled, fillcolor=lightyellow];
251 [label="251: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
257 [label="257: half(s(s(T34)), X90)\n\nT34 is ground\nX90 is free", fontsize=16, style=filled, fillcolor=lightyellow];
258 [label="I: log2(T37, s(s(s(0))), T36)\n\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
267 [label="267: log2(T37, s(s(s(0))), T36), SCOPE: 7, CLAUSE: 1 | log2(T37, s(s(s(0))), T36), SCOPE: 7, CLAUSE: 2 | log2(T37, s(s(s(0))), T36), SCOPE: 7, CLAUSE: 3\n\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
269 [label="269: log2(T37, s(s(s(0))), T36), SCOPE: 7, CLAUSE: 1\n\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
270 [label="270: log2(T37, s(s(s(0))), T36), SCOPE: 7, CLAUSE: 2 | log2(T37, s(s(s(0))), T36), SCOPE: 7, CLAUSE: 3\n\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
286 [label="286: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
287 [label="287: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
289 [label="289: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
293 [label="293: log2(T37, s(s(s(0))), T36), SCOPE: 7, CLAUSE: 2\n\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
294 [label="294: log2(T37, s(s(s(0))), T36), SCOPE: 7, CLAUSE: 3\n\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
295 [label="295: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
297 [label="297: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
298 [label="298: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
305 [label="J: ','(half(s(s(T42)), X113), log2(X113, s(s(s(s(0)))), T44))\n\nT42 is ground\nX113 is free", fontsize=16, style=filled, fillcolor=lightyellow];
306 [label="306: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
325 [label="325: half(s(s(T42)), X113)\n\nT42 is ground\nX113 is free", fontsize=16, style=filled, fillcolor=lightyellow];
326 [label="K: log2(T45, s(s(s(s(0)))), T44)\n\nT45 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
330 [label="330: log2(T45, s(s(s(s(0)))), T44), SCOPE: 8, CLAUSE: 1 | log2(T45, s(s(s(s(0)))), T44), SCOPE: 8, CLAUSE: 2 | log2(T45, s(s(s(s(0)))), T44), SCOPE: 8, CLAUSE: 3\n\nT45 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
335 [label="335: log2(T45, s(s(s(s(0)))), T44), SCOPE: 8, CLAUSE: 1\n\nT45 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
336 [label="336: log2(T45, s(s(s(s(0)))), T44), SCOPE: 8, CLAUSE: 2 | log2(T45, s(s(s(s(0)))), T44), SCOPE: 8, CLAUSE: 3\n\nT45 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
340 [label="340: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
341 [label="341: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
342 [label="342: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
362 [label="362: log2(T45, s(s(s(s(0)))), T44), SCOPE: 8, CLAUSE: 2\n\nT45 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
363 [label="363: log2(T45, s(s(s(s(0)))), T44), SCOPE: 8, CLAUSE: 3\n\nT45 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
364 [label="364: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
366 [label="366: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
367 [label="367: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
369 [label="L: ','(half(s(s(T50)), X136), log2(X136, s(s(s(s(s(0))))), T52))\n\nT50 is ground\nX136 is free", fontsize=16, style=filled, fillcolor=lightyellow];
370 [label="370: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
390 [label="390: half(s(s(T50)), X136)\n\nT50 is ground\nX136 is free", fontsize=16, style=filled, fillcolor=lightyellow];
391 [label="M: log2(T53, s(s(s(s(s(0))))), T52)\n\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
402 [label="402: log2(T53, s(s(s(s(s(0))))), T52), SCOPE: 9, CLAUSE: 1 | log2(T53, s(s(s(s(s(0))))), T52), SCOPE: 9, CLAUSE: 2 | log2(T53, s(s(s(s(s(0))))), T52), SCOPE: 9, CLAUSE: 3\n\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
405 [label="405: log2(T53, s(s(s(s(s(0))))), T52), SCOPE: 9, CLAUSE: 1\n\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
406 [label="406: log2(T53, s(s(s(s(s(0))))), T52), SCOPE: 9, CLAUSE: 2 | log2(T53, s(s(s(s(s(0))))), T52), SCOPE: 9, CLAUSE: 3\n\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
407 [label="407: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
408 [label="408: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
409 [label="409: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
410 [label="410: log2(T53, s(s(s(s(s(0))))), T52), SCOPE: 9, CLAUSE: 2\n\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
411 [label="411: log2(T53, s(s(s(s(s(0))))), T52), SCOPE: 9, CLAUSE: 3\n\nT53 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
412 [label="412: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
413 [label="413: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
414 [label="414: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
415 [label="N: ','(half(s(s(T58)), X159), log2(X159, s(s(s(s(s(s(0)))))), T60))\n\nT58 is ground\nX159 is free", fontsize=16, style=filled, fillcolor=lightyellow];
416 [label="416: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
417 [label="417: half(s(s(T58)), X159)\n\nT58 is ground\nX159 is free", fontsize=16, style=filled, fillcolor=lightyellow];
418 [label="O: log2(T61, s(s(s(s(s(s(0)))))), T60)\n\nT61 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
419 [label="419: log2(T61, s(s(s(s(s(s(0)))))), T60), SCOPE: 10, CLAUSE: 1 | log2(T61, s(s(s(s(s(s(0)))))), T60), SCOPE: 10, CLAUSE: 2 | log2(T61, s(s(s(s(s(s(0)))))), T60), SCOPE: 10, CLAUSE: 3\n\nT61 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
420 [label="420: log2(T61, s(s(s(s(s(s(0)))))), T60), SCOPE: 10, CLAUSE: 1\n\nT61 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
421 [label="421: log2(T61, s(s(s(s(s(s(0)))))), T60), SCOPE: 10, CLAUSE: 2 | log2(T61, s(s(s(s(s(s(0)))))), T60), SCOPE: 10, CLAUSE: 3\n\nT61 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
422 [label="422: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
423 [label="423: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
424 [label="424: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
425 [label="425: log2(T61, s(s(s(s(s(s(0)))))), T60), SCOPE: 10, CLAUSE: 2\n\nT61 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
426 [label="426: log2(T61, s(s(s(s(s(s(0)))))), T60), SCOPE: 10, CLAUSE: 3\n\nT61 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
427 [label="427: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
428 [label="428: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
429 [label="429: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
430 [label="P: ','(half(s(s(T66)), X182), log2(X182, s(s(s(s(s(s(s(0))))))), T68))\n\nT66 is ground\nX182 is free", fontsize=16, style=filled, fillcolor=lightyellow];
431 [label="431: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
432 [label="432: half(s(s(T66)), X182)\n\nT66 is ground\nX182 is free", fontsize=16, style=filled, fillcolor=lightyellow];
433 [label="Q: log2(T69, s(s(s(s(s(s(s(0))))))), T68)\n\nT69 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
434 [label="434: log2(T69, s(s(s(s(s(s(s(0))))))), T68), SCOPE: 11, CLAUSE: 1 | log2(T69, s(s(s(s(s(s(s(0))))))), T68), SCOPE: 11, CLAUSE: 2 | log2(T69, s(s(s(s(s(s(s(0))))))), T68), SCOPE: 11, CLAUSE: 3\n\nT69 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
435 [label="435: log2(T69, s(s(s(s(s(s(s(0))))))), T68), SCOPE: 11, CLAUSE: 1\n\nT69 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
436 [label="436: log2(T69, s(s(s(s(s(s(s(0))))))), T68), SCOPE: 11, CLAUSE: 2 | log2(T69, s(s(s(s(s(s(s(0))))))), T68), SCOPE: 11, CLAUSE: 3\n\nT69 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
437 [label="437: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
438 [label="438: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
439 [label="439: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
440 [label="440: log2(T69, s(s(s(s(s(s(s(0))))))), T68), SCOPE: 11, CLAUSE: 2\n\nT69 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
441 [label="441: log2(T69, s(s(s(s(s(s(s(0))))))), T68), SCOPE: 11, CLAUSE: 3\n\nT69 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
442 [label="442: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
443 [label="443: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
444 [label="444: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
445 [label="445: ','(half(s(s(T74)), X205), log2(X205, s(s(s(s(s(s(s(s(0)))))))), T76))\n\nT74 is ground\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
446 [label="446: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
447 [label="R: ','(half(s(s(T74)), X205), log2(X205, s(T77), T76))\n\nT74 is ground\nT77 is ground\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
448 [label="448: half(s(s(T74)), X205)\n\nT74 is ground\nX205 is free", fontsize=16, style=filled, fillcolor=lightyellow];
449 [label="S: log2(T78, s(T77), T76)\n\nT77 is ground\nT78 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
450 [label="450: log2(T78, s(T77), T76), SCOPE: 12, CLAUSE: 1 | log2(T78, s(T77), T76), SCOPE: 12, CLAUSE: 2 | log2(T78, s(T77), T76), SCOPE: 12, CLAUSE: 3\n\nT77 is ground\nT78 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
451 [label="451: log2(T78, s(T77), T76), SCOPE: 12, CLAUSE: 1\n\nT77 is ground\nT78 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
452 [label="452: log2(T78, s(T77), T76), SCOPE: 12, CLAUSE: 2 | log2(T78, s(T77), T76), SCOPE: 12, CLAUSE: 3\n\nT77 is ground\nT78 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
453 [label="453: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
454 [label="454: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
455 [label="455: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
456 [label="456: log2(T78, s(T77), T76), SCOPE: 12, CLAUSE: 2\n\nT77 is ground\nT78 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
457 [label="457: log2(T78, s(T77), T76), SCOPE: 12, CLAUSE: 3\n\nT77 is ground\nT78 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
458 [label="458: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
459 [label="459: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
460 [label="460: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
461 [label="461: ','(half(s(s(T97)), X228), log2(X228, s(s(T98)), T100))\n\nT97 is ground\nT98 is ground\nX228 is free", fontsize=16, style=filled, fillcolor=lightyellow];
462 [label="462: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
463 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 463 [arrowhead = none ];
463 -> 4;

464 [label="ONLY EVAL with clause\nlog2(X4, X5) :- log2(X4, 0, X5).\nand substitutionT1 -> T5,\nX4 -> T5,\nT2 -> T7,\nX5 -> T7,\nT6 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 464 [arrowhead = none ];
464 -> 8;

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

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

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

468 [label="EVAL with clause\nlog2(0, X10, X10).\nand substitutionT5 -> 0,\nX10 -> 0,\nT7 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 468 [arrowhead = none ];
468 -> 17;

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

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

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

472 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 472 [arrowhead = none ];
472 -> 20;

473 [label="EVAL with clause\nlog2(s(0), X15, X15).\nand substitutionT5 -> s(0),\nX15 -> 0,\nT7 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 473 [arrowhead = none ];
473 -> 42;

474 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
24 -> 474 [arrowhead = none ];
474 -> 43;

475 [label="EVAL with clause\nlog2(s(s(X23)), X24, X25) :- ','(half(s(s(X23)), X26), log2(X26, s(X24), X25)).\nand substitutionX23 -> T12,\nT5 -> s(s(T12)),\nX24 -> 0,\nT7 -> T14,\nX25 -> T14,\nT13 -> T14", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 475 [arrowhead = none ];
475 -> 49;

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

477 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
42 -> 477 [arrowhead = none ];
477 -> 44;

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

479 [label="SPLIT 2\nnew knowledge:\nT12 is ground\nT15 is ground\nreplacements:X26 -> T15", fontsize=14, style = filled, fillcolor = violet];
49 -> 479 [arrowhead = none ];
479 -> 60;

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

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

482 [label="BACKTRACK\nfor clause: half(0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
61 -> 482 [arrowhead = none ];
482 -> 63;

483 [label="BACKTRACK\nfor clause: half(s(0), 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
63 -> 483 [arrowhead = none ];
483 -> 64;

484 [label="ONLY EVAL with clause\nhalf(s(s(X33)), s(X34)) :- half(X33, X34).\nand substitutionT12 -> T18,\nX33 -> T18,\nX34 -> X35,\nX26 -> s(X35)", fontsize=14, style = filled, fillcolor = lightblue];
64 -> 484 [arrowhead = none ];
484 -> 73;

485 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
73 -> 485 [arrowhead = none ];
485 -> 78;

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

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

488 [label="EVAL with clause\nhalf(0, 0).\nand substitutionT18 -> 0,\nX35 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
79 -> 488 [arrowhead = none ];
488 -> 81;

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

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

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

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

493 [label="EVAL with clause\nhalf(s(0), 0).\nand substitutionT18 -> s(0),\nX35 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
84 -> 493 [arrowhead = none ];
493 -> 89;

494 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
84 -> 494 [arrowhead = none ];
494 -> 90;

495 [label="EVAL with clause\nhalf(s(s(X42)), s(X43)) :- half(X42, X43).\nand substitutionX42 -> T21,\nT18 -> s(s(T21)),\nX43 -> X44,\nX35 -> s(X44)", fontsize=14, style = filled, fillcolor = lightblue];
85 -> 495 [arrowhead = none ];
495 -> 95;

496 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
85 -> 496 [arrowhead = none ];
496 -> 97;

497 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
89 -> 497 [arrowhead = none ];
497 -> 91;

498 [label="INSTANCE with matching:\nT18 -> T21\nX35 -> X44", fontsize=14, style = filled, fillcolor = lightgrey];
95 -> 498 [arrowhead = none , style=dashed];
498 -> 73[style=dashed];

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

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

501 [label="EVAL with clause\nlog2(0, X51, X51).\nand substitutionT15 -> 0,\nX51 -> s(0),\nT14 -> s(0)", fontsize=14, style = filled, fillcolor = lightblue];
111 -> 501 [arrowhead = none ];
501 -> 120;

502 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
111 -> 502 [arrowhead = none ];
502 -> 121;

503 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
112 -> 503 [arrowhead = none ];
503 -> 125;

504 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
112 -> 504 [arrowhead = none ];
504 -> 127;

505 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
120 -> 505 [arrowhead = none ];
505 -> 123;

506 [label="EVAL with clause\nlog2(s(0), X56, X56).\nand substitutionT15 -> s(0),\nX56 -> s(0),\nT14 -> s(0)", fontsize=14, style = filled, fillcolor = lightblue];
125 -> 506 [arrowhead = none ];
506 -> 141;

507 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
125 -> 507 [arrowhead = none ];
507 -> 144;

508 [label="EVAL with clause\nlog2(s(s(X64)), X65, X66) :- ','(half(s(s(X64)), X67), log2(X67, s(X65), X66)).\nand substitutionX64 -> T26,\nT15 -> s(s(T26)),\nX65 -> s(0),\nT14 -> T28,\nX66 -> T28,\nT27 -> T28", fontsize=14, style = filled, fillcolor = lightblue];
127 -> 508 [arrowhead = none ];
508 -> 169;

509 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
127 -> 509 [arrowhead = none ];
509 -> 171;

510 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
141 -> 510 [arrowhead = none ];
510 -> 145;

511 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
169 -> 511 [arrowhead = none ];
511 -> 175;

512 [label="SPLIT 2\nnew knowledge:\nT26 is ground\nT29 is ground\nreplacements:X67 -> T29", fontsize=14, style = filled, fillcolor = violet];
169 -> 512 [arrowhead = none ];
512 -> 176;

513 [label="INSTANCE with matching:\nT12 -> T26\nX26 -> X67", fontsize=14, style = filled, fillcolor = lightgrey];
175 -> 513 [arrowhead = none , style=dashed];
513 -> 59[style=dashed];

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

515 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
199 -> 515 [arrowhead = none ];
515 -> 203;

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

517 [label="EVAL with clause\nlog2(0, X74, X74).\nand substitutionT29 -> 0,\nX74 -> s(s(0)),\nT28 -> s(s(0))", fontsize=14, style = filled, fillcolor = lightblue];
203 -> 517 [arrowhead = none ];
517 -> 213;

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

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

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

521 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
213 -> 521 [arrowhead = none ];
521 -> 217;

522 [label="EVAL with clause\nlog2(s(0), X79, X79).\nand substitutionT29 -> s(0),\nX79 -> s(s(0)),\nT28 -> s(s(0))", fontsize=14, style = filled, fillcolor = lightblue];
219 -> 522 [arrowhead = none ];
522 -> 225;

523 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
219 -> 523 [arrowhead = none ];
523 -> 226;

524 [label="EVAL with clause\nlog2(s(s(X87)), X88, X89) :- ','(half(s(s(X87)), X90), log2(X90, s(X88), X89)).\nand substitutionX87 -> T34,\nT29 -> s(s(T34)),\nX88 -> s(s(0)),\nT28 -> T36,\nX89 -> T36,\nT35 -> T36", fontsize=14, style = filled, fillcolor = lightblue];
221 -> 524 [arrowhead = none ];
524 -> 250;

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

526 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
225 -> 526 [arrowhead = none ];
526 -> 228;

527 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
250 -> 527 [arrowhead = none ];
527 -> 257;

528 [label="SPLIT 2\nnew knowledge:\nT34 is ground\nT37 is ground\nreplacements:X90 -> T37", fontsize=14, style = filled, fillcolor = violet];
250 -> 528 [arrowhead = none ];
528 -> 258;

529 [label="INSTANCE with matching:\nT12 -> T34\nX26 -> X90", fontsize=14, style = filled, fillcolor = lightgrey];
257 -> 529 [arrowhead = none , style=dashed];
529 -> 59[style=dashed];

530 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
258 -> 530 [arrowhead = none ];
530 -> 267;

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

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

533 [label="EVAL with clause\nlog2(0, X97, X97).\nand substitutionT37 -> 0,\nX97 -> s(s(s(0))),\nT36 -> s(s(s(0)))", fontsize=14, style = filled, fillcolor = lightblue];
269 -> 533 [arrowhead = none ];
533 -> 286;

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

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

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

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

538 [label="EVAL with clause\nlog2(s(0), X102, X102).\nand substitutionT37 -> s(0),\nX102 -> s(s(s(0))),\nT36 -> s(s(s(0)))", fontsize=14, style = filled, fillcolor = lightblue];
293 -> 538 [arrowhead = none ];
538 -> 295;

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

540 [label="EVAL with clause\nlog2(s(s(X110)), X111, X112) :- ','(half(s(s(X110)), X113), log2(X113, s(X111), X112)).\nand substitutionX110 -> T42,\nT37 -> s(s(T42)),\nX111 -> s(s(s(0))),\nT36 -> T44,\nX112 -> T44,\nT43 -> T44", fontsize=14, style = filled, fillcolor = lightblue];
294 -> 540 [arrowhead = none ];
540 -> 305;

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

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

543 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
305 -> 543 [arrowhead = none ];
543 -> 325;

544 [label="SPLIT 2\nnew knowledge:\nT42 is ground\nT45 is ground\nreplacements:X113 -> T45", fontsize=14, style = filled, fillcolor = violet];
305 -> 544 [arrowhead = none ];
544 -> 326;

545 [label="INSTANCE with matching:\nT12 -> T42\nX26 -> X113", fontsize=14, style = filled, fillcolor = lightgrey];
325 -> 545 [arrowhead = none , style=dashed];
545 -> 59[style=dashed];

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

547 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
330 -> 547 [arrowhead = none ];
547 -> 335;

548 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
330 -> 548 [arrowhead = none ];
548 -> 336;

549 [label="EVAL with clause\nlog2(0, X120, X120).\nand substitutionT45 -> 0,\nX120 -> s(s(s(s(0)))),\nT44 -> s(s(s(s(0))))", fontsize=14, style = filled, fillcolor = lightblue];
335 -> 549 [arrowhead = none ];
549 -> 340;

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

551 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
336 -> 551 [arrowhead = none ];
551 -> 362;

552 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
336 -> 552 [arrowhead = none ];
552 -> 363;

553 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
340 -> 553 [arrowhead = none ];
553 -> 342;

554 [label="EVAL with clause\nlog2(s(0), X125, X125).\nand substitutionT45 -> s(0),\nX125 -> s(s(s(s(0)))),\nT44 -> s(s(s(s(0))))", fontsize=14, style = filled, fillcolor = lightblue];
362 -> 554 [arrowhead = none ];
554 -> 364;

555 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
362 -> 555 [arrowhead = none ];
555 -> 366;

556 [label="EVAL with clause\nlog2(s(s(X133)), X134, X135) :- ','(half(s(s(X133)), X136), log2(X136, s(X134), X135)).\nand substitutionX133 -> T50,\nT45 -> s(s(T50)),\nX134 -> s(s(s(s(0)))),\nT44 -> T52,\nX135 -> T52,\nT51 -> T52", fontsize=14, style = filled, fillcolor = lightblue];
363 -> 556 [arrowhead = none ];
556 -> 369;

557 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
363 -> 557 [arrowhead = none ];
557 -> 370;

558 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
364 -> 558 [arrowhead = none ];
558 -> 367;

559 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
369 -> 559 [arrowhead = none ];
559 -> 390;

560 [label="SPLIT 2\nnew knowledge:\nT50 is ground\nT53 is ground\nreplacements:X136 -> T53", fontsize=14, style = filled, fillcolor = violet];
369 -> 560 [arrowhead = none ];
560 -> 391;

561 [label="INSTANCE with matching:\nT12 -> T50\nX26 -> X136", fontsize=14, style = filled, fillcolor = lightgrey];
390 -> 561 [arrowhead = none , style=dashed];
561 -> 59[style=dashed];

562 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
391 -> 562 [arrowhead = none ];
562 -> 402;

563 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
402 -> 563 [arrowhead = none ];
563 -> 405;

564 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
402 -> 564 [arrowhead = none ];
564 -> 406;

565 [label="EVAL with clause\nlog2(0, X143, X143).\nand substitutionT53 -> 0,\nX143 -> s(s(s(s(s(0))))),\nT52 -> s(s(s(s(s(0)))))", fontsize=14, style = filled, fillcolor = lightblue];
405 -> 565 [arrowhead = none ];
565 -> 407;

566 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
405 -> 566 [arrowhead = none ];
566 -> 408;

567 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
406 -> 567 [arrowhead = none ];
567 -> 410;

568 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
406 -> 568 [arrowhead = none ];
568 -> 411;

569 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
407 -> 569 [arrowhead = none ];
569 -> 409;

570 [label="EVAL with clause\nlog2(s(0), X148, X148).\nand substitutionT53 -> s(0),\nX148 -> s(s(s(s(s(0))))),\nT52 -> s(s(s(s(s(0)))))", fontsize=14, style = filled, fillcolor = lightblue];
410 -> 570 [arrowhead = none ];
570 -> 412;

571 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
410 -> 571 [arrowhead = none ];
571 -> 413;

572 [label="EVAL with clause\nlog2(s(s(X156)), X157, X158) :- ','(half(s(s(X156)), X159), log2(X159, s(X157), X158)).\nand substitutionX156 -> T58,\nT53 -> s(s(T58)),\nX157 -> s(s(s(s(s(0))))),\nT52 -> T60,\nX158 -> T60,\nT59 -> T60", fontsize=14, style = filled, fillcolor = lightblue];
411 -> 572 [arrowhead = none ];
572 -> 415;

573 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
411 -> 573 [arrowhead = none ];
573 -> 416;

574 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
412 -> 574 [arrowhead = none ];
574 -> 414;

575 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
415 -> 575 [arrowhead = none ];
575 -> 417;

576 [label="SPLIT 2\nnew knowledge:\nT58 is ground\nT61 is ground\nreplacements:X159 -> T61", fontsize=14, style = filled, fillcolor = violet];
415 -> 576 [arrowhead = none ];
576 -> 418;

577 [label="INSTANCE with matching:\nT12 -> T58\nX26 -> X159", fontsize=14, style = filled, fillcolor = lightgrey];
417 -> 577 [arrowhead = none , style=dashed];
577 -> 59[style=dashed];

578 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
418 -> 578 [arrowhead = none ];
578 -> 419;

579 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
419 -> 579 [arrowhead = none ];
579 -> 420;

580 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
419 -> 580 [arrowhead = none ];
580 -> 421;

581 [label="EVAL with clause\nlog2(0, X166, X166).\nand substitutionT61 -> 0,\nX166 -> s(s(s(s(s(s(0)))))),\nT60 -> s(s(s(s(s(s(0))))))", fontsize=14, style = filled, fillcolor = lightblue];
420 -> 581 [arrowhead = none ];
581 -> 422;

582 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
420 -> 582 [arrowhead = none ];
582 -> 423;

583 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
421 -> 583 [arrowhead = none ];
583 -> 425;

584 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
421 -> 584 [arrowhead = none ];
584 -> 426;

585 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
422 -> 585 [arrowhead = none ];
585 -> 424;

586 [label="EVAL with clause\nlog2(s(0), X171, X171).\nand substitutionT61 -> s(0),\nX171 -> s(s(s(s(s(s(0)))))),\nT60 -> s(s(s(s(s(s(0))))))", fontsize=14, style = filled, fillcolor = lightblue];
425 -> 586 [arrowhead = none ];
586 -> 427;

587 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
425 -> 587 [arrowhead = none ];
587 -> 428;

588 [label="EVAL with clause\nlog2(s(s(X179)), X180, X181) :- ','(half(s(s(X179)), X182), log2(X182, s(X180), X181)).\nand substitutionX179 -> T66,\nT61 -> s(s(T66)),\nX180 -> s(s(s(s(s(s(0)))))),\nT60 -> T68,\nX181 -> T68,\nT67 -> T68", fontsize=14, style = filled, fillcolor = lightblue];
426 -> 588 [arrowhead = none ];
588 -> 430;

589 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
426 -> 589 [arrowhead = none ];
589 -> 431;

590 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
427 -> 590 [arrowhead = none ];
590 -> 429;

591 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
430 -> 591 [arrowhead = none ];
591 -> 432;

592 [label="SPLIT 2\nnew knowledge:\nT66 is ground\nT69 is ground\nreplacements:X182 -> T69", fontsize=14, style = filled, fillcolor = violet];
430 -> 592 [arrowhead = none ];
592 -> 433;

593 [label="INSTANCE with matching:\nT12 -> T66\nX26 -> X182", fontsize=14, style = filled, fillcolor = lightgrey];
432 -> 593 [arrowhead = none , style=dashed];
593 -> 59[style=dashed];

594 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
433 -> 594 [arrowhead = none ];
594 -> 434;

595 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
434 -> 595 [arrowhead = none ];
595 -> 435;

596 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
434 -> 596 [arrowhead = none ];
596 -> 436;

597 [label="EVAL with clause\nlog2(0, X189, X189).\nand substitutionT69 -> 0,\nX189 -> s(s(s(s(s(s(s(0))))))),\nT68 -> s(s(s(s(s(s(s(0)))))))", fontsize=14, style = filled, fillcolor = lightblue];
435 -> 597 [arrowhead = none ];
597 -> 437;

598 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
435 -> 598 [arrowhead = none ];
598 -> 438;

599 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
436 -> 599 [arrowhead = none ];
599 -> 440;

600 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
436 -> 600 [arrowhead = none ];
600 -> 441;

601 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
437 -> 601 [arrowhead = none ];
601 -> 439;

602 [label="EVAL with clause\nlog2(s(0), X194, X194).\nand substitutionT69 -> s(0),\nX194 -> s(s(s(s(s(s(s(0))))))),\nT68 -> s(s(s(s(s(s(s(0)))))))", fontsize=14, style = filled, fillcolor = lightblue];
440 -> 602 [arrowhead = none ];
602 -> 442;

603 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
440 -> 603 [arrowhead = none ];
603 -> 443;

604 [label="EVAL with clause\nlog2(s(s(X202)), X203, X204) :- ','(half(s(s(X202)), X205), log2(X205, s(X203), X204)).\nand substitutionX202 -> T74,\nT69 -> s(s(T74)),\nX203 -> s(s(s(s(s(s(s(0))))))),\nT68 -> T76,\nX204 -> T76,\nT75 -> T76", fontsize=14, style = filled, fillcolor = lightblue];
441 -> 604 [arrowhead = none ];
604 -> 445;

605 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
441 -> 605 [arrowhead = none ];
605 -> 446;

606 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
442 -> 606 [arrowhead = none ];
606 -> 444;

607 [label="GENERALIZATION\nT77 <-- s(s(s(s(s(s(s(0)))))))\n\nNew Knowledge:\nT77 is ground", fontsize=14, style = filled, fillcolor = violet];
445 -> 607 [arrowhead = none ];
607 -> 447;

608 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
447 -> 608 [arrowhead = none ];
608 -> 448;

609 [label="SPLIT 2\nnew knowledge:\nT74 is ground\nT78 is ground\nreplacements:X205 -> T78", fontsize=14, style = filled, fillcolor = violet];
447 -> 609 [arrowhead = none ];
609 -> 449;

610 [label="INSTANCE with matching:\nT12 -> T74\nX26 -> X205", fontsize=14, style = filled, fillcolor = lightgrey];
448 -> 610 [arrowhead = none , style=dashed];
610 -> 59[style=dashed];

611 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
449 -> 611 [arrowhead = none ];
611 -> 450;

612 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
450 -> 612 [arrowhead = none ];
612 -> 451;

613 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
450 -> 613 [arrowhead = none ];
613 -> 452;

614 [label="EVAL with clause\nlog2(0, X212, X212).\nand substitutionT78 -> 0,\nT77 -> T85,\nX212 -> s(T85),\nT76 -> s(T85)", fontsize=14, style = filled, fillcolor = lightblue];
451 -> 614 [arrowhead = none ];
614 -> 453;

615 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
451 -> 615 [arrowhead = none ];
615 -> 454;

616 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
452 -> 616 [arrowhead = none ];
616 -> 456;

617 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
452 -> 617 [arrowhead = none ];
617 -> 457;

618 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
453 -> 618 [arrowhead = none ];
618 -> 455;

619 [label="EVAL with clause\nlog2(s(0), X217, X217).\nand substitutionT78 -> s(0),\nT77 -> T90,\nX217 -> s(T90),\nT76 -> s(T90)", fontsize=14, style = filled, fillcolor = lightblue];
456 -> 619 [arrowhead = none ];
619 -> 458;

620 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
456 -> 620 [arrowhead = none ];
620 -> 459;

621 [label="EVAL with clause\nlog2(s(s(X225)), X226, X227) :- ','(half(s(s(X225)), X228), log2(X228, s(X226), X227)).\nand substitutionX225 -> T97,\nT78 -> s(s(T97)),\nT77 -> T98,\nX226 -> s(T98),\nT76 -> T100,\nX227 -> T100,\nT99 -> T100", fontsize=14, style = filled, fillcolor = lightblue];
457 -> 621 [arrowhead = none ];
621 -> 461;

622 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
457 -> 622 [arrowhead = none ];
622 -> 462;

623 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
458 -> 623 [arrowhead = none ];
623 -> 460;

624 [label="INSTANCE with matching:\nT74 -> T97\nX205 -> X228\nT77 -> s(T98)\nT76 -> T100", fontsize=14, style = filled, fillcolor = lightgrey];
461 -> 624 [arrowhead = none , style=dashed];
624 -> 447[style=dashed];

}

(2) Obligation:

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

log2A_in_ga(0, 0) → log2A_out_ga(0, 0)
log2A_in_ga(s(0), 0) → log2A_out_ga(s(0), 0)
log2A_in_ga(s(s(T12)), T14) → U1_ga(T12, T14, pB_in_gaa(T12, X26, T14))
pB_in_gaa(T12, T15, T14) → U12_gaa(T12, T15, T14, halfD_in_ga(T12, T15))
halfD_in_ga(T18, s(X35)) → U3_ga(T18, X35, halfC_in_ga(T18, X35))
halfC_in_ga(0, 0) → halfC_out_ga(0, 0)
halfC_in_ga(s(0), 0) → halfC_out_ga(s(0), 0)
halfC_in_ga(s(s(T21)), s(X44)) → U2_ga(T21, X44, halfC_in_ga(T21, X44))
U2_ga(T21, X44, halfC_out_ga(T21, X44)) → halfC_out_ga(s(s(T21)), s(X44))
U3_ga(T18, X35, halfC_out_ga(T18, X35)) → halfD_out_ga(T18, s(X35))
U12_gaa(T12, T15, T14, halfD_out_ga(T12, T15)) → U13_gaa(T12, T15, T14, log2E_in_ga(T15, T14))
log2E_in_ga(0, s(0)) → log2E_out_ga(0, s(0))
log2E_in_ga(s(0), s(0)) → log2E_out_ga(s(0), s(0))
log2E_in_ga(s(s(T26)), T28) → U4_ga(T26, T28, pF_in_gaa(T26, X67, T28))
pF_in_gaa(T26, T29, T28) → U14_gaa(T26, T29, T28, halfD_in_ga(T26, T29))
U14_gaa(T26, T29, T28, halfD_out_ga(T26, T29)) → U15_gaa(T26, T29, T28, log2G_in_ga(T29, T28))
log2G_in_ga(0, s(s(0))) → log2G_out_ga(0, s(s(0)))
log2G_in_ga(s(0), s(s(0))) → log2G_out_ga(s(0), s(s(0)))
log2G_in_ga(s(s(T34)), T36) → U5_ga(T34, T36, pH_in_gaa(T34, X90, T36))
pH_in_gaa(T34, T37, T36) → U16_gaa(T34, T37, T36, halfD_in_ga(T34, T37))
U16_gaa(T34, T37, T36, halfD_out_ga(T34, T37)) → U17_gaa(T34, T37, T36, log2I_in_ga(T37, T36))
log2I_in_ga(0, s(s(s(0)))) → log2I_out_ga(0, s(s(s(0))))
log2I_in_ga(s(0), s(s(s(0)))) → log2I_out_ga(s(0), s(s(s(0))))
log2I_in_ga(s(s(T42)), T44) → U6_ga(T42, T44, pJ_in_gaa(T42, X113, T44))
pJ_in_gaa(T42, T45, T44) → U18_gaa(T42, T45, T44, halfD_in_ga(T42, T45))
U18_gaa(T42, T45, T44, halfD_out_ga(T42, T45)) → U19_gaa(T42, T45, T44, log2K_in_ga(T45, T44))
log2K_in_ga(0, s(s(s(s(0))))) → log2K_out_ga(0, s(s(s(s(0)))))
log2K_in_ga(s(0), s(s(s(s(0))))) → log2K_out_ga(s(0), s(s(s(s(0)))))
log2K_in_ga(s(s(T50)), T52) → U7_ga(T50, T52, pL_in_gaa(T50, X136, T52))
pL_in_gaa(T50, T53, T52) → U20_gaa(T50, T53, T52, halfD_in_ga(T50, T53))
U20_gaa(T50, T53, T52, halfD_out_ga(T50, T53)) → U21_gaa(T50, T53, T52, log2M_in_ga(T53, T52))
log2M_in_ga(0, s(s(s(s(s(0)))))) → log2M_out_ga(0, s(s(s(s(s(0))))))
log2M_in_ga(s(0), s(s(s(s(s(0)))))) → log2M_out_ga(s(0), s(s(s(s(s(0))))))
log2M_in_ga(s(s(T58)), T60) → U8_ga(T58, T60, pN_in_gaa(T58, X159, T60))
pN_in_gaa(T58, T61, T60) → U22_gaa(T58, T61, T60, halfD_in_ga(T58, T61))
U22_gaa(T58, T61, T60, halfD_out_ga(T58, T61)) → U23_gaa(T58, T61, T60, log2O_in_ga(T61, T60))
log2O_in_ga(0, s(s(s(s(s(s(0))))))) → log2O_out_ga(0, s(s(s(s(s(s(0)))))))
log2O_in_ga(s(0), s(s(s(s(s(s(0))))))) → log2O_out_ga(s(0), s(s(s(s(s(s(0)))))))
log2O_in_ga(s(s(T66)), T68) → U9_ga(T66, T68, pP_in_gaa(T66, X182, T68))
pP_in_gaa(T66, T69, T68) → U24_gaa(T66, T69, T68, halfD_in_ga(T66, T69))
U24_gaa(T66, T69, T68, halfD_out_ga(T66, T69)) → U25_gaa(T66, T69, T68, log2Q_in_ga(T69, T68))
log2Q_in_ga(0, s(s(s(s(s(s(s(0)))))))) → log2Q_out_ga(0, s(s(s(s(s(s(s(0))))))))
log2Q_in_ga(s(0), s(s(s(s(s(s(s(0)))))))) → log2Q_out_ga(s(0), s(s(s(s(s(s(s(0))))))))
log2Q_in_ga(s(s(T74)), T76) → U10_ga(T74, T76, pR_in_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76))
pR_in_gaga(T74, T78, T77, T76) → U26_gaga(T74, T78, T77, T76, halfD_in_ga(T74, T78))
U26_gaga(T74, T78, T77, T76, halfD_out_ga(T74, T78)) → U27_gaga(T74, T78, T77, T76, log2S_in_gga(T78, T77, T76))
log2S_in_gga(0, T85, s(T85)) → log2S_out_gga(0, T85, s(T85))
log2S_in_gga(s(0), T90, s(T90)) → log2S_out_gga(s(0), T90, s(T90))
log2S_in_gga(s(s(T97)), T98, T100) → U11_gga(T97, T98, T100, pR_in_gaga(T97, X228, s(T98), T100))
U11_gga(T97, T98, T100, pR_out_gaga(T97, X228, s(T98), T100)) → log2S_out_gga(s(s(T97)), T98, T100)
U27_gaga(T74, T78, T77, T76, log2S_out_gga(T78, T77, T76)) → pR_out_gaga(T74, T78, T77, T76)
U10_ga(T74, T76, pR_out_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76)) → log2Q_out_ga(s(s(T74)), T76)
U25_gaa(T66, T69, T68, log2Q_out_ga(T69, T68)) → pP_out_gaa(T66, T69, T68)
U9_ga(T66, T68, pP_out_gaa(T66, X182, T68)) → log2O_out_ga(s(s(T66)), T68)
U23_gaa(T58, T61, T60, log2O_out_ga(T61, T60)) → pN_out_gaa(T58, T61, T60)
U8_ga(T58, T60, pN_out_gaa(T58, X159, T60)) → log2M_out_ga(s(s(T58)), T60)
U21_gaa(T50, T53, T52, log2M_out_ga(T53, T52)) → pL_out_gaa(T50, T53, T52)
U7_ga(T50, T52, pL_out_gaa(T50, X136, T52)) → log2K_out_ga(s(s(T50)), T52)
U19_gaa(T42, T45, T44, log2K_out_ga(T45, T44)) → pJ_out_gaa(T42, T45, T44)
U6_ga(T42, T44, pJ_out_gaa(T42, X113, T44)) → log2I_out_ga(s(s(T42)), T44)
U17_gaa(T34, T37, T36, log2I_out_ga(T37, T36)) → pH_out_gaa(T34, T37, T36)
U5_ga(T34, T36, pH_out_gaa(T34, X90, T36)) → log2G_out_ga(s(s(T34)), T36)
U15_gaa(T26, T29, T28, log2G_out_ga(T29, T28)) → pF_out_gaa(T26, T29, T28)
U4_ga(T26, T28, pF_out_gaa(T26, X67, T28)) → log2E_out_ga(s(s(T26)), T28)
U13_gaa(T12, T15, T14, log2E_out_ga(T15, T14)) → pB_out_gaa(T12, T15, T14)
U1_ga(T12, T14, pB_out_gaa(T12, X26, T14)) → log2A_out_ga(s(s(T12)), T14)

The argument filtering Pi contains the following mapping:
log2A_in_ga(x1, x2)  =  log2A_in_ga(x1)
0  =  0
log2A_out_ga(x1, x2)  =  log2A_out_ga(x1, x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U12_gaa(x1, x2, x3, x4)  =  U12_gaa(x1, x4)
halfD_in_ga(x1, x2)  =  halfD_in_ga(x1)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
halfC_in_ga(x1, x2)  =  halfC_in_ga(x1)
halfC_out_ga(x1, x2)  =  halfC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
halfD_out_ga(x1, x2)  =  halfD_out_ga(x1, x2)
U13_gaa(x1, x2, x3, x4)  =  U13_gaa(x1, x2, x4)
log2E_in_ga(x1, x2)  =  log2E_in_ga(x1)
log2E_out_ga(x1, x2)  =  log2E_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pF_in_gaa(x1, x2, x3)  =  pF_in_gaa(x1)
U14_gaa(x1, x2, x3, x4)  =  U14_gaa(x1, x4)
U15_gaa(x1, x2, x3, x4)  =  U15_gaa(x1, x2, x4)
log2G_in_ga(x1, x2)  =  log2G_in_ga(x1)
log2G_out_ga(x1, x2)  =  log2G_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
pH_in_gaa(x1, x2, x3)  =  pH_in_gaa(x1)
U16_gaa(x1, x2, x3, x4)  =  U16_gaa(x1, x4)
U17_gaa(x1, x2, x3, x4)  =  U17_gaa(x1, x2, x4)
log2I_in_ga(x1, x2)  =  log2I_in_ga(x1)
log2I_out_ga(x1, x2)  =  log2I_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
pJ_in_gaa(x1, x2, x3)  =  pJ_in_gaa(x1)
U18_gaa(x1, x2, x3, x4)  =  U18_gaa(x1, x4)
U19_gaa(x1, x2, x3, x4)  =  U19_gaa(x1, x2, x4)
log2K_in_ga(x1, x2)  =  log2K_in_ga(x1)
log2K_out_ga(x1, x2)  =  log2K_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
pL_in_gaa(x1, x2, x3)  =  pL_in_gaa(x1)
U20_gaa(x1, x2, x3, x4)  =  U20_gaa(x1, x4)
U21_gaa(x1, x2, x3, x4)  =  U21_gaa(x1, x2, x4)
log2M_in_ga(x1, x2)  =  log2M_in_ga(x1)
log2M_out_ga(x1, x2)  =  log2M_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
pN_in_gaa(x1, x2, x3)  =  pN_in_gaa(x1)
U22_gaa(x1, x2, x3, x4)  =  U22_gaa(x1, x4)
U23_gaa(x1, x2, x3, x4)  =  U23_gaa(x1, x2, x4)
log2O_in_ga(x1, x2)  =  log2O_in_ga(x1)
log2O_out_ga(x1, x2)  =  log2O_out_ga(x1, x2)
U9_ga(x1, x2, x3)  =  U9_ga(x1, x3)
pP_in_gaa(x1, x2, x3)  =  pP_in_gaa(x1)
U24_gaa(x1, x2, x3, x4)  =  U24_gaa(x1, x4)
U25_gaa(x1, x2, x3, x4)  =  U25_gaa(x1, x2, x4)
log2Q_in_ga(x1, x2)  =  log2Q_in_ga(x1)
log2Q_out_ga(x1, x2)  =  log2Q_out_ga(x1, x2)
U10_ga(x1, x2, x3)  =  U10_ga(x1, x3)
pR_in_gaga(x1, x2, x3, x4)  =  pR_in_gaga(x1, x3)
U26_gaga(x1, x2, x3, x4, x5)  =  U26_gaga(x1, x3, x5)
U27_gaga(x1, x2, x3, x4, x5)  =  U27_gaga(x1, x2, x3, x5)
log2S_in_gga(x1, x2, x3)  =  log2S_in_gga(x1, x2)
log2S_out_gga(x1, x2, x3)  =  log2S_out_gga(x1, x2, x3)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x2, x4)
pR_out_gaga(x1, x2, x3, x4)  =  pR_out_gaga(x1, x2, x3, x4)
pP_out_gaa(x1, x2, x3)  =  pP_out_gaa(x1, x2, x3)
pN_out_gaa(x1, x2, x3)  =  pN_out_gaa(x1, x2, x3)
pL_out_gaa(x1, x2, x3)  =  pL_out_gaa(x1, x2, x3)
pJ_out_gaa(x1, x2, x3)  =  pJ_out_gaa(x1, x2, x3)
pH_out_gaa(x1, x2, x3)  =  pH_out_gaa(x1, x2, x3)
pF_out_gaa(x1, x2, x3)  =  pF_out_gaa(x1, x2, x3)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2, x3)

(3) DependencyPairsProof (EQUIVALENT transformation)

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

LOG2A_IN_GA(s(s(T12)), T14) → U1_GA(T12, T14, pB_in_gaa(T12, X26, T14))
LOG2A_IN_GA(s(s(T12)), T14) → PB_IN_GAA(T12, X26, T14)
PB_IN_GAA(T12, T15, T14) → U12_GAA(T12, T15, T14, halfD_in_ga(T12, T15))
PB_IN_GAA(T12, T15, T14) → HALFD_IN_GA(T12, T15)
HALFD_IN_GA(T18, s(X35)) → U3_GA(T18, X35, halfC_in_ga(T18, X35))
HALFD_IN_GA(T18, s(X35)) → HALFC_IN_GA(T18, X35)
HALFC_IN_GA(s(s(T21)), s(X44)) → U2_GA(T21, X44, halfC_in_ga(T21, X44))
HALFC_IN_GA(s(s(T21)), s(X44)) → HALFC_IN_GA(T21, X44)
U12_GAA(T12, T15, T14, halfD_out_ga(T12, T15)) → U13_GAA(T12, T15, T14, log2E_in_ga(T15, T14))
U12_GAA(T12, T15, T14, halfD_out_ga(T12, T15)) → LOG2E_IN_GA(T15, T14)
LOG2E_IN_GA(s(s(T26)), T28) → U4_GA(T26, T28, pF_in_gaa(T26, X67, T28))
LOG2E_IN_GA(s(s(T26)), T28) → PF_IN_GAA(T26, X67, T28)
PF_IN_GAA(T26, T29, T28) → U14_GAA(T26, T29, T28, halfD_in_ga(T26, T29))
PF_IN_GAA(T26, T29, T28) → HALFD_IN_GA(T26, T29)
U14_GAA(T26, T29, T28, halfD_out_ga(T26, T29)) → U15_GAA(T26, T29, T28, log2G_in_ga(T29, T28))
U14_GAA(T26, T29, T28, halfD_out_ga(T26, T29)) → LOG2G_IN_GA(T29, T28)
LOG2G_IN_GA(s(s(T34)), T36) → U5_GA(T34, T36, pH_in_gaa(T34, X90, T36))
LOG2G_IN_GA(s(s(T34)), T36) → PH_IN_GAA(T34, X90, T36)
PH_IN_GAA(T34, T37, T36) → U16_GAA(T34, T37, T36, halfD_in_ga(T34, T37))
PH_IN_GAA(T34, T37, T36) → HALFD_IN_GA(T34, T37)
U16_GAA(T34, T37, T36, halfD_out_ga(T34, T37)) → U17_GAA(T34, T37, T36, log2I_in_ga(T37, T36))
U16_GAA(T34, T37, T36, halfD_out_ga(T34, T37)) → LOG2I_IN_GA(T37, T36)
LOG2I_IN_GA(s(s(T42)), T44) → U6_GA(T42, T44, pJ_in_gaa(T42, X113, T44))
LOG2I_IN_GA(s(s(T42)), T44) → PJ_IN_GAA(T42, X113, T44)
PJ_IN_GAA(T42, T45, T44) → U18_GAA(T42, T45, T44, halfD_in_ga(T42, T45))
PJ_IN_GAA(T42, T45, T44) → HALFD_IN_GA(T42, T45)
U18_GAA(T42, T45, T44, halfD_out_ga(T42, T45)) → U19_GAA(T42, T45, T44, log2K_in_ga(T45, T44))
U18_GAA(T42, T45, T44, halfD_out_ga(T42, T45)) → LOG2K_IN_GA(T45, T44)
LOG2K_IN_GA(s(s(T50)), T52) → U7_GA(T50, T52, pL_in_gaa(T50, X136, T52))
LOG2K_IN_GA(s(s(T50)), T52) → PL_IN_GAA(T50, X136, T52)
PL_IN_GAA(T50, T53, T52) → U20_GAA(T50, T53, T52, halfD_in_ga(T50, T53))
PL_IN_GAA(T50, T53, T52) → HALFD_IN_GA(T50, T53)
U20_GAA(T50, T53, T52, halfD_out_ga(T50, T53)) → U21_GAA(T50, T53, T52, log2M_in_ga(T53, T52))
U20_GAA(T50, T53, T52, halfD_out_ga(T50, T53)) → LOG2M_IN_GA(T53, T52)
LOG2M_IN_GA(s(s(T58)), T60) → U8_GA(T58, T60, pN_in_gaa(T58, X159, T60))
LOG2M_IN_GA(s(s(T58)), T60) → PN_IN_GAA(T58, X159, T60)
PN_IN_GAA(T58, T61, T60) → U22_GAA(T58, T61, T60, halfD_in_ga(T58, T61))
PN_IN_GAA(T58, T61, T60) → HALFD_IN_GA(T58, T61)
U22_GAA(T58, T61, T60, halfD_out_ga(T58, T61)) → U23_GAA(T58, T61, T60, log2O_in_ga(T61, T60))
U22_GAA(T58, T61, T60, halfD_out_ga(T58, T61)) → LOG2O_IN_GA(T61, T60)
LOG2O_IN_GA(s(s(T66)), T68) → U9_GA(T66, T68, pP_in_gaa(T66, X182, T68))
LOG2O_IN_GA(s(s(T66)), T68) → PP_IN_GAA(T66, X182, T68)
PP_IN_GAA(T66, T69, T68) → U24_GAA(T66, T69, T68, halfD_in_ga(T66, T69))
PP_IN_GAA(T66, T69, T68) → HALFD_IN_GA(T66, T69)
U24_GAA(T66, T69, T68, halfD_out_ga(T66, T69)) → U25_GAA(T66, T69, T68, log2Q_in_ga(T69, T68))
U24_GAA(T66, T69, T68, halfD_out_ga(T66, T69)) → LOG2Q_IN_GA(T69, T68)
LOG2Q_IN_GA(s(s(T74)), T76) → U10_GA(T74, T76, pR_in_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76))
LOG2Q_IN_GA(s(s(T74)), T76) → PR_IN_GAGA(T74, X205, s(s(s(s(s(s(s(0))))))), T76)
PR_IN_GAGA(T74, T78, T77, T76) → U26_GAGA(T74, T78, T77, T76, halfD_in_ga(T74, T78))
PR_IN_GAGA(T74, T78, T77, T76) → HALFD_IN_GA(T74, T78)
U26_GAGA(T74, T78, T77, T76, halfD_out_ga(T74, T78)) → U27_GAGA(T74, T78, T77, T76, log2S_in_gga(T78, T77, T76))
U26_GAGA(T74, T78, T77, T76, halfD_out_ga(T74, T78)) → LOG2S_IN_GGA(T78, T77, T76)
LOG2S_IN_GGA(s(s(T97)), T98, T100) → U11_GGA(T97, T98, T100, pR_in_gaga(T97, X228, s(T98), T100))
LOG2S_IN_GGA(s(s(T97)), T98, T100) → PR_IN_GAGA(T97, X228, s(T98), T100)

The TRS R consists of the following rules:

log2A_in_ga(0, 0) → log2A_out_ga(0, 0)
log2A_in_ga(s(0), 0) → log2A_out_ga(s(0), 0)
log2A_in_ga(s(s(T12)), T14) → U1_ga(T12, T14, pB_in_gaa(T12, X26, T14))
pB_in_gaa(T12, T15, T14) → U12_gaa(T12, T15, T14, halfD_in_ga(T12, T15))
halfD_in_ga(T18, s(X35)) → U3_ga(T18, X35, halfC_in_ga(T18, X35))
halfC_in_ga(0, 0) → halfC_out_ga(0, 0)
halfC_in_ga(s(0), 0) → halfC_out_ga(s(0), 0)
halfC_in_ga(s(s(T21)), s(X44)) → U2_ga(T21, X44, halfC_in_ga(T21, X44))
U2_ga(T21, X44, halfC_out_ga(T21, X44)) → halfC_out_ga(s(s(T21)), s(X44))
U3_ga(T18, X35, halfC_out_ga(T18, X35)) → halfD_out_ga(T18, s(X35))
U12_gaa(T12, T15, T14, halfD_out_ga(T12, T15)) → U13_gaa(T12, T15, T14, log2E_in_ga(T15, T14))
log2E_in_ga(0, s(0)) → log2E_out_ga(0, s(0))
log2E_in_ga(s(0), s(0)) → log2E_out_ga(s(0), s(0))
log2E_in_ga(s(s(T26)), T28) → U4_ga(T26, T28, pF_in_gaa(T26, X67, T28))
pF_in_gaa(T26, T29, T28) → U14_gaa(T26, T29, T28, halfD_in_ga(T26, T29))
U14_gaa(T26, T29, T28, halfD_out_ga(T26, T29)) → U15_gaa(T26, T29, T28, log2G_in_ga(T29, T28))
log2G_in_ga(0, s(s(0))) → log2G_out_ga(0, s(s(0)))
log2G_in_ga(s(0), s(s(0))) → log2G_out_ga(s(0), s(s(0)))
log2G_in_ga(s(s(T34)), T36) → U5_ga(T34, T36, pH_in_gaa(T34, X90, T36))
pH_in_gaa(T34, T37, T36) → U16_gaa(T34, T37, T36, halfD_in_ga(T34, T37))
U16_gaa(T34, T37, T36, halfD_out_ga(T34, T37)) → U17_gaa(T34, T37, T36, log2I_in_ga(T37, T36))
log2I_in_ga(0, s(s(s(0)))) → log2I_out_ga(0, s(s(s(0))))
log2I_in_ga(s(0), s(s(s(0)))) → log2I_out_ga(s(0), s(s(s(0))))
log2I_in_ga(s(s(T42)), T44) → U6_ga(T42, T44, pJ_in_gaa(T42, X113, T44))
pJ_in_gaa(T42, T45, T44) → U18_gaa(T42, T45, T44, halfD_in_ga(T42, T45))
U18_gaa(T42, T45, T44, halfD_out_ga(T42, T45)) → U19_gaa(T42, T45, T44, log2K_in_ga(T45, T44))
log2K_in_ga(0, s(s(s(s(0))))) → log2K_out_ga(0, s(s(s(s(0)))))
log2K_in_ga(s(0), s(s(s(s(0))))) → log2K_out_ga(s(0), s(s(s(s(0)))))
log2K_in_ga(s(s(T50)), T52) → U7_ga(T50, T52, pL_in_gaa(T50, X136, T52))
pL_in_gaa(T50, T53, T52) → U20_gaa(T50, T53, T52, halfD_in_ga(T50, T53))
U20_gaa(T50, T53, T52, halfD_out_ga(T50, T53)) → U21_gaa(T50, T53, T52, log2M_in_ga(T53, T52))
log2M_in_ga(0, s(s(s(s(s(0)))))) → log2M_out_ga(0, s(s(s(s(s(0))))))
log2M_in_ga(s(0), s(s(s(s(s(0)))))) → log2M_out_ga(s(0), s(s(s(s(s(0))))))
log2M_in_ga(s(s(T58)), T60) → U8_ga(T58, T60, pN_in_gaa(T58, X159, T60))
pN_in_gaa(T58, T61, T60) → U22_gaa(T58, T61, T60, halfD_in_ga(T58, T61))
U22_gaa(T58, T61, T60, halfD_out_ga(T58, T61)) → U23_gaa(T58, T61, T60, log2O_in_ga(T61, T60))
log2O_in_ga(0, s(s(s(s(s(s(0))))))) → log2O_out_ga(0, s(s(s(s(s(s(0)))))))
log2O_in_ga(s(0), s(s(s(s(s(s(0))))))) → log2O_out_ga(s(0), s(s(s(s(s(s(0)))))))
log2O_in_ga(s(s(T66)), T68) → U9_ga(T66, T68, pP_in_gaa(T66, X182, T68))
pP_in_gaa(T66, T69, T68) → U24_gaa(T66, T69, T68, halfD_in_ga(T66, T69))
U24_gaa(T66, T69, T68, halfD_out_ga(T66, T69)) → U25_gaa(T66, T69, T68, log2Q_in_ga(T69, T68))
log2Q_in_ga(0, s(s(s(s(s(s(s(0)))))))) → log2Q_out_ga(0, s(s(s(s(s(s(s(0))))))))
log2Q_in_ga(s(0), s(s(s(s(s(s(s(0)))))))) → log2Q_out_ga(s(0), s(s(s(s(s(s(s(0))))))))
log2Q_in_ga(s(s(T74)), T76) → U10_ga(T74, T76, pR_in_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76))
pR_in_gaga(T74, T78, T77, T76) → U26_gaga(T74, T78, T77, T76, halfD_in_ga(T74, T78))
U26_gaga(T74, T78, T77, T76, halfD_out_ga(T74, T78)) → U27_gaga(T74, T78, T77, T76, log2S_in_gga(T78, T77, T76))
log2S_in_gga(0, T85, s(T85)) → log2S_out_gga(0, T85, s(T85))
log2S_in_gga(s(0), T90, s(T90)) → log2S_out_gga(s(0), T90, s(T90))
log2S_in_gga(s(s(T97)), T98, T100) → U11_gga(T97, T98, T100, pR_in_gaga(T97, X228, s(T98), T100))
U11_gga(T97, T98, T100, pR_out_gaga(T97, X228, s(T98), T100)) → log2S_out_gga(s(s(T97)), T98, T100)
U27_gaga(T74, T78, T77, T76, log2S_out_gga(T78, T77, T76)) → pR_out_gaga(T74, T78, T77, T76)
U10_ga(T74, T76, pR_out_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76)) → log2Q_out_ga(s(s(T74)), T76)
U25_gaa(T66, T69, T68, log2Q_out_ga(T69, T68)) → pP_out_gaa(T66, T69, T68)
U9_ga(T66, T68, pP_out_gaa(T66, X182, T68)) → log2O_out_ga(s(s(T66)), T68)
U23_gaa(T58, T61, T60, log2O_out_ga(T61, T60)) → pN_out_gaa(T58, T61, T60)
U8_ga(T58, T60, pN_out_gaa(T58, X159, T60)) → log2M_out_ga(s(s(T58)), T60)
U21_gaa(T50, T53, T52, log2M_out_ga(T53, T52)) → pL_out_gaa(T50, T53, T52)
U7_ga(T50, T52, pL_out_gaa(T50, X136, T52)) → log2K_out_ga(s(s(T50)), T52)
U19_gaa(T42, T45, T44, log2K_out_ga(T45, T44)) → pJ_out_gaa(T42, T45, T44)
U6_ga(T42, T44, pJ_out_gaa(T42, X113, T44)) → log2I_out_ga(s(s(T42)), T44)
U17_gaa(T34, T37, T36, log2I_out_ga(T37, T36)) → pH_out_gaa(T34, T37, T36)
U5_ga(T34, T36, pH_out_gaa(T34, X90, T36)) → log2G_out_ga(s(s(T34)), T36)
U15_gaa(T26, T29, T28, log2G_out_ga(T29, T28)) → pF_out_gaa(T26, T29, T28)
U4_ga(T26, T28, pF_out_gaa(T26, X67, T28)) → log2E_out_ga(s(s(T26)), T28)
U13_gaa(T12, T15, T14, log2E_out_ga(T15, T14)) → pB_out_gaa(T12, T15, T14)
U1_ga(T12, T14, pB_out_gaa(T12, X26, T14)) → log2A_out_ga(s(s(T12)), T14)

The argument filtering Pi contains the following mapping:
log2A_in_ga(x1, x2)  =  log2A_in_ga(x1)
0  =  0
log2A_out_ga(x1, x2)  =  log2A_out_ga(x1, x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U12_gaa(x1, x2, x3, x4)  =  U12_gaa(x1, x4)
halfD_in_ga(x1, x2)  =  halfD_in_ga(x1)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
halfC_in_ga(x1, x2)  =  halfC_in_ga(x1)
halfC_out_ga(x1, x2)  =  halfC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
halfD_out_ga(x1, x2)  =  halfD_out_ga(x1, x2)
U13_gaa(x1, x2, x3, x4)  =  U13_gaa(x1, x2, x4)
log2E_in_ga(x1, x2)  =  log2E_in_ga(x1)
log2E_out_ga(x1, x2)  =  log2E_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pF_in_gaa(x1, x2, x3)  =  pF_in_gaa(x1)
U14_gaa(x1, x2, x3, x4)  =  U14_gaa(x1, x4)
U15_gaa(x1, x2, x3, x4)  =  U15_gaa(x1, x2, x4)
log2G_in_ga(x1, x2)  =  log2G_in_ga(x1)
log2G_out_ga(x1, x2)  =  log2G_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
pH_in_gaa(x1, x2, x3)  =  pH_in_gaa(x1)
U16_gaa(x1, x2, x3, x4)  =  U16_gaa(x1, x4)
U17_gaa(x1, x2, x3, x4)  =  U17_gaa(x1, x2, x4)
log2I_in_ga(x1, x2)  =  log2I_in_ga(x1)
log2I_out_ga(x1, x2)  =  log2I_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
pJ_in_gaa(x1, x2, x3)  =  pJ_in_gaa(x1)
U18_gaa(x1, x2, x3, x4)  =  U18_gaa(x1, x4)
U19_gaa(x1, x2, x3, x4)  =  U19_gaa(x1, x2, x4)
log2K_in_ga(x1, x2)  =  log2K_in_ga(x1)
log2K_out_ga(x1, x2)  =  log2K_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
pL_in_gaa(x1, x2, x3)  =  pL_in_gaa(x1)
U20_gaa(x1, x2, x3, x4)  =  U20_gaa(x1, x4)
U21_gaa(x1, x2, x3, x4)  =  U21_gaa(x1, x2, x4)
log2M_in_ga(x1, x2)  =  log2M_in_ga(x1)
log2M_out_ga(x1, x2)  =  log2M_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
pN_in_gaa(x1, x2, x3)  =  pN_in_gaa(x1)
U22_gaa(x1, x2, x3, x4)  =  U22_gaa(x1, x4)
U23_gaa(x1, x2, x3, x4)  =  U23_gaa(x1, x2, x4)
log2O_in_ga(x1, x2)  =  log2O_in_ga(x1)
log2O_out_ga(x1, x2)  =  log2O_out_ga(x1, x2)
U9_ga(x1, x2, x3)  =  U9_ga(x1, x3)
pP_in_gaa(x1, x2, x3)  =  pP_in_gaa(x1)
U24_gaa(x1, x2, x3, x4)  =  U24_gaa(x1, x4)
U25_gaa(x1, x2, x3, x4)  =  U25_gaa(x1, x2, x4)
log2Q_in_ga(x1, x2)  =  log2Q_in_ga(x1)
log2Q_out_ga(x1, x2)  =  log2Q_out_ga(x1, x2)
U10_ga(x1, x2, x3)  =  U10_ga(x1, x3)
pR_in_gaga(x1, x2, x3, x4)  =  pR_in_gaga(x1, x3)
U26_gaga(x1, x2, x3, x4, x5)  =  U26_gaga(x1, x3, x5)
U27_gaga(x1, x2, x3, x4, x5)  =  U27_gaga(x1, x2, x3, x5)
log2S_in_gga(x1, x2, x3)  =  log2S_in_gga(x1, x2)
log2S_out_gga(x1, x2, x3)  =  log2S_out_gga(x1, x2, x3)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x2, x4)
pR_out_gaga(x1, x2, x3, x4)  =  pR_out_gaga(x1, x2, x3, x4)
pP_out_gaa(x1, x2, x3)  =  pP_out_gaa(x1, x2, x3)
pN_out_gaa(x1, x2, x3)  =  pN_out_gaa(x1, x2, x3)
pL_out_gaa(x1, x2, x3)  =  pL_out_gaa(x1, x2, x3)
pJ_out_gaa(x1, x2, x3)  =  pJ_out_gaa(x1, x2, x3)
pH_out_gaa(x1, x2, x3)  =  pH_out_gaa(x1, x2, x3)
pF_out_gaa(x1, x2, x3)  =  pF_out_gaa(x1, x2, x3)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2, x3)
LOG2A_IN_GA(x1, x2)  =  LOG2A_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
PB_IN_GAA(x1, x2, x3)  =  PB_IN_GAA(x1)
U12_GAA(x1, x2, x3, x4)  =  U12_GAA(x1, x4)
HALFD_IN_GA(x1, x2)  =  HALFD_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
HALFC_IN_GA(x1, x2)  =  HALFC_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U13_GAA(x1, x2, x3, x4)  =  U13_GAA(x1, x2, x4)
LOG2E_IN_GA(x1, x2)  =  LOG2E_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
PF_IN_GAA(x1, x2, x3)  =  PF_IN_GAA(x1)
U14_GAA(x1, x2, x3, x4)  =  U14_GAA(x1, x4)
U15_GAA(x1, x2, x3, x4)  =  U15_GAA(x1, x2, x4)
LOG2G_IN_GA(x1, x2)  =  LOG2G_IN_GA(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
PH_IN_GAA(x1, x2, x3)  =  PH_IN_GAA(x1)
U16_GAA(x1, x2, x3, x4)  =  U16_GAA(x1, x4)
U17_GAA(x1, x2, x3, x4)  =  U17_GAA(x1, x2, x4)
LOG2I_IN_GA(x1, x2)  =  LOG2I_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
PJ_IN_GAA(x1, x2, x3)  =  PJ_IN_GAA(x1)
U18_GAA(x1, x2, x3, x4)  =  U18_GAA(x1, x4)
U19_GAA(x1, x2, x3, x4)  =  U19_GAA(x1, x2, x4)
LOG2K_IN_GA(x1, x2)  =  LOG2K_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x1, x3)
PL_IN_GAA(x1, x2, x3)  =  PL_IN_GAA(x1)
U20_GAA(x1, x2, x3, x4)  =  U20_GAA(x1, x4)
U21_GAA(x1, x2, x3, x4)  =  U21_GAA(x1, x2, x4)
LOG2M_IN_GA(x1, x2)  =  LOG2M_IN_GA(x1)
U8_GA(x1, x2, x3)  =  U8_GA(x1, x3)
PN_IN_GAA(x1, x2, x3)  =  PN_IN_GAA(x1)
U22_GAA(x1, x2, x3, x4)  =  U22_GAA(x1, x4)
U23_GAA(x1, x2, x3, x4)  =  U23_GAA(x1, x2, x4)
LOG2O_IN_GA(x1, x2)  =  LOG2O_IN_GA(x1)
U9_GA(x1, x2, x3)  =  U9_GA(x1, x3)
PP_IN_GAA(x1, x2, x3)  =  PP_IN_GAA(x1)
U24_GAA(x1, x2, x3, x4)  =  U24_GAA(x1, x4)
U25_GAA(x1, x2, x3, x4)  =  U25_GAA(x1, x2, x4)
LOG2Q_IN_GA(x1, x2)  =  LOG2Q_IN_GA(x1)
U10_GA(x1, x2, x3)  =  U10_GA(x1, x3)
PR_IN_GAGA(x1, x2, x3, x4)  =  PR_IN_GAGA(x1, x3)
U26_GAGA(x1, x2, x3, x4, x5)  =  U26_GAGA(x1, x3, x5)
U27_GAGA(x1, x2, x3, x4, x5)  =  U27_GAGA(x1, x2, x3, x5)
LOG2S_IN_GGA(x1, x2, x3)  =  LOG2S_IN_GGA(x1, x2)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x1, x2, x4)

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

(4) Obligation:

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

LOG2A_IN_GA(s(s(T12)), T14) → U1_GA(T12, T14, pB_in_gaa(T12, X26, T14))
LOG2A_IN_GA(s(s(T12)), T14) → PB_IN_GAA(T12, X26, T14)
PB_IN_GAA(T12, T15, T14) → U12_GAA(T12, T15, T14, halfD_in_ga(T12, T15))
PB_IN_GAA(T12, T15, T14) → HALFD_IN_GA(T12, T15)
HALFD_IN_GA(T18, s(X35)) → U3_GA(T18, X35, halfC_in_ga(T18, X35))
HALFD_IN_GA(T18, s(X35)) → HALFC_IN_GA(T18, X35)
HALFC_IN_GA(s(s(T21)), s(X44)) → U2_GA(T21, X44, halfC_in_ga(T21, X44))
HALFC_IN_GA(s(s(T21)), s(X44)) → HALFC_IN_GA(T21, X44)
U12_GAA(T12, T15, T14, halfD_out_ga(T12, T15)) → U13_GAA(T12, T15, T14, log2E_in_ga(T15, T14))
U12_GAA(T12, T15, T14, halfD_out_ga(T12, T15)) → LOG2E_IN_GA(T15, T14)
LOG2E_IN_GA(s(s(T26)), T28) → U4_GA(T26, T28, pF_in_gaa(T26, X67, T28))
LOG2E_IN_GA(s(s(T26)), T28) → PF_IN_GAA(T26, X67, T28)
PF_IN_GAA(T26, T29, T28) → U14_GAA(T26, T29, T28, halfD_in_ga(T26, T29))
PF_IN_GAA(T26, T29, T28) → HALFD_IN_GA(T26, T29)
U14_GAA(T26, T29, T28, halfD_out_ga(T26, T29)) → U15_GAA(T26, T29, T28, log2G_in_ga(T29, T28))
U14_GAA(T26, T29, T28, halfD_out_ga(T26, T29)) → LOG2G_IN_GA(T29, T28)
LOG2G_IN_GA(s(s(T34)), T36) → U5_GA(T34, T36, pH_in_gaa(T34, X90, T36))
LOG2G_IN_GA(s(s(T34)), T36) → PH_IN_GAA(T34, X90, T36)
PH_IN_GAA(T34, T37, T36) → U16_GAA(T34, T37, T36, halfD_in_ga(T34, T37))
PH_IN_GAA(T34, T37, T36) → HALFD_IN_GA(T34, T37)
U16_GAA(T34, T37, T36, halfD_out_ga(T34, T37)) → U17_GAA(T34, T37, T36, log2I_in_ga(T37, T36))
U16_GAA(T34, T37, T36, halfD_out_ga(T34, T37)) → LOG2I_IN_GA(T37, T36)
LOG2I_IN_GA(s(s(T42)), T44) → U6_GA(T42, T44, pJ_in_gaa(T42, X113, T44))
LOG2I_IN_GA(s(s(T42)), T44) → PJ_IN_GAA(T42, X113, T44)
PJ_IN_GAA(T42, T45, T44) → U18_GAA(T42, T45, T44, halfD_in_ga(T42, T45))
PJ_IN_GAA(T42, T45, T44) → HALFD_IN_GA(T42, T45)
U18_GAA(T42, T45, T44, halfD_out_ga(T42, T45)) → U19_GAA(T42, T45, T44, log2K_in_ga(T45, T44))
U18_GAA(T42, T45, T44, halfD_out_ga(T42, T45)) → LOG2K_IN_GA(T45, T44)
LOG2K_IN_GA(s(s(T50)), T52) → U7_GA(T50, T52, pL_in_gaa(T50, X136, T52))
LOG2K_IN_GA(s(s(T50)), T52) → PL_IN_GAA(T50, X136, T52)
PL_IN_GAA(T50, T53, T52) → U20_GAA(T50, T53, T52, halfD_in_ga(T50, T53))
PL_IN_GAA(T50, T53, T52) → HALFD_IN_GA(T50, T53)
U20_GAA(T50, T53, T52, halfD_out_ga(T50, T53)) → U21_GAA(T50, T53, T52, log2M_in_ga(T53, T52))
U20_GAA(T50, T53, T52, halfD_out_ga(T50, T53)) → LOG2M_IN_GA(T53, T52)
LOG2M_IN_GA(s(s(T58)), T60) → U8_GA(T58, T60, pN_in_gaa(T58, X159, T60))
LOG2M_IN_GA(s(s(T58)), T60) → PN_IN_GAA(T58, X159, T60)
PN_IN_GAA(T58, T61, T60) → U22_GAA(T58, T61, T60, halfD_in_ga(T58, T61))
PN_IN_GAA(T58, T61, T60) → HALFD_IN_GA(T58, T61)
U22_GAA(T58, T61, T60, halfD_out_ga(T58, T61)) → U23_GAA(T58, T61, T60, log2O_in_ga(T61, T60))
U22_GAA(T58, T61, T60, halfD_out_ga(T58, T61)) → LOG2O_IN_GA(T61, T60)
LOG2O_IN_GA(s(s(T66)), T68) → U9_GA(T66, T68, pP_in_gaa(T66, X182, T68))
LOG2O_IN_GA(s(s(T66)), T68) → PP_IN_GAA(T66, X182, T68)
PP_IN_GAA(T66, T69, T68) → U24_GAA(T66, T69, T68, halfD_in_ga(T66, T69))
PP_IN_GAA(T66, T69, T68) → HALFD_IN_GA(T66, T69)
U24_GAA(T66, T69, T68, halfD_out_ga(T66, T69)) → U25_GAA(T66, T69, T68, log2Q_in_ga(T69, T68))
U24_GAA(T66, T69, T68, halfD_out_ga(T66, T69)) → LOG2Q_IN_GA(T69, T68)
LOG2Q_IN_GA(s(s(T74)), T76) → U10_GA(T74, T76, pR_in_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76))
LOG2Q_IN_GA(s(s(T74)), T76) → PR_IN_GAGA(T74, X205, s(s(s(s(s(s(s(0))))))), T76)
PR_IN_GAGA(T74, T78, T77, T76) → U26_GAGA(T74, T78, T77, T76, halfD_in_ga(T74, T78))
PR_IN_GAGA(T74, T78, T77, T76) → HALFD_IN_GA(T74, T78)
U26_GAGA(T74, T78, T77, T76, halfD_out_ga(T74, T78)) → U27_GAGA(T74, T78, T77, T76, log2S_in_gga(T78, T77, T76))
U26_GAGA(T74, T78, T77, T76, halfD_out_ga(T74, T78)) → LOG2S_IN_GGA(T78, T77, T76)
LOG2S_IN_GGA(s(s(T97)), T98, T100) → U11_GGA(T97, T98, T100, pR_in_gaga(T97, X228, s(T98), T100))
LOG2S_IN_GGA(s(s(T97)), T98, T100) → PR_IN_GAGA(T97, X228, s(T98), T100)

The TRS R consists of the following rules:

log2A_in_ga(0, 0) → log2A_out_ga(0, 0)
log2A_in_ga(s(0), 0) → log2A_out_ga(s(0), 0)
log2A_in_ga(s(s(T12)), T14) → U1_ga(T12, T14, pB_in_gaa(T12, X26, T14))
pB_in_gaa(T12, T15, T14) → U12_gaa(T12, T15, T14, halfD_in_ga(T12, T15))
halfD_in_ga(T18, s(X35)) → U3_ga(T18, X35, halfC_in_ga(T18, X35))
halfC_in_ga(0, 0) → halfC_out_ga(0, 0)
halfC_in_ga(s(0), 0) → halfC_out_ga(s(0), 0)
halfC_in_ga(s(s(T21)), s(X44)) → U2_ga(T21, X44, halfC_in_ga(T21, X44))
U2_ga(T21, X44, halfC_out_ga(T21, X44)) → halfC_out_ga(s(s(T21)), s(X44))
U3_ga(T18, X35, halfC_out_ga(T18, X35)) → halfD_out_ga(T18, s(X35))
U12_gaa(T12, T15, T14, halfD_out_ga(T12, T15)) → U13_gaa(T12, T15, T14, log2E_in_ga(T15, T14))
log2E_in_ga(0, s(0)) → log2E_out_ga(0, s(0))
log2E_in_ga(s(0), s(0)) → log2E_out_ga(s(0), s(0))
log2E_in_ga(s(s(T26)), T28) → U4_ga(T26, T28, pF_in_gaa(T26, X67, T28))
pF_in_gaa(T26, T29, T28) → U14_gaa(T26, T29, T28, halfD_in_ga(T26, T29))
U14_gaa(T26, T29, T28, halfD_out_ga(T26, T29)) → U15_gaa(T26, T29, T28, log2G_in_ga(T29, T28))
log2G_in_ga(0, s(s(0))) → log2G_out_ga(0, s(s(0)))
log2G_in_ga(s(0), s(s(0))) → log2G_out_ga(s(0), s(s(0)))
log2G_in_ga(s(s(T34)), T36) → U5_ga(T34, T36, pH_in_gaa(T34, X90, T36))
pH_in_gaa(T34, T37, T36) → U16_gaa(T34, T37, T36, halfD_in_ga(T34, T37))
U16_gaa(T34, T37, T36, halfD_out_ga(T34, T37)) → U17_gaa(T34, T37, T36, log2I_in_ga(T37, T36))
log2I_in_ga(0, s(s(s(0)))) → log2I_out_ga(0, s(s(s(0))))
log2I_in_ga(s(0), s(s(s(0)))) → log2I_out_ga(s(0), s(s(s(0))))
log2I_in_ga(s(s(T42)), T44) → U6_ga(T42, T44, pJ_in_gaa(T42, X113, T44))
pJ_in_gaa(T42, T45, T44) → U18_gaa(T42, T45, T44, halfD_in_ga(T42, T45))
U18_gaa(T42, T45, T44, halfD_out_ga(T42, T45)) → U19_gaa(T42, T45, T44, log2K_in_ga(T45, T44))
log2K_in_ga(0, s(s(s(s(0))))) → log2K_out_ga(0, s(s(s(s(0)))))
log2K_in_ga(s(0), s(s(s(s(0))))) → log2K_out_ga(s(0), s(s(s(s(0)))))
log2K_in_ga(s(s(T50)), T52) → U7_ga(T50, T52, pL_in_gaa(T50, X136, T52))
pL_in_gaa(T50, T53, T52) → U20_gaa(T50, T53, T52, halfD_in_ga(T50, T53))
U20_gaa(T50, T53, T52, halfD_out_ga(T50, T53)) → U21_gaa(T50, T53, T52, log2M_in_ga(T53, T52))
log2M_in_ga(0, s(s(s(s(s(0)))))) → log2M_out_ga(0, s(s(s(s(s(0))))))
log2M_in_ga(s(0), s(s(s(s(s(0)))))) → log2M_out_ga(s(0), s(s(s(s(s(0))))))
log2M_in_ga(s(s(T58)), T60) → U8_ga(T58, T60, pN_in_gaa(T58, X159, T60))
pN_in_gaa(T58, T61, T60) → U22_gaa(T58, T61, T60, halfD_in_ga(T58, T61))
U22_gaa(T58, T61, T60, halfD_out_ga(T58, T61)) → U23_gaa(T58, T61, T60, log2O_in_ga(T61, T60))
log2O_in_ga(0, s(s(s(s(s(s(0))))))) → log2O_out_ga(0, s(s(s(s(s(s(0)))))))
log2O_in_ga(s(0), s(s(s(s(s(s(0))))))) → log2O_out_ga(s(0), s(s(s(s(s(s(0)))))))
log2O_in_ga(s(s(T66)), T68) → U9_ga(T66, T68, pP_in_gaa(T66, X182, T68))
pP_in_gaa(T66, T69, T68) → U24_gaa(T66, T69, T68, halfD_in_ga(T66, T69))
U24_gaa(T66, T69, T68, halfD_out_ga(T66, T69)) → U25_gaa(T66, T69, T68, log2Q_in_ga(T69, T68))
log2Q_in_ga(0, s(s(s(s(s(s(s(0)))))))) → log2Q_out_ga(0, s(s(s(s(s(s(s(0))))))))
log2Q_in_ga(s(0), s(s(s(s(s(s(s(0)))))))) → log2Q_out_ga(s(0), s(s(s(s(s(s(s(0))))))))
log2Q_in_ga(s(s(T74)), T76) → U10_ga(T74, T76, pR_in_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76))
pR_in_gaga(T74, T78, T77, T76) → U26_gaga(T74, T78, T77, T76, halfD_in_ga(T74, T78))
U26_gaga(T74, T78, T77, T76, halfD_out_ga(T74, T78)) → U27_gaga(T74, T78, T77, T76, log2S_in_gga(T78, T77, T76))
log2S_in_gga(0, T85, s(T85)) → log2S_out_gga(0, T85, s(T85))
log2S_in_gga(s(0), T90, s(T90)) → log2S_out_gga(s(0), T90, s(T90))
log2S_in_gga(s(s(T97)), T98, T100) → U11_gga(T97, T98, T100, pR_in_gaga(T97, X228, s(T98), T100))
U11_gga(T97, T98, T100, pR_out_gaga(T97, X228, s(T98), T100)) → log2S_out_gga(s(s(T97)), T98, T100)
U27_gaga(T74, T78, T77, T76, log2S_out_gga(T78, T77, T76)) → pR_out_gaga(T74, T78, T77, T76)
U10_ga(T74, T76, pR_out_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76)) → log2Q_out_ga(s(s(T74)), T76)
U25_gaa(T66, T69, T68, log2Q_out_ga(T69, T68)) → pP_out_gaa(T66, T69, T68)
U9_ga(T66, T68, pP_out_gaa(T66, X182, T68)) → log2O_out_ga(s(s(T66)), T68)
U23_gaa(T58, T61, T60, log2O_out_ga(T61, T60)) → pN_out_gaa(T58, T61, T60)
U8_ga(T58, T60, pN_out_gaa(T58, X159, T60)) → log2M_out_ga(s(s(T58)), T60)
U21_gaa(T50, T53, T52, log2M_out_ga(T53, T52)) → pL_out_gaa(T50, T53, T52)
U7_ga(T50, T52, pL_out_gaa(T50, X136, T52)) → log2K_out_ga(s(s(T50)), T52)
U19_gaa(T42, T45, T44, log2K_out_ga(T45, T44)) → pJ_out_gaa(T42, T45, T44)
U6_ga(T42, T44, pJ_out_gaa(T42, X113, T44)) → log2I_out_ga(s(s(T42)), T44)
U17_gaa(T34, T37, T36, log2I_out_ga(T37, T36)) → pH_out_gaa(T34, T37, T36)
U5_ga(T34, T36, pH_out_gaa(T34, X90, T36)) → log2G_out_ga(s(s(T34)), T36)
U15_gaa(T26, T29, T28, log2G_out_ga(T29, T28)) → pF_out_gaa(T26, T29, T28)
U4_ga(T26, T28, pF_out_gaa(T26, X67, T28)) → log2E_out_ga(s(s(T26)), T28)
U13_gaa(T12, T15, T14, log2E_out_ga(T15, T14)) → pB_out_gaa(T12, T15, T14)
U1_ga(T12, T14, pB_out_gaa(T12, X26, T14)) → log2A_out_ga(s(s(T12)), T14)

The argument filtering Pi contains the following mapping:
log2A_in_ga(x1, x2)  =  log2A_in_ga(x1)
0  =  0
log2A_out_ga(x1, x2)  =  log2A_out_ga(x1, x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U12_gaa(x1, x2, x3, x4)  =  U12_gaa(x1, x4)
halfD_in_ga(x1, x2)  =  halfD_in_ga(x1)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
halfC_in_ga(x1, x2)  =  halfC_in_ga(x1)
halfC_out_ga(x1, x2)  =  halfC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
halfD_out_ga(x1, x2)  =  halfD_out_ga(x1, x2)
U13_gaa(x1, x2, x3, x4)  =  U13_gaa(x1, x2, x4)
log2E_in_ga(x1, x2)  =  log2E_in_ga(x1)
log2E_out_ga(x1, x2)  =  log2E_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pF_in_gaa(x1, x2, x3)  =  pF_in_gaa(x1)
U14_gaa(x1, x2, x3, x4)  =  U14_gaa(x1, x4)
U15_gaa(x1, x2, x3, x4)  =  U15_gaa(x1, x2, x4)
log2G_in_ga(x1, x2)  =  log2G_in_ga(x1)
log2G_out_ga(x1, x2)  =  log2G_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
pH_in_gaa(x1, x2, x3)  =  pH_in_gaa(x1)
U16_gaa(x1, x2, x3, x4)  =  U16_gaa(x1, x4)
U17_gaa(x1, x2, x3, x4)  =  U17_gaa(x1, x2, x4)
log2I_in_ga(x1, x2)  =  log2I_in_ga(x1)
log2I_out_ga(x1, x2)  =  log2I_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
pJ_in_gaa(x1, x2, x3)  =  pJ_in_gaa(x1)
U18_gaa(x1, x2, x3, x4)  =  U18_gaa(x1, x4)
U19_gaa(x1, x2, x3, x4)  =  U19_gaa(x1, x2, x4)
log2K_in_ga(x1, x2)  =  log2K_in_ga(x1)
log2K_out_ga(x1, x2)  =  log2K_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
pL_in_gaa(x1, x2, x3)  =  pL_in_gaa(x1)
U20_gaa(x1, x2, x3, x4)  =  U20_gaa(x1, x4)
U21_gaa(x1, x2, x3, x4)  =  U21_gaa(x1, x2, x4)
log2M_in_ga(x1, x2)  =  log2M_in_ga(x1)
log2M_out_ga(x1, x2)  =  log2M_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
pN_in_gaa(x1, x2, x3)  =  pN_in_gaa(x1)
U22_gaa(x1, x2, x3, x4)  =  U22_gaa(x1, x4)
U23_gaa(x1, x2, x3, x4)  =  U23_gaa(x1, x2, x4)
log2O_in_ga(x1, x2)  =  log2O_in_ga(x1)
log2O_out_ga(x1, x2)  =  log2O_out_ga(x1, x2)
U9_ga(x1, x2, x3)  =  U9_ga(x1, x3)
pP_in_gaa(x1, x2, x3)  =  pP_in_gaa(x1)
U24_gaa(x1, x2, x3, x4)  =  U24_gaa(x1, x4)
U25_gaa(x1, x2, x3, x4)  =  U25_gaa(x1, x2, x4)
log2Q_in_ga(x1, x2)  =  log2Q_in_ga(x1)
log2Q_out_ga(x1, x2)  =  log2Q_out_ga(x1, x2)
U10_ga(x1, x2, x3)  =  U10_ga(x1, x3)
pR_in_gaga(x1, x2, x3, x4)  =  pR_in_gaga(x1, x3)
U26_gaga(x1, x2, x3, x4, x5)  =  U26_gaga(x1, x3, x5)
U27_gaga(x1, x2, x3, x4, x5)  =  U27_gaga(x1, x2, x3, x5)
log2S_in_gga(x1, x2, x3)  =  log2S_in_gga(x1, x2)
log2S_out_gga(x1, x2, x3)  =  log2S_out_gga(x1, x2, x3)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x2, x4)
pR_out_gaga(x1, x2, x3, x4)  =  pR_out_gaga(x1, x2, x3, x4)
pP_out_gaa(x1, x2, x3)  =  pP_out_gaa(x1, x2, x3)
pN_out_gaa(x1, x2, x3)  =  pN_out_gaa(x1, x2, x3)
pL_out_gaa(x1, x2, x3)  =  pL_out_gaa(x1, x2, x3)
pJ_out_gaa(x1, x2, x3)  =  pJ_out_gaa(x1, x2, x3)
pH_out_gaa(x1, x2, x3)  =  pH_out_gaa(x1, x2, x3)
pF_out_gaa(x1, x2, x3)  =  pF_out_gaa(x1, x2, x3)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2, x3)
LOG2A_IN_GA(x1, x2)  =  LOG2A_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
PB_IN_GAA(x1, x2, x3)  =  PB_IN_GAA(x1)
U12_GAA(x1, x2, x3, x4)  =  U12_GAA(x1, x4)
HALFD_IN_GA(x1, x2)  =  HALFD_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
HALFC_IN_GA(x1, x2)  =  HALFC_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U13_GAA(x1, x2, x3, x4)  =  U13_GAA(x1, x2, x4)
LOG2E_IN_GA(x1, x2)  =  LOG2E_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
PF_IN_GAA(x1, x2, x3)  =  PF_IN_GAA(x1)
U14_GAA(x1, x2, x3, x4)  =  U14_GAA(x1, x4)
U15_GAA(x1, x2, x3, x4)  =  U15_GAA(x1, x2, x4)
LOG2G_IN_GA(x1, x2)  =  LOG2G_IN_GA(x1)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
PH_IN_GAA(x1, x2, x3)  =  PH_IN_GAA(x1)
U16_GAA(x1, x2, x3, x4)  =  U16_GAA(x1, x4)
U17_GAA(x1, x2, x3, x4)  =  U17_GAA(x1, x2, x4)
LOG2I_IN_GA(x1, x2)  =  LOG2I_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
PJ_IN_GAA(x1, x2, x3)  =  PJ_IN_GAA(x1)
U18_GAA(x1, x2, x3, x4)  =  U18_GAA(x1, x4)
U19_GAA(x1, x2, x3, x4)  =  U19_GAA(x1, x2, x4)
LOG2K_IN_GA(x1, x2)  =  LOG2K_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x1, x3)
PL_IN_GAA(x1, x2, x3)  =  PL_IN_GAA(x1)
U20_GAA(x1, x2, x3, x4)  =  U20_GAA(x1, x4)
U21_GAA(x1, x2, x3, x4)  =  U21_GAA(x1, x2, x4)
LOG2M_IN_GA(x1, x2)  =  LOG2M_IN_GA(x1)
U8_GA(x1, x2, x3)  =  U8_GA(x1, x3)
PN_IN_GAA(x1, x2, x3)  =  PN_IN_GAA(x1)
U22_GAA(x1, x2, x3, x4)  =  U22_GAA(x1, x4)
U23_GAA(x1, x2, x3, x4)  =  U23_GAA(x1, x2, x4)
LOG2O_IN_GA(x1, x2)  =  LOG2O_IN_GA(x1)
U9_GA(x1, x2, x3)  =  U9_GA(x1, x3)
PP_IN_GAA(x1, x2, x3)  =  PP_IN_GAA(x1)
U24_GAA(x1, x2, x3, x4)  =  U24_GAA(x1, x4)
U25_GAA(x1, x2, x3, x4)  =  U25_GAA(x1, x2, x4)
LOG2Q_IN_GA(x1, x2)  =  LOG2Q_IN_GA(x1)
U10_GA(x1, x2, x3)  =  U10_GA(x1, x3)
PR_IN_GAGA(x1, x2, x3, x4)  =  PR_IN_GAGA(x1, x3)
U26_GAGA(x1, x2, x3, x4, x5)  =  U26_GAGA(x1, x3, x5)
U27_GAGA(x1, x2, x3, x4, x5)  =  U27_GAGA(x1, x2, x3, x5)
LOG2S_IN_GGA(x1, x2, x3)  =  LOG2S_IN_GGA(x1, x2)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x1, x2, x4)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 50 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

HALFC_IN_GA(s(s(T21)), s(X44)) → HALFC_IN_GA(T21, X44)

The TRS R consists of the following rules:

log2A_in_ga(0, 0) → log2A_out_ga(0, 0)
log2A_in_ga(s(0), 0) → log2A_out_ga(s(0), 0)
log2A_in_ga(s(s(T12)), T14) → U1_ga(T12, T14, pB_in_gaa(T12, X26, T14))
pB_in_gaa(T12, T15, T14) → U12_gaa(T12, T15, T14, halfD_in_ga(T12, T15))
halfD_in_ga(T18, s(X35)) → U3_ga(T18, X35, halfC_in_ga(T18, X35))
halfC_in_ga(0, 0) → halfC_out_ga(0, 0)
halfC_in_ga(s(0), 0) → halfC_out_ga(s(0), 0)
halfC_in_ga(s(s(T21)), s(X44)) → U2_ga(T21, X44, halfC_in_ga(T21, X44))
U2_ga(T21, X44, halfC_out_ga(T21, X44)) → halfC_out_ga(s(s(T21)), s(X44))
U3_ga(T18, X35, halfC_out_ga(T18, X35)) → halfD_out_ga(T18, s(X35))
U12_gaa(T12, T15, T14, halfD_out_ga(T12, T15)) → U13_gaa(T12, T15, T14, log2E_in_ga(T15, T14))
log2E_in_ga(0, s(0)) → log2E_out_ga(0, s(0))
log2E_in_ga(s(0), s(0)) → log2E_out_ga(s(0), s(0))
log2E_in_ga(s(s(T26)), T28) → U4_ga(T26, T28, pF_in_gaa(T26, X67, T28))
pF_in_gaa(T26, T29, T28) → U14_gaa(T26, T29, T28, halfD_in_ga(T26, T29))
U14_gaa(T26, T29, T28, halfD_out_ga(T26, T29)) → U15_gaa(T26, T29, T28, log2G_in_ga(T29, T28))
log2G_in_ga(0, s(s(0))) → log2G_out_ga(0, s(s(0)))
log2G_in_ga(s(0), s(s(0))) → log2G_out_ga(s(0), s(s(0)))
log2G_in_ga(s(s(T34)), T36) → U5_ga(T34, T36, pH_in_gaa(T34, X90, T36))
pH_in_gaa(T34, T37, T36) → U16_gaa(T34, T37, T36, halfD_in_ga(T34, T37))
U16_gaa(T34, T37, T36, halfD_out_ga(T34, T37)) → U17_gaa(T34, T37, T36, log2I_in_ga(T37, T36))
log2I_in_ga(0, s(s(s(0)))) → log2I_out_ga(0, s(s(s(0))))
log2I_in_ga(s(0), s(s(s(0)))) → log2I_out_ga(s(0), s(s(s(0))))
log2I_in_ga(s(s(T42)), T44) → U6_ga(T42, T44, pJ_in_gaa(T42, X113, T44))
pJ_in_gaa(T42, T45, T44) → U18_gaa(T42, T45, T44, halfD_in_ga(T42, T45))
U18_gaa(T42, T45, T44, halfD_out_ga(T42, T45)) → U19_gaa(T42, T45, T44, log2K_in_ga(T45, T44))
log2K_in_ga(0, s(s(s(s(0))))) → log2K_out_ga(0, s(s(s(s(0)))))
log2K_in_ga(s(0), s(s(s(s(0))))) → log2K_out_ga(s(0), s(s(s(s(0)))))
log2K_in_ga(s(s(T50)), T52) → U7_ga(T50, T52, pL_in_gaa(T50, X136, T52))
pL_in_gaa(T50, T53, T52) → U20_gaa(T50, T53, T52, halfD_in_ga(T50, T53))
U20_gaa(T50, T53, T52, halfD_out_ga(T50, T53)) → U21_gaa(T50, T53, T52, log2M_in_ga(T53, T52))
log2M_in_ga(0, s(s(s(s(s(0)))))) → log2M_out_ga(0, s(s(s(s(s(0))))))
log2M_in_ga(s(0), s(s(s(s(s(0)))))) → log2M_out_ga(s(0), s(s(s(s(s(0))))))
log2M_in_ga(s(s(T58)), T60) → U8_ga(T58, T60, pN_in_gaa(T58, X159, T60))
pN_in_gaa(T58, T61, T60) → U22_gaa(T58, T61, T60, halfD_in_ga(T58, T61))
U22_gaa(T58, T61, T60, halfD_out_ga(T58, T61)) → U23_gaa(T58, T61, T60, log2O_in_ga(T61, T60))
log2O_in_ga(0, s(s(s(s(s(s(0))))))) → log2O_out_ga(0, s(s(s(s(s(s(0)))))))
log2O_in_ga(s(0), s(s(s(s(s(s(0))))))) → log2O_out_ga(s(0), s(s(s(s(s(s(0)))))))
log2O_in_ga(s(s(T66)), T68) → U9_ga(T66, T68, pP_in_gaa(T66, X182, T68))
pP_in_gaa(T66, T69, T68) → U24_gaa(T66, T69, T68, halfD_in_ga(T66, T69))
U24_gaa(T66, T69, T68, halfD_out_ga(T66, T69)) → U25_gaa(T66, T69, T68, log2Q_in_ga(T69, T68))
log2Q_in_ga(0, s(s(s(s(s(s(s(0)))))))) → log2Q_out_ga(0, s(s(s(s(s(s(s(0))))))))
log2Q_in_ga(s(0), s(s(s(s(s(s(s(0)))))))) → log2Q_out_ga(s(0), s(s(s(s(s(s(s(0))))))))
log2Q_in_ga(s(s(T74)), T76) → U10_ga(T74, T76, pR_in_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76))
pR_in_gaga(T74, T78, T77, T76) → U26_gaga(T74, T78, T77, T76, halfD_in_ga(T74, T78))
U26_gaga(T74, T78, T77, T76, halfD_out_ga(T74, T78)) → U27_gaga(T74, T78, T77, T76, log2S_in_gga(T78, T77, T76))
log2S_in_gga(0, T85, s(T85)) → log2S_out_gga(0, T85, s(T85))
log2S_in_gga(s(0), T90, s(T90)) → log2S_out_gga(s(0), T90, s(T90))
log2S_in_gga(s(s(T97)), T98, T100) → U11_gga(T97, T98, T100, pR_in_gaga(T97, X228, s(T98), T100))
U11_gga(T97, T98, T100, pR_out_gaga(T97, X228, s(T98), T100)) → log2S_out_gga(s(s(T97)), T98, T100)
U27_gaga(T74, T78, T77, T76, log2S_out_gga(T78, T77, T76)) → pR_out_gaga(T74, T78, T77, T76)
U10_ga(T74, T76, pR_out_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76)) → log2Q_out_ga(s(s(T74)), T76)
U25_gaa(T66, T69, T68, log2Q_out_ga(T69, T68)) → pP_out_gaa(T66, T69, T68)
U9_ga(T66, T68, pP_out_gaa(T66, X182, T68)) → log2O_out_ga(s(s(T66)), T68)
U23_gaa(T58, T61, T60, log2O_out_ga(T61, T60)) → pN_out_gaa(T58, T61, T60)
U8_ga(T58, T60, pN_out_gaa(T58, X159, T60)) → log2M_out_ga(s(s(T58)), T60)
U21_gaa(T50, T53, T52, log2M_out_ga(T53, T52)) → pL_out_gaa(T50, T53, T52)
U7_ga(T50, T52, pL_out_gaa(T50, X136, T52)) → log2K_out_ga(s(s(T50)), T52)
U19_gaa(T42, T45, T44, log2K_out_ga(T45, T44)) → pJ_out_gaa(T42, T45, T44)
U6_ga(T42, T44, pJ_out_gaa(T42, X113, T44)) → log2I_out_ga(s(s(T42)), T44)
U17_gaa(T34, T37, T36, log2I_out_ga(T37, T36)) → pH_out_gaa(T34, T37, T36)
U5_ga(T34, T36, pH_out_gaa(T34, X90, T36)) → log2G_out_ga(s(s(T34)), T36)
U15_gaa(T26, T29, T28, log2G_out_ga(T29, T28)) → pF_out_gaa(T26, T29, T28)
U4_ga(T26, T28, pF_out_gaa(T26, X67, T28)) → log2E_out_ga(s(s(T26)), T28)
U13_gaa(T12, T15, T14, log2E_out_ga(T15, T14)) → pB_out_gaa(T12, T15, T14)
U1_ga(T12, T14, pB_out_gaa(T12, X26, T14)) → log2A_out_ga(s(s(T12)), T14)

The argument filtering Pi contains the following mapping:
log2A_in_ga(x1, x2)  =  log2A_in_ga(x1)
0  =  0
log2A_out_ga(x1, x2)  =  log2A_out_ga(x1, x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U12_gaa(x1, x2, x3, x4)  =  U12_gaa(x1, x4)
halfD_in_ga(x1, x2)  =  halfD_in_ga(x1)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
halfC_in_ga(x1, x2)  =  halfC_in_ga(x1)
halfC_out_ga(x1, x2)  =  halfC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
halfD_out_ga(x1, x2)  =  halfD_out_ga(x1, x2)
U13_gaa(x1, x2, x3, x4)  =  U13_gaa(x1, x2, x4)
log2E_in_ga(x1, x2)  =  log2E_in_ga(x1)
log2E_out_ga(x1, x2)  =  log2E_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pF_in_gaa(x1, x2, x3)  =  pF_in_gaa(x1)
U14_gaa(x1, x2, x3, x4)  =  U14_gaa(x1, x4)
U15_gaa(x1, x2, x3, x4)  =  U15_gaa(x1, x2, x4)
log2G_in_ga(x1, x2)  =  log2G_in_ga(x1)
log2G_out_ga(x1, x2)  =  log2G_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
pH_in_gaa(x1, x2, x3)  =  pH_in_gaa(x1)
U16_gaa(x1, x2, x3, x4)  =  U16_gaa(x1, x4)
U17_gaa(x1, x2, x3, x4)  =  U17_gaa(x1, x2, x4)
log2I_in_ga(x1, x2)  =  log2I_in_ga(x1)
log2I_out_ga(x1, x2)  =  log2I_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
pJ_in_gaa(x1, x2, x3)  =  pJ_in_gaa(x1)
U18_gaa(x1, x2, x3, x4)  =  U18_gaa(x1, x4)
U19_gaa(x1, x2, x3, x4)  =  U19_gaa(x1, x2, x4)
log2K_in_ga(x1, x2)  =  log2K_in_ga(x1)
log2K_out_ga(x1, x2)  =  log2K_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
pL_in_gaa(x1, x2, x3)  =  pL_in_gaa(x1)
U20_gaa(x1, x2, x3, x4)  =  U20_gaa(x1, x4)
U21_gaa(x1, x2, x3, x4)  =  U21_gaa(x1, x2, x4)
log2M_in_ga(x1, x2)  =  log2M_in_ga(x1)
log2M_out_ga(x1, x2)  =  log2M_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
pN_in_gaa(x1, x2, x3)  =  pN_in_gaa(x1)
U22_gaa(x1, x2, x3, x4)  =  U22_gaa(x1, x4)
U23_gaa(x1, x2, x3, x4)  =  U23_gaa(x1, x2, x4)
log2O_in_ga(x1, x2)  =  log2O_in_ga(x1)
log2O_out_ga(x1, x2)  =  log2O_out_ga(x1, x2)
U9_ga(x1, x2, x3)  =  U9_ga(x1, x3)
pP_in_gaa(x1, x2, x3)  =  pP_in_gaa(x1)
U24_gaa(x1, x2, x3, x4)  =  U24_gaa(x1, x4)
U25_gaa(x1, x2, x3, x4)  =  U25_gaa(x1, x2, x4)
log2Q_in_ga(x1, x2)  =  log2Q_in_ga(x1)
log2Q_out_ga(x1, x2)  =  log2Q_out_ga(x1, x2)
U10_ga(x1, x2, x3)  =  U10_ga(x1, x3)
pR_in_gaga(x1, x2, x3, x4)  =  pR_in_gaga(x1, x3)
U26_gaga(x1, x2, x3, x4, x5)  =  U26_gaga(x1, x3, x5)
U27_gaga(x1, x2, x3, x4, x5)  =  U27_gaga(x1, x2, x3, x5)
log2S_in_gga(x1, x2, x3)  =  log2S_in_gga(x1, x2)
log2S_out_gga(x1, x2, x3)  =  log2S_out_gga(x1, x2, x3)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x2, x4)
pR_out_gaga(x1, x2, x3, x4)  =  pR_out_gaga(x1, x2, x3, x4)
pP_out_gaa(x1, x2, x3)  =  pP_out_gaa(x1, x2, x3)
pN_out_gaa(x1, x2, x3)  =  pN_out_gaa(x1, x2, x3)
pL_out_gaa(x1, x2, x3)  =  pL_out_gaa(x1, x2, x3)
pJ_out_gaa(x1, x2, x3)  =  pJ_out_gaa(x1, x2, x3)
pH_out_gaa(x1, x2, x3)  =  pH_out_gaa(x1, x2, x3)
pF_out_gaa(x1, x2, x3)  =  pF_out_gaa(x1, x2, x3)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2, x3)
HALFC_IN_GA(x1, x2)  =  HALFC_IN_GA(x1)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

HALFC_IN_GA(s(s(T21)), s(X44)) → HALFC_IN_GA(T21, X44)

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

HALFC_IN_GA(s(s(T21))) → HALFC_IN_GA(T21)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• HALFC_IN_GA(s(s(T21))) → HALFC_IN_GA(T21)
  The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

PR_IN_GAGA(T74, T78, T77, T76) → U26_GAGA(T74, T78, T77, T76, halfD_in_ga(T74, T78))
U26_GAGA(T74, T78, T77, T76, halfD_out_ga(T74, T78)) → LOG2S_IN_GGA(T78, T77, T76)
LOG2S_IN_GGA(s(s(T97)), T98, T100) → PR_IN_GAGA(T97, X228, s(T98), T100)

The TRS R consists of the following rules:

log2A_in_ga(0, 0) → log2A_out_ga(0, 0)
log2A_in_ga(s(0), 0) → log2A_out_ga(s(0), 0)
log2A_in_ga(s(s(T12)), T14) → U1_ga(T12, T14, pB_in_gaa(T12, X26, T14))
pB_in_gaa(T12, T15, T14) → U12_gaa(T12, T15, T14, halfD_in_ga(T12, T15))
halfD_in_ga(T18, s(X35)) → U3_ga(T18, X35, halfC_in_ga(T18, X35))
halfC_in_ga(0, 0) → halfC_out_ga(0, 0)
halfC_in_ga(s(0), 0) → halfC_out_ga(s(0), 0)
halfC_in_ga(s(s(T21)), s(X44)) → U2_ga(T21, X44, halfC_in_ga(T21, X44))
U2_ga(T21, X44, halfC_out_ga(T21, X44)) → halfC_out_ga(s(s(T21)), s(X44))
U3_ga(T18, X35, halfC_out_ga(T18, X35)) → halfD_out_ga(T18, s(X35))
U12_gaa(T12, T15, T14, halfD_out_ga(T12, T15)) → U13_gaa(T12, T15, T14, log2E_in_ga(T15, T14))
log2E_in_ga(0, s(0)) → log2E_out_ga(0, s(0))
log2E_in_ga(s(0), s(0)) → log2E_out_ga(s(0), s(0))
log2E_in_ga(s(s(T26)), T28) → U4_ga(T26, T28, pF_in_gaa(T26, X67, T28))
pF_in_gaa(T26, T29, T28) → U14_gaa(T26, T29, T28, halfD_in_ga(T26, T29))
U14_gaa(T26, T29, T28, halfD_out_ga(T26, T29)) → U15_gaa(T26, T29, T28, log2G_in_ga(T29, T28))
log2G_in_ga(0, s(s(0))) → log2G_out_ga(0, s(s(0)))
log2G_in_ga(s(0), s(s(0))) → log2G_out_ga(s(0), s(s(0)))
log2G_in_ga(s(s(T34)), T36) → U5_ga(T34, T36, pH_in_gaa(T34, X90, T36))
pH_in_gaa(T34, T37, T36) → U16_gaa(T34, T37, T36, halfD_in_ga(T34, T37))
U16_gaa(T34, T37, T36, halfD_out_ga(T34, T37)) → U17_gaa(T34, T37, T36, log2I_in_ga(T37, T36))
log2I_in_ga(0, s(s(s(0)))) → log2I_out_ga(0, s(s(s(0))))
log2I_in_ga(s(0), s(s(s(0)))) → log2I_out_ga(s(0), s(s(s(0))))
log2I_in_ga(s(s(T42)), T44) → U6_ga(T42, T44, pJ_in_gaa(T42, X113, T44))
pJ_in_gaa(T42, T45, T44) → U18_gaa(T42, T45, T44, halfD_in_ga(T42, T45))
U18_gaa(T42, T45, T44, halfD_out_ga(T42, T45)) → U19_gaa(T42, T45, T44, log2K_in_ga(T45, T44))
log2K_in_ga(0, s(s(s(s(0))))) → log2K_out_ga(0, s(s(s(s(0)))))
log2K_in_ga(s(0), s(s(s(s(0))))) → log2K_out_ga(s(0), s(s(s(s(0)))))
log2K_in_ga(s(s(T50)), T52) → U7_ga(T50, T52, pL_in_gaa(T50, X136, T52))
pL_in_gaa(T50, T53, T52) → U20_gaa(T50, T53, T52, halfD_in_ga(T50, T53))
U20_gaa(T50, T53, T52, halfD_out_ga(T50, T53)) → U21_gaa(T50, T53, T52, log2M_in_ga(T53, T52))
log2M_in_ga(0, s(s(s(s(s(0)))))) → log2M_out_ga(0, s(s(s(s(s(0))))))
log2M_in_ga(s(0), s(s(s(s(s(0)))))) → log2M_out_ga(s(0), s(s(s(s(s(0))))))
log2M_in_ga(s(s(T58)), T60) → U8_ga(T58, T60, pN_in_gaa(T58, X159, T60))
pN_in_gaa(T58, T61, T60) → U22_gaa(T58, T61, T60, halfD_in_ga(T58, T61))
U22_gaa(T58, T61, T60, halfD_out_ga(T58, T61)) → U23_gaa(T58, T61, T60, log2O_in_ga(T61, T60))
log2O_in_ga(0, s(s(s(s(s(s(0))))))) → log2O_out_ga(0, s(s(s(s(s(s(0)))))))
log2O_in_ga(s(0), s(s(s(s(s(s(0))))))) → log2O_out_ga(s(0), s(s(s(s(s(s(0)))))))
log2O_in_ga(s(s(T66)), T68) → U9_ga(T66, T68, pP_in_gaa(T66, X182, T68))
pP_in_gaa(T66, T69, T68) → U24_gaa(T66, T69, T68, halfD_in_ga(T66, T69))
U24_gaa(T66, T69, T68, halfD_out_ga(T66, T69)) → U25_gaa(T66, T69, T68, log2Q_in_ga(T69, T68))
log2Q_in_ga(0, s(s(s(s(s(s(s(0)))))))) → log2Q_out_ga(0, s(s(s(s(s(s(s(0))))))))
log2Q_in_ga(s(0), s(s(s(s(s(s(s(0)))))))) → log2Q_out_ga(s(0), s(s(s(s(s(s(s(0))))))))
log2Q_in_ga(s(s(T74)), T76) → U10_ga(T74, T76, pR_in_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76))
pR_in_gaga(T74, T78, T77, T76) → U26_gaga(T74, T78, T77, T76, halfD_in_ga(T74, T78))
U26_gaga(T74, T78, T77, T76, halfD_out_ga(T74, T78)) → U27_gaga(T74, T78, T77, T76, log2S_in_gga(T78, T77, T76))
log2S_in_gga(0, T85, s(T85)) → log2S_out_gga(0, T85, s(T85))
log2S_in_gga(s(0), T90, s(T90)) → log2S_out_gga(s(0), T90, s(T90))
log2S_in_gga(s(s(T97)), T98, T100) → U11_gga(T97, T98, T100, pR_in_gaga(T97, X228, s(T98), T100))
U11_gga(T97, T98, T100, pR_out_gaga(T97, X228, s(T98), T100)) → log2S_out_gga(s(s(T97)), T98, T100)
U27_gaga(T74, T78, T77, T76, log2S_out_gga(T78, T77, T76)) → pR_out_gaga(T74, T78, T77, T76)
U10_ga(T74, T76, pR_out_gaga(T74, X205, s(s(s(s(s(s(s(0))))))), T76)) → log2Q_out_ga(s(s(T74)), T76)
U25_gaa(T66, T69, T68, log2Q_out_ga(T69, T68)) → pP_out_gaa(T66, T69, T68)
U9_ga(T66, T68, pP_out_gaa(T66, X182, T68)) → log2O_out_ga(s(s(T66)), T68)
U23_gaa(T58, T61, T60, log2O_out_ga(T61, T60)) → pN_out_gaa(T58, T61, T60)
U8_ga(T58, T60, pN_out_gaa(T58, X159, T60)) → log2M_out_ga(s(s(T58)), T60)
U21_gaa(T50, T53, T52, log2M_out_ga(T53, T52)) → pL_out_gaa(T50, T53, T52)
U7_ga(T50, T52, pL_out_gaa(T50, X136, T52)) → log2K_out_ga(s(s(T50)), T52)
U19_gaa(T42, T45, T44, log2K_out_ga(T45, T44)) → pJ_out_gaa(T42, T45, T44)
U6_ga(T42, T44, pJ_out_gaa(T42, X113, T44)) → log2I_out_ga(s(s(T42)), T44)
U17_gaa(T34, T37, T36, log2I_out_ga(T37, T36)) → pH_out_gaa(T34, T37, T36)
U5_ga(T34, T36, pH_out_gaa(T34, X90, T36)) → log2G_out_ga(s(s(T34)), T36)
U15_gaa(T26, T29, T28, log2G_out_ga(T29, T28)) → pF_out_gaa(T26, T29, T28)
U4_ga(T26, T28, pF_out_gaa(T26, X67, T28)) → log2E_out_ga(s(s(T26)), T28)
U13_gaa(T12, T15, T14, log2E_out_ga(T15, T14)) → pB_out_gaa(T12, T15, T14)
U1_ga(T12, T14, pB_out_gaa(T12, X26, T14)) → log2A_out_ga(s(s(T12)), T14)

The argument filtering Pi contains the following mapping:
log2A_in_ga(x1, x2)  =  log2A_in_ga(x1)
0  =  0
log2A_out_ga(x1, x2)  =  log2A_out_ga(x1, x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
pB_in_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U12_gaa(x1, x2, x3, x4)  =  U12_gaa(x1, x4)
halfD_in_ga(x1, x2)  =  halfD_in_ga(x1)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
halfC_in_ga(x1, x2)  =  halfC_in_ga(x1)
halfC_out_ga(x1, x2)  =  halfC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
halfD_out_ga(x1, x2)  =  halfD_out_ga(x1, x2)
U13_gaa(x1, x2, x3, x4)  =  U13_gaa(x1, x2, x4)
log2E_in_ga(x1, x2)  =  log2E_in_ga(x1)
log2E_out_ga(x1, x2)  =  log2E_out_ga(x1, x2)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
pF_in_gaa(x1, x2, x3)  =  pF_in_gaa(x1)
U14_gaa(x1, x2, x3, x4)  =  U14_gaa(x1, x4)
U15_gaa(x1, x2, x3, x4)  =  U15_gaa(x1, x2, x4)
log2G_in_ga(x1, x2)  =  log2G_in_ga(x1)
log2G_out_ga(x1, x2)  =  log2G_out_ga(x1, x2)
U5_ga(x1, x2, x3)  =  U5_ga(x1, x3)
pH_in_gaa(x1, x2, x3)  =  pH_in_gaa(x1)
U16_gaa(x1, x2, x3, x4)  =  U16_gaa(x1, x4)
U17_gaa(x1, x2, x3, x4)  =  U17_gaa(x1, x2, x4)
log2I_in_ga(x1, x2)  =  log2I_in_ga(x1)
log2I_out_ga(x1, x2)  =  log2I_out_ga(x1, x2)
U6_ga(x1, x2, x3)  =  U6_ga(x1, x3)
pJ_in_gaa(x1, x2, x3)  =  pJ_in_gaa(x1)
U18_gaa(x1, x2, x3, x4)  =  U18_gaa(x1, x4)
U19_gaa(x1, x2, x3, x4)  =  U19_gaa(x1, x2, x4)
log2K_in_ga(x1, x2)  =  log2K_in_ga(x1)
log2K_out_ga(x1, x2)  =  log2K_out_ga(x1, x2)
U7_ga(x1, x2, x3)  =  U7_ga(x1, x3)
pL_in_gaa(x1, x2, x3)  =  pL_in_gaa(x1)
U20_gaa(x1, x2, x3, x4)  =  U20_gaa(x1, x4)
U21_gaa(x1, x2, x3, x4)  =  U21_gaa(x1, x2, x4)
log2M_in_ga(x1, x2)  =  log2M_in_ga(x1)
log2M_out_ga(x1, x2)  =  log2M_out_ga(x1, x2)
U8_ga(x1, x2, x3)  =  U8_ga(x1, x3)
pN_in_gaa(x1, x2, x3)  =  pN_in_gaa(x1)
U22_gaa(x1, x2, x3, x4)  =  U22_gaa(x1, x4)
U23_gaa(x1, x2, x3, x4)  =  U23_gaa(x1, x2, x4)
log2O_in_ga(x1, x2)  =  log2O_in_ga(x1)
log2O_out_ga(x1, x2)  =  log2O_out_ga(x1, x2)
U9_ga(x1, x2, x3)  =  U9_ga(x1, x3)
pP_in_gaa(x1, x2, x3)  =  pP_in_gaa(x1)
U24_gaa(x1, x2, x3, x4)  =  U24_gaa(x1, x4)
U25_gaa(x1, x2, x3, x4)  =  U25_gaa(x1, x2, x4)
log2Q_in_ga(x1, x2)  =  log2Q_in_ga(x1)
log2Q_out_ga(x1, x2)  =  log2Q_out_ga(x1, x2)
U10_ga(x1, x2, x3)  =  U10_ga(x1, x3)
pR_in_gaga(x1, x2, x3, x4)  =  pR_in_gaga(x1, x3)
U26_gaga(x1, x2, x3, x4, x5)  =  U26_gaga(x1, x3, x5)
U27_gaga(x1, x2, x3, x4, x5)  =  U27_gaga(x1, x2, x3, x5)
log2S_in_gga(x1, x2, x3)  =  log2S_in_gga(x1, x2)
log2S_out_gga(x1, x2, x3)  =  log2S_out_gga(x1, x2, x3)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x2, x4)
pR_out_gaga(x1, x2, x3, x4)  =  pR_out_gaga(x1, x2, x3, x4)
pP_out_gaa(x1, x2, x3)  =  pP_out_gaa(x1, x2, x3)
pN_out_gaa(x1, x2, x3)  =  pN_out_gaa(x1, x2, x3)
pL_out_gaa(x1, x2, x3)  =  pL_out_gaa(x1, x2, x3)
pJ_out_gaa(x1, x2, x3)  =  pJ_out_gaa(x1, x2, x3)
pH_out_gaa(x1, x2, x3)  =  pH_out_gaa(x1, x2, x3)
pF_out_gaa(x1, x2, x3)  =  pF_out_gaa(x1, x2, x3)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2, x3)
PR_IN_GAGA(x1, x2, x3, x4)  =  PR_IN_GAGA(x1, x3)
U26_GAGA(x1, x2, x3, x4, x5)  =  U26_GAGA(x1, x3, x5)
LOG2S_IN_GGA(x1, x2, x3)  =  LOG2S_IN_GGA(x1, x2)

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

PR_IN_GAGA(T74, T78, T77, T76) → U26_GAGA(T74, T78, T77, T76, halfD_in_ga(T74, T78))
U26_GAGA(T74, T78, T77, T76, halfD_out_ga(T74, T78)) → LOG2S_IN_GGA(T78, T77, T76)
LOG2S_IN_GGA(s(s(T97)), T98, T100) → PR_IN_GAGA(T97, X228, s(T98), T100)

The TRS R consists of the following rules:

halfD_in_ga(T18, s(X35)) → U3_ga(T18, X35, halfC_in_ga(T18, X35))
U3_ga(T18, X35, halfC_out_ga(T18, X35)) → halfD_out_ga(T18, s(X35))
halfC_in_ga(0, 0) → halfC_out_ga(0, 0)
halfC_in_ga(s(0), 0) → halfC_out_ga(s(0), 0)
halfC_in_ga(s(s(T21)), s(X44)) → U2_ga(T21, X44, halfC_in_ga(T21, X44))
U2_ga(T21, X44, halfC_out_ga(T21, X44)) → halfC_out_ga(s(s(T21)), s(X44))

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
halfD_in_ga(x1, x2)  =  halfD_in_ga(x1)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
halfC_in_ga(x1, x2)  =  halfC_in_ga(x1)
halfC_out_ga(x1, x2)  =  halfC_out_ga(x1, x2)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
halfD_out_ga(x1, x2)  =  halfD_out_ga(x1, x2)
PR_IN_GAGA(x1, x2, x3, x4)  =  PR_IN_GAGA(x1, x3)
U26_GAGA(x1, x2, x3, x4, x5)  =  U26_GAGA(x1, x3, x5)
LOG2S_IN_GGA(x1, x2, x3)  =  LOG2S_IN_GGA(x1, x2)

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

PR_IN_GAGA(T74, T77) → U26_GAGA(T74, T77, halfD_in_ga(T74))
U26_GAGA(T74, T77, halfD_out_ga(T74, T78)) → LOG2S_IN_GGA(T78, T77)
LOG2S_IN_GGA(s(s(T97)), T98) → PR_IN_GAGA(T97, s(T98))

The TRS R consists of the following rules:

halfD_in_ga(T18) → U3_ga(T18, halfC_in_ga(T18))
U3_ga(T18, halfC_out_ga(T18, X35)) → halfD_out_ga(T18, s(X35))
halfC_in_ga(0) → halfC_out_ga(0, 0)
halfC_in_ga(s(0)) → halfC_out_ga(s(0), 0)
halfC_in_ga(s(s(T21))) → U2_ga(T21, halfC_in_ga(T21))
U2_ga(T21, halfC_out_ga(T21, X44)) → halfC_out_ga(s(s(T21)), s(X44))

The set Q consists of the following terms:

halfD_in_ga(x0)
U3_ga(x0, x1)
halfC_in_ga(x0)
U2_ga(x0, x1)

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

(19) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule PR_IN_GAGA(T74, T77) → U26_GAGA(T74, T77, halfD_in_ga(T74)) at position [2] we obtained the following new rules [LPAR04]:

PR_IN_GAGA(T74, T77) → U26_GAGA(T74, T77, U3_ga(T74, halfC_in_ga(T74)))

(20) Obligation:

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

U26_GAGA(T74, T77, halfD_out_ga(T74, T78)) → LOG2S_IN_GGA(T78, T77)
LOG2S_IN_GGA(s(s(T97)), T98) → PR_IN_GAGA(T97, s(T98))
PR_IN_GAGA(T74, T77) → U26_GAGA(T74, T77, U3_ga(T74, halfC_in_ga(T74)))

The TRS R consists of the following rules:

halfD_in_ga(T18) → U3_ga(T18, halfC_in_ga(T18))
U3_ga(T18, halfC_out_ga(T18, X35)) → halfD_out_ga(T18, s(X35))
halfC_in_ga(0) → halfC_out_ga(0, 0)
halfC_in_ga(s(0)) → halfC_out_ga(s(0), 0)
halfC_in_ga(s(s(T21))) → U2_ga(T21, halfC_in_ga(T21))
U2_ga(T21, halfC_out_ga(T21, X44)) → halfC_out_ga(s(s(T21)), s(X44))

The set Q consists of the following terms:

halfD_in_ga(x0)
U3_ga(x0, x1)
halfC_in_ga(x0)
U2_ga(x0, x1)

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

(21) UsableRulesProof (EQUIVALENT transformation)

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

(22) Obligation:

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

U26_GAGA(T74, T77, halfD_out_ga(T74, T78)) → LOG2S_IN_GGA(T78, T77)
LOG2S_IN_GGA(s(s(T97)), T98) → PR_IN_GAGA(T97, s(T98))
PR_IN_GAGA(T74, T77) → U26_GAGA(T74, T77, U3_ga(T74, halfC_in_ga(T74)))

The TRS R consists of the following rules:

halfC_in_ga(0) → halfC_out_ga(0, 0)
halfC_in_ga(s(0)) → halfC_out_ga(s(0), 0)
halfC_in_ga(s(s(T21))) → U2_ga(T21, halfC_in_ga(T21))
U3_ga(T18, halfC_out_ga(T18, X35)) → halfD_out_ga(T18, s(X35))
U2_ga(T21, halfC_out_ga(T21, X44)) → halfC_out_ga(s(s(T21)), s(X44))

The set Q consists of the following terms:

halfD_in_ga(x0)
U3_ga(x0, x1)
halfC_in_ga(x0)
U2_ga(x0, x1)

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

(23) QReductionProof (EQUIVALENT transformation)

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

halfD_in_ga(x0)

(24) Obligation:

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

U26_GAGA(T74, T77, halfD_out_ga(T74, T78)) → LOG2S_IN_GGA(T78, T77)
LOG2S_IN_GGA(s(s(T97)), T98) → PR_IN_GAGA(T97, s(T98))
PR_IN_GAGA(T74, T77) → U26_GAGA(T74, T77, U3_ga(T74, halfC_in_ga(T74)))

The TRS R consists of the following rules:

halfC_in_ga(0) → halfC_out_ga(0, 0)
halfC_in_ga(s(0)) → halfC_out_ga(s(0), 0)
halfC_in_ga(s(s(T21))) → U2_ga(T21, halfC_in_ga(T21))
U3_ga(T18, halfC_out_ga(T18, X35)) → halfD_out_ga(T18, s(X35))
U2_ga(T21, halfC_out_ga(T21, X44)) → halfC_out_ga(s(s(T21)), s(X44))

The set Q consists of the following terms:

U3_ga(x0, x1)
halfC_in_ga(x0)
U2_ga(x0, x1)

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

(25) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

LOG2S_IN_GGA(s(s(T97)), T98) → PR_IN_GAGA(T97, s(T98))

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

POL(0) = 1   
POL(LOG2S_IN_GGA(x₁, x₂)) = x₁   
POL(PR_IN_GAGA(x₁, x₂)) = 1 + x₁   
POL(U26_GAGA(x₁, x₂, x₃)) = x₃   
POL(U2_ga(x₁, x₂)) = 1 + x₂   
POL(U3_ga(x₁, x₂)) = x₂   
POL(halfC_in_ga(x₁)) = 1 + x₁   
POL(halfC_out_ga(x₁, x₂)) = 1 + x₂   
POL(halfD_out_ga(x₁, x₂)) = x₂   
POL(s(x₁)) = 1 + x₁   

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

halfC_in_ga(0) → halfC_out_ga(0, 0)
halfC_in_ga(s(0)) → halfC_out_ga(s(0), 0)
halfC_in_ga(s(s(T21))) → U2_ga(T21, halfC_in_ga(T21))
U3_ga(T18, halfC_out_ga(T18, X35)) → halfD_out_ga(T18, s(X35))
U2_ga(T21, halfC_out_ga(T21, X44)) → halfC_out_ga(s(s(T21)), s(X44))

(26) Obligation:

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

U26_GAGA(T74, T77, halfD_out_ga(T74, T78)) → LOG2S_IN_GGA(T78, T77)
PR_IN_GAGA(T74, T77) → U26_GAGA(T74, T77, U3_ga(T74, halfC_in_ga(T74)))

The TRS R consists of the following rules:

halfC_in_ga(0) → halfC_out_ga(0, 0)
halfC_in_ga(s(0)) → halfC_out_ga(s(0), 0)
halfC_in_ga(s(s(T21))) → U2_ga(T21, halfC_in_ga(T21))
U3_ga(T18, halfC_out_ga(T18, X35)) → halfD_out_ga(T18, s(X35))
U2_ga(T21, halfC_out_ga(T21, X44)) → halfC_out_ga(s(s(T21)), s(X44))

The set Q consists of the following terms:

U3_ga(x0, x1)
halfC_in_ga(x0)
U2_ga(x0, x1)

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

(27) DependencyGraphProof (EQUIVALENT transformation)

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

(28) TRUE