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 |
|
|