YES Left Termination proof of ../tpdb/LP/BCGGV05/map_color.pl
Left Termination of the query pattern map_in_1(a) w.r.t. the given Prolog program could successfully be proven:



↳ Prolog
  ↳ PrologToPiTRSProof

Clauses:

color_map([], X).
color_map(.(Region, Regions), Colors) :- ','(color_region(Region, Colors), color_map(Regions, Colors)).
color_region(region(X, 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([], X).
subset(.(X, Xs), Ys) :- ','(member(X, Ys), subset(Xs, Ys)).
member(X, .(X, X1)).
member(X, .(X1, 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).

We use the technique of [30]. 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:

map_in_a(.(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, [])), [])))))))) → map_out_a(.(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, [])), []))))))))

The argument filtering Pi contains the following mapping:
map_in_a(x1)  =  map_in_a
map_out_a(x1)  =  map_out_a

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

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

map_in_a(.(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, [])), [])))))))) → map_out_a(.(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, [])), []))))))))

The argument filtering Pi contains the following mapping:
map_in_a(x1)  =  map_in_a
map_out_a(x1)  =  map_out_a


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

map_in_a(.(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, [])), [])))))))) → map_out_a(.(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, [])), []))))))))

The argument filtering Pi contains the following mapping:
map_in_a(x1)  =  map_in_a
map_out_a(x1)  =  map_out_a

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

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ PisEmptyProof

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

map_in_a(.(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, [])), [])))))))) → map_out_a(.(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, [])), []))))))))

The argument filtering Pi contains the following mapping:
map_in_a(x1)  =  map_in_a
map_out_a(x1)  =  map_out_a

We have to consider all (P,R,Pi)-chains
The TRS P is empty. Hence, there is no (P,R,Pi) chain.