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) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph ICLP10.

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, 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];
24 [label="24: ','(','(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];
25 [label="25: ','(','(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];
26 [label="26: ','(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];
27 [label="27: ','(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];
28 [label="28: ','(','(!_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];
29 [label="29: ?_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];
30 [label="30: ','(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];
31 [label="31: ','(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];
32 [label="32: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ?_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];
34 [label="34: ','(','(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];
35 [label="35: ','(','(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];
36 [label="36: ','(','(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];
37 [label="37: ','(','(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];
38 [label="38: ','(s2l(T15, X31), list(.(X30, X31)))\n\nT15 is ground\nX30 is free\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: s2l(T15, X31)\n\nT15 is ground\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: list(.(X30, T16))\n\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: 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];
43 [label="43: s2l(T15, X31), SCOPE: 13, CLAUSE: 3\n\nT15 is ground\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: s2l(T15, X31), SCOPE: 13, CLAUSE: 4\n\nT15 is ground\nX31 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, X55), s2l(X55, X57)))\n\nT19 is ground\nX57 is free\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(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];
50 [label="50: ','(','(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];
51 [label="51: ','(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];
52 [label="52: ','(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];
53 [label="53: ','(','(!_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];
54 [label="54: ?_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];
55 [label="55: ','(failure(a), ','(p(0, X55), s2l(X55, X57)))\n\nX57 is free\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ','(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];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ?_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];
59 [label="59: ','(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];
60 [label="60: ','(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];
61 [label="61: ','(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];
62 [label="62: ','(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];
63 [label="63: s2l(T28, X57)\n\nT28 is ground\nX57 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: list(.(X30, T16)), SCOPE: 19, CLAUSE: 1 | list(.(X30, T16)), SCOPE: 19, CLAUSE: 2\n\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: list(.(X30, T16)), SCOPE: 19, CLAUSE: 2\n\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: ','(no(empty(.(X74, T33))), ','(tail(.(X74, T33), X73), list(X73)))\n\nX74 is free\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(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];
69 [label="69: ','(','(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];
70 [label="70: ','(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];
71 [label="71: ','(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];
72 [label="72: ?_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];
73 [label="73: ?_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];
74 [label="74: ','(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];
75 [label="75: ','(tail(.(X86, T43), X73), list(X73))\n\nX73 is free\nX86 is free", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: ','(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];
77 [label="77: ','(tail(.(X86, T43), X73), list(X73)), SCOPE: 23, CLAUSE: 6\n\nX73 is free\nX86 is free", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: list(T48)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: list(T48), SCOPE: 24, CLAUSE: 1 | list(T48), SCOPE: 24, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: list(T48), SCOPE: 24, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: list(T48), 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(T53)), ','(tail(T53, X100), list(X100)))\n\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(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];
87 [label="87: ','(','(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];
88 [label="88: ','(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];
89 [label="89: ','(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];
90 [label="90: ','(','(!_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];
91 [label="91: ?_27 | ?_26 | ','(no(empty(T53)), ','(tail(T53, X100), list(X100))), SCOPE: 25, CLAUSE: 12\n\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(failure(a), ','(tail([], X100), list(X100)))\n\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: ','(failure(a), ','(tail([], X100), list(X100))), SCOPE: 28, CLAUSE: 13\n\nX100 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(T53)), ','(tail(T53, X100), list(X100))), SCOPE: 25, CLAUSE: 12\n\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(no(empty(T53)), ','(tail(T53, X100), list(X100))), SCOPE: 25, CLAUSE: 12\n\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(tail(T63, X100), list(X100))\n\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(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];
99 [label="99: ','(tail(T63, X100), list(X100)), SCOPE: 29, CLAUSE: 5\n\nX100 is free", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: ','(tail(T63, X100), list(X100)), SCOPE: 29, CLAUSE: 6\n\nX100 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(T70)\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 substitutionT1 -> T3,\nX5 -> T3", fontsize=14, style = filled, fillcolor = lightblue];
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 substitutionT3 -> 0,\nX6 -> []", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 110 [arrowhead = none ];
110 -> 7;

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

112 [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];
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 = lightblue];
10 -> 116 [arrowhead = none ];
116 -> 12;

117 [label="ONLY EVAL with clause\nlist(X10) :- ','(no(empty(X10)), ','(tail(X10, X11), list(X11))).\nand substitutionX10 -> []", fontsize=14, style = filled, fillcolor = lightblue];
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 substitutionX14 -> empty([])", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 120 [arrowhead = none ];
120 -> 16;

121 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
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 = lightblue];
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 = lightgreen];
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(X34) :- ','(call(X34), ','(!_8, failure(a))).\nand substitutionT6 -> T9,\nX34 -> zero(T9)", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 128 [arrowhead = none ];
128 -> 25;

129 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
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 substitutionT9 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
27 -> 131 [arrowhead = none ];
131 -> 28;

132 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
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 = lightgreen];
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(X37).\nand substitutionT9 -> T12,\nX37 -> zero(T12)", fontsize=14, style = filled, fillcolor = lightblue];
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 = lightgreen];
36 -> 140 [arrowhead = none ];
140 -> 37;

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

142 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
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\nnew knowledge:\nT15 is ground\nreplacements:X31 -> 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 substitutionT15 -> 0,\nX31 -> []", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 149 [arrowhead = none ];
149 -> 45;

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

151 [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];
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(X60) :- ','(call(X60), ','(!_14, failure(a))).\nand substitutionT19 -> T22,\nX60 -> zero(T22)", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 154 [arrowhead = none ];
154 -> 50;

155 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
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 substitutionT22 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
52 -> 157 [arrowhead = none ];
157 -> 53;

158 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
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 = lightgreen];
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(X63).\nand substitutionT22 -> T25,\nX63 -> zero(T25)", fontsize=14, style = filled, fillcolor = lightblue];
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 = lightgreen];
61 -> 166 [arrowhead = none ];
166 -> 62;

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

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

169 [label="INSTANCE with matching:\nT15 -> T28\nX31 -> X57", 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 = lightgreen];
65 -> 170 [arrowhead = none ];
170 -> 66;

171 [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];
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(X79) :- ','(call(X79), ','(!_20, failure(a))).\nand substitutionX74 -> X80,\nT33 -> T38,\nX79 -> empty(.(X80, T38)),\nT37 -> T38", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 173 [arrowhead = none ];
173 -> 69;

174 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
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 = lightgreen];
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(X85).\nand substitutionX74 -> X86,\nT33 -> T43,\nX85 -> empty(.(X86, T43)),\nT42 -> T43", fontsize=14, style = filled, fillcolor = lightblue];
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 = lightgreen];
76 -> 181 [arrowhead = none ];
181 -> 77;

182 [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];
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 substitutionT48 -> []", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 186 [arrowhead = none ];
186 -> 82;

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

188 [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];
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(X103) :- ','(call(X103), ','(!_25, failure(a))).\nand substitutionT53 -> T58,\nX103 -> empty(T58),\nT57 -> T58", fontsize=14, style = filled, fillcolor = lightblue];
86 -> 191 [arrowhead = none ];
191 -> 87;

192 [label="CALL", fontsize=14, style = filled, fillcolor = lightcyan];
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 substitutionT58 -> []", fontsize=14, style = filled, fillcolor = lightblue];
89 -> 194 [arrowhead = none ];
194 -> 90;

195 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
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 = lightgreen];
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(X106).\nand substitutionT53 -> T63,\nX106 -> empty(T63),\nT62 -> T63", fontsize=14, style = filled, fillcolor = lightblue];
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 substitutionT63 -> [],\nX100 -> []", fontsize=14, style = filled, fillcolor = lightblue];
99 -> 205 [arrowhead = none ];
205 -> 101;

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

207 [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];
100 -> 207 [arrowhead = none ];
207 -> 103;

208 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
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:\nT48 -> T70", fontsize=14, style = filled, fillcolor = lightgrey];
103 -> 210 [arrowhead = none , style=dashed];
210 -> 78[style=dashed];

}

(2) Obligation:

Clauses:

s2lA(0, []).
s2lA(s(T28), .(X56, X57)) :- s2lA(T28, X57).
listB.
listC([]).
listC([]) :- listB.
listC(.(T68, T70)) :- listC(T70).
goalD(0) :- listB.
goalD(s(T15)) :- s2lA(T15, X31).
goalD(s(T15)) :- ','(s2lA(T15, T48), listC(T48)).

Query: goalD(g)

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [TOCL09]. With regard to the inferred argument filtering the predicates were used in the following modes:
goalD_in: (b)
s2lA_in: (b,f)
listC_in: (b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

goalD_in_g(0) → U4_g(listB_in_)
listB_in_ → listB_out_
U4_g(listB_out_) → goalD_out_g(0)
goalD_in_g(s(T15)) → U5_g(T15, s2lA_in_ga(T15, X31))
s2lA_in_ga(0, []) → s2lA_out_ga(0, [])
s2lA_in_ga(s(T28), .(X56, X57)) → U1_ga(T28, X56, X57, s2lA_in_ga(T28, X57))
U1_ga(T28, X56, X57, s2lA_out_ga(T28, X57)) → s2lA_out_ga(s(T28), .(X56, X57))
U5_g(T15, s2lA_out_ga(T15, X31)) → goalD_out_g(s(T15))
goalD_in_g(s(T15)) → U6_g(T15, s2lA_in_ga(T15, T48))
U6_g(T15, s2lA_out_ga(T15, T48)) → U7_g(T15, listC_in_g(T48))
listC_in_g([]) → listC_out_g([])
listC_in_g([]) → U2_g(listB_in_)
U2_g(listB_out_) → listC_out_g([])
listC_in_g(.(T68, T70)) → U3_g(T68, T70, listC_in_g(T70))
U3_g(T68, T70, listC_out_g(T70)) → listC_out_g(.(T68, T70))
U7_g(T15, listC_out_g(T48)) → goalD_out_g(s(T15))

The argument filtering Pi contains the following mapping:
goalD_in_g(x1)  =  goalD_in_g(x1)
0  =  0
U4_g(x1)  =  U4_g(x1)
listB_in_  =  listB_in_
listB_out_  =  listB_out_
goalD_out_g(x1)  =  goalD_out_g
s(x1)  =  s(x1)
U5_g(x1, x2)  =  U5_g(x2)
s2lA_in_ga(x1, x2)  =  s2lA_in_ga(x1)
s2lA_out_ga(x1, x2)  =  s2lA_out_ga(x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
.(x1, x2)  =  .(x2)
U6_g(x1, x2)  =  U6_g(x2)
U7_g(x1, x2)  =  U7_g(x2)
listC_in_g(x1)  =  listC_in_g(x1)
[]  =  []
listC_out_g(x1)  =  listC_out_g
U2_g(x1)  =  U2_g(x1)
U3_g(x1, x2, x3)  =  U3_g(x3)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

goalD_in_g(0) → U4_g(listB_in_)
listB_in_ → listB_out_
U4_g(listB_out_) → goalD_out_g(0)
goalD_in_g(s(T15)) → U5_g(T15, s2lA_in_ga(T15, X31))
s2lA_in_ga(0, []) → s2lA_out_ga(0, [])
s2lA_in_ga(s(T28), .(X56, X57)) → U1_ga(T28, X56, X57, s2lA_in_ga(T28, X57))
U1_ga(T28, X56, X57, s2lA_out_ga(T28, X57)) → s2lA_out_ga(s(T28), .(X56, X57))
U5_g(T15, s2lA_out_ga(T15, X31)) → goalD_out_g(s(T15))
goalD_in_g(s(T15)) → U6_g(T15, s2lA_in_ga(T15, T48))
U6_g(T15, s2lA_out_ga(T15, T48)) → U7_g(T15, listC_in_g(T48))
listC_in_g([]) → listC_out_g([])
listC_in_g([]) → U2_g(listB_in_)
U2_g(listB_out_) → listC_out_g([])
listC_in_g(.(T68, T70)) → U3_g(T68, T70, listC_in_g(T70))
U3_g(T68, T70, listC_out_g(T70)) → listC_out_g(.(T68, T70))
U7_g(T15, listC_out_g(T48)) → goalD_out_g(s(T15))

The argument filtering Pi contains the following mapping:
goalD_in_g(x1)  =  goalD_in_g(x1)
0  =  0
U4_g(x1)  =  U4_g(x1)
listB_in_  =  listB_in_
listB_out_  =  listB_out_
goalD_out_g(x1)  =  goalD_out_g
s(x1)  =  s(x1)
U5_g(x1, x2)  =  U5_g(x2)
s2lA_in_ga(x1, x2)  =  s2lA_in_ga(x1)
s2lA_out_ga(x1, x2)  =  s2lA_out_ga(x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
.(x1, x2)  =  .(x2)
U6_g(x1, x2)  =  U6_g(x2)
U7_g(x1, x2)  =  U7_g(x2)
listC_in_g(x1)  =  listC_in_g(x1)
[]  =  []
listC_out_g(x1)  =  listC_out_g
U2_g(x1)  =  U2_g(x1)
U3_g(x1, x2, x3)  =  U3_g(x3)

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

GOALD_IN_G(0) → U4_G(listB_in_)
GOALD_IN_G(0) → LISTB_IN_
GOALD_IN_G(s(T15)) → U5_G(T15, s2lA_in_ga(T15, X31))
GOALD_IN_G(s(T15)) → S2LA_IN_GA(T15, X31)
S2LA_IN_GA(s(T28), .(X56, X57)) → U1_GA(T28, X56, X57, s2lA_in_ga(T28, X57))
S2LA_IN_GA(s(T28), .(X56, X57)) → S2LA_IN_GA(T28, X57)
GOALD_IN_G(s(T15)) → U6_G(T15, s2lA_in_ga(T15, T48))
U6_G(T15, s2lA_out_ga(T15, T48)) → U7_G(T15, listC_in_g(T48))
U6_G(T15, s2lA_out_ga(T15, T48)) → LISTC_IN_G(T48)
LISTC_IN_G([]) → U2_G(listB_in_)
LISTC_IN_G([]) → LISTB_IN_
LISTC_IN_G(.(T68, T70)) → U3_G(T68, T70, listC_in_g(T70))
LISTC_IN_G(.(T68, T70)) → LISTC_IN_G(T70)

The TRS R consists of the following rules:

goalD_in_g(0) → U4_g(listB_in_)
listB_in_ → listB_out_
U4_g(listB_out_) → goalD_out_g(0)
goalD_in_g(s(T15)) → U5_g(T15, s2lA_in_ga(T15, X31))
s2lA_in_ga(0, []) → s2lA_out_ga(0, [])
s2lA_in_ga(s(T28), .(X56, X57)) → U1_ga(T28, X56, X57, s2lA_in_ga(T28, X57))
U1_ga(T28, X56, X57, s2lA_out_ga(T28, X57)) → s2lA_out_ga(s(T28), .(X56, X57))
U5_g(T15, s2lA_out_ga(T15, X31)) → goalD_out_g(s(T15))
goalD_in_g(s(T15)) → U6_g(T15, s2lA_in_ga(T15, T48))
U6_g(T15, s2lA_out_ga(T15, T48)) → U7_g(T15, listC_in_g(T48))
listC_in_g([]) → listC_out_g([])
listC_in_g([]) → U2_g(listB_in_)
U2_g(listB_out_) → listC_out_g([])
listC_in_g(.(T68, T70)) → U3_g(T68, T70, listC_in_g(T70))
U3_g(T68, T70, listC_out_g(T70)) → listC_out_g(.(T68, T70))
U7_g(T15, listC_out_g(T48)) → goalD_out_g(s(T15))

The argument filtering Pi contains the following mapping:
goalD_in_g(x1)  =  goalD_in_g(x1)
0  =  0
U4_g(x1)  =  U4_g(x1)
listB_in_  =  listB_in_
listB_out_  =  listB_out_
goalD_out_g(x1)  =  goalD_out_g
s(x1)  =  s(x1)
U5_g(x1, x2)  =  U5_g(x2)
s2lA_in_ga(x1, x2)  =  s2lA_in_ga(x1)
s2lA_out_ga(x1, x2)  =  s2lA_out_ga(x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
.(x1, x2)  =  .(x2)
U6_g(x1, x2)  =  U6_g(x2)
U7_g(x1, x2)  =  U7_g(x2)
listC_in_g(x1)  =  listC_in_g(x1)
[]  =  []
listC_out_g(x1)  =  listC_out_g
U2_g(x1)  =  U2_g(x1)
U3_g(x1, x2, x3)  =  U3_g(x3)
GOALD_IN_G(x1)  =  GOALD_IN_G(x1)
U4_G(x1)  =  U4_G(x1)
LISTB_IN_  =  LISTB_IN_
U5_G(x1, x2)  =  U5_G(x2)
S2LA_IN_GA(x1, x2)  =  S2LA_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x4)
U6_G(x1, x2)  =  U6_G(x2)
U7_G(x1, x2)  =  U7_G(x2)
LISTC_IN_G(x1)  =  LISTC_IN_G(x1)
U2_G(x1)  =  U2_G(x1)
U3_G(x1, x2, x3)  =  U3_G(x3)

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

(6) Obligation:

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

GOALD_IN_G(0) → U4_G(listB_in_)
GOALD_IN_G(0) → LISTB_IN_
GOALD_IN_G(s(T15)) → U5_G(T15, s2lA_in_ga(T15, X31))
GOALD_IN_G(s(T15)) → S2LA_IN_GA(T15, X31)
S2LA_IN_GA(s(T28), .(X56, X57)) → U1_GA(T28, X56, X57, s2lA_in_ga(T28, X57))
S2LA_IN_GA(s(T28), .(X56, X57)) → S2LA_IN_GA(T28, X57)
GOALD_IN_G(s(T15)) → U6_G(T15, s2lA_in_ga(T15, T48))
U6_G(T15, s2lA_out_ga(T15, T48)) → U7_G(T15, listC_in_g(T48))
U6_G(T15, s2lA_out_ga(T15, T48)) → LISTC_IN_G(T48)
LISTC_IN_G([]) → U2_G(listB_in_)
LISTC_IN_G([]) → LISTB_IN_
LISTC_IN_G(.(T68, T70)) → U3_G(T68, T70, listC_in_g(T70))
LISTC_IN_G(.(T68, T70)) → LISTC_IN_G(T70)

The TRS R consists of the following rules:

goalD_in_g(0) → U4_g(listB_in_)
listB_in_ → listB_out_
U4_g(listB_out_) → goalD_out_g(0)
goalD_in_g(s(T15)) → U5_g(T15, s2lA_in_ga(T15, X31))
s2lA_in_ga(0, []) → s2lA_out_ga(0, [])
s2lA_in_ga(s(T28), .(X56, X57)) → U1_ga(T28, X56, X57, s2lA_in_ga(T28, X57))
U1_ga(T28, X56, X57, s2lA_out_ga(T28, X57)) → s2lA_out_ga(s(T28), .(X56, X57))
U5_g(T15, s2lA_out_ga(T15, X31)) → goalD_out_g(s(T15))
goalD_in_g(s(T15)) → U6_g(T15, s2lA_in_ga(T15, T48))
U6_g(T15, s2lA_out_ga(T15, T48)) → U7_g(T15, listC_in_g(T48))
listC_in_g([]) → listC_out_g([])
listC_in_g([]) → U2_g(listB_in_)
U2_g(listB_out_) → listC_out_g([])
listC_in_g(.(T68, T70)) → U3_g(T68, T70, listC_in_g(T70))
U3_g(T68, T70, listC_out_g(T70)) → listC_out_g(.(T68, T70))
U7_g(T15, listC_out_g(T48)) → goalD_out_g(s(T15))

The argument filtering Pi contains the following mapping:
goalD_in_g(x1)  =  goalD_in_g(x1)
0  =  0
U4_g(x1)  =  U4_g(x1)
listB_in_  =  listB_in_
listB_out_  =  listB_out_
goalD_out_g(x1)  =  goalD_out_g
s(x1)  =  s(x1)
U5_g(x1, x2)  =  U5_g(x2)
s2lA_in_ga(x1, x2)  =  s2lA_in_ga(x1)
s2lA_out_ga(x1, x2)  =  s2lA_out_ga(x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
.(x1, x2)  =  .(x2)
U6_g(x1, x2)  =  U6_g(x2)
U7_g(x1, x2)  =  U7_g(x2)
listC_in_g(x1)  =  listC_in_g(x1)
[]  =  []
listC_out_g(x1)  =  listC_out_g
U2_g(x1)  =  U2_g(x1)
U3_g(x1, x2, x3)  =  U3_g(x3)
GOALD_IN_G(x1)  =  GOALD_IN_G(x1)
U4_G(x1)  =  U4_G(x1)
LISTB_IN_  =  LISTB_IN_
U5_G(x1, x2)  =  U5_G(x2)
S2LA_IN_GA(x1, x2)  =  S2LA_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x4)
U6_G(x1, x2)  =  U6_G(x2)
U7_G(x1, x2)  =  U7_G(x2)
LISTC_IN_G(x1)  =  LISTC_IN_G(x1)
U2_G(x1)  =  U2_G(x1)
U3_G(x1, x2, x3)  =  U3_G(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 11 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

LISTC_IN_G(.(T68, T70)) → LISTC_IN_G(T70)

The TRS R consists of the following rules:

goalD_in_g(0) → U4_g(listB_in_)
listB_in_ → listB_out_
U4_g(listB_out_) → goalD_out_g(0)
goalD_in_g(s(T15)) → U5_g(T15, s2lA_in_ga(T15, X31))
s2lA_in_ga(0, []) → s2lA_out_ga(0, [])
s2lA_in_ga(s(T28), .(X56, X57)) → U1_ga(T28, X56, X57, s2lA_in_ga(T28, X57))
U1_ga(T28, X56, X57, s2lA_out_ga(T28, X57)) → s2lA_out_ga(s(T28), .(X56, X57))
U5_g(T15, s2lA_out_ga(T15, X31)) → goalD_out_g(s(T15))
goalD_in_g(s(T15)) → U6_g(T15, s2lA_in_ga(T15, T48))
U6_g(T15, s2lA_out_ga(T15, T48)) → U7_g(T15, listC_in_g(T48))
listC_in_g([]) → listC_out_g([])
listC_in_g([]) → U2_g(listB_in_)
U2_g(listB_out_) → listC_out_g([])
listC_in_g(.(T68, T70)) → U3_g(T68, T70, listC_in_g(T70))
U3_g(T68, T70, listC_out_g(T70)) → listC_out_g(.(T68, T70))
U7_g(T15, listC_out_g(T48)) → goalD_out_g(s(T15))

The argument filtering Pi contains the following mapping:
goalD_in_g(x1)  =  goalD_in_g(x1)
0  =  0
U4_g(x1)  =  U4_g(x1)
listB_in_  =  listB_in_
listB_out_  =  listB_out_
goalD_out_g(x1)  =  goalD_out_g
s(x1)  =  s(x1)
U5_g(x1, x2)  =  U5_g(x2)
s2lA_in_ga(x1, x2)  =  s2lA_in_ga(x1)
s2lA_out_ga(x1, x2)  =  s2lA_out_ga(x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
.(x1, x2)  =  .(x2)
U6_g(x1, x2)  =  U6_g(x2)
U7_g(x1, x2)  =  U7_g(x2)
listC_in_g(x1)  =  listC_in_g(x1)
[]  =  []
listC_out_g(x1)  =  listC_out_g
U2_g(x1)  =  U2_g(x1)
U3_g(x1, x2, x3)  =  U3_g(x3)
LISTC_IN_G(x1)  =  LISTC_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:

LISTC_IN_G(.(T68, T70)) → LISTC_IN_G(T70)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
LISTC_IN_G(x1)  =  LISTC_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:

LISTC_IN_G(.(T70)) → LISTC_IN_G(T70)

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:

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

(15) YES

(16) Obligation:

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

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

The TRS R consists of the following rules:

goalD_in_g(0) → U4_g(listB_in_)
listB_in_ → listB_out_
U4_g(listB_out_) → goalD_out_g(0)
goalD_in_g(s(T15)) → U5_g(T15, s2lA_in_ga(T15, X31))
s2lA_in_ga(0, []) → s2lA_out_ga(0, [])
s2lA_in_ga(s(T28), .(X56, X57)) → U1_ga(T28, X56, X57, s2lA_in_ga(T28, X57))
U1_ga(T28, X56, X57, s2lA_out_ga(T28, X57)) → s2lA_out_ga(s(T28), .(X56, X57))
U5_g(T15, s2lA_out_ga(T15, X31)) → goalD_out_g(s(T15))
goalD_in_g(s(T15)) → U6_g(T15, s2lA_in_ga(T15, T48))
U6_g(T15, s2lA_out_ga(T15, T48)) → U7_g(T15, listC_in_g(T48))
listC_in_g([]) → listC_out_g([])
listC_in_g([]) → U2_g(listB_in_)
U2_g(listB_out_) → listC_out_g([])
listC_in_g(.(T68, T70)) → U3_g(T68, T70, listC_in_g(T70))
U3_g(T68, T70, listC_out_g(T70)) → listC_out_g(.(T68, T70))
U7_g(T15, listC_out_g(T48)) → goalD_out_g(s(T15))

The argument filtering Pi contains the following mapping:
goalD_in_g(x1)  =  goalD_in_g(x1)
0  =  0
U4_g(x1)  =  U4_g(x1)
listB_in_  =  listB_in_
listB_out_  =  listB_out_
goalD_out_g(x1)  =  goalD_out_g
s(x1)  =  s(x1)
U5_g(x1, x2)  =  U5_g(x2)
s2lA_in_ga(x1, x2)  =  s2lA_in_ga(x1)
s2lA_out_ga(x1, x2)  =  s2lA_out_ga(x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
.(x1, x2)  =  .(x2)
U6_g(x1, x2)  =  U6_g(x2)
U7_g(x1, x2)  =  U7_g(x2)
listC_in_g(x1)  =  listC_in_g(x1)
[]  =  []
listC_out_g(x1)  =  listC_out_g
U2_g(x1)  =  U2_g(x1)
U3_g(x1, x2, x3)  =  U3_g(x3)
S2LA_IN_GA(x1, x2)  =  S2LA_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:

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

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
S2LA_IN_GA(x1, x2)  =  S2LA_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:

S2LA_IN_GA(s(T28)) → S2LA_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:

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

(22) YES