Left Termination of the query pattern mult_in_3(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).

Queries:

mult(g,g,a).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: mult(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: 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];
3 [label="3: true | mult(T5, 0, T3), SCOPE: 1, CLAUSE: 1\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: mult(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground\nmult(T1, T2, T3) !=? mult(X3, 0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: mult(T5, 0, T3), SCOPE: 1, CLAUSE: 1\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(mult(T10, T11, X14), sum(X14, T10, T13))\n\nT10 is ground\nT11 is ground\nX14 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: ','(mult(T10, T11, X14), sum(X14, T10, T13)), SCOPE: 2, CLAUSE: 0 | ','(mult(T10, T11, X14), sum(X14, T10, T13)), SCOPE: 2, CLAUSE: 1\n\nT10 is ground\nT11 is ground\nX14 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(mult(T10, T11, X14), sum(X14, T10, T13)), SCOPE: 2, CLAUSE: 0\n\nT10 is ground\nT11 is ground\nX14 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(mult(T10, T11, X14), sum(X14, T10, T13)), SCOPE: 2, CLAUSE: 1\n\nT10 is ground\nT11 is ground\nX14 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: sum(0, T18, T13)\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: 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];
15 [label="15: sum(0, T18, T13), SCOPE: 3, CLAUSE: 2\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: sum(0, T18, T13), SCOPE: 3, CLAUSE: 3\n\nT18 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: sum(0, T23, T25)\n\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(mult(T30, T31, X58), ','(sum(X58, T30, X59), sum(X59, T30, T13)))\n\nT30 is ground\nT31 is ground\nX59 is free; \nX58 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: mult(T30, T31, X58)\n\nT30 is ground\nT31 is ground\nX58 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(sum(T34, T30, X59), sum(X59, T30, T13))\n\nT30 is ground\nT34 is ground\nX59 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: mult(T30, T31, X58), SCOPE: 4, CLAUSE: 0 | mult(T30, T31, X58), SCOPE: 4, CLAUSE: 1\n\nT30 is ground\nT31 is ground\nX58 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: mult(T30, T31, X58), SCOPE: 4, CLAUSE: 0\n\nT30 is ground\nT31 is ground\nX58 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: mult(T30, T31, X58), SCOPE: 4, CLAUSE: 1\n\nT30 is ground\nT31 is ground\nX58 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(mult(T46, T47, X85), sum(X85, T46, X86))\n\nT46 is ground\nT47 is ground\nX86 is free; \nX85 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: mult(T46, T47, X85)\n\nT46 is ground\nT47 is ground\nX85 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: sum(T50, T46, X86)\n\nT46 is ground\nT50 is ground\nX86 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: sum(T50, T46, X86), SCOPE: 5, CLAUSE: 2 | sum(T50, T46, X86), SCOPE: 5, CLAUSE: 3\n\nT46 is ground\nT50 is ground\nX86 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: sum(T50, T46, X86), SCOPE: 5, CLAUSE: 2\n\nT46 is ground\nT50 is ground\nX86 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: sum(T50, T46, X86), SCOPE: 5, CLAUSE: 3\n\nT46 is ground\nT50 is ground\nX86 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: sum(T64, T65, X113)\n\nT64 is ground\nT65 is ground\nX113 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: sum(T34, T30, X59)\n\nT30 is ground\nT34 is ground\nX59 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: sum(T70, T30, T13)\n\nT30 is ground\nT70 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: 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];
47 [label="47: sum(T70, T30, T13), SCOPE: 6, CLAUSE: 2\n\nT30 is ground\nT70 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: sum(T70, T30, T13), SCOPE: 6, CLAUSE: 3\n\nT30 is ground\nT70 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: sum(T86, T87, T89)\n\nT86 is ground\nT87 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 54 [arrowhead = none ];
54 -> 2;

55 [label="EVAL with clause\nmult(X3, 0, 0).\nand substitution\nT1 -> T5\nX3 -> T5\nT2 -> 0\nT3 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 55 [arrowhead = none ];
55 -> 3;

56 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 56 [arrowhead = none ];
56 -> 4;

57 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 57 [arrowhead = none ];
57 -> 5;

58 [label="EVAL with clause\nmult(X11, s(X12), X13) :- ','(mult(X11, X12, X14), sum(X14, X11, X13)).\nand substitution\nT1 -> T10\nX11 -> T10\nX12 -> T11\nT2 -> s(T11)\nT3 -> T13\nX13 -> T13\nT12 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 58 [arrowhead = none ];
58 -> 7;

59 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 59 [arrowhead = none ];
59 -> 8;

60 [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 = white];
5 -> 60 [arrowhead = none ];
60 -> 6;

61 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
7 -> 61 [arrowhead = none ];
61 -> 9;

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

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

64 [label="EVAL with clause\nmult(X22, 0, 0).\nand substitution\nT10 -> T18\nX22 -> T18\nT11 -> 0\nX14 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 64 [arrowhead = none ];
64 -> 12;

65 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 65 [arrowhead = none ];
65 -> 13;

66 [label="EVAL with clause\nmult(X55, s(X56), X57) :- ','(mult(X55, X56, X58), sum(X58, X55, X57)).\nand substitution\nT10 -> T30\nX55 -> T30\nX56 -> T31\nT11 -> s(T31)\nX14 -> X59\nX57 -> X59", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 66 [arrowhead = none ];
66 -> 22;

67 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 67 [arrowhead = none ];
67 -> 23;

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

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

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

71 [label="EVAL with clause\nsum(X30, 0, X30).\nand substitution\nX30 -> 0\nT18 -> 0\nT13 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 71 [arrowhead = none ];
71 -> 17;

72 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 72 [arrowhead = none ];
72 -> 18;

73 [label="EVAL with clause\nsum(X38, s(X39), s(X40)) :- sum(X38, X39, X40).\nand substitution\nX38 -> 0\nX39 -> T23\nT18 -> s(T23)\nX40 -> T25\nT13 -> s(T25)\nT24 -> T25", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 73 [arrowhead = none ];
73 -> 20;

74 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 74 [arrowhead = none ];
74 -> 21;

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

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

77 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
22 -> 77 [arrowhead = none ];
77 -> 24;

78 [label="SPLIT 2\nnew knowledge:\nT34 is ground\nreplacements:\nX58 -> T34", fontsize=14, style = filled, fillcolor = violet];
22 -> 78 [arrowhead = none ];
78 -> 25;

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

80 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
25 -> 80 [arrowhead = none ];
80 -> 44;

81 [label="SPLIT 2\nnew knowledge:\nT70 is ground\nreplacements:\nX59 -> T70", fontsize=14, style = filled, fillcolor = violet];
25 -> 81 [arrowhead = none ];
81 -> 45;

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

83 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
26 -> 83 [arrowhead = none ];
83 -> 28;

84 [label="EVAL with clause\nmult(X71, 0, 0).\nand substitution\nT30 -> T41\nX71 -> T41\nT31 -> 0\nX58 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
27 -> 84 [arrowhead = none ];
84 -> 29;

85 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
27 -> 85 [arrowhead = none ];
85 -> 30;

86 [label="EVAL with clause\nmult(X82, s(X83), X84) :- ','(mult(X82, X83, X85), sum(X85, X82, X84)).\nand substitution\nT30 -> T46\nX82 -> T46\nX83 -> T47\nT31 -> s(T47)\nX58 -> X86\nX84 -> X86", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 86 [arrowhead = none ];
86 -> 32;

87 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 87 [arrowhead = none ];
87 -> 33;

88 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
29 -> 88 [arrowhead = none ];
88 -> 31;

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

90 [label="SPLIT 2\nnew knowledge:\nT50 is ground\nreplacements:\nX85 -> T50", fontsize=14, style = filled, fillcolor = violet];
32 -> 90 [arrowhead = none ];
90 -> 35;

91 [label="INSTANCE with matching:\nT30 -> T46\nT31 -> T47\nX58 -> X85", fontsize=14, style = filled, fillcolor = lightgrey];
34 -> 91 [arrowhead = none , style=dashed];
91 -> 24[style=dashed];

92 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
35 -> 92 [arrowhead = none ];
92 -> 36;

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

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

95 [label="EVAL with clause\nsum(X100, 0, X100).\nand substitution\nT50 -> T59\nX100 -> T59\nT46 -> 0\nX86 -> T59", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 95 [arrowhead = none ];
95 -> 39;

96 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 96 [arrowhead = none ];
96 -> 40;

97 [label="EVAL with clause\nsum(X110, s(X111), s(X112)) :- sum(X110, X111, X112).\nand substitution\nT50 -> T64\nX110 -> T64\nX111 -> T65\nT46 -> s(T65)\nX112 -> X113\nX86 -> s(X113)", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 97 [arrowhead = none ];
97 -> 42;

98 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 98 [arrowhead = none ];
98 -> 43;

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

100 [label="INSTANCE with matching:\nT50 -> T64\nT46 -> T65\nX86 -> X113", fontsize=14, style = filled, fillcolor = lightgrey];
42 -> 100 [arrowhead = none , style=dashed];
100 -> 35[style=dashed];

101 [label="INSTANCE with matching:\nT50 -> T34\nT46 -> T30\nX86 -> X59", fontsize=14, style = filled, fillcolor = lightgrey];
44 -> 101 [arrowhead = none , style=dashed];
101 -> 35[style=dashed];

102 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
45 -> 102 [arrowhead = none ];
102 -> 46;

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

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

105 [label="EVAL with clause\nsum(X129, 0, X129).\nand substitution\nT70 -> T79\nX129 -> T79\nT30 -> 0\nT13 -> T79", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 105 [arrowhead = none ];
105 -> 49;

106 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 106 [arrowhead = none ];
106 -> 50;

107 [label="EVAL with clause\nsum(X137, s(X138), s(X139)) :- sum(X137, X138, X139).\nand substitution\nT70 -> T86\nX137 -> T86\nX138 -> T87\nT30 -> s(T87)\nX139 -> T89\nT13 -> s(T89)\nT88 -> T89", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 107 [arrowhead = none ];
107 -> 52;

108 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 108 [arrowhead = none ];
108 -> 53;

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

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

}

(2) Obligation:

Clauses:

sum12(0, 0).
sum12(s(T23), s(T25)) :- sum12(T23, T25).
mult24(T41, 0, 0).
mult24(T46, s(T47), X86) :- mult24(T46, T47, X85).
mult24(T46, s(T47), X86) :- ','(mult24(T46, T47, T50), sum35(T50, T46, X86)).
sum35(T59, 0, T59).
sum35(T64, s(T65), s(X113)) :- sum35(T64, T65, X113).
sum45(T79, 0, T79).
sum45(T86, s(T87), s(T89)) :- sum45(T86, T87, T89).
mult1(T5, 0, 0).
mult1(T18, s(0), T13) :- sum12(T18, T13).
mult1(T30, s(s(T31)), T13) :- mult24(T30, T31, X58).
mult1(T30, s(s(T31)), T13) :- ','(mult24(T30, T31, T34), sum35(T34, T30, X59)).
mult1(T30, s(s(T31)), T13) :- ','(mult24(T30, T31, T34), ','(sum35(T34, T30, T70), sum45(T70, T30, T13))).

Queries:

mult1(g,g,a).

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
mult1_in: (b,b,f)
sum12_in: (b,f)
mult24_in: (b,b,f)
sum35_in: (f,b,f)
sum45_in: (f,b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

mult1_in_gga(T5, 0, 0) → mult1_out_gga(T5, 0, 0)
mult1_in_gga(T18, s(0), T13) → U7_gga(T18, T13, sum12_in_ga(T18, T13))
sum12_in_ga(0, 0) → sum12_out_ga(0, 0)
sum12_in_ga(s(T23), s(T25)) → U1_ga(T23, T25, sum12_in_ga(T23, T25))
U1_ga(T23, T25, sum12_out_ga(T23, T25)) → sum12_out_ga(s(T23), s(T25))
U7_gga(T18, T13, sum12_out_ga(T18, T13)) → mult1_out_gga(T18, s(0), T13)
mult1_in_gga(T30, s(s(T31)), T13) → U8_gga(T30, T31, T13, mult24_in_gga(T30, T31, X58))
mult24_in_gga(T41, 0, 0) → mult24_out_gga(T41, 0, 0)
mult24_in_gga(T46, s(T47), X86) → U2_gga(T46, T47, X86, mult24_in_gga(T46, T47, X85))
mult24_in_gga(T46, s(T47), X86) → U3_gga(T46, T47, X86, mult24_in_gga(T46, T47, T50))
U3_gga(T46, T47, X86, mult24_out_gga(T46, T47, T50)) → U4_gga(T46, T47, X86, sum35_in_aga(T50, T46, X86))
sum35_in_aga(T59, 0, T59) → sum35_out_aga(T59, 0, T59)
sum35_in_aga(T64, s(T65), s(X113)) → U5_aga(T64, T65, X113, sum35_in_aga(T64, T65, X113))
U5_aga(T64, T65, X113, sum35_out_aga(T64, T65, X113)) → sum35_out_aga(T64, s(T65), s(X113))
U4_gga(T46, T47, X86, sum35_out_aga(T50, T46, X86)) → mult24_out_gga(T46, s(T47), X86)
U2_gga(T46, T47, X86, mult24_out_gga(T46, T47, X85)) → mult24_out_gga(T46, s(T47), X86)
U8_gga(T30, T31, T13, mult24_out_gga(T30, T31, X58)) → mult1_out_gga(T30, s(s(T31)), T13)
mult1_in_gga(T30, s(s(T31)), T13) → U9_gga(T30, T31, T13, mult24_in_gga(T30, T31, T34))
U9_gga(T30, T31, T13, mult24_out_gga(T30, T31, T34)) → U10_gga(T30, T31, T13, sum35_in_aga(T34, T30, X59))
U10_gga(T30, T31, T13, sum35_out_aga(T34, T30, X59)) → mult1_out_gga(T30, s(s(T31)), T13)
U9_gga(T30, T31, T13, mult24_out_gga(T30, T31, T34)) → U11_gga(T30, T31, T13, sum35_in_aga(T34, T30, T70))
U11_gga(T30, T31, T13, sum35_out_aga(T34, T30, T70)) → U12_gga(T30, T31, T13, sum45_in_aga(T70, T30, T13))
sum45_in_aga(T79, 0, T79) → sum45_out_aga(T79, 0, T79)
sum45_in_aga(T86, s(T87), s(T89)) → U6_aga(T86, T87, T89, sum45_in_aga(T86, T87, T89))
U6_aga(T86, T87, T89, sum45_out_aga(T86, T87, T89)) → sum45_out_aga(T86, s(T87), s(T89))
U12_gga(T30, T31, T13, sum45_out_aga(T70, T30, T13)) → mult1_out_gga(T30, s(s(T31)), T13)

The argument filtering Pi contains the following mapping:
mult1_in_gga(x1, x2, x3)  =  mult1_in_gga(x1, x2)
0  =  0
mult1_out_gga(x1, x2, x3)  =  mult1_out_gga
s(x1)  =  s(x1)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
sum12_in_ga(x1, x2)  =  sum12_in_ga(x1)
sum12_out_ga(x1, x2)  =  sum12_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x4)
mult24_in_gga(x1, x2, x3)  =  mult24_in_gga(x1, x2)
mult24_out_gga(x1, x2, x3)  =  mult24_out_gga
U2_gga(x1, x2, x3, x4)  =  U2_gga(x4)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x4)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x4)
sum35_in_aga(x1, x2, x3)  =  sum35_in_aga(x2)
sum35_out_aga(x1, x2, x3)  =  sum35_out_aga
U5_aga(x1, x2, x3, x4)  =  U5_aga(x4)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x4)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
sum45_in_aga(x1, x2, x3)  =  sum45_in_aga(x2)
sum45_out_aga(x1, x2, x3)  =  sum45_out_aga
U6_aga(x1, x2, x3, x4)  =  U6_aga(x4)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

mult1_in_gga(T5, 0, 0) → mult1_out_gga(T5, 0, 0)
mult1_in_gga(T18, s(0), T13) → U7_gga(T18, T13, sum12_in_ga(T18, T13))
sum12_in_ga(0, 0) → sum12_out_ga(0, 0)
sum12_in_ga(s(T23), s(T25)) → U1_ga(T23, T25, sum12_in_ga(T23, T25))
U1_ga(T23, T25, sum12_out_ga(T23, T25)) → sum12_out_ga(s(T23), s(T25))
U7_gga(T18, T13, sum12_out_ga(T18, T13)) → mult1_out_gga(T18, s(0), T13)
mult1_in_gga(T30, s(s(T31)), T13) → U8_gga(T30, T31, T13, mult24_in_gga(T30, T31, X58))
mult24_in_gga(T41, 0, 0) → mult24_out_gga(T41, 0, 0)
mult24_in_gga(T46, s(T47), X86) → U2_gga(T46, T47, X86, mult24_in_gga(T46, T47, X85))
mult24_in_gga(T46, s(T47), X86) → U3_gga(T46, T47, X86, mult24_in_gga(T46, T47, T50))
U3_gga(T46, T47, X86, mult24_out_gga(T46, T47, T50)) → U4_gga(T46, T47, X86, sum35_in_aga(T50, T46, X86))
sum35_in_aga(T59, 0, T59) → sum35_out_aga(T59, 0, T59)
sum35_in_aga(T64, s(T65), s(X113)) → U5_aga(T64, T65, X113, sum35_in_aga(T64, T65, X113))
U5_aga(T64, T65, X113, sum35_out_aga(T64, T65, X113)) → sum35_out_aga(T64, s(T65), s(X113))
U4_gga(T46, T47, X86, sum35_out_aga(T50, T46, X86)) → mult24_out_gga(T46, s(T47), X86)
U2_gga(T46, T47, X86, mult24_out_gga(T46, T47, X85)) → mult24_out_gga(T46, s(T47), X86)
U8_gga(T30, T31, T13, mult24_out_gga(T30, T31, X58)) → mult1_out_gga(T30, s(s(T31)), T13)
mult1_in_gga(T30, s(s(T31)), T13) → U9_gga(T30, T31, T13, mult24_in_gga(T30, T31, T34))
U9_gga(T30, T31, T13, mult24_out_gga(T30, T31, T34)) → U10_gga(T30, T31, T13, sum35_in_aga(T34, T30, X59))
U10_gga(T30, T31, T13, sum35_out_aga(T34, T30, X59)) → mult1_out_gga(T30, s(s(T31)), T13)
U9_gga(T30, T31, T13, mult24_out_gga(T30, T31, T34)) → U11_gga(T30, T31, T13, sum35_in_aga(T34, T30, T70))
U11_gga(T30, T31, T13, sum35_out_aga(T34, T30, T70)) → U12_gga(T30, T31, T13, sum45_in_aga(T70, T30, T13))
sum45_in_aga(T79, 0, T79) → sum45_out_aga(T79, 0, T79)
sum45_in_aga(T86, s(T87), s(T89)) → U6_aga(T86, T87, T89, sum45_in_aga(T86, T87, T89))
U6_aga(T86, T87, T89, sum45_out_aga(T86, T87, T89)) → sum45_out_aga(T86, s(T87), s(T89))
U12_gga(T30, T31, T13, sum45_out_aga(T70, T30, T13)) → mult1_out_gga(T30, s(s(T31)), T13)

The argument filtering Pi contains the following mapping:
mult1_in_gga(x1, x2, x3)  =  mult1_in_gga(x1, x2)
0  =  0
mult1_out_gga(x1, x2, x3)  =  mult1_out_gga
s(x1)  =  s(x1)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
sum12_in_ga(x1, x2)  =  sum12_in_ga(x1)
sum12_out_ga(x1, x2)  =  sum12_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x4)
mult24_in_gga(x1, x2, x3)  =  mult24_in_gga(x1, x2)
mult24_out_gga(x1, x2, x3)  =  mult24_out_gga
U2_gga(x1, x2, x3, x4)  =  U2_gga(x4)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x4)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x4)
sum35_in_aga(x1, x2, x3)  =  sum35_in_aga(x2)
sum35_out_aga(x1, x2, x3)  =  sum35_out_aga
U5_aga(x1, x2, x3, x4)  =  U5_aga(x4)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x4)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
sum45_in_aga(x1, x2, x3)  =  sum45_in_aga(x2)
sum45_out_aga(x1, x2, x3)  =  sum45_out_aga
U6_aga(x1, x2, x3, x4)  =  U6_aga(x4)

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

MULT1_IN_GGA(T18, s(0), T13) → U7_GGA(T18, T13, sum12_in_ga(T18, T13))
MULT1_IN_GGA(T18, s(0), T13) → SUM12_IN_GA(T18, T13)
SUM12_IN_GA(s(T23), s(T25)) → U1_GA(T23, T25, sum12_in_ga(T23, T25))
SUM12_IN_GA(s(T23), s(T25)) → SUM12_IN_GA(T23, T25)
MULT1_IN_GGA(T30, s(s(T31)), T13) → U8_GGA(T30, T31, T13, mult24_in_gga(T30, T31, X58))
MULT1_IN_GGA(T30, s(s(T31)), T13) → MULT24_IN_GGA(T30, T31, X58)
MULT24_IN_GGA(T46, s(T47), X86) → U2_GGA(T46, T47, X86, mult24_in_gga(T46, T47, X85))
MULT24_IN_GGA(T46, s(T47), X86) → MULT24_IN_GGA(T46, T47, X85)
MULT24_IN_GGA(T46, s(T47), X86) → U3_GGA(T46, T47, X86, mult24_in_gga(T46, T47, T50))
U3_GGA(T46, T47, X86, mult24_out_gga(T46, T47, T50)) → U4_GGA(T46, T47, X86, sum35_in_aga(T50, T46, X86))
U3_GGA(T46, T47, X86, mult24_out_gga(T46, T47, T50)) → SUM35_IN_AGA(T50, T46, X86)
SUM35_IN_AGA(T64, s(T65), s(X113)) → U5_AGA(T64, T65, X113, sum35_in_aga(T64, T65, X113))
SUM35_IN_AGA(T64, s(T65), s(X113)) → SUM35_IN_AGA(T64, T65, X113)
MULT1_IN_GGA(T30, s(s(T31)), T13) → U9_GGA(T30, T31, T13, mult24_in_gga(T30, T31, T34))
U9_GGA(T30, T31, T13, mult24_out_gga(T30, T31, T34)) → U10_GGA(T30, T31, T13, sum35_in_aga(T34, T30, X59))
U9_GGA(T30, T31, T13, mult24_out_gga(T30, T31, T34)) → SUM35_IN_AGA(T34, T30, X59)
U9_GGA(T30, T31, T13, mult24_out_gga(T30, T31, T34)) → U11_GGA(T30, T31, T13, sum35_in_aga(T34, T30, T70))
U11_GGA(T30, T31, T13, sum35_out_aga(T34, T30, T70)) → U12_GGA(T30, T31, T13, sum45_in_aga(T70, T30, T13))
U11_GGA(T30, T31, T13, sum35_out_aga(T34, T30, T70)) → SUM45_IN_AGA(T70, T30, T13)
SUM45_IN_AGA(T86, s(T87), s(T89)) → U6_AGA(T86, T87, T89, sum45_in_aga(T86, T87, T89))
SUM45_IN_AGA(T86, s(T87), s(T89)) → SUM45_IN_AGA(T86, T87, T89)

The TRS R consists of the following rules:

mult1_in_gga(T5, 0, 0) → mult1_out_gga(T5, 0, 0)
mult1_in_gga(T18, s(0), T13) → U7_gga(T18, T13, sum12_in_ga(T18, T13))
sum12_in_ga(0, 0) → sum12_out_ga(0, 0)
sum12_in_ga(s(T23), s(T25)) → U1_ga(T23, T25, sum12_in_ga(T23, T25))
U1_ga(T23, T25, sum12_out_ga(T23, T25)) → sum12_out_ga(s(T23), s(T25))
U7_gga(T18, T13, sum12_out_ga(T18, T13)) → mult1_out_gga(T18, s(0), T13)
mult1_in_gga(T30, s(s(T31)), T13) → U8_gga(T30, T31, T13, mult24_in_gga(T30, T31, X58))
mult24_in_gga(T41, 0, 0) → mult24_out_gga(T41, 0, 0)
mult24_in_gga(T46, s(T47), X86) → U2_gga(T46, T47, X86, mult24_in_gga(T46, T47, X85))
mult24_in_gga(T46, s(T47), X86) → U3_gga(T46, T47, X86, mult24_in_gga(T46, T47, T50))
U3_gga(T46, T47, X86, mult24_out_gga(T46, T47, T50)) → U4_gga(T46, T47, X86, sum35_in_aga(T50, T46, X86))
sum35_in_aga(T59, 0, T59) → sum35_out_aga(T59, 0, T59)
sum35_in_aga(T64, s(T65), s(X113)) → U5_aga(T64, T65, X113, sum35_in_aga(T64, T65, X113))
U5_aga(T64, T65, X113, sum35_out_aga(T64, T65, X113)) → sum35_out_aga(T64, s(T65), s(X113))
U4_gga(T46, T47, X86, sum35_out_aga(T50, T46, X86)) → mult24_out_gga(T46, s(T47), X86)
U2_gga(T46, T47, X86, mult24_out_gga(T46, T47, X85)) → mult24_out_gga(T46, s(T47), X86)
U8_gga(T30, T31, T13, mult24_out_gga(T30, T31, X58)) → mult1_out_gga(T30, s(s(T31)), T13)
mult1_in_gga(T30, s(s(T31)), T13) → U9_gga(T30, T31, T13, mult24_in_gga(T30, T31, T34))
U9_gga(T30, T31, T13, mult24_out_gga(T30, T31, T34)) → U10_gga(T30, T31, T13, sum35_in_aga(T34, T30, X59))
U10_gga(T30, T31, T13, sum35_out_aga(T34, T30, X59)) → mult1_out_gga(T30, s(s(T31)), T13)
U9_gga(T30, T31, T13, mult24_out_gga(T30, T31, T34)) → U11_gga(T30, T31, T13, sum35_in_aga(T34, T30, T70))
U11_gga(T30, T31, T13, sum35_out_aga(T34, T30, T70)) → U12_gga(T30, T31, T13, sum45_in_aga(T70, T30, T13))
sum45_in_aga(T79, 0, T79) → sum45_out_aga(T79, 0, T79)
sum45_in_aga(T86, s(T87), s(T89)) → U6_aga(T86, T87, T89, sum45_in_aga(T86, T87, T89))
U6_aga(T86, T87, T89, sum45_out_aga(T86, T87, T89)) → sum45_out_aga(T86, s(T87), s(T89))
U12_gga(T30, T31, T13, sum45_out_aga(T70, T30, T13)) → mult1_out_gga(T30, s(s(T31)), T13)

The argument filtering Pi contains the following mapping:
mult1_in_gga(x1, x2, x3)  =  mult1_in_gga(x1, x2)
0  =  0
mult1_out_gga(x1, x2, x3)  =  mult1_out_gga
s(x1)  =  s(x1)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
sum12_in_ga(x1, x2)  =  sum12_in_ga(x1)
sum12_out_ga(x1, x2)  =  sum12_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x4)
mult24_in_gga(x1, x2, x3)  =  mult24_in_gga(x1, x2)
mult24_out_gga(x1, x2, x3)  =  mult24_out_gga
U2_gga(x1, x2, x3, x4)  =  U2_gga(x4)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x4)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x4)
sum35_in_aga(x1, x2, x3)  =  sum35_in_aga(x2)
sum35_out_aga(x1, x2, x3)  =  sum35_out_aga
U5_aga(x1, x2, x3, x4)  =  U5_aga(x4)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x4)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
sum45_in_aga(x1, x2, x3)  =  sum45_in_aga(x2)
sum45_out_aga(x1, x2, x3)  =  sum45_out_aga
U6_aga(x1, x2, x3, x4)  =  U6_aga(x4)
MULT1_IN_GGA(x1, x2, x3)  =  MULT1_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3)  =  U7_GGA(x3)
SUM12_IN_GA(x1, x2)  =  SUM12_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x4)
MULT24_IN_GGA(x1, x2, x3)  =  MULT24_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x4)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x4)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x4)
SUM35_IN_AGA(x1, x2, x3)  =  SUM35_IN_AGA(x2)
U5_AGA(x1, x2, x3, x4)  =  U5_AGA(x4)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x1, x4)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x4)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x1, x4)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x4)
SUM45_IN_AGA(x1, x2, x3)  =  SUM45_IN_AGA(x2)
U6_AGA(x1, x2, x3, x4)  =  U6_AGA(x4)

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

(6) Obligation:

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

MULT1_IN_GGA(T18, s(0), T13) → U7_GGA(T18, T13, sum12_in_ga(T18, T13))
MULT1_IN_GGA(T18, s(0), T13) → SUM12_IN_GA(T18, T13)
SUM12_IN_GA(s(T23), s(T25)) → U1_GA(T23, T25, sum12_in_ga(T23, T25))
SUM12_IN_GA(s(T23), s(T25)) → SUM12_IN_GA(T23, T25)
MULT1_IN_GGA(T30, s(s(T31)), T13) → U8_GGA(T30, T31, T13, mult24_in_gga(T30, T31, X58))
MULT1_IN_GGA(T30, s(s(T31)), T13) → MULT24_IN_GGA(T30, T31, X58)
MULT24_IN_GGA(T46, s(T47), X86) → U2_GGA(T46, T47, X86, mult24_in_gga(T46, T47, X85))
MULT24_IN_GGA(T46, s(T47), X86) → MULT24_IN_GGA(T46, T47, X85)
MULT24_IN_GGA(T46, s(T47), X86) → U3_GGA(T46, T47, X86, mult24_in_gga(T46, T47, T50))
U3_GGA(T46, T47, X86, mult24_out_gga(T46, T47, T50)) → U4_GGA(T46, T47, X86, sum35_in_aga(T50, T46, X86))
U3_GGA(T46, T47, X86, mult24_out_gga(T46, T47, T50)) → SUM35_IN_AGA(T50, T46, X86)
SUM35_IN_AGA(T64, s(T65), s(X113)) → U5_AGA(T64, T65, X113, sum35_in_aga(T64, T65, X113))
SUM35_IN_AGA(T64, s(T65), s(X113)) → SUM35_IN_AGA(T64, T65, X113)
MULT1_IN_GGA(T30, s(s(T31)), T13) → U9_GGA(T30, T31, T13, mult24_in_gga(T30, T31, T34))
U9_GGA(T30, T31, T13, mult24_out_gga(T30, T31, T34)) → U10_GGA(T30, T31, T13, sum35_in_aga(T34, T30, X59))
U9_GGA(T30, T31, T13, mult24_out_gga(T30, T31, T34)) → SUM35_IN_AGA(T34, T30, X59)
U9_GGA(T30, T31, T13, mult24_out_gga(T30, T31, T34)) → U11_GGA(T30, T31, T13, sum35_in_aga(T34, T30, T70))
U11_GGA(T30, T31, T13, sum35_out_aga(T34, T30, T70)) → U12_GGA(T30, T31, T13, sum45_in_aga(T70, T30, T13))
U11_GGA(T30, T31, T13, sum35_out_aga(T34, T30, T70)) → SUM45_IN_AGA(T70, T30, T13)
SUM45_IN_AGA(T86, s(T87), s(T89)) → U6_AGA(T86, T87, T89, sum45_in_aga(T86, T87, T89))
SUM45_IN_AGA(T86, s(T87), s(T89)) → SUM45_IN_AGA(T86, T87, T89)

The TRS R consists of the following rules:

mult1_in_gga(T5, 0, 0) → mult1_out_gga(T5, 0, 0)
mult1_in_gga(T18, s(0), T13) → U7_gga(T18, T13, sum12_in_ga(T18, T13))
sum12_in_ga(0, 0) → sum12_out_ga(0, 0)
sum12_in_ga(s(T23), s(T25)) → U1_ga(T23, T25, sum12_in_ga(T23, T25))
U1_ga(T23, T25, sum12_out_ga(T23, T25)) → sum12_out_ga(s(T23), s(T25))
U7_gga(T18, T13, sum12_out_ga(T18, T13)) → mult1_out_gga(T18, s(0), T13)
mult1_in_gga(T30, s(s(T31)), T13) → U8_gga(T30, T31, T13, mult24_in_gga(T30, T31, X58))
mult24_in_gga(T41, 0, 0) → mult24_out_gga(T41, 0, 0)
mult24_in_gga(T46, s(T47), X86) → U2_gga(T46, T47, X86, mult24_in_gga(T46, T47, X85))
mult24_in_gga(T46, s(T47), X86) → U3_gga(T46, T47, X86, mult24_in_gga(T46, T47, T50))
U3_gga(T46, T47, X86, mult24_out_gga(T46, T47, T50)) → U4_gga(T46, T47, X86, sum35_in_aga(T50, T46, X86))
sum35_in_aga(T59, 0, T59) → sum35_out_aga(T59, 0, T59)
sum35_in_aga(T64, s(T65), s(X113)) → U5_aga(T64, T65, X113, sum35_in_aga(T64, T65, X113))
U5_aga(T64, T65, X113, sum35_out_aga(T64, T65, X113)) → sum35_out_aga(T64, s(T65), s(X113))
U4_gga(T46, T47, X86, sum35_out_aga(T50, T46, X86)) → mult24_out_gga(T46, s(T47), X86)
U2_gga(T46, T47, X86, mult24_out_gga(T46, T47, X85)) → mult24_out_gga(T46, s(T47), X86)
U8_gga(T30, T31, T13, mult24_out_gga(T30, T31, X58)) → mult1_out_gga(T30, s(s(T31)), T13)
mult1_in_gga(T30, s(s(T31)), T13) → U9_gga(T30, T31, T13, mult24_in_gga(T30, T31, T34))
U9_gga(T30, T31, T13, mult24_out_gga(T30, T31, T34)) → U10_gga(T30, T31, T13, sum35_in_aga(T34, T30, X59))
U10_gga(T30, T31, T13, sum35_out_aga(T34, T30, X59)) → mult1_out_gga(T30, s(s(T31)), T13)
U9_gga(T30, T31, T13, mult24_out_gga(T30, T31, T34)) → U11_gga(T30, T31, T13, sum35_in_aga(T34, T30, T70))
U11_gga(T30, T31, T13, sum35_out_aga(T34, T30, T70)) → U12_gga(T30, T31, T13, sum45_in_aga(T70, T30, T13))
sum45_in_aga(T79, 0, T79) → sum45_out_aga(T79, 0, T79)
sum45_in_aga(T86, s(T87), s(T89)) → U6_aga(T86, T87, T89, sum45_in_aga(T86, T87, T89))
U6_aga(T86, T87, T89, sum45_out_aga(T86, T87, T89)) → sum45_out_aga(T86, s(T87), s(T89))
U12_gga(T30, T31, T13, sum45_out_aga(T70, T30, T13)) → mult1_out_gga(T30, s(s(T31)), T13)

The argument filtering Pi contains the following mapping:
mult1_in_gga(x1, x2, x3)  =  mult1_in_gga(x1, x2)
0  =  0
mult1_out_gga(x1, x2, x3)  =  mult1_out_gga
s(x1)  =  s(x1)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
sum12_in_ga(x1, x2)  =  sum12_in_ga(x1)
sum12_out_ga(x1, x2)  =  sum12_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x4)
mult24_in_gga(x1, x2, x3)  =  mult24_in_gga(x1, x2)
mult24_out_gga(x1, x2, x3)  =  mult24_out_gga
U2_gga(x1, x2, x3, x4)  =  U2_gga(x4)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x4)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x4)
sum35_in_aga(x1, x2, x3)  =  sum35_in_aga(x2)
sum35_out_aga(x1, x2, x3)  =  sum35_out_aga
U5_aga(x1, x2, x3, x4)  =  U5_aga(x4)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x4)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
sum45_in_aga(x1, x2, x3)  =  sum45_in_aga(x2)
sum45_out_aga(x1, x2, x3)  =  sum45_out_aga
U6_aga(x1, x2, x3, x4)  =  U6_aga(x4)
MULT1_IN_GGA(x1, x2, x3)  =  MULT1_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3)  =  U7_GGA(x3)
SUM12_IN_GA(x1, x2)  =  SUM12_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x4)
MULT24_IN_GGA(x1, x2, x3)  =  MULT24_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x4)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x4)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x4)
SUM35_IN_AGA(x1, x2, x3)  =  SUM35_IN_AGA(x2)
U5_AGA(x1, x2, x3, x4)  =  U5_AGA(x4)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x1, x4)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x4)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x1, x4)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x4)
SUM45_IN_AGA(x1, x2, x3)  =  SUM45_IN_AGA(x2)
U6_AGA(x1, x2, x3, x4)  =  U6_AGA(x4)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Complex Obligation (AND)

(9) Obligation:

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

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

The TRS R consists of the following rules:

mult1_in_gga(T5, 0, 0) → mult1_out_gga(T5, 0, 0)
mult1_in_gga(T18, s(0), T13) → U7_gga(T18, T13, sum12_in_ga(T18, T13))
sum12_in_ga(0, 0) → sum12_out_ga(0, 0)
sum12_in_ga(s(T23), s(T25)) → U1_ga(T23, T25, sum12_in_ga(T23, T25))
U1_ga(T23, T25, sum12_out_ga(T23, T25)) → sum12_out_ga(s(T23), s(T25))
U7_gga(T18, T13, sum12_out_ga(T18, T13)) → mult1_out_gga(T18, s(0), T13)
mult1_in_gga(T30, s(s(T31)), T13) → U8_gga(T30, T31, T13, mult24_in_gga(T30, T31, X58))
mult24_in_gga(T41, 0, 0) → mult24_out_gga(T41, 0, 0)
mult24_in_gga(T46, s(T47), X86) → U2_gga(T46, T47, X86, mult24_in_gga(T46, T47, X85))
mult24_in_gga(T46, s(T47), X86) → U3_gga(T46, T47, X86, mult24_in_gga(T46, T47, T50))
U3_gga(T46, T47, X86, mult24_out_gga(T46, T47, T50)) → U4_gga(T46, T47, X86, sum35_in_aga(T50, T46, X86))
sum35_in_aga(T59, 0, T59) → sum35_out_aga(T59, 0, T59)
sum35_in_aga(T64, s(T65), s(X113)) → U5_aga(T64, T65, X113, sum35_in_aga(T64, T65, X113))
U5_aga(T64, T65, X113, sum35_out_aga(T64, T65, X113)) → sum35_out_aga(T64, s(T65), s(X113))
U4_gga(T46, T47, X86, sum35_out_aga(T50, T46, X86)) → mult24_out_gga(T46, s(T47), X86)
U2_gga(T46, T47, X86, mult24_out_gga(T46, T47, X85)) → mult24_out_gga(T46, s(T47), X86)
U8_gga(T30, T31, T13, mult24_out_gga(T30, T31, X58)) → mult1_out_gga(T30, s(s(T31)), T13)
mult1_in_gga(T30, s(s(T31)), T13) → U9_gga(T30, T31, T13, mult24_in_gga(T30, T31, T34))
U9_gga(T30, T31, T13, mult24_out_gga(T30, T31, T34)) → U10_gga(T30, T31, T13, sum35_in_aga(T34, T30, X59))
U10_gga(T30, T31, T13, sum35_out_aga(T34, T30, X59)) → mult1_out_gga(T30, s(s(T31)), T13)
U9_gga(T30, T31, T13, mult24_out_gga(T30, T31, T34)) → U11_gga(T30, T31, T13, sum35_in_aga(T34, T30, T70))
U11_gga(T30, T31, T13, sum35_out_aga(T34, T30, T70)) → U12_gga(T30, T31, T13, sum45_in_aga(T70, T30, T13))
sum45_in_aga(T79, 0, T79) → sum45_out_aga(T79, 0, T79)
sum45_in_aga(T86, s(T87), s(T89)) → U6_aga(T86, T87, T89, sum45_in_aga(T86, T87, T89))
U6_aga(T86, T87, T89, sum45_out_aga(T86, T87, T89)) → sum45_out_aga(T86, s(T87), s(T89))
U12_gga(T30, T31, T13, sum45_out_aga(T70, T30, T13)) → mult1_out_gga(T30, s(s(T31)), T13)

The argument filtering Pi contains the following mapping:
mult1_in_gga(x1, x2, x3)  =  mult1_in_gga(x1, x2)
0  =  0
mult1_out_gga(x1, x2, x3)  =  mult1_out_gga
s(x1)  =  s(x1)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
sum12_in_ga(x1, x2)  =  sum12_in_ga(x1)
sum12_out_ga(x1, x2)  =  sum12_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x4)
mult24_in_gga(x1, x2, x3)  =  mult24_in_gga(x1, x2)
mult24_out_gga(x1, x2, x3)  =  mult24_out_gga
U2_gga(x1, x2, x3, x4)  =  U2_gga(x4)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x4)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x4)
sum35_in_aga(x1, x2, x3)  =  sum35_in_aga(x2)
sum35_out_aga(x1, x2, x3)  =  sum35_out_aga
U5_aga(x1, x2, x3, x4)  =  U5_aga(x4)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x4)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
sum45_in_aga(x1, x2, x3)  =  sum45_in_aga(x2)
sum45_out_aga(x1, x2, x3)  =  sum45_out_aga
U6_aga(x1, x2, x3, x4)  =  U6_aga(x4)
SUM45_IN_AGA(x1, x2, x3)  =  SUM45_IN_AGA(x2)

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

(10) UsableRulesProof (EQUIVALENT transformation)

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

(11) Obligation:

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

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

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

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

(12) PiDPToQDPProof (SOUND transformation)

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

(13) Obligation:

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

SUM45_IN_AGA(s(T87)) → SUM45_IN_AGA(T87)

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

(14) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

• SUM45_IN_AGA(s(T87)) → SUM45_IN_AGA(T87)
  The graph contains the following edges 1 > 1

(15) YES

(16) Obligation:

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

SUM35_IN_AGA(T64, s(T65), s(X113)) → SUM35_IN_AGA(T64, T65, X113)

The TRS R consists of the following rules:

mult1_in_gga(T5, 0, 0) → mult1_out_gga(T5, 0, 0)
mult1_in_gga(T18, s(0), T13) → U7_gga(T18, T13, sum12_in_ga(T18, T13))
sum12_in_ga(0, 0) → sum12_out_ga(0, 0)
sum12_in_ga(s(T23), s(T25)) → U1_ga(T23, T25, sum12_in_ga(T23, T25))
U1_ga(T23, T25, sum12_out_ga(T23, T25)) → sum12_out_ga(s(T23), s(T25))
U7_gga(T18, T13, sum12_out_ga(T18, T13)) → mult1_out_gga(T18, s(0), T13)
mult1_in_gga(T30, s(s(T31)), T13) → U8_gga(T30, T31, T13, mult24_in_gga(T30, T31, X58))
mult24_in_gga(T41, 0, 0) → mult24_out_gga(T41, 0, 0)
mult24_in_gga(T46, s(T47), X86) → U2_gga(T46, T47, X86, mult24_in_gga(T46, T47, X85))
mult24_in_gga(T46, s(T47), X86) → U3_gga(T46, T47, X86, mult24_in_gga(T46, T47, T50))
U3_gga(T46, T47, X86, mult24_out_gga(T46, T47, T50)) → U4_gga(T46, T47, X86, sum35_in_aga(T50, T46, X86))
sum35_in_aga(T59, 0, T59) → sum35_out_aga(T59, 0, T59)
sum35_in_aga(T64, s(T65), s(X113)) → U5_aga(T64, T65, X113, sum35_in_aga(T64, T65, X113))
U5_aga(T64, T65, X113, sum35_out_aga(T64, T65, X113)) → sum35_out_aga(T64, s(T65), s(X113))
U4_gga(T46, T47, X86, sum35_out_aga(T50, T46, X86)) → mult24_out_gga(T46, s(T47), X86)
U2_gga(T46, T47, X86, mult24_out_gga(T46, T47, X85)) → mult24_out_gga(T46, s(T47), X86)
U8_gga(T30, T31, T13, mult24_out_gga(T30, T31, X58)) → mult1_out_gga(T30, s(s(T31)), T13)
mult1_in_gga(T30, s(s(T31)), T13) → U9_gga(T30, T31, T13, mult24_in_gga(T30, T31, T34))
U9_gga(T30, T31, T13, mult24_out_gga(T30, T31, T34)) → U10_gga(T30, T31, T13, sum35_in_aga(T34, T30, X59))
U10_gga(T30, T31, T13, sum35_out_aga(T34, T30, X59)) → mult1_out_gga(T30, s(s(T31)), T13)
U9_gga(T30, T31, T13, mult24_out_gga(T30, T31, T34)) → U11_gga(T30, T31, T13, sum35_in_aga(T34, T30, T70))
U11_gga(T30, T31, T13, sum35_out_aga(T34, T30, T70)) → U12_gga(T30, T31, T13, sum45_in_aga(T70, T30, T13))
sum45_in_aga(T79, 0, T79) → sum45_out_aga(T79, 0, T79)
sum45_in_aga(T86, s(T87), s(T89)) → U6_aga(T86, T87, T89, sum45_in_aga(T86, T87, T89))
U6_aga(T86, T87, T89, sum45_out_aga(T86, T87, T89)) → sum45_out_aga(T86, s(T87), s(T89))
U12_gga(T30, T31, T13, sum45_out_aga(T70, T30, T13)) → mult1_out_gga(T30, s(s(T31)), T13)

The argument filtering Pi contains the following mapping:
mult1_in_gga(x1, x2, x3)  =  mult1_in_gga(x1, x2)
0  =  0
mult1_out_gga(x1, x2, x3)  =  mult1_out_gga
s(x1)  =  s(x1)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
sum12_in_ga(x1, x2)  =  sum12_in_ga(x1)
sum12_out_ga(x1, x2)  =  sum12_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x4)
mult24_in_gga(x1, x2, x3)  =  mult24_in_gga(x1, x2)
mult24_out_gga(x1, x2, x3)  =  mult24_out_gga
U2_gga(x1, x2, x3, x4)  =  U2_gga(x4)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x4)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x4)
sum35_in_aga(x1, x2, x3)  =  sum35_in_aga(x2)
sum35_out_aga(x1, x2, x3)  =  sum35_out_aga
U5_aga(x1, x2, x3, x4)  =  U5_aga(x4)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x4)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
sum45_in_aga(x1, x2, x3)  =  sum45_in_aga(x2)
sum45_out_aga(x1, x2, x3)  =  sum45_out_aga
U6_aga(x1, x2, x3, x4)  =  U6_aga(x4)
SUM35_IN_AGA(x1, x2, x3)  =  SUM35_IN_AGA(x2)

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

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

SUM35_IN_AGA(T64, s(T65), s(X113)) → SUM35_IN_AGA(T64, T65, X113)

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

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

SUM35_IN_AGA(s(T65)) → SUM35_IN_AGA(T65)

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

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

• SUM35_IN_AGA(s(T65)) → SUM35_IN_AGA(T65)
  The graph contains the following edges 1 > 1

(22) YES

(23) Obligation:

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

MULT24_IN_GGA(T46, s(T47), X86) → MULT24_IN_GGA(T46, T47, X85)

The TRS R consists of the following rules:

mult1_in_gga(T5, 0, 0) → mult1_out_gga(T5, 0, 0)
mult1_in_gga(T18, s(0), T13) → U7_gga(T18, T13, sum12_in_ga(T18, T13))
sum12_in_ga(0, 0) → sum12_out_ga(0, 0)
sum12_in_ga(s(T23), s(T25)) → U1_ga(T23, T25, sum12_in_ga(T23, T25))
U1_ga(T23, T25, sum12_out_ga(T23, T25)) → sum12_out_ga(s(T23), s(T25))
U7_gga(T18, T13, sum12_out_ga(T18, T13)) → mult1_out_gga(T18, s(0), T13)
mult1_in_gga(T30, s(s(T31)), T13) → U8_gga(T30, T31, T13, mult24_in_gga(T30, T31, X58))
mult24_in_gga(T41, 0, 0) → mult24_out_gga(T41, 0, 0)
mult24_in_gga(T46, s(T47), X86) → U2_gga(T46, T47, X86, mult24_in_gga(T46, T47, X85))
mult24_in_gga(T46, s(T47), X86) → U3_gga(T46, T47, X86, mult24_in_gga(T46, T47, T50))
U3_gga(T46, T47, X86, mult24_out_gga(T46, T47, T50)) → U4_gga(T46, T47, X86, sum35_in_aga(T50, T46, X86))
sum35_in_aga(T59, 0, T59) → sum35_out_aga(T59, 0, T59)
sum35_in_aga(T64, s(T65), s(X113)) → U5_aga(T64, T65, X113, sum35_in_aga(T64, T65, X113))
U5_aga(T64, T65, X113, sum35_out_aga(T64, T65, X113)) → sum35_out_aga(T64, s(T65), s(X113))
U4_gga(T46, T47, X86, sum35_out_aga(T50, T46, X86)) → mult24_out_gga(T46, s(T47), X86)
U2_gga(T46, T47, X86, mult24_out_gga(T46, T47, X85)) → mult24_out_gga(T46, s(T47), X86)
U8_gga(T30, T31, T13, mult24_out_gga(T30, T31, X58)) → mult1_out_gga(T30, s(s(T31)), T13)
mult1_in_gga(T30, s(s(T31)), T13) → U9_gga(T30, T31, T13, mult24_in_gga(T30, T31, T34))
U9_gga(T30, T31, T13, mult24_out_gga(T30, T31, T34)) → U10_gga(T30, T31, T13, sum35_in_aga(T34, T30, X59))
U10_gga(T30, T31, T13, sum35_out_aga(T34, T30, X59)) → mult1_out_gga(T30, s(s(T31)), T13)
U9_gga(T30, T31, T13, mult24_out_gga(T30, T31, T34)) → U11_gga(T30, T31, T13, sum35_in_aga(T34, T30, T70))
U11_gga(T30, T31, T13, sum35_out_aga(T34, T30, T70)) → U12_gga(T30, T31, T13, sum45_in_aga(T70, T30, T13))
sum45_in_aga(T79, 0, T79) → sum45_out_aga(T79, 0, T79)
sum45_in_aga(T86, s(T87), s(T89)) → U6_aga(T86, T87, T89, sum45_in_aga(T86, T87, T89))
U6_aga(T86, T87, T89, sum45_out_aga(T86, T87, T89)) → sum45_out_aga(T86, s(T87), s(T89))
U12_gga(T30, T31, T13, sum45_out_aga(T70, T30, T13)) → mult1_out_gga(T30, s(s(T31)), T13)

The argument filtering Pi contains the following mapping:
mult1_in_gga(x1, x2, x3)  =  mult1_in_gga(x1, x2)
0  =  0
mult1_out_gga(x1, x2, x3)  =  mult1_out_gga
s(x1)  =  s(x1)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
sum12_in_ga(x1, x2)  =  sum12_in_ga(x1)
sum12_out_ga(x1, x2)  =  sum12_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x4)
mult24_in_gga(x1, x2, x3)  =  mult24_in_gga(x1, x2)
mult24_out_gga(x1, x2, x3)  =  mult24_out_gga
U2_gga(x1, x2, x3, x4)  =  U2_gga(x4)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x4)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x4)
sum35_in_aga(x1, x2, x3)  =  sum35_in_aga(x2)
sum35_out_aga(x1, x2, x3)  =  sum35_out_aga
U5_aga(x1, x2, x3, x4)  =  U5_aga(x4)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x4)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
sum45_in_aga(x1, x2, x3)  =  sum45_in_aga(x2)
sum45_out_aga(x1, x2, x3)  =  sum45_out_aga
U6_aga(x1, x2, x3, x4)  =  U6_aga(x4)
MULT24_IN_GGA(x1, x2, x3)  =  MULT24_IN_GGA(x1, x2)

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

(24) UsableRulesProof (EQUIVALENT transformation)

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

(25) Obligation:

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

MULT24_IN_GGA(T46, s(T47), X86) → MULT24_IN_GGA(T46, T47, X85)

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

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

(26) PiDPToQDPProof (SOUND transformation)

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

(27) Obligation:

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

MULT24_IN_GGA(T46, s(T47)) → MULT24_IN_GGA(T46, T47)

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

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

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

(29) YES

(30) Obligation:

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

SUM12_IN_GA(s(T23), s(T25)) → SUM12_IN_GA(T23, T25)

The TRS R consists of the following rules:

mult1_in_gga(T5, 0, 0) → mult1_out_gga(T5, 0, 0)
mult1_in_gga(T18, s(0), T13) → U7_gga(T18, T13, sum12_in_ga(T18, T13))
sum12_in_ga(0, 0) → sum12_out_ga(0, 0)
sum12_in_ga(s(T23), s(T25)) → U1_ga(T23, T25, sum12_in_ga(T23, T25))
U1_ga(T23, T25, sum12_out_ga(T23, T25)) → sum12_out_ga(s(T23), s(T25))
U7_gga(T18, T13, sum12_out_ga(T18, T13)) → mult1_out_gga(T18, s(0), T13)
mult1_in_gga(T30, s(s(T31)), T13) → U8_gga(T30, T31, T13, mult24_in_gga(T30, T31, X58))
mult24_in_gga(T41, 0, 0) → mult24_out_gga(T41, 0, 0)
mult24_in_gga(T46, s(T47), X86) → U2_gga(T46, T47, X86, mult24_in_gga(T46, T47, X85))
mult24_in_gga(T46, s(T47), X86) → U3_gga(T46, T47, X86, mult24_in_gga(T46, T47, T50))
U3_gga(T46, T47, X86, mult24_out_gga(T46, T47, T50)) → U4_gga(T46, T47, X86, sum35_in_aga(T50, T46, X86))
sum35_in_aga(T59, 0, T59) → sum35_out_aga(T59, 0, T59)
sum35_in_aga(T64, s(T65), s(X113)) → U5_aga(T64, T65, X113, sum35_in_aga(T64, T65, X113))
U5_aga(T64, T65, X113, sum35_out_aga(T64, T65, X113)) → sum35_out_aga(T64, s(T65), s(X113))
U4_gga(T46, T47, X86, sum35_out_aga(T50, T46, X86)) → mult24_out_gga(T46, s(T47), X86)
U2_gga(T46, T47, X86, mult24_out_gga(T46, T47, X85)) → mult24_out_gga(T46, s(T47), X86)
U8_gga(T30, T31, T13, mult24_out_gga(T30, T31, X58)) → mult1_out_gga(T30, s(s(T31)), T13)
mult1_in_gga(T30, s(s(T31)), T13) → U9_gga(T30, T31, T13, mult24_in_gga(T30, T31, T34))
U9_gga(T30, T31, T13, mult24_out_gga(T30, T31, T34)) → U10_gga(T30, T31, T13, sum35_in_aga(T34, T30, X59))
U10_gga(T30, T31, T13, sum35_out_aga(T34, T30, X59)) → mult1_out_gga(T30, s(s(T31)), T13)
U9_gga(T30, T31, T13, mult24_out_gga(T30, T31, T34)) → U11_gga(T30, T31, T13, sum35_in_aga(T34, T30, T70))
U11_gga(T30, T31, T13, sum35_out_aga(T34, T30, T70)) → U12_gga(T30, T31, T13, sum45_in_aga(T70, T30, T13))
sum45_in_aga(T79, 0, T79) → sum45_out_aga(T79, 0, T79)
sum45_in_aga(T86, s(T87), s(T89)) → U6_aga(T86, T87, T89, sum45_in_aga(T86, T87, T89))
U6_aga(T86, T87, T89, sum45_out_aga(T86, T87, T89)) → sum45_out_aga(T86, s(T87), s(T89))
U12_gga(T30, T31, T13, sum45_out_aga(T70, T30, T13)) → mult1_out_gga(T30, s(s(T31)), T13)

The argument filtering Pi contains the following mapping:
mult1_in_gga(x1, x2, x3)  =  mult1_in_gga(x1, x2)
0  =  0
mult1_out_gga(x1, x2, x3)  =  mult1_out_gga
s(x1)  =  s(x1)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
sum12_in_ga(x1, x2)  =  sum12_in_ga(x1)
sum12_out_ga(x1, x2)  =  sum12_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x4)
mult24_in_gga(x1, x2, x3)  =  mult24_in_gga(x1, x2)
mult24_out_gga(x1, x2, x3)  =  mult24_out_gga
U2_gga(x1, x2, x3, x4)  =  U2_gga(x4)
U3_gga(x1, x2, x3, x4)  =  U3_gga(x1, x4)
U4_gga(x1, x2, x3, x4)  =  U4_gga(x4)
sum35_in_aga(x1, x2, x3)  =  sum35_in_aga(x2)
sum35_out_aga(x1, x2, x3)  =  sum35_out_aga
U5_aga(x1, x2, x3, x4)  =  U5_aga(x4)
U9_gga(x1, x2, x3, x4)  =  U9_gga(x1, x4)
U10_gga(x1, x2, x3, x4)  =  U10_gga(x4)
U11_gga(x1, x2, x3, x4)  =  U11_gga(x1, x4)
U12_gga(x1, x2, x3, x4)  =  U12_gga(x4)
sum45_in_aga(x1, x2, x3)  =  sum45_in_aga(x2)
sum45_out_aga(x1, x2, x3)  =  sum45_out_aga
U6_aga(x1, x2, x3, x4)  =  U6_aga(x4)
SUM12_IN_GA(x1, x2)  =  SUM12_IN_GA(x1)

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

(31) UsableRulesProof (EQUIVALENT transformation)

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

(32) Obligation:

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

SUM12_IN_GA(s(T23), s(T25)) → SUM12_IN_GA(T23, T25)

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

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

(33) PiDPToQDPProof (SOUND transformation)

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

(34) Obligation:

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

SUM12_IN_GA(s(T23)) → SUM12_IN_GA(T23)

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

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

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

(36) YES