Left Termination of the query pattern color_map(f,b) w.r.t. the given Prolog program could not be shown:



PROLOG
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof

colormap2(.2(Region, Regions), Colors) :- colorregion2(Region, Colors), colormap2(Regions, Colors).
colormap2({}0, Colors).
colorregion2(region3(Name, Color, Neighbors), Colors) :- select3(Color, Colors, Colors1), members2(Neighbors, Colors1).
select3(X, .2(X, Xs), Xs).
select3(X, .2(Y, Ys), .2(Y, Zs)) :- select3(X, Ys, Zs).
members2(.2(X, Xs), Ys) :- member2(X, Ys), members2(Xs, Ys).
members2({}0, Ys).
member2(X, .2(X, underscore)).
member2(X, .2(underscore1, Xs)) :- member2(X, Xs).


With regard to the inferred argument filtering the predicates were used in the following modes:
color_map2: (f,b)
color_region2: (f,b)
select3: (f,b,f)
members2: (f,b)
member2: (f,b)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:


color_map_2_in_ag2(._22(Region, Regions), Colors) -> if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_in_ag2(Region, Colors))
color_region_2_in_ag2(region_33(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_in_aga3(Color, Colors, Colors1))
select_3_in_aga3(X, ._22(X, Xs), Xs) -> select_3_out_aga3(X, ._22(X, Xs), Xs)
select_3_in_aga3(X, ._22(Y, Ys), ._22(Y, Zs)) -> if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_in_aga3(X, Ys, Zs))
if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_out_aga3(X, Ys, Zs)) -> select_3_out_aga3(X, ._22(Y, Ys), ._22(Y, Zs))
if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag2(Neighbors, Colors1))
members_2_in_ag2(._22(X, Xs), Ys) -> if_members_2_in_1_ag4(X, Xs, Ys, member_2_in_ag2(X, Ys))
member_2_in_ag2(X, ._22(X, underscore)) -> member_2_out_ag2(X, ._22(X, underscore))
member_2_in_ag2(X, ._22(underscore1, Xs)) -> if_member_2_in_1_ag4(X, underscore1, Xs, member_2_in_ag2(X, Xs))
if_member_2_in_1_ag4(X, underscore1, Xs, member_2_out_ag2(X, Xs)) -> member_2_out_ag2(X, ._22(underscore1, Xs))
if_members_2_in_1_ag4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> if_members_2_in_2_ag4(X, Xs, Ys, members_2_in_ag2(Xs, Ys))
members_2_in_ag2([]_0, Ys) -> members_2_out_ag2([]_0, Ys)
if_members_2_in_2_ag4(X, Xs, Ys, members_2_out_ag2(Xs, Ys)) -> members_2_out_ag2(._22(X, Xs), Ys)
if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_33(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_in_ag2(Regions, Colors))
color_map_2_in_ag2([]_0, Colors) -> color_map_2_out_ag2([]_0, Colors)
if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_out_ag2(Regions, Colors)) -> color_map_2_out_ag2(._22(Region, Regions), Colors)

The argument filtering Pi contains the following mapping:
color_map_2_in_ag2(x1, x2)  =  color_map_2_in_ag1(x2)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
region_33(x1, x2, x3)  =  region_32(x2, x3)
if_color_map_2_in_1_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_1_ag2(x3, x4)
color_region_2_in_ag2(x1, x2)  =  color_region_2_in_ag1(x2)
if_color_region_2_in_1_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_1_ag1(x5)
select_3_in_aga3(x1, x2, x3)  =  select_3_in_aga1(x2)
select_3_out_aga3(x1, x2, x3)  =  select_3_out_aga2(x1, x3)
if_select_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_select_3_in_1_aga2(x2, x5)
if_color_region_2_in_2_ag6(x1, x2, x3, x4, x5, x6)  =  if_color_region_2_in_2_ag2(x2, x6)
members_2_in_ag2(x1, x2)  =  members_2_in_ag1(x2)
if_members_2_in_1_ag4(x1, x2, x3, x4)  =  if_members_2_in_1_ag2(x3, x4)
member_2_in_ag2(x1, x2)  =  member_2_in_ag1(x2)
member_2_out_ag2(x1, x2)  =  member_2_out_ag1(x1)
if_member_2_in_1_ag4(x1, x2, x3, x4)  =  if_member_2_in_1_ag1(x4)
if_members_2_in_2_ag4(x1, x2, x3, x4)  =  if_members_2_in_2_ag2(x1, x4)
members_2_out_ag2(x1, x2)  =  members_2_out_ag1(x1)
color_region_2_out_ag2(x1, x2)  =  color_region_2_out_ag1(x1)
if_color_map_2_in_2_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_2_ag2(x1, x4)
color_map_2_out_ag2(x1, x2)  =  color_map_2_out_ag1(x1)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG



↳ PROLOG
  ↳ PrologToPiTRSProof
PiTRS
      ↳ DependencyPairsProof
  ↳ PrologToPiTRSProof

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

color_map_2_in_ag2(._22(Region, Regions), Colors) -> if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_in_ag2(Region, Colors))
color_region_2_in_ag2(region_33(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_in_aga3(Color, Colors, Colors1))
select_3_in_aga3(X, ._22(X, Xs), Xs) -> select_3_out_aga3(X, ._22(X, Xs), Xs)
select_3_in_aga3(X, ._22(Y, Ys), ._22(Y, Zs)) -> if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_in_aga3(X, Ys, Zs))
if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_out_aga3(X, Ys, Zs)) -> select_3_out_aga3(X, ._22(Y, Ys), ._22(Y, Zs))
if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag2(Neighbors, Colors1))
members_2_in_ag2(._22(X, Xs), Ys) -> if_members_2_in_1_ag4(X, Xs, Ys, member_2_in_ag2(X, Ys))
member_2_in_ag2(X, ._22(X, underscore)) -> member_2_out_ag2(X, ._22(X, underscore))
member_2_in_ag2(X, ._22(underscore1, Xs)) -> if_member_2_in_1_ag4(X, underscore1, Xs, member_2_in_ag2(X, Xs))
if_member_2_in_1_ag4(X, underscore1, Xs, member_2_out_ag2(X, Xs)) -> member_2_out_ag2(X, ._22(underscore1, Xs))
if_members_2_in_1_ag4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> if_members_2_in_2_ag4(X, Xs, Ys, members_2_in_ag2(Xs, Ys))
members_2_in_ag2([]_0, Ys) -> members_2_out_ag2([]_0, Ys)
if_members_2_in_2_ag4(X, Xs, Ys, members_2_out_ag2(Xs, Ys)) -> members_2_out_ag2(._22(X, Xs), Ys)
if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_33(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_in_ag2(Regions, Colors))
color_map_2_in_ag2([]_0, Colors) -> color_map_2_out_ag2([]_0, Colors)
if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_out_ag2(Regions, Colors)) -> color_map_2_out_ag2(._22(Region, Regions), Colors)

The argument filtering Pi contains the following mapping:
color_map_2_in_ag2(x1, x2)  =  color_map_2_in_ag1(x2)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
region_33(x1, x2, x3)  =  region_32(x2, x3)
if_color_map_2_in_1_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_1_ag2(x3, x4)
color_region_2_in_ag2(x1, x2)  =  color_region_2_in_ag1(x2)
if_color_region_2_in_1_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_1_ag1(x5)
select_3_in_aga3(x1, x2, x3)  =  select_3_in_aga1(x2)
select_3_out_aga3(x1, x2, x3)  =  select_3_out_aga2(x1, x3)
if_select_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_select_3_in_1_aga2(x2, x5)
if_color_region_2_in_2_ag6(x1, x2, x3, x4, x5, x6)  =  if_color_region_2_in_2_ag2(x2, x6)
members_2_in_ag2(x1, x2)  =  members_2_in_ag1(x2)
if_members_2_in_1_ag4(x1, x2, x3, x4)  =  if_members_2_in_1_ag2(x3, x4)
member_2_in_ag2(x1, x2)  =  member_2_in_ag1(x2)
member_2_out_ag2(x1, x2)  =  member_2_out_ag1(x1)
if_member_2_in_1_ag4(x1, x2, x3, x4)  =  if_member_2_in_1_ag1(x4)
if_members_2_in_2_ag4(x1, x2, x3, x4)  =  if_members_2_in_2_ag2(x1, x4)
members_2_out_ag2(x1, x2)  =  members_2_out_ag1(x1)
color_region_2_out_ag2(x1, x2)  =  color_region_2_out_ag1(x1)
if_color_map_2_in_2_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_2_ag2(x1, x4)
color_map_2_out_ag2(x1, x2)  =  color_map_2_out_ag1(x1)


Pi DP problem:
The TRS P consists of the following rules:

COLOR_MAP_2_IN_AG2(._22(Region, Regions), Colors) -> IF_COLOR_MAP_2_IN_1_AG4(Region, Regions, Colors, color_region_2_in_ag2(Region, Colors))
COLOR_MAP_2_IN_AG2(._22(Region, Regions), Colors) -> COLOR_REGION_2_IN_AG2(Region, Colors)
COLOR_REGION_2_IN_AG2(region_33(Name, Color, Neighbors), Colors) -> IF_COLOR_REGION_2_IN_1_AG5(Name, Color, Neighbors, Colors, select_3_in_aga3(Color, Colors, Colors1))
COLOR_REGION_2_IN_AG2(region_33(Name, Color, Neighbors), Colors) -> SELECT_3_IN_AGA3(Color, Colors, Colors1)
SELECT_3_IN_AGA3(X, ._22(Y, Ys), ._22(Y, Zs)) -> IF_SELECT_3_IN_1_AGA5(X, Y, Ys, Zs, select_3_in_aga3(X, Ys, Zs))
SELECT_3_IN_AGA3(X, ._22(Y, Ys), ._22(Y, Zs)) -> SELECT_3_IN_AGA3(X, Ys, Zs)
IF_COLOR_REGION_2_IN_1_AG5(Name, Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> IF_COLOR_REGION_2_IN_2_AG6(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag2(Neighbors, Colors1))
IF_COLOR_REGION_2_IN_1_AG5(Name, Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> MEMBERS_2_IN_AG2(Neighbors, Colors1)
MEMBERS_2_IN_AG2(._22(X, Xs), Ys) -> IF_MEMBERS_2_IN_1_AG4(X, Xs, Ys, member_2_in_ag2(X, Ys))
MEMBERS_2_IN_AG2(._22(X, Xs), Ys) -> MEMBER_2_IN_AG2(X, Ys)
MEMBER_2_IN_AG2(X, ._22(underscore1, Xs)) -> IF_MEMBER_2_IN_1_AG4(X, underscore1, Xs, member_2_in_ag2(X, Xs))
MEMBER_2_IN_AG2(X, ._22(underscore1, Xs)) -> MEMBER_2_IN_AG2(X, Xs)
IF_MEMBERS_2_IN_1_AG4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> IF_MEMBERS_2_IN_2_AG4(X, Xs, Ys, members_2_in_ag2(Xs, Ys))
IF_MEMBERS_2_IN_1_AG4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> MEMBERS_2_IN_AG2(Xs, Ys)
IF_COLOR_MAP_2_IN_1_AG4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> IF_COLOR_MAP_2_IN_2_AG4(Region, Regions, Colors, color_map_2_in_ag2(Regions, Colors))
IF_COLOR_MAP_2_IN_1_AG4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> COLOR_MAP_2_IN_AG2(Regions, Colors)

The TRS R consists of the following rules:

color_map_2_in_ag2(._22(Region, Regions), Colors) -> if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_in_ag2(Region, Colors))
color_region_2_in_ag2(region_33(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_in_aga3(Color, Colors, Colors1))
select_3_in_aga3(X, ._22(X, Xs), Xs) -> select_3_out_aga3(X, ._22(X, Xs), Xs)
select_3_in_aga3(X, ._22(Y, Ys), ._22(Y, Zs)) -> if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_in_aga3(X, Ys, Zs))
if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_out_aga3(X, Ys, Zs)) -> select_3_out_aga3(X, ._22(Y, Ys), ._22(Y, Zs))
if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag2(Neighbors, Colors1))
members_2_in_ag2(._22(X, Xs), Ys) -> if_members_2_in_1_ag4(X, Xs, Ys, member_2_in_ag2(X, Ys))
member_2_in_ag2(X, ._22(X, underscore)) -> member_2_out_ag2(X, ._22(X, underscore))
member_2_in_ag2(X, ._22(underscore1, Xs)) -> if_member_2_in_1_ag4(X, underscore1, Xs, member_2_in_ag2(X, Xs))
if_member_2_in_1_ag4(X, underscore1, Xs, member_2_out_ag2(X, Xs)) -> member_2_out_ag2(X, ._22(underscore1, Xs))
if_members_2_in_1_ag4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> if_members_2_in_2_ag4(X, Xs, Ys, members_2_in_ag2(Xs, Ys))
members_2_in_ag2([]_0, Ys) -> members_2_out_ag2([]_0, Ys)
if_members_2_in_2_ag4(X, Xs, Ys, members_2_out_ag2(Xs, Ys)) -> members_2_out_ag2(._22(X, Xs), Ys)
if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_33(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_in_ag2(Regions, Colors))
color_map_2_in_ag2([]_0, Colors) -> color_map_2_out_ag2([]_0, Colors)
if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_out_ag2(Regions, Colors)) -> color_map_2_out_ag2(._22(Region, Regions), Colors)

The argument filtering Pi contains the following mapping:
color_map_2_in_ag2(x1, x2)  =  color_map_2_in_ag1(x2)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
region_33(x1, x2, x3)  =  region_32(x2, x3)
if_color_map_2_in_1_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_1_ag2(x3, x4)
color_region_2_in_ag2(x1, x2)  =  color_region_2_in_ag1(x2)
if_color_region_2_in_1_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_1_ag1(x5)
select_3_in_aga3(x1, x2, x3)  =  select_3_in_aga1(x2)
select_3_out_aga3(x1, x2, x3)  =  select_3_out_aga2(x1, x3)
if_select_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_select_3_in_1_aga2(x2, x5)
if_color_region_2_in_2_ag6(x1, x2, x3, x4, x5, x6)  =  if_color_region_2_in_2_ag2(x2, x6)
members_2_in_ag2(x1, x2)  =  members_2_in_ag1(x2)
if_members_2_in_1_ag4(x1, x2, x3, x4)  =  if_members_2_in_1_ag2(x3, x4)
member_2_in_ag2(x1, x2)  =  member_2_in_ag1(x2)
member_2_out_ag2(x1, x2)  =  member_2_out_ag1(x1)
if_member_2_in_1_ag4(x1, x2, x3, x4)  =  if_member_2_in_1_ag1(x4)
if_members_2_in_2_ag4(x1, x2, x3, x4)  =  if_members_2_in_2_ag2(x1, x4)
members_2_out_ag2(x1, x2)  =  members_2_out_ag1(x1)
color_region_2_out_ag2(x1, x2)  =  color_region_2_out_ag1(x1)
if_color_map_2_in_2_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_2_ag2(x1, x4)
color_map_2_out_ag2(x1, x2)  =  color_map_2_out_ag1(x1)
IF_COLOR_REGION_2_IN_2_AG6(x1, x2, x3, x4, x5, x6)  =  IF_COLOR_REGION_2_IN_2_AG2(x2, x6)
IF_MEMBERS_2_IN_1_AG4(x1, x2, x3, x4)  =  IF_MEMBERS_2_IN_1_AG2(x3, x4)
IF_MEMBERS_2_IN_2_AG4(x1, x2, x3, x4)  =  IF_MEMBERS_2_IN_2_AG2(x1, x4)
COLOR_MAP_2_IN_AG2(x1, x2)  =  COLOR_MAP_2_IN_AG1(x2)
MEMBERS_2_IN_AG2(x1, x2)  =  MEMBERS_2_IN_AG1(x2)
IF_COLOR_MAP_2_IN_1_AG4(x1, x2, x3, x4)  =  IF_COLOR_MAP_2_IN_1_AG2(x3, x4)
MEMBER_2_IN_AG2(x1, x2)  =  MEMBER_2_IN_AG1(x2)
IF_SELECT_3_IN_1_AGA5(x1, x2, x3, x4, x5)  =  IF_SELECT_3_IN_1_AGA2(x2, x5)
IF_COLOR_MAP_2_IN_2_AG4(x1, x2, x3, x4)  =  IF_COLOR_MAP_2_IN_2_AG2(x1, x4)
COLOR_REGION_2_IN_AG2(x1, x2)  =  COLOR_REGION_2_IN_AG1(x2)
IF_MEMBER_2_IN_1_AG4(x1, x2, x3, x4)  =  IF_MEMBER_2_IN_1_AG1(x4)
IF_COLOR_REGION_2_IN_1_AG5(x1, x2, x3, x4, x5)  =  IF_COLOR_REGION_2_IN_1_AG1(x5)
SELECT_3_IN_AGA3(x1, x2, x3)  =  SELECT_3_IN_AGA1(x2)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
PiDP
          ↳ DependencyGraphProof
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

COLOR_MAP_2_IN_AG2(._22(Region, Regions), Colors) -> IF_COLOR_MAP_2_IN_1_AG4(Region, Regions, Colors, color_region_2_in_ag2(Region, Colors))
COLOR_MAP_2_IN_AG2(._22(Region, Regions), Colors) -> COLOR_REGION_2_IN_AG2(Region, Colors)
COLOR_REGION_2_IN_AG2(region_33(Name, Color, Neighbors), Colors) -> IF_COLOR_REGION_2_IN_1_AG5(Name, Color, Neighbors, Colors, select_3_in_aga3(Color, Colors, Colors1))
COLOR_REGION_2_IN_AG2(region_33(Name, Color, Neighbors), Colors) -> SELECT_3_IN_AGA3(Color, Colors, Colors1)
SELECT_3_IN_AGA3(X, ._22(Y, Ys), ._22(Y, Zs)) -> IF_SELECT_3_IN_1_AGA5(X, Y, Ys, Zs, select_3_in_aga3(X, Ys, Zs))
SELECT_3_IN_AGA3(X, ._22(Y, Ys), ._22(Y, Zs)) -> SELECT_3_IN_AGA3(X, Ys, Zs)
IF_COLOR_REGION_2_IN_1_AG5(Name, Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> IF_COLOR_REGION_2_IN_2_AG6(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag2(Neighbors, Colors1))
IF_COLOR_REGION_2_IN_1_AG5(Name, Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> MEMBERS_2_IN_AG2(Neighbors, Colors1)
MEMBERS_2_IN_AG2(._22(X, Xs), Ys) -> IF_MEMBERS_2_IN_1_AG4(X, Xs, Ys, member_2_in_ag2(X, Ys))
MEMBERS_2_IN_AG2(._22(X, Xs), Ys) -> MEMBER_2_IN_AG2(X, Ys)
MEMBER_2_IN_AG2(X, ._22(underscore1, Xs)) -> IF_MEMBER_2_IN_1_AG4(X, underscore1, Xs, member_2_in_ag2(X, Xs))
MEMBER_2_IN_AG2(X, ._22(underscore1, Xs)) -> MEMBER_2_IN_AG2(X, Xs)
IF_MEMBERS_2_IN_1_AG4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> IF_MEMBERS_2_IN_2_AG4(X, Xs, Ys, members_2_in_ag2(Xs, Ys))
IF_MEMBERS_2_IN_1_AG4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> MEMBERS_2_IN_AG2(Xs, Ys)
IF_COLOR_MAP_2_IN_1_AG4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> IF_COLOR_MAP_2_IN_2_AG4(Region, Regions, Colors, color_map_2_in_ag2(Regions, Colors))
IF_COLOR_MAP_2_IN_1_AG4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> COLOR_MAP_2_IN_AG2(Regions, Colors)

The TRS R consists of the following rules:

color_map_2_in_ag2(._22(Region, Regions), Colors) -> if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_in_ag2(Region, Colors))
color_region_2_in_ag2(region_33(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_in_aga3(Color, Colors, Colors1))
select_3_in_aga3(X, ._22(X, Xs), Xs) -> select_3_out_aga3(X, ._22(X, Xs), Xs)
select_3_in_aga3(X, ._22(Y, Ys), ._22(Y, Zs)) -> if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_in_aga3(X, Ys, Zs))
if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_out_aga3(X, Ys, Zs)) -> select_3_out_aga3(X, ._22(Y, Ys), ._22(Y, Zs))
if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag2(Neighbors, Colors1))
members_2_in_ag2(._22(X, Xs), Ys) -> if_members_2_in_1_ag4(X, Xs, Ys, member_2_in_ag2(X, Ys))
member_2_in_ag2(X, ._22(X, underscore)) -> member_2_out_ag2(X, ._22(X, underscore))
member_2_in_ag2(X, ._22(underscore1, Xs)) -> if_member_2_in_1_ag4(X, underscore1, Xs, member_2_in_ag2(X, Xs))
if_member_2_in_1_ag4(X, underscore1, Xs, member_2_out_ag2(X, Xs)) -> member_2_out_ag2(X, ._22(underscore1, Xs))
if_members_2_in_1_ag4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> if_members_2_in_2_ag4(X, Xs, Ys, members_2_in_ag2(Xs, Ys))
members_2_in_ag2([]_0, Ys) -> members_2_out_ag2([]_0, Ys)
if_members_2_in_2_ag4(X, Xs, Ys, members_2_out_ag2(Xs, Ys)) -> members_2_out_ag2(._22(X, Xs), Ys)
if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_33(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_in_ag2(Regions, Colors))
color_map_2_in_ag2([]_0, Colors) -> color_map_2_out_ag2([]_0, Colors)
if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_out_ag2(Regions, Colors)) -> color_map_2_out_ag2(._22(Region, Regions), Colors)

The argument filtering Pi contains the following mapping:
color_map_2_in_ag2(x1, x2)  =  color_map_2_in_ag1(x2)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
region_33(x1, x2, x3)  =  region_32(x2, x3)
if_color_map_2_in_1_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_1_ag2(x3, x4)
color_region_2_in_ag2(x1, x2)  =  color_region_2_in_ag1(x2)
if_color_region_2_in_1_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_1_ag1(x5)
select_3_in_aga3(x1, x2, x3)  =  select_3_in_aga1(x2)
select_3_out_aga3(x1, x2, x3)  =  select_3_out_aga2(x1, x3)
if_select_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_select_3_in_1_aga2(x2, x5)
if_color_region_2_in_2_ag6(x1, x2, x3, x4, x5, x6)  =  if_color_region_2_in_2_ag2(x2, x6)
members_2_in_ag2(x1, x2)  =  members_2_in_ag1(x2)
if_members_2_in_1_ag4(x1, x2, x3, x4)  =  if_members_2_in_1_ag2(x3, x4)
member_2_in_ag2(x1, x2)  =  member_2_in_ag1(x2)
member_2_out_ag2(x1, x2)  =  member_2_out_ag1(x1)
if_member_2_in_1_ag4(x1, x2, x3, x4)  =  if_member_2_in_1_ag1(x4)
if_members_2_in_2_ag4(x1, x2, x3, x4)  =  if_members_2_in_2_ag2(x1, x4)
members_2_out_ag2(x1, x2)  =  members_2_out_ag1(x1)
color_region_2_out_ag2(x1, x2)  =  color_region_2_out_ag1(x1)
if_color_map_2_in_2_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_2_ag2(x1, x4)
color_map_2_out_ag2(x1, x2)  =  color_map_2_out_ag1(x1)
IF_COLOR_REGION_2_IN_2_AG6(x1, x2, x3, x4, x5, x6)  =  IF_COLOR_REGION_2_IN_2_AG2(x2, x6)
IF_MEMBERS_2_IN_1_AG4(x1, x2, x3, x4)  =  IF_MEMBERS_2_IN_1_AG2(x3, x4)
IF_MEMBERS_2_IN_2_AG4(x1, x2, x3, x4)  =  IF_MEMBERS_2_IN_2_AG2(x1, x4)
COLOR_MAP_2_IN_AG2(x1, x2)  =  COLOR_MAP_2_IN_AG1(x2)
MEMBERS_2_IN_AG2(x1, x2)  =  MEMBERS_2_IN_AG1(x2)
IF_COLOR_MAP_2_IN_1_AG4(x1, x2, x3, x4)  =  IF_COLOR_MAP_2_IN_1_AG2(x3, x4)
MEMBER_2_IN_AG2(x1, x2)  =  MEMBER_2_IN_AG1(x2)
IF_SELECT_3_IN_1_AGA5(x1, x2, x3, x4, x5)  =  IF_SELECT_3_IN_1_AGA2(x2, x5)
IF_COLOR_MAP_2_IN_2_AG4(x1, x2, x3, x4)  =  IF_COLOR_MAP_2_IN_2_AG2(x1, x4)
COLOR_REGION_2_IN_AG2(x1, x2)  =  COLOR_REGION_2_IN_AG1(x2)
IF_MEMBER_2_IN_1_AG4(x1, x2, x3, x4)  =  IF_MEMBER_2_IN_1_AG1(x4)
IF_COLOR_REGION_2_IN_1_AG5(x1, x2, x3, x4, x5)  =  IF_COLOR_REGION_2_IN_1_AG1(x5)
SELECT_3_IN_AGA3(x1, x2, x3)  =  SELECT_3_IN_AGA1(x2)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph contains 4 SCCs with 10 less nodes.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_2_IN_AG2(X, ._22(underscore1, Xs)) -> MEMBER_2_IN_AG2(X, Xs)

The TRS R consists of the following rules:

color_map_2_in_ag2(._22(Region, Regions), Colors) -> if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_in_ag2(Region, Colors))
color_region_2_in_ag2(region_33(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_in_aga3(Color, Colors, Colors1))
select_3_in_aga3(X, ._22(X, Xs), Xs) -> select_3_out_aga3(X, ._22(X, Xs), Xs)
select_3_in_aga3(X, ._22(Y, Ys), ._22(Y, Zs)) -> if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_in_aga3(X, Ys, Zs))
if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_out_aga3(X, Ys, Zs)) -> select_3_out_aga3(X, ._22(Y, Ys), ._22(Y, Zs))
if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag2(Neighbors, Colors1))
members_2_in_ag2(._22(X, Xs), Ys) -> if_members_2_in_1_ag4(X, Xs, Ys, member_2_in_ag2(X, Ys))
member_2_in_ag2(X, ._22(X, underscore)) -> member_2_out_ag2(X, ._22(X, underscore))
member_2_in_ag2(X, ._22(underscore1, Xs)) -> if_member_2_in_1_ag4(X, underscore1, Xs, member_2_in_ag2(X, Xs))
if_member_2_in_1_ag4(X, underscore1, Xs, member_2_out_ag2(X, Xs)) -> member_2_out_ag2(X, ._22(underscore1, Xs))
if_members_2_in_1_ag4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> if_members_2_in_2_ag4(X, Xs, Ys, members_2_in_ag2(Xs, Ys))
members_2_in_ag2([]_0, Ys) -> members_2_out_ag2([]_0, Ys)
if_members_2_in_2_ag4(X, Xs, Ys, members_2_out_ag2(Xs, Ys)) -> members_2_out_ag2(._22(X, Xs), Ys)
if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_33(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_in_ag2(Regions, Colors))
color_map_2_in_ag2([]_0, Colors) -> color_map_2_out_ag2([]_0, Colors)
if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_out_ag2(Regions, Colors)) -> color_map_2_out_ag2(._22(Region, Regions), Colors)

The argument filtering Pi contains the following mapping:
color_map_2_in_ag2(x1, x2)  =  color_map_2_in_ag1(x2)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
region_33(x1, x2, x3)  =  region_32(x2, x3)
if_color_map_2_in_1_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_1_ag2(x3, x4)
color_region_2_in_ag2(x1, x2)  =  color_region_2_in_ag1(x2)
if_color_region_2_in_1_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_1_ag1(x5)
select_3_in_aga3(x1, x2, x3)  =  select_3_in_aga1(x2)
select_3_out_aga3(x1, x2, x3)  =  select_3_out_aga2(x1, x3)
if_select_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_select_3_in_1_aga2(x2, x5)
if_color_region_2_in_2_ag6(x1, x2, x3, x4, x5, x6)  =  if_color_region_2_in_2_ag2(x2, x6)
members_2_in_ag2(x1, x2)  =  members_2_in_ag1(x2)
if_members_2_in_1_ag4(x1, x2, x3, x4)  =  if_members_2_in_1_ag2(x3, x4)
member_2_in_ag2(x1, x2)  =  member_2_in_ag1(x2)
member_2_out_ag2(x1, x2)  =  member_2_out_ag1(x1)
if_member_2_in_1_ag4(x1, x2, x3, x4)  =  if_member_2_in_1_ag1(x4)
if_members_2_in_2_ag4(x1, x2, x3, x4)  =  if_members_2_in_2_ag2(x1, x4)
members_2_out_ag2(x1, x2)  =  members_2_out_ag1(x1)
color_region_2_out_ag2(x1, x2)  =  color_region_2_out_ag1(x1)
if_color_map_2_in_2_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_2_ag2(x1, x4)
color_map_2_out_ag2(x1, x2)  =  color_map_2_out_ag1(x1)
MEMBER_2_IN_AG2(x1, x2)  =  MEMBER_2_IN_AG1(x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_2_IN_AG2(X, ._22(underscore1, Xs)) -> MEMBER_2_IN_AG2(X, Xs)

R is empty.
The argument filtering Pi contains the following mapping:
._22(x1, x2)  =  ._22(x1, x2)
MEMBER_2_IN_AG2(x1, x2)  =  MEMBER_2_IN_AG1(x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

MEMBER_2_IN_AG1(._22(underscore1, Xs)) -> MEMBER_2_IN_AG1(Xs)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {MEMBER_2_IN_AG1}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

MEMBERS_2_IN_AG2(._22(X, Xs), Ys) -> IF_MEMBERS_2_IN_1_AG4(X, Xs, Ys, member_2_in_ag2(X, Ys))
IF_MEMBERS_2_IN_1_AG4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> MEMBERS_2_IN_AG2(Xs, Ys)

The TRS R consists of the following rules:

color_map_2_in_ag2(._22(Region, Regions), Colors) -> if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_in_ag2(Region, Colors))
color_region_2_in_ag2(region_33(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_in_aga3(Color, Colors, Colors1))
select_3_in_aga3(X, ._22(X, Xs), Xs) -> select_3_out_aga3(X, ._22(X, Xs), Xs)
select_3_in_aga3(X, ._22(Y, Ys), ._22(Y, Zs)) -> if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_in_aga3(X, Ys, Zs))
if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_out_aga3(X, Ys, Zs)) -> select_3_out_aga3(X, ._22(Y, Ys), ._22(Y, Zs))
if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag2(Neighbors, Colors1))
members_2_in_ag2(._22(X, Xs), Ys) -> if_members_2_in_1_ag4(X, Xs, Ys, member_2_in_ag2(X, Ys))
member_2_in_ag2(X, ._22(X, underscore)) -> member_2_out_ag2(X, ._22(X, underscore))
member_2_in_ag2(X, ._22(underscore1, Xs)) -> if_member_2_in_1_ag4(X, underscore1, Xs, member_2_in_ag2(X, Xs))
if_member_2_in_1_ag4(X, underscore1, Xs, member_2_out_ag2(X, Xs)) -> member_2_out_ag2(X, ._22(underscore1, Xs))
if_members_2_in_1_ag4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> if_members_2_in_2_ag4(X, Xs, Ys, members_2_in_ag2(Xs, Ys))
members_2_in_ag2([]_0, Ys) -> members_2_out_ag2([]_0, Ys)
if_members_2_in_2_ag4(X, Xs, Ys, members_2_out_ag2(Xs, Ys)) -> members_2_out_ag2(._22(X, Xs), Ys)
if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_33(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_in_ag2(Regions, Colors))
color_map_2_in_ag2([]_0, Colors) -> color_map_2_out_ag2([]_0, Colors)
if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_out_ag2(Regions, Colors)) -> color_map_2_out_ag2(._22(Region, Regions), Colors)

The argument filtering Pi contains the following mapping:
color_map_2_in_ag2(x1, x2)  =  color_map_2_in_ag1(x2)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
region_33(x1, x2, x3)  =  region_32(x2, x3)
if_color_map_2_in_1_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_1_ag2(x3, x4)
color_region_2_in_ag2(x1, x2)  =  color_region_2_in_ag1(x2)
if_color_region_2_in_1_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_1_ag1(x5)
select_3_in_aga3(x1, x2, x3)  =  select_3_in_aga1(x2)
select_3_out_aga3(x1, x2, x3)  =  select_3_out_aga2(x1, x3)
if_select_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_select_3_in_1_aga2(x2, x5)
if_color_region_2_in_2_ag6(x1, x2, x3, x4, x5, x6)  =  if_color_region_2_in_2_ag2(x2, x6)
members_2_in_ag2(x1, x2)  =  members_2_in_ag1(x2)
if_members_2_in_1_ag4(x1, x2, x3, x4)  =  if_members_2_in_1_ag2(x3, x4)
member_2_in_ag2(x1, x2)  =  member_2_in_ag1(x2)
member_2_out_ag2(x1, x2)  =  member_2_out_ag1(x1)
if_member_2_in_1_ag4(x1, x2, x3, x4)  =  if_member_2_in_1_ag1(x4)
if_members_2_in_2_ag4(x1, x2, x3, x4)  =  if_members_2_in_2_ag2(x1, x4)
members_2_out_ag2(x1, x2)  =  members_2_out_ag1(x1)
color_region_2_out_ag2(x1, x2)  =  color_region_2_out_ag1(x1)
if_color_map_2_in_2_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_2_ag2(x1, x4)
color_map_2_out_ag2(x1, x2)  =  color_map_2_out_ag1(x1)
IF_MEMBERS_2_IN_1_AG4(x1, x2, x3, x4)  =  IF_MEMBERS_2_IN_1_AG2(x3, x4)
MEMBERS_2_IN_AG2(x1, x2)  =  MEMBERS_2_IN_AG1(x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

MEMBERS_2_IN_AG2(._22(X, Xs), Ys) -> IF_MEMBERS_2_IN_1_AG4(X, Xs, Ys, member_2_in_ag2(X, Ys))
IF_MEMBERS_2_IN_1_AG4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> MEMBERS_2_IN_AG2(Xs, Ys)

The TRS R consists of the following rules:

member_2_in_ag2(X, ._22(X, underscore)) -> member_2_out_ag2(X, ._22(X, underscore))
member_2_in_ag2(X, ._22(underscore1, Xs)) -> if_member_2_in_1_ag4(X, underscore1, Xs, member_2_in_ag2(X, Xs))
if_member_2_in_1_ag4(X, underscore1, Xs, member_2_out_ag2(X, Xs)) -> member_2_out_ag2(X, ._22(underscore1, Xs))

The argument filtering Pi contains the following mapping:
._22(x1, x2)  =  ._22(x1, x2)
member_2_in_ag2(x1, x2)  =  member_2_in_ag1(x2)
member_2_out_ag2(x1, x2)  =  member_2_out_ag1(x1)
if_member_2_in_1_ag4(x1, x2, x3, x4)  =  if_member_2_in_1_ag1(x4)
IF_MEMBERS_2_IN_1_AG4(x1, x2, x3, x4)  =  IF_MEMBERS_2_IN_1_AG2(x3, x4)
MEMBERS_2_IN_AG2(x1, x2)  =  MEMBERS_2_IN_AG1(x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
QDP
              ↳ PiDP
              ↳ PiDP
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

MEMBERS_2_IN_AG1(Ys) -> IF_MEMBERS_2_IN_1_AG2(Ys, member_2_in_ag1(Ys))
IF_MEMBERS_2_IN_1_AG2(Ys, member_2_out_ag1(X)) -> MEMBERS_2_IN_AG1(Ys)

The TRS R consists of the following rules:

member_2_in_ag1(._22(X, underscore)) -> member_2_out_ag1(X)
member_2_in_ag1(._22(underscore1, Xs)) -> if_member_2_in_1_ag1(member_2_in_ag1(Xs))
if_member_2_in_1_ag1(member_2_out_ag1(X)) -> member_2_out_ag1(X)

The set Q consists of the following terms:

member_2_in_ag1(x0)
if_member_2_in_1_ag1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_MEMBERS_2_IN_1_AG2, MEMBERS_2_IN_AG1}.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
PiDP
                ↳ UsableRulesProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

SELECT_3_IN_AGA3(X, ._22(Y, Ys), ._22(Y, Zs)) -> SELECT_3_IN_AGA3(X, Ys, Zs)

The TRS R consists of the following rules:

color_map_2_in_ag2(._22(Region, Regions), Colors) -> if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_in_ag2(Region, Colors))
color_region_2_in_ag2(region_33(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_in_aga3(Color, Colors, Colors1))
select_3_in_aga3(X, ._22(X, Xs), Xs) -> select_3_out_aga3(X, ._22(X, Xs), Xs)
select_3_in_aga3(X, ._22(Y, Ys), ._22(Y, Zs)) -> if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_in_aga3(X, Ys, Zs))
if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_out_aga3(X, Ys, Zs)) -> select_3_out_aga3(X, ._22(Y, Ys), ._22(Y, Zs))
if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag2(Neighbors, Colors1))
members_2_in_ag2(._22(X, Xs), Ys) -> if_members_2_in_1_ag4(X, Xs, Ys, member_2_in_ag2(X, Ys))
member_2_in_ag2(X, ._22(X, underscore)) -> member_2_out_ag2(X, ._22(X, underscore))
member_2_in_ag2(X, ._22(underscore1, Xs)) -> if_member_2_in_1_ag4(X, underscore1, Xs, member_2_in_ag2(X, Xs))
if_member_2_in_1_ag4(X, underscore1, Xs, member_2_out_ag2(X, Xs)) -> member_2_out_ag2(X, ._22(underscore1, Xs))
if_members_2_in_1_ag4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> if_members_2_in_2_ag4(X, Xs, Ys, members_2_in_ag2(Xs, Ys))
members_2_in_ag2([]_0, Ys) -> members_2_out_ag2([]_0, Ys)
if_members_2_in_2_ag4(X, Xs, Ys, members_2_out_ag2(Xs, Ys)) -> members_2_out_ag2(._22(X, Xs), Ys)
if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_33(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_in_ag2(Regions, Colors))
color_map_2_in_ag2([]_0, Colors) -> color_map_2_out_ag2([]_0, Colors)
if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_out_ag2(Regions, Colors)) -> color_map_2_out_ag2(._22(Region, Regions), Colors)

The argument filtering Pi contains the following mapping:
color_map_2_in_ag2(x1, x2)  =  color_map_2_in_ag1(x2)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
region_33(x1, x2, x3)  =  region_32(x2, x3)
if_color_map_2_in_1_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_1_ag2(x3, x4)
color_region_2_in_ag2(x1, x2)  =  color_region_2_in_ag1(x2)
if_color_region_2_in_1_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_1_ag1(x5)
select_3_in_aga3(x1, x2, x3)  =  select_3_in_aga1(x2)
select_3_out_aga3(x1, x2, x3)  =  select_3_out_aga2(x1, x3)
if_select_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_select_3_in_1_aga2(x2, x5)
if_color_region_2_in_2_ag6(x1, x2, x3, x4, x5, x6)  =  if_color_region_2_in_2_ag2(x2, x6)
members_2_in_ag2(x1, x2)  =  members_2_in_ag1(x2)
if_members_2_in_1_ag4(x1, x2, x3, x4)  =  if_members_2_in_1_ag2(x3, x4)
member_2_in_ag2(x1, x2)  =  member_2_in_ag1(x2)
member_2_out_ag2(x1, x2)  =  member_2_out_ag1(x1)
if_member_2_in_1_ag4(x1, x2, x3, x4)  =  if_member_2_in_1_ag1(x4)
if_members_2_in_2_ag4(x1, x2, x3, x4)  =  if_members_2_in_2_ag2(x1, x4)
members_2_out_ag2(x1, x2)  =  members_2_out_ag1(x1)
color_region_2_out_ag2(x1, x2)  =  color_region_2_out_ag1(x1)
if_color_map_2_in_2_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_2_ag2(x1, x4)
color_map_2_out_ag2(x1, x2)  =  color_map_2_out_ag1(x1)
SELECT_3_IN_AGA3(x1, x2, x3)  =  SELECT_3_IN_AGA1(x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

SELECT_3_IN_AGA3(X, ._22(Y, Ys), ._22(Y, Zs)) -> SELECT_3_IN_AGA3(X, Ys, Zs)

R is empty.
The argument filtering Pi contains the following mapping:
._22(x1, x2)  =  ._22(x1, x2)
SELECT_3_IN_AGA3(x1, x2, x3)  =  SELECT_3_IN_AGA1(x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

SELECT_3_IN_AGA1(._22(Y, Ys)) -> SELECT_3_IN_AGA1(Ys)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {SELECT_3_IN_AGA1}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
PiDP
                ↳ UsableRulesProof
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

COLOR_MAP_2_IN_AG2(._22(Region, Regions), Colors) -> IF_COLOR_MAP_2_IN_1_AG4(Region, Regions, Colors, color_region_2_in_ag2(Region, Colors))
IF_COLOR_MAP_2_IN_1_AG4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> COLOR_MAP_2_IN_AG2(Regions, Colors)

The TRS R consists of the following rules:

color_map_2_in_ag2(._22(Region, Regions), Colors) -> if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_in_ag2(Region, Colors))
color_region_2_in_ag2(region_33(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_in_aga3(Color, Colors, Colors1))
select_3_in_aga3(X, ._22(X, Xs), Xs) -> select_3_out_aga3(X, ._22(X, Xs), Xs)
select_3_in_aga3(X, ._22(Y, Ys), ._22(Y, Zs)) -> if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_in_aga3(X, Ys, Zs))
if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_out_aga3(X, Ys, Zs)) -> select_3_out_aga3(X, ._22(Y, Ys), ._22(Y, Zs))
if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag2(Neighbors, Colors1))
members_2_in_ag2(._22(X, Xs), Ys) -> if_members_2_in_1_ag4(X, Xs, Ys, member_2_in_ag2(X, Ys))
member_2_in_ag2(X, ._22(X, underscore)) -> member_2_out_ag2(X, ._22(X, underscore))
member_2_in_ag2(X, ._22(underscore1, Xs)) -> if_member_2_in_1_ag4(X, underscore1, Xs, member_2_in_ag2(X, Xs))
if_member_2_in_1_ag4(X, underscore1, Xs, member_2_out_ag2(X, Xs)) -> member_2_out_ag2(X, ._22(underscore1, Xs))
if_members_2_in_1_ag4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> if_members_2_in_2_ag4(X, Xs, Ys, members_2_in_ag2(Xs, Ys))
members_2_in_ag2([]_0, Ys) -> members_2_out_ag2([]_0, Ys)
if_members_2_in_2_ag4(X, Xs, Ys, members_2_out_ag2(Xs, Ys)) -> members_2_out_ag2(._22(X, Xs), Ys)
if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_33(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_in_ag2(Regions, Colors))
color_map_2_in_ag2([]_0, Colors) -> color_map_2_out_ag2([]_0, Colors)
if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_out_ag2(Regions, Colors)) -> color_map_2_out_ag2(._22(Region, Regions), Colors)

The argument filtering Pi contains the following mapping:
color_map_2_in_ag2(x1, x2)  =  color_map_2_in_ag1(x2)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
region_33(x1, x2, x3)  =  region_32(x2, x3)
if_color_map_2_in_1_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_1_ag2(x3, x4)
color_region_2_in_ag2(x1, x2)  =  color_region_2_in_ag1(x2)
if_color_region_2_in_1_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_1_ag1(x5)
select_3_in_aga3(x1, x2, x3)  =  select_3_in_aga1(x2)
select_3_out_aga3(x1, x2, x3)  =  select_3_out_aga2(x1, x3)
if_select_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_select_3_in_1_aga2(x2, x5)
if_color_region_2_in_2_ag6(x1, x2, x3, x4, x5, x6)  =  if_color_region_2_in_2_ag2(x2, x6)
members_2_in_ag2(x1, x2)  =  members_2_in_ag1(x2)
if_members_2_in_1_ag4(x1, x2, x3, x4)  =  if_members_2_in_1_ag2(x3, x4)
member_2_in_ag2(x1, x2)  =  member_2_in_ag1(x2)
member_2_out_ag2(x1, x2)  =  member_2_out_ag1(x1)
if_member_2_in_1_ag4(x1, x2, x3, x4)  =  if_member_2_in_1_ag1(x4)
if_members_2_in_2_ag4(x1, x2, x3, x4)  =  if_members_2_in_2_ag2(x1, x4)
members_2_out_ag2(x1, x2)  =  members_2_out_ag1(x1)
color_region_2_out_ag2(x1, x2)  =  color_region_2_out_ag1(x1)
if_color_map_2_in_2_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_2_ag2(x1, x4)
color_map_2_out_ag2(x1, x2)  =  color_map_2_out_ag1(x1)
COLOR_MAP_2_IN_AG2(x1, x2)  =  COLOR_MAP_2_IN_AG1(x2)
IF_COLOR_MAP_2_IN_1_AG4(x1, x2, x3, x4)  =  IF_COLOR_MAP_2_IN_1_AG2(x3, x4)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
PiDP
                    ↳ PiDPToQDPProof
  ↳ PrologToPiTRSProof

Pi DP problem:
The TRS P consists of the following rules:

COLOR_MAP_2_IN_AG2(._22(Region, Regions), Colors) -> IF_COLOR_MAP_2_IN_1_AG4(Region, Regions, Colors, color_region_2_in_ag2(Region, Colors))
IF_COLOR_MAP_2_IN_1_AG4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> COLOR_MAP_2_IN_AG2(Regions, Colors)

The TRS R consists of the following rules:

color_region_2_in_ag2(region_33(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_in_aga3(Color, Colors, Colors1))
if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag2(Neighbors, Colors1))
select_3_in_aga3(X, ._22(X, Xs), Xs) -> select_3_out_aga3(X, ._22(X, Xs), Xs)
select_3_in_aga3(X, ._22(Y, Ys), ._22(Y, Zs)) -> if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_in_aga3(X, Ys, Zs))
if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_33(Name, Color, Neighbors), Colors)
if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_out_aga3(X, Ys, Zs)) -> select_3_out_aga3(X, ._22(Y, Ys), ._22(Y, Zs))
members_2_in_ag2(._22(X, Xs), Ys) -> if_members_2_in_1_ag4(X, Xs, Ys, member_2_in_ag2(X, Ys))
members_2_in_ag2([]_0, Ys) -> members_2_out_ag2([]_0, Ys)
if_members_2_in_1_ag4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> if_members_2_in_2_ag4(X, Xs, Ys, members_2_in_ag2(Xs, Ys))
member_2_in_ag2(X, ._22(X, underscore)) -> member_2_out_ag2(X, ._22(X, underscore))
member_2_in_ag2(X, ._22(underscore1, Xs)) -> if_member_2_in_1_ag4(X, underscore1, Xs, member_2_in_ag2(X, Xs))
if_members_2_in_2_ag4(X, Xs, Ys, members_2_out_ag2(Xs, Ys)) -> members_2_out_ag2(._22(X, Xs), Ys)
if_member_2_in_1_ag4(X, underscore1, Xs, member_2_out_ag2(X, Xs)) -> member_2_out_ag2(X, ._22(underscore1, Xs))

The argument filtering Pi contains the following mapping:
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
region_33(x1, x2, x3)  =  region_32(x2, x3)
color_region_2_in_ag2(x1, x2)  =  color_region_2_in_ag1(x2)
if_color_region_2_in_1_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_1_ag1(x5)
select_3_in_aga3(x1, x2, x3)  =  select_3_in_aga1(x2)
select_3_out_aga3(x1, x2, x3)  =  select_3_out_aga2(x1, x3)
if_select_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_select_3_in_1_aga2(x2, x5)
if_color_region_2_in_2_ag6(x1, x2, x3, x4, x5, x6)  =  if_color_region_2_in_2_ag2(x2, x6)
members_2_in_ag2(x1, x2)  =  members_2_in_ag1(x2)
if_members_2_in_1_ag4(x1, x2, x3, x4)  =  if_members_2_in_1_ag2(x3, x4)
member_2_in_ag2(x1, x2)  =  member_2_in_ag1(x2)
member_2_out_ag2(x1, x2)  =  member_2_out_ag1(x1)
if_member_2_in_1_ag4(x1, x2, x3, x4)  =  if_member_2_in_1_ag1(x4)
if_members_2_in_2_ag4(x1, x2, x3, x4)  =  if_members_2_in_2_ag2(x1, x4)
members_2_out_ag2(x1, x2)  =  members_2_out_ag1(x1)
color_region_2_out_ag2(x1, x2)  =  color_region_2_out_ag1(x1)
COLOR_MAP_2_IN_AG2(x1, x2)  =  COLOR_MAP_2_IN_AG1(x2)
IF_COLOR_MAP_2_IN_1_AG4(x1, x2, x3, x4)  =  IF_COLOR_MAP_2_IN_1_AG2(x3, x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
QDP
  ↳ PrologToPiTRSProof

Q DP problem:
The TRS P consists of the following rules:

COLOR_MAP_2_IN_AG1(Colors) -> IF_COLOR_MAP_2_IN_1_AG2(Colors, color_region_2_in_ag1(Colors))
IF_COLOR_MAP_2_IN_1_AG2(Colors, color_region_2_out_ag1(Region)) -> COLOR_MAP_2_IN_AG1(Colors)

The TRS R consists of the following rules:

color_region_2_in_ag1(Colors) -> if_color_region_2_in_1_ag1(select_3_in_aga1(Colors))
if_color_region_2_in_1_ag1(select_3_out_aga2(Color, Colors1)) -> if_color_region_2_in_2_ag2(Color, members_2_in_ag1(Colors1))
select_3_in_aga1(._22(X, Xs)) -> select_3_out_aga2(X, Xs)
select_3_in_aga1(._22(Y, Ys)) -> if_select_3_in_1_aga2(Y, select_3_in_aga1(Ys))
if_color_region_2_in_2_ag2(Color, members_2_out_ag1(Neighbors)) -> color_region_2_out_ag1(region_32(Color, Neighbors))
if_select_3_in_1_aga2(Y, select_3_out_aga2(X, Zs)) -> select_3_out_aga2(X, ._22(Y, Zs))
members_2_in_ag1(Ys) -> if_members_2_in_1_ag2(Ys, member_2_in_ag1(Ys))
members_2_in_ag1(Ys) -> members_2_out_ag1([]_0)
if_members_2_in_1_ag2(Ys, member_2_out_ag1(X)) -> if_members_2_in_2_ag2(X, members_2_in_ag1(Ys))
member_2_in_ag1(._22(X, underscore)) -> member_2_out_ag1(X)
member_2_in_ag1(._22(underscore1, Xs)) -> if_member_2_in_1_ag1(member_2_in_ag1(Xs))
if_members_2_in_2_ag2(X, members_2_out_ag1(Xs)) -> members_2_out_ag1(._22(X, Xs))
if_member_2_in_1_ag1(member_2_out_ag1(X)) -> member_2_out_ag1(X)

The set Q consists of the following terms:

color_region_2_in_ag1(x0)
if_color_region_2_in_1_ag1(x0)
select_3_in_aga1(x0)
if_color_region_2_in_2_ag2(x0, x1)
if_select_3_in_1_aga2(x0, x1)
members_2_in_ag1(x0)
if_members_2_in_1_ag2(x0, x1)
member_2_in_ag1(x0)
if_members_2_in_2_ag2(x0, x1)
if_member_2_in_1_ag1(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_COLOR_MAP_2_IN_1_AG2, COLOR_MAP_2_IN_AG1}.
With regard to the inferred argument filtering the predicates were used in the following modes:
color_map2: (f,b)
color_region2: (f,b)
select3: (f,b,f)
members2: (f,b)
member2: (f,b)
Transforming PROLOG into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

color_map_2_in_ag2(._22(Region, Regions), Colors) -> if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_in_ag2(Region, Colors))
color_region_2_in_ag2(region_33(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_in_aga3(Color, Colors, Colors1))
select_3_in_aga3(X, ._22(X, Xs), Xs) -> select_3_out_aga3(X, ._22(X, Xs), Xs)
select_3_in_aga3(X, ._22(Y, Ys), ._22(Y, Zs)) -> if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_in_aga3(X, Ys, Zs))
if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_out_aga3(X, Ys, Zs)) -> select_3_out_aga3(X, ._22(Y, Ys), ._22(Y, Zs))
if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag2(Neighbors, Colors1))
members_2_in_ag2(._22(X, Xs), Ys) -> if_members_2_in_1_ag4(X, Xs, Ys, member_2_in_ag2(X, Ys))
member_2_in_ag2(X, ._22(X, underscore)) -> member_2_out_ag2(X, ._22(X, underscore))
member_2_in_ag2(X, ._22(underscore1, Xs)) -> if_member_2_in_1_ag4(X, underscore1, Xs, member_2_in_ag2(X, Xs))
if_member_2_in_1_ag4(X, underscore1, Xs, member_2_out_ag2(X, Xs)) -> member_2_out_ag2(X, ._22(underscore1, Xs))
if_members_2_in_1_ag4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> if_members_2_in_2_ag4(X, Xs, Ys, members_2_in_ag2(Xs, Ys))
members_2_in_ag2([]_0, Ys) -> members_2_out_ag2([]_0, Ys)
if_members_2_in_2_ag4(X, Xs, Ys, members_2_out_ag2(Xs, Ys)) -> members_2_out_ag2(._22(X, Xs), Ys)
if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_33(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_in_ag2(Regions, Colors))
color_map_2_in_ag2([]_0, Colors) -> color_map_2_out_ag2([]_0, Colors)
if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_out_ag2(Regions, Colors)) -> color_map_2_out_ag2(._22(Region, Regions), Colors)

The argument filtering Pi contains the following mapping:
color_map_2_in_ag2(x1, x2)  =  color_map_2_in_ag1(x2)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
region_33(x1, x2, x3)  =  region_32(x2, x3)
if_color_map_2_in_1_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_1_ag2(x3, x4)
color_region_2_in_ag2(x1, x2)  =  color_region_2_in_ag1(x2)
if_color_region_2_in_1_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_1_ag2(x4, x5)
select_3_in_aga3(x1, x2, x3)  =  select_3_in_aga1(x2)
select_3_out_aga3(x1, x2, x3)  =  select_3_out_aga3(x1, x2, x3)
if_select_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_select_3_in_1_aga3(x2, x3, x5)
if_color_region_2_in_2_ag6(x1, x2, x3, x4, x5, x6)  =  if_color_region_2_in_2_ag3(x2, x4, x6)
members_2_in_ag2(x1, x2)  =  members_2_in_ag1(x2)
if_members_2_in_1_ag4(x1, x2, x3, x4)  =  if_members_2_in_1_ag2(x3, x4)
member_2_in_ag2(x1, x2)  =  member_2_in_ag1(x2)
member_2_out_ag2(x1, x2)  =  member_2_out_ag2(x1, x2)
if_member_2_in_1_ag4(x1, x2, x3, x4)  =  if_member_2_in_1_ag3(x2, x3, x4)
if_members_2_in_2_ag4(x1, x2, x3, x4)  =  if_members_2_in_2_ag3(x1, x3, x4)
members_2_out_ag2(x1, x2)  =  members_2_out_ag2(x1, x2)
color_region_2_out_ag2(x1, x2)  =  color_region_2_out_ag2(x1, x2)
if_color_map_2_in_2_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_2_ag3(x1, x3, x4)
color_map_2_out_ag2(x1, x2)  =  color_map_2_out_ag2(x1, x2)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG



↳ PROLOG
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
PiTRS
      ↳ DependencyPairsProof

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

color_map_2_in_ag2(._22(Region, Regions), Colors) -> if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_in_ag2(Region, Colors))
color_region_2_in_ag2(region_33(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_in_aga3(Color, Colors, Colors1))
select_3_in_aga3(X, ._22(X, Xs), Xs) -> select_3_out_aga3(X, ._22(X, Xs), Xs)
select_3_in_aga3(X, ._22(Y, Ys), ._22(Y, Zs)) -> if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_in_aga3(X, Ys, Zs))
if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_out_aga3(X, Ys, Zs)) -> select_3_out_aga3(X, ._22(Y, Ys), ._22(Y, Zs))
if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag2(Neighbors, Colors1))
members_2_in_ag2(._22(X, Xs), Ys) -> if_members_2_in_1_ag4(X, Xs, Ys, member_2_in_ag2(X, Ys))
member_2_in_ag2(X, ._22(X, underscore)) -> member_2_out_ag2(X, ._22(X, underscore))
member_2_in_ag2(X, ._22(underscore1, Xs)) -> if_member_2_in_1_ag4(X, underscore1, Xs, member_2_in_ag2(X, Xs))
if_member_2_in_1_ag4(X, underscore1, Xs, member_2_out_ag2(X, Xs)) -> member_2_out_ag2(X, ._22(underscore1, Xs))
if_members_2_in_1_ag4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> if_members_2_in_2_ag4(X, Xs, Ys, members_2_in_ag2(Xs, Ys))
members_2_in_ag2([]_0, Ys) -> members_2_out_ag2([]_0, Ys)
if_members_2_in_2_ag4(X, Xs, Ys, members_2_out_ag2(Xs, Ys)) -> members_2_out_ag2(._22(X, Xs), Ys)
if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_33(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_in_ag2(Regions, Colors))
color_map_2_in_ag2([]_0, Colors) -> color_map_2_out_ag2([]_0, Colors)
if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_out_ag2(Regions, Colors)) -> color_map_2_out_ag2(._22(Region, Regions), Colors)

The argument filtering Pi contains the following mapping:
color_map_2_in_ag2(x1, x2)  =  color_map_2_in_ag1(x2)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
region_33(x1, x2, x3)  =  region_32(x2, x3)
if_color_map_2_in_1_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_1_ag2(x3, x4)
color_region_2_in_ag2(x1, x2)  =  color_region_2_in_ag1(x2)
if_color_region_2_in_1_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_1_ag2(x4, x5)
select_3_in_aga3(x1, x2, x3)  =  select_3_in_aga1(x2)
select_3_out_aga3(x1, x2, x3)  =  select_3_out_aga3(x1, x2, x3)
if_select_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_select_3_in_1_aga3(x2, x3, x5)
if_color_region_2_in_2_ag6(x1, x2, x3, x4, x5, x6)  =  if_color_region_2_in_2_ag3(x2, x4, x6)
members_2_in_ag2(x1, x2)  =  members_2_in_ag1(x2)
if_members_2_in_1_ag4(x1, x2, x3, x4)  =  if_members_2_in_1_ag2(x3, x4)
member_2_in_ag2(x1, x2)  =  member_2_in_ag1(x2)
member_2_out_ag2(x1, x2)  =  member_2_out_ag2(x1, x2)
if_member_2_in_1_ag4(x1, x2, x3, x4)  =  if_member_2_in_1_ag3(x2, x3, x4)
if_members_2_in_2_ag4(x1, x2, x3, x4)  =  if_members_2_in_2_ag3(x1, x3, x4)
members_2_out_ag2(x1, x2)  =  members_2_out_ag2(x1, x2)
color_region_2_out_ag2(x1, x2)  =  color_region_2_out_ag2(x1, x2)
if_color_map_2_in_2_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_2_ag3(x1, x3, x4)
color_map_2_out_ag2(x1, x2)  =  color_map_2_out_ag2(x1, x2)


Pi DP problem:
The TRS P consists of the following rules:

COLOR_MAP_2_IN_AG2(._22(Region, Regions), Colors) -> IF_COLOR_MAP_2_IN_1_AG4(Region, Regions, Colors, color_region_2_in_ag2(Region, Colors))
COLOR_MAP_2_IN_AG2(._22(Region, Regions), Colors) -> COLOR_REGION_2_IN_AG2(Region, Colors)
COLOR_REGION_2_IN_AG2(region_33(Name, Color, Neighbors), Colors) -> IF_COLOR_REGION_2_IN_1_AG5(Name, Color, Neighbors, Colors, select_3_in_aga3(Color, Colors, Colors1))
COLOR_REGION_2_IN_AG2(region_33(Name, Color, Neighbors), Colors) -> SELECT_3_IN_AGA3(Color, Colors, Colors1)
SELECT_3_IN_AGA3(X, ._22(Y, Ys), ._22(Y, Zs)) -> IF_SELECT_3_IN_1_AGA5(X, Y, Ys, Zs, select_3_in_aga3(X, Ys, Zs))
SELECT_3_IN_AGA3(X, ._22(Y, Ys), ._22(Y, Zs)) -> SELECT_3_IN_AGA3(X, Ys, Zs)
IF_COLOR_REGION_2_IN_1_AG5(Name, Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> IF_COLOR_REGION_2_IN_2_AG6(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag2(Neighbors, Colors1))
IF_COLOR_REGION_2_IN_1_AG5(Name, Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> MEMBERS_2_IN_AG2(Neighbors, Colors1)
MEMBERS_2_IN_AG2(._22(X, Xs), Ys) -> IF_MEMBERS_2_IN_1_AG4(X, Xs, Ys, member_2_in_ag2(X, Ys))
MEMBERS_2_IN_AG2(._22(X, Xs), Ys) -> MEMBER_2_IN_AG2(X, Ys)
MEMBER_2_IN_AG2(X, ._22(underscore1, Xs)) -> IF_MEMBER_2_IN_1_AG4(X, underscore1, Xs, member_2_in_ag2(X, Xs))
MEMBER_2_IN_AG2(X, ._22(underscore1, Xs)) -> MEMBER_2_IN_AG2(X, Xs)
IF_MEMBERS_2_IN_1_AG4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> IF_MEMBERS_2_IN_2_AG4(X, Xs, Ys, members_2_in_ag2(Xs, Ys))
IF_MEMBERS_2_IN_1_AG4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> MEMBERS_2_IN_AG2(Xs, Ys)
IF_COLOR_MAP_2_IN_1_AG4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> IF_COLOR_MAP_2_IN_2_AG4(Region, Regions, Colors, color_map_2_in_ag2(Regions, Colors))
IF_COLOR_MAP_2_IN_1_AG4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> COLOR_MAP_2_IN_AG2(Regions, Colors)

The TRS R consists of the following rules:

color_map_2_in_ag2(._22(Region, Regions), Colors) -> if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_in_ag2(Region, Colors))
color_region_2_in_ag2(region_33(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_in_aga3(Color, Colors, Colors1))
select_3_in_aga3(X, ._22(X, Xs), Xs) -> select_3_out_aga3(X, ._22(X, Xs), Xs)
select_3_in_aga3(X, ._22(Y, Ys), ._22(Y, Zs)) -> if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_in_aga3(X, Ys, Zs))
if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_out_aga3(X, Ys, Zs)) -> select_3_out_aga3(X, ._22(Y, Ys), ._22(Y, Zs))
if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag2(Neighbors, Colors1))
members_2_in_ag2(._22(X, Xs), Ys) -> if_members_2_in_1_ag4(X, Xs, Ys, member_2_in_ag2(X, Ys))
member_2_in_ag2(X, ._22(X, underscore)) -> member_2_out_ag2(X, ._22(X, underscore))
member_2_in_ag2(X, ._22(underscore1, Xs)) -> if_member_2_in_1_ag4(X, underscore1, Xs, member_2_in_ag2(X, Xs))
if_member_2_in_1_ag4(X, underscore1, Xs, member_2_out_ag2(X, Xs)) -> member_2_out_ag2(X, ._22(underscore1, Xs))
if_members_2_in_1_ag4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> if_members_2_in_2_ag4(X, Xs, Ys, members_2_in_ag2(Xs, Ys))
members_2_in_ag2([]_0, Ys) -> members_2_out_ag2([]_0, Ys)
if_members_2_in_2_ag4(X, Xs, Ys, members_2_out_ag2(Xs, Ys)) -> members_2_out_ag2(._22(X, Xs), Ys)
if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_33(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_in_ag2(Regions, Colors))
color_map_2_in_ag2([]_0, Colors) -> color_map_2_out_ag2([]_0, Colors)
if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_out_ag2(Regions, Colors)) -> color_map_2_out_ag2(._22(Region, Regions), Colors)

The argument filtering Pi contains the following mapping:
color_map_2_in_ag2(x1, x2)  =  color_map_2_in_ag1(x2)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
region_33(x1, x2, x3)  =  region_32(x2, x3)
if_color_map_2_in_1_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_1_ag2(x3, x4)
color_region_2_in_ag2(x1, x2)  =  color_region_2_in_ag1(x2)
if_color_region_2_in_1_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_1_ag2(x4, x5)
select_3_in_aga3(x1, x2, x3)  =  select_3_in_aga1(x2)
select_3_out_aga3(x1, x2, x3)  =  select_3_out_aga3(x1, x2, x3)
if_select_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_select_3_in_1_aga3(x2, x3, x5)
if_color_region_2_in_2_ag6(x1, x2, x3, x4, x5, x6)  =  if_color_region_2_in_2_ag3(x2, x4, x6)
members_2_in_ag2(x1, x2)  =  members_2_in_ag1(x2)
if_members_2_in_1_ag4(x1, x2, x3, x4)  =  if_members_2_in_1_ag2(x3, x4)
member_2_in_ag2(x1, x2)  =  member_2_in_ag1(x2)
member_2_out_ag2(x1, x2)  =  member_2_out_ag2(x1, x2)
if_member_2_in_1_ag4(x1, x2, x3, x4)  =  if_member_2_in_1_ag3(x2, x3, x4)
if_members_2_in_2_ag4(x1, x2, x3, x4)  =  if_members_2_in_2_ag3(x1, x3, x4)
members_2_out_ag2(x1, x2)  =  members_2_out_ag2(x1, x2)
color_region_2_out_ag2(x1, x2)  =  color_region_2_out_ag2(x1, x2)
if_color_map_2_in_2_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_2_ag3(x1, x3, x4)
color_map_2_out_ag2(x1, x2)  =  color_map_2_out_ag2(x1, x2)
IF_COLOR_REGION_2_IN_2_AG6(x1, x2, x3, x4, x5, x6)  =  IF_COLOR_REGION_2_IN_2_AG3(x2, x4, x6)
IF_MEMBERS_2_IN_1_AG4(x1, x2, x3, x4)  =  IF_MEMBERS_2_IN_1_AG2(x3, x4)
IF_MEMBERS_2_IN_2_AG4(x1, x2, x3, x4)  =  IF_MEMBERS_2_IN_2_AG3(x1, x3, x4)
COLOR_MAP_2_IN_AG2(x1, x2)  =  COLOR_MAP_2_IN_AG1(x2)
MEMBERS_2_IN_AG2(x1, x2)  =  MEMBERS_2_IN_AG1(x2)
IF_COLOR_MAP_2_IN_1_AG4(x1, x2, x3, x4)  =  IF_COLOR_MAP_2_IN_1_AG2(x3, x4)
MEMBER_2_IN_AG2(x1, x2)  =  MEMBER_2_IN_AG1(x2)
IF_SELECT_3_IN_1_AGA5(x1, x2, x3, x4, x5)  =  IF_SELECT_3_IN_1_AGA3(x2, x3, x5)
IF_COLOR_MAP_2_IN_2_AG4(x1, x2, x3, x4)  =  IF_COLOR_MAP_2_IN_2_AG3(x1, x3, x4)
COLOR_REGION_2_IN_AG2(x1, x2)  =  COLOR_REGION_2_IN_AG1(x2)
IF_MEMBER_2_IN_1_AG4(x1, x2, x3, x4)  =  IF_MEMBER_2_IN_1_AG3(x2, x3, x4)
IF_COLOR_REGION_2_IN_1_AG5(x1, x2, x3, x4, x5)  =  IF_COLOR_REGION_2_IN_1_AG2(x4, x5)
SELECT_3_IN_AGA3(x1, x2, x3)  =  SELECT_3_IN_AGA1(x2)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

COLOR_MAP_2_IN_AG2(._22(Region, Regions), Colors) -> IF_COLOR_MAP_2_IN_1_AG4(Region, Regions, Colors, color_region_2_in_ag2(Region, Colors))
COLOR_MAP_2_IN_AG2(._22(Region, Regions), Colors) -> COLOR_REGION_2_IN_AG2(Region, Colors)
COLOR_REGION_2_IN_AG2(region_33(Name, Color, Neighbors), Colors) -> IF_COLOR_REGION_2_IN_1_AG5(Name, Color, Neighbors, Colors, select_3_in_aga3(Color, Colors, Colors1))
COLOR_REGION_2_IN_AG2(region_33(Name, Color, Neighbors), Colors) -> SELECT_3_IN_AGA3(Color, Colors, Colors1)
SELECT_3_IN_AGA3(X, ._22(Y, Ys), ._22(Y, Zs)) -> IF_SELECT_3_IN_1_AGA5(X, Y, Ys, Zs, select_3_in_aga3(X, Ys, Zs))
SELECT_3_IN_AGA3(X, ._22(Y, Ys), ._22(Y, Zs)) -> SELECT_3_IN_AGA3(X, Ys, Zs)
IF_COLOR_REGION_2_IN_1_AG5(Name, Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> IF_COLOR_REGION_2_IN_2_AG6(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag2(Neighbors, Colors1))
IF_COLOR_REGION_2_IN_1_AG5(Name, Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> MEMBERS_2_IN_AG2(Neighbors, Colors1)
MEMBERS_2_IN_AG2(._22(X, Xs), Ys) -> IF_MEMBERS_2_IN_1_AG4(X, Xs, Ys, member_2_in_ag2(X, Ys))
MEMBERS_2_IN_AG2(._22(X, Xs), Ys) -> MEMBER_2_IN_AG2(X, Ys)
MEMBER_2_IN_AG2(X, ._22(underscore1, Xs)) -> IF_MEMBER_2_IN_1_AG4(X, underscore1, Xs, member_2_in_ag2(X, Xs))
MEMBER_2_IN_AG2(X, ._22(underscore1, Xs)) -> MEMBER_2_IN_AG2(X, Xs)
IF_MEMBERS_2_IN_1_AG4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> IF_MEMBERS_2_IN_2_AG4(X, Xs, Ys, members_2_in_ag2(Xs, Ys))
IF_MEMBERS_2_IN_1_AG4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> MEMBERS_2_IN_AG2(Xs, Ys)
IF_COLOR_MAP_2_IN_1_AG4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> IF_COLOR_MAP_2_IN_2_AG4(Region, Regions, Colors, color_map_2_in_ag2(Regions, Colors))
IF_COLOR_MAP_2_IN_1_AG4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> COLOR_MAP_2_IN_AG2(Regions, Colors)

The TRS R consists of the following rules:

color_map_2_in_ag2(._22(Region, Regions), Colors) -> if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_in_ag2(Region, Colors))
color_region_2_in_ag2(region_33(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_in_aga3(Color, Colors, Colors1))
select_3_in_aga3(X, ._22(X, Xs), Xs) -> select_3_out_aga3(X, ._22(X, Xs), Xs)
select_3_in_aga3(X, ._22(Y, Ys), ._22(Y, Zs)) -> if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_in_aga3(X, Ys, Zs))
if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_out_aga3(X, Ys, Zs)) -> select_3_out_aga3(X, ._22(Y, Ys), ._22(Y, Zs))
if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag2(Neighbors, Colors1))
members_2_in_ag2(._22(X, Xs), Ys) -> if_members_2_in_1_ag4(X, Xs, Ys, member_2_in_ag2(X, Ys))
member_2_in_ag2(X, ._22(X, underscore)) -> member_2_out_ag2(X, ._22(X, underscore))
member_2_in_ag2(X, ._22(underscore1, Xs)) -> if_member_2_in_1_ag4(X, underscore1, Xs, member_2_in_ag2(X, Xs))
if_member_2_in_1_ag4(X, underscore1, Xs, member_2_out_ag2(X, Xs)) -> member_2_out_ag2(X, ._22(underscore1, Xs))
if_members_2_in_1_ag4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> if_members_2_in_2_ag4(X, Xs, Ys, members_2_in_ag2(Xs, Ys))
members_2_in_ag2([]_0, Ys) -> members_2_out_ag2([]_0, Ys)
if_members_2_in_2_ag4(X, Xs, Ys, members_2_out_ag2(Xs, Ys)) -> members_2_out_ag2(._22(X, Xs), Ys)
if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_33(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_in_ag2(Regions, Colors))
color_map_2_in_ag2([]_0, Colors) -> color_map_2_out_ag2([]_0, Colors)
if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_out_ag2(Regions, Colors)) -> color_map_2_out_ag2(._22(Region, Regions), Colors)

The argument filtering Pi contains the following mapping:
color_map_2_in_ag2(x1, x2)  =  color_map_2_in_ag1(x2)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
region_33(x1, x2, x3)  =  region_32(x2, x3)
if_color_map_2_in_1_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_1_ag2(x3, x4)
color_region_2_in_ag2(x1, x2)  =  color_region_2_in_ag1(x2)
if_color_region_2_in_1_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_1_ag2(x4, x5)
select_3_in_aga3(x1, x2, x3)  =  select_3_in_aga1(x2)
select_3_out_aga3(x1, x2, x3)  =  select_3_out_aga3(x1, x2, x3)
if_select_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_select_3_in_1_aga3(x2, x3, x5)
if_color_region_2_in_2_ag6(x1, x2, x3, x4, x5, x6)  =  if_color_region_2_in_2_ag3(x2, x4, x6)
members_2_in_ag2(x1, x2)  =  members_2_in_ag1(x2)
if_members_2_in_1_ag4(x1, x2, x3, x4)  =  if_members_2_in_1_ag2(x3, x4)
member_2_in_ag2(x1, x2)  =  member_2_in_ag1(x2)
member_2_out_ag2(x1, x2)  =  member_2_out_ag2(x1, x2)
if_member_2_in_1_ag4(x1, x2, x3, x4)  =  if_member_2_in_1_ag3(x2, x3, x4)
if_members_2_in_2_ag4(x1, x2, x3, x4)  =  if_members_2_in_2_ag3(x1, x3, x4)
members_2_out_ag2(x1, x2)  =  members_2_out_ag2(x1, x2)
color_region_2_out_ag2(x1, x2)  =  color_region_2_out_ag2(x1, x2)
if_color_map_2_in_2_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_2_ag3(x1, x3, x4)
color_map_2_out_ag2(x1, x2)  =  color_map_2_out_ag2(x1, x2)
IF_COLOR_REGION_2_IN_2_AG6(x1, x2, x3, x4, x5, x6)  =  IF_COLOR_REGION_2_IN_2_AG3(x2, x4, x6)
IF_MEMBERS_2_IN_1_AG4(x1, x2, x3, x4)  =  IF_MEMBERS_2_IN_1_AG2(x3, x4)
IF_MEMBERS_2_IN_2_AG4(x1, x2, x3, x4)  =  IF_MEMBERS_2_IN_2_AG3(x1, x3, x4)
COLOR_MAP_2_IN_AG2(x1, x2)  =  COLOR_MAP_2_IN_AG1(x2)
MEMBERS_2_IN_AG2(x1, x2)  =  MEMBERS_2_IN_AG1(x2)
IF_COLOR_MAP_2_IN_1_AG4(x1, x2, x3, x4)  =  IF_COLOR_MAP_2_IN_1_AG2(x3, x4)
MEMBER_2_IN_AG2(x1, x2)  =  MEMBER_2_IN_AG1(x2)
IF_SELECT_3_IN_1_AGA5(x1, x2, x3, x4, x5)  =  IF_SELECT_3_IN_1_AGA3(x2, x3, x5)
IF_COLOR_MAP_2_IN_2_AG4(x1, x2, x3, x4)  =  IF_COLOR_MAP_2_IN_2_AG3(x1, x3, x4)
COLOR_REGION_2_IN_AG2(x1, x2)  =  COLOR_REGION_2_IN_AG1(x2)
IF_MEMBER_2_IN_1_AG4(x1, x2, x3, x4)  =  IF_MEMBER_2_IN_1_AG3(x2, x3, x4)
IF_COLOR_REGION_2_IN_1_AG5(x1, x2, x3, x4, x5)  =  IF_COLOR_REGION_2_IN_1_AG2(x4, x5)
SELECT_3_IN_AGA3(x1, x2, x3)  =  SELECT_3_IN_AGA1(x2)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph contains 4 SCCs with 10 less nodes.

↳ PROLOG
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_2_IN_AG2(X, ._22(underscore1, Xs)) -> MEMBER_2_IN_AG2(X, Xs)

The TRS R consists of the following rules:

color_map_2_in_ag2(._22(Region, Regions), Colors) -> if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_in_ag2(Region, Colors))
color_region_2_in_ag2(region_33(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_in_aga3(Color, Colors, Colors1))
select_3_in_aga3(X, ._22(X, Xs), Xs) -> select_3_out_aga3(X, ._22(X, Xs), Xs)
select_3_in_aga3(X, ._22(Y, Ys), ._22(Y, Zs)) -> if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_in_aga3(X, Ys, Zs))
if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_out_aga3(X, Ys, Zs)) -> select_3_out_aga3(X, ._22(Y, Ys), ._22(Y, Zs))
if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag2(Neighbors, Colors1))
members_2_in_ag2(._22(X, Xs), Ys) -> if_members_2_in_1_ag4(X, Xs, Ys, member_2_in_ag2(X, Ys))
member_2_in_ag2(X, ._22(X, underscore)) -> member_2_out_ag2(X, ._22(X, underscore))
member_2_in_ag2(X, ._22(underscore1, Xs)) -> if_member_2_in_1_ag4(X, underscore1, Xs, member_2_in_ag2(X, Xs))
if_member_2_in_1_ag4(X, underscore1, Xs, member_2_out_ag2(X, Xs)) -> member_2_out_ag2(X, ._22(underscore1, Xs))
if_members_2_in_1_ag4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> if_members_2_in_2_ag4(X, Xs, Ys, members_2_in_ag2(Xs, Ys))
members_2_in_ag2([]_0, Ys) -> members_2_out_ag2([]_0, Ys)
if_members_2_in_2_ag4(X, Xs, Ys, members_2_out_ag2(Xs, Ys)) -> members_2_out_ag2(._22(X, Xs), Ys)
if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_33(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_in_ag2(Regions, Colors))
color_map_2_in_ag2([]_0, Colors) -> color_map_2_out_ag2([]_0, Colors)
if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_out_ag2(Regions, Colors)) -> color_map_2_out_ag2(._22(Region, Regions), Colors)

The argument filtering Pi contains the following mapping:
color_map_2_in_ag2(x1, x2)  =  color_map_2_in_ag1(x2)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
region_33(x1, x2, x3)  =  region_32(x2, x3)
if_color_map_2_in_1_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_1_ag2(x3, x4)
color_region_2_in_ag2(x1, x2)  =  color_region_2_in_ag1(x2)
if_color_region_2_in_1_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_1_ag2(x4, x5)
select_3_in_aga3(x1, x2, x3)  =  select_3_in_aga1(x2)
select_3_out_aga3(x1, x2, x3)  =  select_3_out_aga3(x1, x2, x3)
if_select_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_select_3_in_1_aga3(x2, x3, x5)
if_color_region_2_in_2_ag6(x1, x2, x3, x4, x5, x6)  =  if_color_region_2_in_2_ag3(x2, x4, x6)
members_2_in_ag2(x1, x2)  =  members_2_in_ag1(x2)
if_members_2_in_1_ag4(x1, x2, x3, x4)  =  if_members_2_in_1_ag2(x3, x4)
member_2_in_ag2(x1, x2)  =  member_2_in_ag1(x2)
member_2_out_ag2(x1, x2)  =  member_2_out_ag2(x1, x2)
if_member_2_in_1_ag4(x1, x2, x3, x4)  =  if_member_2_in_1_ag3(x2, x3, x4)
if_members_2_in_2_ag4(x1, x2, x3, x4)  =  if_members_2_in_2_ag3(x1, x3, x4)
members_2_out_ag2(x1, x2)  =  members_2_out_ag2(x1, x2)
color_region_2_out_ag2(x1, x2)  =  color_region_2_out_ag2(x1, x2)
if_color_map_2_in_2_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_2_ag3(x1, x3, x4)
color_map_2_out_ag2(x1, x2)  =  color_map_2_out_ag2(x1, x2)
MEMBER_2_IN_AG2(x1, x2)  =  MEMBER_2_IN_AG1(x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBER_2_IN_AG2(X, ._22(underscore1, Xs)) -> MEMBER_2_IN_AG2(X, Xs)

R is empty.
The argument filtering Pi contains the following mapping:
._22(x1, x2)  =  ._22(x1, x2)
MEMBER_2_IN_AG2(x1, x2)  =  MEMBER_2_IN_AG1(x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

MEMBER_2_IN_AG1(._22(underscore1, Xs)) -> MEMBER_2_IN_AG1(Xs)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {MEMBER_2_IN_AG1}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ PROLOG
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
PiDP
                ↳ UsableRulesProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBERS_2_IN_AG2(._22(X, Xs), Ys) -> IF_MEMBERS_2_IN_1_AG4(X, Xs, Ys, member_2_in_ag2(X, Ys))
IF_MEMBERS_2_IN_1_AG4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> MEMBERS_2_IN_AG2(Xs, Ys)

The TRS R consists of the following rules:

color_map_2_in_ag2(._22(Region, Regions), Colors) -> if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_in_ag2(Region, Colors))
color_region_2_in_ag2(region_33(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_in_aga3(Color, Colors, Colors1))
select_3_in_aga3(X, ._22(X, Xs), Xs) -> select_3_out_aga3(X, ._22(X, Xs), Xs)
select_3_in_aga3(X, ._22(Y, Ys), ._22(Y, Zs)) -> if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_in_aga3(X, Ys, Zs))
if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_out_aga3(X, Ys, Zs)) -> select_3_out_aga3(X, ._22(Y, Ys), ._22(Y, Zs))
if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag2(Neighbors, Colors1))
members_2_in_ag2(._22(X, Xs), Ys) -> if_members_2_in_1_ag4(X, Xs, Ys, member_2_in_ag2(X, Ys))
member_2_in_ag2(X, ._22(X, underscore)) -> member_2_out_ag2(X, ._22(X, underscore))
member_2_in_ag2(X, ._22(underscore1, Xs)) -> if_member_2_in_1_ag4(X, underscore1, Xs, member_2_in_ag2(X, Xs))
if_member_2_in_1_ag4(X, underscore1, Xs, member_2_out_ag2(X, Xs)) -> member_2_out_ag2(X, ._22(underscore1, Xs))
if_members_2_in_1_ag4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> if_members_2_in_2_ag4(X, Xs, Ys, members_2_in_ag2(Xs, Ys))
members_2_in_ag2([]_0, Ys) -> members_2_out_ag2([]_0, Ys)
if_members_2_in_2_ag4(X, Xs, Ys, members_2_out_ag2(Xs, Ys)) -> members_2_out_ag2(._22(X, Xs), Ys)
if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_33(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_in_ag2(Regions, Colors))
color_map_2_in_ag2([]_0, Colors) -> color_map_2_out_ag2([]_0, Colors)
if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_out_ag2(Regions, Colors)) -> color_map_2_out_ag2(._22(Region, Regions), Colors)

The argument filtering Pi contains the following mapping:
color_map_2_in_ag2(x1, x2)  =  color_map_2_in_ag1(x2)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
region_33(x1, x2, x3)  =  region_32(x2, x3)
if_color_map_2_in_1_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_1_ag2(x3, x4)
color_region_2_in_ag2(x1, x2)  =  color_region_2_in_ag1(x2)
if_color_region_2_in_1_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_1_ag2(x4, x5)
select_3_in_aga3(x1, x2, x3)  =  select_3_in_aga1(x2)
select_3_out_aga3(x1, x2, x3)  =  select_3_out_aga3(x1, x2, x3)
if_select_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_select_3_in_1_aga3(x2, x3, x5)
if_color_region_2_in_2_ag6(x1, x2, x3, x4, x5, x6)  =  if_color_region_2_in_2_ag3(x2, x4, x6)
members_2_in_ag2(x1, x2)  =  members_2_in_ag1(x2)
if_members_2_in_1_ag4(x1, x2, x3, x4)  =  if_members_2_in_1_ag2(x3, x4)
member_2_in_ag2(x1, x2)  =  member_2_in_ag1(x2)
member_2_out_ag2(x1, x2)  =  member_2_out_ag2(x1, x2)
if_member_2_in_1_ag4(x1, x2, x3, x4)  =  if_member_2_in_1_ag3(x2, x3, x4)
if_members_2_in_2_ag4(x1, x2, x3, x4)  =  if_members_2_in_2_ag3(x1, x3, x4)
members_2_out_ag2(x1, x2)  =  members_2_out_ag2(x1, x2)
color_region_2_out_ag2(x1, x2)  =  color_region_2_out_ag2(x1, x2)
if_color_map_2_in_2_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_2_ag3(x1, x3, x4)
color_map_2_out_ag2(x1, x2)  =  color_map_2_out_ag2(x1, x2)
IF_MEMBERS_2_IN_1_AG4(x1, x2, x3, x4)  =  IF_MEMBERS_2_IN_1_AG2(x3, x4)
MEMBERS_2_IN_AG2(x1, x2)  =  MEMBERS_2_IN_AG1(x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

MEMBERS_2_IN_AG2(._22(X, Xs), Ys) -> IF_MEMBERS_2_IN_1_AG4(X, Xs, Ys, member_2_in_ag2(X, Ys))
IF_MEMBERS_2_IN_1_AG4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> MEMBERS_2_IN_AG2(Xs, Ys)

The TRS R consists of the following rules:

member_2_in_ag2(X, ._22(X, underscore)) -> member_2_out_ag2(X, ._22(X, underscore))
member_2_in_ag2(X, ._22(underscore1, Xs)) -> if_member_2_in_1_ag4(X, underscore1, Xs, member_2_in_ag2(X, Xs))
if_member_2_in_1_ag4(X, underscore1, Xs, member_2_out_ag2(X, Xs)) -> member_2_out_ag2(X, ._22(underscore1, Xs))

The argument filtering Pi contains the following mapping:
._22(x1, x2)  =  ._22(x1, x2)
member_2_in_ag2(x1, x2)  =  member_2_in_ag1(x2)
member_2_out_ag2(x1, x2)  =  member_2_out_ag2(x1, x2)
if_member_2_in_1_ag4(x1, x2, x3, x4)  =  if_member_2_in_1_ag3(x2, x3, x4)
IF_MEMBERS_2_IN_1_AG4(x1, x2, x3, x4)  =  IF_MEMBERS_2_IN_1_AG2(x3, x4)
MEMBERS_2_IN_AG2(x1, x2)  =  MEMBERS_2_IN_AG1(x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
QDP
              ↳ PiDP
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

MEMBERS_2_IN_AG1(Ys) -> IF_MEMBERS_2_IN_1_AG2(Ys, member_2_in_ag1(Ys))
IF_MEMBERS_2_IN_1_AG2(Ys, member_2_out_ag2(X, Ys)) -> MEMBERS_2_IN_AG1(Ys)

The TRS R consists of the following rules:

member_2_in_ag1(._22(X, underscore)) -> member_2_out_ag2(X, ._22(X, underscore))
member_2_in_ag1(._22(underscore1, Xs)) -> if_member_2_in_1_ag3(underscore1, Xs, member_2_in_ag1(Xs))
if_member_2_in_1_ag3(underscore1, Xs, member_2_out_ag2(X, Xs)) -> member_2_out_ag2(X, ._22(underscore1, Xs))

The set Q consists of the following terms:

member_2_in_ag1(x0)
if_member_2_in_1_ag3(x0, x1, x2)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_MEMBERS_2_IN_1_AG2, MEMBERS_2_IN_AG1}.

↳ PROLOG
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
PiDP
                ↳ UsableRulesProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

SELECT_3_IN_AGA3(X, ._22(Y, Ys), ._22(Y, Zs)) -> SELECT_3_IN_AGA3(X, Ys, Zs)

The TRS R consists of the following rules:

color_map_2_in_ag2(._22(Region, Regions), Colors) -> if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_in_ag2(Region, Colors))
color_region_2_in_ag2(region_33(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_in_aga3(Color, Colors, Colors1))
select_3_in_aga3(X, ._22(X, Xs), Xs) -> select_3_out_aga3(X, ._22(X, Xs), Xs)
select_3_in_aga3(X, ._22(Y, Ys), ._22(Y, Zs)) -> if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_in_aga3(X, Ys, Zs))
if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_out_aga3(X, Ys, Zs)) -> select_3_out_aga3(X, ._22(Y, Ys), ._22(Y, Zs))
if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag2(Neighbors, Colors1))
members_2_in_ag2(._22(X, Xs), Ys) -> if_members_2_in_1_ag4(X, Xs, Ys, member_2_in_ag2(X, Ys))
member_2_in_ag2(X, ._22(X, underscore)) -> member_2_out_ag2(X, ._22(X, underscore))
member_2_in_ag2(X, ._22(underscore1, Xs)) -> if_member_2_in_1_ag4(X, underscore1, Xs, member_2_in_ag2(X, Xs))
if_member_2_in_1_ag4(X, underscore1, Xs, member_2_out_ag2(X, Xs)) -> member_2_out_ag2(X, ._22(underscore1, Xs))
if_members_2_in_1_ag4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> if_members_2_in_2_ag4(X, Xs, Ys, members_2_in_ag2(Xs, Ys))
members_2_in_ag2([]_0, Ys) -> members_2_out_ag2([]_0, Ys)
if_members_2_in_2_ag4(X, Xs, Ys, members_2_out_ag2(Xs, Ys)) -> members_2_out_ag2(._22(X, Xs), Ys)
if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_33(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_in_ag2(Regions, Colors))
color_map_2_in_ag2([]_0, Colors) -> color_map_2_out_ag2([]_0, Colors)
if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_out_ag2(Regions, Colors)) -> color_map_2_out_ag2(._22(Region, Regions), Colors)

The argument filtering Pi contains the following mapping:
color_map_2_in_ag2(x1, x2)  =  color_map_2_in_ag1(x2)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
region_33(x1, x2, x3)  =  region_32(x2, x3)
if_color_map_2_in_1_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_1_ag2(x3, x4)
color_region_2_in_ag2(x1, x2)  =  color_region_2_in_ag1(x2)
if_color_region_2_in_1_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_1_ag2(x4, x5)
select_3_in_aga3(x1, x2, x3)  =  select_3_in_aga1(x2)
select_3_out_aga3(x1, x2, x3)  =  select_3_out_aga3(x1, x2, x3)
if_select_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_select_3_in_1_aga3(x2, x3, x5)
if_color_region_2_in_2_ag6(x1, x2, x3, x4, x5, x6)  =  if_color_region_2_in_2_ag3(x2, x4, x6)
members_2_in_ag2(x1, x2)  =  members_2_in_ag1(x2)
if_members_2_in_1_ag4(x1, x2, x3, x4)  =  if_members_2_in_1_ag2(x3, x4)
member_2_in_ag2(x1, x2)  =  member_2_in_ag1(x2)
member_2_out_ag2(x1, x2)  =  member_2_out_ag2(x1, x2)
if_member_2_in_1_ag4(x1, x2, x3, x4)  =  if_member_2_in_1_ag3(x2, x3, x4)
if_members_2_in_2_ag4(x1, x2, x3, x4)  =  if_members_2_in_2_ag3(x1, x3, x4)
members_2_out_ag2(x1, x2)  =  members_2_out_ag2(x1, x2)
color_region_2_out_ag2(x1, x2)  =  color_region_2_out_ag2(x1, x2)
if_color_map_2_in_2_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_2_ag3(x1, x3, x4)
color_map_2_out_ag2(x1, x2)  =  color_map_2_out_ag2(x1, x2)
SELECT_3_IN_AGA3(x1, x2, x3)  =  SELECT_3_IN_AGA1(x2)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
PiDP
                    ↳ PiDPToQDPProof
              ↳ PiDP

Pi DP problem:
The TRS P consists of the following rules:

SELECT_3_IN_AGA3(X, ._22(Y, Ys), ._22(Y, Zs)) -> SELECT_3_IN_AGA3(X, Ys, Zs)

R is empty.
The argument filtering Pi contains the following mapping:
._22(x1, x2)  =  ._22(x1, x2)
SELECT_3_IN_AGA3(x1, x2, x3)  =  SELECT_3_IN_AGA1(x2)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP

Q DP problem:
The TRS P consists of the following rules:

SELECT_3_IN_AGA1(._22(Y, Ys)) -> SELECT_3_IN_AGA1(Ys)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {SELECT_3_IN_AGA1}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ PROLOG
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
PiDP
                ↳ UsableRulesProof

Pi DP problem:
The TRS P consists of the following rules:

COLOR_MAP_2_IN_AG2(._22(Region, Regions), Colors) -> IF_COLOR_MAP_2_IN_1_AG4(Region, Regions, Colors, color_region_2_in_ag2(Region, Colors))
IF_COLOR_MAP_2_IN_1_AG4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> COLOR_MAP_2_IN_AG2(Regions, Colors)

The TRS R consists of the following rules:

color_map_2_in_ag2(._22(Region, Regions), Colors) -> if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_in_ag2(Region, Colors))
color_region_2_in_ag2(region_33(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_in_aga3(Color, Colors, Colors1))
select_3_in_aga3(X, ._22(X, Xs), Xs) -> select_3_out_aga3(X, ._22(X, Xs), Xs)
select_3_in_aga3(X, ._22(Y, Ys), ._22(Y, Zs)) -> if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_in_aga3(X, Ys, Zs))
if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_out_aga3(X, Ys, Zs)) -> select_3_out_aga3(X, ._22(Y, Ys), ._22(Y, Zs))
if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag2(Neighbors, Colors1))
members_2_in_ag2(._22(X, Xs), Ys) -> if_members_2_in_1_ag4(X, Xs, Ys, member_2_in_ag2(X, Ys))
member_2_in_ag2(X, ._22(X, underscore)) -> member_2_out_ag2(X, ._22(X, underscore))
member_2_in_ag2(X, ._22(underscore1, Xs)) -> if_member_2_in_1_ag4(X, underscore1, Xs, member_2_in_ag2(X, Xs))
if_member_2_in_1_ag4(X, underscore1, Xs, member_2_out_ag2(X, Xs)) -> member_2_out_ag2(X, ._22(underscore1, Xs))
if_members_2_in_1_ag4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> if_members_2_in_2_ag4(X, Xs, Ys, members_2_in_ag2(Xs, Ys))
members_2_in_ag2([]_0, Ys) -> members_2_out_ag2([]_0, Ys)
if_members_2_in_2_ag4(X, Xs, Ys, members_2_out_ag2(Xs, Ys)) -> members_2_out_ag2(._22(X, Xs), Ys)
if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_33(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_in_ag2(Regions, Colors))
color_map_2_in_ag2([]_0, Colors) -> color_map_2_out_ag2([]_0, Colors)
if_color_map_2_in_2_ag4(Region, Regions, Colors, color_map_2_out_ag2(Regions, Colors)) -> color_map_2_out_ag2(._22(Region, Regions), Colors)

The argument filtering Pi contains the following mapping:
color_map_2_in_ag2(x1, x2)  =  color_map_2_in_ag1(x2)
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
region_33(x1, x2, x3)  =  region_32(x2, x3)
if_color_map_2_in_1_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_1_ag2(x3, x4)
color_region_2_in_ag2(x1, x2)  =  color_region_2_in_ag1(x2)
if_color_region_2_in_1_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_1_ag2(x4, x5)
select_3_in_aga3(x1, x2, x3)  =  select_3_in_aga1(x2)
select_3_out_aga3(x1, x2, x3)  =  select_3_out_aga3(x1, x2, x3)
if_select_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_select_3_in_1_aga3(x2, x3, x5)
if_color_region_2_in_2_ag6(x1, x2, x3, x4, x5, x6)  =  if_color_region_2_in_2_ag3(x2, x4, x6)
members_2_in_ag2(x1, x2)  =  members_2_in_ag1(x2)
if_members_2_in_1_ag4(x1, x2, x3, x4)  =  if_members_2_in_1_ag2(x3, x4)
member_2_in_ag2(x1, x2)  =  member_2_in_ag1(x2)
member_2_out_ag2(x1, x2)  =  member_2_out_ag2(x1, x2)
if_member_2_in_1_ag4(x1, x2, x3, x4)  =  if_member_2_in_1_ag3(x2, x3, x4)
if_members_2_in_2_ag4(x1, x2, x3, x4)  =  if_members_2_in_2_ag3(x1, x3, x4)
members_2_out_ag2(x1, x2)  =  members_2_out_ag2(x1, x2)
color_region_2_out_ag2(x1, x2)  =  color_region_2_out_ag2(x1, x2)
if_color_map_2_in_2_ag4(x1, x2, x3, x4)  =  if_color_map_2_in_2_ag3(x1, x3, x4)
color_map_2_out_ag2(x1, x2)  =  color_map_2_out_ag2(x1, x2)
COLOR_MAP_2_IN_AG2(x1, x2)  =  COLOR_MAP_2_IN_AG1(x2)
IF_COLOR_MAP_2_IN_1_AG4(x1, x2, x3, x4)  =  IF_COLOR_MAP_2_IN_1_AG2(x3, x4)

We have to consider all (P,R,Pi)-chains
For (infinitary) constructor rewriting we can delete all non-usable rules from R.

↳ PROLOG
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
PiDP
                    ↳ PiDPToQDPProof

Pi DP problem:
The TRS P consists of the following rules:

COLOR_MAP_2_IN_AG2(._22(Region, Regions), Colors) -> IF_COLOR_MAP_2_IN_1_AG4(Region, Regions, Colors, color_region_2_in_ag2(Region, Colors))
IF_COLOR_MAP_2_IN_1_AG4(Region, Regions, Colors, color_region_2_out_ag2(Region, Colors)) -> COLOR_MAP_2_IN_AG2(Regions, Colors)

The TRS R consists of the following rules:

color_region_2_in_ag2(region_33(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_in_aga3(Color, Colors, Colors1))
if_color_region_2_in_1_ag5(Name, Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag2(Neighbors, Colors1))
select_3_in_aga3(X, ._22(X, Xs), Xs) -> select_3_out_aga3(X, ._22(X, Xs), Xs)
select_3_in_aga3(X, ._22(Y, Ys), ._22(Y, Zs)) -> if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_in_aga3(X, Ys, Zs))
if_color_region_2_in_2_ag6(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_33(Name, Color, Neighbors), Colors)
if_select_3_in_1_aga5(X, Y, Ys, Zs, select_3_out_aga3(X, Ys, Zs)) -> select_3_out_aga3(X, ._22(Y, Ys), ._22(Y, Zs))
members_2_in_ag2(._22(X, Xs), Ys) -> if_members_2_in_1_ag4(X, Xs, Ys, member_2_in_ag2(X, Ys))
members_2_in_ag2([]_0, Ys) -> members_2_out_ag2([]_0, Ys)
if_members_2_in_1_ag4(X, Xs, Ys, member_2_out_ag2(X, Ys)) -> if_members_2_in_2_ag4(X, Xs, Ys, members_2_in_ag2(Xs, Ys))
member_2_in_ag2(X, ._22(X, underscore)) -> member_2_out_ag2(X, ._22(X, underscore))
member_2_in_ag2(X, ._22(underscore1, Xs)) -> if_member_2_in_1_ag4(X, underscore1, Xs, member_2_in_ag2(X, Xs))
if_members_2_in_2_ag4(X, Xs, Ys, members_2_out_ag2(Xs, Ys)) -> members_2_out_ag2(._22(X, Xs), Ys)
if_member_2_in_1_ag4(X, underscore1, Xs, member_2_out_ag2(X, Xs)) -> member_2_out_ag2(X, ._22(underscore1, Xs))

The argument filtering Pi contains the following mapping:
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
region_33(x1, x2, x3)  =  region_32(x2, x3)
color_region_2_in_ag2(x1, x2)  =  color_region_2_in_ag1(x2)
if_color_region_2_in_1_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_1_ag2(x4, x5)
select_3_in_aga3(x1, x2, x3)  =  select_3_in_aga1(x2)
select_3_out_aga3(x1, x2, x3)  =  select_3_out_aga3(x1, x2, x3)
if_select_3_in_1_aga5(x1, x2, x3, x4, x5)  =  if_select_3_in_1_aga3(x2, x3, x5)
if_color_region_2_in_2_ag6(x1, x2, x3, x4, x5, x6)  =  if_color_region_2_in_2_ag3(x2, x4, x6)
members_2_in_ag2(x1, x2)  =  members_2_in_ag1(x2)
if_members_2_in_1_ag4(x1, x2, x3, x4)  =  if_members_2_in_1_ag2(x3, x4)
member_2_in_ag2(x1, x2)  =  member_2_in_ag1(x2)
member_2_out_ag2(x1, x2)  =  member_2_out_ag2(x1, x2)
if_member_2_in_1_ag4(x1, x2, x3, x4)  =  if_member_2_in_1_ag3(x2, x3, x4)
if_members_2_in_2_ag4(x1, x2, x3, x4)  =  if_members_2_in_2_ag3(x1, x3, x4)
members_2_out_ag2(x1, x2)  =  members_2_out_ag2(x1, x2)
color_region_2_out_ag2(x1, x2)  =  color_region_2_out_ag2(x1, x2)
COLOR_MAP_2_IN_AG2(x1, x2)  =  COLOR_MAP_2_IN_AG1(x2)
IF_COLOR_MAP_2_IN_1_AG4(x1, x2, x3, x4)  =  IF_COLOR_MAP_2_IN_1_AG2(x3, x4)

We have to consider all (P,R,Pi)-chains
Transforming (infinitary) constructor rewriting Pi-DP problem into ordinary QDP problem by application of Pi.

↳ PROLOG
  ↳ PrologToPiTRSProof
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof
            ↳ AND
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
              ↳ PiDP
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
QDP

Q DP problem:
The TRS P consists of the following rules:

COLOR_MAP_2_IN_AG1(Colors) -> IF_COLOR_MAP_2_IN_1_AG2(Colors, color_region_2_in_ag1(Colors))
IF_COLOR_MAP_2_IN_1_AG2(Colors, color_region_2_out_ag2(Region, Colors)) -> COLOR_MAP_2_IN_AG1(Colors)

The TRS R consists of the following rules:

color_region_2_in_ag1(Colors) -> if_color_region_2_in_1_ag2(Colors, select_3_in_aga1(Colors))
if_color_region_2_in_1_ag2(Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag3(Color, Colors, members_2_in_ag1(Colors1))
select_3_in_aga1(._22(X, Xs)) -> select_3_out_aga3(X, ._22(X, Xs), Xs)
select_3_in_aga1(._22(Y, Ys)) -> if_select_3_in_1_aga3(Y, Ys, select_3_in_aga1(Ys))
if_color_region_2_in_2_ag3(Color, Colors, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_32(Color, Neighbors), Colors)
if_select_3_in_1_aga3(Y, Ys, select_3_out_aga3(X, Ys, Zs)) -> select_3_out_aga3(X, ._22(Y, Ys), ._22(Y, Zs))
members_2_in_ag1(Ys) -> if_members_2_in_1_ag2(Ys, member_2_in_ag1(Ys))
members_2_in_ag1(Ys) -> members_2_out_ag2([]_0, Ys)
if_members_2_in_1_ag2(Ys, member_2_out_ag2(X, Ys)) -> if_members_2_in_2_ag3(X, Ys, members_2_in_ag1(Ys))
member_2_in_ag1(._22(X, underscore)) -> member_2_out_ag2(X, ._22(X, underscore))
member_2_in_ag1(._22(underscore1, Xs)) -> if_member_2_in_1_ag3(underscore1, Xs, member_2_in_ag1(Xs))
if_members_2_in_2_ag3(X, Ys, members_2_out_ag2(Xs, Ys)) -> members_2_out_ag2(._22(X, Xs), Ys)
if_member_2_in_1_ag3(underscore1, Xs, member_2_out_ag2(X, Xs)) -> member_2_out_ag2(X, ._22(underscore1, Xs))

The set Q consists of the following terms:

color_region_2_in_ag1(x0)
if_color_region_2_in_1_ag2(x0, x1)
select_3_in_aga1(x0)
if_color_region_2_in_2_ag3(x0, x1, x2)
if_select_3_in_1_aga3(x0, x1, x2)
members_2_in_ag1(x0)
if_members_2_in_1_ag2(x0, x1)
member_2_in_ag1(x0)
if_members_2_in_2_ag3(x0, x1, x2)
if_member_2_in_1_ag3(x0, x1, x2)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_COLOR_MAP_2_IN_1_AG2, COLOR_MAP_2_IN_AG1}.