| 827 |
2019/10/05 10:20:49
|
count l n = count (rev l) n
|
hirosegolf |
Success |
|
|
| 826 |
2019/10/05 10:19:14
|
count l n = count (rev l) n
|
hirosegolf |
Failure |
|
|
| 825 |
2019/10/05 10:18:20
|
count l n = count (rev l) n
|
hirosegolf |
Failure |
|
|
| 824 |
2019/10/05 09:13:55
|
gcd(n, n+1) = 1
|
hirosegolf |
Success |
|
|
| 823 |
2019/10/05 01:58:21
|
Multiplication in F_2 is idempotent
|
hirosegolf |
Success |
|
|
| 822 |
2019/10/05 01:08:07
|
Definitions of injectivity
|
hirosegolf |
Success |
|
|
| 821 |
2019/10/05 01:06:07
|
Definitions of injectivity
|
hirosegolf |
Failure |
|
|
| 820 |
2019/10/05 00:49:38
|
Summand of one
|
hirosegolf |
Success |
|
|
| 819 |
2019/10/05 00:46:51
|
Cumulative sum of list
|
hirosegolf |
Success |
|
|
| 818 |
2019/10/04 23:51:04
|
forall l: list nat, l @ [0] <> []
|
hirosegolf |
Success |
|
|
| 817 |
2019/10/04 23:39:24
|
n < m \/ n = m \/ n > m
|
hirosegolf |
Success |
|
|
| 816 |
2019/10/04 23:37:00
|
n * S m = n + n * m
|
hirosegolf |
Success |
|
|
| 815 |
2019/10/04 23:32:23
|
forall f: bool -> bool, f^3(x) = f(x)
|
hirosegolf |
Success |
|
|
| 814 |
2019/10/04 23:17:23
|
1 + 1 = 2
|
hirosegolf |
Success |
|
|
| 813 |
2019/10/03 21:23:07
|
Iterated iteration
|
kozima |
Success |
|
|
| 812 |
2019/10/03 21:22:47
|
Two is not Three
|
kozima |
Success |
|
|
| 811 |
2019/10/03 21:22:23
|
Boolean-hole principle
|
kozima |
Success |
|
|
| 810 |
2019/10/03 21:22:11
|
Three is prime
|
kozima |
Success |
|
|
| 809 |
2019/10/03 21:20:52
|
Boolean-hole principle
|
kozima |
Failure |
|
|
| 808 |
2019/10/03 12:42:53
|
forall l: list nat, l @ [0] <> []
|
nikeya |
Success |
|
|
| 807 |
2019/10/03 12:20:28
|
mult_n_O
|
nikeya |
Success |
|
|
| 806 |
2019/10/03 12:18:21
|
De Morgan's laws in Coq
|
nikeya |
Success |
|
|
| 805 |
2019/10/02 18:16:50
|
1 + 1 = 2
|
nikeya |
Success |
|
|
| 804 |
2019/10/02 18:15:34
|
plus_comm
|
nikeya |
Success |
|
|
| 803 |
2019/10/02 18:14:45
|
plus_comm
|
nikeya |
Failure |
|
|
| 802 |
2019/10/02 17:24:14
|
plus_assoc
|
nikeya |
Success |
|
|
| 801 |
2019/10/01 02:53:35
|
plus_assoc
|
test |
Success |
|
|
| 800 |
2019/09/27 19:48:06
|
mult_n_O
|
yishibashi |
Success |
|
|
| 799 |
2019/09/27 19:21:56
|
n * S m = n + n * m
|
yishibashi |
Success |
|
|
| 798 |
2019/09/27 19:10:58
|
plus_comm
|
yishibashi |
Success |
|
|
| 797 |
2019/09/27 18:48:04
|
plus_assoc
|
yishibashi |
Success |
|
|
| 796 |
2019/09/27 18:24:22
|
Summand of one
|
yishibashi |
Success |
|
|
| 795 |
2019/09/26 13:40:51
|
unique (unique l) = l
|
coorde |
Success |
|
|
| 794 |
2019/09/26 13:38:55
|
unique (unique l) = l
|
coorde |
Failure |
|
|
| 793 |
2019/09/25 15:05:16
|
Any natural number is expressible in binary notation
|
kurgm |
Success |
|
|
| 792 |
2019/09/25 13:58:23
|
De Morgan's laws in Coq
|
kurgm |
Success |
|
|
| 791 |
2019/09/25 13:40:48
|
mult_n_O
|
kurgm |
Success |
|
|
| 790 |
2019/09/25 00:45:20
|
forall l: list nat, l @ [0] <> []
|
kkob |
Success |
|
|
| 789 |
2019/09/25 00:44:43
|
n < m \/ n = m \/ n > m
|
kkob |
Success |
|
|
| 788 |
2019/09/25 00:44:08
|
n * S m = n + n * m
|
kkob |
Success |
|
|
| 787 |
2019/09/25 00:42:54
|
forall f: bool -> bool, f^3(x) = f(x)
|
kkob |
Success |
|
|
| 786 |
2019/09/25 00:40:39
|
1 + 1 = 2
|
kkob |
Success |
|
|
| 785 |
2019/09/25 00:39:22
|
plus_comm
|
kkob |
Success |
|
|
| 784 |
2019/09/24 09:14:21
|
count l n = count (rev l) n
|
coorde |
Success |
|
|
| 783 |
2019/09/24 09:04:50
|
count l n = count (rev l) n
|
coorde |
Failure |
|
|
| 782 |
2019/09/24 08:48:07
|
gcd(n, n+1) = 1
|
coorde |
Success |
|
|
| 781 |
2019/09/23 14:52:40
|
forall f: bool -> bool, f^3(x) = f(x)
|
melan |
Success |
|
|
| 780 |
2019/09/23 12:55:30
|
De Morgan's laws in Coq
|
mkakh |
Success |
|
|
| 779 |
2019/09/23 04:26:51
|
Multiplication of non-zero value in F_p is injective
|
kkob |
Success |
|
|
| 778 |
2019/09/23 04:20:43
|
plus_assoc
|
kkob |
Success |
|
|