Left Termination proof of /tmp/tmp9J7twH/slowsort-bf.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 217 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 278 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 13 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇔, 4 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 QDPOrderProof (⇔, 103 ms)

        ↳41 QDP

        ↳42 DependencyGraphProof (⇔, 0 ms)

        ↳43 TRUE

(0) Obligation:

Clauses:

ss(Xs, Ys) :- ','(perm(Xs, Ys), ordered(Ys)).
perm([], []).
perm(Xs, .(X, Ys)) :- ','(app(X1s, .(X, X2s), Xs), ','(app(X1s, X2s, Zs), perm(Zs, Ys))).
app([], X, X).
app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs).
ordered([]).
ordered(.(X1, [])).
ordered(.(X, .(Y, Xs))) :- ','(less(X, s(Y)), ordered(.(Y, Xs))).
less(0, s(X2)).
less(s(X), s(Y)) :- less(X, Y).

Query: ss(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: ss(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: ss(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(perm(T5, T7), ordered(T7))\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(perm(T5, T7), ordered(T7)), SCOPE: 2, CLAUSE: 1 | ','(perm(T5, T7), ordered(T7)), SCOPE: 2, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(perm(T5, T7), ordered(T7)), SCOPE: 2, CLAUSE: 1\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(perm(T5, T7), ordered(T7)), SCOPE: 2, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ordered([])\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ordered([]), SCOPE: 3, CLAUSE: 5 | ordered([]), SCOPE: 3, CLAUSE: 6 | ordered([]), SCOPE: 3, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: ordered([]), SCOPE: 3, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ordered([]), SCOPE: 3, CLAUSE: 6 | ordered([]), SCOPE: 3, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ordered([]), SCOPE: 3, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="B: ','(','(app(X23, .(T17, X24), T14), ','(app(X23, X24, X25), perm(X25, T18))), ordered(.(T17, T18)))\n\nT14 is ground\nX23 is free\nX24 is free\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="C: app(X23, .(T17, X24), T14)\n\nT14 is ground\nX23 is free\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="K: ','(','(app(T23, T24, X25), perm(X25, T25)), ordered(.(T26, T25)))\n\nT23 is ground\nT26 is ground\nT24 is ground\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: app(X23, .(T17, X24), T14), SCOPE: 4, CLAUSE: 3 | app(X23, .(T17, X24), T14), SCOPE: 4, CLAUSE: 4\n\nT14 is ground\nX23 is free\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: app(X23, .(T17, X24), T14), SCOPE: 4, CLAUSE: 3\n\nT14 is ground\nX23 is free\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: app(X23, .(T17, X24), T14), SCOPE: 4, CLAUSE: 4\n\nT14 is ground\nX23 is free\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: app(X63, .(T50, X64), T49)\n\nT49 is ground\nX63 is free\nX64 is free", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="D: app(T23, T24, X25)\n\nT23 is ground\nT24 is ground\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="L: ','(perm(T57, T25), ordered(.(T26, T25)))\n\nT26 is ground\nT57 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: app(T23, T24, X25), SCOPE: 5, CLAUSE: 3 | app(T23, T24, X25), SCOPE: 5, CLAUSE: 4\n\nT23 is ground\nT24 is ground\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: app(T23, T24, X25), SCOPE: 5, CLAUSE: 3\n\nT23 is ground\nT24 is ground\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: app(T23, T24, X25), SCOPE: 5, CLAUSE: 4\n\nT23 is ground\nT24 is ground\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: app(T72, T73, X92)\n\nT72 is ground\nT73 is ground\nX92 is free", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="E: perm(T57, T25)\n\nT57 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="G: ordered(.(T26, T76))\n\nT26 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: perm(T57, T25), SCOPE: 6, CLAUSE: 1 | perm(T57, T25), SCOPE: 6, CLAUSE: 2\n\nT57 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: perm(T57, T25), SCOPE: 6, CLAUSE: 1\n\nT57 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: perm(T57, T25), SCOPE: 6, CLAUSE: 2\n\nT57 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="F: ','(app(X107, .(T86, X108), T83), ','(app(X107, X108, X109), perm(X109, T87)))\n\nT83 is ground\nX107 is free\nX108 is free\nX109 is free", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: app(X107, .(T86, X108), T83)\n\nT83 is ground\nX107 is free\nX108 is free", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="M: ','(app(T92, T93, X109), perm(X109, T94))\n\nT92 is ground\nT93 is ground\nX109 is free", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: app(T92, T93, X109)\n\nT92 is ground\nT93 is ground\nX109 is free", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: perm(T101, T94)\n\nT101 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: ordered(.(T26, T76)), SCOPE: 7, CLAUSE: 5 | ordered(.(T26, T76)), SCOPE: 7, CLAUSE: 6 | ordered(.(T26, T76)), SCOPE: 7, CLAUSE: 7\n\nT26 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: ordered(.(T26, T76)), SCOPE: 7, CLAUSE: 6 | ordered(.(T26, T76)), SCOPE: 7, CLAUSE: 7\n\nT26 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: ordered(.(T26, T76)), SCOPE: 7, CLAUSE: 6\n\nT26 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: ordered(.(T26, T76)), SCOPE: 7, CLAUSE: 7\n\nT26 is ground\nT76 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="H: ','(less(T115, s(T116)), ordered(.(T116, T117)))\n\nT115 is ground\nT116 is ground\nT117 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
203 [label="J: less(T115, s(T116))\n\nT115 is ground\nT116 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: ordered(.(T116, T117))\n\nT116 is ground\nT117 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: less(T115, s(T116)), SCOPE: 8, CLAUSE: 8 | less(T115, s(T116)), SCOPE: 8, CLAUSE: 9\n\nT115 is ground\nT116 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: less(T115, s(T116)), SCOPE: 8, CLAUSE: 8\n\nT115 is ground\nT116 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: less(T115, s(T116)), SCOPE: 8, CLAUSE: 9\n\nT115 is ground\nT116 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
208 [label="208: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
211 [label="I: less(T131, T132)\n\nT131 is ground\nT132 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: less(T131, T132), SCOPE: 9, CLAUSE: 8 | less(T131, T132), SCOPE: 9, CLAUSE: 9\n\nT131 is ground\nT132 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: less(T131, T132), SCOPE: 9, CLAUSE: 8\n\nT131 is ground\nT132 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: less(T131, T132), SCOPE: 9, CLAUSE: 9\n\nT131 is ground\nT132 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: less(T144, T145)\n\nT144 is ground\nT145 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
220 [label="220: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 221 [arrowhead = none ];
221 -> 6;

222 [label="ONLY EVAL with clause\nss(X5, X6) :- ','(perm(X5, X6), ordered(X6)).\nand substitutionT1 -> T5,\nX5 -> T5,\nT2 -> T7,\nX6 -> T7,\nT6 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 222 [arrowhead = none ];
222 -> 7;

223 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
7 -> 223 [arrowhead = none ];
223 -> 9;

224 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
9 -> 224 [arrowhead = none ];
224 -> 12;

225 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
9 -> 225 [arrowhead = none ];
225 -> 13;

226 [label="EVAL with clause\nperm([], []).\nand substitutionT5 -> [],\nT7 -> []", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 226 [arrowhead = none ];
226 -> 16;

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

228 [label="EVAL with clause\nperm(X20, .(X21, X22)) :- ','(app(X23, .(X21, X24), X20), ','(app(X23, X24, X25), perm(X25, X22))).\nand substitutionT5 -> T14,\nX20 -> T14,\nX21 -> T17,\nX22 -> T18,\nT7 -> .(T17, T18),\nT15 -> T17,\nT16 -> T18", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 228 [arrowhead = none ];
228 -> 43;

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

230 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
16 -> 230 [arrowhead = none ];
230 -> 20;

231 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
20 -> 231 [arrowhead = none ];
231 -> 21;

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

233 [label="ONLY EVAL with clause\nordered([]).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
21 -> 233 [arrowhead = none ];
233 -> 23;

234 [label="BACKTRACK\nfor clause: ordered(.(X1, []))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
22 -> 234 [arrowhead = none ];
234 -> 27;

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

236 [label="BACKTRACK\nfor clause: ordered(.(X, .(Y, Xs))) :- ','(less(X, s(Y)), ordered(.(Y, Xs)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 236 [arrowhead = none ];
236 -> 28;

237 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
43 -> 237 [arrowhead = none ];
237 -> 48;

238 [label="SPLIT 2\nnew knowledge:\nT23 is ground\nT26 is ground\nT24 is ground\nT14 is ground\nreplacements:X23 -> T23,\nX24 -> T24,\nT18 -> T25,\nT17 -> T26", fontsize=14, style = filled, fillcolor = violet];
43 -> 238 [arrowhead = none ];
238 -> 49;

239 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
48 -> 239 [arrowhead = none ];
239 -> 52;

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

241 [label="SPLIT 2\nnew knowledge:\nT23 is ground\nT24 is ground\nT57 is ground\nreplacements:X25 -> T57", fontsize=14, style = filled, fillcolor = violet];
49 -> 241 [arrowhead = none ];
241 -> 82;

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

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

244 [label="EVAL with clause\napp([], X42, X42).\nand substitutionX23 -> [],\nT17 -> T39,\nX24 -> T40,\nX42 -> .(T39, T40),\nX43 -> T40,\nT14 -> .(T39, T40)", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 244 [arrowhead = none ];
244 -> 58;

245 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
53 -> 245 [arrowhead = none ];
245 -> 60;

246 [label="EVAL with clause\napp(.(X58, X59), X60, .(X58, X61)) :- app(X59, X60, X61).\nand substitutionX58 -> T48,\nX59 -> X63,\nX23 -> .(T48, X63),\nT17 -> T50,\nX24 -> X64,\nX60 -> .(T50, X64),\nX62 -> T48,\nX61 -> T49,\nT14 -> .(T48, T49),\nT47 -> T50", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 246 [arrowhead = none ];
246 -> 74;

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

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

249 [label="INSTANCE with matching:\nX23 -> X63\nT17 -> T50\nX24 -> X64\nT14 -> T49", fontsize=14, style = filled, fillcolor = lightgrey];
74 -> 249 [arrowhead = none , style=dashed];
249 -> 48[style=dashed];

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

251 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
82 -> 251 [arrowhead = none ];
251 -> 118;

252 [label="SPLIT 2\nnew knowledge:\nT57 is ground\nT76 is ground\nreplacements:T25 -> T76", fontsize=14, style = filled, fillcolor = violet];
82 -> 252 [arrowhead = none ];
252 -> 119;

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

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

255 [label="EVAL with clause\napp([], X77, X77).\nand substitutionT23 -> [],\nT24 -> T64,\nX77 -> T64,\nX25 -> T64", fontsize=14, style = filled, fillcolor = lightblue];
94 -> 255 [arrowhead = none ];
255 -> 101;

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

257 [label="EVAL with clause\napp(.(X88, X89), X90, .(X88, X91)) :- app(X89, X90, X91).\nand substitutionX88 -> T71,\nX89 -> T72,\nT23 -> .(T71, T72),\nT24 -> T73,\nX90 -> T73,\nX91 -> X92,\nX25 -> .(T71, X92)", fontsize=14, style = filled, fillcolor = lightblue];
96 -> 257 [arrowhead = none ];
257 -> 106;

258 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
96 -> 258 [arrowhead = none ];
258 -> 107;

259 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
101 -> 259 [arrowhead = none ];
259 -> 103;

260 [label="INSTANCE with matching:\nT23 -> T72\nT24 -> T73\nX25 -> X92", fontsize=14, style = filled, fillcolor = lightgrey];
106 -> 260 [arrowhead = none , style=dashed];
260 -> 81[style=dashed];

261 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
118 -> 261 [arrowhead = none ];
261 -> 120;

262 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
119 -> 262 [arrowhead = none ];
262 -> 182;

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

264 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
120 -> 264 [arrowhead = none ];
264 -> 122;

265 [label="EVAL with clause\nperm([], []).\nand substitutionT57 -> [],\nT25 -> []", fontsize=14, style = filled, fillcolor = lightblue];
121 -> 265 [arrowhead = none ];
265 -> 123;

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

267 [label="EVAL with clause\nperm(X104, .(X105, X106)) :- ','(app(X107, .(X105, X108), X104), ','(app(X107, X108, X109), perm(X109, X106))).\nand substitutionT57 -> T83,\nX104 -> T83,\nX105 -> T86,\nX106 -> T87,\nT25 -> .(T86, T87),\nT84 -> T86,\nT85 -> T87", fontsize=14, style = filled, fillcolor = lightblue];
122 -> 267 [arrowhead = none ];
267 -> 148;

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

269 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
123 -> 269 [arrowhead = none ];
269 -> 125;

270 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
148 -> 270 [arrowhead = none ];
270 -> 154;

271 [label="SPLIT 2\nnew knowledge:\nT92 is ground\nT86 is ground\nT93 is ground\nT83 is ground\nreplacements:X107 -> T92,\nX108 -> T93,\nT87 -> T94", fontsize=14, style = filled, fillcolor = violet];
148 -> 271 [arrowhead = none ];
271 -> 156;

272 [label="INSTANCE with matching:\nX23 -> X107\nT17 -> T86\nX24 -> X108\nT14 -> T83", fontsize=14, style = filled, fillcolor = lightgrey];
154 -> 272 [arrowhead = none , style=dashed];
272 -> 48[style=dashed];

273 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
156 -> 273 [arrowhead = none ];
273 -> 174;

274 [label="SPLIT 2\nnew knowledge:\nT92 is ground\nT93 is ground\nT101 is ground\nreplacements:X109 -> T101", fontsize=14, style = filled, fillcolor = violet];
156 -> 274 [arrowhead = none ];
274 -> 175;

275 [label="INSTANCE with matching:\nT23 -> T92\nT24 -> T93\nX25 -> X109", fontsize=14, style = filled, fillcolor = lightgrey];
174 -> 275 [arrowhead = none , style=dashed];
275 -> 81[style=dashed];

276 [label="INSTANCE with matching:\nT57 -> T101\nT25 -> T94", fontsize=14, style = filled, fillcolor = lightgrey];
175 -> 276 [arrowhead = none , style=dashed];
276 -> 118[style=dashed];

277 [label="BACKTRACK\nfor clause: ordered([])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
182 -> 277 [arrowhead = none ];
277 -> 185;

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

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

280 [label="EVAL with clause\nordered(.(X126, [])).\nand substitutionT26 -> T108,\nX126 -> T108,\nT76 -> []", fontsize=14, style = filled, fillcolor = lightblue];
196 -> 280 [arrowhead = none ];
280 -> 198;

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

282 [label="EVAL with clause\nordered(.(X133, .(X134, X135))) :- ','(less(X133, s(X134)), ordered(.(X134, X135))).\nand substitutionT26 -> T115,\nX133 -> T115,\nX134 -> T116,\nX135 -> T117,\nT76 -> .(T116, T117)", fontsize=14, style = filled, fillcolor = lightblue];
197 -> 282 [arrowhead = none ];
282 -> 201;

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

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

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

286 [label="SPLIT 2\nnew knowledge:\nT115 is ground\nT116 is ground", fontsize=14, style = filled, fillcolor = violet];
201 -> 286 [arrowhead = none ];
286 -> 204;

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

288 [label="INSTANCE with matching:\nT26 -> T116\nT76 -> T117", fontsize=14, style = filled, fillcolor = lightgrey];
204 -> 288 [arrowhead = none , style=dashed];
288 -> 119[style=dashed];

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

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

291 [label="EVAL with clause\nless(0, s(X144)).\nand substitutionT115 -> 0,\nT116 -> T126,\nX144 -> T126", fontsize=14, style = filled, fillcolor = lightblue];
206 -> 291 [arrowhead = none ];
291 -> 208;

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

293 [label="EVAL with clause\nless(s(X149), s(X150)) :- less(X149, X150).\nand substitutionX149 -> T131,\nT115 -> s(T131),\nT116 -> T132,\nX150 -> T132", fontsize=14, style = filled, fillcolor = lightblue];
207 -> 293 [arrowhead = none ];
293 -> 211;

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

295 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
208 -> 295 [arrowhead = none ];
295 -> 210;

296 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
211 -> 296 [arrowhead = none ];
296 -> 213;

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

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

299 [label="EVAL with clause\nless(0, s(X157)).\nand substitutionT131 -> 0,\nX157 -> T139,\nT132 -> s(T139)", fontsize=14, style = filled, fillcolor = lightblue];
214 -> 299 [arrowhead = none ];
299 -> 216;

300 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
214 -> 300 [arrowhead = none ];
300 -> 217;

301 [label="EVAL with clause\nless(s(X162), s(X163)) :- less(X162, X163).\nand substitutionX162 -> T144,\nT131 -> s(T144),\nX163 -> T145,\nT132 -> s(T145)", fontsize=14, style = filled, fillcolor = lightblue];
215 -> 301 [arrowhead = none ];
301 -> 219;

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

303 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
216 -> 303 [arrowhead = none ];
303 -> 218;

304 [label="INSTANCE with matching:\nT131 -> T144\nT132 -> T145", fontsize=14, style = filled, fillcolor = lightgrey];
219 -> 304 [arrowhead = none , style=dashed];
304 -> 211[style=dashed];

}

(2) Obligation:

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

ssA_in_ga([], []) → ssA_out_ga([], [])
ssA_in_ga(T14, .(T17, T18)) → U1_ga(T14, T17, T18, pB_in_aaagaa(X23, T17, X24, T14, X25, T18))
pB_in_aaagaa(T23, T26, T24, T14, X25, T25) → U8_aaagaa(T23, T26, T24, T14, X25, T25, appC_in_aaag(T23, T26, T24, T14))
appC_in_aaag([], T39, T40, .(T39, T40)) → appC_out_aaag([], T39, T40, .(T39, T40))
appC_in_aaag(.(T48, X63), T50, X64, .(T48, T49)) → U2_aaag(T48, X63, T50, X64, T49, appC_in_aaag(X63, T50, X64, T49))
U2_aaag(T48, X63, T50, X64, T49, appC_out_aaag(X63, T50, X64, T49)) → appC_out_aaag(.(T48, X63), T50, X64, .(T48, T49))
U8_aaagaa(T23, T26, T24, T14, X25, T25, appC_out_aaag(T23, T26, T24, T14)) → U9_aaagaa(T23, T26, T24, T14, X25, T25, pK_in_ggaag(T23, T24, X25, T25, T26))
pK_in_ggaag(T23, T24, T57, T25, T26) → U10_ggaag(T23, T24, T57, T25, T26, appD_in_gga(T23, T24, T57))
appD_in_gga([], T64, T64) → appD_out_gga([], T64, T64)
appD_in_gga(.(T71, T72), T73, .(T71, X92)) → U3_gga(T71, T72, T73, X92, appD_in_gga(T72, T73, X92))
U3_gga(T71, T72, T73, X92, appD_out_gga(T72, T73, X92)) → appD_out_gga(.(T71, T72), T73, .(T71, X92))
U10_ggaag(T23, T24, T57, T25, T26, appD_out_gga(T23, T24, T57)) → U11_ggaag(T23, T24, T57, T25, T26, pL_in_gag(T57, T25, T26))
pL_in_gag(T57, T76, T26) → U12_gag(T57, T76, T26, permE_in_ga(T57, T76))
permE_in_ga([], []) → permE_out_ga([], [])
permE_in_ga(T83, .(T86, T87)) → U4_ga(T83, T86, T87, pF_in_aaagaa(X107, T86, X108, T83, X109, T87))
pF_in_aaagaa(T92, T86, T93, T83, X109, T94) → U14_aaagaa(T92, T86, T93, T83, X109, T94, appC_in_aaag(T92, T86, T93, T83))
U14_aaagaa(T92, T86, T93, T83, X109, T94, appC_out_aaag(T92, T86, T93, T83)) → U15_aaagaa(T92, T86, T93, T83, X109, T94, pM_in_ggaa(T92, T93, X109, T94))
pM_in_ggaa(T92, T93, T101, T94) → U16_ggaa(T92, T93, T101, T94, appD_in_gga(T92, T93, T101))
U16_ggaa(T92, T93, T101, T94, appD_out_gga(T92, T93, T101)) → U17_ggaa(T92, T93, T101, T94, permE_in_ga(T101, T94))
U17_ggaa(T92, T93, T101, T94, permE_out_ga(T101, T94)) → pM_out_ggaa(T92, T93, T101, T94)
U15_aaagaa(T92, T86, T93, T83, X109, T94, pM_out_ggaa(T92, T93, X109, T94)) → pF_out_aaagaa(T92, T86, T93, T83, X109, T94)
U4_ga(T83, T86, T87, pF_out_aaagaa(X107, T86, X108, T83, X109, T87)) → permE_out_ga(T83, .(T86, T87))
U12_gag(T57, T76, T26, permE_out_ga(T57, T76)) → U13_gag(T57, T76, T26, orderedG_in_gg(T26, T76))
orderedG_in_gg(T108, []) → orderedG_out_gg(T108, [])
orderedG_in_gg(T115, .(T116, T117)) → U5_gg(T115, T116, T117, pH_in_ggg(T115, T116, T117))
pH_in_ggg(T115, T116, T117) → U18_ggg(T115, T116, T117, lessJ_in_gg(T115, T116))
lessJ_in_gg(0, T126) → lessJ_out_gg(0, T126)
lessJ_in_gg(s(T131), T132) → U7_gg(T131, T132, lessI_in_gg(T131, T132))
lessI_in_gg(0, s(T139)) → lessI_out_gg(0, s(T139))
lessI_in_gg(s(T144), s(T145)) → U6_gg(T144, T145, lessI_in_gg(T144, T145))
U6_gg(T144, T145, lessI_out_gg(T144, T145)) → lessI_out_gg(s(T144), s(T145))
U7_gg(T131, T132, lessI_out_gg(T131, T132)) → lessJ_out_gg(s(T131), T132)
U18_ggg(T115, T116, T117, lessJ_out_gg(T115, T116)) → U19_ggg(T115, T116, T117, orderedG_in_gg(T116, T117))
U19_ggg(T115, T116, T117, orderedG_out_gg(T116, T117)) → pH_out_ggg(T115, T116, T117)
U5_gg(T115, T116, T117, pH_out_ggg(T115, T116, T117)) → orderedG_out_gg(T115, .(T116, T117))
U13_gag(T57, T76, T26, orderedG_out_gg(T26, T76)) → pL_out_gag(T57, T76, T26)
U11_ggaag(T23, T24, T57, T25, T26, pL_out_gag(T57, T25, T26)) → pK_out_ggaag(T23, T24, T57, T25, T26)
U9_aaagaa(T23, T26, T24, T14, X25, T25, pK_out_ggaag(T23, T24, X25, T25, T26)) → pB_out_aaagaa(T23, T26, T24, T14, X25, T25)
U1_ga(T14, T17, T18, pB_out_aaagaa(X23, T17, X24, T14, X25, T18)) → ssA_out_ga(T14, .(T17, T18))

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

SSA_IN_GA(T14, .(T17, T18)) → U1_GA(T14, T17, T18, pB_in_aaagaa(X23, T17, X24, T14, X25, T18))
SSA_IN_GA(T14, .(T17, T18)) → PB_IN_AAAGAA(X23, T17, X24, T14, X25, T18)
PB_IN_AAAGAA(T23, T26, T24, T14, X25, T25) → U8_AAAGAA(T23, T26, T24, T14, X25, T25, appC_in_aaag(T23, T26, T24, T14))
PB_IN_AAAGAA(T23, T26, T24, T14, X25, T25) → APPC_IN_AAAG(T23, T26, T24, T14)
APPC_IN_AAAG(.(T48, X63), T50, X64, .(T48, T49)) → U2_AAAG(T48, X63, T50, X64, T49, appC_in_aaag(X63, T50, X64, T49))
APPC_IN_AAAG(.(T48, X63), T50, X64, .(T48, T49)) → APPC_IN_AAAG(X63, T50, X64, T49)
U8_AAAGAA(T23, T26, T24, T14, X25, T25, appC_out_aaag(T23, T26, T24, T14)) → U9_AAAGAA(T23, T26, T24, T14, X25, T25, pK_in_ggaag(T23, T24, X25, T25, T26))
U8_AAAGAA(T23, T26, T24, T14, X25, T25, appC_out_aaag(T23, T26, T24, T14)) → PK_IN_GGAAG(T23, T24, X25, T25, T26)
PK_IN_GGAAG(T23, T24, T57, T25, T26) → U10_GGAAG(T23, T24, T57, T25, T26, appD_in_gga(T23, T24, T57))
PK_IN_GGAAG(T23, T24, T57, T25, T26) → APPD_IN_GGA(T23, T24, T57)
APPD_IN_GGA(.(T71, T72), T73, .(T71, X92)) → U3_GGA(T71, T72, T73, X92, appD_in_gga(T72, T73, X92))
APPD_IN_GGA(.(T71, T72), T73, .(T71, X92)) → APPD_IN_GGA(T72, T73, X92)
U10_GGAAG(T23, T24, T57, T25, T26, appD_out_gga(T23, T24, T57)) → U11_GGAAG(T23, T24, T57, T25, T26, pL_in_gag(T57, T25, T26))
U10_GGAAG(T23, T24, T57, T25, T26, appD_out_gga(T23, T24, T57)) → PL_IN_GAG(T57, T25, T26)
PL_IN_GAG(T57, T76, T26) → U12_GAG(T57, T76, T26, permE_in_ga(T57, T76))
PL_IN_GAG(T57, T76, T26) → PERME_IN_GA(T57, T76)
PERME_IN_GA(T83, .(T86, T87)) → U4_GA(T83, T86, T87, pF_in_aaagaa(X107, T86, X108, T83, X109, T87))
PERME_IN_GA(T83, .(T86, T87)) → PF_IN_AAAGAA(X107, T86, X108, T83, X109, T87)
PF_IN_AAAGAA(T92, T86, T93, T83, X109, T94) → U14_AAAGAA(T92, T86, T93, T83, X109, T94, appC_in_aaag(T92, T86, T93, T83))
PF_IN_AAAGAA(T92, T86, T93, T83, X109, T94) → APPC_IN_AAAG(T92, T86, T93, T83)
U14_AAAGAA(T92, T86, T93, T83, X109, T94, appC_out_aaag(T92, T86, T93, T83)) → U15_AAAGAA(T92, T86, T93, T83, X109, T94, pM_in_ggaa(T92, T93, X109, T94))
U14_AAAGAA(T92, T86, T93, T83, X109, T94, appC_out_aaag(T92, T86, T93, T83)) → PM_IN_GGAA(T92, T93, X109, T94)
PM_IN_GGAA(T92, T93, T101, T94) → U16_GGAA(T92, T93, T101, T94, appD_in_gga(T92, T93, T101))
PM_IN_GGAA(T92, T93, T101, T94) → APPD_IN_GGA(T92, T93, T101)
U16_GGAA(T92, T93, T101, T94, appD_out_gga(T92, T93, T101)) → U17_GGAA(T92, T93, T101, T94, permE_in_ga(T101, T94))
U16_GGAA(T92, T93, T101, T94, appD_out_gga(T92, T93, T101)) → PERME_IN_GA(T101, T94)
U12_GAG(T57, T76, T26, permE_out_ga(T57, T76)) → U13_GAG(T57, T76, T26, orderedG_in_gg(T26, T76))
U12_GAG(T57, T76, T26, permE_out_ga(T57, T76)) → ORDEREDG_IN_GG(T26, T76)
ORDEREDG_IN_GG(T115, .(T116, T117)) → U5_GG(T115, T116, T117, pH_in_ggg(T115, T116, T117))
ORDEREDG_IN_GG(T115, .(T116, T117)) → PH_IN_GGG(T115, T116, T117)
PH_IN_GGG(T115, T116, T117) → U18_GGG(T115, T116, T117, lessJ_in_gg(T115, T116))
PH_IN_GGG(T115, T116, T117) → LESSJ_IN_GG(T115, T116)
LESSJ_IN_GG(s(T131), T132) → U7_GG(T131, T132, lessI_in_gg(T131, T132))
LESSJ_IN_GG(s(T131), T132) → LESSI_IN_GG(T131, T132)
LESSI_IN_GG(s(T144), s(T145)) → U6_GG(T144, T145, lessI_in_gg(T144, T145))
LESSI_IN_GG(s(T144), s(T145)) → LESSI_IN_GG(T144, T145)
U18_GGG(T115, T116, T117, lessJ_out_gg(T115, T116)) → U19_GGG(T115, T116, T117, orderedG_in_gg(T116, T117))
U18_GGG(T115, T116, T117, lessJ_out_gg(T115, T116)) → ORDEREDG_IN_GG(T116, T117)

The TRS R consists of the following rules:

ssA_in_ga([], []) → ssA_out_ga([], [])
ssA_in_ga(T14, .(T17, T18)) → U1_ga(T14, T17, T18, pB_in_aaagaa(X23, T17, X24, T14, X25, T18))
pB_in_aaagaa(T23, T26, T24, T14, X25, T25) → U8_aaagaa(T23, T26, T24, T14, X25, T25, appC_in_aaag(T23, T26, T24, T14))
appC_in_aaag([], T39, T40, .(T39, T40)) → appC_out_aaag([], T39, T40, .(T39, T40))
appC_in_aaag(.(T48, X63), T50, X64, .(T48, T49)) → U2_aaag(T48, X63, T50, X64, T49, appC_in_aaag(X63, T50, X64, T49))
U2_aaag(T48, X63, T50, X64, T49, appC_out_aaag(X63, T50, X64, T49)) → appC_out_aaag(.(T48, X63), T50, X64, .(T48, T49))
U8_aaagaa(T23, T26, T24, T14, X25, T25, appC_out_aaag(T23, T26, T24, T14)) → U9_aaagaa(T23, T26, T24, T14, X25, T25, pK_in_ggaag(T23, T24, X25, T25, T26))
pK_in_ggaag(T23, T24, T57, T25, T26) → U10_ggaag(T23, T24, T57, T25, T26, appD_in_gga(T23, T24, T57))
appD_in_gga([], T64, T64) → appD_out_gga([], T64, T64)
appD_in_gga(.(T71, T72), T73, .(T71, X92)) → U3_gga(T71, T72, T73, X92, appD_in_gga(T72, T73, X92))
U3_gga(T71, T72, T73, X92, appD_out_gga(T72, T73, X92)) → appD_out_gga(.(T71, T72), T73, .(T71, X92))
U10_ggaag(T23, T24, T57, T25, T26, appD_out_gga(T23, T24, T57)) → U11_ggaag(T23, T24, T57, T25, T26, pL_in_gag(T57, T25, T26))
pL_in_gag(T57, T76, T26) → U12_gag(T57, T76, T26, permE_in_ga(T57, T76))
permE_in_ga([], []) → permE_out_ga([], [])
permE_in_ga(T83, .(T86, T87)) → U4_ga(T83, T86, T87, pF_in_aaagaa(X107, T86, X108, T83, X109, T87))
pF_in_aaagaa(T92, T86, T93, T83, X109, T94) → U14_aaagaa(T92, T86, T93, T83, X109, T94, appC_in_aaag(T92, T86, T93, T83))
U14_aaagaa(T92, T86, T93, T83, X109, T94, appC_out_aaag(T92, T86, T93, T83)) → U15_aaagaa(T92, T86, T93, T83, X109, T94, pM_in_ggaa(T92, T93, X109, T94))
pM_in_ggaa(T92, T93, T101, T94) → U16_ggaa(T92, T93, T101, T94, appD_in_gga(T92, T93, T101))
U16_ggaa(T92, T93, T101, T94, appD_out_gga(T92, T93, T101)) → U17_ggaa(T92, T93, T101, T94, permE_in_ga(T101, T94))
U17_ggaa(T92, T93, T101, T94, permE_out_ga(T101, T94)) → pM_out_ggaa(T92, T93, T101, T94)
U15_aaagaa(T92, T86, T93, T83, X109, T94, pM_out_ggaa(T92, T93, X109, T94)) → pF_out_aaagaa(T92, T86, T93, T83, X109, T94)
U4_ga(T83, T86, T87, pF_out_aaagaa(X107, T86, X108, T83, X109, T87)) → permE_out_ga(T83, .(T86, T87))
U12_gag(T57, T76, T26, permE_out_ga(T57, T76)) → U13_gag(T57, T76, T26, orderedG_in_gg(T26, T76))
orderedG_in_gg(T108, []) → orderedG_out_gg(T108, [])
orderedG_in_gg(T115, .(T116, T117)) → U5_gg(T115, T116, T117, pH_in_ggg(T115, T116, T117))
pH_in_ggg(T115, T116, T117) → U18_ggg(T115, T116, T117, lessJ_in_gg(T115, T116))
lessJ_in_gg(0, T126) → lessJ_out_gg(0, T126)
lessJ_in_gg(s(T131), T132) → U7_gg(T131, T132, lessI_in_gg(T131, T132))
lessI_in_gg(0, s(T139)) → lessI_out_gg(0, s(T139))
lessI_in_gg(s(T144), s(T145)) → U6_gg(T144, T145, lessI_in_gg(T144, T145))
U6_gg(T144, T145, lessI_out_gg(T144, T145)) → lessI_out_gg(s(T144), s(T145))
U7_gg(T131, T132, lessI_out_gg(T131, T132)) → lessJ_out_gg(s(T131), T132)
U18_ggg(T115, T116, T117, lessJ_out_gg(T115, T116)) → U19_ggg(T115, T116, T117, orderedG_in_gg(T116, T117))
U19_ggg(T115, T116, T117, orderedG_out_gg(T116, T117)) → pH_out_ggg(T115, T116, T117)
U5_gg(T115, T116, T117, pH_out_ggg(T115, T116, T117)) → orderedG_out_gg(T115, .(T116, T117))
U13_gag(T57, T76, T26, orderedG_out_gg(T26, T76)) → pL_out_gag(T57, T76, T26)
U11_ggaag(T23, T24, T57, T25, T26, pL_out_gag(T57, T25, T26)) → pK_out_ggaag(T23, T24, T57, T25, T26)
U9_aaagaa(T23, T26, T24, T14, X25, T25, pK_out_ggaag(T23, T24, X25, T25, T26)) → pB_out_aaagaa(T23, T26, T24, T14, X25, T25)
U1_ga(T14, T17, T18, pB_out_aaagaa(X23, T17, X24, T14, X25, T18)) → ssA_out_ga(T14, .(T17, T18))

The argument filtering Pi contains the following mapping:
ssA_in_ga(x1, x2) = ssA_in_ga(x1)
[] = []
ssA_out_ga(x1, x2) = ssA_out_ga(x1, x2)
U1_ga(x1, x2, x3, x4) = U1_ga(x1, x4)
pB_in_aaagaa(x1, x2, x3, x4, x5, x6) = pB_in_aaagaa(x4)
U8_aaagaa(x1, x2, x3, x4, x5, x6, x7) = U8_aaagaa(x4, x7)
appC_in_aaag(x1, x2, x3, x4) = appC_in_aaag(x4)
.(x1, x2) = .(x1, x2)
appC_out_aaag(x1, x2, x3, x4) = appC_out_aaag(x1, x2, x3, x4)
U2_aaag(x1, x2, x3, x4, x5, x6) = U2_aaag(x1, x5, x6)
U9_aaagaa(x1, x2, x3, x4, x5, x6, x7) = U9_aaagaa(x1, x2, x3, x4, x7)
pK_in_ggaag(x1, x2, x3, x4, x5) = pK_in_ggaag(x1, x2, x5)
U10_ggaag(x1, x2, x3, x4, x5, x6) = U10_ggaag(x1, x2, x5, x6)
appD_in_gga(x1, x2, x3) = appD_in_gga(x1, x2)
appD_out_gga(x1, x2, x3) = appD_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5) = U3_gga(x1, x2, x3, x5)
U11_ggaag(x1, x2, x3, x4, x5, x6) = U11_ggaag(x1, x2, x3, x5, x6)
pL_in_gag(x1, x2, x3) = pL_in_gag(x1, x3)
U12_gag(x1, x2, x3, x4) = U12_gag(x1, x3, x4)
permE_in_ga(x1, x2) = permE_in_ga(x1)
permE_out_ga(x1, x2) = permE_out_ga(x1, x2)
U4_ga(x1, x2, x3, x4) = U4_ga(x1, x4)
pF_in_aaagaa(x1, x2, x3, x4, x5, x6) = pF_in_aaagaa(x4)
U14_aaagaa(x1, x2, x3, x4, x5, x6, x7) = U14_aaagaa(x4, x7)
U15_aaagaa(x1, x2, x3, x4, x5, x6, x7) = U15_aaagaa(x1, x2, x3, x4, x7)
pM_in_ggaa(x1, x2, x3, x4) = pM_in_ggaa(x1, x2)
U16_ggaa(x1, x2, x3, x4, x5) = U16_ggaa(x1, x2, x5)
U17_ggaa(x1, x2, x3, x4, x5) = U17_ggaa(x1, x2, x3, x5)
pM_out_ggaa(x1, x2, x3, x4) = pM_out_ggaa(x1, x2, x3, x4)
pF_out_aaagaa(x1, x2, x3, x4, x5, x6) = pF_out_aaagaa(x1, x2, x3, x4, x5, x6)
U13_gag(x1, x2, x3, x4) = U13_gag(x1, x2, x3, x4)
orderedG_in_gg(x1, x2) = orderedG_in_gg(x1, x2)
orderedG_out_gg(x1, x2) = orderedG_out_gg(x1, x2)
U5_gg(x1, x2, x3, x4) = U5_gg(x1, x2, x3, x4)
pH_in_ggg(x1, x2, x3) = pH_in_ggg(x1, x2, x3)
U18_ggg(x1, x2, x3, x4) = U18_ggg(x1, x2, x3, x4)
lessJ_in_gg(x1, x2) = lessJ_in_gg(x1, x2)
0 = 0
lessJ_out_gg(x1, x2) = lessJ_out_gg(x1, x2)
s(x1) = s(x1)
U7_gg(x1, x2, x3) = U7_gg(x1, x2, x3)
lessI_in_gg(x1, x2) = lessI_in_gg(x1, x2)
lessI_out_gg(x1, x2) = lessI_out_gg(x1, x2)
U6_gg(x1, x2, x3) = U6_gg(x1, x2, x3)
U19_ggg(x1, x2, x3, x4) = U19_ggg(x1, x2, x3, x4)
pH_out_ggg(x1, x2, x3) = pH_out_ggg(x1, x2, x3)
pL_out_gag(x1, x2, x3) = pL_out_gag(x1, x2, x3)
pK_out_ggaag(x1, x2, x3, x4, x5) = pK_out_ggaag(x1, x2, x3, x4, x5)
pB_out_aaagaa(x1, x2, x3, x4, x5, x6) = pB_out_aaagaa(x1, x2, x3, x4, x5, x6)
SSA_IN_GA(x1, x2) = SSA_IN_GA(x1)
U1_GA(x1, x2, x3, x4) = U1_GA(x1, x4)
PB_IN_AAAGAA(x1, x2, x3, x4, x5, x6) = PB_IN_AAAGAA(x4)
U8_AAAGAA(x1, x2, x3, x4, x5, x6, x7) = U8_AAAGAA(x4, x7)
APPC_IN_AAAG(x1, x2, x3, x4) = APPC_IN_AAAG(x4)
U2_AAAG(x1, x2, x3, x4, x5, x6) = U2_AAAG(x1, x5, x6)
U9_AAAGAA(x1, x2, x3, x4, x5, x6, x7) = U9_AAAGAA(x1, x2, x3, x4, x7)
PK_IN_GGAAG(x1, x2, x3, x4, x5) = PK_IN_GGAAG(x1, x2, x5)
U10_GGAAG(x1, x2, x3, x4, x5, x6) = U10_GGAAG(x1, x2, x5, x6)
APPD_IN_GGA(x1, x2, x3) = APPD_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4, x5) = U3_GGA(x1, x2, x3, x5)
U11_GGAAG(x1, x2, x3, x4, x5, x6) = U11_GGAAG(x1, x2, x3, x5, x6)
PL_IN_GAG(x1, x2, x3) = PL_IN_GAG(x1, x3)
U12_GAG(x1, x2, x3, x4) = U12_GAG(x1, x3, x4)
PERME_IN_GA(x1, x2) = PERME_IN_GA(x1)
U4_GA(x1, x2, x3, x4) = U4_GA(x1, x4)
PF_IN_AAAGAA(x1, x2, x3, x4, x5, x6) = PF_IN_AAAGAA(x4)
U14_AAAGAA(x1, x2, x3, x4, x5, x6, x7) = U14_AAAGAA(x4, x7)
U15_AAAGAA(x1, x2, x3, x4, x5, x6, x7) = U15_AAAGAA(x1, x2, x3, x4, x7)
PM_IN_GGAA(x1, x2, x3, x4) = PM_IN_GGAA(x1, x2)
U16_GGAA(x1, x2, x3, x4, x5) = U16_GGAA(x1, x2, x5)
U17_GGAA(x1, x2, x3, x4, x5) = U17_GGAA(x1, x2, x3, x5)
U13_GAG(x1, x2, x3, x4) = U13_GAG(x1, x2, x3, x4)
ORDEREDG_IN_GG(x1, x2) = ORDEREDG_IN_GG(x1, x2)
U5_GG(x1, x2, x3, x4) = U5_GG(x1, x2, x3, x4)
PH_IN_GGG(x1, x2, x3) = PH_IN_GGG(x1, x2, x3)
U18_GGG(x1, x2, x3, x4) = U18_GGG(x1, x2, x3, x4)
LESSJ_IN_GG(x1, x2) = LESSJ_IN_GG(x1, x2)
U7_GG(x1, x2, x3) = U7_GG(x1, x2, x3)
LESSI_IN_GG(x1, x2) = LESSI_IN_GG(x1, x2)
U6_GG(x1, x2, x3) = U6_GG(x1, x2, x3)
U19_GGG(x1, x2, x3, x4) = U19_GGG(x1, x2, x3, x4)

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

(4) Obligation:

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

SSA_IN_GA(T14, .(T17, T18)) → U1_GA(T14, T17, T18, pB_in_aaagaa(X23, T17, X24, T14, X25, T18))
SSA_IN_GA(T14, .(T17, T18)) → PB_IN_AAAGAA(X23, T17, X24, T14, X25, T18)
PB_IN_AAAGAA(T23, T26, T24, T14, X25, T25) → U8_AAAGAA(T23, T26, T24, T14, X25, T25, appC_in_aaag(T23, T26, T24, T14))
PB_IN_AAAGAA(T23, T26, T24, T14, X25, T25) → APPC_IN_AAAG(T23, T26, T24, T14)
APPC_IN_AAAG(.(T48, X63), T50, X64, .(T48, T49)) → U2_AAAG(T48, X63, T50, X64, T49, appC_in_aaag(X63, T50, X64, T49))
APPC_IN_AAAG(.(T48, X63), T50, X64, .(T48, T49)) → APPC_IN_AAAG(X63, T50, X64, T49)
U8_AAAGAA(T23, T26, T24, T14, X25, T25, appC_out_aaag(T23, T26, T24, T14)) → U9_AAAGAA(T23, T26, T24, T14, X25, T25, pK_in_ggaag(T23, T24, X25, T25, T26))
U8_AAAGAA(T23, T26, T24, T14, X25, T25, appC_out_aaag(T23, T26, T24, T14)) → PK_IN_GGAAG(T23, T24, X25, T25, T26)
PK_IN_GGAAG(T23, T24, T57, T25, T26) → U10_GGAAG(T23, T24, T57, T25, T26, appD_in_gga(T23, T24, T57))
PK_IN_GGAAG(T23, T24, T57, T25, T26) → APPD_IN_GGA(T23, T24, T57)
APPD_IN_GGA(.(T71, T72), T73, .(T71, X92)) → U3_GGA(T71, T72, T73, X92, appD_in_gga(T72, T73, X92))
APPD_IN_GGA(.(T71, T72), T73, .(T71, X92)) → APPD_IN_GGA(T72, T73, X92)
U10_GGAAG(T23, T24, T57, T25, T26, appD_out_gga(T23, T24, T57)) → U11_GGAAG(T23, T24, T57, T25, T26, pL_in_gag(T57, T25, T26))
U10_GGAAG(T23, T24, T57, T25, T26, appD_out_gga(T23, T24, T57)) → PL_IN_GAG(T57, T25, T26)
PL_IN_GAG(T57, T76, T26) → U12_GAG(T57, T76, T26, permE_in_ga(T57, T76))
PL_IN_GAG(T57, T76, T26) → PERME_IN_GA(T57, T76)
PERME_IN_GA(T83, .(T86, T87)) → U4_GA(T83, T86, T87, pF_in_aaagaa(X107, T86, X108, T83, X109, T87))
PERME_IN_GA(T83, .(T86, T87)) → PF_IN_AAAGAA(X107, T86, X108, T83, X109, T87)
PF_IN_AAAGAA(T92, T86, T93, T83, X109, T94) → U14_AAAGAA(T92, T86, T93, T83, X109, T94, appC_in_aaag(T92, T86, T93, T83))
PF_IN_AAAGAA(T92, T86, T93, T83, X109, T94) → APPC_IN_AAAG(T92, T86, T93, T83)
U14_AAAGAA(T92, T86, T93, T83, X109, T94, appC_out_aaag(T92, T86, T93, T83)) → U15_AAAGAA(T92, T86, T93, T83, X109, T94, pM_in_ggaa(T92, T93, X109, T94))
U14_AAAGAA(T92, T86, T93, T83, X109, T94, appC_out_aaag(T92, T86, T93, T83)) → PM_IN_GGAA(T92, T93, X109, T94)
PM_IN_GGAA(T92, T93, T101, T94) → U16_GGAA(T92, T93, T101, T94, appD_in_gga(T92, T93, T101))
PM_IN_GGAA(T92, T93, T101, T94) → APPD_IN_GGA(T92, T93, T101)
U16_GGAA(T92, T93, T101, T94, appD_out_gga(T92, T93, T101)) → U17_GGAA(T92, T93, T101, T94, permE_in_ga(T101, T94))
U16_GGAA(T92, T93, T101, T94, appD_out_gga(T92, T93, T101)) → PERME_IN_GA(T101, T94)
U12_GAG(T57, T76, T26, permE_out_ga(T57, T76)) → U13_GAG(T57, T76, T26, orderedG_in_gg(T26, T76))
U12_GAG(T57, T76, T26, permE_out_ga(T57, T76)) → ORDEREDG_IN_GG(T26, T76)
ORDEREDG_IN_GG(T115, .(T116, T117)) → U5_GG(T115, T116, T117, pH_in_ggg(T115, T116, T117))
ORDEREDG_IN_GG(T115, .(T116, T117)) → PH_IN_GGG(T115, T116, T117)
PH_IN_GGG(T115, T116, T117) → U18_GGG(T115, T116, T117, lessJ_in_gg(T115, T116))
PH_IN_GGG(T115, T116, T117) → LESSJ_IN_GG(T115, T116)
LESSJ_IN_GG(s(T131), T132) → U7_GG(T131, T132, lessI_in_gg(T131, T132))
LESSJ_IN_GG(s(T131), T132) → LESSI_IN_GG(T131, T132)
LESSI_IN_GG(s(T144), s(T145)) → U6_GG(T144, T145, lessI_in_gg(T144, T145))
LESSI_IN_GG(s(T144), s(T145)) → LESSI_IN_GG(T144, T145)
U18_GGG(T115, T116, T117, lessJ_out_gg(T115, T116)) → U19_GGG(T115, T116, T117, orderedG_in_gg(T116, T117))
U18_GGG(T115, T116, T117, lessJ_out_gg(T115, T116)) → ORDEREDG_IN_GG(T116, T117)

The TRS R consists of the following rules:

ssA_in_ga([], []) → ssA_out_ga([], [])
ssA_in_ga(T14, .(T17, T18)) → U1_ga(T14, T17, T18, pB_in_aaagaa(X23, T17, X24, T14, X25, T18))
pB_in_aaagaa(T23, T26, T24, T14, X25, T25) → U8_aaagaa(T23, T26, T24, T14, X25, T25, appC_in_aaag(T23, T26, T24, T14))
appC_in_aaag([], T39, T40, .(T39, T40)) → appC_out_aaag([], T39, T40, .(T39, T40))
appC_in_aaag(.(T48, X63), T50, X64, .(T48, T49)) → U2_aaag(T48, X63, T50, X64, T49, appC_in_aaag(X63, T50, X64, T49))
U2_aaag(T48, X63, T50, X64, T49, appC_out_aaag(X63, T50, X64, T49)) → appC_out_aaag(.(T48, X63), T50, X64, .(T48, T49))
U8_aaagaa(T23, T26, T24, T14, X25, T25, appC_out_aaag(T23, T26, T24, T14)) → U9_aaagaa(T23, T26, T24, T14, X25, T25, pK_in_ggaag(T23, T24, X25, T25, T26))
pK_in_ggaag(T23, T24, T57, T25, T26) → U10_ggaag(T23, T24, T57, T25, T26, appD_in_gga(T23, T24, T57))
appD_in_gga([], T64, T64) → appD_out_gga([], T64, T64)
appD_in_gga(.(T71, T72), T73, .(T71, X92)) → U3_gga(T71, T72, T73, X92, appD_in_gga(T72, T73, X92))
U3_gga(T71, T72, T73, X92, appD_out_gga(T72, T73, X92)) → appD_out_gga(.(T71, T72), T73, .(T71, X92))
U10_ggaag(T23, T24, T57, T25, T26, appD_out_gga(T23, T24, T57)) → U11_ggaag(T23, T24, T57, T25, T26, pL_in_gag(T57, T25, T26))
pL_in_gag(T57, T76, T26) → U12_gag(T57, T76, T26, permE_in_ga(T57, T76))
permE_in_ga([], []) → permE_out_ga([], [])
permE_in_ga(T83, .(T86, T87)) → U4_ga(T83, T86, T87, pF_in_aaagaa(X107, T86, X108, T83, X109, T87))
pF_in_aaagaa(T92, T86, T93, T83, X109, T94) → U14_aaagaa(T92, T86, T93, T83, X109, T94, appC_in_aaag(T92, T86, T93, T83))
U14_aaagaa(T92, T86, T93, T83, X109, T94, appC_out_aaag(T92, T86, T93, T83)) → U15_aaagaa(T92, T86, T93, T83, X109, T94, pM_in_ggaa(T92, T93, X109, T94))
pM_in_ggaa(T92, T93, T101, T94) → U16_ggaa(T92, T93, T101, T94, appD_in_gga(T92, T93, T101))
U16_ggaa(T92, T93, T101, T94, appD_out_gga(T92, T93, T101)) → U17_ggaa(T92, T93, T101, T94, permE_in_ga(T101, T94))
U17_ggaa(T92, T93, T101, T94, permE_out_ga(T101, T94)) → pM_out_ggaa(T92, T93, T101, T94)
U15_aaagaa(T92, T86, T93, T83, X109, T94, pM_out_ggaa(T92, T93, X109, T94)) → pF_out_aaagaa(T92, T86, T93, T83, X109, T94)
U4_ga(T83, T86, T87, pF_out_aaagaa(X107, T86, X108, T83, X109, T87)) → permE_out_ga(T83, .(T86, T87))
U12_gag(T57, T76, T26, permE_out_ga(T57, T76)) → U13_gag(T57, T76, T26, orderedG_in_gg(T26, T76))
orderedG_in_gg(T108, []) → orderedG_out_gg(T108, [])
orderedG_in_gg(T115, .(T116, T117)) → U5_gg(T115, T116, T117, pH_in_ggg(T115, T116, T117))
pH_in_ggg(T115, T116, T117) → U18_ggg(T115, T116, T117, lessJ_in_gg(T115, T116))
lessJ_in_gg(0, T126) → lessJ_out_gg(0, T126)
lessJ_in_gg(s(T131), T132) → U7_gg(T131, T132, lessI_in_gg(T131, T132))
lessI_in_gg(0, s(T139)) → lessI_out_gg(0, s(T139))
lessI_in_gg(s(T144), s(T145)) → U6_gg(T144, T145, lessI_in_gg(T144, T145))
U6_gg(T144, T145, lessI_out_gg(T144, T145)) → lessI_out_gg(s(T144), s(T145))
U7_gg(T131, T132, lessI_out_gg(T131, T132)) → lessJ_out_gg(s(T131), T132)
U18_ggg(T115, T116, T117, lessJ_out_gg(T115, T116)) → U19_ggg(T115, T116, T117, orderedG_in_gg(T116, T117))
U19_ggg(T115, T116, T117, orderedG_out_gg(T116, T117)) → pH_out_ggg(T115, T116, T117)
U5_gg(T115, T116, T117, pH_out_ggg(T115, T116, T117)) → orderedG_out_gg(T115, .(T116, T117))
U13_gag(T57, T76, T26, orderedG_out_gg(T26, T76)) → pL_out_gag(T57, T76, T26)
U11_ggaag(T23, T24, T57, T25, T26, pL_out_gag(T57, T25, T26)) → pK_out_ggaag(T23, T24, T57, T25, T26)
U9_aaagaa(T23, T26, T24, T14, X25, T25, pK_out_ggaag(T23, T24, X25, T25, T26)) → pB_out_aaagaa(T23, T26, T24, T14, X25, T25)
U1_ga(T14, T17, T18, pB_out_aaagaa(X23, T17, X24, T14, X25, T18)) → ssA_out_ga(T14, .(T17, T18))

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 5 SCCs with 27 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

LESSI_IN_GG(s(T144), s(T145)) → LESSI_IN_GG(T144, T145)

The TRS R consists of the following rules:

ssA_in_ga([], []) → ssA_out_ga([], [])
ssA_in_ga(T14, .(T17, T18)) → U1_ga(T14, T17, T18, pB_in_aaagaa(X23, T17, X24, T14, X25, T18))
pB_in_aaagaa(T23, T26, T24, T14, X25, T25) → U8_aaagaa(T23, T26, T24, T14, X25, T25, appC_in_aaag(T23, T26, T24, T14))
appC_in_aaag([], T39, T40, .(T39, T40)) → appC_out_aaag([], T39, T40, .(T39, T40))
appC_in_aaag(.(T48, X63), T50, X64, .(T48, T49)) → U2_aaag(T48, X63, T50, X64, T49, appC_in_aaag(X63, T50, X64, T49))
U2_aaag(T48, X63, T50, X64, T49, appC_out_aaag(X63, T50, X64, T49)) → appC_out_aaag(.(T48, X63), T50, X64, .(T48, T49))
U8_aaagaa(T23, T26, T24, T14, X25, T25, appC_out_aaag(T23, T26, T24, T14)) → U9_aaagaa(T23, T26, T24, T14, X25, T25, pK_in_ggaag(T23, T24, X25, T25, T26))
pK_in_ggaag(T23, T24, T57, T25, T26) → U10_ggaag(T23, T24, T57, T25, T26, appD_in_gga(T23, T24, T57))
appD_in_gga([], T64, T64) → appD_out_gga([], T64, T64)
appD_in_gga(.(T71, T72), T73, .(T71, X92)) → U3_gga(T71, T72, T73, X92, appD_in_gga(T72, T73, X92))
U3_gga(T71, T72, T73, X92, appD_out_gga(T72, T73, X92)) → appD_out_gga(.(T71, T72), T73, .(T71, X92))
U10_ggaag(T23, T24, T57, T25, T26, appD_out_gga(T23, T24, T57)) → U11_ggaag(T23, T24, T57, T25, T26, pL_in_gag(T57, T25, T26))
pL_in_gag(T57, T76, T26) → U12_gag(T57, T76, T26, permE_in_ga(T57, T76))
permE_in_ga([], []) → permE_out_ga([], [])
permE_in_ga(T83, .(T86, T87)) → U4_ga(T83, T86, T87, pF_in_aaagaa(X107, T86, X108, T83, X109, T87))
pF_in_aaagaa(T92, T86, T93, T83, X109, T94) → U14_aaagaa(T92, T86, T93, T83, X109, T94, appC_in_aaag(T92, T86, T93, T83))
U14_aaagaa(T92, T86, T93, T83, X109, T94, appC_out_aaag(T92, T86, T93, T83)) → U15_aaagaa(T92, T86, T93, T83, X109, T94, pM_in_ggaa(T92, T93, X109, T94))
pM_in_ggaa(T92, T93, T101, T94) → U16_ggaa(T92, T93, T101, T94, appD_in_gga(T92, T93, T101))
U16_ggaa(T92, T93, T101, T94, appD_out_gga(T92, T93, T101)) → U17_ggaa(T92, T93, T101, T94, permE_in_ga(T101, T94))
U17_ggaa(T92, T93, T101, T94, permE_out_ga(T101, T94)) → pM_out_ggaa(T92, T93, T101, T94)
U15_aaagaa(T92, T86, T93, T83, X109, T94, pM_out_ggaa(T92, T93, X109, T94)) → pF_out_aaagaa(T92, T86, T93, T83, X109, T94)
U4_ga(T83, T86, T87, pF_out_aaagaa(X107, T86, X108, T83, X109, T87)) → permE_out_ga(T83, .(T86, T87))
U12_gag(T57, T76, T26, permE_out_ga(T57, T76)) → U13_gag(T57, T76, T26, orderedG_in_gg(T26, T76))
orderedG_in_gg(T108, []) → orderedG_out_gg(T108, [])
orderedG_in_gg(T115, .(T116, T117)) → U5_gg(T115, T116, T117, pH_in_ggg(T115, T116, T117))
pH_in_ggg(T115, T116, T117) → U18_ggg(T115, T116, T117, lessJ_in_gg(T115, T116))
lessJ_in_gg(0, T126) → lessJ_out_gg(0, T126)
lessJ_in_gg(s(T131), T132) → U7_gg(T131, T132, lessI_in_gg(T131, T132))
lessI_in_gg(0, s(T139)) → lessI_out_gg(0, s(T139))
lessI_in_gg(s(T144), s(T145)) → U6_gg(T144, T145, lessI_in_gg(T144, T145))
U6_gg(T144, T145, lessI_out_gg(T144, T145)) → lessI_out_gg(s(T144), s(T145))
U7_gg(T131, T132, lessI_out_gg(T131, T132)) → lessJ_out_gg(s(T131), T132)
U18_ggg(T115, T116, T117, lessJ_out_gg(T115, T116)) → U19_ggg(T115, T116, T117, orderedG_in_gg(T116, T117))
U19_ggg(T115, T116, T117, orderedG_out_gg(T116, T117)) → pH_out_ggg(T115, T116, T117)
U5_gg(T115, T116, T117, pH_out_ggg(T115, T116, T117)) → orderedG_out_gg(T115, .(T116, T117))
U13_gag(T57, T76, T26, orderedG_out_gg(T26, T76)) → pL_out_gag(T57, T76, T26)
U11_ggaag(T23, T24, T57, T25, T26, pL_out_gag(T57, T25, T26)) → pK_out_ggaag(T23, T24, T57, T25, T26)
U9_aaagaa(T23, T26, T24, T14, X25, T25, pK_out_ggaag(T23, T24, X25, T25, T26)) → pB_out_aaagaa(T23, T26, T24, T14, X25, T25)
U1_ga(T14, T17, T18, pB_out_aaagaa(X23, T17, X24, T14, X25, T18)) → ssA_out_ga(T14, .(T17, T18))

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

LESSI_IN_GG(s(T144), s(T145)) → LESSI_IN_GG(T144, T145)

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:

LESSI_IN_GG(s(T144), s(T145)) → LESSI_IN_GG(T144, T145)

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:

LESSI_IN_GG(s(T144), s(T145)) → LESSI_IN_GG(T144, T145)
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:

ORDEREDG_IN_GG(T115, .(T116, T117)) → PH_IN_GGG(T115, T116, T117)
PH_IN_GGG(T115, T116, T117) → U18_GGG(T115, T116, T117, lessJ_in_gg(T115, T116))
U18_GGG(T115, T116, T117, lessJ_out_gg(T115, T116)) → ORDEREDG_IN_GG(T116, T117)

The TRS R consists of the following rules:

ssA_in_ga([], []) → ssA_out_ga([], [])
ssA_in_ga(T14, .(T17, T18)) → U1_ga(T14, T17, T18, pB_in_aaagaa(X23, T17, X24, T14, X25, T18))
pB_in_aaagaa(T23, T26, T24, T14, X25, T25) → U8_aaagaa(T23, T26, T24, T14, X25, T25, appC_in_aaag(T23, T26, T24, T14))
appC_in_aaag([], T39, T40, .(T39, T40)) → appC_out_aaag([], T39, T40, .(T39, T40))
appC_in_aaag(.(T48, X63), T50, X64, .(T48, T49)) → U2_aaag(T48, X63, T50, X64, T49, appC_in_aaag(X63, T50, X64, T49))
U2_aaag(T48, X63, T50, X64, T49, appC_out_aaag(X63, T50, X64, T49)) → appC_out_aaag(.(T48, X63), T50, X64, .(T48, T49))
U8_aaagaa(T23, T26, T24, T14, X25, T25, appC_out_aaag(T23, T26, T24, T14)) → U9_aaagaa(T23, T26, T24, T14, X25, T25, pK_in_ggaag(T23, T24, X25, T25, T26))
pK_in_ggaag(T23, T24, T57, T25, T26) → U10_ggaag(T23, T24, T57, T25, T26, appD_in_gga(T23, T24, T57))
appD_in_gga([], T64, T64) → appD_out_gga([], T64, T64)
appD_in_gga(.(T71, T72), T73, .(T71, X92)) → U3_gga(T71, T72, T73, X92, appD_in_gga(T72, T73, X92))
U3_gga(T71, T72, T73, X92, appD_out_gga(T72, T73, X92)) → appD_out_gga(.(T71, T72), T73, .(T71, X92))
U10_ggaag(T23, T24, T57, T25, T26, appD_out_gga(T23, T24, T57)) → U11_ggaag(T23, T24, T57, T25, T26, pL_in_gag(T57, T25, T26))
pL_in_gag(T57, T76, T26) → U12_gag(T57, T76, T26, permE_in_ga(T57, T76))
permE_in_ga([], []) → permE_out_ga([], [])
permE_in_ga(T83, .(T86, T87)) → U4_ga(T83, T86, T87, pF_in_aaagaa(X107, T86, X108, T83, X109, T87))
pF_in_aaagaa(T92, T86, T93, T83, X109, T94) → U14_aaagaa(T92, T86, T93, T83, X109, T94, appC_in_aaag(T92, T86, T93, T83))
U14_aaagaa(T92, T86, T93, T83, X109, T94, appC_out_aaag(T92, T86, T93, T83)) → U15_aaagaa(T92, T86, T93, T83, X109, T94, pM_in_ggaa(T92, T93, X109, T94))
pM_in_ggaa(T92, T93, T101, T94) → U16_ggaa(T92, T93, T101, T94, appD_in_gga(T92, T93, T101))
U16_ggaa(T92, T93, T101, T94, appD_out_gga(T92, T93, T101)) → U17_ggaa(T92, T93, T101, T94, permE_in_ga(T101, T94))
U17_ggaa(T92, T93, T101, T94, permE_out_ga(T101, T94)) → pM_out_ggaa(T92, T93, T101, T94)
U15_aaagaa(T92, T86, T93, T83, X109, T94, pM_out_ggaa(T92, T93, X109, T94)) → pF_out_aaagaa(T92, T86, T93, T83, X109, T94)
U4_ga(T83, T86, T87, pF_out_aaagaa(X107, T86, X108, T83, X109, T87)) → permE_out_ga(T83, .(T86, T87))
U12_gag(T57, T76, T26, permE_out_ga(T57, T76)) → U13_gag(T57, T76, T26, orderedG_in_gg(T26, T76))
orderedG_in_gg(T108, []) → orderedG_out_gg(T108, [])
orderedG_in_gg(T115, .(T116, T117)) → U5_gg(T115, T116, T117, pH_in_ggg(T115, T116, T117))
pH_in_ggg(T115, T116, T117) → U18_ggg(T115, T116, T117, lessJ_in_gg(T115, T116))
lessJ_in_gg(0, T126) → lessJ_out_gg(0, T126)
lessJ_in_gg(s(T131), T132) → U7_gg(T131, T132, lessI_in_gg(T131, T132))
lessI_in_gg(0, s(T139)) → lessI_out_gg(0, s(T139))
lessI_in_gg(s(T144), s(T145)) → U6_gg(T144, T145, lessI_in_gg(T144, T145))
U6_gg(T144, T145, lessI_out_gg(T144, T145)) → lessI_out_gg(s(T144), s(T145))
U7_gg(T131, T132, lessI_out_gg(T131, T132)) → lessJ_out_gg(s(T131), T132)
U18_ggg(T115, T116, T117, lessJ_out_gg(T115, T116)) → U19_ggg(T115, T116, T117, orderedG_in_gg(T116, T117))
U19_ggg(T115, T116, T117, orderedG_out_gg(T116, T117)) → pH_out_ggg(T115, T116, T117)
U5_gg(T115, T116, T117, pH_out_ggg(T115, T116, T117)) → orderedG_out_gg(T115, .(T116, T117))
U13_gag(T57, T76, T26, orderedG_out_gg(T26, T76)) → pL_out_gag(T57, T76, T26)
U11_ggaag(T23, T24, T57, T25, T26, pL_out_gag(T57, T25, T26)) → pK_out_ggaag(T23, T24, T57, T25, T26)
U9_aaagaa(T23, T26, T24, T14, X25, T25, pK_out_ggaag(T23, T24, X25, T25, T26)) → pB_out_aaagaa(T23, T26, T24, T14, X25, T25)
U1_ga(T14, T17, T18, pB_out_aaagaa(X23, T17, X24, T14, X25, T18)) → ssA_out_ga(T14, .(T17, T18))

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

ORDEREDG_IN_GG(T115, .(T116, T117)) → PH_IN_GGG(T115, T116, T117)
PH_IN_GGG(T115, T116, T117) → U18_GGG(T115, T116, T117, lessJ_in_gg(T115, T116))
U18_GGG(T115, T116, T117, lessJ_out_gg(T115, T116)) → ORDEREDG_IN_GG(T116, T117)

The TRS R consists of the following rules:

lessJ_in_gg(0, T126) → lessJ_out_gg(0, T126)
lessJ_in_gg(s(T131), T132) → U7_gg(T131, T132, lessI_in_gg(T131, T132))
U7_gg(T131, T132, lessI_out_gg(T131, T132)) → lessJ_out_gg(s(T131), T132)
lessI_in_gg(0, s(T139)) → lessI_out_gg(0, s(T139))
lessI_in_gg(s(T144), s(T145)) → U6_gg(T144, T145, lessI_in_gg(T144, T145))
U6_gg(T144, T145, lessI_out_gg(T144, T145)) → lessI_out_gg(s(T144), s(T145))

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

(17) PiDPToQDPProof (EQUIVALENT transformation)

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

(18) Obligation:

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

ORDEREDG_IN_GG(T115, .(T116, T117)) → PH_IN_GGG(T115, T116, T117)
PH_IN_GGG(T115, T116, T117) → U18_GGG(T115, T116, T117, lessJ_in_gg(T115, T116))
U18_GGG(T115, T116, T117, lessJ_out_gg(T115, T116)) → ORDEREDG_IN_GG(T116, T117)

The TRS R consists of the following rules:

lessJ_in_gg(0, T126) → lessJ_out_gg(0, T126)
lessJ_in_gg(s(T131), T132) → U7_gg(T131, T132, lessI_in_gg(T131, T132))
U7_gg(T131, T132, lessI_out_gg(T131, T132)) → lessJ_out_gg(s(T131), T132)
lessI_in_gg(0, s(T139)) → lessI_out_gg(0, s(T139))
lessI_in_gg(s(T144), s(T145)) → U6_gg(T144, T145, lessI_in_gg(T144, T145))
U6_gg(T144, T145, lessI_out_gg(T144, T145)) → lessI_out_gg(s(T144), s(T145))

The set Q consists of the following terms:

lessJ_in_gg(x0, x1)
U7_gg(x0, x1, x2)
lessI_in_gg(x0, x1)
U6_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:

PH_IN_GGG(T115, T116, T117) → U18_GGG(T115, T116, T117, lessJ_in_gg(T115, T116))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3
U18_GGG(T115, T116, T117, lessJ_out_gg(T115, T116)) → ORDEREDG_IN_GG(T116, T117)
The graph contains the following edges 2 >= 1, 4 > 1, 3 >= 2
ORDEREDG_IN_GG(T115, .(T116, T117)) → PH_IN_GGG(T115, T116, T117)
The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

(20) YES

(21) Obligation:

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

APPD_IN_GGA(.(T71, T72), T73, .(T71, X92)) → APPD_IN_GGA(T72, T73, X92)

The TRS R consists of the following rules:

ssA_in_ga([], []) → ssA_out_ga([], [])
ssA_in_ga(T14, .(T17, T18)) → U1_ga(T14, T17, T18, pB_in_aaagaa(X23, T17, X24, T14, X25, T18))
pB_in_aaagaa(T23, T26, T24, T14, X25, T25) → U8_aaagaa(T23, T26, T24, T14, X25, T25, appC_in_aaag(T23, T26, T24, T14))
appC_in_aaag([], T39, T40, .(T39, T40)) → appC_out_aaag([], T39, T40, .(T39, T40))
appC_in_aaag(.(T48, X63), T50, X64, .(T48, T49)) → U2_aaag(T48, X63, T50, X64, T49, appC_in_aaag(X63, T50, X64, T49))
U2_aaag(T48, X63, T50, X64, T49, appC_out_aaag(X63, T50, X64, T49)) → appC_out_aaag(.(T48, X63), T50, X64, .(T48, T49))
U8_aaagaa(T23, T26, T24, T14, X25, T25, appC_out_aaag(T23, T26, T24, T14)) → U9_aaagaa(T23, T26, T24, T14, X25, T25, pK_in_ggaag(T23, T24, X25, T25, T26))
pK_in_ggaag(T23, T24, T57, T25, T26) → U10_ggaag(T23, T24, T57, T25, T26, appD_in_gga(T23, T24, T57))
appD_in_gga([], T64, T64) → appD_out_gga([], T64, T64)
appD_in_gga(.(T71, T72), T73, .(T71, X92)) → U3_gga(T71, T72, T73, X92, appD_in_gga(T72, T73, X92))
U3_gga(T71, T72, T73, X92, appD_out_gga(T72, T73, X92)) → appD_out_gga(.(T71, T72), T73, .(T71, X92))
U10_ggaag(T23, T24, T57, T25, T26, appD_out_gga(T23, T24, T57)) → U11_ggaag(T23, T24, T57, T25, T26, pL_in_gag(T57, T25, T26))
pL_in_gag(T57, T76, T26) → U12_gag(T57, T76, T26, permE_in_ga(T57, T76))
permE_in_ga([], []) → permE_out_ga([], [])
permE_in_ga(T83, .(T86, T87)) → U4_ga(T83, T86, T87, pF_in_aaagaa(X107, T86, X108, T83, X109, T87))
pF_in_aaagaa(T92, T86, T93, T83, X109, T94) → U14_aaagaa(T92, T86, T93, T83, X109, T94, appC_in_aaag(T92, T86, T93, T83))
U14_aaagaa(T92, T86, T93, T83, X109, T94, appC_out_aaag(T92, T86, T93, T83)) → U15_aaagaa(T92, T86, T93, T83, X109, T94, pM_in_ggaa(T92, T93, X109, T94))
pM_in_ggaa(T92, T93, T101, T94) → U16_ggaa(T92, T93, T101, T94, appD_in_gga(T92, T93, T101))
U16_ggaa(T92, T93, T101, T94, appD_out_gga(T92, T93, T101)) → U17_ggaa(T92, T93, T101, T94, permE_in_ga(T101, T94))
U17_ggaa(T92, T93, T101, T94, permE_out_ga(T101, T94)) → pM_out_ggaa(T92, T93, T101, T94)
U15_aaagaa(T92, T86, T93, T83, X109, T94, pM_out_ggaa(T92, T93, X109, T94)) → pF_out_aaagaa(T92, T86, T93, T83, X109, T94)
U4_ga(T83, T86, T87, pF_out_aaagaa(X107, T86, X108, T83, X109, T87)) → permE_out_ga(T83, .(T86, T87))
U12_gag(T57, T76, T26, permE_out_ga(T57, T76)) → U13_gag(T57, T76, T26, orderedG_in_gg(T26, T76))
orderedG_in_gg(T108, []) → orderedG_out_gg(T108, [])
orderedG_in_gg(T115, .(T116, T117)) → U5_gg(T115, T116, T117, pH_in_ggg(T115, T116, T117))
pH_in_ggg(T115, T116, T117) → U18_ggg(T115, T116, T117, lessJ_in_gg(T115, T116))
lessJ_in_gg(0, T126) → lessJ_out_gg(0, T126)
lessJ_in_gg(s(T131), T132) → U7_gg(T131, T132, lessI_in_gg(T131, T132))
lessI_in_gg(0, s(T139)) → lessI_out_gg(0, s(T139))
lessI_in_gg(s(T144), s(T145)) → U6_gg(T144, T145, lessI_in_gg(T144, T145))
U6_gg(T144, T145, lessI_out_gg(T144, T145)) → lessI_out_gg(s(T144), s(T145))
U7_gg(T131, T132, lessI_out_gg(T131, T132)) → lessJ_out_gg(s(T131), T132)
U18_ggg(T115, T116, T117, lessJ_out_gg(T115, T116)) → U19_ggg(T115, T116, T117, orderedG_in_gg(T116, T117))
U19_ggg(T115, T116, T117, orderedG_out_gg(T116, T117)) → pH_out_ggg(T115, T116, T117)
U5_gg(T115, T116, T117, pH_out_ggg(T115, T116, T117)) → orderedG_out_gg(T115, .(T116, T117))
U13_gag(T57, T76, T26, orderedG_out_gg(T26, T76)) → pL_out_gag(T57, T76, T26)
U11_ggaag(T23, T24, T57, T25, T26, pL_out_gag(T57, T25, T26)) → pK_out_ggaag(T23, T24, T57, T25, T26)
U9_aaagaa(T23, T26, T24, T14, X25, T25, pK_out_ggaag(T23, T24, X25, T25, T26)) → pB_out_aaagaa(T23, T26, T24, T14, X25, T25)
U1_ga(T14, T17, T18, pB_out_aaagaa(X23, T17, X24, T14, X25, T18)) → ssA_out_ga(T14, .(T17, T18))

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

APPD_IN_GGA(.(T71, T72), T73, .(T71, X92)) → APPD_IN_GGA(T72, T73, X92)

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

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

APPD_IN_GGA(.(T71, T72), T73) → APPD_IN_GGA(T72, T73)

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:

APPD_IN_GGA(.(T71, T72), T73) → APPD_IN_GGA(T72, T73)
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:

APPC_IN_AAAG(.(T48, X63), T50, X64, .(T48, T49)) → APPC_IN_AAAG(X63, T50, X64, T49)

The TRS R consists of the following rules:

ssA_in_ga([], []) → ssA_out_ga([], [])
ssA_in_ga(T14, .(T17, T18)) → U1_ga(T14, T17, T18, pB_in_aaagaa(X23, T17, X24, T14, X25, T18))
pB_in_aaagaa(T23, T26, T24, T14, X25, T25) → U8_aaagaa(T23, T26, T24, T14, X25, T25, appC_in_aaag(T23, T26, T24, T14))
appC_in_aaag([], T39, T40, .(T39, T40)) → appC_out_aaag([], T39, T40, .(T39, T40))
appC_in_aaag(.(T48, X63), T50, X64, .(T48, T49)) → U2_aaag(T48, X63, T50, X64, T49, appC_in_aaag(X63, T50, X64, T49))
U2_aaag(T48, X63, T50, X64, T49, appC_out_aaag(X63, T50, X64, T49)) → appC_out_aaag(.(T48, X63), T50, X64, .(T48, T49))
U8_aaagaa(T23, T26, T24, T14, X25, T25, appC_out_aaag(T23, T26, T24, T14)) → U9_aaagaa(T23, T26, T24, T14, X25, T25, pK_in_ggaag(T23, T24, X25, T25, T26))
pK_in_ggaag(T23, T24, T57, T25, T26) → U10_ggaag(T23, T24, T57, T25, T26, appD_in_gga(T23, T24, T57))
appD_in_gga([], T64, T64) → appD_out_gga([], T64, T64)
appD_in_gga(.(T71, T72), T73, .(T71, X92)) → U3_gga(T71, T72, T73, X92, appD_in_gga(T72, T73, X92))
U3_gga(T71, T72, T73, X92, appD_out_gga(T72, T73, X92)) → appD_out_gga(.(T71, T72), T73, .(T71, X92))
U10_ggaag(T23, T24, T57, T25, T26, appD_out_gga(T23, T24, T57)) → U11_ggaag(T23, T24, T57, T25, T26, pL_in_gag(T57, T25, T26))
pL_in_gag(T57, T76, T26) → U12_gag(T57, T76, T26, permE_in_ga(T57, T76))
permE_in_ga([], []) → permE_out_ga([], [])
permE_in_ga(T83, .(T86, T87)) → U4_ga(T83, T86, T87, pF_in_aaagaa(X107, T86, X108, T83, X109, T87))
pF_in_aaagaa(T92, T86, T93, T83, X109, T94) → U14_aaagaa(T92, T86, T93, T83, X109, T94, appC_in_aaag(T92, T86, T93, T83))
U14_aaagaa(T92, T86, T93, T83, X109, T94, appC_out_aaag(T92, T86, T93, T83)) → U15_aaagaa(T92, T86, T93, T83, X109, T94, pM_in_ggaa(T92, T93, X109, T94))
pM_in_ggaa(T92, T93, T101, T94) → U16_ggaa(T92, T93, T101, T94, appD_in_gga(T92, T93, T101))
U16_ggaa(T92, T93, T101, T94, appD_out_gga(T92, T93, T101)) → U17_ggaa(T92, T93, T101, T94, permE_in_ga(T101, T94))
U17_ggaa(T92, T93, T101, T94, permE_out_ga(T101, T94)) → pM_out_ggaa(T92, T93, T101, T94)
U15_aaagaa(T92, T86, T93, T83, X109, T94, pM_out_ggaa(T92, T93, X109, T94)) → pF_out_aaagaa(T92, T86, T93, T83, X109, T94)
U4_ga(T83, T86, T87, pF_out_aaagaa(X107, T86, X108, T83, X109, T87)) → permE_out_ga(T83, .(T86, T87))
U12_gag(T57, T76, T26, permE_out_ga(T57, T76)) → U13_gag(T57, T76, T26, orderedG_in_gg(T26, T76))
orderedG_in_gg(T108, []) → orderedG_out_gg(T108, [])
orderedG_in_gg(T115, .(T116, T117)) → U5_gg(T115, T116, T117, pH_in_ggg(T115, T116, T117))
pH_in_ggg(T115, T116, T117) → U18_ggg(T115, T116, T117, lessJ_in_gg(T115, T116))
lessJ_in_gg(0, T126) → lessJ_out_gg(0, T126)
lessJ_in_gg(s(T131), T132) → U7_gg(T131, T132, lessI_in_gg(T131, T132))
lessI_in_gg(0, s(T139)) → lessI_out_gg(0, s(T139))
lessI_in_gg(s(T144), s(T145)) → U6_gg(T144, T145, lessI_in_gg(T144, T145))
U6_gg(T144, T145, lessI_out_gg(T144, T145)) → lessI_out_gg(s(T144), s(T145))
U7_gg(T131, T132, lessI_out_gg(T131, T132)) → lessJ_out_gg(s(T131), T132)
U18_ggg(T115, T116, T117, lessJ_out_gg(T115, T116)) → U19_ggg(T115, T116, T117, orderedG_in_gg(T116, T117))
U19_ggg(T115, T116, T117, orderedG_out_gg(T116, T117)) → pH_out_ggg(T115, T116, T117)
U5_gg(T115, T116, T117, pH_out_ggg(T115, T116, T117)) → orderedG_out_gg(T115, .(T116, T117))
U13_gag(T57, T76, T26, orderedG_out_gg(T26, T76)) → pL_out_gag(T57, T76, T26)
U11_ggaag(T23, T24, T57, T25, T26, pL_out_gag(T57, T25, T26)) → pK_out_ggaag(T23, T24, T57, T25, T26)
U9_aaagaa(T23, T26, T24, T14, X25, T25, pK_out_ggaag(T23, T24, X25, T25, T26)) → pB_out_aaagaa(T23, T26, T24, T14, X25, T25)
U1_ga(T14, T17, T18, pB_out_aaagaa(X23, T17, X24, T14, X25, T18)) → ssA_out_ga(T14, .(T17, T18))

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

APPC_IN_AAAG(.(T48, X63), T50, X64, .(T48, T49)) → APPC_IN_AAAG(X63, T50, X64, T49)

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

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

(31) PiDPToQDPProof (SOUND 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:

APPC_IN_AAAG(.(T48, T49)) → APPC_IN_AAAG(T49)

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:

APPC_IN_AAAG(.(T48, T49)) → APPC_IN_AAAG(T49)
The graph contains the following edges 1 > 1

(34) YES

(35) Obligation:

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

PF_IN_AAAGAA(T92, T86, T93, T83, X109, T94) → U14_AAAGAA(T92, T86, T93, T83, X109, T94, appC_in_aaag(T92, T86, T93, T83))
U14_AAAGAA(T92, T86, T93, T83, X109, T94, appC_out_aaag(T92, T86, T93, T83)) → PM_IN_GGAA(T92, T93, X109, T94)
PM_IN_GGAA(T92, T93, T101, T94) → U16_GGAA(T92, T93, T101, T94, appD_in_gga(T92, T93, T101))
U16_GGAA(T92, T93, T101, T94, appD_out_gga(T92, T93, T101)) → PERME_IN_GA(T101, T94)
PERME_IN_GA(T83, .(T86, T87)) → PF_IN_AAAGAA(X107, T86, X108, T83, X109, T87)

The TRS R consists of the following rules:

ssA_in_ga([], []) → ssA_out_ga([], [])
ssA_in_ga(T14, .(T17, T18)) → U1_ga(T14, T17, T18, pB_in_aaagaa(X23, T17, X24, T14, X25, T18))
pB_in_aaagaa(T23, T26, T24, T14, X25, T25) → U8_aaagaa(T23, T26, T24, T14, X25, T25, appC_in_aaag(T23, T26, T24, T14))
appC_in_aaag([], T39, T40, .(T39, T40)) → appC_out_aaag([], T39, T40, .(T39, T40))
appC_in_aaag(.(T48, X63), T50, X64, .(T48, T49)) → U2_aaag(T48, X63, T50, X64, T49, appC_in_aaag(X63, T50, X64, T49))
U2_aaag(T48, X63, T50, X64, T49, appC_out_aaag(X63, T50, X64, T49)) → appC_out_aaag(.(T48, X63), T50, X64, .(T48, T49))
U8_aaagaa(T23, T26, T24, T14, X25, T25, appC_out_aaag(T23, T26, T24, T14)) → U9_aaagaa(T23, T26, T24, T14, X25, T25, pK_in_ggaag(T23, T24, X25, T25, T26))
pK_in_ggaag(T23, T24, T57, T25, T26) → U10_ggaag(T23, T24, T57, T25, T26, appD_in_gga(T23, T24, T57))
appD_in_gga([], T64, T64) → appD_out_gga([], T64, T64)
appD_in_gga(.(T71, T72), T73, .(T71, X92)) → U3_gga(T71, T72, T73, X92, appD_in_gga(T72, T73, X92))
U3_gga(T71, T72, T73, X92, appD_out_gga(T72, T73, X92)) → appD_out_gga(.(T71, T72), T73, .(T71, X92))
U10_ggaag(T23, T24, T57, T25, T26, appD_out_gga(T23, T24, T57)) → U11_ggaag(T23, T24, T57, T25, T26, pL_in_gag(T57, T25, T26))
pL_in_gag(T57, T76, T26) → U12_gag(T57, T76, T26, permE_in_ga(T57, T76))
permE_in_ga([], []) → permE_out_ga([], [])
permE_in_ga(T83, .(T86, T87)) → U4_ga(T83, T86, T87, pF_in_aaagaa(X107, T86, X108, T83, X109, T87))
pF_in_aaagaa(T92, T86, T93, T83, X109, T94) → U14_aaagaa(T92, T86, T93, T83, X109, T94, appC_in_aaag(T92, T86, T93, T83))
U14_aaagaa(T92, T86, T93, T83, X109, T94, appC_out_aaag(T92, T86, T93, T83)) → U15_aaagaa(T92, T86, T93, T83, X109, T94, pM_in_ggaa(T92, T93, X109, T94))
pM_in_ggaa(T92, T93, T101, T94) → U16_ggaa(T92, T93, T101, T94, appD_in_gga(T92, T93, T101))
U16_ggaa(T92, T93, T101, T94, appD_out_gga(T92, T93, T101)) → U17_ggaa(T92, T93, T101, T94, permE_in_ga(T101, T94))
U17_ggaa(T92, T93, T101, T94, permE_out_ga(T101, T94)) → pM_out_ggaa(T92, T93, T101, T94)
U15_aaagaa(T92, T86, T93, T83, X109, T94, pM_out_ggaa(T92, T93, X109, T94)) → pF_out_aaagaa(T92, T86, T93, T83, X109, T94)
U4_ga(T83, T86, T87, pF_out_aaagaa(X107, T86, X108, T83, X109, T87)) → permE_out_ga(T83, .(T86, T87))
U12_gag(T57, T76, T26, permE_out_ga(T57, T76)) → U13_gag(T57, T76, T26, orderedG_in_gg(T26, T76))
orderedG_in_gg(T108, []) → orderedG_out_gg(T108, [])
orderedG_in_gg(T115, .(T116, T117)) → U5_gg(T115, T116, T117, pH_in_ggg(T115, T116, T117))
pH_in_ggg(T115, T116, T117) → U18_ggg(T115, T116, T117, lessJ_in_gg(T115, T116))
lessJ_in_gg(0, T126) → lessJ_out_gg(0, T126)
lessJ_in_gg(s(T131), T132) → U7_gg(T131, T132, lessI_in_gg(T131, T132))
lessI_in_gg(0, s(T139)) → lessI_out_gg(0, s(T139))
lessI_in_gg(s(T144), s(T145)) → U6_gg(T144, T145, lessI_in_gg(T144, T145))
U6_gg(T144, T145, lessI_out_gg(T144, T145)) → lessI_out_gg(s(T144), s(T145))
U7_gg(T131, T132, lessI_out_gg(T131, T132)) → lessJ_out_gg(s(T131), T132)
U18_ggg(T115, T116, T117, lessJ_out_gg(T115, T116)) → U19_ggg(T115, T116, T117, orderedG_in_gg(T116, T117))
U19_ggg(T115, T116, T117, orderedG_out_gg(T116, T117)) → pH_out_ggg(T115, T116, T117)
U5_gg(T115, T116, T117, pH_out_ggg(T115, T116, T117)) → orderedG_out_gg(T115, .(T116, T117))
U13_gag(T57, T76, T26, orderedG_out_gg(T26, T76)) → pL_out_gag(T57, T76, T26)
U11_ggaag(T23, T24, T57, T25, T26, pL_out_gag(T57, T25, T26)) → pK_out_ggaag(T23, T24, T57, T25, T26)
U9_aaagaa(T23, T26, T24, T14, X25, T25, pK_out_ggaag(T23, T24, X25, T25, T26)) → pB_out_aaagaa(T23, T26, T24, T14, X25, T25)
U1_ga(T14, T17, T18, pB_out_aaagaa(X23, T17, X24, T14, X25, T18)) → ssA_out_ga(T14, .(T17, T18))

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

PF_IN_AAAGAA(T92, T86, T93, T83, X109, T94) → U14_AAAGAA(T92, T86, T93, T83, X109, T94, appC_in_aaag(T92, T86, T93, T83))
U14_AAAGAA(T92, T86, T93, T83, X109, T94, appC_out_aaag(T92, T86, T93, T83)) → PM_IN_GGAA(T92, T93, X109, T94)
PM_IN_GGAA(T92, T93, T101, T94) → U16_GGAA(T92, T93, T101, T94, appD_in_gga(T92, T93, T101))
U16_GGAA(T92, T93, T101, T94, appD_out_gga(T92, T93, T101)) → PERME_IN_GA(T101, T94)
PERME_IN_GA(T83, .(T86, T87)) → PF_IN_AAAGAA(X107, T86, X108, T83, X109, T87)

The TRS R consists of the following rules:

appC_in_aaag([], T39, T40, .(T39, T40)) → appC_out_aaag([], T39, T40, .(T39, T40))
appC_in_aaag(.(T48, X63), T50, X64, .(T48, T49)) → U2_aaag(T48, X63, T50, X64, T49, appC_in_aaag(X63, T50, X64, T49))
appD_in_gga([], T64, T64) → appD_out_gga([], T64, T64)
appD_in_gga(.(T71, T72), T73, .(T71, X92)) → U3_gga(T71, T72, T73, X92, appD_in_gga(T72, T73, X92))
U2_aaag(T48, X63, T50, X64, T49, appC_out_aaag(X63, T50, X64, T49)) → appC_out_aaag(.(T48, X63), T50, X64, .(T48, T49))
U3_gga(T71, T72, T73, X92, appD_out_gga(T72, T73, X92)) → appD_out_gga(.(T71, T72), T73, .(T71, X92))

The argument filtering Pi contains the following mapping:
[] = []
appC_in_aaag(x1, x2, x3, x4) = appC_in_aaag(x4)
.(x1, x2) = .(x1, x2)
appC_out_aaag(x1, x2, x3, x4) = appC_out_aaag(x1, x2, x3, x4)
U2_aaag(x1, x2, x3, x4, x5, x6) = U2_aaag(x1, x5, x6)
appD_in_gga(x1, x2, x3) = appD_in_gga(x1, x2)
appD_out_gga(x1, x2, x3) = appD_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5) = U3_gga(x1, x2, x3, x5)
PERME_IN_GA(x1, x2) = PERME_IN_GA(x1)
PF_IN_AAAGAA(x1, x2, x3, x4, x5, x6) = PF_IN_AAAGAA(x4)
U14_AAAGAA(x1, x2, x3, x4, x5, x6, x7) = U14_AAAGAA(x4, x7)
PM_IN_GGAA(x1, x2, x3, x4) = PM_IN_GGAA(x1, x2)
U16_GGAA(x1, x2, x3, x4, x5) = U16_GGAA(x1, x2, x5)

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:

PF_IN_AAAGAA(T83) → U14_AAAGAA(T83, appC_in_aaag(T83))
U14_AAAGAA(T83, appC_out_aaag(T92, T86, T93, T83)) → PM_IN_GGAA(T92, T93)
PM_IN_GGAA(T92, T93) → U16_GGAA(T92, T93, appD_in_gga(T92, T93))
U16_GGAA(T92, T93, appD_out_gga(T92, T93, T101)) → PERME_IN_GA(T101)
PERME_IN_GA(T83) → PF_IN_AAAGAA(T83)

The TRS R consists of the following rules:

appC_in_aaag(.(T39, T40)) → appC_out_aaag([], T39, T40, .(T39, T40))
appC_in_aaag(.(T48, T49)) → U2_aaag(T48, T49, appC_in_aaag(T49))
appD_in_gga([], T64) → appD_out_gga([], T64, T64)
appD_in_gga(.(T71, T72), T73) → U3_gga(T71, T72, T73, appD_in_gga(T72, T73))
U2_aaag(T48, T49, appC_out_aaag(X63, T50, X64, T49)) → appC_out_aaag(.(T48, X63), T50, X64, .(T48, T49))
U3_gga(T71, T72, T73, appD_out_gga(T72, T73, X92)) → appD_out_gga(.(T71, T72), T73, .(T71, X92))

The set Q consists of the following terms:

appC_in_aaag(x0)
appD_in_gga(x0, x1)
U2_aaag(x0, x1, x2)
U3_gga(x0, x1, x2, x3)

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

(40) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

PERME_IN_GA(T83) → PF_IN_AAAGAA(T83)

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

POL(.(x₁, x₂)) = 1 + x₂
POL(PERME_IN_GA(x₁)) = 1 + x₁
POL(PF_IN_AAAGAA(x₁)) = x₁
POL(PM_IN_GGAA(x₁, x₂)) = x₁ + x₂
POL(U14_AAAGAA(x₁, x₂)) = x₂
POL(U16_GGAA(x₁, x₂, x₃)) = x₃
POL(U2_aaag(x₁, x₂, x₃)) = 1 + x₃
POL(U3_gga(x₁, x₂, x₃, x₄)) = 1 + x₄
POL([]) = 1
POL(appC_in_aaag(x₁)) = x₁
POL(appC_out_aaag(x₁, x₂, x₃, x₄)) = x₁ + x₃
POL(appD_in_gga(x₁, x₂)) = x₁ + x₂
POL(appD_out_gga(x₁, x₂, x₃)) = 1 + x₃

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

appC_in_aaag(.(T39, T40)) → appC_out_aaag([], T39, T40, .(T39, T40))
appC_in_aaag(.(T48, T49)) → U2_aaag(T48, T49, appC_in_aaag(T49))
appD_in_gga([], T64) → appD_out_gga([], T64, T64)
appD_in_gga(.(T71, T72), T73) → U3_gga(T71, T72, T73, appD_in_gga(T72, T73))
U2_aaag(T48, T49, appC_out_aaag(X63, T50, X64, T49)) → appC_out_aaag(.(T48, X63), T50, X64, .(T48, T49))
U3_gga(T71, T72, T73, appD_out_gga(T72, T73, X92)) → appD_out_gga(.(T71, T72), T73, .(T71, X92))

(41) Obligation:

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

PF_IN_AAAGAA(T83) → U14_AAAGAA(T83, appC_in_aaag(T83))
U14_AAAGAA(T83, appC_out_aaag(T92, T86, T93, T83)) → PM_IN_GGAA(T92, T93)
PM_IN_GGAA(T92, T93) → U16_GGAA(T92, T93, appD_in_gga(T92, T93))
U16_GGAA(T92, T93, appD_out_gga(T92, T93, T101)) → PERME_IN_GA(T101)

The TRS R consists of the following rules:

appC_in_aaag(.(T39, T40)) → appC_out_aaag([], T39, T40, .(T39, T40))
appC_in_aaag(.(T48, T49)) → U2_aaag(T48, T49, appC_in_aaag(T49))
appD_in_gga([], T64) → appD_out_gga([], T64, T64)
appD_in_gga(.(T71, T72), T73) → U3_gga(T71, T72, T73, appD_in_gga(T72, T73))
U2_aaag(T48, T49, appC_out_aaag(X63, T50, X64, T49)) → appC_out_aaag(.(T48, X63), T50, X64, .(T48, T49))
U3_gga(T71, T72, T73, appD_out_gga(T72, T73, X92)) → appD_out_gga(.(T71, T72), T73, .(T71, X92))

The set Q consists of the following terms:

appC_in_aaag(x0)
appD_in_gga(x0, x1)
U2_aaag(x0, x1, x2)
U3_gga(x0, x1, x2, x3)

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

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

(18) Obligation:

(19) QDPSizeChangeProof (EQUIVALENT transformation)

(20) YES

(21) Obligation:

(22) UsableRulesProof (EQUIVALENT transformation)

(23) Obligation:

(24) PiDPToQDPProof (SOUND transformation)

(25) Obligation:

(26) QDPSizeChangeProof (EQUIVALENT transformation)

(27) YES

(28) Obligation:

(29) UsableRulesProof (EQUIVALENT transformation)

(30) Obligation:

(31) PiDPToQDPProof (SOUND transformation)

(32) Obligation:

(33) QDPSizeChangeProof (EQUIVALENT transformation)

(34) YES

(35) Obligation:

(36) UsableRulesProof (EQUIVALENT transformation)

(37) Obligation:

(38) PiDPToQDPProof (SOUND transformation)

(39) Obligation:

(40) QDPOrderProof (EQUIVALENT transformation)

(41) Obligation:

(42) DependencyGraphProof (EQUIVALENT transformation)

(43) TRUE