Left Termination proof of /tmp/tmpGOcHlG/pl7.6.2c.pl

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

0 Prolog

  ↳1 PrologToPiTRSProof (⇐)

    ↳2 PiTRS

    ↳3 DependencyPairsProof (⇔)

    ↳4 PiDP

    ↳5 DependencyGraphProof (⇔)

    ↳6 AND

      ↳7 PiDP

        ↳8 UsableRulesProof (⇔)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇐)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔)

        ↳13 TRUE

      ↳14 PiDP

        ↳15 UsableRulesProof (⇔)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇐)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔)

        ↳20 TRUE

      ↳21 PiDP

        ↳22 UsableRulesProof (⇔)

        ↳23 PiDP

        ↳24 PiDPToQDPProof (⇔)

        ↳25 QDP

        ↳26 QDPSizeChangeProof (⇔)

        ↳27 TRUE

      ↳28 PiDP

        ↳29 UsableRulesProof (⇔)

        ↳30 PiDP

        ↳31 PiDPToQDPProof (⇐)

        ↳32 QDP

  ↳33 PrologToPiTRSProof (⇐)

    ↳34 PiTRS

    ↳35 DependencyPairsProof (⇔)

    ↳36 PiDP

    ↳37 DependencyGraphProof (⇔)

    ↳38 AND

      ↳39 PiDP

        ↳40 UsableRulesProof (⇔)

        ↳41 PiDP

        ↳42 PiDPToQDPProof (⇐)

        ↳43 QDP

        ↳44 QDPSizeChangeProof (⇔)

        ↳45 TRUE

      ↳46 PiDP

        ↳47 UsableRulesProof (⇔)

        ↳48 PiDP

        ↳49 PiDPToQDPProof (⇐)

        ↳50 QDP

        ↳51 QDPSizeChangeProof (⇔)

        ↳52 TRUE

      ↳53 PiDP

        ↳54 UsableRulesProof (⇔)

        ↳55 PiDP

        ↳56 PiDPToQDPProof (⇔)

        ↳57 QDP

        ↳58 QDPSizeChangeProof (⇔)

        ↳59 TRUE

      ↳60 PiDP

        ↳61 UsableRulesProof (⇔)

        ↳62 PiDP

        ↳63 PiDPToQDPProof (⇐)

        ↳64 QDP

        ↳65 QDPOrderProof (⇔)

        ↳66 QDP

        ↳67 DependencyGraphProof (⇔)

        ↳68 TRUE

(0) Obligation:

Clauses:

reach(X, Y, E, L) :- member(.(X, .(Y, [])), E).
reach(X, Z, E, L) :- ','(member1(.(X, .(Y, [])), E), ','(member(Y, L), ','(delete(Y, L, V1), reach(Y, Z, E, V1)))).
member(H, .(H, L)).
member(X, .(H, L)) :- member(X, L).
member1(H, .(H, L)).
member1(X, .(H, L)) :- member1(X, L).
delete(X, .(X, Y), Y).
delete(X, .(H, T1), .(H, T2)) :- delete(X, T1, T2).

Queries:

reach(g,g,g,g).

(1) PrologToPiTRSProof (SOUND transformation)

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

reach_in_gggg(X, Y, E, L) → U1_gggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_gggg(X, Y, E, L)
reach_in_gggg(X, Z, E, L) → U2_gggg(X, Z, E, L, member1_in_ag(.(X, .(Y, [])), E))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U7_ag(X, H, L, member1_in_ag(X, L))
U7_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_gggg(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → U3_gggg(X, Z, E, L, Y, member_in_gg(Y, L))
U3_gggg(X, Z, E, L, Y, member_out_gg(Y, L)) → U4_gggg(X, Z, E, L, Y, delete_in_gga(Y, L, V1))
delete_in_gga(X, .(X, Y), Y) → delete_out_gga(X, .(X, Y), Y)
delete_in_gga(X, .(H, T1), .(H, T2)) → U8_gga(X, H, T1, T2, delete_in_gga(X, T1, T2))
U8_gga(X, H, T1, T2, delete_out_gga(X, T1, T2)) → delete_out_gga(X, .(H, T1), .(H, T2))
U4_gggg(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → U5_gggg(X, Z, E, L, reach_in_gggg(Y, Z, E, V1))
U5_gggg(X, Z, E, L, reach_out_gggg(Y, Z, E, V1)) → reach_out_gggg(X, Z, E, L)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(2) Obligation:

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

reach_in_gggg(X, Y, E, L) → U1_gggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_gggg(X, Y, E, L)
reach_in_gggg(X, Z, E, L) → U2_gggg(X, Z, E, L, member1_in_ag(.(X, .(Y, [])), E))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U7_ag(X, H, L, member1_in_ag(X, L))
U7_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_gggg(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → U3_gggg(X, Z, E, L, Y, member_in_gg(Y, L))
U3_gggg(X, Z, E, L, Y, member_out_gg(Y, L)) → U4_gggg(X, Z, E, L, Y, delete_in_gga(Y, L, V1))
delete_in_gga(X, .(X, Y), Y) → delete_out_gga(X, .(X, Y), Y)
delete_in_gga(X, .(H, T1), .(H, T2)) → U8_gga(X, H, T1, T2, delete_in_gga(X, T1, T2))
U8_gga(X, H, T1, T2, delete_out_gga(X, T1, T2)) → delete_out_gga(X, .(H, T1), .(H, T2))
U4_gggg(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → U5_gggg(X, Z, E, L, reach_in_gggg(Y, Z, E, V1))
U5_gggg(X, Z, E, L, reach_out_gggg(Y, Z, E, V1)) → reach_out_gggg(X, Z, E, L)

(3) 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:

REACH_IN_GGGG(X, Y, E, L) → U1_GGGG(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
REACH_IN_GGGG(X, Y, E, L) → MEMBER_IN_GG(.(X, .(Y, [])), E)
MEMBER_IN_GG(X, .(H, L)) → U6_GG(X, H, L, member_in_gg(X, L))
MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)
REACH_IN_GGGG(X, Z, E, L) → U2_GGGG(X, Z, E, L, member1_in_ag(.(X, .(Y, [])), E))
REACH_IN_GGGG(X, Z, E, L) → MEMBER1_IN_AG(.(X, .(Y, [])), E)
MEMBER1_IN_AG(X, .(H, L)) → U7_AG(X, H, L, member1_in_ag(X, L))
MEMBER1_IN_AG(X, .(H, L)) → MEMBER1_IN_AG(X, L)
U2_GGGG(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → U3_GGGG(X, Z, E, L, Y, member_in_gg(Y, L))
U2_GGGG(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → MEMBER_IN_GG(Y, L)
U3_GGGG(X, Z, E, L, Y, member_out_gg(Y, L)) → U4_GGGG(X, Z, E, L, Y, delete_in_gga(Y, L, V1))
U3_GGGG(X, Z, E, L, Y, member_out_gg(Y, L)) → DELETE_IN_GGA(Y, L, V1)
DELETE_IN_GGA(X, .(H, T1), .(H, T2)) → U8_GGA(X, H, T1, T2, delete_in_gga(X, T1, T2))
DELETE_IN_GGA(X, .(H, T1), .(H, T2)) → DELETE_IN_GGA(X, T1, T2)
U4_GGGG(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → U5_GGGG(X, Z, E, L, reach_in_gggg(Y, Z, E, V1))
U4_GGGG(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → REACH_IN_GGGG(Y, Z, E, V1)

The TRS R consists of the following rules:

reach_in_gggg(X, Y, E, L) → U1_gggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_gggg(X, Y, E, L)
reach_in_gggg(X, Z, E, L) → U2_gggg(X, Z, E, L, member1_in_ag(.(X, .(Y, [])), E))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U7_ag(X, H, L, member1_in_ag(X, L))
U7_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_gggg(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → U3_gggg(X, Z, E, L, Y, member_in_gg(Y, L))
U3_gggg(X, Z, E, L, Y, member_out_gg(Y, L)) → U4_gggg(X, Z, E, L, Y, delete_in_gga(Y, L, V1))
delete_in_gga(X, .(X, Y), Y) → delete_out_gga(X, .(X, Y), Y)
delete_in_gga(X, .(H, T1), .(H, T2)) → U8_gga(X, H, T1, T2, delete_in_gga(X, T1, T2))
U8_gga(X, H, T1, T2, delete_out_gga(X, T1, T2)) → delete_out_gga(X, .(H, T1), .(H, T2))
U4_gggg(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → U5_gggg(X, Z, E, L, reach_in_gggg(Y, Z, E, V1))
U5_gggg(X, Z, E, L, reach_out_gggg(Y, Z, E, V1)) → reach_out_gggg(X, Z, E, L)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4) = reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5) = U1_gggg(x5)
member_in_gg(x1, x2) = member_in_gg(x1, x2)
.(x1, x2) = .(x1, x2)
member_out_gg(x1, x2) = member_out_gg
U6_gg(x1, x2, x3, x4) = U6_gg(x4)
[] = []
reach_out_gggg(x1, x2, x3, x4) = reach_out_gggg
U2_gggg(x1, x2, x3, x4, x5) = U2_gggg(x2, x3, x4, x5)
member1_in_ag(x1, x2) = member1_in_ag(x2)
member1_out_ag(x1, x2) = member1_out_ag(x1)
U7_ag(x1, x2, x3, x4) = U7_ag(x4)
U3_gggg(x1, x2, x3, x4, x5, x6) = U3_gggg(x2, x3, x4, x5, x6)
U4_gggg(x1, x2, x3, x4, x5, x6) = U4_gggg(x2, x3, x5, x6)
delete_in_gga(x1, x2, x3) = delete_in_gga(x1, x2)
delete_out_gga(x1, x2, x3) = delete_out_gga(x3)
U8_gga(x1, x2, x3, x4, x5) = U8_gga(x2, x5)
U5_gggg(x1, x2, x3, x4, x5) = U5_gggg(x5)
REACH_IN_GGGG(x1, x2, x3, x4) = REACH_IN_GGGG(x1, x2, x3, x4)
U1_GGGG(x1, x2, x3, x4, x5) = U1_GGGG(x5)
MEMBER_IN_GG(x1, x2) = MEMBER_IN_GG(x1, x2)
U6_GG(x1, x2, x3, x4) = U6_GG(x4)
U2_GGGG(x1, x2, x3, x4, x5) = U2_GGGG(x2, x3, x4, x5)
MEMBER1_IN_AG(x1, x2) = MEMBER1_IN_AG(x2)
U7_AG(x1, x2, x3, x4) = U7_AG(x4)
U3_GGGG(x1, x2, x3, x4, x5, x6) = U3_GGGG(x2, x3, x4, x5, x6)
U4_GGGG(x1, x2, x3, x4, x5, x6) = U4_GGGG(x2, x3, x5, x6)
DELETE_IN_GGA(x1, x2, x3) = DELETE_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3, x4, x5) = U8_GGA(x2, x5)
U5_GGGG(x1, x2, x3, x4, x5) = U5_GGGG(x5)

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

(4) Obligation:

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

REACH_IN_GGGG(X, Y, E, L) → U1_GGGG(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
REACH_IN_GGGG(X, Y, E, L) → MEMBER_IN_GG(.(X, .(Y, [])), E)
MEMBER_IN_GG(X, .(H, L)) → U6_GG(X, H, L, member_in_gg(X, L))
MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)
REACH_IN_GGGG(X, Z, E, L) → U2_GGGG(X, Z, E, L, member1_in_ag(.(X, .(Y, [])), E))
REACH_IN_GGGG(X, Z, E, L) → MEMBER1_IN_AG(.(X, .(Y, [])), E)
MEMBER1_IN_AG(X, .(H, L)) → U7_AG(X, H, L, member1_in_ag(X, L))
MEMBER1_IN_AG(X, .(H, L)) → MEMBER1_IN_AG(X, L)
U2_GGGG(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → U3_GGGG(X, Z, E, L, Y, member_in_gg(Y, L))
U2_GGGG(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → MEMBER_IN_GG(Y, L)
U3_GGGG(X, Z, E, L, Y, member_out_gg(Y, L)) → U4_GGGG(X, Z, E, L, Y, delete_in_gga(Y, L, V1))
U3_GGGG(X, Z, E, L, Y, member_out_gg(Y, L)) → DELETE_IN_GGA(Y, L, V1)
DELETE_IN_GGA(X, .(H, T1), .(H, T2)) → U8_GGA(X, H, T1, T2, delete_in_gga(X, T1, T2))
DELETE_IN_GGA(X, .(H, T1), .(H, T2)) → DELETE_IN_GGA(X, T1, T2)
U4_GGGG(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → U5_GGGG(X, Z, E, L, reach_in_gggg(Y, Z, E, V1))
U4_GGGG(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → REACH_IN_GGGG(Y, Z, E, V1)

The TRS R consists of the following rules:

reach_in_gggg(X, Y, E, L) → U1_gggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_gggg(X, Y, E, L)
reach_in_gggg(X, Z, E, L) → U2_gggg(X, Z, E, L, member1_in_ag(.(X, .(Y, [])), E))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U7_ag(X, H, L, member1_in_ag(X, L))
U7_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_gggg(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → U3_gggg(X, Z, E, L, Y, member_in_gg(Y, L))
U3_gggg(X, Z, E, L, Y, member_out_gg(Y, L)) → U4_gggg(X, Z, E, L, Y, delete_in_gga(Y, L, V1))
delete_in_gga(X, .(X, Y), Y) → delete_out_gga(X, .(X, Y), Y)
delete_in_gga(X, .(H, T1), .(H, T2)) → U8_gga(X, H, T1, T2, delete_in_gga(X, T1, T2))
U8_gga(X, H, T1, T2, delete_out_gga(X, T1, T2)) → delete_out_gga(X, .(H, T1), .(H, T2))
U4_gggg(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → U5_gggg(X, Z, E, L, reach_in_gggg(Y, Z, E, V1))
U5_gggg(X, Z, E, L, reach_out_gggg(Y, Z, E, V1)) → reach_out_gggg(X, Z, E, L)

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 9 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

DELETE_IN_GGA(X, .(H, T1), .(H, T2)) → DELETE_IN_GGA(X, T1, T2)

The TRS R consists of the following rules:

reach_in_gggg(X, Y, E, L) → U1_gggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_gggg(X, Y, E, L)
reach_in_gggg(X, Z, E, L) → U2_gggg(X, Z, E, L, member1_in_ag(.(X, .(Y, [])), E))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U7_ag(X, H, L, member1_in_ag(X, L))
U7_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_gggg(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → U3_gggg(X, Z, E, L, Y, member_in_gg(Y, L))
U3_gggg(X, Z, E, L, Y, member_out_gg(Y, L)) → U4_gggg(X, Z, E, L, Y, delete_in_gga(Y, L, V1))
delete_in_gga(X, .(X, Y), Y) → delete_out_gga(X, .(X, Y), Y)
delete_in_gga(X, .(H, T1), .(H, T2)) → U8_gga(X, H, T1, T2, delete_in_gga(X, T1, T2))
U8_gga(X, H, T1, T2, delete_out_gga(X, T1, T2)) → delete_out_gga(X, .(H, T1), .(H, T2))
U4_gggg(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → U5_gggg(X, Z, E, L, reach_in_gggg(Y, Z, E, V1))
U5_gggg(X, Z, E, L, reach_out_gggg(Y, Z, E, V1)) → reach_out_gggg(X, Z, E, L)

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

DELETE_IN_GGA(X, .(H, T1), .(H, T2)) → DELETE_IN_GGA(X, T1, T2)

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

DELETE_IN_GGA(X, .(H, T1)) → DELETE_IN_GGA(X, T1)

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

(12) 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:

DELETE_IN_GGA(X, .(H, T1)) → DELETE_IN_GGA(X, T1)
The graph contains the following edges 1 >= 1, 2 > 2

(13) TRUE

(14) Obligation:

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

MEMBER1_IN_AG(X, .(H, L)) → MEMBER1_IN_AG(X, L)

The TRS R consists of the following rules:

reach_in_gggg(X, Y, E, L) → U1_gggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_gggg(X, Y, E, L)
reach_in_gggg(X, Z, E, L) → U2_gggg(X, Z, E, L, member1_in_ag(.(X, .(Y, [])), E))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U7_ag(X, H, L, member1_in_ag(X, L))
U7_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_gggg(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → U3_gggg(X, Z, E, L, Y, member_in_gg(Y, L))
U3_gggg(X, Z, E, L, Y, member_out_gg(Y, L)) → U4_gggg(X, Z, E, L, Y, delete_in_gga(Y, L, V1))
delete_in_gga(X, .(X, Y), Y) → delete_out_gga(X, .(X, Y), Y)
delete_in_gga(X, .(H, T1), .(H, T2)) → U8_gga(X, H, T1, T2, delete_in_gga(X, T1, T2))
U8_gga(X, H, T1, T2, delete_out_gga(X, T1, T2)) → delete_out_gga(X, .(H, T1), .(H, T2))
U4_gggg(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → U5_gggg(X, Z, E, L, reach_in_gggg(Y, Z, E, V1))
U5_gggg(X, Z, E, L, reach_out_gggg(Y, Z, E, V1)) → reach_out_gggg(X, Z, E, L)

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

MEMBER1_IN_AG(X, .(H, L)) → MEMBER1_IN_AG(X, L)

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

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

MEMBER1_IN_AG(.(H, L)) → MEMBER1_IN_AG(L)

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

(19) 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:

MEMBER1_IN_AG(.(H, L)) → MEMBER1_IN_AG(L)
The graph contains the following edges 1 > 1

(20) TRUE

(21) Obligation:

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

MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)

The TRS R consists of the following rules:

reach_in_gggg(X, Y, E, L) → U1_gggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_gggg(X, Y, E, L)
reach_in_gggg(X, Z, E, L) → U2_gggg(X, Z, E, L, member1_in_ag(.(X, .(Y, [])), E))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U7_ag(X, H, L, member1_in_ag(X, L))
U7_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_gggg(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → U3_gggg(X, Z, E, L, Y, member_in_gg(Y, L))
U3_gggg(X, Z, E, L, Y, member_out_gg(Y, L)) → U4_gggg(X, Z, E, L, Y, delete_in_gga(Y, L, V1))
delete_in_gga(X, .(X, Y), Y) → delete_out_gga(X, .(X, Y), Y)
delete_in_gga(X, .(H, T1), .(H, T2)) → U8_gga(X, H, T1, T2, delete_in_gga(X, T1, T2))
U8_gga(X, H, T1, T2, delete_out_gga(X, T1, T2)) → delete_out_gga(X, .(H, T1), .(H, T2))
U4_gggg(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → U5_gggg(X, Z, E, L, reach_in_gggg(Y, Z, E, V1))
U5_gggg(X, Z, E, L, reach_out_gggg(Y, Z, E, V1)) → reach_out_gggg(X, Z, E, L)

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)

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

(24) PiDPToQDPProof (EQUIVALENT transformation)

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

(25) Obligation:

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

MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)

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

(26) 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, .(H, L)) → MEMBER_IN_GG(X, L)
The graph contains the following edges 1 >= 1, 2 > 2

(27) TRUE

(28) Obligation:

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

REACH_IN_GGGG(X, Z, E, L) → U2_GGGG(X, Z, E, L, member1_in_ag(.(X, .(Y, [])), E))
U2_GGGG(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → U3_GGGG(X, Z, E, L, Y, member_in_gg(Y, L))
U3_GGGG(X, Z, E, L, Y, member_out_gg(Y, L)) → U4_GGGG(X, Z, E, L, Y, delete_in_gga(Y, L, V1))
U4_GGGG(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → REACH_IN_GGGG(Y, Z, E, V1)

The TRS R consists of the following rules:

reach_in_gggg(X, Y, E, L) → U1_gggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_gggg(X, Y, E, L)
reach_in_gggg(X, Z, E, L) → U2_gggg(X, Z, E, L, member1_in_ag(.(X, .(Y, [])), E))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U7_ag(X, H, L, member1_in_ag(X, L))
U7_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_gggg(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → U3_gggg(X, Z, E, L, Y, member_in_gg(Y, L))
U3_gggg(X, Z, E, L, Y, member_out_gg(Y, L)) → U4_gggg(X, Z, E, L, Y, delete_in_gga(Y, L, V1))
delete_in_gga(X, .(X, Y), Y) → delete_out_gga(X, .(X, Y), Y)
delete_in_gga(X, .(H, T1), .(H, T2)) → U8_gga(X, H, T1, T2, delete_in_gga(X, T1, T2))
U8_gga(X, H, T1, T2, delete_out_gga(X, T1, T2)) → delete_out_gga(X, .(H, T1), .(H, T2))
U4_gggg(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → U5_gggg(X, Z, E, L, reach_in_gggg(Y, Z, E, V1))
U5_gggg(X, Z, E, L, reach_out_gggg(Y, Z, E, V1)) → reach_out_gggg(X, Z, E, L)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4) = reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5) = U1_gggg(x5)
member_in_gg(x1, x2) = member_in_gg(x1, x2)
.(x1, x2) = .(x1, x2)
member_out_gg(x1, x2) = member_out_gg
U6_gg(x1, x2, x3, x4) = U6_gg(x4)
[] = []
reach_out_gggg(x1, x2, x3, x4) = reach_out_gggg
U2_gggg(x1, x2, x3, x4, x5) = U2_gggg(x2, x3, x4, x5)
member1_in_ag(x1, x2) = member1_in_ag(x2)
member1_out_ag(x1, x2) = member1_out_ag(x1)
U7_ag(x1, x2, x3, x4) = U7_ag(x4)
U3_gggg(x1, x2, x3, x4, x5, x6) = U3_gggg(x2, x3, x4, x5, x6)
U4_gggg(x1, x2, x3, x4, x5, x6) = U4_gggg(x2, x3, x5, x6)
delete_in_gga(x1, x2, x3) = delete_in_gga(x1, x2)
delete_out_gga(x1, x2, x3) = delete_out_gga(x3)
U8_gga(x1, x2, x3, x4, x5) = U8_gga(x2, x5)
U5_gggg(x1, x2, x3, x4, x5) = U5_gggg(x5)
REACH_IN_GGGG(x1, x2, x3, x4) = REACH_IN_GGGG(x1, x2, x3, x4)
U2_GGGG(x1, x2, x3, x4, x5) = U2_GGGG(x2, x3, x4, x5)
U3_GGGG(x1, x2, x3, x4, x5, x6) = U3_GGGG(x2, x3, x4, x5, x6)
U4_GGGG(x1, x2, x3, x4, x5, x6) = U4_GGGG(x2, x3, x5, x6)

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

(29) UsableRulesProof (EQUIVALENT transformation)

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

(30) Obligation:

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

REACH_IN_GGGG(X, Z, E, L) → U2_GGGG(X, Z, E, L, member1_in_ag(.(X, .(Y, [])), E))
U2_GGGG(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → U3_GGGG(X, Z, E, L, Y, member_in_gg(Y, L))
U3_GGGG(X, Z, E, L, Y, member_out_gg(Y, L)) → U4_GGGG(X, Z, E, L, Y, delete_in_gga(Y, L, V1))
U4_GGGG(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → REACH_IN_GGGG(Y, Z, E, V1)

The TRS R consists of the following rules:

member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U7_ag(X, H, L, member1_in_ag(X, L))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
delete_in_gga(X, .(X, Y), Y) → delete_out_gga(X, .(X, Y), Y)
delete_in_gga(X, .(H, T1), .(H, T2)) → U8_gga(X, H, T1, T2, delete_in_gga(X, T1, T2))
U7_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U8_gga(X, H, T1, T2, delete_out_gga(X, T1, T2)) → delete_out_gga(X, .(H, T1), .(H, T2))

The argument filtering Pi contains the following mapping:
member_in_gg(x1, x2) = member_in_gg(x1, x2)
.(x1, x2) = .(x1, x2)
member_out_gg(x1, x2) = member_out_gg
U6_gg(x1, x2, x3, x4) = U6_gg(x4)
[] = []
member1_in_ag(x1, x2) = member1_in_ag(x2)
member1_out_ag(x1, x2) = member1_out_ag(x1)
U7_ag(x1, x2, x3, x4) = U7_ag(x4)
delete_in_gga(x1, x2, x3) = delete_in_gga(x1, x2)
delete_out_gga(x1, x2, x3) = delete_out_gga(x3)
U8_gga(x1, x2, x3, x4, x5) = U8_gga(x2, x5)
REACH_IN_GGGG(x1, x2, x3, x4) = REACH_IN_GGGG(x1, x2, x3, x4)
U2_GGGG(x1, x2, x3, x4, x5) = U2_GGGG(x2, x3, x4, x5)
U3_GGGG(x1, x2, x3, x4, x5, x6) = U3_GGGG(x2, x3, x4, x5, x6)
U4_GGGG(x1, x2, x3, x4, x5, x6) = U4_GGGG(x2, x3, x5, x6)

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

(31) PiDPToQDPProof (SOUND transformation)

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

(32) Obligation:

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

REACH_IN_GGGG(X, Z, E, L) → U2_GGGG(Z, E, L, member1_in_ag(E))
U2_GGGG(Z, E, L, member1_out_ag(.(X, .(Y, [])))) → U3_GGGG(Z, E, L, Y, member_in_gg(Y, L))
U3_GGGG(Z, E, L, Y, member_out_gg) → U4_GGGG(Z, E, Y, delete_in_gga(Y, L))
U4_GGGG(Z, E, Y, delete_out_gga(V1)) → REACH_IN_GGGG(Y, Z, E, V1)

The TRS R consists of the following rules:

member1_in_ag(.(H, L)) → member1_out_ag(H)
member1_in_ag(.(H, L)) → U7_ag(member1_in_ag(L))
member_in_gg(H, .(H, L)) → member_out_gg
member_in_gg(X, .(H, L)) → U6_gg(member_in_gg(X, L))
delete_in_gga(X, .(X, Y)) → delete_out_gga(Y)
delete_in_gga(X, .(H, T1)) → U8_gga(H, delete_in_gga(X, T1))
U7_ag(member1_out_ag(X)) → member1_out_ag(X)
U6_gg(member_out_gg) → member_out_gg
U8_gga(H, delete_out_gga(T2)) → delete_out_gga(.(H, T2))

The set Q consists of the following terms:

member1_in_ag(x0)
member_in_gg(x0, x1)
delete_in_gga(x0, x1)
U7_ag(x0)
U6_gg(x0)
U8_gga(x0, x1)

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

(33) PrologToPiTRSProof (SOUND transformation)

reach_in_gggg(X, Y, E, L) → U1_gggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_gggg(X, Y, E, L)
reach_in_gggg(X, Z, E, L) → U2_gggg(X, Z, E, L, member1_in_ag(.(X, .(Y, [])), E))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U7_ag(X, H, L, member1_in_ag(X, L))
U7_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_gggg(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → U3_gggg(X, Z, E, L, Y, member_in_gg(Y, L))
U3_gggg(X, Z, E, L, Y, member_out_gg(Y, L)) → U4_gggg(X, Z, E, L, Y, delete_in_gga(Y, L, V1))
delete_in_gga(X, .(X, Y), Y) → delete_out_gga(X, .(X, Y), Y)
delete_in_gga(X, .(H, T1), .(H, T2)) → U8_gga(X, H, T1, T2, delete_in_gga(X, T1, T2))
U8_gga(X, H, T1, T2, delete_out_gga(X, T1, T2)) → delete_out_gga(X, .(H, T1), .(H, T2))
U4_gggg(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → U5_gggg(X, Z, E, L, reach_in_gggg(Y, Z, E, V1))
U5_gggg(X, Z, E, L, reach_out_gggg(Y, Z, E, V1)) → reach_out_gggg(X, Z, E, L)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(34) Obligation:

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

reach_in_gggg(X, Y, E, L) → U1_gggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_gggg(X, Y, E, L)
reach_in_gggg(X, Z, E, L) → U2_gggg(X, Z, E, L, member1_in_ag(.(X, .(Y, [])), E))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U7_ag(X, H, L, member1_in_ag(X, L))
U7_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_gggg(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → U3_gggg(X, Z, E, L, Y, member_in_gg(Y, L))
U3_gggg(X, Z, E, L, Y, member_out_gg(Y, L)) → U4_gggg(X, Z, E, L, Y, delete_in_gga(Y, L, V1))
delete_in_gga(X, .(X, Y), Y) → delete_out_gga(X, .(X, Y), Y)
delete_in_gga(X, .(H, T1), .(H, T2)) → U8_gga(X, H, T1, T2, delete_in_gga(X, T1, T2))
U8_gga(X, H, T1, T2, delete_out_gga(X, T1, T2)) → delete_out_gga(X, .(H, T1), .(H, T2))
U4_gggg(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → U5_gggg(X, Z, E, L, reach_in_gggg(Y, Z, E, V1))
U5_gggg(X, Z, E, L, reach_out_gggg(Y, Z, E, V1)) → reach_out_gggg(X, Z, E, L)

(35) 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:

REACH_IN_GGGG(X, Y, E, L) → U1_GGGG(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
REACH_IN_GGGG(X, Y, E, L) → MEMBER_IN_GG(.(X, .(Y, [])), E)
MEMBER_IN_GG(X, .(H, L)) → U6_GG(X, H, L, member_in_gg(X, L))
MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)
REACH_IN_GGGG(X, Z, E, L) → U2_GGGG(X, Z, E, L, member1_in_ag(.(X, .(Y, [])), E))
REACH_IN_GGGG(X, Z, E, L) → MEMBER1_IN_AG(.(X, .(Y, [])), E)
MEMBER1_IN_AG(X, .(H, L)) → U7_AG(X, H, L, member1_in_ag(X, L))
MEMBER1_IN_AG(X, .(H, L)) → MEMBER1_IN_AG(X, L)
U2_GGGG(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → U3_GGGG(X, Z, E, L, Y, member_in_gg(Y, L))
U2_GGGG(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → MEMBER_IN_GG(Y, L)
U3_GGGG(X, Z, E, L, Y, member_out_gg(Y, L)) → U4_GGGG(X, Z, E, L, Y, delete_in_gga(Y, L, V1))
U3_GGGG(X, Z, E, L, Y, member_out_gg(Y, L)) → DELETE_IN_GGA(Y, L, V1)
DELETE_IN_GGA(X, .(H, T1), .(H, T2)) → U8_GGA(X, H, T1, T2, delete_in_gga(X, T1, T2))
DELETE_IN_GGA(X, .(H, T1), .(H, T2)) → DELETE_IN_GGA(X, T1, T2)
U4_GGGG(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → U5_GGGG(X, Z, E, L, reach_in_gggg(Y, Z, E, V1))
U4_GGGG(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → REACH_IN_GGGG(Y, Z, E, V1)

The TRS R consists of the following rules:

reach_in_gggg(X, Y, E, L) → U1_gggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_gggg(X, Y, E, L)
reach_in_gggg(X, Z, E, L) → U2_gggg(X, Z, E, L, member1_in_ag(.(X, .(Y, [])), E))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U7_ag(X, H, L, member1_in_ag(X, L))
U7_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_gggg(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → U3_gggg(X, Z, E, L, Y, member_in_gg(Y, L))
U3_gggg(X, Z, E, L, Y, member_out_gg(Y, L)) → U4_gggg(X, Z, E, L, Y, delete_in_gga(Y, L, V1))
delete_in_gga(X, .(X, Y), Y) → delete_out_gga(X, .(X, Y), Y)
delete_in_gga(X, .(H, T1), .(H, T2)) → U8_gga(X, H, T1, T2, delete_in_gga(X, T1, T2))
U8_gga(X, H, T1, T2, delete_out_gga(X, T1, T2)) → delete_out_gga(X, .(H, T1), .(H, T2))
U4_gggg(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → U5_gggg(X, Z, E, L, reach_in_gggg(Y, Z, E, V1))
U5_gggg(X, Z, E, L, reach_out_gggg(Y, Z, E, V1)) → reach_out_gggg(X, Z, E, L)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4) = reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5) = U1_gggg(x1, x2, x3, x4, x5)
member_in_gg(x1, x2) = member_in_gg(x1, x2)
.(x1, x2) = .(x1, x2)
member_out_gg(x1, x2) = member_out_gg(x1, x2)
U6_gg(x1, x2, x3, x4) = U6_gg(x1, x2, x3, x4)
[] = []
reach_out_gggg(x1, x2, x3, x4) = reach_out_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5) = U2_gggg(x1, x2, x3, x4, x5)
member1_in_ag(x1, x2) = member1_in_ag(x2)
member1_out_ag(x1, x2) = member1_out_ag(x1, x2)
U7_ag(x1, x2, x3, x4) = U7_ag(x2, x3, x4)
U3_gggg(x1, x2, x3, x4, x5, x6) = U3_gggg(x1, x2, x3, x4, x5, x6)
U4_gggg(x1, x2, x3, x4, x5, x6) = U4_gggg(x1, x2, x3, x4, x5, x6)
delete_in_gga(x1, x2, x3) = delete_in_gga(x1, x2)
delete_out_gga(x1, x2, x3) = delete_out_gga(x1, x2, x3)
U8_gga(x1, x2, x3, x4, x5) = U8_gga(x1, x2, x3, x5)
U5_gggg(x1, x2, x3, x4, x5) = U5_gggg(x1, x2, x3, x4, x5)
REACH_IN_GGGG(x1, x2, x3, x4) = REACH_IN_GGGG(x1, x2, x3, x4)
U1_GGGG(x1, x2, x3, x4, x5) = U1_GGGG(x1, x2, x3, x4, x5)
MEMBER_IN_GG(x1, x2) = MEMBER_IN_GG(x1, x2)
U6_GG(x1, x2, x3, x4) = U6_GG(x1, x2, x3, x4)
U2_GGGG(x1, x2, x3, x4, x5) = U2_GGGG(x1, x2, x3, x4, x5)
MEMBER1_IN_AG(x1, x2) = MEMBER1_IN_AG(x2)
U7_AG(x1, x2, x3, x4) = U7_AG(x2, x3, x4)
U3_GGGG(x1, x2, x3, x4, x5, x6) = U3_GGGG(x1, x2, x3, x4, x5, x6)
U4_GGGG(x1, x2, x3, x4, x5, x6) = U4_GGGG(x1, x2, x3, x4, x5, x6)
DELETE_IN_GGA(x1, x2, x3) = DELETE_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3, x4, x5) = U8_GGA(x1, x2, x3, x5)
U5_GGGG(x1, x2, x3, x4, x5) = U5_GGGG(x1, x2, x3, x4, x5)

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

(36) Obligation:

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

REACH_IN_GGGG(X, Y, E, L) → U1_GGGG(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
REACH_IN_GGGG(X, Y, E, L) → MEMBER_IN_GG(.(X, .(Y, [])), E)
MEMBER_IN_GG(X, .(H, L)) → U6_GG(X, H, L, member_in_gg(X, L))
MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)
REACH_IN_GGGG(X, Z, E, L) → U2_GGGG(X, Z, E, L, member1_in_ag(.(X, .(Y, [])), E))
REACH_IN_GGGG(X, Z, E, L) → MEMBER1_IN_AG(.(X, .(Y, [])), E)
MEMBER1_IN_AG(X, .(H, L)) → U7_AG(X, H, L, member1_in_ag(X, L))
MEMBER1_IN_AG(X, .(H, L)) → MEMBER1_IN_AG(X, L)
U2_GGGG(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → U3_GGGG(X, Z, E, L, Y, member_in_gg(Y, L))
U2_GGGG(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → MEMBER_IN_GG(Y, L)
U3_GGGG(X, Z, E, L, Y, member_out_gg(Y, L)) → U4_GGGG(X, Z, E, L, Y, delete_in_gga(Y, L, V1))
U3_GGGG(X, Z, E, L, Y, member_out_gg(Y, L)) → DELETE_IN_GGA(Y, L, V1)
DELETE_IN_GGA(X, .(H, T1), .(H, T2)) → U8_GGA(X, H, T1, T2, delete_in_gga(X, T1, T2))
DELETE_IN_GGA(X, .(H, T1), .(H, T2)) → DELETE_IN_GGA(X, T1, T2)
U4_GGGG(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → U5_GGGG(X, Z, E, L, reach_in_gggg(Y, Z, E, V1))
U4_GGGG(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → REACH_IN_GGGG(Y, Z, E, V1)

The TRS R consists of the following rules:

reach_in_gggg(X, Y, E, L) → U1_gggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_gggg(X, Y, E, L)
reach_in_gggg(X, Z, E, L) → U2_gggg(X, Z, E, L, member1_in_ag(.(X, .(Y, [])), E))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U7_ag(X, H, L, member1_in_ag(X, L))
U7_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_gggg(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → U3_gggg(X, Z, E, L, Y, member_in_gg(Y, L))
U3_gggg(X, Z, E, L, Y, member_out_gg(Y, L)) → U4_gggg(X, Z, E, L, Y, delete_in_gga(Y, L, V1))
delete_in_gga(X, .(X, Y), Y) → delete_out_gga(X, .(X, Y), Y)
delete_in_gga(X, .(H, T1), .(H, T2)) → U8_gga(X, H, T1, T2, delete_in_gga(X, T1, T2))
U8_gga(X, H, T1, T2, delete_out_gga(X, T1, T2)) → delete_out_gga(X, .(H, T1), .(H, T2))
U4_gggg(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → U5_gggg(X, Z, E, L, reach_in_gggg(Y, Z, E, V1))
U5_gggg(X, Z, E, L, reach_out_gggg(Y, Z, E, V1)) → reach_out_gggg(X, Z, E, L)

(37) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 9 less nodes.

(38) Complex Obligation (AND)

(39) Obligation:

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

DELETE_IN_GGA(X, .(H, T1), .(H, T2)) → DELETE_IN_GGA(X, T1, T2)

The TRS R consists of the following rules:

reach_in_gggg(X, Y, E, L) → U1_gggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_gggg(X, Y, E, L)
reach_in_gggg(X, Z, E, L) → U2_gggg(X, Z, E, L, member1_in_ag(.(X, .(Y, [])), E))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U7_ag(X, H, L, member1_in_ag(X, L))
U7_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_gggg(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → U3_gggg(X, Z, E, L, Y, member_in_gg(Y, L))
U3_gggg(X, Z, E, L, Y, member_out_gg(Y, L)) → U4_gggg(X, Z, E, L, Y, delete_in_gga(Y, L, V1))
delete_in_gga(X, .(X, Y), Y) → delete_out_gga(X, .(X, Y), Y)
delete_in_gga(X, .(H, T1), .(H, T2)) → U8_gga(X, H, T1, T2, delete_in_gga(X, T1, T2))
U8_gga(X, H, T1, T2, delete_out_gga(X, T1, T2)) → delete_out_gga(X, .(H, T1), .(H, T2))
U4_gggg(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → U5_gggg(X, Z, E, L, reach_in_gggg(Y, Z, E, V1))
U5_gggg(X, Z, E, L, reach_out_gggg(Y, Z, E, V1)) → reach_out_gggg(X, Z, E, L)

(40) UsableRulesProof (EQUIVALENT transformation)

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

(41) Obligation:

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

DELETE_IN_GGA(X, .(H, T1), .(H, T2)) → DELETE_IN_GGA(X, T1, T2)

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

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

(42) PiDPToQDPProof (SOUND transformation)

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

(43) Obligation:

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

DELETE_IN_GGA(X, .(H, T1)) → DELETE_IN_GGA(X, T1)

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

(44) 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:

DELETE_IN_GGA(X, .(H, T1)) → DELETE_IN_GGA(X, T1)
The graph contains the following edges 1 >= 1, 2 > 2

(45) TRUE

(46) Obligation:

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

MEMBER1_IN_AG(X, .(H, L)) → MEMBER1_IN_AG(X, L)

The TRS R consists of the following rules:

reach_in_gggg(X, Y, E, L) → U1_gggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_gggg(X, Y, E, L)
reach_in_gggg(X, Z, E, L) → U2_gggg(X, Z, E, L, member1_in_ag(.(X, .(Y, [])), E))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U7_ag(X, H, L, member1_in_ag(X, L))
U7_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_gggg(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → U3_gggg(X, Z, E, L, Y, member_in_gg(Y, L))
U3_gggg(X, Z, E, L, Y, member_out_gg(Y, L)) → U4_gggg(X, Z, E, L, Y, delete_in_gga(Y, L, V1))
delete_in_gga(X, .(X, Y), Y) → delete_out_gga(X, .(X, Y), Y)
delete_in_gga(X, .(H, T1), .(H, T2)) → U8_gga(X, H, T1, T2, delete_in_gga(X, T1, T2))
U8_gga(X, H, T1, T2, delete_out_gga(X, T1, T2)) → delete_out_gga(X, .(H, T1), .(H, T2))
U4_gggg(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → U5_gggg(X, Z, E, L, reach_in_gggg(Y, Z, E, V1))
U5_gggg(X, Z, E, L, reach_out_gggg(Y, Z, E, V1)) → reach_out_gggg(X, Z, E, L)

(47) UsableRulesProof (EQUIVALENT transformation)

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

(48) Obligation:

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

MEMBER1_IN_AG(X, .(H, L)) → MEMBER1_IN_AG(X, L)

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

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

(49) PiDPToQDPProof (SOUND transformation)

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

(50) Obligation:

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

MEMBER1_IN_AG(.(H, L)) → MEMBER1_IN_AG(L)

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

(51) 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:

MEMBER1_IN_AG(.(H, L)) → MEMBER1_IN_AG(L)
The graph contains the following edges 1 > 1

(52) TRUE

(53) Obligation:

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

MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)

The TRS R consists of the following rules:

reach_in_gggg(X, Y, E, L) → U1_gggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_gggg(X, Y, E, L)
reach_in_gggg(X, Z, E, L) → U2_gggg(X, Z, E, L, member1_in_ag(.(X, .(Y, [])), E))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U7_ag(X, H, L, member1_in_ag(X, L))
U7_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_gggg(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → U3_gggg(X, Z, E, L, Y, member_in_gg(Y, L))
U3_gggg(X, Z, E, L, Y, member_out_gg(Y, L)) → U4_gggg(X, Z, E, L, Y, delete_in_gga(Y, L, V1))
delete_in_gga(X, .(X, Y), Y) → delete_out_gga(X, .(X, Y), Y)
delete_in_gga(X, .(H, T1), .(H, T2)) → U8_gga(X, H, T1, T2, delete_in_gga(X, T1, T2))
U8_gga(X, H, T1, T2, delete_out_gga(X, T1, T2)) → delete_out_gga(X, .(H, T1), .(H, T2))
U4_gggg(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → U5_gggg(X, Z, E, L, reach_in_gggg(Y, Z, E, V1))
U5_gggg(X, Z, E, L, reach_out_gggg(Y, Z, E, V1)) → reach_out_gggg(X, Z, E, L)

(54) UsableRulesProof (EQUIVALENT transformation)

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

(55) Obligation:

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

MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)

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

(56) PiDPToQDPProof (EQUIVALENT transformation)

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

(57) Obligation:

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

MEMBER_IN_GG(X, .(H, L)) → MEMBER_IN_GG(X, L)

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

(58) 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, .(H, L)) → MEMBER_IN_GG(X, L)
The graph contains the following edges 1 >= 1, 2 > 2

(59) TRUE

(60) Obligation:

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

REACH_IN_GGGG(X, Z, E, L) → U2_GGGG(X, Z, E, L, member1_in_ag(.(X, .(Y, [])), E))
U2_GGGG(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → U3_GGGG(X, Z, E, L, Y, member_in_gg(Y, L))
U3_GGGG(X, Z, E, L, Y, member_out_gg(Y, L)) → U4_GGGG(X, Z, E, L, Y, delete_in_gga(Y, L, V1))
U4_GGGG(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → REACH_IN_GGGG(Y, Z, E, V1)

The TRS R consists of the following rules:

reach_in_gggg(X, Y, E, L) → U1_gggg(X, Y, E, L, member_in_gg(.(X, .(Y, [])), E))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U1_gggg(X, Y, E, L, member_out_gg(.(X, .(Y, [])), E)) → reach_out_gggg(X, Y, E, L)
reach_in_gggg(X, Z, E, L) → U2_gggg(X, Z, E, L, member1_in_ag(.(X, .(Y, [])), E))
member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U7_ag(X, H, L, member1_in_ag(X, L))
U7_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U2_gggg(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → U3_gggg(X, Z, E, L, Y, member_in_gg(Y, L))
U3_gggg(X, Z, E, L, Y, member_out_gg(Y, L)) → U4_gggg(X, Z, E, L, Y, delete_in_gga(Y, L, V1))
delete_in_gga(X, .(X, Y), Y) → delete_out_gga(X, .(X, Y), Y)
delete_in_gga(X, .(H, T1), .(H, T2)) → U8_gga(X, H, T1, T2, delete_in_gga(X, T1, T2))
U8_gga(X, H, T1, T2, delete_out_gga(X, T1, T2)) → delete_out_gga(X, .(H, T1), .(H, T2))
U4_gggg(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → U5_gggg(X, Z, E, L, reach_in_gggg(Y, Z, E, V1))
U5_gggg(X, Z, E, L, reach_out_gggg(Y, Z, E, V1)) → reach_out_gggg(X, Z, E, L)

The argument filtering Pi contains the following mapping:
reach_in_gggg(x1, x2, x3, x4) = reach_in_gggg(x1, x2, x3, x4)
U1_gggg(x1, x2, x3, x4, x5) = U1_gggg(x1, x2, x3, x4, x5)
member_in_gg(x1, x2) = member_in_gg(x1, x2)
.(x1, x2) = .(x1, x2)
member_out_gg(x1, x2) = member_out_gg(x1, x2)
U6_gg(x1, x2, x3, x4) = U6_gg(x1, x2, x3, x4)
[] = []
reach_out_gggg(x1, x2, x3, x4) = reach_out_gggg(x1, x2, x3, x4)
U2_gggg(x1, x2, x3, x4, x5) = U2_gggg(x1, x2, x3, x4, x5)
member1_in_ag(x1, x2) = member1_in_ag(x2)
member1_out_ag(x1, x2) = member1_out_ag(x1, x2)
U7_ag(x1, x2, x3, x4) = U7_ag(x2, x3, x4)
U3_gggg(x1, x2, x3, x4, x5, x6) = U3_gggg(x1, x2, x3, x4, x5, x6)
U4_gggg(x1, x2, x3, x4, x5, x6) = U4_gggg(x1, x2, x3, x4, x5, x6)
delete_in_gga(x1, x2, x3) = delete_in_gga(x1, x2)
delete_out_gga(x1, x2, x3) = delete_out_gga(x1, x2, x3)
U8_gga(x1, x2, x3, x4, x5) = U8_gga(x1, x2, x3, x5)
U5_gggg(x1, x2, x3, x4, x5) = U5_gggg(x1, x2, x3, x4, x5)
REACH_IN_GGGG(x1, x2, x3, x4) = REACH_IN_GGGG(x1, x2, x3, x4)
U2_GGGG(x1, x2, x3, x4, x5) = U2_GGGG(x1, x2, x3, x4, x5)
U3_GGGG(x1, x2, x3, x4, x5, x6) = U3_GGGG(x1, x2, x3, x4, x5, x6)
U4_GGGG(x1, x2, x3, x4, x5, x6) = U4_GGGG(x1, x2, x3, x4, x5, x6)

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

(61) UsableRulesProof (EQUIVALENT transformation)

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

(62) Obligation:

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

REACH_IN_GGGG(X, Z, E, L) → U2_GGGG(X, Z, E, L, member1_in_ag(.(X, .(Y, [])), E))
U2_GGGG(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → U3_GGGG(X, Z, E, L, Y, member_in_gg(Y, L))
U3_GGGG(X, Z, E, L, Y, member_out_gg(Y, L)) → U4_GGGG(X, Z, E, L, Y, delete_in_gga(Y, L, V1))
U4_GGGG(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → REACH_IN_GGGG(Y, Z, E, V1)

The TRS R consists of the following rules:

member1_in_ag(H, .(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(X, .(H, L)) → U7_ag(X, H, L, member1_in_ag(X, L))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
delete_in_gga(X, .(X, Y), Y) → delete_out_gga(X, .(X, Y), Y)
delete_in_gga(X, .(H, T1), .(H, T2)) → U8_gga(X, H, T1, T2, delete_in_gga(X, T1, T2))
U7_ag(X, H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U8_gga(X, H, T1, T2, delete_out_gga(X, T1, T2)) → delete_out_gga(X, .(H, T1), .(H, T2))

The argument filtering Pi contains the following mapping:
member_in_gg(x1, x2) = member_in_gg(x1, x2)
.(x1, x2) = .(x1, x2)
member_out_gg(x1, x2) = member_out_gg(x1, x2)
U6_gg(x1, x2, x3, x4) = U6_gg(x1, x2, x3, x4)
[] = []
member1_in_ag(x1, x2) = member1_in_ag(x2)
member1_out_ag(x1, x2) = member1_out_ag(x1, x2)
U7_ag(x1, x2, x3, x4) = U7_ag(x2, x3, x4)
delete_in_gga(x1, x2, x3) = delete_in_gga(x1, x2)
delete_out_gga(x1, x2, x3) = delete_out_gga(x1, x2, x3)
U8_gga(x1, x2, x3, x4, x5) = U8_gga(x1, x2, x3, x5)
REACH_IN_GGGG(x1, x2, x3, x4) = REACH_IN_GGGG(x1, x2, x3, x4)
U2_GGGG(x1, x2, x3, x4, x5) = U2_GGGG(x1, x2, x3, x4, x5)
U3_GGGG(x1, x2, x3, x4, x5, x6) = U3_GGGG(x1, x2, x3, x4, x5, x6)
U4_GGGG(x1, x2, x3, x4, x5, x6) = U4_GGGG(x1, x2, x3, x4, x5, x6)

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

(63) PiDPToQDPProof (SOUND transformation)

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

(64) Obligation:

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

REACH_IN_GGGG(X, Z, E, L) → U2_GGGG(X, Z, E, L, member1_in_ag(E))
U2_GGGG(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → U3_GGGG(X, Z, E, L, Y, member_in_gg(Y, L))
U3_GGGG(X, Z, E, L, Y, member_out_gg(Y, L)) → U4_GGGG(X, Z, E, L, Y, delete_in_gga(Y, L))
U4_GGGG(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → REACH_IN_GGGG(Y, Z, E, V1)

The TRS R consists of the following rules:

member1_in_ag(.(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(.(H, L)) → U7_ag(H, L, member1_in_ag(L))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
delete_in_gga(X, .(X, Y)) → delete_out_gga(X, .(X, Y), Y)
delete_in_gga(X, .(H, T1)) → U8_gga(X, H, T1, delete_in_gga(X, T1))
U7_ag(H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U8_gga(X, H, T1, delete_out_gga(X, T1, T2)) → delete_out_gga(X, .(H, T1), .(H, T2))

The set Q consists of the following terms:

member1_in_ag(x0)
member_in_gg(x0, x1)
delete_in_gga(x0, x1)
U7_ag(x0, x1, x2)
U6_gg(x0, x1, x2, x3)
U8_gga(x0, x1, x2, x3)

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

(65) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].

The following pairs can be oriented strictly and are deleted.

U4_GGGG(X, Z, E, L, Y, delete_out_gga(Y, L, V1)) → REACH_IN_GGGG(Y, Z, E, V1)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = 1 + x₂
POL(REACH_IN_GGGG(x₁, x₂, x₃, x₄)) = x₄
POL(U2_GGGG(x₁, x₂, x₃, x₄, x₅)) = x₄
POL(U3_GGGG(x₁, x₂, x₃, x₄, x₅, x₆)) = x₄
POL(U4_GGGG(x₁, x₂, x₃, x₄, x₅, x₆)) = x₆
POL(U6_gg(x₁, x₂, x₃, x₄)) = 0
POL(U7_ag(x₁, x₂, x₃)) = 0
POL(U8_gga(x₁, x₂, x₃, x₄)) = 1 + x₄
POL([]) = 0
POL(delete_in_gga(x₁, x₂)) = x₂
POL(delete_out_gga(x₁, x₂, x₃)) = 1 + x₃
POL(member1_in_ag(x₁)) = 0
POL(member1_out_ag(x₁, x₂)) = 0
POL(member_in_gg(x₁, x₂)) = 0
POL(member_out_gg(x₁, x₂)) = 0

The following usable rules [FROCOS05] were oriented:

delete_in_gga(X, .(X, Y)) → delete_out_gga(X, .(X, Y), Y)
delete_in_gga(X, .(H, T1)) → U8_gga(X, H, T1, delete_in_gga(X, T1))
U8_gga(X, H, T1, delete_out_gga(X, T1, T2)) → delete_out_gga(X, .(H, T1), .(H, T2))

(66) Obligation:

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

REACH_IN_GGGG(X, Z, E, L) → U2_GGGG(X, Z, E, L, member1_in_ag(E))
U2_GGGG(X, Z, E, L, member1_out_ag(.(X, .(Y, [])), E)) → U3_GGGG(X, Z, E, L, Y, member_in_gg(Y, L))
U3_GGGG(X, Z, E, L, Y, member_out_gg(Y, L)) → U4_GGGG(X, Z, E, L, Y, delete_in_gga(Y, L))

The TRS R consists of the following rules:

member1_in_ag(.(H, L)) → member1_out_ag(H, .(H, L))
member1_in_ag(.(H, L)) → U7_ag(H, L, member1_in_ag(L))
member_in_gg(H, .(H, L)) → member_out_gg(H, .(H, L))
member_in_gg(X, .(H, L)) → U6_gg(X, H, L, member_in_gg(X, L))
delete_in_gga(X, .(X, Y)) → delete_out_gga(X, .(X, Y), Y)
delete_in_gga(X, .(H, T1)) → U8_gga(X, H, T1, delete_in_gga(X, T1))
U7_ag(H, L, member1_out_ag(X, L)) → member1_out_ag(X, .(H, L))
U6_gg(X, H, L, member_out_gg(X, L)) → member_out_gg(X, .(H, L))
U8_gga(X, H, T1, delete_out_gga(X, T1, T2)) → delete_out_gga(X, .(H, T1), .(H, T2))

The set Q consists of the following terms:

member1_in_ag(x0)
member_in_gg(x0, x1)
delete_in_gga(x0, x1)
U7_ag(x0, x1, x2)
U6_gg(x0, x1, x2, x3)
U8_gga(x0, x1, x2, x3)

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

(67) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 3 less nodes.

(0) Obligation:

(1) PrologToPiTRSProof (SOUND transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) PiDPToQDPProof (SOUND transformation)

(11) Obligation:

(12) QDPSizeChangeProof (EQUIVALENT transformation)

(13) TRUE

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) PiDPToQDPProof (SOUND transformation)

(18) Obligation:

(19) QDPSizeChangeProof (EQUIVALENT transformation)

(20) TRUE

(21) Obligation:

(22) UsableRulesProof (EQUIVALENT transformation)

(23) Obligation:

(24) PiDPToQDPProof (EQUIVALENT transformation)

(25) Obligation:

(26) QDPSizeChangeProof (EQUIVALENT transformation)

(27) TRUE

(28) Obligation:

(29) UsableRulesProof (EQUIVALENT transformation)

(30) Obligation:

(31) PiDPToQDPProof (SOUND transformation)

(32) Obligation:

(33) PrologToPiTRSProof (SOUND transformation)

(34) Obligation:

(35) DependencyPairsProof (EQUIVALENT transformation)

(36) Obligation:

(37) DependencyGraphProof (EQUIVALENT transformation)

(38) Complex Obligation (AND)

(39) Obligation:

(40) UsableRulesProof (EQUIVALENT transformation)

(41) Obligation:

(42) PiDPToQDPProof (SOUND transformation)

(43) Obligation:

(44) QDPSizeChangeProof (EQUIVALENT transformation)

(45) TRUE

(46) Obligation:

(47) UsableRulesProof (EQUIVALENT transformation)

(48) Obligation:

(49) PiDPToQDPProof (SOUND transformation)

(50) Obligation:

(51) QDPSizeChangeProof (EQUIVALENT transformation)

(52) TRUE

(53) Obligation:

(54) UsableRulesProof (EQUIVALENT transformation)

(55) Obligation:

(56) PiDPToQDPProof (EQUIVALENT transformation)

(57) Obligation:

(58) QDPSizeChangeProof (EQUIVALENT transformation)

(59) TRUE

(60) Obligation:

(61) UsableRulesProof (EQUIVALENT transformation)

(62) Obligation:

(63) PiDPToQDPProof (SOUND transformation)

(64) Obligation:

(65) QDPOrderProof (EQUIVALENT transformation)

(66) Obligation:

(67) DependencyGraphProof (EQUIVALENT transformation)

(68) TRUE