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) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT 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:

Triples:

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

Clauses:

sumc12(0, 0).
sumc12(s(T23), s(T25)) :- sumc12(T23, T25).
multc24(T41, 0, 0).
multc24(T46, s(T47), X86) :- ','(multc24(T46, T47, T50), sumc35(T50, T46, X86)).
sumc35(T59, 0, T59).
sumc35(T64, s(T65), s(X113)) :- sumc35(T64, T65, X113).
sumc45(T79, 0, T79).
sumc45(T86, s(T87), s(T89)) :- sumc45(T86, T87, T89).

Afs:

mult1(x1, x2, x3)  =  mult1(x1, x2)

(3) TriplesToPiDPProof (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)
multc24_in: (b,b,f)
sumc35_in: (b,b,f)
sum35_in: (b,b,f)
sum45_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
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, multc24_in_gga(T46, T47, T50))
U3_GGA(T46, T47, X86, multc24_out_gga(T46, T47, T50)) → U4_GGA(T46, T47, X86, sum35_in_gga(T50, T46, X86))
U3_GGA(T46, T47, X86, multc24_out_gga(T46, T47, T50)) → SUM35_IN_GGA(T50, T46, X86)
SUM35_IN_GGA(T64, s(T65), s(X113)) → U5_GGA(T64, T65, X113, sum35_in_gga(T64, T65, X113))
SUM35_IN_GGA(T64, s(T65), s(X113)) → SUM35_IN_GGA(T64, T65, X113)
MULT1_IN_GGA(T30, s(s(T31)), T13) → U9_GGA(T30, T31, T13, multc24_in_gga(T30, T31, T34))
U9_GGA(T30, T31, T13, multc24_out_gga(T30, T31, T34)) → U10_GGA(T30, T31, T13, sum35_in_gga(T34, T30, X59))
U9_GGA(T30, T31, T13, multc24_out_gga(T30, T31, T34)) → SUM35_IN_GGA(T34, T30, X59)
U9_GGA(T30, T31, T13, multc24_out_gga(T30, T31, T34)) → U11_GGA(T30, T31, T13, sumc35_in_gga(T34, T30, T70))
U11_GGA(T30, T31, T13, sumc35_out_gga(T34, T30, T70)) → U12_GGA(T30, T31, T13, sum45_in_gga(T70, T30, T13))
U11_GGA(T30, T31, T13, sumc35_out_gga(T34, T30, T70)) → SUM45_IN_GGA(T70, T30, T13)
SUM45_IN_GGA(T86, s(T87), s(T89)) → U6_GGA(T86, T87, T89, sum45_in_gga(T86, T87, T89))
SUM45_IN_GGA(T86, s(T87), s(T89)) → SUM45_IN_GGA(T86, T87, T89)

The TRS R consists of the following rules:

multc24_in_gga(T41, 0, 0) → multc24_out_gga(T41, 0, 0)
multc24_in_gga(T46, s(T47), X86) → U15_gga(T46, T47, X86, multc24_in_gga(T46, T47, T50))
U15_gga(T46, T47, X86, multc24_out_gga(T46, T47, T50)) → U16_gga(T46, T47, X86, sumc35_in_gga(T50, T46, X86))
sumc35_in_gga(T59, 0, T59) → sumc35_out_gga(T59, 0, T59)
sumc35_in_gga(T64, s(T65), s(X113)) → U17_gga(T64, T65, X113, sumc35_in_gga(T64, T65, X113))
U17_gga(T64, T65, X113, sumc35_out_gga(T64, T65, X113)) → sumc35_out_gga(T64, s(T65), s(X113))
U16_gga(T46, T47, X86, sumc35_out_gga(T50, T46, X86)) → multc24_out_gga(T46, s(T47), X86)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
sum12_in_ga(x1, x2)  =  sum12_in_ga(x1)
mult24_in_gga(x1, x2, x3)  =  mult24_in_gga(x1, x2)
multc24_in_gga(x1, x2, x3)  =  multc24_in_gga(x1, x2)
multc24_out_gga(x1, x2, x3)  =  multc24_out_gga(x1, x2, x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x1, x2, x4)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
sumc35_in_gga(x1, x2, x3)  =  sumc35_in_gga(x1, x2)
sumc35_out_gga(x1, x2, x3)  =  sumc35_out_gga(x1, x2, x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
sum35_in_gga(x1, x2, x3)  =  sum35_in_gga(x1, x2)
sum45_in_gga(x1, x2, x3)  =  sum45_in_gga(x1, x2)
MULT1_IN_GGA(x1, x2, x3)  =  MULT1_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3)  =  U7_GGA(x1, x3)
SUM12_IN_GA(x1, x2)  =  SUM12_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
MULT24_IN_GGA(x1, x2, x3)  =  MULT24_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
SUM35_IN_GGA(x1, x2, x3)  =  SUM35_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x1, x2, x4)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x1, x2, x4)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x1, x2, x4)
SUM45_IN_GGA(x1, x2, x3)  =  SUM45_IN_GGA(x1, x2)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) 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, multc24_in_gga(T46, T47, T50))
U3_GGA(T46, T47, X86, multc24_out_gga(T46, T47, T50)) → U4_GGA(T46, T47, X86, sum35_in_gga(T50, T46, X86))
U3_GGA(T46, T47, X86, multc24_out_gga(T46, T47, T50)) → SUM35_IN_GGA(T50, T46, X86)
SUM35_IN_GGA(T64, s(T65), s(X113)) → U5_GGA(T64, T65, X113, sum35_in_gga(T64, T65, X113))
SUM35_IN_GGA(T64, s(T65), s(X113)) → SUM35_IN_GGA(T64, T65, X113)
MULT1_IN_GGA(T30, s(s(T31)), T13) → U9_GGA(T30, T31, T13, multc24_in_gga(T30, T31, T34))
U9_GGA(T30, T31, T13, multc24_out_gga(T30, T31, T34)) → U10_GGA(T30, T31, T13, sum35_in_gga(T34, T30, X59))
U9_GGA(T30, T31, T13, multc24_out_gga(T30, T31, T34)) → SUM35_IN_GGA(T34, T30, X59)
U9_GGA(T30, T31, T13, multc24_out_gga(T30, T31, T34)) → U11_GGA(T30, T31, T13, sumc35_in_gga(T34, T30, T70))
U11_GGA(T30, T31, T13, sumc35_out_gga(T34, T30, T70)) → U12_GGA(T30, T31, T13, sum45_in_gga(T70, T30, T13))
U11_GGA(T30, T31, T13, sumc35_out_gga(T34, T30, T70)) → SUM45_IN_GGA(T70, T30, T13)
SUM45_IN_GGA(T86, s(T87), s(T89)) → U6_GGA(T86, T87, T89, sum45_in_gga(T86, T87, T89))
SUM45_IN_GGA(T86, s(T87), s(T89)) → SUM45_IN_GGA(T86, T87, T89)

The TRS R consists of the following rules:

multc24_in_gga(T41, 0, 0) → multc24_out_gga(T41, 0, 0)
multc24_in_gga(T46, s(T47), X86) → U15_gga(T46, T47, X86, multc24_in_gga(T46, T47, T50))
U15_gga(T46, T47, X86, multc24_out_gga(T46, T47, T50)) → U16_gga(T46, T47, X86, sumc35_in_gga(T50, T46, X86))
sumc35_in_gga(T59, 0, T59) → sumc35_out_gga(T59, 0, T59)
sumc35_in_gga(T64, s(T65), s(X113)) → U17_gga(T64, T65, X113, sumc35_in_gga(T64, T65, X113))
U17_gga(T64, T65, X113, sumc35_out_gga(T64, T65, X113)) → sumc35_out_gga(T64, s(T65), s(X113))
U16_gga(T46, T47, X86, sumc35_out_gga(T50, T46, X86)) → multc24_out_gga(T46, s(T47), X86)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
sum12_in_ga(x1, x2)  =  sum12_in_ga(x1)
mult24_in_gga(x1, x2, x3)  =  mult24_in_gga(x1, x2)
multc24_in_gga(x1, x2, x3)  =  multc24_in_gga(x1, x2)
multc24_out_gga(x1, x2, x3)  =  multc24_out_gga(x1, x2, x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x1, x2, x4)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
sumc35_in_gga(x1, x2, x3)  =  sumc35_in_gga(x1, x2)
sumc35_out_gga(x1, x2, x3)  =  sumc35_out_gga(x1, x2, x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
sum35_in_gga(x1, x2, x3)  =  sum35_in_gga(x1, x2)
sum45_in_gga(x1, x2, x3)  =  sum45_in_gga(x1, x2)
MULT1_IN_GGA(x1, x2, x3)  =  MULT1_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3)  =  U7_GGA(x1, x3)
SUM12_IN_GA(x1, x2)  =  SUM12_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
MULT24_IN_GGA(x1, x2, x3)  =  MULT24_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4)  =  U2_GGA(x1, x2, x4)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
SUM35_IN_GGA(x1, x2, x3)  =  SUM35_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x1, x2, x4)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x1, x2, x4)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x1, x2, x4)
SUM45_IN_GGA(x1, x2, x3)  =  SUM45_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 17 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

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

The TRS R consists of the following rules:

multc24_in_gga(T41, 0, 0) → multc24_out_gga(T41, 0, 0)
multc24_in_gga(T46, s(T47), X86) → U15_gga(T46, T47, X86, multc24_in_gga(T46, T47, T50))
U15_gga(T46, T47, X86, multc24_out_gga(T46, T47, T50)) → U16_gga(T46, T47, X86, sumc35_in_gga(T50, T46, X86))
sumc35_in_gga(T59, 0, T59) → sumc35_out_gga(T59, 0, T59)
sumc35_in_gga(T64, s(T65), s(X113)) → U17_gga(T64, T65, X113, sumc35_in_gga(T64, T65, X113))
U17_gga(T64, T65, X113, sumc35_out_gga(T64, T65, X113)) → sumc35_out_gga(T64, s(T65), s(X113))
U16_gga(T46, T47, X86, sumc35_out_gga(T50, T46, X86)) → multc24_out_gga(T46, s(T47), X86)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
multc24_in_gga(x1, x2, x3)  =  multc24_in_gga(x1, x2)
multc24_out_gga(x1, x2, x3)  =  multc24_out_gga(x1, x2, x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x1, x2, x4)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
sumc35_in_gga(x1, x2, x3)  =  sumc35_in_gga(x1, x2)
sumc35_out_gga(x1, x2, x3)  =  sumc35_out_gga(x1, x2, x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
SUM45_IN_GGA(x1, x2, x3)  =  SUM45_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:

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

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

SUM45_IN_GGA(T86, s(T87)) → SUM45_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:

• SUM45_IN_GGA(T86, s(T87)) → SUM45_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:

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

The TRS R consists of the following rules:

multc24_in_gga(T41, 0, 0) → multc24_out_gga(T41, 0, 0)
multc24_in_gga(T46, s(T47), X86) → U15_gga(T46, T47, X86, multc24_in_gga(T46, T47, T50))
U15_gga(T46, T47, X86, multc24_out_gga(T46, T47, T50)) → U16_gga(T46, T47, X86, sumc35_in_gga(T50, T46, X86))
sumc35_in_gga(T59, 0, T59) → sumc35_out_gga(T59, 0, T59)
sumc35_in_gga(T64, s(T65), s(X113)) → U17_gga(T64, T65, X113, sumc35_in_gga(T64, T65, X113))
U17_gga(T64, T65, X113, sumc35_out_gga(T64, T65, X113)) → sumc35_out_gga(T64, s(T65), s(X113))
U16_gga(T46, T47, X86, sumc35_out_gga(T50, T46, X86)) → multc24_out_gga(T46, s(T47), X86)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
multc24_in_gga(x1, x2, x3)  =  multc24_in_gga(x1, x2)
multc24_out_gga(x1, x2, x3)  =  multc24_out_gga(x1, x2, x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x1, x2, x4)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
sumc35_in_gga(x1, x2, x3)  =  sumc35_in_gga(x1, x2)
sumc35_out_gga(x1, x2, x3)  =  sumc35_out_gga(x1, x2, x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
SUM35_IN_GGA(x1, x2, x3)  =  SUM35_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:

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

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

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

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

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

The TRS R consists of the following rules:

multc24_in_gga(T41, 0, 0) → multc24_out_gga(T41, 0, 0)
multc24_in_gga(T46, s(T47), X86) → U15_gga(T46, T47, X86, multc24_in_gga(T46, T47, T50))
U15_gga(T46, T47, X86, multc24_out_gga(T46, T47, T50)) → U16_gga(T46, T47, X86, sumc35_in_gga(T50, T46, X86))
sumc35_in_gga(T59, 0, T59) → sumc35_out_gga(T59, 0, T59)
sumc35_in_gga(T64, s(T65), s(X113)) → U17_gga(T64, T65, X113, sumc35_in_gga(T64, T65, X113))
U17_gga(T64, T65, X113, sumc35_out_gga(T64, T65, X113)) → sumc35_out_gga(T64, s(T65), s(X113))
U16_gga(T46, T47, X86, sumc35_out_gga(T50, T46, X86)) → multc24_out_gga(T46, s(T47), X86)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
multc24_in_gga(x1, x2, x3)  =  multc24_in_gga(x1, x2)
multc24_out_gga(x1, x2, x3)  =  multc24_out_gga(x1, x2, x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x1, x2, x4)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
sumc35_in_gga(x1, x2, x3)  =  sumc35_in_gga(x1, x2)
sumc35_out_gga(x1, x2, x3)  =  sumc35_out_gga(x1, x2, x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
MULT24_IN_GGA(x1, x2, x3)  =  MULT24_IN_GGA(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:

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

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

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.

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

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

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

The TRS R consists of the following rules:

multc24_in_gga(T41, 0, 0) → multc24_out_gga(T41, 0, 0)
multc24_in_gga(T46, s(T47), X86) → U15_gga(T46, T47, X86, multc24_in_gga(T46, T47, T50))
U15_gga(T46, T47, X86, multc24_out_gga(T46, T47, T50)) → U16_gga(T46, T47, X86, sumc35_in_gga(T50, T46, X86))
sumc35_in_gga(T59, 0, T59) → sumc35_out_gga(T59, 0, T59)
sumc35_in_gga(T64, s(T65), s(X113)) → U17_gga(T64, T65, X113, sumc35_in_gga(T64, T65, X113))
U17_gga(T64, T65, X113, sumc35_out_gga(T64, T65, X113)) → sumc35_out_gga(T64, s(T65), s(X113))
U16_gga(T46, T47, X86, sumc35_out_gga(T50, T46, X86)) → multc24_out_gga(T46, s(T47), X86)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
multc24_in_gga(x1, x2, x3)  =  multc24_in_gga(x1, x2)
multc24_out_gga(x1, x2, x3)  =  multc24_out_gga(x1, x2, x3)
U15_gga(x1, x2, x3, x4)  =  U15_gga(x1, x2, x4)
U16_gga(x1, x2, x3, x4)  =  U16_gga(x1, x2, x4)
sumc35_in_gga(x1, x2, x3)  =  sumc35_in_gga(x1, x2)
sumc35_out_gga(x1, x2, x3)  =  sumc35_out_gga(x1, x2, x3)
U17_gga(x1, x2, x3, x4)  =  U17_gga(x1, x2, x4)
SUM12_IN_GA(x1, x2)  =  SUM12_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:

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

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

SUM12_IN_GA(s(T23)) → SUM12_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:

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

(34) YES