也沒那麼差

昨天我以為我導的 partial greedy theorem 沒什麼用，今天再想想，其實還是可以只用這個定理而不用 inherently ordered lists 導出 activity-selection problem（CLRS 第 16 章的開場問題）的解。Specification 是

max ≤ℓ . Λ(mutex . subseq) . ordered

把 mutex . subseq 融成單一個 fold mutex-subseq 之後，可以用昨天證明的等式把 ordered 傳播到 Λ 裡面。再一次融合 mutex-subseq . ordered 成為 mutex-ordered-subseq，但這次只能得到

mutex-subseq . ordered  ⊆  mutex-ordered-subseq

而不是等式，因為給一個 unordered list 仍可能產出一個 ordered (and mutually-exclusive) subsequence。不過顯然 mutex-ordered-subseq ⊆ mutex-subseq，因此我們可以如下推導

  mutex-subseq . ordered
=   { coreflexives are "idempotent" }
  mutex-subseq . ordered . ordered
⊆   { fusion }
  mutex-ordered-subseq . ordered
⊆   { observation above }
  mutex-subseq . ordered

而完成精確的 fusion。Λ 裡贅餘的 ordered 同樣藉著昨天的等式可以被外面的 ordered 吸收。如此一來，partial monotonicity 裡面就會多出我們想要的條件了。整個過程基本上就對應 externalism 處理 ordered lists 的做法吧，看得出來挺麻煩的 XD。

定理本身的限制也很好丟掉，只要把 C-preserving 右邊多出來的 C 改成另一個 coreflexive D 就行了。然後定理本身可能會被拆成兩段吧。至於最後證不出來的 claim，逐點地看沒問題，我也特別用 AoPA 證了一次。當然我還是很希望可以有一個比較 AoP 的證明啦。

--
終究不是完全沒用的東西 XD。