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

(0) Obligation:

Clauses:

d(X, X, 1).
d(T, X1, 0) :- isnumber(T).
d(times(U, V), X, +(times(B, U), times(A, V))) :- ','(d(U, X, A), d(V, X, B)).
d(div(U, V), X, W) :- d(times(U, power(V, p(0))), X, W).
d(power(U, V), X, times(V, times(W, power(U, p(V))))) :- ','(isnumber(V), d(U, X, W)).
isnumber(0).
isnumber(s(X)) :- isnumber(X).
isnumber(p(X)) :- isnumber(X).

Query: d(g,g,a)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="3: d(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: d(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | d(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | d(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | d(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | d(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: d(T1, T2, T3), SCOPE: 1, CLAUSE: 0\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: d(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | d(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | d(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | d(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: d(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: d(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | d(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | d(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: isnumber(T17)\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: isnumber(T17), SCOPE: 2, CLAUSE: 5 | isnumber(T17), SCOPE: 2, CLAUSE: 6 | isnumber(T17), SCOPE: 2, CLAUSE: 7\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: isnumber(T17), SCOPE: 2, CLAUSE: 5\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: isnumber(T17), SCOPE: 2, CLAUSE: 6 | isnumber(T17), SCOPE: 2, CLAUSE: 7\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: isnumber(T17), SCOPE: 2, CLAUSE: 6\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: isnumber(T17), SCOPE: 2, CLAUSE: 7\n\nT17 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: isnumber(T23)\n\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: isnumber(T26)\n\nT26 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: d(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: d(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | d(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: ','(d(T47, T49, T52), d(T48, T49, T53))\n\nT47 is ground\nT48 is ground\nT49 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: d(T47, T49, T52)\n\nT47 is ground\nT49 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: d(T48, T49, T56)\n\nT48 is ground\nT49 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: d(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: d(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: d(times(T77, power(T78, p(0))), T79, T81)\n\nT77 is ground\nT78 is ground\nT79 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: ','(isnumber(T95), d(T94, T96, T98))\n\nT94 is ground\nT95 is ground\nT96 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: isnumber(T95)\n\nT95 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: d(T94, T96, T98)\n\nT94 is ground\nT96 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 130 [arrowhead = none ];
130 -> 4;

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

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

133 [label="EVAL with clause\nd(X6, X6, 1).\nand substitutionT1 -> T8,\nX6 -> T8,\nT2 -> T8,\nT3 -> 1", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 133 [arrowhead = none ];
133 -> 10;

134 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
7 -> 134 [arrowhead = none ];
134 -> 12;

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

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

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

138 [label="EVAL with clause\nd(X15, X16, 0) :- isnumber(X15).\nand substitutionT1 -> T17,\nX15 -> T17,\nT2 -> T18,\nX16 -> T18,\nT3 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
21 -> 138 [arrowhead = none ];
138 -> 32;

139 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
21 -> 139 [arrowhead = none ];
139 -> 34;

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

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

142 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
32 -> 142 [arrowhead = none ];
142 -> 47;

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

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

145 [label="EVAL with clause\nisnumber(0).\nand substitutionT17 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
51 -> 145 [arrowhead = none ];
145 -> 57;

146 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
51 -> 146 [arrowhead = none ];
146 -> 60;

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

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

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

150 [label="EVAL with clause\nisnumber(s(X21)) :- isnumber(X21).\nand substitutionX21 -> T23,\nT17 -> s(T23)", fontsize=14, style = filled, fillcolor = lightblue];
65 -> 150 [arrowhead = none ];
150 -> 69;

151 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
65 -> 151 [arrowhead = none ];
151 -> 71;

152 [label="EVAL with clause\nisnumber(p(X24)) :- isnumber(X24).\nand substitutionX24 -> T26,\nT17 -> p(T26)", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 152 [arrowhead = none ];
152 -> 77;

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

154 [label="INSTANCE with matching:\nT17 -> T23", fontsize=14, style = filled, fillcolor = lightgrey];
69 -> 154 [arrowhead = none , style=dashed];
154 -> 32[style=dashed];

155 [label="INSTANCE with matching:\nT17 -> T26", fontsize=14, style = filled, fillcolor = lightgrey];
77 -> 155 [arrowhead = none , style=dashed];
155 -> 32[style=dashed];

156 [label="EVAL with clause\nd(times(X45, X46), X47, +(times(X48, X45), times(X49, X46))) :- ','(d(X45, X47, X49), d(X46, X47, X48)).\nand substitutionX45 -> T47,\nX46 -> T48,\nT1 -> times(T47, T48),\nT2 -> T49,\nX47 -> T49,\nX48 -> T53,\nX49 -> T52,\nT3 -> +(times(T53, T47), times(T52, T48)),\nT51 -> T52,\nT50 -> T53", fontsize=14, style = filled, fillcolor = lightblue];
85 -> 156 [arrowhead = none ];
156 -> 96;

157 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
85 -> 157 [arrowhead = none ];
157 -> 97;

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

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

160 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
96 -> 160 [arrowhead = none ];
160 -> 102;

161 [label="SPLIT 2\nnew knowledge:\nT47 is ground\nT49 is ground\nT52 is ground\nreplacements:T53 -> T56", fontsize=14, style = filled, fillcolor = violet];
96 -> 161 [arrowhead = none ];
161 -> 103;

162 [label="INSTANCE with matching:\nT1 -> T47\nT2 -> T49\nT3 -> T52", fontsize=14, style = filled, fillcolor = lightgrey];
102 -> 162 [arrowhead = none , style=dashed];
162 -> 3[style=dashed];

163 [label="INSTANCE with matching:\nT1 -> T48\nT2 -> T49\nT3 -> T56", fontsize=14, style = filled, fillcolor = lightgrey];
103 -> 163 [arrowhead = none , style=dashed];
163 -> 3[style=dashed];

164 [label="EVAL with clause\nd(div(X72, X73), X74, X75) :- d(times(X72, power(X73, p(0))), X74, X75).\nand substitutionX72 -> T77,\nX73 -> T78,\nT1 -> div(T77, T78),\nT2 -> T79,\nX74 -> T79,\nT3 -> T81,\nX75 -> T81,\nT80 -> T81", fontsize=14, style = filled, fillcolor = lightblue];
110 -> 164 [arrowhead = none ];
164 -> 117;

165 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
110 -> 165 [arrowhead = none ];
165 -> 119;

166 [label="EVAL with clause\nd(power(X86, X87), X88, times(X87, times(X89, power(X86, p(X87))))) :- ','(isnumber(X87), d(X86, X88, X89)).\nand substitutionX86 -> T94,\nX87 -> T95,\nT1 -> power(T94, T95),\nT2 -> T96,\nX88 -> T96,\nX89 -> T98,\nT3 -> times(T95, times(T98, power(T94, p(T95)))),\nT97 -> T98", fontsize=14, style = filled, fillcolor = lightblue];
111 -> 166 [arrowhead = none ];
166 -> 124;

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

168 [label="INSTANCE with matching:\nT1 -> times(T77, power(T78, p(0)))\nT2 -> T79\nT3 -> T81", fontsize=14, style = filled, fillcolor = lightgrey];
117 -> 168 [arrowhead = none , style=dashed];
168 -> 3[style=dashed];

169 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
124 -> 169 [arrowhead = none ];
169 -> 128;

170 [label="SPLIT 2\nnew knowledge:\nT95 is ground", fontsize=14, style = filled, fillcolor = violet];
124 -> 170 [arrowhead = none ];
170 -> 129;

171 [label="INSTANCE with matching:\nT17 -> T95", fontsize=14, style = filled, fillcolor = lightgrey];
128 -> 171 [arrowhead = none , style=dashed];
171 -> 32[style=dashed];

172 [label="INSTANCE with matching:\nT1 -> T94\nT2 -> T96\nT3 -> T98", fontsize=14, style = filled, fillcolor = lightgrey];
129 -> 172 [arrowhead = none , style=dashed];
172 -> 3[style=dashed];

}

(2) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

f3_in(T8, T8) → f3_out1(1)
f3_in(T17, T18) → U1(f32_in(T17), T17, T18)
U1(f32_out1, T17, T18) → f3_out1(0)
f3_in(times(T47, T48), T49) → U2(f96_in(T47, T49, T48), times(T47, T48), T49)
U2(f96_out1(T52, T53), times(T47, T48), T49) → f3_out1(+(times(T53, T47), times(T52, T48)))
f3_in(div(T77, T78), T79) → U3(f3_in(times(T77, power(T78, p(0))), T79), div(T77, T78), T79)
U3(f3_out1(T81), div(T77, T78), T79) → f3_out1(T81)
f3_in(power(T94, T95), T96) → U4(f124_in(T95, T94, T96), power(T94, T95), T96)
U4(f124_out1(T98), power(T94, T95), T96) → f3_out1(times(T95, times(T98, power(T94, p(T95)))))
f32_in(0) → f32_out1
f32_in(s(T23)) → U5(f32_in(T23), s(T23))
U5(f32_out1, s(T23)) → f32_out1
f32_in(p(T26)) → U6(f32_in(T26), p(T26))
U6(f32_out1, p(T26)) → f32_out1
f96_in(T47, T49, T48) → U7(f3_in(T47, T49), T47, T49, T48)
U7(f3_out1(T52), T47, T49, T48) → U8(f3_in(T48, T49), T47, T49, T48, T52)
U8(f3_out1(T56), T47, T49, T48, T52) → f96_out1(T52, T56)
f124_in(T95, T94, T96) → U9(f32_in(T95), T95, T94, T96)
U9(f32_out1, T95, T94, T96) → U10(f3_in(T94, T96), T95, T94, T96)
U10(f3_out1(T98), T95, T94, T96) → f124_out1(T98)

Q is empty.

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(4) Obligation:

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

F3_IN(T17, T18) → U1¹(f32_in(T17), T17, T18)
F3_IN(T17, T18) → F32_IN(T17)
F3_IN(times(T47, T48), T49) → U2¹(f96_in(T47, T49, T48), times(T47, T48), T49)
F3_IN(times(T47, T48), T49) → F96_IN(T47, T49, T48)
F3_IN(div(T77, T78), T79) → U3¹(f3_in(times(T77, power(T78, p(0))), T79), div(T77, T78), T79)
F3_IN(div(T77, T78), T79) → F3_IN(times(T77, power(T78, p(0))), T79)
F3_IN(power(T94, T95), T96) → U4¹(f124_in(T95, T94, T96), power(T94, T95), T96)
F3_IN(power(T94, T95), T96) → F124_IN(T95, T94, T96)
F32_IN(s(T23)) → U5¹(f32_in(T23), s(T23))
F32_IN(s(T23)) → F32_IN(T23)
F32_IN(p(T26)) → U6¹(f32_in(T26), p(T26))
F32_IN(p(T26)) → F32_IN(T26)
F96_IN(T47, T49, T48) → U7¹(f3_in(T47, T49), T47, T49, T48)
F96_IN(T47, T49, T48) → F3_IN(T47, T49)
U7¹(f3_out1(T52), T47, T49, T48) → U8¹(f3_in(T48, T49), T47, T49, T48, T52)
U7¹(f3_out1(T52), T47, T49, T48) → F3_IN(T48, T49)
F124_IN(T95, T94, T96) → U9¹(f32_in(T95), T95, T94, T96)
F124_IN(T95, T94, T96) → F32_IN(T95)
U9¹(f32_out1, T95, T94, T96) → U10¹(f3_in(T94, T96), T95, T94, T96)
U9¹(f32_out1, T95, T94, T96) → F3_IN(T94, T96)

The TRS R consists of the following rules:

f3_in(T8, T8) → f3_out1(1)
f3_in(T17, T18) → U1(f32_in(T17), T17, T18)
U1(f32_out1, T17, T18) → f3_out1(0)
f3_in(times(T47, T48), T49) → U2(f96_in(T47, T49, T48), times(T47, T48), T49)
U2(f96_out1(T52, T53), times(T47, T48), T49) → f3_out1(+(times(T53, T47), times(T52, T48)))
f3_in(div(T77, T78), T79) → U3(f3_in(times(T77, power(T78, p(0))), T79), div(T77, T78), T79)
U3(f3_out1(T81), div(T77, T78), T79) → f3_out1(T81)
f3_in(power(T94, T95), T96) → U4(f124_in(T95, T94, T96), power(T94, T95), T96)
U4(f124_out1(T98), power(T94, T95), T96) → f3_out1(times(T95, times(T98, power(T94, p(T95)))))
f32_in(0) → f32_out1
f32_in(s(T23)) → U5(f32_in(T23), s(T23))
U5(f32_out1, s(T23)) → f32_out1
f32_in(p(T26)) → U6(f32_in(T26), p(T26))
U6(f32_out1, p(T26)) → f32_out1
f96_in(T47, T49, T48) → U7(f3_in(T47, T49), T47, T49, T48)
U7(f3_out1(T52), T47, T49, T48) → U8(f3_in(T48, T49), T47, T49, T48, T52)
U8(f3_out1(T56), T47, T49, T48, T52) → f96_out1(T52, T56)
f124_in(T95, T94, T96) → U9(f32_in(T95), T95, T94, T96)
U9(f32_out1, T95, T94, T96) → U10(f3_in(T94, T96), T95, T94, T96)
U10(f3_out1(T98), T95, T94, T96) → f124_out1(T98)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

F32_IN(p(T26)) → F32_IN(T26)
F32_IN(s(T23)) → F32_IN(T23)

The TRS R consists of the following rules:

f3_in(T8, T8) → f3_out1(1)
f3_in(T17, T18) → U1(f32_in(T17), T17, T18)
U1(f32_out1, T17, T18) → f3_out1(0)
f3_in(times(T47, T48), T49) → U2(f96_in(T47, T49, T48), times(T47, T48), T49)
U2(f96_out1(T52, T53), times(T47, T48), T49) → f3_out1(+(times(T53, T47), times(T52, T48)))
f3_in(div(T77, T78), T79) → U3(f3_in(times(T77, power(T78, p(0))), T79), div(T77, T78), T79)
U3(f3_out1(T81), div(T77, T78), T79) → f3_out1(T81)
f3_in(power(T94, T95), T96) → U4(f124_in(T95, T94, T96), power(T94, T95), T96)
U4(f124_out1(T98), power(T94, T95), T96) → f3_out1(times(T95, times(T98, power(T94, p(T95)))))
f32_in(0) → f32_out1
f32_in(s(T23)) → U5(f32_in(T23), s(T23))
U5(f32_out1, s(T23)) → f32_out1
f32_in(p(T26)) → U6(f32_in(T26), p(T26))
U6(f32_out1, p(T26)) → f32_out1
f96_in(T47, T49, T48) → U7(f3_in(T47, T49), T47, T49, T48)
U7(f3_out1(T52), T47, T49, T48) → U8(f3_in(T48, T49), T47, T49, T48, T52)
U8(f3_out1(T56), T47, T49, T48, T52) → f96_out1(T52, T56)
f124_in(T95, T94, T96) → U9(f32_in(T95), T95, T94, T96)
U9(f32_out1, T95, T94, T96) → U10(f3_in(T94, T96), T95, T94, T96)
U10(f3_out1(T98), T95, T94, T96) → f124_out1(T98)

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

(8) UsableRulesProof (EQUIVALENT transformation)

We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.

(9) Obligation:

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

F32_IN(p(T26)) → F32_IN(T26)
F32_IN(s(T23)) → F32_IN(T23)

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

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

• F32_IN(p(T26)) → F32_IN(T26)
  The graph contains the following edges 1 > 1

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

(11) YES

(12) Obligation:

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

F3_IN(times(T47, T48), T49) → F96_IN(T47, T49, T48)
F96_IN(T47, T49, T48) → U7¹(f3_in(T47, T49), T47, T49, T48)
U7¹(f3_out1(T52), T47, T49, T48) → F3_IN(T48, T49)
F3_IN(div(T77, T78), T79) → F3_IN(times(T77, power(T78, p(0))), T79)
F3_IN(power(T94, T95), T96) → F124_IN(T95, T94, T96)
F124_IN(T95, T94, T96) → U9¹(f32_in(T95), T95, T94, T96)
U9¹(f32_out1, T95, T94, T96) → F3_IN(T94, T96)
F96_IN(T47, T49, T48) → F3_IN(T47, T49)

The TRS R consists of the following rules:

f3_in(T8, T8) → f3_out1(1)
f3_in(T17, T18) → U1(f32_in(T17), T17, T18)
U1(f32_out1, T17, T18) → f3_out1(0)
f3_in(times(T47, T48), T49) → U2(f96_in(T47, T49, T48), times(T47, T48), T49)
U2(f96_out1(T52, T53), times(T47, T48), T49) → f3_out1(+(times(T53, T47), times(T52, T48)))
f3_in(div(T77, T78), T79) → U3(f3_in(times(T77, power(T78, p(0))), T79), div(T77, T78), T79)
U3(f3_out1(T81), div(T77, T78), T79) → f3_out1(T81)
f3_in(power(T94, T95), T96) → U4(f124_in(T95, T94, T96), power(T94, T95), T96)
U4(f124_out1(T98), power(T94, T95), T96) → f3_out1(times(T95, times(T98, power(T94, p(T95)))))
f32_in(0) → f32_out1
f32_in(s(T23)) → U5(f32_in(T23), s(T23))
U5(f32_out1, s(T23)) → f32_out1
f32_in(p(T26)) → U6(f32_in(T26), p(T26))
U6(f32_out1, p(T26)) → f32_out1
f96_in(T47, T49, T48) → U7(f3_in(T47, T49), T47, T49, T48)
U7(f3_out1(T52), T47, T49, T48) → U8(f3_in(T48, T49), T47, T49, T48, T52)
U8(f3_out1(T56), T47, T49, T48, T52) → f96_out1(T52, T56)
f124_in(T95, T94, T96) → U9(f32_in(T95), T95, T94, T96)
U9(f32_out1, T95, T94, T96) → U10(f3_in(T94, T96), T95, T94, T96)
U10(f3_out1(T98), T95, T94, T96) → f124_out1(T98)

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

(13) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

F124_IN(T95, T94, T96) → U9¹(f32_in(T95), T95, T94, T96)

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

POL(+(x₁, x₂)) = 0   
POL(0) = 0   
POL(1) = 0   
POL(F124_IN(x₁, x₂, x₃)) = 1 + x₂   
POL(F3_IN(x₁, x₂)) = x₁   
POL(F96_IN(x₁, x₂, x₃)) = x₁ + x₃   
POL(U1(x₁, x₂, x₃)) = 0   
POL(U10(x₁, x₂, x₃, x₄)) = 0   
POL(U2(x₁, x₂, x₃)) = 0   
POL(U3(x₁, x₂, x₃)) = 0   
POL(U4(x₁, x₂, x₃)) = 0   
POL(U5(x₁, x₂)) = 0   
POL(U6(x₁, x₂)) = 0   
POL(U7(x₁, x₂, x₃, x₄)) = 0   
POL(U7¹(x₁, x₂, x₃, x₄)) = x₄   
POL(U8(x₁, x₂, x₃, x₄, x₅)) = 0   
POL(U9(x₁, x₂, x₃, x₄)) = 0   
POL(U9¹(x₁, x₂, x₃, x₄)) = x₃   
POL(div(x₁, x₂)) = 1 + x₁ + x₂   
POL(f124_in(x₁, x₂, x₃)) = 0   
POL(f124_out1(x₁)) = 0   
POL(f32_in(x₁)) = 0   
POL(f32_out1) = 0   
POL(f3_in(x₁, x₂)) = 0   
POL(f3_out1(x₁)) = 0   
POL(f96_in(x₁, x₂, x₃)) = 0   
POL(f96_out1(x₁, x₂)) = 0   
POL(p(x₁)) = 0   
POL(power(x₁, x₂)) = 1 + x₁   
POL(s(x₁)) = 0   
POL(times(x₁, x₂)) = x₁ + x₂   

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

(14) Obligation:

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

F3_IN(times(T47, T48), T49) → F96_IN(T47, T49, T48)
F96_IN(T47, T49, T48) → U7¹(f3_in(T47, T49), T47, T49, T48)
U7¹(f3_out1(T52), T47, T49, T48) → F3_IN(T48, T49)
F3_IN(div(T77, T78), T79) → F3_IN(times(T77, power(T78, p(0))), T79)
F3_IN(power(T94, T95), T96) → F124_IN(T95, T94, T96)
U9¹(f32_out1, T95, T94, T96) → F3_IN(T94, T96)
F96_IN(T47, T49, T48) → F3_IN(T47, T49)

The TRS R consists of the following rules:

f3_in(T8, T8) → f3_out1(1)
f3_in(T17, T18) → U1(f32_in(T17), T17, T18)
U1(f32_out1, T17, T18) → f3_out1(0)
f3_in(times(T47, T48), T49) → U2(f96_in(T47, T49, T48), times(T47, T48), T49)
U2(f96_out1(T52, T53), times(T47, T48), T49) → f3_out1(+(times(T53, T47), times(T52, T48)))
f3_in(div(T77, T78), T79) → U3(f3_in(times(T77, power(T78, p(0))), T79), div(T77, T78), T79)
U3(f3_out1(T81), div(T77, T78), T79) → f3_out1(T81)
f3_in(power(T94, T95), T96) → U4(f124_in(T95, T94, T96), power(T94, T95), T96)
U4(f124_out1(T98), power(T94, T95), T96) → f3_out1(times(T95, times(T98, power(T94, p(T95)))))
f32_in(0) → f32_out1
f32_in(s(T23)) → U5(f32_in(T23), s(T23))
U5(f32_out1, s(T23)) → f32_out1
f32_in(p(T26)) → U6(f32_in(T26), p(T26))
U6(f32_out1, p(T26)) → f32_out1
f96_in(T47, T49, T48) → U7(f3_in(T47, T49), T47, T49, T48)
U7(f3_out1(T52), T47, T49, T48) → U8(f3_in(T48, T49), T47, T49, T48, T52)
U8(f3_out1(T56), T47, T49, T48, T52) → f96_out1(T52, T56)
f124_in(T95, T94, T96) → U9(f32_in(T95), T95, T94, T96)
U9(f32_out1, T95, T94, T96) → U10(f3_in(T94, T96), T95, T94, T96)
U10(f3_out1(T98), T95, T94, T96) → f124_out1(T98)

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

(15) DependencyGraphProof (EQUIVALENT transformation)

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

(16) Obligation:

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

F96_IN(T47, T49, T48) → U7¹(f3_in(T47, T49), T47, T49, T48)
U7¹(f3_out1(T52), T47, T49, T48) → F3_IN(T48, T49)
F3_IN(times(T47, T48), T49) → F96_IN(T47, T49, T48)
F96_IN(T47, T49, T48) → F3_IN(T47, T49)
F3_IN(div(T77, T78), T79) → F3_IN(times(T77, power(T78, p(0))), T79)

The TRS R consists of the following rules:

f3_in(T8, T8) → f3_out1(1)
f3_in(T17, T18) → U1(f32_in(T17), T17, T18)
U1(f32_out1, T17, T18) → f3_out1(0)
f3_in(times(T47, T48), T49) → U2(f96_in(T47, T49, T48), times(T47, T48), T49)
U2(f96_out1(T52, T53), times(T47, T48), T49) → f3_out1(+(times(T53, T47), times(T52, T48)))
f3_in(div(T77, T78), T79) → U3(f3_in(times(T77, power(T78, p(0))), T79), div(T77, T78), T79)
U3(f3_out1(T81), div(T77, T78), T79) → f3_out1(T81)
f3_in(power(T94, T95), T96) → U4(f124_in(T95, T94, T96), power(T94, T95), T96)
U4(f124_out1(T98), power(T94, T95), T96) → f3_out1(times(T95, times(T98, power(T94, p(T95)))))
f32_in(0) → f32_out1
f32_in(s(T23)) → U5(f32_in(T23), s(T23))
U5(f32_out1, s(T23)) → f32_out1
f32_in(p(T26)) → U6(f32_in(T26), p(T26))
U6(f32_out1, p(T26)) → f32_out1
f96_in(T47, T49, T48) → U7(f3_in(T47, T49), T47, T49, T48)
U7(f3_out1(T52), T47, T49, T48) → U8(f3_in(T48, T49), T47, T49, T48, T52)
U8(f3_out1(T56), T47, T49, T48, T52) → f96_out1(T52, T56)
f124_in(T95, T94, T96) → U9(f32_in(T95), T95, T94, T96)
U9(f32_out1, T95, T94, T96) → U10(f3_in(T94, T96), T95, T94, T96)
U10(f3_out1(T98), T95, T94, T96) → f124_out1(T98)

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

(17) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

F3_IN(times(T47, T48), T49) → F96_IN(T47, T49, T48)

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

POL(+(x₁, x₂)) = 0   
POL(0) = 0   
POL(1) = 0   
POL(F3_IN(x₁, x₂)) = x₁   
POL(F96_IN(x₁, x₂, x₃)) = x₁ + x₃   
POL(U1(x₁, x₂, x₃)) = 0   
POL(U10(x₁, x₂, x₃, x₄)) = 0   
POL(U2(x₁, x₂, x₃)) = 0   
POL(U3(x₁, x₂, x₃)) = 0   
POL(U4(x₁, x₂, x₃)) = 0   
POL(U5(x₁, x₂)) = 0   
POL(U6(x₁, x₂)) = 0   
POL(U7(x₁, x₂, x₃, x₄)) = 0   
POL(U7¹(x₁, x₂, x₃, x₄)) = x₄   
POL(U8(x₁, x₂, x₃, x₄, x₅)) = 0   
POL(U9(x₁, x₂, x₃, x₄)) = 0   
POL(div(x₁, x₂)) = 1 + x₁ + x₂   
POL(f124_in(x₁, x₂, x₃)) = 0   
POL(f124_out1(x₁)) = 0   
POL(f32_in(x₁)) = 0   
POL(f32_out1) = 0   
POL(f3_in(x₁, x₂)) = 0   
POL(f3_out1(x₁)) = 0   
POL(f96_in(x₁, x₂, x₃)) = 0   
POL(f96_out1(x₁, x₂)) = 0   
POL(p(x₁)) = 0   
POL(power(x₁, x₂)) = x₁   
POL(s(x₁)) = 0   
POL(times(x₁, x₂)) = 1 + x₁ + x₂   

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

(18) Obligation:

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

F96_IN(T47, T49, T48) → U7¹(f3_in(T47, T49), T47, T49, T48)
U7¹(f3_out1(T52), T47, T49, T48) → F3_IN(T48, T49)
F96_IN(T47, T49, T48) → F3_IN(T47, T49)
F3_IN(div(T77, T78), T79) → F3_IN(times(T77, power(T78, p(0))), T79)

The TRS R consists of the following rules:

f3_in(T8, T8) → f3_out1(1)
f3_in(T17, T18) → U1(f32_in(T17), T17, T18)
U1(f32_out1, T17, T18) → f3_out1(0)
f3_in(times(T47, T48), T49) → U2(f96_in(T47, T49, T48), times(T47, T48), T49)
U2(f96_out1(T52, T53), times(T47, T48), T49) → f3_out1(+(times(T53, T47), times(T52, T48)))
f3_in(div(T77, T78), T79) → U3(f3_in(times(T77, power(T78, p(0))), T79), div(T77, T78), T79)
U3(f3_out1(T81), div(T77, T78), T79) → f3_out1(T81)
f3_in(power(T94, T95), T96) → U4(f124_in(T95, T94, T96), power(T94, T95), T96)
U4(f124_out1(T98), power(T94, T95), T96) → f3_out1(times(T95, times(T98, power(T94, p(T95)))))
f32_in(0) → f32_out1
f32_in(s(T23)) → U5(f32_in(T23), s(T23))
U5(f32_out1, s(T23)) → f32_out1
f32_in(p(T26)) → U6(f32_in(T26), p(T26))
U6(f32_out1, p(T26)) → f32_out1
f96_in(T47, T49, T48) → U7(f3_in(T47, T49), T47, T49, T48)
U7(f3_out1(T52), T47, T49, T48) → U8(f3_in(T48, T49), T47, T49, T48, T52)
U8(f3_out1(T56), T47, T49, T48, T52) → f96_out1(T52, T56)
f124_in(T95, T94, T96) → U9(f32_in(T95), T95, T94, T96)
U9(f32_out1, T95, T94, T96) → U10(f3_in(T94, T96), T95, T94, T96)
U10(f3_out1(T98), T95, T94, T96) → f124_out1(T98)

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

(19) DependencyGraphProof (EQUIVALENT transformation)

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

(20) TRUE