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

(0) Obligation:

Clauses:

inorder(nil, []).
inorder(tree(L, V, R), I) :- ','(inorder(L, LI), ','(inorder(R, RI), append(LI, .(V, RI), I))).
append([], X, X).
append(.(X, Xs), Ys, .(X, Zs)) :- append(Xs, Ys, Zs).

Query: inorder(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="A: inorder(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: inorder(T1, T2), SCOPE: 1, CLAUSE: 0 | inorder(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: true | inorder(nil, T2), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: inorder(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\ninorder(T1, T2) !=? inorder(nil, [])", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: inorder(nil, T2), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(inorder(T7, X13), ','(inorder(T9, X14), append(X13, .(T8, X14), T11)))\n\nT7 is ground\nT8 is ground\nT9 is ground\nX13 is free\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(inorder(T7, X13), ','(inorder(T9, X14), append(X13, .(T8, X14), T11))), SCOPE: 2, CLAUSE: 0 | ','(inorder(T7, X13), ','(inorder(T9, X14), append(X13, .(T8, X14), T11))), SCOPE: 2, CLAUSE: 1\n\nT7 is ground\nT8 is ground\nT9 is ground\nX13 is free\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(inorder(T7, X13), ','(inorder(T9, X14), append(X13, .(T8, X14), T11))), SCOPE: 2, CLAUSE: 0\n\nT7 is ground\nT8 is ground\nT9 is ground\nX13 is free\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(inorder(T7, X13), ','(inorder(T9, X14), append(X13, .(T8, X14), T11))), SCOPE: 2, CLAUSE: 1\n\nT7 is ground\nT8 is ground\nT9 is ground\nX13 is free\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="B: ','(inorder(T9, X14), append([], .(T8, X14), T11))\n\nT8 is ground\nT9 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="D: inorder(T9, X14)\n\nT9 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="H: append([], .(T8, T12), T11)\n\nT8 is ground\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: inorder(T9, X14), SCOPE: 3, CLAUSE: 0 | inorder(T9, X14), SCOPE: 3, CLAUSE: 1\n\nT9 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: inorder(T9, X14), SCOPE: 3, CLAUSE: 0\n\nT9 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: inorder(T9, X14), SCOPE: 3, CLAUSE: 1\n\nT9 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="E: ','(inorder(T19, X31), ','(inorder(T21, X32), append(X31, .(T20, X32), X33)))\n\nT19 is ground\nT20 is ground\nT21 is ground\nX33 is free\nX31 is free\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: inorder(T19, X31)\n\nT19 is ground\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="I: ','(inorder(T21, X32), append(T22, .(T20, X32), X33))\n\nT20 is ground\nT21 is ground\nT22 is ground\nX33 is free\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: inorder(T21, X32)\n\nT21 is ground\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="F: append(T22, .(T20, T23), X33)\n\nT20 is ground\nT22 is ground\nT23 is ground\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: append(T22, .(T20, T23), X33), SCOPE: 4, CLAUSE: 2 | append(T22, .(T20, T23), X33), SCOPE: 4, CLAUSE: 3\n\nT20 is ground\nT22 is ground\nT23 is ground\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: append(T22, .(T20, T23), X33), SCOPE: 4, CLAUSE: 2\n\nT20 is ground\nT22 is ground\nT23 is ground\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: append(T22, .(T20, T23), X33), SCOPE: 4, CLAUSE: 3\n\nT20 is ground\nT22 is ground\nT23 is ground\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: append(T47, .(T48, T49), X55)\n\nT47 is ground\nT48 is ground\nT49 is ground\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: append([], .(T8, T12), T11), SCOPE: 5, CLAUSE: 2 | append([], .(T8, T12), T11), SCOPE: 5, CLAUSE: 3\n\nT8 is ground\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: append([], .(T8, T12), T11), SCOPE: 5, CLAUSE: 2\n\nT8 is ground\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: append([], .(T8, T12), T11), SCOPE: 5, CLAUSE: 3\n\nT8 is ground\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="C: ','(','(inorder(T74, X85), ','(inorder(T76, X86), append(X85, .(T75, X86), X87))), ','(inorder(T9, X14), append(X87, .(T8, X14), T11)))\n\nT8 is ground\nT9 is ground\nT74 is ground\nT75 is ground\nT76 is ground\nX14 is free\nX87 is free\nX85 is free\nX86 is free", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: inorder(T74, X85)\n\nT74 is ground\nX85 is free", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="J: ','(','(inorder(T76, X86), append(T77, .(T75, X86), X87)), ','(inorder(T9, X14), append(X87, .(T8, X14), T11)))\n\nT8 is ground\nT9 is ground\nT75 is ground\nT76 is ground\nT77 is ground\nX14 is free\nX87 is free\nX86 is free", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: inorder(T76, X86)\n\nT76 is ground\nX86 is free", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="K: ','(append(T77, .(T75, T78), X87), ','(inorder(T9, X14), append(X87, .(T8, X14), T11)))\n\nT8 is ground\nT9 is ground\nT75 is ground\nT77 is ground\nT78 is ground\nX14 is free\nX87 is free", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: append(T77, .(T75, T78), X87)\n\nT75 is ground\nT77 is ground\nT78 is ground\nX87 is free", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="L: ','(inorder(T9, X14), append(T83, .(T8, X14), T11))\n\nT8 is ground\nT9 is ground\nT83 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: inorder(T9, X14)\n\nT9 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="G: append(T83, .(T8, T88), T11)\n\nT8 is ground\nT83 is ground\nT88 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: append(T83, .(T8, T88), T11), SCOPE: 6, CLAUSE: 2 | append(T83, .(T8, T88), T11), SCOPE: 6, CLAUSE: 3\n\nT8 is ground\nT83 is ground\nT88 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: append(T83, .(T8, T88), T11), SCOPE: 6, CLAUSE: 2\n\nT8 is ground\nT83 is ground\nT88 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: append(T83, .(T8, T88), T11), SCOPE: 6, CLAUSE: 3\n\nT8 is ground\nT83 is ground\nT88 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: append(T114, .(T115, T116), T118)\n\nT114 is ground\nT115 is ground\nT116 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 162 [arrowhead = none ];
162 -> 4;

163 [label="EVAL with clause\ninorder(nil, []).\nand substitutionT1 -> nil,\nT2 -> []", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 163 [arrowhead = none ];
163 -> 11;

164 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
4 -> 164 [arrowhead = none ];
164 -> 14;

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

166 [label="EVAL with clause\ninorder(tree(X9, X10, X11), X12) :- ','(inorder(X9, X13), ','(inorder(X11, X14), append(X13, .(X10, X14), X12))).\nand substitutionX9 -> T7,\nX10 -> T8,\nX11 -> T9,\nT1 -> tree(T7, T8, T9),\nT2 -> T11,\nX12 -> T11,\nT10 -> T11", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 166 [arrowhead = none ];
166 -> 23;

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

168 [label="BACKTRACK\nfor clause: inorder(tree(L, V, R), I) :- ','(inorder(L, LI), ','(inorder(R, RI), append(LI, .(V, RI), I)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 168 [arrowhead = none ];
168 -> 19;

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

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

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

172 [label="EVAL with clause\ninorder(nil, []).\nand substitutionT7 -> nil,\nX13 -> []", fontsize=14, style = filled, fillcolor = lightblue];
29 -> 172 [arrowhead = none ];
172 -> 33;

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

174 [label="EVAL with clause\ninorder(tree(X81, X82, X83), X84) :- ','(inorder(X81, X85), ','(inorder(X83, X86), append(X85, .(X82, X86), X84))).\nand substitutionX81 -> T74,\nX82 -> T75,\nX83 -> T76,\nT7 -> tree(T74, T75, T76),\nX13 -> X87,\nX84 -> X87", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 174 [arrowhead = none ];
174 -> 116;

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

176 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
33 -> 176 [arrowhead = none ];
176 -> 37;

177 [label="SPLIT 2\nnew knowledge:\nT9 is ground\nT12 is ground\nreplacements:X14 -> T12", fontsize=14, style = filled, fillcolor = violet];
33 -> 177 [arrowhead = none ];
177 -> 40;

178 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
37 -> 178 [arrowhead = none ];
178 -> 43;

179 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
40 -> 179 [arrowhead = none ];
179 -> 96;

180 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
43 -> 180 [arrowhead = none ];
180 -> 47;

181 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
43 -> 181 [arrowhead = none ];
181 -> 49;

182 [label="EVAL with clause\ninorder(nil, []).\nand substitutionT9 -> nil,\nX14 -> []", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 182 [arrowhead = none ];
182 -> 52;

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

184 [label="EVAL with clause\ninorder(tree(X27, X28, X29), X30) :- ','(inorder(X27, X31), ','(inorder(X29, X32), append(X31, .(X28, X32), X30))).\nand substitutionX27 -> T19,\nX28 -> T20,\nX29 -> T21,\nT9 -> tree(T19, T20, T21),\nX14 -> X33,\nX30 -> X33", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 184 [arrowhead = none ];
184 -> 61;

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

186 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
52 -> 186 [arrowhead = none ];
186 -> 58;

187 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
61 -> 187 [arrowhead = none ];
187 -> 65;

188 [label="SPLIT 2\nnew knowledge:\nT19 is ground\nT22 is ground\nreplacements:X31 -> T22", fontsize=14, style = filled, fillcolor = violet];
61 -> 188 [arrowhead = none ];
188 -> 67;

189 [label="INSTANCE with matching:\nT9 -> T19\nX14 -> X31", fontsize=14, style = filled, fillcolor = lightgrey];
65 -> 189 [arrowhead = none , style=dashed];
189 -> 37[style=dashed];

190 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
67 -> 190 [arrowhead = none ];
190 -> 73;

191 [label="SPLIT 2\nnew knowledge:\nT21 is ground\nT23 is ground\nreplacements:X32 -> T23", fontsize=14, style = filled, fillcolor = violet];
67 -> 191 [arrowhead = none ];
191 -> 75;

192 [label="INSTANCE with matching:\nT9 -> T21\nX14 -> X32", fontsize=14, style = filled, fillcolor = lightgrey];
73 -> 192 [arrowhead = none , style=dashed];
192 -> 37[style=dashed];

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

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

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

196 [label="EVAL with clause\nappend([], X40, X40).\nand substitutionT22 -> [],\nT20 -> T36,\nT23 -> T37,\nX40 -> .(T36, T37),\nX33 -> .(T36, T37)", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 196 [arrowhead = none ];
196 -> 82;

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

198 [label="EVAL with clause\nappend(.(X51, X52), X53, .(X51, X54)) :- append(X52, X53, X54).\nand substitutionX51 -> T46,\nX52 -> T47,\nT22 -> .(T46, T47),\nT20 -> T48,\nT23 -> T49,\nX53 -> .(T48, T49),\nX54 -> X55,\nX33 -> .(T46, X55)", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 198 [arrowhead = none ];
198 -> 92;

199 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
80 -> 199 [arrowhead = none ];
199 -> 94;

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

201 [label="INSTANCE with matching:\nT22 -> T47\nT20 -> T48\nT23 -> T49\nX33 -> X55", fontsize=14, style = filled, fillcolor = lightgrey];
92 -> 201 [arrowhead = none , style=dashed];
201 -> 75[style=dashed];

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

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

204 [label="EVAL with clause\nappend([], X64, X64).\nand substitutionT8 -> T66,\nT12 -> T67,\nX64 -> .(T66, T67),\nT11 -> .(T66, T67)", fontsize=14, style = filled, fillcolor = lightblue];
101 -> 204 [arrowhead = none ];
204 -> 108;

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

206 [label="BACKTRACK\nfor clause: append(.(X, Xs), Ys, .(X, Zs)) :- append(Xs, Ys, Zs)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
102 -> 206 [arrowhead = none ];
206 -> 113;

207 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
108 -> 207 [arrowhead = none ];
207 -> 111;

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

209 [label="SPLIT 2\nnew knowledge:\nT74 is ground\nT77 is ground\nreplacements:X85 -> T77", fontsize=14, style = filled, fillcolor = violet];
116 -> 209 [arrowhead = none ];
209 -> 121;

210 [label="INSTANCE with matching:\nT9 -> T74\nX14 -> X85", fontsize=14, style = filled, fillcolor = lightgrey];
120 -> 210 [arrowhead = none , style=dashed];
210 -> 37[style=dashed];

211 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
121 -> 211 [arrowhead = none ];
211 -> 126;

212 [label="SPLIT 2\nnew knowledge:\nT76 is ground\nT78 is ground\nreplacements:X86 -> T78", fontsize=14, style = filled, fillcolor = violet];
121 -> 212 [arrowhead = none ];
212 -> 127;

213 [label="INSTANCE with matching:\nT9 -> T76\nX14 -> X86", fontsize=14, style = filled, fillcolor = lightgrey];
126 -> 213 [arrowhead = none , style=dashed];
213 -> 37[style=dashed];

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

215 [label="SPLIT 2\nnew knowledge:\nT77 is ground\nT75 is ground\nT78 is ground\nT83 is ground\nreplacements:X87 -> T83", fontsize=14, style = filled, fillcolor = violet];
127 -> 215 [arrowhead = none ];
215 -> 133;

216 [label="INSTANCE with matching:\nT22 -> T77\nT20 -> T75\nT23 -> T78\nX33 -> X87", fontsize=14, style = filled, fillcolor = lightgrey];
132 -> 216 [arrowhead = none , style=dashed];
216 -> 75[style=dashed];

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

218 [label="SPLIT 2\nnew knowledge:\nT9 is ground\nT88 is ground\nreplacements:X14 -> T88", fontsize=14, style = filled, fillcolor = violet];
133 -> 218 [arrowhead = none ];
218 -> 137;

219 [label="INSTANCE", fontsize=14, style = filled, fillcolor = lightgrey];
136 -> 219 [arrowhead = none , style=dashed];
219 -> 37[style=dashed];

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

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

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

223 [label="EVAL with clause\nappend([], X98, X98).\nand substitutionT83 -> [],\nT8 -> T101,\nT88 -> T102,\nX98 -> .(T101, T102),\nT11 -> .(T101, T102)", fontsize=14, style = filled, fillcolor = lightblue];
148 -> 223 [arrowhead = none ];
223 -> 155;

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

225 [label="EVAL with clause\nappend(.(X107, X108), X109, .(X107, X110)) :- append(X108, X109, X110).\nand substitutionX107 -> T113,\nX108 -> T114,\nT83 -> .(T113, T114),\nT8 -> T115,\nT88 -> T116,\nX109 -> .(T115, T116),\nX110 -> T118,\nT11 -> .(T113, T118),\nT117 -> T118", fontsize=14, style = filled, fillcolor = lightblue];
149 -> 225 [arrowhead = none ];
225 -> 160;

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

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

228 [label="INSTANCE with matching:\nT83 -> T114\nT8 -> T115\nT88 -> T116\nT11 -> T118", fontsize=14, style = filled, fillcolor = lightgrey];
160 -> 228 [arrowhead = none , style=dashed];
228 -> 137[style=dashed];

}

(2) Obligation:

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

inorderA_in_ga(nil, []) → inorderA_out_ga(nil, [])
inorderA_in_ga(tree(nil, T8, T9), T11) → U1_ga(T8, T9, T11, pB_in_gaga(T9, X14, T8, T11))
pB_in_gaga(T9, T12, T8, T11) → U6_gaga(T9, T12, T8, T11, inorderD_in_ga(T9, T12))
inorderD_in_ga(nil, []) → inorderD_out_ga(nil, [])
inorderD_in_ga(tree(T19, T20, T21), X33) → U3_ga(T19, T20, T21, X33, pE_in_gagaga(T19, X31, T21, X32, T20, X33))
pE_in_gagaga(T19, T22, T21, X32, T20, X33) → U8_gagaga(T19, T22, T21, X32, T20, X33, inorderD_in_ga(T19, T22))
U8_gagaga(T19, T22, T21, X32, T20, X33, inorderD_out_ga(T19, T22)) → U9_gagaga(T19, T22, T21, X32, T20, X33, pI_in_gagga(T21, X32, T22, T20, X33))
pI_in_gagga(T21, T23, T22, T20, X33) → U10_gagga(T21, T23, T22, T20, X33, inorderD_in_ga(T21, T23))
U10_gagga(T21, T23, T22, T20, X33, inorderD_out_ga(T21, T23)) → U11_gagga(T21, T23, T22, T20, X33, appendF_in_ggga(T22, T20, T23, X33))
appendF_in_ggga([], T36, T37, .(T36, T37)) → appendF_out_ggga([], T36, T37, .(T36, T37))
appendF_in_ggga(.(T46, T47), T48, T49, .(T46, X55)) → U4_ggga(T46, T47, T48, T49, X55, appendF_in_ggga(T47, T48, T49, X55))
U4_ggga(T46, T47, T48, T49, X55, appendF_out_ggga(T47, T48, T49, X55)) → appendF_out_ggga(.(T46, T47), T48, T49, .(T46, X55))
U11_gagga(T21, T23, T22, T20, X33, appendF_out_ggga(T22, T20, T23, X33)) → pI_out_gagga(T21, T23, T22, T20, X33)
U9_gagaga(T19, T22, T21, X32, T20, X33, pI_out_gagga(T21, X32, T22, T20, X33)) → pE_out_gagaga(T19, T22, T21, X32, T20, X33)
U3_ga(T19, T20, T21, X33, pE_out_gagaga(T19, X31, T21, X32, T20, X33)) → inorderD_out_ga(tree(T19, T20, T21), X33)
U6_gaga(T9, T12, T8, T11, inorderD_out_ga(T9, T12)) → U7_gaga(T9, T12, T8, T11, appendH_in_gga(T8, T12, T11))
appendH_in_gga(T66, T67, .(T66, T67)) → appendH_out_gga(T66, T67, .(T66, T67))
U7_gaga(T9, T12, T8, T11, appendH_out_gga(T8, T12, T11)) → pB_out_gaga(T9, T12, T8, T11)
U1_ga(T8, T9, T11, pB_out_gaga(T9, X14, T8, T11)) → inorderA_out_ga(tree(nil, T8, T9), T11)
inorderA_in_ga(tree(tree(T74, T75, T76), T8, T9), T11) → U2_ga(T74, T75, T76, T8, T9, T11, pC_in_gagagagaga(T74, X85, T76, X86, T75, X87, T9, X14, T8, T11))
pC_in_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11) → U12_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, inorderD_in_ga(T74, T77))
U12_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, inorderD_out_ga(T74, T77)) → U13_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, pJ_in_gaggagaga(T76, X86, T77, T75, X87, T9, X14, T8, T11))
pJ_in_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11) → U14_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11, inorderD_in_ga(T76, T78))
U14_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11, inorderD_out_ga(T76, T78)) → U15_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11, pK_in_gggagaga(T77, T75, T78, X87, T9, X14, T8, T11))
pK_in_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11) → U16_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11, appendF_in_ggga(T77, T75, T78, T83))
U16_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11, appendF_out_ggga(T77, T75, T78, T83)) → U17_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11, pL_in_gagga(T9, X14, T83, T8, T11))
pL_in_gagga(T9, T88, T83, T8, T11) → U18_gagga(T9, T88, T83, T8, T11, inorderD_in_ga(T9, T88))
U18_gagga(T9, T88, T83, T8, T11, inorderD_out_ga(T9, T88)) → U19_gagga(T9, T88, T83, T8, T11, appendG_in_ggga(T83, T8, T88, T11))
appendG_in_ggga([], T101, T102, .(T101, T102)) → appendG_out_ggga([], T101, T102, .(T101, T102))
appendG_in_ggga(.(T113, T114), T115, T116, .(T113, T118)) → U5_ggga(T113, T114, T115, T116, T118, appendG_in_ggga(T114, T115, T116, T118))
U5_ggga(T113, T114, T115, T116, T118, appendG_out_ggga(T114, T115, T116, T118)) → appendG_out_ggga(.(T113, T114), T115, T116, .(T113, T118))
U19_gagga(T9, T88, T83, T8, T11, appendG_out_ggga(T83, T8, T88, T11)) → pL_out_gagga(T9, T88, T83, T8, T11)
U17_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11, pL_out_gagga(T9, X14, T83, T8, T11)) → pK_out_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11)
U15_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11, pK_out_gggagaga(T77, T75, T78, X87, T9, X14, T8, T11)) → pJ_out_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11)
U13_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, pJ_out_gaggagaga(T76, X86, T77, T75, X87, T9, X14, T8, T11)) → pC_out_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11)
U2_ga(T74, T75, T76, T8, T9, T11, pC_out_gagagagaga(T74, X85, T76, X86, T75, X87, T9, X14, T8, T11)) → inorderA_out_ga(tree(tree(T74, T75, T76), T8, T9), T11)

The argument filtering Pi contains the following mapping:
inorderA_in_ga(x1, x2)  =  inorderA_in_ga(x1)
nil  =  nil
inorderA_out_ga(x1, x2)  =  inorderA_out_ga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x2, x4)
pB_in_gaga(x1, x2, x3, x4)  =  pB_in_gaga(x1, x3)
U6_gaga(x1, x2, x3, x4, x5)  =  U6_gaga(x1, x3, x5)
inorderD_in_ga(x1, x2)  =  inorderD_in_ga(x1)
inorderD_out_ga(x1, x2)  =  inorderD_out_ga(x1, x2)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x2, x3, x5)
pE_in_gagaga(x1, x2, x3, x4, x5, x6)  =  pE_in_gagaga(x1, x3, x5)
U8_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U8_gagaga(x1, x3, x5, x7)
U9_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U9_gagaga(x1, x2, x3, x5, x7)
pI_in_gagga(x1, x2, x3, x4, x5)  =  pI_in_gagga(x1, x3, x4)
U10_gagga(x1, x2, x3, x4, x5, x6)  =  U10_gagga(x1, x3, x4, x6)
U11_gagga(x1, x2, x3, x4, x5, x6)  =  U11_gagga(x1, x2, x3, x4, x6)
appendF_in_ggga(x1, x2, x3, x4)  =  appendF_in_ggga(x1, x2, x3)
[]  =  []
appendF_out_ggga(x1, x2, x3, x4)  =  appendF_out_ggga(x1, x2, x3, x4)
.(x1, x2)  =  .(x1, x2)
U4_ggga(x1, x2, x3, x4, x5, x6)  =  U4_ggga(x1, x2, x3, x4, x6)
pI_out_gagga(x1, x2, x3, x4, x5)  =  pI_out_gagga(x1, x2, x3, x4, x5)
pE_out_gagaga(x1, x2, x3, x4, x5, x6)  =  pE_out_gagaga(x1, x2, x3, x4, x5, x6)
U7_gaga(x1, x2, x3, x4, x5)  =  U7_gaga(x1, x2, x3, x5)
appendH_in_gga(x1, x2, x3)  =  appendH_in_gga(x1, x2)
appendH_out_gga(x1, x2, x3)  =  appendH_out_gga(x1, x2, x3)
pB_out_gaga(x1, x2, x3, x4)  =  pB_out_gaga(x1, x2, x3, x4)
U2_ga(x1, x2, x3, x4, x5, x6, x7)  =  U2_ga(x1, x2, x3, x4, x5, x7)
pC_in_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  pC_in_gagagagaga(x1, x3, x5, x7, x9)
U12_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U12_gagagagaga(x1, x3, x5, x7, x9, x11)
U13_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U13_gagagagaga(x1, x2, x3, x5, x7, x9, x11)
pJ_in_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  pJ_in_gaggagaga(x1, x3, x4, x6, x8)
U14_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U14_gaggagaga(x1, x3, x4, x6, x8, x10)
U15_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U15_gaggagaga(x1, x2, x3, x4, x6, x8, x10)
pK_in_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8)  =  pK_in_gggagaga(x1, x2, x3, x5, x7)
U16_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U16_gggagaga(x1, x2, x3, x5, x7, x9)
U17_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U17_gggagaga(x1, x2, x3, x4, x5, x7, x9)
pL_in_gagga(x1, x2, x3, x4, x5)  =  pL_in_gagga(x1, x3, x4)
U18_gagga(x1, x2, x3, x4, x5, x6)  =  U18_gagga(x1, x3, x4, x6)
U19_gagga(x1, x2, x3, x4, x5, x6)  =  U19_gagga(x1, x2, x3, x4, x6)
appendG_in_ggga(x1, x2, x3, x4)  =  appendG_in_ggga(x1, x2, x3)
appendG_out_ggga(x1, x2, x3, x4)  =  appendG_out_ggga(x1, x2, x3, x4)
U5_ggga(x1, x2, x3, x4, x5, x6)  =  U5_ggga(x1, x2, x3, x4, x6)
pL_out_gagga(x1, x2, x3, x4, x5)  =  pL_out_gagga(x1, x2, x3, x4, x5)
pK_out_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8)  =  pK_out_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8)
pJ_out_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  pJ_out_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)
pC_out_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  pC_out_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)

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

INORDERA_IN_GA(tree(nil, T8, T9), T11) → U1_GA(T8, T9, T11, pB_in_gaga(T9, X14, T8, T11))
INORDERA_IN_GA(tree(nil, T8, T9), T11) → PB_IN_GAGA(T9, X14, T8, T11)
PB_IN_GAGA(T9, T12, T8, T11) → U6_GAGA(T9, T12, T8, T11, inorderD_in_ga(T9, T12))
PB_IN_GAGA(T9, T12, T8, T11) → INORDERD_IN_GA(T9, T12)
INORDERD_IN_GA(tree(T19, T20, T21), X33) → U3_GA(T19, T20, T21, X33, pE_in_gagaga(T19, X31, T21, X32, T20, X33))
INORDERD_IN_GA(tree(T19, T20, T21), X33) → PE_IN_GAGAGA(T19, X31, T21, X32, T20, X33)
PE_IN_GAGAGA(T19, T22, T21, X32, T20, X33) → U8_GAGAGA(T19, T22, T21, X32, T20, X33, inorderD_in_ga(T19, T22))
PE_IN_GAGAGA(T19, T22, T21, X32, T20, X33) → INORDERD_IN_GA(T19, T22)
U8_GAGAGA(T19, T22, T21, X32, T20, X33, inorderD_out_ga(T19, T22)) → U9_GAGAGA(T19, T22, T21, X32, T20, X33, pI_in_gagga(T21, X32, T22, T20, X33))
U8_GAGAGA(T19, T22, T21, X32, T20, X33, inorderD_out_ga(T19, T22)) → PI_IN_GAGGA(T21, X32, T22, T20, X33)
PI_IN_GAGGA(T21, T23, T22, T20, X33) → U10_GAGGA(T21, T23, T22, T20, X33, inorderD_in_ga(T21, T23))
PI_IN_GAGGA(T21, T23, T22, T20, X33) → INORDERD_IN_GA(T21, T23)
U10_GAGGA(T21, T23, T22, T20, X33, inorderD_out_ga(T21, T23)) → U11_GAGGA(T21, T23, T22, T20, X33, appendF_in_ggga(T22, T20, T23, X33))
U10_GAGGA(T21, T23, T22, T20, X33, inorderD_out_ga(T21, T23)) → APPENDF_IN_GGGA(T22, T20, T23, X33)
APPENDF_IN_GGGA(.(T46, T47), T48, T49, .(T46, X55)) → U4_GGGA(T46, T47, T48, T49, X55, appendF_in_ggga(T47, T48, T49, X55))
APPENDF_IN_GGGA(.(T46, T47), T48, T49, .(T46, X55)) → APPENDF_IN_GGGA(T47, T48, T49, X55)
U6_GAGA(T9, T12, T8, T11, inorderD_out_ga(T9, T12)) → U7_GAGA(T9, T12, T8, T11, appendH_in_gga(T8, T12, T11))
U6_GAGA(T9, T12, T8, T11, inorderD_out_ga(T9, T12)) → APPENDH_IN_GGA(T8, T12, T11)
INORDERA_IN_GA(tree(tree(T74, T75, T76), T8, T9), T11) → U2_GA(T74, T75, T76, T8, T9, T11, pC_in_gagagagaga(T74, X85, T76, X86, T75, X87, T9, X14, T8, T11))
INORDERA_IN_GA(tree(tree(T74, T75, T76), T8, T9), T11) → PC_IN_GAGAGAGAGA(T74, X85, T76, X86, T75, X87, T9, X14, T8, T11)
PC_IN_GAGAGAGAGA(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11) → U12_GAGAGAGAGA(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, inorderD_in_ga(T74, T77))
PC_IN_GAGAGAGAGA(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11) → INORDERD_IN_GA(T74, T77)
U12_GAGAGAGAGA(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, inorderD_out_ga(T74, T77)) → U13_GAGAGAGAGA(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, pJ_in_gaggagaga(T76, X86, T77, T75, X87, T9, X14, T8, T11))
U12_GAGAGAGAGA(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, inorderD_out_ga(T74, T77)) → PJ_IN_GAGGAGAGA(T76, X86, T77, T75, X87, T9, X14, T8, T11)
PJ_IN_GAGGAGAGA(T76, T78, T77, T75, X87, T9, X14, T8, T11) → U14_GAGGAGAGA(T76, T78, T77, T75, X87, T9, X14, T8, T11, inorderD_in_ga(T76, T78))
PJ_IN_GAGGAGAGA(T76, T78, T77, T75, X87, T9, X14, T8, T11) → INORDERD_IN_GA(T76, T78)
U14_GAGGAGAGA(T76, T78, T77, T75, X87, T9, X14, T8, T11, inorderD_out_ga(T76, T78)) → U15_GAGGAGAGA(T76, T78, T77, T75, X87, T9, X14, T8, T11, pK_in_gggagaga(T77, T75, T78, X87, T9, X14, T8, T11))
U14_GAGGAGAGA(T76, T78, T77, T75, X87, T9, X14, T8, T11, inorderD_out_ga(T76, T78)) → PK_IN_GGGAGAGA(T77, T75, T78, X87, T9, X14, T8, T11)
PK_IN_GGGAGAGA(T77, T75, T78, T83, T9, X14, T8, T11) → U16_GGGAGAGA(T77, T75, T78, T83, T9, X14, T8, T11, appendF_in_ggga(T77, T75, T78, T83))
PK_IN_GGGAGAGA(T77, T75, T78, T83, T9, X14, T8, T11) → APPENDF_IN_GGGA(T77, T75, T78, T83)
U16_GGGAGAGA(T77, T75, T78, T83, T9, X14, T8, T11, appendF_out_ggga(T77, T75, T78, T83)) → U17_GGGAGAGA(T77, T75, T78, T83, T9, X14, T8, T11, pL_in_gagga(T9, X14, T83, T8, T11))
U16_GGGAGAGA(T77, T75, T78, T83, T9, X14, T8, T11, appendF_out_ggga(T77, T75, T78, T83)) → PL_IN_GAGGA(T9, X14, T83, T8, T11)
PL_IN_GAGGA(T9, T88, T83, T8, T11) → U18_GAGGA(T9, T88, T83, T8, T11, inorderD_in_ga(T9, T88))
PL_IN_GAGGA(T9, T88, T83, T8, T11) → INORDERD_IN_GA(T9, T88)
U18_GAGGA(T9, T88, T83, T8, T11, inorderD_out_ga(T9, T88)) → U19_GAGGA(T9, T88, T83, T8, T11, appendG_in_ggga(T83, T8, T88, T11))
U18_GAGGA(T9, T88, T83, T8, T11, inorderD_out_ga(T9, T88)) → APPENDG_IN_GGGA(T83, T8, T88, T11)
APPENDG_IN_GGGA(.(T113, T114), T115, T116, .(T113, T118)) → U5_GGGA(T113, T114, T115, T116, T118, appendG_in_ggga(T114, T115, T116, T118))
APPENDG_IN_GGGA(.(T113, T114), T115, T116, .(T113, T118)) → APPENDG_IN_GGGA(T114, T115, T116, T118)

The TRS R consists of the following rules:

inorderA_in_ga(nil, []) → inorderA_out_ga(nil, [])
inorderA_in_ga(tree(nil, T8, T9), T11) → U1_ga(T8, T9, T11, pB_in_gaga(T9, X14, T8, T11))
pB_in_gaga(T9, T12, T8, T11) → U6_gaga(T9, T12, T8, T11, inorderD_in_ga(T9, T12))
inorderD_in_ga(nil, []) → inorderD_out_ga(nil, [])
inorderD_in_ga(tree(T19, T20, T21), X33) → U3_ga(T19, T20, T21, X33, pE_in_gagaga(T19, X31, T21, X32, T20, X33))
pE_in_gagaga(T19, T22, T21, X32, T20, X33) → U8_gagaga(T19, T22, T21, X32, T20, X33, inorderD_in_ga(T19, T22))
U8_gagaga(T19, T22, T21, X32, T20, X33, inorderD_out_ga(T19, T22)) → U9_gagaga(T19, T22, T21, X32, T20, X33, pI_in_gagga(T21, X32, T22, T20, X33))
pI_in_gagga(T21, T23, T22, T20, X33) → U10_gagga(T21, T23, T22, T20, X33, inorderD_in_ga(T21, T23))
U10_gagga(T21, T23, T22, T20, X33, inorderD_out_ga(T21, T23)) → U11_gagga(T21, T23, T22, T20, X33, appendF_in_ggga(T22, T20, T23, X33))
appendF_in_ggga([], T36, T37, .(T36, T37)) → appendF_out_ggga([], T36, T37, .(T36, T37))
appendF_in_ggga(.(T46, T47), T48, T49, .(T46, X55)) → U4_ggga(T46, T47, T48, T49, X55, appendF_in_ggga(T47, T48, T49, X55))
U4_ggga(T46, T47, T48, T49, X55, appendF_out_ggga(T47, T48, T49, X55)) → appendF_out_ggga(.(T46, T47), T48, T49, .(T46, X55))
U11_gagga(T21, T23, T22, T20, X33, appendF_out_ggga(T22, T20, T23, X33)) → pI_out_gagga(T21, T23, T22, T20, X33)
U9_gagaga(T19, T22, T21, X32, T20, X33, pI_out_gagga(T21, X32, T22, T20, X33)) → pE_out_gagaga(T19, T22, T21, X32, T20, X33)
U3_ga(T19, T20, T21, X33, pE_out_gagaga(T19, X31, T21, X32, T20, X33)) → inorderD_out_ga(tree(T19, T20, T21), X33)
U6_gaga(T9, T12, T8, T11, inorderD_out_ga(T9, T12)) → U7_gaga(T9, T12, T8, T11, appendH_in_gga(T8, T12, T11))
appendH_in_gga(T66, T67, .(T66, T67)) → appendH_out_gga(T66, T67, .(T66, T67))
U7_gaga(T9, T12, T8, T11, appendH_out_gga(T8, T12, T11)) → pB_out_gaga(T9, T12, T8, T11)
U1_ga(T8, T9, T11, pB_out_gaga(T9, X14, T8, T11)) → inorderA_out_ga(tree(nil, T8, T9), T11)
inorderA_in_ga(tree(tree(T74, T75, T76), T8, T9), T11) → U2_ga(T74, T75, T76, T8, T9, T11, pC_in_gagagagaga(T74, X85, T76, X86, T75, X87, T9, X14, T8, T11))
pC_in_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11) → U12_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, inorderD_in_ga(T74, T77))
U12_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, inorderD_out_ga(T74, T77)) → U13_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, pJ_in_gaggagaga(T76, X86, T77, T75, X87, T9, X14, T8, T11))
pJ_in_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11) → U14_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11, inorderD_in_ga(T76, T78))
U14_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11, inorderD_out_ga(T76, T78)) → U15_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11, pK_in_gggagaga(T77, T75, T78, X87, T9, X14, T8, T11))
pK_in_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11) → U16_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11, appendF_in_ggga(T77, T75, T78, T83))
U16_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11, appendF_out_ggga(T77, T75, T78, T83)) → U17_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11, pL_in_gagga(T9, X14, T83, T8, T11))
pL_in_gagga(T9, T88, T83, T8, T11) → U18_gagga(T9, T88, T83, T8, T11, inorderD_in_ga(T9, T88))
U18_gagga(T9, T88, T83, T8, T11, inorderD_out_ga(T9, T88)) → U19_gagga(T9, T88, T83, T8, T11, appendG_in_ggga(T83, T8, T88, T11))
appendG_in_ggga([], T101, T102, .(T101, T102)) → appendG_out_ggga([], T101, T102, .(T101, T102))
appendG_in_ggga(.(T113, T114), T115, T116, .(T113, T118)) → U5_ggga(T113, T114, T115, T116, T118, appendG_in_ggga(T114, T115, T116, T118))
U5_ggga(T113, T114, T115, T116, T118, appendG_out_ggga(T114, T115, T116, T118)) → appendG_out_ggga(.(T113, T114), T115, T116, .(T113, T118))
U19_gagga(T9, T88, T83, T8, T11, appendG_out_ggga(T83, T8, T88, T11)) → pL_out_gagga(T9, T88, T83, T8, T11)
U17_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11, pL_out_gagga(T9, X14, T83, T8, T11)) → pK_out_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11)
U15_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11, pK_out_gggagaga(T77, T75, T78, X87, T9, X14, T8, T11)) → pJ_out_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11)
U13_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, pJ_out_gaggagaga(T76, X86, T77, T75, X87, T9, X14, T8, T11)) → pC_out_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11)
U2_ga(T74, T75, T76, T8, T9, T11, pC_out_gagagagaga(T74, X85, T76, X86, T75, X87, T9, X14, T8, T11)) → inorderA_out_ga(tree(tree(T74, T75, T76), T8, T9), T11)

The argument filtering Pi contains the following mapping:
inorderA_in_ga(x1, x2)  =  inorderA_in_ga(x1)
nil  =  nil
inorderA_out_ga(x1, x2)  =  inorderA_out_ga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x2, x4)
pB_in_gaga(x1, x2, x3, x4)  =  pB_in_gaga(x1, x3)
U6_gaga(x1, x2, x3, x4, x5)  =  U6_gaga(x1, x3, x5)
inorderD_in_ga(x1, x2)  =  inorderD_in_ga(x1)
inorderD_out_ga(x1, x2)  =  inorderD_out_ga(x1, x2)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x2, x3, x5)
pE_in_gagaga(x1, x2, x3, x4, x5, x6)  =  pE_in_gagaga(x1, x3, x5)
U8_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U8_gagaga(x1, x3, x5, x7)
U9_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U9_gagaga(x1, x2, x3, x5, x7)
pI_in_gagga(x1, x2, x3, x4, x5)  =  pI_in_gagga(x1, x3, x4)
U10_gagga(x1, x2, x3, x4, x5, x6)  =  U10_gagga(x1, x3, x4, x6)
U11_gagga(x1, x2, x3, x4, x5, x6)  =  U11_gagga(x1, x2, x3, x4, x6)
appendF_in_ggga(x1, x2, x3, x4)  =  appendF_in_ggga(x1, x2, x3)
[]  =  []
appendF_out_ggga(x1, x2, x3, x4)  =  appendF_out_ggga(x1, x2, x3, x4)
.(x1, x2)  =  .(x1, x2)
U4_ggga(x1, x2, x3, x4, x5, x6)  =  U4_ggga(x1, x2, x3, x4, x6)
pI_out_gagga(x1, x2, x3, x4, x5)  =  pI_out_gagga(x1, x2, x3, x4, x5)
pE_out_gagaga(x1, x2, x3, x4, x5, x6)  =  pE_out_gagaga(x1, x2, x3, x4, x5, x6)
U7_gaga(x1, x2, x3, x4, x5)  =  U7_gaga(x1, x2, x3, x5)
appendH_in_gga(x1, x2, x3)  =  appendH_in_gga(x1, x2)
appendH_out_gga(x1, x2, x3)  =  appendH_out_gga(x1, x2, x3)
pB_out_gaga(x1, x2, x3, x4)  =  pB_out_gaga(x1, x2, x3, x4)
U2_ga(x1, x2, x3, x4, x5, x6, x7)  =  U2_ga(x1, x2, x3, x4, x5, x7)
pC_in_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  pC_in_gagagagaga(x1, x3, x5, x7, x9)
U12_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U12_gagagagaga(x1, x3, x5, x7, x9, x11)
U13_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U13_gagagagaga(x1, x2, x3, x5, x7, x9, x11)
pJ_in_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  pJ_in_gaggagaga(x1, x3, x4, x6, x8)
U14_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U14_gaggagaga(x1, x3, x4, x6, x8, x10)
U15_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U15_gaggagaga(x1, x2, x3, x4, x6, x8, x10)
pK_in_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8)  =  pK_in_gggagaga(x1, x2, x3, x5, x7)
U16_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U16_gggagaga(x1, x2, x3, x5, x7, x9)
U17_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U17_gggagaga(x1, x2, x3, x4, x5, x7, x9)
pL_in_gagga(x1, x2, x3, x4, x5)  =  pL_in_gagga(x1, x3, x4)
U18_gagga(x1, x2, x3, x4, x5, x6)  =  U18_gagga(x1, x3, x4, x6)
U19_gagga(x1, x2, x3, x4, x5, x6)  =  U19_gagga(x1, x2, x3, x4, x6)
appendG_in_ggga(x1, x2, x3, x4)  =  appendG_in_ggga(x1, x2, x3)
appendG_out_ggga(x1, x2, x3, x4)  =  appendG_out_ggga(x1, x2, x3, x4)
U5_ggga(x1, x2, x3, x4, x5, x6)  =  U5_ggga(x1, x2, x3, x4, x6)
pL_out_gagga(x1, x2, x3, x4, x5)  =  pL_out_gagga(x1, x2, x3, x4, x5)
pK_out_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8)  =  pK_out_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8)
pJ_out_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  pJ_out_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)
pC_out_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  pC_out_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)
INORDERA_IN_GA(x1, x2)  =  INORDERA_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x1, x2, x4)
PB_IN_GAGA(x1, x2, x3, x4)  =  PB_IN_GAGA(x1, x3)
U6_GAGA(x1, x2, x3, x4, x5)  =  U6_GAGA(x1, x3, x5)
INORDERD_IN_GA(x1, x2)  =  INORDERD_IN_GA(x1)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x1, x2, x3, x5)
PE_IN_GAGAGA(x1, x2, x3, x4, x5, x6)  =  PE_IN_GAGAGA(x1, x3, x5)
U8_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U8_GAGAGA(x1, x3, x5, x7)
U9_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U9_GAGAGA(x1, x2, x3, x5, x7)
PI_IN_GAGGA(x1, x2, x3, x4, x5)  =  PI_IN_GAGGA(x1, x3, x4)
U10_GAGGA(x1, x2, x3, x4, x5, x6)  =  U10_GAGGA(x1, x3, x4, x6)
U11_GAGGA(x1, x2, x3, x4, x5, x6)  =  U11_GAGGA(x1, x2, x3, x4, x6)
APPENDF_IN_GGGA(x1, x2, x3, x4)  =  APPENDF_IN_GGGA(x1, x2, x3)
U4_GGGA(x1, x2, x3, x4, x5, x6)  =  U4_GGGA(x1, x2, x3, x4, x6)
U7_GAGA(x1, x2, x3, x4, x5)  =  U7_GAGA(x1, x2, x3, x5)
APPENDH_IN_GGA(x1, x2, x3)  =  APPENDH_IN_GGA(x1, x2)
U2_GA(x1, x2, x3, x4, x5, x6, x7)  =  U2_GA(x1, x2, x3, x4, x5, x7)
PC_IN_GAGAGAGAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  PC_IN_GAGAGAGAGA(x1, x3, x5, x7, x9)
U12_GAGAGAGAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U12_GAGAGAGAGA(x1, x3, x5, x7, x9, x11)
U13_GAGAGAGAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U13_GAGAGAGAGA(x1, x2, x3, x5, x7, x9, x11)
PJ_IN_GAGGAGAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  PJ_IN_GAGGAGAGA(x1, x3, x4, x6, x8)
U14_GAGGAGAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U14_GAGGAGAGA(x1, x3, x4, x6, x8, x10)
U15_GAGGAGAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U15_GAGGAGAGA(x1, x2, x3, x4, x6, x8, x10)
PK_IN_GGGAGAGA(x1, x2, x3, x4, x5, x6, x7, x8)  =  PK_IN_GGGAGAGA(x1, x2, x3, x5, x7)
U16_GGGAGAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U16_GGGAGAGA(x1, x2, x3, x5, x7, x9)
U17_GGGAGAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U17_GGGAGAGA(x1, x2, x3, x4, x5, x7, x9)
PL_IN_GAGGA(x1, x2, x3, x4, x5)  =  PL_IN_GAGGA(x1, x3, x4)
U18_GAGGA(x1, x2, x3, x4, x5, x6)  =  U18_GAGGA(x1, x3, x4, x6)
U19_GAGGA(x1, x2, x3, x4, x5, x6)  =  U19_GAGGA(x1, x2, x3, x4, x6)
APPENDG_IN_GGGA(x1, x2, x3, x4)  =  APPENDG_IN_GGGA(x1, x2, x3)
U5_GGGA(x1, x2, x3, x4, x5, x6)  =  U5_GGGA(x1, x2, x3, x4, x6)

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

(4) Obligation:

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

INORDERA_IN_GA(tree(nil, T8, T9), T11) → U1_GA(T8, T9, T11, pB_in_gaga(T9, X14, T8, T11))
INORDERA_IN_GA(tree(nil, T8, T9), T11) → PB_IN_GAGA(T9, X14, T8, T11)
PB_IN_GAGA(T9, T12, T8, T11) → U6_GAGA(T9, T12, T8, T11, inorderD_in_ga(T9, T12))
PB_IN_GAGA(T9, T12, T8, T11) → INORDERD_IN_GA(T9, T12)
INORDERD_IN_GA(tree(T19, T20, T21), X33) → U3_GA(T19, T20, T21, X33, pE_in_gagaga(T19, X31, T21, X32, T20, X33))
INORDERD_IN_GA(tree(T19, T20, T21), X33) → PE_IN_GAGAGA(T19, X31, T21, X32, T20, X33)
PE_IN_GAGAGA(T19, T22, T21, X32, T20, X33) → U8_GAGAGA(T19, T22, T21, X32, T20, X33, inorderD_in_ga(T19, T22))
PE_IN_GAGAGA(T19, T22, T21, X32, T20, X33) → INORDERD_IN_GA(T19, T22)
U8_GAGAGA(T19, T22, T21, X32, T20, X33, inorderD_out_ga(T19, T22)) → U9_GAGAGA(T19, T22, T21, X32, T20, X33, pI_in_gagga(T21, X32, T22, T20, X33))
U8_GAGAGA(T19, T22, T21, X32, T20, X33, inorderD_out_ga(T19, T22)) → PI_IN_GAGGA(T21, X32, T22, T20, X33)
PI_IN_GAGGA(T21, T23, T22, T20, X33) → U10_GAGGA(T21, T23, T22, T20, X33, inorderD_in_ga(T21, T23))
PI_IN_GAGGA(T21, T23, T22, T20, X33) → INORDERD_IN_GA(T21, T23)
U10_GAGGA(T21, T23, T22, T20, X33, inorderD_out_ga(T21, T23)) → U11_GAGGA(T21, T23, T22, T20, X33, appendF_in_ggga(T22, T20, T23, X33))
U10_GAGGA(T21, T23, T22, T20, X33, inorderD_out_ga(T21, T23)) → APPENDF_IN_GGGA(T22, T20, T23, X33)
APPENDF_IN_GGGA(.(T46, T47), T48, T49, .(T46, X55)) → U4_GGGA(T46, T47, T48, T49, X55, appendF_in_ggga(T47, T48, T49, X55))
APPENDF_IN_GGGA(.(T46, T47), T48, T49, .(T46, X55)) → APPENDF_IN_GGGA(T47, T48, T49, X55)
U6_GAGA(T9, T12, T8, T11, inorderD_out_ga(T9, T12)) → U7_GAGA(T9, T12, T8, T11, appendH_in_gga(T8, T12, T11))
U6_GAGA(T9, T12, T8, T11, inorderD_out_ga(T9, T12)) → APPENDH_IN_GGA(T8, T12, T11)
INORDERA_IN_GA(tree(tree(T74, T75, T76), T8, T9), T11) → U2_GA(T74, T75, T76, T8, T9, T11, pC_in_gagagagaga(T74, X85, T76, X86, T75, X87, T9, X14, T8, T11))
INORDERA_IN_GA(tree(tree(T74, T75, T76), T8, T9), T11) → PC_IN_GAGAGAGAGA(T74, X85, T76, X86, T75, X87, T9, X14, T8, T11)
PC_IN_GAGAGAGAGA(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11) → U12_GAGAGAGAGA(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, inorderD_in_ga(T74, T77))
PC_IN_GAGAGAGAGA(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11) → INORDERD_IN_GA(T74, T77)
U12_GAGAGAGAGA(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, inorderD_out_ga(T74, T77)) → U13_GAGAGAGAGA(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, pJ_in_gaggagaga(T76, X86, T77, T75, X87, T9, X14, T8, T11))
U12_GAGAGAGAGA(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, inorderD_out_ga(T74, T77)) → PJ_IN_GAGGAGAGA(T76, X86, T77, T75, X87, T9, X14, T8, T11)
PJ_IN_GAGGAGAGA(T76, T78, T77, T75, X87, T9, X14, T8, T11) → U14_GAGGAGAGA(T76, T78, T77, T75, X87, T9, X14, T8, T11, inorderD_in_ga(T76, T78))
PJ_IN_GAGGAGAGA(T76, T78, T77, T75, X87, T9, X14, T8, T11) → INORDERD_IN_GA(T76, T78)
U14_GAGGAGAGA(T76, T78, T77, T75, X87, T9, X14, T8, T11, inorderD_out_ga(T76, T78)) → U15_GAGGAGAGA(T76, T78, T77, T75, X87, T9, X14, T8, T11, pK_in_gggagaga(T77, T75, T78, X87, T9, X14, T8, T11))
U14_GAGGAGAGA(T76, T78, T77, T75, X87, T9, X14, T8, T11, inorderD_out_ga(T76, T78)) → PK_IN_GGGAGAGA(T77, T75, T78, X87, T9, X14, T8, T11)
PK_IN_GGGAGAGA(T77, T75, T78, T83, T9, X14, T8, T11) → U16_GGGAGAGA(T77, T75, T78, T83, T9, X14, T8, T11, appendF_in_ggga(T77, T75, T78, T83))
PK_IN_GGGAGAGA(T77, T75, T78, T83, T9, X14, T8, T11) → APPENDF_IN_GGGA(T77, T75, T78, T83)
U16_GGGAGAGA(T77, T75, T78, T83, T9, X14, T8, T11, appendF_out_ggga(T77, T75, T78, T83)) → U17_GGGAGAGA(T77, T75, T78, T83, T9, X14, T8, T11, pL_in_gagga(T9, X14, T83, T8, T11))
U16_GGGAGAGA(T77, T75, T78, T83, T9, X14, T8, T11, appendF_out_ggga(T77, T75, T78, T83)) → PL_IN_GAGGA(T9, X14, T83, T8, T11)
PL_IN_GAGGA(T9, T88, T83, T8, T11) → U18_GAGGA(T9, T88, T83, T8, T11, inorderD_in_ga(T9, T88))
PL_IN_GAGGA(T9, T88, T83, T8, T11) → INORDERD_IN_GA(T9, T88)
U18_GAGGA(T9, T88, T83, T8, T11, inorderD_out_ga(T9, T88)) → U19_GAGGA(T9, T88, T83, T8, T11, appendG_in_ggga(T83, T8, T88, T11))
U18_GAGGA(T9, T88, T83, T8, T11, inorderD_out_ga(T9, T88)) → APPENDG_IN_GGGA(T83, T8, T88, T11)
APPENDG_IN_GGGA(.(T113, T114), T115, T116, .(T113, T118)) → U5_GGGA(T113, T114, T115, T116, T118, appendG_in_ggga(T114, T115, T116, T118))
APPENDG_IN_GGGA(.(T113, T114), T115, T116, .(T113, T118)) → APPENDG_IN_GGGA(T114, T115, T116, T118)

The TRS R consists of the following rules:

inorderA_in_ga(nil, []) → inorderA_out_ga(nil, [])
inorderA_in_ga(tree(nil, T8, T9), T11) → U1_ga(T8, T9, T11, pB_in_gaga(T9, X14, T8, T11))
pB_in_gaga(T9, T12, T8, T11) → U6_gaga(T9, T12, T8, T11, inorderD_in_ga(T9, T12))
inorderD_in_ga(nil, []) → inorderD_out_ga(nil, [])
inorderD_in_ga(tree(T19, T20, T21), X33) → U3_ga(T19, T20, T21, X33, pE_in_gagaga(T19, X31, T21, X32, T20, X33))
pE_in_gagaga(T19, T22, T21, X32, T20, X33) → U8_gagaga(T19, T22, T21, X32, T20, X33, inorderD_in_ga(T19, T22))
U8_gagaga(T19, T22, T21, X32, T20, X33, inorderD_out_ga(T19, T22)) → U9_gagaga(T19, T22, T21, X32, T20, X33, pI_in_gagga(T21, X32, T22, T20, X33))
pI_in_gagga(T21, T23, T22, T20, X33) → U10_gagga(T21, T23, T22, T20, X33, inorderD_in_ga(T21, T23))
U10_gagga(T21, T23, T22, T20, X33, inorderD_out_ga(T21, T23)) → U11_gagga(T21, T23, T22, T20, X33, appendF_in_ggga(T22, T20, T23, X33))
appendF_in_ggga([], T36, T37, .(T36, T37)) → appendF_out_ggga([], T36, T37, .(T36, T37))
appendF_in_ggga(.(T46, T47), T48, T49, .(T46, X55)) → U4_ggga(T46, T47, T48, T49, X55, appendF_in_ggga(T47, T48, T49, X55))
U4_ggga(T46, T47, T48, T49, X55, appendF_out_ggga(T47, T48, T49, X55)) → appendF_out_ggga(.(T46, T47), T48, T49, .(T46, X55))
U11_gagga(T21, T23, T22, T20, X33, appendF_out_ggga(T22, T20, T23, X33)) → pI_out_gagga(T21, T23, T22, T20, X33)
U9_gagaga(T19, T22, T21, X32, T20, X33, pI_out_gagga(T21, X32, T22, T20, X33)) → pE_out_gagaga(T19, T22, T21, X32, T20, X33)
U3_ga(T19, T20, T21, X33, pE_out_gagaga(T19, X31, T21, X32, T20, X33)) → inorderD_out_ga(tree(T19, T20, T21), X33)
U6_gaga(T9, T12, T8, T11, inorderD_out_ga(T9, T12)) → U7_gaga(T9, T12, T8, T11, appendH_in_gga(T8, T12, T11))
appendH_in_gga(T66, T67, .(T66, T67)) → appendH_out_gga(T66, T67, .(T66, T67))
U7_gaga(T9, T12, T8, T11, appendH_out_gga(T8, T12, T11)) → pB_out_gaga(T9, T12, T8, T11)
U1_ga(T8, T9, T11, pB_out_gaga(T9, X14, T8, T11)) → inorderA_out_ga(tree(nil, T8, T9), T11)
inorderA_in_ga(tree(tree(T74, T75, T76), T8, T9), T11) → U2_ga(T74, T75, T76, T8, T9, T11, pC_in_gagagagaga(T74, X85, T76, X86, T75, X87, T9, X14, T8, T11))
pC_in_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11) → U12_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, inorderD_in_ga(T74, T77))
U12_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, inorderD_out_ga(T74, T77)) → U13_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, pJ_in_gaggagaga(T76, X86, T77, T75, X87, T9, X14, T8, T11))
pJ_in_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11) → U14_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11, inorderD_in_ga(T76, T78))
U14_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11, inorderD_out_ga(T76, T78)) → U15_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11, pK_in_gggagaga(T77, T75, T78, X87, T9, X14, T8, T11))
pK_in_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11) → U16_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11, appendF_in_ggga(T77, T75, T78, T83))
U16_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11, appendF_out_ggga(T77, T75, T78, T83)) → U17_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11, pL_in_gagga(T9, X14, T83, T8, T11))
pL_in_gagga(T9, T88, T83, T8, T11) → U18_gagga(T9, T88, T83, T8, T11, inorderD_in_ga(T9, T88))
U18_gagga(T9, T88, T83, T8, T11, inorderD_out_ga(T9, T88)) → U19_gagga(T9, T88, T83, T8, T11, appendG_in_ggga(T83, T8, T88, T11))
appendG_in_ggga([], T101, T102, .(T101, T102)) → appendG_out_ggga([], T101, T102, .(T101, T102))
appendG_in_ggga(.(T113, T114), T115, T116, .(T113, T118)) → U5_ggga(T113, T114, T115, T116, T118, appendG_in_ggga(T114, T115, T116, T118))
U5_ggga(T113, T114, T115, T116, T118, appendG_out_ggga(T114, T115, T116, T118)) → appendG_out_ggga(.(T113, T114), T115, T116, .(T113, T118))
U19_gagga(T9, T88, T83, T8, T11, appendG_out_ggga(T83, T8, T88, T11)) → pL_out_gagga(T9, T88, T83, T8, T11)
U17_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11, pL_out_gagga(T9, X14, T83, T8, T11)) → pK_out_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11)
U15_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11, pK_out_gggagaga(T77, T75, T78, X87, T9, X14, T8, T11)) → pJ_out_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11)
U13_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, pJ_out_gaggagaga(T76, X86, T77, T75, X87, T9, X14, T8, T11)) → pC_out_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11)
U2_ga(T74, T75, T76, T8, T9, T11, pC_out_gagagagaga(T74, X85, T76, X86, T75, X87, T9, X14, T8, T11)) → inorderA_out_ga(tree(tree(T74, T75, T76), T8, T9), T11)

The argument filtering Pi contains the following mapping:
inorderA_in_ga(x1, x2)  =  inorderA_in_ga(x1)
nil  =  nil
inorderA_out_ga(x1, x2)  =  inorderA_out_ga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x2, x4)
pB_in_gaga(x1, x2, x3, x4)  =  pB_in_gaga(x1, x3)
U6_gaga(x1, x2, x3, x4, x5)  =  U6_gaga(x1, x3, x5)
inorderD_in_ga(x1, x2)  =  inorderD_in_ga(x1)
inorderD_out_ga(x1, x2)  =  inorderD_out_ga(x1, x2)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x2, x3, x5)
pE_in_gagaga(x1, x2, x3, x4, x5, x6)  =  pE_in_gagaga(x1, x3, x5)
U8_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U8_gagaga(x1, x3, x5, x7)
U9_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U9_gagaga(x1, x2, x3, x5, x7)
pI_in_gagga(x1, x2, x3, x4, x5)  =  pI_in_gagga(x1, x3, x4)
U10_gagga(x1, x2, x3, x4, x5, x6)  =  U10_gagga(x1, x3, x4, x6)
U11_gagga(x1, x2, x3, x4, x5, x6)  =  U11_gagga(x1, x2, x3, x4, x6)
appendF_in_ggga(x1, x2, x3, x4)  =  appendF_in_ggga(x1, x2, x3)
[]  =  []
appendF_out_ggga(x1, x2, x3, x4)  =  appendF_out_ggga(x1, x2, x3, x4)
.(x1, x2)  =  .(x1, x2)
U4_ggga(x1, x2, x3, x4, x5, x6)  =  U4_ggga(x1, x2, x3, x4, x6)
pI_out_gagga(x1, x2, x3, x4, x5)  =  pI_out_gagga(x1, x2, x3, x4, x5)
pE_out_gagaga(x1, x2, x3, x4, x5, x6)  =  pE_out_gagaga(x1, x2, x3, x4, x5, x6)
U7_gaga(x1, x2, x3, x4, x5)  =  U7_gaga(x1, x2, x3, x5)
appendH_in_gga(x1, x2, x3)  =  appendH_in_gga(x1, x2)
appendH_out_gga(x1, x2, x3)  =  appendH_out_gga(x1, x2, x3)
pB_out_gaga(x1, x2, x3, x4)  =  pB_out_gaga(x1, x2, x3, x4)
U2_ga(x1, x2, x3, x4, x5, x6, x7)  =  U2_ga(x1, x2, x3, x4, x5, x7)
pC_in_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  pC_in_gagagagaga(x1, x3, x5, x7, x9)
U12_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U12_gagagagaga(x1, x3, x5, x7, x9, x11)
U13_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U13_gagagagaga(x1, x2, x3, x5, x7, x9, x11)
pJ_in_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  pJ_in_gaggagaga(x1, x3, x4, x6, x8)
U14_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U14_gaggagaga(x1, x3, x4, x6, x8, x10)
U15_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U15_gaggagaga(x1, x2, x3, x4, x6, x8, x10)
pK_in_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8)  =  pK_in_gggagaga(x1, x2, x3, x5, x7)
U16_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U16_gggagaga(x1, x2, x3, x5, x7, x9)
U17_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U17_gggagaga(x1, x2, x3, x4, x5, x7, x9)
pL_in_gagga(x1, x2, x3, x4, x5)  =  pL_in_gagga(x1, x3, x4)
U18_gagga(x1, x2, x3, x4, x5, x6)  =  U18_gagga(x1, x3, x4, x6)
U19_gagga(x1, x2, x3, x4, x5, x6)  =  U19_gagga(x1, x2, x3, x4, x6)
appendG_in_ggga(x1, x2, x3, x4)  =  appendG_in_ggga(x1, x2, x3)
appendG_out_ggga(x1, x2, x3, x4)  =  appendG_out_ggga(x1, x2, x3, x4)
U5_ggga(x1, x2, x3, x4, x5, x6)  =  U5_ggga(x1, x2, x3, x4, x6)
pL_out_gagga(x1, x2, x3, x4, x5)  =  pL_out_gagga(x1, x2, x3, x4, x5)
pK_out_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8)  =  pK_out_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8)
pJ_out_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  pJ_out_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)
pC_out_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  pC_out_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)
INORDERA_IN_GA(x1, x2)  =  INORDERA_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x1, x2, x4)
PB_IN_GAGA(x1, x2, x3, x4)  =  PB_IN_GAGA(x1, x3)
U6_GAGA(x1, x2, x3, x4, x5)  =  U6_GAGA(x1, x3, x5)
INORDERD_IN_GA(x1, x2)  =  INORDERD_IN_GA(x1)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x1, x2, x3, x5)
PE_IN_GAGAGA(x1, x2, x3, x4, x5, x6)  =  PE_IN_GAGAGA(x1, x3, x5)
U8_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U8_GAGAGA(x1, x3, x5, x7)
U9_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U9_GAGAGA(x1, x2, x3, x5, x7)
PI_IN_GAGGA(x1, x2, x3, x4, x5)  =  PI_IN_GAGGA(x1, x3, x4)
U10_GAGGA(x1, x2, x3, x4, x5, x6)  =  U10_GAGGA(x1, x3, x4, x6)
U11_GAGGA(x1, x2, x3, x4, x5, x6)  =  U11_GAGGA(x1, x2, x3, x4, x6)
APPENDF_IN_GGGA(x1, x2, x3, x4)  =  APPENDF_IN_GGGA(x1, x2, x3)
U4_GGGA(x1, x2, x3, x4, x5, x6)  =  U4_GGGA(x1, x2, x3, x4, x6)
U7_GAGA(x1, x2, x3, x4, x5)  =  U7_GAGA(x1, x2, x3, x5)
APPENDH_IN_GGA(x1, x2, x3)  =  APPENDH_IN_GGA(x1, x2)
U2_GA(x1, x2, x3, x4, x5, x6, x7)  =  U2_GA(x1, x2, x3, x4, x5, x7)
PC_IN_GAGAGAGAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  PC_IN_GAGAGAGAGA(x1, x3, x5, x7, x9)
U12_GAGAGAGAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U12_GAGAGAGAGA(x1, x3, x5, x7, x9, x11)
U13_GAGAGAGAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U13_GAGAGAGAGA(x1, x2, x3, x5, x7, x9, x11)
PJ_IN_GAGGAGAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  PJ_IN_GAGGAGAGA(x1, x3, x4, x6, x8)
U14_GAGGAGAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U14_GAGGAGAGA(x1, x3, x4, x6, x8, x10)
U15_GAGGAGAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U15_GAGGAGAGA(x1, x2, x3, x4, x6, x8, x10)
PK_IN_GGGAGAGA(x1, x2, x3, x4, x5, x6, x7, x8)  =  PK_IN_GGGAGAGA(x1, x2, x3, x5, x7)
U16_GGGAGAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U16_GGGAGAGA(x1, x2, x3, x5, x7, x9)
U17_GGGAGAGA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U17_GGGAGAGA(x1, x2, x3, x4, x5, x7, x9)
PL_IN_GAGGA(x1, x2, x3, x4, x5)  =  PL_IN_GAGGA(x1, x3, x4)
U18_GAGGA(x1, x2, x3, x4, x5, x6)  =  U18_GAGGA(x1, x3, x4, x6)
U19_GAGGA(x1, x2, x3, x4, x5, x6)  =  U19_GAGGA(x1, x2, x3, x4, x6)
APPENDG_IN_GGGA(x1, x2, x3, x4)  =  APPENDG_IN_GGGA(x1, x2, x3)
U5_GGGA(x1, x2, x3, x4, x5, x6)  =  U5_GGGA(x1, x2, x3, x4, x6)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

APPENDG_IN_GGGA(.(T113, T114), T115, T116, .(T113, T118)) → APPENDG_IN_GGGA(T114, T115, T116, T118)

The TRS R consists of the following rules:

inorderA_in_ga(nil, []) → inorderA_out_ga(nil, [])
inorderA_in_ga(tree(nil, T8, T9), T11) → U1_ga(T8, T9, T11, pB_in_gaga(T9, X14, T8, T11))
pB_in_gaga(T9, T12, T8, T11) → U6_gaga(T9, T12, T8, T11, inorderD_in_ga(T9, T12))
inorderD_in_ga(nil, []) → inorderD_out_ga(nil, [])
inorderD_in_ga(tree(T19, T20, T21), X33) → U3_ga(T19, T20, T21, X33, pE_in_gagaga(T19, X31, T21, X32, T20, X33))
pE_in_gagaga(T19, T22, T21, X32, T20, X33) → U8_gagaga(T19, T22, T21, X32, T20, X33, inorderD_in_ga(T19, T22))
U8_gagaga(T19, T22, T21, X32, T20, X33, inorderD_out_ga(T19, T22)) → U9_gagaga(T19, T22, T21, X32, T20, X33, pI_in_gagga(T21, X32, T22, T20, X33))
pI_in_gagga(T21, T23, T22, T20, X33) → U10_gagga(T21, T23, T22, T20, X33, inorderD_in_ga(T21, T23))
U10_gagga(T21, T23, T22, T20, X33, inorderD_out_ga(T21, T23)) → U11_gagga(T21, T23, T22, T20, X33, appendF_in_ggga(T22, T20, T23, X33))
appendF_in_ggga([], T36, T37, .(T36, T37)) → appendF_out_ggga([], T36, T37, .(T36, T37))
appendF_in_ggga(.(T46, T47), T48, T49, .(T46, X55)) → U4_ggga(T46, T47, T48, T49, X55, appendF_in_ggga(T47, T48, T49, X55))
U4_ggga(T46, T47, T48, T49, X55, appendF_out_ggga(T47, T48, T49, X55)) → appendF_out_ggga(.(T46, T47), T48, T49, .(T46, X55))
U11_gagga(T21, T23, T22, T20, X33, appendF_out_ggga(T22, T20, T23, X33)) → pI_out_gagga(T21, T23, T22, T20, X33)
U9_gagaga(T19, T22, T21, X32, T20, X33, pI_out_gagga(T21, X32, T22, T20, X33)) → pE_out_gagaga(T19, T22, T21, X32, T20, X33)
U3_ga(T19, T20, T21, X33, pE_out_gagaga(T19, X31, T21, X32, T20, X33)) → inorderD_out_ga(tree(T19, T20, T21), X33)
U6_gaga(T9, T12, T8, T11, inorderD_out_ga(T9, T12)) → U7_gaga(T9, T12, T8, T11, appendH_in_gga(T8, T12, T11))
appendH_in_gga(T66, T67, .(T66, T67)) → appendH_out_gga(T66, T67, .(T66, T67))
U7_gaga(T9, T12, T8, T11, appendH_out_gga(T8, T12, T11)) → pB_out_gaga(T9, T12, T8, T11)
U1_ga(T8, T9, T11, pB_out_gaga(T9, X14, T8, T11)) → inorderA_out_ga(tree(nil, T8, T9), T11)
inorderA_in_ga(tree(tree(T74, T75, T76), T8, T9), T11) → U2_ga(T74, T75, T76, T8, T9, T11, pC_in_gagagagaga(T74, X85, T76, X86, T75, X87, T9, X14, T8, T11))
pC_in_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11) → U12_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, inorderD_in_ga(T74, T77))
U12_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, inorderD_out_ga(T74, T77)) → U13_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, pJ_in_gaggagaga(T76, X86, T77, T75, X87, T9, X14, T8, T11))
pJ_in_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11) → U14_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11, inorderD_in_ga(T76, T78))
U14_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11, inorderD_out_ga(T76, T78)) → U15_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11, pK_in_gggagaga(T77, T75, T78, X87, T9, X14, T8, T11))
pK_in_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11) → U16_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11, appendF_in_ggga(T77, T75, T78, T83))
U16_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11, appendF_out_ggga(T77, T75, T78, T83)) → U17_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11, pL_in_gagga(T9, X14, T83, T8, T11))
pL_in_gagga(T9, T88, T83, T8, T11) → U18_gagga(T9, T88, T83, T8, T11, inorderD_in_ga(T9, T88))
U18_gagga(T9, T88, T83, T8, T11, inorderD_out_ga(T9, T88)) → U19_gagga(T9, T88, T83, T8, T11, appendG_in_ggga(T83, T8, T88, T11))
appendG_in_ggga([], T101, T102, .(T101, T102)) → appendG_out_ggga([], T101, T102, .(T101, T102))
appendG_in_ggga(.(T113, T114), T115, T116, .(T113, T118)) → U5_ggga(T113, T114, T115, T116, T118, appendG_in_ggga(T114, T115, T116, T118))
U5_ggga(T113, T114, T115, T116, T118, appendG_out_ggga(T114, T115, T116, T118)) → appendG_out_ggga(.(T113, T114), T115, T116, .(T113, T118))
U19_gagga(T9, T88, T83, T8, T11, appendG_out_ggga(T83, T8, T88, T11)) → pL_out_gagga(T9, T88, T83, T8, T11)
U17_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11, pL_out_gagga(T9, X14, T83, T8, T11)) → pK_out_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11)
U15_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11, pK_out_gggagaga(T77, T75, T78, X87, T9, X14, T8, T11)) → pJ_out_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11)
U13_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, pJ_out_gaggagaga(T76, X86, T77, T75, X87, T9, X14, T8, T11)) → pC_out_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11)
U2_ga(T74, T75, T76, T8, T9, T11, pC_out_gagagagaga(T74, X85, T76, X86, T75, X87, T9, X14, T8, T11)) → inorderA_out_ga(tree(tree(T74, T75, T76), T8, T9), T11)

The argument filtering Pi contains the following mapping:
inorderA_in_ga(x1, x2)  =  inorderA_in_ga(x1)
nil  =  nil
inorderA_out_ga(x1, x2)  =  inorderA_out_ga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x2, x4)
pB_in_gaga(x1, x2, x3, x4)  =  pB_in_gaga(x1, x3)
U6_gaga(x1, x2, x3, x4, x5)  =  U6_gaga(x1, x3, x5)
inorderD_in_ga(x1, x2)  =  inorderD_in_ga(x1)
inorderD_out_ga(x1, x2)  =  inorderD_out_ga(x1, x2)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x2, x3, x5)
pE_in_gagaga(x1, x2, x3, x4, x5, x6)  =  pE_in_gagaga(x1, x3, x5)
U8_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U8_gagaga(x1, x3, x5, x7)
U9_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U9_gagaga(x1, x2, x3, x5, x7)
pI_in_gagga(x1, x2, x3, x4, x5)  =  pI_in_gagga(x1, x3, x4)
U10_gagga(x1, x2, x3, x4, x5, x6)  =  U10_gagga(x1, x3, x4, x6)
U11_gagga(x1, x2, x3, x4, x5, x6)  =  U11_gagga(x1, x2, x3, x4, x6)
appendF_in_ggga(x1, x2, x3, x4)  =  appendF_in_ggga(x1, x2, x3)
[]  =  []
appendF_out_ggga(x1, x2, x3, x4)  =  appendF_out_ggga(x1, x2, x3, x4)
.(x1, x2)  =  .(x1, x2)
U4_ggga(x1, x2, x3, x4, x5, x6)  =  U4_ggga(x1, x2, x3, x4, x6)
pI_out_gagga(x1, x2, x3, x4, x5)  =  pI_out_gagga(x1, x2, x3, x4, x5)
pE_out_gagaga(x1, x2, x3, x4, x5, x6)  =  pE_out_gagaga(x1, x2, x3, x4, x5, x6)
U7_gaga(x1, x2, x3, x4, x5)  =  U7_gaga(x1, x2, x3, x5)
appendH_in_gga(x1, x2, x3)  =  appendH_in_gga(x1, x2)
appendH_out_gga(x1, x2, x3)  =  appendH_out_gga(x1, x2, x3)
pB_out_gaga(x1, x2, x3, x4)  =  pB_out_gaga(x1, x2, x3, x4)
U2_ga(x1, x2, x3, x4, x5, x6, x7)  =  U2_ga(x1, x2, x3, x4, x5, x7)
pC_in_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  pC_in_gagagagaga(x1, x3, x5, x7, x9)
U12_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U12_gagagagaga(x1, x3, x5, x7, x9, x11)
U13_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U13_gagagagaga(x1, x2, x3, x5, x7, x9, x11)
pJ_in_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  pJ_in_gaggagaga(x1, x3, x4, x6, x8)
U14_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U14_gaggagaga(x1, x3, x4, x6, x8, x10)
U15_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U15_gaggagaga(x1, x2, x3, x4, x6, x8, x10)
pK_in_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8)  =  pK_in_gggagaga(x1, x2, x3, x5, x7)
U16_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U16_gggagaga(x1, x2, x3, x5, x7, x9)
U17_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U17_gggagaga(x1, x2, x3, x4, x5, x7, x9)
pL_in_gagga(x1, x2, x3, x4, x5)  =  pL_in_gagga(x1, x3, x4)
U18_gagga(x1, x2, x3, x4, x5, x6)  =  U18_gagga(x1, x3, x4, x6)
U19_gagga(x1, x2, x3, x4, x5, x6)  =  U19_gagga(x1, x2, x3, x4, x6)
appendG_in_ggga(x1, x2, x3, x4)  =  appendG_in_ggga(x1, x2, x3)
appendG_out_ggga(x1, x2, x3, x4)  =  appendG_out_ggga(x1, x2, x3, x4)
U5_ggga(x1, x2, x3, x4, x5, x6)  =  U5_ggga(x1, x2, x3, x4, x6)
pL_out_gagga(x1, x2, x3, x4, x5)  =  pL_out_gagga(x1, x2, x3, x4, x5)
pK_out_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8)  =  pK_out_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8)
pJ_out_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  pJ_out_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)
pC_out_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  pC_out_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)
APPENDG_IN_GGGA(x1, x2, x3, x4)  =  APPENDG_IN_GGGA(x1, x2, x3)

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:

APPENDG_IN_GGGA(.(T113, T114), T115, T116, .(T113, T118)) → APPENDG_IN_GGGA(T114, T115, T116, T118)

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

APPENDG_IN_GGGA(.(T113, T114), T115, T116) → APPENDG_IN_GGGA(T114, T115, T116)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

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

(13) YES

(14) Obligation:

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

APPENDF_IN_GGGA(.(T46, T47), T48, T49, .(T46, X55)) → APPENDF_IN_GGGA(T47, T48, T49, X55)

The TRS R consists of the following rules:

inorderA_in_ga(nil, []) → inorderA_out_ga(nil, [])
inorderA_in_ga(tree(nil, T8, T9), T11) → U1_ga(T8, T9, T11, pB_in_gaga(T9, X14, T8, T11))
pB_in_gaga(T9, T12, T8, T11) → U6_gaga(T9, T12, T8, T11, inorderD_in_ga(T9, T12))
inorderD_in_ga(nil, []) → inorderD_out_ga(nil, [])
inorderD_in_ga(tree(T19, T20, T21), X33) → U3_ga(T19, T20, T21, X33, pE_in_gagaga(T19, X31, T21, X32, T20, X33))
pE_in_gagaga(T19, T22, T21, X32, T20, X33) → U8_gagaga(T19, T22, T21, X32, T20, X33, inorderD_in_ga(T19, T22))
U8_gagaga(T19, T22, T21, X32, T20, X33, inorderD_out_ga(T19, T22)) → U9_gagaga(T19, T22, T21, X32, T20, X33, pI_in_gagga(T21, X32, T22, T20, X33))
pI_in_gagga(T21, T23, T22, T20, X33) → U10_gagga(T21, T23, T22, T20, X33, inorderD_in_ga(T21, T23))
U10_gagga(T21, T23, T22, T20, X33, inorderD_out_ga(T21, T23)) → U11_gagga(T21, T23, T22, T20, X33, appendF_in_ggga(T22, T20, T23, X33))
appendF_in_ggga([], T36, T37, .(T36, T37)) → appendF_out_ggga([], T36, T37, .(T36, T37))
appendF_in_ggga(.(T46, T47), T48, T49, .(T46, X55)) → U4_ggga(T46, T47, T48, T49, X55, appendF_in_ggga(T47, T48, T49, X55))
U4_ggga(T46, T47, T48, T49, X55, appendF_out_ggga(T47, T48, T49, X55)) → appendF_out_ggga(.(T46, T47), T48, T49, .(T46, X55))
U11_gagga(T21, T23, T22, T20, X33, appendF_out_ggga(T22, T20, T23, X33)) → pI_out_gagga(T21, T23, T22, T20, X33)
U9_gagaga(T19, T22, T21, X32, T20, X33, pI_out_gagga(T21, X32, T22, T20, X33)) → pE_out_gagaga(T19, T22, T21, X32, T20, X33)
U3_ga(T19, T20, T21, X33, pE_out_gagaga(T19, X31, T21, X32, T20, X33)) → inorderD_out_ga(tree(T19, T20, T21), X33)
U6_gaga(T9, T12, T8, T11, inorderD_out_ga(T9, T12)) → U7_gaga(T9, T12, T8, T11, appendH_in_gga(T8, T12, T11))
appendH_in_gga(T66, T67, .(T66, T67)) → appendH_out_gga(T66, T67, .(T66, T67))
U7_gaga(T9, T12, T8, T11, appendH_out_gga(T8, T12, T11)) → pB_out_gaga(T9, T12, T8, T11)
U1_ga(T8, T9, T11, pB_out_gaga(T9, X14, T8, T11)) → inorderA_out_ga(tree(nil, T8, T9), T11)
inorderA_in_ga(tree(tree(T74, T75, T76), T8, T9), T11) → U2_ga(T74, T75, T76, T8, T9, T11, pC_in_gagagagaga(T74, X85, T76, X86, T75, X87, T9, X14, T8, T11))
pC_in_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11) → U12_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, inorderD_in_ga(T74, T77))
U12_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, inorderD_out_ga(T74, T77)) → U13_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, pJ_in_gaggagaga(T76, X86, T77, T75, X87, T9, X14, T8, T11))
pJ_in_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11) → U14_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11, inorderD_in_ga(T76, T78))
U14_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11, inorderD_out_ga(T76, T78)) → U15_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11, pK_in_gggagaga(T77, T75, T78, X87, T9, X14, T8, T11))
pK_in_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11) → U16_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11, appendF_in_ggga(T77, T75, T78, T83))
U16_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11, appendF_out_ggga(T77, T75, T78, T83)) → U17_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11, pL_in_gagga(T9, X14, T83, T8, T11))
pL_in_gagga(T9, T88, T83, T8, T11) → U18_gagga(T9, T88, T83, T8, T11, inorderD_in_ga(T9, T88))
U18_gagga(T9, T88, T83, T8, T11, inorderD_out_ga(T9, T88)) → U19_gagga(T9, T88, T83, T8, T11, appendG_in_ggga(T83, T8, T88, T11))
appendG_in_ggga([], T101, T102, .(T101, T102)) → appendG_out_ggga([], T101, T102, .(T101, T102))
appendG_in_ggga(.(T113, T114), T115, T116, .(T113, T118)) → U5_ggga(T113, T114, T115, T116, T118, appendG_in_ggga(T114, T115, T116, T118))
U5_ggga(T113, T114, T115, T116, T118, appendG_out_ggga(T114, T115, T116, T118)) → appendG_out_ggga(.(T113, T114), T115, T116, .(T113, T118))
U19_gagga(T9, T88, T83, T8, T11, appendG_out_ggga(T83, T8, T88, T11)) → pL_out_gagga(T9, T88, T83, T8, T11)
U17_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11, pL_out_gagga(T9, X14, T83, T8, T11)) → pK_out_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11)
U15_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11, pK_out_gggagaga(T77, T75, T78, X87, T9, X14, T8, T11)) → pJ_out_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11)
U13_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, pJ_out_gaggagaga(T76, X86, T77, T75, X87, T9, X14, T8, T11)) → pC_out_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11)
U2_ga(T74, T75, T76, T8, T9, T11, pC_out_gagagagaga(T74, X85, T76, X86, T75, X87, T9, X14, T8, T11)) → inorderA_out_ga(tree(tree(T74, T75, T76), T8, T9), T11)

The argument filtering Pi contains the following mapping:
inorderA_in_ga(x1, x2)  =  inorderA_in_ga(x1)
nil  =  nil
inorderA_out_ga(x1, x2)  =  inorderA_out_ga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x2, x4)
pB_in_gaga(x1, x2, x3, x4)  =  pB_in_gaga(x1, x3)
U6_gaga(x1, x2, x3, x4, x5)  =  U6_gaga(x1, x3, x5)
inorderD_in_ga(x1, x2)  =  inorderD_in_ga(x1)
inorderD_out_ga(x1, x2)  =  inorderD_out_ga(x1, x2)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x2, x3, x5)
pE_in_gagaga(x1, x2, x3, x4, x5, x6)  =  pE_in_gagaga(x1, x3, x5)
U8_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U8_gagaga(x1, x3, x5, x7)
U9_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U9_gagaga(x1, x2, x3, x5, x7)
pI_in_gagga(x1, x2, x3, x4, x5)  =  pI_in_gagga(x1, x3, x4)
U10_gagga(x1, x2, x3, x4, x5, x6)  =  U10_gagga(x1, x3, x4, x6)
U11_gagga(x1, x2, x3, x4, x5, x6)  =  U11_gagga(x1, x2, x3, x4, x6)
appendF_in_ggga(x1, x2, x3, x4)  =  appendF_in_ggga(x1, x2, x3)
[]  =  []
appendF_out_ggga(x1, x2, x3, x4)  =  appendF_out_ggga(x1, x2, x3, x4)
.(x1, x2)  =  .(x1, x2)
U4_ggga(x1, x2, x3, x4, x5, x6)  =  U4_ggga(x1, x2, x3, x4, x6)
pI_out_gagga(x1, x2, x3, x4, x5)  =  pI_out_gagga(x1, x2, x3, x4, x5)
pE_out_gagaga(x1, x2, x3, x4, x5, x6)  =  pE_out_gagaga(x1, x2, x3, x4, x5, x6)
U7_gaga(x1, x2, x3, x4, x5)  =  U7_gaga(x1, x2, x3, x5)
appendH_in_gga(x1, x2, x3)  =  appendH_in_gga(x1, x2)
appendH_out_gga(x1, x2, x3)  =  appendH_out_gga(x1, x2, x3)
pB_out_gaga(x1, x2, x3, x4)  =  pB_out_gaga(x1, x2, x3, x4)
U2_ga(x1, x2, x3, x4, x5, x6, x7)  =  U2_ga(x1, x2, x3, x4, x5, x7)
pC_in_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  pC_in_gagagagaga(x1, x3, x5, x7, x9)
U12_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U12_gagagagaga(x1, x3, x5, x7, x9, x11)
U13_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U13_gagagagaga(x1, x2, x3, x5, x7, x9, x11)
pJ_in_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  pJ_in_gaggagaga(x1, x3, x4, x6, x8)
U14_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U14_gaggagaga(x1, x3, x4, x6, x8, x10)
U15_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U15_gaggagaga(x1, x2, x3, x4, x6, x8, x10)
pK_in_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8)  =  pK_in_gggagaga(x1, x2, x3, x5, x7)
U16_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U16_gggagaga(x1, x2, x3, x5, x7, x9)
U17_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U17_gggagaga(x1, x2, x3, x4, x5, x7, x9)
pL_in_gagga(x1, x2, x3, x4, x5)  =  pL_in_gagga(x1, x3, x4)
U18_gagga(x1, x2, x3, x4, x5, x6)  =  U18_gagga(x1, x3, x4, x6)
U19_gagga(x1, x2, x3, x4, x5, x6)  =  U19_gagga(x1, x2, x3, x4, x6)
appendG_in_ggga(x1, x2, x3, x4)  =  appendG_in_ggga(x1, x2, x3)
appendG_out_ggga(x1, x2, x3, x4)  =  appendG_out_ggga(x1, x2, x3, x4)
U5_ggga(x1, x2, x3, x4, x5, x6)  =  U5_ggga(x1, x2, x3, x4, x6)
pL_out_gagga(x1, x2, x3, x4, x5)  =  pL_out_gagga(x1, x2, x3, x4, x5)
pK_out_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8)  =  pK_out_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8)
pJ_out_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  pJ_out_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)
pC_out_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  pC_out_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)
APPENDF_IN_GGGA(x1, x2, x3, x4)  =  APPENDF_IN_GGGA(x1, x2, x3)

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:

APPENDF_IN_GGGA(.(T46, T47), T48, T49, .(T46, X55)) → APPENDF_IN_GGGA(T47, T48, T49, X55)

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

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

APPENDF_IN_GGGA(.(T46, T47), T48, T49) → APPENDF_IN_GGGA(T47, T48, T49)

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:

• APPENDF_IN_GGGA(.(T46, T47), T48, T49) → APPENDF_IN_GGGA(T47, T48, T49)
  The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3

(20) YES

(21) Obligation:

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

INORDERD_IN_GA(tree(T19, T20, T21), X33) → PE_IN_GAGAGA(T19, X31, T21, X32, T20, X33)
PE_IN_GAGAGA(T19, T22, T21, X32, T20, X33) → U8_GAGAGA(T19, T22, T21, X32, T20, X33, inorderD_in_ga(T19, T22))
U8_GAGAGA(T19, T22, T21, X32, T20, X33, inorderD_out_ga(T19, T22)) → PI_IN_GAGGA(T21, X32, T22, T20, X33)
PI_IN_GAGGA(T21, T23, T22, T20, X33) → INORDERD_IN_GA(T21, T23)
PE_IN_GAGAGA(T19, T22, T21, X32, T20, X33) → INORDERD_IN_GA(T19, T22)

The TRS R consists of the following rules:

inorderA_in_ga(nil, []) → inorderA_out_ga(nil, [])
inorderA_in_ga(tree(nil, T8, T9), T11) → U1_ga(T8, T9, T11, pB_in_gaga(T9, X14, T8, T11))
pB_in_gaga(T9, T12, T8, T11) → U6_gaga(T9, T12, T8, T11, inorderD_in_ga(T9, T12))
inorderD_in_ga(nil, []) → inorderD_out_ga(nil, [])
inorderD_in_ga(tree(T19, T20, T21), X33) → U3_ga(T19, T20, T21, X33, pE_in_gagaga(T19, X31, T21, X32, T20, X33))
pE_in_gagaga(T19, T22, T21, X32, T20, X33) → U8_gagaga(T19, T22, T21, X32, T20, X33, inorderD_in_ga(T19, T22))
U8_gagaga(T19, T22, T21, X32, T20, X33, inorderD_out_ga(T19, T22)) → U9_gagaga(T19, T22, T21, X32, T20, X33, pI_in_gagga(T21, X32, T22, T20, X33))
pI_in_gagga(T21, T23, T22, T20, X33) → U10_gagga(T21, T23, T22, T20, X33, inorderD_in_ga(T21, T23))
U10_gagga(T21, T23, T22, T20, X33, inorderD_out_ga(T21, T23)) → U11_gagga(T21, T23, T22, T20, X33, appendF_in_ggga(T22, T20, T23, X33))
appendF_in_ggga([], T36, T37, .(T36, T37)) → appendF_out_ggga([], T36, T37, .(T36, T37))
appendF_in_ggga(.(T46, T47), T48, T49, .(T46, X55)) → U4_ggga(T46, T47, T48, T49, X55, appendF_in_ggga(T47, T48, T49, X55))
U4_ggga(T46, T47, T48, T49, X55, appendF_out_ggga(T47, T48, T49, X55)) → appendF_out_ggga(.(T46, T47), T48, T49, .(T46, X55))
U11_gagga(T21, T23, T22, T20, X33, appendF_out_ggga(T22, T20, T23, X33)) → pI_out_gagga(T21, T23, T22, T20, X33)
U9_gagaga(T19, T22, T21, X32, T20, X33, pI_out_gagga(T21, X32, T22, T20, X33)) → pE_out_gagaga(T19, T22, T21, X32, T20, X33)
U3_ga(T19, T20, T21, X33, pE_out_gagaga(T19, X31, T21, X32, T20, X33)) → inorderD_out_ga(tree(T19, T20, T21), X33)
U6_gaga(T9, T12, T8, T11, inorderD_out_ga(T9, T12)) → U7_gaga(T9, T12, T8, T11, appendH_in_gga(T8, T12, T11))
appendH_in_gga(T66, T67, .(T66, T67)) → appendH_out_gga(T66, T67, .(T66, T67))
U7_gaga(T9, T12, T8, T11, appendH_out_gga(T8, T12, T11)) → pB_out_gaga(T9, T12, T8, T11)
U1_ga(T8, T9, T11, pB_out_gaga(T9, X14, T8, T11)) → inorderA_out_ga(tree(nil, T8, T9), T11)
inorderA_in_ga(tree(tree(T74, T75, T76), T8, T9), T11) → U2_ga(T74, T75, T76, T8, T9, T11, pC_in_gagagagaga(T74, X85, T76, X86, T75, X87, T9, X14, T8, T11))
pC_in_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11) → U12_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, inorderD_in_ga(T74, T77))
U12_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, inorderD_out_ga(T74, T77)) → U13_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, pJ_in_gaggagaga(T76, X86, T77, T75, X87, T9, X14, T8, T11))
pJ_in_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11) → U14_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11, inorderD_in_ga(T76, T78))
U14_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11, inorderD_out_ga(T76, T78)) → U15_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11, pK_in_gggagaga(T77, T75, T78, X87, T9, X14, T8, T11))
pK_in_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11) → U16_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11, appendF_in_ggga(T77, T75, T78, T83))
U16_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11, appendF_out_ggga(T77, T75, T78, T83)) → U17_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11, pL_in_gagga(T9, X14, T83, T8, T11))
pL_in_gagga(T9, T88, T83, T8, T11) → U18_gagga(T9, T88, T83, T8, T11, inorderD_in_ga(T9, T88))
U18_gagga(T9, T88, T83, T8, T11, inorderD_out_ga(T9, T88)) → U19_gagga(T9, T88, T83, T8, T11, appendG_in_ggga(T83, T8, T88, T11))
appendG_in_ggga([], T101, T102, .(T101, T102)) → appendG_out_ggga([], T101, T102, .(T101, T102))
appendG_in_ggga(.(T113, T114), T115, T116, .(T113, T118)) → U5_ggga(T113, T114, T115, T116, T118, appendG_in_ggga(T114, T115, T116, T118))
U5_ggga(T113, T114, T115, T116, T118, appendG_out_ggga(T114, T115, T116, T118)) → appendG_out_ggga(.(T113, T114), T115, T116, .(T113, T118))
U19_gagga(T9, T88, T83, T8, T11, appendG_out_ggga(T83, T8, T88, T11)) → pL_out_gagga(T9, T88, T83, T8, T11)
U17_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11, pL_out_gagga(T9, X14, T83, T8, T11)) → pK_out_gggagaga(T77, T75, T78, T83, T9, X14, T8, T11)
U15_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11, pK_out_gggagaga(T77, T75, T78, X87, T9, X14, T8, T11)) → pJ_out_gaggagaga(T76, T78, T77, T75, X87, T9, X14, T8, T11)
U13_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11, pJ_out_gaggagaga(T76, X86, T77, T75, X87, T9, X14, T8, T11)) → pC_out_gagagagaga(T74, T77, T76, X86, T75, X87, T9, X14, T8, T11)
U2_ga(T74, T75, T76, T8, T9, T11, pC_out_gagagagaga(T74, X85, T76, X86, T75, X87, T9, X14, T8, T11)) → inorderA_out_ga(tree(tree(T74, T75, T76), T8, T9), T11)

The argument filtering Pi contains the following mapping:
inorderA_in_ga(x1, x2)  =  inorderA_in_ga(x1)
nil  =  nil
inorderA_out_ga(x1, x2)  =  inorderA_out_ga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x2, x4)
pB_in_gaga(x1, x2, x3, x4)  =  pB_in_gaga(x1, x3)
U6_gaga(x1, x2, x3, x4, x5)  =  U6_gaga(x1, x3, x5)
inorderD_in_ga(x1, x2)  =  inorderD_in_ga(x1)
inorderD_out_ga(x1, x2)  =  inorderD_out_ga(x1, x2)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x2, x3, x5)
pE_in_gagaga(x1, x2, x3, x4, x5, x6)  =  pE_in_gagaga(x1, x3, x5)
U8_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U8_gagaga(x1, x3, x5, x7)
U9_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U9_gagaga(x1, x2, x3, x5, x7)
pI_in_gagga(x1, x2, x3, x4, x5)  =  pI_in_gagga(x1, x3, x4)
U10_gagga(x1, x2, x3, x4, x5, x6)  =  U10_gagga(x1, x3, x4, x6)
U11_gagga(x1, x2, x3, x4, x5, x6)  =  U11_gagga(x1, x2, x3, x4, x6)
appendF_in_ggga(x1, x2, x3, x4)  =  appendF_in_ggga(x1, x2, x3)
[]  =  []
appendF_out_ggga(x1, x2, x3, x4)  =  appendF_out_ggga(x1, x2, x3, x4)
.(x1, x2)  =  .(x1, x2)
U4_ggga(x1, x2, x3, x4, x5, x6)  =  U4_ggga(x1, x2, x3, x4, x6)
pI_out_gagga(x1, x2, x3, x4, x5)  =  pI_out_gagga(x1, x2, x3, x4, x5)
pE_out_gagaga(x1, x2, x3, x4, x5, x6)  =  pE_out_gagaga(x1, x2, x3, x4, x5, x6)
U7_gaga(x1, x2, x3, x4, x5)  =  U7_gaga(x1, x2, x3, x5)
appendH_in_gga(x1, x2, x3)  =  appendH_in_gga(x1, x2)
appendH_out_gga(x1, x2, x3)  =  appendH_out_gga(x1, x2, x3)
pB_out_gaga(x1, x2, x3, x4)  =  pB_out_gaga(x1, x2, x3, x4)
U2_ga(x1, x2, x3, x4, x5, x6, x7)  =  U2_ga(x1, x2, x3, x4, x5, x7)
pC_in_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  pC_in_gagagagaga(x1, x3, x5, x7, x9)
U12_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U12_gagagagaga(x1, x3, x5, x7, x9, x11)
U13_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11)  =  U13_gagagagaga(x1, x2, x3, x5, x7, x9, x11)
pJ_in_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  pJ_in_gaggagaga(x1, x3, x4, x6, x8)
U14_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U14_gaggagaga(x1, x3, x4, x6, x8, x10)
U15_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U15_gaggagaga(x1, x2, x3, x4, x6, x8, x10)
pK_in_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8)  =  pK_in_gggagaga(x1, x2, x3, x5, x7)
U16_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U16_gggagaga(x1, x2, x3, x5, x7, x9)
U17_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U17_gggagaga(x1, x2, x3, x4, x5, x7, x9)
pL_in_gagga(x1, x2, x3, x4, x5)  =  pL_in_gagga(x1, x3, x4)
U18_gagga(x1, x2, x3, x4, x5, x6)  =  U18_gagga(x1, x3, x4, x6)
U19_gagga(x1, x2, x3, x4, x5, x6)  =  U19_gagga(x1, x2, x3, x4, x6)
appendG_in_ggga(x1, x2, x3, x4)  =  appendG_in_ggga(x1, x2, x3)
appendG_out_ggga(x1, x2, x3, x4)  =  appendG_out_ggga(x1, x2, x3, x4)
U5_ggga(x1, x2, x3, x4, x5, x6)  =  U5_ggga(x1, x2, x3, x4, x6)
pL_out_gagga(x1, x2, x3, x4, x5)  =  pL_out_gagga(x1, x2, x3, x4, x5)
pK_out_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8)  =  pK_out_gggagaga(x1, x2, x3, x4, x5, x6, x7, x8)
pJ_out_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  pJ_out_gaggagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9)
pC_out_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  pC_out_gagagagaga(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)
INORDERD_IN_GA(x1, x2)  =  INORDERD_IN_GA(x1)
PE_IN_GAGAGA(x1, x2, x3, x4, x5, x6)  =  PE_IN_GAGAGA(x1, x3, x5)
U8_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U8_GAGAGA(x1, x3, x5, x7)
PI_IN_GAGGA(x1, x2, x3, x4, x5)  =  PI_IN_GAGGA(x1, 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:

INORDERD_IN_GA(tree(T19, T20, T21), X33) → PE_IN_GAGAGA(T19, X31, T21, X32, T20, X33)
PE_IN_GAGAGA(T19, T22, T21, X32, T20, X33) → U8_GAGAGA(T19, T22, T21, X32, T20, X33, inorderD_in_ga(T19, T22))
U8_GAGAGA(T19, T22, T21, X32, T20, X33, inorderD_out_ga(T19, T22)) → PI_IN_GAGGA(T21, X32, T22, T20, X33)
PI_IN_GAGGA(T21, T23, T22, T20, X33) → INORDERD_IN_GA(T21, T23)
PE_IN_GAGAGA(T19, T22, T21, X32, T20, X33) → INORDERD_IN_GA(T19, T22)

The TRS R consists of the following rules:

inorderD_in_ga(nil, []) → inorderD_out_ga(nil, [])
inorderD_in_ga(tree(T19, T20, T21), X33) → U3_ga(T19, T20, T21, X33, pE_in_gagaga(T19, X31, T21, X32, T20, X33))
U3_ga(T19, T20, T21, X33, pE_out_gagaga(T19, X31, T21, X32, T20, X33)) → inorderD_out_ga(tree(T19, T20, T21), X33)
pE_in_gagaga(T19, T22, T21, X32, T20, X33) → U8_gagaga(T19, T22, T21, X32, T20, X33, inorderD_in_ga(T19, T22))
U8_gagaga(T19, T22, T21, X32, T20, X33, inorderD_out_ga(T19, T22)) → U9_gagaga(T19, T22, T21, X32, T20, X33, pI_in_gagga(T21, X32, T22, T20, X33))
U9_gagaga(T19, T22, T21, X32, T20, X33, pI_out_gagga(T21, X32, T22, T20, X33)) → pE_out_gagaga(T19, T22, T21, X32, T20, X33)
pI_in_gagga(T21, T23, T22, T20, X33) → U10_gagga(T21, T23, T22, T20, X33, inorderD_in_ga(T21, T23))
U10_gagga(T21, T23, T22, T20, X33, inorderD_out_ga(T21, T23)) → U11_gagga(T21, T23, T22, T20, X33, appendF_in_ggga(T22, T20, T23, X33))
U11_gagga(T21, T23, T22, T20, X33, appendF_out_ggga(T22, T20, T23, X33)) → pI_out_gagga(T21, T23, T22, T20, X33)
appendF_in_ggga([], T36, T37, .(T36, T37)) → appendF_out_ggga([], T36, T37, .(T36, T37))
appendF_in_ggga(.(T46, T47), T48, T49, .(T46, X55)) → U4_ggga(T46, T47, T48, T49, X55, appendF_in_ggga(T47, T48, T49, X55))
U4_ggga(T46, T47, T48, T49, X55, appendF_out_ggga(T47, T48, T49, X55)) → appendF_out_ggga(.(T46, T47), T48, T49, .(T46, X55))

The argument filtering Pi contains the following mapping:
nil  =  nil
tree(x1, x2, x3)  =  tree(x1, x2, x3)
inorderD_in_ga(x1, x2)  =  inorderD_in_ga(x1)
inorderD_out_ga(x1, x2)  =  inorderD_out_ga(x1, x2)
U3_ga(x1, x2, x3, x4, x5)  =  U3_ga(x1, x2, x3, x5)
pE_in_gagaga(x1, x2, x3, x4, x5, x6)  =  pE_in_gagaga(x1, x3, x5)
U8_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U8_gagaga(x1, x3, x5, x7)
U9_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U9_gagaga(x1, x2, x3, x5, x7)
pI_in_gagga(x1, x2, x3, x4, x5)  =  pI_in_gagga(x1, x3, x4)
U10_gagga(x1, x2, x3, x4, x5, x6)  =  U10_gagga(x1, x3, x4, x6)
U11_gagga(x1, x2, x3, x4, x5, x6)  =  U11_gagga(x1, x2, x3, x4, x6)
appendF_in_ggga(x1, x2, x3, x4)  =  appendF_in_ggga(x1, x2, x3)
[]  =  []
appendF_out_ggga(x1, x2, x3, x4)  =  appendF_out_ggga(x1, x2, x3, x4)
.(x1, x2)  =  .(x1, x2)
U4_ggga(x1, x2, x3, x4, x5, x6)  =  U4_ggga(x1, x2, x3, x4, x6)
pI_out_gagga(x1, x2, x3, x4, x5)  =  pI_out_gagga(x1, x2, x3, x4, x5)
pE_out_gagaga(x1, x2, x3, x4, x5, x6)  =  pE_out_gagaga(x1, x2, x3, x4, x5, x6)
INORDERD_IN_GA(x1, x2)  =  INORDERD_IN_GA(x1)
PE_IN_GAGAGA(x1, x2, x3, x4, x5, x6)  =  PE_IN_GAGAGA(x1, x3, x5)
U8_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U8_GAGAGA(x1, x3, x5, x7)
PI_IN_GAGGA(x1, x2, x3, x4, x5)  =  PI_IN_GAGGA(x1, x3, x4)

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

INORDERD_IN_GA(tree(T19, T20, T21)) → PE_IN_GAGAGA(T19, T21, T20)
PE_IN_GAGAGA(T19, T21, T20) → U8_GAGAGA(T19, T21, T20, inorderD_in_ga(T19))
U8_GAGAGA(T19, T21, T20, inorderD_out_ga(T19, T22)) → PI_IN_GAGGA(T21, T22, T20)
PI_IN_GAGGA(T21, T22, T20) → INORDERD_IN_GA(T21)
PE_IN_GAGAGA(T19, T21, T20) → INORDERD_IN_GA(T19)

The TRS R consists of the following rules:

inorderD_in_ga(nil) → inorderD_out_ga(nil, [])
inorderD_in_ga(tree(T19, T20, T21)) → U3_ga(T19, T20, T21, pE_in_gagaga(T19, T21, T20))
U3_ga(T19, T20, T21, pE_out_gagaga(T19, X31, T21, X32, T20, X33)) → inorderD_out_ga(tree(T19, T20, T21), X33)
pE_in_gagaga(T19, T21, T20) → U8_gagaga(T19, T21, T20, inorderD_in_ga(T19))
U8_gagaga(T19, T21, T20, inorderD_out_ga(T19, T22)) → U9_gagaga(T19, T22, T21, T20, pI_in_gagga(T21, T22, T20))
U9_gagaga(T19, T22, T21, T20, pI_out_gagga(T21, X32, T22, T20, X33)) → pE_out_gagaga(T19, T22, T21, X32, T20, X33)
pI_in_gagga(T21, T22, T20) → U10_gagga(T21, T22, T20, inorderD_in_ga(T21))
U10_gagga(T21, T22, T20, inorderD_out_ga(T21, T23)) → U11_gagga(T21, T23, T22, T20, appendF_in_ggga(T22, T20, T23))
U11_gagga(T21, T23, T22, T20, appendF_out_ggga(T22, T20, T23, X33)) → pI_out_gagga(T21, T23, T22, T20, X33)
appendF_in_ggga([], T36, T37) → appendF_out_ggga([], T36, T37, .(T36, T37))
appendF_in_ggga(.(T46, T47), T48, T49) → U4_ggga(T46, T47, T48, T49, appendF_in_ggga(T47, T48, T49))
U4_ggga(T46, T47, T48, T49, appendF_out_ggga(T47, T48, T49, X55)) → appendF_out_ggga(.(T46, T47), T48, T49, .(T46, X55))

The set Q consists of the following terms:

inorderD_in_ga(x0)
U3_ga(x0, x1, x2, x3)
pE_in_gagaga(x0, x1, x2)
U8_gagaga(x0, x1, x2, x3)
U9_gagaga(x0, x1, x2, x3, x4)
pI_in_gagga(x0, x1, x2)
U10_gagga(x0, x1, x2, x3)
U11_gagga(x0, x1, x2, x3, x4)
appendF_in_ggga(x0, x1, x2)
U4_ggga(x0, x1, x2, x3, x4)

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:

• PE_IN_GAGAGA(T19, T21, T20) → INORDERD_IN_GA(T19)
  The graph contains the following edges 1 >= 1

• PE_IN_GAGAGA(T19, T21, T20) → U8_GAGAGA(T19, T21, T20, inorderD_in_ga(T19))
  The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3

• PI_IN_GAGGA(T21, T22, T20) → INORDERD_IN_GA(T21)
  The graph contains the following edges 1 >= 1

• U8_GAGAGA(T19, T21, T20, inorderD_out_ga(T19, T22)) → PI_IN_GAGGA(T21, T22, T20)
  The graph contains the following edges 2 >= 1, 4 > 2, 3 >= 3

• INORDERD_IN_GA(tree(T19, T20, T21)) → PE_IN_GAGAGA(T19, T21, T20)
  The graph contains the following edges 1 > 1, 1 > 2, 1 > 3

(27) YES