| 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 |
|
|
| 1867 |
2020/11/29 17:53:06
|
Zero test
|
pyusuke |
Success |
|
|
| 1866 |
2020/11/29 17:26:45
|
Constructor is injective
|
pyusuke |
Success |
|
|
| 1865 |
2020/11/29 17:26:19
|
Constructor is injective
|
pyusuke |
Failure |
|
|
| 1864 |
2020/11/29 17:21:01
|
Yoneda embedding for preorder
|
pyusuke |
Success |
|
|
| 1863 |
2020/11/29 17:20:27
|
Yoneda embedding for preorder
|
pyusuke |
Failure |
|
|
| 1862 |
2020/11/29 17:19:04
|
Yoneda embedding for preorder
|
pyusuke |
Failure |
|
|
| 1861 |
2020/11/29 17:11:04
|
De Morgan's laws in Coq
|
pyusuke |
Success |
|
|
| 1860 |
2020/11/29 16:47:45
|
mult_n_O
|
pyusuke |
Success |
|
|
| 1859 |
2020/11/29 16:38:45
|
Three is prime
|
pyusuke |
Success |
|
|
| 1858 |
2020/11/29 15:52:21
|
Boolean-hole principle
|
pyusuke |
Success |
|
|
| 1857 |
2020/11/29 15:51:27
|
Summand of one
|
pyusuke |
Failure |
|
|
| 1856 |
2020/11/29 13:13:21
|
forall l: list nat, l @ [0] <> []
|
pyusuke |
Success |
|
|
| 1855 |
2020/11/28 17:55:41
|
plus_comm
|
pyusuke |
Success |
|
|
| 1854 |
2020/11/28 17:55:08
|
plus_comm
|
pyusuke |
Failure |
|
|
| 1853 |
2020/11/28 17:53:26
|
plus_assoc
|
pyusuke |
Success |
|
|
| 1852 |
2020/11/28 17:31:23
|
forall f: bool -> bool, f^3(x) = f(x)
|
pyusuke |
Success |
|
|
| 1851 |
2020/11/28 16:54:16
|
forall f: bool -> bool, f^3(x) = f(x)
|
pyusuke |
Success |
|
|
| 1850 |
2020/11/28 16:29:37
|
1 + 1 = 2
|
pyusuke |
Success |
|
|
| 1849 |
2020/11/28 16:25:34
|
n * S m = n + n * m
|
pyusuke |
Success |
|
|
| 1848 |
2020/11/28 15:59:55
|
1 + 1 = 2
|
pyusuke |
Success |
|
|
| 1847 |
2020/11/07 19:23:19
|
Summand of one
|
hiromi_mi |
Success |
|
|
| 1846 |
2020/11/07 18:30:25
|
forall l: list nat, l @ [0] <> []
|
hiromi_mi |
Success |
|
|
| 1845 |
2020/11/07 18:10:14
|
n < m \/ n = m \/ n > m
|
hiromi_mi |
Success |
|
|
| 1844 |
2020/11/07 18:08:18
|
n * S m = n + n * m
|
hiromi_mi |
Success |
|
|