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

(0) Obligation:

Clauses:

map([], L) :- ','(!, eq(L, [])).
map(X, .(Y, Ys)) :- ','(head(X, H), ','(tail(X, T), ','(p(H, Y), map(T, Ys)))).
head([], X1).
head(.(H, X2), H).
tail([], []).
tail(.(X3, T), T).
p(X, Y).
eq(X, X).

Queries:

map(g,a).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: map(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
2 [label="2: map(T1, T2), SCOPE: 1, CLAUSE: 0 | map(T1, T2), SCOPE: 1, CLAUSE: 1 | ?_1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
3 [label="3: ','(!_1, eq(T4, [])) | map([], T2), SCOPE: 1, CLAUSE: 1 | ?_1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
4 [label="4: map(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nX5 is free; \nmap(T1, T2) !=? map([], X5)", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: eq(T4, [])\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: eq(T4, []), SCOPE: 2, CLAUSE: 7\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: \n\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(head(T6, X14), ','(tail(T6, X15), ','(p(X14, T9), map(X15, T10))))\n\nT6 is ground\nX5 is free; \nX14 is free; \nX15 is free; \nmap(T6, T2) !=? map([], X5)", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: \n\nX5 is free\nX11 is free; \nX12 is free; \nX13 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(head(T6, X14), ','(tail(T6, X15), ','(p(X14, T9), map(X15, T10)))), SCOPE: 3, CLAUSE: 2 | ','(head(T6, X14), ','(tail(T6, X15), ','(p(X14, T9), map(X15, T10)))), SCOPE: 3, CLAUSE: 3\n\nT6 is ground\nX5 is free; \nX14 is free; \nX15 is free; \nmap(T6, T2) !=? map([], X5)", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(head(T6, X14), ','(tail(T6, X15), ','(p(X14, T9), map(X15, T10)))), SCOPE: 3, CLAUSE: 3\n\nT6 is ground\nX5 is free; \nX14 is free; \nX15 is free; \nX17 is free; \nmap(T6, T2) !=? map([], X5)\nhead(T6, X14) !=? head([], X17)", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: ','(tail(.(T11, T12), X15), ','(p(T11, T9), map(X15, T10)))\n\nT11 is ground\nT12 is ground\nX5 is free; \nX14 is free; \nX15 is free; \nX17 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\nX5 is free\nX14 is free; \nX17 is free; \nX20 is free; \nX21 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(tail(.(T11, T12), X15), ','(p(T11, T9), map(X15, T10))), SCOPE: 4, CLAUSE: 4 | ','(tail(.(T11, T12), X15), ','(p(T11, T9), map(X15, T10))), SCOPE: 4, CLAUSE: 5\n\nT11 is ground\nT12 is ground\nX15 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(tail(.(T11, T12), X15), ','(p(T11, T9), map(X15, T10))), SCOPE: 4, CLAUSE: 5\n\nT11 is ground\nT12 is ground\nX15 is free; ", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(p(T13, T9), map(T14, T10))\n\nT13 is ground\nT14 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(p(T13, T9), map(T14, T10)), SCOPE: 5, CLAUSE: 6\n\nT13 is ground\nT14 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: map(T14, T17)\n\nT14 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 21 [arrowhead = none ];
21 -> 2;

22 [label="EVAL with clause\nmap([], X5) :- ','(!, eq(X5, [])).\nand substitution\nT1 -> []\nT2 -> T4\nX5 -> T4\nT3 -> T4", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 22 [arrowhead = none ];
22 -> 3;

23 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
2 -> 23 [arrowhead = none ];
23 -> 4;

24 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 24 [arrowhead = none ];
24 -> 5;

25 [label="EVAL with clause\nmap(X11, .(X12, X13)) :- ','(head(X11, X14), ','(tail(X11, X15), ','(p(X14, X12), map(X15, X13)))).\nand substitution\nT1 -> T6\nX11 -> T6\nX12 -> T9\nX13 -> T10\nT2 -> .(T9, T10)\nT7 -> T9\nT8 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 25 [arrowhead = none ];
25 -> 10;

26 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 26 [arrowhead = none ];
26 -> 11;

27 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
5 -> 27 [arrowhead = none ];
27 -> 6;

28 [label="EVAL with clause\neq(X7, X7).\nand substitution\nT4 -> []\nX7 -> []\nT5 -> []", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 28 [arrowhead = none ];
28 -> 7;

29 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 29 [arrowhead = none ];
29 -> 8;

30 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
7 -> 30 [arrowhead = none ];
30 -> 9;

31 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
10 -> 31 [arrowhead = none ];
31 -> 12;

32 [label="BACKTRACK\nfor clause: head([], X1)\nwith clash: (map(T6, T2), map([], X5))", fontsize=14, style = filled, fillcolor = white];
12 -> 32 [arrowhead = none ];
32 -> 13;

33 [label="EVAL with clause\nhead(.(X20, X21), X20).\nand substitution\nX20 -> T11\nX21 -> T12\nT6 -> .(T11, T12)\nX14 -> T11", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 33 [arrowhead = none ];
33 -> 14;

34 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 34 [arrowhead = none ];
34 -> 15;

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

36 [label="BACKTRACK\nfor clause: tail([], [])because of non-unification", fontsize=14, style = filled, fillcolor = white];
16 -> 36 [arrowhead = none ];
36 -> 17;

37 [label="EVAL with clause\ntail(.(X24, X25), X25).\nand substitution\nT11 -> T13\nX24 -> T13\nT12 -> T14\nX25 -> T14\nX15 -> T14", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 37 [arrowhead = none ];
37 -> 18;

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

39 [label="EVAL with clause\np(X28, X29).\nand substitution\nT13 -> T15\nX28 -> T15\nT9 -> T16\nX29 -> T16\nT10 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 39 [arrowhead = none ];
39 -> 20;

40 [label="INSTANCE with matching:\nT1 -> T14\nT2 -> T17", fontsize=14, style = filled, fillcolor = lightgrey];
20 -> 40 [arrowhead = none , style=dashed];
40 -> 1[style=dashed];

}

(2) Obligation:

Clauses:

map1([], []).
map1(.(T15, T14), .(T16, T17)) :- map1(T14, T17).

Queries:

map1(g,a).

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
map1_in: (b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

map1_in_ga([], []) → map1_out_ga([], [])
map1_in_ga(.(T15, T14), .(T16, T17)) → U1_ga(T15, T14, T16, T17, map1_in_ga(T14, T17))
U1_ga(T15, T14, T16, T17, map1_out_ga(T14, T17)) → map1_out_ga(.(T15, T14), .(T16, T17))

The argument filtering Pi contains the following mapping:
map1_in_ga(x1, x2)  =  map1_in_ga(x1)
[]  =  []
map1_out_ga(x1, x2)  =  map1_out_ga(x2)
.(x1, x2)  =  .(x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x5)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

map1_in_ga([], []) → map1_out_ga([], [])
map1_in_ga(.(T15, T14), .(T16, T17)) → U1_ga(T15, T14, T16, T17, map1_in_ga(T14, T17))
U1_ga(T15, T14, T16, T17, map1_out_ga(T14, T17)) → map1_out_ga(.(T15, T14), .(T16, T17))

The argument filtering Pi contains the following mapping:
map1_in_ga(x1, x2)  =  map1_in_ga(x1)
[]  =  []
map1_out_ga(x1, x2)  =  map1_out_ga(x2)
.(x1, x2)  =  .(x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x5)

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

MAP1_IN_GA(.(T15, T14), .(T16, T17)) → U1_GA(T15, T14, T16, T17, map1_in_ga(T14, T17))
MAP1_IN_GA(.(T15, T14), .(T16, T17)) → MAP1_IN_GA(T14, T17)

The TRS R consists of the following rules:

map1_in_ga([], []) → map1_out_ga([], [])
map1_in_ga(.(T15, T14), .(T16, T17)) → U1_ga(T15, T14, T16, T17, map1_in_ga(T14, T17))
U1_ga(T15, T14, T16, T17, map1_out_ga(T14, T17)) → map1_out_ga(.(T15, T14), .(T16, T17))

The argument filtering Pi contains the following mapping:
map1_in_ga(x1, x2)  =  map1_in_ga(x1)
[]  =  []
map1_out_ga(x1, x2)  =  map1_out_ga(x2)
.(x1, x2)  =  .(x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x5)
MAP1_IN_GA(x1, x2)  =  MAP1_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5)  =  U1_GA(x5)

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

(6) Obligation:

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

MAP1_IN_GA(.(T15, T14), .(T16, T17)) → U1_GA(T15, T14, T16, T17, map1_in_ga(T14, T17))
MAP1_IN_GA(.(T15, T14), .(T16, T17)) → MAP1_IN_GA(T14, T17)

The TRS R consists of the following rules:

map1_in_ga([], []) → map1_out_ga([], [])
map1_in_ga(.(T15, T14), .(T16, T17)) → U1_ga(T15, T14, T16, T17, map1_in_ga(T14, T17))
U1_ga(T15, T14, T16, T17, map1_out_ga(T14, T17)) → map1_out_ga(.(T15, T14), .(T16, T17))

The argument filtering Pi contains the following mapping:
map1_in_ga(x1, x2)  =  map1_in_ga(x1)
[]  =  []
map1_out_ga(x1, x2)  =  map1_out_ga(x2)
.(x1, x2)  =  .(x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x5)
MAP1_IN_GA(x1, x2)  =  MAP1_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5)  =  U1_GA(x5)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Obligation:

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

MAP1_IN_GA(.(T15, T14), .(T16, T17)) → MAP1_IN_GA(T14, T17)

The TRS R consists of the following rules:

map1_in_ga([], []) → map1_out_ga([], [])
map1_in_ga(.(T15, T14), .(T16, T17)) → U1_ga(T15, T14, T16, T17, map1_in_ga(T14, T17))
U1_ga(T15, T14, T16, T17, map1_out_ga(T14, T17)) → map1_out_ga(.(T15, T14), .(T16, T17))

The argument filtering Pi contains the following mapping:
map1_in_ga(x1, x2)  =  map1_in_ga(x1)
[]  =  []
map1_out_ga(x1, x2)  =  map1_out_ga(x2)
.(x1, x2)  =  .(x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x5)
MAP1_IN_GA(x1, x2)  =  MAP1_IN_GA(x1)

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

(9) UsableRulesProof (EQUIVALENT transformation)

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

(10) Obligation:

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

MAP1_IN_GA(.(T15, T14), .(T16, T17)) → MAP1_IN_GA(T14, T17)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
MAP1_IN_GA(x1, x2)  =  MAP1_IN_GA(x1)

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

(11) PiDPToQDPProof (SOUND transformation)

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

(12) Obligation:

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

MAP1_IN_GA(.(T14)) → MAP1_IN_GA(T14)

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

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

• MAP1_IN_GA(.(T14)) → MAP1_IN_GA(T14)
  The graph contains the following edges 1 > 1

(14) TRUE