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 |
|