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



↳ PROLOG
  ↳ UnrequestedClauseRemoverProof

colormap2(.2(Region, Regions), Colors) :- colorregion2(Region, Colors), colormap2(Regions, Colors).
colormap2({}0, Colors).
colorregion2(region2(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, T)) :- member2(X, T).
testcolor2(Name, Pairs) :- colors2(Name, Colors), colormap2(Map, Colors), map3(Name, Symbols, Map), symbols3(Symbols, Map, Pairs).
symbols3({}0, {}0, {}0).
symbols3(.2(S, Ss), .2(region2(C, N), Rs), .2(pair2(S, C), Ps)) :- symbols3(Ss, Rs, Ps).
map3(test0, .2(a0, .2(b0, .2(c0, .2(d0, .2(e0, .2(f0, {}0)))))), .2(region2(A, .2(B, .2(C, .2(D, {}0)))), .2(region2(B, .2(A, .2(C, .2(E, {}0)))), .2(region2(C, .2(A, .2(B, .2(D, .2(E, .2(F, {}0)))))), .2(region2(D, .2(A, .2(C, .2(F, {}0)))), .2(region2(E, .2(B, .2(C, .2(F, {}0)))), .2(region2(F, .2(C, .2(D, .2(E, {}0)))), {}0))))))).
map3(westeurope0, .2(portugal0, .2(spain0, .2(france0, .2(belgium0, .2(holland0, .2(westgermany0, .2(luxembourg0, .2(italy0, .2(switzerland0, .2(austria0, {}0)))))))))), .2(region2(P, .2(E, {}0)), .2(region2(E, .2(F, .2(P, {}0))), .2(region2(F, .2(E, .2(I, .2(S, .2(B, .2(WG, .2(L, {}0))))))), .2(region2(B, .2(F, .2(H, .2(L, .2(WG, {}0))))), .2(region2(H, .2(B, .2(WG, {}0))), .2(region2(WG, .2(F, .2(A, .2(S, .2(H, .2(B, .2(L, {}0))))))), .2(region2(L, .2(F, .2(B, .2(WG, {}0)))), .2(region2(I, .2(F, .2(A, .2(S, {}0)))), .2(region2(S, .2(F, .2(I, .2(A, .2(WG, {}0))))), .2(region2(A, .2(I, .2(S, .2(WG, {}0)))), {}0))))))))))).
colors2(X, .2(red0, .2(yellow0, .2(blue0, .2(white0, {}0))))).


The clauses

testcolor2(Name, Pairs) :- colors2(Name, Colors), colormap2(Map, Colors), map3(Name, Symbols, Map), symbols3(Symbols, Map, Pairs).
symbols3({}0, {}0, {}0).
symbols3(.2(S, Ss), .2(region2(C, N), Rs), .2(pair2(S, C), Ps)) :- symbols3(Ss, Rs, Ps).
map3(test0, .2(a0, .2(b0, .2(c0, .2(d0, .2(e0, .2(f0, {}0)))))), .2(region2(A, .2(B, .2(C, .2(D, {}0)))), .2(region2(B, .2(A, .2(C, .2(E, {}0)))), .2(region2(C, .2(A, .2(B, .2(D, .2(E, .2(F, {}0)))))), .2(region2(D, .2(A, .2(C, .2(F, {}0)))), .2(region2(E, .2(B, .2(C, .2(F, {}0)))), .2(region2(F, .2(C, .2(D, .2(E, {}0)))), {}0))))))).
map3(westeurope0, .2(portugal0, .2(spain0, .2(france0, .2(belgium0, .2(holland0, .2(westgermany0, .2(luxembourg0, .2(italy0, .2(switzerland0, .2(austria0, {}0)))))))))), .2(region2(P, .2(E, {}0)), .2(region2(E, .2(F, .2(P, {}0))), .2(region2(F, .2(E, .2(I, .2(S, .2(B, .2(WG, .2(L, {}0))))))), .2(region2(B, .2(F, .2(H, .2(L, .2(WG, {}0))))), .2(region2(H, .2(B, .2(WG, {}0))), .2(region2(WG, .2(F, .2(A, .2(S, .2(H, .2(B, .2(L, {}0))))))), .2(region2(L, .2(F, .2(B, .2(WG, {}0)))), .2(region2(I, .2(F, .2(A, .2(S, {}0)))), .2(region2(S, .2(F, .2(I, .2(A, .2(WG, {}0))))), .2(region2(A, .2(I, .2(S, .2(WG, {}0)))), {}0))))))))))).
colors2(X, .2(red0, .2(yellow0, .2(blue0, .2(white0, {}0))))).

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

Deleting these clauses results in the following prolog program:

colormap2(.2(Region, Regions), Colors) :- colorregion2(Region, Colors), colormap2(Regions, Colors).
colormap2({}0, Colors).
colorregion2(region2(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, T)) :- member2(X, T).



↳ PROLOG
  ↳ UnrequestedClauseRemoverProof
    ↳ PROLOG
      ↳ PrologToPiTRSProof
      ↳ PrologToPiTRSProof

colormap2(.2(Region, Regions), Colors) :- colorregion2(Region, Colors), colormap2(Regions, Colors).
colormap2({}0, Colors).
colorregion2(region2(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, T)) :- member2(X, T).


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_22(Color, Neighbors), Colors) -> if_color_region_2_in_1_ag4(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_ag4(Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag5(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, T)) -> if_member_2_in_1_ag4(X, underscore1, T, member_2_in_ag2(X, T))
if_member_2_in_1_ag4(X, underscore1, T, member_2_out_ag2(X, T)) -> member_2_out_ag2(X, ._22(underscore1, T))
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_ag5(Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_22(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_22(x1, x2)  =  region_22(x1, x2)
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_ag4(x1, x2, x3, x4)  =  if_color_region_2_in_1_ag1(x4)
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_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_2_ag2(x1, x5)
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
  ↳ UnrequestedClauseRemoverProof
    ↳ 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_22(Color, Neighbors), Colors) -> if_color_region_2_in_1_ag4(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_ag4(Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag5(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, T)) -> if_member_2_in_1_ag4(X, underscore1, T, member_2_in_ag2(X, T))
if_member_2_in_1_ag4(X, underscore1, T, member_2_out_ag2(X, T)) -> member_2_out_ag2(X, ._22(underscore1, T))
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_ag5(Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_22(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_22(x1, x2)  =  region_22(x1, x2)
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_ag4(x1, x2, x3, x4)  =  if_color_region_2_in_1_ag1(x4)
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_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_2_ag2(x1, x5)
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_22(Color, Neighbors), Colors) -> IF_COLOR_REGION_2_IN_1_AG4(Color, Neighbors, Colors, select_3_in_aga3(Color, Colors, Colors1))
COLOR_REGION_2_IN_AG2(region_22(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_AG4(Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> IF_COLOR_REGION_2_IN_2_AG5(Color, Neighbors, Colors, Colors1, members_2_in_ag2(Neighbors, Colors1))
IF_COLOR_REGION_2_IN_1_AG4(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, T)) -> IF_MEMBER_2_IN_1_AG4(X, underscore1, T, member_2_in_ag2(X, T))
MEMBER_2_IN_AG2(X, ._22(underscore1, T)) -> MEMBER_2_IN_AG2(X, T)
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_22(Color, Neighbors), Colors) -> if_color_region_2_in_1_ag4(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_ag4(Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag5(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, T)) -> if_member_2_in_1_ag4(X, underscore1, T, member_2_in_ag2(X, T))
if_member_2_in_1_ag4(X, underscore1, T, member_2_out_ag2(X, T)) -> member_2_out_ag2(X, ._22(underscore1, T))
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_ag5(Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_22(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_22(x1, x2)  =  region_22(x1, x2)
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_ag4(x1, x2, x3, x4)  =  if_color_region_2_in_1_ag1(x4)
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_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_2_ag2(x1, x5)
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)
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)
IF_COLOR_REGION_2_IN_1_AG4(x1, x2, x3, x4)  =  IF_COLOR_REGION_2_IN_1_AG1(x4)
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)
IF_COLOR_REGION_2_IN_2_AG5(x1, x2, x3, x4, x5)  =  IF_COLOR_REGION_2_IN_2_AG2(x1, x5)
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)
SELECT_3_IN_AGA3(x1, x2, x3)  =  SELECT_3_IN_AGA1(x2)

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

↳ PROLOG
  ↳ UnrequestedClauseRemoverProof
    ↳ 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_22(Color, Neighbors), Colors) -> IF_COLOR_REGION_2_IN_1_AG4(Color, Neighbors, Colors, select_3_in_aga3(Color, Colors, Colors1))
COLOR_REGION_2_IN_AG2(region_22(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_AG4(Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> IF_COLOR_REGION_2_IN_2_AG5(Color, Neighbors, Colors, Colors1, members_2_in_ag2(Neighbors, Colors1))
IF_COLOR_REGION_2_IN_1_AG4(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, T)) -> IF_MEMBER_2_IN_1_AG4(X, underscore1, T, member_2_in_ag2(X, T))
MEMBER_2_IN_AG2(X, ._22(underscore1, T)) -> MEMBER_2_IN_AG2(X, T)
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_22(Color, Neighbors), Colors) -> if_color_region_2_in_1_ag4(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_ag4(Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag5(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, T)) -> if_member_2_in_1_ag4(X, underscore1, T, member_2_in_ag2(X, T))
if_member_2_in_1_ag4(X, underscore1, T, member_2_out_ag2(X, T)) -> member_2_out_ag2(X, ._22(underscore1, T))
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_ag5(Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_22(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_22(x1, x2)  =  region_22(x1, x2)
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_ag4(x1, x2, x3, x4)  =  if_color_region_2_in_1_ag1(x4)
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_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_2_ag2(x1, x5)
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)
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)
IF_COLOR_REGION_2_IN_1_AG4(x1, x2, x3, x4)  =  IF_COLOR_REGION_2_IN_1_AG1(x4)
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)
IF_COLOR_REGION_2_IN_2_AG5(x1, x2, x3, x4, x5)  =  IF_COLOR_REGION_2_IN_2_AG2(x1, x5)
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)
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
  ↳ UnrequestedClauseRemoverProof
    ↳ 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, T)) -> MEMBER_2_IN_AG2(X, T)

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_22(Color, Neighbors), Colors) -> if_color_region_2_in_1_ag4(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_ag4(Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag5(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, T)) -> if_member_2_in_1_ag4(X, underscore1, T, member_2_in_ag2(X, T))
if_member_2_in_1_ag4(X, underscore1, T, member_2_out_ag2(X, T)) -> member_2_out_ag2(X, ._22(underscore1, T))
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_ag5(Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_22(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_22(x1, x2)  =  region_22(x1, x2)
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_ag4(x1, x2, x3, x4)  =  if_color_region_2_in_1_ag1(x4)
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_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_2_ag2(x1, x5)
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
  ↳ UnrequestedClauseRemoverProof
    ↳ 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, T)) -> MEMBER_2_IN_AG2(X, T)

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
  ↳ UnrequestedClauseRemoverProof
    ↳ 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, T)) -> MEMBER_2_IN_AG1(T)

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
  ↳ UnrequestedClauseRemoverProof
    ↳ 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_22(Color, Neighbors), Colors) -> if_color_region_2_in_1_ag4(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_ag4(Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag5(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, T)) -> if_member_2_in_1_ag4(X, underscore1, T, member_2_in_ag2(X, T))
if_member_2_in_1_ag4(X, underscore1, T, member_2_out_ag2(X, T)) -> member_2_out_ag2(X, ._22(underscore1, T))
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_ag5(Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_22(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_22(x1, x2)  =  region_22(x1, x2)
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_ag4(x1, x2, x3, x4)  =  if_color_region_2_in_1_ag1(x4)
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_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_2_ag2(x1, x5)
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
  ↳ UnrequestedClauseRemoverProof
    ↳ 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, T)) -> if_member_2_in_1_ag4(X, underscore1, T, member_2_in_ag2(X, T))
if_member_2_in_1_ag4(X, underscore1, T, member_2_out_ag2(X, T)) -> member_2_out_ag2(X, ._22(underscore1, T))

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
  ↳ UnrequestedClauseRemoverProof
    ↳ 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, T)) -> if_member_2_in_1_ag1(member_2_in_ag1(T))
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
  ↳ UnrequestedClauseRemoverProof
    ↳ 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_22(Color, Neighbors), Colors) -> if_color_region_2_in_1_ag4(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_ag4(Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag5(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, T)) -> if_member_2_in_1_ag4(X, underscore1, T, member_2_in_ag2(X, T))
if_member_2_in_1_ag4(X, underscore1, T, member_2_out_ag2(X, T)) -> member_2_out_ag2(X, ._22(underscore1, T))
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_ag5(Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_22(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_22(x1, x2)  =  region_22(x1, x2)
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_ag4(x1, x2, x3, x4)  =  if_color_region_2_in_1_ag1(x4)
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_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_2_ag2(x1, x5)
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
  ↳ UnrequestedClauseRemoverProof
    ↳ 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
  ↳ UnrequestedClauseRemoverProof
    ↳ 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
  ↳ UnrequestedClauseRemoverProof
    ↳ 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_22(Color, Neighbors), Colors) -> if_color_region_2_in_1_ag4(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_ag4(Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag5(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, T)) -> if_member_2_in_1_ag4(X, underscore1, T, member_2_in_ag2(X, T))
if_member_2_in_1_ag4(X, underscore1, T, member_2_out_ag2(X, T)) -> member_2_out_ag2(X, ._22(underscore1, T))
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_ag5(Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_22(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_22(x1, x2)  =  region_22(x1, x2)
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_ag4(x1, x2, x3, x4)  =  if_color_region_2_in_1_ag1(x4)
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_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_2_ag2(x1, x5)
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
  ↳ UnrequestedClauseRemoverProof
    ↳ 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_22(Color, Neighbors), Colors) -> if_color_region_2_in_1_ag4(Color, Neighbors, Colors, select_3_in_aga3(Color, Colors, Colors1))
if_color_region_2_in_1_ag4(Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag5(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_ag5(Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_22(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, T)) -> if_member_2_in_1_ag4(X, underscore1, T, member_2_in_ag2(X, T))
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, T, member_2_out_ag2(X, T)) -> member_2_out_ag2(X, ._22(underscore1, T))

The argument filtering Pi contains the following mapping:
._22(x1, x2)  =  ._22(x1, x2)
[]_0  =  []_0
region_22(x1, x2)  =  region_22(x1, x2)
color_region_2_in_ag2(x1, x2)  =  color_region_2_in_ag1(x2)
if_color_region_2_in_1_ag4(x1, x2, x3, x4)  =  if_color_region_2_in_1_ag1(x4)
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_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_2_ag2(x1, x5)
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
  ↳ UnrequestedClauseRemoverProof
    ↳ 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_22(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, T)) -> if_member_2_in_1_ag1(member_2_in_ag1(T))
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_22(Color, Neighbors), Colors) -> if_color_region_2_in_1_ag4(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_ag4(Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag5(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, T)) -> if_member_2_in_1_ag4(X, underscore1, T, member_2_in_ag2(X, T))
if_member_2_in_1_ag4(X, underscore1, T, member_2_out_ag2(X, T)) -> member_2_out_ag2(X, ._22(underscore1, T))
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_ag5(Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_22(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_22(x1, x2)  =  region_22(x1, x2)
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_ag4(x1, x2, x3, x4)  =  if_color_region_2_in_1_ag2(x3, x4)
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_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_2_ag3(x1, x3, x5)
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
  ↳ UnrequestedClauseRemoverProof
    ↳ PROLOG
      ↳ PrologToPiTRSProof
      ↳ PrologToPiTRSProof
        ↳ PiTRS

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_22(Color, Neighbors), Colors) -> if_color_region_2_in_1_ag4(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_ag4(Color, Neighbors, Colors, select_3_out_aga3(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag5(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, T)) -> if_member_2_in_1_ag4(X, underscore1, T, member_2_in_ag2(X, T))
if_member_2_in_1_ag4(X, underscore1, T, member_2_out_ag2(X, T)) -> member_2_out_ag2(X, ._22(underscore1, T))
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_ag5(Color, Neighbors, Colors, Colors1, members_2_out_ag2(Neighbors, Colors1)) -> color_region_2_out_ag2(region_22(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_22(x1, x2)  =  region_22(x1, x2)
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_ag4(x1, x2, x3, x4)  =  if_color_region_2_in_1_ag2(x3, x4)
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_ag5(x1, x2, x3, x4, x5)  =  if_color_region_2_in_2_ag3(x1, x3, x5)
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)