Actually, there is an even simpler formulation of this. If you want to find a subset S that, which when moved to the front is not incompatible with reaching the cumulative size/fee point corresponding to each set of transactions P = \{p_1, p_2, \ldots, p_n\}, then S needs to have a feerate at least as high as every p_i, and no intersection S \cap p_i can have a higher feerate.
In the case of Double LIMO, P consists of all prefixes of chunks of L, plus S_1 and S_2.
The LIMO theorem:
Given a set P = \{p_1, p_2, \ldots, p_n\} of topological subsets of transactions of a graph G, a topological subset S of transactions of G, and a linearization L_S for S such that:
- For all i, \operatorname{feerate}(S) \geq \operatorname{feerate}(p_i)
- For all i, \operatorname{feerate}(S) \geq \operatorname{feerate}(S \cap p_i) or S \cap p_i = \varnothing
Then there always exists a linearization L of G for which:
- L_S is a prefix of L
- For all i, \operatorname{diag}_L(\operatorname{size}(p_i)) \geq \operatorname{fee}(p_i)
Such an S necessarily exists, e.g. the highest-feerate subset of all combinations of intersections between the p_i sets, though more efficient approaches exist.
EDIT: expanded on these ideas more in Cluster mempool definitions & theory - #14 by sipa.