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, Z) :- ','(!, eq(Z, 0)).
f(X, Y, Z) :- ','(p(X, P), ','(f(P, Y, U), f(U, Y, Z))).
p(0, 0).
p(s(X), X).
eq(X, X).

Queries:

f(g,a,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

f15(s(T43), T39, X64) :- f15(T43, T39, X63).
f15(s(T43), T46, X64) :- ','(fc15(T43, T46, T45), f15(T45, T46, X64)).
f1(s(T22), T18, T19) :- f15(T22, T18, X18).
f1(s(T22), T25, T26) :- ','(fc15(T22, T25, T24), f1(T24, T25, T26)).

Clauses:

fc1(0, T6, 0).
fc1(s(T22), T25, T26) :- ','(fc15(T22, T25, T24), fc1(T24, T25, T26)).
fc15(0, T30, 0).
fc15(s(T43), T46, X64) :- ','(fc15(T43, T46, T45), fc15(T45, T46, X64)).

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)
f15_in: (b,f,f)
fc15_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(T22), T18, T19) → U4_GAA(T22, T18, T19, f15_in_gaa(T22, T18, X18))
F1_IN_GAA(s(T22), T18, T19) → F15_IN_GAA(T22, T18, X18)
F15_IN_GAA(s(T43), T39, X64) → U1_GAA(T43, T39, X64, f15_in_gaa(T43, T39, X63))
F15_IN_GAA(s(T43), T39, X64) → F15_IN_GAA(T43, T39, X63)
F15_IN_GAA(s(T43), T46, X64) → U2_GAA(T43, T46, X64, fc15_in_gaa(T43, T46, T45))
U2_GAA(T43, T46, X64, fc15_out_gaa(T43, T46, T45)) → U3_GAA(T43, T46, X64, f15_in_gaa(T45, T46, X64))
U2_GAA(T43, T46, X64, fc15_out_gaa(T43, T46, T45)) → F15_IN_GAA(T45, T46, X64)
F1_IN_GAA(s(T22), T25, T26) → U5_GAA(T22, T25, T26, fc15_in_gaa(T22, T25, T24))
U5_GAA(T22, T25, T26, fc15_out_gaa(T22, T25, T24)) → U6_GAA(T22, T25, T26, f1_in_gaa(T24, T25, T26))
U5_GAA(T22, T25, T26, fc15_out_gaa(T22, T25, T24)) → F1_IN_GAA(T24, T25, T26)

The TRS R consists of the following rules:

fc15_in_gaa(0, T30, 0) → fc15_out_gaa(0, T30, 0)
fc15_in_gaa(s(T43), T46, X64) → U10_gaa(T43, T46, X64, fc15_in_gaa(T43, T46, T45))
U10_gaa(T43, T46, X64, fc15_out_gaa(T43, T46, T45)) → U11_gaa(T43, T46, X64, T45, fc15_in_gaa(T45, T46, X64))
U11_gaa(T43, T46, X64, T45, fc15_out_gaa(T45, T46, X64)) → fc15_out_gaa(s(T43), T46, X64)

The argument filtering Pi contains the following mapping:
f1_in_gaa(x1, x2, x3)  =  f1_in_gaa(x1)
s(x1)  =  s(x1)
f15_in_gaa(x1, x2, x3)  =  f15_in_gaa(x1)
fc15_in_gaa(x1, x2, x3)  =  fc15_in_gaa(x1)
0  =  0
fc15_out_gaa(x1, x2, x3)  =  fc15_out_gaa(x1, x3)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x1, x4)
U11_gaa(x1, x2, x3, x4, x5)  =  U11_gaa(x1, x5)
F1_IN_GAA(x1, x2, x3)  =  F1_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4)  =  U4_GAA(x1, x4)
F15_IN_GAA(x1, x2, x3)  =  F15_IN_GAA(x1)
U1_GAA(x1, x2, x3, x4)  =  U1_GAA(x1, x4)
U2_GAA(x1, x2, x3, x4)  =  U2_GAA(x1, x4)
U3_GAA(x1, x2, x3, x4)  =  U3_GAA(x1, x4)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x4)
U6_GAA(x1, x2, x3, x4)  =  U6_GAA(x1, x4)

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(T22), T18, T19) → U4_GAA(T22, T18, T19, f15_in_gaa(T22, T18, X18))
F1_IN_GAA(s(T22), T18, T19) → F15_IN_GAA(T22, T18, X18)
F15_IN_GAA(s(T43), T39, X64) → U1_GAA(T43, T39, X64, f15_in_gaa(T43, T39, X63))
F15_IN_GAA(s(T43), T39, X64) → F15_IN_GAA(T43, T39, X63)
F15_IN_GAA(s(T43), T46, X64) → U2_GAA(T43, T46, X64, fc15_in_gaa(T43, T46, T45))
U2_GAA(T43, T46, X64, fc15_out_gaa(T43, T46, T45)) → U3_GAA(T43, T46, X64, f15_in_gaa(T45, T46, X64))
U2_GAA(T43, T46, X64, fc15_out_gaa(T43, T46, T45)) → F15_IN_GAA(T45, T46, X64)
F1_IN_GAA(s(T22), T25, T26) → U5_GAA(T22, T25, T26, fc15_in_gaa(T22, T25, T24))
U5_GAA(T22, T25, T26, fc15_out_gaa(T22, T25, T24)) → U6_GAA(T22, T25, T26, f1_in_gaa(T24, T25, T26))
U5_GAA(T22, T25, T26, fc15_out_gaa(T22, T25, T24)) → F1_IN_GAA(T24, T25, T26)

The TRS R consists of the following rules:

fc15_in_gaa(0, T30, 0) → fc15_out_gaa(0, T30, 0)
fc15_in_gaa(s(T43), T46, X64) → U10_gaa(T43, T46, X64, fc15_in_gaa(T43, T46, T45))
U10_gaa(T43, T46, X64, fc15_out_gaa(T43, T46, T45)) → U11_gaa(T43, T46, X64, T45, fc15_in_gaa(T45, T46, X64))
U11_gaa(T43, T46, X64, T45, fc15_out_gaa(T45, T46, X64)) → fc15_out_gaa(s(T43), T46, X64)

The argument filtering Pi contains the following mapping:
f1_in_gaa(x1, x2, x3)  =  f1_in_gaa(x1)
s(x1)  =  s(x1)
f15_in_gaa(x1, x2, x3)  =  f15_in_gaa(x1)
fc15_in_gaa(x1, x2, x3)  =  fc15_in_gaa(x1)
0  =  0
fc15_out_gaa(x1, x2, x3)  =  fc15_out_gaa(x1, x3)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x1, x4)
U11_gaa(x1, x2, x3, x4, x5)  =  U11_gaa(x1, x5)
F1_IN_GAA(x1, x2, x3)  =  F1_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4)  =  U4_GAA(x1, x4)
F15_IN_GAA(x1, x2, x3)  =  F15_IN_GAA(x1)
U1_GAA(x1, x2, x3, x4)  =  U1_GAA(x1, x4)
U2_GAA(x1, x2, x3, x4)  =  U2_GAA(x1, x4)
U3_GAA(x1, x2, x3, x4)  =  U3_GAA(x1, x4)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x4)
U6_GAA(x1, x2, x3, x4)  =  U6_GAA(x1, x4)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

F15_IN_GAA(s(T43), T46, X64) → U2_GAA(T43, T46, X64, fc15_in_gaa(T43, T46, T45))
U2_GAA(T43, T46, X64, fc15_out_gaa(T43, T46, T45)) → F15_IN_GAA(T45, T46, X64)
F15_IN_GAA(s(T43), T39, X64) → F15_IN_GAA(T43, T39, X63)

The TRS R consists of the following rules:

fc15_in_gaa(0, T30, 0) → fc15_out_gaa(0, T30, 0)
fc15_in_gaa(s(T43), T46, X64) → U10_gaa(T43, T46, X64, fc15_in_gaa(T43, T46, T45))
U10_gaa(T43, T46, X64, fc15_out_gaa(T43, T46, T45)) → U11_gaa(T43, T46, X64, T45, fc15_in_gaa(T45, T46, X64))
U11_gaa(T43, T46, X64, T45, fc15_out_gaa(T45, T46, X64)) → fc15_out_gaa(s(T43), T46, X64)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
fc15_in_gaa(x1, x2, x3)  =  fc15_in_gaa(x1)
0  =  0
fc15_out_gaa(x1, x2, x3)  =  fc15_out_gaa(x1, x3)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x1, x4)
U11_gaa(x1, x2, x3, x4, x5)  =  U11_gaa(x1, x5)
F15_IN_GAA(x1, x2, x3)  =  F15_IN_GAA(x1)
U2_GAA(x1, x2, x3, x4)  =  U2_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:

F15_IN_GAA(s(T43)) → U2_GAA(T43, fc15_in_gaa(T43))
U2_GAA(T43, fc15_out_gaa(T43, T45)) → F15_IN_GAA(T45)
F15_IN_GAA(s(T43)) → F15_IN_GAA(T43)

The TRS R consists of the following rules:

fc15_in_gaa(0) → fc15_out_gaa(0, 0)
fc15_in_gaa(s(T43)) → U10_gaa(T43, fc15_in_gaa(T43))
U10_gaa(T43, fc15_out_gaa(T43, T45)) → U11_gaa(T43, fc15_in_gaa(T45))
U11_gaa(T43, fc15_out_gaa(T45, X64)) → fc15_out_gaa(s(T43), X64)

The set Q consists of the following terms:

fc15_in_gaa(x0)
U10_gaa(x0, x1)
U11_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:

F15_IN_GAA(s(T43)) → U2_GAA(T43, fc15_in_gaa(T43))
F15_IN_GAA(s(T43)) → F15_IN_GAA(T43)


Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(F15_IN_GAA(x1)) = 2 + 2·x1   
POL(U10_gaa(x1, x2)) = 1 + x1 + x2   
POL(U11_gaa(x1, x2)) = 1 + 2·x1 + x2   
POL(U2_GAA(x1, x2)) = 2 + 2·x1 + 2·x2   
POL(fc15_in_gaa(x1)) = x1   
POL(fc15_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:

U2_GAA(T43, fc15_out_gaa(T43, T45)) → F15_IN_GAA(T45)

The TRS R consists of the following rules:

fc15_in_gaa(0) → fc15_out_gaa(0, 0)
fc15_in_gaa(s(T43)) → U10_gaa(T43, fc15_in_gaa(T43))
U10_gaa(T43, fc15_out_gaa(T43, T45)) → U11_gaa(T43, fc15_in_gaa(T45))
U11_gaa(T43, fc15_out_gaa(T45, X64)) → fc15_out_gaa(s(T43), X64)

The set Q consists of the following terms:

fc15_in_gaa(x0)
U10_gaa(x0, x1)
U11_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:

F1_IN_GAA(s(T22), T25, T26) → U5_GAA(T22, T25, T26, fc15_in_gaa(T22, T25, T24))
U5_GAA(T22, T25, T26, fc15_out_gaa(T22, T25, T24)) → F1_IN_GAA(T24, T25, T26)

The TRS R consists of the following rules:

fc15_in_gaa(0, T30, 0) → fc15_out_gaa(0, T30, 0)
fc15_in_gaa(s(T43), T46, X64) → U10_gaa(T43, T46, X64, fc15_in_gaa(T43, T46, T45))
U10_gaa(T43, T46, X64, fc15_out_gaa(T43, T46, T45)) → U11_gaa(T43, T46, X64, T45, fc15_in_gaa(T45, T46, X64))
U11_gaa(T43, T46, X64, T45, fc15_out_gaa(T45, T46, X64)) → fc15_out_gaa(s(T43), T46, X64)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
fc15_in_gaa(x1, x2, x3)  =  fc15_in_gaa(x1)
0  =  0
fc15_out_gaa(x1, x2, x3)  =  fc15_out_gaa(x1, x3)
U10_gaa(x1, x2, x3, x4)  =  U10_gaa(x1, x4)
U11_gaa(x1, x2, x3, x4, x5)  =  U11_gaa(x1, x5)
F1_IN_GAA(x1, x2, x3)  =  F1_IN_GAA(x1)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x4)

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:

F1_IN_GAA(s(T22)) → U5_GAA(T22, fc15_in_gaa(T22))
U5_GAA(T22, fc15_out_gaa(T22, T24)) → F1_IN_GAA(T24)

The TRS R consists of the following rules:

fc15_in_gaa(0) → fc15_out_gaa(0, 0)
fc15_in_gaa(s(T43)) → U10_gaa(T43, fc15_in_gaa(T43))
U10_gaa(T43, fc15_out_gaa(T43, T45)) → U11_gaa(T43, fc15_in_gaa(T45))
U11_gaa(T43, fc15_out_gaa(T45, X64)) → fc15_out_gaa(s(T43), X64)

The set Q consists of the following terms:

fc15_in_gaa(x0)
U10_gaa(x0, x1)
U11_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:

F1_IN_GAA(s(T22)) → U5_GAA(T22, fc15_in_gaa(T22))


Used ordering: Polynomial interpretation [POLO]:

POL(0) = 0   
POL(F1_IN_GAA(x1)) = 2 + 2·x1   
POL(U10_gaa(x1, x2)) = 1 + x1 + x2   
POL(U11_gaa(x1, x2)) = 1 + 2·x1 + 2·x2   
POL(U5_GAA(x1, x2)) = 2 + x1 + 2·x2   
POL(fc15_in_gaa(x1)) = x1   
POL(fc15_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:

U5_GAA(T22, fc15_out_gaa(T22, T24)) → F1_IN_GAA(T24)

The TRS R consists of the following rules:

fc15_in_gaa(0) → fc15_out_gaa(0, 0)
fc15_in_gaa(s(T43)) → U10_gaa(T43, fc15_in_gaa(T43))
U10_gaa(T43, fc15_out_gaa(T43, T45)) → U11_gaa(T43, fc15_in_gaa(T45))
U11_gaa(T43, fc15_out_gaa(T45, X64)) → fc15_out_gaa(s(T43), X64)

The set Q consists of the following terms:

fc15_in_gaa(x0)
U10_gaa(x0, x1)
U11_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