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



PROLOG
  ↳ PrologToPiTRSProof

perm12(L, M) :- eqlen12(L, M), samesets2(L, M).
eqlen12({}0, {}0).
eqlen12(.2(underscore, Xs), .2(underscore1, Ys)) :- eqlen12(Xs, Ys).
member2(X, .2(X, underscore2)).
member2(X, .2(underscore3, T)) :- member2(X, T).
samesets2({}0, underscore4).
samesets2(.2(X, Xs), L) :- member2(X, L), samesets2(Xs, L).


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


perm1_2_in_gg2(L, M) -> if_perm1_2_in_1_gg3(L, M, eq_len1_2_in_gg2(L, M))
eq_len1_2_in_gg2([]_0, []_0) -> eq_len1_2_out_gg2([]_0, []_0)
eq_len1_2_in_gg2(._22(underscore, Xs), ._22(underscore1, Ys)) -> if_eq_len1_2_in_1_gg5(underscore, Xs, underscore1, Ys, eq_len1_2_in_gg2(Xs, Ys))
if_eq_len1_2_in_1_gg5(underscore, Xs, underscore1, Ys, eq_len1_2_out_gg2(Xs, Ys)) -> eq_len1_2_out_gg2(._22(underscore, Xs), ._22(underscore1, Ys))
if_perm1_2_in_1_gg3(L, M, eq_len1_2_out_gg2(L, M)) -> if_perm1_2_in_2_gg3(L, M, same_sets_2_in_gg2(L, M))
same_sets_2_in_gg2([]_0, underscore4) -> same_sets_2_out_gg2([]_0, underscore4)
same_sets_2_in_gg2(._22(X, Xs), L) -> if_same_sets_2_in_1_gg4(X, Xs, L, member_2_in_gg2(X, L))
member_2_in_gg2(X, ._22(X, underscore2)) -> member_2_out_gg2(X, ._22(X, underscore2))
member_2_in_gg2(X, ._22(underscore3, T)) -> if_member_2_in_1_gg4(X, underscore3, T, member_2_in_gg2(X, T))
if_member_2_in_1_gg4(X, underscore3, T, member_2_out_gg2(X, T)) -> member_2_out_gg2(X, ._22(underscore3, T))
if_same_sets_2_in_1_gg4(X, Xs, L, member_2_out_gg2(X, L)) -> if_same_sets_2_in_2_gg4(X, Xs, L, same_sets_2_in_gg2(Xs, L))
if_same_sets_2_in_2_gg4(X, Xs, L, same_sets_2_out_gg2(Xs, L)) -> same_sets_2_out_gg2(._22(X, Xs), L)
if_perm1_2_in_2_gg3(L, M, same_sets_2_out_gg2(L, M)) -> perm1_2_out_gg2(L, M)

The argument filtering Pi contains the following mapping:
perm1_2_in_gg2(x1, x2)  =  perm1_2_in_gg2(x1, x2)
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
if_perm1_2_in_1_gg3(x1, x2, x3)  =  if_perm1_2_in_1_gg3(x1, x2, x3)
eq_len1_2_in_gg2(x1, x2)  =  eq_len1_2_in_gg2(x1, x2)
eq_len1_2_out_gg2(x1, x2)  =  eq_len1_2_out_gg
if_eq_len1_2_in_1_gg5(x1, x2, x3, x4, x5)  =  if_eq_len1_2_in_1_gg1(x5)
if_perm1_2_in_2_gg3(x1, x2, x3)  =  if_perm1_2_in_2_gg1(x3)
same_sets_2_in_gg2(x1, x2)  =  same_sets_2_in_gg2(x1, x2)
same_sets_2_out_gg2(x1, x2)  =  same_sets_2_out_gg
if_same_sets_2_in_1_gg4(x1, x2, x3, x4)  =  if_same_sets_2_in_1_gg3(x2, x3, x4)
member_2_in_gg2(x1, x2)  =  member_2_in_gg2(x1, x2)
member_2_out_gg2(x1, x2)  =  member_2_out_gg
if_member_2_in_1_gg4(x1, x2, x3, x4)  =  if_member_2_in_1_gg1(x4)
if_same_sets_2_in_2_gg4(x1, x2, x3, x4)  =  if_same_sets_2_in_2_gg1(x4)
perm1_2_out_gg2(x1, x2)  =  perm1_2_out_gg

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of PROLOG



↳ PROLOG
  ↳ PrologToPiTRSProof
PiTRS
      ↳ DependencyPairsProof

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

perm1_2_in_gg2(L, M) -> if_perm1_2_in_1_gg3(L, M, eq_len1_2_in_gg2(L, M))
eq_len1_2_in_gg2([]_0, []_0) -> eq_len1_2_out_gg2([]_0, []_0)
eq_len1_2_in_gg2(._22(underscore, Xs), ._22(underscore1, Ys)) -> if_eq_len1_2_in_1_gg5(underscore, Xs, underscore1, Ys, eq_len1_2_in_gg2(Xs, Ys))
if_eq_len1_2_in_1_gg5(underscore, Xs, underscore1, Ys, eq_len1_2_out_gg2(Xs, Ys)) -> eq_len1_2_out_gg2(._22(underscore, Xs), ._22(underscore1, Ys))
if_perm1_2_in_1_gg3(L, M, eq_len1_2_out_gg2(L, M)) -> if_perm1_2_in_2_gg3(L, M, same_sets_2_in_gg2(L, M))
same_sets_2_in_gg2([]_0, underscore4) -> same_sets_2_out_gg2([]_0, underscore4)
same_sets_2_in_gg2(._22(X, Xs), L) -> if_same_sets_2_in_1_gg4(X, Xs, L, member_2_in_gg2(X, L))
member_2_in_gg2(X, ._22(X, underscore2)) -> member_2_out_gg2(X, ._22(X, underscore2))
member_2_in_gg2(X, ._22(underscore3, T)) -> if_member_2_in_1_gg4(X, underscore3, T, member_2_in_gg2(X, T))
if_member_2_in_1_gg4(X, underscore3, T, member_2_out_gg2(X, T)) -> member_2_out_gg2(X, ._22(underscore3, T))
if_same_sets_2_in_1_gg4(X, Xs, L, member_2_out_gg2(X, L)) -> if_same_sets_2_in_2_gg4(X, Xs, L, same_sets_2_in_gg2(Xs, L))
if_same_sets_2_in_2_gg4(X, Xs, L, same_sets_2_out_gg2(Xs, L)) -> same_sets_2_out_gg2(._22(X, Xs), L)
if_perm1_2_in_2_gg3(L, M, same_sets_2_out_gg2(L, M)) -> perm1_2_out_gg2(L, M)

The argument filtering Pi contains the following mapping:
perm1_2_in_gg2(x1, x2)  =  perm1_2_in_gg2(x1, x2)
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
if_perm1_2_in_1_gg3(x1, x2, x3)  =  if_perm1_2_in_1_gg3(x1, x2, x3)
eq_len1_2_in_gg2(x1, x2)  =  eq_len1_2_in_gg2(x1, x2)
eq_len1_2_out_gg2(x1, x2)  =  eq_len1_2_out_gg
if_eq_len1_2_in_1_gg5(x1, x2, x3, x4, x5)  =  if_eq_len1_2_in_1_gg1(x5)
if_perm1_2_in_2_gg3(x1, x2, x3)  =  if_perm1_2_in_2_gg1(x3)
same_sets_2_in_gg2(x1, x2)  =  same_sets_2_in_gg2(x1, x2)
same_sets_2_out_gg2(x1, x2)  =  same_sets_2_out_gg
if_same_sets_2_in_1_gg4(x1, x2, x3, x4)  =  if_same_sets_2_in_1_gg3(x2, x3, x4)
member_2_in_gg2(x1, x2)  =  member_2_in_gg2(x1, x2)
member_2_out_gg2(x1, x2)  =  member_2_out_gg
if_member_2_in_1_gg4(x1, x2, x3, x4)  =  if_member_2_in_1_gg1(x4)
if_same_sets_2_in_2_gg4(x1, x2, x3, x4)  =  if_same_sets_2_in_2_gg1(x4)
perm1_2_out_gg2(x1, x2)  =  perm1_2_out_gg


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

PERM1_2_IN_GG2(L, M) -> IF_PERM1_2_IN_1_GG3(L, M, eq_len1_2_in_gg2(L, M))
PERM1_2_IN_GG2(L, M) -> EQ_LEN1_2_IN_GG2(L, M)
EQ_LEN1_2_IN_GG2(._22(underscore, Xs), ._22(underscore1, Ys)) -> IF_EQ_LEN1_2_IN_1_GG5(underscore, Xs, underscore1, Ys, eq_len1_2_in_gg2(Xs, Ys))
EQ_LEN1_2_IN_GG2(._22(underscore, Xs), ._22(underscore1, Ys)) -> EQ_LEN1_2_IN_GG2(Xs, Ys)
IF_PERM1_2_IN_1_GG3(L, M, eq_len1_2_out_gg2(L, M)) -> IF_PERM1_2_IN_2_GG3(L, M, same_sets_2_in_gg2(L, M))
IF_PERM1_2_IN_1_GG3(L, M, eq_len1_2_out_gg2(L, M)) -> SAME_SETS_2_IN_GG2(L, M)
SAME_SETS_2_IN_GG2(._22(X, Xs), L) -> IF_SAME_SETS_2_IN_1_GG4(X, Xs, L, member_2_in_gg2(X, L))
SAME_SETS_2_IN_GG2(._22(X, Xs), L) -> MEMBER_2_IN_GG2(X, L)
MEMBER_2_IN_GG2(X, ._22(underscore3, T)) -> IF_MEMBER_2_IN_1_GG4(X, underscore3, T, member_2_in_gg2(X, T))
MEMBER_2_IN_GG2(X, ._22(underscore3, T)) -> MEMBER_2_IN_GG2(X, T)
IF_SAME_SETS_2_IN_1_GG4(X, Xs, L, member_2_out_gg2(X, L)) -> IF_SAME_SETS_2_IN_2_GG4(X, Xs, L, same_sets_2_in_gg2(Xs, L))
IF_SAME_SETS_2_IN_1_GG4(X, Xs, L, member_2_out_gg2(X, L)) -> SAME_SETS_2_IN_GG2(Xs, L)

The TRS R consists of the following rules:

perm1_2_in_gg2(L, M) -> if_perm1_2_in_1_gg3(L, M, eq_len1_2_in_gg2(L, M))
eq_len1_2_in_gg2([]_0, []_0) -> eq_len1_2_out_gg2([]_0, []_0)
eq_len1_2_in_gg2(._22(underscore, Xs), ._22(underscore1, Ys)) -> if_eq_len1_2_in_1_gg5(underscore, Xs, underscore1, Ys, eq_len1_2_in_gg2(Xs, Ys))
if_eq_len1_2_in_1_gg5(underscore, Xs, underscore1, Ys, eq_len1_2_out_gg2(Xs, Ys)) -> eq_len1_2_out_gg2(._22(underscore, Xs), ._22(underscore1, Ys))
if_perm1_2_in_1_gg3(L, M, eq_len1_2_out_gg2(L, M)) -> if_perm1_2_in_2_gg3(L, M, same_sets_2_in_gg2(L, M))
same_sets_2_in_gg2([]_0, underscore4) -> same_sets_2_out_gg2([]_0, underscore4)
same_sets_2_in_gg2(._22(X, Xs), L) -> if_same_sets_2_in_1_gg4(X, Xs, L, member_2_in_gg2(X, L))
member_2_in_gg2(X, ._22(X, underscore2)) -> member_2_out_gg2(X, ._22(X, underscore2))
member_2_in_gg2(X, ._22(underscore3, T)) -> if_member_2_in_1_gg4(X, underscore3, T, member_2_in_gg2(X, T))
if_member_2_in_1_gg4(X, underscore3, T, member_2_out_gg2(X, T)) -> member_2_out_gg2(X, ._22(underscore3, T))
if_same_sets_2_in_1_gg4(X, Xs, L, member_2_out_gg2(X, L)) -> if_same_sets_2_in_2_gg4(X, Xs, L, same_sets_2_in_gg2(Xs, L))
if_same_sets_2_in_2_gg4(X, Xs, L, same_sets_2_out_gg2(Xs, L)) -> same_sets_2_out_gg2(._22(X, Xs), L)
if_perm1_2_in_2_gg3(L, M, same_sets_2_out_gg2(L, M)) -> perm1_2_out_gg2(L, M)

The argument filtering Pi contains the following mapping:
perm1_2_in_gg2(x1, x2)  =  perm1_2_in_gg2(x1, x2)
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
if_perm1_2_in_1_gg3(x1, x2, x3)  =  if_perm1_2_in_1_gg3(x1, x2, x3)
eq_len1_2_in_gg2(x1, x2)  =  eq_len1_2_in_gg2(x1, x2)
eq_len1_2_out_gg2(x1, x2)  =  eq_len1_2_out_gg
if_eq_len1_2_in_1_gg5(x1, x2, x3, x4, x5)  =  if_eq_len1_2_in_1_gg1(x5)
if_perm1_2_in_2_gg3(x1, x2, x3)  =  if_perm1_2_in_2_gg1(x3)
same_sets_2_in_gg2(x1, x2)  =  same_sets_2_in_gg2(x1, x2)
same_sets_2_out_gg2(x1, x2)  =  same_sets_2_out_gg
if_same_sets_2_in_1_gg4(x1, x2, x3, x4)  =  if_same_sets_2_in_1_gg3(x2, x3, x4)
member_2_in_gg2(x1, x2)  =  member_2_in_gg2(x1, x2)
member_2_out_gg2(x1, x2)  =  member_2_out_gg
if_member_2_in_1_gg4(x1, x2, x3, x4)  =  if_member_2_in_1_gg1(x4)
if_same_sets_2_in_2_gg4(x1, x2, x3, x4)  =  if_same_sets_2_in_2_gg1(x4)
perm1_2_out_gg2(x1, x2)  =  perm1_2_out_gg
IF_MEMBER_2_IN_1_GG4(x1, x2, x3, x4)  =  IF_MEMBER_2_IN_1_GG1(x4)
IF_EQ_LEN1_2_IN_1_GG5(x1, x2, x3, x4, x5)  =  IF_EQ_LEN1_2_IN_1_GG1(x5)
MEMBER_2_IN_GG2(x1, x2)  =  MEMBER_2_IN_GG2(x1, x2)
IF_PERM1_2_IN_1_GG3(x1, x2, x3)  =  IF_PERM1_2_IN_1_GG3(x1, x2, x3)
PERM1_2_IN_GG2(x1, x2)  =  PERM1_2_IN_GG2(x1, x2)
SAME_SETS_2_IN_GG2(x1, x2)  =  SAME_SETS_2_IN_GG2(x1, x2)
IF_SAME_SETS_2_IN_1_GG4(x1, x2, x3, x4)  =  IF_SAME_SETS_2_IN_1_GG3(x2, x3, x4)
IF_PERM1_2_IN_2_GG3(x1, x2, x3)  =  IF_PERM1_2_IN_2_GG1(x3)
IF_SAME_SETS_2_IN_2_GG4(x1, x2, x3, x4)  =  IF_SAME_SETS_2_IN_2_GG1(x4)
EQ_LEN1_2_IN_GG2(x1, x2)  =  EQ_LEN1_2_IN_GG2(x1, x2)

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

↳ PROLOG
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
PiDP
          ↳ DependencyGraphProof

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

PERM1_2_IN_GG2(L, M) -> IF_PERM1_2_IN_1_GG3(L, M, eq_len1_2_in_gg2(L, M))
PERM1_2_IN_GG2(L, M) -> EQ_LEN1_2_IN_GG2(L, M)
EQ_LEN1_2_IN_GG2(._22(underscore, Xs), ._22(underscore1, Ys)) -> IF_EQ_LEN1_2_IN_1_GG5(underscore, Xs, underscore1, Ys, eq_len1_2_in_gg2(Xs, Ys))
EQ_LEN1_2_IN_GG2(._22(underscore, Xs), ._22(underscore1, Ys)) -> EQ_LEN1_2_IN_GG2(Xs, Ys)
IF_PERM1_2_IN_1_GG3(L, M, eq_len1_2_out_gg2(L, M)) -> IF_PERM1_2_IN_2_GG3(L, M, same_sets_2_in_gg2(L, M))
IF_PERM1_2_IN_1_GG3(L, M, eq_len1_2_out_gg2(L, M)) -> SAME_SETS_2_IN_GG2(L, M)
SAME_SETS_2_IN_GG2(._22(X, Xs), L) -> IF_SAME_SETS_2_IN_1_GG4(X, Xs, L, member_2_in_gg2(X, L))
SAME_SETS_2_IN_GG2(._22(X, Xs), L) -> MEMBER_2_IN_GG2(X, L)
MEMBER_2_IN_GG2(X, ._22(underscore3, T)) -> IF_MEMBER_2_IN_1_GG4(X, underscore3, T, member_2_in_gg2(X, T))
MEMBER_2_IN_GG2(X, ._22(underscore3, T)) -> MEMBER_2_IN_GG2(X, T)
IF_SAME_SETS_2_IN_1_GG4(X, Xs, L, member_2_out_gg2(X, L)) -> IF_SAME_SETS_2_IN_2_GG4(X, Xs, L, same_sets_2_in_gg2(Xs, L))
IF_SAME_SETS_2_IN_1_GG4(X, Xs, L, member_2_out_gg2(X, L)) -> SAME_SETS_2_IN_GG2(Xs, L)

The TRS R consists of the following rules:

perm1_2_in_gg2(L, M) -> if_perm1_2_in_1_gg3(L, M, eq_len1_2_in_gg2(L, M))
eq_len1_2_in_gg2([]_0, []_0) -> eq_len1_2_out_gg2([]_0, []_0)
eq_len1_2_in_gg2(._22(underscore, Xs), ._22(underscore1, Ys)) -> if_eq_len1_2_in_1_gg5(underscore, Xs, underscore1, Ys, eq_len1_2_in_gg2(Xs, Ys))
if_eq_len1_2_in_1_gg5(underscore, Xs, underscore1, Ys, eq_len1_2_out_gg2(Xs, Ys)) -> eq_len1_2_out_gg2(._22(underscore, Xs), ._22(underscore1, Ys))
if_perm1_2_in_1_gg3(L, M, eq_len1_2_out_gg2(L, M)) -> if_perm1_2_in_2_gg3(L, M, same_sets_2_in_gg2(L, M))
same_sets_2_in_gg2([]_0, underscore4) -> same_sets_2_out_gg2([]_0, underscore4)
same_sets_2_in_gg2(._22(X, Xs), L) -> if_same_sets_2_in_1_gg4(X, Xs, L, member_2_in_gg2(X, L))
member_2_in_gg2(X, ._22(X, underscore2)) -> member_2_out_gg2(X, ._22(X, underscore2))
member_2_in_gg2(X, ._22(underscore3, T)) -> if_member_2_in_1_gg4(X, underscore3, T, member_2_in_gg2(X, T))
if_member_2_in_1_gg4(X, underscore3, T, member_2_out_gg2(X, T)) -> member_2_out_gg2(X, ._22(underscore3, T))
if_same_sets_2_in_1_gg4(X, Xs, L, member_2_out_gg2(X, L)) -> if_same_sets_2_in_2_gg4(X, Xs, L, same_sets_2_in_gg2(Xs, L))
if_same_sets_2_in_2_gg4(X, Xs, L, same_sets_2_out_gg2(Xs, L)) -> same_sets_2_out_gg2(._22(X, Xs), L)
if_perm1_2_in_2_gg3(L, M, same_sets_2_out_gg2(L, M)) -> perm1_2_out_gg2(L, M)

The argument filtering Pi contains the following mapping:
perm1_2_in_gg2(x1, x2)  =  perm1_2_in_gg2(x1, x2)
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
if_perm1_2_in_1_gg3(x1, x2, x3)  =  if_perm1_2_in_1_gg3(x1, x2, x3)
eq_len1_2_in_gg2(x1, x2)  =  eq_len1_2_in_gg2(x1, x2)
eq_len1_2_out_gg2(x1, x2)  =  eq_len1_2_out_gg
if_eq_len1_2_in_1_gg5(x1, x2, x3, x4, x5)  =  if_eq_len1_2_in_1_gg1(x5)
if_perm1_2_in_2_gg3(x1, x2, x3)  =  if_perm1_2_in_2_gg1(x3)
same_sets_2_in_gg2(x1, x2)  =  same_sets_2_in_gg2(x1, x2)
same_sets_2_out_gg2(x1, x2)  =  same_sets_2_out_gg
if_same_sets_2_in_1_gg4(x1, x2, x3, x4)  =  if_same_sets_2_in_1_gg3(x2, x3, x4)
member_2_in_gg2(x1, x2)  =  member_2_in_gg2(x1, x2)
member_2_out_gg2(x1, x2)  =  member_2_out_gg
if_member_2_in_1_gg4(x1, x2, x3, x4)  =  if_member_2_in_1_gg1(x4)
if_same_sets_2_in_2_gg4(x1, x2, x3, x4)  =  if_same_sets_2_in_2_gg1(x4)
perm1_2_out_gg2(x1, x2)  =  perm1_2_out_gg
IF_MEMBER_2_IN_1_GG4(x1, x2, x3, x4)  =  IF_MEMBER_2_IN_1_GG1(x4)
IF_EQ_LEN1_2_IN_1_GG5(x1, x2, x3, x4, x5)  =  IF_EQ_LEN1_2_IN_1_GG1(x5)
MEMBER_2_IN_GG2(x1, x2)  =  MEMBER_2_IN_GG2(x1, x2)
IF_PERM1_2_IN_1_GG3(x1, x2, x3)  =  IF_PERM1_2_IN_1_GG3(x1, x2, x3)
PERM1_2_IN_GG2(x1, x2)  =  PERM1_2_IN_GG2(x1, x2)
SAME_SETS_2_IN_GG2(x1, x2)  =  SAME_SETS_2_IN_GG2(x1, x2)
IF_SAME_SETS_2_IN_1_GG4(x1, x2, x3, x4)  =  IF_SAME_SETS_2_IN_1_GG3(x2, x3, x4)
IF_PERM1_2_IN_2_GG3(x1, x2, x3)  =  IF_PERM1_2_IN_2_GG1(x3)
IF_SAME_SETS_2_IN_2_GG4(x1, x2, x3, x4)  =  IF_SAME_SETS_2_IN_2_GG1(x4)
EQ_LEN1_2_IN_GG2(x1, x2)  =  EQ_LEN1_2_IN_GG2(x1, x2)

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

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

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

MEMBER_2_IN_GG2(X, ._22(underscore3, T)) -> MEMBER_2_IN_GG2(X, T)

The TRS R consists of the following rules:

perm1_2_in_gg2(L, M) -> if_perm1_2_in_1_gg3(L, M, eq_len1_2_in_gg2(L, M))
eq_len1_2_in_gg2([]_0, []_0) -> eq_len1_2_out_gg2([]_0, []_0)
eq_len1_2_in_gg2(._22(underscore, Xs), ._22(underscore1, Ys)) -> if_eq_len1_2_in_1_gg5(underscore, Xs, underscore1, Ys, eq_len1_2_in_gg2(Xs, Ys))
if_eq_len1_2_in_1_gg5(underscore, Xs, underscore1, Ys, eq_len1_2_out_gg2(Xs, Ys)) -> eq_len1_2_out_gg2(._22(underscore, Xs), ._22(underscore1, Ys))
if_perm1_2_in_1_gg3(L, M, eq_len1_2_out_gg2(L, M)) -> if_perm1_2_in_2_gg3(L, M, same_sets_2_in_gg2(L, M))
same_sets_2_in_gg2([]_0, underscore4) -> same_sets_2_out_gg2([]_0, underscore4)
same_sets_2_in_gg2(._22(X, Xs), L) -> if_same_sets_2_in_1_gg4(X, Xs, L, member_2_in_gg2(X, L))
member_2_in_gg2(X, ._22(X, underscore2)) -> member_2_out_gg2(X, ._22(X, underscore2))
member_2_in_gg2(X, ._22(underscore3, T)) -> if_member_2_in_1_gg4(X, underscore3, T, member_2_in_gg2(X, T))
if_member_2_in_1_gg4(X, underscore3, T, member_2_out_gg2(X, T)) -> member_2_out_gg2(X, ._22(underscore3, T))
if_same_sets_2_in_1_gg4(X, Xs, L, member_2_out_gg2(X, L)) -> if_same_sets_2_in_2_gg4(X, Xs, L, same_sets_2_in_gg2(Xs, L))
if_same_sets_2_in_2_gg4(X, Xs, L, same_sets_2_out_gg2(Xs, L)) -> same_sets_2_out_gg2(._22(X, Xs), L)
if_perm1_2_in_2_gg3(L, M, same_sets_2_out_gg2(L, M)) -> perm1_2_out_gg2(L, M)

The argument filtering Pi contains the following mapping:
perm1_2_in_gg2(x1, x2)  =  perm1_2_in_gg2(x1, x2)
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
if_perm1_2_in_1_gg3(x1, x2, x3)  =  if_perm1_2_in_1_gg3(x1, x2, x3)
eq_len1_2_in_gg2(x1, x2)  =  eq_len1_2_in_gg2(x1, x2)
eq_len1_2_out_gg2(x1, x2)  =  eq_len1_2_out_gg
if_eq_len1_2_in_1_gg5(x1, x2, x3, x4, x5)  =  if_eq_len1_2_in_1_gg1(x5)
if_perm1_2_in_2_gg3(x1, x2, x3)  =  if_perm1_2_in_2_gg1(x3)
same_sets_2_in_gg2(x1, x2)  =  same_sets_2_in_gg2(x1, x2)
same_sets_2_out_gg2(x1, x2)  =  same_sets_2_out_gg
if_same_sets_2_in_1_gg4(x1, x2, x3, x4)  =  if_same_sets_2_in_1_gg3(x2, x3, x4)
member_2_in_gg2(x1, x2)  =  member_2_in_gg2(x1, x2)
member_2_out_gg2(x1, x2)  =  member_2_out_gg
if_member_2_in_1_gg4(x1, x2, x3, x4)  =  if_member_2_in_1_gg1(x4)
if_same_sets_2_in_2_gg4(x1, x2, x3, x4)  =  if_same_sets_2_in_2_gg1(x4)
perm1_2_out_gg2(x1, x2)  =  perm1_2_out_gg
MEMBER_2_IN_GG2(x1, x2)  =  MEMBER_2_IN_GG2(x1, x2)

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

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

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

MEMBER_2_IN_GG2(X, ._22(underscore3, T)) -> MEMBER_2_IN_GG2(X, T)

R is empty.
Pi is empty.
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

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

MEMBER_2_IN_GG2(X, ._22(underscore3, T)) -> MEMBER_2_IN_GG2(X, 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_GG2}.
By using the subterm criterion together with the size-change analysis we have proven that there are no infinite chains for this DP problem.

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



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

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

IF_SAME_SETS_2_IN_1_GG4(X, Xs, L, member_2_out_gg2(X, L)) -> SAME_SETS_2_IN_GG2(Xs, L)
SAME_SETS_2_IN_GG2(._22(X, Xs), L) -> IF_SAME_SETS_2_IN_1_GG4(X, Xs, L, member_2_in_gg2(X, L))

The TRS R consists of the following rules:

perm1_2_in_gg2(L, M) -> if_perm1_2_in_1_gg3(L, M, eq_len1_2_in_gg2(L, M))
eq_len1_2_in_gg2([]_0, []_0) -> eq_len1_2_out_gg2([]_0, []_0)
eq_len1_2_in_gg2(._22(underscore, Xs), ._22(underscore1, Ys)) -> if_eq_len1_2_in_1_gg5(underscore, Xs, underscore1, Ys, eq_len1_2_in_gg2(Xs, Ys))
if_eq_len1_2_in_1_gg5(underscore, Xs, underscore1, Ys, eq_len1_2_out_gg2(Xs, Ys)) -> eq_len1_2_out_gg2(._22(underscore, Xs), ._22(underscore1, Ys))
if_perm1_2_in_1_gg3(L, M, eq_len1_2_out_gg2(L, M)) -> if_perm1_2_in_2_gg3(L, M, same_sets_2_in_gg2(L, M))
same_sets_2_in_gg2([]_0, underscore4) -> same_sets_2_out_gg2([]_0, underscore4)
same_sets_2_in_gg2(._22(X, Xs), L) -> if_same_sets_2_in_1_gg4(X, Xs, L, member_2_in_gg2(X, L))
member_2_in_gg2(X, ._22(X, underscore2)) -> member_2_out_gg2(X, ._22(X, underscore2))
member_2_in_gg2(X, ._22(underscore3, T)) -> if_member_2_in_1_gg4(X, underscore3, T, member_2_in_gg2(X, T))
if_member_2_in_1_gg4(X, underscore3, T, member_2_out_gg2(X, T)) -> member_2_out_gg2(X, ._22(underscore3, T))
if_same_sets_2_in_1_gg4(X, Xs, L, member_2_out_gg2(X, L)) -> if_same_sets_2_in_2_gg4(X, Xs, L, same_sets_2_in_gg2(Xs, L))
if_same_sets_2_in_2_gg4(X, Xs, L, same_sets_2_out_gg2(Xs, L)) -> same_sets_2_out_gg2(._22(X, Xs), L)
if_perm1_2_in_2_gg3(L, M, same_sets_2_out_gg2(L, M)) -> perm1_2_out_gg2(L, M)

The argument filtering Pi contains the following mapping:
perm1_2_in_gg2(x1, x2)  =  perm1_2_in_gg2(x1, x2)
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
if_perm1_2_in_1_gg3(x1, x2, x3)  =  if_perm1_2_in_1_gg3(x1, x2, x3)
eq_len1_2_in_gg2(x1, x2)  =  eq_len1_2_in_gg2(x1, x2)
eq_len1_2_out_gg2(x1, x2)  =  eq_len1_2_out_gg
if_eq_len1_2_in_1_gg5(x1, x2, x3, x4, x5)  =  if_eq_len1_2_in_1_gg1(x5)
if_perm1_2_in_2_gg3(x1, x2, x3)  =  if_perm1_2_in_2_gg1(x3)
same_sets_2_in_gg2(x1, x2)  =  same_sets_2_in_gg2(x1, x2)
same_sets_2_out_gg2(x1, x2)  =  same_sets_2_out_gg
if_same_sets_2_in_1_gg4(x1, x2, x3, x4)  =  if_same_sets_2_in_1_gg3(x2, x3, x4)
member_2_in_gg2(x1, x2)  =  member_2_in_gg2(x1, x2)
member_2_out_gg2(x1, x2)  =  member_2_out_gg
if_member_2_in_1_gg4(x1, x2, x3, x4)  =  if_member_2_in_1_gg1(x4)
if_same_sets_2_in_2_gg4(x1, x2, x3, x4)  =  if_same_sets_2_in_2_gg1(x4)
perm1_2_out_gg2(x1, x2)  =  perm1_2_out_gg
SAME_SETS_2_IN_GG2(x1, x2)  =  SAME_SETS_2_IN_GG2(x1, x2)
IF_SAME_SETS_2_IN_1_GG4(x1, x2, x3, x4)  =  IF_SAME_SETS_2_IN_1_GG3(x2, x3, x4)

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

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

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

IF_SAME_SETS_2_IN_1_GG4(X, Xs, L, member_2_out_gg2(X, L)) -> SAME_SETS_2_IN_GG2(Xs, L)
SAME_SETS_2_IN_GG2(._22(X, Xs), L) -> IF_SAME_SETS_2_IN_1_GG4(X, Xs, L, member_2_in_gg2(X, L))

The TRS R consists of the following rules:

member_2_in_gg2(X, ._22(X, underscore2)) -> member_2_out_gg2(X, ._22(X, underscore2))
member_2_in_gg2(X, ._22(underscore3, T)) -> if_member_2_in_1_gg4(X, underscore3, T, member_2_in_gg2(X, T))
if_member_2_in_1_gg4(X, underscore3, T, member_2_out_gg2(X, T)) -> member_2_out_gg2(X, ._22(underscore3, T))

The argument filtering Pi contains the following mapping:
._22(x1, x2)  =  ._22(x1, x2)
member_2_in_gg2(x1, x2)  =  member_2_in_gg2(x1, x2)
member_2_out_gg2(x1, x2)  =  member_2_out_gg
if_member_2_in_1_gg4(x1, x2, x3, x4)  =  if_member_2_in_1_gg1(x4)
SAME_SETS_2_IN_GG2(x1, x2)  =  SAME_SETS_2_IN_GG2(x1, x2)
IF_SAME_SETS_2_IN_1_GG4(x1, x2, x3, x4)  =  IF_SAME_SETS_2_IN_1_GG3(x2, 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
                ↳ UsableRulesProof
                  ↳ PiDP
                    ↳ PiDPToQDPProof
QDP
                        ↳ QDPSizeChangeProof
              ↳ PiDP

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

IF_SAME_SETS_2_IN_1_GG3(Xs, L, member_2_out_gg) -> SAME_SETS_2_IN_GG2(Xs, L)
SAME_SETS_2_IN_GG2(._22(X, Xs), L) -> IF_SAME_SETS_2_IN_1_GG3(Xs, L, member_2_in_gg2(X, L))

The TRS R consists of the following rules:

member_2_in_gg2(X, ._22(X, underscore2)) -> member_2_out_gg
member_2_in_gg2(X, ._22(underscore3, T)) -> if_member_2_in_1_gg1(member_2_in_gg2(X, T))
if_member_2_in_1_gg1(member_2_out_gg) -> member_2_out_gg

The set Q consists of the following terms:

member_2_in_gg2(x0, x1)
if_member_2_in_1_gg1(x0)

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

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



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

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

EQ_LEN1_2_IN_GG2(._22(underscore, Xs), ._22(underscore1, Ys)) -> EQ_LEN1_2_IN_GG2(Xs, Ys)

The TRS R consists of the following rules:

perm1_2_in_gg2(L, M) -> if_perm1_2_in_1_gg3(L, M, eq_len1_2_in_gg2(L, M))
eq_len1_2_in_gg2([]_0, []_0) -> eq_len1_2_out_gg2([]_0, []_0)
eq_len1_2_in_gg2(._22(underscore, Xs), ._22(underscore1, Ys)) -> if_eq_len1_2_in_1_gg5(underscore, Xs, underscore1, Ys, eq_len1_2_in_gg2(Xs, Ys))
if_eq_len1_2_in_1_gg5(underscore, Xs, underscore1, Ys, eq_len1_2_out_gg2(Xs, Ys)) -> eq_len1_2_out_gg2(._22(underscore, Xs), ._22(underscore1, Ys))
if_perm1_2_in_1_gg3(L, M, eq_len1_2_out_gg2(L, M)) -> if_perm1_2_in_2_gg3(L, M, same_sets_2_in_gg2(L, M))
same_sets_2_in_gg2([]_0, underscore4) -> same_sets_2_out_gg2([]_0, underscore4)
same_sets_2_in_gg2(._22(X, Xs), L) -> if_same_sets_2_in_1_gg4(X, Xs, L, member_2_in_gg2(X, L))
member_2_in_gg2(X, ._22(X, underscore2)) -> member_2_out_gg2(X, ._22(X, underscore2))
member_2_in_gg2(X, ._22(underscore3, T)) -> if_member_2_in_1_gg4(X, underscore3, T, member_2_in_gg2(X, T))
if_member_2_in_1_gg4(X, underscore3, T, member_2_out_gg2(X, T)) -> member_2_out_gg2(X, ._22(underscore3, T))
if_same_sets_2_in_1_gg4(X, Xs, L, member_2_out_gg2(X, L)) -> if_same_sets_2_in_2_gg4(X, Xs, L, same_sets_2_in_gg2(Xs, L))
if_same_sets_2_in_2_gg4(X, Xs, L, same_sets_2_out_gg2(Xs, L)) -> same_sets_2_out_gg2(._22(X, Xs), L)
if_perm1_2_in_2_gg3(L, M, same_sets_2_out_gg2(L, M)) -> perm1_2_out_gg2(L, M)

The argument filtering Pi contains the following mapping:
perm1_2_in_gg2(x1, x2)  =  perm1_2_in_gg2(x1, x2)
[]_0  =  []_0
._22(x1, x2)  =  ._22(x1, x2)
if_perm1_2_in_1_gg3(x1, x2, x3)  =  if_perm1_2_in_1_gg3(x1, x2, x3)
eq_len1_2_in_gg2(x1, x2)  =  eq_len1_2_in_gg2(x1, x2)
eq_len1_2_out_gg2(x1, x2)  =  eq_len1_2_out_gg
if_eq_len1_2_in_1_gg5(x1, x2, x3, x4, x5)  =  if_eq_len1_2_in_1_gg1(x5)
if_perm1_2_in_2_gg3(x1, x2, x3)  =  if_perm1_2_in_2_gg1(x3)
same_sets_2_in_gg2(x1, x2)  =  same_sets_2_in_gg2(x1, x2)
same_sets_2_out_gg2(x1, x2)  =  same_sets_2_out_gg
if_same_sets_2_in_1_gg4(x1, x2, x3, x4)  =  if_same_sets_2_in_1_gg3(x2, x3, x4)
member_2_in_gg2(x1, x2)  =  member_2_in_gg2(x1, x2)
member_2_out_gg2(x1, x2)  =  member_2_out_gg
if_member_2_in_1_gg4(x1, x2, x3, x4)  =  if_member_2_in_1_gg1(x4)
if_same_sets_2_in_2_gg4(x1, x2, x3, x4)  =  if_same_sets_2_in_2_gg1(x4)
perm1_2_out_gg2(x1, x2)  =  perm1_2_out_gg
EQ_LEN1_2_IN_GG2(x1, x2)  =  EQ_LEN1_2_IN_GG2(x1, x2)

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

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

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

EQ_LEN1_2_IN_GG2(._22(underscore, Xs), ._22(underscore1, Ys)) -> EQ_LEN1_2_IN_GG2(Xs, Ys)

R is empty.
Pi is empty.
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

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

EQ_LEN1_2_IN_GG2(._22(underscore, Xs), ._22(underscore1, Ys)) -> EQ_LEN1_2_IN_GG2(Xs, Ys)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
The head symbols of this DP problem are {EQ_LEN1_2_IN_GG2}.
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: