(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