Left Termination proof of /tmp/tmp4J3gGB/flatten

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 213 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 242 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 19 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇒, 17 ms)

        ↳11 QDP

        ↳12 UsableRulesReductionPairsProof (⇔, 0 ms)

        ↳13 QDP

        ↳14 QDPSizeChangeProof (⇔, 0 ms)

        ↳15 YES

    ↳16 PiDP

        ↳17 UsableRulesProof (⇔, 0 ms)

        ↳18 PiDP

        ↳19 PiDPToQDPProof (⇒, 11 ms)

        ↳20 QDP

        ↳21 Rewriting (⇔, 13 ms)

        ↳22 QDP

        ↳23 UsableRulesProof (⇔, 0 ms)

        ↳24 QDP

        ↳25 QReductionProof (⇔, 0 ms)

        ↳26 QDP

        ↳27 QDPOrderProof (⇔, 229 ms)

        ↳28 QDP

        ↳29 DependencyGraphProof (⇔, 0 ms)

        ↳30 TRUE

(0) Obligation:

Clauses:

flatten(atom(X), .(X, [])).
flatten(cons(atom(X), U), .(X, Y)) :- flatten(U, Y).
flatten(cons(cons(U, V), W), X) :- flatten(cons(U, cons(V, W)), X).
count(atom(X), s(0)).
count(cons(atom(X), Y), s(Z)) :- count(Y, Z).
count(cons(cons(U, V), W), Z) :- ','(flatten(cons(cons(U, V), W), X), count(X, Z)).

Query: count(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: count(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: count(T1, T2), SCOPE: 1, CLAUSE: 3 | count(T1, T2), SCOPE: 1, CLAUSE: 4 | count(T1, T2), SCOPE: 1, CLAUSE: 5\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: true | count(atom(T4), T2), SCOPE: 1, CLAUSE: 4 | count(atom(T4), T2), SCOPE: 1, CLAUSE: 5\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: count(T1, T2), SCOPE: 1, CLAUSE: 4 | count(T1, T2), SCOPE: 1, CLAUSE: 5\n\nT1 is ground\nX2 is free\ncount(T1, T2) !=? count(atom(X2), s(0))", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: count(atom(T4), T2), SCOPE: 1, CLAUSE: 4 | count(atom(T4), T2), SCOPE: 1, CLAUSE: 5\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: count(atom(T4), T2), SCOPE: 1, CLAUSE: 5\n\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: count(T9, T11) | count(cons(atom(T8), T9), T2), SCOPE: 1, CLAUSE: 5\n\nT8 is ground\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: count(T1, T2), SCOPE: 1, CLAUSE: 5\n\nT1 is ground\nX2 is free\nX13 is free\nX14 is free\nX15 is free\ncount(T1, T2) !=? count(atom(X2), s(0))\ncount(T1, T2) !=? count(cons(atom(X13), X14), s(X15))", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: count(T9, T11), SCOPE: 2, CLAUSE: 3 | count(T9, T11), SCOPE: 2, CLAUSE: 4 | count(T9, T11), SCOPE: 2, CLAUSE: 5 | ?_2 | count(cons(atom(T8), T9), T2), SCOPE: 1, CLAUSE: 5\n\nT8 is ground\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: count(T9, T11), SCOPE: 2, CLAUSE: 3\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: count(T9, T11), SCOPE: 2, CLAUSE: 4 | count(T9, T11), SCOPE: 2, CLAUSE: 5 | ?_2 | count(cons(atom(T8), T9), T2), SCOPE: 1, CLAUSE: 5\n\nT8 is ground\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: count(T9, T11), SCOPE: 2, CLAUSE: 4\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: count(T9, T11), SCOPE: 2, CLAUSE: 5 | ?_2 | count(cons(atom(T8), T9), T2), SCOPE: 1, CLAUSE: 5\n\nT8 is ground\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: count(T30, T32)\n\nT30 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: count(T9, T11), SCOPE: 2, CLAUSE: 5\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: ?_2 | count(cons(atom(T8), T9), T2), SCOPE: 1, CLAUSE: 5\n\nT8 is ground\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="B: ','(flatten(cons(cons(T51, T52), T53), X60), count(X60, T55))\n\nT51 is ground\nT52 is ground\nT53 is ground\nX60 is free", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="F: flatten(cons(cons(T51, T52), T53), X60)\n\nT51 is ground\nT52 is ground\nT53 is ground\nX60 is free", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: count(T56, T55)\n\nT56 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: flatten(cons(cons(T51, T52), T53), X60), SCOPE: 3, CLAUSE: 0 | flatten(cons(cons(T51, T52), T53), X60), SCOPE: 3, CLAUSE: 1 | flatten(cons(cons(T51, T52), T53), X60), SCOPE: 3, CLAUSE: 2\n\nT51 is ground\nT52 is ground\nT53 is ground\nX60 is free", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: flatten(cons(cons(T51, T52), T53), X60), SCOPE: 3, CLAUSE: 1 | flatten(cons(cons(T51, T52), T53), X60), SCOPE: 3, CLAUSE: 2\n\nT51 is ground\nT52 is ground\nT53 is ground\nX60 is free", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: flatten(cons(cons(T51, T52), T53), X60), SCOPE: 3, CLAUSE: 2\n\nT51 is ground\nT52 is ground\nT53 is ground\nX60 is free", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="E: flatten(cons(T63, cons(T64, T65)), X85)\n\nT63 is ground\nT64 is ground\nT65 is ground\nX85 is free", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: flatten(cons(T63, cons(T64, T65)), X85), SCOPE: 4, CLAUSE: 0 | flatten(cons(T63, cons(T64, T65)), X85), SCOPE: 4, CLAUSE: 1 | flatten(cons(T63, cons(T64, T65)), X85), SCOPE: 4, CLAUSE: 2\n\nT63 is ground\nT64 is ground\nT65 is ground\nX85 is free", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: flatten(cons(T63, cons(T64, T65)), X85), SCOPE: 4, CLAUSE: 1 | flatten(cons(T63, cons(T64, T65)), X85), SCOPE: 4, CLAUSE: 2\n\nT63 is ground\nT64 is ground\nT65 is ground\nX85 is free", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: flatten(cons(T63, cons(T64, T65)), X85), SCOPE: 4, CLAUSE: 1\n\nT63 is ground\nT64 is ground\nT65 is ground\nX85 is free", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: flatten(cons(T63, cons(T64, T65)), X85), SCOPE: 4, CLAUSE: 2\n\nT63 is ground\nT64 is ground\nT65 is ground\nX85 is free", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: flatten(cons(T79, T80), X108)\n\nT79 is ground\nT80 is ground\nX108 is free", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: flatten(cons(T79, T80), X108), SCOPE: 5, CLAUSE: 0 | flatten(cons(T79, T80), X108), SCOPE: 5, CLAUSE: 1 | flatten(cons(T79, T80), X108), SCOPE: 5, CLAUSE: 2\n\nT79 is ground\nT80 is ground\nX108 is free", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: flatten(cons(T79, T80), X108), SCOPE: 5, CLAUSE: 1 | flatten(cons(T79, T80), X108), SCOPE: 5, CLAUSE: 2\n\nT79 is ground\nT80 is ground\nX108 is free", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: flatten(cons(T79, T80), X108), SCOPE: 5, CLAUSE: 1\n\nT79 is ground\nT80 is ground\nX108 is free", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: flatten(cons(T79, T80), X108), SCOPE: 5, CLAUSE: 2\n\nT79 is ground\nT80 is ground\nX108 is free", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="D: flatten(T90, X131)\n\nT90 is ground\nX131 is free", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: flatten(T90, X131), SCOPE: 6, CLAUSE: 0 | flatten(T90, X131), SCOPE: 6, CLAUSE: 1 | flatten(T90, X131), SCOPE: 6, CLAUSE: 2\n\nT90 is ground\nX131 is free", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: flatten(T90, X131), SCOPE: 6, CLAUSE: 0\n\nT90 is ground\nX131 is free", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: flatten(T90, X131), SCOPE: 6, CLAUSE: 1 | flatten(T90, X131), SCOPE: 6, CLAUSE: 2\n\nT90 is ground\nX131 is free", fontsize=16, style=filled, fillcolor=lightyellow];
145 [label="145: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
146 [label="146: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
147 [label="147: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
148 [label="148: flatten(T90, X131), SCOPE: 6, CLAUSE: 1\n\nT90 is ground\nX131 is free", fontsize=16, style=filled, fillcolor=lightyellow];
149 [label="149: flatten(T90, X131), SCOPE: 6, CLAUSE: 2\n\nT90 is ground\nX131 is free", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: flatten(T107, X158)\n\nT107 is ground\nX158 is free", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="153: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: flatten(cons(T116, cons(T117, T118)), X175)\n\nT116 is ground\nT117 is ground\nT118 is ground\nX175 is free", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
168 [label="168: flatten(cons(T125, cons(T126, T127)), X192)\n\nT125 is ground\nT126 is ground\nT127 is ground\nX192 is free", fontsize=16, style=filled, fillcolor=lightyellow];
169 [label="169: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
170 [label="170: flatten(cons(T136, cons(T137, cons(T138, T139))), X209)\n\nT136 is ground\nT137 is ground\nT138 is ground\nT139 is ground\nX209 is free", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="171: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: count(cons(atom(T8), T9), T2), SCOPE: 1, CLAUSE: 5\n\nT8 is ground\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: ','(flatten(cons(cons(T146, T147), T148), X226), count(X226, T150))\n\nT146 is ground\nT147 is ground\nT148 is ground\nX226 is free", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: ','(flatten(cons(cons(T146, T147), T148), X226), count(X226, T150)), SCOPE: 7, CLAUSE: 0 | ','(flatten(cons(cons(T146, T147), T148), X226), count(X226, T150)), SCOPE: 7, CLAUSE: 1 | ','(flatten(cons(cons(T146, T147), T148), X226), count(X226, T150)), SCOPE: 7, CLAUSE: 2\n\nT146 is ground\nT147 is ground\nT148 is ground\nX226 is free", fontsize=16, style=filled, fillcolor=lightyellow];
177 [label="177: ','(flatten(cons(cons(T146, T147), T148), X226), count(X226, T150)), SCOPE: 7, CLAUSE: 1 | ','(flatten(cons(cons(T146, T147), T148), X226), count(X226, T150)), SCOPE: 7, CLAUSE: 2\n\nT146 is ground\nT147 is ground\nT148 is ground\nX226 is free", fontsize=16, style=filled, fillcolor=lightyellow];
178 [label="178: ','(flatten(cons(cons(T146, T147), T148), X226), count(X226, T150)), SCOPE: 7, CLAUSE: 2\n\nT146 is ground\nT147 is ground\nT148 is ground\nX226 is free", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="C: ','(flatten(cons(T157, cons(T158, T159)), X247), count(X247, T150))\n\nT157 is ground\nT158 is ground\nT159 is ground\nX247 is free", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: flatten(cons(T157, cons(T158, T159)), X247)\n\nT157 is ground\nT158 is ground\nT159 is ground\nX247 is free", fontsize=16, style=filled, fillcolor=lightyellow];
181 [label="181: count(T160, T150)\n\nT160 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 182 [arrowhead = none ];
182 -> 4;

183 [label="EVAL with clause\ncount(atom(X2), s(0)).\nand substitutionX2 -> T4,\nT1 -> atom(T4),\nT2 -> s(0)", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 183 [arrowhead = none ];
183 -> 11;

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

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

186 [label="EVAL with clause\ncount(cons(atom(X13), X14), s(X15)) :- count(X14, X15).\nand substitutionX13 -> T8,\nX14 -> T9,\nT1 -> cons(atom(T8), T9),\nX15 -> T11,\nT2 -> s(T11),\nT10 -> T11", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 186 [arrowhead = none ];
186 -> 25;

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

188 [label="BACKTRACK\nfor clause: count(cons(atom(X), Y), s(Z)) :- count(Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 188 [arrowhead = none ];
188 -> 18;

189 [label="BACKTRACK\nfor clause: count(cons(cons(U, V), W), Z) :- ','(flatten(cons(cons(U, V), W), X), count(X, Z))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
18 -> 189 [arrowhead = none ];
189 -> 23;

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

191 [label="EVAL with clause\ncount(cons(cons(X222, X223), X224), X225) :- ','(flatten(cons(cons(X222, X223), X224), X226), count(X226, X225)).\nand substitutionX222 -> T146,\nX223 -> T147,\nX224 -> T148,\nT1 -> cons(cons(T146, T147), T148),\nT2 -> T150,\nX225 -> T150,\nT149 -> T150", fontsize=14, style = filled, fillcolor = lightblue];
29 -> 191 [arrowhead = none ];
191 -> 174;

192 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
29 -> 192 [arrowhead = none ];
192 -> 175;

193 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
31 -> 193 [arrowhead = none ];
193 -> 34;

194 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
31 -> 194 [arrowhead = none ];
194 -> 36;

195 [label="EVAL with clause\ncount(atom(X20), s(0)).\nand substitutionX20 -> T16,\nT9 -> atom(T16),\nT11 -> s(0)", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 195 [arrowhead = none ];
195 -> 39;

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

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

198 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
36 -> 198 [arrowhead = none ];
198 -> 45;

199 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 199 [arrowhead = none ];
199 -> 41;

200 [label="EVAL with clause\ncount(cons(atom(X33), X34), s(X35)) :- count(X34, X35).\nand substitutionX33 -> T29,\nX34 -> T30,\nT9 -> cons(atom(T29), T30),\nX35 -> T32,\nT11 -> s(T32),\nT31 -> T32", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 200 [arrowhead = none ];
200 -> 50;

201 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
44 -> 201 [arrowhead = none ];
201 -> 51;

202 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
45 -> 202 [arrowhead = none ];
202 -> 59;

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

204 [label="INSTANCE with matching:\nT1 -> T30\nT2 -> T32", fontsize=14, style = filled, fillcolor = lightgrey];
50 -> 204 [arrowhead = none , style=dashed];
204 -> 3[style=dashed];

205 [label="EVAL with clause\ncount(cons(cons(X56, X57), X58), X59) :- ','(flatten(cons(cons(X56, X57), X58), X60), count(X60, X59)).\nand substitutionX56 -> T51,\nX57 -> T52,\nX58 -> T53,\nT9 -> cons(cons(T51, T52), T53),\nT11 -> T55,\nX59 -> T55,\nT54 -> T55", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 205 [arrowhead = none ];
205 -> 71;

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

207 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
60 -> 207 [arrowhead = none ];
207 -> 172;

208 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
71 -> 208 [arrowhead = none ];
208 -> 73;

209 [label="SPLIT 2\nnew knowledge:\nT51 is ground\nT52 is ground\nT53 is ground\nT56 is ground\nreplacements:X60 -> T56", fontsize=14, style = filled, fillcolor = violet];
71 -> 209 [arrowhead = none ];
209 -> 74;

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

211 [label="INSTANCE with matching:\nT1 -> T56\nT2 -> T55", fontsize=14, style = filled, fillcolor = lightgrey];
74 -> 211 [arrowhead = none , style=dashed];
211 -> 3[style=dashed];

212 [label="BACKTRACK\nfor clause: flatten(atom(X), .(X, []))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
77 -> 212 [arrowhead = none ];
212 -> 78;

213 [label="BACKTRACK\nfor clause: flatten(cons(atom(X), U), .(X, Y)) :- flatten(U, Y)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
78 -> 213 [arrowhead = none ];
213 -> 79;

214 [label="ONLY EVAL with clause\nflatten(cons(cons(X81, X82), X83), X84) :- flatten(cons(X81, cons(X82, X83)), X84).\nand substitutionT51 -> T63,\nX81 -> T63,\nT52 -> T64,\nX82 -> T64,\nT53 -> T65,\nX83 -> T65,\nX60 -> X85,\nX84 -> X85", fontsize=14, style = filled, fillcolor = lightblue];
79 -> 214 [arrowhead = none ];
214 -> 88;

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

216 [label="BACKTRACK\nfor clause: flatten(atom(X), .(X, []))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
90 -> 216 [arrowhead = none ];
216 -> 93;

217 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
93 -> 217 [arrowhead = none ];
217 -> 103;

218 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
93 -> 218 [arrowhead = none ];
218 -> 104;

219 [label="EVAL with clause\nflatten(cons(atom(X105), X106), .(X105, X107)) :- flatten(X106, X107).\nand substitutionX105 -> T78,\nT63 -> atom(T78),\nT64 -> T79,\nT65 -> T80,\nX106 -> cons(T79, T80),\nX107 -> X108,\nX85 -> .(T78, X108)", fontsize=14, style = filled, fillcolor = lightblue];
103 -> 219 [arrowhead = none ];
219 -> 113;

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

221 [label="EVAL with clause\nflatten(cons(cons(X205, X206), X207), X208) :- flatten(cons(X205, cons(X206, X207)), X208).\nand substitutionX205 -> T136,\nX206 -> T137,\nT63 -> cons(T136, T137),\nT64 -> T138,\nT65 -> T139,\nX207 -> cons(T138, T139),\nX85 -> X209,\nX208 -> X209", fontsize=14, style = filled, fillcolor = lightblue];
104 -> 221 [arrowhead = none ];
221 -> 170;

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

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

224 [label="BACKTRACK\nfor clause: flatten(atom(X), .(X, []))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
118 -> 224 [arrowhead = none ];
224 -> 120;

225 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
120 -> 225 [arrowhead = none ];
225 -> 123;

226 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
120 -> 226 [arrowhead = none ];
226 -> 124;

227 [label="EVAL with clause\nflatten(cons(atom(X128), X129), .(X128, X130)) :- flatten(X129, X130).\nand substitutionX128 -> T89,\nT79 -> atom(T89),\nT80 -> T90,\nX129 -> T90,\nX130 -> X131,\nX108 -> .(T89, X131)", fontsize=14, style = filled, fillcolor = lightblue];
123 -> 227 [arrowhead = none ];
227 -> 132;

228 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
123 -> 228 [arrowhead = none ];
228 -> 133;

229 [label="EVAL with clause\nflatten(cons(cons(X188, X189), X190), X191) :- flatten(cons(X188, cons(X189, X190)), X191).\nand substitutionX188 -> T125,\nX189 -> T126,\nT79 -> cons(T125, T126),\nT80 -> T127,\nX190 -> T127,\nX108 -> X192,\nX191 -> X192", fontsize=14, style = filled, fillcolor = lightblue];
124 -> 229 [arrowhead = none ];
229 -> 168;

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

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

232 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
134 -> 232 [arrowhead = none ];
232 -> 143;

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

234 [label="EVAL with clause\nflatten(atom(X138), .(X138, [])).\nand substitutionX138 -> T97,\nT90 -> atom(T97),\nX131 -> .(T97, [])", fontsize=14, style = filled, fillcolor = lightblue];
143 -> 234 [arrowhead = none ];
234 -> 145;

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

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

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

238 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
145 -> 238 [arrowhead = none ];
238 -> 147;

239 [label="EVAL with clause\nflatten(cons(atom(X155), X156), .(X155, X157)) :- flatten(X156, X157).\nand substitutionX155 -> T106,\nX156 -> T107,\nT90 -> cons(atom(T106), T107),\nX157 -> X158,\nX131 -> .(T106, X158)", fontsize=14, style = filled, fillcolor = lightblue];
148 -> 239 [arrowhead = none ];
239 -> 152;

240 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
148 -> 240 [arrowhead = none ];
240 -> 153;

241 [label="EVAL with clause\nflatten(cons(cons(X171, X172), X173), X174) :- flatten(cons(X171, cons(X172, X173)), X174).\nand substitutionX171 -> T116,\nX172 -> T117,\nX173 -> T118,\nT90 -> cons(cons(T116, T117), T118),\nX131 -> X175,\nX174 -> X175", fontsize=14, style = filled, fillcolor = lightblue];
149 -> 241 [arrowhead = none ];
241 -> 162;

242 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
149 -> 242 [arrowhead = none ];
242 -> 163;

243 [label="INSTANCE with matching:\nT90 -> T107\nX131 -> X158", fontsize=14, style = filled, fillcolor = lightgrey];
152 -> 243 [arrowhead = none , style=dashed];
243 -> 132[style=dashed];

244 [label="INSTANCE with matching:\nT63 -> T116\nT64 -> T117\nT65 -> T118\nX85 -> X175", fontsize=14, style = filled, fillcolor = lightgrey];
162 -> 244 [arrowhead = none , style=dashed];
244 -> 88[style=dashed];

245 [label="INSTANCE with matching:\nT63 -> T125\nT64 -> T126\nT65 -> T127\nX85 -> X192", fontsize=14, style = filled, fillcolor = lightgrey];
168 -> 245 [arrowhead = none , style=dashed];
245 -> 88[style=dashed];

246 [label="INSTANCE with matching:\nT63 -> T136\nT64 -> T137\nT65 -> cons(T138, T139)\nX85 -> X209", fontsize=14, style = filled, fillcolor = lightgrey];
170 -> 246 [arrowhead = none , style=dashed];
246 -> 88[style=dashed];

247 [label="BACKTRACK\nfor clause: count(cons(cons(U, V), W), Z) :- ','(flatten(cons(cons(U, V), W), X), count(X, Z))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
172 -> 247 [arrowhead = none ];
247 -> 173;

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

249 [label="BACKTRACK\nfor clause: flatten(atom(X), .(X, []))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
176 -> 249 [arrowhead = none ];
249 -> 177;

250 [label="BACKTRACK\nfor clause: flatten(cons(atom(X), U), .(X, Y)) :- flatten(U, Y)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
177 -> 250 [arrowhead = none ];
250 -> 178;

251 [label="ONLY EVAL with clause\nflatten(cons(cons(X243, X244), X245), X246) :- flatten(cons(X243, cons(X244, X245)), X246).\nand substitutionT146 -> T157,\nX243 -> T157,\nT147 -> T158,\nX244 -> T158,\nT148 -> T159,\nX245 -> T159,\nX226 -> X247,\nX246 -> X247", fontsize=14, style = filled, fillcolor = lightblue];
178 -> 251 [arrowhead = none ];
251 -> 179;

252 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
179 -> 252 [arrowhead = none ];
252 -> 180;

253 [label="SPLIT 2\nnew knowledge:\nT157 is ground\nT158 is ground\nT159 is ground\nT160 is ground\nreplacements:X247 -> T160", fontsize=14, style = filled, fillcolor = violet];
179 -> 253 [arrowhead = none ];
253 -> 181;

254 [label="INSTANCE with matching:\nT63 -> T157\nT64 -> T158\nT65 -> T159\nX85 -> X247", fontsize=14, style = filled, fillcolor = lightgrey];
180 -> 254 [arrowhead = none , style=dashed];
254 -> 88[style=dashed];

255 [label="INSTANCE with matching:\nT1 -> T160\nT2 -> T150", fontsize=14, style = filled, fillcolor = lightgrey];
181 -> 255 [arrowhead = none , style=dashed];
255 -> 3[style=dashed];

}

(2) Obligation:

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

countA_in_ga(atom(T4), s(0)) → countA_out_ga(atom(T4), s(0))
countA_in_ga(cons(atom(T8), atom(T16)), s(s(0))) → countA_out_ga(cons(atom(T8), atom(T16)), s(s(0)))
countA_in_ga(cons(atom(T8), cons(atom(T29), T30)), s(s(T32))) → U1_ga(T8, T29, T30, T32, countA_in_ga(T30, T32))
countA_in_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → U2_ga(T8, T51, T52, T53, T55, pB_in_gggaa(T51, T52, T53, X60, T55))
pB_in_gggaa(T51, T52, T53, T56, T55) → U10_gggaa(T51, T52, T53, T56, T55, flattenF_in_ggga(T51, T52, T53, T56))
flattenF_in_ggga(T63, T64, T65, X85) → U9_ggga(T63, T64, T65, X85, flattenE_in_ggga(T63, T64, T65, X85))
flattenE_in_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131))) → U6_ggga(T78, T89, T90, X131, flattenD_in_ga(T90, X131))
flattenD_in_ga(atom(T97), .(T97, [])) → flattenD_out_ga(atom(T97), .(T97, []))
flattenD_in_ga(cons(atom(T106), T107), .(T106, X158)) → U4_ga(T106, T107, X158, flattenD_in_ga(T107, X158))
flattenD_in_ga(cons(cons(T116, T117), T118), X175) → U5_ga(T116, T117, T118, X175, flattenE_in_ggga(T116, T117, T118, X175))
flattenE_in_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192)) → U7_ggga(T78, T125, T126, T127, X192, flattenE_in_ggga(T125, T126, T127, X192))
flattenE_in_ggga(cons(T136, T137), T138, T139, X209) → U8_ggga(T136, T137, T138, T139, X209, flattenE_in_ggga(T136, T137, cons(T138, T139), X209))
U8_ggga(T136, T137, T138, T139, X209, flattenE_out_ggga(T136, T137, cons(T138, T139), X209)) → flattenE_out_ggga(cons(T136, T137), T138, T139, X209)
U7_ggga(T78, T125, T126, T127, X192, flattenE_out_ggga(T125, T126, T127, X192)) → flattenE_out_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192))
U5_ga(T116, T117, T118, X175, flattenE_out_ggga(T116, T117, T118, X175)) → flattenD_out_ga(cons(cons(T116, T117), T118), X175)
U4_ga(T106, T107, X158, flattenD_out_ga(T107, X158)) → flattenD_out_ga(cons(atom(T106), T107), .(T106, X158))
U6_ggga(T78, T89, T90, X131, flattenD_out_ga(T90, X131)) → flattenE_out_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131)))
U9_ggga(T63, T64, T65, X85, flattenE_out_ggga(T63, T64, T65, X85)) → flattenF_out_ggga(T63, T64, T65, X85)
U10_gggaa(T51, T52, T53, T56, T55, flattenF_out_ggga(T51, T52, T53, T56)) → U11_gggaa(T51, T52, T53, T56, T55, countA_in_ga(T56, T55))
countA_in_ga(cons(cons(T157, T158), T159), T150) → U3_ga(T157, T158, T159, T150, pC_in_gggaa(T157, T158, T159, X247, T150))
pC_in_gggaa(T157, T158, T159, T160, T150) → U12_gggaa(T157, T158, T159, T160, T150, flattenE_in_ggga(T157, T158, T159, T160))
U12_gggaa(T157, T158, T159, T160, T150, flattenE_out_ggga(T157, T158, T159, T160)) → U13_gggaa(T157, T158, T159, T160, T150, countA_in_ga(T160, T150))
U13_gggaa(T157, T158, T159, T160, T150, countA_out_ga(T160, T150)) → pC_out_gggaa(T157, T158, T159, T160, T150)
U3_ga(T157, T158, T159, T150, pC_out_gggaa(T157, T158, T159, X247, T150)) → countA_out_ga(cons(cons(T157, T158), T159), T150)
U11_gggaa(T51, T52, T53, T56, T55, countA_out_ga(T56, T55)) → pB_out_gggaa(T51, T52, T53, T56, T55)
U2_ga(T8, T51, T52, T53, T55, pB_out_gggaa(T51, T52, T53, X60, T55)) → countA_out_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55))
U1_ga(T8, T29, T30, T32, countA_out_ga(T30, T32)) → countA_out_ga(cons(atom(T8), cons(atom(T29), T30)), s(s(T32)))

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

COUNTA_IN_GA(cons(atom(T8), cons(atom(T29), T30)), s(s(T32))) → U1_GA(T8, T29, T30, T32, countA_in_ga(T30, T32))
COUNTA_IN_GA(cons(atom(T8), cons(atom(T29), T30)), s(s(T32))) → COUNTA_IN_GA(T30, T32)
COUNTA_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → U2_GA(T8, T51, T52, T53, T55, pB_in_gggaa(T51, T52, T53, X60, T55))
COUNTA_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → PB_IN_GGGAA(T51, T52, T53, X60, T55)
PB_IN_GGGAA(T51, T52, T53, T56, T55) → U10_GGGAA(T51, T52, T53, T56, T55, flattenF_in_ggga(T51, T52, T53, T56))
PB_IN_GGGAA(T51, T52, T53, T56, T55) → FLATTENF_IN_GGGA(T51, T52, T53, T56)
FLATTENF_IN_GGGA(T63, T64, T65, X85) → U9_GGGA(T63, T64, T65, X85, flattenE_in_ggga(T63, T64, T65, X85))
FLATTENF_IN_GGGA(T63, T64, T65, X85) → FLATTENE_IN_GGGA(T63, T64, T65, X85)
FLATTENE_IN_GGGA(atom(T78), atom(T89), T90, .(T78, .(T89, X131))) → U6_GGGA(T78, T89, T90, X131, flattenD_in_ga(T90, X131))
FLATTENE_IN_GGGA(atom(T78), atom(T89), T90, .(T78, .(T89, X131))) → FLATTEND_IN_GA(T90, X131)
FLATTEND_IN_GA(cons(atom(T106), T107), .(T106, X158)) → U4_GA(T106, T107, X158, flattenD_in_ga(T107, X158))
FLATTEND_IN_GA(cons(atom(T106), T107), .(T106, X158)) → FLATTEND_IN_GA(T107, X158)
FLATTEND_IN_GA(cons(cons(T116, T117), T118), X175) → U5_GA(T116, T117, T118, X175, flattenE_in_ggga(T116, T117, T118, X175))
FLATTEND_IN_GA(cons(cons(T116, T117), T118), X175) → FLATTENE_IN_GGGA(T116, T117, T118, X175)
FLATTENE_IN_GGGA(atom(T78), cons(T125, T126), T127, .(T78, X192)) → U7_GGGA(T78, T125, T126, T127, X192, flattenE_in_ggga(T125, T126, T127, X192))
FLATTENE_IN_GGGA(atom(T78), cons(T125, T126), T127, .(T78, X192)) → FLATTENE_IN_GGGA(T125, T126, T127, X192)
FLATTENE_IN_GGGA(cons(T136, T137), T138, T139, X209) → U8_GGGA(T136, T137, T138, T139, X209, flattenE_in_ggga(T136, T137, cons(T138, T139), X209))
FLATTENE_IN_GGGA(cons(T136, T137), T138, T139, X209) → FLATTENE_IN_GGGA(T136, T137, cons(T138, T139), X209)
U10_GGGAA(T51, T52, T53, T56, T55, flattenF_out_ggga(T51, T52, T53, T56)) → U11_GGGAA(T51, T52, T53, T56, T55, countA_in_ga(T56, T55))
U10_GGGAA(T51, T52, T53, T56, T55, flattenF_out_ggga(T51, T52, T53, T56)) → COUNTA_IN_GA(T56, T55)
COUNTA_IN_GA(cons(cons(T157, T158), T159), T150) → U3_GA(T157, T158, T159, T150, pC_in_gggaa(T157, T158, T159, X247, T150))
COUNTA_IN_GA(cons(cons(T157, T158), T159), T150) → PC_IN_GGGAA(T157, T158, T159, X247, T150)
PC_IN_GGGAA(T157, T158, T159, T160, T150) → U12_GGGAA(T157, T158, T159, T160, T150, flattenE_in_ggga(T157, T158, T159, T160))
PC_IN_GGGAA(T157, T158, T159, T160, T150) → FLATTENE_IN_GGGA(T157, T158, T159, T160)
U12_GGGAA(T157, T158, T159, T160, T150, flattenE_out_ggga(T157, T158, T159, T160)) → U13_GGGAA(T157, T158, T159, T160, T150, countA_in_ga(T160, T150))
U12_GGGAA(T157, T158, T159, T160, T150, flattenE_out_ggga(T157, T158, T159, T160)) → COUNTA_IN_GA(T160, T150)

The TRS R consists of the following rules:

countA_in_ga(atom(T4), s(0)) → countA_out_ga(atom(T4), s(0))
countA_in_ga(cons(atom(T8), atom(T16)), s(s(0))) → countA_out_ga(cons(atom(T8), atom(T16)), s(s(0)))
countA_in_ga(cons(atom(T8), cons(atom(T29), T30)), s(s(T32))) → U1_ga(T8, T29, T30, T32, countA_in_ga(T30, T32))
countA_in_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → U2_ga(T8, T51, T52, T53, T55, pB_in_gggaa(T51, T52, T53, X60, T55))
pB_in_gggaa(T51, T52, T53, T56, T55) → U10_gggaa(T51, T52, T53, T56, T55, flattenF_in_ggga(T51, T52, T53, T56))
flattenF_in_ggga(T63, T64, T65, X85) → U9_ggga(T63, T64, T65, X85, flattenE_in_ggga(T63, T64, T65, X85))
flattenE_in_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131))) → U6_ggga(T78, T89, T90, X131, flattenD_in_ga(T90, X131))
flattenD_in_ga(atom(T97), .(T97, [])) → flattenD_out_ga(atom(T97), .(T97, []))
flattenD_in_ga(cons(atom(T106), T107), .(T106, X158)) → U4_ga(T106, T107, X158, flattenD_in_ga(T107, X158))
flattenD_in_ga(cons(cons(T116, T117), T118), X175) → U5_ga(T116, T117, T118, X175, flattenE_in_ggga(T116, T117, T118, X175))
flattenE_in_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192)) → U7_ggga(T78, T125, T126, T127, X192, flattenE_in_ggga(T125, T126, T127, X192))
flattenE_in_ggga(cons(T136, T137), T138, T139, X209) → U8_ggga(T136, T137, T138, T139, X209, flattenE_in_ggga(T136, T137, cons(T138, T139), X209))
U8_ggga(T136, T137, T138, T139, X209, flattenE_out_ggga(T136, T137, cons(T138, T139), X209)) → flattenE_out_ggga(cons(T136, T137), T138, T139, X209)
U7_ggga(T78, T125, T126, T127, X192, flattenE_out_ggga(T125, T126, T127, X192)) → flattenE_out_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192))
U5_ga(T116, T117, T118, X175, flattenE_out_ggga(T116, T117, T118, X175)) → flattenD_out_ga(cons(cons(T116, T117), T118), X175)
U4_ga(T106, T107, X158, flattenD_out_ga(T107, X158)) → flattenD_out_ga(cons(atom(T106), T107), .(T106, X158))
U6_ggga(T78, T89, T90, X131, flattenD_out_ga(T90, X131)) → flattenE_out_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131)))
U9_ggga(T63, T64, T65, X85, flattenE_out_ggga(T63, T64, T65, X85)) → flattenF_out_ggga(T63, T64, T65, X85)
U10_gggaa(T51, T52, T53, T56, T55, flattenF_out_ggga(T51, T52, T53, T56)) → U11_gggaa(T51, T52, T53, T56, T55, countA_in_ga(T56, T55))
countA_in_ga(cons(cons(T157, T158), T159), T150) → U3_ga(T157, T158, T159, T150, pC_in_gggaa(T157, T158, T159, X247, T150))
pC_in_gggaa(T157, T158, T159, T160, T150) → U12_gggaa(T157, T158, T159, T160, T150, flattenE_in_ggga(T157, T158, T159, T160))
U12_gggaa(T157, T158, T159, T160, T150, flattenE_out_ggga(T157, T158, T159, T160)) → U13_gggaa(T157, T158, T159, T160, T150, countA_in_ga(T160, T150))
U13_gggaa(T157, T158, T159, T160, T150, countA_out_ga(T160, T150)) → pC_out_gggaa(T157, T158, T159, T160, T150)
U3_ga(T157, T158, T159, T150, pC_out_gggaa(T157, T158, T159, X247, T150)) → countA_out_ga(cons(cons(T157, T158), T159), T150)
U11_gggaa(T51, T52, T53, T56, T55, countA_out_ga(T56, T55)) → pB_out_gggaa(T51, T52, T53, T56, T55)
U2_ga(T8, T51, T52, T53, T55, pB_out_gggaa(T51, T52, T53, X60, T55)) → countA_out_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55))
U1_ga(T8, T29, T30, T32, countA_out_ga(T30, T32)) → countA_out_ga(cons(atom(T8), cons(atom(T29), T30)), s(s(T32)))

The argument filtering Pi contains the following mapping:
countA_in_ga(x1, x2) = countA_in_ga(x1)
atom(x1) = atom(x1)
countA_out_ga(x1, x2) = countA_out_ga(x1, x2)
cons(x1, x2) = cons(x1, x2)
U1_ga(x1, x2, x3, x4, x5) = U1_ga(x1, x2, x3, x5)
U2_ga(x1, x2, x3, x4, x5, x6) = U2_ga(x1, x2, x3, x4, x6)
pB_in_gggaa(x1, x2, x3, x4, x5) = pB_in_gggaa(x1, x2, x3)
U10_gggaa(x1, x2, x3, x4, x5, x6) = U10_gggaa(x1, x2, x3, x6)
flattenF_in_ggga(x1, x2, x3, x4) = flattenF_in_ggga(x1, x2, x3)
U9_ggga(x1, x2, x3, x4, x5) = U9_ggga(x1, x2, x3, x5)
flattenE_in_ggga(x1, x2, x3, x4) = flattenE_in_ggga(x1, x2, x3)
U6_ggga(x1, x2, x3, x4, x5) = U6_ggga(x1, x2, x3, x5)
flattenD_in_ga(x1, x2) = flattenD_in_ga(x1)
flattenD_out_ga(x1, x2) = flattenD_out_ga(x1, x2)
U4_ga(x1, x2, x3, x4) = U4_ga(x1, x2, x4)
U5_ga(x1, x2, x3, x4, x5) = U5_ga(x1, x2, x3, x5)
U7_ggga(x1, x2, x3, x4, x5, x6) = U7_ggga(x1, x2, x3, x4, x6)
U8_ggga(x1, x2, x3, x4, x5, x6) = U8_ggga(x1, x2, x3, x4, x6)
flattenE_out_ggga(x1, x2, x3, x4) = flattenE_out_ggga(x1, x2, x3, x4)
flattenF_out_ggga(x1, x2, x3, x4) = flattenF_out_ggga(x1, x2, x3, x4)
U11_gggaa(x1, x2, x3, x4, x5, x6) = U11_gggaa(x1, x2, x3, x4, x6)
U3_ga(x1, x2, x3, x4, x5) = U3_ga(x1, x2, x3, x5)
pC_in_gggaa(x1, x2, x3, x4, x5) = pC_in_gggaa(x1, x2, x3)
U12_gggaa(x1, x2, x3, x4, x5, x6) = U12_gggaa(x1, x2, x3, x6)
U13_gggaa(x1, x2, x3, x4, x5, x6) = U13_gggaa(x1, x2, x3, x4, x6)
pC_out_gggaa(x1, x2, x3, x4, x5) = pC_out_gggaa(x1, x2, x3, x4, x5)
pB_out_gggaa(x1, x2, x3, x4, x5) = pB_out_gggaa(x1, x2, x3, x4, x5)
.(x1, x2) = .(x1, x2)
s(x1) = s(x1)
COUNTA_IN_GA(x1, x2) = COUNTA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5) = U1_GA(x1, x2, x3, x5)
U2_GA(x1, x2, x3, x4, x5, x6) = U2_GA(x1, x2, x3, x4, x6)
PB_IN_GGGAA(x1, x2, x3, x4, x5) = PB_IN_GGGAA(x1, x2, x3)
U10_GGGAA(x1, x2, x3, x4, x5, x6) = U10_GGGAA(x1, x2, x3, x6)
FLATTENF_IN_GGGA(x1, x2, x3, x4) = FLATTENF_IN_GGGA(x1, x2, x3)
U9_GGGA(x1, x2, x3, x4, x5) = U9_GGGA(x1, x2, x3, x5)
FLATTENE_IN_GGGA(x1, x2, x3, x4) = FLATTENE_IN_GGGA(x1, x2, x3)
U6_GGGA(x1, x2, x3, x4, x5) = U6_GGGA(x1, x2, x3, x5)
FLATTEND_IN_GA(x1, x2) = FLATTEND_IN_GA(x1)
U4_GA(x1, x2, x3, x4) = U4_GA(x1, x2, x4)
U5_GA(x1, x2, x3, x4, x5) = U5_GA(x1, x2, x3, x5)
U7_GGGA(x1, x2, x3, x4, x5, x6) = U7_GGGA(x1, x2, x3, x4, x6)
U8_GGGA(x1, x2, x3, x4, x5, x6) = U8_GGGA(x1, x2, x3, x4, x6)
U11_GGGAA(x1, x2, x3, x4, x5, x6) = U11_GGGAA(x1, x2, x3, x4, x6)
U3_GA(x1, x2, x3, x4, x5) = U3_GA(x1, x2, x3, x5)
PC_IN_GGGAA(x1, x2, x3, x4, x5) = PC_IN_GGGAA(x1, x2, x3)
U12_GGGAA(x1, x2, x3, x4, x5, x6) = U12_GGGAA(x1, x2, x3, x6)
U13_GGGAA(x1, x2, x3, x4, x5, x6) = U13_GGGAA(x1, x2, x3, x4, x6)

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

(4) Obligation:

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

COUNTA_IN_GA(cons(atom(T8), cons(atom(T29), T30)), s(s(T32))) → U1_GA(T8, T29, T30, T32, countA_in_ga(T30, T32))
COUNTA_IN_GA(cons(atom(T8), cons(atom(T29), T30)), s(s(T32))) → COUNTA_IN_GA(T30, T32)
COUNTA_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → U2_GA(T8, T51, T52, T53, T55, pB_in_gggaa(T51, T52, T53, X60, T55))
COUNTA_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → PB_IN_GGGAA(T51, T52, T53, X60, T55)
PB_IN_GGGAA(T51, T52, T53, T56, T55) → U10_GGGAA(T51, T52, T53, T56, T55, flattenF_in_ggga(T51, T52, T53, T56))
PB_IN_GGGAA(T51, T52, T53, T56, T55) → FLATTENF_IN_GGGA(T51, T52, T53, T56)
FLATTENF_IN_GGGA(T63, T64, T65, X85) → U9_GGGA(T63, T64, T65, X85, flattenE_in_ggga(T63, T64, T65, X85))
FLATTENF_IN_GGGA(T63, T64, T65, X85) → FLATTENE_IN_GGGA(T63, T64, T65, X85)
FLATTENE_IN_GGGA(atom(T78), atom(T89), T90, .(T78, .(T89, X131))) → U6_GGGA(T78, T89, T90, X131, flattenD_in_ga(T90, X131))
FLATTENE_IN_GGGA(atom(T78), atom(T89), T90, .(T78, .(T89, X131))) → FLATTEND_IN_GA(T90, X131)
FLATTEND_IN_GA(cons(atom(T106), T107), .(T106, X158)) → U4_GA(T106, T107, X158, flattenD_in_ga(T107, X158))
FLATTEND_IN_GA(cons(atom(T106), T107), .(T106, X158)) → FLATTEND_IN_GA(T107, X158)
FLATTEND_IN_GA(cons(cons(T116, T117), T118), X175) → U5_GA(T116, T117, T118, X175, flattenE_in_ggga(T116, T117, T118, X175))
FLATTEND_IN_GA(cons(cons(T116, T117), T118), X175) → FLATTENE_IN_GGGA(T116, T117, T118, X175)
FLATTENE_IN_GGGA(atom(T78), cons(T125, T126), T127, .(T78, X192)) → U7_GGGA(T78, T125, T126, T127, X192, flattenE_in_ggga(T125, T126, T127, X192))
FLATTENE_IN_GGGA(atom(T78), cons(T125, T126), T127, .(T78, X192)) → FLATTENE_IN_GGGA(T125, T126, T127, X192)
FLATTENE_IN_GGGA(cons(T136, T137), T138, T139, X209) → U8_GGGA(T136, T137, T138, T139, X209, flattenE_in_ggga(T136, T137, cons(T138, T139), X209))
FLATTENE_IN_GGGA(cons(T136, T137), T138, T139, X209) → FLATTENE_IN_GGGA(T136, T137, cons(T138, T139), X209)
U10_GGGAA(T51, T52, T53, T56, T55, flattenF_out_ggga(T51, T52, T53, T56)) → U11_GGGAA(T51, T52, T53, T56, T55, countA_in_ga(T56, T55))
U10_GGGAA(T51, T52, T53, T56, T55, flattenF_out_ggga(T51, T52, T53, T56)) → COUNTA_IN_GA(T56, T55)
COUNTA_IN_GA(cons(cons(T157, T158), T159), T150) → U3_GA(T157, T158, T159, T150, pC_in_gggaa(T157, T158, T159, X247, T150))
COUNTA_IN_GA(cons(cons(T157, T158), T159), T150) → PC_IN_GGGAA(T157, T158, T159, X247, T150)
PC_IN_GGGAA(T157, T158, T159, T160, T150) → U12_GGGAA(T157, T158, T159, T160, T150, flattenE_in_ggga(T157, T158, T159, T160))
PC_IN_GGGAA(T157, T158, T159, T160, T150) → FLATTENE_IN_GGGA(T157, T158, T159, T160)
U12_GGGAA(T157, T158, T159, T160, T150, flattenE_out_ggga(T157, T158, T159, T160)) → U13_GGGAA(T157, T158, T159, T160, T150, countA_in_ga(T160, T150))
U12_GGGAA(T157, T158, T159, T160, T150, flattenE_out_ggga(T157, T158, T159, T160)) → COUNTA_IN_GA(T160, T150)

The TRS R consists of the following rules:

countA_in_ga(atom(T4), s(0)) → countA_out_ga(atom(T4), s(0))
countA_in_ga(cons(atom(T8), atom(T16)), s(s(0))) → countA_out_ga(cons(atom(T8), atom(T16)), s(s(0)))
countA_in_ga(cons(atom(T8), cons(atom(T29), T30)), s(s(T32))) → U1_ga(T8, T29, T30, T32, countA_in_ga(T30, T32))
countA_in_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → U2_ga(T8, T51, T52, T53, T55, pB_in_gggaa(T51, T52, T53, X60, T55))
pB_in_gggaa(T51, T52, T53, T56, T55) → U10_gggaa(T51, T52, T53, T56, T55, flattenF_in_ggga(T51, T52, T53, T56))
flattenF_in_ggga(T63, T64, T65, X85) → U9_ggga(T63, T64, T65, X85, flattenE_in_ggga(T63, T64, T65, X85))
flattenE_in_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131))) → U6_ggga(T78, T89, T90, X131, flattenD_in_ga(T90, X131))
flattenD_in_ga(atom(T97), .(T97, [])) → flattenD_out_ga(atom(T97), .(T97, []))
flattenD_in_ga(cons(atom(T106), T107), .(T106, X158)) → U4_ga(T106, T107, X158, flattenD_in_ga(T107, X158))
flattenD_in_ga(cons(cons(T116, T117), T118), X175) → U5_ga(T116, T117, T118, X175, flattenE_in_ggga(T116, T117, T118, X175))
flattenE_in_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192)) → U7_ggga(T78, T125, T126, T127, X192, flattenE_in_ggga(T125, T126, T127, X192))
flattenE_in_ggga(cons(T136, T137), T138, T139, X209) → U8_ggga(T136, T137, T138, T139, X209, flattenE_in_ggga(T136, T137, cons(T138, T139), X209))
U8_ggga(T136, T137, T138, T139, X209, flattenE_out_ggga(T136, T137, cons(T138, T139), X209)) → flattenE_out_ggga(cons(T136, T137), T138, T139, X209)
U7_ggga(T78, T125, T126, T127, X192, flattenE_out_ggga(T125, T126, T127, X192)) → flattenE_out_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192))
U5_ga(T116, T117, T118, X175, flattenE_out_ggga(T116, T117, T118, X175)) → flattenD_out_ga(cons(cons(T116, T117), T118), X175)
U4_ga(T106, T107, X158, flattenD_out_ga(T107, X158)) → flattenD_out_ga(cons(atom(T106), T107), .(T106, X158))
U6_ggga(T78, T89, T90, X131, flattenD_out_ga(T90, X131)) → flattenE_out_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131)))
U9_ggga(T63, T64, T65, X85, flattenE_out_ggga(T63, T64, T65, X85)) → flattenF_out_ggga(T63, T64, T65, X85)
U10_gggaa(T51, T52, T53, T56, T55, flattenF_out_ggga(T51, T52, T53, T56)) → U11_gggaa(T51, T52, T53, T56, T55, countA_in_ga(T56, T55))
countA_in_ga(cons(cons(T157, T158), T159), T150) → U3_ga(T157, T158, T159, T150, pC_in_gggaa(T157, T158, T159, X247, T150))
pC_in_gggaa(T157, T158, T159, T160, T150) → U12_gggaa(T157, T158, T159, T160, T150, flattenE_in_ggga(T157, T158, T159, T160))
U12_gggaa(T157, T158, T159, T160, T150, flattenE_out_ggga(T157, T158, T159, T160)) → U13_gggaa(T157, T158, T159, T160, T150, countA_in_ga(T160, T150))
U13_gggaa(T157, T158, T159, T160, T150, countA_out_ga(T160, T150)) → pC_out_gggaa(T157, T158, T159, T160, T150)
U3_ga(T157, T158, T159, T150, pC_out_gggaa(T157, T158, T159, X247, T150)) → countA_out_ga(cons(cons(T157, T158), T159), T150)
U11_gggaa(T51, T52, T53, T56, T55, countA_out_ga(T56, T55)) → pB_out_gggaa(T51, T52, T53, T56, T55)
U2_ga(T8, T51, T52, T53, T55, pB_out_gggaa(T51, T52, T53, X60, T55)) → countA_out_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55))
U1_ga(T8, T29, T30, T32, countA_out_ga(T30, T32)) → countA_out_ga(cons(atom(T8), cons(atom(T29), T30)), s(s(T32)))

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

FLATTENE_IN_GGGA(atom(T78), atom(T89), T90, .(T78, .(T89, X131))) → FLATTEND_IN_GA(T90, X131)
FLATTEND_IN_GA(cons(atom(T106), T107), .(T106, X158)) → FLATTEND_IN_GA(T107, X158)
FLATTEND_IN_GA(cons(cons(T116, T117), T118), X175) → FLATTENE_IN_GGGA(T116, T117, T118, X175)
FLATTENE_IN_GGGA(atom(T78), cons(T125, T126), T127, .(T78, X192)) → FLATTENE_IN_GGGA(T125, T126, T127, X192)
FLATTENE_IN_GGGA(cons(T136, T137), T138, T139, X209) → FLATTENE_IN_GGGA(T136, T137, cons(T138, T139), X209)

The TRS R consists of the following rules:

countA_in_ga(atom(T4), s(0)) → countA_out_ga(atom(T4), s(0))
countA_in_ga(cons(atom(T8), atom(T16)), s(s(0))) → countA_out_ga(cons(atom(T8), atom(T16)), s(s(0)))
countA_in_ga(cons(atom(T8), cons(atom(T29), T30)), s(s(T32))) → U1_ga(T8, T29, T30, T32, countA_in_ga(T30, T32))
countA_in_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → U2_ga(T8, T51, T52, T53, T55, pB_in_gggaa(T51, T52, T53, X60, T55))
pB_in_gggaa(T51, T52, T53, T56, T55) → U10_gggaa(T51, T52, T53, T56, T55, flattenF_in_ggga(T51, T52, T53, T56))
flattenF_in_ggga(T63, T64, T65, X85) → U9_ggga(T63, T64, T65, X85, flattenE_in_ggga(T63, T64, T65, X85))
flattenE_in_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131))) → U6_ggga(T78, T89, T90, X131, flattenD_in_ga(T90, X131))
flattenD_in_ga(atom(T97), .(T97, [])) → flattenD_out_ga(atom(T97), .(T97, []))
flattenD_in_ga(cons(atom(T106), T107), .(T106, X158)) → U4_ga(T106, T107, X158, flattenD_in_ga(T107, X158))
flattenD_in_ga(cons(cons(T116, T117), T118), X175) → U5_ga(T116, T117, T118, X175, flattenE_in_ggga(T116, T117, T118, X175))
flattenE_in_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192)) → U7_ggga(T78, T125, T126, T127, X192, flattenE_in_ggga(T125, T126, T127, X192))
flattenE_in_ggga(cons(T136, T137), T138, T139, X209) → U8_ggga(T136, T137, T138, T139, X209, flattenE_in_ggga(T136, T137, cons(T138, T139), X209))
U8_ggga(T136, T137, T138, T139, X209, flattenE_out_ggga(T136, T137, cons(T138, T139), X209)) → flattenE_out_ggga(cons(T136, T137), T138, T139, X209)
U7_ggga(T78, T125, T126, T127, X192, flattenE_out_ggga(T125, T126, T127, X192)) → flattenE_out_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192))
U5_ga(T116, T117, T118, X175, flattenE_out_ggga(T116, T117, T118, X175)) → flattenD_out_ga(cons(cons(T116, T117), T118), X175)
U4_ga(T106, T107, X158, flattenD_out_ga(T107, X158)) → flattenD_out_ga(cons(atom(T106), T107), .(T106, X158))
U6_ggga(T78, T89, T90, X131, flattenD_out_ga(T90, X131)) → flattenE_out_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131)))
U9_ggga(T63, T64, T65, X85, flattenE_out_ggga(T63, T64, T65, X85)) → flattenF_out_ggga(T63, T64, T65, X85)
U10_gggaa(T51, T52, T53, T56, T55, flattenF_out_ggga(T51, T52, T53, T56)) → U11_gggaa(T51, T52, T53, T56, T55, countA_in_ga(T56, T55))
countA_in_ga(cons(cons(T157, T158), T159), T150) → U3_ga(T157, T158, T159, T150, pC_in_gggaa(T157, T158, T159, X247, T150))
pC_in_gggaa(T157, T158, T159, T160, T150) → U12_gggaa(T157, T158, T159, T160, T150, flattenE_in_ggga(T157, T158, T159, T160))
U12_gggaa(T157, T158, T159, T160, T150, flattenE_out_ggga(T157, T158, T159, T160)) → U13_gggaa(T157, T158, T159, T160, T150, countA_in_ga(T160, T150))
U13_gggaa(T157, T158, T159, T160, T150, countA_out_ga(T160, T150)) → pC_out_gggaa(T157, T158, T159, T160, T150)
U3_ga(T157, T158, T159, T150, pC_out_gggaa(T157, T158, T159, X247, T150)) → countA_out_ga(cons(cons(T157, T158), T159), T150)
U11_gggaa(T51, T52, T53, T56, T55, countA_out_ga(T56, T55)) → pB_out_gggaa(T51, T52, T53, T56, T55)
U2_ga(T8, T51, T52, T53, T55, pB_out_gggaa(T51, T52, T53, X60, T55)) → countA_out_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55))
U1_ga(T8, T29, T30, T32, countA_out_ga(T30, T32)) → countA_out_ga(cons(atom(T8), cons(atom(T29), T30)), s(s(T32)))

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

FLATTENE_IN_GGGA(atom(T78), atom(T89), T90, .(T78, .(T89, X131))) → FLATTEND_IN_GA(T90, X131)
FLATTEND_IN_GA(cons(atom(T106), T107), .(T106, X158)) → FLATTEND_IN_GA(T107, X158)
FLATTEND_IN_GA(cons(cons(T116, T117), T118), X175) → FLATTENE_IN_GGGA(T116, T117, T118, X175)
FLATTENE_IN_GGGA(atom(T78), cons(T125, T126), T127, .(T78, X192)) → FLATTENE_IN_GGGA(T125, T126, T127, X192)
FLATTENE_IN_GGGA(cons(T136, T137), T138, T139, X209) → FLATTENE_IN_GGGA(T136, T137, cons(T138, T139), X209)

R is empty.
The argument filtering Pi contains the following mapping:
atom(x1) = atom(x1)
cons(x1, x2) = cons(x1, x2)
.(x1, x2) = .(x1, x2)
FLATTENE_IN_GGGA(x1, x2, x3, x4) = FLATTENE_IN_GGGA(x1, x2, x3)
FLATTEND_IN_GA(x1, x2) = FLATTEND_IN_GA(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:

FLATTENE_IN_GGGA(atom(T78), atom(T89), T90) → FLATTEND_IN_GA(T90)
FLATTEND_IN_GA(cons(atom(T106), T107)) → FLATTEND_IN_GA(T107)
FLATTEND_IN_GA(cons(cons(T116, T117), T118)) → FLATTENE_IN_GGGA(T116, T117, T118)
FLATTENE_IN_GGGA(atom(T78), cons(T125, T126), T127) → FLATTENE_IN_GGGA(T125, T126, T127)
FLATTENE_IN_GGGA(cons(T136, T137), T138, T139) → FLATTENE_IN_GGGA(T136, T137, cons(T138, T139))

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

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

FLATTENE_IN_GGGA(atom(T78), atom(T89), T90) → FLATTEND_IN_GA(T90)
FLATTEND_IN_GA(cons(atom(T106), T107)) → FLATTEND_IN_GA(T107)
FLATTEND_IN_GA(cons(cons(T116, T117), T118)) → FLATTENE_IN_GGGA(T116, T117, T118)
FLATTENE_IN_GGGA(atom(T78), cons(T125, T126), T127) → FLATTENE_IN_GGGA(T125, T126, T127)

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(FLATTEND_IN_GA(x₁)) = 1 + 2·x₁
POL(FLATTENE_IN_GGGA(x₁, x₂, x₃)) = 2·x₁ + 2·x₂ + 2·x₃
POL(atom(x₁)) = 1 + x₁
POL(cons(x₁, x₂)) = x₁ + x₂

(13) Obligation:

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

FLATTENE_IN_GGGA(cons(T136, T137), T138, T139) → FLATTENE_IN_GGGA(T136, T137, cons(T138, T139))

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:

FLATTENE_IN_GGGA(cons(T136, T137), T138, T139) → FLATTENE_IN_GGGA(T136, T137, cons(T138, T139))
The graph contains the following edges 1 > 1, 1 > 2

(15) YES

(16) Obligation:

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

COUNTA_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → PB_IN_GGGAA(T51, T52, T53, X60, T55)
PB_IN_GGGAA(T51, T52, T53, T56, T55) → U10_GGGAA(T51, T52, T53, T56, T55, flattenF_in_ggga(T51, T52, T53, T56))
U10_GGGAA(T51, T52, T53, T56, T55, flattenF_out_ggga(T51, T52, T53, T56)) → COUNTA_IN_GA(T56, T55)
COUNTA_IN_GA(cons(atom(T8), cons(atom(T29), T30)), s(s(T32))) → COUNTA_IN_GA(T30, T32)
COUNTA_IN_GA(cons(cons(T157, T158), T159), T150) → PC_IN_GGGAA(T157, T158, T159, X247, T150)
PC_IN_GGGAA(T157, T158, T159, T160, T150) → U12_GGGAA(T157, T158, T159, T160, T150, flattenE_in_ggga(T157, T158, T159, T160))
U12_GGGAA(T157, T158, T159, T160, T150, flattenE_out_ggga(T157, T158, T159, T160)) → COUNTA_IN_GA(T160, T150)

The TRS R consists of the following rules:

countA_in_ga(atom(T4), s(0)) → countA_out_ga(atom(T4), s(0))
countA_in_ga(cons(atom(T8), atom(T16)), s(s(0))) → countA_out_ga(cons(atom(T8), atom(T16)), s(s(0)))
countA_in_ga(cons(atom(T8), cons(atom(T29), T30)), s(s(T32))) → U1_ga(T8, T29, T30, T32, countA_in_ga(T30, T32))
countA_in_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → U2_ga(T8, T51, T52, T53, T55, pB_in_gggaa(T51, T52, T53, X60, T55))
pB_in_gggaa(T51, T52, T53, T56, T55) → U10_gggaa(T51, T52, T53, T56, T55, flattenF_in_ggga(T51, T52, T53, T56))
flattenF_in_ggga(T63, T64, T65, X85) → U9_ggga(T63, T64, T65, X85, flattenE_in_ggga(T63, T64, T65, X85))
flattenE_in_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131))) → U6_ggga(T78, T89, T90, X131, flattenD_in_ga(T90, X131))
flattenD_in_ga(atom(T97), .(T97, [])) → flattenD_out_ga(atom(T97), .(T97, []))
flattenD_in_ga(cons(atom(T106), T107), .(T106, X158)) → U4_ga(T106, T107, X158, flattenD_in_ga(T107, X158))
flattenD_in_ga(cons(cons(T116, T117), T118), X175) → U5_ga(T116, T117, T118, X175, flattenE_in_ggga(T116, T117, T118, X175))
flattenE_in_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192)) → U7_ggga(T78, T125, T126, T127, X192, flattenE_in_ggga(T125, T126, T127, X192))
flattenE_in_ggga(cons(T136, T137), T138, T139, X209) → U8_ggga(T136, T137, T138, T139, X209, flattenE_in_ggga(T136, T137, cons(T138, T139), X209))
U8_ggga(T136, T137, T138, T139, X209, flattenE_out_ggga(T136, T137, cons(T138, T139), X209)) → flattenE_out_ggga(cons(T136, T137), T138, T139, X209)
U7_ggga(T78, T125, T126, T127, X192, flattenE_out_ggga(T125, T126, T127, X192)) → flattenE_out_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192))
U5_ga(T116, T117, T118, X175, flattenE_out_ggga(T116, T117, T118, X175)) → flattenD_out_ga(cons(cons(T116, T117), T118), X175)
U4_ga(T106, T107, X158, flattenD_out_ga(T107, X158)) → flattenD_out_ga(cons(atom(T106), T107), .(T106, X158))
U6_ggga(T78, T89, T90, X131, flattenD_out_ga(T90, X131)) → flattenE_out_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131)))
U9_ggga(T63, T64, T65, X85, flattenE_out_ggga(T63, T64, T65, X85)) → flattenF_out_ggga(T63, T64, T65, X85)
U10_gggaa(T51, T52, T53, T56, T55, flattenF_out_ggga(T51, T52, T53, T56)) → U11_gggaa(T51, T52, T53, T56, T55, countA_in_ga(T56, T55))
countA_in_ga(cons(cons(T157, T158), T159), T150) → U3_ga(T157, T158, T159, T150, pC_in_gggaa(T157, T158, T159, X247, T150))
pC_in_gggaa(T157, T158, T159, T160, T150) → U12_gggaa(T157, T158, T159, T160, T150, flattenE_in_ggga(T157, T158, T159, T160))
U12_gggaa(T157, T158, T159, T160, T150, flattenE_out_ggga(T157, T158, T159, T160)) → U13_gggaa(T157, T158, T159, T160, T150, countA_in_ga(T160, T150))
U13_gggaa(T157, T158, T159, T160, T150, countA_out_ga(T160, T150)) → pC_out_gggaa(T157, T158, T159, T160, T150)
U3_ga(T157, T158, T159, T150, pC_out_gggaa(T157, T158, T159, X247, T150)) → countA_out_ga(cons(cons(T157, T158), T159), T150)
U11_gggaa(T51, T52, T53, T56, T55, countA_out_ga(T56, T55)) → pB_out_gggaa(T51, T52, T53, T56, T55)
U2_ga(T8, T51, T52, T53, T55, pB_out_gggaa(T51, T52, T53, X60, T55)) → countA_out_ga(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55))
U1_ga(T8, T29, T30, T32, countA_out_ga(T30, T32)) → countA_out_ga(cons(atom(T8), cons(atom(T29), T30)), s(s(T32)))

The argument filtering Pi contains the following mapping:
countA_in_ga(x1, x2) = countA_in_ga(x1)
atom(x1) = atom(x1)
countA_out_ga(x1, x2) = countA_out_ga(x1, x2)
cons(x1, x2) = cons(x1, x2)
U1_ga(x1, x2, x3, x4, x5) = U1_ga(x1, x2, x3, x5)
U2_ga(x1, x2, x3, x4, x5, x6) = U2_ga(x1, x2, x3, x4, x6)
pB_in_gggaa(x1, x2, x3, x4, x5) = pB_in_gggaa(x1, x2, x3)
U10_gggaa(x1, x2, x3, x4, x5, x6) = U10_gggaa(x1, x2, x3, x6)
flattenF_in_ggga(x1, x2, x3, x4) = flattenF_in_ggga(x1, x2, x3)
U9_ggga(x1, x2, x3, x4, x5) = U9_ggga(x1, x2, x3, x5)
flattenE_in_ggga(x1, x2, x3, x4) = flattenE_in_ggga(x1, x2, x3)
U6_ggga(x1, x2, x3, x4, x5) = U6_ggga(x1, x2, x3, x5)
flattenD_in_ga(x1, x2) = flattenD_in_ga(x1)
flattenD_out_ga(x1, x2) = flattenD_out_ga(x1, x2)
U4_ga(x1, x2, x3, x4) = U4_ga(x1, x2, x4)
U5_ga(x1, x2, x3, x4, x5) = U5_ga(x1, x2, x3, x5)
U7_ggga(x1, x2, x3, x4, x5, x6) = U7_ggga(x1, x2, x3, x4, x6)
U8_ggga(x1, x2, x3, x4, x5, x6) = U8_ggga(x1, x2, x3, x4, x6)
flattenE_out_ggga(x1, x2, x3, x4) = flattenE_out_ggga(x1, x2, x3, x4)
flattenF_out_ggga(x1, x2, x3, x4) = flattenF_out_ggga(x1, x2, x3, x4)
U11_gggaa(x1, x2, x3, x4, x5, x6) = U11_gggaa(x1, x2, x3, x4, x6)
U3_ga(x1, x2, x3, x4, x5) = U3_ga(x1, x2, x3, x5)
pC_in_gggaa(x1, x2, x3, x4, x5) = pC_in_gggaa(x1, x2, x3)
U12_gggaa(x1, x2, x3, x4, x5, x6) = U12_gggaa(x1, x2, x3, x6)
U13_gggaa(x1, x2, x3, x4, x5, x6) = U13_gggaa(x1, x2, x3, x4, x6)
pC_out_gggaa(x1, x2, x3, x4, x5) = pC_out_gggaa(x1, x2, x3, x4, x5)
pB_out_gggaa(x1, x2, x3, x4, x5) = pB_out_gggaa(x1, x2, x3, x4, x5)
.(x1, x2) = .(x1, x2)
s(x1) = s(x1)
COUNTA_IN_GA(x1, x2) = COUNTA_IN_GA(x1)
PB_IN_GGGAA(x1, x2, x3, x4, x5) = PB_IN_GGGAA(x1, x2, x3)
U10_GGGAA(x1, x2, x3, x4, x5, x6) = U10_GGGAA(x1, x2, x3, x6)
PC_IN_GGGAA(x1, x2, x3, x4, x5) = PC_IN_GGGAA(x1, x2, x3)
U12_GGGAA(x1, x2, x3, x4, x5, x6) = U12_GGGAA(x1, x2, x3, x6)

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:

COUNTA_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53)), s(T55)) → PB_IN_GGGAA(T51, T52, T53, X60, T55)
PB_IN_GGGAA(T51, T52, T53, T56, T55) → U10_GGGAA(T51, T52, T53, T56, T55, flattenF_in_ggga(T51, T52, T53, T56))
U10_GGGAA(T51, T52, T53, T56, T55, flattenF_out_ggga(T51, T52, T53, T56)) → COUNTA_IN_GA(T56, T55)
COUNTA_IN_GA(cons(atom(T8), cons(atom(T29), T30)), s(s(T32))) → COUNTA_IN_GA(T30, T32)
COUNTA_IN_GA(cons(cons(T157, T158), T159), T150) → PC_IN_GGGAA(T157, T158, T159, X247, T150)
PC_IN_GGGAA(T157, T158, T159, T160, T150) → U12_GGGAA(T157, T158, T159, T160, T150, flattenE_in_ggga(T157, T158, T159, T160))
U12_GGGAA(T157, T158, T159, T160, T150, flattenE_out_ggga(T157, T158, T159, T160)) → COUNTA_IN_GA(T160, T150)

The TRS R consists of the following rules:

flattenF_in_ggga(T63, T64, T65, X85) → U9_ggga(T63, T64, T65, X85, flattenE_in_ggga(T63, T64, T65, X85))
flattenE_in_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131))) → U6_ggga(T78, T89, T90, X131, flattenD_in_ga(T90, X131))
flattenE_in_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192)) → U7_ggga(T78, T125, T126, T127, X192, flattenE_in_ggga(T125, T126, T127, X192))
flattenE_in_ggga(cons(T136, T137), T138, T139, X209) → U8_ggga(T136, T137, T138, T139, X209, flattenE_in_ggga(T136, T137, cons(T138, T139), X209))
U9_ggga(T63, T64, T65, X85, flattenE_out_ggga(T63, T64, T65, X85)) → flattenF_out_ggga(T63, T64, T65, X85)
U6_ggga(T78, T89, T90, X131, flattenD_out_ga(T90, X131)) → flattenE_out_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131)))
U7_ggga(T78, T125, T126, T127, X192, flattenE_out_ggga(T125, T126, T127, X192)) → flattenE_out_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192))
U8_ggga(T136, T137, T138, T139, X209, flattenE_out_ggga(T136, T137, cons(T138, T139), X209)) → flattenE_out_ggga(cons(T136, T137), T138, T139, X209)
flattenD_in_ga(atom(T97), .(T97, [])) → flattenD_out_ga(atom(T97), .(T97, []))
flattenD_in_ga(cons(atom(T106), T107), .(T106, X158)) → U4_ga(T106, T107, X158, flattenD_in_ga(T107, X158))
flattenD_in_ga(cons(cons(T116, T117), T118), X175) → U5_ga(T116, T117, T118, X175, flattenE_in_ggga(T116, T117, T118, X175))
U4_ga(T106, T107, X158, flattenD_out_ga(T107, X158)) → flattenD_out_ga(cons(atom(T106), T107), .(T106, X158))
U5_ga(T116, T117, T118, X175, flattenE_out_ggga(T116, T117, T118, X175)) → flattenD_out_ga(cons(cons(T116, T117), T118), X175)

The argument filtering Pi contains the following mapping:
atom(x1) = atom(x1)
cons(x1, x2) = cons(x1, x2)
flattenF_in_ggga(x1, x2, x3, x4) = flattenF_in_ggga(x1, x2, x3)
U9_ggga(x1, x2, x3, x4, x5) = U9_ggga(x1, x2, x3, x5)
flattenE_in_ggga(x1, x2, x3, x4) = flattenE_in_ggga(x1, x2, x3)
U6_ggga(x1, x2, x3, x4, x5) = U6_ggga(x1, x2, x3, x5)
flattenD_in_ga(x1, x2) = flattenD_in_ga(x1)
flattenD_out_ga(x1, x2) = flattenD_out_ga(x1, x2)
U4_ga(x1, x2, x3, x4) = U4_ga(x1, x2, x4)
U5_ga(x1, x2, x3, x4, x5) = U5_ga(x1, x2, x3, x5)
U7_ggga(x1, x2, x3, x4, x5, x6) = U7_ggga(x1, x2, x3, x4, x6)
U8_ggga(x1, x2, x3, x4, x5, x6) = U8_ggga(x1, x2, x3, x4, x6)
flattenE_out_ggga(x1, x2, x3, x4) = flattenE_out_ggga(x1, x2, x3, x4)
flattenF_out_ggga(x1, x2, x3, x4) = flattenF_out_ggga(x1, x2, x3, x4)
.(x1, x2) = .(x1, x2)
s(x1) = s(x1)
COUNTA_IN_GA(x1, x2) = COUNTA_IN_GA(x1)
PB_IN_GGGAA(x1, x2, x3, x4, x5) = PB_IN_GGGAA(x1, x2, x3)
U10_GGGAA(x1, x2, x3, x4, x5, x6) = U10_GGGAA(x1, x2, x3, x6)
PC_IN_GGGAA(x1, x2, x3, x4, x5) = PC_IN_GGGAA(x1, x2, x3)
U12_GGGAA(x1, x2, x3, x4, x5, x6) = U12_GGGAA(x1, x2, x3, x6)

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:

COUNTA_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53))) → PB_IN_GGGAA(T51, T52, T53)
PB_IN_GGGAA(T51, T52, T53) → U10_GGGAA(T51, T52, T53, flattenF_in_ggga(T51, T52, T53))
U10_GGGAA(T51, T52, T53, flattenF_out_ggga(T51, T52, T53, T56)) → COUNTA_IN_GA(T56)
COUNTA_IN_GA(cons(atom(T8), cons(atom(T29), T30))) → COUNTA_IN_GA(T30)
COUNTA_IN_GA(cons(cons(T157, T158), T159)) → PC_IN_GGGAA(T157, T158, T159)
PC_IN_GGGAA(T157, T158, T159) → U12_GGGAA(T157, T158, T159, flattenE_in_ggga(T157, T158, T159))
U12_GGGAA(T157, T158, T159, flattenE_out_ggga(T157, T158, T159, T160)) → COUNTA_IN_GA(T160)

The TRS R consists of the following rules:

flattenF_in_ggga(T63, T64, T65) → U9_ggga(T63, T64, T65, flattenE_in_ggga(T63, T64, T65))
flattenE_in_ggga(atom(T78), atom(T89), T90) → U6_ggga(T78, T89, T90, flattenD_in_ga(T90))
flattenE_in_ggga(atom(T78), cons(T125, T126), T127) → U7_ggga(T78, T125, T126, T127, flattenE_in_ggga(T125, T126, T127))
flattenE_in_ggga(cons(T136, T137), T138, T139) → U8_ggga(T136, T137, T138, T139, flattenE_in_ggga(T136, T137, cons(T138, T139)))
U9_ggga(T63, T64, T65, flattenE_out_ggga(T63, T64, T65, X85)) → flattenF_out_ggga(T63, T64, T65, X85)
U6_ggga(T78, T89, T90, flattenD_out_ga(T90, X131)) → flattenE_out_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131)))
U7_ggga(T78, T125, T126, T127, flattenE_out_ggga(T125, T126, T127, X192)) → flattenE_out_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192))
U8_ggga(T136, T137, T138, T139, flattenE_out_ggga(T136, T137, cons(T138, T139), X209)) → flattenE_out_ggga(cons(T136, T137), T138, T139, X209)
flattenD_in_ga(atom(T97)) → flattenD_out_ga(atom(T97), .(T97, []))
flattenD_in_ga(cons(atom(T106), T107)) → U4_ga(T106, T107, flattenD_in_ga(T107))
flattenD_in_ga(cons(cons(T116, T117), T118)) → U5_ga(T116, T117, T118, flattenE_in_ggga(T116, T117, T118))
U4_ga(T106, T107, flattenD_out_ga(T107, X158)) → flattenD_out_ga(cons(atom(T106), T107), .(T106, X158))
U5_ga(T116, T117, T118, flattenE_out_ggga(T116, T117, T118, X175)) → flattenD_out_ga(cons(cons(T116, T117), T118), X175)

The set Q consists of the following terms:

flattenF_in_ggga(x0, x1, x2)
flattenE_in_ggga(x0, x1, x2)
U9_ggga(x0, x1, x2, x3)
U6_ggga(x0, x1, x2, x3)
U7_ggga(x0, x1, x2, x3, x4)
U8_ggga(x0, x1, x2, x3, x4)
flattenD_in_ga(x0)
U4_ga(x0, x1, x2)
U5_ga(x0, x1, x2, x3)

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

(21) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule PB_IN_GGGAA(T51, T52, T53) → U10_GGGAA(T51, T52, T53, flattenF_in_ggga(T51, T52, T53)) at position [3] we obtained the following new rules [LPAR04]:

PB_IN_GGGAA(T51, T52, T53) → U10_GGGAA(T51, T52, T53, U9_ggga(T51, T52, T53, flattenE_in_ggga(T51, T52, T53)))

(22) Obligation:

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

COUNTA_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53))) → PB_IN_GGGAA(T51, T52, T53)
U10_GGGAA(T51, T52, T53, flattenF_out_ggga(T51, T52, T53, T56)) → COUNTA_IN_GA(T56)
COUNTA_IN_GA(cons(atom(T8), cons(atom(T29), T30))) → COUNTA_IN_GA(T30)
COUNTA_IN_GA(cons(cons(T157, T158), T159)) → PC_IN_GGGAA(T157, T158, T159)
PC_IN_GGGAA(T157, T158, T159) → U12_GGGAA(T157, T158, T159, flattenE_in_ggga(T157, T158, T159))
U12_GGGAA(T157, T158, T159, flattenE_out_ggga(T157, T158, T159, T160)) → COUNTA_IN_GA(T160)
PB_IN_GGGAA(T51, T52, T53) → U10_GGGAA(T51, T52, T53, U9_ggga(T51, T52, T53, flattenE_in_ggga(T51, T52, T53)))

The TRS R consists of the following rules:

flattenF_in_ggga(T63, T64, T65) → U9_ggga(T63, T64, T65, flattenE_in_ggga(T63, T64, T65))
flattenE_in_ggga(atom(T78), atom(T89), T90) → U6_ggga(T78, T89, T90, flattenD_in_ga(T90))
flattenE_in_ggga(atom(T78), cons(T125, T126), T127) → U7_ggga(T78, T125, T126, T127, flattenE_in_ggga(T125, T126, T127))
flattenE_in_ggga(cons(T136, T137), T138, T139) → U8_ggga(T136, T137, T138, T139, flattenE_in_ggga(T136, T137, cons(T138, T139)))
U9_ggga(T63, T64, T65, flattenE_out_ggga(T63, T64, T65, X85)) → flattenF_out_ggga(T63, T64, T65, X85)
U6_ggga(T78, T89, T90, flattenD_out_ga(T90, X131)) → flattenE_out_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131)))
U7_ggga(T78, T125, T126, T127, flattenE_out_ggga(T125, T126, T127, X192)) → flattenE_out_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192))
U8_ggga(T136, T137, T138, T139, flattenE_out_ggga(T136, T137, cons(T138, T139), X209)) → flattenE_out_ggga(cons(T136, T137), T138, T139, X209)
flattenD_in_ga(atom(T97)) → flattenD_out_ga(atom(T97), .(T97, []))
flattenD_in_ga(cons(atom(T106), T107)) → U4_ga(T106, T107, flattenD_in_ga(T107))
flattenD_in_ga(cons(cons(T116, T117), T118)) → U5_ga(T116, T117, T118, flattenE_in_ggga(T116, T117, T118))
U4_ga(T106, T107, flattenD_out_ga(T107, X158)) → flattenD_out_ga(cons(atom(T106), T107), .(T106, X158))
U5_ga(T116, T117, T118, flattenE_out_ggga(T116, T117, T118, X175)) → flattenD_out_ga(cons(cons(T116, T117), T118), X175)

The set Q consists of the following terms:

flattenF_in_ggga(x0, x1, x2)
flattenE_in_ggga(x0, x1, x2)
U9_ggga(x0, x1, x2, x3)
U6_ggga(x0, x1, x2, x3)
U7_ggga(x0, x1, x2, x3, x4)
U8_ggga(x0, x1, x2, x3, x4)
flattenD_in_ga(x0)
U4_ga(x0, x1, x2)
U5_ga(x0, x1, x2, x3)

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

(23) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(24) Obligation:

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

COUNTA_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53))) → PB_IN_GGGAA(T51, T52, T53)
U10_GGGAA(T51, T52, T53, flattenF_out_ggga(T51, T52, T53, T56)) → COUNTA_IN_GA(T56)
COUNTA_IN_GA(cons(atom(T8), cons(atom(T29), T30))) → COUNTA_IN_GA(T30)
COUNTA_IN_GA(cons(cons(T157, T158), T159)) → PC_IN_GGGAA(T157, T158, T159)
PC_IN_GGGAA(T157, T158, T159) → U12_GGGAA(T157, T158, T159, flattenE_in_ggga(T157, T158, T159))
U12_GGGAA(T157, T158, T159, flattenE_out_ggga(T157, T158, T159, T160)) → COUNTA_IN_GA(T160)
PB_IN_GGGAA(T51, T52, T53) → U10_GGGAA(T51, T52, T53, U9_ggga(T51, T52, T53, flattenE_in_ggga(T51, T52, T53)))

The TRS R consists of the following rules:

flattenE_in_ggga(atom(T78), atom(T89), T90) → U6_ggga(T78, T89, T90, flattenD_in_ga(T90))
flattenE_in_ggga(atom(T78), cons(T125, T126), T127) → U7_ggga(T78, T125, T126, T127, flattenE_in_ggga(T125, T126, T127))
flattenE_in_ggga(cons(T136, T137), T138, T139) → U8_ggga(T136, T137, T138, T139, flattenE_in_ggga(T136, T137, cons(T138, T139)))
U9_ggga(T63, T64, T65, flattenE_out_ggga(T63, T64, T65, X85)) → flattenF_out_ggga(T63, T64, T65, X85)
U8_ggga(T136, T137, T138, T139, flattenE_out_ggga(T136, T137, cons(T138, T139), X209)) → flattenE_out_ggga(cons(T136, T137), T138, T139, X209)
U7_ggga(T78, T125, T126, T127, flattenE_out_ggga(T125, T126, T127, X192)) → flattenE_out_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192))
flattenD_in_ga(atom(T97)) → flattenD_out_ga(atom(T97), .(T97, []))
flattenD_in_ga(cons(atom(T106), T107)) → U4_ga(T106, T107, flattenD_in_ga(T107))
flattenD_in_ga(cons(cons(T116, T117), T118)) → U5_ga(T116, T117, T118, flattenE_in_ggga(T116, T117, T118))
U6_ggga(T78, T89, T90, flattenD_out_ga(T90, X131)) → flattenE_out_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131)))
U5_ga(T116, T117, T118, flattenE_out_ggga(T116, T117, T118, X175)) → flattenD_out_ga(cons(cons(T116, T117), T118), X175)
U4_ga(T106, T107, flattenD_out_ga(T107, X158)) → flattenD_out_ga(cons(atom(T106), T107), .(T106, X158))

The set Q consists of the following terms:

flattenF_in_ggga(x0, x1, x2)
flattenE_in_ggga(x0, x1, x2)
U9_ggga(x0, x1, x2, x3)
U6_ggga(x0, x1, x2, x3)
U7_ggga(x0, x1, x2, x3, x4)
U8_ggga(x0, x1, x2, x3, x4)
flattenD_in_ga(x0)
U4_ga(x0, x1, x2)
U5_ga(x0, x1, x2, x3)

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

(25) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

flattenF_in_ggga(x0, x1, x2)

(26) Obligation:

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

COUNTA_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53))) → PB_IN_GGGAA(T51, T52, T53)
U10_GGGAA(T51, T52, T53, flattenF_out_ggga(T51, T52, T53, T56)) → COUNTA_IN_GA(T56)
COUNTA_IN_GA(cons(atom(T8), cons(atom(T29), T30))) → COUNTA_IN_GA(T30)
COUNTA_IN_GA(cons(cons(T157, T158), T159)) → PC_IN_GGGAA(T157, T158, T159)
PC_IN_GGGAA(T157, T158, T159) → U12_GGGAA(T157, T158, T159, flattenE_in_ggga(T157, T158, T159))
U12_GGGAA(T157, T158, T159, flattenE_out_ggga(T157, T158, T159, T160)) → COUNTA_IN_GA(T160)
PB_IN_GGGAA(T51, T52, T53) → U10_GGGAA(T51, T52, T53, U9_ggga(T51, T52, T53, flattenE_in_ggga(T51, T52, T53)))

The TRS R consists of the following rules:

flattenE_in_ggga(atom(T78), atom(T89), T90) → U6_ggga(T78, T89, T90, flattenD_in_ga(T90))
flattenE_in_ggga(atom(T78), cons(T125, T126), T127) → U7_ggga(T78, T125, T126, T127, flattenE_in_ggga(T125, T126, T127))
flattenE_in_ggga(cons(T136, T137), T138, T139) → U8_ggga(T136, T137, T138, T139, flattenE_in_ggga(T136, T137, cons(T138, T139)))
U9_ggga(T63, T64, T65, flattenE_out_ggga(T63, T64, T65, X85)) → flattenF_out_ggga(T63, T64, T65, X85)
U8_ggga(T136, T137, T138, T139, flattenE_out_ggga(T136, T137, cons(T138, T139), X209)) → flattenE_out_ggga(cons(T136, T137), T138, T139, X209)
U7_ggga(T78, T125, T126, T127, flattenE_out_ggga(T125, T126, T127, X192)) → flattenE_out_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192))
flattenD_in_ga(atom(T97)) → flattenD_out_ga(atom(T97), .(T97, []))
flattenD_in_ga(cons(atom(T106), T107)) → U4_ga(T106, T107, flattenD_in_ga(T107))
flattenD_in_ga(cons(cons(T116, T117), T118)) → U5_ga(T116, T117, T118, flattenE_in_ggga(T116, T117, T118))
U6_ggga(T78, T89, T90, flattenD_out_ga(T90, X131)) → flattenE_out_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131)))
U5_ga(T116, T117, T118, flattenE_out_ggga(T116, T117, T118, X175)) → flattenD_out_ga(cons(cons(T116, T117), T118), X175)
U4_ga(T106, T107, flattenD_out_ga(T107, X158)) → flattenD_out_ga(cons(atom(T106), T107), .(T106, X158))

The set Q consists of the following terms:

flattenE_in_ggga(x0, x1, x2)
U9_ggga(x0, x1, x2, x3)
U6_ggga(x0, x1, x2, x3)
U7_ggga(x0, x1, x2, x3, x4)
U8_ggga(x0, x1, x2, x3, x4)
flattenD_in_ga(x0)
U4_ga(x0, x1, x2)
U5_ga(x0, x1, x2, x3)

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

(27) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

COUNTA_IN_GA(cons(atom(T8), cons(cons(T51, T52), T53))) → PB_IN_GGGAA(T51, T52, T53)
COUNTA_IN_GA(cons(atom(T8), cons(atom(T29), T30))) → COUNTA_IN_GA(T30)
COUNTA_IN_GA(cons(cons(T157, T158), T159)) → PC_IN_GGGAA(T157, T158, T159)
PC_IN_GGGAA(T157, T158, T159) → U12_GGGAA(T157, T158, T159, flattenE_in_ggga(T157, T158, T159))
PB_IN_GGGAA(T51, T52, T53) → U10_GGGAA(T51, T52, T53, U9_ggga(T51, T52, T53, flattenE_in_ggga(T51, T52, T53)))

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

POL(.(x₁, x₂)) = 0
POL(COUNTA_IN_GA(x₁)) = x₁
POL(PB_IN_GGGAA(x₁, x₂, x₃)) = 1 + x₁ + x₃
POL(PC_IN_GGGAA(x₁, x₂, x₃)) = 1 + x₁ + x₂ + x₃
POL(U10_GGGAA(x₁, x₂, x₃, x₄)) = x₄
POL(U12_GGGAA(x₁, x₂, x₃, x₄)) = x₄
POL(U4_ga(x₁, x₂, x₃)) = 1 + x₁
POL(U5_ga(x₁, x₂, x₃, x₄)) = 1 + x₃ + x₄
POL(U6_ggga(x₁, x₂, x₃, x₄)) = 0
POL(U7_ggga(x₁, x₂, x₃, x₄, x₅)) = 0
POL(U8_ggga(x₁, x₂, x₃, x₄, x₅)) = 1 + x₂ + x₅
POL(U9_ggga(x₁, x₂, x₃, x₄)) = x₄
POL([]) = 0
POL(atom(x₁)) = 1 + x₁
POL(cons(x₁, x₂)) = 1 + x₁ + x₂
POL(flattenD_in_ga(x₁)) = x₁
POL(flattenD_out_ga(x₁, x₂)) = 0
POL(flattenE_in_ggga(x₁, x₂, x₃)) = x₁
POL(flattenE_out_ggga(x₁, x₂, x₃, x₄)) = x₄
POL(flattenF_out_ggga(x₁, x₂, x₃, x₄)) = x₄

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

flattenE_in_ggga(atom(T78), atom(T89), T90) → U6_ggga(T78, T89, T90, flattenD_in_ga(T90))
flattenE_in_ggga(atom(T78), cons(T125, T126), T127) → U7_ggga(T78, T125, T126, T127, flattenE_in_ggga(T125, T126, T127))
flattenE_in_ggga(cons(T136, T137), T138, T139) → U8_ggga(T136, T137, T138, T139, flattenE_in_ggga(T136, T137, cons(T138, T139)))
U9_ggga(T63, T64, T65, flattenE_out_ggga(T63, T64, T65, X85)) → flattenF_out_ggga(T63, T64, T65, X85)
flattenD_in_ga(cons(atom(T106), T107)) → U4_ga(T106, T107, flattenD_in_ga(T107))
U4_ga(T106, T107, flattenD_out_ga(T107, X158)) → flattenD_out_ga(cons(atom(T106), T107), .(T106, X158))
flattenD_in_ga(cons(cons(T116, T117), T118)) → U5_ga(T116, T117, T118, flattenE_in_ggga(T116, T117, T118))
U5_ga(T116, T117, T118, flattenE_out_ggga(T116, T117, T118, X175)) → flattenD_out_ga(cons(cons(T116, T117), T118), X175)
U6_ggga(T78, T89, T90, flattenD_out_ga(T90, X131)) → flattenE_out_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131)))
U7_ggga(T78, T125, T126, T127, flattenE_out_ggga(T125, T126, T127, X192)) → flattenE_out_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192))
U8_ggga(T136, T137, T138, T139, flattenE_out_ggga(T136, T137, cons(T138, T139), X209)) → flattenE_out_ggga(cons(T136, T137), T138, T139, X209)

(28) Obligation:

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

U10_GGGAA(T51, T52, T53, flattenF_out_ggga(T51, T52, T53, T56)) → COUNTA_IN_GA(T56)
U12_GGGAA(T157, T158, T159, flattenE_out_ggga(T157, T158, T159, T160)) → COUNTA_IN_GA(T160)

The TRS R consists of the following rules:

flattenE_in_ggga(atom(T78), atom(T89), T90) → U6_ggga(T78, T89, T90, flattenD_in_ga(T90))
flattenE_in_ggga(atom(T78), cons(T125, T126), T127) → U7_ggga(T78, T125, T126, T127, flattenE_in_ggga(T125, T126, T127))
flattenE_in_ggga(cons(T136, T137), T138, T139) → U8_ggga(T136, T137, T138, T139, flattenE_in_ggga(T136, T137, cons(T138, T139)))
U9_ggga(T63, T64, T65, flattenE_out_ggga(T63, T64, T65, X85)) → flattenF_out_ggga(T63, T64, T65, X85)
U8_ggga(T136, T137, T138, T139, flattenE_out_ggga(T136, T137, cons(T138, T139), X209)) → flattenE_out_ggga(cons(T136, T137), T138, T139, X209)
U7_ggga(T78, T125, T126, T127, flattenE_out_ggga(T125, T126, T127, X192)) → flattenE_out_ggga(atom(T78), cons(T125, T126), T127, .(T78, X192))
flattenD_in_ga(atom(T97)) → flattenD_out_ga(atom(T97), .(T97, []))
flattenD_in_ga(cons(atom(T106), T107)) → U4_ga(T106, T107, flattenD_in_ga(T107))
flattenD_in_ga(cons(cons(T116, T117), T118)) → U5_ga(T116, T117, T118, flattenE_in_ggga(T116, T117, T118))
U6_ggga(T78, T89, T90, flattenD_out_ga(T90, X131)) → flattenE_out_ggga(atom(T78), atom(T89), T90, .(T78, .(T89, X131)))
U5_ga(T116, T117, T118, flattenE_out_ggga(T116, T117, T118, X175)) → flattenD_out_ga(cons(cons(T116, T117), T118), X175)
U4_ga(T106, T107, flattenD_out_ga(T107, X158)) → flattenD_out_ga(cons(atom(T106), T107), .(T106, X158))

The set Q consists of the following terms:

flattenE_in_ggga(x0, x1, x2)
U9_ggga(x0, x1, x2, x3)
U6_ggga(x0, x1, x2, x3)
U7_ggga(x0, x1, x2, x3, x4)
U8_ggga(x0, x1, x2, x3, x4)
flattenD_in_ga(x0)
U4_ga(x0, x1, x2)
U5_ga(x0, x1, x2, x3)

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

(29) DependencyGraphProof (EQUIVALENT transformation)

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

(0) Obligation:

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) PiDPToQDPProof (SOUND transformation)

(11) Obligation:

(12) UsableRulesReductionPairsProof (EQUIVALENT transformation)

(13) Obligation:

(14) QDPSizeChangeProof (EQUIVALENT transformation)

(15) YES

(16) Obligation:

(17) UsableRulesProof (EQUIVALENT transformation)

(18) Obligation:

(19) PiDPToQDPProof (SOUND transformation)

(20) Obligation:

(21) Rewriting (EQUIVALENT transformation)

(22) Obligation:

(23) UsableRulesProof (EQUIVALENT transformation)

(24) Obligation:

(25) QReductionProof (EQUIVALENT transformation)

(26) Obligation:

(27) QDPOrderProof (EQUIVALENT transformation)

(28) Obligation:

(29) DependencyGraphProof (EQUIVALENT transformation)

(30) TRUE