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

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇐)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇐)
↳4 PiDP
↳5 DependencyGraphProof (⇔)
↳6 AND
    ↳7 PiDP
        ↳8 PiDPToQDPProof (⇐)
        ↳9 QDP
        ↳10 MRRProof (⇔)
        ↳11 QDP
        ↳12 DependencyGraphProof (⇔)
        ↳13 TRUE
    ↳14 PiDP
        ↳15 PiDPToQDPProof (⇐)
        ↳16 QDP
        ↳17 MRRProof (⇔)
        ↳18 QDP
        ↳19 DependencyGraphProof (⇔)
        ↳20 TRUE

(0) Obligation:

Clauses:

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

Queries:

f(g,a,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

p7(s(T32), T34, X47, T35) :- f23(T32, T34, X46).
p7(s(T32), T39, X47, T40) :- ','(fc23(T32, T39, T38), p7(T38, T39, X47, T40)).
f23(s(T52), T54, X74) :- f23(T52, T54, X73).
f23(s(T52), T58, X74) :- ','(fc23(T52, T58, T57), f23(T57, T58, X74)).
f1(s(T9), T12, T13) :- p7(T9, T12, X13, T13).

Clauses:

qc7(0, T27, 0, 0).
qc7(s(T32), T39, X47, T40) :- ','(fc23(T32, T39, T38), qc7(T38, T39, X47, T40)).
fc23(0, T47, 0).
fc23(s(T52), T58, X74) :- ','(fc23(T52, T58, T57), fc23(T57, T58, X74)).

Afs:

f1(x1, x2, x3)  =  f1(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
f1_in: (b,f,f)
p7_in: (b,f,f,f)
f23_in: (b,f,f)
fc23_in: (b,f,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

F1_IN_GAA(s(T9), T12, T13) → U7_GAA(T9, T12, T13, p7_in_gaaa(T9, T12, X13, T13))
F1_IN_GAA(s(T9), T12, T13) → P7_IN_GAAA(T9, T12, X13, T13)
P7_IN_GAAA(s(T32), T34, X47, T35) → U1_GAAA(T32, T34, X47, T35, f23_in_gaa(T32, T34, X46))
P7_IN_GAAA(s(T32), T34, X47, T35) → F23_IN_GAA(T32, T34, X46)
F23_IN_GAA(s(T52), T54, X74) → U4_GAA(T52, T54, X74, f23_in_gaa(T52, T54, X73))
F23_IN_GAA(s(T52), T54, X74) → F23_IN_GAA(T52, T54, X73)
F23_IN_GAA(s(T52), T58, X74) → U5_GAA(T52, T58, X74, fc23_in_gaa(T52, T58, T57))
U5_GAA(T52, T58, X74, fc23_out_gaa(T52, T58, T57)) → U6_GAA(T52, T58, X74, f23_in_gaa(T57, T58, X74))
U5_GAA(T52, T58, X74, fc23_out_gaa(T52, T58, T57)) → F23_IN_GAA(T57, T58, X74)
P7_IN_GAAA(s(T32), T39, X47, T40) → U2_GAAA(T32, T39, X47, T40, fc23_in_gaa(T32, T39, T38))
U2_GAAA(T32, T39, X47, T40, fc23_out_gaa(T32, T39, T38)) → U3_GAAA(T32, T39, X47, T40, p7_in_gaaa(T38, T39, X47, T40))
U2_GAAA(T32, T39, X47, T40, fc23_out_gaa(T32, T39, T38)) → P7_IN_GAAA(T38, T39, X47, T40)

The TRS R consists of the following rules:

fc23_in_gaa(0, T47, 0) → fc23_out_gaa(0, T47, 0)
fc23_in_gaa(s(T52), T58, X74) → U11_gaa(T52, T58, X74, fc23_in_gaa(T52, T58, T57))
U11_gaa(T52, T58, X74, fc23_out_gaa(T52, T58, T57)) → U12_gaa(T52, T58, X74, T57, fc23_in_gaa(T57, T58, X74))
U12_gaa(T52, T58, X74, T57, fc23_out_gaa(T57, T58, X74)) → fc23_out_gaa(s(T52), T58, X74)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
p7_in_gaaa(x1, x2, x3, x4)  =  p7_in_gaaa(x1)
f23_in_gaa(x1, x2, x3)  =  f23_in_gaa(x1)
fc23_in_gaa(x1, x2, x3)  =  fc23_in_gaa(x1)
0  =  0
fc23_out_gaa(x1, x2, x3)  =  fc23_out_gaa(x1, x3)
U11_gaa(x1, x2, x3, x4)  =  U11_gaa(x1, x4)
U12_gaa(x1, x2, x3, x4, x5)  =  U12_gaa(x1, x5)
F1_IN_GAA(x1, x2, x3)  =  F1_IN_GAA(x1)
U7_GAA(x1, x2, x3, x4)  =  U7_GAA(x1, x4)
P7_IN_GAAA(x1, x2, x3, x4)  =  P7_IN_GAAA(x1)
U1_GAAA(x1, x2, x3, x4, x5)  =  U1_GAAA(x1, x5)
F23_IN_GAA(x1, x2, x3)  =  F23_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4)  =  U4_GAA(x1, x4)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x4)
U6_GAA(x1, x2, x3, x4)  =  U6_GAA(x1, x4)
U2_GAAA(x1, x2, x3, x4, x5)  =  U2_GAAA(x1, x5)
U3_GAAA(x1, x2, x3, x4, x5)  =  U3_GAAA(x1, x5)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

F1_IN_GAA(s(T9), T12, T13) → U7_GAA(T9, T12, T13, p7_in_gaaa(T9, T12, X13, T13))
F1_IN_GAA(s(T9), T12, T13) → P7_IN_GAAA(T9, T12, X13, T13)
P7_IN_GAAA(s(T32), T34, X47, T35) → U1_GAAA(T32, T34, X47, T35, f23_in_gaa(T32, T34, X46))
P7_IN_GAAA(s(T32), T34, X47, T35) → F23_IN_GAA(T32, T34, X46)
F23_IN_GAA(s(T52), T54, X74) → U4_GAA(T52, T54, X74, f23_in_gaa(T52, T54, X73))
F23_IN_GAA(s(T52), T54, X74) → F23_IN_GAA(T52, T54, X73)
F23_IN_GAA(s(T52), T58, X74) → U5_GAA(T52, T58, X74, fc23_in_gaa(T52, T58, T57))
U5_GAA(T52, T58, X74, fc23_out_gaa(T52, T58, T57)) → U6_GAA(T52, T58, X74, f23_in_gaa(T57, T58, X74))
U5_GAA(T52, T58, X74, fc23_out_gaa(T52, T58, T57)) → F23_IN_GAA(T57, T58, X74)
P7_IN_GAAA(s(T32), T39, X47, T40) → U2_GAAA(T32, T39, X47, T40, fc23_in_gaa(T32, T39, T38))
U2_GAAA(T32, T39, X47, T40, fc23_out_gaa(T32, T39, T38)) → U3_GAAA(T32, T39, X47, T40, p7_in_gaaa(T38, T39, X47, T40))
U2_GAAA(T32, T39, X47, T40, fc23_out_gaa(T32, T39, T38)) → P7_IN_GAAA(T38, T39, X47, T40)

The TRS R consists of the following rules:

fc23_in_gaa(0, T47, 0) → fc23_out_gaa(0, T47, 0)
fc23_in_gaa(s(T52), T58, X74) → U11_gaa(T52, T58, X74, fc23_in_gaa(T52, T58, T57))
U11_gaa(T52, T58, X74, fc23_out_gaa(T52, T58, T57)) → U12_gaa(T52, T58, X74, T57, fc23_in_gaa(T57, T58, X74))
U12_gaa(T52, T58, X74, T57, fc23_out_gaa(T57, T58, X74)) → fc23_out_gaa(s(T52), T58, X74)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
p7_in_gaaa(x1, x2, x3, x4)  =  p7_in_gaaa(x1)
f23_in_gaa(x1, x2, x3)  =  f23_in_gaa(x1)
fc23_in_gaa(x1, x2, x3)  =  fc23_in_gaa(x1)
0  =  0
fc23_out_gaa(x1, x2, x3)  =  fc23_out_gaa(x1, x3)
U11_gaa(x1, x2, x3, x4)  =  U11_gaa(x1, x4)
U12_gaa(x1, x2, x3, x4, x5)  =  U12_gaa(x1, x5)
F1_IN_GAA(x1, x2, x3)  =  F1_IN_GAA(x1)
U7_GAA(x1, x2, x3, x4)  =  U7_GAA(x1, x4)
P7_IN_GAAA(x1, x2, x3, x4)  =  P7_IN_GAAA(x1)
U1_GAAA(x1, x2, x3, x4, x5)  =  U1_GAAA(x1, x5)
F23_IN_GAA(x1, x2, x3)  =  F23_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4)  =  U4_GAA(x1, x4)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x4)
U6_GAA(x1, x2, x3, x4)  =  U6_GAA(x1, x4)
U2_GAAA(x1, x2, x3, x4, x5)  =  U2_GAAA(x1, x5)
U3_GAAA(x1, x2, x3, x4, x5)  =  U3_GAAA(x1, x5)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 7 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

F23_IN_GAA(s(T52), T58, X74) → U5_GAA(T52, T58, X74, fc23_in_gaa(T52, T58, T57))
U5_GAA(T52, T58, X74, fc23_out_gaa(T52, T58, T57)) → F23_IN_GAA(T57, T58, X74)
F23_IN_GAA(s(T52), T54, X74) → F23_IN_GAA(T52, T54, X73)

The TRS R consists of the following rules:

fc23_in_gaa(0, T47, 0) → fc23_out_gaa(0, T47, 0)
fc23_in_gaa(s(T52), T58, X74) → U11_gaa(T52, T58, X74, fc23_in_gaa(T52, T58, T57))
U11_gaa(T52, T58, X74, fc23_out_gaa(T52, T58, T57)) → U12_gaa(T52, T58, X74, T57, fc23_in_gaa(T57, T58, X74))
U12_gaa(T52, T58, X74, T57, fc23_out_gaa(T57, T58, X74)) → fc23_out_gaa(s(T52), T58, X74)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
fc23_in_gaa(x1, x2, x3)  =  fc23_in_gaa(x1)
0  =  0
fc23_out_gaa(x1, x2, x3)  =  fc23_out_gaa(x1, x3)
U11_gaa(x1, x2, x3, x4)  =  U11_gaa(x1, x4)
U12_gaa(x1, x2, x3, x4, x5)  =  U12_gaa(x1, x5)
F23_IN_GAA(x1, x2, x3)  =  F23_IN_GAA(x1)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x4)

We have to consider all (P,R,Pi)-chains

(8) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

F23_IN_GAA(s(T52)) → U5_GAA(T52, fc23_in_gaa(T52))
U5_GAA(T52, fc23_out_gaa(T52, T57)) → F23_IN_GAA(T57)
F23_IN_GAA(s(T52)) → F23_IN_GAA(T52)

The TRS R consists of the following rules:

fc23_in_gaa(0) → fc23_out_gaa(0, 0)
fc23_in_gaa(s(T52)) → U11_gaa(T52, fc23_in_gaa(T52))
U11_gaa(T52, fc23_out_gaa(T52, T57)) → U12_gaa(T52, fc23_in_gaa(T57))
U12_gaa(T52, fc23_out_gaa(T57, X74)) → fc23_out_gaa(s(T52), X74)

The set Q consists of the following terms:

fc23_in_gaa(x0)
U11_gaa(x0, x1)
U12_gaa(x0, x1)

We have to consider all (P,Q,R)-chains.

(10) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

F23_IN_GAA(s(T52)) → U5_GAA(T52, fc23_in_gaa(T52))
F23_IN_GAA(s(T52)) → F23_IN_GAA(T52)


Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(F23_IN_GAA(x1)) = 2 + 2·x1   
POL(U11_gaa(x1, x2)) = 1 + x1 + x2   
POL(U12_gaa(x1, x2)) = 1 + 2·x1 + x2   
POL(U5_GAA(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(fc23_in_gaa(x1)) = x1   
POL(fc23_out_gaa(x1, x2)) = x1 + x2   
POL(s(x1)) = 1 + 2·x1   

(11) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U5_GAA(T52, fc23_out_gaa(T52, T57)) → F23_IN_GAA(T57)

The TRS R consists of the following rules:

fc23_in_gaa(0) → fc23_out_gaa(0, 0)
fc23_in_gaa(s(T52)) → U11_gaa(T52, fc23_in_gaa(T52))
U11_gaa(T52, fc23_out_gaa(T52, T57)) → U12_gaa(T52, fc23_in_gaa(T57))
U12_gaa(T52, fc23_out_gaa(T57, X74)) → fc23_out_gaa(s(T52), X74)

The set Q consists of the following terms:

fc23_in_gaa(x0)
U11_gaa(x0, x1)
U12_gaa(x0, x1)

We have to consider all (P,Q,R)-chains.

(12) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(13) TRUE

(14) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

P7_IN_GAAA(s(T32), T39, X47, T40) → U2_GAAA(T32, T39, X47, T40, fc23_in_gaa(T32, T39, T38))
U2_GAAA(T32, T39, X47, T40, fc23_out_gaa(T32, T39, T38)) → P7_IN_GAAA(T38, T39, X47, T40)

The TRS R consists of the following rules:

fc23_in_gaa(0, T47, 0) → fc23_out_gaa(0, T47, 0)
fc23_in_gaa(s(T52), T58, X74) → U11_gaa(T52, T58, X74, fc23_in_gaa(T52, T58, T57))
U11_gaa(T52, T58, X74, fc23_out_gaa(T52, T58, T57)) → U12_gaa(T52, T58, X74, T57, fc23_in_gaa(T57, T58, X74))
U12_gaa(T52, T58, X74, T57, fc23_out_gaa(T57, T58, X74)) → fc23_out_gaa(s(T52), T58, X74)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
fc23_in_gaa(x1, x2, x3)  =  fc23_in_gaa(x1)
0  =  0
fc23_out_gaa(x1, x2, x3)  =  fc23_out_gaa(x1, x3)
U11_gaa(x1, x2, x3, x4)  =  U11_gaa(x1, x4)
U12_gaa(x1, x2, x3, x4, x5)  =  U12_gaa(x1, x5)
P7_IN_GAAA(x1, x2, x3, x4)  =  P7_IN_GAAA(x1)
U2_GAAA(x1, x2, x3, x4, x5)  =  U2_GAAA(x1, x5)

We have to consider all (P,R,Pi)-chains

(15) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(16) Obligation:

Q DP problem:
The TRS P consists of the following rules:

P7_IN_GAAA(s(T32)) → U2_GAAA(T32, fc23_in_gaa(T32))
U2_GAAA(T32, fc23_out_gaa(T32, T38)) → P7_IN_GAAA(T38)

The TRS R consists of the following rules:

fc23_in_gaa(0) → fc23_out_gaa(0, 0)
fc23_in_gaa(s(T52)) → U11_gaa(T52, fc23_in_gaa(T52))
U11_gaa(T52, fc23_out_gaa(T52, T57)) → U12_gaa(T52, fc23_in_gaa(T57))
U12_gaa(T52, fc23_out_gaa(T57, X74)) → fc23_out_gaa(s(T52), X74)

The set Q consists of the following terms:

fc23_in_gaa(x0)
U11_gaa(x0, x1)
U12_gaa(x0, x1)

We have to consider all (P,Q,R)-chains.

(17) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

P7_IN_GAAA(s(T32)) → U2_GAAA(T32, fc23_in_gaa(T32))


Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(P7_IN_GAAA(x1)) = 2 + 2·x1   
POL(U11_gaa(x1, x2)) = 1 + x1 + x2   
POL(U12_gaa(x1, x2)) = 1 + 2·x1 + 2·x2   
POL(U2_GAAA(x1, x2)) = 2 + x1 + 2·x2   
POL(fc23_in_gaa(x1)) = x1   
POL(fc23_out_gaa(x1, x2)) = x1 + 2·x2   
POL(s(x1)) = 1 + 2·x1   

(18) Obligation:

Q DP problem:
The TRS P consists of the following rules:

U2_GAAA(T32, fc23_out_gaa(T32, T38)) → P7_IN_GAAA(T38)

The TRS R consists of the following rules:

fc23_in_gaa(0) → fc23_out_gaa(0, 0)
fc23_in_gaa(s(T52)) → U11_gaa(T52, fc23_in_gaa(T52))
U11_gaa(T52, fc23_out_gaa(T52, T57)) → U12_gaa(T52, fc23_in_gaa(T57))
U12_gaa(T52, fc23_out_gaa(T57, X74)) → fc23_out_gaa(s(T52), X74)

The set Q consists of the following terms:

fc23_in_gaa(x0)
U11_gaa(x0, x1)
U12_gaa(x0, x1)

We have to consider all (P,Q,R)-chains.

(19) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(20) TRUE