Left Termination of the query pattern
insert(g,a,g)
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,a,g)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="2: insert(T1, T2, T3)\n\nT1 is ground\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: 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\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 0\n\nT1 is ground\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: 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\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 2 | insert(T1, T2, T3), SCOPE: 1, CLAUSE: 3\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];
37 [label="37: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: insert(T1, T2, T3), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nT3 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ','(less(T44, T45), insert(T44, T49, T48))\n\nT44 is ground\nT45 is ground\nT48 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: less(T44, T45)\n\nT44 is ground\nT45 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: insert(T44, T49, T48)\n\nT44 is ground\nT48 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: 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];
62 [label="62: less(T44, T45), SCOPE: 2, CLAUSE: 4\n\nT44 is ground\nT45 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: less(T44, T45), SCOPE: 2, CLAUSE: 5\n\nT44 is ground\nT45 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: less(T63, T64)\n\nT63 is ground\nT64 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: ','(less(T80, T79), insert(T79, T84, T83))\n\nT79 is ground\nT80 is ground\nT83 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: less(T80, T79)\n\nT79 is ground\nT80 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: insert(T79, T84, T83)\n\nT79 is ground\nT83 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 93 [arrowhead = none ];
93 -> 5;

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

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

96 [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 -> 96 [arrowhead = none ];
96 -> 15;

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

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

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

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

101 [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];
20 -> 101 [arrowhead = none ];
101 -> 26;

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

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

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

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

106 [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 -> T49,\nX45 -> T47,\nT2 -> tree(T45, T49, T47),\nX46 -> T48,\nT3 -> tree(T45, T48, T47),\nT46 -> T49", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 106 [arrowhead = none ];
106 -> 51;

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

108 [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 -> T84,\nT2 -> tree(T80, T81, T84),\nX80 -> T83,\nT3 -> tree(T80, T81, T83),\nT82 -> T84", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 108 [arrowhead = none ];
108 -> 86;

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

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

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

112 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
55 -> 112 [arrowhead = none ];
112 -> 61;

113 [label="INSTANCE with matching:\nT1 -> T44\nT2 -> T49\nT3 -> T48", fontsize=14, style = filled, fillcolor = lightgrey];
56 -> 113 [arrowhead = none , style=dashed];
113 -> 2[style=dashed];

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

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

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

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

118 [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];
64 -> 118 [arrowhead = none ];
118 -> 70;

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

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

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

122 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
86 -> 122 [arrowhead = none ];
122 -> 91;

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

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

125 [label="INSTANCE with matching:\nT1 -> T79\nT2 -> T84\nT3 -> T83", fontsize=14, style = filled, fillcolor = lightgrey];
92 -> 125 [arrowhead = none , style=dashed];
125 -> 2[style=dashed];

}

(2) Obligation:

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

f2_in(T8, tree(T8, void, void)) → f2_out1(void)
f2_in(T21, tree(T21, T22, T23)) → f2_out1(tree(T21, T22, T23))
f2_in(T44, tree(T45, T48, T47)) → U1(f51_in(T44, T45, T48), T44, tree(T45, T48, T47))
U1(f51_out1(T49), T44, tree(T45, T48, T47)) → f2_out1(tree(T45, T49, T47))
f2_in(T79, tree(T80, T81, T83)) → U2(f86_in(T80, T79, T83), T79, tree(T80, T81, T83))
U2(f86_out1(T84), T79, tree(T80, T81, T83)) → f2_out1(tree(T80, T81, T84))
f55_in(0, s(T58)) → f55_out1
f55_in(s(T63), s(T64)) → U3(f55_in(T63, T64), s(T63), s(T64))
U3(f55_out1, s(T63), s(T64)) → f55_out1
f51_in(T44, T45, T48) → U4(f55_in(T44, T45), T44, T45, T48)
U4(f55_out1, T44, T45, T48) → U5(f2_in(T44, T48), T44, T45, T48)
U5(f2_out1(T49), T44, T45, T48) → f51_out1(T49)
f86_in(T80, T79, T83) → U6(f55_in(T80, T79), T80, T79, T83)
U6(f55_out1, T80, T79, T83) → U7(f2_in(T79, T83), T80, T79, T83)
U7(f2_out1(T84), T80, T79, T83) → f86_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:

F2_IN(T44, tree(T45, T48, T47)) → U1¹(f51_in(T44, T45, T48), T44, tree(T45, T48, T47))
F2_IN(T44, tree(T45, T48, T47)) → F51_IN(T44, T45, T48)
F2_IN(T79, tree(T80, T81, T83)) → U2¹(f86_in(T80, T79, T83), T79, tree(T80, T81, T83))
F2_IN(T79, tree(T80, T81, T83)) → F86_IN(T80, T79, T83)
F55_IN(s(T63), s(T64)) → U3¹(f55_in(T63, T64), s(T63), s(T64))
F55_IN(s(T63), s(T64)) → F55_IN(T63, T64)
F51_IN(T44, T45, T48) → U4¹(f55_in(T44, T45), T44, T45, T48)
F51_IN(T44, T45, T48) → F55_IN(T44, T45)
U4¹(f55_out1, T44, T45, T48) → U5¹(f2_in(T44, T48), T44, T45, T48)
U4¹(f55_out1, T44, T45, T48) → F2_IN(T44, T48)
F86_IN(T80, T79, T83) → U6¹(f55_in(T80, T79), T80, T79, T83)
F86_IN(T80, T79, T83) → F55_IN(T80, T79)
U6¹(f55_out1, T80, T79, T83) → U7¹(f2_in(T79, T83), T80, T79, T83)
U6¹(f55_out1, T80, T79, T83) → F2_IN(T79, T83)

The TRS R consists of the following rules:

f2_in(T8, tree(T8, void, void)) → f2_out1(void)
f2_in(T21, tree(T21, T22, T23)) → f2_out1(tree(T21, T22, T23))
f2_in(T44, tree(T45, T48, T47)) → U1(f51_in(T44, T45, T48), T44, tree(T45, T48, T47))
U1(f51_out1(T49), T44, tree(T45, T48, T47)) → f2_out1(tree(T45, T49, T47))
f2_in(T79, tree(T80, T81, T83)) → U2(f86_in(T80, T79, T83), T79, tree(T80, T81, T83))
U2(f86_out1(T84), T79, tree(T80, T81, T83)) → f2_out1(tree(T80, T81, T84))
f55_in(0, s(T58)) → f55_out1
f55_in(s(T63), s(T64)) → U3(f55_in(T63, T64), s(T63), s(T64))
U3(f55_out1, s(T63), s(T64)) → f55_out1
f51_in(T44, T45, T48) → U4(f55_in(T44, T45), T44, T45, T48)
U4(f55_out1, T44, T45, T48) → U5(f2_in(T44, T48), T44, T45, T48)
U5(f2_out1(T49), T44, T45, T48) → f51_out1(T49)
f86_in(T80, T79, T83) → U6(f55_in(T80, T79), T80, T79, T83)
U6(f55_out1, T80, T79, T83) → U7(f2_in(T79, T83), T80, T79, T83)
U7(f2_out1(T84), T80, T79, T83) → f86_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:

F55_IN(s(T63), s(T64)) → F55_IN(T63, T64)

The TRS R consists of the following rules:

f2_in(T8, tree(T8, void, void)) → f2_out1(void)
f2_in(T21, tree(T21, T22, T23)) → f2_out1(tree(T21, T22, T23))
f2_in(T44, tree(T45, T48, T47)) → U1(f51_in(T44, T45, T48), T44, tree(T45, T48, T47))
U1(f51_out1(T49), T44, tree(T45, T48, T47)) → f2_out1(tree(T45, T49, T47))
f2_in(T79, tree(T80, T81, T83)) → U2(f86_in(T80, T79, T83), T79, tree(T80, T81, T83))
U2(f86_out1(T84), T79, tree(T80, T81, T83)) → f2_out1(tree(T80, T81, T84))
f55_in(0, s(T58)) → f55_out1
f55_in(s(T63), s(T64)) → U3(f55_in(T63, T64), s(T63), s(T64))
U3(f55_out1, s(T63), s(T64)) → f55_out1
f51_in(T44, T45, T48) → U4(f55_in(T44, T45), T44, T45, T48)
U4(f55_out1, T44, T45, T48) → U5(f2_in(T44, T48), T44, T45, T48)
U5(f2_out1(T49), T44, T45, T48) → f51_out1(T49)
f86_in(T80, T79, T83) → U6(f55_in(T80, T79), T80, T79, T83)
U6(f55_out1, T80, T79, T83) → U7(f2_in(T79, T83), T80, T79, T83)
U7(f2_out1(T84), T80, T79, T83) → f86_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:

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

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

F2_IN(T44, tree(T45, T48, T47)) → F51_IN(T44, T45, T48)
F51_IN(T44, T45, T48) → U4¹(f55_in(T44, T45), T44, T45, T48)
U4¹(f55_out1, T44, T45, T48) → F2_IN(T44, T48)
F2_IN(T79, tree(T80, T81, T83)) → F86_IN(T80, T79, T83)
F86_IN(T80, T79, T83) → U6¹(f55_in(T80, T79), T80, T79, T83)
U6¹(f55_out1, T80, T79, T83) → F2_IN(T79, T83)

The TRS R consists of the following rules:

f2_in(T8, tree(T8, void, void)) → f2_out1(void)
f2_in(T21, tree(T21, T22, T23)) → f2_out1(tree(T21, T22, T23))
f2_in(T44, tree(T45, T48, T47)) → U1(f51_in(T44, T45, T48), T44, tree(T45, T48, T47))
U1(f51_out1(T49), T44, tree(T45, T48, T47)) → f2_out1(tree(T45, T49, T47))
f2_in(T79, tree(T80, T81, T83)) → U2(f86_in(T80, T79, T83), T79, tree(T80, T81, T83))
U2(f86_out1(T84), T79, tree(T80, T81, T83)) → f2_out1(tree(T80, T81, T84))
f55_in(0, s(T58)) → f55_out1
f55_in(s(T63), s(T64)) → U3(f55_in(T63, T64), s(T63), s(T64))
U3(f55_out1, s(T63), s(T64)) → f55_out1
f51_in(T44, T45, T48) → U4(f55_in(T44, T45), T44, T45, T48)
U4(f55_out1, T44, T45, T48) → U5(f2_in(T44, T48), T44, T45, T48)
U5(f2_out1(T49), T44, T45, T48) → f51_out1(T49)
f86_in(T80, T79, T83) → U6(f55_in(T80, T79), T80, T79, T83)
U6(f55_out1, T80, T79, T83) → U7(f2_in(T79, T83), T80, T79, T83)
U7(f2_out1(T84), T80, T79, T83) → f86_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:

• F51_IN(T44, T45, T48) → U4¹(f55_in(T44, T45), T44, T45, T48)
  The graph contains the following edges 1 >= 2, 2 >= 3, 3 >= 4

• U4¹(f55_out1, T44, T45, T48) → F2_IN(T44, T48)
  The graph contains the following edges 2 >= 1, 4 >= 2

• U6¹(f55_out1, T80, T79, T83) → F2_IN(T79, T83)
  The graph contains the following edges 3 >= 1, 4 >= 2

• F2_IN(T44, tree(T45, T48, T47)) → F51_IN(T44, T45, T48)
  The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

• F2_IN(T79, tree(T80, T81, T83)) → F86_IN(T80, T79, T83)
  The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3

• F86_IN(T80, T79, T83) → U6¹(f55_in(T80, T79), T80, T79, T83)
  The graph contains the following edges 1 >= 2, 2 >= 3, 3 >= 4

(14) YES