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

(0) Obligation:

Clauses:

q(X) :- p(X, 0).
p(0, X1).
p(s(X), Y) :- p(X, s(Y)).

Query: q(g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: q(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: q(T1), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: p(T3, 0)\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: p(T3, 0), SCOPE: 2, CLAUSE: 1 | p(T3, 0), SCOPE: 2, CLAUSE: 2\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: p(T3, 0), SCOPE: 2, CLAUSE: 1\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: p(T3, 0), SCOPE: 2, CLAUSE: 2\n\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: p(T6, s(0))\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: p(T6, s(0)), SCOPE: 3, CLAUSE: 1 | p(T6, s(0)), SCOPE: 3, CLAUSE: 2\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: p(T6, s(0)), SCOPE: 3, CLAUSE: 1\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: p(T6, s(0)), SCOPE: 3, CLAUSE: 2\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: p(T9, s(s(0)))\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: p(T9, s(s(0))), SCOPE: 4, CLAUSE: 1 | p(T9, s(s(0))), SCOPE: 4, CLAUSE: 2\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: p(T9, s(s(0))), SCOPE: 4, CLAUSE: 1\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: p(T9, s(s(0))), SCOPE: 4, CLAUSE: 2\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: p(T12, s(s(s(0))))\n\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: p(T12, s(s(s(0)))), SCOPE: 5, CLAUSE: 1 | p(T12, s(s(s(0)))), SCOPE: 5, CLAUSE: 2\n\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: p(T12, s(s(s(0)))), SCOPE: 5, CLAUSE: 1\n\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: p(T12, s(s(s(0)))), SCOPE: 5, CLAUSE: 2\n\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: p(T15, s(s(s(s(0)))))\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: p(T15, s(s(s(s(0))))), SCOPE: 6, CLAUSE: 1 | p(T15, s(s(s(s(0))))), SCOPE: 6, CLAUSE: 2\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: p(T15, s(s(s(s(0))))), SCOPE: 6, CLAUSE: 1\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: p(T15, s(s(s(s(0))))), SCOPE: 6, CLAUSE: 2\n\nT15 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: p(T18, s(s(s(s(s(0))))))\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: p(T18, s(s(s(s(s(0)))))), SCOPE: 7, CLAUSE: 1 | p(T18, s(s(s(s(s(0)))))), SCOPE: 7, CLAUSE: 2\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: p(T18, s(s(s(s(s(0)))))), SCOPE: 7, CLAUSE: 1\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: p(T18, s(s(s(s(s(0)))))), SCOPE: 7, CLAUSE: 2\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: p(T21, s(s(s(s(s(s(0)))))))\n\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: p(T21, s(s(s(s(s(s(0))))))), SCOPE: 8, CLAUSE: 1 | p(T21, s(s(s(s(s(s(0))))))), SCOPE: 8, CLAUSE: 2\n\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: p(T21, s(s(s(s(s(s(0))))))), SCOPE: 8, CLAUSE: 1\n\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
154 [label="154: p(T21, s(s(s(s(s(s(0))))))), SCOPE: 8, CLAUSE: 2\n\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
159 [label="159: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: p(T24, s(s(s(s(s(s(s(0))))))))\n\nT24 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: p(T24, s(s(s(s(s(s(s(0)))))))), SCOPE: 9, CLAUSE: 1 | p(T24, s(s(s(s(s(s(s(0)))))))), SCOPE: 9, CLAUSE: 2\n\nT24 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: p(T24, s(s(s(s(s(s(s(0)))))))), SCOPE: 9, CLAUSE: 1\n\nT24 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: p(T24, s(s(s(s(s(s(s(0)))))))), SCOPE: 9, CLAUSE: 2\n\nT24 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="182: p(T27, s(s(s(s(s(s(s(s(0)))))))))\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="B: p(T27, s(T28))\n\nT27 is ground\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: p(T27, s(T28)), SCOPE: 10, CLAUSE: 1 | p(T27, s(T28)), SCOPE: 10, CLAUSE: 2\n\nT27 is ground\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: p(T27, s(T28)), SCOPE: 10, CLAUSE: 1\n\nT27 is ground\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: p(T27, s(T28)), SCOPE: 10, CLAUSE: 2\n\nT27 is ground\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: p(T40, s(s(T41)))\n\nT40 is ground\nT41 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
220 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 220 [arrowhead = none ];
220 -> 5;

221 [label="ONLY EVAL with clause\nq(X3) :- p(X3, 0).\nand substitutionT1 -> T3,\nX3 -> T3", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 221 [arrowhead = none ];
221 -> 10;

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

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

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

225 [label="EVAL with clause\np(0, X8).\nand substitutionT3 -> 0,\nX8 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
22 -> 225 [arrowhead = none ];
225 -> 24;

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

227 [label="EVAL with clause\np(s(X13), X14) :- p(X13, s(X14)).\nand substitutionX13 -> T6,\nT3 -> s(T6),\nX14 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 227 [arrowhead = none ];
227 -> 27;

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

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

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

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

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

233 [label="EVAL with clause\np(0, X21).\nand substitutionT6 -> 0,\nX21 -> s(0)", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 233 [arrowhead = none ];
233 -> 33;

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

235 [label="EVAL with clause\np(s(X26), X27) :- p(X26, s(X27)).\nand substitutionX26 -> T9,\nT6 -> s(T9),\nX27 -> s(0)", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 235 [arrowhead = none ];
235 -> 39;

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

237 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
33 -> 237 [arrowhead = none ];
237 -> 35;

238 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
39 -> 238 [arrowhead = none ];
238 -> 43;

239 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
43 -> 239 [arrowhead = none ];
239 -> 67;

240 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
43 -> 240 [arrowhead = none ];
240 -> 68;

241 [label="EVAL with clause\np(0, X34).\nand substitutionT9 -> 0,\nX34 -> s(s(0))", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 241 [arrowhead = none ];
241 -> 69;

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

243 [label="EVAL with clause\np(s(X39), X40) :- p(X39, s(X40)).\nand substitutionX39 -> T12,\nT9 -> s(T12),\nX40 -> s(s(0))", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 243 [arrowhead = none ];
243 -> 72;

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

245 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
69 -> 245 [arrowhead = none ];
245 -> 71;

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

247 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
75 -> 247 [arrowhead = none ];
247 -> 78;

248 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
75 -> 248 [arrowhead = none ];
248 -> 79;

249 [label="EVAL with clause\np(0, X47).\nand substitutionT12 -> 0,\nX47 -> s(s(s(0)))", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 249 [arrowhead = none ];
249 -> 80;

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

251 [label="EVAL with clause\np(s(X52), X53) :- p(X52, s(X53)).\nand substitutionX52 -> T15,\nT12 -> s(T15),\nX53 -> s(s(s(0)))", fontsize=14, style = filled, fillcolor = lightblue];
79 -> 251 [arrowhead = none ];
251 -> 86;

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

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

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

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

256 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
91 -> 256 [arrowhead = none ];
256 -> 93;

257 [label="EVAL with clause\np(0, X60).\nand substitutionT15 -> 0,\nX60 -> s(s(s(s(0))))", fontsize=14, style = filled, fillcolor = lightblue];
92 -> 257 [arrowhead = none ];
257 -> 99;

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

259 [label="EVAL with clause\np(s(X65), X66) :- p(X65, s(X66)).\nand substitutionX65 -> T18,\nT15 -> s(T18),\nX66 -> s(s(s(s(0))))", fontsize=14, style = filled, fillcolor = lightblue];
93 -> 259 [arrowhead = none ];
259 -> 111;

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

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

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

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

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

265 [label="EVAL with clause\np(0, X73).\nand substitutionT18 -> 0,\nX73 -> s(s(s(s(s(0)))))", fontsize=14, style = filled, fillcolor = lightblue];
130 -> 265 [arrowhead = none ];
265 -> 137;

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

267 [label="EVAL with clause\np(s(X78), X79) :- p(X78, s(X79)).\nand substitutionX78 -> T21,\nT18 -> s(T21),\nX79 -> s(s(s(s(s(0)))))", fontsize=14, style = filled, fillcolor = lightblue];
131 -> 267 [arrowhead = none ];
267 -> 144;

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

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

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

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

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

273 [label="EVAL with clause\np(0, X86).\nand substitutionT21 -> 0,\nX86 -> s(s(s(s(s(s(0))))))", fontsize=14, style = filled, fillcolor = lightblue];
153 -> 273 [arrowhead = none ];
273 -> 159;

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

275 [label="EVAL with clause\np(s(X91), X92) :- p(X91, s(X92)).\nand substitutionX91 -> T24,\nT21 -> s(T24),\nX92 -> s(s(s(s(s(s(0))))))", fontsize=14, style = filled, fillcolor = lightblue];
154 -> 275 [arrowhead = none ];
275 -> 165;

276 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
154 -> 276 [arrowhead = none ];
276 -> 166;

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

278 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
165 -> 278 [arrowhead = none ];
278 -> 168;

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

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

281 [label="EVAL with clause\np(0, X99).\nand substitutionT24 -> 0,\nX99 -> s(s(s(s(s(s(s(0)))))))", fontsize=14, style = filled, fillcolor = lightblue];
171 -> 281 [arrowhead = none ];
281 -> 176;

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

283 [label="EVAL with clause\np(s(X104), X105) :- p(X104, s(X105)).\nand substitutionX104 -> T27,\nT24 -> s(T27),\nX105 -> s(s(s(s(s(s(s(0)))))))", fontsize=14, style = filled, fillcolor = lightblue];
172 -> 283 [arrowhead = none ];
283 -> 182;

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

285 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
176 -> 285 [arrowhead = none ];
285 -> 178;

286 [label="GENERALIZATION\nT28 <-- s(s(s(s(s(s(s(0)))))))\n\nNew Knowledge:\nT28 is ground", fontsize=14, style = filled, fillcolor = violet];
182 -> 286 [arrowhead = none ];
286 -> 190;

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

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

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

290 [label="EVAL with clause\np(0, X114).\nand substitutionT27 -> 0,\nT28 -> T35,\nX114 -> s(T35)", fontsize=14, style = filled, fillcolor = lightblue];
198 -> 290 [arrowhead = none ];
290 -> 202;

291 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
198 -> 291 [arrowhead = none ];
291 -> 204;

292 [label="EVAL with clause\np(s(X119), X120) :- p(X119, s(X120)).\nand substitutionX119 -> T40,\nT27 -> s(T40),\nT28 -> T41,\nX120 -> s(T41)", fontsize=14, style = filled, fillcolor = lightblue];
200 -> 292 [arrowhead = none ];
292 -> 218;

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

294 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
202 -> 294 [arrowhead = none ];
294 -> 217;

295 [label="INSTANCE with matching:\nT27 -> T40\nT28 -> s(T41)", fontsize=14, style = filled, fillcolor = lightgrey];
218 -> 295 [arrowhead = none , style=dashed];
295 -> 190[style=dashed];

}

(2) Obligation:

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

qA_in_g(0) → qA_out_g(0)
qA_in_g(s(0)) → qA_out_g(s(0))
qA_in_g(s(s(0))) → qA_out_g(s(s(0)))
qA_in_g(s(s(s(0)))) → qA_out_g(s(s(s(0))))
qA_in_g(s(s(s(s(0))))) → qA_out_g(s(s(s(s(0)))))
qA_in_g(s(s(s(s(s(0)))))) → qA_out_g(s(s(s(s(s(0))))))
qA_in_g(s(s(s(s(s(s(0))))))) → qA_out_g(s(s(s(s(s(s(0)))))))
qA_in_g(s(s(s(s(s(s(s(0)))))))) → qA_out_g(s(s(s(s(s(s(s(0))))))))
qA_in_g(s(s(s(s(s(s(s(s(T27))))))))) → U1_g(T27, pB_in_gg(T27, s(s(s(s(s(s(s(0)))))))))
pB_in_gg(0, T35) → pB_out_gg(0, T35)
pB_in_gg(s(T40), T41) → U2_gg(T40, T41, pB_in_gg(T40, s(T41)))
U2_gg(T40, T41, pB_out_gg(T40, s(T41))) → pB_out_gg(s(T40), T41)
U1_g(T27, pB_out_gg(T27, s(s(s(s(s(s(s(0))))))))) → qA_out_g(s(s(s(s(s(s(s(s(T27)))))))))

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:

QA_IN_G(s(s(s(s(s(s(s(s(T27))))))))) → U1_G(T27, pB_in_gg(T27, s(s(s(s(s(s(s(0)))))))))
QA_IN_G(s(s(s(s(s(s(s(s(T27))))))))) → PB_IN_GG(T27, s(s(s(s(s(s(s(0))))))))
PB_IN_GG(s(T40), T41) → U2_GG(T40, T41, pB_in_gg(T40, s(T41)))
PB_IN_GG(s(T40), T41) → PB_IN_GG(T40, s(T41))

The TRS R consists of the following rules:

qA_in_g(0) → qA_out_g(0)
qA_in_g(s(0)) → qA_out_g(s(0))
qA_in_g(s(s(0))) → qA_out_g(s(s(0)))
qA_in_g(s(s(s(0)))) → qA_out_g(s(s(s(0))))
qA_in_g(s(s(s(s(0))))) → qA_out_g(s(s(s(s(0)))))
qA_in_g(s(s(s(s(s(0)))))) → qA_out_g(s(s(s(s(s(0))))))
qA_in_g(s(s(s(s(s(s(0))))))) → qA_out_g(s(s(s(s(s(s(0)))))))
qA_in_g(s(s(s(s(s(s(s(0)))))))) → qA_out_g(s(s(s(s(s(s(s(0))))))))
qA_in_g(s(s(s(s(s(s(s(s(T27))))))))) → U1_g(T27, pB_in_gg(T27, s(s(s(s(s(s(s(0)))))))))
pB_in_gg(0, T35) → pB_out_gg(0, T35)
pB_in_gg(s(T40), T41) → U2_gg(T40, T41, pB_in_gg(T40, s(T41)))
U2_gg(T40, T41, pB_out_gg(T40, s(T41))) → pB_out_gg(s(T40), T41)
U1_g(T27, pB_out_gg(T27, s(s(s(s(s(s(s(0))))))))) → qA_out_g(s(s(s(s(s(s(s(s(T27)))))))))

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:

QA_IN_G(s(s(s(s(s(s(s(s(T27))))))))) → U1_G(T27, pB_in_gg(T27, s(s(s(s(s(s(s(0)))))))))
QA_IN_G(s(s(s(s(s(s(s(s(T27))))))))) → PB_IN_GG(T27, s(s(s(s(s(s(s(0))))))))
PB_IN_GG(s(T40), T41) → U2_GG(T40, T41, pB_in_gg(T40, s(T41)))
PB_IN_GG(s(T40), T41) → PB_IN_GG(T40, s(T41))

The TRS R consists of the following rules:

qA_in_g(0) → qA_out_g(0)
qA_in_g(s(0)) → qA_out_g(s(0))
qA_in_g(s(s(0))) → qA_out_g(s(s(0)))
qA_in_g(s(s(s(0)))) → qA_out_g(s(s(s(0))))
qA_in_g(s(s(s(s(0))))) → qA_out_g(s(s(s(s(0)))))
qA_in_g(s(s(s(s(s(0)))))) → qA_out_g(s(s(s(s(s(0))))))
qA_in_g(s(s(s(s(s(s(0))))))) → qA_out_g(s(s(s(s(s(s(0)))))))
qA_in_g(s(s(s(s(s(s(s(0)))))))) → qA_out_g(s(s(s(s(s(s(s(0))))))))
qA_in_g(s(s(s(s(s(s(s(s(T27))))))))) → U1_g(T27, pB_in_gg(T27, s(s(s(s(s(s(s(0)))))))))
pB_in_gg(0, T35) → pB_out_gg(0, T35)
pB_in_gg(s(T40), T41) → U2_gg(T40, T41, pB_in_gg(T40, s(T41)))
U2_gg(T40, T41, pB_out_gg(T40, s(T41))) → pB_out_gg(s(T40), T41)
U1_g(T27, pB_out_gg(T27, s(s(s(s(s(s(s(0))))))))) → qA_out_g(s(s(s(s(s(s(s(s(T27)))))))))

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 3 less nodes.

(6) Obligation:

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

PB_IN_GG(s(T40), T41) → PB_IN_GG(T40, s(T41))

The TRS R consists of the following rules:

qA_in_g(0) → qA_out_g(0)
qA_in_g(s(0)) → qA_out_g(s(0))
qA_in_g(s(s(0))) → qA_out_g(s(s(0)))
qA_in_g(s(s(s(0)))) → qA_out_g(s(s(s(0))))
qA_in_g(s(s(s(s(0))))) → qA_out_g(s(s(s(s(0)))))
qA_in_g(s(s(s(s(s(0)))))) → qA_out_g(s(s(s(s(s(0))))))
qA_in_g(s(s(s(s(s(s(0))))))) → qA_out_g(s(s(s(s(s(s(0)))))))
qA_in_g(s(s(s(s(s(s(s(0)))))))) → qA_out_g(s(s(s(s(s(s(s(0))))))))
qA_in_g(s(s(s(s(s(s(s(s(T27))))))))) → U1_g(T27, pB_in_gg(T27, s(s(s(s(s(s(s(0)))))))))
pB_in_gg(0, T35) → pB_out_gg(0, T35)
pB_in_gg(s(T40), T41) → U2_gg(T40, T41, pB_in_gg(T40, s(T41)))
U2_gg(T40, T41, pB_out_gg(T40, s(T41))) → pB_out_gg(s(T40), T41)
U1_g(T27, pB_out_gg(T27, s(s(s(s(s(s(s(0))))))))) → qA_out_g(s(s(s(s(s(s(s(s(T27)))))))))

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

(7) UsableRulesProof (EQUIVALENT transformation)

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

(8) Obligation:

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

PB_IN_GG(s(T40), T41) → PB_IN_GG(T40, s(T41))

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

(9) PiDPToQDPProof (EQUIVALENT transformation)

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

(10) Obligation:

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

PB_IN_GG(s(T40), T41) → PB_IN_GG(T40, s(T41))

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

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

• PB_IN_GG(s(T40), T41) → PB_IN_GG(T40, s(T41))
  The graph contains the following edges 1 > 1

(12) YES