Left Termination proof of /tmp/tmpVkk1Mh/ack.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 218 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 336 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 0 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇒, 0 ms)

        ↳11 QDP

        ↳12 Rewriting (⇔, 15 ms)

        ↳13 QDP

        ↳14 QDPOrderProof (⇔, 146 ms)

        ↳15 QDP

        ↳16 DependencyGraphProof (⇔, 0 ms)

        ↳17 QDP

        ↳18 UsableRulesProof (⇔, 0 ms)

        ↳19 QDP

        ↳20 QReductionProof (⇔, 0 ms)

        ↳21 QDP

        ↳22 QDPSizeChangeProof (⇔, 0 ms)

        ↳23 YES

    ↳24 PiDP

        ↳25 UsableRulesProof (⇔, 5 ms)

        ↳26 PiDP

        ↳27 PiDPToQDPProof (⇒, 0 ms)

        ↳28 QDP

        ↳29 QDPSizeChangeProof (⇔, 0 ms)

        ↳30 YES

(0) Obligation:

Clauses:

ack(0, N, s(N)).
ack(s(M), 0, A) :- ack(M, s(0), A).
ack(s(M), s(N), A) :- ','(ack(s(M), N, A1), ack(M, A1, A)).

Query: ack(g,g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: ack(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: ack(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | ack(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | ack(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: true | ack(0, T5, T3), SCOPE: 1, CLAUSE: 1 | ack(0, T5, T3), SCOPE: 1, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ack(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | ack(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground\nX2 is free\nack(T1, T2, T3) !=? ack(0, X2, s(X2))", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ack(0, T5, T3), SCOPE: 1, CLAUSE: 1 | ack(0, T5, T3), SCOPE: 1, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ack(0, T5, T3), SCOPE: 1, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ack(T8, s(0), T10) | ack(s(T8), 0, T3), SCOPE: 1, CLAUSE: 2\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ack(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground\nX2 is free\nX10 is free\nX11 is free\nack(T1, T2, T3) !=? ack(0, X2, s(X2))\nack(T1, T2, T3) !=? ack(s(X10), 0, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ack(T8, s(0), T10), SCOPE: 2, CLAUSE: 0 | ack(T8, s(0), T10), SCOPE: 2, CLAUSE: 1 | ack(T8, s(0), T10), SCOPE: 2, CLAUSE: 2 | ?_2 | ack(s(T8), 0, T3), SCOPE: 1, CLAUSE: 2\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ack(T8, s(0), T10), SCOPE: 2, CLAUSE: 0\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ack(T8, s(0), T10), SCOPE: 2, CLAUSE: 1 | ack(T8, s(0), T10), SCOPE: 2, CLAUSE: 2 | ?_2 | ack(s(T8), 0, T3), SCOPE: 1, CLAUSE: 2\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ack(T8, s(0), T10), SCOPE: 2, CLAUSE: 2 | ?_2 | ack(s(T8), 0, T3), SCOPE: 1, CLAUSE: 2\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ack(T8, s(0), T10), SCOPE: 2, CLAUSE: 2\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: ?_2 | ack(s(T8), 0, T3), SCOPE: 1, CLAUSE: 2\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="B: ','(ack(s(T20), 0, X36), ack(T20, X36, T22))\n\nT20 is ground\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="E: ack(s(T20), 0, X36)\n\nT20 is ground\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ack(T20, T23, T22)\n\nT20 is ground\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: ack(s(T20), 0, X36), SCOPE: 3, CLAUSE: 0 | ack(s(T20), 0, X36), SCOPE: 3, CLAUSE: 1 | ack(s(T20), 0, X36), SCOPE: 3, CLAUSE: 2\n\nT20 is ground\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ack(s(T20), 0, X36), SCOPE: 3, CLAUSE: 1 | ack(s(T20), 0, X36), SCOPE: 3, CLAUSE: 2\n\nT20 is ground\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: ack(s(T20), 0, X36), SCOPE: 3, CLAUSE: 1\n\nT20 is ground\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ack(s(T20), 0, X36), SCOPE: 3, CLAUSE: 2\n\nT20 is ground\nX36 is free", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="F: ack(T28, s(0), X60)\n\nT28 is ground\nX60 is free", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ack(T28, s(0), X60), SCOPE: 4, CLAUSE: 0 | ack(T28, s(0), X60), SCOPE: 4, CLAUSE: 1 | ack(T28, s(0), X60), SCOPE: 4, CLAUSE: 2\n\nT28 is ground\nX60 is free", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: ack(T28, s(0), X60), SCOPE: 4, CLAUSE: 0\n\nT28 is ground\nX60 is free", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: ack(T28, s(0), X60), SCOPE: 4, CLAUSE: 1 | ack(T28, s(0), X60), SCOPE: 4, CLAUSE: 2\n\nT28 is ground\nX60 is free", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ack(T28, s(0), X60), SCOPE: 4, CLAUSE: 2\n\nT28 is ground\nX60 is free", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="G: ','(ack(s(T32), 0, X82), ack(T32, X82, X83))\n\nT32 is ground\nX83 is free\nX82 is free", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: ack(s(T32), 0, X82)\n\nT32 is ground\nX82 is free", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="H: ack(T32, T33, X83)\n\nT32 is ground\nT33 is ground\nX83 is free", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: ack(T32, T33, X83), SCOPE: 5, CLAUSE: 0 | ack(T32, T33, X83), SCOPE: 5, CLAUSE: 1 | ack(T32, T33, X83), SCOPE: 5, CLAUSE: 2\n\nT32 is ground\nT33 is ground\nX83 is free", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: ack(T32, T33, X83), SCOPE: 5, CLAUSE: 0\n\nT32 is ground\nT33 is ground\nX83 is free", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: ack(T32, T33, X83), SCOPE: 5, CLAUSE: 1 | ack(T32, T33, X83), SCOPE: 5, CLAUSE: 2\n\nT32 is ground\nT33 is ground\nX83 is free", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: ack(T32, T33, X83), SCOPE: 5, CLAUSE: 1\n\nT32 is ground\nT33 is ground\nX83 is free", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: ack(T32, T33, X83), SCOPE: 5, CLAUSE: 2\n\nT32 is ground\nT33 is ground\nX83 is free", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: ack(T45, s(0), X109)\n\nT45 is ground\nX109 is free", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="I: ','(ack(s(T50), T51, X124), ack(T50, X124, X125))\n\nT50 is ground\nT51 is ground\nX125 is free\nX124 is free", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: ack(s(T50), T51, X124)\n\nT50 is ground\nT51 is ground\nX124 is free", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: ack(T50, T52, X125)\n\nT50 is ground\nT52 is ground\nX125 is free", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
143 [label="143: ack(s(T8), 0, T3), SCOPE: 1, CLAUSE: 2\n\nT8 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
144 [label="144: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
161 [label="161: ','(ack(s(T62), T63, X146), ack(T62, X146, T65))\n\nT62 is ground\nT63 is ground\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
162 [label="162: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
163 [label="163: ','(ack(s(T62), T63, X146), ack(T62, X146, T65)), SCOPE: 6, CLAUSE: 0 | ','(ack(s(T62), T63, X146), ack(T62, X146, T65)), SCOPE: 6, CLAUSE: 1 | ','(ack(s(T62), T63, X146), ack(T62, X146, T65)), SCOPE: 6, CLAUSE: 2\n\nT62 is ground\nT63 is ground\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
164 [label="164: ','(ack(s(T62), T63, X146), ack(T62, X146, T65)), SCOPE: 6, CLAUSE: 1 | ','(ack(s(T62), T63, X146), ack(T62, X146, T65)), SCOPE: 6, CLAUSE: 2\n\nT62 is ground\nT63 is ground\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
165 [label="165: ','(ack(s(T62), T63, X146), ack(T62, X146, T65)), SCOPE: 6, CLAUSE: 1\n\nT62 is ground\nT63 is ground\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
166 [label="166: ','(ack(s(T62), T63, X146), ack(T62, X146, T65)), SCOPE: 6, CLAUSE: 2\n\nT62 is ground\nT63 is ground\nX146 is free", fontsize=16, style=filled, fillcolor=lightyellow];
171 [label="C: ','(ack(T70, s(0), X162), ack(T70, X162, T65))\n\nT70 is ground\nX162 is free", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: ack(T70, s(0), X162)\n\nT70 is ground\nX162 is free", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: ack(T70, T71, T65)\n\nT70 is ground\nT71 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
182 [label="D: ','(','(ack(s(T78), T79, X181), ack(T78, X181, X182)), ack(T78, X182, T65))\n\nT78 is ground\nT79 is ground\nX182 is free\nX181 is free", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
188 [label="188: ack(s(T78), T79, X181)\n\nT78 is ground\nT79 is ground\nX181 is free", fontsize=16, style=filled, fillcolor=lightyellow];
189 [label="J: ','(ack(T78, T80, X182), ack(T78, X182, T65))\n\nT78 is ground\nT80 is ground\nX182 is free", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="192: ack(T78, T80, X182)\n\nT78 is ground\nT80 is ground\nX182 is free", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="193: ack(T78, T83, T65)\n\nT78 is ground\nT83 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 194 [arrowhead = none ];
194 -> 5;

195 [label="EVAL with clause\nack(0, X2, s(X2)).\nand substitutionT1 -> 0,\nT2 -> T5,\nX2 -> T5,\nT3 -> s(T5)", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 195 [arrowhead = none ];
195 -> 10;

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

197 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 197 [arrowhead = none ];
197 -> 12;

198 [label="EVAL with clause\nack(s(X10), 0, X11) :- ack(X10, s(0), X11).\nand substitutionX10 -> T8,\nT1 -> s(T8),\nT2 -> 0,\nT3 -> T10,\nX11 -> T10,\nT9 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 198 [arrowhead = none ];
198 -> 24;

199 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
11 -> 199 [arrowhead = none ];
199 -> 26;

200 [label="BACKTRACK\nfor clause: ack(s(M), 0, A) :- ack(M, s(0), A)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
12 -> 200 [arrowhead = none ];
200 -> 15;

201 [label="BACKTRACK\nfor clause: ack(s(M), s(N), A) :- ','(ack(s(M), N, A1), ack(M, A1, A))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 201 [arrowhead = none ];
201 -> 20;

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

203 [label="EVAL with clause\nack(s(X143), s(X144), X145) :- ','(ack(s(X143), X144, X146), ack(X143, X146, X145)).\nand substitutionX143 -> T62,\nT1 -> s(T62),\nX144 -> T63,\nT2 -> s(T63),\nT3 -> T65,\nX145 -> T65,\nT64 -> T65", fontsize=14, style = filled, fillcolor = lightblue];
26 -> 203 [arrowhead = none ];
203 -> 161;

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

205 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
29 -> 205 [arrowhead = none ];
205 -> 32;

206 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
29 -> 206 [arrowhead = none ];
206 -> 33;

207 [label="EVAL with clause\nack(0, X16, s(X16)).\nand substitutionT8 -> 0,\nX16 -> s(0),\nT10 -> s(s(0))", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 207 [arrowhead = none ];
207 -> 36;

208 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
32 -> 208 [arrowhead = none ];
208 -> 37;

209 [label="BACKTRACK\nfor clause: ack(s(M), 0, A) :- ack(M, s(0), A)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
33 -> 209 [arrowhead = none ];
209 -> 39;

210 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 210 [arrowhead = none ];
210 -> 38;

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

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

213 [label="EVAL with clause\nack(s(X33), s(X34), X35) :- ','(ack(s(X33), X34, X36), ack(X33, X36, X35)).\nand substitutionX33 -> T20,\nT8 -> s(T20),\nX34 -> 0,\nT10 -> T22,\nX35 -> T22,\nT21 -> T22", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 213 [arrowhead = none ];
213 -> 52;

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

215 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
45 -> 215 [arrowhead = none ];
215 -> 143;

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

217 [label="SPLIT 2\nnew knowledge:\nT20 is ground\nT23 is ground\nreplacements:X36 -> T23", fontsize=14, style = filled, fillcolor = violet];
52 -> 217 [arrowhead = none ];
217 -> 58;

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

219 [label="INSTANCE with matching:\nT1 -> T20\nT2 -> T23\nT3 -> T22", fontsize=14, style = filled, fillcolor = lightgrey];
58 -> 219 [arrowhead = none , style=dashed];
219 -> 1[style=dashed];

220 [label="BACKTRACK\nfor clause: ack(0, N, s(N))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
63 -> 220 [arrowhead = none ];
220 -> 64;

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

222 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
64 -> 222 [arrowhead = none ];
222 -> 71;

223 [label="ONLY EVAL with clause\nack(s(X58), 0, X59) :- ack(X58, s(0), X59).\nand substitutionT20 -> T28,\nX58 -> T28,\nX36 -> X60,\nX59 -> X60", fontsize=14, style = filled, fillcolor = lightblue];
70 -> 223 [arrowhead = none ];
223 -> 77;

224 [label="BACKTRACK\nfor clause: ack(s(M), s(N), A) :- ','(ack(s(M), N, A1), ack(M, A1, A))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
71 -> 224 [arrowhead = none ];
224 -> 140;

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

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

227 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
79 -> 227 [arrowhead = none ];
227 -> 81;

228 [label="EVAL with clause\nack(0, X67, s(X67)).\nand substitutionT28 -> 0,\nX67 -> s(0),\nX60 -> s(s(0))", fontsize=14, style = filled, fillcolor = lightblue];
80 -> 228 [arrowhead = none ];
228 -> 83;

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

230 [label="BACKTRACK\nfor clause: ack(s(M), 0, A) :- ack(M, s(0), A)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
81 -> 230 [arrowhead = none ];
230 -> 88;

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

232 [label="EVAL with clause\nack(s(X79), s(X80), X81) :- ','(ack(s(X79), X80, X82), ack(X79, X82, X81)).\nand substitutionX79 -> T32,\nT28 -> s(T32),\nX80 -> 0,\nX60 -> X83,\nX81 -> X83", fontsize=14, style = filled, fillcolor = lightblue];
88 -> 232 [arrowhead = none ];
232 -> 95;

233 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
88 -> 233 [arrowhead = none ];
233 -> 96;

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

235 [label="SPLIT 2\nnew knowledge:\nT32 is ground\nT33 is ground\nreplacements:X82 -> T33", fontsize=14, style = filled, fillcolor = violet];
95 -> 235 [arrowhead = none ];
235 -> 100;

236 [label="INSTANCE with matching:\nT20 -> T32\nX36 -> X82", fontsize=14, style = filled, fillcolor = lightgrey];
99 -> 236 [arrowhead = none , style=dashed];
236 -> 57[style=dashed];

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

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

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

240 [label="EVAL with clause\nack(0, X94, s(X94)).\nand substitutionT32 -> 0,\nT33 -> T40,\nX94 -> T40,\nX83 -> s(T40)", fontsize=14, style = filled, fillcolor = lightblue];
107 -> 240 [arrowhead = none ];
240 -> 113;

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

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

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

244 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
113 -> 244 [arrowhead = none ];
244 -> 115;

245 [label="EVAL with clause\nack(s(X107), 0, X108) :- ack(X107, s(0), X108).\nand substitutionX107 -> T45,\nT32 -> s(T45),\nT33 -> 0,\nX83 -> X109,\nX108 -> X109", fontsize=14, style = filled, fillcolor = lightblue];
119 -> 245 [arrowhead = none ];
245 -> 127;

246 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
119 -> 246 [arrowhead = none ];
246 -> 128;

247 [label="EVAL with clause\nack(s(X121), s(X122), X123) :- ','(ack(s(X121), X122, X124), ack(X121, X124, X123)).\nand substitutionX121 -> T50,\nT32 -> s(T50),\nX122 -> T51,\nT33 -> s(T51),\nX83 -> X125,\nX123 -> X125", fontsize=14, style = filled, fillcolor = lightblue];
120 -> 247 [arrowhead = none ];
247 -> 131;

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

249 [label="INSTANCE with matching:\nT28 -> T45\nX60 -> X109", fontsize=14, style = filled, fillcolor = lightgrey];
127 -> 249 [arrowhead = none , style=dashed];
249 -> 77[style=dashed];

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

251 [label="SPLIT 2\nnew knowledge:\nT50 is ground\nT51 is ground\nT52 is ground\nreplacements:X124 -> T52", fontsize=14, style = filled, fillcolor = violet];
131 -> 251 [arrowhead = none ];
251 -> 136;

252 [label="INSTANCE with matching:\nT32 -> s(T50)\nT33 -> T51\nX83 -> X124", fontsize=14, style = filled, fillcolor = lightgrey];
135 -> 252 [arrowhead = none , style=dashed];
252 -> 100[style=dashed];

253 [label="INSTANCE with matching:\nT32 -> T50\nT33 -> T52\nX83 -> X125", fontsize=14, style = filled, fillcolor = lightgrey];
136 -> 253 [arrowhead = none , style=dashed];
253 -> 100[style=dashed];

254 [label="BACKTRACK\nfor clause: ack(s(M), s(N), A) :- ','(ack(s(M), N, A1), ack(M, A1, A))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
143 -> 254 [arrowhead = none ];
254 -> 144;

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

256 [label="BACKTRACK\nfor clause: ack(0, N, s(N))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
163 -> 256 [arrowhead = none ];
256 -> 164;

257 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
164 -> 257 [arrowhead = none ];
257 -> 165;

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

259 [label="EVAL with clause\nack(s(X160), 0, X161) :- ack(X160, s(0), X161).\nand substitutionT62 -> T70,\nX160 -> T70,\nT63 -> 0,\nX146 -> X162,\nX161 -> X162", fontsize=14, style = filled, fillcolor = lightblue];
165 -> 259 [arrowhead = none ];
259 -> 171;

260 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
165 -> 260 [arrowhead = none ];
260 -> 172;

261 [label="EVAL with clause\nack(s(X178), s(X179), X180) :- ','(ack(s(X178), X179, X181), ack(X178, X181, X180)).\nand substitutionT62 -> T78,\nX178 -> T78,\nX179 -> T79,\nT63 -> s(T79),\nX146 -> X182,\nX180 -> X182", fontsize=14, style = filled, fillcolor = lightblue];
166 -> 261 [arrowhead = none ];
261 -> 182;

262 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
166 -> 262 [arrowhead = none ];
262 -> 185;

263 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
171 -> 263 [arrowhead = none ];
263 -> 174;

264 [label="SPLIT 2\nnew knowledge:\nT70 is ground\nT71 is ground\nreplacements:X162 -> T71", fontsize=14, style = filled, fillcolor = violet];
171 -> 264 [arrowhead = none ];
264 -> 175;

265 [label="INSTANCE with matching:\nT28 -> T70\nX60 -> X162", fontsize=14, style = filled, fillcolor = lightgrey];
174 -> 265 [arrowhead = none , style=dashed];
265 -> 77[style=dashed];

266 [label="INSTANCE with matching:\nT1 -> T70\nT2 -> T71\nT3 -> T65", fontsize=14, style = filled, fillcolor = lightgrey];
175 -> 266 [arrowhead = none , style=dashed];
266 -> 1[style=dashed];

267 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
182 -> 267 [arrowhead = none ];
267 -> 188;

268 [label="SPLIT 2\nnew knowledge:\nT78 is ground\nT79 is ground\nT80 is ground\nreplacements:X181 -> T80", fontsize=14, style = filled, fillcolor = violet];
182 -> 268 [arrowhead = none ];
268 -> 189;

269 [label="INSTANCE with matching:\nT32 -> s(T78)\nT33 -> T79\nX83 -> X181", fontsize=14, style = filled, fillcolor = lightgrey];
188 -> 269 [arrowhead = none , style=dashed];
269 -> 100[style=dashed];

270 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
189 -> 270 [arrowhead = none ];
270 -> 192;

271 [label="SPLIT 2\nnew knowledge:\nT78 is ground\nT80 is ground\nT83 is ground\nreplacements:X182 -> T83", fontsize=14, style = filled, fillcolor = violet];
189 -> 271 [arrowhead = none ];
271 -> 193;

272 [label="INSTANCE with matching:\nT32 -> T78\nT33 -> T80\nX83 -> X182", fontsize=14, style = filled, fillcolor = lightgrey];
192 -> 272 [arrowhead = none , style=dashed];
272 -> 100[style=dashed];

273 [label="INSTANCE with matching:\nT1 -> T78\nT2 -> T83\nT3 -> T65", fontsize=14, style = filled, fillcolor = lightgrey];
193 -> 273 [arrowhead = none , style=dashed];
273 -> 1[style=dashed];

}

(2) Obligation:

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

ackA_in_gga(0, T5, s(T5)) → ackA_out_gga(0, T5, s(T5))
ackA_in_gga(s(0), 0, s(s(0))) → ackA_out_gga(s(0), 0, s(s(0)))
ackA_in_gga(s(s(T20)), 0, T22) → U1_gga(T20, T22, pB_in_gaa(T20, X36, T22))
pB_in_gaa(T20, T23, T22) → U8_gaa(T20, T23, T22, ackE_in_ga(T20, T23))
ackE_in_ga(T28, X60) → U4_ga(T28, X60, ackF_in_ga(T28, X60))
ackF_in_ga(0, s(s(0))) → ackF_out_ga(0, s(s(0)))
ackF_in_ga(s(T32), X83) → U5_ga(T32, X83, pG_in_gaa(T32, X82, X83))
pG_in_gaa(T32, T33, X83) → U10_gaa(T32, T33, X83, ackE_in_ga(T32, T33))
U10_gaa(T32, T33, X83, ackE_out_ga(T32, T33)) → U11_gaa(T32, T33, X83, ackH_in_gga(T32, T33, X83))
ackH_in_gga(0, T40, s(T40)) → ackH_out_gga(0, T40, s(T40))
ackH_in_gga(s(T45), 0, X109) → U6_gga(T45, X109, ackF_in_ga(T45, X109))
U6_gga(T45, X109, ackF_out_ga(T45, X109)) → ackH_out_gga(s(T45), 0, X109)
ackH_in_gga(s(T50), s(T51), X125) → U7_gga(T50, T51, X125, pI_in_ggaa(T50, T51, X124, X125))
pI_in_ggaa(T50, T51, T52, X125) → U12_ggaa(T50, T51, T52, X125, ackH_in_gga(s(T50), T51, T52))
U12_ggaa(T50, T51, T52, X125, ackH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, X125, ackH_in_gga(T50, T52, X125))
U13_ggaa(T50, T51, T52, X125, ackH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U7_gga(T50, T51, X125, pI_out_ggaa(T50, T51, X124, X125)) → ackH_out_gga(s(T50), s(T51), X125)
U11_gaa(T32, T33, X83, ackH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)
U5_ga(T32, X83, pG_out_gaa(T32, X82, X83)) → ackF_out_ga(s(T32), X83)
U4_ga(T28, X60, ackF_out_ga(T28, X60)) → ackE_out_ga(T28, X60)
U8_gaa(T20, T23, T22, ackE_out_ga(T20, T23)) → U9_gaa(T20, T23, T22, ackA_in_gga(T20, T23, T22))
ackA_in_gga(s(T70), s(0), T65) → U2_gga(T70, T65, pC_in_gaa(T70, X162, T65))
pC_in_gaa(T70, T71, T65) → U14_gaa(T70, T71, T65, ackF_in_ga(T70, T71))
U14_gaa(T70, T71, T65, ackF_out_ga(T70, T71)) → U15_gaa(T70, T71, T65, ackA_in_gga(T70, T71, T65))
ackA_in_gga(s(T78), s(s(T79)), T65) → U3_gga(T78, T79, T65, pD_in_ggaaa(T78, T79, X181, X182, T65))
pD_in_ggaaa(T78, T79, T80, X182, T65) → U16_ggaaa(T78, T79, T80, X182, T65, ackH_in_gga(s(T78), T79, T80))
U16_ggaaa(T78, T79, T80, X182, T65, ackH_out_gga(s(T78), T79, T80)) → U17_ggaaa(T78, T79, T80, X182, T65, pJ_in_ggaa(T78, T80, X182, T65))
pJ_in_ggaa(T78, T80, T83, T65) → U18_ggaa(T78, T80, T83, T65, ackH_in_gga(T78, T80, T83))
U18_ggaa(T78, T80, T83, T65, ackH_out_gga(T78, T80, T83)) → U19_ggaa(T78, T80, T83, T65, ackA_in_gga(T78, T83, T65))
U19_ggaa(T78, T80, T83, T65, ackA_out_gga(T78, T83, T65)) → pJ_out_ggaa(T78, T80, T83, T65)
U17_ggaaa(T78, T79, T80, X182, T65, pJ_out_ggaa(T78, T80, X182, T65)) → pD_out_ggaaa(T78, T79, T80, X182, T65)
U3_gga(T78, T79, T65, pD_out_ggaaa(T78, T79, X181, X182, T65)) → ackA_out_gga(s(T78), s(s(T79)), T65)
U15_gaa(T70, T71, T65, ackA_out_gga(T70, T71, T65)) → pC_out_gaa(T70, T71, T65)
U2_gga(T70, T65, pC_out_gaa(T70, X162, T65)) → ackA_out_gga(s(T70), s(0), T65)
U9_gaa(T20, T23, T22, ackA_out_gga(T20, T23, T22)) → pB_out_gaa(T20, T23, T22)
U1_gga(T20, T22, pB_out_gaa(T20, X36, T22)) → ackA_out_gga(s(s(T20)), 0, T22)

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

ACKA_IN_GGA(s(s(T20)), 0, T22) → U1_GGA(T20, T22, pB_in_gaa(T20, X36, T22))
ACKA_IN_GGA(s(s(T20)), 0, T22) → PB_IN_GAA(T20, X36, T22)
PB_IN_GAA(T20, T23, T22) → U8_GAA(T20, T23, T22, ackE_in_ga(T20, T23))
PB_IN_GAA(T20, T23, T22) → ACKE_IN_GA(T20, T23)
ACKE_IN_GA(T28, X60) → U4_GA(T28, X60, ackF_in_ga(T28, X60))
ACKE_IN_GA(T28, X60) → ACKF_IN_GA(T28, X60)
ACKF_IN_GA(s(T32), X83) → U5_GA(T32, X83, pG_in_gaa(T32, X82, X83))
ACKF_IN_GA(s(T32), X83) → PG_IN_GAA(T32, X82, X83)
PG_IN_GAA(T32, T33, X83) → U10_GAA(T32, T33, X83, ackE_in_ga(T32, T33))
PG_IN_GAA(T32, T33, X83) → ACKE_IN_GA(T32, T33)
U10_GAA(T32, T33, X83, ackE_out_ga(T32, T33)) → U11_GAA(T32, T33, X83, ackH_in_gga(T32, T33, X83))
U10_GAA(T32, T33, X83, ackE_out_ga(T32, T33)) → ACKH_IN_GGA(T32, T33, X83)
ACKH_IN_GGA(s(T45), 0, X109) → U6_GGA(T45, X109, ackF_in_ga(T45, X109))
ACKH_IN_GGA(s(T45), 0, X109) → ACKF_IN_GA(T45, X109)
ACKH_IN_GGA(s(T50), s(T51), X125) → U7_GGA(T50, T51, X125, pI_in_ggaa(T50, T51, X124, X125))
ACKH_IN_GGA(s(T50), s(T51), X125) → PI_IN_GGAA(T50, T51, X124, X125)
PI_IN_GGAA(T50, T51, T52, X125) → U12_GGAA(T50, T51, T52, X125, ackH_in_gga(s(T50), T51, T52))
PI_IN_GGAA(T50, T51, T52, X125) → ACKH_IN_GGA(s(T50), T51, T52)
U12_GGAA(T50, T51, T52, X125, ackH_out_gga(s(T50), T51, T52)) → U13_GGAA(T50, T51, T52, X125, ackH_in_gga(T50, T52, X125))
U12_GGAA(T50, T51, T52, X125, ackH_out_gga(s(T50), T51, T52)) → ACKH_IN_GGA(T50, T52, X125)
U8_GAA(T20, T23, T22, ackE_out_ga(T20, T23)) → U9_GAA(T20, T23, T22, ackA_in_gga(T20, T23, T22))
U8_GAA(T20, T23, T22, ackE_out_ga(T20, T23)) → ACKA_IN_GGA(T20, T23, T22)
ACKA_IN_GGA(s(T70), s(0), T65) → U2_GGA(T70, T65, pC_in_gaa(T70, X162, T65))
ACKA_IN_GGA(s(T70), s(0), T65) → PC_IN_GAA(T70, X162, T65)
PC_IN_GAA(T70, T71, T65) → U14_GAA(T70, T71, T65, ackF_in_ga(T70, T71))
PC_IN_GAA(T70, T71, T65) → ACKF_IN_GA(T70, T71)
U14_GAA(T70, T71, T65, ackF_out_ga(T70, T71)) → U15_GAA(T70, T71, T65, ackA_in_gga(T70, T71, T65))
U14_GAA(T70, T71, T65, ackF_out_ga(T70, T71)) → ACKA_IN_GGA(T70, T71, T65)
ACKA_IN_GGA(s(T78), s(s(T79)), T65) → U3_GGA(T78, T79, T65, pD_in_ggaaa(T78, T79, X181, X182, T65))
ACKA_IN_GGA(s(T78), s(s(T79)), T65) → PD_IN_GGAAA(T78, T79, X181, X182, T65)
PD_IN_GGAAA(T78, T79, T80, X182, T65) → U16_GGAAA(T78, T79, T80, X182, T65, ackH_in_gga(s(T78), T79, T80))
PD_IN_GGAAA(T78, T79, T80, X182, T65) → ACKH_IN_GGA(s(T78), T79, T80)
U16_GGAAA(T78, T79, T80, X182, T65, ackH_out_gga(s(T78), T79, T80)) → U17_GGAAA(T78, T79, T80, X182, T65, pJ_in_ggaa(T78, T80, X182, T65))
U16_GGAAA(T78, T79, T80, X182, T65, ackH_out_gga(s(T78), T79, T80)) → PJ_IN_GGAA(T78, T80, X182, T65)
PJ_IN_GGAA(T78, T80, T83, T65) → U18_GGAA(T78, T80, T83, T65, ackH_in_gga(T78, T80, T83))
PJ_IN_GGAA(T78, T80, T83, T65) → ACKH_IN_GGA(T78, T80, T83)
U18_GGAA(T78, T80, T83, T65, ackH_out_gga(T78, T80, T83)) → U19_GGAA(T78, T80, T83, T65, ackA_in_gga(T78, T83, T65))
U18_GGAA(T78, T80, T83, T65, ackH_out_gga(T78, T80, T83)) → ACKA_IN_GGA(T78, T83, T65)

The TRS R consists of the following rules:

ackA_in_gga(0, T5, s(T5)) → ackA_out_gga(0, T5, s(T5))
ackA_in_gga(s(0), 0, s(s(0))) → ackA_out_gga(s(0), 0, s(s(0)))
ackA_in_gga(s(s(T20)), 0, T22) → U1_gga(T20, T22, pB_in_gaa(T20, X36, T22))
pB_in_gaa(T20, T23, T22) → U8_gaa(T20, T23, T22, ackE_in_ga(T20, T23))
ackE_in_ga(T28, X60) → U4_ga(T28, X60, ackF_in_ga(T28, X60))
ackF_in_ga(0, s(s(0))) → ackF_out_ga(0, s(s(0)))
ackF_in_ga(s(T32), X83) → U5_ga(T32, X83, pG_in_gaa(T32, X82, X83))
pG_in_gaa(T32, T33, X83) → U10_gaa(T32, T33, X83, ackE_in_ga(T32, T33))
U10_gaa(T32, T33, X83, ackE_out_ga(T32, T33)) → U11_gaa(T32, T33, X83, ackH_in_gga(T32, T33, X83))
ackH_in_gga(0, T40, s(T40)) → ackH_out_gga(0, T40, s(T40))
ackH_in_gga(s(T45), 0, X109) → U6_gga(T45, X109, ackF_in_ga(T45, X109))
U6_gga(T45, X109, ackF_out_ga(T45, X109)) → ackH_out_gga(s(T45), 0, X109)
ackH_in_gga(s(T50), s(T51), X125) → U7_gga(T50, T51, X125, pI_in_ggaa(T50, T51, X124, X125))
pI_in_ggaa(T50, T51, T52, X125) → U12_ggaa(T50, T51, T52, X125, ackH_in_gga(s(T50), T51, T52))
U12_ggaa(T50, T51, T52, X125, ackH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, X125, ackH_in_gga(T50, T52, X125))
U13_ggaa(T50, T51, T52, X125, ackH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U7_gga(T50, T51, X125, pI_out_ggaa(T50, T51, X124, X125)) → ackH_out_gga(s(T50), s(T51), X125)
U11_gaa(T32, T33, X83, ackH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)
U5_ga(T32, X83, pG_out_gaa(T32, X82, X83)) → ackF_out_ga(s(T32), X83)
U4_ga(T28, X60, ackF_out_ga(T28, X60)) → ackE_out_ga(T28, X60)
U8_gaa(T20, T23, T22, ackE_out_ga(T20, T23)) → U9_gaa(T20, T23, T22, ackA_in_gga(T20, T23, T22))
ackA_in_gga(s(T70), s(0), T65) → U2_gga(T70, T65, pC_in_gaa(T70, X162, T65))
pC_in_gaa(T70, T71, T65) → U14_gaa(T70, T71, T65, ackF_in_ga(T70, T71))
U14_gaa(T70, T71, T65, ackF_out_ga(T70, T71)) → U15_gaa(T70, T71, T65, ackA_in_gga(T70, T71, T65))
ackA_in_gga(s(T78), s(s(T79)), T65) → U3_gga(T78, T79, T65, pD_in_ggaaa(T78, T79, X181, X182, T65))
pD_in_ggaaa(T78, T79, T80, X182, T65) → U16_ggaaa(T78, T79, T80, X182, T65, ackH_in_gga(s(T78), T79, T80))
U16_ggaaa(T78, T79, T80, X182, T65, ackH_out_gga(s(T78), T79, T80)) → U17_ggaaa(T78, T79, T80, X182, T65, pJ_in_ggaa(T78, T80, X182, T65))
pJ_in_ggaa(T78, T80, T83, T65) → U18_ggaa(T78, T80, T83, T65, ackH_in_gga(T78, T80, T83))
U18_ggaa(T78, T80, T83, T65, ackH_out_gga(T78, T80, T83)) → U19_ggaa(T78, T80, T83, T65, ackA_in_gga(T78, T83, T65))
U19_ggaa(T78, T80, T83, T65, ackA_out_gga(T78, T83, T65)) → pJ_out_ggaa(T78, T80, T83, T65)
U17_ggaaa(T78, T79, T80, X182, T65, pJ_out_ggaa(T78, T80, X182, T65)) → pD_out_ggaaa(T78, T79, T80, X182, T65)
U3_gga(T78, T79, T65, pD_out_ggaaa(T78, T79, X181, X182, T65)) → ackA_out_gga(s(T78), s(s(T79)), T65)
U15_gaa(T70, T71, T65, ackA_out_gga(T70, T71, T65)) → pC_out_gaa(T70, T71, T65)
U2_gga(T70, T65, pC_out_gaa(T70, X162, T65)) → ackA_out_gga(s(T70), s(0), T65)
U9_gaa(T20, T23, T22, ackA_out_gga(T20, T23, T22)) → pB_out_gaa(T20, T23, T22)
U1_gga(T20, T22, pB_out_gaa(T20, X36, T22)) → ackA_out_gga(s(s(T20)), 0, T22)

The argument filtering Pi contains the following mapping:
ackA_in_gga(x1, x2, x3) = ackA_in_gga(x1, x2)
0 = 0
ackA_out_gga(x1, x2, x3) = ackA_out_gga(x1, x2, x3)
s(x1) = s(x1)
U1_gga(x1, x2, x3) = U1_gga(x1, x3)
pB_in_gaa(x1, x2, x3) = pB_in_gaa(x1)
U8_gaa(x1, x2, x3, x4) = U8_gaa(x1, x4)
ackE_in_ga(x1, x2) = ackE_in_ga(x1)
U4_ga(x1, x2, x3) = U4_ga(x1, x3)
ackF_in_ga(x1, x2) = ackF_in_ga(x1)
ackF_out_ga(x1, x2) = ackF_out_ga(x1, x2)
U5_ga(x1, x2, x3) = U5_ga(x1, x3)
pG_in_gaa(x1, x2, x3) = pG_in_gaa(x1)
U10_gaa(x1, x2, x3, x4) = U10_gaa(x1, x4)
ackE_out_ga(x1, x2) = ackE_out_ga(x1, x2)
U11_gaa(x1, x2, x3, x4) = U11_gaa(x1, x2, x4)
ackH_in_gga(x1, x2, x3) = ackH_in_gga(x1, x2)
ackH_out_gga(x1, x2, x3) = ackH_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3) = U6_gga(x1, x3)
U7_gga(x1, x2, x3, x4) = U7_gga(x1, x2, x4)
pI_in_ggaa(x1, x2, x3, x4) = pI_in_ggaa(x1, x2)
U12_ggaa(x1, x2, x3, x4, x5) = U12_ggaa(x1, x2, x5)
U13_ggaa(x1, x2, x3, x4, x5) = U13_ggaa(x1, x2, x3, x5)
pI_out_ggaa(x1, x2, x3, x4) = pI_out_ggaa(x1, x2, x3, x4)
pG_out_gaa(x1, x2, x3) = pG_out_gaa(x1, x2, x3)
U9_gaa(x1, x2, x3, x4) = U9_gaa(x1, x2, x4)
U2_gga(x1, x2, x3) = U2_gga(x1, x3)
pC_in_gaa(x1, x2, x3) = pC_in_gaa(x1)
U14_gaa(x1, x2, x3, x4) = U14_gaa(x1, x4)
U15_gaa(x1, x2, x3, x4) = U15_gaa(x1, x2, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x1, x2, x4)
pD_in_ggaaa(x1, x2, x3, x4, x5) = pD_in_ggaaa(x1, x2)
U16_ggaaa(x1, x2, x3, x4, x5, x6) = U16_ggaaa(x1, x2, x6)
U17_ggaaa(x1, x2, x3, x4, x5, x6) = U17_ggaaa(x1, x2, x3, x6)
pJ_in_ggaa(x1, x2, x3, x4) = pJ_in_ggaa(x1, x2)
U18_ggaa(x1, x2, x3, x4, x5) = U18_ggaa(x1, x2, x5)
U19_ggaa(x1, x2, x3, x4, x5) = U19_ggaa(x1, x2, x3, x5)
pJ_out_ggaa(x1, x2, x3, x4) = pJ_out_ggaa(x1, x2, x3, x4)
pD_out_ggaaa(x1, x2, x3, x4, x5) = pD_out_ggaaa(x1, x2, x3, x4, x5)
pC_out_gaa(x1, x2, x3) = pC_out_gaa(x1, x2, x3)
pB_out_gaa(x1, x2, x3) = pB_out_gaa(x1, x2, x3)
ACKA_IN_GGA(x1, x2, x3) = ACKA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3) = U1_GGA(x1, x3)
PB_IN_GAA(x1, x2, x3) = PB_IN_GAA(x1)
U8_GAA(x1, x2, x3, x4) = U8_GAA(x1, x4)
ACKE_IN_GA(x1, x2) = ACKE_IN_GA(x1)
U4_GA(x1, x2, x3) = U4_GA(x1, x3)
ACKF_IN_GA(x1, x2) = ACKF_IN_GA(x1)
U5_GA(x1, x2, x3) = U5_GA(x1, x3)
PG_IN_GAA(x1, x2, x3) = PG_IN_GAA(x1)
U10_GAA(x1, x2, x3, x4) = U10_GAA(x1, x4)
U11_GAA(x1, x2, x3, x4) = U11_GAA(x1, x2, x4)
ACKH_IN_GGA(x1, x2, x3) = ACKH_IN_GGA(x1, x2)
U6_GGA(x1, x2, x3) = U6_GGA(x1, x3)
U7_GGA(x1, x2, x3, x4) = U7_GGA(x1, x2, x4)
PI_IN_GGAA(x1, x2, x3, x4) = PI_IN_GGAA(x1, x2)
U12_GGAA(x1, x2, x3, x4, x5) = U12_GGAA(x1, x2, x5)
U13_GGAA(x1, x2, x3, x4, x5) = U13_GGAA(x1, x2, x3, x5)
U9_GAA(x1, x2, x3, x4) = U9_GAA(x1, x2, x4)
U2_GGA(x1, x2, x3) = U2_GGA(x1, x3)
PC_IN_GAA(x1, x2, x3) = PC_IN_GAA(x1)
U14_GAA(x1, x2, x3, x4) = U14_GAA(x1, x4)
U15_GAA(x1, x2, x3, x4) = U15_GAA(x1, x2, x4)
U3_GGA(x1, x2, x3, x4) = U3_GGA(x1, x2, x4)
PD_IN_GGAAA(x1, x2, x3, x4, x5) = PD_IN_GGAAA(x1, x2)
U16_GGAAA(x1, x2, x3, x4, x5, x6) = U16_GGAAA(x1, x2, x6)
U17_GGAAA(x1, x2, x3, x4, x5, x6) = U17_GGAAA(x1, x2, x3, x6)
PJ_IN_GGAA(x1, x2, x3, x4) = PJ_IN_GGAA(x1, x2)
U18_GGAA(x1, x2, x3, x4, x5) = U18_GGAA(x1, x2, x5)
U19_GGAA(x1, x2, x3, x4, x5) = U19_GGAA(x1, x2, x3, x5)

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

(4) Obligation:

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

ACKA_IN_GGA(s(s(T20)), 0, T22) → U1_GGA(T20, T22, pB_in_gaa(T20, X36, T22))
ACKA_IN_GGA(s(s(T20)), 0, T22) → PB_IN_GAA(T20, X36, T22)
PB_IN_GAA(T20, T23, T22) → U8_GAA(T20, T23, T22, ackE_in_ga(T20, T23))
PB_IN_GAA(T20, T23, T22) → ACKE_IN_GA(T20, T23)
ACKE_IN_GA(T28, X60) → U4_GA(T28, X60, ackF_in_ga(T28, X60))
ACKE_IN_GA(T28, X60) → ACKF_IN_GA(T28, X60)
ACKF_IN_GA(s(T32), X83) → U5_GA(T32, X83, pG_in_gaa(T32, X82, X83))
ACKF_IN_GA(s(T32), X83) → PG_IN_GAA(T32, X82, X83)
PG_IN_GAA(T32, T33, X83) → U10_GAA(T32, T33, X83, ackE_in_ga(T32, T33))
PG_IN_GAA(T32, T33, X83) → ACKE_IN_GA(T32, T33)
U10_GAA(T32, T33, X83, ackE_out_ga(T32, T33)) → U11_GAA(T32, T33, X83, ackH_in_gga(T32, T33, X83))
U10_GAA(T32, T33, X83, ackE_out_ga(T32, T33)) → ACKH_IN_GGA(T32, T33, X83)
ACKH_IN_GGA(s(T45), 0, X109) → U6_GGA(T45, X109, ackF_in_ga(T45, X109))
ACKH_IN_GGA(s(T45), 0, X109) → ACKF_IN_GA(T45, X109)
ACKH_IN_GGA(s(T50), s(T51), X125) → U7_GGA(T50, T51, X125, pI_in_ggaa(T50, T51, X124, X125))
ACKH_IN_GGA(s(T50), s(T51), X125) → PI_IN_GGAA(T50, T51, X124, X125)
PI_IN_GGAA(T50, T51, T52, X125) → U12_GGAA(T50, T51, T52, X125, ackH_in_gga(s(T50), T51, T52))
PI_IN_GGAA(T50, T51, T52, X125) → ACKH_IN_GGA(s(T50), T51, T52)
U12_GGAA(T50, T51, T52, X125, ackH_out_gga(s(T50), T51, T52)) → U13_GGAA(T50, T51, T52, X125, ackH_in_gga(T50, T52, X125))
U12_GGAA(T50, T51, T52, X125, ackH_out_gga(s(T50), T51, T52)) → ACKH_IN_GGA(T50, T52, X125)
U8_GAA(T20, T23, T22, ackE_out_ga(T20, T23)) → U9_GAA(T20, T23, T22, ackA_in_gga(T20, T23, T22))
U8_GAA(T20, T23, T22, ackE_out_ga(T20, T23)) → ACKA_IN_GGA(T20, T23, T22)
ACKA_IN_GGA(s(T70), s(0), T65) → U2_GGA(T70, T65, pC_in_gaa(T70, X162, T65))
ACKA_IN_GGA(s(T70), s(0), T65) → PC_IN_GAA(T70, X162, T65)
PC_IN_GAA(T70, T71, T65) → U14_GAA(T70, T71, T65, ackF_in_ga(T70, T71))
PC_IN_GAA(T70, T71, T65) → ACKF_IN_GA(T70, T71)
U14_GAA(T70, T71, T65, ackF_out_ga(T70, T71)) → U15_GAA(T70, T71, T65, ackA_in_gga(T70, T71, T65))
U14_GAA(T70, T71, T65, ackF_out_ga(T70, T71)) → ACKA_IN_GGA(T70, T71, T65)
ACKA_IN_GGA(s(T78), s(s(T79)), T65) → U3_GGA(T78, T79, T65, pD_in_ggaaa(T78, T79, X181, X182, T65))
ACKA_IN_GGA(s(T78), s(s(T79)), T65) → PD_IN_GGAAA(T78, T79, X181, X182, T65)
PD_IN_GGAAA(T78, T79, T80, X182, T65) → U16_GGAAA(T78, T79, T80, X182, T65, ackH_in_gga(s(T78), T79, T80))
PD_IN_GGAAA(T78, T79, T80, X182, T65) → ACKH_IN_GGA(s(T78), T79, T80)
U16_GGAAA(T78, T79, T80, X182, T65, ackH_out_gga(s(T78), T79, T80)) → U17_GGAAA(T78, T79, T80, X182, T65, pJ_in_ggaa(T78, T80, X182, T65))
U16_GGAAA(T78, T79, T80, X182, T65, ackH_out_gga(s(T78), T79, T80)) → PJ_IN_GGAA(T78, T80, X182, T65)
PJ_IN_GGAA(T78, T80, T83, T65) → U18_GGAA(T78, T80, T83, T65, ackH_in_gga(T78, T80, T83))
PJ_IN_GGAA(T78, T80, T83, T65) → ACKH_IN_GGA(T78, T80, T83)
U18_GGAA(T78, T80, T83, T65, ackH_out_gga(T78, T80, T83)) → U19_GGAA(T78, T80, T83, T65, ackA_in_gga(T78, T83, T65))
U18_GGAA(T78, T80, T83, T65, ackH_out_gga(T78, T80, T83)) → ACKA_IN_GGA(T78, T83, T65)

The TRS R consists of the following rules:

ackA_in_gga(0, T5, s(T5)) → ackA_out_gga(0, T5, s(T5))
ackA_in_gga(s(0), 0, s(s(0))) → ackA_out_gga(s(0), 0, s(s(0)))
ackA_in_gga(s(s(T20)), 0, T22) → U1_gga(T20, T22, pB_in_gaa(T20, X36, T22))
pB_in_gaa(T20, T23, T22) → U8_gaa(T20, T23, T22, ackE_in_ga(T20, T23))
ackE_in_ga(T28, X60) → U4_ga(T28, X60, ackF_in_ga(T28, X60))
ackF_in_ga(0, s(s(0))) → ackF_out_ga(0, s(s(0)))
ackF_in_ga(s(T32), X83) → U5_ga(T32, X83, pG_in_gaa(T32, X82, X83))
pG_in_gaa(T32, T33, X83) → U10_gaa(T32, T33, X83, ackE_in_ga(T32, T33))
U10_gaa(T32, T33, X83, ackE_out_ga(T32, T33)) → U11_gaa(T32, T33, X83, ackH_in_gga(T32, T33, X83))
ackH_in_gga(0, T40, s(T40)) → ackH_out_gga(0, T40, s(T40))
ackH_in_gga(s(T45), 0, X109) → U6_gga(T45, X109, ackF_in_ga(T45, X109))
U6_gga(T45, X109, ackF_out_ga(T45, X109)) → ackH_out_gga(s(T45), 0, X109)
ackH_in_gga(s(T50), s(T51), X125) → U7_gga(T50, T51, X125, pI_in_ggaa(T50, T51, X124, X125))
pI_in_ggaa(T50, T51, T52, X125) → U12_ggaa(T50, T51, T52, X125, ackH_in_gga(s(T50), T51, T52))
U12_ggaa(T50, T51, T52, X125, ackH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, X125, ackH_in_gga(T50, T52, X125))
U13_ggaa(T50, T51, T52, X125, ackH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U7_gga(T50, T51, X125, pI_out_ggaa(T50, T51, X124, X125)) → ackH_out_gga(s(T50), s(T51), X125)
U11_gaa(T32, T33, X83, ackH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)
U5_ga(T32, X83, pG_out_gaa(T32, X82, X83)) → ackF_out_ga(s(T32), X83)
U4_ga(T28, X60, ackF_out_ga(T28, X60)) → ackE_out_ga(T28, X60)
U8_gaa(T20, T23, T22, ackE_out_ga(T20, T23)) → U9_gaa(T20, T23, T22, ackA_in_gga(T20, T23, T22))
ackA_in_gga(s(T70), s(0), T65) → U2_gga(T70, T65, pC_in_gaa(T70, X162, T65))
pC_in_gaa(T70, T71, T65) → U14_gaa(T70, T71, T65, ackF_in_ga(T70, T71))
U14_gaa(T70, T71, T65, ackF_out_ga(T70, T71)) → U15_gaa(T70, T71, T65, ackA_in_gga(T70, T71, T65))
ackA_in_gga(s(T78), s(s(T79)), T65) → U3_gga(T78, T79, T65, pD_in_ggaaa(T78, T79, X181, X182, T65))
pD_in_ggaaa(T78, T79, T80, X182, T65) → U16_ggaaa(T78, T79, T80, X182, T65, ackH_in_gga(s(T78), T79, T80))
U16_ggaaa(T78, T79, T80, X182, T65, ackH_out_gga(s(T78), T79, T80)) → U17_ggaaa(T78, T79, T80, X182, T65, pJ_in_ggaa(T78, T80, X182, T65))
pJ_in_ggaa(T78, T80, T83, T65) → U18_ggaa(T78, T80, T83, T65, ackH_in_gga(T78, T80, T83))
U18_ggaa(T78, T80, T83, T65, ackH_out_gga(T78, T80, T83)) → U19_ggaa(T78, T80, T83, T65, ackA_in_gga(T78, T83, T65))
U19_ggaa(T78, T80, T83, T65, ackA_out_gga(T78, T83, T65)) → pJ_out_ggaa(T78, T80, T83, T65)
U17_ggaaa(T78, T79, T80, X182, T65, pJ_out_ggaa(T78, T80, X182, T65)) → pD_out_ggaaa(T78, T79, T80, X182, T65)
U3_gga(T78, T79, T65, pD_out_ggaaa(T78, T79, X181, X182, T65)) → ackA_out_gga(s(T78), s(s(T79)), T65)
U15_gaa(T70, T71, T65, ackA_out_gga(T70, T71, T65)) → pC_out_gaa(T70, T71, T65)
U2_gga(T70, T65, pC_out_gaa(T70, X162, T65)) → ackA_out_gga(s(T70), s(0), T65)
U9_gaa(T20, T23, T22, ackA_out_gga(T20, T23, T22)) → pB_out_gaa(T20, T23, T22)
U1_gga(T20, T22, pB_out_gaa(T20, X36, T22)) → ackA_out_gga(s(s(T20)), 0, T22)

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

ACKE_IN_GA(T28, X60) → ACKF_IN_GA(T28, X60)
ACKF_IN_GA(s(T32), X83) → PG_IN_GAA(T32, X82, X83)
PG_IN_GAA(T32, T33, X83) → U10_GAA(T32, T33, X83, ackE_in_ga(T32, T33))
U10_GAA(T32, T33, X83, ackE_out_ga(T32, T33)) → ACKH_IN_GGA(T32, T33, X83)
ACKH_IN_GGA(s(T45), 0, X109) → ACKF_IN_GA(T45, X109)
ACKH_IN_GGA(s(T50), s(T51), X125) → PI_IN_GGAA(T50, T51, X124, X125)
PI_IN_GGAA(T50, T51, T52, X125) → U12_GGAA(T50, T51, T52, X125, ackH_in_gga(s(T50), T51, T52))
U12_GGAA(T50, T51, T52, X125, ackH_out_gga(s(T50), T51, T52)) → ACKH_IN_GGA(T50, T52, X125)
PI_IN_GGAA(T50, T51, T52, X125) → ACKH_IN_GGA(s(T50), T51, T52)
PG_IN_GAA(T32, T33, X83) → ACKE_IN_GA(T32, T33)

The TRS R consists of the following rules:

ackA_in_gga(0, T5, s(T5)) → ackA_out_gga(0, T5, s(T5))
ackA_in_gga(s(0), 0, s(s(0))) → ackA_out_gga(s(0), 0, s(s(0)))
ackA_in_gga(s(s(T20)), 0, T22) → U1_gga(T20, T22, pB_in_gaa(T20, X36, T22))
pB_in_gaa(T20, T23, T22) → U8_gaa(T20, T23, T22, ackE_in_ga(T20, T23))
ackE_in_ga(T28, X60) → U4_ga(T28, X60, ackF_in_ga(T28, X60))
ackF_in_ga(0, s(s(0))) → ackF_out_ga(0, s(s(0)))
ackF_in_ga(s(T32), X83) → U5_ga(T32, X83, pG_in_gaa(T32, X82, X83))
pG_in_gaa(T32, T33, X83) → U10_gaa(T32, T33, X83, ackE_in_ga(T32, T33))
U10_gaa(T32, T33, X83, ackE_out_ga(T32, T33)) → U11_gaa(T32, T33, X83, ackH_in_gga(T32, T33, X83))
ackH_in_gga(0, T40, s(T40)) → ackH_out_gga(0, T40, s(T40))
ackH_in_gga(s(T45), 0, X109) → U6_gga(T45, X109, ackF_in_ga(T45, X109))
U6_gga(T45, X109, ackF_out_ga(T45, X109)) → ackH_out_gga(s(T45), 0, X109)
ackH_in_gga(s(T50), s(T51), X125) → U7_gga(T50, T51, X125, pI_in_ggaa(T50, T51, X124, X125))
pI_in_ggaa(T50, T51, T52, X125) → U12_ggaa(T50, T51, T52, X125, ackH_in_gga(s(T50), T51, T52))
U12_ggaa(T50, T51, T52, X125, ackH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, X125, ackH_in_gga(T50, T52, X125))
U13_ggaa(T50, T51, T52, X125, ackH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U7_gga(T50, T51, X125, pI_out_ggaa(T50, T51, X124, X125)) → ackH_out_gga(s(T50), s(T51), X125)
U11_gaa(T32, T33, X83, ackH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)
U5_ga(T32, X83, pG_out_gaa(T32, X82, X83)) → ackF_out_ga(s(T32), X83)
U4_ga(T28, X60, ackF_out_ga(T28, X60)) → ackE_out_ga(T28, X60)
U8_gaa(T20, T23, T22, ackE_out_ga(T20, T23)) → U9_gaa(T20, T23, T22, ackA_in_gga(T20, T23, T22))
ackA_in_gga(s(T70), s(0), T65) → U2_gga(T70, T65, pC_in_gaa(T70, X162, T65))
pC_in_gaa(T70, T71, T65) → U14_gaa(T70, T71, T65, ackF_in_ga(T70, T71))
U14_gaa(T70, T71, T65, ackF_out_ga(T70, T71)) → U15_gaa(T70, T71, T65, ackA_in_gga(T70, T71, T65))
ackA_in_gga(s(T78), s(s(T79)), T65) → U3_gga(T78, T79, T65, pD_in_ggaaa(T78, T79, X181, X182, T65))
pD_in_ggaaa(T78, T79, T80, X182, T65) → U16_ggaaa(T78, T79, T80, X182, T65, ackH_in_gga(s(T78), T79, T80))
U16_ggaaa(T78, T79, T80, X182, T65, ackH_out_gga(s(T78), T79, T80)) → U17_ggaaa(T78, T79, T80, X182, T65, pJ_in_ggaa(T78, T80, X182, T65))
pJ_in_ggaa(T78, T80, T83, T65) → U18_ggaa(T78, T80, T83, T65, ackH_in_gga(T78, T80, T83))
U18_ggaa(T78, T80, T83, T65, ackH_out_gga(T78, T80, T83)) → U19_ggaa(T78, T80, T83, T65, ackA_in_gga(T78, T83, T65))
U19_ggaa(T78, T80, T83, T65, ackA_out_gga(T78, T83, T65)) → pJ_out_ggaa(T78, T80, T83, T65)
U17_ggaaa(T78, T79, T80, X182, T65, pJ_out_ggaa(T78, T80, X182, T65)) → pD_out_ggaaa(T78, T79, T80, X182, T65)
U3_gga(T78, T79, T65, pD_out_ggaaa(T78, T79, X181, X182, T65)) → ackA_out_gga(s(T78), s(s(T79)), T65)
U15_gaa(T70, T71, T65, ackA_out_gga(T70, T71, T65)) → pC_out_gaa(T70, T71, T65)
U2_gga(T70, T65, pC_out_gaa(T70, X162, T65)) → ackA_out_gga(s(T70), s(0), T65)
U9_gaa(T20, T23, T22, ackA_out_gga(T20, T23, T22)) → pB_out_gaa(T20, T23, T22)
U1_gga(T20, T22, pB_out_gaa(T20, X36, T22)) → ackA_out_gga(s(s(T20)), 0, T22)

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

ACKE_IN_GA(T28, X60) → ACKF_IN_GA(T28, X60)
ACKF_IN_GA(s(T32), X83) → PG_IN_GAA(T32, X82, X83)
PG_IN_GAA(T32, T33, X83) → U10_GAA(T32, T33, X83, ackE_in_ga(T32, T33))
U10_GAA(T32, T33, X83, ackE_out_ga(T32, T33)) → ACKH_IN_GGA(T32, T33, X83)
ACKH_IN_GGA(s(T45), 0, X109) → ACKF_IN_GA(T45, X109)
ACKH_IN_GGA(s(T50), s(T51), X125) → PI_IN_GGAA(T50, T51, X124, X125)
PI_IN_GGAA(T50, T51, T52, X125) → U12_GGAA(T50, T51, T52, X125, ackH_in_gga(s(T50), T51, T52))
U12_GGAA(T50, T51, T52, X125, ackH_out_gga(s(T50), T51, T52)) → ACKH_IN_GGA(T50, T52, X125)
PI_IN_GGAA(T50, T51, T52, X125) → ACKH_IN_GGA(s(T50), T51, T52)
PG_IN_GAA(T32, T33, X83) → ACKE_IN_GA(T32, T33)

The TRS R consists of the following rules:

ackE_in_ga(T28, X60) → U4_ga(T28, X60, ackF_in_ga(T28, X60))
ackH_in_gga(s(T45), 0, X109) → U6_gga(T45, X109, ackF_in_ga(T45, X109))
ackH_in_gga(s(T50), s(T51), X125) → U7_gga(T50, T51, X125, pI_in_ggaa(T50, T51, X124, X125))
U4_ga(T28, X60, ackF_out_ga(T28, X60)) → ackE_out_ga(T28, X60)
U6_gga(T45, X109, ackF_out_ga(T45, X109)) → ackH_out_gga(s(T45), 0, X109)
U7_gga(T50, T51, X125, pI_out_ggaa(T50, T51, X124, X125)) → ackH_out_gga(s(T50), s(T51), X125)
ackF_in_ga(0, s(s(0))) → ackF_out_ga(0, s(s(0)))
ackF_in_ga(s(T32), X83) → U5_ga(T32, X83, pG_in_gaa(T32, X82, X83))
pI_in_ggaa(T50, T51, T52, X125) → U12_ggaa(T50, T51, T52, X125, ackH_in_gga(s(T50), T51, T52))
U5_ga(T32, X83, pG_out_gaa(T32, X82, X83)) → ackF_out_ga(s(T32), X83)
U12_ggaa(T50, T51, T52, X125, ackH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, X125, ackH_in_gga(T50, T52, X125))
pG_in_gaa(T32, T33, X83) → U10_gaa(T32, T33, X83, ackE_in_ga(T32, T33))
U13_ggaa(T50, T51, T52, X125, ackH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U10_gaa(T32, T33, X83, ackE_out_ga(T32, T33)) → U11_gaa(T32, T33, X83, ackH_in_gga(T32, T33, X83))
ackH_in_gga(0, T40, s(T40)) → ackH_out_gga(0, T40, s(T40))
U11_gaa(T32, T33, X83, ackH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)

The argument filtering Pi contains the following mapping:
0 = 0
s(x1) = s(x1)
ackE_in_ga(x1, x2) = ackE_in_ga(x1)
U4_ga(x1, x2, x3) = U4_ga(x1, x3)
ackF_in_ga(x1, x2) = ackF_in_ga(x1)
ackF_out_ga(x1, x2) = ackF_out_ga(x1, x2)
U5_ga(x1, x2, x3) = U5_ga(x1, x3)
pG_in_gaa(x1, x2, x3) = pG_in_gaa(x1)
U10_gaa(x1, x2, x3, x4) = U10_gaa(x1, x4)
ackE_out_ga(x1, x2) = ackE_out_ga(x1, x2)
U11_gaa(x1, x2, x3, x4) = U11_gaa(x1, x2, x4)
ackH_in_gga(x1, x2, x3) = ackH_in_gga(x1, x2)
ackH_out_gga(x1, x2, x3) = ackH_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3) = U6_gga(x1, x3)
U7_gga(x1, x2, x3, x4) = U7_gga(x1, x2, x4)
pI_in_ggaa(x1, x2, x3, x4) = pI_in_ggaa(x1, x2)
U12_ggaa(x1, x2, x3, x4, x5) = U12_ggaa(x1, x2, x5)
U13_ggaa(x1, x2, x3, x4, x5) = U13_ggaa(x1, x2, x3, x5)
pI_out_ggaa(x1, x2, x3, x4) = pI_out_ggaa(x1, x2, x3, x4)
pG_out_gaa(x1, x2, x3) = pG_out_gaa(x1, x2, x3)
ACKE_IN_GA(x1, x2) = ACKE_IN_GA(x1)
ACKF_IN_GA(x1, x2) = ACKF_IN_GA(x1)
PG_IN_GAA(x1, x2, x3) = PG_IN_GAA(x1)
U10_GAA(x1, x2, x3, x4) = U10_GAA(x1, x4)
ACKH_IN_GGA(x1, x2, x3) = ACKH_IN_GGA(x1, x2)
PI_IN_GGAA(x1, x2, x3, x4) = PI_IN_GGAA(x1, x2)
U12_GGAA(x1, x2, x3, x4, x5) = U12_GGAA(x1, x2, x5)

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:

ACKE_IN_GA(T28) → ACKF_IN_GA(T28)
ACKF_IN_GA(s(T32)) → PG_IN_GAA(T32)
PG_IN_GAA(T32) → U10_GAA(T32, ackE_in_ga(T32))
U10_GAA(T32, ackE_out_ga(T32, T33)) → ACKH_IN_GGA(T32, T33)
ACKH_IN_GGA(s(T45), 0) → ACKF_IN_GA(T45)
ACKH_IN_GGA(s(T50), s(T51)) → PI_IN_GGAA(T50, T51)
PI_IN_GGAA(T50, T51) → U12_GGAA(T50, T51, ackH_in_gga(s(T50), T51))
U12_GGAA(T50, T51, ackH_out_gga(s(T50), T51, T52)) → ACKH_IN_GGA(T50, T52)
PI_IN_GGAA(T50, T51) → ACKH_IN_GGA(s(T50), T51)
PG_IN_GAA(T32) → ACKE_IN_GA(T32)

The TRS R consists of the following rules:

ackE_in_ga(T28) → U4_ga(T28, ackF_in_ga(T28))
ackH_in_gga(s(T45), 0) → U6_gga(T45, ackF_in_ga(T45))
ackH_in_gga(s(T50), s(T51)) → U7_gga(T50, T51, pI_in_ggaa(T50, T51))
U4_ga(T28, ackF_out_ga(T28, X60)) → ackE_out_ga(T28, X60)
U6_gga(T45, ackF_out_ga(T45, X109)) → ackH_out_gga(s(T45), 0, X109)
U7_gga(T50, T51, pI_out_ggaa(T50, T51, X124, X125)) → ackH_out_gga(s(T50), s(T51), X125)
ackF_in_ga(0) → ackF_out_ga(0, s(s(0)))
ackF_in_ga(s(T32)) → U5_ga(T32, pG_in_gaa(T32))
pI_in_ggaa(T50, T51) → U12_ggaa(T50, T51, ackH_in_gga(s(T50), T51))
U5_ga(T32, pG_out_gaa(T32, X82, X83)) → ackF_out_ga(s(T32), X83)
U12_ggaa(T50, T51, ackH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, ackH_in_gga(T50, T52))
pG_in_gaa(T32) → U10_gaa(T32, ackE_in_ga(T32))
U13_ggaa(T50, T51, T52, ackH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U10_gaa(T32, ackE_out_ga(T32, T33)) → U11_gaa(T32, T33, ackH_in_gga(T32, T33))
ackH_in_gga(0, T40) → ackH_out_gga(0, T40, s(T40))
U11_gaa(T32, T33, ackH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)

The set Q consists of the following terms:

ackE_in_ga(x0)
ackH_in_gga(x0, x1)
U4_ga(x0, x1)
U6_gga(x0, x1)
U7_gga(x0, x1, x2)
ackF_in_ga(x0)
pI_in_ggaa(x0, x1)
U5_ga(x0, x1)
U12_ggaa(x0, x1, x2)
pG_in_gaa(x0)
U13_ggaa(x0, x1, x2, x3)
U10_gaa(x0, x1)
U11_gaa(x0, x1, x2)

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

(12) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule PG_IN_GAA(T32) → U10_GAA(T32, ackE_in_ga(T32)) at position [1] we obtained the following new rules [LPAR04]:

PG_IN_GAA(T32) → U10_GAA(T32, U4_ga(T32, ackF_in_ga(T32)))

(13) Obligation:

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

ACKE_IN_GA(T28) → ACKF_IN_GA(T28)
ACKF_IN_GA(s(T32)) → PG_IN_GAA(T32)
U10_GAA(T32, ackE_out_ga(T32, T33)) → ACKH_IN_GGA(T32, T33)
ACKH_IN_GGA(s(T45), 0) → ACKF_IN_GA(T45)
ACKH_IN_GGA(s(T50), s(T51)) → PI_IN_GGAA(T50, T51)
PI_IN_GGAA(T50, T51) → U12_GGAA(T50, T51, ackH_in_gga(s(T50), T51))
U12_GGAA(T50, T51, ackH_out_gga(s(T50), T51, T52)) → ACKH_IN_GGA(T50, T52)
PI_IN_GGAA(T50, T51) → ACKH_IN_GGA(s(T50), T51)
PG_IN_GAA(T32) → ACKE_IN_GA(T32)
PG_IN_GAA(T32) → U10_GAA(T32, U4_ga(T32, ackF_in_ga(T32)))

The TRS R consists of the following rules:

ackE_in_ga(T28) → U4_ga(T28, ackF_in_ga(T28))
ackH_in_gga(s(T45), 0) → U6_gga(T45, ackF_in_ga(T45))
ackH_in_gga(s(T50), s(T51)) → U7_gga(T50, T51, pI_in_ggaa(T50, T51))
U4_ga(T28, ackF_out_ga(T28, X60)) → ackE_out_ga(T28, X60)
U6_gga(T45, ackF_out_ga(T45, X109)) → ackH_out_gga(s(T45), 0, X109)
U7_gga(T50, T51, pI_out_ggaa(T50, T51, X124, X125)) → ackH_out_gga(s(T50), s(T51), X125)
ackF_in_ga(0) → ackF_out_ga(0, s(s(0)))
ackF_in_ga(s(T32)) → U5_ga(T32, pG_in_gaa(T32))
pI_in_ggaa(T50, T51) → U12_ggaa(T50, T51, ackH_in_gga(s(T50), T51))
U5_ga(T32, pG_out_gaa(T32, X82, X83)) → ackF_out_ga(s(T32), X83)
U12_ggaa(T50, T51, ackH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, ackH_in_gga(T50, T52))
pG_in_gaa(T32) → U10_gaa(T32, ackE_in_ga(T32))
U13_ggaa(T50, T51, T52, ackH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U10_gaa(T32, ackE_out_ga(T32, T33)) → U11_gaa(T32, T33, ackH_in_gga(T32, T33))
ackH_in_gga(0, T40) → ackH_out_gga(0, T40, s(T40))
U11_gaa(T32, T33, ackH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)

The set Q consists of the following terms:

ackE_in_ga(x0)
ackH_in_gga(x0, x1)
U4_ga(x0, x1)
U6_gga(x0, x1)
U7_gga(x0, x1, x2)
ackF_in_ga(x0)
pI_in_ggaa(x0, x1)
U5_ga(x0, x1)
U12_ggaa(x0, x1, x2)
pG_in_gaa(x0)
U13_ggaa(x0, x1, x2, x3)
U10_gaa(x0, x1)
U11_gaa(x0, x1, x2)

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

(14) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

ACKH_IN_GGA(s(T45), 0) → ACKF_IN_GA(T45)
PI_IN_GGAA(T50, T51) → U12_GGAA(T50, T51, ackH_in_gga(s(T50), T51))
PG_IN_GAA(T32) → ACKE_IN_GA(T32)
PG_IN_GAA(T32) → U10_GAA(T32, U4_ga(T32, ackF_in_ga(T32)))

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

POL(0) = 1
POL(ACKE_IN_GA(x₁)) = x₁
POL(ACKF_IN_GA(x₁)) = x₁
POL(ACKH_IN_GGA(x₁, x₂)) = x₁
POL(PG_IN_GAA(x₁)) = 1 + x₁
POL(PI_IN_GGAA(x₁, x₂)) = 1 + x₁
POL(U10_GAA(x₁, x₂)) = x₁
POL(U10_gaa(x₁, x₂)) = 0
POL(U11_gaa(x₁, x₂, x₃)) = 0
POL(U12_GGAA(x₁, x₂, x₃)) = x₁
POL(U12_ggaa(x₁, x₂, x₃)) = 0
POL(U13_ggaa(x₁, x₂, x₃, x₄)) = 0
POL(U4_ga(x₁, x₂)) = 0
POL(U5_ga(x₁, x₂)) = 0
POL(U6_gga(x₁, x₂)) = 0
POL(U7_gga(x₁, x₂, x₃)) = 0
POL(ackE_in_ga(x₁)) = 0
POL(ackE_out_ga(x₁, x₂)) = 0
POL(ackF_in_ga(x₁)) = x₁
POL(ackF_out_ga(x₁, x₂)) = 0
POL(ackH_in_gga(x₁, x₂)) = 1 + x₁ + x₂
POL(ackH_out_gga(x₁, x₂, x₃)) = x₁
POL(pG_in_gaa(x₁)) = 0
POL(pG_out_gaa(x₁, x₂, x₃)) = 0
POL(pI_in_ggaa(x₁, x₂)) = 0
POL(pI_out_ggaa(x₁, x₂, x₃, x₄)) = 0
POL(s(x₁)) = 1 + x₁

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

(15) Obligation:

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

ACKE_IN_GA(T28) → ACKF_IN_GA(T28)
ACKF_IN_GA(s(T32)) → PG_IN_GAA(T32)
U10_GAA(T32, ackE_out_ga(T32, T33)) → ACKH_IN_GGA(T32, T33)
ACKH_IN_GGA(s(T50), s(T51)) → PI_IN_GGAA(T50, T51)
U12_GGAA(T50, T51, ackH_out_gga(s(T50), T51, T52)) → ACKH_IN_GGA(T50, T52)
PI_IN_GGAA(T50, T51) → ACKH_IN_GGA(s(T50), T51)

The TRS R consists of the following rules:

ackE_in_ga(T28) → U4_ga(T28, ackF_in_ga(T28))
ackH_in_gga(s(T45), 0) → U6_gga(T45, ackF_in_ga(T45))
ackH_in_gga(s(T50), s(T51)) → U7_gga(T50, T51, pI_in_ggaa(T50, T51))
U4_ga(T28, ackF_out_ga(T28, X60)) → ackE_out_ga(T28, X60)
U6_gga(T45, ackF_out_ga(T45, X109)) → ackH_out_gga(s(T45), 0, X109)
U7_gga(T50, T51, pI_out_ggaa(T50, T51, X124, X125)) → ackH_out_gga(s(T50), s(T51), X125)
ackF_in_ga(0) → ackF_out_ga(0, s(s(0)))
ackF_in_ga(s(T32)) → U5_ga(T32, pG_in_gaa(T32))
pI_in_ggaa(T50, T51) → U12_ggaa(T50, T51, ackH_in_gga(s(T50), T51))
U5_ga(T32, pG_out_gaa(T32, X82, X83)) → ackF_out_ga(s(T32), X83)
U12_ggaa(T50, T51, ackH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, ackH_in_gga(T50, T52))
pG_in_gaa(T32) → U10_gaa(T32, ackE_in_ga(T32))
U13_ggaa(T50, T51, T52, ackH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U10_gaa(T32, ackE_out_ga(T32, T33)) → U11_gaa(T32, T33, ackH_in_gga(T32, T33))
ackH_in_gga(0, T40) → ackH_out_gga(0, T40, s(T40))
U11_gaa(T32, T33, ackH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)

The set Q consists of the following terms:

ackE_in_ga(x0)
ackH_in_gga(x0, x1)
U4_ga(x0, x1)
U6_gga(x0, x1)
U7_gga(x0, x1, x2)
ackF_in_ga(x0)
pI_in_ggaa(x0, x1)
U5_ga(x0, x1)
U12_ggaa(x0, x1, x2)
pG_in_gaa(x0)
U13_ggaa(x0, x1, x2, x3)
U10_gaa(x0, x1)
U11_gaa(x0, x1, x2)

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

(16) DependencyGraphProof (EQUIVALENT transformation)

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

(17) Obligation:

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

PI_IN_GGAA(T50, T51) → ACKH_IN_GGA(s(T50), T51)
ACKH_IN_GGA(s(T50), s(T51)) → PI_IN_GGAA(T50, T51)

The TRS R consists of the following rules:

ackE_in_ga(T28) → U4_ga(T28, ackF_in_ga(T28))
ackH_in_gga(s(T45), 0) → U6_gga(T45, ackF_in_ga(T45))
ackH_in_gga(s(T50), s(T51)) → U7_gga(T50, T51, pI_in_ggaa(T50, T51))
U4_ga(T28, ackF_out_ga(T28, X60)) → ackE_out_ga(T28, X60)
U6_gga(T45, ackF_out_ga(T45, X109)) → ackH_out_gga(s(T45), 0, X109)
U7_gga(T50, T51, pI_out_ggaa(T50, T51, X124, X125)) → ackH_out_gga(s(T50), s(T51), X125)
ackF_in_ga(0) → ackF_out_ga(0, s(s(0)))
ackF_in_ga(s(T32)) → U5_ga(T32, pG_in_gaa(T32))
pI_in_ggaa(T50, T51) → U12_ggaa(T50, T51, ackH_in_gga(s(T50), T51))
U5_ga(T32, pG_out_gaa(T32, X82, X83)) → ackF_out_ga(s(T32), X83)
U12_ggaa(T50, T51, ackH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, ackH_in_gga(T50, T52))
pG_in_gaa(T32) → U10_gaa(T32, ackE_in_ga(T32))
U13_ggaa(T50, T51, T52, ackH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U10_gaa(T32, ackE_out_ga(T32, T33)) → U11_gaa(T32, T33, ackH_in_gga(T32, T33))
ackH_in_gga(0, T40) → ackH_out_gga(0, T40, s(T40))
U11_gaa(T32, T33, ackH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)

The set Q consists of the following terms:

ackE_in_ga(x0)
ackH_in_gga(x0, x1)
U4_ga(x0, x1)
U6_gga(x0, x1)
U7_gga(x0, x1, x2)
ackF_in_ga(x0)
pI_in_ggaa(x0, x1)
U5_ga(x0, x1)
U12_ggaa(x0, x1, x2)
pG_in_gaa(x0)
U13_ggaa(x0, x1, x2, x3)
U10_gaa(x0, x1)
U11_gaa(x0, x1, x2)

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

(18) 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.

(19) Obligation:

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

PI_IN_GGAA(T50, T51) → ACKH_IN_GGA(s(T50), T51)
ACKH_IN_GGA(s(T50), s(T51)) → PI_IN_GGAA(T50, T51)

R is empty.
The set Q consists of the following terms:

ackE_in_ga(x0)
ackH_in_gga(x0, x1)
U4_ga(x0, x1)
U6_gga(x0, x1)
U7_gga(x0, x1, x2)
ackF_in_ga(x0)
pI_in_ggaa(x0, x1)
U5_ga(x0, x1)
U12_ggaa(x0, x1, x2)
pG_in_gaa(x0)
U13_ggaa(x0, x1, x2, x3)
U10_gaa(x0, x1)
U11_gaa(x0, x1, x2)

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

(20) 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].

ackE_in_ga(x0)
ackH_in_gga(x0, x1)
U4_ga(x0, x1)
U6_gga(x0, x1)
U7_gga(x0, x1, x2)
ackF_in_ga(x0)
pI_in_ggaa(x0, x1)
U5_ga(x0, x1)
U12_ggaa(x0, x1, x2)
pG_in_gaa(x0)
U13_ggaa(x0, x1, x2, x3)
U10_gaa(x0, x1)
U11_gaa(x0, x1, x2)

(21) Obligation:

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

PI_IN_GGAA(T50, T51) → ACKH_IN_GGA(s(T50), T51)
ACKH_IN_GGA(s(T50), s(T51)) → PI_IN_GGAA(T50, T51)

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

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

ACKH_IN_GGA(s(T50), s(T51)) → PI_IN_GGAA(T50, T51)
The graph contains the following edges 1 > 1, 2 > 2
PI_IN_GGAA(T50, T51) → ACKH_IN_GGA(s(T50), T51)
The graph contains the following edges 2 >= 2

(23) YES

(24) Obligation:

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

ACKA_IN_GGA(s(s(T20)), 0, T22) → PB_IN_GAA(T20, X36, T22)
PB_IN_GAA(T20, T23, T22) → U8_GAA(T20, T23, T22, ackE_in_ga(T20, T23))
U8_GAA(T20, T23, T22, ackE_out_ga(T20, T23)) → ACKA_IN_GGA(T20, T23, T22)
ACKA_IN_GGA(s(T70), s(0), T65) → PC_IN_GAA(T70, X162, T65)
PC_IN_GAA(T70, T71, T65) → U14_GAA(T70, T71, T65, ackF_in_ga(T70, T71))
U14_GAA(T70, T71, T65, ackF_out_ga(T70, T71)) → ACKA_IN_GGA(T70, T71, T65)
ACKA_IN_GGA(s(T78), s(s(T79)), T65) → PD_IN_GGAAA(T78, T79, X181, X182, T65)
PD_IN_GGAAA(T78, T79, T80, X182, T65) → U16_GGAAA(T78, T79, T80, X182, T65, ackH_in_gga(s(T78), T79, T80))
U16_GGAAA(T78, T79, T80, X182, T65, ackH_out_gga(s(T78), T79, T80)) → PJ_IN_GGAA(T78, T80, X182, T65)
PJ_IN_GGAA(T78, T80, T83, T65) → U18_GGAA(T78, T80, T83, T65, ackH_in_gga(T78, T80, T83))
U18_GGAA(T78, T80, T83, T65, ackH_out_gga(T78, T80, T83)) → ACKA_IN_GGA(T78, T83, T65)

The TRS R consists of the following rules:

ackA_in_gga(0, T5, s(T5)) → ackA_out_gga(0, T5, s(T5))
ackA_in_gga(s(0), 0, s(s(0))) → ackA_out_gga(s(0), 0, s(s(0)))
ackA_in_gga(s(s(T20)), 0, T22) → U1_gga(T20, T22, pB_in_gaa(T20, X36, T22))
pB_in_gaa(T20, T23, T22) → U8_gaa(T20, T23, T22, ackE_in_ga(T20, T23))
ackE_in_ga(T28, X60) → U4_ga(T28, X60, ackF_in_ga(T28, X60))
ackF_in_ga(0, s(s(0))) → ackF_out_ga(0, s(s(0)))
ackF_in_ga(s(T32), X83) → U5_ga(T32, X83, pG_in_gaa(T32, X82, X83))
pG_in_gaa(T32, T33, X83) → U10_gaa(T32, T33, X83, ackE_in_ga(T32, T33))
U10_gaa(T32, T33, X83, ackE_out_ga(T32, T33)) → U11_gaa(T32, T33, X83, ackH_in_gga(T32, T33, X83))
ackH_in_gga(0, T40, s(T40)) → ackH_out_gga(0, T40, s(T40))
ackH_in_gga(s(T45), 0, X109) → U6_gga(T45, X109, ackF_in_ga(T45, X109))
U6_gga(T45, X109, ackF_out_ga(T45, X109)) → ackH_out_gga(s(T45), 0, X109)
ackH_in_gga(s(T50), s(T51), X125) → U7_gga(T50, T51, X125, pI_in_ggaa(T50, T51, X124, X125))
pI_in_ggaa(T50, T51, T52, X125) → U12_ggaa(T50, T51, T52, X125, ackH_in_gga(s(T50), T51, T52))
U12_ggaa(T50, T51, T52, X125, ackH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, X125, ackH_in_gga(T50, T52, X125))
U13_ggaa(T50, T51, T52, X125, ackH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)
U7_gga(T50, T51, X125, pI_out_ggaa(T50, T51, X124, X125)) → ackH_out_gga(s(T50), s(T51), X125)
U11_gaa(T32, T33, X83, ackH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)
U5_ga(T32, X83, pG_out_gaa(T32, X82, X83)) → ackF_out_ga(s(T32), X83)
U4_ga(T28, X60, ackF_out_ga(T28, X60)) → ackE_out_ga(T28, X60)
U8_gaa(T20, T23, T22, ackE_out_ga(T20, T23)) → U9_gaa(T20, T23, T22, ackA_in_gga(T20, T23, T22))
ackA_in_gga(s(T70), s(0), T65) → U2_gga(T70, T65, pC_in_gaa(T70, X162, T65))
pC_in_gaa(T70, T71, T65) → U14_gaa(T70, T71, T65, ackF_in_ga(T70, T71))
U14_gaa(T70, T71, T65, ackF_out_ga(T70, T71)) → U15_gaa(T70, T71, T65, ackA_in_gga(T70, T71, T65))
ackA_in_gga(s(T78), s(s(T79)), T65) → U3_gga(T78, T79, T65, pD_in_ggaaa(T78, T79, X181, X182, T65))
pD_in_ggaaa(T78, T79, T80, X182, T65) → U16_ggaaa(T78, T79, T80, X182, T65, ackH_in_gga(s(T78), T79, T80))
U16_ggaaa(T78, T79, T80, X182, T65, ackH_out_gga(s(T78), T79, T80)) → U17_ggaaa(T78, T79, T80, X182, T65, pJ_in_ggaa(T78, T80, X182, T65))
pJ_in_ggaa(T78, T80, T83, T65) → U18_ggaa(T78, T80, T83, T65, ackH_in_gga(T78, T80, T83))
U18_ggaa(T78, T80, T83, T65, ackH_out_gga(T78, T80, T83)) → U19_ggaa(T78, T80, T83, T65, ackA_in_gga(T78, T83, T65))
U19_ggaa(T78, T80, T83, T65, ackA_out_gga(T78, T83, T65)) → pJ_out_ggaa(T78, T80, T83, T65)
U17_ggaaa(T78, T79, T80, X182, T65, pJ_out_ggaa(T78, T80, X182, T65)) → pD_out_ggaaa(T78, T79, T80, X182, T65)
U3_gga(T78, T79, T65, pD_out_ggaaa(T78, T79, X181, X182, T65)) → ackA_out_gga(s(T78), s(s(T79)), T65)
U15_gaa(T70, T71, T65, ackA_out_gga(T70, T71, T65)) → pC_out_gaa(T70, T71, T65)
U2_gga(T70, T65, pC_out_gaa(T70, X162, T65)) → ackA_out_gga(s(T70), s(0), T65)
U9_gaa(T20, T23, T22, ackA_out_gga(T20, T23, T22)) → pB_out_gaa(T20, T23, T22)
U1_gga(T20, T22, pB_out_gaa(T20, X36, T22)) → ackA_out_gga(s(s(T20)), 0, T22)

The argument filtering Pi contains the following mapping:
ackA_in_gga(x1, x2, x3) = ackA_in_gga(x1, x2)
0 = 0
ackA_out_gga(x1, x2, x3) = ackA_out_gga(x1, x2, x3)
s(x1) = s(x1)
U1_gga(x1, x2, x3) = U1_gga(x1, x3)
pB_in_gaa(x1, x2, x3) = pB_in_gaa(x1)
U8_gaa(x1, x2, x3, x4) = U8_gaa(x1, x4)
ackE_in_ga(x1, x2) = ackE_in_ga(x1)
U4_ga(x1, x2, x3) = U4_ga(x1, x3)
ackF_in_ga(x1, x2) = ackF_in_ga(x1)
ackF_out_ga(x1, x2) = ackF_out_ga(x1, x2)
U5_ga(x1, x2, x3) = U5_ga(x1, x3)
pG_in_gaa(x1, x2, x3) = pG_in_gaa(x1)
U10_gaa(x1, x2, x3, x4) = U10_gaa(x1, x4)
ackE_out_ga(x1, x2) = ackE_out_ga(x1, x2)
U11_gaa(x1, x2, x3, x4) = U11_gaa(x1, x2, x4)
ackH_in_gga(x1, x2, x3) = ackH_in_gga(x1, x2)
ackH_out_gga(x1, x2, x3) = ackH_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3) = U6_gga(x1, x3)
U7_gga(x1, x2, x3, x4) = U7_gga(x1, x2, x4)
pI_in_ggaa(x1, x2, x3, x4) = pI_in_ggaa(x1, x2)
U12_ggaa(x1, x2, x3, x4, x5) = U12_ggaa(x1, x2, x5)
U13_ggaa(x1, x2, x3, x4, x5) = U13_ggaa(x1, x2, x3, x5)
pI_out_ggaa(x1, x2, x3, x4) = pI_out_ggaa(x1, x2, x3, x4)
pG_out_gaa(x1, x2, x3) = pG_out_gaa(x1, x2, x3)
U9_gaa(x1, x2, x3, x4) = U9_gaa(x1, x2, x4)
U2_gga(x1, x2, x3) = U2_gga(x1, x3)
pC_in_gaa(x1, x2, x3) = pC_in_gaa(x1)
U14_gaa(x1, x2, x3, x4) = U14_gaa(x1, x4)
U15_gaa(x1, x2, x3, x4) = U15_gaa(x1, x2, x4)
U3_gga(x1, x2, x3, x4) = U3_gga(x1, x2, x4)
pD_in_ggaaa(x1, x2, x3, x4, x5) = pD_in_ggaaa(x1, x2)
U16_ggaaa(x1, x2, x3, x4, x5, x6) = U16_ggaaa(x1, x2, x6)
U17_ggaaa(x1, x2, x3, x4, x5, x6) = U17_ggaaa(x1, x2, x3, x6)
pJ_in_ggaa(x1, x2, x3, x4) = pJ_in_ggaa(x1, x2)
U18_ggaa(x1, x2, x3, x4, x5) = U18_ggaa(x1, x2, x5)
U19_ggaa(x1, x2, x3, x4, x5) = U19_ggaa(x1, x2, x3, x5)
pJ_out_ggaa(x1, x2, x3, x4) = pJ_out_ggaa(x1, x2, x3, x4)
pD_out_ggaaa(x1, x2, x3, x4, x5) = pD_out_ggaaa(x1, x2, x3, x4, x5)
pC_out_gaa(x1, x2, x3) = pC_out_gaa(x1, x2, x3)
pB_out_gaa(x1, x2, x3) = pB_out_gaa(x1, x2, x3)
ACKA_IN_GGA(x1, x2, x3) = ACKA_IN_GGA(x1, x2)
PB_IN_GAA(x1, x2, x3) = PB_IN_GAA(x1)
U8_GAA(x1, x2, x3, x4) = U8_GAA(x1, x4)
PC_IN_GAA(x1, x2, x3) = PC_IN_GAA(x1)
U14_GAA(x1, x2, x3, x4) = U14_GAA(x1, x4)
PD_IN_GGAAA(x1, x2, x3, x4, x5) = PD_IN_GGAAA(x1, x2)
U16_GGAAA(x1, x2, x3, x4, x5, x6) = U16_GGAAA(x1, x2, x6)
PJ_IN_GGAA(x1, x2, x3, x4) = PJ_IN_GGAA(x1, x2)
U18_GGAA(x1, x2, x3, x4, x5) = U18_GGAA(x1, x2, x5)

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

(25) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(26) Obligation:

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

ACKA_IN_GGA(s(s(T20)), 0, T22) → PB_IN_GAA(T20, X36, T22)
PB_IN_GAA(T20, T23, T22) → U8_GAA(T20, T23, T22, ackE_in_ga(T20, T23))
U8_GAA(T20, T23, T22, ackE_out_ga(T20, T23)) → ACKA_IN_GGA(T20, T23, T22)
ACKA_IN_GGA(s(T70), s(0), T65) → PC_IN_GAA(T70, X162, T65)
PC_IN_GAA(T70, T71, T65) → U14_GAA(T70, T71, T65, ackF_in_ga(T70, T71))
U14_GAA(T70, T71, T65, ackF_out_ga(T70, T71)) → ACKA_IN_GGA(T70, T71, T65)
ACKA_IN_GGA(s(T78), s(s(T79)), T65) → PD_IN_GGAAA(T78, T79, X181, X182, T65)
PD_IN_GGAAA(T78, T79, T80, X182, T65) → U16_GGAAA(T78, T79, T80, X182, T65, ackH_in_gga(s(T78), T79, T80))
U16_GGAAA(T78, T79, T80, X182, T65, ackH_out_gga(s(T78), T79, T80)) → PJ_IN_GGAA(T78, T80, X182, T65)
PJ_IN_GGAA(T78, T80, T83, T65) → U18_GGAA(T78, T80, T83, T65, ackH_in_gga(T78, T80, T83))
U18_GGAA(T78, T80, T83, T65, ackH_out_gga(T78, T80, T83)) → ACKA_IN_GGA(T78, T83, T65)

The TRS R consists of the following rules:

ackE_in_ga(T28, X60) → U4_ga(T28, X60, ackF_in_ga(T28, X60))
ackF_in_ga(0, s(s(0))) → ackF_out_ga(0, s(s(0)))
ackF_in_ga(s(T32), X83) → U5_ga(T32, X83, pG_in_gaa(T32, X82, X83))
ackH_in_gga(s(T45), 0, X109) → U6_gga(T45, X109, ackF_in_ga(T45, X109))
ackH_in_gga(s(T50), s(T51), X125) → U7_gga(T50, T51, X125, pI_in_ggaa(T50, T51, X124, X125))
ackH_in_gga(0, T40, s(T40)) → ackH_out_gga(0, T40, s(T40))
U4_ga(T28, X60, ackF_out_ga(T28, X60)) → ackE_out_ga(T28, X60)
U5_ga(T32, X83, pG_out_gaa(T32, X82, X83)) → ackF_out_ga(s(T32), X83)
U6_gga(T45, X109, ackF_out_ga(T45, X109)) → ackH_out_gga(s(T45), 0, X109)
U7_gga(T50, T51, X125, pI_out_ggaa(T50, T51, X124, X125)) → ackH_out_gga(s(T50), s(T51), X125)
pG_in_gaa(T32, T33, X83) → U10_gaa(T32, T33, X83, ackE_in_ga(T32, T33))
pI_in_ggaa(T50, T51, T52, X125) → U12_ggaa(T50, T51, T52, X125, ackH_in_gga(s(T50), T51, T52))
U10_gaa(T32, T33, X83, ackE_out_ga(T32, T33)) → U11_gaa(T32, T33, X83, ackH_in_gga(T32, T33, X83))
U12_ggaa(T50, T51, T52, X125, ackH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, X125, ackH_in_gga(T50, T52, X125))
U11_gaa(T32, T33, X83, ackH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)
U13_ggaa(T50, T51, T52, X125, ackH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)

The argument filtering Pi contains the following mapping:
0 = 0
s(x1) = s(x1)
ackE_in_ga(x1, x2) = ackE_in_ga(x1)
U4_ga(x1, x2, x3) = U4_ga(x1, x3)
ackF_in_ga(x1, x2) = ackF_in_ga(x1)
ackF_out_ga(x1, x2) = ackF_out_ga(x1, x2)
U5_ga(x1, x2, x3) = U5_ga(x1, x3)
pG_in_gaa(x1, x2, x3) = pG_in_gaa(x1)
U10_gaa(x1, x2, x3, x4) = U10_gaa(x1, x4)
ackE_out_ga(x1, x2) = ackE_out_ga(x1, x2)
U11_gaa(x1, x2, x3, x4) = U11_gaa(x1, x2, x4)
ackH_in_gga(x1, x2, x3) = ackH_in_gga(x1, x2)
ackH_out_gga(x1, x2, x3) = ackH_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3) = U6_gga(x1, x3)
U7_gga(x1, x2, x3, x4) = U7_gga(x1, x2, x4)
pI_in_ggaa(x1, x2, x3, x4) = pI_in_ggaa(x1, x2)
U12_ggaa(x1, x2, x3, x4, x5) = U12_ggaa(x1, x2, x5)
U13_ggaa(x1, x2, x3, x4, x5) = U13_ggaa(x1, x2, x3, x5)
pI_out_ggaa(x1, x2, x3, x4) = pI_out_ggaa(x1, x2, x3, x4)
pG_out_gaa(x1, x2, x3) = pG_out_gaa(x1, x2, x3)
ACKA_IN_GGA(x1, x2, x3) = ACKA_IN_GGA(x1, x2)
PB_IN_GAA(x1, x2, x3) = PB_IN_GAA(x1)
U8_GAA(x1, x2, x3, x4) = U8_GAA(x1, x4)
PC_IN_GAA(x1, x2, x3) = PC_IN_GAA(x1)
U14_GAA(x1, x2, x3, x4) = U14_GAA(x1, x4)
PD_IN_GGAAA(x1, x2, x3, x4, x5) = PD_IN_GGAAA(x1, x2)
U16_GGAAA(x1, x2, x3, x4, x5, x6) = U16_GGAAA(x1, x2, x6)
PJ_IN_GGAA(x1, x2, x3, x4) = PJ_IN_GGAA(x1, x2)
U18_GGAA(x1, x2, x3, x4, x5) = U18_GGAA(x1, x2, x5)

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

(27) PiDPToQDPProof (SOUND transformation)

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

(28) Obligation:

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

ACKA_IN_GGA(s(s(T20)), 0) → PB_IN_GAA(T20)
PB_IN_GAA(T20) → U8_GAA(T20, ackE_in_ga(T20))
U8_GAA(T20, ackE_out_ga(T20, T23)) → ACKA_IN_GGA(T20, T23)
ACKA_IN_GGA(s(T70), s(0)) → PC_IN_GAA(T70)
PC_IN_GAA(T70) → U14_GAA(T70, ackF_in_ga(T70))
U14_GAA(T70, ackF_out_ga(T70, T71)) → ACKA_IN_GGA(T70, T71)
ACKA_IN_GGA(s(T78), s(s(T79))) → PD_IN_GGAAA(T78, T79)
PD_IN_GGAAA(T78, T79) → U16_GGAAA(T78, T79, ackH_in_gga(s(T78), T79))
U16_GGAAA(T78, T79, ackH_out_gga(s(T78), T79, T80)) → PJ_IN_GGAA(T78, T80)
PJ_IN_GGAA(T78, T80) → U18_GGAA(T78, T80, ackH_in_gga(T78, T80))
U18_GGAA(T78, T80, ackH_out_gga(T78, T80, T83)) → ACKA_IN_GGA(T78, T83)

The TRS R consists of the following rules:

ackE_in_ga(T28) → U4_ga(T28, ackF_in_ga(T28))
ackF_in_ga(0) → ackF_out_ga(0, s(s(0)))
ackF_in_ga(s(T32)) → U5_ga(T32, pG_in_gaa(T32))
ackH_in_gga(s(T45), 0) → U6_gga(T45, ackF_in_ga(T45))
ackH_in_gga(s(T50), s(T51)) → U7_gga(T50, T51, pI_in_ggaa(T50, T51))
ackH_in_gga(0, T40) → ackH_out_gga(0, T40, s(T40))
U4_ga(T28, ackF_out_ga(T28, X60)) → ackE_out_ga(T28, X60)
U5_ga(T32, pG_out_gaa(T32, X82, X83)) → ackF_out_ga(s(T32), X83)
U6_gga(T45, ackF_out_ga(T45, X109)) → ackH_out_gga(s(T45), 0, X109)
U7_gga(T50, T51, pI_out_ggaa(T50, T51, X124, X125)) → ackH_out_gga(s(T50), s(T51), X125)
pG_in_gaa(T32) → U10_gaa(T32, ackE_in_ga(T32))
pI_in_ggaa(T50, T51) → U12_ggaa(T50, T51, ackH_in_gga(s(T50), T51))
U10_gaa(T32, ackE_out_ga(T32, T33)) → U11_gaa(T32, T33, ackH_in_gga(T32, T33))
U12_ggaa(T50, T51, ackH_out_gga(s(T50), T51, T52)) → U13_ggaa(T50, T51, T52, ackH_in_gga(T50, T52))
U11_gaa(T32, T33, ackH_out_gga(T32, T33, X83)) → pG_out_gaa(T32, T33, X83)
U13_ggaa(T50, T51, T52, ackH_out_gga(T50, T52, X125)) → pI_out_ggaa(T50, T51, T52, X125)

The set Q consists of the following terms:

ackE_in_ga(x0)
ackF_in_ga(x0)
ackH_in_gga(x0, x1)
U4_ga(x0, x1)
U5_ga(x0, x1)
U6_gga(x0, x1)
U7_gga(x0, x1, x2)
pG_in_gaa(x0)
pI_in_ggaa(x0, x1)
U10_gaa(x0, x1)
U12_ggaa(x0, x1, x2)
U11_gaa(x0, x1, x2)
U13_ggaa(x0, x1, x2, x3)

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

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

PB_IN_GAA(T20) → U8_GAA(T20, ackE_in_ga(T20))
The graph contains the following edges 1 >= 1
U8_GAA(T20, ackE_out_ga(T20, T23)) → ACKA_IN_GGA(T20, T23)
The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2
ACKA_IN_GGA(s(s(T20)), 0) → PB_IN_GAA(T20)
The graph contains the following edges 1 > 1
PC_IN_GAA(T70) → U14_GAA(T70, ackF_in_ga(T70))
The graph contains the following edges 1 >= 1
U14_GAA(T70, ackF_out_ga(T70, T71)) → ACKA_IN_GGA(T70, T71)
The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2
U18_GGAA(T78, T80, ackH_out_gga(T78, T80, T83)) → ACKA_IN_GGA(T78, T83)
The graph contains the following edges 1 >= 1, 3 > 1, 3 > 2
ACKA_IN_GGA(s(T70), s(0)) → PC_IN_GAA(T70)
The graph contains the following edges 1 > 1
ACKA_IN_GGA(s(T78), s(s(T79))) → PD_IN_GGAAA(T78, T79)
The graph contains the following edges 1 > 1, 2 > 2
PD_IN_GGAAA(T78, T79) → U16_GGAAA(T78, T79, ackH_in_gga(s(T78), T79))
The graph contains the following edges 1 >= 1, 2 >= 2
U16_GGAAA(T78, T79, ackH_out_gga(s(T78), T79, T80)) → PJ_IN_GGAA(T78, T80)
The graph contains the following edges 1 >= 1, 3 > 1, 3 > 2
PJ_IN_GGAA(T78, T80) → U18_GGAA(T78, T80, ackH_in_gga(T78, T80))
The graph contains the following edges 1 >= 1, 2 >= 2

(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) Rewriting (EQUIVALENT transformation)

(13) Obligation:

(14) QDPOrderProof (EQUIVALENT transformation)

(15) Obligation:

(16) DependencyGraphProof (EQUIVALENT transformation)

(17) Obligation:

(18) UsableRulesProof (EQUIVALENT transformation)

(19) Obligation:

(20) QReductionProof (EQUIVALENT transformation)

(21) Obligation:

(22) QDPSizeChangeProof (EQUIVALENT transformation)

(23) YES

(24) Obligation:

(25) UsableRulesProof (EQUIVALENT transformation)

(26) Obligation:

(27) PiDPToQDPProof (SOUND transformation)

(28) Obligation:

(29) QDPSizeChangeProof (EQUIVALENT transformation)

(30) YES