(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) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:


Clauses:


Afs:

(3) TPisEmptyProof (EQUIVALENT transformation)

There are no more dependency triples. Hence, the dependency triple problem trivially terminates.

(4) YES