proof

1热度

1回答

我已经试过证明乐趣bubble_main是有序的，但没有办法似乎工作。请问这里有人能帮我证明引理is_ordered (bubble_main L)。我刚刚删除了我以前的所有引理，因为似乎没有任何帮助Isabelle找到一个证明。这里是我的代码/理论：所有的 text{*check if the list is ordered ascendant*} fun is_sorted :: "na

0热度

1回答

悬而未决METAS在阿格达

限定记录时考虑下面的代码： module UnresolvedMeta where record Test (M : Set) : Set1 where field _≈_ : M -> M -> Set _⊕_ : M -> M -> M assoc⊕ : ∀ {r s t} -> ((r ⊕ s) ⊕ t) ≈ (r ⊕ (s ⊕ t

1热度

1回答

第III类型与/的rewrite脱糖

的背景是由按键有序的有限地图的数据类型，如本previous question提到： open import Function open import Relation.Binary renaming (IsEquivalence to IsEq) open import Relation.Binary.PropositionalEquality as P using (_≡_) modu

0热度

1回答

如果我们证明没有饥饿，我们不需要证明没有死锁或活锁（进展）？

我用Google搜索Peterson算法证明并注意到大多数网站不打扰证明进度要求，为什么？有人可以解释吗？

-1热度

2回答

怎么我的教授想出这个算法分析递归情况下？

我的教授给我们的递归算法如下解释寻找一组数字的排列：当他（T（M + 1），N -1））这是从哪里来的？为什么是m + 1和n-1？我真的很困惑，如该从何而来。

1热度

2回答

证明min-heap中的最大项目必须位于其中一个叶子上

如何证明min-heap中的最大项目必须位于具有N个项目的树中的某个叶子上？我明白一个最小堆的整体设计和I可以显示/图，其最大产品在叶子中的一个（在在精度N的深度N + 1>节点node）。我只是不确定如何格式化证明。

1热度

1回答

证明通过使用+2

我想知道是否通过诱导这种变异证明是正确的感应感应的证明标准规定，如果一个公式/算法，适用于N和可以证明它适用于N + 1那么你可以假设它适用于每个大于或等于n的整数。现在，如果你有2个基本情况（例如：2和3），并且你要证明它适用于n + 2，那么你可以说它适用于每个大于2的整数吗？，因为假设你能证明它的正确的N + 2， 2+2=4 3+2=5 4+2=6 等，让你覆盖每一个整数更大然

1热度

1回答

贝宝付款验证

您好，我的英语水平抱歉... 我已实施贝宝SDK为Android，它工作正常！但也许，我的英语我不明白我在这里做： @Override protected void onActivityResult (int requestCode, int resultCode, Intent data) { if (resultCode == Activity.RESULT_OK) {

1热度

2回答

证明/反驳BigO和BigTheta

我有问题完全理解如何证明以下某些语句。例如我有一个声明：n^2logn = O(n^2)。如果我错了，请纠正我，但是这表明n^2是n^2logn的bigO。这意味着n^2的增长速度快于n^2logn。现在我们将如何去证明这一点？我认为我需要通过我尝试使用的感应来使用证明，但是在这个过程中被卡住了。我能否重写这个声明为n^2logn <= n^2？是否有可能使用归纳来反证某些事物？例如，反驳n

0热度

1回答

关于主定理证明的问题

我正在读这本书CLRS（Introduction to Alglorithms，第3版），并发现在主定理的证明中似乎存在错误。在104页，以延长证明所有的整数，它使用一个不等式，这似乎是不正确的。在书上它说：我们的第一个目标是确定深度k，使nk是一个常数。使用不等式[X] < = X + 1，我们得到 [X]在这里是指x的天花板上，显而易见的是，[x] < x+1，不[x] <= x+1。此外