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

(0) Obligation:

Clauses:

tree_member(X, tree(X, X1, X2)).
tree_member(X, tree(X3, Left, X4)) :- tree_member(X, Left).
tree_member(X, tree(X5, X6, Right)) :- tree_member(X, Right).

Query: tree_member(a,g)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: tree_member(T1, T2)\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: tree_member(T1, T2), SCOPE: 1, CLAUSE: 0 | tree_member(T1, T2), SCOPE: 1, CLAUSE: 1 | tree_member(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: tree_member(T1, T2), SCOPE: 1, CLAUSE: 0\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: tree_member(T1, T2), SCOPE: 1, CLAUSE: 1 | tree_member(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT2 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];
18 [label="18: tree_member(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: tree_member(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: tree_member(T38, T36)\n\nT36 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: tree_member(T57, T56)\n\nT56 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 42 [arrowhead = none ];
42 -> 6;

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

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

45 [label="EVAL with clause\ntree_member(X19, tree(X19, X20, X21)).\nand substitutionT1 -> T15,\nX19 -> T15,\nX20 -> T16,\nX21 -> T17,\nT2 -> tree(T15, T16, T17)", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 45 [arrowhead = none ];
45 -> 11;

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

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

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

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

50 [label="EVAL with clause\ntree_member(X38, tree(X39, X40, X41)) :- tree_member(X38, X40).\nand substitutionT1 -> T38,\nX38 -> T38,\nX39 -> T35,\nX40 -> T36,\nX41 -> T37,\nT2 -> tree(T35, T36, T37),\nT34 -> T38", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 50 [arrowhead = none ];
50 -> 24;

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

52 [label="EVAL with clause\ntree_member(X56, tree(X57, X58, X59)) :- tree_member(X56, X59).\nand substitutionT1 -> T57,\nX56 -> T57,\nX57 -> T54,\nX58 -> T55,\nX59 -> T56,\nT2 -> tree(T54, T55, T56),\nT53 -> T57", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 52 [arrowhead = none ];
52 -> 40;

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

54 [label="INSTANCE with matching:\nT1 -> T38\nT2 -> T36", fontsize=14, style = filled, fillcolor = lightgrey];
24 -> 54 [arrowhead = none , style=dashed];
54 -> 1[style=dashed];

55 [label="INSTANCE with matching:\nT1 -> T57\nT2 -> T56", fontsize=14, style = filled, fillcolor = lightgrey];
40 -> 55 [arrowhead = none , style=dashed];
55 -> 1[style=dashed];

}

(2) Obligation:

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

f1_in(tree(T15, T16, T17)) → f1_out1(T15)
f1_in(tree(T35, T36, T37)) → U1(f1_in(T36), tree(T35, T36, T37))
U1(f1_out1(T38), tree(T35, T36, T37)) → f1_out1(T38)
f1_in(tree(T54, T55, T56)) → U2(f1_in(T56), tree(T54, T55, T56))
U2(f1_out1(T57), tree(T54, T55, T56)) → f1_out1(T57)

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(U1(x₁, x₂)) = 2 + x₁ + x₂   
POL(U2(x₁, x₂)) = 1 + x₁ + x₂   
POL(f1_in(x₁)) = 2·x₁   
POL(f1_out1(x₁)) = 2·x₁   
POL(tree(x₁, x₂, x₃)) = 2 + 2·x₁ + 2·x₂ + 2·x₃   

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

f1_in(tree(T15, T16, T17)) → f1_out1(T15)
U1(f1_out1(T38), tree(T35, T36, T37)) → f1_out1(T38)
f1_in(tree(T54, T55, T56)) → U2(f1_in(T56), tree(T54, T55, T56))
U2(f1_out1(T57), tree(T54, T55, T56)) → f1_out1(T57)

(4) Obligation:

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

f1_in(tree(T35, T36, T37)) → U1(f1_in(T36), tree(T35, T36, T37))

Q is empty.

(5) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(U1(x₁, x₂)) = 1 + x₁ + x₂   
POL(f1_in(x₁)) = 2·x₁   
POL(tree(x₁, x₂, x₃)) = 2 + x₁ + 2·x₂ + x₃   

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

f1_in(tree(T35, T36, T37)) → U1(f1_in(T36), tree(T35, T36, T37))

(6) Obligation:

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

(7) RisEmptyProof (EQUIVALENT transformation)

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

(8) YES