0 Prolog
↳1 PrologToPiTRSProof (⇐)
↳2 PiTRS
↳3 DependencyPairsProof (⇔)
↳4 PiDP
↳5 DependencyGraphProof (⇔)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔)
↳9 PiDP
↳10 PiDPToQDPProof (⇐)
↳11 QDP
↳12 QDPSizeChangeProof (⇔)
↳13 TRUE
↳14 PiDP
↳15 UsableRulesProof (⇔)
↳16 PiDP
↳17 PiDPToQDPProof (⇐)
↳18 QDP
↳19 NonTerminationProof (⇔)
↳20 FALSE
↳21 PiDP
↳22 UsableRulesProof (⇔)
↳23 PiDP
↳24 PiDPToQDPProof (⇐)
↳25 QDP
↳26 QDPSizeChangeProof (⇔)
↳27 TRUE
↳28 PiDP
↳29 UsableRulesProof (⇔)
↳30 PiDP
↳31 PiDPToQDPProof (⇐)
↳32 QDP
↳33 Narrowing (⇐)
↳34 QDP
↳35 Instantiation (⇔)
↳36 QDP
↳37 NonTerminationProof (⇔)
↳38 FALSE
↳39 PiDP
↳40 UsableRulesProof (⇔)
↳41 PiDP
↳42 PiDPToQDPProof (⇐)
↳43 QDP
↳44 NonTerminationProof (⇔)
↳45 FALSE
↳46 PiDP
↳47 UsableRulesProof (⇔)
↳48 PiDP
↳49 PiDPToQDPProof (⇐)
↳50 QDP
↳51 NonTerminationProof (⇔)
↳52 FALSE
↳53 PiDP
↳54 UsableRulesProof (⇔)
↳55 PiDP
↳56 PiDPToQDPProof (⇐)
↳57 QDP
↳58 Narrowing (⇐)
↳59 QDP
↳60 Narrowing (⇐)
↳61 QDP
↳62 NonTerminationProof (⇔)
↳63 FALSE
↳64 PrologToPiTRSProof (⇐)
↳65 PiTRS
↳66 DependencyPairsProof (⇔)
↳67 PiDP
↳68 DependencyGraphProof (⇔)
↳69 AND
↳70 PiDP
↳71 UsableRulesProof (⇔)
↳72 PiDP
↳73 PiDPToQDPProof (⇐)
↳74 QDP
↳75 QDPSizeChangeProof (⇔)
↳76 TRUE
↳77 PiDP
↳78 UsableRulesProof (⇔)
↳79 PiDP
↳80 PiDPToQDPProof (⇐)
↳81 QDP
↳82 NonTerminationProof (⇔)
↳83 FALSE
↳84 PiDP
↳85 UsableRulesProof (⇔)
↳86 PiDP
↳87 PiDPToQDPProof (⇐)
↳88 QDP
↳89 QDPSizeChangeProof (⇔)
↳90 TRUE
↳91 PiDP
↳92 UsableRulesProof (⇔)
↳93 PiDP
↳94 PiDPToQDPProof (⇐)
↳95 QDP
↳96 Narrowing (⇐)
↳97 QDP
↳98 Instantiation (⇔)
↳99 QDP
↳100 NonTerminationProof (⇔)
↳101 FALSE
↳102 PiDP
↳103 UsableRulesProof (⇔)
↳104 PiDP
↳105 PiDPToQDPProof (⇐)
↳106 QDP
↳107 NonTerminationProof (⇔)
↳108 FALSE
↳109 PiDP
↳110 UsableRulesProof (⇔)
↳111 PiDP
↳112 PiDPToQDPProof (⇐)
↳113 QDP
↳114 NonTerminationProof (⇔)
↳115 FALSE
↳116 PiDP
↳117 UsableRulesProof (⇔)
↳118 PiDP
↳119 PiDPToQDPProof (⇐)
↳120 QDP
↳121 Narrowing (⇐)
↳122 QDP
↳123 Narrowing (⇐)
↳124 QDP
↳125 NonTerminationProof (⇔)
↳126 FALSE
qs_in_ag([], []) → qs_out_ag([], [])
qs_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
part_in_aaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_aaaa(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
less_in_aa(0, s(X2)) → less_out_aa(0, s(X2))
less_in_aa(s(X), s(Y)) → U9_aa(X, Y, less_in_aa(X, Y))
U9_aa(X, Y, less_out_aa(X, Y)) → less_out_aa(s(X), s(Y))
U5_aaaa(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_aaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_gaaa(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
less_in_ga(0, s(X2)) → less_out_ga(0, s(X2))
less_in_ga(s(X), s(Y)) → U9_ga(X, Y, less_in_ga(X, Y))
U9_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U5_gaaa(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X1, [], [], []) → part_out_gaaa(X1, [], [], [])
U7_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U6_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), .(Y, Ls), Bs)
U6_aaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), .(Y, Ls), Bs)
part_in_aaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_aaaa(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
part_in_aaaa(X1, [], [], []) → part_out_aaaa(X1, [], [], [])
U7_aaaa(X, Y, Xs, Ls, Bs, part_out_aaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U1_ag(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_ag(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
qs_in_aa([], []) → qs_out_aa([], [])
qs_in_aa(.(X, Xs), Ys) → U1_aa(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U1_aa(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_aa(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U2_aa(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_aa(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_aa(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_aa(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
app_in_aaa([], X, X) → app_out_aaa([], X, X)
app_in_aaa(.(X, Xs), Ys, .(X, Zs)) → U8_aaa(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
U8_aaa(X, Xs, Ys, Zs, app_out_aaa(Xs, Ys, Zs)) → app_out_aaa(.(X, Xs), Ys, .(X, Zs))
U4_aa(X, Xs, Ys, app_out_aaa(Ls, .(X, Bs), Ys)) → qs_out_aa(.(X, Xs), Ys)
U2_ag(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_ag(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_ag(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_ag(X, Xs, Ys, app_in_aag(Ls, .(X, Bs), Ys))
app_in_aag([], X, X) → app_out_aag([], X, X)
app_in_aag(.(X, Xs), Ys, .(X, Zs)) → U8_aag(X, Xs, Ys, Zs, app_in_aag(Xs, Ys, Zs))
U8_aag(X, Xs, Ys, Zs, app_out_aag(Xs, Ys, Zs)) → app_out_aag(.(X, Xs), Ys, .(X, Zs))
U4_ag(X, Xs, Ys, app_out_aag(Ls, .(X, Bs), Ys)) → qs_out_ag(.(X, Xs), Ys)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
qs_in_ag([], []) → qs_out_ag([], [])
qs_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
part_in_aaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_aaaa(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
less_in_aa(0, s(X2)) → less_out_aa(0, s(X2))
less_in_aa(s(X), s(Y)) → U9_aa(X, Y, less_in_aa(X, Y))
U9_aa(X, Y, less_out_aa(X, Y)) → less_out_aa(s(X), s(Y))
U5_aaaa(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_aaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_gaaa(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
less_in_ga(0, s(X2)) → less_out_ga(0, s(X2))
less_in_ga(s(X), s(Y)) → U9_ga(X, Y, less_in_ga(X, Y))
U9_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U5_gaaa(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X1, [], [], []) → part_out_gaaa(X1, [], [], [])
U7_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U6_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), .(Y, Ls), Bs)
U6_aaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), .(Y, Ls), Bs)
part_in_aaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_aaaa(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
part_in_aaaa(X1, [], [], []) → part_out_aaaa(X1, [], [], [])
U7_aaaa(X, Y, Xs, Ls, Bs, part_out_aaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U1_ag(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_ag(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
qs_in_aa([], []) → qs_out_aa([], [])
qs_in_aa(.(X, Xs), Ys) → U1_aa(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U1_aa(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_aa(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U2_aa(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_aa(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_aa(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_aa(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
app_in_aaa([], X, X) → app_out_aaa([], X, X)
app_in_aaa(.(X, Xs), Ys, .(X, Zs)) → U8_aaa(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
U8_aaa(X, Xs, Ys, Zs, app_out_aaa(Xs, Ys, Zs)) → app_out_aaa(.(X, Xs), Ys, .(X, Zs))
U4_aa(X, Xs, Ys, app_out_aaa(Ls, .(X, Bs), Ys)) → qs_out_aa(.(X, Xs), Ys)
U2_ag(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_ag(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_ag(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_ag(X, Xs, Ys, app_in_aag(Ls, .(X, Bs), Ys))
app_in_aag([], X, X) → app_out_aag([], X, X)
app_in_aag(.(X, Xs), Ys, .(X, Zs)) → U8_aag(X, Xs, Ys, Zs, app_in_aag(Xs, Ys, Zs))
U8_aag(X, Xs, Ys, Zs, app_out_aag(Xs, Ys, Zs)) → app_out_aag(.(X, Xs), Ys, .(X, Zs))
U4_ag(X, Xs, Ys, app_out_aag(Ls, .(X, Bs), Ys)) → qs_out_ag(.(X, Xs), Ys)
QS_IN_AG(.(X, Xs), Ys) → U1_AG(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
QS_IN_AG(.(X, Xs), Ys) → PART_IN_AAAA(X, Xs, Littles, Bigs)
PART_IN_AAAA(X, .(Y, Xs), .(Y, Ls), Bs) → U5_AAAA(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
PART_IN_AAAA(X, .(Y, Xs), .(Y, Ls), Bs) → LESS_IN_AA(X, Y)
LESS_IN_AA(s(X), s(Y)) → U9_AA(X, Y, less_in_aa(X, Y))
LESS_IN_AA(s(X), s(Y)) → LESS_IN_AA(X, Y)
U5_AAAA(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_AAAA(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
U5_AAAA(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → PART_IN_GAAA(X, Xs, Ls, Bs)
PART_IN_GAAA(X, .(Y, Xs), .(Y, Ls), Bs) → U5_GAAA(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
PART_IN_GAAA(X, .(Y, Xs), .(Y, Ls), Bs) → LESS_IN_GA(X, Y)
LESS_IN_GA(s(X), s(Y)) → U9_GA(X, Y, less_in_ga(X, Y))
LESS_IN_GA(s(X), s(Y)) → LESS_IN_GA(X, Y)
U5_GAAA(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_GAAA(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
U5_GAAA(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → PART_IN_GAAA(X, Xs, Ls, Bs)
PART_IN_GAAA(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_GAAA(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
PART_IN_GAAA(X, .(Y, Xs), Ls, .(Y, Bs)) → PART_IN_GAAA(X, Xs, Ls, Bs)
PART_IN_AAAA(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_AAAA(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
PART_IN_AAAA(X, .(Y, Xs), Ls, .(Y, Bs)) → PART_IN_AAAA(X, Xs, Ls, Bs)
U1_AG(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_AG(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U1_AG(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → QS_IN_AA(Littles, Ls)
QS_IN_AA(.(X, Xs), Ys) → U1_AA(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
QS_IN_AA(.(X, Xs), Ys) → PART_IN_AAAA(X, Xs, Littles, Bigs)
U1_AA(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_AA(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U1_AA(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → QS_IN_AA(Littles, Ls)
U2_AA(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_AA(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U2_AA(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → QS_IN_AA(Bigs, Bs)
U3_AA(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_AA(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
U3_AA(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → APP_IN_AAA(Ls, .(X, Bs), Ys)
APP_IN_AAA(.(X, Xs), Ys, .(X, Zs)) → U8_AAA(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
APP_IN_AAA(.(X, Xs), Ys, .(X, Zs)) → APP_IN_AAA(Xs, Ys, Zs)
U2_AG(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_AG(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U2_AG(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → QS_IN_AA(Bigs, Bs)
U3_AG(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_AG(X, Xs, Ys, app_in_aag(Ls, .(X, Bs), Ys))
U3_AG(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → APP_IN_AAG(Ls, .(X, Bs), Ys)
APP_IN_AAG(.(X, Xs), Ys, .(X, Zs)) → U8_AAG(X, Xs, Ys, Zs, app_in_aag(Xs, Ys, Zs))
APP_IN_AAG(.(X, Xs), Ys, .(X, Zs)) → APP_IN_AAG(Xs, Ys, Zs)
qs_in_ag([], []) → qs_out_ag([], [])
qs_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
part_in_aaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_aaaa(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
less_in_aa(0, s(X2)) → less_out_aa(0, s(X2))
less_in_aa(s(X), s(Y)) → U9_aa(X, Y, less_in_aa(X, Y))
U9_aa(X, Y, less_out_aa(X, Y)) → less_out_aa(s(X), s(Y))
U5_aaaa(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_aaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_gaaa(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
less_in_ga(0, s(X2)) → less_out_ga(0, s(X2))
less_in_ga(s(X), s(Y)) → U9_ga(X, Y, less_in_ga(X, Y))
U9_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U5_gaaa(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X1, [], [], []) → part_out_gaaa(X1, [], [], [])
U7_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U6_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), .(Y, Ls), Bs)
U6_aaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), .(Y, Ls), Bs)
part_in_aaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_aaaa(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
part_in_aaaa(X1, [], [], []) → part_out_aaaa(X1, [], [], [])
U7_aaaa(X, Y, Xs, Ls, Bs, part_out_aaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U1_ag(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_ag(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
qs_in_aa([], []) → qs_out_aa([], [])
qs_in_aa(.(X, Xs), Ys) → U1_aa(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U1_aa(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_aa(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U2_aa(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_aa(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_aa(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_aa(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
app_in_aaa([], X, X) → app_out_aaa([], X, X)
app_in_aaa(.(X, Xs), Ys, .(X, Zs)) → U8_aaa(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
U8_aaa(X, Xs, Ys, Zs, app_out_aaa(Xs, Ys, Zs)) → app_out_aaa(.(X, Xs), Ys, .(X, Zs))
U4_aa(X, Xs, Ys, app_out_aaa(Ls, .(X, Bs), Ys)) → qs_out_aa(.(X, Xs), Ys)
U2_ag(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_ag(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_ag(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_ag(X, Xs, Ys, app_in_aag(Ls, .(X, Bs), Ys))
app_in_aag([], X, X) → app_out_aag([], X, X)
app_in_aag(.(X, Xs), Ys, .(X, Zs)) → U8_aag(X, Xs, Ys, Zs, app_in_aag(Xs, Ys, Zs))
U8_aag(X, Xs, Ys, Zs, app_out_aag(Xs, Ys, Zs)) → app_out_aag(.(X, Xs), Ys, .(X, Zs))
U4_ag(X, Xs, Ys, app_out_aag(Ls, .(X, Bs), Ys)) → qs_out_ag(.(X, Xs), Ys)
QS_IN_AG(.(X, Xs), Ys) → U1_AG(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
QS_IN_AG(.(X, Xs), Ys) → PART_IN_AAAA(X, Xs, Littles, Bigs)
PART_IN_AAAA(X, .(Y, Xs), .(Y, Ls), Bs) → U5_AAAA(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
PART_IN_AAAA(X, .(Y, Xs), .(Y, Ls), Bs) → LESS_IN_AA(X, Y)
LESS_IN_AA(s(X), s(Y)) → U9_AA(X, Y, less_in_aa(X, Y))
LESS_IN_AA(s(X), s(Y)) → LESS_IN_AA(X, Y)
U5_AAAA(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_AAAA(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
U5_AAAA(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → PART_IN_GAAA(X, Xs, Ls, Bs)
PART_IN_GAAA(X, .(Y, Xs), .(Y, Ls), Bs) → U5_GAAA(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
PART_IN_GAAA(X, .(Y, Xs), .(Y, Ls), Bs) → LESS_IN_GA(X, Y)
LESS_IN_GA(s(X), s(Y)) → U9_GA(X, Y, less_in_ga(X, Y))
LESS_IN_GA(s(X), s(Y)) → LESS_IN_GA(X, Y)
U5_GAAA(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_GAAA(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
U5_GAAA(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → PART_IN_GAAA(X, Xs, Ls, Bs)
PART_IN_GAAA(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_GAAA(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
PART_IN_GAAA(X, .(Y, Xs), Ls, .(Y, Bs)) → PART_IN_GAAA(X, Xs, Ls, Bs)
PART_IN_AAAA(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_AAAA(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
PART_IN_AAAA(X, .(Y, Xs), Ls, .(Y, Bs)) → PART_IN_AAAA(X, Xs, Ls, Bs)
U1_AG(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_AG(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U1_AG(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → QS_IN_AA(Littles, Ls)
QS_IN_AA(.(X, Xs), Ys) → U1_AA(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
QS_IN_AA(.(X, Xs), Ys) → PART_IN_AAAA(X, Xs, Littles, Bigs)
U1_AA(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_AA(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U1_AA(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → QS_IN_AA(Littles, Ls)
U2_AA(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_AA(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U2_AA(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → QS_IN_AA(Bigs, Bs)
U3_AA(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_AA(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
U3_AA(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → APP_IN_AAA(Ls, .(X, Bs), Ys)
APP_IN_AAA(.(X, Xs), Ys, .(X, Zs)) → U8_AAA(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
APP_IN_AAA(.(X, Xs), Ys, .(X, Zs)) → APP_IN_AAA(Xs, Ys, Zs)
U2_AG(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_AG(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U2_AG(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → QS_IN_AA(Bigs, Bs)
U3_AG(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_AG(X, Xs, Ys, app_in_aag(Ls, .(X, Bs), Ys))
U3_AG(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → APP_IN_AAG(Ls, .(X, Bs), Ys)
APP_IN_AAG(.(X, Xs), Ys, .(X, Zs)) → U8_AAG(X, Xs, Ys, Zs, app_in_aag(Xs, Ys, Zs))
APP_IN_AAG(.(X, Xs), Ys, .(X, Zs)) → APP_IN_AAG(Xs, Ys, Zs)
qs_in_ag([], []) → qs_out_ag([], [])
qs_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
part_in_aaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_aaaa(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
less_in_aa(0, s(X2)) → less_out_aa(0, s(X2))
less_in_aa(s(X), s(Y)) → U9_aa(X, Y, less_in_aa(X, Y))
U9_aa(X, Y, less_out_aa(X, Y)) → less_out_aa(s(X), s(Y))
U5_aaaa(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_aaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_gaaa(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
less_in_ga(0, s(X2)) → less_out_ga(0, s(X2))
less_in_ga(s(X), s(Y)) → U9_ga(X, Y, less_in_ga(X, Y))
U9_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U5_gaaa(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X1, [], [], []) → part_out_gaaa(X1, [], [], [])
U7_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U6_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), .(Y, Ls), Bs)
U6_aaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), .(Y, Ls), Bs)
part_in_aaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_aaaa(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
part_in_aaaa(X1, [], [], []) → part_out_aaaa(X1, [], [], [])
U7_aaaa(X, Y, Xs, Ls, Bs, part_out_aaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U1_ag(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_ag(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
qs_in_aa([], []) → qs_out_aa([], [])
qs_in_aa(.(X, Xs), Ys) → U1_aa(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U1_aa(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_aa(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U2_aa(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_aa(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_aa(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_aa(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
app_in_aaa([], X, X) → app_out_aaa([], X, X)
app_in_aaa(.(X, Xs), Ys, .(X, Zs)) → U8_aaa(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
U8_aaa(X, Xs, Ys, Zs, app_out_aaa(Xs, Ys, Zs)) → app_out_aaa(.(X, Xs), Ys, .(X, Zs))
U4_aa(X, Xs, Ys, app_out_aaa(Ls, .(X, Bs), Ys)) → qs_out_aa(.(X, Xs), Ys)
U2_ag(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_ag(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_ag(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_ag(X, Xs, Ys, app_in_aag(Ls, .(X, Bs), Ys))
app_in_aag([], X, X) → app_out_aag([], X, X)
app_in_aag(.(X, Xs), Ys, .(X, Zs)) → U8_aag(X, Xs, Ys, Zs, app_in_aag(Xs, Ys, Zs))
U8_aag(X, Xs, Ys, Zs, app_out_aag(Xs, Ys, Zs)) → app_out_aag(.(X, Xs), Ys, .(X, Zs))
U4_ag(X, Xs, Ys, app_out_aag(Ls, .(X, Bs), Ys)) → qs_out_ag(.(X, Xs), Ys)
APP_IN_AAG(.(X, Xs), Ys, .(X, Zs)) → APP_IN_AAG(Xs, Ys, Zs)
qs_in_ag([], []) → qs_out_ag([], [])
qs_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
part_in_aaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_aaaa(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
less_in_aa(0, s(X2)) → less_out_aa(0, s(X2))
less_in_aa(s(X), s(Y)) → U9_aa(X, Y, less_in_aa(X, Y))
U9_aa(X, Y, less_out_aa(X, Y)) → less_out_aa(s(X), s(Y))
U5_aaaa(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_aaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_gaaa(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
less_in_ga(0, s(X2)) → less_out_ga(0, s(X2))
less_in_ga(s(X), s(Y)) → U9_ga(X, Y, less_in_ga(X, Y))
U9_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U5_gaaa(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X1, [], [], []) → part_out_gaaa(X1, [], [], [])
U7_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U6_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), .(Y, Ls), Bs)
U6_aaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), .(Y, Ls), Bs)
part_in_aaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_aaaa(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
part_in_aaaa(X1, [], [], []) → part_out_aaaa(X1, [], [], [])
U7_aaaa(X, Y, Xs, Ls, Bs, part_out_aaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U1_ag(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_ag(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
qs_in_aa([], []) → qs_out_aa([], [])
qs_in_aa(.(X, Xs), Ys) → U1_aa(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U1_aa(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_aa(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U2_aa(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_aa(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_aa(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_aa(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
app_in_aaa([], X, X) → app_out_aaa([], X, X)
app_in_aaa(.(X, Xs), Ys, .(X, Zs)) → U8_aaa(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
U8_aaa(X, Xs, Ys, Zs, app_out_aaa(Xs, Ys, Zs)) → app_out_aaa(.(X, Xs), Ys, .(X, Zs))
U4_aa(X, Xs, Ys, app_out_aaa(Ls, .(X, Bs), Ys)) → qs_out_aa(.(X, Xs), Ys)
U2_ag(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_ag(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_ag(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_ag(X, Xs, Ys, app_in_aag(Ls, .(X, Bs), Ys))
app_in_aag([], X, X) → app_out_aag([], X, X)
app_in_aag(.(X, Xs), Ys, .(X, Zs)) → U8_aag(X, Xs, Ys, Zs, app_in_aag(Xs, Ys, Zs))
U8_aag(X, Xs, Ys, Zs, app_out_aag(Xs, Ys, Zs)) → app_out_aag(.(X, Xs), Ys, .(X, Zs))
U4_ag(X, Xs, Ys, app_out_aag(Ls, .(X, Bs), Ys)) → qs_out_ag(.(X, Xs), Ys)
APP_IN_AAG(.(X, Xs), Ys, .(X, Zs)) → APP_IN_AAG(Xs, Ys, Zs)
APP_IN_AAG(.(X, Zs)) → APP_IN_AAG(Zs)
From the DPs we obtained the following set of size-change graphs:
APP_IN_AAA(.(X, Xs), Ys, .(X, Zs)) → APP_IN_AAA(Xs, Ys, Zs)
qs_in_ag([], []) → qs_out_ag([], [])
qs_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
part_in_aaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_aaaa(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
less_in_aa(0, s(X2)) → less_out_aa(0, s(X2))
less_in_aa(s(X), s(Y)) → U9_aa(X, Y, less_in_aa(X, Y))
U9_aa(X, Y, less_out_aa(X, Y)) → less_out_aa(s(X), s(Y))
U5_aaaa(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_aaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_gaaa(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
less_in_ga(0, s(X2)) → less_out_ga(0, s(X2))
less_in_ga(s(X), s(Y)) → U9_ga(X, Y, less_in_ga(X, Y))
U9_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U5_gaaa(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X1, [], [], []) → part_out_gaaa(X1, [], [], [])
U7_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U6_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), .(Y, Ls), Bs)
U6_aaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), .(Y, Ls), Bs)
part_in_aaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_aaaa(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
part_in_aaaa(X1, [], [], []) → part_out_aaaa(X1, [], [], [])
U7_aaaa(X, Y, Xs, Ls, Bs, part_out_aaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U1_ag(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_ag(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
qs_in_aa([], []) → qs_out_aa([], [])
qs_in_aa(.(X, Xs), Ys) → U1_aa(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U1_aa(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_aa(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U2_aa(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_aa(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_aa(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_aa(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
app_in_aaa([], X, X) → app_out_aaa([], X, X)
app_in_aaa(.(X, Xs), Ys, .(X, Zs)) → U8_aaa(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
U8_aaa(X, Xs, Ys, Zs, app_out_aaa(Xs, Ys, Zs)) → app_out_aaa(.(X, Xs), Ys, .(X, Zs))
U4_aa(X, Xs, Ys, app_out_aaa(Ls, .(X, Bs), Ys)) → qs_out_aa(.(X, Xs), Ys)
U2_ag(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_ag(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_ag(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_ag(X, Xs, Ys, app_in_aag(Ls, .(X, Bs), Ys))
app_in_aag([], X, X) → app_out_aag([], X, X)
app_in_aag(.(X, Xs), Ys, .(X, Zs)) → U8_aag(X, Xs, Ys, Zs, app_in_aag(Xs, Ys, Zs))
U8_aag(X, Xs, Ys, Zs, app_out_aag(Xs, Ys, Zs)) → app_out_aag(.(X, Xs), Ys, .(X, Zs))
U4_ag(X, Xs, Ys, app_out_aag(Ls, .(X, Bs), Ys)) → qs_out_ag(.(X, Xs), Ys)
APP_IN_AAA(.(X, Xs), Ys, .(X, Zs)) → APP_IN_AAA(Xs, Ys, Zs)
APP_IN_AAA → APP_IN_AAA
LESS_IN_GA(s(X), s(Y)) → LESS_IN_GA(X, Y)
qs_in_ag([], []) → qs_out_ag([], [])
qs_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
part_in_aaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_aaaa(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
less_in_aa(0, s(X2)) → less_out_aa(0, s(X2))
less_in_aa(s(X), s(Y)) → U9_aa(X, Y, less_in_aa(X, Y))
U9_aa(X, Y, less_out_aa(X, Y)) → less_out_aa(s(X), s(Y))
U5_aaaa(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_aaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_gaaa(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
less_in_ga(0, s(X2)) → less_out_ga(0, s(X2))
less_in_ga(s(X), s(Y)) → U9_ga(X, Y, less_in_ga(X, Y))
U9_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U5_gaaa(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X1, [], [], []) → part_out_gaaa(X1, [], [], [])
U7_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U6_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), .(Y, Ls), Bs)
U6_aaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), .(Y, Ls), Bs)
part_in_aaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_aaaa(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
part_in_aaaa(X1, [], [], []) → part_out_aaaa(X1, [], [], [])
U7_aaaa(X, Y, Xs, Ls, Bs, part_out_aaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U1_ag(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_ag(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
qs_in_aa([], []) → qs_out_aa([], [])
qs_in_aa(.(X, Xs), Ys) → U1_aa(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U1_aa(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_aa(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U2_aa(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_aa(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_aa(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_aa(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
app_in_aaa([], X, X) → app_out_aaa([], X, X)
app_in_aaa(.(X, Xs), Ys, .(X, Zs)) → U8_aaa(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
U8_aaa(X, Xs, Ys, Zs, app_out_aaa(Xs, Ys, Zs)) → app_out_aaa(.(X, Xs), Ys, .(X, Zs))
U4_aa(X, Xs, Ys, app_out_aaa(Ls, .(X, Bs), Ys)) → qs_out_aa(.(X, Xs), Ys)
U2_ag(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_ag(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_ag(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_ag(X, Xs, Ys, app_in_aag(Ls, .(X, Bs), Ys))
app_in_aag([], X, X) → app_out_aag([], X, X)
app_in_aag(.(X, Xs), Ys, .(X, Zs)) → U8_aag(X, Xs, Ys, Zs, app_in_aag(Xs, Ys, Zs))
U8_aag(X, Xs, Ys, Zs, app_out_aag(Xs, Ys, Zs)) → app_out_aag(.(X, Xs), Ys, .(X, Zs))
U4_ag(X, Xs, Ys, app_out_aag(Ls, .(X, Bs), Ys)) → qs_out_ag(.(X, Xs), Ys)
LESS_IN_GA(s(X), s(Y)) → LESS_IN_GA(X, Y)
LESS_IN_GA(s(X)) → LESS_IN_GA(X)
From the DPs we obtained the following set of size-change graphs:
U5_GAAA(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → PART_IN_GAAA(X, Xs, Ls, Bs)
PART_IN_GAAA(X, .(Y, Xs), .(Y, Ls), Bs) → U5_GAAA(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
PART_IN_GAAA(X, .(Y, Xs), Ls, .(Y, Bs)) → PART_IN_GAAA(X, Xs, Ls, Bs)
qs_in_ag([], []) → qs_out_ag([], [])
qs_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
part_in_aaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_aaaa(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
less_in_aa(0, s(X2)) → less_out_aa(0, s(X2))
less_in_aa(s(X), s(Y)) → U9_aa(X, Y, less_in_aa(X, Y))
U9_aa(X, Y, less_out_aa(X, Y)) → less_out_aa(s(X), s(Y))
U5_aaaa(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_aaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_gaaa(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
less_in_ga(0, s(X2)) → less_out_ga(0, s(X2))
less_in_ga(s(X), s(Y)) → U9_ga(X, Y, less_in_ga(X, Y))
U9_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U5_gaaa(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X1, [], [], []) → part_out_gaaa(X1, [], [], [])
U7_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U6_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), .(Y, Ls), Bs)
U6_aaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), .(Y, Ls), Bs)
part_in_aaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_aaaa(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
part_in_aaaa(X1, [], [], []) → part_out_aaaa(X1, [], [], [])
U7_aaaa(X, Y, Xs, Ls, Bs, part_out_aaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U1_ag(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_ag(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
qs_in_aa([], []) → qs_out_aa([], [])
qs_in_aa(.(X, Xs), Ys) → U1_aa(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U1_aa(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_aa(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U2_aa(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_aa(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_aa(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_aa(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
app_in_aaa([], X, X) → app_out_aaa([], X, X)
app_in_aaa(.(X, Xs), Ys, .(X, Zs)) → U8_aaa(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
U8_aaa(X, Xs, Ys, Zs, app_out_aaa(Xs, Ys, Zs)) → app_out_aaa(.(X, Xs), Ys, .(X, Zs))
U4_aa(X, Xs, Ys, app_out_aaa(Ls, .(X, Bs), Ys)) → qs_out_aa(.(X, Xs), Ys)
U2_ag(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_ag(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_ag(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_ag(X, Xs, Ys, app_in_aag(Ls, .(X, Bs), Ys))
app_in_aag([], X, X) → app_out_aag([], X, X)
app_in_aag(.(X, Xs), Ys, .(X, Zs)) → U8_aag(X, Xs, Ys, Zs, app_in_aag(Xs, Ys, Zs))
U8_aag(X, Xs, Ys, Zs, app_out_aag(Xs, Ys, Zs)) → app_out_aag(.(X, Xs), Ys, .(X, Zs))
U4_ag(X, Xs, Ys, app_out_aag(Ls, .(X, Bs), Ys)) → qs_out_ag(.(X, Xs), Ys)
U5_GAAA(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → PART_IN_GAAA(X, Xs, Ls, Bs)
PART_IN_GAAA(X, .(Y, Xs), .(Y, Ls), Bs) → U5_GAAA(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
PART_IN_GAAA(X, .(Y, Xs), Ls, .(Y, Bs)) → PART_IN_GAAA(X, Xs, Ls, Bs)
less_in_ga(0, s(X2)) → less_out_ga(0, s(X2))
less_in_ga(s(X), s(Y)) → U9_ga(X, Y, less_in_ga(X, Y))
U9_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U5_GAAA(X, less_out_ga(X)) → PART_IN_GAAA(X)
PART_IN_GAAA(X) → U5_GAAA(X, less_in_ga(X))
PART_IN_GAAA(X) → PART_IN_GAAA(X)
less_in_ga(0) → less_out_ga(0)
less_in_ga(s(X)) → U9_ga(X, less_in_ga(X))
U9_ga(X, less_out_ga(X)) → less_out_ga(s(X))
less_in_ga(x0)
U9_ga(x0, x1)
PART_IN_GAAA(0) → U5_GAAA(0, less_out_ga(0))
PART_IN_GAAA(s(x0)) → U5_GAAA(s(x0), U9_ga(x0, less_in_ga(x0)))
U5_GAAA(X, less_out_ga(X)) → PART_IN_GAAA(X)
PART_IN_GAAA(X) → PART_IN_GAAA(X)
PART_IN_GAAA(0) → U5_GAAA(0, less_out_ga(0))
PART_IN_GAAA(s(x0)) → U5_GAAA(s(x0), U9_ga(x0, less_in_ga(x0)))
less_in_ga(0) → less_out_ga(0)
less_in_ga(s(X)) → U9_ga(X, less_in_ga(X))
U9_ga(X, less_out_ga(X)) → less_out_ga(s(X))
less_in_ga(x0)
U9_ga(x0, x1)
U5_GAAA(0, less_out_ga(0)) → PART_IN_GAAA(0)
U5_GAAA(s(z0), less_out_ga(s(z0))) → PART_IN_GAAA(s(z0))
PART_IN_GAAA(X) → PART_IN_GAAA(X)
PART_IN_GAAA(0) → U5_GAAA(0, less_out_ga(0))
PART_IN_GAAA(s(x0)) → U5_GAAA(s(x0), U9_ga(x0, less_in_ga(x0)))
U5_GAAA(0, less_out_ga(0)) → PART_IN_GAAA(0)
U5_GAAA(s(z0), less_out_ga(s(z0))) → PART_IN_GAAA(s(z0))
less_in_ga(0) → less_out_ga(0)
less_in_ga(s(X)) → U9_ga(X, less_in_ga(X))
U9_ga(X, less_out_ga(X)) → less_out_ga(s(X))
less_in_ga(x0)
U9_ga(x0, x1)
LESS_IN_AA(s(X), s(Y)) → LESS_IN_AA(X, Y)
qs_in_ag([], []) → qs_out_ag([], [])
qs_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
part_in_aaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_aaaa(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
less_in_aa(0, s(X2)) → less_out_aa(0, s(X2))
less_in_aa(s(X), s(Y)) → U9_aa(X, Y, less_in_aa(X, Y))
U9_aa(X, Y, less_out_aa(X, Y)) → less_out_aa(s(X), s(Y))
U5_aaaa(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_aaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_gaaa(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
less_in_ga(0, s(X2)) → less_out_ga(0, s(X2))
less_in_ga(s(X), s(Y)) → U9_ga(X, Y, less_in_ga(X, Y))
U9_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U5_gaaa(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X1, [], [], []) → part_out_gaaa(X1, [], [], [])
U7_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U6_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), .(Y, Ls), Bs)
U6_aaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), .(Y, Ls), Bs)
part_in_aaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_aaaa(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
part_in_aaaa(X1, [], [], []) → part_out_aaaa(X1, [], [], [])
U7_aaaa(X, Y, Xs, Ls, Bs, part_out_aaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U1_ag(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_ag(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
qs_in_aa([], []) → qs_out_aa([], [])
qs_in_aa(.(X, Xs), Ys) → U1_aa(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U1_aa(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_aa(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U2_aa(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_aa(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_aa(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_aa(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
app_in_aaa([], X, X) → app_out_aaa([], X, X)
app_in_aaa(.(X, Xs), Ys, .(X, Zs)) → U8_aaa(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
U8_aaa(X, Xs, Ys, Zs, app_out_aaa(Xs, Ys, Zs)) → app_out_aaa(.(X, Xs), Ys, .(X, Zs))
U4_aa(X, Xs, Ys, app_out_aaa(Ls, .(X, Bs), Ys)) → qs_out_aa(.(X, Xs), Ys)
U2_ag(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_ag(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_ag(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_ag(X, Xs, Ys, app_in_aag(Ls, .(X, Bs), Ys))
app_in_aag([], X, X) → app_out_aag([], X, X)
app_in_aag(.(X, Xs), Ys, .(X, Zs)) → U8_aag(X, Xs, Ys, Zs, app_in_aag(Xs, Ys, Zs))
U8_aag(X, Xs, Ys, Zs, app_out_aag(Xs, Ys, Zs)) → app_out_aag(.(X, Xs), Ys, .(X, Zs))
U4_ag(X, Xs, Ys, app_out_aag(Ls, .(X, Bs), Ys)) → qs_out_ag(.(X, Xs), Ys)
LESS_IN_AA(s(X), s(Y)) → LESS_IN_AA(X, Y)
LESS_IN_AA → LESS_IN_AA
PART_IN_AAAA(X, .(Y, Xs), Ls, .(Y, Bs)) → PART_IN_AAAA(X, Xs, Ls, Bs)
qs_in_ag([], []) → qs_out_ag([], [])
qs_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
part_in_aaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_aaaa(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
less_in_aa(0, s(X2)) → less_out_aa(0, s(X2))
less_in_aa(s(X), s(Y)) → U9_aa(X, Y, less_in_aa(X, Y))
U9_aa(X, Y, less_out_aa(X, Y)) → less_out_aa(s(X), s(Y))
U5_aaaa(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_aaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_gaaa(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
less_in_ga(0, s(X2)) → less_out_ga(0, s(X2))
less_in_ga(s(X), s(Y)) → U9_ga(X, Y, less_in_ga(X, Y))
U9_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U5_gaaa(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X1, [], [], []) → part_out_gaaa(X1, [], [], [])
U7_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U6_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), .(Y, Ls), Bs)
U6_aaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), .(Y, Ls), Bs)
part_in_aaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_aaaa(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
part_in_aaaa(X1, [], [], []) → part_out_aaaa(X1, [], [], [])
U7_aaaa(X, Y, Xs, Ls, Bs, part_out_aaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U1_ag(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_ag(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
qs_in_aa([], []) → qs_out_aa([], [])
qs_in_aa(.(X, Xs), Ys) → U1_aa(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U1_aa(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_aa(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U2_aa(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_aa(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_aa(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_aa(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
app_in_aaa([], X, X) → app_out_aaa([], X, X)
app_in_aaa(.(X, Xs), Ys, .(X, Zs)) → U8_aaa(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
U8_aaa(X, Xs, Ys, Zs, app_out_aaa(Xs, Ys, Zs)) → app_out_aaa(.(X, Xs), Ys, .(X, Zs))
U4_aa(X, Xs, Ys, app_out_aaa(Ls, .(X, Bs), Ys)) → qs_out_aa(.(X, Xs), Ys)
U2_ag(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_ag(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_ag(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_ag(X, Xs, Ys, app_in_aag(Ls, .(X, Bs), Ys))
app_in_aag([], X, X) → app_out_aag([], X, X)
app_in_aag(.(X, Xs), Ys, .(X, Zs)) → U8_aag(X, Xs, Ys, Zs, app_in_aag(Xs, Ys, Zs))
U8_aag(X, Xs, Ys, Zs, app_out_aag(Xs, Ys, Zs)) → app_out_aag(.(X, Xs), Ys, .(X, Zs))
U4_ag(X, Xs, Ys, app_out_aag(Ls, .(X, Bs), Ys)) → qs_out_ag(.(X, Xs), Ys)
PART_IN_AAAA(X, .(Y, Xs), Ls, .(Y, Bs)) → PART_IN_AAAA(X, Xs, Ls, Bs)
PART_IN_AAAA → PART_IN_AAAA
QS_IN_AA(.(X, Xs), Ys) → U1_AA(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U1_AA(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_AA(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U2_AA(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → QS_IN_AA(Bigs, Bs)
U1_AA(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → QS_IN_AA(Littles, Ls)
qs_in_ag([], []) → qs_out_ag([], [])
qs_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
part_in_aaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_aaaa(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
less_in_aa(0, s(X2)) → less_out_aa(0, s(X2))
less_in_aa(s(X), s(Y)) → U9_aa(X, Y, less_in_aa(X, Y))
U9_aa(X, Y, less_out_aa(X, Y)) → less_out_aa(s(X), s(Y))
U5_aaaa(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_aaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_gaaa(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
less_in_ga(0, s(X2)) → less_out_ga(0, s(X2))
less_in_ga(s(X), s(Y)) → U9_ga(X, Y, less_in_ga(X, Y))
U9_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U5_gaaa(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X1, [], [], []) → part_out_gaaa(X1, [], [], [])
U7_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U6_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), .(Y, Ls), Bs)
U6_aaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), .(Y, Ls), Bs)
part_in_aaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_aaaa(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
part_in_aaaa(X1, [], [], []) → part_out_aaaa(X1, [], [], [])
U7_aaaa(X, Y, Xs, Ls, Bs, part_out_aaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U1_ag(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_ag(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
qs_in_aa([], []) → qs_out_aa([], [])
qs_in_aa(.(X, Xs), Ys) → U1_aa(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U1_aa(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_aa(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U2_aa(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_aa(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_aa(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_aa(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
app_in_aaa([], X, X) → app_out_aaa([], X, X)
app_in_aaa(.(X, Xs), Ys, .(X, Zs)) → U8_aaa(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
U8_aaa(X, Xs, Ys, Zs, app_out_aaa(Xs, Ys, Zs)) → app_out_aaa(.(X, Xs), Ys, .(X, Zs))
U4_aa(X, Xs, Ys, app_out_aaa(Ls, .(X, Bs), Ys)) → qs_out_aa(.(X, Xs), Ys)
U2_ag(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_ag(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_ag(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_ag(X, Xs, Ys, app_in_aag(Ls, .(X, Bs), Ys))
app_in_aag([], X, X) → app_out_aag([], X, X)
app_in_aag(.(X, Xs), Ys, .(X, Zs)) → U8_aag(X, Xs, Ys, Zs, app_in_aag(Xs, Ys, Zs))
U8_aag(X, Xs, Ys, Zs, app_out_aag(Xs, Ys, Zs)) → app_out_aag(.(X, Xs), Ys, .(X, Zs))
U4_ag(X, Xs, Ys, app_out_aag(Ls, .(X, Bs), Ys)) → qs_out_ag(.(X, Xs), Ys)
QS_IN_AA(.(X, Xs), Ys) → U1_AA(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U1_AA(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_AA(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U2_AA(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → QS_IN_AA(Bigs, Bs)
U1_AA(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → QS_IN_AA(Littles, Ls)
part_in_aaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_aaaa(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
part_in_aaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_aaaa(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
part_in_aaaa(X1, [], [], []) → part_out_aaaa(X1, [], [], [])
qs_in_aa([], []) → qs_out_aa([], [])
qs_in_aa(.(X, Xs), Ys) → U1_aa(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U5_aaaa(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_aaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
U7_aaaa(X, Y, Xs, Ls, Bs, part_out_aaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U1_aa(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_aa(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
less_in_aa(0, s(X2)) → less_out_aa(0, s(X2))
less_in_aa(s(X), s(Y)) → U9_aa(X, Y, less_in_aa(X, Y))
U6_aaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), .(Y, Ls), Bs)
U2_aa(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_aa(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U9_aa(X, Y, less_out_aa(X, Y)) → less_out_aa(s(X), s(Y))
part_in_gaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_gaaa(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
part_in_gaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X1, [], [], []) → part_out_gaaa(X1, [], [], [])
U3_aa(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_aa(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
U5_gaaa(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
U7_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U4_aa(X, Xs, Ys, app_out_aaa(Ls, .(X, Bs), Ys)) → qs_out_aa(.(X, Xs), Ys)
less_in_ga(0, s(X2)) → less_out_ga(0, s(X2))
less_in_ga(s(X), s(Y)) → U9_ga(X, Y, less_in_ga(X, Y))
U6_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), .(Y, Ls), Bs)
app_in_aaa([], X, X) → app_out_aaa([], X, X)
app_in_aaa(.(X, Xs), Ys, .(X, Zs)) → U8_aaa(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
U9_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U8_aaa(X, Xs, Ys, Zs, app_out_aaa(Xs, Ys, Zs)) → app_out_aaa(.(X, Xs), Ys, .(X, Zs))
QS_IN_AA → U1_AA(part_in_aaaa)
U1_AA(part_out_aaaa) → U2_AA(qs_in_aa)
U2_AA(qs_out_aa) → QS_IN_AA
U1_AA(part_out_aaaa) → QS_IN_AA
part_in_aaaa → U5_aaaa(less_in_aa)
part_in_aaaa → U7_aaaa(part_in_aaaa)
part_in_aaaa → part_out_aaaa
qs_in_aa → qs_out_aa
qs_in_aa → U1_aa(part_in_aaaa)
U5_aaaa(less_out_aa(X)) → U6_aaaa(part_in_gaaa(X))
U7_aaaa(part_out_aaaa) → part_out_aaaa
U1_aa(part_out_aaaa) → U2_aa(qs_in_aa)
less_in_aa → less_out_aa(0)
less_in_aa → U9_aa(less_in_aa)
U6_aaaa(part_out_gaaa(X)) → part_out_aaaa
U2_aa(qs_out_aa) → U3_aa(qs_in_aa)
U9_aa(less_out_aa(X)) → less_out_aa(s(X))
part_in_gaaa(X) → U5_gaaa(X, less_in_ga(X))
part_in_gaaa(X) → U7_gaaa(X, part_in_gaaa(X))
part_in_gaaa(X1) → part_out_gaaa(X1)
U3_aa(qs_out_aa) → U4_aa(app_in_aaa)
U5_gaaa(X, less_out_ga(X)) → U6_gaaa(X, part_in_gaaa(X))
U7_gaaa(X, part_out_gaaa(X)) → part_out_gaaa(X)
U4_aa(app_out_aaa) → qs_out_aa
less_in_ga(0) → less_out_ga(0)
less_in_ga(s(X)) → U9_ga(X, less_in_ga(X))
U6_gaaa(X, part_out_gaaa(X)) → part_out_gaaa(X)
app_in_aaa → app_out_aaa
app_in_aaa → U8_aaa(app_in_aaa)
U9_ga(X, less_out_ga(X)) → less_out_ga(s(X))
U8_aaa(app_out_aaa) → app_out_aaa
part_in_aaaa
qs_in_aa
U5_aaaa(x0)
U7_aaaa(x0)
U1_aa(x0)
less_in_aa
U6_aaaa(x0)
U2_aa(x0)
U9_aa(x0)
part_in_gaaa(x0)
U3_aa(x0)
U5_gaaa(x0, x1)
U7_gaaa(x0, x1)
U4_aa(x0)
less_in_ga(x0)
U6_gaaa(x0, x1)
app_in_aaa
U9_ga(x0, x1)
U8_aaa(x0)
QS_IN_AA → U1_AA(U5_aaaa(less_in_aa))
QS_IN_AA → U1_AA(U7_aaaa(part_in_aaaa))
QS_IN_AA → U1_AA(part_out_aaaa)
U1_AA(part_out_aaaa) → U2_AA(qs_in_aa)
U2_AA(qs_out_aa) → QS_IN_AA
U1_AA(part_out_aaaa) → QS_IN_AA
QS_IN_AA → U1_AA(U5_aaaa(less_in_aa))
QS_IN_AA → U1_AA(U7_aaaa(part_in_aaaa))
QS_IN_AA → U1_AA(part_out_aaaa)
part_in_aaaa → U5_aaaa(less_in_aa)
part_in_aaaa → U7_aaaa(part_in_aaaa)
part_in_aaaa → part_out_aaaa
qs_in_aa → qs_out_aa
qs_in_aa → U1_aa(part_in_aaaa)
U5_aaaa(less_out_aa(X)) → U6_aaaa(part_in_gaaa(X))
U7_aaaa(part_out_aaaa) → part_out_aaaa
U1_aa(part_out_aaaa) → U2_aa(qs_in_aa)
less_in_aa → less_out_aa(0)
less_in_aa → U9_aa(less_in_aa)
U6_aaaa(part_out_gaaa(X)) → part_out_aaaa
U2_aa(qs_out_aa) → U3_aa(qs_in_aa)
U9_aa(less_out_aa(X)) → less_out_aa(s(X))
part_in_gaaa(X) → U5_gaaa(X, less_in_ga(X))
part_in_gaaa(X) → U7_gaaa(X, part_in_gaaa(X))
part_in_gaaa(X1) → part_out_gaaa(X1)
U3_aa(qs_out_aa) → U4_aa(app_in_aaa)
U5_gaaa(X, less_out_ga(X)) → U6_gaaa(X, part_in_gaaa(X))
U7_gaaa(X, part_out_gaaa(X)) → part_out_gaaa(X)
U4_aa(app_out_aaa) → qs_out_aa
less_in_ga(0) → less_out_ga(0)
less_in_ga(s(X)) → U9_ga(X, less_in_ga(X))
U6_gaaa(X, part_out_gaaa(X)) → part_out_gaaa(X)
app_in_aaa → app_out_aaa
app_in_aaa → U8_aaa(app_in_aaa)
U9_ga(X, less_out_ga(X)) → less_out_ga(s(X))
U8_aaa(app_out_aaa) → app_out_aaa
part_in_aaaa
qs_in_aa
U5_aaaa(x0)
U7_aaaa(x0)
U1_aa(x0)
less_in_aa
U6_aaaa(x0)
U2_aa(x0)
U9_aa(x0)
part_in_gaaa(x0)
U3_aa(x0)
U5_gaaa(x0, x1)
U7_gaaa(x0, x1)
U4_aa(x0)
less_in_ga(x0)
U6_gaaa(x0, x1)
app_in_aaa
U9_ga(x0, x1)
U8_aaa(x0)
U1_AA(part_out_aaaa) → U2_AA(qs_out_aa)
U1_AA(part_out_aaaa) → U2_AA(U1_aa(part_in_aaaa))
U2_AA(qs_out_aa) → QS_IN_AA
U1_AA(part_out_aaaa) → QS_IN_AA
QS_IN_AA → U1_AA(U5_aaaa(less_in_aa))
QS_IN_AA → U1_AA(U7_aaaa(part_in_aaaa))
QS_IN_AA → U1_AA(part_out_aaaa)
U1_AA(part_out_aaaa) → U2_AA(qs_out_aa)
U1_AA(part_out_aaaa) → U2_AA(U1_aa(part_in_aaaa))
part_in_aaaa → U5_aaaa(less_in_aa)
part_in_aaaa → U7_aaaa(part_in_aaaa)
part_in_aaaa → part_out_aaaa
qs_in_aa → qs_out_aa
qs_in_aa → U1_aa(part_in_aaaa)
U5_aaaa(less_out_aa(X)) → U6_aaaa(part_in_gaaa(X))
U7_aaaa(part_out_aaaa) → part_out_aaaa
U1_aa(part_out_aaaa) → U2_aa(qs_in_aa)
less_in_aa → less_out_aa(0)
less_in_aa → U9_aa(less_in_aa)
U6_aaaa(part_out_gaaa(X)) → part_out_aaaa
U2_aa(qs_out_aa) → U3_aa(qs_in_aa)
U9_aa(less_out_aa(X)) → less_out_aa(s(X))
part_in_gaaa(X) → U5_gaaa(X, less_in_ga(X))
part_in_gaaa(X) → U7_gaaa(X, part_in_gaaa(X))
part_in_gaaa(X1) → part_out_gaaa(X1)
U3_aa(qs_out_aa) → U4_aa(app_in_aaa)
U5_gaaa(X, less_out_ga(X)) → U6_gaaa(X, part_in_gaaa(X))
U7_gaaa(X, part_out_gaaa(X)) → part_out_gaaa(X)
U4_aa(app_out_aaa) → qs_out_aa
less_in_ga(0) → less_out_ga(0)
less_in_ga(s(X)) → U9_ga(X, less_in_ga(X))
U6_gaaa(X, part_out_gaaa(X)) → part_out_gaaa(X)
app_in_aaa → app_out_aaa
app_in_aaa → U8_aaa(app_in_aaa)
U9_ga(X, less_out_ga(X)) → less_out_ga(s(X))
U8_aaa(app_out_aaa) → app_out_aaa
part_in_aaaa
qs_in_aa
U5_aaaa(x0)
U7_aaaa(x0)
U1_aa(x0)
less_in_aa
U6_aaaa(x0)
U2_aa(x0)
U9_aa(x0)
part_in_gaaa(x0)
U3_aa(x0)
U5_gaaa(x0, x1)
U7_gaaa(x0, x1)
U4_aa(x0)
less_in_ga(x0)
U6_gaaa(x0, x1)
app_in_aaa
U9_ga(x0, x1)
U8_aaa(x0)
qs_in_ag([], []) → qs_out_ag([], [])
qs_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
part_in_aaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_aaaa(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
less_in_aa(0, s(X2)) → less_out_aa(0, s(X2))
less_in_aa(s(X), s(Y)) → U9_aa(X, Y, less_in_aa(X, Y))
U9_aa(X, Y, less_out_aa(X, Y)) → less_out_aa(s(X), s(Y))
U5_aaaa(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_aaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_gaaa(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
less_in_ga(0, s(X2)) → less_out_ga(0, s(X2))
less_in_ga(s(X), s(Y)) → U9_ga(X, Y, less_in_ga(X, Y))
U9_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U5_gaaa(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X1, [], [], []) → part_out_gaaa(X1, [], [], [])
U7_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U6_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), .(Y, Ls), Bs)
U6_aaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), .(Y, Ls), Bs)
part_in_aaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_aaaa(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
part_in_aaaa(X1, [], [], []) → part_out_aaaa(X1, [], [], [])
U7_aaaa(X, Y, Xs, Ls, Bs, part_out_aaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U1_ag(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_ag(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
qs_in_aa([], []) → qs_out_aa([], [])
qs_in_aa(.(X, Xs), Ys) → U1_aa(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U1_aa(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_aa(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U2_aa(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_aa(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_aa(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_aa(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
app_in_aaa([], X, X) → app_out_aaa([], X, X)
app_in_aaa(.(X, Xs), Ys, .(X, Zs)) → U8_aaa(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
U8_aaa(X, Xs, Ys, Zs, app_out_aaa(Xs, Ys, Zs)) → app_out_aaa(.(X, Xs), Ys, .(X, Zs))
U4_aa(X, Xs, Ys, app_out_aaa(Ls, .(X, Bs), Ys)) → qs_out_aa(.(X, Xs), Ys)
U2_ag(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_ag(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_ag(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_ag(X, Xs, Ys, app_in_aag(Ls, .(X, Bs), Ys))
app_in_aag([], X, X) → app_out_aag([], X, X)
app_in_aag(.(X, Xs), Ys, .(X, Zs)) → U8_aag(X, Xs, Ys, Zs, app_in_aag(Xs, Ys, Zs))
U8_aag(X, Xs, Ys, Zs, app_out_aag(Xs, Ys, Zs)) → app_out_aag(.(X, Xs), Ys, .(X, Zs))
U4_ag(X, Xs, Ys, app_out_aag(Ls, .(X, Bs), Ys)) → qs_out_ag(.(X, Xs), Ys)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
qs_in_ag([], []) → qs_out_ag([], [])
qs_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
part_in_aaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_aaaa(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
less_in_aa(0, s(X2)) → less_out_aa(0, s(X2))
less_in_aa(s(X), s(Y)) → U9_aa(X, Y, less_in_aa(X, Y))
U9_aa(X, Y, less_out_aa(X, Y)) → less_out_aa(s(X), s(Y))
U5_aaaa(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_aaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_gaaa(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
less_in_ga(0, s(X2)) → less_out_ga(0, s(X2))
less_in_ga(s(X), s(Y)) → U9_ga(X, Y, less_in_ga(X, Y))
U9_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U5_gaaa(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X1, [], [], []) → part_out_gaaa(X1, [], [], [])
U7_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U6_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), .(Y, Ls), Bs)
U6_aaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), .(Y, Ls), Bs)
part_in_aaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_aaaa(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
part_in_aaaa(X1, [], [], []) → part_out_aaaa(X1, [], [], [])
U7_aaaa(X, Y, Xs, Ls, Bs, part_out_aaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U1_ag(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_ag(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
qs_in_aa([], []) → qs_out_aa([], [])
qs_in_aa(.(X, Xs), Ys) → U1_aa(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U1_aa(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_aa(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U2_aa(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_aa(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_aa(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_aa(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
app_in_aaa([], X, X) → app_out_aaa([], X, X)
app_in_aaa(.(X, Xs), Ys, .(X, Zs)) → U8_aaa(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
U8_aaa(X, Xs, Ys, Zs, app_out_aaa(Xs, Ys, Zs)) → app_out_aaa(.(X, Xs), Ys, .(X, Zs))
U4_aa(X, Xs, Ys, app_out_aaa(Ls, .(X, Bs), Ys)) → qs_out_aa(.(X, Xs), Ys)
U2_ag(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_ag(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_ag(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_ag(X, Xs, Ys, app_in_aag(Ls, .(X, Bs), Ys))
app_in_aag([], X, X) → app_out_aag([], X, X)
app_in_aag(.(X, Xs), Ys, .(X, Zs)) → U8_aag(X, Xs, Ys, Zs, app_in_aag(Xs, Ys, Zs))
U8_aag(X, Xs, Ys, Zs, app_out_aag(Xs, Ys, Zs)) → app_out_aag(.(X, Xs), Ys, .(X, Zs))
U4_ag(X, Xs, Ys, app_out_aag(Ls, .(X, Bs), Ys)) → qs_out_ag(.(X, Xs), Ys)
QS_IN_AG(.(X, Xs), Ys) → U1_AG(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
QS_IN_AG(.(X, Xs), Ys) → PART_IN_AAAA(X, Xs, Littles, Bigs)
PART_IN_AAAA(X, .(Y, Xs), .(Y, Ls), Bs) → U5_AAAA(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
PART_IN_AAAA(X, .(Y, Xs), .(Y, Ls), Bs) → LESS_IN_AA(X, Y)
LESS_IN_AA(s(X), s(Y)) → U9_AA(X, Y, less_in_aa(X, Y))
LESS_IN_AA(s(X), s(Y)) → LESS_IN_AA(X, Y)
U5_AAAA(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_AAAA(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
U5_AAAA(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → PART_IN_GAAA(X, Xs, Ls, Bs)
PART_IN_GAAA(X, .(Y, Xs), .(Y, Ls), Bs) → U5_GAAA(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
PART_IN_GAAA(X, .(Y, Xs), .(Y, Ls), Bs) → LESS_IN_GA(X, Y)
LESS_IN_GA(s(X), s(Y)) → U9_GA(X, Y, less_in_ga(X, Y))
LESS_IN_GA(s(X), s(Y)) → LESS_IN_GA(X, Y)
U5_GAAA(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_GAAA(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
U5_GAAA(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → PART_IN_GAAA(X, Xs, Ls, Bs)
PART_IN_GAAA(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_GAAA(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
PART_IN_GAAA(X, .(Y, Xs), Ls, .(Y, Bs)) → PART_IN_GAAA(X, Xs, Ls, Bs)
PART_IN_AAAA(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_AAAA(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
PART_IN_AAAA(X, .(Y, Xs), Ls, .(Y, Bs)) → PART_IN_AAAA(X, Xs, Ls, Bs)
U1_AG(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_AG(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U1_AG(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → QS_IN_AA(Littles, Ls)
QS_IN_AA(.(X, Xs), Ys) → U1_AA(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
QS_IN_AA(.(X, Xs), Ys) → PART_IN_AAAA(X, Xs, Littles, Bigs)
U1_AA(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_AA(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U1_AA(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → QS_IN_AA(Littles, Ls)
U2_AA(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_AA(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U2_AA(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → QS_IN_AA(Bigs, Bs)
U3_AA(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_AA(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
U3_AA(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → APP_IN_AAA(Ls, .(X, Bs), Ys)
APP_IN_AAA(.(X, Xs), Ys, .(X, Zs)) → U8_AAA(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
APP_IN_AAA(.(X, Xs), Ys, .(X, Zs)) → APP_IN_AAA(Xs, Ys, Zs)
U2_AG(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_AG(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U2_AG(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → QS_IN_AA(Bigs, Bs)
U3_AG(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_AG(X, Xs, Ys, app_in_aag(Ls, .(X, Bs), Ys))
U3_AG(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → APP_IN_AAG(Ls, .(X, Bs), Ys)
APP_IN_AAG(.(X, Xs), Ys, .(X, Zs)) → U8_AAG(X, Xs, Ys, Zs, app_in_aag(Xs, Ys, Zs))
APP_IN_AAG(.(X, Xs), Ys, .(X, Zs)) → APP_IN_AAG(Xs, Ys, Zs)
qs_in_ag([], []) → qs_out_ag([], [])
qs_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
part_in_aaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_aaaa(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
less_in_aa(0, s(X2)) → less_out_aa(0, s(X2))
less_in_aa(s(X), s(Y)) → U9_aa(X, Y, less_in_aa(X, Y))
U9_aa(X, Y, less_out_aa(X, Y)) → less_out_aa(s(X), s(Y))
U5_aaaa(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_aaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_gaaa(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
less_in_ga(0, s(X2)) → less_out_ga(0, s(X2))
less_in_ga(s(X), s(Y)) → U9_ga(X, Y, less_in_ga(X, Y))
U9_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U5_gaaa(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X1, [], [], []) → part_out_gaaa(X1, [], [], [])
U7_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U6_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), .(Y, Ls), Bs)
U6_aaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), .(Y, Ls), Bs)
part_in_aaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_aaaa(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
part_in_aaaa(X1, [], [], []) → part_out_aaaa(X1, [], [], [])
U7_aaaa(X, Y, Xs, Ls, Bs, part_out_aaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U1_ag(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_ag(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
qs_in_aa([], []) → qs_out_aa([], [])
qs_in_aa(.(X, Xs), Ys) → U1_aa(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U1_aa(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_aa(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U2_aa(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_aa(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_aa(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_aa(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
app_in_aaa([], X, X) → app_out_aaa([], X, X)
app_in_aaa(.(X, Xs), Ys, .(X, Zs)) → U8_aaa(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
U8_aaa(X, Xs, Ys, Zs, app_out_aaa(Xs, Ys, Zs)) → app_out_aaa(.(X, Xs), Ys, .(X, Zs))
U4_aa(X, Xs, Ys, app_out_aaa(Ls, .(X, Bs), Ys)) → qs_out_aa(.(X, Xs), Ys)
U2_ag(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_ag(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_ag(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_ag(X, Xs, Ys, app_in_aag(Ls, .(X, Bs), Ys))
app_in_aag([], X, X) → app_out_aag([], X, X)
app_in_aag(.(X, Xs), Ys, .(X, Zs)) → U8_aag(X, Xs, Ys, Zs, app_in_aag(Xs, Ys, Zs))
U8_aag(X, Xs, Ys, Zs, app_out_aag(Xs, Ys, Zs)) → app_out_aag(.(X, Xs), Ys, .(X, Zs))
U4_ag(X, Xs, Ys, app_out_aag(Ls, .(X, Bs), Ys)) → qs_out_ag(.(X, Xs), Ys)
QS_IN_AG(.(X, Xs), Ys) → U1_AG(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
QS_IN_AG(.(X, Xs), Ys) → PART_IN_AAAA(X, Xs, Littles, Bigs)
PART_IN_AAAA(X, .(Y, Xs), .(Y, Ls), Bs) → U5_AAAA(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
PART_IN_AAAA(X, .(Y, Xs), .(Y, Ls), Bs) → LESS_IN_AA(X, Y)
LESS_IN_AA(s(X), s(Y)) → U9_AA(X, Y, less_in_aa(X, Y))
LESS_IN_AA(s(X), s(Y)) → LESS_IN_AA(X, Y)
U5_AAAA(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_AAAA(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
U5_AAAA(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → PART_IN_GAAA(X, Xs, Ls, Bs)
PART_IN_GAAA(X, .(Y, Xs), .(Y, Ls), Bs) → U5_GAAA(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
PART_IN_GAAA(X, .(Y, Xs), .(Y, Ls), Bs) → LESS_IN_GA(X, Y)
LESS_IN_GA(s(X), s(Y)) → U9_GA(X, Y, less_in_ga(X, Y))
LESS_IN_GA(s(X), s(Y)) → LESS_IN_GA(X, Y)
U5_GAAA(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_GAAA(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
U5_GAAA(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → PART_IN_GAAA(X, Xs, Ls, Bs)
PART_IN_GAAA(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_GAAA(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
PART_IN_GAAA(X, .(Y, Xs), Ls, .(Y, Bs)) → PART_IN_GAAA(X, Xs, Ls, Bs)
PART_IN_AAAA(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_AAAA(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
PART_IN_AAAA(X, .(Y, Xs), Ls, .(Y, Bs)) → PART_IN_AAAA(X, Xs, Ls, Bs)
U1_AG(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_AG(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U1_AG(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → QS_IN_AA(Littles, Ls)
QS_IN_AA(.(X, Xs), Ys) → U1_AA(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
QS_IN_AA(.(X, Xs), Ys) → PART_IN_AAAA(X, Xs, Littles, Bigs)
U1_AA(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_AA(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U1_AA(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → QS_IN_AA(Littles, Ls)
U2_AA(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_AA(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U2_AA(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → QS_IN_AA(Bigs, Bs)
U3_AA(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_AA(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
U3_AA(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → APP_IN_AAA(Ls, .(X, Bs), Ys)
APP_IN_AAA(.(X, Xs), Ys, .(X, Zs)) → U8_AAA(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
APP_IN_AAA(.(X, Xs), Ys, .(X, Zs)) → APP_IN_AAA(Xs, Ys, Zs)
U2_AG(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_AG(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U2_AG(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → QS_IN_AA(Bigs, Bs)
U3_AG(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_AG(X, Xs, Ys, app_in_aag(Ls, .(X, Bs), Ys))
U3_AG(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → APP_IN_AAG(Ls, .(X, Bs), Ys)
APP_IN_AAG(.(X, Xs), Ys, .(X, Zs)) → U8_AAG(X, Xs, Ys, Zs, app_in_aag(Xs, Ys, Zs))
APP_IN_AAG(.(X, Xs), Ys, .(X, Zs)) → APP_IN_AAG(Xs, Ys, Zs)
qs_in_ag([], []) → qs_out_ag([], [])
qs_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
part_in_aaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_aaaa(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
less_in_aa(0, s(X2)) → less_out_aa(0, s(X2))
less_in_aa(s(X), s(Y)) → U9_aa(X, Y, less_in_aa(X, Y))
U9_aa(X, Y, less_out_aa(X, Y)) → less_out_aa(s(X), s(Y))
U5_aaaa(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_aaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_gaaa(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
less_in_ga(0, s(X2)) → less_out_ga(0, s(X2))
less_in_ga(s(X), s(Y)) → U9_ga(X, Y, less_in_ga(X, Y))
U9_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U5_gaaa(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X1, [], [], []) → part_out_gaaa(X1, [], [], [])
U7_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U6_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), .(Y, Ls), Bs)
U6_aaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), .(Y, Ls), Bs)
part_in_aaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_aaaa(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
part_in_aaaa(X1, [], [], []) → part_out_aaaa(X1, [], [], [])
U7_aaaa(X, Y, Xs, Ls, Bs, part_out_aaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U1_ag(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_ag(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
qs_in_aa([], []) → qs_out_aa([], [])
qs_in_aa(.(X, Xs), Ys) → U1_aa(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U1_aa(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_aa(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U2_aa(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_aa(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_aa(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_aa(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
app_in_aaa([], X, X) → app_out_aaa([], X, X)
app_in_aaa(.(X, Xs), Ys, .(X, Zs)) → U8_aaa(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
U8_aaa(X, Xs, Ys, Zs, app_out_aaa(Xs, Ys, Zs)) → app_out_aaa(.(X, Xs), Ys, .(X, Zs))
U4_aa(X, Xs, Ys, app_out_aaa(Ls, .(X, Bs), Ys)) → qs_out_aa(.(X, Xs), Ys)
U2_ag(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_ag(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_ag(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_ag(X, Xs, Ys, app_in_aag(Ls, .(X, Bs), Ys))
app_in_aag([], X, X) → app_out_aag([], X, X)
app_in_aag(.(X, Xs), Ys, .(X, Zs)) → U8_aag(X, Xs, Ys, Zs, app_in_aag(Xs, Ys, Zs))
U8_aag(X, Xs, Ys, Zs, app_out_aag(Xs, Ys, Zs)) → app_out_aag(.(X, Xs), Ys, .(X, Zs))
U4_ag(X, Xs, Ys, app_out_aag(Ls, .(X, Bs), Ys)) → qs_out_ag(.(X, Xs), Ys)
APP_IN_AAG(.(X, Xs), Ys, .(X, Zs)) → APP_IN_AAG(Xs, Ys, Zs)
qs_in_ag([], []) → qs_out_ag([], [])
qs_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
part_in_aaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_aaaa(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
less_in_aa(0, s(X2)) → less_out_aa(0, s(X2))
less_in_aa(s(X), s(Y)) → U9_aa(X, Y, less_in_aa(X, Y))
U9_aa(X, Y, less_out_aa(X, Y)) → less_out_aa(s(X), s(Y))
U5_aaaa(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_aaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_gaaa(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
less_in_ga(0, s(X2)) → less_out_ga(0, s(X2))
less_in_ga(s(X), s(Y)) → U9_ga(X, Y, less_in_ga(X, Y))
U9_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U5_gaaa(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X1, [], [], []) → part_out_gaaa(X1, [], [], [])
U7_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U6_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), .(Y, Ls), Bs)
U6_aaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), .(Y, Ls), Bs)
part_in_aaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_aaaa(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
part_in_aaaa(X1, [], [], []) → part_out_aaaa(X1, [], [], [])
U7_aaaa(X, Y, Xs, Ls, Bs, part_out_aaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U1_ag(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_ag(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
qs_in_aa([], []) → qs_out_aa([], [])
qs_in_aa(.(X, Xs), Ys) → U1_aa(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U1_aa(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_aa(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U2_aa(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_aa(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_aa(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_aa(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
app_in_aaa([], X, X) → app_out_aaa([], X, X)
app_in_aaa(.(X, Xs), Ys, .(X, Zs)) → U8_aaa(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
U8_aaa(X, Xs, Ys, Zs, app_out_aaa(Xs, Ys, Zs)) → app_out_aaa(.(X, Xs), Ys, .(X, Zs))
U4_aa(X, Xs, Ys, app_out_aaa(Ls, .(X, Bs), Ys)) → qs_out_aa(.(X, Xs), Ys)
U2_ag(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_ag(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_ag(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_ag(X, Xs, Ys, app_in_aag(Ls, .(X, Bs), Ys))
app_in_aag([], X, X) → app_out_aag([], X, X)
app_in_aag(.(X, Xs), Ys, .(X, Zs)) → U8_aag(X, Xs, Ys, Zs, app_in_aag(Xs, Ys, Zs))
U8_aag(X, Xs, Ys, Zs, app_out_aag(Xs, Ys, Zs)) → app_out_aag(.(X, Xs), Ys, .(X, Zs))
U4_ag(X, Xs, Ys, app_out_aag(Ls, .(X, Bs), Ys)) → qs_out_ag(.(X, Xs), Ys)
APP_IN_AAG(.(X, Xs), Ys, .(X, Zs)) → APP_IN_AAG(Xs, Ys, Zs)
APP_IN_AAG(.(X, Zs)) → APP_IN_AAG(Zs)
From the DPs we obtained the following set of size-change graphs:
APP_IN_AAA(.(X, Xs), Ys, .(X, Zs)) → APP_IN_AAA(Xs, Ys, Zs)
qs_in_ag([], []) → qs_out_ag([], [])
qs_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
part_in_aaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_aaaa(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
less_in_aa(0, s(X2)) → less_out_aa(0, s(X2))
less_in_aa(s(X), s(Y)) → U9_aa(X, Y, less_in_aa(X, Y))
U9_aa(X, Y, less_out_aa(X, Y)) → less_out_aa(s(X), s(Y))
U5_aaaa(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_aaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_gaaa(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
less_in_ga(0, s(X2)) → less_out_ga(0, s(X2))
less_in_ga(s(X), s(Y)) → U9_ga(X, Y, less_in_ga(X, Y))
U9_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U5_gaaa(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X1, [], [], []) → part_out_gaaa(X1, [], [], [])
U7_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U6_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), .(Y, Ls), Bs)
U6_aaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), .(Y, Ls), Bs)
part_in_aaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_aaaa(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
part_in_aaaa(X1, [], [], []) → part_out_aaaa(X1, [], [], [])
U7_aaaa(X, Y, Xs, Ls, Bs, part_out_aaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U1_ag(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_ag(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
qs_in_aa([], []) → qs_out_aa([], [])
qs_in_aa(.(X, Xs), Ys) → U1_aa(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U1_aa(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_aa(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U2_aa(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_aa(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_aa(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_aa(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
app_in_aaa([], X, X) → app_out_aaa([], X, X)
app_in_aaa(.(X, Xs), Ys, .(X, Zs)) → U8_aaa(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
U8_aaa(X, Xs, Ys, Zs, app_out_aaa(Xs, Ys, Zs)) → app_out_aaa(.(X, Xs), Ys, .(X, Zs))
U4_aa(X, Xs, Ys, app_out_aaa(Ls, .(X, Bs), Ys)) → qs_out_aa(.(X, Xs), Ys)
U2_ag(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_ag(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_ag(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_ag(X, Xs, Ys, app_in_aag(Ls, .(X, Bs), Ys))
app_in_aag([], X, X) → app_out_aag([], X, X)
app_in_aag(.(X, Xs), Ys, .(X, Zs)) → U8_aag(X, Xs, Ys, Zs, app_in_aag(Xs, Ys, Zs))
U8_aag(X, Xs, Ys, Zs, app_out_aag(Xs, Ys, Zs)) → app_out_aag(.(X, Xs), Ys, .(X, Zs))
U4_ag(X, Xs, Ys, app_out_aag(Ls, .(X, Bs), Ys)) → qs_out_ag(.(X, Xs), Ys)
APP_IN_AAA(.(X, Xs), Ys, .(X, Zs)) → APP_IN_AAA(Xs, Ys, Zs)
APP_IN_AAA → APP_IN_AAA
LESS_IN_GA(s(X), s(Y)) → LESS_IN_GA(X, Y)
qs_in_ag([], []) → qs_out_ag([], [])
qs_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
part_in_aaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_aaaa(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
less_in_aa(0, s(X2)) → less_out_aa(0, s(X2))
less_in_aa(s(X), s(Y)) → U9_aa(X, Y, less_in_aa(X, Y))
U9_aa(X, Y, less_out_aa(X, Y)) → less_out_aa(s(X), s(Y))
U5_aaaa(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_aaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_gaaa(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
less_in_ga(0, s(X2)) → less_out_ga(0, s(X2))
less_in_ga(s(X), s(Y)) → U9_ga(X, Y, less_in_ga(X, Y))
U9_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U5_gaaa(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X1, [], [], []) → part_out_gaaa(X1, [], [], [])
U7_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U6_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), .(Y, Ls), Bs)
U6_aaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), .(Y, Ls), Bs)
part_in_aaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_aaaa(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
part_in_aaaa(X1, [], [], []) → part_out_aaaa(X1, [], [], [])
U7_aaaa(X, Y, Xs, Ls, Bs, part_out_aaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U1_ag(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_ag(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
qs_in_aa([], []) → qs_out_aa([], [])
qs_in_aa(.(X, Xs), Ys) → U1_aa(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U1_aa(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_aa(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U2_aa(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_aa(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_aa(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_aa(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
app_in_aaa([], X, X) → app_out_aaa([], X, X)
app_in_aaa(.(X, Xs), Ys, .(X, Zs)) → U8_aaa(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
U8_aaa(X, Xs, Ys, Zs, app_out_aaa(Xs, Ys, Zs)) → app_out_aaa(.(X, Xs), Ys, .(X, Zs))
U4_aa(X, Xs, Ys, app_out_aaa(Ls, .(X, Bs), Ys)) → qs_out_aa(.(X, Xs), Ys)
U2_ag(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_ag(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_ag(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_ag(X, Xs, Ys, app_in_aag(Ls, .(X, Bs), Ys))
app_in_aag([], X, X) → app_out_aag([], X, X)
app_in_aag(.(X, Xs), Ys, .(X, Zs)) → U8_aag(X, Xs, Ys, Zs, app_in_aag(Xs, Ys, Zs))
U8_aag(X, Xs, Ys, Zs, app_out_aag(Xs, Ys, Zs)) → app_out_aag(.(X, Xs), Ys, .(X, Zs))
U4_ag(X, Xs, Ys, app_out_aag(Ls, .(X, Bs), Ys)) → qs_out_ag(.(X, Xs), Ys)
LESS_IN_GA(s(X), s(Y)) → LESS_IN_GA(X, Y)
LESS_IN_GA(s(X)) → LESS_IN_GA(X)
From the DPs we obtained the following set of size-change graphs:
U5_GAAA(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → PART_IN_GAAA(X, Xs, Ls, Bs)
PART_IN_GAAA(X, .(Y, Xs), .(Y, Ls), Bs) → U5_GAAA(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
PART_IN_GAAA(X, .(Y, Xs), Ls, .(Y, Bs)) → PART_IN_GAAA(X, Xs, Ls, Bs)
qs_in_ag([], []) → qs_out_ag([], [])
qs_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
part_in_aaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_aaaa(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
less_in_aa(0, s(X2)) → less_out_aa(0, s(X2))
less_in_aa(s(X), s(Y)) → U9_aa(X, Y, less_in_aa(X, Y))
U9_aa(X, Y, less_out_aa(X, Y)) → less_out_aa(s(X), s(Y))
U5_aaaa(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_aaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_gaaa(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
less_in_ga(0, s(X2)) → less_out_ga(0, s(X2))
less_in_ga(s(X), s(Y)) → U9_ga(X, Y, less_in_ga(X, Y))
U9_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U5_gaaa(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X1, [], [], []) → part_out_gaaa(X1, [], [], [])
U7_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U6_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), .(Y, Ls), Bs)
U6_aaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), .(Y, Ls), Bs)
part_in_aaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_aaaa(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
part_in_aaaa(X1, [], [], []) → part_out_aaaa(X1, [], [], [])
U7_aaaa(X, Y, Xs, Ls, Bs, part_out_aaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U1_ag(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_ag(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
qs_in_aa([], []) → qs_out_aa([], [])
qs_in_aa(.(X, Xs), Ys) → U1_aa(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U1_aa(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_aa(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U2_aa(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_aa(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_aa(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_aa(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
app_in_aaa([], X, X) → app_out_aaa([], X, X)
app_in_aaa(.(X, Xs), Ys, .(X, Zs)) → U8_aaa(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
U8_aaa(X, Xs, Ys, Zs, app_out_aaa(Xs, Ys, Zs)) → app_out_aaa(.(X, Xs), Ys, .(X, Zs))
U4_aa(X, Xs, Ys, app_out_aaa(Ls, .(X, Bs), Ys)) → qs_out_aa(.(X, Xs), Ys)
U2_ag(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_ag(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_ag(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_ag(X, Xs, Ys, app_in_aag(Ls, .(X, Bs), Ys))
app_in_aag([], X, X) → app_out_aag([], X, X)
app_in_aag(.(X, Xs), Ys, .(X, Zs)) → U8_aag(X, Xs, Ys, Zs, app_in_aag(Xs, Ys, Zs))
U8_aag(X, Xs, Ys, Zs, app_out_aag(Xs, Ys, Zs)) → app_out_aag(.(X, Xs), Ys, .(X, Zs))
U4_ag(X, Xs, Ys, app_out_aag(Ls, .(X, Bs), Ys)) → qs_out_ag(.(X, Xs), Ys)
U5_GAAA(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → PART_IN_GAAA(X, Xs, Ls, Bs)
PART_IN_GAAA(X, .(Y, Xs), .(Y, Ls), Bs) → U5_GAAA(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
PART_IN_GAAA(X, .(Y, Xs), Ls, .(Y, Bs)) → PART_IN_GAAA(X, Xs, Ls, Bs)
less_in_ga(0, s(X2)) → less_out_ga(0, s(X2))
less_in_ga(s(X), s(Y)) → U9_ga(X, Y, less_in_ga(X, Y))
U9_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U5_GAAA(X, less_out_ga) → PART_IN_GAAA(X)
PART_IN_GAAA(X) → U5_GAAA(X, less_in_ga(X))
PART_IN_GAAA(X) → PART_IN_GAAA(X)
less_in_ga(0) → less_out_ga
less_in_ga(s(X)) → U9_ga(less_in_ga(X))
U9_ga(less_out_ga) → less_out_ga
less_in_ga(x0)
U9_ga(x0)
PART_IN_GAAA(0) → U5_GAAA(0, less_out_ga)
PART_IN_GAAA(s(x0)) → U5_GAAA(s(x0), U9_ga(less_in_ga(x0)))
U5_GAAA(X, less_out_ga) → PART_IN_GAAA(X)
PART_IN_GAAA(X) → PART_IN_GAAA(X)
PART_IN_GAAA(0) → U5_GAAA(0, less_out_ga)
PART_IN_GAAA(s(x0)) → U5_GAAA(s(x0), U9_ga(less_in_ga(x0)))
less_in_ga(0) → less_out_ga
less_in_ga(s(X)) → U9_ga(less_in_ga(X))
U9_ga(less_out_ga) → less_out_ga
less_in_ga(x0)
U9_ga(x0)
U5_GAAA(0, less_out_ga) → PART_IN_GAAA(0)
U5_GAAA(s(z0), less_out_ga) → PART_IN_GAAA(s(z0))
PART_IN_GAAA(X) → PART_IN_GAAA(X)
PART_IN_GAAA(0) → U5_GAAA(0, less_out_ga)
PART_IN_GAAA(s(x0)) → U5_GAAA(s(x0), U9_ga(less_in_ga(x0)))
U5_GAAA(0, less_out_ga) → PART_IN_GAAA(0)
U5_GAAA(s(z0), less_out_ga) → PART_IN_GAAA(s(z0))
less_in_ga(0) → less_out_ga
less_in_ga(s(X)) → U9_ga(less_in_ga(X))
U9_ga(less_out_ga) → less_out_ga
less_in_ga(x0)
U9_ga(x0)
LESS_IN_AA(s(X), s(Y)) → LESS_IN_AA(X, Y)
qs_in_ag([], []) → qs_out_ag([], [])
qs_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
part_in_aaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_aaaa(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
less_in_aa(0, s(X2)) → less_out_aa(0, s(X2))
less_in_aa(s(X), s(Y)) → U9_aa(X, Y, less_in_aa(X, Y))
U9_aa(X, Y, less_out_aa(X, Y)) → less_out_aa(s(X), s(Y))
U5_aaaa(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_aaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_gaaa(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
less_in_ga(0, s(X2)) → less_out_ga(0, s(X2))
less_in_ga(s(X), s(Y)) → U9_ga(X, Y, less_in_ga(X, Y))
U9_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U5_gaaa(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X1, [], [], []) → part_out_gaaa(X1, [], [], [])
U7_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U6_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), .(Y, Ls), Bs)
U6_aaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), .(Y, Ls), Bs)
part_in_aaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_aaaa(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
part_in_aaaa(X1, [], [], []) → part_out_aaaa(X1, [], [], [])
U7_aaaa(X, Y, Xs, Ls, Bs, part_out_aaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U1_ag(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_ag(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
qs_in_aa([], []) → qs_out_aa([], [])
qs_in_aa(.(X, Xs), Ys) → U1_aa(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U1_aa(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_aa(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U2_aa(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_aa(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_aa(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_aa(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
app_in_aaa([], X, X) → app_out_aaa([], X, X)
app_in_aaa(.(X, Xs), Ys, .(X, Zs)) → U8_aaa(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
U8_aaa(X, Xs, Ys, Zs, app_out_aaa(Xs, Ys, Zs)) → app_out_aaa(.(X, Xs), Ys, .(X, Zs))
U4_aa(X, Xs, Ys, app_out_aaa(Ls, .(X, Bs), Ys)) → qs_out_aa(.(X, Xs), Ys)
U2_ag(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_ag(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_ag(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_ag(X, Xs, Ys, app_in_aag(Ls, .(X, Bs), Ys))
app_in_aag([], X, X) → app_out_aag([], X, X)
app_in_aag(.(X, Xs), Ys, .(X, Zs)) → U8_aag(X, Xs, Ys, Zs, app_in_aag(Xs, Ys, Zs))
U8_aag(X, Xs, Ys, Zs, app_out_aag(Xs, Ys, Zs)) → app_out_aag(.(X, Xs), Ys, .(X, Zs))
U4_ag(X, Xs, Ys, app_out_aag(Ls, .(X, Bs), Ys)) → qs_out_ag(.(X, Xs), Ys)
LESS_IN_AA(s(X), s(Y)) → LESS_IN_AA(X, Y)
LESS_IN_AA → LESS_IN_AA
PART_IN_AAAA(X, .(Y, Xs), Ls, .(Y, Bs)) → PART_IN_AAAA(X, Xs, Ls, Bs)
qs_in_ag([], []) → qs_out_ag([], [])
qs_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
part_in_aaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_aaaa(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
less_in_aa(0, s(X2)) → less_out_aa(0, s(X2))
less_in_aa(s(X), s(Y)) → U9_aa(X, Y, less_in_aa(X, Y))
U9_aa(X, Y, less_out_aa(X, Y)) → less_out_aa(s(X), s(Y))
U5_aaaa(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_aaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_gaaa(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
less_in_ga(0, s(X2)) → less_out_ga(0, s(X2))
less_in_ga(s(X), s(Y)) → U9_ga(X, Y, less_in_ga(X, Y))
U9_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U5_gaaa(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X1, [], [], []) → part_out_gaaa(X1, [], [], [])
U7_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U6_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), .(Y, Ls), Bs)
U6_aaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), .(Y, Ls), Bs)
part_in_aaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_aaaa(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
part_in_aaaa(X1, [], [], []) → part_out_aaaa(X1, [], [], [])
U7_aaaa(X, Y, Xs, Ls, Bs, part_out_aaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U1_ag(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_ag(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
qs_in_aa([], []) → qs_out_aa([], [])
qs_in_aa(.(X, Xs), Ys) → U1_aa(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U1_aa(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_aa(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U2_aa(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_aa(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_aa(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_aa(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
app_in_aaa([], X, X) → app_out_aaa([], X, X)
app_in_aaa(.(X, Xs), Ys, .(X, Zs)) → U8_aaa(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
U8_aaa(X, Xs, Ys, Zs, app_out_aaa(Xs, Ys, Zs)) → app_out_aaa(.(X, Xs), Ys, .(X, Zs))
U4_aa(X, Xs, Ys, app_out_aaa(Ls, .(X, Bs), Ys)) → qs_out_aa(.(X, Xs), Ys)
U2_ag(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_ag(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_ag(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_ag(X, Xs, Ys, app_in_aag(Ls, .(X, Bs), Ys))
app_in_aag([], X, X) → app_out_aag([], X, X)
app_in_aag(.(X, Xs), Ys, .(X, Zs)) → U8_aag(X, Xs, Ys, Zs, app_in_aag(Xs, Ys, Zs))
U8_aag(X, Xs, Ys, Zs, app_out_aag(Xs, Ys, Zs)) → app_out_aag(.(X, Xs), Ys, .(X, Zs))
U4_ag(X, Xs, Ys, app_out_aag(Ls, .(X, Bs), Ys)) → qs_out_ag(.(X, Xs), Ys)
PART_IN_AAAA(X, .(Y, Xs), Ls, .(Y, Bs)) → PART_IN_AAAA(X, Xs, Ls, Bs)
PART_IN_AAAA → PART_IN_AAAA
QS_IN_AA(.(X, Xs), Ys) → U1_AA(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U1_AA(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_AA(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U2_AA(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → QS_IN_AA(Bigs, Bs)
U1_AA(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → QS_IN_AA(Littles, Ls)
qs_in_ag([], []) → qs_out_ag([], [])
qs_in_ag(.(X, Xs), Ys) → U1_ag(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
part_in_aaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_aaaa(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
less_in_aa(0, s(X2)) → less_out_aa(0, s(X2))
less_in_aa(s(X), s(Y)) → U9_aa(X, Y, less_in_aa(X, Y))
U9_aa(X, Y, less_out_aa(X, Y)) → less_out_aa(s(X), s(Y))
U5_aaaa(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_aaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_gaaa(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
less_in_ga(0, s(X2)) → less_out_ga(0, s(X2))
less_in_ga(s(X), s(Y)) → U9_ga(X, Y, less_in_ga(X, Y))
U9_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U5_gaaa(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X1, [], [], []) → part_out_gaaa(X1, [], [], [])
U7_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U6_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), .(Y, Ls), Bs)
U6_aaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), .(Y, Ls), Bs)
part_in_aaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_aaaa(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
part_in_aaaa(X1, [], [], []) → part_out_aaaa(X1, [], [], [])
U7_aaaa(X, Y, Xs, Ls, Bs, part_out_aaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U1_ag(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_ag(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
qs_in_aa([], []) → qs_out_aa([], [])
qs_in_aa(.(X, Xs), Ys) → U1_aa(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U1_aa(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_aa(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U2_aa(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_aa(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_aa(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_aa(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
app_in_aaa([], X, X) → app_out_aaa([], X, X)
app_in_aaa(.(X, Xs), Ys, .(X, Zs)) → U8_aaa(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
U8_aaa(X, Xs, Ys, Zs, app_out_aaa(Xs, Ys, Zs)) → app_out_aaa(.(X, Xs), Ys, .(X, Zs))
U4_aa(X, Xs, Ys, app_out_aaa(Ls, .(X, Bs), Ys)) → qs_out_aa(.(X, Xs), Ys)
U2_ag(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_ag(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U3_ag(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_ag(X, Xs, Ys, app_in_aag(Ls, .(X, Bs), Ys))
app_in_aag([], X, X) → app_out_aag([], X, X)
app_in_aag(.(X, Xs), Ys, .(X, Zs)) → U8_aag(X, Xs, Ys, Zs, app_in_aag(Xs, Ys, Zs))
U8_aag(X, Xs, Ys, Zs, app_out_aag(Xs, Ys, Zs)) → app_out_aag(.(X, Xs), Ys, .(X, Zs))
U4_ag(X, Xs, Ys, app_out_aag(Ls, .(X, Bs), Ys)) → qs_out_ag(.(X, Xs), Ys)
QS_IN_AA(.(X, Xs), Ys) → U1_AA(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U1_AA(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_AA(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
U2_AA(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → QS_IN_AA(Bigs, Bs)
U1_AA(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → QS_IN_AA(Littles, Ls)
part_in_aaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_aaaa(X, Y, Xs, Ls, Bs, less_in_aa(X, Y))
part_in_aaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_aaaa(X, Y, Xs, Ls, Bs, part_in_aaaa(X, Xs, Ls, Bs))
part_in_aaaa(X1, [], [], []) → part_out_aaaa(X1, [], [], [])
qs_in_aa([], []) → qs_out_aa([], [])
qs_in_aa(.(X, Xs), Ys) → U1_aa(X, Xs, Ys, part_in_aaaa(X, Xs, Littles, Bigs))
U5_aaaa(X, Y, Xs, Ls, Bs, less_out_aa(X, Y)) → U6_aaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
U7_aaaa(X, Y, Xs, Ls, Bs, part_out_aaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U1_aa(X, Xs, Ys, part_out_aaaa(X, Xs, Littles, Bigs)) → U2_aa(X, Xs, Ys, Bigs, qs_in_aa(Littles, Ls))
less_in_aa(0, s(X2)) → less_out_aa(0, s(X2))
less_in_aa(s(X), s(Y)) → U9_aa(X, Y, less_in_aa(X, Y))
U6_aaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_aaaa(X, .(Y, Xs), .(Y, Ls), Bs)
U2_aa(X, Xs, Ys, Bigs, qs_out_aa(Littles, Ls)) → U3_aa(X, Xs, Ys, Ls, qs_in_aa(Bigs, Bs))
U9_aa(X, Y, less_out_aa(X, Y)) → less_out_aa(s(X), s(Y))
part_in_gaaa(X, .(Y, Xs), .(Y, Ls), Bs) → U5_gaaa(X, Y, Xs, Ls, Bs, less_in_ga(X, Y))
part_in_gaaa(X, .(Y, Xs), Ls, .(Y, Bs)) → U7_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
part_in_gaaa(X1, [], [], []) → part_out_gaaa(X1, [], [], [])
U3_aa(X, Xs, Ys, Ls, qs_out_aa(Bigs, Bs)) → U4_aa(X, Xs, Ys, app_in_aaa(Ls, .(X, Bs), Ys))
U5_gaaa(X, Y, Xs, Ls, Bs, less_out_ga(X, Y)) → U6_gaaa(X, Y, Xs, Ls, Bs, part_in_gaaa(X, Xs, Ls, Bs))
U7_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), Ls, .(Y, Bs))
U4_aa(X, Xs, Ys, app_out_aaa(Ls, .(X, Bs), Ys)) → qs_out_aa(.(X, Xs), Ys)
less_in_ga(0, s(X2)) → less_out_ga(0, s(X2))
less_in_ga(s(X), s(Y)) → U9_ga(X, Y, less_in_ga(X, Y))
U6_gaaa(X, Y, Xs, Ls, Bs, part_out_gaaa(X, Xs, Ls, Bs)) → part_out_gaaa(X, .(Y, Xs), .(Y, Ls), Bs)
app_in_aaa([], X, X) → app_out_aaa([], X, X)
app_in_aaa(.(X, Xs), Ys, .(X, Zs)) → U8_aaa(X, Xs, Ys, Zs, app_in_aaa(Xs, Ys, Zs))
U9_ga(X, Y, less_out_ga(X, Y)) → less_out_ga(s(X), s(Y))
U8_aaa(X, Xs, Ys, Zs, app_out_aaa(Xs, Ys, Zs)) → app_out_aaa(.(X, Xs), Ys, .(X, Zs))
QS_IN_AA → U1_AA(part_in_aaaa)
U1_AA(part_out_aaaa) → U2_AA(qs_in_aa)
U2_AA(qs_out_aa) → QS_IN_AA
U1_AA(part_out_aaaa) → QS_IN_AA
part_in_aaaa → U5_aaaa(less_in_aa)
part_in_aaaa → U7_aaaa(part_in_aaaa)
part_in_aaaa → part_out_aaaa
qs_in_aa → qs_out_aa
qs_in_aa → U1_aa(part_in_aaaa)
U5_aaaa(less_out_aa(X)) → U6_aaaa(part_in_gaaa(X))
U7_aaaa(part_out_aaaa) → part_out_aaaa
U1_aa(part_out_aaaa) → U2_aa(qs_in_aa)
less_in_aa → less_out_aa(0)
less_in_aa → U9_aa(less_in_aa)
U6_aaaa(part_out_gaaa) → part_out_aaaa
U2_aa(qs_out_aa) → U3_aa(qs_in_aa)
U9_aa(less_out_aa(X)) → less_out_aa(s(X))
part_in_gaaa(X) → U5_gaaa(X, less_in_ga(X))
part_in_gaaa(X) → U7_gaaa(part_in_gaaa(X))
part_in_gaaa(X1) → part_out_gaaa
U3_aa(qs_out_aa) → U4_aa(app_in_aaa)
U5_gaaa(X, less_out_ga) → U6_gaaa(part_in_gaaa(X))
U7_gaaa(part_out_gaaa) → part_out_gaaa
U4_aa(app_out_aaa) → qs_out_aa
less_in_ga(0) → less_out_ga
less_in_ga(s(X)) → U9_ga(less_in_ga(X))
U6_gaaa(part_out_gaaa) → part_out_gaaa
app_in_aaa → app_out_aaa
app_in_aaa → U8_aaa(app_in_aaa)
U9_ga(less_out_ga) → less_out_ga
U8_aaa(app_out_aaa) → app_out_aaa
part_in_aaaa
qs_in_aa
U5_aaaa(x0)
U7_aaaa(x0)
U1_aa(x0)
less_in_aa
U6_aaaa(x0)
U2_aa(x0)
U9_aa(x0)
part_in_gaaa(x0)
U3_aa(x0)
U5_gaaa(x0, x1)
U7_gaaa(x0)
U4_aa(x0)
less_in_ga(x0)
U6_gaaa(x0)
app_in_aaa
U9_ga(x0)
U8_aaa(x0)
QS_IN_AA → U1_AA(U5_aaaa(less_in_aa))
QS_IN_AA → U1_AA(U7_aaaa(part_in_aaaa))
QS_IN_AA → U1_AA(part_out_aaaa)
U1_AA(part_out_aaaa) → U2_AA(qs_in_aa)
U2_AA(qs_out_aa) → QS_IN_AA
U1_AA(part_out_aaaa) → QS_IN_AA
QS_IN_AA → U1_AA(U5_aaaa(less_in_aa))
QS_IN_AA → U1_AA(U7_aaaa(part_in_aaaa))
QS_IN_AA → U1_AA(part_out_aaaa)
part_in_aaaa → U5_aaaa(less_in_aa)
part_in_aaaa → U7_aaaa(part_in_aaaa)
part_in_aaaa → part_out_aaaa
qs_in_aa → qs_out_aa
qs_in_aa → U1_aa(part_in_aaaa)
U5_aaaa(less_out_aa(X)) → U6_aaaa(part_in_gaaa(X))
U7_aaaa(part_out_aaaa) → part_out_aaaa
U1_aa(part_out_aaaa) → U2_aa(qs_in_aa)
less_in_aa → less_out_aa(0)
less_in_aa → U9_aa(less_in_aa)
U6_aaaa(part_out_gaaa) → part_out_aaaa
U2_aa(qs_out_aa) → U3_aa(qs_in_aa)
U9_aa(less_out_aa(X)) → less_out_aa(s(X))
part_in_gaaa(X) → U5_gaaa(X, less_in_ga(X))
part_in_gaaa(X) → U7_gaaa(part_in_gaaa(X))
part_in_gaaa(X1) → part_out_gaaa
U3_aa(qs_out_aa) → U4_aa(app_in_aaa)
U5_gaaa(X, less_out_ga) → U6_gaaa(part_in_gaaa(X))
U7_gaaa(part_out_gaaa) → part_out_gaaa
U4_aa(app_out_aaa) → qs_out_aa
less_in_ga(0) → less_out_ga
less_in_ga(s(X)) → U9_ga(less_in_ga(X))
U6_gaaa(part_out_gaaa) → part_out_gaaa
app_in_aaa → app_out_aaa
app_in_aaa → U8_aaa(app_in_aaa)
U9_ga(less_out_ga) → less_out_ga
U8_aaa(app_out_aaa) → app_out_aaa
part_in_aaaa
qs_in_aa
U5_aaaa(x0)
U7_aaaa(x0)
U1_aa(x0)
less_in_aa
U6_aaaa(x0)
U2_aa(x0)
U9_aa(x0)
part_in_gaaa(x0)
U3_aa(x0)
U5_gaaa(x0, x1)
U7_gaaa(x0)
U4_aa(x0)
less_in_ga(x0)
U6_gaaa(x0)
app_in_aaa
U9_ga(x0)
U8_aaa(x0)
U1_AA(part_out_aaaa) → U2_AA(qs_out_aa)
U1_AA(part_out_aaaa) → U2_AA(U1_aa(part_in_aaaa))
U2_AA(qs_out_aa) → QS_IN_AA
U1_AA(part_out_aaaa) → QS_IN_AA
QS_IN_AA → U1_AA(U5_aaaa(less_in_aa))
QS_IN_AA → U1_AA(U7_aaaa(part_in_aaaa))
QS_IN_AA → U1_AA(part_out_aaaa)
U1_AA(part_out_aaaa) → U2_AA(qs_out_aa)
U1_AA(part_out_aaaa) → U2_AA(U1_aa(part_in_aaaa))
part_in_aaaa → U5_aaaa(less_in_aa)
part_in_aaaa → U7_aaaa(part_in_aaaa)
part_in_aaaa → part_out_aaaa
qs_in_aa → qs_out_aa
qs_in_aa → U1_aa(part_in_aaaa)
U5_aaaa(less_out_aa(X)) → U6_aaaa(part_in_gaaa(X))
U7_aaaa(part_out_aaaa) → part_out_aaaa
U1_aa(part_out_aaaa) → U2_aa(qs_in_aa)
less_in_aa → less_out_aa(0)
less_in_aa → U9_aa(less_in_aa)
U6_aaaa(part_out_gaaa) → part_out_aaaa
U2_aa(qs_out_aa) → U3_aa(qs_in_aa)
U9_aa(less_out_aa(X)) → less_out_aa(s(X))
part_in_gaaa(X) → U5_gaaa(X, less_in_ga(X))
part_in_gaaa(X) → U7_gaaa(part_in_gaaa(X))
part_in_gaaa(X1) → part_out_gaaa
U3_aa(qs_out_aa) → U4_aa(app_in_aaa)
U5_gaaa(X, less_out_ga) → U6_gaaa(part_in_gaaa(X))
U7_gaaa(part_out_gaaa) → part_out_gaaa
U4_aa(app_out_aaa) → qs_out_aa
less_in_ga(0) → less_out_ga
less_in_ga(s(X)) → U9_ga(less_in_ga(X))
U6_gaaa(part_out_gaaa) → part_out_gaaa
app_in_aaa → app_out_aaa
app_in_aaa → U8_aaa(app_in_aaa)
U9_ga(less_out_ga) → less_out_ga
U8_aaa(app_out_aaa) → app_out_aaa
part_in_aaaa
qs_in_aa
U5_aaaa(x0)
U7_aaaa(x0)
U1_aa(x0)
less_in_aa
U6_aaaa(x0)
U2_aa(x0)
U9_aa(x0)
part_in_gaaa(x0)
U3_aa(x0)
U5_gaaa(x0, x1)
U7_gaaa(x0)
U4_aa(x0)
less_in_ga(x0)
U6_gaaa(x0)
app_in_aaa
U9_ga(x0)
U8_aaa(x0)