Left Termination of the query pattern map(f) w.r.t. the given Prolog program could successfully be proven:



↳ PROLOG
  ↳ UnrequestedClauseRemoverProof

colormap2({}0, underscore).
colormap2(.2(Region, Regions), Colors) :- colorregion2(Region, Colors), colormap2(Regions, Colors).
colorregion2(region3(underscore1, Color, Neighbors), Colors) :- select3(Color, Colors, Colors1), subset2(Neighbors, Colors1).
select3(X, .2(X, Xs), Xs).
select3(X, .2(Y, Xs), .2(Y, Zs)) :- select3(X, Xs, Zs).
subset2({}0, underscore2).
subset2(.2(X, Xs), Ys) :- member2(X, Ys), subset2(Xs, Ys).
member2(X, .2(X, underscore3)).
member2(X, .2(underscore4, Xs)) :- member2(X, Xs).
map1(.2(region3(belize0, Belize, .2(Guatemala, {}0)), .2(region3(guatemala0, Guatemala, .2(Belize, .2(ElSalvador, .2(Honduras, {}0)))), .2(region3(elsalvador0, ElSalvador, .2(Guatemala, .2(Honduras, {}0))), .2(region3(honduras0, Honduras, .2(Guatemala, .2(ElSalvador, .2(Nicaragua, {}0)))), .2(region3(nicaragua0, Nicaragua, .2(Honduras, .2(Costarica, {}0))), .2(region3(costarica0, Costarica, .2(Nicaragua, .2(Panama, {}0))), .2(region3(panama0, Panama, .2(Costarica, {}0)), {}0)))))))).
query0 :- map1(X), colormap2(X, .2(red0, .2(blue0, .2(green0, {}0)))).


The clauses

colormap2({}0, underscore).
colormap2(.2(Region, Regions), Colors) :- colorregion2(Region, Colors), colormap2(Regions, Colors).
colorregion2(region3(underscore1, Color, Neighbors), Colors) :- select3(Color, Colors, Colors1), subset2(Neighbors, Colors1).
select3(X, .2(X, Xs), Xs).
select3(X, .2(Y, Xs), .2(Y, Zs)) :- select3(X, Xs, Zs).
subset2({}0, underscore2).
subset2(.2(X, Xs), Ys) :- member2(X, Ys), subset2(Xs, Ys).
member2(X, .2(X, underscore3)).
member2(X, .2(underscore4, Xs)) :- member2(X, Xs).
query0 :- map1(X), colormap2(X, .2(red0, .2(blue0, .2(green0, {}0)))).

can be ignored, as they are not needed by any of the given querys.

Deleting these clauses results in the following prolog program:

map1(.2(region3(belize0, Belize, .2(Guatemala, {}0)), .2(region3(guatemala0, Guatemala, .2(Belize, .2(ElSalvador, .2(Honduras, {}0)))), .2(region3(elsalvador0, ElSalvador, .2(Guatemala, .2(Honduras, {}0))), .2(region3(honduras0, Honduras, .2(Guatemala, .2(ElSalvador, .2(Nicaragua, {}0)))), .2(region3(nicaragua0, Nicaragua, .2(Honduras, .2(Costarica, {}0))), .2(region3(costarica0, Costarica, .2(Nicaragua, .2(Panama, {}0))), .2(region3(panama0, Panama, .2(Costarica, {}0)), {}0)))))))).



↳ PROLOG
  ↳ UnrequestedClauseRemoverProof
    ↳ PROLOG
      ↳ PrologToPiTRSProof

map1(.2(region3(belize0, Belize, .2(Guatemala, {}0)), .2(region3(guatemala0, Guatemala, .2(Belize, .2(ElSalvador, .2(Honduras, {}0)))), .2(region3(elsalvador0, ElSalvador, .2(Guatemala, .2(Honduras, {}0))), .2(region3(honduras0, Honduras, .2(Guatemala, .2(ElSalvador, .2(Nicaragua, {}0)))), .2(region3(nicaragua0, Nicaragua, .2(Honduras, .2(Costarica, {}0))), .2(region3(costarica0, Costarica, .2(Nicaragua, .2(Panama, {}0))), .2(region3(panama0, Panama, .2(Costarica, {}0)), {}0)))))))).


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_1_in_a1(._22(region_33(belize_0, Belize, ._22(Guatemala, []_0)), ._22(region_33(guatemala_0, Guatemala, ._22(Belize, ._22(El_Salvador, ._22(Honduras, []_0)))), ._22(region_33(el_salvador_0, El_Salvador, ._22(Guatemala, ._22(Honduras, []_0))), ._22(region_33(honduras_0, Honduras, ._22(Guatemala, ._22(El_Salvador, ._22(Nicaragua, []_0)))), ._22(region_33(nicaragua_0, Nicaragua, ._22(Honduras, ._22(Costa_rica, []_0))), ._22(region_33(costa_rica_0, Costa_rica, ._22(Nicaragua, ._22(Panama, []_0))), ._22(region_33(panama_0, Panama, ._22(Costa_rica, []_0)), []_0)))))))) -> map_1_out_a1(._22(region_33(belize_0, Belize, ._22(Guatemala, []_0)), ._22(region_33(guatemala_0, Guatemala, ._22(Belize, ._22(El_Salvador, ._22(Honduras, []_0)))), ._22(region_33(el_salvador_0, El_Salvador, ._22(Guatemala, ._22(Honduras, []_0))), ._22(region_33(honduras_0, Honduras, ._22(Guatemala, ._22(El_Salvador, ._22(Nicaragua, []_0)))), ._22(region_33(nicaragua_0, Nicaragua, ._22(Honduras, ._22(Costa_rica, []_0))), ._22(region_33(costa_rica_0, Costa_rica, ._22(Nicaragua, ._22(Panama, []_0))), ._22(region_33(panama_0, Panama, ._22(Costa_rica, []_0)), []_0))))))))

The argument filtering Pi contains the following mapping:
map_1_in_a1(x1)  =  map_1_in_a
._22(x1, x2)  =  ._21(x2)
region_33(x1, x2, x3)  =  region_32(x1, x3)
belize_0  =  belize_0
[]_0  =  []_0
guatemala_0  =  guatemala_0
el_salvador_0  =  el_salvador_0
honduras_0  =  honduras_0
nicaragua_0  =  nicaragua_0
costa_rica_0  =  costa_rica_0
panama_0  =  panama_0
map_1_out_a1(x1)  =  map_1_out_a1(x1)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG



↳ PROLOG
  ↳ UnrequestedClauseRemoverProof
    ↳ PROLOG
      ↳ PrologToPiTRSProof
        ↳ PiTRS
          ↳ DependencyPairsProof

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

map_1_in_a1(._22(region_33(belize_0, Belize, ._22(Guatemala, []_0)), ._22(region_33(guatemala_0, Guatemala, ._22(Belize, ._22(El_Salvador, ._22(Honduras, []_0)))), ._22(region_33(el_salvador_0, El_Salvador, ._22(Guatemala, ._22(Honduras, []_0))), ._22(region_33(honduras_0, Honduras, ._22(Guatemala, ._22(El_Salvador, ._22(Nicaragua, []_0)))), ._22(region_33(nicaragua_0, Nicaragua, ._22(Honduras, ._22(Costa_rica, []_0))), ._22(region_33(costa_rica_0, Costa_rica, ._22(Nicaragua, ._22(Panama, []_0))), ._22(region_33(panama_0, Panama, ._22(Costa_rica, []_0)), []_0)))))))) -> map_1_out_a1(._22(region_33(belize_0, Belize, ._22(Guatemala, []_0)), ._22(region_33(guatemala_0, Guatemala, ._22(Belize, ._22(El_Salvador, ._22(Honduras, []_0)))), ._22(region_33(el_salvador_0, El_Salvador, ._22(Guatemala, ._22(Honduras, []_0))), ._22(region_33(honduras_0, Honduras, ._22(Guatemala, ._22(El_Salvador, ._22(Nicaragua, []_0)))), ._22(region_33(nicaragua_0, Nicaragua, ._22(Honduras, ._22(Costa_rica, []_0))), ._22(region_33(costa_rica_0, Costa_rica, ._22(Nicaragua, ._22(Panama, []_0))), ._22(region_33(panama_0, Panama, ._22(Costa_rica, []_0)), []_0))))))))

The argument filtering Pi contains the following mapping:
map_1_in_a1(x1)  =  map_1_in_a
._22(x1, x2)  =  ._21(x2)
region_33(x1, x2, x3)  =  region_32(x1, x3)
belize_0  =  belize_0
[]_0  =  []_0
guatemala_0  =  guatemala_0
el_salvador_0  =  el_salvador_0
honduras_0  =  honduras_0
nicaragua_0  =  nicaragua_0
costa_rica_0  =  costa_rica_0
panama_0  =  panama_0
map_1_out_a1(x1)  =  map_1_out_a1(x1)


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

map_1_in_a1(._22(region_33(belize_0, Belize, ._22(Guatemala, []_0)), ._22(region_33(guatemala_0, Guatemala, ._22(Belize, ._22(El_Salvador, ._22(Honduras, []_0)))), ._22(region_33(el_salvador_0, El_Salvador, ._22(Guatemala, ._22(Honduras, []_0))), ._22(region_33(honduras_0, Honduras, ._22(Guatemala, ._22(El_Salvador, ._22(Nicaragua, []_0)))), ._22(region_33(nicaragua_0, Nicaragua, ._22(Honduras, ._22(Costa_rica, []_0))), ._22(region_33(costa_rica_0, Costa_rica, ._22(Nicaragua, ._22(Panama, []_0))), ._22(region_33(panama_0, Panama, ._22(Costa_rica, []_0)), []_0)))))))) -> map_1_out_a1(._22(region_33(belize_0, Belize, ._22(Guatemala, []_0)), ._22(region_33(guatemala_0, Guatemala, ._22(Belize, ._22(El_Salvador, ._22(Honduras, []_0)))), ._22(region_33(el_salvador_0, El_Salvador, ._22(Guatemala, ._22(Honduras, []_0))), ._22(region_33(honduras_0, Honduras, ._22(Guatemala, ._22(El_Salvador, ._22(Nicaragua, []_0)))), ._22(region_33(nicaragua_0, Nicaragua, ._22(Honduras, ._22(Costa_rica, []_0))), ._22(region_33(costa_rica_0, Costa_rica, ._22(Nicaragua, ._22(Panama, []_0))), ._22(region_33(panama_0, Panama, ._22(Costa_rica, []_0)), []_0))))))))

The argument filtering Pi contains the following mapping:
map_1_in_a1(x1)  =  map_1_in_a
._22(x1, x2)  =  ._21(x2)
region_33(x1, x2, x3)  =  region_32(x1, x3)
belize_0  =  belize_0
[]_0  =  []_0
guatemala_0  =  guatemala_0
el_salvador_0  =  el_salvador_0
honduras_0  =  honduras_0
nicaragua_0  =  nicaragua_0
costa_rica_0  =  costa_rica_0
panama_0  =  panama_0
map_1_out_a1(x1)  =  map_1_out_a1(x1)

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

↳ PROLOG
  ↳ UnrequestedClauseRemoverProof
    ↳ PROLOG
      ↳ PrologToPiTRSProof
        ↳ PiTRS
          ↳ DependencyPairsProof
            ↳ PiDP
              ↳ PisEmptyProof

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

map_1_in_a1(._22(region_33(belize_0, Belize, ._22(Guatemala, []_0)), ._22(region_33(guatemala_0, Guatemala, ._22(Belize, ._22(El_Salvador, ._22(Honduras, []_0)))), ._22(region_33(el_salvador_0, El_Salvador, ._22(Guatemala, ._22(Honduras, []_0))), ._22(region_33(honduras_0, Honduras, ._22(Guatemala, ._22(El_Salvador, ._22(Nicaragua, []_0)))), ._22(region_33(nicaragua_0, Nicaragua, ._22(Honduras, ._22(Costa_rica, []_0))), ._22(region_33(costa_rica_0, Costa_rica, ._22(Nicaragua, ._22(Panama, []_0))), ._22(region_33(panama_0, Panama, ._22(Costa_rica, []_0)), []_0)))))))) -> map_1_out_a1(._22(region_33(belize_0, Belize, ._22(Guatemala, []_0)), ._22(region_33(guatemala_0, Guatemala, ._22(Belize, ._22(El_Salvador, ._22(Honduras, []_0)))), ._22(region_33(el_salvador_0, El_Salvador, ._22(Guatemala, ._22(Honduras, []_0))), ._22(region_33(honduras_0, Honduras, ._22(Guatemala, ._22(El_Salvador, ._22(Nicaragua, []_0)))), ._22(region_33(nicaragua_0, Nicaragua, ._22(Honduras, ._22(Costa_rica, []_0))), ._22(region_33(costa_rica_0, Costa_rica, ._22(Nicaragua, ._22(Panama, []_0))), ._22(region_33(panama_0, Panama, ._22(Costa_rica, []_0)), []_0))))))))

The argument filtering Pi contains the following mapping:
map_1_in_a1(x1)  =  map_1_in_a
._22(x1, x2)  =  ._21(x2)
region_33(x1, x2, x3)  =  region_32(x1, x3)
belize_0  =  belize_0
[]_0  =  []_0
guatemala_0  =  guatemala_0
el_salvador_0  =  el_salvador_0
honduras_0  =  honduras_0
nicaragua_0  =  nicaragua_0
costa_rica_0  =  costa_rica_0
panama_0  =  panama_0
map_1_out_a1(x1)  =  map_1_out_a1(x1)

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