| 64 |
Eat the Candies
|
2020/09/27 20:00:00 |
3
|
Coq 8.11.1 |
Public |
|
| 63 |
Perfect Square?
|
2020/09/27 20:00:00 |
2
|
Coq 8.11.1 |
Public |
|
| 62 |
If zero were not nat
|
2020/09/27 20:00:00 |
2
|
Coq 8.11.1 |
Public |
|
| 61 |
Flat CPO
|
2020/09/27 20:00:00 |
1
|
Coq 8.11.1 |
Public |
|
| 60 |
Friends and strangers (corrected)
|
2020/08/17 00:40:00 |
3
|
Coq 8.11.1 |
Public |
|
| 59 |
Friends and strangers
|
2020/08/16 20:00:00 |
1
|
Coq 8.11.1 |
Public |
|
| 58 |
The set of all finite sequences of bool is countable
|
2020/08/16 20:00:00 |
2
|
Coq 8.11.1 |
Public |
|
| 57 |
Fibonacci numbers modulo 2
|
2020/08/16 20:00:00 |
2
|
Coq 8.11.1 |
Public |
|
| 56 |
Rotate once
|
2020/08/16 20:00:00 |
2
|
Coq 8.11.1 |
Public |
|
| 55 |
Sum of n^3
|
2020/08/16 20:00:00 |
1
|
Coq 8.11.1 |
Public |
|
| 54 |
Tree Syntax Unambiguity
|
2020/06/14 19:00:00 |
4
|
Coq 8.11.1 |
Public |
|
| 53 |
Tree Induction
|
2020/06/14 19:00:00 |
3
|
Coq 8.11.1 |
Public |
|
| 52 |
count_occ_app
|
2020/06/14 19:00:00 |
2
|
Coq 8.11.1 |
Public |
|
| 51 |
S preserves comparison
|
2020/06/14 19:00:00 |
1
|
Coq 8.11.1 |
Public |
|
| 50 |
Infinite duplication
|
2020/05/03 20:00:00 |
3
|
Coq 8.11.1 |
Public |
|
| 49 |
Upper triangular (completeness)
|
2020/05/03 20:00:00 |
2
|
Coq 8.11.1 |
Public |
|
| 48 |
Upper triangular (soundness)
|
2020/05/03 20:00:00 |
2
|
Coq 8.11.1 |
Public |
|
| 47 |
Drinker paradox?
|
2020/05/03 20:00:00 |
2
|
Coq 8.11.1 |
Public |
|
| 46 |
Swap twice
|
2020/05/03 20:00:00 |
1
|
Coq 8.11.1 |
Public |
|
| 45 |
Cycle detection
|
2020/03/15 20:00:00 |
4
|
Coq 8.11.1 |
Public |
|
| 44 |
Postorder traversal
|
2020/03/15 20:00:00 |
2
|
Coq 8.11.1 |
Public |
|
| 43 |
Not a sum of squares
|
2020/03/15 20:00:00 |
2
|
Coq 8.11.1 |
Public |
|
| 42 |
eq_sym?
|
2020/03/15 20:00:00 |
1
|
Coq 8.11.1 |
Public |
|
| 41 |
and_comm (Lean)
|
2020/02/05 03:15:00 |
1
|
Lean 3.4.2 |
Public |
|
| 40 |
Binary search
|
2019/12/08 20:00:00 |
3
|
Coq 8.11.1 |
Public |
|
| 39 |
Boolean-hole principle revisited
|
2019/12/08 20:00:00 |
2
|
Coq 8.11.1 |
Public |
|
| 38 |
Midpoint
|
2019/12/08 20:00:00 |
1
|
Coq 8.11.1 |
Public |
|
| 37 |
Zero test
|
2019/12/08 20:00:00 |
1
|
Coq 8.11.1 |
Public |
|
| 36 |
Relative prime squares
|
2019/11/24 20:00:00 |
3
|
Coq 8.11.1 |
Public |
|
| 35 |
infinite bool sequence is uncountable
|
2019/11/24 20:00:00 |
2
|
Coq 8.11.1 |
Public |
|
| 34 |
Tree addressing is injective
|
2019/11/24 20:00:00 |
2
|
Coq 8.11.1 |
Public |
|
| 33 |
Constructor is injective
|
2019/11/24 20:00:00 |
1
|
Coq 8.11.1 |
Public |
|
| 32 |
Uniqueness of inequality proofs
|
2019/10/26 18:00:00 |
4
|
Coq 8.11.1 |
Public |
|
| 31 |
Sum of binomial coefficients
|
2019/10/26 18:00:00 |
3
|
Coq 8.11.1 |
Public |
|
| 30 |
Double
|
2019/10/26 18:00:00 |
2
|
Coq 8.11.1 |
Public |
|
| 29 |
Yoneda embedding for preorder
|
2019/10/26 18:00:00 |
1
|
Coq 8.11.1 |
Public |
|
| 28 |
Iterated iteration
|
2019/10/06 20:00:00 |
3
|
Coq 8.11.1 |
Public |
|
| 27 |
Two is not Three
|
2019/10/06 20:00:00 |
2
|
Coq 8.11.1 |
Public |
|
| 26 |
Three is prime
|
2019/10/06 20:00:00 |
1
|
Coq 8.11.1 |
Public |
|
| 25 |
Boolean-hole principle
|
2019/10/06 20:00:00 |
1
|
Coq 8.11.1 |
Public |
|
| 24 |
Multiplication of non-zero value in F_p is injective
|
2019/09/22 20:00:00 |
3
|
Coq 8.11.1 |
Public |
|
| 23 |
Any natural number is expressible in binary notation
|
2019/09/22 20:00:00 |
2
|
Coq 8.11.1 |
Public |
|
| 22 |
De Morgan's laws in Coq
|
2019/09/22 20:00:00 |
1
|
Coq 8.11.1 |
Public |
|
| 21 |
mult_n_O
|
2019/09/22 20:00:00 |
1
|
Coq 8.11.1 |
Public |
|
| 20 |
Grand Garden
|
2019/09/15 17:00:00 |
3
|
Coq 8.11.1 |
Public |
|
| 19 |
unique count
|
2019/09/15 17:00:00 |
2
|
Coq 8.11.1 |
Public |
|
| 18 |
unique (unique l) = l
|
2019/09/15 17:00:00 |
2
|
Coq 8.11.1 |
Public |
|
| 17 |
count l n = count (rev l) n
|
2019/09/15 17:00:00 |
2
|
Coq 8.11.1 |
Public |
|
| 16 |
gcd(n, n+1) = 1
|
2019/09/15 17:00:00 |
1
|
Coq 8.11.1 |
Public |
|
| 15 |
Identity permutation
|
2019/09/08 20:00:00 |
3
|
Coq 8.11.1 |
Public |
|
| 14 |
Multiplication in F_2 is idempotent
|
2019/09/08 20:00:00 |
2
|
Coq 8.11.1 |
Public |
|
| 13 |
Definitions of injectivity
|
2019/09/08 20:00:00 |
2
|
Coq 8.11.1 |
Public |
|
| 12 |
Summand of one
|
2019/09/08 20:00:00 |
1
|
Coq 8.11.1 |
Public |
|
| 11 |
l1 <> l2 if l2 is an odd permutation of l1
|
2019/08/25 21:00:00 |
4
|
Coq 8.11.1 |
Public |
|
| 10 |
Cumulative sum of list
|
2019/08/25 21:00:00 |
2
|
Coq 8.11.1 |
Public |
|
| 9 |
forall l: list nat, l @ [0] <> []
|
2019/08/25 21:00:00 |
1
|
Coq 8.11.1 |
Public |
|
| 8 |
Equivalent two quicksorts
|
2019/08/18 16:00:00 |
4
|
Coq 8.11.1 |
Public |
|
| 7 |
Product of n consecutive integers is divisible by n!
|
2019/08/18 16:00:00 |
3
|
Coq 8.11.1 |
Public |
|
| 6 |
n < m \/ n = m \/ n > m
|
2019/08/18 16:00:00 |
2
|
Coq 8.11.1 |
Public |
|
| 5 |
n * S m = n + n * m
|
2019/08/18 16:00:00 |
1
|
Coq 8.11.1 |
Public |
|
| 4 |
forall f: bool -> bool, f^3(x) = f(x)
|
2019/08/18 16:00:00 |
1
|
Coq 8.11.1 |
Public |
|
| 3 |
1 + 1 = 2
|
2019/08/18 16:00:00 |
1
|
Coq 8.11.1 |
Public |
|
| 2 |
plus_comm
|
2019/08/03 09:00:00 |
1
|
Coq 8.11.1 |
Public |
|
| 1 |
plus_assoc
|
2019/08/03 09:00:00 |
1
|
Coq 8.11.1 |
Public |
|