| 1585 |
2020/06/14 19:21:38
|
count_occ_app
|
natsugiri |
Success |
|
|
| 1584 |
2020/06/14 19:21:37
|
S preserves comparison
|
efk |
Success |
|
|
| 1583 |
2020/06/14 19:18:13
|
Tree Induction
|
kozima |
Success |
|
|
| 1582 |
2020/06/14 19:15:31
|
count_occ_app
|
tanakh |
Success |
|
|
| 1581 |
2020/06/14 19:15:10
|
count_occ_app
|
kik |
Success |
|
|
| 1580 |
2020/06/14 19:09:23
|
count_occ_app
|
kozima |
Success |
|
|
| 1579 |
2020/06/14 19:07:49
|
S preserves comparison
|
kik |
Success |
|
|
| 1578 |
2020/06/14 19:06:38
|
count_occ_app
|
yodvhskd |
Success |
|
|
| 1577 |
2020/06/14 19:05:53
|
count_occ_app
|
sorata |
Success |
|
|
| 1576 |
2020/06/14 19:05:47
|
S preserves comparison
|
tanakh |
Success |
|
|
| 1575 |
2020/06/14 19:05:15
|
S preserves comparison
|
natsugiri |
Success |
|
|
| 1574 |
2020/06/14 19:04:13
|
S preserves comparison
|
natsugiri |
Failure |
|
|
| 1573 |
2020/06/14 19:03:58
|
S preserves comparison
|
kano |
Success |
|
|
| 1572 |
2020/06/14 19:03:48
|
S preserves comparison
|
yodvhskd |
Success |
|
|
| 1571 |
2020/06/14 19:02:11
|
S preserves comparison
|
kozima |
Success |
|
|
| 1570 |
2020/06/14 19:01:35
|
S preserves comparison
|
sorata |
Success |
|
|
| 1569 |
2020/06/14 18:55:43
|
Boolean-hole principle
|
kano |
Success |
|
|
| 1568 |
2020/06/13 15:34:20
|
Tree Induction
|
kkob |
Success |
|
|
| 1567 |
2020/06/13 15:29:21
|
Tree Induction
|
kkob |
Success |
|
|
| 1566 |
2020/06/11 17:29:01
|
S preserves comparison
|
kkob |
Success |
|
|
| 1565 |
2020/06/09 20:09:15
|
n < m \/ n = m \/ n > m
|
hammer |
Success |
|
|
| 1564 |
2020/06/09 18:33:49
|
n * S m = n + n * m
|
hammer |
Success |
|
|
| 1563 |
2020/06/09 18:11:23
|
forall f: bool -> bool, f^3(x) = f(x)
|
hammer |
Success |
|
|
| 1562 |
2020/06/09 17:33:07
|
1 + 1 = 2
|
hammer |
Success |
|
|
| 1561 |
2020/06/09 17:31:47
|
plus_comm
|
hammer |
Success |
|
|
| 1560 |
2020/06/09 17:01:10
|
plus_assoc
|
hammer |
Success |
|
|
| 1559 |
2020/06/09 16:58:24
|
plus_assoc
|
hammer |
Failure |
|
|
| 1558 |
2020/06/08 00:38:06
|
count_occ_app
|
kkob |
Success |
|
|
| 1557 |
2020/06/08 00:37:28
|
Tree Syntax Unambiguity
|
kkob |
Success |
|
|
| 1556 |
2020/06/08 00:17:20
|
Tree Induction
|
kkob |
Success |
|
|
| 1555 |
2020/06/04 01:33:54
|
De Morgan's laws in Coq
|
kano |
Success |
|
|
| 1554 |
2020/06/04 00:43:28
|
gcd(n, n+1) = 1
|
kano |
Success |
|
|
| 1553 |
2020/06/04 00:32:25
|
gcd(n, n+1) = 1
|
kano |
Failure |
|
|
| 1552 |
2020/06/04 00:20:54
|
forall l: list nat, l @ [0] <> []
|
kano |
Success |
|
|
| 1551 |
2020/06/04 00:15:54
|
Summand of one
|
kano |
Success |
|
|
| 1550 |
2020/05/28 10:38:02
|
1 + 1 = 2
|
Tqk |
Success |
|
|
| 1549 |
2020/05/21 20:39:56
|
Yoneda embedding for preorder
|
efk |
Success |
|
|
| 1548 |
2020/05/21 20:08:57
|
Swap twice
|
kkob |
Rejected |
|
|
| 1547 |
2020/05/21 19:33:02
|
Boolean-hole principle
|
efk |
Success |
|
|
| 1546 |
2020/05/20 20:26:35
|
plus_assoc
|
aaa |
Success |
|
|
| 1545 |
2020/05/20 20:26:01
|
plus_assoc
|
aaa |
Failure |
|
|
| 1544 |
2020/05/20 13:36:38
|
Boolean-hole principle
|
cympfh |
Success |
|
|
| 1543 |
2020/05/13 02:21:51
|
eq_sym?
|
cympfh |
Success |
|
|
| 1542 |
2020/05/10 19:34:47
|
eq_sym?
|
kano |
Success |
|
|
| 1541 |
2020/05/10 19:23:22
|
mult_n_O
|
kano |
Success |
|
|
| 1540 |
2020/05/10 19:20:34
|
n * S m = n + n * m
|
kano |
Success |
|
|
| 1539 |
2020/05/10 18:51:45
|
forall f: bool -> bool, f^3(x) = f(x)
|
kano |
Success |
|
|
| 1538 |
2020/05/10 18:40:39
|
1 + 1 = 2
|
kano |
Success |
|
|
| 1537 |
2020/05/10 18:39:40
|
plus_comm
|
kano |
Success |
|
|
| 1536 |
2020/05/08 23:40:34
|
Infinite duplication
|
tzik |
Success |
|
|