Left Termination proof of /tmp/tmp90Bmdk/mapcolor.pl

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

↳ PROLOG

  ↳ PrologToPiTRSProof

  ↳ PrologToPiTRSProof

color_map₂(.₂(Region, Regions), Colors) :- color_region₂(Region, Colors), color_map₂(Regions, Colors).
color_map₂({}₀, Colors).
color_region₂(region₃(Name, Color, Neighbors), Colors) :- select₃(Color, Colors, Colors1), members₂(Neighbors, Colors1).
select₃(X, .₂(X, Xs), Xs).
select₃(X, .₂(Y, Ys), .₂(Y, Zs)) :- select₃(X, Ys, Zs).
members₂(.₂(X, Xs), Ys) :- member₂(X, Ys), members₂(Xs, Ys).
members₂({}₀, Ys).
member₂(X, .₂(X, underscore)).
member₂(X, .₂(underscore1, Xs)) :- member₂(X, Xs).

With regard to the inferred argument filtering the predicates were used in the following modes:
color_map₂: (f,b)
color_region₂: (f,b)
select₃: (f,b,f)
members₂: (f,b)
member₂: (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_ag₂(._2₂(Region, Regions), Colors) -> if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_in_ag₂(Region, Colors))
color_region_2_in_ag₂(region_3₃(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_in_aga₃(Color, Colors, Colors1))
select_3_in_aga₃(X, ._2₂(X, Xs), Xs) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
select_3_in_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_in_aga₃(X, Ys, Zs))
if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_out_aga₃(X, Ys, Zs)) -> select_3_out_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs))
if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_out_aga₃(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag₂(Neighbors, Colors1))
members_2_in_ag₂(._2₂(X, Xs), Ys) -> if_members_2_in_1_ag₄(X, Xs, Ys, member_2_in_ag₂(X, Ys))
member_2_in_ag₂(X, ._2₂(X, underscore)) -> member_2_out_ag₂(X, ._2₂(X, underscore))
member_2_in_ag₂(X, ._2₂(underscore1, Xs)) -> if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_in_ag₂(X, Xs))
if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_out_ag₂(X, Xs)) -> member_2_out_ag₂(X, ._2₂(underscore1, Xs))
if_members_2_in_1_ag₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> if_members_2_in_2_ag₄(X, Xs, Ys, members_2_in_ag₂(Xs, Ys))
members_2_in_ag₂([]_0, Ys) -> members_2_out_ag₂([]_0, Ys)
if_members_2_in_2_ag₄(X, Xs, Ys, members_2_out_ag₂(Xs, Ys)) -> members_2_out_ag₂(._2₂(X, Xs), Ys)
if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag₂(Neighbors, Colors1)) -> color_region_2_out_ag₂(region_3₃(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_in_ag₂(Regions, Colors))
color_map_2_in_ag₂([]_0, Colors) -> color_map_2_out_ag₂([]_0, Colors)
if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_out_ag₂(Regions, Colors)) -> color_map_2_out_ag₂(._2₂(Region, Regions), Colors)

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_ag₂(._2₂(Region, Regions), Colors) -> if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_in_ag₂(Region, Colors))
color_region_2_in_ag₂(region_3₃(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_in_aga₃(Color, Colors, Colors1))
select_3_in_aga₃(X, ._2₂(X, Xs), Xs) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
select_3_in_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_in_aga₃(X, Ys, Zs))
if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_out_aga₃(X, Ys, Zs)) -> select_3_out_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs))
if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_out_aga₃(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag₂(Neighbors, Colors1))
members_2_in_ag₂(._2₂(X, Xs), Ys) -> if_members_2_in_1_ag₄(X, Xs, Ys, member_2_in_ag₂(X, Ys))
member_2_in_ag₂(X, ._2₂(X, underscore)) -> member_2_out_ag₂(X, ._2₂(X, underscore))
member_2_in_ag₂(X, ._2₂(underscore1, Xs)) -> if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_in_ag₂(X, Xs))
if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_out_ag₂(X, Xs)) -> member_2_out_ag₂(X, ._2₂(underscore1, Xs))
if_members_2_in_1_ag₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> if_members_2_in_2_ag₄(X, Xs, Ys, members_2_in_ag₂(Xs, Ys))
members_2_in_ag₂([]_0, Ys) -> members_2_out_ag₂([]_0, Ys)
if_members_2_in_2_ag₄(X, Xs, Ys, members_2_out_ag₂(Xs, Ys)) -> members_2_out_ag₂(._2₂(X, Xs), Ys)
if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag₂(Neighbors, Colors1)) -> color_region_2_out_ag₂(region_3₃(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_in_ag₂(Regions, Colors))
color_map_2_in_ag₂([]_0, Colors) -> color_map_2_out_ag₂([]_0, Colors)
if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_out_ag₂(Regions, Colors)) -> color_map_2_out_ag₂(._2₂(Region, Regions), Colors)

COLOR_MAP_2_IN_AG₂(._2₂(Region, Regions), Colors) -> IF_COLOR_MAP_2_IN_1_AG₄(Region, Regions, Colors, color_region_2_in_ag₂(Region, Colors))
COLOR_MAP_2_IN_AG₂(._2₂(Region, Regions), Colors) -> COLOR_REGION_2_IN_AG₂(Region, Colors)
COLOR_REGION_2_IN_AG₂(region_3₃(Name, Color, Neighbors), Colors) -> IF_COLOR_REGION_2_IN_1_AG₅(Name, Color, Neighbors, Colors, select_3_in_aga₃(Color, Colors, Colors1))
COLOR_REGION_2_IN_AG₂(region_3₃(Name, Color, Neighbors), Colors) -> SELECT_3_IN_AGA₃(Color, Colors, Colors1)
SELECT_3_IN_AGA₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> IF_SELECT_3_IN_1_AGA₅(X, Y, Ys, Zs, select_3_in_aga₃(X, Ys, Zs))
SELECT_3_IN_AGA₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> SELECT_3_IN_AGA₃(X, Ys, Zs)
IF_COLOR_REGION_2_IN_1_AG₅(Name, Color, Neighbors, Colors, select_3_out_aga₃(Color, Colors, Colors1)) -> IF_COLOR_REGION_2_IN_2_AG₆(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag₂(Neighbors, Colors1))
IF_COLOR_REGION_2_IN_1_AG₅(Name, Color, Neighbors, Colors, select_3_out_aga₃(Color, Colors, Colors1)) -> MEMBERS_2_IN_AG₂(Neighbors, Colors1)
MEMBERS_2_IN_AG₂(._2₂(X, Xs), Ys) -> IF_MEMBERS_2_IN_1_AG₄(X, Xs, Ys, member_2_in_ag₂(X, Ys))
MEMBERS_2_IN_AG₂(._2₂(X, Xs), Ys) -> MEMBER_2_IN_AG₂(X, Ys)
MEMBER_2_IN_AG₂(X, ._2₂(underscore1, Xs)) -> IF_MEMBER_2_IN_1_AG₄(X, underscore1, Xs, member_2_in_ag₂(X, Xs))
MEMBER_2_IN_AG₂(X, ._2₂(underscore1, Xs)) -> MEMBER_2_IN_AG₂(X, Xs)
IF_MEMBERS_2_IN_1_AG₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> IF_MEMBERS_2_IN_2_AG₄(X, Xs, Ys, members_2_in_ag₂(Xs, Ys))
IF_MEMBERS_2_IN_1_AG₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> MEMBERS_2_IN_AG₂(Xs, Ys)
IF_COLOR_MAP_2_IN_1_AG₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> IF_COLOR_MAP_2_IN_2_AG₄(Region, Regions, Colors, color_map_2_in_ag₂(Regions, Colors))
IF_COLOR_MAP_2_IN_1_AG₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> COLOR_MAP_2_IN_AG₂(Regions, Colors)

The TRS R consists of the following rules:

color_map_2_in_ag₂(._2₂(Region, Regions), Colors) -> if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_in_ag₂(Region, Colors))
color_region_2_in_ag₂(region_3₃(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_in_aga₃(Color, Colors, Colors1))
select_3_in_aga₃(X, ._2₂(X, Xs), Xs) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
select_3_in_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_in_aga₃(X, Ys, Zs))
if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_out_aga₃(X, Ys, Zs)) -> select_3_out_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs))
if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_out_aga₃(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag₂(Neighbors, Colors1))
members_2_in_ag₂(._2₂(X, Xs), Ys) -> if_members_2_in_1_ag₄(X, Xs, Ys, member_2_in_ag₂(X, Ys))
member_2_in_ag₂(X, ._2₂(X, underscore)) -> member_2_out_ag₂(X, ._2₂(X, underscore))
member_2_in_ag₂(X, ._2₂(underscore1, Xs)) -> if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_in_ag₂(X, Xs))
if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_out_ag₂(X, Xs)) -> member_2_out_ag₂(X, ._2₂(underscore1, Xs))
if_members_2_in_1_ag₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> if_members_2_in_2_ag₄(X, Xs, Ys, members_2_in_ag₂(Xs, Ys))
members_2_in_ag₂([]_0, Ys) -> members_2_out_ag₂([]_0, Ys)
if_members_2_in_2_ag₄(X, Xs, Ys, members_2_out_ag₂(Xs, Ys)) -> members_2_out_ag₂(._2₂(X, Xs), Ys)
if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag₂(Neighbors, Colors1)) -> color_region_2_out_ag₂(region_3₃(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_in_ag₂(Regions, Colors))
color_map_2_in_ag₂([]_0, Colors) -> color_map_2_out_ag₂([]_0, Colors)
if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_out_ag₂(Regions, Colors)) -> color_map_2_out_ag₂(._2₂(Region, Regions), Colors)

The argument filtering Pi contains the following mapping:
color_map_2_in_ag₂(x1, x2) = color_map_2_in_ag₁(x2)
._2₂(x1, x2) = ._2₂(x1, x2)
[]_0 = []_0
region_3₃(x1, x2, x3) = region_3₂(x2, x3)
if_color_map_2_in_1_ag₄(x1, x2, x3, x4) = if_color_map_2_in_1_ag₂(x3, x4)
color_region_2_in_ag₂(x1, x2) = color_region_2_in_ag₁(x2)
if_color_region_2_in_1_ag₅(x1, x2, x3, x4, x5) = if_color_region_2_in_1_ag₁(x5)
select_3_in_aga₃(x1, x2, x3) = select_3_in_aga₁(x2)
select_3_out_aga₃(x1, x2, x3) = select_3_out_aga₂(x1, x3)
if_select_3_in_1_aga₅(x1, x2, x3, x4, x5) = if_select_3_in_1_aga₂(x2, x5)
if_color_region_2_in_2_ag₆(x1, x2, x3, x4, x5, x6) = if_color_region_2_in_2_ag₂(x2, x6)
members_2_in_ag₂(x1, x2) = members_2_in_ag₁(x2)
if_members_2_in_1_ag₄(x1, x2, x3, x4) = if_members_2_in_1_ag₂(x3, x4)
member_2_in_ag₂(x1, x2) = member_2_in_ag₁(x2)
member_2_out_ag₂(x1, x2) = member_2_out_ag₁(x1)
if_member_2_in_1_ag₄(x1, x2, x3, x4) = if_member_2_in_1_ag₁(x4)
if_members_2_in_2_ag₄(x1, x2, x3, x4) = if_members_2_in_2_ag₂(x1, x4)
members_2_out_ag₂(x1, x2) = members_2_out_ag₁(x1)
color_region_2_out_ag₂(x1, x2) = color_region_2_out_ag₁(x1)
if_color_map_2_in_2_ag₄(x1, x2, x3, x4) = if_color_map_2_in_2_ag₂(x1, x4)
color_map_2_out_ag₂(x1, x2) = color_map_2_out_ag₁(x1)
IF_COLOR_REGION_2_IN_2_AG₆(x1, x2, x3, x4, x5, x6) = IF_COLOR_REGION_2_IN_2_AG₂(x2, x6)
IF_MEMBERS_2_IN_1_AG₄(x1, x2, x3, x4) = IF_MEMBERS_2_IN_1_AG₂(x3, x4)
IF_MEMBERS_2_IN_2_AG₄(x1, x2, x3, x4) = IF_MEMBERS_2_IN_2_AG₂(x1, x4)
COLOR_MAP_2_IN_AG₂(x1, x2) = COLOR_MAP_2_IN_AG₁(x2)
MEMBERS_2_IN_AG₂(x1, x2) = MEMBERS_2_IN_AG₁(x2)
IF_COLOR_MAP_2_IN_1_AG₄(x1, x2, x3, x4) = IF_COLOR_MAP_2_IN_1_AG₂(x3, x4)
MEMBER_2_IN_AG₂(x1, x2) = MEMBER_2_IN_AG₁(x2)
IF_SELECT_3_IN_1_AGA₅(x1, x2, x3, x4, x5) = IF_SELECT_3_IN_1_AGA₂(x2, x5)
IF_COLOR_MAP_2_IN_2_AG₄(x1, x2, x3, x4) = IF_COLOR_MAP_2_IN_2_AG₂(x1, x4)
COLOR_REGION_2_IN_AG₂(x1, x2) = COLOR_REGION_2_IN_AG₁(x2)
IF_MEMBER_2_IN_1_AG₄(x1, x2, x3, x4) = IF_MEMBER_2_IN_1_AG₁(x4)
IF_COLOR_REGION_2_IN_1_AG₅(x1, x2, x3, x4, x5) = IF_COLOR_REGION_2_IN_1_AG₁(x5)
SELECT_3_IN_AGA₃(x1, x2, x3) = SELECT_3_IN_AGA₁(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_AG₂(._2₂(Region, Regions), Colors) -> IF_COLOR_MAP_2_IN_1_AG₄(Region, Regions, Colors, color_region_2_in_ag₂(Region, Colors))
COLOR_MAP_2_IN_AG₂(._2₂(Region, Regions), Colors) -> COLOR_REGION_2_IN_AG₂(Region, Colors)
COLOR_REGION_2_IN_AG₂(region_3₃(Name, Color, Neighbors), Colors) -> IF_COLOR_REGION_2_IN_1_AG₅(Name, Color, Neighbors, Colors, select_3_in_aga₃(Color, Colors, Colors1))
COLOR_REGION_2_IN_AG₂(region_3₃(Name, Color, Neighbors), Colors) -> SELECT_3_IN_AGA₃(Color, Colors, Colors1)
SELECT_3_IN_AGA₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> IF_SELECT_3_IN_1_AGA₅(X, Y, Ys, Zs, select_3_in_aga₃(X, Ys, Zs))
SELECT_3_IN_AGA₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> SELECT_3_IN_AGA₃(X, Ys, Zs)
IF_COLOR_REGION_2_IN_1_AG₅(Name, Color, Neighbors, Colors, select_3_out_aga₃(Color, Colors, Colors1)) -> IF_COLOR_REGION_2_IN_2_AG₆(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag₂(Neighbors, Colors1))
IF_COLOR_REGION_2_IN_1_AG₅(Name, Color, Neighbors, Colors, select_3_out_aga₃(Color, Colors, Colors1)) -> MEMBERS_2_IN_AG₂(Neighbors, Colors1)
MEMBERS_2_IN_AG₂(._2₂(X, Xs), Ys) -> IF_MEMBERS_2_IN_1_AG₄(X, Xs, Ys, member_2_in_ag₂(X, Ys))
MEMBERS_2_IN_AG₂(._2₂(X, Xs), Ys) -> MEMBER_2_IN_AG₂(X, Ys)
MEMBER_2_IN_AG₂(X, ._2₂(underscore1, Xs)) -> IF_MEMBER_2_IN_1_AG₄(X, underscore1, Xs, member_2_in_ag₂(X, Xs))
MEMBER_2_IN_AG₂(X, ._2₂(underscore1, Xs)) -> MEMBER_2_IN_AG₂(X, Xs)
IF_MEMBERS_2_IN_1_AG₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> IF_MEMBERS_2_IN_2_AG₄(X, Xs, Ys, members_2_in_ag₂(Xs, Ys))
IF_MEMBERS_2_IN_1_AG₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> MEMBERS_2_IN_AG₂(Xs, Ys)
IF_COLOR_MAP_2_IN_1_AG₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> IF_COLOR_MAP_2_IN_2_AG₄(Region, Regions, Colors, color_map_2_in_ag₂(Regions, Colors))
IF_COLOR_MAP_2_IN_1_AG₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> COLOR_MAP_2_IN_AG₂(Regions, Colors)

The TRS R consists of the following rules:

color_map_2_in_ag₂(._2₂(Region, Regions), Colors) -> if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_in_ag₂(Region, Colors))
color_region_2_in_ag₂(region_3₃(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_in_aga₃(Color, Colors, Colors1))
select_3_in_aga₃(X, ._2₂(X, Xs), Xs) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
select_3_in_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_in_aga₃(X, Ys, Zs))
if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_out_aga₃(X, Ys, Zs)) -> select_3_out_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs))
if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_out_aga₃(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag₂(Neighbors, Colors1))
members_2_in_ag₂(._2₂(X, Xs), Ys) -> if_members_2_in_1_ag₄(X, Xs, Ys, member_2_in_ag₂(X, Ys))
member_2_in_ag₂(X, ._2₂(X, underscore)) -> member_2_out_ag₂(X, ._2₂(X, underscore))
member_2_in_ag₂(X, ._2₂(underscore1, Xs)) -> if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_in_ag₂(X, Xs))
if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_out_ag₂(X, Xs)) -> member_2_out_ag₂(X, ._2₂(underscore1, Xs))
if_members_2_in_1_ag₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> if_members_2_in_2_ag₄(X, Xs, Ys, members_2_in_ag₂(Xs, Ys))
members_2_in_ag₂([]_0, Ys) -> members_2_out_ag₂([]_0, Ys)
if_members_2_in_2_ag₄(X, Xs, Ys, members_2_out_ag₂(Xs, Ys)) -> members_2_out_ag₂(._2₂(X, Xs), Ys)
if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag₂(Neighbors, Colors1)) -> color_region_2_out_ag₂(region_3₃(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_in_ag₂(Regions, Colors))
color_map_2_in_ag₂([]_0, Colors) -> color_map_2_out_ag₂([]_0, Colors)
if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_out_ag₂(Regions, Colors)) -> color_map_2_out_ag₂(._2₂(Region, Regions), Colors)

↳ 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_AG₂(X, ._2₂(underscore1, Xs)) -> MEMBER_2_IN_AG₂(X, Xs)

The TRS R consists of the following rules:

color_map_2_in_ag₂(._2₂(Region, Regions), Colors) -> if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_in_ag₂(Region, Colors))
color_region_2_in_ag₂(region_3₃(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_in_aga₃(Color, Colors, Colors1))
select_3_in_aga₃(X, ._2₂(X, Xs), Xs) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
select_3_in_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_in_aga₃(X, Ys, Zs))
if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_out_aga₃(X, Ys, Zs)) -> select_3_out_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs))
if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_out_aga₃(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag₂(Neighbors, Colors1))
members_2_in_ag₂(._2₂(X, Xs), Ys) -> if_members_2_in_1_ag₄(X, Xs, Ys, member_2_in_ag₂(X, Ys))
member_2_in_ag₂(X, ._2₂(X, underscore)) -> member_2_out_ag₂(X, ._2₂(X, underscore))
member_2_in_ag₂(X, ._2₂(underscore1, Xs)) -> if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_in_ag₂(X, Xs))
if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_out_ag₂(X, Xs)) -> member_2_out_ag₂(X, ._2₂(underscore1, Xs))
if_members_2_in_1_ag₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> if_members_2_in_2_ag₄(X, Xs, Ys, members_2_in_ag₂(Xs, Ys))
members_2_in_ag₂([]_0, Ys) -> members_2_out_ag₂([]_0, Ys)
if_members_2_in_2_ag₄(X, Xs, Ys, members_2_out_ag₂(Xs, Ys)) -> members_2_out_ag₂(._2₂(X, Xs), Ys)
if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag₂(Neighbors, Colors1)) -> color_region_2_out_ag₂(region_3₃(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_in_ag₂(Regions, Colors))
color_map_2_in_ag₂([]_0, Colors) -> color_map_2_out_ag₂([]_0, Colors)
if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_out_ag₂(Regions, Colors)) -> color_map_2_out_ag₂(._2₂(Region, Regions), Colors)

↳ 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_AG₂(X, ._2₂(underscore1, Xs)) -> MEMBER_2_IN_AG₂(X, Xs)

R is empty.
The argument filtering Pi contains the following mapping:
._2₂(x1, x2) = ._2₂(x1, x2)
MEMBER_2_IN_AG₂(x1, x2) = MEMBER_2_IN_AG₁(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_AG₁(._2₂(underscore1, Xs)) -> MEMBER_2_IN_AG₁(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_AG₁}.
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:

MEMBER_2_IN_AG₁(._2₂(underscore1, Xs)) -> MEMBER_2_IN_AG₁(Xs)
The graph contains the following edges 1 > 1

↳ 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_AG₂(._2₂(X, Xs), Ys) -> IF_MEMBERS_2_IN_1_AG₄(X, Xs, Ys, member_2_in_ag₂(X, Ys))
IF_MEMBERS_2_IN_1_AG₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> MEMBERS_2_IN_AG₂(Xs, Ys)

The TRS R consists of the following rules:

color_map_2_in_ag₂(._2₂(Region, Regions), Colors) -> if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_in_ag₂(Region, Colors))
color_region_2_in_ag₂(region_3₃(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_in_aga₃(Color, Colors, Colors1))
select_3_in_aga₃(X, ._2₂(X, Xs), Xs) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
select_3_in_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_in_aga₃(X, Ys, Zs))
if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_out_aga₃(X, Ys, Zs)) -> select_3_out_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs))
if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_out_aga₃(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag₂(Neighbors, Colors1))
members_2_in_ag₂(._2₂(X, Xs), Ys) -> if_members_2_in_1_ag₄(X, Xs, Ys, member_2_in_ag₂(X, Ys))
member_2_in_ag₂(X, ._2₂(X, underscore)) -> member_2_out_ag₂(X, ._2₂(X, underscore))
member_2_in_ag₂(X, ._2₂(underscore1, Xs)) -> if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_in_ag₂(X, Xs))
if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_out_ag₂(X, Xs)) -> member_2_out_ag₂(X, ._2₂(underscore1, Xs))
if_members_2_in_1_ag₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> if_members_2_in_2_ag₄(X, Xs, Ys, members_2_in_ag₂(Xs, Ys))
members_2_in_ag₂([]_0, Ys) -> members_2_out_ag₂([]_0, Ys)
if_members_2_in_2_ag₄(X, Xs, Ys, members_2_out_ag₂(Xs, Ys)) -> members_2_out_ag₂(._2₂(X, Xs), Ys)
if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag₂(Neighbors, Colors1)) -> color_region_2_out_ag₂(region_3₃(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_in_ag₂(Regions, Colors))
color_map_2_in_ag₂([]_0, Colors) -> color_map_2_out_ag₂([]_0, Colors)
if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_out_ag₂(Regions, Colors)) -> color_map_2_out_ag₂(._2₂(Region, Regions), Colors)

↳ 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_AG₂(._2₂(X, Xs), Ys) -> IF_MEMBERS_2_IN_1_AG₄(X, Xs, Ys, member_2_in_ag₂(X, Ys))
IF_MEMBERS_2_IN_1_AG₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> MEMBERS_2_IN_AG₂(Xs, Ys)

The TRS R consists of the following rules:

member_2_in_ag₂(X, ._2₂(X, underscore)) -> member_2_out_ag₂(X, ._2₂(X, underscore))
member_2_in_ag₂(X, ._2₂(underscore1, Xs)) -> if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_in_ag₂(X, Xs))
if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_out_ag₂(X, Xs)) -> member_2_out_ag₂(X, ._2₂(underscore1, Xs))

The argument filtering Pi contains the following mapping:
._2₂(x1, x2) = ._2₂(x1, x2)
member_2_in_ag₂(x1, x2) = member_2_in_ag₁(x2)
member_2_out_ag₂(x1, x2) = member_2_out_ag₁(x1)
if_member_2_in_1_ag₄(x1, x2, x3, x4) = if_member_2_in_1_ag₁(x4)
IF_MEMBERS_2_IN_1_AG₄(x1, x2, x3, x4) = IF_MEMBERS_2_IN_1_AG₂(x3, x4)
MEMBERS_2_IN_AG₂(x1, x2) = MEMBERS_2_IN_AG₁(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_AG₁(Ys) -> IF_MEMBERS_2_IN_1_AG₂(Ys, member_2_in_ag₁(Ys))
IF_MEMBERS_2_IN_1_AG₂(Ys, member_2_out_ag₁(X)) -> MEMBERS_2_IN_AG₁(Ys)

The TRS R consists of the following rules:

member_2_in_ag₁(._2₂(X, underscore)) -> member_2_out_ag₁(X)
member_2_in_ag₁(._2₂(underscore1, Xs)) -> if_member_2_in_1_ag₁(member_2_in_ag₁(Xs))
if_member_2_in_1_ag₁(member_2_out_ag₁(X)) -> member_2_out_ag₁(X)

The set Q consists of the following terms:

member_2_in_ag₁(x0)
if_member_2_in_1_ag₁(x0)

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

↳ 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_AGA₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> SELECT_3_IN_AGA₃(X, Ys, Zs)

The TRS R consists of the following rules:

color_map_2_in_ag₂(._2₂(Region, Regions), Colors) -> if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_in_ag₂(Region, Colors))
color_region_2_in_ag₂(region_3₃(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_in_aga₃(Color, Colors, Colors1))
select_3_in_aga₃(X, ._2₂(X, Xs), Xs) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
select_3_in_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_in_aga₃(X, Ys, Zs))
if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_out_aga₃(X, Ys, Zs)) -> select_3_out_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs))
if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_out_aga₃(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag₂(Neighbors, Colors1))
members_2_in_ag₂(._2₂(X, Xs), Ys) -> if_members_2_in_1_ag₄(X, Xs, Ys, member_2_in_ag₂(X, Ys))
member_2_in_ag₂(X, ._2₂(X, underscore)) -> member_2_out_ag₂(X, ._2₂(X, underscore))
member_2_in_ag₂(X, ._2₂(underscore1, Xs)) -> if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_in_ag₂(X, Xs))
if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_out_ag₂(X, Xs)) -> member_2_out_ag₂(X, ._2₂(underscore1, Xs))
if_members_2_in_1_ag₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> if_members_2_in_2_ag₄(X, Xs, Ys, members_2_in_ag₂(Xs, Ys))
members_2_in_ag₂([]_0, Ys) -> members_2_out_ag₂([]_0, Ys)
if_members_2_in_2_ag₄(X, Xs, Ys, members_2_out_ag₂(Xs, Ys)) -> members_2_out_ag₂(._2₂(X, Xs), Ys)
if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag₂(Neighbors, Colors1)) -> color_region_2_out_ag₂(region_3₃(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_in_ag₂(Regions, Colors))
color_map_2_in_ag₂([]_0, Colors) -> color_map_2_out_ag₂([]_0, Colors)
if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_out_ag₂(Regions, Colors)) -> color_map_2_out_ag₂(._2₂(Region, Regions), Colors)

↳ 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_AGA₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> SELECT_3_IN_AGA₃(X, Ys, Zs)

R is empty.
The argument filtering Pi contains the following mapping:
._2₂(x1, x2) = ._2₂(x1, x2)
SELECT_3_IN_AGA₃(x1, x2, x3) = SELECT_3_IN_AGA₁(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_AGA₁(._2₂(Y, Ys)) -> SELECT_3_IN_AGA₁(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_AGA₁}.
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:

SELECT_3_IN_AGA₁(._2₂(Y, Ys)) -> SELECT_3_IN_AGA₁(Ys)
The graph contains the following edges 1 > 1

↳ 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_AG₂(._2₂(Region, Regions), Colors) -> IF_COLOR_MAP_2_IN_1_AG₄(Region, Regions, Colors, color_region_2_in_ag₂(Region, Colors))
IF_COLOR_MAP_2_IN_1_AG₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> COLOR_MAP_2_IN_AG₂(Regions, Colors)

The TRS R consists of the following rules:

color_map_2_in_ag₂(._2₂(Region, Regions), Colors) -> if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_in_ag₂(Region, Colors))
color_region_2_in_ag₂(region_3₃(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_in_aga₃(Color, Colors, Colors1))
select_3_in_aga₃(X, ._2₂(X, Xs), Xs) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
select_3_in_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_in_aga₃(X, Ys, Zs))
if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_out_aga₃(X, Ys, Zs)) -> select_3_out_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs))
if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_out_aga₃(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag₂(Neighbors, Colors1))
members_2_in_ag₂(._2₂(X, Xs), Ys) -> if_members_2_in_1_ag₄(X, Xs, Ys, member_2_in_ag₂(X, Ys))
member_2_in_ag₂(X, ._2₂(X, underscore)) -> member_2_out_ag₂(X, ._2₂(X, underscore))
member_2_in_ag₂(X, ._2₂(underscore1, Xs)) -> if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_in_ag₂(X, Xs))
if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_out_ag₂(X, Xs)) -> member_2_out_ag₂(X, ._2₂(underscore1, Xs))
if_members_2_in_1_ag₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> if_members_2_in_2_ag₄(X, Xs, Ys, members_2_in_ag₂(Xs, Ys))
members_2_in_ag₂([]_0, Ys) -> members_2_out_ag₂([]_0, Ys)
if_members_2_in_2_ag₄(X, Xs, Ys, members_2_out_ag₂(Xs, Ys)) -> members_2_out_ag₂(._2₂(X, Xs), Ys)
if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag₂(Neighbors, Colors1)) -> color_region_2_out_ag₂(region_3₃(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_in_ag₂(Regions, Colors))
color_map_2_in_ag₂([]_0, Colors) -> color_map_2_out_ag₂([]_0, Colors)
if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_out_ag₂(Regions, Colors)) -> color_map_2_out_ag₂(._2₂(Region, Regions), Colors)

↳ 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_AG₂(._2₂(Region, Regions), Colors) -> IF_COLOR_MAP_2_IN_1_AG₄(Region, Regions, Colors, color_region_2_in_ag₂(Region, Colors))
IF_COLOR_MAP_2_IN_1_AG₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> COLOR_MAP_2_IN_AG₂(Regions, Colors)

The TRS R consists of the following rules:

color_region_2_in_ag₂(region_3₃(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_in_aga₃(Color, Colors, Colors1))
if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_out_aga₃(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag₂(Neighbors, Colors1))
select_3_in_aga₃(X, ._2₂(X, Xs), Xs) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
select_3_in_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_in_aga₃(X, Ys, Zs))
if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag₂(Neighbors, Colors1)) -> color_region_2_out_ag₂(region_3₃(Name, Color, Neighbors), Colors)
if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_out_aga₃(X, Ys, Zs)) -> select_3_out_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs))
members_2_in_ag₂(._2₂(X, Xs), Ys) -> if_members_2_in_1_ag₄(X, Xs, Ys, member_2_in_ag₂(X, Ys))
members_2_in_ag₂([]_0, Ys) -> members_2_out_ag₂([]_0, Ys)
if_members_2_in_1_ag₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> if_members_2_in_2_ag₄(X, Xs, Ys, members_2_in_ag₂(Xs, Ys))
member_2_in_ag₂(X, ._2₂(X, underscore)) -> member_2_out_ag₂(X, ._2₂(X, underscore))
member_2_in_ag₂(X, ._2₂(underscore1, Xs)) -> if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_in_ag₂(X, Xs))
if_members_2_in_2_ag₄(X, Xs, Ys, members_2_out_ag₂(Xs, Ys)) -> members_2_out_ag₂(._2₂(X, Xs), Ys)
if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_out_ag₂(X, Xs)) -> member_2_out_ag₂(X, ._2₂(underscore1, Xs))

The argument filtering Pi contains the following mapping:
._2₂(x1, x2) = ._2₂(x1, x2)
[]_0 = []_0
region_3₃(x1, x2, x3) = region_3₂(x2, x3)
color_region_2_in_ag₂(x1, x2) = color_region_2_in_ag₁(x2)
if_color_region_2_in_1_ag₅(x1, x2, x3, x4, x5) = if_color_region_2_in_1_ag₁(x5)
select_3_in_aga₃(x1, x2, x3) = select_3_in_aga₁(x2)
select_3_out_aga₃(x1, x2, x3) = select_3_out_aga₂(x1, x3)
if_select_3_in_1_aga₅(x1, x2, x3, x4, x5) = if_select_3_in_1_aga₂(x2, x5)
if_color_region_2_in_2_ag₆(x1, x2, x3, x4, x5, x6) = if_color_region_2_in_2_ag₂(x2, x6)
members_2_in_ag₂(x1, x2) = members_2_in_ag₁(x2)
if_members_2_in_1_ag₄(x1, x2, x3, x4) = if_members_2_in_1_ag₂(x3, x4)
member_2_in_ag₂(x1, x2) = member_2_in_ag₁(x2)
member_2_out_ag₂(x1, x2) = member_2_out_ag₁(x1)
if_member_2_in_1_ag₄(x1, x2, x3, x4) = if_member_2_in_1_ag₁(x4)
if_members_2_in_2_ag₄(x1, x2, x3, x4) = if_members_2_in_2_ag₂(x1, x4)
members_2_out_ag₂(x1, x2) = members_2_out_ag₁(x1)
color_region_2_out_ag₂(x1, x2) = color_region_2_out_ag₁(x1)
COLOR_MAP_2_IN_AG₂(x1, x2) = COLOR_MAP_2_IN_AG₁(x2)
IF_COLOR_MAP_2_IN_1_AG₄(x1, x2, x3, x4) = IF_COLOR_MAP_2_IN_1_AG₂(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_AG₁(Colors) -> IF_COLOR_MAP_2_IN_1_AG₂(Colors, color_region_2_in_ag₁(Colors))
IF_COLOR_MAP_2_IN_1_AG₂(Colors, color_region_2_out_ag₁(Region)) -> COLOR_MAP_2_IN_AG₁(Colors)

The TRS R consists of the following rules:

color_region_2_in_ag₁(Colors) -> if_color_region_2_in_1_ag₁(select_3_in_aga₁(Colors))
if_color_region_2_in_1_ag₁(select_3_out_aga₂(Color, Colors1)) -> if_color_region_2_in_2_ag₂(Color, members_2_in_ag₁(Colors1))
select_3_in_aga₁(._2₂(X, Xs)) -> select_3_out_aga₂(X, Xs)
select_3_in_aga₁(._2₂(Y, Ys)) -> if_select_3_in_1_aga₂(Y, select_3_in_aga₁(Ys))
if_color_region_2_in_2_ag₂(Color, members_2_out_ag₁(Neighbors)) -> color_region_2_out_ag₁(region_3₂(Color, Neighbors))
if_select_3_in_1_aga₂(Y, select_3_out_aga₂(X, Zs)) -> select_3_out_aga₂(X, ._2₂(Y, Zs))
members_2_in_ag₁(Ys) -> if_members_2_in_1_ag₂(Ys, member_2_in_ag₁(Ys))
members_2_in_ag₁(Ys) -> members_2_out_ag₁([]_0)
if_members_2_in_1_ag₂(Ys, member_2_out_ag₁(X)) -> if_members_2_in_2_ag₂(X, members_2_in_ag₁(Ys))
member_2_in_ag₁(._2₂(X, underscore)) -> member_2_out_ag₁(X)
member_2_in_ag₁(._2₂(underscore1, Xs)) -> if_member_2_in_1_ag₁(member_2_in_ag₁(Xs))
if_members_2_in_2_ag₂(X, members_2_out_ag₁(Xs)) -> members_2_out_ag₁(._2₂(X, Xs))
if_member_2_in_1_ag₁(member_2_out_ag₁(X)) -> member_2_out_ag₁(X)

The set Q consists of the following terms:

color_region_2_in_ag₁(x0)
if_color_region_2_in_1_ag₁(x0)
select_3_in_aga₁(x0)
if_color_region_2_in_2_ag₂(x0, x1)
if_select_3_in_1_aga₂(x0, x1)
members_2_in_ag₁(x0)
if_members_2_in_1_ag₂(x0, x1)
member_2_in_ag₁(x0)
if_members_2_in_2_ag₂(x0, x1)
if_member_2_in_1_ag₁(x0)

We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {IF_COLOR_MAP_2_IN_1_AG₂, COLOR_MAP_2_IN_AG₁}.
With regard to the inferred argument filtering the predicates were used in the following modes:
color_map₂: (f,b)
color_region₂: (f,b)
select₃: (f,b,f)
members₂: (f,b)
member₂: (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_ag₂(._2₂(Region, Regions), Colors) -> if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_in_ag₂(Region, Colors))
color_region_2_in_ag₂(region_3₃(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_in_aga₃(Color, Colors, Colors1))
select_3_in_aga₃(X, ._2₂(X, Xs), Xs) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
select_3_in_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_in_aga₃(X, Ys, Zs))
if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_out_aga₃(X, Ys, Zs)) -> select_3_out_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs))
if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_out_aga₃(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag₂(Neighbors, Colors1))
members_2_in_ag₂(._2₂(X, Xs), Ys) -> if_members_2_in_1_ag₄(X, Xs, Ys, member_2_in_ag₂(X, Ys))
member_2_in_ag₂(X, ._2₂(X, underscore)) -> member_2_out_ag₂(X, ._2₂(X, underscore))
member_2_in_ag₂(X, ._2₂(underscore1, Xs)) -> if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_in_ag₂(X, Xs))
if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_out_ag₂(X, Xs)) -> member_2_out_ag₂(X, ._2₂(underscore1, Xs))
if_members_2_in_1_ag₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> if_members_2_in_2_ag₄(X, Xs, Ys, members_2_in_ag₂(Xs, Ys))
members_2_in_ag₂([]_0, Ys) -> members_2_out_ag₂([]_0, Ys)
if_members_2_in_2_ag₄(X, Xs, Ys, members_2_out_ag₂(Xs, Ys)) -> members_2_out_ag₂(._2₂(X, Xs), Ys)
if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag₂(Neighbors, Colors1)) -> color_region_2_out_ag₂(region_3₃(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_in_ag₂(Regions, Colors))
color_map_2_in_ag₂([]_0, Colors) -> color_map_2_out_ag₂([]_0, Colors)
if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_out_ag₂(Regions, Colors)) -> color_map_2_out_ag₂(._2₂(Region, Regions), Colors)

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_ag₂(._2₂(Region, Regions), Colors) -> if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_in_ag₂(Region, Colors))
color_region_2_in_ag₂(region_3₃(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_in_aga₃(Color, Colors, Colors1))
select_3_in_aga₃(X, ._2₂(X, Xs), Xs) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
select_3_in_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_in_aga₃(X, Ys, Zs))
if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_out_aga₃(X, Ys, Zs)) -> select_3_out_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs))
if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_out_aga₃(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag₂(Neighbors, Colors1))
members_2_in_ag₂(._2₂(X, Xs), Ys) -> if_members_2_in_1_ag₄(X, Xs, Ys, member_2_in_ag₂(X, Ys))
member_2_in_ag₂(X, ._2₂(X, underscore)) -> member_2_out_ag₂(X, ._2₂(X, underscore))
member_2_in_ag₂(X, ._2₂(underscore1, Xs)) -> if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_in_ag₂(X, Xs))
if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_out_ag₂(X, Xs)) -> member_2_out_ag₂(X, ._2₂(underscore1, Xs))
if_members_2_in_1_ag₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> if_members_2_in_2_ag₄(X, Xs, Ys, members_2_in_ag₂(Xs, Ys))
members_2_in_ag₂([]_0, Ys) -> members_2_out_ag₂([]_0, Ys)
if_members_2_in_2_ag₄(X, Xs, Ys, members_2_out_ag₂(Xs, Ys)) -> members_2_out_ag₂(._2₂(X, Xs), Ys)
if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag₂(Neighbors, Colors1)) -> color_region_2_out_ag₂(region_3₃(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_in_ag₂(Regions, Colors))
color_map_2_in_ag₂([]_0, Colors) -> color_map_2_out_ag₂([]_0, Colors)
if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_out_ag₂(Regions, Colors)) -> color_map_2_out_ag₂(._2₂(Region, Regions), Colors)

COLOR_MAP_2_IN_AG₂(._2₂(Region, Regions), Colors) -> IF_COLOR_MAP_2_IN_1_AG₄(Region, Regions, Colors, color_region_2_in_ag₂(Region, Colors))
COLOR_MAP_2_IN_AG₂(._2₂(Region, Regions), Colors) -> COLOR_REGION_2_IN_AG₂(Region, Colors)
COLOR_REGION_2_IN_AG₂(region_3₃(Name, Color, Neighbors), Colors) -> IF_COLOR_REGION_2_IN_1_AG₅(Name, Color, Neighbors, Colors, select_3_in_aga₃(Color, Colors, Colors1))
COLOR_REGION_2_IN_AG₂(region_3₃(Name, Color, Neighbors), Colors) -> SELECT_3_IN_AGA₃(Color, Colors, Colors1)
SELECT_3_IN_AGA₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> IF_SELECT_3_IN_1_AGA₅(X, Y, Ys, Zs, select_3_in_aga₃(X, Ys, Zs))
SELECT_3_IN_AGA₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> SELECT_3_IN_AGA₃(X, Ys, Zs)
IF_COLOR_REGION_2_IN_1_AG₅(Name, Color, Neighbors, Colors, select_3_out_aga₃(Color, Colors, Colors1)) -> IF_COLOR_REGION_2_IN_2_AG₆(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag₂(Neighbors, Colors1))
IF_COLOR_REGION_2_IN_1_AG₅(Name, Color, Neighbors, Colors, select_3_out_aga₃(Color, Colors, Colors1)) -> MEMBERS_2_IN_AG₂(Neighbors, Colors1)
MEMBERS_2_IN_AG₂(._2₂(X, Xs), Ys) -> IF_MEMBERS_2_IN_1_AG₄(X, Xs, Ys, member_2_in_ag₂(X, Ys))
MEMBERS_2_IN_AG₂(._2₂(X, Xs), Ys) -> MEMBER_2_IN_AG₂(X, Ys)
MEMBER_2_IN_AG₂(X, ._2₂(underscore1, Xs)) -> IF_MEMBER_2_IN_1_AG₄(X, underscore1, Xs, member_2_in_ag₂(X, Xs))
MEMBER_2_IN_AG₂(X, ._2₂(underscore1, Xs)) -> MEMBER_2_IN_AG₂(X, Xs)
IF_MEMBERS_2_IN_1_AG₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> IF_MEMBERS_2_IN_2_AG₄(X, Xs, Ys, members_2_in_ag₂(Xs, Ys))
IF_MEMBERS_2_IN_1_AG₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> MEMBERS_2_IN_AG₂(Xs, Ys)
IF_COLOR_MAP_2_IN_1_AG₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> IF_COLOR_MAP_2_IN_2_AG₄(Region, Regions, Colors, color_map_2_in_ag₂(Regions, Colors))
IF_COLOR_MAP_2_IN_1_AG₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> COLOR_MAP_2_IN_AG₂(Regions, Colors)

The TRS R consists of the following rules:

color_map_2_in_ag₂(._2₂(Region, Regions), Colors) -> if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_in_ag₂(Region, Colors))
color_region_2_in_ag₂(region_3₃(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_in_aga₃(Color, Colors, Colors1))
select_3_in_aga₃(X, ._2₂(X, Xs), Xs) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
select_3_in_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_in_aga₃(X, Ys, Zs))
if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_out_aga₃(X, Ys, Zs)) -> select_3_out_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs))
if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_out_aga₃(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag₂(Neighbors, Colors1))
members_2_in_ag₂(._2₂(X, Xs), Ys) -> if_members_2_in_1_ag₄(X, Xs, Ys, member_2_in_ag₂(X, Ys))
member_2_in_ag₂(X, ._2₂(X, underscore)) -> member_2_out_ag₂(X, ._2₂(X, underscore))
member_2_in_ag₂(X, ._2₂(underscore1, Xs)) -> if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_in_ag₂(X, Xs))
if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_out_ag₂(X, Xs)) -> member_2_out_ag₂(X, ._2₂(underscore1, Xs))
if_members_2_in_1_ag₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> if_members_2_in_2_ag₄(X, Xs, Ys, members_2_in_ag₂(Xs, Ys))
members_2_in_ag₂([]_0, Ys) -> members_2_out_ag₂([]_0, Ys)
if_members_2_in_2_ag₄(X, Xs, Ys, members_2_out_ag₂(Xs, Ys)) -> members_2_out_ag₂(._2₂(X, Xs), Ys)
if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag₂(Neighbors, Colors1)) -> color_region_2_out_ag₂(region_3₃(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_in_ag₂(Regions, Colors))
color_map_2_in_ag₂([]_0, Colors) -> color_map_2_out_ag₂([]_0, Colors)
if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_out_ag₂(Regions, Colors)) -> color_map_2_out_ag₂(._2₂(Region, Regions), Colors)

The argument filtering Pi contains the following mapping:
color_map_2_in_ag₂(x1, x2) = color_map_2_in_ag₁(x2)
._2₂(x1, x2) = ._2₂(x1, x2)
[]_0 = []_0
region_3₃(x1, x2, x3) = region_3₂(x2, x3)
if_color_map_2_in_1_ag₄(x1, x2, x3, x4) = if_color_map_2_in_1_ag₂(x3, x4)
color_region_2_in_ag₂(x1, x2) = color_region_2_in_ag₁(x2)
if_color_region_2_in_1_ag₅(x1, x2, x3, x4, x5) = if_color_region_2_in_1_ag₂(x4, x5)
select_3_in_aga₃(x1, x2, x3) = select_3_in_aga₁(x2)
select_3_out_aga₃(x1, x2, x3) = select_3_out_aga₃(x1, x2, x3)
if_select_3_in_1_aga₅(x1, x2, x3, x4, x5) = if_select_3_in_1_aga₃(x2, x3, x5)
if_color_region_2_in_2_ag₆(x1, x2, x3, x4, x5, x6) = if_color_region_2_in_2_ag₃(x2, x4, x6)
members_2_in_ag₂(x1, x2) = members_2_in_ag₁(x2)
if_members_2_in_1_ag₄(x1, x2, x3, x4) = if_members_2_in_1_ag₂(x3, x4)
member_2_in_ag₂(x1, x2) = member_2_in_ag₁(x2)
member_2_out_ag₂(x1, x2) = member_2_out_ag₂(x1, x2)
if_member_2_in_1_ag₄(x1, x2, x3, x4) = if_member_2_in_1_ag₃(x2, x3, x4)
if_members_2_in_2_ag₄(x1, x2, x3, x4) = if_members_2_in_2_ag₃(x1, x3, x4)
members_2_out_ag₂(x1, x2) = members_2_out_ag₂(x1, x2)
color_region_2_out_ag₂(x1, x2) = color_region_2_out_ag₂(x1, x2)
if_color_map_2_in_2_ag₄(x1, x2, x3, x4) = if_color_map_2_in_2_ag₃(x1, x3, x4)
color_map_2_out_ag₂(x1, x2) = color_map_2_out_ag₂(x1, x2)
IF_COLOR_REGION_2_IN_2_AG₆(x1, x2, x3, x4, x5, x6) = IF_COLOR_REGION_2_IN_2_AG₃(x2, x4, x6)
IF_MEMBERS_2_IN_1_AG₄(x1, x2, x3, x4) = IF_MEMBERS_2_IN_1_AG₂(x3, x4)
IF_MEMBERS_2_IN_2_AG₄(x1, x2, x3, x4) = IF_MEMBERS_2_IN_2_AG₃(x1, x3, x4)
COLOR_MAP_2_IN_AG₂(x1, x2) = COLOR_MAP_2_IN_AG₁(x2)
MEMBERS_2_IN_AG₂(x1, x2) = MEMBERS_2_IN_AG₁(x2)
IF_COLOR_MAP_2_IN_1_AG₄(x1, x2, x3, x4) = IF_COLOR_MAP_2_IN_1_AG₂(x3, x4)
MEMBER_2_IN_AG₂(x1, x2) = MEMBER_2_IN_AG₁(x2)
IF_SELECT_3_IN_1_AGA₅(x1, x2, x3, x4, x5) = IF_SELECT_3_IN_1_AGA₃(x2, x3, x5)
IF_COLOR_MAP_2_IN_2_AG₄(x1, x2, x3, x4) = IF_COLOR_MAP_2_IN_2_AG₃(x1, x3, x4)
COLOR_REGION_2_IN_AG₂(x1, x2) = COLOR_REGION_2_IN_AG₁(x2)
IF_MEMBER_2_IN_1_AG₄(x1, x2, x3, x4) = IF_MEMBER_2_IN_1_AG₃(x2, x3, x4)
IF_COLOR_REGION_2_IN_1_AG₅(x1, x2, x3, x4, x5) = IF_COLOR_REGION_2_IN_1_AG₂(x4, x5)
SELECT_3_IN_AGA₃(x1, x2, x3) = SELECT_3_IN_AGA₁(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_AG₂(._2₂(Region, Regions), Colors) -> IF_COLOR_MAP_2_IN_1_AG₄(Region, Regions, Colors, color_region_2_in_ag₂(Region, Colors))
COLOR_MAP_2_IN_AG₂(._2₂(Region, Regions), Colors) -> COLOR_REGION_2_IN_AG₂(Region, Colors)
COLOR_REGION_2_IN_AG₂(region_3₃(Name, Color, Neighbors), Colors) -> IF_COLOR_REGION_2_IN_1_AG₅(Name, Color, Neighbors, Colors, select_3_in_aga₃(Color, Colors, Colors1))
COLOR_REGION_2_IN_AG₂(region_3₃(Name, Color, Neighbors), Colors) -> SELECT_3_IN_AGA₃(Color, Colors, Colors1)
SELECT_3_IN_AGA₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> IF_SELECT_3_IN_1_AGA₅(X, Y, Ys, Zs, select_3_in_aga₃(X, Ys, Zs))
SELECT_3_IN_AGA₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> SELECT_3_IN_AGA₃(X, Ys, Zs)
IF_COLOR_REGION_2_IN_1_AG₅(Name, Color, Neighbors, Colors, select_3_out_aga₃(Color, Colors, Colors1)) -> IF_COLOR_REGION_2_IN_2_AG₆(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag₂(Neighbors, Colors1))
IF_COLOR_REGION_2_IN_1_AG₅(Name, Color, Neighbors, Colors, select_3_out_aga₃(Color, Colors, Colors1)) -> MEMBERS_2_IN_AG₂(Neighbors, Colors1)
MEMBERS_2_IN_AG₂(._2₂(X, Xs), Ys) -> IF_MEMBERS_2_IN_1_AG₄(X, Xs, Ys, member_2_in_ag₂(X, Ys))
MEMBERS_2_IN_AG₂(._2₂(X, Xs), Ys) -> MEMBER_2_IN_AG₂(X, Ys)
MEMBER_2_IN_AG₂(X, ._2₂(underscore1, Xs)) -> IF_MEMBER_2_IN_1_AG₄(X, underscore1, Xs, member_2_in_ag₂(X, Xs))
MEMBER_2_IN_AG₂(X, ._2₂(underscore1, Xs)) -> MEMBER_2_IN_AG₂(X, Xs)
IF_MEMBERS_2_IN_1_AG₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> IF_MEMBERS_2_IN_2_AG₄(X, Xs, Ys, members_2_in_ag₂(Xs, Ys))
IF_MEMBERS_2_IN_1_AG₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> MEMBERS_2_IN_AG₂(Xs, Ys)
IF_COLOR_MAP_2_IN_1_AG₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> IF_COLOR_MAP_2_IN_2_AG₄(Region, Regions, Colors, color_map_2_in_ag₂(Regions, Colors))
IF_COLOR_MAP_2_IN_1_AG₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> COLOR_MAP_2_IN_AG₂(Regions, Colors)

The TRS R consists of the following rules:

color_map_2_in_ag₂(._2₂(Region, Regions), Colors) -> if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_in_ag₂(Region, Colors))
color_region_2_in_ag₂(region_3₃(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_in_aga₃(Color, Colors, Colors1))
select_3_in_aga₃(X, ._2₂(X, Xs), Xs) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
select_3_in_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_in_aga₃(X, Ys, Zs))
if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_out_aga₃(X, Ys, Zs)) -> select_3_out_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs))
if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_out_aga₃(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag₂(Neighbors, Colors1))
members_2_in_ag₂(._2₂(X, Xs), Ys) -> if_members_2_in_1_ag₄(X, Xs, Ys, member_2_in_ag₂(X, Ys))
member_2_in_ag₂(X, ._2₂(X, underscore)) -> member_2_out_ag₂(X, ._2₂(X, underscore))
member_2_in_ag₂(X, ._2₂(underscore1, Xs)) -> if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_in_ag₂(X, Xs))
if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_out_ag₂(X, Xs)) -> member_2_out_ag₂(X, ._2₂(underscore1, Xs))
if_members_2_in_1_ag₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> if_members_2_in_2_ag₄(X, Xs, Ys, members_2_in_ag₂(Xs, Ys))
members_2_in_ag₂([]_0, Ys) -> members_2_out_ag₂([]_0, Ys)
if_members_2_in_2_ag₄(X, Xs, Ys, members_2_out_ag₂(Xs, Ys)) -> members_2_out_ag₂(._2₂(X, Xs), Ys)
if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag₂(Neighbors, Colors1)) -> color_region_2_out_ag₂(region_3₃(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_in_ag₂(Regions, Colors))
color_map_2_in_ag₂([]_0, Colors) -> color_map_2_out_ag₂([]_0, Colors)
if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_out_ag₂(Regions, Colors)) -> color_map_2_out_ag₂(._2₂(Region, Regions), Colors)

The argument filtering Pi contains the following mapping:
color_map_2_in_ag₂(x1, x2) = color_map_2_in_ag₁(x2)
._2₂(x1, x2) = ._2₂(x1, x2)
[]_0 = []_0
region_3₃(x1, x2, x3) = region_3₂(x2, x3)
if_color_map_2_in_1_ag₄(x1, x2, x3, x4) = if_color_map_2_in_1_ag₂(x3, x4)
color_region_2_in_ag₂(x1, x2) = color_region_2_in_ag₁(x2)
if_color_region_2_in_1_ag₅(x1, x2, x3, x4, x5) = if_color_region_2_in_1_ag₂(x4, x5)
select_3_in_aga₃(x1, x2, x3) = select_3_in_aga₁(x2)
select_3_out_aga₃(x1, x2, x3) = select_3_out_aga₃(x1, x2, x3)
if_select_3_in_1_aga₅(x1, x2, x3, x4, x5) = if_select_3_in_1_aga₃(x2, x3, x5)
if_color_region_2_in_2_ag₆(x1, x2, x3, x4, x5, x6) = if_color_region_2_in_2_ag₃(x2, x4, x6)
members_2_in_ag₂(x1, x2) = members_2_in_ag₁(x2)
if_members_2_in_1_ag₄(x1, x2, x3, x4) = if_members_2_in_1_ag₂(x3, x4)
member_2_in_ag₂(x1, x2) = member_2_in_ag₁(x2)
member_2_out_ag₂(x1, x2) = member_2_out_ag₂(x1, x2)
if_member_2_in_1_ag₄(x1, x2, x3, x4) = if_member_2_in_1_ag₃(x2, x3, x4)
if_members_2_in_2_ag₄(x1, x2, x3, x4) = if_members_2_in_2_ag₃(x1, x3, x4)
members_2_out_ag₂(x1, x2) = members_2_out_ag₂(x1, x2)
color_region_2_out_ag₂(x1, x2) = color_region_2_out_ag₂(x1, x2)
if_color_map_2_in_2_ag₄(x1, x2, x3, x4) = if_color_map_2_in_2_ag₃(x1, x3, x4)
color_map_2_out_ag₂(x1, x2) = color_map_2_out_ag₂(x1, x2)
IF_COLOR_REGION_2_IN_2_AG₆(x1, x2, x3, x4, x5, x6) = IF_COLOR_REGION_2_IN_2_AG₃(x2, x4, x6)
IF_MEMBERS_2_IN_1_AG₄(x1, x2, x3, x4) = IF_MEMBERS_2_IN_1_AG₂(x3, x4)
IF_MEMBERS_2_IN_2_AG₄(x1, x2, x3, x4) = IF_MEMBERS_2_IN_2_AG₃(x1, x3, x4)
COLOR_MAP_2_IN_AG₂(x1, x2) = COLOR_MAP_2_IN_AG₁(x2)
MEMBERS_2_IN_AG₂(x1, x2) = MEMBERS_2_IN_AG₁(x2)
IF_COLOR_MAP_2_IN_1_AG₄(x1, x2, x3, x4) = IF_COLOR_MAP_2_IN_1_AG₂(x3, x4)
MEMBER_2_IN_AG₂(x1, x2) = MEMBER_2_IN_AG₁(x2)
IF_SELECT_3_IN_1_AGA₅(x1, x2, x3, x4, x5) = IF_SELECT_3_IN_1_AGA₃(x2, x3, x5)
IF_COLOR_MAP_2_IN_2_AG₄(x1, x2, x3, x4) = IF_COLOR_MAP_2_IN_2_AG₃(x1, x3, x4)
COLOR_REGION_2_IN_AG₂(x1, x2) = COLOR_REGION_2_IN_AG₁(x2)
IF_MEMBER_2_IN_1_AG₄(x1, x2, x3, x4) = IF_MEMBER_2_IN_1_AG₃(x2, x3, x4)
IF_COLOR_REGION_2_IN_1_AG₅(x1, x2, x3, x4, x5) = IF_COLOR_REGION_2_IN_1_AG₂(x4, x5)
SELECT_3_IN_AGA₃(x1, x2, x3) = SELECT_3_IN_AGA₁(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_AG₂(X, ._2₂(underscore1, Xs)) -> MEMBER_2_IN_AG₂(X, Xs)

The TRS R consists of the following rules:

color_map_2_in_ag₂(._2₂(Region, Regions), Colors) -> if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_in_ag₂(Region, Colors))
color_region_2_in_ag₂(region_3₃(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_in_aga₃(Color, Colors, Colors1))
select_3_in_aga₃(X, ._2₂(X, Xs), Xs) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
select_3_in_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_in_aga₃(X, Ys, Zs))
if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_out_aga₃(X, Ys, Zs)) -> select_3_out_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs))
if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_out_aga₃(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag₂(Neighbors, Colors1))
members_2_in_ag₂(._2₂(X, Xs), Ys) -> if_members_2_in_1_ag₄(X, Xs, Ys, member_2_in_ag₂(X, Ys))
member_2_in_ag₂(X, ._2₂(X, underscore)) -> member_2_out_ag₂(X, ._2₂(X, underscore))
member_2_in_ag₂(X, ._2₂(underscore1, Xs)) -> if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_in_ag₂(X, Xs))
if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_out_ag₂(X, Xs)) -> member_2_out_ag₂(X, ._2₂(underscore1, Xs))
if_members_2_in_1_ag₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> if_members_2_in_2_ag₄(X, Xs, Ys, members_2_in_ag₂(Xs, Ys))
members_2_in_ag₂([]_0, Ys) -> members_2_out_ag₂([]_0, Ys)
if_members_2_in_2_ag₄(X, Xs, Ys, members_2_out_ag₂(Xs, Ys)) -> members_2_out_ag₂(._2₂(X, Xs), Ys)
if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag₂(Neighbors, Colors1)) -> color_region_2_out_ag₂(region_3₃(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_in_ag₂(Regions, Colors))
color_map_2_in_ag₂([]_0, Colors) -> color_map_2_out_ag₂([]_0, Colors)
if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_out_ag₂(Regions, Colors)) -> color_map_2_out_ag₂(._2₂(Region, Regions), Colors)

↳ 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_AG₂(X, ._2₂(underscore1, Xs)) -> MEMBER_2_IN_AG₂(X, Xs)

↳ 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_AG₁(._2₂(underscore1, Xs)) -> MEMBER_2_IN_AG₁(Xs)

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

MEMBER_2_IN_AG₁(._2₂(underscore1, Xs)) -> MEMBER_2_IN_AG₁(Xs)
The graph contains the following edges 1 > 1

↳ 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_AG₂(._2₂(X, Xs), Ys) -> IF_MEMBERS_2_IN_1_AG₄(X, Xs, Ys, member_2_in_ag₂(X, Ys))
IF_MEMBERS_2_IN_1_AG₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> MEMBERS_2_IN_AG₂(Xs, Ys)

The TRS R consists of the following rules:

color_map_2_in_ag₂(._2₂(Region, Regions), Colors) -> if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_in_ag₂(Region, Colors))
color_region_2_in_ag₂(region_3₃(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_in_aga₃(Color, Colors, Colors1))
select_3_in_aga₃(X, ._2₂(X, Xs), Xs) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
select_3_in_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_in_aga₃(X, Ys, Zs))
if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_out_aga₃(X, Ys, Zs)) -> select_3_out_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs))
if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_out_aga₃(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag₂(Neighbors, Colors1))
members_2_in_ag₂(._2₂(X, Xs), Ys) -> if_members_2_in_1_ag₄(X, Xs, Ys, member_2_in_ag₂(X, Ys))
member_2_in_ag₂(X, ._2₂(X, underscore)) -> member_2_out_ag₂(X, ._2₂(X, underscore))
member_2_in_ag₂(X, ._2₂(underscore1, Xs)) -> if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_in_ag₂(X, Xs))
if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_out_ag₂(X, Xs)) -> member_2_out_ag₂(X, ._2₂(underscore1, Xs))
if_members_2_in_1_ag₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> if_members_2_in_2_ag₄(X, Xs, Ys, members_2_in_ag₂(Xs, Ys))
members_2_in_ag₂([]_0, Ys) -> members_2_out_ag₂([]_0, Ys)
if_members_2_in_2_ag₄(X, Xs, Ys, members_2_out_ag₂(Xs, Ys)) -> members_2_out_ag₂(._2₂(X, Xs), Ys)
if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag₂(Neighbors, Colors1)) -> color_region_2_out_ag₂(region_3₃(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_in_ag₂(Regions, Colors))
color_map_2_in_ag₂([]_0, Colors) -> color_map_2_out_ag₂([]_0, Colors)
if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_out_ag₂(Regions, Colors)) -> color_map_2_out_ag₂(._2₂(Region, Regions), Colors)

↳ 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_AG₂(._2₂(X, Xs), Ys) -> IF_MEMBERS_2_IN_1_AG₄(X, Xs, Ys, member_2_in_ag₂(X, Ys))
IF_MEMBERS_2_IN_1_AG₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> MEMBERS_2_IN_AG₂(Xs, Ys)

The TRS R consists of the following rules:

member_2_in_ag₂(X, ._2₂(X, underscore)) -> member_2_out_ag₂(X, ._2₂(X, underscore))
member_2_in_ag₂(X, ._2₂(underscore1, Xs)) -> if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_in_ag₂(X, Xs))
if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_out_ag₂(X, Xs)) -> member_2_out_ag₂(X, ._2₂(underscore1, Xs))

The argument filtering Pi contains the following mapping:
._2₂(x1, x2) = ._2₂(x1, x2)
member_2_in_ag₂(x1, x2) = member_2_in_ag₁(x2)
member_2_out_ag₂(x1, x2) = member_2_out_ag₂(x1, x2)
if_member_2_in_1_ag₄(x1, x2, x3, x4) = if_member_2_in_1_ag₃(x2, x3, x4)
IF_MEMBERS_2_IN_1_AG₄(x1, x2, x3, x4) = IF_MEMBERS_2_IN_1_AG₂(x3, x4)
MEMBERS_2_IN_AG₂(x1, x2) = MEMBERS_2_IN_AG₁(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_AG₁(Ys) -> IF_MEMBERS_2_IN_1_AG₂(Ys, member_2_in_ag₁(Ys))
IF_MEMBERS_2_IN_1_AG₂(Ys, member_2_out_ag₂(X, Ys)) -> MEMBERS_2_IN_AG₁(Ys)

The TRS R consists of the following rules:

member_2_in_ag₁(._2₂(X, underscore)) -> member_2_out_ag₂(X, ._2₂(X, underscore))
member_2_in_ag₁(._2₂(underscore1, Xs)) -> if_member_2_in_1_ag₃(underscore1, Xs, member_2_in_ag₁(Xs))
if_member_2_in_1_ag₃(underscore1, Xs, member_2_out_ag₂(X, Xs)) -> member_2_out_ag₂(X, ._2₂(underscore1, Xs))

The set Q consists of the following terms:

member_2_in_ag₁(x0)
if_member_2_in_1_ag₃(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_AG₂, MEMBERS_2_IN_AG₁}.

↳ 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_AGA₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> SELECT_3_IN_AGA₃(X, Ys, Zs)

The TRS R consists of the following rules:

color_map_2_in_ag₂(._2₂(Region, Regions), Colors) -> if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_in_ag₂(Region, Colors))
color_region_2_in_ag₂(region_3₃(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_in_aga₃(Color, Colors, Colors1))
select_3_in_aga₃(X, ._2₂(X, Xs), Xs) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
select_3_in_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_in_aga₃(X, Ys, Zs))
if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_out_aga₃(X, Ys, Zs)) -> select_3_out_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs))
if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_out_aga₃(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag₂(Neighbors, Colors1))
members_2_in_ag₂(._2₂(X, Xs), Ys) -> if_members_2_in_1_ag₄(X, Xs, Ys, member_2_in_ag₂(X, Ys))
member_2_in_ag₂(X, ._2₂(X, underscore)) -> member_2_out_ag₂(X, ._2₂(X, underscore))
member_2_in_ag₂(X, ._2₂(underscore1, Xs)) -> if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_in_ag₂(X, Xs))
if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_out_ag₂(X, Xs)) -> member_2_out_ag₂(X, ._2₂(underscore1, Xs))
if_members_2_in_1_ag₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> if_members_2_in_2_ag₄(X, Xs, Ys, members_2_in_ag₂(Xs, Ys))
members_2_in_ag₂([]_0, Ys) -> members_2_out_ag₂([]_0, Ys)
if_members_2_in_2_ag₄(X, Xs, Ys, members_2_out_ag₂(Xs, Ys)) -> members_2_out_ag₂(._2₂(X, Xs), Ys)
if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag₂(Neighbors, Colors1)) -> color_region_2_out_ag₂(region_3₃(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_in_ag₂(Regions, Colors))
color_map_2_in_ag₂([]_0, Colors) -> color_map_2_out_ag₂([]_0, Colors)
if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_out_ag₂(Regions, Colors)) -> color_map_2_out_ag₂(._2₂(Region, Regions), Colors)

↳ 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_AGA₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> SELECT_3_IN_AGA₃(X, Ys, Zs)

↳ 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_AGA₁(._2₂(Y, Ys)) -> SELECT_3_IN_AGA₁(Ys)

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

SELECT_3_IN_AGA₁(._2₂(Y, Ys)) -> SELECT_3_IN_AGA₁(Ys)
The graph contains the following edges 1 > 1

↳ 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_AG₂(._2₂(Region, Regions), Colors) -> IF_COLOR_MAP_2_IN_1_AG₄(Region, Regions, Colors, color_region_2_in_ag₂(Region, Colors))
IF_COLOR_MAP_2_IN_1_AG₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> COLOR_MAP_2_IN_AG₂(Regions, Colors)

The TRS R consists of the following rules:

color_map_2_in_ag₂(._2₂(Region, Regions), Colors) -> if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_in_ag₂(Region, Colors))
color_region_2_in_ag₂(region_3₃(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_in_aga₃(Color, Colors, Colors1))
select_3_in_aga₃(X, ._2₂(X, Xs), Xs) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
select_3_in_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_in_aga₃(X, Ys, Zs))
if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_out_aga₃(X, Ys, Zs)) -> select_3_out_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs))
if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_out_aga₃(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag₂(Neighbors, Colors1))
members_2_in_ag₂(._2₂(X, Xs), Ys) -> if_members_2_in_1_ag₄(X, Xs, Ys, member_2_in_ag₂(X, Ys))
member_2_in_ag₂(X, ._2₂(X, underscore)) -> member_2_out_ag₂(X, ._2₂(X, underscore))
member_2_in_ag₂(X, ._2₂(underscore1, Xs)) -> if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_in_ag₂(X, Xs))
if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_out_ag₂(X, Xs)) -> member_2_out_ag₂(X, ._2₂(underscore1, Xs))
if_members_2_in_1_ag₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> if_members_2_in_2_ag₄(X, Xs, Ys, members_2_in_ag₂(Xs, Ys))
members_2_in_ag₂([]_0, Ys) -> members_2_out_ag₂([]_0, Ys)
if_members_2_in_2_ag₄(X, Xs, Ys, members_2_out_ag₂(Xs, Ys)) -> members_2_out_ag₂(._2₂(X, Xs), Ys)
if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag₂(Neighbors, Colors1)) -> color_region_2_out_ag₂(region_3₃(Name, Color, Neighbors), Colors)
if_color_map_2_in_1_ag₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_in_ag₂(Regions, Colors))
color_map_2_in_ag₂([]_0, Colors) -> color_map_2_out_ag₂([]_0, Colors)
if_color_map_2_in_2_ag₄(Region, Regions, Colors, color_map_2_out_ag₂(Regions, Colors)) -> color_map_2_out_ag₂(._2₂(Region, Regions), Colors)

↳ 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_AG₂(._2₂(Region, Regions), Colors) -> IF_COLOR_MAP_2_IN_1_AG₄(Region, Regions, Colors, color_region_2_in_ag₂(Region, Colors))
IF_COLOR_MAP_2_IN_1_AG₄(Region, Regions, Colors, color_region_2_out_ag₂(Region, Colors)) -> COLOR_MAP_2_IN_AG₂(Regions, Colors)

The TRS R consists of the following rules:

color_region_2_in_ag₂(region_3₃(Name, Color, Neighbors), Colors) -> if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_in_aga₃(Color, Colors, Colors1))
if_color_region_2_in_1_ag₅(Name, Color, Neighbors, Colors, select_3_out_aga₃(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_in_ag₂(Neighbors, Colors1))
select_3_in_aga₃(X, ._2₂(X, Xs), Xs) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
select_3_in_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs)) -> if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_in_aga₃(X, Ys, Zs))
if_color_region_2_in_2_ag₆(Name, Color, Neighbors, Colors, Colors1, members_2_out_ag₂(Neighbors, Colors1)) -> color_region_2_out_ag₂(region_3₃(Name, Color, Neighbors), Colors)
if_select_3_in_1_aga₅(X, Y, Ys, Zs, select_3_out_aga₃(X, Ys, Zs)) -> select_3_out_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs))
members_2_in_ag₂(._2₂(X, Xs), Ys) -> if_members_2_in_1_ag₄(X, Xs, Ys, member_2_in_ag₂(X, Ys))
members_2_in_ag₂([]_0, Ys) -> members_2_out_ag₂([]_0, Ys)
if_members_2_in_1_ag₄(X, Xs, Ys, member_2_out_ag₂(X, Ys)) -> if_members_2_in_2_ag₄(X, Xs, Ys, members_2_in_ag₂(Xs, Ys))
member_2_in_ag₂(X, ._2₂(X, underscore)) -> member_2_out_ag₂(X, ._2₂(X, underscore))
member_2_in_ag₂(X, ._2₂(underscore1, Xs)) -> if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_in_ag₂(X, Xs))
if_members_2_in_2_ag₄(X, Xs, Ys, members_2_out_ag₂(Xs, Ys)) -> members_2_out_ag₂(._2₂(X, Xs), Ys)
if_member_2_in_1_ag₄(X, underscore1, Xs, member_2_out_ag₂(X, Xs)) -> member_2_out_ag₂(X, ._2₂(underscore1, Xs))

The argument filtering Pi contains the following mapping:
._2₂(x1, x2) = ._2₂(x1, x2)
[]_0 = []_0
region_3₃(x1, x2, x3) = region_3₂(x2, x3)
color_region_2_in_ag₂(x1, x2) = color_region_2_in_ag₁(x2)
if_color_region_2_in_1_ag₅(x1, x2, x3, x4, x5) = if_color_region_2_in_1_ag₂(x4, x5)
select_3_in_aga₃(x1, x2, x3) = select_3_in_aga₁(x2)
select_3_out_aga₃(x1, x2, x3) = select_3_out_aga₃(x1, x2, x3)
if_select_3_in_1_aga₅(x1, x2, x3, x4, x5) = if_select_3_in_1_aga₃(x2, x3, x5)
if_color_region_2_in_2_ag₆(x1, x2, x3, x4, x5, x6) = if_color_region_2_in_2_ag₃(x2, x4, x6)
members_2_in_ag₂(x1, x2) = members_2_in_ag₁(x2)
if_members_2_in_1_ag₄(x1, x2, x3, x4) = if_members_2_in_1_ag₂(x3, x4)
member_2_in_ag₂(x1, x2) = member_2_in_ag₁(x2)
member_2_out_ag₂(x1, x2) = member_2_out_ag₂(x1, x2)
if_member_2_in_1_ag₄(x1, x2, x3, x4) = if_member_2_in_1_ag₃(x2, x3, x4)
if_members_2_in_2_ag₄(x1, x2, x3, x4) = if_members_2_in_2_ag₃(x1, x3, x4)
members_2_out_ag₂(x1, x2) = members_2_out_ag₂(x1, x2)
color_region_2_out_ag₂(x1, x2) = color_region_2_out_ag₂(x1, x2)
COLOR_MAP_2_IN_AG₂(x1, x2) = COLOR_MAP_2_IN_AG₁(x2)
IF_COLOR_MAP_2_IN_1_AG₄(x1, x2, x3, x4) = IF_COLOR_MAP_2_IN_1_AG₂(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_AG₁(Colors) -> IF_COLOR_MAP_2_IN_1_AG₂(Colors, color_region_2_in_ag₁(Colors))
IF_COLOR_MAP_2_IN_1_AG₂(Colors, color_region_2_out_ag₂(Region, Colors)) -> COLOR_MAP_2_IN_AG₁(Colors)

The TRS R consists of the following rules:

color_region_2_in_ag₁(Colors) -> if_color_region_2_in_1_ag₂(Colors, select_3_in_aga₁(Colors))
if_color_region_2_in_1_ag₂(Colors, select_3_out_aga₃(Color, Colors, Colors1)) -> if_color_region_2_in_2_ag₃(Color, Colors, members_2_in_ag₁(Colors1))
select_3_in_aga₁(._2₂(X, Xs)) -> select_3_out_aga₃(X, ._2₂(X, Xs), Xs)
select_3_in_aga₁(._2₂(Y, Ys)) -> if_select_3_in_1_aga₃(Y, Ys, select_3_in_aga₁(Ys))
if_color_region_2_in_2_ag₃(Color, Colors, members_2_out_ag₂(Neighbors, Colors1)) -> color_region_2_out_ag₂(region_3₂(Color, Neighbors), Colors)
if_select_3_in_1_aga₃(Y, Ys, select_3_out_aga₃(X, Ys, Zs)) -> select_3_out_aga₃(X, ._2₂(Y, Ys), ._2₂(Y, Zs))
members_2_in_ag₁(Ys) -> if_members_2_in_1_ag₂(Ys, member_2_in_ag₁(Ys))
members_2_in_ag₁(Ys) -> members_2_out_ag₂([]_0, Ys)
if_members_2_in_1_ag₂(Ys, member_2_out_ag₂(X, Ys)) -> if_members_2_in_2_ag₃(X, Ys, members_2_in_ag₁(Ys))
member_2_in_ag₁(._2₂(X, underscore)) -> member_2_out_ag₂(X, ._2₂(X, underscore))
member_2_in_ag₁(._2₂(underscore1, Xs)) -> if_member_2_in_1_ag₃(underscore1, Xs, member_2_in_ag₁(Xs))
if_members_2_in_2_ag₃(X, Ys, members_2_out_ag₂(Xs, Ys)) -> members_2_out_ag₂(._2₂(X, Xs), Ys)
if_member_2_in_1_ag₃(underscore1, Xs, member_2_out_ag₂(X, Xs)) -> member_2_out_ag₂(X, ._2₂(underscore1, Xs))

The set Q consists of the following terms:

color_region_2_in_ag₁(x0)
if_color_region_2_in_1_ag₂(x0, x1)
select_3_in_aga₁(x0)
if_color_region_2_in_2_ag₃(x0, x1, x2)
if_select_3_in_1_aga₃(x0, x1, x2)
members_2_in_ag₁(x0)
if_members_2_in_1_ag₂(x0, x1)
member_2_in_ag₁(x0)
if_members_2_in_2_ag₃(x0, x1, x2)
if_member_2_in_1_ag₃(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_AG₂, COLOR_MAP_2_IN_AG₁}.