| 1163 |
2019/11/29 04:57:32
|
forall l: list nat, l @ [0] <> []
|
natsugiri |
Success |
|
|
| 1162 |
2019/11/29 02:18:37
|
plus_assoc
|
natsugiri |
Success |
|
|
| 1161 |
2019/11/28 22:33:57
|
Relative prime squares
|
tzik |
Success |
|
|
| 1160 |
2019/11/28 20:56:50
|
Multiplication of non-zero value in F_p is injective
|
CoiL |
Success |
|
|
| 1159 |
2019/11/28 20:38:33
|
Two is not Three
|
blue_jam |
Failure |
|
|
| 1158 |
2019/11/28 20:38:24
|
Summand of one
|
blue_jam |
Failure |
|
|
| 1157 |
2019/11/28 20:37:32
|
Two is not Three
|
nuip |
Failure |
|
|
| 1156 |
2019/11/28 20:37:29
|
Two is not Three
|
nekodesu |
Failure |
|
|
| 1155 |
2019/11/28 19:11:30
|
Double
|
natsugiri |
Success |
|
|
| 1154 |
2019/11/28 18:52:43
|
forall f: bool -> bool, f^3(x) = f(x)
|
cyan |
Success |
|
|
| 1153 |
2019/11/28 18:35:38
|
1 + 1 = 2
|
cyan |
Success |
|
|
| 1152 |
2019/11/28 18:33:54
|
plus_comm
|
cyan |
Success |
|
|
| 1151 |
2019/11/28 18:11:56
|
n < m \/ n = m \/ n > m
|
tanakh |
Success |
|
|
| 1150 |
2019/11/28 17:43:10
|
plus_assoc
|
cyan |
Success |
|
|
| 1149 |
2019/11/28 17:09:16
|
Three is prime
|
tanakh |
Success |
|
|
| 1148 |
2019/11/28 15:52:15
|
Uniqueness of inequality proofs
|
yodvhskd |
Success |
|
|
| 1147 |
2019/11/28 10:01:37
|
Multiplication of non-zero value in F_p is injective
|
tzik |
Success |
|
|
| 1146 |
2019/11/28 07:27:14
|
Iterated iteration
|
tzik |
Success |
|
|
| 1145 |
2019/11/28 03:22:36
|
unique (unique l) = l
|
natsugiri |
Success |
|
|
| 1144 |
2019/11/27 22:29:22
|
Multiplication in F_2 is idempotent
|
natsugiri |
Success |
|
|
| 1143 |
2019/11/27 22:29:09
|
Multiplication in F_2 is idempotent
|
natsugiri |
Failure |
|
|
| 1142 |
2019/11/27 20:52:25
|
Definitions of injectivity
|
natsugiri |
Success |
|
|
| 1141 |
2019/11/27 16:12:53
|
De Morgan's laws in Coq
|
tanakh |
Success |
|
|
| 1140 |
2019/11/27 16:12:00
|
De Morgan's laws in Coq
|
tanakh |
Rejected |
|
|
| 1139 |
2019/11/27 02:45:47
|
Cumulative sum of list
|
natsugiri |
Success |
|
|
| 1138 |
2019/11/27 01:37:47
|
Two is not Three
|
tzik |
Success |
|
|
| 1137 |
2019/11/27 01:37:14
|
Identity permutation
|
tzik |
Success |
|
|
| 1136 |
2019/11/26 23:46:59
|
n < m \/ n = m \/ n > m
|
natsugiri |
Success |
|
|
| 1135 |
2019/11/26 23:28:49
|
infinite bool sequence is uncountable
|
mttm |
Success |
|
|
| 1134 |
2019/11/26 22:57:57
|
Constructor is injective
|
natsugiri |
Success |
|
|
| 1133 |
2019/11/26 22:57:25
|
Constructor is injective
|
natsugiri |
Failure |
|
|
| 1132 |
2019/11/26 22:56:44
|
Constructor is injective
|
natsugiri |
Failure |
|
|
| 1131 |
2019/11/26 22:53:50
|
Yoneda embedding for preorder
|
natsugiri |
Success |
|
|
| 1130 |
2019/11/26 05:02:00
|
count l n = count (rev l) n
|
natsugiri |
Success |
|
|
| 1129 |
2019/11/26 03:18:29
|
Three is prime
|
natsugiri |
Success |
|
|
| 1128 |
2019/11/26 03:04:53
|
Relative prime squares
|
yodvhskd |
Success |
|
|
| 1127 |
2019/11/26 02:32:48
|
Boolean-hole principle
|
natsugiri |
Success |
|
|
| 1126 |
2019/11/26 02:28:31
|
De Morgan's laws in Coq
|
natsugiri |
Success |
|
|
| 1125 |
2019/11/26 02:28:03
|
De Morgan's laws in Coq
|
natsugiri |
Rejected |
|
|
| 1124 |
2019/11/26 01:30:34
|
mult_n_O
|
natsugiri |
Success |
|
|
| 1123 |
2019/11/26 01:29:01
|
gcd(n, n+1) = 1
|
natsugiri |
Success |
|
|
| 1122 |
2019/11/26 01:27:19
|
gcd(n, n+1) = 1
|
natsugiri |
Failure |
|
|
| 1121 |
2019/11/26 01:25:16
|
gcd(n, n+1) = 1
|
natsugiri |
Failure |
|
|
| 1120 |
2019/11/26 01:22:41
|
gcd(n, n+1) = 1
|
natsugiri |
Failure |
|
|
| 1119 |
2019/11/26 01:01:15
|
Summand of one
|
natsugiri |
Success |
|
|
| 1118 |
2019/11/26 00:08:57
|
Summand of one
|
saitou |
Success |
|
|
| 1117 |
2019/11/26 00:03:52
|
forall l: list nat, l @ [0] <> []
|
saitou |
Success |
|
|
| 1116 |
2019/11/25 04:46:29
|
unique (unique l) = l
|
tzik |
Success |
|
|
| 1115 |
2019/11/25 04:32:56
|
unique count
|
tzik |
Success |
|
|
| 1114 |
2019/11/25 03:31:31
|
Double
|
tzik |
Success |
|
|