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) :- ','(tail(X, T), list(T)).
s2l(0, L) :- ','(!, eq(L, [])).
s2l(X, .(X1, Xs)) :- ','(p(X, P), s2l(P, Xs)).
tail([], []).
tail(.(X2, Xs), Xs).
p(0, 0).
p(s(X), X).
eq(X, X).

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];
8 [label="8: ','(s2l(T3, X5), list(X5))\n\nT3 is ground\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(s2l(T3, X5), list(X5)), SCOPE: 2, CLAUSE: 3 | ','(s2l(T3, X5), list(X5)), SCOPE: 2, CLAUSE: 4\n\nT3 is ground\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(','(!_2, eq(X11, [])), list(X11)) | ','(s2l(0, X5), list(X5)), SCOPE: 2, CLAUSE: 4\n\nX5 is free\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(s2l(T3, X5), list(X5)), SCOPE: 2, CLAUSE: 4\n\nT3 is ground\nX5 is free\nX10 is free\ns2l(T3, X5) !=? s2l(0, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(eq(X11, []), list(X11))\n\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(eq(X11, []), list(X11)), SCOPE: 3, CLAUSE: 9\n\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="B: list([])\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: list([]), SCOPE: 4, CLAUSE: 1 | list([]), SCOPE: 4, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: !_4 | list([]), SCOPE: 4, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(','(p(T6, X34), s2l(X34, X36)), list(.(X35, X36)))\n\nT6 is ground\nX5 is free\nX10 is free\nX35 is free\nX36 is free\nX34 is free\ns2l(T6, X5) !=? s2l(0, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(','(p(T6, X34), s2l(X34, X36)), list(.(X35, X36))), SCOPE: 5, CLAUSE: 7 | ','(','(p(T6, X34), s2l(X34, X36)), list(.(X35, X36))), SCOPE: 5, CLAUSE: 8\n\nT6 is ground\nX5 is free\nX10 is free\nX35 is free\nX36 is free\nX34 is free\ns2l(T6, X5) !=? s2l(0, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ','(','(p(T6, X34), s2l(X34, X36)), list(.(X35, X36))), SCOPE: 5, CLAUSE: 8\n\nT6 is ground\nX5 is free\nX10 is free\nX35 is free\nX36 is free\nX34 is free\ns2l(T6, X5) !=? s2l(0, X10)", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="C: ','(s2l(T9, X36), list(.(X35, X36)))\n\nT9 is ground\nX35 is free\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="D: s2l(T9, X36)\n\nT9 is ground\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="F: list(.(X35, T10))\n\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: s2l(T9, X36), SCOPE: 6, CLAUSE: 3 | s2l(T9, X36), SCOPE: 6, CLAUSE: 4\n\nT9 is ground\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(!_6, eq(X51, [])) | s2l(0, X36), SCOPE: 6, CLAUSE: 4\n\nX36 is free\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: s2l(T9, X36), SCOPE: 6, CLAUSE: 4\n\nT9 is ground\nX36 is free\nX50 is free\ns2l(T9, X36) !=? s2l(0, X50)", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: eq(X51, [])\n\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: eq(X51, []), SCOPE: 7, CLAUSE: 9\n\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: ','(p(T13, X74), s2l(X74, X76))\n\nT13 is ground\nX36 is free\nX50 is free\nX76 is free\nX74 is free\ns2l(T13, X36) !=? s2l(0, X50)", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: ','(p(T13, X74), s2l(X74, X76)), SCOPE: 8, CLAUSE: 7 | ','(p(T13, X74), s2l(X74, X76)), SCOPE: 8, CLAUSE: 8\n\nT13 is ground\nX36 is free\nX50 is free\nX76 is free\nX74 is free\ns2l(T13, X36) !=? s2l(0, X50)", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: ','(p(T13, X74), s2l(X74, X76)), SCOPE: 8, CLAUSE: 8\n\nT13 is ground\nX36 is free\nX50 is free\nX76 is free\nX74 is free\ns2l(T13, X36) !=? s2l(0, X50)", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: s2l(T16, X76)\n\nT16 is ground\nX76 is free", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: list(.(X35, T10)), SCOPE: 9, CLAUSE: 1 | list(.(X35, T10)), SCOPE: 9, CLAUSE: 2\n\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: list(.(X35, T10)), SCOPE: 9, CLAUSE: 2\n\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(tail(.(X91, T21), X90), list(X90))\n\nX91 is free\nX90 is free", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: ','(tail(.(X91, T21), X90), list(X90)), SCOPE: 10, CLAUSE: 5 | ','(tail(.(X91, T21), X90), list(X90)), SCOPE: 10, CLAUSE: 6\n\nX91 is free\nX90 is free", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: ','(tail(.(X91, T21), X90), list(X90)), SCOPE: 10, CLAUSE: 6\n\nX91 is free\nX90 is free", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="E: list(T26)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: list(T26), SCOPE: 11, CLAUSE: 1 | list(T26), SCOPE: 11, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: !_11 | list(T26), SCOPE: 11, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: list(T26), SCOPE: 11, CLAUSE: 2\n\nlist(T26) !=? list([])", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: ','(tail(T31, X105), list(X105))\n\nX105 is free", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: ','(tail(T31, X105), list(X105)), SCOPE: 12, CLAUSE: 5 | ','(tail(T31, X105), list(X105)), SCOPE: 12, CLAUSE: 6\n\nX105 is free", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: ','(tail(T31, X105), list(X105)), SCOPE: 12, CLAUSE: 5\n\nX105 is free", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: ','(tail(T31, X105), list(X105)), SCOPE: 12, CLAUSE: 6\n\nX105 is free", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: list([])\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: list(T38)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 114 [arrowhead = none ];
114 -> 4;

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

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

117 [label="EVAL with clause\ns2l(0, X10) :- ','(!_2, eq(X10, [])).\nand substitutionT3 -> 0,\nX5 -> X11,\nX10 -> X11", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 117 [arrowhead = none ];
117 -> 12;

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

119 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
12 -> 119 [arrowhead = none ];
119 -> 16;

120 [label="ONLY EVAL with clause\ns2l(X31, .(X32, X33)) :- ','(p(X31, X34), s2l(X34, X33)).\nand substitutionT3 -> T6,\nX31 -> T6,\nX32 -> X35,\nX33 -> X36,\nX5 -> .(X35, X36)", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 120 [arrowhead = none ];
120 -> 39;

121 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
16 -> 121 [arrowhead = none ];
121 -> 19;

122 [label="ONLY EVAL with clause\neq(X16, X16).\nand substitutionX11 -> [],\nX16 -> [],\nX17 -> []", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 122 [arrowhead = none ];
122 -> 22;

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

124 [label="ONLY EVAL with clause\nlist([]) :- !_4.\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 124 [arrowhead = none ];
124 -> 26;

125 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
26 -> 125 [arrowhead = none ];
125 -> 27;

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

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

128 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (s2l(T6, X5), s2l(0, X10))", fontsize=14, style = filled, fillcolor = lightgreen];
41 -> 128 [arrowhead = none ];
128 -> 42;

129 [label="EVAL with clause\np(s(X41), X41).\nand substitutionX41 -> T9,\nT6 -> s(T9),\nX34 -> T9", fontsize=14, style = filled, fillcolor = lightblue];
42 -> 129 [arrowhead = none ];
129 -> 45;

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

131 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
45 -> 131 [arrowhead = none ];
131 -> 52;

132 [label="SPLIT 2\nnew knowledge:\nT9 is ground\nreplacements:X36 -> T10", fontsize=14, style = filled, fillcolor = violet];
45 -> 132 [arrowhead = none ];
132 -> 53;

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

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

135 [label="EVAL with clause\ns2l(0, X50) :- ','(!_6, eq(X50, [])).\nand substitutionT9 -> 0,\nX36 -> X51,\nX50 -> X51", fontsize=14, style = filled, fillcolor = lightblue];
56 -> 135 [arrowhead = none ];
135 -> 57;

136 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
56 -> 136 [arrowhead = none ];
136 -> 58;

137 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
57 -> 137 [arrowhead = none ];
137 -> 59;

138 [label="ONLY EVAL with clause\ns2l(X71, .(X72, X73)) :- ','(p(X71, X74), s2l(X74, X73)).\nand substitutionT9 -> T13,\nX71 -> T13,\nX72 -> X75,\nX73 -> X76,\nX36 -> .(X75, X76)", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 138 [arrowhead = none ];
138 -> 89;

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

140 [label="ONLY EVAL with clause\neq(X56, X56).\nand substitutionX51 -> [],\nX56 -> [],\nX57 -> []", fontsize=14, style = filled, fillcolor = lightblue];
60 -> 140 [arrowhead = none ];
140 -> 64;

141 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
64 -> 141 [arrowhead = none ];
141 -> 65;

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

143 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (s2l(T13, X36), s2l(0, X50))", fontsize=14, style = filled, fillcolor = lightgreen];
90 -> 143 [arrowhead = none ];
143 -> 91;

144 [label="EVAL with clause\np(s(X81), X81).\nand substitutionX81 -> T16,\nT13 -> s(T16),\nX74 -> T16", fontsize=14, style = filled, fillcolor = lightblue];
91 -> 144 [arrowhead = none ];
144 -> 92;

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

146 [label="INSTANCE with matching:\nT9 -> T16\nX36 -> X76", fontsize=14, style = filled, fillcolor = lightgrey];
92 -> 146 [arrowhead = none , style=dashed];
146 -> 52[style=dashed];

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

148 [label="ONLY EVAL with clause\nlist(X89) :- ','(tail(X89, X90), list(X90)).\nand substitutionX35 -> X91,\nT10 -> T21,\nX89 -> .(X91, T21),\nT20 -> T21", fontsize=14, style = filled, fillcolor = lightblue];
95 -> 148 [arrowhead = none ];
148 -> 96;

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

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

151 [label="ONLY EVAL with clause\ntail(.(X98, X99), X99).\nand substitutionX91 -> X100,\nX98 -> X100,\nT21 -> T26,\nX99 -> T26,\nX90 -> T26,\nT25 -> T26", fontsize=14, style = filled, fillcolor = lightblue];
98 -> 151 [arrowhead = none ];
151 -> 100;

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

153 [label="EVAL with clause\nlist([]) :- !_11.\nand substitutionT26 -> []", fontsize=14, style = filled, fillcolor = lightblue];
101 -> 153 [arrowhead = none ];
153 -> 102;

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

155 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
102 -> 155 [arrowhead = none ];
155 -> 104;

156 [label="ONLY EVAL with clause\nlist(X104) :- ','(tail(X104, X105), list(X105)).\nand substitutionT26 -> T31,\nX104 -> T31,\nT30 -> T31", fontsize=14, style = filled, fillcolor = lightblue];
103 -> 156 [arrowhead = none ];
156 -> 106;

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

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

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

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

161 [label="EVAL with clause\ntail([], []).\nand substitutionT31 -> [],\nX105 -> []", fontsize=14, style = filled, fillcolor = lightblue];
108 -> 161 [arrowhead = none ];
161 -> 110;

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

163 [label="EVAL with clause\ntail(.(X110, X111), X111).\nand substitutionX110 -> T36,\nX111 -> T38,\nT31 -> .(T36, T38),\nX105 -> T38,\nT37 -> T38", fontsize=14, style = filled, fillcolor = lightblue];
109 -> 163 [arrowhead = none ];
163 -> 112;

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

165 [label="INSTANCE", fontsize=14, style = filled, fillcolor = lightgrey];
110 -> 165 [arrowhead = none , style=dashed];
165 -> 22[style=dashed];

166 [label="INSTANCE with matching:\nT26 -> T38", fontsize=14, style = filled, fillcolor = lightgrey];
112 -> 166 [arrowhead = none , style=dashed];
166 -> 100[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(T9)) → U2_g(T9, pC_in_gaa(T9, X36, X35))
pC_in_gaa(T9, T10, X35) → U7_gaa(T9, T10, X35, s2lD_in_ga(T9, T10))
s2lD_in_ga(0, []) → s2lD_out_ga(0, [])
s2lD_in_ga(s(T16), .(X75, X76)) → U3_ga(T16, X75, X76, s2lD_in_ga(T16, X76))
U3_ga(T16, X75, X76, s2lD_out_ga(T16, X76)) → s2lD_out_ga(s(T16), .(X75, X76))
U7_gaa(T9, T10, X35, s2lD_out_ga(T9, T10)) → U8_gaa(T9, T10, X35, listF_in_ag(X35, T10))
listF_in_ag(X100, T26) → U6_ag(X100, T26, listE_in_g(T26))
listE_in_g([]) → listE_out_g([])
listE_in_g([]) → U4_g(listB_in_)
U4_g(listB_out_) → listE_out_g([])
listE_in_g(.(T36, T38)) → U5_g(T36, T38, listE_in_g(T38))
U5_g(T36, T38, listE_out_g(T38)) → listE_out_g(.(T36, T38))
U6_ag(X100, T26, listE_out_g(T26)) → listF_out_ag(X100, T26)
U8_gaa(T9, T10, X35, listF_out_ag(X35, T10)) → pC_out_gaa(T9, T10, X35)
U2_g(T9, pC_out_gaa(T9, X36, X35)) → goalA_out_g(s(T9))

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(T9)) → U2_G(T9, pC_in_gaa(T9, X36, X35))
GOALA_IN_G(s(T9)) → PC_IN_GAA(T9, X36, X35)
PC_IN_GAA(T9, T10, X35) → U7_GAA(T9, T10, X35, s2lD_in_ga(T9, T10))
PC_IN_GAA(T9, T10, X35) → S2LD_IN_GA(T9, T10)
S2LD_IN_GA(s(T16), .(X75, X76)) → U3_GA(T16, X75, X76, s2lD_in_ga(T16, X76))
S2LD_IN_GA(s(T16), .(X75, X76)) → S2LD_IN_GA(T16, X76)
U7_GAA(T9, T10, X35, s2lD_out_ga(T9, T10)) → U8_GAA(T9, T10, X35, listF_in_ag(X35, T10))
U7_GAA(T9, T10, X35, s2lD_out_ga(T9, T10)) → LISTF_IN_AG(X35, T10)
LISTF_IN_AG(X100, T26) → U6_AG(X100, T26, listE_in_g(T26))
LISTF_IN_AG(X100, T26) → LISTE_IN_G(T26)
LISTE_IN_G([]) → U4_G(listB_in_)
LISTE_IN_G([]) → LISTB_IN_
LISTE_IN_G(.(T36, T38)) → U5_G(T36, T38, listE_in_g(T38))
LISTE_IN_G(.(T36, T38)) → LISTE_IN_G(T38)

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(T9)) → U2_g(T9, pC_in_gaa(T9, X36, X35))
pC_in_gaa(T9, T10, X35) → U7_gaa(T9, T10, X35, s2lD_in_ga(T9, T10))
s2lD_in_ga(0, []) → s2lD_out_ga(0, [])
s2lD_in_ga(s(T16), .(X75, X76)) → U3_ga(T16, X75, X76, s2lD_in_ga(T16, X76))
U3_ga(T16, X75, X76, s2lD_out_ga(T16, X76)) → s2lD_out_ga(s(T16), .(X75, X76))
U7_gaa(T9, T10, X35, s2lD_out_ga(T9, T10)) → U8_gaa(T9, T10, X35, listF_in_ag(X35, T10))
listF_in_ag(X100, T26) → U6_ag(X100, T26, listE_in_g(T26))
listE_in_g([]) → listE_out_g([])
listE_in_g([]) → U4_g(listB_in_)
U4_g(listB_out_) → listE_out_g([])
listE_in_g(.(T36, T38)) → U5_g(T36, T38, listE_in_g(T38))
U5_g(T36, T38, listE_out_g(T38)) → listE_out_g(.(T36, T38))
U6_ag(X100, T26, listE_out_g(T26)) → listF_out_ag(X100, T26)
U8_gaa(T9, T10, X35, listF_out_ag(X35, T10)) → pC_out_gaa(T9, T10, X35)
U2_g(T9, pC_out_gaa(T9, X36, X35)) → goalA_out_g(s(T9))

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(T9)) → U2_G(T9, pC_in_gaa(T9, X36, X35))
GOALA_IN_G(s(T9)) → PC_IN_GAA(T9, X36, X35)
PC_IN_GAA(T9, T10, X35) → U7_GAA(T9, T10, X35, s2lD_in_ga(T9, T10))
PC_IN_GAA(T9, T10, X35) → S2LD_IN_GA(T9, T10)
S2LD_IN_GA(s(T16), .(X75, X76)) → U3_GA(T16, X75, X76, s2lD_in_ga(T16, X76))
S2LD_IN_GA(s(T16), .(X75, X76)) → S2LD_IN_GA(T16, X76)
U7_GAA(T9, T10, X35, s2lD_out_ga(T9, T10)) → U8_GAA(T9, T10, X35, listF_in_ag(X35, T10))
U7_GAA(T9, T10, X35, s2lD_out_ga(T9, T10)) → LISTF_IN_AG(X35, T10)
LISTF_IN_AG(X100, T26) → U6_AG(X100, T26, listE_in_g(T26))
LISTF_IN_AG(X100, T26) → LISTE_IN_G(T26)
LISTE_IN_G([]) → U4_G(listB_in_)
LISTE_IN_G([]) → LISTB_IN_
LISTE_IN_G(.(T36, T38)) → U5_G(T36, T38, listE_in_g(T38))
LISTE_IN_G(.(T36, T38)) → LISTE_IN_G(T38)

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(T9)) → U2_g(T9, pC_in_gaa(T9, X36, X35))
pC_in_gaa(T9, T10, X35) → U7_gaa(T9, T10, X35, s2lD_in_ga(T9, T10))
s2lD_in_ga(0, []) → s2lD_out_ga(0, [])
s2lD_in_ga(s(T16), .(X75, X76)) → U3_ga(T16, X75, X76, s2lD_in_ga(T16, X76))
U3_ga(T16, X75, X76, s2lD_out_ga(T16, X76)) → s2lD_out_ga(s(T16), .(X75, X76))
U7_gaa(T9, T10, X35, s2lD_out_ga(T9, T10)) → U8_gaa(T9, T10, X35, listF_in_ag(X35, T10))
listF_in_ag(X100, T26) → U6_ag(X100, T26, listE_in_g(T26))
listE_in_g([]) → listE_out_g([])
listE_in_g([]) → U4_g(listB_in_)
U4_g(listB_out_) → listE_out_g([])
listE_in_g(.(T36, T38)) → U5_g(T36, T38, listE_in_g(T38))
U5_g(T36, T38, listE_out_g(T38)) → listE_out_g(.(T36, T38))
U6_ag(X100, T26, listE_out_g(T26)) → listF_out_ag(X100, T26)
U8_gaa(T9, T10, X35, listF_out_ag(X35, T10)) → pC_out_gaa(T9, T10, X35)
U2_g(T9, pC_out_gaa(T9, X36, X35)) → goalA_out_g(s(T9))

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(.(T36, T38)) → LISTE_IN_G(T38)

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(T9)) → U2_g(T9, pC_in_gaa(T9, X36, X35))
pC_in_gaa(T9, T10, X35) → U7_gaa(T9, T10, X35, s2lD_in_ga(T9, T10))
s2lD_in_ga(0, []) → s2lD_out_ga(0, [])
s2lD_in_ga(s(T16), .(X75, X76)) → U3_ga(T16, X75, X76, s2lD_in_ga(T16, X76))
U3_ga(T16, X75, X76, s2lD_out_ga(T16, X76)) → s2lD_out_ga(s(T16), .(X75, X76))
U7_gaa(T9, T10, X35, s2lD_out_ga(T9, T10)) → U8_gaa(T9, T10, X35, listF_in_ag(X35, T10))
listF_in_ag(X100, T26) → U6_ag(X100, T26, listE_in_g(T26))
listE_in_g([]) → listE_out_g([])
listE_in_g([]) → U4_g(listB_in_)
U4_g(listB_out_) → listE_out_g([])
listE_in_g(.(T36, T38)) → U5_g(T36, T38, listE_in_g(T38))
U5_g(T36, T38, listE_out_g(T38)) → listE_out_g(.(T36, T38))
U6_ag(X100, T26, listE_out_g(T26)) → listF_out_ag(X100, T26)
U8_gaa(T9, T10, X35, listF_out_ag(X35, T10)) → pC_out_gaa(T9, T10, X35)
U2_g(T9, pC_out_gaa(T9, X36, X35)) → goalA_out_g(s(T9))

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(.(T36, T38)) → LISTE_IN_G(T38)

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(.(T38)) → LISTE_IN_G(T38)

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(.(T38)) → LISTE_IN_G(T38)
  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(T16), .(X75, X76)) → S2LD_IN_GA(T16, X76)

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(T9)) → U2_g(T9, pC_in_gaa(T9, X36, X35))
pC_in_gaa(T9, T10, X35) → U7_gaa(T9, T10, X35, s2lD_in_ga(T9, T10))
s2lD_in_ga(0, []) → s2lD_out_ga(0, [])
s2lD_in_ga(s(T16), .(X75, X76)) → U3_ga(T16, X75, X76, s2lD_in_ga(T16, X76))
U3_ga(T16, X75, X76, s2lD_out_ga(T16, X76)) → s2lD_out_ga(s(T16), .(X75, X76))
U7_gaa(T9, T10, X35, s2lD_out_ga(T9, T10)) → U8_gaa(T9, T10, X35, listF_in_ag(X35, T10))
listF_in_ag(X100, T26) → U6_ag(X100, T26, listE_in_g(T26))
listE_in_g([]) → listE_out_g([])
listE_in_g([]) → U4_g(listB_in_)
U4_g(listB_out_) → listE_out_g([])
listE_in_g(.(T36, T38)) → U5_g(T36, T38, listE_in_g(T38))
U5_g(T36, T38, listE_out_g(T38)) → listE_out_g(.(T36, T38))
U6_ag(X100, T26, listE_out_g(T26)) → listF_out_ag(X100, T26)
U8_gaa(T9, T10, X35, listF_out_ag(X35, T10)) → pC_out_gaa(T9, T10, X35)
U2_g(T9, pC_out_gaa(T9, X36, X35)) → goalA_out_g(s(T9))

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(T16), .(X75, X76)) → S2LD_IN_GA(T16, X76)

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(T16)) → S2LD_IN_GA(T16)

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(T16)) → S2LD_IN_GA(T16)
  The graph contains the following edges 1 > 1

(20) YES