(0) Obligation:

Clauses:

f(RES, [], RES).
f([], .(Head, Tail), RES) :- f(.(Head, Tail), Tail, RES).
f(.(Head, Tail), Y, RES) :- f(Y, Tail, RES).

Query: f(g,g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

(2) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

fA_in_gga(T5, [], T5) → fA_out_gga(T5, [], T5)
fA_in_gga(.(T9, []), [], []) → fA_out_gga(.(T9, []), [], [])
fA_in_gga(.(T9, .(T25, T26)), [], T28) → U1_gga(T9, T25, T26, T28, fA_in_gga(.(T25, T26), T26, T28))
fA_in_gga([], .(T48, []), .(T48, [])) → fA_out_gga([], .(T48, []), .(T48, []))
fA_in_gga([], .(T68, []), []) → fA_out_gga([], .(T68, []), [])
fA_in_gga([], .(T68, .(T85, T86)), T88) → U2_gga(T68, T85, T86, T88, fA_in_gga(.(T85, T86), T86, T88))
fA_in_gga(.(T97, []), T106, T106) → fA_out_gga(.(T97, []), T106, T106)
fA_in_gga(.(T97, .(T119, T120)), [], T122) → U3_gga(T97, T119, T120, T122, fA_in_gga(.(T119, T120), T120, T122))
fA_in_gga(.(T97, T137), .(T135, T136), T139) → U4_gga(T97, T137, T135, T136, T139, fA_in_gga(T137, T136, T139))
U4_gga(T97, T137, T135, T136, T139, fA_out_gga(T137, T136, T139)) → fA_out_gga(.(T97, T137), .(T135, T136), T139)
U3_gga(T97, T119, T120, T122, fA_out_gga(.(T119, T120), T120, T122)) → fA_out_gga(.(T97, .(T119, T120)), [], T122)
U2_gga(T68, T85, T86, T88, fA_out_gga(.(T85, T86), T86, T88)) → fA_out_gga([], .(T68, .(T85, T86)), T88)
U1_gga(T9, T25, T26, T28, fA_out_gga(.(T25, T26), T26, T28)) → fA_out_gga(.(T9, .(T25, T26)), [], T28)

The argument filtering Pi contains the following mapping:
fA_in_gga(x1, x2, x3)  =  fA_in_gga(x1, x2)
[]  =  []
fA_out_gga(x1, x2, x3)  =  fA_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
U1_gga(x1, x2, x3, x4, x5)  =  U1_gga(x1, x2, x3, x5)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
U3_gga(x1, x2, x3, x4, x5)  =  U3_gga(x1, x2, x3, x5)
U4_gga(x1, x2, x3, x4, x5, x6)  =  U4_gga(x1, x2, x3, x4, x6)

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

FA_IN_GGA(.(T9, .(T25, T26)), [], T28) → U1_GGA(T9, T25, T26, T28, fA_in_gga(.(T25, T26), T26, T28))
FA_IN_GGA(.(T9, .(T25, T26)), [], T28) → FA_IN_GGA(.(T25, T26), T26, T28)
FA_IN_GGA([], .(T68, .(T85, T86)), T88) → U2_GGA(T68, T85, T86, T88, fA_in_gga(.(T85, T86), T86, T88))
FA_IN_GGA([], .(T68, .(T85, T86)), T88) → FA_IN_GGA(.(T85, T86), T86, T88)
FA_IN_GGA(.(T97, .(T119, T120)), [], T122) → U3_GGA(T97, T119, T120, T122, fA_in_gga(.(T119, T120), T120, T122))
FA_IN_GGA(.(T97, T137), .(T135, T136), T139) → U4_GGA(T97, T137, T135, T136, T139, fA_in_gga(T137, T136, T139))
FA_IN_GGA(.(T97, T137), .(T135, T136), T139) → FA_IN_GGA(T137, T136, T139)

The TRS R consists of the following rules:

fA_in_gga(T5, [], T5) → fA_out_gga(T5, [], T5)
fA_in_gga(.(T9, []), [], []) → fA_out_gga(.(T9, []), [], [])
fA_in_gga(.(T9, .(T25, T26)), [], T28) → U1_gga(T9, T25, T26, T28, fA_in_gga(.(T25, T26), T26, T28))
fA_in_gga([], .(T48, []), .(T48, [])) → fA_out_gga([], .(T48, []), .(T48, []))
fA_in_gga([], .(T68, []), []) → fA_out_gga([], .(T68, []), [])
fA_in_gga([], .(T68, .(T85, T86)), T88) → U2_gga(T68, T85, T86, T88, fA_in_gga(.(T85, T86), T86, T88))
fA_in_gga(.(T97, []), T106, T106) → fA_out_gga(.(T97, []), T106, T106)
fA_in_gga(.(T97, .(T119, T120)), [], T122) → U3_gga(T97, T119, T120, T122, fA_in_gga(.(T119, T120), T120, T122))
fA_in_gga(.(T97, T137), .(T135, T136), T139) → U4_gga(T97, T137, T135, T136, T139, fA_in_gga(T137, T136, T139))
U4_gga(T97, T137, T135, T136, T139, fA_out_gga(T137, T136, T139)) → fA_out_gga(.(T97, T137), .(T135, T136), T139)
U3_gga(T97, T119, T120, T122, fA_out_gga(.(T119, T120), T120, T122)) → fA_out_gga(.(T97, .(T119, T120)), [], T122)
U2_gga(T68, T85, T86, T88, fA_out_gga(.(T85, T86), T86, T88)) → fA_out_gga([], .(T68, .(T85, T86)), T88)
U1_gga(T9, T25, T26, T28, fA_out_gga(.(T25, T26), T26, T28)) → fA_out_gga(.(T9, .(T25, T26)), [], T28)

The argument filtering Pi contains the following mapping:
fA_in_gga(x1, x2, x3)  =  fA_in_gga(x1, x2)
[]  =  []
fA_out_gga(x1, x2, x3)  =  fA_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
U1_gga(x1, x2, x3, x4, x5)  =  U1_gga(x1, x2, x3, x5)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
U3_gga(x1, x2, x3, x4, x5)  =  U3_gga(x1, x2, x3, x5)
U4_gga(x1, x2, x3, x4, x5, x6)  =  U4_gga(x1, x2, x3, x4, x6)
FA_IN_GGA(x1, x2, x3)  =  FA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4, x5)  =  U1_GGA(x1, x2, x3, x5)
U2_GGA(x1, x2, x3, x4, x5)  =  U2_GGA(x1, x2, x3, x5)
U3_GGA(x1, x2, x3, x4, x5)  =  U3_GGA(x1, x2, x3, x5)
U4_GGA(x1, x2, x3, x4, x5, x6)  =  U4_GGA(x1, x2, x3, x4, x6)

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

(4) Obligation:

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

FA_IN_GGA(.(T9, .(T25, T26)), [], T28) → U1_GGA(T9, T25, T26, T28, fA_in_gga(.(T25, T26), T26, T28))
FA_IN_GGA(.(T9, .(T25, T26)), [], T28) → FA_IN_GGA(.(T25, T26), T26, T28)
FA_IN_GGA([], .(T68, .(T85, T86)), T88) → U2_GGA(T68, T85, T86, T88, fA_in_gga(.(T85, T86), T86, T88))
FA_IN_GGA([], .(T68, .(T85, T86)), T88) → FA_IN_GGA(.(T85, T86), T86, T88)
FA_IN_GGA(.(T97, .(T119, T120)), [], T122) → U3_GGA(T97, T119, T120, T122, fA_in_gga(.(T119, T120), T120, T122))
FA_IN_GGA(.(T97, T137), .(T135, T136), T139) → U4_GGA(T97, T137, T135, T136, T139, fA_in_gga(T137, T136, T139))
FA_IN_GGA(.(T97, T137), .(T135, T136), T139) → FA_IN_GGA(T137, T136, T139)

The TRS R consists of the following rules:

fA_in_gga(T5, [], T5) → fA_out_gga(T5, [], T5)
fA_in_gga(.(T9, []), [], []) → fA_out_gga(.(T9, []), [], [])
fA_in_gga(.(T9, .(T25, T26)), [], T28) → U1_gga(T9, T25, T26, T28, fA_in_gga(.(T25, T26), T26, T28))
fA_in_gga([], .(T48, []), .(T48, [])) → fA_out_gga([], .(T48, []), .(T48, []))
fA_in_gga([], .(T68, []), []) → fA_out_gga([], .(T68, []), [])
fA_in_gga([], .(T68, .(T85, T86)), T88) → U2_gga(T68, T85, T86, T88, fA_in_gga(.(T85, T86), T86, T88))
fA_in_gga(.(T97, []), T106, T106) → fA_out_gga(.(T97, []), T106, T106)
fA_in_gga(.(T97, .(T119, T120)), [], T122) → U3_gga(T97, T119, T120, T122, fA_in_gga(.(T119, T120), T120, T122))
fA_in_gga(.(T97, T137), .(T135, T136), T139) → U4_gga(T97, T137, T135, T136, T139, fA_in_gga(T137, T136, T139))
U4_gga(T97, T137, T135, T136, T139, fA_out_gga(T137, T136, T139)) → fA_out_gga(.(T97, T137), .(T135, T136), T139)
U3_gga(T97, T119, T120, T122, fA_out_gga(.(T119, T120), T120, T122)) → fA_out_gga(.(T97, .(T119, T120)), [], T122)
U2_gga(T68, T85, T86, T88, fA_out_gga(.(T85, T86), T86, T88)) → fA_out_gga([], .(T68, .(T85, T86)), T88)
U1_gga(T9, T25, T26, T28, fA_out_gga(.(T25, T26), T26, T28)) → fA_out_gga(.(T9, .(T25, T26)), [], T28)

The argument filtering Pi contains the following mapping:
fA_in_gga(x1, x2, x3)  =  fA_in_gga(x1, x2)
[]  =  []
fA_out_gga(x1, x2, x3)  =  fA_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
U1_gga(x1, x2, x3, x4, x5)  =  U1_gga(x1, x2, x3, x5)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
U3_gga(x1, x2, x3, x4, x5)  =  U3_gga(x1, x2, x3, x5)
U4_gga(x1, x2, x3, x4, x5, x6)  =  U4_gga(x1, x2, x3, x4, x6)
FA_IN_GGA(x1, x2, x3)  =  FA_IN_GGA(x1, x2)
U1_GGA(x1, x2, x3, x4, x5)  =  U1_GGA(x1, x2, x3, x5)
U2_GGA(x1, x2, x3, x4, x5)  =  U2_GGA(x1, x2, x3, x5)
U3_GGA(x1, x2, x3, x4, x5)  =  U3_GGA(x1, x2, x3, x5)
U4_GGA(x1, x2, x3, x4, x5, x6)  =  U4_GGA(x1, x2, x3, x4, x6)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 4 less nodes.

(6) Obligation:

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

FA_IN_GGA(.(T97, T137), .(T135, T136), T139) → FA_IN_GGA(T137, T136, T139)
FA_IN_GGA(.(T9, .(T25, T26)), [], T28) → FA_IN_GGA(.(T25, T26), T26, T28)
FA_IN_GGA([], .(T68, .(T85, T86)), T88) → FA_IN_GGA(.(T85, T86), T86, T88)

The TRS R consists of the following rules:

fA_in_gga(T5, [], T5) → fA_out_gga(T5, [], T5)
fA_in_gga(.(T9, []), [], []) → fA_out_gga(.(T9, []), [], [])
fA_in_gga(.(T9, .(T25, T26)), [], T28) → U1_gga(T9, T25, T26, T28, fA_in_gga(.(T25, T26), T26, T28))
fA_in_gga([], .(T48, []), .(T48, [])) → fA_out_gga([], .(T48, []), .(T48, []))
fA_in_gga([], .(T68, []), []) → fA_out_gga([], .(T68, []), [])
fA_in_gga([], .(T68, .(T85, T86)), T88) → U2_gga(T68, T85, T86, T88, fA_in_gga(.(T85, T86), T86, T88))
fA_in_gga(.(T97, []), T106, T106) → fA_out_gga(.(T97, []), T106, T106)
fA_in_gga(.(T97, .(T119, T120)), [], T122) → U3_gga(T97, T119, T120, T122, fA_in_gga(.(T119, T120), T120, T122))
fA_in_gga(.(T97, T137), .(T135, T136), T139) → U4_gga(T97, T137, T135, T136, T139, fA_in_gga(T137, T136, T139))
U4_gga(T97, T137, T135, T136, T139, fA_out_gga(T137, T136, T139)) → fA_out_gga(.(T97, T137), .(T135, T136), T139)
U3_gga(T97, T119, T120, T122, fA_out_gga(.(T119, T120), T120, T122)) → fA_out_gga(.(T97, .(T119, T120)), [], T122)
U2_gga(T68, T85, T86, T88, fA_out_gga(.(T85, T86), T86, T88)) → fA_out_gga([], .(T68, .(T85, T86)), T88)
U1_gga(T9, T25, T26, T28, fA_out_gga(.(T25, T26), T26, T28)) → fA_out_gga(.(T9, .(T25, T26)), [], T28)

The argument filtering Pi contains the following mapping:
fA_in_gga(x1, x2, x3)  =  fA_in_gga(x1, x2)
[]  =  []
fA_out_gga(x1, x2, x3)  =  fA_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
U1_gga(x1, x2, x3, x4, x5)  =  U1_gga(x1, x2, x3, x5)
U2_gga(x1, x2, x3, x4, x5)  =  U2_gga(x1, x2, x3, x5)
U3_gga(x1, x2, x3, x4, x5)  =  U3_gga(x1, x2, x3, x5)
U4_gga(x1, x2, x3, x4, x5, x6)  =  U4_gga(x1, x2, x3, x4, x6)
FA_IN_GGA(x1, x2, x3)  =  FA_IN_GGA(x1, x2)

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

(7) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(8) Obligation:

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

FA_IN_GGA(.(T97, T137), .(T135, T136), T139) → FA_IN_GGA(T137, T136, T139)
FA_IN_GGA(.(T9, .(T25, T26)), [], T28) → FA_IN_GGA(.(T25, T26), T26, T28)
FA_IN_GGA([], .(T68, .(T85, T86)), T88) → FA_IN_GGA(.(T85, T86), T86, T88)

R is empty.
The argument filtering Pi contains the following mapping:
[]  =  []
.(x1, x2)  =  .(x1, x2)
FA_IN_GGA(x1, x2, x3)  =  FA_IN_GGA(x1, x2)

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

(9) PiDPToQDPProof (SOUND transformation)

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

(10) Obligation:

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

FA_IN_GGA(.(T97, T137), .(T135, T136)) → FA_IN_GGA(T137, T136)
FA_IN_GGA(.(T9, .(T25, T26)), []) → FA_IN_GGA(.(T25, T26), T26)
FA_IN_GGA([], .(T68, .(T85, T86))) → FA_IN_GGA(.(T85, T86), T86)

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

(11) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • FA_IN_GGA(.(T97, T137), .(T135, T136)) → FA_IN_GGA(T137, T136)
    The graph contains the following edges 1 > 1, 2 > 2

  • FA_IN_GGA(.(T9, .(T25, T26)), []) → FA_IN_GGA(.(T25, T26), T26)
    The graph contains the following edges 1 > 1, 1 > 2

  • FA_IN_GGA([], .(T68, .(T85, T86))) → FA_IN_GGA(.(T85, T86), T86)
    The graph contains the following edges 2 > 1, 2 > 2

(12) YES