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

(0) Obligation:

Clauses:

insert(X, void, tree(X, void, void)).
insert(X, tree(X, Left, Right), tree(X, Left, Right)).
insert(X, tree(Y, Left, Right), tree(Y, Left1, Right)) :- ','(less(X, Y), insert(X, Left, Left1)).
insert(X, tree(Y, Left, Right), tree(Y, Left, Right1)) :- ','(less(Y, X), insert(X, Right, Right1)).
less(0, s(X1)).
less(s(X), s(Y)) :- less(X, Y).

Query: insert(g,g,a)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: insert(T1, T2, T3)\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 0\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 1 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 3\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];
11 [label="11: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(less(T44, T45), insert(T44, T46, T49))\n\nT44 is ground\nT45 is ground\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: less(T44, T45)\n\nT44 is ground\nT45 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: insert(T44, T46, T49)\n\nT44 is ground\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: less(T44, T45), SCOPE: 2, CLAUSE: 4 | less(T44, T45), SCOPE: 2, CLAUSE: 5\n\nT44 is ground\nT45 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: less(T44, T45), SCOPE: 2, CLAUSE: 4\n\nT44 is ground\nT45 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: less(T44, T45), SCOPE: 2, CLAUSE: 5\n\nT44 is ground\nT45 is ground", 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];
76 [label="76: less(T63, T64)\n\nT63 is ground\nT64 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: ','(less(T80, T79), insert(T79, T82, T84))\n\nT79 is ground\nT80 is ground\nT82 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
96 [label="96: less(T80, T79)\n\nT79 is ground\nT80 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: insert(T79, T82, T84)\n\nT79 is ground\nT82 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 98 [arrowhead = none ];
98 -> 4;

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

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

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

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

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

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

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

106 [label="EVAL with clause\ninsert(X19, tree(X19, X20, X21), tree(X19, X20, X21)).\nand substitutionT1 -> T21,\nX19 -> T21,\nX20 -> T22,\nX21 -> T23,\nT2 -> tree(T21, T22, T23),\nT3 -> tree(T21, T22, T23)", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 106 [arrowhead = none ];
106 -> 22;

107 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
18 -> 107 [arrowhead = none ];
107 -> 23;

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

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

110 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
22 -> 110 [arrowhead = none ];
110 -> 25;

111 [label="EVAL with clause\ninsert(X42, tree(X43, X44, X45), tree(X43, X46, X45)) :- ','(less(X42, X43), insert(X42, X44, X46)).\nand substitutionT1 -> T44,\nX42 -> T44,\nX43 -> T45,\nX44 -> T46,\nX45 -> T47,\nT2 -> tree(T45, T46, T47),\nX46 -> T49,\nT3 -> tree(T45, T49, T47),\nT48 -> T49", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 111 [arrowhead = none ];
111 -> 38;

112 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 112 [arrowhead = none ];
112 -> 39;

113 [label="EVAL with clause\ninsert(X76, tree(X77, X78, X79), tree(X77, X78, X80)) :- ','(less(X77, X76), insert(X76, X79, X80)).\nand substitutionT1 -> T79,\nX76 -> T79,\nX77 -> T80,\nX78 -> T81,\nX79 -> T82,\nT2 -> tree(T80, T81, T82),\nX80 -> T84,\nT3 -> tree(T80, T81, T84),\nT83 -> T84", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 113 [arrowhead = none ];
113 -> 92;

114 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 114 [arrowhead = none ];
114 -> 93;

115 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
38 -> 115 [arrowhead = none ];
115 -> 56;

116 [label="SPLIT 2\nnew knowledge:\nT44 is ground\nT45 is ground", fontsize=14, style = filled, fillcolor = violet];
38 -> 116 [arrowhead = none ];
116 -> 59;

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

118 [label="INSTANCE with matching:\nT1 -> T44\nT2 -> T46\nT3 -> T49", fontsize=14, style = filled, fillcolor = lightgrey];
59 -> 118 [arrowhead = none , style=dashed];
118 -> 1[style=dashed];

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

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

121 [label="EVAL with clause\nless(0, s(X55)).\nand substitutionT44 -> 0,\nX55 -> T58,\nT45 -> s(T58)", fontsize=14, style = filled, fillcolor = lightblue];
66 -> 121 [arrowhead = none ];
121 -> 70;

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

123 [label="EVAL with clause\nless(s(X60), s(X61)) :- less(X60, X61).\nand substitutionX60 -> T63,\nT44 -> s(T63),\nX61 -> T64,\nT45 -> s(T64)", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 123 [arrowhead = none ];
123 -> 76;

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

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

126 [label="INSTANCE with matching:\nT44 -> T63\nT45 -> T64", fontsize=14, style = filled, fillcolor = lightgrey];
76 -> 126 [arrowhead = none , style=dashed];
126 -> 56[style=dashed];

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

128 [label="SPLIT 2\nnew knowledge:\nT80 is ground\nT79 is ground", fontsize=14, style = filled, fillcolor = violet];
92 -> 128 [arrowhead = none ];
128 -> 97;

129 [label="INSTANCE with matching:\nT44 -> T80\nT45 -> T79", fontsize=14, style = filled, fillcolor = lightgrey];
96 -> 129 [arrowhead = none , style=dashed];
129 -> 56[style=dashed];

130 [label="INSTANCE with matching:\nT1 -> T79\nT2 -> T82\nT3 -> T84", fontsize=14, style = filled, fillcolor = lightgrey];
97 -> 130 [arrowhead = none , style=dashed];
130 -> 1[style=dashed];

}

(2) Obligation:

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

f1_in(T8, void) → f1_out1(tree(T8, void, void))
f1_in(T21, tree(T21, T22, T23)) → f1_out1(tree(T21, T22, T23))
f1_in(T44, tree(T45, T46, T47)) → U1(f38_in(T44, T45, T46), T44, tree(T45, T46, T47))
U1(f38_out1(T49), T44, tree(T45, T46, T47)) → f1_out1(tree(T45, T49, T47))
f1_in(T79, tree(T80, T81, T82)) → U2(f92_in(T80, T79, T82), T79, tree(T80, T81, T82))
U2(f92_out1(T84), T79, tree(T80, T81, T82)) → f1_out1(tree(T80, T81, T84))
f56_in(0, s(T58)) → f56_out1
f56_in(s(T63), s(T64)) → U3(f56_in(T63, T64), s(T63), s(T64))
U3(f56_out1, s(T63), s(T64)) → f56_out1
f38_in(T44, T45, T46) → U4(f56_in(T44, T45), T44, T45, T46)
U4(f56_out1, T44, T45, T46) → U5(f1_in(T44, T46), T44, T45, T46)
U5(f1_out1(T49), T44, T45, T46) → f38_out1(T49)
f92_in(T80, T79, T82) → U6(f56_in(T80, T79), T80, T79, T82)
U6(f56_out1, T80, T79, T82) → U7(f1_in(T79, T82), T80, T79, T82)
U7(f1_out1(T84), T80, T79, T82) → f92_out1(T84)

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(T44, tree(T45, T46, T47)) → U1¹(f38_in(T44, T45, T46), T44, tree(T45, T46, T47))
F1_IN(T44, tree(T45, T46, T47)) → F38_IN(T44, T45, T46)
F1_IN(T79, tree(T80, T81, T82)) → U2¹(f92_in(T80, T79, T82), T79, tree(T80, T81, T82))
F1_IN(T79, tree(T80, T81, T82)) → F92_IN(T80, T79, T82)
F56_IN(s(T63), s(T64)) → U3¹(f56_in(T63, T64), s(T63), s(T64))
F56_IN(s(T63), s(T64)) → F56_IN(T63, T64)
F38_IN(T44, T45, T46) → U4¹(f56_in(T44, T45), T44, T45, T46)
F38_IN(T44, T45, T46) → F56_IN(T44, T45)
U4¹(f56_out1, T44, T45, T46) → U5¹(f1_in(T44, T46), T44, T45, T46)
U4¹(f56_out1, T44, T45, T46) → F1_IN(T44, T46)
F92_IN(T80, T79, T82) → U6¹(f56_in(T80, T79), T80, T79, T82)
F92_IN(T80, T79, T82) → F56_IN(T80, T79)
U6¹(f56_out1, T80, T79, T82) → U7¹(f1_in(T79, T82), T80, T79, T82)
U6¹(f56_out1, T80, T79, T82) → F1_IN(T79, T82)

The TRS R consists of the following rules:

f1_in(T8, void) → f1_out1(tree(T8, void, void))
f1_in(T21, tree(T21, T22, T23)) → f1_out1(tree(T21, T22, T23))
f1_in(T44, tree(T45, T46, T47)) → U1(f38_in(T44, T45, T46), T44, tree(T45, T46, T47))
U1(f38_out1(T49), T44, tree(T45, T46, T47)) → f1_out1(tree(T45, T49, T47))
f1_in(T79, tree(T80, T81, T82)) → U2(f92_in(T80, T79, T82), T79, tree(T80, T81, T82))
U2(f92_out1(T84), T79, tree(T80, T81, T82)) → f1_out1(tree(T80, T81, T84))
f56_in(0, s(T58)) → f56_out1
f56_in(s(T63), s(T64)) → U3(f56_in(T63, T64), s(T63), s(T64))
U3(f56_out1, s(T63), s(T64)) → f56_out1
f38_in(T44, T45, T46) → U4(f56_in(T44, T45), T44, T45, T46)
U4(f56_out1, T44, T45, T46) → U5(f1_in(T44, T46), T44, T45, T46)
U5(f1_out1(T49), T44, T45, T46) → f38_out1(T49)
f92_in(T80, T79, T82) → U6(f56_in(T80, T79), T80, T79, T82)
U6(f56_out1, T80, T79, T82) → U7(f1_in(T79, T82), T80, T79, T82)
U7(f1_out1(T84), T80, T79, T82) → f92_out1(T84)

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 7 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

F56_IN(s(T63), s(T64)) → F56_IN(T63, T64)

The TRS R consists of the following rules:

f1_in(T8, void) → f1_out1(tree(T8, void, void))
f1_in(T21, tree(T21, T22, T23)) → f1_out1(tree(T21, T22, T23))
f1_in(T44, tree(T45, T46, T47)) → U1(f38_in(T44, T45, T46), T44, tree(T45, T46, T47))
U1(f38_out1(T49), T44, tree(T45, T46, T47)) → f1_out1(tree(T45, T49, T47))
f1_in(T79, tree(T80, T81, T82)) → U2(f92_in(T80, T79, T82), T79, tree(T80, T81, T82))
U2(f92_out1(T84), T79, tree(T80, T81, T82)) → f1_out1(tree(T80, T81, T84))
f56_in(0, s(T58)) → f56_out1
f56_in(s(T63), s(T64)) → U3(f56_in(T63, T64), s(T63), s(T64))
U3(f56_out1, s(T63), s(T64)) → f56_out1
f38_in(T44, T45, T46) → U4(f56_in(T44, T45), T44, T45, T46)
U4(f56_out1, T44, T45, T46) → U5(f1_in(T44, T46), T44, T45, T46)
U5(f1_out1(T49), T44, T45, T46) → f38_out1(T49)
f92_in(T80, T79, T82) → U6(f56_in(T80, T79), T80, T79, T82)
U6(f56_out1, T80, T79, T82) → U7(f1_in(T79, T82), T80, T79, T82)
U7(f1_out1(T84), T80, T79, T82) → f92_out1(T84)

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:

F56_IN(s(T63), s(T64)) → F56_IN(T63, T64)

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:

• F56_IN(s(T63), s(T64)) → F56_IN(T63, T64)
  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:

F1_IN(T44, tree(T45, T46, T47)) → F38_IN(T44, T45, T46)
F38_IN(T44, T45, T46) → U4¹(f56_in(T44, T45), T44, T45, T46)
U4¹(f56_out1, T44, T45, T46) → F1_IN(T44, T46)
F1_IN(T79, tree(T80, T81, T82)) → F92_IN(T80, T79, T82)
F92_IN(T80, T79, T82) → U6¹(f56_in(T80, T79), T80, T79, T82)
U6¹(f56_out1, T80, T79, T82) → F1_IN(T79, T82)

The TRS R consists of the following rules:

f1_in(T8, void) → f1_out1(tree(T8, void, void))
f1_in(T21, tree(T21, T22, T23)) → f1_out1(tree(T21, T22, T23))
f1_in(T44, tree(T45, T46, T47)) → U1(f38_in(T44, T45, T46), T44, tree(T45, T46, T47))
U1(f38_out1(T49), T44, tree(T45, T46, T47)) → f1_out1(tree(T45, T49, T47))
f1_in(T79, tree(T80, T81, T82)) → U2(f92_in(T80, T79, T82), T79, tree(T80, T81, T82))
U2(f92_out1(T84), T79, tree(T80, T81, T82)) → f1_out1(tree(T80, T81, T84))
f56_in(0, s(T58)) → f56_out1
f56_in(s(T63), s(T64)) → U3(f56_in(T63, T64), s(T63), s(T64))
U3(f56_out1, s(T63), s(T64)) → f56_out1
f38_in(T44, T45, T46) → U4(f56_in(T44, T45), T44, T45, T46)
U4(f56_out1, T44, T45, T46) → U5(f1_in(T44, T46), T44, T45, T46)
U5(f1_out1(T49), T44, T45, T46) → f38_out1(T49)
f92_in(T80, T79, T82) → U6(f56_in(T80, T79), T80, T79, T82)
U6(f56_out1, T80, T79, T82) → U7(f1_in(T79, T82), T80, T79, T82)
U7(f1_out1(T84), T80, T79, T82) → f92_out1(T84)

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

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

• F38_IN(T44, T45, T46) → U4¹(f56_in(T44, T45), T44, T45, T46)
  The graph contains the following edges 1 >= 2, 2 >= 3, 3 >= 4

• U4¹(f56_out1, T44, T45, T46) → F1_IN(T44, T46)
  The graph contains the following edges 2 >= 1, 4 >= 2

• U6¹(f56_out1, T80, T79, T82) → F1_IN(T79, T82)
  The graph contains the following edges 3 >= 1, 4 >= 2

• F1_IN(T44, tree(T45, T46, T47)) → F38_IN(T44, T45, T46)
  The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

• F1_IN(T79, tree(T80, T81, T82)) → F92_IN(T80, T79, T82)
  The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3

• F92_IN(T80, T79, T82) → U6¹(f56_in(T80, T79), T80, T79, T82)
  The graph contains the following edges 1 >= 2, 2 >= 3, 3 >= 4

(14) YES