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

(0) Obligation:

Clauses:

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

Query: mult(g,g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: mult(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: mult(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | mult(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: true | mult(T5, 0, T3), SCOPE: 1, CLAUSE: 1\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: mult(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground\nX3 is free\nmult(T1, T2, T3) !=? mult(X3, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: mult(T5, 0, T3), SCOPE: 1, CLAUSE: 1\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(mult(T10, T11, X13), sum(X13, T10, T13))\n\nT10 is ground\nT11 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: ','(mult(T10, T11, X13), sum(X13, T10, T13)), SCOPE: 2, CLAUSE: 0 | ','(mult(T10, T11, X13), sum(X13, T10, T13)), SCOPE: 2, CLAUSE: 1\n\nT10 is ground\nT11 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(mult(T10, T11, X13), sum(X13, T10, T13)), SCOPE: 2, CLAUSE: 0\n\nT10 is ground\nT11 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(mult(T10, T11, X13), sum(X13, T10, T13)), SCOPE: 2, CLAUSE: 1\n\nT10 is ground\nT11 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="B: sum(0, T18, T13)\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: sum(0, T18, T13), SCOPE: 3, CLAUSE: 2 | sum(0, T18, T13), SCOPE: 3, CLAUSE: 3\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: sum(0, T18, T13), SCOPE: 3, CLAUSE: 2\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: sum(0, T18, T13), SCOPE: 3, CLAUSE: 3\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: sum(0, T23, T25)\n\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="C: ','(','(mult(T30, T31, X49), sum(X49, T30, X50)), sum(X50, T30, T13))\n\nT30 is ground\nT31 is ground\nX50 is free\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="D: mult(T30, T31, X49)\n\nT30 is ground\nT31 is ground\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="H: ','(sum(T34, T30, X50), sum(X50, T30, T13))\n\nT30 is ground\nT34 is ground\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: mult(T30, T31, X49), SCOPE: 4, CLAUSE: 0 | mult(T30, T31, X49), SCOPE: 4, CLAUSE: 1\n\nT30 is ground\nT31 is ground\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: mult(T30, T31, X49), SCOPE: 4, CLAUSE: 0\n\nT30 is ground\nT31 is ground\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: mult(T30, T31, X49), SCOPE: 4, CLAUSE: 1\n\nT30 is ground\nT31 is ground\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="E: ','(mult(T46, T47, X72), sum(X72, T46, X73))\n\nT46 is ground\nT47 is ground\nX73 is free\nX72 is free", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: mult(T46, T47, X72)\n\nT46 is ground\nT47 is ground\nX72 is free", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="F: sum(T50, T46, X73)\n\nT46 is ground\nT50 is ground\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: sum(T50, T46, X73), SCOPE: 5, CLAUSE: 2 | sum(T50, T46, X73), SCOPE: 5, CLAUSE: 3\n\nT46 is ground\nT50 is ground\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: sum(T50, T46, X73), SCOPE: 5, CLAUSE: 2\n\nT46 is ground\nT50 is ground\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: sum(T50, T46, X73), SCOPE: 5, CLAUSE: 3\n\nT46 is ground\nT50 is ground\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: sum(T64, T65, X96)\n\nT64 is ground\nT65 is ground\nX96 is free", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: sum(T34, T30, X50)\n\nT30 is ground\nT34 is ground\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="G: sum(T70, T30, T13)\n\nT30 is ground\nT70 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: sum(T70, T30, T13), SCOPE: 6, CLAUSE: 2 | sum(T70, T30, T13), SCOPE: 6, CLAUSE: 3\n\nT30 is ground\nT70 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: sum(T70, T30, T13), SCOPE: 6, CLAUSE: 2\n\nT30 is ground\nT70 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: sum(T70, T30, T13), SCOPE: 6, CLAUSE: 3\n\nT30 is ground\nT70 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: sum(T86, T87, T89)\n\nT86 is ground\nT87 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 142 [arrowhead = none ];
142 -> 4;

143 [label="EVAL with clause\nmult(X3, 0, 0).\nand substitutionT1 -> T5,\nX3 -> T5,\nT2 -> 0,\nT3 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 143 [arrowhead = none ];
143 -> 10;

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

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

146 [label="EVAL with clause\nmult(X10, s(X11), X12) :- ','(mult(X10, X11, X13), sum(X13, X10, X12)).\nand substitutionT1 -> T10,\nX10 -> T10,\nX11 -> T11,\nT2 -> s(T11),\nT3 -> T13,\nX12 -> T13,\nT12 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 146 [arrowhead = none ];
146 -> 23;

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

148 [label="BACKTRACK\nfor clause: mult(X, s(Y), Z) :- ','(mult(X, Y, W), sum(W, X, Z))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 148 [arrowhead = none ];
148 -> 19;

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

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

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

152 [label="EVAL with clause\nmult(X18, 0, 0).\nand substitutionT10 -> T18,\nX18 -> T18,\nT11 -> 0,\nX13 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
29 -> 152 [arrowhead = none ];
152 -> 33;

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

154 [label="EVAL with clause\nmult(X46, s(X47), X48) :- ','(mult(X46, X47, X49), sum(X49, X46, X48)).\nand substitutionT10 -> T30,\nX46 -> T30,\nX47 -> T31,\nT11 -> s(T31),\nX13 -> X50,\nX48 -> X50", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 154 [arrowhead = none ];
154 -> 62;

155 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 155 [arrowhead = none ];
155 -> 64;

156 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
33 -> 156 [arrowhead = none ];
156 -> 37;

157 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
37 -> 157 [arrowhead = none ];
157 -> 40;

158 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
37 -> 158 [arrowhead = none ];
158 -> 41;

159 [label="EVAL with clause\nsum(X25, 0, X25).\nand substitutionX25 -> 0,\nT18 -> 0,\nT13 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 159 [arrowhead = none ];
159 -> 45;

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

161 [label="EVAL with clause\nsum(X32, s(X33), s(X34)) :- sum(X32, X33, X34).\nand substitutionX32 -> 0,\nX33 -> T23,\nT18 -> s(T23),\nX34 -> T25,\nT13 -> s(T25),\nT24 -> T25", fontsize=14, style = filled, fillcolor = lightblue];
41 -> 161 [arrowhead = none ];
161 -> 53;

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

163 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
45 -> 163 [arrowhead = none ];
163 -> 49;

164 [label="INSTANCE with matching:\nT18 -> T23\nT13 -> T25", fontsize=14, style = filled, fillcolor = lightgrey];
53 -> 164 [arrowhead = none , style=dashed];
164 -> 33[style=dashed];

165 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
62 -> 165 [arrowhead = none ];
165 -> 68;

166 [label="SPLIT 2\nnew knowledge:\nT30 is ground\nT31 is ground\nT34 is ground\nreplacements:X49 -> T34", fontsize=14, style = filled, fillcolor = violet];
62 -> 166 [arrowhead = none ];
166 -> 69;

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

168 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
69 -> 168 [arrowhead = none ];
168 -> 118;

169 [label="SPLIT 2\nnew knowledge:\nT34 is ground\nT30 is ground\nT70 is ground\nreplacements:X50 -> T70", fontsize=14, style = filled, fillcolor = violet];
69 -> 169 [arrowhead = none ];
169 -> 119;

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

171 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
73 -> 171 [arrowhead = none ];
171 -> 75;

172 [label="EVAL with clause\nmult(X59, 0, 0).\nand substitutionT30 -> T41,\nX59 -> T41,\nT31 -> 0,\nX49 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
74 -> 172 [arrowhead = none ];
172 -> 79;

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

174 [label="EVAL with clause\nmult(X69, s(X70), X71) :- ','(mult(X69, X70, X72), sum(X72, X69, X71)).\nand substitutionT30 -> T46,\nX69 -> T46,\nX70 -> T47,\nT31 -> s(T47),\nX49 -> X73,\nX71 -> X73", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 174 [arrowhead = none ];
174 -> 86;

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

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

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

178 [label="SPLIT 2\nnew knowledge:\nT46 is ground\nT47 is ground\nT50 is ground\nreplacements:X72 -> T50", fontsize=14, style = filled, fillcolor = violet];
86 -> 178 [arrowhead = none ];
178 -> 91;

179 [label="INSTANCE with matching:\nT30 -> T46\nT31 -> T47\nX49 -> X72", fontsize=14, style = filled, fillcolor = lightgrey];
90 -> 179 [arrowhead = none , style=dashed];
179 -> 68[style=dashed];

180 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
91 -> 180 [arrowhead = none ];
180 -> 98;

181 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
98 -> 181 [arrowhead = none ];
181 -> 102;

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

183 [label="EVAL with clause\nsum(X84, 0, X84).\nand substitutionT50 -> T59,\nX84 -> T59,\nT46 -> 0,\nX73 -> T59", fontsize=14, style = filled, fillcolor = lightblue];
102 -> 183 [arrowhead = none ];
183 -> 107;

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

185 [label="EVAL with clause\nsum(X93, s(X94), s(X95)) :- sum(X93, X94, X95).\nand substitutionT50 -> T64,\nX93 -> T64,\nX94 -> T65,\nT46 -> s(T65),\nX95 -> X96,\nX73 -> s(X96)", fontsize=14, style = filled, fillcolor = lightblue];
103 -> 185 [arrowhead = none ];
185 -> 114;

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

187 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
107 -> 187 [arrowhead = none ];
187 -> 109;

188 [label="INSTANCE with matching:\nT50 -> T64\nT46 -> T65\nX73 -> X96", fontsize=14, style = filled, fillcolor = lightgrey];
114 -> 188 [arrowhead = none , style=dashed];
188 -> 91[style=dashed];

189 [label="INSTANCE with matching:\nT50 -> T34\nT46 -> T30\nX73 -> X50", fontsize=14, style = filled, fillcolor = lightgrey];
118 -> 189 [arrowhead = none , style=dashed];
189 -> 91[style=dashed];

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

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

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

193 [label="EVAL with clause\nsum(X109, 0, X109).\nand substitutionT70 -> T79,\nX109 -> T79,\nT30 -> 0,\nT13 -> T79", fontsize=14, style = filled, fillcolor = lightblue];
127 -> 193 [arrowhead = none ];
193 -> 129;

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

195 [label="EVAL with clause\nsum(X116, s(X117), s(X118)) :- sum(X116, X117, X118).\nand substitutionT70 -> T86,\nX116 -> T86,\nX117 -> T87,\nT30 -> s(T87),\nX118 -> T89,\nT13 -> s(T89),\nT88 -> T89", fontsize=14, style = filled, fillcolor = lightblue];
128 -> 195 [arrowhead = none ];
195 -> 140;

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

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

198 [label="INSTANCE with matching:\nT70 -> T86\nT30 -> T87\nT13 -> T89", fontsize=14, style = filled, fillcolor = lightgrey];
140 -> 198 [arrowhead = none , style=dashed];
198 -> 119[style=dashed];

}

(2) Obligation:

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

multA_in_gga(T5, 0, 0) → multA_out_gga(T5, 0, 0)
multA_in_gga(T18, s(0), T13) → U1_gga(T18, T13, sumB_in_ga(T18, T13))
sumB_in_ga(0, 0) → sumB_out_ga(0, 0)
sumB_in_ga(s(T23), s(T25)) → U3_ga(T23, T25, sumB_in_ga(T23, T25))
U3_ga(T23, T25, sumB_out_ga(T23, T25)) → sumB_out_ga(s(T23), s(T25))
U1_gga(T18, T13, sumB_out_ga(T18, T13)) → multA_out_gga(T18, s(0), T13)
multA_in_gga(T30, s(s(T31)), T13) → U2_gga(T30, T31, T13, pC_in_ggaaa(T30, T31, X49, X50, T13))
pC_in_ggaaa(T30, T31, T34, X50, T13) → U7_ggaaa(T30, T31, T34, X50, T13, multD_in_gga(T30, T31, T34))
multD_in_gga(T41, 0, 0) → multD_out_gga(T41, 0, 0)
multD_in_gga(T46, s(T47), X73) → U4_gga(T46, T47, X73, pE_in_ggaa(T46, T47, X72, X73))
pE_in_ggaa(T46, T47, T50, X73) → U11_ggaa(T46, T47, T50, X73, multD_in_gga(T46, T47, T50))
U11_ggaa(T46, T47, T50, X73, multD_out_gga(T46, T47, T50)) → U12_ggaa(T46, T47, T50, X73, sumF_in_gga(T50, T46, X73))
sumF_in_gga(T59, 0, T59) → sumF_out_gga(T59, 0, T59)
sumF_in_gga(T64, s(T65), s(X96)) → U5_gga(T64, T65, X96, sumF_in_gga(T64, T65, X96))
U5_gga(T64, T65, X96, sumF_out_gga(T64, T65, X96)) → sumF_out_gga(T64, s(T65), s(X96))
U12_ggaa(T46, T47, T50, X73, sumF_out_gga(T50, T46, X73)) → pE_out_ggaa(T46, T47, T50, X73)
U4_gga(T46, T47, X73, pE_out_ggaa(T46, T47, X72, X73)) → multD_out_gga(T46, s(T47), X73)
U7_ggaaa(T30, T31, T34, X50, T13, multD_out_gga(T30, T31, T34)) → U8_ggaaa(T30, T31, T34, X50, T13, pH_in_ggaa(T34, T30, X50, T13))
pH_in_ggaa(T34, T30, T70, T13) → U9_ggaa(T34, T30, T70, T13, sumF_in_gga(T34, T30, T70))
U9_ggaa(T34, T30, T70, T13, sumF_out_gga(T34, T30, T70)) → U10_ggaa(T34, T30, T70, T13, sumG_in_gga(T70, T30, T13))
sumG_in_gga(T79, 0, T79) → sumG_out_gga(T79, 0, T79)
sumG_in_gga(T86, s(T87), s(T89)) → U6_gga(T86, T87, T89, sumG_in_gga(T86, T87, T89))
U6_gga(T86, T87, T89, sumG_out_gga(T86, T87, T89)) → sumG_out_gga(T86, s(T87), s(T89))
U10_ggaa(T34, T30, T70, T13, sumG_out_gga(T70, T30, T13)) → pH_out_ggaa(T34, T30, T70, T13)
U8_ggaaa(T30, T31, T34, X50, T13, pH_out_ggaa(T34, T30, X50, T13)) → pC_out_ggaaa(T30, T31, T34, X50, T13)
U2_gga(T30, T31, T13, pC_out_ggaaa(T30, T31, X49, X50, T13)) → multA_out_gga(T30, s(s(T31)), T13)

The argument filtering Pi contains the following mapping:
multA_in_gga(x1, x2, x3)  =  multA_in_gga(x1, x2)
0  =  0
multA_out_gga(x1, x2, x3)  =  multA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
sumB_in_ga(x1, x2)  =  sumB_in_ga(x1)
sumB_out_ga(x1, x2)  =  sumB_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
pC_in_ggaaa(x1, x2, x3, x4, x5)  =  pC_in_ggaaa(x1, x2)
U7_ggaaa(x1, x2, x3, x4, x5, x6)  =  U7_ggaaa(x1, x2, x6)
multD_in_gga(x1, x2, x3)  =  multD_in_gga(x1, x2)
multD_out_gga(x1, x2, x3)  =  multD_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
pE_in_ggaa(x1, x2, x3, x4)  =  pE_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
sumF_in_gga(x1, x2, x3)  =  sumF_in_gga(x1, x2)
sumF_out_gga(x1, x2, x3)  =  sumF_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pE_out_ggaa(x1, x2, x3, x4)  =  pE_out_ggaa(x1, x2, x3, x4)
U8_ggaaa(x1, x2, x3, x4, x5, x6)  =  U8_ggaaa(x1, x2, x3, x6)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_in_ggaa(x1, x2)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x1, x2, x5)
U10_ggaa(x1, x2, x3, x4, x5)  =  U10_ggaa(x1, x2, x3, x5)
sumG_in_gga(x1, x2, x3)  =  sumG_in_gga(x1, x2)
sumG_out_gga(x1, x2, x3)  =  sumG_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
pH_out_ggaa(x1, x2, x3, x4)  =  pH_out_ggaa(x1, x2, x3, x4)
pC_out_ggaaa(x1, x2, x3, x4, x5)  =  pC_out_ggaaa(x1, x2, x3, x4, x5)

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

MULTA_IN_GGA(T18, s(0), T13) → U1_GGA(T18, T13, sumB_in_ga(T18, T13))
MULTA_IN_GGA(T18, s(0), T13) → SUMB_IN_GA(T18, T13)
SUMB_IN_GA(s(T23), s(T25)) → U3_GA(T23, T25, sumB_in_ga(T23, T25))
SUMB_IN_GA(s(T23), s(T25)) → SUMB_IN_GA(T23, T25)
MULTA_IN_GGA(T30, s(s(T31)), T13) → U2_GGA(T30, T31, T13, pC_in_ggaaa(T30, T31, X49, X50, T13))
MULTA_IN_GGA(T30, s(s(T31)), T13) → PC_IN_GGAAA(T30, T31, X49, X50, T13)
PC_IN_GGAAA(T30, T31, T34, X50, T13) → U7_GGAAA(T30, T31, T34, X50, T13, multD_in_gga(T30, T31, T34))
PC_IN_GGAAA(T30, T31, T34, X50, T13) → MULTD_IN_GGA(T30, T31, T34)
MULTD_IN_GGA(T46, s(T47), X73) → U4_GGA(T46, T47, X73, pE_in_ggaa(T46, T47, X72, X73))
MULTD_IN_GGA(T46, s(T47), X73) → PE_IN_GGAA(T46, T47, X72, X73)
PE_IN_GGAA(T46, T47, T50, X73) → U11_GGAA(T46, T47, T50, X73, multD_in_gga(T46, T47, T50))
PE_IN_GGAA(T46, T47, T50, X73) → MULTD_IN_GGA(T46, T47, T50)
U11_GGAA(T46, T47, T50, X73, multD_out_gga(T46, T47, T50)) → U12_GGAA(T46, T47, T50, X73, sumF_in_gga(T50, T46, X73))
U11_GGAA(T46, T47, T50, X73, multD_out_gga(T46, T47, T50)) → SUMF_IN_GGA(T50, T46, X73)
SUMF_IN_GGA(T64, s(T65), s(X96)) → U5_GGA(T64, T65, X96, sumF_in_gga(T64, T65, X96))
SUMF_IN_GGA(T64, s(T65), s(X96)) → SUMF_IN_GGA(T64, T65, X96)
U7_GGAAA(T30, T31, T34, X50, T13, multD_out_gga(T30, T31, T34)) → U8_GGAAA(T30, T31, T34, X50, T13, pH_in_ggaa(T34, T30, X50, T13))
U7_GGAAA(T30, T31, T34, X50, T13, multD_out_gga(T30, T31, T34)) → PH_IN_GGAA(T34, T30, X50, T13)
PH_IN_GGAA(T34, T30, T70, T13) → U9_GGAA(T34, T30, T70, T13, sumF_in_gga(T34, T30, T70))
PH_IN_GGAA(T34, T30, T70, T13) → SUMF_IN_GGA(T34, T30, T70)
U9_GGAA(T34, T30, T70, T13, sumF_out_gga(T34, T30, T70)) → U10_GGAA(T34, T30, T70, T13, sumG_in_gga(T70, T30, T13))
U9_GGAA(T34, T30, T70, T13, sumF_out_gga(T34, T30, T70)) → SUMG_IN_GGA(T70, T30, T13)
SUMG_IN_GGA(T86, s(T87), s(T89)) → U6_GGA(T86, T87, T89, sumG_in_gga(T86, T87, T89))
SUMG_IN_GGA(T86, s(T87), s(T89)) → SUMG_IN_GGA(T86, T87, T89)

The TRS R consists of the following rules:

multA_in_gga(T5, 0, 0) → multA_out_gga(T5, 0, 0)
multA_in_gga(T18, s(0), T13) → U1_gga(T18, T13, sumB_in_ga(T18, T13))
sumB_in_ga(0, 0) → sumB_out_ga(0, 0)
sumB_in_ga(s(T23), s(T25)) → U3_ga(T23, T25, sumB_in_ga(T23, T25))
U3_ga(T23, T25, sumB_out_ga(T23, T25)) → sumB_out_ga(s(T23), s(T25))
U1_gga(T18, T13, sumB_out_ga(T18, T13)) → multA_out_gga(T18, s(0), T13)
multA_in_gga(T30, s(s(T31)), T13) → U2_gga(T30, T31, T13, pC_in_ggaaa(T30, T31, X49, X50, T13))
pC_in_ggaaa(T30, T31, T34, X50, T13) → U7_ggaaa(T30, T31, T34, X50, T13, multD_in_gga(T30, T31, T34))
multD_in_gga(T41, 0, 0) → multD_out_gga(T41, 0, 0)
multD_in_gga(T46, s(T47), X73) → U4_gga(T46, T47, X73, pE_in_ggaa(T46, T47, X72, X73))
pE_in_ggaa(T46, T47, T50, X73) → U11_ggaa(T46, T47, T50, X73, multD_in_gga(T46, T47, T50))
U11_ggaa(T46, T47, T50, X73, multD_out_gga(T46, T47, T50)) → U12_ggaa(T46, T47, T50, X73, sumF_in_gga(T50, T46, X73))
sumF_in_gga(T59, 0, T59) → sumF_out_gga(T59, 0, T59)
sumF_in_gga(T64, s(T65), s(X96)) → U5_gga(T64, T65, X96, sumF_in_gga(T64, T65, X96))
U5_gga(T64, T65, X96, sumF_out_gga(T64, T65, X96)) → sumF_out_gga(T64, s(T65), s(X96))
U12_ggaa(T46, T47, T50, X73, sumF_out_gga(T50, T46, X73)) → pE_out_ggaa(T46, T47, T50, X73)
U4_gga(T46, T47, X73, pE_out_ggaa(T46, T47, X72, X73)) → multD_out_gga(T46, s(T47), X73)
U7_ggaaa(T30, T31, T34, X50, T13, multD_out_gga(T30, T31, T34)) → U8_ggaaa(T30, T31, T34, X50, T13, pH_in_ggaa(T34, T30, X50, T13))
pH_in_ggaa(T34, T30, T70, T13) → U9_ggaa(T34, T30, T70, T13, sumF_in_gga(T34, T30, T70))
U9_ggaa(T34, T30, T70, T13, sumF_out_gga(T34, T30, T70)) → U10_ggaa(T34, T30, T70, T13, sumG_in_gga(T70, T30, T13))
sumG_in_gga(T79, 0, T79) → sumG_out_gga(T79, 0, T79)
sumG_in_gga(T86, s(T87), s(T89)) → U6_gga(T86, T87, T89, sumG_in_gga(T86, T87, T89))
U6_gga(T86, T87, T89, sumG_out_gga(T86, T87, T89)) → sumG_out_gga(T86, s(T87), s(T89))
U10_ggaa(T34, T30, T70, T13, sumG_out_gga(T70, T30, T13)) → pH_out_ggaa(T34, T30, T70, T13)
U8_ggaaa(T30, T31, T34, X50, T13, pH_out_ggaa(T34, T30, X50, T13)) → pC_out_ggaaa(T30, T31, T34, X50, T13)
U2_gga(T30, T31, T13, pC_out_ggaaa(T30, T31, X49, X50, T13)) → multA_out_gga(T30, s(s(T31)), T13)

The argument filtering Pi contains the following mapping:
multA_in_gga(x1, x2, x3)  =  multA_in_gga(x1, x2)
0  =  0
multA_out_gga(x1, x2, x3)  =  multA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
sumB_in_ga(x1, x2)  =  sumB_in_ga(x1)
sumB_out_ga(x1, x2)  =  sumB_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
pC_in_ggaaa(x1, x2, x3, x4, x5)  =  pC_in_ggaaa(x1, x2)
U7_ggaaa(x1, x2, x3, x4, x5, x6)  =  U7_ggaaa(x1, x2, x6)
multD_in_gga(x1, x2, x3)  =  multD_in_gga(x1, x2)
multD_out_gga(x1, x2, x3)  =  multD_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
pE_in_ggaa(x1, x2, x3, x4)  =  pE_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
sumF_in_gga(x1, x2, x3)  =  sumF_in_gga(x1, x2)
sumF_out_gga(x1, x2, x3)  =  sumF_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pE_out_ggaa(x1, x2, x3, x4)  =  pE_out_ggaa(x1, x2, x3, x4)
U8_ggaaa(x1, x2, x3, x4, x5, x6)  =  U8_ggaaa(x1, x2, x3, x6)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_in_ggaa(x1, x2)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x1, x2, x5)
U10_ggaa(x1, x2, x3, x4, x5)  =  U10_ggaa(x1, x2, x3, x5)
sumG_in_gga(x1, x2, x3)  =  sumG_in_gga(x1, x2)
sumG_out_gga(x1, x2, x3)  =  sumG_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
pH_out_ggaa(x1, x2, x3, x4)  =  pH_out_ggaa(x1, x2, x3, x4)
pC_out_ggaaa(x1, x2, x3, x4, x5)  =  pC_out_ggaaa(x1, x2, x3, x4, x5)
MULTA_IN_GGA(x1, x2, x3)  =  MULTA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3)  =  U1_GGA(x1, x3)
SUMB_IN_GA(x1, x2)  =  SUMB_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)
PC_IN_GGAAA(x1, x2, x3, x4, x5)  =  PC_IN_GGAAA(x1, x2)
U7_GGAAA(x1, x2, x3, x4, x5, x6)  =  U7_GGAAA(x1, x2, x6)
MULTD_IN_GGA(x1, x2, x3)  =  MULTD_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
PE_IN_GGAA(x1, x2, x3, x4)  =  PE_IN_GGAA(x1, x2)
U11_GGAA(x1, x2, x3, x4, x5)  =  U11_GGAA(x1, x2, x5)
U12_GGAA(x1, x2, x3, x4, x5)  =  U12_GGAA(x1, x2, x3, x5)
SUMF_IN_GGA(x1, x2, x3)  =  SUMF_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
U8_GGAAA(x1, x2, x3, x4, x5, x6)  =  U8_GGAAA(x1, x2, x3, x6)
PH_IN_GGAA(x1, x2, x3, x4)  =  PH_IN_GGAA(x1, x2)
U9_GGAA(x1, x2, x3, x4, x5)  =  U9_GGAA(x1, x2, x5)
U10_GGAA(x1, x2, x3, x4, x5)  =  U10_GGAA(x1, x2, x3, x5)
SUMG_IN_GGA(x1, x2, x3)  =  SUMG_IN_GGA(x1, x2)
U6_GGA(x1, x2, x3, x4)  =  U6_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:

MULTA_IN_GGA(T18, s(0), T13) → U1_GGA(T18, T13, sumB_in_ga(T18, T13))
MULTA_IN_GGA(T18, s(0), T13) → SUMB_IN_GA(T18, T13)
SUMB_IN_GA(s(T23), s(T25)) → U3_GA(T23, T25, sumB_in_ga(T23, T25))
SUMB_IN_GA(s(T23), s(T25)) → SUMB_IN_GA(T23, T25)
MULTA_IN_GGA(T30, s(s(T31)), T13) → U2_GGA(T30, T31, T13, pC_in_ggaaa(T30, T31, X49, X50, T13))
MULTA_IN_GGA(T30, s(s(T31)), T13) → PC_IN_GGAAA(T30, T31, X49, X50, T13)
PC_IN_GGAAA(T30, T31, T34, X50, T13) → U7_GGAAA(T30, T31, T34, X50, T13, multD_in_gga(T30, T31, T34))
PC_IN_GGAAA(T30, T31, T34, X50, T13) → MULTD_IN_GGA(T30, T31, T34)
MULTD_IN_GGA(T46, s(T47), X73) → U4_GGA(T46, T47, X73, pE_in_ggaa(T46, T47, X72, X73))
MULTD_IN_GGA(T46, s(T47), X73) → PE_IN_GGAA(T46, T47, X72, X73)
PE_IN_GGAA(T46, T47, T50, X73) → U11_GGAA(T46, T47, T50, X73, multD_in_gga(T46, T47, T50))
PE_IN_GGAA(T46, T47, T50, X73) → MULTD_IN_GGA(T46, T47, T50)
U11_GGAA(T46, T47, T50, X73, multD_out_gga(T46, T47, T50)) → U12_GGAA(T46, T47, T50, X73, sumF_in_gga(T50, T46, X73))
U11_GGAA(T46, T47, T50, X73, multD_out_gga(T46, T47, T50)) → SUMF_IN_GGA(T50, T46, X73)
SUMF_IN_GGA(T64, s(T65), s(X96)) → U5_GGA(T64, T65, X96, sumF_in_gga(T64, T65, X96))
SUMF_IN_GGA(T64, s(T65), s(X96)) → SUMF_IN_GGA(T64, T65, X96)
U7_GGAAA(T30, T31, T34, X50, T13, multD_out_gga(T30, T31, T34)) → U8_GGAAA(T30, T31, T34, X50, T13, pH_in_ggaa(T34, T30, X50, T13))
U7_GGAAA(T30, T31, T34, X50, T13, multD_out_gga(T30, T31, T34)) → PH_IN_GGAA(T34, T30, X50, T13)
PH_IN_GGAA(T34, T30, T70, T13) → U9_GGAA(T34, T30, T70, T13, sumF_in_gga(T34, T30, T70))
PH_IN_GGAA(T34, T30, T70, T13) → SUMF_IN_GGA(T34, T30, T70)
U9_GGAA(T34, T30, T70, T13, sumF_out_gga(T34, T30, T70)) → U10_GGAA(T34, T30, T70, T13, sumG_in_gga(T70, T30, T13))
U9_GGAA(T34, T30, T70, T13, sumF_out_gga(T34, T30, T70)) → SUMG_IN_GGA(T70, T30, T13)
SUMG_IN_GGA(T86, s(T87), s(T89)) → U6_GGA(T86, T87, T89, sumG_in_gga(T86, T87, T89))
SUMG_IN_GGA(T86, s(T87), s(T89)) → SUMG_IN_GGA(T86, T87, T89)

The TRS R consists of the following rules:

multA_in_gga(T5, 0, 0) → multA_out_gga(T5, 0, 0)
multA_in_gga(T18, s(0), T13) → U1_gga(T18, T13, sumB_in_ga(T18, T13))
sumB_in_ga(0, 0) → sumB_out_ga(0, 0)
sumB_in_ga(s(T23), s(T25)) → U3_ga(T23, T25, sumB_in_ga(T23, T25))
U3_ga(T23, T25, sumB_out_ga(T23, T25)) → sumB_out_ga(s(T23), s(T25))
U1_gga(T18, T13, sumB_out_ga(T18, T13)) → multA_out_gga(T18, s(0), T13)
multA_in_gga(T30, s(s(T31)), T13) → U2_gga(T30, T31, T13, pC_in_ggaaa(T30, T31, X49, X50, T13))
pC_in_ggaaa(T30, T31, T34, X50, T13) → U7_ggaaa(T30, T31, T34, X50, T13, multD_in_gga(T30, T31, T34))
multD_in_gga(T41, 0, 0) → multD_out_gga(T41, 0, 0)
multD_in_gga(T46, s(T47), X73) → U4_gga(T46, T47, X73, pE_in_ggaa(T46, T47, X72, X73))
pE_in_ggaa(T46, T47, T50, X73) → U11_ggaa(T46, T47, T50, X73, multD_in_gga(T46, T47, T50))
U11_ggaa(T46, T47, T50, X73, multD_out_gga(T46, T47, T50)) → U12_ggaa(T46, T47, T50, X73, sumF_in_gga(T50, T46, X73))
sumF_in_gga(T59, 0, T59) → sumF_out_gga(T59, 0, T59)
sumF_in_gga(T64, s(T65), s(X96)) → U5_gga(T64, T65, X96, sumF_in_gga(T64, T65, X96))
U5_gga(T64, T65, X96, sumF_out_gga(T64, T65, X96)) → sumF_out_gga(T64, s(T65), s(X96))
U12_ggaa(T46, T47, T50, X73, sumF_out_gga(T50, T46, X73)) → pE_out_ggaa(T46, T47, T50, X73)
U4_gga(T46, T47, X73, pE_out_ggaa(T46, T47, X72, X73)) → multD_out_gga(T46, s(T47), X73)
U7_ggaaa(T30, T31, T34, X50, T13, multD_out_gga(T30, T31, T34)) → U8_ggaaa(T30, T31, T34, X50, T13, pH_in_ggaa(T34, T30, X50, T13))
pH_in_ggaa(T34, T30, T70, T13) → U9_ggaa(T34, T30, T70, T13, sumF_in_gga(T34, T30, T70))
U9_ggaa(T34, T30, T70, T13, sumF_out_gga(T34, T30, T70)) → U10_ggaa(T34, T30, T70, T13, sumG_in_gga(T70, T30, T13))
sumG_in_gga(T79, 0, T79) → sumG_out_gga(T79, 0, T79)
sumG_in_gga(T86, s(T87), s(T89)) → U6_gga(T86, T87, T89, sumG_in_gga(T86, T87, T89))
U6_gga(T86, T87, T89, sumG_out_gga(T86, T87, T89)) → sumG_out_gga(T86, s(T87), s(T89))
U10_ggaa(T34, T30, T70, T13, sumG_out_gga(T70, T30, T13)) → pH_out_ggaa(T34, T30, T70, T13)
U8_ggaaa(T30, T31, T34, X50, T13, pH_out_ggaa(T34, T30, X50, T13)) → pC_out_ggaaa(T30, T31, T34, X50, T13)
U2_gga(T30, T31, T13, pC_out_ggaaa(T30, T31, X49, X50, T13)) → multA_out_gga(T30, s(s(T31)), T13)

The argument filtering Pi contains the following mapping:
multA_in_gga(x1, x2, x3)  =  multA_in_gga(x1, x2)
0  =  0
multA_out_gga(x1, x2, x3)  =  multA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
sumB_in_ga(x1, x2)  =  sumB_in_ga(x1)
sumB_out_ga(x1, x2)  =  sumB_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
pC_in_ggaaa(x1, x2, x3, x4, x5)  =  pC_in_ggaaa(x1, x2)
U7_ggaaa(x1, x2, x3, x4, x5, x6)  =  U7_ggaaa(x1, x2, x6)
multD_in_gga(x1, x2, x3)  =  multD_in_gga(x1, x2)
multD_out_gga(x1, x2, x3)  =  multD_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
pE_in_ggaa(x1, x2, x3, x4)  =  pE_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
sumF_in_gga(x1, x2, x3)  =  sumF_in_gga(x1, x2)
sumF_out_gga(x1, x2, x3)  =  sumF_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pE_out_ggaa(x1, x2, x3, x4)  =  pE_out_ggaa(x1, x2, x3, x4)
U8_ggaaa(x1, x2, x3, x4, x5, x6)  =  U8_ggaaa(x1, x2, x3, x6)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_in_ggaa(x1, x2)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x1, x2, x5)
U10_ggaa(x1, x2, x3, x4, x5)  =  U10_ggaa(x1, x2, x3, x5)
sumG_in_gga(x1, x2, x3)  =  sumG_in_gga(x1, x2)
sumG_out_gga(x1, x2, x3)  =  sumG_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
pH_out_ggaa(x1, x2, x3, x4)  =  pH_out_ggaa(x1, x2, x3, x4)
pC_out_ggaaa(x1, x2, x3, x4, x5)  =  pC_out_ggaaa(x1, x2, x3, x4, x5)
MULTA_IN_GGA(x1, x2, x3)  =  MULTA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3)  =  U1_GGA(x1, x3)
SUMB_IN_GA(x1, x2)  =  SUMB_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)
PC_IN_GGAAA(x1, x2, x3, x4, x5)  =  PC_IN_GGAAA(x1, x2)
U7_GGAAA(x1, x2, x3, x4, x5, x6)  =  U7_GGAAA(x1, x2, x6)
MULTD_IN_GGA(x1, x2, x3)  =  MULTD_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
PE_IN_GGAA(x1, x2, x3, x4)  =  PE_IN_GGAA(x1, x2)
U11_GGAA(x1, x2, x3, x4, x5)  =  U11_GGAA(x1, x2, x5)
U12_GGAA(x1, x2, x3, x4, x5)  =  U12_GGAA(x1, x2, x3, x5)
SUMF_IN_GGA(x1, x2, x3)  =  SUMF_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
U8_GGAAA(x1, x2, x3, x4, x5, x6)  =  U8_GGAAA(x1, x2, x3, x6)
PH_IN_GGAA(x1, x2, x3, x4)  =  PH_IN_GGAA(x1, x2)
U9_GGAA(x1, x2, x3, x4, x5)  =  U9_GGAA(x1, x2, x5)
U10_GGAA(x1, x2, x3, x4, x5)  =  U10_GGAA(x1, x2, x3, x5)
SUMG_IN_GGA(x1, x2, x3)  =  SUMG_IN_GGA(x1, x2)
U6_GGA(x1, x2, x3, x4)  =  U6_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 4 SCCs with 19 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

SUMG_IN_GGA(T86, s(T87), s(T89)) → SUMG_IN_GGA(T86, T87, T89)

The TRS R consists of the following rules:

multA_in_gga(T5, 0, 0) → multA_out_gga(T5, 0, 0)
multA_in_gga(T18, s(0), T13) → U1_gga(T18, T13, sumB_in_ga(T18, T13))
sumB_in_ga(0, 0) → sumB_out_ga(0, 0)
sumB_in_ga(s(T23), s(T25)) → U3_ga(T23, T25, sumB_in_ga(T23, T25))
U3_ga(T23, T25, sumB_out_ga(T23, T25)) → sumB_out_ga(s(T23), s(T25))
U1_gga(T18, T13, sumB_out_ga(T18, T13)) → multA_out_gga(T18, s(0), T13)
multA_in_gga(T30, s(s(T31)), T13) → U2_gga(T30, T31, T13, pC_in_ggaaa(T30, T31, X49, X50, T13))
pC_in_ggaaa(T30, T31, T34, X50, T13) → U7_ggaaa(T30, T31, T34, X50, T13, multD_in_gga(T30, T31, T34))
multD_in_gga(T41, 0, 0) → multD_out_gga(T41, 0, 0)
multD_in_gga(T46, s(T47), X73) → U4_gga(T46, T47, X73, pE_in_ggaa(T46, T47, X72, X73))
pE_in_ggaa(T46, T47, T50, X73) → U11_ggaa(T46, T47, T50, X73, multD_in_gga(T46, T47, T50))
U11_ggaa(T46, T47, T50, X73, multD_out_gga(T46, T47, T50)) → U12_ggaa(T46, T47, T50, X73, sumF_in_gga(T50, T46, X73))
sumF_in_gga(T59, 0, T59) → sumF_out_gga(T59, 0, T59)
sumF_in_gga(T64, s(T65), s(X96)) → U5_gga(T64, T65, X96, sumF_in_gga(T64, T65, X96))
U5_gga(T64, T65, X96, sumF_out_gga(T64, T65, X96)) → sumF_out_gga(T64, s(T65), s(X96))
U12_ggaa(T46, T47, T50, X73, sumF_out_gga(T50, T46, X73)) → pE_out_ggaa(T46, T47, T50, X73)
U4_gga(T46, T47, X73, pE_out_ggaa(T46, T47, X72, X73)) → multD_out_gga(T46, s(T47), X73)
U7_ggaaa(T30, T31, T34, X50, T13, multD_out_gga(T30, T31, T34)) → U8_ggaaa(T30, T31, T34, X50, T13, pH_in_ggaa(T34, T30, X50, T13))
pH_in_ggaa(T34, T30, T70, T13) → U9_ggaa(T34, T30, T70, T13, sumF_in_gga(T34, T30, T70))
U9_ggaa(T34, T30, T70, T13, sumF_out_gga(T34, T30, T70)) → U10_ggaa(T34, T30, T70, T13, sumG_in_gga(T70, T30, T13))
sumG_in_gga(T79, 0, T79) → sumG_out_gga(T79, 0, T79)
sumG_in_gga(T86, s(T87), s(T89)) → U6_gga(T86, T87, T89, sumG_in_gga(T86, T87, T89))
U6_gga(T86, T87, T89, sumG_out_gga(T86, T87, T89)) → sumG_out_gga(T86, s(T87), s(T89))
U10_ggaa(T34, T30, T70, T13, sumG_out_gga(T70, T30, T13)) → pH_out_ggaa(T34, T30, T70, T13)
U8_ggaaa(T30, T31, T34, X50, T13, pH_out_ggaa(T34, T30, X50, T13)) → pC_out_ggaaa(T30, T31, T34, X50, T13)
U2_gga(T30, T31, T13, pC_out_ggaaa(T30, T31, X49, X50, T13)) → multA_out_gga(T30, s(s(T31)), T13)

The argument filtering Pi contains the following mapping:
multA_in_gga(x1, x2, x3)  =  multA_in_gga(x1, x2)
0  =  0
multA_out_gga(x1, x2, x3)  =  multA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
sumB_in_ga(x1, x2)  =  sumB_in_ga(x1)
sumB_out_ga(x1, x2)  =  sumB_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
pC_in_ggaaa(x1, x2, x3, x4, x5)  =  pC_in_ggaaa(x1, x2)
U7_ggaaa(x1, x2, x3, x4, x5, x6)  =  U7_ggaaa(x1, x2, x6)
multD_in_gga(x1, x2, x3)  =  multD_in_gga(x1, x2)
multD_out_gga(x1, x2, x3)  =  multD_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
pE_in_ggaa(x1, x2, x3, x4)  =  pE_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
sumF_in_gga(x1, x2, x3)  =  sumF_in_gga(x1, x2)
sumF_out_gga(x1, x2, x3)  =  sumF_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pE_out_ggaa(x1, x2, x3, x4)  =  pE_out_ggaa(x1, x2, x3, x4)
U8_ggaaa(x1, x2, x3, x4, x5, x6)  =  U8_ggaaa(x1, x2, x3, x6)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_in_ggaa(x1, x2)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x1, x2, x5)
U10_ggaa(x1, x2, x3, x4, x5)  =  U10_ggaa(x1, x2, x3, x5)
sumG_in_gga(x1, x2, x3)  =  sumG_in_gga(x1, x2)
sumG_out_gga(x1, x2, x3)  =  sumG_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
pH_out_ggaa(x1, x2, x3, x4)  =  pH_out_ggaa(x1, x2, x3, x4)
pC_out_ggaaa(x1, x2, x3, x4, x5)  =  pC_out_ggaaa(x1, x2, x3, x4, x5)
SUMG_IN_GGA(x1, x2, x3)  =  SUMG_IN_GGA(x1, x2)

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:

SUMG_IN_GGA(T86, s(T87), s(T89)) → SUMG_IN_GGA(T86, T87, T89)

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

SUMG_IN_GGA(T86, s(T87)) → SUMG_IN_GGA(T86, T87)

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:

• SUMG_IN_GGA(T86, s(T87)) → SUMG_IN_GGA(T86, T87)
  The graph contains the following edges 1 >= 1, 2 > 2

(13) YES

(14) Obligation:

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

SUMF_IN_GGA(T64, s(T65), s(X96)) → SUMF_IN_GGA(T64, T65, X96)

The TRS R consists of the following rules:

multA_in_gga(T5, 0, 0) → multA_out_gga(T5, 0, 0)
multA_in_gga(T18, s(0), T13) → U1_gga(T18, T13, sumB_in_ga(T18, T13))
sumB_in_ga(0, 0) → sumB_out_ga(0, 0)
sumB_in_ga(s(T23), s(T25)) → U3_ga(T23, T25, sumB_in_ga(T23, T25))
U3_ga(T23, T25, sumB_out_ga(T23, T25)) → sumB_out_ga(s(T23), s(T25))
U1_gga(T18, T13, sumB_out_ga(T18, T13)) → multA_out_gga(T18, s(0), T13)
multA_in_gga(T30, s(s(T31)), T13) → U2_gga(T30, T31, T13, pC_in_ggaaa(T30, T31, X49, X50, T13))
pC_in_ggaaa(T30, T31, T34, X50, T13) → U7_ggaaa(T30, T31, T34, X50, T13, multD_in_gga(T30, T31, T34))
multD_in_gga(T41, 0, 0) → multD_out_gga(T41, 0, 0)
multD_in_gga(T46, s(T47), X73) → U4_gga(T46, T47, X73, pE_in_ggaa(T46, T47, X72, X73))
pE_in_ggaa(T46, T47, T50, X73) → U11_ggaa(T46, T47, T50, X73, multD_in_gga(T46, T47, T50))
U11_ggaa(T46, T47, T50, X73, multD_out_gga(T46, T47, T50)) → U12_ggaa(T46, T47, T50, X73, sumF_in_gga(T50, T46, X73))
sumF_in_gga(T59, 0, T59) → sumF_out_gga(T59, 0, T59)
sumF_in_gga(T64, s(T65), s(X96)) → U5_gga(T64, T65, X96, sumF_in_gga(T64, T65, X96))
U5_gga(T64, T65, X96, sumF_out_gga(T64, T65, X96)) → sumF_out_gga(T64, s(T65), s(X96))
U12_ggaa(T46, T47, T50, X73, sumF_out_gga(T50, T46, X73)) → pE_out_ggaa(T46, T47, T50, X73)
U4_gga(T46, T47, X73, pE_out_ggaa(T46, T47, X72, X73)) → multD_out_gga(T46, s(T47), X73)
U7_ggaaa(T30, T31, T34, X50, T13, multD_out_gga(T30, T31, T34)) → U8_ggaaa(T30, T31, T34, X50, T13, pH_in_ggaa(T34, T30, X50, T13))
pH_in_ggaa(T34, T30, T70, T13) → U9_ggaa(T34, T30, T70, T13, sumF_in_gga(T34, T30, T70))
U9_ggaa(T34, T30, T70, T13, sumF_out_gga(T34, T30, T70)) → U10_ggaa(T34, T30, T70, T13, sumG_in_gga(T70, T30, T13))
sumG_in_gga(T79, 0, T79) → sumG_out_gga(T79, 0, T79)
sumG_in_gga(T86, s(T87), s(T89)) → U6_gga(T86, T87, T89, sumG_in_gga(T86, T87, T89))
U6_gga(T86, T87, T89, sumG_out_gga(T86, T87, T89)) → sumG_out_gga(T86, s(T87), s(T89))
U10_ggaa(T34, T30, T70, T13, sumG_out_gga(T70, T30, T13)) → pH_out_ggaa(T34, T30, T70, T13)
U8_ggaaa(T30, T31, T34, X50, T13, pH_out_ggaa(T34, T30, X50, T13)) → pC_out_ggaaa(T30, T31, T34, X50, T13)
U2_gga(T30, T31, T13, pC_out_ggaaa(T30, T31, X49, X50, T13)) → multA_out_gga(T30, s(s(T31)), T13)

The argument filtering Pi contains the following mapping:
multA_in_gga(x1, x2, x3)  =  multA_in_gga(x1, x2)
0  =  0
multA_out_gga(x1, x2, x3)  =  multA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
sumB_in_ga(x1, x2)  =  sumB_in_ga(x1)
sumB_out_ga(x1, x2)  =  sumB_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
pC_in_ggaaa(x1, x2, x3, x4, x5)  =  pC_in_ggaaa(x1, x2)
U7_ggaaa(x1, x2, x3, x4, x5, x6)  =  U7_ggaaa(x1, x2, x6)
multD_in_gga(x1, x2, x3)  =  multD_in_gga(x1, x2)
multD_out_gga(x1, x2, x3)  =  multD_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
pE_in_ggaa(x1, x2, x3, x4)  =  pE_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
sumF_in_gga(x1, x2, x3)  =  sumF_in_gga(x1, x2)
sumF_out_gga(x1, x2, x3)  =  sumF_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pE_out_ggaa(x1, x2, x3, x4)  =  pE_out_ggaa(x1, x2, x3, x4)
U8_ggaaa(x1, x2, x3, x4, x5, x6)  =  U8_ggaaa(x1, x2, x3, x6)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_in_ggaa(x1, x2)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x1, x2, x5)
U10_ggaa(x1, x2, x3, x4, x5)  =  U10_ggaa(x1, x2, x3, x5)
sumG_in_gga(x1, x2, x3)  =  sumG_in_gga(x1, x2)
sumG_out_gga(x1, x2, x3)  =  sumG_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
pH_out_ggaa(x1, x2, x3, x4)  =  pH_out_ggaa(x1, x2, x3, x4)
pC_out_ggaaa(x1, x2, x3, x4, x5)  =  pC_out_ggaaa(x1, x2, x3, x4, x5)
SUMF_IN_GGA(x1, x2, x3)  =  SUMF_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:

SUMF_IN_GGA(T64, s(T65), s(X96)) → SUMF_IN_GGA(T64, T65, X96)

R is empty.
The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
SUMF_IN_GGA(x1, x2, x3)  =  SUMF_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:

SUMF_IN_GGA(T64, s(T65)) → SUMF_IN_GGA(T64, T65)

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:

• SUMF_IN_GGA(T64, s(T65)) → SUMF_IN_GGA(T64, T65)
  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:

MULTD_IN_GGA(T46, s(T47), X73) → PE_IN_GGAA(T46, T47, X72, X73)
PE_IN_GGAA(T46, T47, T50, X73) → MULTD_IN_GGA(T46, T47, T50)

The TRS R consists of the following rules:

multA_in_gga(T5, 0, 0) → multA_out_gga(T5, 0, 0)
multA_in_gga(T18, s(0), T13) → U1_gga(T18, T13, sumB_in_ga(T18, T13))
sumB_in_ga(0, 0) → sumB_out_ga(0, 0)
sumB_in_ga(s(T23), s(T25)) → U3_ga(T23, T25, sumB_in_ga(T23, T25))
U3_ga(T23, T25, sumB_out_ga(T23, T25)) → sumB_out_ga(s(T23), s(T25))
U1_gga(T18, T13, sumB_out_ga(T18, T13)) → multA_out_gga(T18, s(0), T13)
multA_in_gga(T30, s(s(T31)), T13) → U2_gga(T30, T31, T13, pC_in_ggaaa(T30, T31, X49, X50, T13))
pC_in_ggaaa(T30, T31, T34, X50, T13) → U7_ggaaa(T30, T31, T34, X50, T13, multD_in_gga(T30, T31, T34))
multD_in_gga(T41, 0, 0) → multD_out_gga(T41, 0, 0)
multD_in_gga(T46, s(T47), X73) → U4_gga(T46, T47, X73, pE_in_ggaa(T46, T47, X72, X73))
pE_in_ggaa(T46, T47, T50, X73) → U11_ggaa(T46, T47, T50, X73, multD_in_gga(T46, T47, T50))
U11_ggaa(T46, T47, T50, X73, multD_out_gga(T46, T47, T50)) → U12_ggaa(T46, T47, T50, X73, sumF_in_gga(T50, T46, X73))
sumF_in_gga(T59, 0, T59) → sumF_out_gga(T59, 0, T59)
sumF_in_gga(T64, s(T65), s(X96)) → U5_gga(T64, T65, X96, sumF_in_gga(T64, T65, X96))
U5_gga(T64, T65, X96, sumF_out_gga(T64, T65, X96)) → sumF_out_gga(T64, s(T65), s(X96))
U12_ggaa(T46, T47, T50, X73, sumF_out_gga(T50, T46, X73)) → pE_out_ggaa(T46, T47, T50, X73)
U4_gga(T46, T47, X73, pE_out_ggaa(T46, T47, X72, X73)) → multD_out_gga(T46, s(T47), X73)
U7_ggaaa(T30, T31, T34, X50, T13, multD_out_gga(T30, T31, T34)) → U8_ggaaa(T30, T31, T34, X50, T13, pH_in_ggaa(T34, T30, X50, T13))
pH_in_ggaa(T34, T30, T70, T13) → U9_ggaa(T34, T30, T70, T13, sumF_in_gga(T34, T30, T70))
U9_ggaa(T34, T30, T70, T13, sumF_out_gga(T34, T30, T70)) → U10_ggaa(T34, T30, T70, T13, sumG_in_gga(T70, T30, T13))
sumG_in_gga(T79, 0, T79) → sumG_out_gga(T79, 0, T79)
sumG_in_gga(T86, s(T87), s(T89)) → U6_gga(T86, T87, T89, sumG_in_gga(T86, T87, T89))
U6_gga(T86, T87, T89, sumG_out_gga(T86, T87, T89)) → sumG_out_gga(T86, s(T87), s(T89))
U10_ggaa(T34, T30, T70, T13, sumG_out_gga(T70, T30, T13)) → pH_out_ggaa(T34, T30, T70, T13)
U8_ggaaa(T30, T31, T34, X50, T13, pH_out_ggaa(T34, T30, X50, T13)) → pC_out_ggaaa(T30, T31, T34, X50, T13)
U2_gga(T30, T31, T13, pC_out_ggaaa(T30, T31, X49, X50, T13)) → multA_out_gga(T30, s(s(T31)), T13)

The argument filtering Pi contains the following mapping:
multA_in_gga(x1, x2, x3)  =  multA_in_gga(x1, x2)
0  =  0
multA_out_gga(x1, x2, x3)  =  multA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
sumB_in_ga(x1, x2)  =  sumB_in_ga(x1)
sumB_out_ga(x1, x2)  =  sumB_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
pC_in_ggaaa(x1, x2, x3, x4, x5)  =  pC_in_ggaaa(x1, x2)
U7_ggaaa(x1, x2, x3, x4, x5, x6)  =  U7_ggaaa(x1, x2, x6)
multD_in_gga(x1, x2, x3)  =  multD_in_gga(x1, x2)
multD_out_gga(x1, x2, x3)  =  multD_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
pE_in_ggaa(x1, x2, x3, x4)  =  pE_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
sumF_in_gga(x1, x2, x3)  =  sumF_in_gga(x1, x2)
sumF_out_gga(x1, x2, x3)  =  sumF_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pE_out_ggaa(x1, x2, x3, x4)  =  pE_out_ggaa(x1, x2, x3, x4)
U8_ggaaa(x1, x2, x3, x4, x5, x6)  =  U8_ggaaa(x1, x2, x3, x6)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_in_ggaa(x1, x2)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x1, x2, x5)
U10_ggaa(x1, x2, x3, x4, x5)  =  U10_ggaa(x1, x2, x3, x5)
sumG_in_gga(x1, x2, x3)  =  sumG_in_gga(x1, x2)
sumG_out_gga(x1, x2, x3)  =  sumG_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
pH_out_ggaa(x1, x2, x3, x4)  =  pH_out_ggaa(x1, x2, x3, x4)
pC_out_ggaaa(x1, x2, x3, x4, x5)  =  pC_out_ggaaa(x1, x2, x3, x4, x5)
MULTD_IN_GGA(x1, x2, x3)  =  MULTD_IN_GGA(x1, x2)
PE_IN_GGAA(x1, x2, x3, x4)  =  PE_IN_GGAA(x1, x2)

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:

MULTD_IN_GGA(T46, s(T47), X73) → PE_IN_GGAA(T46, T47, X72, X73)
PE_IN_GGAA(T46, T47, T50, X73) → MULTD_IN_GGA(T46, T47, T50)

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

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:

MULTD_IN_GGA(T46, s(T47)) → PE_IN_GGAA(T46, T47)
PE_IN_GGAA(T46, T47) → MULTD_IN_GGA(T46, T47)

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:

• PE_IN_GGAA(T46, T47) → MULTD_IN_GGA(T46, T47)
  The graph contains the following edges 1 >= 1, 2 >= 2

• MULTD_IN_GGA(T46, s(T47)) → PE_IN_GGAA(T46, T47)
  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:

SUMB_IN_GA(s(T23), s(T25)) → SUMB_IN_GA(T23, T25)

The TRS R consists of the following rules:

multA_in_gga(T5, 0, 0) → multA_out_gga(T5, 0, 0)
multA_in_gga(T18, s(0), T13) → U1_gga(T18, T13, sumB_in_ga(T18, T13))
sumB_in_ga(0, 0) → sumB_out_ga(0, 0)
sumB_in_ga(s(T23), s(T25)) → U3_ga(T23, T25, sumB_in_ga(T23, T25))
U3_ga(T23, T25, sumB_out_ga(T23, T25)) → sumB_out_ga(s(T23), s(T25))
U1_gga(T18, T13, sumB_out_ga(T18, T13)) → multA_out_gga(T18, s(0), T13)
multA_in_gga(T30, s(s(T31)), T13) → U2_gga(T30, T31, T13, pC_in_ggaaa(T30, T31, X49, X50, T13))
pC_in_ggaaa(T30, T31, T34, X50, T13) → U7_ggaaa(T30, T31, T34, X50, T13, multD_in_gga(T30, T31, T34))
multD_in_gga(T41, 0, 0) → multD_out_gga(T41, 0, 0)
multD_in_gga(T46, s(T47), X73) → U4_gga(T46, T47, X73, pE_in_ggaa(T46, T47, X72, X73))
pE_in_ggaa(T46, T47, T50, X73) → U11_ggaa(T46, T47, T50, X73, multD_in_gga(T46, T47, T50))
U11_ggaa(T46, T47, T50, X73, multD_out_gga(T46, T47, T50)) → U12_ggaa(T46, T47, T50, X73, sumF_in_gga(T50, T46, X73))
sumF_in_gga(T59, 0, T59) → sumF_out_gga(T59, 0, T59)
sumF_in_gga(T64, s(T65), s(X96)) → U5_gga(T64, T65, X96, sumF_in_gga(T64, T65, X96))
U5_gga(T64, T65, X96, sumF_out_gga(T64, T65, X96)) → sumF_out_gga(T64, s(T65), s(X96))
U12_ggaa(T46, T47, T50, X73, sumF_out_gga(T50, T46, X73)) → pE_out_ggaa(T46, T47, T50, X73)
U4_gga(T46, T47, X73, pE_out_ggaa(T46, T47, X72, X73)) → multD_out_gga(T46, s(T47), X73)
U7_ggaaa(T30, T31, T34, X50, T13, multD_out_gga(T30, T31, T34)) → U8_ggaaa(T30, T31, T34, X50, T13, pH_in_ggaa(T34, T30, X50, T13))
pH_in_ggaa(T34, T30, T70, T13) → U9_ggaa(T34, T30, T70, T13, sumF_in_gga(T34, T30, T70))
U9_ggaa(T34, T30, T70, T13, sumF_out_gga(T34, T30, T70)) → U10_ggaa(T34, T30, T70, T13, sumG_in_gga(T70, T30, T13))
sumG_in_gga(T79, 0, T79) → sumG_out_gga(T79, 0, T79)
sumG_in_gga(T86, s(T87), s(T89)) → U6_gga(T86, T87, T89, sumG_in_gga(T86, T87, T89))
U6_gga(T86, T87, T89, sumG_out_gga(T86, T87, T89)) → sumG_out_gga(T86, s(T87), s(T89))
U10_ggaa(T34, T30, T70, T13, sumG_out_gga(T70, T30, T13)) → pH_out_ggaa(T34, T30, T70, T13)
U8_ggaaa(T30, T31, T34, X50, T13, pH_out_ggaa(T34, T30, X50, T13)) → pC_out_ggaaa(T30, T31, T34, X50, T13)
U2_gga(T30, T31, T13, pC_out_ggaaa(T30, T31, X49, X50, T13)) → multA_out_gga(T30, s(s(T31)), T13)

The argument filtering Pi contains the following mapping:
multA_in_gga(x1, x2, x3)  =  multA_in_gga(x1, x2)
0  =  0
multA_out_gga(x1, x2, x3)  =  multA_out_gga(x1, x2, x3)
s(x1)  =  s(x1)
U1_gga(x1, x2, x3)  =  U1_gga(x1, x3)
sumB_in_ga(x1, x2)  =  sumB_in_ga(x1)
sumB_out_ga(x1, x2)  =  sumB_out_ga(x1, x2)
U3_ga(x1, x2, x3)  =  U3_ga(x1, x3)
U2_gga(x1, x2, x3, x4)  =  U2_gga(x1, x2, x4)
pC_in_ggaaa(x1, x2, x3, x4, x5)  =  pC_in_ggaaa(x1, x2)
U7_ggaaa(x1, x2, x3, x4, x5, x6)  =  U7_ggaaa(x1, x2, x6)
multD_in_gga(x1, x2, x3)  =  multD_in_gga(x1, x2)
multD_out_gga(x1, x2, x3)  =  multD_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x1, x2, x4)
pE_in_ggaa(x1, x2, x3, x4)  =  pE_in_ggaa(x1, x2)
U11_ggaa(x1, x2, x3, x4, x5)  =  U11_ggaa(x1, x2, x5)
U12_ggaa(x1, x2, x3, x4, x5)  =  U12_ggaa(x1, x2, x3, x5)
sumF_in_gga(x1, x2, x3)  =  sumF_in_gga(x1, x2)
sumF_out_gga(x1, x2, x3)  =  sumF_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4)  =  U5_gga(x1, x2, x4)
pE_out_ggaa(x1, x2, x3, x4)  =  pE_out_ggaa(x1, x2, x3, x4)
U8_ggaaa(x1, x2, x3, x4, x5, x6)  =  U8_ggaaa(x1, x2, x3, x6)
pH_in_ggaa(x1, x2, x3, x4)  =  pH_in_ggaa(x1, x2)
U9_ggaa(x1, x2, x3, x4, x5)  =  U9_ggaa(x1, x2, x5)
U10_ggaa(x1, x2, x3, x4, x5)  =  U10_ggaa(x1, x2, x3, x5)
sumG_in_gga(x1, x2, x3)  =  sumG_in_gga(x1, x2)
sumG_out_gga(x1, x2, x3)  =  sumG_out_gga(x1, x2, x3)
U6_gga(x1, x2, x3, x4)  =  U6_gga(x1, x2, x4)
pH_out_ggaa(x1, x2, x3, x4)  =  pH_out_ggaa(x1, x2, x3, x4)
pC_out_ggaaa(x1, x2, x3, x4, x5)  =  pC_out_ggaaa(x1, x2, x3, x4, x5)
SUMB_IN_GA(x1, x2)  =  SUMB_IN_GA(x1)

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:

SUMB_IN_GA(s(T23), s(T25)) → SUMB_IN_GA(T23, T25)

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

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:

SUMB_IN_GA(s(T23)) → SUMB_IN_GA(T23)

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:

• SUMB_IN_GA(s(T23)) → SUMB_IN_GA(T23)
  The graph contains the following edges 1 > 1

(34) YES