(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) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

member12(T68, T69, .(.(T68, .(T69, [])), T70)).
member12(T79, T80, .(T81, T82)) :- member12(T79, T80, T82).
member124(T122, X119, .(.(T122, .(X119, [])), T123)).
member124(T130, X133, .(T131, T132)) :- member124(T130, X133, T132).
member34(T153, .(T153, T154)).
member34(T161, .(T162, T163)) :- member34(T161, T163).
delete44(T185, .(T185, T186), T186).
delete44(T193, .(T194, T195), .(T194, X213)) :- delete44(T193, T195, X213).
reach1(T27, T28, .(.(T27, .(T28, [])), T29), T14).
reach1(T46, T47, .(T48, T49), T14) :- member12(T46, T47, T49).
reach1(T101, T102, T103, T104) :- member124(T101, X91, T103).
reach1(T101, T102, T103, T104) :- ','(member124(T101, T109, T103), member34(T109, T104)).
reach1(T101, T102, T103, T104) :- ','(member124(T101, T109, T103), ','(member34(T109, T104), delete44(T109, T104, X92))).
reach1(T101, T102, T103, T104) :- ','(member124(T101, T109, T103), ','(member34(T109, T104), ','(delete44(T109, T104, T172), reach1(T109, T102, T103, T172)))).

Queries:

reach1(g,g,g,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:
reach1_in: (b,b,b,b)
member12_in: (b,b,b)
member124_in: (b,f,b)
member34_in: (b,b)
delete44_in: (b,b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

reach1_in_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14) → reach1_out_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14)
reach1_in_gggg(T46, T47, .(T48, T49), T14) → U5_gggg(T46, T47, T48, T49, T14, member12_in_ggg(T46, T47, T49))
member12_in_ggg(T68, T69, .(.(T68, .(T69, [])), T70)) → member12_out_ggg(T68, T69, .(.(T68, .(T69, [])), T70))
member12_in_ggg(T79, T80, .(T81, T82)) → U1_ggg(T79, T80, T81, T82, member12_in_ggg(T79, T80, T82))
U1_ggg(T79, T80, T81, T82, member12_out_ggg(T79, T80, T82)) → member12_out_ggg(T79, T80, .(T81, T82))
U5_gggg(T46, T47, T48, T49, T14, member12_out_ggg(T46, T47, T49)) → reach1_out_gggg(T46, T47, .(T48, T49), T14)
reach1_in_gggg(T101, T102, T103, T104) → U6_gggg(T101, T102, T103, T104, member124_in_gag(T101, X91, T103))
member124_in_gag(T122, X119, .(.(T122, .(X119, [])), T123)) → member124_out_gag(T122, X119, .(.(T122, .(X119, [])), T123))
member124_in_gag(T130, X133, .(T131, T132)) → U2_gag(T130, X133, T131, T132, member124_in_gag(T130, X133, T132))
U2_gag(T130, X133, T131, T132, member124_out_gag(T130, X133, T132)) → member124_out_gag(T130, X133, .(T131, T132))
U6_gggg(T101, T102, T103, T104, member124_out_gag(T101, X91, T103)) → reach1_out_gggg(T101, T102, T103, T104)
reach1_in_gggg(T101, T102, T103, T104) → U7_gggg(T101, T102, T103, T104, member124_in_gag(T101, T109, T103))
U7_gggg(T101, T102, T103, T104, member124_out_gag(T101, T109, T103)) → U8_gggg(T101, T102, T103, T104, T109, member34_in_gg(T109, T104))
member34_in_gg(T153, .(T153, T154)) → member34_out_gg(T153, .(T153, T154))
member34_in_gg(T161, .(T162, T163)) → U3_gg(T161, T162, T163, member34_in_gg(T161, T163))
U3_gg(T161, T162, T163, member34_out_gg(T161, T163)) → member34_out_gg(T161, .(T162, T163))
U8_gggg(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → reach1_out_gggg(T101, T102, T103, T104)
U8_gggg(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → U9_gggg(T101, T102, T103, T104, delete44_in_gga(T109, T104, X92))
delete44_in_gga(T185, .(T185, T186), T186) → delete44_out_gga(T185, .(T185, T186), T186)
delete44_in_gga(T193, .(T194, T195), .(T194, X213)) → U4_gga(T193, T194, T195, X213, delete44_in_gga(T193, T195, X213))
U4_gga(T193, T194, T195, X213, delete44_out_gga(T193, T195, X213)) → delete44_out_gga(T193, .(T194, T195), .(T194, X213))
U9_gggg(T101, T102, T103, T104, delete44_out_gga(T109, T104, X92)) → reach1_out_gggg(T101, T102, T103, T104)
U8_gggg(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → U10_gggg(T101, T102, T103, T104, T109, delete44_in_gga(T109, T104, T172))
U10_gggg(T101, T102, T103, T104, T109, delete44_out_gga(T109, T104, T172)) → U11_gggg(T101, T102, T103, T104, reach1_in_gggg(T109, T102, T103, T172))
U11_gggg(T101, T102, T103, T104, reach1_out_gggg(T109, T102, T103, T172)) → reach1_out_gggg(T101, T102, T103, T104)

The argument filtering Pi contains the following mapping:
reach1_in_gggg(x1, x2, x3, x4)  =  reach1_in_gggg(x1, x2, x3, x4)
.(x1, x2)  =  .(x1, x2)
[]  =  []
reach1_out_gggg(x1, x2, x3, x4)  =  reach1_out_gggg
U5_gggg(x1, x2, x3, x4, x5, x6)  =  U5_gggg(x6)
member12_in_ggg(x1, x2, x3)  =  member12_in_ggg(x1, x2, x3)
member12_out_ggg(x1, x2, x3)  =  member12_out_ggg
U1_ggg(x1, x2, x3, x4, x5)  =  U1_ggg(x5)
U6_gggg(x1, x2, x3, x4, x5)  =  U6_gggg(x5)
member124_in_gag(x1, x2, x3)  =  member124_in_gag(x1, x3)
member124_out_gag(x1, x2, x3)  =  member124_out_gag(x2)
U2_gag(x1, x2, x3, x4, x5)  =  U2_gag(x5)
U7_gggg(x1, x2, x3, x4, x5)  =  U7_gggg(x2, x3, x4, x5)
U8_gggg(x1, x2, x3, x4, x5, x6)  =  U8_gggg(x2, x3, x4, x5, x6)
member34_in_gg(x1, x2)  =  member34_in_gg(x1, x2)
member34_out_gg(x1, x2)  =  member34_out_gg
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
U9_gggg(x1, x2, x3, x4, x5)  =  U9_gggg(x5)
delete44_in_gga(x1, x2, x3)  =  delete44_in_gga(x1, x2)
delete44_out_gga(x1, x2, x3)  =  delete44_out_gga(x3)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x2, x5)
U10_gggg(x1, x2, x3, x4, x5, x6)  =  U10_gggg(x2, x3, x5, x6)
U11_gggg(x1, x2, x3, x4, x5)  =  U11_gggg(x5)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

reach1_in_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14) → reach1_out_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14)
reach1_in_gggg(T46, T47, .(T48, T49), T14) → U5_gggg(T46, T47, T48, T49, T14, member12_in_ggg(T46, T47, T49))
member12_in_ggg(T68, T69, .(.(T68, .(T69, [])), T70)) → member12_out_ggg(T68, T69, .(.(T68, .(T69, [])), T70))
member12_in_ggg(T79, T80, .(T81, T82)) → U1_ggg(T79, T80, T81, T82, member12_in_ggg(T79, T80, T82))
U1_ggg(T79, T80, T81, T82, member12_out_ggg(T79, T80, T82)) → member12_out_ggg(T79, T80, .(T81, T82))
U5_gggg(T46, T47, T48, T49, T14, member12_out_ggg(T46, T47, T49)) → reach1_out_gggg(T46, T47, .(T48, T49), T14)
reach1_in_gggg(T101, T102, T103, T104) → U6_gggg(T101, T102, T103, T104, member124_in_gag(T101, X91, T103))
member124_in_gag(T122, X119, .(.(T122, .(X119, [])), T123)) → member124_out_gag(T122, X119, .(.(T122, .(X119, [])), T123))
member124_in_gag(T130, X133, .(T131, T132)) → U2_gag(T130, X133, T131, T132, member124_in_gag(T130, X133, T132))
U2_gag(T130, X133, T131, T132, member124_out_gag(T130, X133, T132)) → member124_out_gag(T130, X133, .(T131, T132))
U6_gggg(T101, T102, T103, T104, member124_out_gag(T101, X91, T103)) → reach1_out_gggg(T101, T102, T103, T104)
reach1_in_gggg(T101, T102, T103, T104) → U7_gggg(T101, T102, T103, T104, member124_in_gag(T101, T109, T103))
U7_gggg(T101, T102, T103, T104, member124_out_gag(T101, T109, T103)) → U8_gggg(T101, T102, T103, T104, T109, member34_in_gg(T109, T104))
member34_in_gg(T153, .(T153, T154)) → member34_out_gg(T153, .(T153, T154))
member34_in_gg(T161, .(T162, T163)) → U3_gg(T161, T162, T163, member34_in_gg(T161, T163))
U3_gg(T161, T162, T163, member34_out_gg(T161, T163)) → member34_out_gg(T161, .(T162, T163))
U8_gggg(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → reach1_out_gggg(T101, T102, T103, T104)
U8_gggg(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → U9_gggg(T101, T102, T103, T104, delete44_in_gga(T109, T104, X92))
delete44_in_gga(T185, .(T185, T186), T186) → delete44_out_gga(T185, .(T185, T186), T186)
delete44_in_gga(T193, .(T194, T195), .(T194, X213)) → U4_gga(T193, T194, T195, X213, delete44_in_gga(T193, T195, X213))
U4_gga(T193, T194, T195, X213, delete44_out_gga(T193, T195, X213)) → delete44_out_gga(T193, .(T194, T195), .(T194, X213))
U9_gggg(T101, T102, T103, T104, delete44_out_gga(T109, T104, X92)) → reach1_out_gggg(T101, T102, T103, T104)
U8_gggg(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → U10_gggg(T101, T102, T103, T104, T109, delete44_in_gga(T109, T104, T172))
U10_gggg(T101, T102, T103, T104, T109, delete44_out_gga(T109, T104, T172)) → U11_gggg(T101, T102, T103, T104, reach1_in_gggg(T109, T102, T103, T172))
U11_gggg(T101, T102, T103, T104, reach1_out_gggg(T109, T102, T103, T172)) → reach1_out_gggg(T101, T102, T103, T104)

The argument filtering Pi contains the following mapping:
reach1_in_gggg(x1, x2, x3, x4)  =  reach1_in_gggg(x1, x2, x3, x4)
.(x1, x2)  =  .(x1, x2)
[]  =  []
reach1_out_gggg(x1, x2, x3, x4)  =  reach1_out_gggg
U5_gggg(x1, x2, x3, x4, x5, x6)  =  U5_gggg(x6)
member12_in_ggg(x1, x2, x3)  =  member12_in_ggg(x1, x2, x3)
member12_out_ggg(x1, x2, x3)  =  member12_out_ggg
U1_ggg(x1, x2, x3, x4, x5)  =  U1_ggg(x5)
U6_gggg(x1, x2, x3, x4, x5)  =  U6_gggg(x5)
member124_in_gag(x1, x2, x3)  =  member124_in_gag(x1, x3)
member124_out_gag(x1, x2, x3)  =  member124_out_gag(x2)
U2_gag(x1, x2, x3, x4, x5)  =  U2_gag(x5)
U7_gggg(x1, x2, x3, x4, x5)  =  U7_gggg(x2, x3, x4, x5)
U8_gggg(x1, x2, x3, x4, x5, x6)  =  U8_gggg(x2, x3, x4, x5, x6)
member34_in_gg(x1, x2)  =  member34_in_gg(x1, x2)
member34_out_gg(x1, x2)  =  member34_out_gg
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
U9_gggg(x1, x2, x3, x4, x5)  =  U9_gggg(x5)
delete44_in_gga(x1, x2, x3)  =  delete44_in_gga(x1, x2)
delete44_out_gga(x1, x2, x3)  =  delete44_out_gga(x3)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x2, x5)
U10_gggg(x1, x2, x3, x4, x5, x6)  =  U10_gggg(x2, x3, x5, x6)
U11_gggg(x1, x2, x3, x4, x5)  =  U11_gggg(x5)

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

REACH1_IN_GGGG(T46, T47, .(T48, T49), T14) → U5_GGGG(T46, T47, T48, T49, T14, member12_in_ggg(T46, T47, T49))
REACH1_IN_GGGG(T46, T47, .(T48, T49), T14) → MEMBER12_IN_GGG(T46, T47, T49)
MEMBER12_IN_GGG(T79, T80, .(T81, T82)) → U1_GGG(T79, T80, T81, T82, member12_in_ggg(T79, T80, T82))
MEMBER12_IN_GGG(T79, T80, .(T81, T82)) → MEMBER12_IN_GGG(T79, T80, T82)
REACH1_IN_GGGG(T101, T102, T103, T104) → U6_GGGG(T101, T102, T103, T104, member124_in_gag(T101, X91, T103))
REACH1_IN_GGGG(T101, T102, T103, T104) → MEMBER124_IN_GAG(T101, X91, T103)
MEMBER124_IN_GAG(T130, X133, .(T131, T132)) → U2_GAG(T130, X133, T131, T132, member124_in_gag(T130, X133, T132))
MEMBER124_IN_GAG(T130, X133, .(T131, T132)) → MEMBER124_IN_GAG(T130, X133, T132)
REACH1_IN_GGGG(T101, T102, T103, T104) → U7_GGGG(T101, T102, T103, T104, member124_in_gag(T101, T109, T103))
U7_GGGG(T101, T102, T103, T104, member124_out_gag(T101, T109, T103)) → U8_GGGG(T101, T102, T103, T104, T109, member34_in_gg(T109, T104))
U7_GGGG(T101, T102, T103, T104, member124_out_gag(T101, T109, T103)) → MEMBER34_IN_GG(T109, T104)
MEMBER34_IN_GG(T161, .(T162, T163)) → U3_GG(T161, T162, T163, member34_in_gg(T161, T163))
MEMBER34_IN_GG(T161, .(T162, T163)) → MEMBER34_IN_GG(T161, T163)
U8_GGGG(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → U9_GGGG(T101, T102, T103, T104, delete44_in_gga(T109, T104, X92))
U8_GGGG(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → DELETE44_IN_GGA(T109, T104, X92)
DELETE44_IN_GGA(T193, .(T194, T195), .(T194, X213)) → U4_GGA(T193, T194, T195, X213, delete44_in_gga(T193, T195, X213))
DELETE44_IN_GGA(T193, .(T194, T195), .(T194, X213)) → DELETE44_IN_GGA(T193, T195, X213)
U8_GGGG(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → U10_GGGG(T101, T102, T103, T104, T109, delete44_in_gga(T109, T104, T172))
U10_GGGG(T101, T102, T103, T104, T109, delete44_out_gga(T109, T104, T172)) → U11_GGGG(T101, T102, T103, T104, reach1_in_gggg(T109, T102, T103, T172))
U10_GGGG(T101, T102, T103, T104, T109, delete44_out_gga(T109, T104, T172)) → REACH1_IN_GGGG(T109, T102, T103, T172)

The TRS R consists of the following rules:

reach1_in_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14) → reach1_out_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14)
reach1_in_gggg(T46, T47, .(T48, T49), T14) → U5_gggg(T46, T47, T48, T49, T14, member12_in_ggg(T46, T47, T49))
member12_in_ggg(T68, T69, .(.(T68, .(T69, [])), T70)) → member12_out_ggg(T68, T69, .(.(T68, .(T69, [])), T70))
member12_in_ggg(T79, T80, .(T81, T82)) → U1_ggg(T79, T80, T81, T82, member12_in_ggg(T79, T80, T82))
U1_ggg(T79, T80, T81, T82, member12_out_ggg(T79, T80, T82)) → member12_out_ggg(T79, T80, .(T81, T82))
U5_gggg(T46, T47, T48, T49, T14, member12_out_ggg(T46, T47, T49)) → reach1_out_gggg(T46, T47, .(T48, T49), T14)
reach1_in_gggg(T101, T102, T103, T104) → U6_gggg(T101, T102, T103, T104, member124_in_gag(T101, X91, T103))
member124_in_gag(T122, X119, .(.(T122, .(X119, [])), T123)) → member124_out_gag(T122, X119, .(.(T122, .(X119, [])), T123))
member124_in_gag(T130, X133, .(T131, T132)) → U2_gag(T130, X133, T131, T132, member124_in_gag(T130, X133, T132))
U2_gag(T130, X133, T131, T132, member124_out_gag(T130, X133, T132)) → member124_out_gag(T130, X133, .(T131, T132))
U6_gggg(T101, T102, T103, T104, member124_out_gag(T101, X91, T103)) → reach1_out_gggg(T101, T102, T103, T104)
reach1_in_gggg(T101, T102, T103, T104) → U7_gggg(T101, T102, T103, T104, member124_in_gag(T101, T109, T103))
U7_gggg(T101, T102, T103, T104, member124_out_gag(T101, T109, T103)) → U8_gggg(T101, T102, T103, T104, T109, member34_in_gg(T109, T104))
member34_in_gg(T153, .(T153, T154)) → member34_out_gg(T153, .(T153, T154))
member34_in_gg(T161, .(T162, T163)) → U3_gg(T161, T162, T163, member34_in_gg(T161, T163))
U3_gg(T161, T162, T163, member34_out_gg(T161, T163)) → member34_out_gg(T161, .(T162, T163))
U8_gggg(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → reach1_out_gggg(T101, T102, T103, T104)
U8_gggg(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → U9_gggg(T101, T102, T103, T104, delete44_in_gga(T109, T104, X92))
delete44_in_gga(T185, .(T185, T186), T186) → delete44_out_gga(T185, .(T185, T186), T186)
delete44_in_gga(T193, .(T194, T195), .(T194, X213)) → U4_gga(T193, T194, T195, X213, delete44_in_gga(T193, T195, X213))
U4_gga(T193, T194, T195, X213, delete44_out_gga(T193, T195, X213)) → delete44_out_gga(T193, .(T194, T195), .(T194, X213))
U9_gggg(T101, T102, T103, T104, delete44_out_gga(T109, T104, X92)) → reach1_out_gggg(T101, T102, T103, T104)
U8_gggg(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → U10_gggg(T101, T102, T103, T104, T109, delete44_in_gga(T109, T104, T172))
U10_gggg(T101, T102, T103, T104, T109, delete44_out_gga(T109, T104, T172)) → U11_gggg(T101, T102, T103, T104, reach1_in_gggg(T109, T102, T103, T172))
U11_gggg(T101, T102, T103, T104, reach1_out_gggg(T109, T102, T103, T172)) → reach1_out_gggg(T101, T102, T103, T104)

The argument filtering Pi contains the following mapping:
reach1_in_gggg(x1, x2, x3, x4)  =  reach1_in_gggg(x1, x2, x3, x4)
.(x1, x2)  =  .(x1, x2)
[]  =  []
reach1_out_gggg(x1, x2, x3, x4)  =  reach1_out_gggg
U5_gggg(x1, x2, x3, x4, x5, x6)  =  U5_gggg(x6)
member12_in_ggg(x1, x2, x3)  =  member12_in_ggg(x1, x2, x3)
member12_out_ggg(x1, x2, x3)  =  member12_out_ggg
U1_ggg(x1, x2, x3, x4, x5)  =  U1_ggg(x5)
U6_gggg(x1, x2, x3, x4, x5)  =  U6_gggg(x5)
member124_in_gag(x1, x2, x3)  =  member124_in_gag(x1, x3)
member124_out_gag(x1, x2, x3)  =  member124_out_gag(x2)
U2_gag(x1, x2, x3, x4, x5)  =  U2_gag(x5)
U7_gggg(x1, x2, x3, x4, x5)  =  U7_gggg(x2, x3, x4, x5)
U8_gggg(x1, x2, x3, x4, x5, x6)  =  U8_gggg(x2, x3, x4, x5, x6)
member34_in_gg(x1, x2)  =  member34_in_gg(x1, x2)
member34_out_gg(x1, x2)  =  member34_out_gg
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
U9_gggg(x1, x2, x3, x4, x5)  =  U9_gggg(x5)
delete44_in_gga(x1, x2, x3)  =  delete44_in_gga(x1, x2)
delete44_out_gga(x1, x2, x3)  =  delete44_out_gga(x3)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x2, x5)
U10_gggg(x1, x2, x3, x4, x5, x6)  =  U10_gggg(x2, x3, x5, x6)
U11_gggg(x1, x2, x3, x4, x5)  =  U11_gggg(x5)
REACH1_IN_GGGG(x1, x2, x3, x4)  =  REACH1_IN_GGGG(x1, x2, x3, x4)
U5_GGGG(x1, x2, x3, x4, x5, x6)  =  U5_GGGG(x6)
MEMBER12_IN_GGG(x1, x2, x3)  =  MEMBER12_IN_GGG(x1, x2, x3)
U1_GGG(x1, x2, x3, x4, x5)  =  U1_GGG(x5)
U6_GGGG(x1, x2, x3, x4, x5)  =  U6_GGGG(x5)
MEMBER124_IN_GAG(x1, x2, x3)  =  MEMBER124_IN_GAG(x1, x3)
U2_GAG(x1, x2, x3, x4, x5)  =  U2_GAG(x5)
U7_GGGG(x1, x2, x3, x4, x5)  =  U7_GGGG(x2, x3, x4, x5)
U8_GGGG(x1, x2, x3, x4, x5, x6)  =  U8_GGGG(x2, x3, x4, x5, x6)
MEMBER34_IN_GG(x1, x2)  =  MEMBER34_IN_GG(x1, x2)
U3_GG(x1, x2, x3, x4)  =  U3_GG(x4)
U9_GGGG(x1, x2, x3, x4, x5)  =  U9_GGGG(x5)
DELETE44_IN_GGA(x1, x2, x3)  =  DELETE44_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4, x5)  =  U4_GGA(x2, x5)
U10_GGGG(x1, x2, x3, x4, x5, x6)  =  U10_GGGG(x2, x3, x5, x6)
U11_GGGG(x1, x2, x3, x4, x5)  =  U11_GGGG(x5)

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

(6) Obligation:

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

REACH1_IN_GGGG(T46, T47, .(T48, T49), T14) → U5_GGGG(T46, T47, T48, T49, T14, member12_in_ggg(T46, T47, T49))
REACH1_IN_GGGG(T46, T47, .(T48, T49), T14) → MEMBER12_IN_GGG(T46, T47, T49)
MEMBER12_IN_GGG(T79, T80, .(T81, T82)) → U1_GGG(T79, T80, T81, T82, member12_in_ggg(T79, T80, T82))
MEMBER12_IN_GGG(T79, T80, .(T81, T82)) → MEMBER12_IN_GGG(T79, T80, T82)
REACH1_IN_GGGG(T101, T102, T103, T104) → U6_GGGG(T101, T102, T103, T104, member124_in_gag(T101, X91, T103))
REACH1_IN_GGGG(T101, T102, T103, T104) → MEMBER124_IN_GAG(T101, X91, T103)
MEMBER124_IN_GAG(T130, X133, .(T131, T132)) → U2_GAG(T130, X133, T131, T132, member124_in_gag(T130, X133, T132))
MEMBER124_IN_GAG(T130, X133, .(T131, T132)) → MEMBER124_IN_GAG(T130, X133, T132)
REACH1_IN_GGGG(T101, T102, T103, T104) → U7_GGGG(T101, T102, T103, T104, member124_in_gag(T101, T109, T103))
U7_GGGG(T101, T102, T103, T104, member124_out_gag(T101, T109, T103)) → U8_GGGG(T101, T102, T103, T104, T109, member34_in_gg(T109, T104))
U7_GGGG(T101, T102, T103, T104, member124_out_gag(T101, T109, T103)) → MEMBER34_IN_GG(T109, T104)
MEMBER34_IN_GG(T161, .(T162, T163)) → U3_GG(T161, T162, T163, member34_in_gg(T161, T163))
MEMBER34_IN_GG(T161, .(T162, T163)) → MEMBER34_IN_GG(T161, T163)
U8_GGGG(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → U9_GGGG(T101, T102, T103, T104, delete44_in_gga(T109, T104, X92))
U8_GGGG(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → DELETE44_IN_GGA(T109, T104, X92)
DELETE44_IN_GGA(T193, .(T194, T195), .(T194, X213)) → U4_GGA(T193, T194, T195, X213, delete44_in_gga(T193, T195, X213))
DELETE44_IN_GGA(T193, .(T194, T195), .(T194, X213)) → DELETE44_IN_GGA(T193, T195, X213)
U8_GGGG(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → U10_GGGG(T101, T102, T103, T104, T109, delete44_in_gga(T109, T104, T172))
U10_GGGG(T101, T102, T103, T104, T109, delete44_out_gga(T109, T104, T172)) → U11_GGGG(T101, T102, T103, T104, reach1_in_gggg(T109, T102, T103, T172))
U10_GGGG(T101, T102, T103, T104, T109, delete44_out_gga(T109, T104, T172)) → REACH1_IN_GGGG(T109, T102, T103, T172)

The TRS R consists of the following rules:

reach1_in_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14) → reach1_out_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14)
reach1_in_gggg(T46, T47, .(T48, T49), T14) → U5_gggg(T46, T47, T48, T49, T14, member12_in_ggg(T46, T47, T49))
member12_in_ggg(T68, T69, .(.(T68, .(T69, [])), T70)) → member12_out_ggg(T68, T69, .(.(T68, .(T69, [])), T70))
member12_in_ggg(T79, T80, .(T81, T82)) → U1_ggg(T79, T80, T81, T82, member12_in_ggg(T79, T80, T82))
U1_ggg(T79, T80, T81, T82, member12_out_ggg(T79, T80, T82)) → member12_out_ggg(T79, T80, .(T81, T82))
U5_gggg(T46, T47, T48, T49, T14, member12_out_ggg(T46, T47, T49)) → reach1_out_gggg(T46, T47, .(T48, T49), T14)
reach1_in_gggg(T101, T102, T103, T104) → U6_gggg(T101, T102, T103, T104, member124_in_gag(T101, X91, T103))
member124_in_gag(T122, X119, .(.(T122, .(X119, [])), T123)) → member124_out_gag(T122, X119, .(.(T122, .(X119, [])), T123))
member124_in_gag(T130, X133, .(T131, T132)) → U2_gag(T130, X133, T131, T132, member124_in_gag(T130, X133, T132))
U2_gag(T130, X133, T131, T132, member124_out_gag(T130, X133, T132)) → member124_out_gag(T130, X133, .(T131, T132))
U6_gggg(T101, T102, T103, T104, member124_out_gag(T101, X91, T103)) → reach1_out_gggg(T101, T102, T103, T104)
reach1_in_gggg(T101, T102, T103, T104) → U7_gggg(T101, T102, T103, T104, member124_in_gag(T101, T109, T103))
U7_gggg(T101, T102, T103, T104, member124_out_gag(T101, T109, T103)) → U8_gggg(T101, T102, T103, T104, T109, member34_in_gg(T109, T104))
member34_in_gg(T153, .(T153, T154)) → member34_out_gg(T153, .(T153, T154))
member34_in_gg(T161, .(T162, T163)) → U3_gg(T161, T162, T163, member34_in_gg(T161, T163))
U3_gg(T161, T162, T163, member34_out_gg(T161, T163)) → member34_out_gg(T161, .(T162, T163))
U8_gggg(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → reach1_out_gggg(T101, T102, T103, T104)
U8_gggg(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → U9_gggg(T101, T102, T103, T104, delete44_in_gga(T109, T104, X92))
delete44_in_gga(T185, .(T185, T186), T186) → delete44_out_gga(T185, .(T185, T186), T186)
delete44_in_gga(T193, .(T194, T195), .(T194, X213)) → U4_gga(T193, T194, T195, X213, delete44_in_gga(T193, T195, X213))
U4_gga(T193, T194, T195, X213, delete44_out_gga(T193, T195, X213)) → delete44_out_gga(T193, .(T194, T195), .(T194, X213))
U9_gggg(T101, T102, T103, T104, delete44_out_gga(T109, T104, X92)) → reach1_out_gggg(T101, T102, T103, T104)
U8_gggg(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → U10_gggg(T101, T102, T103, T104, T109, delete44_in_gga(T109, T104, T172))
U10_gggg(T101, T102, T103, T104, T109, delete44_out_gga(T109, T104, T172)) → U11_gggg(T101, T102, T103, T104, reach1_in_gggg(T109, T102, T103, T172))
U11_gggg(T101, T102, T103, T104, reach1_out_gggg(T109, T102, T103, T172)) → reach1_out_gggg(T101, T102, T103, T104)

The argument filtering Pi contains the following mapping:
reach1_in_gggg(x1, x2, x3, x4)  =  reach1_in_gggg(x1, x2, x3, x4)
.(x1, x2)  =  .(x1, x2)
[]  =  []
reach1_out_gggg(x1, x2, x3, x4)  =  reach1_out_gggg
U5_gggg(x1, x2, x3, x4, x5, x6)  =  U5_gggg(x6)
member12_in_ggg(x1, x2, x3)  =  member12_in_ggg(x1, x2, x3)
member12_out_ggg(x1, x2, x3)  =  member12_out_ggg
U1_ggg(x1, x2, x3, x4, x5)  =  U1_ggg(x5)
U6_gggg(x1, x2, x3, x4, x5)  =  U6_gggg(x5)
member124_in_gag(x1, x2, x3)  =  member124_in_gag(x1, x3)
member124_out_gag(x1, x2, x3)  =  member124_out_gag(x2)
U2_gag(x1, x2, x3, x4, x5)  =  U2_gag(x5)
U7_gggg(x1, x2, x3, x4, x5)  =  U7_gggg(x2, x3, x4, x5)
U8_gggg(x1, x2, x3, x4, x5, x6)  =  U8_gggg(x2, x3, x4, x5, x6)
member34_in_gg(x1, x2)  =  member34_in_gg(x1, x2)
member34_out_gg(x1, x2)  =  member34_out_gg
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
U9_gggg(x1, x2, x3, x4, x5)  =  U9_gggg(x5)
delete44_in_gga(x1, x2, x3)  =  delete44_in_gga(x1, x2)
delete44_out_gga(x1, x2, x3)  =  delete44_out_gga(x3)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x2, x5)
U10_gggg(x1, x2, x3, x4, x5, x6)  =  U10_gggg(x2, x3, x5, x6)
U11_gggg(x1, x2, x3, x4, x5)  =  U11_gggg(x5)
REACH1_IN_GGGG(x1, x2, x3, x4)  =  REACH1_IN_GGGG(x1, x2, x3, x4)
U5_GGGG(x1, x2, x3, x4, x5, x6)  =  U5_GGGG(x6)
MEMBER12_IN_GGG(x1, x2, x3)  =  MEMBER12_IN_GGG(x1, x2, x3)
U1_GGG(x1, x2, x3, x4, x5)  =  U1_GGG(x5)
U6_GGGG(x1, x2, x3, x4, x5)  =  U6_GGGG(x5)
MEMBER124_IN_GAG(x1, x2, x3)  =  MEMBER124_IN_GAG(x1, x3)
U2_GAG(x1, x2, x3, x4, x5)  =  U2_GAG(x5)
U7_GGGG(x1, x2, x3, x4, x5)  =  U7_GGGG(x2, x3, x4, x5)
U8_GGGG(x1, x2, x3, x4, x5, x6)  =  U8_GGGG(x2, x3, x4, x5, x6)
MEMBER34_IN_GG(x1, x2)  =  MEMBER34_IN_GG(x1, x2)
U3_GG(x1, x2, x3, x4)  =  U3_GG(x4)
U9_GGGG(x1, x2, x3, x4, x5)  =  U9_GGGG(x5)
DELETE44_IN_GGA(x1, x2, x3)  =  DELETE44_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4, x5)  =  U4_GGA(x2, x5)
U10_GGGG(x1, x2, x3, x4, x5, x6)  =  U10_GGGG(x2, x3, x5, x6)
U11_GGGG(x1, x2, x3, x4, x5)  =  U11_GGGG(x5)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 5 SCCs with 12 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

DELETE44_IN_GGA(T193, .(T194, T195), .(T194, X213)) → DELETE44_IN_GGA(T193, T195, X213)

The TRS R consists of the following rules:

reach1_in_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14) → reach1_out_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14)
reach1_in_gggg(T46, T47, .(T48, T49), T14) → U5_gggg(T46, T47, T48, T49, T14, member12_in_ggg(T46, T47, T49))
member12_in_ggg(T68, T69, .(.(T68, .(T69, [])), T70)) → member12_out_ggg(T68, T69, .(.(T68, .(T69, [])), T70))
member12_in_ggg(T79, T80, .(T81, T82)) → U1_ggg(T79, T80, T81, T82, member12_in_ggg(T79, T80, T82))
U1_ggg(T79, T80, T81, T82, member12_out_ggg(T79, T80, T82)) → member12_out_ggg(T79, T80, .(T81, T82))
U5_gggg(T46, T47, T48, T49, T14, member12_out_ggg(T46, T47, T49)) → reach1_out_gggg(T46, T47, .(T48, T49), T14)
reach1_in_gggg(T101, T102, T103, T104) → U6_gggg(T101, T102, T103, T104, member124_in_gag(T101, X91, T103))
member124_in_gag(T122, X119, .(.(T122, .(X119, [])), T123)) → member124_out_gag(T122, X119, .(.(T122, .(X119, [])), T123))
member124_in_gag(T130, X133, .(T131, T132)) → U2_gag(T130, X133, T131, T132, member124_in_gag(T130, X133, T132))
U2_gag(T130, X133, T131, T132, member124_out_gag(T130, X133, T132)) → member124_out_gag(T130, X133, .(T131, T132))
U6_gggg(T101, T102, T103, T104, member124_out_gag(T101, X91, T103)) → reach1_out_gggg(T101, T102, T103, T104)
reach1_in_gggg(T101, T102, T103, T104) → U7_gggg(T101, T102, T103, T104, member124_in_gag(T101, T109, T103))
U7_gggg(T101, T102, T103, T104, member124_out_gag(T101, T109, T103)) → U8_gggg(T101, T102, T103, T104, T109, member34_in_gg(T109, T104))
member34_in_gg(T153, .(T153, T154)) → member34_out_gg(T153, .(T153, T154))
member34_in_gg(T161, .(T162, T163)) → U3_gg(T161, T162, T163, member34_in_gg(T161, T163))
U3_gg(T161, T162, T163, member34_out_gg(T161, T163)) → member34_out_gg(T161, .(T162, T163))
U8_gggg(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → reach1_out_gggg(T101, T102, T103, T104)
U8_gggg(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → U9_gggg(T101, T102, T103, T104, delete44_in_gga(T109, T104, X92))
delete44_in_gga(T185, .(T185, T186), T186) → delete44_out_gga(T185, .(T185, T186), T186)
delete44_in_gga(T193, .(T194, T195), .(T194, X213)) → U4_gga(T193, T194, T195, X213, delete44_in_gga(T193, T195, X213))
U4_gga(T193, T194, T195, X213, delete44_out_gga(T193, T195, X213)) → delete44_out_gga(T193, .(T194, T195), .(T194, X213))
U9_gggg(T101, T102, T103, T104, delete44_out_gga(T109, T104, X92)) → reach1_out_gggg(T101, T102, T103, T104)
U8_gggg(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → U10_gggg(T101, T102, T103, T104, T109, delete44_in_gga(T109, T104, T172))
U10_gggg(T101, T102, T103, T104, T109, delete44_out_gga(T109, T104, T172)) → U11_gggg(T101, T102, T103, T104, reach1_in_gggg(T109, T102, T103, T172))
U11_gggg(T101, T102, T103, T104, reach1_out_gggg(T109, T102, T103, T172)) → reach1_out_gggg(T101, T102, T103, T104)

The argument filtering Pi contains the following mapping:
reach1_in_gggg(x1, x2, x3, x4)  =  reach1_in_gggg(x1, x2, x3, x4)
.(x1, x2)  =  .(x1, x2)
[]  =  []
reach1_out_gggg(x1, x2, x3, x4)  =  reach1_out_gggg
U5_gggg(x1, x2, x3, x4, x5, x6)  =  U5_gggg(x6)
member12_in_ggg(x1, x2, x3)  =  member12_in_ggg(x1, x2, x3)
member12_out_ggg(x1, x2, x3)  =  member12_out_ggg
U1_ggg(x1, x2, x3, x4, x5)  =  U1_ggg(x5)
U6_gggg(x1, x2, x3, x4, x5)  =  U6_gggg(x5)
member124_in_gag(x1, x2, x3)  =  member124_in_gag(x1, x3)
member124_out_gag(x1, x2, x3)  =  member124_out_gag(x2)
U2_gag(x1, x2, x3, x4, x5)  =  U2_gag(x5)
U7_gggg(x1, x2, x3, x4, x5)  =  U7_gggg(x2, x3, x4, x5)
U8_gggg(x1, x2, x3, x4, x5, x6)  =  U8_gggg(x2, x3, x4, x5, x6)
member34_in_gg(x1, x2)  =  member34_in_gg(x1, x2)
member34_out_gg(x1, x2)  =  member34_out_gg
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
U9_gggg(x1, x2, x3, x4, x5)  =  U9_gggg(x5)
delete44_in_gga(x1, x2, x3)  =  delete44_in_gga(x1, x2)
delete44_out_gga(x1, x2, x3)  =  delete44_out_gga(x3)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x2, x5)
U10_gggg(x1, x2, x3, x4, x5, x6)  =  U10_gggg(x2, x3, x5, x6)
U11_gggg(x1, x2, x3, x4, x5)  =  U11_gggg(x5)
DELETE44_IN_GGA(x1, x2, x3)  =  DELETE44_IN_GGA(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:

DELETE44_IN_GGA(T193, .(T194, T195), .(T194, X213)) → DELETE44_IN_GGA(T193, T195, X213)

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

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

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

DELETE44_IN_GGA(T193, .(T194, T195)) → DELETE44_IN_GGA(T193, T195)

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:

  • DELETE44_IN_GGA(T193, .(T194, T195)) → DELETE44_IN_GGA(T193, T195)
    The graph contains the following edges 1 >= 1, 2 > 2

(15) YES

(16) Obligation:

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

MEMBER34_IN_GG(T161, .(T162, T163)) → MEMBER34_IN_GG(T161, T163)

The TRS R consists of the following rules:

reach1_in_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14) → reach1_out_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14)
reach1_in_gggg(T46, T47, .(T48, T49), T14) → U5_gggg(T46, T47, T48, T49, T14, member12_in_ggg(T46, T47, T49))
member12_in_ggg(T68, T69, .(.(T68, .(T69, [])), T70)) → member12_out_ggg(T68, T69, .(.(T68, .(T69, [])), T70))
member12_in_ggg(T79, T80, .(T81, T82)) → U1_ggg(T79, T80, T81, T82, member12_in_ggg(T79, T80, T82))
U1_ggg(T79, T80, T81, T82, member12_out_ggg(T79, T80, T82)) → member12_out_ggg(T79, T80, .(T81, T82))
U5_gggg(T46, T47, T48, T49, T14, member12_out_ggg(T46, T47, T49)) → reach1_out_gggg(T46, T47, .(T48, T49), T14)
reach1_in_gggg(T101, T102, T103, T104) → U6_gggg(T101, T102, T103, T104, member124_in_gag(T101, X91, T103))
member124_in_gag(T122, X119, .(.(T122, .(X119, [])), T123)) → member124_out_gag(T122, X119, .(.(T122, .(X119, [])), T123))
member124_in_gag(T130, X133, .(T131, T132)) → U2_gag(T130, X133, T131, T132, member124_in_gag(T130, X133, T132))
U2_gag(T130, X133, T131, T132, member124_out_gag(T130, X133, T132)) → member124_out_gag(T130, X133, .(T131, T132))
U6_gggg(T101, T102, T103, T104, member124_out_gag(T101, X91, T103)) → reach1_out_gggg(T101, T102, T103, T104)
reach1_in_gggg(T101, T102, T103, T104) → U7_gggg(T101, T102, T103, T104, member124_in_gag(T101, T109, T103))
U7_gggg(T101, T102, T103, T104, member124_out_gag(T101, T109, T103)) → U8_gggg(T101, T102, T103, T104, T109, member34_in_gg(T109, T104))
member34_in_gg(T153, .(T153, T154)) → member34_out_gg(T153, .(T153, T154))
member34_in_gg(T161, .(T162, T163)) → U3_gg(T161, T162, T163, member34_in_gg(T161, T163))
U3_gg(T161, T162, T163, member34_out_gg(T161, T163)) → member34_out_gg(T161, .(T162, T163))
U8_gggg(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → reach1_out_gggg(T101, T102, T103, T104)
U8_gggg(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → U9_gggg(T101, T102, T103, T104, delete44_in_gga(T109, T104, X92))
delete44_in_gga(T185, .(T185, T186), T186) → delete44_out_gga(T185, .(T185, T186), T186)
delete44_in_gga(T193, .(T194, T195), .(T194, X213)) → U4_gga(T193, T194, T195, X213, delete44_in_gga(T193, T195, X213))
U4_gga(T193, T194, T195, X213, delete44_out_gga(T193, T195, X213)) → delete44_out_gga(T193, .(T194, T195), .(T194, X213))
U9_gggg(T101, T102, T103, T104, delete44_out_gga(T109, T104, X92)) → reach1_out_gggg(T101, T102, T103, T104)
U8_gggg(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → U10_gggg(T101, T102, T103, T104, T109, delete44_in_gga(T109, T104, T172))
U10_gggg(T101, T102, T103, T104, T109, delete44_out_gga(T109, T104, T172)) → U11_gggg(T101, T102, T103, T104, reach1_in_gggg(T109, T102, T103, T172))
U11_gggg(T101, T102, T103, T104, reach1_out_gggg(T109, T102, T103, T172)) → reach1_out_gggg(T101, T102, T103, T104)

The argument filtering Pi contains the following mapping:
reach1_in_gggg(x1, x2, x3, x4)  =  reach1_in_gggg(x1, x2, x3, x4)
.(x1, x2)  =  .(x1, x2)
[]  =  []
reach1_out_gggg(x1, x2, x3, x4)  =  reach1_out_gggg
U5_gggg(x1, x2, x3, x4, x5, x6)  =  U5_gggg(x6)
member12_in_ggg(x1, x2, x3)  =  member12_in_ggg(x1, x2, x3)
member12_out_ggg(x1, x2, x3)  =  member12_out_ggg
U1_ggg(x1, x2, x3, x4, x5)  =  U1_ggg(x5)
U6_gggg(x1, x2, x3, x4, x5)  =  U6_gggg(x5)
member124_in_gag(x1, x2, x3)  =  member124_in_gag(x1, x3)
member124_out_gag(x1, x2, x3)  =  member124_out_gag(x2)
U2_gag(x1, x2, x3, x4, x5)  =  U2_gag(x5)
U7_gggg(x1, x2, x3, x4, x5)  =  U7_gggg(x2, x3, x4, x5)
U8_gggg(x1, x2, x3, x4, x5, x6)  =  U8_gggg(x2, x3, x4, x5, x6)
member34_in_gg(x1, x2)  =  member34_in_gg(x1, x2)
member34_out_gg(x1, x2)  =  member34_out_gg
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
U9_gggg(x1, x2, x3, x4, x5)  =  U9_gggg(x5)
delete44_in_gga(x1, x2, x3)  =  delete44_in_gga(x1, x2)
delete44_out_gga(x1, x2, x3)  =  delete44_out_gga(x3)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x2, x5)
U10_gggg(x1, x2, x3, x4, x5, x6)  =  U10_gggg(x2, x3, x5, x6)
U11_gggg(x1, x2, x3, x4, x5)  =  U11_gggg(x5)
MEMBER34_IN_GG(x1, x2)  =  MEMBER34_IN_GG(x1, 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:

MEMBER34_IN_GG(T161, .(T162, T163)) → MEMBER34_IN_GG(T161, T163)

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

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

MEMBER34_IN_GG(T161, .(T162, T163)) → MEMBER34_IN_GG(T161, T163)

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:

  • MEMBER34_IN_GG(T161, .(T162, T163)) → MEMBER34_IN_GG(T161, T163)
    The graph contains the following edges 1 >= 1, 2 > 2

(22) YES

(23) Obligation:

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

MEMBER124_IN_GAG(T130, X133, .(T131, T132)) → MEMBER124_IN_GAG(T130, X133, T132)

The TRS R consists of the following rules:

reach1_in_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14) → reach1_out_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14)
reach1_in_gggg(T46, T47, .(T48, T49), T14) → U5_gggg(T46, T47, T48, T49, T14, member12_in_ggg(T46, T47, T49))
member12_in_ggg(T68, T69, .(.(T68, .(T69, [])), T70)) → member12_out_ggg(T68, T69, .(.(T68, .(T69, [])), T70))
member12_in_ggg(T79, T80, .(T81, T82)) → U1_ggg(T79, T80, T81, T82, member12_in_ggg(T79, T80, T82))
U1_ggg(T79, T80, T81, T82, member12_out_ggg(T79, T80, T82)) → member12_out_ggg(T79, T80, .(T81, T82))
U5_gggg(T46, T47, T48, T49, T14, member12_out_ggg(T46, T47, T49)) → reach1_out_gggg(T46, T47, .(T48, T49), T14)
reach1_in_gggg(T101, T102, T103, T104) → U6_gggg(T101, T102, T103, T104, member124_in_gag(T101, X91, T103))
member124_in_gag(T122, X119, .(.(T122, .(X119, [])), T123)) → member124_out_gag(T122, X119, .(.(T122, .(X119, [])), T123))
member124_in_gag(T130, X133, .(T131, T132)) → U2_gag(T130, X133, T131, T132, member124_in_gag(T130, X133, T132))
U2_gag(T130, X133, T131, T132, member124_out_gag(T130, X133, T132)) → member124_out_gag(T130, X133, .(T131, T132))
U6_gggg(T101, T102, T103, T104, member124_out_gag(T101, X91, T103)) → reach1_out_gggg(T101, T102, T103, T104)
reach1_in_gggg(T101, T102, T103, T104) → U7_gggg(T101, T102, T103, T104, member124_in_gag(T101, T109, T103))
U7_gggg(T101, T102, T103, T104, member124_out_gag(T101, T109, T103)) → U8_gggg(T101, T102, T103, T104, T109, member34_in_gg(T109, T104))
member34_in_gg(T153, .(T153, T154)) → member34_out_gg(T153, .(T153, T154))
member34_in_gg(T161, .(T162, T163)) → U3_gg(T161, T162, T163, member34_in_gg(T161, T163))
U3_gg(T161, T162, T163, member34_out_gg(T161, T163)) → member34_out_gg(T161, .(T162, T163))
U8_gggg(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → reach1_out_gggg(T101, T102, T103, T104)
U8_gggg(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → U9_gggg(T101, T102, T103, T104, delete44_in_gga(T109, T104, X92))
delete44_in_gga(T185, .(T185, T186), T186) → delete44_out_gga(T185, .(T185, T186), T186)
delete44_in_gga(T193, .(T194, T195), .(T194, X213)) → U4_gga(T193, T194, T195, X213, delete44_in_gga(T193, T195, X213))
U4_gga(T193, T194, T195, X213, delete44_out_gga(T193, T195, X213)) → delete44_out_gga(T193, .(T194, T195), .(T194, X213))
U9_gggg(T101, T102, T103, T104, delete44_out_gga(T109, T104, X92)) → reach1_out_gggg(T101, T102, T103, T104)
U8_gggg(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → U10_gggg(T101, T102, T103, T104, T109, delete44_in_gga(T109, T104, T172))
U10_gggg(T101, T102, T103, T104, T109, delete44_out_gga(T109, T104, T172)) → U11_gggg(T101, T102, T103, T104, reach1_in_gggg(T109, T102, T103, T172))
U11_gggg(T101, T102, T103, T104, reach1_out_gggg(T109, T102, T103, T172)) → reach1_out_gggg(T101, T102, T103, T104)

The argument filtering Pi contains the following mapping:
reach1_in_gggg(x1, x2, x3, x4)  =  reach1_in_gggg(x1, x2, x3, x4)
.(x1, x2)  =  .(x1, x2)
[]  =  []
reach1_out_gggg(x1, x2, x3, x4)  =  reach1_out_gggg
U5_gggg(x1, x2, x3, x4, x5, x6)  =  U5_gggg(x6)
member12_in_ggg(x1, x2, x3)  =  member12_in_ggg(x1, x2, x3)
member12_out_ggg(x1, x2, x3)  =  member12_out_ggg
U1_ggg(x1, x2, x3, x4, x5)  =  U1_ggg(x5)
U6_gggg(x1, x2, x3, x4, x5)  =  U6_gggg(x5)
member124_in_gag(x1, x2, x3)  =  member124_in_gag(x1, x3)
member124_out_gag(x1, x2, x3)  =  member124_out_gag(x2)
U2_gag(x1, x2, x3, x4, x5)  =  U2_gag(x5)
U7_gggg(x1, x2, x3, x4, x5)  =  U7_gggg(x2, x3, x4, x5)
U8_gggg(x1, x2, x3, x4, x5, x6)  =  U8_gggg(x2, x3, x4, x5, x6)
member34_in_gg(x1, x2)  =  member34_in_gg(x1, x2)
member34_out_gg(x1, x2)  =  member34_out_gg
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
U9_gggg(x1, x2, x3, x4, x5)  =  U9_gggg(x5)
delete44_in_gga(x1, x2, x3)  =  delete44_in_gga(x1, x2)
delete44_out_gga(x1, x2, x3)  =  delete44_out_gga(x3)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x2, x5)
U10_gggg(x1, x2, x3, x4, x5, x6)  =  U10_gggg(x2, x3, x5, x6)
U11_gggg(x1, x2, x3, x4, x5)  =  U11_gggg(x5)
MEMBER124_IN_GAG(x1, x2, x3)  =  MEMBER124_IN_GAG(x1, x3)

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:

MEMBER124_IN_GAG(T130, X133, .(T131, T132)) → MEMBER124_IN_GAG(T130, X133, T132)

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

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:

MEMBER124_IN_GAG(T130, .(T131, T132)) → MEMBER124_IN_GAG(T130, T132)

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

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

  • MEMBER124_IN_GAG(T130, .(T131, T132)) → MEMBER124_IN_GAG(T130, T132)
    The graph contains the following edges 1 >= 1, 2 > 2

(29) YES

(30) Obligation:

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

MEMBER12_IN_GGG(T79, T80, .(T81, T82)) → MEMBER12_IN_GGG(T79, T80, T82)

The TRS R consists of the following rules:

reach1_in_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14) → reach1_out_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14)
reach1_in_gggg(T46, T47, .(T48, T49), T14) → U5_gggg(T46, T47, T48, T49, T14, member12_in_ggg(T46, T47, T49))
member12_in_ggg(T68, T69, .(.(T68, .(T69, [])), T70)) → member12_out_ggg(T68, T69, .(.(T68, .(T69, [])), T70))
member12_in_ggg(T79, T80, .(T81, T82)) → U1_ggg(T79, T80, T81, T82, member12_in_ggg(T79, T80, T82))
U1_ggg(T79, T80, T81, T82, member12_out_ggg(T79, T80, T82)) → member12_out_ggg(T79, T80, .(T81, T82))
U5_gggg(T46, T47, T48, T49, T14, member12_out_ggg(T46, T47, T49)) → reach1_out_gggg(T46, T47, .(T48, T49), T14)
reach1_in_gggg(T101, T102, T103, T104) → U6_gggg(T101, T102, T103, T104, member124_in_gag(T101, X91, T103))
member124_in_gag(T122, X119, .(.(T122, .(X119, [])), T123)) → member124_out_gag(T122, X119, .(.(T122, .(X119, [])), T123))
member124_in_gag(T130, X133, .(T131, T132)) → U2_gag(T130, X133, T131, T132, member124_in_gag(T130, X133, T132))
U2_gag(T130, X133, T131, T132, member124_out_gag(T130, X133, T132)) → member124_out_gag(T130, X133, .(T131, T132))
U6_gggg(T101, T102, T103, T104, member124_out_gag(T101, X91, T103)) → reach1_out_gggg(T101, T102, T103, T104)
reach1_in_gggg(T101, T102, T103, T104) → U7_gggg(T101, T102, T103, T104, member124_in_gag(T101, T109, T103))
U7_gggg(T101, T102, T103, T104, member124_out_gag(T101, T109, T103)) → U8_gggg(T101, T102, T103, T104, T109, member34_in_gg(T109, T104))
member34_in_gg(T153, .(T153, T154)) → member34_out_gg(T153, .(T153, T154))
member34_in_gg(T161, .(T162, T163)) → U3_gg(T161, T162, T163, member34_in_gg(T161, T163))
U3_gg(T161, T162, T163, member34_out_gg(T161, T163)) → member34_out_gg(T161, .(T162, T163))
U8_gggg(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → reach1_out_gggg(T101, T102, T103, T104)
U8_gggg(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → U9_gggg(T101, T102, T103, T104, delete44_in_gga(T109, T104, X92))
delete44_in_gga(T185, .(T185, T186), T186) → delete44_out_gga(T185, .(T185, T186), T186)
delete44_in_gga(T193, .(T194, T195), .(T194, X213)) → U4_gga(T193, T194, T195, X213, delete44_in_gga(T193, T195, X213))
U4_gga(T193, T194, T195, X213, delete44_out_gga(T193, T195, X213)) → delete44_out_gga(T193, .(T194, T195), .(T194, X213))
U9_gggg(T101, T102, T103, T104, delete44_out_gga(T109, T104, X92)) → reach1_out_gggg(T101, T102, T103, T104)
U8_gggg(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → U10_gggg(T101, T102, T103, T104, T109, delete44_in_gga(T109, T104, T172))
U10_gggg(T101, T102, T103, T104, T109, delete44_out_gga(T109, T104, T172)) → U11_gggg(T101, T102, T103, T104, reach1_in_gggg(T109, T102, T103, T172))
U11_gggg(T101, T102, T103, T104, reach1_out_gggg(T109, T102, T103, T172)) → reach1_out_gggg(T101, T102, T103, T104)

The argument filtering Pi contains the following mapping:
reach1_in_gggg(x1, x2, x3, x4)  =  reach1_in_gggg(x1, x2, x3, x4)
.(x1, x2)  =  .(x1, x2)
[]  =  []
reach1_out_gggg(x1, x2, x3, x4)  =  reach1_out_gggg
U5_gggg(x1, x2, x3, x4, x5, x6)  =  U5_gggg(x6)
member12_in_ggg(x1, x2, x3)  =  member12_in_ggg(x1, x2, x3)
member12_out_ggg(x1, x2, x3)  =  member12_out_ggg
U1_ggg(x1, x2, x3, x4, x5)  =  U1_ggg(x5)
U6_gggg(x1, x2, x3, x4, x5)  =  U6_gggg(x5)
member124_in_gag(x1, x2, x3)  =  member124_in_gag(x1, x3)
member124_out_gag(x1, x2, x3)  =  member124_out_gag(x2)
U2_gag(x1, x2, x3, x4, x5)  =  U2_gag(x5)
U7_gggg(x1, x2, x3, x4, x5)  =  U7_gggg(x2, x3, x4, x5)
U8_gggg(x1, x2, x3, x4, x5, x6)  =  U8_gggg(x2, x3, x4, x5, x6)
member34_in_gg(x1, x2)  =  member34_in_gg(x1, x2)
member34_out_gg(x1, x2)  =  member34_out_gg
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
U9_gggg(x1, x2, x3, x4, x5)  =  U9_gggg(x5)
delete44_in_gga(x1, x2, x3)  =  delete44_in_gga(x1, x2)
delete44_out_gga(x1, x2, x3)  =  delete44_out_gga(x3)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x2, x5)
U10_gggg(x1, x2, x3, x4, x5, x6)  =  U10_gggg(x2, x3, x5, x6)
U11_gggg(x1, x2, x3, x4, x5)  =  U11_gggg(x5)
MEMBER12_IN_GGG(x1, x2, x3)  =  MEMBER12_IN_GGG(x1, x2, x3)

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

(31) UsableRulesProof (EQUIVALENT transformation)

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

(32) Obligation:

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

MEMBER12_IN_GGG(T79, T80, .(T81, T82)) → MEMBER12_IN_GGG(T79, T80, T82)

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

(33) PiDPToQDPProof (EQUIVALENT transformation)

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

(34) Obligation:

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

MEMBER12_IN_GGG(T79, T80, .(T81, T82)) → MEMBER12_IN_GGG(T79, T80, T82)

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

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

  • MEMBER12_IN_GGG(T79, T80, .(T81, T82)) → MEMBER12_IN_GGG(T79, T80, T82)
    The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3

(36) YES

(37) Obligation:

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

REACH1_IN_GGGG(T101, T102, T103, T104) → U7_GGGG(T101, T102, T103, T104, member124_in_gag(T101, T109, T103))
U7_GGGG(T101, T102, T103, T104, member124_out_gag(T101, T109, T103)) → U8_GGGG(T101, T102, T103, T104, T109, member34_in_gg(T109, T104))
U8_GGGG(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → U10_GGGG(T101, T102, T103, T104, T109, delete44_in_gga(T109, T104, T172))
U10_GGGG(T101, T102, T103, T104, T109, delete44_out_gga(T109, T104, T172)) → REACH1_IN_GGGG(T109, T102, T103, T172)

The TRS R consists of the following rules:

reach1_in_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14) → reach1_out_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14)
reach1_in_gggg(T46, T47, .(T48, T49), T14) → U5_gggg(T46, T47, T48, T49, T14, member12_in_ggg(T46, T47, T49))
member12_in_ggg(T68, T69, .(.(T68, .(T69, [])), T70)) → member12_out_ggg(T68, T69, .(.(T68, .(T69, [])), T70))
member12_in_ggg(T79, T80, .(T81, T82)) → U1_ggg(T79, T80, T81, T82, member12_in_ggg(T79, T80, T82))
U1_ggg(T79, T80, T81, T82, member12_out_ggg(T79, T80, T82)) → member12_out_ggg(T79, T80, .(T81, T82))
U5_gggg(T46, T47, T48, T49, T14, member12_out_ggg(T46, T47, T49)) → reach1_out_gggg(T46, T47, .(T48, T49), T14)
reach1_in_gggg(T101, T102, T103, T104) → U6_gggg(T101, T102, T103, T104, member124_in_gag(T101, X91, T103))
member124_in_gag(T122, X119, .(.(T122, .(X119, [])), T123)) → member124_out_gag(T122, X119, .(.(T122, .(X119, [])), T123))
member124_in_gag(T130, X133, .(T131, T132)) → U2_gag(T130, X133, T131, T132, member124_in_gag(T130, X133, T132))
U2_gag(T130, X133, T131, T132, member124_out_gag(T130, X133, T132)) → member124_out_gag(T130, X133, .(T131, T132))
U6_gggg(T101, T102, T103, T104, member124_out_gag(T101, X91, T103)) → reach1_out_gggg(T101, T102, T103, T104)
reach1_in_gggg(T101, T102, T103, T104) → U7_gggg(T101, T102, T103, T104, member124_in_gag(T101, T109, T103))
U7_gggg(T101, T102, T103, T104, member124_out_gag(T101, T109, T103)) → U8_gggg(T101, T102, T103, T104, T109, member34_in_gg(T109, T104))
member34_in_gg(T153, .(T153, T154)) → member34_out_gg(T153, .(T153, T154))
member34_in_gg(T161, .(T162, T163)) → U3_gg(T161, T162, T163, member34_in_gg(T161, T163))
U3_gg(T161, T162, T163, member34_out_gg(T161, T163)) → member34_out_gg(T161, .(T162, T163))
U8_gggg(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → reach1_out_gggg(T101, T102, T103, T104)
U8_gggg(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → U9_gggg(T101, T102, T103, T104, delete44_in_gga(T109, T104, X92))
delete44_in_gga(T185, .(T185, T186), T186) → delete44_out_gga(T185, .(T185, T186), T186)
delete44_in_gga(T193, .(T194, T195), .(T194, X213)) → U4_gga(T193, T194, T195, X213, delete44_in_gga(T193, T195, X213))
U4_gga(T193, T194, T195, X213, delete44_out_gga(T193, T195, X213)) → delete44_out_gga(T193, .(T194, T195), .(T194, X213))
U9_gggg(T101, T102, T103, T104, delete44_out_gga(T109, T104, X92)) → reach1_out_gggg(T101, T102, T103, T104)
U8_gggg(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → U10_gggg(T101, T102, T103, T104, T109, delete44_in_gga(T109, T104, T172))
U10_gggg(T101, T102, T103, T104, T109, delete44_out_gga(T109, T104, T172)) → U11_gggg(T101, T102, T103, T104, reach1_in_gggg(T109, T102, T103, T172))
U11_gggg(T101, T102, T103, T104, reach1_out_gggg(T109, T102, T103, T172)) → reach1_out_gggg(T101, T102, T103, T104)

The argument filtering Pi contains the following mapping:
reach1_in_gggg(x1, x2, x3, x4)  =  reach1_in_gggg(x1, x2, x3, x4)
.(x1, x2)  =  .(x1, x2)
[]  =  []
reach1_out_gggg(x1, x2, x3, x4)  =  reach1_out_gggg
U5_gggg(x1, x2, x3, x4, x5, x6)  =  U5_gggg(x6)
member12_in_ggg(x1, x2, x3)  =  member12_in_ggg(x1, x2, x3)
member12_out_ggg(x1, x2, x3)  =  member12_out_ggg
U1_ggg(x1, x2, x3, x4, x5)  =  U1_ggg(x5)
U6_gggg(x1, x2, x3, x4, x5)  =  U6_gggg(x5)
member124_in_gag(x1, x2, x3)  =  member124_in_gag(x1, x3)
member124_out_gag(x1, x2, x3)  =  member124_out_gag(x2)
U2_gag(x1, x2, x3, x4, x5)  =  U2_gag(x5)
U7_gggg(x1, x2, x3, x4, x5)  =  U7_gggg(x2, x3, x4, x5)
U8_gggg(x1, x2, x3, x4, x5, x6)  =  U8_gggg(x2, x3, x4, x5, x6)
member34_in_gg(x1, x2)  =  member34_in_gg(x1, x2)
member34_out_gg(x1, x2)  =  member34_out_gg
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
U9_gggg(x1, x2, x3, x4, x5)  =  U9_gggg(x5)
delete44_in_gga(x1, x2, x3)  =  delete44_in_gga(x1, x2)
delete44_out_gga(x1, x2, x3)  =  delete44_out_gga(x3)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x2, x5)
U10_gggg(x1, x2, x3, x4, x5, x6)  =  U10_gggg(x2, x3, x5, x6)
U11_gggg(x1, x2, x3, x4, x5)  =  U11_gggg(x5)
REACH1_IN_GGGG(x1, x2, x3, x4)  =  REACH1_IN_GGGG(x1, x2, x3, x4)
U7_GGGG(x1, x2, x3, x4, x5)  =  U7_GGGG(x2, x3, x4, x5)
U8_GGGG(x1, x2, x3, x4, x5, x6)  =  U8_GGGG(x2, x3, x4, x5, x6)
U10_GGGG(x1, x2, x3, x4, x5, x6)  =  U10_GGGG(x2, x3, x5, x6)

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

(38) UsableRulesProof (EQUIVALENT transformation)

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

(39) Obligation:

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

REACH1_IN_GGGG(T101, T102, T103, T104) → U7_GGGG(T101, T102, T103, T104, member124_in_gag(T101, T109, T103))
U7_GGGG(T101, T102, T103, T104, member124_out_gag(T101, T109, T103)) → U8_GGGG(T101, T102, T103, T104, T109, member34_in_gg(T109, T104))
U8_GGGG(T101, T102, T103, T104, T109, member34_out_gg(T109, T104)) → U10_GGGG(T101, T102, T103, T104, T109, delete44_in_gga(T109, T104, T172))
U10_GGGG(T101, T102, T103, T104, T109, delete44_out_gga(T109, T104, T172)) → REACH1_IN_GGGG(T109, T102, T103, T172)

The TRS R consists of the following rules:

member124_in_gag(T122, X119, .(.(T122, .(X119, [])), T123)) → member124_out_gag(T122, X119, .(.(T122, .(X119, [])), T123))
member124_in_gag(T130, X133, .(T131, T132)) → U2_gag(T130, X133, T131, T132, member124_in_gag(T130, X133, T132))
member34_in_gg(T153, .(T153, T154)) → member34_out_gg(T153, .(T153, T154))
member34_in_gg(T161, .(T162, T163)) → U3_gg(T161, T162, T163, member34_in_gg(T161, T163))
delete44_in_gga(T185, .(T185, T186), T186) → delete44_out_gga(T185, .(T185, T186), T186)
delete44_in_gga(T193, .(T194, T195), .(T194, X213)) → U4_gga(T193, T194, T195, X213, delete44_in_gga(T193, T195, X213))
U2_gag(T130, X133, T131, T132, member124_out_gag(T130, X133, T132)) → member124_out_gag(T130, X133, .(T131, T132))
U3_gg(T161, T162, T163, member34_out_gg(T161, T163)) → member34_out_gg(T161, .(T162, T163))
U4_gga(T193, T194, T195, X213, delete44_out_gga(T193, T195, X213)) → delete44_out_gga(T193, .(T194, T195), .(T194, X213))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
member124_in_gag(x1, x2, x3)  =  member124_in_gag(x1, x3)
member124_out_gag(x1, x2, x3)  =  member124_out_gag(x2)
U2_gag(x1, x2, x3, x4, x5)  =  U2_gag(x5)
member34_in_gg(x1, x2)  =  member34_in_gg(x1, x2)
member34_out_gg(x1, x2)  =  member34_out_gg
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
delete44_in_gga(x1, x2, x3)  =  delete44_in_gga(x1, x2)
delete44_out_gga(x1, x2, x3)  =  delete44_out_gga(x3)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x2, x5)
REACH1_IN_GGGG(x1, x2, x3, x4)  =  REACH1_IN_GGGG(x1, x2, x3, x4)
U7_GGGG(x1, x2, x3, x4, x5)  =  U7_GGGG(x2, x3, x4, x5)
U8_GGGG(x1, x2, x3, x4, x5, x6)  =  U8_GGGG(x2, x3, x4, x5, x6)
U10_GGGG(x1, x2, x3, x4, x5, x6)  =  U10_GGGG(x2, x3, x5, x6)

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

(40) PiDPToQDPProof (SOUND transformation)

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

(41) Obligation:

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

REACH1_IN_GGGG(T101, T102, T103, T104) → U7_GGGG(T102, T103, T104, member124_in_gag(T101, T103))
U7_GGGG(T102, T103, T104, member124_out_gag(T109)) → U8_GGGG(T102, T103, T104, T109, member34_in_gg(T109, T104))
U8_GGGG(T102, T103, T104, T109, member34_out_gg) → U10_GGGG(T102, T103, T109, delete44_in_gga(T109, T104))
U10_GGGG(T102, T103, T109, delete44_out_gga(T172)) → REACH1_IN_GGGG(T109, T102, T103, T172)

The TRS R consists of the following rules:

member124_in_gag(T122, .(.(T122, .(X119, [])), T123)) → member124_out_gag(X119)
member124_in_gag(T130, .(T131, T132)) → U2_gag(member124_in_gag(T130, T132))
member34_in_gg(T153, .(T153, T154)) → member34_out_gg
member34_in_gg(T161, .(T162, T163)) → U3_gg(member34_in_gg(T161, T163))
delete44_in_gga(T185, .(T185, T186)) → delete44_out_gga(T186)
delete44_in_gga(T193, .(T194, T195)) → U4_gga(T194, delete44_in_gga(T193, T195))
U2_gag(member124_out_gag(X133)) → member124_out_gag(X133)
U3_gg(member34_out_gg) → member34_out_gg
U4_gga(T194, delete44_out_gga(X213)) → delete44_out_gga(.(T194, X213))

The set Q consists of the following terms:

member124_in_gag(x0, x1)
member34_in_gg(x0, x1)
delete44_in_gga(x0, x1)
U2_gag(x0)
U3_gg(x0)
U4_gga(x0, x1)

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

(42) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


REACH1_IN_GGGG(T101, T102, T103, T104) → U7_GGGG(T102, T103, T104, member124_in_gag(T101, T103))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 1 + x2   
POL(REACH1_IN_GGGG(x1, x2, x3, x4)) = 1 + x4   
POL(U10_GGGG(x1, x2, x3, x4)) = x4   
POL(U2_gag(x1)) = 0   
POL(U3_gg(x1)) = 0   
POL(U4_gga(x1, x2)) = 1 + x2   
POL(U7_GGGG(x1, x2, x3, x4)) = x3   
POL(U8_GGGG(x1, x2, x3, x4, x5)) = x3   
POL([]) = 0   
POL(delete44_in_gga(x1, x2)) = x2   
POL(delete44_out_gga(x1)) = 1 + x1   
POL(member124_in_gag(x1, x2)) = 0   
POL(member124_out_gag(x1)) = 0   
POL(member34_in_gg(x1, x2)) = 0   
POL(member34_out_gg) = 0   

The following usable rules [FROCOS05] were oriented:

delete44_in_gga(T185, .(T185, T186)) → delete44_out_gga(T186)
delete44_in_gga(T193, .(T194, T195)) → U4_gga(T194, delete44_in_gga(T193, T195))
U4_gga(T194, delete44_out_gga(X213)) → delete44_out_gga(.(T194, X213))

(43) Obligation:

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

U7_GGGG(T102, T103, T104, member124_out_gag(T109)) → U8_GGGG(T102, T103, T104, T109, member34_in_gg(T109, T104))
U8_GGGG(T102, T103, T104, T109, member34_out_gg) → U10_GGGG(T102, T103, T109, delete44_in_gga(T109, T104))
U10_GGGG(T102, T103, T109, delete44_out_gga(T172)) → REACH1_IN_GGGG(T109, T102, T103, T172)

The TRS R consists of the following rules:

member124_in_gag(T122, .(.(T122, .(X119, [])), T123)) → member124_out_gag(X119)
member124_in_gag(T130, .(T131, T132)) → U2_gag(member124_in_gag(T130, T132))
member34_in_gg(T153, .(T153, T154)) → member34_out_gg
member34_in_gg(T161, .(T162, T163)) → U3_gg(member34_in_gg(T161, T163))
delete44_in_gga(T185, .(T185, T186)) → delete44_out_gga(T186)
delete44_in_gga(T193, .(T194, T195)) → U4_gga(T194, delete44_in_gga(T193, T195))
U2_gag(member124_out_gag(X133)) → member124_out_gag(X133)
U3_gg(member34_out_gg) → member34_out_gg
U4_gga(T194, delete44_out_gga(X213)) → delete44_out_gga(.(T194, X213))

The set Q consists of the following terms:

member124_in_gag(x0, x1)
member34_in_gg(x0, x1)
delete44_in_gga(x0, x1)
U2_gag(x0)
U3_gg(x0)
U4_gga(x0, x1)

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

(44) DependencyGraphProof (EQUIVALENT transformation)

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

(45) TRUE