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

(0) Obligation:

Clauses:

list([]) :- !.
list(X) :- ','(tail(X, T), list(T)).
tail([], []).
tail(.(X, Xs), Xs).

Query: list(g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: list(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: list(T1), SCOPE: 1, CLAUSE: 0 | list(T1), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: !_1 | list([]), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: list(T1), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nlist(T1) !=? list([])", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(tail(T3, X3), list(X3))\n\nT3 is ground\nX3 is free\nlist(T3) !=? list([])", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(tail(T3, X3), list(X3)), SCOPE: 2, CLAUSE: 2 | ','(tail(T3, X3), list(X3)), SCOPE: 2, CLAUSE: 3\n\nT3 is ground\nX3 is free\nlist(T3) !=? list([])", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(tail(T3, X3), list(X3)), SCOPE: 2, CLAUSE: 3\n\nT3 is ground\nX3 is free\nlist(T3) !=? list([])", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: list(T9)\n\nT9 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 32 [arrowhead = none ];
32 -> 4;

33 [label="EVAL with clause\nlist([]) :- !_1.\nand substitutionT1 -> []", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 33 [arrowhead = none ];
33 -> 7;

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

35 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
7 -> 35 [arrowhead = none ];
35 -> 14;

36 [label="ONLY EVAL with clause\nlist(X2) :- ','(tail(X2, X3), list(X3)).\nand substitutionT1 -> T3,\nX2 -> T3", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 36 [arrowhead = none ];
36 -> 19;

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

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

39 [label="BACKTRACK\nfor clause: tail([], [])\nwith clash: (list(T3), list([]))", fontsize=14, style = filled, fillcolor = lightgreen];
22 -> 39 [arrowhead = none ];
39 -> 25;

40 [label="EVAL with clause\ntail(.(X8, X9), X9).\nand substitutionX8 -> T8,\nX9 -> T9,\nT3 -> .(T8, T9),\nX3 -> T9", fontsize=14, style = filled, fillcolor = lightblue];
25 -> 40 [arrowhead = none ];
40 -> 28;

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

42 [label="INSTANCE with matching:\nT1 -> T9", fontsize=14, style = filled, fillcolor = lightgrey];
28 -> 42 [arrowhead = none , style=dashed];
42 -> 1[style=dashed];

}

(2) Obligation:

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

listA_in_g([]) → listA_out_g([])
listA_in_g(.(T8, T9)) → U1_g(T8, T9, listA_in_g(T9))
U1_g(T8, T9, listA_out_g(T9)) → listA_out_g(.(T8, T9))

Pi is empty.

(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:

LISTA_IN_G(.(T8, T9)) → U1_G(T8, T9, listA_in_g(T9))
LISTA_IN_G(.(T8, T9)) → LISTA_IN_G(T9)

The TRS R consists of the following rules:

listA_in_g([]) → listA_out_g([])
listA_in_g(.(T8, T9)) → U1_g(T8, T9, listA_in_g(T9))
U1_g(T8, T9, listA_out_g(T9)) → listA_out_g(.(T8, T9))

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

(4) Obligation:

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

LISTA_IN_G(.(T8, T9)) → U1_G(T8, T9, listA_in_g(T9))
LISTA_IN_G(.(T8, T9)) → LISTA_IN_G(T9)

The TRS R consists of the following rules:

listA_in_g([]) → listA_out_g([])
listA_in_g(.(T8, T9)) → U1_g(T8, T9, listA_in_g(T9))
U1_g(T8, T9, listA_out_g(T9)) → listA_out_g(.(T8, T9))

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Obligation:

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

LISTA_IN_G(.(T8, T9)) → LISTA_IN_G(T9)

The TRS R consists of the following rules:

listA_in_g([]) → listA_out_g([])
listA_in_g(.(T8, T9)) → U1_g(T8, T9, listA_in_g(T9))
U1_g(T8, T9, listA_out_g(T9)) → listA_out_g(.(T8, T9))

Pi is empty.
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:

LISTA_IN_G(.(T8, T9)) → LISTA_IN_G(T9)

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

(9) PiDPToQDPProof (EQUIVALENT 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:

LISTA_IN_G(.(T8, T9)) → LISTA_IN_G(T9)

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:

• LISTA_IN_G(.(T8, T9)) → LISTA_IN_G(T9)
  The graph contains the following edges 1 > 1

(12) YES