Left Termination of the query pattern
goal(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).

Query: goal(g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="A: goal(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: goal(T1), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(s2l(T3, X6), list(X6))\n\nT3 is ground\nX6 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(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];
14 [label="14: ','(s2l(T3, X6), list(X6)), SCOPE: 2, CLAUSE: 3\n\nT3 is ground\nX6 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(s2l(T3, X6), list(X6)), SCOPE: 2, CLAUSE: 4\n\nT3 is ground\nX6 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="B: list([])\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: list([]), SCOPE: 3, CLAUSE: 1 | list([]), SCOPE: 3, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: list([]), SCOPE: 3, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: list([]), SCOPE: 3, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(no(empty([])), ','(tail([], X11), list(X11)))\n\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(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];
44 [label="44: ','(','(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];
45 [label="45: ','(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];
47 [label="47: ','(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];
52 [label="52: ','(','(!_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];
63 [label="63: ','(failure(a), ','(tail([], X11), list(X11)))\n\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ','(failure(a), ','(tail([], X11), list(X11))), SCOPE: 7, CLAUSE: 13\n\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(','(no(zero(T6)), ','(p(T6, X29), s2l(X29, X31))), list(.(X30, X31)))\n\nT6 is ground\nX30 is free\nX31 is free\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: ','(','(no(zero(T6)), ','(p(T6, X29), s2l(X29, X31))), list(.(X30, X31))), SCOPE: 8, CLAUSE: 11 | ','(','(no(zero(T6)), ','(p(T6, X29), s2l(X29, X31))), list(.(X30, X31))), SCOPE: 8, CLAUSE: 12\n\nT6 is ground\nX30 is free\nX31 is free\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(','(call(zero(T9)), ','(!_8, failure(a))), ','(','(p(T9, X29), s2l(X29, X31)), list(.(X30, X31)))) | ','(','(no(zero(T9)), ','(p(T9, X29), s2l(X29, X31))), list(.(X30, X31))), SCOPE: 8, CLAUSE: 12\n\nT9 is ground\nX30 is free\nX31 is free\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ','(zero(T9), ','(','(!_8, failure(a)), ','(','(p(T9, X29), s2l(X29, X31)), list(.(X30, X31))))) | ?_9 | ','(','(no(zero(T9)), ','(p(T9, X29), s2l(X29, X31))), list(.(X30, X31))), SCOPE: 8, CLAUSE: 12\n\nT9 is ground\nX30 is free\nX31 is free\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: ','(zero(T9), ','(','(!_8, failure(a)), ','(','(p(T9, X29), s2l(X29, X31)), list(.(X30, X31))))), SCOPE: 10, CLAUSE: 10 | ?_10 | ?_9 | ','(','(no(zero(T9)), ','(p(T9, X29), s2l(X29, X31))), list(.(X30, X31))), SCOPE: 8, CLAUSE: 12\n\nT9 is ground\nX30 is free\nX31 is free\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(','(!_8, failure(a)), ','(','(p(0, X29), s2l(X29, X31)), list(.(X30, X31)))) | ?_10 | ?_9 | ','(','(no(zero(0)), ','(p(0, X29), s2l(X29, X31))), list(.(X30, X31))), SCOPE: 8, CLAUSE: 12\n\nX30 is free\nX31 is free\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: ?_10 | ?_9 | ','(','(no(zero(T9)), ','(p(T9, X29), s2l(X29, X31))), list(.(X30, X31))), SCOPE: 8, CLAUSE: 12\n\nT9 is ground\nX30 is free\nX31 is free\nX29 is free\nzero(T9) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(failure(a), ','(','(p(0, X29), s2l(X29, X31)), list(.(X30, X31))))\n\nX30 is free\nX31 is free\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: ','(failure(a), ','(','(p(0, X29), s2l(X29, X31)), list(.(X30, X31)))), SCOPE: 11, CLAUSE: 13\n\nX30 is free\nX31 is free\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: ?_9 | ','(','(no(zero(T9)), ','(p(T9, X29), s2l(X29, X31))), list(.(X30, X31))), SCOPE: 8, CLAUSE: 12\n\nT9 is ground\nX30 is free\nX31 is free\nX29 is free\nzero(T9) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: ','(','(no(zero(T9)), ','(p(T9, X29), s2l(X29, X31))), list(.(X30, X31))), SCOPE: 8, CLAUSE: 12\n\nT9 is ground\nX30 is free\nX31 is free\nX29 is free\nzero(T9) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: ','(','(p(T12, X29), s2l(X29, X31)), list(.(X30, X31)))\n\nT12 is ground\nX30 is free\nX31 is free\nX29 is free\nzero(T12) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: ','(','(p(T12, X29), s2l(X29, X31)), list(.(X30, X31))), SCOPE: 12, CLAUSE: 7 | ','(','(p(T12, X29), s2l(X29, X31)), list(.(X30, X31))), SCOPE: 12, CLAUSE: 8\n\nT12 is ground\nX30 is free\nX31 is free\nX29 is free\nzero(T12) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: ','(','(p(T12, X29), s2l(X29, X31)), list(.(X30, X31))), SCOPE: 12, CLAUSE: 8\n\nT12 is ground\nX30 is free\nX31 is free\nX29 is free\nzero(T12) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="C: ','(s2l(T15, X31), list(.(X30, X31)))\n\nT15 is ground\nX30 is free\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="D: s2l(T15, X31)\n\nT15 is ground\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="F: list(.(X30, T16))\n\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: s2l(T15, X31), SCOPE: 13, CLAUSE: 3 | s2l(T15, X31), SCOPE: 13, CLAUSE: 4\n\nT15 is ground\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: s2l(T15, X31), SCOPE: 13, CLAUSE: 3\n\nT15 is ground\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: s2l(T15, X31), SCOPE: 13, CLAUSE: 4\n\nT15 is ground\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: ','(no(zero(T19)), ','(p(T19, X55), s2l(X55, X57)))\n\nT19 is ground\nX57 is free\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
167 [label="167: ','(no(zero(T19)), ','(p(T19, X55), s2l(X55, X57))), SCOPE: 14, CLAUSE: 11 | ','(no(zero(T19)), ','(p(T19, X55), s2l(X55, X57))), SCOPE: 14, CLAUSE: 12\n\nT19 is ground\nX57 is free\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: ','(','(call(zero(T22)), ','(!_14, failure(a))), ','(p(T22, X55), s2l(X55, X57))) | ','(no(zero(T22)), ','(p(T22, X55), s2l(X55, X57))), SCOPE: 14, CLAUSE: 12\n\nT22 is ground\nX57 is free\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: ','(zero(T22), ','(','(!_14, failure(a)), ','(p(T22, X55), s2l(X55, X57)))) | ?_15 | ','(no(zero(T22)), ','(p(T22, X55), s2l(X55, X57))), SCOPE: 14, CLAUSE: 12\n\nT22 is ground\nX57 is free\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: ','(zero(T22), ','(','(!_14, failure(a)), ','(p(T22, X55), s2l(X55, X57)))), SCOPE: 16, CLAUSE: 10 | ?_16 | ?_15 | ','(no(zero(T22)), ','(p(T22, X55), s2l(X55, X57))), SCOPE: 14, CLAUSE: 12\n\nT22 is ground\nX57 is free\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: ','(','(!_14, failure(a)), ','(p(0, X55), s2l(X55, X57))) | ?_16 | ?_15 | ','(no(zero(0)), ','(p(0, X55), s2l(X55, X57))), SCOPE: 14, CLAUSE: 12\n\nX57 is free\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: ?_16 | ?_15 | ','(no(zero(T22)), ','(p(T22, X55), s2l(X55, X57))), SCOPE: 14, CLAUSE: 12\n\nT22 is ground\nX57 is free\nX55 is free\nzero(T22) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
183 [label="183: ','(failure(a), ','(p(0, X55), s2l(X55, X57)))\n\nX57 is free\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
186 [label="186: ','(failure(a), ','(p(0, X55), s2l(X55, X57))), SCOPE: 17, CLAUSE: 13\n\nX57 is free\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
187 [label="187: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: ?_15 | ','(no(zero(T22)), ','(p(T22, X55), s2l(X55, X57))), SCOPE: 14, CLAUSE: 12\n\nT22 is ground\nX57 is free\nX55 is free\nzero(T22) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="189: ','(no(zero(T22)), ','(p(T22, X55), s2l(X55, X57))), SCOPE: 14, CLAUSE: 12\n\nT22 is ground\nX57 is free\nX55 is free\nzero(T22) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: ','(p(T25, X55), s2l(X55, X57))\n\nT25 is ground\nX57 is free\nX55 is free\nzero(T25) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: ','(p(T25, X55), s2l(X55, X57)), SCOPE: 18, CLAUSE: 7 | ','(p(T25, X55), s2l(X55, X57)), SCOPE: 18, CLAUSE: 8\n\nT25 is ground\nX57 is free\nX55 is free\nzero(T25) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: ','(p(T25, X55), s2l(X55, X57)), SCOPE: 18, CLAUSE: 8\n\nT25 is ground\nX57 is free\nX55 is free\nzero(T25) !=? zero(0)", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="197: s2l(T28, X57)\n\nT28 is ground\nX57 is free", fontsize=16, style=filled, fillcolor=lightyellow];
198 [label="198: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: list(.(X30, T16)), SCOPE: 19, CLAUSE: 1 | list(.(X30, T16)), SCOPE: 19, CLAUSE: 2\n\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: list(.(X30, T16)), SCOPE: 19, CLAUSE: 2\n\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
209 [label="209: ','(no(empty(.(X74, T33))), ','(tail(.(X74, T33), X73), list(X73)))\n\nX74 is free\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
210 [label="210: ','(no(empty(.(X74, T33))), ','(tail(.(X74, T33), X73), list(X73))), SCOPE: 20, CLAUSE: 11 | ','(no(empty(.(X74, T33))), ','(tail(.(X74, T33), X73), list(X73))), SCOPE: 20, CLAUSE: 12\n\nX74 is free\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: ','(','(call(empty(.(X80, T38))), ','(!_20, failure(a))), ','(tail(.(X80, T38), X73), list(X73))) | ','(no(empty(.(X74, T33))), ','(tail(.(X74, T33), X73), list(X73))), SCOPE: 20, CLAUSE: 12\n\nX74 is free\nX73 is free\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: ','(empty(.(X80, T38)), ','(','(!_20, failure(a)), ','(tail(.(X80, T38), X73), list(X73)))) | ?_21 | ','(no(empty(.(X74, T33))), ','(tail(.(X74, T33), X73), list(X73))), SCOPE: 20, CLAUSE: 12\n\nX74 is free\nX73 is free\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="216: ','(empty(.(X80, T38)), ','(','(!_20, failure(a)), ','(tail(.(X80, T38), X73), list(X73)))), SCOPE: 22, CLAUSE: 9 | ?_22 | ?_21 | ','(no(empty(.(X74, T33))), ','(tail(.(X74, T33), X73), list(X73))), SCOPE: 20, CLAUSE: 12\n\nX74 is free\nX73 is free\nX80 is free", fontsize=16, style=filled, fillcolor=lightyellow];
217 [label="217: ?_22 | ?_21 | ','(no(empty(.(X74, T33))), ','(tail(.(X74, T33), X73), list(X73))), SCOPE: 20, CLAUSE: 12\n\nX74 is free\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
218 [label="218: ?_21 | ','(no(empty(.(X74, T33))), ','(tail(.(X74, T33), X73), list(X73))), SCOPE: 20, CLAUSE: 12\n\nX74 is free\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
219 [label="219: ','(no(empty(.(X74, T33))), ','(tail(.(X74, T33), X73), list(X73))), SCOPE: 20, CLAUSE: 12\n\nX74 is free\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
221 [label="221: ','(tail(.(X86, T43), X73), list(X73))\n\nX73 is free\nX86 is free", fontsize=16, style=filled, fillcolor=lightyellow];
222 [label="222: ','(tail(.(X86, T43), X73), list(X73)), SCOPE: 23, CLAUSE: 5 | ','(tail(.(X86, T43), X73), list(X73)), SCOPE: 23, CLAUSE: 6\n\nX73 is free\nX86 is free", fontsize=16, style=filled, fillcolor=lightyellow];
223 [label="223: ','(tail(.(X86, T43), X73), list(X73)), SCOPE: 23, CLAUSE: 6\n\nX73 is free\nX86 is free", fontsize=16, style=filled, fillcolor=lightyellow];
231 [label="E: list(T48)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
233 [label="233: list(T48), SCOPE: 24, CLAUSE: 1 | list(T48), SCOPE: 24, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
234 [label="234: list(T48), SCOPE: 24, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
235 [label="235: list(T48), SCOPE: 24, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
236 [label="236: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
238 [label="238: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
239 [label="239: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
255 [label="255: ','(no(empty(T53)), ','(tail(T53, X100), list(X100)))\n\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
258 [label="258: ','(no(empty(T53)), ','(tail(T53, X100), list(X100))), SCOPE: 25, CLAUSE: 11 | ','(no(empty(T53)), ','(tail(T53, X100), list(X100))), SCOPE: 25, CLAUSE: 12\n\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
259 [label="259: ','(','(call(empty(T58)), ','(!_25, failure(a))), ','(tail(T58, X100), list(X100))) | ','(no(empty(T53)), ','(tail(T53, X100), list(X100))), SCOPE: 25, CLAUSE: 12\n\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
260 [label="260: ','(empty(T58), ','(','(!_25, failure(a)), ','(tail(T58, X100), list(X100)))) | ?_26 | ','(no(empty(T53)), ','(tail(T53, X100), list(X100))), SCOPE: 25, CLAUSE: 12\n\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
261 [label="261: ','(empty(T58), ','(','(!_25, failure(a)), ','(tail(T58, X100), list(X100)))), SCOPE: 27, CLAUSE: 9 | ?_27 | ?_26 | ','(no(empty(T53)), ','(tail(T53, X100), list(X100))), SCOPE: 25, CLAUSE: 12\n\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
262 [label="262: ','(','(!_25, failure(a)), ','(tail([], X100), list(X100))) | ?_27 | ?_26 | ','(no(empty(T53)), ','(tail(T53, X100), list(X100))), SCOPE: 25, CLAUSE: 12\n\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
263 [label="263: ?_27 | ?_26 | ','(no(empty(T53)), ','(tail(T53, X100), list(X100))), SCOPE: 25, CLAUSE: 12\n\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
264 [label="264: ','(failure(a), ','(tail([], X100), list(X100)))\n\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
265 [label="265: ','(failure(a), ','(tail([], X100), list(X100))), SCOPE: 28, CLAUSE: 13\n\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
266 [label="266: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
267 [label="267: ?_26 | ','(no(empty(T53)), ','(tail(T53, X100), list(X100))), SCOPE: 25, CLAUSE: 12\n\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
268 [label="268: ','(no(empty(T53)), ','(tail(T53, X100), list(X100))), SCOPE: 25, CLAUSE: 12\n\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
269 [label="269: ','(tail(T63, X100), list(X100))\n\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
270 [label="270: ','(tail(T63, X100), list(X100)), SCOPE: 29, CLAUSE: 5 | ','(tail(T63, X100), list(X100)), SCOPE: 29, CLAUSE: 6\n\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
271 [label="271: ','(tail(T63, X100), list(X100)), SCOPE: 29, CLAUSE: 5\n\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
272 [label="272: ','(tail(T63, X100), list(X100)), SCOPE: 29, CLAUSE: 6\n\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
273 [label="273: list([])\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
274 [label="274: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
275 [label="275: list(T70)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
276 [label="276: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
277 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 277 [arrowhead = none ];
277 -> 4;

278 [label="ONLY EVAL with clause\ngoal(X5) :- ','(s2l(X5, X6), list(X6)).\nand substitutionT1 -> T3,\nX5 -> T3", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 278 [arrowhead = none ];
278 -> 12;

279 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
12 -> 279 [arrowhead = none ];
279 -> 13;

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

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

282 [label="EVAL with clause\ns2l(0, []).\nand substitutionT3 -> 0,\nX6 -> []", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 282 [arrowhead = none ];
282 -> 18;

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

284 [label="ONLY EVAL with clause\ns2l(X26, .(X27, X28)) :- ','(no(zero(X26)), ','(p(X26, X29), s2l(X29, X28))).\nand substitutionT3 -> T6,\nX26 -> T6,\nX27 -> X30,\nX28 -> X31,\nX6 -> .(X30, X31)", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 284 [arrowhead = none ];
284 -> 76;

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

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

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

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

289 [label="ONLY EVAL with clause\nlist(X10) :- ','(no(empty(X10)), ','(tail(X10, X11), list(X11))).\nand substitutionX10 -> []", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 289 [arrowhead = none ];
289 -> 34;

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

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

292 [label="ONLY EVAL with clause\nno(X14) :- ','(call(X14), ','(!_4, failure(a))).\nand substitutionX14 -> empty([])", fontsize=14, style = filled, fillcolor = lightblue];
39 -> 292 [arrowhead = none ];
292 -> 44;

293 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
44 -> 293 [arrowhead = none ];
293 -> 45;

294 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
45 -> 294 [arrowhead = none ];
294 -> 47;

295 [label="ONLY EVAL with clause\nempty([]).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 295 [arrowhead = none ];
295 -> 52;

296 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
52 -> 296 [arrowhead = none ];
296 -> 63;

297 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
63 -> 297 [arrowhead = none ];
297 -> 66;

298 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
66 -> 298 [arrowhead = none ];
298 -> 67;

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

300 [label="ONLY EVAL with clause\nno(X34) :- ','(call(X34), ','(!_8, failure(a))).\nand substitutionT6 -> T9,\nX34 -> zero(T9)", fontsize=14, style = filled, fillcolor = lightblue];
78 -> 300 [arrowhead = none ];
300 -> 86;

301 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
86 -> 301 [arrowhead = none ];
301 -> 88;

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

303 [label="EVAL with clause\nzero(0).\nand substitutionT9 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
89 -> 303 [arrowhead = none ];
303 -> 92;

304 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
89 -> 304 [arrowhead = none ];
304 -> 95;

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

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

307 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
96 -> 307 [arrowhead = none ];
307 -> 102;

308 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
102 -> 308 [arrowhead = none ];
308 -> 103;

309 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
104 -> 309 [arrowhead = none ];
309 -> 105;

310 [label="ONLY EVAL with clause\nno(X37).\nand substitutionT9 -> T12,\nX37 -> zero(T12)", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 310 [arrowhead = none ];
310 -> 109;

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

312 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T12), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
111 -> 312 [arrowhead = none ];
312 -> 112;

313 [label="EVAL with clause\np(s(X40), X40).\nand substitutionX40 -> T15,\nT12 -> s(T15),\nX29 -> T15", fontsize=14, style = filled, fillcolor = lightblue];
112 -> 313 [arrowhead = none ];
313 -> 113;

314 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
112 -> 314 [arrowhead = none ];
314 -> 117;

315 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
113 -> 315 [arrowhead = none ];
315 -> 133;

316 [label="SPLIT 2\nnew knowledge:\nT15 is ground\nreplacements:X31 -> T16", fontsize=14, style = filled, fillcolor = violet];
113 -> 316 [arrowhead = none ];
316 -> 134;

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

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

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

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

321 [label="EVAL with clause\ns2l(0, []).\nand substitutionT15 -> 0,\nX31 -> []", fontsize=14, style = filled, fillcolor = lightblue];
140 -> 321 [arrowhead = none ];
321 -> 144;

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

323 [label="ONLY EVAL with clause\ns2l(X52, .(X53, X54)) :- ','(no(zero(X52)), ','(p(X52, X55), s2l(X55, X54))).\nand substitutionT15 -> T19,\nX52 -> T19,\nX53 -> X56,\nX54 -> X57,\nX31 -> .(X56, X57)", fontsize=14, style = filled, fillcolor = lightblue];
141 -> 323 [arrowhead = none ];
323 -> 165;

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

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

326 [label="ONLY EVAL with clause\nno(X60) :- ','(call(X60), ','(!_14, failure(a))).\nand substitutionT19 -> T22,\nX60 -> zero(T22)", fontsize=14, style = filled, fillcolor = lightblue];
167 -> 326 [arrowhead = none ];
326 -> 171;

327 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
171 -> 327 [arrowhead = none ];
327 -> 174;

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

329 [label="EVAL with clause\nzero(0).\nand substitutionT22 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
176 -> 329 [arrowhead = none ];
329 -> 179;

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

331 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
179 -> 331 [arrowhead = none ];
331 -> 183;

332 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
181 -> 332 [arrowhead = none ];
332 -> 188;

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

334 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
186 -> 334 [arrowhead = none ];
334 -> 187;

335 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
188 -> 335 [arrowhead = none ];
335 -> 189;

336 [label="ONLY EVAL with clause\nno(X63).\nand substitutionT22 -> T25,\nX63 -> zero(T25)", fontsize=14, style = filled, fillcolor = lightblue];
189 -> 336 [arrowhead = none ];
336 -> 194;

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

338 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (zero(T25), zero(0))", fontsize=14, style = filled, fillcolor = lightgreen];
195 -> 338 [arrowhead = none ];
338 -> 196;

339 [label="EVAL with clause\np(s(X66), X66).\nand substitutionX66 -> T28,\nT25 -> s(T28),\nX55 -> T28", fontsize=14, style = filled, fillcolor = lightblue];
196 -> 339 [arrowhead = none ];
339 -> 197;

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

341 [label="INSTANCE with matching:\nT15 -> T28\nX31 -> X57", fontsize=14, style = filled, fillcolor = lightgrey];
197 -> 341 [arrowhead = none , style=dashed];
341 -> 133[style=dashed];

342 [label="BACKTRACK\nfor clause: list([])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
201 -> 342 [arrowhead = none ];
342 -> 202;

343 [label="ONLY EVAL with clause\nlist(X72) :- ','(no(empty(X72)), ','(tail(X72, X73), list(X73))).\nand substitutionX30 -> X74,\nT16 -> T33,\nX72 -> .(X74, T33),\nT32 -> T33", fontsize=14, style = filled, fillcolor = lightblue];
202 -> 343 [arrowhead = none ];
343 -> 209;

344 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
209 -> 344 [arrowhead = none ];
344 -> 210;

345 [label="ONLY EVAL with clause\nno(X79) :- ','(call(X79), ','(!_20, failure(a))).\nand substitutionX74 -> X80,\nT33 -> T38,\nX79 -> empty(.(X80, T38)),\nT37 -> T38", fontsize=14, style = filled, fillcolor = lightblue];
210 -> 345 [arrowhead = none ];
345 -> 214;

346 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
214 -> 346 [arrowhead = none ];
346 -> 215;

347 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
215 -> 347 [arrowhead = none ];
347 -> 216;

348 [label="BACKTRACK\nfor clause: empty([])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
216 -> 348 [arrowhead = none ];
348 -> 217;

349 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
217 -> 349 [arrowhead = none ];
349 -> 218;

350 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
218 -> 350 [arrowhead = none ];
350 -> 219;

351 [label="ONLY EVAL with clause\nno(X85).\nand substitutionX74 -> X86,\nT33 -> T43,\nX85 -> empty(.(X86, T43)),\nT42 -> T43", fontsize=14, style = filled, fillcolor = lightblue];
219 -> 351 [arrowhead = none ];
351 -> 221;

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

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

354 [label="ONLY EVAL with clause\ntail(.(X93, X94), X94).\nand substitutionX86 -> X95,\nX93 -> X95,\nT43 -> T48,\nX94 -> T48,\nX73 -> T48,\nT47 -> T48", fontsize=14, style = filled, fillcolor = lightblue];
223 -> 354 [arrowhead = none ];
354 -> 231;

355 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
231 -> 355 [arrowhead = none ];
355 -> 233;

356 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
233 -> 356 [arrowhead = none ];
356 -> 234;

357 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
233 -> 357 [arrowhead = none ];
357 -> 235;

358 [label="EVAL with clause\nlist([]).\nand substitutionT48 -> []", fontsize=14, style = filled, fillcolor = lightblue];
234 -> 358 [arrowhead = none ];
358 -> 236;

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

360 [label="ONLY EVAL with clause\nlist(X99) :- ','(no(empty(X99)), ','(tail(X99, X100), list(X100))).\nand substitutionT48 -> T53,\nX99 -> T53,\nT52 -> T53", fontsize=14, style = filled, fillcolor = lightblue];
235 -> 360 [arrowhead = none ];
360 -> 255;

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

362 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
255 -> 362 [arrowhead = none ];
362 -> 258;

363 [label="ONLY EVAL with clause\nno(X103) :- ','(call(X103), ','(!_25, failure(a))).\nand substitutionT53 -> T58,\nX103 -> empty(T58),\nT57 -> T58", fontsize=14, style = filled, fillcolor = lightblue];
258 -> 363 [arrowhead = none ];
363 -> 259;

364 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
259 -> 364 [arrowhead = none ];
364 -> 260;

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

366 [label="EVAL with clause\nempty([]).\nand substitutionT58 -> []", fontsize=14, style = filled, fillcolor = lightblue];
261 -> 366 [arrowhead = none ];
366 -> 262;

367 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
261 -> 367 [arrowhead = none ];
367 -> 263;

368 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
262 -> 368 [arrowhead = none ];
368 -> 264;

369 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
263 -> 369 [arrowhead = none ];
369 -> 267;

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

371 [label="BACKTRACK\nfor clause: failure(b)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
265 -> 371 [arrowhead = none ];
371 -> 266;

372 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
267 -> 372 [arrowhead = none ];
372 -> 268;

373 [label="ONLY EVAL with clause\nno(X106).\nand substitutionT53 -> T63,\nX106 -> empty(T63),\nT62 -> T63", fontsize=14, style = filled, fillcolor = lightblue];
268 -> 373 [arrowhead = none ];
373 -> 269;

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

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

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

377 [label="EVAL with clause\ntail([], []).\nand substitutionT63 -> [],\nX100 -> []", fontsize=14, style = filled, fillcolor = lightblue];
271 -> 377 [arrowhead = none ];
377 -> 273;

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

379 [label="EVAL with clause\ntail(.(X111, X112), X112).\nand substitutionX111 -> T68,\nX112 -> T70,\nT63 -> .(T68, T70),\nX100 -> T70,\nT69 -> T70", fontsize=14, style = filled, fillcolor = lightblue];
272 -> 379 [arrowhead = none ];
379 -> 275;

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

381 [label="INSTANCE", fontsize=14, style = filled, fillcolor = lightgrey];
273 -> 381 [arrowhead = none , style=dashed];
381 -> 18[style=dashed];

382 [label="INSTANCE with matching:\nT48 -> T70", fontsize=14, style = filled, fillcolor = lightgrey];
275 -> 382 [arrowhead = none , style=dashed];
382 -> 231[style=dashed];

}

(2) Obligation:

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

goalA_in_g(0) → U1_g(listB_in_)
listB_in_ → listB_out_
U1_g(listB_out_) → goalA_out_g(0)
goalA_in_g(s(T15)) → U2_g(T15, pC_in_gaa(T15, X31, X30))
pC_in_gaa(T15, T16, X30) → U7_gaa(T15, T16, X30, s2lD_in_ga(T15, T16))
s2lD_in_ga(0, []) → s2lD_out_ga(0, [])
s2lD_in_ga(s(T28), .(X56, X57)) → U3_ga(T28, X56, X57, s2lD_in_ga(T28, X57))
U3_ga(T28, X56, X57, s2lD_out_ga(T28, X57)) → s2lD_out_ga(s(T28), .(X56, X57))
U7_gaa(T15, T16, X30, s2lD_out_ga(T15, T16)) → U8_gaa(T15, T16, X30, listF_in_ag(X30, T16))
listF_in_ag(X95, T48) → U6_ag(X95, T48, listE_in_g(T48))
listE_in_g([]) → listE_out_g([])
listE_in_g([]) → U4_g(listB_in_)
U4_g(listB_out_) → listE_out_g([])
listE_in_g(.(T68, T70)) → U5_g(T68, T70, listE_in_g(T70))
U5_g(T68, T70, listE_out_g(T70)) → listE_out_g(.(T68, T70))
U6_ag(X95, T48, listE_out_g(T48)) → listF_out_ag(X95, T48)
U8_gaa(T15, T16, X30, listF_out_ag(X30, T16)) → pC_out_gaa(T15, T16, X30)
U2_g(T15, pC_out_gaa(T15, X31, X30)) → goalA_out_g(s(T15))

The argument filtering Pi contains the following mapping:
goalA_in_g(x1)  =  goalA_in_g(x1)
0  =  0
U1_g(x1)  =  U1_g(x1)
listB_in_  =  listB_in_
listB_out_  =  listB_out_
goalA_out_g(x1)  =  goalA_out_g(x1)
s(x1)  =  s(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
pC_in_gaa(x1, x2, x3)  =  pC_in_gaa(x1)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x1, x4)
s2lD_in_ga(x1, x2)  =  s2lD_in_ga(x1)
s2lD_out_ga(x1, x2)  =  s2lD_out_ga(x1, x2)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x1, x4)
.(x1, x2)  =  .(x2)
U8_gaa(x1, x2, x3, x4)  =  U8_gaa(x1, x2, x4)
listF_in_ag(x1, x2)  =  listF_in_ag(x2)
U6_ag(x1, x2, x3)  =  U6_ag(x2, x3)
listE_in_g(x1)  =  listE_in_g(x1)
[]  =  []
listE_out_g(x1)  =  listE_out_g(x1)
U4_g(x1)  =  U4_g(x1)
U5_g(x1, x2, x3)  =  U5_g(x2, x3)
listF_out_ag(x1, x2)  =  listF_out_ag(x2)
pC_out_gaa(x1, x2, x3)  =  pC_out_gaa(x1, x2)

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

GOALA_IN_G(0) → U1_G(listB_in_)
GOALA_IN_G(0) → LISTB_IN_
GOALA_IN_G(s(T15)) → U2_G(T15, pC_in_gaa(T15, X31, X30))
GOALA_IN_G(s(T15)) → PC_IN_GAA(T15, X31, X30)
PC_IN_GAA(T15, T16, X30) → U7_GAA(T15, T16, X30, s2lD_in_ga(T15, T16))
PC_IN_GAA(T15, T16, X30) → S2LD_IN_GA(T15, T16)
S2LD_IN_GA(s(T28), .(X56, X57)) → U3_GA(T28, X56, X57, s2lD_in_ga(T28, X57))
S2LD_IN_GA(s(T28), .(X56, X57)) → S2LD_IN_GA(T28, X57)
U7_GAA(T15, T16, X30, s2lD_out_ga(T15, T16)) → U8_GAA(T15, T16, X30, listF_in_ag(X30, T16))
U7_GAA(T15, T16, X30, s2lD_out_ga(T15, T16)) → LISTF_IN_AG(X30, T16)
LISTF_IN_AG(X95, T48) → U6_AG(X95, T48, listE_in_g(T48))
LISTF_IN_AG(X95, T48) → LISTE_IN_G(T48)
LISTE_IN_G([]) → U4_G(listB_in_)
LISTE_IN_G([]) → LISTB_IN_
LISTE_IN_G(.(T68, T70)) → U5_G(T68, T70, listE_in_g(T70))
LISTE_IN_G(.(T68, T70)) → LISTE_IN_G(T70)

The TRS R consists of the following rules:

goalA_in_g(0) → U1_g(listB_in_)
listB_in_ → listB_out_
U1_g(listB_out_) → goalA_out_g(0)
goalA_in_g(s(T15)) → U2_g(T15, pC_in_gaa(T15, X31, X30))
pC_in_gaa(T15, T16, X30) → U7_gaa(T15, T16, X30, s2lD_in_ga(T15, T16))
s2lD_in_ga(0, []) → s2lD_out_ga(0, [])
s2lD_in_ga(s(T28), .(X56, X57)) → U3_ga(T28, X56, X57, s2lD_in_ga(T28, X57))
U3_ga(T28, X56, X57, s2lD_out_ga(T28, X57)) → s2lD_out_ga(s(T28), .(X56, X57))
U7_gaa(T15, T16, X30, s2lD_out_ga(T15, T16)) → U8_gaa(T15, T16, X30, listF_in_ag(X30, T16))
listF_in_ag(X95, T48) → U6_ag(X95, T48, listE_in_g(T48))
listE_in_g([]) → listE_out_g([])
listE_in_g([]) → U4_g(listB_in_)
U4_g(listB_out_) → listE_out_g([])
listE_in_g(.(T68, T70)) → U5_g(T68, T70, listE_in_g(T70))
U5_g(T68, T70, listE_out_g(T70)) → listE_out_g(.(T68, T70))
U6_ag(X95, T48, listE_out_g(T48)) → listF_out_ag(X95, T48)
U8_gaa(T15, T16, X30, listF_out_ag(X30, T16)) → pC_out_gaa(T15, T16, X30)
U2_g(T15, pC_out_gaa(T15, X31, X30)) → goalA_out_g(s(T15))

The argument filtering Pi contains the following mapping:
goalA_in_g(x1)  =  goalA_in_g(x1)
0  =  0
U1_g(x1)  =  U1_g(x1)
listB_in_  =  listB_in_
listB_out_  =  listB_out_
goalA_out_g(x1)  =  goalA_out_g(x1)
s(x1)  =  s(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
pC_in_gaa(x1, x2, x3)  =  pC_in_gaa(x1)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x1, x4)
s2lD_in_ga(x1, x2)  =  s2lD_in_ga(x1)
s2lD_out_ga(x1, x2)  =  s2lD_out_ga(x1, x2)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x1, x4)
.(x1, x2)  =  .(x2)
U8_gaa(x1, x2, x3, x4)  =  U8_gaa(x1, x2, x4)
listF_in_ag(x1, x2)  =  listF_in_ag(x2)
U6_ag(x1, x2, x3)  =  U6_ag(x2, x3)
listE_in_g(x1)  =  listE_in_g(x1)
[]  =  []
listE_out_g(x1)  =  listE_out_g(x1)
U4_g(x1)  =  U4_g(x1)
U5_g(x1, x2, x3)  =  U5_g(x2, x3)
listF_out_ag(x1, x2)  =  listF_out_ag(x2)
pC_out_gaa(x1, x2, x3)  =  pC_out_gaa(x1, x2)
GOALA_IN_G(x1)  =  GOALA_IN_G(x1)
U1_G(x1)  =  U1_G(x1)
LISTB_IN_  =  LISTB_IN_
U2_G(x1, x2)  =  U2_G(x1, x2)
PC_IN_GAA(x1, x2, x3)  =  PC_IN_GAA(x1)
U7_GAA(x1, x2, x3, x4)  =  U7_GAA(x1, x4)
S2LD_IN_GA(x1, x2)  =  S2LD_IN_GA(x1)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x4)
U8_GAA(x1, x2, x3, x4)  =  U8_GAA(x1, x2, x4)
LISTF_IN_AG(x1, x2)  =  LISTF_IN_AG(x2)
U6_AG(x1, x2, x3)  =  U6_AG(x2, x3)
LISTE_IN_G(x1)  =  LISTE_IN_G(x1)
U4_G(x1)  =  U4_G(x1)
U5_G(x1, x2, x3)  =  U5_G(x2, x3)

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

(4) Obligation:

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

GOALA_IN_G(0) → U1_G(listB_in_)
GOALA_IN_G(0) → LISTB_IN_
GOALA_IN_G(s(T15)) → U2_G(T15, pC_in_gaa(T15, X31, X30))
GOALA_IN_G(s(T15)) → PC_IN_GAA(T15, X31, X30)
PC_IN_GAA(T15, T16, X30) → U7_GAA(T15, T16, X30, s2lD_in_ga(T15, T16))
PC_IN_GAA(T15, T16, X30) → S2LD_IN_GA(T15, T16)
S2LD_IN_GA(s(T28), .(X56, X57)) → U3_GA(T28, X56, X57, s2lD_in_ga(T28, X57))
S2LD_IN_GA(s(T28), .(X56, X57)) → S2LD_IN_GA(T28, X57)
U7_GAA(T15, T16, X30, s2lD_out_ga(T15, T16)) → U8_GAA(T15, T16, X30, listF_in_ag(X30, T16))
U7_GAA(T15, T16, X30, s2lD_out_ga(T15, T16)) → LISTF_IN_AG(X30, T16)
LISTF_IN_AG(X95, T48) → U6_AG(X95, T48, listE_in_g(T48))
LISTF_IN_AG(X95, T48) → LISTE_IN_G(T48)
LISTE_IN_G([]) → U4_G(listB_in_)
LISTE_IN_G([]) → LISTB_IN_
LISTE_IN_G(.(T68, T70)) → U5_G(T68, T70, listE_in_g(T70))
LISTE_IN_G(.(T68, T70)) → LISTE_IN_G(T70)

The TRS R consists of the following rules:

goalA_in_g(0) → U1_g(listB_in_)
listB_in_ → listB_out_
U1_g(listB_out_) → goalA_out_g(0)
goalA_in_g(s(T15)) → U2_g(T15, pC_in_gaa(T15, X31, X30))
pC_in_gaa(T15, T16, X30) → U7_gaa(T15, T16, X30, s2lD_in_ga(T15, T16))
s2lD_in_ga(0, []) → s2lD_out_ga(0, [])
s2lD_in_ga(s(T28), .(X56, X57)) → U3_ga(T28, X56, X57, s2lD_in_ga(T28, X57))
U3_ga(T28, X56, X57, s2lD_out_ga(T28, X57)) → s2lD_out_ga(s(T28), .(X56, X57))
U7_gaa(T15, T16, X30, s2lD_out_ga(T15, T16)) → U8_gaa(T15, T16, X30, listF_in_ag(X30, T16))
listF_in_ag(X95, T48) → U6_ag(X95, T48, listE_in_g(T48))
listE_in_g([]) → listE_out_g([])
listE_in_g([]) → U4_g(listB_in_)
U4_g(listB_out_) → listE_out_g([])
listE_in_g(.(T68, T70)) → U5_g(T68, T70, listE_in_g(T70))
U5_g(T68, T70, listE_out_g(T70)) → listE_out_g(.(T68, T70))
U6_ag(X95, T48, listE_out_g(T48)) → listF_out_ag(X95, T48)
U8_gaa(T15, T16, X30, listF_out_ag(X30, T16)) → pC_out_gaa(T15, T16, X30)
U2_g(T15, pC_out_gaa(T15, X31, X30)) → goalA_out_g(s(T15))

The argument filtering Pi contains the following mapping:
goalA_in_g(x1)  =  goalA_in_g(x1)
0  =  0
U1_g(x1)  =  U1_g(x1)
listB_in_  =  listB_in_
listB_out_  =  listB_out_
goalA_out_g(x1)  =  goalA_out_g(x1)
s(x1)  =  s(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
pC_in_gaa(x1, x2, x3)  =  pC_in_gaa(x1)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x1, x4)
s2lD_in_ga(x1, x2)  =  s2lD_in_ga(x1)
s2lD_out_ga(x1, x2)  =  s2lD_out_ga(x1, x2)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x1, x4)
.(x1, x2)  =  .(x2)
U8_gaa(x1, x2, x3, x4)  =  U8_gaa(x1, x2, x4)
listF_in_ag(x1, x2)  =  listF_in_ag(x2)
U6_ag(x1, x2, x3)  =  U6_ag(x2, x3)
listE_in_g(x1)  =  listE_in_g(x1)
[]  =  []
listE_out_g(x1)  =  listE_out_g(x1)
U4_g(x1)  =  U4_g(x1)
U5_g(x1, x2, x3)  =  U5_g(x2, x3)
listF_out_ag(x1, x2)  =  listF_out_ag(x2)
pC_out_gaa(x1, x2, x3)  =  pC_out_gaa(x1, x2)
GOALA_IN_G(x1)  =  GOALA_IN_G(x1)
U1_G(x1)  =  U1_G(x1)
LISTB_IN_  =  LISTB_IN_
U2_G(x1, x2)  =  U2_G(x1, x2)
PC_IN_GAA(x1, x2, x3)  =  PC_IN_GAA(x1)
U7_GAA(x1, x2, x3, x4)  =  U7_GAA(x1, x4)
S2LD_IN_GA(x1, x2)  =  S2LD_IN_GA(x1)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x4)
U8_GAA(x1, x2, x3, x4)  =  U8_GAA(x1, x2, x4)
LISTF_IN_AG(x1, x2)  =  LISTF_IN_AG(x2)
U6_AG(x1, x2, x3)  =  U6_AG(x2, x3)
LISTE_IN_G(x1)  =  LISTE_IN_G(x1)
U4_G(x1)  =  U4_G(x1)
U5_G(x1, x2, x3)  =  U5_G(x2, x3)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

LISTE_IN_G(.(T68, T70)) → LISTE_IN_G(T70)

The TRS R consists of the following rules:

goalA_in_g(0) → U1_g(listB_in_)
listB_in_ → listB_out_
U1_g(listB_out_) → goalA_out_g(0)
goalA_in_g(s(T15)) → U2_g(T15, pC_in_gaa(T15, X31, X30))
pC_in_gaa(T15, T16, X30) → U7_gaa(T15, T16, X30, s2lD_in_ga(T15, T16))
s2lD_in_ga(0, []) → s2lD_out_ga(0, [])
s2lD_in_ga(s(T28), .(X56, X57)) → U3_ga(T28, X56, X57, s2lD_in_ga(T28, X57))
U3_ga(T28, X56, X57, s2lD_out_ga(T28, X57)) → s2lD_out_ga(s(T28), .(X56, X57))
U7_gaa(T15, T16, X30, s2lD_out_ga(T15, T16)) → U8_gaa(T15, T16, X30, listF_in_ag(X30, T16))
listF_in_ag(X95, T48) → U6_ag(X95, T48, listE_in_g(T48))
listE_in_g([]) → listE_out_g([])
listE_in_g([]) → U4_g(listB_in_)
U4_g(listB_out_) → listE_out_g([])
listE_in_g(.(T68, T70)) → U5_g(T68, T70, listE_in_g(T70))
U5_g(T68, T70, listE_out_g(T70)) → listE_out_g(.(T68, T70))
U6_ag(X95, T48, listE_out_g(T48)) → listF_out_ag(X95, T48)
U8_gaa(T15, T16, X30, listF_out_ag(X30, T16)) → pC_out_gaa(T15, T16, X30)
U2_g(T15, pC_out_gaa(T15, X31, X30)) → goalA_out_g(s(T15))

The argument filtering Pi contains the following mapping:
goalA_in_g(x1)  =  goalA_in_g(x1)
0  =  0
U1_g(x1)  =  U1_g(x1)
listB_in_  =  listB_in_
listB_out_  =  listB_out_
goalA_out_g(x1)  =  goalA_out_g(x1)
s(x1)  =  s(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
pC_in_gaa(x1, x2, x3)  =  pC_in_gaa(x1)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x1, x4)
s2lD_in_ga(x1, x2)  =  s2lD_in_ga(x1)
s2lD_out_ga(x1, x2)  =  s2lD_out_ga(x1, x2)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x1, x4)
.(x1, x2)  =  .(x2)
U8_gaa(x1, x2, x3, x4)  =  U8_gaa(x1, x2, x4)
listF_in_ag(x1, x2)  =  listF_in_ag(x2)
U6_ag(x1, x2, x3)  =  U6_ag(x2, x3)
listE_in_g(x1)  =  listE_in_g(x1)
[]  =  []
listE_out_g(x1)  =  listE_out_g(x1)
U4_g(x1)  =  U4_g(x1)
U5_g(x1, x2, x3)  =  U5_g(x2, x3)
listF_out_ag(x1, x2)  =  listF_out_ag(x2)
pC_out_gaa(x1, x2, x3)  =  pC_out_gaa(x1, x2)
LISTE_IN_G(x1)  =  LISTE_IN_G(x1)

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:

LISTE_IN_G(.(T68, T70)) → LISTE_IN_G(T70)

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

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

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

LISTE_IN_G(.(T70)) → LISTE_IN_G(T70)

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:

• LISTE_IN_G(.(T70)) → LISTE_IN_G(T70)
  The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

S2LD_IN_GA(s(T28), .(X56, X57)) → S2LD_IN_GA(T28, X57)

The TRS R consists of the following rules:

goalA_in_g(0) → U1_g(listB_in_)
listB_in_ → listB_out_
U1_g(listB_out_) → goalA_out_g(0)
goalA_in_g(s(T15)) → U2_g(T15, pC_in_gaa(T15, X31, X30))
pC_in_gaa(T15, T16, X30) → U7_gaa(T15, T16, X30, s2lD_in_ga(T15, T16))
s2lD_in_ga(0, []) → s2lD_out_ga(0, [])
s2lD_in_ga(s(T28), .(X56, X57)) → U3_ga(T28, X56, X57, s2lD_in_ga(T28, X57))
U3_ga(T28, X56, X57, s2lD_out_ga(T28, X57)) → s2lD_out_ga(s(T28), .(X56, X57))
U7_gaa(T15, T16, X30, s2lD_out_ga(T15, T16)) → U8_gaa(T15, T16, X30, listF_in_ag(X30, T16))
listF_in_ag(X95, T48) → U6_ag(X95, T48, listE_in_g(T48))
listE_in_g([]) → listE_out_g([])
listE_in_g([]) → U4_g(listB_in_)
U4_g(listB_out_) → listE_out_g([])
listE_in_g(.(T68, T70)) → U5_g(T68, T70, listE_in_g(T70))
U5_g(T68, T70, listE_out_g(T70)) → listE_out_g(.(T68, T70))
U6_ag(X95, T48, listE_out_g(T48)) → listF_out_ag(X95, T48)
U8_gaa(T15, T16, X30, listF_out_ag(X30, T16)) → pC_out_gaa(T15, T16, X30)
U2_g(T15, pC_out_gaa(T15, X31, X30)) → goalA_out_g(s(T15))

The argument filtering Pi contains the following mapping:
goalA_in_g(x1)  =  goalA_in_g(x1)
0  =  0
U1_g(x1)  =  U1_g(x1)
listB_in_  =  listB_in_
listB_out_  =  listB_out_
goalA_out_g(x1)  =  goalA_out_g(x1)
s(x1)  =  s(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
pC_in_gaa(x1, x2, x3)  =  pC_in_gaa(x1)
U7_gaa(x1, x2, x3, x4)  =  U7_gaa(x1, x4)
s2lD_in_ga(x1, x2)  =  s2lD_in_ga(x1)
s2lD_out_ga(x1, x2)  =  s2lD_out_ga(x1, x2)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x1, x4)
.(x1, x2)  =  .(x2)
U8_gaa(x1, x2, x3, x4)  =  U8_gaa(x1, x2, x4)
listF_in_ag(x1, x2)  =  listF_in_ag(x2)
U6_ag(x1, x2, x3)  =  U6_ag(x2, x3)
listE_in_g(x1)  =  listE_in_g(x1)
[]  =  []
listE_out_g(x1)  =  listE_out_g(x1)
U4_g(x1)  =  U4_g(x1)
U5_g(x1, x2, x3)  =  U5_g(x2, x3)
listF_out_ag(x1, x2)  =  listF_out_ag(x2)
pC_out_gaa(x1, x2, x3)  =  pC_out_gaa(x1, x2)
S2LD_IN_GA(x1, x2)  =  S2LD_IN_GA(x1)

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:

S2LD_IN_GA(s(T28), .(X56, X57)) → S2LD_IN_GA(T28, X57)

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

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

S2LD_IN_GA(s(T28)) → S2LD_IN_GA(T28)

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:

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

(20) YES