還是錯

好不容易湊出一個新的 "nearly connected" preorder，最後關頭還是失敗了。再拖的話我的 JPEG decoder 會來不及生出來…

--
最討厭的就是這種「好像要出來又不肯出來」的狀況…

---

用 greedy theorem 重做 takeWhile 的 derivation，果然非常簡單。可是在 paper 裡面用這種問題當作 optimisation problem 的例子應該會被笑吧…

--
嗯，再撐一下 XD。

---

好啦，現在至少發現兩個互相拉扯的力量了。Monotonicity condition 要求新的 ordering 必須強一點，以便讓 implication 成立；greedy theorem 套用後，新的 algebra 要求 ordering 要弱一點，才能讓長的那一個勝出。只要找到平衡點，演算法就導出來啦。

--
天知有沒有那個平衡點… 而且之後用 Agda 證大概會瘋掉吧 XD。