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

(0) Obligation:

Clauses:

merge(X, [], X).
merge([], X, X).
merge(.(A, X), .(B, Y), .(A, Z)) :- ','(le(A, B), merge(X, .(B, Y), Z)).
merge(.(A, X), .(B, Y), .(B, Z)) :- ','(gt(A, B), merge(.(A, X), Y, Z)).
gt(s(X), s(Y)) :- gt(X, Y).
gt(s(X), zero).
le(s(X), s(Y)) :- le(X, Y).
le(zero, s(Y)).
le(zero, zero).

Query: merge(g,g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: merge(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: merge(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | merge(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | merge(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | merge(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: true | merge(T5, [], T3), SCOPE: 1, CLAUSE: 1 | merge(T5, [], T3), SCOPE: 1, CLAUSE: 2 | merge(T5, [], T3), SCOPE: 1, CLAUSE: 3\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: merge(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | merge(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | merge(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground\nX2 is free\nmerge(T1, T2, T3) !=? merge(X2, [], X2)", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: merge(T5, [], T3), SCOPE: 1, CLAUSE: 1 | merge(T5, [], T3), SCOPE: 1, CLAUSE: 2 | merge(T5, [], T3), SCOPE: 1, CLAUSE: 3\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: true | merge([], [], T3), SCOPE: 1, CLAUSE: 2 | merge([], [], T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: merge(T5, [], T3), SCOPE: 1, CLAUSE: 2 | merge(T5, [], T3), SCOPE: 1, CLAUSE: 3\n\nT5 is ground\nX4 is free\nmerge(T5, [], T3) !=? merge([], X4, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: merge([], [], T3), SCOPE: 1, CLAUSE: 2 | merge([], [], T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: merge([], [], T3), SCOPE: 1, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: merge(T5, [], T3), SCOPE: 1, CLAUSE: 3\n\nT5 is ground\nX4 is free\nmerge(T5, [], T3) !=? merge([], X4, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: true | merge([], T11, T3), SCOPE: 1, CLAUSE: 2 | merge([], T11, T3), SCOPE: 1, CLAUSE: 3\n\nT11 is ground\nX2 is free\nmerge([], T11, T3) !=? merge(X2, [], X2)", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: merge(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | merge(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground\nX2 is free\nX26 is free\nmerge(T1, T2, T3) !=? merge(X2, [], X2)\nmerge(T1, T2, T3) !=? merge([], X26, X26)", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: merge([], T11, T3), SCOPE: 1, CLAUSE: 2 | merge([], T11, T3), SCOPE: 1, CLAUSE: 3\n\nT11 is ground\nX2 is free\nmerge([], T11, T3) !=? merge(X2, [], X2)", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: merge([], T11, T3), SCOPE: 1, CLAUSE: 3\n\nT11 is ground\nX2 is free\nmerge([], T11, T3) !=? merge(X2, [], X2)", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(le(T17, T19), merge(T18, .(T19, T20), T22)) | merge(.(T17, T18), .(T19, T20), T3), SCOPE: 1, CLAUSE: 3\n\nT17 is ground\nT18 is ground\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: merge(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground\nX2 is free\nX26 is free\nX42 is free\nX43 is free\nX44 is free\nX45 is free\nX46 is free\nmerge(T1, T2, T3) !=? merge(X2, [], X2)\nmerge(T1, T2, T3) !=? merge([], X26, X26)\nmerge(T1, T2, T3) !=? merge(.(X42, X43), .(X44, X45), .(X42, X46))", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(le(T17, T19), merge(T18, .(T19, T20), T22)), SCOPE: 2, CLAUSE: 6 | ','(le(T17, T19), merge(T18, .(T19, T20), T22)), SCOPE: 2, CLAUSE: 7 | ','(le(T17, T19), merge(T18, .(T19, T20), T22)), SCOPE: 2, CLAUSE: 8 | ?_2 | merge(.(T17, T18), .(T19, T20), T3), SCOPE: 1, CLAUSE: 3\n\nT17 is ground\nT18 is ground\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(le(T17, T19), merge(T18, .(T19, T20), T22)), SCOPE: 2, CLAUSE: 6\n\nT17 is ground\nT18 is ground\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ','(le(T17, T19), merge(T18, .(T19, T20), T22)), SCOPE: 2, CLAUSE: 7 | ','(le(T17, T19), merge(T18, .(T19, T20), T22)), SCOPE: 2, CLAUSE: 8 | ?_2 | merge(.(T17, T18), .(T19, T20), T3), SCOPE: 1, CLAUSE: 3\n\nT17 is ground\nT18 is ground\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="B: ','(le(T31, T32), merge(T18, .(s(T32), T20), T22))\n\nT18 is ground\nT20 is ground\nT31 is ground\nT32 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="E: le(T31, T32)\n\nT31 is ground\nT32 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: merge(T18, .(s(T32), T20), T22)\n\nT18 is ground\nT20 is ground\nT32 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: le(T31, T32), SCOPE: 3, CLAUSE: 6 | le(T31, T32), SCOPE: 3, CLAUSE: 7 | le(T31, T32), SCOPE: 3, CLAUSE: 8\n\nT31 is ground\nT32 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: le(T31, T32), SCOPE: 3, CLAUSE: 6\n\nT31 is ground\nT32 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: le(T31, T32), SCOPE: 3, CLAUSE: 7 | le(T31, T32), SCOPE: 3, CLAUSE: 8\n\nT31 is ground\nT32 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: le(T45, T46)\n\nT45 is ground\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: le(T31, T32), SCOPE: 3, CLAUSE: 7\n\nT31 is ground\nT32 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: le(T31, T32), SCOPE: 3, CLAUSE: 8\n\nT31 is ground\nT32 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: ','(le(T17, T19), merge(T18, .(T19, T20), T22)), SCOPE: 2, CLAUSE: 7\n\nT17 is ground\nT18 is ground\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="142: ','(le(T17, T19), merge(T18, .(T19, T20), T22)), SCOPE: 2, CLAUSE: 8 | ?_2 | merge(.(T17, T18), .(T19, T20), T3), SCOPE: 1, CLAUSE: 3\n\nT17 is ground\nT18 is ground\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: merge(T18, .(s(T60), T20), T22)\n\nT18 is ground\nT20 is ground\nT60 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: ','(le(T17, T19), merge(T18, .(T19, T20), T22)), SCOPE: 2, CLAUSE: 8\n\nT17 is ground\nT18 is ground\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: ?_2 | merge(.(T17, T18), .(T19, T20), T3), SCOPE: 1, CLAUSE: 3\n\nT17 is ground\nT18 is ground\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: merge(T18, .(zero, T20), T22)\n\nT18 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
150 [label="150: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: merge(.(T17, T18), .(T19, T20), T3), SCOPE: 1, CLAUSE: 3\n\nT17 is ground\nT18 is ground\nT19 is ground\nT20 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="C: ','(gt(T75, T77), merge(.(T75, T76), T78, T80))\n\nT75 is ground\nT76 is ground\nT77 is ground\nT78 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
160 [label="160: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="F: gt(T75, T77)\n\nT75 is ground\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: merge(.(T75, T76), T78, T80)\n\nT75 is ground\nT76 is ground\nT78 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: gt(T75, T77), SCOPE: 4, CLAUSE: 4 | gt(T75, T77), SCOPE: 4, CLAUSE: 5\n\nT75 is ground\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: gt(T75, T77), SCOPE: 4, CLAUSE: 4\n\nT75 is ground\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: gt(T75, T77), SCOPE: 4, CLAUSE: 5\n\nT75 is ground\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: gt(T93, T94)\n\nT93 is ground\nT94 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: ','(gt(T109, T111), merge(.(T109, T110), T112, T114))\n\nT109 is ground\nT110 is ground\nT111 is ground\nT112 is ground\nX42 is free\nX43 is free\nX44 is free\nX45 is free\nX46 is free\nmerge(.(T109, T110), .(T111, T112), T3) !=? merge(.(X42, X43), .(X44, X45), .(X42, X46))", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: ','(gt(T109, T111), merge(.(T109, T110), T112, T114)), SCOPE: 5, CLAUSE: 4 | ','(gt(T109, T111), merge(.(T109, T110), T112, T114)), SCOPE: 5, CLAUSE: 5\n\nT109 is ground\nT110 is ground\nT111 is ground\nT112 is ground\nX42 is free\nX43 is free\nX44 is free\nX45 is free\nX46 is free\nmerge(.(T109, T110), .(T111, T112), T3) !=? merge(.(X42, X43), .(X44, X45), .(X42, X46))", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: ','(gt(T109, T111), merge(.(T109, T110), T112, T114)), SCOPE: 5, CLAUSE: 4\n\nT109 is ground\nT110 is ground\nT111 is ground\nT112 is ground\nX42 is free\nX43 is free\nX44 is free\nX45 is free\nX46 is free\nmerge(.(T109, T110), .(T111, T112), T3) !=? merge(.(X42, X43), .(X44, X45), .(X42, X46))", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: ','(gt(T109, T111), merge(.(T109, T110), T112, T114)), SCOPE: 5, CLAUSE: 5\n\nT109 is ground\nT110 is ground\nT111 is ground\nT112 is ground\nX42 is free\nX43 is free\nX44 is free\nX45 is free\nX46 is free\nmerge(.(T109, T110), .(T111, T112), T3) !=? merge(.(X42, X43), .(X44, X45), .(X42, X46))", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="D: ','(gt(T123, T124), merge(.(s(T123), T110), T112, T114))\n\nT110 is ground\nT112 is ground\nT123 is ground\nT124 is ground\nX42 is free\nX43 is free\nX44 is free\nX45 is free\nX46 is free\nmerge(.(s(T123), T110), .(s(T124), T112), T3) !=? merge(.(X42, X43), .(X44, X45), .(X42, X46))", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: gt(T123, T124)\n\nT110 is ground\nT112 is ground\nT123 is ground\nT124 is ground\nX42 is free\nX43 is free\nX44 is free\nX45 is free\nX46 is free\nmerge(.(s(T123), T110), .(s(T124), T112), T3) !=? merge(.(X42, X43), .(X44, X45), .(X42, X46))", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: merge(.(s(T123), T110), T112, T114)\n\nT110 is ground\nT112 is ground\nT123 is ground\nT124 is ground\nX42 is free\nX43 is free\nX44 is free\nX45 is free\nX46 is free\nmerge(.(s(T123), T110), .(s(T124), T112), T3) !=? merge(.(X42, X43), .(X44, X45), .(X42, X46))", fontsize=16, style=filled, fillcolor=lightyellow];
184 [label="184: merge(.(s(T135), T110), T112, T114)\n\nT110 is ground\nT112 is ground\nT135 is ground\nX42 is free\nX43 is free\nX44 is free\nX45 is free\nX46 is free\nmerge(.(s(T135), T110), .(zero, T112), T3) !=? merge(.(X42, X43), .(X44, X45), .(X42, X46))", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 186 [arrowhead = none ];
186 -> 4;

187 [label="EVAL with clause\nmerge(X2, [], X2).\nand substitutionT1 -> T5,\nX2 -> T5,\nT2 -> [],\nT3 -> T5", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 187 [arrowhead = none ];
187 -> 10;

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

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

190 [label="EVAL with clause\nmerge([], X26, X26).\nand substitutionT1 -> [],\nT2 -> T11,\nX26 -> T11,\nT3 -> T11", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 190 [arrowhead = none ];
190 -> 40;

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

192 [label="EVAL with clause\nmerge([], X4, X4).\nand substitutionT5 -> [],\nX4 -> [],\nT3 -> []", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 192 [arrowhead = none ];
192 -> 20;

193 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 193 [arrowhead = none ];
193 -> 23;

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

195 [label="BACKTRACK\nfor clause: merge(.(A, X), .(B, Y), .(A, Z)) :- ','(le(A, B), merge(X, .(B, Y), Z))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
23 -> 195 [arrowhead = none ];
195 -> 34;

196 [label="BACKTRACK\nfor clause: merge(.(A, X), .(B, Y), .(A, Z)) :- ','(le(A, B), merge(X, .(B, Y), Z))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 196 [arrowhead = none ];
196 -> 27;

197 [label="BACKTRACK\nfor clause: merge(.(A, X), .(B, Y), .(B, Z)) :- ','(gt(A, B), merge(.(A, X), Y, Z))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 197 [arrowhead = none ];
197 -> 32;

198 [label="BACKTRACK\nfor clause: merge(.(A, X), .(B, Y), .(B, Z)) :- ','(gt(A, B), merge(.(A, X), Y, Z))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
34 -> 198 [arrowhead = none ];
198 -> 36;

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

200 [label="EVAL with clause\nmerge(.(X42, X43), .(X44, X45), .(X42, X46)) :- ','(le(X42, X44), merge(X43, .(X44, X45), X46)).\nand substitutionX42 -> T17,\nX43 -> T18,\nT1 -> .(T17, T18),\nX44 -> T19,\nX45 -> T20,\nT2 -> .(T19, T20),\nX46 -> T22,\nT3 -> .(T17, T22),\nT21 -> T22", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 200 [arrowhead = none ];
200 -> 55;

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

202 [label="BACKTRACK\nfor clause: merge(.(A, X), .(B, Y), .(A, Z)) :- ','(le(A, B), merge(X, .(B, Y), Z))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
45 -> 202 [arrowhead = none ];
202 -> 47;

203 [label="BACKTRACK\nfor clause: merge(.(A, X), .(B, Y), .(B, Z)) :- ','(gt(A, B), merge(.(A, X), Y, Z))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
47 -> 203 [arrowhead = none ];
203 -> 48;

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

205 [label="EVAL with clause\nmerge(.(X130, X131), .(X132, X133), .(X132, X134)) :- ','(gt(X130, X132), merge(.(X130, X131), X133, X134)).\nand substitutionX130 -> T109,\nX131 -> T110,\nT1 -> .(T109, T110),\nX132 -> T111,\nX133 -> T112,\nT2 -> .(T111, T112),\nX134 -> T114,\nT3 -> .(T111, T114),\nT113 -> T114", fontsize=14, style = filled, fillcolor = lightblue];
57 -> 205 [arrowhead = none ];
205 -> 175;

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

207 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
59 -> 207 [arrowhead = none ];
207 -> 61;

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

209 [label="EVAL with clause\nle(s(X55), s(X56)) :- le(X55, X56).\nand substitutionX55 -> T31,\nT17 -> s(T31),\nX56 -> T32,\nT19 -> s(T32)", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 209 [arrowhead = none ];
209 -> 73;

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

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

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

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

214 [label="SPLIT 2\nnew knowledge:\nT31 is ground\nT32 is ground", fontsize=14, style = filled, fillcolor = violet];
73 -> 214 [arrowhead = none ];
214 -> 80;

215 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
79 -> 215 [arrowhead = none ];
215 -> 101;

216 [label="INSTANCE with matching:\nT1 -> T18\nT2 -> .(s(T32), T20)\nT3 -> T22", fontsize=14, style = filled, fillcolor = lightgrey];
80 -> 216 [arrowhead = none , style=dashed];
216 -> 3[style=dashed];

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

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

219 [label="EVAL with clause\nle(s(X69), s(X70)) :- le(X69, X70).\nand substitutionX69 -> T45,\nT31 -> s(T45),\nX70 -> T46,\nT32 -> s(T46)", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 219 [arrowhead = none ];
219 -> 110;

220 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
105 -> 220 [arrowhead = none ];
220 -> 112;

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

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

223 [label="INSTANCE with matching:\nT31 -> T45\nT32 -> T46", fontsize=14, style = filled, fillcolor = lightgrey];
110 -> 223 [arrowhead = none , style=dashed];
223 -> 79[style=dashed];

224 [label="EVAL with clause\nle(zero, s(X77)).\nand substitutionT31 -> zero,\nX77 -> T53,\nT32 -> s(T53)", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 224 [arrowhead = none ];
224 -> 118;

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

226 [label="EVAL with clause\nle(zero, zero).\nand substitutionT31 -> zero,\nT32 -> zero", fontsize=14, style = filled, fillcolor = lightblue];
116 -> 226 [arrowhead = none ];
226 -> 137;

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

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

229 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
137 -> 229 [arrowhead = none ];
229 -> 139;

230 [label="EVAL with clause\nle(zero, s(X84)).\nand substitutionT17 -> zero,\nX84 -> T60,\nT19 -> s(T60)", fontsize=14, style = filled, fillcolor = lightblue];
140 -> 230 [arrowhead = none ];
230 -> 145;

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

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

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

234 [label="INSTANCE with matching:\nT1 -> T18\nT2 -> .(s(T60), T20)\nT3 -> T22", fontsize=14, style = filled, fillcolor = lightgrey];
145 -> 234 [arrowhead = none , style=dashed];
234 -> 3[style=dashed];

235 [label="EVAL with clause\nle(zero, zero).\nand substitutionT17 -> zero,\nT19 -> zero", fontsize=14, style = filled, fillcolor = lightblue];
147 -> 235 [arrowhead = none ];
235 -> 149;

236 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
147 -> 236 [arrowhead = none ];
236 -> 150;

237 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
148 -> 237 [arrowhead = none ];
237 -> 156;

238 [label="INSTANCE with matching:\nT1 -> T18\nT2 -> .(zero, T20)\nT3 -> T22", fontsize=14, style = filled, fillcolor = lightgrey];
149 -> 238 [arrowhead = none , style=dashed];
238 -> 3[style=dashed];

239 [label="EVAL with clause\nmerge(.(X99, X100), .(X101, X102), .(X101, X103)) :- ','(gt(X99, X101), merge(.(X99, X100), X102, X103)).\nand substitutionT17 -> T75,\nX99 -> T75,\nT18 -> T76,\nX100 -> T76,\nT19 -> T77,\nX101 -> T77,\nT20 -> T78,\nX102 -> T78,\nX103 -> T80,\nT3 -> .(T77, T80),\nT79 -> T80", fontsize=14, style = filled, fillcolor = lightblue];
156 -> 239 [arrowhead = none ];
239 -> 159;

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

241 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
159 -> 241 [arrowhead = none ];
241 -> 164;

242 [label="SPLIT 2\nnew knowledge:\nT75 is ground\nT77 is ground", fontsize=14, style = filled, fillcolor = violet];
159 -> 242 [arrowhead = none ];
242 -> 166;

243 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
164 -> 243 [arrowhead = none ];
243 -> 167;

244 [label="INSTANCE with matching:\nT1 -> .(T75, T76)\nT2 -> T78\nT3 -> T80", fontsize=14, style = filled, fillcolor = lightgrey];
166 -> 244 [arrowhead = none , style=dashed];
244 -> 3[style=dashed];

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

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

247 [label="EVAL with clause\ngt(s(X116), s(X117)) :- gt(X116, X117).\nand substitutionX116 -> T93,\nT75 -> s(T93),\nX117 -> T94,\nT77 -> s(T94)", fontsize=14, style = filled, fillcolor = lightblue];
168 -> 247 [arrowhead = none ];
247 -> 170;

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

249 [label="EVAL with clause\ngt(s(X122), zero).\nand substitutionX122 -> T99,\nT75 -> s(T99),\nT77 -> zero", fontsize=14, style = filled, fillcolor = lightblue];
169 -> 249 [arrowhead = none ];
249 -> 172;

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

251 [label="INSTANCE with matching:\nT75 -> T93\nT77 -> T94", fontsize=14, style = filled, fillcolor = lightgrey];
170 -> 251 [arrowhead = none , style=dashed];
251 -> 164[style=dashed];

252 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
172 -> 252 [arrowhead = none ];
252 -> 174;

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

254 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
177 -> 254 [arrowhead = none ];
254 -> 178;

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

256 [label="EVAL with clause\ngt(s(X143), s(X144)) :- gt(X143, X144).\nand substitutionX143 -> T123,\nT109 -> s(T123),\nX144 -> T124,\nT111 -> s(T124)", fontsize=14, style = filled, fillcolor = lightblue];
178 -> 256 [arrowhead = none ];
256 -> 180;

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

258 [label="EVAL with clause\ngt(s(X153), zero).\nand substitutionX153 -> T135,\nT109 -> s(T135),\nT111 -> zero", fontsize=14, style = filled, fillcolor = lightblue];
179 -> 258 [arrowhead = none ];
258 -> 184;

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

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

261 [label="SPLIT 2\nnew knowledge:\nT123 is ground\nT124 is ground", fontsize=14, style = filled, fillcolor = violet];
180 -> 261 [arrowhead = none ];
261 -> 183;

262 [label="INSTANCE with matching:\nT75 -> T123\nT77 -> T124", fontsize=14, style = filled, fillcolor = lightgrey];
182 -> 262 [arrowhead = none , style=dashed];
262 -> 164[style=dashed];

263 [label="INSTANCE with matching:\nT1 -> .(s(T123), T110)\nT2 -> T112\nT3 -> T114", fontsize=14, style = filled, fillcolor = lightgrey];
183 -> 263 [arrowhead = none , style=dashed];
263 -> 3[style=dashed];

264 [label="INSTANCE with matching:\nT1 -> .(s(T135), T110)\nT2 -> T112\nT3 -> T114", fontsize=14, style = filled, fillcolor = lightgrey];
184 -> 264 [arrowhead = none , style=dashed];
264 -> 3[style=dashed];

}

(2) Obligation:

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

mergeA_in_gga(T5, [], T5) → mergeA_out_gga(T5, [], T5)
mergeA_in_gga([], [], []) → mergeA_out_gga([], [], [])
mergeA_in_gga([], T11, T11) → mergeA_out_gga([], T11, T11)
mergeA_in_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22)) → U1_gga(T31, T18, T32, T20, T22, pB_in_gggga(T31, T32, T18, T20, T22))
pB_in_gggga(T31, T32, T18, T20, T22) → U9_gggga(T31, T32, T18, T20, T22, leE_in_gg(T31, T32))
leE_in_gg(s(T45), s(T46)) → U7_gg(T45, T46, leE_in_gg(T45, T46))
leE_in_gg(zero, s(T53)) → leE_out_gg(zero, s(T53))
leE_in_gg(zero, zero) → leE_out_gg(zero, zero)
U7_gg(T45, T46, leE_out_gg(T45, T46)) → leE_out_gg(s(T45), s(T46))
U9_gggga(T31, T32, T18, T20, T22, leE_out_gg(T31, T32)) → U10_gggga(T31, T32, T18, T20, T22, mergeA_in_gga(T18, .(s(T32), T20), T22))
mergeA_in_gga(.(zero, T18), .(s(T60), T20), .(zero, T22)) → U2_gga(T18, T60, T20, T22, mergeA_in_gga(T18, .(s(T60), T20), T22))
mergeA_in_gga(.(zero, T18), .(zero, T20), .(zero, T22)) → U3_gga(T18, T20, T22, mergeA_in_gga(T18, .(zero, T20), T22))
mergeA_in_gga(.(T75, T76), .(T77, T78), .(T77, T80)) → U4_gga(T75, T76, T77, T78, T80, pC_in_gggga(T75, T77, T76, T78, T80))
pC_in_gggga(T75, T77, T76, T78, T80) → U11_gggga(T75, T77, T76, T78, T80, gtF_in_gg(T75, T77))
gtF_in_gg(s(T93), s(T94)) → U8_gg(T93, T94, gtF_in_gg(T93, T94))
gtF_in_gg(s(T99), zero) → gtF_out_gg(s(T99), zero)
U8_gg(T93, T94, gtF_out_gg(T93, T94)) → gtF_out_gg(s(T93), s(T94))
U11_gggga(T75, T77, T76, T78, T80, gtF_out_gg(T75, T77)) → U12_gggga(T75, T77, T76, T78, T80, mergeA_in_gga(.(T75, T76), T78, T80))
mergeA_in_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114)) → U5_gga(T123, T110, T124, T112, T114, pD_in_gggga(T123, T124, T110, T112, T114))
pD_in_gggga(T123, T124, T110, T112, T114) → U13_gggga(T123, T124, T110, T112, T114, gtF_in_gg(T123, T124))
U13_gggga(T123, T124, T110, T112, T114, gtF_out_gg(T123, T124)) → U14_gggga(T123, T124, T110, T112, T114, mergeA_in_gga(.(s(T123), T110), T112, T114))
mergeA_in_gga(.(s(T135), T110), .(zero, T112), .(zero, T114)) → U6_gga(T135, T110, T112, T114, mergeA_in_gga(.(s(T135), T110), T112, T114))
U6_gga(T135, T110, T112, T114, mergeA_out_gga(.(s(T135), T110), T112, T114)) → mergeA_out_gga(.(s(T135), T110), .(zero, T112), .(zero, T114))
U14_gggga(T123, T124, T110, T112, T114, mergeA_out_gga(.(s(T123), T110), T112, T114)) → pD_out_gggga(T123, T124, T110, T112, T114)
U5_gga(T123, T110, T124, T112, T114, pD_out_gggga(T123, T124, T110, T112, T114)) → mergeA_out_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114))
U12_gggga(T75, T77, T76, T78, T80, mergeA_out_gga(.(T75, T76), T78, T80)) → pC_out_gggga(T75, T77, T76, T78, T80)
U4_gga(T75, T76, T77, T78, T80, pC_out_gggga(T75, T77, T76, T78, T80)) → mergeA_out_gga(.(T75, T76), .(T77, T78), .(T77, T80))
U3_gga(T18, T20, T22, mergeA_out_gga(T18, .(zero, T20), T22)) → mergeA_out_gga(.(zero, T18), .(zero, T20), .(zero, T22))
U2_gga(T18, T60, T20, T22, mergeA_out_gga(T18, .(s(T60), T20), T22)) → mergeA_out_gga(.(zero, T18), .(s(T60), T20), .(zero, T22))
U10_gggga(T31, T32, T18, T20, T22, mergeA_out_gga(T18, .(s(T32), T20), T22)) → pB_out_gggga(T31, T32, T18, T20, T22)
U1_gga(T31, T18, T32, T20, T22, pB_out_gggga(T31, T32, T18, T20, T22)) → mergeA_out_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22))

The argument filtering Pi contains the following mapping:
mergeA_in_gga(x1, x2, x3)  =  mergeA_in_gga(x1, x2)
[]  =  []
mergeA_out_gga(x1, x2, x3)  =  mergeA_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3, x4, x5, x6)  =  U1_gga(x1, x2, x3, x4, x6)
pB_in_gggga(x1, x2, x3, x4, x5)  =  pB_in_gggga(x1, x2, x3, x4)
U9_gggga(x1, x2, x3, x4, x5, x6)  =  U9_gggga(x1, x2, x3, x4, x6)
leE_in_gg(x1, x2)  =  leE_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
zero  =  zero
leE_out_gg(x1, x2)  =  leE_out_gg(x1, x2)
U10_gggga(x1, x2, x3, x4, x5, x6)  =  U10_gggga(x1, x2, x3, x4, x6)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
U4_gga(x1, x2, x3, x4, x5, x6)  =  U4_gga(x1, x2, x3, x4, x6)
pC_in_gggga(x1, x2, x3, x4, x5)  =  pC_in_gggga(x1, x2, x3, x4)
U11_gggga(x1, x2, x3, x4, x5, x6)  =  U11_gggga(x1, x2, x3, x4, x6)
gtF_in_gg(x1, x2)  =  gtF_in_gg(x1, x2)
U8_gg(x1, x2, x3)  =  U8_gg(x1, x2, x3)
gtF_out_gg(x1, x2)  =  gtF_out_gg(x1, x2)
U12_gggga(x1, x2, x3, x4, x5, x6)  =  U12_gggga(x1, x2, x3, x4, x6)
U5_gga(x1, x2, x3, x4, x5, x6)  =  U5_gga(x1, x2, x3, x4, x6)
pD_in_gggga(x1, x2, x3, x4, x5)  =  pD_in_gggga(x1, x2, x3, x4)
U13_gggga(x1, x2, x3, x4, x5, x6)  =  U13_gggga(x1, x2, x3, x4, x6)
U14_gggga(x1, x2, x3, x4, x5, x6)  =  U14_gggga(x1, x2, x3, x4, x6)
U6_gga(x1, x2, x3, x4, x5)  =  U6_gga(x1, x2, x3, x5)
pD_out_gggga(x1, x2, x3, x4, x5)  =  pD_out_gggga(x1, x2, x3, x4, x5)
pC_out_gggga(x1, x2, x3, x4, x5)  =  pC_out_gggga(x1, x2, x3, x4, x5)
pB_out_gggga(x1, x2, x3, x4, x5)  =  pB_out_gggga(x1, x2, x3, x4, x5)

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

MERGEA_IN_GGA(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22)) → U1_GGA(T31, T18, T32, T20, T22, pB_in_gggga(T31, T32, T18, T20, T22))
MERGEA_IN_GGA(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22)) → PB_IN_GGGGA(T31, T32, T18, T20, T22)
PB_IN_GGGGA(T31, T32, T18, T20, T22) → U9_GGGGA(T31, T32, T18, T20, T22, leE_in_gg(T31, T32))
PB_IN_GGGGA(T31, T32, T18, T20, T22) → LEE_IN_GG(T31, T32)
LEE_IN_GG(s(T45), s(T46)) → U7_GG(T45, T46, leE_in_gg(T45, T46))
LEE_IN_GG(s(T45), s(T46)) → LEE_IN_GG(T45, T46)
U9_GGGGA(T31, T32, T18, T20, T22, leE_out_gg(T31, T32)) → U10_GGGGA(T31, T32, T18, T20, T22, mergeA_in_gga(T18, .(s(T32), T20), T22))
U9_GGGGA(T31, T32, T18, T20, T22, leE_out_gg(T31, T32)) → MERGEA_IN_GGA(T18, .(s(T32), T20), T22)
MERGEA_IN_GGA(.(zero, T18), .(s(T60), T20), .(zero, T22)) → U2_GGA(T18, T60, T20, T22, mergeA_in_gga(T18, .(s(T60), T20), T22))
MERGEA_IN_GGA(.(zero, T18), .(s(T60), T20), .(zero, T22)) → MERGEA_IN_GGA(T18, .(s(T60), T20), T22)
MERGEA_IN_GGA(.(zero, T18), .(zero, T20), .(zero, T22)) → U3_GGA(T18, T20, T22, mergeA_in_gga(T18, .(zero, T20), T22))
MERGEA_IN_GGA(.(zero, T18), .(zero, T20), .(zero, T22)) → MERGEA_IN_GGA(T18, .(zero, T20), T22)
MERGEA_IN_GGA(.(T75, T76), .(T77, T78), .(T77, T80)) → U4_GGA(T75, T76, T77, T78, T80, pC_in_gggga(T75, T77, T76, T78, T80))
MERGEA_IN_GGA(.(T75, T76), .(T77, T78), .(T77, T80)) → PC_IN_GGGGA(T75, T77, T76, T78, T80)
PC_IN_GGGGA(T75, T77, T76, T78, T80) → U11_GGGGA(T75, T77, T76, T78, T80, gtF_in_gg(T75, T77))
PC_IN_GGGGA(T75, T77, T76, T78, T80) → GTF_IN_GG(T75, T77)
GTF_IN_GG(s(T93), s(T94)) → U8_GG(T93, T94, gtF_in_gg(T93, T94))
GTF_IN_GG(s(T93), s(T94)) → GTF_IN_GG(T93, T94)
U11_GGGGA(T75, T77, T76, T78, T80, gtF_out_gg(T75, T77)) → U12_GGGGA(T75, T77, T76, T78, T80, mergeA_in_gga(.(T75, T76), T78, T80))
U11_GGGGA(T75, T77, T76, T78, T80, gtF_out_gg(T75, T77)) → MERGEA_IN_GGA(.(T75, T76), T78, T80)
MERGEA_IN_GGA(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114)) → U5_GGA(T123, T110, T124, T112, T114, pD_in_gggga(T123, T124, T110, T112, T114))
MERGEA_IN_GGA(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114)) → PD_IN_GGGGA(T123, T124, T110, T112, T114)
PD_IN_GGGGA(T123, T124, T110, T112, T114) → U13_GGGGA(T123, T124, T110, T112, T114, gtF_in_gg(T123, T124))
PD_IN_GGGGA(T123, T124, T110, T112, T114) → GTF_IN_GG(T123, T124)
U13_GGGGA(T123, T124, T110, T112, T114, gtF_out_gg(T123, T124)) → U14_GGGGA(T123, T124, T110, T112, T114, mergeA_in_gga(.(s(T123), T110), T112, T114))
U13_GGGGA(T123, T124, T110, T112, T114, gtF_out_gg(T123, T124)) → MERGEA_IN_GGA(.(s(T123), T110), T112, T114)
MERGEA_IN_GGA(.(s(T135), T110), .(zero, T112), .(zero, T114)) → U6_GGA(T135, T110, T112, T114, mergeA_in_gga(.(s(T135), T110), T112, T114))
MERGEA_IN_GGA(.(s(T135), T110), .(zero, T112), .(zero, T114)) → MERGEA_IN_GGA(.(s(T135), T110), T112, T114)

The TRS R consists of the following rules:

mergeA_in_gga(T5, [], T5) → mergeA_out_gga(T5, [], T5)
mergeA_in_gga([], [], []) → mergeA_out_gga([], [], [])
mergeA_in_gga([], T11, T11) → mergeA_out_gga([], T11, T11)
mergeA_in_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22)) → U1_gga(T31, T18, T32, T20, T22, pB_in_gggga(T31, T32, T18, T20, T22))
pB_in_gggga(T31, T32, T18, T20, T22) → U9_gggga(T31, T32, T18, T20, T22, leE_in_gg(T31, T32))
leE_in_gg(s(T45), s(T46)) → U7_gg(T45, T46, leE_in_gg(T45, T46))
leE_in_gg(zero, s(T53)) → leE_out_gg(zero, s(T53))
leE_in_gg(zero, zero) → leE_out_gg(zero, zero)
U7_gg(T45, T46, leE_out_gg(T45, T46)) → leE_out_gg(s(T45), s(T46))
U9_gggga(T31, T32, T18, T20, T22, leE_out_gg(T31, T32)) → U10_gggga(T31, T32, T18, T20, T22, mergeA_in_gga(T18, .(s(T32), T20), T22))
mergeA_in_gga(.(zero, T18), .(s(T60), T20), .(zero, T22)) → U2_gga(T18, T60, T20, T22, mergeA_in_gga(T18, .(s(T60), T20), T22))
mergeA_in_gga(.(zero, T18), .(zero, T20), .(zero, T22)) → U3_gga(T18, T20, T22, mergeA_in_gga(T18, .(zero, T20), T22))
mergeA_in_gga(.(T75, T76), .(T77, T78), .(T77, T80)) → U4_gga(T75, T76, T77, T78, T80, pC_in_gggga(T75, T77, T76, T78, T80))
pC_in_gggga(T75, T77, T76, T78, T80) → U11_gggga(T75, T77, T76, T78, T80, gtF_in_gg(T75, T77))
gtF_in_gg(s(T93), s(T94)) → U8_gg(T93, T94, gtF_in_gg(T93, T94))
gtF_in_gg(s(T99), zero) → gtF_out_gg(s(T99), zero)
U8_gg(T93, T94, gtF_out_gg(T93, T94)) → gtF_out_gg(s(T93), s(T94))
U11_gggga(T75, T77, T76, T78, T80, gtF_out_gg(T75, T77)) → U12_gggga(T75, T77, T76, T78, T80, mergeA_in_gga(.(T75, T76), T78, T80))
mergeA_in_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114)) → U5_gga(T123, T110, T124, T112, T114, pD_in_gggga(T123, T124, T110, T112, T114))
pD_in_gggga(T123, T124, T110, T112, T114) → U13_gggga(T123, T124, T110, T112, T114, gtF_in_gg(T123, T124))
U13_gggga(T123, T124, T110, T112, T114, gtF_out_gg(T123, T124)) → U14_gggga(T123, T124, T110, T112, T114, mergeA_in_gga(.(s(T123), T110), T112, T114))
mergeA_in_gga(.(s(T135), T110), .(zero, T112), .(zero, T114)) → U6_gga(T135, T110, T112, T114, mergeA_in_gga(.(s(T135), T110), T112, T114))
U6_gga(T135, T110, T112, T114, mergeA_out_gga(.(s(T135), T110), T112, T114)) → mergeA_out_gga(.(s(T135), T110), .(zero, T112), .(zero, T114))
U14_gggga(T123, T124, T110, T112, T114, mergeA_out_gga(.(s(T123), T110), T112, T114)) → pD_out_gggga(T123, T124, T110, T112, T114)
U5_gga(T123, T110, T124, T112, T114, pD_out_gggga(T123, T124, T110, T112, T114)) → mergeA_out_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114))
U12_gggga(T75, T77, T76, T78, T80, mergeA_out_gga(.(T75, T76), T78, T80)) → pC_out_gggga(T75, T77, T76, T78, T80)
U4_gga(T75, T76, T77, T78, T80, pC_out_gggga(T75, T77, T76, T78, T80)) → mergeA_out_gga(.(T75, T76), .(T77, T78), .(T77, T80))
U3_gga(T18, T20, T22, mergeA_out_gga(T18, .(zero, T20), T22)) → mergeA_out_gga(.(zero, T18), .(zero, T20), .(zero, T22))
U2_gga(T18, T60, T20, T22, mergeA_out_gga(T18, .(s(T60), T20), T22)) → mergeA_out_gga(.(zero, T18), .(s(T60), T20), .(zero, T22))
U10_gggga(T31, T32, T18, T20, T22, mergeA_out_gga(T18, .(s(T32), T20), T22)) → pB_out_gggga(T31, T32, T18, T20, T22)
U1_gga(T31, T18, T32, T20, T22, pB_out_gggga(T31, T32, T18, T20, T22)) → mergeA_out_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22))

The argument filtering Pi contains the following mapping:
mergeA_in_gga(x1, x2, x3)  =  mergeA_in_gga(x1, x2)
[]  =  []
mergeA_out_gga(x1, x2, x3)  =  mergeA_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3, x4, x5, x6)  =  U1_gga(x1, x2, x3, x4, x6)
pB_in_gggga(x1, x2, x3, x4, x5)  =  pB_in_gggga(x1, x2, x3, x4)
U9_gggga(x1, x2, x3, x4, x5, x6)  =  U9_gggga(x1, x2, x3, x4, x6)
leE_in_gg(x1, x2)  =  leE_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
zero  =  zero
leE_out_gg(x1, x2)  =  leE_out_gg(x1, x2)
U10_gggga(x1, x2, x3, x4, x5, x6)  =  U10_gggga(x1, x2, x3, x4, x6)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
U4_gga(x1, x2, x3, x4, x5, x6)  =  U4_gga(x1, x2, x3, x4, x6)
pC_in_gggga(x1, x2, x3, x4, x5)  =  pC_in_gggga(x1, x2, x3, x4)
U11_gggga(x1, x2, x3, x4, x5, x6)  =  U11_gggga(x1, x2, x3, x4, x6)
gtF_in_gg(x1, x2)  =  gtF_in_gg(x1, x2)
U8_gg(x1, x2, x3)  =  U8_gg(x1, x2, x3)
gtF_out_gg(x1, x2)  =  gtF_out_gg(x1, x2)
U12_gggga(x1, x2, x3, x4, x5, x6)  =  U12_gggga(x1, x2, x3, x4, x6)
U5_gga(x1, x2, x3, x4, x5, x6)  =  U5_gga(x1, x2, x3, x4, x6)
pD_in_gggga(x1, x2, x3, x4, x5)  =  pD_in_gggga(x1, x2, x3, x4)
U13_gggga(x1, x2, x3, x4, x5, x6)  =  U13_gggga(x1, x2, x3, x4, x6)
U14_gggga(x1, x2, x3, x4, x5, x6)  =  U14_gggga(x1, x2, x3, x4, x6)
U6_gga(x1, x2, x3, x4, x5)  =  U6_gga(x1, x2, x3, x5)
pD_out_gggga(x1, x2, x3, x4, x5)  =  pD_out_gggga(x1, x2, x3, x4, x5)
pC_out_gggga(x1, x2, x3, x4, x5)  =  pC_out_gggga(x1, x2, x3, x4, x5)
pB_out_gggga(x1, x2, x3, x4, x5)  =  pB_out_gggga(x1, x2, x3, x4, x5)
MERGEA_IN_GGA(x1, x2, x3)  =  MERGEA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4, x5, x6)  =  U1_GGA(x1, x2, x3, x4, x6)
PB_IN_GGGGA(x1, x2, x3, x4, x5)  =  PB_IN_GGGGA(x1, x2, x3, x4)
U9_GGGGA(x1, x2, x3, x4, x5, x6)  =  U9_GGGGA(x1, x2, x3, x4, x6)
LEE_IN_GG(x1, x2)  =  LEE_IN_GG(x1, x2)
U7_GG(x1, x2, x3)  =  U7_GG(x1, x2, x3)
U10_GGGGA(x1, x2, x3, x4, x5, x6)  =  U10_GGGGA(x1, x2, x3, x4, x6)
U2_GGA(x1, x2, x3, x4, x5)  =  U2_GGA(x1, x2, x3, x5)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
U4_GGA(x1, x2, x3, x4, x5, x6)  =  U4_GGA(x1, x2, x3, x4, x6)
PC_IN_GGGGA(x1, x2, x3, x4, x5)  =  PC_IN_GGGGA(x1, x2, x3, x4)
U11_GGGGA(x1, x2, x3, x4, x5, x6)  =  U11_GGGGA(x1, x2, x3, x4, x6)
GTF_IN_GG(x1, x2)  =  GTF_IN_GG(x1, x2)
U8_GG(x1, x2, x3)  =  U8_GG(x1, x2, x3)
U12_GGGGA(x1, x2, x3, x4, x5, x6)  =  U12_GGGGA(x1, x2, x3, x4, x6)
U5_GGA(x1, x2, x3, x4, x5, x6)  =  U5_GGA(x1, x2, x3, x4, x6)
PD_IN_GGGGA(x1, x2, x3, x4, x5)  =  PD_IN_GGGGA(x1, x2, x3, x4)
U13_GGGGA(x1, x2, x3, x4, x5, x6)  =  U13_GGGGA(x1, x2, x3, x4, x6)
U14_GGGGA(x1, x2, x3, x4, x5, x6)  =  U14_GGGGA(x1, x2, x3, x4, x6)
U6_GGA(x1, x2, x3, x4, x5)  =  U6_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:

MERGEA_IN_GGA(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22)) → U1_GGA(T31, T18, T32, T20, T22, pB_in_gggga(T31, T32, T18, T20, T22))
MERGEA_IN_GGA(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22)) → PB_IN_GGGGA(T31, T32, T18, T20, T22)
PB_IN_GGGGA(T31, T32, T18, T20, T22) → U9_GGGGA(T31, T32, T18, T20, T22, leE_in_gg(T31, T32))
PB_IN_GGGGA(T31, T32, T18, T20, T22) → LEE_IN_GG(T31, T32)
LEE_IN_GG(s(T45), s(T46)) → U7_GG(T45, T46, leE_in_gg(T45, T46))
LEE_IN_GG(s(T45), s(T46)) → LEE_IN_GG(T45, T46)
U9_GGGGA(T31, T32, T18, T20, T22, leE_out_gg(T31, T32)) → U10_GGGGA(T31, T32, T18, T20, T22, mergeA_in_gga(T18, .(s(T32), T20), T22))
U9_GGGGA(T31, T32, T18, T20, T22, leE_out_gg(T31, T32)) → MERGEA_IN_GGA(T18, .(s(T32), T20), T22)
MERGEA_IN_GGA(.(zero, T18), .(s(T60), T20), .(zero, T22)) → U2_GGA(T18, T60, T20, T22, mergeA_in_gga(T18, .(s(T60), T20), T22))
MERGEA_IN_GGA(.(zero, T18), .(s(T60), T20), .(zero, T22)) → MERGEA_IN_GGA(T18, .(s(T60), T20), T22)
MERGEA_IN_GGA(.(zero, T18), .(zero, T20), .(zero, T22)) → U3_GGA(T18, T20, T22, mergeA_in_gga(T18, .(zero, T20), T22))
MERGEA_IN_GGA(.(zero, T18), .(zero, T20), .(zero, T22)) → MERGEA_IN_GGA(T18, .(zero, T20), T22)
MERGEA_IN_GGA(.(T75, T76), .(T77, T78), .(T77, T80)) → U4_GGA(T75, T76, T77, T78, T80, pC_in_gggga(T75, T77, T76, T78, T80))
MERGEA_IN_GGA(.(T75, T76), .(T77, T78), .(T77, T80)) → PC_IN_GGGGA(T75, T77, T76, T78, T80)
PC_IN_GGGGA(T75, T77, T76, T78, T80) → U11_GGGGA(T75, T77, T76, T78, T80, gtF_in_gg(T75, T77))
PC_IN_GGGGA(T75, T77, T76, T78, T80) → GTF_IN_GG(T75, T77)
GTF_IN_GG(s(T93), s(T94)) → U8_GG(T93, T94, gtF_in_gg(T93, T94))
GTF_IN_GG(s(T93), s(T94)) → GTF_IN_GG(T93, T94)
U11_GGGGA(T75, T77, T76, T78, T80, gtF_out_gg(T75, T77)) → U12_GGGGA(T75, T77, T76, T78, T80, mergeA_in_gga(.(T75, T76), T78, T80))
U11_GGGGA(T75, T77, T76, T78, T80, gtF_out_gg(T75, T77)) → MERGEA_IN_GGA(.(T75, T76), T78, T80)
MERGEA_IN_GGA(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114)) → U5_GGA(T123, T110, T124, T112, T114, pD_in_gggga(T123, T124, T110, T112, T114))
MERGEA_IN_GGA(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114)) → PD_IN_GGGGA(T123, T124, T110, T112, T114)
PD_IN_GGGGA(T123, T124, T110, T112, T114) → U13_GGGGA(T123, T124, T110, T112, T114, gtF_in_gg(T123, T124))
PD_IN_GGGGA(T123, T124, T110, T112, T114) → GTF_IN_GG(T123, T124)
U13_GGGGA(T123, T124, T110, T112, T114, gtF_out_gg(T123, T124)) → U14_GGGGA(T123, T124, T110, T112, T114, mergeA_in_gga(.(s(T123), T110), T112, T114))
U13_GGGGA(T123, T124, T110, T112, T114, gtF_out_gg(T123, T124)) → MERGEA_IN_GGA(.(s(T123), T110), T112, T114)
MERGEA_IN_GGA(.(s(T135), T110), .(zero, T112), .(zero, T114)) → U6_GGA(T135, T110, T112, T114, mergeA_in_gga(.(s(T135), T110), T112, T114))
MERGEA_IN_GGA(.(s(T135), T110), .(zero, T112), .(zero, T114)) → MERGEA_IN_GGA(.(s(T135), T110), T112, T114)

The TRS R consists of the following rules:

mergeA_in_gga(T5, [], T5) → mergeA_out_gga(T5, [], T5)
mergeA_in_gga([], [], []) → mergeA_out_gga([], [], [])
mergeA_in_gga([], T11, T11) → mergeA_out_gga([], T11, T11)
mergeA_in_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22)) → U1_gga(T31, T18, T32, T20, T22, pB_in_gggga(T31, T32, T18, T20, T22))
pB_in_gggga(T31, T32, T18, T20, T22) → U9_gggga(T31, T32, T18, T20, T22, leE_in_gg(T31, T32))
leE_in_gg(s(T45), s(T46)) → U7_gg(T45, T46, leE_in_gg(T45, T46))
leE_in_gg(zero, s(T53)) → leE_out_gg(zero, s(T53))
leE_in_gg(zero, zero) → leE_out_gg(zero, zero)
U7_gg(T45, T46, leE_out_gg(T45, T46)) → leE_out_gg(s(T45), s(T46))
U9_gggga(T31, T32, T18, T20, T22, leE_out_gg(T31, T32)) → U10_gggga(T31, T32, T18, T20, T22, mergeA_in_gga(T18, .(s(T32), T20), T22))
mergeA_in_gga(.(zero, T18), .(s(T60), T20), .(zero, T22)) → U2_gga(T18, T60, T20, T22, mergeA_in_gga(T18, .(s(T60), T20), T22))
mergeA_in_gga(.(zero, T18), .(zero, T20), .(zero, T22)) → U3_gga(T18, T20, T22, mergeA_in_gga(T18, .(zero, T20), T22))
mergeA_in_gga(.(T75, T76), .(T77, T78), .(T77, T80)) → U4_gga(T75, T76, T77, T78, T80, pC_in_gggga(T75, T77, T76, T78, T80))
pC_in_gggga(T75, T77, T76, T78, T80) → U11_gggga(T75, T77, T76, T78, T80, gtF_in_gg(T75, T77))
gtF_in_gg(s(T93), s(T94)) → U8_gg(T93, T94, gtF_in_gg(T93, T94))
gtF_in_gg(s(T99), zero) → gtF_out_gg(s(T99), zero)
U8_gg(T93, T94, gtF_out_gg(T93, T94)) → gtF_out_gg(s(T93), s(T94))
U11_gggga(T75, T77, T76, T78, T80, gtF_out_gg(T75, T77)) → U12_gggga(T75, T77, T76, T78, T80, mergeA_in_gga(.(T75, T76), T78, T80))
mergeA_in_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114)) → U5_gga(T123, T110, T124, T112, T114, pD_in_gggga(T123, T124, T110, T112, T114))
pD_in_gggga(T123, T124, T110, T112, T114) → U13_gggga(T123, T124, T110, T112, T114, gtF_in_gg(T123, T124))
U13_gggga(T123, T124, T110, T112, T114, gtF_out_gg(T123, T124)) → U14_gggga(T123, T124, T110, T112, T114, mergeA_in_gga(.(s(T123), T110), T112, T114))
mergeA_in_gga(.(s(T135), T110), .(zero, T112), .(zero, T114)) → U6_gga(T135, T110, T112, T114, mergeA_in_gga(.(s(T135), T110), T112, T114))
U6_gga(T135, T110, T112, T114, mergeA_out_gga(.(s(T135), T110), T112, T114)) → mergeA_out_gga(.(s(T135), T110), .(zero, T112), .(zero, T114))
U14_gggga(T123, T124, T110, T112, T114, mergeA_out_gga(.(s(T123), T110), T112, T114)) → pD_out_gggga(T123, T124, T110, T112, T114)
U5_gga(T123, T110, T124, T112, T114, pD_out_gggga(T123, T124, T110, T112, T114)) → mergeA_out_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114))
U12_gggga(T75, T77, T76, T78, T80, mergeA_out_gga(.(T75, T76), T78, T80)) → pC_out_gggga(T75, T77, T76, T78, T80)
U4_gga(T75, T76, T77, T78, T80, pC_out_gggga(T75, T77, T76, T78, T80)) → mergeA_out_gga(.(T75, T76), .(T77, T78), .(T77, T80))
U3_gga(T18, T20, T22, mergeA_out_gga(T18, .(zero, T20), T22)) → mergeA_out_gga(.(zero, T18), .(zero, T20), .(zero, T22))
U2_gga(T18, T60, T20, T22, mergeA_out_gga(T18, .(s(T60), T20), T22)) → mergeA_out_gga(.(zero, T18), .(s(T60), T20), .(zero, T22))
U10_gggga(T31, T32, T18, T20, T22, mergeA_out_gga(T18, .(s(T32), T20), T22)) → pB_out_gggga(T31, T32, T18, T20, T22)
U1_gga(T31, T18, T32, T20, T22, pB_out_gggga(T31, T32, T18, T20, T22)) → mergeA_out_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22))

The argument filtering Pi contains the following mapping:
mergeA_in_gga(x1, x2, x3)  =  mergeA_in_gga(x1, x2)
[]  =  []
mergeA_out_gga(x1, x2, x3)  =  mergeA_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3, x4, x5, x6)  =  U1_gga(x1, x2, x3, x4, x6)
pB_in_gggga(x1, x2, x3, x4, x5)  =  pB_in_gggga(x1, x2, x3, x4)
U9_gggga(x1, x2, x3, x4, x5, x6)  =  U9_gggga(x1, x2, x3, x4, x6)
leE_in_gg(x1, x2)  =  leE_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
zero  =  zero
leE_out_gg(x1, x2)  =  leE_out_gg(x1, x2)
U10_gggga(x1, x2, x3, x4, x5, x6)  =  U10_gggga(x1, x2, x3, x4, x6)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
U4_gga(x1, x2, x3, x4, x5, x6)  =  U4_gga(x1, x2, x3, x4, x6)
pC_in_gggga(x1, x2, x3, x4, x5)  =  pC_in_gggga(x1, x2, x3, x4)
U11_gggga(x1, x2, x3, x4, x5, x6)  =  U11_gggga(x1, x2, x3, x4, x6)
gtF_in_gg(x1, x2)  =  gtF_in_gg(x1, x2)
U8_gg(x1, x2, x3)  =  U8_gg(x1, x2, x3)
gtF_out_gg(x1, x2)  =  gtF_out_gg(x1, x2)
U12_gggga(x1, x2, x3, x4, x5, x6)  =  U12_gggga(x1, x2, x3, x4, x6)
U5_gga(x1, x2, x3, x4, x5, x6)  =  U5_gga(x1, x2, x3, x4, x6)
pD_in_gggga(x1, x2, x3, x4, x5)  =  pD_in_gggga(x1, x2, x3, x4)
U13_gggga(x1, x2, x3, x4, x5, x6)  =  U13_gggga(x1, x2, x3, x4, x6)
U14_gggga(x1, x2, x3, x4, x5, x6)  =  U14_gggga(x1, x2, x3, x4, x6)
U6_gga(x1, x2, x3, x4, x5)  =  U6_gga(x1, x2, x3, x5)
pD_out_gggga(x1, x2, x3, x4, x5)  =  pD_out_gggga(x1, x2, x3, x4, x5)
pC_out_gggga(x1, x2, x3, x4, x5)  =  pC_out_gggga(x1, x2, x3, x4, x5)
pB_out_gggga(x1, x2, x3, x4, x5)  =  pB_out_gggga(x1, x2, x3, x4, x5)
MERGEA_IN_GGA(x1, x2, x3)  =  MERGEA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4, x5, x6)  =  U1_GGA(x1, x2, x3, x4, x6)
PB_IN_GGGGA(x1, x2, x3, x4, x5)  =  PB_IN_GGGGA(x1, x2, x3, x4)
U9_GGGGA(x1, x2, x3, x4, x5, x6)  =  U9_GGGGA(x1, x2, x3, x4, x6)
LEE_IN_GG(x1, x2)  =  LEE_IN_GG(x1, x2)
U7_GG(x1, x2, x3)  =  U7_GG(x1, x2, x3)
U10_GGGGA(x1, x2, x3, x4, x5, x6)  =  U10_GGGGA(x1, x2, x3, x4, x6)
U2_GGA(x1, x2, x3, x4, x5)  =  U2_GGA(x1, x2, x3, x5)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
U4_GGA(x1, x2, x3, x4, x5, x6)  =  U4_GGA(x1, x2, x3, x4, x6)
PC_IN_GGGGA(x1, x2, x3, x4, x5)  =  PC_IN_GGGGA(x1, x2, x3, x4)
U11_GGGGA(x1, x2, x3, x4, x5, x6)  =  U11_GGGGA(x1, x2, x3, x4, x6)
GTF_IN_GG(x1, x2)  =  GTF_IN_GG(x1, x2)
U8_GG(x1, x2, x3)  =  U8_GG(x1, x2, x3)
U12_GGGGA(x1, x2, x3, x4, x5, x6)  =  U12_GGGGA(x1, x2, x3, x4, x6)
U5_GGA(x1, x2, x3, x4, x5, x6)  =  U5_GGA(x1, x2, x3, x4, x6)
PD_IN_GGGGA(x1, x2, x3, x4, x5)  =  PD_IN_GGGGA(x1, x2, x3, x4)
U13_GGGGA(x1, x2, x3, x4, x5, x6)  =  U13_GGGGA(x1, x2, x3, x4, x6)
U14_GGGGA(x1, x2, x3, x4, x5, x6)  =  U14_GGGGA(x1, x2, x3, x4, x6)
U6_GGA(x1, x2, x3, x4, x5)  =  U6_GGA(x1, x2, x3, x5)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

GTF_IN_GG(s(T93), s(T94)) → GTF_IN_GG(T93, T94)

The TRS R consists of the following rules:

mergeA_in_gga(T5, [], T5) → mergeA_out_gga(T5, [], T5)
mergeA_in_gga([], [], []) → mergeA_out_gga([], [], [])
mergeA_in_gga([], T11, T11) → mergeA_out_gga([], T11, T11)
mergeA_in_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22)) → U1_gga(T31, T18, T32, T20, T22, pB_in_gggga(T31, T32, T18, T20, T22))
pB_in_gggga(T31, T32, T18, T20, T22) → U9_gggga(T31, T32, T18, T20, T22, leE_in_gg(T31, T32))
leE_in_gg(s(T45), s(T46)) → U7_gg(T45, T46, leE_in_gg(T45, T46))
leE_in_gg(zero, s(T53)) → leE_out_gg(zero, s(T53))
leE_in_gg(zero, zero) → leE_out_gg(zero, zero)
U7_gg(T45, T46, leE_out_gg(T45, T46)) → leE_out_gg(s(T45), s(T46))
U9_gggga(T31, T32, T18, T20, T22, leE_out_gg(T31, T32)) → U10_gggga(T31, T32, T18, T20, T22, mergeA_in_gga(T18, .(s(T32), T20), T22))
mergeA_in_gga(.(zero, T18), .(s(T60), T20), .(zero, T22)) → U2_gga(T18, T60, T20, T22, mergeA_in_gga(T18, .(s(T60), T20), T22))
mergeA_in_gga(.(zero, T18), .(zero, T20), .(zero, T22)) → U3_gga(T18, T20, T22, mergeA_in_gga(T18, .(zero, T20), T22))
mergeA_in_gga(.(T75, T76), .(T77, T78), .(T77, T80)) → U4_gga(T75, T76, T77, T78, T80, pC_in_gggga(T75, T77, T76, T78, T80))
pC_in_gggga(T75, T77, T76, T78, T80) → U11_gggga(T75, T77, T76, T78, T80, gtF_in_gg(T75, T77))
gtF_in_gg(s(T93), s(T94)) → U8_gg(T93, T94, gtF_in_gg(T93, T94))
gtF_in_gg(s(T99), zero) → gtF_out_gg(s(T99), zero)
U8_gg(T93, T94, gtF_out_gg(T93, T94)) → gtF_out_gg(s(T93), s(T94))
U11_gggga(T75, T77, T76, T78, T80, gtF_out_gg(T75, T77)) → U12_gggga(T75, T77, T76, T78, T80, mergeA_in_gga(.(T75, T76), T78, T80))
mergeA_in_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114)) → U5_gga(T123, T110, T124, T112, T114, pD_in_gggga(T123, T124, T110, T112, T114))
pD_in_gggga(T123, T124, T110, T112, T114) → U13_gggga(T123, T124, T110, T112, T114, gtF_in_gg(T123, T124))
U13_gggga(T123, T124, T110, T112, T114, gtF_out_gg(T123, T124)) → U14_gggga(T123, T124, T110, T112, T114, mergeA_in_gga(.(s(T123), T110), T112, T114))
mergeA_in_gga(.(s(T135), T110), .(zero, T112), .(zero, T114)) → U6_gga(T135, T110, T112, T114, mergeA_in_gga(.(s(T135), T110), T112, T114))
U6_gga(T135, T110, T112, T114, mergeA_out_gga(.(s(T135), T110), T112, T114)) → mergeA_out_gga(.(s(T135), T110), .(zero, T112), .(zero, T114))
U14_gggga(T123, T124, T110, T112, T114, mergeA_out_gga(.(s(T123), T110), T112, T114)) → pD_out_gggga(T123, T124, T110, T112, T114)
U5_gga(T123, T110, T124, T112, T114, pD_out_gggga(T123, T124, T110, T112, T114)) → mergeA_out_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114))
U12_gggga(T75, T77, T76, T78, T80, mergeA_out_gga(.(T75, T76), T78, T80)) → pC_out_gggga(T75, T77, T76, T78, T80)
U4_gga(T75, T76, T77, T78, T80, pC_out_gggga(T75, T77, T76, T78, T80)) → mergeA_out_gga(.(T75, T76), .(T77, T78), .(T77, T80))
U3_gga(T18, T20, T22, mergeA_out_gga(T18, .(zero, T20), T22)) → mergeA_out_gga(.(zero, T18), .(zero, T20), .(zero, T22))
U2_gga(T18, T60, T20, T22, mergeA_out_gga(T18, .(s(T60), T20), T22)) → mergeA_out_gga(.(zero, T18), .(s(T60), T20), .(zero, T22))
U10_gggga(T31, T32, T18, T20, T22, mergeA_out_gga(T18, .(s(T32), T20), T22)) → pB_out_gggga(T31, T32, T18, T20, T22)
U1_gga(T31, T18, T32, T20, T22, pB_out_gggga(T31, T32, T18, T20, T22)) → mergeA_out_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22))

The argument filtering Pi contains the following mapping:
mergeA_in_gga(x1, x2, x3)  =  mergeA_in_gga(x1, x2)
[]  =  []
mergeA_out_gga(x1, x2, x3)  =  mergeA_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3, x4, x5, x6)  =  U1_gga(x1, x2, x3, x4, x6)
pB_in_gggga(x1, x2, x3, x4, x5)  =  pB_in_gggga(x1, x2, x3, x4)
U9_gggga(x1, x2, x3, x4, x5, x6)  =  U9_gggga(x1, x2, x3, x4, x6)
leE_in_gg(x1, x2)  =  leE_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
zero  =  zero
leE_out_gg(x1, x2)  =  leE_out_gg(x1, x2)
U10_gggga(x1, x2, x3, x4, x5, x6)  =  U10_gggga(x1, x2, x3, x4, x6)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
U4_gga(x1, x2, x3, x4, x5, x6)  =  U4_gga(x1, x2, x3, x4, x6)
pC_in_gggga(x1, x2, x3, x4, x5)  =  pC_in_gggga(x1, x2, x3, x4)
U11_gggga(x1, x2, x3, x4, x5, x6)  =  U11_gggga(x1, x2, x3, x4, x6)
gtF_in_gg(x1, x2)  =  gtF_in_gg(x1, x2)
U8_gg(x1, x2, x3)  =  U8_gg(x1, x2, x3)
gtF_out_gg(x1, x2)  =  gtF_out_gg(x1, x2)
U12_gggga(x1, x2, x3, x4, x5, x6)  =  U12_gggga(x1, x2, x3, x4, x6)
U5_gga(x1, x2, x3, x4, x5, x6)  =  U5_gga(x1, x2, x3, x4, x6)
pD_in_gggga(x1, x2, x3, x4, x5)  =  pD_in_gggga(x1, x2, x3, x4)
U13_gggga(x1, x2, x3, x4, x5, x6)  =  U13_gggga(x1, x2, x3, x4, x6)
U14_gggga(x1, x2, x3, x4, x5, x6)  =  U14_gggga(x1, x2, x3, x4, x6)
U6_gga(x1, x2, x3, x4, x5)  =  U6_gga(x1, x2, x3, x5)
pD_out_gggga(x1, x2, x3, x4, x5)  =  pD_out_gggga(x1, x2, x3, x4, x5)
pC_out_gggga(x1, x2, x3, x4, x5)  =  pC_out_gggga(x1, x2, x3, x4, x5)
pB_out_gggga(x1, x2, x3, x4, x5)  =  pB_out_gggga(x1, x2, x3, x4, x5)
GTF_IN_GG(x1, x2)  =  GTF_IN_GG(x1, x2)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

GTF_IN_GG(s(T93), s(T94)) → GTF_IN_GG(T93, T94)

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

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

GTF_IN_GG(s(T93), s(T94)) → GTF_IN_GG(T93, T94)

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:

• GTF_IN_GG(s(T93), s(T94)) → GTF_IN_GG(T93, T94)
  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:

LEE_IN_GG(s(T45), s(T46)) → LEE_IN_GG(T45, T46)

The TRS R consists of the following rules:

mergeA_in_gga(T5, [], T5) → mergeA_out_gga(T5, [], T5)
mergeA_in_gga([], [], []) → mergeA_out_gga([], [], [])
mergeA_in_gga([], T11, T11) → mergeA_out_gga([], T11, T11)
mergeA_in_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22)) → U1_gga(T31, T18, T32, T20, T22, pB_in_gggga(T31, T32, T18, T20, T22))
pB_in_gggga(T31, T32, T18, T20, T22) → U9_gggga(T31, T32, T18, T20, T22, leE_in_gg(T31, T32))
leE_in_gg(s(T45), s(T46)) → U7_gg(T45, T46, leE_in_gg(T45, T46))
leE_in_gg(zero, s(T53)) → leE_out_gg(zero, s(T53))
leE_in_gg(zero, zero) → leE_out_gg(zero, zero)
U7_gg(T45, T46, leE_out_gg(T45, T46)) → leE_out_gg(s(T45), s(T46))
U9_gggga(T31, T32, T18, T20, T22, leE_out_gg(T31, T32)) → U10_gggga(T31, T32, T18, T20, T22, mergeA_in_gga(T18, .(s(T32), T20), T22))
mergeA_in_gga(.(zero, T18), .(s(T60), T20), .(zero, T22)) → U2_gga(T18, T60, T20, T22, mergeA_in_gga(T18, .(s(T60), T20), T22))
mergeA_in_gga(.(zero, T18), .(zero, T20), .(zero, T22)) → U3_gga(T18, T20, T22, mergeA_in_gga(T18, .(zero, T20), T22))
mergeA_in_gga(.(T75, T76), .(T77, T78), .(T77, T80)) → U4_gga(T75, T76, T77, T78, T80, pC_in_gggga(T75, T77, T76, T78, T80))
pC_in_gggga(T75, T77, T76, T78, T80) → U11_gggga(T75, T77, T76, T78, T80, gtF_in_gg(T75, T77))
gtF_in_gg(s(T93), s(T94)) → U8_gg(T93, T94, gtF_in_gg(T93, T94))
gtF_in_gg(s(T99), zero) → gtF_out_gg(s(T99), zero)
U8_gg(T93, T94, gtF_out_gg(T93, T94)) → gtF_out_gg(s(T93), s(T94))
U11_gggga(T75, T77, T76, T78, T80, gtF_out_gg(T75, T77)) → U12_gggga(T75, T77, T76, T78, T80, mergeA_in_gga(.(T75, T76), T78, T80))
mergeA_in_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114)) → U5_gga(T123, T110, T124, T112, T114, pD_in_gggga(T123, T124, T110, T112, T114))
pD_in_gggga(T123, T124, T110, T112, T114) → U13_gggga(T123, T124, T110, T112, T114, gtF_in_gg(T123, T124))
U13_gggga(T123, T124, T110, T112, T114, gtF_out_gg(T123, T124)) → U14_gggga(T123, T124, T110, T112, T114, mergeA_in_gga(.(s(T123), T110), T112, T114))
mergeA_in_gga(.(s(T135), T110), .(zero, T112), .(zero, T114)) → U6_gga(T135, T110, T112, T114, mergeA_in_gga(.(s(T135), T110), T112, T114))
U6_gga(T135, T110, T112, T114, mergeA_out_gga(.(s(T135), T110), T112, T114)) → mergeA_out_gga(.(s(T135), T110), .(zero, T112), .(zero, T114))
U14_gggga(T123, T124, T110, T112, T114, mergeA_out_gga(.(s(T123), T110), T112, T114)) → pD_out_gggga(T123, T124, T110, T112, T114)
U5_gga(T123, T110, T124, T112, T114, pD_out_gggga(T123, T124, T110, T112, T114)) → mergeA_out_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114))
U12_gggga(T75, T77, T76, T78, T80, mergeA_out_gga(.(T75, T76), T78, T80)) → pC_out_gggga(T75, T77, T76, T78, T80)
U4_gga(T75, T76, T77, T78, T80, pC_out_gggga(T75, T77, T76, T78, T80)) → mergeA_out_gga(.(T75, T76), .(T77, T78), .(T77, T80))
U3_gga(T18, T20, T22, mergeA_out_gga(T18, .(zero, T20), T22)) → mergeA_out_gga(.(zero, T18), .(zero, T20), .(zero, T22))
U2_gga(T18, T60, T20, T22, mergeA_out_gga(T18, .(s(T60), T20), T22)) → mergeA_out_gga(.(zero, T18), .(s(T60), T20), .(zero, T22))
U10_gggga(T31, T32, T18, T20, T22, mergeA_out_gga(T18, .(s(T32), T20), T22)) → pB_out_gggga(T31, T32, T18, T20, T22)
U1_gga(T31, T18, T32, T20, T22, pB_out_gggga(T31, T32, T18, T20, T22)) → mergeA_out_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22))

The argument filtering Pi contains the following mapping:
mergeA_in_gga(x1, x2, x3)  =  mergeA_in_gga(x1, x2)
[]  =  []
mergeA_out_gga(x1, x2, x3)  =  mergeA_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3, x4, x5, x6)  =  U1_gga(x1, x2, x3, x4, x6)
pB_in_gggga(x1, x2, x3, x4, x5)  =  pB_in_gggga(x1, x2, x3, x4)
U9_gggga(x1, x2, x3, x4, x5, x6)  =  U9_gggga(x1, x2, x3, x4, x6)
leE_in_gg(x1, x2)  =  leE_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
zero  =  zero
leE_out_gg(x1, x2)  =  leE_out_gg(x1, x2)
U10_gggga(x1, x2, x3, x4, x5, x6)  =  U10_gggga(x1, x2, x3, x4, x6)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
U4_gga(x1, x2, x3, x4, x5, x6)  =  U4_gga(x1, x2, x3, x4, x6)
pC_in_gggga(x1, x2, x3, x4, x5)  =  pC_in_gggga(x1, x2, x3, x4)
U11_gggga(x1, x2, x3, x4, x5, x6)  =  U11_gggga(x1, x2, x3, x4, x6)
gtF_in_gg(x1, x2)  =  gtF_in_gg(x1, x2)
U8_gg(x1, x2, x3)  =  U8_gg(x1, x2, x3)
gtF_out_gg(x1, x2)  =  gtF_out_gg(x1, x2)
U12_gggga(x1, x2, x3, x4, x5, x6)  =  U12_gggga(x1, x2, x3, x4, x6)
U5_gga(x1, x2, x3, x4, x5, x6)  =  U5_gga(x1, x2, x3, x4, x6)
pD_in_gggga(x1, x2, x3, x4, x5)  =  pD_in_gggga(x1, x2, x3, x4)
U13_gggga(x1, x2, x3, x4, x5, x6)  =  U13_gggga(x1, x2, x3, x4, x6)
U14_gggga(x1, x2, x3, x4, x5, x6)  =  U14_gggga(x1, x2, x3, x4, x6)
U6_gga(x1, x2, x3, x4, x5)  =  U6_gga(x1, x2, x3, x5)
pD_out_gggga(x1, x2, x3, x4, x5)  =  pD_out_gggga(x1, x2, x3, x4, x5)
pC_out_gggga(x1, x2, x3, x4, x5)  =  pC_out_gggga(x1, x2, x3, x4, x5)
pB_out_gggga(x1, x2, x3, x4, x5)  =  pB_out_gggga(x1, x2, x3, x4, x5)
LEE_IN_GG(x1, x2)  =  LEE_IN_GG(x1, x2)

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

LEE_IN_GG(s(T45), s(T46)) → LEE_IN_GG(T45, T46)

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

(17) PiDPToQDPProof (EQUIVALENT transformation)

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

(18) Obligation:

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

LEE_IN_GG(s(T45), s(T46)) → LEE_IN_GG(T45, T46)

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:

• LEE_IN_GG(s(T45), s(T46)) → LEE_IN_GG(T45, T46)
  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:

MERGEA_IN_GGA(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22)) → PB_IN_GGGGA(T31, T32, T18, T20, T22)
PB_IN_GGGGA(T31, T32, T18, T20, T22) → U9_GGGGA(T31, T32, T18, T20, T22, leE_in_gg(T31, T32))
U9_GGGGA(T31, T32, T18, T20, T22, leE_out_gg(T31, T32)) → MERGEA_IN_GGA(T18, .(s(T32), T20), T22)
MERGEA_IN_GGA(.(zero, T18), .(s(T60), T20), .(zero, T22)) → MERGEA_IN_GGA(T18, .(s(T60), T20), T22)
MERGEA_IN_GGA(.(T75, T76), .(T77, T78), .(T77, T80)) → PC_IN_GGGGA(T75, T77, T76, T78, T80)
PC_IN_GGGGA(T75, T77, T76, T78, T80) → U11_GGGGA(T75, T77, T76, T78, T80, gtF_in_gg(T75, T77))
U11_GGGGA(T75, T77, T76, T78, T80, gtF_out_gg(T75, T77)) → MERGEA_IN_GGA(.(T75, T76), T78, T80)
MERGEA_IN_GGA(.(zero, T18), .(zero, T20), .(zero, T22)) → MERGEA_IN_GGA(T18, .(zero, T20), T22)
MERGEA_IN_GGA(.(s(T135), T110), .(zero, T112), .(zero, T114)) → MERGEA_IN_GGA(.(s(T135), T110), T112, T114)
MERGEA_IN_GGA(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114)) → PD_IN_GGGGA(T123, T124, T110, T112, T114)
PD_IN_GGGGA(T123, T124, T110, T112, T114) → U13_GGGGA(T123, T124, T110, T112, T114, gtF_in_gg(T123, T124))
U13_GGGGA(T123, T124, T110, T112, T114, gtF_out_gg(T123, T124)) → MERGEA_IN_GGA(.(s(T123), T110), T112, T114)

The TRS R consists of the following rules:

mergeA_in_gga(T5, [], T5) → mergeA_out_gga(T5, [], T5)
mergeA_in_gga([], [], []) → mergeA_out_gga([], [], [])
mergeA_in_gga([], T11, T11) → mergeA_out_gga([], T11, T11)
mergeA_in_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22)) → U1_gga(T31, T18, T32, T20, T22, pB_in_gggga(T31, T32, T18, T20, T22))
pB_in_gggga(T31, T32, T18, T20, T22) → U9_gggga(T31, T32, T18, T20, T22, leE_in_gg(T31, T32))
leE_in_gg(s(T45), s(T46)) → U7_gg(T45, T46, leE_in_gg(T45, T46))
leE_in_gg(zero, s(T53)) → leE_out_gg(zero, s(T53))
leE_in_gg(zero, zero) → leE_out_gg(zero, zero)
U7_gg(T45, T46, leE_out_gg(T45, T46)) → leE_out_gg(s(T45), s(T46))
U9_gggga(T31, T32, T18, T20, T22, leE_out_gg(T31, T32)) → U10_gggga(T31, T32, T18, T20, T22, mergeA_in_gga(T18, .(s(T32), T20), T22))
mergeA_in_gga(.(zero, T18), .(s(T60), T20), .(zero, T22)) → U2_gga(T18, T60, T20, T22, mergeA_in_gga(T18, .(s(T60), T20), T22))
mergeA_in_gga(.(zero, T18), .(zero, T20), .(zero, T22)) → U3_gga(T18, T20, T22, mergeA_in_gga(T18, .(zero, T20), T22))
mergeA_in_gga(.(T75, T76), .(T77, T78), .(T77, T80)) → U4_gga(T75, T76, T77, T78, T80, pC_in_gggga(T75, T77, T76, T78, T80))
pC_in_gggga(T75, T77, T76, T78, T80) → U11_gggga(T75, T77, T76, T78, T80, gtF_in_gg(T75, T77))
gtF_in_gg(s(T93), s(T94)) → U8_gg(T93, T94, gtF_in_gg(T93, T94))
gtF_in_gg(s(T99), zero) → gtF_out_gg(s(T99), zero)
U8_gg(T93, T94, gtF_out_gg(T93, T94)) → gtF_out_gg(s(T93), s(T94))
U11_gggga(T75, T77, T76, T78, T80, gtF_out_gg(T75, T77)) → U12_gggga(T75, T77, T76, T78, T80, mergeA_in_gga(.(T75, T76), T78, T80))
mergeA_in_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114)) → U5_gga(T123, T110, T124, T112, T114, pD_in_gggga(T123, T124, T110, T112, T114))
pD_in_gggga(T123, T124, T110, T112, T114) → U13_gggga(T123, T124, T110, T112, T114, gtF_in_gg(T123, T124))
U13_gggga(T123, T124, T110, T112, T114, gtF_out_gg(T123, T124)) → U14_gggga(T123, T124, T110, T112, T114, mergeA_in_gga(.(s(T123), T110), T112, T114))
mergeA_in_gga(.(s(T135), T110), .(zero, T112), .(zero, T114)) → U6_gga(T135, T110, T112, T114, mergeA_in_gga(.(s(T135), T110), T112, T114))
U6_gga(T135, T110, T112, T114, mergeA_out_gga(.(s(T135), T110), T112, T114)) → mergeA_out_gga(.(s(T135), T110), .(zero, T112), .(zero, T114))
U14_gggga(T123, T124, T110, T112, T114, mergeA_out_gga(.(s(T123), T110), T112, T114)) → pD_out_gggga(T123, T124, T110, T112, T114)
U5_gga(T123, T110, T124, T112, T114, pD_out_gggga(T123, T124, T110, T112, T114)) → mergeA_out_gga(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114))
U12_gggga(T75, T77, T76, T78, T80, mergeA_out_gga(.(T75, T76), T78, T80)) → pC_out_gggga(T75, T77, T76, T78, T80)
U4_gga(T75, T76, T77, T78, T80, pC_out_gggga(T75, T77, T76, T78, T80)) → mergeA_out_gga(.(T75, T76), .(T77, T78), .(T77, T80))
U3_gga(T18, T20, T22, mergeA_out_gga(T18, .(zero, T20), T22)) → mergeA_out_gga(.(zero, T18), .(zero, T20), .(zero, T22))
U2_gga(T18, T60, T20, T22, mergeA_out_gga(T18, .(s(T60), T20), T22)) → mergeA_out_gga(.(zero, T18), .(s(T60), T20), .(zero, T22))
U10_gggga(T31, T32, T18, T20, T22, mergeA_out_gga(T18, .(s(T32), T20), T22)) → pB_out_gggga(T31, T32, T18, T20, T22)
U1_gga(T31, T18, T32, T20, T22, pB_out_gggga(T31, T32, T18, T20, T22)) → mergeA_out_gga(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22))

The argument filtering Pi contains the following mapping:
mergeA_in_gga(x1, x2, x3)  =  mergeA_in_gga(x1, x2)
[]  =  []
mergeA_out_gga(x1, x2, x3)  =  mergeA_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3, x4, x5, x6)  =  U1_gga(x1, x2, x3, x4, x6)
pB_in_gggga(x1, x2, x3, x4, x5)  =  pB_in_gggga(x1, x2, x3, x4)
U9_gggga(x1, x2, x3, x4, x5, x6)  =  U9_gggga(x1, x2, x3, x4, x6)
leE_in_gg(x1, x2)  =  leE_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
zero  =  zero
leE_out_gg(x1, x2)  =  leE_out_gg(x1, x2)
U10_gggga(x1, x2, x3, x4, x5, x6)  =  U10_gggga(x1, x2, x3, x4, x6)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x2, x4)
U4_gga(x1, x2, x3, x4, x5, x6)  =  U4_gga(x1, x2, x3, x4, x6)
pC_in_gggga(x1, x2, x3, x4, x5)  =  pC_in_gggga(x1, x2, x3, x4)
U11_gggga(x1, x2, x3, x4, x5, x6)  =  U11_gggga(x1, x2, x3, x4, x6)
gtF_in_gg(x1, x2)  =  gtF_in_gg(x1, x2)
U8_gg(x1, x2, x3)  =  U8_gg(x1, x2, x3)
gtF_out_gg(x1, x2)  =  gtF_out_gg(x1, x2)
U12_gggga(x1, x2, x3, x4, x5, x6)  =  U12_gggga(x1, x2, x3, x4, x6)
U5_gga(x1, x2, x3, x4, x5, x6)  =  U5_gga(x1, x2, x3, x4, x6)
pD_in_gggga(x1, x2, x3, x4, x5)  =  pD_in_gggga(x1, x2, x3, x4)
U13_gggga(x1, x2, x3, x4, x5, x6)  =  U13_gggga(x1, x2, x3, x4, x6)
U14_gggga(x1, x2, x3, x4, x5, x6)  =  U14_gggga(x1, x2, x3, x4, x6)
U6_gga(x1, x2, x3, x4, x5)  =  U6_gga(x1, x2, x3, x5)
pD_out_gggga(x1, x2, x3, x4, x5)  =  pD_out_gggga(x1, x2, x3, x4, x5)
pC_out_gggga(x1, x2, x3, x4, x5)  =  pC_out_gggga(x1, x2, x3, x4, x5)
pB_out_gggga(x1, x2, x3, x4, x5)  =  pB_out_gggga(x1, x2, x3, x4, x5)
MERGEA_IN_GGA(x1, x2, x3)  =  MERGEA_IN_GGA(x1, x2)
PB_IN_GGGGA(x1, x2, x3, x4, x5)  =  PB_IN_GGGGA(x1, x2, x3, x4)
U9_GGGGA(x1, x2, x3, x4, x5, x6)  =  U9_GGGGA(x1, x2, x3, x4, x6)
PC_IN_GGGGA(x1, x2, x3, x4, x5)  =  PC_IN_GGGGA(x1, x2, x3, x4)
U11_GGGGA(x1, x2, x3, x4, x5, x6)  =  U11_GGGGA(x1, x2, x3, x4, x6)
PD_IN_GGGGA(x1, x2, x3, x4, x5)  =  PD_IN_GGGGA(x1, x2, x3, x4)
U13_GGGGA(x1, x2, x3, x4, x5, x6)  =  U13_GGGGA(x1, x2, x3, x4, x6)

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

MERGEA_IN_GGA(.(s(T31), T18), .(s(T32), T20), .(s(T31), T22)) → PB_IN_GGGGA(T31, T32, T18, T20, T22)
PB_IN_GGGGA(T31, T32, T18, T20, T22) → U9_GGGGA(T31, T32, T18, T20, T22, leE_in_gg(T31, T32))
U9_GGGGA(T31, T32, T18, T20, T22, leE_out_gg(T31, T32)) → MERGEA_IN_GGA(T18, .(s(T32), T20), T22)
MERGEA_IN_GGA(.(zero, T18), .(s(T60), T20), .(zero, T22)) → MERGEA_IN_GGA(T18, .(s(T60), T20), T22)
MERGEA_IN_GGA(.(T75, T76), .(T77, T78), .(T77, T80)) → PC_IN_GGGGA(T75, T77, T76, T78, T80)
PC_IN_GGGGA(T75, T77, T76, T78, T80) → U11_GGGGA(T75, T77, T76, T78, T80, gtF_in_gg(T75, T77))
U11_GGGGA(T75, T77, T76, T78, T80, gtF_out_gg(T75, T77)) → MERGEA_IN_GGA(.(T75, T76), T78, T80)
MERGEA_IN_GGA(.(zero, T18), .(zero, T20), .(zero, T22)) → MERGEA_IN_GGA(T18, .(zero, T20), T22)
MERGEA_IN_GGA(.(s(T135), T110), .(zero, T112), .(zero, T114)) → MERGEA_IN_GGA(.(s(T135), T110), T112, T114)
MERGEA_IN_GGA(.(s(T123), T110), .(s(T124), T112), .(s(T124), T114)) → PD_IN_GGGGA(T123, T124, T110, T112, T114)
PD_IN_GGGGA(T123, T124, T110, T112, T114) → U13_GGGGA(T123, T124, T110, T112, T114, gtF_in_gg(T123, T124))
U13_GGGGA(T123, T124, T110, T112, T114, gtF_out_gg(T123, T124)) → MERGEA_IN_GGA(.(s(T123), T110), T112, T114)

The TRS R consists of the following rules:

leE_in_gg(s(T45), s(T46)) → U7_gg(T45, T46, leE_in_gg(T45, T46))
leE_in_gg(zero, s(T53)) → leE_out_gg(zero, s(T53))
leE_in_gg(zero, zero) → leE_out_gg(zero, zero)
gtF_in_gg(s(T93), s(T94)) → U8_gg(T93, T94, gtF_in_gg(T93, T94))
gtF_in_gg(s(T99), zero) → gtF_out_gg(s(T99), zero)
U7_gg(T45, T46, leE_out_gg(T45, T46)) → leE_out_gg(s(T45), s(T46))
U8_gg(T93, T94, gtF_out_gg(T93, T94)) → gtF_out_gg(s(T93), s(T94))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
s(x1)  =  s(x1)
leE_in_gg(x1, x2)  =  leE_in_gg(x1, x2)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
zero  =  zero
leE_out_gg(x1, x2)  =  leE_out_gg(x1, x2)
gtF_in_gg(x1, x2)  =  gtF_in_gg(x1, x2)
U8_gg(x1, x2, x3)  =  U8_gg(x1, x2, x3)
gtF_out_gg(x1, x2)  =  gtF_out_gg(x1, x2)
MERGEA_IN_GGA(x1, x2, x3)  =  MERGEA_IN_GGA(x1, x2)
PB_IN_GGGGA(x1, x2, x3, x4, x5)  =  PB_IN_GGGGA(x1, x2, x3, x4)
U9_GGGGA(x1, x2, x3, x4, x5, x6)  =  U9_GGGGA(x1, x2, x3, x4, x6)
PC_IN_GGGGA(x1, x2, x3, x4, x5)  =  PC_IN_GGGGA(x1, x2, x3, x4)
U11_GGGGA(x1, x2, x3, x4, x5, x6)  =  U11_GGGGA(x1, x2, x3, x4, x6)
PD_IN_GGGGA(x1, x2, x3, x4, x5)  =  PD_IN_GGGGA(x1, x2, x3, x4)
U13_GGGGA(x1, x2, x3, x4, x5, x6)  =  U13_GGGGA(x1, x2, x3, x4, x6)

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:

MERGEA_IN_GGA(.(s(T31), T18), .(s(T32), T20)) → PB_IN_GGGGA(T31, T32, T18, T20)
PB_IN_GGGGA(T31, T32, T18, T20) → U9_GGGGA(T31, T32, T18, T20, leE_in_gg(T31, T32))
U9_GGGGA(T31, T32, T18, T20, leE_out_gg(T31, T32)) → MERGEA_IN_GGA(T18, .(s(T32), T20))
MERGEA_IN_GGA(.(zero, T18), .(s(T60), T20)) → MERGEA_IN_GGA(T18, .(s(T60), T20))
MERGEA_IN_GGA(.(T75, T76), .(T77, T78)) → PC_IN_GGGGA(T75, T77, T76, T78)
PC_IN_GGGGA(T75, T77, T76, T78) → U11_GGGGA(T75, T77, T76, T78, gtF_in_gg(T75, T77))
U11_GGGGA(T75, T77, T76, T78, gtF_out_gg(T75, T77)) → MERGEA_IN_GGA(.(T75, T76), T78)
MERGEA_IN_GGA(.(zero, T18), .(zero, T20)) → MERGEA_IN_GGA(T18, .(zero, T20))
MERGEA_IN_GGA(.(s(T135), T110), .(zero, T112)) → MERGEA_IN_GGA(.(s(T135), T110), T112)
MERGEA_IN_GGA(.(s(T123), T110), .(s(T124), T112)) → PD_IN_GGGGA(T123, T124, T110, T112)
PD_IN_GGGGA(T123, T124, T110, T112) → U13_GGGGA(T123, T124, T110, T112, gtF_in_gg(T123, T124))
U13_GGGGA(T123, T124, T110, T112, gtF_out_gg(T123, T124)) → MERGEA_IN_GGA(.(s(T123), T110), T112)

The TRS R consists of the following rules:

leE_in_gg(s(T45), s(T46)) → U7_gg(T45, T46, leE_in_gg(T45, T46))
leE_in_gg(zero, s(T53)) → leE_out_gg(zero, s(T53))
leE_in_gg(zero, zero) → leE_out_gg(zero, zero)
gtF_in_gg(s(T93), s(T94)) → U8_gg(T93, T94, gtF_in_gg(T93, T94))
gtF_in_gg(s(T99), zero) → gtF_out_gg(s(T99), zero)
U7_gg(T45, T46, leE_out_gg(T45, T46)) → leE_out_gg(s(T45), s(T46))
U8_gg(T93, T94, gtF_out_gg(T93, T94)) → gtF_out_gg(s(T93), s(T94))

The set Q consists of the following terms:

leE_in_gg(x0, x1)
gtF_in_gg(x0, x1)
U7_gg(x0, x1, x2)
U8_gg(x0, x1, x2)

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

(26) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

MERGEA_IN_GGA(.(T75, T76), .(T77, T78)) → PC_IN_GGGGA(T75, T77, T76, T78)
MERGEA_IN_GGA(.(s(T135), T110), .(zero, T112)) → MERGEA_IN_GGA(.(s(T135), T110), T112)
MERGEA_IN_GGA(.(s(T123), T110), .(s(T124), T112)) → PD_IN_GGGGA(T123, T124, T110, T112)

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

POL(.(x₁, x₂)) = 1 + x₂   
POL(MERGEA_IN_GGA(x₁, x₂)) = x₂   
POL(PB_IN_GGGGA(x₁, x₂, x₃, x₄)) = 1 + x₄   
POL(PC_IN_GGGGA(x₁, x₂, x₃, x₄)) = x₄   
POL(PD_IN_GGGGA(x₁, x₂, x₃, x₄)) = x₄   
POL(U11_GGGGA(x₁, x₂, x₃, x₄, x₅)) = x₄   
POL(U13_GGGGA(x₁, x₂, x₃, x₄, x₅)) = x₄   
POL(U7_gg(x₁, x₂, x₃)) = 0   
POL(U8_gg(x₁, x₂, x₃)) = 0   
POL(U9_GGGGA(x₁, x₂, x₃, x₄, x₅)) = 1 + x₄   
POL(gtF_in_gg(x₁, x₂)) = 0   
POL(gtF_out_gg(x₁, x₂)) = 0   
POL(leE_in_gg(x₁, x₂)) = 0   
POL(leE_out_gg(x₁, x₂)) = 0   
POL(s(x₁)) = 0   
POL(zero) = 0   

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

(27) Obligation:

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

MERGEA_IN_GGA(.(s(T31), T18), .(s(T32), T20)) → PB_IN_GGGGA(T31, T32, T18, T20)
PB_IN_GGGGA(T31, T32, T18, T20) → U9_GGGGA(T31, T32, T18, T20, leE_in_gg(T31, T32))
U9_GGGGA(T31, T32, T18, T20, leE_out_gg(T31, T32)) → MERGEA_IN_GGA(T18, .(s(T32), T20))
MERGEA_IN_GGA(.(zero, T18), .(s(T60), T20)) → MERGEA_IN_GGA(T18, .(s(T60), T20))
PC_IN_GGGGA(T75, T77, T76, T78) → U11_GGGGA(T75, T77, T76, T78, gtF_in_gg(T75, T77))
U11_GGGGA(T75, T77, T76, T78, gtF_out_gg(T75, T77)) → MERGEA_IN_GGA(.(T75, T76), T78)
MERGEA_IN_GGA(.(zero, T18), .(zero, T20)) → MERGEA_IN_GGA(T18, .(zero, T20))
PD_IN_GGGGA(T123, T124, T110, T112) → U13_GGGGA(T123, T124, T110, T112, gtF_in_gg(T123, T124))
U13_GGGGA(T123, T124, T110, T112, gtF_out_gg(T123, T124)) → MERGEA_IN_GGA(.(s(T123), T110), T112)

The TRS R consists of the following rules:

leE_in_gg(s(T45), s(T46)) → U7_gg(T45, T46, leE_in_gg(T45, T46))
leE_in_gg(zero, s(T53)) → leE_out_gg(zero, s(T53))
leE_in_gg(zero, zero) → leE_out_gg(zero, zero)
gtF_in_gg(s(T93), s(T94)) → U8_gg(T93, T94, gtF_in_gg(T93, T94))
gtF_in_gg(s(T99), zero) → gtF_out_gg(s(T99), zero)
U7_gg(T45, T46, leE_out_gg(T45, T46)) → leE_out_gg(s(T45), s(T46))
U8_gg(T93, T94, gtF_out_gg(T93, T94)) → gtF_out_gg(s(T93), s(T94))

The set Q consists of the following terms:

leE_in_gg(x0, x1)
gtF_in_gg(x0, x1)
U7_gg(x0, x1, x2)
U8_gg(x0, x1, x2)

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

(28) DependencyGraphProof (EQUIVALENT transformation)

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

(29) Complex Obligation (AND)

(30) Obligation:

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

MERGEA_IN_GGA(.(zero, T18), .(zero, T20)) → MERGEA_IN_GGA(T18, .(zero, T20))

The TRS R consists of the following rules:

leE_in_gg(s(T45), s(T46)) → U7_gg(T45, T46, leE_in_gg(T45, T46))
leE_in_gg(zero, s(T53)) → leE_out_gg(zero, s(T53))
leE_in_gg(zero, zero) → leE_out_gg(zero, zero)
gtF_in_gg(s(T93), s(T94)) → U8_gg(T93, T94, gtF_in_gg(T93, T94))
gtF_in_gg(s(T99), zero) → gtF_out_gg(s(T99), zero)
U7_gg(T45, T46, leE_out_gg(T45, T46)) → leE_out_gg(s(T45), s(T46))
U8_gg(T93, T94, gtF_out_gg(T93, T94)) → gtF_out_gg(s(T93), s(T94))

The set Q consists of the following terms:

leE_in_gg(x0, x1)
gtF_in_gg(x0, x1)
U7_gg(x0, x1, x2)
U8_gg(x0, x1, x2)

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

(31) UsableRulesProof (EQUIVALENT transformation)

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

(32) Obligation:

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

MERGEA_IN_GGA(.(zero, T18), .(zero, T20)) → MERGEA_IN_GGA(T18, .(zero, T20))

R is empty.
The set Q consists of the following terms:

leE_in_gg(x0, x1)
gtF_in_gg(x0, x1)
U7_gg(x0, x1, x2)
U8_gg(x0, x1, x2)

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

(33) QReductionProof (EQUIVALENT transformation)

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

leE_in_gg(x0, x1)
gtF_in_gg(x0, x1)
U7_gg(x0, x1, x2)
U8_gg(x0, x1, x2)

(34) Obligation:

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

MERGEA_IN_GGA(.(zero, T18), .(zero, T20)) → MERGEA_IN_GGA(T18, .(zero, T20))

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

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

• MERGEA_IN_GGA(.(zero, T18), .(zero, T20)) → MERGEA_IN_GGA(T18, .(zero, T20))
  The graph contains the following edges 1 > 1, 2 >= 2

(36) YES

(37) Obligation:

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

PB_IN_GGGGA(T31, T32, T18, T20) → U9_GGGGA(T31, T32, T18, T20, leE_in_gg(T31, T32))
U9_GGGGA(T31, T32, T18, T20, leE_out_gg(T31, T32)) → MERGEA_IN_GGA(T18, .(s(T32), T20))
MERGEA_IN_GGA(.(s(T31), T18), .(s(T32), T20)) → PB_IN_GGGGA(T31, T32, T18, T20)
MERGEA_IN_GGA(.(zero, T18), .(s(T60), T20)) → MERGEA_IN_GGA(T18, .(s(T60), T20))

The TRS R consists of the following rules:

leE_in_gg(s(T45), s(T46)) → U7_gg(T45, T46, leE_in_gg(T45, T46))
leE_in_gg(zero, s(T53)) → leE_out_gg(zero, s(T53))
leE_in_gg(zero, zero) → leE_out_gg(zero, zero)
gtF_in_gg(s(T93), s(T94)) → U8_gg(T93, T94, gtF_in_gg(T93, T94))
gtF_in_gg(s(T99), zero) → gtF_out_gg(s(T99), zero)
U7_gg(T45, T46, leE_out_gg(T45, T46)) → leE_out_gg(s(T45), s(T46))
U8_gg(T93, T94, gtF_out_gg(T93, T94)) → gtF_out_gg(s(T93), s(T94))

The set Q consists of the following terms:

leE_in_gg(x0, x1)
gtF_in_gg(x0, x1)
U7_gg(x0, x1, x2)
U8_gg(x0, x1, x2)

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

(38) UsableRulesProof (EQUIVALENT transformation)

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

(39) Obligation:

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

PB_IN_GGGGA(T31, T32, T18, T20) → U9_GGGGA(T31, T32, T18, T20, leE_in_gg(T31, T32))
U9_GGGGA(T31, T32, T18, T20, leE_out_gg(T31, T32)) → MERGEA_IN_GGA(T18, .(s(T32), T20))
MERGEA_IN_GGA(.(s(T31), T18), .(s(T32), T20)) → PB_IN_GGGGA(T31, T32, T18, T20)
MERGEA_IN_GGA(.(zero, T18), .(s(T60), T20)) → MERGEA_IN_GGA(T18, .(s(T60), T20))

The TRS R consists of the following rules:

leE_in_gg(s(T45), s(T46)) → U7_gg(T45, T46, leE_in_gg(T45, T46))
leE_in_gg(zero, s(T53)) → leE_out_gg(zero, s(T53))
leE_in_gg(zero, zero) → leE_out_gg(zero, zero)
U7_gg(T45, T46, leE_out_gg(T45, T46)) → leE_out_gg(s(T45), s(T46))

The set Q consists of the following terms:

leE_in_gg(x0, x1)
gtF_in_gg(x0, x1)
U7_gg(x0, x1, x2)
U8_gg(x0, x1, x2)

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

(40) QReductionProof (EQUIVALENT transformation)

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

gtF_in_gg(x0, x1)
U8_gg(x0, x1, x2)

(41) Obligation:

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

PB_IN_GGGGA(T31, T32, T18, T20) → U9_GGGGA(T31, T32, T18, T20, leE_in_gg(T31, T32))
U9_GGGGA(T31, T32, T18, T20, leE_out_gg(T31, T32)) → MERGEA_IN_GGA(T18, .(s(T32), T20))
MERGEA_IN_GGA(.(s(T31), T18), .(s(T32), T20)) → PB_IN_GGGGA(T31, T32, T18, T20)
MERGEA_IN_GGA(.(zero, T18), .(s(T60), T20)) → MERGEA_IN_GGA(T18, .(s(T60), T20))

The TRS R consists of the following rules:

leE_in_gg(s(T45), s(T46)) → U7_gg(T45, T46, leE_in_gg(T45, T46))
leE_in_gg(zero, s(T53)) → leE_out_gg(zero, s(T53))
leE_in_gg(zero, zero) → leE_out_gg(zero, zero)
U7_gg(T45, T46, leE_out_gg(T45, T46)) → leE_out_gg(s(T45), s(T46))

The set Q consists of the following terms:

leE_in_gg(x0, x1)
U7_gg(x0, x1, x2)

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

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

• U9_GGGGA(T31, T32, T18, T20, leE_out_gg(T31, T32)) → MERGEA_IN_GGA(T18, .(s(T32), T20))
  The graph contains the following edges 3 >= 1

• MERGEA_IN_GGA(.(s(T31), T18), .(s(T32), T20)) → PB_IN_GGGGA(T31, T32, T18, T20)
  The graph contains the following edges 1 > 1, 2 > 2, 1 > 3, 2 > 4

• MERGEA_IN_GGA(.(zero, T18), .(s(T60), T20)) → MERGEA_IN_GGA(T18, .(s(T60), T20))
  The graph contains the following edges 1 > 1, 2 >= 2

• PB_IN_GGGGA(T31, T32, T18, T20) → U9_GGGGA(T31, T32, T18, T20, leE_in_gg(T31, T32))
  The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4

(43) YES