proof
-
对数 T(n) = T(logn)+log(log(n)) 的递归
-
证明如果 G 的深度优先搜索树等于 G 的广度优先搜索树则 G 是树
-
Coq："lens is closed under composition" 的证明
-
渐近符号属性证明？
-
如何证明 SPARK.Text_IO 程序前提条件成立
-
函数具有负值时的大 O 表示法
-
上下文无关语言（泵引理 a^n b^m c^min(n,m)）
-
证明在 Agda 中 n 乘以一个偶数得到一个偶数
-
通过归纳法证明函数被调用 n-1 次
-
在编写作为传递链接步骤的长链的相等性证明时跟踪 "state"
-
我怎样才能让 Idris 自动证明两个值不相等？
-
用代入法解决递归
-
使用递归关系的算法时间复杂度
-
证明大 O 符号语句
-
证明展开的融合法则
-
证明自动化
-
重写简单的定理证明
-
证明程序的等价性
-
如何用Coq证明《Types and Programming Languages》定理3.5.4？
-
哪种编程语言具有测试并发算法的特定目的？