Left Termination proof of /tmp/tmpz8hbg3/inorder-bf.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 180 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 452 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 14 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇒, 0 ms)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔, 0 ms)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇒, 0 ms)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔, 0 ms)

        ↳20 YES

    ↳21 PiDP

        ↳22 UsableRulesProof (⇔, 0 ms)

        ↳23 PiDP

        ↳24 PiDPToQDPProof (⇒, 25 ms)

        ↳25 QDP

        ↳26 QDPSizeChangeProof (⇔, 0 ms)

        ↳27 YES

(0) Obligation:

Clauses:

in_order(void, []).
in_order(tree(X, Left, Right), Xs) :- ','(in_order(Left, Ls), ','(in_order(Right, Rs), app(Ls, .(X, Rs), Xs))).
app([], X, X).
app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs).

Query: in_order(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: in_order(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: in_order(T1, T2), SCOPE: 1, CLAUSE: 0 | in_order(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: true | in_order(void, T2), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: in_order(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nin_order(T1, T2) !=? in_order(void, [])", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: in_order(void, T2), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(in_order(T8, X13), ','(in_order(T9, X14), app(X13, .(T7, X14), T11)))\n\nT7 is ground\nT8 is ground\nT9 is ground\nX13 is free\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(in_order(T8, X13), ','(in_order(T9, X14), app(X13, .(T7, X14), T11))), SCOPE: 2, CLAUSE: 0 | ','(in_order(T8, X13), ','(in_order(T9, X14), app(X13, .(T7, 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];
28 [label="28: ','(in_order(T8, X13), ','(in_order(T9, X14), app(X13, .(T7, 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];
30 [label="30: ','(in_order(T8, X13), ','(in_order(T9, X14), app(X13, .(T7, 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];
34 [label="B: ','(in_order(T9, X14), app([], .(T7, X14), T11))\n\nT7 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];
40 [label="D: in_order(T9, X14)\n\nT9 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="H: app([], .(T7, T12), T11)\n\nT7 is ground\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: in_order(T9, X14), SCOPE: 3, CLAUSE: 0 | in_order(T9, X14), SCOPE: 3, CLAUSE: 1\n\nT9 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: in_order(T9, X14), SCOPE: 3, CLAUSE: 0\n\nT9 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: in_order(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];
54 [label="54: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="E: ','(in_order(T20, X31), ','(in_order(T21, X32), app(X31, .(T19, 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];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: in_order(T20, X31)\n\nT20 is ground\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="I: ','(in_order(T21, X32), app(T22, .(T19, X32), X33))\n\nT19 is ground\nT21 is ground\nT22 is ground\nX33 is free\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: in_order(T21, X32)\n\nT21 is ground\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="F: app(T22, .(T19, T23), X33)\n\nT19 is ground\nT22 is ground\nT23 is ground\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: app(T22, .(T19, T23), X33), SCOPE: 4, CLAUSE: 2 | app(T22, .(T19, T23), X33), SCOPE: 4, CLAUSE: 3\n\nT19 is ground\nT22 is ground\nT23 is ground\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: app(T22, .(T19, T23), X33), SCOPE: 4, CLAUSE: 2\n\nT19 is ground\nT22 is ground\nT23 is ground\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: app(T22, .(T19, T23), X33), SCOPE: 4, CLAUSE: 3\n\nT19 is ground\nT22 is ground\nT23 is ground\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: app(T47, .(T48, T49), X55)\n\nT47 is ground\nT48 is ground\nT49 is ground\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: app([], .(T7, T12), T11), SCOPE: 5, CLAUSE: 2 | app([], .(T7, T12), T11), SCOPE: 5, CLAUSE: 3\n\nT7 is ground\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: app([], .(T7, T12), T11), SCOPE: 5, CLAUSE: 2\n\nT7 is ground\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: app([], .(T7, T12), T11), SCOPE: 5, CLAUSE: 3\n\nT7 is ground\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="C: ','(','(in_order(T75, X85), ','(in_order(T76, X86), app(X85, .(T74, X86), X87))), ','(in_order(T9, X14), app(X87, .(T7, X14), T11)))\n\nT7 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];
129 [label="129: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: in_order(T75, X85)\n\nT75 is ground\nX85 is free", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="J: ','(','(in_order(T76, X86), app(T77, .(T74, X86), X87)), ','(in_order(T9, X14), app(X87, .(T7, X14), T11)))\n\nT7 is ground\nT9 is ground\nT74 is ground\nT76 is ground\nT77 is ground\nX14 is free\nX87 is free\nX86 is free", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: in_order(T76, X86)\n\nT76 is ground\nX86 is free", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="K: ','(app(T77, .(T74, T78), X87), ','(in_order(T9, X14), app(X87, .(T7, X14), T11)))\n\nT7 is ground\nT9 is ground\nT74 is ground\nT77 is ground\nT78 is ground\nX14 is free\nX87 is free", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: app(T77, .(T74, T78), X87)\n\nT74 is ground\nT77 is ground\nT78 is ground\nX87 is free", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="L: ','(in_order(T9, X14), app(T83, .(T7, X14), T11))\n\nT7 is ground\nT9 is ground\nT83 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: in_order(T9, X14)\n\nT9 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="G: app(T83, .(T7, T88), T11)\n\nT7 is ground\nT83 is ground\nT88 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: app(T83, .(T7, T88), T11), SCOPE: 6, CLAUSE: 2 | app(T83, .(T7, T88), T11), SCOPE: 6, CLAUSE: 3\n\nT7 is ground\nT83 is ground\nT88 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
155 [label="155: app(T83, .(T7, T88), T11), SCOPE: 6, CLAUSE: 2\n\nT7 is ground\nT83 is ground\nT88 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: app(T83, .(T7, T88), T11), SCOPE: 6, CLAUSE: 3\n\nT7 is ground\nT83 is ground\nT88 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: app(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];
1 -> 162 [arrowhead = none ];
162 -> 6;

163 [label="EVAL with clause\nin_order(void, []).\nand substitutionT1 -> void,\nT2 -> []", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 163 [arrowhead = none ];
163 -> 10;

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

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

166 [label="EVAL with clause\nin_order(tree(X9, X10, X11), X12) :- ','(in_order(X10, X13), ','(in_order(X11, X14), app(X13, .(X9, 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];
13 -> 166 [arrowhead = none ];
166 -> 22;

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

168 [label="BACKTRACK\nfor clause: in_order(tree(X, Left, Right), Xs) :- ','(in_order(Left, Ls), ','(in_order(Right, Rs), app(Ls, .(X, Rs), Xs)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 168 [arrowhead = none ];
168 -> 18;

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

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

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

172 [label="EVAL with clause\nin_order(void, []).\nand substitutionT8 -> void,\nX13 -> []", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 172 [arrowhead = none ];
172 -> 34;

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

174 [label="EVAL with clause\nin_order(tree(X81, X82, X83), X84) :- ','(in_order(X82, X85), ','(in_order(X83, X86), app(X85, .(X81, X86), X84))).\nand substitutionX81 -> T74,\nX82 -> T75,\nX83 -> T76,\nT8 -> tree(T74, T75, T76),\nX13 -> X87,\nX84 -> X87", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 174 [arrowhead = none ];
174 -> 128;

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

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

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

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

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

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

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

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

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

184 [label="EVAL with clause\nin_order(tree(X27, X28, X29), X30) :- ','(in_order(X28, X31), ','(in_order(X29, X32), app(X31, .(X27, 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 -> 60;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

216 [label="INSTANCE with matching:\nT22 -> T77\nT19 -> T74\nT23 -> T78\nX33 -> X87", fontsize=14, style = filled, fillcolor = lightgrey];
143 -> 216 [arrowhead = none , style=dashed];
216 -> 81[style=dashed];

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

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

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

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

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

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

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

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

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

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

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

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

}

(2) Obligation:

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

in_orderA_in_ga(void, []) → in_orderA_out_ga(void, [])
in_orderA_in_ga(tree(T7, void, T9), T11) → U1_ga(T7, T9, T11, pB_in_gaga(T9, X14, T7, T11))
pB_in_gaga(T9, T12, T7, T11) → U6_gaga(T9, T12, T7, T11, in_orderD_in_ga(T9, T12))
in_orderD_in_ga(void, []) → in_orderD_out_ga(void, [])
in_orderD_in_ga(tree(T19, T20, T21), X33) → U3_ga(T19, T20, T21, X33, pE_in_gagaga(T20, X31, T21, X32, T19, X33))
pE_in_gagaga(T20, T22, T21, X32, T19, X33) → U8_gagaga(T20, T22, T21, X32, T19, X33, in_orderD_in_ga(T20, T22))
U8_gagaga(T20, T22, T21, X32, T19, X33, in_orderD_out_ga(T20, T22)) → U9_gagaga(T20, T22, T21, X32, T19, X33, pI_in_gagga(T21, X32, T22, T19, X33))
pI_in_gagga(T21, T23, T22, T19, X33) → U10_gagga(T21, T23, T22, T19, X33, in_orderD_in_ga(T21, T23))
U10_gagga(T21, T23, T22, T19, X33, in_orderD_out_ga(T21, T23)) → U11_gagga(T21, T23, T22, T19, X33, appF_in_ggga(T22, T19, T23, X33))
appF_in_ggga([], T36, T37, .(T36, T37)) → appF_out_ggga([], T36, T37, .(T36, T37))
appF_in_ggga(.(T46, T47), T48, T49, .(T46, X55)) → U4_ggga(T46, T47, T48, T49, X55, appF_in_ggga(T47, T48, T49, X55))
U4_ggga(T46, T47, T48, T49, X55, appF_out_ggga(T47, T48, T49, X55)) → appF_out_ggga(.(T46, T47), T48, T49, .(T46, X55))
U11_gagga(T21, T23, T22, T19, X33, appF_out_ggga(T22, T19, T23, X33)) → pI_out_gagga(T21, T23, T22, T19, X33)
U9_gagaga(T20, T22, T21, X32, T19, X33, pI_out_gagga(T21, X32, T22, T19, X33)) → pE_out_gagaga(T20, T22, T21, X32, T19, X33)
U3_ga(T19, T20, T21, X33, pE_out_gagaga(T20, X31, T21, X32, T19, X33)) → in_orderD_out_ga(tree(T19, T20, T21), X33)
U6_gaga(T9, T12, T7, T11, in_orderD_out_ga(T9, T12)) → U7_gaga(T9, T12, T7, T11, appH_in_gga(T7, T12, T11))
appH_in_gga(T66, T67, .(T66, T67)) → appH_out_gga(T66, T67, .(T66, T67))
U7_gaga(T9, T12, T7, T11, appH_out_gga(T7, T12, T11)) → pB_out_gaga(T9, T12, T7, T11)
U1_ga(T7, T9, T11, pB_out_gaga(T9, X14, T7, T11)) → in_orderA_out_ga(tree(T7, void, T9), T11)
in_orderA_in_ga(tree(T7, tree(T74, T75, T76), T9), T11) → U2_ga(T7, T74, T75, T76, T9, T11, pC_in_gagagagaga(T75, X85, T76, X86, T74, X87, T9, X14, T7, T11))
pC_in_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11) → U12_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, in_orderD_in_ga(T75, T77))
U12_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, in_orderD_out_ga(T75, T77)) → U13_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, pJ_in_gaggagaga(T76, X86, T77, T74, X87, T9, X14, T7, T11))
pJ_in_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11) → U14_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11, in_orderD_in_ga(T76, T78))
U14_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11, in_orderD_out_ga(T76, T78)) → U15_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11, pK_in_gggagaga(T77, T74, T78, X87, T9, X14, T7, T11))
pK_in_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11) → U16_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11, appF_in_ggga(T77, T74, T78, T83))
U16_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11, appF_out_ggga(T77, T74, T78, T83)) → U17_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11, pL_in_gagga(T9, X14, T83, T7, T11))
pL_in_gagga(T9, T88, T83, T7, T11) → U18_gagga(T9, T88, T83, T7, T11, in_orderD_in_ga(T9, T88))
U18_gagga(T9, T88, T83, T7, T11, in_orderD_out_ga(T9, T88)) → U19_gagga(T9, T88, T83, T7, T11, appG_in_ggga(T83, T7, T88, T11))
appG_in_ggga([], T101, T102, .(T101, T102)) → appG_out_ggga([], T101, T102, .(T101, T102))
appG_in_ggga(.(T113, T114), T115, T116, .(T113, T118)) → U5_ggga(T113, T114, T115, T116, T118, appG_in_ggga(T114, T115, T116, T118))
U5_ggga(T113, T114, T115, T116, T118, appG_out_ggga(T114, T115, T116, T118)) → appG_out_ggga(.(T113, T114), T115, T116, .(T113, T118))
U19_gagga(T9, T88, T83, T7, T11, appG_out_ggga(T83, T7, T88, T11)) → pL_out_gagga(T9, T88, T83, T7, T11)
U17_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11, pL_out_gagga(T9, X14, T83, T7, T11)) → pK_out_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11)
U15_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11, pK_out_gggagaga(T77, T74, T78, X87, T9, X14, T7, T11)) → pJ_out_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11)
U13_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, pJ_out_gaggagaga(T76, X86, T77, T74, X87, T9, X14, T7, T11)) → pC_out_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11)
U2_ga(T7, T74, T75, T76, T9, T11, pC_out_gagagagaga(T75, X85, T76, X86, T74, X87, T9, X14, T7, T11)) → in_orderA_out_ga(tree(T7, tree(T74, T75, T76), T9), T11)

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

IN_ORDERA_IN_GA(tree(T7, void, T9), T11) → U1_GA(T7, T9, T11, pB_in_gaga(T9, X14, T7, T11))
IN_ORDERA_IN_GA(tree(T7, void, T9), T11) → PB_IN_GAGA(T9, X14, T7, T11)
PB_IN_GAGA(T9, T12, T7, T11) → U6_GAGA(T9, T12, T7, T11, in_orderD_in_ga(T9, T12))
PB_IN_GAGA(T9, T12, T7, T11) → IN_ORDERD_IN_GA(T9, T12)
IN_ORDERD_IN_GA(tree(T19, T20, T21), X33) → U3_GA(T19, T20, T21, X33, pE_in_gagaga(T20, X31, T21, X32, T19, X33))
IN_ORDERD_IN_GA(tree(T19, T20, T21), X33) → PE_IN_GAGAGA(T20, X31, T21, X32, T19, X33)
PE_IN_GAGAGA(T20, T22, T21, X32, T19, X33) → U8_GAGAGA(T20, T22, T21, X32, T19, X33, in_orderD_in_ga(T20, T22))
PE_IN_GAGAGA(T20, T22, T21, X32, T19, X33) → IN_ORDERD_IN_GA(T20, T22)
U8_GAGAGA(T20, T22, T21, X32, T19, X33, in_orderD_out_ga(T20, T22)) → U9_GAGAGA(T20, T22, T21, X32, T19, X33, pI_in_gagga(T21, X32, T22, T19, X33))
U8_GAGAGA(T20, T22, T21, X32, T19, X33, in_orderD_out_ga(T20, T22)) → PI_IN_GAGGA(T21, X32, T22, T19, X33)
PI_IN_GAGGA(T21, T23, T22, T19, X33) → U10_GAGGA(T21, T23, T22, T19, X33, in_orderD_in_ga(T21, T23))
PI_IN_GAGGA(T21, T23, T22, T19, X33) → IN_ORDERD_IN_GA(T21, T23)
U10_GAGGA(T21, T23, T22, T19, X33, in_orderD_out_ga(T21, T23)) → U11_GAGGA(T21, T23, T22, T19, X33, appF_in_ggga(T22, T19, T23, X33))
U10_GAGGA(T21, T23, T22, T19, X33, in_orderD_out_ga(T21, T23)) → APPF_IN_GGGA(T22, T19, T23, X33)
APPF_IN_GGGA(.(T46, T47), T48, T49, .(T46, X55)) → U4_GGGA(T46, T47, T48, T49, X55, appF_in_ggga(T47, T48, T49, X55))
APPF_IN_GGGA(.(T46, T47), T48, T49, .(T46, X55)) → APPF_IN_GGGA(T47, T48, T49, X55)
U6_GAGA(T9, T12, T7, T11, in_orderD_out_ga(T9, T12)) → U7_GAGA(T9, T12, T7, T11, appH_in_gga(T7, T12, T11))
U6_GAGA(T9, T12, T7, T11, in_orderD_out_ga(T9, T12)) → APPH_IN_GGA(T7, T12, T11)
IN_ORDERA_IN_GA(tree(T7, tree(T74, T75, T76), T9), T11) → U2_GA(T7, T74, T75, T76, T9, T11, pC_in_gagagagaga(T75, X85, T76, X86, T74, X87, T9, X14, T7, T11))
IN_ORDERA_IN_GA(tree(T7, tree(T74, T75, T76), T9), T11) → PC_IN_GAGAGAGAGA(T75, X85, T76, X86, T74, X87, T9, X14, T7, T11)
PC_IN_GAGAGAGAGA(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11) → U12_GAGAGAGAGA(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, in_orderD_in_ga(T75, T77))
PC_IN_GAGAGAGAGA(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11) → IN_ORDERD_IN_GA(T75, T77)
U12_GAGAGAGAGA(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, in_orderD_out_ga(T75, T77)) → U13_GAGAGAGAGA(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, pJ_in_gaggagaga(T76, X86, T77, T74, X87, T9, X14, T7, T11))
U12_GAGAGAGAGA(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, in_orderD_out_ga(T75, T77)) → PJ_IN_GAGGAGAGA(T76, X86, T77, T74, X87, T9, X14, T7, T11)
PJ_IN_GAGGAGAGA(T76, T78, T77, T74, X87, T9, X14, T7, T11) → U14_GAGGAGAGA(T76, T78, T77, T74, X87, T9, X14, T7, T11, in_orderD_in_ga(T76, T78))
PJ_IN_GAGGAGAGA(T76, T78, T77, T74, X87, T9, X14, T7, T11) → IN_ORDERD_IN_GA(T76, T78)
U14_GAGGAGAGA(T76, T78, T77, T74, X87, T9, X14, T7, T11, in_orderD_out_ga(T76, T78)) → U15_GAGGAGAGA(T76, T78, T77, T74, X87, T9, X14, T7, T11, pK_in_gggagaga(T77, T74, T78, X87, T9, X14, T7, T11))
U14_GAGGAGAGA(T76, T78, T77, T74, X87, T9, X14, T7, T11, in_orderD_out_ga(T76, T78)) → PK_IN_GGGAGAGA(T77, T74, T78, X87, T9, X14, T7, T11)
PK_IN_GGGAGAGA(T77, T74, T78, T83, T9, X14, T7, T11) → U16_GGGAGAGA(T77, T74, T78, T83, T9, X14, T7, T11, appF_in_ggga(T77, T74, T78, T83))
PK_IN_GGGAGAGA(T77, T74, T78, T83, T9, X14, T7, T11) → APPF_IN_GGGA(T77, T74, T78, T83)
U16_GGGAGAGA(T77, T74, T78, T83, T9, X14, T7, T11, appF_out_ggga(T77, T74, T78, T83)) → U17_GGGAGAGA(T77, T74, T78, T83, T9, X14, T7, T11, pL_in_gagga(T9, X14, T83, T7, T11))
U16_GGGAGAGA(T77, T74, T78, T83, T9, X14, T7, T11, appF_out_ggga(T77, T74, T78, T83)) → PL_IN_GAGGA(T9, X14, T83, T7, T11)
PL_IN_GAGGA(T9, T88, T83, T7, T11) → U18_GAGGA(T9, T88, T83, T7, T11, in_orderD_in_ga(T9, T88))
PL_IN_GAGGA(T9, T88, T83, T7, T11) → IN_ORDERD_IN_GA(T9, T88)
U18_GAGGA(T9, T88, T83, T7, T11, in_orderD_out_ga(T9, T88)) → U19_GAGGA(T9, T88, T83, T7, T11, appG_in_ggga(T83, T7, T88, T11))
U18_GAGGA(T9, T88, T83, T7, T11, in_orderD_out_ga(T9, T88)) → APPG_IN_GGGA(T83, T7, T88, T11)
APPG_IN_GGGA(.(T113, T114), T115, T116, .(T113, T118)) → U5_GGGA(T113, T114, T115, T116, T118, appG_in_ggga(T114, T115, T116, T118))
APPG_IN_GGGA(.(T113, T114), T115, T116, .(T113, T118)) → APPG_IN_GGGA(T114, T115, T116, T118)

The TRS R consists of the following rules:

in_orderA_in_ga(void, []) → in_orderA_out_ga(void, [])
in_orderA_in_ga(tree(T7, void, T9), T11) → U1_ga(T7, T9, T11, pB_in_gaga(T9, X14, T7, T11))
pB_in_gaga(T9, T12, T7, T11) → U6_gaga(T9, T12, T7, T11, in_orderD_in_ga(T9, T12))
in_orderD_in_ga(void, []) → in_orderD_out_ga(void, [])
in_orderD_in_ga(tree(T19, T20, T21), X33) → U3_ga(T19, T20, T21, X33, pE_in_gagaga(T20, X31, T21, X32, T19, X33))
pE_in_gagaga(T20, T22, T21, X32, T19, X33) → U8_gagaga(T20, T22, T21, X32, T19, X33, in_orderD_in_ga(T20, T22))
U8_gagaga(T20, T22, T21, X32, T19, X33, in_orderD_out_ga(T20, T22)) → U9_gagaga(T20, T22, T21, X32, T19, X33, pI_in_gagga(T21, X32, T22, T19, X33))
pI_in_gagga(T21, T23, T22, T19, X33) → U10_gagga(T21, T23, T22, T19, X33, in_orderD_in_ga(T21, T23))
U10_gagga(T21, T23, T22, T19, X33, in_orderD_out_ga(T21, T23)) → U11_gagga(T21, T23, T22, T19, X33, appF_in_ggga(T22, T19, T23, X33))
appF_in_ggga([], T36, T37, .(T36, T37)) → appF_out_ggga([], T36, T37, .(T36, T37))
appF_in_ggga(.(T46, T47), T48, T49, .(T46, X55)) → U4_ggga(T46, T47, T48, T49, X55, appF_in_ggga(T47, T48, T49, X55))
U4_ggga(T46, T47, T48, T49, X55, appF_out_ggga(T47, T48, T49, X55)) → appF_out_ggga(.(T46, T47), T48, T49, .(T46, X55))
U11_gagga(T21, T23, T22, T19, X33, appF_out_ggga(T22, T19, T23, X33)) → pI_out_gagga(T21, T23, T22, T19, X33)
U9_gagaga(T20, T22, T21, X32, T19, X33, pI_out_gagga(T21, X32, T22, T19, X33)) → pE_out_gagaga(T20, T22, T21, X32, T19, X33)
U3_ga(T19, T20, T21, X33, pE_out_gagaga(T20, X31, T21, X32, T19, X33)) → in_orderD_out_ga(tree(T19, T20, T21), X33)
U6_gaga(T9, T12, T7, T11, in_orderD_out_ga(T9, T12)) → U7_gaga(T9, T12, T7, T11, appH_in_gga(T7, T12, T11))
appH_in_gga(T66, T67, .(T66, T67)) → appH_out_gga(T66, T67, .(T66, T67))
U7_gaga(T9, T12, T7, T11, appH_out_gga(T7, T12, T11)) → pB_out_gaga(T9, T12, T7, T11)
U1_ga(T7, T9, T11, pB_out_gaga(T9, X14, T7, T11)) → in_orderA_out_ga(tree(T7, void, T9), T11)
in_orderA_in_ga(tree(T7, tree(T74, T75, T76), T9), T11) → U2_ga(T7, T74, T75, T76, T9, T11, pC_in_gagagagaga(T75, X85, T76, X86, T74, X87, T9, X14, T7, T11))
pC_in_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11) → U12_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, in_orderD_in_ga(T75, T77))
U12_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, in_orderD_out_ga(T75, T77)) → U13_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, pJ_in_gaggagaga(T76, X86, T77, T74, X87, T9, X14, T7, T11))
pJ_in_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11) → U14_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11, in_orderD_in_ga(T76, T78))
U14_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11, in_orderD_out_ga(T76, T78)) → U15_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11, pK_in_gggagaga(T77, T74, T78, X87, T9, X14, T7, T11))
pK_in_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11) → U16_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11, appF_in_ggga(T77, T74, T78, T83))
U16_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11, appF_out_ggga(T77, T74, T78, T83)) → U17_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11, pL_in_gagga(T9, X14, T83, T7, T11))
pL_in_gagga(T9, T88, T83, T7, T11) → U18_gagga(T9, T88, T83, T7, T11, in_orderD_in_ga(T9, T88))
U18_gagga(T9, T88, T83, T7, T11, in_orderD_out_ga(T9, T88)) → U19_gagga(T9, T88, T83, T7, T11, appG_in_ggga(T83, T7, T88, T11))
appG_in_ggga([], T101, T102, .(T101, T102)) → appG_out_ggga([], T101, T102, .(T101, T102))
appG_in_ggga(.(T113, T114), T115, T116, .(T113, T118)) → U5_ggga(T113, T114, T115, T116, T118, appG_in_ggga(T114, T115, T116, T118))
U5_ggga(T113, T114, T115, T116, T118, appG_out_ggga(T114, T115, T116, T118)) → appG_out_ggga(.(T113, T114), T115, T116, .(T113, T118))
U19_gagga(T9, T88, T83, T7, T11, appG_out_ggga(T83, T7, T88, T11)) → pL_out_gagga(T9, T88, T83, T7, T11)
U17_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11, pL_out_gagga(T9, X14, T83, T7, T11)) → pK_out_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11)
U15_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11, pK_out_gggagaga(T77, T74, T78, X87, T9, X14, T7, T11)) → pJ_out_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11)
U13_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, pJ_out_gaggagaga(T76, X86, T77, T74, X87, T9, X14, T7, T11)) → pC_out_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11)
U2_ga(T7, T74, T75, T76, T9, T11, pC_out_gagagagaga(T75, X85, T76, X86, T74, X87, T9, X14, T7, T11)) → in_orderA_out_ga(tree(T7, tree(T74, T75, T76), T9), T11)

The argument filtering Pi contains the following mapping:
in_orderA_in_ga(x1, x2) = in_orderA_in_ga(x1)
void = void
in_orderA_out_ga(x1, x2) = in_orderA_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)
in_orderD_in_ga(x1, x2) = in_orderD_in_ga(x1)
in_orderD_out_ga(x1, x2) = in_orderD_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)
appF_in_ggga(x1, x2, x3, x4) = appF_in_ggga(x1, x2, x3)
[] = []
appF_out_ggga(x1, x2, x3, x4) = appF_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)
appH_in_gga(x1, x2, x3) = appH_in_gga(x1, x2)
appH_out_gga(x1, x2, x3) = appH_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)
appG_in_ggga(x1, x2, x3, x4) = appG_in_ggga(x1, x2, x3)
appG_out_ggga(x1, x2, x3, x4) = appG_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)
IN_ORDERA_IN_GA(x1, x2) = IN_ORDERA_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)
IN_ORDERD_IN_GA(x1, x2) = IN_ORDERD_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)
APPF_IN_GGGA(x1, x2, x3, x4) = APPF_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)
APPH_IN_GGA(x1, x2, x3) = APPH_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)
APPG_IN_GGGA(x1, x2, x3, x4) = APPG_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:

IN_ORDERA_IN_GA(tree(T7, void, T9), T11) → U1_GA(T7, T9, T11, pB_in_gaga(T9, X14, T7, T11))
IN_ORDERA_IN_GA(tree(T7, void, T9), T11) → PB_IN_GAGA(T9, X14, T7, T11)
PB_IN_GAGA(T9, T12, T7, T11) → U6_GAGA(T9, T12, T7, T11, in_orderD_in_ga(T9, T12))
PB_IN_GAGA(T9, T12, T7, T11) → IN_ORDERD_IN_GA(T9, T12)
IN_ORDERD_IN_GA(tree(T19, T20, T21), X33) → U3_GA(T19, T20, T21, X33, pE_in_gagaga(T20, X31, T21, X32, T19, X33))
IN_ORDERD_IN_GA(tree(T19, T20, T21), X33) → PE_IN_GAGAGA(T20, X31, T21, X32, T19, X33)
PE_IN_GAGAGA(T20, T22, T21, X32, T19, X33) → U8_GAGAGA(T20, T22, T21, X32, T19, X33, in_orderD_in_ga(T20, T22))
PE_IN_GAGAGA(T20, T22, T21, X32, T19, X33) → IN_ORDERD_IN_GA(T20, T22)
U8_GAGAGA(T20, T22, T21, X32, T19, X33, in_orderD_out_ga(T20, T22)) → U9_GAGAGA(T20, T22, T21, X32, T19, X33, pI_in_gagga(T21, X32, T22, T19, X33))
U8_GAGAGA(T20, T22, T21, X32, T19, X33, in_orderD_out_ga(T20, T22)) → PI_IN_GAGGA(T21, X32, T22, T19, X33)
PI_IN_GAGGA(T21, T23, T22, T19, X33) → U10_GAGGA(T21, T23, T22, T19, X33, in_orderD_in_ga(T21, T23))
PI_IN_GAGGA(T21, T23, T22, T19, X33) → IN_ORDERD_IN_GA(T21, T23)
U10_GAGGA(T21, T23, T22, T19, X33, in_orderD_out_ga(T21, T23)) → U11_GAGGA(T21, T23, T22, T19, X33, appF_in_ggga(T22, T19, T23, X33))
U10_GAGGA(T21, T23, T22, T19, X33, in_orderD_out_ga(T21, T23)) → APPF_IN_GGGA(T22, T19, T23, X33)
APPF_IN_GGGA(.(T46, T47), T48, T49, .(T46, X55)) → U4_GGGA(T46, T47, T48, T49, X55, appF_in_ggga(T47, T48, T49, X55))
APPF_IN_GGGA(.(T46, T47), T48, T49, .(T46, X55)) → APPF_IN_GGGA(T47, T48, T49, X55)
U6_GAGA(T9, T12, T7, T11, in_orderD_out_ga(T9, T12)) → U7_GAGA(T9, T12, T7, T11, appH_in_gga(T7, T12, T11))
U6_GAGA(T9, T12, T7, T11, in_orderD_out_ga(T9, T12)) → APPH_IN_GGA(T7, T12, T11)
IN_ORDERA_IN_GA(tree(T7, tree(T74, T75, T76), T9), T11) → U2_GA(T7, T74, T75, T76, T9, T11, pC_in_gagagagaga(T75, X85, T76, X86, T74, X87, T9, X14, T7, T11))
IN_ORDERA_IN_GA(tree(T7, tree(T74, T75, T76), T9), T11) → PC_IN_GAGAGAGAGA(T75, X85, T76, X86, T74, X87, T9, X14, T7, T11)
PC_IN_GAGAGAGAGA(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11) → U12_GAGAGAGAGA(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, in_orderD_in_ga(T75, T77))
PC_IN_GAGAGAGAGA(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11) → IN_ORDERD_IN_GA(T75, T77)
U12_GAGAGAGAGA(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, in_orderD_out_ga(T75, T77)) → U13_GAGAGAGAGA(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, pJ_in_gaggagaga(T76, X86, T77, T74, X87, T9, X14, T7, T11))
U12_GAGAGAGAGA(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, in_orderD_out_ga(T75, T77)) → PJ_IN_GAGGAGAGA(T76, X86, T77, T74, X87, T9, X14, T7, T11)
PJ_IN_GAGGAGAGA(T76, T78, T77, T74, X87, T9, X14, T7, T11) → U14_GAGGAGAGA(T76, T78, T77, T74, X87, T9, X14, T7, T11, in_orderD_in_ga(T76, T78))
PJ_IN_GAGGAGAGA(T76, T78, T77, T74, X87, T9, X14, T7, T11) → IN_ORDERD_IN_GA(T76, T78)
U14_GAGGAGAGA(T76, T78, T77, T74, X87, T9, X14, T7, T11, in_orderD_out_ga(T76, T78)) → U15_GAGGAGAGA(T76, T78, T77, T74, X87, T9, X14, T7, T11, pK_in_gggagaga(T77, T74, T78, X87, T9, X14, T7, T11))
U14_GAGGAGAGA(T76, T78, T77, T74, X87, T9, X14, T7, T11, in_orderD_out_ga(T76, T78)) → PK_IN_GGGAGAGA(T77, T74, T78, X87, T9, X14, T7, T11)
PK_IN_GGGAGAGA(T77, T74, T78, T83, T9, X14, T7, T11) → U16_GGGAGAGA(T77, T74, T78, T83, T9, X14, T7, T11, appF_in_ggga(T77, T74, T78, T83))
PK_IN_GGGAGAGA(T77, T74, T78, T83, T9, X14, T7, T11) → APPF_IN_GGGA(T77, T74, T78, T83)
U16_GGGAGAGA(T77, T74, T78, T83, T9, X14, T7, T11, appF_out_ggga(T77, T74, T78, T83)) → U17_GGGAGAGA(T77, T74, T78, T83, T9, X14, T7, T11, pL_in_gagga(T9, X14, T83, T7, T11))
U16_GGGAGAGA(T77, T74, T78, T83, T9, X14, T7, T11, appF_out_ggga(T77, T74, T78, T83)) → PL_IN_GAGGA(T9, X14, T83, T7, T11)
PL_IN_GAGGA(T9, T88, T83, T7, T11) → U18_GAGGA(T9, T88, T83, T7, T11, in_orderD_in_ga(T9, T88))
PL_IN_GAGGA(T9, T88, T83, T7, T11) → IN_ORDERD_IN_GA(T9, T88)
U18_GAGGA(T9, T88, T83, T7, T11, in_orderD_out_ga(T9, T88)) → U19_GAGGA(T9, T88, T83, T7, T11, appG_in_ggga(T83, T7, T88, T11))
U18_GAGGA(T9, T88, T83, T7, T11, in_orderD_out_ga(T9, T88)) → APPG_IN_GGGA(T83, T7, T88, T11)
APPG_IN_GGGA(.(T113, T114), T115, T116, .(T113, T118)) → U5_GGGA(T113, T114, T115, T116, T118, appG_in_ggga(T114, T115, T116, T118))
APPG_IN_GGGA(.(T113, T114), T115, T116, .(T113, T118)) → APPG_IN_GGGA(T114, T115, T116, T118)

The TRS R consists of the following rules:

in_orderA_in_ga(void, []) → in_orderA_out_ga(void, [])
in_orderA_in_ga(tree(T7, void, T9), T11) → U1_ga(T7, T9, T11, pB_in_gaga(T9, X14, T7, T11))
pB_in_gaga(T9, T12, T7, T11) → U6_gaga(T9, T12, T7, T11, in_orderD_in_ga(T9, T12))
in_orderD_in_ga(void, []) → in_orderD_out_ga(void, [])
in_orderD_in_ga(tree(T19, T20, T21), X33) → U3_ga(T19, T20, T21, X33, pE_in_gagaga(T20, X31, T21, X32, T19, X33))
pE_in_gagaga(T20, T22, T21, X32, T19, X33) → U8_gagaga(T20, T22, T21, X32, T19, X33, in_orderD_in_ga(T20, T22))
U8_gagaga(T20, T22, T21, X32, T19, X33, in_orderD_out_ga(T20, T22)) → U9_gagaga(T20, T22, T21, X32, T19, X33, pI_in_gagga(T21, X32, T22, T19, X33))
pI_in_gagga(T21, T23, T22, T19, X33) → U10_gagga(T21, T23, T22, T19, X33, in_orderD_in_ga(T21, T23))
U10_gagga(T21, T23, T22, T19, X33, in_orderD_out_ga(T21, T23)) → U11_gagga(T21, T23, T22, T19, X33, appF_in_ggga(T22, T19, T23, X33))
appF_in_ggga([], T36, T37, .(T36, T37)) → appF_out_ggga([], T36, T37, .(T36, T37))
appF_in_ggga(.(T46, T47), T48, T49, .(T46, X55)) → U4_ggga(T46, T47, T48, T49, X55, appF_in_ggga(T47, T48, T49, X55))
U4_ggga(T46, T47, T48, T49, X55, appF_out_ggga(T47, T48, T49, X55)) → appF_out_ggga(.(T46, T47), T48, T49, .(T46, X55))
U11_gagga(T21, T23, T22, T19, X33, appF_out_ggga(T22, T19, T23, X33)) → pI_out_gagga(T21, T23, T22, T19, X33)
U9_gagaga(T20, T22, T21, X32, T19, X33, pI_out_gagga(T21, X32, T22, T19, X33)) → pE_out_gagaga(T20, T22, T21, X32, T19, X33)
U3_ga(T19, T20, T21, X33, pE_out_gagaga(T20, X31, T21, X32, T19, X33)) → in_orderD_out_ga(tree(T19, T20, T21), X33)
U6_gaga(T9, T12, T7, T11, in_orderD_out_ga(T9, T12)) → U7_gaga(T9, T12, T7, T11, appH_in_gga(T7, T12, T11))
appH_in_gga(T66, T67, .(T66, T67)) → appH_out_gga(T66, T67, .(T66, T67))
U7_gaga(T9, T12, T7, T11, appH_out_gga(T7, T12, T11)) → pB_out_gaga(T9, T12, T7, T11)
U1_ga(T7, T9, T11, pB_out_gaga(T9, X14, T7, T11)) → in_orderA_out_ga(tree(T7, void, T9), T11)
in_orderA_in_ga(tree(T7, tree(T74, T75, T76), T9), T11) → U2_ga(T7, T74, T75, T76, T9, T11, pC_in_gagagagaga(T75, X85, T76, X86, T74, X87, T9, X14, T7, T11))
pC_in_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11) → U12_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, in_orderD_in_ga(T75, T77))
U12_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, in_orderD_out_ga(T75, T77)) → U13_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, pJ_in_gaggagaga(T76, X86, T77, T74, X87, T9, X14, T7, T11))
pJ_in_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11) → U14_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11, in_orderD_in_ga(T76, T78))
U14_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11, in_orderD_out_ga(T76, T78)) → U15_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11, pK_in_gggagaga(T77, T74, T78, X87, T9, X14, T7, T11))
pK_in_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11) → U16_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11, appF_in_ggga(T77, T74, T78, T83))
U16_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11, appF_out_ggga(T77, T74, T78, T83)) → U17_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11, pL_in_gagga(T9, X14, T83, T7, T11))
pL_in_gagga(T9, T88, T83, T7, T11) → U18_gagga(T9, T88, T83, T7, T11, in_orderD_in_ga(T9, T88))
U18_gagga(T9, T88, T83, T7, T11, in_orderD_out_ga(T9, T88)) → U19_gagga(T9, T88, T83, T7, T11, appG_in_ggga(T83, T7, T88, T11))
appG_in_ggga([], T101, T102, .(T101, T102)) → appG_out_ggga([], T101, T102, .(T101, T102))
appG_in_ggga(.(T113, T114), T115, T116, .(T113, T118)) → U5_ggga(T113, T114, T115, T116, T118, appG_in_ggga(T114, T115, T116, T118))
U5_ggga(T113, T114, T115, T116, T118, appG_out_ggga(T114, T115, T116, T118)) → appG_out_ggga(.(T113, T114), T115, T116, .(T113, T118))
U19_gagga(T9, T88, T83, T7, T11, appG_out_ggga(T83, T7, T88, T11)) → pL_out_gagga(T9, T88, T83, T7, T11)
U17_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11, pL_out_gagga(T9, X14, T83, T7, T11)) → pK_out_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11)
U15_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11, pK_out_gggagaga(T77, T74, T78, X87, T9, X14, T7, T11)) → pJ_out_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11)
U13_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, pJ_out_gaggagaga(T76, X86, T77, T74, X87, T9, X14, T7, T11)) → pC_out_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11)
U2_ga(T7, T74, T75, T76, T9, T11, pC_out_gagagagaga(T75, X85, T76, X86, T74, X87, T9, X14, T7, T11)) → in_orderA_out_ga(tree(T7, tree(T74, T75, T76), T9), T11)

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

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

The TRS R consists of the following rules:

in_orderA_in_ga(void, []) → in_orderA_out_ga(void, [])
in_orderA_in_ga(tree(T7, void, T9), T11) → U1_ga(T7, T9, T11, pB_in_gaga(T9, X14, T7, T11))
pB_in_gaga(T9, T12, T7, T11) → U6_gaga(T9, T12, T7, T11, in_orderD_in_ga(T9, T12))
in_orderD_in_ga(void, []) → in_orderD_out_ga(void, [])
in_orderD_in_ga(tree(T19, T20, T21), X33) → U3_ga(T19, T20, T21, X33, pE_in_gagaga(T20, X31, T21, X32, T19, X33))
pE_in_gagaga(T20, T22, T21, X32, T19, X33) → U8_gagaga(T20, T22, T21, X32, T19, X33, in_orderD_in_ga(T20, T22))
U8_gagaga(T20, T22, T21, X32, T19, X33, in_orderD_out_ga(T20, T22)) → U9_gagaga(T20, T22, T21, X32, T19, X33, pI_in_gagga(T21, X32, T22, T19, X33))
pI_in_gagga(T21, T23, T22, T19, X33) → U10_gagga(T21, T23, T22, T19, X33, in_orderD_in_ga(T21, T23))
U10_gagga(T21, T23, T22, T19, X33, in_orderD_out_ga(T21, T23)) → U11_gagga(T21, T23, T22, T19, X33, appF_in_ggga(T22, T19, T23, X33))
appF_in_ggga([], T36, T37, .(T36, T37)) → appF_out_ggga([], T36, T37, .(T36, T37))
appF_in_ggga(.(T46, T47), T48, T49, .(T46, X55)) → U4_ggga(T46, T47, T48, T49, X55, appF_in_ggga(T47, T48, T49, X55))
U4_ggga(T46, T47, T48, T49, X55, appF_out_ggga(T47, T48, T49, X55)) → appF_out_ggga(.(T46, T47), T48, T49, .(T46, X55))
U11_gagga(T21, T23, T22, T19, X33, appF_out_ggga(T22, T19, T23, X33)) → pI_out_gagga(T21, T23, T22, T19, X33)
U9_gagaga(T20, T22, T21, X32, T19, X33, pI_out_gagga(T21, X32, T22, T19, X33)) → pE_out_gagaga(T20, T22, T21, X32, T19, X33)
U3_ga(T19, T20, T21, X33, pE_out_gagaga(T20, X31, T21, X32, T19, X33)) → in_orderD_out_ga(tree(T19, T20, T21), X33)
U6_gaga(T9, T12, T7, T11, in_orderD_out_ga(T9, T12)) → U7_gaga(T9, T12, T7, T11, appH_in_gga(T7, T12, T11))
appH_in_gga(T66, T67, .(T66, T67)) → appH_out_gga(T66, T67, .(T66, T67))
U7_gaga(T9, T12, T7, T11, appH_out_gga(T7, T12, T11)) → pB_out_gaga(T9, T12, T7, T11)
U1_ga(T7, T9, T11, pB_out_gaga(T9, X14, T7, T11)) → in_orderA_out_ga(tree(T7, void, T9), T11)
in_orderA_in_ga(tree(T7, tree(T74, T75, T76), T9), T11) → U2_ga(T7, T74, T75, T76, T9, T11, pC_in_gagagagaga(T75, X85, T76, X86, T74, X87, T9, X14, T7, T11))
pC_in_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11) → U12_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, in_orderD_in_ga(T75, T77))
U12_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, in_orderD_out_ga(T75, T77)) → U13_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, pJ_in_gaggagaga(T76, X86, T77, T74, X87, T9, X14, T7, T11))
pJ_in_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11) → U14_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11, in_orderD_in_ga(T76, T78))
U14_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11, in_orderD_out_ga(T76, T78)) → U15_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11, pK_in_gggagaga(T77, T74, T78, X87, T9, X14, T7, T11))
pK_in_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11) → U16_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11, appF_in_ggga(T77, T74, T78, T83))
U16_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11, appF_out_ggga(T77, T74, T78, T83)) → U17_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11, pL_in_gagga(T9, X14, T83, T7, T11))
pL_in_gagga(T9, T88, T83, T7, T11) → U18_gagga(T9, T88, T83, T7, T11, in_orderD_in_ga(T9, T88))
U18_gagga(T9, T88, T83, T7, T11, in_orderD_out_ga(T9, T88)) → U19_gagga(T9, T88, T83, T7, T11, appG_in_ggga(T83, T7, T88, T11))
appG_in_ggga([], T101, T102, .(T101, T102)) → appG_out_ggga([], T101, T102, .(T101, T102))
appG_in_ggga(.(T113, T114), T115, T116, .(T113, T118)) → U5_ggga(T113, T114, T115, T116, T118, appG_in_ggga(T114, T115, T116, T118))
U5_ggga(T113, T114, T115, T116, T118, appG_out_ggga(T114, T115, T116, T118)) → appG_out_ggga(.(T113, T114), T115, T116, .(T113, T118))
U19_gagga(T9, T88, T83, T7, T11, appG_out_ggga(T83, T7, T88, T11)) → pL_out_gagga(T9, T88, T83, T7, T11)
U17_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11, pL_out_gagga(T9, X14, T83, T7, T11)) → pK_out_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11)
U15_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11, pK_out_gggagaga(T77, T74, T78, X87, T9, X14, T7, T11)) → pJ_out_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11)
U13_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, pJ_out_gaggagaga(T76, X86, T77, T74, X87, T9, X14, T7, T11)) → pC_out_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11)
U2_ga(T7, T74, T75, T76, T9, T11, pC_out_gagagagaga(T75, X85, T76, X86, T74, X87, T9, X14, T7, T11)) → in_orderA_out_ga(tree(T7, tree(T74, T75, T76), T9), T11)

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

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

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
APPG_IN_GGGA(x1, x2, x3, x4) = APPG_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:

APPG_IN_GGGA(.(T113, T114), T115, T116) → APPG_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:

APPG_IN_GGGA(.(T113, T114), T115, T116) → APPG_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:

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

The TRS R consists of the following rules:

in_orderA_in_ga(void, []) → in_orderA_out_ga(void, [])
in_orderA_in_ga(tree(T7, void, T9), T11) → U1_ga(T7, T9, T11, pB_in_gaga(T9, X14, T7, T11))
pB_in_gaga(T9, T12, T7, T11) → U6_gaga(T9, T12, T7, T11, in_orderD_in_ga(T9, T12))
in_orderD_in_ga(void, []) → in_orderD_out_ga(void, [])
in_orderD_in_ga(tree(T19, T20, T21), X33) → U3_ga(T19, T20, T21, X33, pE_in_gagaga(T20, X31, T21, X32, T19, X33))
pE_in_gagaga(T20, T22, T21, X32, T19, X33) → U8_gagaga(T20, T22, T21, X32, T19, X33, in_orderD_in_ga(T20, T22))
U8_gagaga(T20, T22, T21, X32, T19, X33, in_orderD_out_ga(T20, T22)) → U9_gagaga(T20, T22, T21, X32, T19, X33, pI_in_gagga(T21, X32, T22, T19, X33))
pI_in_gagga(T21, T23, T22, T19, X33) → U10_gagga(T21, T23, T22, T19, X33, in_orderD_in_ga(T21, T23))
U10_gagga(T21, T23, T22, T19, X33, in_orderD_out_ga(T21, T23)) → U11_gagga(T21, T23, T22, T19, X33, appF_in_ggga(T22, T19, T23, X33))
appF_in_ggga([], T36, T37, .(T36, T37)) → appF_out_ggga([], T36, T37, .(T36, T37))
appF_in_ggga(.(T46, T47), T48, T49, .(T46, X55)) → U4_ggga(T46, T47, T48, T49, X55, appF_in_ggga(T47, T48, T49, X55))
U4_ggga(T46, T47, T48, T49, X55, appF_out_ggga(T47, T48, T49, X55)) → appF_out_ggga(.(T46, T47), T48, T49, .(T46, X55))
U11_gagga(T21, T23, T22, T19, X33, appF_out_ggga(T22, T19, T23, X33)) → pI_out_gagga(T21, T23, T22, T19, X33)
U9_gagaga(T20, T22, T21, X32, T19, X33, pI_out_gagga(T21, X32, T22, T19, X33)) → pE_out_gagaga(T20, T22, T21, X32, T19, X33)
U3_ga(T19, T20, T21, X33, pE_out_gagaga(T20, X31, T21, X32, T19, X33)) → in_orderD_out_ga(tree(T19, T20, T21), X33)
U6_gaga(T9, T12, T7, T11, in_orderD_out_ga(T9, T12)) → U7_gaga(T9, T12, T7, T11, appH_in_gga(T7, T12, T11))
appH_in_gga(T66, T67, .(T66, T67)) → appH_out_gga(T66, T67, .(T66, T67))
U7_gaga(T9, T12, T7, T11, appH_out_gga(T7, T12, T11)) → pB_out_gaga(T9, T12, T7, T11)
U1_ga(T7, T9, T11, pB_out_gaga(T9, X14, T7, T11)) → in_orderA_out_ga(tree(T7, void, T9), T11)
in_orderA_in_ga(tree(T7, tree(T74, T75, T76), T9), T11) → U2_ga(T7, T74, T75, T76, T9, T11, pC_in_gagagagaga(T75, X85, T76, X86, T74, X87, T9, X14, T7, T11))
pC_in_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11) → U12_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, in_orderD_in_ga(T75, T77))
U12_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, in_orderD_out_ga(T75, T77)) → U13_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, pJ_in_gaggagaga(T76, X86, T77, T74, X87, T9, X14, T7, T11))
pJ_in_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11) → U14_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11, in_orderD_in_ga(T76, T78))
U14_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11, in_orderD_out_ga(T76, T78)) → U15_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11, pK_in_gggagaga(T77, T74, T78, X87, T9, X14, T7, T11))
pK_in_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11) → U16_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11, appF_in_ggga(T77, T74, T78, T83))
U16_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11, appF_out_ggga(T77, T74, T78, T83)) → U17_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11, pL_in_gagga(T9, X14, T83, T7, T11))
pL_in_gagga(T9, T88, T83, T7, T11) → U18_gagga(T9, T88, T83, T7, T11, in_orderD_in_ga(T9, T88))
U18_gagga(T9, T88, T83, T7, T11, in_orderD_out_ga(T9, T88)) → U19_gagga(T9, T88, T83, T7, T11, appG_in_ggga(T83, T7, T88, T11))
appG_in_ggga([], T101, T102, .(T101, T102)) → appG_out_ggga([], T101, T102, .(T101, T102))
appG_in_ggga(.(T113, T114), T115, T116, .(T113, T118)) → U5_ggga(T113, T114, T115, T116, T118, appG_in_ggga(T114, T115, T116, T118))
U5_ggga(T113, T114, T115, T116, T118, appG_out_ggga(T114, T115, T116, T118)) → appG_out_ggga(.(T113, T114), T115, T116, .(T113, T118))
U19_gagga(T9, T88, T83, T7, T11, appG_out_ggga(T83, T7, T88, T11)) → pL_out_gagga(T9, T88, T83, T7, T11)
U17_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11, pL_out_gagga(T9, X14, T83, T7, T11)) → pK_out_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11)
U15_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11, pK_out_gggagaga(T77, T74, T78, X87, T9, X14, T7, T11)) → pJ_out_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11)
U13_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, pJ_out_gaggagaga(T76, X86, T77, T74, X87, T9, X14, T7, T11)) → pC_out_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11)
U2_ga(T7, T74, T75, T76, T9, T11, pC_out_gagagagaga(T75, X85, T76, X86, T74, X87, T9, X14, T7, T11)) → in_orderA_out_ga(tree(T7, tree(T74, T75, T76), T9), T11)

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

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

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
APPF_IN_GGGA(x1, x2, x3, x4) = APPF_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:

APPF_IN_GGGA(.(T46, T47), T48, T49) → APPF_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:

APPF_IN_GGGA(.(T46, T47), T48, T49) → APPF_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:

IN_ORDERD_IN_GA(tree(T19, T20, T21), X33) → PE_IN_GAGAGA(T20, X31, T21, X32, T19, X33)
PE_IN_GAGAGA(T20, T22, T21, X32, T19, X33) → U8_GAGAGA(T20, T22, T21, X32, T19, X33, in_orderD_in_ga(T20, T22))
U8_GAGAGA(T20, T22, T21, X32, T19, X33, in_orderD_out_ga(T20, T22)) → PI_IN_GAGGA(T21, X32, T22, T19, X33)
PI_IN_GAGGA(T21, T23, T22, T19, X33) → IN_ORDERD_IN_GA(T21, T23)
PE_IN_GAGAGA(T20, T22, T21, X32, T19, X33) → IN_ORDERD_IN_GA(T20, T22)

The TRS R consists of the following rules:

in_orderA_in_ga(void, []) → in_orderA_out_ga(void, [])
in_orderA_in_ga(tree(T7, void, T9), T11) → U1_ga(T7, T9, T11, pB_in_gaga(T9, X14, T7, T11))
pB_in_gaga(T9, T12, T7, T11) → U6_gaga(T9, T12, T7, T11, in_orderD_in_ga(T9, T12))
in_orderD_in_ga(void, []) → in_orderD_out_ga(void, [])
in_orderD_in_ga(tree(T19, T20, T21), X33) → U3_ga(T19, T20, T21, X33, pE_in_gagaga(T20, X31, T21, X32, T19, X33))
pE_in_gagaga(T20, T22, T21, X32, T19, X33) → U8_gagaga(T20, T22, T21, X32, T19, X33, in_orderD_in_ga(T20, T22))
U8_gagaga(T20, T22, T21, X32, T19, X33, in_orderD_out_ga(T20, T22)) → U9_gagaga(T20, T22, T21, X32, T19, X33, pI_in_gagga(T21, X32, T22, T19, X33))
pI_in_gagga(T21, T23, T22, T19, X33) → U10_gagga(T21, T23, T22, T19, X33, in_orderD_in_ga(T21, T23))
U10_gagga(T21, T23, T22, T19, X33, in_orderD_out_ga(T21, T23)) → U11_gagga(T21, T23, T22, T19, X33, appF_in_ggga(T22, T19, T23, X33))
appF_in_ggga([], T36, T37, .(T36, T37)) → appF_out_ggga([], T36, T37, .(T36, T37))
appF_in_ggga(.(T46, T47), T48, T49, .(T46, X55)) → U4_ggga(T46, T47, T48, T49, X55, appF_in_ggga(T47, T48, T49, X55))
U4_ggga(T46, T47, T48, T49, X55, appF_out_ggga(T47, T48, T49, X55)) → appF_out_ggga(.(T46, T47), T48, T49, .(T46, X55))
U11_gagga(T21, T23, T22, T19, X33, appF_out_ggga(T22, T19, T23, X33)) → pI_out_gagga(T21, T23, T22, T19, X33)
U9_gagaga(T20, T22, T21, X32, T19, X33, pI_out_gagga(T21, X32, T22, T19, X33)) → pE_out_gagaga(T20, T22, T21, X32, T19, X33)
U3_ga(T19, T20, T21, X33, pE_out_gagaga(T20, X31, T21, X32, T19, X33)) → in_orderD_out_ga(tree(T19, T20, T21), X33)
U6_gaga(T9, T12, T7, T11, in_orderD_out_ga(T9, T12)) → U7_gaga(T9, T12, T7, T11, appH_in_gga(T7, T12, T11))
appH_in_gga(T66, T67, .(T66, T67)) → appH_out_gga(T66, T67, .(T66, T67))
U7_gaga(T9, T12, T7, T11, appH_out_gga(T7, T12, T11)) → pB_out_gaga(T9, T12, T7, T11)
U1_ga(T7, T9, T11, pB_out_gaga(T9, X14, T7, T11)) → in_orderA_out_ga(tree(T7, void, T9), T11)
in_orderA_in_ga(tree(T7, tree(T74, T75, T76), T9), T11) → U2_ga(T7, T74, T75, T76, T9, T11, pC_in_gagagagaga(T75, X85, T76, X86, T74, X87, T9, X14, T7, T11))
pC_in_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11) → U12_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, in_orderD_in_ga(T75, T77))
U12_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, in_orderD_out_ga(T75, T77)) → U13_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, pJ_in_gaggagaga(T76, X86, T77, T74, X87, T9, X14, T7, T11))
pJ_in_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11) → U14_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11, in_orderD_in_ga(T76, T78))
U14_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11, in_orderD_out_ga(T76, T78)) → U15_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11, pK_in_gggagaga(T77, T74, T78, X87, T9, X14, T7, T11))
pK_in_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11) → U16_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11, appF_in_ggga(T77, T74, T78, T83))
U16_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11, appF_out_ggga(T77, T74, T78, T83)) → U17_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11, pL_in_gagga(T9, X14, T83, T7, T11))
pL_in_gagga(T9, T88, T83, T7, T11) → U18_gagga(T9, T88, T83, T7, T11, in_orderD_in_ga(T9, T88))
U18_gagga(T9, T88, T83, T7, T11, in_orderD_out_ga(T9, T88)) → U19_gagga(T9, T88, T83, T7, T11, appG_in_ggga(T83, T7, T88, T11))
appG_in_ggga([], T101, T102, .(T101, T102)) → appG_out_ggga([], T101, T102, .(T101, T102))
appG_in_ggga(.(T113, T114), T115, T116, .(T113, T118)) → U5_ggga(T113, T114, T115, T116, T118, appG_in_ggga(T114, T115, T116, T118))
U5_ggga(T113, T114, T115, T116, T118, appG_out_ggga(T114, T115, T116, T118)) → appG_out_ggga(.(T113, T114), T115, T116, .(T113, T118))
U19_gagga(T9, T88, T83, T7, T11, appG_out_ggga(T83, T7, T88, T11)) → pL_out_gagga(T9, T88, T83, T7, T11)
U17_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11, pL_out_gagga(T9, X14, T83, T7, T11)) → pK_out_gggagaga(T77, T74, T78, T83, T9, X14, T7, T11)
U15_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11, pK_out_gggagaga(T77, T74, T78, X87, T9, X14, T7, T11)) → pJ_out_gaggagaga(T76, T78, T77, T74, X87, T9, X14, T7, T11)
U13_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11, pJ_out_gaggagaga(T76, X86, T77, T74, X87, T9, X14, T7, T11)) → pC_out_gagagagaga(T75, T77, T76, X86, T74, X87, T9, X14, T7, T11)
U2_ga(T7, T74, T75, T76, T9, T11, pC_out_gagagagaga(T75, X85, T76, X86, T74, X87, T9, X14, T7, T11)) → in_orderA_out_ga(tree(T7, tree(T74, T75, T76), T9), T11)

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

IN_ORDERD_IN_GA(tree(T19, T20, T21), X33) → PE_IN_GAGAGA(T20, X31, T21, X32, T19, X33)
PE_IN_GAGAGA(T20, T22, T21, X32, T19, X33) → U8_GAGAGA(T20, T22, T21, X32, T19, X33, in_orderD_in_ga(T20, T22))
U8_GAGAGA(T20, T22, T21, X32, T19, X33, in_orderD_out_ga(T20, T22)) → PI_IN_GAGGA(T21, X32, T22, T19, X33)
PI_IN_GAGGA(T21, T23, T22, T19, X33) → IN_ORDERD_IN_GA(T21, T23)
PE_IN_GAGAGA(T20, T22, T21, X32, T19, X33) → IN_ORDERD_IN_GA(T20, T22)

The TRS R consists of the following rules:

in_orderD_in_ga(void, []) → in_orderD_out_ga(void, [])
in_orderD_in_ga(tree(T19, T20, T21), X33) → U3_ga(T19, T20, T21, X33, pE_in_gagaga(T20, X31, T21, X32, T19, X33))
U3_ga(T19, T20, T21, X33, pE_out_gagaga(T20, X31, T21, X32, T19, X33)) → in_orderD_out_ga(tree(T19, T20, T21), X33)
pE_in_gagaga(T20, T22, T21, X32, T19, X33) → U8_gagaga(T20, T22, T21, X32, T19, X33, in_orderD_in_ga(T20, T22))
U8_gagaga(T20, T22, T21, X32, T19, X33, in_orderD_out_ga(T20, T22)) → U9_gagaga(T20, T22, T21, X32, T19, X33, pI_in_gagga(T21, X32, T22, T19, X33))
U9_gagaga(T20, T22, T21, X32, T19, X33, pI_out_gagga(T21, X32, T22, T19, X33)) → pE_out_gagaga(T20, T22, T21, X32, T19, X33)
pI_in_gagga(T21, T23, T22, T19, X33) → U10_gagga(T21, T23, T22, T19, X33, in_orderD_in_ga(T21, T23))
U10_gagga(T21, T23, T22, T19, X33, in_orderD_out_ga(T21, T23)) → U11_gagga(T21, T23, T22, T19, X33, appF_in_ggga(T22, T19, T23, X33))
U11_gagga(T21, T23, T22, T19, X33, appF_out_ggga(T22, T19, T23, X33)) → pI_out_gagga(T21, T23, T22, T19, X33)
appF_in_ggga([], T36, T37, .(T36, T37)) → appF_out_ggga([], T36, T37, .(T36, T37))
appF_in_ggga(.(T46, T47), T48, T49, .(T46, X55)) → U4_ggga(T46, T47, T48, T49, X55, appF_in_ggga(T47, T48, T49, X55))
U4_ggga(T46, T47, T48, T49, X55, appF_out_ggga(T47, T48, T49, X55)) → appF_out_ggga(.(T46, T47), T48, T49, .(T46, X55))

The argument filtering Pi contains the following mapping:
void = void
tree(x1, x2, x3) = tree(x1, x2, x3)
in_orderD_in_ga(x1, x2) = in_orderD_in_ga(x1)
in_orderD_out_ga(x1, x2) = in_orderD_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)
appF_in_ggga(x1, x2, x3, x4) = appF_in_ggga(x1, x2, x3)
[] = []
appF_out_ggga(x1, x2, x3, x4) = appF_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)
IN_ORDERD_IN_GA(x1, x2) = IN_ORDERD_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:

IN_ORDERD_IN_GA(tree(T19, T20, T21)) → PE_IN_GAGAGA(T20, T21, T19)
PE_IN_GAGAGA(T20, T21, T19) → U8_GAGAGA(T20, T21, T19, in_orderD_in_ga(T20))
U8_GAGAGA(T20, T21, T19, in_orderD_out_ga(T20, T22)) → PI_IN_GAGGA(T21, T22, T19)
PI_IN_GAGGA(T21, T22, T19) → IN_ORDERD_IN_GA(T21)
PE_IN_GAGAGA(T20, T21, T19) → IN_ORDERD_IN_GA(T20)

The TRS R consists of the following rules:

in_orderD_in_ga(void) → in_orderD_out_ga(void, [])
in_orderD_in_ga(tree(T19, T20, T21)) → U3_ga(T19, T20, T21, pE_in_gagaga(T20, T21, T19))
U3_ga(T19, T20, T21, pE_out_gagaga(T20, X31, T21, X32, T19, X33)) → in_orderD_out_ga(tree(T19, T20, T21), X33)
pE_in_gagaga(T20, T21, T19) → U8_gagaga(T20, T21, T19, in_orderD_in_ga(T20))
U8_gagaga(T20, T21, T19, in_orderD_out_ga(T20, T22)) → U9_gagaga(T20, T22, T21, T19, pI_in_gagga(T21, T22, T19))
U9_gagaga(T20, T22, T21, T19, pI_out_gagga(T21, X32, T22, T19, X33)) → pE_out_gagaga(T20, T22, T21, X32, T19, X33)
pI_in_gagga(T21, T22, T19) → U10_gagga(T21, T22, T19, in_orderD_in_ga(T21))
U10_gagga(T21, T22, T19, in_orderD_out_ga(T21, T23)) → U11_gagga(T21, T23, T22, T19, appF_in_ggga(T22, T19, T23))
U11_gagga(T21, T23, T22, T19, appF_out_ggga(T22, T19, T23, X33)) → pI_out_gagga(T21, T23, T22, T19, X33)
appF_in_ggga([], T36, T37) → appF_out_ggga([], T36, T37, .(T36, T37))
appF_in_ggga(.(T46, T47), T48, T49) → U4_ggga(T46, T47, T48, T49, appF_in_ggga(T47, T48, T49))
U4_ggga(T46, T47, T48, T49, appF_out_ggga(T47, T48, T49, X55)) → appF_out_ggga(.(T46, T47), T48, T49, .(T46, X55))

The set Q consists of the following terms:

in_orderD_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)
appF_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(T20, T21, T19) → IN_ORDERD_IN_GA(T20)
The graph contains the following edges 1 >= 1
PE_IN_GAGAGA(T20, T21, T19) → U8_GAGAGA(T20, T21, T19, in_orderD_in_ga(T20))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3
PI_IN_GAGGA(T21, T22, T19) → IN_ORDERD_IN_GA(T21)
The graph contains the following edges 1 >= 1
U8_GAGAGA(T20, T21, T19, in_orderD_out_ga(T20, T22)) → PI_IN_GAGGA(T21, T22, T19)
The graph contains the following edges 2 >= 1, 4 > 2, 3 >= 3
IN_ORDERD_IN_GA(tree(T19, T20, T21)) → PE_IN_GAGAGA(T20, T21, T19)
The graph contains the following edges 1 > 1, 1 > 2, 1 > 3

(0) Obligation:

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) PiDPToQDPProof (SOUND transformation)

(11) Obligation:

(12) QDPSizeChangeProof (EQUIVALENT transformation)

(13) YES

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) PiDPToQDPProof (SOUND transformation)

(18) Obligation:

(19) QDPSizeChangeProof (EQUIVALENT transformation)

(20) YES

(21) Obligation:

(22) UsableRulesProof (EQUIVALENT transformation)

(23) Obligation:

(24) PiDPToQDPProof (SOUND transformation)

(25) Obligation:

(26) QDPSizeChangeProof (EQUIVALENT transformation)

(27) YES