0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 172 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 0 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 115 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇒, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇔, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 0 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
↳30 PiDP
↳31 UsableRulesProof (⇔, 0 ms)
↳32 PiDP
↳33 PiDPToQDPProof (⇔, 0 ms)
↳34 QDP
↳35 QDPSizeChangeProof (⇔, 0 ms)
↳36 YES
↳37 PiDP
↳38 UsableRulesProof (⇔, 0 ms)
↳39 PiDP
↳40 PiDPToQDPProof (⇒, 0 ms)
↳41 QDP
↳42 QDPOrderProof (⇔, 68 ms)
↳43 QDP
↳44 DependencyGraphProof (⇔, 0 ms)
↳45 TRUE
reachE_in_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14) → reachE_out_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14)
reachE_in_gggg(T46, T47, .(T48, T49), T14) → U5_gggg(T46, T47, T48, T49, T14, memberA_in_ggg(T46, T47, T49))
memberA_in_ggg(T68, T69, .(.(T68, .(T69, [])), T70)) → memberA_out_ggg(T68, T69, .(.(T68, .(T69, [])), T70))
memberA_in_ggg(T79, T80, .(T81, T82)) → U1_ggg(T79, T80, T81, T82, memberA_in_ggg(T79, T80, T82))
U1_ggg(T79, T80, T81, T82, memberA_out_ggg(T79, T80, T82)) → memberA_out_ggg(T79, T80, .(T81, T82))
U5_gggg(T46, T47, T48, T49, T14, memberA_out_ggg(T46, T47, T49)) → reachE_out_gggg(T46, T47, .(T48, T49), T14)
reachE_in_gggg(T103, T104, T105, T106) → U6_gggg(T103, T104, T105, T106, member1B_in_gag(T103, X81, T105))
member1B_in_gag(T132, T133, .(.(T132, .(T133, [])), T134)) → member1B_out_gag(T132, T133, .(.(T132, .(T133, [])), T134))
member1B_in_gag(T141, X121, .(T142, T143)) → U2_gag(T141, X121, T142, T143, member1B_in_gag(T141, X121, T143))
U2_gag(T141, X121, T142, T143, member1B_out_gag(T141, X121, T143)) → member1B_out_gag(T141, X121, .(T142, T143))
U6_gggg(T103, T104, T105, T106, member1B_out_gag(T103, X81, T105)) → reachE_out_gggg(T103, T104, T105, T106)
reachE_in_gggg(T103, T104, T105, T106) → U7_gggg(T103, T104, T105, T106, member1B_in_gag(T103, T113, T105))
U7_gggg(T103, T104, T105, T106, member1B_out_gag(T103, T113, T105)) → U8_gggg(T103, T104, T105, T106, T113, memberC_in_gg(T113, T106))
memberC_in_gg(T166, .(T166, T167)) → memberC_out_gg(T166, .(T166, T167))
memberC_in_gg(T174, .(T175, T176)) → U3_gg(T174, T175, T176, memberC_in_gg(T174, T176))
U3_gg(T174, T175, T176, memberC_out_gg(T174, T176)) → memberC_out_gg(T174, .(T175, T176))
U8_gggg(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → reachE_out_gggg(T103, T104, T105, T106)
U8_gggg(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → U9_gggg(T103, T104, T105, T106, deleteD_in_gga(T113, T106, X82))
deleteD_in_gga(T198, .(T198, T199), T199) → deleteD_out_gga(T198, .(T198, T199), T199)
deleteD_in_gga(T206, .(T207, T208), .(T207, X191)) → U4_gga(T206, T207, T208, X191, deleteD_in_gga(T206, T208, X191))
U4_gga(T206, T207, T208, X191, deleteD_out_gga(T206, T208, X191)) → deleteD_out_gga(T206, .(T207, T208), .(T207, X191))
U9_gggg(T103, T104, T105, T106, deleteD_out_gga(T113, T106, X82)) → reachE_out_gggg(T103, T104, T105, T106)
U8_gggg(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → U10_gggg(T103, T104, T105, T106, T113, deleteD_in_gga(T113, T106, T185))
U10_gggg(T103, T104, T105, T106, T113, deleteD_out_gga(T113, T106, T185)) → U11_gggg(T103, T104, T105, T106, reachE_in_gggg(T113, T104, T105, T185))
U11_gggg(T103, T104, T105, T106, reachE_out_gggg(T113, T104, T105, T185)) → reachE_out_gggg(T103, T104, T105, T106)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
reachE_in_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14) → reachE_out_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14)
reachE_in_gggg(T46, T47, .(T48, T49), T14) → U5_gggg(T46, T47, T48, T49, T14, memberA_in_ggg(T46, T47, T49))
memberA_in_ggg(T68, T69, .(.(T68, .(T69, [])), T70)) → memberA_out_ggg(T68, T69, .(.(T68, .(T69, [])), T70))
memberA_in_ggg(T79, T80, .(T81, T82)) → U1_ggg(T79, T80, T81, T82, memberA_in_ggg(T79, T80, T82))
U1_ggg(T79, T80, T81, T82, memberA_out_ggg(T79, T80, T82)) → memberA_out_ggg(T79, T80, .(T81, T82))
U5_gggg(T46, T47, T48, T49, T14, memberA_out_ggg(T46, T47, T49)) → reachE_out_gggg(T46, T47, .(T48, T49), T14)
reachE_in_gggg(T103, T104, T105, T106) → U6_gggg(T103, T104, T105, T106, member1B_in_gag(T103, X81, T105))
member1B_in_gag(T132, T133, .(.(T132, .(T133, [])), T134)) → member1B_out_gag(T132, T133, .(.(T132, .(T133, [])), T134))
member1B_in_gag(T141, X121, .(T142, T143)) → U2_gag(T141, X121, T142, T143, member1B_in_gag(T141, X121, T143))
U2_gag(T141, X121, T142, T143, member1B_out_gag(T141, X121, T143)) → member1B_out_gag(T141, X121, .(T142, T143))
U6_gggg(T103, T104, T105, T106, member1B_out_gag(T103, X81, T105)) → reachE_out_gggg(T103, T104, T105, T106)
reachE_in_gggg(T103, T104, T105, T106) → U7_gggg(T103, T104, T105, T106, member1B_in_gag(T103, T113, T105))
U7_gggg(T103, T104, T105, T106, member1B_out_gag(T103, T113, T105)) → U8_gggg(T103, T104, T105, T106, T113, memberC_in_gg(T113, T106))
memberC_in_gg(T166, .(T166, T167)) → memberC_out_gg(T166, .(T166, T167))
memberC_in_gg(T174, .(T175, T176)) → U3_gg(T174, T175, T176, memberC_in_gg(T174, T176))
U3_gg(T174, T175, T176, memberC_out_gg(T174, T176)) → memberC_out_gg(T174, .(T175, T176))
U8_gggg(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → reachE_out_gggg(T103, T104, T105, T106)
U8_gggg(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → U9_gggg(T103, T104, T105, T106, deleteD_in_gga(T113, T106, X82))
deleteD_in_gga(T198, .(T198, T199), T199) → deleteD_out_gga(T198, .(T198, T199), T199)
deleteD_in_gga(T206, .(T207, T208), .(T207, X191)) → U4_gga(T206, T207, T208, X191, deleteD_in_gga(T206, T208, X191))
U4_gga(T206, T207, T208, X191, deleteD_out_gga(T206, T208, X191)) → deleteD_out_gga(T206, .(T207, T208), .(T207, X191))
U9_gggg(T103, T104, T105, T106, deleteD_out_gga(T113, T106, X82)) → reachE_out_gggg(T103, T104, T105, T106)
U8_gggg(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → U10_gggg(T103, T104, T105, T106, T113, deleteD_in_gga(T113, T106, T185))
U10_gggg(T103, T104, T105, T106, T113, deleteD_out_gga(T113, T106, T185)) → U11_gggg(T103, T104, T105, T106, reachE_in_gggg(T113, T104, T105, T185))
U11_gggg(T103, T104, T105, T106, reachE_out_gggg(T113, T104, T105, T185)) → reachE_out_gggg(T103, T104, T105, T106)
REACHE_IN_GGGG(T46, T47, .(T48, T49), T14) → U5_GGGG(T46, T47, T48, T49, T14, memberA_in_ggg(T46, T47, T49))
REACHE_IN_GGGG(T46, T47, .(T48, T49), T14) → MEMBERA_IN_GGG(T46, T47, T49)
MEMBERA_IN_GGG(T79, T80, .(T81, T82)) → U1_GGG(T79, T80, T81, T82, memberA_in_ggg(T79, T80, T82))
MEMBERA_IN_GGG(T79, T80, .(T81, T82)) → MEMBERA_IN_GGG(T79, T80, T82)
REACHE_IN_GGGG(T103, T104, T105, T106) → U6_GGGG(T103, T104, T105, T106, member1B_in_gag(T103, X81, T105))
REACHE_IN_GGGG(T103, T104, T105, T106) → MEMBER1B_IN_GAG(T103, X81, T105)
MEMBER1B_IN_GAG(T141, X121, .(T142, T143)) → U2_GAG(T141, X121, T142, T143, member1B_in_gag(T141, X121, T143))
MEMBER1B_IN_GAG(T141, X121, .(T142, T143)) → MEMBER1B_IN_GAG(T141, X121, T143)
REACHE_IN_GGGG(T103, T104, T105, T106) → U7_GGGG(T103, T104, T105, T106, member1B_in_gag(T103, T113, T105))
U7_GGGG(T103, T104, T105, T106, member1B_out_gag(T103, T113, T105)) → U8_GGGG(T103, T104, T105, T106, T113, memberC_in_gg(T113, T106))
U7_GGGG(T103, T104, T105, T106, member1B_out_gag(T103, T113, T105)) → MEMBERC_IN_GG(T113, T106)
MEMBERC_IN_GG(T174, .(T175, T176)) → U3_GG(T174, T175, T176, memberC_in_gg(T174, T176))
MEMBERC_IN_GG(T174, .(T175, T176)) → MEMBERC_IN_GG(T174, T176)
U8_GGGG(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → U9_GGGG(T103, T104, T105, T106, deleteD_in_gga(T113, T106, X82))
U8_GGGG(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → DELETED_IN_GGA(T113, T106, X82)
DELETED_IN_GGA(T206, .(T207, T208), .(T207, X191)) → U4_GGA(T206, T207, T208, X191, deleteD_in_gga(T206, T208, X191))
DELETED_IN_GGA(T206, .(T207, T208), .(T207, X191)) → DELETED_IN_GGA(T206, T208, X191)
U8_GGGG(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → U10_GGGG(T103, T104, T105, T106, T113, deleteD_in_gga(T113, T106, T185))
U10_GGGG(T103, T104, T105, T106, T113, deleteD_out_gga(T113, T106, T185)) → U11_GGGG(T103, T104, T105, T106, reachE_in_gggg(T113, T104, T105, T185))
U10_GGGG(T103, T104, T105, T106, T113, deleteD_out_gga(T113, T106, T185)) → REACHE_IN_GGGG(T113, T104, T105, T185)
reachE_in_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14) → reachE_out_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14)
reachE_in_gggg(T46, T47, .(T48, T49), T14) → U5_gggg(T46, T47, T48, T49, T14, memberA_in_ggg(T46, T47, T49))
memberA_in_ggg(T68, T69, .(.(T68, .(T69, [])), T70)) → memberA_out_ggg(T68, T69, .(.(T68, .(T69, [])), T70))
memberA_in_ggg(T79, T80, .(T81, T82)) → U1_ggg(T79, T80, T81, T82, memberA_in_ggg(T79, T80, T82))
U1_ggg(T79, T80, T81, T82, memberA_out_ggg(T79, T80, T82)) → memberA_out_ggg(T79, T80, .(T81, T82))
U5_gggg(T46, T47, T48, T49, T14, memberA_out_ggg(T46, T47, T49)) → reachE_out_gggg(T46, T47, .(T48, T49), T14)
reachE_in_gggg(T103, T104, T105, T106) → U6_gggg(T103, T104, T105, T106, member1B_in_gag(T103, X81, T105))
member1B_in_gag(T132, T133, .(.(T132, .(T133, [])), T134)) → member1B_out_gag(T132, T133, .(.(T132, .(T133, [])), T134))
member1B_in_gag(T141, X121, .(T142, T143)) → U2_gag(T141, X121, T142, T143, member1B_in_gag(T141, X121, T143))
U2_gag(T141, X121, T142, T143, member1B_out_gag(T141, X121, T143)) → member1B_out_gag(T141, X121, .(T142, T143))
U6_gggg(T103, T104, T105, T106, member1B_out_gag(T103, X81, T105)) → reachE_out_gggg(T103, T104, T105, T106)
reachE_in_gggg(T103, T104, T105, T106) → U7_gggg(T103, T104, T105, T106, member1B_in_gag(T103, T113, T105))
U7_gggg(T103, T104, T105, T106, member1B_out_gag(T103, T113, T105)) → U8_gggg(T103, T104, T105, T106, T113, memberC_in_gg(T113, T106))
memberC_in_gg(T166, .(T166, T167)) → memberC_out_gg(T166, .(T166, T167))
memberC_in_gg(T174, .(T175, T176)) → U3_gg(T174, T175, T176, memberC_in_gg(T174, T176))
U3_gg(T174, T175, T176, memberC_out_gg(T174, T176)) → memberC_out_gg(T174, .(T175, T176))
U8_gggg(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → reachE_out_gggg(T103, T104, T105, T106)
U8_gggg(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → U9_gggg(T103, T104, T105, T106, deleteD_in_gga(T113, T106, X82))
deleteD_in_gga(T198, .(T198, T199), T199) → deleteD_out_gga(T198, .(T198, T199), T199)
deleteD_in_gga(T206, .(T207, T208), .(T207, X191)) → U4_gga(T206, T207, T208, X191, deleteD_in_gga(T206, T208, X191))
U4_gga(T206, T207, T208, X191, deleteD_out_gga(T206, T208, X191)) → deleteD_out_gga(T206, .(T207, T208), .(T207, X191))
U9_gggg(T103, T104, T105, T106, deleteD_out_gga(T113, T106, X82)) → reachE_out_gggg(T103, T104, T105, T106)
U8_gggg(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → U10_gggg(T103, T104, T105, T106, T113, deleteD_in_gga(T113, T106, T185))
U10_gggg(T103, T104, T105, T106, T113, deleteD_out_gga(T113, T106, T185)) → U11_gggg(T103, T104, T105, T106, reachE_in_gggg(T113, T104, T105, T185))
U11_gggg(T103, T104, T105, T106, reachE_out_gggg(T113, T104, T105, T185)) → reachE_out_gggg(T103, T104, T105, T106)
REACHE_IN_GGGG(T46, T47, .(T48, T49), T14) → U5_GGGG(T46, T47, T48, T49, T14, memberA_in_ggg(T46, T47, T49))
REACHE_IN_GGGG(T46, T47, .(T48, T49), T14) → MEMBERA_IN_GGG(T46, T47, T49)
MEMBERA_IN_GGG(T79, T80, .(T81, T82)) → U1_GGG(T79, T80, T81, T82, memberA_in_ggg(T79, T80, T82))
MEMBERA_IN_GGG(T79, T80, .(T81, T82)) → MEMBERA_IN_GGG(T79, T80, T82)
REACHE_IN_GGGG(T103, T104, T105, T106) → U6_GGGG(T103, T104, T105, T106, member1B_in_gag(T103, X81, T105))
REACHE_IN_GGGG(T103, T104, T105, T106) → MEMBER1B_IN_GAG(T103, X81, T105)
MEMBER1B_IN_GAG(T141, X121, .(T142, T143)) → U2_GAG(T141, X121, T142, T143, member1B_in_gag(T141, X121, T143))
MEMBER1B_IN_GAG(T141, X121, .(T142, T143)) → MEMBER1B_IN_GAG(T141, X121, T143)
REACHE_IN_GGGG(T103, T104, T105, T106) → U7_GGGG(T103, T104, T105, T106, member1B_in_gag(T103, T113, T105))
U7_GGGG(T103, T104, T105, T106, member1B_out_gag(T103, T113, T105)) → U8_GGGG(T103, T104, T105, T106, T113, memberC_in_gg(T113, T106))
U7_GGGG(T103, T104, T105, T106, member1B_out_gag(T103, T113, T105)) → MEMBERC_IN_GG(T113, T106)
MEMBERC_IN_GG(T174, .(T175, T176)) → U3_GG(T174, T175, T176, memberC_in_gg(T174, T176))
MEMBERC_IN_GG(T174, .(T175, T176)) → MEMBERC_IN_GG(T174, T176)
U8_GGGG(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → U9_GGGG(T103, T104, T105, T106, deleteD_in_gga(T113, T106, X82))
U8_GGGG(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → DELETED_IN_GGA(T113, T106, X82)
DELETED_IN_GGA(T206, .(T207, T208), .(T207, X191)) → U4_GGA(T206, T207, T208, X191, deleteD_in_gga(T206, T208, X191))
DELETED_IN_GGA(T206, .(T207, T208), .(T207, X191)) → DELETED_IN_GGA(T206, T208, X191)
U8_GGGG(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → U10_GGGG(T103, T104, T105, T106, T113, deleteD_in_gga(T113, T106, T185))
U10_GGGG(T103, T104, T105, T106, T113, deleteD_out_gga(T113, T106, T185)) → U11_GGGG(T103, T104, T105, T106, reachE_in_gggg(T113, T104, T105, T185))
U10_GGGG(T103, T104, T105, T106, T113, deleteD_out_gga(T113, T106, T185)) → REACHE_IN_GGGG(T113, T104, T105, T185)
reachE_in_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14) → reachE_out_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14)
reachE_in_gggg(T46, T47, .(T48, T49), T14) → U5_gggg(T46, T47, T48, T49, T14, memberA_in_ggg(T46, T47, T49))
memberA_in_ggg(T68, T69, .(.(T68, .(T69, [])), T70)) → memberA_out_ggg(T68, T69, .(.(T68, .(T69, [])), T70))
memberA_in_ggg(T79, T80, .(T81, T82)) → U1_ggg(T79, T80, T81, T82, memberA_in_ggg(T79, T80, T82))
U1_ggg(T79, T80, T81, T82, memberA_out_ggg(T79, T80, T82)) → memberA_out_ggg(T79, T80, .(T81, T82))
U5_gggg(T46, T47, T48, T49, T14, memberA_out_ggg(T46, T47, T49)) → reachE_out_gggg(T46, T47, .(T48, T49), T14)
reachE_in_gggg(T103, T104, T105, T106) → U6_gggg(T103, T104, T105, T106, member1B_in_gag(T103, X81, T105))
member1B_in_gag(T132, T133, .(.(T132, .(T133, [])), T134)) → member1B_out_gag(T132, T133, .(.(T132, .(T133, [])), T134))
member1B_in_gag(T141, X121, .(T142, T143)) → U2_gag(T141, X121, T142, T143, member1B_in_gag(T141, X121, T143))
U2_gag(T141, X121, T142, T143, member1B_out_gag(T141, X121, T143)) → member1B_out_gag(T141, X121, .(T142, T143))
U6_gggg(T103, T104, T105, T106, member1B_out_gag(T103, X81, T105)) → reachE_out_gggg(T103, T104, T105, T106)
reachE_in_gggg(T103, T104, T105, T106) → U7_gggg(T103, T104, T105, T106, member1B_in_gag(T103, T113, T105))
U7_gggg(T103, T104, T105, T106, member1B_out_gag(T103, T113, T105)) → U8_gggg(T103, T104, T105, T106, T113, memberC_in_gg(T113, T106))
memberC_in_gg(T166, .(T166, T167)) → memberC_out_gg(T166, .(T166, T167))
memberC_in_gg(T174, .(T175, T176)) → U3_gg(T174, T175, T176, memberC_in_gg(T174, T176))
U3_gg(T174, T175, T176, memberC_out_gg(T174, T176)) → memberC_out_gg(T174, .(T175, T176))
U8_gggg(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → reachE_out_gggg(T103, T104, T105, T106)
U8_gggg(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → U9_gggg(T103, T104, T105, T106, deleteD_in_gga(T113, T106, X82))
deleteD_in_gga(T198, .(T198, T199), T199) → deleteD_out_gga(T198, .(T198, T199), T199)
deleteD_in_gga(T206, .(T207, T208), .(T207, X191)) → U4_gga(T206, T207, T208, X191, deleteD_in_gga(T206, T208, X191))
U4_gga(T206, T207, T208, X191, deleteD_out_gga(T206, T208, X191)) → deleteD_out_gga(T206, .(T207, T208), .(T207, X191))
U9_gggg(T103, T104, T105, T106, deleteD_out_gga(T113, T106, X82)) → reachE_out_gggg(T103, T104, T105, T106)
U8_gggg(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → U10_gggg(T103, T104, T105, T106, T113, deleteD_in_gga(T113, T106, T185))
U10_gggg(T103, T104, T105, T106, T113, deleteD_out_gga(T113, T106, T185)) → U11_gggg(T103, T104, T105, T106, reachE_in_gggg(T113, T104, T105, T185))
U11_gggg(T103, T104, T105, T106, reachE_out_gggg(T113, T104, T105, T185)) → reachE_out_gggg(T103, T104, T105, T106)
DELETED_IN_GGA(T206, .(T207, T208), .(T207, X191)) → DELETED_IN_GGA(T206, T208, X191)
reachE_in_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14) → reachE_out_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14)
reachE_in_gggg(T46, T47, .(T48, T49), T14) → U5_gggg(T46, T47, T48, T49, T14, memberA_in_ggg(T46, T47, T49))
memberA_in_ggg(T68, T69, .(.(T68, .(T69, [])), T70)) → memberA_out_ggg(T68, T69, .(.(T68, .(T69, [])), T70))
memberA_in_ggg(T79, T80, .(T81, T82)) → U1_ggg(T79, T80, T81, T82, memberA_in_ggg(T79, T80, T82))
U1_ggg(T79, T80, T81, T82, memberA_out_ggg(T79, T80, T82)) → memberA_out_ggg(T79, T80, .(T81, T82))
U5_gggg(T46, T47, T48, T49, T14, memberA_out_ggg(T46, T47, T49)) → reachE_out_gggg(T46, T47, .(T48, T49), T14)
reachE_in_gggg(T103, T104, T105, T106) → U6_gggg(T103, T104, T105, T106, member1B_in_gag(T103, X81, T105))
member1B_in_gag(T132, T133, .(.(T132, .(T133, [])), T134)) → member1B_out_gag(T132, T133, .(.(T132, .(T133, [])), T134))
member1B_in_gag(T141, X121, .(T142, T143)) → U2_gag(T141, X121, T142, T143, member1B_in_gag(T141, X121, T143))
U2_gag(T141, X121, T142, T143, member1B_out_gag(T141, X121, T143)) → member1B_out_gag(T141, X121, .(T142, T143))
U6_gggg(T103, T104, T105, T106, member1B_out_gag(T103, X81, T105)) → reachE_out_gggg(T103, T104, T105, T106)
reachE_in_gggg(T103, T104, T105, T106) → U7_gggg(T103, T104, T105, T106, member1B_in_gag(T103, T113, T105))
U7_gggg(T103, T104, T105, T106, member1B_out_gag(T103, T113, T105)) → U8_gggg(T103, T104, T105, T106, T113, memberC_in_gg(T113, T106))
memberC_in_gg(T166, .(T166, T167)) → memberC_out_gg(T166, .(T166, T167))
memberC_in_gg(T174, .(T175, T176)) → U3_gg(T174, T175, T176, memberC_in_gg(T174, T176))
U3_gg(T174, T175, T176, memberC_out_gg(T174, T176)) → memberC_out_gg(T174, .(T175, T176))
U8_gggg(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → reachE_out_gggg(T103, T104, T105, T106)
U8_gggg(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → U9_gggg(T103, T104, T105, T106, deleteD_in_gga(T113, T106, X82))
deleteD_in_gga(T198, .(T198, T199), T199) → deleteD_out_gga(T198, .(T198, T199), T199)
deleteD_in_gga(T206, .(T207, T208), .(T207, X191)) → U4_gga(T206, T207, T208, X191, deleteD_in_gga(T206, T208, X191))
U4_gga(T206, T207, T208, X191, deleteD_out_gga(T206, T208, X191)) → deleteD_out_gga(T206, .(T207, T208), .(T207, X191))
U9_gggg(T103, T104, T105, T106, deleteD_out_gga(T113, T106, X82)) → reachE_out_gggg(T103, T104, T105, T106)
U8_gggg(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → U10_gggg(T103, T104, T105, T106, T113, deleteD_in_gga(T113, T106, T185))
U10_gggg(T103, T104, T105, T106, T113, deleteD_out_gga(T113, T106, T185)) → U11_gggg(T103, T104, T105, T106, reachE_in_gggg(T113, T104, T105, T185))
U11_gggg(T103, T104, T105, T106, reachE_out_gggg(T113, T104, T105, T185)) → reachE_out_gggg(T103, T104, T105, T106)
DELETED_IN_GGA(T206, .(T207, T208), .(T207, X191)) → DELETED_IN_GGA(T206, T208, X191)
DELETED_IN_GGA(T206, .(T207, T208)) → DELETED_IN_GGA(T206, T208)
From the DPs we obtained the following set of size-change graphs:
MEMBERC_IN_GG(T174, .(T175, T176)) → MEMBERC_IN_GG(T174, T176)
reachE_in_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14) → reachE_out_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14)
reachE_in_gggg(T46, T47, .(T48, T49), T14) → U5_gggg(T46, T47, T48, T49, T14, memberA_in_ggg(T46, T47, T49))
memberA_in_ggg(T68, T69, .(.(T68, .(T69, [])), T70)) → memberA_out_ggg(T68, T69, .(.(T68, .(T69, [])), T70))
memberA_in_ggg(T79, T80, .(T81, T82)) → U1_ggg(T79, T80, T81, T82, memberA_in_ggg(T79, T80, T82))
U1_ggg(T79, T80, T81, T82, memberA_out_ggg(T79, T80, T82)) → memberA_out_ggg(T79, T80, .(T81, T82))
U5_gggg(T46, T47, T48, T49, T14, memberA_out_ggg(T46, T47, T49)) → reachE_out_gggg(T46, T47, .(T48, T49), T14)
reachE_in_gggg(T103, T104, T105, T106) → U6_gggg(T103, T104, T105, T106, member1B_in_gag(T103, X81, T105))
member1B_in_gag(T132, T133, .(.(T132, .(T133, [])), T134)) → member1B_out_gag(T132, T133, .(.(T132, .(T133, [])), T134))
member1B_in_gag(T141, X121, .(T142, T143)) → U2_gag(T141, X121, T142, T143, member1B_in_gag(T141, X121, T143))
U2_gag(T141, X121, T142, T143, member1B_out_gag(T141, X121, T143)) → member1B_out_gag(T141, X121, .(T142, T143))
U6_gggg(T103, T104, T105, T106, member1B_out_gag(T103, X81, T105)) → reachE_out_gggg(T103, T104, T105, T106)
reachE_in_gggg(T103, T104, T105, T106) → U7_gggg(T103, T104, T105, T106, member1B_in_gag(T103, T113, T105))
U7_gggg(T103, T104, T105, T106, member1B_out_gag(T103, T113, T105)) → U8_gggg(T103, T104, T105, T106, T113, memberC_in_gg(T113, T106))
memberC_in_gg(T166, .(T166, T167)) → memberC_out_gg(T166, .(T166, T167))
memberC_in_gg(T174, .(T175, T176)) → U3_gg(T174, T175, T176, memberC_in_gg(T174, T176))
U3_gg(T174, T175, T176, memberC_out_gg(T174, T176)) → memberC_out_gg(T174, .(T175, T176))
U8_gggg(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → reachE_out_gggg(T103, T104, T105, T106)
U8_gggg(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → U9_gggg(T103, T104, T105, T106, deleteD_in_gga(T113, T106, X82))
deleteD_in_gga(T198, .(T198, T199), T199) → deleteD_out_gga(T198, .(T198, T199), T199)
deleteD_in_gga(T206, .(T207, T208), .(T207, X191)) → U4_gga(T206, T207, T208, X191, deleteD_in_gga(T206, T208, X191))
U4_gga(T206, T207, T208, X191, deleteD_out_gga(T206, T208, X191)) → deleteD_out_gga(T206, .(T207, T208), .(T207, X191))
U9_gggg(T103, T104, T105, T106, deleteD_out_gga(T113, T106, X82)) → reachE_out_gggg(T103, T104, T105, T106)
U8_gggg(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → U10_gggg(T103, T104, T105, T106, T113, deleteD_in_gga(T113, T106, T185))
U10_gggg(T103, T104, T105, T106, T113, deleteD_out_gga(T113, T106, T185)) → U11_gggg(T103, T104, T105, T106, reachE_in_gggg(T113, T104, T105, T185))
U11_gggg(T103, T104, T105, T106, reachE_out_gggg(T113, T104, T105, T185)) → reachE_out_gggg(T103, T104, T105, T106)
MEMBERC_IN_GG(T174, .(T175, T176)) → MEMBERC_IN_GG(T174, T176)
MEMBERC_IN_GG(T174, .(T175, T176)) → MEMBERC_IN_GG(T174, T176)
From the DPs we obtained the following set of size-change graphs:
MEMBER1B_IN_GAG(T141, X121, .(T142, T143)) → MEMBER1B_IN_GAG(T141, X121, T143)
reachE_in_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14) → reachE_out_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14)
reachE_in_gggg(T46, T47, .(T48, T49), T14) → U5_gggg(T46, T47, T48, T49, T14, memberA_in_ggg(T46, T47, T49))
memberA_in_ggg(T68, T69, .(.(T68, .(T69, [])), T70)) → memberA_out_ggg(T68, T69, .(.(T68, .(T69, [])), T70))
memberA_in_ggg(T79, T80, .(T81, T82)) → U1_ggg(T79, T80, T81, T82, memberA_in_ggg(T79, T80, T82))
U1_ggg(T79, T80, T81, T82, memberA_out_ggg(T79, T80, T82)) → memberA_out_ggg(T79, T80, .(T81, T82))
U5_gggg(T46, T47, T48, T49, T14, memberA_out_ggg(T46, T47, T49)) → reachE_out_gggg(T46, T47, .(T48, T49), T14)
reachE_in_gggg(T103, T104, T105, T106) → U6_gggg(T103, T104, T105, T106, member1B_in_gag(T103, X81, T105))
member1B_in_gag(T132, T133, .(.(T132, .(T133, [])), T134)) → member1B_out_gag(T132, T133, .(.(T132, .(T133, [])), T134))
member1B_in_gag(T141, X121, .(T142, T143)) → U2_gag(T141, X121, T142, T143, member1B_in_gag(T141, X121, T143))
U2_gag(T141, X121, T142, T143, member1B_out_gag(T141, X121, T143)) → member1B_out_gag(T141, X121, .(T142, T143))
U6_gggg(T103, T104, T105, T106, member1B_out_gag(T103, X81, T105)) → reachE_out_gggg(T103, T104, T105, T106)
reachE_in_gggg(T103, T104, T105, T106) → U7_gggg(T103, T104, T105, T106, member1B_in_gag(T103, T113, T105))
U7_gggg(T103, T104, T105, T106, member1B_out_gag(T103, T113, T105)) → U8_gggg(T103, T104, T105, T106, T113, memberC_in_gg(T113, T106))
memberC_in_gg(T166, .(T166, T167)) → memberC_out_gg(T166, .(T166, T167))
memberC_in_gg(T174, .(T175, T176)) → U3_gg(T174, T175, T176, memberC_in_gg(T174, T176))
U3_gg(T174, T175, T176, memberC_out_gg(T174, T176)) → memberC_out_gg(T174, .(T175, T176))
U8_gggg(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → reachE_out_gggg(T103, T104, T105, T106)
U8_gggg(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → U9_gggg(T103, T104, T105, T106, deleteD_in_gga(T113, T106, X82))
deleteD_in_gga(T198, .(T198, T199), T199) → deleteD_out_gga(T198, .(T198, T199), T199)
deleteD_in_gga(T206, .(T207, T208), .(T207, X191)) → U4_gga(T206, T207, T208, X191, deleteD_in_gga(T206, T208, X191))
U4_gga(T206, T207, T208, X191, deleteD_out_gga(T206, T208, X191)) → deleteD_out_gga(T206, .(T207, T208), .(T207, X191))
U9_gggg(T103, T104, T105, T106, deleteD_out_gga(T113, T106, X82)) → reachE_out_gggg(T103, T104, T105, T106)
U8_gggg(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → U10_gggg(T103, T104, T105, T106, T113, deleteD_in_gga(T113, T106, T185))
U10_gggg(T103, T104, T105, T106, T113, deleteD_out_gga(T113, T106, T185)) → U11_gggg(T103, T104, T105, T106, reachE_in_gggg(T113, T104, T105, T185))
U11_gggg(T103, T104, T105, T106, reachE_out_gggg(T113, T104, T105, T185)) → reachE_out_gggg(T103, T104, T105, T106)
MEMBER1B_IN_GAG(T141, X121, .(T142, T143)) → MEMBER1B_IN_GAG(T141, X121, T143)
MEMBER1B_IN_GAG(T141, .(T142, T143)) → MEMBER1B_IN_GAG(T141, T143)
From the DPs we obtained the following set of size-change graphs:
MEMBERA_IN_GGG(T79, T80, .(T81, T82)) → MEMBERA_IN_GGG(T79, T80, T82)
reachE_in_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14) → reachE_out_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14)
reachE_in_gggg(T46, T47, .(T48, T49), T14) → U5_gggg(T46, T47, T48, T49, T14, memberA_in_ggg(T46, T47, T49))
memberA_in_ggg(T68, T69, .(.(T68, .(T69, [])), T70)) → memberA_out_ggg(T68, T69, .(.(T68, .(T69, [])), T70))
memberA_in_ggg(T79, T80, .(T81, T82)) → U1_ggg(T79, T80, T81, T82, memberA_in_ggg(T79, T80, T82))
U1_ggg(T79, T80, T81, T82, memberA_out_ggg(T79, T80, T82)) → memberA_out_ggg(T79, T80, .(T81, T82))
U5_gggg(T46, T47, T48, T49, T14, memberA_out_ggg(T46, T47, T49)) → reachE_out_gggg(T46, T47, .(T48, T49), T14)
reachE_in_gggg(T103, T104, T105, T106) → U6_gggg(T103, T104, T105, T106, member1B_in_gag(T103, X81, T105))
member1B_in_gag(T132, T133, .(.(T132, .(T133, [])), T134)) → member1B_out_gag(T132, T133, .(.(T132, .(T133, [])), T134))
member1B_in_gag(T141, X121, .(T142, T143)) → U2_gag(T141, X121, T142, T143, member1B_in_gag(T141, X121, T143))
U2_gag(T141, X121, T142, T143, member1B_out_gag(T141, X121, T143)) → member1B_out_gag(T141, X121, .(T142, T143))
U6_gggg(T103, T104, T105, T106, member1B_out_gag(T103, X81, T105)) → reachE_out_gggg(T103, T104, T105, T106)
reachE_in_gggg(T103, T104, T105, T106) → U7_gggg(T103, T104, T105, T106, member1B_in_gag(T103, T113, T105))
U7_gggg(T103, T104, T105, T106, member1B_out_gag(T103, T113, T105)) → U8_gggg(T103, T104, T105, T106, T113, memberC_in_gg(T113, T106))
memberC_in_gg(T166, .(T166, T167)) → memberC_out_gg(T166, .(T166, T167))
memberC_in_gg(T174, .(T175, T176)) → U3_gg(T174, T175, T176, memberC_in_gg(T174, T176))
U3_gg(T174, T175, T176, memberC_out_gg(T174, T176)) → memberC_out_gg(T174, .(T175, T176))
U8_gggg(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → reachE_out_gggg(T103, T104, T105, T106)
U8_gggg(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → U9_gggg(T103, T104, T105, T106, deleteD_in_gga(T113, T106, X82))
deleteD_in_gga(T198, .(T198, T199), T199) → deleteD_out_gga(T198, .(T198, T199), T199)
deleteD_in_gga(T206, .(T207, T208), .(T207, X191)) → U4_gga(T206, T207, T208, X191, deleteD_in_gga(T206, T208, X191))
U4_gga(T206, T207, T208, X191, deleteD_out_gga(T206, T208, X191)) → deleteD_out_gga(T206, .(T207, T208), .(T207, X191))
U9_gggg(T103, T104, T105, T106, deleteD_out_gga(T113, T106, X82)) → reachE_out_gggg(T103, T104, T105, T106)
U8_gggg(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → U10_gggg(T103, T104, T105, T106, T113, deleteD_in_gga(T113, T106, T185))
U10_gggg(T103, T104, T105, T106, T113, deleteD_out_gga(T113, T106, T185)) → U11_gggg(T103, T104, T105, T106, reachE_in_gggg(T113, T104, T105, T185))
U11_gggg(T103, T104, T105, T106, reachE_out_gggg(T113, T104, T105, T185)) → reachE_out_gggg(T103, T104, T105, T106)
MEMBERA_IN_GGG(T79, T80, .(T81, T82)) → MEMBERA_IN_GGG(T79, T80, T82)
MEMBERA_IN_GGG(T79, T80, .(T81, T82)) → MEMBERA_IN_GGG(T79, T80, T82)
From the DPs we obtained the following set of size-change graphs:
REACHE_IN_GGGG(T103, T104, T105, T106) → U7_GGGG(T103, T104, T105, T106, member1B_in_gag(T103, T113, T105))
U7_GGGG(T103, T104, T105, T106, member1B_out_gag(T103, T113, T105)) → U8_GGGG(T103, T104, T105, T106, T113, memberC_in_gg(T113, T106))
U8_GGGG(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → U10_GGGG(T103, T104, T105, T106, T113, deleteD_in_gga(T113, T106, T185))
U10_GGGG(T103, T104, T105, T106, T113, deleteD_out_gga(T113, T106, T185)) → REACHE_IN_GGGG(T113, T104, T105, T185)
reachE_in_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14) → reachE_out_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14)
reachE_in_gggg(T46, T47, .(T48, T49), T14) → U5_gggg(T46, T47, T48, T49, T14, memberA_in_ggg(T46, T47, T49))
memberA_in_ggg(T68, T69, .(.(T68, .(T69, [])), T70)) → memberA_out_ggg(T68, T69, .(.(T68, .(T69, [])), T70))
memberA_in_ggg(T79, T80, .(T81, T82)) → U1_ggg(T79, T80, T81, T82, memberA_in_ggg(T79, T80, T82))
U1_ggg(T79, T80, T81, T82, memberA_out_ggg(T79, T80, T82)) → memberA_out_ggg(T79, T80, .(T81, T82))
U5_gggg(T46, T47, T48, T49, T14, memberA_out_ggg(T46, T47, T49)) → reachE_out_gggg(T46, T47, .(T48, T49), T14)
reachE_in_gggg(T103, T104, T105, T106) → U6_gggg(T103, T104, T105, T106, member1B_in_gag(T103, X81, T105))
member1B_in_gag(T132, T133, .(.(T132, .(T133, [])), T134)) → member1B_out_gag(T132, T133, .(.(T132, .(T133, [])), T134))
member1B_in_gag(T141, X121, .(T142, T143)) → U2_gag(T141, X121, T142, T143, member1B_in_gag(T141, X121, T143))
U2_gag(T141, X121, T142, T143, member1B_out_gag(T141, X121, T143)) → member1B_out_gag(T141, X121, .(T142, T143))
U6_gggg(T103, T104, T105, T106, member1B_out_gag(T103, X81, T105)) → reachE_out_gggg(T103, T104, T105, T106)
reachE_in_gggg(T103, T104, T105, T106) → U7_gggg(T103, T104, T105, T106, member1B_in_gag(T103, T113, T105))
U7_gggg(T103, T104, T105, T106, member1B_out_gag(T103, T113, T105)) → U8_gggg(T103, T104, T105, T106, T113, memberC_in_gg(T113, T106))
memberC_in_gg(T166, .(T166, T167)) → memberC_out_gg(T166, .(T166, T167))
memberC_in_gg(T174, .(T175, T176)) → U3_gg(T174, T175, T176, memberC_in_gg(T174, T176))
U3_gg(T174, T175, T176, memberC_out_gg(T174, T176)) → memberC_out_gg(T174, .(T175, T176))
U8_gggg(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → reachE_out_gggg(T103, T104, T105, T106)
U8_gggg(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → U9_gggg(T103, T104, T105, T106, deleteD_in_gga(T113, T106, X82))
deleteD_in_gga(T198, .(T198, T199), T199) → deleteD_out_gga(T198, .(T198, T199), T199)
deleteD_in_gga(T206, .(T207, T208), .(T207, X191)) → U4_gga(T206, T207, T208, X191, deleteD_in_gga(T206, T208, X191))
U4_gga(T206, T207, T208, X191, deleteD_out_gga(T206, T208, X191)) → deleteD_out_gga(T206, .(T207, T208), .(T207, X191))
U9_gggg(T103, T104, T105, T106, deleteD_out_gga(T113, T106, X82)) → reachE_out_gggg(T103, T104, T105, T106)
U8_gggg(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → U10_gggg(T103, T104, T105, T106, T113, deleteD_in_gga(T113, T106, T185))
U10_gggg(T103, T104, T105, T106, T113, deleteD_out_gga(T113, T106, T185)) → U11_gggg(T103, T104, T105, T106, reachE_in_gggg(T113, T104, T105, T185))
U11_gggg(T103, T104, T105, T106, reachE_out_gggg(T113, T104, T105, T185)) → reachE_out_gggg(T103, T104, T105, T106)
REACHE_IN_GGGG(T103, T104, T105, T106) → U7_GGGG(T103, T104, T105, T106, member1B_in_gag(T103, T113, T105))
U7_GGGG(T103, T104, T105, T106, member1B_out_gag(T103, T113, T105)) → U8_GGGG(T103, T104, T105, T106, T113, memberC_in_gg(T113, T106))
U8_GGGG(T103, T104, T105, T106, T113, memberC_out_gg(T113, T106)) → U10_GGGG(T103, T104, T105, T106, T113, deleteD_in_gga(T113, T106, T185))
U10_GGGG(T103, T104, T105, T106, T113, deleteD_out_gga(T113, T106, T185)) → REACHE_IN_GGGG(T113, T104, T105, T185)
member1B_in_gag(T132, T133, .(.(T132, .(T133, [])), T134)) → member1B_out_gag(T132, T133, .(.(T132, .(T133, [])), T134))
member1B_in_gag(T141, X121, .(T142, T143)) → U2_gag(T141, X121, T142, T143, member1B_in_gag(T141, X121, T143))
memberC_in_gg(T166, .(T166, T167)) → memberC_out_gg(T166, .(T166, T167))
memberC_in_gg(T174, .(T175, T176)) → U3_gg(T174, T175, T176, memberC_in_gg(T174, T176))
deleteD_in_gga(T198, .(T198, T199), T199) → deleteD_out_gga(T198, .(T198, T199), T199)
deleteD_in_gga(T206, .(T207, T208), .(T207, X191)) → U4_gga(T206, T207, T208, X191, deleteD_in_gga(T206, T208, X191))
U2_gag(T141, X121, T142, T143, member1B_out_gag(T141, X121, T143)) → member1B_out_gag(T141, X121, .(T142, T143))
U3_gg(T174, T175, T176, memberC_out_gg(T174, T176)) → memberC_out_gg(T174, .(T175, T176))
U4_gga(T206, T207, T208, X191, deleteD_out_gga(T206, T208, X191)) → deleteD_out_gga(T206, .(T207, T208), .(T207, X191))
REACHE_IN_GGGG(T103, T104, T105, T106) → U7_GGGG(T104, T105, T106, member1B_in_gag(T103, T105))
U7_GGGG(T104, T105, T106, member1B_out_gag(T113)) → U8_GGGG(T104, T105, T106, T113, memberC_in_gg(T113, T106))
U8_GGGG(T104, T105, T106, T113, memberC_out_gg) → U10_GGGG(T104, T105, T113, deleteD_in_gga(T113, T106))
U10_GGGG(T104, T105, T113, deleteD_out_gga(T185)) → REACHE_IN_GGGG(T113, T104, T105, T185)
member1B_in_gag(T132, .(.(T132, .(T133, [])), T134)) → member1B_out_gag(T133)
member1B_in_gag(T141, .(T142, T143)) → U2_gag(member1B_in_gag(T141, T143))
memberC_in_gg(T166, .(T166, T167)) → memberC_out_gg
memberC_in_gg(T174, .(T175, T176)) → U3_gg(memberC_in_gg(T174, T176))
deleteD_in_gga(T198, .(T198, T199)) → deleteD_out_gga(T199)
deleteD_in_gga(T206, .(T207, T208)) → U4_gga(T207, deleteD_in_gga(T206, T208))
U2_gag(member1B_out_gag(X121)) → member1B_out_gag(X121)
U3_gg(memberC_out_gg) → memberC_out_gg
U4_gga(T207, deleteD_out_gga(X191)) → deleteD_out_gga(.(T207, X191))
member1B_in_gag(x0, x1)
memberC_in_gg(x0, x1)
deleteD_in_gga(x0, x1)
U2_gag(x0)
U3_gg(x0)
U4_gga(x0, x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
REACHE_IN_GGGG(T103, T104, T105, T106) → U7_GGGG(T104, T105, T106, member1B_in_gag(T103, T105))
POL(.(x1, x2)) = 1 + x2
POL(REACHE_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(deleteD_in_gga(x1, x2)) = x2
POL(deleteD_out_gga(x1)) = 1 + x1
POL(member1B_in_gag(x1, x2)) = 0
POL(member1B_out_gag(x1)) = 0
POL(memberC_in_gg(x1, x2)) = 0
POL(memberC_out_gg) = 0
deleteD_in_gga(T198, .(T198, T199)) → deleteD_out_gga(T199)
deleteD_in_gga(T206, .(T207, T208)) → U4_gga(T207, deleteD_in_gga(T206, T208))
U4_gga(T207, deleteD_out_gga(X191)) → deleteD_out_gga(.(T207, X191))
U7_GGGG(T104, T105, T106, member1B_out_gag(T113)) → U8_GGGG(T104, T105, T106, T113, memberC_in_gg(T113, T106))
U8_GGGG(T104, T105, T106, T113, memberC_out_gg) → U10_GGGG(T104, T105, T113, deleteD_in_gga(T113, T106))
U10_GGGG(T104, T105, T113, deleteD_out_gga(T185)) → REACHE_IN_GGGG(T113, T104, T105, T185)
member1B_in_gag(T132, .(.(T132, .(T133, [])), T134)) → member1B_out_gag(T133)
member1B_in_gag(T141, .(T142, T143)) → U2_gag(member1B_in_gag(T141, T143))
memberC_in_gg(T166, .(T166, T167)) → memberC_out_gg
memberC_in_gg(T174, .(T175, T176)) → U3_gg(memberC_in_gg(T174, T176))
deleteD_in_gga(T198, .(T198, T199)) → deleteD_out_gga(T199)
deleteD_in_gga(T206, .(T207, T208)) → U4_gga(T207, deleteD_in_gga(T206, T208))
U2_gag(member1B_out_gag(X121)) → member1B_out_gag(X121)
U3_gg(memberC_out_gg) → memberC_out_gg
U4_gga(T207, deleteD_out_gga(X191)) → deleteD_out_gga(.(T207, X191))
member1B_in_gag(x0, x1)
memberC_in_gg(x0, x1)
deleteD_in_gga(x0, x1)
U2_gag(x0)
U3_gg(x0)
U4_gga(x0, x1)