程序验证（六）：纳尔逊-欧朋算法(Nelson-Oppen Procedure) 动机 截至目前，我们学习了一些一阶理论，每一个都是关于某一种数据类型 然而，现实中的公式并不是由单一的理论组成，如： ∀ i . 0 ≤ i ≤ n → a [ i ] ≤ a [ i + 1 ] \forall i.0\le i\le n\to a[i]\le a[i+1] ∀i.0≤i≤n→a[i]≤a[i