Left Termination proof of /tmp/tmp5l

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 283 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 606 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 0 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 (⇒, 9 ms)

        ↳25 QDP

        ↳26 QDPSizeChangeProof (⇔, 0 ms)

        ↳27 YES

(0) Obligation:

Clauses:

front(void, []).
front(tree(X, void, void), .(X, [])).
front(tree(X1, L, R), Xs) :- ','(front(L, Ls), ','(front(R, Rs), app(Ls, Rs, Xs))).
app([], X, X).
app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs).

Query: front(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: front(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: front(T1, T2), SCOPE: 1, CLAUSE: 0 | front(T1, T2), SCOPE: 1, CLAUSE: 1 | front(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: true | front(void, T2), SCOPE: 1, CLAUSE: 1 | front(void, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: front(T1, T2), SCOPE: 1, CLAUSE: 1 | front(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nfront(T1, T2) !=? front(void, [])", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: front(void, T2), SCOPE: 1, CLAUSE: 1 | front(void, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: front(void, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: true | front(tree(T4, void, void), T2), SCOPE: 1, CLAUSE: 2\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: front(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nX8 is free\nfront(T1, T2) !=? front(void, [])\nfront(T1, T2) !=? front(tree(X8, void, void), .(X8, []))", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: front(tree(T4, void, void), T2), SCOPE: 1, CLAUSE: 2\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(front(void, X17), ','(front(void, X18), app(X17, X18, T9)))\n\nX17 is free\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(front(void, X17), ','(front(void, X18), app(X17, X18, T9))), SCOPE: 2, CLAUSE: 0 | ','(front(void, X17), ','(front(void, X18), app(X17, X18, T9))), SCOPE: 2, CLAUSE: 1 | ','(front(void, X17), ','(front(void, X18), app(X17, X18, T9))), SCOPE: 2, CLAUSE: 2\n\nX17 is free\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(front(void, X17), ','(front(void, X18), app(X17, X18, T9))), SCOPE: 2, CLAUSE: 0\n\nX17 is free\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(front(void, X17), ','(front(void, X18), app(X17, X18, T9))), SCOPE: 2, CLAUSE: 1 | ','(front(void, X17), ','(front(void, X18), app(X17, X18, T9))), SCOPE: 2, CLAUSE: 2\n\nX17 is free\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="B: ','(front(void, X18), app([], X18, T9))\n\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="K: front(void, X18)\n\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="F: app([], T13, T9)\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: front(void, X18), SCOPE: 3, CLAUSE: 0 | front(void, X18), SCOPE: 3, CLAUSE: 1 | front(void, X18), SCOPE: 3, CLAUSE: 2\n\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: front(void, X18), SCOPE: 3, CLAUSE: 0\n\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: front(void, X18), SCOPE: 3, CLAUSE: 1 | front(void, X18), SCOPE: 3, CLAUSE: 2\n\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: front(void, X18), SCOPE: 3, CLAUSE: 2\n\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: app([], T13, T9), SCOPE: 4, CLAUSE: 3 | app([], T13, T9), SCOPE: 4, CLAUSE: 4\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: app([], T13, T9), SCOPE: 4, CLAUSE: 3\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: app([], T13, T9), SCOPE: 4, CLAUSE: 4\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: ','(front(void, X17), ','(front(void, X18), app(X17, X18, T9))), SCOPE: 2, CLAUSE: 2\n\nX17 is free\nX18 is free", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: ','(front(T26, X54), ','(front(T27, X55), app(X54, X55, T29)))\n\nT25 is ground\nT26 is ground\nT27 is ground\nX8 is free\nX54 is free\nX55 is free\nfront(tree(T25, T26, T27), T2) !=? front(tree(X8, void, void), .(X8, []))", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(front(T26, X54), ','(front(T27, X55), app(X54, X55, T29))), SCOPE: 5, CLAUSE: 0 | ','(front(T26, X54), ','(front(T27, X55), app(X54, X55, T29))), SCOPE: 5, CLAUSE: 1 | ','(front(T26, X54), ','(front(T27, X55), app(X54, X55, T29))), SCOPE: 5, CLAUSE: 2\n\nT25 is ground\nT26 is ground\nT27 is ground\nX8 is free\nX54 is free\nX55 is free\nfront(tree(T25, T26, T27), T2) !=? front(tree(X8, void, void), .(X8, []))", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(front(T26, X54), ','(front(T27, X55), app(X54, X55, T29))), SCOPE: 5, CLAUSE: 0\n\nT25 is ground\nT26 is ground\nT27 is ground\nX8 is free\nX54 is free\nX55 is free\nfront(tree(T25, T26, T27), T2) !=? front(tree(X8, void, void), .(X8, []))", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ','(front(T26, X54), ','(front(T27, X55), app(X54, X55, T29))), SCOPE: 5, CLAUSE: 1 | ','(front(T26, X54), ','(front(T27, X55), app(X54, X55, T29))), SCOPE: 5, CLAUSE: 2\n\nT25 is ground\nT26 is ground\nT27 is ground\nX8 is free\nX54 is free\nX55 is free\nfront(tree(T25, T26, T27), T2) !=? front(tree(X8, void, void), .(X8, []))", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="C: ','(front(T27, X55), app([], X55, T29))\n\nT25 is ground\nT27 is ground\nX8 is free\nX55 is free\nfront(tree(T25, void, T27), T2) !=? front(tree(X8, void, void), .(X8, []))", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="L: front(T27, X55)\n\nT25 is ground\nT27 is ground\nX8 is free\nX55 is free\nfront(tree(T25, void, T27), T2) !=? front(tree(X8, void, void), .(X8, []))", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: app([], T30, T29)\n\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: front(T27, X55), SCOPE: 6, CLAUSE: 0 | front(T27, X55), SCOPE: 6, CLAUSE: 1 | front(T27, X55), SCOPE: 6, CLAUSE: 2\n\nT25 is ground\nT27 is ground\nX8 is free\nX55 is free\nfront(tree(T25, void, T27), T2) !=? front(tree(X8, void, void), .(X8, []))", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: front(T27, X55), SCOPE: 6, CLAUSE: 0\n\nT25 is ground\nT27 is ground\nX8 is free\nX55 is free\nfront(tree(T25, void, T27), T2) !=? front(tree(X8, void, void), .(X8, []))", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: front(T27, X55), SCOPE: 6, CLAUSE: 1 | front(T27, X55), SCOPE: 6, CLAUSE: 2\n\nT25 is ground\nT27 is ground\nX8 is free\nX55 is free\nfront(tree(T25, void, T27), T2) !=? front(tree(X8, void, void), .(X8, []))", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: front(T27, X55), SCOPE: 6, CLAUSE: 1\n\nT25 is ground\nT27 is ground\nX8 is free\nX55 is free\nfront(tree(T25, void, T27), T2) !=? front(tree(X8, void, void), .(X8, []))", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: front(T27, X55), SCOPE: 6, CLAUSE: 2\n\nT25 is ground\nT27 is ground\nX8 is free\nX55 is free\nfront(tree(T25, void, T27), T2) !=? front(tree(X8, void, void), .(X8, []))", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="H: ','(front(T43, X77), ','(front(T44, X78), app(X77, X78, X79)))\n\nT43 is ground\nT44 is ground\nX79 is free\nX77 is free\nX78 is free", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="G: front(T43, X77)\n\nT43 is ground\nX77 is free", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="N: ','(front(T44, X78), app(T45, X78, X79))\n\nT44 is ground\nT45 is ground\nX79 is free\nX78 is free", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: front(T43, X77), SCOPE: 7, CLAUSE: 0 | front(T43, X77), SCOPE: 7, CLAUSE: 1 | front(T43, X77), SCOPE: 7, CLAUSE: 2\n\nT43 is ground\nX77 is free", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: front(T43, X77), SCOPE: 7, CLAUSE: 0\n\nT43 is ground\nX77 is free", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="157: front(T43, X77), SCOPE: 7, CLAUSE: 1 | front(T43, X77), SCOPE: 7, CLAUSE: 2\n\nT43 is ground\nX77 is free", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: front(T43, X77), SCOPE: 7, CLAUSE: 1\n\nT43 is ground\nX77 is free", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: front(T43, X77), SCOPE: 7, CLAUSE: 2\n\nT43 is ground\nX77 is free", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: ','(front(T58, X101), ','(front(T59, X102), app(X101, X102, X103)))\n\nT58 is ground\nT59 is ground\nX103 is free\nX101 is free\nX102 is free", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: front(T44, X78)\n\nT44 is ground\nX78 is free", fontsize=16, style=filled, fillcolor=lightyellow];
191 [label="I: app(T45, T60, X79)\n\nT45 is ground\nT60 is ground\nX79 is free", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: app(T45, T60, X79), SCOPE: 8, CLAUSE: 3 | app(T45, T60, X79), SCOPE: 8, CLAUSE: 4\n\nT45 is ground\nT60 is ground\nX79 is free", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: app(T45, T60, X79), SCOPE: 8, CLAUSE: 3\n\nT45 is ground\nT60 is ground\nX79 is free", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: app(T45, T60, X79), SCOPE: 8, CLAUSE: 4\n\nT45 is ground\nT60 is ground\nX79 is free", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: app(T75, T76, X125)\n\nT75 is ground\nT76 is ground\nX125 is free", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: ','(front(T26, X54), ','(front(T27, X55), app(X54, X55, T29))), SCOPE: 5, CLAUSE: 1\n\nT25 is ground\nT26 is ground\nT27 is ground\nX8 is free\nX54 is free\nX55 is free\nfront(tree(T25, T26, T27), T2) !=? front(tree(X8, void, void), .(X8, []))", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: ','(front(T26, X54), ','(front(T27, X55), app(X54, X55, T29))), SCOPE: 5, CLAUSE: 2\n\nT25 is ground\nT26 is ground\nT27 is ground\nX8 is free\nX54 is free\nX55 is free\nfront(tree(T25, T26, T27), T2) !=? front(tree(X8, void, void), .(X8, []))", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="D: ','(front(T27, X55), app(.(T85, []), X55, T29))\n\nT27 is ground\nT85 is ground\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: front(T27, X55)\n\nT27 is ground\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="M: app(.(T85, []), T86, T29)\n\nT85 is ground\nT86 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
222 [label="222: app(.(T85, []), T86, T29), SCOPE: 9, CLAUSE: 3 | app(.(T85, []), T86, T29), SCOPE: 9, CLAUSE: 4\n\nT85 is ground\nT86 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: app(.(T85, []), T86, T29), SCOPE: 9, CLAUSE: 4\n\nT85 is ground\nT86 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
226 [label="226: app([], T94, T96)\n\nT94 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="227: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
230 [label="E: ','(','(front(T106, X168), ','(front(T107, X169), app(X168, X169, X170))), ','(front(T27, X55), app(X170, X55, T29)))\n\nT27 is ground\nT106 is ground\nT107 is ground\nX55 is free\nX170 is free\nX168 is free\nX169 is free", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="231: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: front(T106, X168)\n\nT106 is ground\nX168 is free", fontsize=16, style=filled, fillcolor=lightyellow];
233 [label="O: ','(','(front(T107, X169), app(T108, X169, X170)), ','(front(T27, X55), app(X170, X55, T29)))\n\nT27 is ground\nT107 is ground\nT108 is ground\nX55 is free\nX170 is free\nX169 is free", fontsize=16, style=filled, fillcolor=lightyellow];
247 [label="247: front(T107, X169)\n\nT107 is ground\nX169 is free", fontsize=16, style=filled, fillcolor=lightyellow];
248 [label="P: ','(app(T108, T109, X170), ','(front(T27, X55), app(X170, X55, T29)))\n\nT27 is ground\nT108 is ground\nT109 is ground\nX55 is free\nX170 is free", fontsize=16, style=filled, fillcolor=lightyellow];
254 [label="254: app(T108, T109, X170)\n\nT108 is ground\nT109 is ground\nX170 is free", fontsize=16, style=filled, fillcolor=lightyellow];
255 [label="Q: ','(front(T27, X55), app(T112, X55, T29))\n\nT27 is ground\nT112 is ground\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
258 [label="258: front(T27, X55)\n\nT27 is ground\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
259 [label="J: app(T112, T115, T29)\n\nT112 is ground\nT115 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
260 [label="260: app(T112, T115, T29), SCOPE: 10, CLAUSE: 3 | app(T112, T115, T29), SCOPE: 10, CLAUSE: 4\n\nT112 is ground\nT115 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
261 [label="261: app(T112, T115, T29), SCOPE: 10, CLAUSE: 3\n\nT112 is ground\nT115 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
262 [label="262: app(T112, T115, T29), SCOPE: 10, CLAUSE: 4\n\nT112 is ground\nT115 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
263 [label="263: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
264 [label="264: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
265 [label="265: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
266 [label="266: app(T132, T133, T135)\n\nT132 is ground\nT133 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
267 [label="267: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
268 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 268 [arrowhead = none ];
268 -> 4;

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

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

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

272 [label="EVAL with clause\nfront(tree(X8, void, void), .(X8, [])).\nand substitutionX8 -> T4,\nT1 -> tree(T4, void, void),\nT2 -> .(T4, [])", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 272 [arrowhead = none ];
272 -> 24;

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

274 [label="BACKTRACK\nfor clause: front(tree(X, void, void), .(X, []))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 274 [arrowhead = none ];
274 -> 18;

275 [label="BACKTRACK\nfor clause: front(tree(X1, L, R), Xs) :- ','(front(L, Ls), ','(front(R, Rs), app(Ls, Rs, Xs)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
18 -> 275 [arrowhead = none ];
275 -> 22;

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

277 [label="EVAL with clause\nfront(tree(X50, X51, X52), X53) :- ','(front(X51, X54), ','(front(X52, X55), app(X54, X55, X53))).\nand substitutionX50 -> T25,\nX51 -> T26,\nX52 -> T27,\nT1 -> tree(T25, T26, T27),\nT2 -> T29,\nX53 -> T29,\nT28 -> T29", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 277 [arrowhead = none ];
277 -> 94;

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

279 [label="ONLY EVAL with clause\nfront(tree(X13, X14, X15), X16) :- ','(front(X14, X17), ','(front(X15, X18), app(X17, X18, X16))).\nand substitutionT4 -> T7,\nX13 -> T7,\nX14 -> void,\nX15 -> void,\nT2 -> T9,\nX16 -> T9,\nT8 -> T9", fontsize=14, style = filled, fillcolor = lightblue];
26 -> 279 [arrowhead = none ];
279 -> 30;

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

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

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

283 [label="ONLY EVAL with clause\nfront(void, []).\nand substitutionX17 -> []", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 283 [arrowhead = none ];
283 -> 41;

284 [label="BACKTRACK\nfor clause: front(tree(X, void, void), .(X, []))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
38 -> 284 [arrowhead = none ];
284 -> 83;

285 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
41 -> 285 [arrowhead = none ];
285 -> 45;

286 [label="SPLIT 2\nnew knowledge:\nT13 is ground\nreplacements:X18 -> T13", fontsize=14, style = filled, fillcolor = violet];
41 -> 286 [arrowhead = none ];
286 -> 47;

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

288 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
47 -> 288 [arrowhead = none ];
288 -> 69;

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

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

291 [label="ONLY EVAL with clause\nfront(void, []).\nand substitutionX18 -> []", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 291 [arrowhead = none ];
291 -> 60;

292 [label="BACKTRACK\nfor clause: front(tree(X, void, void), .(X, []))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
55 -> 292 [arrowhead = none ];
292 -> 64;

293 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
60 -> 293 [arrowhead = none ];
293 -> 62;

294 [label="BACKTRACK\nfor clause: front(tree(X1, L, R), Xs) :- ','(front(L, Ls), ','(front(R, Rs), app(Ls, Rs, Xs)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
64 -> 294 [arrowhead = none ];
294 -> 66;

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

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

297 [label="EVAL with clause\napp([], X36, X36).\nand substitutionT13 -> T20,\nX36 -> T20,\nT9 -> T20", fontsize=14, style = filled, fillcolor = lightblue];
70 -> 297 [arrowhead = none ];
297 -> 78;

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

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

300 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
78 -> 300 [arrowhead = none ];
300 -> 80;

301 [label="BACKTRACK\nfor clause: front(tree(X1, L, R), Xs) :- ','(front(L, Ls), ','(front(R, Rs), app(Ls, Rs, Xs)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
83 -> 301 [arrowhead = none ];
301 -> 85;

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

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

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

305 [label="EVAL with clause\nfront(void, []).\nand substitutionT26 -> void,\nX54 -> []", fontsize=14, style = filled, fillcolor = lightblue];
97 -> 305 [arrowhead = none ];
305 -> 102;

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

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

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

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

310 [label="SPLIT 2\nnew knowledge:\nT27 is ground\nT30 is ground\nreplacements:X55 -> T30", fontsize=14, style = filled, fillcolor = violet];
102 -> 310 [arrowhead = none ];
310 -> 111;

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

312 [label="INSTANCE with matching:\nT13 -> T30\nT9 -> T29", fontsize=14, style = filled, fillcolor = lightgrey];
111 -> 312 [arrowhead = none , style=dashed];
312 -> 47[style=dashed];

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

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

315 [label="EVAL with clause\nfront(void, []).\nand substitutionT27 -> void,\nX55 -> []", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 315 [arrowhead = none ];
315 -> 118;

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

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

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

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

320 [label="EVAL with clause\nfront(tree(X60, void, void), .(X60, [])).\nand substitutionX60 -> T35,\nT27 -> tree(T35, void, void),\nX55 -> .(T35, [])", fontsize=14, style = filled, fillcolor = lightblue];
124 -> 320 [arrowhead = none ];
320 -> 129;

321 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
124 -> 321 [arrowhead = none ];
321 -> 130;

322 [label="EVAL with clause\nfront(tree(X73, X74, X75), X76) :- ','(front(X74, X77), ','(front(X75, X78), app(X77, X78, X76))).\nand substitutionX73 -> T42,\nX74 -> T43,\nX75 -> T44,\nT27 -> tree(T42, T43, T44),\nX55 -> X79,\nX76 -> X79", fontsize=14, style = filled, fillcolor = lightblue];
125 -> 322 [arrowhead = none ];
322 -> 138;

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

324 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
129 -> 324 [arrowhead = none ];
324 -> 131;

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

326 [label="SPLIT 2\nnew knowledge:\nT43 is ground\nT45 is ground\nreplacements:X77 -> T45", fontsize=14, style = filled, fillcolor = violet];
138 -> 326 [arrowhead = none ];
326 -> 153;

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

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

329 [label="SPLIT 2\nnew knowledge:\nT44 is ground\nT60 is ground\nreplacements:X78 -> T60", fontsize=14, style = filled, fillcolor = violet];
153 -> 329 [arrowhead = none ];
329 -> 191;

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

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

332 [label="EVAL with clause\nfront(void, []).\nand substitutionT43 -> void,\nX77 -> []", fontsize=14, style = filled, fillcolor = lightblue];
156 -> 332 [arrowhead = none ];
332 -> 160;

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

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

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

336 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
160 -> 336 [arrowhead = none ];
336 -> 162;

337 [label="EVAL with clause\nfront(tree(X84, void, void), .(X84, [])).\nand substitutionX84 -> T50,\nT43 -> tree(T50, void, void),\nX77 -> .(T50, [])", fontsize=14, style = filled, fillcolor = lightblue];
163 -> 337 [arrowhead = none ];
337 -> 167;

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

339 [label="EVAL with clause\nfront(tree(X97, X98, X99), X100) :- ','(front(X98, X101), ','(front(X99, X102), app(X101, X102, X100))).\nand substitutionX97 -> T57,\nX98 -> T58,\nX99 -> T59,\nT43 -> tree(T57, T58, T59),\nX77 -> X103,\nX100 -> X103", fontsize=14, style = filled, fillcolor = lightblue];
164 -> 339 [arrowhead = none ];
339 -> 180;

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

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

342 [label="INSTANCE with matching:\nT43 -> T58\nX77 -> X101\nT44 -> T59\nX78 -> X102\nX79 -> X103", fontsize=14, style = filled, fillcolor = lightgrey];
180 -> 342 [arrowhead = none , style=dashed];
342 -> 138[style=dashed];

343 [label="INSTANCE with matching:\nT43 -> T44\nX77 -> X78", fontsize=14, style = filled, fillcolor = lightgrey];
189 -> 343 [arrowhead = none , style=dashed];
343 -> 152[style=dashed];

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

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

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

347 [label="EVAL with clause\napp([], X110, X110).\nand substitutionT45 -> [],\nT60 -> T67,\nX110 -> T67,\nX79 -> T67", fontsize=14, style = filled, fillcolor = lightblue];
195 -> 347 [arrowhead = none ];
347 -> 199;

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

349 [label="EVAL with clause\napp(.(X121, X122), X123, .(X121, X124)) :- app(X122, X123, X124).\nand substitutionX121 -> T74,\nX122 -> T75,\nT45 -> .(T74, T75),\nT60 -> T76,\nX123 -> T76,\nX124 -> X125,\nX79 -> .(T74, X125)", fontsize=14, style = filled, fillcolor = lightblue];
196 -> 349 [arrowhead = none ];
349 -> 205;

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

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

352 [label="INSTANCE with matching:\nT45 -> T75\nT60 -> T76\nX79 -> X125", fontsize=14, style = filled, fillcolor = lightgrey];
205 -> 352 [arrowhead = none , style=dashed];
352 -> 191[style=dashed];

353 [label="EVAL with clause\nfront(tree(X134, void, void), .(X134, [])).\nand substitutionX134 -> T85,\nT26 -> tree(T85, void, void),\nX54 -> .(T85, [])", fontsize=14, style = filled, fillcolor = lightblue];
212 -> 353 [arrowhead = none ];
353 -> 214;

354 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
212 -> 354 [arrowhead = none ];
354 -> 215;

355 [label="EVAL with clause\nfront(tree(X164, X165, X166), X167) :- ','(front(X165, X168), ','(front(X166, X169), app(X168, X169, X167))).\nand substitutionX164 -> T105,\nX165 -> T106,\nX166 -> T107,\nT26 -> tree(T105, T106, T107),\nX54 -> X170,\nX167 -> X170", fontsize=14, style = filled, fillcolor = lightblue];
213 -> 355 [arrowhead = none ];
355 -> 230;

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

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

358 [label="SPLIT 2\nnew knowledge:\nT27 is ground\nT86 is ground\nreplacements:X55 -> T86", fontsize=14, style = filled, fillcolor = violet];
214 -> 358 [arrowhead = none ];
358 -> 219;

359 [label="INSTANCE with matching:\nT43 -> T27\nX77 -> X55", fontsize=14, style = filled, fillcolor = lightgrey];
218 -> 359 [arrowhead = none , style=dashed];
359 -> 152[style=dashed];

360 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
219 -> 360 [arrowhead = none ];
360 -> 222;

361 [label="BACKTRACK\nfor clause: app([], X, X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
222 -> 361 [arrowhead = none ];
361 -> 223;

362 [label="EVAL with clause\napp(.(X146, X147), X148, .(X146, X149)) :- app(X147, X148, X149).\nand substitutionT85 -> T93,\nX146 -> T93,\nX147 -> [],\nT86 -> T94,\nX148 -> T94,\nX149 -> T96,\nT29 -> .(T93, T96),\nT95 -> T96", fontsize=14, style = filled, fillcolor = lightblue];
223 -> 362 [arrowhead = none ];
362 -> 226;

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

364 [label="INSTANCE with matching:\nT13 -> T94\nT9 -> T96", fontsize=14, style = filled, fillcolor = lightgrey];
226 -> 364 [arrowhead = none , style=dashed];
364 -> 47[style=dashed];

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

366 [label="SPLIT 2\nnew knowledge:\nT106 is ground\nT108 is ground\nreplacements:X168 -> T108", fontsize=14, style = filled, fillcolor = violet];
230 -> 366 [arrowhead = none ];
366 -> 233;

367 [label="INSTANCE with matching:\nT43 -> T106\nX77 -> X168", fontsize=14, style = filled, fillcolor = lightgrey];
232 -> 367 [arrowhead = none , style=dashed];
367 -> 152[style=dashed];

368 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
233 -> 368 [arrowhead = none ];
368 -> 247;

369 [label="SPLIT 2\nnew knowledge:\nT107 is ground\nT109 is ground\nreplacements:X169 -> T109", fontsize=14, style = filled, fillcolor = violet];
233 -> 369 [arrowhead = none ];
369 -> 248;

370 [label="INSTANCE with matching:\nT43 -> T107\nX77 -> X169", fontsize=14, style = filled, fillcolor = lightgrey];
247 -> 370 [arrowhead = none , style=dashed];
370 -> 152[style=dashed];

371 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
248 -> 371 [arrowhead = none ];
371 -> 254;

372 [label="SPLIT 2\nnew knowledge:\nT108 is ground\nT109 is ground\nT112 is ground\nreplacements:X170 -> T112", fontsize=14, style = filled, fillcolor = violet];
248 -> 372 [arrowhead = none ];
372 -> 255;

373 [label="INSTANCE with matching:\nT45 -> T108\nT60 -> T109\nX79 -> X170", fontsize=14, style = filled, fillcolor = lightgrey];
254 -> 373 [arrowhead = none , style=dashed];
373 -> 191[style=dashed];

374 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
255 -> 374 [arrowhead = none ];
374 -> 258;

375 [label="SPLIT 2\nnew knowledge:\nT27 is ground\nT115 is ground\nreplacements:X55 -> T115", fontsize=14, style = filled, fillcolor = violet];
255 -> 375 [arrowhead = none ];
375 -> 259;

376 [label="INSTANCE with matching:\nT43 -> T27\nX77 -> X55", fontsize=14, style = filled, fillcolor = lightgrey];
258 -> 376 [arrowhead = none , style=dashed];
376 -> 152[style=dashed];

377 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
259 -> 377 [arrowhead = none ];
377 -> 260;

378 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
260 -> 378 [arrowhead = none ];
378 -> 261;

379 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
260 -> 379 [arrowhead = none ];
379 -> 262;

380 [label="EVAL with clause\napp([], X181, X181).\nand substitutionT112 -> [],\nT115 -> T122,\nX181 -> T122,\nT29 -> T122", fontsize=14, style = filled, fillcolor = lightblue];
261 -> 380 [arrowhead = none ];
380 -> 263;

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

382 [label="EVAL with clause\napp(.(X190, X191), X192, .(X190, X193)) :- app(X191, X192, X193).\nand substitutionX190 -> T131,\nX191 -> T132,\nT112 -> .(T131, T132),\nT115 -> T133,\nX192 -> T133,\nX193 -> T135,\nT29 -> .(T131, T135),\nT134 -> T135", fontsize=14, style = filled, fillcolor = lightblue];
262 -> 382 [arrowhead = none ];
382 -> 266;

383 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
262 -> 383 [arrowhead = none ];
383 -> 267;

384 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
263 -> 384 [arrowhead = none ];
384 -> 265;

385 [label="INSTANCE with matching:\nT112 -> T132\nT115 -> T133\nT29 -> T135", fontsize=14, style = filled, fillcolor = lightgrey];
266 -> 385 [arrowhead = none , style=dashed];
385 -> 259[style=dashed];

}

(2) Obligation:

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

frontA_in_ga(void, []) → frontA_out_ga(void, [])
frontA_in_ga(tree(T4, void, void), .(T4, [])) → frontA_out_ga(tree(T4, void, void), .(T4, []))
frontA_in_ga(tree(T7, void, void), T9) → U1_ga(T7, T9, pB_in_aa(X18, T9))
pB_in_aa(T13, T9) → U10_aa(T13, T9, frontK_in_a(T13))
frontK_in_a([]) → frontK_out_a([])
U10_aa(T13, T9, frontK_out_a(T13)) → U11_aa(T13, T9, appF_in_ga(T13, T9))
appF_in_ga(T20, T20) → appF_out_ga(T20, T20)
U11_aa(T13, T9, appF_out_ga(T13, T9)) → pB_out_aa(T13, T9)
U1_ga(T7, T9, pB_out_aa(X18, T9)) → frontA_out_ga(tree(T7, void, void), T9)
frontA_in_ga(tree(T25, void, T27), T29) → U2_ga(T25, T27, T29, pC_in_gaa(T27, X55, T29))
pC_in_gaa(T27, T30, T29) → U12_gaa(T27, T30, T29, frontL_in_ga(T27, T30))
frontL_in_ga(void, []) → frontL_out_ga(void, [])
frontL_in_ga(tree(T35, void, void), .(T35, [])) → frontL_out_ga(tree(T35, void, void), .(T35, []))
frontL_in_ga(tree(T42, T43, T44), X79) → U8_ga(T42, T43, T44, X79, pH_in_gagaa(T43, X77, T44, X78, X79))
pH_in_gagaa(T43, T45, T44, X78, X79) → U14_gagaa(T43, T45, T44, X78, X79, frontG_in_ga(T43, T45))
frontG_in_ga(void, []) → frontG_out_ga(void, [])
frontG_in_ga(tree(T50, void, void), .(T50, [])) → frontG_out_ga(tree(T50, void, void), .(T50, []))
frontG_in_ga(tree(T57, T58, T59), X103) → U5_ga(T57, T58, T59, X103, pH_in_gagaa(T58, X101, T59, X102, X103))
U5_ga(T57, T58, T59, X103, pH_out_gagaa(T58, X101, T59, X102, X103)) → frontG_out_ga(tree(T57, T58, T59), X103)
U14_gagaa(T43, T45, T44, X78, X79, frontG_out_ga(T43, T45)) → U15_gagaa(T43, T45, T44, X78, X79, pN_in_gaga(T44, X78, T45, X79))
pN_in_gaga(T44, T60, T45, X79) → U16_gaga(T44, T60, T45, X79, frontG_in_ga(T44, T60))
U16_gaga(T44, T60, T45, X79, frontG_out_ga(T44, T60)) → U17_gaga(T44, T60, T45, X79, appI_in_gga(T45, T60, X79))
appI_in_gga([], T67, T67) → appI_out_gga([], T67, T67)
appI_in_gga(.(T74, T75), T76, .(T74, X125)) → U6_gga(T74, T75, T76, X125, appI_in_gga(T75, T76, X125))
U6_gga(T74, T75, T76, X125, appI_out_gga(T75, T76, X125)) → appI_out_gga(.(T74, T75), T76, .(T74, X125))
U17_gaga(T44, T60, T45, X79, appI_out_gga(T45, T60, X79)) → pN_out_gaga(T44, T60, T45, X79)
U15_gagaa(T43, T45, T44, X78, X79, pN_out_gaga(T44, X78, T45, X79)) → pH_out_gagaa(T43, T45, T44, X78, X79)
U8_ga(T42, T43, T44, X79, pH_out_gagaa(T43, X77, T44, X78, X79)) → frontL_out_ga(tree(T42, T43, T44), X79)
U12_gaa(T27, T30, T29, frontL_out_ga(T27, T30)) → U13_gaa(T27, T30, T29, appF_in_ga(T30, T29))
U13_gaa(T27, T30, T29, appF_out_ga(T30, T29)) → pC_out_gaa(T27, T30, T29)
U2_ga(T25, T27, T29, pC_out_gaa(T27, X55, T29)) → frontA_out_ga(tree(T25, void, T27), T29)
frontA_in_ga(tree(T25, tree(T85, void, void), T27), T29) → U3_ga(T25, T85, T27, T29, pD_in_gaga(T27, X55, T85, T29))
pD_in_gaga(T27, T86, T85, T29) → U18_gaga(T27, T86, T85, T29, frontG_in_ga(T27, T86))
U18_gaga(T27, T86, T85, T29, frontG_out_ga(T27, T86)) → U19_gaga(T27, T86, T85, T29, appM_in_gga(T85, T86, T29))
appM_in_gga(T93, T94, .(T93, T96)) → U9_gga(T93, T94, T96, appF_in_ga(T94, T96))
U9_gga(T93, T94, T96, appF_out_ga(T94, T96)) → appM_out_gga(T93, T94, .(T93, T96))
U19_gaga(T27, T86, T85, T29, appM_out_gga(T85, T86, T29)) → pD_out_gaga(T27, T86, T85, T29)
U3_ga(T25, T85, T27, T29, pD_out_gaga(T27, X55, T85, T29)) → frontA_out_ga(tree(T25, tree(T85, void, void), T27), T29)
frontA_in_ga(tree(T25, tree(T105, T106, T107), T27), T29) → U4_ga(T25, T105, T106, T107, T27, T29, pE_in_gagaagaa(T106, X168, T107, X169, X170, T27, X55, T29))
pE_in_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29) → U20_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29, frontG_in_ga(T106, T108))
U20_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29, frontG_out_ga(T106, T108)) → U21_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29, pO_in_gagagaa(T107, X169, T108, X170, T27, X55, T29))
pO_in_gagagaa(T107, T109, T108, X170, T27, X55, T29) → U22_gagagaa(T107, T109, T108, X170, T27, X55, T29, frontG_in_ga(T107, T109))
U22_gagagaa(T107, T109, T108, X170, T27, X55, T29, frontG_out_ga(T107, T109)) → U23_gagagaa(T107, T109, T108, X170, T27, X55, T29, pP_in_ggagaa(T108, T109, X170, T27, X55, T29))
pP_in_ggagaa(T108, T109, T112, T27, X55, T29) → U24_ggagaa(T108, T109, T112, T27, X55, T29, appI_in_gga(T108, T109, T112))
U24_ggagaa(T108, T109, T112, T27, X55, T29, appI_out_gga(T108, T109, T112)) → U25_ggagaa(T108, T109, T112, T27, X55, T29, pQ_in_gaga(T27, X55, T112, T29))
pQ_in_gaga(T27, T115, T112, T29) → U26_gaga(T27, T115, T112, T29, frontG_in_ga(T27, T115))
U26_gaga(T27, T115, T112, T29, frontG_out_ga(T27, T115)) → U27_gaga(T27, T115, T112, T29, appJ_in_gga(T112, T115, T29))
appJ_in_gga([], T122, T122) → appJ_out_gga([], T122, T122)
appJ_in_gga(.(T131, T132), T133, .(T131, T135)) → U7_gga(T131, T132, T133, T135, appJ_in_gga(T132, T133, T135))
U7_gga(T131, T132, T133, T135, appJ_out_gga(T132, T133, T135)) → appJ_out_gga(.(T131, T132), T133, .(T131, T135))
U27_gaga(T27, T115, T112, T29, appJ_out_gga(T112, T115, T29)) → pQ_out_gaga(T27, T115, T112, T29)
U25_ggagaa(T108, T109, T112, T27, X55, T29, pQ_out_gaga(T27, X55, T112, T29)) → pP_out_ggagaa(T108, T109, T112, T27, X55, T29)
U23_gagagaa(T107, T109, T108, X170, T27, X55, T29, pP_out_ggagaa(T108, T109, X170, T27, X55, T29)) → pO_out_gagagaa(T107, T109, T108, X170, T27, X55, T29)
U21_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29, pO_out_gagagaa(T107, X169, T108, X170, T27, X55, T29)) → pE_out_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29)
U4_ga(T25, T105, T106, T107, T27, T29, pE_out_gagaagaa(T106, X168, T107, X169, X170, T27, X55, T29)) → frontA_out_ga(tree(T25, tree(T105, T106, T107), T27), T29)

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

FRONTA_IN_GA(tree(T7, void, void), T9) → U1_GA(T7, T9, pB_in_aa(X18, T9))
FRONTA_IN_GA(tree(T7, void, void), T9) → PB_IN_AA(X18, T9)
PB_IN_AA(T13, T9) → U10_AA(T13, T9, frontK_in_a(T13))
PB_IN_AA(T13, T9) → FRONTK_IN_A(T13)
U10_AA(T13, T9, frontK_out_a(T13)) → U11_AA(T13, T9, appF_in_ga(T13, T9))
U10_AA(T13, T9, frontK_out_a(T13)) → APPF_IN_GA(T13, T9)
FRONTA_IN_GA(tree(T25, void, T27), T29) → U2_GA(T25, T27, T29, pC_in_gaa(T27, X55, T29))
FRONTA_IN_GA(tree(T25, void, T27), T29) → PC_IN_GAA(T27, X55, T29)
PC_IN_GAA(T27, T30, T29) → U12_GAA(T27, T30, T29, frontL_in_ga(T27, T30))
PC_IN_GAA(T27, T30, T29) → FRONTL_IN_GA(T27, T30)
FRONTL_IN_GA(tree(T42, T43, T44), X79) → U8_GA(T42, T43, T44, X79, pH_in_gagaa(T43, X77, T44, X78, X79))
FRONTL_IN_GA(tree(T42, T43, T44), X79) → PH_IN_GAGAA(T43, X77, T44, X78, X79)
PH_IN_GAGAA(T43, T45, T44, X78, X79) → U14_GAGAA(T43, T45, T44, X78, X79, frontG_in_ga(T43, T45))
PH_IN_GAGAA(T43, T45, T44, X78, X79) → FRONTG_IN_GA(T43, T45)
FRONTG_IN_GA(tree(T57, T58, T59), X103) → U5_GA(T57, T58, T59, X103, pH_in_gagaa(T58, X101, T59, X102, X103))
FRONTG_IN_GA(tree(T57, T58, T59), X103) → PH_IN_GAGAA(T58, X101, T59, X102, X103)
U14_GAGAA(T43, T45, T44, X78, X79, frontG_out_ga(T43, T45)) → U15_GAGAA(T43, T45, T44, X78, X79, pN_in_gaga(T44, X78, T45, X79))
U14_GAGAA(T43, T45, T44, X78, X79, frontG_out_ga(T43, T45)) → PN_IN_GAGA(T44, X78, T45, X79)
PN_IN_GAGA(T44, T60, T45, X79) → U16_GAGA(T44, T60, T45, X79, frontG_in_ga(T44, T60))
PN_IN_GAGA(T44, T60, T45, X79) → FRONTG_IN_GA(T44, T60)
U16_GAGA(T44, T60, T45, X79, frontG_out_ga(T44, T60)) → U17_GAGA(T44, T60, T45, X79, appI_in_gga(T45, T60, X79))
U16_GAGA(T44, T60, T45, X79, frontG_out_ga(T44, T60)) → APPI_IN_GGA(T45, T60, X79)
APPI_IN_GGA(.(T74, T75), T76, .(T74, X125)) → U6_GGA(T74, T75, T76, X125, appI_in_gga(T75, T76, X125))
APPI_IN_GGA(.(T74, T75), T76, .(T74, X125)) → APPI_IN_GGA(T75, T76, X125)
U12_GAA(T27, T30, T29, frontL_out_ga(T27, T30)) → U13_GAA(T27, T30, T29, appF_in_ga(T30, T29))
U12_GAA(T27, T30, T29, frontL_out_ga(T27, T30)) → APPF_IN_GA(T30, T29)
FRONTA_IN_GA(tree(T25, tree(T85, void, void), T27), T29) → U3_GA(T25, T85, T27, T29, pD_in_gaga(T27, X55, T85, T29))
FRONTA_IN_GA(tree(T25, tree(T85, void, void), T27), T29) → PD_IN_GAGA(T27, X55, T85, T29)
PD_IN_GAGA(T27, T86, T85, T29) → U18_GAGA(T27, T86, T85, T29, frontG_in_ga(T27, T86))
PD_IN_GAGA(T27, T86, T85, T29) → FRONTG_IN_GA(T27, T86)
U18_GAGA(T27, T86, T85, T29, frontG_out_ga(T27, T86)) → U19_GAGA(T27, T86, T85, T29, appM_in_gga(T85, T86, T29))
U18_GAGA(T27, T86, T85, T29, frontG_out_ga(T27, T86)) → APPM_IN_GGA(T85, T86, T29)
APPM_IN_GGA(T93, T94, .(T93, T96)) → U9_GGA(T93, T94, T96, appF_in_ga(T94, T96))
APPM_IN_GGA(T93, T94, .(T93, T96)) → APPF_IN_GA(T94, T96)
FRONTA_IN_GA(tree(T25, tree(T105, T106, T107), T27), T29) → U4_GA(T25, T105, T106, T107, T27, T29, pE_in_gagaagaa(T106, X168, T107, X169, X170, T27, X55, T29))
FRONTA_IN_GA(tree(T25, tree(T105, T106, T107), T27), T29) → PE_IN_GAGAAGAA(T106, X168, T107, X169, X170, T27, X55, T29)
PE_IN_GAGAAGAA(T106, T108, T107, X169, X170, T27, X55, T29) → U20_GAGAAGAA(T106, T108, T107, X169, X170, T27, X55, T29, frontG_in_ga(T106, T108))
PE_IN_GAGAAGAA(T106, T108, T107, X169, X170, T27, X55, T29) → FRONTG_IN_GA(T106, T108)
U20_GAGAAGAA(T106, T108, T107, X169, X170, T27, X55, T29, frontG_out_ga(T106, T108)) → U21_GAGAAGAA(T106, T108, T107, X169, X170, T27, X55, T29, pO_in_gagagaa(T107, X169, T108, X170, T27, X55, T29))
U20_GAGAAGAA(T106, T108, T107, X169, X170, T27, X55, T29, frontG_out_ga(T106, T108)) → PO_IN_GAGAGAA(T107, X169, T108, X170, T27, X55, T29)
PO_IN_GAGAGAA(T107, T109, T108, X170, T27, X55, T29) → U22_GAGAGAA(T107, T109, T108, X170, T27, X55, T29, frontG_in_ga(T107, T109))
PO_IN_GAGAGAA(T107, T109, T108, X170, T27, X55, T29) → FRONTG_IN_GA(T107, T109)
U22_GAGAGAA(T107, T109, T108, X170, T27, X55, T29, frontG_out_ga(T107, T109)) → U23_GAGAGAA(T107, T109, T108, X170, T27, X55, T29, pP_in_ggagaa(T108, T109, X170, T27, X55, T29))
U22_GAGAGAA(T107, T109, T108, X170, T27, X55, T29, frontG_out_ga(T107, T109)) → PP_IN_GGAGAA(T108, T109, X170, T27, X55, T29)
PP_IN_GGAGAA(T108, T109, T112, T27, X55, T29) → U24_GGAGAA(T108, T109, T112, T27, X55, T29, appI_in_gga(T108, T109, T112))
PP_IN_GGAGAA(T108, T109, T112, T27, X55, T29) → APPI_IN_GGA(T108, T109, T112)
U24_GGAGAA(T108, T109, T112, T27, X55, T29, appI_out_gga(T108, T109, T112)) → U25_GGAGAA(T108, T109, T112, T27, X55, T29, pQ_in_gaga(T27, X55, T112, T29))
U24_GGAGAA(T108, T109, T112, T27, X55, T29, appI_out_gga(T108, T109, T112)) → PQ_IN_GAGA(T27, X55, T112, T29)
PQ_IN_GAGA(T27, T115, T112, T29) → U26_GAGA(T27, T115, T112, T29, frontG_in_ga(T27, T115))
PQ_IN_GAGA(T27, T115, T112, T29) → FRONTG_IN_GA(T27, T115)
U26_GAGA(T27, T115, T112, T29, frontG_out_ga(T27, T115)) → U27_GAGA(T27, T115, T112, T29, appJ_in_gga(T112, T115, T29))
U26_GAGA(T27, T115, T112, T29, frontG_out_ga(T27, T115)) → APPJ_IN_GGA(T112, T115, T29)
APPJ_IN_GGA(.(T131, T132), T133, .(T131, T135)) → U7_GGA(T131, T132, T133, T135, appJ_in_gga(T132, T133, T135))
APPJ_IN_GGA(.(T131, T132), T133, .(T131, T135)) → APPJ_IN_GGA(T132, T133, T135)

The TRS R consists of the following rules:

frontA_in_ga(void, []) → frontA_out_ga(void, [])
frontA_in_ga(tree(T4, void, void), .(T4, [])) → frontA_out_ga(tree(T4, void, void), .(T4, []))
frontA_in_ga(tree(T7, void, void), T9) → U1_ga(T7, T9, pB_in_aa(X18, T9))
pB_in_aa(T13, T9) → U10_aa(T13, T9, frontK_in_a(T13))
frontK_in_a([]) → frontK_out_a([])
U10_aa(T13, T9, frontK_out_a(T13)) → U11_aa(T13, T9, appF_in_ga(T13, T9))
appF_in_ga(T20, T20) → appF_out_ga(T20, T20)
U11_aa(T13, T9, appF_out_ga(T13, T9)) → pB_out_aa(T13, T9)
U1_ga(T7, T9, pB_out_aa(X18, T9)) → frontA_out_ga(tree(T7, void, void), T9)
frontA_in_ga(tree(T25, void, T27), T29) → U2_ga(T25, T27, T29, pC_in_gaa(T27, X55, T29))
pC_in_gaa(T27, T30, T29) → U12_gaa(T27, T30, T29, frontL_in_ga(T27, T30))
frontL_in_ga(void, []) → frontL_out_ga(void, [])
frontL_in_ga(tree(T35, void, void), .(T35, [])) → frontL_out_ga(tree(T35, void, void), .(T35, []))
frontL_in_ga(tree(T42, T43, T44), X79) → U8_ga(T42, T43, T44, X79, pH_in_gagaa(T43, X77, T44, X78, X79))
pH_in_gagaa(T43, T45, T44, X78, X79) → U14_gagaa(T43, T45, T44, X78, X79, frontG_in_ga(T43, T45))
frontG_in_ga(void, []) → frontG_out_ga(void, [])
frontG_in_ga(tree(T50, void, void), .(T50, [])) → frontG_out_ga(tree(T50, void, void), .(T50, []))
frontG_in_ga(tree(T57, T58, T59), X103) → U5_ga(T57, T58, T59, X103, pH_in_gagaa(T58, X101, T59, X102, X103))
U5_ga(T57, T58, T59, X103, pH_out_gagaa(T58, X101, T59, X102, X103)) → frontG_out_ga(tree(T57, T58, T59), X103)
U14_gagaa(T43, T45, T44, X78, X79, frontG_out_ga(T43, T45)) → U15_gagaa(T43, T45, T44, X78, X79, pN_in_gaga(T44, X78, T45, X79))
pN_in_gaga(T44, T60, T45, X79) → U16_gaga(T44, T60, T45, X79, frontG_in_ga(T44, T60))
U16_gaga(T44, T60, T45, X79, frontG_out_ga(T44, T60)) → U17_gaga(T44, T60, T45, X79, appI_in_gga(T45, T60, X79))
appI_in_gga([], T67, T67) → appI_out_gga([], T67, T67)
appI_in_gga(.(T74, T75), T76, .(T74, X125)) → U6_gga(T74, T75, T76, X125, appI_in_gga(T75, T76, X125))
U6_gga(T74, T75, T76, X125, appI_out_gga(T75, T76, X125)) → appI_out_gga(.(T74, T75), T76, .(T74, X125))
U17_gaga(T44, T60, T45, X79, appI_out_gga(T45, T60, X79)) → pN_out_gaga(T44, T60, T45, X79)
U15_gagaa(T43, T45, T44, X78, X79, pN_out_gaga(T44, X78, T45, X79)) → pH_out_gagaa(T43, T45, T44, X78, X79)
U8_ga(T42, T43, T44, X79, pH_out_gagaa(T43, X77, T44, X78, X79)) → frontL_out_ga(tree(T42, T43, T44), X79)
U12_gaa(T27, T30, T29, frontL_out_ga(T27, T30)) → U13_gaa(T27, T30, T29, appF_in_ga(T30, T29))
U13_gaa(T27, T30, T29, appF_out_ga(T30, T29)) → pC_out_gaa(T27, T30, T29)
U2_ga(T25, T27, T29, pC_out_gaa(T27, X55, T29)) → frontA_out_ga(tree(T25, void, T27), T29)
frontA_in_ga(tree(T25, tree(T85, void, void), T27), T29) → U3_ga(T25, T85, T27, T29, pD_in_gaga(T27, X55, T85, T29))
pD_in_gaga(T27, T86, T85, T29) → U18_gaga(T27, T86, T85, T29, frontG_in_ga(T27, T86))
U18_gaga(T27, T86, T85, T29, frontG_out_ga(T27, T86)) → U19_gaga(T27, T86, T85, T29, appM_in_gga(T85, T86, T29))
appM_in_gga(T93, T94, .(T93, T96)) → U9_gga(T93, T94, T96, appF_in_ga(T94, T96))
U9_gga(T93, T94, T96, appF_out_ga(T94, T96)) → appM_out_gga(T93, T94, .(T93, T96))
U19_gaga(T27, T86, T85, T29, appM_out_gga(T85, T86, T29)) → pD_out_gaga(T27, T86, T85, T29)
U3_ga(T25, T85, T27, T29, pD_out_gaga(T27, X55, T85, T29)) → frontA_out_ga(tree(T25, tree(T85, void, void), T27), T29)
frontA_in_ga(tree(T25, tree(T105, T106, T107), T27), T29) → U4_ga(T25, T105, T106, T107, T27, T29, pE_in_gagaagaa(T106, X168, T107, X169, X170, T27, X55, T29))
pE_in_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29) → U20_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29, frontG_in_ga(T106, T108))
U20_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29, frontG_out_ga(T106, T108)) → U21_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29, pO_in_gagagaa(T107, X169, T108, X170, T27, X55, T29))
pO_in_gagagaa(T107, T109, T108, X170, T27, X55, T29) → U22_gagagaa(T107, T109, T108, X170, T27, X55, T29, frontG_in_ga(T107, T109))
U22_gagagaa(T107, T109, T108, X170, T27, X55, T29, frontG_out_ga(T107, T109)) → U23_gagagaa(T107, T109, T108, X170, T27, X55, T29, pP_in_ggagaa(T108, T109, X170, T27, X55, T29))
pP_in_ggagaa(T108, T109, T112, T27, X55, T29) → U24_ggagaa(T108, T109, T112, T27, X55, T29, appI_in_gga(T108, T109, T112))
U24_ggagaa(T108, T109, T112, T27, X55, T29, appI_out_gga(T108, T109, T112)) → U25_ggagaa(T108, T109, T112, T27, X55, T29, pQ_in_gaga(T27, X55, T112, T29))
pQ_in_gaga(T27, T115, T112, T29) → U26_gaga(T27, T115, T112, T29, frontG_in_ga(T27, T115))
U26_gaga(T27, T115, T112, T29, frontG_out_ga(T27, T115)) → U27_gaga(T27, T115, T112, T29, appJ_in_gga(T112, T115, T29))
appJ_in_gga([], T122, T122) → appJ_out_gga([], T122, T122)
appJ_in_gga(.(T131, T132), T133, .(T131, T135)) → U7_gga(T131, T132, T133, T135, appJ_in_gga(T132, T133, T135))
U7_gga(T131, T132, T133, T135, appJ_out_gga(T132, T133, T135)) → appJ_out_gga(.(T131, T132), T133, .(T131, T135))
U27_gaga(T27, T115, T112, T29, appJ_out_gga(T112, T115, T29)) → pQ_out_gaga(T27, T115, T112, T29)
U25_ggagaa(T108, T109, T112, T27, X55, T29, pQ_out_gaga(T27, X55, T112, T29)) → pP_out_ggagaa(T108, T109, T112, T27, X55, T29)
U23_gagagaa(T107, T109, T108, X170, T27, X55, T29, pP_out_ggagaa(T108, T109, X170, T27, X55, T29)) → pO_out_gagagaa(T107, T109, T108, X170, T27, X55, T29)
U21_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29, pO_out_gagagaa(T107, X169, T108, X170, T27, X55, T29)) → pE_out_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29)
U4_ga(T25, T105, T106, T107, T27, T29, pE_out_gagaagaa(T106, X168, T107, X169, X170, T27, X55, T29)) → frontA_out_ga(tree(T25, tree(T105, T106, T107), T27), T29)

The argument filtering Pi contains the following mapping:
frontA_in_ga(x1, x2) = frontA_in_ga(x1)
void = void
frontA_out_ga(x1, x2) = frontA_out_ga(x1, x2)
tree(x1, x2, x3) = tree(x1, x2, x3)
U1_ga(x1, x2, x3) = U1_ga(x1, x3)
pB_in_aa(x1, x2) = pB_in_aa
U10_aa(x1, x2, x3) = U10_aa(x3)
frontK_in_a(x1) = frontK_in_a
frontK_out_a(x1) = frontK_out_a(x1)
U11_aa(x1, x2, x3) = U11_aa(x1, x3)
appF_in_ga(x1, x2) = appF_in_ga(x1)
appF_out_ga(x1, x2) = appF_out_ga(x1, x2)
pB_out_aa(x1, x2) = pB_out_aa(x1, x2)
U2_ga(x1, x2, x3, x4) = U2_ga(x1, x2, x4)
pC_in_gaa(x1, x2, x3) = pC_in_gaa(x1)
U12_gaa(x1, x2, x3, x4) = U12_gaa(x1, x4)
frontL_in_ga(x1, x2) = frontL_in_ga(x1)
frontL_out_ga(x1, x2) = frontL_out_ga(x1, x2)
U8_ga(x1, x2, x3, x4, x5) = U8_ga(x1, x2, x3, x5)
pH_in_gagaa(x1, x2, x3, x4, x5) = pH_in_gagaa(x1, x3)
U14_gagaa(x1, x2, x3, x4, x5, x6) = U14_gagaa(x1, x3, x6)
frontG_in_ga(x1, x2) = frontG_in_ga(x1)
frontG_out_ga(x1, x2) = frontG_out_ga(x1, x2)
U5_ga(x1, x2, x3, x4, x5) = U5_ga(x1, x2, x3, x5)
pH_out_gagaa(x1, x2, x3, x4, x5) = pH_out_gagaa(x1, x2, x3, x4, x5)
U15_gagaa(x1, x2, x3, x4, x5, x6) = U15_gagaa(x1, x2, x3, x6)
pN_in_gaga(x1, x2, x3, x4) = pN_in_gaga(x1, x3)
U16_gaga(x1, x2, x3, x4, x5) = U16_gaga(x1, x3, x5)
U17_gaga(x1, x2, x3, x4, x5) = U17_gaga(x1, x2, x3, x5)
appI_in_gga(x1, x2, x3) = appI_in_gga(x1, x2)
[] = []
appI_out_gga(x1, x2, x3) = appI_out_gga(x1, x2, x3)
.(x1, x2) = .(x1, x2)
U6_gga(x1, x2, x3, x4, x5) = U6_gga(x1, x2, x3, x5)
pN_out_gaga(x1, x2, x3, x4) = pN_out_gaga(x1, x2, x3, x4)
U13_gaa(x1, x2, x3, x4) = U13_gaa(x1, x2, x4)
pC_out_gaa(x1, x2, x3) = pC_out_gaa(x1, x2, x3)
U3_ga(x1, x2, x3, x4, x5) = U3_ga(x1, x2, x3, x5)
pD_in_gaga(x1, x2, x3, x4) = pD_in_gaga(x1, x3)
U18_gaga(x1, x2, x3, x4, x5) = U18_gaga(x1, x3, x5)
U19_gaga(x1, x2, x3, x4, x5) = U19_gaga(x1, x2, x3, x5)
appM_in_gga(x1, x2, x3) = appM_in_gga(x1, x2)
U9_gga(x1, x2, x3, x4) = U9_gga(x1, x2, x4)
appM_out_gga(x1, x2, x3) = appM_out_gga(x1, x2, x3)
pD_out_gaga(x1, x2, x3, x4) = pD_out_gaga(x1, x2, x3, x4)
U4_ga(x1, x2, x3, x4, x5, x6, x7) = U4_ga(x1, x2, x3, x4, x5, x7)
pE_in_gagaagaa(x1, x2, x3, x4, x5, x6, x7, x8) = pE_in_gagaagaa(x1, x3, x6)
U20_gagaagaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U20_gagaagaa(x1, x3, x6, x9)
U21_gagaagaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U21_gagaagaa(x1, x2, x3, x6, x9)
pO_in_gagagaa(x1, x2, x3, x4, x5, x6, x7) = pO_in_gagagaa(x1, x3, x5)
U22_gagagaa(x1, x2, x3, x4, x5, x6, x7, x8) = U22_gagagaa(x1, x3, x5, x8)
U23_gagagaa(x1, x2, x3, x4, x5, x6, x7, x8) = U23_gagagaa(x1, x2, x3, x5, x8)
pP_in_ggagaa(x1, x2, x3, x4, x5, x6) = pP_in_ggagaa(x1, x2, x4)
U24_ggagaa(x1, x2, x3, x4, x5, x6, x7) = U24_ggagaa(x1, x2, x4, x7)
U25_ggagaa(x1, x2, x3, x4, x5, x6, x7) = U25_ggagaa(x1, x2, x3, x4, x7)
pQ_in_gaga(x1, x2, x3, x4) = pQ_in_gaga(x1, x3)
U26_gaga(x1, x2, x3, x4, x5) = U26_gaga(x1, x3, x5)
U27_gaga(x1, x2, x3, x4, x5) = U27_gaga(x1, x2, x3, x5)
appJ_in_gga(x1, x2, x3) = appJ_in_gga(x1, x2)
appJ_out_gga(x1, x2, x3) = appJ_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4, x5) = U7_gga(x1, x2, x3, x5)
pQ_out_gaga(x1, x2, x3, x4) = pQ_out_gaga(x1, x2, x3, x4)
pP_out_ggagaa(x1, x2, x3, x4, x5, x6) = pP_out_ggagaa(x1, x2, x3, x4, x5, x6)
pO_out_gagagaa(x1, x2, x3, x4, x5, x6, x7) = pO_out_gagagaa(x1, x2, x3, x4, x5, x6, x7)
pE_out_gagaagaa(x1, x2, x3, x4, x5, x6, x7, x8) = pE_out_gagaagaa(x1, x2, x3, x4, x5, x6, x7, x8)
FRONTA_IN_GA(x1, x2) = FRONTA_IN_GA(x1)
U1_GA(x1, x2, x3) = U1_GA(x1, x3)
PB_IN_AA(x1, x2) = PB_IN_AA
U10_AA(x1, x2, x3) = U10_AA(x3)
FRONTK_IN_A(x1) = FRONTK_IN_A
U11_AA(x1, x2, x3) = U11_AA(x1, x3)
APPF_IN_GA(x1, x2) = APPF_IN_GA(x1)
U2_GA(x1, x2, x3, x4) = U2_GA(x1, x2, x4)
PC_IN_GAA(x1, x2, x3) = PC_IN_GAA(x1)
U12_GAA(x1, x2, x3, x4) = U12_GAA(x1, x4)
FRONTL_IN_GA(x1, x2) = FRONTL_IN_GA(x1)
U8_GA(x1, x2, x3, x4, x5) = U8_GA(x1, x2, x3, x5)
PH_IN_GAGAA(x1, x2, x3, x4, x5) = PH_IN_GAGAA(x1, x3)
U14_GAGAA(x1, x2, x3, x4, x5, x6) = U14_GAGAA(x1, x3, x6)
FRONTG_IN_GA(x1, x2) = FRONTG_IN_GA(x1)
U5_GA(x1, x2, x3, x4, x5) = U5_GA(x1, x2, x3, x5)
U15_GAGAA(x1, x2, x3, x4, x5, x6) = U15_GAGAA(x1, x2, x3, x6)
PN_IN_GAGA(x1, x2, x3, x4) = PN_IN_GAGA(x1, x3)
U16_GAGA(x1, x2, x3, x4, x5) = U16_GAGA(x1, x3, x5)
U17_GAGA(x1, x2, x3, x4, x5) = U17_GAGA(x1, x2, x3, x5)
APPI_IN_GGA(x1, x2, x3) = APPI_IN_GGA(x1, x2)
U6_GGA(x1, x2, x3, x4, x5) = U6_GGA(x1, x2, x3, x5)
U13_GAA(x1, x2, x3, x4) = U13_GAA(x1, x2, x4)
U3_GA(x1, x2, x3, x4, x5) = U3_GA(x1, x2, x3, x5)
PD_IN_GAGA(x1, x2, x3, x4) = PD_IN_GAGA(x1, x3)
U18_GAGA(x1, x2, x3, x4, x5) = U18_GAGA(x1, x3, x5)
U19_GAGA(x1, x2, x3, x4, x5) = U19_GAGA(x1, x2, x3, x5)
APPM_IN_GGA(x1, x2, x3) = APPM_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3, x4) = U9_GGA(x1, x2, x4)
U4_GA(x1, x2, x3, x4, x5, x6, x7) = U4_GA(x1, x2, x3, x4, x5, x7)
PE_IN_GAGAAGAA(x1, x2, x3, x4, x5, x6, x7, x8) = PE_IN_GAGAAGAA(x1, x3, x6)
U20_GAGAAGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U20_GAGAAGAA(x1, x3, x6, x9)
U21_GAGAAGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U21_GAGAAGAA(x1, x2, x3, x6, x9)
PO_IN_GAGAGAA(x1, x2, x3, x4, x5, x6, x7) = PO_IN_GAGAGAA(x1, x3, x5)
U22_GAGAGAA(x1, x2, x3, x4, x5, x6, x7, x8) = U22_GAGAGAA(x1, x3, x5, x8)
U23_GAGAGAA(x1, x2, x3, x4, x5, x6, x7, x8) = U23_GAGAGAA(x1, x2, x3, x5, x8)
PP_IN_GGAGAA(x1, x2, x3, x4, x5, x6) = PP_IN_GGAGAA(x1, x2, x4)
U24_GGAGAA(x1, x2, x3, x4, x5, x6, x7) = U24_GGAGAA(x1, x2, x4, x7)
U25_GGAGAA(x1, x2, x3, x4, x5, x6, x7) = U25_GGAGAA(x1, x2, x3, x4, x7)
PQ_IN_GAGA(x1, x2, x3, x4) = PQ_IN_GAGA(x1, x3)
U26_GAGA(x1, x2, x3, x4, x5) = U26_GAGA(x1, x3, x5)
U27_GAGA(x1, x2, x3, x4, x5) = U27_GAGA(x1, x2, x3, x5)
APPJ_IN_GGA(x1, x2, x3) = APPJ_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4, x5) = U7_GGA(x1, x2, x3, x5)

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

(4) Obligation:

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

FRONTA_IN_GA(tree(T7, void, void), T9) → U1_GA(T7, T9, pB_in_aa(X18, T9))
FRONTA_IN_GA(tree(T7, void, void), T9) → PB_IN_AA(X18, T9)
PB_IN_AA(T13, T9) → U10_AA(T13, T9, frontK_in_a(T13))
PB_IN_AA(T13, T9) → FRONTK_IN_A(T13)
U10_AA(T13, T9, frontK_out_a(T13)) → U11_AA(T13, T9, appF_in_ga(T13, T9))
U10_AA(T13, T9, frontK_out_a(T13)) → APPF_IN_GA(T13, T9)
FRONTA_IN_GA(tree(T25, void, T27), T29) → U2_GA(T25, T27, T29, pC_in_gaa(T27, X55, T29))
FRONTA_IN_GA(tree(T25, void, T27), T29) → PC_IN_GAA(T27, X55, T29)
PC_IN_GAA(T27, T30, T29) → U12_GAA(T27, T30, T29, frontL_in_ga(T27, T30))
PC_IN_GAA(T27, T30, T29) → FRONTL_IN_GA(T27, T30)
FRONTL_IN_GA(tree(T42, T43, T44), X79) → U8_GA(T42, T43, T44, X79, pH_in_gagaa(T43, X77, T44, X78, X79))
FRONTL_IN_GA(tree(T42, T43, T44), X79) → PH_IN_GAGAA(T43, X77, T44, X78, X79)
PH_IN_GAGAA(T43, T45, T44, X78, X79) → U14_GAGAA(T43, T45, T44, X78, X79, frontG_in_ga(T43, T45))
PH_IN_GAGAA(T43, T45, T44, X78, X79) → FRONTG_IN_GA(T43, T45)
FRONTG_IN_GA(tree(T57, T58, T59), X103) → U5_GA(T57, T58, T59, X103, pH_in_gagaa(T58, X101, T59, X102, X103))
FRONTG_IN_GA(tree(T57, T58, T59), X103) → PH_IN_GAGAA(T58, X101, T59, X102, X103)
U14_GAGAA(T43, T45, T44, X78, X79, frontG_out_ga(T43, T45)) → U15_GAGAA(T43, T45, T44, X78, X79, pN_in_gaga(T44, X78, T45, X79))
U14_GAGAA(T43, T45, T44, X78, X79, frontG_out_ga(T43, T45)) → PN_IN_GAGA(T44, X78, T45, X79)
PN_IN_GAGA(T44, T60, T45, X79) → U16_GAGA(T44, T60, T45, X79, frontG_in_ga(T44, T60))
PN_IN_GAGA(T44, T60, T45, X79) → FRONTG_IN_GA(T44, T60)
U16_GAGA(T44, T60, T45, X79, frontG_out_ga(T44, T60)) → U17_GAGA(T44, T60, T45, X79, appI_in_gga(T45, T60, X79))
U16_GAGA(T44, T60, T45, X79, frontG_out_ga(T44, T60)) → APPI_IN_GGA(T45, T60, X79)
APPI_IN_GGA(.(T74, T75), T76, .(T74, X125)) → U6_GGA(T74, T75, T76, X125, appI_in_gga(T75, T76, X125))
APPI_IN_GGA(.(T74, T75), T76, .(T74, X125)) → APPI_IN_GGA(T75, T76, X125)
U12_GAA(T27, T30, T29, frontL_out_ga(T27, T30)) → U13_GAA(T27, T30, T29, appF_in_ga(T30, T29))
U12_GAA(T27, T30, T29, frontL_out_ga(T27, T30)) → APPF_IN_GA(T30, T29)
FRONTA_IN_GA(tree(T25, tree(T85, void, void), T27), T29) → U3_GA(T25, T85, T27, T29, pD_in_gaga(T27, X55, T85, T29))
FRONTA_IN_GA(tree(T25, tree(T85, void, void), T27), T29) → PD_IN_GAGA(T27, X55, T85, T29)
PD_IN_GAGA(T27, T86, T85, T29) → U18_GAGA(T27, T86, T85, T29, frontG_in_ga(T27, T86))
PD_IN_GAGA(T27, T86, T85, T29) → FRONTG_IN_GA(T27, T86)
U18_GAGA(T27, T86, T85, T29, frontG_out_ga(T27, T86)) → U19_GAGA(T27, T86, T85, T29, appM_in_gga(T85, T86, T29))
U18_GAGA(T27, T86, T85, T29, frontG_out_ga(T27, T86)) → APPM_IN_GGA(T85, T86, T29)
APPM_IN_GGA(T93, T94, .(T93, T96)) → U9_GGA(T93, T94, T96, appF_in_ga(T94, T96))
APPM_IN_GGA(T93, T94, .(T93, T96)) → APPF_IN_GA(T94, T96)
FRONTA_IN_GA(tree(T25, tree(T105, T106, T107), T27), T29) → U4_GA(T25, T105, T106, T107, T27, T29, pE_in_gagaagaa(T106, X168, T107, X169, X170, T27, X55, T29))
FRONTA_IN_GA(tree(T25, tree(T105, T106, T107), T27), T29) → PE_IN_GAGAAGAA(T106, X168, T107, X169, X170, T27, X55, T29)
PE_IN_GAGAAGAA(T106, T108, T107, X169, X170, T27, X55, T29) → U20_GAGAAGAA(T106, T108, T107, X169, X170, T27, X55, T29, frontG_in_ga(T106, T108))
PE_IN_GAGAAGAA(T106, T108, T107, X169, X170, T27, X55, T29) → FRONTG_IN_GA(T106, T108)
U20_GAGAAGAA(T106, T108, T107, X169, X170, T27, X55, T29, frontG_out_ga(T106, T108)) → U21_GAGAAGAA(T106, T108, T107, X169, X170, T27, X55, T29, pO_in_gagagaa(T107, X169, T108, X170, T27, X55, T29))
U20_GAGAAGAA(T106, T108, T107, X169, X170, T27, X55, T29, frontG_out_ga(T106, T108)) → PO_IN_GAGAGAA(T107, X169, T108, X170, T27, X55, T29)
PO_IN_GAGAGAA(T107, T109, T108, X170, T27, X55, T29) → U22_GAGAGAA(T107, T109, T108, X170, T27, X55, T29, frontG_in_ga(T107, T109))
PO_IN_GAGAGAA(T107, T109, T108, X170, T27, X55, T29) → FRONTG_IN_GA(T107, T109)
U22_GAGAGAA(T107, T109, T108, X170, T27, X55, T29, frontG_out_ga(T107, T109)) → U23_GAGAGAA(T107, T109, T108, X170, T27, X55, T29, pP_in_ggagaa(T108, T109, X170, T27, X55, T29))
U22_GAGAGAA(T107, T109, T108, X170, T27, X55, T29, frontG_out_ga(T107, T109)) → PP_IN_GGAGAA(T108, T109, X170, T27, X55, T29)
PP_IN_GGAGAA(T108, T109, T112, T27, X55, T29) → U24_GGAGAA(T108, T109, T112, T27, X55, T29, appI_in_gga(T108, T109, T112))
PP_IN_GGAGAA(T108, T109, T112, T27, X55, T29) → APPI_IN_GGA(T108, T109, T112)
U24_GGAGAA(T108, T109, T112, T27, X55, T29, appI_out_gga(T108, T109, T112)) → U25_GGAGAA(T108, T109, T112, T27, X55, T29, pQ_in_gaga(T27, X55, T112, T29))
U24_GGAGAA(T108, T109, T112, T27, X55, T29, appI_out_gga(T108, T109, T112)) → PQ_IN_GAGA(T27, X55, T112, T29)
PQ_IN_GAGA(T27, T115, T112, T29) → U26_GAGA(T27, T115, T112, T29, frontG_in_ga(T27, T115))
PQ_IN_GAGA(T27, T115, T112, T29) → FRONTG_IN_GA(T27, T115)
U26_GAGA(T27, T115, T112, T29, frontG_out_ga(T27, T115)) → U27_GAGA(T27, T115, T112, T29, appJ_in_gga(T112, T115, T29))
U26_GAGA(T27, T115, T112, T29, frontG_out_ga(T27, T115)) → APPJ_IN_GGA(T112, T115, T29)
APPJ_IN_GGA(.(T131, T132), T133, .(T131, T135)) → U7_GGA(T131, T132, T133, T135, appJ_in_gga(T132, T133, T135))
APPJ_IN_GGA(.(T131, T132), T133, .(T131, T135)) → APPJ_IN_GGA(T132, T133, T135)

The TRS R consists of the following rules:

frontA_in_ga(void, []) → frontA_out_ga(void, [])
frontA_in_ga(tree(T4, void, void), .(T4, [])) → frontA_out_ga(tree(T4, void, void), .(T4, []))
frontA_in_ga(tree(T7, void, void), T9) → U1_ga(T7, T9, pB_in_aa(X18, T9))
pB_in_aa(T13, T9) → U10_aa(T13, T9, frontK_in_a(T13))
frontK_in_a([]) → frontK_out_a([])
U10_aa(T13, T9, frontK_out_a(T13)) → U11_aa(T13, T9, appF_in_ga(T13, T9))
appF_in_ga(T20, T20) → appF_out_ga(T20, T20)
U11_aa(T13, T9, appF_out_ga(T13, T9)) → pB_out_aa(T13, T9)
U1_ga(T7, T9, pB_out_aa(X18, T9)) → frontA_out_ga(tree(T7, void, void), T9)
frontA_in_ga(tree(T25, void, T27), T29) → U2_ga(T25, T27, T29, pC_in_gaa(T27, X55, T29))
pC_in_gaa(T27, T30, T29) → U12_gaa(T27, T30, T29, frontL_in_ga(T27, T30))
frontL_in_ga(void, []) → frontL_out_ga(void, [])
frontL_in_ga(tree(T35, void, void), .(T35, [])) → frontL_out_ga(tree(T35, void, void), .(T35, []))
frontL_in_ga(tree(T42, T43, T44), X79) → U8_ga(T42, T43, T44, X79, pH_in_gagaa(T43, X77, T44, X78, X79))
pH_in_gagaa(T43, T45, T44, X78, X79) → U14_gagaa(T43, T45, T44, X78, X79, frontG_in_ga(T43, T45))
frontG_in_ga(void, []) → frontG_out_ga(void, [])
frontG_in_ga(tree(T50, void, void), .(T50, [])) → frontG_out_ga(tree(T50, void, void), .(T50, []))
frontG_in_ga(tree(T57, T58, T59), X103) → U5_ga(T57, T58, T59, X103, pH_in_gagaa(T58, X101, T59, X102, X103))
U5_ga(T57, T58, T59, X103, pH_out_gagaa(T58, X101, T59, X102, X103)) → frontG_out_ga(tree(T57, T58, T59), X103)
U14_gagaa(T43, T45, T44, X78, X79, frontG_out_ga(T43, T45)) → U15_gagaa(T43, T45, T44, X78, X79, pN_in_gaga(T44, X78, T45, X79))
pN_in_gaga(T44, T60, T45, X79) → U16_gaga(T44, T60, T45, X79, frontG_in_ga(T44, T60))
U16_gaga(T44, T60, T45, X79, frontG_out_ga(T44, T60)) → U17_gaga(T44, T60, T45, X79, appI_in_gga(T45, T60, X79))
appI_in_gga([], T67, T67) → appI_out_gga([], T67, T67)
appI_in_gga(.(T74, T75), T76, .(T74, X125)) → U6_gga(T74, T75, T76, X125, appI_in_gga(T75, T76, X125))
U6_gga(T74, T75, T76, X125, appI_out_gga(T75, T76, X125)) → appI_out_gga(.(T74, T75), T76, .(T74, X125))
U17_gaga(T44, T60, T45, X79, appI_out_gga(T45, T60, X79)) → pN_out_gaga(T44, T60, T45, X79)
U15_gagaa(T43, T45, T44, X78, X79, pN_out_gaga(T44, X78, T45, X79)) → pH_out_gagaa(T43, T45, T44, X78, X79)
U8_ga(T42, T43, T44, X79, pH_out_gagaa(T43, X77, T44, X78, X79)) → frontL_out_ga(tree(T42, T43, T44), X79)
U12_gaa(T27, T30, T29, frontL_out_ga(T27, T30)) → U13_gaa(T27, T30, T29, appF_in_ga(T30, T29))
U13_gaa(T27, T30, T29, appF_out_ga(T30, T29)) → pC_out_gaa(T27, T30, T29)
U2_ga(T25, T27, T29, pC_out_gaa(T27, X55, T29)) → frontA_out_ga(tree(T25, void, T27), T29)
frontA_in_ga(tree(T25, tree(T85, void, void), T27), T29) → U3_ga(T25, T85, T27, T29, pD_in_gaga(T27, X55, T85, T29))
pD_in_gaga(T27, T86, T85, T29) → U18_gaga(T27, T86, T85, T29, frontG_in_ga(T27, T86))
U18_gaga(T27, T86, T85, T29, frontG_out_ga(T27, T86)) → U19_gaga(T27, T86, T85, T29, appM_in_gga(T85, T86, T29))
appM_in_gga(T93, T94, .(T93, T96)) → U9_gga(T93, T94, T96, appF_in_ga(T94, T96))
U9_gga(T93, T94, T96, appF_out_ga(T94, T96)) → appM_out_gga(T93, T94, .(T93, T96))
U19_gaga(T27, T86, T85, T29, appM_out_gga(T85, T86, T29)) → pD_out_gaga(T27, T86, T85, T29)
U3_ga(T25, T85, T27, T29, pD_out_gaga(T27, X55, T85, T29)) → frontA_out_ga(tree(T25, tree(T85, void, void), T27), T29)
frontA_in_ga(tree(T25, tree(T105, T106, T107), T27), T29) → U4_ga(T25, T105, T106, T107, T27, T29, pE_in_gagaagaa(T106, X168, T107, X169, X170, T27, X55, T29))
pE_in_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29) → U20_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29, frontG_in_ga(T106, T108))
U20_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29, frontG_out_ga(T106, T108)) → U21_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29, pO_in_gagagaa(T107, X169, T108, X170, T27, X55, T29))
pO_in_gagagaa(T107, T109, T108, X170, T27, X55, T29) → U22_gagagaa(T107, T109, T108, X170, T27, X55, T29, frontG_in_ga(T107, T109))
U22_gagagaa(T107, T109, T108, X170, T27, X55, T29, frontG_out_ga(T107, T109)) → U23_gagagaa(T107, T109, T108, X170, T27, X55, T29, pP_in_ggagaa(T108, T109, X170, T27, X55, T29))
pP_in_ggagaa(T108, T109, T112, T27, X55, T29) → U24_ggagaa(T108, T109, T112, T27, X55, T29, appI_in_gga(T108, T109, T112))
U24_ggagaa(T108, T109, T112, T27, X55, T29, appI_out_gga(T108, T109, T112)) → U25_ggagaa(T108, T109, T112, T27, X55, T29, pQ_in_gaga(T27, X55, T112, T29))
pQ_in_gaga(T27, T115, T112, T29) → U26_gaga(T27, T115, T112, T29, frontG_in_ga(T27, T115))
U26_gaga(T27, T115, T112, T29, frontG_out_ga(T27, T115)) → U27_gaga(T27, T115, T112, T29, appJ_in_gga(T112, T115, T29))
appJ_in_gga([], T122, T122) → appJ_out_gga([], T122, T122)
appJ_in_gga(.(T131, T132), T133, .(T131, T135)) → U7_gga(T131, T132, T133, T135, appJ_in_gga(T132, T133, T135))
U7_gga(T131, T132, T133, T135, appJ_out_gga(T132, T133, T135)) → appJ_out_gga(.(T131, T132), T133, .(T131, T135))
U27_gaga(T27, T115, T112, T29, appJ_out_gga(T112, T115, T29)) → pQ_out_gaga(T27, T115, T112, T29)
U25_ggagaa(T108, T109, T112, T27, X55, T29, pQ_out_gaga(T27, X55, T112, T29)) → pP_out_ggagaa(T108, T109, T112, T27, X55, T29)
U23_gagagaa(T107, T109, T108, X170, T27, X55, T29, pP_out_ggagaa(T108, T109, X170, T27, X55, T29)) → pO_out_gagagaa(T107, T109, T108, X170, T27, X55, T29)
U21_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29, pO_out_gagagaa(T107, X169, T108, X170, T27, X55, T29)) → pE_out_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29)
U4_ga(T25, T105, T106, T107, T27, T29, pE_out_gagaagaa(T106, X168, T107, X169, X170, T27, X55, T29)) → frontA_out_ga(tree(T25, tree(T105, T106, T107), T27), T29)

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

APPJ_IN_GGA(.(T131, T132), T133, .(T131, T135)) → APPJ_IN_GGA(T132, T133, T135)

The TRS R consists of the following rules:

frontA_in_ga(void, []) → frontA_out_ga(void, [])
frontA_in_ga(tree(T4, void, void), .(T4, [])) → frontA_out_ga(tree(T4, void, void), .(T4, []))
frontA_in_ga(tree(T7, void, void), T9) → U1_ga(T7, T9, pB_in_aa(X18, T9))
pB_in_aa(T13, T9) → U10_aa(T13, T9, frontK_in_a(T13))
frontK_in_a([]) → frontK_out_a([])
U10_aa(T13, T9, frontK_out_a(T13)) → U11_aa(T13, T9, appF_in_ga(T13, T9))
appF_in_ga(T20, T20) → appF_out_ga(T20, T20)
U11_aa(T13, T9, appF_out_ga(T13, T9)) → pB_out_aa(T13, T9)
U1_ga(T7, T9, pB_out_aa(X18, T9)) → frontA_out_ga(tree(T7, void, void), T9)
frontA_in_ga(tree(T25, void, T27), T29) → U2_ga(T25, T27, T29, pC_in_gaa(T27, X55, T29))
pC_in_gaa(T27, T30, T29) → U12_gaa(T27, T30, T29, frontL_in_ga(T27, T30))
frontL_in_ga(void, []) → frontL_out_ga(void, [])
frontL_in_ga(tree(T35, void, void), .(T35, [])) → frontL_out_ga(tree(T35, void, void), .(T35, []))
frontL_in_ga(tree(T42, T43, T44), X79) → U8_ga(T42, T43, T44, X79, pH_in_gagaa(T43, X77, T44, X78, X79))
pH_in_gagaa(T43, T45, T44, X78, X79) → U14_gagaa(T43, T45, T44, X78, X79, frontG_in_ga(T43, T45))
frontG_in_ga(void, []) → frontG_out_ga(void, [])
frontG_in_ga(tree(T50, void, void), .(T50, [])) → frontG_out_ga(tree(T50, void, void), .(T50, []))
frontG_in_ga(tree(T57, T58, T59), X103) → U5_ga(T57, T58, T59, X103, pH_in_gagaa(T58, X101, T59, X102, X103))
U5_ga(T57, T58, T59, X103, pH_out_gagaa(T58, X101, T59, X102, X103)) → frontG_out_ga(tree(T57, T58, T59), X103)
U14_gagaa(T43, T45, T44, X78, X79, frontG_out_ga(T43, T45)) → U15_gagaa(T43, T45, T44, X78, X79, pN_in_gaga(T44, X78, T45, X79))
pN_in_gaga(T44, T60, T45, X79) → U16_gaga(T44, T60, T45, X79, frontG_in_ga(T44, T60))
U16_gaga(T44, T60, T45, X79, frontG_out_ga(T44, T60)) → U17_gaga(T44, T60, T45, X79, appI_in_gga(T45, T60, X79))
appI_in_gga([], T67, T67) → appI_out_gga([], T67, T67)
appI_in_gga(.(T74, T75), T76, .(T74, X125)) → U6_gga(T74, T75, T76, X125, appI_in_gga(T75, T76, X125))
U6_gga(T74, T75, T76, X125, appI_out_gga(T75, T76, X125)) → appI_out_gga(.(T74, T75), T76, .(T74, X125))
U17_gaga(T44, T60, T45, X79, appI_out_gga(T45, T60, X79)) → pN_out_gaga(T44, T60, T45, X79)
U15_gagaa(T43, T45, T44, X78, X79, pN_out_gaga(T44, X78, T45, X79)) → pH_out_gagaa(T43, T45, T44, X78, X79)
U8_ga(T42, T43, T44, X79, pH_out_gagaa(T43, X77, T44, X78, X79)) → frontL_out_ga(tree(T42, T43, T44), X79)
U12_gaa(T27, T30, T29, frontL_out_ga(T27, T30)) → U13_gaa(T27, T30, T29, appF_in_ga(T30, T29))
U13_gaa(T27, T30, T29, appF_out_ga(T30, T29)) → pC_out_gaa(T27, T30, T29)
U2_ga(T25, T27, T29, pC_out_gaa(T27, X55, T29)) → frontA_out_ga(tree(T25, void, T27), T29)
frontA_in_ga(tree(T25, tree(T85, void, void), T27), T29) → U3_ga(T25, T85, T27, T29, pD_in_gaga(T27, X55, T85, T29))
pD_in_gaga(T27, T86, T85, T29) → U18_gaga(T27, T86, T85, T29, frontG_in_ga(T27, T86))
U18_gaga(T27, T86, T85, T29, frontG_out_ga(T27, T86)) → U19_gaga(T27, T86, T85, T29, appM_in_gga(T85, T86, T29))
appM_in_gga(T93, T94, .(T93, T96)) → U9_gga(T93, T94, T96, appF_in_ga(T94, T96))
U9_gga(T93, T94, T96, appF_out_ga(T94, T96)) → appM_out_gga(T93, T94, .(T93, T96))
U19_gaga(T27, T86, T85, T29, appM_out_gga(T85, T86, T29)) → pD_out_gaga(T27, T86, T85, T29)
U3_ga(T25, T85, T27, T29, pD_out_gaga(T27, X55, T85, T29)) → frontA_out_ga(tree(T25, tree(T85, void, void), T27), T29)
frontA_in_ga(tree(T25, tree(T105, T106, T107), T27), T29) → U4_ga(T25, T105, T106, T107, T27, T29, pE_in_gagaagaa(T106, X168, T107, X169, X170, T27, X55, T29))
pE_in_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29) → U20_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29, frontG_in_ga(T106, T108))
U20_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29, frontG_out_ga(T106, T108)) → U21_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29, pO_in_gagagaa(T107, X169, T108, X170, T27, X55, T29))
pO_in_gagagaa(T107, T109, T108, X170, T27, X55, T29) → U22_gagagaa(T107, T109, T108, X170, T27, X55, T29, frontG_in_ga(T107, T109))
U22_gagagaa(T107, T109, T108, X170, T27, X55, T29, frontG_out_ga(T107, T109)) → U23_gagagaa(T107, T109, T108, X170, T27, X55, T29, pP_in_ggagaa(T108, T109, X170, T27, X55, T29))
pP_in_ggagaa(T108, T109, T112, T27, X55, T29) → U24_ggagaa(T108, T109, T112, T27, X55, T29, appI_in_gga(T108, T109, T112))
U24_ggagaa(T108, T109, T112, T27, X55, T29, appI_out_gga(T108, T109, T112)) → U25_ggagaa(T108, T109, T112, T27, X55, T29, pQ_in_gaga(T27, X55, T112, T29))
pQ_in_gaga(T27, T115, T112, T29) → U26_gaga(T27, T115, T112, T29, frontG_in_ga(T27, T115))
U26_gaga(T27, T115, T112, T29, frontG_out_ga(T27, T115)) → U27_gaga(T27, T115, T112, T29, appJ_in_gga(T112, T115, T29))
appJ_in_gga([], T122, T122) → appJ_out_gga([], T122, T122)
appJ_in_gga(.(T131, T132), T133, .(T131, T135)) → U7_gga(T131, T132, T133, T135, appJ_in_gga(T132, T133, T135))
U7_gga(T131, T132, T133, T135, appJ_out_gga(T132, T133, T135)) → appJ_out_gga(.(T131, T132), T133, .(T131, T135))
U27_gaga(T27, T115, T112, T29, appJ_out_gga(T112, T115, T29)) → pQ_out_gaga(T27, T115, T112, T29)
U25_ggagaa(T108, T109, T112, T27, X55, T29, pQ_out_gaga(T27, X55, T112, T29)) → pP_out_ggagaa(T108, T109, T112, T27, X55, T29)
U23_gagagaa(T107, T109, T108, X170, T27, X55, T29, pP_out_ggagaa(T108, T109, X170, T27, X55, T29)) → pO_out_gagagaa(T107, T109, T108, X170, T27, X55, T29)
U21_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29, pO_out_gagagaa(T107, X169, T108, X170, T27, X55, T29)) → pE_out_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29)
U4_ga(T25, T105, T106, T107, T27, T29, pE_out_gagaagaa(T106, X168, T107, X169, X170, T27, X55, T29)) → frontA_out_ga(tree(T25, tree(T105, T106, T107), T27), T29)

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

APPJ_IN_GGA(.(T131, T132), T133, .(T131, T135)) → APPJ_IN_GGA(T132, T133, T135)

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

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:

APPJ_IN_GGA(.(T131, T132), T133) → APPJ_IN_GGA(T132, T133)

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:

APPJ_IN_GGA(.(T131, T132), T133) → APPJ_IN_GGA(T132, T133)
The graph contains the following edges 1 > 1, 2 >= 2

(13) YES

(14) Obligation:

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

APPI_IN_GGA(.(T74, T75), T76, .(T74, X125)) → APPI_IN_GGA(T75, T76, X125)

The TRS R consists of the following rules:

frontA_in_ga(void, []) → frontA_out_ga(void, [])
frontA_in_ga(tree(T4, void, void), .(T4, [])) → frontA_out_ga(tree(T4, void, void), .(T4, []))
frontA_in_ga(tree(T7, void, void), T9) → U1_ga(T7, T9, pB_in_aa(X18, T9))
pB_in_aa(T13, T9) → U10_aa(T13, T9, frontK_in_a(T13))
frontK_in_a([]) → frontK_out_a([])
U10_aa(T13, T9, frontK_out_a(T13)) → U11_aa(T13, T9, appF_in_ga(T13, T9))
appF_in_ga(T20, T20) → appF_out_ga(T20, T20)
U11_aa(T13, T9, appF_out_ga(T13, T9)) → pB_out_aa(T13, T9)
U1_ga(T7, T9, pB_out_aa(X18, T9)) → frontA_out_ga(tree(T7, void, void), T9)
frontA_in_ga(tree(T25, void, T27), T29) → U2_ga(T25, T27, T29, pC_in_gaa(T27, X55, T29))
pC_in_gaa(T27, T30, T29) → U12_gaa(T27, T30, T29, frontL_in_ga(T27, T30))
frontL_in_ga(void, []) → frontL_out_ga(void, [])
frontL_in_ga(tree(T35, void, void), .(T35, [])) → frontL_out_ga(tree(T35, void, void), .(T35, []))
frontL_in_ga(tree(T42, T43, T44), X79) → U8_ga(T42, T43, T44, X79, pH_in_gagaa(T43, X77, T44, X78, X79))
pH_in_gagaa(T43, T45, T44, X78, X79) → U14_gagaa(T43, T45, T44, X78, X79, frontG_in_ga(T43, T45))
frontG_in_ga(void, []) → frontG_out_ga(void, [])
frontG_in_ga(tree(T50, void, void), .(T50, [])) → frontG_out_ga(tree(T50, void, void), .(T50, []))
frontG_in_ga(tree(T57, T58, T59), X103) → U5_ga(T57, T58, T59, X103, pH_in_gagaa(T58, X101, T59, X102, X103))
U5_ga(T57, T58, T59, X103, pH_out_gagaa(T58, X101, T59, X102, X103)) → frontG_out_ga(tree(T57, T58, T59), X103)
U14_gagaa(T43, T45, T44, X78, X79, frontG_out_ga(T43, T45)) → U15_gagaa(T43, T45, T44, X78, X79, pN_in_gaga(T44, X78, T45, X79))
pN_in_gaga(T44, T60, T45, X79) → U16_gaga(T44, T60, T45, X79, frontG_in_ga(T44, T60))
U16_gaga(T44, T60, T45, X79, frontG_out_ga(T44, T60)) → U17_gaga(T44, T60, T45, X79, appI_in_gga(T45, T60, X79))
appI_in_gga([], T67, T67) → appI_out_gga([], T67, T67)
appI_in_gga(.(T74, T75), T76, .(T74, X125)) → U6_gga(T74, T75, T76, X125, appI_in_gga(T75, T76, X125))
U6_gga(T74, T75, T76, X125, appI_out_gga(T75, T76, X125)) → appI_out_gga(.(T74, T75), T76, .(T74, X125))
U17_gaga(T44, T60, T45, X79, appI_out_gga(T45, T60, X79)) → pN_out_gaga(T44, T60, T45, X79)
U15_gagaa(T43, T45, T44, X78, X79, pN_out_gaga(T44, X78, T45, X79)) → pH_out_gagaa(T43, T45, T44, X78, X79)
U8_ga(T42, T43, T44, X79, pH_out_gagaa(T43, X77, T44, X78, X79)) → frontL_out_ga(tree(T42, T43, T44), X79)
U12_gaa(T27, T30, T29, frontL_out_ga(T27, T30)) → U13_gaa(T27, T30, T29, appF_in_ga(T30, T29))
U13_gaa(T27, T30, T29, appF_out_ga(T30, T29)) → pC_out_gaa(T27, T30, T29)
U2_ga(T25, T27, T29, pC_out_gaa(T27, X55, T29)) → frontA_out_ga(tree(T25, void, T27), T29)
frontA_in_ga(tree(T25, tree(T85, void, void), T27), T29) → U3_ga(T25, T85, T27, T29, pD_in_gaga(T27, X55, T85, T29))
pD_in_gaga(T27, T86, T85, T29) → U18_gaga(T27, T86, T85, T29, frontG_in_ga(T27, T86))
U18_gaga(T27, T86, T85, T29, frontG_out_ga(T27, T86)) → U19_gaga(T27, T86, T85, T29, appM_in_gga(T85, T86, T29))
appM_in_gga(T93, T94, .(T93, T96)) → U9_gga(T93, T94, T96, appF_in_ga(T94, T96))
U9_gga(T93, T94, T96, appF_out_ga(T94, T96)) → appM_out_gga(T93, T94, .(T93, T96))
U19_gaga(T27, T86, T85, T29, appM_out_gga(T85, T86, T29)) → pD_out_gaga(T27, T86, T85, T29)
U3_ga(T25, T85, T27, T29, pD_out_gaga(T27, X55, T85, T29)) → frontA_out_ga(tree(T25, tree(T85, void, void), T27), T29)
frontA_in_ga(tree(T25, tree(T105, T106, T107), T27), T29) → U4_ga(T25, T105, T106, T107, T27, T29, pE_in_gagaagaa(T106, X168, T107, X169, X170, T27, X55, T29))
pE_in_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29) → U20_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29, frontG_in_ga(T106, T108))
U20_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29, frontG_out_ga(T106, T108)) → U21_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29, pO_in_gagagaa(T107, X169, T108, X170, T27, X55, T29))
pO_in_gagagaa(T107, T109, T108, X170, T27, X55, T29) → U22_gagagaa(T107, T109, T108, X170, T27, X55, T29, frontG_in_ga(T107, T109))
U22_gagagaa(T107, T109, T108, X170, T27, X55, T29, frontG_out_ga(T107, T109)) → U23_gagagaa(T107, T109, T108, X170, T27, X55, T29, pP_in_ggagaa(T108, T109, X170, T27, X55, T29))
pP_in_ggagaa(T108, T109, T112, T27, X55, T29) → U24_ggagaa(T108, T109, T112, T27, X55, T29, appI_in_gga(T108, T109, T112))
U24_ggagaa(T108, T109, T112, T27, X55, T29, appI_out_gga(T108, T109, T112)) → U25_ggagaa(T108, T109, T112, T27, X55, T29, pQ_in_gaga(T27, X55, T112, T29))
pQ_in_gaga(T27, T115, T112, T29) → U26_gaga(T27, T115, T112, T29, frontG_in_ga(T27, T115))
U26_gaga(T27, T115, T112, T29, frontG_out_ga(T27, T115)) → U27_gaga(T27, T115, T112, T29, appJ_in_gga(T112, T115, T29))
appJ_in_gga([], T122, T122) → appJ_out_gga([], T122, T122)
appJ_in_gga(.(T131, T132), T133, .(T131, T135)) → U7_gga(T131, T132, T133, T135, appJ_in_gga(T132, T133, T135))
U7_gga(T131, T132, T133, T135, appJ_out_gga(T132, T133, T135)) → appJ_out_gga(.(T131, T132), T133, .(T131, T135))
U27_gaga(T27, T115, T112, T29, appJ_out_gga(T112, T115, T29)) → pQ_out_gaga(T27, T115, T112, T29)
U25_ggagaa(T108, T109, T112, T27, X55, T29, pQ_out_gaga(T27, X55, T112, T29)) → pP_out_ggagaa(T108, T109, T112, T27, X55, T29)
U23_gagagaa(T107, T109, T108, X170, T27, X55, T29, pP_out_ggagaa(T108, T109, X170, T27, X55, T29)) → pO_out_gagagaa(T107, T109, T108, X170, T27, X55, T29)
U21_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29, pO_out_gagagaa(T107, X169, T108, X170, T27, X55, T29)) → pE_out_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29)
U4_ga(T25, T105, T106, T107, T27, T29, pE_out_gagaagaa(T106, X168, T107, X169, X170, T27, X55, T29)) → frontA_out_ga(tree(T25, tree(T105, T106, T107), T27), T29)

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

APPI_IN_GGA(.(T74, T75), T76, .(T74, X125)) → APPI_IN_GGA(T75, T76, X125)

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

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

APPI_IN_GGA(.(T74, T75), T76) → APPI_IN_GGA(T75, T76)

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:

APPI_IN_GGA(.(T74, T75), T76) → APPI_IN_GGA(T75, T76)
The graph contains the following edges 1 > 1, 2 >= 2

(20) YES

(21) Obligation:

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

U14_GAGAA(T43, T45, T44, X78, X79, frontG_out_ga(T43, T45)) → PN_IN_GAGA(T44, X78, T45, X79)
PN_IN_GAGA(T44, T60, T45, X79) → FRONTG_IN_GA(T44, T60)
FRONTG_IN_GA(tree(T57, T58, T59), X103) → PH_IN_GAGAA(T58, X101, T59, X102, X103)
PH_IN_GAGAA(T43, T45, T44, X78, X79) → U14_GAGAA(T43, T45, T44, X78, X79, frontG_in_ga(T43, T45))
PH_IN_GAGAA(T43, T45, T44, X78, X79) → FRONTG_IN_GA(T43, T45)

The TRS R consists of the following rules:

frontA_in_ga(void, []) → frontA_out_ga(void, [])
frontA_in_ga(tree(T4, void, void), .(T4, [])) → frontA_out_ga(tree(T4, void, void), .(T4, []))
frontA_in_ga(tree(T7, void, void), T9) → U1_ga(T7, T9, pB_in_aa(X18, T9))
pB_in_aa(T13, T9) → U10_aa(T13, T9, frontK_in_a(T13))
frontK_in_a([]) → frontK_out_a([])
U10_aa(T13, T9, frontK_out_a(T13)) → U11_aa(T13, T9, appF_in_ga(T13, T9))
appF_in_ga(T20, T20) → appF_out_ga(T20, T20)
U11_aa(T13, T9, appF_out_ga(T13, T9)) → pB_out_aa(T13, T9)
U1_ga(T7, T9, pB_out_aa(X18, T9)) → frontA_out_ga(tree(T7, void, void), T9)
frontA_in_ga(tree(T25, void, T27), T29) → U2_ga(T25, T27, T29, pC_in_gaa(T27, X55, T29))
pC_in_gaa(T27, T30, T29) → U12_gaa(T27, T30, T29, frontL_in_ga(T27, T30))
frontL_in_ga(void, []) → frontL_out_ga(void, [])
frontL_in_ga(tree(T35, void, void), .(T35, [])) → frontL_out_ga(tree(T35, void, void), .(T35, []))
frontL_in_ga(tree(T42, T43, T44), X79) → U8_ga(T42, T43, T44, X79, pH_in_gagaa(T43, X77, T44, X78, X79))
pH_in_gagaa(T43, T45, T44, X78, X79) → U14_gagaa(T43, T45, T44, X78, X79, frontG_in_ga(T43, T45))
frontG_in_ga(void, []) → frontG_out_ga(void, [])
frontG_in_ga(tree(T50, void, void), .(T50, [])) → frontG_out_ga(tree(T50, void, void), .(T50, []))
frontG_in_ga(tree(T57, T58, T59), X103) → U5_ga(T57, T58, T59, X103, pH_in_gagaa(T58, X101, T59, X102, X103))
U5_ga(T57, T58, T59, X103, pH_out_gagaa(T58, X101, T59, X102, X103)) → frontG_out_ga(tree(T57, T58, T59), X103)
U14_gagaa(T43, T45, T44, X78, X79, frontG_out_ga(T43, T45)) → U15_gagaa(T43, T45, T44, X78, X79, pN_in_gaga(T44, X78, T45, X79))
pN_in_gaga(T44, T60, T45, X79) → U16_gaga(T44, T60, T45, X79, frontG_in_ga(T44, T60))
U16_gaga(T44, T60, T45, X79, frontG_out_ga(T44, T60)) → U17_gaga(T44, T60, T45, X79, appI_in_gga(T45, T60, X79))
appI_in_gga([], T67, T67) → appI_out_gga([], T67, T67)
appI_in_gga(.(T74, T75), T76, .(T74, X125)) → U6_gga(T74, T75, T76, X125, appI_in_gga(T75, T76, X125))
U6_gga(T74, T75, T76, X125, appI_out_gga(T75, T76, X125)) → appI_out_gga(.(T74, T75), T76, .(T74, X125))
U17_gaga(T44, T60, T45, X79, appI_out_gga(T45, T60, X79)) → pN_out_gaga(T44, T60, T45, X79)
U15_gagaa(T43, T45, T44, X78, X79, pN_out_gaga(T44, X78, T45, X79)) → pH_out_gagaa(T43, T45, T44, X78, X79)
U8_ga(T42, T43, T44, X79, pH_out_gagaa(T43, X77, T44, X78, X79)) → frontL_out_ga(tree(T42, T43, T44), X79)
U12_gaa(T27, T30, T29, frontL_out_ga(T27, T30)) → U13_gaa(T27, T30, T29, appF_in_ga(T30, T29))
U13_gaa(T27, T30, T29, appF_out_ga(T30, T29)) → pC_out_gaa(T27, T30, T29)
U2_ga(T25, T27, T29, pC_out_gaa(T27, X55, T29)) → frontA_out_ga(tree(T25, void, T27), T29)
frontA_in_ga(tree(T25, tree(T85, void, void), T27), T29) → U3_ga(T25, T85, T27, T29, pD_in_gaga(T27, X55, T85, T29))
pD_in_gaga(T27, T86, T85, T29) → U18_gaga(T27, T86, T85, T29, frontG_in_ga(T27, T86))
U18_gaga(T27, T86, T85, T29, frontG_out_ga(T27, T86)) → U19_gaga(T27, T86, T85, T29, appM_in_gga(T85, T86, T29))
appM_in_gga(T93, T94, .(T93, T96)) → U9_gga(T93, T94, T96, appF_in_ga(T94, T96))
U9_gga(T93, T94, T96, appF_out_ga(T94, T96)) → appM_out_gga(T93, T94, .(T93, T96))
U19_gaga(T27, T86, T85, T29, appM_out_gga(T85, T86, T29)) → pD_out_gaga(T27, T86, T85, T29)
U3_ga(T25, T85, T27, T29, pD_out_gaga(T27, X55, T85, T29)) → frontA_out_ga(tree(T25, tree(T85, void, void), T27), T29)
frontA_in_ga(tree(T25, tree(T105, T106, T107), T27), T29) → U4_ga(T25, T105, T106, T107, T27, T29, pE_in_gagaagaa(T106, X168, T107, X169, X170, T27, X55, T29))
pE_in_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29) → U20_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29, frontG_in_ga(T106, T108))
U20_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29, frontG_out_ga(T106, T108)) → U21_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29, pO_in_gagagaa(T107, X169, T108, X170, T27, X55, T29))
pO_in_gagagaa(T107, T109, T108, X170, T27, X55, T29) → U22_gagagaa(T107, T109, T108, X170, T27, X55, T29, frontG_in_ga(T107, T109))
U22_gagagaa(T107, T109, T108, X170, T27, X55, T29, frontG_out_ga(T107, T109)) → U23_gagagaa(T107, T109, T108, X170, T27, X55, T29, pP_in_ggagaa(T108, T109, X170, T27, X55, T29))
pP_in_ggagaa(T108, T109, T112, T27, X55, T29) → U24_ggagaa(T108, T109, T112, T27, X55, T29, appI_in_gga(T108, T109, T112))
U24_ggagaa(T108, T109, T112, T27, X55, T29, appI_out_gga(T108, T109, T112)) → U25_ggagaa(T108, T109, T112, T27, X55, T29, pQ_in_gaga(T27, X55, T112, T29))
pQ_in_gaga(T27, T115, T112, T29) → U26_gaga(T27, T115, T112, T29, frontG_in_ga(T27, T115))
U26_gaga(T27, T115, T112, T29, frontG_out_ga(T27, T115)) → U27_gaga(T27, T115, T112, T29, appJ_in_gga(T112, T115, T29))
appJ_in_gga([], T122, T122) → appJ_out_gga([], T122, T122)
appJ_in_gga(.(T131, T132), T133, .(T131, T135)) → U7_gga(T131, T132, T133, T135, appJ_in_gga(T132, T133, T135))
U7_gga(T131, T132, T133, T135, appJ_out_gga(T132, T133, T135)) → appJ_out_gga(.(T131, T132), T133, .(T131, T135))
U27_gaga(T27, T115, T112, T29, appJ_out_gga(T112, T115, T29)) → pQ_out_gaga(T27, T115, T112, T29)
U25_ggagaa(T108, T109, T112, T27, X55, T29, pQ_out_gaga(T27, X55, T112, T29)) → pP_out_ggagaa(T108, T109, T112, T27, X55, T29)
U23_gagagaa(T107, T109, T108, X170, T27, X55, T29, pP_out_ggagaa(T108, T109, X170, T27, X55, T29)) → pO_out_gagagaa(T107, T109, T108, X170, T27, X55, T29)
U21_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29, pO_out_gagagaa(T107, X169, T108, X170, T27, X55, T29)) → pE_out_gagaagaa(T106, T108, T107, X169, X170, T27, X55, T29)
U4_ga(T25, T105, T106, T107, T27, T29, pE_out_gagaagaa(T106, X168, T107, X169, X170, T27, X55, T29)) → frontA_out_ga(tree(T25, tree(T105, T106, T107), T27), T29)

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

U14_GAGAA(T43, T45, T44, X78, X79, frontG_out_ga(T43, T45)) → PN_IN_GAGA(T44, X78, T45, X79)
PN_IN_GAGA(T44, T60, T45, X79) → FRONTG_IN_GA(T44, T60)
FRONTG_IN_GA(tree(T57, T58, T59), X103) → PH_IN_GAGAA(T58, X101, T59, X102, X103)
PH_IN_GAGAA(T43, T45, T44, X78, X79) → U14_GAGAA(T43, T45, T44, X78, X79, frontG_in_ga(T43, T45))
PH_IN_GAGAA(T43, T45, T44, X78, X79) → FRONTG_IN_GA(T43, T45)

The TRS R consists of the following rules:

frontG_in_ga(void, []) → frontG_out_ga(void, [])
frontG_in_ga(tree(T50, void, void), .(T50, [])) → frontG_out_ga(tree(T50, void, void), .(T50, []))
frontG_in_ga(tree(T57, T58, T59), X103) → U5_ga(T57, T58, T59, X103, pH_in_gagaa(T58, X101, T59, X102, X103))
U5_ga(T57, T58, T59, X103, pH_out_gagaa(T58, X101, T59, X102, X103)) → frontG_out_ga(tree(T57, T58, T59), X103)
pH_in_gagaa(T43, T45, T44, X78, X79) → U14_gagaa(T43, T45, T44, X78, X79, frontG_in_ga(T43, T45))
U14_gagaa(T43, T45, T44, X78, X79, frontG_out_ga(T43, T45)) → U15_gagaa(T43, T45, T44, X78, X79, pN_in_gaga(T44, X78, T45, X79))
U15_gagaa(T43, T45, T44, X78, X79, pN_out_gaga(T44, X78, T45, X79)) → pH_out_gagaa(T43, T45, T44, X78, X79)
pN_in_gaga(T44, T60, T45, X79) → U16_gaga(T44, T60, T45, X79, frontG_in_ga(T44, T60))
U16_gaga(T44, T60, T45, X79, frontG_out_ga(T44, T60)) → U17_gaga(T44, T60, T45, X79, appI_in_gga(T45, T60, X79))
U17_gaga(T44, T60, T45, X79, appI_out_gga(T45, T60, X79)) → pN_out_gaga(T44, T60, T45, X79)
appI_in_gga([], T67, T67) → appI_out_gga([], T67, T67)
appI_in_gga(.(T74, T75), T76, .(T74, X125)) → U6_gga(T74, T75, T76, X125, appI_in_gga(T75, T76, X125))
U6_gga(T74, T75, T76, X125, appI_out_gga(T75, T76, X125)) → appI_out_gga(.(T74, T75), T76, .(T74, X125))

The argument filtering Pi contains the following mapping:
void = void
tree(x1, x2, x3) = tree(x1, x2, x3)
pH_in_gagaa(x1, x2, x3, x4, x5) = pH_in_gagaa(x1, x3)
U14_gagaa(x1, x2, x3, x4, x5, x6) = U14_gagaa(x1, x3, x6)
frontG_in_ga(x1, x2) = frontG_in_ga(x1)
frontG_out_ga(x1, x2) = frontG_out_ga(x1, x2)
U5_ga(x1, x2, x3, x4, x5) = U5_ga(x1, x2, x3, x5)
pH_out_gagaa(x1, x2, x3, x4, x5) = pH_out_gagaa(x1, x2, x3, x4, x5)
U15_gagaa(x1, x2, x3, x4, x5, x6) = U15_gagaa(x1, x2, x3, x6)
pN_in_gaga(x1, x2, x3, x4) = pN_in_gaga(x1, x3)
U16_gaga(x1, x2, x3, x4, x5) = U16_gaga(x1, x3, x5)
U17_gaga(x1, x2, x3, x4, x5) = U17_gaga(x1, x2, x3, x5)
appI_in_gga(x1, x2, x3) = appI_in_gga(x1, x2)
[] = []
appI_out_gga(x1, x2, x3) = appI_out_gga(x1, x2, x3)
.(x1, x2) = .(x1, x2)
U6_gga(x1, x2, x3, x4, x5) = U6_gga(x1, x2, x3, x5)
pN_out_gaga(x1, x2, x3, x4) = pN_out_gaga(x1, x2, x3, x4)
PH_IN_GAGAA(x1, x2, x3, x4, x5) = PH_IN_GAGAA(x1, x3)
U14_GAGAA(x1, x2, x3, x4, x5, x6) = U14_GAGAA(x1, x3, x6)
FRONTG_IN_GA(x1, x2) = FRONTG_IN_GA(x1)
PN_IN_GAGA(x1, x2, x3, x4) = PN_IN_GAGA(x1, x3)

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:

U14_GAGAA(T43, T44, frontG_out_ga(T43, T45)) → PN_IN_GAGA(T44, T45)
PN_IN_GAGA(T44, T45) → FRONTG_IN_GA(T44)
FRONTG_IN_GA(tree(T57, T58, T59)) → PH_IN_GAGAA(T58, T59)
PH_IN_GAGAA(T43, T44) → U14_GAGAA(T43, T44, frontG_in_ga(T43))
PH_IN_GAGAA(T43, T44) → FRONTG_IN_GA(T43)

The TRS R consists of the following rules:

frontG_in_ga(void) → frontG_out_ga(void, [])
frontG_in_ga(tree(T50, void, void)) → frontG_out_ga(tree(T50, void, void), .(T50, []))
frontG_in_ga(tree(T57, T58, T59)) → U5_ga(T57, T58, T59, pH_in_gagaa(T58, T59))
U5_ga(T57, T58, T59, pH_out_gagaa(T58, X101, T59, X102, X103)) → frontG_out_ga(tree(T57, T58, T59), X103)
pH_in_gagaa(T43, T44) → U14_gagaa(T43, T44, frontG_in_ga(T43))
U14_gagaa(T43, T44, frontG_out_ga(T43, T45)) → U15_gagaa(T43, T45, T44, pN_in_gaga(T44, T45))
U15_gagaa(T43, T45, T44, pN_out_gaga(T44, X78, T45, X79)) → pH_out_gagaa(T43, T45, T44, X78, X79)
pN_in_gaga(T44, T45) → U16_gaga(T44, T45, frontG_in_ga(T44))
U16_gaga(T44, T45, frontG_out_ga(T44, T60)) → U17_gaga(T44, T60, T45, appI_in_gga(T45, T60))
U17_gaga(T44, T60, T45, appI_out_gga(T45, T60, X79)) → pN_out_gaga(T44, T60, T45, X79)
appI_in_gga([], T67) → appI_out_gga([], T67, T67)
appI_in_gga(.(T74, T75), T76) → U6_gga(T74, T75, T76, appI_in_gga(T75, T76))
U6_gga(T74, T75, T76, appI_out_gga(T75, T76, X125)) → appI_out_gga(.(T74, T75), T76, .(T74, X125))

The set Q consists of the following terms:

frontG_in_ga(x0)
U5_ga(x0, x1, x2, x3)
pH_in_gagaa(x0, x1)
U14_gagaa(x0, x1, x2)
U15_gagaa(x0, x1, x2, x3)
pN_in_gaga(x0, x1)
U16_gaga(x0, x1, x2)
U17_gaga(x0, x1, x2, x3)
appI_in_gga(x0, x1)
U6_gga(x0, x1, x2, x3)

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:

PN_IN_GAGA(T44, T45) → FRONTG_IN_GA(T44)
The graph contains the following edges 1 >= 1
PH_IN_GAGAA(T43, T44) → U14_GAGAA(T43, T44, frontG_in_ga(T43))
The graph contains the following edges 1 >= 1, 2 >= 2
FRONTG_IN_GA(tree(T57, T58, T59)) → PH_IN_GAGAA(T58, T59)
The graph contains the following edges 1 > 1, 1 > 2
U14_GAGAA(T43, T44, frontG_out_ga(T43, T45)) → PN_IN_GAGA(T44, T45)
The graph contains the following edges 2 >= 1, 3 > 2
PH_IN_GAGAA(T43, T44) → FRONTG_IN_GA(T43)
The graph contains the following edges 1 >= 1

(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