proof

0热度

1回答

常数的条件，我们定义大O记法如下：f(x) = O(g(x))如果有存在正的常数M和x0，从而f(x) <= M g(x)所有x > x0。我现在定义大O记法的新版本：f(x) = O'(g(x))如果有存在正的常数M'和x0' 这样f(x) <= M'g(x)所有x >= x0'（区别在于非严格不等式>=）。这两个定义是否相同？换句话说，如果f(x) = O(g(x))，必须它是f(x

2热度

1回答

精益证明助理中的交换环的幂等问题

嗨，我想在精益证明助手中做一些数学，看看它是如何工作的。我决定玩一个交换戒指的幂等物应该很有趣。下面是我的尝试： variables (A : Type) (R : comm_ring A) definition KR : Type := \Sigma x : A, x * x = x 然后我得到的错误 failed to synthesize placeholder A : Type,

1热度

1回答

以下算法是否稳定？

这个算法稳定与否？我检查了稳定的含义并在本网站上找到了一些东西。如果我理解正确，那么当两个具有相同键的事物在输入中以相同的顺序出现时，但在排序的输出中，也是稳定的（我们讨论排序算法）。下面的算法是众所周知的Bubblesort。我会说它是稳定的，因为我看不到2个相等的元素在那里交换，因此它必须是稳定的算法。我说得对吗？是否足够做“证明”？ Input: Array arr with n in

-1热度

2回答

质数的欧几里德引理

欧几里德的引理说如果p除以ab，那么p除a或p除b。如果是这种情况，那么p是素数。当p = 4，a = 8和b = 9时怎么办？ p |那么，（p | 8或p | 9）是真的。这推断p是素数。但4不是素数。我忽略了一些东西，我不确定它是什么。 a，b和p绝对没有限制，除了它们都是整数。任何帮助或提示将不胜感激。

1热度

1回答

g-sorted-ness不受以后的h-sorting影响：证明是否正确？

假设：数组A是g-sorted。即对于所有整数x和一个特定的整数克，A [X] < A [X + G] < A [X +2克] ... 现在，如果我们将其复制到数组乙h后排序，实现的条件：对于另一特定整数小时，B [X] < B [X + H] < B [X + 2H] ... 的假设是，经过H-排序它，阵列对于任意整数h和g仍然是g-sorted。证明如果与假设相反，h-sorting会影响g

1热度

1回答

从Z3（版本4）的无核心

去年我一直在使用Z3 4.0的Ocaml API，主要是bitvector理论。现在我需要在做一个Z3.solver_check之后提取不饱和核心，不幸的是版本4没有这个能力。我可以做一个重写来使用公式中的假设来代表公式中的每个位向量方程，然后得到不可靠的核心，但这是代码的关键部分，它可能会影响整体性能。有没有一种方法可以在不通过第4版假设的情况下获得不合格核心？长期的解决方案当然是转向最新版本

1热度

1回答

NFA是否有最终状态？

我试图证明所有的NFA都可以转换成一个最终状态，但我不知道如何/如果我必须处理0最终状态的情况。

0热度

2回答

所有最大独立集的一个matriid具有相同的基数

如何证明matriid的所有最大独立集具有相同的基数。提供的拟阵是一个2元组（M，j），其中M是一个有限集和J是家族的一些M的满足下述属性子集：如果A是A的子集，B属于J，则A属于J，如果A，B属于J，则| A | < = | B |，和x属于A - B，则存在ÿ属于乙 - A使得（BU {X}） - {Y}属于J. j的成员被称为独立组。

1热度

1回答

后缀树根边缘的证明

我想知道如何编写一个证据，证明后缀树中分支或根边的数量等于字符串S的字母大小。假设我们有S = {aaabaac} ，字母表= {a，b，c}，字母大小= 3，那么根边缘（或从根开始的分支）仅仅是3，即a，b和c。或者这可以通过定义来证明吗？我不确定！

1热度

1回答

如何使用等式推理来证明这个Haskell代码

我在Haskell的等式推理和证明中发现了这个练习。以下代码给出： type Stack = [Int] type Code = [Op] data Op = PUSH Int | ADD deriving (Show) -- -- Stack machine -- exec :: Code -> Stack -> Stack exec [ ] s = s exec (PUSH