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

(0) Obligation:

Clauses:

nat(0).
nat(s(X)) :- nat(X).
plus(0, X, X) :- nat(X).
plus(s(X), Y, s(Z)) :- plus(X, Y, Z).
ways(0, X1, s(0)).
ways(X2, [], 0).
ways(Amount, .(s(C), Coins), N) :- ','(=(Amount, s(X3)), ','(plus(s(C), NewAmount, Amount), ','(ways(Amount, Coins, N1), ','(ways(NewAmount, .(s(C), Coins), N2), plus(N1, N2, N))))).
ways(Amount, .(s(C), Coins), N) :- ','(=(Amount, s(X4)), ','(plus(Amount, s(X5), s(C)), ways(Amount, Coins, N))).

Query: ways(g,g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: ways(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: ways(T1, T2, T3), SCOPE: 1, CLAUSE: 4 | ways(T1, T2, T3), SCOPE: 1, CLAUSE: 5 | ways(T1, T2, T3), SCOPE: 1, CLAUSE: 6 | ways(T1, T2, T3), SCOPE: 1, CLAUSE: 7\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: true | ways(0, T5, T3), SCOPE: 1, CLAUSE: 5 | ways(0, T5, T3), SCOPE: 1, CLAUSE: 6 | ways(0, T5, T3), SCOPE: 1, CLAUSE: 7\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ways(T1, T2, T3), SCOPE: 1, CLAUSE: 5 | ways(T1, T2, T3), SCOPE: 1, CLAUSE: 6 | ways(T1, T2, T3), SCOPE: 1, CLAUSE: 7\n\nT1 is ground\nT2 is ground\nX7 is free\nways(T1, T2, T3) !=? ways(0, X7, s(0))", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ways(0, T5, T3), SCOPE: 1, CLAUSE: 5 | ways(0, T5, T3), SCOPE: 1, CLAUSE: 6 | ways(0, T5, T3), SCOPE: 1, CLAUSE: 7\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: true | ways(0, [], T3), SCOPE: 1, CLAUSE: 6 | ways(0, [], T3), SCOPE: 1, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ways(0, T5, T3), SCOPE: 1, CLAUSE: 6 | ways(0, T5, T3), SCOPE: 1, CLAUSE: 7\n\nT5 is ground\nX9 is free\nways(0, T5, T3) !=? ways(X9, [], 0)", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ways(0, [], T3), SCOPE: 1, CLAUSE: 6 | ways(0, [], T3), SCOPE: 1, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ways(0, [], T3), SCOPE: 1, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(=(0, s(X26)), ','(plus(s(T9), X27, 0), ','(ways(0, T10, X28), ','(ways(X27, .(s(T9), T10), X29), plus(X28, X29, T12))))) | ways(0, .(s(T9), T10), T3), SCOPE: 1, CLAUSE: 7\n\nT9 is ground\nT10 is ground\nX26 is free\nX27 is free\nX28 is free\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ways(0, T5, T3), SCOPE: 1, CLAUSE: 7\n\nT5 is ground\nX9 is free\nX22 is free\nX23 is free\nX24 is free\nX25 is free\nways(0, T5, T3) !=? ways(X9, [], 0)\nways(0, T5, T3) !=? ways(X22, .(s(X23), X24), X25)", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: ways(0, .(s(T9), T10), T3), SCOPE: 1, CLAUSE: 7\n\nT9 is ground\nT10 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: ','(=(0, s(X38)), ','(plus(0, s(X39), s(T16)), ways(0, T17, T19)))\n\nT16 is ground\nT17 is ground\nX38 is free\nX39 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: true | ways(T24, [], T3), SCOPE: 1, CLAUSE: 6 | ways(T24, [], T3), SCOPE: 1, CLAUSE: 7\n\nT24 is ground\nX7 is free\nways(T24, [], T3) !=? ways(0, X7, s(0))", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ways(T1, T2, T3), SCOPE: 1, CLAUSE: 6 | ways(T1, T2, T3), SCOPE: 1, CLAUSE: 7\n\nT1 is ground\nT2 is ground\nX7 is free\nX45 is free\nways(T1, T2, T3) !=? ways(0, X7, s(0))\nways(T1, T2, T3) !=? ways(X45, [], 0)", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ways(T24, [], T3), SCOPE: 1, CLAUSE: 6 | ways(T24, [], T3), SCOPE: 1, CLAUSE: 7\n\nT24 is ground\nX7 is free\nways(T24, [], T3) !=? ways(0, X7, s(0))", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ways(T24, [], T3), SCOPE: 1, CLAUSE: 7\n\nT24 is ground\nX7 is free\nways(T24, [], T3) !=? ways(0, X7, s(0))", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: ','(=(T31, s(X62)), ','(plus(s(T32), X63, T31), ','(ways(T31, T33, X64), ','(ways(X63, .(s(T32), T33), X65), plus(X64, X65, T35))))) | ways(T31, .(s(T32), T33), T3), SCOPE: 1, CLAUSE: 7\n\nT31 is ground\nT32 is ground\nT33 is ground\nX7 is free\nX62 is free\nX63 is free\nX64 is free\nX65 is free\nways(T31, .(s(T32), T33), T3) !=? ways(0, X7, s(0))", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: ways(T1, T2, T3), SCOPE: 1, CLAUSE: 7\n\nT1 is ground\nT2 is ground\nX7 is free\nX45 is free\nX58 is free\nX59 is free\nX60 is free\nX61 is free\nways(T1, T2, T3) !=? ways(0, X7, s(0))\nways(T1, T2, T3) !=? ways(X45, [], 0)\nways(T1, T2, T3) !=? ways(X58, .(s(X59), X60), X61)", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: ','(plus(s(T32), X63, s(T37)), ','(ways(s(T37), T33, X64), ','(ways(X63, .(s(T32), T33), X65), plus(X64, X65, T35)))) | ways(s(T37), .(s(T32), T33), T3), SCOPE: 1, CLAUSE: 7\n\nT32 is ground\nT33 is ground\nT37 is ground\nX63 is free\nX64 is free\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: ways(T31, .(s(T32), T33), T3), SCOPE: 1, CLAUSE: 7\n\nT31 is ground\nT32 is ground\nT33 is ground\nX7 is free\nX62 is free\nways(T31, .(s(T32), T33), T3) !=? ways(0, X7, s(0))\nT31 !=? s(X62)", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: ','(plus(s(T32), X63, s(T37)), ','(ways(s(T37), T33, X64), ','(ways(X63, .(s(T32), T33), X65), plus(X64, X65, T35)))), SCOPE: 2, CLAUSE: 2 | ','(plus(s(T32), X63, s(T37)), ','(ways(s(T37), T33, X64), ','(ways(X63, .(s(T32), T33), X65), plus(X64, X65, T35)))), SCOPE: 2, CLAUSE: 3 | ?_2 | ways(s(T37), .(s(T32), T33), T3), SCOPE: 1, CLAUSE: 7\n\nT32 is ground\nT33 is ground\nT37 is ground\nX63 is free\nX64 is free\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: ','(plus(s(T32), X63, s(T37)), ','(ways(s(T37), T33, X64), ','(ways(X63, .(s(T32), T33), X65), plus(X64, X65, T35)))), SCOPE: 2, CLAUSE: 3 | ?_2 | ways(s(T37), .(s(T32), T33), T3), SCOPE: 1, CLAUSE: 7\n\nT32 is ground\nT33 is ground\nT37 is ground\nX63 is free\nX64 is free\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: ','(plus(s(T32), X63, s(T37)), ','(ways(s(T37), T33, X64), ','(ways(X63, .(s(T32), T33), X65), plus(X64, X65, T35)))), SCOPE: 2, CLAUSE: 3\n\nT32 is ground\nT33 is ground\nT37 is ground\nX63 is free\nX64 is free\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: ?_2 | ways(s(T37), .(s(T32), T33), T3), SCOPE: 1, CLAUSE: 7\n\nT32 is ground\nT33 is ground\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="B: ','(plus(T48, X90, T49), ','(ways(s(T49), T33, X64), ','(ways(X90, .(s(T48), T33), X65), plus(X64, X65, T35))))\n\nT33 is ground\nT48 is ground\nT49 is ground\nX64 is free\nX65 is free\nX90 is free", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="E: plus(T48, X90, T49)\n\nT48 is ground\nT49 is ground\nX90 is free", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="I: ','(ways(s(T49), T33, X64), ','(ways(T51, .(s(T48), T33), X65), plus(X64, X65, T35)))\n\nT33 is ground\nT48 is ground\nT49 is ground\nT51 is ground\nX64 is free\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: plus(T48, X90, T49), SCOPE: 3, CLAUSE: 2 | plus(T48, X90, T49), SCOPE: 3, CLAUSE: 3\n\nT48 is ground\nT49 is ground\nX90 is free", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: plus(T48, X90, T49), SCOPE: 3, CLAUSE: 2\n\nT48 is ground\nT49 is ground\nX90 is free", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: plus(T48, X90, T49), SCOPE: 3, CLAUSE: 3\n\nT48 is ground\nT49 is ground\nX90 is free", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="D: nat(T57)\n\nT57 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: nat(T57), SCOPE: 4, CLAUSE: 0 | nat(T57), SCOPE: 4, CLAUSE: 1\n\nT57 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: nat(T57), SCOPE: 4, CLAUSE: 0\n\nT57 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: nat(T57), SCOPE: 4, CLAUSE: 1\n\nT57 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: nat(T60)\n\nT60 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: plus(T65, X119, T66)\n\nT65 is ground\nT66 is ground\nX119 is free", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
152 [label="152: ways(s(T49), T33, X64)\n\nT33 is ground\nT49 is ground\nX64 is free", fontsize=16, style=filled, fillcolor=lightyellow];
153 [label="J: ','(ways(T51, .(s(T48), T33), X65), plus(T68, X65, T35))\n\nT33 is ground\nT48 is ground\nT51 is ground\nT68 is ground\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
156 [label="156: ways(T51, .(s(T48), T33), X65)\n\nT33 is ground\nT48 is ground\nT51 is ground\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
157 [label="F: plus(T68, T73, T35)\n\nT68 is ground\nT73 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
172 [label="172: plus(T68, T73, T35), SCOPE: 5, CLAUSE: 2 | plus(T68, T73, T35), SCOPE: 5, CLAUSE: 3\n\nT68 is ground\nT73 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
173 [label="173: plus(T68, T73, T35), SCOPE: 5, CLAUSE: 2\n\nT68 is ground\nT73 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
174 [label="174: plus(T68, T73, T35), SCOPE: 5, CLAUSE: 3\n\nT68 is ground\nT73 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
175 [label="175: nat(T83)\n\nT83 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
176 [label="176: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
179 [label="179: plus(T90, T91, T93)\n\nT90 is ground\nT91 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
180 [label="180: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
185 [label="185: ways(s(T37), .(s(T32), T33), T3), SCOPE: 1, CLAUSE: 7\n\nT32 is ground\nT33 is ground\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
190 [label="190: ','(=(s(T104), s(X160)), ','(plus(s(T104), s(X161), s(T105)), ways(s(T104), T106, T108)))\n\nT104 is ground\nT105 is ground\nT106 is ground\nX160 is free\nX161 is free", fontsize=16, style=filled, fillcolor=lightyellow];
192 [label="C: ','(plus(s(T110), s(X161), s(T105)), ways(s(T110), T106, T108))\n\nT105 is ground\nT106 is ground\nT110 is ground\nX161 is free", fontsize=16, style=filled, fillcolor=lightyellow];
193 [label="H: plus(s(T110), s(X161), s(T105))\n\nT105 is ground\nT110 is ground\nX161 is free", fontsize=16, style=filled, fillcolor=lightyellow];
194 [label="194: ways(s(T110), T106, T108)\n\nT106 is ground\nT110 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
195 [label="195: plus(s(T110), s(X161), s(T105)), SCOPE: 6, CLAUSE: 2 | plus(s(T110), s(X161), s(T105)), SCOPE: 6, CLAUSE: 3\n\nT105 is ground\nT110 is ground\nX161 is free", fontsize=16, style=filled, fillcolor=lightyellow];
196 [label="196: plus(s(T110), s(X161), s(T105)), SCOPE: 6, CLAUSE: 3\n\nT105 is ground\nT110 is ground\nX161 is free", fontsize=16, style=filled, fillcolor=lightyellow];
197 [label="G: plus(T117, s(X178), T118)\n\nT117 is ground\nT118 is ground\nX178 is free", fontsize=16, style=filled, fillcolor=lightyellow];
200 [label="200: plus(T117, s(X178), T118), SCOPE: 7, CLAUSE: 2 | plus(T117, s(X178), T118), SCOPE: 7, CLAUSE: 3\n\nT117 is ground\nT118 is ground\nX178 is free", fontsize=16, style=filled, fillcolor=lightyellow];
201 [label="201: plus(T117, s(X178), T118), SCOPE: 7, CLAUSE: 2\n\nT117 is ground\nT118 is ground\nX178 is free", fontsize=16, style=filled, fillcolor=lightyellow];
202 [label="202: plus(T117, s(X178), T118), SCOPE: 7, CLAUSE: 3\n\nT117 is ground\nT118 is ground\nX178 is free", fontsize=16, style=filled, fillcolor=lightyellow];
204 [label="204: nat(s(T124))\n\nT124 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
205 [label="205: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
206 [label="206: plus(T129, s(X202), T130)\n\nT129 is ground\nT130 is ground\nX202 is free", fontsize=16, style=filled, fillcolor=lightyellow];
207 [label="207: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
213 [label="213: ','(=(T136, s(X215)), ','(plus(T136, s(X216), s(T137)), ways(T136, T138, T140)))\n\nT136 is ground\nT137 is ground\nT138 is ground\nX7 is free\nX62 is free\nX215 is free\nX216 is free\nways(T136, .(s(T137), T138), T3) !=? ways(0, X7, s(0))\nT136 !=? s(X62)", fontsize=16, style=filled, fillcolor=lightyellow];
214 [label="214: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
215 [label="215: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
216 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 216 [arrowhead = none ];
216 -> 5;

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

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

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

220 [label="EVAL with clause\nways(X45, [], 0).\nand substitutionT1 -> T24,\nX45 -> T24,\nT2 -> [],\nT3 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 220 [arrowhead = none ];
220 -> 55;

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

222 [label="EVAL with clause\nways(X9, [], 0).\nand substitutionX9 -> 0,\nT5 -> [],\nT3 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 222 [arrowhead = none ];
222 -> 19;

223 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 223 [arrowhead = none ];
223 -> 23;

224 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 224 [arrowhead = none ];
224 -> 25;

225 [label="EVAL with clause\nways(X22, .(s(X23), X24), X25) :- ','(=(X22, s(X26)), ','(plus(s(X23), X27, X22), ','(ways(X22, X24, X28), ','(ways(X27, .(s(X23), X24), X29), plus(X28, X29, X25))))).\nand substitutionX22 -> 0,\nX23 -> T9,\nX24 -> T10,\nT5 -> .(s(T9), T10),\nT3 -> T12,\nX25 -> T12,\nT11 -> T12", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 225 [arrowhead = none ];
225 -> 36;

226 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
23 -> 226 [arrowhead = none ];
226 -> 39;

227 [label="BACKTRACK\nfor clause: ways(Amount, .(s(C), Coins), N) :- ','(=(Amount, s(X3)), ','(plus(s(C), NewAmount, Amount), ','(ways(Amount, Coins, N1), ','(ways(NewAmount, .(s(C), Coins), N2), plus(N1, N2, N)))))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 227 [arrowhead = none ];
227 -> 27;

228 [label="BACKTRACK\nfor clause: ways(Amount, .(s(C), Coins), N) :- ','(=(Amount, s(X4)), ','(plus(Amount, s(X5), s(C)), ways(Amount, Coins, N)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 228 [arrowhead = none ];
228 -> 32;

229 [label="UNIFY-FAIL\nbecause of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
36 -> 229 [arrowhead = none ];
229 -> 40;

230 [label="BACKTRACK\nfor clause: ways(Amount, .(s(C), Coins), N) :- ','(=(Amount, s(X4)), ','(plus(Amount, s(X5), s(C)), ways(Amount, Coins, N)))\nwith clash: (ways(0, T5, T3), ways(X22, .(s(X23), X24), X25))", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 230 [arrowhead = none ];
230 -> 52;

231 [label="ONLY EVAL with clause\nways(X34, .(s(X35), X36), X37) :- ','(=(X34, s(X38)), ','(plus(X34, s(X39), s(X35)), ways(X34, X36, X37))).\nand substitutionX34 -> 0,\nT9 -> T16,\nX35 -> T16,\nT10 -> T17,\nX36 -> T17,\nT3 -> T19,\nX37 -> T19,\nT18 -> T19", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 231 [arrowhead = none ];
231 -> 45;

232 [label="UNIFY-FAIL\nbecause of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
45 -> 232 [arrowhead = none ];
232 -> 46;

233 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
55 -> 233 [arrowhead = none ];
233 -> 58;

234 [label="EVAL with clause\nways(X58, .(s(X59), X60), X61) :- ','(=(X58, s(X62)), ','(plus(s(X59), X63, X58), ','(ways(X58, X60, X64), ','(ways(X63, .(s(X59), X60), X65), plus(X64, X65, X61))))).\nand substitutionT1 -> T31,\nX58 -> T31,\nX59 -> T32,\nX60 -> T33,\nT2 -> .(s(T32), T33),\nT3 -> T35,\nX61 -> T35,\nT34 -> T35", fontsize=14, style = filled, fillcolor = lightblue];
57 -> 234 [arrowhead = none ];
234 -> 63;

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

236 [label="BACKTRACK\nfor clause: ways(Amount, .(s(C), Coins), N) :- ','(=(Amount, s(X3)), ','(plus(s(C), NewAmount, Amount), ','(ways(Amount, Coins, N1), ','(ways(NewAmount, .(s(C), Coins), N2), plus(N1, N2, N)))))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
58 -> 236 [arrowhead = none ];
236 -> 59;

237 [label="BACKTRACK\nfor clause: ways(Amount, .(s(C), Coins), N) :- ','(=(Amount, s(X4)), ','(plus(Amount, s(X5), s(C)), ways(Amount, Coins, N)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 237 [arrowhead = none ];
237 -> 60;

238 [label="UNIFY CASE with substitutionX62 -> T37,\nT31 -> s(T37)", fontsize=14, style = filled, fillcolor = lightblue];
63 -> 238 [arrowhead = none ];
238 -> 71;

239 [label="UNIFY-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
63 -> 239 [arrowhead = none ];
239 -> 72;

240 [label="BACKTRACK\nfor clause: ways(Amount, .(s(C), Coins), N) :- ','(=(Amount, s(X4)), ','(plus(Amount, s(X5), s(C)), ways(Amount, Coins, N)))\nwith clash: (ways(T1, T2, T3), ways(X58, .(s(X59), X60), X61))", fontsize=14, style = filled, fillcolor = lightgreen];
69 -> 240 [arrowhead = none ];
240 -> 215;

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

242 [label="ONLY EVAL with clause\nways(X211, .(s(X212), X213), X214) :- ','(=(X211, s(X215)), ','(plus(X211, s(X216), s(X212)), ways(X211, X213, X214))).\nand substitutionT31 -> T136,\nX211 -> T136,\nT32 -> T137,\nX212 -> T137,\nT33 -> T138,\nX213 -> T138,\nT3 -> T140,\nX214 -> T140,\nT139 -> T140", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 242 [arrowhead = none ];
242 -> 213;

243 [label="BACKTRACK\nfor clause: plus(0, X, X) :- nat(X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
73 -> 243 [arrowhead = none ];
243 -> 74;

244 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
74 -> 244 [arrowhead = none ];
244 -> 77;

245 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
74 -> 245 [arrowhead = none ];
245 -> 78;

246 [label="ONLY EVAL with clause\nplus(s(X87), X88, s(X89)) :- plus(X87, X88, X89).\nand substitutionT32 -> T48,\nX87 -> T48,\nX63 -> X90,\nX88 -> X90,\nT37 -> T49,\nX89 -> T49", fontsize=14, style = filled, fillcolor = lightblue];
77 -> 246 [arrowhead = none ];
246 -> 82;

247 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
78 -> 247 [arrowhead = none ];
247 -> 185;

248 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
82 -> 248 [arrowhead = none ];
248 -> 90;

249 [label="SPLIT 2\nnew knowledge:\nT48 is ground\nT51 is ground\nT49 is ground\nreplacements:X90 -> T51", fontsize=14, style = filled, fillcolor = violet];
82 -> 249 [arrowhead = none ];
249 -> 91;

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

251 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
91 -> 251 [arrowhead = none ];
251 -> 152;

252 [label="SPLIT 2\nnew knowledge:\nT49 is ground\nT33 is ground\nT68 is ground\nreplacements:X64 -> T68", fontsize=14, style = filled, fillcolor = violet];
91 -> 252 [arrowhead = none ];
252 -> 153;

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

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

255 [label="EVAL with clause\nplus(0, X103, X103) :- nat(X103).\nand substitutionT48 -> 0,\nX90 -> T57,\nX103 -> T57,\nT49 -> T57,\nX104 -> T57", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 255 [arrowhead = none ];
255 -> 123;

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

257 [label="EVAL with clause\nplus(s(X116), X117, s(X118)) :- plus(X116, X117, X118).\nand substitutionX116 -> T65,\nT48 -> s(T65),\nX90 -> X119,\nX117 -> X119,\nX118 -> T66,\nT49 -> s(T66)", fontsize=14, style = filled, fillcolor = lightblue];
116 -> 257 [arrowhead = none ];
257 -> 136;

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

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

260 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
125 -> 260 [arrowhead = none ];
260 -> 126;

261 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
125 -> 261 [arrowhead = none ];
261 -> 127;

262 [label="EVAL with clause\nnat(0).\nand substitutionT57 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
126 -> 262 [arrowhead = none ];
262 -> 128;

263 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
126 -> 263 [arrowhead = none ];
263 -> 129;

264 [label="EVAL with clause\nnat(s(X107)) :- nat(X107).\nand substitutionX107 -> T60,\nT57 -> s(T60)", fontsize=14, style = filled, fillcolor = lightblue];
127 -> 264 [arrowhead = none ];
264 -> 131;

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

266 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
128 -> 266 [arrowhead = none ];
266 -> 130;

267 [label="INSTANCE with matching:\nT57 -> T60", fontsize=14, style = filled, fillcolor = lightgrey];
131 -> 267 [arrowhead = none , style=dashed];
267 -> 123[style=dashed];

268 [label="INSTANCE with matching:\nT48 -> T65\nX90 -> X119\nT49 -> T66", fontsize=14, style = filled, fillcolor = lightgrey];
136 -> 268 [arrowhead = none , style=dashed];
268 -> 90[style=dashed];

269 [label="INSTANCE with matching:\nT1 -> s(T49)\nT2 -> T33\nT3 -> X64", fontsize=14, style = filled, fillcolor = lightgrey];
152 -> 269 [arrowhead = none , style=dashed];
269 -> 3[style=dashed];

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

271 [label="SPLIT 2\nnew knowledge:\nT51 is ground\nT48 is ground\nT33 is ground\nT73 is ground\nreplacements:X65 -> T73", fontsize=14, style = filled, fillcolor = violet];
153 -> 271 [arrowhead = none ];
271 -> 157;

272 [label="INSTANCE with matching:\nT1 -> T51\nT2 -> .(s(T48), T33)\nT3 -> X65", fontsize=14, style = filled, fillcolor = lightgrey];
156 -> 272 [arrowhead = none , style=dashed];
272 -> 3[style=dashed];

273 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
157 -> 273 [arrowhead = none ];
273 -> 172;

274 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
172 -> 274 [arrowhead = none ];
274 -> 173;

275 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
172 -> 275 [arrowhead = none ];
275 -> 174;

276 [label="EVAL with clause\nplus(0, X135, X135) :- nat(X135).\nand substitutionT68 -> 0,\nT73 -> T83,\nX135 -> T83,\nT35 -> T83", fontsize=14, style = filled, fillcolor = lightblue];
173 -> 276 [arrowhead = none ];
276 -> 175;

277 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
173 -> 277 [arrowhead = none ];
277 -> 176;

278 [label="EVAL with clause\nplus(s(X142), X143, s(X144)) :- plus(X142, X143, X144).\nand substitutionX142 -> T90,\nT68 -> s(T90),\nT73 -> T91,\nX143 -> T91,\nX144 -> T93,\nT35 -> s(T93),\nT92 -> T93", fontsize=14, style = filled, fillcolor = lightblue];
174 -> 278 [arrowhead = none ];
278 -> 179;

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

280 [label="INSTANCE with matching:\nT57 -> T83", fontsize=14, style = filled, fillcolor = lightgrey];
175 -> 280 [arrowhead = none , style=dashed];
280 -> 123[style=dashed];

281 [label="INSTANCE with matching:\nT68 -> T90\nT73 -> T91\nT35 -> T93", fontsize=14, style = filled, fillcolor = lightgrey];
179 -> 281 [arrowhead = none , style=dashed];
281 -> 157[style=dashed];

282 [label="ONLY EVAL with clause\nways(X156, .(s(X157), X158), X159) :- ','(=(X156, s(X160)), ','(plus(X156, s(X161), s(X157)), ways(X156, X158, X159))).\nand substitutionT37 -> T104,\nX156 -> s(T104),\nT32 -> T105,\nX157 -> T105,\nT33 -> T106,\nX158 -> T106,\nT3 -> T108,\nX159 -> T108,\nT107 -> T108", fontsize=14, style = filled, fillcolor = lightblue];
185 -> 282 [arrowhead = none ];
282 -> 190;

283 [label="UNIFY SUCCESS with substitutionT104 -> T110,\nX160 -> T110", fontsize=14, style = filled, fillcolor = lightblue];
190 -> 283 [arrowhead = none ];
283 -> 192;

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

285 [label="SPLIT 2\nnew knowledge:\nT110 is ground\nT111 is ground\nT105 is ground\nreplacements:X161 -> T111", fontsize=14, style = filled, fillcolor = violet];
192 -> 285 [arrowhead = none ];
285 -> 194;

286 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
193 -> 286 [arrowhead = none ];
286 -> 195;

287 [label="INSTANCE with matching:\nT1 -> s(T110)\nT2 -> T106\nT3 -> T108", fontsize=14, style = filled, fillcolor = lightgrey];
194 -> 287 [arrowhead = none , style=dashed];
287 -> 3[style=dashed];

288 [label="BACKTRACK\nfor clause: plus(0, X, X) :- nat(X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
195 -> 288 [arrowhead = none ];
288 -> 196;

289 [label="ONLY EVAL with clause\nplus(s(X175), X176, s(X177)) :- plus(X175, X176, X177).\nand substitutionT110 -> T117,\nX175 -> T117,\nX161 -> X178,\nX176 -> s(X178),\nT105 -> T118,\nX177 -> T118", fontsize=14, style = filled, fillcolor = lightblue];
196 -> 289 [arrowhead = none ];
289 -> 197;

290 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
197 -> 290 [arrowhead = none ];
290 -> 200;

291 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
200 -> 291 [arrowhead = none ];
291 -> 201;

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

293 [label="EVAL with clause\nplus(0, X189, X189) :- nat(X189).\nand substitutionT117 -> 0,\nX178 -> T124,\nX189 -> s(T124),\nX190 -> T124,\nT118 -> s(T124)", fontsize=14, style = filled, fillcolor = lightblue];
201 -> 293 [arrowhead = none ];
293 -> 204;

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

295 [label="EVAL with clause\nplus(s(X199), X200, s(X201)) :- plus(X199, X200, X201).\nand substitutionX199 -> T129,\nT117 -> s(T129),\nX178 -> X202,\nX200 -> s(X202),\nX201 -> T130,\nT118 -> s(T130)", fontsize=14, style = filled, fillcolor = lightblue];
202 -> 295 [arrowhead = none ];
295 -> 206;

296 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
202 -> 296 [arrowhead = none ];
296 -> 207;

297 [label="INSTANCE with matching:\nT57 -> s(T124)", fontsize=14, style = filled, fillcolor = lightgrey];
204 -> 297 [arrowhead = none , style=dashed];
297 -> 123[style=dashed];

298 [label="INSTANCE with matching:\nT117 -> T129\nX178 -> X202\nT118 -> T130", fontsize=14, style = filled, fillcolor = lightgrey];
206 -> 298 [arrowhead = none , style=dashed];
298 -> 197[style=dashed];

299 [label="UNIFY-FAIL\nwith clash: (T136, s(X62))", fontsize=14, style = filled, fillcolor = lightgreen];
213 -> 299 [arrowhead = none ];
299 -> 214;

}

(2) Obligation:

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

waysA_in_gga(0, T5, s(0)) → waysA_out_gga(0, T5, s(0))
waysA_in_gga(0, [], 0) → waysA_out_gga(0, [], 0)
waysA_in_gga(T24, [], 0) → waysA_out_gga(T24, [], 0)
waysA_in_gga(s(T49), .(s(T48), T33), T35) → U1_gga(T49, T48, T33, T35, pB_in_gaggaaa(T48, X90, T49, T33, X64, X65, T35))
pB_in_gaggaaa(T48, T51, T49, T33, X64, X65, T35) → U11_gaggaaa(T48, T51, T49, T33, X64, X65, T35, plusE_in_gag(T48, T51, T49))
plusE_in_gag(0, T57, T57) → U4_gag(T57, natD_in_g(T57))
natD_in_g(0) → natD_out_g(0)
natD_in_g(s(T60)) → U3_g(T60, natD_in_g(T60))
U3_g(T60, natD_out_g(T60)) → natD_out_g(s(T60))
U4_gag(T57, natD_out_g(T57)) → plusE_out_gag(0, T57, T57)
plusE_in_gag(s(T65), X119, s(T66)) → U5_gag(T65, X119, T66, plusE_in_gag(T65, X119, T66))
U5_gag(T65, X119, T66, plusE_out_gag(T65, X119, T66)) → plusE_out_gag(s(T65), X119, s(T66))
U11_gaggaaa(T48, T51, T49, T33, X64, X65, T35, plusE_out_gag(T48, T51, T49)) → U12_gaggaaa(T48, T51, T49, T33, X64, X65, T35, pI_in_ggaggaa(T49, T33, X64, T51, T48, X65, T35))
pI_in_ggaggaa(T49, T33, T68, T51, T48, X65, T35) → U13_ggaggaa(T49, T33, T68, T51, T48, X65, T35, waysA_in_gga(s(T49), T33, T68))
waysA_in_gga(s(T110), .(s(T105), T106), T108) → U2_gga(T110, T105, T106, T108, pC_in_gagga(T110, X161, T105, T106, T108))
pC_in_gagga(T110, T111, T105, T106, T108) → U17_gagga(T110, T111, T105, T106, T108, plusH_in_gag(T110, T111, T105))
plusH_in_gag(T117, X178, T118) → U10_gag(T117, X178, T118, plusG_in_gag(T117, X178, T118))
plusG_in_gag(0, T124, s(T124)) → U8_gag(T124, natD_in_g(s(T124)))
U8_gag(T124, natD_out_g(s(T124))) → plusG_out_gag(0, T124, s(T124))
plusG_in_gag(s(T129), X202, s(T130)) → U9_gag(T129, X202, T130, plusG_in_gag(T129, X202, T130))
U9_gag(T129, X202, T130, plusG_out_gag(T129, X202, T130)) → plusG_out_gag(s(T129), X202, s(T130))
U10_gag(T117, X178, T118, plusG_out_gag(T117, X178, T118)) → plusH_out_gag(T117, X178, T118)
U17_gagga(T110, T111, T105, T106, T108, plusH_out_gag(T110, T111, T105)) → U18_gagga(T110, T111, T105, T106, T108, waysA_in_gga(s(T110), T106, T108))
U18_gagga(T110, T111, T105, T106, T108, waysA_out_gga(s(T110), T106, T108)) → pC_out_gagga(T110, T111, T105, T106, T108)
U2_gga(T110, T105, T106, T108, pC_out_gagga(T110, X161, T105, T106, T108)) → waysA_out_gga(s(T110), .(s(T105), T106), T108)
U13_ggaggaa(T49, T33, T68, T51, T48, X65, T35, waysA_out_gga(s(T49), T33, T68)) → U14_ggaggaa(T49, T33, T68, T51, T48, X65, T35, pJ_in_gggaga(T51, T48, T33, X65, T68, T35))
pJ_in_gggaga(T51, T48, T33, T73, T68, T35) → U15_gggaga(T51, T48, T33, T73, T68, T35, waysA_in_gga(T51, .(s(T48), T33), T73))
U15_gggaga(T51, T48, T33, T73, T68, T35, waysA_out_gga(T51, .(s(T48), T33), T73)) → U16_gggaga(T51, T48, T33, T73, T68, T35, plusF_in_gga(T68, T73, T35))
plusF_in_gga(0, T83, T83) → U6_gga(T83, natD_in_g(T83))
U6_gga(T83, natD_out_g(T83)) → plusF_out_gga(0, T83, T83)
plusF_in_gga(s(T90), T91, s(T93)) → U7_gga(T90, T91, T93, plusF_in_gga(T90, T91, T93))
U7_gga(T90, T91, T93, plusF_out_gga(T90, T91, T93)) → plusF_out_gga(s(T90), T91, s(T93))
U16_gggaga(T51, T48, T33, T73, T68, T35, plusF_out_gga(T68, T73, T35)) → pJ_out_gggaga(T51, T48, T33, T73, T68, T35)
U14_ggaggaa(T49, T33, T68, T51, T48, X65, T35, pJ_out_gggaga(T51, T48, T33, X65, T68, T35)) → pI_out_ggaggaa(T49, T33, T68, T51, T48, X65, T35)
U12_gaggaaa(T48, T51, T49, T33, X64, X65, T35, pI_out_ggaggaa(T49, T33, X64, T51, T48, X65, T35)) → pB_out_gaggaaa(T48, T51, T49, T33, X64, X65, T35)
U1_gga(T49, T48, T33, T35, pB_out_gaggaaa(T48, X90, T49, T33, X64, X65, T35)) → waysA_out_gga(s(T49), .(s(T48), T33), T35)

The argument filtering Pi contains the following mapping:
waysA_in_gga(x1, x2, x3)  =  waysA_in_gga(x1, x2)
0  =  0
waysA_out_gga(x1, x2, x3)  =  waysA_out_gga(x1, x2, x3)
[]  =  []
s(x1)  =  s(x1)
.(x1, x2)  =  .(x1, x2)
U1_gga(x1, x2, x3, x4, x5)  =  U1_gga(x1, x2, x3, x5)
pB_in_gaggaaa(x1, x2, x3, x4, x5, x6, x7)  =  pB_in_gaggaaa(x1, x3, x4)
U11_gaggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U11_gaggaaa(x1, x3, x4, x8)
plusE_in_gag(x1, x2, x3)  =  plusE_in_gag(x1, x3)
U4_gag(x1, x2)  =  U4_gag(x1, x2)
natD_in_g(x1)  =  natD_in_g(x1)
natD_out_g(x1)  =  natD_out_g(x1)
U3_g(x1, x2)  =  U3_g(x1, x2)
plusE_out_gag(x1, x2, x3)  =  plusE_out_gag(x1, x2, x3)
U5_gag(x1, x2, x3, x4)  =  U5_gag(x1, x3, x4)
U12_gaggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_gaggaaa(x1, x2, x3, x4, x8)
pI_in_ggaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pI_in_ggaggaa(x1, x2, x4, x5)
U13_ggaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_ggaggaa(x1, x2, x4, x5, x8)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
pC_in_gagga(x1, x2, x3, x4, x5)  =  pC_in_gagga(x1, x3, x4)
U17_gagga(x1, x2, x3, x4, x5, x6)  =  U17_gagga(x1, x3, x4, x6)
plusH_in_gag(x1, x2, x3)  =  plusH_in_gag(x1, x3)
U10_gag(x1, x2, x3, x4)  =  U10_gag(x1, x3, x4)
plusG_in_gag(x1, x2, x3)  =  plusG_in_gag(x1, x3)
U8_gag(x1, x2)  =  U8_gag(x1, x2)
plusG_out_gag(x1, x2, x3)  =  plusG_out_gag(x1, x2, x3)
U9_gag(x1, x2, x3, x4)  =  U9_gag(x1, x3, x4)
plusH_out_gag(x1, x2, x3)  =  plusH_out_gag(x1, x2, x3)
U18_gagga(x1, x2, x3, x4, x5, x6)  =  U18_gagga(x1, x2, x3, x4, x6)
pC_out_gagga(x1, x2, x3, x4, x5)  =  pC_out_gagga(x1, x2, x3, x4, x5)
U14_ggaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U14_ggaggaa(x1, x2, x3, x4, x5, x8)
pJ_in_gggaga(x1, x2, x3, x4, x5, x6)  =  pJ_in_gggaga(x1, x2, x3, x5)
U15_gggaga(x1, x2, x3, x4, x5, x6, x7)  =  U15_gggaga(x1, x2, x3, x5, x7)
U16_gggaga(x1, x2, x3, x4, x5, x6, x7)  =  U16_gggaga(x1, x2, x3, x4, x5, x7)
plusF_in_gga(x1, x2, x3)  =  plusF_in_gga(x1, x2)
U6_gga(x1, x2)  =  U6_gga(x1, x2)
plusF_out_gga(x1, x2, x3)  =  plusF_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pJ_out_gggaga(x1, x2, x3, x4, x5, x6)  =  pJ_out_gggaga(x1, x2, x3, x4, x5, x6)
pI_out_ggaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pI_out_ggaggaa(x1, x2, x3, x4, x5, x6, x7)
pB_out_gaggaaa(x1, x2, x3, x4, x5, x6, x7)  =  pB_out_gaggaaa(x1, x2, x3, x4, x5, x6, x7)

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

WAYSA_IN_GGA(s(T49), .(s(T48), T33), T35) → U1_GGA(T49, T48, T33, T35, pB_in_gaggaaa(T48, X90, T49, T33, X64, X65, T35))
WAYSA_IN_GGA(s(T49), .(s(T48), T33), T35) → PB_IN_GAGGAAA(T48, X90, T49, T33, X64, X65, T35)
PB_IN_GAGGAAA(T48, T51, T49, T33, X64, X65, T35) → U11_GAGGAAA(T48, T51, T49, T33, X64, X65, T35, plusE_in_gag(T48, T51, T49))
PB_IN_GAGGAAA(T48, T51, T49, T33, X64, X65, T35) → PLUSE_IN_GAG(T48, T51, T49)
PLUSE_IN_GAG(0, T57, T57) → U4_GAG(T57, natD_in_g(T57))
PLUSE_IN_GAG(0, T57, T57) → NATD_IN_G(T57)
NATD_IN_G(s(T60)) → U3_G(T60, natD_in_g(T60))
NATD_IN_G(s(T60)) → NATD_IN_G(T60)
PLUSE_IN_GAG(s(T65), X119, s(T66)) → U5_GAG(T65, X119, T66, plusE_in_gag(T65, X119, T66))
PLUSE_IN_GAG(s(T65), X119, s(T66)) → PLUSE_IN_GAG(T65, X119, T66)
U11_GAGGAAA(T48, T51, T49, T33, X64, X65, T35, plusE_out_gag(T48, T51, T49)) → U12_GAGGAAA(T48, T51, T49, T33, X64, X65, T35, pI_in_ggaggaa(T49, T33, X64, T51, T48, X65, T35))
U11_GAGGAAA(T48, T51, T49, T33, X64, X65, T35, plusE_out_gag(T48, T51, T49)) → PI_IN_GGAGGAA(T49, T33, X64, T51, T48, X65, T35)
PI_IN_GGAGGAA(T49, T33, T68, T51, T48, X65, T35) → U13_GGAGGAA(T49, T33, T68, T51, T48, X65, T35, waysA_in_gga(s(T49), T33, T68))
PI_IN_GGAGGAA(T49, T33, T68, T51, T48, X65, T35) → WAYSA_IN_GGA(s(T49), T33, T68)
WAYSA_IN_GGA(s(T110), .(s(T105), T106), T108) → U2_GGA(T110, T105, T106, T108, pC_in_gagga(T110, X161, T105, T106, T108))
WAYSA_IN_GGA(s(T110), .(s(T105), T106), T108) → PC_IN_GAGGA(T110, X161, T105, T106, T108)
PC_IN_GAGGA(T110, T111, T105, T106, T108) → U17_GAGGA(T110, T111, T105, T106, T108, plusH_in_gag(T110, T111, T105))
PC_IN_GAGGA(T110, T111, T105, T106, T108) → PLUSH_IN_GAG(T110, T111, T105)
PLUSH_IN_GAG(T117, X178, T118) → U10_GAG(T117, X178, T118, plusG_in_gag(T117, X178, T118))
PLUSH_IN_GAG(T117, X178, T118) → PLUSG_IN_GAG(T117, X178, T118)
PLUSG_IN_GAG(0, T124, s(T124)) → U8_GAG(T124, natD_in_g(s(T124)))
PLUSG_IN_GAG(0, T124, s(T124)) → NATD_IN_G(s(T124))
PLUSG_IN_GAG(s(T129), X202, s(T130)) → U9_GAG(T129, X202, T130, plusG_in_gag(T129, X202, T130))
PLUSG_IN_GAG(s(T129), X202, s(T130)) → PLUSG_IN_GAG(T129, X202, T130)
U17_GAGGA(T110, T111, T105, T106, T108, plusH_out_gag(T110, T111, T105)) → U18_GAGGA(T110, T111, T105, T106, T108, waysA_in_gga(s(T110), T106, T108))
U17_GAGGA(T110, T111, T105, T106, T108, plusH_out_gag(T110, T111, T105)) → WAYSA_IN_GGA(s(T110), T106, T108)
U13_GGAGGAA(T49, T33, T68, T51, T48, X65, T35, waysA_out_gga(s(T49), T33, T68)) → U14_GGAGGAA(T49, T33, T68, T51, T48, X65, T35, pJ_in_gggaga(T51, T48, T33, X65, T68, T35))
U13_GGAGGAA(T49, T33, T68, T51, T48, X65, T35, waysA_out_gga(s(T49), T33, T68)) → PJ_IN_GGGAGA(T51, T48, T33, X65, T68, T35)
PJ_IN_GGGAGA(T51, T48, T33, T73, T68, T35) → U15_GGGAGA(T51, T48, T33, T73, T68, T35, waysA_in_gga(T51, .(s(T48), T33), T73))
PJ_IN_GGGAGA(T51, T48, T33, T73, T68, T35) → WAYSA_IN_GGA(T51, .(s(T48), T33), T73)
U15_GGGAGA(T51, T48, T33, T73, T68, T35, waysA_out_gga(T51, .(s(T48), T33), T73)) → U16_GGGAGA(T51, T48, T33, T73, T68, T35, plusF_in_gga(T68, T73, T35))
U15_GGGAGA(T51, T48, T33, T73, T68, T35, waysA_out_gga(T51, .(s(T48), T33), T73)) → PLUSF_IN_GGA(T68, T73, T35)
PLUSF_IN_GGA(0, T83, T83) → U6_GGA(T83, natD_in_g(T83))
PLUSF_IN_GGA(0, T83, T83) → NATD_IN_G(T83)
PLUSF_IN_GGA(s(T90), T91, s(T93)) → U7_GGA(T90, T91, T93, plusF_in_gga(T90, T91, T93))
PLUSF_IN_GGA(s(T90), T91, s(T93)) → PLUSF_IN_GGA(T90, T91, T93)

The TRS R consists of the following rules:

waysA_in_gga(0, T5, s(0)) → waysA_out_gga(0, T5, s(0))
waysA_in_gga(0, [], 0) → waysA_out_gga(0, [], 0)
waysA_in_gga(T24, [], 0) → waysA_out_gga(T24, [], 0)
waysA_in_gga(s(T49), .(s(T48), T33), T35) → U1_gga(T49, T48, T33, T35, pB_in_gaggaaa(T48, X90, T49, T33, X64, X65, T35))
pB_in_gaggaaa(T48, T51, T49, T33, X64, X65, T35) → U11_gaggaaa(T48, T51, T49, T33, X64, X65, T35, plusE_in_gag(T48, T51, T49))
plusE_in_gag(0, T57, T57) → U4_gag(T57, natD_in_g(T57))
natD_in_g(0) → natD_out_g(0)
natD_in_g(s(T60)) → U3_g(T60, natD_in_g(T60))
U3_g(T60, natD_out_g(T60)) → natD_out_g(s(T60))
U4_gag(T57, natD_out_g(T57)) → plusE_out_gag(0, T57, T57)
plusE_in_gag(s(T65), X119, s(T66)) → U5_gag(T65, X119, T66, plusE_in_gag(T65, X119, T66))
U5_gag(T65, X119, T66, plusE_out_gag(T65, X119, T66)) → plusE_out_gag(s(T65), X119, s(T66))
U11_gaggaaa(T48, T51, T49, T33, X64, X65, T35, plusE_out_gag(T48, T51, T49)) → U12_gaggaaa(T48, T51, T49, T33, X64, X65, T35, pI_in_ggaggaa(T49, T33, X64, T51, T48, X65, T35))
pI_in_ggaggaa(T49, T33, T68, T51, T48, X65, T35) → U13_ggaggaa(T49, T33, T68, T51, T48, X65, T35, waysA_in_gga(s(T49), T33, T68))
waysA_in_gga(s(T110), .(s(T105), T106), T108) → U2_gga(T110, T105, T106, T108, pC_in_gagga(T110, X161, T105, T106, T108))
pC_in_gagga(T110, T111, T105, T106, T108) → U17_gagga(T110, T111, T105, T106, T108, plusH_in_gag(T110, T111, T105))
plusH_in_gag(T117, X178, T118) → U10_gag(T117, X178, T118, plusG_in_gag(T117, X178, T118))
plusG_in_gag(0, T124, s(T124)) → U8_gag(T124, natD_in_g(s(T124)))
U8_gag(T124, natD_out_g(s(T124))) → plusG_out_gag(0, T124, s(T124))
plusG_in_gag(s(T129), X202, s(T130)) → U9_gag(T129, X202, T130, plusG_in_gag(T129, X202, T130))
U9_gag(T129, X202, T130, plusG_out_gag(T129, X202, T130)) → plusG_out_gag(s(T129), X202, s(T130))
U10_gag(T117, X178, T118, plusG_out_gag(T117, X178, T118)) → plusH_out_gag(T117, X178, T118)
U17_gagga(T110, T111, T105, T106, T108, plusH_out_gag(T110, T111, T105)) → U18_gagga(T110, T111, T105, T106, T108, waysA_in_gga(s(T110), T106, T108))
U18_gagga(T110, T111, T105, T106, T108, waysA_out_gga(s(T110), T106, T108)) → pC_out_gagga(T110, T111, T105, T106, T108)
U2_gga(T110, T105, T106, T108, pC_out_gagga(T110, X161, T105, T106, T108)) → waysA_out_gga(s(T110), .(s(T105), T106), T108)
U13_ggaggaa(T49, T33, T68, T51, T48, X65, T35, waysA_out_gga(s(T49), T33, T68)) → U14_ggaggaa(T49, T33, T68, T51, T48, X65, T35, pJ_in_gggaga(T51, T48, T33, X65, T68, T35))
pJ_in_gggaga(T51, T48, T33, T73, T68, T35) → U15_gggaga(T51, T48, T33, T73, T68, T35, waysA_in_gga(T51, .(s(T48), T33), T73))
U15_gggaga(T51, T48, T33, T73, T68, T35, waysA_out_gga(T51, .(s(T48), T33), T73)) → U16_gggaga(T51, T48, T33, T73, T68, T35, plusF_in_gga(T68, T73, T35))
plusF_in_gga(0, T83, T83) → U6_gga(T83, natD_in_g(T83))
U6_gga(T83, natD_out_g(T83)) → plusF_out_gga(0, T83, T83)
plusF_in_gga(s(T90), T91, s(T93)) → U7_gga(T90, T91, T93, plusF_in_gga(T90, T91, T93))
U7_gga(T90, T91, T93, plusF_out_gga(T90, T91, T93)) → plusF_out_gga(s(T90), T91, s(T93))
U16_gggaga(T51, T48, T33, T73, T68, T35, plusF_out_gga(T68, T73, T35)) → pJ_out_gggaga(T51, T48, T33, T73, T68, T35)
U14_ggaggaa(T49, T33, T68, T51, T48, X65, T35, pJ_out_gggaga(T51, T48, T33, X65, T68, T35)) → pI_out_ggaggaa(T49, T33, T68, T51, T48, X65, T35)
U12_gaggaaa(T48, T51, T49, T33, X64, X65, T35, pI_out_ggaggaa(T49, T33, X64, T51, T48, X65, T35)) → pB_out_gaggaaa(T48, T51, T49, T33, X64, X65, T35)
U1_gga(T49, T48, T33, T35, pB_out_gaggaaa(T48, X90, T49, T33, X64, X65, T35)) → waysA_out_gga(s(T49), .(s(T48), T33), T35)

The argument filtering Pi contains the following mapping:
waysA_in_gga(x1, x2, x3)  =  waysA_in_gga(x1, x2)
0  =  0
waysA_out_gga(x1, x2, x3)  =  waysA_out_gga(x1, x2, x3)
[]  =  []
s(x1)  =  s(x1)
.(x1, x2)  =  .(x1, x2)
U1_gga(x1, x2, x3, x4, x5)  =  U1_gga(x1, x2, x3, x5)
pB_in_gaggaaa(x1, x2, x3, x4, x5, x6, x7)  =  pB_in_gaggaaa(x1, x3, x4)
U11_gaggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U11_gaggaaa(x1, x3, x4, x8)
plusE_in_gag(x1, x2, x3)  =  plusE_in_gag(x1, x3)
U4_gag(x1, x2)  =  U4_gag(x1, x2)
natD_in_g(x1)  =  natD_in_g(x1)
natD_out_g(x1)  =  natD_out_g(x1)
U3_g(x1, x2)  =  U3_g(x1, x2)
plusE_out_gag(x1, x2, x3)  =  plusE_out_gag(x1, x2, x3)
U5_gag(x1, x2, x3, x4)  =  U5_gag(x1, x3, x4)
U12_gaggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_gaggaaa(x1, x2, x3, x4, x8)
pI_in_ggaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pI_in_ggaggaa(x1, x2, x4, x5)
U13_ggaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_ggaggaa(x1, x2, x4, x5, x8)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
pC_in_gagga(x1, x2, x3, x4, x5)  =  pC_in_gagga(x1, x3, x4)
U17_gagga(x1, x2, x3, x4, x5, x6)  =  U17_gagga(x1, x3, x4, x6)
plusH_in_gag(x1, x2, x3)  =  plusH_in_gag(x1, x3)
U10_gag(x1, x2, x3, x4)  =  U10_gag(x1, x3, x4)
plusG_in_gag(x1, x2, x3)  =  plusG_in_gag(x1, x3)
U8_gag(x1, x2)  =  U8_gag(x1, x2)
plusG_out_gag(x1, x2, x3)  =  plusG_out_gag(x1, x2, x3)
U9_gag(x1, x2, x3, x4)  =  U9_gag(x1, x3, x4)
plusH_out_gag(x1, x2, x3)  =  plusH_out_gag(x1, x2, x3)
U18_gagga(x1, x2, x3, x4, x5, x6)  =  U18_gagga(x1, x2, x3, x4, x6)
pC_out_gagga(x1, x2, x3, x4, x5)  =  pC_out_gagga(x1, x2, x3, x4, x5)
U14_ggaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U14_ggaggaa(x1, x2, x3, x4, x5, x8)
pJ_in_gggaga(x1, x2, x3, x4, x5, x6)  =  pJ_in_gggaga(x1, x2, x3, x5)
U15_gggaga(x1, x2, x3, x4, x5, x6, x7)  =  U15_gggaga(x1, x2, x3, x5, x7)
U16_gggaga(x1, x2, x3, x4, x5, x6, x7)  =  U16_gggaga(x1, x2, x3, x4, x5, x7)
plusF_in_gga(x1, x2, x3)  =  plusF_in_gga(x1, x2)
U6_gga(x1, x2)  =  U6_gga(x1, x2)
plusF_out_gga(x1, x2, x3)  =  plusF_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pJ_out_gggaga(x1, x2, x3, x4, x5, x6)  =  pJ_out_gggaga(x1, x2, x3, x4, x5, x6)
pI_out_ggaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pI_out_ggaggaa(x1, x2, x3, x4, x5, x6, x7)
pB_out_gaggaaa(x1, x2, x3, x4, x5, x6, x7)  =  pB_out_gaggaaa(x1, x2, x3, x4, x5, x6, x7)
WAYSA_IN_GGA(x1, x2, x3)  =  WAYSA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4, x5)  =  U1_GGA(x1, x2, x3, x5)
PB_IN_GAGGAAA(x1, x2, x3, x4, x5, x6, x7)  =  PB_IN_GAGGAAA(x1, x3, x4)
U11_GAGGAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U11_GAGGAAA(x1, x3, x4, x8)
PLUSE_IN_GAG(x1, x2, x3)  =  PLUSE_IN_GAG(x1, x3)
U4_GAG(x1, x2)  =  U4_GAG(x1, x2)
NATD_IN_G(x1)  =  NATD_IN_G(x1)
U3_G(x1, x2)  =  U3_G(x1, x2)
U5_GAG(x1, x2, x3, x4)  =  U5_GAG(x1, x3, x4)
U12_GAGGAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_GAGGAAA(x1, x2, x3, x4, x8)
PI_IN_GGAGGAA(x1, x2, x3, x4, x5, x6, x7)  =  PI_IN_GGAGGAA(x1, x2, x4, x5)
U13_GGAGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_GGAGGAA(x1, x2, x4, x5, x8)
U2_GGA(x1, x2, x3, x4, x5)  =  U2_GGA(x1, x2, x3, x5)
PC_IN_GAGGA(x1, x2, x3, x4, x5)  =  PC_IN_GAGGA(x1, x3, x4)
U17_GAGGA(x1, x2, x3, x4, x5, x6)  =  U17_GAGGA(x1, x3, x4, x6)
PLUSH_IN_GAG(x1, x2, x3)  =  PLUSH_IN_GAG(x1, x3)
U10_GAG(x1, x2, x3, x4)  =  U10_GAG(x1, x3, x4)
PLUSG_IN_GAG(x1, x2, x3)  =  PLUSG_IN_GAG(x1, x3)
U8_GAG(x1, x2)  =  U8_GAG(x1, x2)
U9_GAG(x1, x2, x3, x4)  =  U9_GAG(x1, x3, x4)
U18_GAGGA(x1, x2, x3, x4, x5, x6)  =  U18_GAGGA(x1, x2, x3, x4, x6)
U14_GGAGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U14_GGAGGAA(x1, x2, x3, x4, x5, x8)
PJ_IN_GGGAGA(x1, x2, x3, x4, x5, x6)  =  PJ_IN_GGGAGA(x1, x2, x3, x5)
U15_GGGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U15_GGGAGA(x1, x2, x3, x5, x7)
U16_GGGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U16_GGGAGA(x1, x2, x3, x4, x5, x7)
PLUSF_IN_GGA(x1, x2, x3)  =  PLUSF_IN_GGA(x1, x2)
U6_GGA(x1, x2)  =  U6_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)

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

(4) Obligation:

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

WAYSA_IN_GGA(s(T49), .(s(T48), T33), T35) → U1_GGA(T49, T48, T33, T35, pB_in_gaggaaa(T48, X90, T49, T33, X64, X65, T35))
WAYSA_IN_GGA(s(T49), .(s(T48), T33), T35) → PB_IN_GAGGAAA(T48, X90, T49, T33, X64, X65, T35)
PB_IN_GAGGAAA(T48, T51, T49, T33, X64, X65, T35) → U11_GAGGAAA(T48, T51, T49, T33, X64, X65, T35, plusE_in_gag(T48, T51, T49))
PB_IN_GAGGAAA(T48, T51, T49, T33, X64, X65, T35) → PLUSE_IN_GAG(T48, T51, T49)
PLUSE_IN_GAG(0, T57, T57) → U4_GAG(T57, natD_in_g(T57))
PLUSE_IN_GAG(0, T57, T57) → NATD_IN_G(T57)
NATD_IN_G(s(T60)) → U3_G(T60, natD_in_g(T60))
NATD_IN_G(s(T60)) → NATD_IN_G(T60)
PLUSE_IN_GAG(s(T65), X119, s(T66)) → U5_GAG(T65, X119, T66, plusE_in_gag(T65, X119, T66))
PLUSE_IN_GAG(s(T65), X119, s(T66)) → PLUSE_IN_GAG(T65, X119, T66)
U11_GAGGAAA(T48, T51, T49, T33, X64, X65, T35, plusE_out_gag(T48, T51, T49)) → U12_GAGGAAA(T48, T51, T49, T33, X64, X65, T35, pI_in_ggaggaa(T49, T33, X64, T51, T48, X65, T35))
U11_GAGGAAA(T48, T51, T49, T33, X64, X65, T35, plusE_out_gag(T48, T51, T49)) → PI_IN_GGAGGAA(T49, T33, X64, T51, T48, X65, T35)
PI_IN_GGAGGAA(T49, T33, T68, T51, T48, X65, T35) → U13_GGAGGAA(T49, T33, T68, T51, T48, X65, T35, waysA_in_gga(s(T49), T33, T68))
PI_IN_GGAGGAA(T49, T33, T68, T51, T48, X65, T35) → WAYSA_IN_GGA(s(T49), T33, T68)
WAYSA_IN_GGA(s(T110), .(s(T105), T106), T108) → U2_GGA(T110, T105, T106, T108, pC_in_gagga(T110, X161, T105, T106, T108))
WAYSA_IN_GGA(s(T110), .(s(T105), T106), T108) → PC_IN_GAGGA(T110, X161, T105, T106, T108)
PC_IN_GAGGA(T110, T111, T105, T106, T108) → U17_GAGGA(T110, T111, T105, T106, T108, plusH_in_gag(T110, T111, T105))
PC_IN_GAGGA(T110, T111, T105, T106, T108) → PLUSH_IN_GAG(T110, T111, T105)
PLUSH_IN_GAG(T117, X178, T118) → U10_GAG(T117, X178, T118, plusG_in_gag(T117, X178, T118))
PLUSH_IN_GAG(T117, X178, T118) → PLUSG_IN_GAG(T117, X178, T118)
PLUSG_IN_GAG(0, T124, s(T124)) → U8_GAG(T124, natD_in_g(s(T124)))
PLUSG_IN_GAG(0, T124, s(T124)) → NATD_IN_G(s(T124))
PLUSG_IN_GAG(s(T129), X202, s(T130)) → U9_GAG(T129, X202, T130, plusG_in_gag(T129, X202, T130))
PLUSG_IN_GAG(s(T129), X202, s(T130)) → PLUSG_IN_GAG(T129, X202, T130)
U17_GAGGA(T110, T111, T105, T106, T108, plusH_out_gag(T110, T111, T105)) → U18_GAGGA(T110, T111, T105, T106, T108, waysA_in_gga(s(T110), T106, T108))
U17_GAGGA(T110, T111, T105, T106, T108, plusH_out_gag(T110, T111, T105)) → WAYSA_IN_GGA(s(T110), T106, T108)
U13_GGAGGAA(T49, T33, T68, T51, T48, X65, T35, waysA_out_gga(s(T49), T33, T68)) → U14_GGAGGAA(T49, T33, T68, T51, T48, X65, T35, pJ_in_gggaga(T51, T48, T33, X65, T68, T35))
U13_GGAGGAA(T49, T33, T68, T51, T48, X65, T35, waysA_out_gga(s(T49), T33, T68)) → PJ_IN_GGGAGA(T51, T48, T33, X65, T68, T35)
PJ_IN_GGGAGA(T51, T48, T33, T73, T68, T35) → U15_GGGAGA(T51, T48, T33, T73, T68, T35, waysA_in_gga(T51, .(s(T48), T33), T73))
PJ_IN_GGGAGA(T51, T48, T33, T73, T68, T35) → WAYSA_IN_GGA(T51, .(s(T48), T33), T73)
U15_GGGAGA(T51, T48, T33, T73, T68, T35, waysA_out_gga(T51, .(s(T48), T33), T73)) → U16_GGGAGA(T51, T48, T33, T73, T68, T35, plusF_in_gga(T68, T73, T35))
U15_GGGAGA(T51, T48, T33, T73, T68, T35, waysA_out_gga(T51, .(s(T48), T33), T73)) → PLUSF_IN_GGA(T68, T73, T35)
PLUSF_IN_GGA(0, T83, T83) → U6_GGA(T83, natD_in_g(T83))
PLUSF_IN_GGA(0, T83, T83) → NATD_IN_G(T83)
PLUSF_IN_GGA(s(T90), T91, s(T93)) → U7_GGA(T90, T91, T93, plusF_in_gga(T90, T91, T93))
PLUSF_IN_GGA(s(T90), T91, s(T93)) → PLUSF_IN_GGA(T90, T91, T93)

The TRS R consists of the following rules:

waysA_in_gga(0, T5, s(0)) → waysA_out_gga(0, T5, s(0))
waysA_in_gga(0, [], 0) → waysA_out_gga(0, [], 0)
waysA_in_gga(T24, [], 0) → waysA_out_gga(T24, [], 0)
waysA_in_gga(s(T49), .(s(T48), T33), T35) → U1_gga(T49, T48, T33, T35, pB_in_gaggaaa(T48, X90, T49, T33, X64, X65, T35))
pB_in_gaggaaa(T48, T51, T49, T33, X64, X65, T35) → U11_gaggaaa(T48, T51, T49, T33, X64, X65, T35, plusE_in_gag(T48, T51, T49))
plusE_in_gag(0, T57, T57) → U4_gag(T57, natD_in_g(T57))
natD_in_g(0) → natD_out_g(0)
natD_in_g(s(T60)) → U3_g(T60, natD_in_g(T60))
U3_g(T60, natD_out_g(T60)) → natD_out_g(s(T60))
U4_gag(T57, natD_out_g(T57)) → plusE_out_gag(0, T57, T57)
plusE_in_gag(s(T65), X119, s(T66)) → U5_gag(T65, X119, T66, plusE_in_gag(T65, X119, T66))
U5_gag(T65, X119, T66, plusE_out_gag(T65, X119, T66)) → plusE_out_gag(s(T65), X119, s(T66))
U11_gaggaaa(T48, T51, T49, T33, X64, X65, T35, plusE_out_gag(T48, T51, T49)) → U12_gaggaaa(T48, T51, T49, T33, X64, X65, T35, pI_in_ggaggaa(T49, T33, X64, T51, T48, X65, T35))
pI_in_ggaggaa(T49, T33, T68, T51, T48, X65, T35) → U13_ggaggaa(T49, T33, T68, T51, T48, X65, T35, waysA_in_gga(s(T49), T33, T68))
waysA_in_gga(s(T110), .(s(T105), T106), T108) → U2_gga(T110, T105, T106, T108, pC_in_gagga(T110, X161, T105, T106, T108))
pC_in_gagga(T110, T111, T105, T106, T108) → U17_gagga(T110, T111, T105, T106, T108, plusH_in_gag(T110, T111, T105))
plusH_in_gag(T117, X178, T118) → U10_gag(T117, X178, T118, plusG_in_gag(T117, X178, T118))
plusG_in_gag(0, T124, s(T124)) → U8_gag(T124, natD_in_g(s(T124)))
U8_gag(T124, natD_out_g(s(T124))) → plusG_out_gag(0, T124, s(T124))
plusG_in_gag(s(T129), X202, s(T130)) → U9_gag(T129, X202, T130, plusG_in_gag(T129, X202, T130))
U9_gag(T129, X202, T130, plusG_out_gag(T129, X202, T130)) → plusG_out_gag(s(T129), X202, s(T130))
U10_gag(T117, X178, T118, plusG_out_gag(T117, X178, T118)) → plusH_out_gag(T117, X178, T118)
U17_gagga(T110, T111, T105, T106, T108, plusH_out_gag(T110, T111, T105)) → U18_gagga(T110, T111, T105, T106, T108, waysA_in_gga(s(T110), T106, T108))
U18_gagga(T110, T111, T105, T106, T108, waysA_out_gga(s(T110), T106, T108)) → pC_out_gagga(T110, T111, T105, T106, T108)
U2_gga(T110, T105, T106, T108, pC_out_gagga(T110, X161, T105, T106, T108)) → waysA_out_gga(s(T110), .(s(T105), T106), T108)
U13_ggaggaa(T49, T33, T68, T51, T48, X65, T35, waysA_out_gga(s(T49), T33, T68)) → U14_ggaggaa(T49, T33, T68, T51, T48, X65, T35, pJ_in_gggaga(T51, T48, T33, X65, T68, T35))
pJ_in_gggaga(T51, T48, T33, T73, T68, T35) → U15_gggaga(T51, T48, T33, T73, T68, T35, waysA_in_gga(T51, .(s(T48), T33), T73))
U15_gggaga(T51, T48, T33, T73, T68, T35, waysA_out_gga(T51, .(s(T48), T33), T73)) → U16_gggaga(T51, T48, T33, T73, T68, T35, plusF_in_gga(T68, T73, T35))
plusF_in_gga(0, T83, T83) → U6_gga(T83, natD_in_g(T83))
U6_gga(T83, natD_out_g(T83)) → plusF_out_gga(0, T83, T83)
plusF_in_gga(s(T90), T91, s(T93)) → U7_gga(T90, T91, T93, plusF_in_gga(T90, T91, T93))
U7_gga(T90, T91, T93, plusF_out_gga(T90, T91, T93)) → plusF_out_gga(s(T90), T91, s(T93))
U16_gggaga(T51, T48, T33, T73, T68, T35, plusF_out_gga(T68, T73, T35)) → pJ_out_gggaga(T51, T48, T33, T73, T68, T35)
U14_ggaggaa(T49, T33, T68, T51, T48, X65, T35, pJ_out_gggaga(T51, T48, T33, X65, T68, T35)) → pI_out_ggaggaa(T49, T33, T68, T51, T48, X65, T35)
U12_gaggaaa(T48, T51, T49, T33, X64, X65, T35, pI_out_ggaggaa(T49, T33, X64, T51, T48, X65, T35)) → pB_out_gaggaaa(T48, T51, T49, T33, X64, X65, T35)
U1_gga(T49, T48, T33, T35, pB_out_gaggaaa(T48, X90, T49, T33, X64, X65, T35)) → waysA_out_gga(s(T49), .(s(T48), T33), T35)

The argument filtering Pi contains the following mapping:
waysA_in_gga(x1, x2, x3)  =  waysA_in_gga(x1, x2)
0  =  0
waysA_out_gga(x1, x2, x3)  =  waysA_out_gga(x1, x2, x3)
[]  =  []
s(x1)  =  s(x1)
.(x1, x2)  =  .(x1, x2)
U1_gga(x1, x2, x3, x4, x5)  =  U1_gga(x1, x2, x3, x5)
pB_in_gaggaaa(x1, x2, x3, x4, x5, x6, x7)  =  pB_in_gaggaaa(x1, x3, x4)
U11_gaggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U11_gaggaaa(x1, x3, x4, x8)
plusE_in_gag(x1, x2, x3)  =  plusE_in_gag(x1, x3)
U4_gag(x1, x2)  =  U4_gag(x1, x2)
natD_in_g(x1)  =  natD_in_g(x1)
natD_out_g(x1)  =  natD_out_g(x1)
U3_g(x1, x2)  =  U3_g(x1, x2)
plusE_out_gag(x1, x2, x3)  =  plusE_out_gag(x1, x2, x3)
U5_gag(x1, x2, x3, x4)  =  U5_gag(x1, x3, x4)
U12_gaggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_gaggaaa(x1, x2, x3, x4, x8)
pI_in_ggaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pI_in_ggaggaa(x1, x2, x4, x5)
U13_ggaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_ggaggaa(x1, x2, x4, x5, x8)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
pC_in_gagga(x1, x2, x3, x4, x5)  =  pC_in_gagga(x1, x3, x4)
U17_gagga(x1, x2, x3, x4, x5, x6)  =  U17_gagga(x1, x3, x4, x6)
plusH_in_gag(x1, x2, x3)  =  plusH_in_gag(x1, x3)
U10_gag(x1, x2, x3, x4)  =  U10_gag(x1, x3, x4)
plusG_in_gag(x1, x2, x3)  =  plusG_in_gag(x1, x3)
U8_gag(x1, x2)  =  U8_gag(x1, x2)
plusG_out_gag(x1, x2, x3)  =  plusG_out_gag(x1, x2, x3)
U9_gag(x1, x2, x3, x4)  =  U9_gag(x1, x3, x4)
plusH_out_gag(x1, x2, x3)  =  plusH_out_gag(x1, x2, x3)
U18_gagga(x1, x2, x3, x4, x5, x6)  =  U18_gagga(x1, x2, x3, x4, x6)
pC_out_gagga(x1, x2, x3, x4, x5)  =  pC_out_gagga(x1, x2, x3, x4, x5)
U14_ggaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U14_ggaggaa(x1, x2, x3, x4, x5, x8)
pJ_in_gggaga(x1, x2, x3, x4, x5, x6)  =  pJ_in_gggaga(x1, x2, x3, x5)
U15_gggaga(x1, x2, x3, x4, x5, x6, x7)  =  U15_gggaga(x1, x2, x3, x5, x7)
U16_gggaga(x1, x2, x3, x4, x5, x6, x7)  =  U16_gggaga(x1, x2, x3, x4, x5, x7)
plusF_in_gga(x1, x2, x3)  =  plusF_in_gga(x1, x2)
U6_gga(x1, x2)  =  U6_gga(x1, x2)
plusF_out_gga(x1, x2, x3)  =  plusF_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pJ_out_gggaga(x1, x2, x3, x4, x5, x6)  =  pJ_out_gggaga(x1, x2, x3, x4, x5, x6)
pI_out_ggaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pI_out_ggaggaa(x1, x2, x3, x4, x5, x6, x7)
pB_out_gaggaaa(x1, x2, x3, x4, x5, x6, x7)  =  pB_out_gaggaaa(x1, x2, x3, x4, x5, x6, x7)
WAYSA_IN_GGA(x1, x2, x3)  =  WAYSA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4, x5)  =  U1_GGA(x1, x2, x3, x5)
PB_IN_GAGGAAA(x1, x2, x3, x4, x5, x6, x7)  =  PB_IN_GAGGAAA(x1, x3, x4)
U11_GAGGAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U11_GAGGAAA(x1, x3, x4, x8)
PLUSE_IN_GAG(x1, x2, x3)  =  PLUSE_IN_GAG(x1, x3)
U4_GAG(x1, x2)  =  U4_GAG(x1, x2)
NATD_IN_G(x1)  =  NATD_IN_G(x1)
U3_G(x1, x2)  =  U3_G(x1, x2)
U5_GAG(x1, x2, x3, x4)  =  U5_GAG(x1, x3, x4)
U12_GAGGAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_GAGGAAA(x1, x2, x3, x4, x8)
PI_IN_GGAGGAA(x1, x2, x3, x4, x5, x6, x7)  =  PI_IN_GGAGGAA(x1, x2, x4, x5)
U13_GGAGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_GGAGGAA(x1, x2, x4, x5, x8)
U2_GGA(x1, x2, x3, x4, x5)  =  U2_GGA(x1, x2, x3, x5)
PC_IN_GAGGA(x1, x2, x3, x4, x5)  =  PC_IN_GAGGA(x1, x3, x4)
U17_GAGGA(x1, x2, x3, x4, x5, x6)  =  U17_GAGGA(x1, x3, x4, x6)
PLUSH_IN_GAG(x1, x2, x3)  =  PLUSH_IN_GAG(x1, x3)
U10_GAG(x1, x2, x3, x4)  =  U10_GAG(x1, x3, x4)
PLUSG_IN_GAG(x1, x2, x3)  =  PLUSG_IN_GAG(x1, x3)
U8_GAG(x1, x2)  =  U8_GAG(x1, x2)
U9_GAG(x1, x2, x3, x4)  =  U9_GAG(x1, x3, x4)
U18_GAGGA(x1, x2, x3, x4, x5, x6)  =  U18_GAGGA(x1, x2, x3, x4, x6)
U14_GGAGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U14_GGAGGAA(x1, x2, x3, x4, x5, x8)
PJ_IN_GGGAGA(x1, x2, x3, x4, x5, x6)  =  PJ_IN_GGGAGA(x1, x2, x3, x5)
U15_GGGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U15_GGGAGA(x1, x2, x3, x5, x7)
U16_GGGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U16_GGGAGA(x1, x2, x3, x4, x5, x7)
PLUSF_IN_GGA(x1, x2, x3)  =  PLUSF_IN_GGA(x1, x2)
U6_GGA(x1, x2)  =  U6_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 5 SCCs with 22 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

NATD_IN_G(s(T60)) → NATD_IN_G(T60)

The TRS R consists of the following rules:

waysA_in_gga(0, T5, s(0)) → waysA_out_gga(0, T5, s(0))
waysA_in_gga(0, [], 0) → waysA_out_gga(0, [], 0)
waysA_in_gga(T24, [], 0) → waysA_out_gga(T24, [], 0)
waysA_in_gga(s(T49), .(s(T48), T33), T35) → U1_gga(T49, T48, T33, T35, pB_in_gaggaaa(T48, X90, T49, T33, X64, X65, T35))
pB_in_gaggaaa(T48, T51, T49, T33, X64, X65, T35) → U11_gaggaaa(T48, T51, T49, T33, X64, X65, T35, plusE_in_gag(T48, T51, T49))
plusE_in_gag(0, T57, T57) → U4_gag(T57, natD_in_g(T57))
natD_in_g(0) → natD_out_g(0)
natD_in_g(s(T60)) → U3_g(T60, natD_in_g(T60))
U3_g(T60, natD_out_g(T60)) → natD_out_g(s(T60))
U4_gag(T57, natD_out_g(T57)) → plusE_out_gag(0, T57, T57)
plusE_in_gag(s(T65), X119, s(T66)) → U5_gag(T65, X119, T66, plusE_in_gag(T65, X119, T66))
U5_gag(T65, X119, T66, plusE_out_gag(T65, X119, T66)) → plusE_out_gag(s(T65), X119, s(T66))
U11_gaggaaa(T48, T51, T49, T33, X64, X65, T35, plusE_out_gag(T48, T51, T49)) → U12_gaggaaa(T48, T51, T49, T33, X64, X65, T35, pI_in_ggaggaa(T49, T33, X64, T51, T48, X65, T35))
pI_in_ggaggaa(T49, T33, T68, T51, T48, X65, T35) → U13_ggaggaa(T49, T33, T68, T51, T48, X65, T35, waysA_in_gga(s(T49), T33, T68))
waysA_in_gga(s(T110), .(s(T105), T106), T108) → U2_gga(T110, T105, T106, T108, pC_in_gagga(T110, X161, T105, T106, T108))
pC_in_gagga(T110, T111, T105, T106, T108) → U17_gagga(T110, T111, T105, T106, T108, plusH_in_gag(T110, T111, T105))
plusH_in_gag(T117, X178, T118) → U10_gag(T117, X178, T118, plusG_in_gag(T117, X178, T118))
plusG_in_gag(0, T124, s(T124)) → U8_gag(T124, natD_in_g(s(T124)))
U8_gag(T124, natD_out_g(s(T124))) → plusG_out_gag(0, T124, s(T124))
plusG_in_gag(s(T129), X202, s(T130)) → U9_gag(T129, X202, T130, plusG_in_gag(T129, X202, T130))
U9_gag(T129, X202, T130, plusG_out_gag(T129, X202, T130)) → plusG_out_gag(s(T129), X202, s(T130))
U10_gag(T117, X178, T118, plusG_out_gag(T117, X178, T118)) → plusH_out_gag(T117, X178, T118)
U17_gagga(T110, T111, T105, T106, T108, plusH_out_gag(T110, T111, T105)) → U18_gagga(T110, T111, T105, T106, T108, waysA_in_gga(s(T110), T106, T108))
U18_gagga(T110, T111, T105, T106, T108, waysA_out_gga(s(T110), T106, T108)) → pC_out_gagga(T110, T111, T105, T106, T108)
U2_gga(T110, T105, T106, T108, pC_out_gagga(T110, X161, T105, T106, T108)) → waysA_out_gga(s(T110), .(s(T105), T106), T108)
U13_ggaggaa(T49, T33, T68, T51, T48, X65, T35, waysA_out_gga(s(T49), T33, T68)) → U14_ggaggaa(T49, T33, T68, T51, T48, X65, T35, pJ_in_gggaga(T51, T48, T33, X65, T68, T35))
pJ_in_gggaga(T51, T48, T33, T73, T68, T35) → U15_gggaga(T51, T48, T33, T73, T68, T35, waysA_in_gga(T51, .(s(T48), T33), T73))
U15_gggaga(T51, T48, T33, T73, T68, T35, waysA_out_gga(T51, .(s(T48), T33), T73)) → U16_gggaga(T51, T48, T33, T73, T68, T35, plusF_in_gga(T68, T73, T35))
plusF_in_gga(0, T83, T83) → U6_gga(T83, natD_in_g(T83))
U6_gga(T83, natD_out_g(T83)) → plusF_out_gga(0, T83, T83)
plusF_in_gga(s(T90), T91, s(T93)) → U7_gga(T90, T91, T93, plusF_in_gga(T90, T91, T93))
U7_gga(T90, T91, T93, plusF_out_gga(T90, T91, T93)) → plusF_out_gga(s(T90), T91, s(T93))
U16_gggaga(T51, T48, T33, T73, T68, T35, plusF_out_gga(T68, T73, T35)) → pJ_out_gggaga(T51, T48, T33, T73, T68, T35)
U14_ggaggaa(T49, T33, T68, T51, T48, X65, T35, pJ_out_gggaga(T51, T48, T33, X65, T68, T35)) → pI_out_ggaggaa(T49, T33, T68, T51, T48, X65, T35)
U12_gaggaaa(T48, T51, T49, T33, X64, X65, T35, pI_out_ggaggaa(T49, T33, X64, T51, T48, X65, T35)) → pB_out_gaggaaa(T48, T51, T49, T33, X64, X65, T35)
U1_gga(T49, T48, T33, T35, pB_out_gaggaaa(T48, X90, T49, T33, X64, X65, T35)) → waysA_out_gga(s(T49), .(s(T48), T33), T35)

The argument filtering Pi contains the following mapping:
waysA_in_gga(x1, x2, x3)  =  waysA_in_gga(x1, x2)
0  =  0
waysA_out_gga(x1, x2, x3)  =  waysA_out_gga(x1, x2, x3)
[]  =  []
s(x1)  =  s(x1)
.(x1, x2)  =  .(x1, x2)
U1_gga(x1, x2, x3, x4, x5)  =  U1_gga(x1, x2, x3, x5)
pB_in_gaggaaa(x1, x2, x3, x4, x5, x6, x7)  =  pB_in_gaggaaa(x1, x3, x4)
U11_gaggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U11_gaggaaa(x1, x3, x4, x8)
plusE_in_gag(x1, x2, x3)  =  plusE_in_gag(x1, x3)
U4_gag(x1, x2)  =  U4_gag(x1, x2)
natD_in_g(x1)  =  natD_in_g(x1)
natD_out_g(x1)  =  natD_out_g(x1)
U3_g(x1, x2)  =  U3_g(x1, x2)
plusE_out_gag(x1, x2, x3)  =  plusE_out_gag(x1, x2, x3)
U5_gag(x1, x2, x3, x4)  =  U5_gag(x1, x3, x4)
U12_gaggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_gaggaaa(x1, x2, x3, x4, x8)
pI_in_ggaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pI_in_ggaggaa(x1, x2, x4, x5)
U13_ggaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_ggaggaa(x1, x2, x4, x5, x8)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
pC_in_gagga(x1, x2, x3, x4, x5)  =  pC_in_gagga(x1, x3, x4)
U17_gagga(x1, x2, x3, x4, x5, x6)  =  U17_gagga(x1, x3, x4, x6)
plusH_in_gag(x1, x2, x3)  =  plusH_in_gag(x1, x3)
U10_gag(x1, x2, x3, x4)  =  U10_gag(x1, x3, x4)
plusG_in_gag(x1, x2, x3)  =  plusG_in_gag(x1, x3)
U8_gag(x1, x2)  =  U8_gag(x1, x2)
plusG_out_gag(x1, x2, x3)  =  plusG_out_gag(x1, x2, x3)
U9_gag(x1, x2, x3, x4)  =  U9_gag(x1, x3, x4)
plusH_out_gag(x1, x2, x3)  =  plusH_out_gag(x1, x2, x3)
U18_gagga(x1, x2, x3, x4, x5, x6)  =  U18_gagga(x1, x2, x3, x4, x6)
pC_out_gagga(x1, x2, x3, x4, x5)  =  pC_out_gagga(x1, x2, x3, x4, x5)
U14_ggaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U14_ggaggaa(x1, x2, x3, x4, x5, x8)
pJ_in_gggaga(x1, x2, x3, x4, x5, x6)  =  pJ_in_gggaga(x1, x2, x3, x5)
U15_gggaga(x1, x2, x3, x4, x5, x6, x7)  =  U15_gggaga(x1, x2, x3, x5, x7)
U16_gggaga(x1, x2, x3, x4, x5, x6, x7)  =  U16_gggaga(x1, x2, x3, x4, x5, x7)
plusF_in_gga(x1, x2, x3)  =  plusF_in_gga(x1, x2)
U6_gga(x1, x2)  =  U6_gga(x1, x2)
plusF_out_gga(x1, x2, x3)  =  plusF_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pJ_out_gggaga(x1, x2, x3, x4, x5, x6)  =  pJ_out_gggaga(x1, x2, x3, x4, x5, x6)
pI_out_ggaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pI_out_ggaggaa(x1, x2, x3, x4, x5, x6, x7)
pB_out_gaggaaa(x1, x2, x3, x4, x5, x6, x7)  =  pB_out_gaggaaa(x1, x2, x3, x4, x5, x6, x7)
NATD_IN_G(x1)  =  NATD_IN_G(x1)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

NATD_IN_G(s(T60)) → NATD_IN_G(T60)

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

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

NATD_IN_G(s(T60)) → NATD_IN_G(T60)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• NATD_IN_G(s(T60)) → NATD_IN_G(T60)
  The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

PLUSF_IN_GGA(s(T90), T91, s(T93)) → PLUSF_IN_GGA(T90, T91, T93)

The TRS R consists of the following rules:

waysA_in_gga(0, T5, s(0)) → waysA_out_gga(0, T5, s(0))
waysA_in_gga(0, [], 0) → waysA_out_gga(0, [], 0)
waysA_in_gga(T24, [], 0) → waysA_out_gga(T24, [], 0)
waysA_in_gga(s(T49), .(s(T48), T33), T35) → U1_gga(T49, T48, T33, T35, pB_in_gaggaaa(T48, X90, T49, T33, X64, X65, T35))
pB_in_gaggaaa(T48, T51, T49, T33, X64, X65, T35) → U11_gaggaaa(T48, T51, T49, T33, X64, X65, T35, plusE_in_gag(T48, T51, T49))
plusE_in_gag(0, T57, T57) → U4_gag(T57, natD_in_g(T57))
natD_in_g(0) → natD_out_g(0)
natD_in_g(s(T60)) → U3_g(T60, natD_in_g(T60))
U3_g(T60, natD_out_g(T60)) → natD_out_g(s(T60))
U4_gag(T57, natD_out_g(T57)) → plusE_out_gag(0, T57, T57)
plusE_in_gag(s(T65), X119, s(T66)) → U5_gag(T65, X119, T66, plusE_in_gag(T65, X119, T66))
U5_gag(T65, X119, T66, plusE_out_gag(T65, X119, T66)) → plusE_out_gag(s(T65), X119, s(T66))
U11_gaggaaa(T48, T51, T49, T33, X64, X65, T35, plusE_out_gag(T48, T51, T49)) → U12_gaggaaa(T48, T51, T49, T33, X64, X65, T35, pI_in_ggaggaa(T49, T33, X64, T51, T48, X65, T35))
pI_in_ggaggaa(T49, T33, T68, T51, T48, X65, T35) → U13_ggaggaa(T49, T33, T68, T51, T48, X65, T35, waysA_in_gga(s(T49), T33, T68))
waysA_in_gga(s(T110), .(s(T105), T106), T108) → U2_gga(T110, T105, T106, T108, pC_in_gagga(T110, X161, T105, T106, T108))
pC_in_gagga(T110, T111, T105, T106, T108) → U17_gagga(T110, T111, T105, T106, T108, plusH_in_gag(T110, T111, T105))
plusH_in_gag(T117, X178, T118) → U10_gag(T117, X178, T118, plusG_in_gag(T117, X178, T118))
plusG_in_gag(0, T124, s(T124)) → U8_gag(T124, natD_in_g(s(T124)))
U8_gag(T124, natD_out_g(s(T124))) → plusG_out_gag(0, T124, s(T124))
plusG_in_gag(s(T129), X202, s(T130)) → U9_gag(T129, X202, T130, plusG_in_gag(T129, X202, T130))
U9_gag(T129, X202, T130, plusG_out_gag(T129, X202, T130)) → plusG_out_gag(s(T129), X202, s(T130))
U10_gag(T117, X178, T118, plusG_out_gag(T117, X178, T118)) → plusH_out_gag(T117, X178, T118)
U17_gagga(T110, T111, T105, T106, T108, plusH_out_gag(T110, T111, T105)) → U18_gagga(T110, T111, T105, T106, T108, waysA_in_gga(s(T110), T106, T108))
U18_gagga(T110, T111, T105, T106, T108, waysA_out_gga(s(T110), T106, T108)) → pC_out_gagga(T110, T111, T105, T106, T108)
U2_gga(T110, T105, T106, T108, pC_out_gagga(T110, X161, T105, T106, T108)) → waysA_out_gga(s(T110), .(s(T105), T106), T108)
U13_ggaggaa(T49, T33, T68, T51, T48, X65, T35, waysA_out_gga(s(T49), T33, T68)) → U14_ggaggaa(T49, T33, T68, T51, T48, X65, T35, pJ_in_gggaga(T51, T48, T33, X65, T68, T35))
pJ_in_gggaga(T51, T48, T33, T73, T68, T35) → U15_gggaga(T51, T48, T33, T73, T68, T35, waysA_in_gga(T51, .(s(T48), T33), T73))
U15_gggaga(T51, T48, T33, T73, T68, T35, waysA_out_gga(T51, .(s(T48), T33), T73)) → U16_gggaga(T51, T48, T33, T73, T68, T35, plusF_in_gga(T68, T73, T35))
plusF_in_gga(0, T83, T83) → U6_gga(T83, natD_in_g(T83))
U6_gga(T83, natD_out_g(T83)) → plusF_out_gga(0, T83, T83)
plusF_in_gga(s(T90), T91, s(T93)) → U7_gga(T90, T91, T93, plusF_in_gga(T90, T91, T93))
U7_gga(T90, T91, T93, plusF_out_gga(T90, T91, T93)) → plusF_out_gga(s(T90), T91, s(T93))
U16_gggaga(T51, T48, T33, T73, T68, T35, plusF_out_gga(T68, T73, T35)) → pJ_out_gggaga(T51, T48, T33, T73, T68, T35)
U14_ggaggaa(T49, T33, T68, T51, T48, X65, T35, pJ_out_gggaga(T51, T48, T33, X65, T68, T35)) → pI_out_ggaggaa(T49, T33, T68, T51, T48, X65, T35)
U12_gaggaaa(T48, T51, T49, T33, X64, X65, T35, pI_out_ggaggaa(T49, T33, X64, T51, T48, X65, T35)) → pB_out_gaggaaa(T48, T51, T49, T33, X64, X65, T35)
U1_gga(T49, T48, T33, T35, pB_out_gaggaaa(T48, X90, T49, T33, X64, X65, T35)) → waysA_out_gga(s(T49), .(s(T48), T33), T35)

The argument filtering Pi contains the following mapping:
waysA_in_gga(x1, x2, x3)  =  waysA_in_gga(x1, x2)
0  =  0
waysA_out_gga(x1, x2, x3)  =  waysA_out_gga(x1, x2, x3)
[]  =  []
s(x1)  =  s(x1)
.(x1, x2)  =  .(x1, x2)
U1_gga(x1, x2, x3, x4, x5)  =  U1_gga(x1, x2, x3, x5)
pB_in_gaggaaa(x1, x2, x3, x4, x5, x6, x7)  =  pB_in_gaggaaa(x1, x3, x4)
U11_gaggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U11_gaggaaa(x1, x3, x4, x8)
plusE_in_gag(x1, x2, x3)  =  plusE_in_gag(x1, x3)
U4_gag(x1, x2)  =  U4_gag(x1, x2)
natD_in_g(x1)  =  natD_in_g(x1)
natD_out_g(x1)  =  natD_out_g(x1)
U3_g(x1, x2)  =  U3_g(x1, x2)
plusE_out_gag(x1, x2, x3)  =  plusE_out_gag(x1, x2, x3)
U5_gag(x1, x2, x3, x4)  =  U5_gag(x1, x3, x4)
U12_gaggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_gaggaaa(x1, x2, x3, x4, x8)
pI_in_ggaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pI_in_ggaggaa(x1, x2, x4, x5)
U13_ggaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_ggaggaa(x1, x2, x4, x5, x8)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
pC_in_gagga(x1, x2, x3, x4, x5)  =  pC_in_gagga(x1, x3, x4)
U17_gagga(x1, x2, x3, x4, x5, x6)  =  U17_gagga(x1, x3, x4, x6)
plusH_in_gag(x1, x2, x3)  =  plusH_in_gag(x1, x3)
U10_gag(x1, x2, x3, x4)  =  U10_gag(x1, x3, x4)
plusG_in_gag(x1, x2, x3)  =  plusG_in_gag(x1, x3)
U8_gag(x1, x2)  =  U8_gag(x1, x2)
plusG_out_gag(x1, x2, x3)  =  plusG_out_gag(x1, x2, x3)
U9_gag(x1, x2, x3, x4)  =  U9_gag(x1, x3, x4)
plusH_out_gag(x1, x2, x3)  =  plusH_out_gag(x1, x2, x3)
U18_gagga(x1, x2, x3, x4, x5, x6)  =  U18_gagga(x1, x2, x3, x4, x6)
pC_out_gagga(x1, x2, x3, x4, x5)  =  pC_out_gagga(x1, x2, x3, x4, x5)
U14_ggaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U14_ggaggaa(x1, x2, x3, x4, x5, x8)
pJ_in_gggaga(x1, x2, x3, x4, x5, x6)  =  pJ_in_gggaga(x1, x2, x3, x5)
U15_gggaga(x1, x2, x3, x4, x5, x6, x7)  =  U15_gggaga(x1, x2, x3, x5, x7)
U16_gggaga(x1, x2, x3, x4, x5, x6, x7)  =  U16_gggaga(x1, x2, x3, x4, x5, x7)
plusF_in_gga(x1, x2, x3)  =  plusF_in_gga(x1, x2)
U6_gga(x1, x2)  =  U6_gga(x1, x2)
plusF_out_gga(x1, x2, x3)  =  plusF_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pJ_out_gggaga(x1, x2, x3, x4, x5, x6)  =  pJ_out_gggaga(x1, x2, x3, x4, x5, x6)
pI_out_ggaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pI_out_ggaggaa(x1, x2, x3, x4, x5, x6, x7)
pB_out_gaggaaa(x1, x2, x3, x4, x5, x6, x7)  =  pB_out_gaggaaa(x1, x2, x3, x4, x5, x6, x7)
PLUSF_IN_GGA(x1, x2, x3)  =  PLUSF_IN_GGA(x1, x2)

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

PLUSF_IN_GGA(s(T90), T91, s(T93)) → PLUSF_IN_GGA(T90, T91, T93)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
PLUSF_IN_GGA(x1, x2, x3)  =  PLUSF_IN_GGA(x1, x2)

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

PLUSF_IN_GGA(s(T90), T91) → PLUSF_IN_GGA(T90, T91)

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• PLUSF_IN_GGA(s(T90), T91) → PLUSF_IN_GGA(T90, T91)
  The graph contains the following edges 1 > 1, 2 >= 2

(20) YES

(21) Obligation:

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

PLUSG_IN_GAG(s(T129), X202, s(T130)) → PLUSG_IN_GAG(T129, X202, T130)

The TRS R consists of the following rules:

waysA_in_gga(0, T5, s(0)) → waysA_out_gga(0, T5, s(0))
waysA_in_gga(0, [], 0) → waysA_out_gga(0, [], 0)
waysA_in_gga(T24, [], 0) → waysA_out_gga(T24, [], 0)
waysA_in_gga(s(T49), .(s(T48), T33), T35) → U1_gga(T49, T48, T33, T35, pB_in_gaggaaa(T48, X90, T49, T33, X64, X65, T35))
pB_in_gaggaaa(T48, T51, T49, T33, X64, X65, T35) → U11_gaggaaa(T48, T51, T49, T33, X64, X65, T35, plusE_in_gag(T48, T51, T49))
plusE_in_gag(0, T57, T57) → U4_gag(T57, natD_in_g(T57))
natD_in_g(0) → natD_out_g(0)
natD_in_g(s(T60)) → U3_g(T60, natD_in_g(T60))
U3_g(T60, natD_out_g(T60)) → natD_out_g(s(T60))
U4_gag(T57, natD_out_g(T57)) → plusE_out_gag(0, T57, T57)
plusE_in_gag(s(T65), X119, s(T66)) → U5_gag(T65, X119, T66, plusE_in_gag(T65, X119, T66))
U5_gag(T65, X119, T66, plusE_out_gag(T65, X119, T66)) → plusE_out_gag(s(T65), X119, s(T66))
U11_gaggaaa(T48, T51, T49, T33, X64, X65, T35, plusE_out_gag(T48, T51, T49)) → U12_gaggaaa(T48, T51, T49, T33, X64, X65, T35, pI_in_ggaggaa(T49, T33, X64, T51, T48, X65, T35))
pI_in_ggaggaa(T49, T33, T68, T51, T48, X65, T35) → U13_ggaggaa(T49, T33, T68, T51, T48, X65, T35, waysA_in_gga(s(T49), T33, T68))
waysA_in_gga(s(T110), .(s(T105), T106), T108) → U2_gga(T110, T105, T106, T108, pC_in_gagga(T110, X161, T105, T106, T108))
pC_in_gagga(T110, T111, T105, T106, T108) → U17_gagga(T110, T111, T105, T106, T108, plusH_in_gag(T110, T111, T105))
plusH_in_gag(T117, X178, T118) → U10_gag(T117, X178, T118, plusG_in_gag(T117, X178, T118))
plusG_in_gag(0, T124, s(T124)) → U8_gag(T124, natD_in_g(s(T124)))
U8_gag(T124, natD_out_g(s(T124))) → plusG_out_gag(0, T124, s(T124))
plusG_in_gag(s(T129), X202, s(T130)) → U9_gag(T129, X202, T130, plusG_in_gag(T129, X202, T130))
U9_gag(T129, X202, T130, plusG_out_gag(T129, X202, T130)) → plusG_out_gag(s(T129), X202, s(T130))
U10_gag(T117, X178, T118, plusG_out_gag(T117, X178, T118)) → plusH_out_gag(T117, X178, T118)
U17_gagga(T110, T111, T105, T106, T108, plusH_out_gag(T110, T111, T105)) → U18_gagga(T110, T111, T105, T106, T108, waysA_in_gga(s(T110), T106, T108))
U18_gagga(T110, T111, T105, T106, T108, waysA_out_gga(s(T110), T106, T108)) → pC_out_gagga(T110, T111, T105, T106, T108)
U2_gga(T110, T105, T106, T108, pC_out_gagga(T110, X161, T105, T106, T108)) → waysA_out_gga(s(T110), .(s(T105), T106), T108)
U13_ggaggaa(T49, T33, T68, T51, T48, X65, T35, waysA_out_gga(s(T49), T33, T68)) → U14_ggaggaa(T49, T33, T68, T51, T48, X65, T35, pJ_in_gggaga(T51, T48, T33, X65, T68, T35))
pJ_in_gggaga(T51, T48, T33, T73, T68, T35) → U15_gggaga(T51, T48, T33, T73, T68, T35, waysA_in_gga(T51, .(s(T48), T33), T73))
U15_gggaga(T51, T48, T33, T73, T68, T35, waysA_out_gga(T51, .(s(T48), T33), T73)) → U16_gggaga(T51, T48, T33, T73, T68, T35, plusF_in_gga(T68, T73, T35))
plusF_in_gga(0, T83, T83) → U6_gga(T83, natD_in_g(T83))
U6_gga(T83, natD_out_g(T83)) → plusF_out_gga(0, T83, T83)
plusF_in_gga(s(T90), T91, s(T93)) → U7_gga(T90, T91, T93, plusF_in_gga(T90, T91, T93))
U7_gga(T90, T91, T93, plusF_out_gga(T90, T91, T93)) → plusF_out_gga(s(T90), T91, s(T93))
U16_gggaga(T51, T48, T33, T73, T68, T35, plusF_out_gga(T68, T73, T35)) → pJ_out_gggaga(T51, T48, T33, T73, T68, T35)
U14_ggaggaa(T49, T33, T68, T51, T48, X65, T35, pJ_out_gggaga(T51, T48, T33, X65, T68, T35)) → pI_out_ggaggaa(T49, T33, T68, T51, T48, X65, T35)
U12_gaggaaa(T48, T51, T49, T33, X64, X65, T35, pI_out_ggaggaa(T49, T33, X64, T51, T48, X65, T35)) → pB_out_gaggaaa(T48, T51, T49, T33, X64, X65, T35)
U1_gga(T49, T48, T33, T35, pB_out_gaggaaa(T48, X90, T49, T33, X64, X65, T35)) → waysA_out_gga(s(T49), .(s(T48), T33), T35)

The argument filtering Pi contains the following mapping:
waysA_in_gga(x1, x2, x3)  =  waysA_in_gga(x1, x2)
0  =  0
waysA_out_gga(x1, x2, x3)  =  waysA_out_gga(x1, x2, x3)
[]  =  []
s(x1)  =  s(x1)
.(x1, x2)  =  .(x1, x2)
U1_gga(x1, x2, x3, x4, x5)  =  U1_gga(x1, x2, x3, x5)
pB_in_gaggaaa(x1, x2, x3, x4, x5, x6, x7)  =  pB_in_gaggaaa(x1, x3, x4)
U11_gaggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U11_gaggaaa(x1, x3, x4, x8)
plusE_in_gag(x1, x2, x3)  =  plusE_in_gag(x1, x3)
U4_gag(x1, x2)  =  U4_gag(x1, x2)
natD_in_g(x1)  =  natD_in_g(x1)
natD_out_g(x1)  =  natD_out_g(x1)
U3_g(x1, x2)  =  U3_g(x1, x2)
plusE_out_gag(x1, x2, x3)  =  plusE_out_gag(x1, x2, x3)
U5_gag(x1, x2, x3, x4)  =  U5_gag(x1, x3, x4)
U12_gaggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_gaggaaa(x1, x2, x3, x4, x8)
pI_in_ggaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pI_in_ggaggaa(x1, x2, x4, x5)
U13_ggaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_ggaggaa(x1, x2, x4, x5, x8)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
pC_in_gagga(x1, x2, x3, x4, x5)  =  pC_in_gagga(x1, x3, x4)
U17_gagga(x1, x2, x3, x4, x5, x6)  =  U17_gagga(x1, x3, x4, x6)
plusH_in_gag(x1, x2, x3)  =  plusH_in_gag(x1, x3)
U10_gag(x1, x2, x3, x4)  =  U10_gag(x1, x3, x4)
plusG_in_gag(x1, x2, x3)  =  plusG_in_gag(x1, x3)
U8_gag(x1, x2)  =  U8_gag(x1, x2)
plusG_out_gag(x1, x2, x3)  =  plusG_out_gag(x1, x2, x3)
U9_gag(x1, x2, x3, x4)  =  U9_gag(x1, x3, x4)
plusH_out_gag(x1, x2, x3)  =  plusH_out_gag(x1, x2, x3)
U18_gagga(x1, x2, x3, x4, x5, x6)  =  U18_gagga(x1, x2, x3, x4, x6)
pC_out_gagga(x1, x2, x3, x4, x5)  =  pC_out_gagga(x1, x2, x3, x4, x5)
U14_ggaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U14_ggaggaa(x1, x2, x3, x4, x5, x8)
pJ_in_gggaga(x1, x2, x3, x4, x5, x6)  =  pJ_in_gggaga(x1, x2, x3, x5)
U15_gggaga(x1, x2, x3, x4, x5, x6, x7)  =  U15_gggaga(x1, x2, x3, x5, x7)
U16_gggaga(x1, x2, x3, x4, x5, x6, x7)  =  U16_gggaga(x1, x2, x3, x4, x5, x7)
plusF_in_gga(x1, x2, x3)  =  plusF_in_gga(x1, x2)
U6_gga(x1, x2)  =  U6_gga(x1, x2)
plusF_out_gga(x1, x2, x3)  =  plusF_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pJ_out_gggaga(x1, x2, x3, x4, x5, x6)  =  pJ_out_gggaga(x1, x2, x3, x4, x5, x6)
pI_out_ggaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pI_out_ggaggaa(x1, x2, x3, x4, x5, x6, x7)
pB_out_gaggaaa(x1, x2, x3, x4, x5, x6, x7)  =  pB_out_gaggaaa(x1, x2, x3, x4, x5, x6, x7)
PLUSG_IN_GAG(x1, x2, x3)  =  PLUSG_IN_GAG(x1, x3)

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

PLUSG_IN_GAG(s(T129), X202, s(T130)) → PLUSG_IN_GAG(T129, X202, T130)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
PLUSG_IN_GAG(x1, x2, x3)  =  PLUSG_IN_GAG(x1, x3)

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

PLUSG_IN_GAG(s(T129), s(T130)) → PLUSG_IN_GAG(T129, T130)

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

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

• PLUSG_IN_GAG(s(T129), s(T130)) → PLUSG_IN_GAG(T129, T130)
  The graph contains the following edges 1 > 1, 2 > 2

(27) YES

(28) Obligation:

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

PLUSE_IN_GAG(s(T65), X119, s(T66)) → PLUSE_IN_GAG(T65, X119, T66)

The TRS R consists of the following rules:

waysA_in_gga(0, T5, s(0)) → waysA_out_gga(0, T5, s(0))
waysA_in_gga(0, [], 0) → waysA_out_gga(0, [], 0)
waysA_in_gga(T24, [], 0) → waysA_out_gga(T24, [], 0)
waysA_in_gga(s(T49), .(s(T48), T33), T35) → U1_gga(T49, T48, T33, T35, pB_in_gaggaaa(T48, X90, T49, T33, X64, X65, T35))
pB_in_gaggaaa(T48, T51, T49, T33, X64, X65, T35) → U11_gaggaaa(T48, T51, T49, T33, X64, X65, T35, plusE_in_gag(T48, T51, T49))
plusE_in_gag(0, T57, T57) → U4_gag(T57, natD_in_g(T57))
natD_in_g(0) → natD_out_g(0)
natD_in_g(s(T60)) → U3_g(T60, natD_in_g(T60))
U3_g(T60, natD_out_g(T60)) → natD_out_g(s(T60))
U4_gag(T57, natD_out_g(T57)) → plusE_out_gag(0, T57, T57)
plusE_in_gag(s(T65), X119, s(T66)) → U5_gag(T65, X119, T66, plusE_in_gag(T65, X119, T66))
U5_gag(T65, X119, T66, plusE_out_gag(T65, X119, T66)) → plusE_out_gag(s(T65), X119, s(T66))
U11_gaggaaa(T48, T51, T49, T33, X64, X65, T35, plusE_out_gag(T48, T51, T49)) → U12_gaggaaa(T48, T51, T49, T33, X64, X65, T35, pI_in_ggaggaa(T49, T33, X64, T51, T48, X65, T35))
pI_in_ggaggaa(T49, T33, T68, T51, T48, X65, T35) → U13_ggaggaa(T49, T33, T68, T51, T48, X65, T35, waysA_in_gga(s(T49), T33, T68))
waysA_in_gga(s(T110), .(s(T105), T106), T108) → U2_gga(T110, T105, T106, T108, pC_in_gagga(T110, X161, T105, T106, T108))
pC_in_gagga(T110, T111, T105, T106, T108) → U17_gagga(T110, T111, T105, T106, T108, plusH_in_gag(T110, T111, T105))
plusH_in_gag(T117, X178, T118) → U10_gag(T117, X178, T118, plusG_in_gag(T117, X178, T118))
plusG_in_gag(0, T124, s(T124)) → U8_gag(T124, natD_in_g(s(T124)))
U8_gag(T124, natD_out_g(s(T124))) → plusG_out_gag(0, T124, s(T124))
plusG_in_gag(s(T129), X202, s(T130)) → U9_gag(T129, X202, T130, plusG_in_gag(T129, X202, T130))
U9_gag(T129, X202, T130, plusG_out_gag(T129, X202, T130)) → plusG_out_gag(s(T129), X202, s(T130))
U10_gag(T117, X178, T118, plusG_out_gag(T117, X178, T118)) → plusH_out_gag(T117, X178, T118)
U17_gagga(T110, T111, T105, T106, T108, plusH_out_gag(T110, T111, T105)) → U18_gagga(T110, T111, T105, T106, T108, waysA_in_gga(s(T110), T106, T108))
U18_gagga(T110, T111, T105, T106, T108, waysA_out_gga(s(T110), T106, T108)) → pC_out_gagga(T110, T111, T105, T106, T108)
U2_gga(T110, T105, T106, T108, pC_out_gagga(T110, X161, T105, T106, T108)) → waysA_out_gga(s(T110), .(s(T105), T106), T108)
U13_ggaggaa(T49, T33, T68, T51, T48, X65, T35, waysA_out_gga(s(T49), T33, T68)) → U14_ggaggaa(T49, T33, T68, T51, T48, X65, T35, pJ_in_gggaga(T51, T48, T33, X65, T68, T35))
pJ_in_gggaga(T51, T48, T33, T73, T68, T35) → U15_gggaga(T51, T48, T33, T73, T68, T35, waysA_in_gga(T51, .(s(T48), T33), T73))
U15_gggaga(T51, T48, T33, T73, T68, T35, waysA_out_gga(T51, .(s(T48), T33), T73)) → U16_gggaga(T51, T48, T33, T73, T68, T35, plusF_in_gga(T68, T73, T35))
plusF_in_gga(0, T83, T83) → U6_gga(T83, natD_in_g(T83))
U6_gga(T83, natD_out_g(T83)) → plusF_out_gga(0, T83, T83)
plusF_in_gga(s(T90), T91, s(T93)) → U7_gga(T90, T91, T93, plusF_in_gga(T90, T91, T93))
U7_gga(T90, T91, T93, plusF_out_gga(T90, T91, T93)) → plusF_out_gga(s(T90), T91, s(T93))
U16_gggaga(T51, T48, T33, T73, T68, T35, plusF_out_gga(T68, T73, T35)) → pJ_out_gggaga(T51, T48, T33, T73, T68, T35)
U14_ggaggaa(T49, T33, T68, T51, T48, X65, T35, pJ_out_gggaga(T51, T48, T33, X65, T68, T35)) → pI_out_ggaggaa(T49, T33, T68, T51, T48, X65, T35)
U12_gaggaaa(T48, T51, T49, T33, X64, X65, T35, pI_out_ggaggaa(T49, T33, X64, T51, T48, X65, T35)) → pB_out_gaggaaa(T48, T51, T49, T33, X64, X65, T35)
U1_gga(T49, T48, T33, T35, pB_out_gaggaaa(T48, X90, T49, T33, X64, X65, T35)) → waysA_out_gga(s(T49), .(s(T48), T33), T35)

The argument filtering Pi contains the following mapping:
waysA_in_gga(x1, x2, x3)  =  waysA_in_gga(x1, x2)
0  =  0
waysA_out_gga(x1, x2, x3)  =  waysA_out_gga(x1, x2, x3)
[]  =  []
s(x1)  =  s(x1)
.(x1, x2)  =  .(x1, x2)
U1_gga(x1, x2, x3, x4, x5)  =  U1_gga(x1, x2, x3, x5)
pB_in_gaggaaa(x1, x2, x3, x4, x5, x6, x7)  =  pB_in_gaggaaa(x1, x3, x4)
U11_gaggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U11_gaggaaa(x1, x3, x4, x8)
plusE_in_gag(x1, x2, x3)  =  plusE_in_gag(x1, x3)
U4_gag(x1, x2)  =  U4_gag(x1, x2)
natD_in_g(x1)  =  natD_in_g(x1)
natD_out_g(x1)  =  natD_out_g(x1)
U3_g(x1, x2)  =  U3_g(x1, x2)
plusE_out_gag(x1, x2, x3)  =  plusE_out_gag(x1, x2, x3)
U5_gag(x1, x2, x3, x4)  =  U5_gag(x1, x3, x4)
U12_gaggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_gaggaaa(x1, x2, x3, x4, x8)
pI_in_ggaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pI_in_ggaggaa(x1, x2, x4, x5)
U13_ggaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_ggaggaa(x1, x2, x4, x5, x8)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
pC_in_gagga(x1, x2, x3, x4, x5)  =  pC_in_gagga(x1, x3, x4)
U17_gagga(x1, x2, x3, x4, x5, x6)  =  U17_gagga(x1, x3, x4, x6)
plusH_in_gag(x1, x2, x3)  =  plusH_in_gag(x1, x3)
U10_gag(x1, x2, x3, x4)  =  U10_gag(x1, x3, x4)
plusG_in_gag(x1, x2, x3)  =  plusG_in_gag(x1, x3)
U8_gag(x1, x2)  =  U8_gag(x1, x2)
plusG_out_gag(x1, x2, x3)  =  plusG_out_gag(x1, x2, x3)
U9_gag(x1, x2, x3, x4)  =  U9_gag(x1, x3, x4)
plusH_out_gag(x1, x2, x3)  =  plusH_out_gag(x1, x2, x3)
U18_gagga(x1, x2, x3, x4, x5, x6)  =  U18_gagga(x1, x2, x3, x4, x6)
pC_out_gagga(x1, x2, x3, x4, x5)  =  pC_out_gagga(x1, x2, x3, x4, x5)
U14_ggaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U14_ggaggaa(x1, x2, x3, x4, x5, x8)
pJ_in_gggaga(x1, x2, x3, x4, x5, x6)  =  pJ_in_gggaga(x1, x2, x3, x5)
U15_gggaga(x1, x2, x3, x4, x5, x6, x7)  =  U15_gggaga(x1, x2, x3, x5, x7)
U16_gggaga(x1, x2, x3, x4, x5, x6, x7)  =  U16_gggaga(x1, x2, x3, x4, x5, x7)
plusF_in_gga(x1, x2, x3)  =  plusF_in_gga(x1, x2)
U6_gga(x1, x2)  =  U6_gga(x1, x2)
plusF_out_gga(x1, x2, x3)  =  plusF_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pJ_out_gggaga(x1, x2, x3, x4, x5, x6)  =  pJ_out_gggaga(x1, x2, x3, x4, x5, x6)
pI_out_ggaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pI_out_ggaggaa(x1, x2, x3, x4, x5, x6, x7)
pB_out_gaggaaa(x1, x2, x3, x4, x5, x6, x7)  =  pB_out_gaggaaa(x1, x2, x3, x4, x5, x6, x7)
PLUSE_IN_GAG(x1, x2, x3)  =  PLUSE_IN_GAG(x1, x3)

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

(29) UsableRulesProof (EQUIVALENT transformation)

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

(30) Obligation:

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

PLUSE_IN_GAG(s(T65), X119, s(T66)) → PLUSE_IN_GAG(T65, X119, T66)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
PLUSE_IN_GAG(x1, x2, x3)  =  PLUSE_IN_GAG(x1, x3)

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

(31) PiDPToQDPProof (SOUND transformation)

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

(32) Obligation:

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

PLUSE_IN_GAG(s(T65), s(T66)) → PLUSE_IN_GAG(T65, T66)

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

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

• PLUSE_IN_GAG(s(T65), s(T66)) → PLUSE_IN_GAG(T65, T66)
  The graph contains the following edges 1 > 1, 2 > 2

(34) YES

(35) Obligation:

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

WAYSA_IN_GGA(s(T49), .(s(T48), T33), T35) → PB_IN_GAGGAAA(T48, X90, T49, T33, X64, X65, T35)
PB_IN_GAGGAAA(T48, T51, T49, T33, X64, X65, T35) → U11_GAGGAAA(T48, T51, T49, T33, X64, X65, T35, plusE_in_gag(T48, T51, T49))
U11_GAGGAAA(T48, T51, T49, T33, X64, X65, T35, plusE_out_gag(T48, T51, T49)) → PI_IN_GGAGGAA(T49, T33, X64, T51, T48, X65, T35)
PI_IN_GGAGGAA(T49, T33, T68, T51, T48, X65, T35) → U13_GGAGGAA(T49, T33, T68, T51, T48, X65, T35, waysA_in_gga(s(T49), T33, T68))
U13_GGAGGAA(T49, T33, T68, T51, T48, X65, T35, waysA_out_gga(s(T49), T33, T68)) → PJ_IN_GGGAGA(T51, T48, T33, X65, T68, T35)
PJ_IN_GGGAGA(T51, T48, T33, T73, T68, T35) → WAYSA_IN_GGA(T51, .(s(T48), T33), T73)
WAYSA_IN_GGA(s(T110), .(s(T105), T106), T108) → PC_IN_GAGGA(T110, X161, T105, T106, T108)
PC_IN_GAGGA(T110, T111, T105, T106, T108) → U17_GAGGA(T110, T111, T105, T106, T108, plusH_in_gag(T110, T111, T105))
U17_GAGGA(T110, T111, T105, T106, T108, plusH_out_gag(T110, T111, T105)) → WAYSA_IN_GGA(s(T110), T106, T108)
PI_IN_GGAGGAA(T49, T33, T68, T51, T48, X65, T35) → WAYSA_IN_GGA(s(T49), T33, T68)

The TRS R consists of the following rules:

waysA_in_gga(0, T5, s(0)) → waysA_out_gga(0, T5, s(0))
waysA_in_gga(0, [], 0) → waysA_out_gga(0, [], 0)
waysA_in_gga(T24, [], 0) → waysA_out_gga(T24, [], 0)
waysA_in_gga(s(T49), .(s(T48), T33), T35) → U1_gga(T49, T48, T33, T35, pB_in_gaggaaa(T48, X90, T49, T33, X64, X65, T35))
pB_in_gaggaaa(T48, T51, T49, T33, X64, X65, T35) → U11_gaggaaa(T48, T51, T49, T33, X64, X65, T35, plusE_in_gag(T48, T51, T49))
plusE_in_gag(0, T57, T57) → U4_gag(T57, natD_in_g(T57))
natD_in_g(0) → natD_out_g(0)
natD_in_g(s(T60)) → U3_g(T60, natD_in_g(T60))
U3_g(T60, natD_out_g(T60)) → natD_out_g(s(T60))
U4_gag(T57, natD_out_g(T57)) → plusE_out_gag(0, T57, T57)
plusE_in_gag(s(T65), X119, s(T66)) → U5_gag(T65, X119, T66, plusE_in_gag(T65, X119, T66))
U5_gag(T65, X119, T66, plusE_out_gag(T65, X119, T66)) → plusE_out_gag(s(T65), X119, s(T66))
U11_gaggaaa(T48, T51, T49, T33, X64, X65, T35, plusE_out_gag(T48, T51, T49)) → U12_gaggaaa(T48, T51, T49, T33, X64, X65, T35, pI_in_ggaggaa(T49, T33, X64, T51, T48, X65, T35))
pI_in_ggaggaa(T49, T33, T68, T51, T48, X65, T35) → U13_ggaggaa(T49, T33, T68, T51, T48, X65, T35, waysA_in_gga(s(T49), T33, T68))
waysA_in_gga(s(T110), .(s(T105), T106), T108) → U2_gga(T110, T105, T106, T108, pC_in_gagga(T110, X161, T105, T106, T108))
pC_in_gagga(T110, T111, T105, T106, T108) → U17_gagga(T110, T111, T105, T106, T108, plusH_in_gag(T110, T111, T105))
plusH_in_gag(T117, X178, T118) → U10_gag(T117, X178, T118, plusG_in_gag(T117, X178, T118))
plusG_in_gag(0, T124, s(T124)) → U8_gag(T124, natD_in_g(s(T124)))
U8_gag(T124, natD_out_g(s(T124))) → plusG_out_gag(0, T124, s(T124))
plusG_in_gag(s(T129), X202, s(T130)) → U9_gag(T129, X202, T130, plusG_in_gag(T129, X202, T130))
U9_gag(T129, X202, T130, plusG_out_gag(T129, X202, T130)) → plusG_out_gag(s(T129), X202, s(T130))
U10_gag(T117, X178, T118, plusG_out_gag(T117, X178, T118)) → plusH_out_gag(T117, X178, T118)
U17_gagga(T110, T111, T105, T106, T108, plusH_out_gag(T110, T111, T105)) → U18_gagga(T110, T111, T105, T106, T108, waysA_in_gga(s(T110), T106, T108))
U18_gagga(T110, T111, T105, T106, T108, waysA_out_gga(s(T110), T106, T108)) → pC_out_gagga(T110, T111, T105, T106, T108)
U2_gga(T110, T105, T106, T108, pC_out_gagga(T110, X161, T105, T106, T108)) → waysA_out_gga(s(T110), .(s(T105), T106), T108)
U13_ggaggaa(T49, T33, T68, T51, T48, X65, T35, waysA_out_gga(s(T49), T33, T68)) → U14_ggaggaa(T49, T33, T68, T51, T48, X65, T35, pJ_in_gggaga(T51, T48, T33, X65, T68, T35))
pJ_in_gggaga(T51, T48, T33, T73, T68, T35) → U15_gggaga(T51, T48, T33, T73, T68, T35, waysA_in_gga(T51, .(s(T48), T33), T73))
U15_gggaga(T51, T48, T33, T73, T68, T35, waysA_out_gga(T51, .(s(T48), T33), T73)) → U16_gggaga(T51, T48, T33, T73, T68, T35, plusF_in_gga(T68, T73, T35))
plusF_in_gga(0, T83, T83) → U6_gga(T83, natD_in_g(T83))
U6_gga(T83, natD_out_g(T83)) → plusF_out_gga(0, T83, T83)
plusF_in_gga(s(T90), T91, s(T93)) → U7_gga(T90, T91, T93, plusF_in_gga(T90, T91, T93))
U7_gga(T90, T91, T93, plusF_out_gga(T90, T91, T93)) → plusF_out_gga(s(T90), T91, s(T93))
U16_gggaga(T51, T48, T33, T73, T68, T35, plusF_out_gga(T68, T73, T35)) → pJ_out_gggaga(T51, T48, T33, T73, T68, T35)
U14_ggaggaa(T49, T33, T68, T51, T48, X65, T35, pJ_out_gggaga(T51, T48, T33, X65, T68, T35)) → pI_out_ggaggaa(T49, T33, T68, T51, T48, X65, T35)
U12_gaggaaa(T48, T51, T49, T33, X64, X65, T35, pI_out_ggaggaa(T49, T33, X64, T51, T48, X65, T35)) → pB_out_gaggaaa(T48, T51, T49, T33, X64, X65, T35)
U1_gga(T49, T48, T33, T35, pB_out_gaggaaa(T48, X90, T49, T33, X64, X65, T35)) → waysA_out_gga(s(T49), .(s(T48), T33), T35)

The argument filtering Pi contains the following mapping:
waysA_in_gga(x1, x2, x3)  =  waysA_in_gga(x1, x2)
0  =  0
waysA_out_gga(x1, x2, x3)  =  waysA_out_gga(x1, x2, x3)
[]  =  []
s(x1)  =  s(x1)
.(x1, x2)  =  .(x1, x2)
U1_gga(x1, x2, x3, x4, x5)  =  U1_gga(x1, x2, x3, x5)
pB_in_gaggaaa(x1, x2, x3, x4, x5, x6, x7)  =  pB_in_gaggaaa(x1, x3, x4)
U11_gaggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U11_gaggaaa(x1, x3, x4, x8)
plusE_in_gag(x1, x2, x3)  =  plusE_in_gag(x1, x3)
U4_gag(x1, x2)  =  U4_gag(x1, x2)
natD_in_g(x1)  =  natD_in_g(x1)
natD_out_g(x1)  =  natD_out_g(x1)
U3_g(x1, x2)  =  U3_g(x1, x2)
plusE_out_gag(x1, x2, x3)  =  plusE_out_gag(x1, x2, x3)
U5_gag(x1, x2, x3, x4)  =  U5_gag(x1, x3, x4)
U12_gaggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_gaggaaa(x1, x2, x3, x4, x8)
pI_in_ggaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pI_in_ggaggaa(x1, x2, x4, x5)
U13_ggaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_ggaggaa(x1, x2, x4, x5, x8)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
pC_in_gagga(x1, x2, x3, x4, x5)  =  pC_in_gagga(x1, x3, x4)
U17_gagga(x1, x2, x3, x4, x5, x6)  =  U17_gagga(x1, x3, x4, x6)
plusH_in_gag(x1, x2, x3)  =  plusH_in_gag(x1, x3)
U10_gag(x1, x2, x3, x4)  =  U10_gag(x1, x3, x4)
plusG_in_gag(x1, x2, x3)  =  plusG_in_gag(x1, x3)
U8_gag(x1, x2)  =  U8_gag(x1, x2)
plusG_out_gag(x1, x2, x3)  =  plusG_out_gag(x1, x2, x3)
U9_gag(x1, x2, x3, x4)  =  U9_gag(x1, x3, x4)
plusH_out_gag(x1, x2, x3)  =  plusH_out_gag(x1, x2, x3)
U18_gagga(x1, x2, x3, x4, x5, x6)  =  U18_gagga(x1, x2, x3, x4, x6)
pC_out_gagga(x1, x2, x3, x4, x5)  =  pC_out_gagga(x1, x2, x3, x4, x5)
U14_ggaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U14_ggaggaa(x1, x2, x3, x4, x5, x8)
pJ_in_gggaga(x1, x2, x3, x4, x5, x6)  =  pJ_in_gggaga(x1, x2, x3, x5)
U15_gggaga(x1, x2, x3, x4, x5, x6, x7)  =  U15_gggaga(x1, x2, x3, x5, x7)
U16_gggaga(x1, x2, x3, x4, x5, x6, x7)  =  U16_gggaga(x1, x2, x3, x4, x5, x7)
plusF_in_gga(x1, x2, x3)  =  plusF_in_gga(x1, x2)
U6_gga(x1, x2)  =  U6_gga(x1, x2)
plusF_out_gga(x1, x2, x3)  =  plusF_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pJ_out_gggaga(x1, x2, x3, x4, x5, x6)  =  pJ_out_gggaga(x1, x2, x3, x4, x5, x6)
pI_out_ggaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pI_out_ggaggaa(x1, x2, x3, x4, x5, x6, x7)
pB_out_gaggaaa(x1, x2, x3, x4, x5, x6, x7)  =  pB_out_gaggaaa(x1, x2, x3, x4, x5, x6, x7)
WAYSA_IN_GGA(x1, x2, x3)  =  WAYSA_IN_GGA(x1, x2)
PB_IN_GAGGAAA(x1, x2, x3, x4, x5, x6, x7)  =  PB_IN_GAGGAAA(x1, x3, x4)
U11_GAGGAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U11_GAGGAAA(x1, x3, x4, x8)
PI_IN_GGAGGAA(x1, x2, x3, x4, x5, x6, x7)  =  PI_IN_GGAGGAA(x1, x2, x4, x5)
U13_GGAGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_GGAGGAA(x1, x2, x4, x5, x8)
PC_IN_GAGGA(x1, x2, x3, x4, x5)  =  PC_IN_GAGGA(x1, x3, x4)
U17_GAGGA(x1, x2, x3, x4, x5, x6)  =  U17_GAGGA(x1, x3, x4, x6)
PJ_IN_GGGAGA(x1, x2, x3, x4, x5, x6)  =  PJ_IN_GGGAGA(x1, x2, x3, x5)

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

(36) UsableRulesProof (EQUIVALENT transformation)

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

(37) Obligation:

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

WAYSA_IN_GGA(s(T49), .(s(T48), T33), T35) → PB_IN_GAGGAAA(T48, X90, T49, T33, X64, X65, T35)
PB_IN_GAGGAAA(T48, T51, T49, T33, X64, X65, T35) → U11_GAGGAAA(T48, T51, T49, T33, X64, X65, T35, plusE_in_gag(T48, T51, T49))
U11_GAGGAAA(T48, T51, T49, T33, X64, X65, T35, plusE_out_gag(T48, T51, T49)) → PI_IN_GGAGGAA(T49, T33, X64, T51, T48, X65, T35)
PI_IN_GGAGGAA(T49, T33, T68, T51, T48, X65, T35) → U13_GGAGGAA(T49, T33, T68, T51, T48, X65, T35, waysA_in_gga(s(T49), T33, T68))
U13_GGAGGAA(T49, T33, T68, T51, T48, X65, T35, waysA_out_gga(s(T49), T33, T68)) → PJ_IN_GGGAGA(T51, T48, T33, X65, T68, T35)
PJ_IN_GGGAGA(T51, T48, T33, T73, T68, T35) → WAYSA_IN_GGA(T51, .(s(T48), T33), T73)
WAYSA_IN_GGA(s(T110), .(s(T105), T106), T108) → PC_IN_GAGGA(T110, X161, T105, T106, T108)
PC_IN_GAGGA(T110, T111, T105, T106, T108) → U17_GAGGA(T110, T111, T105, T106, T108, plusH_in_gag(T110, T111, T105))
U17_GAGGA(T110, T111, T105, T106, T108, plusH_out_gag(T110, T111, T105)) → WAYSA_IN_GGA(s(T110), T106, T108)
PI_IN_GGAGGAA(T49, T33, T68, T51, T48, X65, T35) → WAYSA_IN_GGA(s(T49), T33, T68)

The TRS R consists of the following rules:

plusE_in_gag(0, T57, T57) → U4_gag(T57, natD_in_g(T57))
plusE_in_gag(s(T65), X119, s(T66)) → U5_gag(T65, X119, T66, plusE_in_gag(T65, X119, T66))
waysA_in_gga(T24, [], 0) → waysA_out_gga(T24, [], 0)
waysA_in_gga(s(T49), .(s(T48), T33), T35) → U1_gga(T49, T48, T33, T35, pB_in_gaggaaa(T48, X90, T49, T33, X64, X65, T35))
waysA_in_gga(s(T110), .(s(T105), T106), T108) → U2_gga(T110, T105, T106, T108, pC_in_gagga(T110, X161, T105, T106, T108))
plusH_in_gag(T117, X178, T118) → U10_gag(T117, X178, T118, plusG_in_gag(T117, X178, T118))
U4_gag(T57, natD_out_g(T57)) → plusE_out_gag(0, T57, T57)
U5_gag(T65, X119, T66, plusE_out_gag(T65, X119, T66)) → plusE_out_gag(s(T65), X119, s(T66))
U1_gga(T49, T48, T33, T35, pB_out_gaggaaa(T48, X90, T49, T33, X64, X65, T35)) → waysA_out_gga(s(T49), .(s(T48), T33), T35)
U2_gga(T110, T105, T106, T108, pC_out_gagga(T110, X161, T105, T106, T108)) → waysA_out_gga(s(T110), .(s(T105), T106), T108)
U10_gag(T117, X178, T118, plusG_out_gag(T117, X178, T118)) → plusH_out_gag(T117, X178, T118)
natD_in_g(0) → natD_out_g(0)
natD_in_g(s(T60)) → U3_g(T60, natD_in_g(T60))
pB_in_gaggaaa(T48, T51, T49, T33, X64, X65, T35) → U11_gaggaaa(T48, T51, T49, T33, X64, X65, T35, plusE_in_gag(T48, T51, T49))
pC_in_gagga(T110, T111, T105, T106, T108) → U17_gagga(T110, T111, T105, T106, T108, plusH_in_gag(T110, T111, T105))
plusG_in_gag(0, T124, s(T124)) → U8_gag(T124, natD_in_g(s(T124)))
plusG_in_gag(s(T129), X202, s(T130)) → U9_gag(T129, X202, T130, plusG_in_gag(T129, X202, T130))
U3_g(T60, natD_out_g(T60)) → natD_out_g(s(T60))
U11_gaggaaa(T48, T51, T49, T33, X64, X65, T35, plusE_out_gag(T48, T51, T49)) → U12_gaggaaa(T48, T51, T49, T33, X64, X65, T35, pI_in_ggaggaa(T49, T33, X64, T51, T48, X65, T35))
U17_gagga(T110, T111, T105, T106, T108, plusH_out_gag(T110, T111, T105)) → U18_gagga(T110, T111, T105, T106, T108, waysA_in_gga(s(T110), T106, T108))
U8_gag(T124, natD_out_g(s(T124))) → plusG_out_gag(0, T124, s(T124))
U9_gag(T129, X202, T130, plusG_out_gag(T129, X202, T130)) → plusG_out_gag(s(T129), X202, s(T130))
U12_gaggaaa(T48, T51, T49, T33, X64, X65, T35, pI_out_ggaggaa(T49, T33, X64, T51, T48, X65, T35)) → pB_out_gaggaaa(T48, T51, T49, T33, X64, X65, T35)
U18_gagga(T110, T111, T105, T106, T108, waysA_out_gga(s(T110), T106, T108)) → pC_out_gagga(T110, T111, T105, T106, T108)
pI_in_ggaggaa(T49, T33, T68, T51, T48, X65, T35) → U13_ggaggaa(T49, T33, T68, T51, T48, X65, T35, waysA_in_gga(s(T49), T33, T68))
U13_ggaggaa(T49, T33, T68, T51, T48, X65, T35, waysA_out_gga(s(T49), T33, T68)) → U14_ggaggaa(T49, T33, T68, T51, T48, X65, T35, pJ_in_gggaga(T51, T48, T33, X65, T68, T35))
U14_ggaggaa(T49, T33, T68, T51, T48, X65, T35, pJ_out_gggaga(T51, T48, T33, X65, T68, T35)) → pI_out_ggaggaa(T49, T33, T68, T51, T48, X65, T35)
pJ_in_gggaga(T51, T48, T33, T73, T68, T35) → U15_gggaga(T51, T48, T33, T73, T68, T35, waysA_in_gga(T51, .(s(T48), T33), T73))
U15_gggaga(T51, T48, T33, T73, T68, T35, waysA_out_gga(T51, .(s(T48), T33), T73)) → U16_gggaga(T51, T48, T33, T73, T68, T35, plusF_in_gga(T68, T73, T35))
waysA_in_gga(0, T5, s(0)) → waysA_out_gga(0, T5, s(0))
U16_gggaga(T51, T48, T33, T73, T68, T35, plusF_out_gga(T68, T73, T35)) → pJ_out_gggaga(T51, T48, T33, T73, T68, T35)
plusF_in_gga(0, T83, T83) → U6_gga(T83, natD_in_g(T83))
plusF_in_gga(s(T90), T91, s(T93)) → U7_gga(T90, T91, T93, plusF_in_gga(T90, T91, T93))
U6_gga(T83, natD_out_g(T83)) → plusF_out_gga(0, T83, T83)
U7_gga(T90, T91, T93, plusF_out_gga(T90, T91, T93)) → plusF_out_gga(s(T90), T91, s(T93))

The argument filtering Pi contains the following mapping:
waysA_in_gga(x1, x2, x3)  =  waysA_in_gga(x1, x2)
0  =  0
waysA_out_gga(x1, x2, x3)  =  waysA_out_gga(x1, x2, x3)
[]  =  []
s(x1)  =  s(x1)
.(x1, x2)  =  .(x1, x2)
U1_gga(x1, x2, x3, x4, x5)  =  U1_gga(x1, x2, x3, x5)
pB_in_gaggaaa(x1, x2, x3, x4, x5, x6, x7)  =  pB_in_gaggaaa(x1, x3, x4)
U11_gaggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U11_gaggaaa(x1, x3, x4, x8)
plusE_in_gag(x1, x2, x3)  =  plusE_in_gag(x1, x3)
U4_gag(x1, x2)  =  U4_gag(x1, x2)
natD_in_g(x1)  =  natD_in_g(x1)
natD_out_g(x1)  =  natD_out_g(x1)
U3_g(x1, x2)  =  U3_g(x1, x2)
plusE_out_gag(x1, x2, x3)  =  plusE_out_gag(x1, x2, x3)
U5_gag(x1, x2, x3, x4)  =  U5_gag(x1, x3, x4)
U12_gaggaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_gaggaaa(x1, x2, x3, x4, x8)
pI_in_ggaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pI_in_ggaggaa(x1, x2, x4, x5)
U13_ggaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_ggaggaa(x1, x2, x4, x5, x8)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
pC_in_gagga(x1, x2, x3, x4, x5)  =  pC_in_gagga(x1, x3, x4)
U17_gagga(x1, x2, x3, x4, x5, x6)  =  U17_gagga(x1, x3, x4, x6)
plusH_in_gag(x1, x2, x3)  =  plusH_in_gag(x1, x3)
U10_gag(x1, x2, x3, x4)  =  U10_gag(x1, x3, x4)
plusG_in_gag(x1, x2, x3)  =  plusG_in_gag(x1, x3)
U8_gag(x1, x2)  =  U8_gag(x1, x2)
plusG_out_gag(x1, x2, x3)  =  plusG_out_gag(x1, x2, x3)
U9_gag(x1, x2, x3, x4)  =  U9_gag(x1, x3, x4)
plusH_out_gag(x1, x2, x3)  =  plusH_out_gag(x1, x2, x3)
U18_gagga(x1, x2, x3, x4, x5, x6)  =  U18_gagga(x1, x2, x3, x4, x6)
pC_out_gagga(x1, x2, x3, x4, x5)  =  pC_out_gagga(x1, x2, x3, x4, x5)
U14_ggaggaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  U14_ggaggaa(x1, x2, x3, x4, x5, x8)
pJ_in_gggaga(x1, x2, x3, x4, x5, x6)  =  pJ_in_gggaga(x1, x2, x3, x5)
U15_gggaga(x1, x2, x3, x4, x5, x6, x7)  =  U15_gggaga(x1, x2, x3, x5, x7)
U16_gggaga(x1, x2, x3, x4, x5, x6, x7)  =  U16_gggaga(x1, x2, x3, x4, x5, x7)
plusF_in_gga(x1, x2, x3)  =  plusF_in_gga(x1, x2)
U6_gga(x1, x2)  =  U6_gga(x1, x2)
plusF_out_gga(x1, x2, x3)  =  plusF_out_gga(x1, x2, x3)
U7_gga(x1, x2, x3, x4)  =  U7_gga(x1, x2, x4)
pJ_out_gggaga(x1, x2, x3, x4, x5, x6)  =  pJ_out_gggaga(x1, x2, x3, x4, x5, x6)
pI_out_ggaggaa(x1, x2, x3, x4, x5, x6, x7)  =  pI_out_ggaggaa(x1, x2, x3, x4, x5, x6, x7)
pB_out_gaggaaa(x1, x2, x3, x4, x5, x6, x7)  =  pB_out_gaggaaa(x1, x2, x3, x4, x5, x6, x7)
WAYSA_IN_GGA(x1, x2, x3)  =  WAYSA_IN_GGA(x1, x2)
PB_IN_GAGGAAA(x1, x2, x3, x4, x5, x6, x7)  =  PB_IN_GAGGAAA(x1, x3, x4)
U11_GAGGAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U11_GAGGAAA(x1, x3, x4, x8)
PI_IN_GGAGGAA(x1, x2, x3, x4, x5, x6, x7)  =  PI_IN_GGAGGAA(x1, x2, x4, x5)
U13_GGAGGAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U13_GGAGGAA(x1, x2, x4, x5, x8)
PC_IN_GAGGA(x1, x2, x3, x4, x5)  =  PC_IN_GAGGA(x1, x3, x4)
U17_GAGGA(x1, x2, x3, x4, x5, x6)  =  U17_GAGGA(x1, x3, x4, x6)
PJ_IN_GGGAGA(x1, x2, x3, x4, x5, x6)  =  PJ_IN_GGGAGA(x1, x2, x3, x5)

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

(38) PiDPToQDPProof (SOUND transformation)

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

(39) Obligation:

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

WAYSA_IN_GGA(s(T49), .(s(T48), T33)) → PB_IN_GAGGAAA(T48, T49, T33)
PB_IN_GAGGAAA(T48, T49, T33) → U11_GAGGAAA(T48, T49, T33, plusE_in_gag(T48, T49))
U11_GAGGAAA(T48, T49, T33, plusE_out_gag(T48, T51, T49)) → PI_IN_GGAGGAA(T49, T33, T51, T48)
PI_IN_GGAGGAA(T49, T33, T51, T48) → U13_GGAGGAA(T49, T33, T51, T48, waysA_in_gga(s(T49), T33))
U13_GGAGGAA(T49, T33, T51, T48, waysA_out_gga(s(T49), T33, T68)) → PJ_IN_GGGAGA(T51, T48, T33, T68)
PJ_IN_GGGAGA(T51, T48, T33, T68) → WAYSA_IN_GGA(T51, .(s(T48), T33))
WAYSA_IN_GGA(s(T110), .(s(T105), T106)) → PC_IN_GAGGA(T110, T105, T106)
PC_IN_GAGGA(T110, T105, T106) → U17_GAGGA(T110, T105, T106, plusH_in_gag(T110, T105))
U17_GAGGA(T110, T105, T106, plusH_out_gag(T110, T111, T105)) → WAYSA_IN_GGA(s(T110), T106)
PI_IN_GGAGGAA(T49, T33, T51, T48) → WAYSA_IN_GGA(s(T49), T33)

The TRS R consists of the following rules:

plusE_in_gag(0, T57) → U4_gag(T57, natD_in_g(T57))
plusE_in_gag(s(T65), s(T66)) → U5_gag(T65, T66, plusE_in_gag(T65, T66))
waysA_in_gga(T24, []) → waysA_out_gga(T24, [], 0)
waysA_in_gga(s(T49), .(s(T48), T33)) → U1_gga(T49, T48, T33, pB_in_gaggaaa(T48, T49, T33))
waysA_in_gga(s(T110), .(s(T105), T106)) → U2_gga(T110, T105, T106, pC_in_gagga(T110, T105, T106))
plusH_in_gag(T117, T118) → U10_gag(T117, T118, plusG_in_gag(T117, T118))
U4_gag(T57, natD_out_g(T57)) → plusE_out_gag(0, T57, T57)
U5_gag(T65, T66, plusE_out_gag(T65, X119, T66)) → plusE_out_gag(s(T65), X119, s(T66))
U1_gga(T49, T48, T33, pB_out_gaggaaa(T48, X90, T49, T33, X64, X65, T35)) → waysA_out_gga(s(T49), .(s(T48), T33), T35)
U2_gga(T110, T105, T106, pC_out_gagga(T110, X161, T105, T106, T108)) → waysA_out_gga(s(T110), .(s(T105), T106), T108)
U10_gag(T117, T118, plusG_out_gag(T117, X178, T118)) → plusH_out_gag(T117, X178, T118)
natD_in_g(0) → natD_out_g(0)
natD_in_g(s(T60)) → U3_g(T60, natD_in_g(T60))
pB_in_gaggaaa(T48, T49, T33) → U11_gaggaaa(T48, T49, T33, plusE_in_gag(T48, T49))
pC_in_gagga(T110, T105, T106) → U17_gagga(T110, T105, T106, plusH_in_gag(T110, T105))
plusG_in_gag(0, s(T124)) → U8_gag(T124, natD_in_g(s(T124)))
plusG_in_gag(s(T129), s(T130)) → U9_gag(T129, T130, plusG_in_gag(T129, T130))
U3_g(T60, natD_out_g(T60)) → natD_out_g(s(T60))
U11_gaggaaa(T48, T49, T33, plusE_out_gag(T48, T51, T49)) → U12_gaggaaa(T48, T51, T49, T33, pI_in_ggaggaa(T49, T33, T51, T48))
U17_gagga(T110, T105, T106, plusH_out_gag(T110, T111, T105)) → U18_gagga(T110, T111, T105, T106, waysA_in_gga(s(T110), T106))
U8_gag(T124, natD_out_g(s(T124))) → plusG_out_gag(0, T124, s(T124))
U9_gag(T129, T130, plusG_out_gag(T129, X202, T130)) → plusG_out_gag(s(T129), X202, s(T130))
U12_gaggaaa(T48, T51, T49, T33, pI_out_ggaggaa(T49, T33, X64, T51, T48, X65, T35)) → pB_out_gaggaaa(T48, T51, T49, T33, X64, X65, T35)
U18_gagga(T110, T111, T105, T106, waysA_out_gga(s(T110), T106, T108)) → pC_out_gagga(T110, T111, T105, T106, T108)
pI_in_ggaggaa(T49, T33, T51, T48) → U13_ggaggaa(T49, T33, T51, T48, waysA_in_gga(s(T49), T33))
U13_ggaggaa(T49, T33, T51, T48, waysA_out_gga(s(T49), T33, T68)) → U14_ggaggaa(T49, T33, T68, T51, T48, pJ_in_gggaga(T51, T48, T33, T68))
U14_ggaggaa(T49, T33, T68, T51, T48, pJ_out_gggaga(T51, T48, T33, X65, T68, T35)) → pI_out_ggaggaa(T49, T33, T68, T51, T48, X65, T35)
pJ_in_gggaga(T51, T48, T33, T68) → U15_gggaga(T51, T48, T33, T68, waysA_in_gga(T51, .(s(T48), T33)))
U15_gggaga(T51, T48, T33, T68, waysA_out_gga(T51, .(s(T48), T33), T73)) → U16_gggaga(T51, T48, T33, T73, T68, plusF_in_gga(T68, T73))
waysA_in_gga(0, T5) → waysA_out_gga(0, T5, s(0))
U16_gggaga(T51, T48, T33, T73, T68, plusF_out_gga(T68, T73, T35)) → pJ_out_gggaga(T51, T48, T33, T73, T68, T35)
plusF_in_gga(0, T83) → U6_gga(T83, natD_in_g(T83))
plusF_in_gga(s(T90), T91) → U7_gga(T90, T91, plusF_in_gga(T90, T91))
U6_gga(T83, natD_out_g(T83)) → plusF_out_gga(0, T83, T83)
U7_gga(T90, T91, plusF_out_gga(T90, T91, T93)) → plusF_out_gga(s(T90), T91, s(T93))

The set Q consists of the following terms:

plusE_in_gag(x0, x1)
waysA_in_gga(x0, x1)
plusH_in_gag(x0, x1)
U4_gag(x0, x1)
U5_gag(x0, x1, x2)
U1_gga(x0, x1, x2, x3)
U2_gga(x0, x1, x2, x3)
U10_gag(x0, x1, x2)
natD_in_g(x0)
pB_in_gaggaaa(x0, x1, x2)
pC_in_gagga(x0, x1, x2)
plusG_in_gag(x0, x1)
U3_g(x0, x1)
U11_gaggaaa(x0, x1, x2, x3)
U17_gagga(x0, x1, x2, x3)
U8_gag(x0, x1)
U9_gag(x0, x1, x2)
U12_gaggaaa(x0, x1, x2, x3, x4)
U18_gagga(x0, x1, x2, x3, x4)
pI_in_ggaggaa(x0, x1, x2, x3)
U13_ggaggaa(x0, x1, x2, x3, x4)
U14_ggaggaa(x0, x1, x2, x3, x4, x5)
pJ_in_gggaga(x0, x1, x2, x3)
U15_gggaga(x0, x1, x2, x3, x4)
U16_gggaga(x0, x1, x2, x3, x4, x5)
plusF_in_gga(x0, x1)
U6_gga(x0, x1)
U7_gga(x0, x1, x2)

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

(40) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule PC_IN_GAGGA(T110, T105, T106) → U17_GAGGA(T110, T105, T106, plusH_in_gag(T110, T105)) at position [3] we obtained the following new rules [LPAR04]:

PC_IN_GAGGA(T110, T105, T106) → U17_GAGGA(T110, T105, T106, U10_gag(T110, T105, plusG_in_gag(T110, T105)))

(41) Obligation:

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

WAYSA_IN_GGA(s(T49), .(s(T48), T33)) → PB_IN_GAGGAAA(T48, T49, T33)
PB_IN_GAGGAAA(T48, T49, T33) → U11_GAGGAAA(T48, T49, T33, plusE_in_gag(T48, T49))
U11_GAGGAAA(T48, T49, T33, plusE_out_gag(T48, T51, T49)) → PI_IN_GGAGGAA(T49, T33, T51, T48)
PI_IN_GGAGGAA(T49, T33, T51, T48) → U13_GGAGGAA(T49, T33, T51, T48, waysA_in_gga(s(T49), T33))
U13_GGAGGAA(T49, T33, T51, T48, waysA_out_gga(s(T49), T33, T68)) → PJ_IN_GGGAGA(T51, T48, T33, T68)
PJ_IN_GGGAGA(T51, T48, T33, T68) → WAYSA_IN_GGA(T51, .(s(T48), T33))
WAYSA_IN_GGA(s(T110), .(s(T105), T106)) → PC_IN_GAGGA(T110, T105, T106)
U17_GAGGA(T110, T105, T106, plusH_out_gag(T110, T111, T105)) → WAYSA_IN_GGA(s(T110), T106)
PI_IN_GGAGGAA(T49, T33, T51, T48) → WAYSA_IN_GGA(s(T49), T33)
PC_IN_GAGGA(T110, T105, T106) → U17_GAGGA(T110, T105, T106, U10_gag(T110, T105, plusG_in_gag(T110, T105)))

The TRS R consists of the following rules:

plusE_in_gag(0, T57) → U4_gag(T57, natD_in_g(T57))
plusE_in_gag(s(T65), s(T66)) → U5_gag(T65, T66, plusE_in_gag(T65, T66))
waysA_in_gga(T24, []) → waysA_out_gga(T24, [], 0)
waysA_in_gga(s(T49), .(s(T48), T33)) → U1_gga(T49, T48, T33, pB_in_gaggaaa(T48, T49, T33))
waysA_in_gga(s(T110), .(s(T105), T106)) → U2_gga(T110, T105, T106, pC_in_gagga(T110, T105, T106))
plusH_in_gag(T117, T118) → U10_gag(T117, T118, plusG_in_gag(T117, T118))
U4_gag(T57, natD_out_g(T57)) → plusE_out_gag(0, T57, T57)
U5_gag(T65, T66, plusE_out_gag(T65, X119, T66)) → plusE_out_gag(s(T65), X119, s(T66))
U1_gga(T49, T48, T33, pB_out_gaggaaa(T48, X90, T49, T33, X64, X65, T35)) → waysA_out_gga(s(T49), .(s(T48), T33), T35)
U2_gga(T110, T105, T106, pC_out_gagga(T110, X161, T105, T106, T108)) → waysA_out_gga(s(T110), .(s(T105), T106), T108)
U10_gag(T117, T118, plusG_out_gag(T117, X178, T118)) → plusH_out_gag(T117, X178, T118)
natD_in_g(0) → natD_out_g(0)
natD_in_g(s(T60)) → U3_g(T60, natD_in_g(T60))
pB_in_gaggaaa(T48, T49, T33) → U11_gaggaaa(T48, T49, T33, plusE_in_gag(T48, T49))
pC_in_gagga(T110, T105, T106) → U17_gagga(T110, T105, T106, plusH_in_gag(T110, T105))
plusG_in_gag(0, s(T124)) → U8_gag(T124, natD_in_g(s(T124)))
plusG_in_gag(s(T129), s(T130)) → U9_gag(T129, T130, plusG_in_gag(T129, T130))
U3_g(T60, natD_out_g(T60)) → natD_out_g(s(T60))
U11_gaggaaa(T48, T49, T33, plusE_out_gag(T48, T51, T49)) → U12_gaggaaa(T48, T51, T49, T33, pI_in_ggaggaa(T49, T33, T51, T48))
U17_gagga(T110, T105, T106, plusH_out_gag(T110, T111, T105)) → U18_gagga(T110, T111, T105, T106, waysA_in_gga(s(T110), T106))
U8_gag(T124, natD_out_g(s(T124))) → plusG_out_gag(0, T124, s(T124))
U9_gag(T129, T130, plusG_out_gag(T129, X202, T130)) → plusG_out_gag(s(T129), X202, s(T130))
U12_gaggaaa(T48, T51, T49, T33, pI_out_ggaggaa(T49, T33, X64, T51, T48, X65, T35)) → pB_out_gaggaaa(T48, T51, T49, T33, X64, X65, T35)
U18_gagga(T110, T111, T105, T106, waysA_out_gga(s(T110), T106, T108)) → pC_out_gagga(T110, T111, T105, T106, T108)
pI_in_ggaggaa(T49, T33, T51, T48) → U13_ggaggaa(T49, T33, T51, T48, waysA_in_gga(s(T49), T33))
U13_ggaggaa(T49, T33, T51, T48, waysA_out_gga(s(T49), T33, T68)) → U14_ggaggaa(T49, T33, T68, T51, T48, pJ_in_gggaga(T51, T48, T33, T68))
U14_ggaggaa(T49, T33, T68, T51, T48, pJ_out_gggaga(T51, T48, T33, X65, T68, T35)) → pI_out_ggaggaa(T49, T33, T68, T51, T48, X65, T35)
pJ_in_gggaga(T51, T48, T33, T68) → U15_gggaga(T51, T48, T33, T68, waysA_in_gga(T51, .(s(T48), T33)))
U15_gggaga(T51, T48, T33, T68, waysA_out_gga(T51, .(s(T48), T33), T73)) → U16_gggaga(T51, T48, T33, T73, T68, plusF_in_gga(T68, T73))
waysA_in_gga(0, T5) → waysA_out_gga(0, T5, s(0))
U16_gggaga(T51, T48, T33, T73, T68, plusF_out_gga(T68, T73, T35)) → pJ_out_gggaga(T51, T48, T33, T73, T68, T35)
plusF_in_gga(0, T83) → U6_gga(T83, natD_in_g(T83))
plusF_in_gga(s(T90), T91) → U7_gga(T90, T91, plusF_in_gga(T90, T91))
U6_gga(T83, natD_out_g(T83)) → plusF_out_gga(0, T83, T83)
U7_gga(T90, T91, plusF_out_gga(T90, T91, T93)) → plusF_out_gga(s(T90), T91, s(T93))

The set Q consists of the following terms:

plusE_in_gag(x0, x1)
waysA_in_gga(x0, x1)
plusH_in_gag(x0, x1)
U4_gag(x0, x1)
U5_gag(x0, x1, x2)
U1_gga(x0, x1, x2, x3)
U2_gga(x0, x1, x2, x3)
U10_gag(x0, x1, x2)
natD_in_g(x0)
pB_in_gaggaaa(x0, x1, x2)
pC_in_gagga(x0, x1, x2)
plusG_in_gag(x0, x1)
U3_g(x0, x1)
U11_gaggaaa(x0, x1, x2, x3)
U17_gagga(x0, x1, x2, x3)
U8_gag(x0, x1)
U9_gag(x0, x1, x2)
U12_gaggaaa(x0, x1, x2, x3, x4)
U18_gagga(x0, x1, x2, x3, x4)
pI_in_ggaggaa(x0, x1, x2, x3)
U13_ggaggaa(x0, x1, x2, x3, x4)
U14_ggaggaa(x0, x1, x2, x3, x4, x5)
pJ_in_gggaga(x0, x1, x2, x3)
U15_gggaga(x0, x1, x2, x3, x4)
U16_gggaga(x0, x1, x2, x3, x4, x5)
plusF_in_gga(x0, x1)
U6_gga(x0, x1)
U7_gga(x0, x1, x2)

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

(42) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

WAYSA_IN_GGA(s(T110), .(s(T105), T106)) → PC_IN_GAGGA(T110, T105, T106)
PI_IN_GGAGGAA(T49, T33, T51, T48) → WAYSA_IN_GGA(s(T49), T33)

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

POL(.(x₁, x₂)) = 1 + x₂   
POL(0) = 0   
POL(PB_IN_GAGGAAA(x₁, x₂, x₃)) = 1 + x₃   
POL(PC_IN_GAGGA(x₁, x₂, x₃)) = x₃   
POL(PI_IN_GGAGGAA(x₁, x₂, x₃, x₄)) = 1 + x₂   
POL(PJ_IN_GGGAGA(x₁, x₂, x₃, x₄)) = 1 + x₃   
POL(U10_gag(x₁, x₂, x₃)) = 0   
POL(U11_GAGGAAA(x₁, x₂, x₃, x₄)) = 1 + x₃   
POL(U11_gaggaaa(x₁, x₂, x₃, x₄)) = 0   
POL(U12_gaggaaa(x₁, x₂, x₃, x₄, x₅)) = 0   
POL(U13_GGAGGAA(x₁, x₂, x₃, x₄, x₅)) = 1 + x₂   
POL(U13_ggaggaa(x₁, x₂, x₃, x₄, x₅)) = 0   
POL(U14_ggaggaa(x₁, x₂, x₃, x₄, x₅, x₆)) = 0   
POL(U15_gggaga(x₁, x₂, x₃, x₄, x₅)) = 0   
POL(U16_gggaga(x₁, x₂, x₃, x₄, x₅, x₆)) = 0   
POL(U17_GAGGA(x₁, x₂, x₃, x₄)) = x₃   
POL(U17_gagga(x₁, x₂, x₃, x₄)) = 0   
POL(U18_gagga(x₁, x₂, x₃, x₄, x₅)) = 0   
POL(U1_gga(x₁, x₂, x₃, x₄)) = 0   
POL(U2_gga(x₁, x₂, x₃, x₄)) = 0   
POL(U3_g(x₁, x₂)) = 0   
POL(U4_gag(x₁, x₂)) = 0   
POL(U5_gag(x₁, x₂, x₃)) = 0   
POL(U6_gga(x₁, x₂)) = 0   
POL(U7_gga(x₁, x₂, x₃)) = 0   
POL(U8_gag(x₁, x₂)) = 0   
POL(U9_gag(x₁, x₂, x₃)) = 0   
POL(WAYSA_IN_GGA(x₁, x₂)) = x₂   
POL([]) = 0   
POL(natD_in_g(x₁)) = 0   
POL(natD_out_g(x₁)) = 0   
POL(pB_in_gaggaaa(x₁, x₂, x₃)) = 0   
POL(pB_out_gaggaaa(x₁, x₂, x₃, x₄, x₅, x₆, x₇)) = 0   
POL(pC_in_gagga(x₁, x₂, x₃)) = 0   
POL(pC_out_gagga(x₁, x₂, x₃, x₄, x₅)) = 0   
POL(pI_in_ggaggaa(x₁, x₂, x₃, x₄)) = 0   
POL(pI_out_ggaggaa(x₁, x₂, x₃, x₄, x₅, x₆, x₇)) = 0   
POL(pJ_in_gggaga(x₁, x₂, x₃, x₄)) = 0   
POL(pJ_out_gggaga(x₁, x₂, x₃, x₄, x₅, x₆)) = 0   
POL(plusE_in_gag(x₁, x₂)) = 0   
POL(plusE_out_gag(x₁, x₂, x₃)) = 0   
POL(plusF_in_gga(x₁, x₂)) = 0   
POL(plusF_out_gga(x₁, x₂, x₃)) = 0   
POL(plusG_in_gag(x₁, x₂)) = 0   
POL(plusG_out_gag(x₁, x₂, x₃)) = 0   
POL(plusH_in_gag(x₁, x₂)) = 1 + x₁ + x₂   
POL(plusH_out_gag(x₁, x₂, x₃)) = 0   
POL(s(x₁)) = 0   
POL(waysA_in_gga(x₁, x₂)) = 0   
POL(waysA_out_gga(x₁, x₂, x₃)) = 0   

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

(43) Obligation:

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

WAYSA_IN_GGA(s(T49), .(s(T48), T33)) → PB_IN_GAGGAAA(T48, T49, T33)
PB_IN_GAGGAAA(T48, T49, T33) → U11_GAGGAAA(T48, T49, T33, plusE_in_gag(T48, T49))
U11_GAGGAAA(T48, T49, T33, plusE_out_gag(T48, T51, T49)) → PI_IN_GGAGGAA(T49, T33, T51, T48)
PI_IN_GGAGGAA(T49, T33, T51, T48) → U13_GGAGGAA(T49, T33, T51, T48, waysA_in_gga(s(T49), T33))
U13_GGAGGAA(T49, T33, T51, T48, waysA_out_gga(s(T49), T33, T68)) → PJ_IN_GGGAGA(T51, T48, T33, T68)
PJ_IN_GGGAGA(T51, T48, T33, T68) → WAYSA_IN_GGA(T51, .(s(T48), T33))
U17_GAGGA(T110, T105, T106, plusH_out_gag(T110, T111, T105)) → WAYSA_IN_GGA(s(T110), T106)
PC_IN_GAGGA(T110, T105, T106) → U17_GAGGA(T110, T105, T106, U10_gag(T110, T105, plusG_in_gag(T110, T105)))

The TRS R consists of the following rules:

plusE_in_gag(0, T57) → U4_gag(T57, natD_in_g(T57))
plusE_in_gag(s(T65), s(T66)) → U5_gag(T65, T66, plusE_in_gag(T65, T66))
waysA_in_gga(T24, []) → waysA_out_gga(T24, [], 0)
waysA_in_gga(s(T49), .(s(T48), T33)) → U1_gga(T49, T48, T33, pB_in_gaggaaa(T48, T49, T33))
waysA_in_gga(s(T110), .(s(T105), T106)) → U2_gga(T110, T105, T106, pC_in_gagga(T110, T105, T106))
plusH_in_gag(T117, T118) → U10_gag(T117, T118, plusG_in_gag(T117, T118))
U4_gag(T57, natD_out_g(T57)) → plusE_out_gag(0, T57, T57)
U5_gag(T65, T66, plusE_out_gag(T65, X119, T66)) → plusE_out_gag(s(T65), X119, s(T66))
U1_gga(T49, T48, T33, pB_out_gaggaaa(T48, X90, T49, T33, X64, X65, T35)) → waysA_out_gga(s(T49), .(s(T48), T33), T35)
U2_gga(T110, T105, T106, pC_out_gagga(T110, X161, T105, T106, T108)) → waysA_out_gga(s(T110), .(s(T105), T106), T108)
U10_gag(T117, T118, plusG_out_gag(T117, X178, T118)) → plusH_out_gag(T117, X178, T118)
natD_in_g(0) → natD_out_g(0)
natD_in_g(s(T60)) → U3_g(T60, natD_in_g(T60))
pB_in_gaggaaa(T48, T49, T33) → U11_gaggaaa(T48, T49, T33, plusE_in_gag(T48, T49))
pC_in_gagga(T110, T105, T106) → U17_gagga(T110, T105, T106, plusH_in_gag(T110, T105))
plusG_in_gag(0, s(T124)) → U8_gag(T124, natD_in_g(s(T124)))
plusG_in_gag(s(T129), s(T130)) → U9_gag(T129, T130, plusG_in_gag(T129, T130))
U3_g(T60, natD_out_g(T60)) → natD_out_g(s(T60))
U11_gaggaaa(T48, T49, T33, plusE_out_gag(T48, T51, T49)) → U12_gaggaaa(T48, T51, T49, T33, pI_in_ggaggaa(T49, T33, T51, T48))
U17_gagga(T110, T105, T106, plusH_out_gag(T110, T111, T105)) → U18_gagga(T110, T111, T105, T106, waysA_in_gga(s(T110), T106))
U8_gag(T124, natD_out_g(s(T124))) → plusG_out_gag(0, T124, s(T124))
U9_gag(T129, T130, plusG_out_gag(T129, X202, T130)) → plusG_out_gag(s(T129), X202, s(T130))
U12_gaggaaa(T48, T51, T49, T33, pI_out_ggaggaa(T49, T33, X64, T51, T48, X65, T35)) → pB_out_gaggaaa(T48, T51, T49, T33, X64, X65, T35)
U18_gagga(T110, T111, T105, T106, waysA_out_gga(s(T110), T106, T108)) → pC_out_gagga(T110, T111, T105, T106, T108)
pI_in_ggaggaa(T49, T33, T51, T48) → U13_ggaggaa(T49, T33, T51, T48, waysA_in_gga(s(T49), T33))
U13_ggaggaa(T49, T33, T51, T48, waysA_out_gga(s(T49), T33, T68)) → U14_ggaggaa(T49, T33, T68, T51, T48, pJ_in_gggaga(T51, T48, T33, T68))
U14_ggaggaa(T49, T33, T68, T51, T48, pJ_out_gggaga(T51, T48, T33, X65, T68, T35)) → pI_out_ggaggaa(T49, T33, T68, T51, T48, X65, T35)
pJ_in_gggaga(T51, T48, T33, T68) → U15_gggaga(T51, T48, T33, T68, waysA_in_gga(T51, .(s(T48), T33)))
U15_gggaga(T51, T48, T33, T68, waysA_out_gga(T51, .(s(T48), T33), T73)) → U16_gggaga(T51, T48, T33, T73, T68, plusF_in_gga(T68, T73))
waysA_in_gga(0, T5) → waysA_out_gga(0, T5, s(0))
U16_gggaga(T51, T48, T33, T73, T68, plusF_out_gga(T68, T73, T35)) → pJ_out_gggaga(T51, T48, T33, T73, T68, T35)
plusF_in_gga(0, T83) → U6_gga(T83, natD_in_g(T83))
plusF_in_gga(s(T90), T91) → U7_gga(T90, T91, plusF_in_gga(T90, T91))
U6_gga(T83, natD_out_g(T83)) → plusF_out_gga(0, T83, T83)
U7_gga(T90, T91, plusF_out_gga(T90, T91, T93)) → plusF_out_gga(s(T90), T91, s(T93))

The set Q consists of the following terms:

plusE_in_gag(x0, x1)
waysA_in_gga(x0, x1)
plusH_in_gag(x0, x1)
U4_gag(x0, x1)
U5_gag(x0, x1, x2)
U1_gga(x0, x1, x2, x3)
U2_gga(x0, x1, x2, x3)
U10_gag(x0, x1, x2)
natD_in_g(x0)
pB_in_gaggaaa(x0, x1, x2)
pC_in_gagga(x0, x1, x2)
plusG_in_gag(x0, x1)
U3_g(x0, x1)
U11_gaggaaa(x0, x1, x2, x3)
U17_gagga(x0, x1, x2, x3)
U8_gag(x0, x1)
U9_gag(x0, x1, x2)
U12_gaggaaa(x0, x1, x2, x3, x4)
U18_gagga(x0, x1, x2, x3, x4)
pI_in_ggaggaa(x0, x1, x2, x3)
U13_ggaggaa(x0, x1, x2, x3, x4)
U14_ggaggaa(x0, x1, x2, x3, x4, x5)
pJ_in_gggaga(x0, x1, x2, x3)
U15_gggaga(x0, x1, x2, x3, x4)
U16_gggaga(x0, x1, x2, x3, x4, x5)
plusF_in_gga(x0, x1)
U6_gga(x0, x1)
U7_gga(x0, x1, x2)

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

(44) DependencyGraphProof (EQUIVALENT transformation)

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

(45) Obligation:

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

PB_IN_GAGGAAA(T48, T49, T33) → U11_GAGGAAA(T48, T49, T33, plusE_in_gag(T48, T49))
U11_GAGGAAA(T48, T49, T33, plusE_out_gag(T48, T51, T49)) → PI_IN_GGAGGAA(T49, T33, T51, T48)
PI_IN_GGAGGAA(T49, T33, T51, T48) → U13_GGAGGAA(T49, T33, T51, T48, waysA_in_gga(s(T49), T33))
U13_GGAGGAA(T49, T33, T51, T48, waysA_out_gga(s(T49), T33, T68)) → PJ_IN_GGGAGA(T51, T48, T33, T68)
PJ_IN_GGGAGA(T51, T48, T33, T68) → WAYSA_IN_GGA(T51, .(s(T48), T33))
WAYSA_IN_GGA(s(T49), .(s(T48), T33)) → PB_IN_GAGGAAA(T48, T49, T33)

The TRS R consists of the following rules:

plusE_in_gag(0, T57) → U4_gag(T57, natD_in_g(T57))
plusE_in_gag(s(T65), s(T66)) → U5_gag(T65, T66, plusE_in_gag(T65, T66))
waysA_in_gga(T24, []) → waysA_out_gga(T24, [], 0)
waysA_in_gga(s(T49), .(s(T48), T33)) → U1_gga(T49, T48, T33, pB_in_gaggaaa(T48, T49, T33))
waysA_in_gga(s(T110), .(s(T105), T106)) → U2_gga(T110, T105, T106, pC_in_gagga(T110, T105, T106))
plusH_in_gag(T117, T118) → U10_gag(T117, T118, plusG_in_gag(T117, T118))
U4_gag(T57, natD_out_g(T57)) → plusE_out_gag(0, T57, T57)
U5_gag(T65, T66, plusE_out_gag(T65, X119, T66)) → plusE_out_gag(s(T65), X119, s(T66))
U1_gga(T49, T48, T33, pB_out_gaggaaa(T48, X90, T49, T33, X64, X65, T35)) → waysA_out_gga(s(T49), .(s(T48), T33), T35)
U2_gga(T110, T105, T106, pC_out_gagga(T110, X161, T105, T106, T108)) → waysA_out_gga(s(T110), .(s(T105), T106), T108)
U10_gag(T117, T118, plusG_out_gag(T117, X178, T118)) → plusH_out_gag(T117, X178, T118)
natD_in_g(0) → natD_out_g(0)
natD_in_g(s(T60)) → U3_g(T60, natD_in_g(T60))
pB_in_gaggaaa(T48, T49, T33) → U11_gaggaaa(T48, T49, T33, plusE_in_gag(T48, T49))
pC_in_gagga(T110, T105, T106) → U17_gagga(T110, T105, T106, plusH_in_gag(T110, T105))
plusG_in_gag(0, s(T124)) → U8_gag(T124, natD_in_g(s(T124)))
plusG_in_gag(s(T129), s(T130)) → U9_gag(T129, T130, plusG_in_gag(T129, T130))
U3_g(T60, natD_out_g(T60)) → natD_out_g(s(T60))
U11_gaggaaa(T48, T49, T33, plusE_out_gag(T48, T51, T49)) → U12_gaggaaa(T48, T51, T49, T33, pI_in_ggaggaa(T49, T33, T51, T48))
U17_gagga(T110, T105, T106, plusH_out_gag(T110, T111, T105)) → U18_gagga(T110, T111, T105, T106, waysA_in_gga(s(T110), T106))
U8_gag(T124, natD_out_g(s(T124))) → plusG_out_gag(0, T124, s(T124))
U9_gag(T129, T130, plusG_out_gag(T129, X202, T130)) → plusG_out_gag(s(T129), X202, s(T130))
U12_gaggaaa(T48, T51, T49, T33, pI_out_ggaggaa(T49, T33, X64, T51, T48, X65, T35)) → pB_out_gaggaaa(T48, T51, T49, T33, X64, X65, T35)
U18_gagga(T110, T111, T105, T106, waysA_out_gga(s(T110), T106, T108)) → pC_out_gagga(T110, T111, T105, T106, T108)
pI_in_ggaggaa(T49, T33, T51, T48) → U13_ggaggaa(T49, T33, T51, T48, waysA_in_gga(s(T49), T33))
U13_ggaggaa(T49, T33, T51, T48, waysA_out_gga(s(T49), T33, T68)) → U14_ggaggaa(T49, T33, T68, T51, T48, pJ_in_gggaga(T51, T48, T33, T68))
U14_ggaggaa(T49, T33, T68, T51, T48, pJ_out_gggaga(T51, T48, T33, X65, T68, T35)) → pI_out_ggaggaa(T49, T33, T68, T51, T48, X65, T35)
pJ_in_gggaga(T51, T48, T33, T68) → U15_gggaga(T51, T48, T33, T68, waysA_in_gga(T51, .(s(T48), T33)))
U15_gggaga(T51, T48, T33, T68, waysA_out_gga(T51, .(s(T48), T33), T73)) → U16_gggaga(T51, T48, T33, T73, T68, plusF_in_gga(T68, T73))
waysA_in_gga(0, T5) → waysA_out_gga(0, T5, s(0))
U16_gggaga(T51, T48, T33, T73, T68, plusF_out_gga(T68, T73, T35)) → pJ_out_gggaga(T51, T48, T33, T73, T68, T35)
plusF_in_gga(0, T83) → U6_gga(T83, natD_in_g(T83))
plusF_in_gga(s(T90), T91) → U7_gga(T90, T91, plusF_in_gga(T90, T91))
U6_gga(T83, natD_out_g(T83)) → plusF_out_gga(0, T83, T83)
U7_gga(T90, T91, plusF_out_gga(T90, T91, T93)) → plusF_out_gga(s(T90), T91, s(T93))

The set Q consists of the following terms:

plusE_in_gag(x0, x1)
waysA_in_gga(x0, x1)
plusH_in_gag(x0, x1)
U4_gag(x0, x1)
U5_gag(x0, x1, x2)
U1_gga(x0, x1, x2, x3)
U2_gga(x0, x1, x2, x3)
U10_gag(x0, x1, x2)
natD_in_g(x0)
pB_in_gaggaaa(x0, x1, x2)
pC_in_gagga(x0, x1, x2)
plusG_in_gag(x0, x1)
U3_g(x0, x1)
U11_gaggaaa(x0, x1, x2, x3)
U17_gagga(x0, x1, x2, x3)
U8_gag(x0, x1)
U9_gag(x0, x1, x2)
U12_gaggaaa(x0, x1, x2, x3, x4)
U18_gagga(x0, x1, x2, x3, x4)
pI_in_ggaggaa(x0, x1, x2, x3)
U13_ggaggaa(x0, x1, x2, x3, x4)
U14_ggaggaa(x0, x1, x2, x3, x4, x5)
pJ_in_gggaga(x0, x1, x2, x3)
U15_gggaga(x0, x1, x2, x3, x4)
U16_gggaga(x0, x1, x2, x3, x4, x5)
plusF_in_gga(x0, x1)
U6_gga(x0, x1)
U7_gga(x0, x1, x2)

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

(46) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

PB_IN_GAGGAAA(T48, T49, T33) → U11_GAGGAAA(T48, T49, T33, plusE_in_gag(T48, T49))

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

POL(.(x₁, x₂)) = 0   
POL(0) = 0   
POL(PB_IN_GAGGAAA(x₁, x₂, x₃)) = 1 + x₂   
POL(PI_IN_GGAGGAA(x₁, x₂, x₃, x₄)) = x₃   
POL(PJ_IN_GGGAGA(x₁, x₂, x₃, x₄)) = x₁   
POL(U10_gag(x₁, x₂, x₃)) = 0   
POL(U11_GAGGAAA(x₁, x₂, x₃, x₄)) = x₄   
POL(U11_gaggaaa(x₁, x₂, x₃, x₄)) = 0   
POL(U12_gaggaaa(x₁, x₂, x₃, x₄, x₅)) = 0   
POL(U13_GGAGGAA(x₁, x₂, x₃, x₄, x₅)) = x₃   
POL(U13_ggaggaa(x₁, x₂, x₃, x₄, x₅)) = 0   
POL(U14_ggaggaa(x₁, x₂, x₃, x₄, x₅, x₆)) = 0   
POL(U15_gggaga(x₁, x₂, x₃, x₄, x₅)) = 0   
POL(U16_gggaga(x₁, x₂, x₃, x₄, x₅, x₆)) = 0   
POL(U17_gagga(x₁, x₂, x₃, x₄)) = 0   
POL(U18_gagga(x₁, x₂, x₃, x₄, x₅)) = 0   
POL(U1_gga(x₁, x₂, x₃, x₄)) = 0   
POL(U2_gga(x₁, x₂, x₃, x₄)) = 0   
POL(U3_g(x₁, x₂)) = 0   
POL(U4_gag(x₁, x₂)) = x₁   
POL(U5_gag(x₁, x₂, x₃)) = 1 + x₃   
POL(U6_gga(x₁, x₂)) = 0   
POL(U7_gga(x₁, x₂, x₃)) = 0   
POL(U8_gag(x₁, x₂)) = 0   
POL(U9_gag(x₁, x₂, x₃)) = 0   
POL(WAYSA_IN_GGA(x₁, x₂)) = x₁   
POL([]) = 0   
POL(natD_in_g(x₁)) = 0   
POL(natD_out_g(x₁)) = 0   
POL(pB_in_gaggaaa(x₁, x₂, x₃)) = 0   
POL(pB_out_gaggaaa(x₁, x₂, x₃, x₄, x₅, x₆, x₇)) = 0   
POL(pC_in_gagga(x₁, x₂, x₃)) = 0   
POL(pC_out_gagga(x₁, x₂, x₃, x₄, x₅)) = 0   
POL(pI_in_ggaggaa(x₁, x₂, x₃, x₄)) = 0   
POL(pI_out_ggaggaa(x₁, x₂, x₃, x₄, x₅, x₆, x₇)) = 0   
POL(pJ_in_gggaga(x₁, x₂, x₃, x₄)) = 0   
POL(pJ_out_gggaga(x₁, x₂, x₃, x₄, x₅, x₆)) = 0   
POL(plusE_in_gag(x₁, x₂)) = x₂   
POL(plusE_out_gag(x₁, x₂, x₃)) = x₂   
POL(plusF_in_gga(x₁, x₂)) = 0   
POL(plusF_out_gga(x₁, x₂, x₃)) = 0   
POL(plusG_in_gag(x₁, x₂)) = 0   
POL(plusG_out_gag(x₁, x₂, x₃)) = 0   
POL(plusH_in_gag(x₁, x₂)) = 0   
POL(plusH_out_gag(x₁, x₂, x₃)) = 0   
POL(s(x₁)) = 1 + x₁   
POL(waysA_in_gga(x₁, x₂)) = 0   
POL(waysA_out_gga(x₁, x₂, x₃)) = 0   

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

plusE_in_gag(0, T57) → U4_gag(T57, natD_in_g(T57))
plusE_in_gag(s(T65), s(T66)) → U5_gag(T65, T66, plusE_in_gag(T65, T66))
U5_gag(T65, T66, plusE_out_gag(T65, X119, T66)) → plusE_out_gag(s(T65), X119, s(T66))
U4_gag(T57, natD_out_g(T57)) → plusE_out_gag(0, T57, T57)

(47) Obligation:

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

U11_GAGGAAA(T48, T49, T33, plusE_out_gag(T48, T51, T49)) → PI_IN_GGAGGAA(T49, T33, T51, T48)
PI_IN_GGAGGAA(T49, T33, T51, T48) → U13_GGAGGAA(T49, T33, T51, T48, waysA_in_gga(s(T49), T33))
U13_GGAGGAA(T49, T33, T51, T48, waysA_out_gga(s(T49), T33, T68)) → PJ_IN_GGGAGA(T51, T48, T33, T68)
PJ_IN_GGGAGA(T51, T48, T33, T68) → WAYSA_IN_GGA(T51, .(s(T48), T33))
WAYSA_IN_GGA(s(T49), .(s(T48), T33)) → PB_IN_GAGGAAA(T48, T49, T33)

The TRS R consists of the following rules:

plusE_in_gag(0, T57) → U4_gag(T57, natD_in_g(T57))
plusE_in_gag(s(T65), s(T66)) → U5_gag(T65, T66, plusE_in_gag(T65, T66))
waysA_in_gga(T24, []) → waysA_out_gga(T24, [], 0)
waysA_in_gga(s(T49), .(s(T48), T33)) → U1_gga(T49, T48, T33, pB_in_gaggaaa(T48, T49, T33))
waysA_in_gga(s(T110), .(s(T105), T106)) → U2_gga(T110, T105, T106, pC_in_gagga(T110, T105, T106))
plusH_in_gag(T117, T118) → U10_gag(T117, T118, plusG_in_gag(T117, T118))
U4_gag(T57, natD_out_g(T57)) → plusE_out_gag(0, T57, T57)
U5_gag(T65, T66, plusE_out_gag(T65, X119, T66)) → plusE_out_gag(s(T65), X119, s(T66))
U1_gga(T49, T48, T33, pB_out_gaggaaa(T48, X90, T49, T33, X64, X65, T35)) → waysA_out_gga(s(T49), .(s(T48), T33), T35)
U2_gga(T110, T105, T106, pC_out_gagga(T110, X161, T105, T106, T108)) → waysA_out_gga(s(T110), .(s(T105), T106), T108)
U10_gag(T117, T118, plusG_out_gag(T117, X178, T118)) → plusH_out_gag(T117, X178, T118)
natD_in_g(0) → natD_out_g(0)
natD_in_g(s(T60)) → U3_g(T60, natD_in_g(T60))
pB_in_gaggaaa(T48, T49, T33) → U11_gaggaaa(T48, T49, T33, plusE_in_gag(T48, T49))
pC_in_gagga(T110, T105, T106) → U17_gagga(T110, T105, T106, plusH_in_gag(T110, T105))
plusG_in_gag(0, s(T124)) → U8_gag(T124, natD_in_g(s(T124)))
plusG_in_gag(s(T129), s(T130)) → U9_gag(T129, T130, plusG_in_gag(T129, T130))
U3_g(T60, natD_out_g(T60)) → natD_out_g(s(T60))
U11_gaggaaa(T48, T49, T33, plusE_out_gag(T48, T51, T49)) → U12_gaggaaa(T48, T51, T49, T33, pI_in_ggaggaa(T49, T33, T51, T48))
U17_gagga(T110, T105, T106, plusH_out_gag(T110, T111, T105)) → U18_gagga(T110, T111, T105, T106, waysA_in_gga(s(T110), T106))
U8_gag(T124, natD_out_g(s(T124))) → plusG_out_gag(0, T124, s(T124))
U9_gag(T129, T130, plusG_out_gag(T129, X202, T130)) → plusG_out_gag(s(T129), X202, s(T130))
U12_gaggaaa(T48, T51, T49, T33, pI_out_ggaggaa(T49, T33, X64, T51, T48, X65, T35)) → pB_out_gaggaaa(T48, T51, T49, T33, X64, X65, T35)
U18_gagga(T110, T111, T105, T106, waysA_out_gga(s(T110), T106, T108)) → pC_out_gagga(T110, T111, T105, T106, T108)
pI_in_ggaggaa(T49, T33, T51, T48) → U13_ggaggaa(T49, T33, T51, T48, waysA_in_gga(s(T49), T33))
U13_ggaggaa(T49, T33, T51, T48, waysA_out_gga(s(T49), T33, T68)) → U14_ggaggaa(T49, T33, T68, T51, T48, pJ_in_gggaga(T51, T48, T33, T68))
U14_ggaggaa(T49, T33, T68, T51, T48, pJ_out_gggaga(T51, T48, T33, X65, T68, T35)) → pI_out_ggaggaa(T49, T33, T68, T51, T48, X65, T35)
pJ_in_gggaga(T51, T48, T33, T68) → U15_gggaga(T51, T48, T33, T68, waysA_in_gga(T51, .(s(T48), T33)))
U15_gggaga(T51, T48, T33, T68, waysA_out_gga(T51, .(s(T48), T33), T73)) → U16_gggaga(T51, T48, T33, T73, T68, plusF_in_gga(T68, T73))
waysA_in_gga(0, T5) → waysA_out_gga(0, T5, s(0))
U16_gggaga(T51, T48, T33, T73, T68, plusF_out_gga(T68, T73, T35)) → pJ_out_gggaga(T51, T48, T33, T73, T68, T35)
plusF_in_gga(0, T83) → U6_gga(T83, natD_in_g(T83))
plusF_in_gga(s(T90), T91) → U7_gga(T90, T91, plusF_in_gga(T90, T91))
U6_gga(T83, natD_out_g(T83)) → plusF_out_gga(0, T83, T83)
U7_gga(T90, T91, plusF_out_gga(T90, T91, T93)) → plusF_out_gga(s(T90), T91, s(T93))

The set Q consists of the following terms:

plusE_in_gag(x0, x1)
waysA_in_gga(x0, x1)
plusH_in_gag(x0, x1)
U4_gag(x0, x1)
U5_gag(x0, x1, x2)
U1_gga(x0, x1, x2, x3)
U2_gga(x0, x1, x2, x3)
U10_gag(x0, x1, x2)
natD_in_g(x0)
pB_in_gaggaaa(x0, x1, x2)
pC_in_gagga(x0, x1, x2)
plusG_in_gag(x0, x1)
U3_g(x0, x1)
U11_gaggaaa(x0, x1, x2, x3)
U17_gagga(x0, x1, x2, x3)
U8_gag(x0, x1)
U9_gag(x0, x1, x2)
U12_gaggaaa(x0, x1, x2, x3, x4)
U18_gagga(x0, x1, x2, x3, x4)
pI_in_ggaggaa(x0, x1, x2, x3)
U13_ggaggaa(x0, x1, x2, x3, x4)
U14_ggaggaa(x0, x1, x2, x3, x4, x5)
pJ_in_gggaga(x0, x1, x2, x3)
U15_gggaga(x0, x1, x2, x3, x4)
U16_gggaga(x0, x1, x2, x3, x4, x5)
plusF_in_gga(x0, x1)
U6_gga(x0, x1)
U7_gga(x0, x1, x2)

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

(48) DependencyGraphProof (EQUIVALENT transformation)

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

(49) TRUE