0 Prolog
↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 190 ms)
↳2 PiTRS
↳3 DependencyPairsProof (⇔, 179 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇔, 4 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 QDPOrderProof (⇔, 89 ms)
↳27 QDP
↳28 DependencyGraphProof (⇔, 0 ms)
↳29 TRUE
slowsortA_in_ga([], []) → slowsortA_out_ga([], [])
slowsortA_in_ga(.(T16, .(T17, [])), .(T20, .(T21, []))) → U1_ga(T16, T17, T20, T21, pB_in_aggaa(T20, T16, T17, X22, T21))
pB_in_aggaa(T28, T16, T17, T26, T27) → U7_aggaa(T28, T16, T17, T26, T27, deleteD_in_agga(T28, T16, T17, T26))
deleteD_in_agga(T41, T41, T42, T42) → deleteD_out_agga(T41, T41, T42, T42)
deleteD_in_agga(T57, T55, T56, X59) → U3_agga(T57, T55, T56, X59, deleteC_in_aga(T57, T56, X59))
deleteC_in_aga(T70, .(T70, T71), T71) → deleteC_out_aga(T70, .(T70, T71), T71)
deleteC_in_aga(T81, .(T79, T80), X88) → U2_aga(T81, T79, T80, X88, deleteC_in_aga(T81, T80, X88))
U2_aga(T81, T79, T80, X88, deleteC_out_aga(T81, T80, X88)) → deleteC_out_aga(T81, .(T79, T80), X88)
U3_agga(T57, T55, T56, X59, deleteC_out_aga(T57, T56, X59)) → deleteD_out_agga(T57, T55, T56, X59)
U7_aggaa(T28, T16, T17, T26, T27, deleteD_out_agga(T28, T16, T17, T26)) → U8_aggaa(T28, T16, T17, T26, T27, pK_in_gag(T26, T27, T28))
pK_in_gag(T26, T86, T28) → U9_gag(T26, T86, T28, permE_in_ga(T26, T86))
permE_in_ga([], []) → permE_out_ga([], [])
permE_in_ga(.(T95, .(T96, [])), .(T99, .(T100, []))) → U4_ga(T95, T96, T99, T100, pF_in_aggaa(T99, T95, T96, X106, T100))
pF_in_aggaa(T99, T95, T96, T105, T106) → U11_aggaa(T99, T95, T96, T105, T106, deleteD_in_agga(T99, T95, T96, T105))
U11_aggaa(T99, T95, T96, T105, T106, deleteD_out_agga(T99, T95, T96, T105)) → U12_aggaa(T99, T95, T96, T105, T106, permE_in_ga(T105, T106))
U12_aggaa(T99, T95, T96, T105, T106, permE_out_ga(T105, T106)) → pF_out_aggaa(T99, T95, T96, T105, T106)
U4_ga(T95, T96, T99, T100, pF_out_aggaa(T99, T95, T96, X106, T100)) → permE_out_ga(.(T95, .(T96, [])), .(T99, .(T100, [])))
U9_gag(T26, T86, T28, permE_out_ga(T26, T86)) → U10_gag(T26, T86, T28, sortedH_in_gg(T28, T86))
sortedH_in_gg(T118, T119) → U6_gg(T118, T119, pI_in_gg(T118, T119))
pI_in_gg(T118, T119) → U13_gg(T118, T119, leG_in_gg(T118, T119))
leG_in_gg(s(T132), s(T133)) → U5_gg(T132, T133, leG_in_gg(T132, T133))
leG_in_gg(0, s(T140)) → leG_out_gg(0, s(T140))
leG_in_gg(0, 0) → leG_out_gg(0, 0)
U5_gg(T132, T133, leG_out_gg(T132, T133)) → leG_out_gg(s(T132), s(T133))
U13_gg(T118, T119, leG_out_gg(T118, T119)) → U14_gg(T118, T119, sortedJ_in_g(T119))
sortedJ_in_g(T145) → sortedJ_out_g(T145)
U14_gg(T118, T119, sortedJ_out_g(T119)) → pI_out_gg(T118, T119)
U6_gg(T118, T119, pI_out_gg(T118, T119)) → sortedH_out_gg(T118, T119)
U10_gag(T26, T86, T28, sortedH_out_gg(T28, T86)) → pK_out_gag(T26, T86, T28)
U8_aggaa(T28, T16, T17, T26, T27, pK_out_gag(T26, T27, T28)) → pB_out_aggaa(T28, T16, T17, T26, T27)
U1_ga(T16, T17, T20, T21, pB_out_aggaa(T20, T16, T17, X22, T21)) → slowsortA_out_ga(.(T16, .(T17, [])), .(T20, .(T21, [])))
SLOWSORTA_IN_GA(.(T16, .(T17, [])), .(T20, .(T21, []))) → U1_GA(T16, T17, T20, T21, pB_in_aggaa(T20, T16, T17, X22, T21))
SLOWSORTA_IN_GA(.(T16, .(T17, [])), .(T20, .(T21, []))) → PB_IN_AGGAA(T20, T16, T17, X22, T21)
PB_IN_AGGAA(T28, T16, T17, T26, T27) → U7_AGGAA(T28, T16, T17, T26, T27, deleteD_in_agga(T28, T16, T17, T26))
PB_IN_AGGAA(T28, T16, T17, T26, T27) → DELETED_IN_AGGA(T28, T16, T17, T26)
DELETED_IN_AGGA(T57, T55, T56, X59) → U3_AGGA(T57, T55, T56, X59, deleteC_in_aga(T57, T56, X59))
DELETED_IN_AGGA(T57, T55, T56, X59) → DELETEC_IN_AGA(T57, T56, X59)
DELETEC_IN_AGA(T81, .(T79, T80), X88) → U2_AGA(T81, T79, T80, X88, deleteC_in_aga(T81, T80, X88))
DELETEC_IN_AGA(T81, .(T79, T80), X88) → DELETEC_IN_AGA(T81, T80, X88)
U7_AGGAA(T28, T16, T17, T26, T27, deleteD_out_agga(T28, T16, T17, T26)) → U8_AGGAA(T28, T16, T17, T26, T27, pK_in_gag(T26, T27, T28))
U7_AGGAA(T28, T16, T17, T26, T27, deleteD_out_agga(T28, T16, T17, T26)) → PK_IN_GAG(T26, T27, T28)
PK_IN_GAG(T26, T86, T28) → U9_GAG(T26, T86, T28, permE_in_ga(T26, T86))
PK_IN_GAG(T26, T86, T28) → PERME_IN_GA(T26, T86)
PERME_IN_GA(.(T95, .(T96, [])), .(T99, .(T100, []))) → U4_GA(T95, T96, T99, T100, pF_in_aggaa(T99, T95, T96, X106, T100))
PERME_IN_GA(.(T95, .(T96, [])), .(T99, .(T100, []))) → PF_IN_AGGAA(T99, T95, T96, X106, T100)
PF_IN_AGGAA(T99, T95, T96, T105, T106) → U11_AGGAA(T99, T95, T96, T105, T106, deleteD_in_agga(T99, T95, T96, T105))
PF_IN_AGGAA(T99, T95, T96, T105, T106) → DELETED_IN_AGGA(T99, T95, T96, T105)
U11_AGGAA(T99, T95, T96, T105, T106, deleteD_out_agga(T99, T95, T96, T105)) → U12_AGGAA(T99, T95, T96, T105, T106, permE_in_ga(T105, T106))
U11_AGGAA(T99, T95, T96, T105, T106, deleteD_out_agga(T99, T95, T96, T105)) → PERME_IN_GA(T105, T106)
U9_GAG(T26, T86, T28, permE_out_ga(T26, T86)) → U10_GAG(T26, T86, T28, sortedH_in_gg(T28, T86))
U9_GAG(T26, T86, T28, permE_out_ga(T26, T86)) → SORTEDH_IN_GG(T28, T86)
SORTEDH_IN_GG(T118, T119) → U6_GG(T118, T119, pI_in_gg(T118, T119))
SORTEDH_IN_GG(T118, T119) → PI_IN_GG(T118, T119)
PI_IN_GG(T118, T119) → U13_GG(T118, T119, leG_in_gg(T118, T119))
PI_IN_GG(T118, T119) → LEG_IN_GG(T118, T119)
LEG_IN_GG(s(T132), s(T133)) → U5_GG(T132, T133, leG_in_gg(T132, T133))
LEG_IN_GG(s(T132), s(T133)) → LEG_IN_GG(T132, T133)
U13_GG(T118, T119, leG_out_gg(T118, T119)) → U14_GG(T118, T119, sortedJ_in_g(T119))
U13_GG(T118, T119, leG_out_gg(T118, T119)) → SORTEDJ_IN_G(T119)
slowsortA_in_ga([], []) → slowsortA_out_ga([], [])
slowsortA_in_ga(.(T16, .(T17, [])), .(T20, .(T21, []))) → U1_ga(T16, T17, T20, T21, pB_in_aggaa(T20, T16, T17, X22, T21))
pB_in_aggaa(T28, T16, T17, T26, T27) → U7_aggaa(T28, T16, T17, T26, T27, deleteD_in_agga(T28, T16, T17, T26))
deleteD_in_agga(T41, T41, T42, T42) → deleteD_out_agga(T41, T41, T42, T42)
deleteD_in_agga(T57, T55, T56, X59) → U3_agga(T57, T55, T56, X59, deleteC_in_aga(T57, T56, X59))
deleteC_in_aga(T70, .(T70, T71), T71) → deleteC_out_aga(T70, .(T70, T71), T71)
deleteC_in_aga(T81, .(T79, T80), X88) → U2_aga(T81, T79, T80, X88, deleteC_in_aga(T81, T80, X88))
U2_aga(T81, T79, T80, X88, deleteC_out_aga(T81, T80, X88)) → deleteC_out_aga(T81, .(T79, T80), X88)
U3_agga(T57, T55, T56, X59, deleteC_out_aga(T57, T56, X59)) → deleteD_out_agga(T57, T55, T56, X59)
U7_aggaa(T28, T16, T17, T26, T27, deleteD_out_agga(T28, T16, T17, T26)) → U8_aggaa(T28, T16, T17, T26, T27, pK_in_gag(T26, T27, T28))
pK_in_gag(T26, T86, T28) → U9_gag(T26, T86, T28, permE_in_ga(T26, T86))
permE_in_ga([], []) → permE_out_ga([], [])
permE_in_ga(.(T95, .(T96, [])), .(T99, .(T100, []))) → U4_ga(T95, T96, T99, T100, pF_in_aggaa(T99, T95, T96, X106, T100))
pF_in_aggaa(T99, T95, T96, T105, T106) → U11_aggaa(T99, T95, T96, T105, T106, deleteD_in_agga(T99, T95, T96, T105))
U11_aggaa(T99, T95, T96, T105, T106, deleteD_out_agga(T99, T95, T96, T105)) → U12_aggaa(T99, T95, T96, T105, T106, permE_in_ga(T105, T106))
U12_aggaa(T99, T95, T96, T105, T106, permE_out_ga(T105, T106)) → pF_out_aggaa(T99, T95, T96, T105, T106)
U4_ga(T95, T96, T99, T100, pF_out_aggaa(T99, T95, T96, X106, T100)) → permE_out_ga(.(T95, .(T96, [])), .(T99, .(T100, [])))
U9_gag(T26, T86, T28, permE_out_ga(T26, T86)) → U10_gag(T26, T86, T28, sortedH_in_gg(T28, T86))
sortedH_in_gg(T118, T119) → U6_gg(T118, T119, pI_in_gg(T118, T119))
pI_in_gg(T118, T119) → U13_gg(T118, T119, leG_in_gg(T118, T119))
leG_in_gg(s(T132), s(T133)) → U5_gg(T132, T133, leG_in_gg(T132, T133))
leG_in_gg(0, s(T140)) → leG_out_gg(0, s(T140))
leG_in_gg(0, 0) → leG_out_gg(0, 0)
U5_gg(T132, T133, leG_out_gg(T132, T133)) → leG_out_gg(s(T132), s(T133))
U13_gg(T118, T119, leG_out_gg(T118, T119)) → U14_gg(T118, T119, sortedJ_in_g(T119))
sortedJ_in_g(T145) → sortedJ_out_g(T145)
U14_gg(T118, T119, sortedJ_out_g(T119)) → pI_out_gg(T118, T119)
U6_gg(T118, T119, pI_out_gg(T118, T119)) → sortedH_out_gg(T118, T119)
U10_gag(T26, T86, T28, sortedH_out_gg(T28, T86)) → pK_out_gag(T26, T86, T28)
U8_aggaa(T28, T16, T17, T26, T27, pK_out_gag(T26, T27, T28)) → pB_out_aggaa(T28, T16, T17, T26, T27)
U1_ga(T16, T17, T20, T21, pB_out_aggaa(T20, T16, T17, X22, T21)) → slowsortA_out_ga(.(T16, .(T17, [])), .(T20, .(T21, [])))
SLOWSORTA_IN_GA(.(T16, .(T17, [])), .(T20, .(T21, []))) → U1_GA(T16, T17, T20, T21, pB_in_aggaa(T20, T16, T17, X22, T21))
SLOWSORTA_IN_GA(.(T16, .(T17, [])), .(T20, .(T21, []))) → PB_IN_AGGAA(T20, T16, T17, X22, T21)
PB_IN_AGGAA(T28, T16, T17, T26, T27) → U7_AGGAA(T28, T16, T17, T26, T27, deleteD_in_agga(T28, T16, T17, T26))
PB_IN_AGGAA(T28, T16, T17, T26, T27) → DELETED_IN_AGGA(T28, T16, T17, T26)
DELETED_IN_AGGA(T57, T55, T56, X59) → U3_AGGA(T57, T55, T56, X59, deleteC_in_aga(T57, T56, X59))
DELETED_IN_AGGA(T57, T55, T56, X59) → DELETEC_IN_AGA(T57, T56, X59)
DELETEC_IN_AGA(T81, .(T79, T80), X88) → U2_AGA(T81, T79, T80, X88, deleteC_in_aga(T81, T80, X88))
DELETEC_IN_AGA(T81, .(T79, T80), X88) → DELETEC_IN_AGA(T81, T80, X88)
U7_AGGAA(T28, T16, T17, T26, T27, deleteD_out_agga(T28, T16, T17, T26)) → U8_AGGAA(T28, T16, T17, T26, T27, pK_in_gag(T26, T27, T28))
U7_AGGAA(T28, T16, T17, T26, T27, deleteD_out_agga(T28, T16, T17, T26)) → PK_IN_GAG(T26, T27, T28)
PK_IN_GAG(T26, T86, T28) → U9_GAG(T26, T86, T28, permE_in_ga(T26, T86))
PK_IN_GAG(T26, T86, T28) → PERME_IN_GA(T26, T86)
PERME_IN_GA(.(T95, .(T96, [])), .(T99, .(T100, []))) → U4_GA(T95, T96, T99, T100, pF_in_aggaa(T99, T95, T96, X106, T100))
PERME_IN_GA(.(T95, .(T96, [])), .(T99, .(T100, []))) → PF_IN_AGGAA(T99, T95, T96, X106, T100)
PF_IN_AGGAA(T99, T95, T96, T105, T106) → U11_AGGAA(T99, T95, T96, T105, T106, deleteD_in_agga(T99, T95, T96, T105))
PF_IN_AGGAA(T99, T95, T96, T105, T106) → DELETED_IN_AGGA(T99, T95, T96, T105)
U11_AGGAA(T99, T95, T96, T105, T106, deleteD_out_agga(T99, T95, T96, T105)) → U12_AGGAA(T99, T95, T96, T105, T106, permE_in_ga(T105, T106))
U11_AGGAA(T99, T95, T96, T105, T106, deleteD_out_agga(T99, T95, T96, T105)) → PERME_IN_GA(T105, T106)
U9_GAG(T26, T86, T28, permE_out_ga(T26, T86)) → U10_GAG(T26, T86, T28, sortedH_in_gg(T28, T86))
U9_GAG(T26, T86, T28, permE_out_ga(T26, T86)) → SORTEDH_IN_GG(T28, T86)
SORTEDH_IN_GG(T118, T119) → U6_GG(T118, T119, pI_in_gg(T118, T119))
SORTEDH_IN_GG(T118, T119) → PI_IN_GG(T118, T119)
PI_IN_GG(T118, T119) → U13_GG(T118, T119, leG_in_gg(T118, T119))
PI_IN_GG(T118, T119) → LEG_IN_GG(T118, T119)
LEG_IN_GG(s(T132), s(T133)) → U5_GG(T132, T133, leG_in_gg(T132, T133))
LEG_IN_GG(s(T132), s(T133)) → LEG_IN_GG(T132, T133)
U13_GG(T118, T119, leG_out_gg(T118, T119)) → U14_GG(T118, T119, sortedJ_in_g(T119))
U13_GG(T118, T119, leG_out_gg(T118, T119)) → SORTEDJ_IN_G(T119)
slowsortA_in_ga([], []) → slowsortA_out_ga([], [])
slowsortA_in_ga(.(T16, .(T17, [])), .(T20, .(T21, []))) → U1_ga(T16, T17, T20, T21, pB_in_aggaa(T20, T16, T17, X22, T21))
pB_in_aggaa(T28, T16, T17, T26, T27) → U7_aggaa(T28, T16, T17, T26, T27, deleteD_in_agga(T28, T16, T17, T26))
deleteD_in_agga(T41, T41, T42, T42) → deleteD_out_agga(T41, T41, T42, T42)
deleteD_in_agga(T57, T55, T56, X59) → U3_agga(T57, T55, T56, X59, deleteC_in_aga(T57, T56, X59))
deleteC_in_aga(T70, .(T70, T71), T71) → deleteC_out_aga(T70, .(T70, T71), T71)
deleteC_in_aga(T81, .(T79, T80), X88) → U2_aga(T81, T79, T80, X88, deleteC_in_aga(T81, T80, X88))
U2_aga(T81, T79, T80, X88, deleteC_out_aga(T81, T80, X88)) → deleteC_out_aga(T81, .(T79, T80), X88)
U3_agga(T57, T55, T56, X59, deleteC_out_aga(T57, T56, X59)) → deleteD_out_agga(T57, T55, T56, X59)
U7_aggaa(T28, T16, T17, T26, T27, deleteD_out_agga(T28, T16, T17, T26)) → U8_aggaa(T28, T16, T17, T26, T27, pK_in_gag(T26, T27, T28))
pK_in_gag(T26, T86, T28) → U9_gag(T26, T86, T28, permE_in_ga(T26, T86))
permE_in_ga([], []) → permE_out_ga([], [])
permE_in_ga(.(T95, .(T96, [])), .(T99, .(T100, []))) → U4_ga(T95, T96, T99, T100, pF_in_aggaa(T99, T95, T96, X106, T100))
pF_in_aggaa(T99, T95, T96, T105, T106) → U11_aggaa(T99, T95, T96, T105, T106, deleteD_in_agga(T99, T95, T96, T105))
U11_aggaa(T99, T95, T96, T105, T106, deleteD_out_agga(T99, T95, T96, T105)) → U12_aggaa(T99, T95, T96, T105, T106, permE_in_ga(T105, T106))
U12_aggaa(T99, T95, T96, T105, T106, permE_out_ga(T105, T106)) → pF_out_aggaa(T99, T95, T96, T105, T106)
U4_ga(T95, T96, T99, T100, pF_out_aggaa(T99, T95, T96, X106, T100)) → permE_out_ga(.(T95, .(T96, [])), .(T99, .(T100, [])))
U9_gag(T26, T86, T28, permE_out_ga(T26, T86)) → U10_gag(T26, T86, T28, sortedH_in_gg(T28, T86))
sortedH_in_gg(T118, T119) → U6_gg(T118, T119, pI_in_gg(T118, T119))
pI_in_gg(T118, T119) → U13_gg(T118, T119, leG_in_gg(T118, T119))
leG_in_gg(s(T132), s(T133)) → U5_gg(T132, T133, leG_in_gg(T132, T133))
leG_in_gg(0, s(T140)) → leG_out_gg(0, s(T140))
leG_in_gg(0, 0) → leG_out_gg(0, 0)
U5_gg(T132, T133, leG_out_gg(T132, T133)) → leG_out_gg(s(T132), s(T133))
U13_gg(T118, T119, leG_out_gg(T118, T119)) → U14_gg(T118, T119, sortedJ_in_g(T119))
sortedJ_in_g(T145) → sortedJ_out_g(T145)
U14_gg(T118, T119, sortedJ_out_g(T119)) → pI_out_gg(T118, T119)
U6_gg(T118, T119, pI_out_gg(T118, T119)) → sortedH_out_gg(T118, T119)
U10_gag(T26, T86, T28, sortedH_out_gg(T28, T86)) → pK_out_gag(T26, T86, T28)
U8_aggaa(T28, T16, T17, T26, T27, pK_out_gag(T26, T27, T28)) → pB_out_aggaa(T28, T16, T17, T26, T27)
U1_ga(T16, T17, T20, T21, pB_out_aggaa(T20, T16, T17, X22, T21)) → slowsortA_out_ga(.(T16, .(T17, [])), .(T20, .(T21, [])))
LEG_IN_GG(s(T132), s(T133)) → LEG_IN_GG(T132, T133)
slowsortA_in_ga([], []) → slowsortA_out_ga([], [])
slowsortA_in_ga(.(T16, .(T17, [])), .(T20, .(T21, []))) → U1_ga(T16, T17, T20, T21, pB_in_aggaa(T20, T16, T17, X22, T21))
pB_in_aggaa(T28, T16, T17, T26, T27) → U7_aggaa(T28, T16, T17, T26, T27, deleteD_in_agga(T28, T16, T17, T26))
deleteD_in_agga(T41, T41, T42, T42) → deleteD_out_agga(T41, T41, T42, T42)
deleteD_in_agga(T57, T55, T56, X59) → U3_agga(T57, T55, T56, X59, deleteC_in_aga(T57, T56, X59))
deleteC_in_aga(T70, .(T70, T71), T71) → deleteC_out_aga(T70, .(T70, T71), T71)
deleteC_in_aga(T81, .(T79, T80), X88) → U2_aga(T81, T79, T80, X88, deleteC_in_aga(T81, T80, X88))
U2_aga(T81, T79, T80, X88, deleteC_out_aga(T81, T80, X88)) → deleteC_out_aga(T81, .(T79, T80), X88)
U3_agga(T57, T55, T56, X59, deleteC_out_aga(T57, T56, X59)) → deleteD_out_agga(T57, T55, T56, X59)
U7_aggaa(T28, T16, T17, T26, T27, deleteD_out_agga(T28, T16, T17, T26)) → U8_aggaa(T28, T16, T17, T26, T27, pK_in_gag(T26, T27, T28))
pK_in_gag(T26, T86, T28) → U9_gag(T26, T86, T28, permE_in_ga(T26, T86))
permE_in_ga([], []) → permE_out_ga([], [])
permE_in_ga(.(T95, .(T96, [])), .(T99, .(T100, []))) → U4_ga(T95, T96, T99, T100, pF_in_aggaa(T99, T95, T96, X106, T100))
pF_in_aggaa(T99, T95, T96, T105, T106) → U11_aggaa(T99, T95, T96, T105, T106, deleteD_in_agga(T99, T95, T96, T105))
U11_aggaa(T99, T95, T96, T105, T106, deleteD_out_agga(T99, T95, T96, T105)) → U12_aggaa(T99, T95, T96, T105, T106, permE_in_ga(T105, T106))
U12_aggaa(T99, T95, T96, T105, T106, permE_out_ga(T105, T106)) → pF_out_aggaa(T99, T95, T96, T105, T106)
U4_ga(T95, T96, T99, T100, pF_out_aggaa(T99, T95, T96, X106, T100)) → permE_out_ga(.(T95, .(T96, [])), .(T99, .(T100, [])))
U9_gag(T26, T86, T28, permE_out_ga(T26, T86)) → U10_gag(T26, T86, T28, sortedH_in_gg(T28, T86))
sortedH_in_gg(T118, T119) → U6_gg(T118, T119, pI_in_gg(T118, T119))
pI_in_gg(T118, T119) → U13_gg(T118, T119, leG_in_gg(T118, T119))
leG_in_gg(s(T132), s(T133)) → U5_gg(T132, T133, leG_in_gg(T132, T133))
leG_in_gg(0, s(T140)) → leG_out_gg(0, s(T140))
leG_in_gg(0, 0) → leG_out_gg(0, 0)
U5_gg(T132, T133, leG_out_gg(T132, T133)) → leG_out_gg(s(T132), s(T133))
U13_gg(T118, T119, leG_out_gg(T118, T119)) → U14_gg(T118, T119, sortedJ_in_g(T119))
sortedJ_in_g(T145) → sortedJ_out_g(T145)
U14_gg(T118, T119, sortedJ_out_g(T119)) → pI_out_gg(T118, T119)
U6_gg(T118, T119, pI_out_gg(T118, T119)) → sortedH_out_gg(T118, T119)
U10_gag(T26, T86, T28, sortedH_out_gg(T28, T86)) → pK_out_gag(T26, T86, T28)
U8_aggaa(T28, T16, T17, T26, T27, pK_out_gag(T26, T27, T28)) → pB_out_aggaa(T28, T16, T17, T26, T27)
U1_ga(T16, T17, T20, T21, pB_out_aggaa(T20, T16, T17, X22, T21)) → slowsortA_out_ga(.(T16, .(T17, [])), .(T20, .(T21, [])))
LEG_IN_GG(s(T132), s(T133)) → LEG_IN_GG(T132, T133)
LEG_IN_GG(s(T132), s(T133)) → LEG_IN_GG(T132, T133)
From the DPs we obtained the following set of size-change graphs:
DELETEC_IN_AGA(T81, .(T79, T80), X88) → DELETEC_IN_AGA(T81, T80, X88)
slowsortA_in_ga([], []) → slowsortA_out_ga([], [])
slowsortA_in_ga(.(T16, .(T17, [])), .(T20, .(T21, []))) → U1_ga(T16, T17, T20, T21, pB_in_aggaa(T20, T16, T17, X22, T21))
pB_in_aggaa(T28, T16, T17, T26, T27) → U7_aggaa(T28, T16, T17, T26, T27, deleteD_in_agga(T28, T16, T17, T26))
deleteD_in_agga(T41, T41, T42, T42) → deleteD_out_agga(T41, T41, T42, T42)
deleteD_in_agga(T57, T55, T56, X59) → U3_agga(T57, T55, T56, X59, deleteC_in_aga(T57, T56, X59))
deleteC_in_aga(T70, .(T70, T71), T71) → deleteC_out_aga(T70, .(T70, T71), T71)
deleteC_in_aga(T81, .(T79, T80), X88) → U2_aga(T81, T79, T80, X88, deleteC_in_aga(T81, T80, X88))
U2_aga(T81, T79, T80, X88, deleteC_out_aga(T81, T80, X88)) → deleteC_out_aga(T81, .(T79, T80), X88)
U3_agga(T57, T55, T56, X59, deleteC_out_aga(T57, T56, X59)) → deleteD_out_agga(T57, T55, T56, X59)
U7_aggaa(T28, T16, T17, T26, T27, deleteD_out_agga(T28, T16, T17, T26)) → U8_aggaa(T28, T16, T17, T26, T27, pK_in_gag(T26, T27, T28))
pK_in_gag(T26, T86, T28) → U9_gag(T26, T86, T28, permE_in_ga(T26, T86))
permE_in_ga([], []) → permE_out_ga([], [])
permE_in_ga(.(T95, .(T96, [])), .(T99, .(T100, []))) → U4_ga(T95, T96, T99, T100, pF_in_aggaa(T99, T95, T96, X106, T100))
pF_in_aggaa(T99, T95, T96, T105, T106) → U11_aggaa(T99, T95, T96, T105, T106, deleteD_in_agga(T99, T95, T96, T105))
U11_aggaa(T99, T95, T96, T105, T106, deleteD_out_agga(T99, T95, T96, T105)) → U12_aggaa(T99, T95, T96, T105, T106, permE_in_ga(T105, T106))
U12_aggaa(T99, T95, T96, T105, T106, permE_out_ga(T105, T106)) → pF_out_aggaa(T99, T95, T96, T105, T106)
U4_ga(T95, T96, T99, T100, pF_out_aggaa(T99, T95, T96, X106, T100)) → permE_out_ga(.(T95, .(T96, [])), .(T99, .(T100, [])))
U9_gag(T26, T86, T28, permE_out_ga(T26, T86)) → U10_gag(T26, T86, T28, sortedH_in_gg(T28, T86))
sortedH_in_gg(T118, T119) → U6_gg(T118, T119, pI_in_gg(T118, T119))
pI_in_gg(T118, T119) → U13_gg(T118, T119, leG_in_gg(T118, T119))
leG_in_gg(s(T132), s(T133)) → U5_gg(T132, T133, leG_in_gg(T132, T133))
leG_in_gg(0, s(T140)) → leG_out_gg(0, s(T140))
leG_in_gg(0, 0) → leG_out_gg(0, 0)
U5_gg(T132, T133, leG_out_gg(T132, T133)) → leG_out_gg(s(T132), s(T133))
U13_gg(T118, T119, leG_out_gg(T118, T119)) → U14_gg(T118, T119, sortedJ_in_g(T119))
sortedJ_in_g(T145) → sortedJ_out_g(T145)
U14_gg(T118, T119, sortedJ_out_g(T119)) → pI_out_gg(T118, T119)
U6_gg(T118, T119, pI_out_gg(T118, T119)) → sortedH_out_gg(T118, T119)
U10_gag(T26, T86, T28, sortedH_out_gg(T28, T86)) → pK_out_gag(T26, T86, T28)
U8_aggaa(T28, T16, T17, T26, T27, pK_out_gag(T26, T27, T28)) → pB_out_aggaa(T28, T16, T17, T26, T27)
U1_ga(T16, T17, T20, T21, pB_out_aggaa(T20, T16, T17, X22, T21)) → slowsortA_out_ga(.(T16, .(T17, [])), .(T20, .(T21, [])))
DELETEC_IN_AGA(T81, .(T79, T80), X88) → DELETEC_IN_AGA(T81, T80, X88)
DELETEC_IN_AGA(.(T79, T80)) → DELETEC_IN_AGA(T80)
From the DPs we obtained the following set of size-change graphs:
PF_IN_AGGAA(T99, T95, T96, T105, T106) → U11_AGGAA(T99, T95, T96, T105, T106, deleteD_in_agga(T99, T95, T96, T105))
U11_AGGAA(T99, T95, T96, T105, T106, deleteD_out_agga(T99, T95, T96, T105)) → PERME_IN_GA(T105, T106)
PERME_IN_GA(.(T95, .(T96, [])), .(T99, .(T100, []))) → PF_IN_AGGAA(T99, T95, T96, X106, T100)
slowsortA_in_ga([], []) → slowsortA_out_ga([], [])
slowsortA_in_ga(.(T16, .(T17, [])), .(T20, .(T21, []))) → U1_ga(T16, T17, T20, T21, pB_in_aggaa(T20, T16, T17, X22, T21))
pB_in_aggaa(T28, T16, T17, T26, T27) → U7_aggaa(T28, T16, T17, T26, T27, deleteD_in_agga(T28, T16, T17, T26))
deleteD_in_agga(T41, T41, T42, T42) → deleteD_out_agga(T41, T41, T42, T42)
deleteD_in_agga(T57, T55, T56, X59) → U3_agga(T57, T55, T56, X59, deleteC_in_aga(T57, T56, X59))
deleteC_in_aga(T70, .(T70, T71), T71) → deleteC_out_aga(T70, .(T70, T71), T71)
deleteC_in_aga(T81, .(T79, T80), X88) → U2_aga(T81, T79, T80, X88, deleteC_in_aga(T81, T80, X88))
U2_aga(T81, T79, T80, X88, deleteC_out_aga(T81, T80, X88)) → deleteC_out_aga(T81, .(T79, T80), X88)
U3_agga(T57, T55, T56, X59, deleteC_out_aga(T57, T56, X59)) → deleteD_out_agga(T57, T55, T56, X59)
U7_aggaa(T28, T16, T17, T26, T27, deleteD_out_agga(T28, T16, T17, T26)) → U8_aggaa(T28, T16, T17, T26, T27, pK_in_gag(T26, T27, T28))
pK_in_gag(T26, T86, T28) → U9_gag(T26, T86, T28, permE_in_ga(T26, T86))
permE_in_ga([], []) → permE_out_ga([], [])
permE_in_ga(.(T95, .(T96, [])), .(T99, .(T100, []))) → U4_ga(T95, T96, T99, T100, pF_in_aggaa(T99, T95, T96, X106, T100))
pF_in_aggaa(T99, T95, T96, T105, T106) → U11_aggaa(T99, T95, T96, T105, T106, deleteD_in_agga(T99, T95, T96, T105))
U11_aggaa(T99, T95, T96, T105, T106, deleteD_out_agga(T99, T95, T96, T105)) → U12_aggaa(T99, T95, T96, T105, T106, permE_in_ga(T105, T106))
U12_aggaa(T99, T95, T96, T105, T106, permE_out_ga(T105, T106)) → pF_out_aggaa(T99, T95, T96, T105, T106)
U4_ga(T95, T96, T99, T100, pF_out_aggaa(T99, T95, T96, X106, T100)) → permE_out_ga(.(T95, .(T96, [])), .(T99, .(T100, [])))
U9_gag(T26, T86, T28, permE_out_ga(T26, T86)) → U10_gag(T26, T86, T28, sortedH_in_gg(T28, T86))
sortedH_in_gg(T118, T119) → U6_gg(T118, T119, pI_in_gg(T118, T119))
pI_in_gg(T118, T119) → U13_gg(T118, T119, leG_in_gg(T118, T119))
leG_in_gg(s(T132), s(T133)) → U5_gg(T132, T133, leG_in_gg(T132, T133))
leG_in_gg(0, s(T140)) → leG_out_gg(0, s(T140))
leG_in_gg(0, 0) → leG_out_gg(0, 0)
U5_gg(T132, T133, leG_out_gg(T132, T133)) → leG_out_gg(s(T132), s(T133))
U13_gg(T118, T119, leG_out_gg(T118, T119)) → U14_gg(T118, T119, sortedJ_in_g(T119))
sortedJ_in_g(T145) → sortedJ_out_g(T145)
U14_gg(T118, T119, sortedJ_out_g(T119)) → pI_out_gg(T118, T119)
U6_gg(T118, T119, pI_out_gg(T118, T119)) → sortedH_out_gg(T118, T119)
U10_gag(T26, T86, T28, sortedH_out_gg(T28, T86)) → pK_out_gag(T26, T86, T28)
U8_aggaa(T28, T16, T17, T26, T27, pK_out_gag(T26, T27, T28)) → pB_out_aggaa(T28, T16, T17, T26, T27)
U1_ga(T16, T17, T20, T21, pB_out_aggaa(T20, T16, T17, X22, T21)) → slowsortA_out_ga(.(T16, .(T17, [])), .(T20, .(T21, [])))
PF_IN_AGGAA(T99, T95, T96, T105, T106) → U11_AGGAA(T99, T95, T96, T105, T106, deleteD_in_agga(T99, T95, T96, T105))
U11_AGGAA(T99, T95, T96, T105, T106, deleteD_out_agga(T99, T95, T96, T105)) → PERME_IN_GA(T105, T106)
PERME_IN_GA(.(T95, .(T96, [])), .(T99, .(T100, []))) → PF_IN_AGGAA(T99, T95, T96, X106, T100)
deleteD_in_agga(T41, T41, T42, T42) → deleteD_out_agga(T41, T41, T42, T42)
deleteD_in_agga(T57, T55, T56, X59) → U3_agga(T57, T55, T56, X59, deleteC_in_aga(T57, T56, X59))
U3_agga(T57, T55, T56, X59, deleteC_out_aga(T57, T56, X59)) → deleteD_out_agga(T57, T55, T56, X59)
deleteC_in_aga(T70, .(T70, T71), T71) → deleteC_out_aga(T70, .(T70, T71), T71)
deleteC_in_aga(T81, .(T79, T80), X88) → U2_aga(T81, T79, T80, X88, deleteC_in_aga(T81, T80, X88))
U2_aga(T81, T79, T80, X88, deleteC_out_aga(T81, T80, X88)) → deleteC_out_aga(T81, .(T79, T80), X88)
PF_IN_AGGAA(T95, T96) → U11_AGGAA(T95, T96, deleteD_in_agga(T95, T96))
U11_AGGAA(T95, T96, deleteD_out_agga(T99, T95, T96, T105)) → PERME_IN_GA(T105)
PERME_IN_GA(.(T95, .(T96, []))) → PF_IN_AGGAA(T95, T96)
deleteD_in_agga(T41, T42) → deleteD_out_agga(T41, T41, T42, T42)
deleteD_in_agga(T55, T56) → U3_agga(T55, T56, deleteC_in_aga(T56))
U3_agga(T55, T56, deleteC_out_aga(T57, T56, X59)) → deleteD_out_agga(T57, T55, T56, X59)
deleteC_in_aga(.(T70, T71)) → deleteC_out_aga(T70, .(T70, T71), T71)
deleteC_in_aga(.(T79, T80)) → U2_aga(T79, T80, deleteC_in_aga(T80))
U2_aga(T79, T80, deleteC_out_aga(T81, T80, X88)) → deleteC_out_aga(T81, .(T79, T80), X88)
deleteD_in_agga(x0, x1)
U3_agga(x0, x1, x2)
deleteC_in_aga(x0)
U2_aga(x0, x1, x2)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
PERME_IN_GA(.(T95, .(T96, []))) → PF_IN_AGGAA(T95, T96)
POL(.(x1, x2)) = 1 + x1 + x2
POL(PERME_IN_GA(x1)) = x1
POL(PF_IN_AGGAA(x1, x2)) = x2
POL(U11_AGGAA(x1, x2, x3)) = x3
POL(U2_aga(x1, x2, x3)) = x3
POL(U3_agga(x1, x2, x3)) = x3
POL([]) = 1
POL(deleteC_in_aga(x1)) = x1
POL(deleteC_out_aga(x1, x2, x3)) = x3
POL(deleteD_in_agga(x1, x2)) = x2
POL(deleteD_out_agga(x1, x2, x3, x4)) = x4
deleteD_in_agga(T41, T42) → deleteD_out_agga(T41, T41, T42, T42)
deleteD_in_agga(T55, T56) → U3_agga(T55, T56, deleteC_in_aga(T56))
deleteC_in_aga(.(T70, T71)) → deleteC_out_aga(T70, .(T70, T71), T71)
deleteC_in_aga(.(T79, T80)) → U2_aga(T79, T80, deleteC_in_aga(T80))
U3_agga(T55, T56, deleteC_out_aga(T57, T56, X59)) → deleteD_out_agga(T57, T55, T56, X59)
U2_aga(T79, T80, deleteC_out_aga(T81, T80, X88)) → deleteC_out_aga(T81, .(T79, T80), X88)
PF_IN_AGGAA(T95, T96) → U11_AGGAA(T95, T96, deleteD_in_agga(T95, T96))
U11_AGGAA(T95, T96, deleteD_out_agga(T99, T95, T96, T105)) → PERME_IN_GA(T105)
deleteD_in_agga(T41, T42) → deleteD_out_agga(T41, T41, T42, T42)
deleteD_in_agga(T55, T56) → U3_agga(T55, T56, deleteC_in_aga(T56))
U3_agga(T55, T56, deleteC_out_aga(T57, T56, X59)) → deleteD_out_agga(T57, T55, T56, X59)
deleteC_in_aga(.(T70, T71)) → deleteC_out_aga(T70, .(T70, T71), T71)
deleteC_in_aga(.(T79, T80)) → U2_aga(T79, T80, deleteC_in_aga(T80))
U2_aga(T79, T80, deleteC_out_aga(T81, T80, X88)) → deleteC_out_aga(T81, .(T79, T80), X88)
deleteD_in_agga(x0, x1)
U3_agga(x0, x1, x2)
deleteC_in_aga(x0)
U2_aga(x0, x1, x2)