Left Termination proof of /tmp/tmphCAYR2/pl8.3.1a.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 252 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 260 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 14 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇔, 0 ms)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔, 0 ms)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇒, 0 ms)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔, 0 ms)

        ↳20 YES

    ↳21 PiDP

        ↳22 UsableRulesProof (⇔, 0 ms)

        ↳23 PiDP

        ↳24 PiDPToQDPProof (⇔, 0 ms)

        ↳25 QDP

        ↳26 QDPSizeChangeProof (⇔, 0 ms)

        ↳27 YES

    ↳28 PiDP

        ↳29 UsableRulesProof (⇔, 0 ms)

        ↳30 PiDP

        ↳31 PiDPToQDPProof (⇔, 0 ms)

        ↳32 QDP

        ↳33 QDPSizeChangeProof (⇔, 0 ms)

        ↳34 YES

    ↳35 PiDP

        ↳36 UsableRulesProof (⇔, 0 ms)

        ↳37 PiDP

        ↳38 PiDPToQDPProof (⇒, 0 ms)

        ↳39 QDP

        ↳40 QDPSizeChangeProof (⇔, 0 ms)

        ↳41 YES

    ↳42 PiDP

        ↳43 UsableRulesProof (⇔, 0 ms)

        ↳44 PiDP

        ↳45 PiDPToQDPProof (⇒, 6 ms)

        ↳46 QDP

        ↳47 QDPOrderProof (⇔, 283 ms)

        ↳48 QDP

        ↳49 DependencyGraphProof (⇔, 0 ms)

        ↳50 TRUE

(0) Obligation:

Clauses:

minsort([], []).
minsort(L, .(X, L1)) :- ','(min1(X, L), ','(remove(X, L, L2), minsort(L2, L1))).
min1(M, .(X, L)) :- min2(X, M, L).
min2(X, X, []).
min2(X, A, .(M, L)) :- ','(min(X, M, B), min2(B, A, L)).
min(X, Y, X) :- le(X, Y).
min(X, Y, Y) :- gt(X, Y).
remove(N, .(N, L), L).
remove(N, .(M, L), .(M, L1)) :- ','(notEq(N, M), remove(N, L, L1)).
gt(s(X), s(Y)) :- gt(X, Y).
gt(s(X), 0).
le(s(X), s(Y)) :- le(X, Y).
le(0, s(Y)).
le(0, 0).
notEq(s(X), s(Y)) :- notEq(X, Y).
notEq(s(X), 0).
notEq(0, s(X)).

Query: minsort(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: minsort(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: minsort(T1, T2), SCOPE: 1, CLAUSE: 0 | minsort(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: true | minsort([], T2), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: minsort(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nminsort(T1, T2) !=? minsort([], [])", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: minsort([], T2), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(min1(T7, []), ','(remove(T7, [], X7), minsort(X7, T8)))\n\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(min1(T7, []), ','(remove(T7, [], X7), minsort(X7, T8))), SCOPE: 2, CLAUSE: 2\n\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(min1(T16, T13), ','(remove(T16, T13, X17), minsort(X17, T17)))\n\nT13 is ground\nX17 is free\nminsort(T13, T2) !=? minsort([], [])", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(min1(T16, T13), ','(remove(T16, T13, X17), minsort(X17, T17))), SCOPE: 3, CLAUSE: 2\n\nT13 is ground\nX17 is free\nminsort(T13, T2) !=? minsort([], [])", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="B: ','(min2(T25, T27, T26), ','(remove(T27, .(T25, T26), X17), minsort(X17, T28)))\n\nT25 is ground\nT26 is ground\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="C: min2(T25, T27, T26)\n\nT25 is ground\nT26 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="L: ','(remove(T31, .(T25, T26), X17), minsort(X17, T32))\n\nT25 is ground\nT26 is ground\nT31 is ground\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: min2(T25, T27, T26), SCOPE: 4, CLAUSE: 3 | min2(T25, T27, T26), SCOPE: 4, CLAUSE: 4\n\nT25 is ground\nT26 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: min2(T25, T27, T26), SCOPE: 4, CLAUSE: 3\n\nT25 is ground\nT26 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: min2(T25, T27, T26), SCOPE: 4, CLAUSE: 4\n\nT25 is ground\nT26 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="D: ','(min(T48, T50, X49), min2(X49, T52, T51))\n\nT48 is ground\nT50 is ground\nT51 is ground\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="J: min(T48, T50, X49)\n\nT48 is ground\nT50 is ground\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: min2(T55, T52, T51)\n\nT51 is ground\nT55 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: min(T48, T50, X49), SCOPE: 5, CLAUSE: 5 | min(T48, T50, X49), SCOPE: 5, CLAUSE: 6\n\nT48 is ground\nT50 is ground\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: min(T48, T50, X49), SCOPE: 5, CLAUSE: 5\n\nT48 is ground\nT50 is ground\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: min(T48, T50, X49), SCOPE: 5, CLAUSE: 6\n\nT48 is ground\nT50 is ground\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="E: le(T70, T71)\n\nT70 is ground\nT71 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: le(T70, T71), SCOPE: 6, CLAUSE: 11 | le(T70, T71), SCOPE: 6, CLAUSE: 12 | le(T70, T71), SCOPE: 6, CLAUSE: 13\n\nT70 is ground\nT71 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: le(T70, T71), SCOPE: 6, CLAUSE: 11\n\nT70 is ground\nT71 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: le(T70, T71), SCOPE: 6, CLAUSE: 12 | le(T70, T71), SCOPE: 6, CLAUSE: 13\n\nT70 is ground\nT71 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: le(T82, T83)\n\nT82 is ground\nT83 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: le(T70, T71), SCOPE: 6, CLAUSE: 12\n\nT70 is ground\nT71 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: le(T70, T71), SCOPE: 6, CLAUSE: 13\n\nT70 is ground\nT71 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: \n\n", 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];
125 [label="F: gt(T97, T98)\n\nT97 is ground\nT98 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: gt(T97, T98), SCOPE: 7, CLAUSE: 9 | gt(T97, T98), SCOPE: 7, CLAUSE: 10\n\nT97 is ground\nT98 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: gt(T97, T98), SCOPE: 7, CLAUSE: 9\n\nT97 is ground\nT98 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: gt(T97, T98), SCOPE: 7, CLAUSE: 10\n\nT97 is ground\nT98 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: gt(T109, T110)\n\nT109 is ground\nT110 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="H: remove(T31, .(T25, T26), X17)\n\nT25 is ground\nT26 is ground\nT31 is ground\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: minsort(T122, T32)\n\nT122 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: remove(T31, .(T25, T26), X17), SCOPE: 8, CLAUSE: 7 | remove(T31, .(T25, T26), X17), SCOPE: 8, CLAUSE: 8\n\nT25 is ground\nT26 is ground\nT31 is ground\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: remove(T31, .(T25, T26), X17), SCOPE: 8, CLAUSE: 7\n\nT25 is ground\nT26 is ground\nT31 is ground\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: remove(T31, .(T25, T26), X17), SCOPE: 8, CLAUSE: 8\n\nT25 is ground\nT26 is ground\nT31 is ground\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="I: ','(notEq(T145, T146), remove(T145, T147, X148))\n\nT145 is ground\nT146 is ground\nT147 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="G: notEq(T145, T146)\n\nT145 is ground\nT146 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="K: remove(T145, T147, X148)\n\nT145 is ground\nT147 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: notEq(T145, T146), SCOPE: 9, CLAUSE: 14 | notEq(T145, T146), SCOPE: 9, CLAUSE: 15 | notEq(T145, T146), SCOPE: 9, CLAUSE: 16\n\nT145 is ground\nT146 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: notEq(T145, T146), SCOPE: 9, CLAUSE: 14\n\nT145 is ground\nT146 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: notEq(T145, T146), SCOPE: 9, CLAUSE: 15 | notEq(T145, T146), SCOPE: 9, CLAUSE: 16\n\nT145 is ground\nT146 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: notEq(T160, T161)\n\nT160 is ground\nT161 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
227 [label="227: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
228 [label="228: notEq(T145, T146), SCOPE: 9, CLAUSE: 15\n\nT145 is ground\nT146 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
229 [label="229: notEq(T145, T146), SCOPE: 9, CLAUSE: 16\n\nT145 is ground\nT146 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
230 [label="230: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="231: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
232 [label="232: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
233 [label="233: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
234 [label="234: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
236 [label="236: remove(T145, T147, X148), SCOPE: 10, CLAUSE: 7 | remove(T145, T147, X148), SCOPE: 10, CLAUSE: 8\n\nT145 is ground\nT147 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
237 [label="237: remove(T145, T147, X148), SCOPE: 10, CLAUSE: 7\n\nT145 is ground\nT147 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
238 [label="238: remove(T145, T147, X148), SCOPE: 10, CLAUSE: 8\n\nT145 is ground\nT147 is ground\nX148 is free", fontsize=16, style=filled, fillcolor=lightyellow];
239 [label="239: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
240 [label="240: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
241 [label="241: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
242 [label="242: ','(notEq(T192, T193), remove(T192, T194, X201))\n\nT192 is ground\nT193 is ground\nT194 is ground\nX201 is free", fontsize=16, style=filled, fillcolor=lightyellow];
243 [label="243: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
244 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 244 [arrowhead = none ];
244 -> 6;

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

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

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

248 [label="EVAL with clause\nminsort(X14, .(X15, X16)) :- ','(min1(X15, X14), ','(remove(X15, X14, X17), minsort(X17, X16))).\nand substitutionT1 -> T13,\nX14 -> T13,\nX15 -> T16,\nX16 -> T17,\nT2 -> .(T16, T17),\nT14 -> T16,\nT15 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 248 [arrowhead = none ];
248 -> 30;

249 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 249 [arrowhead = none ];
249 -> 32;

250 [label="EVAL with clause\nminsort(X4, .(X5, X6)) :- ','(min1(X5, X4), ','(remove(X5, X4, X7), minsort(X7, X6))).\nand substitutionX4 -> [],\nX5 -> T7,\nX6 -> T8,\nT2 -> .(T7, T8),\nT5 -> T7,\nT6 -> T8", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 250 [arrowhead = none ];
250 -> 24;

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

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

253 [label="BACKTRACK\nfor clause: min1(M, .(X, L)) :- min2(X, M, L)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
26 -> 253 [arrowhead = none ];
253 -> 27;

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

255 [label="EVAL with clause\nmin1(X24, .(X25, X26)) :- min2(X25, X24, X26).\nand substitutionT16 -> T27,\nX24 -> T27,\nX25 -> T25,\nX26 -> T26,\nT13 -> .(T25, T26),\nT24 -> T27,\nT17 -> T28", fontsize=14, style = filled, fillcolor = lightblue];
33 -> 255 [arrowhead = none ];
255 -> 38;

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

257 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
38 -> 257 [arrowhead = none ];
257 -> 49;

258 [label="SPLIT 2\nnew knowledge:\nT25 is ground\nT31 is ground\nT26 is ground\nreplacements:T27 -> T31,\nT28 -> T32", fontsize=14, style = filled, fillcolor = violet];
38 -> 258 [arrowhead = none ];
258 -> 50;

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

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

261 [label="SPLIT 2\nnew knowledge:\nT31 is ground\nT25 is ground\nT26 is ground\nT122 is ground\nreplacements:X17 -> T122", fontsize=14, style = filled, fillcolor = violet];
50 -> 261 [arrowhead = none ];
261 -> 159;

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

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

264 [label="EVAL with clause\nmin2(X35, X35, []).\nand substitutionT25 -> T39,\nX35 -> T39,\nT27 -> T39,\nT26 -> []", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 264 [arrowhead = none ];
264 -> 56;

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

266 [label="EVAL with clause\nmin2(X45, X46, .(X47, X48)) :- ','(min(X45, X47, X49), min2(X49, X46, X48)).\nand substitutionT25 -> T48,\nX45 -> T48,\nT27 -> T52,\nX46 -> T52,\nX47 -> T50,\nX48 -> T51,\nT26 -> .(T50, T51),\nT49 -> T52", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 266 [arrowhead = none ];
266 -> 67;

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

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

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

270 [label="SPLIT 2\nnew knowledge:\nT48 is ground\nT50 is ground\nT55 is ground\nreplacements:X49 -> T55", fontsize=14, style = filled, fillcolor = violet];
67 -> 270 [arrowhead = none ];
270 -> 75;

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

272 [label="INSTANCE with matching:\nT25 -> T55\nT27 -> T52\nT26 -> T51", fontsize=14, style = filled, fillcolor = lightgrey];
75 -> 272 [arrowhead = none , style=dashed];
272 -> 49[style=dashed];

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

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

275 [label="ONLY EVAL with clause\nmin(X66, X67, X66) :- le(X66, X67).\nand substitutionT48 -> T70,\nX66 -> T70,\nT50 -> T71,\nX67 -> T71,\nX49 -> T70", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 275 [arrowhead = none ];
275 -> 88;

276 [label="ONLY EVAL with clause\nmin(X93, X94, X94) :- gt(X93, X94).\nand substitutionT48 -> T97,\nX93 -> T97,\nT50 -> T98,\nX94 -> T98,\nX49 -> T98", fontsize=14, style = filled, fillcolor = lightblue];
81 -> 276 [arrowhead = none ];
276 -> 125;

277 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
88 -> 277 [arrowhead = none ];
277 -> 89;

278 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
89 -> 278 [arrowhead = none ];
278 -> 94;

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

280 [label="EVAL with clause\nle(s(X78), s(X79)) :- le(X78, X79).\nand substitutionX78 -> T82,\nT70 -> s(T82),\nX79 -> T83,\nT71 -> s(T83)", fontsize=14, style = filled, fillcolor = lightblue];
94 -> 280 [arrowhead = none ];
280 -> 99;

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

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

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

284 [label="INSTANCE with matching:\nT70 -> T82\nT71 -> T83", fontsize=14, style = filled, fillcolor = lightgrey];
99 -> 284 [arrowhead = none , style=dashed];
284 -> 88[style=dashed];

285 [label="EVAL with clause\nle(0, s(X86)).\nand substitutionT70 -> 0,\nX86 -> T90,\nT71 -> s(T90)", fontsize=14, style = filled, fillcolor = lightblue];
110 -> 285 [arrowhead = none ];
285 -> 112;

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

287 [label="EVAL with clause\nle(0, 0).\nand substitutionT70 -> 0,\nT71 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
111 -> 287 [arrowhead = none ];
287 -> 118;

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

289 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
112 -> 289 [arrowhead = none ];
289 -> 114;

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

291 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
125 -> 291 [arrowhead = none ];
291 -> 133;

292 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
133 -> 292 [arrowhead = none ];
292 -> 136;

293 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
133 -> 293 [arrowhead = none ];
293 -> 137;

294 [label="EVAL with clause\ngt(s(X105), s(X106)) :- gt(X105, X106).\nand substitutionX105 -> T109,\nT97 -> s(T109),\nX106 -> T110,\nT98 -> s(T110)", fontsize=14, style = filled, fillcolor = lightblue];
136 -> 294 [arrowhead = none ];
294 -> 139;

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

296 [label="EVAL with clause\ngt(s(X111), 0).\nand substitutionX111 -> T115,\nT97 -> s(T115),\nT98 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
137 -> 296 [arrowhead = none ];
296 -> 147;

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

298 [label="INSTANCE with matching:\nT97 -> T109\nT98 -> T110", fontsize=14, style = filled, fillcolor = lightgrey];
139 -> 298 [arrowhead = none , style=dashed];
298 -> 125[style=dashed];

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

300 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
158 -> 300 [arrowhead = none ];
300 -> 162;

301 [label="INSTANCE with matching:\nT1 -> T122\nT2 -> T32", fontsize=14, style = filled, fillcolor = lightgrey];
159 -> 301 [arrowhead = none , style=dashed];
301 -> 3[style=dashed];

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

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

304 [label="EVAL with clause\nremove(X130, .(X130, X131), X131).\nand substitutionT31 -> T135,\nX130 -> T135,\nT25 -> T135,\nT26 -> T136,\nX131 -> T136,\nX17 -> T136", fontsize=14, style = filled, fillcolor = lightblue];
168 -> 304 [arrowhead = none ];
304 -> 171;

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

306 [label="ONLY EVAL with clause\nremove(X144, .(X145, X146), .(X145, X147)) :- ','(notEq(X144, X145), remove(X144, X146, X147)).\nand substitutionT31 -> T145,\nX144 -> T145,\nT25 -> T146,\nX145 -> T146,\nT26 -> T147,\nX146 -> T147,\nX147 -> X148,\nX17 -> .(T146, X148)", fontsize=14, style = filled, fillcolor = lightblue];
169 -> 306 [arrowhead = none ];
306 -> 182;

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

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

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

310 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
200 -> 310 [arrowhead = none ];
310 -> 207;

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

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

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

314 [label="EVAL with clause\nnotEq(s(X161), s(X162)) :- notEq(X161, X162).\nand substitutionX161 -> T160,\nT145 -> s(T160),\nX162 -> T161,\nT146 -> s(T161)", fontsize=14, style = filled, fillcolor = lightblue];
208 -> 314 [arrowhead = none ];
314 -> 218;

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

316 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
209 -> 316 [arrowhead = none ];
316 -> 228;

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

318 [label="INSTANCE with matching:\nT145 -> T160\nT146 -> T161", fontsize=14, style = filled, fillcolor = lightgrey];
218 -> 318 [arrowhead = none , style=dashed];
318 -> 200[style=dashed];

319 [label="EVAL with clause\nnotEq(s(X169), 0).\nand substitutionX169 -> T168,\nT145 -> s(T168),\nT146 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
228 -> 319 [arrowhead = none ];
319 -> 230;

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

321 [label="EVAL with clause\nnotEq(0, s(X172)).\nand substitutionT145 -> 0,\nX172 -> T171,\nT146 -> s(T171)", fontsize=14, style = filled, fillcolor = lightblue];
229 -> 321 [arrowhead = none ];
321 -> 233;

322 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
229 -> 322 [arrowhead = none ];
322 -> 234;

323 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
230 -> 323 [arrowhead = none ];
323 -> 232;

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

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

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

327 [label="EVAL with clause\nremove(X185, .(X185, X186), X186).\nand substitutionT145 -> T184,\nX185 -> T184,\nX186 -> T185,\nT147 -> .(T184, T185),\nX148 -> T185", fontsize=14, style = filled, fillcolor = lightblue];
237 -> 327 [arrowhead = none ];
327 -> 239;

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

329 [label="EVAL with clause\nremove(X197, .(X198, X199), .(X198, X200)) :- ','(notEq(X197, X198), remove(X197, X199, X200)).\nand substitutionT145 -> T192,\nX197 -> T192,\nX198 -> T193,\nX199 -> T194,\nT147 -> .(T193, T194),\nX200 -> X201,\nX148 -> .(T193, X201)", fontsize=14, style = filled, fillcolor = lightblue];
238 -> 329 [arrowhead = none ];
329 -> 242;

330 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
238 -> 330 [arrowhead = none ];
330 -> 243;

331 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
239 -> 331 [arrowhead = none ];
331 -> 241;

332 [label="INSTANCE with matching:\nT145 -> T192\nT146 -> T193\nT147 -> T194\nX148 -> X201", fontsize=14, style = filled, fillcolor = lightgrey];
242 -> 332 [arrowhead = none , style=dashed];
332 -> 182[style=dashed];

}

(2) Obligation:

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

minsortA_in_ga([], []) → minsortA_out_ga([], [])
minsortA_in_ga(.(T25, T26), .(T27, T28)) → U1_ga(T25, T26, T27, T28, pB_in_gagaa(T25, T27, T26, X17, T28))
pB_in_gagaa(T25, T31, T26, X17, T32) → U10_gagaa(T25, T31, T26, X17, T32, min2C_in_gag(T25, T31, T26))
min2C_in_gag(T39, T39, []) → min2C_out_gag(T39, T39, [])
min2C_in_gag(T48, T52, .(T50, T51)) → U2_gag(T48, T52, T50, T51, pD_in_ggaag(T48, T50, X49, T52, T51))
pD_in_ggaag(T48, T50, T55, T52, T51) → U14_ggaag(T48, T50, T55, T52, T51, minJ_in_gga(T48, T50, T55))
minJ_in_gga(T70, T71, T70) → U7_gga(T70, T71, leE_in_gg(T70, T71))
leE_in_gg(s(T82), s(T83)) → U3_gg(T82, T83, leE_in_gg(T82, T83))
leE_in_gg(0, s(T90)) → leE_out_gg(0, s(T90))
leE_in_gg(0, 0) → leE_out_gg(0, 0)
U3_gg(T82, T83, leE_out_gg(T82, T83)) → leE_out_gg(s(T82), s(T83))
U7_gga(T70, T71, leE_out_gg(T70, T71)) → minJ_out_gga(T70, T71, T70)
minJ_in_gga(T97, T98, T98) → U8_gga(T97, T98, gtF_in_gg(T97, T98))
gtF_in_gg(s(T109), s(T110)) → U4_gg(T109, T110, gtF_in_gg(T109, T110))
gtF_in_gg(s(T115), 0) → gtF_out_gg(s(T115), 0)
U4_gg(T109, T110, gtF_out_gg(T109, T110)) → gtF_out_gg(s(T109), s(T110))
U8_gga(T97, T98, gtF_out_gg(T97, T98)) → minJ_out_gga(T97, T98, T98)
U14_ggaag(T48, T50, T55, T52, T51, minJ_out_gga(T48, T50, T55)) → U15_ggaag(T48, T50, T55, T52, T51, min2C_in_gag(T55, T52, T51))
U15_ggaag(T48, T50, T55, T52, T51, min2C_out_gag(T55, T52, T51)) → pD_out_ggaag(T48, T50, T55, T52, T51)
U2_gag(T48, T52, T50, T51, pD_out_ggaag(T48, T50, X49, T52, T51)) → min2C_out_gag(T48, T52, .(T50, T51))
U10_gagaa(T25, T31, T26, X17, T32, min2C_out_gag(T25, T31, T26)) → U11_gagaa(T25, T31, T26, X17, T32, pL_in_gggaa(T31, T25, T26, X17, T32))
pL_in_gggaa(T31, T25, T26, T122, T32) → U12_gggaa(T31, T25, T26, T122, T32, removeH_in_ggga(T31, T25, T26, T122))
removeH_in_ggga(T135, T135, T136, T136) → removeH_out_ggga(T135, T135, T136, T136)
removeH_in_ggga(T145, T146, T147, .(T146, X148)) → U6_ggga(T145, T146, T147, X148, pI_in_ggga(T145, T146, T147, X148))
pI_in_ggga(T145, T146, T147, X148) → U16_ggga(T145, T146, T147, X148, notEqG_in_gg(T145, T146))
notEqG_in_gg(s(T160), s(T161)) → U5_gg(T160, T161, notEqG_in_gg(T160, T161))
notEqG_in_gg(s(T168), 0) → notEqG_out_gg(s(T168), 0)
notEqG_in_gg(0, s(T171)) → notEqG_out_gg(0, s(T171))
U5_gg(T160, T161, notEqG_out_gg(T160, T161)) → notEqG_out_gg(s(T160), s(T161))
U16_ggga(T145, T146, T147, X148, notEqG_out_gg(T145, T146)) → U17_ggga(T145, T146, T147, X148, removeK_in_gga(T145, T147, X148))
removeK_in_gga(T184, .(T184, T185), T185) → removeK_out_gga(T184, .(T184, T185), T185)
removeK_in_gga(T192, .(T193, T194), .(T193, X201)) → U9_gga(T192, T193, T194, X201, pI_in_ggga(T192, T193, T194, X201))
U9_gga(T192, T193, T194, X201, pI_out_ggga(T192, T193, T194, X201)) → removeK_out_gga(T192, .(T193, T194), .(T193, X201))
U17_ggga(T145, T146, T147, X148, removeK_out_gga(T145, T147, X148)) → pI_out_ggga(T145, T146, T147, X148)
U6_ggga(T145, T146, T147, X148, pI_out_ggga(T145, T146, T147, X148)) → removeH_out_ggga(T145, T146, T147, .(T146, X148))
U12_gggaa(T31, T25, T26, T122, T32, removeH_out_ggga(T31, T25, T26, T122)) → U13_gggaa(T31, T25, T26, T122, T32, minsortA_in_ga(T122, T32))
U13_gggaa(T31, T25, T26, T122, T32, minsortA_out_ga(T122, T32)) → pL_out_gggaa(T31, T25, T26, T122, T32)
U11_gagaa(T25, T31, T26, X17, T32, pL_out_gggaa(T31, T25, T26, X17, T32)) → pB_out_gagaa(T25, T31, T26, X17, T32)
U1_ga(T25, T26, T27, T28, pB_out_gagaa(T25, T27, T26, X17, T28)) → minsortA_out_ga(.(T25, T26), .(T27, T28))

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

MINSORTA_IN_GA(.(T25, T26), .(T27, T28)) → U1_GA(T25, T26, T27, T28, pB_in_gagaa(T25, T27, T26, X17, T28))
MINSORTA_IN_GA(.(T25, T26), .(T27, T28)) → PB_IN_GAGAA(T25, T27, T26, X17, T28)
PB_IN_GAGAA(T25, T31, T26, X17, T32) → U10_GAGAA(T25, T31, T26, X17, T32, min2C_in_gag(T25, T31, T26))
PB_IN_GAGAA(T25, T31, T26, X17, T32) → MIN2C_IN_GAG(T25, T31, T26)
MIN2C_IN_GAG(T48, T52, .(T50, T51)) → U2_GAG(T48, T52, T50, T51, pD_in_ggaag(T48, T50, X49, T52, T51))
MIN2C_IN_GAG(T48, T52, .(T50, T51)) → PD_IN_GGAAG(T48, T50, X49, T52, T51)
PD_IN_GGAAG(T48, T50, T55, T52, T51) → U14_GGAAG(T48, T50, T55, T52, T51, minJ_in_gga(T48, T50, T55))
PD_IN_GGAAG(T48, T50, T55, T52, T51) → MINJ_IN_GGA(T48, T50, T55)
MINJ_IN_GGA(T70, T71, T70) → U7_GGA(T70, T71, leE_in_gg(T70, T71))
MINJ_IN_GGA(T70, T71, T70) → LEE_IN_GG(T70, T71)
LEE_IN_GG(s(T82), s(T83)) → U3_GG(T82, T83, leE_in_gg(T82, T83))
LEE_IN_GG(s(T82), s(T83)) → LEE_IN_GG(T82, T83)
MINJ_IN_GGA(T97, T98, T98) → U8_GGA(T97, T98, gtF_in_gg(T97, T98))
MINJ_IN_GGA(T97, T98, T98) → GTF_IN_GG(T97, T98)
GTF_IN_GG(s(T109), s(T110)) → U4_GG(T109, T110, gtF_in_gg(T109, T110))
GTF_IN_GG(s(T109), s(T110)) → GTF_IN_GG(T109, T110)
U14_GGAAG(T48, T50, T55, T52, T51, minJ_out_gga(T48, T50, T55)) → U15_GGAAG(T48, T50, T55, T52, T51, min2C_in_gag(T55, T52, T51))
U14_GGAAG(T48, T50, T55, T52, T51, minJ_out_gga(T48, T50, T55)) → MIN2C_IN_GAG(T55, T52, T51)
U10_GAGAA(T25, T31, T26, X17, T32, min2C_out_gag(T25, T31, T26)) → U11_GAGAA(T25, T31, T26, X17, T32, pL_in_gggaa(T31, T25, T26, X17, T32))
U10_GAGAA(T25, T31, T26, X17, T32, min2C_out_gag(T25, T31, T26)) → PL_IN_GGGAA(T31, T25, T26, X17, T32)
PL_IN_GGGAA(T31, T25, T26, T122, T32) → U12_GGGAA(T31, T25, T26, T122, T32, removeH_in_ggga(T31, T25, T26, T122))
PL_IN_GGGAA(T31, T25, T26, T122, T32) → REMOVEH_IN_GGGA(T31, T25, T26, T122)
REMOVEH_IN_GGGA(T145, T146, T147, .(T146, X148)) → U6_GGGA(T145, T146, T147, X148, pI_in_ggga(T145, T146, T147, X148))
REMOVEH_IN_GGGA(T145, T146, T147, .(T146, X148)) → PI_IN_GGGA(T145, T146, T147, X148)
PI_IN_GGGA(T145, T146, T147, X148) → U16_GGGA(T145, T146, T147, X148, notEqG_in_gg(T145, T146))
PI_IN_GGGA(T145, T146, T147, X148) → NOTEQG_IN_GG(T145, T146)
NOTEQG_IN_GG(s(T160), s(T161)) → U5_GG(T160, T161, notEqG_in_gg(T160, T161))
NOTEQG_IN_GG(s(T160), s(T161)) → NOTEQG_IN_GG(T160, T161)
U16_GGGA(T145, T146, T147, X148, notEqG_out_gg(T145, T146)) → U17_GGGA(T145, T146, T147, X148, removeK_in_gga(T145, T147, X148))
U16_GGGA(T145, T146, T147, X148, notEqG_out_gg(T145, T146)) → REMOVEK_IN_GGA(T145, T147, X148)
REMOVEK_IN_GGA(T192, .(T193, T194), .(T193, X201)) → U9_GGA(T192, T193, T194, X201, pI_in_ggga(T192, T193, T194, X201))
REMOVEK_IN_GGA(T192, .(T193, T194), .(T193, X201)) → PI_IN_GGGA(T192, T193, T194, X201)
U12_GGGAA(T31, T25, T26, T122, T32, removeH_out_ggga(T31, T25, T26, T122)) → U13_GGGAA(T31, T25, T26, T122, T32, minsortA_in_ga(T122, T32))
U12_GGGAA(T31, T25, T26, T122, T32, removeH_out_ggga(T31, T25, T26, T122)) → MINSORTA_IN_GA(T122, T32)

The TRS R consists of the following rules:

minsortA_in_ga([], []) → minsortA_out_ga([], [])
minsortA_in_ga(.(T25, T26), .(T27, T28)) → U1_ga(T25, T26, T27, T28, pB_in_gagaa(T25, T27, T26, X17, T28))
pB_in_gagaa(T25, T31, T26, X17, T32) → U10_gagaa(T25, T31, T26, X17, T32, min2C_in_gag(T25, T31, T26))
min2C_in_gag(T39, T39, []) → min2C_out_gag(T39, T39, [])
min2C_in_gag(T48, T52, .(T50, T51)) → U2_gag(T48, T52, T50, T51, pD_in_ggaag(T48, T50, X49, T52, T51))
pD_in_ggaag(T48, T50, T55, T52, T51) → U14_ggaag(T48, T50, T55, T52, T51, minJ_in_gga(T48, T50, T55))
minJ_in_gga(T70, T71, T70) → U7_gga(T70, T71, leE_in_gg(T70, T71))
leE_in_gg(s(T82), s(T83)) → U3_gg(T82, T83, leE_in_gg(T82, T83))
leE_in_gg(0, s(T90)) → leE_out_gg(0, s(T90))
leE_in_gg(0, 0) → leE_out_gg(0, 0)
U3_gg(T82, T83, leE_out_gg(T82, T83)) → leE_out_gg(s(T82), s(T83))
U7_gga(T70, T71, leE_out_gg(T70, T71)) → minJ_out_gga(T70, T71, T70)
minJ_in_gga(T97, T98, T98) → U8_gga(T97, T98, gtF_in_gg(T97, T98))
gtF_in_gg(s(T109), s(T110)) → U4_gg(T109, T110, gtF_in_gg(T109, T110))
gtF_in_gg(s(T115), 0) → gtF_out_gg(s(T115), 0)
U4_gg(T109, T110, gtF_out_gg(T109, T110)) → gtF_out_gg(s(T109), s(T110))
U8_gga(T97, T98, gtF_out_gg(T97, T98)) → minJ_out_gga(T97, T98, T98)
U14_ggaag(T48, T50, T55, T52, T51, minJ_out_gga(T48, T50, T55)) → U15_ggaag(T48, T50, T55, T52, T51, min2C_in_gag(T55, T52, T51))
U15_ggaag(T48, T50, T55, T52, T51, min2C_out_gag(T55, T52, T51)) → pD_out_ggaag(T48, T50, T55, T52, T51)
U2_gag(T48, T52, T50, T51, pD_out_ggaag(T48, T50, X49, T52, T51)) → min2C_out_gag(T48, T52, .(T50, T51))
U10_gagaa(T25, T31, T26, X17, T32, min2C_out_gag(T25, T31, T26)) → U11_gagaa(T25, T31, T26, X17, T32, pL_in_gggaa(T31, T25, T26, X17, T32))
pL_in_gggaa(T31, T25, T26, T122, T32) → U12_gggaa(T31, T25, T26, T122, T32, removeH_in_ggga(T31, T25, T26, T122))
removeH_in_ggga(T135, T135, T136, T136) → removeH_out_ggga(T135, T135, T136, T136)
removeH_in_ggga(T145, T146, T147, .(T146, X148)) → U6_ggga(T145, T146, T147, X148, pI_in_ggga(T145, T146, T147, X148))
pI_in_ggga(T145, T146, T147, X148) → U16_ggga(T145, T146, T147, X148, notEqG_in_gg(T145, T146))
notEqG_in_gg(s(T160), s(T161)) → U5_gg(T160, T161, notEqG_in_gg(T160, T161))
notEqG_in_gg(s(T168), 0) → notEqG_out_gg(s(T168), 0)
notEqG_in_gg(0, s(T171)) → notEqG_out_gg(0, s(T171))
U5_gg(T160, T161, notEqG_out_gg(T160, T161)) → notEqG_out_gg(s(T160), s(T161))
U16_ggga(T145, T146, T147, X148, notEqG_out_gg(T145, T146)) → U17_ggga(T145, T146, T147, X148, removeK_in_gga(T145, T147, X148))
removeK_in_gga(T184, .(T184, T185), T185) → removeK_out_gga(T184, .(T184, T185), T185)
removeK_in_gga(T192, .(T193, T194), .(T193, X201)) → U9_gga(T192, T193, T194, X201, pI_in_ggga(T192, T193, T194, X201))
U9_gga(T192, T193, T194, X201, pI_out_ggga(T192, T193, T194, X201)) → removeK_out_gga(T192, .(T193, T194), .(T193, X201))
U17_ggga(T145, T146, T147, X148, removeK_out_gga(T145, T147, X148)) → pI_out_ggga(T145, T146, T147, X148)
U6_ggga(T145, T146, T147, X148, pI_out_ggga(T145, T146, T147, X148)) → removeH_out_ggga(T145, T146, T147, .(T146, X148))
U12_gggaa(T31, T25, T26, T122, T32, removeH_out_ggga(T31, T25, T26, T122)) → U13_gggaa(T31, T25, T26, T122, T32, minsortA_in_ga(T122, T32))
U13_gggaa(T31, T25, T26, T122, T32, minsortA_out_ga(T122, T32)) → pL_out_gggaa(T31, T25, T26, T122, T32)
U11_gagaa(T25, T31, T26, X17, T32, pL_out_gggaa(T31, T25, T26, X17, T32)) → pB_out_gagaa(T25, T31, T26, X17, T32)
U1_ga(T25, T26, T27, T28, pB_out_gagaa(T25, T27, T26, X17, T28)) → minsortA_out_ga(.(T25, T26), .(T27, T28))

The argument filtering Pi contains the following mapping:
minsortA_in_ga(x1, x2) = minsortA_in_ga(x1)
[] = []
minsortA_out_ga(x1, x2) = minsortA_out_ga(x1, x2)
.(x1, x2) = .(x1, x2)
U1_ga(x1, x2, x3, x4, x5) = U1_ga(x1, x2, x5)
pB_in_gagaa(x1, x2, x3, x4, x5) = pB_in_gagaa(x1, x3)
U10_gagaa(x1, x2, x3, x4, x5, x6) = U10_gagaa(x1, x3, x6)
min2C_in_gag(x1, x2, x3) = min2C_in_gag(x1, x3)
min2C_out_gag(x1, x2, x3) = min2C_out_gag(x1, x2, x3)
U2_gag(x1, x2, x3, x4, x5) = U2_gag(x1, x3, x4, x5)
pD_in_ggaag(x1, x2, x3, x4, x5) = pD_in_ggaag(x1, x2, x5)
U14_ggaag(x1, x2, x3, x4, x5, x6) = U14_ggaag(x1, x2, x5, x6)
minJ_in_gga(x1, x2, x3) = minJ_in_gga(x1, x2)
U7_gga(x1, x2, x3) = U7_gga(x1, x2, x3)
leE_in_gg(x1, x2) = leE_in_gg(x1, x2)
s(x1) = s(x1)
U3_gg(x1, x2, x3) = U3_gg(x1, x2, x3)
0 = 0
leE_out_gg(x1, x2) = leE_out_gg(x1, x2)
minJ_out_gga(x1, x2, x3) = minJ_out_gga(x1, x2, x3)
U8_gga(x1, x2, x3) = U8_gga(x1, x2, x3)
gtF_in_gg(x1, x2) = gtF_in_gg(x1, x2)
U4_gg(x1, x2, x3) = U4_gg(x1, x2, x3)
gtF_out_gg(x1, x2) = gtF_out_gg(x1, x2)
U15_ggaag(x1, x2, x3, x4, x5, x6) = U15_ggaag(x1, x2, x3, x5, x6)
pD_out_ggaag(x1, x2, x3, x4, x5) = pD_out_ggaag(x1, x2, x3, x4, x5)
U11_gagaa(x1, x2, x3, x4, x5, x6) = U11_gagaa(x1, x2, x3, x6)
pL_in_gggaa(x1, x2, x3, x4, x5) = pL_in_gggaa(x1, x2, x3)
U12_gggaa(x1, x2, x3, x4, x5, x6) = U12_gggaa(x1, x2, x3, x6)
removeH_in_ggga(x1, x2, x3, x4) = removeH_in_ggga(x1, x2, x3)
removeH_out_ggga(x1, x2, x3, x4) = removeH_out_ggga(x1, x2, x3, x4)
U6_ggga(x1, x2, x3, x4, x5) = U6_ggga(x1, x2, x3, x5)
pI_in_ggga(x1, x2, x3, x4) = pI_in_ggga(x1, x2, x3)
U16_ggga(x1, x2, x3, x4, x5) = U16_ggga(x1, x2, x3, x5)
notEqG_in_gg(x1, x2) = notEqG_in_gg(x1, x2)
U5_gg(x1, x2, x3) = U5_gg(x1, x2, x3)
notEqG_out_gg(x1, x2) = notEqG_out_gg(x1, x2)
U17_ggga(x1, x2, x3, x4, x5) = U17_ggga(x1, x2, x3, x5)
removeK_in_gga(x1, x2, x3) = removeK_in_gga(x1, x2)
removeK_out_gga(x1, x2, x3) = removeK_out_gga(x1, x2, x3)
U9_gga(x1, x2, x3, x4, x5) = U9_gga(x1, x2, x3, x5)
pI_out_ggga(x1, x2, x3, x4) = pI_out_ggga(x1, x2, x3, x4)
U13_gggaa(x1, x2, x3, x4, x5, x6) = U13_gggaa(x1, x2, x3, x4, x6)
pL_out_gggaa(x1, x2, x3, x4, x5) = pL_out_gggaa(x1, x2, x3, x4, x5)
pB_out_gagaa(x1, x2, x3, x4, x5) = pB_out_gagaa(x1, x2, x3, x4, x5)
MINSORTA_IN_GA(x1, x2) = MINSORTA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5) = U1_GA(x1, x2, x5)
PB_IN_GAGAA(x1, x2, x3, x4, x5) = PB_IN_GAGAA(x1, x3)
U10_GAGAA(x1, x2, x3, x4, x5, x6) = U10_GAGAA(x1, x3, x6)
MIN2C_IN_GAG(x1, x2, x3) = MIN2C_IN_GAG(x1, x3)
U2_GAG(x1, x2, x3, x4, x5) = U2_GAG(x1, x3, x4, x5)
PD_IN_GGAAG(x1, x2, x3, x4, x5) = PD_IN_GGAAG(x1, x2, x5)
U14_GGAAG(x1, x2, x3, x4, x5, x6) = U14_GGAAG(x1, x2, x5, x6)
MINJ_IN_GGA(x1, x2, x3) = MINJ_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3) = U7_GGA(x1, x2, x3)
LEE_IN_GG(x1, x2) = LEE_IN_GG(x1, x2)
U3_GG(x1, x2, x3) = U3_GG(x1, x2, x3)
U8_GGA(x1, x2, x3) = U8_GGA(x1, x2, x3)
GTF_IN_GG(x1, x2) = GTF_IN_GG(x1, x2)
U4_GG(x1, x2, x3) = U4_GG(x1, x2, x3)
U15_GGAAG(x1, x2, x3, x4, x5, x6) = U15_GGAAG(x1, x2, x3, x5, x6)
U11_GAGAA(x1, x2, x3, x4, x5, x6) = U11_GAGAA(x1, x2, x3, x6)
PL_IN_GGGAA(x1, x2, x3, x4, x5) = PL_IN_GGGAA(x1, x2, x3)
U12_GGGAA(x1, x2, x3, x4, x5, x6) = U12_GGGAA(x1, x2, x3, x6)
REMOVEH_IN_GGGA(x1, x2, x3, x4) = REMOVEH_IN_GGGA(x1, x2, x3)
U6_GGGA(x1, x2, x3, x4, x5) = U6_GGGA(x1, x2, x3, x5)
PI_IN_GGGA(x1, x2, x3, x4) = PI_IN_GGGA(x1, x2, x3)
U16_GGGA(x1, x2, x3, x4, x5) = U16_GGGA(x1, x2, x3, x5)
NOTEQG_IN_GG(x1, x2) = NOTEQG_IN_GG(x1, x2)
U5_GG(x1, x2, x3) = U5_GG(x1, x2, x3)
U17_GGGA(x1, x2, x3, x4, x5) = U17_GGGA(x1, x2, x3, x5)
REMOVEK_IN_GGA(x1, x2, x3) = REMOVEK_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3, x4, x5) = U9_GGA(x1, x2, x3, x5)
U13_GGGAA(x1, x2, x3, x4, x5, x6) = U13_GGGAA(x1, x2, x3, x4, x6)

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

(4) Obligation:

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

MINSORTA_IN_GA(.(T25, T26), .(T27, T28)) → U1_GA(T25, T26, T27, T28, pB_in_gagaa(T25, T27, T26, X17, T28))
MINSORTA_IN_GA(.(T25, T26), .(T27, T28)) → PB_IN_GAGAA(T25, T27, T26, X17, T28)
PB_IN_GAGAA(T25, T31, T26, X17, T32) → U10_GAGAA(T25, T31, T26, X17, T32, min2C_in_gag(T25, T31, T26))
PB_IN_GAGAA(T25, T31, T26, X17, T32) → MIN2C_IN_GAG(T25, T31, T26)
MIN2C_IN_GAG(T48, T52, .(T50, T51)) → U2_GAG(T48, T52, T50, T51, pD_in_ggaag(T48, T50, X49, T52, T51))
MIN2C_IN_GAG(T48, T52, .(T50, T51)) → PD_IN_GGAAG(T48, T50, X49, T52, T51)
PD_IN_GGAAG(T48, T50, T55, T52, T51) → U14_GGAAG(T48, T50, T55, T52, T51, minJ_in_gga(T48, T50, T55))
PD_IN_GGAAG(T48, T50, T55, T52, T51) → MINJ_IN_GGA(T48, T50, T55)
MINJ_IN_GGA(T70, T71, T70) → U7_GGA(T70, T71, leE_in_gg(T70, T71))
MINJ_IN_GGA(T70, T71, T70) → LEE_IN_GG(T70, T71)
LEE_IN_GG(s(T82), s(T83)) → U3_GG(T82, T83, leE_in_gg(T82, T83))
LEE_IN_GG(s(T82), s(T83)) → LEE_IN_GG(T82, T83)
MINJ_IN_GGA(T97, T98, T98) → U8_GGA(T97, T98, gtF_in_gg(T97, T98))
MINJ_IN_GGA(T97, T98, T98) → GTF_IN_GG(T97, T98)
GTF_IN_GG(s(T109), s(T110)) → U4_GG(T109, T110, gtF_in_gg(T109, T110))
GTF_IN_GG(s(T109), s(T110)) → GTF_IN_GG(T109, T110)
U14_GGAAG(T48, T50, T55, T52, T51, minJ_out_gga(T48, T50, T55)) → U15_GGAAG(T48, T50, T55, T52, T51, min2C_in_gag(T55, T52, T51))
U14_GGAAG(T48, T50, T55, T52, T51, minJ_out_gga(T48, T50, T55)) → MIN2C_IN_GAG(T55, T52, T51)
U10_GAGAA(T25, T31, T26, X17, T32, min2C_out_gag(T25, T31, T26)) → U11_GAGAA(T25, T31, T26, X17, T32, pL_in_gggaa(T31, T25, T26, X17, T32))
U10_GAGAA(T25, T31, T26, X17, T32, min2C_out_gag(T25, T31, T26)) → PL_IN_GGGAA(T31, T25, T26, X17, T32)
PL_IN_GGGAA(T31, T25, T26, T122, T32) → U12_GGGAA(T31, T25, T26, T122, T32, removeH_in_ggga(T31, T25, T26, T122))
PL_IN_GGGAA(T31, T25, T26, T122, T32) → REMOVEH_IN_GGGA(T31, T25, T26, T122)
REMOVEH_IN_GGGA(T145, T146, T147, .(T146, X148)) → U6_GGGA(T145, T146, T147, X148, pI_in_ggga(T145, T146, T147, X148))
REMOVEH_IN_GGGA(T145, T146, T147, .(T146, X148)) → PI_IN_GGGA(T145, T146, T147, X148)
PI_IN_GGGA(T145, T146, T147, X148) → U16_GGGA(T145, T146, T147, X148, notEqG_in_gg(T145, T146))
PI_IN_GGGA(T145, T146, T147, X148) → NOTEQG_IN_GG(T145, T146)
NOTEQG_IN_GG(s(T160), s(T161)) → U5_GG(T160, T161, notEqG_in_gg(T160, T161))
NOTEQG_IN_GG(s(T160), s(T161)) → NOTEQG_IN_GG(T160, T161)
U16_GGGA(T145, T146, T147, X148, notEqG_out_gg(T145, T146)) → U17_GGGA(T145, T146, T147, X148, removeK_in_gga(T145, T147, X148))
U16_GGGA(T145, T146, T147, X148, notEqG_out_gg(T145, T146)) → REMOVEK_IN_GGA(T145, T147, X148)
REMOVEK_IN_GGA(T192, .(T193, T194), .(T193, X201)) → U9_GGA(T192, T193, T194, X201, pI_in_ggga(T192, T193, T194, X201))
REMOVEK_IN_GGA(T192, .(T193, T194), .(T193, X201)) → PI_IN_GGGA(T192, T193, T194, X201)
U12_GGGAA(T31, T25, T26, T122, T32, removeH_out_ggga(T31, T25, T26, T122)) → U13_GGGAA(T31, T25, T26, T122, T32, minsortA_in_ga(T122, T32))
U12_GGGAA(T31, T25, T26, T122, T32, removeH_out_ggga(T31, T25, T26, T122)) → MINSORTA_IN_GA(T122, T32)

The TRS R consists of the following rules:

minsortA_in_ga([], []) → minsortA_out_ga([], [])
minsortA_in_ga(.(T25, T26), .(T27, T28)) → U1_ga(T25, T26, T27, T28, pB_in_gagaa(T25, T27, T26, X17, T28))
pB_in_gagaa(T25, T31, T26, X17, T32) → U10_gagaa(T25, T31, T26, X17, T32, min2C_in_gag(T25, T31, T26))
min2C_in_gag(T39, T39, []) → min2C_out_gag(T39, T39, [])
min2C_in_gag(T48, T52, .(T50, T51)) → U2_gag(T48, T52, T50, T51, pD_in_ggaag(T48, T50, X49, T52, T51))
pD_in_ggaag(T48, T50, T55, T52, T51) → U14_ggaag(T48, T50, T55, T52, T51, minJ_in_gga(T48, T50, T55))
minJ_in_gga(T70, T71, T70) → U7_gga(T70, T71, leE_in_gg(T70, T71))
leE_in_gg(s(T82), s(T83)) → U3_gg(T82, T83, leE_in_gg(T82, T83))
leE_in_gg(0, s(T90)) → leE_out_gg(0, s(T90))
leE_in_gg(0, 0) → leE_out_gg(0, 0)
U3_gg(T82, T83, leE_out_gg(T82, T83)) → leE_out_gg(s(T82), s(T83))
U7_gga(T70, T71, leE_out_gg(T70, T71)) → minJ_out_gga(T70, T71, T70)
minJ_in_gga(T97, T98, T98) → U8_gga(T97, T98, gtF_in_gg(T97, T98))
gtF_in_gg(s(T109), s(T110)) → U4_gg(T109, T110, gtF_in_gg(T109, T110))
gtF_in_gg(s(T115), 0) → gtF_out_gg(s(T115), 0)
U4_gg(T109, T110, gtF_out_gg(T109, T110)) → gtF_out_gg(s(T109), s(T110))
U8_gga(T97, T98, gtF_out_gg(T97, T98)) → minJ_out_gga(T97, T98, T98)
U14_ggaag(T48, T50, T55, T52, T51, minJ_out_gga(T48, T50, T55)) → U15_ggaag(T48, T50, T55, T52, T51, min2C_in_gag(T55, T52, T51))
U15_ggaag(T48, T50, T55, T52, T51, min2C_out_gag(T55, T52, T51)) → pD_out_ggaag(T48, T50, T55, T52, T51)
U2_gag(T48, T52, T50, T51, pD_out_ggaag(T48, T50, X49, T52, T51)) → min2C_out_gag(T48, T52, .(T50, T51))
U10_gagaa(T25, T31, T26, X17, T32, min2C_out_gag(T25, T31, T26)) → U11_gagaa(T25, T31, T26, X17, T32, pL_in_gggaa(T31, T25, T26, X17, T32))
pL_in_gggaa(T31, T25, T26, T122, T32) → U12_gggaa(T31, T25, T26, T122, T32, removeH_in_ggga(T31, T25, T26, T122))
removeH_in_ggga(T135, T135, T136, T136) → removeH_out_ggga(T135, T135, T136, T136)
removeH_in_ggga(T145, T146, T147, .(T146, X148)) → U6_ggga(T145, T146, T147, X148, pI_in_ggga(T145, T146, T147, X148))
pI_in_ggga(T145, T146, T147, X148) → U16_ggga(T145, T146, T147, X148, notEqG_in_gg(T145, T146))
notEqG_in_gg(s(T160), s(T161)) → U5_gg(T160, T161, notEqG_in_gg(T160, T161))
notEqG_in_gg(s(T168), 0) → notEqG_out_gg(s(T168), 0)
notEqG_in_gg(0, s(T171)) → notEqG_out_gg(0, s(T171))
U5_gg(T160, T161, notEqG_out_gg(T160, T161)) → notEqG_out_gg(s(T160), s(T161))
U16_ggga(T145, T146, T147, X148, notEqG_out_gg(T145, T146)) → U17_ggga(T145, T146, T147, X148, removeK_in_gga(T145, T147, X148))
removeK_in_gga(T184, .(T184, T185), T185) → removeK_out_gga(T184, .(T184, T185), T185)
removeK_in_gga(T192, .(T193, T194), .(T193, X201)) → U9_gga(T192, T193, T194, X201, pI_in_ggga(T192, T193, T194, X201))
U9_gga(T192, T193, T194, X201, pI_out_ggga(T192, T193, T194, X201)) → removeK_out_gga(T192, .(T193, T194), .(T193, X201))
U17_ggga(T145, T146, T147, X148, removeK_out_gga(T145, T147, X148)) → pI_out_ggga(T145, T146, T147, X148)
U6_ggga(T145, T146, T147, X148, pI_out_ggga(T145, T146, T147, X148)) → removeH_out_ggga(T145, T146, T147, .(T146, X148))
U12_gggaa(T31, T25, T26, T122, T32, removeH_out_ggga(T31, T25, T26, T122)) → U13_gggaa(T31, T25, T26, T122, T32, minsortA_in_ga(T122, T32))
U13_gggaa(T31, T25, T26, T122, T32, minsortA_out_ga(T122, T32)) → pL_out_gggaa(T31, T25, T26, T122, T32)
U11_gagaa(T25, T31, T26, X17, T32, pL_out_gggaa(T31, T25, T26, X17, T32)) → pB_out_gagaa(T25, T31, T26, X17, T32)
U1_ga(T25, T26, T27, T28, pB_out_gagaa(T25, T27, T26, X17, T28)) → minsortA_out_ga(.(T25, T26), .(T27, T28))

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

NOTEQG_IN_GG(s(T160), s(T161)) → NOTEQG_IN_GG(T160, T161)

The TRS R consists of the following rules:

minsortA_in_ga([], []) → minsortA_out_ga([], [])
minsortA_in_ga(.(T25, T26), .(T27, T28)) → U1_ga(T25, T26, T27, T28, pB_in_gagaa(T25, T27, T26, X17, T28))
pB_in_gagaa(T25, T31, T26, X17, T32) → U10_gagaa(T25, T31, T26, X17, T32, min2C_in_gag(T25, T31, T26))
min2C_in_gag(T39, T39, []) → min2C_out_gag(T39, T39, [])
min2C_in_gag(T48, T52, .(T50, T51)) → U2_gag(T48, T52, T50, T51, pD_in_ggaag(T48, T50, X49, T52, T51))
pD_in_ggaag(T48, T50, T55, T52, T51) → U14_ggaag(T48, T50, T55, T52, T51, minJ_in_gga(T48, T50, T55))
minJ_in_gga(T70, T71, T70) → U7_gga(T70, T71, leE_in_gg(T70, T71))
leE_in_gg(s(T82), s(T83)) → U3_gg(T82, T83, leE_in_gg(T82, T83))
leE_in_gg(0, s(T90)) → leE_out_gg(0, s(T90))
leE_in_gg(0, 0) → leE_out_gg(0, 0)
U3_gg(T82, T83, leE_out_gg(T82, T83)) → leE_out_gg(s(T82), s(T83))
U7_gga(T70, T71, leE_out_gg(T70, T71)) → minJ_out_gga(T70, T71, T70)
minJ_in_gga(T97, T98, T98) → U8_gga(T97, T98, gtF_in_gg(T97, T98))
gtF_in_gg(s(T109), s(T110)) → U4_gg(T109, T110, gtF_in_gg(T109, T110))
gtF_in_gg(s(T115), 0) → gtF_out_gg(s(T115), 0)
U4_gg(T109, T110, gtF_out_gg(T109, T110)) → gtF_out_gg(s(T109), s(T110))
U8_gga(T97, T98, gtF_out_gg(T97, T98)) → minJ_out_gga(T97, T98, T98)
U14_ggaag(T48, T50, T55, T52, T51, minJ_out_gga(T48, T50, T55)) → U15_ggaag(T48, T50, T55, T52, T51, min2C_in_gag(T55, T52, T51))
U15_ggaag(T48, T50, T55, T52, T51, min2C_out_gag(T55, T52, T51)) → pD_out_ggaag(T48, T50, T55, T52, T51)
U2_gag(T48, T52, T50, T51, pD_out_ggaag(T48, T50, X49, T52, T51)) → min2C_out_gag(T48, T52, .(T50, T51))
U10_gagaa(T25, T31, T26, X17, T32, min2C_out_gag(T25, T31, T26)) → U11_gagaa(T25, T31, T26, X17, T32, pL_in_gggaa(T31, T25, T26, X17, T32))
pL_in_gggaa(T31, T25, T26, T122, T32) → U12_gggaa(T31, T25, T26, T122, T32, removeH_in_ggga(T31, T25, T26, T122))
removeH_in_ggga(T135, T135, T136, T136) → removeH_out_ggga(T135, T135, T136, T136)
removeH_in_ggga(T145, T146, T147, .(T146, X148)) → U6_ggga(T145, T146, T147, X148, pI_in_ggga(T145, T146, T147, X148))
pI_in_ggga(T145, T146, T147, X148) → U16_ggga(T145, T146, T147, X148, notEqG_in_gg(T145, T146))
notEqG_in_gg(s(T160), s(T161)) → U5_gg(T160, T161, notEqG_in_gg(T160, T161))
notEqG_in_gg(s(T168), 0) → notEqG_out_gg(s(T168), 0)
notEqG_in_gg(0, s(T171)) → notEqG_out_gg(0, s(T171))
U5_gg(T160, T161, notEqG_out_gg(T160, T161)) → notEqG_out_gg(s(T160), s(T161))
U16_ggga(T145, T146, T147, X148, notEqG_out_gg(T145, T146)) → U17_ggga(T145, T146, T147, X148, removeK_in_gga(T145, T147, X148))
removeK_in_gga(T184, .(T184, T185), T185) → removeK_out_gga(T184, .(T184, T185), T185)
removeK_in_gga(T192, .(T193, T194), .(T193, X201)) → U9_gga(T192, T193, T194, X201, pI_in_ggga(T192, T193, T194, X201))
U9_gga(T192, T193, T194, X201, pI_out_ggga(T192, T193, T194, X201)) → removeK_out_gga(T192, .(T193, T194), .(T193, X201))
U17_ggga(T145, T146, T147, X148, removeK_out_gga(T145, T147, X148)) → pI_out_ggga(T145, T146, T147, X148)
U6_ggga(T145, T146, T147, X148, pI_out_ggga(T145, T146, T147, X148)) → removeH_out_ggga(T145, T146, T147, .(T146, X148))
U12_gggaa(T31, T25, T26, T122, T32, removeH_out_ggga(T31, T25, T26, T122)) → U13_gggaa(T31, T25, T26, T122, T32, minsortA_in_ga(T122, T32))
U13_gggaa(T31, T25, T26, T122, T32, minsortA_out_ga(T122, T32)) → pL_out_gggaa(T31, T25, T26, T122, T32)
U11_gagaa(T25, T31, T26, X17, T32, pL_out_gggaa(T31, T25, T26, X17, T32)) → pB_out_gagaa(T25, T31, T26, X17, T32)
U1_ga(T25, T26, T27, T28, pB_out_gagaa(T25, T27, T26, X17, T28)) → minsortA_out_ga(.(T25, T26), .(T27, T28))

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

NOTEQG_IN_GG(s(T160), s(T161)) → NOTEQG_IN_GG(T160, T161)

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:

NOTEQG_IN_GG(s(T160), s(T161)) → NOTEQG_IN_GG(T160, T161)

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:

NOTEQG_IN_GG(s(T160), s(T161)) → NOTEQG_IN_GG(T160, T161)
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:

U16_GGGA(T145, T146, T147, X148, notEqG_out_gg(T145, T146)) → REMOVEK_IN_GGA(T145, T147, X148)
REMOVEK_IN_GGA(T192, .(T193, T194), .(T193, X201)) → PI_IN_GGGA(T192, T193, T194, X201)
PI_IN_GGGA(T145, T146, T147, X148) → U16_GGGA(T145, T146, T147, X148, notEqG_in_gg(T145, T146))

The TRS R consists of the following rules:

minsortA_in_ga([], []) → minsortA_out_ga([], [])
minsortA_in_ga(.(T25, T26), .(T27, T28)) → U1_ga(T25, T26, T27, T28, pB_in_gagaa(T25, T27, T26, X17, T28))
pB_in_gagaa(T25, T31, T26, X17, T32) → U10_gagaa(T25, T31, T26, X17, T32, min2C_in_gag(T25, T31, T26))
min2C_in_gag(T39, T39, []) → min2C_out_gag(T39, T39, [])
min2C_in_gag(T48, T52, .(T50, T51)) → U2_gag(T48, T52, T50, T51, pD_in_ggaag(T48, T50, X49, T52, T51))
pD_in_ggaag(T48, T50, T55, T52, T51) → U14_ggaag(T48, T50, T55, T52, T51, minJ_in_gga(T48, T50, T55))
minJ_in_gga(T70, T71, T70) → U7_gga(T70, T71, leE_in_gg(T70, T71))
leE_in_gg(s(T82), s(T83)) → U3_gg(T82, T83, leE_in_gg(T82, T83))
leE_in_gg(0, s(T90)) → leE_out_gg(0, s(T90))
leE_in_gg(0, 0) → leE_out_gg(0, 0)
U3_gg(T82, T83, leE_out_gg(T82, T83)) → leE_out_gg(s(T82), s(T83))
U7_gga(T70, T71, leE_out_gg(T70, T71)) → minJ_out_gga(T70, T71, T70)
minJ_in_gga(T97, T98, T98) → U8_gga(T97, T98, gtF_in_gg(T97, T98))
gtF_in_gg(s(T109), s(T110)) → U4_gg(T109, T110, gtF_in_gg(T109, T110))
gtF_in_gg(s(T115), 0) → gtF_out_gg(s(T115), 0)
U4_gg(T109, T110, gtF_out_gg(T109, T110)) → gtF_out_gg(s(T109), s(T110))
U8_gga(T97, T98, gtF_out_gg(T97, T98)) → minJ_out_gga(T97, T98, T98)
U14_ggaag(T48, T50, T55, T52, T51, minJ_out_gga(T48, T50, T55)) → U15_ggaag(T48, T50, T55, T52, T51, min2C_in_gag(T55, T52, T51))
U15_ggaag(T48, T50, T55, T52, T51, min2C_out_gag(T55, T52, T51)) → pD_out_ggaag(T48, T50, T55, T52, T51)
U2_gag(T48, T52, T50, T51, pD_out_ggaag(T48, T50, X49, T52, T51)) → min2C_out_gag(T48, T52, .(T50, T51))
U10_gagaa(T25, T31, T26, X17, T32, min2C_out_gag(T25, T31, T26)) → U11_gagaa(T25, T31, T26, X17, T32, pL_in_gggaa(T31, T25, T26, X17, T32))
pL_in_gggaa(T31, T25, T26, T122, T32) → U12_gggaa(T31, T25, T26, T122, T32, removeH_in_ggga(T31, T25, T26, T122))
removeH_in_ggga(T135, T135, T136, T136) → removeH_out_ggga(T135, T135, T136, T136)
removeH_in_ggga(T145, T146, T147, .(T146, X148)) → U6_ggga(T145, T146, T147, X148, pI_in_ggga(T145, T146, T147, X148))
pI_in_ggga(T145, T146, T147, X148) → U16_ggga(T145, T146, T147, X148, notEqG_in_gg(T145, T146))
notEqG_in_gg(s(T160), s(T161)) → U5_gg(T160, T161, notEqG_in_gg(T160, T161))
notEqG_in_gg(s(T168), 0) → notEqG_out_gg(s(T168), 0)
notEqG_in_gg(0, s(T171)) → notEqG_out_gg(0, s(T171))
U5_gg(T160, T161, notEqG_out_gg(T160, T161)) → notEqG_out_gg(s(T160), s(T161))
U16_ggga(T145, T146, T147, X148, notEqG_out_gg(T145, T146)) → U17_ggga(T145, T146, T147, X148, removeK_in_gga(T145, T147, X148))
removeK_in_gga(T184, .(T184, T185), T185) → removeK_out_gga(T184, .(T184, T185), T185)
removeK_in_gga(T192, .(T193, T194), .(T193, X201)) → U9_gga(T192, T193, T194, X201, pI_in_ggga(T192, T193, T194, X201))
U9_gga(T192, T193, T194, X201, pI_out_ggga(T192, T193, T194, X201)) → removeK_out_gga(T192, .(T193, T194), .(T193, X201))
U17_ggga(T145, T146, T147, X148, removeK_out_gga(T145, T147, X148)) → pI_out_ggga(T145, T146, T147, X148)
U6_ggga(T145, T146, T147, X148, pI_out_ggga(T145, T146, T147, X148)) → removeH_out_ggga(T145, T146, T147, .(T146, X148))
U12_gggaa(T31, T25, T26, T122, T32, removeH_out_ggga(T31, T25, T26, T122)) → U13_gggaa(T31, T25, T26, T122, T32, minsortA_in_ga(T122, T32))
U13_gggaa(T31, T25, T26, T122, T32, minsortA_out_ga(T122, T32)) → pL_out_gggaa(T31, T25, T26, T122, T32)
U11_gagaa(T25, T31, T26, X17, T32, pL_out_gggaa(T31, T25, T26, X17, T32)) → pB_out_gagaa(T25, T31, T26, X17, T32)
U1_ga(T25, T26, T27, T28, pB_out_gagaa(T25, T27, T26, X17, T28)) → minsortA_out_ga(.(T25, T26), .(T27, T28))

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

U16_GGGA(T145, T146, T147, X148, notEqG_out_gg(T145, T146)) → REMOVEK_IN_GGA(T145, T147, X148)
REMOVEK_IN_GGA(T192, .(T193, T194), .(T193, X201)) → PI_IN_GGGA(T192, T193, T194, X201)
PI_IN_GGGA(T145, T146, T147, X148) → U16_GGGA(T145, T146, T147, X148, notEqG_in_gg(T145, T146))

The TRS R consists of the following rules:

notEqG_in_gg(s(T160), s(T161)) → U5_gg(T160, T161, notEqG_in_gg(T160, T161))
notEqG_in_gg(s(T168), 0) → notEqG_out_gg(s(T168), 0)
notEqG_in_gg(0, s(T171)) → notEqG_out_gg(0, s(T171))
U5_gg(T160, T161, notEqG_out_gg(T160, T161)) → notEqG_out_gg(s(T160), s(T161))

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
s(x1) = s(x1)
0 = 0
notEqG_in_gg(x1, x2) = notEqG_in_gg(x1, x2)
U5_gg(x1, x2, x3) = U5_gg(x1, x2, x3)
notEqG_out_gg(x1, x2) = notEqG_out_gg(x1, x2)
PI_IN_GGGA(x1, x2, x3, x4) = PI_IN_GGGA(x1, x2, x3)
U16_GGGA(x1, x2, x3, x4, x5) = U16_GGGA(x1, x2, x3, x5)
REMOVEK_IN_GGA(x1, x2, x3) = REMOVEK_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:

U16_GGGA(T145, T146, T147, notEqG_out_gg(T145, T146)) → REMOVEK_IN_GGA(T145, T147)
REMOVEK_IN_GGA(T192, .(T193, T194)) → PI_IN_GGGA(T192, T193, T194)
PI_IN_GGGA(T145, T146, T147) → U16_GGGA(T145, T146, T147, notEqG_in_gg(T145, T146))

The TRS R consists of the following rules:

notEqG_in_gg(s(T160), s(T161)) → U5_gg(T160, T161, notEqG_in_gg(T160, T161))
notEqG_in_gg(s(T168), 0) → notEqG_out_gg(s(T168), 0)
notEqG_in_gg(0, s(T171)) → notEqG_out_gg(0, s(T171))
U5_gg(T160, T161, notEqG_out_gg(T160, T161)) → notEqG_out_gg(s(T160), s(T161))

The set Q consists of the following terms:

notEqG_in_gg(x0, x1)
U5_gg(x0, x1, x2)

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:

REMOVEK_IN_GGA(T192, .(T193, T194)) → PI_IN_GGGA(T192, T193, T194)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3
PI_IN_GGGA(T145, T146, T147) → U16_GGGA(T145, T146, T147, notEqG_in_gg(T145, T146))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3
U16_GGGA(T145, T146, T147, notEqG_out_gg(T145, T146)) → REMOVEK_IN_GGA(T145, T147)
The graph contains the following edges 1 >= 1, 4 > 1, 3 >= 2

(20) YES

(21) Obligation:

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

GTF_IN_GG(s(T109), s(T110)) → GTF_IN_GG(T109, T110)

The TRS R consists of the following rules:

minsortA_in_ga([], []) → minsortA_out_ga([], [])
minsortA_in_ga(.(T25, T26), .(T27, T28)) → U1_ga(T25, T26, T27, T28, pB_in_gagaa(T25, T27, T26, X17, T28))
pB_in_gagaa(T25, T31, T26, X17, T32) → U10_gagaa(T25, T31, T26, X17, T32, min2C_in_gag(T25, T31, T26))
min2C_in_gag(T39, T39, []) → min2C_out_gag(T39, T39, [])
min2C_in_gag(T48, T52, .(T50, T51)) → U2_gag(T48, T52, T50, T51, pD_in_ggaag(T48, T50, X49, T52, T51))
pD_in_ggaag(T48, T50, T55, T52, T51) → U14_ggaag(T48, T50, T55, T52, T51, minJ_in_gga(T48, T50, T55))
minJ_in_gga(T70, T71, T70) → U7_gga(T70, T71, leE_in_gg(T70, T71))
leE_in_gg(s(T82), s(T83)) → U3_gg(T82, T83, leE_in_gg(T82, T83))
leE_in_gg(0, s(T90)) → leE_out_gg(0, s(T90))
leE_in_gg(0, 0) → leE_out_gg(0, 0)
U3_gg(T82, T83, leE_out_gg(T82, T83)) → leE_out_gg(s(T82), s(T83))
U7_gga(T70, T71, leE_out_gg(T70, T71)) → minJ_out_gga(T70, T71, T70)
minJ_in_gga(T97, T98, T98) → U8_gga(T97, T98, gtF_in_gg(T97, T98))
gtF_in_gg(s(T109), s(T110)) → U4_gg(T109, T110, gtF_in_gg(T109, T110))
gtF_in_gg(s(T115), 0) → gtF_out_gg(s(T115), 0)
U4_gg(T109, T110, gtF_out_gg(T109, T110)) → gtF_out_gg(s(T109), s(T110))
U8_gga(T97, T98, gtF_out_gg(T97, T98)) → minJ_out_gga(T97, T98, T98)
U14_ggaag(T48, T50, T55, T52, T51, minJ_out_gga(T48, T50, T55)) → U15_ggaag(T48, T50, T55, T52, T51, min2C_in_gag(T55, T52, T51))
U15_ggaag(T48, T50, T55, T52, T51, min2C_out_gag(T55, T52, T51)) → pD_out_ggaag(T48, T50, T55, T52, T51)
U2_gag(T48, T52, T50, T51, pD_out_ggaag(T48, T50, X49, T52, T51)) → min2C_out_gag(T48, T52, .(T50, T51))
U10_gagaa(T25, T31, T26, X17, T32, min2C_out_gag(T25, T31, T26)) → U11_gagaa(T25, T31, T26, X17, T32, pL_in_gggaa(T31, T25, T26, X17, T32))
pL_in_gggaa(T31, T25, T26, T122, T32) → U12_gggaa(T31, T25, T26, T122, T32, removeH_in_ggga(T31, T25, T26, T122))
removeH_in_ggga(T135, T135, T136, T136) → removeH_out_ggga(T135, T135, T136, T136)
removeH_in_ggga(T145, T146, T147, .(T146, X148)) → U6_ggga(T145, T146, T147, X148, pI_in_ggga(T145, T146, T147, X148))
pI_in_ggga(T145, T146, T147, X148) → U16_ggga(T145, T146, T147, X148, notEqG_in_gg(T145, T146))
notEqG_in_gg(s(T160), s(T161)) → U5_gg(T160, T161, notEqG_in_gg(T160, T161))
notEqG_in_gg(s(T168), 0) → notEqG_out_gg(s(T168), 0)
notEqG_in_gg(0, s(T171)) → notEqG_out_gg(0, s(T171))
U5_gg(T160, T161, notEqG_out_gg(T160, T161)) → notEqG_out_gg(s(T160), s(T161))
U16_ggga(T145, T146, T147, X148, notEqG_out_gg(T145, T146)) → U17_ggga(T145, T146, T147, X148, removeK_in_gga(T145, T147, X148))
removeK_in_gga(T184, .(T184, T185), T185) → removeK_out_gga(T184, .(T184, T185), T185)
removeK_in_gga(T192, .(T193, T194), .(T193, X201)) → U9_gga(T192, T193, T194, X201, pI_in_ggga(T192, T193, T194, X201))
U9_gga(T192, T193, T194, X201, pI_out_ggga(T192, T193, T194, X201)) → removeK_out_gga(T192, .(T193, T194), .(T193, X201))
U17_ggga(T145, T146, T147, X148, removeK_out_gga(T145, T147, X148)) → pI_out_ggga(T145, T146, T147, X148)
U6_ggga(T145, T146, T147, X148, pI_out_ggga(T145, T146, T147, X148)) → removeH_out_ggga(T145, T146, T147, .(T146, X148))
U12_gggaa(T31, T25, T26, T122, T32, removeH_out_ggga(T31, T25, T26, T122)) → U13_gggaa(T31, T25, T26, T122, T32, minsortA_in_ga(T122, T32))
U13_gggaa(T31, T25, T26, T122, T32, minsortA_out_ga(T122, T32)) → pL_out_gggaa(T31, T25, T26, T122, T32)
U11_gagaa(T25, T31, T26, X17, T32, pL_out_gggaa(T31, T25, T26, X17, T32)) → pB_out_gagaa(T25, T31, T26, X17, T32)
U1_ga(T25, T26, T27, T28, pB_out_gagaa(T25, T27, T26, X17, T28)) → minsortA_out_ga(.(T25, T26), .(T27, T28))

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

GTF_IN_GG(s(T109), s(T110)) → GTF_IN_GG(T109, T110)

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

(24) PiDPToQDPProof (EQUIVALENT transformation)

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

(25) Obligation:

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

GTF_IN_GG(s(T109), s(T110)) → GTF_IN_GG(T109, T110)

R is empty.
Q is empty.
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:

GTF_IN_GG(s(T109), s(T110)) → GTF_IN_GG(T109, T110)
The graph contains the following edges 1 > 1, 2 > 2

(27) YES

(28) Obligation:

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

LEE_IN_GG(s(T82), s(T83)) → LEE_IN_GG(T82, T83)

The TRS R consists of the following rules:

minsortA_in_ga([], []) → minsortA_out_ga([], [])
minsortA_in_ga(.(T25, T26), .(T27, T28)) → U1_ga(T25, T26, T27, T28, pB_in_gagaa(T25, T27, T26, X17, T28))
pB_in_gagaa(T25, T31, T26, X17, T32) → U10_gagaa(T25, T31, T26, X17, T32, min2C_in_gag(T25, T31, T26))
min2C_in_gag(T39, T39, []) → min2C_out_gag(T39, T39, [])
min2C_in_gag(T48, T52, .(T50, T51)) → U2_gag(T48, T52, T50, T51, pD_in_ggaag(T48, T50, X49, T52, T51))
pD_in_ggaag(T48, T50, T55, T52, T51) → U14_ggaag(T48, T50, T55, T52, T51, minJ_in_gga(T48, T50, T55))
minJ_in_gga(T70, T71, T70) → U7_gga(T70, T71, leE_in_gg(T70, T71))
leE_in_gg(s(T82), s(T83)) → U3_gg(T82, T83, leE_in_gg(T82, T83))
leE_in_gg(0, s(T90)) → leE_out_gg(0, s(T90))
leE_in_gg(0, 0) → leE_out_gg(0, 0)
U3_gg(T82, T83, leE_out_gg(T82, T83)) → leE_out_gg(s(T82), s(T83))
U7_gga(T70, T71, leE_out_gg(T70, T71)) → minJ_out_gga(T70, T71, T70)
minJ_in_gga(T97, T98, T98) → U8_gga(T97, T98, gtF_in_gg(T97, T98))
gtF_in_gg(s(T109), s(T110)) → U4_gg(T109, T110, gtF_in_gg(T109, T110))
gtF_in_gg(s(T115), 0) → gtF_out_gg(s(T115), 0)
U4_gg(T109, T110, gtF_out_gg(T109, T110)) → gtF_out_gg(s(T109), s(T110))
U8_gga(T97, T98, gtF_out_gg(T97, T98)) → minJ_out_gga(T97, T98, T98)
U14_ggaag(T48, T50, T55, T52, T51, minJ_out_gga(T48, T50, T55)) → U15_ggaag(T48, T50, T55, T52, T51, min2C_in_gag(T55, T52, T51))
U15_ggaag(T48, T50, T55, T52, T51, min2C_out_gag(T55, T52, T51)) → pD_out_ggaag(T48, T50, T55, T52, T51)
U2_gag(T48, T52, T50, T51, pD_out_ggaag(T48, T50, X49, T52, T51)) → min2C_out_gag(T48, T52, .(T50, T51))
U10_gagaa(T25, T31, T26, X17, T32, min2C_out_gag(T25, T31, T26)) → U11_gagaa(T25, T31, T26, X17, T32, pL_in_gggaa(T31, T25, T26, X17, T32))
pL_in_gggaa(T31, T25, T26, T122, T32) → U12_gggaa(T31, T25, T26, T122, T32, removeH_in_ggga(T31, T25, T26, T122))
removeH_in_ggga(T135, T135, T136, T136) → removeH_out_ggga(T135, T135, T136, T136)
removeH_in_ggga(T145, T146, T147, .(T146, X148)) → U6_ggga(T145, T146, T147, X148, pI_in_ggga(T145, T146, T147, X148))
pI_in_ggga(T145, T146, T147, X148) → U16_ggga(T145, T146, T147, X148, notEqG_in_gg(T145, T146))
notEqG_in_gg(s(T160), s(T161)) → U5_gg(T160, T161, notEqG_in_gg(T160, T161))
notEqG_in_gg(s(T168), 0) → notEqG_out_gg(s(T168), 0)
notEqG_in_gg(0, s(T171)) → notEqG_out_gg(0, s(T171))
U5_gg(T160, T161, notEqG_out_gg(T160, T161)) → notEqG_out_gg(s(T160), s(T161))
U16_ggga(T145, T146, T147, X148, notEqG_out_gg(T145, T146)) → U17_ggga(T145, T146, T147, X148, removeK_in_gga(T145, T147, X148))
removeK_in_gga(T184, .(T184, T185), T185) → removeK_out_gga(T184, .(T184, T185), T185)
removeK_in_gga(T192, .(T193, T194), .(T193, X201)) → U9_gga(T192, T193, T194, X201, pI_in_ggga(T192, T193, T194, X201))
U9_gga(T192, T193, T194, X201, pI_out_ggga(T192, T193, T194, X201)) → removeK_out_gga(T192, .(T193, T194), .(T193, X201))
U17_ggga(T145, T146, T147, X148, removeK_out_gga(T145, T147, X148)) → pI_out_ggga(T145, T146, T147, X148)
U6_ggga(T145, T146, T147, X148, pI_out_ggga(T145, T146, T147, X148)) → removeH_out_ggga(T145, T146, T147, .(T146, X148))
U12_gggaa(T31, T25, T26, T122, T32, removeH_out_ggga(T31, T25, T26, T122)) → U13_gggaa(T31, T25, T26, T122, T32, minsortA_in_ga(T122, T32))
U13_gggaa(T31, T25, T26, T122, T32, minsortA_out_ga(T122, T32)) → pL_out_gggaa(T31, T25, T26, T122, T32)
U11_gagaa(T25, T31, T26, X17, T32, pL_out_gggaa(T31, T25, T26, X17, T32)) → pB_out_gagaa(T25, T31, T26, X17, T32)
U1_ga(T25, T26, T27, T28, pB_out_gagaa(T25, T27, T26, X17, T28)) → minsortA_out_ga(.(T25, T26), .(T27, T28))

(29) UsableRulesProof (EQUIVALENT transformation)

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

(30) Obligation:

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

LEE_IN_GG(s(T82), s(T83)) → LEE_IN_GG(T82, T83)

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

(31) PiDPToQDPProof (EQUIVALENT transformation)

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

(32) Obligation:

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

LEE_IN_GG(s(T82), s(T83)) → LEE_IN_GG(T82, T83)

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

(33) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

LEE_IN_GG(s(T82), s(T83)) → LEE_IN_GG(T82, T83)
The graph contains the following edges 1 > 1, 2 > 2

(34) YES

(35) Obligation:

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

MIN2C_IN_GAG(T48, T52, .(T50, T51)) → PD_IN_GGAAG(T48, T50, X49, T52, T51)
PD_IN_GGAAG(T48, T50, T55, T52, T51) → U14_GGAAG(T48, T50, T55, T52, T51, minJ_in_gga(T48, T50, T55))
U14_GGAAG(T48, T50, T55, T52, T51, minJ_out_gga(T48, T50, T55)) → MIN2C_IN_GAG(T55, T52, T51)

The TRS R consists of the following rules:

minsortA_in_ga([], []) → minsortA_out_ga([], [])
minsortA_in_ga(.(T25, T26), .(T27, T28)) → U1_ga(T25, T26, T27, T28, pB_in_gagaa(T25, T27, T26, X17, T28))
pB_in_gagaa(T25, T31, T26, X17, T32) → U10_gagaa(T25, T31, T26, X17, T32, min2C_in_gag(T25, T31, T26))
min2C_in_gag(T39, T39, []) → min2C_out_gag(T39, T39, [])
min2C_in_gag(T48, T52, .(T50, T51)) → U2_gag(T48, T52, T50, T51, pD_in_ggaag(T48, T50, X49, T52, T51))
pD_in_ggaag(T48, T50, T55, T52, T51) → U14_ggaag(T48, T50, T55, T52, T51, minJ_in_gga(T48, T50, T55))
minJ_in_gga(T70, T71, T70) → U7_gga(T70, T71, leE_in_gg(T70, T71))
leE_in_gg(s(T82), s(T83)) → U3_gg(T82, T83, leE_in_gg(T82, T83))
leE_in_gg(0, s(T90)) → leE_out_gg(0, s(T90))
leE_in_gg(0, 0) → leE_out_gg(0, 0)
U3_gg(T82, T83, leE_out_gg(T82, T83)) → leE_out_gg(s(T82), s(T83))
U7_gga(T70, T71, leE_out_gg(T70, T71)) → minJ_out_gga(T70, T71, T70)
minJ_in_gga(T97, T98, T98) → U8_gga(T97, T98, gtF_in_gg(T97, T98))
gtF_in_gg(s(T109), s(T110)) → U4_gg(T109, T110, gtF_in_gg(T109, T110))
gtF_in_gg(s(T115), 0) → gtF_out_gg(s(T115), 0)
U4_gg(T109, T110, gtF_out_gg(T109, T110)) → gtF_out_gg(s(T109), s(T110))
U8_gga(T97, T98, gtF_out_gg(T97, T98)) → minJ_out_gga(T97, T98, T98)
U14_ggaag(T48, T50, T55, T52, T51, minJ_out_gga(T48, T50, T55)) → U15_ggaag(T48, T50, T55, T52, T51, min2C_in_gag(T55, T52, T51))
U15_ggaag(T48, T50, T55, T52, T51, min2C_out_gag(T55, T52, T51)) → pD_out_ggaag(T48, T50, T55, T52, T51)
U2_gag(T48, T52, T50, T51, pD_out_ggaag(T48, T50, X49, T52, T51)) → min2C_out_gag(T48, T52, .(T50, T51))
U10_gagaa(T25, T31, T26, X17, T32, min2C_out_gag(T25, T31, T26)) → U11_gagaa(T25, T31, T26, X17, T32, pL_in_gggaa(T31, T25, T26, X17, T32))
pL_in_gggaa(T31, T25, T26, T122, T32) → U12_gggaa(T31, T25, T26, T122, T32, removeH_in_ggga(T31, T25, T26, T122))
removeH_in_ggga(T135, T135, T136, T136) → removeH_out_ggga(T135, T135, T136, T136)
removeH_in_ggga(T145, T146, T147, .(T146, X148)) → U6_ggga(T145, T146, T147, X148, pI_in_ggga(T145, T146, T147, X148))
pI_in_ggga(T145, T146, T147, X148) → U16_ggga(T145, T146, T147, X148, notEqG_in_gg(T145, T146))
notEqG_in_gg(s(T160), s(T161)) → U5_gg(T160, T161, notEqG_in_gg(T160, T161))
notEqG_in_gg(s(T168), 0) → notEqG_out_gg(s(T168), 0)
notEqG_in_gg(0, s(T171)) → notEqG_out_gg(0, s(T171))
U5_gg(T160, T161, notEqG_out_gg(T160, T161)) → notEqG_out_gg(s(T160), s(T161))
U16_ggga(T145, T146, T147, X148, notEqG_out_gg(T145, T146)) → U17_ggga(T145, T146, T147, X148, removeK_in_gga(T145, T147, X148))
removeK_in_gga(T184, .(T184, T185), T185) → removeK_out_gga(T184, .(T184, T185), T185)
removeK_in_gga(T192, .(T193, T194), .(T193, X201)) → U9_gga(T192, T193, T194, X201, pI_in_ggga(T192, T193, T194, X201))
U9_gga(T192, T193, T194, X201, pI_out_ggga(T192, T193, T194, X201)) → removeK_out_gga(T192, .(T193, T194), .(T193, X201))
U17_ggga(T145, T146, T147, X148, removeK_out_gga(T145, T147, X148)) → pI_out_ggga(T145, T146, T147, X148)
U6_ggga(T145, T146, T147, X148, pI_out_ggga(T145, T146, T147, X148)) → removeH_out_ggga(T145, T146, T147, .(T146, X148))
U12_gggaa(T31, T25, T26, T122, T32, removeH_out_ggga(T31, T25, T26, T122)) → U13_gggaa(T31, T25, T26, T122, T32, minsortA_in_ga(T122, T32))
U13_gggaa(T31, T25, T26, T122, T32, minsortA_out_ga(T122, T32)) → pL_out_gggaa(T31, T25, T26, T122, T32)
U11_gagaa(T25, T31, T26, X17, T32, pL_out_gggaa(T31, T25, T26, X17, T32)) → pB_out_gagaa(T25, T31, T26, X17, T32)
U1_ga(T25, T26, T27, T28, pB_out_gagaa(T25, T27, T26, X17, T28)) → minsortA_out_ga(.(T25, T26), .(T27, T28))

(36) UsableRulesProof (EQUIVALENT transformation)

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

(37) Obligation:

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

MIN2C_IN_GAG(T48, T52, .(T50, T51)) → PD_IN_GGAAG(T48, T50, X49, T52, T51)
PD_IN_GGAAG(T48, T50, T55, T52, T51) → U14_GGAAG(T48, T50, T55, T52, T51, minJ_in_gga(T48, T50, T55))
U14_GGAAG(T48, T50, T55, T52, T51, minJ_out_gga(T48, T50, T55)) → MIN2C_IN_GAG(T55, T52, T51)

The TRS R consists of the following rules:

minJ_in_gga(T70, T71, T70) → U7_gga(T70, T71, leE_in_gg(T70, T71))
minJ_in_gga(T97, T98, T98) → U8_gga(T97, T98, gtF_in_gg(T97, T98))
U7_gga(T70, T71, leE_out_gg(T70, T71)) → minJ_out_gga(T70, T71, T70)
U8_gga(T97, T98, gtF_out_gg(T97, T98)) → minJ_out_gga(T97, T98, T98)
leE_in_gg(s(T82), s(T83)) → U3_gg(T82, T83, leE_in_gg(T82, T83))
leE_in_gg(0, s(T90)) → leE_out_gg(0, s(T90))
leE_in_gg(0, 0) → leE_out_gg(0, 0)
gtF_in_gg(s(T109), s(T110)) → U4_gg(T109, T110, gtF_in_gg(T109, T110))
gtF_in_gg(s(T115), 0) → gtF_out_gg(s(T115), 0)
U3_gg(T82, T83, leE_out_gg(T82, T83)) → leE_out_gg(s(T82), s(T83))
U4_gg(T109, T110, gtF_out_gg(T109, T110)) → gtF_out_gg(s(T109), s(T110))

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
minJ_in_gga(x1, x2, x3) = minJ_in_gga(x1, x2)
U7_gga(x1, x2, x3) = U7_gga(x1, x2, x3)
leE_in_gg(x1, x2) = leE_in_gg(x1, x2)
s(x1) = s(x1)
U3_gg(x1, x2, x3) = U3_gg(x1, x2, x3)
0 = 0
leE_out_gg(x1, x2) = leE_out_gg(x1, x2)
minJ_out_gga(x1, x2, x3) = minJ_out_gga(x1, x2, x3)
U8_gga(x1, x2, x3) = U8_gga(x1, x2, x3)
gtF_in_gg(x1, x2) = gtF_in_gg(x1, x2)
U4_gg(x1, x2, x3) = U4_gg(x1, x2, x3)
gtF_out_gg(x1, x2) = gtF_out_gg(x1, x2)
MIN2C_IN_GAG(x1, x2, x3) = MIN2C_IN_GAG(x1, x3)
PD_IN_GGAAG(x1, x2, x3, x4, x5) = PD_IN_GGAAG(x1, x2, x5)
U14_GGAAG(x1, x2, x3, x4, x5, x6) = U14_GGAAG(x1, x2, x5, x6)

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

(38) PiDPToQDPProof (SOUND transformation)

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

(39) Obligation:

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

MIN2C_IN_GAG(T48, .(T50, T51)) → PD_IN_GGAAG(T48, T50, T51)
PD_IN_GGAAG(T48, T50, T51) → U14_GGAAG(T48, T50, T51, minJ_in_gga(T48, T50))
U14_GGAAG(T48, T50, T51, minJ_out_gga(T48, T50, T55)) → MIN2C_IN_GAG(T55, T51)

The TRS R consists of the following rules:

minJ_in_gga(T70, T71) → U7_gga(T70, T71, leE_in_gg(T70, T71))
minJ_in_gga(T97, T98) → U8_gga(T97, T98, gtF_in_gg(T97, T98))
U7_gga(T70, T71, leE_out_gg(T70, T71)) → minJ_out_gga(T70, T71, T70)
U8_gga(T97, T98, gtF_out_gg(T97, T98)) → minJ_out_gga(T97, T98, T98)
leE_in_gg(s(T82), s(T83)) → U3_gg(T82, T83, leE_in_gg(T82, T83))
leE_in_gg(0, s(T90)) → leE_out_gg(0, s(T90))
leE_in_gg(0, 0) → leE_out_gg(0, 0)
gtF_in_gg(s(T109), s(T110)) → U4_gg(T109, T110, gtF_in_gg(T109, T110))
gtF_in_gg(s(T115), 0) → gtF_out_gg(s(T115), 0)
U3_gg(T82, T83, leE_out_gg(T82, T83)) → leE_out_gg(s(T82), s(T83))
U4_gg(T109, T110, gtF_out_gg(T109, T110)) → gtF_out_gg(s(T109), s(T110))

The set Q consists of the following terms:

minJ_in_gga(x0, x1)
U7_gga(x0, x1, x2)
U8_gga(x0, x1, x2)
leE_in_gg(x0, x1)
gtF_in_gg(x0, x1)
U3_gg(x0, x1, x2)
U4_gg(x0, x1, x2)

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

(40) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

PD_IN_GGAAG(T48, T50, T51) → U14_GGAAG(T48, T50, T51, minJ_in_gga(T48, T50))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3
U14_GGAAG(T48, T50, T51, minJ_out_gga(T48, T50, T55)) → MIN2C_IN_GAG(T55, T51)
The graph contains the following edges 4 > 1, 3 >= 2
MIN2C_IN_GAG(T48, .(T50, T51)) → PD_IN_GGAAG(T48, T50, T51)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

(41) YES

(42) Obligation:

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

MINSORTA_IN_GA(.(T25, T26), .(T27, T28)) → PB_IN_GAGAA(T25, T27, T26, X17, T28)
PB_IN_GAGAA(T25, T31, T26, X17, T32) → U10_GAGAA(T25, T31, T26, X17, T32, min2C_in_gag(T25, T31, T26))
U10_GAGAA(T25, T31, T26, X17, T32, min2C_out_gag(T25, T31, T26)) → PL_IN_GGGAA(T31, T25, T26, X17, T32)
PL_IN_GGGAA(T31, T25, T26, T122, T32) → U12_GGGAA(T31, T25, T26, T122, T32, removeH_in_ggga(T31, T25, T26, T122))
U12_GGGAA(T31, T25, T26, T122, T32, removeH_out_ggga(T31, T25, T26, T122)) → MINSORTA_IN_GA(T122, T32)

The TRS R consists of the following rules:

minsortA_in_ga([], []) → minsortA_out_ga([], [])
minsortA_in_ga(.(T25, T26), .(T27, T28)) → U1_ga(T25, T26, T27, T28, pB_in_gagaa(T25, T27, T26, X17, T28))
pB_in_gagaa(T25, T31, T26, X17, T32) → U10_gagaa(T25, T31, T26, X17, T32, min2C_in_gag(T25, T31, T26))
min2C_in_gag(T39, T39, []) → min2C_out_gag(T39, T39, [])
min2C_in_gag(T48, T52, .(T50, T51)) → U2_gag(T48, T52, T50, T51, pD_in_ggaag(T48, T50, X49, T52, T51))
pD_in_ggaag(T48, T50, T55, T52, T51) → U14_ggaag(T48, T50, T55, T52, T51, minJ_in_gga(T48, T50, T55))
minJ_in_gga(T70, T71, T70) → U7_gga(T70, T71, leE_in_gg(T70, T71))
leE_in_gg(s(T82), s(T83)) → U3_gg(T82, T83, leE_in_gg(T82, T83))
leE_in_gg(0, s(T90)) → leE_out_gg(0, s(T90))
leE_in_gg(0, 0) → leE_out_gg(0, 0)
U3_gg(T82, T83, leE_out_gg(T82, T83)) → leE_out_gg(s(T82), s(T83))
U7_gga(T70, T71, leE_out_gg(T70, T71)) → minJ_out_gga(T70, T71, T70)
minJ_in_gga(T97, T98, T98) → U8_gga(T97, T98, gtF_in_gg(T97, T98))
gtF_in_gg(s(T109), s(T110)) → U4_gg(T109, T110, gtF_in_gg(T109, T110))
gtF_in_gg(s(T115), 0) → gtF_out_gg(s(T115), 0)
U4_gg(T109, T110, gtF_out_gg(T109, T110)) → gtF_out_gg(s(T109), s(T110))
U8_gga(T97, T98, gtF_out_gg(T97, T98)) → minJ_out_gga(T97, T98, T98)
U14_ggaag(T48, T50, T55, T52, T51, minJ_out_gga(T48, T50, T55)) → U15_ggaag(T48, T50, T55, T52, T51, min2C_in_gag(T55, T52, T51))
U15_ggaag(T48, T50, T55, T52, T51, min2C_out_gag(T55, T52, T51)) → pD_out_ggaag(T48, T50, T55, T52, T51)
U2_gag(T48, T52, T50, T51, pD_out_ggaag(T48, T50, X49, T52, T51)) → min2C_out_gag(T48, T52, .(T50, T51))
U10_gagaa(T25, T31, T26, X17, T32, min2C_out_gag(T25, T31, T26)) → U11_gagaa(T25, T31, T26, X17, T32, pL_in_gggaa(T31, T25, T26, X17, T32))
pL_in_gggaa(T31, T25, T26, T122, T32) → U12_gggaa(T31, T25, T26, T122, T32, removeH_in_ggga(T31, T25, T26, T122))
removeH_in_ggga(T135, T135, T136, T136) → removeH_out_ggga(T135, T135, T136, T136)
removeH_in_ggga(T145, T146, T147, .(T146, X148)) → U6_ggga(T145, T146, T147, X148, pI_in_ggga(T145, T146, T147, X148))
pI_in_ggga(T145, T146, T147, X148) → U16_ggga(T145, T146, T147, X148, notEqG_in_gg(T145, T146))
notEqG_in_gg(s(T160), s(T161)) → U5_gg(T160, T161, notEqG_in_gg(T160, T161))
notEqG_in_gg(s(T168), 0) → notEqG_out_gg(s(T168), 0)
notEqG_in_gg(0, s(T171)) → notEqG_out_gg(0, s(T171))
U5_gg(T160, T161, notEqG_out_gg(T160, T161)) → notEqG_out_gg(s(T160), s(T161))
U16_ggga(T145, T146, T147, X148, notEqG_out_gg(T145, T146)) → U17_ggga(T145, T146, T147, X148, removeK_in_gga(T145, T147, X148))
removeK_in_gga(T184, .(T184, T185), T185) → removeK_out_gga(T184, .(T184, T185), T185)
removeK_in_gga(T192, .(T193, T194), .(T193, X201)) → U9_gga(T192, T193, T194, X201, pI_in_ggga(T192, T193, T194, X201))
U9_gga(T192, T193, T194, X201, pI_out_ggga(T192, T193, T194, X201)) → removeK_out_gga(T192, .(T193, T194), .(T193, X201))
U17_ggga(T145, T146, T147, X148, removeK_out_gga(T145, T147, X148)) → pI_out_ggga(T145, T146, T147, X148)
U6_ggga(T145, T146, T147, X148, pI_out_ggga(T145, T146, T147, X148)) → removeH_out_ggga(T145, T146, T147, .(T146, X148))
U12_gggaa(T31, T25, T26, T122, T32, removeH_out_ggga(T31, T25, T26, T122)) → U13_gggaa(T31, T25, T26, T122, T32, minsortA_in_ga(T122, T32))
U13_gggaa(T31, T25, T26, T122, T32, minsortA_out_ga(T122, T32)) → pL_out_gggaa(T31, T25, T26, T122, T32)
U11_gagaa(T25, T31, T26, X17, T32, pL_out_gggaa(T31, T25, T26, X17, T32)) → pB_out_gagaa(T25, T31, T26, X17, T32)
U1_ga(T25, T26, T27, T28, pB_out_gagaa(T25, T27, T26, X17, T28)) → minsortA_out_ga(.(T25, T26), .(T27, T28))

(43) UsableRulesProof (EQUIVALENT transformation)

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

(44) Obligation:

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

MINSORTA_IN_GA(.(T25, T26), .(T27, T28)) → PB_IN_GAGAA(T25, T27, T26, X17, T28)
PB_IN_GAGAA(T25, T31, T26, X17, T32) → U10_GAGAA(T25, T31, T26, X17, T32, min2C_in_gag(T25, T31, T26))
U10_GAGAA(T25, T31, T26, X17, T32, min2C_out_gag(T25, T31, T26)) → PL_IN_GGGAA(T31, T25, T26, X17, T32)
PL_IN_GGGAA(T31, T25, T26, T122, T32) → U12_GGGAA(T31, T25, T26, T122, T32, removeH_in_ggga(T31, T25, T26, T122))
U12_GGGAA(T31, T25, T26, T122, T32, removeH_out_ggga(T31, T25, T26, T122)) → MINSORTA_IN_GA(T122, T32)

The TRS R consists of the following rules:

min2C_in_gag(T39, T39, []) → min2C_out_gag(T39, T39, [])
min2C_in_gag(T48, T52, .(T50, T51)) → U2_gag(T48, T52, T50, T51, pD_in_ggaag(T48, T50, X49, T52, T51))
removeH_in_ggga(T135, T135, T136, T136) → removeH_out_ggga(T135, T135, T136, T136)
removeH_in_ggga(T145, T146, T147, .(T146, X148)) → U6_ggga(T145, T146, T147, X148, pI_in_ggga(T145, T146, T147, X148))
U2_gag(T48, T52, T50, T51, pD_out_ggaag(T48, T50, X49, T52, T51)) → min2C_out_gag(T48, T52, .(T50, T51))
U6_ggga(T145, T146, T147, X148, pI_out_ggga(T145, T146, T147, X148)) → removeH_out_ggga(T145, T146, T147, .(T146, X148))
pD_in_ggaag(T48, T50, T55, T52, T51) → U14_ggaag(T48, T50, T55, T52, T51, minJ_in_gga(T48, T50, T55))
pI_in_ggga(T145, T146, T147, X148) → U16_ggga(T145, T146, T147, X148, notEqG_in_gg(T145, T146))
U14_ggaag(T48, T50, T55, T52, T51, minJ_out_gga(T48, T50, T55)) → U15_ggaag(T48, T50, T55, T52, T51, min2C_in_gag(T55, T52, T51))
U16_ggga(T145, T146, T147, X148, notEqG_out_gg(T145, T146)) → U17_ggga(T145, T146, T147, X148, removeK_in_gga(T145, T147, X148))
minJ_in_gga(T70, T71, T70) → U7_gga(T70, T71, leE_in_gg(T70, T71))
minJ_in_gga(T97, T98, T98) → U8_gga(T97, T98, gtF_in_gg(T97, T98))
U15_ggaag(T48, T50, T55, T52, T51, min2C_out_gag(T55, T52, T51)) → pD_out_ggaag(T48, T50, T55, T52, T51)
notEqG_in_gg(s(T160), s(T161)) → U5_gg(T160, T161, notEqG_in_gg(T160, T161))
notEqG_in_gg(s(T168), 0) → notEqG_out_gg(s(T168), 0)
notEqG_in_gg(0, s(T171)) → notEqG_out_gg(0, s(T171))
U17_ggga(T145, T146, T147, X148, removeK_out_gga(T145, T147, X148)) → pI_out_ggga(T145, T146, T147, X148)
U7_gga(T70, T71, leE_out_gg(T70, T71)) → minJ_out_gga(T70, T71, T70)
U8_gga(T97, T98, gtF_out_gg(T97, T98)) → minJ_out_gga(T97, T98, T98)
U5_gg(T160, T161, notEqG_out_gg(T160, T161)) → notEqG_out_gg(s(T160), s(T161))
removeK_in_gga(T184, .(T184, T185), T185) → removeK_out_gga(T184, .(T184, T185), T185)
removeK_in_gga(T192, .(T193, T194), .(T193, X201)) → U9_gga(T192, T193, T194, X201, pI_in_ggga(T192, T193, T194, X201))
leE_in_gg(s(T82), s(T83)) → U3_gg(T82, T83, leE_in_gg(T82, T83))
leE_in_gg(0, s(T90)) → leE_out_gg(0, s(T90))
leE_in_gg(0, 0) → leE_out_gg(0, 0)
gtF_in_gg(s(T109), s(T110)) → U4_gg(T109, T110, gtF_in_gg(T109, T110))
gtF_in_gg(s(T115), 0) → gtF_out_gg(s(T115), 0)
U9_gga(T192, T193, T194, X201, pI_out_ggga(T192, T193, T194, X201)) → removeK_out_gga(T192, .(T193, T194), .(T193, X201))
U3_gg(T82, T83, leE_out_gg(T82, T83)) → leE_out_gg(s(T82), s(T83))
U4_gg(T109, T110, gtF_out_gg(T109, T110)) → gtF_out_gg(s(T109), s(T110))

The argument filtering Pi contains the following mapping:
[] = []
.(x1, x2) = .(x1, x2)
min2C_in_gag(x1, x2, x3) = min2C_in_gag(x1, x3)
min2C_out_gag(x1, x2, x3) = min2C_out_gag(x1, x2, x3)
U2_gag(x1, x2, x3, x4, x5) = U2_gag(x1, x3, x4, x5)
pD_in_ggaag(x1, x2, x3, x4, x5) = pD_in_ggaag(x1, x2, x5)
U14_ggaag(x1, x2, x3, x4, x5, x6) = U14_ggaag(x1, x2, x5, x6)
minJ_in_gga(x1, x2, x3) = minJ_in_gga(x1, x2)
U7_gga(x1, x2, x3) = U7_gga(x1, x2, x3)
leE_in_gg(x1, x2) = leE_in_gg(x1, x2)
s(x1) = s(x1)
U3_gg(x1, x2, x3) = U3_gg(x1, x2, x3)
0 = 0
leE_out_gg(x1, x2) = leE_out_gg(x1, x2)
minJ_out_gga(x1, x2, x3) = minJ_out_gga(x1, x2, x3)
U8_gga(x1, x2, x3) = U8_gga(x1, x2, x3)
gtF_in_gg(x1, x2) = gtF_in_gg(x1, x2)
U4_gg(x1, x2, x3) = U4_gg(x1, x2, x3)
gtF_out_gg(x1, x2) = gtF_out_gg(x1, x2)
U15_ggaag(x1, x2, x3, x4, x5, x6) = U15_ggaag(x1, x2, x3, x5, x6)
pD_out_ggaag(x1, x2, x3, x4, x5) = pD_out_ggaag(x1, x2, x3, x4, x5)
removeH_in_ggga(x1, x2, x3, x4) = removeH_in_ggga(x1, x2, x3)
removeH_out_ggga(x1, x2, x3, x4) = removeH_out_ggga(x1, x2, x3, x4)
U6_ggga(x1, x2, x3, x4, x5) = U6_ggga(x1, x2, x3, x5)
pI_in_ggga(x1, x2, x3, x4) = pI_in_ggga(x1, x2, x3)
U16_ggga(x1, x2, x3, x4, x5) = U16_ggga(x1, x2, x3, x5)
notEqG_in_gg(x1, x2) = notEqG_in_gg(x1, x2)
U5_gg(x1, x2, x3) = U5_gg(x1, x2, x3)
notEqG_out_gg(x1, x2) = notEqG_out_gg(x1, x2)
U17_ggga(x1, x2, x3, x4, x5) = U17_ggga(x1, x2, x3, x5)
removeK_in_gga(x1, x2, x3) = removeK_in_gga(x1, x2)
removeK_out_gga(x1, x2, x3) = removeK_out_gga(x1, x2, x3)
U9_gga(x1, x2, x3, x4, x5) = U9_gga(x1, x2, x3, x5)
pI_out_ggga(x1, x2, x3, x4) = pI_out_ggga(x1, x2, x3, x4)
MINSORTA_IN_GA(x1, x2) = MINSORTA_IN_GA(x1)
PB_IN_GAGAA(x1, x2, x3, x4, x5) = PB_IN_GAGAA(x1, x3)
U10_GAGAA(x1, x2, x3, x4, x5, x6) = U10_GAGAA(x1, x3, x6)
PL_IN_GGGAA(x1, x2, x3, x4, x5) = PL_IN_GGGAA(x1, x2, x3)
U12_GGGAA(x1, x2, x3, x4, x5, x6) = U12_GGGAA(x1, x2, x3, x6)

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

(45) PiDPToQDPProof (SOUND transformation)

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

(46) Obligation:

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

MINSORTA_IN_GA(.(T25, T26)) → PB_IN_GAGAA(T25, T26)
PB_IN_GAGAA(T25, T26) → U10_GAGAA(T25, T26, min2C_in_gag(T25, T26))
U10_GAGAA(T25, T26, min2C_out_gag(T25, T31, T26)) → PL_IN_GGGAA(T31, T25, T26)
PL_IN_GGGAA(T31, T25, T26) → U12_GGGAA(T31, T25, T26, removeH_in_ggga(T31, T25, T26))
U12_GGGAA(T31, T25, T26, removeH_out_ggga(T31, T25, T26, T122)) → MINSORTA_IN_GA(T122)

The TRS R consists of the following rules:

min2C_in_gag(T39, []) → min2C_out_gag(T39, T39, [])
min2C_in_gag(T48, .(T50, T51)) → U2_gag(T48, T50, T51, pD_in_ggaag(T48, T50, T51))
removeH_in_ggga(T135, T135, T136) → removeH_out_ggga(T135, T135, T136, T136)
removeH_in_ggga(T145, T146, T147) → U6_ggga(T145, T146, T147, pI_in_ggga(T145, T146, T147))
U2_gag(T48, T50, T51, pD_out_ggaag(T48, T50, X49, T52, T51)) → min2C_out_gag(T48, T52, .(T50, T51))
U6_ggga(T145, T146, T147, pI_out_ggga(T145, T146, T147, X148)) → removeH_out_ggga(T145, T146, T147, .(T146, X148))
pD_in_ggaag(T48, T50, T51) → U14_ggaag(T48, T50, T51, minJ_in_gga(T48, T50))
pI_in_ggga(T145, T146, T147) → U16_ggga(T145, T146, T147, notEqG_in_gg(T145, T146))
U14_ggaag(T48, T50, T51, minJ_out_gga(T48, T50, T55)) → U15_ggaag(T48, T50, T55, T51, min2C_in_gag(T55, T51))
U16_ggga(T145, T146, T147, notEqG_out_gg(T145, T146)) → U17_ggga(T145, T146, T147, removeK_in_gga(T145, T147))
minJ_in_gga(T70, T71) → U7_gga(T70, T71, leE_in_gg(T70, T71))
minJ_in_gga(T97, T98) → U8_gga(T97, T98, gtF_in_gg(T97, T98))
U15_ggaag(T48, T50, T55, T51, min2C_out_gag(T55, T52, T51)) → pD_out_ggaag(T48, T50, T55, T52, T51)
notEqG_in_gg(s(T160), s(T161)) → U5_gg(T160, T161, notEqG_in_gg(T160, T161))
notEqG_in_gg(s(T168), 0) → notEqG_out_gg(s(T168), 0)
notEqG_in_gg(0, s(T171)) → notEqG_out_gg(0, s(T171))
U17_ggga(T145, T146, T147, removeK_out_gga(T145, T147, X148)) → pI_out_ggga(T145, T146, T147, X148)
U7_gga(T70, T71, leE_out_gg(T70, T71)) → minJ_out_gga(T70, T71, T70)
U8_gga(T97, T98, gtF_out_gg(T97, T98)) → minJ_out_gga(T97, T98, T98)
U5_gg(T160, T161, notEqG_out_gg(T160, T161)) → notEqG_out_gg(s(T160), s(T161))
removeK_in_gga(T184, .(T184, T185)) → removeK_out_gga(T184, .(T184, T185), T185)
removeK_in_gga(T192, .(T193, T194)) → U9_gga(T192, T193, T194, pI_in_ggga(T192, T193, T194))
leE_in_gg(s(T82), s(T83)) → U3_gg(T82, T83, leE_in_gg(T82, T83))
leE_in_gg(0, s(T90)) → leE_out_gg(0, s(T90))
leE_in_gg(0, 0) → leE_out_gg(0, 0)
gtF_in_gg(s(T109), s(T110)) → U4_gg(T109, T110, gtF_in_gg(T109, T110))
gtF_in_gg(s(T115), 0) → gtF_out_gg(s(T115), 0)
U9_gga(T192, T193, T194, pI_out_ggga(T192, T193, T194, X201)) → removeK_out_gga(T192, .(T193, T194), .(T193, X201))
U3_gg(T82, T83, leE_out_gg(T82, T83)) → leE_out_gg(s(T82), s(T83))
U4_gg(T109, T110, gtF_out_gg(T109, T110)) → gtF_out_gg(s(T109), s(T110))

The set Q consists of the following terms:

min2C_in_gag(x0, x1)
removeH_in_ggga(x0, x1, x2)
U2_gag(x0, x1, x2, x3)
U6_ggga(x0, x1, x2, x3)
pD_in_ggaag(x0, x1, x2)
pI_in_ggga(x0, x1, x2)
U14_ggaag(x0, x1, x2, x3)
U16_ggga(x0, x1, x2, x3)
minJ_in_gga(x0, x1)
U15_ggaag(x0, x1, x2, x3, x4)
notEqG_in_gg(x0, x1)
U17_ggga(x0, x1, x2, x3)
U7_gga(x0, x1, x2)
U8_gga(x0, x1, x2)
U5_gg(x0, x1, x2)
removeK_in_gga(x0, x1)
leE_in_gg(x0, x1)
gtF_in_gg(x0, x1)
U9_gga(x0, x1, x2, x3)
U3_gg(x0, x1, x2)
U4_gg(x0, x1, x2)

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

(47) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

PB_IN_GAGAA(T25, T26) → U10_GAGAA(T25, T26, min2C_in_gag(T25, T26))

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

POL(.(x₁, x₂)) = 1 + x₂
POL(0) = 0
POL(MINSORTA_IN_GA(x₁)) = x₁
POL(PB_IN_GAGAA(x₁, x₂)) = 1 + x₂
POL(PL_IN_GGGAA(x₁, x₂, x₃)) = x₃
POL(U10_GAGAA(x₁, x₂, x₃)) = x₂
POL(U12_GGGAA(x₁, x₂, x₃, x₄)) = x₄
POL(U14_ggaag(x₁, x₂, x₃, x₄)) = 0
POL(U15_ggaag(x₁, x₂, x₃, x₄, x₅)) = 0
POL(U16_ggga(x₁, x₂, x₃, x₄)) = x₃
POL(U17_ggga(x₁, x₂, x₃, x₄)) = x₄
POL(U2_gag(x₁, x₂, x₃, x₄)) = 0
POL(U3_gg(x₁, x₂, x₃)) = 0
POL(U4_gg(x₁, x₂, x₃)) = 0
POL(U5_gg(x₁, x₂, x₃)) = 0
POL(U6_ggga(x₁, x₂, x₃, x₄)) = x₄
POL(U7_gga(x₁, x₂, x₃)) = 1 + x₁ + x₃
POL(U8_gga(x₁, x₂, x₃)) = x₁ + x₂ + x₃
POL(U9_gga(x₁, x₂, x₃, x₄)) = 1 + x₄
POL([]) = 0
POL(gtF_in_gg(x₁, x₂)) = 0
POL(gtF_out_gg(x₁, x₂)) = 1 + x₁ + x₂
POL(leE_in_gg(x₁, x₂)) = 0
POL(leE_out_gg(x₁, x₂)) = 1 + x₁
POL(min2C_in_gag(x₁, x₂)) = 0
POL(min2C_out_gag(x₁, x₂, x₃)) = 0
POL(minJ_in_gga(x₁, x₂)) = 1 + x₁ + x₂
POL(minJ_out_gga(x₁, x₂, x₃)) = 1 + x₁ + x₃
POL(notEqG_in_gg(x₁, x₂)) = 0
POL(notEqG_out_gg(x₁, x₂)) = 0
POL(pD_in_ggaag(x₁, x₂, x₃)) = 0
POL(pD_out_ggaag(x₁, x₂, x₃, x₄, x₅)) = 0
POL(pI_in_ggga(x₁, x₂, x₃)) = x₃
POL(pI_out_ggga(x₁, x₂, x₃, x₄)) = 1 + x₄
POL(removeH_in_ggga(x₁, x₂, x₃)) = x₃
POL(removeH_out_ggga(x₁, x₂, x₃, x₄)) = x₄
POL(removeK_in_gga(x₁, x₂)) = x₂
POL(removeK_out_gga(x₁, x₂, x₃)) = 1 + x₃
POL(s(x₁)) = 0

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

removeH_in_ggga(T135, T135, T136) → removeH_out_ggga(T135, T135, T136, T136)
removeH_in_ggga(T145, T146, T147) → U6_ggga(T145, T146, T147, pI_in_ggga(T145, T146, T147))
pI_in_ggga(T145, T146, T147) → U16_ggga(T145, T146, T147, notEqG_in_gg(T145, T146))
U6_ggga(T145, T146, T147, pI_out_ggga(T145, T146, T147, X148)) → removeH_out_ggga(T145, T146, T147, .(T146, X148))
U16_ggga(T145, T146, T147, notEqG_out_gg(T145, T146)) → U17_ggga(T145, T146, T147, removeK_in_gga(T145, T147))
removeK_in_gga(T184, .(T184, T185)) → removeK_out_gga(T184, .(T184, T185), T185)
U17_ggga(T145, T146, T147, removeK_out_gga(T145, T147, X148)) → pI_out_ggga(T145, T146, T147, X148)
removeK_in_gga(T192, .(T193, T194)) → U9_gga(T192, T193, T194, pI_in_ggga(T192, T193, T194))
U9_gga(T192, T193, T194, pI_out_ggga(T192, T193, T194, X201)) → removeK_out_gga(T192, .(T193, T194), .(T193, X201))

(48) Obligation:

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

MINSORTA_IN_GA(.(T25, T26)) → PB_IN_GAGAA(T25, T26)
U10_GAGAA(T25, T26, min2C_out_gag(T25, T31, T26)) → PL_IN_GGGAA(T31, T25, T26)
PL_IN_GGGAA(T31, T25, T26) → U12_GGGAA(T31, T25, T26, removeH_in_ggga(T31, T25, T26))
U12_GGGAA(T31, T25, T26, removeH_out_ggga(T31, T25, T26, T122)) → MINSORTA_IN_GA(T122)

The TRS R consists of the following rules:

min2C_in_gag(T39, []) → min2C_out_gag(T39, T39, [])
min2C_in_gag(T48, .(T50, T51)) → U2_gag(T48, T50, T51, pD_in_ggaag(T48, T50, T51))
removeH_in_ggga(T135, T135, T136) → removeH_out_ggga(T135, T135, T136, T136)
removeH_in_ggga(T145, T146, T147) → U6_ggga(T145, T146, T147, pI_in_ggga(T145, T146, T147))
U2_gag(T48, T50, T51, pD_out_ggaag(T48, T50, X49, T52, T51)) → min2C_out_gag(T48, T52, .(T50, T51))
U6_ggga(T145, T146, T147, pI_out_ggga(T145, T146, T147, X148)) → removeH_out_ggga(T145, T146, T147, .(T146, X148))
pD_in_ggaag(T48, T50, T51) → U14_ggaag(T48, T50, T51, minJ_in_gga(T48, T50))
pI_in_ggga(T145, T146, T147) → U16_ggga(T145, T146, T147, notEqG_in_gg(T145, T146))
U14_ggaag(T48, T50, T51, minJ_out_gga(T48, T50, T55)) → U15_ggaag(T48, T50, T55, T51, min2C_in_gag(T55, T51))
U16_ggga(T145, T146, T147, notEqG_out_gg(T145, T146)) → U17_ggga(T145, T146, T147, removeK_in_gga(T145, T147))
minJ_in_gga(T70, T71) → U7_gga(T70, T71, leE_in_gg(T70, T71))
minJ_in_gga(T97, T98) → U8_gga(T97, T98, gtF_in_gg(T97, T98))
U15_ggaag(T48, T50, T55, T51, min2C_out_gag(T55, T52, T51)) → pD_out_ggaag(T48, T50, T55, T52, T51)
notEqG_in_gg(s(T160), s(T161)) → U5_gg(T160, T161, notEqG_in_gg(T160, T161))
notEqG_in_gg(s(T168), 0) → notEqG_out_gg(s(T168), 0)
notEqG_in_gg(0, s(T171)) → notEqG_out_gg(0, s(T171))
U17_ggga(T145, T146, T147, removeK_out_gga(T145, T147, X148)) → pI_out_ggga(T145, T146, T147, X148)
U7_gga(T70, T71, leE_out_gg(T70, T71)) → minJ_out_gga(T70, T71, T70)
U8_gga(T97, T98, gtF_out_gg(T97, T98)) → minJ_out_gga(T97, T98, T98)
U5_gg(T160, T161, notEqG_out_gg(T160, T161)) → notEqG_out_gg(s(T160), s(T161))
removeK_in_gga(T184, .(T184, T185)) → removeK_out_gga(T184, .(T184, T185), T185)
removeK_in_gga(T192, .(T193, T194)) → U9_gga(T192, T193, T194, pI_in_ggga(T192, T193, T194))
leE_in_gg(s(T82), s(T83)) → U3_gg(T82, T83, leE_in_gg(T82, T83))
leE_in_gg(0, s(T90)) → leE_out_gg(0, s(T90))
leE_in_gg(0, 0) → leE_out_gg(0, 0)
gtF_in_gg(s(T109), s(T110)) → U4_gg(T109, T110, gtF_in_gg(T109, T110))
gtF_in_gg(s(T115), 0) → gtF_out_gg(s(T115), 0)
U9_gga(T192, T193, T194, pI_out_ggga(T192, T193, T194, X201)) → removeK_out_gga(T192, .(T193, T194), .(T193, X201))
U3_gg(T82, T83, leE_out_gg(T82, T83)) → leE_out_gg(s(T82), s(T83))
U4_gg(T109, T110, gtF_out_gg(T109, T110)) → gtF_out_gg(s(T109), s(T110))

The set Q consists of the following terms:

min2C_in_gag(x0, x1)
removeH_in_ggga(x0, x1, x2)
U2_gag(x0, x1, x2, x3)
U6_ggga(x0, x1, x2, x3)
pD_in_ggaag(x0, x1, x2)
pI_in_ggga(x0, x1, x2)
U14_ggaag(x0, x1, x2, x3)
U16_ggga(x0, x1, x2, x3)
minJ_in_gga(x0, x1)
U15_ggaag(x0, x1, x2, x3, x4)
notEqG_in_gg(x0, x1)
U17_ggga(x0, x1, x2, x3)
U7_gga(x0, x1, x2)
U8_gga(x0, x1, x2)
U5_gg(x0, x1, x2)
removeK_in_gga(x0, x1)
leE_in_gg(x0, x1)
gtF_in_gg(x0, x1)
U9_gga(x0, x1, x2, x3)
U3_gg(x0, x1, x2)
U4_gg(x0, x1, x2)

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

(49) DependencyGraphProof (EQUIVALENT transformation)

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

(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 (EQUIVALENT 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 (EQUIVALENT transformation)

(25) Obligation:

(26) QDPSizeChangeProof (EQUIVALENT transformation)

(27) YES

(28) Obligation:

(29) UsableRulesProof (EQUIVALENT transformation)

(30) Obligation:

(31) PiDPToQDPProof (EQUIVALENT transformation)

(32) Obligation:

(33) QDPSizeChangeProof (EQUIVALENT transformation)

(34) YES

(35) Obligation:

(36) UsableRulesProof (EQUIVALENT transformation)

(37) Obligation:

(38) PiDPToQDPProof (SOUND transformation)

(39) Obligation:

(40) QDPSizeChangeProof (EQUIVALENT transformation)

(41) YES

(42) Obligation:

(43) UsableRulesProof (EQUIVALENT transformation)

(44) Obligation:

(45) PiDPToQDPProof (SOUND transformation)

(46) Obligation:

(47) QDPOrderProof (EQUIVALENT transformation)

(48) Obligation:

(49) DependencyGraphProof (EQUIVALENT transformation)

(50) TRUE