| 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 |
|
|
| 1843 |
2020/11/07 18:06:57
|
forall f: bool -> bool, f^3(x) = f(x)
|
hiromi_mi |
Success |
|
|
| 1842 |
2020/11/07 17:52:43
|
1 + 1 = 2
|
hiromi_mi |
Success |
|
|
| 1841 |
2020/11/07 17:52:14
|
1 + 1 = 2
|
hiromi_mi |
Failure |
|
|
| 1840 |
2020/11/07 17:51:18
|
plus_comm
|
hiromi_mi |
Success |
|
|
| 1839 |
2020/11/07 17:48:50
|
plus_assoc
|
hiromi_mi |
Success |
|
|
| 1838 |
2020/11/03 16:51:47
|
Definitions of injectivity
|
aaaa |
Success |
|
|
| 1837 |
2020/11/03 16:48:17
|
Definitions of injectivity
|
aaaa |
Failure |
|
|
| 1836 |
2020/11/03 16:21:18
|
Definitions of injectivity
|
aaaa |
Rejected |
|
|
| 1835 |
2020/11/03 16:03:11
|
forall l: list nat, l @ [0] <> []
|
aaaa |
Success |
|
|
| 1834 |
2020/11/03 15:50:54
|
Two is not Three
|
aaaa |
Success |
|
|
| 1833 |
2020/11/03 15:46:19
|
Two is not Three
|
aaaa |
Success |
|
|
| 1832 |
2020/11/03 15:43:11
|
Boolean-hole principle
|
aaaa |
Success |
|
|
| 1831 |
2020/11/03 15:36:28
|
Boolean-hole principle
|
aaaa |
Success |
|
|
| 1830 |
2020/11/03 15:19:08
|
Two is not Three
|
aaaa |
Success |
|
|
| 1829 |
2020/11/03 13:51:07
|
1 + 1 = 2
|
aaaa |
Success |
|
|
| 1828 |
2020/11/03 13:47:20
|
n < m \/ n = m \/ n > m
|
aaaa |
Success |
|
|
| 1827 |
2020/11/03 12:03:14
|
Summand of one
|
aaaa |
Success |
|
|
| 1826 |
2020/11/03 11:46:37
|
n * S m = n + n * m
|
aaaa |
Success |
|
|
| 1825 |
2020/11/03 11:11:36
|
plus_assoc
|
aaaa |
Success |
|
|
| 1824 |
2020/11/03 11:00:10
|
plus_comm
|
aaaa |
Success |
|
|
| 1823 |
2020/11/02 23:20:02
|
1 + 1 = 2
|
aaaa |
Failure |
|
|
| 1822 |
2020/11/02 23:17:37
|
mult_n_O
|
aaaa |
Success |
|
|
| 1821 |
2020/11/02 23:08:20
|
mult_n_O
|
aaaa |
Success |
|
|
| 1820 |
2020/11/02 16:01:08
|
De Morgan's laws in Coq
|
aaaa |
Success |
|
|
| 1819 |
2020/11/02 06:29:56
|
1 + 1 = 2
|
aaaa |
Failure |
|
|
| 1818 |
2020/11/02 06:25:18
|
plus_comm
|
aaaa |
Success |
|
|