| 1943 |
2022/07/18 21:02:43
|
forall f: bool -> bool, f^3(x) = f(x)
|
platypus |
Success |
|
|
| 1942 |
2022/06/23 17:54:09
|
mult_n_O
|
toga |
Success |
|
|
| 1941 |
2022/06/23 13:54:12
|
plus_assoc
|
nikosai |
Failure |
|
|
| 1940 |
2022/06/23 13:12:05
|
gcd(n, n+1) = 1
|
toga |
Success |
|
|
| 1939 |
2022/06/22 14:15:44
|
forall l: list nat, l @ [0] <> []
|
toga |
Success |
|
|
| 1938 |
2022/06/22 14:01:02
|
forall f: bool -> bool, f^3(x) = f(x)
|
toga |
Success |
|
|
| 1937 |
2022/06/21 14:28:39
|
Summand of one
|
toga |
Success |
|
|
| 1936 |
2022/06/15 16:06:22
|
n * S m = n + n * m
|
toga |
Success |
|
|
| 1935 |
2022/06/14 12:26:41
|
plus_comm
|
toga |
Success |
|
|
| 1934 |
2022/06/13 19:51:17
|
plus_comm
|
toga |
Success |
|
|
| 1933 |
2022/06/13 18:39:02
|
1 + 1 = 2
|
toga |
Success |
|
|
| 1932 |
2022/06/11 17:58:25
|
plus_assoc
|
toga |
Success |
|
|
| 1931 |
2022/04/20 04:08:08
|
count_occ_app
|
minus3theta |
Success |
|
|
| 1930 |
2022/04/19 06:42:20
|
Flat CPO
|
minus3theta |
Success |
|
|
| 1929 |
2022/04/19 05:57:43
|
Swap twice
|
minus3theta |
Success |
|
|
| 1928 |
2022/04/19 05:56:05
|
S preserves comparison
|
minus3theta |
Success |
|
|
| 1927 |
2022/04/19 05:54:18
|
Sum of n^3
|
minus3theta |
Success |
|
|
| 1926 |
2022/04/19 05:48:38
|
Boolean-hole principle revisited
|
minus3theta |
Success |
|
|
| 1925 |
2022/04/19 05:37:35
|
Cumulative sum of list
|
minus3theta |
Success |
|
|
| 1924 |
2022/04/19 05:02:26
|
Zero test
|
minus3theta |
Success |
|
|
| 1923 |
2022/04/19 05:00:07
|
eq_sym?
|
minus3theta |
Success |
|
|
| 1922 |
2022/04/11 17:42:24
|
Zero test
|
minus3theta |
Failure |
|
|
| 1921 |
2022/04/11 15:49:29
|
Double
|
minus3theta |
Success |
|
|
| 1920 |
2022/04/11 15:21:22
|
Yoneda embedding for preorder
|
minus3theta |
Success |
|
|
| 1919 |
2022/04/11 15:20:37
|
Yoneda embedding for preorder
|
minus3theta |
Failure |
|
|
| 1918 |
2022/04/11 14:25:45
|
unique (unique l) = l
|
minus3theta |
Success |
|
|
| 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 |
|
|