Left Termination of the query pattern subset_in_2(a, g) w.r.t. the given Prolog program could not be shown:

(0) Obligation:

Clauses:

subset(X, Y) :- subsetchecked(X, [], Y).
subsetchecked([], X1, X2).
subsetchecked(.(X, Xs), Ys, Zs) :- ','(member(X, Zs), ','(not_member(X, Ys), subsetchecked(Xs, .(X, Ys), Zs))).
member(X, .(X, X3)).
member(X, .(X4, Xs)) :- member(X, Xs).
not_member(X, Y) :- ','(member(X, Y), ','(!, failure(a))).
not_member(X5, X6).
failure(b).

Queries:

subset(a,g).

(1) CutEliminatorProof (SOUND transformation)

Eliminated all cuts by simply ignoring them[PROLOG].

(2) Obligation:

Clauses:

subset(X, Y) :- subsetchecked(X, [], Y).
subsetchecked([], X1, X2).
subsetchecked(.(X, Xs), Ys, Zs) :- ','(member(X, Zs), ','(not_member(X, Ys), subsetchecked(Xs, .(X, Ys), Zs))).
member(X, .(X, X3)).
member(X, .(X4, Xs)) :- member(X, Xs).
not_member(X, Y) :- ','(member(X, Y), failure(a)).
not_member(X5, X6).
failure(b).

Queries:

subset(a,g).

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
subset_in: (f,b)
subsetchecked_in: (f,b,b)
member_in: (f,b) (b,b)
not_member_in: (b,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

subset_in_ag(X, Y) → U1_ag(X, Y, subsetchecked_in_agg(X, [], Y))
subsetchecked_in_agg([], X1, X2) → subsetchecked_out_agg([], X1, X2)
subsetchecked_in_agg(.(X, Xs), Ys, Zs) → U2_agg(X, Xs, Ys, Zs, member_in_ag(X, Zs))
member_in_ag(X, .(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(X, .(X4, Xs)) → U5_ag(X, X4, Xs, member_in_ag(X, Xs))
U5_ag(X, X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))
U2_agg(X, Xs, Ys, Zs, member_out_ag(X, Zs)) → U3_agg(X, Xs, Ys, Zs, not_member_in_gg(X, Ys))
not_member_in_gg(X, Y) → U6_gg(X, Y, member_in_gg(X, Y))
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, Xs)) → U5_gg(X, X4, Xs, member_in_gg(X, Xs))
U5_gg(X, X4, Xs, member_out_gg(X, Xs)) → member_out_gg(X, .(X4, Xs))
U6_gg(X, Y, member_out_gg(X, Y)) → U7_gg(X, Y, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U7_gg(X, Y, failure_out_g(a)) → not_member_out_gg(X, Y)
not_member_in_gg(X5, X6) → not_member_out_gg(X5, X6)
U3_agg(X, Xs, Ys, Zs, not_member_out_gg(X, Ys)) → U4_agg(X, Xs, Ys, Zs, subsetchecked_in_agg(Xs, .(X, Ys), Zs))
U4_agg(X, Xs, Ys, Zs, subsetchecked_out_agg(Xs, .(X, Ys), Zs)) → subsetchecked_out_agg(.(X, Xs), Ys, Zs)
U1_ag(X, Y, subsetchecked_out_agg(X, [], Y)) → subset_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
subset_in_ag(x1, x2)  =  subset_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x2, x3)
subsetchecked_in_agg(x1, x2, x3)  =  subsetchecked_in_agg(x2, x3)
subsetchecked_out_agg(x1, x2, x3)  =  subsetchecked_out_agg(x1, x2, x3)
U2_agg(x1, x2, x3, x4, x5)  =  U2_agg(x3, x4, x5)
member_in_ag(x1, x2)  =  member_in_ag(x2)
.(x1, x2)  =  .(x1, x2)
member_out_ag(x1, x2)  =  member_out_ag(x1, x2)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x2, x3, x4)
U3_agg(x1, x2, x3, x4, x5)  =  U3_agg(x1, x3, x4, x5)
not_member_in_gg(x1, x2)  =  not_member_in_gg(x1, x2)
U6_gg(x1, x2, x3)  =  U6_gg(x1, x2, x3)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
member_out_gg(x1, x2)  =  member_out_gg(x1, x2)
U5_gg(x1, x2, x3, x4)  =  U5_gg(x1, x2, x3, x4)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
failure_in_g(x1)  =  failure_in_g(x1)
b  =  b
failure_out_g(x1)  =  failure_out_g(x1)
a  =  a
not_member_out_gg(x1, x2)  =  not_member_out_gg(x1, x2)
U4_agg(x1, x2, x3, x4, x5)  =  U4_agg(x1, x3, x4, x5)
[]  =  []
subset_out_ag(x1, x2)  =  subset_out_ag(x1, x2)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

subset_in_ag(X, Y) → U1_ag(X, Y, subsetchecked_in_agg(X, [], Y))
subsetchecked_in_agg([], X1, X2) → subsetchecked_out_agg([], X1, X2)
subsetchecked_in_agg(.(X, Xs), Ys, Zs) → U2_agg(X, Xs, Ys, Zs, member_in_ag(X, Zs))
member_in_ag(X, .(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(X, .(X4, Xs)) → U5_ag(X, X4, Xs, member_in_ag(X, Xs))
U5_ag(X, X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))
U2_agg(X, Xs, Ys, Zs, member_out_ag(X, Zs)) → U3_agg(X, Xs, Ys, Zs, not_member_in_gg(X, Ys))
not_member_in_gg(X, Y) → U6_gg(X, Y, member_in_gg(X, Y))
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, Xs)) → U5_gg(X, X4, Xs, member_in_gg(X, Xs))
U5_gg(X, X4, Xs, member_out_gg(X, Xs)) → member_out_gg(X, .(X4, Xs))
U6_gg(X, Y, member_out_gg(X, Y)) → U7_gg(X, Y, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U7_gg(X, Y, failure_out_g(a)) → not_member_out_gg(X, Y)
not_member_in_gg(X5, X6) → not_member_out_gg(X5, X6)
U3_agg(X, Xs, Ys, Zs, not_member_out_gg(X, Ys)) → U4_agg(X, Xs, Ys, Zs, subsetchecked_in_agg(Xs, .(X, Ys), Zs))
U4_agg(X, Xs, Ys, Zs, subsetchecked_out_agg(Xs, .(X, Ys), Zs)) → subsetchecked_out_agg(.(X, Xs), Ys, Zs)
U1_ag(X, Y, subsetchecked_out_agg(X, [], Y)) → subset_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
subset_in_ag(x1, x2)  =  subset_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x2, x3)
subsetchecked_in_agg(x1, x2, x3)  =  subsetchecked_in_agg(x2, x3)
subsetchecked_out_agg(x1, x2, x3)  =  subsetchecked_out_agg(x1, x2, x3)
U2_agg(x1, x2, x3, x4, x5)  =  U2_agg(x3, x4, x5)
member_in_ag(x1, x2)  =  member_in_ag(x2)
.(x1, x2)  =  .(x1, x2)
member_out_ag(x1, x2)  =  member_out_ag(x1, x2)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x2, x3, x4)
U3_agg(x1, x2, x3, x4, x5)  =  U3_agg(x1, x3, x4, x5)
not_member_in_gg(x1, x2)  =  not_member_in_gg(x1, x2)
U6_gg(x1, x2, x3)  =  U6_gg(x1, x2, x3)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
member_out_gg(x1, x2)  =  member_out_gg(x1, x2)
U5_gg(x1, x2, x3, x4)  =  U5_gg(x1, x2, x3, x4)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
failure_in_g(x1)  =  failure_in_g(x1)
b  =  b
failure_out_g(x1)  =  failure_out_g(x1)
a  =  a
not_member_out_gg(x1, x2)  =  not_member_out_gg(x1, x2)
U4_agg(x1, x2, x3, x4, x5)  =  U4_agg(x1, x3, x4, x5)
[]  =  []
subset_out_ag(x1, x2)  =  subset_out_ag(x1, x2)

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

SUBSET_IN_AG(X, Y) → U1_AG(X, Y, subsetchecked_in_agg(X, [], Y))
SUBSET_IN_AG(X, Y) → SUBSETCHECKED_IN_AGG(X, [], Y)
SUBSETCHECKED_IN_AGG(.(X, Xs), Ys, Zs) → U2_AGG(X, Xs, Ys, Zs, member_in_ag(X, Zs))
SUBSETCHECKED_IN_AGG(.(X, Xs), Ys, Zs) → MEMBER_IN_AG(X, Zs)
MEMBER_IN_AG(X, .(X4, Xs)) → U5_AG(X, X4, Xs, member_in_ag(X, Xs))
MEMBER_IN_AG(X, .(X4, Xs)) → MEMBER_IN_AG(X, Xs)
U2_AGG(X, Xs, Ys, Zs, member_out_ag(X, Zs)) → U3_AGG(X, Xs, Ys, Zs, not_member_in_gg(X, Ys))
U2_AGG(X, Xs, Ys, Zs, member_out_ag(X, Zs)) → NOT_MEMBER_IN_GG(X, Ys)
NOT_MEMBER_IN_GG(X, Y) → U6_GG(X, Y, member_in_gg(X, Y))
NOT_MEMBER_IN_GG(X, Y) → MEMBER_IN_GG(X, Y)
MEMBER_IN_GG(X, .(X4, Xs)) → U5_GG(X, X4, Xs, member_in_gg(X, Xs))
MEMBER_IN_GG(X, .(X4, Xs)) → MEMBER_IN_GG(X, Xs)
U6_GG(X, Y, member_out_gg(X, Y)) → U7_GG(X, Y, failure_in_g(a))
U6_GG(X, Y, member_out_gg(X, Y)) → FAILURE_IN_G(a)
U3_AGG(X, Xs, Ys, Zs, not_member_out_gg(X, Ys)) → U4_AGG(X, Xs, Ys, Zs, subsetchecked_in_agg(Xs, .(X, Ys), Zs))
U3_AGG(X, Xs, Ys, Zs, not_member_out_gg(X, Ys)) → SUBSETCHECKED_IN_AGG(Xs, .(X, Ys), Zs)

The TRS R consists of the following rules:

subset_in_ag(X, Y) → U1_ag(X, Y, subsetchecked_in_agg(X, [], Y))
subsetchecked_in_agg([], X1, X2) → subsetchecked_out_agg([], X1, X2)
subsetchecked_in_agg(.(X, Xs), Ys, Zs) → U2_agg(X, Xs, Ys, Zs, member_in_ag(X, Zs))
member_in_ag(X, .(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(X, .(X4, Xs)) → U5_ag(X, X4, Xs, member_in_ag(X, Xs))
U5_ag(X, X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))
U2_agg(X, Xs, Ys, Zs, member_out_ag(X, Zs)) → U3_agg(X, Xs, Ys, Zs, not_member_in_gg(X, Ys))
not_member_in_gg(X, Y) → U6_gg(X, Y, member_in_gg(X, Y))
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, Xs)) → U5_gg(X, X4, Xs, member_in_gg(X, Xs))
U5_gg(X, X4, Xs, member_out_gg(X, Xs)) → member_out_gg(X, .(X4, Xs))
U6_gg(X, Y, member_out_gg(X, Y)) → U7_gg(X, Y, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U7_gg(X, Y, failure_out_g(a)) → not_member_out_gg(X, Y)
not_member_in_gg(X5, X6) → not_member_out_gg(X5, X6)
U3_agg(X, Xs, Ys, Zs, not_member_out_gg(X, Ys)) → U4_agg(X, Xs, Ys, Zs, subsetchecked_in_agg(Xs, .(X, Ys), Zs))
U4_agg(X, Xs, Ys, Zs, subsetchecked_out_agg(Xs, .(X, Ys), Zs)) → subsetchecked_out_agg(.(X, Xs), Ys, Zs)
U1_ag(X, Y, subsetchecked_out_agg(X, [], Y)) → subset_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
subset_in_ag(x1, x2)  =  subset_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x2, x3)
subsetchecked_in_agg(x1, x2, x3)  =  subsetchecked_in_agg(x2, x3)
subsetchecked_out_agg(x1, x2, x3)  =  subsetchecked_out_agg(x1, x2, x3)
U2_agg(x1, x2, x3, x4, x5)  =  U2_agg(x3, x4, x5)
member_in_ag(x1, x2)  =  member_in_ag(x2)
.(x1, x2)  =  .(x1, x2)
member_out_ag(x1, x2)  =  member_out_ag(x1, x2)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x2, x3, x4)
U3_agg(x1, x2, x3, x4, x5)  =  U3_agg(x1, x3, x4, x5)
not_member_in_gg(x1, x2)  =  not_member_in_gg(x1, x2)
U6_gg(x1, x2, x3)  =  U6_gg(x1, x2, x3)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
member_out_gg(x1, x2)  =  member_out_gg(x1, x2)
U5_gg(x1, x2, x3, x4)  =  U5_gg(x1, x2, x3, x4)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
failure_in_g(x1)  =  failure_in_g(x1)
b  =  b
failure_out_g(x1)  =  failure_out_g(x1)
a  =  a
not_member_out_gg(x1, x2)  =  not_member_out_gg(x1, x2)
U4_agg(x1, x2, x3, x4, x5)  =  U4_agg(x1, x3, x4, x5)
[]  =  []
subset_out_ag(x1, x2)  =  subset_out_ag(x1, x2)
SUBSET_IN_AG(x1, x2)  =  SUBSET_IN_AG(x2)
U1_AG(x1, x2, x3)  =  U1_AG(x2, x3)
SUBSETCHECKED_IN_AGG(x1, x2, x3)  =  SUBSETCHECKED_IN_AGG(x2, x3)
U2_AGG(x1, x2, x3, x4, x5)  =  U2_AGG(x3, x4, x5)
MEMBER_IN_AG(x1, x2)  =  MEMBER_IN_AG(x2)
U5_AG(x1, x2, x3, x4)  =  U5_AG(x2, x3, x4)
U3_AGG(x1, x2, x3, x4, x5)  =  U3_AGG(x1, x3, x4, x5)
NOT_MEMBER_IN_GG(x1, x2)  =  NOT_MEMBER_IN_GG(x1, x2)
U6_GG(x1, x2, x3)  =  U6_GG(x1, x2, x3)
MEMBER_IN_GG(x1, x2)  =  MEMBER_IN_GG(x1, x2)
U5_GG(x1, x2, x3, x4)  =  U5_GG(x1, x2, x3, x4)
U7_GG(x1, x2, x3)  =  U7_GG(x1, x2, x3)
FAILURE_IN_G(x1)  =  FAILURE_IN_G(x1)
U4_AGG(x1, x2, x3, x4, x5)  =  U4_AGG(x1, x3, x4, x5)

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

(6) Obligation:

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

SUBSET_IN_AG(X, Y) → U1_AG(X, Y, subsetchecked_in_agg(X, [], Y))
SUBSET_IN_AG(X, Y) → SUBSETCHECKED_IN_AGG(X, [], Y)
SUBSETCHECKED_IN_AGG(.(X, Xs), Ys, Zs) → U2_AGG(X, Xs, Ys, Zs, member_in_ag(X, Zs))
SUBSETCHECKED_IN_AGG(.(X, Xs), Ys, Zs) → MEMBER_IN_AG(X, Zs)
MEMBER_IN_AG(X, .(X4, Xs)) → U5_AG(X, X4, Xs, member_in_ag(X, Xs))
MEMBER_IN_AG(X, .(X4, Xs)) → MEMBER_IN_AG(X, Xs)
U2_AGG(X, Xs, Ys, Zs, member_out_ag(X, Zs)) → U3_AGG(X, Xs, Ys, Zs, not_member_in_gg(X, Ys))
U2_AGG(X, Xs, Ys, Zs, member_out_ag(X, Zs)) → NOT_MEMBER_IN_GG(X, Ys)
NOT_MEMBER_IN_GG(X, Y) → U6_GG(X, Y, member_in_gg(X, Y))
NOT_MEMBER_IN_GG(X, Y) → MEMBER_IN_GG(X, Y)
MEMBER_IN_GG(X, .(X4, Xs)) → U5_GG(X, X4, Xs, member_in_gg(X, Xs))
MEMBER_IN_GG(X, .(X4, Xs)) → MEMBER_IN_GG(X, Xs)
U6_GG(X, Y, member_out_gg(X, Y)) → U7_GG(X, Y, failure_in_g(a))
U6_GG(X, Y, member_out_gg(X, Y)) → FAILURE_IN_G(a)
U3_AGG(X, Xs, Ys, Zs, not_member_out_gg(X, Ys)) → U4_AGG(X, Xs, Ys, Zs, subsetchecked_in_agg(Xs, .(X, Ys), Zs))
U3_AGG(X, Xs, Ys, Zs, not_member_out_gg(X, Ys)) → SUBSETCHECKED_IN_AGG(Xs, .(X, Ys), Zs)

The TRS R consists of the following rules:

subset_in_ag(X, Y) → U1_ag(X, Y, subsetchecked_in_agg(X, [], Y))
subsetchecked_in_agg([], X1, X2) → subsetchecked_out_agg([], X1, X2)
subsetchecked_in_agg(.(X, Xs), Ys, Zs) → U2_agg(X, Xs, Ys, Zs, member_in_ag(X, Zs))
member_in_ag(X, .(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(X, .(X4, Xs)) → U5_ag(X, X4, Xs, member_in_ag(X, Xs))
U5_ag(X, X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))
U2_agg(X, Xs, Ys, Zs, member_out_ag(X, Zs)) → U3_agg(X, Xs, Ys, Zs, not_member_in_gg(X, Ys))
not_member_in_gg(X, Y) → U6_gg(X, Y, member_in_gg(X, Y))
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, Xs)) → U5_gg(X, X4, Xs, member_in_gg(X, Xs))
U5_gg(X, X4, Xs, member_out_gg(X, Xs)) → member_out_gg(X, .(X4, Xs))
U6_gg(X, Y, member_out_gg(X, Y)) → U7_gg(X, Y, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U7_gg(X, Y, failure_out_g(a)) → not_member_out_gg(X, Y)
not_member_in_gg(X5, X6) → not_member_out_gg(X5, X6)
U3_agg(X, Xs, Ys, Zs, not_member_out_gg(X, Ys)) → U4_agg(X, Xs, Ys, Zs, subsetchecked_in_agg(Xs, .(X, Ys), Zs))
U4_agg(X, Xs, Ys, Zs, subsetchecked_out_agg(Xs, .(X, Ys), Zs)) → subsetchecked_out_agg(.(X, Xs), Ys, Zs)
U1_ag(X, Y, subsetchecked_out_agg(X, [], Y)) → subset_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
subset_in_ag(x1, x2)  =  subset_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x2, x3)
subsetchecked_in_agg(x1, x2, x3)  =  subsetchecked_in_agg(x2, x3)
subsetchecked_out_agg(x1, x2, x3)  =  subsetchecked_out_agg(x1, x2, x3)
U2_agg(x1, x2, x3, x4, x5)  =  U2_agg(x3, x4, x5)
member_in_ag(x1, x2)  =  member_in_ag(x2)
.(x1, x2)  =  .(x1, x2)
member_out_ag(x1, x2)  =  member_out_ag(x1, x2)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x2, x3, x4)
U3_agg(x1, x2, x3, x4, x5)  =  U3_agg(x1, x3, x4, x5)
not_member_in_gg(x1, x2)  =  not_member_in_gg(x1, x2)
U6_gg(x1, x2, x3)  =  U6_gg(x1, x2, x3)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
member_out_gg(x1, x2)  =  member_out_gg(x1, x2)
U5_gg(x1, x2, x3, x4)  =  U5_gg(x1, x2, x3, x4)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
failure_in_g(x1)  =  failure_in_g(x1)
b  =  b
failure_out_g(x1)  =  failure_out_g(x1)
a  =  a
not_member_out_gg(x1, x2)  =  not_member_out_gg(x1, x2)
U4_agg(x1, x2, x3, x4, x5)  =  U4_agg(x1, x3, x4, x5)
[]  =  []
subset_out_ag(x1, x2)  =  subset_out_ag(x1, x2)
SUBSET_IN_AG(x1, x2)  =  SUBSET_IN_AG(x2)
U1_AG(x1, x2, x3)  =  U1_AG(x2, x3)
SUBSETCHECKED_IN_AGG(x1, x2, x3)  =  SUBSETCHECKED_IN_AGG(x2, x3)
U2_AGG(x1, x2, x3, x4, x5)  =  U2_AGG(x3, x4, x5)
MEMBER_IN_AG(x1, x2)  =  MEMBER_IN_AG(x2)
U5_AG(x1, x2, x3, x4)  =  U5_AG(x2, x3, x4)
U3_AGG(x1, x2, x3, x4, x5)  =  U3_AGG(x1, x3, x4, x5)
NOT_MEMBER_IN_GG(x1, x2)  =  NOT_MEMBER_IN_GG(x1, x2)
U6_GG(x1, x2, x3)  =  U6_GG(x1, x2, x3)
MEMBER_IN_GG(x1, x2)  =  MEMBER_IN_GG(x1, x2)
U5_GG(x1, x2, x3, x4)  =  U5_GG(x1, x2, x3, x4)
U7_GG(x1, x2, x3)  =  U7_GG(x1, x2, x3)
FAILURE_IN_G(x1)  =  FAILURE_IN_G(x1)
U4_AGG(x1, x2, x3, x4, x5)  =  U4_AGG(x1, x3, x4, x5)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 11 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

MEMBER_IN_GG(X, .(X4, Xs)) → MEMBER_IN_GG(X, Xs)

The TRS R consists of the following rules:

subset_in_ag(X, Y) → U1_ag(X, Y, subsetchecked_in_agg(X, [], Y))
subsetchecked_in_agg([], X1, X2) → subsetchecked_out_agg([], X1, X2)
subsetchecked_in_agg(.(X, Xs), Ys, Zs) → U2_agg(X, Xs, Ys, Zs, member_in_ag(X, Zs))
member_in_ag(X, .(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(X, .(X4, Xs)) → U5_ag(X, X4, Xs, member_in_ag(X, Xs))
U5_ag(X, X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))
U2_agg(X, Xs, Ys, Zs, member_out_ag(X, Zs)) → U3_agg(X, Xs, Ys, Zs, not_member_in_gg(X, Ys))
not_member_in_gg(X, Y) → U6_gg(X, Y, member_in_gg(X, Y))
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, Xs)) → U5_gg(X, X4, Xs, member_in_gg(X, Xs))
U5_gg(X, X4, Xs, member_out_gg(X, Xs)) → member_out_gg(X, .(X4, Xs))
U6_gg(X, Y, member_out_gg(X, Y)) → U7_gg(X, Y, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U7_gg(X, Y, failure_out_g(a)) → not_member_out_gg(X, Y)
not_member_in_gg(X5, X6) → not_member_out_gg(X5, X6)
U3_agg(X, Xs, Ys, Zs, not_member_out_gg(X, Ys)) → U4_agg(X, Xs, Ys, Zs, subsetchecked_in_agg(Xs, .(X, Ys), Zs))
U4_agg(X, Xs, Ys, Zs, subsetchecked_out_agg(Xs, .(X, Ys), Zs)) → subsetchecked_out_agg(.(X, Xs), Ys, Zs)
U1_ag(X, Y, subsetchecked_out_agg(X, [], Y)) → subset_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
subset_in_ag(x1, x2)  =  subset_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x2, x3)
subsetchecked_in_agg(x1, x2, x3)  =  subsetchecked_in_agg(x2, x3)
subsetchecked_out_agg(x1, x2, x3)  =  subsetchecked_out_agg(x1, x2, x3)
U2_agg(x1, x2, x3, x4, x5)  =  U2_agg(x3, x4, x5)
member_in_ag(x1, x2)  =  member_in_ag(x2)
.(x1, x2)  =  .(x1, x2)
member_out_ag(x1, x2)  =  member_out_ag(x1, x2)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x2, x3, x4)
U3_agg(x1, x2, x3, x4, x5)  =  U3_agg(x1, x3, x4, x5)
not_member_in_gg(x1, x2)  =  not_member_in_gg(x1, x2)
U6_gg(x1, x2, x3)  =  U6_gg(x1, x2, x3)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
member_out_gg(x1, x2)  =  member_out_gg(x1, x2)
U5_gg(x1, x2, x3, x4)  =  U5_gg(x1, x2, x3, x4)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
failure_in_g(x1)  =  failure_in_g(x1)
b  =  b
failure_out_g(x1)  =  failure_out_g(x1)
a  =  a
not_member_out_gg(x1, x2)  =  not_member_out_gg(x1, x2)
U4_agg(x1, x2, x3, x4, x5)  =  U4_agg(x1, x3, x4, x5)
[]  =  []
subset_out_ag(x1, x2)  =  subset_out_ag(x1, x2)
MEMBER_IN_GG(x1, x2)  =  MEMBER_IN_GG(x1, x2)

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

(10) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(11) Obligation:

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

MEMBER_IN_GG(X, .(X4, Xs)) → MEMBER_IN_GG(X, Xs)

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

(12) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(13) Obligation:

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

MEMBER_IN_GG(X, .(X4, Xs)) → MEMBER_IN_GG(X, Xs)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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_IN_GG(X, .(X4, Xs)) → MEMBER_IN_GG(X, Xs)
  The graph contains the following edges 1 >= 1, 2 > 2

(15) TRUE

(16) Obligation:

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

MEMBER_IN_AG(X, .(X4, Xs)) → MEMBER_IN_AG(X, Xs)

The TRS R consists of the following rules:

subset_in_ag(X, Y) → U1_ag(X, Y, subsetchecked_in_agg(X, [], Y))
subsetchecked_in_agg([], X1, X2) → subsetchecked_out_agg([], X1, X2)
subsetchecked_in_agg(.(X, Xs), Ys, Zs) → U2_agg(X, Xs, Ys, Zs, member_in_ag(X, Zs))
member_in_ag(X, .(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(X, .(X4, Xs)) → U5_ag(X, X4, Xs, member_in_ag(X, Xs))
U5_ag(X, X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))
U2_agg(X, Xs, Ys, Zs, member_out_ag(X, Zs)) → U3_agg(X, Xs, Ys, Zs, not_member_in_gg(X, Ys))
not_member_in_gg(X, Y) → U6_gg(X, Y, member_in_gg(X, Y))
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, Xs)) → U5_gg(X, X4, Xs, member_in_gg(X, Xs))
U5_gg(X, X4, Xs, member_out_gg(X, Xs)) → member_out_gg(X, .(X4, Xs))
U6_gg(X, Y, member_out_gg(X, Y)) → U7_gg(X, Y, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U7_gg(X, Y, failure_out_g(a)) → not_member_out_gg(X, Y)
not_member_in_gg(X5, X6) → not_member_out_gg(X5, X6)
U3_agg(X, Xs, Ys, Zs, not_member_out_gg(X, Ys)) → U4_agg(X, Xs, Ys, Zs, subsetchecked_in_agg(Xs, .(X, Ys), Zs))
U4_agg(X, Xs, Ys, Zs, subsetchecked_out_agg(Xs, .(X, Ys), Zs)) → subsetchecked_out_agg(.(X, Xs), Ys, Zs)
U1_ag(X, Y, subsetchecked_out_agg(X, [], Y)) → subset_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
subset_in_ag(x1, x2)  =  subset_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x2, x3)
subsetchecked_in_agg(x1, x2, x3)  =  subsetchecked_in_agg(x2, x3)
subsetchecked_out_agg(x1, x2, x3)  =  subsetchecked_out_agg(x1, x2, x3)
U2_agg(x1, x2, x3, x4, x5)  =  U2_agg(x3, x4, x5)
member_in_ag(x1, x2)  =  member_in_ag(x2)
.(x1, x2)  =  .(x1, x2)
member_out_ag(x1, x2)  =  member_out_ag(x1, x2)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x2, x3, x4)
U3_agg(x1, x2, x3, x4, x5)  =  U3_agg(x1, x3, x4, x5)
not_member_in_gg(x1, x2)  =  not_member_in_gg(x1, x2)
U6_gg(x1, x2, x3)  =  U6_gg(x1, x2, x3)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
member_out_gg(x1, x2)  =  member_out_gg(x1, x2)
U5_gg(x1, x2, x3, x4)  =  U5_gg(x1, x2, x3, x4)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
failure_in_g(x1)  =  failure_in_g(x1)
b  =  b
failure_out_g(x1)  =  failure_out_g(x1)
a  =  a
not_member_out_gg(x1, x2)  =  not_member_out_gg(x1, x2)
U4_agg(x1, x2, x3, x4, x5)  =  U4_agg(x1, x3, x4, x5)
[]  =  []
subset_out_ag(x1, x2)  =  subset_out_ag(x1, x2)
MEMBER_IN_AG(x1, x2)  =  MEMBER_IN_AG(x2)

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

(17) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(18) Obligation:

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

MEMBER_IN_AG(X, .(X4, Xs)) → MEMBER_IN_AG(X, Xs)

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

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

(19) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(20) Obligation:

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

MEMBER_IN_AG(.(X4, Xs)) → MEMBER_IN_AG(Xs)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(21) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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_IN_AG(.(X4, Xs)) → MEMBER_IN_AG(Xs)
  The graph contains the following edges 1 > 1

(22) TRUE

(23) Obligation:

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

U2_AGG(X, Xs, Ys, Zs, member_out_ag(X, Zs)) → U3_AGG(X, Xs, Ys, Zs, not_member_in_gg(X, Ys))
U3_AGG(X, Xs, Ys, Zs, not_member_out_gg(X, Ys)) → SUBSETCHECKED_IN_AGG(Xs, .(X, Ys), Zs)
SUBSETCHECKED_IN_AGG(.(X, Xs), Ys, Zs) → U2_AGG(X, Xs, Ys, Zs, member_in_ag(X, Zs))

The TRS R consists of the following rules:

subset_in_ag(X, Y) → U1_ag(X, Y, subsetchecked_in_agg(X, [], Y))
subsetchecked_in_agg([], X1, X2) → subsetchecked_out_agg([], X1, X2)
subsetchecked_in_agg(.(X, Xs), Ys, Zs) → U2_agg(X, Xs, Ys, Zs, member_in_ag(X, Zs))
member_in_ag(X, .(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(X, .(X4, Xs)) → U5_ag(X, X4, Xs, member_in_ag(X, Xs))
U5_ag(X, X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))
U2_agg(X, Xs, Ys, Zs, member_out_ag(X, Zs)) → U3_agg(X, Xs, Ys, Zs, not_member_in_gg(X, Ys))
not_member_in_gg(X, Y) → U6_gg(X, Y, member_in_gg(X, Y))
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, Xs)) → U5_gg(X, X4, Xs, member_in_gg(X, Xs))
U5_gg(X, X4, Xs, member_out_gg(X, Xs)) → member_out_gg(X, .(X4, Xs))
U6_gg(X, Y, member_out_gg(X, Y)) → U7_gg(X, Y, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U7_gg(X, Y, failure_out_g(a)) → not_member_out_gg(X, Y)
not_member_in_gg(X5, X6) → not_member_out_gg(X5, X6)
U3_agg(X, Xs, Ys, Zs, not_member_out_gg(X, Ys)) → U4_agg(X, Xs, Ys, Zs, subsetchecked_in_agg(Xs, .(X, Ys), Zs))
U4_agg(X, Xs, Ys, Zs, subsetchecked_out_agg(Xs, .(X, Ys), Zs)) → subsetchecked_out_agg(.(X, Xs), Ys, Zs)
U1_ag(X, Y, subsetchecked_out_agg(X, [], Y)) → subset_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
subset_in_ag(x1, x2)  =  subset_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x2, x3)
subsetchecked_in_agg(x1, x2, x3)  =  subsetchecked_in_agg(x2, x3)
subsetchecked_out_agg(x1, x2, x3)  =  subsetchecked_out_agg(x1, x2, x3)
U2_agg(x1, x2, x3, x4, x5)  =  U2_agg(x3, x4, x5)
member_in_ag(x1, x2)  =  member_in_ag(x2)
.(x1, x2)  =  .(x1, x2)
member_out_ag(x1, x2)  =  member_out_ag(x1, x2)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x2, x3, x4)
U3_agg(x1, x2, x3, x4, x5)  =  U3_agg(x1, x3, x4, x5)
not_member_in_gg(x1, x2)  =  not_member_in_gg(x1, x2)
U6_gg(x1, x2, x3)  =  U6_gg(x1, x2, x3)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
member_out_gg(x1, x2)  =  member_out_gg(x1, x2)
U5_gg(x1, x2, x3, x4)  =  U5_gg(x1, x2, x3, x4)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
failure_in_g(x1)  =  failure_in_g(x1)
b  =  b
failure_out_g(x1)  =  failure_out_g(x1)
a  =  a
not_member_out_gg(x1, x2)  =  not_member_out_gg(x1, x2)
U4_agg(x1, x2, x3, x4, x5)  =  U4_agg(x1, x3, x4, x5)
[]  =  []
subset_out_ag(x1, x2)  =  subset_out_ag(x1, x2)
SUBSETCHECKED_IN_AGG(x1, x2, x3)  =  SUBSETCHECKED_IN_AGG(x2, x3)
U2_AGG(x1, x2, x3, x4, x5)  =  U2_AGG(x3, x4, x5)
U3_AGG(x1, x2, x3, x4, x5)  =  U3_AGG(x1, x3, x4, x5)

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

(24) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(25) Obligation:

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

U2_AGG(X, Xs, Ys, Zs, member_out_ag(X, Zs)) → U3_AGG(X, Xs, Ys, Zs, not_member_in_gg(X, Ys))
U3_AGG(X, Xs, Ys, Zs, not_member_out_gg(X, Ys)) → SUBSETCHECKED_IN_AGG(Xs, .(X, Ys), Zs)
SUBSETCHECKED_IN_AGG(.(X, Xs), Ys, Zs) → U2_AGG(X, Xs, Ys, Zs, member_in_ag(X, Zs))

The TRS R consists of the following rules:

not_member_in_gg(X, Y) → U6_gg(X, Y, member_in_gg(X, Y))
not_member_in_gg(X5, X6) → not_member_out_gg(X5, X6)
member_in_ag(X, .(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(X, .(X4, Xs)) → U5_ag(X, X4, Xs, member_in_ag(X, Xs))
U6_gg(X, Y, member_out_gg(X, Y)) → U7_gg(X, Y, failure_in_g(a))
U5_ag(X, X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, Xs)) → U5_gg(X, X4, Xs, member_in_gg(X, Xs))
U5_gg(X, X4, Xs, member_out_gg(X, Xs)) → member_out_gg(X, .(X4, Xs))

The argument filtering Pi contains the following mapping:
member_in_ag(x1, x2)  =  member_in_ag(x2)
.(x1, x2)  =  .(x1, x2)
member_out_ag(x1, x2)  =  member_out_ag(x1, x2)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x2, x3, x4)
not_member_in_gg(x1, x2)  =  not_member_in_gg(x1, x2)
U6_gg(x1, x2, x3)  =  U6_gg(x1, x2, x3)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
member_out_gg(x1, x2)  =  member_out_gg(x1, x2)
U5_gg(x1, x2, x3, x4)  =  U5_gg(x1, x2, x3, x4)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
failure_in_g(x1)  =  failure_in_g(x1)
a  =  a
not_member_out_gg(x1, x2)  =  not_member_out_gg(x1, x2)
SUBSETCHECKED_IN_AGG(x1, x2, x3)  =  SUBSETCHECKED_IN_AGG(x2, x3)
U2_AGG(x1, x2, x3, x4, x5)  =  U2_AGG(x3, x4, x5)
U3_AGG(x1, x2, x3, x4, x5)  =  U3_AGG(x1, x3, x4, x5)

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

(26) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(27) Obligation:

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

U2_AGG(Ys, Zs, member_out_ag(X, Zs)) → U3_AGG(X, Ys, Zs, not_member_in_gg(X, Ys))
U3_AGG(X, Ys, Zs, not_member_out_gg(X, Ys)) → SUBSETCHECKED_IN_AGG(.(X, Ys), Zs)
SUBSETCHECKED_IN_AGG(Ys, Zs) → U2_AGG(Ys, Zs, member_in_ag(Zs))

The TRS R consists of the following rules:

not_member_in_gg(X, Y) → U6_gg(X, Y, member_in_gg(X, Y))
not_member_in_gg(X5, X6) → not_member_out_gg(X5, X6)
member_in_ag(.(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(.(X4, Xs)) → U5_ag(X4, Xs, member_in_ag(Xs))
U6_gg(X, Y, member_out_gg(X, Y)) → U7_gg(X, Y, failure_in_g(a))
U5_ag(X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, Xs)) → U5_gg(X, X4, Xs, member_in_gg(X, Xs))
U5_gg(X, X4, Xs, member_out_gg(X, Xs)) → member_out_gg(X, .(X4, Xs))

The set Q consists of the following terms:

not_member_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0, x1, x2)
U5_ag(x0, x1, x2)
member_in_gg(x0, x1)
U5_gg(x0, x1, x2, x3)

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

(28) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule SUBSETCHECKED_IN_AGG(Ys, Zs) → U2_AGG(Ys, Zs, member_in_ag(Zs)) we obtained the following new rules [LPAR04]:

SUBSETCHECKED_IN_AGG(.(z0, z1), z2) → U2_AGG(.(z0, z1), z2, member_in_ag(z2))

(29) Obligation:

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

U2_AGG(Ys, Zs, member_out_ag(X, Zs)) → U3_AGG(X, Ys, Zs, not_member_in_gg(X, Ys))
U3_AGG(X, Ys, Zs, not_member_out_gg(X, Ys)) → SUBSETCHECKED_IN_AGG(.(X, Ys), Zs)
SUBSETCHECKED_IN_AGG(.(z0, z1), z2) → U2_AGG(.(z0, z1), z2, member_in_ag(z2))

The TRS R consists of the following rules:

not_member_in_gg(X, Y) → U6_gg(X, Y, member_in_gg(X, Y))
not_member_in_gg(X5, X6) → not_member_out_gg(X5, X6)
member_in_ag(.(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(.(X4, Xs)) → U5_ag(X4, Xs, member_in_ag(Xs))
U6_gg(X, Y, member_out_gg(X, Y)) → U7_gg(X, Y, failure_in_g(a))
U5_ag(X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, Xs)) → U5_gg(X, X4, Xs, member_in_gg(X, Xs))
U5_gg(X, X4, Xs, member_out_gg(X, Xs)) → member_out_gg(X, .(X4, Xs))

The set Q consists of the following terms:

not_member_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0, x1, x2)
U5_ag(x0, x1, x2)
member_in_gg(x0, x1)
U5_gg(x0, x1, x2, x3)

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

(30) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U2_AGG(Ys, Zs, member_out_ag(X, Zs)) → U3_AGG(X, Ys, Zs, not_member_in_gg(X, Ys)) at position [3] we obtained the following new rules [LPAR04]:

U2_AGG(x1, y1, member_out_ag(x0, y1)) → U3_AGG(x0, x1, y1, U6_gg(x0, x1, member_in_gg(x0, x1)))
U2_AGG(x1, y1, member_out_ag(x0, y1)) → U3_AGG(x0, x1, y1, not_member_out_gg(x0, x1))

(31) Obligation:

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

U3_AGG(X, Ys, Zs, not_member_out_gg(X, Ys)) → SUBSETCHECKED_IN_AGG(.(X, Ys), Zs)
SUBSETCHECKED_IN_AGG(Ys, Zs) → U2_AGG(Ys, Zs, member_in_ag(Zs))
U2_AGG(x1, y1, member_out_ag(x0, y1)) → U3_AGG(x0, x1, y1, U6_gg(x0, x1, member_in_gg(x0, x1)))
U2_AGG(x1, y1, member_out_ag(x0, y1)) → U3_AGG(x0, x1, y1, not_member_out_gg(x0, x1))

The TRS R consists of the following rules:

not_member_in_gg(X, Y) → U6_gg(X, Y, member_in_gg(X, Y))
not_member_in_gg(X5, X6) → not_member_out_gg(X5, X6)
member_in_ag(.(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(.(X4, Xs)) → U5_ag(X4, Xs, member_in_ag(Xs))
U6_gg(X, Y, member_out_gg(X, Y)) → U7_gg(X, Y, failure_in_g(a))
U5_ag(X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, Xs)) → U5_gg(X, X4, Xs, member_in_gg(X, Xs))
U5_gg(X, X4, Xs, member_out_gg(X, Xs)) → member_out_gg(X, .(X4, Xs))

The set Q consists of the following terms:

not_member_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0, x1, x2)
U5_ag(x0, x1, x2)
member_in_gg(x0, x1)
U5_gg(x0, x1, x2, x3)

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

(32) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(33) Obligation:

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

SUBSETCHECKED_IN_AGG(Ys, Zs) → U2_AGG(Ys, Zs, member_in_ag(Zs))
U2_AGG(x1, y1, member_out_ag(x0, y1)) → U3_AGG(x0, x1, y1, not_member_out_gg(x0, x1))
U3_AGG(X, Ys, Zs, not_member_out_gg(X, Ys)) → SUBSETCHECKED_IN_AGG(.(X, Ys), Zs)

The TRS R consists of the following rules:

not_member_in_gg(X, Y) → U6_gg(X, Y, member_in_gg(X, Y))
not_member_in_gg(X5, X6) → not_member_out_gg(X5, X6)
member_in_ag(.(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(.(X4, Xs)) → U5_ag(X4, Xs, member_in_ag(Xs))
U6_gg(X, Y, member_out_gg(X, Y)) → U7_gg(X, Y, failure_in_g(a))
U5_ag(X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, Xs)) → U5_gg(X, X4, Xs, member_in_gg(X, Xs))
U5_gg(X, X4, Xs, member_out_gg(X, Xs)) → member_out_gg(X, .(X4, Xs))

The set Q consists of the following terms:

not_member_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0, x1, x2)
U5_ag(x0, x1, x2)
member_in_gg(x0, x1)
U5_gg(x0, x1, x2, x3)

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

(34) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(35) Obligation:

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

SUBSETCHECKED_IN_AGG(Ys, Zs) → U2_AGG(Ys, Zs, member_in_ag(Zs))
U2_AGG(x1, y1, member_out_ag(x0, y1)) → U3_AGG(x0, x1, y1, not_member_out_gg(x0, x1))
U3_AGG(X, Ys, Zs, not_member_out_gg(X, Ys)) → SUBSETCHECKED_IN_AGG(.(X, Ys), Zs)

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(.(X4, Xs)) → U5_ag(X4, Xs, member_in_ag(Xs))
U5_ag(X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))

The set Q consists of the following terms:

not_member_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0, x1, x2)
U5_ag(x0, x1, x2)
member_in_gg(x0, x1)
U5_gg(x0, x1, x2, x3)

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

(36) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

not_member_in_gg(x0, x1)
U6_gg(x0, x1, x2)
member_in_gg(x0, x1)
U5_gg(x0, x1, x2, x3)

(37) Obligation:

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

SUBSETCHECKED_IN_AGG(Ys, Zs) → U2_AGG(Ys, Zs, member_in_ag(Zs))
U2_AGG(x1, y1, member_out_ag(x0, y1)) → U3_AGG(x0, x1, y1, not_member_out_gg(x0, x1))
U3_AGG(X, Ys, Zs, not_member_out_gg(X, Ys)) → SUBSETCHECKED_IN_AGG(.(X, Ys), Zs)

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(.(X4, Xs)) → U5_ag(X4, Xs, member_in_ag(Xs))
U5_ag(X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0, x1, x2)

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

(38) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule SUBSETCHECKED_IN_AGG(Ys, Zs) → U2_AGG(Ys, Zs, member_in_ag(Zs)) at position [2] we obtained the following new rules [LPAR04]:

SUBSETCHECKED_IN_AGG(y0, .(x0, x1)) → U2_AGG(y0, .(x0, x1), member_out_ag(x0, .(x0, x1)))
SUBSETCHECKED_IN_AGG(y0, .(x0, x1)) → U2_AGG(y0, .(x0, x1), U5_ag(x0, x1, member_in_ag(x1)))

(39) Obligation:

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

U2_AGG(x1, y1, member_out_ag(x0, y1)) → U3_AGG(x0, x1, y1, not_member_out_gg(x0, x1))
U3_AGG(X, Ys, Zs, not_member_out_gg(X, Ys)) → SUBSETCHECKED_IN_AGG(.(X, Ys), Zs)
SUBSETCHECKED_IN_AGG(y0, .(x0, x1)) → U2_AGG(y0, .(x0, x1), member_out_ag(x0, .(x0, x1)))
SUBSETCHECKED_IN_AGG(y0, .(x0, x1)) → U2_AGG(y0, .(x0, x1), U5_ag(x0, x1, member_in_ag(x1)))

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(.(X4, Xs)) → U5_ag(X4, Xs, member_in_ag(Xs))
U5_ag(X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0, x1, x2)

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

(40) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U2_AGG(x1, y1, member_out_ag(x0, y1)) → U3_AGG(x0, x1, y1, not_member_out_gg(x0, x1)) we obtained the following new rules [LPAR04]:

U2_AGG(z0, .(z1, z2), member_out_ag(z1, .(z1, z2))) → U3_AGG(z1, z0, .(z1, z2), not_member_out_gg(z1, z0))
U2_AGG(z0, .(z1, z2), member_out_ag(x2, .(z1, z2))) → U3_AGG(x2, z0, .(z1, z2), not_member_out_gg(x2, z0))

(41) Obligation:

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

U3_AGG(X, Ys, Zs, not_member_out_gg(X, Ys)) → SUBSETCHECKED_IN_AGG(.(X, Ys), Zs)
SUBSETCHECKED_IN_AGG(y0, .(x0, x1)) → U2_AGG(y0, .(x0, x1), member_out_ag(x0, .(x0, x1)))
SUBSETCHECKED_IN_AGG(y0, .(x0, x1)) → U2_AGG(y0, .(x0, x1), U5_ag(x0, x1, member_in_ag(x1)))
U2_AGG(z0, .(z1, z2), member_out_ag(z1, .(z1, z2))) → U3_AGG(z1, z0, .(z1, z2), not_member_out_gg(z1, z0))
U2_AGG(z0, .(z1, z2), member_out_ag(x2, .(z1, z2))) → U3_AGG(x2, z0, .(z1, z2), not_member_out_gg(x2, z0))

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(.(X4, Xs)) → U5_ag(X4, Xs, member_in_ag(Xs))
U5_ag(X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0, x1, x2)

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

(42) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U3_AGG(X, Ys, Zs, not_member_out_gg(X, Ys)) → SUBSETCHECKED_IN_AGG(.(X, Ys), Zs) we obtained the following new rules [LPAR04]:

U3_AGG(z1, z0, .(z1, z2), not_member_out_gg(z1, z0)) → SUBSETCHECKED_IN_AGG(.(z1, z0), .(z1, z2))
U3_AGG(z3, z0, .(z1, z2), not_member_out_gg(z3, z0)) → SUBSETCHECKED_IN_AGG(.(z3, z0), .(z1, z2))

(43) Obligation:

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

SUBSETCHECKED_IN_AGG(y0, .(x0, x1)) → U2_AGG(y0, .(x0, x1), member_out_ag(x0, .(x0, x1)))
SUBSETCHECKED_IN_AGG(y0, .(x0, x1)) → U2_AGG(y0, .(x0, x1), U5_ag(x0, x1, member_in_ag(x1)))
U2_AGG(z0, .(z1, z2), member_out_ag(z1, .(z1, z2))) → U3_AGG(z1, z0, .(z1, z2), not_member_out_gg(z1, z0))
U2_AGG(z0, .(z1, z2), member_out_ag(x2, .(z1, z2))) → U3_AGG(x2, z0, .(z1, z2), not_member_out_gg(x2, z0))
U3_AGG(z1, z0, .(z1, z2), not_member_out_gg(z1, z0)) → SUBSETCHECKED_IN_AGG(.(z1, z0), .(z1, z2))
U3_AGG(z3, z0, .(z1, z2), not_member_out_gg(z3, z0)) → SUBSETCHECKED_IN_AGG(.(z3, z0), .(z1, z2))

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(.(X4, Xs)) → U5_ag(X4, Xs, member_in_ag(Xs))
U5_ag(X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0, x1, x2)

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

(44) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule SUBSETCHECKED_IN_AGG(y0, .(x0, x1)) → U2_AGG(y0, .(x0, x1), member_out_ag(x0, .(x0, x1))) we obtained the following new rules [LPAR04]:

SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0, .(z0, z2)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2, .(z2, z3)))

(45) Obligation:

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

SUBSETCHECKED_IN_AGG(y0, .(x0, x1)) → U2_AGG(y0, .(x0, x1), U5_ag(x0, x1, member_in_ag(x1)))
U2_AGG(z0, .(z1, z2), member_out_ag(z1, .(z1, z2))) → U3_AGG(z1, z0, .(z1, z2), not_member_out_gg(z1, z0))
U2_AGG(z0, .(z1, z2), member_out_ag(x2, .(z1, z2))) → U3_AGG(x2, z0, .(z1, z2), not_member_out_gg(x2, z0))
U3_AGG(z1, z0, .(z1, z2), not_member_out_gg(z1, z0)) → SUBSETCHECKED_IN_AGG(.(z1, z0), .(z1, z2))
U3_AGG(z3, z0, .(z1, z2), not_member_out_gg(z3, z0)) → SUBSETCHECKED_IN_AGG(.(z3, z0), .(z1, z2))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0, .(z0, z2)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2, .(z2, z3)))

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(.(X4, Xs)) → U5_ag(X4, Xs, member_in_ag(Xs))
U5_ag(X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0, x1, x2)

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

(46) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule SUBSETCHECKED_IN_AGG(y0, .(x0, x1)) → U2_AGG(y0, .(x0, x1), U5_ag(x0, x1, member_in_ag(x1))) we obtained the following new rules [LPAR04]:

SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), U5_ag(z0, z2, member_in_ag(z2)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), U5_ag(z2, z3, member_in_ag(z3)))

(47) Obligation:

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

U2_AGG(z0, .(z1, z2), member_out_ag(z1, .(z1, z2))) → U3_AGG(z1, z0, .(z1, z2), not_member_out_gg(z1, z0))
U2_AGG(z0, .(z1, z2), member_out_ag(x2, .(z1, z2))) → U3_AGG(x2, z0, .(z1, z2), not_member_out_gg(x2, z0))
U3_AGG(z1, z0, .(z1, z2), not_member_out_gg(z1, z0)) → SUBSETCHECKED_IN_AGG(.(z1, z0), .(z1, z2))
U3_AGG(z3, z0, .(z1, z2), not_member_out_gg(z3, z0)) → SUBSETCHECKED_IN_AGG(.(z3, z0), .(z1, z2))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0, .(z0, z2)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2, .(z2, z3)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), U5_ag(z0, z2, member_in_ag(z2)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), U5_ag(z2, z3, member_in_ag(z3)))

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(.(X4, Xs)) → U5_ag(X4, Xs, member_in_ag(Xs))
U5_ag(X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0, x1, x2)

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

(48) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U2_AGG(z0, .(z1, z2), member_out_ag(z1, .(z1, z2))) → U3_AGG(z1, z0, .(z1, z2), not_member_out_gg(z1, z0)) we obtained the following new rules [LPAR04]:

U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0, .(z0, z2))) → U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg(z0, .(z0, z1)))
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2, .(z2, z3))) → U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg(z2, .(z0, z1)))

(49) Obligation:

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

U2_AGG(z0, .(z1, z2), member_out_ag(x2, .(z1, z2))) → U3_AGG(x2, z0, .(z1, z2), not_member_out_gg(x2, z0))
U3_AGG(z1, z0, .(z1, z2), not_member_out_gg(z1, z0)) → SUBSETCHECKED_IN_AGG(.(z1, z0), .(z1, z2))
U3_AGG(z3, z0, .(z1, z2), not_member_out_gg(z3, z0)) → SUBSETCHECKED_IN_AGG(.(z3, z0), .(z1, z2))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0, .(z0, z2)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2, .(z2, z3)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), U5_ag(z0, z2, member_in_ag(z2)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), U5_ag(z2, z3, member_in_ag(z3)))
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0, .(z0, z2))) → U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg(z0, .(z0, z1)))
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2, .(z2, z3))) → U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg(z2, .(z0, z1)))

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(.(X4, Xs)) → U5_ag(X4, Xs, member_in_ag(Xs))
U5_ag(X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0, x1, x2)

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

(50) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U2_AGG(z0, .(z1, z2), member_out_ag(x2, .(z1, z2))) → U3_AGG(x2, z0, .(z1, z2), not_member_out_gg(x2, z0)) we obtained the following new rules [LPAR04]:

U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0, .(z0, z2))) → U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg(z0, .(z0, z1)))
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2, .(z2, z3))) → U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg(z2, .(z0, z1)))
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(x3, .(z0, z2))) → U3_AGG(x3, .(z0, z1), .(z0, z2), not_member_out_gg(x3, .(z0, z1)))
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(x3, .(z2, z3))) → U3_AGG(x3, .(z0, z1), .(z2, z3), not_member_out_gg(x3, .(z0, z1)))

(51) Obligation:

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

U3_AGG(z1, z0, .(z1, z2), not_member_out_gg(z1, z0)) → SUBSETCHECKED_IN_AGG(.(z1, z0), .(z1, z2))
U3_AGG(z3, z0, .(z1, z2), not_member_out_gg(z3, z0)) → SUBSETCHECKED_IN_AGG(.(z3, z0), .(z1, z2))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0, .(z0, z2)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2, .(z2, z3)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), U5_ag(z0, z2, member_in_ag(z2)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), U5_ag(z2, z3, member_in_ag(z3)))
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0, .(z0, z2))) → U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg(z0, .(z0, z1)))
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2, .(z2, z3))) → U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg(z2, .(z0, z1)))
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(x3, .(z0, z2))) → U3_AGG(x3, .(z0, z1), .(z0, z2), not_member_out_gg(x3, .(z0, z1)))
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(x3, .(z2, z3))) → U3_AGG(x3, .(z0, z1), .(z2, z3), not_member_out_gg(x3, .(z0, z1)))

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(.(X4, Xs)) → U5_ag(X4, Xs, member_in_ag(Xs))
U5_ag(X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0, x1, x2)

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

(52) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U3_AGG(z1, z0, .(z1, z2), not_member_out_gg(z1, z0)) → SUBSETCHECKED_IN_AGG(.(z1, z0), .(z1, z2)) we obtained the following new rules [LPAR04]:

U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg(z0, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2))
U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg(z2, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z2, .(z0, z1)), .(z2, z3))

(53) Obligation:

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

U3_AGG(z3, z0, .(z1, z2), not_member_out_gg(z3, z0)) → SUBSETCHECKED_IN_AGG(.(z3, z0), .(z1, z2))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0, .(z0, z2)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2, .(z2, z3)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), U5_ag(z0, z2, member_in_ag(z2)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), U5_ag(z2, z3, member_in_ag(z3)))
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0, .(z0, z2))) → U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg(z0, .(z0, z1)))
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2, .(z2, z3))) → U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg(z2, .(z0, z1)))
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(x3, .(z0, z2))) → U3_AGG(x3, .(z0, z1), .(z0, z2), not_member_out_gg(x3, .(z0, z1)))
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(x3, .(z2, z3))) → U3_AGG(x3, .(z0, z1), .(z2, z3), not_member_out_gg(x3, .(z0, z1)))
U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg(z0, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2))
U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg(z2, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z2, .(z0, z1)), .(z2, z3))

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(.(X4, Xs)) → U5_ag(X4, Xs, member_in_ag(Xs))
U5_ag(X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0, x1, x2)

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

(54) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U3_AGG(z3, z0, .(z1, z2), not_member_out_gg(z3, z0)) → SUBSETCHECKED_IN_AGG(.(z3, z0), .(z1, z2)) we obtained the following new rules [LPAR04]:

U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg(z0, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2))
U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg(z2, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z2, .(z0, z1)), .(z2, z3))
U3_AGG(z3, .(z0, z1), .(z0, z2), not_member_out_gg(z3, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z3, .(z0, z1)), .(z0, z2))
U3_AGG(z4, .(z0, z1), .(z2, z3), not_member_out_gg(z4, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z4, .(z0, z1)), .(z2, z3))

(55) Obligation:

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

SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0, .(z0, z2)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2, .(z2, z3)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), U5_ag(z0, z2, member_in_ag(z2)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), U5_ag(z2, z3, member_in_ag(z3)))
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0, .(z0, z2))) → U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg(z0, .(z0, z1)))
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2, .(z2, z3))) → U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg(z2, .(z0, z1)))
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(x3, .(z0, z2))) → U3_AGG(x3, .(z0, z1), .(z0, z2), not_member_out_gg(x3, .(z0, z1)))
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(x3, .(z2, z3))) → U3_AGG(x3, .(z0, z1), .(z2, z3), not_member_out_gg(x3, .(z0, z1)))
U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg(z0, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2))
U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg(z2, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z2, .(z0, z1)), .(z2, z3))
U3_AGG(z3, .(z0, z1), .(z0, z2), not_member_out_gg(z3, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z3, .(z0, z1)), .(z0, z2))
U3_AGG(z4, .(z0, z1), .(z2, z3), not_member_out_gg(z4, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z4, .(z0, z1)), .(z2, z3))

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(.(X4, Xs)) → U5_ag(X4, Xs, member_in_ag(Xs))
U5_ag(X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0, x1, x2)

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

(56) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0, .(z0, z2))) we obtained the following new rules [LPAR04]:

SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2)) → U2_AGG(.(z0, .(z0, z1)), .(z0, z2), member_out_ag(z0, .(z0, z2)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z0, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z0, z3), member_out_ag(z0, .(z0, z3)))

(57) Obligation:

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

SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2, .(z2, z3)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), U5_ag(z0, z2, member_in_ag(z2)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), U5_ag(z2, z3, member_in_ag(z3)))
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0, .(z0, z2))) → U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg(z0, .(z0, z1)))
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2, .(z2, z3))) → U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg(z2, .(z0, z1)))
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(x3, .(z0, z2))) → U3_AGG(x3, .(z0, z1), .(z0, z2), not_member_out_gg(x3, .(z0, z1)))
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(x3, .(z2, z3))) → U3_AGG(x3, .(z0, z1), .(z2, z3), not_member_out_gg(x3, .(z0, z1)))
U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg(z0, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2))
U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg(z2, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z2, .(z0, z1)), .(z2, z3))
U3_AGG(z3, .(z0, z1), .(z0, z2), not_member_out_gg(z3, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z3, .(z0, z1)), .(z0, z2))
U3_AGG(z4, .(z0, z1), .(z2, z3), not_member_out_gg(z4, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z4, .(z0, z1)), .(z2, z3))
SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2)) → U2_AGG(.(z0, .(z0, z1)), .(z0, z2), member_out_ag(z0, .(z0, z2)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z0, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z0, z3), member_out_ag(z0, .(z0, z3)))

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(.(X4, Xs)) → U5_ag(X4, Xs, member_in_ag(Xs))
U5_ag(X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0, x1, x2)

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

(58) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2, .(z2, z3))) we obtained the following new rules [LPAR04]:

SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2)) → U2_AGG(.(z0, .(z0, z1)), .(z0, z2), member_out_ag(z0, .(z0, z2)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z0, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z0, z3), member_out_ag(z0, .(z0, z3)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z1, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z1, z3), member_out_ag(z1, .(z1, z3)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z3, z4)) → U2_AGG(.(z0, .(z1, z2)), .(z3, z4), member_out_ag(z3, .(z3, z4)))

(59) Obligation:

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

SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), U5_ag(z0, z2, member_in_ag(z2)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), U5_ag(z2, z3, member_in_ag(z3)))
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0, .(z0, z2))) → U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg(z0, .(z0, z1)))
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2, .(z2, z3))) → U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg(z2, .(z0, z1)))
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(x3, .(z0, z2))) → U3_AGG(x3, .(z0, z1), .(z0, z2), not_member_out_gg(x3, .(z0, z1)))
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(x3, .(z2, z3))) → U3_AGG(x3, .(z0, z1), .(z2, z3), not_member_out_gg(x3, .(z0, z1)))
U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg(z0, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2))
U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg(z2, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z2, .(z0, z1)), .(z2, z3))
U3_AGG(z3, .(z0, z1), .(z0, z2), not_member_out_gg(z3, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z3, .(z0, z1)), .(z0, z2))
U3_AGG(z4, .(z0, z1), .(z2, z3), not_member_out_gg(z4, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z4, .(z0, z1)), .(z2, z3))
SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2)) → U2_AGG(.(z0, .(z0, z1)), .(z0, z2), member_out_ag(z0, .(z0, z2)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z0, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z0, z3), member_out_ag(z0, .(z0, z3)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z1, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z1, z3), member_out_ag(z1, .(z1, z3)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z3, z4)) → U2_AGG(.(z0, .(z1, z2)), .(z3, z4), member_out_ag(z3, .(z3, z4)))

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(.(X4, Xs)) → U5_ag(X4, Xs, member_in_ag(Xs))
U5_ag(X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0, x1, x2)

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

(60) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), U5_ag(z0, z2, member_in_ag(z2))) we obtained the following new rules [LPAR04]:

SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2)) → U2_AGG(.(z0, .(z0, z1)), .(z0, z2), U5_ag(z0, z2, member_in_ag(z2)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z0, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z0, z3), U5_ag(z0, z3, member_in_ag(z3)))

(61) Obligation:

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

SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), U5_ag(z2, z3, member_in_ag(z3)))
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0, .(z0, z2))) → U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg(z0, .(z0, z1)))
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2, .(z2, z3))) → U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg(z2, .(z0, z1)))
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(x3, .(z0, z2))) → U3_AGG(x3, .(z0, z1), .(z0, z2), not_member_out_gg(x3, .(z0, z1)))
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(x3, .(z2, z3))) → U3_AGG(x3, .(z0, z1), .(z2, z3), not_member_out_gg(x3, .(z0, z1)))
U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg(z0, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2))
U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg(z2, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z2, .(z0, z1)), .(z2, z3))
U3_AGG(z3, .(z0, z1), .(z0, z2), not_member_out_gg(z3, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z3, .(z0, z1)), .(z0, z2))
U3_AGG(z4, .(z0, z1), .(z2, z3), not_member_out_gg(z4, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z4, .(z0, z1)), .(z2, z3))
SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2)) → U2_AGG(.(z0, .(z0, z1)), .(z0, z2), member_out_ag(z0, .(z0, z2)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z0, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z0, z3), member_out_ag(z0, .(z0, z3)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z1, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z1, z3), member_out_ag(z1, .(z1, z3)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z3, z4)) → U2_AGG(.(z0, .(z1, z2)), .(z3, z4), member_out_ag(z3, .(z3, z4)))
SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2)) → U2_AGG(.(z0, .(z0, z1)), .(z0, z2), U5_ag(z0, z2, member_in_ag(z2)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z0, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z0, z3), U5_ag(z0, z3, member_in_ag(z3)))

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(.(X4, Xs)) → U5_ag(X4, Xs, member_in_ag(Xs))
U5_ag(X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0, x1, x2)

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

(62) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), U5_ag(z2, z3, member_in_ag(z3))) we obtained the following new rules [LPAR04]:

SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2)) → U2_AGG(.(z0, .(z0, z1)), .(z0, z2), U5_ag(z0, z2, member_in_ag(z2)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z0, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z0, z3), U5_ag(z0, z3, member_in_ag(z3)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z1, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z1, z3), U5_ag(z1, z3, member_in_ag(z3)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z3, z4)) → U2_AGG(.(z0, .(z1, z2)), .(z3, z4), U5_ag(z3, z4, member_in_ag(z4)))

(63) Obligation:

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

U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0, .(z0, z2))) → U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg(z0, .(z0, z1)))
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2, .(z2, z3))) → U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg(z2, .(z0, z1)))
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(x3, .(z0, z2))) → U3_AGG(x3, .(z0, z1), .(z0, z2), not_member_out_gg(x3, .(z0, z1)))
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(x3, .(z2, z3))) → U3_AGG(x3, .(z0, z1), .(z2, z3), not_member_out_gg(x3, .(z0, z1)))
U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg(z0, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2))
U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg(z2, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z2, .(z0, z1)), .(z2, z3))
U3_AGG(z3, .(z0, z1), .(z0, z2), not_member_out_gg(z3, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z3, .(z0, z1)), .(z0, z2))
U3_AGG(z4, .(z0, z1), .(z2, z3), not_member_out_gg(z4, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z4, .(z0, z1)), .(z2, z3))
SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2)) → U2_AGG(.(z0, .(z0, z1)), .(z0, z2), member_out_ag(z0, .(z0, z2)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z0, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z0, z3), member_out_ag(z0, .(z0, z3)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z1, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z1, z3), member_out_ag(z1, .(z1, z3)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z3, z4)) → U2_AGG(.(z0, .(z1, z2)), .(z3, z4), member_out_ag(z3, .(z3, z4)))
SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2)) → U2_AGG(.(z0, .(z0, z1)), .(z0, z2), U5_ag(z0, z2, member_in_ag(z2)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z0, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z0, z3), U5_ag(z0, z3, member_in_ag(z3)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z1, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z1, z3), U5_ag(z1, z3, member_in_ag(z3)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z3, z4)) → U2_AGG(.(z0, .(z1, z2)), .(z3, z4), U5_ag(z3, z4, member_in_ag(z4)))

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(.(X4, Xs)) → U5_ag(X4, Xs, member_in_ag(Xs))
U5_ag(X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0, x1, x2)

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

(64) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg(z0, .(z0, z1))) evaluates to t =U3_AGG(z0, .(z0, .(z0, z1)), .(z0, z2), not_member_out_gg(z0, .(z0, .(z0, z1))))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Semiunifier: [ ]
• Matcher: [z1 / .(z0, z1)]

---

Rewriting sequence

U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg(z0, .(z0, z1))) → SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2))
with rule U3_AGG(z0', .(z0', z1'), .(z0', z2'), not_member_out_gg(z0', .(z0', z1'))) → SUBSETCHECKED_IN_AGG(.(z0', .(z0', z1')), .(z0', z2')) at position [] and matcher [z0' / z0, z1' / z1, z2' / z2]

SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2)) → U2_AGG(.(z0, .(z0, z1)), .(z0, z2), member_out_ag(z0, .(z0, z2)))
with rule SUBSETCHECKED_IN_AGG(.(z0', .(z0', z1')), .(z0', z2')) → U2_AGG(.(z0', .(z0', z1')), .(z0', z2'), member_out_ag(z0', .(z0', z2'))) at position [] and matcher [z0' / z0, z1' / z1, z2' / z2]

U2_AGG(.(z0, .(z0, z1)), .(z0, z2), member_out_ag(z0, .(z0, z2))) → U3_AGG(z0, .(z0, .(z0, z1)), .(z0, z2), not_member_out_gg(z0, .(z0, .(z0, z1))))
with rule U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0, .(z0, z2))) → U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg(z0, .(z0, z1)))

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.

(65) FALSE

(66) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
subset_in: (f,b)
subsetchecked_in: (f,b,b)
member_in: (f,b) (b,b)
not_member_in: (b,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

subset_in_ag(X, Y) → U1_ag(X, Y, subsetchecked_in_agg(X, [], Y))
subsetchecked_in_agg([], X1, X2) → subsetchecked_out_agg([], X1, X2)
subsetchecked_in_agg(.(X, Xs), Ys, Zs) → U2_agg(X, Xs, Ys, Zs, member_in_ag(X, Zs))
member_in_ag(X, .(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(X, .(X4, Xs)) → U5_ag(X, X4, Xs, member_in_ag(X, Xs))
U5_ag(X, X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))
U2_agg(X, Xs, Ys, Zs, member_out_ag(X, Zs)) → U3_agg(X, Xs, Ys, Zs, not_member_in_gg(X, Ys))
not_member_in_gg(X, Y) → U6_gg(X, Y, member_in_gg(X, Y))
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, Xs)) → U5_gg(X, X4, Xs, member_in_gg(X, Xs))
U5_gg(X, X4, Xs, member_out_gg(X, Xs)) → member_out_gg(X, .(X4, Xs))
U6_gg(X, Y, member_out_gg(X, Y)) → U7_gg(X, Y, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U7_gg(X, Y, failure_out_g(a)) → not_member_out_gg(X, Y)
not_member_in_gg(X5, X6) → not_member_out_gg(X5, X6)
U3_agg(X, Xs, Ys, Zs, not_member_out_gg(X, Ys)) → U4_agg(X, Xs, Ys, Zs, subsetchecked_in_agg(Xs, .(X, Ys), Zs))
U4_agg(X, Xs, Ys, Zs, subsetchecked_out_agg(Xs, .(X, Ys), Zs)) → subsetchecked_out_agg(.(X, Xs), Ys, Zs)
U1_ag(X, Y, subsetchecked_out_agg(X, [], Y)) → subset_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
subset_in_ag(x1, x2)  =  subset_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x3)
subsetchecked_in_agg(x1, x2, x3)  =  subsetchecked_in_agg(x2, x3)
subsetchecked_out_agg(x1, x2, x3)  =  subsetchecked_out_agg(x1)
U2_agg(x1, x2, x3, x4, x5)  =  U2_agg(x3, x4, x5)
member_in_ag(x1, x2)  =  member_in_ag(x2)
.(x1, x2)  =  .(x1, x2)
member_out_ag(x1, x2)  =  member_out_ag(x1)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x4)
U3_agg(x1, x2, x3, x4, x5)  =  U3_agg(x1, x3, x4, x5)
not_member_in_gg(x1, x2)  =  not_member_in_gg(x1, x2)
U6_gg(x1, x2, x3)  =  U6_gg(x3)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
member_out_gg(x1, x2)  =  member_out_gg
U5_gg(x1, x2, x3, x4)  =  U5_gg(x4)
U7_gg(x1, x2, x3)  =  U7_gg(x3)
failure_in_g(x1)  =  failure_in_g(x1)
b  =  b
failure_out_g(x1)  =  failure_out_g
a  =  a
not_member_out_gg(x1, x2)  =  not_member_out_gg
U4_agg(x1, x2, x3, x4, x5)  =  U4_agg(x1, x5)
[]  =  []
subset_out_ag(x1, x2)  =  subset_out_ag(x1)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(67) Obligation:

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

subset_in_ag(X, Y) → U1_ag(X, Y, subsetchecked_in_agg(X, [], Y))
subsetchecked_in_agg([], X1, X2) → subsetchecked_out_agg([], X1, X2)
subsetchecked_in_agg(.(X, Xs), Ys, Zs) → U2_agg(X, Xs, Ys, Zs, member_in_ag(X, Zs))
member_in_ag(X, .(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(X, .(X4, Xs)) → U5_ag(X, X4, Xs, member_in_ag(X, Xs))
U5_ag(X, X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))
U2_agg(X, Xs, Ys, Zs, member_out_ag(X, Zs)) → U3_agg(X, Xs, Ys, Zs, not_member_in_gg(X, Ys))
not_member_in_gg(X, Y) → U6_gg(X, Y, member_in_gg(X, Y))
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, Xs)) → U5_gg(X, X4, Xs, member_in_gg(X, Xs))
U5_gg(X, X4, Xs, member_out_gg(X, Xs)) → member_out_gg(X, .(X4, Xs))
U6_gg(X, Y, member_out_gg(X, Y)) → U7_gg(X, Y, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U7_gg(X, Y, failure_out_g(a)) → not_member_out_gg(X, Y)
not_member_in_gg(X5, X6) → not_member_out_gg(X5, X6)
U3_agg(X, Xs, Ys, Zs, not_member_out_gg(X, Ys)) → U4_agg(X, Xs, Ys, Zs, subsetchecked_in_agg(Xs, .(X, Ys), Zs))
U4_agg(X, Xs, Ys, Zs, subsetchecked_out_agg(Xs, .(X, Ys), Zs)) → subsetchecked_out_agg(.(X, Xs), Ys, Zs)
U1_ag(X, Y, subsetchecked_out_agg(X, [], Y)) → subset_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
subset_in_ag(x1, x2)  =  subset_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x3)
subsetchecked_in_agg(x1, x2, x3)  =  subsetchecked_in_agg(x2, x3)
subsetchecked_out_agg(x1, x2, x3)  =  subsetchecked_out_agg(x1)
U2_agg(x1, x2, x3, x4, x5)  =  U2_agg(x3, x4, x5)
member_in_ag(x1, x2)  =  member_in_ag(x2)
.(x1, x2)  =  .(x1, x2)
member_out_ag(x1, x2)  =  member_out_ag(x1)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x4)
U3_agg(x1, x2, x3, x4, x5)  =  U3_agg(x1, x3, x4, x5)
not_member_in_gg(x1, x2)  =  not_member_in_gg(x1, x2)
U6_gg(x1, x2, x3)  =  U6_gg(x3)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
member_out_gg(x1, x2)  =  member_out_gg
U5_gg(x1, x2, x3, x4)  =  U5_gg(x4)
U7_gg(x1, x2, x3)  =  U7_gg(x3)
failure_in_g(x1)  =  failure_in_g(x1)
b  =  b
failure_out_g(x1)  =  failure_out_g
a  =  a
not_member_out_gg(x1, x2)  =  not_member_out_gg
U4_agg(x1, x2, x3, x4, x5)  =  U4_agg(x1, x5)
[]  =  []
subset_out_ag(x1, x2)  =  subset_out_ag(x1)

(68) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

SUBSET_IN_AG(X, Y) → U1_AG(X, Y, subsetchecked_in_agg(X, [], Y))
SUBSET_IN_AG(X, Y) → SUBSETCHECKED_IN_AGG(X, [], Y)
SUBSETCHECKED_IN_AGG(.(X, Xs), Ys, Zs) → U2_AGG(X, Xs, Ys, Zs, member_in_ag(X, Zs))
SUBSETCHECKED_IN_AGG(.(X, Xs), Ys, Zs) → MEMBER_IN_AG(X, Zs)
MEMBER_IN_AG(X, .(X4, Xs)) → U5_AG(X, X4, Xs, member_in_ag(X, Xs))
MEMBER_IN_AG(X, .(X4, Xs)) → MEMBER_IN_AG(X, Xs)
U2_AGG(X, Xs, Ys, Zs, member_out_ag(X, Zs)) → U3_AGG(X, Xs, Ys, Zs, not_member_in_gg(X, Ys))
U2_AGG(X, Xs, Ys, Zs, member_out_ag(X, Zs)) → NOT_MEMBER_IN_GG(X, Ys)
NOT_MEMBER_IN_GG(X, Y) → U6_GG(X, Y, member_in_gg(X, Y))
NOT_MEMBER_IN_GG(X, Y) → MEMBER_IN_GG(X, Y)
MEMBER_IN_GG(X, .(X4, Xs)) → U5_GG(X, X4, Xs, member_in_gg(X, Xs))
MEMBER_IN_GG(X, .(X4, Xs)) → MEMBER_IN_GG(X, Xs)
U6_GG(X, Y, member_out_gg(X, Y)) → U7_GG(X, Y, failure_in_g(a))
U6_GG(X, Y, member_out_gg(X, Y)) → FAILURE_IN_G(a)
U3_AGG(X, Xs, Ys, Zs, not_member_out_gg(X, Ys)) → U4_AGG(X, Xs, Ys, Zs, subsetchecked_in_agg(Xs, .(X, Ys), Zs))
U3_AGG(X, Xs, Ys, Zs, not_member_out_gg(X, Ys)) → SUBSETCHECKED_IN_AGG(Xs, .(X, Ys), Zs)

The TRS R consists of the following rules:

subset_in_ag(X, Y) → U1_ag(X, Y, subsetchecked_in_agg(X, [], Y))
subsetchecked_in_agg([], X1, X2) → subsetchecked_out_agg([], X1, X2)
subsetchecked_in_agg(.(X, Xs), Ys, Zs) → U2_agg(X, Xs, Ys, Zs, member_in_ag(X, Zs))
member_in_ag(X, .(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(X, .(X4, Xs)) → U5_ag(X, X4, Xs, member_in_ag(X, Xs))
U5_ag(X, X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))
U2_agg(X, Xs, Ys, Zs, member_out_ag(X, Zs)) → U3_agg(X, Xs, Ys, Zs, not_member_in_gg(X, Ys))
not_member_in_gg(X, Y) → U6_gg(X, Y, member_in_gg(X, Y))
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, Xs)) → U5_gg(X, X4, Xs, member_in_gg(X, Xs))
U5_gg(X, X4, Xs, member_out_gg(X, Xs)) → member_out_gg(X, .(X4, Xs))
U6_gg(X, Y, member_out_gg(X, Y)) → U7_gg(X, Y, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U7_gg(X, Y, failure_out_g(a)) → not_member_out_gg(X, Y)
not_member_in_gg(X5, X6) → not_member_out_gg(X5, X6)
U3_agg(X, Xs, Ys, Zs, not_member_out_gg(X, Ys)) → U4_agg(X, Xs, Ys, Zs, subsetchecked_in_agg(Xs, .(X, Ys), Zs))
U4_agg(X, Xs, Ys, Zs, subsetchecked_out_agg(Xs, .(X, Ys), Zs)) → subsetchecked_out_agg(.(X, Xs), Ys, Zs)
U1_ag(X, Y, subsetchecked_out_agg(X, [], Y)) → subset_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
subset_in_ag(x1, x2)  =  subset_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x3)
subsetchecked_in_agg(x1, x2, x3)  =  subsetchecked_in_agg(x2, x3)
subsetchecked_out_agg(x1, x2, x3)  =  subsetchecked_out_agg(x1)
U2_agg(x1, x2, x3, x4, x5)  =  U2_agg(x3, x4, x5)
member_in_ag(x1, x2)  =  member_in_ag(x2)
.(x1, x2)  =  .(x1, x2)
member_out_ag(x1, x2)  =  member_out_ag(x1)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x4)
U3_agg(x1, x2, x3, x4, x5)  =  U3_agg(x1, x3, x4, x5)
not_member_in_gg(x1, x2)  =  not_member_in_gg(x1, x2)
U6_gg(x1, x2, x3)  =  U6_gg(x3)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
member_out_gg(x1, x2)  =  member_out_gg
U5_gg(x1, x2, x3, x4)  =  U5_gg(x4)
U7_gg(x1, x2, x3)  =  U7_gg(x3)
failure_in_g(x1)  =  failure_in_g(x1)
b  =  b
failure_out_g(x1)  =  failure_out_g
a  =  a
not_member_out_gg(x1, x2)  =  not_member_out_gg
U4_agg(x1, x2, x3, x4, x5)  =  U4_agg(x1, x5)
[]  =  []
subset_out_ag(x1, x2)  =  subset_out_ag(x1)
SUBSET_IN_AG(x1, x2)  =  SUBSET_IN_AG(x2)
U1_AG(x1, x2, x3)  =  U1_AG(x3)
SUBSETCHECKED_IN_AGG(x1, x2, x3)  =  SUBSETCHECKED_IN_AGG(x2, x3)
U2_AGG(x1, x2, x3, x4, x5)  =  U2_AGG(x3, x4, x5)
MEMBER_IN_AG(x1, x2)  =  MEMBER_IN_AG(x2)
U5_AG(x1, x2, x3, x4)  =  U5_AG(x4)
U3_AGG(x1, x2, x3, x4, x5)  =  U3_AGG(x1, x3, x4, x5)
NOT_MEMBER_IN_GG(x1, x2)  =  NOT_MEMBER_IN_GG(x1, x2)
U6_GG(x1, x2, x3)  =  U6_GG(x3)
MEMBER_IN_GG(x1, x2)  =  MEMBER_IN_GG(x1, x2)
U5_GG(x1, x2, x3, x4)  =  U5_GG(x4)
U7_GG(x1, x2, x3)  =  U7_GG(x3)
FAILURE_IN_G(x1)  =  FAILURE_IN_G(x1)
U4_AGG(x1, x2, x3, x4, x5)  =  U4_AGG(x1, x5)

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

(69) Obligation:

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

SUBSET_IN_AG(X, Y) → U1_AG(X, Y, subsetchecked_in_agg(X, [], Y))
SUBSET_IN_AG(X, Y) → SUBSETCHECKED_IN_AGG(X, [], Y)
SUBSETCHECKED_IN_AGG(.(X, Xs), Ys, Zs) → U2_AGG(X, Xs, Ys, Zs, member_in_ag(X, Zs))
SUBSETCHECKED_IN_AGG(.(X, Xs), Ys, Zs) → MEMBER_IN_AG(X, Zs)
MEMBER_IN_AG(X, .(X4, Xs)) → U5_AG(X, X4, Xs, member_in_ag(X, Xs))
MEMBER_IN_AG(X, .(X4, Xs)) → MEMBER_IN_AG(X, Xs)
U2_AGG(X, Xs, Ys, Zs, member_out_ag(X, Zs)) → U3_AGG(X, Xs, Ys, Zs, not_member_in_gg(X, Ys))
U2_AGG(X, Xs, Ys, Zs, member_out_ag(X, Zs)) → NOT_MEMBER_IN_GG(X, Ys)
NOT_MEMBER_IN_GG(X, Y) → U6_GG(X, Y, member_in_gg(X, Y))
NOT_MEMBER_IN_GG(X, Y) → MEMBER_IN_GG(X, Y)
MEMBER_IN_GG(X, .(X4, Xs)) → U5_GG(X, X4, Xs, member_in_gg(X, Xs))
MEMBER_IN_GG(X, .(X4, Xs)) → MEMBER_IN_GG(X, Xs)
U6_GG(X, Y, member_out_gg(X, Y)) → U7_GG(X, Y, failure_in_g(a))
U6_GG(X, Y, member_out_gg(X, Y)) → FAILURE_IN_G(a)
U3_AGG(X, Xs, Ys, Zs, not_member_out_gg(X, Ys)) → U4_AGG(X, Xs, Ys, Zs, subsetchecked_in_agg(Xs, .(X, Ys), Zs))
U3_AGG(X, Xs, Ys, Zs, not_member_out_gg(X, Ys)) → SUBSETCHECKED_IN_AGG(Xs, .(X, Ys), Zs)

The TRS R consists of the following rules:

subset_in_ag(X, Y) → U1_ag(X, Y, subsetchecked_in_agg(X, [], Y))
subsetchecked_in_agg([], X1, X2) → subsetchecked_out_agg([], X1, X2)
subsetchecked_in_agg(.(X, Xs), Ys, Zs) → U2_agg(X, Xs, Ys, Zs, member_in_ag(X, Zs))
member_in_ag(X, .(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(X, .(X4, Xs)) → U5_ag(X, X4, Xs, member_in_ag(X, Xs))
U5_ag(X, X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))
U2_agg(X, Xs, Ys, Zs, member_out_ag(X, Zs)) → U3_agg(X, Xs, Ys, Zs, not_member_in_gg(X, Ys))
not_member_in_gg(X, Y) → U6_gg(X, Y, member_in_gg(X, Y))
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, Xs)) → U5_gg(X, X4, Xs, member_in_gg(X, Xs))
U5_gg(X, X4, Xs, member_out_gg(X, Xs)) → member_out_gg(X, .(X4, Xs))
U6_gg(X, Y, member_out_gg(X, Y)) → U7_gg(X, Y, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U7_gg(X, Y, failure_out_g(a)) → not_member_out_gg(X, Y)
not_member_in_gg(X5, X6) → not_member_out_gg(X5, X6)
U3_agg(X, Xs, Ys, Zs, not_member_out_gg(X, Ys)) → U4_agg(X, Xs, Ys, Zs, subsetchecked_in_agg(Xs, .(X, Ys), Zs))
U4_agg(X, Xs, Ys, Zs, subsetchecked_out_agg(Xs, .(X, Ys), Zs)) → subsetchecked_out_agg(.(X, Xs), Ys, Zs)
U1_ag(X, Y, subsetchecked_out_agg(X, [], Y)) → subset_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
subset_in_ag(x1, x2)  =  subset_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x3)
subsetchecked_in_agg(x1, x2, x3)  =  subsetchecked_in_agg(x2, x3)
subsetchecked_out_agg(x1, x2, x3)  =  subsetchecked_out_agg(x1)
U2_agg(x1, x2, x3, x4, x5)  =  U2_agg(x3, x4, x5)
member_in_ag(x1, x2)  =  member_in_ag(x2)
.(x1, x2)  =  .(x1, x2)
member_out_ag(x1, x2)  =  member_out_ag(x1)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x4)
U3_agg(x1, x2, x3, x4, x5)  =  U3_agg(x1, x3, x4, x5)
not_member_in_gg(x1, x2)  =  not_member_in_gg(x1, x2)
U6_gg(x1, x2, x3)  =  U6_gg(x3)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
member_out_gg(x1, x2)  =  member_out_gg
U5_gg(x1, x2, x3, x4)  =  U5_gg(x4)
U7_gg(x1, x2, x3)  =  U7_gg(x3)
failure_in_g(x1)  =  failure_in_g(x1)
b  =  b
failure_out_g(x1)  =  failure_out_g
a  =  a
not_member_out_gg(x1, x2)  =  not_member_out_gg
U4_agg(x1, x2, x3, x4, x5)  =  U4_agg(x1, x5)
[]  =  []
subset_out_ag(x1, x2)  =  subset_out_ag(x1)
SUBSET_IN_AG(x1, x2)  =  SUBSET_IN_AG(x2)
U1_AG(x1, x2, x3)  =  U1_AG(x3)
SUBSETCHECKED_IN_AGG(x1, x2, x3)  =  SUBSETCHECKED_IN_AGG(x2, x3)
U2_AGG(x1, x2, x3, x4, x5)  =  U2_AGG(x3, x4, x5)
MEMBER_IN_AG(x1, x2)  =  MEMBER_IN_AG(x2)
U5_AG(x1, x2, x3, x4)  =  U5_AG(x4)
U3_AGG(x1, x2, x3, x4, x5)  =  U3_AGG(x1, x3, x4, x5)
NOT_MEMBER_IN_GG(x1, x2)  =  NOT_MEMBER_IN_GG(x1, x2)
U6_GG(x1, x2, x3)  =  U6_GG(x3)
MEMBER_IN_GG(x1, x2)  =  MEMBER_IN_GG(x1, x2)
U5_GG(x1, x2, x3, x4)  =  U5_GG(x4)
U7_GG(x1, x2, x3)  =  U7_GG(x3)
FAILURE_IN_G(x1)  =  FAILURE_IN_G(x1)
U4_AGG(x1, x2, x3, x4, x5)  =  U4_AGG(x1, x5)

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

(70) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 11 less nodes.

(71) Complex Obligation (AND)

(72) Obligation:

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

MEMBER_IN_GG(X, .(X4, Xs)) → MEMBER_IN_GG(X, Xs)

The TRS R consists of the following rules:

subset_in_ag(X, Y) → U1_ag(X, Y, subsetchecked_in_agg(X, [], Y))
subsetchecked_in_agg([], X1, X2) → subsetchecked_out_agg([], X1, X2)
subsetchecked_in_agg(.(X, Xs), Ys, Zs) → U2_agg(X, Xs, Ys, Zs, member_in_ag(X, Zs))
member_in_ag(X, .(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(X, .(X4, Xs)) → U5_ag(X, X4, Xs, member_in_ag(X, Xs))
U5_ag(X, X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))
U2_agg(X, Xs, Ys, Zs, member_out_ag(X, Zs)) → U3_agg(X, Xs, Ys, Zs, not_member_in_gg(X, Ys))
not_member_in_gg(X, Y) → U6_gg(X, Y, member_in_gg(X, Y))
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, Xs)) → U5_gg(X, X4, Xs, member_in_gg(X, Xs))
U5_gg(X, X4, Xs, member_out_gg(X, Xs)) → member_out_gg(X, .(X4, Xs))
U6_gg(X, Y, member_out_gg(X, Y)) → U7_gg(X, Y, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U7_gg(X, Y, failure_out_g(a)) → not_member_out_gg(X, Y)
not_member_in_gg(X5, X6) → not_member_out_gg(X5, X6)
U3_agg(X, Xs, Ys, Zs, not_member_out_gg(X, Ys)) → U4_agg(X, Xs, Ys, Zs, subsetchecked_in_agg(Xs, .(X, Ys), Zs))
U4_agg(X, Xs, Ys, Zs, subsetchecked_out_agg(Xs, .(X, Ys), Zs)) → subsetchecked_out_agg(.(X, Xs), Ys, Zs)
U1_ag(X, Y, subsetchecked_out_agg(X, [], Y)) → subset_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
subset_in_ag(x1, x2)  =  subset_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x3)
subsetchecked_in_agg(x1, x2, x3)  =  subsetchecked_in_agg(x2, x3)
subsetchecked_out_agg(x1, x2, x3)  =  subsetchecked_out_agg(x1)
U2_agg(x1, x2, x3, x4, x5)  =  U2_agg(x3, x4, x5)
member_in_ag(x1, x2)  =  member_in_ag(x2)
.(x1, x2)  =  .(x1, x2)
member_out_ag(x1, x2)  =  member_out_ag(x1)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x4)
U3_agg(x1, x2, x3, x4, x5)  =  U3_agg(x1, x3, x4, x5)
not_member_in_gg(x1, x2)  =  not_member_in_gg(x1, x2)
U6_gg(x1, x2, x3)  =  U6_gg(x3)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
member_out_gg(x1, x2)  =  member_out_gg
U5_gg(x1, x2, x3, x4)  =  U5_gg(x4)
U7_gg(x1, x2, x3)  =  U7_gg(x3)
failure_in_g(x1)  =  failure_in_g(x1)
b  =  b
failure_out_g(x1)  =  failure_out_g
a  =  a
not_member_out_gg(x1, x2)  =  not_member_out_gg
U4_agg(x1, x2, x3, x4, x5)  =  U4_agg(x1, x5)
[]  =  []
subset_out_ag(x1, x2)  =  subset_out_ag(x1)
MEMBER_IN_GG(x1, x2)  =  MEMBER_IN_GG(x1, x2)

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

(73) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(74) Obligation:

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

MEMBER_IN_GG(X, .(X4, Xs)) → MEMBER_IN_GG(X, Xs)

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

(75) PiDPToQDPProof (EQUIVALENT transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(76) Obligation:

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

MEMBER_IN_GG(X, .(X4, Xs)) → MEMBER_IN_GG(X, Xs)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(77) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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_IN_GG(X, .(X4, Xs)) → MEMBER_IN_GG(X, Xs)
  The graph contains the following edges 1 >= 1, 2 > 2

(78) TRUE

(79) Obligation:

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

MEMBER_IN_AG(X, .(X4, Xs)) → MEMBER_IN_AG(X, Xs)

The TRS R consists of the following rules:

subset_in_ag(X, Y) → U1_ag(X, Y, subsetchecked_in_agg(X, [], Y))
subsetchecked_in_agg([], X1, X2) → subsetchecked_out_agg([], X1, X2)
subsetchecked_in_agg(.(X, Xs), Ys, Zs) → U2_agg(X, Xs, Ys, Zs, member_in_ag(X, Zs))
member_in_ag(X, .(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(X, .(X4, Xs)) → U5_ag(X, X4, Xs, member_in_ag(X, Xs))
U5_ag(X, X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))
U2_agg(X, Xs, Ys, Zs, member_out_ag(X, Zs)) → U3_agg(X, Xs, Ys, Zs, not_member_in_gg(X, Ys))
not_member_in_gg(X, Y) → U6_gg(X, Y, member_in_gg(X, Y))
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, Xs)) → U5_gg(X, X4, Xs, member_in_gg(X, Xs))
U5_gg(X, X4, Xs, member_out_gg(X, Xs)) → member_out_gg(X, .(X4, Xs))
U6_gg(X, Y, member_out_gg(X, Y)) → U7_gg(X, Y, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U7_gg(X, Y, failure_out_g(a)) → not_member_out_gg(X, Y)
not_member_in_gg(X5, X6) → not_member_out_gg(X5, X6)
U3_agg(X, Xs, Ys, Zs, not_member_out_gg(X, Ys)) → U4_agg(X, Xs, Ys, Zs, subsetchecked_in_agg(Xs, .(X, Ys), Zs))
U4_agg(X, Xs, Ys, Zs, subsetchecked_out_agg(Xs, .(X, Ys), Zs)) → subsetchecked_out_agg(.(X, Xs), Ys, Zs)
U1_ag(X, Y, subsetchecked_out_agg(X, [], Y)) → subset_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
subset_in_ag(x1, x2)  =  subset_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x3)
subsetchecked_in_agg(x1, x2, x3)  =  subsetchecked_in_agg(x2, x3)
subsetchecked_out_agg(x1, x2, x3)  =  subsetchecked_out_agg(x1)
U2_agg(x1, x2, x3, x4, x5)  =  U2_agg(x3, x4, x5)
member_in_ag(x1, x2)  =  member_in_ag(x2)
.(x1, x2)  =  .(x1, x2)
member_out_ag(x1, x2)  =  member_out_ag(x1)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x4)
U3_agg(x1, x2, x3, x4, x5)  =  U3_agg(x1, x3, x4, x5)
not_member_in_gg(x1, x2)  =  not_member_in_gg(x1, x2)
U6_gg(x1, x2, x3)  =  U6_gg(x3)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
member_out_gg(x1, x2)  =  member_out_gg
U5_gg(x1, x2, x3, x4)  =  U5_gg(x4)
U7_gg(x1, x2, x3)  =  U7_gg(x3)
failure_in_g(x1)  =  failure_in_g(x1)
b  =  b
failure_out_g(x1)  =  failure_out_g
a  =  a
not_member_out_gg(x1, x2)  =  not_member_out_gg
U4_agg(x1, x2, x3, x4, x5)  =  U4_agg(x1, x5)
[]  =  []
subset_out_ag(x1, x2)  =  subset_out_ag(x1)
MEMBER_IN_AG(x1, x2)  =  MEMBER_IN_AG(x2)

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

(80) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(81) Obligation:

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

MEMBER_IN_AG(X, .(X4, Xs)) → MEMBER_IN_AG(X, Xs)

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

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

(82) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(83) Obligation:

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

MEMBER_IN_AG(.(X4, Xs)) → MEMBER_IN_AG(Xs)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(84) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] 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_IN_AG(.(X4, Xs)) → MEMBER_IN_AG(Xs)
  The graph contains the following edges 1 > 1

(85) TRUE

(86) Obligation:

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

U2_AGG(X, Xs, Ys, Zs, member_out_ag(X, Zs)) → U3_AGG(X, Xs, Ys, Zs, not_member_in_gg(X, Ys))
U3_AGG(X, Xs, Ys, Zs, not_member_out_gg(X, Ys)) → SUBSETCHECKED_IN_AGG(Xs, .(X, Ys), Zs)
SUBSETCHECKED_IN_AGG(.(X, Xs), Ys, Zs) → U2_AGG(X, Xs, Ys, Zs, member_in_ag(X, Zs))

The TRS R consists of the following rules:

subset_in_ag(X, Y) → U1_ag(X, Y, subsetchecked_in_agg(X, [], Y))
subsetchecked_in_agg([], X1, X2) → subsetchecked_out_agg([], X1, X2)
subsetchecked_in_agg(.(X, Xs), Ys, Zs) → U2_agg(X, Xs, Ys, Zs, member_in_ag(X, Zs))
member_in_ag(X, .(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(X, .(X4, Xs)) → U5_ag(X, X4, Xs, member_in_ag(X, Xs))
U5_ag(X, X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))
U2_agg(X, Xs, Ys, Zs, member_out_ag(X, Zs)) → U3_agg(X, Xs, Ys, Zs, not_member_in_gg(X, Ys))
not_member_in_gg(X, Y) → U6_gg(X, Y, member_in_gg(X, Y))
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, Xs)) → U5_gg(X, X4, Xs, member_in_gg(X, Xs))
U5_gg(X, X4, Xs, member_out_gg(X, Xs)) → member_out_gg(X, .(X4, Xs))
U6_gg(X, Y, member_out_gg(X, Y)) → U7_gg(X, Y, failure_in_g(a))
failure_in_g(b) → failure_out_g(b)
U7_gg(X, Y, failure_out_g(a)) → not_member_out_gg(X, Y)
not_member_in_gg(X5, X6) → not_member_out_gg(X5, X6)
U3_agg(X, Xs, Ys, Zs, not_member_out_gg(X, Ys)) → U4_agg(X, Xs, Ys, Zs, subsetchecked_in_agg(Xs, .(X, Ys), Zs))
U4_agg(X, Xs, Ys, Zs, subsetchecked_out_agg(Xs, .(X, Ys), Zs)) → subsetchecked_out_agg(.(X, Xs), Ys, Zs)
U1_ag(X, Y, subsetchecked_out_agg(X, [], Y)) → subset_out_ag(X, Y)

The argument filtering Pi contains the following mapping:
subset_in_ag(x1, x2)  =  subset_in_ag(x2)
U1_ag(x1, x2, x3)  =  U1_ag(x3)
subsetchecked_in_agg(x1, x2, x3)  =  subsetchecked_in_agg(x2, x3)
subsetchecked_out_agg(x1, x2, x3)  =  subsetchecked_out_agg(x1)
U2_agg(x1, x2, x3, x4, x5)  =  U2_agg(x3, x4, x5)
member_in_ag(x1, x2)  =  member_in_ag(x2)
.(x1, x2)  =  .(x1, x2)
member_out_ag(x1, x2)  =  member_out_ag(x1)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x4)
U3_agg(x1, x2, x3, x4, x5)  =  U3_agg(x1, x3, x4, x5)
not_member_in_gg(x1, x2)  =  not_member_in_gg(x1, x2)
U6_gg(x1, x2, x3)  =  U6_gg(x3)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
member_out_gg(x1, x2)  =  member_out_gg
U5_gg(x1, x2, x3, x4)  =  U5_gg(x4)
U7_gg(x1, x2, x3)  =  U7_gg(x3)
failure_in_g(x1)  =  failure_in_g(x1)
b  =  b
failure_out_g(x1)  =  failure_out_g
a  =  a
not_member_out_gg(x1, x2)  =  not_member_out_gg
U4_agg(x1, x2, x3, x4, x5)  =  U4_agg(x1, x5)
[]  =  []
subset_out_ag(x1, x2)  =  subset_out_ag(x1)
SUBSETCHECKED_IN_AGG(x1, x2, x3)  =  SUBSETCHECKED_IN_AGG(x2, x3)
U2_AGG(x1, x2, x3, x4, x5)  =  U2_AGG(x3, x4, x5)
U3_AGG(x1, x2, x3, x4, x5)  =  U3_AGG(x1, x3, x4, x5)

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

(87) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(88) Obligation:

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

U2_AGG(X, Xs, Ys, Zs, member_out_ag(X, Zs)) → U3_AGG(X, Xs, Ys, Zs, not_member_in_gg(X, Ys))
U3_AGG(X, Xs, Ys, Zs, not_member_out_gg(X, Ys)) → SUBSETCHECKED_IN_AGG(Xs, .(X, Ys), Zs)
SUBSETCHECKED_IN_AGG(.(X, Xs), Ys, Zs) → U2_AGG(X, Xs, Ys, Zs, member_in_ag(X, Zs))

The TRS R consists of the following rules:

not_member_in_gg(X, Y) → U6_gg(X, Y, member_in_gg(X, Y))
not_member_in_gg(X5, X6) → not_member_out_gg(X5, X6)
member_in_ag(X, .(X, X3)) → member_out_ag(X, .(X, X3))
member_in_ag(X, .(X4, Xs)) → U5_ag(X, X4, Xs, member_in_ag(X, Xs))
U6_gg(X, Y, member_out_gg(X, Y)) → U7_gg(X, Y, failure_in_g(a))
U5_ag(X, X4, Xs, member_out_ag(X, Xs)) → member_out_ag(X, .(X4, Xs))
member_in_gg(X, .(X, X3)) → member_out_gg(X, .(X, X3))
member_in_gg(X, .(X4, Xs)) → U5_gg(X, X4, Xs, member_in_gg(X, Xs))
U5_gg(X, X4, Xs, member_out_gg(X, Xs)) → member_out_gg(X, .(X4, Xs))

The argument filtering Pi contains the following mapping:
member_in_ag(x1, x2)  =  member_in_ag(x2)
.(x1, x2)  =  .(x1, x2)
member_out_ag(x1, x2)  =  member_out_ag(x1)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x4)
not_member_in_gg(x1, x2)  =  not_member_in_gg(x1, x2)
U6_gg(x1, x2, x3)  =  U6_gg(x3)
member_in_gg(x1, x2)  =  member_in_gg(x1, x2)
member_out_gg(x1, x2)  =  member_out_gg
U5_gg(x1, x2, x3, x4)  =  U5_gg(x4)
U7_gg(x1, x2, x3)  =  U7_gg(x3)
failure_in_g(x1)  =  failure_in_g(x1)
a  =  a
not_member_out_gg(x1, x2)  =  not_member_out_gg
SUBSETCHECKED_IN_AGG(x1, x2, x3)  =  SUBSETCHECKED_IN_AGG(x2, x3)
U2_AGG(x1, x2, x3, x4, x5)  =  U2_AGG(x3, x4, x5)
U3_AGG(x1, x2, x3, x4, x5)  =  U3_AGG(x1, x3, x4, x5)

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

(89) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(90) Obligation:

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

U2_AGG(Ys, Zs, member_out_ag(X)) → U3_AGG(X, Ys, Zs, not_member_in_gg(X, Ys))
U3_AGG(X, Ys, Zs, not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(X, Ys), Zs)
SUBSETCHECKED_IN_AGG(Ys, Zs) → U2_AGG(Ys, Zs, member_in_ag(Zs))

The TRS R consists of the following rules:

not_member_in_gg(X, Y) → U6_gg(member_in_gg(X, Y))
not_member_in_gg(X5, X6) → not_member_out_gg
member_in_ag(.(X, X3)) → member_out_ag(X)
member_in_ag(.(X4, Xs)) → U5_ag(member_in_ag(Xs))
U6_gg(member_out_gg) → U7_gg(failure_in_g(a))
U5_ag(member_out_ag(X)) → member_out_ag(X)
member_in_gg(X, .(X, X3)) → member_out_gg
member_in_gg(X, .(X4, Xs)) → U5_gg(member_in_gg(X, Xs))
U5_gg(member_out_gg) → member_out_gg

The set Q consists of the following terms:

not_member_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0)
U5_ag(x0)
member_in_gg(x0, x1)
U5_gg(x0)

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

(91) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule SUBSETCHECKED_IN_AGG(Ys, Zs) → U2_AGG(Ys, Zs, member_in_ag(Zs)) we obtained the following new rules [LPAR04]:

SUBSETCHECKED_IN_AGG(.(z0, z1), z2) → U2_AGG(.(z0, z1), z2, member_in_ag(z2))

(92) Obligation:

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

U2_AGG(Ys, Zs, member_out_ag(X)) → U3_AGG(X, Ys, Zs, not_member_in_gg(X, Ys))
U3_AGG(X, Ys, Zs, not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(X, Ys), Zs)
SUBSETCHECKED_IN_AGG(.(z0, z1), z2) → U2_AGG(.(z0, z1), z2, member_in_ag(z2))

The TRS R consists of the following rules:

not_member_in_gg(X, Y) → U6_gg(member_in_gg(X, Y))
not_member_in_gg(X5, X6) → not_member_out_gg
member_in_ag(.(X, X3)) → member_out_ag(X)
member_in_ag(.(X4, Xs)) → U5_ag(member_in_ag(Xs))
U6_gg(member_out_gg) → U7_gg(failure_in_g(a))
U5_ag(member_out_ag(X)) → member_out_ag(X)
member_in_gg(X, .(X, X3)) → member_out_gg
member_in_gg(X, .(X4, Xs)) → U5_gg(member_in_gg(X, Xs))
U5_gg(member_out_gg) → member_out_gg

The set Q consists of the following terms:

not_member_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0)
U5_ag(x0)
member_in_gg(x0, x1)
U5_gg(x0)

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

(93) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U2_AGG(Ys, Zs, member_out_ag(X)) → U3_AGG(X, Ys, Zs, not_member_in_gg(X, Ys)) at position [3] we obtained the following new rules [LPAR04]:

U2_AGG(x1, y1, member_out_ag(x0)) → U3_AGG(x0, x1, y1, U6_gg(member_in_gg(x0, x1)))
U2_AGG(x1, y1, member_out_ag(x0)) → U3_AGG(x0, x1, y1, not_member_out_gg)

(94) Obligation:

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

U3_AGG(X, Ys, Zs, not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(X, Ys), Zs)
SUBSETCHECKED_IN_AGG(Ys, Zs) → U2_AGG(Ys, Zs, member_in_ag(Zs))
U2_AGG(x1, y1, member_out_ag(x0)) → U3_AGG(x0, x1, y1, U6_gg(member_in_gg(x0, x1)))
U2_AGG(x1, y1, member_out_ag(x0)) → U3_AGG(x0, x1, y1, not_member_out_gg)

The TRS R consists of the following rules:

not_member_in_gg(X, Y) → U6_gg(member_in_gg(X, Y))
not_member_in_gg(X5, X6) → not_member_out_gg
member_in_ag(.(X, X3)) → member_out_ag(X)
member_in_ag(.(X4, Xs)) → U5_ag(member_in_ag(Xs))
U6_gg(member_out_gg) → U7_gg(failure_in_g(a))
U5_ag(member_out_ag(X)) → member_out_ag(X)
member_in_gg(X, .(X, X3)) → member_out_gg
member_in_gg(X, .(X4, Xs)) → U5_gg(member_in_gg(X, Xs))
U5_gg(member_out_gg) → member_out_gg

The set Q consists of the following terms:

not_member_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0)
U5_ag(x0)
member_in_gg(x0, x1)
U5_gg(x0)

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

(95) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(96) Obligation:

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

SUBSETCHECKED_IN_AGG(Ys, Zs) → U2_AGG(Ys, Zs, member_in_ag(Zs))
U2_AGG(x1, y1, member_out_ag(x0)) → U3_AGG(x0, x1, y1, not_member_out_gg)
U3_AGG(X, Ys, Zs, not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(X, Ys), Zs)

The TRS R consists of the following rules:

not_member_in_gg(X, Y) → U6_gg(member_in_gg(X, Y))
not_member_in_gg(X5, X6) → not_member_out_gg
member_in_ag(.(X, X3)) → member_out_ag(X)
member_in_ag(.(X4, Xs)) → U5_ag(member_in_ag(Xs))
U6_gg(member_out_gg) → U7_gg(failure_in_g(a))
U5_ag(member_out_ag(X)) → member_out_ag(X)
member_in_gg(X, .(X, X3)) → member_out_gg
member_in_gg(X, .(X4, Xs)) → U5_gg(member_in_gg(X, Xs))
U5_gg(member_out_gg) → member_out_gg

The set Q consists of the following terms:

not_member_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0)
U5_ag(x0)
member_in_gg(x0, x1)
U5_gg(x0)

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

(97) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(98) Obligation:

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

SUBSETCHECKED_IN_AGG(Ys, Zs) → U2_AGG(Ys, Zs, member_in_ag(Zs))
U2_AGG(x1, y1, member_out_ag(x0)) → U3_AGG(x0, x1, y1, not_member_out_gg)
U3_AGG(X, Ys, Zs, not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(X, Ys), Zs)

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X)
member_in_ag(.(X4, Xs)) → U5_ag(member_in_ag(Xs))
U5_ag(member_out_ag(X)) → member_out_ag(X)

The set Q consists of the following terms:

not_member_in_gg(x0, x1)
member_in_ag(x0)
U6_gg(x0)
U5_ag(x0)
member_in_gg(x0, x1)
U5_gg(x0)

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

(99) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

not_member_in_gg(x0, x1)
U6_gg(x0)
member_in_gg(x0, x1)
U5_gg(x0)

(100) Obligation:

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

SUBSETCHECKED_IN_AGG(Ys, Zs) → U2_AGG(Ys, Zs, member_in_ag(Zs))
U2_AGG(x1, y1, member_out_ag(x0)) → U3_AGG(x0, x1, y1, not_member_out_gg)
U3_AGG(X, Ys, Zs, not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(X, Ys), Zs)

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X)
member_in_ag(.(X4, Xs)) → U5_ag(member_in_ag(Xs))
U5_ag(member_out_ag(X)) → member_out_ag(X)

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0)

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

(101) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule SUBSETCHECKED_IN_AGG(Ys, Zs) → U2_AGG(Ys, Zs, member_in_ag(Zs)) at position [2] we obtained the following new rules [LPAR04]:

SUBSETCHECKED_IN_AGG(y0, .(x0, x1)) → U2_AGG(y0, .(x0, x1), member_out_ag(x0))
SUBSETCHECKED_IN_AGG(y0, .(x0, x1)) → U2_AGG(y0, .(x0, x1), U5_ag(member_in_ag(x1)))

(102) Obligation:

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

U2_AGG(x1, y1, member_out_ag(x0)) → U3_AGG(x0, x1, y1, not_member_out_gg)
U3_AGG(X, Ys, Zs, not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(X, Ys), Zs)
SUBSETCHECKED_IN_AGG(y0, .(x0, x1)) → U2_AGG(y0, .(x0, x1), member_out_ag(x0))
SUBSETCHECKED_IN_AGG(y0, .(x0, x1)) → U2_AGG(y0, .(x0, x1), U5_ag(member_in_ag(x1)))

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X)
member_in_ag(.(X4, Xs)) → U5_ag(member_in_ag(Xs))
U5_ag(member_out_ag(X)) → member_out_ag(X)

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0)

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

(103) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U2_AGG(x1, y1, member_out_ag(x0)) → U3_AGG(x0, x1, y1, not_member_out_gg) we obtained the following new rules [LPAR04]:

U2_AGG(z0, .(z1, z2), member_out_ag(z1)) → U3_AGG(z1, z0, .(z1, z2), not_member_out_gg)
U2_AGG(z0, .(z1, z2), member_out_ag(x2)) → U3_AGG(x2, z0, .(z1, z2), not_member_out_gg)

(104) Obligation:

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

U3_AGG(X, Ys, Zs, not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(X, Ys), Zs)
SUBSETCHECKED_IN_AGG(y0, .(x0, x1)) → U2_AGG(y0, .(x0, x1), member_out_ag(x0))
SUBSETCHECKED_IN_AGG(y0, .(x0, x1)) → U2_AGG(y0, .(x0, x1), U5_ag(member_in_ag(x1)))
U2_AGG(z0, .(z1, z2), member_out_ag(z1)) → U3_AGG(z1, z0, .(z1, z2), not_member_out_gg)
U2_AGG(z0, .(z1, z2), member_out_ag(x2)) → U3_AGG(x2, z0, .(z1, z2), not_member_out_gg)

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X)
member_in_ag(.(X4, Xs)) → U5_ag(member_in_ag(Xs))
U5_ag(member_out_ag(X)) → member_out_ag(X)

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0)

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

(105) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U3_AGG(X, Ys, Zs, not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(X, Ys), Zs) we obtained the following new rules [LPAR04]:

U3_AGG(z1, z0, .(z1, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z1, z0), .(z1, z2))
U3_AGG(z3, z0, .(z1, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z3, z0), .(z1, z2))

(106) Obligation:

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

SUBSETCHECKED_IN_AGG(y0, .(x0, x1)) → U2_AGG(y0, .(x0, x1), member_out_ag(x0))
SUBSETCHECKED_IN_AGG(y0, .(x0, x1)) → U2_AGG(y0, .(x0, x1), U5_ag(member_in_ag(x1)))
U2_AGG(z0, .(z1, z2), member_out_ag(z1)) → U3_AGG(z1, z0, .(z1, z2), not_member_out_gg)
U2_AGG(z0, .(z1, z2), member_out_ag(x2)) → U3_AGG(x2, z0, .(z1, z2), not_member_out_gg)
U3_AGG(z1, z0, .(z1, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z1, z0), .(z1, z2))
U3_AGG(z3, z0, .(z1, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z3, z0), .(z1, z2))

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X)
member_in_ag(.(X4, Xs)) → U5_ag(member_in_ag(Xs))
U5_ag(member_out_ag(X)) → member_out_ag(X)

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0)

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

(107) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule SUBSETCHECKED_IN_AGG(y0, .(x0, x1)) → U2_AGG(y0, .(x0, x1), member_out_ag(x0)) we obtained the following new rules [LPAR04]:

SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2))

(108) Obligation:

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

SUBSETCHECKED_IN_AGG(y0, .(x0, x1)) → U2_AGG(y0, .(x0, x1), U5_ag(member_in_ag(x1)))
U2_AGG(z0, .(z1, z2), member_out_ag(z1)) → U3_AGG(z1, z0, .(z1, z2), not_member_out_gg)
U2_AGG(z0, .(z1, z2), member_out_ag(x2)) → U3_AGG(x2, z0, .(z1, z2), not_member_out_gg)
U3_AGG(z1, z0, .(z1, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z1, z0), .(z1, z2))
U3_AGG(z3, z0, .(z1, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z3, z0), .(z1, z2))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2))

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X)
member_in_ag(.(X4, Xs)) → U5_ag(member_in_ag(Xs))
U5_ag(member_out_ag(X)) → member_out_ag(X)

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0)

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

(109) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule SUBSETCHECKED_IN_AGG(y0, .(x0, x1)) → U2_AGG(y0, .(x0, x1), U5_ag(member_in_ag(x1))) we obtained the following new rules [LPAR04]:

SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), U5_ag(member_in_ag(z2)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), U5_ag(member_in_ag(z3)))

(110) Obligation:

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

U2_AGG(z0, .(z1, z2), member_out_ag(z1)) → U3_AGG(z1, z0, .(z1, z2), not_member_out_gg)
U2_AGG(z0, .(z1, z2), member_out_ag(x2)) → U3_AGG(x2, z0, .(z1, z2), not_member_out_gg)
U3_AGG(z1, z0, .(z1, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z1, z0), .(z1, z2))
U3_AGG(z3, z0, .(z1, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z3, z0), .(z1, z2))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), U5_ag(member_in_ag(z2)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), U5_ag(member_in_ag(z3)))

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X)
member_in_ag(.(X4, Xs)) → U5_ag(member_in_ag(Xs))
U5_ag(member_out_ag(X)) → member_out_ag(X)

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0)

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

(111) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U2_AGG(z0, .(z1, z2), member_out_ag(z1)) → U3_AGG(z1, z0, .(z1, z2), not_member_out_gg) we obtained the following new rules [LPAR04]:

U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0)) → U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg)
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2)) → U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg)

(112) Obligation:

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

U2_AGG(z0, .(z1, z2), member_out_ag(x2)) → U3_AGG(x2, z0, .(z1, z2), not_member_out_gg)
U3_AGG(z1, z0, .(z1, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z1, z0), .(z1, z2))
U3_AGG(z3, z0, .(z1, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z3, z0), .(z1, z2))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), U5_ag(member_in_ag(z2)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), U5_ag(member_in_ag(z3)))
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0)) → U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg)
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2)) → U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg)

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X)
member_in_ag(.(X4, Xs)) → U5_ag(member_in_ag(Xs))
U5_ag(member_out_ag(X)) → member_out_ag(X)

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0)

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

(113) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U2_AGG(z0, .(z1, z2), member_out_ag(x2)) → U3_AGG(x2, z0, .(z1, z2), not_member_out_gg) we obtained the following new rules [LPAR04]:

U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0)) → U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg)
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2)) → U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg)
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(x3)) → U3_AGG(x3, .(z0, z1), .(z0, z2), not_member_out_gg)
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(x3)) → U3_AGG(x3, .(z0, z1), .(z2, z3), not_member_out_gg)

(114) Obligation:

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

U3_AGG(z1, z0, .(z1, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z1, z0), .(z1, z2))
U3_AGG(z3, z0, .(z1, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z3, z0), .(z1, z2))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), U5_ag(member_in_ag(z2)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), U5_ag(member_in_ag(z3)))
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0)) → U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg)
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2)) → U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg)
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(x3)) → U3_AGG(x3, .(z0, z1), .(z0, z2), not_member_out_gg)
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(x3)) → U3_AGG(x3, .(z0, z1), .(z2, z3), not_member_out_gg)

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X)
member_in_ag(.(X4, Xs)) → U5_ag(member_in_ag(Xs))
U5_ag(member_out_ag(X)) → member_out_ag(X)

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0)

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

(115) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U3_AGG(z1, z0, .(z1, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z1, z0), .(z1, z2)) we obtained the following new rules [LPAR04]:

U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2))
U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z2, .(z0, z1)), .(z2, z3))

(116) Obligation:

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

U3_AGG(z3, z0, .(z1, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z3, z0), .(z1, z2))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), U5_ag(member_in_ag(z2)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), U5_ag(member_in_ag(z3)))
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0)) → U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg)
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2)) → U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg)
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(x3)) → U3_AGG(x3, .(z0, z1), .(z0, z2), not_member_out_gg)
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(x3)) → U3_AGG(x3, .(z0, z1), .(z2, z3), not_member_out_gg)
U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2))
U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z2, .(z0, z1)), .(z2, z3))

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X)
member_in_ag(.(X4, Xs)) → U5_ag(member_in_ag(Xs))
U5_ag(member_out_ag(X)) → member_out_ag(X)

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0)

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

(117) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U3_AGG(z3, z0, .(z1, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z3, z0), .(z1, z2)) we obtained the following new rules [LPAR04]:

U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2))
U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z2, .(z0, z1)), .(z2, z3))
U3_AGG(z3, .(z0, z1), .(z0, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z3, .(z0, z1)), .(z0, z2))
U3_AGG(z4, .(z0, z1), .(z2, z3), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z4, .(z0, z1)), .(z2, z3))

(118) Obligation:

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

SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), U5_ag(member_in_ag(z2)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), U5_ag(member_in_ag(z3)))
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0)) → U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg)
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2)) → U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg)
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(x3)) → U3_AGG(x3, .(z0, z1), .(z0, z2), not_member_out_gg)
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(x3)) → U3_AGG(x3, .(z0, z1), .(z2, z3), not_member_out_gg)
U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2))
U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z2, .(z0, z1)), .(z2, z3))
U3_AGG(z3, .(z0, z1), .(z0, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z3, .(z0, z1)), .(z0, z2))
U3_AGG(z4, .(z0, z1), .(z2, z3), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z4, .(z0, z1)), .(z2, z3))

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X)
member_in_ag(.(X4, Xs)) → U5_ag(member_in_ag(Xs))
U5_ag(member_out_ag(X)) → member_out_ag(X)

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0)

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

(119) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0)) we obtained the following new rules [LPAR04]:

SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2)) → U2_AGG(.(z0, .(z0, z1)), .(z0, z2), member_out_ag(z0))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z0, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z0, z3), member_out_ag(z0))

(120) Obligation:

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

SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), U5_ag(member_in_ag(z2)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), U5_ag(member_in_ag(z3)))
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0)) → U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg)
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2)) → U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg)
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(x3)) → U3_AGG(x3, .(z0, z1), .(z0, z2), not_member_out_gg)
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(x3)) → U3_AGG(x3, .(z0, z1), .(z2, z3), not_member_out_gg)
U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2))
U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z2, .(z0, z1)), .(z2, z3))
U3_AGG(z3, .(z0, z1), .(z0, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z3, .(z0, z1)), .(z0, z2))
U3_AGG(z4, .(z0, z1), .(z2, z3), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z4, .(z0, z1)), .(z2, z3))
SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2)) → U2_AGG(.(z0, .(z0, z1)), .(z0, z2), member_out_ag(z0))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z0, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z0, z3), member_out_ag(z0))

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X)
member_in_ag(.(X4, Xs)) → U5_ag(member_in_ag(Xs))
U5_ag(member_out_ag(X)) → member_out_ag(X)

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0)

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

(121) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2)) we obtained the following new rules [LPAR04]:

SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2)) → U2_AGG(.(z0, .(z0, z1)), .(z0, z2), member_out_ag(z0))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z0, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z0, z3), member_out_ag(z0))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z1, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z1, z3), member_out_ag(z1))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z3, z4)) → U2_AGG(.(z0, .(z1, z2)), .(z3, z4), member_out_ag(z3))

(122) Obligation:

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

SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), U5_ag(member_in_ag(z2)))
SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), U5_ag(member_in_ag(z3)))
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0)) → U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg)
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2)) → U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg)
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(x3)) → U3_AGG(x3, .(z0, z1), .(z0, z2), not_member_out_gg)
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(x3)) → U3_AGG(x3, .(z0, z1), .(z2, z3), not_member_out_gg)
U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2))
U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z2, .(z0, z1)), .(z2, z3))
U3_AGG(z3, .(z0, z1), .(z0, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z3, .(z0, z1)), .(z0, z2))
U3_AGG(z4, .(z0, z1), .(z2, z3), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z4, .(z0, z1)), .(z2, z3))
SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2)) → U2_AGG(.(z0, .(z0, z1)), .(z0, z2), member_out_ag(z0))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z0, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z0, z3), member_out_ag(z0))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z1, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z1, z3), member_out_ag(z1))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z3, z4)) → U2_AGG(.(z0, .(z1, z2)), .(z3, z4), member_out_ag(z3))

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X)
member_in_ag(.(X4, Xs)) → U5_ag(member_in_ag(Xs))
U5_ag(member_out_ag(X)) → member_out_ag(X)

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0)

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

(123) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule SUBSETCHECKED_IN_AGG(.(z0, z1), .(z0, z2)) → U2_AGG(.(z0, z1), .(z0, z2), U5_ag(member_in_ag(z2))) we obtained the following new rules [LPAR04]:

SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2)) → U2_AGG(.(z0, .(z0, z1)), .(z0, z2), U5_ag(member_in_ag(z2)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z0, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z0, z3), U5_ag(member_in_ag(z3)))

(124) Obligation:

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

SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), U5_ag(member_in_ag(z3)))
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0)) → U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg)
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2)) → U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg)
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(x3)) → U3_AGG(x3, .(z0, z1), .(z0, z2), not_member_out_gg)
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(x3)) → U3_AGG(x3, .(z0, z1), .(z2, z3), not_member_out_gg)
U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2))
U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z2, .(z0, z1)), .(z2, z3))
U3_AGG(z3, .(z0, z1), .(z0, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z3, .(z0, z1)), .(z0, z2))
U3_AGG(z4, .(z0, z1), .(z2, z3), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z4, .(z0, z1)), .(z2, z3))
SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2)) → U2_AGG(.(z0, .(z0, z1)), .(z0, z2), member_out_ag(z0))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z0, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z0, z3), member_out_ag(z0))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z1, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z1, z3), member_out_ag(z1))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z3, z4)) → U2_AGG(.(z0, .(z1, z2)), .(z3, z4), member_out_ag(z3))
SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2)) → U2_AGG(.(z0, .(z0, z1)), .(z0, z2), U5_ag(member_in_ag(z2)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z0, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z0, z3), U5_ag(member_in_ag(z3)))

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X)
member_in_ag(.(X4, Xs)) → U5_ag(member_in_ag(Xs))
U5_ag(member_out_ag(X)) → member_out_ag(X)

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0)

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

(125) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule SUBSETCHECKED_IN_AGG(.(z0, z1), .(z2, z3)) → U2_AGG(.(z0, z1), .(z2, z3), U5_ag(member_in_ag(z3))) we obtained the following new rules [LPAR04]:

SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2)) → U2_AGG(.(z0, .(z0, z1)), .(z0, z2), U5_ag(member_in_ag(z2)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z0, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z0, z3), U5_ag(member_in_ag(z3)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z1, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z1, z3), U5_ag(member_in_ag(z3)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z3, z4)) → U2_AGG(.(z0, .(z1, z2)), .(z3, z4), U5_ag(member_in_ag(z4)))

(126) Obligation:

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

U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0)) → U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg)
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(z2)) → U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg)
U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(x3)) → U3_AGG(x3, .(z0, z1), .(z0, z2), not_member_out_gg)
U2_AGG(.(z0, z1), .(z2, z3), member_out_ag(x3)) → U3_AGG(x3, .(z0, z1), .(z2, z3), not_member_out_gg)
U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2))
U3_AGG(z2, .(z0, z1), .(z2, z3), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z2, .(z0, z1)), .(z2, z3))
U3_AGG(z3, .(z0, z1), .(z0, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z3, .(z0, z1)), .(z0, z2))
U3_AGG(z4, .(z0, z1), .(z2, z3), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z4, .(z0, z1)), .(z2, z3))
SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2)) → U2_AGG(.(z0, .(z0, z1)), .(z0, z2), member_out_ag(z0))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z0, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z0, z3), member_out_ag(z0))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z1, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z1, z3), member_out_ag(z1))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z3, z4)) → U2_AGG(.(z0, .(z1, z2)), .(z3, z4), member_out_ag(z3))
SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2)) → U2_AGG(.(z0, .(z0, z1)), .(z0, z2), U5_ag(member_in_ag(z2)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z0, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z0, z3), U5_ag(member_in_ag(z3)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z1, z3)) → U2_AGG(.(z0, .(z1, z2)), .(z1, z3), U5_ag(member_in_ag(z3)))
SUBSETCHECKED_IN_AGG(.(z0, .(z1, z2)), .(z3, z4)) → U2_AGG(.(z0, .(z1, z2)), .(z3, z4), U5_ag(member_in_ag(z4)))

The TRS R consists of the following rules:

member_in_ag(.(X, X3)) → member_out_ag(X)
member_in_ag(.(X4, Xs)) → U5_ag(member_in_ag(Xs))
U5_ag(member_out_ag(X)) → member_out_ag(X)

The set Q consists of the following terms:

member_in_ag(x0)
U5_ag(x0)

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

(127) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg) evaluates to t =U3_AGG(z0, .(z0, .(z0, z1)), .(z0, z2), not_member_out_gg)

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Semiunifier: [ ]
• Matcher: [z1 / .(z0, z1)]

---

Rewriting sequence

U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2))
with rule U3_AGG(z0', .(z0', z1'), .(z0', z2'), not_member_out_gg) → SUBSETCHECKED_IN_AGG(.(z0', .(z0', z1')), .(z0', z2')) at position [] and matcher [z0' / z0, z1' / z1, z2' / z2]

SUBSETCHECKED_IN_AGG(.(z0, .(z0, z1)), .(z0, z2)) → U2_AGG(.(z0, .(z0, z1)), .(z0, z2), member_out_ag(z0))
with rule SUBSETCHECKED_IN_AGG(.(z0', .(z0', z1')), .(z0', z2')) → U2_AGG(.(z0', .(z0', z1')), .(z0', z2'), member_out_ag(z0')) at position [] and matcher [z0' / z0, z1' / z1, z2' / z2]

U2_AGG(.(z0, .(z0, z1)), .(z0, z2), member_out_ag(z0)) → U3_AGG(z0, .(z0, .(z0, z1)), .(z0, z2), not_member_out_gg)
with rule U2_AGG(.(z0, z1), .(z0, z2), member_out_ag(z0)) → U3_AGG(z0, .(z0, z1), .(z0, z2), not_member_out_gg)

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.

(128) FALSE