0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 162 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 116 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 30 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 23 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇔, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 UsableRulesProof (⇔, 0 ms)
↳23 PiDP
↳24 PiDPToQDPProof (⇒, 0 ms)
↳25 QDP
↳26 QDPSizeChangeProof (⇔, 0 ms)
↳27 YES
↳28 PiDP
↳29 UsableRulesProof (⇔, 0 ms)
↳30 PiDP
↳31 PiDPToQDPProof (⇔, 0 ms)
↳32 QDP
↳33 QDPSizeChangeProof (⇔, 0 ms)
↳34 YES
↳35 PiDP
↳36 UsableRulesProof (⇔, 0 ms)
↳37 PiDP
↳38 PiDPToQDPProof (⇒, 19 ms)
↳39 QDP
↳40 QDPOrderProof (⇔, 237 ms)
↳41 QDP
↳42 DependencyGraphProof (⇔, 0 ms)
↳43 TRUE
reachA_in_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14) → reachA_out_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14)
reachA_in_gggg(T46, T47, .(T48, T49), T14) → U1_gggg(T46, T47, T48, T49, T14, memberB_in_ggg(T46, T47, T49))
memberB_in_ggg(T68, T69, .(.(T68, .(T69, [])), T70)) → memberB_out_ggg(T68, T69, .(.(T68, .(T69, [])), T70))
memberB_in_ggg(T79, T80, .(T81, T82)) → U3_ggg(T79, T80, T81, T82, memberB_in_ggg(T79, T80, T82))
U3_ggg(T79, T80, T81, T82, memberB_out_ggg(T79, T80, T82)) → memberB_out_ggg(T79, T80, .(T81, T82))
U1_gggg(T46, T47, T48, T49, T14, memberB_out_ggg(T46, T47, T49)) → reachA_out_gggg(T46, T47, .(T48, T49), T14)
reachA_in_gggg(T103, T104, T105, T106) → U2_gggg(T103, T104, T105, T106, pC_in_gaggag(T103, X81, T105, T106, X82, T104))
pC_in_gaggag(T103, T113, T105, T106, X82, T104) → U7_gaggag(T103, T113, T105, T106, X82, T104, memberD_in_gag(T103, T113, T105))
memberD_in_gag(T132, T133, .(.(T132, .(T133, [])), T134)) → memberD_out_gag(T132, T133, .(.(T132, .(T133, [])), T134))
memberD_in_gag(T141, X121, .(T142, T143)) → U4_gag(T141, X121, T142, T143, memberD_in_gag(T141, X121, T143))
U4_gag(T141, X121, T142, T143, memberD_out_gag(T141, X121, T143)) → memberD_out_gag(T141, X121, .(T142, T143))
U7_gaggag(T103, T113, T105, T106, X82, T104, memberD_out_gag(T103, T113, T105)) → U8_gaggag(T103, T113, T105, T106, X82, T104, pG_in_ggagg(T113, T106, X82, T104, T105))
pG_in_ggagg(T113, T106, X82, T104, T105) → U9_ggagg(T113, T106, X82, T104, T105, memberE_in_gg(T113, T106))
memberE_in_gg(T166, .(T166, T167)) → memberE_out_gg(T166, .(T166, T167))
memberE_in_gg(T174, .(T175, T176)) → U5_gg(T174, T175, T176, memberE_in_gg(T174, T176))
U5_gg(T174, T175, T176, memberE_out_gg(T174, T176)) → memberE_out_gg(T174, .(T175, T176))
U9_ggagg(T113, T106, X82, T104, T105, memberE_out_gg(T113, T106)) → U10_ggagg(T113, T106, X82, T104, T105, pH_in_ggagg(T113, T106, X82, T104, T105))
pH_in_ggagg(T113, T106, T185, T104, T105) → U11_ggagg(T113, T106, T185, T104, T105, deleteF_in_gga(T113, T106, T185))
deleteF_in_gga(T198, .(T198, T199), T199) → deleteF_out_gga(T198, .(T198, T199), T199)
deleteF_in_gga(T206, .(T207, T208), .(T207, X191)) → U6_gga(T206, T207, T208, X191, deleteF_in_gga(T206, T208, X191))
U6_gga(T206, T207, T208, X191, deleteF_out_gga(T206, T208, X191)) → deleteF_out_gga(T206, .(T207, T208), .(T207, X191))
U11_ggagg(T113, T106, T185, T104, T105, deleteF_out_gga(T113, T106, T185)) → U12_ggagg(T113, T106, T185, T104, T105, reachA_in_gggg(T113, T104, T105, T185))
U12_ggagg(T113, T106, T185, T104, T105, reachA_out_gggg(T113, T104, T105, T185)) → pH_out_ggagg(T113, T106, T185, T104, T105)
U10_ggagg(T113, T106, X82, T104, T105, pH_out_ggagg(T113, T106, X82, T104, T105)) → pG_out_ggagg(T113, T106, X82, T104, T105)
U8_gaggag(T103, T113, T105, T106, X82, T104, pG_out_ggagg(T113, T106, X82, T104, T105)) → pC_out_gaggag(T103, T113, T105, T106, X82, T104)
U2_gggg(T103, T104, T105, T106, pC_out_gaggag(T103, X81, T105, T106, X82, T104)) → reachA_out_gggg(T103, T104, T105, T106)
REACHA_IN_GGGG(T46, T47, .(T48, T49), T14) → U1_GGGG(T46, T47, T48, T49, T14, memberB_in_ggg(T46, T47, T49))
REACHA_IN_GGGG(T46, T47, .(T48, T49), T14) → MEMBERB_IN_GGG(T46, T47, T49)
MEMBERB_IN_GGG(T79, T80, .(T81, T82)) → U3_GGG(T79, T80, T81, T82, memberB_in_ggg(T79, T80, T82))
MEMBERB_IN_GGG(T79, T80, .(T81, T82)) → MEMBERB_IN_GGG(T79, T80, T82)
REACHA_IN_GGGG(T103, T104, T105, T106) → U2_GGGG(T103, T104, T105, T106, pC_in_gaggag(T103, X81, T105, T106, X82, T104))
REACHA_IN_GGGG(T103, T104, T105, T106) → PC_IN_GAGGAG(T103, X81, T105, T106, X82, T104)
PC_IN_GAGGAG(T103, T113, T105, T106, X82, T104) → U7_GAGGAG(T103, T113, T105, T106, X82, T104, memberD_in_gag(T103, T113, T105))
PC_IN_GAGGAG(T103, T113, T105, T106, X82, T104) → MEMBERD_IN_GAG(T103, T113, T105)
MEMBERD_IN_GAG(T141, X121, .(T142, T143)) → U4_GAG(T141, X121, T142, T143, memberD_in_gag(T141, X121, T143))
MEMBERD_IN_GAG(T141, X121, .(T142, T143)) → MEMBERD_IN_GAG(T141, X121, T143)
U7_GAGGAG(T103, T113, T105, T106, X82, T104, memberD_out_gag(T103, T113, T105)) → U8_GAGGAG(T103, T113, T105, T106, X82, T104, pG_in_ggagg(T113, T106, X82, T104, T105))
U7_GAGGAG(T103, T113, T105, T106, X82, T104, memberD_out_gag(T103, T113, T105)) → PG_IN_GGAGG(T113, T106, X82, T104, T105)
PG_IN_GGAGG(T113, T106, X82, T104, T105) → U9_GGAGG(T113, T106, X82, T104, T105, memberE_in_gg(T113, T106))
PG_IN_GGAGG(T113, T106, X82, T104, T105) → MEMBERE_IN_GG(T113, T106)
MEMBERE_IN_GG(T174, .(T175, T176)) → U5_GG(T174, T175, T176, memberE_in_gg(T174, T176))
MEMBERE_IN_GG(T174, .(T175, T176)) → MEMBERE_IN_GG(T174, T176)
U9_GGAGG(T113, T106, X82, T104, T105, memberE_out_gg(T113, T106)) → U10_GGAGG(T113, T106, X82, T104, T105, pH_in_ggagg(T113, T106, X82, T104, T105))
U9_GGAGG(T113, T106, X82, T104, T105, memberE_out_gg(T113, T106)) → PH_IN_GGAGG(T113, T106, X82, T104, T105)
PH_IN_GGAGG(T113, T106, T185, T104, T105) → U11_GGAGG(T113, T106, T185, T104, T105, deleteF_in_gga(T113, T106, T185))
PH_IN_GGAGG(T113, T106, T185, T104, T105) → DELETEF_IN_GGA(T113, T106, T185)
DELETEF_IN_GGA(T206, .(T207, T208), .(T207, X191)) → U6_GGA(T206, T207, T208, X191, deleteF_in_gga(T206, T208, X191))
DELETEF_IN_GGA(T206, .(T207, T208), .(T207, X191)) → DELETEF_IN_GGA(T206, T208, X191)
U11_GGAGG(T113, T106, T185, T104, T105, deleteF_out_gga(T113, T106, T185)) → U12_GGAGG(T113, T106, T185, T104, T105, reachA_in_gggg(T113, T104, T105, T185))
U11_GGAGG(T113, T106, T185, T104, T105, deleteF_out_gga(T113, T106, T185)) → REACHA_IN_GGGG(T113, T104, T105, T185)
reachA_in_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14) → reachA_out_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14)
reachA_in_gggg(T46, T47, .(T48, T49), T14) → U1_gggg(T46, T47, T48, T49, T14, memberB_in_ggg(T46, T47, T49))
memberB_in_ggg(T68, T69, .(.(T68, .(T69, [])), T70)) → memberB_out_ggg(T68, T69, .(.(T68, .(T69, [])), T70))
memberB_in_ggg(T79, T80, .(T81, T82)) → U3_ggg(T79, T80, T81, T82, memberB_in_ggg(T79, T80, T82))
U3_ggg(T79, T80, T81, T82, memberB_out_ggg(T79, T80, T82)) → memberB_out_ggg(T79, T80, .(T81, T82))
U1_gggg(T46, T47, T48, T49, T14, memberB_out_ggg(T46, T47, T49)) → reachA_out_gggg(T46, T47, .(T48, T49), T14)
reachA_in_gggg(T103, T104, T105, T106) → U2_gggg(T103, T104, T105, T106, pC_in_gaggag(T103, X81, T105, T106, X82, T104))
pC_in_gaggag(T103, T113, T105, T106, X82, T104) → U7_gaggag(T103, T113, T105, T106, X82, T104, memberD_in_gag(T103, T113, T105))
memberD_in_gag(T132, T133, .(.(T132, .(T133, [])), T134)) → memberD_out_gag(T132, T133, .(.(T132, .(T133, [])), T134))
memberD_in_gag(T141, X121, .(T142, T143)) → U4_gag(T141, X121, T142, T143, memberD_in_gag(T141, X121, T143))
U4_gag(T141, X121, T142, T143, memberD_out_gag(T141, X121, T143)) → memberD_out_gag(T141, X121, .(T142, T143))
U7_gaggag(T103, T113, T105, T106, X82, T104, memberD_out_gag(T103, T113, T105)) → U8_gaggag(T103, T113, T105, T106, X82, T104, pG_in_ggagg(T113, T106, X82, T104, T105))
pG_in_ggagg(T113, T106, X82, T104, T105) → U9_ggagg(T113, T106, X82, T104, T105, memberE_in_gg(T113, T106))
memberE_in_gg(T166, .(T166, T167)) → memberE_out_gg(T166, .(T166, T167))
memberE_in_gg(T174, .(T175, T176)) → U5_gg(T174, T175, T176, memberE_in_gg(T174, T176))
U5_gg(T174, T175, T176, memberE_out_gg(T174, T176)) → memberE_out_gg(T174, .(T175, T176))
U9_ggagg(T113, T106, X82, T104, T105, memberE_out_gg(T113, T106)) → U10_ggagg(T113, T106, X82, T104, T105, pH_in_ggagg(T113, T106, X82, T104, T105))
pH_in_ggagg(T113, T106, T185, T104, T105) → U11_ggagg(T113, T106, T185, T104, T105, deleteF_in_gga(T113, T106, T185))
deleteF_in_gga(T198, .(T198, T199), T199) → deleteF_out_gga(T198, .(T198, T199), T199)
deleteF_in_gga(T206, .(T207, T208), .(T207, X191)) → U6_gga(T206, T207, T208, X191, deleteF_in_gga(T206, T208, X191))
U6_gga(T206, T207, T208, X191, deleteF_out_gga(T206, T208, X191)) → deleteF_out_gga(T206, .(T207, T208), .(T207, X191))
U11_ggagg(T113, T106, T185, T104, T105, deleteF_out_gga(T113, T106, T185)) → U12_ggagg(T113, T106, T185, T104, T105, reachA_in_gggg(T113, T104, T105, T185))
U12_ggagg(T113, T106, T185, T104, T105, reachA_out_gggg(T113, T104, T105, T185)) → pH_out_ggagg(T113, T106, T185, T104, T105)
U10_ggagg(T113, T106, X82, T104, T105, pH_out_ggagg(T113, T106, X82, T104, T105)) → pG_out_ggagg(T113, T106, X82, T104, T105)
U8_gaggag(T103, T113, T105, T106, X82, T104, pG_out_ggagg(T113, T106, X82, T104, T105)) → pC_out_gaggag(T103, T113, T105, T106, X82, T104)
U2_gggg(T103, T104, T105, T106, pC_out_gaggag(T103, X81, T105, T106, X82, T104)) → reachA_out_gggg(T103, T104, T105, T106)
REACHA_IN_GGGG(T46, T47, .(T48, T49), T14) → U1_GGGG(T46, T47, T48, T49, T14, memberB_in_ggg(T46, T47, T49))
REACHA_IN_GGGG(T46, T47, .(T48, T49), T14) → MEMBERB_IN_GGG(T46, T47, T49)
MEMBERB_IN_GGG(T79, T80, .(T81, T82)) → U3_GGG(T79, T80, T81, T82, memberB_in_ggg(T79, T80, T82))
MEMBERB_IN_GGG(T79, T80, .(T81, T82)) → MEMBERB_IN_GGG(T79, T80, T82)
REACHA_IN_GGGG(T103, T104, T105, T106) → U2_GGGG(T103, T104, T105, T106, pC_in_gaggag(T103, X81, T105, T106, X82, T104))
REACHA_IN_GGGG(T103, T104, T105, T106) → PC_IN_GAGGAG(T103, X81, T105, T106, X82, T104)
PC_IN_GAGGAG(T103, T113, T105, T106, X82, T104) → U7_GAGGAG(T103, T113, T105, T106, X82, T104, memberD_in_gag(T103, T113, T105))
PC_IN_GAGGAG(T103, T113, T105, T106, X82, T104) → MEMBERD_IN_GAG(T103, T113, T105)
MEMBERD_IN_GAG(T141, X121, .(T142, T143)) → U4_GAG(T141, X121, T142, T143, memberD_in_gag(T141, X121, T143))
MEMBERD_IN_GAG(T141, X121, .(T142, T143)) → MEMBERD_IN_GAG(T141, X121, T143)
U7_GAGGAG(T103, T113, T105, T106, X82, T104, memberD_out_gag(T103, T113, T105)) → U8_GAGGAG(T103, T113, T105, T106, X82, T104, pG_in_ggagg(T113, T106, X82, T104, T105))
U7_GAGGAG(T103, T113, T105, T106, X82, T104, memberD_out_gag(T103, T113, T105)) → PG_IN_GGAGG(T113, T106, X82, T104, T105)
PG_IN_GGAGG(T113, T106, X82, T104, T105) → U9_GGAGG(T113, T106, X82, T104, T105, memberE_in_gg(T113, T106))
PG_IN_GGAGG(T113, T106, X82, T104, T105) → MEMBERE_IN_GG(T113, T106)
MEMBERE_IN_GG(T174, .(T175, T176)) → U5_GG(T174, T175, T176, memberE_in_gg(T174, T176))
MEMBERE_IN_GG(T174, .(T175, T176)) → MEMBERE_IN_GG(T174, T176)
U9_GGAGG(T113, T106, X82, T104, T105, memberE_out_gg(T113, T106)) → U10_GGAGG(T113, T106, X82, T104, T105, pH_in_ggagg(T113, T106, X82, T104, T105))
U9_GGAGG(T113, T106, X82, T104, T105, memberE_out_gg(T113, T106)) → PH_IN_GGAGG(T113, T106, X82, T104, T105)
PH_IN_GGAGG(T113, T106, T185, T104, T105) → U11_GGAGG(T113, T106, T185, T104, T105, deleteF_in_gga(T113, T106, T185))
PH_IN_GGAGG(T113, T106, T185, T104, T105) → DELETEF_IN_GGA(T113, T106, T185)
DELETEF_IN_GGA(T206, .(T207, T208), .(T207, X191)) → U6_GGA(T206, T207, T208, X191, deleteF_in_gga(T206, T208, X191))
DELETEF_IN_GGA(T206, .(T207, T208), .(T207, X191)) → DELETEF_IN_GGA(T206, T208, X191)
U11_GGAGG(T113, T106, T185, T104, T105, deleteF_out_gga(T113, T106, T185)) → U12_GGAGG(T113, T106, T185, T104, T105, reachA_in_gggg(T113, T104, T105, T185))
U11_GGAGG(T113, T106, T185, T104, T105, deleteF_out_gga(T113, T106, T185)) → REACHA_IN_GGGG(T113, T104, T105, T185)
reachA_in_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14) → reachA_out_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14)
reachA_in_gggg(T46, T47, .(T48, T49), T14) → U1_gggg(T46, T47, T48, T49, T14, memberB_in_ggg(T46, T47, T49))
memberB_in_ggg(T68, T69, .(.(T68, .(T69, [])), T70)) → memberB_out_ggg(T68, T69, .(.(T68, .(T69, [])), T70))
memberB_in_ggg(T79, T80, .(T81, T82)) → U3_ggg(T79, T80, T81, T82, memberB_in_ggg(T79, T80, T82))
U3_ggg(T79, T80, T81, T82, memberB_out_ggg(T79, T80, T82)) → memberB_out_ggg(T79, T80, .(T81, T82))
U1_gggg(T46, T47, T48, T49, T14, memberB_out_ggg(T46, T47, T49)) → reachA_out_gggg(T46, T47, .(T48, T49), T14)
reachA_in_gggg(T103, T104, T105, T106) → U2_gggg(T103, T104, T105, T106, pC_in_gaggag(T103, X81, T105, T106, X82, T104))
pC_in_gaggag(T103, T113, T105, T106, X82, T104) → U7_gaggag(T103, T113, T105, T106, X82, T104, memberD_in_gag(T103, T113, T105))
memberD_in_gag(T132, T133, .(.(T132, .(T133, [])), T134)) → memberD_out_gag(T132, T133, .(.(T132, .(T133, [])), T134))
memberD_in_gag(T141, X121, .(T142, T143)) → U4_gag(T141, X121, T142, T143, memberD_in_gag(T141, X121, T143))
U4_gag(T141, X121, T142, T143, memberD_out_gag(T141, X121, T143)) → memberD_out_gag(T141, X121, .(T142, T143))
U7_gaggag(T103, T113, T105, T106, X82, T104, memberD_out_gag(T103, T113, T105)) → U8_gaggag(T103, T113, T105, T106, X82, T104, pG_in_ggagg(T113, T106, X82, T104, T105))
pG_in_ggagg(T113, T106, X82, T104, T105) → U9_ggagg(T113, T106, X82, T104, T105, memberE_in_gg(T113, T106))
memberE_in_gg(T166, .(T166, T167)) → memberE_out_gg(T166, .(T166, T167))
memberE_in_gg(T174, .(T175, T176)) → U5_gg(T174, T175, T176, memberE_in_gg(T174, T176))
U5_gg(T174, T175, T176, memberE_out_gg(T174, T176)) → memberE_out_gg(T174, .(T175, T176))
U9_ggagg(T113, T106, X82, T104, T105, memberE_out_gg(T113, T106)) → U10_ggagg(T113, T106, X82, T104, T105, pH_in_ggagg(T113, T106, X82, T104, T105))
pH_in_ggagg(T113, T106, T185, T104, T105) → U11_ggagg(T113, T106, T185, T104, T105, deleteF_in_gga(T113, T106, T185))
deleteF_in_gga(T198, .(T198, T199), T199) → deleteF_out_gga(T198, .(T198, T199), T199)
deleteF_in_gga(T206, .(T207, T208), .(T207, X191)) → U6_gga(T206, T207, T208, X191, deleteF_in_gga(T206, T208, X191))
U6_gga(T206, T207, T208, X191, deleteF_out_gga(T206, T208, X191)) → deleteF_out_gga(T206, .(T207, T208), .(T207, X191))
U11_ggagg(T113, T106, T185, T104, T105, deleteF_out_gga(T113, T106, T185)) → U12_ggagg(T113, T106, T185, T104, T105, reachA_in_gggg(T113, T104, T105, T185))
U12_ggagg(T113, T106, T185, T104, T105, reachA_out_gggg(T113, T104, T105, T185)) → pH_out_ggagg(T113, T106, T185, T104, T105)
U10_ggagg(T113, T106, X82, T104, T105, pH_out_ggagg(T113, T106, X82, T104, T105)) → pG_out_ggagg(T113, T106, X82, T104, T105)
U8_gaggag(T103, T113, T105, T106, X82, T104, pG_out_ggagg(T113, T106, X82, T104, T105)) → pC_out_gaggag(T103, T113, T105, T106, X82, T104)
U2_gggg(T103, T104, T105, T106, pC_out_gaggag(T103, X81, T105, T106, X82, T104)) → reachA_out_gggg(T103, T104, T105, T106)
DELETEF_IN_GGA(T206, .(T207, T208), .(T207, X191)) → DELETEF_IN_GGA(T206, T208, X191)
reachA_in_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14) → reachA_out_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14)
reachA_in_gggg(T46, T47, .(T48, T49), T14) → U1_gggg(T46, T47, T48, T49, T14, memberB_in_ggg(T46, T47, T49))
memberB_in_ggg(T68, T69, .(.(T68, .(T69, [])), T70)) → memberB_out_ggg(T68, T69, .(.(T68, .(T69, [])), T70))
memberB_in_ggg(T79, T80, .(T81, T82)) → U3_ggg(T79, T80, T81, T82, memberB_in_ggg(T79, T80, T82))
U3_ggg(T79, T80, T81, T82, memberB_out_ggg(T79, T80, T82)) → memberB_out_ggg(T79, T80, .(T81, T82))
U1_gggg(T46, T47, T48, T49, T14, memberB_out_ggg(T46, T47, T49)) → reachA_out_gggg(T46, T47, .(T48, T49), T14)
reachA_in_gggg(T103, T104, T105, T106) → U2_gggg(T103, T104, T105, T106, pC_in_gaggag(T103, X81, T105, T106, X82, T104))
pC_in_gaggag(T103, T113, T105, T106, X82, T104) → U7_gaggag(T103, T113, T105, T106, X82, T104, memberD_in_gag(T103, T113, T105))
memberD_in_gag(T132, T133, .(.(T132, .(T133, [])), T134)) → memberD_out_gag(T132, T133, .(.(T132, .(T133, [])), T134))
memberD_in_gag(T141, X121, .(T142, T143)) → U4_gag(T141, X121, T142, T143, memberD_in_gag(T141, X121, T143))
U4_gag(T141, X121, T142, T143, memberD_out_gag(T141, X121, T143)) → memberD_out_gag(T141, X121, .(T142, T143))
U7_gaggag(T103, T113, T105, T106, X82, T104, memberD_out_gag(T103, T113, T105)) → U8_gaggag(T103, T113, T105, T106, X82, T104, pG_in_ggagg(T113, T106, X82, T104, T105))
pG_in_ggagg(T113, T106, X82, T104, T105) → U9_ggagg(T113, T106, X82, T104, T105, memberE_in_gg(T113, T106))
memberE_in_gg(T166, .(T166, T167)) → memberE_out_gg(T166, .(T166, T167))
memberE_in_gg(T174, .(T175, T176)) → U5_gg(T174, T175, T176, memberE_in_gg(T174, T176))
U5_gg(T174, T175, T176, memberE_out_gg(T174, T176)) → memberE_out_gg(T174, .(T175, T176))
U9_ggagg(T113, T106, X82, T104, T105, memberE_out_gg(T113, T106)) → U10_ggagg(T113, T106, X82, T104, T105, pH_in_ggagg(T113, T106, X82, T104, T105))
pH_in_ggagg(T113, T106, T185, T104, T105) → U11_ggagg(T113, T106, T185, T104, T105, deleteF_in_gga(T113, T106, T185))
deleteF_in_gga(T198, .(T198, T199), T199) → deleteF_out_gga(T198, .(T198, T199), T199)
deleteF_in_gga(T206, .(T207, T208), .(T207, X191)) → U6_gga(T206, T207, T208, X191, deleteF_in_gga(T206, T208, X191))
U6_gga(T206, T207, T208, X191, deleteF_out_gga(T206, T208, X191)) → deleteF_out_gga(T206, .(T207, T208), .(T207, X191))
U11_ggagg(T113, T106, T185, T104, T105, deleteF_out_gga(T113, T106, T185)) → U12_ggagg(T113, T106, T185, T104, T105, reachA_in_gggg(T113, T104, T105, T185))
U12_ggagg(T113, T106, T185, T104, T105, reachA_out_gggg(T113, T104, T105, T185)) → pH_out_ggagg(T113, T106, T185, T104, T105)
U10_ggagg(T113, T106, X82, T104, T105, pH_out_ggagg(T113, T106, X82, T104, T105)) → pG_out_ggagg(T113, T106, X82, T104, T105)
U8_gaggag(T103, T113, T105, T106, X82, T104, pG_out_ggagg(T113, T106, X82, T104, T105)) → pC_out_gaggag(T103, T113, T105, T106, X82, T104)
U2_gggg(T103, T104, T105, T106, pC_out_gaggag(T103, X81, T105, T106, X82, T104)) → reachA_out_gggg(T103, T104, T105, T106)
DELETEF_IN_GGA(T206, .(T207, T208), .(T207, X191)) → DELETEF_IN_GGA(T206, T208, X191)
DELETEF_IN_GGA(T206, .(T207, T208)) → DELETEF_IN_GGA(T206, T208)
From the DPs we obtained the following set of size-change graphs:
MEMBERE_IN_GG(T174, .(T175, T176)) → MEMBERE_IN_GG(T174, T176)
reachA_in_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14) → reachA_out_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14)
reachA_in_gggg(T46, T47, .(T48, T49), T14) → U1_gggg(T46, T47, T48, T49, T14, memberB_in_ggg(T46, T47, T49))
memberB_in_ggg(T68, T69, .(.(T68, .(T69, [])), T70)) → memberB_out_ggg(T68, T69, .(.(T68, .(T69, [])), T70))
memberB_in_ggg(T79, T80, .(T81, T82)) → U3_ggg(T79, T80, T81, T82, memberB_in_ggg(T79, T80, T82))
U3_ggg(T79, T80, T81, T82, memberB_out_ggg(T79, T80, T82)) → memberB_out_ggg(T79, T80, .(T81, T82))
U1_gggg(T46, T47, T48, T49, T14, memberB_out_ggg(T46, T47, T49)) → reachA_out_gggg(T46, T47, .(T48, T49), T14)
reachA_in_gggg(T103, T104, T105, T106) → U2_gggg(T103, T104, T105, T106, pC_in_gaggag(T103, X81, T105, T106, X82, T104))
pC_in_gaggag(T103, T113, T105, T106, X82, T104) → U7_gaggag(T103, T113, T105, T106, X82, T104, memberD_in_gag(T103, T113, T105))
memberD_in_gag(T132, T133, .(.(T132, .(T133, [])), T134)) → memberD_out_gag(T132, T133, .(.(T132, .(T133, [])), T134))
memberD_in_gag(T141, X121, .(T142, T143)) → U4_gag(T141, X121, T142, T143, memberD_in_gag(T141, X121, T143))
U4_gag(T141, X121, T142, T143, memberD_out_gag(T141, X121, T143)) → memberD_out_gag(T141, X121, .(T142, T143))
U7_gaggag(T103, T113, T105, T106, X82, T104, memberD_out_gag(T103, T113, T105)) → U8_gaggag(T103, T113, T105, T106, X82, T104, pG_in_ggagg(T113, T106, X82, T104, T105))
pG_in_ggagg(T113, T106, X82, T104, T105) → U9_ggagg(T113, T106, X82, T104, T105, memberE_in_gg(T113, T106))
memberE_in_gg(T166, .(T166, T167)) → memberE_out_gg(T166, .(T166, T167))
memberE_in_gg(T174, .(T175, T176)) → U5_gg(T174, T175, T176, memberE_in_gg(T174, T176))
U5_gg(T174, T175, T176, memberE_out_gg(T174, T176)) → memberE_out_gg(T174, .(T175, T176))
U9_ggagg(T113, T106, X82, T104, T105, memberE_out_gg(T113, T106)) → U10_ggagg(T113, T106, X82, T104, T105, pH_in_ggagg(T113, T106, X82, T104, T105))
pH_in_ggagg(T113, T106, T185, T104, T105) → U11_ggagg(T113, T106, T185, T104, T105, deleteF_in_gga(T113, T106, T185))
deleteF_in_gga(T198, .(T198, T199), T199) → deleteF_out_gga(T198, .(T198, T199), T199)
deleteF_in_gga(T206, .(T207, T208), .(T207, X191)) → U6_gga(T206, T207, T208, X191, deleteF_in_gga(T206, T208, X191))
U6_gga(T206, T207, T208, X191, deleteF_out_gga(T206, T208, X191)) → deleteF_out_gga(T206, .(T207, T208), .(T207, X191))
U11_ggagg(T113, T106, T185, T104, T105, deleteF_out_gga(T113, T106, T185)) → U12_ggagg(T113, T106, T185, T104, T105, reachA_in_gggg(T113, T104, T105, T185))
U12_ggagg(T113, T106, T185, T104, T105, reachA_out_gggg(T113, T104, T105, T185)) → pH_out_ggagg(T113, T106, T185, T104, T105)
U10_ggagg(T113, T106, X82, T104, T105, pH_out_ggagg(T113, T106, X82, T104, T105)) → pG_out_ggagg(T113, T106, X82, T104, T105)
U8_gaggag(T103, T113, T105, T106, X82, T104, pG_out_ggagg(T113, T106, X82, T104, T105)) → pC_out_gaggag(T103, T113, T105, T106, X82, T104)
U2_gggg(T103, T104, T105, T106, pC_out_gaggag(T103, X81, T105, T106, X82, T104)) → reachA_out_gggg(T103, T104, T105, T106)
MEMBERE_IN_GG(T174, .(T175, T176)) → MEMBERE_IN_GG(T174, T176)
MEMBERE_IN_GG(T174, .(T175, T176)) → MEMBERE_IN_GG(T174, T176)
From the DPs we obtained the following set of size-change graphs:
MEMBERD_IN_GAG(T141, X121, .(T142, T143)) → MEMBERD_IN_GAG(T141, X121, T143)
reachA_in_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14) → reachA_out_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14)
reachA_in_gggg(T46, T47, .(T48, T49), T14) → U1_gggg(T46, T47, T48, T49, T14, memberB_in_ggg(T46, T47, T49))
memberB_in_ggg(T68, T69, .(.(T68, .(T69, [])), T70)) → memberB_out_ggg(T68, T69, .(.(T68, .(T69, [])), T70))
memberB_in_ggg(T79, T80, .(T81, T82)) → U3_ggg(T79, T80, T81, T82, memberB_in_ggg(T79, T80, T82))
U3_ggg(T79, T80, T81, T82, memberB_out_ggg(T79, T80, T82)) → memberB_out_ggg(T79, T80, .(T81, T82))
U1_gggg(T46, T47, T48, T49, T14, memberB_out_ggg(T46, T47, T49)) → reachA_out_gggg(T46, T47, .(T48, T49), T14)
reachA_in_gggg(T103, T104, T105, T106) → U2_gggg(T103, T104, T105, T106, pC_in_gaggag(T103, X81, T105, T106, X82, T104))
pC_in_gaggag(T103, T113, T105, T106, X82, T104) → U7_gaggag(T103, T113, T105, T106, X82, T104, memberD_in_gag(T103, T113, T105))
memberD_in_gag(T132, T133, .(.(T132, .(T133, [])), T134)) → memberD_out_gag(T132, T133, .(.(T132, .(T133, [])), T134))
memberD_in_gag(T141, X121, .(T142, T143)) → U4_gag(T141, X121, T142, T143, memberD_in_gag(T141, X121, T143))
U4_gag(T141, X121, T142, T143, memberD_out_gag(T141, X121, T143)) → memberD_out_gag(T141, X121, .(T142, T143))
U7_gaggag(T103, T113, T105, T106, X82, T104, memberD_out_gag(T103, T113, T105)) → U8_gaggag(T103, T113, T105, T106, X82, T104, pG_in_ggagg(T113, T106, X82, T104, T105))
pG_in_ggagg(T113, T106, X82, T104, T105) → U9_ggagg(T113, T106, X82, T104, T105, memberE_in_gg(T113, T106))
memberE_in_gg(T166, .(T166, T167)) → memberE_out_gg(T166, .(T166, T167))
memberE_in_gg(T174, .(T175, T176)) → U5_gg(T174, T175, T176, memberE_in_gg(T174, T176))
U5_gg(T174, T175, T176, memberE_out_gg(T174, T176)) → memberE_out_gg(T174, .(T175, T176))
U9_ggagg(T113, T106, X82, T104, T105, memberE_out_gg(T113, T106)) → U10_ggagg(T113, T106, X82, T104, T105, pH_in_ggagg(T113, T106, X82, T104, T105))
pH_in_ggagg(T113, T106, T185, T104, T105) → U11_ggagg(T113, T106, T185, T104, T105, deleteF_in_gga(T113, T106, T185))
deleteF_in_gga(T198, .(T198, T199), T199) → deleteF_out_gga(T198, .(T198, T199), T199)
deleteF_in_gga(T206, .(T207, T208), .(T207, X191)) → U6_gga(T206, T207, T208, X191, deleteF_in_gga(T206, T208, X191))
U6_gga(T206, T207, T208, X191, deleteF_out_gga(T206, T208, X191)) → deleteF_out_gga(T206, .(T207, T208), .(T207, X191))
U11_ggagg(T113, T106, T185, T104, T105, deleteF_out_gga(T113, T106, T185)) → U12_ggagg(T113, T106, T185, T104, T105, reachA_in_gggg(T113, T104, T105, T185))
U12_ggagg(T113, T106, T185, T104, T105, reachA_out_gggg(T113, T104, T105, T185)) → pH_out_ggagg(T113, T106, T185, T104, T105)
U10_ggagg(T113, T106, X82, T104, T105, pH_out_ggagg(T113, T106, X82, T104, T105)) → pG_out_ggagg(T113, T106, X82, T104, T105)
U8_gaggag(T103, T113, T105, T106, X82, T104, pG_out_ggagg(T113, T106, X82, T104, T105)) → pC_out_gaggag(T103, T113, T105, T106, X82, T104)
U2_gggg(T103, T104, T105, T106, pC_out_gaggag(T103, X81, T105, T106, X82, T104)) → reachA_out_gggg(T103, T104, T105, T106)
MEMBERD_IN_GAG(T141, X121, .(T142, T143)) → MEMBERD_IN_GAG(T141, X121, T143)
MEMBERD_IN_GAG(T141, .(T142, T143)) → MEMBERD_IN_GAG(T141, T143)
From the DPs we obtained the following set of size-change graphs:
MEMBERB_IN_GGG(T79, T80, .(T81, T82)) → MEMBERB_IN_GGG(T79, T80, T82)
reachA_in_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14) → reachA_out_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14)
reachA_in_gggg(T46, T47, .(T48, T49), T14) → U1_gggg(T46, T47, T48, T49, T14, memberB_in_ggg(T46, T47, T49))
memberB_in_ggg(T68, T69, .(.(T68, .(T69, [])), T70)) → memberB_out_ggg(T68, T69, .(.(T68, .(T69, [])), T70))
memberB_in_ggg(T79, T80, .(T81, T82)) → U3_ggg(T79, T80, T81, T82, memberB_in_ggg(T79, T80, T82))
U3_ggg(T79, T80, T81, T82, memberB_out_ggg(T79, T80, T82)) → memberB_out_ggg(T79, T80, .(T81, T82))
U1_gggg(T46, T47, T48, T49, T14, memberB_out_ggg(T46, T47, T49)) → reachA_out_gggg(T46, T47, .(T48, T49), T14)
reachA_in_gggg(T103, T104, T105, T106) → U2_gggg(T103, T104, T105, T106, pC_in_gaggag(T103, X81, T105, T106, X82, T104))
pC_in_gaggag(T103, T113, T105, T106, X82, T104) → U7_gaggag(T103, T113, T105, T106, X82, T104, memberD_in_gag(T103, T113, T105))
memberD_in_gag(T132, T133, .(.(T132, .(T133, [])), T134)) → memberD_out_gag(T132, T133, .(.(T132, .(T133, [])), T134))
memberD_in_gag(T141, X121, .(T142, T143)) → U4_gag(T141, X121, T142, T143, memberD_in_gag(T141, X121, T143))
U4_gag(T141, X121, T142, T143, memberD_out_gag(T141, X121, T143)) → memberD_out_gag(T141, X121, .(T142, T143))
U7_gaggag(T103, T113, T105, T106, X82, T104, memberD_out_gag(T103, T113, T105)) → U8_gaggag(T103, T113, T105, T106, X82, T104, pG_in_ggagg(T113, T106, X82, T104, T105))
pG_in_ggagg(T113, T106, X82, T104, T105) → U9_ggagg(T113, T106, X82, T104, T105, memberE_in_gg(T113, T106))
memberE_in_gg(T166, .(T166, T167)) → memberE_out_gg(T166, .(T166, T167))
memberE_in_gg(T174, .(T175, T176)) → U5_gg(T174, T175, T176, memberE_in_gg(T174, T176))
U5_gg(T174, T175, T176, memberE_out_gg(T174, T176)) → memberE_out_gg(T174, .(T175, T176))
U9_ggagg(T113, T106, X82, T104, T105, memberE_out_gg(T113, T106)) → U10_ggagg(T113, T106, X82, T104, T105, pH_in_ggagg(T113, T106, X82, T104, T105))
pH_in_ggagg(T113, T106, T185, T104, T105) → U11_ggagg(T113, T106, T185, T104, T105, deleteF_in_gga(T113, T106, T185))
deleteF_in_gga(T198, .(T198, T199), T199) → deleteF_out_gga(T198, .(T198, T199), T199)
deleteF_in_gga(T206, .(T207, T208), .(T207, X191)) → U6_gga(T206, T207, T208, X191, deleteF_in_gga(T206, T208, X191))
U6_gga(T206, T207, T208, X191, deleteF_out_gga(T206, T208, X191)) → deleteF_out_gga(T206, .(T207, T208), .(T207, X191))
U11_ggagg(T113, T106, T185, T104, T105, deleteF_out_gga(T113, T106, T185)) → U12_ggagg(T113, T106, T185, T104, T105, reachA_in_gggg(T113, T104, T105, T185))
U12_ggagg(T113, T106, T185, T104, T105, reachA_out_gggg(T113, T104, T105, T185)) → pH_out_ggagg(T113, T106, T185, T104, T105)
U10_ggagg(T113, T106, X82, T104, T105, pH_out_ggagg(T113, T106, X82, T104, T105)) → pG_out_ggagg(T113, T106, X82, T104, T105)
U8_gaggag(T103, T113, T105, T106, X82, T104, pG_out_ggagg(T113, T106, X82, T104, T105)) → pC_out_gaggag(T103, T113, T105, T106, X82, T104)
U2_gggg(T103, T104, T105, T106, pC_out_gaggag(T103, X81, T105, T106, X82, T104)) → reachA_out_gggg(T103, T104, T105, T106)
MEMBERB_IN_GGG(T79, T80, .(T81, T82)) → MEMBERB_IN_GGG(T79, T80, T82)
MEMBERB_IN_GGG(T79, T80, .(T81, T82)) → MEMBERB_IN_GGG(T79, T80, T82)
From the DPs we obtained the following set of size-change graphs:
REACHA_IN_GGGG(T103, T104, T105, T106) → PC_IN_GAGGAG(T103, X81, T105, T106, X82, T104)
PC_IN_GAGGAG(T103, T113, T105, T106, X82, T104) → U7_GAGGAG(T103, T113, T105, T106, X82, T104, memberD_in_gag(T103, T113, T105))
U7_GAGGAG(T103, T113, T105, T106, X82, T104, memberD_out_gag(T103, T113, T105)) → PG_IN_GGAGG(T113, T106, X82, T104, T105)
PG_IN_GGAGG(T113, T106, X82, T104, T105) → U9_GGAGG(T113, T106, X82, T104, T105, memberE_in_gg(T113, T106))
U9_GGAGG(T113, T106, X82, T104, T105, memberE_out_gg(T113, T106)) → PH_IN_GGAGG(T113, T106, X82, T104, T105)
PH_IN_GGAGG(T113, T106, T185, T104, T105) → U11_GGAGG(T113, T106, T185, T104, T105, deleteF_in_gga(T113, T106, T185))
U11_GGAGG(T113, T106, T185, T104, T105, deleteF_out_gga(T113, T106, T185)) → REACHA_IN_GGGG(T113, T104, T105, T185)
reachA_in_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14) → reachA_out_gggg(T27, T28, .(.(T27, .(T28, [])), T29), T14)
reachA_in_gggg(T46, T47, .(T48, T49), T14) → U1_gggg(T46, T47, T48, T49, T14, memberB_in_ggg(T46, T47, T49))
memberB_in_ggg(T68, T69, .(.(T68, .(T69, [])), T70)) → memberB_out_ggg(T68, T69, .(.(T68, .(T69, [])), T70))
memberB_in_ggg(T79, T80, .(T81, T82)) → U3_ggg(T79, T80, T81, T82, memberB_in_ggg(T79, T80, T82))
U3_ggg(T79, T80, T81, T82, memberB_out_ggg(T79, T80, T82)) → memberB_out_ggg(T79, T80, .(T81, T82))
U1_gggg(T46, T47, T48, T49, T14, memberB_out_ggg(T46, T47, T49)) → reachA_out_gggg(T46, T47, .(T48, T49), T14)
reachA_in_gggg(T103, T104, T105, T106) → U2_gggg(T103, T104, T105, T106, pC_in_gaggag(T103, X81, T105, T106, X82, T104))
pC_in_gaggag(T103, T113, T105, T106, X82, T104) → U7_gaggag(T103, T113, T105, T106, X82, T104, memberD_in_gag(T103, T113, T105))
memberD_in_gag(T132, T133, .(.(T132, .(T133, [])), T134)) → memberD_out_gag(T132, T133, .(.(T132, .(T133, [])), T134))
memberD_in_gag(T141, X121, .(T142, T143)) → U4_gag(T141, X121, T142, T143, memberD_in_gag(T141, X121, T143))
U4_gag(T141, X121, T142, T143, memberD_out_gag(T141, X121, T143)) → memberD_out_gag(T141, X121, .(T142, T143))
U7_gaggag(T103, T113, T105, T106, X82, T104, memberD_out_gag(T103, T113, T105)) → U8_gaggag(T103, T113, T105, T106, X82, T104, pG_in_ggagg(T113, T106, X82, T104, T105))
pG_in_ggagg(T113, T106, X82, T104, T105) → U9_ggagg(T113, T106, X82, T104, T105, memberE_in_gg(T113, T106))
memberE_in_gg(T166, .(T166, T167)) → memberE_out_gg(T166, .(T166, T167))
memberE_in_gg(T174, .(T175, T176)) → U5_gg(T174, T175, T176, memberE_in_gg(T174, T176))
U5_gg(T174, T175, T176, memberE_out_gg(T174, T176)) → memberE_out_gg(T174, .(T175, T176))
U9_ggagg(T113, T106, X82, T104, T105, memberE_out_gg(T113, T106)) → U10_ggagg(T113, T106, X82, T104, T105, pH_in_ggagg(T113, T106, X82, T104, T105))
pH_in_ggagg(T113, T106, T185, T104, T105) → U11_ggagg(T113, T106, T185, T104, T105, deleteF_in_gga(T113, T106, T185))
deleteF_in_gga(T198, .(T198, T199), T199) → deleteF_out_gga(T198, .(T198, T199), T199)
deleteF_in_gga(T206, .(T207, T208), .(T207, X191)) → U6_gga(T206, T207, T208, X191, deleteF_in_gga(T206, T208, X191))
U6_gga(T206, T207, T208, X191, deleteF_out_gga(T206, T208, X191)) → deleteF_out_gga(T206, .(T207, T208), .(T207, X191))
U11_ggagg(T113, T106, T185, T104, T105, deleteF_out_gga(T113, T106, T185)) → U12_ggagg(T113, T106, T185, T104, T105, reachA_in_gggg(T113, T104, T105, T185))
U12_ggagg(T113, T106, T185, T104, T105, reachA_out_gggg(T113, T104, T105, T185)) → pH_out_ggagg(T113, T106, T185, T104, T105)
U10_ggagg(T113, T106, X82, T104, T105, pH_out_ggagg(T113, T106, X82, T104, T105)) → pG_out_ggagg(T113, T106, X82, T104, T105)
U8_gaggag(T103, T113, T105, T106, X82, T104, pG_out_ggagg(T113, T106, X82, T104, T105)) → pC_out_gaggag(T103, T113, T105, T106, X82, T104)
U2_gggg(T103, T104, T105, T106, pC_out_gaggag(T103, X81, T105, T106, X82, T104)) → reachA_out_gggg(T103, T104, T105, T106)
REACHA_IN_GGGG(T103, T104, T105, T106) → PC_IN_GAGGAG(T103, X81, T105, T106, X82, T104)
PC_IN_GAGGAG(T103, T113, T105, T106, X82, T104) → U7_GAGGAG(T103, T113, T105, T106, X82, T104, memberD_in_gag(T103, T113, T105))
U7_GAGGAG(T103, T113, T105, T106, X82, T104, memberD_out_gag(T103, T113, T105)) → PG_IN_GGAGG(T113, T106, X82, T104, T105)
PG_IN_GGAGG(T113, T106, X82, T104, T105) → U9_GGAGG(T113, T106, X82, T104, T105, memberE_in_gg(T113, T106))
U9_GGAGG(T113, T106, X82, T104, T105, memberE_out_gg(T113, T106)) → PH_IN_GGAGG(T113, T106, X82, T104, T105)
PH_IN_GGAGG(T113, T106, T185, T104, T105) → U11_GGAGG(T113, T106, T185, T104, T105, deleteF_in_gga(T113, T106, T185))
U11_GGAGG(T113, T106, T185, T104, T105, deleteF_out_gga(T113, T106, T185)) → REACHA_IN_GGGG(T113, T104, T105, T185)
memberD_in_gag(T132, T133, .(.(T132, .(T133, [])), T134)) → memberD_out_gag(T132, T133, .(.(T132, .(T133, [])), T134))
memberD_in_gag(T141, X121, .(T142, T143)) → U4_gag(T141, X121, T142, T143, memberD_in_gag(T141, X121, T143))
memberE_in_gg(T166, .(T166, T167)) → memberE_out_gg(T166, .(T166, T167))
memberE_in_gg(T174, .(T175, T176)) → U5_gg(T174, T175, T176, memberE_in_gg(T174, T176))
deleteF_in_gga(T198, .(T198, T199), T199) → deleteF_out_gga(T198, .(T198, T199), T199)
deleteF_in_gga(T206, .(T207, T208), .(T207, X191)) → U6_gga(T206, T207, T208, X191, deleteF_in_gga(T206, T208, X191))
U4_gag(T141, X121, T142, T143, memberD_out_gag(T141, X121, T143)) → memberD_out_gag(T141, X121, .(T142, T143))
U5_gg(T174, T175, T176, memberE_out_gg(T174, T176)) → memberE_out_gg(T174, .(T175, T176))
U6_gga(T206, T207, T208, X191, deleteF_out_gga(T206, T208, X191)) → deleteF_out_gga(T206, .(T207, T208), .(T207, X191))
REACHA_IN_GGGG(T103, T104, T105, T106) → PC_IN_GAGGAG(T103, T105, T106, T104)
PC_IN_GAGGAG(T103, T105, T106, T104) → U7_GAGGAG(T103, T105, T106, T104, memberD_in_gag(T103, T105))
U7_GAGGAG(T103, T105, T106, T104, memberD_out_gag(T103, T113, T105)) → PG_IN_GGAGG(T113, T106, T104, T105)
PG_IN_GGAGG(T113, T106, T104, T105) → U9_GGAGG(T113, T106, T104, T105, memberE_in_gg(T113, T106))
U9_GGAGG(T113, T106, T104, T105, memberE_out_gg(T113, T106)) → PH_IN_GGAGG(T113, T106, T104, T105)
PH_IN_GGAGG(T113, T106, T104, T105) → U11_GGAGG(T113, T106, T104, T105, deleteF_in_gga(T113, T106))
U11_GGAGG(T113, T106, T104, T105, deleteF_out_gga(T113, T106, T185)) → REACHA_IN_GGGG(T113, T104, T105, T185)
memberD_in_gag(T132, .(.(T132, .(T133, [])), T134)) → memberD_out_gag(T132, T133, .(.(T132, .(T133, [])), T134))
memberD_in_gag(T141, .(T142, T143)) → U4_gag(T141, T142, T143, memberD_in_gag(T141, T143))
memberE_in_gg(T166, .(T166, T167)) → memberE_out_gg(T166, .(T166, T167))
memberE_in_gg(T174, .(T175, T176)) → U5_gg(T174, T175, T176, memberE_in_gg(T174, T176))
deleteF_in_gga(T198, .(T198, T199)) → deleteF_out_gga(T198, .(T198, T199), T199)
deleteF_in_gga(T206, .(T207, T208)) → U6_gga(T206, T207, T208, deleteF_in_gga(T206, T208))
U4_gag(T141, T142, T143, memberD_out_gag(T141, X121, T143)) → memberD_out_gag(T141, X121, .(T142, T143))
U5_gg(T174, T175, T176, memberE_out_gg(T174, T176)) → memberE_out_gg(T174, .(T175, T176))
U6_gga(T206, T207, T208, deleteF_out_gga(T206, T208, X191)) → deleteF_out_gga(T206, .(T207, T208), .(T207, X191))
memberD_in_gag(x0, x1)
memberE_in_gg(x0, x1)
deleteF_in_gga(x0, x1)
U4_gag(x0, x1, x2, x3)
U5_gg(x0, x1, x2, x3)
U6_gga(x0, x1, x2, x3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PG_IN_GGAGG(T113, T106, T104, T105) → U9_GGAGG(T113, T106, T104, T105, memberE_in_gg(T113, T106))
POL(.(x1, x2)) = 1 + x1 + x2
POL(PC_IN_GAGGAG(x1, x2, x3, x4)) = 1 + x1 + x3
POL(PG_IN_GGAGG(x1, x2, x3, x4)) = 1 + x2
POL(PH_IN_GGAGG(x1, x2, x3, x4)) = x2
POL(REACHA_IN_GGGG(x1, x2, x3, x4)) = 1 + x1 + x4
POL(U11_GGAGG(x1, x2, x3, x4, x5)) = x5
POL(U4_gag(x1, x2, x3, x4)) = x3
POL(U5_gg(x1, x2, x3, x4)) = 0
POL(U6_gga(x1, x2, x3, x4)) = 1 + x2 + x4
POL(U7_GAGGAG(x1, x2, x3, x4, x5)) = 1 + x3
POL(U9_GGAGG(x1, x2, x3, x4, x5)) = x2
POL([]) = 0
POL(deleteF_in_gga(x1, x2)) = x2
POL(deleteF_out_gga(x1, x2, x3)) = 1 + x1 + x3
POL(memberD_in_gag(x1, x2)) = x1 + x2
POL(memberD_out_gag(x1, x2, x3)) = 0
POL(memberE_in_gg(x1, x2)) = 0
POL(memberE_out_gg(x1, x2)) = 0
deleteF_in_gga(T198, .(T198, T199)) → deleteF_out_gga(T198, .(T198, T199), T199)
deleteF_in_gga(T206, .(T207, T208)) → U6_gga(T206, T207, T208, deleteF_in_gga(T206, T208))
U6_gga(T206, T207, T208, deleteF_out_gga(T206, T208, X191)) → deleteF_out_gga(T206, .(T207, T208), .(T207, X191))
REACHA_IN_GGGG(T103, T104, T105, T106) → PC_IN_GAGGAG(T103, T105, T106, T104)
PC_IN_GAGGAG(T103, T105, T106, T104) → U7_GAGGAG(T103, T105, T106, T104, memberD_in_gag(T103, T105))
U7_GAGGAG(T103, T105, T106, T104, memberD_out_gag(T103, T113, T105)) → PG_IN_GGAGG(T113, T106, T104, T105)
U9_GGAGG(T113, T106, T104, T105, memberE_out_gg(T113, T106)) → PH_IN_GGAGG(T113, T106, T104, T105)
PH_IN_GGAGG(T113, T106, T104, T105) → U11_GGAGG(T113, T106, T104, T105, deleteF_in_gga(T113, T106))
U11_GGAGG(T113, T106, T104, T105, deleteF_out_gga(T113, T106, T185)) → REACHA_IN_GGGG(T113, T104, T105, T185)
memberD_in_gag(T132, .(.(T132, .(T133, [])), T134)) → memberD_out_gag(T132, T133, .(.(T132, .(T133, [])), T134))
memberD_in_gag(T141, .(T142, T143)) → U4_gag(T141, T142, T143, memberD_in_gag(T141, T143))
memberE_in_gg(T166, .(T166, T167)) → memberE_out_gg(T166, .(T166, T167))
memberE_in_gg(T174, .(T175, T176)) → U5_gg(T174, T175, T176, memberE_in_gg(T174, T176))
deleteF_in_gga(T198, .(T198, T199)) → deleteF_out_gga(T198, .(T198, T199), T199)
deleteF_in_gga(T206, .(T207, T208)) → U6_gga(T206, T207, T208, deleteF_in_gga(T206, T208))
U4_gag(T141, T142, T143, memberD_out_gag(T141, X121, T143)) → memberD_out_gag(T141, X121, .(T142, T143))
U5_gg(T174, T175, T176, memberE_out_gg(T174, T176)) → memberE_out_gg(T174, .(T175, T176))
U6_gga(T206, T207, T208, deleteF_out_gga(T206, T208, X191)) → deleteF_out_gga(T206, .(T207, T208), .(T207, X191))
memberD_in_gag(x0, x1)
memberE_in_gg(x0, x1)
deleteF_in_gga(x0, x1)
U4_gag(x0, x1, x2, x3)
U5_gg(x0, x1, x2, x3)
U6_gga(x0, x1, x2, x3)