| 1293 |
2019/12/19 20:09:31
|
Boolean-hole principle revisited
|
nuip |
Failure |
|
|
| 1292 |
2019/12/19 20:03:05
|
Boolean-hole principle revisited
|
nekodesu |
Failure |
|
|
| 1291 |
2019/12/18 23:58:47
|
Boolean-hole principle revisited
|
fetburner |
Success |
|
|
| 1290 |
2019/12/18 23:54:11
|
Midpoint
|
fetburner |
Success |
|
|
| 1289 |
2019/12/18 23:23:05
|
Zero test
|
fetburner |
Success |
|
|
| 1288 |
2019/12/18 23:20:57
|
Constructor is injective
|
fetburner |
Success |
|
|
| 1287 |
2019/12/18 23:19:55
|
Yoneda embedding for preorder
|
fetburner |
Success |
|
|
| 1286 |
2019/12/18 23:06:13
|
Two is not Three
|
fetburner |
Success |
|
|
| 1285 |
2019/12/18 22:52:38
|
Three is prime
|
fetburner |
Success |
|
|
| 1284 |
2019/12/18 22:38:47
|
Boolean-hole principle
|
fetburner |
Success |
|
|
| 1283 |
2019/12/18 22:36:49
|
De Morgan's laws in Coq
|
fetburner |
Success |
|
|
| 1282 |
2019/12/18 22:32:35
|
Any natural number is expressible in binary notation
|
fetburner |
Success |
|
|
| 1281 |
2019/12/18 22:21:03
|
De Morgan's laws in Coq
|
fetburner |
Rejected |
|
|
| 1280 |
2019/12/18 22:08:28
|
mult_n_O
|
fetburner |
Success |
|
|
| 1279 |
2019/12/18 20:28:17
|
unique count
|
fetburner |
Success |
|
|
| 1278 |
2019/12/18 18:42:09
|
Tree addressing is injective
|
natsugiri |
Success |
|
|
| 1277 |
2019/12/18 16:07:16
|
count l n = count (rev l) n
|
fetburner |
Success |
|
|
| 1276 |
2019/12/18 15:36:37
|
unique (unique l) = l
|
fetburner |
Success |
|
|
| 1275 |
2019/12/18 15:35:25
|
unique count
|
fetburner |
Failure |
|
|
| 1274 |
2019/12/18 15:23:38
|
unique count
|
fetburner |
Failure |
|
|
| 1273 |
2019/12/18 14:54:21
|
gcd(n, n+1) = 1
|
fetburner |
Success |
|
|
| 1272 |
2019/12/18 14:34:59
|
Identity permutation
|
fetburner |
Success |
|
|
| 1271 |
2019/12/18 14:27:26
|
Multiplication in F_2 is idempotent
|
fetburner |
Success |
|
|
| 1270 |
2019/12/18 14:04:07
|
Summand of one
|
fetburner |
Success |
|
|
| 1269 |
2019/12/18 14:03:43
|
Definitions of injectivity
|
fetburner |
Success |
|
|
| 1268 |
2019/12/18 13:58:24
|
Summand of one
|
fetburner |
Failure |
|
|
| 1267 |
2019/12/18 13:55:14
|
Cumulative sum of list
|
fetburner |
Success |
|
|
| 1266 |
2019/12/18 13:39:04
|
forall l: list nat, l @ [0] <> []
|
fetburner |
Success |
|
|
| 1265 |
2019/12/17 02:12:58
|
Equivalent two quicksorts
|
tzik |
Success |
|
|
| 1264 |
2019/12/14 04:21:16
|
Product of n consecutive integers is divisible by n!
|
fetburner |
Success |
|
|
| 1263 |
2019/12/14 04:14:37
|
Product of n consecutive integers is divisible by n!
|
fetburner |
Success |
|
|
| 1262 |
2019/12/14 02:46:17
|
n < m \/ n = m \/ n > m
|
fetburner |
Success |
|
|
| 1261 |
2019/12/14 02:42:56
|
n * S m = n + n * m
|
fetburner |
Success |
|
|
| 1260 |
2019/12/14 02:39:35
|
forall f: bool -> bool, f^3(x) = f(x)
|
fetburner |
Success |
|
|
| 1259 |
2019/12/14 02:36:49
|
1 + 1 = 2
|
fetburner |
Success |
|
|
| 1258 |
2019/12/14 02:35:48
|
plus_comm
|
fetburner |
Success |
|
|
| 1257 |
2019/12/14 02:32:44
|
plus_assoc
|
fetburner |
Success |
|
|
| 1256 |
2019/12/12 23:11:45
|
Midpoint
|
natsugiri |
Success |
|
|
| 1255 |
2019/12/12 20:26:03
|
Zero test
|
CoiL |
Success |
|
|
| 1254 |
2019/12/12 20:11:40
|
Iterated iteration
|
CoiL |
Success |
|
|
| 1253 |
2019/12/12 19:33:10
|
Iterated iteration
|
CoiL |
Rejected |
|
|
| 1252 |
2019/12/10 21:38:47
|
Midpoint
|
maple |
Success |
|
|
| 1251 |
2019/12/10 18:14:22
|
Zero test
|
maple |
Success |
|
|
| 1250 |
2019/12/10 17:04:59
|
plus_comm
|
maple |
Success |
|
|
| 1249 |
2019/12/10 16:55:06
|
plus_assoc
|
maple |
Success |
|
|
| 1248 |
2019/12/10 12:54:47
|
Iterated iteration
|
chy |
Success |
|
|
| 1247 |
2019/12/10 12:54:04
|
Iterated iteration
|
chy |
Failure |
|
|
| 1246 |
2019/12/10 03:08:26
|
Binary search
|
tzik |
Success |
|
|
| 1245 |
2019/12/09 23:48:52
|
Midpoint
|
tzik |
Success |
|
|
| 1244 |
2019/12/09 21:09:15
|
Boolean-hole principle revisited
|
natsugiri |
Success |
|
|