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

(0) Obligation:

Clauses:

f(0, Y, 0).
f(s(X), Y, Z) :- ','(f(X, Y, U), f(U, Y, Z)).

Query: f(g,a,a)

(1) PrologToTRSTransformerProof (SOUND transformation)

Transformed Prolog program to TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: f(T1, T2, T3)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: f(T1, T2, T3), SCOPE: 1, CLAUSE: 0 | f(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: f(T1, T2, T3), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: f(T1, T2, T3), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(f(T15, T18, X16), f(X16, T18, T19))\n\nT15 is ground\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: f(T15, T18, X16)\n\nT15 is ground\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: f(T22, T23, T24)\n\nT22 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: f(T15, T18, X16), SCOPE: 2, CLAUSE: 0 | f(T15, T18, X16), SCOPE: 2, CLAUSE: 1\n\nT15 is ground\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: f(T15, T18, X16), SCOPE: 2, CLAUSE: 0\n\nT15 is ground\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: f(T15, T18, X16), SCOPE: 2, CLAUSE: 1\n\nT15 is ground\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(f(T36, T38, X38), f(X38, T38, X39))\n\nT36 is ground\nX39 is free\nX38 is free", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: f(T36, T38, X38)\n\nT36 is ground\nX38 is free", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: f(T41, T42, X39)\n\nT41 is ground\nX39 is free", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 66 [arrowhead = none ];
66 -> 5;

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

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

69 [label="EVAL with clause\nf(0, X5, 0).\nand substitutionT1 -> 0,\nT2 -> T8,\nX5 -> T8,\nT3 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 69 [arrowhead = none ];
69 -> 12;

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

71 [label="EVAL with clause\nf(s(X13), X14, X15) :- ','(f(X13, X14, X16), f(X16, X14, X15)).\nand substitutionX13 -> T15,\nT1 -> s(T15),\nT2 -> T18,\nX14 -> T18,\nT3 -> T19,\nX15 -> T19,\nT16 -> T18,\nT17 -> T19", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 71 [arrowhead = none ];
71 -> 16;

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

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

74 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
16 -> 74 [arrowhead = none ];
74 -> 35;

75 [label="SPLIT 2\nnew knowledge:\nT15 is ground\nT22 is ground\nreplacements:X16 -> T22,\nT18 -> T23,\nT19 -> T24", fontsize=14, style = filled, fillcolor = violet];
16 -> 75 [arrowhead = none ];
75 -> 36;

76 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
35 -> 76 [arrowhead = none ];
76 -> 44;

77 [label="INSTANCE with matching:\nT1 -> T22\nT2 -> T23\nT3 -> T24", fontsize=14, style = filled, fillcolor = lightgrey];
36 -> 77 [arrowhead = none , style=dashed];
77 -> 1[style=dashed];

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

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

80 [label="EVAL with clause\nf(0, X25, 0).\nand substitutionT15 -> 0,\nT18 -> T31,\nX25 -> T31,\nX16 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 80 [arrowhead = none ];
80 -> 50;

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

82 [label="EVAL with clause\nf(s(X35), X36, X37) :- ','(f(X35, X36, X38), f(X38, X36, X37)).\nand substitutionX35 -> T36,\nT15 -> s(T36),\nT18 -> T38,\nX36 -> T38,\nX16 -> X39,\nX37 -> X39,\nT37 -> T38", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 82 [arrowhead = none ];
82 -> 59;

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

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

85 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
59 -> 85 [arrowhead = none ];
85 -> 64;

86 [label="SPLIT 2\nnew knowledge:\nT36 is ground\nT41 is ground\nreplacements:X38 -> T41,\nT38 -> T42", fontsize=14, style = filled, fillcolor = violet];
59 -> 86 [arrowhead = none ];
86 -> 65;

87 [label="INSTANCE with matching:\nT15 -> T36\nT18 -> T38\nX16 -> X38", fontsize=14, style = filled, fillcolor = lightgrey];
64 -> 87 [arrowhead = none , style=dashed];
87 -> 35[style=dashed];

88 [label="INSTANCE with matching:\nT15 -> T41\nT18 -> T42\nX16 -> X39", fontsize=14, style = filled, fillcolor = lightgrey];
65 -> 88 [arrowhead = none , style=dashed];
88 -> 35[style=dashed];

}

(2) Obligation:

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

f1_in(0) → f1_out1(0)
f1_in(s(T15)) → U1(f16_in(T15), s(T15))
U1(f16_out1(X16, T19), s(T15)) → f1_out1(T19)
f35_in(0) → f35_out1(0)
f35_in(s(T36)) → U2(f59_in(T36), s(T36))
U2(f59_out1(X38, X39), s(T36)) → f35_out1(X39)
f16_in(T15) → U3(f35_in(T15), T15)
U3(f35_out1(T22), T15) → U4(f1_in(T22), T15, T22)
U4(f1_out1(T24), T15, T22) → f16_out1(T22, T24)
f59_in(T36) → U5(f35_in(T36), T36)
U5(f35_out1(T41), T36) → U6(f35_in(T41), T36, T41)
U6(f35_out1(X39), T36, T41) → f59_out1(T41, X39)

Q is empty.

(3) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Combined order from the following AFS and order.
f1_in(x1)  =  f1_in(x1)
0  =  0
f1_out1(x1)  =  f1_out1(x1)
s(x1)  =  s(x1)
U1(x1, x2)  =  U1(x1, x2)
f16_in(x1)  =  f16_in(x1)
f16_out1(x1, x2)  =  f16_out1(x1, x2)
f35_in(x1)  =  f35_in(x1)
f35_out1(x1)  =  x1
U2(x1, x2)  =  U2(x1, x2)
f59_in(x1)  =  f59_in(x1)
f59_out1(x1, x2)  =  f59_out1(x1, x2)
U3(x1, x2)  =  U3(x1, x2)
U4(x1, x2, x3)  =  U4(x1, x2, x3)
U5(x1, x2)  =  U5(x1, x2)
U6(x1, x2, x3)  =  U6(x1, x2, x3)

Recursive path order with status [RPO].
Quasi-Precedence:

[s₁, f16_in1] > [f1_in1, U3₂] > 0 > f59_out12
[s₁, f16_in1] > [f1_in1, U3₂] > [f1_out11, U1₂] > f16_out12 > f59_out12
[s₁, f16_in1] > [f1_in1, U3₂] > U4₃ > f16_out12 > f59_out12
[s₁, f16_in1] > f59_in1 > U5₂ > [f35_in1, U2₂] > f59_out12
[s₁, f16_in1] > f59_in1 > U5₂ > U6₃ > f59_out12

Status:

f1_in1: multiset
0: multiset
f1_out11: multiset
s₁: [1]
U1₂: multiset
f16_in1: [1]
f16_out12: multiset
f35_in1: [1]
U2₂: [1,2]
f59_in1: multiset
f59_out12: [1,2]
U3₂: multiset
U4₃: multiset
U5₂: [1,2]
U6₃: [1,2,3]

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

f1_in(0) → f1_out1(0)
f1_in(s(T15)) → U1(f16_in(T15), s(T15))
U1(f16_out1(X16, T19), s(T15)) → f1_out1(T19)
f35_in(0) → f35_out1(0)
f35_in(s(T36)) → U2(f59_in(T36), s(T36))
U2(f59_out1(X38, X39), s(T36)) → f35_out1(X39)
f16_in(T15) → U3(f35_in(T15), T15)
U3(f35_out1(T22), T15) → U4(f1_in(T22), T15, T22)
U4(f1_out1(T24), T15, T22) → f16_out1(T22, T24)
f59_in(T36) → U5(f35_in(T36), T36)
U5(f35_out1(T41), T36) → U6(f35_in(T41), T36, T41)
U6(f35_out1(X39), T36, T41) → f59_out1(T41, X39)

(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