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

(0) Obligation:

Clauses:

in(X, tree(X, X1, X2)).
in(X, tree(Y, Left, X3)) :- ','(less(X, Y), in(X, Left)).
in(X, tree(Y, X4, Right)) :- ','(less(Y, X), in(X, Right)).
less(0, s(X5)).
less(s(X), s(Y)) :- less(X, Y).

Query: in(a,g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: in(T1, T2)\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: in(T1, T2), SCOPE: 1, CLAUSE: 0 | in(T1, T2), SCOPE: 1, CLAUSE: 1 | in(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: true | in(T1, tree(T6, T7, T8)), SCOPE: 1, CLAUSE: 1 | in(T1, tree(T6, T7, T8)), SCOPE: 1, CLAUSE: 2\n\nT6 is ground\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: in(T1, T2), SCOPE: 1, CLAUSE: 1 | in(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT2 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, T2) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: in(T1, tree(T6, T7, T8)), SCOPE: 1, CLAUSE: 1 | in(T1, tree(T6, T7, T8)), SCOPE: 1, CLAUSE: 2\n\nT6 is ground\nT7 is ground\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: ','(less(T17, T14), in(T17, T15)) | in(T1, tree(T14, T15, T16)), SCOPE: 1, CLAUSE: 2\n\nT14 is ground\nT15 is ground\nT16 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(less(T17, T14), in(T17, T15)), SCOPE: 2, CLAUSE: 3 | ','(less(T17, T14), in(T17, T15)), SCOPE: 2, CLAUSE: 4 | ?_2 | in(T1, tree(T14, T15, T16)), SCOPE: 1, CLAUSE: 2\n\nT14 is ground\nT15 is ground\nT16 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(less(T17, T14), in(T17, T15)), SCOPE: 2, CLAUSE: 3\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(less(T17, T14), in(T17, T15)), SCOPE: 2, CLAUSE: 4 | ?_2 | in(T1, tree(T14, T15, T16)), SCOPE: 1, CLAUSE: 2\n\nT14 is ground\nT15 is ground\nT16 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="B: in(0, T15)\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: in(0, T15), SCOPE: 3, CLAUSE: 0 | in(0, T15), SCOPE: 3, CLAUSE: 1 | in(0, T15), SCOPE: 3, CLAUSE: 2\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: in(0, T15), SCOPE: 3, CLAUSE: 0\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: in(0, T15), SCOPE: 3, CLAUSE: 1 | in(0, T15), SCOPE: 3, CLAUSE: 2\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: in(0, T15), SCOPE: 3, CLAUSE: 1\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: in(0, T15), SCOPE: 3, CLAUSE: 2\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="F: ','(less(0, T49), in(0, T50))\n\nT49 is ground\nT50 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="N: less(0, T49)\n\nT49 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: in(0, T50)\n\nT50 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: less(0, T49), SCOPE: 4, CLAUSE: 3 | less(0, T49), SCOPE: 4, CLAUSE: 4\n\nT49 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: less(0, T49), SCOPE: 4, CLAUSE: 3\n\nT49 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: less(0, T49), SCOPE: 4, CLAUSE: 4\n\nT49 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="G: ','(less(T71, 0), in(0, T73))\n\nT71 is ground\nT73 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="P: less(T71, 0)\n\nT71 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: in(0, T73)\n\nT73 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: less(T71, 0), SCOPE: 5, CLAUSE: 3 | less(T71, 0), SCOPE: 5, CLAUSE: 4\n\nT71 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: less(T71, 0), SCOPE: 5, CLAUSE: 4\n\nT71 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: ','(less(T17, T14), in(T17, T15)), SCOPE: 2, CLAUSE: 4\n\nT14 is ground\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: ?_2 | in(T1, tree(T14, T15, T16)), SCOPE: 1, CLAUSE: 2\n\nT14 is ground\nT15 is ground\nT16 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="C: ','(less(T89, T88), in(s(T89), T15))\n\nT15 is ground\nT88 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="H: less(T89, T88)\n\nT88 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="I: in(s(T92), T15)\n\nT15 is ground\nT92 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: less(T89, T88), SCOPE: 6, CLAUSE: 3 | less(T89, T88), SCOPE: 6, CLAUSE: 4\n\nT88 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: less(T89, T88), SCOPE: 6, CLAUSE: 3\n\nT88 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: less(T89, T88), SCOPE: 6, CLAUSE: 4\n\nT88 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: less(T106, T105)\n\nT105 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: in(s(T92), T15), SCOPE: 7, CLAUSE: 0 | in(s(T92), T15), SCOPE: 7, CLAUSE: 1 | in(s(T92), T15), SCOPE: 7, CLAUSE: 2\n\nT15 is ground\nT92 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: in(s(T92), T15), SCOPE: 7, CLAUSE: 0\n\nT15 is ground\nT92 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: in(s(T92), T15), SCOPE: 7, CLAUSE: 1 | in(s(T92), T15), SCOPE: 7, CLAUSE: 2\n\nT15 is ground\nT92 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: in(s(T92), T15), SCOPE: 7, CLAUSE: 1\n\nT15 is ground\nT92 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: in(s(T92), T15), SCOPE: 7, CLAUSE: 2\n\nT15 is ground\nT92 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="J: ','(less(s(T146), T147), in(s(T146), T148))\n\nT146 is ground\nT147 is ground\nT148 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="O: less(s(T146), T147)\n\nT146 is ground\nT147 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: in(s(T146), T148)\n\nT146 is ground\nT148 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: less(s(T146), T147), SCOPE: 8, CLAUSE: 3 | less(s(T146), T147), SCOPE: 8, CLAUSE: 4\n\nT146 is ground\nT147 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: less(s(T146), T147), SCOPE: 8, CLAUSE: 4\n\nT146 is ground\nT147 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="L: less(T154, T155)\n\nT154 is ground\nT155 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: less(T154, T155), SCOPE: 9, CLAUSE: 3 | less(T154, T155), SCOPE: 9, CLAUSE: 4\n\nT154 is ground\nT155 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: less(T154, T155), SCOPE: 9, CLAUSE: 3\n\nT154 is ground\nT155 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: less(T154, T155), SCOPE: 9, CLAUSE: 4\n\nT154 is ground\nT155 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="203: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: less(T167, T168)\n\nT167 is ground\nT168 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="K: ','(less(T186, s(T185)), in(s(T185), T188))\n\nT185 is ground\nT186 is ground\nT188 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: less(T186, s(T185))\n\nT185 is ground\nT186 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="211: in(s(T185), T188)\n\nT185 is ground\nT188 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: in(T1, tree(T14, T15, T16)), SCOPE: 1, CLAUSE: 2\n\nT14 is ground\nT15 is ground\nT16 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="D: ','(less(T211, T214), in(T214, T213))\n\nT211 is ground\nT213 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="M: less(T211, T214)\n\nT211 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: in(T217, T213)\n\nT213 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
220 [label="220: less(T211, T214), SCOPE: 10, CLAUSE: 3 | less(T211, T214), SCOPE: 10, CLAUSE: 4\n\nT211 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="221: less(T211, T214), SCOPE: 10, CLAUSE: 3\n\nT211 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
222 [label="222: less(T211, T214), SCOPE: 10, CLAUSE: 4\n\nT211 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
224 [label="224: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
225 [label="225: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: less(T229, T231)\n\nT229 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="227: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
229 [label="229: ','(less(T248, T245), in(T248, T246)) | in(T1, tree(T245, T246, T247)), SCOPE: 1, CLAUSE: 2\n\nT245 is ground\nT246 is ground\nT247 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(T245, T246, T247)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
230 [label="230: in(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT2 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, T2) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="231: ','(less(T248, T245), in(T248, T246)), SCOPE: 11, CLAUSE: 3 | ','(less(T248, T245), in(T248, T246)), SCOPE: 11, CLAUSE: 4 | ?_11 | in(T1, tree(T245, T246, T247)), SCOPE: 1, CLAUSE: 2\n\nT245 is ground\nT246 is ground\nT247 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(T245, T246, T247)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: ','(less(T248, T245), in(T248, T246)), SCOPE: 11, CLAUSE: 3\n\nT245 is ground\nT246 is ground\nT247 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(T245, T246, T247)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
233 [label="233: ','(less(T248, T245), in(T248, T246)), SCOPE: 11, CLAUSE: 4 | ?_11 | in(T1, tree(T245, T246, T247)), SCOPE: 1, CLAUSE: 2\n\nT245 is ground\nT246 is ground\nT247 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(T245, T246, T247)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
234 [label="234: in(0, T246)\n\nT246 is ground\nT247 is ground\nT253 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(s(T253), T246, T247)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
237 [label="237: ','(less(T248, T245), in(T248, T246)), SCOPE: 11, CLAUSE: 4\n\nT245 is ground\nT246 is ground\nT247 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(T245, T246, T247)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
238 [label="238: ?_11 | in(T1, tree(T245, T246, T247)), SCOPE: 1, CLAUSE: 2\n\nT245 is ground\nT246 is ground\nT247 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(T245, T246, T247)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
239 [label="239: ','(less(T268, T267), in(s(T268), T246))\n\nT246 is ground\nT247 is ground\nT267 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(s(T267), T246, T247)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
240 [label="240: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
241 [label="241: in(T1, tree(T245, T246, T247)), SCOPE: 1, CLAUSE: 2\n\nT245 is ground\nT246 is ground\nT247 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(T245, T246, T247)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
244 [label="244: ','(less(T283, T286), in(T286, T285))\n\nT283 is ground\nT284 is ground\nT285 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(T283, T284, T285)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
253 [label="253: ','(less(T294, T297), in(T297, T296))\n\nT294 is ground\nT295 is ground\nT296 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(T294, T295, T296)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
254 [label="254: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
255 [label="255: ','(less(T294, T297), in(T297, T296)), SCOPE: 12, CLAUSE: 3 | ','(less(T294, T297), in(T297, T296)), SCOPE: 12, CLAUSE: 4\n\nT294 is ground\nT295 is ground\nT296 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(T294, T295, T296)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
256 [label="256: ','(less(T294, T297), in(T297, T296)), SCOPE: 12, CLAUSE: 3\n\nT294 is ground\nT295 is ground\nT296 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(T294, T295, T296)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
257 [label="257: ','(less(T294, T297), in(T297, T296)), SCOPE: 12, CLAUSE: 4\n\nT294 is ground\nT295 is ground\nT296 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(T294, T295, T296)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
258 [label="258: in(s(T303), T296)\n\nT295 is ground\nT296 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(0, T295, T296)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
259 [label="259: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
260 [label="E: ','(less(T314, T316), in(s(T316), T296))\n\nT295 is ground\nT296 is ground\nT314 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(s(T314), T295, T296)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
261 [label="261: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
262 [label="262: less(T314, T316)\n\nT295 is ground\nT296 is ground\nT314 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T1, tree(s(T314), T295, T296)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
263 [label="263: in(s(T319), T296)\n\nT295 is ground\nT296 is ground\nT314 is ground\nX9 is free\nX10 is free\nX11 is free\nin(T320, tree(s(T314), T295, T296)) !=? in(X9, tree(X9, X10, X11))", fontsize=16, style=filled, fillcolor=lightyellow];
264 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 264 [arrowhead = none ];
264 -> 6;

265 [label="EVAL with clause\nin(X9, tree(X9, X10, X11)).\nand substitutionT1 -> T6,\nX9 -> T6,\nX10 -> T7,\nX11 -> T8,\nT2 -> tree(T6, T7, T8)", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 265 [arrowhead = none ];
265 -> 9;

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

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

268 [label="EVAL with clause\nin(X271, tree(X272, X273, X274)) :- ','(less(X271, X272), in(X271, X273)).\nand substitutionT1 -> T248,\nX271 -> T248,\nX272 -> T245,\nX273 -> T246,\nX274 -> T247,\nT2 -> tree(T245, T246, T247),\nT244 -> T248", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 268 [arrowhead = none ];
268 -> 229;

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

270 [label="ONLY EVAL with clause\nin(X16, tree(X17, X18, X19)) :- ','(less(X16, X17), in(X16, X18)).\nand substitutionT1 -> T17,\nX16 -> T17,\nT6 -> T14,\nX17 -> T14,\nT7 -> T15,\nX18 -> T15,\nT8 -> T16,\nX19 -> T16,\nT13 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 270 [arrowhead = none ];
270 -> 21;

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

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

273 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
23 -> 273 [arrowhead = none ];
273 -> 27;

274 [label="EVAL with clause\nless(0, s(X24)).\nand substitutionT17 -> 0,\nX24 -> T22,\nT14 -> s(T22)", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 274 [arrowhead = none ];
274 -> 31;

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

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

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

278 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
31 -> 278 [arrowhead = none ];
278 -> 34;

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

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

281 [label="EVAL with clause\nin(X43, tree(X43, X44, X45)).\nand substitutionX43 -> 0,\nX44 -> T35,\nX45 -> T36,\nT15 -> tree(0, T35, T36)", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 281 [arrowhead = none ];
281 -> 45;

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

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

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

285 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
45 -> 285 [arrowhead = none ];
285 -> 47;

286 [label="EVAL with clause\nin(X62, tree(X63, X64, X65)) :- ','(less(X62, X63), in(X62, X64)).\nand substitutionX62 -> 0,\nX63 -> T49,\nX64 -> T50,\nX65 -> T51,\nT15 -> tree(T49, T50, T51)", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 286 [arrowhead = none ];
286 -> 55;

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

288 [label="EVAL with clause\nin(X91, tree(X92, X93, X94)) :- ','(less(X92, X91), in(X91, X94)).\nand substitutionX91 -> 0,\nX92 -> T71,\nX93 -> T72,\nX94 -> T73,\nT15 -> tree(T71, T72, T73)", fontsize=14, style = filled, fillcolor = lightblue];
52 -> 288 [arrowhead = none ];
288 -> 94;

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

290 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
55 -> 290 [arrowhead = none ];
290 -> 58;

291 [label="SPLIT 2\nnew knowledge:\nT49 is ground", fontsize=14, style = filled, fillcolor = violet];
55 -> 291 [arrowhead = none ];
291 -> 61;

292 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
58 -> 292 [arrowhead = none ];
292 -> 64;

293 [label="INSTANCE with matching:\nT15 -> T50", fontsize=14, style = filled, fillcolor = lightgrey];
61 -> 293 [arrowhead = none , style=dashed];
293 -> 31[style=dashed];

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

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

296 [label="EVAL with clause\nless(0, s(X74)).\nand substitutionX74 -> T60,\nT49 -> s(T60)", fontsize=14, style = filled, fillcolor = lightblue];
69 -> 296 [arrowhead = none ];
296 -> 81;

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

298 [label="BACKTRACK\nfor clause: less(s(X), s(Y)) :- less(X, Y)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
70 -> 298 [arrowhead = none ];
298 -> 84;

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

300 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
94 -> 300 [arrowhead = none ];
300 -> 118;

301 [label="SPLIT 2\nnew knowledge:\nT71 is ground", fontsize=14, style = filled, fillcolor = violet];
94 -> 301 [arrowhead = none ];
301 -> 119;

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

303 [label="INSTANCE with matching:\nT15 -> T73", fontsize=14, style = filled, fillcolor = lightgrey];
119 -> 303 [arrowhead = none , style=dashed];
303 -> 31[style=dashed];

304 [label="BACKTRACK\nfor clause: less(0, s(X5))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
122 -> 304 [arrowhead = none ];
304 -> 123;

305 [label="BACKTRACK\nfor clause: less(s(X), s(Y)) :- less(X, Y)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
123 -> 305 [arrowhead = none ];
305 -> 125;

306 [label="EVAL with clause\nless(s(X116), s(X117)) :- less(X116, X117).\nand substitutionX116 -> T89,\nT17 -> s(T89),\nX117 -> T88,\nT14 -> s(T88),\nT87 -> T89", fontsize=14, style = filled, fillcolor = lightblue];
128 -> 306 [arrowhead = none ];
306 -> 132;

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

308 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
129 -> 308 [arrowhead = none ];
308 -> 212;

309 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
132 -> 309 [arrowhead = none ];
309 -> 136;

310 [label="SPLIT 2\nnew knowledge:\nT92 is ground\nT88 is ground\nreplacements:T89 -> T92", fontsize=14, style = filled, fillcolor = violet];
132 -> 310 [arrowhead = none ];
310 -> 137;

311 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
136 -> 311 [arrowhead = none ];
311 -> 143;

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

313 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
143 -> 313 [arrowhead = none ];
313 -> 144;

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

315 [label="EVAL with clause\nless(0, s(X126)).\nand substitutionT89 -> 0,\nX126 -> T99,\nT88 -> s(T99)", fontsize=14, style = filled, fillcolor = lightblue];
144 -> 315 [arrowhead = none ];
315 -> 148;

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

317 [label="EVAL with clause\nless(s(X131), s(X132)) :- less(X131, X132).\nand substitutionX131 -> T106,\nT89 -> s(T106),\nX132 -> T105,\nT88 -> s(T105),\nT104 -> T106", fontsize=14, style = filled, fillcolor = lightblue];
145 -> 317 [arrowhead = none ];
317 -> 152;

318 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
145 -> 318 [arrowhead = none ];
318 -> 153;

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

320 [label="INSTANCE with matching:\nT89 -> T106\nT88 -> T105", fontsize=14, style = filled, fillcolor = lightgrey];
152 -> 320 [arrowhead = none , style=dashed];
320 -> 136[style=dashed];

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

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

323 [label="EVAL with clause\nin(X153, tree(X153, X154, X155)).\nand substitutionT92 -> T127,\nX153 -> s(T127),\nX154 -> T128,\nX155 -> T129,\nT15 -> tree(s(T127), T128, T129)", fontsize=14, style = filled, fillcolor = lightblue];
169 -> 323 [arrowhead = none ];
323 -> 171;

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

325 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
170 -> 325 [arrowhead = none ];
325 -> 174;

326 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
170 -> 326 [arrowhead = none ];
326 -> 175;

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

328 [label="EVAL with clause\nin(X172, tree(X173, X174, X175)) :- ','(less(X172, X173), in(X172, X174)).\nand substitutionT92 -> T146,\nX172 -> s(T146),\nX173 -> T147,\nX174 -> T148,\nX175 -> T149,\nT15 -> tree(T147, T148, T149)", fontsize=14, style = filled, fillcolor = lightblue];
174 -> 328 [arrowhead = none ];
328 -> 182;

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

330 [label="EVAL with clause\nin(X216, tree(X217, X218, X219)) :- ','(less(X217, X216), in(X216, X219)).\nand substitutionT92 -> T185,\nX216 -> s(T185),\nX217 -> T186,\nX218 -> T187,\nX219 -> T188,\nT15 -> tree(T186, T187, T188)", fontsize=14, style = filled, fillcolor = lightblue];
175 -> 330 [arrowhead = none ];
330 -> 208;

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

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

333 [label="SPLIT 2\nnew knowledge:\nT146 is ground\nT147 is ground", fontsize=14, style = filled, fillcolor = violet];
182 -> 333 [arrowhead = none ];
333 -> 193;

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

335 [label="INSTANCE with matching:\nT92 -> T146\nT15 -> T148", fontsize=14, style = filled, fillcolor = lightgrey];
193 -> 335 [arrowhead = none , style=dashed];
335 -> 137[style=dashed];

336 [label="BACKTRACK\nfor clause: less(0, s(X5))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
194 -> 336 [arrowhead = none ];
336 -> 195;

337 [label="EVAL with clause\nless(s(X185), s(X186)) :- less(X185, X186).\nand substitutionT146 -> T154,\nX185 -> T154,\nX186 -> T155,\nT147 -> s(T155)", fontsize=14, style = filled, fillcolor = lightblue];
195 -> 337 [arrowhead = none ];
337 -> 196;

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

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

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

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

342 [label="EVAL with clause\nless(0, s(X193)).\nand substitutionT154 -> 0,\nX193 -> T162,\nT155 -> s(T162)", fontsize=14, style = filled, fillcolor = lightblue];
201 -> 342 [arrowhead = none ];
342 -> 203;

343 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
201 -> 343 [arrowhead = none ];
343 -> 204;

344 [label="EVAL with clause\nless(s(X198), s(X199)) :- less(X198, X199).\nand substitutionX198 -> T167,\nT154 -> s(T167),\nX199 -> T168,\nT155 -> s(T168)", fontsize=14, style = filled, fillcolor = lightblue];
202 -> 344 [arrowhead = none ];
344 -> 206;

345 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
202 -> 345 [arrowhead = none ];
345 -> 207;

346 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
203 -> 346 [arrowhead = none ];
346 -> 205;

347 [label="INSTANCE with matching:\nT154 -> T167\nT155 -> T168", fontsize=14, style = filled, fillcolor = lightgrey];
206 -> 347 [arrowhead = none , style=dashed];
347 -> 196[style=dashed];

348 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
208 -> 348 [arrowhead = none ];
348 -> 210;

349 [label="SPLIT 2\nnew knowledge:\nT186 is ground\nT185 is ground", fontsize=14, style = filled, fillcolor = violet];
208 -> 349 [arrowhead = none ];
349 -> 211;

350 [label="INSTANCE with matching:\nT154 -> T186\nT155 -> s(T185)", fontsize=14, style = filled, fillcolor = lightgrey];
210 -> 350 [arrowhead = none , style=dashed];
350 -> 196[style=dashed];

351 [label="INSTANCE with matching:\nT92 -> T185\nT15 -> T188", fontsize=14, style = filled, fillcolor = lightgrey];
211 -> 351 [arrowhead = none , style=dashed];
351 -> 137[style=dashed];

352 [label="ONLY EVAL with clause\nin(X240, tree(X241, X242, X243)) :- ','(less(X241, X240), in(X240, X243)).\nand substitutionT1 -> T214,\nX240 -> T214,\nT14 -> T211,\nX241 -> T211,\nT15 -> T212,\nX242 -> T212,\nT16 -> T213,\nX243 -> T213,\nT210 -> T214", fontsize=14, style = filled, fillcolor = lightblue];
212 -> 352 [arrowhead = none ];
352 -> 216;

353 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
216 -> 353 [arrowhead = none ];
353 -> 218;

354 [label="SPLIT 2\nnew knowledge:\nT211 is ground\nreplacements:T214 -> T217", fontsize=14, style = filled, fillcolor = violet];
216 -> 354 [arrowhead = none ];
354 -> 219;

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

356 [label="INSTANCE with matching:\nT1 -> T217\nT2 -> T213", fontsize=14, style = filled, fillcolor = lightgrey];
219 -> 356 [arrowhead = none , style=dashed];
356 -> 1[style=dashed];

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

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

359 [label="EVAL with clause\nless(0, s(X252)).\nand substitutionT211 -> 0,\nX252 -> T224,\nT214 -> s(T224)", fontsize=14, style = filled, fillcolor = lightblue];
221 -> 359 [arrowhead = none ];
359 -> 223;

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

361 [label="EVAL with clause\nless(s(X257), s(X258)) :- less(X257, X258).\nand substitutionX257 -> T229,\nT211 -> s(T229),\nX258 -> T231,\nT214 -> s(T231),\nT230 -> T231", fontsize=14, style = filled, fillcolor = lightblue];
222 -> 361 [arrowhead = none ];
361 -> 226;

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

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

364 [label="INSTANCE with matching:\nT211 -> T229\nT214 -> T231", fontsize=14, style = filled, fillcolor = lightgrey];
226 -> 364 [arrowhead = none , style=dashed];
364 -> 218[style=dashed];

365 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
229 -> 365 [arrowhead = none ];
365 -> 231;

366 [label="EVAL with clause\nin(X318, tree(X319, X320, X321)) :- ','(less(X319, X318), in(X318, X321)).\nand substitutionT1 -> T297,\nX318 -> T297,\nX319 -> T294,\nX320 -> T295,\nX321 -> T296,\nT2 -> tree(T294, T295, T296),\nT293 -> T297", fontsize=14, style = filled, fillcolor = lightblue];
230 -> 366 [arrowhead = none ];
366 -> 253;

367 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
230 -> 367 [arrowhead = none ];
367 -> 254;

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

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

370 [label="EVAL with clause\nless(0, s(X279)).\nand substitutionT248 -> 0,\nX279 -> T253,\nT245 -> s(T253)", fontsize=14, style = filled, fillcolor = lightblue];
232 -> 370 [arrowhead = none ];
370 -> 234;

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

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

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

374 [label="INSTANCE with matching:\nT15 -> T246", fontsize=14, style = filled, fillcolor = lightgrey];
234 -> 374 [arrowhead = none , style=dashed];
374 -> 31[style=dashed];

375 [label="EVAL with clause\nless(s(X294), s(X295)) :- less(X294, X295).\nand substitutionX294 -> T268,\nT248 -> s(T268),\nX295 -> T267,\nT245 -> s(T267),\nT266 -> T268", fontsize=14, style = filled, fillcolor = lightblue];
237 -> 375 [arrowhead = none ];
375 -> 239;

376 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
237 -> 376 [arrowhead = none ];
376 -> 240;

377 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
238 -> 377 [arrowhead = none ];
377 -> 241;

378 [label="INSTANCE with matching:\nT89 -> T268\nT88 -> T267\nT15 -> T246", fontsize=14, style = filled, fillcolor = lightgrey];
239 -> 378 [arrowhead = none , style=dashed];
378 -> 132[style=dashed];

379 [label="ONLY EVAL with clause\nin(X308, tree(X309, X310, X311)) :- ','(less(X309, X308), in(X308, X311)).\nand substitutionT1 -> T286,\nX308 -> T286,\nT245 -> T283,\nX309 -> T283,\nT246 -> T284,\nX310 -> T284,\nT247 -> T285,\nX311 -> T285,\nT282 -> T286", fontsize=14, style = filled, fillcolor = lightblue];
241 -> 379 [arrowhead = none ];
379 -> 244;

380 [label="INSTANCE with matching:\nT211 -> T283\nT214 -> T286\nT213 -> T285", fontsize=14, style = filled, fillcolor = lightgrey];
244 -> 380 [arrowhead = none , style=dashed];
380 -> 216[style=dashed];

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

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

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

384 [label="EVAL with clause\nless(0, s(X326)).\nand substitutionT294 -> 0,\nX326 -> T303,\nT297 -> s(T303),\nT302 -> T303", fontsize=14, style = filled, fillcolor = lightblue];
256 -> 384 [arrowhead = none ];
384 -> 258;

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

386 [label="EVAL with clause\nless(s(X337), s(X338)) :- less(X337, X338).\nand substitutionX337 -> T314,\nT294 -> s(T314),\nX338 -> T316,\nT297 -> s(T316),\nT315 -> T316", fontsize=14, style = filled, fillcolor = lightblue];
257 -> 386 [arrowhead = none ];
386 -> 260;

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

388 [label="INSTANCE with matching:\nT1 -> s(T303)\nT2 -> T296", fontsize=14, style = filled, fillcolor = lightgrey];
258 -> 388 [arrowhead = none , style=dashed];
388 -> 1[style=dashed];

389 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
260 -> 389 [arrowhead = none ];
389 -> 262;

390 [label="SPLIT 2\nnew knowledge:\nT314 is ground\nreplacements:T316 -> T319,\nT1 -> T320", fontsize=14, style = filled, fillcolor = violet];
260 -> 390 [arrowhead = none ];
390 -> 263;

391 [label="INSTANCE with matching:\nT211 -> T314\nT214 -> T316", fontsize=14, style = filled, fillcolor = lightgrey];
262 -> 391 [arrowhead = none , style=dashed];
391 -> 218[style=dashed];

392 [label="INSTANCE with matching:\nT1 -> s(T319)\nT2 -> T296", fontsize=14, style = filled, fillcolor = lightgrey];
263 -> 392 [arrowhead = none , style=dashed];
392 -> 1[style=dashed];

}

(2) Obligation:

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

inA_in_ag(T6, tree(T6, T7, T8)) → inA_out_ag(T6, tree(T6, T7, T8))
inA_in_ag(0, tree(s(T22), T15, T16)) → U1_ag(T22, T15, T16, inB_in_g(T15))
inB_in_g(tree(0, T35, T36)) → inB_out_g(tree(0, T35, T36))
inB_in_g(tree(T49, T50, T51)) → U9_g(T49, T50, T51, pF_in_gg(T49, T50))
pF_in_gg(T49, T50) → U16_gg(T49, T50, lessN_in_g(T49))
lessN_in_g(s(T60)) → lessN_out_g(s(T60))
U16_gg(T49, T50, lessN_out_g(T49)) → U17_gg(T49, T50, inB_in_g(T50))
U17_gg(T49, T50, inB_out_g(T50)) → pF_out_gg(T49, T50)
U9_g(T49, T50, T51, pF_out_gg(T49, T50)) → inB_out_g(tree(T49, T50, T51))
U1_ag(T22, T15, T16, inB_out_g(T15)) → inA_out_ag(0, tree(s(T22), T15, T16))
inA_in_ag(s(T89), tree(s(T88), T15, T16)) → U2_ag(T89, T88, T15, T16, pC_in_agg(T89, T88, T15))
pC_in_agg(T92, T88, T15) → U18_agg(T92, T88, T15, lessH_in_ag(T92, T88))
lessH_in_ag(0, s(T99)) → lessH_out_ag(0, s(T99))
lessH_in_ag(s(T106), s(T105)) → U10_ag(T106, T105, lessH_in_ag(T106, T105))
U10_ag(T106, T105, lessH_out_ag(T106, T105)) → lessH_out_ag(s(T106), s(T105))
U18_agg(T92, T88, T15, lessH_out_ag(T92, T88)) → U19_agg(T92, T88, T15, inI_in_gg(T92, T15))
inI_in_gg(T127, tree(s(T127), T128, T129)) → inI_out_gg(T127, tree(s(T127), T128, T129))
inI_in_gg(T146, tree(T147, T148, T149)) → U11_gg(T146, T147, T148, T149, pJ_in_ggg(T146, T147, T148))
pJ_in_ggg(T146, T147, T148) → U20_ggg(T146, T147, T148, lessO_in_gg(T146, T147))
lessO_in_gg(T154, s(T155)) → U15_gg(T154, T155, lessL_in_gg(T154, T155))
lessL_in_gg(0, s(T162)) → lessL_out_gg(0, s(T162))
lessL_in_gg(s(T167), s(T168)) → U13_gg(T167, T168, lessL_in_gg(T167, T168))
U13_gg(T167, T168, lessL_out_gg(T167, T168)) → lessL_out_gg(s(T167), s(T168))
U15_gg(T154, T155, lessL_out_gg(T154, T155)) → lessO_out_gg(T154, s(T155))
U20_ggg(T146, T147, T148, lessO_out_gg(T146, T147)) → U21_ggg(T146, T147, T148, inI_in_gg(T146, T148))
inI_in_gg(T185, tree(T186, T187, T188)) → U12_gg(T185, T186, T187, T188, pK_in_ggg(T186, T185, T188))
pK_in_ggg(T186, T185, T188) → U22_ggg(T186, T185, T188, lessL_in_gg(T186, s(T185)))
U22_ggg(T186, T185, T188, lessL_out_gg(T186, s(T185))) → U23_ggg(T186, T185, T188, inI_in_gg(T185, T188))
U23_ggg(T186, T185, T188, inI_out_gg(T185, T188)) → pK_out_ggg(T186, T185, T188)
U12_gg(T185, T186, T187, T188, pK_out_ggg(T186, T185, T188)) → inI_out_gg(T185, tree(T186, T187, T188))
U21_ggg(T146, T147, T148, inI_out_gg(T146, T148)) → pJ_out_ggg(T146, T147, T148)
U11_gg(T146, T147, T148, T149, pJ_out_ggg(T146, T147, T148)) → inI_out_gg(T146, tree(T147, T148, T149))
U19_agg(T92, T88, T15, inI_out_gg(T92, T15)) → pC_out_agg(T92, T88, T15)
U2_ag(T89, T88, T15, T16, pC_out_agg(T89, T88, T15)) → inA_out_ag(s(T89), tree(s(T88), T15, T16))
inA_in_ag(T214, tree(T211, T212, T213)) → U3_ag(T214, T211, T212, T213, pD_in_gag(T211, T214, T213))
pD_in_gag(T211, T217, T213) → U24_gag(T211, T217, T213, lessM_in_ga(T211, T217))
lessM_in_ga(0, s(T224)) → lessM_out_ga(0, s(T224))
lessM_in_ga(s(T229), s(T231)) → U14_ga(T229, T231, lessM_in_ga(T229, T231))
U14_ga(T229, T231, lessM_out_ga(T229, T231)) → lessM_out_ga(s(T229), s(T231))
U24_gag(T211, T217, T213, lessM_out_ga(T211, T217)) → U25_gag(T211, T217, T213, inA_in_ag(T217, T213))
inA_in_ag(0, tree(s(T253), T246, T247)) → U4_ag(T253, T246, T247, inB_in_g(T246))
U4_ag(T253, T246, T247, inB_out_g(T246)) → inA_out_ag(0, tree(s(T253), T246, T247))
inA_in_ag(s(T268), tree(s(T267), T246, T247)) → U5_ag(T268, T267, T246, T247, pC_in_agg(T268, T267, T246))
U5_ag(T268, T267, T246, T247, pC_out_agg(T268, T267, T246)) → inA_out_ag(s(T268), tree(s(T267), T246, T247))
inA_in_ag(T286, tree(T283, T284, T285)) → U6_ag(T286, T283, T284, T285, pD_in_gag(T283, T286, T285))
U6_ag(T286, T283, T284, T285, pD_out_gag(T283, T286, T285)) → inA_out_ag(T286, tree(T283, T284, T285))
inA_in_ag(s(T303), tree(0, T295, T296)) → U7_ag(T303, T295, T296, inA_in_ag(s(T303), T296))
inA_in_ag(s(T316), tree(s(T314), T295, T296)) → U8_ag(T316, T314, T295, T296, pE_in_gag(T314, T316, T296))
pE_in_gag(T314, T319, T296) → U26_gag(T314, T319, T296, lessM_in_ga(T314, T319))
U26_gag(T314, T319, T296, lessM_out_ga(T314, T319)) → U27_gag(T314, T319, T296, inA_in_ag(s(T319), T296))
U27_gag(T314, T319, T296, inA_out_ag(s(T319), T296)) → pE_out_gag(T314, T319, T296)
U8_ag(T316, T314, T295, T296, pE_out_gag(T314, T316, T296)) → inA_out_ag(s(T316), tree(s(T314), T295, T296))
U7_ag(T303, T295, T296, inA_out_ag(s(T303), T296)) → inA_out_ag(s(T303), tree(0, T295, T296))
U25_gag(T211, T217, T213, inA_out_ag(T217, T213)) → pD_out_gag(T211, T217, T213)
U3_ag(T214, T211, T212, T213, pD_out_gag(T211, T214, T213)) → inA_out_ag(T214, tree(T211, T212, T213))

The argument filtering Pi contains the following mapping:
inA_in_ag(x1, x2)  =  inA_in_ag(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
inA_out_ag(x1, x2)  =  inA_out_ag(x1, x2)
s(x1)  =  s(x1)
U1_ag(x1, x2, x3, x4)  =  U1_ag(x1, x2, x3, x4)
inB_in_g(x1)  =  inB_in_g(x1)
0  =  0
inB_out_g(x1)  =  inB_out_g(x1)
U9_g(x1, x2, x3, x4)  =  U9_g(x1, x2, x3, x4)
pF_in_gg(x1, x2)  =  pF_in_gg(x1, x2)
U16_gg(x1, x2, x3)  =  U16_gg(x1, x2, x3)
lessN_in_g(x1)  =  lessN_in_g(x1)
lessN_out_g(x1)  =  lessN_out_g(x1)
U17_gg(x1, x2, x3)  =  U17_gg(x1, x2, x3)
pF_out_gg(x1, x2)  =  pF_out_gg(x1, x2)
U2_ag(x1, x2, x3, x4, x5)  =  U2_ag(x2, x3, x4, x5)
pC_in_agg(x1, x2, x3)  =  pC_in_agg(x2, x3)
U18_agg(x1, x2, x3, x4)  =  U18_agg(x2, x3, x4)
lessH_in_ag(x1, x2)  =  lessH_in_ag(x2)
lessH_out_ag(x1, x2)  =  lessH_out_ag(x1, x2)
U10_ag(x1, x2, x3)  =  U10_ag(x2, x3)
U19_agg(x1, x2, x3, x4)  =  U19_agg(x1, x2, x3, x4)
inI_in_gg(x1, x2)  =  inI_in_gg(x1, x2)
inI_out_gg(x1, x2)  =  inI_out_gg(x1, x2)
U11_gg(x1, x2, x3, x4, x5)  =  U11_gg(x1, x2, x3, x4, x5)
pJ_in_ggg(x1, x2, x3)  =  pJ_in_ggg(x1, x2, x3)
U20_ggg(x1, x2, x3, x4)  =  U20_ggg(x1, x2, x3, x4)
lessO_in_gg(x1, x2)  =  lessO_in_gg(x1, x2)
U15_gg(x1, x2, x3)  =  U15_gg(x1, x2, x3)
lessL_in_gg(x1, x2)  =  lessL_in_gg(x1, x2)
lessL_out_gg(x1, x2)  =  lessL_out_gg(x1, x2)
U13_gg(x1, x2, x3)  =  U13_gg(x1, x2, x3)
lessO_out_gg(x1, x2)  =  lessO_out_gg(x1, x2)
U21_ggg(x1, x2, x3, x4)  =  U21_ggg(x1, x2, x3, x4)
U12_gg(x1, x2, x3, x4, x5)  =  U12_gg(x1, x2, x3, x4, x5)
pK_in_ggg(x1, x2, x3)  =  pK_in_ggg(x1, x2, x3)
U22_ggg(x1, x2, x3, x4)  =  U22_ggg(x1, x2, x3, x4)
U23_ggg(x1, x2, x3, x4)  =  U23_ggg(x1, x2, x3, x4)
pK_out_ggg(x1, x2, x3)  =  pK_out_ggg(x1, x2, x3)
pJ_out_ggg(x1, x2, x3)  =  pJ_out_ggg(x1, x2, x3)
pC_out_agg(x1, x2, x3)  =  pC_out_agg(x1, x2, x3)
U3_ag(x1, x2, x3, x4, x5)  =  U3_ag(x2, x3, x4, x5)
pD_in_gag(x1, x2, x3)  =  pD_in_gag(x1, x3)
U24_gag(x1, x2, x3, x4)  =  U24_gag(x1, x3, x4)
lessM_in_ga(x1, x2)  =  lessM_in_ga(x1)
lessM_out_ga(x1, x2)  =  lessM_out_ga(x1)
U14_ga(x1, x2, x3)  =  U14_ga(x1, x3)
U25_gag(x1, x2, x3, x4)  =  U25_gag(x1, x3, x4)
U4_ag(x1, x2, x3, x4)  =  U4_ag(x1, x2, x3, x4)
U5_ag(x1, x2, x3, x4, x5)  =  U5_ag(x2, x3, x4, x5)
U6_ag(x1, x2, x3, x4, x5)  =  U6_ag(x2, x3, x4, x5)
pD_out_gag(x1, x2, x3)  =  pD_out_gag(x1, x2, x3)
U7_ag(x1, x2, x3, x4)  =  U7_ag(x2, x3, x4)
U8_ag(x1, x2, x3, x4, x5)  =  U8_ag(x2, x3, x4, x5)
pE_in_gag(x1, x2, x3)  =  pE_in_gag(x1, x3)
U26_gag(x1, x2, x3, x4)  =  U26_gag(x1, x3, x4)
U27_gag(x1, x2, x3, x4)  =  U27_gag(x1, x3, x4)
pE_out_gag(x1, x2, x3)  =  pE_out_gag(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:

INA_IN_AG(0, tree(s(T22), T15, T16)) → U1_AG(T22, T15, T16, inB_in_g(T15))
INA_IN_AG(0, tree(s(T22), T15, T16)) → INB_IN_G(T15)
INB_IN_G(tree(T49, T50, T51)) → U9_G(T49, T50, T51, pF_in_gg(T49, T50))
INB_IN_G(tree(T49, T50, T51)) → PF_IN_GG(T49, T50)
PF_IN_GG(T49, T50) → U16_GG(T49, T50, lessN_in_g(T49))
PF_IN_GG(T49, T50) → LESSN_IN_G(T49)
U16_GG(T49, T50, lessN_out_g(T49)) → U17_GG(T49, T50, inB_in_g(T50))
U16_GG(T49, T50, lessN_out_g(T49)) → INB_IN_G(T50)
INA_IN_AG(s(T89), tree(s(T88), T15, T16)) → U2_AG(T89, T88, T15, T16, pC_in_agg(T89, T88, T15))
INA_IN_AG(s(T89), tree(s(T88), T15, T16)) → PC_IN_AGG(T89, T88, T15)
PC_IN_AGG(T92, T88, T15) → U18_AGG(T92, T88, T15, lessH_in_ag(T92, T88))
PC_IN_AGG(T92, T88, T15) → LESSH_IN_AG(T92, T88)
LESSH_IN_AG(s(T106), s(T105)) → U10_AG(T106, T105, lessH_in_ag(T106, T105))
LESSH_IN_AG(s(T106), s(T105)) → LESSH_IN_AG(T106, T105)
U18_AGG(T92, T88, T15, lessH_out_ag(T92, T88)) → U19_AGG(T92, T88, T15, inI_in_gg(T92, T15))
U18_AGG(T92, T88, T15, lessH_out_ag(T92, T88)) → INI_IN_GG(T92, T15)
INI_IN_GG(T146, tree(T147, T148, T149)) → U11_GG(T146, T147, T148, T149, pJ_in_ggg(T146, T147, T148))
INI_IN_GG(T146, tree(T147, T148, T149)) → PJ_IN_GGG(T146, T147, T148)
PJ_IN_GGG(T146, T147, T148) → U20_GGG(T146, T147, T148, lessO_in_gg(T146, T147))
PJ_IN_GGG(T146, T147, T148) → LESSO_IN_GG(T146, T147)
LESSO_IN_GG(T154, s(T155)) → U15_GG(T154, T155, lessL_in_gg(T154, T155))
LESSO_IN_GG(T154, s(T155)) → LESSL_IN_GG(T154, T155)
LESSL_IN_GG(s(T167), s(T168)) → U13_GG(T167, T168, lessL_in_gg(T167, T168))
LESSL_IN_GG(s(T167), s(T168)) → LESSL_IN_GG(T167, T168)
U20_GGG(T146, T147, T148, lessO_out_gg(T146, T147)) → U21_GGG(T146, T147, T148, inI_in_gg(T146, T148))
U20_GGG(T146, T147, T148, lessO_out_gg(T146, T147)) → INI_IN_GG(T146, T148)
INI_IN_GG(T185, tree(T186, T187, T188)) → U12_GG(T185, T186, T187, T188, pK_in_ggg(T186, T185, T188))
INI_IN_GG(T185, tree(T186, T187, T188)) → PK_IN_GGG(T186, T185, T188)
PK_IN_GGG(T186, T185, T188) → U22_GGG(T186, T185, T188, lessL_in_gg(T186, s(T185)))
PK_IN_GGG(T186, T185, T188) → LESSL_IN_GG(T186, s(T185))
U22_GGG(T186, T185, T188, lessL_out_gg(T186, s(T185))) → U23_GGG(T186, T185, T188, inI_in_gg(T185, T188))
U22_GGG(T186, T185, T188, lessL_out_gg(T186, s(T185))) → INI_IN_GG(T185, T188)
INA_IN_AG(T214, tree(T211, T212, T213)) → U3_AG(T214, T211, T212, T213, pD_in_gag(T211, T214, T213))
INA_IN_AG(T214, tree(T211, T212, T213)) → PD_IN_GAG(T211, T214, T213)
PD_IN_GAG(T211, T217, T213) → U24_GAG(T211, T217, T213, lessM_in_ga(T211, T217))
PD_IN_GAG(T211, T217, T213) → LESSM_IN_GA(T211, T217)
LESSM_IN_GA(s(T229), s(T231)) → U14_GA(T229, T231, lessM_in_ga(T229, T231))
LESSM_IN_GA(s(T229), s(T231)) → LESSM_IN_GA(T229, T231)
U24_GAG(T211, T217, T213, lessM_out_ga(T211, T217)) → U25_GAG(T211, T217, T213, inA_in_ag(T217, T213))
U24_GAG(T211, T217, T213, lessM_out_ga(T211, T217)) → INA_IN_AG(T217, T213)
INA_IN_AG(0, tree(s(T253), T246, T247)) → U4_AG(T253, T246, T247, inB_in_g(T246))
INA_IN_AG(s(T268), tree(s(T267), T246, T247)) → U5_AG(T268, T267, T246, T247, pC_in_agg(T268, T267, T246))
INA_IN_AG(T286, tree(T283, T284, T285)) → U6_AG(T286, T283, T284, T285, pD_in_gag(T283, T286, T285))
INA_IN_AG(s(T303), tree(0, T295, T296)) → U7_AG(T303, T295, T296, inA_in_ag(s(T303), T296))
INA_IN_AG(s(T303), tree(0, T295, T296)) → INA_IN_AG(s(T303), T296)
INA_IN_AG(s(T316), tree(s(T314), T295, T296)) → U8_AG(T316, T314, T295, T296, pE_in_gag(T314, T316, T296))
INA_IN_AG(s(T316), tree(s(T314), T295, T296)) → PE_IN_GAG(T314, T316, T296)
PE_IN_GAG(T314, T319, T296) → U26_GAG(T314, T319, T296, lessM_in_ga(T314, T319))
PE_IN_GAG(T314, T319, T296) → LESSM_IN_GA(T314, T319)
U26_GAG(T314, T319, T296, lessM_out_ga(T314, T319)) → U27_GAG(T314, T319, T296, inA_in_ag(s(T319), T296))
U26_GAG(T314, T319, T296, lessM_out_ga(T314, T319)) → INA_IN_AG(s(T319), T296)

The TRS R consists of the following rules:

inA_in_ag(T6, tree(T6, T7, T8)) → inA_out_ag(T6, tree(T6, T7, T8))
inA_in_ag(0, tree(s(T22), T15, T16)) → U1_ag(T22, T15, T16, inB_in_g(T15))
inB_in_g(tree(0, T35, T36)) → inB_out_g(tree(0, T35, T36))
inB_in_g(tree(T49, T50, T51)) → U9_g(T49, T50, T51, pF_in_gg(T49, T50))
pF_in_gg(T49, T50) → U16_gg(T49, T50, lessN_in_g(T49))
lessN_in_g(s(T60)) → lessN_out_g(s(T60))
U16_gg(T49, T50, lessN_out_g(T49)) → U17_gg(T49, T50, inB_in_g(T50))
U17_gg(T49, T50, inB_out_g(T50)) → pF_out_gg(T49, T50)
U9_g(T49, T50, T51, pF_out_gg(T49, T50)) → inB_out_g(tree(T49, T50, T51))
U1_ag(T22, T15, T16, inB_out_g(T15)) → inA_out_ag(0, tree(s(T22), T15, T16))
inA_in_ag(s(T89), tree(s(T88), T15, T16)) → U2_ag(T89, T88, T15, T16, pC_in_agg(T89, T88, T15))
pC_in_agg(T92, T88, T15) → U18_agg(T92, T88, T15, lessH_in_ag(T92, T88))
lessH_in_ag(0, s(T99)) → lessH_out_ag(0, s(T99))
lessH_in_ag(s(T106), s(T105)) → U10_ag(T106, T105, lessH_in_ag(T106, T105))
U10_ag(T106, T105, lessH_out_ag(T106, T105)) → lessH_out_ag(s(T106), s(T105))
U18_agg(T92, T88, T15, lessH_out_ag(T92, T88)) → U19_agg(T92, T88, T15, inI_in_gg(T92, T15))
inI_in_gg(T127, tree(s(T127), T128, T129)) → inI_out_gg(T127, tree(s(T127), T128, T129))
inI_in_gg(T146, tree(T147, T148, T149)) → U11_gg(T146, T147, T148, T149, pJ_in_ggg(T146, T147, T148))
pJ_in_ggg(T146, T147, T148) → U20_ggg(T146, T147, T148, lessO_in_gg(T146, T147))
lessO_in_gg(T154, s(T155)) → U15_gg(T154, T155, lessL_in_gg(T154, T155))
lessL_in_gg(0, s(T162)) → lessL_out_gg(0, s(T162))
lessL_in_gg(s(T167), s(T168)) → U13_gg(T167, T168, lessL_in_gg(T167, T168))
U13_gg(T167, T168, lessL_out_gg(T167, T168)) → lessL_out_gg(s(T167), s(T168))
U15_gg(T154, T155, lessL_out_gg(T154, T155)) → lessO_out_gg(T154, s(T155))
U20_ggg(T146, T147, T148, lessO_out_gg(T146, T147)) → U21_ggg(T146, T147, T148, inI_in_gg(T146, T148))
inI_in_gg(T185, tree(T186, T187, T188)) → U12_gg(T185, T186, T187, T188, pK_in_ggg(T186, T185, T188))
pK_in_ggg(T186, T185, T188) → U22_ggg(T186, T185, T188, lessL_in_gg(T186, s(T185)))
U22_ggg(T186, T185, T188, lessL_out_gg(T186, s(T185))) → U23_ggg(T186, T185, T188, inI_in_gg(T185, T188))
U23_ggg(T186, T185, T188, inI_out_gg(T185, T188)) → pK_out_ggg(T186, T185, T188)
U12_gg(T185, T186, T187, T188, pK_out_ggg(T186, T185, T188)) → inI_out_gg(T185, tree(T186, T187, T188))
U21_ggg(T146, T147, T148, inI_out_gg(T146, T148)) → pJ_out_ggg(T146, T147, T148)
U11_gg(T146, T147, T148, T149, pJ_out_ggg(T146, T147, T148)) → inI_out_gg(T146, tree(T147, T148, T149))
U19_agg(T92, T88, T15, inI_out_gg(T92, T15)) → pC_out_agg(T92, T88, T15)
U2_ag(T89, T88, T15, T16, pC_out_agg(T89, T88, T15)) → inA_out_ag(s(T89), tree(s(T88), T15, T16))
inA_in_ag(T214, tree(T211, T212, T213)) → U3_ag(T214, T211, T212, T213, pD_in_gag(T211, T214, T213))
pD_in_gag(T211, T217, T213) → U24_gag(T211, T217, T213, lessM_in_ga(T211, T217))
lessM_in_ga(0, s(T224)) → lessM_out_ga(0, s(T224))
lessM_in_ga(s(T229), s(T231)) → U14_ga(T229, T231, lessM_in_ga(T229, T231))
U14_ga(T229, T231, lessM_out_ga(T229, T231)) → lessM_out_ga(s(T229), s(T231))
U24_gag(T211, T217, T213, lessM_out_ga(T211, T217)) → U25_gag(T211, T217, T213, inA_in_ag(T217, T213))
inA_in_ag(0, tree(s(T253), T246, T247)) → U4_ag(T253, T246, T247, inB_in_g(T246))
U4_ag(T253, T246, T247, inB_out_g(T246)) → inA_out_ag(0, tree(s(T253), T246, T247))
inA_in_ag(s(T268), tree(s(T267), T246, T247)) → U5_ag(T268, T267, T246, T247, pC_in_agg(T268, T267, T246))
U5_ag(T268, T267, T246, T247, pC_out_agg(T268, T267, T246)) → inA_out_ag(s(T268), tree(s(T267), T246, T247))
inA_in_ag(T286, tree(T283, T284, T285)) → U6_ag(T286, T283, T284, T285, pD_in_gag(T283, T286, T285))
U6_ag(T286, T283, T284, T285, pD_out_gag(T283, T286, T285)) → inA_out_ag(T286, tree(T283, T284, T285))
inA_in_ag(s(T303), tree(0, T295, T296)) → U7_ag(T303, T295, T296, inA_in_ag(s(T303), T296))
inA_in_ag(s(T316), tree(s(T314), T295, T296)) → U8_ag(T316, T314, T295, T296, pE_in_gag(T314, T316, T296))
pE_in_gag(T314, T319, T296) → U26_gag(T314, T319, T296, lessM_in_ga(T314, T319))
U26_gag(T314, T319, T296, lessM_out_ga(T314, T319)) → U27_gag(T314, T319, T296, inA_in_ag(s(T319), T296))
U27_gag(T314, T319, T296, inA_out_ag(s(T319), T296)) → pE_out_gag(T314, T319, T296)
U8_ag(T316, T314, T295, T296, pE_out_gag(T314, T316, T296)) → inA_out_ag(s(T316), tree(s(T314), T295, T296))
U7_ag(T303, T295, T296, inA_out_ag(s(T303), T296)) → inA_out_ag(s(T303), tree(0, T295, T296))
U25_gag(T211, T217, T213, inA_out_ag(T217, T213)) → pD_out_gag(T211, T217, T213)
U3_ag(T214, T211, T212, T213, pD_out_gag(T211, T214, T213)) → inA_out_ag(T214, tree(T211, T212, T213))

The argument filtering Pi contains the following mapping:
inA_in_ag(x1, x2)  =  inA_in_ag(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
inA_out_ag(x1, x2)  =  inA_out_ag(x1, x2)
s(x1)  =  s(x1)
U1_ag(x1, x2, x3, x4)  =  U1_ag(x1, x2, x3, x4)
inB_in_g(x1)  =  inB_in_g(x1)
0  =  0
inB_out_g(x1)  =  inB_out_g(x1)
U9_g(x1, x2, x3, x4)  =  U9_g(x1, x2, x3, x4)
pF_in_gg(x1, x2)  =  pF_in_gg(x1, x2)
U16_gg(x1, x2, x3)  =  U16_gg(x1, x2, x3)
lessN_in_g(x1)  =  lessN_in_g(x1)
lessN_out_g(x1)  =  lessN_out_g(x1)
U17_gg(x1, x2, x3)  =  U17_gg(x1, x2, x3)
pF_out_gg(x1, x2)  =  pF_out_gg(x1, x2)
U2_ag(x1, x2, x3, x4, x5)  =  U2_ag(x2, x3, x4, x5)
pC_in_agg(x1, x2, x3)  =  pC_in_agg(x2, x3)
U18_agg(x1, x2, x3, x4)  =  U18_agg(x2, x3, x4)
lessH_in_ag(x1, x2)  =  lessH_in_ag(x2)
lessH_out_ag(x1, x2)  =  lessH_out_ag(x1, x2)
U10_ag(x1, x2, x3)  =  U10_ag(x2, x3)
U19_agg(x1, x2, x3, x4)  =  U19_agg(x1, x2, x3, x4)
inI_in_gg(x1, x2)  =  inI_in_gg(x1, x2)
inI_out_gg(x1, x2)  =  inI_out_gg(x1, x2)
U11_gg(x1, x2, x3, x4, x5)  =  U11_gg(x1, x2, x3, x4, x5)
pJ_in_ggg(x1, x2, x3)  =  pJ_in_ggg(x1, x2, x3)
U20_ggg(x1, x2, x3, x4)  =  U20_ggg(x1, x2, x3, x4)
lessO_in_gg(x1, x2)  =  lessO_in_gg(x1, x2)
U15_gg(x1, x2, x3)  =  U15_gg(x1, x2, x3)
lessL_in_gg(x1, x2)  =  lessL_in_gg(x1, x2)
lessL_out_gg(x1, x2)  =  lessL_out_gg(x1, x2)
U13_gg(x1, x2, x3)  =  U13_gg(x1, x2, x3)
lessO_out_gg(x1, x2)  =  lessO_out_gg(x1, x2)
U21_ggg(x1, x2, x3, x4)  =  U21_ggg(x1, x2, x3, x4)
U12_gg(x1, x2, x3, x4, x5)  =  U12_gg(x1, x2, x3, x4, x5)
pK_in_ggg(x1, x2, x3)  =  pK_in_ggg(x1, x2, x3)
U22_ggg(x1, x2, x3, x4)  =  U22_ggg(x1, x2, x3, x4)
U23_ggg(x1, x2, x3, x4)  =  U23_ggg(x1, x2, x3, x4)
pK_out_ggg(x1, x2, x3)  =  pK_out_ggg(x1, x2, x3)
pJ_out_ggg(x1, x2, x3)  =  pJ_out_ggg(x1, x2, x3)
pC_out_agg(x1, x2, x3)  =  pC_out_agg(x1, x2, x3)
U3_ag(x1, x2, x3, x4, x5)  =  U3_ag(x2, x3, x4, x5)
pD_in_gag(x1, x2, x3)  =  pD_in_gag(x1, x3)
U24_gag(x1, x2, x3, x4)  =  U24_gag(x1, x3, x4)
lessM_in_ga(x1, x2)  =  lessM_in_ga(x1)
lessM_out_ga(x1, x2)  =  lessM_out_ga(x1)
U14_ga(x1, x2, x3)  =  U14_ga(x1, x3)
U25_gag(x1, x2, x3, x4)  =  U25_gag(x1, x3, x4)
U4_ag(x1, x2, x3, x4)  =  U4_ag(x1, x2, x3, x4)
U5_ag(x1, x2, x3, x4, x5)  =  U5_ag(x2, x3, x4, x5)
U6_ag(x1, x2, x3, x4, x5)  =  U6_ag(x2, x3, x4, x5)
pD_out_gag(x1, x2, x3)  =  pD_out_gag(x1, x2, x3)
U7_ag(x1, x2, x3, x4)  =  U7_ag(x2, x3, x4)
U8_ag(x1, x2, x3, x4, x5)  =  U8_ag(x2, x3, x4, x5)
pE_in_gag(x1, x2, x3)  =  pE_in_gag(x1, x3)
U26_gag(x1, x2, x3, x4)  =  U26_gag(x1, x3, x4)
U27_gag(x1, x2, x3, x4)  =  U27_gag(x1, x3, x4)
pE_out_gag(x1, x2, x3)  =  pE_out_gag(x1, x2, x3)
INA_IN_AG(x1, x2)  =  INA_IN_AG(x2)
U1_AG(x1, x2, x3, x4)  =  U1_AG(x1, x2, x3, x4)
INB_IN_G(x1)  =  INB_IN_G(x1)
U9_G(x1, x2, x3, x4)  =  U9_G(x1, x2, x3, x4)
PF_IN_GG(x1, x2)  =  PF_IN_GG(x1, x2)
U16_GG(x1, x2, x3)  =  U16_GG(x1, x2, x3)
LESSN_IN_G(x1)  =  LESSN_IN_G(x1)
U17_GG(x1, x2, x3)  =  U17_GG(x1, x2, x3)
U2_AG(x1, x2, x3, x4, x5)  =  U2_AG(x2, x3, x4, x5)
PC_IN_AGG(x1, x2, x3)  =  PC_IN_AGG(x2, x3)
U18_AGG(x1, x2, x3, x4)  =  U18_AGG(x2, x3, x4)
LESSH_IN_AG(x1, x2)  =  LESSH_IN_AG(x2)
U10_AG(x1, x2, x3)  =  U10_AG(x2, x3)
U19_AGG(x1, x2, x3, x4)  =  U19_AGG(x1, x2, x3, x4)
INI_IN_GG(x1, x2)  =  INI_IN_GG(x1, x2)
U11_GG(x1, x2, x3, x4, x5)  =  U11_GG(x1, x2, x3, x4, x5)
PJ_IN_GGG(x1, x2, x3)  =  PJ_IN_GGG(x1, x2, x3)
U20_GGG(x1, x2, x3, x4)  =  U20_GGG(x1, x2, x3, x4)
LESSO_IN_GG(x1, x2)  =  LESSO_IN_GG(x1, x2)
U15_GG(x1, x2, x3)  =  U15_GG(x1, x2, x3)
LESSL_IN_GG(x1, x2)  =  LESSL_IN_GG(x1, x2)
U13_GG(x1, x2, x3)  =  U13_GG(x1, x2, x3)
U21_GGG(x1, x2, x3, x4)  =  U21_GGG(x1, x2, x3, x4)
U12_GG(x1, x2, x3, x4, x5)  =  U12_GG(x1, x2, x3, x4, x5)
PK_IN_GGG(x1, x2, x3)  =  PK_IN_GGG(x1, x2, x3)
U22_GGG(x1, x2, x3, x4)  =  U22_GGG(x1, x2, x3, x4)
U23_GGG(x1, x2, x3, x4)  =  U23_GGG(x1, x2, x3, x4)
U3_AG(x1, x2, x3, x4, x5)  =  U3_AG(x2, x3, x4, x5)
PD_IN_GAG(x1, x2, x3)  =  PD_IN_GAG(x1, x3)
U24_GAG(x1, x2, x3, x4)  =  U24_GAG(x1, x3, x4)
LESSM_IN_GA(x1, x2)  =  LESSM_IN_GA(x1)
U14_GA(x1, x2, x3)  =  U14_GA(x1, x3)
U25_GAG(x1, x2, x3, x4)  =  U25_GAG(x1, x3, x4)
U4_AG(x1, x2, x3, x4)  =  U4_AG(x1, x2, x3, x4)
U5_AG(x1, x2, x3, x4, x5)  =  U5_AG(x2, x3, x4, x5)
U6_AG(x1, x2, x3, x4, x5)  =  U6_AG(x2, x3, x4, x5)
U7_AG(x1, x2, x3, x4)  =  U7_AG(x2, x3, x4)
U8_AG(x1, x2, x3, x4, x5)  =  U8_AG(x2, x3, x4, x5)
PE_IN_GAG(x1, x2, x3)  =  PE_IN_GAG(x1, x3)
U26_GAG(x1, x2, x3, x4)  =  U26_GAG(x1, x3, x4)
U27_GAG(x1, x2, x3, x4)  =  U27_GAG(x1, x3, x4)

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

(4) Obligation:

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

INA_IN_AG(0, tree(s(T22), T15, T16)) → U1_AG(T22, T15, T16, inB_in_g(T15))
INA_IN_AG(0, tree(s(T22), T15, T16)) → INB_IN_G(T15)
INB_IN_G(tree(T49, T50, T51)) → U9_G(T49, T50, T51, pF_in_gg(T49, T50))
INB_IN_G(tree(T49, T50, T51)) → PF_IN_GG(T49, T50)
PF_IN_GG(T49, T50) → U16_GG(T49, T50, lessN_in_g(T49))
PF_IN_GG(T49, T50) → LESSN_IN_G(T49)
U16_GG(T49, T50, lessN_out_g(T49)) → U17_GG(T49, T50, inB_in_g(T50))
U16_GG(T49, T50, lessN_out_g(T49)) → INB_IN_G(T50)
INA_IN_AG(s(T89), tree(s(T88), T15, T16)) → U2_AG(T89, T88, T15, T16, pC_in_agg(T89, T88, T15))
INA_IN_AG(s(T89), tree(s(T88), T15, T16)) → PC_IN_AGG(T89, T88, T15)
PC_IN_AGG(T92, T88, T15) → U18_AGG(T92, T88, T15, lessH_in_ag(T92, T88))
PC_IN_AGG(T92, T88, T15) → LESSH_IN_AG(T92, T88)
LESSH_IN_AG(s(T106), s(T105)) → U10_AG(T106, T105, lessH_in_ag(T106, T105))
LESSH_IN_AG(s(T106), s(T105)) → LESSH_IN_AG(T106, T105)
U18_AGG(T92, T88, T15, lessH_out_ag(T92, T88)) → U19_AGG(T92, T88, T15, inI_in_gg(T92, T15))
U18_AGG(T92, T88, T15, lessH_out_ag(T92, T88)) → INI_IN_GG(T92, T15)
INI_IN_GG(T146, tree(T147, T148, T149)) → U11_GG(T146, T147, T148, T149, pJ_in_ggg(T146, T147, T148))
INI_IN_GG(T146, tree(T147, T148, T149)) → PJ_IN_GGG(T146, T147, T148)
PJ_IN_GGG(T146, T147, T148) → U20_GGG(T146, T147, T148, lessO_in_gg(T146, T147))
PJ_IN_GGG(T146, T147, T148) → LESSO_IN_GG(T146, T147)
LESSO_IN_GG(T154, s(T155)) → U15_GG(T154, T155, lessL_in_gg(T154, T155))
LESSO_IN_GG(T154, s(T155)) → LESSL_IN_GG(T154, T155)
LESSL_IN_GG(s(T167), s(T168)) → U13_GG(T167, T168, lessL_in_gg(T167, T168))
LESSL_IN_GG(s(T167), s(T168)) → LESSL_IN_GG(T167, T168)
U20_GGG(T146, T147, T148, lessO_out_gg(T146, T147)) → U21_GGG(T146, T147, T148, inI_in_gg(T146, T148))
U20_GGG(T146, T147, T148, lessO_out_gg(T146, T147)) → INI_IN_GG(T146, T148)
INI_IN_GG(T185, tree(T186, T187, T188)) → U12_GG(T185, T186, T187, T188, pK_in_ggg(T186, T185, T188))
INI_IN_GG(T185, tree(T186, T187, T188)) → PK_IN_GGG(T186, T185, T188)
PK_IN_GGG(T186, T185, T188) → U22_GGG(T186, T185, T188, lessL_in_gg(T186, s(T185)))
PK_IN_GGG(T186, T185, T188) → LESSL_IN_GG(T186, s(T185))
U22_GGG(T186, T185, T188, lessL_out_gg(T186, s(T185))) → U23_GGG(T186, T185, T188, inI_in_gg(T185, T188))
U22_GGG(T186, T185, T188, lessL_out_gg(T186, s(T185))) → INI_IN_GG(T185, T188)
INA_IN_AG(T214, tree(T211, T212, T213)) → U3_AG(T214, T211, T212, T213, pD_in_gag(T211, T214, T213))
INA_IN_AG(T214, tree(T211, T212, T213)) → PD_IN_GAG(T211, T214, T213)
PD_IN_GAG(T211, T217, T213) → U24_GAG(T211, T217, T213, lessM_in_ga(T211, T217))
PD_IN_GAG(T211, T217, T213) → LESSM_IN_GA(T211, T217)
LESSM_IN_GA(s(T229), s(T231)) → U14_GA(T229, T231, lessM_in_ga(T229, T231))
LESSM_IN_GA(s(T229), s(T231)) → LESSM_IN_GA(T229, T231)
U24_GAG(T211, T217, T213, lessM_out_ga(T211, T217)) → U25_GAG(T211, T217, T213, inA_in_ag(T217, T213))
U24_GAG(T211, T217, T213, lessM_out_ga(T211, T217)) → INA_IN_AG(T217, T213)
INA_IN_AG(0, tree(s(T253), T246, T247)) → U4_AG(T253, T246, T247, inB_in_g(T246))
INA_IN_AG(s(T268), tree(s(T267), T246, T247)) → U5_AG(T268, T267, T246, T247, pC_in_agg(T268, T267, T246))
INA_IN_AG(T286, tree(T283, T284, T285)) → U6_AG(T286, T283, T284, T285, pD_in_gag(T283, T286, T285))
INA_IN_AG(s(T303), tree(0, T295, T296)) → U7_AG(T303, T295, T296, inA_in_ag(s(T303), T296))
INA_IN_AG(s(T303), tree(0, T295, T296)) → INA_IN_AG(s(T303), T296)
INA_IN_AG(s(T316), tree(s(T314), T295, T296)) → U8_AG(T316, T314, T295, T296, pE_in_gag(T314, T316, T296))
INA_IN_AG(s(T316), tree(s(T314), T295, T296)) → PE_IN_GAG(T314, T316, T296)
PE_IN_GAG(T314, T319, T296) → U26_GAG(T314, T319, T296, lessM_in_ga(T314, T319))
PE_IN_GAG(T314, T319, T296) → LESSM_IN_GA(T314, T319)
U26_GAG(T314, T319, T296, lessM_out_ga(T314, T319)) → U27_GAG(T314, T319, T296, inA_in_ag(s(T319), T296))
U26_GAG(T314, T319, T296, lessM_out_ga(T314, T319)) → INA_IN_AG(s(T319), T296)

The TRS R consists of the following rules:

inA_in_ag(T6, tree(T6, T7, T8)) → inA_out_ag(T6, tree(T6, T7, T8))
inA_in_ag(0, tree(s(T22), T15, T16)) → U1_ag(T22, T15, T16, inB_in_g(T15))
inB_in_g(tree(0, T35, T36)) → inB_out_g(tree(0, T35, T36))
inB_in_g(tree(T49, T50, T51)) → U9_g(T49, T50, T51, pF_in_gg(T49, T50))
pF_in_gg(T49, T50) → U16_gg(T49, T50, lessN_in_g(T49))
lessN_in_g(s(T60)) → lessN_out_g(s(T60))
U16_gg(T49, T50, lessN_out_g(T49)) → U17_gg(T49, T50, inB_in_g(T50))
U17_gg(T49, T50, inB_out_g(T50)) → pF_out_gg(T49, T50)
U9_g(T49, T50, T51, pF_out_gg(T49, T50)) → inB_out_g(tree(T49, T50, T51))
U1_ag(T22, T15, T16, inB_out_g(T15)) → inA_out_ag(0, tree(s(T22), T15, T16))
inA_in_ag(s(T89), tree(s(T88), T15, T16)) → U2_ag(T89, T88, T15, T16, pC_in_agg(T89, T88, T15))
pC_in_agg(T92, T88, T15) → U18_agg(T92, T88, T15, lessH_in_ag(T92, T88))
lessH_in_ag(0, s(T99)) → lessH_out_ag(0, s(T99))
lessH_in_ag(s(T106), s(T105)) → U10_ag(T106, T105, lessH_in_ag(T106, T105))
U10_ag(T106, T105, lessH_out_ag(T106, T105)) → lessH_out_ag(s(T106), s(T105))
U18_agg(T92, T88, T15, lessH_out_ag(T92, T88)) → U19_agg(T92, T88, T15, inI_in_gg(T92, T15))
inI_in_gg(T127, tree(s(T127), T128, T129)) → inI_out_gg(T127, tree(s(T127), T128, T129))
inI_in_gg(T146, tree(T147, T148, T149)) → U11_gg(T146, T147, T148, T149, pJ_in_ggg(T146, T147, T148))
pJ_in_ggg(T146, T147, T148) → U20_ggg(T146, T147, T148, lessO_in_gg(T146, T147))
lessO_in_gg(T154, s(T155)) → U15_gg(T154, T155, lessL_in_gg(T154, T155))
lessL_in_gg(0, s(T162)) → lessL_out_gg(0, s(T162))
lessL_in_gg(s(T167), s(T168)) → U13_gg(T167, T168, lessL_in_gg(T167, T168))
U13_gg(T167, T168, lessL_out_gg(T167, T168)) → lessL_out_gg(s(T167), s(T168))
U15_gg(T154, T155, lessL_out_gg(T154, T155)) → lessO_out_gg(T154, s(T155))
U20_ggg(T146, T147, T148, lessO_out_gg(T146, T147)) → U21_ggg(T146, T147, T148, inI_in_gg(T146, T148))
inI_in_gg(T185, tree(T186, T187, T188)) → U12_gg(T185, T186, T187, T188, pK_in_ggg(T186, T185, T188))
pK_in_ggg(T186, T185, T188) → U22_ggg(T186, T185, T188, lessL_in_gg(T186, s(T185)))
U22_ggg(T186, T185, T188, lessL_out_gg(T186, s(T185))) → U23_ggg(T186, T185, T188, inI_in_gg(T185, T188))
U23_ggg(T186, T185, T188, inI_out_gg(T185, T188)) → pK_out_ggg(T186, T185, T188)
U12_gg(T185, T186, T187, T188, pK_out_ggg(T186, T185, T188)) → inI_out_gg(T185, tree(T186, T187, T188))
U21_ggg(T146, T147, T148, inI_out_gg(T146, T148)) → pJ_out_ggg(T146, T147, T148)
U11_gg(T146, T147, T148, T149, pJ_out_ggg(T146, T147, T148)) → inI_out_gg(T146, tree(T147, T148, T149))
U19_agg(T92, T88, T15, inI_out_gg(T92, T15)) → pC_out_agg(T92, T88, T15)
U2_ag(T89, T88, T15, T16, pC_out_agg(T89, T88, T15)) → inA_out_ag(s(T89), tree(s(T88), T15, T16))
inA_in_ag(T214, tree(T211, T212, T213)) → U3_ag(T214, T211, T212, T213, pD_in_gag(T211, T214, T213))
pD_in_gag(T211, T217, T213) → U24_gag(T211, T217, T213, lessM_in_ga(T211, T217))
lessM_in_ga(0, s(T224)) → lessM_out_ga(0, s(T224))
lessM_in_ga(s(T229), s(T231)) → U14_ga(T229, T231, lessM_in_ga(T229, T231))
U14_ga(T229, T231, lessM_out_ga(T229, T231)) → lessM_out_ga(s(T229), s(T231))
U24_gag(T211, T217, T213, lessM_out_ga(T211, T217)) → U25_gag(T211, T217, T213, inA_in_ag(T217, T213))
inA_in_ag(0, tree(s(T253), T246, T247)) → U4_ag(T253, T246, T247, inB_in_g(T246))
U4_ag(T253, T246, T247, inB_out_g(T246)) → inA_out_ag(0, tree(s(T253), T246, T247))
inA_in_ag(s(T268), tree(s(T267), T246, T247)) → U5_ag(T268, T267, T246, T247, pC_in_agg(T268, T267, T246))
U5_ag(T268, T267, T246, T247, pC_out_agg(T268, T267, T246)) → inA_out_ag(s(T268), tree(s(T267), T246, T247))
inA_in_ag(T286, tree(T283, T284, T285)) → U6_ag(T286, T283, T284, T285, pD_in_gag(T283, T286, T285))
U6_ag(T286, T283, T284, T285, pD_out_gag(T283, T286, T285)) → inA_out_ag(T286, tree(T283, T284, T285))
inA_in_ag(s(T303), tree(0, T295, T296)) → U7_ag(T303, T295, T296, inA_in_ag(s(T303), T296))
inA_in_ag(s(T316), tree(s(T314), T295, T296)) → U8_ag(T316, T314, T295, T296, pE_in_gag(T314, T316, T296))
pE_in_gag(T314, T319, T296) → U26_gag(T314, T319, T296, lessM_in_ga(T314, T319))
U26_gag(T314, T319, T296, lessM_out_ga(T314, T319)) → U27_gag(T314, T319, T296, inA_in_ag(s(T319), T296))
U27_gag(T314, T319, T296, inA_out_ag(s(T319), T296)) → pE_out_gag(T314, T319, T296)
U8_ag(T316, T314, T295, T296, pE_out_gag(T314, T316, T296)) → inA_out_ag(s(T316), tree(s(T314), T295, T296))
U7_ag(T303, T295, T296, inA_out_ag(s(T303), T296)) → inA_out_ag(s(T303), tree(0, T295, T296))
U25_gag(T211, T217, T213, inA_out_ag(T217, T213)) → pD_out_gag(T211, T217, T213)
U3_ag(T214, T211, T212, T213, pD_out_gag(T211, T214, T213)) → inA_out_ag(T214, tree(T211, T212, T213))

The argument filtering Pi contains the following mapping:
inA_in_ag(x1, x2)  =  inA_in_ag(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
inA_out_ag(x1, x2)  =  inA_out_ag(x1, x2)
s(x1)  =  s(x1)
U1_ag(x1, x2, x3, x4)  =  U1_ag(x1, x2, x3, x4)
inB_in_g(x1)  =  inB_in_g(x1)
0  =  0
inB_out_g(x1)  =  inB_out_g(x1)
U9_g(x1, x2, x3, x4)  =  U9_g(x1, x2, x3, x4)
pF_in_gg(x1, x2)  =  pF_in_gg(x1, x2)
U16_gg(x1, x2, x3)  =  U16_gg(x1, x2, x3)
lessN_in_g(x1)  =  lessN_in_g(x1)
lessN_out_g(x1)  =  lessN_out_g(x1)
U17_gg(x1, x2, x3)  =  U17_gg(x1, x2, x3)
pF_out_gg(x1, x2)  =  pF_out_gg(x1, x2)
U2_ag(x1, x2, x3, x4, x5)  =  U2_ag(x2, x3, x4, x5)
pC_in_agg(x1, x2, x3)  =  pC_in_agg(x2, x3)
U18_agg(x1, x2, x3, x4)  =  U18_agg(x2, x3, x4)
lessH_in_ag(x1, x2)  =  lessH_in_ag(x2)
lessH_out_ag(x1, x2)  =  lessH_out_ag(x1, x2)
U10_ag(x1, x2, x3)  =  U10_ag(x2, x3)
U19_agg(x1, x2, x3, x4)  =  U19_agg(x1, x2, x3, x4)
inI_in_gg(x1, x2)  =  inI_in_gg(x1, x2)
inI_out_gg(x1, x2)  =  inI_out_gg(x1, x2)
U11_gg(x1, x2, x3, x4, x5)  =  U11_gg(x1, x2, x3, x4, x5)
pJ_in_ggg(x1, x2, x3)  =  pJ_in_ggg(x1, x2, x3)
U20_ggg(x1, x2, x3, x4)  =  U20_ggg(x1, x2, x3, x4)
lessO_in_gg(x1, x2)  =  lessO_in_gg(x1, x2)
U15_gg(x1, x2, x3)  =  U15_gg(x1, x2, x3)
lessL_in_gg(x1, x2)  =  lessL_in_gg(x1, x2)
lessL_out_gg(x1, x2)  =  lessL_out_gg(x1, x2)
U13_gg(x1, x2, x3)  =  U13_gg(x1, x2, x3)
lessO_out_gg(x1, x2)  =  lessO_out_gg(x1, x2)
U21_ggg(x1, x2, x3, x4)  =  U21_ggg(x1, x2, x3, x4)
U12_gg(x1, x2, x3, x4, x5)  =  U12_gg(x1, x2, x3, x4, x5)
pK_in_ggg(x1, x2, x3)  =  pK_in_ggg(x1, x2, x3)
U22_ggg(x1, x2, x3, x4)  =  U22_ggg(x1, x2, x3, x4)
U23_ggg(x1, x2, x3, x4)  =  U23_ggg(x1, x2, x3, x4)
pK_out_ggg(x1, x2, x3)  =  pK_out_ggg(x1, x2, x3)
pJ_out_ggg(x1, x2, x3)  =  pJ_out_ggg(x1, x2, x3)
pC_out_agg(x1, x2, x3)  =  pC_out_agg(x1, x2, x3)
U3_ag(x1, x2, x3, x4, x5)  =  U3_ag(x2, x3, x4, x5)
pD_in_gag(x1, x2, x3)  =  pD_in_gag(x1, x3)
U24_gag(x1, x2, x3, x4)  =  U24_gag(x1, x3, x4)
lessM_in_ga(x1, x2)  =  lessM_in_ga(x1)
lessM_out_ga(x1, x2)  =  lessM_out_ga(x1)
U14_ga(x1, x2, x3)  =  U14_ga(x1, x3)
U25_gag(x1, x2, x3, x4)  =  U25_gag(x1, x3, x4)
U4_ag(x1, x2, x3, x4)  =  U4_ag(x1, x2, x3, x4)
U5_ag(x1, x2, x3, x4, x5)  =  U5_ag(x2, x3, x4, x5)
U6_ag(x1, x2, x3, x4, x5)  =  U6_ag(x2, x3, x4, x5)
pD_out_gag(x1, x2, x3)  =  pD_out_gag(x1, x2, x3)
U7_ag(x1, x2, x3, x4)  =  U7_ag(x2, x3, x4)
U8_ag(x1, x2, x3, x4, x5)  =  U8_ag(x2, x3, x4, x5)
pE_in_gag(x1, x2, x3)  =  pE_in_gag(x1, x3)
U26_gag(x1, x2, x3, x4)  =  U26_gag(x1, x3, x4)
U27_gag(x1, x2, x3, x4)  =  U27_gag(x1, x3, x4)
pE_out_gag(x1, x2, x3)  =  pE_out_gag(x1, x2, x3)
INA_IN_AG(x1, x2)  =  INA_IN_AG(x2)
U1_AG(x1, x2, x3, x4)  =  U1_AG(x1, x2, x3, x4)
INB_IN_G(x1)  =  INB_IN_G(x1)
U9_G(x1, x2, x3, x4)  =  U9_G(x1, x2, x3, x4)
PF_IN_GG(x1, x2)  =  PF_IN_GG(x1, x2)
U16_GG(x1, x2, x3)  =  U16_GG(x1, x2, x3)
LESSN_IN_G(x1)  =  LESSN_IN_G(x1)
U17_GG(x1, x2, x3)  =  U17_GG(x1, x2, x3)
U2_AG(x1, x2, x3, x4, x5)  =  U2_AG(x2, x3, x4, x5)
PC_IN_AGG(x1, x2, x3)  =  PC_IN_AGG(x2, x3)
U18_AGG(x1, x2, x3, x4)  =  U18_AGG(x2, x3, x4)
LESSH_IN_AG(x1, x2)  =  LESSH_IN_AG(x2)
U10_AG(x1, x2, x3)  =  U10_AG(x2, x3)
U19_AGG(x1, x2, x3, x4)  =  U19_AGG(x1, x2, x3, x4)
INI_IN_GG(x1, x2)  =  INI_IN_GG(x1, x2)
U11_GG(x1, x2, x3, x4, x5)  =  U11_GG(x1, x2, x3, x4, x5)
PJ_IN_GGG(x1, x2, x3)  =  PJ_IN_GGG(x1, x2, x3)
U20_GGG(x1, x2, x3, x4)  =  U20_GGG(x1, x2, x3, x4)
LESSO_IN_GG(x1, x2)  =  LESSO_IN_GG(x1, x2)
U15_GG(x1, x2, x3)  =  U15_GG(x1, x2, x3)
LESSL_IN_GG(x1, x2)  =  LESSL_IN_GG(x1, x2)
U13_GG(x1, x2, x3)  =  U13_GG(x1, x2, x3)
U21_GGG(x1, x2, x3, x4)  =  U21_GGG(x1, x2, x3, x4)
U12_GG(x1, x2, x3, x4, x5)  =  U12_GG(x1, x2, x3, x4, x5)
PK_IN_GGG(x1, x2, x3)  =  PK_IN_GGG(x1, x2, x3)
U22_GGG(x1, x2, x3, x4)  =  U22_GGG(x1, x2, x3, x4)
U23_GGG(x1, x2, x3, x4)  =  U23_GGG(x1, x2, x3, x4)
U3_AG(x1, x2, x3, x4, x5)  =  U3_AG(x2, x3, x4, x5)
PD_IN_GAG(x1, x2, x3)  =  PD_IN_GAG(x1, x3)
U24_GAG(x1, x2, x3, x4)  =  U24_GAG(x1, x3, x4)
LESSM_IN_GA(x1, x2)  =  LESSM_IN_GA(x1)
U14_GA(x1, x2, x3)  =  U14_GA(x1, x3)
U25_GAG(x1, x2, x3, x4)  =  U25_GAG(x1, x3, x4)
U4_AG(x1, x2, x3, x4)  =  U4_AG(x1, x2, x3, x4)
U5_AG(x1, x2, x3, x4, x5)  =  U5_AG(x2, x3, x4, x5)
U6_AG(x1, x2, x3, x4, x5)  =  U6_AG(x2, x3, x4, x5)
U7_AG(x1, x2, x3, x4)  =  U7_AG(x2, x3, x4)
U8_AG(x1, x2, x3, x4, x5)  =  U8_AG(x2, x3, x4, x5)
PE_IN_GAG(x1, x2, x3)  =  PE_IN_GAG(x1, x3)
U26_GAG(x1, x2, x3, x4)  =  U26_GAG(x1, x3, x4)
U27_GAG(x1, x2, x3, x4)  =  U27_GAG(x1, x3, x4)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 6 SCCs with 32 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

LESSM_IN_GA(s(T229), s(T231)) → LESSM_IN_GA(T229, T231)

The TRS R consists of the following rules:

inA_in_ag(T6, tree(T6, T7, T8)) → inA_out_ag(T6, tree(T6, T7, T8))
inA_in_ag(0, tree(s(T22), T15, T16)) → U1_ag(T22, T15, T16, inB_in_g(T15))
inB_in_g(tree(0, T35, T36)) → inB_out_g(tree(0, T35, T36))
inB_in_g(tree(T49, T50, T51)) → U9_g(T49, T50, T51, pF_in_gg(T49, T50))
pF_in_gg(T49, T50) → U16_gg(T49, T50, lessN_in_g(T49))
lessN_in_g(s(T60)) → lessN_out_g(s(T60))
U16_gg(T49, T50, lessN_out_g(T49)) → U17_gg(T49, T50, inB_in_g(T50))
U17_gg(T49, T50, inB_out_g(T50)) → pF_out_gg(T49, T50)
U9_g(T49, T50, T51, pF_out_gg(T49, T50)) → inB_out_g(tree(T49, T50, T51))
U1_ag(T22, T15, T16, inB_out_g(T15)) → inA_out_ag(0, tree(s(T22), T15, T16))
inA_in_ag(s(T89), tree(s(T88), T15, T16)) → U2_ag(T89, T88, T15, T16, pC_in_agg(T89, T88, T15))
pC_in_agg(T92, T88, T15) → U18_agg(T92, T88, T15, lessH_in_ag(T92, T88))
lessH_in_ag(0, s(T99)) → lessH_out_ag(0, s(T99))
lessH_in_ag(s(T106), s(T105)) → U10_ag(T106, T105, lessH_in_ag(T106, T105))
U10_ag(T106, T105, lessH_out_ag(T106, T105)) → lessH_out_ag(s(T106), s(T105))
U18_agg(T92, T88, T15, lessH_out_ag(T92, T88)) → U19_agg(T92, T88, T15, inI_in_gg(T92, T15))
inI_in_gg(T127, tree(s(T127), T128, T129)) → inI_out_gg(T127, tree(s(T127), T128, T129))
inI_in_gg(T146, tree(T147, T148, T149)) → U11_gg(T146, T147, T148, T149, pJ_in_ggg(T146, T147, T148))
pJ_in_ggg(T146, T147, T148) → U20_ggg(T146, T147, T148, lessO_in_gg(T146, T147))
lessO_in_gg(T154, s(T155)) → U15_gg(T154, T155, lessL_in_gg(T154, T155))
lessL_in_gg(0, s(T162)) → lessL_out_gg(0, s(T162))
lessL_in_gg(s(T167), s(T168)) → U13_gg(T167, T168, lessL_in_gg(T167, T168))
U13_gg(T167, T168, lessL_out_gg(T167, T168)) → lessL_out_gg(s(T167), s(T168))
U15_gg(T154, T155, lessL_out_gg(T154, T155)) → lessO_out_gg(T154, s(T155))
U20_ggg(T146, T147, T148, lessO_out_gg(T146, T147)) → U21_ggg(T146, T147, T148, inI_in_gg(T146, T148))
inI_in_gg(T185, tree(T186, T187, T188)) → U12_gg(T185, T186, T187, T188, pK_in_ggg(T186, T185, T188))
pK_in_ggg(T186, T185, T188) → U22_ggg(T186, T185, T188, lessL_in_gg(T186, s(T185)))
U22_ggg(T186, T185, T188, lessL_out_gg(T186, s(T185))) → U23_ggg(T186, T185, T188, inI_in_gg(T185, T188))
U23_ggg(T186, T185, T188, inI_out_gg(T185, T188)) → pK_out_ggg(T186, T185, T188)
U12_gg(T185, T186, T187, T188, pK_out_ggg(T186, T185, T188)) → inI_out_gg(T185, tree(T186, T187, T188))
U21_ggg(T146, T147, T148, inI_out_gg(T146, T148)) → pJ_out_ggg(T146, T147, T148)
U11_gg(T146, T147, T148, T149, pJ_out_ggg(T146, T147, T148)) → inI_out_gg(T146, tree(T147, T148, T149))
U19_agg(T92, T88, T15, inI_out_gg(T92, T15)) → pC_out_agg(T92, T88, T15)
U2_ag(T89, T88, T15, T16, pC_out_agg(T89, T88, T15)) → inA_out_ag(s(T89), tree(s(T88), T15, T16))
inA_in_ag(T214, tree(T211, T212, T213)) → U3_ag(T214, T211, T212, T213, pD_in_gag(T211, T214, T213))
pD_in_gag(T211, T217, T213) → U24_gag(T211, T217, T213, lessM_in_ga(T211, T217))
lessM_in_ga(0, s(T224)) → lessM_out_ga(0, s(T224))
lessM_in_ga(s(T229), s(T231)) → U14_ga(T229, T231, lessM_in_ga(T229, T231))
U14_ga(T229, T231, lessM_out_ga(T229, T231)) → lessM_out_ga(s(T229), s(T231))
U24_gag(T211, T217, T213, lessM_out_ga(T211, T217)) → U25_gag(T211, T217, T213, inA_in_ag(T217, T213))
inA_in_ag(0, tree(s(T253), T246, T247)) → U4_ag(T253, T246, T247, inB_in_g(T246))
U4_ag(T253, T246, T247, inB_out_g(T246)) → inA_out_ag(0, tree(s(T253), T246, T247))
inA_in_ag(s(T268), tree(s(T267), T246, T247)) → U5_ag(T268, T267, T246, T247, pC_in_agg(T268, T267, T246))
U5_ag(T268, T267, T246, T247, pC_out_agg(T268, T267, T246)) → inA_out_ag(s(T268), tree(s(T267), T246, T247))
inA_in_ag(T286, tree(T283, T284, T285)) → U6_ag(T286, T283, T284, T285, pD_in_gag(T283, T286, T285))
U6_ag(T286, T283, T284, T285, pD_out_gag(T283, T286, T285)) → inA_out_ag(T286, tree(T283, T284, T285))
inA_in_ag(s(T303), tree(0, T295, T296)) → U7_ag(T303, T295, T296, inA_in_ag(s(T303), T296))
inA_in_ag(s(T316), tree(s(T314), T295, T296)) → U8_ag(T316, T314, T295, T296, pE_in_gag(T314, T316, T296))
pE_in_gag(T314, T319, T296) → U26_gag(T314, T319, T296, lessM_in_ga(T314, T319))
U26_gag(T314, T319, T296, lessM_out_ga(T314, T319)) → U27_gag(T314, T319, T296, inA_in_ag(s(T319), T296))
U27_gag(T314, T319, T296, inA_out_ag(s(T319), T296)) → pE_out_gag(T314, T319, T296)
U8_ag(T316, T314, T295, T296, pE_out_gag(T314, T316, T296)) → inA_out_ag(s(T316), tree(s(T314), T295, T296))
U7_ag(T303, T295, T296, inA_out_ag(s(T303), T296)) → inA_out_ag(s(T303), tree(0, T295, T296))
U25_gag(T211, T217, T213, inA_out_ag(T217, T213)) → pD_out_gag(T211, T217, T213)
U3_ag(T214, T211, T212, T213, pD_out_gag(T211, T214, T213)) → inA_out_ag(T214, tree(T211, T212, T213))

The argument filtering Pi contains the following mapping:
inA_in_ag(x1, x2)  =  inA_in_ag(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
inA_out_ag(x1, x2)  =  inA_out_ag(x1, x2)
s(x1)  =  s(x1)
U1_ag(x1, x2, x3, x4)  =  U1_ag(x1, x2, x3, x4)
inB_in_g(x1)  =  inB_in_g(x1)
0  =  0
inB_out_g(x1)  =  inB_out_g(x1)
U9_g(x1, x2, x3, x4)  =  U9_g(x1, x2, x3, x4)
pF_in_gg(x1, x2)  =  pF_in_gg(x1, x2)
U16_gg(x1, x2, x3)  =  U16_gg(x1, x2, x3)
lessN_in_g(x1)  =  lessN_in_g(x1)
lessN_out_g(x1)  =  lessN_out_g(x1)
U17_gg(x1, x2, x3)  =  U17_gg(x1, x2, x3)
pF_out_gg(x1, x2)  =  pF_out_gg(x1, x2)
U2_ag(x1, x2, x3, x4, x5)  =  U2_ag(x2, x3, x4, x5)
pC_in_agg(x1, x2, x3)  =  pC_in_agg(x2, x3)
U18_agg(x1, x2, x3, x4)  =  U18_agg(x2, x3, x4)
lessH_in_ag(x1, x2)  =  lessH_in_ag(x2)
lessH_out_ag(x1, x2)  =  lessH_out_ag(x1, x2)
U10_ag(x1, x2, x3)  =  U10_ag(x2, x3)
U19_agg(x1, x2, x3, x4)  =  U19_agg(x1, x2, x3, x4)
inI_in_gg(x1, x2)  =  inI_in_gg(x1, x2)
inI_out_gg(x1, x2)  =  inI_out_gg(x1, x2)
U11_gg(x1, x2, x3, x4, x5)  =  U11_gg(x1, x2, x3, x4, x5)
pJ_in_ggg(x1, x2, x3)  =  pJ_in_ggg(x1, x2, x3)
U20_ggg(x1, x2, x3, x4)  =  U20_ggg(x1, x2, x3, x4)
lessO_in_gg(x1, x2)  =  lessO_in_gg(x1, x2)
U15_gg(x1, x2, x3)  =  U15_gg(x1, x2, x3)
lessL_in_gg(x1, x2)  =  lessL_in_gg(x1, x2)
lessL_out_gg(x1, x2)  =  lessL_out_gg(x1, x2)
U13_gg(x1, x2, x3)  =  U13_gg(x1, x2, x3)
lessO_out_gg(x1, x2)  =  lessO_out_gg(x1, x2)
U21_ggg(x1, x2, x3, x4)  =  U21_ggg(x1, x2, x3, x4)
U12_gg(x1, x2, x3, x4, x5)  =  U12_gg(x1, x2, x3, x4, x5)
pK_in_ggg(x1, x2, x3)  =  pK_in_ggg(x1, x2, x3)
U22_ggg(x1, x2, x3, x4)  =  U22_ggg(x1, x2, x3, x4)
U23_ggg(x1, x2, x3, x4)  =  U23_ggg(x1, x2, x3, x4)
pK_out_ggg(x1, x2, x3)  =  pK_out_ggg(x1, x2, x3)
pJ_out_ggg(x1, x2, x3)  =  pJ_out_ggg(x1, x2, x3)
pC_out_agg(x1, x2, x3)  =  pC_out_agg(x1, x2, x3)
U3_ag(x1, x2, x3, x4, x5)  =  U3_ag(x2, x3, x4, x5)
pD_in_gag(x1, x2, x3)  =  pD_in_gag(x1, x3)
U24_gag(x1, x2, x3, x4)  =  U24_gag(x1, x3, x4)
lessM_in_ga(x1, x2)  =  lessM_in_ga(x1)
lessM_out_ga(x1, x2)  =  lessM_out_ga(x1)
U14_ga(x1, x2, x3)  =  U14_ga(x1, x3)
U25_gag(x1, x2, x3, x4)  =  U25_gag(x1, x3, x4)
U4_ag(x1, x2, x3, x4)  =  U4_ag(x1, x2, x3, x4)
U5_ag(x1, x2, x3, x4, x5)  =  U5_ag(x2, x3, x4, x5)
U6_ag(x1, x2, x3, x4, x5)  =  U6_ag(x2, x3, x4, x5)
pD_out_gag(x1, x2, x3)  =  pD_out_gag(x1, x2, x3)
U7_ag(x1, x2, x3, x4)  =  U7_ag(x2, x3, x4)
U8_ag(x1, x2, x3, x4, x5)  =  U8_ag(x2, x3, x4, x5)
pE_in_gag(x1, x2, x3)  =  pE_in_gag(x1, x3)
U26_gag(x1, x2, x3, x4)  =  U26_gag(x1, x3, x4)
U27_gag(x1, x2, x3, x4)  =  U27_gag(x1, x3, x4)
pE_out_gag(x1, x2, x3)  =  pE_out_gag(x1, x2, x3)
LESSM_IN_GA(x1, x2)  =  LESSM_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:

LESSM_IN_GA(s(T229), s(T231)) → LESSM_IN_GA(T229, T231)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
LESSM_IN_GA(x1, x2)  =  LESSM_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:

LESSM_IN_GA(s(T229)) → LESSM_IN_GA(T229)

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:

• LESSM_IN_GA(s(T229)) → LESSM_IN_GA(T229)
  The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

LESSL_IN_GG(s(T167), s(T168)) → LESSL_IN_GG(T167, T168)

The TRS R consists of the following rules:

inA_in_ag(T6, tree(T6, T7, T8)) → inA_out_ag(T6, tree(T6, T7, T8))
inA_in_ag(0, tree(s(T22), T15, T16)) → U1_ag(T22, T15, T16, inB_in_g(T15))
inB_in_g(tree(0, T35, T36)) → inB_out_g(tree(0, T35, T36))
inB_in_g(tree(T49, T50, T51)) → U9_g(T49, T50, T51, pF_in_gg(T49, T50))
pF_in_gg(T49, T50) → U16_gg(T49, T50, lessN_in_g(T49))
lessN_in_g(s(T60)) → lessN_out_g(s(T60))
U16_gg(T49, T50, lessN_out_g(T49)) → U17_gg(T49, T50, inB_in_g(T50))
U17_gg(T49, T50, inB_out_g(T50)) → pF_out_gg(T49, T50)
U9_g(T49, T50, T51, pF_out_gg(T49, T50)) → inB_out_g(tree(T49, T50, T51))
U1_ag(T22, T15, T16, inB_out_g(T15)) → inA_out_ag(0, tree(s(T22), T15, T16))
inA_in_ag(s(T89), tree(s(T88), T15, T16)) → U2_ag(T89, T88, T15, T16, pC_in_agg(T89, T88, T15))
pC_in_agg(T92, T88, T15) → U18_agg(T92, T88, T15, lessH_in_ag(T92, T88))
lessH_in_ag(0, s(T99)) → lessH_out_ag(0, s(T99))
lessH_in_ag(s(T106), s(T105)) → U10_ag(T106, T105, lessH_in_ag(T106, T105))
U10_ag(T106, T105, lessH_out_ag(T106, T105)) → lessH_out_ag(s(T106), s(T105))
U18_agg(T92, T88, T15, lessH_out_ag(T92, T88)) → U19_agg(T92, T88, T15, inI_in_gg(T92, T15))
inI_in_gg(T127, tree(s(T127), T128, T129)) → inI_out_gg(T127, tree(s(T127), T128, T129))
inI_in_gg(T146, tree(T147, T148, T149)) → U11_gg(T146, T147, T148, T149, pJ_in_ggg(T146, T147, T148))
pJ_in_ggg(T146, T147, T148) → U20_ggg(T146, T147, T148, lessO_in_gg(T146, T147))
lessO_in_gg(T154, s(T155)) → U15_gg(T154, T155, lessL_in_gg(T154, T155))
lessL_in_gg(0, s(T162)) → lessL_out_gg(0, s(T162))
lessL_in_gg(s(T167), s(T168)) → U13_gg(T167, T168, lessL_in_gg(T167, T168))
U13_gg(T167, T168, lessL_out_gg(T167, T168)) → lessL_out_gg(s(T167), s(T168))
U15_gg(T154, T155, lessL_out_gg(T154, T155)) → lessO_out_gg(T154, s(T155))
U20_ggg(T146, T147, T148, lessO_out_gg(T146, T147)) → U21_ggg(T146, T147, T148, inI_in_gg(T146, T148))
inI_in_gg(T185, tree(T186, T187, T188)) → U12_gg(T185, T186, T187, T188, pK_in_ggg(T186, T185, T188))
pK_in_ggg(T186, T185, T188) → U22_ggg(T186, T185, T188, lessL_in_gg(T186, s(T185)))
U22_ggg(T186, T185, T188, lessL_out_gg(T186, s(T185))) → U23_ggg(T186, T185, T188, inI_in_gg(T185, T188))
U23_ggg(T186, T185, T188, inI_out_gg(T185, T188)) → pK_out_ggg(T186, T185, T188)
U12_gg(T185, T186, T187, T188, pK_out_ggg(T186, T185, T188)) → inI_out_gg(T185, tree(T186, T187, T188))
U21_ggg(T146, T147, T148, inI_out_gg(T146, T148)) → pJ_out_ggg(T146, T147, T148)
U11_gg(T146, T147, T148, T149, pJ_out_ggg(T146, T147, T148)) → inI_out_gg(T146, tree(T147, T148, T149))
U19_agg(T92, T88, T15, inI_out_gg(T92, T15)) → pC_out_agg(T92, T88, T15)
U2_ag(T89, T88, T15, T16, pC_out_agg(T89, T88, T15)) → inA_out_ag(s(T89), tree(s(T88), T15, T16))
inA_in_ag(T214, tree(T211, T212, T213)) → U3_ag(T214, T211, T212, T213, pD_in_gag(T211, T214, T213))
pD_in_gag(T211, T217, T213) → U24_gag(T211, T217, T213, lessM_in_ga(T211, T217))
lessM_in_ga(0, s(T224)) → lessM_out_ga(0, s(T224))
lessM_in_ga(s(T229), s(T231)) → U14_ga(T229, T231, lessM_in_ga(T229, T231))
U14_ga(T229, T231, lessM_out_ga(T229, T231)) → lessM_out_ga(s(T229), s(T231))
U24_gag(T211, T217, T213, lessM_out_ga(T211, T217)) → U25_gag(T211, T217, T213, inA_in_ag(T217, T213))
inA_in_ag(0, tree(s(T253), T246, T247)) → U4_ag(T253, T246, T247, inB_in_g(T246))
U4_ag(T253, T246, T247, inB_out_g(T246)) → inA_out_ag(0, tree(s(T253), T246, T247))
inA_in_ag(s(T268), tree(s(T267), T246, T247)) → U5_ag(T268, T267, T246, T247, pC_in_agg(T268, T267, T246))
U5_ag(T268, T267, T246, T247, pC_out_agg(T268, T267, T246)) → inA_out_ag(s(T268), tree(s(T267), T246, T247))
inA_in_ag(T286, tree(T283, T284, T285)) → U6_ag(T286, T283, T284, T285, pD_in_gag(T283, T286, T285))
U6_ag(T286, T283, T284, T285, pD_out_gag(T283, T286, T285)) → inA_out_ag(T286, tree(T283, T284, T285))
inA_in_ag(s(T303), tree(0, T295, T296)) → U7_ag(T303, T295, T296, inA_in_ag(s(T303), T296))
inA_in_ag(s(T316), tree(s(T314), T295, T296)) → U8_ag(T316, T314, T295, T296, pE_in_gag(T314, T316, T296))
pE_in_gag(T314, T319, T296) → U26_gag(T314, T319, T296, lessM_in_ga(T314, T319))
U26_gag(T314, T319, T296, lessM_out_ga(T314, T319)) → U27_gag(T314, T319, T296, inA_in_ag(s(T319), T296))
U27_gag(T314, T319, T296, inA_out_ag(s(T319), T296)) → pE_out_gag(T314, T319, T296)
U8_ag(T316, T314, T295, T296, pE_out_gag(T314, T316, T296)) → inA_out_ag(s(T316), tree(s(T314), T295, T296))
U7_ag(T303, T295, T296, inA_out_ag(s(T303), T296)) → inA_out_ag(s(T303), tree(0, T295, T296))
U25_gag(T211, T217, T213, inA_out_ag(T217, T213)) → pD_out_gag(T211, T217, T213)
U3_ag(T214, T211, T212, T213, pD_out_gag(T211, T214, T213)) → inA_out_ag(T214, tree(T211, T212, T213))

The argument filtering Pi contains the following mapping:
inA_in_ag(x1, x2)  =  inA_in_ag(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
inA_out_ag(x1, x2)  =  inA_out_ag(x1, x2)
s(x1)  =  s(x1)
U1_ag(x1, x2, x3, x4)  =  U1_ag(x1, x2, x3, x4)
inB_in_g(x1)  =  inB_in_g(x1)
0  =  0
inB_out_g(x1)  =  inB_out_g(x1)
U9_g(x1, x2, x3, x4)  =  U9_g(x1, x2, x3, x4)
pF_in_gg(x1, x2)  =  pF_in_gg(x1, x2)
U16_gg(x1, x2, x3)  =  U16_gg(x1, x2, x3)
lessN_in_g(x1)  =  lessN_in_g(x1)
lessN_out_g(x1)  =  lessN_out_g(x1)
U17_gg(x1, x2, x3)  =  U17_gg(x1, x2, x3)
pF_out_gg(x1, x2)  =  pF_out_gg(x1, x2)
U2_ag(x1, x2, x3, x4, x5)  =  U2_ag(x2, x3, x4, x5)
pC_in_agg(x1, x2, x3)  =  pC_in_agg(x2, x3)
U18_agg(x1, x2, x3, x4)  =  U18_agg(x2, x3, x4)
lessH_in_ag(x1, x2)  =  lessH_in_ag(x2)
lessH_out_ag(x1, x2)  =  lessH_out_ag(x1, x2)
U10_ag(x1, x2, x3)  =  U10_ag(x2, x3)
U19_agg(x1, x2, x3, x4)  =  U19_agg(x1, x2, x3, x4)
inI_in_gg(x1, x2)  =  inI_in_gg(x1, x2)
inI_out_gg(x1, x2)  =  inI_out_gg(x1, x2)
U11_gg(x1, x2, x3, x4, x5)  =  U11_gg(x1, x2, x3, x4, x5)
pJ_in_ggg(x1, x2, x3)  =  pJ_in_ggg(x1, x2, x3)
U20_ggg(x1, x2, x3, x4)  =  U20_ggg(x1, x2, x3, x4)
lessO_in_gg(x1, x2)  =  lessO_in_gg(x1, x2)
U15_gg(x1, x2, x3)  =  U15_gg(x1, x2, x3)
lessL_in_gg(x1, x2)  =  lessL_in_gg(x1, x2)
lessL_out_gg(x1, x2)  =  lessL_out_gg(x1, x2)
U13_gg(x1, x2, x3)  =  U13_gg(x1, x2, x3)
lessO_out_gg(x1, x2)  =  lessO_out_gg(x1, x2)
U21_ggg(x1, x2, x3, x4)  =  U21_ggg(x1, x2, x3, x4)
U12_gg(x1, x2, x3, x4, x5)  =  U12_gg(x1, x2, x3, x4, x5)
pK_in_ggg(x1, x2, x3)  =  pK_in_ggg(x1, x2, x3)
U22_ggg(x1, x2, x3, x4)  =  U22_ggg(x1, x2, x3, x4)
U23_ggg(x1, x2, x3, x4)  =  U23_ggg(x1, x2, x3, x4)
pK_out_ggg(x1, x2, x3)  =  pK_out_ggg(x1, x2, x3)
pJ_out_ggg(x1, x2, x3)  =  pJ_out_ggg(x1, x2, x3)
pC_out_agg(x1, x2, x3)  =  pC_out_agg(x1, x2, x3)
U3_ag(x1, x2, x3, x4, x5)  =  U3_ag(x2, x3, x4, x5)
pD_in_gag(x1, x2, x3)  =  pD_in_gag(x1, x3)
U24_gag(x1, x2, x3, x4)  =  U24_gag(x1, x3, x4)
lessM_in_ga(x1, x2)  =  lessM_in_ga(x1)
lessM_out_ga(x1, x2)  =  lessM_out_ga(x1)
U14_ga(x1, x2, x3)  =  U14_ga(x1, x3)
U25_gag(x1, x2, x3, x4)  =  U25_gag(x1, x3, x4)
U4_ag(x1, x2, x3, x4)  =  U4_ag(x1, x2, x3, x4)
U5_ag(x1, x2, x3, x4, x5)  =  U5_ag(x2, x3, x4, x5)
U6_ag(x1, x2, x3, x4, x5)  =  U6_ag(x2, x3, x4, x5)
pD_out_gag(x1, x2, x3)  =  pD_out_gag(x1, x2, x3)
U7_ag(x1, x2, x3, x4)  =  U7_ag(x2, x3, x4)
U8_ag(x1, x2, x3, x4, x5)  =  U8_ag(x2, x3, x4, x5)
pE_in_gag(x1, x2, x3)  =  pE_in_gag(x1, x3)
U26_gag(x1, x2, x3, x4)  =  U26_gag(x1, x3, x4)
U27_gag(x1, x2, x3, x4)  =  U27_gag(x1, x3, x4)
pE_out_gag(x1, x2, x3)  =  pE_out_gag(x1, x2, x3)
LESSL_IN_GG(x1, x2)  =  LESSL_IN_GG(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:

LESSL_IN_GG(s(T167), s(T168)) → LESSL_IN_GG(T167, T168)

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

(17) PiDPToQDPProof (EQUIVALENT 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:

LESSL_IN_GG(s(T167), s(T168)) → LESSL_IN_GG(T167, T168)

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

• LESSL_IN_GG(s(T167), s(T168)) → LESSL_IN_GG(T167, T168)
  The graph contains the following edges 1 > 1, 2 > 2

(20) YES

(21) Obligation:

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

INI_IN_GG(T146, tree(T147, T148, T149)) → PJ_IN_GGG(T146, T147, T148)
PJ_IN_GGG(T146, T147, T148) → U20_GGG(T146, T147, T148, lessO_in_gg(T146, T147))
U20_GGG(T146, T147, T148, lessO_out_gg(T146, T147)) → INI_IN_GG(T146, T148)
INI_IN_GG(T185, tree(T186, T187, T188)) → PK_IN_GGG(T186, T185, T188)
PK_IN_GGG(T186, T185, T188) → U22_GGG(T186, T185, T188, lessL_in_gg(T186, s(T185)))
U22_GGG(T186, T185, T188, lessL_out_gg(T186, s(T185))) → INI_IN_GG(T185, T188)

The TRS R consists of the following rules:

inA_in_ag(T6, tree(T6, T7, T8)) → inA_out_ag(T6, tree(T6, T7, T8))
inA_in_ag(0, tree(s(T22), T15, T16)) → U1_ag(T22, T15, T16, inB_in_g(T15))
inB_in_g(tree(0, T35, T36)) → inB_out_g(tree(0, T35, T36))
inB_in_g(tree(T49, T50, T51)) → U9_g(T49, T50, T51, pF_in_gg(T49, T50))
pF_in_gg(T49, T50) → U16_gg(T49, T50, lessN_in_g(T49))
lessN_in_g(s(T60)) → lessN_out_g(s(T60))
U16_gg(T49, T50, lessN_out_g(T49)) → U17_gg(T49, T50, inB_in_g(T50))
U17_gg(T49, T50, inB_out_g(T50)) → pF_out_gg(T49, T50)
U9_g(T49, T50, T51, pF_out_gg(T49, T50)) → inB_out_g(tree(T49, T50, T51))
U1_ag(T22, T15, T16, inB_out_g(T15)) → inA_out_ag(0, tree(s(T22), T15, T16))
inA_in_ag(s(T89), tree(s(T88), T15, T16)) → U2_ag(T89, T88, T15, T16, pC_in_agg(T89, T88, T15))
pC_in_agg(T92, T88, T15) → U18_agg(T92, T88, T15, lessH_in_ag(T92, T88))
lessH_in_ag(0, s(T99)) → lessH_out_ag(0, s(T99))
lessH_in_ag(s(T106), s(T105)) → U10_ag(T106, T105, lessH_in_ag(T106, T105))
U10_ag(T106, T105, lessH_out_ag(T106, T105)) → lessH_out_ag(s(T106), s(T105))
U18_agg(T92, T88, T15, lessH_out_ag(T92, T88)) → U19_agg(T92, T88, T15, inI_in_gg(T92, T15))
inI_in_gg(T127, tree(s(T127), T128, T129)) → inI_out_gg(T127, tree(s(T127), T128, T129))
inI_in_gg(T146, tree(T147, T148, T149)) → U11_gg(T146, T147, T148, T149, pJ_in_ggg(T146, T147, T148))
pJ_in_ggg(T146, T147, T148) → U20_ggg(T146, T147, T148, lessO_in_gg(T146, T147))
lessO_in_gg(T154, s(T155)) → U15_gg(T154, T155, lessL_in_gg(T154, T155))
lessL_in_gg(0, s(T162)) → lessL_out_gg(0, s(T162))
lessL_in_gg(s(T167), s(T168)) → U13_gg(T167, T168, lessL_in_gg(T167, T168))
U13_gg(T167, T168, lessL_out_gg(T167, T168)) → lessL_out_gg(s(T167), s(T168))
U15_gg(T154, T155, lessL_out_gg(T154, T155)) → lessO_out_gg(T154, s(T155))
U20_ggg(T146, T147, T148, lessO_out_gg(T146, T147)) → U21_ggg(T146, T147, T148, inI_in_gg(T146, T148))
inI_in_gg(T185, tree(T186, T187, T188)) → U12_gg(T185, T186, T187, T188, pK_in_ggg(T186, T185, T188))
pK_in_ggg(T186, T185, T188) → U22_ggg(T186, T185, T188, lessL_in_gg(T186, s(T185)))
U22_ggg(T186, T185, T188, lessL_out_gg(T186, s(T185))) → U23_ggg(T186, T185, T188, inI_in_gg(T185, T188))
U23_ggg(T186, T185, T188, inI_out_gg(T185, T188)) → pK_out_ggg(T186, T185, T188)
U12_gg(T185, T186, T187, T188, pK_out_ggg(T186, T185, T188)) → inI_out_gg(T185, tree(T186, T187, T188))
U21_ggg(T146, T147, T148, inI_out_gg(T146, T148)) → pJ_out_ggg(T146, T147, T148)
U11_gg(T146, T147, T148, T149, pJ_out_ggg(T146, T147, T148)) → inI_out_gg(T146, tree(T147, T148, T149))
U19_agg(T92, T88, T15, inI_out_gg(T92, T15)) → pC_out_agg(T92, T88, T15)
U2_ag(T89, T88, T15, T16, pC_out_agg(T89, T88, T15)) → inA_out_ag(s(T89), tree(s(T88), T15, T16))
inA_in_ag(T214, tree(T211, T212, T213)) → U3_ag(T214, T211, T212, T213, pD_in_gag(T211, T214, T213))
pD_in_gag(T211, T217, T213) → U24_gag(T211, T217, T213, lessM_in_ga(T211, T217))
lessM_in_ga(0, s(T224)) → lessM_out_ga(0, s(T224))
lessM_in_ga(s(T229), s(T231)) → U14_ga(T229, T231, lessM_in_ga(T229, T231))
U14_ga(T229, T231, lessM_out_ga(T229, T231)) → lessM_out_ga(s(T229), s(T231))
U24_gag(T211, T217, T213, lessM_out_ga(T211, T217)) → U25_gag(T211, T217, T213, inA_in_ag(T217, T213))
inA_in_ag(0, tree(s(T253), T246, T247)) → U4_ag(T253, T246, T247, inB_in_g(T246))
U4_ag(T253, T246, T247, inB_out_g(T246)) → inA_out_ag(0, tree(s(T253), T246, T247))
inA_in_ag(s(T268), tree(s(T267), T246, T247)) → U5_ag(T268, T267, T246, T247, pC_in_agg(T268, T267, T246))
U5_ag(T268, T267, T246, T247, pC_out_agg(T268, T267, T246)) → inA_out_ag(s(T268), tree(s(T267), T246, T247))
inA_in_ag(T286, tree(T283, T284, T285)) → U6_ag(T286, T283, T284, T285, pD_in_gag(T283, T286, T285))
U6_ag(T286, T283, T284, T285, pD_out_gag(T283, T286, T285)) → inA_out_ag(T286, tree(T283, T284, T285))
inA_in_ag(s(T303), tree(0, T295, T296)) → U7_ag(T303, T295, T296, inA_in_ag(s(T303), T296))
inA_in_ag(s(T316), tree(s(T314), T295, T296)) → U8_ag(T316, T314, T295, T296, pE_in_gag(T314, T316, T296))
pE_in_gag(T314, T319, T296) → U26_gag(T314, T319, T296, lessM_in_ga(T314, T319))
U26_gag(T314, T319, T296, lessM_out_ga(T314, T319)) → U27_gag(T314, T319, T296, inA_in_ag(s(T319), T296))
U27_gag(T314, T319, T296, inA_out_ag(s(T319), T296)) → pE_out_gag(T314, T319, T296)
U8_ag(T316, T314, T295, T296, pE_out_gag(T314, T316, T296)) → inA_out_ag(s(T316), tree(s(T314), T295, T296))
U7_ag(T303, T295, T296, inA_out_ag(s(T303), T296)) → inA_out_ag(s(T303), tree(0, T295, T296))
U25_gag(T211, T217, T213, inA_out_ag(T217, T213)) → pD_out_gag(T211, T217, T213)
U3_ag(T214, T211, T212, T213, pD_out_gag(T211, T214, T213)) → inA_out_ag(T214, tree(T211, T212, T213))

The argument filtering Pi contains the following mapping:
inA_in_ag(x1, x2)  =  inA_in_ag(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
inA_out_ag(x1, x2)  =  inA_out_ag(x1, x2)
s(x1)  =  s(x1)
U1_ag(x1, x2, x3, x4)  =  U1_ag(x1, x2, x3, x4)
inB_in_g(x1)  =  inB_in_g(x1)
0  =  0
inB_out_g(x1)  =  inB_out_g(x1)
U9_g(x1, x2, x3, x4)  =  U9_g(x1, x2, x3, x4)
pF_in_gg(x1, x2)  =  pF_in_gg(x1, x2)
U16_gg(x1, x2, x3)  =  U16_gg(x1, x2, x3)
lessN_in_g(x1)  =  lessN_in_g(x1)
lessN_out_g(x1)  =  lessN_out_g(x1)
U17_gg(x1, x2, x3)  =  U17_gg(x1, x2, x3)
pF_out_gg(x1, x2)  =  pF_out_gg(x1, x2)
U2_ag(x1, x2, x3, x4, x5)  =  U2_ag(x2, x3, x4, x5)
pC_in_agg(x1, x2, x3)  =  pC_in_agg(x2, x3)
U18_agg(x1, x2, x3, x4)  =  U18_agg(x2, x3, x4)
lessH_in_ag(x1, x2)  =  lessH_in_ag(x2)
lessH_out_ag(x1, x2)  =  lessH_out_ag(x1, x2)
U10_ag(x1, x2, x3)  =  U10_ag(x2, x3)
U19_agg(x1, x2, x3, x4)  =  U19_agg(x1, x2, x3, x4)
inI_in_gg(x1, x2)  =  inI_in_gg(x1, x2)
inI_out_gg(x1, x2)  =  inI_out_gg(x1, x2)
U11_gg(x1, x2, x3, x4, x5)  =  U11_gg(x1, x2, x3, x4, x5)
pJ_in_ggg(x1, x2, x3)  =  pJ_in_ggg(x1, x2, x3)
U20_ggg(x1, x2, x3, x4)  =  U20_ggg(x1, x2, x3, x4)
lessO_in_gg(x1, x2)  =  lessO_in_gg(x1, x2)
U15_gg(x1, x2, x3)  =  U15_gg(x1, x2, x3)
lessL_in_gg(x1, x2)  =  lessL_in_gg(x1, x2)
lessL_out_gg(x1, x2)  =  lessL_out_gg(x1, x2)
U13_gg(x1, x2, x3)  =  U13_gg(x1, x2, x3)
lessO_out_gg(x1, x2)  =  lessO_out_gg(x1, x2)
U21_ggg(x1, x2, x3, x4)  =  U21_ggg(x1, x2, x3, x4)
U12_gg(x1, x2, x3, x4, x5)  =  U12_gg(x1, x2, x3, x4, x5)
pK_in_ggg(x1, x2, x3)  =  pK_in_ggg(x1, x2, x3)
U22_ggg(x1, x2, x3, x4)  =  U22_ggg(x1, x2, x3, x4)
U23_ggg(x1, x2, x3, x4)  =  U23_ggg(x1, x2, x3, x4)
pK_out_ggg(x1, x2, x3)  =  pK_out_ggg(x1, x2, x3)
pJ_out_ggg(x1, x2, x3)  =  pJ_out_ggg(x1, x2, x3)
pC_out_agg(x1, x2, x3)  =  pC_out_agg(x1, x2, x3)
U3_ag(x1, x2, x3, x4, x5)  =  U3_ag(x2, x3, x4, x5)
pD_in_gag(x1, x2, x3)  =  pD_in_gag(x1, x3)
U24_gag(x1, x2, x3, x4)  =  U24_gag(x1, x3, x4)
lessM_in_ga(x1, x2)  =  lessM_in_ga(x1)
lessM_out_ga(x1, x2)  =  lessM_out_ga(x1)
U14_ga(x1, x2, x3)  =  U14_ga(x1, x3)
U25_gag(x1, x2, x3, x4)  =  U25_gag(x1, x3, x4)
U4_ag(x1, x2, x3, x4)  =  U4_ag(x1, x2, x3, x4)
U5_ag(x1, x2, x3, x4, x5)  =  U5_ag(x2, x3, x4, x5)
U6_ag(x1, x2, x3, x4, x5)  =  U6_ag(x2, x3, x4, x5)
pD_out_gag(x1, x2, x3)  =  pD_out_gag(x1, x2, x3)
U7_ag(x1, x2, x3, x4)  =  U7_ag(x2, x3, x4)
U8_ag(x1, x2, x3, x4, x5)  =  U8_ag(x2, x3, x4, x5)
pE_in_gag(x1, x2, x3)  =  pE_in_gag(x1, x3)
U26_gag(x1, x2, x3, x4)  =  U26_gag(x1, x3, x4)
U27_gag(x1, x2, x3, x4)  =  U27_gag(x1, x3, x4)
pE_out_gag(x1, x2, x3)  =  pE_out_gag(x1, x2, x3)
INI_IN_GG(x1, x2)  =  INI_IN_GG(x1, x2)
PJ_IN_GGG(x1, x2, x3)  =  PJ_IN_GGG(x1, x2, x3)
U20_GGG(x1, x2, x3, x4)  =  U20_GGG(x1, x2, x3, x4)
PK_IN_GGG(x1, x2, x3)  =  PK_IN_GGG(x1, x2, x3)
U22_GGG(x1, x2, x3, x4)  =  U22_GGG(x1, x2, x3, x4)

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

INI_IN_GG(T146, tree(T147, T148, T149)) → PJ_IN_GGG(T146, T147, T148)
PJ_IN_GGG(T146, T147, T148) → U20_GGG(T146, T147, T148, lessO_in_gg(T146, T147))
U20_GGG(T146, T147, T148, lessO_out_gg(T146, T147)) → INI_IN_GG(T146, T148)
INI_IN_GG(T185, tree(T186, T187, T188)) → PK_IN_GGG(T186, T185, T188)
PK_IN_GGG(T186, T185, T188) → U22_GGG(T186, T185, T188, lessL_in_gg(T186, s(T185)))
U22_GGG(T186, T185, T188, lessL_out_gg(T186, s(T185))) → INI_IN_GG(T185, T188)

The TRS R consists of the following rules:

lessO_in_gg(T154, s(T155)) → U15_gg(T154, T155, lessL_in_gg(T154, T155))
lessL_in_gg(0, s(T162)) → lessL_out_gg(0, s(T162))
lessL_in_gg(s(T167), s(T168)) → U13_gg(T167, T168, lessL_in_gg(T167, T168))
U15_gg(T154, T155, lessL_out_gg(T154, T155)) → lessO_out_gg(T154, s(T155))
U13_gg(T167, T168, lessL_out_gg(T167, T168)) → lessL_out_gg(s(T167), s(T168))

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

(24) PiDPToQDPProof (EQUIVALENT transformation)

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

(25) Obligation:

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

INI_IN_GG(T146, tree(T147, T148, T149)) → PJ_IN_GGG(T146, T147, T148)
PJ_IN_GGG(T146, T147, T148) → U20_GGG(T146, T147, T148, lessO_in_gg(T146, T147))
U20_GGG(T146, T147, T148, lessO_out_gg(T146, T147)) → INI_IN_GG(T146, T148)
INI_IN_GG(T185, tree(T186, T187, T188)) → PK_IN_GGG(T186, T185, T188)
PK_IN_GGG(T186, T185, T188) → U22_GGG(T186, T185, T188, lessL_in_gg(T186, s(T185)))
U22_GGG(T186, T185, T188, lessL_out_gg(T186, s(T185))) → INI_IN_GG(T185, T188)

The TRS R consists of the following rules:

lessO_in_gg(T154, s(T155)) → U15_gg(T154, T155, lessL_in_gg(T154, T155))
lessL_in_gg(0, s(T162)) → lessL_out_gg(0, s(T162))
lessL_in_gg(s(T167), s(T168)) → U13_gg(T167, T168, lessL_in_gg(T167, T168))
U15_gg(T154, T155, lessL_out_gg(T154, T155)) → lessO_out_gg(T154, s(T155))
U13_gg(T167, T168, lessL_out_gg(T167, T168)) → lessL_out_gg(s(T167), s(T168))

The set Q consists of the following terms:

lessO_in_gg(x0, x1)
lessL_in_gg(x0, x1)
U15_gg(x0, x1, x2)
U13_gg(x0, x1, x2)

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

(26) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

• PJ_IN_GGG(T146, T147, T148) → U20_GGG(T146, T147, T148, lessO_in_gg(T146, T147))
  The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3

• U20_GGG(T146, T147, T148, lessO_out_gg(T146, T147)) → INI_IN_GG(T146, T148)
  The graph contains the following edges 1 >= 1, 4 > 1, 3 >= 2

• U22_GGG(T186, T185, T188, lessL_out_gg(T186, s(T185))) → INI_IN_GG(T185, T188)
  The graph contains the following edges 2 >= 1, 4 > 1, 3 >= 2

• INI_IN_GG(T146, tree(T147, T148, T149)) → PJ_IN_GGG(T146, T147, T148)
  The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

• INI_IN_GG(T185, tree(T186, T187, T188)) → PK_IN_GGG(T186, T185, T188)
  The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3

• PK_IN_GGG(T186, T185, T188) → U22_GGG(T186, T185, T188, lessL_in_gg(T186, s(T185)))
  The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3

(27) YES

(28) Obligation:

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

LESSH_IN_AG(s(T106), s(T105)) → LESSH_IN_AG(T106, T105)

The TRS R consists of the following rules:

inA_in_ag(T6, tree(T6, T7, T8)) → inA_out_ag(T6, tree(T6, T7, T8))
inA_in_ag(0, tree(s(T22), T15, T16)) → U1_ag(T22, T15, T16, inB_in_g(T15))
inB_in_g(tree(0, T35, T36)) → inB_out_g(tree(0, T35, T36))
inB_in_g(tree(T49, T50, T51)) → U9_g(T49, T50, T51, pF_in_gg(T49, T50))
pF_in_gg(T49, T50) → U16_gg(T49, T50, lessN_in_g(T49))
lessN_in_g(s(T60)) → lessN_out_g(s(T60))
U16_gg(T49, T50, lessN_out_g(T49)) → U17_gg(T49, T50, inB_in_g(T50))
U17_gg(T49, T50, inB_out_g(T50)) → pF_out_gg(T49, T50)
U9_g(T49, T50, T51, pF_out_gg(T49, T50)) → inB_out_g(tree(T49, T50, T51))
U1_ag(T22, T15, T16, inB_out_g(T15)) → inA_out_ag(0, tree(s(T22), T15, T16))
inA_in_ag(s(T89), tree(s(T88), T15, T16)) → U2_ag(T89, T88, T15, T16, pC_in_agg(T89, T88, T15))
pC_in_agg(T92, T88, T15) → U18_agg(T92, T88, T15, lessH_in_ag(T92, T88))
lessH_in_ag(0, s(T99)) → lessH_out_ag(0, s(T99))
lessH_in_ag(s(T106), s(T105)) → U10_ag(T106, T105, lessH_in_ag(T106, T105))
U10_ag(T106, T105, lessH_out_ag(T106, T105)) → lessH_out_ag(s(T106), s(T105))
U18_agg(T92, T88, T15, lessH_out_ag(T92, T88)) → U19_agg(T92, T88, T15, inI_in_gg(T92, T15))
inI_in_gg(T127, tree(s(T127), T128, T129)) → inI_out_gg(T127, tree(s(T127), T128, T129))
inI_in_gg(T146, tree(T147, T148, T149)) → U11_gg(T146, T147, T148, T149, pJ_in_ggg(T146, T147, T148))
pJ_in_ggg(T146, T147, T148) → U20_ggg(T146, T147, T148, lessO_in_gg(T146, T147))
lessO_in_gg(T154, s(T155)) → U15_gg(T154, T155, lessL_in_gg(T154, T155))
lessL_in_gg(0, s(T162)) → lessL_out_gg(0, s(T162))
lessL_in_gg(s(T167), s(T168)) → U13_gg(T167, T168, lessL_in_gg(T167, T168))
U13_gg(T167, T168, lessL_out_gg(T167, T168)) → lessL_out_gg(s(T167), s(T168))
U15_gg(T154, T155, lessL_out_gg(T154, T155)) → lessO_out_gg(T154, s(T155))
U20_ggg(T146, T147, T148, lessO_out_gg(T146, T147)) → U21_ggg(T146, T147, T148, inI_in_gg(T146, T148))
inI_in_gg(T185, tree(T186, T187, T188)) → U12_gg(T185, T186, T187, T188, pK_in_ggg(T186, T185, T188))
pK_in_ggg(T186, T185, T188) → U22_ggg(T186, T185, T188, lessL_in_gg(T186, s(T185)))
U22_ggg(T186, T185, T188, lessL_out_gg(T186, s(T185))) → U23_ggg(T186, T185, T188, inI_in_gg(T185, T188))
U23_ggg(T186, T185, T188, inI_out_gg(T185, T188)) → pK_out_ggg(T186, T185, T188)
U12_gg(T185, T186, T187, T188, pK_out_ggg(T186, T185, T188)) → inI_out_gg(T185, tree(T186, T187, T188))
U21_ggg(T146, T147, T148, inI_out_gg(T146, T148)) → pJ_out_ggg(T146, T147, T148)
U11_gg(T146, T147, T148, T149, pJ_out_ggg(T146, T147, T148)) → inI_out_gg(T146, tree(T147, T148, T149))
U19_agg(T92, T88, T15, inI_out_gg(T92, T15)) → pC_out_agg(T92, T88, T15)
U2_ag(T89, T88, T15, T16, pC_out_agg(T89, T88, T15)) → inA_out_ag(s(T89), tree(s(T88), T15, T16))
inA_in_ag(T214, tree(T211, T212, T213)) → U3_ag(T214, T211, T212, T213, pD_in_gag(T211, T214, T213))
pD_in_gag(T211, T217, T213) → U24_gag(T211, T217, T213, lessM_in_ga(T211, T217))
lessM_in_ga(0, s(T224)) → lessM_out_ga(0, s(T224))
lessM_in_ga(s(T229), s(T231)) → U14_ga(T229, T231, lessM_in_ga(T229, T231))
U14_ga(T229, T231, lessM_out_ga(T229, T231)) → lessM_out_ga(s(T229), s(T231))
U24_gag(T211, T217, T213, lessM_out_ga(T211, T217)) → U25_gag(T211, T217, T213, inA_in_ag(T217, T213))
inA_in_ag(0, tree(s(T253), T246, T247)) → U4_ag(T253, T246, T247, inB_in_g(T246))
U4_ag(T253, T246, T247, inB_out_g(T246)) → inA_out_ag(0, tree(s(T253), T246, T247))
inA_in_ag(s(T268), tree(s(T267), T246, T247)) → U5_ag(T268, T267, T246, T247, pC_in_agg(T268, T267, T246))
U5_ag(T268, T267, T246, T247, pC_out_agg(T268, T267, T246)) → inA_out_ag(s(T268), tree(s(T267), T246, T247))
inA_in_ag(T286, tree(T283, T284, T285)) → U6_ag(T286, T283, T284, T285, pD_in_gag(T283, T286, T285))
U6_ag(T286, T283, T284, T285, pD_out_gag(T283, T286, T285)) → inA_out_ag(T286, tree(T283, T284, T285))
inA_in_ag(s(T303), tree(0, T295, T296)) → U7_ag(T303, T295, T296, inA_in_ag(s(T303), T296))
inA_in_ag(s(T316), tree(s(T314), T295, T296)) → U8_ag(T316, T314, T295, T296, pE_in_gag(T314, T316, T296))
pE_in_gag(T314, T319, T296) → U26_gag(T314, T319, T296, lessM_in_ga(T314, T319))
U26_gag(T314, T319, T296, lessM_out_ga(T314, T319)) → U27_gag(T314, T319, T296, inA_in_ag(s(T319), T296))
U27_gag(T314, T319, T296, inA_out_ag(s(T319), T296)) → pE_out_gag(T314, T319, T296)
U8_ag(T316, T314, T295, T296, pE_out_gag(T314, T316, T296)) → inA_out_ag(s(T316), tree(s(T314), T295, T296))
U7_ag(T303, T295, T296, inA_out_ag(s(T303), T296)) → inA_out_ag(s(T303), tree(0, T295, T296))
U25_gag(T211, T217, T213, inA_out_ag(T217, T213)) → pD_out_gag(T211, T217, T213)
U3_ag(T214, T211, T212, T213, pD_out_gag(T211, T214, T213)) → inA_out_ag(T214, tree(T211, T212, T213))

The argument filtering Pi contains the following mapping:
inA_in_ag(x1, x2)  =  inA_in_ag(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
inA_out_ag(x1, x2)  =  inA_out_ag(x1, x2)
s(x1)  =  s(x1)
U1_ag(x1, x2, x3, x4)  =  U1_ag(x1, x2, x3, x4)
inB_in_g(x1)  =  inB_in_g(x1)
0  =  0
inB_out_g(x1)  =  inB_out_g(x1)
U9_g(x1, x2, x3, x4)  =  U9_g(x1, x2, x3, x4)
pF_in_gg(x1, x2)  =  pF_in_gg(x1, x2)
U16_gg(x1, x2, x3)  =  U16_gg(x1, x2, x3)
lessN_in_g(x1)  =  lessN_in_g(x1)
lessN_out_g(x1)  =  lessN_out_g(x1)
U17_gg(x1, x2, x3)  =  U17_gg(x1, x2, x3)
pF_out_gg(x1, x2)  =  pF_out_gg(x1, x2)
U2_ag(x1, x2, x3, x4, x5)  =  U2_ag(x2, x3, x4, x5)
pC_in_agg(x1, x2, x3)  =  pC_in_agg(x2, x3)
U18_agg(x1, x2, x3, x4)  =  U18_agg(x2, x3, x4)
lessH_in_ag(x1, x2)  =  lessH_in_ag(x2)
lessH_out_ag(x1, x2)  =  lessH_out_ag(x1, x2)
U10_ag(x1, x2, x3)  =  U10_ag(x2, x3)
U19_agg(x1, x2, x3, x4)  =  U19_agg(x1, x2, x3, x4)
inI_in_gg(x1, x2)  =  inI_in_gg(x1, x2)
inI_out_gg(x1, x2)  =  inI_out_gg(x1, x2)
U11_gg(x1, x2, x3, x4, x5)  =  U11_gg(x1, x2, x3, x4, x5)
pJ_in_ggg(x1, x2, x3)  =  pJ_in_ggg(x1, x2, x3)
U20_ggg(x1, x2, x3, x4)  =  U20_ggg(x1, x2, x3, x4)
lessO_in_gg(x1, x2)  =  lessO_in_gg(x1, x2)
U15_gg(x1, x2, x3)  =  U15_gg(x1, x2, x3)
lessL_in_gg(x1, x2)  =  lessL_in_gg(x1, x2)
lessL_out_gg(x1, x2)  =  lessL_out_gg(x1, x2)
U13_gg(x1, x2, x3)  =  U13_gg(x1, x2, x3)
lessO_out_gg(x1, x2)  =  lessO_out_gg(x1, x2)
U21_ggg(x1, x2, x3, x4)  =  U21_ggg(x1, x2, x3, x4)
U12_gg(x1, x2, x3, x4, x5)  =  U12_gg(x1, x2, x3, x4, x5)
pK_in_ggg(x1, x2, x3)  =  pK_in_ggg(x1, x2, x3)
U22_ggg(x1, x2, x3, x4)  =  U22_ggg(x1, x2, x3, x4)
U23_ggg(x1, x2, x3, x4)  =  U23_ggg(x1, x2, x3, x4)
pK_out_ggg(x1, x2, x3)  =  pK_out_ggg(x1, x2, x3)
pJ_out_ggg(x1, x2, x3)  =  pJ_out_ggg(x1, x2, x3)
pC_out_agg(x1, x2, x3)  =  pC_out_agg(x1, x2, x3)
U3_ag(x1, x2, x3, x4, x5)  =  U3_ag(x2, x3, x4, x5)
pD_in_gag(x1, x2, x3)  =  pD_in_gag(x1, x3)
U24_gag(x1, x2, x3, x4)  =  U24_gag(x1, x3, x4)
lessM_in_ga(x1, x2)  =  lessM_in_ga(x1)
lessM_out_ga(x1, x2)  =  lessM_out_ga(x1)
U14_ga(x1, x2, x3)  =  U14_ga(x1, x3)
U25_gag(x1, x2, x3, x4)  =  U25_gag(x1, x3, x4)
U4_ag(x1, x2, x3, x4)  =  U4_ag(x1, x2, x3, x4)
U5_ag(x1, x2, x3, x4, x5)  =  U5_ag(x2, x3, x4, x5)
U6_ag(x1, x2, x3, x4, x5)  =  U6_ag(x2, x3, x4, x5)
pD_out_gag(x1, x2, x3)  =  pD_out_gag(x1, x2, x3)
U7_ag(x1, x2, x3, x4)  =  U7_ag(x2, x3, x4)
U8_ag(x1, x2, x3, x4, x5)  =  U8_ag(x2, x3, x4, x5)
pE_in_gag(x1, x2, x3)  =  pE_in_gag(x1, x3)
U26_gag(x1, x2, x3, x4)  =  U26_gag(x1, x3, x4)
U27_gag(x1, x2, x3, x4)  =  U27_gag(x1, x3, x4)
pE_out_gag(x1, x2, x3)  =  pE_out_gag(x1, x2, x3)
LESSH_IN_AG(x1, x2)  =  LESSH_IN_AG(x2)

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

(29) UsableRulesProof (EQUIVALENT transformation)

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

(30) Obligation:

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

LESSH_IN_AG(s(T106), s(T105)) → LESSH_IN_AG(T106, T105)

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

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

(31) PiDPToQDPProof (SOUND transformation)

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

(32) Obligation:

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

LESSH_IN_AG(s(T105)) → LESSH_IN_AG(T105)

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

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

• LESSH_IN_AG(s(T105)) → LESSH_IN_AG(T105)
  The graph contains the following edges 1 > 1

(34) YES

(35) Obligation:

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

INB_IN_G(tree(T49, T50, T51)) → PF_IN_GG(T49, T50)
PF_IN_GG(T49, T50) → U16_GG(T49, T50, lessN_in_g(T49))
U16_GG(T49, T50, lessN_out_g(T49)) → INB_IN_G(T50)

The TRS R consists of the following rules:

inA_in_ag(T6, tree(T6, T7, T8)) → inA_out_ag(T6, tree(T6, T7, T8))
inA_in_ag(0, tree(s(T22), T15, T16)) → U1_ag(T22, T15, T16, inB_in_g(T15))
inB_in_g(tree(0, T35, T36)) → inB_out_g(tree(0, T35, T36))
inB_in_g(tree(T49, T50, T51)) → U9_g(T49, T50, T51, pF_in_gg(T49, T50))
pF_in_gg(T49, T50) → U16_gg(T49, T50, lessN_in_g(T49))
lessN_in_g(s(T60)) → lessN_out_g(s(T60))
U16_gg(T49, T50, lessN_out_g(T49)) → U17_gg(T49, T50, inB_in_g(T50))
U17_gg(T49, T50, inB_out_g(T50)) → pF_out_gg(T49, T50)
U9_g(T49, T50, T51, pF_out_gg(T49, T50)) → inB_out_g(tree(T49, T50, T51))
U1_ag(T22, T15, T16, inB_out_g(T15)) → inA_out_ag(0, tree(s(T22), T15, T16))
inA_in_ag(s(T89), tree(s(T88), T15, T16)) → U2_ag(T89, T88, T15, T16, pC_in_agg(T89, T88, T15))
pC_in_agg(T92, T88, T15) → U18_agg(T92, T88, T15, lessH_in_ag(T92, T88))
lessH_in_ag(0, s(T99)) → lessH_out_ag(0, s(T99))
lessH_in_ag(s(T106), s(T105)) → U10_ag(T106, T105, lessH_in_ag(T106, T105))
U10_ag(T106, T105, lessH_out_ag(T106, T105)) → lessH_out_ag(s(T106), s(T105))
U18_agg(T92, T88, T15, lessH_out_ag(T92, T88)) → U19_agg(T92, T88, T15, inI_in_gg(T92, T15))
inI_in_gg(T127, tree(s(T127), T128, T129)) → inI_out_gg(T127, tree(s(T127), T128, T129))
inI_in_gg(T146, tree(T147, T148, T149)) → U11_gg(T146, T147, T148, T149, pJ_in_ggg(T146, T147, T148))
pJ_in_ggg(T146, T147, T148) → U20_ggg(T146, T147, T148, lessO_in_gg(T146, T147))
lessO_in_gg(T154, s(T155)) → U15_gg(T154, T155, lessL_in_gg(T154, T155))
lessL_in_gg(0, s(T162)) → lessL_out_gg(0, s(T162))
lessL_in_gg(s(T167), s(T168)) → U13_gg(T167, T168, lessL_in_gg(T167, T168))
U13_gg(T167, T168, lessL_out_gg(T167, T168)) → lessL_out_gg(s(T167), s(T168))
U15_gg(T154, T155, lessL_out_gg(T154, T155)) → lessO_out_gg(T154, s(T155))
U20_ggg(T146, T147, T148, lessO_out_gg(T146, T147)) → U21_ggg(T146, T147, T148, inI_in_gg(T146, T148))
inI_in_gg(T185, tree(T186, T187, T188)) → U12_gg(T185, T186, T187, T188, pK_in_ggg(T186, T185, T188))
pK_in_ggg(T186, T185, T188) → U22_ggg(T186, T185, T188, lessL_in_gg(T186, s(T185)))
U22_ggg(T186, T185, T188, lessL_out_gg(T186, s(T185))) → U23_ggg(T186, T185, T188, inI_in_gg(T185, T188))
U23_ggg(T186, T185, T188, inI_out_gg(T185, T188)) → pK_out_ggg(T186, T185, T188)
U12_gg(T185, T186, T187, T188, pK_out_ggg(T186, T185, T188)) → inI_out_gg(T185, tree(T186, T187, T188))
U21_ggg(T146, T147, T148, inI_out_gg(T146, T148)) → pJ_out_ggg(T146, T147, T148)
U11_gg(T146, T147, T148, T149, pJ_out_ggg(T146, T147, T148)) → inI_out_gg(T146, tree(T147, T148, T149))
U19_agg(T92, T88, T15, inI_out_gg(T92, T15)) → pC_out_agg(T92, T88, T15)
U2_ag(T89, T88, T15, T16, pC_out_agg(T89, T88, T15)) → inA_out_ag(s(T89), tree(s(T88), T15, T16))
inA_in_ag(T214, tree(T211, T212, T213)) → U3_ag(T214, T211, T212, T213, pD_in_gag(T211, T214, T213))
pD_in_gag(T211, T217, T213) → U24_gag(T211, T217, T213, lessM_in_ga(T211, T217))
lessM_in_ga(0, s(T224)) → lessM_out_ga(0, s(T224))
lessM_in_ga(s(T229), s(T231)) → U14_ga(T229, T231, lessM_in_ga(T229, T231))
U14_ga(T229, T231, lessM_out_ga(T229, T231)) → lessM_out_ga(s(T229), s(T231))
U24_gag(T211, T217, T213, lessM_out_ga(T211, T217)) → U25_gag(T211, T217, T213, inA_in_ag(T217, T213))
inA_in_ag(0, tree(s(T253), T246, T247)) → U4_ag(T253, T246, T247, inB_in_g(T246))
U4_ag(T253, T246, T247, inB_out_g(T246)) → inA_out_ag(0, tree(s(T253), T246, T247))
inA_in_ag(s(T268), tree(s(T267), T246, T247)) → U5_ag(T268, T267, T246, T247, pC_in_agg(T268, T267, T246))
U5_ag(T268, T267, T246, T247, pC_out_agg(T268, T267, T246)) → inA_out_ag(s(T268), tree(s(T267), T246, T247))
inA_in_ag(T286, tree(T283, T284, T285)) → U6_ag(T286, T283, T284, T285, pD_in_gag(T283, T286, T285))
U6_ag(T286, T283, T284, T285, pD_out_gag(T283, T286, T285)) → inA_out_ag(T286, tree(T283, T284, T285))
inA_in_ag(s(T303), tree(0, T295, T296)) → U7_ag(T303, T295, T296, inA_in_ag(s(T303), T296))
inA_in_ag(s(T316), tree(s(T314), T295, T296)) → U8_ag(T316, T314, T295, T296, pE_in_gag(T314, T316, T296))
pE_in_gag(T314, T319, T296) → U26_gag(T314, T319, T296, lessM_in_ga(T314, T319))
U26_gag(T314, T319, T296, lessM_out_ga(T314, T319)) → U27_gag(T314, T319, T296, inA_in_ag(s(T319), T296))
U27_gag(T314, T319, T296, inA_out_ag(s(T319), T296)) → pE_out_gag(T314, T319, T296)
U8_ag(T316, T314, T295, T296, pE_out_gag(T314, T316, T296)) → inA_out_ag(s(T316), tree(s(T314), T295, T296))
U7_ag(T303, T295, T296, inA_out_ag(s(T303), T296)) → inA_out_ag(s(T303), tree(0, T295, T296))
U25_gag(T211, T217, T213, inA_out_ag(T217, T213)) → pD_out_gag(T211, T217, T213)
U3_ag(T214, T211, T212, T213, pD_out_gag(T211, T214, T213)) → inA_out_ag(T214, tree(T211, T212, T213))

The argument filtering Pi contains the following mapping:
inA_in_ag(x1, x2)  =  inA_in_ag(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
inA_out_ag(x1, x2)  =  inA_out_ag(x1, x2)
s(x1)  =  s(x1)
U1_ag(x1, x2, x3, x4)  =  U1_ag(x1, x2, x3, x4)
inB_in_g(x1)  =  inB_in_g(x1)
0  =  0
inB_out_g(x1)  =  inB_out_g(x1)
U9_g(x1, x2, x3, x4)  =  U9_g(x1, x2, x3, x4)
pF_in_gg(x1, x2)  =  pF_in_gg(x1, x2)
U16_gg(x1, x2, x3)  =  U16_gg(x1, x2, x3)
lessN_in_g(x1)  =  lessN_in_g(x1)
lessN_out_g(x1)  =  lessN_out_g(x1)
U17_gg(x1, x2, x3)  =  U17_gg(x1, x2, x3)
pF_out_gg(x1, x2)  =  pF_out_gg(x1, x2)
U2_ag(x1, x2, x3, x4, x5)  =  U2_ag(x2, x3, x4, x5)
pC_in_agg(x1, x2, x3)  =  pC_in_agg(x2, x3)
U18_agg(x1, x2, x3, x4)  =  U18_agg(x2, x3, x4)
lessH_in_ag(x1, x2)  =  lessH_in_ag(x2)
lessH_out_ag(x1, x2)  =  lessH_out_ag(x1, x2)
U10_ag(x1, x2, x3)  =  U10_ag(x2, x3)
U19_agg(x1, x2, x3, x4)  =  U19_agg(x1, x2, x3, x4)
inI_in_gg(x1, x2)  =  inI_in_gg(x1, x2)
inI_out_gg(x1, x2)  =  inI_out_gg(x1, x2)
U11_gg(x1, x2, x3, x4, x5)  =  U11_gg(x1, x2, x3, x4, x5)
pJ_in_ggg(x1, x2, x3)  =  pJ_in_ggg(x1, x2, x3)
U20_ggg(x1, x2, x3, x4)  =  U20_ggg(x1, x2, x3, x4)
lessO_in_gg(x1, x2)  =  lessO_in_gg(x1, x2)
U15_gg(x1, x2, x3)  =  U15_gg(x1, x2, x3)
lessL_in_gg(x1, x2)  =  lessL_in_gg(x1, x2)
lessL_out_gg(x1, x2)  =  lessL_out_gg(x1, x2)
U13_gg(x1, x2, x3)  =  U13_gg(x1, x2, x3)
lessO_out_gg(x1, x2)  =  lessO_out_gg(x1, x2)
U21_ggg(x1, x2, x3, x4)  =  U21_ggg(x1, x2, x3, x4)
U12_gg(x1, x2, x3, x4, x5)  =  U12_gg(x1, x2, x3, x4, x5)
pK_in_ggg(x1, x2, x3)  =  pK_in_ggg(x1, x2, x3)
U22_ggg(x1, x2, x3, x4)  =  U22_ggg(x1, x2, x3, x4)
U23_ggg(x1, x2, x3, x4)  =  U23_ggg(x1, x2, x3, x4)
pK_out_ggg(x1, x2, x3)  =  pK_out_ggg(x1, x2, x3)
pJ_out_ggg(x1, x2, x3)  =  pJ_out_ggg(x1, x2, x3)
pC_out_agg(x1, x2, x3)  =  pC_out_agg(x1, x2, x3)
U3_ag(x1, x2, x3, x4, x5)  =  U3_ag(x2, x3, x4, x5)
pD_in_gag(x1, x2, x3)  =  pD_in_gag(x1, x3)
U24_gag(x1, x2, x3, x4)  =  U24_gag(x1, x3, x4)
lessM_in_ga(x1, x2)  =  lessM_in_ga(x1)
lessM_out_ga(x1, x2)  =  lessM_out_ga(x1)
U14_ga(x1, x2, x3)  =  U14_ga(x1, x3)
U25_gag(x1, x2, x3, x4)  =  U25_gag(x1, x3, x4)
U4_ag(x1, x2, x3, x4)  =  U4_ag(x1, x2, x3, x4)
U5_ag(x1, x2, x3, x4, x5)  =  U5_ag(x2, x3, x4, x5)
U6_ag(x1, x2, x3, x4, x5)  =  U6_ag(x2, x3, x4, x5)
pD_out_gag(x1, x2, x3)  =  pD_out_gag(x1, x2, x3)
U7_ag(x1, x2, x3, x4)  =  U7_ag(x2, x3, x4)
U8_ag(x1, x2, x3, x4, x5)  =  U8_ag(x2, x3, x4, x5)
pE_in_gag(x1, x2, x3)  =  pE_in_gag(x1, x3)
U26_gag(x1, x2, x3, x4)  =  U26_gag(x1, x3, x4)
U27_gag(x1, x2, x3, x4)  =  U27_gag(x1, x3, x4)
pE_out_gag(x1, x2, x3)  =  pE_out_gag(x1, x2, x3)
INB_IN_G(x1)  =  INB_IN_G(x1)
PF_IN_GG(x1, x2)  =  PF_IN_GG(x1, x2)
U16_GG(x1, x2, x3)  =  U16_GG(x1, x2, x3)

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

(36) UsableRulesProof (EQUIVALENT transformation)

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

(37) Obligation:

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

INB_IN_G(tree(T49, T50, T51)) → PF_IN_GG(T49, T50)
PF_IN_GG(T49, T50) → U16_GG(T49, T50, lessN_in_g(T49))
U16_GG(T49, T50, lessN_out_g(T49)) → INB_IN_G(T50)

The TRS R consists of the following rules:

lessN_in_g(s(T60)) → lessN_out_g(s(T60))

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

(38) PiDPToQDPProof (EQUIVALENT transformation)

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

(39) Obligation:

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

INB_IN_G(tree(T49, T50, T51)) → PF_IN_GG(T49, T50)
PF_IN_GG(T49, T50) → U16_GG(T49, T50, lessN_in_g(T49))
U16_GG(T49, T50, lessN_out_g(T49)) → INB_IN_G(T50)

The TRS R consists of the following rules:

lessN_in_g(s(T60)) → lessN_out_g(s(T60))

The set Q consists of the following terms:

lessN_in_g(x0)

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

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

• PF_IN_GG(T49, T50) → U16_GG(T49, T50, lessN_in_g(T49))
  The graph contains the following edges 1 >= 1, 2 >= 2

• U16_GG(T49, T50, lessN_out_g(T49)) → INB_IN_G(T50)
  The graph contains the following edges 2 >= 1

• INB_IN_G(tree(T49, T50, T51)) → PF_IN_GG(T49, T50)
  The graph contains the following edges 1 > 1, 1 > 2

(41) YES

(42) Obligation:

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

INA_IN_AG(T214, tree(T211, T212, T213)) → PD_IN_GAG(T211, T214, T213)
PD_IN_GAG(T211, T217, T213) → U24_GAG(T211, T217, T213, lessM_in_ga(T211, T217))
U24_GAG(T211, T217, T213, lessM_out_ga(T211, T217)) → INA_IN_AG(T217, T213)
INA_IN_AG(s(T303), tree(0, T295, T296)) → INA_IN_AG(s(T303), T296)
INA_IN_AG(s(T316), tree(s(T314), T295, T296)) → PE_IN_GAG(T314, T316, T296)
PE_IN_GAG(T314, T319, T296) → U26_GAG(T314, T319, T296, lessM_in_ga(T314, T319))
U26_GAG(T314, T319, T296, lessM_out_ga(T314, T319)) → INA_IN_AG(s(T319), T296)

The TRS R consists of the following rules:

inA_in_ag(T6, tree(T6, T7, T8)) → inA_out_ag(T6, tree(T6, T7, T8))
inA_in_ag(0, tree(s(T22), T15, T16)) → U1_ag(T22, T15, T16, inB_in_g(T15))
inB_in_g(tree(0, T35, T36)) → inB_out_g(tree(0, T35, T36))
inB_in_g(tree(T49, T50, T51)) → U9_g(T49, T50, T51, pF_in_gg(T49, T50))
pF_in_gg(T49, T50) → U16_gg(T49, T50, lessN_in_g(T49))
lessN_in_g(s(T60)) → lessN_out_g(s(T60))
U16_gg(T49, T50, lessN_out_g(T49)) → U17_gg(T49, T50, inB_in_g(T50))
U17_gg(T49, T50, inB_out_g(T50)) → pF_out_gg(T49, T50)
U9_g(T49, T50, T51, pF_out_gg(T49, T50)) → inB_out_g(tree(T49, T50, T51))
U1_ag(T22, T15, T16, inB_out_g(T15)) → inA_out_ag(0, tree(s(T22), T15, T16))
inA_in_ag(s(T89), tree(s(T88), T15, T16)) → U2_ag(T89, T88, T15, T16, pC_in_agg(T89, T88, T15))
pC_in_agg(T92, T88, T15) → U18_agg(T92, T88, T15, lessH_in_ag(T92, T88))
lessH_in_ag(0, s(T99)) → lessH_out_ag(0, s(T99))
lessH_in_ag(s(T106), s(T105)) → U10_ag(T106, T105, lessH_in_ag(T106, T105))
U10_ag(T106, T105, lessH_out_ag(T106, T105)) → lessH_out_ag(s(T106), s(T105))
U18_agg(T92, T88, T15, lessH_out_ag(T92, T88)) → U19_agg(T92, T88, T15, inI_in_gg(T92, T15))
inI_in_gg(T127, tree(s(T127), T128, T129)) → inI_out_gg(T127, tree(s(T127), T128, T129))
inI_in_gg(T146, tree(T147, T148, T149)) → U11_gg(T146, T147, T148, T149, pJ_in_ggg(T146, T147, T148))
pJ_in_ggg(T146, T147, T148) → U20_ggg(T146, T147, T148, lessO_in_gg(T146, T147))
lessO_in_gg(T154, s(T155)) → U15_gg(T154, T155, lessL_in_gg(T154, T155))
lessL_in_gg(0, s(T162)) → lessL_out_gg(0, s(T162))
lessL_in_gg(s(T167), s(T168)) → U13_gg(T167, T168, lessL_in_gg(T167, T168))
U13_gg(T167, T168, lessL_out_gg(T167, T168)) → lessL_out_gg(s(T167), s(T168))
U15_gg(T154, T155, lessL_out_gg(T154, T155)) → lessO_out_gg(T154, s(T155))
U20_ggg(T146, T147, T148, lessO_out_gg(T146, T147)) → U21_ggg(T146, T147, T148, inI_in_gg(T146, T148))
inI_in_gg(T185, tree(T186, T187, T188)) → U12_gg(T185, T186, T187, T188, pK_in_ggg(T186, T185, T188))
pK_in_ggg(T186, T185, T188) → U22_ggg(T186, T185, T188, lessL_in_gg(T186, s(T185)))
U22_ggg(T186, T185, T188, lessL_out_gg(T186, s(T185))) → U23_ggg(T186, T185, T188, inI_in_gg(T185, T188))
U23_ggg(T186, T185, T188, inI_out_gg(T185, T188)) → pK_out_ggg(T186, T185, T188)
U12_gg(T185, T186, T187, T188, pK_out_ggg(T186, T185, T188)) → inI_out_gg(T185, tree(T186, T187, T188))
U21_ggg(T146, T147, T148, inI_out_gg(T146, T148)) → pJ_out_ggg(T146, T147, T148)
U11_gg(T146, T147, T148, T149, pJ_out_ggg(T146, T147, T148)) → inI_out_gg(T146, tree(T147, T148, T149))
U19_agg(T92, T88, T15, inI_out_gg(T92, T15)) → pC_out_agg(T92, T88, T15)
U2_ag(T89, T88, T15, T16, pC_out_agg(T89, T88, T15)) → inA_out_ag(s(T89), tree(s(T88), T15, T16))
inA_in_ag(T214, tree(T211, T212, T213)) → U3_ag(T214, T211, T212, T213, pD_in_gag(T211, T214, T213))
pD_in_gag(T211, T217, T213) → U24_gag(T211, T217, T213, lessM_in_ga(T211, T217))
lessM_in_ga(0, s(T224)) → lessM_out_ga(0, s(T224))
lessM_in_ga(s(T229), s(T231)) → U14_ga(T229, T231, lessM_in_ga(T229, T231))
U14_ga(T229, T231, lessM_out_ga(T229, T231)) → lessM_out_ga(s(T229), s(T231))
U24_gag(T211, T217, T213, lessM_out_ga(T211, T217)) → U25_gag(T211, T217, T213, inA_in_ag(T217, T213))
inA_in_ag(0, tree(s(T253), T246, T247)) → U4_ag(T253, T246, T247, inB_in_g(T246))
U4_ag(T253, T246, T247, inB_out_g(T246)) → inA_out_ag(0, tree(s(T253), T246, T247))
inA_in_ag(s(T268), tree(s(T267), T246, T247)) → U5_ag(T268, T267, T246, T247, pC_in_agg(T268, T267, T246))
U5_ag(T268, T267, T246, T247, pC_out_agg(T268, T267, T246)) → inA_out_ag(s(T268), tree(s(T267), T246, T247))
inA_in_ag(T286, tree(T283, T284, T285)) → U6_ag(T286, T283, T284, T285, pD_in_gag(T283, T286, T285))
U6_ag(T286, T283, T284, T285, pD_out_gag(T283, T286, T285)) → inA_out_ag(T286, tree(T283, T284, T285))
inA_in_ag(s(T303), tree(0, T295, T296)) → U7_ag(T303, T295, T296, inA_in_ag(s(T303), T296))
inA_in_ag(s(T316), tree(s(T314), T295, T296)) → U8_ag(T316, T314, T295, T296, pE_in_gag(T314, T316, T296))
pE_in_gag(T314, T319, T296) → U26_gag(T314, T319, T296, lessM_in_ga(T314, T319))
U26_gag(T314, T319, T296, lessM_out_ga(T314, T319)) → U27_gag(T314, T319, T296, inA_in_ag(s(T319), T296))
U27_gag(T314, T319, T296, inA_out_ag(s(T319), T296)) → pE_out_gag(T314, T319, T296)
U8_ag(T316, T314, T295, T296, pE_out_gag(T314, T316, T296)) → inA_out_ag(s(T316), tree(s(T314), T295, T296))
U7_ag(T303, T295, T296, inA_out_ag(s(T303), T296)) → inA_out_ag(s(T303), tree(0, T295, T296))
U25_gag(T211, T217, T213, inA_out_ag(T217, T213)) → pD_out_gag(T211, T217, T213)
U3_ag(T214, T211, T212, T213, pD_out_gag(T211, T214, T213)) → inA_out_ag(T214, tree(T211, T212, T213))

The argument filtering Pi contains the following mapping:
inA_in_ag(x1, x2)  =  inA_in_ag(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
inA_out_ag(x1, x2)  =  inA_out_ag(x1, x2)
s(x1)  =  s(x1)
U1_ag(x1, x2, x3, x4)  =  U1_ag(x1, x2, x3, x4)
inB_in_g(x1)  =  inB_in_g(x1)
0  =  0
inB_out_g(x1)  =  inB_out_g(x1)
U9_g(x1, x2, x3, x4)  =  U9_g(x1, x2, x3, x4)
pF_in_gg(x1, x2)  =  pF_in_gg(x1, x2)
U16_gg(x1, x2, x3)  =  U16_gg(x1, x2, x3)
lessN_in_g(x1)  =  lessN_in_g(x1)
lessN_out_g(x1)  =  lessN_out_g(x1)
U17_gg(x1, x2, x3)  =  U17_gg(x1, x2, x3)
pF_out_gg(x1, x2)  =  pF_out_gg(x1, x2)
U2_ag(x1, x2, x3, x4, x5)  =  U2_ag(x2, x3, x4, x5)
pC_in_agg(x1, x2, x3)  =  pC_in_agg(x2, x3)
U18_agg(x1, x2, x3, x4)  =  U18_agg(x2, x3, x4)
lessH_in_ag(x1, x2)  =  lessH_in_ag(x2)
lessH_out_ag(x1, x2)  =  lessH_out_ag(x1, x2)
U10_ag(x1, x2, x3)  =  U10_ag(x2, x3)
U19_agg(x1, x2, x3, x4)  =  U19_agg(x1, x2, x3, x4)
inI_in_gg(x1, x2)  =  inI_in_gg(x1, x2)
inI_out_gg(x1, x2)  =  inI_out_gg(x1, x2)
U11_gg(x1, x2, x3, x4, x5)  =  U11_gg(x1, x2, x3, x4, x5)
pJ_in_ggg(x1, x2, x3)  =  pJ_in_ggg(x1, x2, x3)
U20_ggg(x1, x2, x3, x4)  =  U20_ggg(x1, x2, x3, x4)
lessO_in_gg(x1, x2)  =  lessO_in_gg(x1, x2)
U15_gg(x1, x2, x3)  =  U15_gg(x1, x2, x3)
lessL_in_gg(x1, x2)  =  lessL_in_gg(x1, x2)
lessL_out_gg(x1, x2)  =  lessL_out_gg(x1, x2)
U13_gg(x1, x2, x3)  =  U13_gg(x1, x2, x3)
lessO_out_gg(x1, x2)  =  lessO_out_gg(x1, x2)
U21_ggg(x1, x2, x3, x4)  =  U21_ggg(x1, x2, x3, x4)
U12_gg(x1, x2, x3, x4, x5)  =  U12_gg(x1, x2, x3, x4, x5)
pK_in_ggg(x1, x2, x3)  =  pK_in_ggg(x1, x2, x3)
U22_ggg(x1, x2, x3, x4)  =  U22_ggg(x1, x2, x3, x4)
U23_ggg(x1, x2, x3, x4)  =  U23_ggg(x1, x2, x3, x4)
pK_out_ggg(x1, x2, x3)  =  pK_out_ggg(x1, x2, x3)
pJ_out_ggg(x1, x2, x3)  =  pJ_out_ggg(x1, x2, x3)
pC_out_agg(x1, x2, x3)  =  pC_out_agg(x1, x2, x3)
U3_ag(x1, x2, x3, x4, x5)  =  U3_ag(x2, x3, x4, x5)
pD_in_gag(x1, x2, x3)  =  pD_in_gag(x1, x3)
U24_gag(x1, x2, x3, x4)  =  U24_gag(x1, x3, x4)
lessM_in_ga(x1, x2)  =  lessM_in_ga(x1)
lessM_out_ga(x1, x2)  =  lessM_out_ga(x1)
U14_ga(x1, x2, x3)  =  U14_ga(x1, x3)
U25_gag(x1, x2, x3, x4)  =  U25_gag(x1, x3, x4)
U4_ag(x1, x2, x3, x4)  =  U4_ag(x1, x2, x3, x4)
U5_ag(x1, x2, x3, x4, x5)  =  U5_ag(x2, x3, x4, x5)
U6_ag(x1, x2, x3, x4, x5)  =  U6_ag(x2, x3, x4, x5)
pD_out_gag(x1, x2, x3)  =  pD_out_gag(x1, x2, x3)
U7_ag(x1, x2, x3, x4)  =  U7_ag(x2, x3, x4)
U8_ag(x1, x2, x3, x4, x5)  =  U8_ag(x2, x3, x4, x5)
pE_in_gag(x1, x2, x3)  =  pE_in_gag(x1, x3)
U26_gag(x1, x2, x3, x4)  =  U26_gag(x1, x3, x4)
U27_gag(x1, x2, x3, x4)  =  U27_gag(x1, x3, x4)
pE_out_gag(x1, x2, x3)  =  pE_out_gag(x1, x2, x3)
INA_IN_AG(x1, x2)  =  INA_IN_AG(x2)
PD_IN_GAG(x1, x2, x3)  =  PD_IN_GAG(x1, x3)
U24_GAG(x1, x2, x3, x4)  =  U24_GAG(x1, x3, x4)
PE_IN_GAG(x1, x2, x3)  =  PE_IN_GAG(x1, x3)
U26_GAG(x1, x2, x3, x4)  =  U26_GAG(x1, x3, x4)

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

(43) UsableRulesProof (EQUIVALENT transformation)

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

(44) Obligation:

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

INA_IN_AG(T214, tree(T211, T212, T213)) → PD_IN_GAG(T211, T214, T213)
PD_IN_GAG(T211, T217, T213) → U24_GAG(T211, T217, T213, lessM_in_ga(T211, T217))
U24_GAG(T211, T217, T213, lessM_out_ga(T211, T217)) → INA_IN_AG(T217, T213)
INA_IN_AG(s(T303), tree(0, T295, T296)) → INA_IN_AG(s(T303), T296)
INA_IN_AG(s(T316), tree(s(T314), T295, T296)) → PE_IN_GAG(T314, T316, T296)
PE_IN_GAG(T314, T319, T296) → U26_GAG(T314, T319, T296, lessM_in_ga(T314, T319))
U26_GAG(T314, T319, T296, lessM_out_ga(T314, T319)) → INA_IN_AG(s(T319), T296)

The TRS R consists of the following rules:

lessM_in_ga(0, s(T224)) → lessM_out_ga(0, s(T224))
lessM_in_ga(s(T229), s(T231)) → U14_ga(T229, T231, lessM_in_ga(T229, T231))
U14_ga(T229, T231, lessM_out_ga(T229, T231)) → lessM_out_ga(s(T229), s(T231))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
0  =  0
lessM_in_ga(x1, x2)  =  lessM_in_ga(x1)
lessM_out_ga(x1, x2)  =  lessM_out_ga(x1)
U14_ga(x1, x2, x3)  =  U14_ga(x1, x3)
INA_IN_AG(x1, x2)  =  INA_IN_AG(x2)
PD_IN_GAG(x1, x2, x3)  =  PD_IN_GAG(x1, x3)
U24_GAG(x1, x2, x3, x4)  =  U24_GAG(x1, x3, x4)
PE_IN_GAG(x1, x2, x3)  =  PE_IN_GAG(x1, x3)
U26_GAG(x1, x2, x3, x4)  =  U26_GAG(x1, x3, x4)

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

(45) PiDPToQDPProof (SOUND transformation)

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

(46) Obligation:

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

INA_IN_AG(tree(T211, T212, T213)) → PD_IN_GAG(T211, T213)
PD_IN_GAG(T211, T213) → U24_GAG(T211, T213, lessM_in_ga(T211))
U24_GAG(T211, T213, lessM_out_ga(T211)) → INA_IN_AG(T213)
INA_IN_AG(tree(0, T295, T296)) → INA_IN_AG(T296)
INA_IN_AG(tree(s(T314), T295, T296)) → PE_IN_GAG(T314, T296)
PE_IN_GAG(T314, T296) → U26_GAG(T314, T296, lessM_in_ga(T314))
U26_GAG(T314, T296, lessM_out_ga(T314)) → INA_IN_AG(T296)

The TRS R consists of the following rules:

lessM_in_ga(0) → lessM_out_ga(0)
lessM_in_ga(s(T229)) → U14_ga(T229, lessM_in_ga(T229))
U14_ga(T229, lessM_out_ga(T229)) → lessM_out_ga(s(T229))

The set Q consists of the following terms:

lessM_in_ga(x0)
U14_ga(x0, x1)

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

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

• PD_IN_GAG(T211, T213) → U24_GAG(T211, T213, lessM_in_ga(T211))
  The graph contains the following edges 1 >= 1, 2 >= 2

• U24_GAG(T211, T213, lessM_out_ga(T211)) → INA_IN_AG(T213)
  The graph contains the following edges 2 >= 1

• INA_IN_AG(tree(T211, T212, T213)) → PD_IN_GAG(T211, T213)
  The graph contains the following edges 1 > 1, 1 > 2

• INA_IN_AG(tree(0, T295, T296)) → INA_IN_AG(T296)
  The graph contains the following edges 1 > 1

• U26_GAG(T314, T296, lessM_out_ga(T314)) → INA_IN_AG(T296)
  The graph contains the following edges 2 >= 1

• INA_IN_AG(tree(s(T314), T295, T296)) → PE_IN_GAG(T314, T296)
  The graph contains the following edges 1 > 1, 1 > 2

• PE_IN_GAG(T314, T296) → U26_GAG(T314, T296, lessM_in_ga(T314))
  The graph contains the following edges 1 >= 1, 2 >= 2

(48) YES