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

(0) Obligation:

Clauses:

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

Query: p(g)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: p(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: p(T1), SCOPE: 1, CLAUSE: 0 | p(T1), SCOPE: 1, CLAUSE: 1 | p(T1), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: p(T1), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: p(T1), SCOPE: 1, CLAUSE: 1 | p(T1), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: p(T1), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: p(T1), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(p(.(T19, .(T20, T21))), ','(mult(T19, T20, X24), p(.(X24, T21))))\n\nT19 is ground\nT20 is ground\nT21 is ground\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: p(.(T19, .(T20, T21)))\n\nT19 is ground\nT20 is ground\nT21 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ','(mult(T19, T20, X24), p(.(X24, T21)))\n\nT19 is ground\nT20 is ground\nT21 is ground\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: mult(T19, T20, X24)\n\nT19 is ground\nT20 is ground\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: p(.(T28, T21))\n\nT21 is ground\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: mult(T19, T20, X24), SCOPE: 2, CLAUSE: 5 | mult(T19, T20, X24), SCOPE: 2, CLAUSE: 6\n\nT19 is ground\nT20 is ground\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: mult(T19, T20, X24), SCOPE: 2, CLAUSE: 5\n\nT19 is ground\nT20 is ground\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: mult(T19, T20, X24), SCOPE: 2, CLAUSE: 6\n\nT19 is ground\nT20 is ground\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: ','(mult(T40, T41, X50), sum(X50, T40, X51))\n\nT40 is ground\nT41 is ground\nX51 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: mult(T40, T41, X50)\n\nT40 is ground\nT41 is ground\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: sum(T44, T40, X51)\n\nT40 is ground\nT44 is ground\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: sum(T44, T40, X51), SCOPE: 3, CLAUSE: 3 | sum(T44, T40, X51), SCOPE: 3, CLAUSE: 4\n\nT40 is ground\nT44 is ground\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: sum(T44, T40, X51), SCOPE: 3, CLAUSE: 3\n\nT40 is ground\nT44 is ground\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: sum(T44, T40, X51), SCOPE: 3, CLAUSE: 4\n\nT40 is ground\nT44 is ground\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: sum(T58, T59, X74)\n\nT58 is ground\nT59 is ground\nX74 is free", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: p(T66)\n\nT66 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 120 [arrowhead = none ];
120 -> 4;

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

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

123 [label="EVAL with clause\np(.(X6, [])).\nand substitutionX6 -> T6,\nT1 -> .(T6, [])", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 123 [arrowhead = none ];
123 -> 11;

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

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

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

127 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
11 -> 127 [arrowhead = none ];
127 -> 13;

128 [label="EVAL with clause\np(.(s(s(X21)), .(X22, X23))) :- ','(p(.(X21, .(X22, X23))), ','(mult(X21, X22, X24), p(.(X24, X23)))).\nand substitutionX21 -> T19,\nX22 -> T20,\nX23 -> T21,\nT1 -> .(s(s(T19)), .(T20, T21))", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 128 [arrowhead = none ];
128 -> 46;

129 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
20 -> 129 [arrowhead = none ];
129 -> 47;

130 [label="EVAL with clause\np(.(0, X81)) :- p(X81).\nand substitutionX81 -> T66,\nT1 -> .(0, T66)", fontsize=14, style = filled, fillcolor = lightblue];
21 -> 130 [arrowhead = none ];
130 -> 118;

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

132 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
46 -> 132 [arrowhead = none ];
132 -> 52;

133 [label="SPLIT 2\nnew knowledge:\nT19 is ground\nT20 is ground\nT21 is ground", fontsize=14, style = filled, fillcolor = violet];
46 -> 133 [arrowhead = none ];
133 -> 53;

134 [label="INSTANCE with matching:\nT1 -> .(T19, .(T20, T21))", fontsize=14, style = filled, fillcolor = lightgrey];
52 -> 134 [arrowhead = none , style=dashed];
134 -> 1[style=dashed];

135 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
53 -> 135 [arrowhead = none ];
135 -> 58;

136 [label="SPLIT 2\nnew knowledge:\nT19 is ground\nT20 is ground\nT28 is ground\nreplacements:X24 -> T28", fontsize=14, style = filled, fillcolor = violet];
53 -> 136 [arrowhead = none ];
136 -> 60;

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

138 [label="INSTANCE with matching:\nT1 -> .(T28, T21)", fontsize=14, style = filled, fillcolor = lightgrey];
60 -> 138 [arrowhead = none , style=dashed];
138 -> 1[style=dashed];

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

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

141 [label="EVAL with clause\nmult(X37, 0, 0).\nand substitutionT19 -> T35,\nX37 -> T35,\nT20 -> 0,\nX24 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 141 [arrowhead = none ];
141 -> 73;

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

143 [label="EVAL with clause\nmult(X47, s(X48), X49) :- ','(mult(X47, X48, X50), sum(X50, X47, X49)).\nand substitutionT19 -> T40,\nX47 -> T40,\nX48 -> T41,\nT20 -> s(T41),\nX24 -> X51,\nX49 -> X51", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 143 [arrowhead = none ];
143 -> 82;

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

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

146 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
82 -> 146 [arrowhead = none ];
146 -> 88;

147 [label="SPLIT 2\nnew knowledge:\nT40 is ground\nT41 is ground\nT44 is ground\nreplacements:X50 -> T44", fontsize=14, style = filled, fillcolor = violet];
82 -> 147 [arrowhead = none ];
147 -> 89;

148 [label="INSTANCE with matching:\nT19 -> T40\nT20 -> T41\nX24 -> X50", fontsize=14, style = filled, fillcolor = lightgrey];
88 -> 148 [arrowhead = none , style=dashed];
148 -> 58[style=dashed];

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

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

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

152 [label="EVAL with clause\nsum(X62, 0, X62).\nand substitutionT44 -> T53,\nX62 -> T53,\nT40 -> 0,\nX51 -> T53", fontsize=14, style = filled, fillcolor = lightblue];
95 -> 152 [arrowhead = none ];
152 -> 101;

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

154 [label="EVAL with clause\nsum(X71, s(X72), s(X73)) :- sum(X71, X72, X73).\nand substitutionT44 -> T58,\nX71 -> T58,\nX72 -> T59,\nT40 -> s(T59),\nX73 -> X74,\nX51 -> s(X74)", fontsize=14, style = filled, fillcolor = lightblue];
96 -> 154 [arrowhead = none ];
154 -> 112;

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

156 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
101 -> 156 [arrowhead = none ];
156 -> 103;

157 [label="INSTANCE with matching:\nT44 -> T58\nT40 -> T59\nX51 -> X74", fontsize=14, style = filled, fillcolor = lightgrey];
112 -> 157 [arrowhead = none , style=dashed];
157 -> 89[style=dashed];

158 [label="INSTANCE with matching:\nT1 -> T66", fontsize=14, style = filled, fillcolor = lightgrey];
118 -> 158 [arrowhead = none , style=dashed];
158 -> 1[style=dashed];

}

(2) Obligation:

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

f1_in(.(T6, [])) → f1_out1
f1_in(.(s(s(T19)), .(T20, T21))) → U1(f46_in(T19, T20, T21), .(s(s(T19)), .(T20, T21)))
U1(f46_out1(X24), .(s(s(T19)), .(T20, T21))) → f1_out1
f1_in(.(0, T66)) → U2(f1_in(T66), .(0, T66))
U2(f1_out1, .(0, T66)) → f1_out1
f58_in(T35, 0) → f58_out1(0)
f58_in(T40, s(T41)) → U3(f82_in(T40, T41), T40, s(T41))
U3(f82_out1(X50, X51), T40, s(T41)) → f58_out1(X51)
f89_in(T53, 0) → f89_out1(T53)
f89_in(T58, s(T59)) → U4(f89_in(T58, T59), T58, s(T59))
U4(f89_out1(X74), T58, s(T59)) → f89_out1(s(X74))
f46_in(T19, T20, T21) → U5(f1_in(.(T19, .(T20, T21))), T19, T20, T21)
U5(f1_out1, T19, T20, T21) → U6(f53_in(T19, T20, T21), T19, T20, T21)
U6(f53_out1(X24), T19, T20, T21) → f46_out1(X24)
f53_in(T19, T20, T21) → U7(f58_in(T19, T20), T19, T20, T21)
U7(f58_out1(T28), T19, T20, T21) → U8(f1_in(.(T28, T21)), T19, T20, T21, T28)
U8(f1_out1, T19, T20, T21, T28) → f53_out1(T28)
f82_in(T40, T41) → U9(f58_in(T40, T41), T40, T41)
U9(f58_out1(T44), T40, T41) → U10(f89_in(T44, T40), T40, T41, T44)
U10(f89_out1(X51), T40, T41, T44) → f82_out1(T44, X51)

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:

F1_IN(.(s(s(T19)), .(T20, T21))) → U1¹(f46_in(T19, T20, T21), .(s(s(T19)), .(T20, T21)))
F1_IN(.(s(s(T19)), .(T20, T21))) → F46_IN(T19, T20, T21)
F1_IN(.(0, T66)) → U2¹(f1_in(T66), .(0, T66))
F1_IN(.(0, T66)) → F1_IN(T66)
F58_IN(T40, s(T41)) → U3¹(f82_in(T40, T41), T40, s(T41))
F58_IN(T40, s(T41)) → F82_IN(T40, T41)
F89_IN(T58, s(T59)) → U4¹(f89_in(T58, T59), T58, s(T59))
F89_IN(T58, s(T59)) → F89_IN(T58, T59)
F46_IN(T19, T20, T21) → U5¹(f1_in(.(T19, .(T20, T21))), T19, T20, T21)
F46_IN(T19, T20, T21) → F1_IN(.(T19, .(T20, T21)))
U5¹(f1_out1, T19, T20, T21) → U6¹(f53_in(T19, T20, T21), T19, T20, T21)
U5¹(f1_out1, T19, T20, T21) → F53_IN(T19, T20, T21)
F53_IN(T19, T20, T21) → U7¹(f58_in(T19, T20), T19, T20, T21)
F53_IN(T19, T20, T21) → F58_IN(T19, T20)
U7¹(f58_out1(T28), T19, T20, T21) → U8¹(f1_in(.(T28, T21)), T19, T20, T21, T28)
U7¹(f58_out1(T28), T19, T20, T21) → F1_IN(.(T28, T21))
F82_IN(T40, T41) → U9¹(f58_in(T40, T41), T40, T41)
F82_IN(T40, T41) → F58_IN(T40, T41)
U9¹(f58_out1(T44), T40, T41) → U10¹(f89_in(T44, T40), T40, T41, T44)
U9¹(f58_out1(T44), T40, T41) → F89_IN(T44, T40)

The TRS R consists of the following rules:

f1_in(.(T6, [])) → f1_out1
f1_in(.(s(s(T19)), .(T20, T21))) → U1(f46_in(T19, T20, T21), .(s(s(T19)), .(T20, T21)))
U1(f46_out1(X24), .(s(s(T19)), .(T20, T21))) → f1_out1
f1_in(.(0, T66)) → U2(f1_in(T66), .(0, T66))
U2(f1_out1, .(0, T66)) → f1_out1
f58_in(T35, 0) → f58_out1(0)
f58_in(T40, s(T41)) → U3(f82_in(T40, T41), T40, s(T41))
U3(f82_out1(X50, X51), T40, s(T41)) → f58_out1(X51)
f89_in(T53, 0) → f89_out1(T53)
f89_in(T58, s(T59)) → U4(f89_in(T58, T59), T58, s(T59))
U4(f89_out1(X74), T58, s(T59)) → f89_out1(s(X74))
f46_in(T19, T20, T21) → U5(f1_in(.(T19, .(T20, T21))), T19, T20, T21)
U5(f1_out1, T19, T20, T21) → U6(f53_in(T19, T20, T21), T19, T20, T21)
U6(f53_out1(X24), T19, T20, T21) → f46_out1(X24)
f53_in(T19, T20, T21) → U7(f58_in(T19, T20), T19, T20, T21)
U7(f58_out1(T28), T19, T20, T21) → U8(f1_in(.(T28, T21)), T19, T20, T21, T28)
U8(f1_out1, T19, T20, T21, T28) → f53_out1(T28)
f82_in(T40, T41) → U9(f58_in(T40, T41), T40, T41)
U9(f58_out1(T44), T40, T41) → U10(f89_in(T44, T40), T40, T41, T44)
U10(f89_out1(X51), T40, T41, T44) → f82_out1(T44, X51)

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 3 SCCs with 10 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

F89_IN(T58, s(T59)) → F89_IN(T58, T59)

The TRS R consists of the following rules:

f1_in(.(T6, [])) → f1_out1
f1_in(.(s(s(T19)), .(T20, T21))) → U1(f46_in(T19, T20, T21), .(s(s(T19)), .(T20, T21)))
U1(f46_out1(X24), .(s(s(T19)), .(T20, T21))) → f1_out1
f1_in(.(0, T66)) → U2(f1_in(T66), .(0, T66))
U2(f1_out1, .(0, T66)) → f1_out1
f58_in(T35, 0) → f58_out1(0)
f58_in(T40, s(T41)) → U3(f82_in(T40, T41), T40, s(T41))
U3(f82_out1(X50, X51), T40, s(T41)) → f58_out1(X51)
f89_in(T53, 0) → f89_out1(T53)
f89_in(T58, s(T59)) → U4(f89_in(T58, T59), T58, s(T59))
U4(f89_out1(X74), T58, s(T59)) → f89_out1(s(X74))
f46_in(T19, T20, T21) → U5(f1_in(.(T19, .(T20, T21))), T19, T20, T21)
U5(f1_out1, T19, T20, T21) → U6(f53_in(T19, T20, T21), T19, T20, T21)
U6(f53_out1(X24), T19, T20, T21) → f46_out1(X24)
f53_in(T19, T20, T21) → U7(f58_in(T19, T20), T19, T20, T21)
U7(f58_out1(T28), T19, T20, T21) → U8(f1_in(.(T28, T21)), T19, T20, T21, T28)
U8(f1_out1, T19, T20, T21, T28) → f53_out1(T28)
f82_in(T40, T41) → U9(f58_in(T40, T41), T40, T41)
U9(f58_out1(T44), T40, T41) → U10(f89_in(T44, T40), T40, T41, T44)
U10(f89_out1(X51), T40, T41, T44) → f82_out1(T44, X51)

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:

F89_IN(T58, s(T59)) → F89_IN(T58, T59)

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:

• F89_IN(T58, s(T59)) → F89_IN(T58, T59)
  The graph contains the following edges 1 >= 1, 2 > 2

(11) YES

(12) Obligation:

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

F58_IN(T40, s(T41)) → F82_IN(T40, T41)
F82_IN(T40, T41) → F58_IN(T40, T41)

The TRS R consists of the following rules:

f1_in(.(T6, [])) → f1_out1
f1_in(.(s(s(T19)), .(T20, T21))) → U1(f46_in(T19, T20, T21), .(s(s(T19)), .(T20, T21)))
U1(f46_out1(X24), .(s(s(T19)), .(T20, T21))) → f1_out1
f1_in(.(0, T66)) → U2(f1_in(T66), .(0, T66))
U2(f1_out1, .(0, T66)) → f1_out1
f58_in(T35, 0) → f58_out1(0)
f58_in(T40, s(T41)) → U3(f82_in(T40, T41), T40, s(T41))
U3(f82_out1(X50, X51), T40, s(T41)) → f58_out1(X51)
f89_in(T53, 0) → f89_out1(T53)
f89_in(T58, s(T59)) → U4(f89_in(T58, T59), T58, s(T59))
U4(f89_out1(X74), T58, s(T59)) → f89_out1(s(X74))
f46_in(T19, T20, T21) → U5(f1_in(.(T19, .(T20, T21))), T19, T20, T21)
U5(f1_out1, T19, T20, T21) → U6(f53_in(T19, T20, T21), T19, T20, T21)
U6(f53_out1(X24), T19, T20, T21) → f46_out1(X24)
f53_in(T19, T20, T21) → U7(f58_in(T19, T20), T19, T20, T21)
U7(f58_out1(T28), T19, T20, T21) → U8(f1_in(.(T28, T21)), T19, T20, T21, T28)
U8(f1_out1, T19, T20, T21, T28) → f53_out1(T28)
f82_in(T40, T41) → U9(f58_in(T40, T41), T40, T41)
U9(f58_out1(T44), T40, T41) → U10(f89_in(T44, T40), T40, T41, T44)
U10(f89_out1(X51), T40, T41, T44) → f82_out1(T44, X51)

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

(13) 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.

(14) Obligation:

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

F58_IN(T40, s(T41)) → F82_IN(T40, T41)
F82_IN(T40, T41) → F58_IN(T40, T41)

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

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

• F82_IN(T40, T41) → F58_IN(T40, T41)
  The graph contains the following edges 1 >= 1, 2 >= 2

• F58_IN(T40, s(T41)) → F82_IN(T40, T41)
  The graph contains the following edges 1 >= 1, 2 > 2

(16) YES

(17) Obligation:

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

F1_IN(.(s(s(T19)), .(T20, T21))) → F46_IN(T19, T20, T21)
F46_IN(T19, T20, T21) → U5¹(f1_in(.(T19, .(T20, T21))), T19, T20, T21)
U5¹(f1_out1, T19, T20, T21) → F53_IN(T19, T20, T21)
F53_IN(T19, T20, T21) → U7¹(f58_in(T19, T20), T19, T20, T21)
U7¹(f58_out1(T28), T19, T20, T21) → F1_IN(.(T28, T21))
F1_IN(.(0, T66)) → F1_IN(T66)
F46_IN(T19, T20, T21) → F1_IN(.(T19, .(T20, T21)))

The TRS R consists of the following rules:

f1_in(.(T6, [])) → f1_out1
f1_in(.(s(s(T19)), .(T20, T21))) → U1(f46_in(T19, T20, T21), .(s(s(T19)), .(T20, T21)))
U1(f46_out1(X24), .(s(s(T19)), .(T20, T21))) → f1_out1
f1_in(.(0, T66)) → U2(f1_in(T66), .(0, T66))
U2(f1_out1, .(0, T66)) → f1_out1
f58_in(T35, 0) → f58_out1(0)
f58_in(T40, s(T41)) → U3(f82_in(T40, T41), T40, s(T41))
U3(f82_out1(X50, X51), T40, s(T41)) → f58_out1(X51)
f89_in(T53, 0) → f89_out1(T53)
f89_in(T58, s(T59)) → U4(f89_in(T58, T59), T58, s(T59))
U4(f89_out1(X74), T58, s(T59)) → f89_out1(s(X74))
f46_in(T19, T20, T21) → U5(f1_in(.(T19, .(T20, T21))), T19, T20, T21)
U5(f1_out1, T19, T20, T21) → U6(f53_in(T19, T20, T21), T19, T20, T21)
U6(f53_out1(X24), T19, T20, T21) → f46_out1(X24)
f53_in(T19, T20, T21) → U7(f58_in(T19, T20), T19, T20, T21)
U7(f58_out1(T28), T19, T20, T21) → U8(f1_in(.(T28, T21)), T19, T20, T21, T28)
U8(f1_out1, T19, T20, T21, T28) → f53_out1(T28)
f82_in(T40, T41) → U9(f58_in(T40, T41), T40, T41)
U9(f58_out1(T44), T40, T41) → U10(f89_in(T44, T40), T40, T41, T44)
U10(f89_out1(X51), T40, T41, T44) → f82_out1(T44, X51)

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

(18) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

F1_IN(.(0, T66)) → F1_IN(T66)

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

POL(.(x₁, x₂)) = x₁ + x₂   
POL(0) = 1   
POL(F1_IN(x₁)) = x₁   
POL(F46_IN(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(F53_IN(x₁, x₂, x₃)) = x₂ + x₃   
POL(U1(x₁, x₂)) = 0   
POL(U10(x₁, x₂, x₃, x₄)) = x₁   
POL(U2(x₁, x₂)) = 0   
POL(U3(x₁, x₂, x₃)) = x₁   
POL(U4(x₁, x₂, x₃)) = x₁   
POL(U5(x₁, x₂, x₃, x₄)) = 1   
POL(U5¹(x₁, x₂, x₃, x₄)) = x₃ + x₄   
POL(U6(x₁, x₂, x₃, x₄)) = 1   
POL(U7(x₁, x₂, x₃, x₄)) = 0   
POL(U7¹(x₁, x₂, x₃, x₄)) = x₁ + x₄   
POL(U8(x₁, x₂, x₃, x₄, x₅)) = 0   
POL(U9(x₁, x₂, x₃)) = x₁   
POL([]) = 0   
POL(f1_in(x₁)) = 0   
POL(f1_out1) = 0   
POL(f46_in(x₁, x₂, x₃)) = 1 + x₃   
POL(f46_out1(x₁)) = 0   
POL(f53_in(x₁, x₂, x₃)) = 1   
POL(f53_out1(x₁)) = 0   
POL(f58_in(x₁, x₂)) = x₂   
POL(f58_out1(x₁)) = x₁   
POL(f82_in(x₁, x₂)) = x₂   
POL(f82_out1(x₁, x₂)) = x₂   
POL(f89_in(x₁, x₂)) = x₁   
POL(f89_out1(x₁)) = x₁   
POL(s(x₁)) = x₁   

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

f58_in(T35, 0) → f58_out1(0)
f58_in(T40, s(T41)) → U3(f82_in(T40, T41), T40, s(T41))
U3(f82_out1(X50, X51), T40, s(T41)) → f58_out1(X51)
f82_in(T40, T41) → U9(f58_in(T40, T41), T40, T41)
U9(f58_out1(T44), T40, T41) → U10(f89_in(T44, T40), T40, T41, T44)
f89_in(T53, 0) → f89_out1(T53)
f89_in(T58, s(T59)) → U4(f89_in(T58, T59), T58, s(T59))
U10(f89_out1(X51), T40, T41, T44) → f82_out1(T44, X51)
U4(f89_out1(X74), T58, s(T59)) → f89_out1(s(X74))

(19) Obligation:

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

F1_IN(.(s(s(T19)), .(T20, T21))) → F46_IN(T19, T20, T21)
F46_IN(T19, T20, T21) → U5¹(f1_in(.(T19, .(T20, T21))), T19, T20, T21)
U5¹(f1_out1, T19, T20, T21) → F53_IN(T19, T20, T21)
F53_IN(T19, T20, T21) → U7¹(f58_in(T19, T20), T19, T20, T21)
U7¹(f58_out1(T28), T19, T20, T21) → F1_IN(.(T28, T21))
F46_IN(T19, T20, T21) → F1_IN(.(T19, .(T20, T21)))

The TRS R consists of the following rules:

f1_in(.(T6, [])) → f1_out1
f1_in(.(s(s(T19)), .(T20, T21))) → U1(f46_in(T19, T20, T21), .(s(s(T19)), .(T20, T21)))
U1(f46_out1(X24), .(s(s(T19)), .(T20, T21))) → f1_out1
f1_in(.(0, T66)) → U2(f1_in(T66), .(0, T66))
U2(f1_out1, .(0, T66)) → f1_out1
f58_in(T35, 0) → f58_out1(0)
f58_in(T40, s(T41)) → U3(f82_in(T40, T41), T40, s(T41))
U3(f82_out1(X50, X51), T40, s(T41)) → f58_out1(X51)
f89_in(T53, 0) → f89_out1(T53)
f89_in(T58, s(T59)) → U4(f89_in(T58, T59), T58, s(T59))
U4(f89_out1(X74), T58, s(T59)) → f89_out1(s(X74))
f46_in(T19, T20, T21) → U5(f1_in(.(T19, .(T20, T21))), T19, T20, T21)
U5(f1_out1, T19, T20, T21) → U6(f53_in(T19, T20, T21), T19, T20, T21)
U6(f53_out1(X24), T19, T20, T21) → f46_out1(X24)
f53_in(T19, T20, T21) → U7(f58_in(T19, T20), T19, T20, T21)
U7(f58_out1(T28), T19, T20, T21) → U8(f1_in(.(T28, T21)), T19, T20, T21, T28)
U8(f1_out1, T19, T20, T21, T28) → f53_out1(T28)
f82_in(T40, T41) → U9(f58_in(T40, T41), T40, T41)
U9(f58_out1(T44), T40, T41) → U10(f89_in(T44, T40), T40, T41, T44)
U10(f89_out1(X51), T40, T41, T44) → f82_out1(T44, X51)

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

(20) QDPOrderProof (EQUIVALENT transformation)

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

The following pairs can be oriented strictly and are deleted.

U7¹(f58_out1(T28), T19, T20, T21) → F1_IN(.(T28, T21))

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( U5¹(x₁, ..., x₄) ) = 2x₄ + 2

POL( f1_in(x₁) ) = max{0, -2}

POL( .(x₁, x₂) ) = x₂ + 1

POL( s(x₁) ) = 0

POL( U1(x₁, x₂) ) = max{0, 2x₁ - 1}

POL( f46_in(x₁, ..., x₃) ) = x₂ + x₃

POL( 0 ) = 2

POL( U2(x₁, x₂) ) = max{0, -1}

POL( U7¹(x₁, ..., x₄) ) = 2x₄ + 2

POL( U7(x₁, ..., x₄) ) = 2x₂ + x₃ + x₄ + 2

POL( f58_in(x₁, x₂) ) = 2x₁

POL( f58_out1(x₁) ) = max{0, 2x₁ - 2}

POL( U3(x₁, ..., x₃) ) = max{0, x₁ - 2}

POL( f82_in(x₁, x₂) ) = x₁ + x₂ + 1

POL( f46_out1(x₁) ) = 2x₁

POL( f1_out1 ) = 0

POL( U5(x₁, ..., x₄) ) = max{0, x₁ + 2x₃ + 2x₄ - 2}

POL( U8(x₁, ..., x₅) ) = max{0, 2x₁ - 2}

POL( [] ) = 2

POL( U6(x₁, ..., x₄) ) = 2x₁ + x₂ + 2x₃ + x₄

POL( f53_in(x₁, ..., x₃) ) = 2x₁ + x₂ + 2x₃

POL( f53_out1(x₁) ) = 2

POL( f82_out1(x₁, x₂) ) = 2x₁ + x₂ + 2

POL( U9(x₁, ..., x₃) ) = max{0, 2x₁ + 2x₂ + 2x₃ - 1}

POL( U10(x₁, ..., x₄) ) = max{0, -2}

POL( f89_in(x₁, x₂) ) = 2x₁ + x₂

POL( f89_out1(x₁) ) = max{0, 2x₁ - 2}

POL( U4(x₁, ..., x₃) ) = max{0, 2x₁ + x₂ - 2}

POL( F1_IN(x₁) ) = max{0, 2x₁ - 2}

POL( F46_IN(x₁, ..., x₃) ) = 2x₃ + 2

POL( F53_IN(x₁, ..., x₃) ) = 2x₃ + 2

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

(21) Obligation:

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

F1_IN(.(s(s(T19)), .(T20, T21))) → F46_IN(T19, T20, T21)
F46_IN(T19, T20, T21) → U5¹(f1_in(.(T19, .(T20, T21))), T19, T20, T21)
U5¹(f1_out1, T19, T20, T21) → F53_IN(T19, T20, T21)
F53_IN(T19, T20, T21) → U7¹(f58_in(T19, T20), T19, T20, T21)
F46_IN(T19, T20, T21) → F1_IN(.(T19, .(T20, T21)))

The TRS R consists of the following rules:

f1_in(.(T6, [])) → f1_out1
f1_in(.(s(s(T19)), .(T20, T21))) → U1(f46_in(T19, T20, T21), .(s(s(T19)), .(T20, T21)))
U1(f46_out1(X24), .(s(s(T19)), .(T20, T21))) → f1_out1
f1_in(.(0, T66)) → U2(f1_in(T66), .(0, T66))
U2(f1_out1, .(0, T66)) → f1_out1
f58_in(T35, 0) → f58_out1(0)
f58_in(T40, s(T41)) → U3(f82_in(T40, T41), T40, s(T41))
U3(f82_out1(X50, X51), T40, s(T41)) → f58_out1(X51)
f89_in(T53, 0) → f89_out1(T53)
f89_in(T58, s(T59)) → U4(f89_in(T58, T59), T58, s(T59))
U4(f89_out1(X74), T58, s(T59)) → f89_out1(s(X74))
f46_in(T19, T20, T21) → U5(f1_in(.(T19, .(T20, T21))), T19, T20, T21)
U5(f1_out1, T19, T20, T21) → U6(f53_in(T19, T20, T21), T19, T20, T21)
U6(f53_out1(X24), T19, T20, T21) → f46_out1(X24)
f53_in(T19, T20, T21) → U7(f58_in(T19, T20), T19, T20, T21)
U7(f58_out1(T28), T19, T20, T21) → U8(f1_in(.(T28, T21)), T19, T20, T21, T28)
U8(f1_out1, T19, T20, T21, T28) → f53_out1(T28)
f82_in(T40, T41) → U9(f58_in(T40, T41), T40, T41)
U9(f58_out1(T44), T40, T41) → U10(f89_in(T44, T40), T40, T41, T44)
U10(f89_out1(X51), T40, T41, T44) → f82_out1(T44, X51)

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

(22) DependencyGraphProof (EQUIVALENT transformation)

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

(23) Obligation:

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

F46_IN(T19, T20, T21) → F1_IN(.(T19, .(T20, T21)))
F1_IN(.(s(s(T19)), .(T20, T21))) → F46_IN(T19, T20, T21)

The TRS R consists of the following rules:

f1_in(.(T6, [])) → f1_out1
f1_in(.(s(s(T19)), .(T20, T21))) → U1(f46_in(T19, T20, T21), .(s(s(T19)), .(T20, T21)))
U1(f46_out1(X24), .(s(s(T19)), .(T20, T21))) → f1_out1
f1_in(.(0, T66)) → U2(f1_in(T66), .(0, T66))
U2(f1_out1, .(0, T66)) → f1_out1
f58_in(T35, 0) → f58_out1(0)
f58_in(T40, s(T41)) → U3(f82_in(T40, T41), T40, s(T41))
U3(f82_out1(X50, X51), T40, s(T41)) → f58_out1(X51)
f89_in(T53, 0) → f89_out1(T53)
f89_in(T58, s(T59)) → U4(f89_in(T58, T59), T58, s(T59))
U4(f89_out1(X74), T58, s(T59)) → f89_out1(s(X74))
f46_in(T19, T20, T21) → U5(f1_in(.(T19, .(T20, T21))), T19, T20, T21)
U5(f1_out1, T19, T20, T21) → U6(f53_in(T19, T20, T21), T19, T20, T21)
U6(f53_out1(X24), T19, T20, T21) → f46_out1(X24)
f53_in(T19, T20, T21) → U7(f58_in(T19, T20), T19, T20, T21)
U7(f58_out1(T28), T19, T20, T21) → U8(f1_in(.(T28, T21)), T19, T20, T21, T28)
U8(f1_out1, T19, T20, T21, T28) → f53_out1(T28)
f82_in(T40, T41) → U9(f58_in(T40, T41), T40, T41)
U9(f58_out1(T44), T40, T41) → U10(f89_in(T44, T40), T40, T41, T44)
U10(f89_out1(X51), T40, T41, T44) → f82_out1(T44, X51)

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

(24) 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.

(25) Obligation:

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

F46_IN(T19, T20, T21) → F1_IN(.(T19, .(T20, T21)))
F1_IN(.(s(s(T19)), .(T20, T21))) → F46_IN(T19, T20, T21)

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

(26) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

F1_IN(.(s(s(T19)), .(T20, T21))) → F46_IN(T19, T20, T21)

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = x₁ + x₂   
POL(F1_IN(x₁)) = x₁   
POL(F46_IN(x₁, x₂, x₃)) = x₁ + x₂ + x₃   
POL(s(x₁)) = 2·x₁   

(27) Obligation:

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

F46_IN(T19, T20, T21) → F1_IN(.(T19, .(T20, T21)))

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

(28) DependencyGraphProof (EQUIVALENT transformation)

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

(29) TRUE