| 1917 |
2022/04/10 02:57:17
|
Boolean-hole principle
|
minus3theta |
Success |
|
|
| 1916 |
2022/04/10 00:57:00
|
De Morgan's laws in Coq
|
minus3theta |
Success |
|
|
| 1915 |
2022/04/10 00:48:01
|
mult_n_O
|
minus3theta |
Success |
|
|
| 1914 |
2022/04/09 00:59:02
|
count l n = count (rev l) n
|
minus3theta |
Failure |
|
|
| 1913 |
2022/04/08 21:12:55
|
gcd(n, n+1) = 1
|
minus3theta |
Success |
|
|
| 1912 |
2022/04/08 21:11:47
|
gcd(n, n+1) = 1
|
minus3theta |
Failure |
|
|
| 1911 |
2022/04/08 20:53:14
|
Identity permutation
|
minus3theta |
Success |
|
|
| 1910 |
2022/04/08 18:26:29
|
Multiplication in F_2 is idempotent
|
minus3theta |
Success |
|
|
| 1909 |
2022/04/08 17:19:30
|
Definitions of injectivity
|
minus3theta |
Success |
|
|
| 1908 |
2022/04/08 16:06:22
|
Definitions of injectivity
|
minus3theta |
Rejected |
|
|
| 1907 |
2022/04/08 12:45:09
|
Summand of one
|
minus3theta |
Success |
|
|
| 1906 |
2022/04/08 12:44:34
|
Summand of one
|
minus3theta |
Failure |
|
|
| 1905 |
2022/04/08 12:43:42
|
Summand of one
|
minus3theta |
Failure |
|
|
| 1904 |
2022/01/30 22:09:07
|
Summand of one
|
myazakky |
Success |
|
|
| 1903 |
2022/01/30 21:59:58
|
plus_comm
|
myazakky |
Success |
|
|
| 1902 |
2022/01/30 21:54:31
|
plus_assoc
|
myazakky |
Success |
|
|
| 1901 |
2022/01/10 18:23:46
|
plus_assoc
|
magurofly |
Success |
|
|
| 1900 |
2021/09/18 22:03:19
|
1 + 1 = 2
|
jambo |
Success |
|
|
| 1899 |
2021/09/18 22:02:46
|
1 + 1 = 2
|
jambo |
Failure |
|
|
| 1898 |
2021/09/17 12:28:24
|
1 + 1 = 2
|
platypus |
Success |
|
|
| 1897 |
2021/09/17 12:27:25
|
plus_comm
|
platypus |
Success |
|
|
| 1896 |
2021/09/17 12:26:50
|
plus_comm
|
platypus |
Failure |
|
|
| 1895 |
2021/09/17 12:25:14
|
plus_comm
|
platypus |
Failure |
|
|
| 1894 |
2021/09/17 11:45:38
|
plus_assoc
|
platypus |
Success |
|
|
| 1893 |
2021/09/15 03:02:43
|
n * S m = n + n * m
|
TanakaTaroh |
Success |
|
|
| 1892 |
2021/09/15 03:02:12
|
n * S m = n + n * m
|
TanakaTaroh |
Failure |
|
|
| 1891 |
2021/09/15 02:34:40
|
forall f: bool -> bool, f^3(x) = f(x)
|
TanakaTaroh |
Success |
|
|
| 1890 |
2021/09/14 18:43:13
|
1 + 1 = 2
|
TanakaTaroh |
Success |
|
|
| 1889 |
2021/09/14 18:36:34
|
plus_comm
|
TanakaTaroh |
Success |
|
|
| 1888 |
2021/09/13 04:34:22
|
plus_assoc
|
TanakaTaroh |
Success |
|
|
| 1887 |
2021/04/29 19:05:18
|
Friends and strangers
|
pyusuke |
Success |
|
|
| 1886 |
2021/04/29 18:56:28
|
Flat CPO
|
pyusuke |
Success |
|
|
| 1885 |
2021/04/10 11:54:41
|
n < m \/ n = m \/ n > m
|
sash0 |
Success |
|
|
| 1884 |
2021/04/10 00:07:43
|
plus_comm
|
sash0 |
Success |
|
|
| 1883 |
2021/04/09 23:49:52
|
plus_assoc
|
sash0 |
Success |
|
|
| 1882 |
2021/03/19 11:38:30
|
1 + 1 = 2
|
jeb |
Success |
|
|
| 1881 |
2021/02/20 13:34:52
|
Definitions of injectivity
|
matonix |
Success |
|
|
| 1880 |
2021/02/17 00:53:46
|
Summand of one
|
matonix |
Success |
|
|
| 1879 |
2021/02/15 01:36:56
|
Cumulative sum of list
|
matonix |
Success |
|
|
| 1878 |
2021/02/10 01:12:35
|
forall l: list nat, l @ [0] <> []
|
matonix |
Success |
|
|
| 1877 |
2021/02/08 23:16:38
|
Product of n consecutive integers is divisible by n!
|
matonix |
Success |
|
|
| 1876 |
2021/01/15 01:54:09
|
n < m \/ n = m \/ n > m
|
matonix |
Success |
|
|
| 1875 |
2021/01/13 01:39:58
|
n * S m = n + n * m
|
matonix |
Success |
|
|
| 1874 |
2021/01/12 01:00:16
|
forall f: bool -> bool, f^3(x) = f(x)
|
matonix |
Success |
|
|
| 1873 |
2021/01/12 00:22:20
|
1 + 1 = 2
|
matonix |
Success |
|
|
| 1872 |
2021/01/10 20:09:34
|
plus_comm
|
matonix |
Success |
|
|
| 1871 |
2021/01/08 01:58:25
|
plus_assoc
|
matonix |
Success |
|
|
| 1870 |
2021/01/08 01:57:17
|
plus_assoc
|
matonix |
Failure |
|
|
| 1869 |
2020/11/29 18:28:54
|
Definitions of injectivity
|
pyusuke |
Success |
|
|
| 1868 |
2020/11/29 18:28:25
|
Definitions of injectivity
|
pyusuke |
Failure |
|
|