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

(0) Obligation:

Clauses:

p(cons(X, nil)).
p(cons(s(s(X)), cons(Y, Xs))) :- ','(p(cons(X, cons(Y, Xs))), ','(mult(X, Y, Z), p(cons(Z, Xs)))).
p(cons(0, Xs)) :- p(Xs).
sum(X, 0, X).
sum(X, s(Y), s(Z)) :- sum(X, Y, Z).
mult(X1, 0, 0).
mult(X, s(Y), Z) :- ','(mult(X, Y, W), sum(W, X, Z)).

Query: p(g)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="3: p(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: p(T1), SCOPE: 1, CLAUSE: 0 | p(T1), SCOPE: 1, CLAUSE: 1 | p(T1), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: p(T1), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: p(T1), SCOPE: 1, CLAUSE: 1 | p(T1), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: p(T1), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: p(T1), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(p(cons(T19, cons(T20, T21))), ','(mult(T19, T20, X24), p(cons(X24, T21))))\n\nT19 is ground\nT20 is ground\nT21 is ground\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: p(cons(T19, cons(T20, T21)))\n\nT19 is ground\nT20 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(mult(T19, T20, X24), p(cons(X24, T21)))\n\nT19 is ground\nT20 is ground\nT21 is ground\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: mult(T19, T20, X24)\n\nT19 is ground\nT20 is ground\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: p(cons(T28, T21))\n\nT21 is ground\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: mult(T19, T20, X24), SCOPE: 2, CLAUSE: 5 | mult(T19, T20, X24), SCOPE: 2, CLAUSE: 6\n\nT19 is ground\nT20 is ground\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: mult(T19, T20, X24), SCOPE: 2, CLAUSE: 5\n\nT19 is ground\nT20 is ground\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: mult(T19, T20, X24), SCOPE: 2, CLAUSE: 6\n\nT19 is ground\nT20 is ground\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: ','(mult(T40, T41, X50), sum(X50, T40, X51))\n\nT40 is ground\nT41 is ground\nX51 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: mult(T40, T41, X50)\n\nT40 is ground\nT41 is ground\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: sum(T44, T40, X51)\n\nT40 is ground\nT44 is ground\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: sum(T44, T40, X51), SCOPE: 3, CLAUSE: 3 | sum(T44, T40, X51), SCOPE: 3, CLAUSE: 4\n\nT40 is ground\nT44 is ground\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: sum(T44, T40, X51), SCOPE: 3, CLAUSE: 3\n\nT40 is ground\nT44 is ground\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: sum(T44, T40, X51), SCOPE: 3, CLAUSE: 4\n\nT40 is ground\nT44 is ground\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: sum(T58, T59, X74)\n\nT58 is ground\nT59 is ground\nX74 is free", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: p(T66)\n\nT66 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 147 [arrowhead = none ];
147 -> 5;

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

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

150 [label="EVAL with clause\np(cons(X6, nil)).\nand substitutionX6 -> T6,\nT1 -> cons(T6, nil)", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 150 [arrowhead = none ];
150 -> 13;

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

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

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

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

155 [label="EVAL with clause\np(cons(s(s(X21)), cons(X22, X23))) :- ','(p(cons(X21, cons(X22, X23))), ','(mult(X21, X22, X24), p(cons(X24, X23)))).\nand substitutionX21 -> T19,\nX22 -> T20,\nX23 -> T21,\nT1 -> cons(s(s(T19)), cons(T20, T21))", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 155 [arrowhead = none ];
155 -> 34;

156 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
20 -> 156 [arrowhead = none ];
156 -> 35;

157 [label="EVAL with clause\np(cons(0, X81)) :- p(X81).\nand substitutionX81 -> T66,\nT1 -> cons(0, T66)", fontsize=14, style = filled, fillcolor = lightblue];
21 -> 157 [arrowhead = none ];
157 -> 144;

158 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
21 -> 158 [arrowhead = none ];
158 -> 146;

159 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
34 -> 159 [arrowhead = none ];
159 -> 48;

160 [label="SPLIT 2\nnew knowledge:\nT19 is ground\nT20 is ground\nT21 is ground", fontsize=14, style = filled, fillcolor = violet];
34 -> 160 [arrowhead = none ];
160 -> 49;

161 [label="INSTANCE with matching:\nT1 -> cons(T19, cons(T20, T21))", fontsize=14, style = filled, fillcolor = lightgrey];
48 -> 161 [arrowhead = none , style=dashed];
161 -> 3[style=dashed];

162 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
49 -> 162 [arrowhead = none ];
162 -> 60;

163 [label="SPLIT 2\nnew knowledge:\nT19 is ground\nT20 is ground\nT28 is ground\nreplacements:X24 -> T28", fontsize=14, style = filled, fillcolor = violet];
49 -> 163 [arrowhead = none ];
163 -> 61;

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

165 [label="INSTANCE with matching:\nT1 -> cons(T28, T21)", fontsize=14, style = filled, fillcolor = lightgrey];
61 -> 165 [arrowhead = none , style=dashed];
165 -> 3[style=dashed];

166 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
65 -> 166 [arrowhead = none ];
166 -> 69;

167 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
65 -> 167 [arrowhead = none ];
167 -> 70;

168 [label="EVAL with clause\nmult(X37, 0, 0).\nand substitutionT19 -> T35,\nX37 -> T35,\nT20 -> 0,\nX24 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
69 -> 168 [arrowhead = none ];
168 -> 81;

169 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
69 -> 169 [arrowhead = none ];
169 -> 82;

170 [label="EVAL with clause\nmult(X47, s(X48), X49) :- ','(mult(X47, X48, X50), sum(X50, X47, X49)).\nand substitutionT19 -> T40,\nX47 -> T40,\nX48 -> T41,\nT20 -> s(T41),\nX24 -> X51,\nX49 -> X51", fontsize=14, style = filled, fillcolor = lightblue];
70 -> 170 [arrowhead = none ];
170 -> 99;

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

172 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
81 -> 172 [arrowhead = none ];
172 -> 83;

173 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
99 -> 173 [arrowhead = none ];
173 -> 106;

174 [label="SPLIT 2\nnew knowledge:\nT40 is ground\nT41 is ground\nT44 is ground\nreplacements:X50 -> T44", fontsize=14, style = filled, fillcolor = violet];
99 -> 174 [arrowhead = none ];
174 -> 107;

175 [label="INSTANCE with matching:\nT19 -> T40\nT20 -> T41\nX24 -> X50", fontsize=14, style = filled, fillcolor = lightgrey];
106 -> 175 [arrowhead = none , style=dashed];
175 -> 60[style=dashed];

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

177 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
112 -> 177 [arrowhead = none ];
177 -> 113;

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

179 [label="EVAL with clause\nsum(X62, 0, X62).\nand substitutionT44 -> T53,\nX62 -> T53,\nT40 -> 0,\nX51 -> T53", fontsize=14, style = filled, fillcolor = lightblue];
113 -> 179 [arrowhead = none ];
179 -> 123;

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

181 [label="EVAL with clause\nsum(X71, s(X72), s(X73)) :- sum(X71, X72, X73).\nand substitutionT44 -> T58,\nX71 -> T58,\nX72 -> T59,\nT40 -> s(T59),\nX73 -> X74,\nX51 -> s(X74)", fontsize=14, style = filled, fillcolor = lightblue];
114 -> 181 [arrowhead = none ];
181 -> 136;

182 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
114 -> 182 [arrowhead = none ];
182 -> 137;

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

184 [label="INSTANCE with matching:\nT44 -> T58\nT40 -> T59\nX51 -> X74", fontsize=14, style = filled, fillcolor = lightgrey];
136 -> 184 [arrowhead = none , style=dashed];
184 -> 107[style=dashed];

185 [label="INSTANCE with matching:\nT1 -> T66", fontsize=14, style = filled, fillcolor = lightgrey];
144 -> 185 [arrowhead = none , style=dashed];
185 -> 3[style=dashed];

}

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

f3_in(cons(T6, nil)) → f3_out1
f3_in(cons(s(s(T19)), cons(T20, T21))) → U1(f34_in(T19, T20, T21), cons(s(s(T19)), cons(T20, T21)))
U1(f34_out1(X24), cons(s(s(T19)), cons(T20, T21))) → f3_out1
f3_in(cons(0, T66)) → U2(f3_in(T66), cons(0, T66))
U2(f3_out1, cons(0, T66)) → f3_out1
f60_in(T35, 0) → f60_out1(0)
f60_in(T40, s(T41)) → U3(f99_in(T40, T41), T40, s(T41))
U3(f99_out1(X50, X51), T40, s(T41)) → f60_out1(X51)
f107_in(T53, 0) → f107_out1(T53)
f107_in(T58, s(T59)) → U4(f107_in(T58, T59), T58, s(T59))
U4(f107_out1(X74), T58, s(T59)) → f107_out1(s(X74))
f34_in(T19, T20, T21) → U5(f3_in(cons(T19, cons(T20, T21))), T19, T20, T21)
U5(f3_out1, T19, T20, T21) → U6(f49_in(T19, T20, T21), T19, T20, T21)
U6(f49_out1(X24), T19, T20, T21) → f34_out1(X24)
f49_in(T19, T20, T21) → U7(f60_in(T19, T20), T19, T20, T21)
U7(f60_out1(T28), T19, T20, T21) → U8(f3_in(cons(T28, T21)), T19, T20, T21, T28)
U8(f3_out1, T19, T20, T21, T28) → f49_out1(T28)
f99_in(T40, T41) → U9(f60_in(T40, T41), T40, T41)
U9(f60_out1(T44), T40, T41) → U10(f107_in(T44, T40), T40, T41, T44)
U10(f107_out1(X51), T40, T41, T44) → f99_out1(T44, X51)

Q is empty.

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(4) Obligation:

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

F3_IN(cons(s(s(T19)), cons(T20, T21))) → U1¹(f34_in(T19, T20, T21), cons(s(s(T19)), cons(T20, T21)))
F3_IN(cons(s(s(T19)), cons(T20, T21))) → F34_IN(T19, T20, T21)
F3_IN(cons(0, T66)) → U2¹(f3_in(T66), cons(0, T66))
F3_IN(cons(0, T66)) → F3_IN(T66)
F60_IN(T40, s(T41)) → U3¹(f99_in(T40, T41), T40, s(T41))
F60_IN(T40, s(T41)) → F99_IN(T40, T41)
F107_IN(T58, s(T59)) → U4¹(f107_in(T58, T59), T58, s(T59))
F107_IN(T58, s(T59)) → F107_IN(T58, T59)
F34_IN(T19, T20, T21) → U5¹(f3_in(cons(T19, cons(T20, T21))), T19, T20, T21)
F34_IN(T19, T20, T21) → F3_IN(cons(T19, cons(T20, T21)))
U5¹(f3_out1, T19, T20, T21) → U6¹(f49_in(T19, T20, T21), T19, T20, T21)
U5¹(f3_out1, T19, T20, T21) → F49_IN(T19, T20, T21)
F49_IN(T19, T20, T21) → U7¹(f60_in(T19, T20), T19, T20, T21)
F49_IN(T19, T20, T21) → F60_IN(T19, T20)
U7¹(f60_out1(T28), T19, T20, T21) → U8¹(f3_in(cons(T28, T21)), T19, T20, T21, T28)
U7¹(f60_out1(T28), T19, T20, T21) → F3_IN(cons(T28, T21))
F99_IN(T40, T41) → U9¹(f60_in(T40, T41), T40, T41)
F99_IN(T40, T41) → F60_IN(T40, T41)
U9¹(f60_out1(T44), T40, T41) → U10¹(f107_in(T44, T40), T40, T41, T44)
U9¹(f60_out1(T44), T40, T41) → F107_IN(T44, T40)

The TRS R consists of the following rules:

f3_in(cons(T6, nil)) → f3_out1
f3_in(cons(s(s(T19)), cons(T20, T21))) → U1(f34_in(T19, T20, T21), cons(s(s(T19)), cons(T20, T21)))
U1(f34_out1(X24), cons(s(s(T19)), cons(T20, T21))) → f3_out1
f3_in(cons(0, T66)) → U2(f3_in(T66), cons(0, T66))
U2(f3_out1, cons(0, T66)) → f3_out1
f60_in(T35, 0) → f60_out1(0)
f60_in(T40, s(T41)) → U3(f99_in(T40, T41), T40, s(T41))
U3(f99_out1(X50, X51), T40, s(T41)) → f60_out1(X51)
f107_in(T53, 0) → f107_out1(T53)
f107_in(T58, s(T59)) → U4(f107_in(T58, T59), T58, s(T59))
U4(f107_out1(X74), T58, s(T59)) → f107_out1(s(X74))
f34_in(T19, T20, T21) → U5(f3_in(cons(T19, cons(T20, T21))), T19, T20, T21)
U5(f3_out1, T19, T20, T21) → U6(f49_in(T19, T20, T21), T19, T20, T21)
U6(f49_out1(X24), T19, T20, T21) → f34_out1(X24)
f49_in(T19, T20, T21) → U7(f60_in(T19, T20), T19, T20, T21)
U7(f60_out1(T28), T19, T20, T21) → U8(f3_in(cons(T28, T21)), T19, T20, T21, T28)
U8(f3_out1, T19, T20, T21, T28) → f49_out1(T28)
f99_in(T40, T41) → U9(f60_in(T40, T41), T40, T41)
U9(f60_out1(T44), T40, T41) → U10(f107_in(T44, T40), T40, T41, T44)
U10(f107_out1(X51), T40, T41, T44) → f99_out1(T44, X51)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 3 SCCs with 10 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

F107_IN(T58, s(T59)) → F107_IN(T58, T59)

The TRS R consists of the following rules:

f3_in(cons(T6, nil)) → f3_out1
f3_in(cons(s(s(T19)), cons(T20, T21))) → U1(f34_in(T19, T20, T21), cons(s(s(T19)), cons(T20, T21)))
U1(f34_out1(X24), cons(s(s(T19)), cons(T20, T21))) → f3_out1
f3_in(cons(0, T66)) → U2(f3_in(T66), cons(0, T66))
U2(f3_out1, cons(0, T66)) → f3_out1
f60_in(T35, 0) → f60_out1(0)
f60_in(T40, s(T41)) → U3(f99_in(T40, T41), T40, s(T41))
U3(f99_out1(X50, X51), T40, s(T41)) → f60_out1(X51)
f107_in(T53, 0) → f107_out1(T53)
f107_in(T58, s(T59)) → U4(f107_in(T58, T59), T58, s(T59))
U4(f107_out1(X74), T58, s(T59)) → f107_out1(s(X74))
f34_in(T19, T20, T21) → U5(f3_in(cons(T19, cons(T20, T21))), T19, T20, T21)
U5(f3_out1, T19, T20, T21) → U6(f49_in(T19, T20, T21), T19, T20, T21)
U6(f49_out1(X24), T19, T20, T21) → f34_out1(X24)
f49_in(T19, T20, T21) → U7(f60_in(T19, T20), T19, T20, T21)
U7(f60_out1(T28), T19, T20, T21) → U8(f3_in(cons(T28, T21)), T19, T20, T21, T28)
U8(f3_out1, T19, T20, T21, T28) → f49_out1(T28)
f99_in(T40, T41) → U9(f60_in(T40, T41), T40, T41)
U9(f60_out1(T44), T40, T41) → U10(f107_in(T44, T40), T40, T41, T44)
U10(f107_out1(X51), T40, T41, T44) → f99_out1(T44, X51)

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

(8) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(9) Obligation:

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

F107_IN(T58, s(T59)) → F107_IN(T58, T59)

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

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

• F107_IN(T58, s(T59)) → F107_IN(T58, T59)
  The graph contains the following edges 1 >= 1, 2 > 2

(11) YES

(12) Obligation:

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

F60_IN(T40, s(T41)) → F99_IN(T40, T41)
F99_IN(T40, T41) → F60_IN(T40, T41)

The TRS R consists of the following rules:

f3_in(cons(T6, nil)) → f3_out1
f3_in(cons(s(s(T19)), cons(T20, T21))) → U1(f34_in(T19, T20, T21), cons(s(s(T19)), cons(T20, T21)))
U1(f34_out1(X24), cons(s(s(T19)), cons(T20, T21))) → f3_out1
f3_in(cons(0, T66)) → U2(f3_in(T66), cons(0, T66))
U2(f3_out1, cons(0, T66)) → f3_out1
f60_in(T35, 0) → f60_out1(0)
f60_in(T40, s(T41)) → U3(f99_in(T40, T41), T40, s(T41))
U3(f99_out1(X50, X51), T40, s(T41)) → f60_out1(X51)
f107_in(T53, 0) → f107_out1(T53)
f107_in(T58, s(T59)) → U4(f107_in(T58, T59), T58, s(T59))
U4(f107_out1(X74), T58, s(T59)) → f107_out1(s(X74))
f34_in(T19, T20, T21) → U5(f3_in(cons(T19, cons(T20, T21))), T19, T20, T21)
U5(f3_out1, T19, T20, T21) → U6(f49_in(T19, T20, T21), T19, T20, T21)
U6(f49_out1(X24), T19, T20, T21) → f34_out1(X24)
f49_in(T19, T20, T21) → U7(f60_in(T19, T20), T19, T20, T21)
U7(f60_out1(T28), T19, T20, T21) → U8(f3_in(cons(T28, T21)), T19, T20, T21, T28)
U8(f3_out1, T19, T20, T21, T28) → f49_out1(T28)
f99_in(T40, T41) → U9(f60_in(T40, T41), T40, T41)
U9(f60_out1(T44), T40, T41) → U10(f107_in(T44, T40), T40, T41, T44)
U10(f107_out1(X51), T40, T41, T44) → f99_out1(T44, X51)

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

(13) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(14) Obligation:

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

F60_IN(T40, s(T41)) → F99_IN(T40, T41)
F99_IN(T40, T41) → F60_IN(T40, T41)

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

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

• F99_IN(T40, T41) → F60_IN(T40, T41)
  The graph contains the following edges 1 >= 1, 2 >= 2

• F60_IN(T40, s(T41)) → F99_IN(T40, T41)
  The graph contains the following edges 1 >= 1, 2 > 2

(16) YES

(17) Obligation:

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

F3_IN(cons(s(s(T19)), cons(T20, T21))) → F34_IN(T19, T20, T21)
F34_IN(T19, T20, T21) → U5¹(f3_in(cons(T19, cons(T20, T21))), T19, T20, T21)
U5¹(f3_out1, T19, T20, T21) → F49_IN(T19, T20, T21)
F49_IN(T19, T20, T21) → U7¹(f60_in(T19, T20), T19, T20, T21)
U7¹(f60_out1(T28), T19, T20, T21) → F3_IN(cons(T28, T21))
F3_IN(cons(0, T66)) → F3_IN(T66)
F34_IN(T19, T20, T21) → F3_IN(cons(T19, cons(T20, T21)))

The TRS R consists of the following rules:

f3_in(cons(T6, nil)) → f3_out1
f3_in(cons(s(s(T19)), cons(T20, T21))) → U1(f34_in(T19, T20, T21), cons(s(s(T19)), cons(T20, T21)))
U1(f34_out1(X24), cons(s(s(T19)), cons(T20, T21))) → f3_out1
f3_in(cons(0, T66)) → U2(f3_in(T66), cons(0, T66))
U2(f3_out1, cons(0, T66)) → f3_out1
f60_in(T35, 0) → f60_out1(0)
f60_in(T40, s(T41)) → U3(f99_in(T40, T41), T40, s(T41))
U3(f99_out1(X50, X51), T40, s(T41)) → f60_out1(X51)
f107_in(T53, 0) → f107_out1(T53)
f107_in(T58, s(T59)) → U4(f107_in(T58, T59), T58, s(T59))
U4(f107_out1(X74), T58, s(T59)) → f107_out1(s(X74))
f34_in(T19, T20, T21) → U5(f3_in(cons(T19, cons(T20, T21))), T19, T20, T21)
U5(f3_out1, T19, T20, T21) → U6(f49_in(T19, T20, T21), T19, T20, T21)
U6(f49_out1(X24), T19, T20, T21) → f34_out1(X24)
f49_in(T19, T20, T21) → U7(f60_in(T19, T20), T19, T20, T21)
U7(f60_out1(T28), T19, T20, T21) → U8(f3_in(cons(T28, T21)), T19, T20, T21, T28)
U8(f3_out1, T19, T20, T21, T28) → f49_out1(T28)
f99_in(T40, T41) → U9(f60_in(T40, T41), T40, T41)
U9(f60_out1(T44), T40, T41) → U10(f107_in(T44, T40), T40, T41, T44)
U10(f107_out1(X51), T40, T41, T44) → f99_out1(T44, X51)

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

(18) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

F3_IN(cons(0, T66)) → F3_IN(T66)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(0) = 1   
POL(F34_IN(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(F3_IN(x₁)) = x₁   
POL(F49_IN(x₁, x₂, x₃)) = x₂ + x₃   
POL(U1(x₁, x₂)) = 0   
POL(U10(x₁, x₂, x₃, x₄)) = x₁   
POL(U2(x₁, x₂)) = 0   
POL(U3(x₁, x₂, x₃)) = x₁   
POL(U4(x₁, x₂, x₃)) = x₁   
POL(U5(x₁, x₂, x₃, x₄)) = 1   
POL(U5¹(x₁, x₂, x₃, x₄)) = x₃ + x₄   
POL(U6(x₁, x₂, x₃, x₄)) = 1   
POL(U7(x₁, x₂, x₃, x₄)) = 0   
POL(U7¹(x₁, x₂, x₃, x₄)) = x₁ + x₄   
POL(U8(x₁, x₂, x₃, x₄, x₅)) = 0   
POL(U9(x₁, x₂, x₃)) = x₁   
POL(cons(x₁, x₂)) = x₁ + x₂   
POL(f107_in(x₁, x₂)) = x₁   
POL(f107_out1(x₁)) = x₁   
POL(f34_in(x₁, x₂, x₃)) = 1 + x₃   
POL(f34_out1(x₁)) = 0   
POL(f3_in(x₁)) = 0   
POL(f3_out1) = 0   
POL(f49_in(x₁, x₂, x₃)) = 1   
POL(f49_out1(x₁)) = 0   
POL(f60_in(x₁, x₂)) = x₂   
POL(f60_out1(x₁)) = x₁   
POL(f99_in(x₁, x₂)) = x₂   
POL(f99_out1(x₁, x₂)) = x₂   
POL(nil) = 0   
POL(s(x₁)) = x₁   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

f60_in(T35, 0) → f60_out1(0)
f60_in(T40, s(T41)) → U3(f99_in(T40, T41), T40, s(T41))
U3(f99_out1(X50, X51), T40, s(T41)) → f60_out1(X51)
f99_in(T40, T41) → U9(f60_in(T40, T41), T40, T41)
U9(f60_out1(T44), T40, T41) → U10(f107_in(T44, T40), T40, T41, T44)
f107_in(T53, 0) → f107_out1(T53)
f107_in(T58, s(T59)) → U4(f107_in(T58, T59), T58, s(T59))
U10(f107_out1(X51), T40, T41, T44) → f99_out1(T44, X51)
U4(f107_out1(X74), T58, s(T59)) → f107_out1(s(X74))

(19) Obligation:

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

F3_IN(cons(s(s(T19)), cons(T20, T21))) → F34_IN(T19, T20, T21)
F34_IN(T19, T20, T21) → U5¹(f3_in(cons(T19, cons(T20, T21))), T19, T20, T21)
U5¹(f3_out1, T19, T20, T21) → F49_IN(T19, T20, T21)
F49_IN(T19, T20, T21) → U7¹(f60_in(T19, T20), T19, T20, T21)
U7¹(f60_out1(T28), T19, T20, T21) → F3_IN(cons(T28, T21))
F34_IN(T19, T20, T21) → F3_IN(cons(T19, cons(T20, T21)))

The TRS R consists of the following rules:

f3_in(cons(T6, nil)) → f3_out1
f3_in(cons(s(s(T19)), cons(T20, T21))) → U1(f34_in(T19, T20, T21), cons(s(s(T19)), cons(T20, T21)))
U1(f34_out1(X24), cons(s(s(T19)), cons(T20, T21))) → f3_out1
f3_in(cons(0, T66)) → U2(f3_in(T66), cons(0, T66))
U2(f3_out1, cons(0, T66)) → f3_out1
f60_in(T35, 0) → f60_out1(0)
f60_in(T40, s(T41)) → U3(f99_in(T40, T41), T40, s(T41))
U3(f99_out1(X50, X51), T40, s(T41)) → f60_out1(X51)
f107_in(T53, 0) → f107_out1(T53)
f107_in(T58, s(T59)) → U4(f107_in(T58, T59), T58, s(T59))
U4(f107_out1(X74), T58, s(T59)) → f107_out1(s(X74))
f34_in(T19, T20, T21) → U5(f3_in(cons(T19, cons(T20, T21))), T19, T20, T21)
U5(f3_out1, T19, T20, T21) → U6(f49_in(T19, T20, T21), T19, T20, T21)
U6(f49_out1(X24), T19, T20, T21) → f34_out1(X24)
f49_in(T19, T20, T21) → U7(f60_in(T19, T20), T19, T20, T21)
U7(f60_out1(T28), T19, T20, T21) → U8(f3_in(cons(T28, T21)), T19, T20, T21, T28)
U8(f3_out1, T19, T20, T21, T28) → f49_out1(T28)
f99_in(T40, T41) → U9(f60_in(T40, T41), T40, T41)
U9(f60_out1(T44), T40, T41) → U10(f107_in(T44, T40), T40, T41, T44)
U10(f107_out1(X51), T40, T41, T44) → f99_out1(T44, X51)

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

(20) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

U7¹(f60_out1(T28), T19, T20, T21) → F3_IN(cons(T28, T21))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( U5¹(x₁, ..., x₄) ) = 2x₄ + 2

POL( f3_in(x₁) ) = max{0, -2}

POL( cons(x₁, x₂) ) = x₂ + 1

POL( s(x₁) ) = 0

POL( U1(x₁, x₂) ) = max{0, 2x₁ - 1}

POL( f34_in(x₁, ..., x₃) ) = x₂ + x₃

POL( 0 ) = 2

POL( U2(x₁, x₂) ) = max{0, -1}

POL( U7¹(x₁, ..., x₄) ) = 2x₄ + 2

POL( U7(x₁, ..., x₄) ) = 2x₂ + x₃ + x₄ + 2

POL( f60_in(x₁, x₂) ) = 2x₁

POL( f60_out1(x₁) ) = max{0, 2x₁ - 2}

POL( U3(x₁, ..., x₃) ) = max{0, x₁ - 2}

POL( f99_in(x₁, x₂) ) = x₁ + x₂ + 1

POL( f34_out1(x₁) ) = 2x₁

POL( f3_out1 ) = 0

POL( U5(x₁, ..., x₄) ) = max{0, x₁ + 2x₃ + 2x₄ - 2}

POL( U8(x₁, ..., x₅) ) = max{0, 2x₁ - 2}

POL( nil ) = 2

POL( U6(x₁, ..., x₄) ) = 2x₁ + x₂ + 2x₃ + x₄

POL( f49_in(x₁, ..., x₃) ) = 2x₁ + x₂ + 2x₃

POL( f49_out1(x₁) ) = 2

POL( f99_out1(x₁, x₂) ) = 2x₁ + x₂ + 2

POL( U9(x₁, ..., x₃) ) = max{0, 2x₁ + 2x₂ + 2x₃ - 1}

POL( U10(x₁, ..., x₄) ) = max{0, -2}

POL( f107_in(x₁, x₂) ) = 2x₁ + x₂

POL( f107_out1(x₁) ) = max{0, 2x₁ - 2}

POL( U4(x₁, ..., x₃) ) = max{0, 2x₁ + x₂ - 2}

POL( F3_IN(x₁) ) = max{0, 2x₁ - 2}

POL( F34_IN(x₁, ..., x₃) ) = 2x₃ + 2

POL( F49_IN(x₁, ..., x₃) ) = 2x₃ + 2

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
none

(21) Obligation:

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

F3_IN(cons(s(s(T19)), cons(T20, T21))) → F34_IN(T19, T20, T21)
F34_IN(T19, T20, T21) → U5¹(f3_in(cons(T19, cons(T20, T21))), T19, T20, T21)
U5¹(f3_out1, T19, T20, T21) → F49_IN(T19, T20, T21)
F49_IN(T19, T20, T21) → U7¹(f60_in(T19, T20), T19, T20, T21)
F34_IN(T19, T20, T21) → F3_IN(cons(T19, cons(T20, T21)))

The TRS R consists of the following rules:

f3_in(cons(T6, nil)) → f3_out1
f3_in(cons(s(s(T19)), cons(T20, T21))) → U1(f34_in(T19, T20, T21), cons(s(s(T19)), cons(T20, T21)))
U1(f34_out1(X24), cons(s(s(T19)), cons(T20, T21))) → f3_out1
f3_in(cons(0, T66)) → U2(f3_in(T66), cons(0, T66))
U2(f3_out1, cons(0, T66)) → f3_out1
f60_in(T35, 0) → f60_out1(0)
f60_in(T40, s(T41)) → U3(f99_in(T40, T41), T40, s(T41))
U3(f99_out1(X50, X51), T40, s(T41)) → f60_out1(X51)
f107_in(T53, 0) → f107_out1(T53)
f107_in(T58, s(T59)) → U4(f107_in(T58, T59), T58, s(T59))
U4(f107_out1(X74), T58, s(T59)) → f107_out1(s(X74))
f34_in(T19, T20, T21) → U5(f3_in(cons(T19, cons(T20, T21))), T19, T20, T21)
U5(f3_out1, T19, T20, T21) → U6(f49_in(T19, T20, T21), T19, T20, T21)
U6(f49_out1(X24), T19, T20, T21) → f34_out1(X24)
f49_in(T19, T20, T21) → U7(f60_in(T19, T20), T19, T20, T21)
U7(f60_out1(T28), T19, T20, T21) → U8(f3_in(cons(T28, T21)), T19, T20, T21, T28)
U8(f3_out1, T19, T20, T21, T28) → f49_out1(T28)
f99_in(T40, T41) → U9(f60_in(T40, T41), T40, T41)
U9(f60_out1(T44), T40, T41) → U10(f107_in(T44, T40), T40, T41, T44)
U10(f107_out1(X51), T40, T41, T44) → f99_out1(T44, X51)

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

(22) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 3 less nodes.

(23) Obligation:

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

F34_IN(T19, T20, T21) → F3_IN(cons(T19, cons(T20, T21)))
F3_IN(cons(s(s(T19)), cons(T20, T21))) → F34_IN(T19, T20, T21)

The TRS R consists of the following rules:

f3_in(cons(T6, nil)) → f3_out1
f3_in(cons(s(s(T19)), cons(T20, T21))) → U1(f34_in(T19, T20, T21), cons(s(s(T19)), cons(T20, T21)))
U1(f34_out1(X24), cons(s(s(T19)), cons(T20, T21))) → f3_out1
f3_in(cons(0, T66)) → U2(f3_in(T66), cons(0, T66))
U2(f3_out1, cons(0, T66)) → f3_out1
f60_in(T35, 0) → f60_out1(0)
f60_in(T40, s(T41)) → U3(f99_in(T40, T41), T40, s(T41))
U3(f99_out1(X50, X51), T40, s(T41)) → f60_out1(X51)
f107_in(T53, 0) → f107_out1(T53)
f107_in(T58, s(T59)) → U4(f107_in(T58, T59), T58, s(T59))
U4(f107_out1(X74), T58, s(T59)) → f107_out1(s(X74))
f34_in(T19, T20, T21) → U5(f3_in(cons(T19, cons(T20, T21))), T19, T20, T21)
U5(f3_out1, T19, T20, T21) → U6(f49_in(T19, T20, T21), T19, T20, T21)
U6(f49_out1(X24), T19, T20, T21) → f34_out1(X24)
f49_in(T19, T20, T21) → U7(f60_in(T19, T20), T19, T20, T21)
U7(f60_out1(T28), T19, T20, T21) → U8(f3_in(cons(T28, T21)), T19, T20, T21, T28)
U8(f3_out1, T19, T20, T21, T28) → f49_out1(T28)
f99_in(T40, T41) → U9(f60_in(T40, T41), T40, T41)
U9(f60_out1(T44), T40, T41) → U10(f107_in(T44, T40), T40, T41, T44)
U10(f107_out1(X51), T40, T41, T44) → f99_out1(T44, X51)

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

(24) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(25) Obligation:

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

F34_IN(T19, T20, T21) → F3_IN(cons(T19, cons(T20, T21)))
F3_IN(cons(s(s(T19)), cons(T20, T21))) → F34_IN(T19, T20, T21)

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

(26) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

F3_IN(cons(s(s(T19)), cons(T20, T21))) → F34_IN(T19, T20, T21)

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(F34_IN(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(F3_IN(x₁)) = x₁   
POL(cons(x₁, x₂)) = x₁ + x₂   
POL(s(x₁)) = 2·x₁   

(27) Obligation:

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

F34_IN(T19, T20, T21) → F3_IN(cons(T19, cons(T20, T21)))

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

(28) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(29) TRUE