| 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 |
|
|
| 1535 |
2020/05/08 19:29:47
|
Swap twice
|
cympfh |
Success |
|
|
| 1534 |
2020/05/08 19:29:11
|
Swap twice
|
cympfh |
Failure |
|
|
| 1533 |
2020/05/05 05:39:20
|
Cycle detection
|
aaa |
Success |
|
|
| 1532 |
2020/05/05 05:37:43
|
Cycle detection
|
aaa |
Failure |
|
|
| 1531 |
2020/05/05 02:23:06
|
Equivalent two quicksorts
|
yodvhskd |
Success |
|
|
| 1530 |
2020/05/05 02:18:06
|
Equivalent two quicksorts
|
yodvhskd |
Failure |
|
|
| 1529 |
2020/05/03 23:50:39
|
Upper triangular (soundness)
|
mttm |
Success |
|
|
| 1528 |
2020/05/03 23:39:22
|
Drinker paradox?
|
mttm |
Success |
|
|
| 1527 |
2020/05/03 21:51:34
|
Infinite duplication
|
kik |
Success |
|
|
| 1526 |
2020/05/03 21:49:17
|
Upper triangular (completeness)
|
natsugiri |
Success |
|
|
| 1525 |
2020/05/03 21:43:42
|
Infinite duplication
|
yodvhskd |
Success |
|
|
| 1524 |
2020/05/03 21:42:51
|
Infinite duplication
|
hirosegolf |
Failure |
|
|
| 1523 |
2020/05/03 21:02:03
|
Upper triangular (completeness)
|
tzik |
Success |
|
|
| 1522 |
2020/05/03 20:54:52
|
Upper triangular (completeness)
|
hirosegolf |
Success |
|
|
| 1521 |
2020/05/03 20:54:27
|
Upper triangular (soundness)
|
hirosegolf |
Failure |
|
|
| 1520 |
2020/05/03 20:41:38
|
Upper triangular (completeness)
|
kik |
Success |
|
|
| 1519 |
2020/05/03 20:41:08
|
Drinker paradox?
|
tzik |
Success |
|
|
| 1518 |
2020/05/03 20:32:54
|
Upper triangular (soundness)
|
hirosegolf |
Success |
|
|