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

(0) Obligation:

Clauses:

member(X, .(X, X1)).
member(X, .(X2, Xs)) :- member(X, Xs).

Query: member(a,g)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: member(T1, T2)\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: member(T1, T2), SCOPE: 1, CLAUSE: 0 | member(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: true | member(T1, .(T5, T6)), SCOPE: 1, CLAUSE: 1\n\nT5 is ground\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: member(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT2 is ground\nX5 is free\nX6 is free\nmember(T1, T2) !=? member(X5, .(X5, X6))", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: member(T1, .(T5, T6)), SCOPE: 1, CLAUSE: 1\n\nT5 is ground\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: member(T13, T12)\n\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: member(T13, T12), SCOPE: 2, CLAUSE: 0 | member(T13, T12), SCOPE: 2, CLAUSE: 1\n\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: member(T13, T12), SCOPE: 2, CLAUSE: 0\n\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: member(T13, T12), SCOPE: 2, CLAUSE: 1\n\nT12 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: member(T33, T32)\n\nT32 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: member(T44, T43)\n\nT42 is ground\nT43 is ground\nX5 is free\nX6 is free\nmember(T1, .(T42, T43)) !=? member(X5, .(X5, X6))", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: member(T44, T43), SCOPE: 3, CLAUSE: 0 | member(T44, T43), SCOPE: 3, CLAUSE: 1\n\nT42 is ground\nT43 is ground\nX5 is free\nX6 is free\nmember(T1, .(T42, T43)) !=? member(X5, .(X5, X6))", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: member(T44, T43), SCOPE: 3, CLAUSE: 0\n\nT42 is ground\nT43 is ground\nX5 is free\nX6 is free\nmember(T1, .(T42, T43)) !=? member(X5, .(X5, X6))", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: member(T44, T43), SCOPE: 3, CLAUSE: 1\n\nT42 is ground\nT43 is ground\nX5 is free\nX6 is free\nmember(T1, .(T42, T43)) !=? member(X5, .(X5, X6))", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: member(T64, T63)\n\nT42 is ground\nT62 is ground\nT63 is ground\nX5 is free\nX6 is free\nmember(T1, .(T42, .(T62, T63))) !=? member(X5, .(X5, X6))", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 56 [arrowhead = none ];
56 -> 2;

57 [label="EVAL with clause\nmember(X5, .(X5, X6)).\nand substitutionT1 -> T5,\nX5 -> T5,\nX6 -> T6,\nT2 -> .(T5, T6)", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 57 [arrowhead = none ];
57 -> 10;

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

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

60 [label="EVAL with clause\nmember(X39, .(X40, X41)) :- member(X39, X41).\nand substitutionT1 -> T44,\nX39 -> T44,\nX40 -> T42,\nX41 -> T43,\nT2 -> .(T42, T43),\nT41 -> T44", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 60 [arrowhead = none ];
60 -> 38;

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

62 [label="ONLY EVAL with clause\nmember(X10, .(X11, X12)) :- member(X10, X12).\nand substitutionT1 -> T13,\nX10 -> T13,\nT5 -> T11,\nX11 -> T11,\nT6 -> T12,\nX12 -> T12,\nT10 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
14 -> 62 [arrowhead = none ];
62 -> 17;

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

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

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

66 [label="EVAL with clause\nmember(X21, .(X21, X22)).\nand substitutionT13 -> T22,\nX21 -> T22,\nX22 -> T23,\nT12 -> .(T22, T23)", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 66 [arrowhead = none ];
66 -> 31;

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

68 [label="EVAL with clause\nmember(X29, .(X30, X31)) :- member(X29, X31).\nand substitutionT13 -> T33,\nX29 -> T33,\nX30 -> T31,\nX31 -> T32,\nT12 -> .(T31, T32),\nT30 -> T33", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 68 [arrowhead = none ];
68 -> 36;

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

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

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

72 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
38 -> 72 [arrowhead = none ];
72 -> 42;

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

74 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
42 -> 74 [arrowhead = none ];
74 -> 45;

75 [label="EVAL with clause\nmember(X50, .(X50, X51)).\nand substitutionT44 -> T53,\nX50 -> T53,\nX51 -> T54,\nT43 -> .(T53, T54)", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 75 [arrowhead = none ];
75 -> 48;

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

77 [label="EVAL with clause\nmember(X58, .(X59, X60)) :- member(X58, X60).\nand substitutionT44 -> T64,\nX58 -> T64,\nX59 -> T62,\nX60 -> T63,\nT43 -> .(T62, T63),\nT61 -> T64", fontsize=14, style = filled, fillcolor = lightblue];
45 -> 77 [arrowhead = none ];
77 -> 54;

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

79 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
48 -> 79 [arrowhead = none ];
79 -> 50;

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

}

(2) Obligation:

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

f1_in(.(T5, T6)) → f1_out1(T5)
f1_in(.(T11, .(T22, T23))) → f1_out1(T22)
f1_in(.(T11, .(T31, T32))) → U1(f1_in(T32), .(T11, .(T31, T32)))
U1(f1_out1(T33), .(T11, .(T31, T32))) → f1_out1(T33)
f1_in(.(T42, .(T62, T63))) → U2(f1_in(T63), .(T42, .(T62, T63)))
U2(f1_out1(T64), .(T42, .(T62, T63))) → f1_out1(T64)

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = 2 + 2·x₁ + 2·x₂   
POL(U1(x₁, x₂)) = x₁ + x₂   
POL(U2(x₁, x₂)) = 1 + 2·x₁ + x₂   
POL(f1_in(x₁)) = 2·x₁   
POL(f1_out1(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(.(T5, T6)) → f1_out1(T5)
f1_in(.(T11, .(T22, T23))) → f1_out1(T22)
f1_in(.(T11, .(T31, T32))) → U1(f1_in(T32), .(T11, .(T31, T32)))
U1(f1_out1(T33), .(T11, .(T31, T32))) → f1_out1(T33)
f1_in(.(T42, .(T62, T63))) → U2(f1_in(T63), .(T42, .(T62, T63)))
U2(f1_out1(T64), .(T42, .(T62, T63))) → f1_out1(T64)

(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