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

(0) Obligation:

Clauses:

delete(X, tree(X, void, Right), Right).
delete(X, tree(X, Left, void), Left).
delete(X, tree(X, Left, Right), tree(Y, Left, Right1)) :- delmin(Right, Y, Right1).
delete(X, tree(Y, Left, Right), tree(Y, Left1, Right)) :- ','(less(X, Y), delete(X, Left, Left1)).
delete(X, tree(Y, Left, Right), tree(Y, Left, Right1)) :- ','(less(Y, X), delete(X, Right, Right1)).
delmin(tree(Y, void, Right), Y, Right).
delmin(tree(X, Left, X1), Y, tree(X, Left1, X2)) :- delmin(Left, Y, Left1).
less(0, s(X3)).
less(s(X), s(Y)) :- less(X, Y).

Query: delete(g,a,g)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="2: delete(T1, T2, T3)\n\nT1 is ground\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 0\n\nT1 is ground\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3 | delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: delmin(T49, T47, T48)\n\nT47 is ground\nT48 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: delmin(T49, T47, T48), SCOPE: 2, CLAUSE: 5 | delmin(T49, T47, T48), SCOPE: 2, CLAUSE: 6\n\nT47 is ground\nT48 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: delmin(T49, T47, T48), SCOPE: 2, CLAUSE: 5\n\nT47 is ground\nT48 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: delmin(T49, T47, T48), SCOPE: 2, CLAUSE: 6\n\nT47 is ground\nT48 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: delmin(T82, T79, T80)\n\nT79 is ground\nT80 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: delete(T1, T2, T3), SCOPE: 1, CLAUSE: 4\n\nT1 is ground\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: ','(less(T107, T108), delete(T107, T112, T111))\n\nT107 is ground\nT108 is ground\nT111 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: less(T107, T108)\n\nT107 is ground\nT108 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: delete(T107, T112, T111)\n\nT107 is ground\nT111 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: less(T107, T108), SCOPE: 3, CLAUSE: 7 | less(T107, T108), SCOPE: 3, CLAUSE: 8\n\nT107 is ground\nT108 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: less(T107, T108), SCOPE: 3, CLAUSE: 7\n\nT107 is ground\nT108 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: less(T107, T108), SCOPE: 3, CLAUSE: 8\n\nT107 is ground\nT108 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: less(T126, T127)\n\nT126 is ground\nT127 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: ','(less(T145, T144), delete(T144, T149, T148))\n\nT144 is ground\nT145 is ground\nT148 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: less(T145, T144)\n\nT144 is ground\nT145 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: delete(T144, T149, T148)\n\nT144 is ground\nT148 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 116 [arrowhead = none ];
116 -> 5;

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

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

119 [label="EVAL with clause\ndelete(X12, tree(X12, void, X13), X13).\nand substitutionT1 -> T12,\nX12 -> T12,\nX13 -> T13,\nT2 -> tree(T12, void, T13),\nT3 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 119 [arrowhead = none ];
119 -> 11;

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

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

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

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

124 [label="EVAL with clause\ndelete(X22, tree(X22, X23, void), X23).\nand substitutionT1 -> T22,\nX22 -> T22,\nX23 -> T23,\nT2 -> tree(T22, T23, void),\nT3 -> T23", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 124 [arrowhead = none ];
124 -> 26;

125 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 125 [arrowhead = none ];
125 -> 27;

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

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

128 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
26 -> 128 [arrowhead = none ];
128 -> 28;

129 [label="EVAL with clause\ndelete(X44, tree(X44, X45, X46), tree(X47, X45, X48)) :- delmin(X46, X47, X48).\nand substitutionT1 -> T44,\nX44 -> T44,\nX45 -> T45,\nX46 -> T49,\nT2 -> tree(T44, T45, T49),\nX47 -> T47,\nX48 -> T48,\nT3 -> tree(T47, T45, T48),\nT46 -> T49", fontsize=14, style = filled, fillcolor = lightblue];
33 -> 129 [arrowhead = none ];
129 -> 44;

130 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
33 -> 130 [arrowhead = none ];
130 -> 45;

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

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

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

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

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

136 [label="EVAL with clause\ndelmin(tree(X61, void, X62), X61, X62).\nand substitutionX61 -> T62,\nX62 -> T63,\nT49 -> tree(T62, void, T63),\nT47 -> T62,\nT48 -> T63", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 136 [arrowhead = none ];
136 -> 59;

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

138 [label="EVAL with clause\ndelmin(tree(X75, X76, X77), X78, tree(X75, X79, X80)) :- delmin(X76, X78, X79).\nand substitutionX75 -> T76,\nX76 -> T82,\nX77 -> T78,\nT49 -> tree(T76, T82, T78),\nT47 -> T79,\nX78 -> T79,\nX79 -> T80,\nX80 -> T81,\nT48 -> tree(T76, T80, T81),\nT77 -> T82", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 138 [arrowhead = none ];
138 -> 67;

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

140 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 140 [arrowhead = none ];
140 -> 61;

141 [label="INSTANCE with matching:\nT49 -> T82\nT47 -> T79\nT48 -> T80", fontsize=14, style = filled, fillcolor = lightgrey];
67 -> 141 [arrowhead = none , style=dashed];
141 -> 44[style=dashed];

142 [label="EVAL with clause\ndelete(X105, tree(X106, X107, X108), tree(X106, X109, X108)) :- ','(less(X105, X106), delete(X105, X107, X109)).\nand substitutionT1 -> T107,\nX105 -> T107,\nX106 -> T108,\nX107 -> T112,\nX108 -> T110,\nT2 -> tree(T108, T112, T110),\nX109 -> T111,\nT3 -> tree(T108, T111, T110),\nT109 -> T112", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 142 [arrowhead = none ];
142 -> 79;

143 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
72 -> 143 [arrowhead = none ];
143 -> 80;

144 [label="EVAL with clause\ndelete(X141, tree(X142, X143, X144), tree(X142, X143, X145)) :- ','(less(X142, X141), delete(X141, X144, X145)).\nand substitutionT1 -> T144,\nX141 -> T144,\nX142 -> T145,\nX143 -> T146,\nX144 -> T149,\nT2 -> tree(T145, T146, T149),\nX145 -> T148,\nT3 -> tree(T145, T146, T148),\nT147 -> T149", fontsize=14, style = filled, fillcolor = lightblue];
73 -> 144 [arrowhead = none ];
144 -> 109;

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

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

147 [label="SPLIT 2\nnew knowledge:\nT107 is ground\nT108 is ground", fontsize=14, style = filled, fillcolor = violet];
79 -> 147 [arrowhead = none ];
147 -> 82;

148 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
81 -> 148 [arrowhead = none ];
148 -> 86;

149 [label="INSTANCE with matching:\nT1 -> T107\nT2 -> T112\nT3 -> T111", fontsize=14, style = filled, fillcolor = lightgrey];
82 -> 149 [arrowhead = none , style=dashed];
149 -> 2[style=dashed];

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

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

152 [label="EVAL with clause\nless(0, s(X118)).\nand substitutionT107 -> 0,\nX118 -> T121,\nT108 -> s(T121)", fontsize=14, style = filled, fillcolor = lightblue];
88 -> 152 [arrowhead = none ];
152 -> 91;

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

154 [label="EVAL with clause\nless(s(X123), s(X124)) :- less(X123, X124).\nand substitutionX123 -> T126,\nT107 -> s(T126),\nX124 -> T127,\nT108 -> s(T127)", fontsize=14, style = filled, fillcolor = lightblue];
89 -> 154 [arrowhead = none ];
154 -> 101;

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

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

157 [label="INSTANCE with matching:\nT107 -> T126\nT108 -> T127", fontsize=14, style = filled, fillcolor = lightgrey];
101 -> 157 [arrowhead = none , style=dashed];
157 -> 81[style=dashed];

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

159 [label="SPLIT 2\nnew knowledge:\nT145 is ground\nT144 is ground", fontsize=14, style = filled, fillcolor = violet];
109 -> 159 [arrowhead = none ];
159 -> 115;

160 [label="INSTANCE with matching:\nT107 -> T145\nT108 -> T144", fontsize=14, style = filled, fillcolor = lightgrey];
114 -> 160 [arrowhead = none , style=dashed];
160 -> 81[style=dashed];

161 [label="INSTANCE with matching:\nT1 -> T144\nT2 -> T149\nT3 -> T148", fontsize=14, style = filled, fillcolor = lightgrey];
115 -> 161 [arrowhead = none , style=dashed];
161 -> 2[style=dashed];

}

(2) Obligation:

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

f2_in(T12, T13) → f2_out1
f2_in(T44, tree(T47, T45, T48)) → U1(f44_in(T47, T48), T44, tree(T47, T45, T48))
U1(f44_out1, T44, tree(T47, T45, T48)) → f2_out1
f2_in(T107, tree(T108, T111, T110)) → U2(f79_in(T107, T108, T111), T107, tree(T108, T111, T110))
U2(f79_out1, T107, tree(T108, T111, T110)) → f2_out1
f2_in(T144, tree(T145, T146, T148)) → U3(f109_in(T145, T144, T148), T144, tree(T145, T146, T148))
U3(f109_out1, T144, tree(T145, T146, T148)) → f2_out1
f44_in(T62, T63) → f44_out1
f44_in(T79, tree(T76, T80, T81)) → U4(f44_in(T79, T80), T79, tree(T76, T80, T81))
U4(f44_out1, T79, tree(T76, T80, T81)) → f44_out1
f81_in(0, s(T121)) → f81_out1
f81_in(s(T126), s(T127)) → U5(f81_in(T126, T127), s(T126), s(T127))
U5(f81_out1, s(T126), s(T127)) → f81_out1
f79_in(T107, T108, T111) → U6(f81_in(T107, T108), T107, T108, T111)
U6(f81_out1, T107, T108, T111) → U7(f2_in(T107, T111), T107, T108, T111)
U7(f2_out1, T107, T108, T111) → f79_out1
f109_in(T145, T144, T148) → U8(f81_in(T145, T144), T145, T144, T148)
U8(f81_out1, T145, T144, T148) → U9(f2_in(T144, T148), T145, T144, T148)
U9(f2_out1, T145, T144, T148) → f109_out1

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:

F2_IN(T44, tree(T47, T45, T48)) → U1¹(f44_in(T47, T48), T44, tree(T47, T45, T48))
F2_IN(T44, tree(T47, T45, T48)) → F44_IN(T47, T48)
F2_IN(T107, tree(T108, T111, T110)) → U2¹(f79_in(T107, T108, T111), T107, tree(T108, T111, T110))
F2_IN(T107, tree(T108, T111, T110)) → F79_IN(T107, T108, T111)
F2_IN(T144, tree(T145, T146, T148)) → U3¹(f109_in(T145, T144, T148), T144, tree(T145, T146, T148))
F2_IN(T144, tree(T145, T146, T148)) → F109_IN(T145, T144, T148)
F44_IN(T79, tree(T76, T80, T81)) → U4¹(f44_in(T79, T80), T79, tree(T76, T80, T81))
F44_IN(T79, tree(T76, T80, T81)) → F44_IN(T79, T80)
F81_IN(s(T126), s(T127)) → U5¹(f81_in(T126, T127), s(T126), s(T127))
F81_IN(s(T126), s(T127)) → F81_IN(T126, T127)
F79_IN(T107, T108, T111) → U6¹(f81_in(T107, T108), T107, T108, T111)
F79_IN(T107, T108, T111) → F81_IN(T107, T108)
U6¹(f81_out1, T107, T108, T111) → U7¹(f2_in(T107, T111), T107, T108, T111)
U6¹(f81_out1, T107, T108, T111) → F2_IN(T107, T111)
F109_IN(T145, T144, T148) → U8¹(f81_in(T145, T144), T145, T144, T148)
F109_IN(T145, T144, T148) → F81_IN(T145, T144)
U8¹(f81_out1, T145, T144, T148) → U9¹(f2_in(T144, T148), T145, T144, T148)
U8¹(f81_out1, T145, T144, T148) → F2_IN(T144, T148)

The TRS R consists of the following rules:

f2_in(T12, T13) → f2_out1
f2_in(T44, tree(T47, T45, T48)) → U1(f44_in(T47, T48), T44, tree(T47, T45, T48))
U1(f44_out1, T44, tree(T47, T45, T48)) → f2_out1
f2_in(T107, tree(T108, T111, T110)) → U2(f79_in(T107, T108, T111), T107, tree(T108, T111, T110))
U2(f79_out1, T107, tree(T108, T111, T110)) → f2_out1
f2_in(T144, tree(T145, T146, T148)) → U3(f109_in(T145, T144, T148), T144, tree(T145, T146, T148))
U3(f109_out1, T144, tree(T145, T146, T148)) → f2_out1
f44_in(T62, T63) → f44_out1
f44_in(T79, tree(T76, T80, T81)) → U4(f44_in(T79, T80), T79, tree(T76, T80, T81))
U4(f44_out1, T79, tree(T76, T80, T81)) → f44_out1
f81_in(0, s(T121)) → f81_out1
f81_in(s(T126), s(T127)) → U5(f81_in(T126, T127), s(T126), s(T127))
U5(f81_out1, s(T126), s(T127)) → f81_out1
f79_in(T107, T108, T111) → U6(f81_in(T107, T108), T107, T108, T111)
U6(f81_out1, T107, T108, T111) → U7(f2_in(T107, T111), T107, T108, T111)
U7(f2_out1, T107, T108, T111) → f79_out1
f109_in(T145, T144, T148) → U8(f81_in(T145, T144), T145, T144, T148)
U8(f81_out1, T145, T144, T148) → U9(f2_in(T144, T148), T145, T144, T148)
U9(f2_out1, T145, T144, T148) → f109_out1

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:

F81_IN(s(T126), s(T127)) → F81_IN(T126, T127)

The TRS R consists of the following rules:

f2_in(T12, T13) → f2_out1
f2_in(T44, tree(T47, T45, T48)) → U1(f44_in(T47, T48), T44, tree(T47, T45, T48))
U1(f44_out1, T44, tree(T47, T45, T48)) → f2_out1
f2_in(T107, tree(T108, T111, T110)) → U2(f79_in(T107, T108, T111), T107, tree(T108, T111, T110))
U2(f79_out1, T107, tree(T108, T111, T110)) → f2_out1
f2_in(T144, tree(T145, T146, T148)) → U3(f109_in(T145, T144, T148), T144, tree(T145, T146, T148))
U3(f109_out1, T144, tree(T145, T146, T148)) → f2_out1
f44_in(T62, T63) → f44_out1
f44_in(T79, tree(T76, T80, T81)) → U4(f44_in(T79, T80), T79, tree(T76, T80, T81))
U4(f44_out1, T79, tree(T76, T80, T81)) → f44_out1
f81_in(0, s(T121)) → f81_out1
f81_in(s(T126), s(T127)) → U5(f81_in(T126, T127), s(T126), s(T127))
U5(f81_out1, s(T126), s(T127)) → f81_out1
f79_in(T107, T108, T111) → U6(f81_in(T107, T108), T107, T108, T111)
U6(f81_out1, T107, T108, T111) → U7(f2_in(T107, T111), T107, T108, T111)
U7(f2_out1, T107, T108, T111) → f79_out1
f109_in(T145, T144, T148) → U8(f81_in(T145, T144), T145, T144, T148)
U8(f81_out1, T145, T144, T148) → U9(f2_in(T144, T148), T145, T144, T148)
U9(f2_out1, T145, T144, T148) → f109_out1

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:

F81_IN(s(T126), s(T127)) → F81_IN(T126, T127)

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:

• F81_IN(s(T126), s(T127)) → F81_IN(T126, T127)
  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:

F44_IN(T79, tree(T76, T80, T81)) → F44_IN(T79, T80)

The TRS R consists of the following rules:

f2_in(T12, T13) → f2_out1
f2_in(T44, tree(T47, T45, T48)) → U1(f44_in(T47, T48), T44, tree(T47, T45, T48))
U1(f44_out1, T44, tree(T47, T45, T48)) → f2_out1
f2_in(T107, tree(T108, T111, T110)) → U2(f79_in(T107, T108, T111), T107, tree(T108, T111, T110))
U2(f79_out1, T107, tree(T108, T111, T110)) → f2_out1
f2_in(T144, tree(T145, T146, T148)) → U3(f109_in(T145, T144, T148), T144, tree(T145, T146, T148))
U3(f109_out1, T144, tree(T145, T146, T148)) → f2_out1
f44_in(T62, T63) → f44_out1
f44_in(T79, tree(T76, T80, T81)) → U4(f44_in(T79, T80), T79, tree(T76, T80, T81))
U4(f44_out1, T79, tree(T76, T80, T81)) → f44_out1
f81_in(0, s(T121)) → f81_out1
f81_in(s(T126), s(T127)) → U5(f81_in(T126, T127), s(T126), s(T127))
U5(f81_out1, s(T126), s(T127)) → f81_out1
f79_in(T107, T108, T111) → U6(f81_in(T107, T108), T107, T108, T111)
U6(f81_out1, T107, T108, T111) → U7(f2_in(T107, T111), T107, T108, T111)
U7(f2_out1, T107, T108, T111) → f79_out1
f109_in(T145, T144, T148) → U8(f81_in(T145, T144), T145, T144, T148)
U8(f81_out1, T145, T144, T148) → U9(f2_in(T144, T148), T145, T144, T148)
U9(f2_out1, T145, T144, T148) → f109_out1

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:

F44_IN(T79, tree(T76, T80, T81)) → F44_IN(T79, T80)

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:

• F44_IN(T79, tree(T76, T80, T81)) → F44_IN(T79, T80)
  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:

F2_IN(T107, tree(T108, T111, T110)) → F79_IN(T107, T108, T111)
F79_IN(T107, T108, T111) → U6¹(f81_in(T107, T108), T107, T108, T111)
U6¹(f81_out1, T107, T108, T111) → F2_IN(T107, T111)
F2_IN(T144, tree(T145, T146, T148)) → F109_IN(T145, T144, T148)
F109_IN(T145, T144, T148) → U8¹(f81_in(T145, T144), T145, T144, T148)
U8¹(f81_out1, T145, T144, T148) → F2_IN(T144, T148)

The TRS R consists of the following rules:

f2_in(T12, T13) → f2_out1
f2_in(T44, tree(T47, T45, T48)) → U1(f44_in(T47, T48), T44, tree(T47, T45, T48))
U1(f44_out1, T44, tree(T47, T45, T48)) → f2_out1
f2_in(T107, tree(T108, T111, T110)) → U2(f79_in(T107, T108, T111), T107, tree(T108, T111, T110))
U2(f79_out1, T107, tree(T108, T111, T110)) → f2_out1
f2_in(T144, tree(T145, T146, T148)) → U3(f109_in(T145, T144, T148), T144, tree(T145, T146, T148))
U3(f109_out1, T144, tree(T145, T146, T148)) → f2_out1
f44_in(T62, T63) → f44_out1
f44_in(T79, tree(T76, T80, T81)) → U4(f44_in(T79, T80), T79, tree(T76, T80, T81))
U4(f44_out1, T79, tree(T76, T80, T81)) → f44_out1
f81_in(0, s(T121)) → f81_out1
f81_in(s(T126), s(T127)) → U5(f81_in(T126, T127), s(T126), s(T127))
U5(f81_out1, s(T126), s(T127)) → f81_out1
f79_in(T107, T108, T111) → U6(f81_in(T107, T108), T107, T108, T111)
U6(f81_out1, T107, T108, T111) → U7(f2_in(T107, T111), T107, T108, T111)
U7(f2_out1, T107, T108, T111) → f79_out1
f109_in(T145, T144, T148) → U8(f81_in(T145, T144), T145, T144, T148)
U8(f81_out1, T145, T144, T148) → U9(f2_in(T144, T148), T145, T144, T148)
U9(f2_out1, T145, T144, T148) → f109_out1

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

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

• F79_IN(T107, T108, T111) → U6¹(f81_in(T107, T108), T107, T108, T111)
  The graph contains the following edges 1 >= 2, 2 >= 3, 3 >= 4

• U6¹(f81_out1, T107, T108, T111) → F2_IN(T107, T111)
  The graph contains the following edges 2 >= 1, 4 >= 2

• U8¹(f81_out1, T145, T144, T148) → F2_IN(T144, T148)
  The graph contains the following edges 3 >= 1, 4 >= 2

• F2_IN(T107, tree(T108, T111, T110)) → F79_IN(T107, T108, T111)
  The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

• F2_IN(T144, tree(T145, T146, T148)) → F109_IN(T145, T144, T148)
  The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3

• F109_IN(T145, T144, T148) → U8¹(f81_in(T145, T144), T145, T144, T148)
  The graph contains the following edges 1 >= 2, 2 >= 3, 3 >= 4

(19) YES