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

(0) Obligation:

Clauses:

ordered([]) :- !.
ordered(.(X1, [])) :- !.
ordered(Xs) :- ','(head(Xs, X), ','(tail(Xs, Ys), ','(head(Ys, Y), ','(tail(Ys, Zs), ','(less(X, s(Y)), ordered(.(Y, Zs))))))).
head([], X2).
head(.(X, X3), X).
tail([], []).
tail(.(X4, Xs), Xs).
less(0, Y) :- ','(!, eq(Y, s(X5))).
less(X, Y) :- ','(p(X, Px), ','(p(Y, Py), less(Px, Py))).
p(0, 0).
p(s(X), X).
eq(X, X).

Query: ordered(g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="A: ordered(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: ordered(T1), SCOPE: 1, CLAUSE: 0 | ordered(T1), SCOPE: 1, CLAUSE: 1 | ordered(T1), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: !_1 | ordered([]), SCOPE: 1, CLAUSE: 1 | ordered([]), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ordered(T1), SCOPE: 1, CLAUSE: 1 | ordered(T1), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nordered(T1) !=? ordered([])", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: !_1 | ordered(.(T3, [])), SCOPE: 1, CLAUSE: 2\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ordered(T1), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nX7 is free\nordered(T1) !=? ordered([])\nordered(T1) !=? ordered(.(X7, []))", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(head(T5, X10), ','(tail(T5, X11), ','(head(X11, X12), ','(tail(X11, X13), ','(less(X10, s(X12)), ordered(.(X12, X13)))))))\n\nT5 is ground\nX7 is free\nX10 is free\nX11 is free\nX12 is free\nX13 is free\nordered(T5) !=? ordered([])\nordered(T5) !=? ordered(.(X7, []))", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(head(T5, X10), ','(tail(T5, X11), ','(head(X11, X12), ','(tail(X11, X13), ','(less(X10, s(X12)), ordered(.(X12, X13))))))), SCOPE: 2, CLAUSE: 3 | ','(head(T5, X10), ','(tail(T5, X11), ','(head(X11, X12), ','(tail(X11, X13), ','(less(X10, s(X12)), ordered(.(X12, X13))))))), SCOPE: 2, CLAUSE: 4\n\nT5 is ground\nX7 is free\nX10 is free\nX11 is free\nX12 is free\nX13 is free\nordered(T5) !=? ordered([])\nordered(T5) !=? ordered(.(X7, []))", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(head(T5, X10), ','(tail(T5, X11), ','(head(X11, X12), ','(tail(X11, X13), ','(less(X10, s(X12)), ordered(.(X12, X13))))))), SCOPE: 2, CLAUSE: 4\n\nT5 is ground\nX7 is free\nX10 is free\nX11 is free\nX12 is free\nX13 is free\nordered(T5) !=? ordered([])\nordered(T5) !=? ordered(.(X7, []))", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ','(tail(.(T10, T11), X11), ','(head(X11, X12), ','(tail(X11, X13), ','(less(T10, s(X12)), ordered(.(X12, X13))))))\n\nT10 is ground\nT11 is ground\nX7 is free\nX11 is free\nX12 is free\nX13 is free\nordered(.(T10, T11)) !=? ordered(.(X7, []))", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(tail(.(T10, T11), X11), ','(head(X11, X12), ','(tail(X11, X13), ','(less(T10, s(X12)), ordered(.(X12, X13)))))), SCOPE: 3, CLAUSE: 5 | ','(tail(.(T10, T11), X11), ','(head(X11, X12), ','(tail(X11, X13), ','(less(T10, s(X12)), ordered(.(X12, X13)))))), SCOPE: 3, CLAUSE: 6\n\nT10 is ground\nT11 is ground\nX7 is free\nX11 is free\nX12 is free\nX13 is free\nordered(.(T10, T11)) !=? ordered(.(X7, []))", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: ','(tail(.(T10, T11), X11), ','(head(X11, X12), ','(tail(X11, X13), ','(less(T10, s(X12)), ordered(.(X12, X13)))))), SCOPE: 3, CLAUSE: 6\n\nT10 is ground\nT11 is ground\nX7 is free\nX11 is free\nX12 is free\nX13 is free\nordered(.(T10, T11)) !=? ordered(.(X7, []))", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(head(T17, X12), ','(tail(T17, X13), ','(less(T16, s(X12)), ordered(.(X12, X13)))))\n\nT16 is ground\nT17 is ground\nX7 is free\nX12 is free\nX13 is free\nordered(.(T16, T17)) !=? ordered(.(X7, []))", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ','(head(T17, X12), ','(tail(T17, X13), ','(less(T16, s(X12)), ordered(.(X12, X13))))), SCOPE: 4, CLAUSE: 3 | ','(head(T17, X12), ','(tail(T17, X13), ','(less(T16, s(X12)), ordered(.(X12, X13))))), SCOPE: 4, CLAUSE: 4\n\nT16 is ground\nT17 is ground\nX7 is free\nX12 is free\nX13 is free\nordered(.(T16, T17)) !=? ordered(.(X7, []))", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: ','(head(T17, X12), ','(tail(T17, X13), ','(less(T16, s(X12)), ordered(.(X12, X13))))), SCOPE: 4, CLAUSE: 4\n\nT16 is ground\nT17 is ground\nX7 is free\nX12 is free\nX13 is free\nordered(.(T16, T17)) !=? ordered(.(X7, []))", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(tail(.(T22, T23), X13), ','(less(T16, s(T22)), ordered(.(T22, X13))))\n\nT16 is ground\nT22 is ground\nT23 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(tail(.(T22, T23), X13), ','(less(T16, s(T22)), ordered(.(T22, X13)))), SCOPE: 5, CLAUSE: 5 | ','(tail(.(T22, T23), X13), ','(less(T16, s(T22)), ordered(.(T22, X13)))), SCOPE: 5, CLAUSE: 6\n\nT16 is ground\nT22 is ground\nT23 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(tail(.(T22, T23), X13), ','(less(T16, s(T22)), ordered(.(T22, X13)))), SCOPE: 5, CLAUSE: 6\n\nT16 is ground\nT22 is ground\nT23 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="B: ','(less(T16, s(T30)), ordered(.(T30, T31)))\n\nT16 is ground\nT30 is ground\nT31 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="E: less(T16, s(T30))\n\nT16 is ground\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ordered(.(T30, T31))\n\nT30 is ground\nT31 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: less(T16, s(T30)), SCOPE: 6, CLAUSE: 7 | less(T16, s(T30)), SCOPE: 6, CLAUSE: 8\n\nT16 is ground\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ','(!_6, eq(s(T36), s(X63))) | less(0, s(T36)), SCOPE: 6, CLAUSE: 8\n\nT36 is ground\nX63 is free", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: less(T16, s(T30)), SCOPE: 6, CLAUSE: 8\n\nT16 is ground\nT30 is ground\nX62 is free\nless(T16, s(T30)) !=? less(0, X62)", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: eq(s(T36), s(X63))\n\nT36 is ground\nX63 is free", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: eq(s(T36), s(X63)), SCOPE: 7, CLAUSE: 11\n\nT36 is ground\nX63 is free", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ','(p(T44, X78), ','(p(s(T45), X79), less(X78, X79)))\n\nT44 is ground\nT45 is ground\nX62 is free\nX78 is free\nX79 is free\nless(T44, s(T45)) !=? less(0, X62)", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ','(p(T44, X78), ','(p(s(T45), X79), less(X78, X79))), SCOPE: 8, CLAUSE: 9 | ','(p(T44, X78), ','(p(s(T45), X79), less(X78, X79))), SCOPE: 8, CLAUSE: 10\n\nT44 is ground\nT45 is ground\nX62 is free\nX78 is free\nX79 is free\nless(T44, s(T45)) !=? less(0, X62)", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(p(T44, X78), ','(p(s(T45), X79), less(X78, X79))), SCOPE: 8, CLAUSE: 10\n\nT44 is ground\nT45 is ground\nX62 is free\nX78 is free\nX79 is free\nless(T44, s(T45)) !=? less(0, X62)", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ','(p(s(T45), X79), less(T48, X79))\n\nT45 is ground\nT48 is ground\nX79 is free", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: ','(p(s(T45), X79), less(T48, X79)), SCOPE: 9, CLAUSE: 9 | ','(p(s(T45), X79), less(T48, X79)), SCOPE: 9, CLAUSE: 10\n\nT45 is ground\nT48 is ground\nX79 is free", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: ','(p(s(T45), X79), less(T48, X79)), SCOPE: 9, CLAUSE: 10\n\nT45 is ground\nT48 is ground\nX79 is free", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="D: less(T48, T52)\n\nT48 is ground\nT52 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: less(T48, T52), SCOPE: 10, CLAUSE: 7 | less(T48, T52), SCOPE: 10, CLAUSE: 8\n\nT48 is ground\nT52 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: ','(!_10, eq(T56, s(X100))) | less(0, T56), SCOPE: 10, CLAUSE: 8\n\nT56 is ground\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: less(T48, T52), SCOPE: 10, CLAUSE: 8\n\nT48 is ground\nT52 is ground\nX99 is free\nless(T48, T52) !=? less(0, X99)", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: eq(T56, s(X100))\n\nT56 is ground\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: eq(T56, s(X100)), SCOPE: 11, CLAUSE: 11\n\nT56 is ground\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: ','(p(T67, X115), ','(p(T68, X116), less(X115, X116)))\n\nT67 is ground\nT68 is ground\nX99 is free\nX115 is free\nX116 is free\nless(T67, T68) !=? less(0, X99)", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: ','(p(T67, X115), ','(p(T68, X116), less(X115, X116))), SCOPE: 12, CLAUSE: 9 | ','(p(T67, X115), ','(p(T68, X116), less(X115, X116))), SCOPE: 12, CLAUSE: 10\n\nT67 is ground\nT68 is ground\nX99 is free\nX115 is free\nX116 is free\nless(T67, T68) !=? less(0, X99)", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: ','(p(T67, X115), ','(p(T68, X116), less(X115, X116))), SCOPE: 12, CLAUSE: 10\n\nT67 is ground\nT68 is ground\nX99 is free\nX115 is free\nX116 is free\nless(T67, T68) !=? less(0, X99)", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: ','(p(T68, X116), less(T71, X116))\n\nT68 is ground\nT71 is ground\nX116 is free", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: ','(p(T68, X116), less(T71, X116)), SCOPE: 13, CLAUSE: 9 | ','(p(T68, X116), less(T71, X116)), SCOPE: 13, CLAUSE: 10\n\nT68 is ground\nT71 is ground\nX116 is free", fontsize=16, style=filled, fillcolor=lightyellow];
151 [label="151: ','(p(T68, X116), less(T71, X116)), SCOPE: 13, CLAUSE: 9\n\nT68 is ground\nT71 is ground\nX116 is free", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: ','(p(T68, X116), less(T71, X116)), SCOPE: 13, CLAUSE: 10\n\nT68 is ground\nT71 is ground\nX116 is free", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="C: less(T71, 0)\n\nT71 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
158 [label="158: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: less(T71, 0), SCOPE: 14, CLAUSE: 7 | less(T71, 0), SCOPE: 14, CLAUSE: 8\n\nT71 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: ','(!_14, eq(0, s(X132))) | less(0, 0), SCOPE: 14, CLAUSE: 8\n\nX132 is free", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: less(T71, 0), SCOPE: 14, CLAUSE: 8\n\nT71 is ground\nX131 is free\nless(T71, 0) !=? less(0, X131)", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: eq(0, s(X132))\n\nX132 is free", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: eq(0, s(X132)), SCOPE: 15, CLAUSE: 11\n\nX132 is free", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: ','(p(T74, X145), ','(p(0, X146), less(X145, X146)))\n\nT74 is ground\nX131 is free\nX145 is free\nX146 is free\nless(T74, 0) !=? less(0, X131)", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: ','(p(T74, X145), ','(p(0, X146), less(X145, X146))), SCOPE: 16, CLAUSE: 9 | ','(p(T74, X145), ','(p(0, X146), less(X145, X146))), SCOPE: 16, CLAUSE: 10\n\nT74 is ground\nX131 is free\nX145 is free\nX146 is free\nless(T74, 0) !=? less(0, X131)", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: ','(p(T74, X145), ','(p(0, X146), less(X145, X146))), SCOPE: 16, CLAUSE: 10\n\nT74 is ground\nX131 is free\nX145 is free\nX146 is free\nless(T74, 0) !=? less(0, X131)", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: ','(p(0, X146), less(T77, X146))\n\nT77 is ground\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: ','(p(0, X146), less(T77, X146)), SCOPE: 17, CLAUSE: 9 | ','(p(0, X146), less(T77, X146)), SCOPE: 17, CLAUSE: 10\n\nT77 is ground\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
199 [label="199: ','(p(0, X146), less(T77, X146)), SCOPE: 17, CLAUSE: 9\n\nT77 is ground\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: ','(p(0, X146), less(T77, X146)), SCOPE: 17, CLAUSE: 10\n\nT77 is ground\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: less(T77, 0)\n\nT77 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
212 [label="212: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: less(T71, T80)\n\nT71 is ground\nT80 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 218 [arrowhead = none ];
218 -> 5;

219 [label="EVAL with clause\nordered([]) :- !_1.\nand substitutionT1 -> []", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 219 [arrowhead = none ];
219 -> 8;

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

221 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
8 -> 221 [arrowhead = none ];
221 -> 14;

222 [label="EVAL with clause\nordered(.(X7, [])) :- !_1.\nand substitutionX7 -> T3,\nT1 -> .(T3, [])", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 222 [arrowhead = none ];
222 -> 19;

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

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

225 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 225 [arrowhead = none ];
225 -> 25;

226 [label="ONLY EVAL with clause\nordered(X9) :- ','(head(X9, X10), ','(tail(X9, X11), ','(head(X11, X12), ','(tail(X11, X13), ','(less(X10, s(X12)), ordered(.(X12, X13))))))).\nand substitutionT1 -> T5,\nX9 -> T5", fontsize=14, style = filled, fillcolor = lightblue];
22 -> 226 [arrowhead = none ];
226 -> 31;

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

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

229 [label="BACKTRACK\nfor clause: head([], X2)\nwith clash: (ordered(T5), ordered([]))", fontsize=14, style = filled, fillcolor = lightgreen];
34 -> 229 [arrowhead = none ];
229 -> 36;

230 [label="EVAL with clause\nhead(.(X20, X21), X20).\nand substitutionX20 -> T10,\nX21 -> T11,\nT5 -> .(T10, T11),\nX10 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 230 [arrowhead = none ];
230 -> 40;

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

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

233 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
44 -> 233 [arrowhead = none ];
233 -> 45;

234 [label="ONLY EVAL with clause\ntail(.(X32, X33), X33).\nand substitutionT10 -> T16,\nX32 -> T16,\nT11 -> T17,\nX33 -> T17,\nX11 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
45 -> 234 [arrowhead = none ];
234 -> 49;

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

236 [label="BACKTRACK\nfor clause: head([], X2)\nwith clash: (ordered(.(T16, T17)), ordered(.(X7, [])))", fontsize=14, style = filled, fillcolor = lightgreen];
51 -> 236 [arrowhead = none ];
236 -> 52;

237 [label="EVAL with clause\nhead(.(X43, X44), X43).\nand substitutionX43 -> T22,\nX44 -> T23,\nT17 -> .(T22, T23),\nX12 -> T22", fontsize=14, style = filled, fillcolor = lightblue];
52 -> 237 [arrowhead = none ];
237 -> 55;

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

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

240 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 240 [arrowhead = none ];
240 -> 60;

241 [label="ONLY EVAL with clause\ntail(.(X53, X54), X54).\nand substitutionT22 -> T30,\nX53 -> T30,\nT23 -> T31,\nX54 -> T31,\nX13 -> T31", fontsize=14, style = filled, fillcolor = lightblue];
60 -> 241 [arrowhead = none ];
241 -> 64;

242 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
64 -> 242 [arrowhead = none ];
242 -> 69;

243 [label="SPLIT 2\nnew knowledge:\nT16 is ground\nT30 is ground", fontsize=14, style = filled, fillcolor = violet];
64 -> 243 [arrowhead = none ];
243 -> 71;

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

245 [label="INSTANCE with matching:\nT1 -> .(T30, T31)", fontsize=14, style = filled, fillcolor = lightgrey];
71 -> 245 [arrowhead = none , style=dashed];
245 -> 2[style=dashed];

246 [label="EVAL with clause\nless(0, X62) :- ','(!_6, eq(X62, s(X63))).\nand substitutionT16 -> 0,\nT30 -> T36,\nX62 -> s(T36)", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 246 [arrowhead = none ];
246 -> 77;

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

248 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
77 -> 248 [arrowhead = none ];
248 -> 80;

249 [label="ONLY EVAL with clause\nless(X76, X77) :- ','(p(X76, X78), ','(p(X77, X79), less(X78, X79))).\nand substitutionT16 -> T44,\nX76 -> T44,\nT30 -> T45,\nX77 -> s(T45)", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 249 [arrowhead = none ];
249 -> 93;

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

251 [label="ONLY EVAL with clause\neq(X66, X66).\nand substitutionT36 -> T39,\nX66 -> s(T39),\nX63 -> T39", fontsize=14, style = filled, fillcolor = lightblue];
82 -> 251 [arrowhead = none ];
251 -> 85;

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

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

254 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (less(T44, s(T45)), less(0, X62))", fontsize=14, style = filled, fillcolor = lightgreen];
95 -> 254 [arrowhead = none ];
254 -> 96;

255 [label="EVAL with clause\np(s(X85), X85).\nand substitutionX85 -> T48,\nT44 -> s(T48),\nX78 -> T48", fontsize=14, style = filled, fillcolor = lightblue];
96 -> 255 [arrowhead = none ];
255 -> 100;

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

257 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
100 -> 257 [arrowhead = none ];
257 -> 103;

258 [label="BACKTRACK\nfor clause: p(0, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
103 -> 258 [arrowhead = none ];
258 -> 104;

259 [label="ONLY EVAL with clause\np(s(X93), X93).\nand substitutionT45 -> T52,\nX93 -> T52,\nX79 -> T52", fontsize=14, style = filled, fillcolor = lightblue];
104 -> 259 [arrowhead = none ];
259 -> 109;

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

261 [label="EVAL with clause\nless(0, X99) :- ','(!_10, eq(X99, s(X100))).\nand substitutionT48 -> 0,\nT52 -> T56,\nX99 -> T56", fontsize=14, style = filled, fillcolor = lightblue];
110 -> 261 [arrowhead = none ];
261 -> 114;

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

263 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
114 -> 263 [arrowhead = none ];
263 -> 117;

264 [label="ONLY EVAL with clause\nless(X113, X114) :- ','(p(X113, X115), ','(p(X114, X116), less(X115, X116))).\nand substitutionT48 -> T67,\nX113 -> T67,\nT52 -> T68,\nX114 -> T68", fontsize=14, style = filled, fillcolor = lightblue];
116 -> 264 [arrowhead = none ];
264 -> 135;

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

266 [label="EVAL with clause\neq(X103, X103).\nand substitutionT56 -> s(T62),\nX103 -> s(T62),\nX100 -> T62,\nT61 -> s(T62)", fontsize=14, style = filled, fillcolor = lightblue];
118 -> 266 [arrowhead = none ];
266 -> 123;

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

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

269 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
135 -> 269 [arrowhead = none ];
269 -> 138;

270 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (less(T67, T68), less(0, X99))", fontsize=14, style = filled, fillcolor = lightgreen];
138 -> 270 [arrowhead = none ];
270 -> 140;

271 [label="EVAL with clause\np(s(X122), X122).\nand substitutionX122 -> T71,\nT67 -> s(T71),\nX115 -> T71", fontsize=14, style = filled, fillcolor = lightblue];
140 -> 271 [arrowhead = none ];
271 -> 144;

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

273 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
144 -> 273 [arrowhead = none ];
273 -> 149;

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

275 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
149 -> 275 [arrowhead = none ];
275 -> 153;

276 [label="EVAL with clause\np(0, 0).\nand substitutionT68 -> 0,\nX116 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
151 -> 276 [arrowhead = none ];
276 -> 156;

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

278 [label="EVAL with clause\np(s(X165), X165).\nand substitutionX165 -> T80,\nT68 -> s(T80),\nX116 -> T80", fontsize=14, style = filled, fillcolor = lightblue];
153 -> 278 [arrowhead = none ];
278 -> 215;

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

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

281 [label="EVAL with clause\nless(0, X131) :- ','(!_14, eq(X131, s(X132))).\nand substitutionT71 -> 0,\nX131 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
164 -> 281 [arrowhead = none ];
281 -> 168;

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

283 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
168 -> 283 [arrowhead = none ];
283 -> 172;

284 [label="ONLY EVAL with clause\nless(X143, X144) :- ','(p(X143, X145), ','(p(X144, X146), less(X145, X146))).\nand substitutionT71 -> T74,\nX143 -> T74,\nX144 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
170 -> 284 [arrowhead = none ];
284 -> 183;

285 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
172 -> 285 [arrowhead = none ];
285 -> 174;

286 [label="BACKTRACK\nfor clause: eq(X, X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
174 -> 286 [arrowhead = none ];
286 -> 176;

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

288 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (less(T74, 0), less(0, X131))", fontsize=14, style = filled, fillcolor = lightgreen];
185 -> 288 [arrowhead = none ];
288 -> 187;

289 [label="EVAL with clause\np(s(X152), X152).\nand substitutionX152 -> T77,\nT74 -> s(T77),\nX145 -> T77", fontsize=14, style = filled, fillcolor = lightblue];
187 -> 289 [arrowhead = none ];
289 -> 192;

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

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

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

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

294 [label="ONLY EVAL with clause\np(0, 0).\nand substitutionX146 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
199 -> 294 [arrowhead = none ];
294 -> 204;

295 [label="BACKTRACK\nfor clause: p(s(X), X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
200 -> 295 [arrowhead = none ];
295 -> 212;

296 [label="INSTANCE with matching:\nT71 -> T77", fontsize=14, style = filled, fillcolor = lightgrey];
204 -> 296 [arrowhead = none , style=dashed];
296 -> 156[style=dashed];

297 [label="INSTANCE with matching:\nT48 -> T71\nT52 -> T80", fontsize=14, style = filled, fillcolor = lightgrey];
215 -> 297 [arrowhead = none , style=dashed];
297 -> 109[style=dashed];

}

(2) Obligation:

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

orderedA_in_g([]) → orderedA_out_g([])
orderedA_in_g(.(T3, [])) → orderedA_out_g(.(T3, []))
orderedA_in_g(.(T16, .(T30, T31))) → U1_g(T16, T30, T31, pB_in_ggg(T16, T30, T31))
pB_in_ggg(T16, T30, T31) → U6_ggg(T16, T30, T31, lessE_in_gg(T16, T30))
lessE_in_gg(0, T39) → lessE_out_gg(0, T39)
lessE_in_gg(s(T48), T52) → U5_gg(T48, T52, lessD_in_gg(T48, T52))
lessD_in_gg(0, s(T62)) → lessD_out_gg(0, s(T62))
lessD_in_gg(s(T71), 0) → U3_gg(T71, lessC_in_g(T71))
lessC_in_g(s(T77)) → U2_g(T77, lessC_in_g(T77))
U2_g(T77, lessC_out_g(T77)) → lessC_out_g(s(T77))
U3_gg(T71, lessC_out_g(T71)) → lessD_out_gg(s(T71), 0)
lessD_in_gg(s(T71), s(T80)) → U4_gg(T71, T80, lessD_in_gg(T71, T80))
U4_gg(T71, T80, lessD_out_gg(T71, T80)) → lessD_out_gg(s(T71), s(T80))
U5_gg(T48, T52, lessD_out_gg(T48, T52)) → lessE_out_gg(s(T48), T52)
U6_ggg(T16, T30, T31, lessE_out_gg(T16, T30)) → U7_ggg(T16, T30, T31, orderedA_in_g(.(T30, T31)))
U7_ggg(T16, T30, T31, orderedA_out_g(.(T30, T31))) → pB_out_ggg(T16, T30, T31)
U1_g(T16, T30, T31, pB_out_ggg(T16, T30, T31)) → orderedA_out_g(.(T16, .(T30, T31)))

Pi is empty.

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

ORDEREDA_IN_G(.(T16, .(T30, T31))) → U1_G(T16, T30, T31, pB_in_ggg(T16, T30, T31))
ORDEREDA_IN_G(.(T16, .(T30, T31))) → PB_IN_GGG(T16, T30, T31)
PB_IN_GGG(T16, T30, T31) → U6_GGG(T16, T30, T31, lessE_in_gg(T16, T30))
PB_IN_GGG(T16, T30, T31) → LESSE_IN_GG(T16, T30)
LESSE_IN_GG(s(T48), T52) → U5_GG(T48, T52, lessD_in_gg(T48, T52))
LESSE_IN_GG(s(T48), T52) → LESSD_IN_GG(T48, T52)
LESSD_IN_GG(s(T71), 0) → U3_GG(T71, lessC_in_g(T71))
LESSD_IN_GG(s(T71), 0) → LESSC_IN_G(T71)
LESSC_IN_G(s(T77)) → U2_G(T77, lessC_in_g(T77))
LESSC_IN_G(s(T77)) → LESSC_IN_G(T77)
LESSD_IN_GG(s(T71), s(T80)) → U4_GG(T71, T80, lessD_in_gg(T71, T80))
LESSD_IN_GG(s(T71), s(T80)) → LESSD_IN_GG(T71, T80)
U6_GGG(T16, T30, T31, lessE_out_gg(T16, T30)) → U7_GGG(T16, T30, T31, orderedA_in_g(.(T30, T31)))
U6_GGG(T16, T30, T31, lessE_out_gg(T16, T30)) → ORDEREDA_IN_G(.(T30, T31))

The TRS R consists of the following rules:

orderedA_in_g([]) → orderedA_out_g([])
orderedA_in_g(.(T3, [])) → orderedA_out_g(.(T3, []))
orderedA_in_g(.(T16, .(T30, T31))) → U1_g(T16, T30, T31, pB_in_ggg(T16, T30, T31))
pB_in_ggg(T16, T30, T31) → U6_ggg(T16, T30, T31, lessE_in_gg(T16, T30))
lessE_in_gg(0, T39) → lessE_out_gg(0, T39)
lessE_in_gg(s(T48), T52) → U5_gg(T48, T52, lessD_in_gg(T48, T52))
lessD_in_gg(0, s(T62)) → lessD_out_gg(0, s(T62))
lessD_in_gg(s(T71), 0) → U3_gg(T71, lessC_in_g(T71))
lessC_in_g(s(T77)) → U2_g(T77, lessC_in_g(T77))
U2_g(T77, lessC_out_g(T77)) → lessC_out_g(s(T77))
U3_gg(T71, lessC_out_g(T71)) → lessD_out_gg(s(T71), 0)
lessD_in_gg(s(T71), s(T80)) → U4_gg(T71, T80, lessD_in_gg(T71, T80))
U4_gg(T71, T80, lessD_out_gg(T71, T80)) → lessD_out_gg(s(T71), s(T80))
U5_gg(T48, T52, lessD_out_gg(T48, T52)) → lessE_out_gg(s(T48), T52)
U6_ggg(T16, T30, T31, lessE_out_gg(T16, T30)) → U7_ggg(T16, T30, T31, orderedA_in_g(.(T30, T31)))
U7_ggg(T16, T30, T31, orderedA_out_g(.(T30, T31))) → pB_out_ggg(T16, T30, T31)
U1_g(T16, T30, T31, pB_out_ggg(T16, T30, T31)) → orderedA_out_g(.(T16, .(T30, T31)))

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

(4) Obligation:

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

ORDEREDA_IN_G(.(T16, .(T30, T31))) → U1_G(T16, T30, T31, pB_in_ggg(T16, T30, T31))
ORDEREDA_IN_G(.(T16, .(T30, T31))) → PB_IN_GGG(T16, T30, T31)
PB_IN_GGG(T16, T30, T31) → U6_GGG(T16, T30, T31, lessE_in_gg(T16, T30))
PB_IN_GGG(T16, T30, T31) → LESSE_IN_GG(T16, T30)
LESSE_IN_GG(s(T48), T52) → U5_GG(T48, T52, lessD_in_gg(T48, T52))
LESSE_IN_GG(s(T48), T52) → LESSD_IN_GG(T48, T52)
LESSD_IN_GG(s(T71), 0) → U3_GG(T71, lessC_in_g(T71))
LESSD_IN_GG(s(T71), 0) → LESSC_IN_G(T71)
LESSC_IN_G(s(T77)) → U2_G(T77, lessC_in_g(T77))
LESSC_IN_G(s(T77)) → LESSC_IN_G(T77)
LESSD_IN_GG(s(T71), s(T80)) → U4_GG(T71, T80, lessD_in_gg(T71, T80))
LESSD_IN_GG(s(T71), s(T80)) → LESSD_IN_GG(T71, T80)
U6_GGG(T16, T30, T31, lessE_out_gg(T16, T30)) → U7_GGG(T16, T30, T31, orderedA_in_g(.(T30, T31)))
U6_GGG(T16, T30, T31, lessE_out_gg(T16, T30)) → ORDEREDA_IN_G(.(T30, T31))

The TRS R consists of the following rules:

orderedA_in_g([]) → orderedA_out_g([])
orderedA_in_g(.(T3, [])) → orderedA_out_g(.(T3, []))
orderedA_in_g(.(T16, .(T30, T31))) → U1_g(T16, T30, T31, pB_in_ggg(T16, T30, T31))
pB_in_ggg(T16, T30, T31) → U6_ggg(T16, T30, T31, lessE_in_gg(T16, T30))
lessE_in_gg(0, T39) → lessE_out_gg(0, T39)
lessE_in_gg(s(T48), T52) → U5_gg(T48, T52, lessD_in_gg(T48, T52))
lessD_in_gg(0, s(T62)) → lessD_out_gg(0, s(T62))
lessD_in_gg(s(T71), 0) → U3_gg(T71, lessC_in_g(T71))
lessC_in_g(s(T77)) → U2_g(T77, lessC_in_g(T77))
U2_g(T77, lessC_out_g(T77)) → lessC_out_g(s(T77))
U3_gg(T71, lessC_out_g(T71)) → lessD_out_gg(s(T71), 0)
lessD_in_gg(s(T71), s(T80)) → U4_gg(T71, T80, lessD_in_gg(T71, T80))
U4_gg(T71, T80, lessD_out_gg(T71, T80)) → lessD_out_gg(s(T71), s(T80))
U5_gg(T48, T52, lessD_out_gg(T48, T52)) → lessE_out_gg(s(T48), T52)
U6_ggg(T16, T30, T31, lessE_out_gg(T16, T30)) → U7_ggg(T16, T30, T31, orderedA_in_g(.(T30, T31)))
U7_ggg(T16, T30, T31, orderedA_out_g(.(T30, T31))) → pB_out_ggg(T16, T30, T31)
U1_g(T16, T30, T31, pB_out_ggg(T16, T30, T31)) → orderedA_out_g(.(T16, .(T30, T31)))

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

LESSC_IN_G(s(T77)) → LESSC_IN_G(T77)

The TRS R consists of the following rules:

orderedA_in_g([]) → orderedA_out_g([])
orderedA_in_g(.(T3, [])) → orderedA_out_g(.(T3, []))
orderedA_in_g(.(T16, .(T30, T31))) → U1_g(T16, T30, T31, pB_in_ggg(T16, T30, T31))
pB_in_ggg(T16, T30, T31) → U6_ggg(T16, T30, T31, lessE_in_gg(T16, T30))
lessE_in_gg(0, T39) → lessE_out_gg(0, T39)
lessE_in_gg(s(T48), T52) → U5_gg(T48, T52, lessD_in_gg(T48, T52))
lessD_in_gg(0, s(T62)) → lessD_out_gg(0, s(T62))
lessD_in_gg(s(T71), 0) → U3_gg(T71, lessC_in_g(T71))
lessC_in_g(s(T77)) → U2_g(T77, lessC_in_g(T77))
U2_g(T77, lessC_out_g(T77)) → lessC_out_g(s(T77))
U3_gg(T71, lessC_out_g(T71)) → lessD_out_gg(s(T71), 0)
lessD_in_gg(s(T71), s(T80)) → U4_gg(T71, T80, lessD_in_gg(T71, T80))
U4_gg(T71, T80, lessD_out_gg(T71, T80)) → lessD_out_gg(s(T71), s(T80))
U5_gg(T48, T52, lessD_out_gg(T48, T52)) → lessE_out_gg(s(T48), T52)
U6_ggg(T16, T30, T31, lessE_out_gg(T16, T30)) → U7_ggg(T16, T30, T31, orderedA_in_g(.(T30, T31)))
U7_ggg(T16, T30, T31, orderedA_out_g(.(T30, T31))) → pB_out_ggg(T16, T30, T31)
U1_g(T16, T30, T31, pB_out_ggg(T16, T30, T31)) → orderedA_out_g(.(T16, .(T30, T31)))

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

LESSC_IN_G(s(T77)) → LESSC_IN_G(T77)

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:

LESSC_IN_G(s(T77)) → LESSC_IN_G(T77)

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:

• LESSC_IN_G(s(T77)) → LESSC_IN_G(T77)
  The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

LESSD_IN_GG(s(T71), s(T80)) → LESSD_IN_GG(T71, T80)

The TRS R consists of the following rules:

orderedA_in_g([]) → orderedA_out_g([])
orderedA_in_g(.(T3, [])) → orderedA_out_g(.(T3, []))
orderedA_in_g(.(T16, .(T30, T31))) → U1_g(T16, T30, T31, pB_in_ggg(T16, T30, T31))
pB_in_ggg(T16, T30, T31) → U6_ggg(T16, T30, T31, lessE_in_gg(T16, T30))
lessE_in_gg(0, T39) → lessE_out_gg(0, T39)
lessE_in_gg(s(T48), T52) → U5_gg(T48, T52, lessD_in_gg(T48, T52))
lessD_in_gg(0, s(T62)) → lessD_out_gg(0, s(T62))
lessD_in_gg(s(T71), 0) → U3_gg(T71, lessC_in_g(T71))
lessC_in_g(s(T77)) → U2_g(T77, lessC_in_g(T77))
U2_g(T77, lessC_out_g(T77)) → lessC_out_g(s(T77))
U3_gg(T71, lessC_out_g(T71)) → lessD_out_gg(s(T71), 0)
lessD_in_gg(s(T71), s(T80)) → U4_gg(T71, T80, lessD_in_gg(T71, T80))
U4_gg(T71, T80, lessD_out_gg(T71, T80)) → lessD_out_gg(s(T71), s(T80))
U5_gg(T48, T52, lessD_out_gg(T48, T52)) → lessE_out_gg(s(T48), T52)
U6_ggg(T16, T30, T31, lessE_out_gg(T16, T30)) → U7_ggg(T16, T30, T31, orderedA_in_g(.(T30, T31)))
U7_ggg(T16, T30, T31, orderedA_out_g(.(T30, T31))) → pB_out_ggg(T16, T30, T31)
U1_g(T16, T30, T31, pB_out_ggg(T16, T30, T31)) → orderedA_out_g(.(T16, .(T30, T31)))

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

LESSD_IN_GG(s(T71), s(T80)) → LESSD_IN_GG(T71, T80)

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

(17) PiDPToQDPProof (EQUIVALENT transformation)

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

(18) Obligation:

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

LESSD_IN_GG(s(T71), s(T80)) → LESSD_IN_GG(T71, T80)

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

• LESSD_IN_GG(s(T71), s(T80)) → LESSD_IN_GG(T71, T80)
  The graph contains the following edges 1 > 1, 2 > 2

(20) YES

(21) Obligation:

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

ORDEREDA_IN_G(.(T16, .(T30, T31))) → PB_IN_GGG(T16, T30, T31)
PB_IN_GGG(T16, T30, T31) → U6_GGG(T16, T30, T31, lessE_in_gg(T16, T30))
U6_GGG(T16, T30, T31, lessE_out_gg(T16, T30)) → ORDEREDA_IN_G(.(T30, T31))

The TRS R consists of the following rules:

orderedA_in_g([]) → orderedA_out_g([])
orderedA_in_g(.(T3, [])) → orderedA_out_g(.(T3, []))
orderedA_in_g(.(T16, .(T30, T31))) → U1_g(T16, T30, T31, pB_in_ggg(T16, T30, T31))
pB_in_ggg(T16, T30, T31) → U6_ggg(T16, T30, T31, lessE_in_gg(T16, T30))
lessE_in_gg(0, T39) → lessE_out_gg(0, T39)
lessE_in_gg(s(T48), T52) → U5_gg(T48, T52, lessD_in_gg(T48, T52))
lessD_in_gg(0, s(T62)) → lessD_out_gg(0, s(T62))
lessD_in_gg(s(T71), 0) → U3_gg(T71, lessC_in_g(T71))
lessC_in_g(s(T77)) → U2_g(T77, lessC_in_g(T77))
U2_g(T77, lessC_out_g(T77)) → lessC_out_g(s(T77))
U3_gg(T71, lessC_out_g(T71)) → lessD_out_gg(s(T71), 0)
lessD_in_gg(s(T71), s(T80)) → U4_gg(T71, T80, lessD_in_gg(T71, T80))
U4_gg(T71, T80, lessD_out_gg(T71, T80)) → lessD_out_gg(s(T71), s(T80))
U5_gg(T48, T52, lessD_out_gg(T48, T52)) → lessE_out_gg(s(T48), T52)
U6_ggg(T16, T30, T31, lessE_out_gg(T16, T30)) → U7_ggg(T16, T30, T31, orderedA_in_g(.(T30, T31)))
U7_ggg(T16, T30, T31, orderedA_out_g(.(T30, T31))) → pB_out_ggg(T16, T30, T31)
U1_g(T16, T30, T31, pB_out_ggg(T16, T30, T31)) → orderedA_out_g(.(T16, .(T30, T31)))

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

ORDEREDA_IN_G(.(T16, .(T30, T31))) → PB_IN_GGG(T16, T30, T31)
PB_IN_GGG(T16, T30, T31) → U6_GGG(T16, T30, T31, lessE_in_gg(T16, T30))
U6_GGG(T16, T30, T31, lessE_out_gg(T16, T30)) → ORDEREDA_IN_G(.(T30, T31))

The TRS R consists of the following rules:

lessE_in_gg(0, T39) → lessE_out_gg(0, T39)
lessE_in_gg(s(T48), T52) → U5_gg(T48, T52, lessD_in_gg(T48, T52))
U5_gg(T48, T52, lessD_out_gg(T48, T52)) → lessE_out_gg(s(T48), T52)
lessD_in_gg(0, s(T62)) → lessD_out_gg(0, s(T62))
lessD_in_gg(s(T71), 0) → U3_gg(T71, lessC_in_g(T71))
lessD_in_gg(s(T71), s(T80)) → U4_gg(T71, T80, lessD_in_gg(T71, T80))
U3_gg(T71, lessC_out_g(T71)) → lessD_out_gg(s(T71), 0)
U4_gg(T71, T80, lessD_out_gg(T71, T80)) → lessD_out_gg(s(T71), s(T80))
lessC_in_g(s(T77)) → U2_g(T77, lessC_in_g(T77))
U2_g(T77, lessC_out_g(T77)) → lessC_out_g(s(T77))

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:

ORDEREDA_IN_G(.(T16, .(T30, T31))) → PB_IN_GGG(T16, T30, T31)
PB_IN_GGG(T16, T30, T31) → U6_GGG(T16, T30, T31, lessE_in_gg(T16, T30))
U6_GGG(T16, T30, T31, lessE_out_gg(T16, T30)) → ORDEREDA_IN_G(.(T30, T31))

The TRS R consists of the following rules:

lessE_in_gg(0, T39) → lessE_out_gg(0, T39)
lessE_in_gg(s(T48), T52) → U5_gg(T48, T52, lessD_in_gg(T48, T52))
U5_gg(T48, T52, lessD_out_gg(T48, T52)) → lessE_out_gg(s(T48), T52)
lessD_in_gg(0, s(T62)) → lessD_out_gg(0, s(T62))
lessD_in_gg(s(T71), 0) → U3_gg(T71, lessC_in_g(T71))
lessD_in_gg(s(T71), s(T80)) → U4_gg(T71, T80, lessD_in_gg(T71, T80))
U3_gg(T71, lessC_out_g(T71)) → lessD_out_gg(s(T71), 0)
U4_gg(T71, T80, lessD_out_gg(T71, T80)) → lessD_out_gg(s(T71), s(T80))
lessC_in_g(s(T77)) → U2_g(T77, lessC_in_g(T77))
U2_g(T77, lessC_out_g(T77)) → lessC_out_g(s(T77))

The set Q consists of the following terms:

lessE_in_gg(x0, x1)
U5_gg(x0, x1, x2)
lessD_in_gg(x0, x1)
U3_gg(x0, x1)
U4_gg(x0, x1, x2)
lessC_in_g(x0)
U2_g(x0, x1)

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

(26) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

ORDEREDA_IN_G(.(T16, .(T30, T31))) → PB_IN_GGG(T16, T30, T31)

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

POL(.(x₁, x₂)) = 1 + x₂   
POL(0) = 0   
POL(ORDEREDA_IN_G(x₁)) = x₁   
POL(PB_IN_GGG(x₁, x₂, x₃)) = 1 + x₃   
POL(U2_g(x₁, x₂)) = 0   
POL(U3_gg(x₁, x₂)) = 0   
POL(U4_gg(x₁, x₂, x₃)) = 0   
POL(U5_gg(x₁, x₂, x₃)) = 0   
POL(U6_GGG(x₁, x₂, x₃, x₄)) = 1 + x₃   
POL(lessC_in_g(x₁)) = 0   
POL(lessC_out_g(x₁)) = 0   
POL(lessD_in_gg(x₁, x₂)) = 0   
POL(lessD_out_gg(x₁, x₂)) = 0   
POL(lessE_in_gg(x₁, x₂)) = 0   
POL(lessE_out_gg(x₁, x₂)) = 0   
POL(s(x₁)) = 0   

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

(27) Obligation:

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

PB_IN_GGG(T16, T30, T31) → U6_GGG(T16, T30, T31, lessE_in_gg(T16, T30))
U6_GGG(T16, T30, T31, lessE_out_gg(T16, T30)) → ORDEREDA_IN_G(.(T30, T31))

The TRS R consists of the following rules:

lessE_in_gg(0, T39) → lessE_out_gg(0, T39)
lessE_in_gg(s(T48), T52) → U5_gg(T48, T52, lessD_in_gg(T48, T52))
U5_gg(T48, T52, lessD_out_gg(T48, T52)) → lessE_out_gg(s(T48), T52)
lessD_in_gg(0, s(T62)) → lessD_out_gg(0, s(T62))
lessD_in_gg(s(T71), 0) → U3_gg(T71, lessC_in_g(T71))
lessD_in_gg(s(T71), s(T80)) → U4_gg(T71, T80, lessD_in_gg(T71, T80))
U3_gg(T71, lessC_out_g(T71)) → lessD_out_gg(s(T71), 0)
U4_gg(T71, T80, lessD_out_gg(T71, T80)) → lessD_out_gg(s(T71), s(T80))
lessC_in_g(s(T77)) → U2_g(T77, lessC_in_g(T77))
U2_g(T77, lessC_out_g(T77)) → lessC_out_g(s(T77))

The set Q consists of the following terms:

lessE_in_gg(x0, x1)
U5_gg(x0, x1, x2)
lessD_in_gg(x0, x1)
U3_gg(x0, x1)
U4_gg(x0, x1, x2)
lessC_in_g(x0)
U2_g(x0, x1)

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

(28) DependencyGraphProof (EQUIVALENT transformation)

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

(29) TRUE