Left Termination proof of /tmp/tmpEIIlp5/evaluate.pl

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

0 Prolog

↳1 PrologToDTProblemTransformerProof (⇐)

↳2 TRIPLES

↳3 TriplesToPiDPProof (⇐)

↳4 PiDP

↳5 DependencyGraphProof (⇔)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇐)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇔)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔)

        ↳20 YES

    ↳21 PiDP

        ↳22 UsableRulesProof (⇔)

        ↳23 PiDP

        ↳24 PiDPToQDPProof (⇐)

        ↳25 QDP

        ↳26 QDPSizeChangeProof (⇔)

        ↳27 YES

    ↳28 PiDP

        ↳29 UsableRulesProof (⇔)

        ↳30 PiDP

        ↳31 PiDPToQDPProof (⇐)

        ↳32 QDP

        ↳33 QDPSizeChangeProof (⇔)

        ↳34 YES

    ↳35 PiDP

        ↳36 UsableRulesProof (⇔)

        ↳37 PiDP

        ↳38 PiDPToQDPProof (⇐)

        ↳39 QDP

        ↳40 QDPSizeChangeProof (⇔)

        ↳41 YES

    ↳42 PiDP

        ↳43 PiDPToQDPProof (⇐)

        ↳44 QDP

        ↳45 QDPSizeChangeProof (⇔)

        ↳46 YES

(0) Obligation:

Clauses:

myis(Z, X) :- evaluate(X, Z).
evaluate(+(X, Y), Z) :- ','(evaluate(X, X1), ','(evaluate(Y, Y1), add(X1, Y1, Z))).
evaluate(-(X, Y), Z) :- ','(evaluate(X, X1), ','(evaluate(Y, Y1), sub(X1, Y1, Z))).
evaluate(*(X, Y), Z) :- ','(evaluate(X, X1), ','(evaluate(Y, Y1), mult(X1, Y1, Z))).
evaluate(X, X) :- myinteger(X).
myinteger(s(X)) :- myinteger(X).
myinteger(0).
add(s(X), Y, s(Z)) :- add(X, Y, Z).
add(0, X, X).
sub(s(X), s(Y), Z) :- sub(X, Y, Z).
sub(X, 0, X).
mult(s(X), Y, R) :- ','(mult(X, Y, Z), add(Y, Z, R)).
mult(0, Y, 0).
notEq(s(X), s(Y)) :- notEq(X, Y).
notEq(s(X), 0).
notEq(0, s(X)).
lt(s(X), s(Y)) :- lt(X, Y).
lt(0, s(Y)).
gt(s(X), s(Y)) :- gt(X, Y).
gt(s(X), 0).
le(s(X), s(Y)) :- le(X, Y).
le(0, s(Y)).
le(0, 0).

Queries:

myis(a,g).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: myis(T1, T2)\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: myis(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: evaluate(T6, T7)\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: evaluate(T6, T7), SCOPE: 2, CLAUSE: 1 | evaluate(T6, T7), SCOPE: 2, CLAUSE: 2 | evaluate(T6, T7), SCOPE: 2, CLAUSE: 3 | evaluate(T6, T7), SCOPE: 2, CLAUSE: 4\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: evaluate(T6, T7), SCOPE: 2, CLAUSE: 1\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: evaluate(T6, T7), SCOPE: 2, CLAUSE: 2 | evaluate(T6, T7), SCOPE: 2, CLAUSE: 3 | evaluate(T6, T7), SCOPE: 2, CLAUSE: 4\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(evaluate(T20, X25), ','(evaluate(T21, X26), add(X25, X26, T23)))\n\nT20 is ground\nT21 is ground\nX25 is free; \nX26 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: evaluate(T20, X25)\n\nT20 is ground\nX25 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(evaluate(T21, X26), add(T26, X26, T23))\n\nT21 is ground\nT26 is ground\nX26 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: evaluate(T21, X26)\n\nT21 is ground\nX26 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: add(T26, T31, T23)\n\nT26 is ground\nT31 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: add(T26, T31, T23), SCOPE: 3, CLAUSE: 7 | add(T26, T31, T23), SCOPE: 3, CLAUSE: 8\n\nT26 is ground\nT31 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: add(T26, T31, T23), SCOPE: 3, CLAUSE: 7\n\nT26 is ground\nT31 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: add(T26, T31, T23), SCOPE: 3, CLAUSE: 8\n\nT26 is ground\nT31 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: add(T49, T50, T52)\n\nT49 is ground\nT50 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: evaluate(T6, T7), SCOPE: 2, CLAUSE: 2\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: evaluate(T6, T7), SCOPE: 2, CLAUSE: 3 | evaluate(T6, T7), SCOPE: 2, CLAUSE: 4\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(evaluate(T71, X101), ','(evaluate(T72, X102), sub(X101, X102, T74)))\n\nT71 is ground\nT72 is ground\nX101 is free; \nX102 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: evaluate(T71, X101)\n\nT71 is ground\nX101 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(evaluate(T72, X102), sub(T77, X102, T74))\n\nT72 is ground\nT77 is ground\nX102 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: evaluate(T72, X102)\n\nT72 is ground\nX102 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: sub(T77, T82, T74)\n\nT77 is ground\nT82 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: sub(T77, T82, T74), SCOPE: 4, CLAUSE: 9 | sub(T77, T82, T74), SCOPE: 4, CLAUSE: 10\n\nT77 is ground\nT82 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: sub(T77, T82, T74), SCOPE: 4, CLAUSE: 9\n\nT77 is ground\nT82 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: sub(T77, T82, T74), SCOPE: 4, CLAUSE: 10\n\nT77 is ground\nT82 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: sub(T100, T101, T103)\n\nT100 is ground\nT101 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: evaluate(T6, T7), SCOPE: 2, CLAUSE: 3\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: evaluate(T6, T7), SCOPE: 2, CLAUSE: 4\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(evaluate(T122, X177), ','(evaluate(T123, X178), mult(X177, X178, T125)))\n\nT122 is ground\nT123 is ground\nX177 is free; \nX178 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: evaluate(T122, X177)\n\nT122 is ground\nX177 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ','(evaluate(T123, X178), mult(T128, X178, T125))\n\nT123 is ground\nT128 is ground\nX178 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: evaluate(T123, X178)\n\nT123 is ground\nX178 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: mult(T128, T133, T125)\n\nT128 is ground\nT133 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: mult(T128, T133, T125), SCOPE: 5, CLAUSE: 11 | mult(T128, T133, T125), SCOPE: 5, CLAUSE: 12\n\nT128 is ground\nT133 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: mult(T128, T133, T125), SCOPE: 5, CLAUSE: 11\n\nT128 is ground\nT133 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: mult(T128, T133, T125), SCOPE: 5, CLAUSE: 12\n\nT128 is ground\nT133 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(mult(T151, T152, X227), add(T152, X227, T154))\n\nT151 is ground\nT152 is ground\nX227 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: mult(T151, T152, X227)\n\nT151 is ground\nT152 is ground\nX227 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: add(T152, T157, T154)\n\nT152 is ground\nT157 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: mult(T151, T152, X227), SCOPE: 6, CLAUSE: 11 | mult(T151, T152, X227), SCOPE: 6, CLAUSE: 12\n\nT151 is ground\nT152 is ground\nX227 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: mult(T151, T152, X227), SCOPE: 6, CLAUSE: 11\n\nT151 is ground\nT152 is ground\nX227 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: mult(T151, T152, X227), SCOPE: 6, CLAUSE: 12\n\nT151 is ground\nT152 is ground\nX227 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(mult(T168, T169, X262), add(T169, X262, X263))\n\nT168 is ground\nT169 is ground\nX263 is free; \nX262 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: mult(T168, T169, X262)\n\nT168 is ground\nT169 is ground\nX262 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: add(T169, T172, X263)\n\nT169 is ground\nT172 is ground\nX263 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: add(T169, T172, X263), SCOPE: 7, CLAUSE: 7 | add(T169, T172, X263), SCOPE: 7, CLAUSE: 8\n\nT169 is ground\nT172 is ground\nX263 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: add(T169, T172, X263), SCOPE: 7, CLAUSE: 7\n\nT169 is ground\nT172 is ground\nX263 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: add(T169, T172, X263), SCOPE: 7, CLAUSE: 8\n\nT169 is ground\nT172 is ground\nX263 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: add(T185, T186, X300)\n\nT185 is ground\nT186 is ground\nX300 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: myinteger(T203)\n\nT203 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: myinteger(T203), SCOPE: 8, CLAUSE: 5 | myinteger(T203), SCOPE: 8, CLAUSE: 6\n\nT203 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: myinteger(T203), SCOPE: 8, CLAUSE: 5\n\nT203 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: myinteger(T203), SCOPE: 8, CLAUSE: 6\n\nT203 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: myinteger(T209)\n\nT209 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 83 [arrowhead = none ];
83 -> 2;

84 [label="ONLY EVAL with clause\nmyis(X4, X5) :- evaluate(X5, X4).\nand substitution\nT1 -> T7\nX4 -> T7\nT2 -> T6\nX5 -> T6\nT5 -> T7", fontsize=14, style = filled, fillcolor = white];
2 -> 84 [arrowhead = none ];
84 -> 3;

85 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 85 [arrowhead = none ];
85 -> 4;

86 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 86 [arrowhead = none ];
86 -> 5;

87 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
4 -> 87 [arrowhead = none ];
87 -> 6;

88 [label="EVAL with clause\nevaluate(+(X22, X23), X24) :- ','(evaluate(X22, X25), ','(evaluate(X23, X26), add(X25, X26, X24))).\nand substitution\nX22 -> T20\nX23 -> T21\nT6 -> +(T20, T21)\nT7 -> T23\nX24 -> T23\nT22 -> T23", fontsize=14, style = filled, fillcolor = lightblue];
5 -> 88 [arrowhead = none ];
88 -> 7;

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

90 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
6 -> 90 [arrowhead = none ];
90 -> 21;

91 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
6 -> 91 [arrowhead = none ];
91 -> 22;

92 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
7 -> 92 [arrowhead = none ];
92 -> 9;

93 [label="SPLIT 2\nnew knowledge:\nT26 is ground\nreplacements:\nX25 -> T26", fontsize=14, style = filled, fillcolor = violet];
7 -> 93 [arrowhead = none ];
93 -> 10;

94 [label="INSTANCE with matching:\nT6 -> T20\nT7 -> X25", fontsize=14, style = filled, fillcolor = lightgrey];
9 -> 94 [arrowhead = none , style=dashed];
94 -> 3[style=dashed];

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

96 [label="SPLIT 2\nnew knowledge:\nT31 is ground\nreplacements:\nX26 -> T31", fontsize=14, style = filled, fillcolor = violet];
10 -> 96 [arrowhead = none ];
96 -> 12;

97 [label="INSTANCE with matching:\nT6 -> T21\nT7 -> X26", fontsize=14, style = filled, fillcolor = lightgrey];
11 -> 97 [arrowhead = none , style=dashed];
97 -> 3[style=dashed];

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

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

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

101 [label="EVAL with clause\nadd(s(X69), X70, s(X71)) :- add(X69, X70, X71).\nand substitution\nX69 -> T49\nT26 -> s(T49)\nT31 -> T50\nX70 -> T50\nX71 -> T52\nT23 -> s(T52)\nT51 -> T52", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 101 [arrowhead = none ];
101 -> 16;

102 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 102 [arrowhead = none ];
102 -> 17;

103 [label="EVAL with clause\nadd(0, X80, X80).\nand substitution\nT26 -> 0\nT31 -> T58\nX80 -> T58\nT23 -> T58", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 103 [arrowhead = none ];
103 -> 18;

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

105 [label="INSTANCE with matching:\nT26 -> T49\nT31 -> T50\nT23 -> T52", fontsize=14, style = filled, fillcolor = lightgrey];
16 -> 105 [arrowhead = none , style=dashed];
105 -> 12[style=dashed];

106 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
18 -> 106 [arrowhead = none ];
106 -> 20;

107 [label="EVAL with clause\nevaluate(-(X98, X99), X100) :- ','(evaluate(X98, X101), ','(evaluate(X99, X102), sub(X101, X102, X100))).\nand substitution\nX98 -> T71\nX99 -> T72\nT6 -> -(T71, T72)\nT7 -> T74\nX100 -> T74\nT73 -> T74", fontsize=14, style = filled, fillcolor = lightblue];
21 -> 107 [arrowhead = none ];
107 -> 23;

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

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

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

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

112 [label="SPLIT 2\nnew knowledge:\nT77 is ground\nreplacements:\nX101 -> T77", fontsize=14, style = filled, fillcolor = violet];
23 -> 112 [arrowhead = none ];
112 -> 26;

113 [label="INSTANCE with matching:\nT6 -> T71\nT7 -> X101", fontsize=14, style = filled, fillcolor = lightgrey];
25 -> 113 [arrowhead = none , style=dashed];
113 -> 3[style=dashed];

114 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
26 -> 114 [arrowhead = none ];
114 -> 27;

115 [label="SPLIT 2\nnew knowledge:\nT82 is ground\nreplacements:\nX102 -> T82", fontsize=14, style = filled, fillcolor = violet];
26 -> 115 [arrowhead = none ];
115 -> 28;

116 [label="INSTANCE with matching:\nT6 -> T72\nT7 -> X102", fontsize=14, style = filled, fillcolor = lightgrey];
27 -> 116 [arrowhead = none , style=dashed];
116 -> 3[style=dashed];

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

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

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

120 [label="EVAL with clause\nsub(s(X145), s(X146), X147) :- sub(X145, X146, X147).\nand substitution\nX145 -> T100\nT77 -> s(T100)\nX146 -> T101\nT82 -> s(T101)\nT74 -> T103\nX147 -> T103\nT102 -> T103", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 120 [arrowhead = none ];
120 -> 32;

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

122 [label="EVAL with clause\nsub(X156, 0, X156).\nand substitution\nT77 -> T109\nX156 -> T109\nT82 -> 0\nT74 -> T109", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 122 [arrowhead = none ];
122 -> 34;

123 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 123 [arrowhead = none ];
123 -> 35;

124 [label="INSTANCE with matching:\nT77 -> T100\nT82 -> T101\nT74 -> T103", fontsize=14, style = filled, fillcolor = lightgrey];
32 -> 124 [arrowhead = none , style=dashed];
124 -> 28[style=dashed];

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

126 [label="EVAL with clause\nevaluate(*(X174, X175), X176) :- ','(evaluate(X174, X177), ','(evaluate(X175, X178), mult(X177, X178, X176))).\nand substitution\nX174 -> T122\nX175 -> T123\nT6 -> *(T122, T123)\nT7 -> T125\nX176 -> T125\nT124 -> T125", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 126 [arrowhead = none ];
126 -> 39;

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

128 [label="EVAL with clause\nevaluate(X325, X325) :- myinteger(X325).\nand substitution\nT6 -> T203\nX325 -> T203\nT7 -> T203", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 128 [arrowhead = none ];
128 -> 73;

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

130 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
39 -> 130 [arrowhead = none ];
130 -> 41;

131 [label="SPLIT 2\nnew knowledge:\nT128 is ground\nreplacements:\nX177 -> T128", fontsize=14, style = filled, fillcolor = violet];
39 -> 131 [arrowhead = none ];
131 -> 42;

132 [label="INSTANCE with matching:\nT6 -> T122\nT7 -> X177", fontsize=14, style = filled, fillcolor = lightgrey];
41 -> 132 [arrowhead = none , style=dashed];
132 -> 3[style=dashed];

133 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
42 -> 133 [arrowhead = none ];
133 -> 43;

134 [label="SPLIT 2\nnew knowledge:\nT133 is ground\nreplacements:\nX178 -> T133", fontsize=14, style = filled, fillcolor = violet];
42 -> 134 [arrowhead = none ];
134 -> 44;

135 [label="INSTANCE with matching:\nT6 -> T123\nT7 -> X178", fontsize=14, style = filled, fillcolor = lightgrey];
43 -> 135 [arrowhead = none , style=dashed];
135 -> 3[style=dashed];

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

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

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

139 [label="EVAL with clause\nmult(s(X224), X225, X226) :- ','(mult(X224, X225, X227), add(X225, X227, X226)).\nand substitution\nX224 -> T151\nT128 -> s(T151)\nT133 -> T152\nX225 -> T152\nT125 -> T154\nX226 -> T154\nT153 -> T154", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 139 [arrowhead = none ];
139 -> 48;

140 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 140 [arrowhead = none ];
140 -> 49;

141 [label="EVAL with clause\nmult(0, X321, 0).\nand substitution\nT128 -> 0\nT133 -> T200\nX321 -> T200\nT125 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 141 [arrowhead = none ];
141 -> 70;

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

143 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
48 -> 143 [arrowhead = none ];
143 -> 50;

144 [label="SPLIT 2\nnew knowledge:\nT157 is ground\nreplacements:\nX227 -> T157", fontsize=14, style = filled, fillcolor = violet];
48 -> 144 [arrowhead = none ];
144 -> 51;

145 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
50 -> 145 [arrowhead = none ];
145 -> 52;

146 [label="INSTANCE with matching:\nT26 -> T152\nT31 -> T157\nT23 -> T154", fontsize=14, style = filled, fillcolor = lightgrey];
51 -> 146 [arrowhead = none , style=dashed];
146 -> 12[style=dashed];

147 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
52 -> 147 [arrowhead = none ];
147 -> 53;

148 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
52 -> 148 [arrowhead = none ];
148 -> 54;

149 [label="EVAL with clause\nmult(s(X259), X260, X261) :- ','(mult(X259, X260, X262), add(X260, X262, X261)).\nand substitution\nX259 -> T168\nT151 -> s(T168)\nT152 -> T169\nX260 -> T169\nX227 -> X263\nX261 -> X263", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 149 [arrowhead = none ];
149 -> 55;

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

151 [label="EVAL with clause\nmult(0, X314, 0).\nand substitution\nT151 -> 0\nT152 -> T194\nX314 -> T194\nX227 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 151 [arrowhead = none ];
151 -> 67;

152 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 152 [arrowhead = none ];
152 -> 68;

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

154 [label="SPLIT 2\nnew knowledge:\nT172 is ground\nreplacements:\nX262 -> T172", fontsize=14, style = filled, fillcolor = violet];
55 -> 154 [arrowhead = none ];
154 -> 58;

155 [label="INSTANCE with matching:\nT151 -> T168\nT152 -> T169\nX227 -> X262", fontsize=14, style = filled, fillcolor = lightgrey];
57 -> 155 [arrowhead = none , style=dashed];
155 -> 50[style=dashed];

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

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

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

159 [label="EVAL with clause\nadd(s(X297), X298, s(X299)) :- add(X297, X298, X299).\nand substitution\nX297 -> T185\nT169 -> s(T185)\nT172 -> T186\nX298 -> T186\nX299 -> X300\nX263 -> s(X300)", fontsize=14, style = filled, fillcolor = lightblue];
60 -> 159 [arrowhead = none ];
159 -> 62;

160 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
60 -> 160 [arrowhead = none ];
160 -> 63;

161 [label="EVAL with clause\nadd(0, X310, X310).\nand substitution\nT169 -> 0\nT172 -> T191\nX310 -> T191\nX263 -> T191", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 161 [arrowhead = none ];
161 -> 64;

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

163 [label="INSTANCE with matching:\nT169 -> T185\nT172 -> T186\nX263 -> X300", fontsize=14, style = filled, fillcolor = lightgrey];
62 -> 163 [arrowhead = none , style=dashed];
163 -> 58[style=dashed];

164 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
64 -> 164 [arrowhead = none ];
164 -> 66;

165 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
67 -> 165 [arrowhead = none ];
165 -> 69;

166 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
70 -> 166 [arrowhead = none ];
166 -> 72;

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

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

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

170 [label="EVAL with clause\nmyinteger(s(X332)) :- myinteger(X332).\nand substitution\nX332 -> T209\nT203 -> s(T209)", fontsize=14, style = filled, fillcolor = lightblue];
76 -> 170 [arrowhead = none ];
170 -> 78;

171 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
76 -> 171 [arrowhead = none ];
171 -> 79;

172 [label="EVAL with clause\nmyinteger(0).\nand substitution\nT203 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
77 -> 172 [arrowhead = none ];
172 -> 80;

173 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
77 -> 173 [arrowhead = none ];
173 -> 81;

174 [label="INSTANCE with matching:\nT203 -> T209", fontsize=14, style = filled, fillcolor = lightgrey];
78 -> 174 [arrowhead = none , style=dashed];
174 -> 73[style=dashed];

175 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
80 -> 175 [arrowhead = none ];
175 -> 82;

}

(2) Obligation:

Triples:

evaluate3(+(T20, T21), T23) :- evaluate3(T20, X25).
evaluate3(+(T20, T21), T23) :- ','(evaluatec3(T20, T26), evaluate3(T21, X26)).
evaluate3(+(T20, T21), T23) :- ','(evaluatec3(T20, T26), ','(evaluatec3(T21, T31), add12(T26, T31, T23))).
evaluate3(-(T71, T72), T74) :- evaluate3(T71, X101).
evaluate3(-(T71, T72), T74) :- ','(evaluatec3(T71, T77), evaluate3(T72, X102)).
evaluate3(-(T71, T72), T74) :- ','(evaluatec3(T71, T77), ','(evaluatec3(T72, T82), sub28(T77, T82, T74))).
evaluate3(*(T122, T123), T125) :- evaluate3(T122, X177).
evaluate3(*(T122, T123), T125) :- ','(evaluatec3(T122, T128), evaluate3(T123, X178)).
evaluate3(*(T122, T123), T154) :- ','(evaluatec3(T122, s(T151)), ','(evaluatec3(T123, T152), mult50(T151, T152, X227))).
evaluate3(*(T122, T123), T154) :- ','(evaluatec3(T122, s(T151)), ','(evaluatec3(T123, T152), ','(multc50(T151, T152, T157), add12(T152, T157, T154)))).
evaluate3(T203, T203) :- myinteger73(T203).
add12(s(T49), T50, s(T52)) :- add12(T49, T50, T52).
sub28(s(T100), s(T101), T103) :- sub28(T100, T101, T103).
mult50(s(T168), T169, X263) :- mult50(T168, T169, X262).
mult50(s(T168), T169, X263) :- ','(multc50(T168, T169, T172), add58(T169, T172, X263)).
add58(s(T185), T186, s(X300)) :- add58(T185, T186, X300).
myinteger73(s(T209)) :- myinteger73(T209).
myis1(T7, T6) :- evaluate3(T6, T7).

Clauses:

evaluatec3(+(T20, T21), T23) :- ','(evaluatec3(T20, T26), ','(evaluatec3(T21, T31), addc12(T26, T31, T23))).
evaluatec3(-(T71, T72), T74) :- ','(evaluatec3(T71, T77), ','(evaluatec3(T72, T82), subc28(T77, T82, T74))).
evaluatec3(*(T122, T123), T154) :- ','(evaluatec3(T122, s(T151)), ','(evaluatec3(T123, T152), ','(multc50(T151, T152, T157), addc12(T152, T157, T154)))).
evaluatec3(*(T122, T123), 0) :- ','(evaluatec3(T122, 0), evaluatec3(T123, T200)).
evaluatec3(T203, T203) :- myintegerc73(T203).
addc12(s(T49), T50, s(T52)) :- addc12(T49, T50, T52).
addc12(0, T58, T58).
subc28(s(T100), s(T101), T103) :- subc28(T100, T101, T103).
subc28(T109, 0, T109).
multc50(s(T168), T169, X263) :- ','(multc50(T168, T169, T172), addc58(T169, T172, X263)).
multc50(0, T194, 0).
addc58(s(T185), T186, s(X300)) :- addc58(T185, T186, X300).
addc58(0, T191, T191).
myintegerc73(s(T209)) :- myintegerc73(T209).
myintegerc73(0).

Afs:

myis1(x1, x2) = myis1(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:
myis1_in: (f,b)
evaluate3_in: (b,f)
evaluatec3_in: (b,f) (b,b)
myintegerc73_in: (b)
addc12_in: (b,b,b) (b,b,f)
subc28_in: (b,b,b) (b,b,f)
multc50_in: (b,b,f)
addc58_in: (b,b,f)
mult50_in: (b,b,f)
add58_in: (b,b,f)
add12_in: (b,b,f)
myinteger73_in: (b)
sub28_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

MYIS1_IN_AG(T7, T6) → U27_AG(T7, T6, evaluate3_in_ga(T6, T7))
MYIS1_IN_AG(T7, T6) → EVALUATE3_IN_GA(T6, T7)
EVALUATE3_IN_GA(+(T20, T21), T23) → U1_GA(T20, T21, T23, evaluate3_in_ga(T20, X25))
EVALUATE3_IN_GA(+(T20, T21), T23) → EVALUATE3_IN_GA(T20, X25)
EVALUATE3_IN_GA(+(T20, T21), T23) → U2_GA(T20, T21, T23, evaluatec3_in_ga(T20, T26))
U2_GA(T20, T21, T23, evaluatec3_out_ga(T20, T26)) → U3_GA(T20, T21, T23, evaluate3_in_ga(T21, X26))
U2_GA(T20, T21, T23, evaluatec3_out_ga(T20, T26)) → EVALUATE3_IN_GA(T21, X26)
EVALUATE3_IN_GA(-(T71, T72), T74) → U6_GA(T71, T72, T74, evaluate3_in_ga(T71, X101))
EVALUATE3_IN_GA(-(T71, T72), T74) → EVALUATE3_IN_GA(T71, X101)
EVALUATE3_IN_GA(-(T71, T72), T74) → U7_GA(T71, T72, T74, evaluatec3_in_ga(T71, T77))
U7_GA(T71, T72, T74, evaluatec3_out_ga(T71, T77)) → U8_GA(T71, T72, T74, evaluate3_in_ga(T72, X102))
U7_GA(T71, T72, T74, evaluatec3_out_ga(T71, T77)) → EVALUATE3_IN_GA(T72, X102)
EVALUATE3_IN_GA(*(T122, T123), T125) → U11_GA(T122, T123, T125, evaluate3_in_ga(T122, X177))
EVALUATE3_IN_GA(*(T122, T123), T125) → EVALUATE3_IN_GA(T122, X177)
EVALUATE3_IN_GA(*(T122, T123), T125) → U12_GA(T122, T123, T125, evaluatec3_in_ga(T122, T128))
U12_GA(T122, T123, T125, evaluatec3_out_ga(T122, T128)) → U13_GA(T122, T123, T125, evaluate3_in_ga(T123, X178))
U12_GA(T122, T123, T125, evaluatec3_out_ga(T122, T128)) → EVALUATE3_IN_GA(T123, X178)
EVALUATE3_IN_GA(*(T122, T123), T154) → U14_GA(T122, T123, T154, evaluatec3_in_ga(T122, s(T151)))
U14_GA(T122, T123, T154, evaluatec3_out_ga(T122, s(T151))) → U15_GA(T122, T123, T154, T151, evaluatec3_in_ga(T123, T152))
U15_GA(T122, T123, T154, T151, evaluatec3_out_ga(T123, T152)) → U16_GA(T122, T123, T154, mult50_in_gga(T151, T152, X227))
U15_GA(T122, T123, T154, T151, evaluatec3_out_ga(T123, T152)) → MULT50_IN_GGA(T151, T152, X227)
MULT50_IN_GGA(s(T168), T169, X263) → U22_GGA(T168, T169, X263, mult50_in_gga(T168, T169, X262))
MULT50_IN_GGA(s(T168), T169, X263) → MULT50_IN_GGA(T168, T169, X262)
MULT50_IN_GGA(s(T168), T169, X263) → U23_GGA(T168, T169, X263, multc50_in_gga(T168, T169, T172))
U23_GGA(T168, T169, X263, multc50_out_gga(T168, T169, T172)) → U24_GGA(T168, T169, X263, add58_in_gga(T169, T172, X263))
U23_GGA(T168, T169, X263, multc50_out_gga(T168, T169, T172)) → ADD58_IN_GGA(T169, T172, X263)
ADD58_IN_GGA(s(T185), T186, s(X300)) → U25_GGA(T185, T186, X300, add58_in_gga(T185, T186, X300))
ADD58_IN_GGA(s(T185), T186, s(X300)) → ADD58_IN_GGA(T185, T186, X300)
U15_GA(T122, T123, T154, T151, evaluatec3_out_ga(T123, T152)) → U17_GA(T122, T123, T154, T152, multc50_in_gga(T151, T152, T157))
U17_GA(T122, T123, T154, T152, multc50_out_gga(T151, T152, T157)) → U18_GA(T122, T123, T154, add12_in_gga(T152, T157, T154))
U17_GA(T122, T123, T154, T152, multc50_out_gga(T151, T152, T157)) → ADD12_IN_GGA(T152, T157, T154)
ADD12_IN_GGA(s(T49), T50, s(T52)) → U20_GGA(T49, T50, T52, add12_in_gga(T49, T50, T52))
ADD12_IN_GGA(s(T49), T50, s(T52)) → ADD12_IN_GGA(T49, T50, T52)
EVALUATE3_IN_GA(T203, T203) → U19_GA(T203, myinteger73_in_g(T203))
EVALUATE3_IN_GA(T203, T203) → MYINTEGER73_IN_G(T203)
MYINTEGER73_IN_G(s(T209)) → U26_G(T209, myinteger73_in_g(T209))
MYINTEGER73_IN_G(s(T209)) → MYINTEGER73_IN_G(T209)
U7_GA(T71, T72, T74, evaluatec3_out_ga(T71, T77)) → U9_GA(T71, T72, T74, T77, evaluatec3_in_ga(T72, T82))
U9_GA(T71, T72, T74, T77, evaluatec3_out_ga(T72, T82)) → U10_GA(T71, T72, T74, sub28_in_gga(T77, T82, T74))
U9_GA(T71, T72, T74, T77, evaluatec3_out_ga(T72, T82)) → SUB28_IN_GGA(T77, T82, T74)
SUB28_IN_GGA(s(T100), s(T101), T103) → U21_GGA(T100, T101, T103, sub28_in_gga(T100, T101, T103))
SUB28_IN_GGA(s(T100), s(T101), T103) → SUB28_IN_GGA(T100, T101, T103)
U2_GA(T20, T21, T23, evaluatec3_out_ga(T20, T26)) → U4_GA(T20, T21, T23, T26, evaluatec3_in_ga(T21, T31))
U4_GA(T20, T21, T23, T26, evaluatec3_out_ga(T21, T31)) → U5_GA(T20, T21, T23, add12_in_gga(T26, T31, T23))
U4_GA(T20, T21, T23, T26, evaluatec3_out_ga(T21, T31)) → ADD12_IN_GGA(T26, T31, T23)

The TRS R consists of the following rules:

evaluatec3_in_ga(+(T20, T21), T23) → U29_ga(T20, T21, T23, evaluatec3_in_ga(T20, T26))
evaluatec3_in_ga(-(T71, T72), T74) → U32_ga(T71, T72, T74, evaluatec3_in_ga(T71, T77))
evaluatec3_in_ga(*(T122, T123), T154) → U35_ga(T122, T123, T154, evaluatec3_in_ga(T122, s(T151)))
evaluatec3_in_ga(*(T122, T123), 0) → U39_ga(T122, T123, evaluatec3_in_gg(T122, 0))
evaluatec3_in_gg(+(T20, T21), T23) → U29_gg(T20, T21, T23, evaluatec3_in_ga(T20, T26))
evaluatec3_in_ga(T203, T203) → U41_ga(T203, myintegerc73_in_g(T203))
myintegerc73_in_g(s(T209)) → U47_g(T209, myintegerc73_in_g(T209))
myintegerc73_in_g(0) → myintegerc73_out_g(0)
U47_g(T209, myintegerc73_out_g(T209)) → myintegerc73_out_g(s(T209))
U41_ga(T203, myintegerc73_out_g(T203)) → evaluatec3_out_ga(T203, T203)
U29_gg(T20, T21, T23, evaluatec3_out_ga(T20, T26)) → U30_gg(T20, T21, T23, T26, evaluatec3_in_ga(T21, T31))
U30_gg(T20, T21, T23, T26, evaluatec3_out_ga(T21, T31)) → U31_gg(T20, T21, T23, addc12_in_ggg(T26, T31, T23))
addc12_in_ggg(s(T49), T50, s(T52)) → U42_ggg(T49, T50, T52, addc12_in_ggg(T49, T50, T52))
addc12_in_ggg(0, T58, T58) → addc12_out_ggg(0, T58, T58)
U42_ggg(T49, T50, T52, addc12_out_ggg(T49, T50, T52)) → addc12_out_ggg(s(T49), T50, s(T52))
U31_gg(T20, T21, T23, addc12_out_ggg(T26, T31, T23)) → evaluatec3_out_gg(+(T20, T21), T23)
evaluatec3_in_gg(-(T71, T72), T74) → U32_gg(T71, T72, T74, evaluatec3_in_ga(T71, T77))
U32_gg(T71, T72, T74, evaluatec3_out_ga(T71, T77)) → U33_gg(T71, T72, T74, T77, evaluatec3_in_ga(T72, T82))
U33_gg(T71, T72, T74, T77, evaluatec3_out_ga(T72, T82)) → U34_gg(T71, T72, T74, subc28_in_ggg(T77, T82, T74))
subc28_in_ggg(s(T100), s(T101), T103) → U43_ggg(T100, T101, T103, subc28_in_ggg(T100, T101, T103))
subc28_in_ggg(T109, 0, T109) → subc28_out_ggg(T109, 0, T109)
U43_ggg(T100, T101, T103, subc28_out_ggg(T100, T101, T103)) → subc28_out_ggg(s(T100), s(T101), T103)
U34_gg(T71, T72, T74, subc28_out_ggg(T77, T82, T74)) → evaluatec3_out_gg(-(T71, T72), T74)
evaluatec3_in_gg(*(T122, T123), T154) → U35_gg(T122, T123, T154, evaluatec3_in_ga(T122, s(T151)))
U35_gg(T122, T123, T154, evaluatec3_out_ga(T122, s(T151))) → U36_gg(T122, T123, T154, T151, evaluatec3_in_ga(T123, T152))
U36_gg(T122, T123, T154, T151, evaluatec3_out_ga(T123, T152)) → U37_gg(T122, T123, T154, T152, multc50_in_gga(T151, T152, T157))
multc50_in_gga(s(T168), T169, X263) → U44_gga(T168, T169, X263, multc50_in_gga(T168, T169, T172))
multc50_in_gga(0, T194, 0) → multc50_out_gga(0, T194, 0)
U44_gga(T168, T169, X263, multc50_out_gga(T168, T169, T172)) → U45_gga(T168, T169, X263, addc58_in_gga(T169, T172, X263))
addc58_in_gga(s(T185), T186, s(X300)) → U46_gga(T185, T186, X300, addc58_in_gga(T185, T186, X300))
addc58_in_gga(0, T191, T191) → addc58_out_gga(0, T191, T191)
U46_gga(T185, T186, X300, addc58_out_gga(T185, T186, X300)) → addc58_out_gga(s(T185), T186, s(X300))
U45_gga(T168, T169, X263, addc58_out_gga(T169, T172, X263)) → multc50_out_gga(s(T168), T169, X263)
U37_gg(T122, T123, T154, T152, multc50_out_gga(T151, T152, T157)) → U38_gg(T122, T123, T154, addc12_in_ggg(T152, T157, T154))
U38_gg(T122, T123, T154, addc12_out_ggg(T152, T157, T154)) → evaluatec3_out_gg(*(T122, T123), T154)
evaluatec3_in_gg(*(T122, T123), 0) → U39_gg(T122, T123, evaluatec3_in_gg(T122, 0))
evaluatec3_in_gg(T203, T203) → U41_gg(T203, myintegerc73_in_g(T203))
U41_gg(T203, myintegerc73_out_g(T203)) → evaluatec3_out_gg(T203, T203)
U39_gg(T122, T123, evaluatec3_out_gg(T122, 0)) → U40_gg(T122, T123, evaluatec3_in_ga(T123, T200))
U40_gg(T122, T123, evaluatec3_out_ga(T123, T200)) → evaluatec3_out_gg(*(T122, T123), 0)
U39_ga(T122, T123, evaluatec3_out_gg(T122, 0)) → U40_ga(T122, T123, evaluatec3_in_ga(T123, T200))
U40_ga(T122, T123, evaluatec3_out_ga(T123, T200)) → evaluatec3_out_ga(*(T122, T123), 0)
U35_ga(T122, T123, T154, evaluatec3_out_ga(T122, s(T151))) → U36_ga(T122, T123, T154, T151, evaluatec3_in_ga(T123, T152))
U36_ga(T122, T123, T154, T151, evaluatec3_out_ga(T123, T152)) → U37_ga(T122, T123, T154, T152, multc50_in_gga(T151, T152, T157))
U37_ga(T122, T123, T154, T152, multc50_out_gga(T151, T152, T157)) → U38_ga(T122, T123, T154, addc12_in_gga(T152, T157, T154))
addc12_in_gga(s(T49), T50, s(T52)) → U42_gga(T49, T50, T52, addc12_in_gga(T49, T50, T52))
addc12_in_gga(0, T58, T58) → addc12_out_gga(0, T58, T58)
U42_gga(T49, T50, T52, addc12_out_gga(T49, T50, T52)) → addc12_out_gga(s(T49), T50, s(T52))
U38_ga(T122, T123, T154, addc12_out_gga(T152, T157, T154)) → evaluatec3_out_ga(*(T122, T123), T154)
U32_ga(T71, T72, T74, evaluatec3_out_ga(T71, T77)) → U33_ga(T71, T72, T74, T77, evaluatec3_in_ga(T72, T82))
U33_ga(T71, T72, T74, T77, evaluatec3_out_ga(T72, T82)) → U34_ga(T71, T72, T74, subc28_in_gga(T77, T82, T74))
subc28_in_gga(s(T100), s(T101), T103) → U43_gga(T100, T101, T103, subc28_in_gga(T100, T101, T103))
subc28_in_gga(T109, 0, T109) → subc28_out_gga(T109, 0, T109)
U43_gga(T100, T101, T103, subc28_out_gga(T100, T101, T103)) → subc28_out_gga(s(T100), s(T101), T103)
U34_ga(T71, T72, T74, subc28_out_gga(T77, T82, T74)) → evaluatec3_out_ga(-(T71, T72), T74)
U29_ga(T20, T21, T23, evaluatec3_out_ga(T20, T26)) → U30_ga(T20, T21, T23, T26, evaluatec3_in_ga(T21, T31))
U30_ga(T20, T21, T23, T26, evaluatec3_out_ga(T21, T31)) → U31_ga(T20, T21, T23, addc12_in_gga(T26, T31, T23))
U31_ga(T20, T21, T23, addc12_out_gga(T26, T31, T23)) → evaluatec3_out_ga(+(T20, T21), T23)

The argument filtering Pi contains the following mapping:
evaluate3_in_ga(x1, x2) = evaluate3_in_ga(x1)
+(x1, x2) = +(x1, x2)
evaluatec3_in_ga(x1, x2) = evaluatec3_in_ga(x1)
U29_ga(x1, x2, x3, x4) = U29_ga(x1, x2, x4)
-(x1, x2) = -(x1, x2)
U32_ga(x1, x2, x3, x4) = U32_ga(x1, x2, x4)
*(x1, x2) = *(x1, x2)
U35_ga(x1, x2, x3, x4) = U35_ga(x1, x2, x4)
U39_ga(x1, x2, x3) = U39_ga(x1, x2, x3)
evaluatec3_in_gg(x1, x2) = evaluatec3_in_gg(x1, x2)
U29_gg(x1, x2, x3, x4) = U29_gg(x1, x2, x3, x4)
U41_ga(x1, x2) = U41_ga(x1, x2)
myintegerc73_in_g(x1) = myintegerc73_in_g(x1)
s(x1) = s(x1)
U47_g(x1, x2) = U47_g(x1, x2)
0 = 0
myintegerc73_out_g(x1) = myintegerc73_out_g(x1)
evaluatec3_out_ga(x1, x2) = evaluatec3_out_ga(x1, x2)
U30_gg(x1, x2, x3, x4, x5) = U30_gg(x1, x2, x3, x4, x5)
U31_gg(x1, x2, x3, x4) = U31_gg(x1, x2, x3, x4)
addc12_in_ggg(x1, x2, x3) = addc12_in_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3, x4) = U42_ggg(x1, x2, x3, x4)
addc12_out_ggg(x1, x2, x3) = addc12_out_ggg(x1, x2, x3)
evaluatec3_out_gg(x1, x2) = evaluatec3_out_gg(x1, x2)
U32_gg(x1, x2, x3, x4) = U32_gg(x1, x2, x3, x4)
U33_gg(x1, x2, x3, x4, x5) = U33_gg(x1, x2, x3, x4, x5)
U34_gg(x1, x2, x3, x4) = U34_gg(x1, x2, x3, x4)
subc28_in_ggg(x1, x2, x3) = subc28_in_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3, x4) = U43_ggg(x1, x2, x3, x4)
subc28_out_ggg(x1, x2, x3) = subc28_out_ggg(x1, x2, x3)
U35_gg(x1, x2, x3, x4) = U35_gg(x1, x2, x3, x4)
U36_gg(x1, x2, x3, x4, x5) = U36_gg(x1, x2, x3, x4, x5)
U37_gg(x1, x2, x3, x4, x5) = U37_gg(x1, x2, x3, x4, x5)
multc50_in_gga(x1, x2, x3) = multc50_in_gga(x1, x2)
U44_gga(x1, x2, x3, x4) = U44_gga(x1, x2, x4)
multc50_out_gga(x1, x2, x3) = multc50_out_gga(x1, x2, x3)
U45_gga(x1, x2, x3, x4) = U45_gga(x1, x2, x4)
addc58_in_gga(x1, x2, x3) = addc58_in_gga(x1, x2)
U46_gga(x1, x2, x3, x4) = U46_gga(x1, x2, x4)
addc58_out_gga(x1, x2, x3) = addc58_out_gga(x1, x2, x3)
U38_gg(x1, x2, x3, x4) = U38_gg(x1, x2, x3, x4)
U39_gg(x1, x2, x3) = U39_gg(x1, x2, x3)
U41_gg(x1, x2) = U41_gg(x1, x2)
U40_gg(x1, x2, x3) = U40_gg(x1, x2, x3)
U40_ga(x1, x2, x3) = U40_ga(x1, x2, x3)
U36_ga(x1, x2, x3, x4, x5) = U36_ga(x1, x2, x4, x5)
U37_ga(x1, x2, x3, x4, x5) = U37_ga(x1, x2, x4, x5)
U38_ga(x1, x2, x3, x4) = U38_ga(x1, x2, x4)
addc12_in_gga(x1, x2, x3) = addc12_in_gga(x1, x2)
U42_gga(x1, x2, x3, x4) = U42_gga(x1, x2, x4)
addc12_out_gga(x1, x2, x3) = addc12_out_gga(x1, x2, x3)
U33_ga(x1, x2, x3, x4, x5) = U33_ga(x1, x2, x4, x5)
U34_ga(x1, x2, x3, x4) = U34_ga(x1, x2, x4)
subc28_in_gga(x1, x2, x3) = subc28_in_gga(x1, x2)
U43_gga(x1, x2, x3, x4) = U43_gga(x1, x2, x4)
subc28_out_gga(x1, x2, x3) = subc28_out_gga(x1, x2, x3)
U30_ga(x1, x2, x3, x4, x5) = U30_ga(x1, x2, x4, x5)
U31_ga(x1, x2, x3, x4) = U31_ga(x1, x2, x4)
mult50_in_gga(x1, x2, x3) = mult50_in_gga(x1, x2)
add58_in_gga(x1, x2, x3) = add58_in_gga(x1, x2)
add12_in_gga(x1, x2, x3) = add12_in_gga(x1, x2)
myinteger73_in_g(x1) = myinteger73_in_g(x1)
sub28_in_gga(x1, x2, x3) = sub28_in_gga(x1, x2)
MYIS1_IN_AG(x1, x2) = MYIS1_IN_AG(x2)
U27_AG(x1, x2, x3) = U27_AG(x2, x3)
EVALUATE3_IN_GA(x1, x2) = EVALUATE3_IN_GA(x1)
U1_GA(x1, x2, x3, x4) = U1_GA(x1, x2, x4)
U2_GA(x1, x2, x3, x4) = U2_GA(x1, x2, x4)
U3_GA(x1, x2, x3, x4) = U3_GA(x1, x2, x4)
U6_GA(x1, x2, x3, x4) = U6_GA(x1, x2, x4)
U7_GA(x1, x2, x3, x4) = U7_GA(x1, x2, x4)
U8_GA(x1, x2, x3, x4) = U8_GA(x1, x2, x4)
U11_GA(x1, x2, x3, x4) = U11_GA(x1, x2, x4)
U12_GA(x1, x2, x3, x4) = U12_GA(x1, x2, x4)
U13_GA(x1, x2, x3, x4) = U13_GA(x1, x2, x4)
U14_GA(x1, x2, x3, x4) = U14_GA(x1, x2, x4)
U15_GA(x1, x2, x3, x4, x5) = U15_GA(x1, x2, x4, x5)
U16_GA(x1, x2, x3, x4) = U16_GA(x1, x2, x4)
MULT50_IN_GGA(x1, x2, x3) = MULT50_IN_GGA(x1, x2)
U22_GGA(x1, x2, x3, x4) = U22_GGA(x1, x2, x4)
U23_GGA(x1, x2, x3, x4) = U23_GGA(x1, x2, x4)
U24_GGA(x1, x2, x3, x4) = U24_GGA(x1, x2, x4)
ADD58_IN_GGA(x1, x2, x3) = ADD58_IN_GGA(x1, x2)
U25_GGA(x1, x2, x3, x4) = U25_GGA(x1, x2, x4)
U17_GA(x1, x2, x3, x4, x5) = U17_GA(x1, x2, x4, x5)
U18_GA(x1, x2, x3, x4) = U18_GA(x1, x2, x4)
ADD12_IN_GGA(x1, x2, x3) = ADD12_IN_GGA(x1, x2)
U20_GGA(x1, x2, x3, x4) = U20_GGA(x1, x2, x4)
U19_GA(x1, x2) = U19_GA(x1, x2)
MYINTEGER73_IN_G(x1) = MYINTEGER73_IN_G(x1)
U26_G(x1, x2) = U26_G(x1, x2)
U9_GA(x1, x2, x3, x4, x5) = U9_GA(x1, x2, x4, x5)
U10_GA(x1, x2, x3, x4) = U10_GA(x1, x2, x4)
SUB28_IN_GGA(x1, x2, x3) = SUB28_IN_GGA(x1, x2)
U21_GGA(x1, x2, x3, x4) = U21_GGA(x1, x2, x4)
U4_GA(x1, x2, x3, x4, x5) = U4_GA(x1, x2, x4, x5)
U5_GA(x1, x2, x3, x4) = U5_GA(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:

MYIS1_IN_AG(T7, T6) → U27_AG(T7, T6, evaluate3_in_ga(T6, T7))
MYIS1_IN_AG(T7, T6) → EVALUATE3_IN_GA(T6, T7)
EVALUATE3_IN_GA(+(T20, T21), T23) → U1_GA(T20, T21, T23, evaluate3_in_ga(T20, X25))
EVALUATE3_IN_GA(+(T20, T21), T23) → EVALUATE3_IN_GA(T20, X25)
EVALUATE3_IN_GA(+(T20, T21), T23) → U2_GA(T20, T21, T23, evaluatec3_in_ga(T20, T26))
U2_GA(T20, T21, T23, evaluatec3_out_ga(T20, T26)) → U3_GA(T20, T21, T23, evaluate3_in_ga(T21, X26))
U2_GA(T20, T21, T23, evaluatec3_out_ga(T20, T26)) → EVALUATE3_IN_GA(T21, X26)
EVALUATE3_IN_GA(-(T71, T72), T74) → U6_GA(T71, T72, T74, evaluate3_in_ga(T71, X101))
EVALUATE3_IN_GA(-(T71, T72), T74) → EVALUATE3_IN_GA(T71, X101)
EVALUATE3_IN_GA(-(T71, T72), T74) → U7_GA(T71, T72, T74, evaluatec3_in_ga(T71, T77))
U7_GA(T71, T72, T74, evaluatec3_out_ga(T71, T77)) → U8_GA(T71, T72, T74, evaluate3_in_ga(T72, X102))
U7_GA(T71, T72, T74, evaluatec3_out_ga(T71, T77)) → EVALUATE3_IN_GA(T72, X102)
EVALUATE3_IN_GA(*(T122, T123), T125) → U11_GA(T122, T123, T125, evaluate3_in_ga(T122, X177))
EVALUATE3_IN_GA(*(T122, T123), T125) → EVALUATE3_IN_GA(T122, X177)
EVALUATE3_IN_GA(*(T122, T123), T125) → U12_GA(T122, T123, T125, evaluatec3_in_ga(T122, T128))
U12_GA(T122, T123, T125, evaluatec3_out_ga(T122, T128)) → U13_GA(T122, T123, T125, evaluate3_in_ga(T123, X178))
U12_GA(T122, T123, T125, evaluatec3_out_ga(T122, T128)) → EVALUATE3_IN_GA(T123, X178)
EVALUATE3_IN_GA(*(T122, T123), T154) → U14_GA(T122, T123, T154, evaluatec3_in_ga(T122, s(T151)))
U14_GA(T122, T123, T154, evaluatec3_out_ga(T122, s(T151))) → U15_GA(T122, T123, T154, T151, evaluatec3_in_ga(T123, T152))
U15_GA(T122, T123, T154, T151, evaluatec3_out_ga(T123, T152)) → U16_GA(T122, T123, T154, mult50_in_gga(T151, T152, X227))
U15_GA(T122, T123, T154, T151, evaluatec3_out_ga(T123, T152)) → MULT50_IN_GGA(T151, T152, X227)
MULT50_IN_GGA(s(T168), T169, X263) → U22_GGA(T168, T169, X263, mult50_in_gga(T168, T169, X262))
MULT50_IN_GGA(s(T168), T169, X263) → MULT50_IN_GGA(T168, T169, X262)
MULT50_IN_GGA(s(T168), T169, X263) → U23_GGA(T168, T169, X263, multc50_in_gga(T168, T169, T172))
U23_GGA(T168, T169, X263, multc50_out_gga(T168, T169, T172)) → U24_GGA(T168, T169, X263, add58_in_gga(T169, T172, X263))
U23_GGA(T168, T169, X263, multc50_out_gga(T168, T169, T172)) → ADD58_IN_GGA(T169, T172, X263)
ADD58_IN_GGA(s(T185), T186, s(X300)) → U25_GGA(T185, T186, X300, add58_in_gga(T185, T186, X300))
ADD58_IN_GGA(s(T185), T186, s(X300)) → ADD58_IN_GGA(T185, T186, X300)
U15_GA(T122, T123, T154, T151, evaluatec3_out_ga(T123, T152)) → U17_GA(T122, T123, T154, T152, multc50_in_gga(T151, T152, T157))
U17_GA(T122, T123, T154, T152, multc50_out_gga(T151, T152, T157)) → U18_GA(T122, T123, T154, add12_in_gga(T152, T157, T154))
U17_GA(T122, T123, T154, T152, multc50_out_gga(T151, T152, T157)) → ADD12_IN_GGA(T152, T157, T154)
ADD12_IN_GGA(s(T49), T50, s(T52)) → U20_GGA(T49, T50, T52, add12_in_gga(T49, T50, T52))
ADD12_IN_GGA(s(T49), T50, s(T52)) → ADD12_IN_GGA(T49, T50, T52)
EVALUATE3_IN_GA(T203, T203) → U19_GA(T203, myinteger73_in_g(T203))
EVALUATE3_IN_GA(T203, T203) → MYINTEGER73_IN_G(T203)
MYINTEGER73_IN_G(s(T209)) → U26_G(T209, myinteger73_in_g(T209))
MYINTEGER73_IN_G(s(T209)) → MYINTEGER73_IN_G(T209)
U7_GA(T71, T72, T74, evaluatec3_out_ga(T71, T77)) → U9_GA(T71, T72, T74, T77, evaluatec3_in_ga(T72, T82))
U9_GA(T71, T72, T74, T77, evaluatec3_out_ga(T72, T82)) → U10_GA(T71, T72, T74, sub28_in_gga(T77, T82, T74))
U9_GA(T71, T72, T74, T77, evaluatec3_out_ga(T72, T82)) → SUB28_IN_GGA(T77, T82, T74)
SUB28_IN_GGA(s(T100), s(T101), T103) → U21_GGA(T100, T101, T103, sub28_in_gga(T100, T101, T103))
SUB28_IN_GGA(s(T100), s(T101), T103) → SUB28_IN_GGA(T100, T101, T103)
U2_GA(T20, T21, T23, evaluatec3_out_ga(T20, T26)) → U4_GA(T20, T21, T23, T26, evaluatec3_in_ga(T21, T31))
U4_GA(T20, T21, T23, T26, evaluatec3_out_ga(T21, T31)) → U5_GA(T20, T21, T23, add12_in_gga(T26, T31, T23))
U4_GA(T20, T21, T23, T26, evaluatec3_out_ga(T21, T31)) → ADD12_IN_GGA(T26, T31, T23)

The TRS R consists of the following rules:

evaluatec3_in_ga(+(T20, T21), T23) → U29_ga(T20, T21, T23, evaluatec3_in_ga(T20, T26))
evaluatec3_in_ga(-(T71, T72), T74) → U32_ga(T71, T72, T74, evaluatec3_in_ga(T71, T77))
evaluatec3_in_ga(*(T122, T123), T154) → U35_ga(T122, T123, T154, evaluatec3_in_ga(T122, s(T151)))
evaluatec3_in_ga(*(T122, T123), 0) → U39_ga(T122, T123, evaluatec3_in_gg(T122, 0))
evaluatec3_in_gg(+(T20, T21), T23) → U29_gg(T20, T21, T23, evaluatec3_in_ga(T20, T26))
evaluatec3_in_ga(T203, T203) → U41_ga(T203, myintegerc73_in_g(T203))
myintegerc73_in_g(s(T209)) → U47_g(T209, myintegerc73_in_g(T209))
myintegerc73_in_g(0) → myintegerc73_out_g(0)
U47_g(T209, myintegerc73_out_g(T209)) → myintegerc73_out_g(s(T209))
U41_ga(T203, myintegerc73_out_g(T203)) → evaluatec3_out_ga(T203, T203)
U29_gg(T20, T21, T23, evaluatec3_out_ga(T20, T26)) → U30_gg(T20, T21, T23, T26, evaluatec3_in_ga(T21, T31))
U30_gg(T20, T21, T23, T26, evaluatec3_out_ga(T21, T31)) → U31_gg(T20, T21, T23, addc12_in_ggg(T26, T31, T23))
addc12_in_ggg(s(T49), T50, s(T52)) → U42_ggg(T49, T50, T52, addc12_in_ggg(T49, T50, T52))
addc12_in_ggg(0, T58, T58) → addc12_out_ggg(0, T58, T58)
U42_ggg(T49, T50, T52, addc12_out_ggg(T49, T50, T52)) → addc12_out_ggg(s(T49), T50, s(T52))
U31_gg(T20, T21, T23, addc12_out_ggg(T26, T31, T23)) → evaluatec3_out_gg(+(T20, T21), T23)
evaluatec3_in_gg(-(T71, T72), T74) → U32_gg(T71, T72, T74, evaluatec3_in_ga(T71, T77))
U32_gg(T71, T72, T74, evaluatec3_out_ga(T71, T77)) → U33_gg(T71, T72, T74, T77, evaluatec3_in_ga(T72, T82))
U33_gg(T71, T72, T74, T77, evaluatec3_out_ga(T72, T82)) → U34_gg(T71, T72, T74, subc28_in_ggg(T77, T82, T74))
subc28_in_ggg(s(T100), s(T101), T103) → U43_ggg(T100, T101, T103, subc28_in_ggg(T100, T101, T103))
subc28_in_ggg(T109, 0, T109) → subc28_out_ggg(T109, 0, T109)
U43_ggg(T100, T101, T103, subc28_out_ggg(T100, T101, T103)) → subc28_out_ggg(s(T100), s(T101), T103)
U34_gg(T71, T72, T74, subc28_out_ggg(T77, T82, T74)) → evaluatec3_out_gg(-(T71, T72), T74)
evaluatec3_in_gg(*(T122, T123), T154) → U35_gg(T122, T123, T154, evaluatec3_in_ga(T122, s(T151)))
U35_gg(T122, T123, T154, evaluatec3_out_ga(T122, s(T151))) → U36_gg(T122, T123, T154, T151, evaluatec3_in_ga(T123, T152))
U36_gg(T122, T123, T154, T151, evaluatec3_out_ga(T123, T152)) → U37_gg(T122, T123, T154, T152, multc50_in_gga(T151, T152, T157))
multc50_in_gga(s(T168), T169, X263) → U44_gga(T168, T169, X263, multc50_in_gga(T168, T169, T172))
multc50_in_gga(0, T194, 0) → multc50_out_gga(0, T194, 0)
U44_gga(T168, T169, X263, multc50_out_gga(T168, T169, T172)) → U45_gga(T168, T169, X263, addc58_in_gga(T169, T172, X263))
addc58_in_gga(s(T185), T186, s(X300)) → U46_gga(T185, T186, X300, addc58_in_gga(T185, T186, X300))
addc58_in_gga(0, T191, T191) → addc58_out_gga(0, T191, T191)
U46_gga(T185, T186, X300, addc58_out_gga(T185, T186, X300)) → addc58_out_gga(s(T185), T186, s(X300))
U45_gga(T168, T169, X263, addc58_out_gga(T169, T172, X263)) → multc50_out_gga(s(T168), T169, X263)
U37_gg(T122, T123, T154, T152, multc50_out_gga(T151, T152, T157)) → U38_gg(T122, T123, T154, addc12_in_ggg(T152, T157, T154))
U38_gg(T122, T123, T154, addc12_out_ggg(T152, T157, T154)) → evaluatec3_out_gg(*(T122, T123), T154)
evaluatec3_in_gg(*(T122, T123), 0) → U39_gg(T122, T123, evaluatec3_in_gg(T122, 0))
evaluatec3_in_gg(T203, T203) → U41_gg(T203, myintegerc73_in_g(T203))
U41_gg(T203, myintegerc73_out_g(T203)) → evaluatec3_out_gg(T203, T203)
U39_gg(T122, T123, evaluatec3_out_gg(T122, 0)) → U40_gg(T122, T123, evaluatec3_in_ga(T123, T200))
U40_gg(T122, T123, evaluatec3_out_ga(T123, T200)) → evaluatec3_out_gg(*(T122, T123), 0)
U39_ga(T122, T123, evaluatec3_out_gg(T122, 0)) → U40_ga(T122, T123, evaluatec3_in_ga(T123, T200))
U40_ga(T122, T123, evaluatec3_out_ga(T123, T200)) → evaluatec3_out_ga(*(T122, T123), 0)
U35_ga(T122, T123, T154, evaluatec3_out_ga(T122, s(T151))) → U36_ga(T122, T123, T154, T151, evaluatec3_in_ga(T123, T152))
U36_ga(T122, T123, T154, T151, evaluatec3_out_ga(T123, T152)) → U37_ga(T122, T123, T154, T152, multc50_in_gga(T151, T152, T157))
U37_ga(T122, T123, T154, T152, multc50_out_gga(T151, T152, T157)) → U38_ga(T122, T123, T154, addc12_in_gga(T152, T157, T154))
addc12_in_gga(s(T49), T50, s(T52)) → U42_gga(T49, T50, T52, addc12_in_gga(T49, T50, T52))
addc12_in_gga(0, T58, T58) → addc12_out_gga(0, T58, T58)
U42_gga(T49, T50, T52, addc12_out_gga(T49, T50, T52)) → addc12_out_gga(s(T49), T50, s(T52))
U38_ga(T122, T123, T154, addc12_out_gga(T152, T157, T154)) → evaluatec3_out_ga(*(T122, T123), T154)
U32_ga(T71, T72, T74, evaluatec3_out_ga(T71, T77)) → U33_ga(T71, T72, T74, T77, evaluatec3_in_ga(T72, T82))
U33_ga(T71, T72, T74, T77, evaluatec3_out_ga(T72, T82)) → U34_ga(T71, T72, T74, subc28_in_gga(T77, T82, T74))
subc28_in_gga(s(T100), s(T101), T103) → U43_gga(T100, T101, T103, subc28_in_gga(T100, T101, T103))
subc28_in_gga(T109, 0, T109) → subc28_out_gga(T109, 0, T109)
U43_gga(T100, T101, T103, subc28_out_gga(T100, T101, T103)) → subc28_out_gga(s(T100), s(T101), T103)
U34_ga(T71, T72, T74, subc28_out_gga(T77, T82, T74)) → evaluatec3_out_ga(-(T71, T72), T74)
U29_ga(T20, T21, T23, evaluatec3_out_ga(T20, T26)) → U30_ga(T20, T21, T23, T26, evaluatec3_in_ga(T21, T31))
U30_ga(T20, T21, T23, T26, evaluatec3_out_ga(T21, T31)) → U31_ga(T20, T21, T23, addc12_in_gga(T26, T31, T23))
U31_ga(T20, T21, T23, addc12_out_gga(T26, T31, T23)) → evaluatec3_out_ga(+(T20, T21), T23)

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 6 SCCs with 31 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

SUB28_IN_GGA(s(T100), s(T101), T103) → SUB28_IN_GGA(T100, T101, T103)

The TRS R consists of the following rules:

evaluatec3_in_ga(+(T20, T21), T23) → U29_ga(T20, T21, T23, evaluatec3_in_ga(T20, T26))
evaluatec3_in_ga(-(T71, T72), T74) → U32_ga(T71, T72, T74, evaluatec3_in_ga(T71, T77))
evaluatec3_in_ga(*(T122, T123), T154) → U35_ga(T122, T123, T154, evaluatec3_in_ga(T122, s(T151)))
evaluatec3_in_ga(*(T122, T123), 0) → U39_ga(T122, T123, evaluatec3_in_gg(T122, 0))
evaluatec3_in_gg(+(T20, T21), T23) → U29_gg(T20, T21, T23, evaluatec3_in_ga(T20, T26))
evaluatec3_in_ga(T203, T203) → U41_ga(T203, myintegerc73_in_g(T203))
myintegerc73_in_g(s(T209)) → U47_g(T209, myintegerc73_in_g(T209))
myintegerc73_in_g(0) → myintegerc73_out_g(0)
U47_g(T209, myintegerc73_out_g(T209)) → myintegerc73_out_g(s(T209))
U41_ga(T203, myintegerc73_out_g(T203)) → evaluatec3_out_ga(T203, T203)
U29_gg(T20, T21, T23, evaluatec3_out_ga(T20, T26)) → U30_gg(T20, T21, T23, T26, evaluatec3_in_ga(T21, T31))
U30_gg(T20, T21, T23, T26, evaluatec3_out_ga(T21, T31)) → U31_gg(T20, T21, T23, addc12_in_ggg(T26, T31, T23))
addc12_in_ggg(s(T49), T50, s(T52)) → U42_ggg(T49, T50, T52, addc12_in_ggg(T49, T50, T52))
addc12_in_ggg(0, T58, T58) → addc12_out_ggg(0, T58, T58)
U42_ggg(T49, T50, T52, addc12_out_ggg(T49, T50, T52)) → addc12_out_ggg(s(T49), T50, s(T52))
U31_gg(T20, T21, T23, addc12_out_ggg(T26, T31, T23)) → evaluatec3_out_gg(+(T20, T21), T23)
evaluatec3_in_gg(-(T71, T72), T74) → U32_gg(T71, T72, T74, evaluatec3_in_ga(T71, T77))
U32_gg(T71, T72, T74, evaluatec3_out_ga(T71, T77)) → U33_gg(T71, T72, T74, T77, evaluatec3_in_ga(T72, T82))
U33_gg(T71, T72, T74, T77, evaluatec3_out_ga(T72, T82)) → U34_gg(T71, T72, T74, subc28_in_ggg(T77, T82, T74))
subc28_in_ggg(s(T100), s(T101), T103) → U43_ggg(T100, T101, T103, subc28_in_ggg(T100, T101, T103))
subc28_in_ggg(T109, 0, T109) → subc28_out_ggg(T109, 0, T109)
U43_ggg(T100, T101, T103, subc28_out_ggg(T100, T101, T103)) → subc28_out_ggg(s(T100), s(T101), T103)
U34_gg(T71, T72, T74, subc28_out_ggg(T77, T82, T74)) → evaluatec3_out_gg(-(T71, T72), T74)
evaluatec3_in_gg(*(T122, T123), T154) → U35_gg(T122, T123, T154, evaluatec3_in_ga(T122, s(T151)))
U35_gg(T122, T123, T154, evaluatec3_out_ga(T122, s(T151))) → U36_gg(T122, T123, T154, T151, evaluatec3_in_ga(T123, T152))
U36_gg(T122, T123, T154, T151, evaluatec3_out_ga(T123, T152)) → U37_gg(T122, T123, T154, T152, multc50_in_gga(T151, T152, T157))
multc50_in_gga(s(T168), T169, X263) → U44_gga(T168, T169, X263, multc50_in_gga(T168, T169, T172))
multc50_in_gga(0, T194, 0) → multc50_out_gga(0, T194, 0)
U44_gga(T168, T169, X263, multc50_out_gga(T168, T169, T172)) → U45_gga(T168, T169, X263, addc58_in_gga(T169, T172, X263))
addc58_in_gga(s(T185), T186, s(X300)) → U46_gga(T185, T186, X300, addc58_in_gga(T185, T186, X300))
addc58_in_gga(0, T191, T191) → addc58_out_gga(0, T191, T191)
U46_gga(T185, T186, X300, addc58_out_gga(T185, T186, X300)) → addc58_out_gga(s(T185), T186, s(X300))
U45_gga(T168, T169, X263, addc58_out_gga(T169, T172, X263)) → multc50_out_gga(s(T168), T169, X263)
U37_gg(T122, T123, T154, T152, multc50_out_gga(T151, T152, T157)) → U38_gg(T122, T123, T154, addc12_in_ggg(T152, T157, T154))
U38_gg(T122, T123, T154, addc12_out_ggg(T152, T157, T154)) → evaluatec3_out_gg(*(T122, T123), T154)
evaluatec3_in_gg(*(T122, T123), 0) → U39_gg(T122, T123, evaluatec3_in_gg(T122, 0))
evaluatec3_in_gg(T203, T203) → U41_gg(T203, myintegerc73_in_g(T203))
U41_gg(T203, myintegerc73_out_g(T203)) → evaluatec3_out_gg(T203, T203)
U39_gg(T122, T123, evaluatec3_out_gg(T122, 0)) → U40_gg(T122, T123, evaluatec3_in_ga(T123, T200))
U40_gg(T122, T123, evaluatec3_out_ga(T123, T200)) → evaluatec3_out_gg(*(T122, T123), 0)
U39_ga(T122, T123, evaluatec3_out_gg(T122, 0)) → U40_ga(T122, T123, evaluatec3_in_ga(T123, T200))
U40_ga(T122, T123, evaluatec3_out_ga(T123, T200)) → evaluatec3_out_ga(*(T122, T123), 0)
U35_ga(T122, T123, T154, evaluatec3_out_ga(T122, s(T151))) → U36_ga(T122, T123, T154, T151, evaluatec3_in_ga(T123, T152))
U36_ga(T122, T123, T154, T151, evaluatec3_out_ga(T123, T152)) → U37_ga(T122, T123, T154, T152, multc50_in_gga(T151, T152, T157))
U37_ga(T122, T123, T154, T152, multc50_out_gga(T151, T152, T157)) → U38_ga(T122, T123, T154, addc12_in_gga(T152, T157, T154))
addc12_in_gga(s(T49), T50, s(T52)) → U42_gga(T49, T50, T52, addc12_in_gga(T49, T50, T52))
addc12_in_gga(0, T58, T58) → addc12_out_gga(0, T58, T58)
U42_gga(T49, T50, T52, addc12_out_gga(T49, T50, T52)) → addc12_out_gga(s(T49), T50, s(T52))
U38_ga(T122, T123, T154, addc12_out_gga(T152, T157, T154)) → evaluatec3_out_ga(*(T122, T123), T154)
U32_ga(T71, T72, T74, evaluatec3_out_ga(T71, T77)) → U33_ga(T71, T72, T74, T77, evaluatec3_in_ga(T72, T82))
U33_ga(T71, T72, T74, T77, evaluatec3_out_ga(T72, T82)) → U34_ga(T71, T72, T74, subc28_in_gga(T77, T82, T74))
subc28_in_gga(s(T100), s(T101), T103) → U43_gga(T100, T101, T103, subc28_in_gga(T100, T101, T103))
subc28_in_gga(T109, 0, T109) → subc28_out_gga(T109, 0, T109)
U43_gga(T100, T101, T103, subc28_out_gga(T100, T101, T103)) → subc28_out_gga(s(T100), s(T101), T103)
U34_ga(T71, T72, T74, subc28_out_gga(T77, T82, T74)) → evaluatec3_out_ga(-(T71, T72), T74)
U29_ga(T20, T21, T23, evaluatec3_out_ga(T20, T26)) → U30_ga(T20, T21, T23, T26, evaluatec3_in_ga(T21, T31))
U30_ga(T20, T21, T23, T26, evaluatec3_out_ga(T21, T31)) → U31_ga(T20, T21, T23, addc12_in_gga(T26, T31, T23))
U31_ga(T20, T21, T23, addc12_out_gga(T26, T31, T23)) → evaluatec3_out_ga(+(T20, T21), T23)

The argument filtering Pi contains the following mapping:
+(x1, x2) = +(x1, x2)
evaluatec3_in_ga(x1, x2) = evaluatec3_in_ga(x1)
U29_ga(x1, x2, x3, x4) = U29_ga(x1, x2, x4)
-(x1, x2) = -(x1, x2)
U32_ga(x1, x2, x3, x4) = U32_ga(x1, x2, x4)
*(x1, x2) = *(x1, x2)
U35_ga(x1, x2, x3, x4) = U35_ga(x1, x2, x4)
U39_ga(x1, x2, x3) = U39_ga(x1, x2, x3)
evaluatec3_in_gg(x1, x2) = evaluatec3_in_gg(x1, x2)
U29_gg(x1, x2, x3, x4) = U29_gg(x1, x2, x3, x4)
U41_ga(x1, x2) = U41_ga(x1, x2)
myintegerc73_in_g(x1) = myintegerc73_in_g(x1)
s(x1) = s(x1)
U47_g(x1, x2) = U47_g(x1, x2)
0 = 0
myintegerc73_out_g(x1) = myintegerc73_out_g(x1)
evaluatec3_out_ga(x1, x2) = evaluatec3_out_ga(x1, x2)
U30_gg(x1, x2, x3, x4, x5) = U30_gg(x1, x2, x3, x4, x5)
U31_gg(x1, x2, x3, x4) = U31_gg(x1, x2, x3, x4)
addc12_in_ggg(x1, x2, x3) = addc12_in_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3, x4) = U42_ggg(x1, x2, x3, x4)
addc12_out_ggg(x1, x2, x3) = addc12_out_ggg(x1, x2, x3)
evaluatec3_out_gg(x1, x2) = evaluatec3_out_gg(x1, x2)
U32_gg(x1, x2, x3, x4) = U32_gg(x1, x2, x3, x4)
U33_gg(x1, x2, x3, x4, x5) = U33_gg(x1, x2, x3, x4, x5)
U34_gg(x1, x2, x3, x4) = U34_gg(x1, x2, x3, x4)
subc28_in_ggg(x1, x2, x3) = subc28_in_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3, x4) = U43_ggg(x1, x2, x3, x4)
subc28_out_ggg(x1, x2, x3) = subc28_out_ggg(x1, x2, x3)
U35_gg(x1, x2, x3, x4) = U35_gg(x1, x2, x3, x4)
U36_gg(x1, x2, x3, x4, x5) = U36_gg(x1, x2, x3, x4, x5)
U37_gg(x1, x2, x3, x4, x5) = U37_gg(x1, x2, x3, x4, x5)
multc50_in_gga(x1, x2, x3) = multc50_in_gga(x1, x2)
U44_gga(x1, x2, x3, x4) = U44_gga(x1, x2, x4)
multc50_out_gga(x1, x2, x3) = multc50_out_gga(x1, x2, x3)
U45_gga(x1, x2, x3, x4) = U45_gga(x1, x2, x4)
addc58_in_gga(x1, x2, x3) = addc58_in_gga(x1, x2)
U46_gga(x1, x2, x3, x4) = U46_gga(x1, x2, x4)
addc58_out_gga(x1, x2, x3) = addc58_out_gga(x1, x2, x3)
U38_gg(x1, x2, x3, x4) = U38_gg(x1, x2, x3, x4)
U39_gg(x1, x2, x3) = U39_gg(x1, x2, x3)
U41_gg(x1, x2) = U41_gg(x1, x2)
U40_gg(x1, x2, x3) = U40_gg(x1, x2, x3)
U40_ga(x1, x2, x3) = U40_ga(x1, x2, x3)
U36_ga(x1, x2, x3, x4, x5) = U36_ga(x1, x2, x4, x5)
U37_ga(x1, x2, x3, x4, x5) = U37_ga(x1, x2, x4, x5)
U38_ga(x1, x2, x3, x4) = U38_ga(x1, x2, x4)
addc12_in_gga(x1, x2, x3) = addc12_in_gga(x1, x2)
U42_gga(x1, x2, x3, x4) = U42_gga(x1, x2, x4)
addc12_out_gga(x1, x2, x3) = addc12_out_gga(x1, x2, x3)
U33_ga(x1, x2, x3, x4, x5) = U33_ga(x1, x2, x4, x5)
U34_ga(x1, x2, x3, x4) = U34_ga(x1, x2, x4)
subc28_in_gga(x1, x2, x3) = subc28_in_gga(x1, x2)
U43_gga(x1, x2, x3, x4) = U43_gga(x1, x2, x4)
subc28_out_gga(x1, x2, x3) = subc28_out_gga(x1, x2, x3)
U30_ga(x1, x2, x3, x4, x5) = U30_ga(x1, x2, x4, x5)
U31_ga(x1, x2, x3, x4) = U31_ga(x1, x2, x4)
SUB28_IN_GGA(x1, x2, x3) = SUB28_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:

SUB28_IN_GGA(s(T100), s(T101), T103) → SUB28_IN_GGA(T100, T101, T103)

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

SUB28_IN_GGA(s(T100), s(T101)) → SUB28_IN_GGA(T100, T101)

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:

SUB28_IN_GGA(s(T100), s(T101)) → SUB28_IN_GGA(T100, T101)
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:

MYINTEGER73_IN_G(s(T209)) → MYINTEGER73_IN_G(T209)

The TRS R consists of the following rules:

evaluatec3_in_ga(+(T20, T21), T23) → U29_ga(T20, T21, T23, evaluatec3_in_ga(T20, T26))
evaluatec3_in_ga(-(T71, T72), T74) → U32_ga(T71, T72, T74, evaluatec3_in_ga(T71, T77))
evaluatec3_in_ga(*(T122, T123), T154) → U35_ga(T122, T123, T154, evaluatec3_in_ga(T122, s(T151)))
evaluatec3_in_ga(*(T122, T123), 0) → U39_ga(T122, T123, evaluatec3_in_gg(T122, 0))
evaluatec3_in_gg(+(T20, T21), T23) → U29_gg(T20, T21, T23, evaluatec3_in_ga(T20, T26))
evaluatec3_in_ga(T203, T203) → U41_ga(T203, myintegerc73_in_g(T203))
myintegerc73_in_g(s(T209)) → U47_g(T209, myintegerc73_in_g(T209))
myintegerc73_in_g(0) → myintegerc73_out_g(0)
U47_g(T209, myintegerc73_out_g(T209)) → myintegerc73_out_g(s(T209))
U41_ga(T203, myintegerc73_out_g(T203)) → evaluatec3_out_ga(T203, T203)
U29_gg(T20, T21, T23, evaluatec3_out_ga(T20, T26)) → U30_gg(T20, T21, T23, T26, evaluatec3_in_ga(T21, T31))
U30_gg(T20, T21, T23, T26, evaluatec3_out_ga(T21, T31)) → U31_gg(T20, T21, T23, addc12_in_ggg(T26, T31, T23))
addc12_in_ggg(s(T49), T50, s(T52)) → U42_ggg(T49, T50, T52, addc12_in_ggg(T49, T50, T52))
addc12_in_ggg(0, T58, T58) → addc12_out_ggg(0, T58, T58)
U42_ggg(T49, T50, T52, addc12_out_ggg(T49, T50, T52)) → addc12_out_ggg(s(T49), T50, s(T52))
U31_gg(T20, T21, T23, addc12_out_ggg(T26, T31, T23)) → evaluatec3_out_gg(+(T20, T21), T23)
evaluatec3_in_gg(-(T71, T72), T74) → U32_gg(T71, T72, T74, evaluatec3_in_ga(T71, T77))
U32_gg(T71, T72, T74, evaluatec3_out_ga(T71, T77)) → U33_gg(T71, T72, T74, T77, evaluatec3_in_ga(T72, T82))
U33_gg(T71, T72, T74, T77, evaluatec3_out_ga(T72, T82)) → U34_gg(T71, T72, T74, subc28_in_ggg(T77, T82, T74))
subc28_in_ggg(s(T100), s(T101), T103) → U43_ggg(T100, T101, T103, subc28_in_ggg(T100, T101, T103))
subc28_in_ggg(T109, 0, T109) → subc28_out_ggg(T109, 0, T109)
U43_ggg(T100, T101, T103, subc28_out_ggg(T100, T101, T103)) → subc28_out_ggg(s(T100), s(T101), T103)
U34_gg(T71, T72, T74, subc28_out_ggg(T77, T82, T74)) → evaluatec3_out_gg(-(T71, T72), T74)
evaluatec3_in_gg(*(T122, T123), T154) → U35_gg(T122, T123, T154, evaluatec3_in_ga(T122, s(T151)))
U35_gg(T122, T123, T154, evaluatec3_out_ga(T122, s(T151))) → U36_gg(T122, T123, T154, T151, evaluatec3_in_ga(T123, T152))
U36_gg(T122, T123, T154, T151, evaluatec3_out_ga(T123, T152)) → U37_gg(T122, T123, T154, T152, multc50_in_gga(T151, T152, T157))
multc50_in_gga(s(T168), T169, X263) → U44_gga(T168, T169, X263, multc50_in_gga(T168, T169, T172))
multc50_in_gga(0, T194, 0) → multc50_out_gga(0, T194, 0)
U44_gga(T168, T169, X263, multc50_out_gga(T168, T169, T172)) → U45_gga(T168, T169, X263, addc58_in_gga(T169, T172, X263))
addc58_in_gga(s(T185), T186, s(X300)) → U46_gga(T185, T186, X300, addc58_in_gga(T185, T186, X300))
addc58_in_gga(0, T191, T191) → addc58_out_gga(0, T191, T191)
U46_gga(T185, T186, X300, addc58_out_gga(T185, T186, X300)) → addc58_out_gga(s(T185), T186, s(X300))
U45_gga(T168, T169, X263, addc58_out_gga(T169, T172, X263)) → multc50_out_gga(s(T168), T169, X263)
U37_gg(T122, T123, T154, T152, multc50_out_gga(T151, T152, T157)) → U38_gg(T122, T123, T154, addc12_in_ggg(T152, T157, T154))
U38_gg(T122, T123, T154, addc12_out_ggg(T152, T157, T154)) → evaluatec3_out_gg(*(T122, T123), T154)
evaluatec3_in_gg(*(T122, T123), 0) → U39_gg(T122, T123, evaluatec3_in_gg(T122, 0))
evaluatec3_in_gg(T203, T203) → U41_gg(T203, myintegerc73_in_g(T203))
U41_gg(T203, myintegerc73_out_g(T203)) → evaluatec3_out_gg(T203, T203)
U39_gg(T122, T123, evaluatec3_out_gg(T122, 0)) → U40_gg(T122, T123, evaluatec3_in_ga(T123, T200))
U40_gg(T122, T123, evaluatec3_out_ga(T123, T200)) → evaluatec3_out_gg(*(T122, T123), 0)
U39_ga(T122, T123, evaluatec3_out_gg(T122, 0)) → U40_ga(T122, T123, evaluatec3_in_ga(T123, T200))
U40_ga(T122, T123, evaluatec3_out_ga(T123, T200)) → evaluatec3_out_ga(*(T122, T123), 0)
U35_ga(T122, T123, T154, evaluatec3_out_ga(T122, s(T151))) → U36_ga(T122, T123, T154, T151, evaluatec3_in_ga(T123, T152))
U36_ga(T122, T123, T154, T151, evaluatec3_out_ga(T123, T152)) → U37_ga(T122, T123, T154, T152, multc50_in_gga(T151, T152, T157))
U37_ga(T122, T123, T154, T152, multc50_out_gga(T151, T152, T157)) → U38_ga(T122, T123, T154, addc12_in_gga(T152, T157, T154))
addc12_in_gga(s(T49), T50, s(T52)) → U42_gga(T49, T50, T52, addc12_in_gga(T49, T50, T52))
addc12_in_gga(0, T58, T58) → addc12_out_gga(0, T58, T58)
U42_gga(T49, T50, T52, addc12_out_gga(T49, T50, T52)) → addc12_out_gga(s(T49), T50, s(T52))
U38_ga(T122, T123, T154, addc12_out_gga(T152, T157, T154)) → evaluatec3_out_ga(*(T122, T123), T154)
U32_ga(T71, T72, T74, evaluatec3_out_ga(T71, T77)) → U33_ga(T71, T72, T74, T77, evaluatec3_in_ga(T72, T82))
U33_ga(T71, T72, T74, T77, evaluatec3_out_ga(T72, T82)) → U34_ga(T71, T72, T74, subc28_in_gga(T77, T82, T74))
subc28_in_gga(s(T100), s(T101), T103) → U43_gga(T100, T101, T103, subc28_in_gga(T100, T101, T103))
subc28_in_gga(T109, 0, T109) → subc28_out_gga(T109, 0, T109)
U43_gga(T100, T101, T103, subc28_out_gga(T100, T101, T103)) → subc28_out_gga(s(T100), s(T101), T103)
U34_ga(T71, T72, T74, subc28_out_gga(T77, T82, T74)) → evaluatec3_out_ga(-(T71, T72), T74)
U29_ga(T20, T21, T23, evaluatec3_out_ga(T20, T26)) → U30_ga(T20, T21, T23, T26, evaluatec3_in_ga(T21, T31))
U30_ga(T20, T21, T23, T26, evaluatec3_out_ga(T21, T31)) → U31_ga(T20, T21, T23, addc12_in_gga(T26, T31, T23))
U31_ga(T20, T21, T23, addc12_out_gga(T26, T31, T23)) → evaluatec3_out_ga(+(T20, T21), T23)

The argument filtering Pi contains the following mapping:
+(x1, x2) = +(x1, x2)
evaluatec3_in_ga(x1, x2) = evaluatec3_in_ga(x1)
U29_ga(x1, x2, x3, x4) = U29_ga(x1, x2, x4)
-(x1, x2) = -(x1, x2)
U32_ga(x1, x2, x3, x4) = U32_ga(x1, x2, x4)
*(x1, x2) = *(x1, x2)
U35_ga(x1, x2, x3, x4) = U35_ga(x1, x2, x4)
U39_ga(x1, x2, x3) = U39_ga(x1, x2, x3)
evaluatec3_in_gg(x1, x2) = evaluatec3_in_gg(x1, x2)
U29_gg(x1, x2, x3, x4) = U29_gg(x1, x2, x3, x4)
U41_ga(x1, x2) = U41_ga(x1, x2)
myintegerc73_in_g(x1) = myintegerc73_in_g(x1)
s(x1) = s(x1)
U47_g(x1, x2) = U47_g(x1, x2)
0 = 0
myintegerc73_out_g(x1) = myintegerc73_out_g(x1)
evaluatec3_out_ga(x1, x2) = evaluatec3_out_ga(x1, x2)
U30_gg(x1, x2, x3, x4, x5) = U30_gg(x1, x2, x3, x4, x5)
U31_gg(x1, x2, x3, x4) = U31_gg(x1, x2, x3, x4)
addc12_in_ggg(x1, x2, x3) = addc12_in_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3, x4) = U42_ggg(x1, x2, x3, x4)
addc12_out_ggg(x1, x2, x3) = addc12_out_ggg(x1, x2, x3)
evaluatec3_out_gg(x1, x2) = evaluatec3_out_gg(x1, x2)
U32_gg(x1, x2, x3, x4) = U32_gg(x1, x2, x3, x4)
U33_gg(x1, x2, x3, x4, x5) = U33_gg(x1, x2, x3, x4, x5)
U34_gg(x1, x2, x3, x4) = U34_gg(x1, x2, x3, x4)
subc28_in_ggg(x1, x2, x3) = subc28_in_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3, x4) = U43_ggg(x1, x2, x3, x4)
subc28_out_ggg(x1, x2, x3) = subc28_out_ggg(x1, x2, x3)
U35_gg(x1, x2, x3, x4) = U35_gg(x1, x2, x3, x4)
U36_gg(x1, x2, x3, x4, x5) = U36_gg(x1, x2, x3, x4, x5)
U37_gg(x1, x2, x3, x4, x5) = U37_gg(x1, x2, x3, x4, x5)
multc50_in_gga(x1, x2, x3) = multc50_in_gga(x1, x2)
U44_gga(x1, x2, x3, x4) = U44_gga(x1, x2, x4)
multc50_out_gga(x1, x2, x3) = multc50_out_gga(x1, x2, x3)
U45_gga(x1, x2, x3, x4) = U45_gga(x1, x2, x4)
addc58_in_gga(x1, x2, x3) = addc58_in_gga(x1, x2)
U46_gga(x1, x2, x3, x4) = U46_gga(x1, x2, x4)
addc58_out_gga(x1, x2, x3) = addc58_out_gga(x1, x2, x3)
U38_gg(x1, x2, x3, x4) = U38_gg(x1, x2, x3, x4)
U39_gg(x1, x2, x3) = U39_gg(x1, x2, x3)
U41_gg(x1, x2) = U41_gg(x1, x2)
U40_gg(x1, x2, x3) = U40_gg(x1, x2, x3)
U40_ga(x1, x2, x3) = U40_ga(x1, x2, x3)
U36_ga(x1, x2, x3, x4, x5) = U36_ga(x1, x2, x4, x5)
U37_ga(x1, x2, x3, x4, x5) = U37_ga(x1, x2, x4, x5)
U38_ga(x1, x2, x3, x4) = U38_ga(x1, x2, x4)
addc12_in_gga(x1, x2, x3) = addc12_in_gga(x1, x2)
U42_gga(x1, x2, x3, x4) = U42_gga(x1, x2, x4)
addc12_out_gga(x1, x2, x3) = addc12_out_gga(x1, x2, x3)
U33_ga(x1, x2, x3, x4, x5) = U33_ga(x1, x2, x4, x5)
U34_ga(x1, x2, x3, x4) = U34_ga(x1, x2, x4)
subc28_in_gga(x1, x2, x3) = subc28_in_gga(x1, x2)
U43_gga(x1, x2, x3, x4) = U43_gga(x1, x2, x4)
subc28_out_gga(x1, x2, x3) = subc28_out_gga(x1, x2, x3)
U30_ga(x1, x2, x3, x4, x5) = U30_ga(x1, x2, x4, x5)
U31_ga(x1, x2, x3, x4) = U31_ga(x1, x2, x4)
MYINTEGER73_IN_G(x1) = MYINTEGER73_IN_G(x1)

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:

MYINTEGER73_IN_G(s(T209)) → MYINTEGER73_IN_G(T209)

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

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

MYINTEGER73_IN_G(s(T209)) → MYINTEGER73_IN_G(T209)

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:

MYINTEGER73_IN_G(s(T209)) → MYINTEGER73_IN_G(T209)
The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

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

ADD12_IN_GGA(s(T49), T50, s(T52)) → ADD12_IN_GGA(T49, T50, T52)

The TRS R consists of the following rules:

evaluatec3_in_ga(+(T20, T21), T23) → U29_ga(T20, T21, T23, evaluatec3_in_ga(T20, T26))
evaluatec3_in_ga(-(T71, T72), T74) → U32_ga(T71, T72, T74, evaluatec3_in_ga(T71, T77))
evaluatec3_in_ga(*(T122, T123), T154) → U35_ga(T122, T123, T154, evaluatec3_in_ga(T122, s(T151)))
evaluatec3_in_ga(*(T122, T123), 0) → U39_ga(T122, T123, evaluatec3_in_gg(T122, 0))
evaluatec3_in_gg(+(T20, T21), T23) → U29_gg(T20, T21, T23, evaluatec3_in_ga(T20, T26))
evaluatec3_in_ga(T203, T203) → U41_ga(T203, myintegerc73_in_g(T203))
myintegerc73_in_g(s(T209)) → U47_g(T209, myintegerc73_in_g(T209))
myintegerc73_in_g(0) → myintegerc73_out_g(0)
U47_g(T209, myintegerc73_out_g(T209)) → myintegerc73_out_g(s(T209))
U41_ga(T203, myintegerc73_out_g(T203)) → evaluatec3_out_ga(T203, T203)
U29_gg(T20, T21, T23, evaluatec3_out_ga(T20, T26)) → U30_gg(T20, T21, T23, T26, evaluatec3_in_ga(T21, T31))
U30_gg(T20, T21, T23, T26, evaluatec3_out_ga(T21, T31)) → U31_gg(T20, T21, T23, addc12_in_ggg(T26, T31, T23))
addc12_in_ggg(s(T49), T50, s(T52)) → U42_ggg(T49, T50, T52, addc12_in_ggg(T49, T50, T52))
addc12_in_ggg(0, T58, T58) → addc12_out_ggg(0, T58, T58)
U42_ggg(T49, T50, T52, addc12_out_ggg(T49, T50, T52)) → addc12_out_ggg(s(T49), T50, s(T52))
U31_gg(T20, T21, T23, addc12_out_ggg(T26, T31, T23)) → evaluatec3_out_gg(+(T20, T21), T23)
evaluatec3_in_gg(-(T71, T72), T74) → U32_gg(T71, T72, T74, evaluatec3_in_ga(T71, T77))
U32_gg(T71, T72, T74, evaluatec3_out_ga(T71, T77)) → U33_gg(T71, T72, T74, T77, evaluatec3_in_ga(T72, T82))
U33_gg(T71, T72, T74, T77, evaluatec3_out_ga(T72, T82)) → U34_gg(T71, T72, T74, subc28_in_ggg(T77, T82, T74))
subc28_in_ggg(s(T100), s(T101), T103) → U43_ggg(T100, T101, T103, subc28_in_ggg(T100, T101, T103))
subc28_in_ggg(T109, 0, T109) → subc28_out_ggg(T109, 0, T109)
U43_ggg(T100, T101, T103, subc28_out_ggg(T100, T101, T103)) → subc28_out_ggg(s(T100), s(T101), T103)
U34_gg(T71, T72, T74, subc28_out_ggg(T77, T82, T74)) → evaluatec3_out_gg(-(T71, T72), T74)
evaluatec3_in_gg(*(T122, T123), T154) → U35_gg(T122, T123, T154, evaluatec3_in_ga(T122, s(T151)))
U35_gg(T122, T123, T154, evaluatec3_out_ga(T122, s(T151))) → U36_gg(T122, T123, T154, T151, evaluatec3_in_ga(T123, T152))
U36_gg(T122, T123, T154, T151, evaluatec3_out_ga(T123, T152)) → U37_gg(T122, T123, T154, T152, multc50_in_gga(T151, T152, T157))
multc50_in_gga(s(T168), T169, X263) → U44_gga(T168, T169, X263, multc50_in_gga(T168, T169, T172))
multc50_in_gga(0, T194, 0) → multc50_out_gga(0, T194, 0)
U44_gga(T168, T169, X263, multc50_out_gga(T168, T169, T172)) → U45_gga(T168, T169, X263, addc58_in_gga(T169, T172, X263))
addc58_in_gga(s(T185), T186, s(X300)) → U46_gga(T185, T186, X300, addc58_in_gga(T185, T186, X300))
addc58_in_gga(0, T191, T191) → addc58_out_gga(0, T191, T191)
U46_gga(T185, T186, X300, addc58_out_gga(T185, T186, X300)) → addc58_out_gga(s(T185), T186, s(X300))
U45_gga(T168, T169, X263, addc58_out_gga(T169, T172, X263)) → multc50_out_gga(s(T168), T169, X263)
U37_gg(T122, T123, T154, T152, multc50_out_gga(T151, T152, T157)) → U38_gg(T122, T123, T154, addc12_in_ggg(T152, T157, T154))
U38_gg(T122, T123, T154, addc12_out_ggg(T152, T157, T154)) → evaluatec3_out_gg(*(T122, T123), T154)
evaluatec3_in_gg(*(T122, T123), 0) → U39_gg(T122, T123, evaluatec3_in_gg(T122, 0))
evaluatec3_in_gg(T203, T203) → U41_gg(T203, myintegerc73_in_g(T203))
U41_gg(T203, myintegerc73_out_g(T203)) → evaluatec3_out_gg(T203, T203)
U39_gg(T122, T123, evaluatec3_out_gg(T122, 0)) → U40_gg(T122, T123, evaluatec3_in_ga(T123, T200))
U40_gg(T122, T123, evaluatec3_out_ga(T123, T200)) → evaluatec3_out_gg(*(T122, T123), 0)
U39_ga(T122, T123, evaluatec3_out_gg(T122, 0)) → U40_ga(T122, T123, evaluatec3_in_ga(T123, T200))
U40_ga(T122, T123, evaluatec3_out_ga(T123, T200)) → evaluatec3_out_ga(*(T122, T123), 0)
U35_ga(T122, T123, T154, evaluatec3_out_ga(T122, s(T151))) → U36_ga(T122, T123, T154, T151, evaluatec3_in_ga(T123, T152))
U36_ga(T122, T123, T154, T151, evaluatec3_out_ga(T123, T152)) → U37_ga(T122, T123, T154, T152, multc50_in_gga(T151, T152, T157))
U37_ga(T122, T123, T154, T152, multc50_out_gga(T151, T152, T157)) → U38_ga(T122, T123, T154, addc12_in_gga(T152, T157, T154))
addc12_in_gga(s(T49), T50, s(T52)) → U42_gga(T49, T50, T52, addc12_in_gga(T49, T50, T52))
addc12_in_gga(0, T58, T58) → addc12_out_gga(0, T58, T58)
U42_gga(T49, T50, T52, addc12_out_gga(T49, T50, T52)) → addc12_out_gga(s(T49), T50, s(T52))
U38_ga(T122, T123, T154, addc12_out_gga(T152, T157, T154)) → evaluatec3_out_ga(*(T122, T123), T154)
U32_ga(T71, T72, T74, evaluatec3_out_ga(T71, T77)) → U33_ga(T71, T72, T74, T77, evaluatec3_in_ga(T72, T82))
U33_ga(T71, T72, T74, T77, evaluatec3_out_ga(T72, T82)) → U34_ga(T71, T72, T74, subc28_in_gga(T77, T82, T74))
subc28_in_gga(s(T100), s(T101), T103) → U43_gga(T100, T101, T103, subc28_in_gga(T100, T101, T103))
subc28_in_gga(T109, 0, T109) → subc28_out_gga(T109, 0, T109)
U43_gga(T100, T101, T103, subc28_out_gga(T100, T101, T103)) → subc28_out_gga(s(T100), s(T101), T103)
U34_ga(T71, T72, T74, subc28_out_gga(T77, T82, T74)) → evaluatec3_out_ga(-(T71, T72), T74)
U29_ga(T20, T21, T23, evaluatec3_out_ga(T20, T26)) → U30_ga(T20, T21, T23, T26, evaluatec3_in_ga(T21, T31))
U30_ga(T20, T21, T23, T26, evaluatec3_out_ga(T21, T31)) → U31_ga(T20, T21, T23, addc12_in_gga(T26, T31, T23))
U31_ga(T20, T21, T23, addc12_out_gga(T26, T31, T23)) → evaluatec3_out_ga(+(T20, T21), T23)

The argument filtering Pi contains the following mapping:
+(x1, x2) = +(x1, x2)
evaluatec3_in_ga(x1, x2) = evaluatec3_in_ga(x1)
U29_ga(x1, x2, x3, x4) = U29_ga(x1, x2, x4)
-(x1, x2) = -(x1, x2)
U32_ga(x1, x2, x3, x4) = U32_ga(x1, x2, x4)
*(x1, x2) = *(x1, x2)
U35_ga(x1, x2, x3, x4) = U35_ga(x1, x2, x4)
U39_ga(x1, x2, x3) = U39_ga(x1, x2, x3)
evaluatec3_in_gg(x1, x2) = evaluatec3_in_gg(x1, x2)
U29_gg(x1, x2, x3, x4) = U29_gg(x1, x2, x3, x4)
U41_ga(x1, x2) = U41_ga(x1, x2)
myintegerc73_in_g(x1) = myintegerc73_in_g(x1)
s(x1) = s(x1)
U47_g(x1, x2) = U47_g(x1, x2)
0 = 0
myintegerc73_out_g(x1) = myintegerc73_out_g(x1)
evaluatec3_out_ga(x1, x2) = evaluatec3_out_ga(x1, x2)
U30_gg(x1, x2, x3, x4, x5) = U30_gg(x1, x2, x3, x4, x5)
U31_gg(x1, x2, x3, x4) = U31_gg(x1, x2, x3, x4)
addc12_in_ggg(x1, x2, x3) = addc12_in_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3, x4) = U42_ggg(x1, x2, x3, x4)
addc12_out_ggg(x1, x2, x3) = addc12_out_ggg(x1, x2, x3)
evaluatec3_out_gg(x1, x2) = evaluatec3_out_gg(x1, x2)
U32_gg(x1, x2, x3, x4) = U32_gg(x1, x2, x3, x4)
U33_gg(x1, x2, x3, x4, x5) = U33_gg(x1, x2, x3, x4, x5)
U34_gg(x1, x2, x3, x4) = U34_gg(x1, x2, x3, x4)
subc28_in_ggg(x1, x2, x3) = subc28_in_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3, x4) = U43_ggg(x1, x2, x3, x4)
subc28_out_ggg(x1, x2, x3) = subc28_out_ggg(x1, x2, x3)
U35_gg(x1, x2, x3, x4) = U35_gg(x1, x2, x3, x4)
U36_gg(x1, x2, x3, x4, x5) = U36_gg(x1, x2, x3, x4, x5)
U37_gg(x1, x2, x3, x4, x5) = U37_gg(x1, x2, x3, x4, x5)
multc50_in_gga(x1, x2, x3) = multc50_in_gga(x1, x2)
U44_gga(x1, x2, x3, x4) = U44_gga(x1, x2, x4)
multc50_out_gga(x1, x2, x3) = multc50_out_gga(x1, x2, x3)
U45_gga(x1, x2, x3, x4) = U45_gga(x1, x2, x4)
addc58_in_gga(x1, x2, x3) = addc58_in_gga(x1, x2)
U46_gga(x1, x2, x3, x4) = U46_gga(x1, x2, x4)
addc58_out_gga(x1, x2, x3) = addc58_out_gga(x1, x2, x3)
U38_gg(x1, x2, x3, x4) = U38_gg(x1, x2, x3, x4)
U39_gg(x1, x2, x3) = U39_gg(x1, x2, x3)
U41_gg(x1, x2) = U41_gg(x1, x2)
U40_gg(x1, x2, x3) = U40_gg(x1, x2, x3)
U40_ga(x1, x2, x3) = U40_ga(x1, x2, x3)
U36_ga(x1, x2, x3, x4, x5) = U36_ga(x1, x2, x4, x5)
U37_ga(x1, x2, x3, x4, x5) = U37_ga(x1, x2, x4, x5)
U38_ga(x1, x2, x3, x4) = U38_ga(x1, x2, x4)
addc12_in_gga(x1, x2, x3) = addc12_in_gga(x1, x2)
U42_gga(x1, x2, x3, x4) = U42_gga(x1, x2, x4)
addc12_out_gga(x1, x2, x3) = addc12_out_gga(x1, x2, x3)
U33_ga(x1, x2, x3, x4, x5) = U33_ga(x1, x2, x4, x5)
U34_ga(x1, x2, x3, x4) = U34_ga(x1, x2, x4)
subc28_in_gga(x1, x2, x3) = subc28_in_gga(x1, x2)
U43_gga(x1, x2, x3, x4) = U43_gga(x1, x2, x4)
subc28_out_gga(x1, x2, x3) = subc28_out_gga(x1, x2, x3)
U30_ga(x1, x2, x3, x4, x5) = U30_ga(x1, x2, x4, x5)
U31_ga(x1, x2, x3, x4) = U31_ga(x1, x2, x4)
ADD12_IN_GGA(x1, x2, x3) = ADD12_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:

ADD12_IN_GGA(s(T49), T50, s(T52)) → ADD12_IN_GGA(T49, T50, T52)

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

ADD12_IN_GGA(s(T49), T50) → ADD12_IN_GGA(T49, T50)

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:

ADD12_IN_GGA(s(T49), T50) → ADD12_IN_GGA(T49, T50)
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:

ADD58_IN_GGA(s(T185), T186, s(X300)) → ADD58_IN_GGA(T185, T186, X300)

The TRS R consists of the following rules:

evaluatec3_in_ga(+(T20, T21), T23) → U29_ga(T20, T21, T23, evaluatec3_in_ga(T20, T26))
evaluatec3_in_ga(-(T71, T72), T74) → U32_ga(T71, T72, T74, evaluatec3_in_ga(T71, T77))
evaluatec3_in_ga(*(T122, T123), T154) → U35_ga(T122, T123, T154, evaluatec3_in_ga(T122, s(T151)))
evaluatec3_in_ga(*(T122, T123), 0) → U39_ga(T122, T123, evaluatec3_in_gg(T122, 0))
evaluatec3_in_gg(+(T20, T21), T23) → U29_gg(T20, T21, T23, evaluatec3_in_ga(T20, T26))
evaluatec3_in_ga(T203, T203) → U41_ga(T203, myintegerc73_in_g(T203))
myintegerc73_in_g(s(T209)) → U47_g(T209, myintegerc73_in_g(T209))
myintegerc73_in_g(0) → myintegerc73_out_g(0)
U47_g(T209, myintegerc73_out_g(T209)) → myintegerc73_out_g(s(T209))
U41_ga(T203, myintegerc73_out_g(T203)) → evaluatec3_out_ga(T203, T203)
U29_gg(T20, T21, T23, evaluatec3_out_ga(T20, T26)) → U30_gg(T20, T21, T23, T26, evaluatec3_in_ga(T21, T31))
U30_gg(T20, T21, T23, T26, evaluatec3_out_ga(T21, T31)) → U31_gg(T20, T21, T23, addc12_in_ggg(T26, T31, T23))
addc12_in_ggg(s(T49), T50, s(T52)) → U42_ggg(T49, T50, T52, addc12_in_ggg(T49, T50, T52))
addc12_in_ggg(0, T58, T58) → addc12_out_ggg(0, T58, T58)
U42_ggg(T49, T50, T52, addc12_out_ggg(T49, T50, T52)) → addc12_out_ggg(s(T49), T50, s(T52))
U31_gg(T20, T21, T23, addc12_out_ggg(T26, T31, T23)) → evaluatec3_out_gg(+(T20, T21), T23)
evaluatec3_in_gg(-(T71, T72), T74) → U32_gg(T71, T72, T74, evaluatec3_in_ga(T71, T77))
U32_gg(T71, T72, T74, evaluatec3_out_ga(T71, T77)) → U33_gg(T71, T72, T74, T77, evaluatec3_in_ga(T72, T82))
U33_gg(T71, T72, T74, T77, evaluatec3_out_ga(T72, T82)) → U34_gg(T71, T72, T74, subc28_in_ggg(T77, T82, T74))
subc28_in_ggg(s(T100), s(T101), T103) → U43_ggg(T100, T101, T103, subc28_in_ggg(T100, T101, T103))
subc28_in_ggg(T109, 0, T109) → subc28_out_ggg(T109, 0, T109)
U43_ggg(T100, T101, T103, subc28_out_ggg(T100, T101, T103)) → subc28_out_ggg(s(T100), s(T101), T103)
U34_gg(T71, T72, T74, subc28_out_ggg(T77, T82, T74)) → evaluatec3_out_gg(-(T71, T72), T74)
evaluatec3_in_gg(*(T122, T123), T154) → U35_gg(T122, T123, T154, evaluatec3_in_ga(T122, s(T151)))
U35_gg(T122, T123, T154, evaluatec3_out_ga(T122, s(T151))) → U36_gg(T122, T123, T154, T151, evaluatec3_in_ga(T123, T152))
U36_gg(T122, T123, T154, T151, evaluatec3_out_ga(T123, T152)) → U37_gg(T122, T123, T154, T152, multc50_in_gga(T151, T152, T157))
multc50_in_gga(s(T168), T169, X263) → U44_gga(T168, T169, X263, multc50_in_gga(T168, T169, T172))
multc50_in_gga(0, T194, 0) → multc50_out_gga(0, T194, 0)
U44_gga(T168, T169, X263, multc50_out_gga(T168, T169, T172)) → U45_gga(T168, T169, X263, addc58_in_gga(T169, T172, X263))
addc58_in_gga(s(T185), T186, s(X300)) → U46_gga(T185, T186, X300, addc58_in_gga(T185, T186, X300))
addc58_in_gga(0, T191, T191) → addc58_out_gga(0, T191, T191)
U46_gga(T185, T186, X300, addc58_out_gga(T185, T186, X300)) → addc58_out_gga(s(T185), T186, s(X300))
U45_gga(T168, T169, X263, addc58_out_gga(T169, T172, X263)) → multc50_out_gga(s(T168), T169, X263)
U37_gg(T122, T123, T154, T152, multc50_out_gga(T151, T152, T157)) → U38_gg(T122, T123, T154, addc12_in_ggg(T152, T157, T154))
U38_gg(T122, T123, T154, addc12_out_ggg(T152, T157, T154)) → evaluatec3_out_gg(*(T122, T123), T154)
evaluatec3_in_gg(*(T122, T123), 0) → U39_gg(T122, T123, evaluatec3_in_gg(T122, 0))
evaluatec3_in_gg(T203, T203) → U41_gg(T203, myintegerc73_in_g(T203))
U41_gg(T203, myintegerc73_out_g(T203)) → evaluatec3_out_gg(T203, T203)
U39_gg(T122, T123, evaluatec3_out_gg(T122, 0)) → U40_gg(T122, T123, evaluatec3_in_ga(T123, T200))
U40_gg(T122, T123, evaluatec3_out_ga(T123, T200)) → evaluatec3_out_gg(*(T122, T123), 0)
U39_ga(T122, T123, evaluatec3_out_gg(T122, 0)) → U40_ga(T122, T123, evaluatec3_in_ga(T123, T200))
U40_ga(T122, T123, evaluatec3_out_ga(T123, T200)) → evaluatec3_out_ga(*(T122, T123), 0)
U35_ga(T122, T123, T154, evaluatec3_out_ga(T122, s(T151))) → U36_ga(T122, T123, T154, T151, evaluatec3_in_ga(T123, T152))
U36_ga(T122, T123, T154, T151, evaluatec3_out_ga(T123, T152)) → U37_ga(T122, T123, T154, T152, multc50_in_gga(T151, T152, T157))
U37_ga(T122, T123, T154, T152, multc50_out_gga(T151, T152, T157)) → U38_ga(T122, T123, T154, addc12_in_gga(T152, T157, T154))
addc12_in_gga(s(T49), T50, s(T52)) → U42_gga(T49, T50, T52, addc12_in_gga(T49, T50, T52))
addc12_in_gga(0, T58, T58) → addc12_out_gga(0, T58, T58)
U42_gga(T49, T50, T52, addc12_out_gga(T49, T50, T52)) → addc12_out_gga(s(T49), T50, s(T52))
U38_ga(T122, T123, T154, addc12_out_gga(T152, T157, T154)) → evaluatec3_out_ga(*(T122, T123), T154)
U32_ga(T71, T72, T74, evaluatec3_out_ga(T71, T77)) → U33_ga(T71, T72, T74, T77, evaluatec3_in_ga(T72, T82))
U33_ga(T71, T72, T74, T77, evaluatec3_out_ga(T72, T82)) → U34_ga(T71, T72, T74, subc28_in_gga(T77, T82, T74))
subc28_in_gga(s(T100), s(T101), T103) → U43_gga(T100, T101, T103, subc28_in_gga(T100, T101, T103))
subc28_in_gga(T109, 0, T109) → subc28_out_gga(T109, 0, T109)
U43_gga(T100, T101, T103, subc28_out_gga(T100, T101, T103)) → subc28_out_gga(s(T100), s(T101), T103)
U34_ga(T71, T72, T74, subc28_out_gga(T77, T82, T74)) → evaluatec3_out_ga(-(T71, T72), T74)
U29_ga(T20, T21, T23, evaluatec3_out_ga(T20, T26)) → U30_ga(T20, T21, T23, T26, evaluatec3_in_ga(T21, T31))
U30_ga(T20, T21, T23, T26, evaluatec3_out_ga(T21, T31)) → U31_ga(T20, T21, T23, addc12_in_gga(T26, T31, T23))
U31_ga(T20, T21, T23, addc12_out_gga(T26, T31, T23)) → evaluatec3_out_ga(+(T20, T21), T23)

The argument filtering Pi contains the following mapping:
+(x1, x2) = +(x1, x2)
evaluatec3_in_ga(x1, x2) = evaluatec3_in_ga(x1)
U29_ga(x1, x2, x3, x4) = U29_ga(x1, x2, x4)
-(x1, x2) = -(x1, x2)
U32_ga(x1, x2, x3, x4) = U32_ga(x1, x2, x4)
*(x1, x2) = *(x1, x2)
U35_ga(x1, x2, x3, x4) = U35_ga(x1, x2, x4)
U39_ga(x1, x2, x3) = U39_ga(x1, x2, x3)
evaluatec3_in_gg(x1, x2) = evaluatec3_in_gg(x1, x2)
U29_gg(x1, x2, x3, x4) = U29_gg(x1, x2, x3, x4)
U41_ga(x1, x2) = U41_ga(x1, x2)
myintegerc73_in_g(x1) = myintegerc73_in_g(x1)
s(x1) = s(x1)
U47_g(x1, x2) = U47_g(x1, x2)
0 = 0
myintegerc73_out_g(x1) = myintegerc73_out_g(x1)
evaluatec3_out_ga(x1, x2) = evaluatec3_out_ga(x1, x2)
U30_gg(x1, x2, x3, x4, x5) = U30_gg(x1, x2, x3, x4, x5)
U31_gg(x1, x2, x3, x4) = U31_gg(x1, x2, x3, x4)
addc12_in_ggg(x1, x2, x3) = addc12_in_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3, x4) = U42_ggg(x1, x2, x3, x4)
addc12_out_ggg(x1, x2, x3) = addc12_out_ggg(x1, x2, x3)
evaluatec3_out_gg(x1, x2) = evaluatec3_out_gg(x1, x2)
U32_gg(x1, x2, x3, x4) = U32_gg(x1, x2, x3, x4)
U33_gg(x1, x2, x3, x4, x5) = U33_gg(x1, x2, x3, x4, x5)
U34_gg(x1, x2, x3, x4) = U34_gg(x1, x2, x3, x4)
subc28_in_ggg(x1, x2, x3) = subc28_in_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3, x4) = U43_ggg(x1, x2, x3, x4)
subc28_out_ggg(x1, x2, x3) = subc28_out_ggg(x1, x2, x3)
U35_gg(x1, x2, x3, x4) = U35_gg(x1, x2, x3, x4)
U36_gg(x1, x2, x3, x4, x5) = U36_gg(x1, x2, x3, x4, x5)
U37_gg(x1, x2, x3, x4, x5) = U37_gg(x1, x2, x3, x4, x5)
multc50_in_gga(x1, x2, x3) = multc50_in_gga(x1, x2)
U44_gga(x1, x2, x3, x4) = U44_gga(x1, x2, x4)
multc50_out_gga(x1, x2, x3) = multc50_out_gga(x1, x2, x3)
U45_gga(x1, x2, x3, x4) = U45_gga(x1, x2, x4)
addc58_in_gga(x1, x2, x3) = addc58_in_gga(x1, x2)
U46_gga(x1, x2, x3, x4) = U46_gga(x1, x2, x4)
addc58_out_gga(x1, x2, x3) = addc58_out_gga(x1, x2, x3)
U38_gg(x1, x2, x3, x4) = U38_gg(x1, x2, x3, x4)
U39_gg(x1, x2, x3) = U39_gg(x1, x2, x3)
U41_gg(x1, x2) = U41_gg(x1, x2)
U40_gg(x1, x2, x3) = U40_gg(x1, x2, x3)
U40_ga(x1, x2, x3) = U40_ga(x1, x2, x3)
U36_ga(x1, x2, x3, x4, x5) = U36_ga(x1, x2, x4, x5)
U37_ga(x1, x2, x3, x4, x5) = U37_ga(x1, x2, x4, x5)
U38_ga(x1, x2, x3, x4) = U38_ga(x1, x2, x4)
addc12_in_gga(x1, x2, x3) = addc12_in_gga(x1, x2)
U42_gga(x1, x2, x3, x4) = U42_gga(x1, x2, x4)
addc12_out_gga(x1, x2, x3) = addc12_out_gga(x1, x2, x3)
U33_ga(x1, x2, x3, x4, x5) = U33_ga(x1, x2, x4, x5)
U34_ga(x1, x2, x3, x4) = U34_ga(x1, x2, x4)
subc28_in_gga(x1, x2, x3) = subc28_in_gga(x1, x2)
U43_gga(x1, x2, x3, x4) = U43_gga(x1, x2, x4)
subc28_out_gga(x1, x2, x3) = subc28_out_gga(x1, x2, x3)
U30_ga(x1, x2, x3, x4, x5) = U30_ga(x1, x2, x4, x5)
U31_ga(x1, x2, x3, x4) = U31_ga(x1, x2, x4)
ADD58_IN_GGA(x1, x2, x3) = ADD58_IN_GGA(x1, x2)

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:

ADD58_IN_GGA(s(T185), T186, s(X300)) → ADD58_IN_GGA(T185, T186, X300)

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

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:

ADD58_IN_GGA(s(T185), T186) → ADD58_IN_GGA(T185, T186)

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:

ADD58_IN_GGA(s(T185), T186) → ADD58_IN_GGA(T185, T186)
The graph contains the following edges 1 > 1, 2 >= 2

(34) YES

(35) Obligation:

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

MULT50_IN_GGA(s(T168), T169, X263) → MULT50_IN_GGA(T168, T169, X262)

The TRS R consists of the following rules:

evaluatec3_in_ga(+(T20, T21), T23) → U29_ga(T20, T21, T23, evaluatec3_in_ga(T20, T26))
evaluatec3_in_ga(-(T71, T72), T74) → U32_ga(T71, T72, T74, evaluatec3_in_ga(T71, T77))
evaluatec3_in_ga(*(T122, T123), T154) → U35_ga(T122, T123, T154, evaluatec3_in_ga(T122, s(T151)))
evaluatec3_in_ga(*(T122, T123), 0) → U39_ga(T122, T123, evaluatec3_in_gg(T122, 0))
evaluatec3_in_gg(+(T20, T21), T23) → U29_gg(T20, T21, T23, evaluatec3_in_ga(T20, T26))
evaluatec3_in_ga(T203, T203) → U41_ga(T203, myintegerc73_in_g(T203))
myintegerc73_in_g(s(T209)) → U47_g(T209, myintegerc73_in_g(T209))
myintegerc73_in_g(0) → myintegerc73_out_g(0)
U47_g(T209, myintegerc73_out_g(T209)) → myintegerc73_out_g(s(T209))
U41_ga(T203, myintegerc73_out_g(T203)) → evaluatec3_out_ga(T203, T203)
U29_gg(T20, T21, T23, evaluatec3_out_ga(T20, T26)) → U30_gg(T20, T21, T23, T26, evaluatec3_in_ga(T21, T31))
U30_gg(T20, T21, T23, T26, evaluatec3_out_ga(T21, T31)) → U31_gg(T20, T21, T23, addc12_in_ggg(T26, T31, T23))
addc12_in_ggg(s(T49), T50, s(T52)) → U42_ggg(T49, T50, T52, addc12_in_ggg(T49, T50, T52))
addc12_in_ggg(0, T58, T58) → addc12_out_ggg(0, T58, T58)
U42_ggg(T49, T50, T52, addc12_out_ggg(T49, T50, T52)) → addc12_out_ggg(s(T49), T50, s(T52))
U31_gg(T20, T21, T23, addc12_out_ggg(T26, T31, T23)) → evaluatec3_out_gg(+(T20, T21), T23)
evaluatec3_in_gg(-(T71, T72), T74) → U32_gg(T71, T72, T74, evaluatec3_in_ga(T71, T77))
U32_gg(T71, T72, T74, evaluatec3_out_ga(T71, T77)) → U33_gg(T71, T72, T74, T77, evaluatec3_in_ga(T72, T82))
U33_gg(T71, T72, T74, T77, evaluatec3_out_ga(T72, T82)) → U34_gg(T71, T72, T74, subc28_in_ggg(T77, T82, T74))
subc28_in_ggg(s(T100), s(T101), T103) → U43_ggg(T100, T101, T103, subc28_in_ggg(T100, T101, T103))
subc28_in_ggg(T109, 0, T109) → subc28_out_ggg(T109, 0, T109)
U43_ggg(T100, T101, T103, subc28_out_ggg(T100, T101, T103)) → subc28_out_ggg(s(T100), s(T101), T103)
U34_gg(T71, T72, T74, subc28_out_ggg(T77, T82, T74)) → evaluatec3_out_gg(-(T71, T72), T74)
evaluatec3_in_gg(*(T122, T123), T154) → U35_gg(T122, T123, T154, evaluatec3_in_ga(T122, s(T151)))
U35_gg(T122, T123, T154, evaluatec3_out_ga(T122, s(T151))) → U36_gg(T122, T123, T154, T151, evaluatec3_in_ga(T123, T152))
U36_gg(T122, T123, T154, T151, evaluatec3_out_ga(T123, T152)) → U37_gg(T122, T123, T154, T152, multc50_in_gga(T151, T152, T157))
multc50_in_gga(s(T168), T169, X263) → U44_gga(T168, T169, X263, multc50_in_gga(T168, T169, T172))
multc50_in_gga(0, T194, 0) → multc50_out_gga(0, T194, 0)
U44_gga(T168, T169, X263, multc50_out_gga(T168, T169, T172)) → U45_gga(T168, T169, X263, addc58_in_gga(T169, T172, X263))
addc58_in_gga(s(T185), T186, s(X300)) → U46_gga(T185, T186, X300, addc58_in_gga(T185, T186, X300))
addc58_in_gga(0, T191, T191) → addc58_out_gga(0, T191, T191)
U46_gga(T185, T186, X300, addc58_out_gga(T185, T186, X300)) → addc58_out_gga(s(T185), T186, s(X300))
U45_gga(T168, T169, X263, addc58_out_gga(T169, T172, X263)) → multc50_out_gga(s(T168), T169, X263)
U37_gg(T122, T123, T154, T152, multc50_out_gga(T151, T152, T157)) → U38_gg(T122, T123, T154, addc12_in_ggg(T152, T157, T154))
U38_gg(T122, T123, T154, addc12_out_ggg(T152, T157, T154)) → evaluatec3_out_gg(*(T122, T123), T154)
evaluatec3_in_gg(*(T122, T123), 0) → U39_gg(T122, T123, evaluatec3_in_gg(T122, 0))
evaluatec3_in_gg(T203, T203) → U41_gg(T203, myintegerc73_in_g(T203))
U41_gg(T203, myintegerc73_out_g(T203)) → evaluatec3_out_gg(T203, T203)
U39_gg(T122, T123, evaluatec3_out_gg(T122, 0)) → U40_gg(T122, T123, evaluatec3_in_ga(T123, T200))
U40_gg(T122, T123, evaluatec3_out_ga(T123, T200)) → evaluatec3_out_gg(*(T122, T123), 0)
U39_ga(T122, T123, evaluatec3_out_gg(T122, 0)) → U40_ga(T122, T123, evaluatec3_in_ga(T123, T200))
U40_ga(T122, T123, evaluatec3_out_ga(T123, T200)) → evaluatec3_out_ga(*(T122, T123), 0)
U35_ga(T122, T123, T154, evaluatec3_out_ga(T122, s(T151))) → U36_ga(T122, T123, T154, T151, evaluatec3_in_ga(T123, T152))
U36_ga(T122, T123, T154, T151, evaluatec3_out_ga(T123, T152)) → U37_ga(T122, T123, T154, T152, multc50_in_gga(T151, T152, T157))
U37_ga(T122, T123, T154, T152, multc50_out_gga(T151, T152, T157)) → U38_ga(T122, T123, T154, addc12_in_gga(T152, T157, T154))
addc12_in_gga(s(T49), T50, s(T52)) → U42_gga(T49, T50, T52, addc12_in_gga(T49, T50, T52))
addc12_in_gga(0, T58, T58) → addc12_out_gga(0, T58, T58)
U42_gga(T49, T50, T52, addc12_out_gga(T49, T50, T52)) → addc12_out_gga(s(T49), T50, s(T52))
U38_ga(T122, T123, T154, addc12_out_gga(T152, T157, T154)) → evaluatec3_out_ga(*(T122, T123), T154)
U32_ga(T71, T72, T74, evaluatec3_out_ga(T71, T77)) → U33_ga(T71, T72, T74, T77, evaluatec3_in_ga(T72, T82))
U33_ga(T71, T72, T74, T77, evaluatec3_out_ga(T72, T82)) → U34_ga(T71, T72, T74, subc28_in_gga(T77, T82, T74))
subc28_in_gga(s(T100), s(T101), T103) → U43_gga(T100, T101, T103, subc28_in_gga(T100, T101, T103))
subc28_in_gga(T109, 0, T109) → subc28_out_gga(T109, 0, T109)
U43_gga(T100, T101, T103, subc28_out_gga(T100, T101, T103)) → subc28_out_gga(s(T100), s(T101), T103)
U34_ga(T71, T72, T74, subc28_out_gga(T77, T82, T74)) → evaluatec3_out_ga(-(T71, T72), T74)
U29_ga(T20, T21, T23, evaluatec3_out_ga(T20, T26)) → U30_ga(T20, T21, T23, T26, evaluatec3_in_ga(T21, T31))
U30_ga(T20, T21, T23, T26, evaluatec3_out_ga(T21, T31)) → U31_ga(T20, T21, T23, addc12_in_gga(T26, T31, T23))
U31_ga(T20, T21, T23, addc12_out_gga(T26, T31, T23)) → evaluatec3_out_ga(+(T20, T21), T23)

The argument filtering Pi contains the following mapping:
+(x1, x2) = +(x1, x2)
evaluatec3_in_ga(x1, x2) = evaluatec3_in_ga(x1)
U29_ga(x1, x2, x3, x4) = U29_ga(x1, x2, x4)
-(x1, x2) = -(x1, x2)
U32_ga(x1, x2, x3, x4) = U32_ga(x1, x2, x4)
*(x1, x2) = *(x1, x2)
U35_ga(x1, x2, x3, x4) = U35_ga(x1, x2, x4)
U39_ga(x1, x2, x3) = U39_ga(x1, x2, x3)
evaluatec3_in_gg(x1, x2) = evaluatec3_in_gg(x1, x2)
U29_gg(x1, x2, x3, x4) = U29_gg(x1, x2, x3, x4)
U41_ga(x1, x2) = U41_ga(x1, x2)
myintegerc73_in_g(x1) = myintegerc73_in_g(x1)
s(x1) = s(x1)
U47_g(x1, x2) = U47_g(x1, x2)
0 = 0
myintegerc73_out_g(x1) = myintegerc73_out_g(x1)
evaluatec3_out_ga(x1, x2) = evaluatec3_out_ga(x1, x2)
U30_gg(x1, x2, x3, x4, x5) = U30_gg(x1, x2, x3, x4, x5)
U31_gg(x1, x2, x3, x4) = U31_gg(x1, x2, x3, x4)
addc12_in_ggg(x1, x2, x3) = addc12_in_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3, x4) = U42_ggg(x1, x2, x3, x4)
addc12_out_ggg(x1, x2, x3) = addc12_out_ggg(x1, x2, x3)
evaluatec3_out_gg(x1, x2) = evaluatec3_out_gg(x1, x2)
U32_gg(x1, x2, x3, x4) = U32_gg(x1, x2, x3, x4)
U33_gg(x1, x2, x3, x4, x5) = U33_gg(x1, x2, x3, x4, x5)
U34_gg(x1, x2, x3, x4) = U34_gg(x1, x2, x3, x4)
subc28_in_ggg(x1, x2, x3) = subc28_in_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3, x4) = U43_ggg(x1, x2, x3, x4)
subc28_out_ggg(x1, x2, x3) = subc28_out_ggg(x1, x2, x3)
U35_gg(x1, x2, x3, x4) = U35_gg(x1, x2, x3, x4)
U36_gg(x1, x2, x3, x4, x5) = U36_gg(x1, x2, x3, x4, x5)
U37_gg(x1, x2, x3, x4, x5) = U37_gg(x1, x2, x3, x4, x5)
multc50_in_gga(x1, x2, x3) = multc50_in_gga(x1, x2)
U44_gga(x1, x2, x3, x4) = U44_gga(x1, x2, x4)
multc50_out_gga(x1, x2, x3) = multc50_out_gga(x1, x2, x3)
U45_gga(x1, x2, x3, x4) = U45_gga(x1, x2, x4)
addc58_in_gga(x1, x2, x3) = addc58_in_gga(x1, x2)
U46_gga(x1, x2, x3, x4) = U46_gga(x1, x2, x4)
addc58_out_gga(x1, x2, x3) = addc58_out_gga(x1, x2, x3)
U38_gg(x1, x2, x3, x4) = U38_gg(x1, x2, x3, x4)
U39_gg(x1, x2, x3) = U39_gg(x1, x2, x3)
U41_gg(x1, x2) = U41_gg(x1, x2)
U40_gg(x1, x2, x3) = U40_gg(x1, x2, x3)
U40_ga(x1, x2, x3) = U40_ga(x1, x2, x3)
U36_ga(x1, x2, x3, x4, x5) = U36_ga(x1, x2, x4, x5)
U37_ga(x1, x2, x3, x4, x5) = U37_ga(x1, x2, x4, x5)
U38_ga(x1, x2, x3, x4) = U38_ga(x1, x2, x4)
addc12_in_gga(x1, x2, x3) = addc12_in_gga(x1, x2)
U42_gga(x1, x2, x3, x4) = U42_gga(x1, x2, x4)
addc12_out_gga(x1, x2, x3) = addc12_out_gga(x1, x2, x3)
U33_ga(x1, x2, x3, x4, x5) = U33_ga(x1, x2, x4, x5)
U34_ga(x1, x2, x3, x4) = U34_ga(x1, x2, x4)
subc28_in_gga(x1, x2, x3) = subc28_in_gga(x1, x2)
U43_gga(x1, x2, x3, x4) = U43_gga(x1, x2, x4)
subc28_out_gga(x1, x2, x3) = subc28_out_gga(x1, x2, x3)
U30_ga(x1, x2, x3, x4, x5) = U30_ga(x1, x2, x4, x5)
U31_ga(x1, x2, x3, x4) = U31_ga(x1, x2, x4)
MULT50_IN_GGA(x1, x2, x3) = MULT50_IN_GGA(x1, x2)

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

(36) UsableRulesProof (EQUIVALENT transformation)

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

(37) Obligation:

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

MULT50_IN_GGA(s(T168), T169, X263) → MULT50_IN_GGA(T168, T169, X262)

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

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

(38) PiDPToQDPProof (SOUND transformation)

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

(39) Obligation:

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

MULT50_IN_GGA(s(T168), T169) → MULT50_IN_GGA(T168, T169)

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

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

MULT50_IN_GGA(s(T168), T169) → MULT50_IN_GGA(T168, T169)
The graph contains the following edges 1 > 1, 2 >= 2

(41) YES

(42) Obligation:

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

EVALUATE3_IN_GA(+(T20, T21), T23) → U2_GA(T20, T21, T23, evaluatec3_in_ga(T20, T26))
U2_GA(T20, T21, T23, evaluatec3_out_ga(T20, T26)) → EVALUATE3_IN_GA(T21, X26)
EVALUATE3_IN_GA(+(T20, T21), T23) → EVALUATE3_IN_GA(T20, X25)
EVALUATE3_IN_GA(-(T71, T72), T74) → EVALUATE3_IN_GA(T71, X101)
EVALUATE3_IN_GA(-(T71, T72), T74) → U7_GA(T71, T72, T74, evaluatec3_in_ga(T71, T77))
U7_GA(T71, T72, T74, evaluatec3_out_ga(T71, T77)) → EVALUATE3_IN_GA(T72, X102)
EVALUATE3_IN_GA(*(T122, T123), T125) → EVALUATE3_IN_GA(T122, X177)
EVALUATE3_IN_GA(*(T122, T123), T125) → U12_GA(T122, T123, T125, evaluatec3_in_ga(T122, T128))
U12_GA(T122, T123, T125, evaluatec3_out_ga(T122, T128)) → EVALUATE3_IN_GA(T123, X178)

The TRS R consists of the following rules:

evaluatec3_in_ga(+(T20, T21), T23) → U29_ga(T20, T21, T23, evaluatec3_in_ga(T20, T26))
evaluatec3_in_ga(-(T71, T72), T74) → U32_ga(T71, T72, T74, evaluatec3_in_ga(T71, T77))
evaluatec3_in_ga(*(T122, T123), T154) → U35_ga(T122, T123, T154, evaluatec3_in_ga(T122, s(T151)))
evaluatec3_in_ga(*(T122, T123), 0) → U39_ga(T122, T123, evaluatec3_in_gg(T122, 0))
evaluatec3_in_gg(+(T20, T21), T23) → U29_gg(T20, T21, T23, evaluatec3_in_ga(T20, T26))
evaluatec3_in_ga(T203, T203) → U41_ga(T203, myintegerc73_in_g(T203))
myintegerc73_in_g(s(T209)) → U47_g(T209, myintegerc73_in_g(T209))
myintegerc73_in_g(0) → myintegerc73_out_g(0)
U47_g(T209, myintegerc73_out_g(T209)) → myintegerc73_out_g(s(T209))
U41_ga(T203, myintegerc73_out_g(T203)) → evaluatec3_out_ga(T203, T203)
U29_gg(T20, T21, T23, evaluatec3_out_ga(T20, T26)) → U30_gg(T20, T21, T23, T26, evaluatec3_in_ga(T21, T31))
U30_gg(T20, T21, T23, T26, evaluatec3_out_ga(T21, T31)) → U31_gg(T20, T21, T23, addc12_in_ggg(T26, T31, T23))
addc12_in_ggg(s(T49), T50, s(T52)) → U42_ggg(T49, T50, T52, addc12_in_ggg(T49, T50, T52))
addc12_in_ggg(0, T58, T58) → addc12_out_ggg(0, T58, T58)
U42_ggg(T49, T50, T52, addc12_out_ggg(T49, T50, T52)) → addc12_out_ggg(s(T49), T50, s(T52))
U31_gg(T20, T21, T23, addc12_out_ggg(T26, T31, T23)) → evaluatec3_out_gg(+(T20, T21), T23)
evaluatec3_in_gg(-(T71, T72), T74) → U32_gg(T71, T72, T74, evaluatec3_in_ga(T71, T77))
U32_gg(T71, T72, T74, evaluatec3_out_ga(T71, T77)) → U33_gg(T71, T72, T74, T77, evaluatec3_in_ga(T72, T82))
U33_gg(T71, T72, T74, T77, evaluatec3_out_ga(T72, T82)) → U34_gg(T71, T72, T74, subc28_in_ggg(T77, T82, T74))
subc28_in_ggg(s(T100), s(T101), T103) → U43_ggg(T100, T101, T103, subc28_in_ggg(T100, T101, T103))
subc28_in_ggg(T109, 0, T109) → subc28_out_ggg(T109, 0, T109)
U43_ggg(T100, T101, T103, subc28_out_ggg(T100, T101, T103)) → subc28_out_ggg(s(T100), s(T101), T103)
U34_gg(T71, T72, T74, subc28_out_ggg(T77, T82, T74)) → evaluatec3_out_gg(-(T71, T72), T74)
evaluatec3_in_gg(*(T122, T123), T154) → U35_gg(T122, T123, T154, evaluatec3_in_ga(T122, s(T151)))
U35_gg(T122, T123, T154, evaluatec3_out_ga(T122, s(T151))) → U36_gg(T122, T123, T154, T151, evaluatec3_in_ga(T123, T152))
U36_gg(T122, T123, T154, T151, evaluatec3_out_ga(T123, T152)) → U37_gg(T122, T123, T154, T152, multc50_in_gga(T151, T152, T157))
multc50_in_gga(s(T168), T169, X263) → U44_gga(T168, T169, X263, multc50_in_gga(T168, T169, T172))
multc50_in_gga(0, T194, 0) → multc50_out_gga(0, T194, 0)
U44_gga(T168, T169, X263, multc50_out_gga(T168, T169, T172)) → U45_gga(T168, T169, X263, addc58_in_gga(T169, T172, X263))
addc58_in_gga(s(T185), T186, s(X300)) → U46_gga(T185, T186, X300, addc58_in_gga(T185, T186, X300))
addc58_in_gga(0, T191, T191) → addc58_out_gga(0, T191, T191)
U46_gga(T185, T186, X300, addc58_out_gga(T185, T186, X300)) → addc58_out_gga(s(T185), T186, s(X300))
U45_gga(T168, T169, X263, addc58_out_gga(T169, T172, X263)) → multc50_out_gga(s(T168), T169, X263)
U37_gg(T122, T123, T154, T152, multc50_out_gga(T151, T152, T157)) → U38_gg(T122, T123, T154, addc12_in_ggg(T152, T157, T154))
U38_gg(T122, T123, T154, addc12_out_ggg(T152, T157, T154)) → evaluatec3_out_gg(*(T122, T123), T154)
evaluatec3_in_gg(*(T122, T123), 0) → U39_gg(T122, T123, evaluatec3_in_gg(T122, 0))
evaluatec3_in_gg(T203, T203) → U41_gg(T203, myintegerc73_in_g(T203))
U41_gg(T203, myintegerc73_out_g(T203)) → evaluatec3_out_gg(T203, T203)
U39_gg(T122, T123, evaluatec3_out_gg(T122, 0)) → U40_gg(T122, T123, evaluatec3_in_ga(T123, T200))
U40_gg(T122, T123, evaluatec3_out_ga(T123, T200)) → evaluatec3_out_gg(*(T122, T123), 0)
U39_ga(T122, T123, evaluatec3_out_gg(T122, 0)) → U40_ga(T122, T123, evaluatec3_in_ga(T123, T200))
U40_ga(T122, T123, evaluatec3_out_ga(T123, T200)) → evaluatec3_out_ga(*(T122, T123), 0)
U35_ga(T122, T123, T154, evaluatec3_out_ga(T122, s(T151))) → U36_ga(T122, T123, T154, T151, evaluatec3_in_ga(T123, T152))
U36_ga(T122, T123, T154, T151, evaluatec3_out_ga(T123, T152)) → U37_ga(T122, T123, T154, T152, multc50_in_gga(T151, T152, T157))
U37_ga(T122, T123, T154, T152, multc50_out_gga(T151, T152, T157)) → U38_ga(T122, T123, T154, addc12_in_gga(T152, T157, T154))
addc12_in_gga(s(T49), T50, s(T52)) → U42_gga(T49, T50, T52, addc12_in_gga(T49, T50, T52))
addc12_in_gga(0, T58, T58) → addc12_out_gga(0, T58, T58)
U42_gga(T49, T50, T52, addc12_out_gga(T49, T50, T52)) → addc12_out_gga(s(T49), T50, s(T52))
U38_ga(T122, T123, T154, addc12_out_gga(T152, T157, T154)) → evaluatec3_out_ga(*(T122, T123), T154)
U32_ga(T71, T72, T74, evaluatec3_out_ga(T71, T77)) → U33_ga(T71, T72, T74, T77, evaluatec3_in_ga(T72, T82))
U33_ga(T71, T72, T74, T77, evaluatec3_out_ga(T72, T82)) → U34_ga(T71, T72, T74, subc28_in_gga(T77, T82, T74))
subc28_in_gga(s(T100), s(T101), T103) → U43_gga(T100, T101, T103, subc28_in_gga(T100, T101, T103))
subc28_in_gga(T109, 0, T109) → subc28_out_gga(T109, 0, T109)
U43_gga(T100, T101, T103, subc28_out_gga(T100, T101, T103)) → subc28_out_gga(s(T100), s(T101), T103)
U34_ga(T71, T72, T74, subc28_out_gga(T77, T82, T74)) → evaluatec3_out_ga(-(T71, T72), T74)
U29_ga(T20, T21, T23, evaluatec3_out_ga(T20, T26)) → U30_ga(T20, T21, T23, T26, evaluatec3_in_ga(T21, T31))
U30_ga(T20, T21, T23, T26, evaluatec3_out_ga(T21, T31)) → U31_ga(T20, T21, T23, addc12_in_gga(T26, T31, T23))
U31_ga(T20, T21, T23, addc12_out_gga(T26, T31, T23)) → evaluatec3_out_ga(+(T20, T21), T23)

The argument filtering Pi contains the following mapping:
+(x1, x2) = +(x1, x2)
evaluatec3_in_ga(x1, x2) = evaluatec3_in_ga(x1)
U29_ga(x1, x2, x3, x4) = U29_ga(x1, x2, x4)
-(x1, x2) = -(x1, x2)
U32_ga(x1, x2, x3, x4) = U32_ga(x1, x2, x4)
*(x1, x2) = *(x1, x2)
U35_ga(x1, x2, x3, x4) = U35_ga(x1, x2, x4)
U39_ga(x1, x2, x3) = U39_ga(x1, x2, x3)
evaluatec3_in_gg(x1, x2) = evaluatec3_in_gg(x1, x2)
U29_gg(x1, x2, x3, x4) = U29_gg(x1, x2, x3, x4)
U41_ga(x1, x2) = U41_ga(x1, x2)
myintegerc73_in_g(x1) = myintegerc73_in_g(x1)
s(x1) = s(x1)
U47_g(x1, x2) = U47_g(x1, x2)
0 = 0
myintegerc73_out_g(x1) = myintegerc73_out_g(x1)
evaluatec3_out_ga(x1, x2) = evaluatec3_out_ga(x1, x2)
U30_gg(x1, x2, x3, x4, x5) = U30_gg(x1, x2, x3, x4, x5)
U31_gg(x1, x2, x3, x4) = U31_gg(x1, x2, x3, x4)
addc12_in_ggg(x1, x2, x3) = addc12_in_ggg(x1, x2, x3)
U42_ggg(x1, x2, x3, x4) = U42_ggg(x1, x2, x3, x4)
addc12_out_ggg(x1, x2, x3) = addc12_out_ggg(x1, x2, x3)
evaluatec3_out_gg(x1, x2) = evaluatec3_out_gg(x1, x2)
U32_gg(x1, x2, x3, x4) = U32_gg(x1, x2, x3, x4)
U33_gg(x1, x2, x3, x4, x5) = U33_gg(x1, x2, x3, x4, x5)
U34_gg(x1, x2, x3, x4) = U34_gg(x1, x2, x3, x4)
subc28_in_ggg(x1, x2, x3) = subc28_in_ggg(x1, x2, x3)
U43_ggg(x1, x2, x3, x4) = U43_ggg(x1, x2, x3, x4)
subc28_out_ggg(x1, x2, x3) = subc28_out_ggg(x1, x2, x3)
U35_gg(x1, x2, x3, x4) = U35_gg(x1, x2, x3, x4)
U36_gg(x1, x2, x3, x4, x5) = U36_gg(x1, x2, x3, x4, x5)
U37_gg(x1, x2, x3, x4, x5) = U37_gg(x1, x2, x3, x4, x5)
multc50_in_gga(x1, x2, x3) = multc50_in_gga(x1, x2)
U44_gga(x1, x2, x3, x4) = U44_gga(x1, x2, x4)
multc50_out_gga(x1, x2, x3) = multc50_out_gga(x1, x2, x3)
U45_gga(x1, x2, x3, x4) = U45_gga(x1, x2, x4)
addc58_in_gga(x1, x2, x3) = addc58_in_gga(x1, x2)
U46_gga(x1, x2, x3, x4) = U46_gga(x1, x2, x4)
addc58_out_gga(x1, x2, x3) = addc58_out_gga(x1, x2, x3)
U38_gg(x1, x2, x3, x4) = U38_gg(x1, x2, x3, x4)
U39_gg(x1, x2, x3) = U39_gg(x1, x2, x3)
U41_gg(x1, x2) = U41_gg(x1, x2)
U40_gg(x1, x2, x3) = U40_gg(x1, x2, x3)
U40_ga(x1, x2, x3) = U40_ga(x1, x2, x3)
U36_ga(x1, x2, x3, x4, x5) = U36_ga(x1, x2, x4, x5)
U37_ga(x1, x2, x3, x4, x5) = U37_ga(x1, x2, x4, x5)
U38_ga(x1, x2, x3, x4) = U38_ga(x1, x2, x4)
addc12_in_gga(x1, x2, x3) = addc12_in_gga(x1, x2)
U42_gga(x1, x2, x3, x4) = U42_gga(x1, x2, x4)
addc12_out_gga(x1, x2, x3) = addc12_out_gga(x1, x2, x3)
U33_ga(x1, x2, x3, x4, x5) = U33_ga(x1, x2, x4, x5)
U34_ga(x1, x2, x3, x4) = U34_ga(x1, x2, x4)
subc28_in_gga(x1, x2, x3) = subc28_in_gga(x1, x2)
U43_gga(x1, x2, x3, x4) = U43_gga(x1, x2, x4)
subc28_out_gga(x1, x2, x3) = subc28_out_gga(x1, x2, x3)
U30_ga(x1, x2, x3, x4, x5) = U30_ga(x1, x2, x4, x5)
U31_ga(x1, x2, x3, x4) = U31_ga(x1, x2, x4)
EVALUATE3_IN_GA(x1, x2) = EVALUATE3_IN_GA(x1)
U2_GA(x1, x2, x3, x4) = U2_GA(x1, x2, x4)
U7_GA(x1, x2, x3, x4) = U7_GA(x1, x2, x4)
U12_GA(x1, x2, x3, x4) = U12_GA(x1, x2, x4)

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

(43) PiDPToQDPProof (SOUND transformation)

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

(44) Obligation:

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

EVALUATE3_IN_GA(+(T20, T21)) → U2_GA(T20, T21, evaluatec3_in_ga(T20))
U2_GA(T20, T21, evaluatec3_out_ga(T20, T26)) → EVALUATE3_IN_GA(T21)
EVALUATE3_IN_GA(+(T20, T21)) → EVALUATE3_IN_GA(T20)
EVALUATE3_IN_GA(-(T71, T72)) → EVALUATE3_IN_GA(T71)
EVALUATE3_IN_GA(-(T71, T72)) → U7_GA(T71, T72, evaluatec3_in_ga(T71))
U7_GA(T71, T72, evaluatec3_out_ga(T71, T77)) → EVALUATE3_IN_GA(T72)
EVALUATE3_IN_GA(*(T122, T123)) → EVALUATE3_IN_GA(T122)
EVALUATE3_IN_GA(*(T122, T123)) → U12_GA(T122, T123, evaluatec3_in_ga(T122))
U12_GA(T122, T123, evaluatec3_out_ga(T122, T128)) → EVALUATE3_IN_GA(T123)

The TRS R consists of the following rules:

evaluatec3_in_ga(+(T20, T21)) → U29_ga(T20, T21, evaluatec3_in_ga(T20))
evaluatec3_in_ga(-(T71, T72)) → U32_ga(T71, T72, evaluatec3_in_ga(T71))
evaluatec3_in_ga(*(T122, T123)) → U35_ga(T122, T123, evaluatec3_in_ga(T122))
evaluatec3_in_ga(*(T122, T123)) → U39_ga(T122, T123, evaluatec3_in_gg(T122, 0))
evaluatec3_in_gg(+(T20, T21), T23) → U29_gg(T20, T21, T23, evaluatec3_in_ga(T20))
evaluatec3_in_ga(T203) → U41_ga(T203, myintegerc73_in_g(T203))
myintegerc73_in_g(s(T209)) → U47_g(T209, myintegerc73_in_g(T209))
myintegerc73_in_g(0) → myintegerc73_out_g(0)
U47_g(T209, myintegerc73_out_g(T209)) → myintegerc73_out_g(s(T209))
U41_ga(T203, myintegerc73_out_g(T203)) → evaluatec3_out_ga(T203, T203)
U29_gg(T20, T21, T23, evaluatec3_out_ga(T20, T26)) → U30_gg(T20, T21, T23, T26, evaluatec3_in_ga(T21))
U30_gg(T20, T21, T23, T26, evaluatec3_out_ga(T21, T31)) → U31_gg(T20, T21, T23, addc12_in_ggg(T26, T31, T23))
addc12_in_ggg(s(T49), T50, s(T52)) → U42_ggg(T49, T50, T52, addc12_in_ggg(T49, T50, T52))
addc12_in_ggg(0, T58, T58) → addc12_out_ggg(0, T58, T58)
U42_ggg(T49, T50, T52, addc12_out_ggg(T49, T50, T52)) → addc12_out_ggg(s(T49), T50, s(T52))
U31_gg(T20, T21, T23, addc12_out_ggg(T26, T31, T23)) → evaluatec3_out_gg(+(T20, T21), T23)
evaluatec3_in_gg(-(T71, T72), T74) → U32_gg(T71, T72, T74, evaluatec3_in_ga(T71))
U32_gg(T71, T72, T74, evaluatec3_out_ga(T71, T77)) → U33_gg(T71, T72, T74, T77, evaluatec3_in_ga(T72))
U33_gg(T71, T72, T74, T77, evaluatec3_out_ga(T72, T82)) → U34_gg(T71, T72, T74, subc28_in_ggg(T77, T82, T74))
subc28_in_ggg(s(T100), s(T101), T103) → U43_ggg(T100, T101, T103, subc28_in_ggg(T100, T101, T103))
subc28_in_ggg(T109, 0, T109) → subc28_out_ggg(T109, 0, T109)
U43_ggg(T100, T101, T103, subc28_out_ggg(T100, T101, T103)) → subc28_out_ggg(s(T100), s(T101), T103)
U34_gg(T71, T72, T74, subc28_out_ggg(T77, T82, T74)) → evaluatec3_out_gg(-(T71, T72), T74)
evaluatec3_in_gg(*(T122, T123), T154) → U35_gg(T122, T123, T154, evaluatec3_in_ga(T122))
U35_gg(T122, T123, T154, evaluatec3_out_ga(T122, s(T151))) → U36_gg(T122, T123, T154, T151, evaluatec3_in_ga(T123))
U36_gg(T122, T123, T154, T151, evaluatec3_out_ga(T123, T152)) → U37_gg(T122, T123, T154, T152, multc50_in_gga(T151, T152))
multc50_in_gga(s(T168), T169) → U44_gga(T168, T169, multc50_in_gga(T168, T169))
multc50_in_gga(0, T194) → multc50_out_gga(0, T194, 0)
U44_gga(T168, T169, multc50_out_gga(T168, T169, T172)) → U45_gga(T168, T169, addc58_in_gga(T169, T172))
addc58_in_gga(s(T185), T186) → U46_gga(T185, T186, addc58_in_gga(T185, T186))
addc58_in_gga(0, T191) → addc58_out_gga(0, T191, T191)
U46_gga(T185, T186, addc58_out_gga(T185, T186, X300)) → addc58_out_gga(s(T185), T186, s(X300))
U45_gga(T168, T169, addc58_out_gga(T169, T172, X263)) → multc50_out_gga(s(T168), T169, X263)
U37_gg(T122, T123, T154, T152, multc50_out_gga(T151, T152, T157)) → U38_gg(T122, T123, T154, addc12_in_ggg(T152, T157, T154))
U38_gg(T122, T123, T154, addc12_out_ggg(T152, T157, T154)) → evaluatec3_out_gg(*(T122, T123), T154)
evaluatec3_in_gg(*(T122, T123), 0) → U39_gg(T122, T123, evaluatec3_in_gg(T122, 0))
evaluatec3_in_gg(T203, T203) → U41_gg(T203, myintegerc73_in_g(T203))
U41_gg(T203, myintegerc73_out_g(T203)) → evaluatec3_out_gg(T203, T203)
U39_gg(T122, T123, evaluatec3_out_gg(T122, 0)) → U40_gg(T122, T123, evaluatec3_in_ga(T123))
U40_gg(T122, T123, evaluatec3_out_ga(T123, T200)) → evaluatec3_out_gg(*(T122, T123), 0)
U39_ga(T122, T123, evaluatec3_out_gg(T122, 0)) → U40_ga(T122, T123, evaluatec3_in_ga(T123))
U40_ga(T122, T123, evaluatec3_out_ga(T123, T200)) → evaluatec3_out_ga(*(T122, T123), 0)
U35_ga(T122, T123, evaluatec3_out_ga(T122, s(T151))) → U36_ga(T122, T123, T151, evaluatec3_in_ga(T123))
U36_ga(T122, T123, T151, evaluatec3_out_ga(T123, T152)) → U37_ga(T122, T123, T152, multc50_in_gga(T151, T152))
U37_ga(T122, T123, T152, multc50_out_gga(T151, T152, T157)) → U38_ga(T122, T123, addc12_in_gga(T152, T157))
addc12_in_gga(s(T49), T50) → U42_gga(T49, T50, addc12_in_gga(T49, T50))
addc12_in_gga(0, T58) → addc12_out_gga(0, T58, T58)
U42_gga(T49, T50, addc12_out_gga(T49, T50, T52)) → addc12_out_gga(s(T49), T50, s(T52))
U38_ga(T122, T123, addc12_out_gga(T152, T157, T154)) → evaluatec3_out_ga(*(T122, T123), T154)
U32_ga(T71, T72, evaluatec3_out_ga(T71, T77)) → U33_ga(T71, T72, T77, evaluatec3_in_ga(T72))
U33_ga(T71, T72, T77, evaluatec3_out_ga(T72, T82)) → U34_ga(T71, T72, subc28_in_gga(T77, T82))
subc28_in_gga(s(T100), s(T101)) → U43_gga(T100, T101, subc28_in_gga(T100, T101))
subc28_in_gga(T109, 0) → subc28_out_gga(T109, 0, T109)
U43_gga(T100, T101, subc28_out_gga(T100, T101, T103)) → subc28_out_gga(s(T100), s(T101), T103)
U34_ga(T71, T72, subc28_out_gga(T77, T82, T74)) → evaluatec3_out_ga(-(T71, T72), T74)
U29_ga(T20, T21, evaluatec3_out_ga(T20, T26)) → U30_ga(T20, T21, T26, evaluatec3_in_ga(T21))
U30_ga(T20, T21, T26, evaluatec3_out_ga(T21, T31)) → U31_ga(T20, T21, addc12_in_gga(T26, T31))
U31_ga(T20, T21, addc12_out_gga(T26, T31, T23)) → evaluatec3_out_ga(+(T20, T21), T23)

The set Q consists of the following terms:

evaluatec3_in_ga(x0)
evaluatec3_in_gg(x0, x1)
myintegerc73_in_g(x0)
U47_g(x0, x1)
U41_ga(x0, x1)
U29_gg(x0, x1, x2, x3)
U30_gg(x0, x1, x2, x3, x4)
addc12_in_ggg(x0, x1, x2)
U42_ggg(x0, x1, x2, x3)
U31_gg(x0, x1, x2, x3)
U32_gg(x0, x1, x2, x3)
U33_gg(x0, x1, x2, x3, x4)
subc28_in_ggg(x0, x1, x2)
U43_ggg(x0, x1, x2, x3)
U34_gg(x0, x1, x2, x3)
U35_gg(x0, x1, x2, x3)
U36_gg(x0, x1, x2, x3, x4)
multc50_in_gga(x0, x1)
U44_gga(x0, x1, x2)
addc58_in_gga(x0, x1)
U46_gga(x0, x1, x2)
U45_gga(x0, x1, x2)
U37_gg(x0, x1, x2, x3, x4)
U38_gg(x0, x1, x2, x3)
U41_gg(x0, x1)
U39_gg(x0, x1, x2)
U40_gg(x0, x1, x2)
U39_ga(x0, x1, x2)
U40_ga(x0, x1, x2)
U35_ga(x0, x1, x2)
U36_ga(x0, x1, x2, x3)
U37_ga(x0, x1, x2, x3)
addc12_in_gga(x0, x1)
U42_gga(x0, x1, x2)
U38_ga(x0, x1, x2)
U32_ga(x0, x1, x2)
U33_ga(x0, x1, x2, x3)
subc28_in_gga(x0, x1)
U43_gga(x0, x1, x2)
U34_ga(x0, x1, x2)
U29_ga(x0, x1, x2)
U30_ga(x0, x1, x2, x3)
U31_ga(x0, x1, x2)

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

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

U2_GA(T20, T21, evaluatec3_out_ga(T20, T26)) → EVALUATE3_IN_GA(T21)
The graph contains the following edges 2 >= 1
EVALUATE3_IN_GA(+(T20, T21)) → U2_GA(T20, T21, evaluatec3_in_ga(T20))
The graph contains the following edges 1 > 1, 1 > 2
U7_GA(T71, T72, evaluatec3_out_ga(T71, T77)) → EVALUATE3_IN_GA(T72)
The graph contains the following edges 2 >= 1
U12_GA(T122, T123, evaluatec3_out_ga(T122, T128)) → EVALUATE3_IN_GA(T123)
The graph contains the following edges 2 >= 1
EVALUATE3_IN_GA(-(T71, T72)) → U7_GA(T71, T72, evaluatec3_in_ga(T71))
The graph contains the following edges 1 > 1, 1 > 2
EVALUATE3_IN_GA(*(T122, T123)) → U12_GA(T122, T123, evaluatec3_in_ga(T122))
The graph contains the following edges 1 > 1, 1 > 2
EVALUATE3_IN_GA(+(T20, T21)) → EVALUATE3_IN_GA(T20)
The graph contains the following edges 1 > 1
EVALUATE3_IN_GA(-(T71, T72)) → EVALUATE3_IN_GA(T71)
The graph contains the following edges 1 > 1
EVALUATE3_IN_GA(*(T122, T123)) → EVALUATE3_IN_GA(T122)
The graph contains the following edges 1 > 1

(0) Obligation:

(1) PrologToDTProblemTransformerProof (SOUND transformation)

(2) Obligation:

(3) TriplesToPiDPProof (SOUND transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) PiDPToQDPProof (SOUND transformation)

(11) Obligation:

(12) QDPSizeChangeProof (EQUIVALENT transformation)

(13) YES

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) PiDPToQDPProof (EQUIVALENT transformation)

(18) Obligation:

(19) QDPSizeChangeProof (EQUIVALENT transformation)

(20) YES

(21) Obligation:

(22) UsableRulesProof (EQUIVALENT transformation)

(23) Obligation:

(24) PiDPToQDPProof (SOUND transformation)

(25) Obligation:

(26) QDPSizeChangeProof (EQUIVALENT transformation)

(27) YES

(28) Obligation:

(29) UsableRulesProof (EQUIVALENT transformation)

(30) Obligation:

(31) PiDPToQDPProof (SOUND transformation)

(32) Obligation:

(33) QDPSizeChangeProof (EQUIVALENT transformation)

(34) YES

(35) Obligation:

(36) UsableRulesProof (EQUIVALENT transformation)

(37) Obligation:

(38) PiDPToQDPProof (SOUND transformation)

(39) Obligation:

(40) QDPSizeChangeProof (EQUIVALENT transformation)

(41) YES

(42) Obligation:

(43) PiDPToQDPProof (SOUND transformation)

(44) Obligation:

(45) QDPSizeChangeProof (EQUIVALENT transformation)

(46) YES