| 1317 |
2019/12/22 21:20:17
|
n < m \/ n = m \/ n > m
|
nmjr31 |
Success |
|
|
| 1316 |
2019/12/22 11:51:52
|
l1 <> l2 if l2 is an odd permutation of l1
|
fetburner |
Success |
|
|
| 1315 |
2019/12/22 09:05:44
|
Equivalent two quicksorts
|
fetburner |
Success |
|
|
| 1314 |
2019/12/22 08:58:19
|
Equivalent two quicksorts
|
fetburner |
Failure |
|
|
| 1313 |
2019/12/21 23:12:41
|
n * S m = n + n * m
|
nmjr31 |
Success |
|
|
| 1312 |
2019/12/21 22:48:32
|
forall f: bool -> bool, f^3(x) = f(x)
|
nmjr31 |
Success |
|
|
| 1311 |
2019/12/21 22:23:29
|
1 + 1 = 2
|
nmjr31 |
Success |
|
|
| 1310 |
2019/12/21 22:21:41
|
plus_comm
|
nmjr31 |
Success |
|
|
| 1309 |
2019/12/21 22:02:40
|
plus_assoc
|
nmjr31 |
Success |
|
|
| 1308 |
2019/12/21 22:00:49
|
plus_assoc
|
nmjr31 |
Failure |
|
|
| 1307 |
2019/12/21 16:31:58
|
n * S m = n + n * m
|
ry3s |
Success |
|
|
| 1306 |
2019/12/21 16:10:00
|
forall f: bool -> bool, f^3(x) = f(x)
|
ry3s |
Success |
|
|
| 1305 |
2019/12/21 15:58:36
|
1 + 1 = 2
|
ry3s |
Success |
|
|
| 1304 |
2019/12/21 15:55:31
|
plus_comm
|
ry3s |
Success |
|
|
| 1303 |
2019/12/21 15:33:37
|
plus_assoc
|
ry3s |
Success |
|
|
| 1302 |
2019/12/20 16:13:13
|
Uniqueness of inequality proofs
|
fetburner |
Success |
|
|
| 1301 |
2019/12/20 15:08:28
|
Binary search
|
fetburner |
Success |
|
|
| 1300 |
2019/12/20 14:02:28
|
Iterated iteration
|
fetburner |
Success |
|
|
| 1299 |
2019/12/20 12:01:04
|
Grand Garden
|
fetburner |
Success |
|
|
| 1298 |
2019/12/20 10:13:28
|
Sum of binomial coefficients
|
fetburner |
Success |
|
|
| 1297 |
2019/12/20 09:30:37
|
Tree addressing is injective
|
fetburner |
Success |
|
|
| 1296 |
2019/12/20 09:19:16
|
infinite bool sequence is uncountable
|
fetburner |
Success |
|
|
| 1295 |
2019/12/20 09:07:02
|
Double
|
fetburner |
Success |
|
|
| 1294 |
2019/12/19 20:19:06
|
Zero test
|
nekodesu |
Failure |
|
|
| 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 |
|
|