(0) Obligation:

Clauses:

color_map([], X1).
color_map(.(Region, Regions), Colors) :- ','(color_region(Region, Colors), color_map(Regions, Colors)).
color_region(region(X2, Color, Neighbors), Colors) :- ','(select(Color, Colors, Colors1), subset(Neighbors, Colors1)).
select(X, .(X, Xs), Xs).
select(X, .(Y, Xs), .(Y, Zs)) :- select(X, Xs, Zs).
subset([], X3).
subset(.(X, Xs), Ys) :- ','(member(X, Ys), subset(Xs, Ys)).
member(X, .(X, X4)).
member(X, .(X5, Xs)) :- member(X, Xs).
map(.(region(belize, Belize, .(Guatemala, [])), .(region(guatemala, Guatemala, .(Belize, .(El_Salvador, .(Honduras, [])))), .(region(el_salvador, El_Salvador, .(Guatemala, .(Honduras, []))), .(region(honduras, Honduras, .(Guatemala, .(El_Salvador, .(Nicaragua, [])))), .(region(nicaragua, Nicaragua, .(Honduras, .(Costa_rica, []))), .(region(costa_rica, Costa_rica, .(Nicaragua, .(Panama, []))), .(region(panama, Panama, .(Costa_rica, [])), [])))))))).
query :- ','(map(X), color_map(X, .(red, .(blue, .(green, []))))).

Queries:

map(a).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

map1(.(region(belize, T9, .(T10, [])), .(region(guatemala, T10, .(T9, .(T11, .(T12, [])))), .(region(el_salvador, T11, .(T10, .(T12, []))), .(region(honduras, T12, .(T10, .(T11, .(T13, [])))), .(region(nicaragua, T13, .(T12, .(T14, []))), .(region(costa_rica, T14, .(T13, .(T15, []))), .(region(panama, T15, .(T14, [])), [])))))))).

Queries:

map1(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:
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

map1_in_a(.(region(belize, T9, .(T10, [])), .(region(guatemala, T10, .(T9, .(T11, .(T12, [])))), .(region(el_salvador, T11, .(T10, .(T12, []))), .(region(honduras, T12, .(T10, .(T11, .(T13, [])))), .(region(nicaragua, T13, .(T12, .(T14, []))), .(region(costa_rica, T14, .(T13, .(T15, []))), .(region(panama, T15, .(T14, [])), [])))))))) → map1_out_a(.(region(belize, T9, .(T10, [])), .(region(guatemala, T10, .(T9, .(T11, .(T12, [])))), .(region(el_salvador, T11, .(T10, .(T12, []))), .(region(honduras, T12, .(T10, .(T11, .(T13, [])))), .(region(nicaragua, T13, .(T12, .(T14, []))), .(region(costa_rica, T14, .(T13, .(T15, []))), .(region(panama, T15, .(T14, [])), []))))))))

The argument filtering Pi contains the following mapping:
map1_in_a(x1)  =  map1_in_a
map1_out_a(x1)  =  map1_out_a

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_a(.(region(belize, T9, .(T10, [])), .(region(guatemala, T10, .(T9, .(T11, .(T12, [])))), .(region(el_salvador, T11, .(T10, .(T12, []))), .(region(honduras, T12, .(T10, .(T11, .(T13, [])))), .(region(nicaragua, T13, .(T12, .(T14, []))), .(region(costa_rica, T14, .(T13, .(T15, []))), .(region(panama, T15, .(T14, [])), [])))))))) → map1_out_a(.(region(belize, T9, .(T10, [])), .(region(guatemala, T10, .(T9, .(T11, .(T12, [])))), .(region(el_salvador, T11, .(T10, .(T12, []))), .(region(honduras, T12, .(T10, .(T11, .(T13, [])))), .(region(nicaragua, T13, .(T12, .(T14, []))), .(region(costa_rica, T14, .(T13, .(T15, []))), .(region(panama, T15, .(T14, [])), []))))))))

The argument filtering Pi contains the following mapping:
map1_in_a(x1)  =  map1_in_a
map1_out_a(x1)  =  map1_out_a

(5) DependencyPairsProof (EQUIVALENT transformation)

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

map1_in_a(.(region(belize, T9, .(T10, [])), .(region(guatemala, T10, .(T9, .(T11, .(T12, [])))), .(region(el_salvador, T11, .(T10, .(T12, []))), .(region(honduras, T12, .(T10, .(T11, .(T13, [])))), .(region(nicaragua, T13, .(T12, .(T14, []))), .(region(costa_rica, T14, .(T13, .(T15, []))), .(region(panama, T15, .(T14, [])), [])))))))) → map1_out_a(.(region(belize, T9, .(T10, [])), .(region(guatemala, T10, .(T9, .(T11, .(T12, [])))), .(region(el_salvador, T11, .(T10, .(T12, []))), .(region(honduras, T12, .(T10, .(T11, .(T13, [])))), .(region(nicaragua, T13, .(T12, .(T14, []))), .(region(costa_rica, T14, .(T13, .(T15, []))), .(region(panama, T15, .(T14, [])), []))))))))

The argument filtering Pi contains the following mapping:
map1_in_a(x1)  =  map1_in_a
map1_out_a(x1)  =  map1_out_a

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

(6) Obligation:

Pi DP problem:
P is empty.
The TRS R consists of the following rules:

map1_in_a(.(region(belize, T9, .(T10, [])), .(region(guatemala, T10, .(T9, .(T11, .(T12, [])))), .(region(el_salvador, T11, .(T10, .(T12, []))), .(region(honduras, T12, .(T10, .(T11, .(T13, [])))), .(region(nicaragua, T13, .(T12, .(T14, []))), .(region(costa_rica, T14, .(T13, .(T15, []))), .(region(panama, T15, .(T14, [])), [])))))))) → map1_out_a(.(region(belize, T9, .(T10, [])), .(region(guatemala, T10, .(T9, .(T11, .(T12, [])))), .(region(el_salvador, T11, .(T10, .(T12, []))), .(region(honduras, T12, .(T10, .(T11, .(T13, [])))), .(region(nicaragua, T13, .(T12, .(T14, []))), .(region(costa_rica, T14, .(T13, .(T15, []))), .(region(panama, T15, .(T14, [])), []))))))))

The argument filtering Pi contains the following mapping:
map1_in_a(x1)  =  map1_in_a
map1_out_a(x1)  =  map1_out_a

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

(7) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,R,Pi) chain.

(8) YES