(0) Obligation:

Clauses:

mergesort([], []).
mergesort(.(E, []), .(E, [])).
mergesort(.(E, .(F, U)), V) :- ','(split(.(E, .(F, U)), W, Y), ','(mergesort(W, X), ','(mergesort(Y, Z), merge(X, Z, V)))).
merge(X, [], X).
merge([], X, X).
merge(.(A, X), .(B, Y), .(A, Z)) :- ','(le(A, B), merge(X, .(B, Y), Z)).
merge(.(A, X), .(B, Y), .(B, Z)) :- ','(gt(A, B), merge(.(A, X), Y, Z)).
split([], [], []).
split(.(E, U), .(E, V), W) :- split(U, W, V).
gt(s(X), s(Y)) :- gt(X, Y).
gt(s(X), 0).
le(s(X), s(Y)) :- le(X, Y).
le(0, s(Y)).
le(0, 0).

Query: mergesort(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

(2) Obligation:

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

mergesortA_in_ga([], []) → mergesortA_out_ga([], [])
mergesortA_in_ga(.(T4, []), .(T4, [])) → mergesortA_out_ga(.(T4, []), .(T4, []))
mergesortA_in_ga(.(T21, .(T22, T23)), T14) → U1_ga(T21, T22, T23, T14, pB_in_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14))
pB_in_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14) → U9_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_in_ggaa(T22, T23, T24, T25))
splitD_in_ggaa(T30, T31, .(T30, X58), X59) → U3_ggaa(T30, T31, X58, X59, splitC_in_gaa(T31, X59, X58))
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37), .(T36, X76), X77) → U2_gaa(T36, T37, X76, X77, splitC_in_gaa(T37, X77, X76))
U2_gaa(T36, T37, X76, X77, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U3_ggaa(T30, T31, X58, X59, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U9_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → U10_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pL_in_ggagaa(T21, T25, X22, T24, X23, T14))
pL_in_ggagaa(T21, T25, T38, T24, X23, T14) → U11_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_in_ga(.(T21, T25), T38))
U11_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_out_ga(.(T21, T25), T38)) → U12_ggagaa(T21, T25, T38, T24, X23, T14, pM_in_gaga(T24, X23, T38, T14))
pM_in_gaga(T24, T39, T38, T14) → U13_gaga(T24, T39, T38, T14, mergesortE_in_ga(T24, T39))
mergesortE_in_ga([], []) → mergesortE_out_ga([], [])
mergesortE_in_ga(.(T44, []), .(T44, [])) → mergesortE_out_ga(.(T44, []), .(T44, []))
mergesortE_in_ga(.(T51, .(T52, T53)), X105) → U4_ga(T51, T52, T53, X105, pF_in_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105))
pF_in_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105) → U15_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_in_ggaa(T51, .(T52, T53), T54, T55))
U15_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U16_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pN_in_gagaa(T54, X103, T55, X104, X105))
pN_in_gagaa(T54, T56, T55, X104, X105) → U17_gagaa(T54, T56, T55, X104, X105, mergesortE_in_ga(T54, T56))
U17_gagaa(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → U18_gagaa(T54, T56, T55, X104, X105, pO_in_gaga(T55, X104, T56, X105))
pO_in_gaga(T55, T57, T56, X105) → U19_gaga(T55, T57, T56, X105, mergesortE_in_ga(T55, T57))
U19_gaga(T55, T57, T56, X105, mergesortE_out_ga(T55, T57)) → U20_gaga(T55, T57, T56, X105, mergeG_in_gga(T56, T57, X105))
mergeG_in_gga(T66, [], T66) → mergeG_out_gga(T66, [], T66)
mergeG_in_gga([], T71, T71) → mergeG_out_gga([], T71, T71)
mergeG_in_gga(.(T92, T93), .(T94, T95), .(T92, T97)) → U5_gga(T92, T93, T94, T95, T97, pH_in_gggga(T92, T94, T93, T95, T97))
pH_in_gggga(T92, T94, T93, T95, T97) → U21_gggga(T92, T94, T93, T95, T97, leJ_in_gg(T92, T94))
leJ_in_gg(s(T110), s(T111)) → U7_gg(T110, T111, leJ_in_gg(T110, T111))
leJ_in_gg(0, s(T118)) → leJ_out_gg(0, s(T118))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U7_gg(T110, T111, leJ_out_gg(T110, T111)) → leJ_out_gg(s(T110), s(T111))
U21_gggga(T92, T94, T93, T95, T97, leJ_out_gg(T92, T94)) → U22_gggga(T92, T94, T93, T95, T97, mergeG_in_gga(T93, .(T94, T95), T97))
mergeG_in_gga(.(T131, T132), .(T133, T134), .(T133, T136)) → U6_gga(T131, T132, T133, T134, T136, pI_in_gggga(T131, T133, T132, T134, T136))
pI_in_gggga(T131, T133, T132, T134, T136) → U23_gggga(T131, T133, T132, T134, T136, gtK_in_gg(T131, T133))
gtK_in_gg(s(T149), s(T150)) → U8_gg(T149, T150, gtK_in_gg(T149, T150))
gtK_in_gg(s(T155), 0) → gtK_out_gg(s(T155), 0)
U8_gg(T149, T150, gtK_out_gg(T149, T150)) → gtK_out_gg(s(T149), s(T150))
U23_gggga(T131, T133, T132, T134, T136, gtK_out_gg(T131, T133)) → U24_gggga(T131, T133, T132, T134, T136, mergeG_in_gga(.(T131, T132), T134, T136))
U24_gggga(T131, T133, T132, T134, T136, mergeG_out_gga(.(T131, T132), T134, T136)) → pI_out_gggga(T131, T133, T132, T134, T136)
U6_gga(T131, T132, T133, T134, T136, pI_out_gggga(T131, T133, T132, T134, T136)) → mergeG_out_gga(.(T131, T132), .(T133, T134), .(T133, T136))
U22_gggga(T92, T94, T93, T95, T97, mergeG_out_gga(T93, .(T94, T95), T97)) → pH_out_gggga(T92, T94, T93, T95, T97)
U5_gga(T92, T93, T94, T95, T97, pH_out_gggga(T92, T94, T93, T95, T97)) → mergeG_out_gga(.(T92, T93), .(T94, T95), .(T92, T97))
U20_gaga(T55, T57, T56, X105, mergeG_out_gga(T56, T57, X105)) → pO_out_gaga(T55, T57, T56, X105)
U18_gagaa(T54, T56, T55, X104, X105, pO_out_gaga(T55, X104, T56, X105)) → pN_out_gagaa(T54, T56, T55, X104, X105)
U16_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pN_out_gagaa(T54, X103, T55, X104, X105)) → pF_out_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105)
U4_ga(T51, T52, T53, X105, pF_out_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105)) → mergesortE_out_ga(.(T51, .(T52, T53)), X105)
U13_gaga(T24, T39, T38, T14, mergesortE_out_ga(T24, T39)) → U14_gaga(T24, T39, T38, T14, mergeG_in_gga(T38, T39, T14))
U14_gaga(T24, T39, T38, T14, mergeG_out_gga(T38, T39, T14)) → pM_out_gaga(T24, T39, T38, T14)
U12_ggagaa(T21, T25, T38, T24, X23, T14, pM_out_gaga(T24, X23, T38, T14)) → pL_out_ggagaa(T21, T25, T38, T24, X23, T14)
U10_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pL_out_ggagaa(T21, T25, X22, T24, X23, T14)) → pB_out_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14)
U1_ga(T21, T22, T23, T14, pB_out_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14)) → mergesortA_out_ga(.(T21, .(T22, T23)), T14)

The argument filtering Pi contains the following mapping:
mergesortA_in_ga(x1, x2)  =  mergesortA_in_ga(x1)
[]  =  []
mergesortA_out_ga(x1, x2)  =  mergesortA_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
pB_in_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pB_in_ggaagaaa(x1, x2, x5)
U9_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U9_ggaagaaa(x1, x2, x5, x9)
splitD_in_ggaa(x1, x2, x3, x4)  =  splitD_in_ggaa(x1, x2)
U3_ggaa(x1, x2, x3, x4, x5)  =  U3_ggaa(x1, x2, x5)
splitC_in_gaa(x1, x2, x3)  =  splitC_in_gaa(x1)
splitC_out_gaa(x1, x2, x3)  =  splitC_out_gaa(x1, x2, x3)
U2_gaa(x1, x2, x3, x4, x5)  =  U2_gaa(x1, x2, x5)
splitD_out_ggaa(x1, x2, x3, x4)  =  splitD_out_ggaa(x1, x2, x3, x4)
U10_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U10_ggaagaaa(x1, x2, x3, x4, x5, x9)
pL_in_ggagaa(x1, x2, x3, x4, x5, x6)  =  pL_in_ggagaa(x1, x2, x4)
U11_ggagaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_ggagaa(x1, x2, x4, x7)
U12_ggagaa(x1, x2, x3, x4, x5, x6, x7)  =  U12_ggagaa(x1, x2, x3, x4, x7)
pM_in_gaga(x1, x2, x3, x4)  =  pM_in_gaga(x1, x3)
U13_gaga(x1, x2, x3, x4, x5)  =  U13_gaga(x1, x3, x5)
mergesortE_in_ga(x1, x2)  =  mergesortE_in_ga(x1)
mergesortE_out_ga(x1, x2)  =  mergesortE_out_ga(x1, x2)
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x2, x3, x5)
pF_in_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pF_in_gggaaaaa(x1, x2, x3)
U15_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U15_gggaaaaa(x1, x2, x3, x9)
U16_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U16_gggaaaaa(x1, x2, x3, x4, x5, x9)
pN_in_gagaa(x1, x2, x3, x4, x5)  =  pN_in_gagaa(x1, x3)
U17_gagaa(x1, x2, x3, x4, x5, x6)  =  U17_gagaa(x1, x3, x6)
U18_gagaa(x1, x2, x3, x4, x5, x6)  =  U18_gagaa(x1, x2, x3, x6)
pO_in_gaga(x1, x2, x3, x4)  =  pO_in_gaga(x1, x3)
U19_gaga(x1, x2, x3, x4, x5)  =  U19_gaga(x1, x3, x5)
U20_gaga(x1, x2, x3, x4, x5)  =  U20_gaga(x1, x2, x3, x5)
mergeG_in_gga(x1, x2, x3)  =  mergeG_in_gga(x1, x2)
mergeG_out_gga(x1, x2, x3)  =  mergeG_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4, x5, x6)  =  U5_gga(x1, x2, x3, x4, x6)
pH_in_gggga(x1, x2, x3, x4, x5)  =  pH_in_gggga(x1, x2, x3, x4)
U21_gggga(x1, x2, x3, x4, x5, x6)  =  U21_gggga(x1, x2, x3, x4, x6)
leJ_in_gg(x1, x2)  =  leJ_in_gg(x1, x2)
s(x1)  =  s(x1)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
0  =  0
leJ_out_gg(x1, x2)  =  leJ_out_gg(x1, x2)
U22_gggga(x1, x2, x3, x4, x5, x6)  =  U22_gggga(x1, x2, x3, x4, x6)
U6_gga(x1, x2, x3, x4, x5, x6)  =  U6_gga(x1, x2, x3, x4, x6)
pI_in_gggga(x1, x2, x3, x4, x5)  =  pI_in_gggga(x1, x2, x3, x4)
U23_gggga(x1, x2, x3, x4, x5, x6)  =  U23_gggga(x1, x2, x3, x4, x6)
gtK_in_gg(x1, x2)  =  gtK_in_gg(x1, x2)
U8_gg(x1, x2, x3)  =  U8_gg(x1, x2, x3)
gtK_out_gg(x1, x2)  =  gtK_out_gg(x1, x2)
U24_gggga(x1, x2, x3, x4, x5, x6)  =  U24_gggga(x1, x2, x3, x4, x6)
pI_out_gggga(x1, x2, x3, x4, x5)  =  pI_out_gggga(x1, x2, x3, x4, x5)
pH_out_gggga(x1, x2, x3, x4, x5)  =  pH_out_gggga(x1, x2, x3, x4, x5)
pO_out_gaga(x1, x2, x3, x4)  =  pO_out_gaga(x1, x2, x3, x4)
pN_out_gagaa(x1, x2, x3, x4, x5)  =  pN_out_gagaa(x1, x2, x3, x4, x5)
pF_out_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pF_out_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)
U14_gaga(x1, x2, x3, x4, x5)  =  U14_gaga(x1, x2, x3, x5)
pM_out_gaga(x1, x2, x3, x4)  =  pM_out_gaga(x1, x2, x3, x4)
pL_out_ggagaa(x1, x2, x3, x4, x5, x6)  =  pL_out_ggagaa(x1, x2, x3, x4, x5, x6)
pB_out_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pB_out_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

MERGESORTA_IN_GA(.(T21, .(T22, T23)), T14) → U1_GA(T21, T22, T23, T14, pB_in_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14))
MERGESORTA_IN_GA(.(T21, .(T22, T23)), T14) → PB_IN_GGAAGAAA(T22, T23, X41, X40, T21, X22, X23, T14)
PB_IN_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14) → U9_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14, splitD_in_ggaa(T22, T23, T24, T25))
PB_IN_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14) → SPLITD_IN_GGAA(T22, T23, T24, T25)
SPLITD_IN_GGAA(T30, T31, .(T30, X58), X59) → U3_GGAA(T30, T31, X58, X59, splitC_in_gaa(T31, X59, X58))
SPLITD_IN_GGAA(T30, T31, .(T30, X58), X59) → SPLITC_IN_GAA(T31, X59, X58)
SPLITC_IN_GAA(.(T36, T37), .(T36, X76), X77) → U2_GAA(T36, T37, X76, X77, splitC_in_gaa(T37, X77, X76))
SPLITC_IN_GAA(.(T36, T37), .(T36, X76), X77) → SPLITC_IN_GAA(T37, X77, X76)
U9_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → U10_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14, pL_in_ggagaa(T21, T25, X22, T24, X23, T14))
U9_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → PL_IN_GGAGAA(T21, T25, X22, T24, X23, T14)
PL_IN_GGAGAA(T21, T25, T38, T24, X23, T14) → U11_GGAGAA(T21, T25, T38, T24, X23, T14, mergesortA_in_ga(.(T21, T25), T38))
PL_IN_GGAGAA(T21, T25, T38, T24, X23, T14) → MERGESORTA_IN_GA(.(T21, T25), T38)
U11_GGAGAA(T21, T25, T38, T24, X23, T14, mergesortA_out_ga(.(T21, T25), T38)) → U12_GGAGAA(T21, T25, T38, T24, X23, T14, pM_in_gaga(T24, X23, T38, T14))
U11_GGAGAA(T21, T25, T38, T24, X23, T14, mergesortA_out_ga(.(T21, T25), T38)) → PM_IN_GAGA(T24, X23, T38, T14)
PM_IN_GAGA(T24, T39, T38, T14) → U13_GAGA(T24, T39, T38, T14, mergesortE_in_ga(T24, T39))
PM_IN_GAGA(T24, T39, T38, T14) → MERGESORTE_IN_GA(T24, T39)
MERGESORTE_IN_GA(.(T51, .(T52, T53)), X105) → U4_GA(T51, T52, T53, X105, pF_in_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105))
MERGESORTE_IN_GA(.(T51, .(T52, T53)), X105) → PF_IN_GGGAAAAA(T51, T52, T53, X101, X102, X103, X104, X105)
PF_IN_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105) → U15_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105, splitD_in_ggaa(T51, .(T52, T53), T54, T55))
PF_IN_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105) → SPLITD_IN_GGAA(T51, .(T52, T53), T54, T55)
U15_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U16_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105, pN_in_gagaa(T54, X103, T55, X104, X105))
U15_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → PN_IN_GAGAA(T54, X103, T55, X104, X105)
PN_IN_GAGAA(T54, T56, T55, X104, X105) → U17_GAGAA(T54, T56, T55, X104, X105, mergesortE_in_ga(T54, T56))
PN_IN_GAGAA(T54, T56, T55, X104, X105) → MERGESORTE_IN_GA(T54, T56)
U17_GAGAA(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → U18_GAGAA(T54, T56, T55, X104, X105, pO_in_gaga(T55, X104, T56, X105))
U17_GAGAA(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → PO_IN_GAGA(T55, X104, T56, X105)
PO_IN_GAGA(T55, T57, T56, X105) → U19_GAGA(T55, T57, T56, X105, mergesortE_in_ga(T55, T57))
PO_IN_GAGA(T55, T57, T56, X105) → MERGESORTE_IN_GA(T55, T57)
U19_GAGA(T55, T57, T56, X105, mergesortE_out_ga(T55, T57)) → U20_GAGA(T55, T57, T56, X105, mergeG_in_gga(T56, T57, X105))
U19_GAGA(T55, T57, T56, X105, mergesortE_out_ga(T55, T57)) → MERGEG_IN_GGA(T56, T57, X105)
MERGEG_IN_GGA(.(T92, T93), .(T94, T95), .(T92, T97)) → U5_GGA(T92, T93, T94, T95, T97, pH_in_gggga(T92, T94, T93, T95, T97))
MERGEG_IN_GGA(.(T92, T93), .(T94, T95), .(T92, T97)) → PH_IN_GGGGA(T92, T94, T93, T95, T97)
PH_IN_GGGGA(T92, T94, T93, T95, T97) → U21_GGGGA(T92, T94, T93, T95, T97, leJ_in_gg(T92, T94))
PH_IN_GGGGA(T92, T94, T93, T95, T97) → LEJ_IN_GG(T92, T94)
LEJ_IN_GG(s(T110), s(T111)) → U7_GG(T110, T111, leJ_in_gg(T110, T111))
LEJ_IN_GG(s(T110), s(T111)) → LEJ_IN_GG(T110, T111)
U21_GGGGA(T92, T94, T93, T95, T97, leJ_out_gg(T92, T94)) → U22_GGGGA(T92, T94, T93, T95, T97, mergeG_in_gga(T93, .(T94, T95), T97))
U21_GGGGA(T92, T94, T93, T95, T97, leJ_out_gg(T92, T94)) → MERGEG_IN_GGA(T93, .(T94, T95), T97)
MERGEG_IN_GGA(.(T131, T132), .(T133, T134), .(T133, T136)) → U6_GGA(T131, T132, T133, T134, T136, pI_in_gggga(T131, T133, T132, T134, T136))
MERGEG_IN_GGA(.(T131, T132), .(T133, T134), .(T133, T136)) → PI_IN_GGGGA(T131, T133, T132, T134, T136)
PI_IN_GGGGA(T131, T133, T132, T134, T136) → U23_GGGGA(T131, T133, T132, T134, T136, gtK_in_gg(T131, T133))
PI_IN_GGGGA(T131, T133, T132, T134, T136) → GTK_IN_GG(T131, T133)
GTK_IN_GG(s(T149), s(T150)) → U8_GG(T149, T150, gtK_in_gg(T149, T150))
GTK_IN_GG(s(T149), s(T150)) → GTK_IN_GG(T149, T150)
U23_GGGGA(T131, T133, T132, T134, T136, gtK_out_gg(T131, T133)) → U24_GGGGA(T131, T133, T132, T134, T136, mergeG_in_gga(.(T131, T132), T134, T136))
U23_GGGGA(T131, T133, T132, T134, T136, gtK_out_gg(T131, T133)) → MERGEG_IN_GGA(.(T131, T132), T134, T136)
U13_GAGA(T24, T39, T38, T14, mergesortE_out_ga(T24, T39)) → U14_GAGA(T24, T39, T38, T14, mergeG_in_gga(T38, T39, T14))
U13_GAGA(T24, T39, T38, T14, mergesortE_out_ga(T24, T39)) → MERGEG_IN_GGA(T38, T39, T14)

The TRS R consists of the following rules:

mergesortA_in_ga([], []) → mergesortA_out_ga([], [])
mergesortA_in_ga(.(T4, []), .(T4, [])) → mergesortA_out_ga(.(T4, []), .(T4, []))
mergesortA_in_ga(.(T21, .(T22, T23)), T14) → U1_ga(T21, T22, T23, T14, pB_in_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14))
pB_in_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14) → U9_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_in_ggaa(T22, T23, T24, T25))
splitD_in_ggaa(T30, T31, .(T30, X58), X59) → U3_ggaa(T30, T31, X58, X59, splitC_in_gaa(T31, X59, X58))
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37), .(T36, X76), X77) → U2_gaa(T36, T37, X76, X77, splitC_in_gaa(T37, X77, X76))
U2_gaa(T36, T37, X76, X77, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U3_ggaa(T30, T31, X58, X59, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U9_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → U10_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pL_in_ggagaa(T21, T25, X22, T24, X23, T14))
pL_in_ggagaa(T21, T25, T38, T24, X23, T14) → U11_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_in_ga(.(T21, T25), T38))
U11_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_out_ga(.(T21, T25), T38)) → U12_ggagaa(T21, T25, T38, T24, X23, T14, pM_in_gaga(T24, X23, T38, T14))
pM_in_gaga(T24, T39, T38, T14) → U13_gaga(T24, T39, T38, T14, mergesortE_in_ga(T24, T39))
mergesortE_in_ga([], []) → mergesortE_out_ga([], [])
mergesortE_in_ga(.(T44, []), .(T44, [])) → mergesortE_out_ga(.(T44, []), .(T44, []))
mergesortE_in_ga(.(T51, .(T52, T53)), X105) → U4_ga(T51, T52, T53, X105, pF_in_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105))
pF_in_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105) → U15_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_in_ggaa(T51, .(T52, T53), T54, T55))
U15_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U16_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pN_in_gagaa(T54, X103, T55, X104, X105))
pN_in_gagaa(T54, T56, T55, X104, X105) → U17_gagaa(T54, T56, T55, X104, X105, mergesortE_in_ga(T54, T56))
U17_gagaa(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → U18_gagaa(T54, T56, T55, X104, X105, pO_in_gaga(T55, X104, T56, X105))
pO_in_gaga(T55, T57, T56, X105) → U19_gaga(T55, T57, T56, X105, mergesortE_in_ga(T55, T57))
U19_gaga(T55, T57, T56, X105, mergesortE_out_ga(T55, T57)) → U20_gaga(T55, T57, T56, X105, mergeG_in_gga(T56, T57, X105))
mergeG_in_gga(T66, [], T66) → mergeG_out_gga(T66, [], T66)
mergeG_in_gga([], T71, T71) → mergeG_out_gga([], T71, T71)
mergeG_in_gga(.(T92, T93), .(T94, T95), .(T92, T97)) → U5_gga(T92, T93, T94, T95, T97, pH_in_gggga(T92, T94, T93, T95, T97))
pH_in_gggga(T92, T94, T93, T95, T97) → U21_gggga(T92, T94, T93, T95, T97, leJ_in_gg(T92, T94))
leJ_in_gg(s(T110), s(T111)) → U7_gg(T110, T111, leJ_in_gg(T110, T111))
leJ_in_gg(0, s(T118)) → leJ_out_gg(0, s(T118))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U7_gg(T110, T111, leJ_out_gg(T110, T111)) → leJ_out_gg(s(T110), s(T111))
U21_gggga(T92, T94, T93, T95, T97, leJ_out_gg(T92, T94)) → U22_gggga(T92, T94, T93, T95, T97, mergeG_in_gga(T93, .(T94, T95), T97))
mergeG_in_gga(.(T131, T132), .(T133, T134), .(T133, T136)) → U6_gga(T131, T132, T133, T134, T136, pI_in_gggga(T131, T133, T132, T134, T136))
pI_in_gggga(T131, T133, T132, T134, T136) → U23_gggga(T131, T133, T132, T134, T136, gtK_in_gg(T131, T133))
gtK_in_gg(s(T149), s(T150)) → U8_gg(T149, T150, gtK_in_gg(T149, T150))
gtK_in_gg(s(T155), 0) → gtK_out_gg(s(T155), 0)
U8_gg(T149, T150, gtK_out_gg(T149, T150)) → gtK_out_gg(s(T149), s(T150))
U23_gggga(T131, T133, T132, T134, T136, gtK_out_gg(T131, T133)) → U24_gggga(T131, T133, T132, T134, T136, mergeG_in_gga(.(T131, T132), T134, T136))
U24_gggga(T131, T133, T132, T134, T136, mergeG_out_gga(.(T131, T132), T134, T136)) → pI_out_gggga(T131, T133, T132, T134, T136)
U6_gga(T131, T132, T133, T134, T136, pI_out_gggga(T131, T133, T132, T134, T136)) → mergeG_out_gga(.(T131, T132), .(T133, T134), .(T133, T136))
U22_gggga(T92, T94, T93, T95, T97, mergeG_out_gga(T93, .(T94, T95), T97)) → pH_out_gggga(T92, T94, T93, T95, T97)
U5_gga(T92, T93, T94, T95, T97, pH_out_gggga(T92, T94, T93, T95, T97)) → mergeG_out_gga(.(T92, T93), .(T94, T95), .(T92, T97))
U20_gaga(T55, T57, T56, X105, mergeG_out_gga(T56, T57, X105)) → pO_out_gaga(T55, T57, T56, X105)
U18_gagaa(T54, T56, T55, X104, X105, pO_out_gaga(T55, X104, T56, X105)) → pN_out_gagaa(T54, T56, T55, X104, X105)
U16_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pN_out_gagaa(T54, X103, T55, X104, X105)) → pF_out_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105)
U4_ga(T51, T52, T53, X105, pF_out_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105)) → mergesortE_out_ga(.(T51, .(T52, T53)), X105)
U13_gaga(T24, T39, T38, T14, mergesortE_out_ga(T24, T39)) → U14_gaga(T24, T39, T38, T14, mergeG_in_gga(T38, T39, T14))
U14_gaga(T24, T39, T38, T14, mergeG_out_gga(T38, T39, T14)) → pM_out_gaga(T24, T39, T38, T14)
U12_ggagaa(T21, T25, T38, T24, X23, T14, pM_out_gaga(T24, X23, T38, T14)) → pL_out_ggagaa(T21, T25, T38, T24, X23, T14)
U10_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pL_out_ggagaa(T21, T25, X22, T24, X23, T14)) → pB_out_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14)
U1_ga(T21, T22, T23, T14, pB_out_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14)) → mergesortA_out_ga(.(T21, .(T22, T23)), T14)

The argument filtering Pi contains the following mapping:
mergesortA_in_ga(x1, x2)  =  mergesortA_in_ga(x1)
[]  =  []
mergesortA_out_ga(x1, x2)  =  mergesortA_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
pB_in_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pB_in_ggaagaaa(x1, x2, x5)
U9_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U9_ggaagaaa(x1, x2, x5, x9)
splitD_in_ggaa(x1, x2, x3, x4)  =  splitD_in_ggaa(x1, x2)
U3_ggaa(x1, x2, x3, x4, x5)  =  U3_ggaa(x1, x2, x5)
splitC_in_gaa(x1, x2, x3)  =  splitC_in_gaa(x1)
splitC_out_gaa(x1, x2, x3)  =  splitC_out_gaa(x1, x2, x3)
U2_gaa(x1, x2, x3, x4, x5)  =  U2_gaa(x1, x2, x5)
splitD_out_ggaa(x1, x2, x3, x4)  =  splitD_out_ggaa(x1, x2, x3, x4)
U10_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U10_ggaagaaa(x1, x2, x3, x4, x5, x9)
pL_in_ggagaa(x1, x2, x3, x4, x5, x6)  =  pL_in_ggagaa(x1, x2, x4)
U11_ggagaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_ggagaa(x1, x2, x4, x7)
U12_ggagaa(x1, x2, x3, x4, x5, x6, x7)  =  U12_ggagaa(x1, x2, x3, x4, x7)
pM_in_gaga(x1, x2, x3, x4)  =  pM_in_gaga(x1, x3)
U13_gaga(x1, x2, x3, x4, x5)  =  U13_gaga(x1, x3, x5)
mergesortE_in_ga(x1, x2)  =  mergesortE_in_ga(x1)
mergesortE_out_ga(x1, x2)  =  mergesortE_out_ga(x1, x2)
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x2, x3, x5)
pF_in_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pF_in_gggaaaaa(x1, x2, x3)
U15_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U15_gggaaaaa(x1, x2, x3, x9)
U16_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U16_gggaaaaa(x1, x2, x3, x4, x5, x9)
pN_in_gagaa(x1, x2, x3, x4, x5)  =  pN_in_gagaa(x1, x3)
U17_gagaa(x1, x2, x3, x4, x5, x6)  =  U17_gagaa(x1, x3, x6)
U18_gagaa(x1, x2, x3, x4, x5, x6)  =  U18_gagaa(x1, x2, x3, x6)
pO_in_gaga(x1, x2, x3, x4)  =  pO_in_gaga(x1, x3)
U19_gaga(x1, x2, x3, x4, x5)  =  U19_gaga(x1, x3, x5)
U20_gaga(x1, x2, x3, x4, x5)  =  U20_gaga(x1, x2, x3, x5)
mergeG_in_gga(x1, x2, x3)  =  mergeG_in_gga(x1, x2)
mergeG_out_gga(x1, x2, x3)  =  mergeG_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4, x5, x6)  =  U5_gga(x1, x2, x3, x4, x6)
pH_in_gggga(x1, x2, x3, x4, x5)  =  pH_in_gggga(x1, x2, x3, x4)
U21_gggga(x1, x2, x3, x4, x5, x6)  =  U21_gggga(x1, x2, x3, x4, x6)
leJ_in_gg(x1, x2)  =  leJ_in_gg(x1, x2)
s(x1)  =  s(x1)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
0  =  0
leJ_out_gg(x1, x2)  =  leJ_out_gg(x1, x2)
U22_gggga(x1, x2, x3, x4, x5, x6)  =  U22_gggga(x1, x2, x3, x4, x6)
U6_gga(x1, x2, x3, x4, x5, x6)  =  U6_gga(x1, x2, x3, x4, x6)
pI_in_gggga(x1, x2, x3, x4, x5)  =  pI_in_gggga(x1, x2, x3, x4)
U23_gggga(x1, x2, x3, x4, x5, x6)  =  U23_gggga(x1, x2, x3, x4, x6)
gtK_in_gg(x1, x2)  =  gtK_in_gg(x1, x2)
U8_gg(x1, x2, x3)  =  U8_gg(x1, x2, x3)
gtK_out_gg(x1, x2)  =  gtK_out_gg(x1, x2)
U24_gggga(x1, x2, x3, x4, x5, x6)  =  U24_gggga(x1, x2, x3, x4, x6)
pI_out_gggga(x1, x2, x3, x4, x5)  =  pI_out_gggga(x1, x2, x3, x4, x5)
pH_out_gggga(x1, x2, x3, x4, x5)  =  pH_out_gggga(x1, x2, x3, x4, x5)
pO_out_gaga(x1, x2, x3, x4)  =  pO_out_gaga(x1, x2, x3, x4)
pN_out_gagaa(x1, x2, x3, x4, x5)  =  pN_out_gagaa(x1, x2, x3, x4, x5)
pF_out_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pF_out_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)
U14_gaga(x1, x2, x3, x4, x5)  =  U14_gaga(x1, x2, x3, x5)
pM_out_gaga(x1, x2, x3, x4)  =  pM_out_gaga(x1, x2, x3, x4)
pL_out_ggagaa(x1, x2, x3, x4, x5, x6)  =  pL_out_ggagaa(x1, x2, x3, x4, x5, x6)
pB_out_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pB_out_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)
MERGESORTA_IN_GA(x1, x2)  =  MERGESORTA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5)  =  U1_GA(x1, x2, x3, x5)
PB_IN_GGAAGAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  PB_IN_GGAAGAAA(x1, x2, x5)
U9_GGAAGAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U9_GGAAGAAA(x1, x2, x5, x9)
SPLITD_IN_GGAA(x1, x2, x3, x4)  =  SPLITD_IN_GGAA(x1, x2)
U3_GGAA(x1, x2, x3, x4, x5)  =  U3_GGAA(x1, x2, x5)
SPLITC_IN_GAA(x1, x2, x3)  =  SPLITC_IN_GAA(x1)
U2_GAA(x1, x2, x3, x4, x5)  =  U2_GAA(x1, x2, x5)
U10_GGAAGAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U10_GGAAGAAA(x1, x2, x3, x4, x5, x9)
PL_IN_GGAGAA(x1, x2, x3, x4, x5, x6)  =  PL_IN_GGAGAA(x1, x2, x4)
U11_GGAGAA(x1, x2, x3, x4, x5, x6, x7)  =  U11_GGAGAA(x1, x2, x4, x7)
U12_GGAGAA(x1, x2, x3, x4, x5, x6, x7)  =  U12_GGAGAA(x1, x2, x3, x4, x7)
PM_IN_GAGA(x1, x2, x3, x4)  =  PM_IN_GAGA(x1, x3)
U13_GAGA(x1, x2, x3, x4, x5)  =  U13_GAGA(x1, x3, x5)
MERGESORTE_IN_GA(x1, x2)  =  MERGESORTE_IN_GA(x1)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x1, x2, x3, x5)
PF_IN_GGGAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  PF_IN_GGGAAAAA(x1, x2, x3)
U15_GGGAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U15_GGGAAAAA(x1, x2, x3, x9)
U16_GGGAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U16_GGGAAAAA(x1, x2, x3, x4, x5, x9)
PN_IN_GAGAA(x1, x2, x3, x4, x5)  =  PN_IN_GAGAA(x1, x3)
U17_GAGAA(x1, x2, x3, x4, x5, x6)  =  U17_GAGAA(x1, x3, x6)
U18_GAGAA(x1, x2, x3, x4, x5, x6)  =  U18_GAGAA(x1, x2, x3, x6)
PO_IN_GAGA(x1, x2, x3, x4)  =  PO_IN_GAGA(x1, x3)
U19_GAGA(x1, x2, x3, x4, x5)  =  U19_GAGA(x1, x3, x5)
U20_GAGA(x1, x2, x3, x4, x5)  =  U20_GAGA(x1, x2, x3, x5)
MERGEG_IN_GGA(x1, x2, x3)  =  MERGEG_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4, x5, x6)  =  U5_GGA(x1, x2, x3, x4, x6)
PH_IN_GGGGA(x1, x2, x3, x4, x5)  =  PH_IN_GGGGA(x1, x2, x3, x4)
U21_GGGGA(x1, x2, x3, x4, x5, x6)  =  U21_GGGGA(x1, x2, x3, x4, x6)
LEJ_IN_GG(x1, x2)  =  LEJ_IN_GG(x1, x2)
U7_GG(x1, x2, x3)  =  U7_GG(x1, x2, x3)
U22_GGGGA(x1, x2, x3, x4, x5, x6)  =  U22_GGGGA(x1, x2, x3, x4, x6)
U6_GGA(x1, x2, x3, x4, x5, x6)  =  U6_GGA(x1, x2, x3, x4, x6)
PI_IN_GGGGA(x1, x2, x3, x4, x5)  =  PI_IN_GGGGA(x1, x2, x3, x4)
U23_GGGGA(x1, x2, x3, x4, x5, x6)  =  U23_GGGGA(x1, x2, x3, x4, x6)
GTK_IN_GG(x1, x2)  =  GTK_IN_GG(x1, x2)
U8_GG(x1, x2, x3)  =  U8_GG(x1, x2, x3)
U24_GGGGA(x1, x2, x3, x4, x5, x6)  =  U24_GGGGA(x1, x2, x3, x4, x6)
U14_GAGA(x1, x2, x3, x4, x5)  =  U14_GAGA(x1, x2, x3, x5)

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

(4) Obligation:

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

MERGESORTA_IN_GA(.(T21, .(T22, T23)), T14) → U1_GA(T21, T22, T23, T14, pB_in_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14))
MERGESORTA_IN_GA(.(T21, .(T22, T23)), T14) → PB_IN_GGAAGAAA(T22, T23, X41, X40, T21, X22, X23, T14)
PB_IN_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14) → U9_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14, splitD_in_ggaa(T22, T23, T24, T25))
PB_IN_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14) → SPLITD_IN_GGAA(T22, T23, T24, T25)
SPLITD_IN_GGAA(T30, T31, .(T30, X58), X59) → U3_GGAA(T30, T31, X58, X59, splitC_in_gaa(T31, X59, X58))
SPLITD_IN_GGAA(T30, T31, .(T30, X58), X59) → SPLITC_IN_GAA(T31, X59, X58)
SPLITC_IN_GAA(.(T36, T37), .(T36, X76), X77) → U2_GAA(T36, T37, X76, X77, splitC_in_gaa(T37, X77, X76))
SPLITC_IN_GAA(.(T36, T37), .(T36, X76), X77) → SPLITC_IN_GAA(T37, X77, X76)
U9_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → U10_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14, pL_in_ggagaa(T21, T25, X22, T24, X23, T14))
U9_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → PL_IN_GGAGAA(T21, T25, X22, T24, X23, T14)
PL_IN_GGAGAA(T21, T25, T38, T24, X23, T14) → U11_GGAGAA(T21, T25, T38, T24, X23, T14, mergesortA_in_ga(.(T21, T25), T38))
PL_IN_GGAGAA(T21, T25, T38, T24, X23, T14) → MERGESORTA_IN_GA(.(T21, T25), T38)
U11_GGAGAA(T21, T25, T38, T24, X23, T14, mergesortA_out_ga(.(T21, T25), T38)) → U12_GGAGAA(T21, T25, T38, T24, X23, T14, pM_in_gaga(T24, X23, T38, T14))
U11_GGAGAA(T21, T25, T38, T24, X23, T14, mergesortA_out_ga(.(T21, T25), T38)) → PM_IN_GAGA(T24, X23, T38, T14)
PM_IN_GAGA(T24, T39, T38, T14) → U13_GAGA(T24, T39, T38, T14, mergesortE_in_ga(T24, T39))
PM_IN_GAGA(T24, T39, T38, T14) → MERGESORTE_IN_GA(T24, T39)
MERGESORTE_IN_GA(.(T51, .(T52, T53)), X105) → U4_GA(T51, T52, T53, X105, pF_in_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105))
MERGESORTE_IN_GA(.(T51, .(T52, T53)), X105) → PF_IN_GGGAAAAA(T51, T52, T53, X101, X102, X103, X104, X105)
PF_IN_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105) → U15_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105, splitD_in_ggaa(T51, .(T52, T53), T54, T55))
PF_IN_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105) → SPLITD_IN_GGAA(T51, .(T52, T53), T54, T55)
U15_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U16_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105, pN_in_gagaa(T54, X103, T55, X104, X105))
U15_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → PN_IN_GAGAA(T54, X103, T55, X104, X105)
PN_IN_GAGAA(T54, T56, T55, X104, X105) → U17_GAGAA(T54, T56, T55, X104, X105, mergesortE_in_ga(T54, T56))
PN_IN_GAGAA(T54, T56, T55, X104, X105) → MERGESORTE_IN_GA(T54, T56)
U17_GAGAA(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → U18_GAGAA(T54, T56, T55, X104, X105, pO_in_gaga(T55, X104, T56, X105))
U17_GAGAA(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → PO_IN_GAGA(T55, X104, T56, X105)
PO_IN_GAGA(T55, T57, T56, X105) → U19_GAGA(T55, T57, T56, X105, mergesortE_in_ga(T55, T57))
PO_IN_GAGA(T55, T57, T56, X105) → MERGESORTE_IN_GA(T55, T57)
U19_GAGA(T55, T57, T56, X105, mergesortE_out_ga(T55, T57)) → U20_GAGA(T55, T57, T56, X105, mergeG_in_gga(T56, T57, X105))
U19_GAGA(T55, T57, T56, X105, mergesortE_out_ga(T55, T57)) → MERGEG_IN_GGA(T56, T57, X105)
MERGEG_IN_GGA(.(T92, T93), .(T94, T95), .(T92, T97)) → U5_GGA(T92, T93, T94, T95, T97, pH_in_gggga(T92, T94, T93, T95, T97))
MERGEG_IN_GGA(.(T92, T93), .(T94, T95), .(T92, T97)) → PH_IN_GGGGA(T92, T94, T93, T95, T97)
PH_IN_GGGGA(T92, T94, T93, T95, T97) → U21_GGGGA(T92, T94, T93, T95, T97, leJ_in_gg(T92, T94))
PH_IN_GGGGA(T92, T94, T93, T95, T97) → LEJ_IN_GG(T92, T94)
LEJ_IN_GG(s(T110), s(T111)) → U7_GG(T110, T111, leJ_in_gg(T110, T111))
LEJ_IN_GG(s(T110), s(T111)) → LEJ_IN_GG(T110, T111)
U21_GGGGA(T92, T94, T93, T95, T97, leJ_out_gg(T92, T94)) → U22_GGGGA(T92, T94, T93, T95, T97, mergeG_in_gga(T93, .(T94, T95), T97))
U21_GGGGA(T92, T94, T93, T95, T97, leJ_out_gg(T92, T94)) → MERGEG_IN_GGA(T93, .(T94, T95), T97)
MERGEG_IN_GGA(.(T131, T132), .(T133, T134), .(T133, T136)) → U6_GGA(T131, T132, T133, T134, T136, pI_in_gggga(T131, T133, T132, T134, T136))
MERGEG_IN_GGA(.(T131, T132), .(T133, T134), .(T133, T136)) → PI_IN_GGGGA(T131, T133, T132, T134, T136)
PI_IN_GGGGA(T131, T133, T132, T134, T136) → U23_GGGGA(T131, T133, T132, T134, T136, gtK_in_gg(T131, T133))
PI_IN_GGGGA(T131, T133, T132, T134, T136) → GTK_IN_GG(T131, T133)
GTK_IN_GG(s(T149), s(T150)) → U8_GG(T149, T150, gtK_in_gg(T149, T150))
GTK_IN_GG(s(T149), s(T150)) → GTK_IN_GG(T149, T150)
U23_GGGGA(T131, T133, T132, T134, T136, gtK_out_gg(T131, T133)) → U24_GGGGA(T131, T133, T132, T134, T136, mergeG_in_gga(.(T131, T132), T134, T136))
U23_GGGGA(T131, T133, T132, T134, T136, gtK_out_gg(T131, T133)) → MERGEG_IN_GGA(.(T131, T132), T134, T136)
U13_GAGA(T24, T39, T38, T14, mergesortE_out_ga(T24, T39)) → U14_GAGA(T24, T39, T38, T14, mergeG_in_gga(T38, T39, T14))
U13_GAGA(T24, T39, T38, T14, mergesortE_out_ga(T24, T39)) → MERGEG_IN_GGA(T38, T39, T14)

The TRS R consists of the following rules:

mergesortA_in_ga([], []) → mergesortA_out_ga([], [])
mergesortA_in_ga(.(T4, []), .(T4, [])) → mergesortA_out_ga(.(T4, []), .(T4, []))
mergesortA_in_ga(.(T21, .(T22, T23)), T14) → U1_ga(T21, T22, T23, T14, pB_in_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14))
pB_in_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14) → U9_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_in_ggaa(T22, T23, T24, T25))
splitD_in_ggaa(T30, T31, .(T30, X58), X59) → U3_ggaa(T30, T31, X58, X59, splitC_in_gaa(T31, X59, X58))
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37), .(T36, X76), X77) → U2_gaa(T36, T37, X76, X77, splitC_in_gaa(T37, X77, X76))
U2_gaa(T36, T37, X76, X77, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U3_ggaa(T30, T31, X58, X59, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U9_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → U10_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pL_in_ggagaa(T21, T25, X22, T24, X23, T14))
pL_in_ggagaa(T21, T25, T38, T24, X23, T14) → U11_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_in_ga(.(T21, T25), T38))
U11_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_out_ga(.(T21, T25), T38)) → U12_ggagaa(T21, T25, T38, T24, X23, T14, pM_in_gaga(T24, X23, T38, T14))
pM_in_gaga(T24, T39, T38, T14) → U13_gaga(T24, T39, T38, T14, mergesortE_in_ga(T24, T39))
mergesortE_in_ga([], []) → mergesortE_out_ga([], [])
mergesortE_in_ga(.(T44, []), .(T44, [])) → mergesortE_out_ga(.(T44, []), .(T44, []))
mergesortE_in_ga(.(T51, .(T52, T53)), X105) → U4_ga(T51, T52, T53, X105, pF_in_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105))
pF_in_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105) → U15_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_in_ggaa(T51, .(T52, T53), T54, T55))
U15_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U16_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pN_in_gagaa(T54, X103, T55, X104, X105))
pN_in_gagaa(T54, T56, T55, X104, X105) → U17_gagaa(T54, T56, T55, X104, X105, mergesortE_in_ga(T54, T56))
U17_gagaa(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → U18_gagaa(T54, T56, T55, X104, X105, pO_in_gaga(T55, X104, T56, X105))
pO_in_gaga(T55, T57, T56, X105) → U19_gaga(T55, T57, T56, X105, mergesortE_in_ga(T55, T57))
U19_gaga(T55, T57, T56, X105, mergesortE_out_ga(T55, T57)) → U20_gaga(T55, T57, T56, X105, mergeG_in_gga(T56, T57, X105))
mergeG_in_gga(T66, [], T66) → mergeG_out_gga(T66, [], T66)
mergeG_in_gga([], T71, T71) → mergeG_out_gga([], T71, T71)
mergeG_in_gga(.(T92, T93), .(T94, T95), .(T92, T97)) → U5_gga(T92, T93, T94, T95, T97, pH_in_gggga(T92, T94, T93, T95, T97))
pH_in_gggga(T92, T94, T93, T95, T97) → U21_gggga(T92, T94, T93, T95, T97, leJ_in_gg(T92, T94))
leJ_in_gg(s(T110), s(T111)) → U7_gg(T110, T111, leJ_in_gg(T110, T111))
leJ_in_gg(0, s(T118)) → leJ_out_gg(0, s(T118))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U7_gg(T110, T111, leJ_out_gg(T110, T111)) → leJ_out_gg(s(T110), s(T111))
U21_gggga(T92, T94, T93, T95, T97, leJ_out_gg(T92, T94)) → U22_gggga(T92, T94, T93, T95, T97, mergeG_in_gga(T93, .(T94, T95), T97))
mergeG_in_gga(.(T131, T132), .(T133, T134), .(T133, T136)) → U6_gga(T131, T132, T133, T134, T136, pI_in_gggga(T131, T133, T132, T134, T136))
pI_in_gggga(T131, T133, T132, T134, T136) → U23_gggga(T131, T133, T132, T134, T136, gtK_in_gg(T131, T133))
gtK_in_gg(s(T149), s(T150)) → U8_gg(T149, T150, gtK_in_gg(T149, T150))
gtK_in_gg(s(T155), 0) → gtK_out_gg(s(T155), 0)
U8_gg(T149, T150, gtK_out_gg(T149, T150)) → gtK_out_gg(s(T149), s(T150))
U23_gggga(T131, T133, T132, T134, T136, gtK_out_gg(T131, T133)) → U24_gggga(T131, T133, T132, T134, T136, mergeG_in_gga(.(T131, T132), T134, T136))
U24_gggga(T131, T133, T132, T134, T136, mergeG_out_gga(.(T131, T132), T134, T136)) → pI_out_gggga(T131, T133, T132, T134, T136)
U6_gga(T131, T132, T133, T134, T136, pI_out_gggga(T131, T133, T132, T134, T136)) → mergeG_out_gga(.(T131, T132), .(T133, T134), .(T133, T136))
U22_gggga(T92, T94, T93, T95, T97, mergeG_out_gga(T93, .(T94, T95), T97)) → pH_out_gggga(T92, T94, T93, T95, T97)
U5_gga(T92, T93, T94, T95, T97, pH_out_gggga(T92, T94, T93, T95, T97)) → mergeG_out_gga(.(T92, T93), .(T94, T95), .(T92, T97))
U20_gaga(T55, T57, T56, X105, mergeG_out_gga(T56, T57, X105)) → pO_out_gaga(T55, T57, T56, X105)
U18_gagaa(T54, T56, T55, X104, X105, pO_out_gaga(T55, X104, T56, X105)) → pN_out_gagaa(T54, T56, T55, X104, X105)
U16_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pN_out_gagaa(T54, X103, T55, X104, X105)) → pF_out_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105)
U4_ga(T51, T52, T53, X105, pF_out_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105)) → mergesortE_out_ga(.(T51, .(T52, T53)), X105)
U13_gaga(T24, T39, T38, T14, mergesortE_out_ga(T24, T39)) → U14_gaga(T24, T39, T38, T14, mergeG_in_gga(T38, T39, T14))
U14_gaga(T24, T39, T38, T14, mergeG_out_gga(T38, T39, T14)) → pM_out_gaga(T24, T39, T38, T14)
U12_ggagaa(T21, T25, T38, T24, X23, T14, pM_out_gaga(T24, X23, T38, T14)) → pL_out_ggagaa(T21, T25, T38, T24, X23, T14)
U10_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pL_out_ggagaa(T21, T25, X22, T24, X23, T14)) → pB_out_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14)
U1_ga(T21, T22, T23, T14, pB_out_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14)) → mergesortA_out_ga(.(T21, .(T22, T23)), T14)

The argument filtering Pi contains the following mapping:
mergesortA_in_ga(x1, x2)  =  mergesortA_in_ga(x1)
[]  =  []
mergesortA_out_ga(x1, x2)  =  mergesortA_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
pB_in_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pB_in_ggaagaaa(x1, x2, x5)
U9_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U9_ggaagaaa(x1, x2, x5, x9)
splitD_in_ggaa(x1, x2, x3, x4)  =  splitD_in_ggaa(x1, x2)
U3_ggaa(x1, x2, x3, x4, x5)  =  U3_ggaa(x1, x2, x5)
splitC_in_gaa(x1, x2, x3)  =  splitC_in_gaa(x1)
splitC_out_gaa(x1, x2, x3)  =  splitC_out_gaa(x1, x2, x3)
U2_gaa(x1, x2, x3, x4, x5)  =  U2_gaa(x1, x2, x5)
splitD_out_ggaa(x1, x2, x3, x4)  =  splitD_out_ggaa(x1, x2, x3, x4)
U10_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U10_ggaagaaa(x1, x2, x3, x4, x5, x9)
pL_in_ggagaa(x1, x2, x3, x4, x5, x6)  =  pL_in_ggagaa(x1, x2, x4)
U11_ggagaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_ggagaa(x1, x2, x4, x7)
U12_ggagaa(x1, x2, x3, x4, x5, x6, x7)  =  U12_ggagaa(x1, x2, x3, x4, x7)
pM_in_gaga(x1, x2, x3, x4)  =  pM_in_gaga(x1, x3)
U13_gaga(x1, x2, x3, x4, x5)  =  U13_gaga(x1, x3, x5)
mergesortE_in_ga(x1, x2)  =  mergesortE_in_ga(x1)
mergesortE_out_ga(x1, x2)  =  mergesortE_out_ga(x1, x2)
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x2, x3, x5)
pF_in_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pF_in_gggaaaaa(x1, x2, x3)
U15_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U15_gggaaaaa(x1, x2, x3, x9)
U16_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U16_gggaaaaa(x1, x2, x3, x4, x5, x9)
pN_in_gagaa(x1, x2, x3, x4, x5)  =  pN_in_gagaa(x1, x3)
U17_gagaa(x1, x2, x3, x4, x5, x6)  =  U17_gagaa(x1, x3, x6)
U18_gagaa(x1, x2, x3, x4, x5, x6)  =  U18_gagaa(x1, x2, x3, x6)
pO_in_gaga(x1, x2, x3, x4)  =  pO_in_gaga(x1, x3)
U19_gaga(x1, x2, x3, x4, x5)  =  U19_gaga(x1, x3, x5)
U20_gaga(x1, x2, x3, x4, x5)  =  U20_gaga(x1, x2, x3, x5)
mergeG_in_gga(x1, x2, x3)  =  mergeG_in_gga(x1, x2)
mergeG_out_gga(x1, x2, x3)  =  mergeG_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4, x5, x6)  =  U5_gga(x1, x2, x3, x4, x6)
pH_in_gggga(x1, x2, x3, x4, x5)  =  pH_in_gggga(x1, x2, x3, x4)
U21_gggga(x1, x2, x3, x4, x5, x6)  =  U21_gggga(x1, x2, x3, x4, x6)
leJ_in_gg(x1, x2)  =  leJ_in_gg(x1, x2)
s(x1)  =  s(x1)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
0  =  0
leJ_out_gg(x1, x2)  =  leJ_out_gg(x1, x2)
U22_gggga(x1, x2, x3, x4, x5, x6)  =  U22_gggga(x1, x2, x3, x4, x6)
U6_gga(x1, x2, x3, x4, x5, x6)  =  U6_gga(x1, x2, x3, x4, x6)
pI_in_gggga(x1, x2, x3, x4, x5)  =  pI_in_gggga(x1, x2, x3, x4)
U23_gggga(x1, x2, x3, x4, x5, x6)  =  U23_gggga(x1, x2, x3, x4, x6)
gtK_in_gg(x1, x2)  =  gtK_in_gg(x1, x2)
U8_gg(x1, x2, x3)  =  U8_gg(x1, x2, x3)
gtK_out_gg(x1, x2)  =  gtK_out_gg(x1, x2)
U24_gggga(x1, x2, x3, x4, x5, x6)  =  U24_gggga(x1, x2, x3, x4, x6)
pI_out_gggga(x1, x2, x3, x4, x5)  =  pI_out_gggga(x1, x2, x3, x4, x5)
pH_out_gggga(x1, x2, x3, x4, x5)  =  pH_out_gggga(x1, x2, x3, x4, x5)
pO_out_gaga(x1, x2, x3, x4)  =  pO_out_gaga(x1, x2, x3, x4)
pN_out_gagaa(x1, x2, x3, x4, x5)  =  pN_out_gagaa(x1, x2, x3, x4, x5)
pF_out_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pF_out_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)
U14_gaga(x1, x2, x3, x4, x5)  =  U14_gaga(x1, x2, x3, x5)
pM_out_gaga(x1, x2, x3, x4)  =  pM_out_gaga(x1, x2, x3, x4)
pL_out_ggagaa(x1, x2, x3, x4, x5, x6)  =  pL_out_ggagaa(x1, x2, x3, x4, x5, x6)
pB_out_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pB_out_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)
MERGESORTA_IN_GA(x1, x2)  =  MERGESORTA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5)  =  U1_GA(x1, x2, x3, x5)
PB_IN_GGAAGAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  PB_IN_GGAAGAAA(x1, x2, x5)
U9_GGAAGAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U9_GGAAGAAA(x1, x2, x5, x9)
SPLITD_IN_GGAA(x1, x2, x3, x4)  =  SPLITD_IN_GGAA(x1, x2)
U3_GGAA(x1, x2, x3, x4, x5)  =  U3_GGAA(x1, x2, x5)
SPLITC_IN_GAA(x1, x2, x3)  =  SPLITC_IN_GAA(x1)
U2_GAA(x1, x2, x3, x4, x5)  =  U2_GAA(x1, x2, x5)
U10_GGAAGAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U10_GGAAGAAA(x1, x2, x3, x4, x5, x9)
PL_IN_GGAGAA(x1, x2, x3, x4, x5, x6)  =  PL_IN_GGAGAA(x1, x2, x4)
U11_GGAGAA(x1, x2, x3, x4, x5, x6, x7)  =  U11_GGAGAA(x1, x2, x4, x7)
U12_GGAGAA(x1, x2, x3, x4, x5, x6, x7)  =  U12_GGAGAA(x1, x2, x3, x4, x7)
PM_IN_GAGA(x1, x2, x3, x4)  =  PM_IN_GAGA(x1, x3)
U13_GAGA(x1, x2, x3, x4, x5)  =  U13_GAGA(x1, x3, x5)
MERGESORTE_IN_GA(x1, x2)  =  MERGESORTE_IN_GA(x1)
U4_GA(x1, x2, x3, x4, x5)  =  U4_GA(x1, x2, x3, x5)
PF_IN_GGGAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  PF_IN_GGGAAAAA(x1, x2, x3)
U15_GGGAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U15_GGGAAAAA(x1, x2, x3, x9)
U16_GGGAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U16_GGGAAAAA(x1, x2, x3, x4, x5, x9)
PN_IN_GAGAA(x1, x2, x3, x4, x5)  =  PN_IN_GAGAA(x1, x3)
U17_GAGAA(x1, x2, x3, x4, x5, x6)  =  U17_GAGAA(x1, x3, x6)
U18_GAGAA(x1, x2, x3, x4, x5, x6)  =  U18_GAGAA(x1, x2, x3, x6)
PO_IN_GAGA(x1, x2, x3, x4)  =  PO_IN_GAGA(x1, x3)
U19_GAGA(x1, x2, x3, x4, x5)  =  U19_GAGA(x1, x3, x5)
U20_GAGA(x1, x2, x3, x4, x5)  =  U20_GAGA(x1, x2, x3, x5)
MERGEG_IN_GGA(x1, x2, x3)  =  MERGEG_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4, x5, x6)  =  U5_GGA(x1, x2, x3, x4, x6)
PH_IN_GGGGA(x1, x2, x3, x4, x5)  =  PH_IN_GGGGA(x1, x2, x3, x4)
U21_GGGGA(x1, x2, x3, x4, x5, x6)  =  U21_GGGGA(x1, x2, x3, x4, x6)
LEJ_IN_GG(x1, x2)  =  LEJ_IN_GG(x1, x2)
U7_GG(x1, x2, x3)  =  U7_GG(x1, x2, x3)
U22_GGGGA(x1, x2, x3, x4, x5, x6)  =  U22_GGGGA(x1, x2, x3, x4, x6)
U6_GGA(x1, x2, x3, x4, x5, x6)  =  U6_GGA(x1, x2, x3, x4, x6)
PI_IN_GGGGA(x1, x2, x3, x4, x5)  =  PI_IN_GGGGA(x1, x2, x3, x4)
U23_GGGGA(x1, x2, x3, x4, x5, x6)  =  U23_GGGGA(x1, x2, x3, x4, x6)
GTK_IN_GG(x1, x2)  =  GTK_IN_GG(x1, x2)
U8_GG(x1, x2, x3)  =  U8_GG(x1, x2, x3)
U24_GGGGA(x1, x2, x3, x4, x5, x6)  =  U24_GGGGA(x1, x2, x3, x4, x6)
U14_GAGA(x1, x2, x3, x4, x5)  =  U14_GAGA(x1, x2, x3, x5)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 6 SCCs with 28 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

GTK_IN_GG(s(T149), s(T150)) → GTK_IN_GG(T149, T150)

The TRS R consists of the following rules:

mergesortA_in_ga([], []) → mergesortA_out_ga([], [])
mergesortA_in_ga(.(T4, []), .(T4, [])) → mergesortA_out_ga(.(T4, []), .(T4, []))
mergesortA_in_ga(.(T21, .(T22, T23)), T14) → U1_ga(T21, T22, T23, T14, pB_in_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14))
pB_in_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14) → U9_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_in_ggaa(T22, T23, T24, T25))
splitD_in_ggaa(T30, T31, .(T30, X58), X59) → U3_ggaa(T30, T31, X58, X59, splitC_in_gaa(T31, X59, X58))
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37), .(T36, X76), X77) → U2_gaa(T36, T37, X76, X77, splitC_in_gaa(T37, X77, X76))
U2_gaa(T36, T37, X76, X77, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U3_ggaa(T30, T31, X58, X59, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U9_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → U10_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pL_in_ggagaa(T21, T25, X22, T24, X23, T14))
pL_in_ggagaa(T21, T25, T38, T24, X23, T14) → U11_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_in_ga(.(T21, T25), T38))
U11_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_out_ga(.(T21, T25), T38)) → U12_ggagaa(T21, T25, T38, T24, X23, T14, pM_in_gaga(T24, X23, T38, T14))
pM_in_gaga(T24, T39, T38, T14) → U13_gaga(T24, T39, T38, T14, mergesortE_in_ga(T24, T39))
mergesortE_in_ga([], []) → mergesortE_out_ga([], [])
mergesortE_in_ga(.(T44, []), .(T44, [])) → mergesortE_out_ga(.(T44, []), .(T44, []))
mergesortE_in_ga(.(T51, .(T52, T53)), X105) → U4_ga(T51, T52, T53, X105, pF_in_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105))
pF_in_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105) → U15_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_in_ggaa(T51, .(T52, T53), T54, T55))
U15_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U16_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pN_in_gagaa(T54, X103, T55, X104, X105))
pN_in_gagaa(T54, T56, T55, X104, X105) → U17_gagaa(T54, T56, T55, X104, X105, mergesortE_in_ga(T54, T56))
U17_gagaa(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → U18_gagaa(T54, T56, T55, X104, X105, pO_in_gaga(T55, X104, T56, X105))
pO_in_gaga(T55, T57, T56, X105) → U19_gaga(T55, T57, T56, X105, mergesortE_in_ga(T55, T57))
U19_gaga(T55, T57, T56, X105, mergesortE_out_ga(T55, T57)) → U20_gaga(T55, T57, T56, X105, mergeG_in_gga(T56, T57, X105))
mergeG_in_gga(T66, [], T66) → mergeG_out_gga(T66, [], T66)
mergeG_in_gga([], T71, T71) → mergeG_out_gga([], T71, T71)
mergeG_in_gga(.(T92, T93), .(T94, T95), .(T92, T97)) → U5_gga(T92, T93, T94, T95, T97, pH_in_gggga(T92, T94, T93, T95, T97))
pH_in_gggga(T92, T94, T93, T95, T97) → U21_gggga(T92, T94, T93, T95, T97, leJ_in_gg(T92, T94))
leJ_in_gg(s(T110), s(T111)) → U7_gg(T110, T111, leJ_in_gg(T110, T111))
leJ_in_gg(0, s(T118)) → leJ_out_gg(0, s(T118))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U7_gg(T110, T111, leJ_out_gg(T110, T111)) → leJ_out_gg(s(T110), s(T111))
U21_gggga(T92, T94, T93, T95, T97, leJ_out_gg(T92, T94)) → U22_gggga(T92, T94, T93, T95, T97, mergeG_in_gga(T93, .(T94, T95), T97))
mergeG_in_gga(.(T131, T132), .(T133, T134), .(T133, T136)) → U6_gga(T131, T132, T133, T134, T136, pI_in_gggga(T131, T133, T132, T134, T136))
pI_in_gggga(T131, T133, T132, T134, T136) → U23_gggga(T131, T133, T132, T134, T136, gtK_in_gg(T131, T133))
gtK_in_gg(s(T149), s(T150)) → U8_gg(T149, T150, gtK_in_gg(T149, T150))
gtK_in_gg(s(T155), 0) → gtK_out_gg(s(T155), 0)
U8_gg(T149, T150, gtK_out_gg(T149, T150)) → gtK_out_gg(s(T149), s(T150))
U23_gggga(T131, T133, T132, T134, T136, gtK_out_gg(T131, T133)) → U24_gggga(T131, T133, T132, T134, T136, mergeG_in_gga(.(T131, T132), T134, T136))
U24_gggga(T131, T133, T132, T134, T136, mergeG_out_gga(.(T131, T132), T134, T136)) → pI_out_gggga(T131, T133, T132, T134, T136)
U6_gga(T131, T132, T133, T134, T136, pI_out_gggga(T131, T133, T132, T134, T136)) → mergeG_out_gga(.(T131, T132), .(T133, T134), .(T133, T136))
U22_gggga(T92, T94, T93, T95, T97, mergeG_out_gga(T93, .(T94, T95), T97)) → pH_out_gggga(T92, T94, T93, T95, T97)
U5_gga(T92, T93, T94, T95, T97, pH_out_gggga(T92, T94, T93, T95, T97)) → mergeG_out_gga(.(T92, T93), .(T94, T95), .(T92, T97))
U20_gaga(T55, T57, T56, X105, mergeG_out_gga(T56, T57, X105)) → pO_out_gaga(T55, T57, T56, X105)
U18_gagaa(T54, T56, T55, X104, X105, pO_out_gaga(T55, X104, T56, X105)) → pN_out_gagaa(T54, T56, T55, X104, X105)
U16_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pN_out_gagaa(T54, X103, T55, X104, X105)) → pF_out_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105)
U4_ga(T51, T52, T53, X105, pF_out_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105)) → mergesortE_out_ga(.(T51, .(T52, T53)), X105)
U13_gaga(T24, T39, T38, T14, mergesortE_out_ga(T24, T39)) → U14_gaga(T24, T39, T38, T14, mergeG_in_gga(T38, T39, T14))
U14_gaga(T24, T39, T38, T14, mergeG_out_gga(T38, T39, T14)) → pM_out_gaga(T24, T39, T38, T14)
U12_ggagaa(T21, T25, T38, T24, X23, T14, pM_out_gaga(T24, X23, T38, T14)) → pL_out_ggagaa(T21, T25, T38, T24, X23, T14)
U10_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pL_out_ggagaa(T21, T25, X22, T24, X23, T14)) → pB_out_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14)
U1_ga(T21, T22, T23, T14, pB_out_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14)) → mergesortA_out_ga(.(T21, .(T22, T23)), T14)

The argument filtering Pi contains the following mapping:
mergesortA_in_ga(x1, x2)  =  mergesortA_in_ga(x1)
[]  =  []
mergesortA_out_ga(x1, x2)  =  mergesortA_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
pB_in_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pB_in_ggaagaaa(x1, x2, x5)
U9_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U9_ggaagaaa(x1, x2, x5, x9)
splitD_in_ggaa(x1, x2, x3, x4)  =  splitD_in_ggaa(x1, x2)
U3_ggaa(x1, x2, x3, x4, x5)  =  U3_ggaa(x1, x2, x5)
splitC_in_gaa(x1, x2, x3)  =  splitC_in_gaa(x1)
splitC_out_gaa(x1, x2, x3)  =  splitC_out_gaa(x1, x2, x3)
U2_gaa(x1, x2, x3, x4, x5)  =  U2_gaa(x1, x2, x5)
splitD_out_ggaa(x1, x2, x3, x4)  =  splitD_out_ggaa(x1, x2, x3, x4)
U10_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U10_ggaagaaa(x1, x2, x3, x4, x5, x9)
pL_in_ggagaa(x1, x2, x3, x4, x5, x6)  =  pL_in_ggagaa(x1, x2, x4)
U11_ggagaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_ggagaa(x1, x2, x4, x7)
U12_ggagaa(x1, x2, x3, x4, x5, x6, x7)  =  U12_ggagaa(x1, x2, x3, x4, x7)
pM_in_gaga(x1, x2, x3, x4)  =  pM_in_gaga(x1, x3)
U13_gaga(x1, x2, x3, x4, x5)  =  U13_gaga(x1, x3, x5)
mergesortE_in_ga(x1, x2)  =  mergesortE_in_ga(x1)
mergesortE_out_ga(x1, x2)  =  mergesortE_out_ga(x1, x2)
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x2, x3, x5)
pF_in_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pF_in_gggaaaaa(x1, x2, x3)
U15_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U15_gggaaaaa(x1, x2, x3, x9)
U16_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U16_gggaaaaa(x1, x2, x3, x4, x5, x9)
pN_in_gagaa(x1, x2, x3, x4, x5)  =  pN_in_gagaa(x1, x3)
U17_gagaa(x1, x2, x3, x4, x5, x6)  =  U17_gagaa(x1, x3, x6)
U18_gagaa(x1, x2, x3, x4, x5, x6)  =  U18_gagaa(x1, x2, x3, x6)
pO_in_gaga(x1, x2, x3, x4)  =  pO_in_gaga(x1, x3)
U19_gaga(x1, x2, x3, x4, x5)  =  U19_gaga(x1, x3, x5)
U20_gaga(x1, x2, x3, x4, x5)  =  U20_gaga(x1, x2, x3, x5)
mergeG_in_gga(x1, x2, x3)  =  mergeG_in_gga(x1, x2)
mergeG_out_gga(x1, x2, x3)  =  mergeG_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4, x5, x6)  =  U5_gga(x1, x2, x3, x4, x6)
pH_in_gggga(x1, x2, x3, x4, x5)  =  pH_in_gggga(x1, x2, x3, x4)
U21_gggga(x1, x2, x3, x4, x5, x6)  =  U21_gggga(x1, x2, x3, x4, x6)
leJ_in_gg(x1, x2)  =  leJ_in_gg(x1, x2)
s(x1)  =  s(x1)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
0  =  0
leJ_out_gg(x1, x2)  =  leJ_out_gg(x1, x2)
U22_gggga(x1, x2, x3, x4, x5, x6)  =  U22_gggga(x1, x2, x3, x4, x6)
U6_gga(x1, x2, x3, x4, x5, x6)  =  U6_gga(x1, x2, x3, x4, x6)
pI_in_gggga(x1, x2, x3, x4, x5)  =  pI_in_gggga(x1, x2, x3, x4)
U23_gggga(x1, x2, x3, x4, x5, x6)  =  U23_gggga(x1, x2, x3, x4, x6)
gtK_in_gg(x1, x2)  =  gtK_in_gg(x1, x2)
U8_gg(x1, x2, x3)  =  U8_gg(x1, x2, x3)
gtK_out_gg(x1, x2)  =  gtK_out_gg(x1, x2)
U24_gggga(x1, x2, x3, x4, x5, x6)  =  U24_gggga(x1, x2, x3, x4, x6)
pI_out_gggga(x1, x2, x3, x4, x5)  =  pI_out_gggga(x1, x2, x3, x4, x5)
pH_out_gggga(x1, x2, x3, x4, x5)  =  pH_out_gggga(x1, x2, x3, x4, x5)
pO_out_gaga(x1, x2, x3, x4)  =  pO_out_gaga(x1, x2, x3, x4)
pN_out_gagaa(x1, x2, x3, x4, x5)  =  pN_out_gagaa(x1, x2, x3, x4, x5)
pF_out_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pF_out_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)
U14_gaga(x1, x2, x3, x4, x5)  =  U14_gaga(x1, x2, x3, x5)
pM_out_gaga(x1, x2, x3, x4)  =  pM_out_gaga(x1, x2, x3, x4)
pL_out_ggagaa(x1, x2, x3, x4, x5, x6)  =  pL_out_ggagaa(x1, x2, x3, x4, x5, x6)
pB_out_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pB_out_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)
GTK_IN_GG(x1, x2)  =  GTK_IN_GG(x1, x2)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

GTK_IN_GG(s(T149), s(T150)) → GTK_IN_GG(T149, T150)

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

(10) PiDPToQDPProof (EQUIVALENT transformation)

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

(11) Obligation:

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

GTK_IN_GG(s(T149), s(T150)) → GTK_IN_GG(T149, T150)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • GTK_IN_GG(s(T149), s(T150)) → GTK_IN_GG(T149, T150)
    The graph contains the following edges 1 > 1, 2 > 2

(13) YES

(14) Obligation:

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

LEJ_IN_GG(s(T110), s(T111)) → LEJ_IN_GG(T110, T111)

The TRS R consists of the following rules:

mergesortA_in_ga([], []) → mergesortA_out_ga([], [])
mergesortA_in_ga(.(T4, []), .(T4, [])) → mergesortA_out_ga(.(T4, []), .(T4, []))
mergesortA_in_ga(.(T21, .(T22, T23)), T14) → U1_ga(T21, T22, T23, T14, pB_in_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14))
pB_in_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14) → U9_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_in_ggaa(T22, T23, T24, T25))
splitD_in_ggaa(T30, T31, .(T30, X58), X59) → U3_ggaa(T30, T31, X58, X59, splitC_in_gaa(T31, X59, X58))
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37), .(T36, X76), X77) → U2_gaa(T36, T37, X76, X77, splitC_in_gaa(T37, X77, X76))
U2_gaa(T36, T37, X76, X77, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U3_ggaa(T30, T31, X58, X59, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U9_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → U10_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pL_in_ggagaa(T21, T25, X22, T24, X23, T14))
pL_in_ggagaa(T21, T25, T38, T24, X23, T14) → U11_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_in_ga(.(T21, T25), T38))
U11_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_out_ga(.(T21, T25), T38)) → U12_ggagaa(T21, T25, T38, T24, X23, T14, pM_in_gaga(T24, X23, T38, T14))
pM_in_gaga(T24, T39, T38, T14) → U13_gaga(T24, T39, T38, T14, mergesortE_in_ga(T24, T39))
mergesortE_in_ga([], []) → mergesortE_out_ga([], [])
mergesortE_in_ga(.(T44, []), .(T44, [])) → mergesortE_out_ga(.(T44, []), .(T44, []))
mergesortE_in_ga(.(T51, .(T52, T53)), X105) → U4_ga(T51, T52, T53, X105, pF_in_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105))
pF_in_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105) → U15_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_in_ggaa(T51, .(T52, T53), T54, T55))
U15_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U16_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pN_in_gagaa(T54, X103, T55, X104, X105))
pN_in_gagaa(T54, T56, T55, X104, X105) → U17_gagaa(T54, T56, T55, X104, X105, mergesortE_in_ga(T54, T56))
U17_gagaa(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → U18_gagaa(T54, T56, T55, X104, X105, pO_in_gaga(T55, X104, T56, X105))
pO_in_gaga(T55, T57, T56, X105) → U19_gaga(T55, T57, T56, X105, mergesortE_in_ga(T55, T57))
U19_gaga(T55, T57, T56, X105, mergesortE_out_ga(T55, T57)) → U20_gaga(T55, T57, T56, X105, mergeG_in_gga(T56, T57, X105))
mergeG_in_gga(T66, [], T66) → mergeG_out_gga(T66, [], T66)
mergeG_in_gga([], T71, T71) → mergeG_out_gga([], T71, T71)
mergeG_in_gga(.(T92, T93), .(T94, T95), .(T92, T97)) → U5_gga(T92, T93, T94, T95, T97, pH_in_gggga(T92, T94, T93, T95, T97))
pH_in_gggga(T92, T94, T93, T95, T97) → U21_gggga(T92, T94, T93, T95, T97, leJ_in_gg(T92, T94))
leJ_in_gg(s(T110), s(T111)) → U7_gg(T110, T111, leJ_in_gg(T110, T111))
leJ_in_gg(0, s(T118)) → leJ_out_gg(0, s(T118))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U7_gg(T110, T111, leJ_out_gg(T110, T111)) → leJ_out_gg(s(T110), s(T111))
U21_gggga(T92, T94, T93, T95, T97, leJ_out_gg(T92, T94)) → U22_gggga(T92, T94, T93, T95, T97, mergeG_in_gga(T93, .(T94, T95), T97))
mergeG_in_gga(.(T131, T132), .(T133, T134), .(T133, T136)) → U6_gga(T131, T132, T133, T134, T136, pI_in_gggga(T131, T133, T132, T134, T136))
pI_in_gggga(T131, T133, T132, T134, T136) → U23_gggga(T131, T133, T132, T134, T136, gtK_in_gg(T131, T133))
gtK_in_gg(s(T149), s(T150)) → U8_gg(T149, T150, gtK_in_gg(T149, T150))
gtK_in_gg(s(T155), 0) → gtK_out_gg(s(T155), 0)
U8_gg(T149, T150, gtK_out_gg(T149, T150)) → gtK_out_gg(s(T149), s(T150))
U23_gggga(T131, T133, T132, T134, T136, gtK_out_gg(T131, T133)) → U24_gggga(T131, T133, T132, T134, T136, mergeG_in_gga(.(T131, T132), T134, T136))
U24_gggga(T131, T133, T132, T134, T136, mergeG_out_gga(.(T131, T132), T134, T136)) → pI_out_gggga(T131, T133, T132, T134, T136)
U6_gga(T131, T132, T133, T134, T136, pI_out_gggga(T131, T133, T132, T134, T136)) → mergeG_out_gga(.(T131, T132), .(T133, T134), .(T133, T136))
U22_gggga(T92, T94, T93, T95, T97, mergeG_out_gga(T93, .(T94, T95), T97)) → pH_out_gggga(T92, T94, T93, T95, T97)
U5_gga(T92, T93, T94, T95, T97, pH_out_gggga(T92, T94, T93, T95, T97)) → mergeG_out_gga(.(T92, T93), .(T94, T95), .(T92, T97))
U20_gaga(T55, T57, T56, X105, mergeG_out_gga(T56, T57, X105)) → pO_out_gaga(T55, T57, T56, X105)
U18_gagaa(T54, T56, T55, X104, X105, pO_out_gaga(T55, X104, T56, X105)) → pN_out_gagaa(T54, T56, T55, X104, X105)
U16_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pN_out_gagaa(T54, X103, T55, X104, X105)) → pF_out_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105)
U4_ga(T51, T52, T53, X105, pF_out_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105)) → mergesortE_out_ga(.(T51, .(T52, T53)), X105)
U13_gaga(T24, T39, T38, T14, mergesortE_out_ga(T24, T39)) → U14_gaga(T24, T39, T38, T14, mergeG_in_gga(T38, T39, T14))
U14_gaga(T24, T39, T38, T14, mergeG_out_gga(T38, T39, T14)) → pM_out_gaga(T24, T39, T38, T14)
U12_ggagaa(T21, T25, T38, T24, X23, T14, pM_out_gaga(T24, X23, T38, T14)) → pL_out_ggagaa(T21, T25, T38, T24, X23, T14)
U10_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pL_out_ggagaa(T21, T25, X22, T24, X23, T14)) → pB_out_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14)
U1_ga(T21, T22, T23, T14, pB_out_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14)) → mergesortA_out_ga(.(T21, .(T22, T23)), T14)

The argument filtering Pi contains the following mapping:
mergesortA_in_ga(x1, x2)  =  mergesortA_in_ga(x1)
[]  =  []
mergesortA_out_ga(x1, x2)  =  mergesortA_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
pB_in_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pB_in_ggaagaaa(x1, x2, x5)
U9_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U9_ggaagaaa(x1, x2, x5, x9)
splitD_in_ggaa(x1, x2, x3, x4)  =  splitD_in_ggaa(x1, x2)
U3_ggaa(x1, x2, x3, x4, x5)  =  U3_ggaa(x1, x2, x5)
splitC_in_gaa(x1, x2, x3)  =  splitC_in_gaa(x1)
splitC_out_gaa(x1, x2, x3)  =  splitC_out_gaa(x1, x2, x3)
U2_gaa(x1, x2, x3, x4, x5)  =  U2_gaa(x1, x2, x5)
splitD_out_ggaa(x1, x2, x3, x4)  =  splitD_out_ggaa(x1, x2, x3, x4)
U10_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U10_ggaagaaa(x1, x2, x3, x4, x5, x9)
pL_in_ggagaa(x1, x2, x3, x4, x5, x6)  =  pL_in_ggagaa(x1, x2, x4)
U11_ggagaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_ggagaa(x1, x2, x4, x7)
U12_ggagaa(x1, x2, x3, x4, x5, x6, x7)  =  U12_ggagaa(x1, x2, x3, x4, x7)
pM_in_gaga(x1, x2, x3, x4)  =  pM_in_gaga(x1, x3)
U13_gaga(x1, x2, x3, x4, x5)  =  U13_gaga(x1, x3, x5)
mergesortE_in_ga(x1, x2)  =  mergesortE_in_ga(x1)
mergesortE_out_ga(x1, x2)  =  mergesortE_out_ga(x1, x2)
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x2, x3, x5)
pF_in_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pF_in_gggaaaaa(x1, x2, x3)
U15_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U15_gggaaaaa(x1, x2, x3, x9)
U16_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U16_gggaaaaa(x1, x2, x3, x4, x5, x9)
pN_in_gagaa(x1, x2, x3, x4, x5)  =  pN_in_gagaa(x1, x3)
U17_gagaa(x1, x2, x3, x4, x5, x6)  =  U17_gagaa(x1, x3, x6)
U18_gagaa(x1, x2, x3, x4, x5, x6)  =  U18_gagaa(x1, x2, x3, x6)
pO_in_gaga(x1, x2, x3, x4)  =  pO_in_gaga(x1, x3)
U19_gaga(x1, x2, x3, x4, x5)  =  U19_gaga(x1, x3, x5)
U20_gaga(x1, x2, x3, x4, x5)  =  U20_gaga(x1, x2, x3, x5)
mergeG_in_gga(x1, x2, x3)  =  mergeG_in_gga(x1, x2)
mergeG_out_gga(x1, x2, x3)  =  mergeG_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4, x5, x6)  =  U5_gga(x1, x2, x3, x4, x6)
pH_in_gggga(x1, x2, x3, x4, x5)  =  pH_in_gggga(x1, x2, x3, x4)
U21_gggga(x1, x2, x3, x4, x5, x6)  =  U21_gggga(x1, x2, x3, x4, x6)
leJ_in_gg(x1, x2)  =  leJ_in_gg(x1, x2)
s(x1)  =  s(x1)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
0  =  0
leJ_out_gg(x1, x2)  =  leJ_out_gg(x1, x2)
U22_gggga(x1, x2, x3, x4, x5, x6)  =  U22_gggga(x1, x2, x3, x4, x6)
U6_gga(x1, x2, x3, x4, x5, x6)  =  U6_gga(x1, x2, x3, x4, x6)
pI_in_gggga(x1, x2, x3, x4, x5)  =  pI_in_gggga(x1, x2, x3, x4)
U23_gggga(x1, x2, x3, x4, x5, x6)  =  U23_gggga(x1, x2, x3, x4, x6)
gtK_in_gg(x1, x2)  =  gtK_in_gg(x1, x2)
U8_gg(x1, x2, x3)  =  U8_gg(x1, x2, x3)
gtK_out_gg(x1, x2)  =  gtK_out_gg(x1, x2)
U24_gggga(x1, x2, x3, x4, x5, x6)  =  U24_gggga(x1, x2, x3, x4, x6)
pI_out_gggga(x1, x2, x3, x4, x5)  =  pI_out_gggga(x1, x2, x3, x4, x5)
pH_out_gggga(x1, x2, x3, x4, x5)  =  pH_out_gggga(x1, x2, x3, x4, x5)
pO_out_gaga(x1, x2, x3, x4)  =  pO_out_gaga(x1, x2, x3, x4)
pN_out_gagaa(x1, x2, x3, x4, x5)  =  pN_out_gagaa(x1, x2, x3, x4, x5)
pF_out_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pF_out_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)
U14_gaga(x1, x2, x3, x4, x5)  =  U14_gaga(x1, x2, x3, x5)
pM_out_gaga(x1, x2, x3, x4)  =  pM_out_gaga(x1, x2, x3, x4)
pL_out_ggagaa(x1, x2, x3, x4, x5, x6)  =  pL_out_ggagaa(x1, x2, x3, x4, x5, x6)
pB_out_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pB_out_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)
LEJ_IN_GG(x1, x2)  =  LEJ_IN_GG(x1, x2)

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

LEJ_IN_GG(s(T110), s(T111)) → LEJ_IN_GG(T110, T111)

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

(17) PiDPToQDPProof (EQUIVALENT transformation)

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

(18) Obligation:

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

LEJ_IN_GG(s(T110), s(T111)) → LEJ_IN_GG(T110, T111)

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • LEJ_IN_GG(s(T110), s(T111)) → LEJ_IN_GG(T110, T111)
    The graph contains the following edges 1 > 1, 2 > 2

(20) YES

(21) Obligation:

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

MERGEG_IN_GGA(.(T92, T93), .(T94, T95), .(T92, T97)) → PH_IN_GGGGA(T92, T94, T93, T95, T97)
PH_IN_GGGGA(T92, T94, T93, T95, T97) → U21_GGGGA(T92, T94, T93, T95, T97, leJ_in_gg(T92, T94))
U21_GGGGA(T92, T94, T93, T95, T97, leJ_out_gg(T92, T94)) → MERGEG_IN_GGA(T93, .(T94, T95), T97)
MERGEG_IN_GGA(.(T131, T132), .(T133, T134), .(T133, T136)) → PI_IN_GGGGA(T131, T133, T132, T134, T136)
PI_IN_GGGGA(T131, T133, T132, T134, T136) → U23_GGGGA(T131, T133, T132, T134, T136, gtK_in_gg(T131, T133))
U23_GGGGA(T131, T133, T132, T134, T136, gtK_out_gg(T131, T133)) → MERGEG_IN_GGA(.(T131, T132), T134, T136)

The TRS R consists of the following rules:

mergesortA_in_ga([], []) → mergesortA_out_ga([], [])
mergesortA_in_ga(.(T4, []), .(T4, [])) → mergesortA_out_ga(.(T4, []), .(T4, []))
mergesortA_in_ga(.(T21, .(T22, T23)), T14) → U1_ga(T21, T22, T23, T14, pB_in_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14))
pB_in_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14) → U9_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_in_ggaa(T22, T23, T24, T25))
splitD_in_ggaa(T30, T31, .(T30, X58), X59) → U3_ggaa(T30, T31, X58, X59, splitC_in_gaa(T31, X59, X58))
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37), .(T36, X76), X77) → U2_gaa(T36, T37, X76, X77, splitC_in_gaa(T37, X77, X76))
U2_gaa(T36, T37, X76, X77, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U3_ggaa(T30, T31, X58, X59, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U9_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → U10_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pL_in_ggagaa(T21, T25, X22, T24, X23, T14))
pL_in_ggagaa(T21, T25, T38, T24, X23, T14) → U11_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_in_ga(.(T21, T25), T38))
U11_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_out_ga(.(T21, T25), T38)) → U12_ggagaa(T21, T25, T38, T24, X23, T14, pM_in_gaga(T24, X23, T38, T14))
pM_in_gaga(T24, T39, T38, T14) → U13_gaga(T24, T39, T38, T14, mergesortE_in_ga(T24, T39))
mergesortE_in_ga([], []) → mergesortE_out_ga([], [])
mergesortE_in_ga(.(T44, []), .(T44, [])) → mergesortE_out_ga(.(T44, []), .(T44, []))
mergesortE_in_ga(.(T51, .(T52, T53)), X105) → U4_ga(T51, T52, T53, X105, pF_in_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105))
pF_in_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105) → U15_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_in_ggaa(T51, .(T52, T53), T54, T55))
U15_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U16_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pN_in_gagaa(T54, X103, T55, X104, X105))
pN_in_gagaa(T54, T56, T55, X104, X105) → U17_gagaa(T54, T56, T55, X104, X105, mergesortE_in_ga(T54, T56))
U17_gagaa(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → U18_gagaa(T54, T56, T55, X104, X105, pO_in_gaga(T55, X104, T56, X105))
pO_in_gaga(T55, T57, T56, X105) → U19_gaga(T55, T57, T56, X105, mergesortE_in_ga(T55, T57))
U19_gaga(T55, T57, T56, X105, mergesortE_out_ga(T55, T57)) → U20_gaga(T55, T57, T56, X105, mergeG_in_gga(T56, T57, X105))
mergeG_in_gga(T66, [], T66) → mergeG_out_gga(T66, [], T66)
mergeG_in_gga([], T71, T71) → mergeG_out_gga([], T71, T71)
mergeG_in_gga(.(T92, T93), .(T94, T95), .(T92, T97)) → U5_gga(T92, T93, T94, T95, T97, pH_in_gggga(T92, T94, T93, T95, T97))
pH_in_gggga(T92, T94, T93, T95, T97) → U21_gggga(T92, T94, T93, T95, T97, leJ_in_gg(T92, T94))
leJ_in_gg(s(T110), s(T111)) → U7_gg(T110, T111, leJ_in_gg(T110, T111))
leJ_in_gg(0, s(T118)) → leJ_out_gg(0, s(T118))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U7_gg(T110, T111, leJ_out_gg(T110, T111)) → leJ_out_gg(s(T110), s(T111))
U21_gggga(T92, T94, T93, T95, T97, leJ_out_gg(T92, T94)) → U22_gggga(T92, T94, T93, T95, T97, mergeG_in_gga(T93, .(T94, T95), T97))
mergeG_in_gga(.(T131, T132), .(T133, T134), .(T133, T136)) → U6_gga(T131, T132, T133, T134, T136, pI_in_gggga(T131, T133, T132, T134, T136))
pI_in_gggga(T131, T133, T132, T134, T136) → U23_gggga(T131, T133, T132, T134, T136, gtK_in_gg(T131, T133))
gtK_in_gg(s(T149), s(T150)) → U8_gg(T149, T150, gtK_in_gg(T149, T150))
gtK_in_gg(s(T155), 0) → gtK_out_gg(s(T155), 0)
U8_gg(T149, T150, gtK_out_gg(T149, T150)) → gtK_out_gg(s(T149), s(T150))
U23_gggga(T131, T133, T132, T134, T136, gtK_out_gg(T131, T133)) → U24_gggga(T131, T133, T132, T134, T136, mergeG_in_gga(.(T131, T132), T134, T136))
U24_gggga(T131, T133, T132, T134, T136, mergeG_out_gga(.(T131, T132), T134, T136)) → pI_out_gggga(T131, T133, T132, T134, T136)
U6_gga(T131, T132, T133, T134, T136, pI_out_gggga(T131, T133, T132, T134, T136)) → mergeG_out_gga(.(T131, T132), .(T133, T134), .(T133, T136))
U22_gggga(T92, T94, T93, T95, T97, mergeG_out_gga(T93, .(T94, T95), T97)) → pH_out_gggga(T92, T94, T93, T95, T97)
U5_gga(T92, T93, T94, T95, T97, pH_out_gggga(T92, T94, T93, T95, T97)) → mergeG_out_gga(.(T92, T93), .(T94, T95), .(T92, T97))
U20_gaga(T55, T57, T56, X105, mergeG_out_gga(T56, T57, X105)) → pO_out_gaga(T55, T57, T56, X105)
U18_gagaa(T54, T56, T55, X104, X105, pO_out_gaga(T55, X104, T56, X105)) → pN_out_gagaa(T54, T56, T55, X104, X105)
U16_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pN_out_gagaa(T54, X103, T55, X104, X105)) → pF_out_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105)
U4_ga(T51, T52, T53, X105, pF_out_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105)) → mergesortE_out_ga(.(T51, .(T52, T53)), X105)
U13_gaga(T24, T39, T38, T14, mergesortE_out_ga(T24, T39)) → U14_gaga(T24, T39, T38, T14, mergeG_in_gga(T38, T39, T14))
U14_gaga(T24, T39, T38, T14, mergeG_out_gga(T38, T39, T14)) → pM_out_gaga(T24, T39, T38, T14)
U12_ggagaa(T21, T25, T38, T24, X23, T14, pM_out_gaga(T24, X23, T38, T14)) → pL_out_ggagaa(T21, T25, T38, T24, X23, T14)
U10_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pL_out_ggagaa(T21, T25, X22, T24, X23, T14)) → pB_out_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14)
U1_ga(T21, T22, T23, T14, pB_out_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14)) → mergesortA_out_ga(.(T21, .(T22, T23)), T14)

The argument filtering Pi contains the following mapping:
mergesortA_in_ga(x1, x2)  =  mergesortA_in_ga(x1)
[]  =  []
mergesortA_out_ga(x1, x2)  =  mergesortA_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
pB_in_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pB_in_ggaagaaa(x1, x2, x5)
U9_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U9_ggaagaaa(x1, x2, x5, x9)
splitD_in_ggaa(x1, x2, x3, x4)  =  splitD_in_ggaa(x1, x2)
U3_ggaa(x1, x2, x3, x4, x5)  =  U3_ggaa(x1, x2, x5)
splitC_in_gaa(x1, x2, x3)  =  splitC_in_gaa(x1)
splitC_out_gaa(x1, x2, x3)  =  splitC_out_gaa(x1, x2, x3)
U2_gaa(x1, x2, x3, x4, x5)  =  U2_gaa(x1, x2, x5)
splitD_out_ggaa(x1, x2, x3, x4)  =  splitD_out_ggaa(x1, x2, x3, x4)
U10_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U10_ggaagaaa(x1, x2, x3, x4, x5, x9)
pL_in_ggagaa(x1, x2, x3, x4, x5, x6)  =  pL_in_ggagaa(x1, x2, x4)
U11_ggagaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_ggagaa(x1, x2, x4, x7)
U12_ggagaa(x1, x2, x3, x4, x5, x6, x7)  =  U12_ggagaa(x1, x2, x3, x4, x7)
pM_in_gaga(x1, x2, x3, x4)  =  pM_in_gaga(x1, x3)
U13_gaga(x1, x2, x3, x4, x5)  =  U13_gaga(x1, x3, x5)
mergesortE_in_ga(x1, x2)  =  mergesortE_in_ga(x1)
mergesortE_out_ga(x1, x2)  =  mergesortE_out_ga(x1, x2)
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x2, x3, x5)
pF_in_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pF_in_gggaaaaa(x1, x2, x3)
U15_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U15_gggaaaaa(x1, x2, x3, x9)
U16_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U16_gggaaaaa(x1, x2, x3, x4, x5, x9)
pN_in_gagaa(x1, x2, x3, x4, x5)  =  pN_in_gagaa(x1, x3)
U17_gagaa(x1, x2, x3, x4, x5, x6)  =  U17_gagaa(x1, x3, x6)
U18_gagaa(x1, x2, x3, x4, x5, x6)  =  U18_gagaa(x1, x2, x3, x6)
pO_in_gaga(x1, x2, x3, x4)  =  pO_in_gaga(x1, x3)
U19_gaga(x1, x2, x3, x4, x5)  =  U19_gaga(x1, x3, x5)
U20_gaga(x1, x2, x3, x4, x5)  =  U20_gaga(x1, x2, x3, x5)
mergeG_in_gga(x1, x2, x3)  =  mergeG_in_gga(x1, x2)
mergeG_out_gga(x1, x2, x3)  =  mergeG_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4, x5, x6)  =  U5_gga(x1, x2, x3, x4, x6)
pH_in_gggga(x1, x2, x3, x4, x5)  =  pH_in_gggga(x1, x2, x3, x4)
U21_gggga(x1, x2, x3, x4, x5, x6)  =  U21_gggga(x1, x2, x3, x4, x6)
leJ_in_gg(x1, x2)  =  leJ_in_gg(x1, x2)
s(x1)  =  s(x1)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
0  =  0
leJ_out_gg(x1, x2)  =  leJ_out_gg(x1, x2)
U22_gggga(x1, x2, x3, x4, x5, x6)  =  U22_gggga(x1, x2, x3, x4, x6)
U6_gga(x1, x2, x3, x4, x5, x6)  =  U6_gga(x1, x2, x3, x4, x6)
pI_in_gggga(x1, x2, x3, x4, x5)  =  pI_in_gggga(x1, x2, x3, x4)
U23_gggga(x1, x2, x3, x4, x5, x6)  =  U23_gggga(x1, x2, x3, x4, x6)
gtK_in_gg(x1, x2)  =  gtK_in_gg(x1, x2)
U8_gg(x1, x2, x3)  =  U8_gg(x1, x2, x3)
gtK_out_gg(x1, x2)  =  gtK_out_gg(x1, x2)
U24_gggga(x1, x2, x3, x4, x5, x6)  =  U24_gggga(x1, x2, x3, x4, x6)
pI_out_gggga(x1, x2, x3, x4, x5)  =  pI_out_gggga(x1, x2, x3, x4, x5)
pH_out_gggga(x1, x2, x3, x4, x5)  =  pH_out_gggga(x1, x2, x3, x4, x5)
pO_out_gaga(x1, x2, x3, x4)  =  pO_out_gaga(x1, x2, x3, x4)
pN_out_gagaa(x1, x2, x3, x4, x5)  =  pN_out_gagaa(x1, x2, x3, x4, x5)
pF_out_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pF_out_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)
U14_gaga(x1, x2, x3, x4, x5)  =  U14_gaga(x1, x2, x3, x5)
pM_out_gaga(x1, x2, x3, x4)  =  pM_out_gaga(x1, x2, x3, x4)
pL_out_ggagaa(x1, x2, x3, x4, x5, x6)  =  pL_out_ggagaa(x1, x2, x3, x4, x5, x6)
pB_out_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pB_out_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)
MERGEG_IN_GGA(x1, x2, x3)  =  MERGEG_IN_GGA(x1, x2)
PH_IN_GGGGA(x1, x2, x3, x4, x5)  =  PH_IN_GGGGA(x1, x2, x3, x4)
U21_GGGGA(x1, x2, x3, x4, x5, x6)  =  U21_GGGGA(x1, x2, x3, x4, x6)
PI_IN_GGGGA(x1, x2, x3, x4, x5)  =  PI_IN_GGGGA(x1, x2, x3, x4)
U23_GGGGA(x1, x2, x3, x4, x5, x6)  =  U23_GGGGA(x1, x2, x3, x4, x6)

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

MERGEG_IN_GGA(.(T92, T93), .(T94, T95), .(T92, T97)) → PH_IN_GGGGA(T92, T94, T93, T95, T97)
PH_IN_GGGGA(T92, T94, T93, T95, T97) → U21_GGGGA(T92, T94, T93, T95, T97, leJ_in_gg(T92, T94))
U21_GGGGA(T92, T94, T93, T95, T97, leJ_out_gg(T92, T94)) → MERGEG_IN_GGA(T93, .(T94, T95), T97)
MERGEG_IN_GGA(.(T131, T132), .(T133, T134), .(T133, T136)) → PI_IN_GGGGA(T131, T133, T132, T134, T136)
PI_IN_GGGGA(T131, T133, T132, T134, T136) → U23_GGGGA(T131, T133, T132, T134, T136, gtK_in_gg(T131, T133))
U23_GGGGA(T131, T133, T132, T134, T136, gtK_out_gg(T131, T133)) → MERGEG_IN_GGA(.(T131, T132), T134, T136)

The TRS R consists of the following rules:

leJ_in_gg(s(T110), s(T111)) → U7_gg(T110, T111, leJ_in_gg(T110, T111))
leJ_in_gg(0, s(T118)) → leJ_out_gg(0, s(T118))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
gtK_in_gg(s(T149), s(T150)) → U8_gg(T149, T150, gtK_in_gg(T149, T150))
gtK_in_gg(s(T155), 0) → gtK_out_gg(s(T155), 0)
U7_gg(T110, T111, leJ_out_gg(T110, T111)) → leJ_out_gg(s(T110), s(T111))
U8_gg(T149, T150, gtK_out_gg(T149, T150)) → gtK_out_gg(s(T149), s(T150))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
leJ_in_gg(x1, x2)  =  leJ_in_gg(x1, x2)
s(x1)  =  s(x1)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
0  =  0
leJ_out_gg(x1, x2)  =  leJ_out_gg(x1, x2)
gtK_in_gg(x1, x2)  =  gtK_in_gg(x1, x2)
U8_gg(x1, x2, x3)  =  U8_gg(x1, x2, x3)
gtK_out_gg(x1, x2)  =  gtK_out_gg(x1, x2)
MERGEG_IN_GGA(x1, x2, x3)  =  MERGEG_IN_GGA(x1, x2)
PH_IN_GGGGA(x1, x2, x3, x4, x5)  =  PH_IN_GGGGA(x1, x2, x3, x4)
U21_GGGGA(x1, x2, x3, x4, x5, x6)  =  U21_GGGGA(x1, x2, x3, x4, x6)
PI_IN_GGGGA(x1, x2, x3, x4, x5)  =  PI_IN_GGGGA(x1, x2, x3, x4)
U23_GGGGA(x1, x2, x3, x4, x5, x6)  =  U23_GGGGA(x1, x2, x3, x4, x6)

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

MERGEG_IN_GGA(.(T92, T93), .(T94, T95)) → PH_IN_GGGGA(T92, T94, T93, T95)
PH_IN_GGGGA(T92, T94, T93, T95) → U21_GGGGA(T92, T94, T93, T95, leJ_in_gg(T92, T94))
U21_GGGGA(T92, T94, T93, T95, leJ_out_gg(T92, T94)) → MERGEG_IN_GGA(T93, .(T94, T95))
MERGEG_IN_GGA(.(T131, T132), .(T133, T134)) → PI_IN_GGGGA(T131, T133, T132, T134)
PI_IN_GGGGA(T131, T133, T132, T134) → U23_GGGGA(T131, T133, T132, T134, gtK_in_gg(T131, T133))
U23_GGGGA(T131, T133, T132, T134, gtK_out_gg(T131, T133)) → MERGEG_IN_GGA(.(T131, T132), T134)

The TRS R consists of the following rules:

leJ_in_gg(s(T110), s(T111)) → U7_gg(T110, T111, leJ_in_gg(T110, T111))
leJ_in_gg(0, s(T118)) → leJ_out_gg(0, s(T118))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
gtK_in_gg(s(T149), s(T150)) → U8_gg(T149, T150, gtK_in_gg(T149, T150))
gtK_in_gg(s(T155), 0) → gtK_out_gg(s(T155), 0)
U7_gg(T110, T111, leJ_out_gg(T110, T111)) → leJ_out_gg(s(T110), s(T111))
U8_gg(T149, T150, gtK_out_gg(T149, T150)) → gtK_out_gg(s(T149), s(T150))

The set Q consists of the following terms:

leJ_in_gg(x0, x1)
gtK_in_gg(x0, x1)
U7_gg(x0, x1, x2)
U8_gg(x0, x1, x2)

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

(26) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

MERGEG_IN_GGA(.(T92, T93), .(T94, T95)) → PH_IN_GGGGA(T92, T94, T93, T95)
MERGEG_IN_GGA(.(T131, T132), .(T133, T134)) → PI_IN_GGGGA(T131, T133, T132, T134)


Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 1 + 2·x1 + 2·x2   
POL(0) = 0   
POL(MERGEG_IN_GGA(x1, x2)) = x1 + x2   
POL(PH_IN_GGGGA(x1, x2, x3, x4)) = 1 + 2·x1 + 2·x2 + 2·x3 + 2·x4   
POL(PI_IN_GGGGA(x1, x2, x3, x4)) = 1 + 2·x1 + 2·x2 + 2·x3 + 2·x4   
POL(U21_GGGGA(x1, x2, x3, x4, x5)) = 1 + x1 + x2 + 2·x3 + 2·x4 + x5   
POL(U23_GGGGA(x1, x2, x3, x4, x5)) = 1 + x1 + x2 + 2·x3 + x4 + x5   
POL(U7_gg(x1, x2, x3)) = x1 + x2 + x3   
POL(U8_gg(x1, x2, x3)) = x1 + x2 + x3   
POL(gtK_in_gg(x1, x2)) = x1 + x2   
POL(gtK_out_gg(x1, x2)) = x1 + x2   
POL(leJ_in_gg(x1, x2)) = x1 + x2   
POL(leJ_out_gg(x1, x2)) = x1 + x2   
POL(s(x1)) = 2·x1   

(27) Obligation:

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

PH_IN_GGGGA(T92, T94, T93, T95) → U21_GGGGA(T92, T94, T93, T95, leJ_in_gg(T92, T94))
U21_GGGGA(T92, T94, T93, T95, leJ_out_gg(T92, T94)) → MERGEG_IN_GGA(T93, .(T94, T95))
PI_IN_GGGGA(T131, T133, T132, T134) → U23_GGGGA(T131, T133, T132, T134, gtK_in_gg(T131, T133))
U23_GGGGA(T131, T133, T132, T134, gtK_out_gg(T131, T133)) → MERGEG_IN_GGA(.(T131, T132), T134)

The TRS R consists of the following rules:

leJ_in_gg(s(T110), s(T111)) → U7_gg(T110, T111, leJ_in_gg(T110, T111))
leJ_in_gg(0, s(T118)) → leJ_out_gg(0, s(T118))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
gtK_in_gg(s(T149), s(T150)) → U8_gg(T149, T150, gtK_in_gg(T149, T150))
gtK_in_gg(s(T155), 0) → gtK_out_gg(s(T155), 0)
U7_gg(T110, T111, leJ_out_gg(T110, T111)) → leJ_out_gg(s(T110), s(T111))
U8_gg(T149, T150, gtK_out_gg(T149, T150)) → gtK_out_gg(s(T149), s(T150))

The set Q consists of the following terms:

leJ_in_gg(x0, x1)
gtK_in_gg(x0, x1)
U7_gg(x0, x1, x2)
U8_gg(x0, x1, x2)

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

(28) DependencyGraphProof (EQUIVALENT transformation)

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

(29) TRUE

(30) Obligation:

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

SPLITC_IN_GAA(.(T36, T37), .(T36, X76), X77) → SPLITC_IN_GAA(T37, X77, X76)

The TRS R consists of the following rules:

mergesortA_in_ga([], []) → mergesortA_out_ga([], [])
mergesortA_in_ga(.(T4, []), .(T4, [])) → mergesortA_out_ga(.(T4, []), .(T4, []))
mergesortA_in_ga(.(T21, .(T22, T23)), T14) → U1_ga(T21, T22, T23, T14, pB_in_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14))
pB_in_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14) → U9_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_in_ggaa(T22, T23, T24, T25))
splitD_in_ggaa(T30, T31, .(T30, X58), X59) → U3_ggaa(T30, T31, X58, X59, splitC_in_gaa(T31, X59, X58))
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37), .(T36, X76), X77) → U2_gaa(T36, T37, X76, X77, splitC_in_gaa(T37, X77, X76))
U2_gaa(T36, T37, X76, X77, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U3_ggaa(T30, T31, X58, X59, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U9_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → U10_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pL_in_ggagaa(T21, T25, X22, T24, X23, T14))
pL_in_ggagaa(T21, T25, T38, T24, X23, T14) → U11_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_in_ga(.(T21, T25), T38))
U11_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_out_ga(.(T21, T25), T38)) → U12_ggagaa(T21, T25, T38, T24, X23, T14, pM_in_gaga(T24, X23, T38, T14))
pM_in_gaga(T24, T39, T38, T14) → U13_gaga(T24, T39, T38, T14, mergesortE_in_ga(T24, T39))
mergesortE_in_ga([], []) → mergesortE_out_ga([], [])
mergesortE_in_ga(.(T44, []), .(T44, [])) → mergesortE_out_ga(.(T44, []), .(T44, []))
mergesortE_in_ga(.(T51, .(T52, T53)), X105) → U4_ga(T51, T52, T53, X105, pF_in_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105))
pF_in_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105) → U15_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_in_ggaa(T51, .(T52, T53), T54, T55))
U15_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U16_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pN_in_gagaa(T54, X103, T55, X104, X105))
pN_in_gagaa(T54, T56, T55, X104, X105) → U17_gagaa(T54, T56, T55, X104, X105, mergesortE_in_ga(T54, T56))
U17_gagaa(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → U18_gagaa(T54, T56, T55, X104, X105, pO_in_gaga(T55, X104, T56, X105))
pO_in_gaga(T55, T57, T56, X105) → U19_gaga(T55, T57, T56, X105, mergesortE_in_ga(T55, T57))
U19_gaga(T55, T57, T56, X105, mergesortE_out_ga(T55, T57)) → U20_gaga(T55, T57, T56, X105, mergeG_in_gga(T56, T57, X105))
mergeG_in_gga(T66, [], T66) → mergeG_out_gga(T66, [], T66)
mergeG_in_gga([], T71, T71) → mergeG_out_gga([], T71, T71)
mergeG_in_gga(.(T92, T93), .(T94, T95), .(T92, T97)) → U5_gga(T92, T93, T94, T95, T97, pH_in_gggga(T92, T94, T93, T95, T97))
pH_in_gggga(T92, T94, T93, T95, T97) → U21_gggga(T92, T94, T93, T95, T97, leJ_in_gg(T92, T94))
leJ_in_gg(s(T110), s(T111)) → U7_gg(T110, T111, leJ_in_gg(T110, T111))
leJ_in_gg(0, s(T118)) → leJ_out_gg(0, s(T118))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U7_gg(T110, T111, leJ_out_gg(T110, T111)) → leJ_out_gg(s(T110), s(T111))
U21_gggga(T92, T94, T93, T95, T97, leJ_out_gg(T92, T94)) → U22_gggga(T92, T94, T93, T95, T97, mergeG_in_gga(T93, .(T94, T95), T97))
mergeG_in_gga(.(T131, T132), .(T133, T134), .(T133, T136)) → U6_gga(T131, T132, T133, T134, T136, pI_in_gggga(T131, T133, T132, T134, T136))
pI_in_gggga(T131, T133, T132, T134, T136) → U23_gggga(T131, T133, T132, T134, T136, gtK_in_gg(T131, T133))
gtK_in_gg(s(T149), s(T150)) → U8_gg(T149, T150, gtK_in_gg(T149, T150))
gtK_in_gg(s(T155), 0) → gtK_out_gg(s(T155), 0)
U8_gg(T149, T150, gtK_out_gg(T149, T150)) → gtK_out_gg(s(T149), s(T150))
U23_gggga(T131, T133, T132, T134, T136, gtK_out_gg(T131, T133)) → U24_gggga(T131, T133, T132, T134, T136, mergeG_in_gga(.(T131, T132), T134, T136))
U24_gggga(T131, T133, T132, T134, T136, mergeG_out_gga(.(T131, T132), T134, T136)) → pI_out_gggga(T131, T133, T132, T134, T136)
U6_gga(T131, T132, T133, T134, T136, pI_out_gggga(T131, T133, T132, T134, T136)) → mergeG_out_gga(.(T131, T132), .(T133, T134), .(T133, T136))
U22_gggga(T92, T94, T93, T95, T97, mergeG_out_gga(T93, .(T94, T95), T97)) → pH_out_gggga(T92, T94, T93, T95, T97)
U5_gga(T92, T93, T94, T95, T97, pH_out_gggga(T92, T94, T93, T95, T97)) → mergeG_out_gga(.(T92, T93), .(T94, T95), .(T92, T97))
U20_gaga(T55, T57, T56, X105, mergeG_out_gga(T56, T57, X105)) → pO_out_gaga(T55, T57, T56, X105)
U18_gagaa(T54, T56, T55, X104, X105, pO_out_gaga(T55, X104, T56, X105)) → pN_out_gagaa(T54, T56, T55, X104, X105)
U16_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pN_out_gagaa(T54, X103, T55, X104, X105)) → pF_out_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105)
U4_ga(T51, T52, T53, X105, pF_out_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105)) → mergesortE_out_ga(.(T51, .(T52, T53)), X105)
U13_gaga(T24, T39, T38, T14, mergesortE_out_ga(T24, T39)) → U14_gaga(T24, T39, T38, T14, mergeG_in_gga(T38, T39, T14))
U14_gaga(T24, T39, T38, T14, mergeG_out_gga(T38, T39, T14)) → pM_out_gaga(T24, T39, T38, T14)
U12_ggagaa(T21, T25, T38, T24, X23, T14, pM_out_gaga(T24, X23, T38, T14)) → pL_out_ggagaa(T21, T25, T38, T24, X23, T14)
U10_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pL_out_ggagaa(T21, T25, X22, T24, X23, T14)) → pB_out_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14)
U1_ga(T21, T22, T23, T14, pB_out_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14)) → mergesortA_out_ga(.(T21, .(T22, T23)), T14)

The argument filtering Pi contains the following mapping:
mergesortA_in_ga(x1, x2)  =  mergesortA_in_ga(x1)
[]  =  []
mergesortA_out_ga(x1, x2)  =  mergesortA_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
pB_in_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pB_in_ggaagaaa(x1, x2, x5)
U9_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U9_ggaagaaa(x1, x2, x5, x9)
splitD_in_ggaa(x1, x2, x3, x4)  =  splitD_in_ggaa(x1, x2)
U3_ggaa(x1, x2, x3, x4, x5)  =  U3_ggaa(x1, x2, x5)
splitC_in_gaa(x1, x2, x3)  =  splitC_in_gaa(x1)
splitC_out_gaa(x1, x2, x3)  =  splitC_out_gaa(x1, x2, x3)
U2_gaa(x1, x2, x3, x4, x5)  =  U2_gaa(x1, x2, x5)
splitD_out_ggaa(x1, x2, x3, x4)  =  splitD_out_ggaa(x1, x2, x3, x4)
U10_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U10_ggaagaaa(x1, x2, x3, x4, x5, x9)
pL_in_ggagaa(x1, x2, x3, x4, x5, x6)  =  pL_in_ggagaa(x1, x2, x4)
U11_ggagaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_ggagaa(x1, x2, x4, x7)
U12_ggagaa(x1, x2, x3, x4, x5, x6, x7)  =  U12_ggagaa(x1, x2, x3, x4, x7)
pM_in_gaga(x1, x2, x3, x4)  =  pM_in_gaga(x1, x3)
U13_gaga(x1, x2, x3, x4, x5)  =  U13_gaga(x1, x3, x5)
mergesortE_in_ga(x1, x2)  =  mergesortE_in_ga(x1)
mergesortE_out_ga(x1, x2)  =  mergesortE_out_ga(x1, x2)
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x2, x3, x5)
pF_in_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pF_in_gggaaaaa(x1, x2, x3)
U15_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U15_gggaaaaa(x1, x2, x3, x9)
U16_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U16_gggaaaaa(x1, x2, x3, x4, x5, x9)
pN_in_gagaa(x1, x2, x3, x4, x5)  =  pN_in_gagaa(x1, x3)
U17_gagaa(x1, x2, x3, x4, x5, x6)  =  U17_gagaa(x1, x3, x6)
U18_gagaa(x1, x2, x3, x4, x5, x6)  =  U18_gagaa(x1, x2, x3, x6)
pO_in_gaga(x1, x2, x3, x4)  =  pO_in_gaga(x1, x3)
U19_gaga(x1, x2, x3, x4, x5)  =  U19_gaga(x1, x3, x5)
U20_gaga(x1, x2, x3, x4, x5)  =  U20_gaga(x1, x2, x3, x5)
mergeG_in_gga(x1, x2, x3)  =  mergeG_in_gga(x1, x2)
mergeG_out_gga(x1, x2, x3)  =  mergeG_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4, x5, x6)  =  U5_gga(x1, x2, x3, x4, x6)
pH_in_gggga(x1, x2, x3, x4, x5)  =  pH_in_gggga(x1, x2, x3, x4)
U21_gggga(x1, x2, x3, x4, x5, x6)  =  U21_gggga(x1, x2, x3, x4, x6)
leJ_in_gg(x1, x2)  =  leJ_in_gg(x1, x2)
s(x1)  =  s(x1)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
0  =  0
leJ_out_gg(x1, x2)  =  leJ_out_gg(x1, x2)
U22_gggga(x1, x2, x3, x4, x5, x6)  =  U22_gggga(x1, x2, x3, x4, x6)
U6_gga(x1, x2, x3, x4, x5, x6)  =  U6_gga(x1, x2, x3, x4, x6)
pI_in_gggga(x1, x2, x3, x4, x5)  =  pI_in_gggga(x1, x2, x3, x4)
U23_gggga(x1, x2, x3, x4, x5, x6)  =  U23_gggga(x1, x2, x3, x4, x6)
gtK_in_gg(x1, x2)  =  gtK_in_gg(x1, x2)
U8_gg(x1, x2, x3)  =  U8_gg(x1, x2, x3)
gtK_out_gg(x1, x2)  =  gtK_out_gg(x1, x2)
U24_gggga(x1, x2, x3, x4, x5, x6)  =  U24_gggga(x1, x2, x3, x4, x6)
pI_out_gggga(x1, x2, x3, x4, x5)  =  pI_out_gggga(x1, x2, x3, x4, x5)
pH_out_gggga(x1, x2, x3, x4, x5)  =  pH_out_gggga(x1, x2, x3, x4, x5)
pO_out_gaga(x1, x2, x3, x4)  =  pO_out_gaga(x1, x2, x3, x4)
pN_out_gagaa(x1, x2, x3, x4, x5)  =  pN_out_gagaa(x1, x2, x3, x4, x5)
pF_out_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pF_out_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)
U14_gaga(x1, x2, x3, x4, x5)  =  U14_gaga(x1, x2, x3, x5)
pM_out_gaga(x1, x2, x3, x4)  =  pM_out_gaga(x1, x2, x3, x4)
pL_out_ggagaa(x1, x2, x3, x4, x5, x6)  =  pL_out_ggagaa(x1, x2, x3, x4, x5, x6)
pB_out_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pB_out_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)
SPLITC_IN_GAA(x1, x2, x3)  =  SPLITC_IN_GAA(x1)

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

(31) UsableRulesProof (EQUIVALENT transformation)

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

(32) Obligation:

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

SPLITC_IN_GAA(.(T36, T37), .(T36, X76), X77) → SPLITC_IN_GAA(T37, X77, X76)

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

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

(33) PiDPToQDPProof (SOUND transformation)

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

(34) Obligation:

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

SPLITC_IN_GAA(.(T36, T37)) → SPLITC_IN_GAA(T37)

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

(35) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • SPLITC_IN_GAA(.(T36, T37)) → SPLITC_IN_GAA(T37)
    The graph contains the following edges 1 > 1

(36) YES

(37) Obligation:

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

PF_IN_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105) → U15_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105, splitD_in_ggaa(T51, .(T52, T53), T54, T55))
U15_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → PN_IN_GAGAA(T54, X103, T55, X104, X105)
PN_IN_GAGAA(T54, T56, T55, X104, X105) → U17_GAGAA(T54, T56, T55, X104, X105, mergesortE_in_ga(T54, T56))
U17_GAGAA(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → PO_IN_GAGA(T55, X104, T56, X105)
PO_IN_GAGA(T55, T57, T56, X105) → MERGESORTE_IN_GA(T55, T57)
MERGESORTE_IN_GA(.(T51, .(T52, T53)), X105) → PF_IN_GGGAAAAA(T51, T52, T53, X101, X102, X103, X104, X105)
PN_IN_GAGAA(T54, T56, T55, X104, X105) → MERGESORTE_IN_GA(T54, T56)

The TRS R consists of the following rules:

mergesortA_in_ga([], []) → mergesortA_out_ga([], [])
mergesortA_in_ga(.(T4, []), .(T4, [])) → mergesortA_out_ga(.(T4, []), .(T4, []))
mergesortA_in_ga(.(T21, .(T22, T23)), T14) → U1_ga(T21, T22, T23, T14, pB_in_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14))
pB_in_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14) → U9_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_in_ggaa(T22, T23, T24, T25))
splitD_in_ggaa(T30, T31, .(T30, X58), X59) → U3_ggaa(T30, T31, X58, X59, splitC_in_gaa(T31, X59, X58))
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37), .(T36, X76), X77) → U2_gaa(T36, T37, X76, X77, splitC_in_gaa(T37, X77, X76))
U2_gaa(T36, T37, X76, X77, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U3_ggaa(T30, T31, X58, X59, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U9_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → U10_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pL_in_ggagaa(T21, T25, X22, T24, X23, T14))
pL_in_ggagaa(T21, T25, T38, T24, X23, T14) → U11_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_in_ga(.(T21, T25), T38))
U11_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_out_ga(.(T21, T25), T38)) → U12_ggagaa(T21, T25, T38, T24, X23, T14, pM_in_gaga(T24, X23, T38, T14))
pM_in_gaga(T24, T39, T38, T14) → U13_gaga(T24, T39, T38, T14, mergesortE_in_ga(T24, T39))
mergesortE_in_ga([], []) → mergesortE_out_ga([], [])
mergesortE_in_ga(.(T44, []), .(T44, [])) → mergesortE_out_ga(.(T44, []), .(T44, []))
mergesortE_in_ga(.(T51, .(T52, T53)), X105) → U4_ga(T51, T52, T53, X105, pF_in_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105))
pF_in_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105) → U15_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_in_ggaa(T51, .(T52, T53), T54, T55))
U15_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U16_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pN_in_gagaa(T54, X103, T55, X104, X105))
pN_in_gagaa(T54, T56, T55, X104, X105) → U17_gagaa(T54, T56, T55, X104, X105, mergesortE_in_ga(T54, T56))
U17_gagaa(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → U18_gagaa(T54, T56, T55, X104, X105, pO_in_gaga(T55, X104, T56, X105))
pO_in_gaga(T55, T57, T56, X105) → U19_gaga(T55, T57, T56, X105, mergesortE_in_ga(T55, T57))
U19_gaga(T55, T57, T56, X105, mergesortE_out_ga(T55, T57)) → U20_gaga(T55, T57, T56, X105, mergeG_in_gga(T56, T57, X105))
mergeG_in_gga(T66, [], T66) → mergeG_out_gga(T66, [], T66)
mergeG_in_gga([], T71, T71) → mergeG_out_gga([], T71, T71)
mergeG_in_gga(.(T92, T93), .(T94, T95), .(T92, T97)) → U5_gga(T92, T93, T94, T95, T97, pH_in_gggga(T92, T94, T93, T95, T97))
pH_in_gggga(T92, T94, T93, T95, T97) → U21_gggga(T92, T94, T93, T95, T97, leJ_in_gg(T92, T94))
leJ_in_gg(s(T110), s(T111)) → U7_gg(T110, T111, leJ_in_gg(T110, T111))
leJ_in_gg(0, s(T118)) → leJ_out_gg(0, s(T118))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U7_gg(T110, T111, leJ_out_gg(T110, T111)) → leJ_out_gg(s(T110), s(T111))
U21_gggga(T92, T94, T93, T95, T97, leJ_out_gg(T92, T94)) → U22_gggga(T92, T94, T93, T95, T97, mergeG_in_gga(T93, .(T94, T95), T97))
mergeG_in_gga(.(T131, T132), .(T133, T134), .(T133, T136)) → U6_gga(T131, T132, T133, T134, T136, pI_in_gggga(T131, T133, T132, T134, T136))
pI_in_gggga(T131, T133, T132, T134, T136) → U23_gggga(T131, T133, T132, T134, T136, gtK_in_gg(T131, T133))
gtK_in_gg(s(T149), s(T150)) → U8_gg(T149, T150, gtK_in_gg(T149, T150))
gtK_in_gg(s(T155), 0) → gtK_out_gg(s(T155), 0)
U8_gg(T149, T150, gtK_out_gg(T149, T150)) → gtK_out_gg(s(T149), s(T150))
U23_gggga(T131, T133, T132, T134, T136, gtK_out_gg(T131, T133)) → U24_gggga(T131, T133, T132, T134, T136, mergeG_in_gga(.(T131, T132), T134, T136))
U24_gggga(T131, T133, T132, T134, T136, mergeG_out_gga(.(T131, T132), T134, T136)) → pI_out_gggga(T131, T133, T132, T134, T136)
U6_gga(T131, T132, T133, T134, T136, pI_out_gggga(T131, T133, T132, T134, T136)) → mergeG_out_gga(.(T131, T132), .(T133, T134), .(T133, T136))
U22_gggga(T92, T94, T93, T95, T97, mergeG_out_gga(T93, .(T94, T95), T97)) → pH_out_gggga(T92, T94, T93, T95, T97)
U5_gga(T92, T93, T94, T95, T97, pH_out_gggga(T92, T94, T93, T95, T97)) → mergeG_out_gga(.(T92, T93), .(T94, T95), .(T92, T97))
U20_gaga(T55, T57, T56, X105, mergeG_out_gga(T56, T57, X105)) → pO_out_gaga(T55, T57, T56, X105)
U18_gagaa(T54, T56, T55, X104, X105, pO_out_gaga(T55, X104, T56, X105)) → pN_out_gagaa(T54, T56, T55, X104, X105)
U16_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pN_out_gagaa(T54, X103, T55, X104, X105)) → pF_out_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105)
U4_ga(T51, T52, T53, X105, pF_out_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105)) → mergesortE_out_ga(.(T51, .(T52, T53)), X105)
U13_gaga(T24, T39, T38, T14, mergesortE_out_ga(T24, T39)) → U14_gaga(T24, T39, T38, T14, mergeG_in_gga(T38, T39, T14))
U14_gaga(T24, T39, T38, T14, mergeG_out_gga(T38, T39, T14)) → pM_out_gaga(T24, T39, T38, T14)
U12_ggagaa(T21, T25, T38, T24, X23, T14, pM_out_gaga(T24, X23, T38, T14)) → pL_out_ggagaa(T21, T25, T38, T24, X23, T14)
U10_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pL_out_ggagaa(T21, T25, X22, T24, X23, T14)) → pB_out_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14)
U1_ga(T21, T22, T23, T14, pB_out_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14)) → mergesortA_out_ga(.(T21, .(T22, T23)), T14)

The argument filtering Pi contains the following mapping:
mergesortA_in_ga(x1, x2)  =  mergesortA_in_ga(x1)
[]  =  []
mergesortA_out_ga(x1, x2)  =  mergesortA_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
pB_in_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pB_in_ggaagaaa(x1, x2, x5)
U9_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U9_ggaagaaa(x1, x2, x5, x9)
splitD_in_ggaa(x1, x2, x3, x4)  =  splitD_in_ggaa(x1, x2)
U3_ggaa(x1, x2, x3, x4, x5)  =  U3_ggaa(x1, x2, x5)
splitC_in_gaa(x1, x2, x3)  =  splitC_in_gaa(x1)
splitC_out_gaa(x1, x2, x3)  =  splitC_out_gaa(x1, x2, x3)
U2_gaa(x1, x2, x3, x4, x5)  =  U2_gaa(x1, x2, x5)
splitD_out_ggaa(x1, x2, x3, x4)  =  splitD_out_ggaa(x1, x2, x3, x4)
U10_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U10_ggaagaaa(x1, x2, x3, x4, x5, x9)
pL_in_ggagaa(x1, x2, x3, x4, x5, x6)  =  pL_in_ggagaa(x1, x2, x4)
U11_ggagaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_ggagaa(x1, x2, x4, x7)
U12_ggagaa(x1, x2, x3, x4, x5, x6, x7)  =  U12_ggagaa(x1, x2, x3, x4, x7)
pM_in_gaga(x1, x2, x3, x4)  =  pM_in_gaga(x1, x3)
U13_gaga(x1, x2, x3, x4, x5)  =  U13_gaga(x1, x3, x5)
mergesortE_in_ga(x1, x2)  =  mergesortE_in_ga(x1)
mergesortE_out_ga(x1, x2)  =  mergesortE_out_ga(x1, x2)
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x2, x3, x5)
pF_in_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pF_in_gggaaaaa(x1, x2, x3)
U15_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U15_gggaaaaa(x1, x2, x3, x9)
U16_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U16_gggaaaaa(x1, x2, x3, x4, x5, x9)
pN_in_gagaa(x1, x2, x3, x4, x5)  =  pN_in_gagaa(x1, x3)
U17_gagaa(x1, x2, x3, x4, x5, x6)  =  U17_gagaa(x1, x3, x6)
U18_gagaa(x1, x2, x3, x4, x5, x6)  =  U18_gagaa(x1, x2, x3, x6)
pO_in_gaga(x1, x2, x3, x4)  =  pO_in_gaga(x1, x3)
U19_gaga(x1, x2, x3, x4, x5)  =  U19_gaga(x1, x3, x5)
U20_gaga(x1, x2, x3, x4, x5)  =  U20_gaga(x1, x2, x3, x5)
mergeG_in_gga(x1, x2, x3)  =  mergeG_in_gga(x1, x2)
mergeG_out_gga(x1, x2, x3)  =  mergeG_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4, x5, x6)  =  U5_gga(x1, x2, x3, x4, x6)
pH_in_gggga(x1, x2, x3, x4, x5)  =  pH_in_gggga(x1, x2, x3, x4)
U21_gggga(x1, x2, x3, x4, x5, x6)  =  U21_gggga(x1, x2, x3, x4, x6)
leJ_in_gg(x1, x2)  =  leJ_in_gg(x1, x2)
s(x1)  =  s(x1)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
0  =  0
leJ_out_gg(x1, x2)  =  leJ_out_gg(x1, x2)
U22_gggga(x1, x2, x3, x4, x5, x6)  =  U22_gggga(x1, x2, x3, x4, x6)
U6_gga(x1, x2, x3, x4, x5, x6)  =  U6_gga(x1, x2, x3, x4, x6)
pI_in_gggga(x1, x2, x3, x4, x5)  =  pI_in_gggga(x1, x2, x3, x4)
U23_gggga(x1, x2, x3, x4, x5, x6)  =  U23_gggga(x1, x2, x3, x4, x6)
gtK_in_gg(x1, x2)  =  gtK_in_gg(x1, x2)
U8_gg(x1, x2, x3)  =  U8_gg(x1, x2, x3)
gtK_out_gg(x1, x2)  =  gtK_out_gg(x1, x2)
U24_gggga(x1, x2, x3, x4, x5, x6)  =  U24_gggga(x1, x2, x3, x4, x6)
pI_out_gggga(x1, x2, x3, x4, x5)  =  pI_out_gggga(x1, x2, x3, x4, x5)
pH_out_gggga(x1, x2, x3, x4, x5)  =  pH_out_gggga(x1, x2, x3, x4, x5)
pO_out_gaga(x1, x2, x3, x4)  =  pO_out_gaga(x1, x2, x3, x4)
pN_out_gagaa(x1, x2, x3, x4, x5)  =  pN_out_gagaa(x1, x2, x3, x4, x5)
pF_out_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pF_out_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)
U14_gaga(x1, x2, x3, x4, x5)  =  U14_gaga(x1, x2, x3, x5)
pM_out_gaga(x1, x2, x3, x4)  =  pM_out_gaga(x1, x2, x3, x4)
pL_out_ggagaa(x1, x2, x3, x4, x5, x6)  =  pL_out_ggagaa(x1, x2, x3, x4, x5, x6)
pB_out_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pB_out_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)
MERGESORTE_IN_GA(x1, x2)  =  MERGESORTE_IN_GA(x1)
PF_IN_GGGAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  PF_IN_GGGAAAAA(x1, x2, x3)
U15_GGGAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U15_GGGAAAAA(x1, x2, x3, x9)
PN_IN_GAGAA(x1, x2, x3, x4, x5)  =  PN_IN_GAGAA(x1, x3)
U17_GAGAA(x1, x2, x3, x4, x5, x6)  =  U17_GAGAA(x1, x3, x6)
PO_IN_GAGA(x1, x2, x3, x4)  =  PO_IN_GAGA(x1, x3)

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

(38) UsableRulesProof (EQUIVALENT transformation)

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

(39) Obligation:

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

PF_IN_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105) → U15_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105, splitD_in_ggaa(T51, .(T52, T53), T54, T55))
U15_GGGAAAAA(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → PN_IN_GAGAA(T54, X103, T55, X104, X105)
PN_IN_GAGAA(T54, T56, T55, X104, X105) → U17_GAGAA(T54, T56, T55, X104, X105, mergesortE_in_ga(T54, T56))
U17_GAGAA(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → PO_IN_GAGA(T55, X104, T56, X105)
PO_IN_GAGA(T55, T57, T56, X105) → MERGESORTE_IN_GA(T55, T57)
MERGESORTE_IN_GA(.(T51, .(T52, T53)), X105) → PF_IN_GGGAAAAA(T51, T52, T53, X101, X102, X103, X104, X105)
PN_IN_GAGAA(T54, T56, T55, X104, X105) → MERGESORTE_IN_GA(T54, T56)

The TRS R consists of the following rules:

splitD_in_ggaa(T30, T31, .(T30, X58), X59) → U3_ggaa(T30, T31, X58, X59, splitC_in_gaa(T31, X59, X58))
mergesortE_in_ga([], []) → mergesortE_out_ga([], [])
mergesortE_in_ga(.(T44, []), .(T44, [])) → mergesortE_out_ga(.(T44, []), .(T44, []))
mergesortE_in_ga(.(T51, .(T52, T53)), X105) → U4_ga(T51, T52, T53, X105, pF_in_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105))
U3_ggaa(T30, T31, X58, X59, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U4_ga(T51, T52, T53, X105, pF_out_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105)) → mergesortE_out_ga(.(T51, .(T52, T53)), X105)
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37), .(T36, X76), X77) → U2_gaa(T36, T37, X76, X77, splitC_in_gaa(T37, X77, X76))
pF_in_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105) → U15_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_in_ggaa(T51, .(T52, T53), T54, T55))
U2_gaa(T36, T37, X76, X77, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U15_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U16_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pN_in_gagaa(T54, X103, T55, X104, X105))
U16_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pN_out_gagaa(T54, X103, T55, X104, X105)) → pF_out_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105)
pN_in_gagaa(T54, T56, T55, X104, X105) → U17_gagaa(T54, T56, T55, X104, X105, mergesortE_in_ga(T54, T56))
U17_gagaa(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → U18_gagaa(T54, T56, T55, X104, X105, pO_in_gaga(T55, X104, T56, X105))
U18_gagaa(T54, T56, T55, X104, X105, pO_out_gaga(T55, X104, T56, X105)) → pN_out_gagaa(T54, T56, T55, X104, X105)
pO_in_gaga(T55, T57, T56, X105) → U19_gaga(T55, T57, T56, X105, mergesortE_in_ga(T55, T57))
U19_gaga(T55, T57, T56, X105, mergesortE_out_ga(T55, T57)) → U20_gaga(T55, T57, T56, X105, mergeG_in_gga(T56, T57, X105))
U20_gaga(T55, T57, T56, X105, mergeG_out_gga(T56, T57, X105)) → pO_out_gaga(T55, T57, T56, X105)
mergeG_in_gga(T66, [], T66) → mergeG_out_gga(T66, [], T66)
mergeG_in_gga([], T71, T71) → mergeG_out_gga([], T71, T71)
mergeG_in_gga(.(T92, T93), .(T94, T95), .(T92, T97)) → U5_gga(T92, T93, T94, T95, T97, pH_in_gggga(T92, T94, T93, T95, T97))
mergeG_in_gga(.(T131, T132), .(T133, T134), .(T133, T136)) → U6_gga(T131, T132, T133, T134, T136, pI_in_gggga(T131, T133, T132, T134, T136))
U5_gga(T92, T93, T94, T95, T97, pH_out_gggga(T92, T94, T93, T95, T97)) → mergeG_out_gga(.(T92, T93), .(T94, T95), .(T92, T97))
U6_gga(T131, T132, T133, T134, T136, pI_out_gggga(T131, T133, T132, T134, T136)) → mergeG_out_gga(.(T131, T132), .(T133, T134), .(T133, T136))
pH_in_gggga(T92, T94, T93, T95, T97) → U21_gggga(T92, T94, T93, T95, T97, leJ_in_gg(T92, T94))
pI_in_gggga(T131, T133, T132, T134, T136) → U23_gggga(T131, T133, T132, T134, T136, gtK_in_gg(T131, T133))
U21_gggga(T92, T94, T93, T95, T97, leJ_out_gg(T92, T94)) → U22_gggga(T92, T94, T93, T95, T97, mergeG_in_gga(T93, .(T94, T95), T97))
U23_gggga(T131, T133, T132, T134, T136, gtK_out_gg(T131, T133)) → U24_gggga(T131, T133, T132, T134, T136, mergeG_in_gga(.(T131, T132), T134, T136))
leJ_in_gg(s(T110), s(T111)) → U7_gg(T110, T111, leJ_in_gg(T110, T111))
leJ_in_gg(0, s(T118)) → leJ_out_gg(0, s(T118))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U22_gggga(T92, T94, T93, T95, T97, mergeG_out_gga(T93, .(T94, T95), T97)) → pH_out_gggga(T92, T94, T93, T95, T97)
gtK_in_gg(s(T149), s(T150)) → U8_gg(T149, T150, gtK_in_gg(T149, T150))
gtK_in_gg(s(T155), 0) → gtK_out_gg(s(T155), 0)
U24_gggga(T131, T133, T132, T134, T136, mergeG_out_gga(.(T131, T132), T134, T136)) → pI_out_gggga(T131, T133, T132, T134, T136)
U7_gg(T110, T111, leJ_out_gg(T110, T111)) → leJ_out_gg(s(T110), s(T111))
U8_gg(T149, T150, gtK_out_gg(T149, T150)) → gtK_out_gg(s(T149), s(T150))

The argument filtering Pi contains the following mapping:
[]  =  []
.(x1, x2)  =  .(x1, x2)
splitD_in_ggaa(x1, x2, x3, x4)  =  splitD_in_ggaa(x1, x2)
U3_ggaa(x1, x2, x3, x4, x5)  =  U3_ggaa(x1, x2, x5)
splitC_in_gaa(x1, x2, x3)  =  splitC_in_gaa(x1)
splitC_out_gaa(x1, x2, x3)  =  splitC_out_gaa(x1, x2, x3)
U2_gaa(x1, x2, x3, x4, x5)  =  U2_gaa(x1, x2, x5)
splitD_out_ggaa(x1, x2, x3, x4)  =  splitD_out_ggaa(x1, x2, x3, x4)
mergesortE_in_ga(x1, x2)  =  mergesortE_in_ga(x1)
mergesortE_out_ga(x1, x2)  =  mergesortE_out_ga(x1, x2)
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x2, x3, x5)
pF_in_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pF_in_gggaaaaa(x1, x2, x3)
U15_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U15_gggaaaaa(x1, x2, x3, x9)
U16_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U16_gggaaaaa(x1, x2, x3, x4, x5, x9)
pN_in_gagaa(x1, x2, x3, x4, x5)  =  pN_in_gagaa(x1, x3)
U17_gagaa(x1, x2, x3, x4, x5, x6)  =  U17_gagaa(x1, x3, x6)
U18_gagaa(x1, x2, x3, x4, x5, x6)  =  U18_gagaa(x1, x2, x3, x6)
pO_in_gaga(x1, x2, x3, x4)  =  pO_in_gaga(x1, x3)
U19_gaga(x1, x2, x3, x4, x5)  =  U19_gaga(x1, x3, x5)
U20_gaga(x1, x2, x3, x4, x5)  =  U20_gaga(x1, x2, x3, x5)
mergeG_in_gga(x1, x2, x3)  =  mergeG_in_gga(x1, x2)
mergeG_out_gga(x1, x2, x3)  =  mergeG_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4, x5, x6)  =  U5_gga(x1, x2, x3, x4, x6)
pH_in_gggga(x1, x2, x3, x4, x5)  =  pH_in_gggga(x1, x2, x3, x4)
U21_gggga(x1, x2, x3, x4, x5, x6)  =  U21_gggga(x1, x2, x3, x4, x6)
leJ_in_gg(x1, x2)  =  leJ_in_gg(x1, x2)
s(x1)  =  s(x1)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
0  =  0
leJ_out_gg(x1, x2)  =  leJ_out_gg(x1, x2)
U22_gggga(x1, x2, x3, x4, x5, x6)  =  U22_gggga(x1, x2, x3, x4, x6)
U6_gga(x1, x2, x3, x4, x5, x6)  =  U6_gga(x1, x2, x3, x4, x6)
pI_in_gggga(x1, x2, x3, x4, x5)  =  pI_in_gggga(x1, x2, x3, x4)
U23_gggga(x1, x2, x3, x4, x5, x6)  =  U23_gggga(x1, x2, x3, x4, x6)
gtK_in_gg(x1, x2)  =  gtK_in_gg(x1, x2)
U8_gg(x1, x2, x3)  =  U8_gg(x1, x2, x3)
gtK_out_gg(x1, x2)  =  gtK_out_gg(x1, x2)
U24_gggga(x1, x2, x3, x4, x5, x6)  =  U24_gggga(x1, x2, x3, x4, x6)
pI_out_gggga(x1, x2, x3, x4, x5)  =  pI_out_gggga(x1, x2, x3, x4, x5)
pH_out_gggga(x1, x2, x3, x4, x5)  =  pH_out_gggga(x1, x2, x3, x4, x5)
pO_out_gaga(x1, x2, x3, x4)  =  pO_out_gaga(x1, x2, x3, x4)
pN_out_gagaa(x1, x2, x3, x4, x5)  =  pN_out_gagaa(x1, x2, x3, x4, x5)
pF_out_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pF_out_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)
MERGESORTE_IN_GA(x1, x2)  =  MERGESORTE_IN_GA(x1)
PF_IN_GGGAAAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  PF_IN_GGGAAAAA(x1, x2, x3)
U15_GGGAAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U15_GGGAAAAA(x1, x2, x3, x9)
PN_IN_GAGAA(x1, x2, x3, x4, x5)  =  PN_IN_GAGAA(x1, x3)
U17_GAGAA(x1, x2, x3, x4, x5, x6)  =  U17_GAGAA(x1, x3, x6)
PO_IN_GAGA(x1, x2, x3, x4)  =  PO_IN_GAGA(x1, x3)

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

(40) PiDPToQDPProof (SOUND transformation)

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

(41) Obligation:

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

PF_IN_GGGAAAAA(T51, T52, T53) → U15_GGGAAAAA(T51, T52, T53, splitD_in_ggaa(T51, .(T52, T53)))
U15_GGGAAAAA(T51, T52, T53, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → PN_IN_GAGAA(T54, T55)
PN_IN_GAGAA(T54, T55) → U17_GAGAA(T54, T55, mergesortE_in_ga(T54))
U17_GAGAA(T54, T55, mergesortE_out_ga(T54, T56)) → PO_IN_GAGA(T55, T56)
PO_IN_GAGA(T55, T56) → MERGESORTE_IN_GA(T55)
MERGESORTE_IN_GA(.(T51, .(T52, T53))) → PF_IN_GGGAAAAA(T51, T52, T53)
PN_IN_GAGAA(T54, T55) → MERGESORTE_IN_GA(T54)

The TRS R consists of the following rules:

splitD_in_ggaa(T30, T31) → U3_ggaa(T30, T31, splitC_in_gaa(T31))
mergesortE_in_ga([]) → mergesortE_out_ga([], [])
mergesortE_in_ga(.(T44, [])) → mergesortE_out_ga(.(T44, []), .(T44, []))
mergesortE_in_ga(.(T51, .(T52, T53))) → U4_ga(T51, T52, T53, pF_in_gggaaaaa(T51, T52, T53))
U3_ggaa(T30, T31, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U4_ga(T51, T52, T53, pF_out_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105)) → mergesortE_out_ga(.(T51, .(T52, T53)), X105)
splitC_in_gaa([]) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37)) → U2_gaa(T36, T37, splitC_in_gaa(T37))
pF_in_gggaaaaa(T51, T52, T53) → U15_gggaaaaa(T51, T52, T53, splitD_in_ggaa(T51, .(T52, T53)))
U2_gaa(T36, T37, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U15_gggaaaaa(T51, T52, T53, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U16_gggaaaaa(T51, T52, T53, T54, T55, pN_in_gagaa(T54, T55))
U16_gggaaaaa(T51, T52, T53, T54, T55, pN_out_gagaa(T54, X103, T55, X104, X105)) → pF_out_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105)
pN_in_gagaa(T54, T55) → U17_gagaa(T54, T55, mergesortE_in_ga(T54))
U17_gagaa(T54, T55, mergesortE_out_ga(T54, T56)) → U18_gagaa(T54, T56, T55, pO_in_gaga(T55, T56))
U18_gagaa(T54, T56, T55, pO_out_gaga(T55, X104, T56, X105)) → pN_out_gagaa(T54, T56, T55, X104, X105)
pO_in_gaga(T55, T56) → U19_gaga(T55, T56, mergesortE_in_ga(T55))
U19_gaga(T55, T56, mergesortE_out_ga(T55, T57)) → U20_gaga(T55, T57, T56, mergeG_in_gga(T56, T57))
U20_gaga(T55, T57, T56, mergeG_out_gga(T56, T57, X105)) → pO_out_gaga(T55, T57, T56, X105)
mergeG_in_gga(T66, []) → mergeG_out_gga(T66, [], T66)
mergeG_in_gga([], T71) → mergeG_out_gga([], T71, T71)
mergeG_in_gga(.(T92, T93), .(T94, T95)) → U5_gga(T92, T93, T94, T95, pH_in_gggga(T92, T94, T93, T95))
mergeG_in_gga(.(T131, T132), .(T133, T134)) → U6_gga(T131, T132, T133, T134, pI_in_gggga(T131, T133, T132, T134))
U5_gga(T92, T93, T94, T95, pH_out_gggga(T92, T94, T93, T95, T97)) → mergeG_out_gga(.(T92, T93), .(T94, T95), .(T92, T97))
U6_gga(T131, T132, T133, T134, pI_out_gggga(T131, T133, T132, T134, T136)) → mergeG_out_gga(.(T131, T132), .(T133, T134), .(T133, T136))
pH_in_gggga(T92, T94, T93, T95) → U21_gggga(T92, T94, T93, T95, leJ_in_gg(T92, T94))
pI_in_gggga(T131, T133, T132, T134) → U23_gggga(T131, T133, T132, T134, gtK_in_gg(T131, T133))
U21_gggga(T92, T94, T93, T95, leJ_out_gg(T92, T94)) → U22_gggga(T92, T94, T93, T95, mergeG_in_gga(T93, .(T94, T95)))
U23_gggga(T131, T133, T132, T134, gtK_out_gg(T131, T133)) → U24_gggga(T131, T133, T132, T134, mergeG_in_gga(.(T131, T132), T134))
leJ_in_gg(s(T110), s(T111)) → U7_gg(T110, T111, leJ_in_gg(T110, T111))
leJ_in_gg(0, s(T118)) → leJ_out_gg(0, s(T118))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U22_gggga(T92, T94, T93, T95, mergeG_out_gga(T93, .(T94, T95), T97)) → pH_out_gggga(T92, T94, T93, T95, T97)
gtK_in_gg(s(T149), s(T150)) → U8_gg(T149, T150, gtK_in_gg(T149, T150))
gtK_in_gg(s(T155), 0) → gtK_out_gg(s(T155), 0)
U24_gggga(T131, T133, T132, T134, mergeG_out_gga(.(T131, T132), T134, T136)) → pI_out_gggga(T131, T133, T132, T134, T136)
U7_gg(T110, T111, leJ_out_gg(T110, T111)) → leJ_out_gg(s(T110), s(T111))
U8_gg(T149, T150, gtK_out_gg(T149, T150)) → gtK_out_gg(s(T149), s(T150))

The set Q consists of the following terms:

splitD_in_ggaa(x0, x1)
mergesortE_in_ga(x0)
U3_ggaa(x0, x1, x2)
U4_ga(x0, x1, x2, x3)
splitC_in_gaa(x0)
pF_in_gggaaaaa(x0, x1, x2)
U2_gaa(x0, x1, x2)
U15_gggaaaaa(x0, x1, x2, x3)
U16_gggaaaaa(x0, x1, x2, x3, x4, x5)
pN_in_gagaa(x0, x1)
U17_gagaa(x0, x1, x2)
U18_gagaa(x0, x1, x2, x3)
pO_in_gaga(x0, x1)
U19_gaga(x0, x1, x2)
U20_gaga(x0, x1, x2, x3)
mergeG_in_gga(x0, x1)
U5_gga(x0, x1, x2, x3, x4)
U6_gga(x0, x1, x2, x3, x4)
pH_in_gggga(x0, x1, x2, x3)
pI_in_gggga(x0, x1, x2, x3)
U21_gggga(x0, x1, x2, x3, x4)
U23_gggga(x0, x1, x2, x3, x4)
leJ_in_gg(x0, x1)
U22_gggga(x0, x1, x2, x3, x4)
gtK_in_gg(x0, x1)
U24_gggga(x0, x1, x2, x3, x4)
U7_gg(x0, x1, x2)
U8_gg(x0, x1, x2)

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

(42) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule PF_IN_GGGAAAAA(T51, T52, T53) → U15_GGGAAAAA(T51, T52, T53, splitD_in_ggaa(T51, .(T52, T53))) at position [3] we obtained the following new rules [LPAR04]:

PF_IN_GGGAAAAA(T51, T52, T53) → U15_GGGAAAAA(T51, T52, T53, U3_ggaa(T51, .(T52, T53), splitC_in_gaa(.(T52, T53))))

(43) Obligation:

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

U15_GGGAAAAA(T51, T52, T53, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → PN_IN_GAGAA(T54, T55)
PN_IN_GAGAA(T54, T55) → U17_GAGAA(T54, T55, mergesortE_in_ga(T54))
U17_GAGAA(T54, T55, mergesortE_out_ga(T54, T56)) → PO_IN_GAGA(T55, T56)
PO_IN_GAGA(T55, T56) → MERGESORTE_IN_GA(T55)
MERGESORTE_IN_GA(.(T51, .(T52, T53))) → PF_IN_GGGAAAAA(T51, T52, T53)
PN_IN_GAGAA(T54, T55) → MERGESORTE_IN_GA(T54)
PF_IN_GGGAAAAA(T51, T52, T53) → U15_GGGAAAAA(T51, T52, T53, U3_ggaa(T51, .(T52, T53), splitC_in_gaa(.(T52, T53))))

The TRS R consists of the following rules:

splitD_in_ggaa(T30, T31) → U3_ggaa(T30, T31, splitC_in_gaa(T31))
mergesortE_in_ga([]) → mergesortE_out_ga([], [])
mergesortE_in_ga(.(T44, [])) → mergesortE_out_ga(.(T44, []), .(T44, []))
mergesortE_in_ga(.(T51, .(T52, T53))) → U4_ga(T51, T52, T53, pF_in_gggaaaaa(T51, T52, T53))
U3_ggaa(T30, T31, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U4_ga(T51, T52, T53, pF_out_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105)) → mergesortE_out_ga(.(T51, .(T52, T53)), X105)
splitC_in_gaa([]) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37)) → U2_gaa(T36, T37, splitC_in_gaa(T37))
pF_in_gggaaaaa(T51, T52, T53) → U15_gggaaaaa(T51, T52, T53, splitD_in_ggaa(T51, .(T52, T53)))
U2_gaa(T36, T37, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U15_gggaaaaa(T51, T52, T53, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U16_gggaaaaa(T51, T52, T53, T54, T55, pN_in_gagaa(T54, T55))
U16_gggaaaaa(T51, T52, T53, T54, T55, pN_out_gagaa(T54, X103, T55, X104, X105)) → pF_out_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105)
pN_in_gagaa(T54, T55) → U17_gagaa(T54, T55, mergesortE_in_ga(T54))
U17_gagaa(T54, T55, mergesortE_out_ga(T54, T56)) → U18_gagaa(T54, T56, T55, pO_in_gaga(T55, T56))
U18_gagaa(T54, T56, T55, pO_out_gaga(T55, X104, T56, X105)) → pN_out_gagaa(T54, T56, T55, X104, X105)
pO_in_gaga(T55, T56) → U19_gaga(T55, T56, mergesortE_in_ga(T55))
U19_gaga(T55, T56, mergesortE_out_ga(T55, T57)) → U20_gaga(T55, T57, T56, mergeG_in_gga(T56, T57))
U20_gaga(T55, T57, T56, mergeG_out_gga(T56, T57, X105)) → pO_out_gaga(T55, T57, T56, X105)
mergeG_in_gga(T66, []) → mergeG_out_gga(T66, [], T66)
mergeG_in_gga([], T71) → mergeG_out_gga([], T71, T71)
mergeG_in_gga(.(T92, T93), .(T94, T95)) → U5_gga(T92, T93, T94, T95, pH_in_gggga(T92, T94, T93, T95))
mergeG_in_gga(.(T131, T132), .(T133, T134)) → U6_gga(T131, T132, T133, T134, pI_in_gggga(T131, T133, T132, T134))
U5_gga(T92, T93, T94, T95, pH_out_gggga(T92, T94, T93, T95, T97)) → mergeG_out_gga(.(T92, T93), .(T94, T95), .(T92, T97))
U6_gga(T131, T132, T133, T134, pI_out_gggga(T131, T133, T132, T134, T136)) → mergeG_out_gga(.(T131, T132), .(T133, T134), .(T133, T136))
pH_in_gggga(T92, T94, T93, T95) → U21_gggga(T92, T94, T93, T95, leJ_in_gg(T92, T94))
pI_in_gggga(T131, T133, T132, T134) → U23_gggga(T131, T133, T132, T134, gtK_in_gg(T131, T133))
U21_gggga(T92, T94, T93, T95, leJ_out_gg(T92, T94)) → U22_gggga(T92, T94, T93, T95, mergeG_in_gga(T93, .(T94, T95)))
U23_gggga(T131, T133, T132, T134, gtK_out_gg(T131, T133)) → U24_gggga(T131, T133, T132, T134, mergeG_in_gga(.(T131, T132), T134))
leJ_in_gg(s(T110), s(T111)) → U7_gg(T110, T111, leJ_in_gg(T110, T111))
leJ_in_gg(0, s(T118)) → leJ_out_gg(0, s(T118))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U22_gggga(T92, T94, T93, T95, mergeG_out_gga(T93, .(T94, T95), T97)) → pH_out_gggga(T92, T94, T93, T95, T97)
gtK_in_gg(s(T149), s(T150)) → U8_gg(T149, T150, gtK_in_gg(T149, T150))
gtK_in_gg(s(T155), 0) → gtK_out_gg(s(T155), 0)
U24_gggga(T131, T133, T132, T134, mergeG_out_gga(.(T131, T132), T134, T136)) → pI_out_gggga(T131, T133, T132, T134, T136)
U7_gg(T110, T111, leJ_out_gg(T110, T111)) → leJ_out_gg(s(T110), s(T111))
U8_gg(T149, T150, gtK_out_gg(T149, T150)) → gtK_out_gg(s(T149), s(T150))

The set Q consists of the following terms:

splitD_in_ggaa(x0, x1)
mergesortE_in_ga(x0)
U3_ggaa(x0, x1, x2)
U4_ga(x0, x1, x2, x3)
splitC_in_gaa(x0)
pF_in_gggaaaaa(x0, x1, x2)
U2_gaa(x0, x1, x2)
U15_gggaaaaa(x0, x1, x2, x3)
U16_gggaaaaa(x0, x1, x2, x3, x4, x5)
pN_in_gagaa(x0, x1)
U17_gagaa(x0, x1, x2)
U18_gagaa(x0, x1, x2, x3)
pO_in_gaga(x0, x1)
U19_gaga(x0, x1, x2)
U20_gaga(x0, x1, x2, x3)
mergeG_in_gga(x0, x1)
U5_gga(x0, x1, x2, x3, x4)
U6_gga(x0, x1, x2, x3, x4)
pH_in_gggga(x0, x1, x2, x3)
pI_in_gggga(x0, x1, x2, x3)
U21_gggga(x0, x1, x2, x3, x4)
U23_gggga(x0, x1, x2, x3, x4)
leJ_in_gg(x0, x1)
U22_gggga(x0, x1, x2, x3, x4)
gtK_in_gg(x0, x1)
U24_gggga(x0, x1, x2, x3, x4)
U7_gg(x0, x1, x2)
U8_gg(x0, x1, x2)

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

(44) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule PF_IN_GGGAAAAA(T51, T52, T53) → U15_GGGAAAAA(T51, T52, T53, U3_ggaa(T51, .(T52, T53), splitC_in_gaa(.(T52, T53)))) at position [3,2] we obtained the following new rules [LPAR04]:

PF_IN_GGGAAAAA(T51, T52, T53) → U15_GGGAAAAA(T51, T52, T53, U3_ggaa(T51, .(T52, T53), U2_gaa(T52, T53, splitC_in_gaa(T53))))

(45) Obligation:

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

U15_GGGAAAAA(T51, T52, T53, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → PN_IN_GAGAA(T54, T55)
PN_IN_GAGAA(T54, T55) → U17_GAGAA(T54, T55, mergesortE_in_ga(T54))
U17_GAGAA(T54, T55, mergesortE_out_ga(T54, T56)) → PO_IN_GAGA(T55, T56)
PO_IN_GAGA(T55, T56) → MERGESORTE_IN_GA(T55)
MERGESORTE_IN_GA(.(T51, .(T52, T53))) → PF_IN_GGGAAAAA(T51, T52, T53)
PN_IN_GAGAA(T54, T55) → MERGESORTE_IN_GA(T54)
PF_IN_GGGAAAAA(T51, T52, T53) → U15_GGGAAAAA(T51, T52, T53, U3_ggaa(T51, .(T52, T53), U2_gaa(T52, T53, splitC_in_gaa(T53))))

The TRS R consists of the following rules:

splitD_in_ggaa(T30, T31) → U3_ggaa(T30, T31, splitC_in_gaa(T31))
mergesortE_in_ga([]) → mergesortE_out_ga([], [])
mergesortE_in_ga(.(T44, [])) → mergesortE_out_ga(.(T44, []), .(T44, []))
mergesortE_in_ga(.(T51, .(T52, T53))) → U4_ga(T51, T52, T53, pF_in_gggaaaaa(T51, T52, T53))
U3_ggaa(T30, T31, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U4_ga(T51, T52, T53, pF_out_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105)) → mergesortE_out_ga(.(T51, .(T52, T53)), X105)
splitC_in_gaa([]) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37)) → U2_gaa(T36, T37, splitC_in_gaa(T37))
pF_in_gggaaaaa(T51, T52, T53) → U15_gggaaaaa(T51, T52, T53, splitD_in_ggaa(T51, .(T52, T53)))
U2_gaa(T36, T37, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U15_gggaaaaa(T51, T52, T53, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U16_gggaaaaa(T51, T52, T53, T54, T55, pN_in_gagaa(T54, T55))
U16_gggaaaaa(T51, T52, T53, T54, T55, pN_out_gagaa(T54, X103, T55, X104, X105)) → pF_out_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105)
pN_in_gagaa(T54, T55) → U17_gagaa(T54, T55, mergesortE_in_ga(T54))
U17_gagaa(T54, T55, mergesortE_out_ga(T54, T56)) → U18_gagaa(T54, T56, T55, pO_in_gaga(T55, T56))
U18_gagaa(T54, T56, T55, pO_out_gaga(T55, X104, T56, X105)) → pN_out_gagaa(T54, T56, T55, X104, X105)
pO_in_gaga(T55, T56) → U19_gaga(T55, T56, mergesortE_in_ga(T55))
U19_gaga(T55, T56, mergesortE_out_ga(T55, T57)) → U20_gaga(T55, T57, T56, mergeG_in_gga(T56, T57))
U20_gaga(T55, T57, T56, mergeG_out_gga(T56, T57, X105)) → pO_out_gaga(T55, T57, T56, X105)
mergeG_in_gga(T66, []) → mergeG_out_gga(T66, [], T66)
mergeG_in_gga([], T71) → mergeG_out_gga([], T71, T71)
mergeG_in_gga(.(T92, T93), .(T94, T95)) → U5_gga(T92, T93, T94, T95, pH_in_gggga(T92, T94, T93, T95))
mergeG_in_gga(.(T131, T132), .(T133, T134)) → U6_gga(T131, T132, T133, T134, pI_in_gggga(T131, T133, T132, T134))
U5_gga(T92, T93, T94, T95, pH_out_gggga(T92, T94, T93, T95, T97)) → mergeG_out_gga(.(T92, T93), .(T94, T95), .(T92, T97))
U6_gga(T131, T132, T133, T134, pI_out_gggga(T131, T133, T132, T134, T136)) → mergeG_out_gga(.(T131, T132), .(T133, T134), .(T133, T136))
pH_in_gggga(T92, T94, T93, T95) → U21_gggga(T92, T94, T93, T95, leJ_in_gg(T92, T94))
pI_in_gggga(T131, T133, T132, T134) → U23_gggga(T131, T133, T132, T134, gtK_in_gg(T131, T133))
U21_gggga(T92, T94, T93, T95, leJ_out_gg(T92, T94)) → U22_gggga(T92, T94, T93, T95, mergeG_in_gga(T93, .(T94, T95)))
U23_gggga(T131, T133, T132, T134, gtK_out_gg(T131, T133)) → U24_gggga(T131, T133, T132, T134, mergeG_in_gga(.(T131, T132), T134))
leJ_in_gg(s(T110), s(T111)) → U7_gg(T110, T111, leJ_in_gg(T110, T111))
leJ_in_gg(0, s(T118)) → leJ_out_gg(0, s(T118))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U22_gggga(T92, T94, T93, T95, mergeG_out_gga(T93, .(T94, T95), T97)) → pH_out_gggga(T92, T94, T93, T95, T97)
gtK_in_gg(s(T149), s(T150)) → U8_gg(T149, T150, gtK_in_gg(T149, T150))
gtK_in_gg(s(T155), 0) → gtK_out_gg(s(T155), 0)
U24_gggga(T131, T133, T132, T134, mergeG_out_gga(.(T131, T132), T134, T136)) → pI_out_gggga(T131, T133, T132, T134, T136)
U7_gg(T110, T111, leJ_out_gg(T110, T111)) → leJ_out_gg(s(T110), s(T111))
U8_gg(T149, T150, gtK_out_gg(T149, T150)) → gtK_out_gg(s(T149), s(T150))

The set Q consists of the following terms:

splitD_in_ggaa(x0, x1)
mergesortE_in_ga(x0)
U3_ggaa(x0, x1, x2)
U4_ga(x0, x1, x2, x3)
splitC_in_gaa(x0)
pF_in_gggaaaaa(x0, x1, x2)
U2_gaa(x0, x1, x2)
U15_gggaaaaa(x0, x1, x2, x3)
U16_gggaaaaa(x0, x1, x2, x3, x4, x5)
pN_in_gagaa(x0, x1)
U17_gagaa(x0, x1, x2)
U18_gagaa(x0, x1, x2, x3)
pO_in_gaga(x0, x1)
U19_gaga(x0, x1, x2)
U20_gaga(x0, x1, x2, x3)
mergeG_in_gga(x0, x1)
U5_gga(x0, x1, x2, x3, x4)
U6_gga(x0, x1, x2, x3, x4)
pH_in_gggga(x0, x1, x2, x3)
pI_in_gggga(x0, x1, x2, x3)
U21_gggga(x0, x1, x2, x3, x4)
U23_gggga(x0, x1, x2, x3, x4)
leJ_in_gg(x0, x1)
U22_gggga(x0, x1, x2, x3, x4)
gtK_in_gg(x0, x1)
U24_gggga(x0, x1, x2, x3, x4)
U7_gg(x0, x1, x2)
U8_gg(x0, x1, x2)

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

(46) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MERGESORTE_IN_GA(.(T51, .(T52, T53))) → PF_IN_GGGAAAAA(T51, T52, T53)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( U17_GAGAA(x1, ..., x3) ) = x2


POL( mergesortE_in_ga(x1) ) = 0


POL( [] ) = 0


POL( mergesortE_out_ga(x1, x2) ) = max{0, 2x2 - 2}


POL( .(x1, x2) ) = x1 + 2x2 + 1


POL( U4_ga(x1, ..., x4) ) = x4 + 2


POL( pF_in_gggaaaaa(x1, ..., x3) ) = 2x1 + 1


POL( U15_GGGAAAAA(x1, ..., x4) ) = max{0, x4 - 2}


POL( U2_gaa(x1, ..., x3) ) = max{0, x1 + 2x3 - 1}


POL( U3_ggaa(x1, ..., x3) ) = x1 + x3 + 1


POL( U15_gggaaaaa(x1, ..., x4) ) = max{0, 2x1 + 2x3 + x4 - 1}


POL( splitC_in_gaa(x1) ) = x1 + 2


POL( splitC_out_gaa(x1, ..., x3) ) = x2 + 2x3 + 2


POL( splitD_out_ggaa(x1, ..., x4) ) = x3 + x4 + 2


POL( U16_gggaaaaa(x1, ..., x6) ) = max{0, x1 + x2 + 2x4 - 1}


POL( pN_in_gagaa(x1, x2) ) = 0


POL( pN_out_gagaa(x1, ..., x5) ) = 2x1 + x2 + x4 + 2x5 + 1


POL( pF_out_gggaaaaa(x1, ..., x8) ) = x3 + x4 + x5 + 2x6 + x7 + 2x8 + 1


POL( U17_gagaa(x1, ..., x3) ) = max{0, x2 + x3 - 2}


POL( splitD_in_ggaa(x1, x2) ) = 2x1 + x2 + 1


POL( U18_gagaa(x1, ..., x4) ) = max{0, x1 + 2x4 - 2}


POL( pO_in_gaga(x1, x2) ) = x1 + x2


POL( pO_out_gaga(x1, ..., x4) ) = 2x1 + 2x2 + 2x3 + 2x4


POL( U19_gaga(x1, ..., x3) ) = max{0, x1 + 2x2 - 2}


POL( U20_gaga(x1, ..., x4) ) = 2x1 + x3 + 2


POL( mergeG_in_gga(x1, x2) ) = max{0, 2x1 + x2 - 1}


POL( mergeG_out_gga(x1, ..., x3) ) = max{0, x2 + x3 - 2}


POL( U5_gga(x1, ..., x5) ) = 2


POL( pH_in_gggga(x1, ..., x4) ) = 1


POL( U6_gga(x1, ..., x5) ) = max{0, x3 + x4 - 2}


POL( pI_in_gggga(x1, ..., x4) ) = x1 + 2x2 + x3 + x4


POL( pH_out_gggga(x1, ..., x5) ) = x1 + 2x2 + x3 + 2x4 + 2x5 + 2


POL( U21_gggga(x1, ..., x5) ) = x1 + x2 + 2x3 + 2x5 + 2


POL( leJ_in_gg(x1, x2) ) = x1 + x2


POL( s(x1) ) = 0


POL( U7_gg(x1, ..., x3) ) = max{0, x2 - 2}


POL( 0 ) = 0


POL( leJ_out_gg(x1, x2) ) = 2x2


POL( U22_gggga(x1, ..., x5) ) = 2x1 + x2 + 2x3 + 2x4 + 2


POL( pI_out_gggga(x1, ..., x5) ) = 2x1 + x2 + x3 + x4 + 2x5 + 2


POL( U23_gggga(x1, ..., x5) ) = max{0, 2x3 + 2x4 + x5 - 2}


POL( gtK_in_gg(x1, x2) ) = 2x2


POL( U8_gg(x1, ..., x3) ) = max{0, -2}


POL( gtK_out_gg(x1, x2) ) = max{0, 2x2 - 1}


POL( U24_gggga(x1, ..., x5) ) = max{0, x1 + 2x2 + 2x3 + x4 - 2}


POL( PN_IN_GAGAA(x1, x2) ) = x1 + x2


POL( PO_IN_GAGA(x1, x2) ) = x1


POL( MERGESORTE_IN_GA(x1) ) = x1


POL( PF_IN_GGGAAAAA(x1, ..., x3) ) = x1 + x2 + 2x3 + 2



The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

splitC_in_gaa([]) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37)) → U2_gaa(T36, T37, splitC_in_gaa(T37))
U2_gaa(T36, T37, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U3_ggaa(T30, T31, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)

(47) Obligation:

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

U15_GGGAAAAA(T51, T52, T53, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → PN_IN_GAGAA(T54, T55)
PN_IN_GAGAA(T54, T55) → U17_GAGAA(T54, T55, mergesortE_in_ga(T54))
U17_GAGAA(T54, T55, mergesortE_out_ga(T54, T56)) → PO_IN_GAGA(T55, T56)
PO_IN_GAGA(T55, T56) → MERGESORTE_IN_GA(T55)
PN_IN_GAGAA(T54, T55) → MERGESORTE_IN_GA(T54)
PF_IN_GGGAAAAA(T51, T52, T53) → U15_GGGAAAAA(T51, T52, T53, U3_ggaa(T51, .(T52, T53), U2_gaa(T52, T53, splitC_in_gaa(T53))))

The TRS R consists of the following rules:

splitD_in_ggaa(T30, T31) → U3_ggaa(T30, T31, splitC_in_gaa(T31))
mergesortE_in_ga([]) → mergesortE_out_ga([], [])
mergesortE_in_ga(.(T44, [])) → mergesortE_out_ga(.(T44, []), .(T44, []))
mergesortE_in_ga(.(T51, .(T52, T53))) → U4_ga(T51, T52, T53, pF_in_gggaaaaa(T51, T52, T53))
U3_ggaa(T30, T31, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U4_ga(T51, T52, T53, pF_out_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105)) → mergesortE_out_ga(.(T51, .(T52, T53)), X105)
splitC_in_gaa([]) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37)) → U2_gaa(T36, T37, splitC_in_gaa(T37))
pF_in_gggaaaaa(T51, T52, T53) → U15_gggaaaaa(T51, T52, T53, splitD_in_ggaa(T51, .(T52, T53)))
U2_gaa(T36, T37, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U15_gggaaaaa(T51, T52, T53, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U16_gggaaaaa(T51, T52, T53, T54, T55, pN_in_gagaa(T54, T55))
U16_gggaaaaa(T51, T52, T53, T54, T55, pN_out_gagaa(T54, X103, T55, X104, X105)) → pF_out_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105)
pN_in_gagaa(T54, T55) → U17_gagaa(T54, T55, mergesortE_in_ga(T54))
U17_gagaa(T54, T55, mergesortE_out_ga(T54, T56)) → U18_gagaa(T54, T56, T55, pO_in_gaga(T55, T56))
U18_gagaa(T54, T56, T55, pO_out_gaga(T55, X104, T56, X105)) → pN_out_gagaa(T54, T56, T55, X104, X105)
pO_in_gaga(T55, T56) → U19_gaga(T55, T56, mergesortE_in_ga(T55))
U19_gaga(T55, T56, mergesortE_out_ga(T55, T57)) → U20_gaga(T55, T57, T56, mergeG_in_gga(T56, T57))
U20_gaga(T55, T57, T56, mergeG_out_gga(T56, T57, X105)) → pO_out_gaga(T55, T57, T56, X105)
mergeG_in_gga(T66, []) → mergeG_out_gga(T66, [], T66)
mergeG_in_gga([], T71) → mergeG_out_gga([], T71, T71)
mergeG_in_gga(.(T92, T93), .(T94, T95)) → U5_gga(T92, T93, T94, T95, pH_in_gggga(T92, T94, T93, T95))
mergeG_in_gga(.(T131, T132), .(T133, T134)) → U6_gga(T131, T132, T133, T134, pI_in_gggga(T131, T133, T132, T134))
U5_gga(T92, T93, T94, T95, pH_out_gggga(T92, T94, T93, T95, T97)) → mergeG_out_gga(.(T92, T93), .(T94, T95), .(T92, T97))
U6_gga(T131, T132, T133, T134, pI_out_gggga(T131, T133, T132, T134, T136)) → mergeG_out_gga(.(T131, T132), .(T133, T134), .(T133, T136))
pH_in_gggga(T92, T94, T93, T95) → U21_gggga(T92, T94, T93, T95, leJ_in_gg(T92, T94))
pI_in_gggga(T131, T133, T132, T134) → U23_gggga(T131, T133, T132, T134, gtK_in_gg(T131, T133))
U21_gggga(T92, T94, T93, T95, leJ_out_gg(T92, T94)) → U22_gggga(T92, T94, T93, T95, mergeG_in_gga(T93, .(T94, T95)))
U23_gggga(T131, T133, T132, T134, gtK_out_gg(T131, T133)) → U24_gggga(T131, T133, T132, T134, mergeG_in_gga(.(T131, T132), T134))
leJ_in_gg(s(T110), s(T111)) → U7_gg(T110, T111, leJ_in_gg(T110, T111))
leJ_in_gg(0, s(T118)) → leJ_out_gg(0, s(T118))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U22_gggga(T92, T94, T93, T95, mergeG_out_gga(T93, .(T94, T95), T97)) → pH_out_gggga(T92, T94, T93, T95, T97)
gtK_in_gg(s(T149), s(T150)) → U8_gg(T149, T150, gtK_in_gg(T149, T150))
gtK_in_gg(s(T155), 0) → gtK_out_gg(s(T155), 0)
U24_gggga(T131, T133, T132, T134, mergeG_out_gga(.(T131, T132), T134, T136)) → pI_out_gggga(T131, T133, T132, T134, T136)
U7_gg(T110, T111, leJ_out_gg(T110, T111)) → leJ_out_gg(s(T110), s(T111))
U8_gg(T149, T150, gtK_out_gg(T149, T150)) → gtK_out_gg(s(T149), s(T150))

The set Q consists of the following terms:

splitD_in_ggaa(x0, x1)
mergesortE_in_ga(x0)
U3_ggaa(x0, x1, x2)
U4_ga(x0, x1, x2, x3)
splitC_in_gaa(x0)
pF_in_gggaaaaa(x0, x1, x2)
U2_gaa(x0, x1, x2)
U15_gggaaaaa(x0, x1, x2, x3)
U16_gggaaaaa(x0, x1, x2, x3, x4, x5)
pN_in_gagaa(x0, x1)
U17_gagaa(x0, x1, x2)
U18_gagaa(x0, x1, x2, x3)
pO_in_gaga(x0, x1)
U19_gaga(x0, x1, x2)
U20_gaga(x0, x1, x2, x3)
mergeG_in_gga(x0, x1)
U5_gga(x0, x1, x2, x3, x4)
U6_gga(x0, x1, x2, x3, x4)
pH_in_gggga(x0, x1, x2, x3)
pI_in_gggga(x0, x1, x2, x3)
U21_gggga(x0, x1, x2, x3, x4)
U23_gggga(x0, x1, x2, x3, x4)
leJ_in_gg(x0, x1)
U22_gggga(x0, x1, x2, x3, x4)
gtK_in_gg(x0, x1)
U24_gggga(x0, x1, x2, x3, x4)
U7_gg(x0, x1, x2)
U8_gg(x0, x1, x2)

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

(48) DependencyGraphProof (EQUIVALENT transformation)

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

(49) TRUE

(50) Obligation:

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

MERGESORTA_IN_GA(.(T21, .(T22, T23)), T14) → PB_IN_GGAAGAAA(T22, T23, X41, X40, T21, X22, X23, T14)
PB_IN_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14) → U9_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14, splitD_in_ggaa(T22, T23, T24, T25))
U9_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → PL_IN_GGAGAA(T21, T25, X22, T24, X23, T14)
PL_IN_GGAGAA(T21, T25, T38, T24, X23, T14) → MERGESORTA_IN_GA(.(T21, T25), T38)

The TRS R consists of the following rules:

mergesortA_in_ga([], []) → mergesortA_out_ga([], [])
mergesortA_in_ga(.(T4, []), .(T4, [])) → mergesortA_out_ga(.(T4, []), .(T4, []))
mergesortA_in_ga(.(T21, .(T22, T23)), T14) → U1_ga(T21, T22, T23, T14, pB_in_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14))
pB_in_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14) → U9_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_in_ggaa(T22, T23, T24, T25))
splitD_in_ggaa(T30, T31, .(T30, X58), X59) → U3_ggaa(T30, T31, X58, X59, splitC_in_gaa(T31, X59, X58))
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37), .(T36, X76), X77) → U2_gaa(T36, T37, X76, X77, splitC_in_gaa(T37, X77, X76))
U2_gaa(T36, T37, X76, X77, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)
U3_ggaa(T30, T31, X58, X59, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U9_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → U10_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pL_in_ggagaa(T21, T25, X22, T24, X23, T14))
pL_in_ggagaa(T21, T25, T38, T24, X23, T14) → U11_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_in_ga(.(T21, T25), T38))
U11_ggagaa(T21, T25, T38, T24, X23, T14, mergesortA_out_ga(.(T21, T25), T38)) → U12_ggagaa(T21, T25, T38, T24, X23, T14, pM_in_gaga(T24, X23, T38, T14))
pM_in_gaga(T24, T39, T38, T14) → U13_gaga(T24, T39, T38, T14, mergesortE_in_ga(T24, T39))
mergesortE_in_ga([], []) → mergesortE_out_ga([], [])
mergesortE_in_ga(.(T44, []), .(T44, [])) → mergesortE_out_ga(.(T44, []), .(T44, []))
mergesortE_in_ga(.(T51, .(T52, T53)), X105) → U4_ga(T51, T52, T53, X105, pF_in_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105))
pF_in_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105) → U15_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_in_ggaa(T51, .(T52, T53), T54, T55))
U15_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, splitD_out_ggaa(T51, .(T52, T53), T54, T55)) → U16_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pN_in_gagaa(T54, X103, T55, X104, X105))
pN_in_gagaa(T54, T56, T55, X104, X105) → U17_gagaa(T54, T56, T55, X104, X105, mergesortE_in_ga(T54, T56))
U17_gagaa(T54, T56, T55, X104, X105, mergesortE_out_ga(T54, T56)) → U18_gagaa(T54, T56, T55, X104, X105, pO_in_gaga(T55, X104, T56, X105))
pO_in_gaga(T55, T57, T56, X105) → U19_gaga(T55, T57, T56, X105, mergesortE_in_ga(T55, T57))
U19_gaga(T55, T57, T56, X105, mergesortE_out_ga(T55, T57)) → U20_gaga(T55, T57, T56, X105, mergeG_in_gga(T56, T57, X105))
mergeG_in_gga(T66, [], T66) → mergeG_out_gga(T66, [], T66)
mergeG_in_gga([], T71, T71) → mergeG_out_gga([], T71, T71)
mergeG_in_gga(.(T92, T93), .(T94, T95), .(T92, T97)) → U5_gga(T92, T93, T94, T95, T97, pH_in_gggga(T92, T94, T93, T95, T97))
pH_in_gggga(T92, T94, T93, T95, T97) → U21_gggga(T92, T94, T93, T95, T97, leJ_in_gg(T92, T94))
leJ_in_gg(s(T110), s(T111)) → U7_gg(T110, T111, leJ_in_gg(T110, T111))
leJ_in_gg(0, s(T118)) → leJ_out_gg(0, s(T118))
leJ_in_gg(0, 0) → leJ_out_gg(0, 0)
U7_gg(T110, T111, leJ_out_gg(T110, T111)) → leJ_out_gg(s(T110), s(T111))
U21_gggga(T92, T94, T93, T95, T97, leJ_out_gg(T92, T94)) → U22_gggga(T92, T94, T93, T95, T97, mergeG_in_gga(T93, .(T94, T95), T97))
mergeG_in_gga(.(T131, T132), .(T133, T134), .(T133, T136)) → U6_gga(T131, T132, T133, T134, T136, pI_in_gggga(T131, T133, T132, T134, T136))
pI_in_gggga(T131, T133, T132, T134, T136) → U23_gggga(T131, T133, T132, T134, T136, gtK_in_gg(T131, T133))
gtK_in_gg(s(T149), s(T150)) → U8_gg(T149, T150, gtK_in_gg(T149, T150))
gtK_in_gg(s(T155), 0) → gtK_out_gg(s(T155), 0)
U8_gg(T149, T150, gtK_out_gg(T149, T150)) → gtK_out_gg(s(T149), s(T150))
U23_gggga(T131, T133, T132, T134, T136, gtK_out_gg(T131, T133)) → U24_gggga(T131, T133, T132, T134, T136, mergeG_in_gga(.(T131, T132), T134, T136))
U24_gggga(T131, T133, T132, T134, T136, mergeG_out_gga(.(T131, T132), T134, T136)) → pI_out_gggga(T131, T133, T132, T134, T136)
U6_gga(T131, T132, T133, T134, T136, pI_out_gggga(T131, T133, T132, T134, T136)) → mergeG_out_gga(.(T131, T132), .(T133, T134), .(T133, T136))
U22_gggga(T92, T94, T93, T95, T97, mergeG_out_gga(T93, .(T94, T95), T97)) → pH_out_gggga(T92, T94, T93, T95, T97)
U5_gga(T92, T93, T94, T95, T97, pH_out_gggga(T92, T94, T93, T95, T97)) → mergeG_out_gga(.(T92, T93), .(T94, T95), .(T92, T97))
U20_gaga(T55, T57, T56, X105, mergeG_out_gga(T56, T57, X105)) → pO_out_gaga(T55, T57, T56, X105)
U18_gagaa(T54, T56, T55, X104, X105, pO_out_gaga(T55, X104, T56, X105)) → pN_out_gagaa(T54, T56, T55, X104, X105)
U16_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105, pN_out_gagaa(T54, X103, T55, X104, X105)) → pF_out_gggaaaaa(T51, T52, T53, T54, T55, X103, X104, X105)
U4_ga(T51, T52, T53, X105, pF_out_gggaaaaa(T51, T52, T53, X101, X102, X103, X104, X105)) → mergesortE_out_ga(.(T51, .(T52, T53)), X105)
U13_gaga(T24, T39, T38, T14, mergesortE_out_ga(T24, T39)) → U14_gaga(T24, T39, T38, T14, mergeG_in_gga(T38, T39, T14))
U14_gaga(T24, T39, T38, T14, mergeG_out_gga(T38, T39, T14)) → pM_out_gaga(T24, T39, T38, T14)
U12_ggagaa(T21, T25, T38, T24, X23, T14, pM_out_gaga(T24, X23, T38, T14)) → pL_out_ggagaa(T21, T25, T38, T24, X23, T14)
U10_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14, pL_out_ggagaa(T21, T25, X22, T24, X23, T14)) → pB_out_ggaagaaa(T22, T23, T24, T25, T21, X22, X23, T14)
U1_ga(T21, T22, T23, T14, pB_out_ggaagaaa(T22, T23, X41, X40, T21, X22, X23, T14)) → mergesortA_out_ga(.(T21, .(T22, T23)), T14)

The argument filtering Pi contains the following mapping:
mergesortA_in_ga(x1, x2)  =  mergesortA_in_ga(x1)
[]  =  []
mergesortA_out_ga(x1, x2)  =  mergesortA_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
pB_in_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pB_in_ggaagaaa(x1, x2, x5)
U9_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U9_ggaagaaa(x1, x2, x5, x9)
splitD_in_ggaa(x1, x2, x3, x4)  =  splitD_in_ggaa(x1, x2)
U3_ggaa(x1, x2, x3, x4, x5)  =  U3_ggaa(x1, x2, x5)
splitC_in_gaa(x1, x2, x3)  =  splitC_in_gaa(x1)
splitC_out_gaa(x1, x2, x3)  =  splitC_out_gaa(x1, x2, x3)
U2_gaa(x1, x2, x3, x4, x5)  =  U2_gaa(x1, x2, x5)
splitD_out_ggaa(x1, x2, x3, x4)  =  splitD_out_ggaa(x1, x2, x3, x4)
U10_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U10_ggaagaaa(x1, x2, x3, x4, x5, x9)
pL_in_ggagaa(x1, x2, x3, x4, x5, x6)  =  pL_in_ggagaa(x1, x2, x4)
U11_ggagaa(x1, x2, x3, x4, x5, x6, x7)  =  U11_ggagaa(x1, x2, x4, x7)
U12_ggagaa(x1, x2, x3, x4, x5, x6, x7)  =  U12_ggagaa(x1, x2, x3, x4, x7)
pM_in_gaga(x1, x2, x3, x4)  =  pM_in_gaga(x1, x3)
U13_gaga(x1, x2, x3, x4, x5)  =  U13_gaga(x1, x3, x5)
mergesortE_in_ga(x1, x2)  =  mergesortE_in_ga(x1)
mergesortE_out_ga(x1, x2)  =  mergesortE_out_ga(x1, x2)
U4_ga(x1, x2, x3, x4, x5)  =  U4_ga(x1, x2, x3, x5)
pF_in_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pF_in_gggaaaaa(x1, x2, x3)
U15_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U15_gggaaaaa(x1, x2, x3, x9)
U16_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U16_gggaaaaa(x1, x2, x3, x4, x5, x9)
pN_in_gagaa(x1, x2, x3, x4, x5)  =  pN_in_gagaa(x1, x3)
U17_gagaa(x1, x2, x3, x4, x5, x6)  =  U17_gagaa(x1, x3, x6)
U18_gagaa(x1, x2, x3, x4, x5, x6)  =  U18_gagaa(x1, x2, x3, x6)
pO_in_gaga(x1, x2, x3, x4)  =  pO_in_gaga(x1, x3)
U19_gaga(x1, x2, x3, x4, x5)  =  U19_gaga(x1, x3, x5)
U20_gaga(x1, x2, x3, x4, x5)  =  U20_gaga(x1, x2, x3, x5)
mergeG_in_gga(x1, x2, x3)  =  mergeG_in_gga(x1, x2)
mergeG_out_gga(x1, x2, x3)  =  mergeG_out_gga(x1, x2, x3)
U5_gga(x1, x2, x3, x4, x5, x6)  =  U5_gga(x1, x2, x3, x4, x6)
pH_in_gggga(x1, x2, x3, x4, x5)  =  pH_in_gggga(x1, x2, x3, x4)
U21_gggga(x1, x2, x3, x4, x5, x6)  =  U21_gggga(x1, x2, x3, x4, x6)
leJ_in_gg(x1, x2)  =  leJ_in_gg(x1, x2)
s(x1)  =  s(x1)
U7_gg(x1, x2, x3)  =  U7_gg(x1, x2, x3)
0  =  0
leJ_out_gg(x1, x2)  =  leJ_out_gg(x1, x2)
U22_gggga(x1, x2, x3, x4, x5, x6)  =  U22_gggga(x1, x2, x3, x4, x6)
U6_gga(x1, x2, x3, x4, x5, x6)  =  U6_gga(x1, x2, x3, x4, x6)
pI_in_gggga(x1, x2, x3, x4, x5)  =  pI_in_gggga(x1, x2, x3, x4)
U23_gggga(x1, x2, x3, x4, x5, x6)  =  U23_gggga(x1, x2, x3, x4, x6)
gtK_in_gg(x1, x2)  =  gtK_in_gg(x1, x2)
U8_gg(x1, x2, x3)  =  U8_gg(x1, x2, x3)
gtK_out_gg(x1, x2)  =  gtK_out_gg(x1, x2)
U24_gggga(x1, x2, x3, x4, x5, x6)  =  U24_gggga(x1, x2, x3, x4, x6)
pI_out_gggga(x1, x2, x3, x4, x5)  =  pI_out_gggga(x1, x2, x3, x4, x5)
pH_out_gggga(x1, x2, x3, x4, x5)  =  pH_out_gggga(x1, x2, x3, x4, x5)
pO_out_gaga(x1, x2, x3, x4)  =  pO_out_gaga(x1, x2, x3, x4)
pN_out_gagaa(x1, x2, x3, x4, x5)  =  pN_out_gagaa(x1, x2, x3, x4, x5)
pF_out_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pF_out_gggaaaaa(x1, x2, x3, x4, x5, x6, x7, x8)
U14_gaga(x1, x2, x3, x4, x5)  =  U14_gaga(x1, x2, x3, x5)
pM_out_gaga(x1, x2, x3, x4)  =  pM_out_gaga(x1, x2, x3, x4)
pL_out_ggagaa(x1, x2, x3, x4, x5, x6)  =  pL_out_ggagaa(x1, x2, x3, x4, x5, x6)
pB_out_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)  =  pB_out_ggaagaaa(x1, x2, x3, x4, x5, x6, x7, x8)
MERGESORTA_IN_GA(x1, x2)  =  MERGESORTA_IN_GA(x1)
PB_IN_GGAAGAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  PB_IN_GGAAGAAA(x1, x2, x5)
U9_GGAAGAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U9_GGAAGAAA(x1, x2, x5, x9)
PL_IN_GGAGAA(x1, x2, x3, x4, x5, x6)  =  PL_IN_GGAGAA(x1, x2, x4)

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

(51) UsableRulesProof (EQUIVALENT transformation)

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

(52) Obligation:

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

MERGESORTA_IN_GA(.(T21, .(T22, T23)), T14) → PB_IN_GGAAGAAA(T22, T23, X41, X40, T21, X22, X23, T14)
PB_IN_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14) → U9_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14, splitD_in_ggaa(T22, T23, T24, T25))
U9_GGAAGAAA(T22, T23, T24, T25, T21, X22, X23, T14, splitD_out_ggaa(T22, T23, T24, T25)) → PL_IN_GGAGAA(T21, T25, X22, T24, X23, T14)
PL_IN_GGAGAA(T21, T25, T38, T24, X23, T14) → MERGESORTA_IN_GA(.(T21, T25), T38)

The TRS R consists of the following rules:

splitD_in_ggaa(T30, T31, .(T30, X58), X59) → U3_ggaa(T30, T31, X58, X59, splitC_in_gaa(T31, X59, X58))
U3_ggaa(T30, T31, X58, X59, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
splitC_in_gaa([], [], []) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37), .(T36, X76), X77) → U2_gaa(T36, T37, X76, X77, splitC_in_gaa(T37, X77, X76))
U2_gaa(T36, T37, X76, X77, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)

The argument filtering Pi contains the following mapping:
[]  =  []
.(x1, x2)  =  .(x1, x2)
splitD_in_ggaa(x1, x2, x3, x4)  =  splitD_in_ggaa(x1, x2)
U3_ggaa(x1, x2, x3, x4, x5)  =  U3_ggaa(x1, x2, x5)
splitC_in_gaa(x1, x2, x3)  =  splitC_in_gaa(x1)
splitC_out_gaa(x1, x2, x3)  =  splitC_out_gaa(x1, x2, x3)
U2_gaa(x1, x2, x3, x4, x5)  =  U2_gaa(x1, x2, x5)
splitD_out_ggaa(x1, x2, x3, x4)  =  splitD_out_ggaa(x1, x2, x3, x4)
MERGESORTA_IN_GA(x1, x2)  =  MERGESORTA_IN_GA(x1)
PB_IN_GGAAGAAA(x1, x2, x3, x4, x5, x6, x7, x8)  =  PB_IN_GGAAGAAA(x1, x2, x5)
U9_GGAAGAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U9_GGAAGAAA(x1, x2, x5, x9)
PL_IN_GGAGAA(x1, x2, x3, x4, x5, x6)  =  PL_IN_GGAGAA(x1, x2, x4)

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

(53) PiDPToQDPProof (SOUND transformation)

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

(54) Obligation:

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

MERGESORTA_IN_GA(.(T21, .(T22, T23))) → PB_IN_GGAAGAAA(T22, T23, T21)
PB_IN_GGAAGAAA(T22, T23, T21) → U9_GGAAGAAA(T22, T23, T21, splitD_in_ggaa(T22, T23))
U9_GGAAGAAA(T22, T23, T21, splitD_out_ggaa(T22, T23, T24, T25)) → PL_IN_GGAGAA(T21, T25, T24)
PL_IN_GGAGAA(T21, T25, T24) → MERGESORTA_IN_GA(.(T21, T25))

The TRS R consists of the following rules:

splitD_in_ggaa(T30, T31) → U3_ggaa(T30, T31, splitC_in_gaa(T31))
U3_ggaa(T30, T31, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
splitC_in_gaa([]) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37)) → U2_gaa(T36, T37, splitC_in_gaa(T37))
U2_gaa(T36, T37, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)

The set Q consists of the following terms:

splitD_in_ggaa(x0, x1)
U3_ggaa(x0, x1, x2)
splitC_in_gaa(x0)
U2_gaa(x0, x1, x2)

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

(55) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule PB_IN_GGAAGAAA(T22, T23, T21) → U9_GGAAGAAA(T22, T23, T21, splitD_in_ggaa(T22, T23)) at position [3] we obtained the following new rules [LPAR04]:

PB_IN_GGAAGAAA(T22, T23, T21) → U9_GGAAGAAA(T22, T23, T21, U3_ggaa(T22, T23, splitC_in_gaa(T23)))

(56) Obligation:

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

MERGESORTA_IN_GA(.(T21, .(T22, T23))) → PB_IN_GGAAGAAA(T22, T23, T21)
U9_GGAAGAAA(T22, T23, T21, splitD_out_ggaa(T22, T23, T24, T25)) → PL_IN_GGAGAA(T21, T25, T24)
PL_IN_GGAGAA(T21, T25, T24) → MERGESORTA_IN_GA(.(T21, T25))
PB_IN_GGAAGAAA(T22, T23, T21) → U9_GGAAGAAA(T22, T23, T21, U3_ggaa(T22, T23, splitC_in_gaa(T23)))

The TRS R consists of the following rules:

splitD_in_ggaa(T30, T31) → U3_ggaa(T30, T31, splitC_in_gaa(T31))
U3_ggaa(T30, T31, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
splitC_in_gaa([]) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37)) → U2_gaa(T36, T37, splitC_in_gaa(T37))
U2_gaa(T36, T37, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)

The set Q consists of the following terms:

splitD_in_ggaa(x0, x1)
U3_ggaa(x0, x1, x2)
splitC_in_gaa(x0)
U2_gaa(x0, x1, x2)

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

(57) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(58) Obligation:

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

MERGESORTA_IN_GA(.(T21, .(T22, T23))) → PB_IN_GGAAGAAA(T22, T23, T21)
U9_GGAAGAAA(T22, T23, T21, splitD_out_ggaa(T22, T23, T24, T25)) → PL_IN_GGAGAA(T21, T25, T24)
PL_IN_GGAGAA(T21, T25, T24) → MERGESORTA_IN_GA(.(T21, T25))
PB_IN_GGAAGAAA(T22, T23, T21) → U9_GGAAGAAA(T22, T23, T21, U3_ggaa(T22, T23, splitC_in_gaa(T23)))

The TRS R consists of the following rules:

splitC_in_gaa([]) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37)) → U2_gaa(T36, T37, splitC_in_gaa(T37))
U3_ggaa(T30, T31, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U2_gaa(T36, T37, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)

The set Q consists of the following terms:

splitD_in_ggaa(x0, x1)
U3_ggaa(x0, x1, x2)
splitC_in_gaa(x0)
U2_gaa(x0, x1, x2)

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

(59) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

splitD_in_ggaa(x0, x1)

(60) Obligation:

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

MERGESORTA_IN_GA(.(T21, .(T22, T23))) → PB_IN_GGAAGAAA(T22, T23, T21)
U9_GGAAGAAA(T22, T23, T21, splitD_out_ggaa(T22, T23, T24, T25)) → PL_IN_GGAGAA(T21, T25, T24)
PL_IN_GGAGAA(T21, T25, T24) → MERGESORTA_IN_GA(.(T21, T25))
PB_IN_GGAAGAAA(T22, T23, T21) → U9_GGAAGAAA(T22, T23, T21, U3_ggaa(T22, T23, splitC_in_gaa(T23)))

The TRS R consists of the following rules:

splitC_in_gaa([]) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37)) → U2_gaa(T36, T37, splitC_in_gaa(T37))
U3_ggaa(T30, T31, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U2_gaa(T36, T37, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)

The set Q consists of the following terms:

U3_ggaa(x0, x1, x2)
splitC_in_gaa(x0)
U2_gaa(x0, x1, x2)

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

(61) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


MERGESORTA_IN_GA(.(T21, .(T22, T23))) → PB_IN_GGAAGAAA(T22, T23, T21)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 1 + x2   
POL(MERGESORTA_IN_GA(x1)) = x1   
POL(PB_IN_GGAAGAAA(x1, x2, x3)) = 1 + x2   
POL(PL_IN_GGAGAA(x1, x2, x3)) = 1 + x2   
POL(U2_gaa(x1, x2, x3)) = 1 + x3   
POL(U3_ggaa(x1, x2, x3)) = x3   
POL(U9_GGAAGAAA(x1, x2, x3, x4)) = x4   
POL([]) = 0   
POL(splitC_in_gaa(x1)) = 1 + x1   
POL(splitC_out_gaa(x1, x2, x3)) = 1 + x2 + x3   
POL(splitD_out_ggaa(x1, x2, x3, x4)) = 1 + x4   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

splitC_in_gaa([]) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37)) → U2_gaa(T36, T37, splitC_in_gaa(T37))
U3_ggaa(T30, T31, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U2_gaa(T36, T37, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)

(62) Obligation:

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

U9_GGAAGAAA(T22, T23, T21, splitD_out_ggaa(T22, T23, T24, T25)) → PL_IN_GGAGAA(T21, T25, T24)
PL_IN_GGAGAA(T21, T25, T24) → MERGESORTA_IN_GA(.(T21, T25))
PB_IN_GGAAGAAA(T22, T23, T21) → U9_GGAAGAAA(T22, T23, T21, U3_ggaa(T22, T23, splitC_in_gaa(T23)))

The TRS R consists of the following rules:

splitC_in_gaa([]) → splitC_out_gaa([], [], [])
splitC_in_gaa(.(T36, T37)) → U2_gaa(T36, T37, splitC_in_gaa(T37))
U3_ggaa(T30, T31, splitC_out_gaa(T31, X59, X58)) → splitD_out_ggaa(T30, T31, .(T30, X58), X59)
U2_gaa(T36, T37, splitC_out_gaa(T37, X77, X76)) → splitC_out_gaa(.(T36, T37), .(T36, X76), X77)

The set Q consists of the following terms:

U3_ggaa(x0, x1, x2)
splitC_in_gaa(x0)
U2_gaa(x0, x1, x2)

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

(63) DependencyGraphProof (EQUIVALENT transformation)

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

(64) TRUE