| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (968 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (799 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (141 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |
Global Index
A
agree [definition, in Kolmogorov.preliminaries]agree_trans [lemma, in Kolmogorov.preliminaries]
agree_ref [lemma, in Kolmogorov.preliminaries]
a:144 [binder, in Kolmogorov.random_lower_bound]
a:147 [binder, in Kolmogorov.random_lower_bound]
A:154 [binder, in Kolmogorov.listFacts]
A:159 [binder, in Kolmogorov.listFacts]
A:2 [binder, in Kolmogorov.listFacts]
A:26 [binder, in Kolmogorov.uncomputability]
A:29 [binder, in Kolmogorov.uncomputability]
A:41 [binder, in Kolmogorov.listFacts]
a:50 [binder, in Kolmogorov.preliminaries]
a:63 [binder, in Kolmogorov.binaryEncoding]
a:70 [binder, in Kolmogorov.binaryEncoding]
B
binaryEncoding [library]B:3 [binder, in Kolmogorov.listFacts]
B:42 [binder, in Kolmogorov.listFacts]
b:64 [binder, in Kolmogorov.binaryEncoding]
b:71 [binder, in Kolmogorov.binaryEncoding]
C
constructive_least_witness [lemma, in Kolmogorov.preliminaries]CT [axiom, in Kolmogorov.preliminaries]
c':27 [binder, in Kolmogorov.kolmogorov]
c:101 [binder, in Kolmogorov.randomNumbers]
c:102 [binder, in Kolmogorov.randomNumbers]
c:11 [binder, in Kolmogorov.randomNumbers]
c:12 [binder, in Kolmogorov.kolmogorov]
c:16 [binder, in Kolmogorov.randomNumbers]
c:18 [binder, in Kolmogorov.kolmogorov]
c:194 [binder, in Kolmogorov.random_lower_bound]
c:26 [binder, in Kolmogorov.kolmogorov]
c:3 [binder, in Kolmogorov.kolmogorov]
c:30 [binder, in Kolmogorov.kolmogorov]
c:32 [binder, in Kolmogorov.uncomputability]
C:43 [binder, in Kolmogorov.listFacts]
c:44 [binder, in Kolmogorov.randomNumbers]
c:51 [binder, in Kolmogorov.binaryEncoding]
c:52 [binder, in Kolmogorov.randomNumbers]
c:53 [binder, in Kolmogorov.randomNumbers]
c:59 [binder, in Kolmogorov.preliminaries]
c:60 [binder, in Kolmogorov.randomNumbers]
c:63 [binder, in Kolmogorov.kolmogorov]
c:64 [binder, in Kolmogorov.preliminaries]
c:66 [binder, in Kolmogorov.randomNumbers]
c:70 [binder, in Kolmogorov.kolmogorov]
c:72 [binder, in Kolmogorov.randomNumbers]
c:77 [binder, in Kolmogorov.randomNumbers]
c:80 [binder, in Kolmogorov.randomNumbers]
c:81 [binder, in Kolmogorov.kolmogorov]
c:83 [binder, in Kolmogorov.randomNumbers]
c:84 [binder, in Kolmogorov.kolmogorov]
c:9 [binder, in Kolmogorov.randomNumbers]
c:99 [binder, in Kolmogorov.randomNumbers]
D
decode [axiom, in Kolmogorov.binaryEncoding]decodeEncode [axiom, in Kolmogorov.binaryEncoding]
decode_v_lt_pow2 [lemma, in Kolmogorov.random_lower_bound]
decode_pow2 [lemma, in Kolmogorov.binaryEncoding]
decode_nil_O [lemma, in Kolmogorov.binaryEncoding]
decode_injective [lemma, in Kolmogorov.binaryEncoding]
decode_surjective [lemma, in Kolmogorov.binaryEncoding]
decode_monotone [lemma, in Kolmogorov.binaryEncoding]
DN_intro [lemma, in Kolmogorov.preliminaries]
DN_imp [lemma, in Kolmogorov.preliminaries]
DN_LM [lemma, in Kolmogorov.preliminaries]
d:192 [binder, in Kolmogorov.random_lower_bound]
d:195 [binder, in Kolmogorov.random_lower_bound]
d:201 [binder, in Kolmogorov.random_lower_bound]
d:213 [binder, in Kolmogorov.random_lower_bound]
d:24 [binder, in Kolmogorov.kolmogorov]
E
encode [axiom, in Kolmogorov.binaryEncoding]encodeDecode [axiom, in Kolmogorov.binaryEncoding]
encode_finite_all [lemma, in Kolmogorov.binaryEncoding]
encode_finite [lemma, in Kolmogorov.binaryEncoding]
encode_injective [lemma, in Kolmogorov.binaryEncoding]
encode_surjective [lemma, in Kolmogorov.binaryEncoding]
encode_monotone2 [lemma, in Kolmogorov.binaryEncoding]
encode_monotone [axiom, in Kolmogorov.binaryEncoding]
encode_logarithmic [axiom, in Kolmogorov.binaryEncoding]
enumerator_list_NoDup [lemma, in Kolmogorov.listFacts]
enumerator_list [lemma, in Kolmogorov.listFacts]
enum_p_list_option_least_monotonic [lemma, in Kolmogorov.random_lower_bound]
enum_p_list_option_exists [lemma, in Kolmogorov.random_lower_bound]
enum_p_list_option_least [lemma, in Kolmogorov.random_lower_bound]
enum_p_list_least [lemma, in Kolmogorov.random_lower_bound]
enum_p_list_exists [lemma, in Kolmogorov.random_lower_bound]
enum_p_list_correct [lemma, in Kolmogorov.random_lower_bound]
enum_p_m_mono_incl [lemma, in Kolmogorov.random_lower_bound]
enum_p_m_step_incl [lemma, in Kolmogorov.random_lower_bound]
enum_p_m_step_length_iff [lemma, in Kolmogorov.random_lower_bound]
enum_p_m0_nil [lemma, in Kolmogorov.random_lower_bound]
enum_p_m_length [lemma, in Kolmogorov.random_lower_bound]
enum_p_m_length' [lemma, in Kolmogorov.random_lower_bound]
enum_p_m_eq_length [lemma, in Kolmogorov.random_lower_bound]
enum_p_m_equiv [lemma, in Kolmogorov.random_lower_bound]
enum_p_m_step_length [lemma, in Kolmogorov.random_lower_bound]
enum_p_m_Sm [lemma, in Kolmogorov.random_lower_bound]
enum_p_list_equiv [lemma, in Kolmogorov.random_lower_bound]
enum_p_list_max_length [lemma, in Kolmogorov.random_lower_bound]
enum_p_list_mono_length [lemma, in Kolmogorov.random_lower_bound]
enum_p_list_incl [lemma, in Kolmogorov.random_lower_bound]
enum_p_list_incl_step [lemma, in Kolmogorov.random_lower_bound]
enum_p_list_sat_len_n [lemma, in Kolmogorov.random_lower_bound]
enum_p_list_sat_p [lemma, in Kolmogorov.random_lower_bound]
enum_p_list_length_s [lemma, in Kolmogorov.random_lower_bound]
enum_p_list_length [lemma, in Kolmogorov.random_lower_bound]
enum_p_list_NoDup [lemma, in Kolmogorov.random_lower_bound]
enum_p_list [definition, in Kolmogorov.random_lower_bound]
EqDecision0:155 [binder, in Kolmogorov.listFacts]
EqDecision0:160 [binder, in Kolmogorov.listFacts]
eqdec:14 [binder, in Kolmogorov.listFacts]
eqdec:147 [binder, in Kolmogorov.listFacts]
eqdec:18 [binder, in Kolmogorov.listFacts]
eqdec:22 [binder, in Kolmogorov.listFacts]
eqdec:45 [binder, in Kolmogorov.listFacts]
equiv [definition, in Kolmogorov.listFacts]
exists_kol_le [lemma, in Kolmogorov.kolmogorov]
exists_kol [lemma, in Kolmogorov.kolmogorov]
exists_univ [lemma, in Kolmogorov.kolmogorov]
exp_superlinear [lemma, in Kolmogorov.binaryEncoding]
F
firstn_incl [lemma, in Kolmogorov.listFacts]firstn_incl_le [lemma, in Kolmogorov.listFacts]
firstn_In [lemma, in Kolmogorov.listFacts]
firstn_app [lemma, in Kolmogorov.listFacts]
first_false_replicate [lemma, in Kolmogorov.listFacts]
Forall_remove [lemma, in Kolmogorov.listFacts]
f:103 [binder, in Kolmogorov.random_lower_bound]
f:107 [binder, in Kolmogorov.random_lower_bound]
f:108 [binder, in Kolmogorov.listFacts]
f:112 [binder, in Kolmogorov.random_lower_bound]
f:117 [binder, in Kolmogorov.random_lower_bound]
f:123 [binder, in Kolmogorov.random_lower_bound]
f:130 [binder, in Kolmogorov.random_lower_bound]
f:14 [binder, in Kolmogorov.random_lower_bound]
f:161 [binder, in Kolmogorov.random_lower_bound]
f:172 [binder, in Kolmogorov.random_lower_bound]
f:180 [binder, in Kolmogorov.random_lower_bound]
f:188 [binder, in Kolmogorov.random_lower_bound]
f:19 [binder, in Kolmogorov.random_lower_bound]
f:199 [binder, in Kolmogorov.random_lower_bound]
f:2 [binder, in Kolmogorov.random_lower_bound]
f:211 [binder, in Kolmogorov.random_lower_bound]
f:24 [binder, in Kolmogorov.random_lower_bound]
f:31 [binder, in Kolmogorov.kolmogorov]
f:32 [binder, in Kolmogorov.random_lower_bound]
f:35 [binder, in Kolmogorov.random_lower_bound]
f:37 [binder, in Kolmogorov.uncomputability]
f:39 [binder, in Kolmogorov.preliminaries]
f:41 [binder, in Kolmogorov.random_lower_bound]
f:45 [binder, in Kolmogorov.randomNumbers]
f:46 [binder, in Kolmogorov.random_lower_bound]
f:52 [binder, in Kolmogorov.random_lower_bound]
f:58 [binder, in Kolmogorov.random_lower_bound]
f:58 [binder, in Kolmogorov.preliminaries]
f:63 [binder, in Kolmogorov.preliminaries]
f:64 [binder, in Kolmogorov.random_lower_bound]
f:70 [binder, in Kolmogorov.random_lower_bound]
f:70 [binder, in Kolmogorov.preliminaries]
f:76 [binder, in Kolmogorov.random_lower_bound]
f:8 [binder, in Kolmogorov.preliminaries]
f:81 [binder, in Kolmogorov.random_lower_bound]
f:83 [binder, in Kolmogorov.kolmogorov]
f:86 [binder, in Kolmogorov.random_lower_bound]
f:9 [binder, in Kolmogorov.kolmogorov]
f:91 [binder, in Kolmogorov.random_lower_bound]
f:93 [binder, in Kolmogorov.listFacts]
f:97 [binder, in Kolmogorov.random_lower_bound]
G
g:10 [binder, in Kolmogorov.kolmogorov]H
H:183 [binder, in Kolmogorov.random_lower_bound]H:69 [binder, in Kolmogorov.preliminaries]
I
incl_transitive [lemma, in Kolmogorov.listFacts]Injective_rev_seq [lemma, in Kolmogorov.listFacts]
Injective_rev [lemma, in Kolmogorov.listFacts]
input:43 [binder, in Kolmogorov.kolmogorov]
input:48 [binder, in Kolmogorov.kolmogorov]
input:53 [binder, in Kolmogorov.kolmogorov]
input:58 [binder, in Kolmogorov.kolmogorov]
InvarianceTheorem [lemma, in Kolmogorov.kolmogorov]
In_skipn [lemma, in Kolmogorov.listFacts]
In_le_n_list [lemma, in Kolmogorov.binaryEncoding]
i:3 [binder, in Kolmogorov.randomNumbers]
i:30 [binder, in Kolmogorov.randomNumbers]
i:32 [binder, in Kolmogorov.randomNumbers]
i:34 [binder, in Kolmogorov.kolmogorov]
i:39 [binder, in Kolmogorov.randomNumbers]
i:42 [binder, in Kolmogorov.randomNumbers]
i:47 [binder, in Kolmogorov.randomNumbers]
i:50 [binder, in Kolmogorov.randomNumbers]
i:57 [binder, in Kolmogorov.randomNumbers]
i:60 [binder, in Kolmogorov.kolmogorov]
i:7 [binder, in Kolmogorov.randomNumbers]
i:78 [binder, in Kolmogorov.kolmogorov]
J
j:64 [binder, in Kolmogorov.kolmogorov]j:65 [binder, in Kolmogorov.kolmogorov]
j:67 [binder, in Kolmogorov.kolmogorov]
j:68 [binder, in Kolmogorov.kolmogorov]
K
kc':21 [binder, in Kolmogorov.kolmogorov]kc:13 [binder, in Kolmogorov.randomNumbers]
kc:14 [binder, in Kolmogorov.randomNumbers]
kc:15 [binder, in Kolmogorov.randomNumbers]
kc:18 [binder, in Kolmogorov.randomNumbers]
kc:19 [binder, in Kolmogorov.randomNumbers]
kc:20 [binder, in Kolmogorov.kolmogorov]
kc:20 [binder, in Kolmogorov.randomNumbers]
kc:21 [binder, in Kolmogorov.randomNumbers]
kc:22 [binder, in Kolmogorov.randomNumbers]
kc:23 [binder, in Kolmogorov.randomNumbers]
kc:24 [binder, in Kolmogorov.randomNumbers]
kc:25 [binder, in Kolmogorov.randomNumbers]
kc:26 [binder, in Kolmogorov.randomNumbers]
kc:27 [binder, in Kolmogorov.randomNumbers]
kc:35 [binder, in Kolmogorov.uncomputability]
kol [definition, in Kolmogorov.kolmogorov]
kolmogorov [library]
kol_unbounded [lemma, in Kolmogorov.uncomputability]
kol_list_le [lemma, in Kolmogorov.uncomputability]
kol_list_eq [lemma, in Kolmogorov.uncomputability]
kol_functional [lemma, in Kolmogorov.kolmogorov]
kol_alt [lemma, in Kolmogorov.kolmogorov]
k':87 [binder, in Kolmogorov.preliminaries]
k:14 [binder, in Kolmogorov.kolmogorov]
k:15 [binder, in Kolmogorov.kolmogorov]
k:196 [binder, in Kolmogorov.random_lower_bound]
k:231 [binder, in Kolmogorov.random_lower_bound]
k:232 [binder, in Kolmogorov.random_lower_bound]
k:24 [binder, in Kolmogorov.preliminaries]
k:28 [binder, in Kolmogorov.preliminaries]
k:32 [binder, in Kolmogorov.kolmogorov]
k:47 [binder, in Kolmogorov.binaryEncoding]
k:54 [binder, in Kolmogorov.randomNumbers]
k:62 [binder, in Kolmogorov.randomNumbers]
k:67 [binder, in Kolmogorov.randomNumbers]
k:72 [binder, in Kolmogorov.kolmogorov]
k:73 [binder, in Kolmogorov.randomNumbers]
k:78 [binder, in Kolmogorov.binaryEncoding]
k:78 [binder, in Kolmogorov.randomNumbers]
k:86 [binder, in Kolmogorov.preliminaries]
k:86 [binder, in Kolmogorov.kolmogorov]
L
last_rev_first [lemma, in Kolmogorov.listFacts]least_unique [lemma, in Kolmogorov.preliminaries]
le_list_encode [lemma, in Kolmogorov.binaryEncoding]
le_list [lemma, in Kolmogorov.binaryEncoding]
le_n_list_lt_n_list [lemma, in Kolmogorov.binaryEncoding]
le_n_list_length [lemma, in Kolmogorov.binaryEncoding]
le_n_list_NoDup [lemma, in Kolmogorov.binaryEncoding]
le_n_list_In [lemma, in Kolmogorov.binaryEncoding]
le_n_list [definition, in Kolmogorov.binaryEncoding]
listFacts [library]
list_difference_noDup_length [lemma, in Kolmogorov.listFacts]
list_differece_not_in_eq [lemma, in Kolmogorov.listFacts]
LM_DN [lemma, in Kolmogorov.preliminaries]
log2_pow2_lt [lemma, in Kolmogorov.binaryEncoding]
lt_length_list' [lemma, in Kolmogorov.listFacts]
lt_length_list [lemma, in Kolmogorov.listFacts]
l_sublinear [lemma, in Kolmogorov.binaryEncoding]
l_encode_unbounded [lemma, in Kolmogorov.binaryEncoding]
L':103 [binder, in Kolmogorov.listFacts]
L':110 [binder, in Kolmogorov.listFacts]
L':114 [binder, in Kolmogorov.listFacts]
L':118 [binder, in Kolmogorov.listFacts]
L':149 [binder, in Kolmogorov.listFacts]
L':15 [binder, in Kolmogorov.binaryEncoding]
l':15 [binder, in Kolmogorov.preliminaries]
L':157 [binder, in Kolmogorov.listFacts]
L':162 [binder, in Kolmogorov.listFacts]
l':197 [binder, in Kolmogorov.random_lower_bound]
l':20 [binder, in Kolmogorov.preliminaries]
l':22 [binder, in Kolmogorov.uncomputability]
l':48 [binder, in Kolmogorov.listFacts]
L':56 [binder, in Kolmogorov.randomNumbers]
l':61 [binder, in Kolmogorov.randomNumbers]
l':68 [binder, in Kolmogorov.randomNumbers]
L':91 [binder, in Kolmogorov.listFacts]
L':95 [binder, in Kolmogorov.listFacts]
L':99 [binder, in Kolmogorov.listFacts]
L:10 [binder, in Kolmogorov.random_lower_bound]
L:102 [binder, in Kolmogorov.listFacts]
L:109 [binder, in Kolmogorov.listFacts]
L:11 [binder, in Kolmogorov.uncomputability]
L:113 [binder, in Kolmogorov.listFacts]
L:117 [binder, in Kolmogorov.listFacts]
L:12 [binder, in Kolmogorov.listFacts]
L:123 [binder, in Kolmogorov.listFacts]
L:125 [binder, in Kolmogorov.listFacts]
L:128 [binder, in Kolmogorov.listFacts]
L:133 [binder, in Kolmogorov.random_lower_bound]
L:14 [binder, in Kolmogorov.binaryEncoding]
l:14 [binder, in Kolmogorov.preliminaries]
L:148 [binder, in Kolmogorov.listFacts]
L:156 [binder, in Kolmogorov.listFacts]
L:16 [binder, in Kolmogorov.listFacts]
L:16 [binder, in Kolmogorov.binaryEncoding]
L:161 [binder, in Kolmogorov.listFacts]
L:165 [binder, in Kolmogorov.listFacts]
L:184 [binder, in Kolmogorov.random_lower_bound]
L:19 [binder, in Kolmogorov.binaryEncoding]
l:19 [binder, in Kolmogorov.preliminaries]
l:2 [binder, in Kolmogorov.uncomputability]
l:20 [binder, in Kolmogorov.uncomputability]
L:20 [binder, in Kolmogorov.listFacts]
L:206 [binder, in Kolmogorov.random_lower_bound]
L:209 [binder, in Kolmogorov.random_lower_bound]
L:21 [binder, in Kolmogorov.uncomputability]
L:218 [binder, in Kolmogorov.random_lower_bound]
L:221 [binder, in Kolmogorov.random_lower_bound]
L:24 [binder, in Kolmogorov.uncomputability]
L:25 [binder, in Kolmogorov.listFacts]
L:25 [binder, in Kolmogorov.binaryEncoding]
L:26 [binder, in Kolmogorov.listFacts]
L:29 [binder, in Kolmogorov.binaryEncoding]
L:3 [binder, in Kolmogorov.uncomputability]
l:3 [binder, in Kolmogorov.binaryEncoding]
L:30 [binder, in Kolmogorov.listFacts]
L:34 [binder, in Kolmogorov.listFacts]
L:37 [binder, in Kolmogorov.binaryEncoding]
L:39 [binder, in Kolmogorov.listFacts]
l:41 [binder, in Kolmogorov.binaryEncoding]
L:42 [binder, in Kolmogorov.binaryEncoding]
l:44 [binder, in Kolmogorov.binaryEncoding]
L:45 [binder, in Kolmogorov.binaryEncoding]
L:46 [binder, in Kolmogorov.listFacts]
l:47 [binder, in Kolmogorov.listFacts]
L:52 [binder, in Kolmogorov.listFacts]
L:55 [binder, in Kolmogorov.randomNumbers]
L:57 [binder, in Kolmogorov.binaryEncoding]
L:58 [binder, in Kolmogorov.listFacts]
L:6 [binder, in Kolmogorov.uncomputability]
L:61 [binder, in Kolmogorov.binaryEncoding]
L:62 [binder, in Kolmogorov.listFacts]
L:65 [binder, in Kolmogorov.binaryEncoding]
L:66 [binder, in Kolmogorov.listFacts]
L:69 [binder, in Kolmogorov.listFacts]
L:7 [binder, in Kolmogorov.listFacts]
L:72 [binder, in Kolmogorov.listFacts]
L:74 [binder, in Kolmogorov.random_lower_bound]
L:75 [binder, in Kolmogorov.listFacts]
L:85 [binder, in Kolmogorov.listFacts]
L:89 [binder, in Kolmogorov.listFacts]
L:9 [binder, in Kolmogorov.random_lower_bound]
L:94 [binder, in Kolmogorov.listFacts]
L:98 [binder, in Kolmogorov.listFacts]
M
map_n_list_NoDup [lemma, in Kolmogorov.binaryEncoding]model:47 [binder, in Kolmogorov.preliminaries]
monotonic_eq [lemma, in Kolmogorov.preliminaries]
MP_LM [lemma, in Kolmogorov.preliminaries]
m':100 [binder, in Kolmogorov.random_lower_bound]
m':120 [binder, in Kolmogorov.random_lower_bound]
m':95 [binder, in Kolmogorov.random_lower_bound]
m:10 [binder, in Kolmogorov.uncomputability]
m:101 [binder, in Kolmogorov.random_lower_bound]
m:108 [binder, in Kolmogorov.random_lower_bound]
m:115 [binder, in Kolmogorov.random_lower_bound]
m:121 [binder, in Kolmogorov.random_lower_bound]
m:124 [binder, in Kolmogorov.random_lower_bound]
m:131 [binder, in Kolmogorov.random_lower_bound]
m:15 [binder, in Kolmogorov.random_lower_bound]
m:162 [binder, in Kolmogorov.random_lower_bound]
m:173 [binder, in Kolmogorov.random_lower_bound]
m:189 [binder, in Kolmogorov.random_lower_bound]
m:20 [binder, in Kolmogorov.random_lower_bound]
m:21 [binder, in Kolmogorov.binaryEncoding]
m:23 [binder, in Kolmogorov.kolmogorov]
m:25 [binder, in Kolmogorov.random_lower_bound]
m:29 [binder, in Kolmogorov.random_lower_bound]
m:3 [binder, in Kolmogorov.random_lower_bound]
m:32 [binder, in Kolmogorov.preliminaries]
m:33 [binder, in Kolmogorov.uncomputability]
m:36 [binder, in Kolmogorov.random_lower_bound]
m:39 [binder, in Kolmogorov.uncomputability]
m:40 [binder, in Kolmogorov.preliminaries]
m:42 [binder, in Kolmogorov.uncomputability]
m:42 [binder, in Kolmogorov.random_lower_bound]
m:47 [binder, in Kolmogorov.random_lower_bound]
m:49 [binder, in Kolmogorov.uncomputability]
m:5 [binder, in Kolmogorov.uncomputability]
m:50 [binder, in Kolmogorov.uncomputability]
m:51 [binder, in Kolmogorov.uncomputability]
m:52 [binder, in Kolmogorov.uncomputability]
m:53 [binder, in Kolmogorov.uncomputability]
m:53 [binder, in Kolmogorov.random_lower_bound]
m:54 [binder, in Kolmogorov.uncomputability]
m:59 [binder, in Kolmogorov.random_lower_bound]
m:65 [binder, in Kolmogorov.random_lower_bound]
m:73 [binder, in Kolmogorov.random_lower_bound]
m:77 [binder, in Kolmogorov.random_lower_bound]
m:82 [binder, in Kolmogorov.random_lower_bound]
m:85 [binder, in Kolmogorov.kolmogorov]
m:86 [binder, in Kolmogorov.randomNumbers]
m:87 [binder, in Kolmogorov.random_lower_bound]
m:88 [binder, in Kolmogorov.randomNumbers]
m:90 [binder, in Kolmogorov.randomNumbers]
m:91 [binder, in Kolmogorov.randomNumbers]
m:94 [binder, in Kolmogorov.random_lower_bound]
N
nat_infinite [lemma, in Kolmogorov.uncomputability]nat_list_NoDup_size [lemma, in Kolmogorov.listFacts]
NoDup_equiv_length_eq [lemma, in Kolmogorov.listFacts]
NoDup_firstn [lemma, in Kolmogorov.listFacts]
NoDup_skipn [lemma, in Kolmogorov.listFacts]
nodup_length [lemma, in Kolmogorov.listFacts]
NoDup_partition [lemma, in Kolmogorov.listFacts]
NoDup_remove_length [lemma, in Kolmogorov.listFacts]
NoDup_remove [lemma, in Kolmogorov.listFacts]
nonR [definition, in Kolmogorov.randomNumbers]
nonR_m_incomplete [lemma, in Kolmogorov.randomNumbers]
nonR_undecidable [lemma, in Kolmogorov.randomNumbers]
nonR_simple [lemma, in Kolmogorov.randomNumbers]
nonR_length [lemma, in Kolmogorov.randomNumbers]
nonR_list [lemma, in Kolmogorov.randomNumbers]
nonR_enum [lemma, in Kolmogorov.randomNumbers]
nonR_enumerator [lemma, in Kolmogorov.randomNumbers]
nonR_R [lemma, in Kolmogorov.randomNumbers]
nonR_nonRalt [lemma, in Kolmogorov.randomNumbers]
not_In_le_n_list [lemma, in Kolmogorov.binaryEncoding]
num_first_false [definition, in Kolmogorov.listFacts]
n_list_length [lemma, in Kolmogorov.binaryEncoding]
n_list_NoDup [lemma, in Kolmogorov.binaryEncoding]
n_list_In [lemma, in Kolmogorov.binaryEncoding]
n_list [definition, in Kolmogorov.binaryEncoding]
N_imp [lemma, in Kolmogorov.preliminaries]
n':61 [binder, in Kolmogorov.listFacts]
n':64 [binder, in Kolmogorov.listFacts]
n':72 [binder, in Kolmogorov.preliminaries]
n1:45 [binder, in Kolmogorov.uncomputability]
n1:46 [binder, in Kolmogorov.uncomputability]
n:1 [binder, in Kolmogorov.uncomputability]
n:1 [binder, in Kolmogorov.kolmogorov]
n:1 [binder, in Kolmogorov.randomNumbers]
n:10 [binder, in Kolmogorov.preliminaries]
n:101 [binder, in Kolmogorov.listFacts]
n:104 [binder, in Kolmogorov.random_lower_bound]
n:109 [binder, in Kolmogorov.random_lower_bound]
n:11 [binder, in Kolmogorov.listFacts]
n:112 [binder, in Kolmogorov.listFacts]
n:113 [binder, in Kolmogorov.random_lower_bound]
n:116 [binder, in Kolmogorov.listFacts]
n:118 [binder, in Kolmogorov.random_lower_bound]
n:122 [binder, in Kolmogorov.listFacts]
n:125 [binder, in Kolmogorov.random_lower_bound]
n:126 [binder, in Kolmogorov.listFacts]
n:132 [binder, in Kolmogorov.random_lower_bound]
n:16 [binder, in Kolmogorov.random_lower_bound]
n:163 [binder, in Kolmogorov.random_lower_bound]
n:164 [binder, in Kolmogorov.listFacts]
n:174 [binder, in Kolmogorov.random_lower_bound]
n:181 [binder, in Kolmogorov.random_lower_bound]
n:19 [binder, in Kolmogorov.uncomputability]
n:190 [binder, in Kolmogorov.random_lower_bound]
n:20 [binder, in Kolmogorov.binaryEncoding]
n:203 [binder, in Kolmogorov.random_lower_bound]
n:21 [binder, in Kolmogorov.random_lower_bound]
n:215 [binder, in Kolmogorov.random_lower_bound]
n:22 [binder, in Kolmogorov.binaryEncoding]
n:22 [binder, in Kolmogorov.kolmogorov]
n:223 [binder, in Kolmogorov.random_lower_bound]
n:224 [binder, in Kolmogorov.random_lower_bound]
n:225 [binder, in Kolmogorov.random_lower_bound]
n:226 [binder, in Kolmogorov.random_lower_bound]
n:23 [binder, in Kolmogorov.preliminaries]
n:25 [binder, in Kolmogorov.uncomputability]
n:26 [binder, in Kolmogorov.random_lower_bound]
n:26 [binder, in Kolmogorov.preliminaries]
n:27 [binder, in Kolmogorov.uncomputability]
n:27 [binder, in Kolmogorov.preliminaries]
n:28 [binder, in Kolmogorov.binaryEncoding]
n:28 [binder, in Kolmogorov.randomNumbers]
n:30 [binder, in Kolmogorov.uncomputability]
n:30 [binder, in Kolmogorov.random_lower_bound]
n:30 [binder, in Kolmogorov.binaryEncoding]
n:30 [binder, in Kolmogorov.preliminaries]
n:31 [binder, in Kolmogorov.binaryEncoding]
n:32 [binder, in Kolmogorov.binaryEncoding]
n:33 [binder, in Kolmogorov.listFacts]
n:33 [binder, in Kolmogorov.binaryEncoding]
n:33 [binder, in Kolmogorov.preliminaries]
n:34 [binder, in Kolmogorov.randomNumbers]
n:36 [binder, in Kolmogorov.uncomputability]
n:36 [binder, in Kolmogorov.binaryEncoding]
n:36 [binder, in Kolmogorov.randomNumbers]
n:37 [binder, in Kolmogorov.random_lower_bound]
n:38 [binder, in Kolmogorov.listFacts]
n:38 [binder, in Kolmogorov.binaryEncoding]
n:38 [binder, in Kolmogorov.kolmogorov]
n:39 [binder, in Kolmogorov.binaryEncoding]
n:4 [binder, in Kolmogorov.random_lower_bound]
n:40 [binder, in Kolmogorov.binaryEncoding]
n:41 [binder, in Kolmogorov.preliminaries]
n:43 [binder, in Kolmogorov.random_lower_bound]
n:48 [binder, in Kolmogorov.random_lower_bound]
n:48 [binder, in Kolmogorov.binaryEncoding]
n:5 [binder, in Kolmogorov.binaryEncoding]
n:5 [binder, in Kolmogorov.randomNumbers]
n:52 [binder, in Kolmogorov.binaryEncoding]
n:53 [binder, in Kolmogorov.binaryEncoding]
n:54 [binder, in Kolmogorov.random_lower_bound]
n:54 [binder, in Kolmogorov.binaryEncoding]
n:55 [binder, in Kolmogorov.binaryEncoding]
n:57 [binder, in Kolmogorov.listFacts]
n:59 [binder, in Kolmogorov.binaryEncoding]
n:59 [binder, in Kolmogorov.kolmogorov]
n:6 [binder, in Kolmogorov.listFacts]
n:60 [binder, in Kolmogorov.listFacts]
n:60 [binder, in Kolmogorov.random_lower_bound]
n:65 [binder, in Kolmogorov.listFacts]
n:66 [binder, in Kolmogorov.random_lower_bound]
n:68 [binder, in Kolmogorov.listFacts]
n:7 [binder, in Kolmogorov.binaryEncoding]
n:71 [binder, in Kolmogorov.listFacts]
n:71 [binder, in Kolmogorov.random_lower_bound]
n:71 [binder, in Kolmogorov.preliminaries]
n:73 [binder, in Kolmogorov.binaryEncoding]
n:74 [binder, in Kolmogorov.listFacts]
n:76 [binder, in Kolmogorov.listFacts]
n:77 [binder, in Kolmogorov.listFacts]
n:77 [binder, in Kolmogorov.binaryEncoding]
n:77 [binder, in Kolmogorov.kolmogorov]
n:78 [binder, in Kolmogorov.random_lower_bound]
n:79 [binder, in Kolmogorov.listFacts]
n:79 [binder, in Kolmogorov.binaryEncoding]
n:8 [binder, in Kolmogorov.kolmogorov]
n:81 [binder, in Kolmogorov.listFacts]
n:82 [binder, in Kolmogorov.kolmogorov]
n:83 [binder, in Kolmogorov.random_lower_bound]
n:87 [binder, in Kolmogorov.randomNumbers]
n:88 [binder, in Kolmogorov.random_lower_bound]
n:89 [binder, in Kolmogorov.randomNumbers]
n:9 [binder, in Kolmogorov.preliminaries]
n:90 [binder, in Kolmogorov.listFacts]
n:92 [binder, in Kolmogorov.random_lower_bound]
n:92 [binder, in Kolmogorov.randomNumbers]
n:94 [binder, in Kolmogorov.randomNumbers]
n:97 [binder, in Kolmogorov.listFacts]
n:98 [binder, in Kolmogorov.random_lower_bound]
O
ONat_eqb_neq [lemma, in Kolmogorov.preliminaries]ONat_eqb_eq [lemma, in Kolmogorov.preliminaries]
ONat_eqb [definition, in Kolmogorov.preliminaries]
o:176 [binder, in Kolmogorov.random_lower_bound]
o:59 [binder, in Kolmogorov.randomNumbers]
P
PCT [axiom, in Kolmogorov.preliminaries]pow_ge_1 [lemma, in Kolmogorov.binaryEncoding]
pow_div_ge_1 [lemma, in Kolmogorov.preliminaries]
pow2_length_encode [lemma, in Kolmogorov.binaryEncoding]
preliminaries [library]
program:42 [binder, in Kolmogorov.kolmogorov]
program:47 [binder, in Kolmogorov.kolmogorov]
program:52 [binder, in Kolmogorov.kolmogorov]
program:57 [binder, in Kolmogorov.kolmogorov]
p_enumerable_infinite_unbounded [lemma, in Kolmogorov.preliminaries]
p_infinite_unbounded [lemma, in Kolmogorov.preliminaries]
p_sublist_NoDup [lemma, in Kolmogorov.preliminaries]
p_sublist [lemma, in Kolmogorov.preliminaries]
p:1 [binder, in Kolmogorov.random_lower_bound]
p:100 [binder, in Kolmogorov.randomNumbers]
p:102 [binder, in Kolmogorov.random_lower_bound]
p:106 [binder, in Kolmogorov.random_lower_bound]
p:107 [binder, in Kolmogorov.listFacts]
P:11 [binder, in Kolmogorov.preliminaries]
p:111 [binder, in Kolmogorov.random_lower_bound]
p:116 [binder, in Kolmogorov.random_lower_bound]
p:122 [binder, in Kolmogorov.random_lower_bound]
p:129 [binder, in Kolmogorov.random_lower_bound]
p:13 [binder, in Kolmogorov.random_lower_bound]
p:13 [binder, in Kolmogorov.preliminaries]
p:160 [binder, in Kolmogorov.random_lower_bound]
p:171 [binder, in Kolmogorov.random_lower_bound]
p:179 [binder, in Kolmogorov.random_lower_bound]
p:18 [binder, in Kolmogorov.random_lower_bound]
p:18 [binder, in Kolmogorov.preliminaries]
p:187 [binder, in Kolmogorov.random_lower_bound]
P:2 [binder, in Kolmogorov.preliminaries]
p:22 [binder, in Kolmogorov.preliminaries]
p:23 [binder, in Kolmogorov.listFacts]
p:23 [binder, in Kolmogorov.random_lower_bound]
p:28 [binder, in Kolmogorov.random_lower_bound]
P:3 [binder, in Kolmogorov.preliminaries]
p:34 [binder, in Kolmogorov.random_lower_bound]
p:38 [binder, in Kolmogorov.randomNumbers]
p:40 [binder, in Kolmogorov.random_lower_bound]
p:41 [binder, in Kolmogorov.randomNumbers]
p:45 [binder, in Kolmogorov.random_lower_bound]
p:46 [binder, in Kolmogorov.randomNumbers]
p:49 [binder, in Kolmogorov.randomNumbers]
P:5 [binder, in Kolmogorov.preliminaries]
p:51 [binder, in Kolmogorov.random_lower_bound]
p:57 [binder, in Kolmogorov.random_lower_bound]
p:63 [binder, in Kolmogorov.random_lower_bound]
p:69 [binder, in Kolmogorov.random_lower_bound]
p:75 [binder, in Kolmogorov.random_lower_bound]
p:75 [binder, in Kolmogorov.preliminaries]
p:80 [binder, in Kolmogorov.random_lower_bound]
p:85 [binder, in Kolmogorov.random_lower_bound]
p:90 [binder, in Kolmogorov.random_lower_bound]
p:92 [binder, in Kolmogorov.listFacts]
p:96 [binder, in Kolmogorov.random_lower_bound]
p:96 [binder, in Kolmogorov.randomNumbers]
Q
Q:1 [binder, in Kolmogorov.preliminaries]q:31 [binder, in Kolmogorov.preliminaries]
q:38 [binder, in Kolmogorov.preliminaries]
Q:4 [binder, in Kolmogorov.preliminaries]
Q:6 [binder, in Kolmogorov.preliminaries]
Q:7 [binder, in Kolmogorov.preliminaries]
q:84 [binder, in Kolmogorov.randomNumbers]
q:97 [binder, in Kolmogorov.randomNumbers]
R
R [definition, in Kolmogorov.randomNumbers]randomNumbers [library]
random_lower_bound [library]
rev_seq_rev [lemma, in Kolmogorov.listFacts]
rev_rev_seq [lemma, in Kolmogorov.listFacts]
rev_seq_last_O [lemma, in Kolmogorov.listFacts]
rev_seq_not_nil [lemma, in Kolmogorov.listFacts]
rev_seq [definition, in Kolmogorov.listFacts]
R_length_min [lemma, in Kolmogorov.random_lower_bound]
R_no_enum_inf_subp [lemma, in Kolmogorov.randomNumbers]
R_infinite [lemma, in Kolmogorov.randomNumbers]
R_unbounded' [lemma, in Kolmogorov.randomNumbers]
R_unbounded [lemma, in Kolmogorov.randomNumbers]
R_non_empty [lemma, in Kolmogorov.randomNumbers]
R_nonR [lemma, in Kolmogorov.randomNumbers]
R_nonR1 [lemma, in Kolmogorov.randomNumbers]
R_Ralt [lemma, in Kolmogorov.randomNumbers]
R_nonR_contradiction [lemma, in Kolmogorov.randomNumbers]
r:14 [binder, in Kolmogorov.uncomputability]
r:16 [binder, in Kolmogorov.uncomputability]
r:18 [binder, in Kolmogorov.uncomputability]
r:9 [binder, in Kolmogorov.uncomputability]
S
simple [definition, in Kolmogorov.randomNumbers]simple_enum_sdec [lemma, in Kolmogorov.randomNumbers]
size:41 [binder, in Kolmogorov.kolmogorov]
size:46 [binder, in Kolmogorov.kolmogorov]
size:51 [binder, in Kolmogorov.kolmogorov]
size:56 [binder, in Kolmogorov.kolmogorov]
skipn_length [lemma, in Kolmogorov.listFacts]
skipn_incl_le [lemma, in Kolmogorov.listFacts]
skipn_incl [lemma, in Kolmogorov.listFacts]
skipn_replicate_app_cons [lemma, in Kolmogorov.listFacts]
skipn_replicate_app [lemma, in Kolmogorov.listFacts]
start:53 [binder, in Kolmogorov.listFacts]
s':127 [binder, in Kolmogorov.random_lower_bound]
s':227 [binder, in Kolmogorov.random_lower_bound]
s':228 [binder, in Kolmogorov.random_lower_bound]
s':50 [binder, in Kolmogorov.random_lower_bound]
s':56 [binder, in Kolmogorov.random_lower_bound]
s':62 [binder, in Kolmogorov.random_lower_bound]
s':68 [binder, in Kolmogorov.random_lower_bound]
s:105 [binder, in Kolmogorov.random_lower_bound]
s:110 [binder, in Kolmogorov.random_lower_bound]
s:114 [binder, in Kolmogorov.random_lower_bound]
s:119 [binder, in Kolmogorov.random_lower_bound]
s:126 [binder, in Kolmogorov.random_lower_bound]
s:13 [binder, in Kolmogorov.uncomputability]
s:134 [binder, in Kolmogorov.random_lower_bound]
s:15 [binder, in Kolmogorov.uncomputability]
s:164 [binder, in Kolmogorov.random_lower_bound]
s:17 [binder, in Kolmogorov.uncomputability]
s:17 [binder, in Kolmogorov.random_lower_bound]
s:17 [binder, in Kolmogorov.kolmogorov]
s:175 [binder, in Kolmogorov.random_lower_bound]
s:185 [binder, in Kolmogorov.random_lower_bound]
s:191 [binder, in Kolmogorov.random_lower_bound]
s:205 [binder, in Kolmogorov.random_lower_bound]
s:208 [binder, in Kolmogorov.random_lower_bound]
s:217 [binder, in Kolmogorov.random_lower_bound]
s:22 [binder, in Kolmogorov.random_lower_bound]
s:220 [binder, in Kolmogorov.random_lower_bound]
s:229 [binder, in Kolmogorov.random_lower_bound]
s:230 [binder, in Kolmogorov.random_lower_bound]
s:238 [binder, in Kolmogorov.random_lower_bound]
s:240 [binder, in Kolmogorov.random_lower_bound]
s:241 [binder, in Kolmogorov.random_lower_bound]
s:243 [binder, in Kolmogorov.random_lower_bound]
s:27 [binder, in Kolmogorov.random_lower_bound]
s:28 [binder, in Kolmogorov.kolmogorov]
s:29 [binder, in Kolmogorov.kolmogorov]
s:31 [binder, in Kolmogorov.random_lower_bound]
s:31 [binder, in Kolmogorov.randomNumbers]
s:33 [binder, in Kolmogorov.randomNumbers]
s:35 [binder, in Kolmogorov.kolmogorov]
s:36 [binder, in Kolmogorov.kolmogorov]
s:37 [binder, in Kolmogorov.kolmogorov]
s:38 [binder, in Kolmogorov.random_lower_bound]
s:4 [binder, in Kolmogorov.randomNumbers]
s:40 [binder, in Kolmogorov.kolmogorov]
s:40 [binder, in Kolmogorov.randomNumbers]
s:43 [binder, in Kolmogorov.randomNumbers]
s:44 [binder, in Kolmogorov.random_lower_bound]
s:45 [binder, in Kolmogorov.kolmogorov]
s:48 [binder, in Kolmogorov.randomNumbers]
s:49 [binder, in Kolmogorov.random_lower_bound]
s:5 [binder, in Kolmogorov.random_lower_bound]
s:5 [binder, in Kolmogorov.kolmogorov]
s:50 [binder, in Kolmogorov.kolmogorov]
s:51 [binder, in Kolmogorov.preliminaries]
s:51 [binder, in Kolmogorov.randomNumbers]
s:52 [binder, in Kolmogorov.preliminaries]
s:55 [binder, in Kolmogorov.random_lower_bound]
s:55 [binder, in Kolmogorov.kolmogorov]
s:58 [binder, in Kolmogorov.randomNumbers]
s:61 [binder, in Kolmogorov.random_lower_bound]
s:61 [binder, in Kolmogorov.preliminaries]
s:62 [binder, in Kolmogorov.kolmogorov]
s:66 [binder, in Kolmogorov.kolmogorov]
s:67 [binder, in Kolmogorov.random_lower_bound]
s:69 [binder, in Kolmogorov.kolmogorov]
s:7 [binder, in Kolmogorov.kolmogorov]
s:72 [binder, in Kolmogorov.random_lower_bound]
s:75 [binder, in Kolmogorov.kolmogorov]
s:76 [binder, in Kolmogorov.kolmogorov]
s:79 [binder, in Kolmogorov.random_lower_bound]
s:8 [binder, in Kolmogorov.uncomputability]
s:8 [binder, in Kolmogorov.randomNumbers]
s:80 [binder, in Kolmogorov.kolmogorov]
s:84 [binder, in Kolmogorov.random_lower_bound]
s:89 [binder, in Kolmogorov.random_lower_bound]
s:93 [binder, in Kolmogorov.random_lower_bound]
s:99 [binder, in Kolmogorov.random_lower_bound]
T
T'':57 [binder, in Kolmogorov.preliminaries]T':49 [binder, in Kolmogorov.preliminaries]
T':54 [binder, in Kolmogorov.preliminaries]
T':56 [binder, in Kolmogorov.preliminaries]
T:48 [binder, in Kolmogorov.preliminaries]
T:53 [binder, in Kolmogorov.preliminaries]
T:55 [binder, in Kolmogorov.preliminaries]
U
uncomputability [lemma, in Kolmogorov.uncomputability]uncomputability [library]
univ [definition, in Kolmogorov.kolmogorov]
univ_exists_kol [lemma, in Kolmogorov.kolmogorov]
univ_upper_bound [lemma, in Kolmogorov.kolmogorov]
upper_bound [lemma, in Kolmogorov.kolmogorov]
V
v_prefixed:193 [binder, in Kolmogorov.random_lower_bound]v:202 [binder, in Kolmogorov.random_lower_bound]
v:214 [binder, in Kolmogorov.random_lower_bound]
X
Xeqdec:51 [binder, in Kolmogorov.listFacts]Xeqdec:87 [binder, in Kolmogorov.listFacts]
x':74 [binder, in Kolmogorov.preliminaries]
x0:150 [binder, in Kolmogorov.random_lower_bound]
x0:151 [binder, in Kolmogorov.random_lower_bound]
x0:152 [binder, in Kolmogorov.random_lower_bound]
x0:153 [binder, in Kolmogorov.random_lower_bound]
x0:154 [binder, in Kolmogorov.random_lower_bound]
x0:155 [binder, in Kolmogorov.random_lower_bound]
x0:156 [binder, in Kolmogorov.random_lower_bound]
x0:157 [binder, in Kolmogorov.random_lower_bound]
x0:158 [binder, in Kolmogorov.random_lower_bound]
x0:159 [binder, in Kolmogorov.random_lower_bound]
x1:150 [binder, in Kolmogorov.listFacts]
x1:152 [binder, in Kolmogorov.listFacts]
x1:167 [binder, in Kolmogorov.random_lower_bound]
x1:169 [binder, in Kolmogorov.random_lower_bound]
x1:34 [binder, in Kolmogorov.preliminaries]
x1:36 [binder, in Kolmogorov.preliminaries]
x1:43 [binder, in Kolmogorov.preliminaries]
x1:45 [binder, in Kolmogorov.preliminaries]
x1:66 [binder, in Kolmogorov.binaryEncoding]
x1:68 [binder, in Kolmogorov.binaryEncoding]
x2:151 [binder, in Kolmogorov.listFacts]
x2:153 [binder, in Kolmogorov.listFacts]
x2:168 [binder, in Kolmogorov.random_lower_bound]
x2:170 [binder, in Kolmogorov.random_lower_bound]
x2:35 [binder, in Kolmogorov.preliminaries]
x2:37 [binder, in Kolmogorov.preliminaries]
x2:44 [binder, in Kolmogorov.preliminaries]
x2:46 [binder, in Kolmogorov.preliminaries]
x2:67 [binder, in Kolmogorov.binaryEncoding]
x2:69 [binder, in Kolmogorov.binaryEncoding]
X:1 [binder, in Kolmogorov.listFacts]
x:10 [binder, in Kolmogorov.randomNumbers]
x:100 [binder, in Kolmogorov.listFacts]
x:104 [binder, in Kolmogorov.listFacts]
x:105 [binder, in Kolmogorov.listFacts]
x:106 [binder, in Kolmogorov.listFacts]
x:11 [binder, in Kolmogorov.random_lower_bound]
x:11 [binder, in Kolmogorov.kolmogorov]
x:111 [binder, in Kolmogorov.listFacts]
x:115 [binder, in Kolmogorov.listFacts]
x:119 [binder, in Kolmogorov.listFacts]
x:12 [binder, in Kolmogorov.uncomputability]
x:12 [binder, in Kolmogorov.random_lower_bound]
x:12 [binder, in Kolmogorov.binaryEncoding]
X:12 [binder, in Kolmogorov.preliminaries]
x:12 [binder, in Kolmogorov.randomNumbers]
x:120 [binder, in Kolmogorov.listFacts]
x:121 [binder, in Kolmogorov.listFacts]
x:124 [binder, in Kolmogorov.listFacts]
x:127 [binder, in Kolmogorov.listFacts]
x:129 [binder, in Kolmogorov.listFacts]
X:13 [binder, in Kolmogorov.listFacts]
x:13 [binder, in Kolmogorov.kolmogorov]
x:130 [binder, in Kolmogorov.listFacts]
x:131 [binder, in Kolmogorov.listFacts]
x:132 [binder, in Kolmogorov.listFacts]
x:133 [binder, in Kolmogorov.listFacts]
x:134 [binder, in Kolmogorov.listFacts]
x:135 [binder, in Kolmogorov.listFacts]
x:135 [binder, in Kolmogorov.random_lower_bound]
x:136 [binder, in Kolmogorov.listFacts]
x:136 [binder, in Kolmogorov.random_lower_bound]
x:137 [binder, in Kolmogorov.listFacts]
x:137 [binder, in Kolmogorov.random_lower_bound]
x:138 [binder, in Kolmogorov.listFacts]
x:138 [binder, in Kolmogorov.random_lower_bound]
x:139 [binder, in Kolmogorov.listFacts]
x:139 [binder, in Kolmogorov.random_lower_bound]
x:140 [binder, in Kolmogorov.listFacts]
x:140 [binder, in Kolmogorov.random_lower_bound]
x:141 [binder, in Kolmogorov.listFacts]
x:141 [binder, in Kolmogorov.random_lower_bound]
x:142 [binder, in Kolmogorov.listFacts]
x:142 [binder, in Kolmogorov.random_lower_bound]
x:143 [binder, in Kolmogorov.listFacts]
x:143 [binder, in Kolmogorov.random_lower_bound]
x:144 [binder, in Kolmogorov.listFacts]
x:145 [binder, in Kolmogorov.listFacts]
x:145 [binder, in Kolmogorov.random_lower_bound]
X:146 [binder, in Kolmogorov.listFacts]
x:146 [binder, in Kolmogorov.random_lower_bound]
x:148 [binder, in Kolmogorov.random_lower_bound]
x:149 [binder, in Kolmogorov.random_lower_bound]
x:15 [binder, in Kolmogorov.listFacts]
x:158 [binder, in Kolmogorov.listFacts]
x:16 [binder, in Kolmogorov.preliminaries]
X:163 [binder, in Kolmogorov.listFacts]
x:165 [binder, in Kolmogorov.random_lower_bound]
x:166 [binder, in Kolmogorov.random_lower_bound]
X:17 [binder, in Kolmogorov.listFacts]
x:17 [binder, in Kolmogorov.binaryEncoding]
X:17 [binder, in Kolmogorov.preliminaries]
x:17 [binder, in Kolmogorov.randomNumbers]
x:177 [binder, in Kolmogorov.random_lower_bound]
x:178 [binder, in Kolmogorov.random_lower_bound]
x:18 [binder, in Kolmogorov.binaryEncoding]
x:182 [binder, in Kolmogorov.random_lower_bound]
x:186 [binder, in Kolmogorov.random_lower_bound]
x:19 [binder, in Kolmogorov.listFacts]
x:19 [binder, in Kolmogorov.kolmogorov]
x:198 [binder, in Kolmogorov.random_lower_bound]
x:2 [binder, in Kolmogorov.kolmogorov]
x:2 [binder, in Kolmogorov.randomNumbers]
x:200 [binder, in Kolmogorov.random_lower_bound]
x:207 [binder, in Kolmogorov.random_lower_bound]
X:21 [binder, in Kolmogorov.listFacts]
x:21 [binder, in Kolmogorov.preliminaries]
x:210 [binder, in Kolmogorov.random_lower_bound]
x:212 [binder, in Kolmogorov.random_lower_bound]
x:219 [binder, in Kolmogorov.random_lower_bound]
x:222 [binder, in Kolmogorov.random_lower_bound]
x:23 [binder, in Kolmogorov.uncomputability]
x:233 [binder, in Kolmogorov.random_lower_bound]
x:234 [binder, in Kolmogorov.random_lower_bound]
x:235 [binder, in Kolmogorov.random_lower_bound]
x:236 [binder, in Kolmogorov.random_lower_bound]
x:24 [binder, in Kolmogorov.listFacts]
x:25 [binder, in Kolmogorov.kolmogorov]
x:26 [binder, in Kolmogorov.binaryEncoding]
x:27 [binder, in Kolmogorov.binaryEncoding]
x:28 [binder, in Kolmogorov.uncomputability]
x:29 [binder, in Kolmogorov.listFacts]
x:29 [binder, in Kolmogorov.randomNumbers]
x:31 [binder, in Kolmogorov.uncomputability]
X:31 [binder, in Kolmogorov.listFacts]
x:32 [binder, in Kolmogorov.listFacts]
x:33 [binder, in Kolmogorov.random_lower_bound]
x:33 [binder, in Kolmogorov.kolmogorov]
x:34 [binder, in Kolmogorov.uncomputability]
X:35 [binder, in Kolmogorov.listFacts]
x:35 [binder, in Kolmogorov.randomNumbers]
x:36 [binder, in Kolmogorov.listFacts]
x:37 [binder, in Kolmogorov.randomNumbers]
x:38 [binder, in Kolmogorov.uncomputability]
x:39 [binder, in Kolmogorov.random_lower_bound]
x:39 [binder, in Kolmogorov.kolmogorov]
x:4 [binder, in Kolmogorov.uncomputability]
X:4 [binder, in Kolmogorov.listFacts]
x:40 [binder, in Kolmogorov.uncomputability]
X:40 [binder, in Kolmogorov.listFacts]
x:41 [binder, in Kolmogorov.uncomputability]
x:42 [binder, in Kolmogorov.preliminaries]
x:43 [binder, in Kolmogorov.uncomputability]
x:43 [binder, in Kolmogorov.binaryEncoding]
x:44 [binder, in Kolmogorov.uncomputability]
X:44 [binder, in Kolmogorov.listFacts]
x:44 [binder, in Kolmogorov.kolmogorov]
x:46 [binder, in Kolmogorov.binaryEncoding]
x:47 [binder, in Kolmogorov.uncomputability]
x:48 [binder, in Kolmogorov.uncomputability]
x:49 [binder, in Kolmogorov.listFacts]
x:49 [binder, in Kolmogorov.binaryEncoding]
x:49 [binder, in Kolmogorov.kolmogorov]
x:5 [binder, in Kolmogorov.listFacts]
X:50 [binder, in Kolmogorov.listFacts]
x:50 [binder, in Kolmogorov.binaryEncoding]
x:54 [binder, in Kolmogorov.kolmogorov]
x:55 [binder, in Kolmogorov.listFacts]
X:56 [binder, in Kolmogorov.listFacts]
x:58 [binder, in Kolmogorov.binaryEncoding]
X:59 [binder, in Kolmogorov.listFacts]
x:6 [binder, in Kolmogorov.randomNumbers]
x:60 [binder, in Kolmogorov.preliminaries]
x:61 [binder, in Kolmogorov.kolmogorov]
x:62 [binder, in Kolmogorov.binaryEncoding]
X:63 [binder, in Kolmogorov.listFacts]
x:63 [binder, in Kolmogorov.randomNumbers]
x:64 [binder, in Kolmogorov.randomNumbers]
x:65 [binder, in Kolmogorov.preliminaries]
x:65 [binder, in Kolmogorov.randomNumbers]
x:66 [binder, in Kolmogorov.preliminaries]
X:67 [binder, in Kolmogorov.listFacts]
X:68 [binder, in Kolmogorov.preliminaries]
x:69 [binder, in Kolmogorov.randomNumbers]
x:7 [binder, in Kolmogorov.uncomputability]
x:7 [binder, in Kolmogorov.random_lower_bound]
X:70 [binder, in Kolmogorov.listFacts]
x:70 [binder, in Kolmogorov.randomNumbers]
x:71 [binder, in Kolmogorov.kolmogorov]
x:71 [binder, in Kolmogorov.randomNumbers]
x:72 [binder, in Kolmogorov.binaryEncoding]
X:73 [binder, in Kolmogorov.listFacts]
x:73 [binder, in Kolmogorov.preliminaries]
x:73 [binder, in Kolmogorov.kolmogorov]
x:74 [binder, in Kolmogorov.kolmogorov]
x:74 [binder, in Kolmogorov.randomNumbers]
x:75 [binder, in Kolmogorov.randomNumbers]
x:76 [binder, in Kolmogorov.binaryEncoding]
x:76 [binder, in Kolmogorov.preliminaries]
x:76 [binder, in Kolmogorov.randomNumbers]
x:78 [binder, in Kolmogorov.listFacts]
x:78 [binder, in Kolmogorov.preliminaries]
x:79 [binder, in Kolmogorov.kolmogorov]
x:79 [binder, in Kolmogorov.randomNumbers]
X:8 [binder, in Kolmogorov.listFacts]
x:8 [binder, in Kolmogorov.random_lower_bound]
X:80 [binder, in Kolmogorov.listFacts]
x:81 [binder, in Kolmogorov.randomNumbers]
X:82 [binder, in Kolmogorov.listFacts]
x:82 [binder, in Kolmogorov.preliminaries]
x:82 [binder, in Kolmogorov.randomNumbers]
x:83 [binder, in Kolmogorov.listFacts]
x:84 [binder, in Kolmogorov.preliminaries]
x:85 [binder, in Kolmogorov.randomNumbers]
X:86 [binder, in Kolmogorov.listFacts]
x:88 [binder, in Kolmogorov.listFacts]
x:9 [binder, in Kolmogorov.listFacts]
x:9 [binder, in Kolmogorov.binaryEncoding]
x:93 [binder, in Kolmogorov.randomNumbers]
x:95 [binder, in Kolmogorov.randomNumbers]
x:96 [binder, in Kolmogorov.listFacts]
x:98 [binder, in Kolmogorov.randomNumbers]
Y
y':6 [binder, in Kolmogorov.kolmogorov]y:10 [binder, in Kolmogorov.listFacts]
y:10 [binder, in Kolmogorov.binaryEncoding]
y:128 [binder, in Kolmogorov.random_lower_bound]
y:13 [binder, in Kolmogorov.binaryEncoding]
y:16 [binder, in Kolmogorov.kolmogorov]
y:25 [binder, in Kolmogorov.preliminaries]
y:29 [binder, in Kolmogorov.preliminaries]
y:37 [binder, in Kolmogorov.listFacts]
y:4 [binder, in Kolmogorov.kolmogorov]
y:56 [binder, in Kolmogorov.binaryEncoding]
y:60 [binder, in Kolmogorov.binaryEncoding]
y:74 [binder, in Kolmogorov.binaryEncoding]
y:75 [binder, in Kolmogorov.binaryEncoding]
y:77 [binder, in Kolmogorov.preliminaries]
y:79 [binder, in Kolmogorov.preliminaries]
y:83 [binder, in Kolmogorov.preliminaries]
y:84 [binder, in Kolmogorov.listFacts]
y:85 [binder, in Kolmogorov.preliminaries]
Z
z:204 [binder, in Kolmogorov.random_lower_bound]z:216 [binder, in Kolmogorov.random_lower_bound]
z:237 [binder, in Kolmogorov.random_lower_bound]
z:239 [binder, in Kolmogorov.random_lower_bound]
z:242 [binder, in Kolmogorov.random_lower_bound]
z:244 [binder, in Kolmogorov.random_lower_bound]
Binder Index
A
a:144 [in Kolmogorov.random_lower_bound]a:147 [in Kolmogorov.random_lower_bound]
A:154 [in Kolmogorov.listFacts]
A:159 [in Kolmogorov.listFacts]
A:2 [in Kolmogorov.listFacts]
A:26 [in Kolmogorov.uncomputability]
A:29 [in Kolmogorov.uncomputability]
A:41 [in Kolmogorov.listFacts]
a:50 [in Kolmogorov.preliminaries]
a:63 [in Kolmogorov.binaryEncoding]
a:70 [in Kolmogorov.binaryEncoding]
B
B:3 [in Kolmogorov.listFacts]B:42 [in Kolmogorov.listFacts]
b:64 [in Kolmogorov.binaryEncoding]
b:71 [in Kolmogorov.binaryEncoding]
C
c':27 [in Kolmogorov.kolmogorov]c:101 [in Kolmogorov.randomNumbers]
c:102 [in Kolmogorov.randomNumbers]
c:11 [in Kolmogorov.randomNumbers]
c:12 [in Kolmogorov.kolmogorov]
c:16 [in Kolmogorov.randomNumbers]
c:18 [in Kolmogorov.kolmogorov]
c:194 [in Kolmogorov.random_lower_bound]
c:26 [in Kolmogorov.kolmogorov]
c:3 [in Kolmogorov.kolmogorov]
c:30 [in Kolmogorov.kolmogorov]
c:32 [in Kolmogorov.uncomputability]
C:43 [in Kolmogorov.listFacts]
c:44 [in Kolmogorov.randomNumbers]
c:51 [in Kolmogorov.binaryEncoding]
c:52 [in Kolmogorov.randomNumbers]
c:53 [in Kolmogorov.randomNumbers]
c:59 [in Kolmogorov.preliminaries]
c:60 [in Kolmogorov.randomNumbers]
c:63 [in Kolmogorov.kolmogorov]
c:64 [in Kolmogorov.preliminaries]
c:66 [in Kolmogorov.randomNumbers]
c:70 [in Kolmogorov.kolmogorov]
c:72 [in Kolmogorov.randomNumbers]
c:77 [in Kolmogorov.randomNumbers]
c:80 [in Kolmogorov.randomNumbers]
c:81 [in Kolmogorov.kolmogorov]
c:83 [in Kolmogorov.randomNumbers]
c:84 [in Kolmogorov.kolmogorov]
c:9 [in Kolmogorov.randomNumbers]
c:99 [in Kolmogorov.randomNumbers]
D
d:192 [in Kolmogorov.random_lower_bound]d:195 [in Kolmogorov.random_lower_bound]
d:201 [in Kolmogorov.random_lower_bound]
d:213 [in Kolmogorov.random_lower_bound]
d:24 [in Kolmogorov.kolmogorov]
E
EqDecision0:155 [in Kolmogorov.listFacts]EqDecision0:160 [in Kolmogorov.listFacts]
eqdec:14 [in Kolmogorov.listFacts]
eqdec:147 [in Kolmogorov.listFacts]
eqdec:18 [in Kolmogorov.listFacts]
eqdec:22 [in Kolmogorov.listFacts]
eqdec:45 [in Kolmogorov.listFacts]
F
f:103 [in Kolmogorov.random_lower_bound]f:107 [in Kolmogorov.random_lower_bound]
f:108 [in Kolmogorov.listFacts]
f:112 [in Kolmogorov.random_lower_bound]
f:117 [in Kolmogorov.random_lower_bound]
f:123 [in Kolmogorov.random_lower_bound]
f:130 [in Kolmogorov.random_lower_bound]
f:14 [in Kolmogorov.random_lower_bound]
f:161 [in Kolmogorov.random_lower_bound]
f:172 [in Kolmogorov.random_lower_bound]
f:180 [in Kolmogorov.random_lower_bound]
f:188 [in Kolmogorov.random_lower_bound]
f:19 [in Kolmogorov.random_lower_bound]
f:199 [in Kolmogorov.random_lower_bound]
f:2 [in Kolmogorov.random_lower_bound]
f:211 [in Kolmogorov.random_lower_bound]
f:24 [in Kolmogorov.random_lower_bound]
f:31 [in Kolmogorov.kolmogorov]
f:32 [in Kolmogorov.random_lower_bound]
f:35 [in Kolmogorov.random_lower_bound]
f:37 [in Kolmogorov.uncomputability]
f:39 [in Kolmogorov.preliminaries]
f:41 [in Kolmogorov.random_lower_bound]
f:45 [in Kolmogorov.randomNumbers]
f:46 [in Kolmogorov.random_lower_bound]
f:52 [in Kolmogorov.random_lower_bound]
f:58 [in Kolmogorov.random_lower_bound]
f:58 [in Kolmogorov.preliminaries]
f:63 [in Kolmogorov.preliminaries]
f:64 [in Kolmogorov.random_lower_bound]
f:70 [in Kolmogorov.random_lower_bound]
f:70 [in Kolmogorov.preliminaries]
f:76 [in Kolmogorov.random_lower_bound]
f:8 [in Kolmogorov.preliminaries]
f:81 [in Kolmogorov.random_lower_bound]
f:83 [in Kolmogorov.kolmogorov]
f:86 [in Kolmogorov.random_lower_bound]
f:9 [in Kolmogorov.kolmogorov]
f:91 [in Kolmogorov.random_lower_bound]
f:93 [in Kolmogorov.listFacts]
f:97 [in Kolmogorov.random_lower_bound]
G
g:10 [in Kolmogorov.kolmogorov]H
H:183 [in Kolmogorov.random_lower_bound]H:69 [in Kolmogorov.preliminaries]
I
input:43 [in Kolmogorov.kolmogorov]input:48 [in Kolmogorov.kolmogorov]
input:53 [in Kolmogorov.kolmogorov]
input:58 [in Kolmogorov.kolmogorov]
i:3 [in Kolmogorov.randomNumbers]
i:30 [in Kolmogorov.randomNumbers]
i:32 [in Kolmogorov.randomNumbers]
i:34 [in Kolmogorov.kolmogorov]
i:39 [in Kolmogorov.randomNumbers]
i:42 [in Kolmogorov.randomNumbers]
i:47 [in Kolmogorov.randomNumbers]
i:50 [in Kolmogorov.randomNumbers]
i:57 [in Kolmogorov.randomNumbers]
i:60 [in Kolmogorov.kolmogorov]
i:7 [in Kolmogorov.randomNumbers]
i:78 [in Kolmogorov.kolmogorov]
J
j:64 [in Kolmogorov.kolmogorov]j:65 [in Kolmogorov.kolmogorov]
j:67 [in Kolmogorov.kolmogorov]
j:68 [in Kolmogorov.kolmogorov]
K
kc':21 [in Kolmogorov.kolmogorov]kc:13 [in Kolmogorov.randomNumbers]
kc:14 [in Kolmogorov.randomNumbers]
kc:15 [in Kolmogorov.randomNumbers]
kc:18 [in Kolmogorov.randomNumbers]
kc:19 [in Kolmogorov.randomNumbers]
kc:20 [in Kolmogorov.kolmogorov]
kc:20 [in Kolmogorov.randomNumbers]
kc:21 [in Kolmogorov.randomNumbers]
kc:22 [in Kolmogorov.randomNumbers]
kc:23 [in Kolmogorov.randomNumbers]
kc:24 [in Kolmogorov.randomNumbers]
kc:25 [in Kolmogorov.randomNumbers]
kc:26 [in Kolmogorov.randomNumbers]
kc:27 [in Kolmogorov.randomNumbers]
kc:35 [in Kolmogorov.uncomputability]
k':87 [in Kolmogorov.preliminaries]
k:14 [in Kolmogorov.kolmogorov]
k:15 [in Kolmogorov.kolmogorov]
k:196 [in Kolmogorov.random_lower_bound]
k:231 [in Kolmogorov.random_lower_bound]
k:232 [in Kolmogorov.random_lower_bound]
k:24 [in Kolmogorov.preliminaries]
k:28 [in Kolmogorov.preliminaries]
k:32 [in Kolmogorov.kolmogorov]
k:47 [in Kolmogorov.binaryEncoding]
k:54 [in Kolmogorov.randomNumbers]
k:62 [in Kolmogorov.randomNumbers]
k:67 [in Kolmogorov.randomNumbers]
k:72 [in Kolmogorov.kolmogorov]
k:73 [in Kolmogorov.randomNumbers]
k:78 [in Kolmogorov.binaryEncoding]
k:78 [in Kolmogorov.randomNumbers]
k:86 [in Kolmogorov.preliminaries]
k:86 [in Kolmogorov.kolmogorov]
L
L':103 [in Kolmogorov.listFacts]L':110 [in Kolmogorov.listFacts]
L':114 [in Kolmogorov.listFacts]
L':118 [in Kolmogorov.listFacts]
L':149 [in Kolmogorov.listFacts]
L':15 [in Kolmogorov.binaryEncoding]
l':15 [in Kolmogorov.preliminaries]
L':157 [in Kolmogorov.listFacts]
L':162 [in Kolmogorov.listFacts]
l':197 [in Kolmogorov.random_lower_bound]
l':20 [in Kolmogorov.preliminaries]
l':22 [in Kolmogorov.uncomputability]
l':48 [in Kolmogorov.listFacts]
L':56 [in Kolmogorov.randomNumbers]
l':61 [in Kolmogorov.randomNumbers]
l':68 [in Kolmogorov.randomNumbers]
L':91 [in Kolmogorov.listFacts]
L':95 [in Kolmogorov.listFacts]
L':99 [in Kolmogorov.listFacts]
L:10 [in Kolmogorov.random_lower_bound]
L:102 [in Kolmogorov.listFacts]
L:109 [in Kolmogorov.listFacts]
L:11 [in Kolmogorov.uncomputability]
L:113 [in Kolmogorov.listFacts]
L:117 [in Kolmogorov.listFacts]
L:12 [in Kolmogorov.listFacts]
L:123 [in Kolmogorov.listFacts]
L:125 [in Kolmogorov.listFacts]
L:128 [in Kolmogorov.listFacts]
L:133 [in Kolmogorov.random_lower_bound]
L:14 [in Kolmogorov.binaryEncoding]
l:14 [in Kolmogorov.preliminaries]
L:148 [in Kolmogorov.listFacts]
L:156 [in Kolmogorov.listFacts]
L:16 [in Kolmogorov.listFacts]
L:16 [in Kolmogorov.binaryEncoding]
L:161 [in Kolmogorov.listFacts]
L:165 [in Kolmogorov.listFacts]
L:184 [in Kolmogorov.random_lower_bound]
L:19 [in Kolmogorov.binaryEncoding]
l:19 [in Kolmogorov.preliminaries]
l:2 [in Kolmogorov.uncomputability]
l:20 [in Kolmogorov.uncomputability]
L:20 [in Kolmogorov.listFacts]
L:206 [in Kolmogorov.random_lower_bound]
L:209 [in Kolmogorov.random_lower_bound]
L:21 [in Kolmogorov.uncomputability]
L:218 [in Kolmogorov.random_lower_bound]
L:221 [in Kolmogorov.random_lower_bound]
L:24 [in Kolmogorov.uncomputability]
L:25 [in Kolmogorov.listFacts]
L:25 [in Kolmogorov.binaryEncoding]
L:26 [in Kolmogorov.listFacts]
L:29 [in Kolmogorov.binaryEncoding]
L:3 [in Kolmogorov.uncomputability]
l:3 [in Kolmogorov.binaryEncoding]
L:30 [in Kolmogorov.listFacts]
L:34 [in Kolmogorov.listFacts]
L:37 [in Kolmogorov.binaryEncoding]
L:39 [in Kolmogorov.listFacts]
l:41 [in Kolmogorov.binaryEncoding]
L:42 [in Kolmogorov.binaryEncoding]
l:44 [in Kolmogorov.binaryEncoding]
L:45 [in Kolmogorov.binaryEncoding]
L:46 [in Kolmogorov.listFacts]
l:47 [in Kolmogorov.listFacts]
L:52 [in Kolmogorov.listFacts]
L:55 [in Kolmogorov.randomNumbers]
L:57 [in Kolmogorov.binaryEncoding]
L:58 [in Kolmogorov.listFacts]
L:6 [in Kolmogorov.uncomputability]
L:61 [in Kolmogorov.binaryEncoding]
L:62 [in Kolmogorov.listFacts]
L:65 [in Kolmogorov.binaryEncoding]
L:66 [in Kolmogorov.listFacts]
L:69 [in Kolmogorov.listFacts]
L:7 [in Kolmogorov.listFacts]
L:72 [in Kolmogorov.listFacts]
L:74 [in Kolmogorov.random_lower_bound]
L:75 [in Kolmogorov.listFacts]
L:85 [in Kolmogorov.listFacts]
L:89 [in Kolmogorov.listFacts]
L:9 [in Kolmogorov.random_lower_bound]
L:94 [in Kolmogorov.listFacts]
L:98 [in Kolmogorov.listFacts]
M
model:47 [in Kolmogorov.preliminaries]m':100 [in Kolmogorov.random_lower_bound]
m':120 [in Kolmogorov.random_lower_bound]
m':95 [in Kolmogorov.random_lower_bound]
m:10 [in Kolmogorov.uncomputability]
m:101 [in Kolmogorov.random_lower_bound]
m:108 [in Kolmogorov.random_lower_bound]
m:115 [in Kolmogorov.random_lower_bound]
m:121 [in Kolmogorov.random_lower_bound]
m:124 [in Kolmogorov.random_lower_bound]
m:131 [in Kolmogorov.random_lower_bound]
m:15 [in Kolmogorov.random_lower_bound]
m:162 [in Kolmogorov.random_lower_bound]
m:173 [in Kolmogorov.random_lower_bound]
m:189 [in Kolmogorov.random_lower_bound]
m:20 [in Kolmogorov.random_lower_bound]
m:21 [in Kolmogorov.binaryEncoding]
m:23 [in Kolmogorov.kolmogorov]
m:25 [in Kolmogorov.random_lower_bound]
m:29 [in Kolmogorov.random_lower_bound]
m:3 [in Kolmogorov.random_lower_bound]
m:32 [in Kolmogorov.preliminaries]
m:33 [in Kolmogorov.uncomputability]
m:36 [in Kolmogorov.random_lower_bound]
m:39 [in Kolmogorov.uncomputability]
m:40 [in Kolmogorov.preliminaries]
m:42 [in Kolmogorov.uncomputability]
m:42 [in Kolmogorov.random_lower_bound]
m:47 [in Kolmogorov.random_lower_bound]
m:49 [in Kolmogorov.uncomputability]
m:5 [in Kolmogorov.uncomputability]
m:50 [in Kolmogorov.uncomputability]
m:51 [in Kolmogorov.uncomputability]
m:52 [in Kolmogorov.uncomputability]
m:53 [in Kolmogorov.uncomputability]
m:53 [in Kolmogorov.random_lower_bound]
m:54 [in Kolmogorov.uncomputability]
m:59 [in Kolmogorov.random_lower_bound]
m:65 [in Kolmogorov.random_lower_bound]
m:73 [in Kolmogorov.random_lower_bound]
m:77 [in Kolmogorov.random_lower_bound]
m:82 [in Kolmogorov.random_lower_bound]
m:85 [in Kolmogorov.kolmogorov]
m:86 [in Kolmogorov.randomNumbers]
m:87 [in Kolmogorov.random_lower_bound]
m:88 [in Kolmogorov.randomNumbers]
m:90 [in Kolmogorov.randomNumbers]
m:91 [in Kolmogorov.randomNumbers]
m:94 [in Kolmogorov.random_lower_bound]
N
n':61 [in Kolmogorov.listFacts]n':64 [in Kolmogorov.listFacts]
n':72 [in Kolmogorov.preliminaries]
n1:45 [in Kolmogorov.uncomputability]
n1:46 [in Kolmogorov.uncomputability]
n:1 [in Kolmogorov.uncomputability]
n:1 [in Kolmogorov.kolmogorov]
n:1 [in Kolmogorov.randomNumbers]
n:10 [in Kolmogorov.preliminaries]
n:101 [in Kolmogorov.listFacts]
n:104 [in Kolmogorov.random_lower_bound]
n:109 [in Kolmogorov.random_lower_bound]
n:11 [in Kolmogorov.listFacts]
n:112 [in Kolmogorov.listFacts]
n:113 [in Kolmogorov.random_lower_bound]
n:116 [in Kolmogorov.listFacts]
n:118 [in Kolmogorov.random_lower_bound]
n:122 [in Kolmogorov.listFacts]
n:125 [in Kolmogorov.random_lower_bound]
n:126 [in Kolmogorov.listFacts]
n:132 [in Kolmogorov.random_lower_bound]
n:16 [in Kolmogorov.random_lower_bound]
n:163 [in Kolmogorov.random_lower_bound]
n:164 [in Kolmogorov.listFacts]
n:174 [in Kolmogorov.random_lower_bound]
n:181 [in Kolmogorov.random_lower_bound]
n:19 [in Kolmogorov.uncomputability]
n:190 [in Kolmogorov.random_lower_bound]
n:20 [in Kolmogorov.binaryEncoding]
n:203 [in Kolmogorov.random_lower_bound]
n:21 [in Kolmogorov.random_lower_bound]
n:215 [in Kolmogorov.random_lower_bound]
n:22 [in Kolmogorov.binaryEncoding]
n:22 [in Kolmogorov.kolmogorov]
n:223 [in Kolmogorov.random_lower_bound]
n:224 [in Kolmogorov.random_lower_bound]
n:225 [in Kolmogorov.random_lower_bound]
n:226 [in Kolmogorov.random_lower_bound]
n:23 [in Kolmogorov.preliminaries]
n:25 [in Kolmogorov.uncomputability]
n:26 [in Kolmogorov.random_lower_bound]
n:26 [in Kolmogorov.preliminaries]
n:27 [in Kolmogorov.uncomputability]
n:27 [in Kolmogorov.preliminaries]
n:28 [in Kolmogorov.binaryEncoding]
n:28 [in Kolmogorov.randomNumbers]
n:30 [in Kolmogorov.uncomputability]
n:30 [in Kolmogorov.random_lower_bound]
n:30 [in Kolmogorov.binaryEncoding]
n:30 [in Kolmogorov.preliminaries]
n:31 [in Kolmogorov.binaryEncoding]
n:32 [in Kolmogorov.binaryEncoding]
n:33 [in Kolmogorov.listFacts]
n:33 [in Kolmogorov.binaryEncoding]
n:33 [in Kolmogorov.preliminaries]
n:34 [in Kolmogorov.randomNumbers]
n:36 [in Kolmogorov.uncomputability]
n:36 [in Kolmogorov.binaryEncoding]
n:36 [in Kolmogorov.randomNumbers]
n:37 [in Kolmogorov.random_lower_bound]
n:38 [in Kolmogorov.listFacts]
n:38 [in Kolmogorov.binaryEncoding]
n:38 [in Kolmogorov.kolmogorov]
n:39 [in Kolmogorov.binaryEncoding]
n:4 [in Kolmogorov.random_lower_bound]
n:40 [in Kolmogorov.binaryEncoding]
n:41 [in Kolmogorov.preliminaries]
n:43 [in Kolmogorov.random_lower_bound]
n:48 [in Kolmogorov.random_lower_bound]
n:48 [in Kolmogorov.binaryEncoding]
n:5 [in Kolmogorov.binaryEncoding]
n:5 [in Kolmogorov.randomNumbers]
n:52 [in Kolmogorov.binaryEncoding]
n:53 [in Kolmogorov.binaryEncoding]
n:54 [in Kolmogorov.random_lower_bound]
n:54 [in Kolmogorov.binaryEncoding]
n:55 [in Kolmogorov.binaryEncoding]
n:57 [in Kolmogorov.listFacts]
n:59 [in Kolmogorov.binaryEncoding]
n:59 [in Kolmogorov.kolmogorov]
n:6 [in Kolmogorov.listFacts]
n:60 [in Kolmogorov.listFacts]
n:60 [in Kolmogorov.random_lower_bound]
n:65 [in Kolmogorov.listFacts]
n:66 [in Kolmogorov.random_lower_bound]
n:68 [in Kolmogorov.listFacts]
n:7 [in Kolmogorov.binaryEncoding]
n:71 [in Kolmogorov.listFacts]
n:71 [in Kolmogorov.random_lower_bound]
n:71 [in Kolmogorov.preliminaries]
n:73 [in Kolmogorov.binaryEncoding]
n:74 [in Kolmogorov.listFacts]
n:76 [in Kolmogorov.listFacts]
n:77 [in Kolmogorov.listFacts]
n:77 [in Kolmogorov.binaryEncoding]
n:77 [in Kolmogorov.kolmogorov]
n:78 [in Kolmogorov.random_lower_bound]
n:79 [in Kolmogorov.listFacts]
n:79 [in Kolmogorov.binaryEncoding]
n:8 [in Kolmogorov.kolmogorov]
n:81 [in Kolmogorov.listFacts]
n:82 [in Kolmogorov.kolmogorov]
n:83 [in Kolmogorov.random_lower_bound]
n:87 [in Kolmogorov.randomNumbers]
n:88 [in Kolmogorov.random_lower_bound]
n:89 [in Kolmogorov.randomNumbers]
n:9 [in Kolmogorov.preliminaries]
n:90 [in Kolmogorov.listFacts]
n:92 [in Kolmogorov.random_lower_bound]
n:92 [in Kolmogorov.randomNumbers]
n:94 [in Kolmogorov.randomNumbers]
n:97 [in Kolmogorov.listFacts]
n:98 [in Kolmogorov.random_lower_bound]
O
o:176 [in Kolmogorov.random_lower_bound]o:59 [in Kolmogorov.randomNumbers]
P
program:42 [in Kolmogorov.kolmogorov]program:47 [in Kolmogorov.kolmogorov]
program:52 [in Kolmogorov.kolmogorov]
program:57 [in Kolmogorov.kolmogorov]
p:1 [in Kolmogorov.random_lower_bound]
p:100 [in Kolmogorov.randomNumbers]
p:102 [in Kolmogorov.random_lower_bound]
p:106 [in Kolmogorov.random_lower_bound]
p:107 [in Kolmogorov.listFacts]
P:11 [in Kolmogorov.preliminaries]
p:111 [in Kolmogorov.random_lower_bound]
p:116 [in Kolmogorov.random_lower_bound]
p:122 [in Kolmogorov.random_lower_bound]
p:129 [in Kolmogorov.random_lower_bound]
p:13 [in Kolmogorov.random_lower_bound]
p:13 [in Kolmogorov.preliminaries]
p:160 [in Kolmogorov.random_lower_bound]
p:171 [in Kolmogorov.random_lower_bound]
p:179 [in Kolmogorov.random_lower_bound]
p:18 [in Kolmogorov.random_lower_bound]
p:18 [in Kolmogorov.preliminaries]
p:187 [in Kolmogorov.random_lower_bound]
P:2 [in Kolmogorov.preliminaries]
p:22 [in Kolmogorov.preliminaries]
p:23 [in Kolmogorov.listFacts]
p:23 [in Kolmogorov.random_lower_bound]
p:28 [in Kolmogorov.random_lower_bound]
P:3 [in Kolmogorov.preliminaries]
p:34 [in Kolmogorov.random_lower_bound]
p:38 [in Kolmogorov.randomNumbers]
p:40 [in Kolmogorov.random_lower_bound]
p:41 [in Kolmogorov.randomNumbers]
p:45 [in Kolmogorov.random_lower_bound]
p:46 [in Kolmogorov.randomNumbers]
p:49 [in Kolmogorov.randomNumbers]
P:5 [in Kolmogorov.preliminaries]
p:51 [in Kolmogorov.random_lower_bound]
p:57 [in Kolmogorov.random_lower_bound]
p:63 [in Kolmogorov.random_lower_bound]
p:69 [in Kolmogorov.random_lower_bound]
p:75 [in Kolmogorov.random_lower_bound]
p:75 [in Kolmogorov.preliminaries]
p:80 [in Kolmogorov.random_lower_bound]
p:85 [in Kolmogorov.random_lower_bound]
p:90 [in Kolmogorov.random_lower_bound]
p:92 [in Kolmogorov.listFacts]
p:96 [in Kolmogorov.random_lower_bound]
p:96 [in Kolmogorov.randomNumbers]
Q
Q:1 [in Kolmogorov.preliminaries]q:31 [in Kolmogorov.preliminaries]
q:38 [in Kolmogorov.preliminaries]
Q:4 [in Kolmogorov.preliminaries]
Q:6 [in Kolmogorov.preliminaries]
Q:7 [in Kolmogorov.preliminaries]
q:84 [in Kolmogorov.randomNumbers]
q:97 [in Kolmogorov.randomNumbers]
R
r:14 [in Kolmogorov.uncomputability]r:16 [in Kolmogorov.uncomputability]
r:18 [in Kolmogorov.uncomputability]
r:9 [in Kolmogorov.uncomputability]
S
size:41 [in Kolmogorov.kolmogorov]size:46 [in Kolmogorov.kolmogorov]
size:51 [in Kolmogorov.kolmogorov]
size:56 [in Kolmogorov.kolmogorov]
start:53 [in Kolmogorov.listFacts]
s':127 [in Kolmogorov.random_lower_bound]
s':227 [in Kolmogorov.random_lower_bound]
s':228 [in Kolmogorov.random_lower_bound]
s':50 [in Kolmogorov.random_lower_bound]
s':56 [in Kolmogorov.random_lower_bound]
s':62 [in Kolmogorov.random_lower_bound]
s':68 [in Kolmogorov.random_lower_bound]
s:105 [in Kolmogorov.random_lower_bound]
s:110 [in Kolmogorov.random_lower_bound]
s:114 [in Kolmogorov.random_lower_bound]
s:119 [in Kolmogorov.random_lower_bound]
s:126 [in Kolmogorov.random_lower_bound]
s:13 [in Kolmogorov.uncomputability]
s:134 [in Kolmogorov.random_lower_bound]
s:15 [in Kolmogorov.uncomputability]
s:164 [in Kolmogorov.random_lower_bound]
s:17 [in Kolmogorov.uncomputability]
s:17 [in Kolmogorov.random_lower_bound]
s:17 [in Kolmogorov.kolmogorov]
s:175 [in Kolmogorov.random_lower_bound]
s:185 [in Kolmogorov.random_lower_bound]
s:191 [in Kolmogorov.random_lower_bound]
s:205 [in Kolmogorov.random_lower_bound]
s:208 [in Kolmogorov.random_lower_bound]
s:217 [in Kolmogorov.random_lower_bound]
s:22 [in Kolmogorov.random_lower_bound]
s:220 [in Kolmogorov.random_lower_bound]
s:229 [in Kolmogorov.random_lower_bound]
s:230 [in Kolmogorov.random_lower_bound]
s:238 [in Kolmogorov.random_lower_bound]
s:240 [in Kolmogorov.random_lower_bound]
s:241 [in Kolmogorov.random_lower_bound]
s:243 [in Kolmogorov.random_lower_bound]
s:27 [in Kolmogorov.random_lower_bound]
s:28 [in Kolmogorov.kolmogorov]
s:29 [in Kolmogorov.kolmogorov]
s:31 [in Kolmogorov.random_lower_bound]
s:31 [in Kolmogorov.randomNumbers]
s:33 [in Kolmogorov.randomNumbers]
s:35 [in Kolmogorov.kolmogorov]
s:36 [in Kolmogorov.kolmogorov]
s:37 [in Kolmogorov.kolmogorov]
s:38 [in Kolmogorov.random_lower_bound]
s:4 [in Kolmogorov.randomNumbers]
s:40 [in Kolmogorov.kolmogorov]
s:40 [in Kolmogorov.randomNumbers]
s:43 [in Kolmogorov.randomNumbers]
s:44 [in Kolmogorov.random_lower_bound]
s:45 [in Kolmogorov.kolmogorov]
s:48 [in Kolmogorov.randomNumbers]
s:49 [in Kolmogorov.random_lower_bound]
s:5 [in Kolmogorov.random_lower_bound]
s:5 [in Kolmogorov.kolmogorov]
s:50 [in Kolmogorov.kolmogorov]
s:51 [in Kolmogorov.preliminaries]
s:51 [in Kolmogorov.randomNumbers]
s:52 [in Kolmogorov.preliminaries]
s:55 [in Kolmogorov.random_lower_bound]
s:55 [in Kolmogorov.kolmogorov]
s:58 [in Kolmogorov.randomNumbers]
s:61 [in Kolmogorov.random_lower_bound]
s:61 [in Kolmogorov.preliminaries]
s:62 [in Kolmogorov.kolmogorov]
s:66 [in Kolmogorov.kolmogorov]
s:67 [in Kolmogorov.random_lower_bound]
s:69 [in Kolmogorov.kolmogorov]
s:7 [in Kolmogorov.kolmogorov]
s:72 [in Kolmogorov.random_lower_bound]
s:75 [in Kolmogorov.kolmogorov]
s:76 [in Kolmogorov.kolmogorov]
s:79 [in Kolmogorov.random_lower_bound]
s:8 [in Kolmogorov.uncomputability]
s:8 [in Kolmogorov.randomNumbers]
s:80 [in Kolmogorov.kolmogorov]
s:84 [in Kolmogorov.random_lower_bound]
s:89 [in Kolmogorov.random_lower_bound]
s:93 [in Kolmogorov.random_lower_bound]
s:99 [in Kolmogorov.random_lower_bound]
T
T'':57 [in Kolmogorov.preliminaries]T':49 [in Kolmogorov.preliminaries]
T':54 [in Kolmogorov.preliminaries]
T':56 [in Kolmogorov.preliminaries]
T:48 [in Kolmogorov.preliminaries]
T:53 [in Kolmogorov.preliminaries]
T:55 [in Kolmogorov.preliminaries]
V
v_prefixed:193 [in Kolmogorov.random_lower_bound]v:202 [in Kolmogorov.random_lower_bound]
v:214 [in Kolmogorov.random_lower_bound]
X
Xeqdec:51 [in Kolmogorov.listFacts]Xeqdec:87 [in Kolmogorov.listFacts]
x':74 [in Kolmogorov.preliminaries]
x0:150 [in Kolmogorov.random_lower_bound]
x0:151 [in Kolmogorov.random_lower_bound]
x0:152 [in Kolmogorov.random_lower_bound]
x0:153 [in Kolmogorov.random_lower_bound]
x0:154 [in Kolmogorov.random_lower_bound]
x0:155 [in Kolmogorov.random_lower_bound]
x0:156 [in Kolmogorov.random_lower_bound]
x0:157 [in Kolmogorov.random_lower_bound]
x0:158 [in Kolmogorov.random_lower_bound]
x0:159 [in Kolmogorov.random_lower_bound]
x1:150 [in Kolmogorov.listFacts]
x1:152 [in Kolmogorov.listFacts]
x1:167 [in Kolmogorov.random_lower_bound]
x1:169 [in Kolmogorov.random_lower_bound]
x1:34 [in Kolmogorov.preliminaries]
x1:36 [in Kolmogorov.preliminaries]
x1:43 [in Kolmogorov.preliminaries]
x1:45 [in Kolmogorov.preliminaries]
x1:66 [in Kolmogorov.binaryEncoding]
x1:68 [in Kolmogorov.binaryEncoding]
x2:151 [in Kolmogorov.listFacts]
x2:153 [in Kolmogorov.listFacts]
x2:168 [in Kolmogorov.random_lower_bound]
x2:170 [in Kolmogorov.random_lower_bound]
x2:35 [in Kolmogorov.preliminaries]
x2:37 [in Kolmogorov.preliminaries]
x2:44 [in Kolmogorov.preliminaries]
x2:46 [in Kolmogorov.preliminaries]
x2:67 [in Kolmogorov.binaryEncoding]
x2:69 [in Kolmogorov.binaryEncoding]
X:1 [in Kolmogorov.listFacts]
x:10 [in Kolmogorov.randomNumbers]
x:100 [in Kolmogorov.listFacts]
x:104 [in Kolmogorov.listFacts]
x:105 [in Kolmogorov.listFacts]
x:106 [in Kolmogorov.listFacts]
x:11 [in Kolmogorov.random_lower_bound]
x:11 [in Kolmogorov.kolmogorov]
x:111 [in Kolmogorov.listFacts]
x:115 [in Kolmogorov.listFacts]
x:119 [in Kolmogorov.listFacts]
x:12 [in Kolmogorov.uncomputability]
x:12 [in Kolmogorov.random_lower_bound]
x:12 [in Kolmogorov.binaryEncoding]
X:12 [in Kolmogorov.preliminaries]
x:12 [in Kolmogorov.randomNumbers]
x:120 [in Kolmogorov.listFacts]
x:121 [in Kolmogorov.listFacts]
x:124 [in Kolmogorov.listFacts]
x:127 [in Kolmogorov.listFacts]
x:129 [in Kolmogorov.listFacts]
X:13 [in Kolmogorov.listFacts]
x:13 [in Kolmogorov.kolmogorov]
x:130 [in Kolmogorov.listFacts]
x:131 [in Kolmogorov.listFacts]
x:132 [in Kolmogorov.listFacts]
x:133 [in Kolmogorov.listFacts]
x:134 [in Kolmogorov.listFacts]
x:135 [in Kolmogorov.listFacts]
x:135 [in Kolmogorov.random_lower_bound]
x:136 [in Kolmogorov.listFacts]
x:136 [in Kolmogorov.random_lower_bound]
x:137 [in Kolmogorov.listFacts]
x:137 [in Kolmogorov.random_lower_bound]
x:138 [in Kolmogorov.listFacts]
x:138 [in Kolmogorov.random_lower_bound]
x:139 [in Kolmogorov.listFacts]
x:139 [in Kolmogorov.random_lower_bound]
x:140 [in Kolmogorov.listFacts]
x:140 [in Kolmogorov.random_lower_bound]
x:141 [in Kolmogorov.listFacts]
x:141 [in Kolmogorov.random_lower_bound]
x:142 [in Kolmogorov.listFacts]
x:142 [in Kolmogorov.random_lower_bound]
x:143 [in Kolmogorov.listFacts]
x:143 [in Kolmogorov.random_lower_bound]
x:144 [in Kolmogorov.listFacts]
x:145 [in Kolmogorov.listFacts]
x:145 [in Kolmogorov.random_lower_bound]
X:146 [in Kolmogorov.listFacts]
x:146 [in Kolmogorov.random_lower_bound]
x:148 [in Kolmogorov.random_lower_bound]
x:149 [in Kolmogorov.random_lower_bound]
x:15 [in Kolmogorov.listFacts]
x:158 [in Kolmogorov.listFacts]
x:16 [in Kolmogorov.preliminaries]
X:163 [in Kolmogorov.listFacts]
x:165 [in Kolmogorov.random_lower_bound]
x:166 [in Kolmogorov.random_lower_bound]
X:17 [in Kolmogorov.listFacts]
x:17 [in Kolmogorov.binaryEncoding]
X:17 [in Kolmogorov.preliminaries]
x:17 [in Kolmogorov.randomNumbers]
x:177 [in Kolmogorov.random_lower_bound]
x:178 [in Kolmogorov.random_lower_bound]
x:18 [in Kolmogorov.binaryEncoding]
x:182 [in Kolmogorov.random_lower_bound]
x:186 [in Kolmogorov.random_lower_bound]
x:19 [in Kolmogorov.listFacts]
x:19 [in Kolmogorov.kolmogorov]
x:198 [in Kolmogorov.random_lower_bound]
x:2 [in Kolmogorov.kolmogorov]
x:2 [in Kolmogorov.randomNumbers]
x:200 [in Kolmogorov.random_lower_bound]
x:207 [in Kolmogorov.random_lower_bound]
X:21 [in Kolmogorov.listFacts]
x:21 [in Kolmogorov.preliminaries]
x:210 [in Kolmogorov.random_lower_bound]
x:212 [in Kolmogorov.random_lower_bound]
x:219 [in Kolmogorov.random_lower_bound]
x:222 [in Kolmogorov.random_lower_bound]
x:23 [in Kolmogorov.uncomputability]
x:233 [in Kolmogorov.random_lower_bound]
x:234 [in Kolmogorov.random_lower_bound]
x:235 [in Kolmogorov.random_lower_bound]
x:236 [in Kolmogorov.random_lower_bound]
x:24 [in Kolmogorov.listFacts]
x:25 [in Kolmogorov.kolmogorov]
x:26 [in Kolmogorov.binaryEncoding]
x:27 [in Kolmogorov.binaryEncoding]
x:28 [in Kolmogorov.uncomputability]
x:29 [in Kolmogorov.listFacts]
x:29 [in Kolmogorov.randomNumbers]
x:31 [in Kolmogorov.uncomputability]
X:31 [in Kolmogorov.listFacts]
x:32 [in Kolmogorov.listFacts]
x:33 [in Kolmogorov.random_lower_bound]
x:33 [in Kolmogorov.kolmogorov]
x:34 [in Kolmogorov.uncomputability]
X:35 [in Kolmogorov.listFacts]
x:35 [in Kolmogorov.randomNumbers]
x:36 [in Kolmogorov.listFacts]
x:37 [in Kolmogorov.randomNumbers]
x:38 [in Kolmogorov.uncomputability]
x:39 [in Kolmogorov.random_lower_bound]
x:39 [in Kolmogorov.kolmogorov]
x:4 [in Kolmogorov.uncomputability]
X:4 [in Kolmogorov.listFacts]
x:40 [in Kolmogorov.uncomputability]
X:40 [in Kolmogorov.listFacts]
x:41 [in Kolmogorov.uncomputability]
x:42 [in Kolmogorov.preliminaries]
x:43 [in Kolmogorov.uncomputability]
x:43 [in Kolmogorov.binaryEncoding]
x:44 [in Kolmogorov.uncomputability]
X:44 [in Kolmogorov.listFacts]
x:44 [in Kolmogorov.kolmogorov]
x:46 [in Kolmogorov.binaryEncoding]
x:47 [in Kolmogorov.uncomputability]
x:48 [in Kolmogorov.uncomputability]
x:49 [in Kolmogorov.listFacts]
x:49 [in Kolmogorov.binaryEncoding]
x:49 [in Kolmogorov.kolmogorov]
x:5 [in Kolmogorov.listFacts]
X:50 [in Kolmogorov.listFacts]
x:50 [in Kolmogorov.binaryEncoding]
x:54 [in Kolmogorov.kolmogorov]
x:55 [in Kolmogorov.listFacts]
X:56 [in Kolmogorov.listFacts]
x:58 [in Kolmogorov.binaryEncoding]
X:59 [in Kolmogorov.listFacts]
x:6 [in Kolmogorov.randomNumbers]
x:60 [in Kolmogorov.preliminaries]
x:61 [in Kolmogorov.kolmogorov]
x:62 [in Kolmogorov.binaryEncoding]
X:63 [in Kolmogorov.listFacts]
x:63 [in Kolmogorov.randomNumbers]
x:64 [in Kolmogorov.randomNumbers]
x:65 [in Kolmogorov.preliminaries]
x:65 [in Kolmogorov.randomNumbers]
x:66 [in Kolmogorov.preliminaries]
X:67 [in Kolmogorov.listFacts]
X:68 [in Kolmogorov.preliminaries]
x:69 [in Kolmogorov.randomNumbers]
x:7 [in Kolmogorov.uncomputability]
x:7 [in Kolmogorov.random_lower_bound]
X:70 [in Kolmogorov.listFacts]
x:70 [in Kolmogorov.randomNumbers]
x:71 [in Kolmogorov.kolmogorov]
x:71 [in Kolmogorov.randomNumbers]
x:72 [in Kolmogorov.binaryEncoding]
X:73 [in Kolmogorov.listFacts]
x:73 [in Kolmogorov.preliminaries]
x:73 [in Kolmogorov.kolmogorov]
x:74 [in Kolmogorov.kolmogorov]
x:74 [in Kolmogorov.randomNumbers]
x:75 [in Kolmogorov.randomNumbers]
x:76 [in Kolmogorov.binaryEncoding]
x:76 [in Kolmogorov.preliminaries]
x:76 [in Kolmogorov.randomNumbers]
x:78 [in Kolmogorov.listFacts]
x:78 [in Kolmogorov.preliminaries]
x:79 [in Kolmogorov.kolmogorov]
x:79 [in Kolmogorov.randomNumbers]
X:8 [in Kolmogorov.listFacts]
x:8 [in Kolmogorov.random_lower_bound]
X:80 [in Kolmogorov.listFacts]
x:81 [in Kolmogorov.randomNumbers]
X:82 [in Kolmogorov.listFacts]
x:82 [in Kolmogorov.preliminaries]
x:82 [in Kolmogorov.randomNumbers]
x:83 [in Kolmogorov.listFacts]
x:84 [in Kolmogorov.preliminaries]
x:85 [in Kolmogorov.randomNumbers]
X:86 [in Kolmogorov.listFacts]
x:88 [in Kolmogorov.listFacts]
x:9 [in Kolmogorov.listFacts]
x:9 [in Kolmogorov.binaryEncoding]
x:93 [in Kolmogorov.randomNumbers]
x:95 [in Kolmogorov.randomNumbers]
x:96 [in Kolmogorov.listFacts]
x:98 [in Kolmogorov.randomNumbers]
Y
y':6 [in Kolmogorov.kolmogorov]y:10 [in Kolmogorov.listFacts]
y:10 [in Kolmogorov.binaryEncoding]
y:128 [in Kolmogorov.random_lower_bound]
y:13 [in Kolmogorov.binaryEncoding]
y:16 [in Kolmogorov.kolmogorov]
y:25 [in Kolmogorov.preliminaries]
y:29 [in Kolmogorov.preliminaries]
y:37 [in Kolmogorov.listFacts]
y:4 [in Kolmogorov.kolmogorov]
y:56 [in Kolmogorov.binaryEncoding]
y:60 [in Kolmogorov.binaryEncoding]
y:74 [in Kolmogorov.binaryEncoding]
y:75 [in Kolmogorov.binaryEncoding]
y:77 [in Kolmogorov.preliminaries]
y:79 [in Kolmogorov.preliminaries]
y:83 [in Kolmogorov.preliminaries]
y:84 [in Kolmogorov.listFacts]
y:85 [in Kolmogorov.preliminaries]
Z
z:204 [in Kolmogorov.random_lower_bound]z:216 [in Kolmogorov.random_lower_bound]
z:237 [in Kolmogorov.random_lower_bound]
z:239 [in Kolmogorov.random_lower_bound]
z:242 [in Kolmogorov.random_lower_bound]
z:244 [in Kolmogorov.random_lower_bound]
Library Index
B
binaryEncodingK
kolmogorovL
listFactsP
preliminariesR
randomNumbersrandom_lower_bound
U
uncomputabilityLemma Index
A
agree_trans [in Kolmogorov.preliminaries]agree_ref [in Kolmogorov.preliminaries]
C
constructive_least_witness [in Kolmogorov.preliminaries]D
decode_v_lt_pow2 [in Kolmogorov.random_lower_bound]decode_pow2 [in Kolmogorov.binaryEncoding]
decode_nil_O [in Kolmogorov.binaryEncoding]
decode_injective [in Kolmogorov.binaryEncoding]
decode_surjective [in Kolmogorov.binaryEncoding]
decode_monotone [in Kolmogorov.binaryEncoding]
DN_intro [in Kolmogorov.preliminaries]
DN_imp [in Kolmogorov.preliminaries]
DN_LM [in Kolmogorov.preliminaries]
E
encode_finite_all [in Kolmogorov.binaryEncoding]encode_finite [in Kolmogorov.binaryEncoding]
encode_injective [in Kolmogorov.binaryEncoding]
encode_surjective [in Kolmogorov.binaryEncoding]
encode_monotone2 [in Kolmogorov.binaryEncoding]
enumerator_list_NoDup [in Kolmogorov.listFacts]
enumerator_list [in Kolmogorov.listFacts]
enum_p_list_option_least_monotonic [in Kolmogorov.random_lower_bound]
enum_p_list_option_exists [in Kolmogorov.random_lower_bound]
enum_p_list_option_least [in Kolmogorov.random_lower_bound]
enum_p_list_least [in Kolmogorov.random_lower_bound]
enum_p_list_exists [in Kolmogorov.random_lower_bound]
enum_p_list_correct [in Kolmogorov.random_lower_bound]
enum_p_m_mono_incl [in Kolmogorov.random_lower_bound]
enum_p_m_step_incl [in Kolmogorov.random_lower_bound]
enum_p_m_step_length_iff [in Kolmogorov.random_lower_bound]
enum_p_m0_nil [in Kolmogorov.random_lower_bound]
enum_p_m_length [in Kolmogorov.random_lower_bound]
enum_p_m_length' [in Kolmogorov.random_lower_bound]
enum_p_m_eq_length [in Kolmogorov.random_lower_bound]
enum_p_m_equiv [in Kolmogorov.random_lower_bound]
enum_p_m_step_length [in Kolmogorov.random_lower_bound]
enum_p_m_Sm [in Kolmogorov.random_lower_bound]
enum_p_list_equiv [in Kolmogorov.random_lower_bound]
enum_p_list_max_length [in Kolmogorov.random_lower_bound]
enum_p_list_mono_length [in Kolmogorov.random_lower_bound]
enum_p_list_incl [in Kolmogorov.random_lower_bound]
enum_p_list_incl_step [in Kolmogorov.random_lower_bound]
enum_p_list_sat_len_n [in Kolmogorov.random_lower_bound]
enum_p_list_sat_p [in Kolmogorov.random_lower_bound]
enum_p_list_length_s [in Kolmogorov.random_lower_bound]
enum_p_list_length [in Kolmogorov.random_lower_bound]
enum_p_list_NoDup [in Kolmogorov.random_lower_bound]
exists_kol_le [in Kolmogorov.kolmogorov]
exists_kol [in Kolmogorov.kolmogorov]
exists_univ [in Kolmogorov.kolmogorov]
exp_superlinear [in Kolmogorov.binaryEncoding]
F
firstn_incl [in Kolmogorov.listFacts]firstn_incl_le [in Kolmogorov.listFacts]
firstn_In [in Kolmogorov.listFacts]
firstn_app [in Kolmogorov.listFacts]
first_false_replicate [in Kolmogorov.listFacts]
Forall_remove [in Kolmogorov.listFacts]
I
incl_transitive [in Kolmogorov.listFacts]Injective_rev_seq [in Kolmogorov.listFacts]
Injective_rev [in Kolmogorov.listFacts]
InvarianceTheorem [in Kolmogorov.kolmogorov]
In_skipn [in Kolmogorov.listFacts]
In_le_n_list [in Kolmogorov.binaryEncoding]
K
kol_unbounded [in Kolmogorov.uncomputability]kol_list_le [in Kolmogorov.uncomputability]
kol_list_eq [in Kolmogorov.uncomputability]
kol_functional [in Kolmogorov.kolmogorov]
kol_alt [in Kolmogorov.kolmogorov]
L
last_rev_first [in Kolmogorov.listFacts]least_unique [in Kolmogorov.preliminaries]
le_list_encode [in Kolmogorov.binaryEncoding]
le_list [in Kolmogorov.binaryEncoding]
le_n_list_lt_n_list [in Kolmogorov.binaryEncoding]
le_n_list_length [in Kolmogorov.binaryEncoding]
le_n_list_NoDup [in Kolmogorov.binaryEncoding]
le_n_list_In [in Kolmogorov.binaryEncoding]
list_difference_noDup_length [in Kolmogorov.listFacts]
list_differece_not_in_eq [in Kolmogorov.listFacts]
LM_DN [in Kolmogorov.preliminaries]
log2_pow2_lt [in Kolmogorov.binaryEncoding]
lt_length_list' [in Kolmogorov.listFacts]
lt_length_list [in Kolmogorov.listFacts]
l_sublinear [in Kolmogorov.binaryEncoding]
l_encode_unbounded [in Kolmogorov.binaryEncoding]
M
map_n_list_NoDup [in Kolmogorov.binaryEncoding]monotonic_eq [in Kolmogorov.preliminaries]
MP_LM [in Kolmogorov.preliminaries]
N
nat_infinite [in Kolmogorov.uncomputability]nat_list_NoDup_size [in Kolmogorov.listFacts]
NoDup_equiv_length_eq [in Kolmogorov.listFacts]
NoDup_firstn [in Kolmogorov.listFacts]
NoDup_skipn [in Kolmogorov.listFacts]
nodup_length [in Kolmogorov.listFacts]
NoDup_partition [in Kolmogorov.listFacts]
NoDup_remove_length [in Kolmogorov.listFacts]
NoDup_remove [in Kolmogorov.listFacts]
nonR_m_incomplete [in Kolmogorov.randomNumbers]
nonR_undecidable [in Kolmogorov.randomNumbers]
nonR_simple [in Kolmogorov.randomNumbers]
nonR_length [in Kolmogorov.randomNumbers]
nonR_list [in Kolmogorov.randomNumbers]
nonR_enum [in Kolmogorov.randomNumbers]
nonR_enumerator [in Kolmogorov.randomNumbers]
nonR_R [in Kolmogorov.randomNumbers]
nonR_nonRalt [in Kolmogorov.randomNumbers]
not_In_le_n_list [in Kolmogorov.binaryEncoding]
n_list_length [in Kolmogorov.binaryEncoding]
n_list_NoDup [in Kolmogorov.binaryEncoding]
n_list_In [in Kolmogorov.binaryEncoding]
N_imp [in Kolmogorov.preliminaries]
O
ONat_eqb_neq [in Kolmogorov.preliminaries]ONat_eqb_eq [in Kolmogorov.preliminaries]
P
pow_ge_1 [in Kolmogorov.binaryEncoding]pow_div_ge_1 [in Kolmogorov.preliminaries]
pow2_length_encode [in Kolmogorov.binaryEncoding]
p_enumerable_infinite_unbounded [in Kolmogorov.preliminaries]
p_infinite_unbounded [in Kolmogorov.preliminaries]
p_sublist_NoDup [in Kolmogorov.preliminaries]
p_sublist [in Kolmogorov.preliminaries]
R
rev_seq_rev [in Kolmogorov.listFacts]rev_rev_seq [in Kolmogorov.listFacts]
rev_seq_last_O [in Kolmogorov.listFacts]
rev_seq_not_nil [in Kolmogorov.listFacts]
R_length_min [in Kolmogorov.random_lower_bound]
R_no_enum_inf_subp [in Kolmogorov.randomNumbers]
R_infinite [in Kolmogorov.randomNumbers]
R_unbounded' [in Kolmogorov.randomNumbers]
R_unbounded [in Kolmogorov.randomNumbers]
R_non_empty [in Kolmogorov.randomNumbers]
R_nonR [in Kolmogorov.randomNumbers]
R_nonR1 [in Kolmogorov.randomNumbers]
R_Ralt [in Kolmogorov.randomNumbers]
R_nonR_contradiction [in Kolmogorov.randomNumbers]
S
simple_enum_sdec [in Kolmogorov.randomNumbers]skipn_length [in Kolmogorov.listFacts]
skipn_incl_le [in Kolmogorov.listFacts]
skipn_incl [in Kolmogorov.listFacts]
skipn_replicate_app_cons [in Kolmogorov.listFacts]
skipn_replicate_app [in Kolmogorov.listFacts]
U
uncomputability [in Kolmogorov.uncomputability]univ_exists_kol [in Kolmogorov.kolmogorov]
univ_upper_bound [in Kolmogorov.kolmogorov]
upper_bound [in Kolmogorov.kolmogorov]
Axiom Index
C
CT [in Kolmogorov.preliminaries]D
decode [in Kolmogorov.binaryEncoding]decodeEncode [in Kolmogorov.binaryEncoding]
E
encode [in Kolmogorov.binaryEncoding]encodeDecode [in Kolmogorov.binaryEncoding]
encode_monotone [in Kolmogorov.binaryEncoding]
encode_logarithmic [in Kolmogorov.binaryEncoding]
P
PCT [in Kolmogorov.preliminaries]Definition Index
A
agree [in Kolmogorov.preliminaries]E
enum_p_list [in Kolmogorov.random_lower_bound]equiv [in Kolmogorov.listFacts]
K
kol [in Kolmogorov.kolmogorov]L
le_n_list [in Kolmogorov.binaryEncoding]N
nonR [in Kolmogorov.randomNumbers]num_first_false [in Kolmogorov.listFacts]
n_list [in Kolmogorov.binaryEncoding]
O
ONat_eqb [in Kolmogorov.preliminaries]R
R [in Kolmogorov.randomNumbers]rev_seq [in Kolmogorov.listFacts]
S
simple [in Kolmogorov.randomNumbers]U
univ [in Kolmogorov.kolmogorov]| Global Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (968 entries) |
| Binder Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (799 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (141 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |