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

(0) Obligation:

Clauses:

goal(X) :- ','(s2l(X, Xs), list(Xs)).
list([]).
list(X) :- ','(no(empty(X)), ','(tail(X, T), list(T))).
s2l(0, []).
s2l(X, .(X1, Xs)) :- ','(no(zero(X)), ','(p(X, P), s2l(P, Xs))).
tail([], []).
tail(.(X2, Xs), Xs).
p(0, 0).
p(s(X), X).
empty([]).
zero(0).
no(X) :- ','(X, ','(!, failure(a))).
no(X3).
failure(b).

Queries:

goal(g).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: goal(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: goal(T1), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: ','(s2l(T3, X6), list(X6))\n\nT3 is ground\nX6 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: ','(s2l(T3, X6), list(X6)), SCOPE: 2, CLAUSE: 3 | ','(s2l(T3, X6), list(X6)), SCOPE: 2, CLAUSE: 4\n\nT3 is ground\nX6 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: ','(s2l(T3, X6), list(X6)), SCOPE: 2, CLAUSE: 3\n\nT3 is ground\nX6 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: ','(s2l(T3, X6), list(X6)), SCOPE: 2, CLAUSE: 4\n\nT3 is ground\nX6 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: list([])\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: list([]), SCOPE: 3, CLAUSE: 1 | list([]), SCOPE: 3, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: list([]), SCOPE: 3, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: list([]), SCOPE: 3, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(no(empty([])), ','(tail([], X11), list(X11)))\n\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(no(empty([])), ','(tail([], X11), list(X11))), SCOPE: 4, CLAUSE: 11 | ','(no(empty([])), ','(tail([], X11), list(X11))), SCOPE: 4, CLAUSE: 12\n\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(call(empty([])), ','(!_4, ','(failure(a), ','(tail([], X11), list(X11))))) | ','(no(empty([])), ','(tail([], X11), list(X11))), SCOPE: 4, CLAUSE: 12\n\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(empty([]), ','(!_4, ','(failure(a), ','(tail([], X11), list(X11))))) | ?_5 | ','(no(empty([])), ','(tail([], X11), list(X11))), SCOPE: 4, CLAUSE: 12\n\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(empty([]), ','(!_4, ','(failure(a), ','(tail([], X11), list(X11))))), SCOPE: 6, CLAUSE: 9 | ?_6 | ?_5 | ','(no(empty([])), ','(tail([], X11), list(X11))), SCOPE: 4, CLAUSE: 12\n\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(!_4, ','(failure(a), ','(tail([], X11), list(X11)))) | ?_6 | ?_5 | ','(no(empty([])), ','(tail([], X11), list(X11))), SCOPE: 4, CLAUSE: 12\n\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(failure(a), ','(tail([], X11), list(X11)))\n\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: ','(failure(a), ','(tail([], X11), list(X11))), SCOPE: 7, CLAUSE: 13\n\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(no(zero(T6)), ','(p(T6, X33), ','(s2l(X33, X35), list(.(X34, X35)))))\n\nT6 is ground\nX34 is free; \nX35 is free; \nX33 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(no(zero(T6)), ','(p(T6, X33), ','(s2l(X33, X35), list(.(X34, X35))))), SCOPE: 8, CLAUSE: 11 | ','(no(zero(T6)), ','(p(T6, X33), ','(s2l(X33, X35), list(.(X34, X35))))), SCOPE: 8, CLAUSE: 12\n\nT6 is ground\nX34 is free; \nX35 is free; \nX33 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(call(zero(T9)), ','(!_8, ','(failure(a), ','(p(T9, X33), ','(s2l(X33, X35), list(.(X34, X35))))))) | ','(no(zero(T9)), ','(p(T9, X33), ','(s2l(X33, X35), list(.(X34, X35))))), SCOPE: 8, CLAUSE: 12\n\nT9 is ground\nX34 is free; \nX35 is free; \nX33 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(zero(T9), ','(!_8, ','(failure(a), ','(p(T9, X33), ','(s2l(X33, X35), list(.(X34, X35))))))) | ?_9 | ','(no(zero(T9)), ','(p(T9, X33), ','(s2l(X33, X35), list(.(X34, X35))))), SCOPE: 8, CLAUSE: 12\n\nT9 is ground\nX34 is free; \nX35 is free; \nX33 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(zero(T9), ','(!_8, ','(failure(a), ','(p(T9, X33), ','(s2l(X33, X35), list(.(X34, X35))))))), SCOPE: 10, CLAUSE: 10 | ?_10 | ?_9 | ','(no(zero(T9)), ','(p(T9, X33), ','(s2l(X33, X35), list(.(X34, X35))))), SCOPE: 8, CLAUSE: 12\n\nT9 is ground\nX34 is free; \nX35 is free; \nX33 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(!_8, ','(failure(a), ','(p(0, X33), ','(s2l(X33, X35), list(.(X34, X35)))))) | ?_10 | ?_9 | ','(no(zero(0)), ','(p(0, X33), ','(s2l(X33, X35), list(.(X34, X35))))), SCOPE: 8, CLAUSE: 12\n\nX34 is free\nX35 is free; \nX33 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ?_10 | ?_9 | ','(no(zero(T9)), ','(p(T9, X33), ','(s2l(X33, X35), list(.(X34, X35))))), SCOPE: 8, CLAUSE: 12\n\nT9 is ground\nX34 is free; \nX35 is free; \nX33 is free; \nzero(T9) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(failure(a), ','(p(0, X33), ','(s2l(X33, X35), list(.(X34, X35)))))\n\nX34 is free\nX35 is free; \nX33 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(failure(a), ','(p(0, X33), ','(s2l(X33, X35), list(.(X34, X35))))), SCOPE: 11, CLAUSE: 13\n\nX34 is free\nX35 is free; \nX33 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ?_9 | ','(no(zero(T9)), ','(p(T9, X33), ','(s2l(X33, X35), list(.(X34, X35))))), SCOPE: 8, CLAUSE: 12\n\nT9 is ground\nX34 is free; \nX35 is free; \nX33 is free; \nzero(T9) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(no(zero(T9)), ','(p(T9, X33), ','(s2l(X33, X35), list(.(X34, X35))))), SCOPE: 8, CLAUSE: 12\n\nT9 is ground\nX34 is free; \nX35 is free; \nX33 is free; \nzero(T9) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(p(T12, X33), ','(s2l(X33, X35), list(.(X34, X35))))\n\nT12 is ground\nX34 is free; \nX35 is free; \nX33 is free; \nzero(T12) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(p(T12, X33), ','(s2l(X33, X35), list(.(X34, X35)))), SCOPE: 12, CLAUSE: 7 | ','(p(T12, X33), ','(s2l(X33, X35), list(.(X34, X35)))), SCOPE: 12, CLAUSE: 8\n\nT12 is ground\nX34 is free; \nX35 is free; \nX33 is free; \nzero(T12) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(p(T12, X33), ','(s2l(X33, X35), list(.(X34, X35)))), SCOPE: 12, CLAUSE: 8\n\nT12 is ground\nX34 is free; \nX35 is free; \nX33 is free; \nzero(T12) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(s2l(T15, X35), list(.(X34, X35)))\n\nT15 is ground\nX34 is free; \nX35 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: s2l(T15, X35)\n\nT15 is ground\nX35 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: list(.(X34, T16))\n\nX34 is free", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: s2l(T15, X35), SCOPE: 13, CLAUSE: 3 | s2l(T15, X35), SCOPE: 13, CLAUSE: 4\n\nT15 is ground\nX35 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: s2l(T15, X35), SCOPE: 13, CLAUSE: 3\n\nT15 is ground\nX35 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: s2l(T15, X35), SCOPE: 13, CLAUSE: 4\n\nT15 is ground\nX35 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(no(zero(T19)), ','(p(T19, X76), s2l(X76, X78)))\n\nT19 is ground\nX78 is free; \nX76 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(no(zero(T19)), ','(p(T19, X76), s2l(X76, X78))), SCOPE: 14, CLAUSE: 11 | ','(no(zero(T19)), ','(p(T19, X76), s2l(X76, X78))), SCOPE: 14, CLAUSE: 12\n\nT19 is ground\nX78 is free; \nX76 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(call(zero(T22)), ','(!_14, ','(failure(a), ','(p(T22, X76), s2l(X76, X78))))) | ','(no(zero(T22)), ','(p(T22, X76), s2l(X76, X78))), SCOPE: 14, CLAUSE: 12\n\nT22 is ground\nX78 is free; \nX76 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ','(zero(T22), ','(!_14, ','(failure(a), ','(p(T22, X76), s2l(X76, X78))))) | ?_15 | ','(no(zero(T22)), ','(p(T22, X76), s2l(X76, X78))), SCOPE: 14, CLAUSE: 12\n\nT22 is ground\nX78 is free; \nX76 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: ','(zero(T22), ','(!_14, ','(failure(a), ','(p(T22, X76), s2l(X76, X78))))), SCOPE: 16, CLAUSE: 10 | ?_16 | ?_15 | ','(no(zero(T22)), ','(p(T22, X76), s2l(X76, X78))), SCOPE: 14, CLAUSE: 12\n\nT22 is ground\nX78 is free; \nX76 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ','(!_14, ','(failure(a), ','(p(0, X76), s2l(X76, X78)))) | ?_16 | ?_15 | ','(no(zero(0)), ','(p(0, X76), s2l(X76, X78))), SCOPE: 14, CLAUSE: 12\n\nX78 is free\nX76 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ?_16 | ?_15 | ','(no(zero(T22)), ','(p(T22, X76), s2l(X76, X78))), SCOPE: 14, CLAUSE: 12\n\nT22 is ground\nX78 is free; \nX76 is free; \nzero(T22) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(failure(a), ','(p(0, X76), s2l(X76, X78)))\n\nX78 is free\nX76 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ','(failure(a), ','(p(0, X76), s2l(X76, X78))), SCOPE: 17, CLAUSE: 13\n\nX78 is free\nX76 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ?_15 | ','(no(zero(T22)), ','(p(T22, X76), s2l(X76, X78))), SCOPE: 14, CLAUSE: 12\n\nT22 is ground\nX78 is free; \nX76 is free; \nzero(T22) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(no(zero(T22)), ','(p(T22, X76), s2l(X76, X78))), SCOPE: 14, CLAUSE: 12\n\nT22 is ground\nX78 is free; \nX76 is free; \nzero(T22) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ','(p(T25, X76), s2l(X76, X78))\n\nT25 is ground\nX78 is free; \nX76 is free; \nzero(T25) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(p(T25, X76), s2l(X76, X78)), SCOPE: 18, CLAUSE: 7 | ','(p(T25, X76), s2l(X76, X78)), SCOPE: 18, CLAUSE: 8\n\nT25 is ground\nX78 is free; \nX76 is free; \nzero(T25) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ','(p(T25, X76), s2l(X76, X78)), SCOPE: 18, CLAUSE: 8\n\nT25 is ground\nX78 is free; \nX76 is free; \nzero(T25) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: s2l(T28, X78)\n\nT28 is ground\nX78 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: list(.(X34, T16)), SCOPE: 19, CLAUSE: 1 | list(.(X34, T16)), SCOPE: 19, CLAUSE: 2\n\nX34 is free", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: list(.(X34, T16)), SCOPE: 19, CLAUSE: 2\n\nX34 is free", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: ','(no(empty(.(X99, T34))), ','(tail(.(X99, T34), X98), list(X98)))\n\nX99 is free\nX98 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(no(empty(.(X99, T34))), ','(tail(.(X99, T34), X98), list(X98))), SCOPE: 20, CLAUSE: 11 | ','(no(empty(.(X99, T34))), ','(tail(.(X99, T34), X98), list(X98))), SCOPE: 20, CLAUSE: 12\n\nX99 is free\nX98 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: ','(call(empty(.(X105, T39))), ','(!_20, ','(failure(a), ','(tail(.(X105, T39), X98), list(X98))))) | ','(no(empty(.(X99, T34))), ','(tail(.(X99, T34), X98), list(X98))), SCOPE: 20, CLAUSE: 12\n\nX99 is free\nX98 is free; \nX105 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: ','(empty(.(X105, T39)), ','(!_20, ','(failure(a), ','(tail(.(X105, T39), X98), list(X98))))) | ?_21 | ','(no(empty(.(X99, T34))), ','(tail(.(X99, T34), X98), list(X98))), SCOPE: 20, CLAUSE: 12\n\nX99 is free\nX98 is free; \nX105 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ','(empty(.(X105, T39)), ','(!_20, ','(failure(a), ','(tail(.(X105, T39), X98), list(X98))))), SCOPE: 22, CLAUSE: 9 | ?_22 | ?_21 | ','(no(empty(.(X99, T34))), ','(tail(.(X99, T34), X98), list(X98))), SCOPE: 20, CLAUSE: 12\n\nX99 is free\nX98 is free; \nX105 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ?_22 | ?_21 | ','(no(empty(.(X99, T34))), ','(tail(.(X99, T34), X98), list(X98))), SCOPE: 20, CLAUSE: 12\n\nX99 is free\nX98 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: ?_21 | ','(no(empty(.(X99, T34))), ','(tail(.(X99, T34), X98), list(X98))), SCOPE: 20, CLAUSE: 12\n\nX99 is free\nX98 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: ','(no(empty(.(X99, T34))), ','(tail(.(X99, T34), X98), list(X98))), SCOPE: 20, CLAUSE: 12\n\nX99 is free\nX98 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ','(tail(.(X111, T44), X98), list(X98))\n\nX98 is free\nX111 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(tail(.(X111, T44), X98), list(X98)), SCOPE: 23, CLAUSE: 5 | ','(tail(.(X111, T44), X98), list(X98)), SCOPE: 23, CLAUSE: 6\n\nX98 is free\nX111 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ','(tail(.(X111, T44), X98), list(X98)), SCOPE: 23, CLAUSE: 6\n\nX98 is free\nX111 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: list(T49)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: list(T49), SCOPE: 24, CLAUSE: 1 | list(T49), SCOPE: 24, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: list(T49), SCOPE: 24, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: list(T49), SCOPE: 24, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: ','(no(empty(T54)), ','(tail(T54, X125), list(X125)))\n\nX125 is free", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(no(empty(T54)), ','(tail(T54, X125), list(X125))), SCOPE: 25, CLAUSE: 11 | ','(no(empty(T54)), ','(tail(T54, X125), list(X125))), SCOPE: 25, CLAUSE: 12\n\nX125 is free", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: ','(call(empty(T59)), ','(!_25, ','(failure(a), ','(tail(T59, X125), list(X125))))) | ','(no(empty(T54)), ','(tail(T54, X125), list(X125))), SCOPE: 25, CLAUSE: 12\n\nX125 is free", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ','(empty(T59), ','(!_25, ','(failure(a), ','(tail(T59, X125), list(X125))))) | ?_26 | ','(no(empty(T54)), ','(tail(T54, X125), list(X125))), SCOPE: 25, CLAUSE: 12\n\nX125 is free", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: ','(empty(T59), ','(!_25, ','(failure(a), ','(tail(T59, X125), list(X125))))), SCOPE: 27, CLAUSE: 9 | ?_27 | ?_26 | ','(no(empty(T54)), ','(tail(T54, X125), list(X125))), SCOPE: 25, CLAUSE: 12\n\nX125 is free", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(!_25, ','(failure(a), ','(tail([], X125), list(X125)))) | ?_27 | ?_26 | ','(no(empty(T54)), ','(tail(T54, X125), list(X125))), SCOPE: 25, CLAUSE: 12\n\nX125 is free", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: ?_27 | ?_26 | ','(no(empty(T54)), ','(tail(T54, X125), list(X125))), SCOPE: 25, CLAUSE: 12\n\nX125 is free", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(failure(a), ','(tail([], X125), list(X125)))\n\nX125 is free", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ','(failure(a), ','(tail([], X125), list(X125))), SCOPE: 28, CLAUSE: 13\n\nX125 is free", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ?_26 | ','(no(empty(T54)), ','(tail(T54, X125), list(X125))), SCOPE: 25, CLAUSE: 12\n\nX125 is free", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(no(empty(T54)), ','(tail(T54, X125), list(X125))), SCOPE: 25, CLAUSE: 12\n\nX125 is free", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(tail(T64, X125), list(X125))\n\nX125 is free", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(tail(T64, X125), list(X125)), SCOPE: 29, CLAUSE: 5 | ','(tail(T64, X125), list(X125)), SCOPE: 29, CLAUSE: 6\n\nX125 is free", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: ','(tail(T64, X125), list(X125)), SCOPE: 29, CLAUSE: 5\n\nX125 is free", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ','(tail(T64, X125), list(X125)), SCOPE: 29, CLAUSE: 6\n\nX125 is free", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: list([])\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: list(T71)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 105 [arrowhead = none ];
105 -> 2;

106 [label="ONLY EVAL with clause\ngoal(X5) :- ','(s2l(X5, X6), list(X6)).\nand substitution\nT1 -> T3\nX5 -> T3", fontsize=14, style = filled, fillcolor = white];
2 -> 106 [arrowhead = none ];
106 -> 3;

107 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 107 [arrowhead = none ];
107 -> 4;

108 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 108 [arrowhead = none ];
108 -> 5;

109 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 109 [arrowhead = none ];
109 -> 6;

110 [label="EVAL with clause\ns2l(0, []).\nand substitution\nT3 -> 0\nX6 -> []", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 110 [arrowhead = none ];
110 -> 7;

111 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 111 [arrowhead = none ];
111 -> 8;

112 [label="ONLY EVAL with clause\ns2l(X30, .(X31, X32)) :- ','(no(zero(X30)), ','(p(X30, X33), s2l(X33, X32))).\nand substitution\nT3 -> T6\nX30 -> T6\nX31 -> X34\nX32 -> X35\nX6 -> .(X34, X35)", fontsize=14, style = filled, fillcolor = white];
6 -> 112 [arrowhead = none ];
112 -> 23;

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

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

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

116 [label="ONLY EVAL with clause\nlist([]).\nand substitution", fontsize=14, style = filled, fillcolor = white];
10 -> 116 [arrowhead = none ];
116 -> 12;

117 [label="ONLY EVAL with clause\nlist(X10) :- ','(no(empty(X10)), ','(tail(X10, X11), list(X11))).\nand substitution\nX10 -> []", fontsize=14, style = filled, fillcolor = white];
11 -> 117 [arrowhead = none ];
117 -> 14;

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

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

120 [label="ONLY EVAL with clause\nno(X14) :- ','(call(X14), ','(!_4, failure(a))).\nand substitution\nX14 -> empty([])", fontsize=14, style = filled, fillcolor = white];
15 -> 120 [arrowhead = none ];
120 -> 16;

121 [label="CALL", fontsize=14, style = filled, fillcolor = white];
16 -> 121 [arrowhead = none ];
121 -> 17;

122 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
17 -> 122 [arrowhead = none ];
122 -> 18;

123 [label="ONLY EVAL with clause\nempty([]).\nand substitution", fontsize=14, style = filled, fillcolor = white];
18 -> 123 [arrowhead = none ];
123 -> 19;

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

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

126 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = white];
21 -> 126 [arrowhead = none ];
126 -> 22;

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

128 [label="ONLY EVAL with clause\nno(X42) :- ','(call(X42), ','(!_8, failure(a))).\nand substitution\nT6 -> T9\nX42 -> zero(T9)", fontsize=14, style = filled, fillcolor = white];
24 -> 128 [arrowhead = none ];
128 -> 25;

129 [label="CALL", fontsize=14, style = filled, fillcolor = white];
25 -> 129 [arrowhead = none ];
129 -> 26;

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

131 [label="EVAL with clause\nzero(0).\nand substitution\nT9 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
27 -> 131 [arrowhead = none ];
131 -> 28;

132 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
27 -> 132 [arrowhead = none ];
132 -> 29;

133 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
28 -> 133 [arrowhead = none ];
133 -> 30;

134 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
29 -> 134 [arrowhead = none ];
134 -> 33;

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

136 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = white];
31 -> 136 [arrowhead = none ];
136 -> 32;

137 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
33 -> 137 [arrowhead = none ];
137 -> 34;

138 [label="ONLY EVAL with clause\nno(X53).\nand substitution\nT9 -> T12\nX53 -> zero(T12)", fontsize=14, style = filled, fillcolor = white];
34 -> 138 [arrowhead = none ];
138 -> 35;

139 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
35 -> 139 [arrowhead = none ];
139 -> 36;

140 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T12), zero(0))", fontsize=14, style = filled, fillcolor = white];
36 -> 140 [arrowhead = none ];
140 -> 37;

141 [label="EVAL with clause\np(s(X60), X60).\nand substitution\nX60 -> T15\nT12 -> s(T15)\nX33 -> T15", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 141 [arrowhead = none ];
141 -> 38;

142 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 142 [arrowhead = none ];
142 -> 39;

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

144 [label="SPLIT 2\nreplacements:\nX35 -> T16", fontsize=14, style = filled, fillcolor = violet];
38 -> 144 [arrowhead = none ];
144 -> 41;

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

146 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
41 -> 146 [arrowhead = none ];
146 -> 65;

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

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

149 [label="EVAL with clause\ns2l(0, []).\nand substitution\nT15 -> 0\nX35 -> []", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 149 [arrowhead = none ];
149 -> 45;

150 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 150 [arrowhead = none ];
150 -> 46;

151 [label="ONLY EVAL with clause\ns2l(X73, .(X74, X75)) :- ','(no(zero(X73)), ','(p(X73, X76), s2l(X76, X75))).\nand substitution\nT15 -> T19\nX73 -> T19\nX74 -> X77\nX75 -> X78\nX35 -> .(X77, X78)", fontsize=14, style = filled, fillcolor = white];
44 -> 151 [arrowhead = none ];
151 -> 48;

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

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

154 [label="ONLY EVAL with clause\nno(X81) :- ','(call(X81), ','(!_14, failure(a))).\nand substitution\nT19 -> T22\nX81 -> zero(T22)", fontsize=14, style = filled, fillcolor = white];
49 -> 154 [arrowhead = none ];
154 -> 50;

155 [label="CALL", fontsize=14, style = filled, fillcolor = white];
50 -> 155 [arrowhead = none ];
155 -> 51;

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

157 [label="EVAL with clause\nzero(0).\nand substitution\nT22 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
52 -> 157 [arrowhead = none ];
157 -> 53;

158 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
52 -> 158 [arrowhead = none ];
158 -> 54;

159 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
53 -> 159 [arrowhead = none ];
159 -> 55;

160 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
54 -> 160 [arrowhead = none ];
160 -> 58;

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

162 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = white];
56 -> 162 [arrowhead = none ];
162 -> 57;

163 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
58 -> 163 [arrowhead = none ];
163 -> 59;

164 [label="ONLY EVAL with clause\nno(X84).\nand substitution\nT22 -> T25\nX84 -> zero(T25)", fontsize=14, style = filled, fillcolor = white];
59 -> 164 [arrowhead = none ];
164 -> 60;

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

166 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T25), zero(0))", fontsize=14, style = filled, fillcolor = white];
61 -> 166 [arrowhead = none ];
166 -> 62;

167 [label="EVAL with clause\np(s(X87), X87).\nand substitution\nX87 -> T28\nT25 -> s(T28)\nX76 -> T28", fontsize=14, style = filled, fillcolor = lightblue];
62 -> 167 [arrowhead = none ];
167 -> 63;

168 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
62 -> 168 [arrowhead = none ];
168 -> 64;

169 [label="INSTANCE with matching:\nT15 -> T28\nX35 -> X78", fontsize=14, style = filled, fillcolor = lightgrey];
63 -> 169 [arrowhead = none , style=dashed];
169 -> 40[style=dashed];

170 [label="BACKTRACK\nfor clause: list([])because of non-unification", fontsize=14, style = filled, fillcolor = white];
65 -> 170 [arrowhead = none ];
170 -> 66;

171 [label="ONLY EVAL with clause\nlist(X97) :- ','(no(empty(X97)), ','(tail(X97, X98), list(X98))).\nand substitution\nX34 -> X99\nT16 -> T34\nX97 -> .(X99, T34)\nT33 -> T34", fontsize=14, style = filled, fillcolor = white];
66 -> 171 [arrowhead = none ];
171 -> 67;

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

173 [label="ONLY EVAL with clause\nno(X104) :- ','(call(X104), ','(!_20, failure(a))).\nand substitution\nX99 -> X105\nT34 -> T39\nX104 -> empty(.(X105, T39))\nT38 -> T39", fontsize=14, style = filled, fillcolor = white];
68 -> 173 [arrowhead = none ];
173 -> 69;

174 [label="CALL", fontsize=14, style = filled, fillcolor = white];
69 -> 174 [arrowhead = none ];
174 -> 70;

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

176 [label="BACKTRACK\nfor clause: empty([])because of non-unification", fontsize=14, style = filled, fillcolor = white];
71 -> 176 [arrowhead = none ];
176 -> 72;

177 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
72 -> 177 [arrowhead = none ];
177 -> 73;

178 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
73 -> 178 [arrowhead = none ];
178 -> 74;

179 [label="ONLY EVAL with clause\nno(X110).\nand substitution\nX99 -> X111\nT34 -> T44\nX110 -> empty(.(X111, T44))\nT43 -> T44", fontsize=14, style = filled, fillcolor = white];
74 -> 179 [arrowhead = none ];
179 -> 75;

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

181 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = white];
76 -> 181 [arrowhead = none ];
181 -> 77;

182 [label="ONLY EVAL with clause\ntail(.(X118, X119), X119).\nand substitution\nX111 -> X120\nX118 -> X120\nT44 -> T49\nX119 -> T49\nX98 -> T49\nT48 -> T49", fontsize=14, style = filled, fillcolor = white];
77 -> 182 [arrowhead = none ];
182 -> 78;

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

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

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

186 [label="EVAL with clause\nlist([]).\nand substitution\nT49 -> []", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 186 [arrowhead = none ];
186 -> 82;

187 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 187 [arrowhead = none ];
187 -> 83;

188 [label="ONLY EVAL with clause\nlist(X124) :- ','(no(empty(X124)), ','(tail(X124, X125), list(X125))).\nand substitution\nT49 -> T54\nX124 -> T54\nT53 -> T54", fontsize=14, style = filled, fillcolor = white];
81 -> 188 [arrowhead = none ];
188 -> 85;

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

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

191 [label="ONLY EVAL with clause\nno(X128) :- ','(call(X128), ','(!_25, failure(a))).\nand substitution\nT54 -> T59\nX128 -> empty(T59)\nT58 -> T59", fontsize=14, style = filled, fillcolor = white];
86 -> 191 [arrowhead = none ];
191 -> 87;

192 [label="CALL", fontsize=14, style = filled, fillcolor = white];
87 -> 192 [arrowhead = none ];
192 -> 88;

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

194 [label="EVAL with clause\nempty([]).\nand substitution\nT59 -> []", fontsize=14, style = filled, fillcolor = lightblue];
89 -> 194 [arrowhead = none ];
194 -> 90;

195 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
89 -> 195 [arrowhead = none ];
195 -> 91;

196 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
90 -> 196 [arrowhead = none ];
196 -> 92;

197 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
91 -> 197 [arrowhead = none ];
197 -> 95;

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

199 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = white];
93 -> 199 [arrowhead = none ];
199 -> 94;

200 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
95 -> 200 [arrowhead = none ];
200 -> 96;

201 [label="ONLY EVAL with clause\nno(X131).\nand substitution\nT54 -> T64\nX131 -> empty(T64)\nT63 -> T64", fontsize=14, style = filled, fillcolor = white];
96 -> 201 [arrowhead = none ];
201 -> 97;

202 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
97 -> 202 [arrowhead = none ];
202 -> 98;

203 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
98 -> 203 [arrowhead = none ];
203 -> 99;

204 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
98 -> 204 [arrowhead = none ];
204 -> 100;

205 [label="EVAL with clause\ntail([], []).\nand substitution\nT64 -> []\nX125 -> []", fontsize=14, style = filled, fillcolor = lightblue];
99 -> 205 [arrowhead = none ];
205 -> 101;

206 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
99 -> 206 [arrowhead = none ];
206 -> 102;

207 [label="EVAL with clause\ntail(.(X136, X137), X137).\nand substitution\nX136 -> T69\nX137 -> T71\nT64 -> .(T69, T71)\nX125 -> T71\nT70 -> T71", fontsize=14, style = filled, fillcolor = lightblue];
100 -> 207 [arrowhead = none ];
207 -> 103;

208 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
100 -> 208 [arrowhead = none ];
208 -> 104;

209 [label="INSTANCE", fontsize=14, style = filled, fillcolor = lightgrey];
101 -> 209 [arrowhead = none , style=dashed];
209 -> 7[style=dashed];

210 [label="INSTANCE with matching:\nT49 -> T71", fontsize=14, style = filled, fillcolor = lightgrey];
103 -> 210 [arrowhead = none , style=dashed];
210 -> 78[style=dashed];

}

(2) Obligation:

Triples:

s2l40(s(T28), .(X77, X78)) :- s2l40(T28, X78).
list78([]) :- list7.
list78(.(T69, T71)) :- list78(T71).
goal1(0) :- list7.
goal1(s(T15)) :- s2l40(T15, X35).
goal1(s(T15)) :- ','(s2lc40(T15, T49), list78(T49)).

Clauses:

s2lc40(0, []).
s2lc40(s(T28), .(X77, X78)) :- s2lc40(T28, X78).
listc7.
listc78([]).
listc78([]) :- listc7.
listc78(.(T69, T71)) :- listc78(T71).

Afs:

goal1(x1)  =  goal1(x1)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [UNKNOWN].

(4) Obligation:

Triples:

s2l40(s(T28), .(X77, X78)) :- s2l40(T28, X78).
list78(.(T69, T71)) :- list78(T71).
goal1(s(T15)) :- s2l40(T15, X35).
goal1(s(T15)) :- ','(s2lc40(T15, T49), list78(T49)).

Clauses:

s2lc40(0, []).
s2lc40(s(T28), .(X77, X78)) :- s2lc40(T28, X78).
listc7.
listc78([]).
listc78([]) :- listc7.
listc78(.(T69, T71)) :- listc78(T71).

Afs:

goal1(x1)  =  goal1(x1)

(5) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
goal1_in: (b)
s2l40_in: (b,f)
s2lc40_in: (b,f)
list78_in: (b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

GOAL1_IN_G(s(T15)) → U3_G(T15, s2l40_in_ga(T15, X35))
GOAL1_IN_G(s(T15)) → S2L40_IN_GA(T15, X35)
S2L40_IN_GA(s(T28), .(X77, X78)) → U1_GA(T28, X77, X78, s2l40_in_ga(T28, X78))
S2L40_IN_GA(s(T28), .(X77, X78)) → S2L40_IN_GA(T28, X78)
GOAL1_IN_G(s(T15)) → U4_G(T15, s2lc40_in_ga(T15, T49))
U4_G(T15, s2lc40_out_ga(T15, T49)) → U5_G(T15, list78_in_g(T49))
U4_G(T15, s2lc40_out_ga(T15, T49)) → LIST78_IN_G(T49)
LIST78_IN_G(.(T69, T71)) → U2_G(T69, T71, list78_in_g(T71))
LIST78_IN_G(.(T69, T71)) → LIST78_IN_G(T71)

The TRS R consists of the following rules:

s2lc40_in_ga(0, []) → s2lc40_out_ga(0, [])
s2lc40_in_ga(s(T28), .(X77, X78)) → U7_ga(T28, X77, X78, s2lc40_in_ga(T28, X78))
U7_ga(T28, X77, X78, s2lc40_out_ga(T28, X78)) → s2lc40_out_ga(s(T28), .(X77, X78))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
s2l40_in_ga(x1, x2)  =  s2l40_in_ga(x1)
.(x1, x2)  =  .(x2)
s2lc40_in_ga(x1, x2)  =  s2lc40_in_ga(x1)
0  =  0
s2lc40_out_ga(x1, x2)  =  s2lc40_out_ga(x1, x2)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x4)
list78_in_g(x1)  =  list78_in_g(x1)
GOAL1_IN_G(x1)  =  GOAL1_IN_G(x1)
U3_G(x1, x2)  =  U3_G(x1, x2)
S2L40_IN_GA(x1, x2)  =  S2L40_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x1, x4)
U4_G(x1, x2)  =  U4_G(x1, x2)
U5_G(x1, x2)  =  U5_G(x1, x2)
LIST78_IN_G(x1)  =  LIST78_IN_G(x1)
U2_G(x1, x2, x3)  =  U2_G(x2, x3)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(6) Obligation:

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

GOAL1_IN_G(s(T15)) → U3_G(T15, s2l40_in_ga(T15, X35))
GOAL1_IN_G(s(T15)) → S2L40_IN_GA(T15, X35)
S2L40_IN_GA(s(T28), .(X77, X78)) → U1_GA(T28, X77, X78, s2l40_in_ga(T28, X78))
S2L40_IN_GA(s(T28), .(X77, X78)) → S2L40_IN_GA(T28, X78)
GOAL1_IN_G(s(T15)) → U4_G(T15, s2lc40_in_ga(T15, T49))
U4_G(T15, s2lc40_out_ga(T15, T49)) → U5_G(T15, list78_in_g(T49))
U4_G(T15, s2lc40_out_ga(T15, T49)) → LIST78_IN_G(T49)
LIST78_IN_G(.(T69, T71)) → U2_G(T69, T71, list78_in_g(T71))
LIST78_IN_G(.(T69, T71)) → LIST78_IN_G(T71)

The TRS R consists of the following rules:

s2lc40_in_ga(0, []) → s2lc40_out_ga(0, [])
s2lc40_in_ga(s(T28), .(X77, X78)) → U7_ga(T28, X77, X78, s2lc40_in_ga(T28, X78))
U7_ga(T28, X77, X78, s2lc40_out_ga(T28, X78)) → s2lc40_out_ga(s(T28), .(X77, X78))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
s2l40_in_ga(x1, x2)  =  s2l40_in_ga(x1)
.(x1, x2)  =  .(x2)
s2lc40_in_ga(x1, x2)  =  s2lc40_in_ga(x1)
0  =  0
s2lc40_out_ga(x1, x2)  =  s2lc40_out_ga(x1, x2)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x4)
list78_in_g(x1)  =  list78_in_g(x1)
GOAL1_IN_G(x1)  =  GOAL1_IN_G(x1)
U3_G(x1, x2)  =  U3_G(x1, x2)
S2L40_IN_GA(x1, x2)  =  S2L40_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x1, x4)
U4_G(x1, x2)  =  U4_G(x1, x2)
U5_G(x1, x2)  =  U5_G(x1, x2)
LIST78_IN_G(x1)  =  LIST78_IN_G(x1)
U2_G(x1, x2, x3)  =  U2_G(x2, x3)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 7 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

LIST78_IN_G(.(T69, T71)) → LIST78_IN_G(T71)

The TRS R consists of the following rules:

s2lc40_in_ga(0, []) → s2lc40_out_ga(0, [])
s2lc40_in_ga(s(T28), .(X77, X78)) → U7_ga(T28, X77, X78, s2lc40_in_ga(T28, X78))
U7_ga(T28, X77, X78, s2lc40_out_ga(T28, X78)) → s2lc40_out_ga(s(T28), .(X77, X78))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
s2lc40_in_ga(x1, x2)  =  s2lc40_in_ga(x1)
0  =  0
s2lc40_out_ga(x1, x2)  =  s2lc40_out_ga(x1, x2)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x4)
LIST78_IN_G(x1)  =  LIST78_IN_G(x1)

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

(10) UsableRulesProof (EQUIVALENT transformation)

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

(11) Obligation:

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

LIST78_IN_G(.(T69, T71)) → LIST78_IN_G(T71)

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

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

(12) PiDPToQDPProof (SOUND transformation)

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

(13) Obligation:

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

LIST78_IN_G(.(T71)) → LIST78_IN_G(T71)

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

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

• LIST78_IN_G(.(T71)) → LIST78_IN_G(T71)
  The graph contains the following edges 1 > 1

(15) YES

(16) Obligation:

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

S2L40_IN_GA(s(T28), .(X77, X78)) → S2L40_IN_GA(T28, X78)

The TRS R consists of the following rules:

s2lc40_in_ga(0, []) → s2lc40_out_ga(0, [])
s2lc40_in_ga(s(T28), .(X77, X78)) → U7_ga(T28, X77, X78, s2lc40_in_ga(T28, X78))
U7_ga(T28, X77, X78, s2lc40_out_ga(T28, X78)) → s2lc40_out_ga(s(T28), .(X77, X78))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
s2lc40_in_ga(x1, x2)  =  s2lc40_in_ga(x1)
0  =  0
s2lc40_out_ga(x1, x2)  =  s2lc40_out_ga(x1, x2)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x4)
S2L40_IN_GA(x1, x2)  =  S2L40_IN_GA(x1)

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

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

S2L40_IN_GA(s(T28), .(X77, X78)) → S2L40_IN_GA(T28, X78)

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

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

S2L40_IN_GA(s(T28)) → S2L40_IN_GA(T28)

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

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

• S2L40_IN_GA(s(T28)) → S2L40_IN_GA(T28)
  The graph contains the following edges 1 > 1

(22) YES