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

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="2: delmin(T1, T2, T3)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: delmin(T1, T2, T3), SCOPE: 1, CLAUSE: 5 | delmin(T1, T2, T3), SCOPE: 1, CLAUSE: 6\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: delmin(T1, T2, T3), SCOPE: 1, CLAUSE: 5\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: delmin(T1, T2, T3), SCOPE: 1, CLAUSE: 6\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];
15 [label="15: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: delmin(T27, T32, T33)\n\nT27 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 28 [arrowhead = none ];
28 -> 5;

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

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

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

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

33 [label="EVAL with clause\ndelmin(tree(X26, X27, X28), X29, tree(X26, X30, X31)) :- delmin(X27, X29, X30).\nand substitutionX26 -> T26,\nX27 -> T27,\nX28 -> T28,\nT1 -> tree(T26, T27, T28),\nT2 -> T32,\nX29 -> T32,\nX30 -> T33,\nX31 -> T31,\nT3 -> tree(T26, T33, T31),\nT29 -> T32,\nT30 -> T33", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 33 [arrowhead = none ];
33 -> 25;

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

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

36 [label="INSTANCE with matching:\nT1 -> T27\nT2 -> T32\nT3 -> T33", fontsize=14, style = filled, fillcolor = lightgrey];
25 -> 36 [arrowhead = none , style=dashed];
36 -> 2[style=dashed];

}

(2) Obligation:

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

f2_in(tree(T12, void, T13)) → f2_out1(T12)
f2_in(tree(T26, T27, T28)) → U1(f2_in(T27), tree(T26, T27, T28))
U1(f2_out1(T32), tree(T26, T27, T28)) → f2_out1(T32)

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(U1(x₁, x₂)) = x₁ + x₂   
POL(f2_in(x₁)) = 2·x₁   
POL(f2_out1(x₁)) = 2·x₁   
POL(tree(x₁, x₂, x₃)) = 1 + 2·x₁ + 2·x₂ + x₃   
POL(void) = 2   

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

f2_in(tree(T12, void, T13)) → f2_out1(T12)
f2_in(tree(T26, T27, T28)) → U1(f2_in(T27), tree(T26, T27, T28))
U1(f2_out1(T32), tree(T26, T27, T28)) → f2_out1(T32)

(4) Obligation:

Q restricted rewrite system:
R is empty.
Q is empty.

(5) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(6) YES