| 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 | (686 entries) |
| Notation 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 | (19 entries) |
| Module 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 | (1 entry) |
| Variable 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 | (35 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 | (21 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 | (349 entries) |
| Constructor 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 | (2 entries) |
| Projection 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 | (32 entries) |
| Inductive 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 | (1 entry) |
| Instance 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 | (32 entries) |
| Section 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 | (19 entries) |
| Abbreviation 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 | (10 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 | (158 entries) |
| Record 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) |
Global Index
A
AC [definition, in SyntheticComputability.Axioms.principles]ACC [definition, in SyntheticComputability.Axioms.principles]
AC_0_0_LPO_incompat [lemma, in SyntheticComputability.Axioms.principles]
AC_0_0_LPO_incompat' [lemma, in SyntheticComputability.Axioms.principles]
AC_1_0_Fext_incompat [lemma, in SyntheticComputability.Axioms.principles]
AC_1_0_Fext [lemma, in SyntheticComputability.Axioms.principles]
AC_rel_to_ADC [lemma, in SyntheticComputability.Axioms.principles]
AC_1_0 [definition, in SyntheticComputability.Axioms.principles]
AC_0_0 [definition, in SyntheticComputability.Axioms.principles]
AC_on [definition, in SyntheticComputability.Axioms.principles]
ADC [definition, in SyntheticComputability.Axioms.principles]
ADC_on'_iff [lemma, in SyntheticComputability.Axioms.principles]
ADC_on' [definition, in SyntheticComputability.Axioms.principles]
ADC_on [definition, in SyntheticComputability.Axioms.principles]
agnostic [definition, in SyntheticComputability.Shared.partial]
and_dec [instance, in SyntheticComputability.Shared.Dec]
app_sum_list_with [lemma, in SyntheticComputability.Axioms.baire_cantor]
assm [section, in SyntheticComputability.Axioms.halting]
assm_part.G [variable, in SyntheticComputability.Axioms.axioms]
assm_part.F [variable, in SyntheticComputability.Axioms.axioms]
assm_part [section, in SyntheticComputability.Axioms.axioms]
assm_EA'.ax [variable, in SyntheticComputability.Axioms.axioms]
assm_EA' [section, in SyntheticComputability.Axioms.axioms]
assm_model_of_computation [section, in SyntheticComputability.Axioms.axioms]
assm.ax [variable, in SyntheticComputability.Axioms.halting]
assume_part [section, in SyntheticComputability.Shared.partial]
AUC_to_dec [lemma, in SyntheticComputability.Axioms.principles]
AUC_on [definition, in SyntheticComputability.Axioms.principles]
axioms [library]
B
baire_cantor [library]bind [projection, in SyntheticComputability.Shared.partial]
bind_hasvalue [projection, in SyntheticComputability.Shared.partial]
bool_equiv [instance, in SyntheticComputability.Shared.equiv_on]
bool_enum [definition, in SyntheticComputability.Synthetic.EnumerabilityFacts]
bool_eq_dec [instance, in SyntheticComputability.Shared.Dec]
bounded_longest_path [lemma, in SyntheticComputability.Axioms.kleenetree]
bounded_to_wellfounded [lemma, in SyntheticComputability.Axioms.kleenetree]
bounded_tree_iff [lemma, in SyntheticComputability.Axioms.kleenetree]
bounded_iff [lemma, in SyntheticComputability.Axioms.kleenetree]
bounded_tree' [definition, in SyntheticComputability.Axioms.kleenetree]
bounded_infinite_contra [lemma, in SyntheticComputability.Axioms.kleenetree]
bounded_tree [definition, in SyntheticComputability.Axioms.kleenetree]
C
Cantor [lemma, in SyntheticComputability.Axioms.axioms]Cantor [section, in SyntheticComputability.Axioms.axioms]
Cantor.A [variable, in SyntheticComputability.Axioms.axioms]
Cantor.g [variable, in SyntheticComputability.Axioms.axioms]
compl [definition, in SyntheticComputability.Synthetic.reductions]
compl [definition, in SyntheticComputability.Synthetic.Definitions]
computes_ext [lemma, in SyntheticComputability.Axioms.axioms]
Cont [definition, in SyntheticComputability.Axioms.principles]
continuous [definition, in SyntheticComputability.Axioms.baire_cantor]
continuous_G [lemma, in SyntheticComputability.Axioms.baire_cantor]
continuous_F [lemma, in SyntheticComputability.Axioms.baire_cantor]
coS_ADC_on_weak_to_WKL [lemma, in SyntheticComputability.Axioms.kleenetree]
cos_AC_on_weak_to_coS_ADC_on_weak [lemma, in SyntheticComputability.Axioms.kleenetree]
coS_ADC_on_weak [definition, in SyntheticComputability.Axioms.kleenetree]
coS_AC_on_weak [definition, in SyntheticComputability.Axioms.kleenetree]
coS_AC_on [definition, in SyntheticComputability.Axioms.kleenetree]
countable [definition, in SyntheticComputability.Synthetic.EnumerabilityFacts]
countable_enumerable [lemma, in SyntheticComputability.Synthetic.EnumerabilityFacts]
countable_discrete [lemma, in SyntheticComputability.Synthetic.EnumerabilityFacts]
co_semi_decidable_iff [lemma, in SyntheticComputability.Axioms.kleenetree]
co_semi_decidable_stable [lemma, in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
co_semi_decidable_and [lemma, in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
co_semi_decidable [definition, in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
co_semi_decidable_impl [lemma, in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
CT [definition, in SyntheticComputability.Axioms.axioms]
CTP [definition, in SyntheticComputability.Axioms.axioms]
CTP_to_CT [lemma, in SyntheticComputability.Axioms.axioms]
CT_to_EPF [lemma, in SyntheticComputability.Axioms.axioms]
CT_to_EPF' [lemma, in SyntheticComputability.Axioms.axioms]
CT_to_EA [lemma, in SyntheticComputability.Axioms.axioms]
CT_to_EA' [lemma, in SyntheticComputability.Axioms.axioms]
CT_Sigma_wrong [lemma, in SyntheticComputability.Axioms.principles]
CT_Sigma [definition, in SyntheticComputability.Axioms.principles]
CT_wrong.model [variable, in SyntheticComputability.Axioms.principles]
CT_wrong [section, in SyntheticComputability.Axioms.principles]
cumul [abbreviation, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
cumulative [definition, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
cumul_spec [lemma, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
cumul_spec__T [lemma, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
cumul_In [lemma, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
cum_ge' [lemma, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
cum_ge [lemma, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
D
D [definition, in SyntheticComputability.Axioms.kleenetree]d [definition, in SyntheticComputability.Axioms.kleenetree]
Dec [definition, in SyntheticComputability.Shared.Dec]
dec [definition, in SyntheticComputability.Shared.Dec]
Dec [library]
DecidabilityFacts [library]
decidable [definition, in SyntheticComputability.Synthetic.Definitions]
decidable_stable [lemma, in SyntheticComputability.Synthetic.DecidabilityFacts]
decidable_iff [lemma, in SyntheticComputability.Synthetic.DecidabilityFacts]
decidable_decidme [lemma, in SyntheticComputability.Synthetic.DecidabilityFacts]
decidable_length_T [lemma, in SyntheticComputability.Axioms.kleenetree]
decidable_stable [lemma, in SyntheticComputability.Axioms.kleenetree]
decidable_AC [lemma, in SyntheticComputability.Axioms.principles]
decidable_compl_semi_decidable [lemma, in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
decidable_semi_decidable [lemma, in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
decider [definition, in SyntheticComputability.Synthetic.Definitions]
decider_decide [lemma, in SyntheticComputability.Synthetic.DecidabilityFacts]
dec_disj [lemma, in SyntheticComputability.Synthetic.DecidabilityFacts]
dec_conj [lemma, in SyntheticComputability.Synthetic.DecidabilityFacts]
dec_compl [lemma, in SyntheticComputability.Synthetic.DecidabilityFacts]
dec_inf_decidable [lemma, in SyntheticComputability.Synthetic.DecidabilityFacts]
dec_count_enum' [lemma, in SyntheticComputability.Synthetic.EnumerabilityFacts]
dec_count_enum [lemma, in SyntheticComputability.Synthetic.EnumerabilityFacts]
dec_transfer [lemma, in SyntheticComputability.Shared.Dec]
dec_DM_impl [lemma, in SyntheticComputability.Shared.Dec]
dec_DM_and [lemma, in SyntheticComputability.Shared.Dec]
dec_DN [lemma, in SyntheticComputability.Shared.Dec]
Dec_false [lemma, in SyntheticComputability.Shared.Dec]
Dec_true [lemma, in SyntheticComputability.Shared.Dec]
Dec_auto [lemma, in SyntheticComputability.Shared.Dec]
Dec_reflect [lemma, in SyntheticComputability.Shared.Dec]
dec_to_enum [lemma, in SyntheticComputability.Axioms.halting]
dec_bounded_quant [lemma, in SyntheticComputability.Axioms.principles]
Definitions [library]
DGP [definition, in SyntheticComputability.Axioms.principles]
DGP_sdec [definition, in SyntheticComputability.Axioms.principles]
DGP_to_WLEM [lemma, in SyntheticComputability.Axioms.principles]
Diaconescu [lemma, in SyntheticComputability.Axioms.principles]
diag [lemma, in SyntheticComputability.Axioms.kleenetree]
discrete [definition, in SyntheticComputability.Synthetic.DecidabilityFacts]
discrete_list [lemma, in SyntheticComputability.Synthetic.DecidabilityFacts]
discrete_option [lemma, in SyntheticComputability.Synthetic.DecidabilityFacts]
discrete_sum [lemma, in SyntheticComputability.Synthetic.DecidabilityFacts]
discrete_prod [lemma, in SyntheticComputability.Synthetic.DecidabilityFacts]
discrete_nat_nat [lemma, in SyntheticComputability.Synthetic.DecidabilityFacts]
discrete_nat [lemma, in SyntheticComputability.Synthetic.DecidabilityFacts]
discrete_bool [lemma, in SyntheticComputability.Synthetic.DecidabilityFacts]
discrete_iff [lemma, in SyntheticComputability.Synthetic.DecidabilityFacts]
DM_Sigma_0_1_to_LLPO_split [lemma, in SyntheticComputability.Axioms.principles]
DM_Sigma_0_1_iff_totality [lemma, in SyntheticComputability.Axioms.principles]
DM_Sigma_0_1_iff_DM_sdec [lemma, in SyntheticComputability.Axioms.principles]
DM_sdec [definition, in SyntheticComputability.Axioms.principles]
DM_Sigma_0_1 [definition, in SyntheticComputability.Axioms.principles]
DNE [definition, in SyntheticComputability.Axioms.principles]
DNE_sdec_to_cosdec [lemma, in SyntheticComputability.Axioms.principles]
drop_lookup_iff [lemma, in SyntheticComputability.Axioms.baire_cantor]
dummy [definition, in SyntheticComputability.Synthetic.Infinite]
d_co_semi_decidable_impl [lemma, in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
d_semi_decidable_impl [lemma, in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
E
e [definition, in SyntheticComputability.Axioms.axioms]EA [definition, in SyntheticComputability.Axioms.axioms]
EA_to_EPF [lemma, in SyntheticComputability.Axioms.axioms]
EA_to_EA' [lemma, in SyntheticComputability.Axioms.axioms]
EA_to_EA'_prf [lemma, in SyntheticComputability.Axioms.axioms]
EA' [definition, in SyntheticComputability.Axioms.axioms]
el_dec [instance, in SyntheticComputability.Synthetic.Infinite]
el_T [definition, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
embed [definition, in SyntheticComputability.Shared.embed_nat]
EmbedNatNotations [module, in SyntheticComputability.Shared.embed_nat]
⟨ _ , _ ⟩ [notation, in SyntheticComputability.Shared.embed_nat]
embedP [lemma, in SyntheticComputability.Shared.embed_nat]
embed_nat [library]
Empty_set_eq_dec [instance, in SyntheticComputability.Shared.Dec]
EnumerabilityFacts [library]
enumerable [definition, in SyntheticComputability.Synthetic.Definitions]
enumerable_disj [lemma, in SyntheticComputability.Synthetic.MoreEnumerabilityFacts]
enumerable_conj [lemma, in SyntheticComputability.Synthetic.MoreEnumerabilityFacts]
enumerable_enum [lemma, in SyntheticComputability.Synthetic.MoreEnumerabilityFacts]
enumerable_red [lemma, in SyntheticComputability.Synthetic.ReducibilityTransport]
enumerable_graph' [lemma, in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerable_discrete_countable [lemma, in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerable_graph [lemma, in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerable_enumerable_T [lemma, in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerable__T [definition, in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerable_semi_decidable [lemma, in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerable_red_K_iff [lemma, in SyntheticComputability.Axioms.halting]
enumerable_W [lemma, in SyntheticComputability.Axioms.halting]
enumerable_code [lemma, in SyntheticComputability.Axioms.principles]
enumerable_AC [lemma, in SyntheticComputability.Axioms.principles]
enumerable_leaf [lemma, in SyntheticComputability.Axioms.baire_cantor]
enumerable_enum [lemma, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enumerable_list [lemma, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enumerable__T_list_enumerable [lemma, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enumerable_list_enumerable [lemma, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enumerates_ext [lemma, in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerator [definition, in SyntheticComputability.Synthetic.Definitions]
enumerator_enumerable [lemma, in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerator__T_option [lemma, in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerator__T_prod [lemma, in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerator__T_bool [lemma, in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerator__T_unit [lemma, in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerator__T_nat [lemma, in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerator__T [abbreviation, in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerator__T' [definition, in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerator__T_of_list [instance, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enumerator__T_to_list [instance, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enumerator__T_list [lemma, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator.e [variable, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator.T [variable, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator.X [variable, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator [section, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enumerator_to_list_enumerator [lemma, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator.T [variable, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator.e [variable, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator.p [variable, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator.X [variable, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator [section, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enum_length [lemma, in SyntheticComputability.Axioms.baire_cantor]
enum_enumT [lemma, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
EPF [definition, in SyntheticComputability.Axioms.axioms]
EPF_to_EPF_bool [lemma, in SyntheticComputability.Axioms.axioms]
EPF_bool [definition, in SyntheticComputability.Axioms.axioms]
EPF_to_EA [lemma, in SyntheticComputability.Axioms.axioms]
EPF_to_CT [lemma, in SyntheticComputability.Axioms.axioms]
eqType [record, in SyntheticComputability.Shared.Dec]
EqType [constructor, in SyntheticComputability.Shared.Dec]
eqType_dec [projection, in SyntheticComputability.Shared.Dec]
eqType_X [projection, in SyntheticComputability.Shared.Dec]
equiv_rel_is_equiv [projection, in SyntheticComputability.Shared.equiv_on]
equiv_rel [projection, in SyntheticComputability.Shared.equiv_on]
equiv_on [record, in SyntheticComputability.Shared.equiv_on]
equiv_part [instance, in SyntheticComputability.Axioms.axioms]
equiv_ran [instance, in SyntheticComputability.Synthetic.EnumerabilityFacts]
equiv_on_eq [lemma, in SyntheticComputability.Axioms.baire_cantor]
equiv_on [library]
eval [definition, in SyntheticComputability.Shared.partial]
eval_hasvalue [definition, in SyntheticComputability.Shared.partial]
eval' [definition, in SyntheticComputability.Shared.partial]
exists_leaf [lemma, in SyntheticComputability.Axioms.baire_cantor]
extend [definition, in SyntheticComputability.Axioms.baire_cantor]
ext_equiv [instance, in SyntheticComputability.Shared.equiv_on]
F
F [definition, in SyntheticComputability.Synthetic.Infinite]f [definition, in SyntheticComputability.Synthetic.Infinite]
F [definition, in SyntheticComputability.Axioms.baire_cantor]
False_eq_dec [instance, in SyntheticComputability.Shared.Dec]
False_dec [instance, in SyntheticComputability.Shared.Dec]
FAN [definition, in SyntheticComputability.Axioms.kleenetree]
Fext [definition, in SyntheticComputability.Axioms.principles]
Fext_hProp_wdisj [lemma, in SyntheticComputability.Axioms.principles]
Fext_hProp_disj [lemma, in SyntheticComputability.Axioms.principles]
Fext_hProp_neg [lemma, in SyntheticComputability.Axioms.principles]
Filter [section, in SyntheticComputability.Shared.FilterFacts]
FilterFacts [library]
filter_comm [lemma, in SyntheticComputability.Shared.FilterFacts]
filter_and [lemma, in SyntheticComputability.Shared.FilterFacts]
filter_pq_eq [lemma, in SyntheticComputability.Shared.FilterFacts]
filter_pq_mono [lemma, in SyntheticComputability.Shared.FilterFacts]
filter_fst' [lemma, in SyntheticComputability.Shared.FilterFacts]
filter_fst [lemma, in SyntheticComputability.Shared.FilterFacts]
filter_app [lemma, in SyntheticComputability.Shared.FilterFacts]
filter_id [lemma, in SyntheticComputability.Shared.FilterFacts]
filter_mono [lemma, in SyntheticComputability.Shared.FilterFacts]
filter_incl [lemma, in SyntheticComputability.Shared.FilterFacts]
Filter.X [variable, in SyntheticComputability.Shared.FilterFacts]
_ <<= _ [notation, in SyntheticComputability.Shared.FilterFacts]
_ el _ [notation, in SyntheticComputability.Shared.FilterFacts]
fix_enum.e_enum [variable, in SyntheticComputability.Axioms.kleenetree]
fix_enum.e [variable, in SyntheticComputability.Axioms.kleenetree]
fix_enum [section, in SyntheticComputability.Axioms.kleenetree]
fix_tree.ℓ_injective [variable, in SyntheticComputability.Axioms.baire_cantor]
fix_tree.enumerable_leafs [variable, in SyntheticComputability.Axioms.baire_cantor]
fix_tree.ℓ [variable, in SyntheticComputability.Axioms.baire_cantor]
fix_tree.T_K [variable, in SyntheticComputability.Axioms.baire_cantor]
fix_tree [section, in SyntheticComputability.Axioms.baire_cantor]
forall_neg_exists_iff [lemma, in SyntheticComputability.Axioms.principles]
forall_neg_exists_iff [lemma, in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
F_sur [lemma, in SyntheticComputability.Synthetic.Infinite]
F_p [lemma, in SyntheticComputability.Synthetic.Infinite]
F_inj [lemma, in SyntheticComputability.Synthetic.Infinite]
F_inj' [lemma, in SyntheticComputability.Synthetic.Infinite]
F_lt [lemma, in SyntheticComputability.Synthetic.Infinite]
F_el [lemma, in SyntheticComputability.Synthetic.Infinite]
F_nel [lemma, in SyntheticComputability.Synthetic.Infinite]
f_sur [lemma, in SyntheticComputability.Synthetic.Infinite]
F_ext [lemma, in SyntheticComputability.Axioms.baire_cantor]
F_find_pref_ext [lemma, in SyntheticComputability.Axioms.baire_cantor]
F_G_inv [lemma, in SyntheticComputability.Axioms.baire_cantor]
F_surj [lemma, in SyntheticComputability.Axioms.baire_cantor]
F_inv [lemma, in SyntheticComputability.Axioms.baire_cantor]
F_find_pref [lemma, in SyntheticComputability.Axioms.baire_cantor]
F_inj [lemma, in SyntheticComputability.Axioms.baire_cantor]
F_inj_help [lemma, in SyntheticComputability.Axioms.baire_cantor]
F' [definition, in SyntheticComputability.Axioms.baire_cantor]
F'_length_g [lemma, in SyntheticComputability.Axioms.baire_cantor]
F'_eq_lt [lemma, in SyntheticComputability.Axioms.baire_cantor]
F'_prefix [lemma, in SyntheticComputability.Axioms.baire_cantor]
F'_length [lemma, in SyntheticComputability.Axioms.baire_cantor]
F'_offset [lemma, in SyntheticComputability.Axioms.baire_cantor]
G
G [inductive, in SyntheticComputability.Axioms.axioms]G [definition, in SyntheticComputability.Axioms.baire_cantor]
gen [lemma, in SyntheticComputability.Synthetic.Infinite]
generating [definition, in SyntheticComputability.Synthetic.Infinite]
gen_le_f [lemma, in SyntheticComputability.Synthetic.Infinite]
gen_spec [lemma, in SyntheticComputability.Synthetic.Infinite]
gen' [definition, in SyntheticComputability.Synthetic.Infinite]
GI [constructor, in SyntheticComputability.Axioms.axioms]
G_zero [lemma, in SyntheticComputability.Axioms.axioms]
G_sig [lemma, in SyntheticComputability.Axioms.axioms]
G_inv [lemma, in SyntheticComputability.Axioms.baire_cantor]
H
halting [library]hasvalue [projection, in SyntheticComputability.Shared.partial]
hasvalue_det [projection, in SyntheticComputability.Shared.partial]
help [lemma, in SyntheticComputability.Axioms.baire_cantor]
Homeo_M_Cantor_Baire_to_KT [lemma, in SyntheticComputability.Axioms.baire_cantor]
Homeo_M [definition, in SyntheticComputability.Axioms.baire_cantor]
hProp [definition, in SyntheticComputability.Axioms.principles]
hProp_disj [lemma, in SyntheticComputability.Axioms.principles]
I
iff_dec [instance, in SyntheticComputability.Shared.Dec]impl_dec [instance, in SyntheticComputability.Shared.Dec]
inconsistent [definition, in SyntheticComputability.Axioms.kleenetree]
Inf [section, in SyntheticComputability.Synthetic.Infinite]
infinite [definition, in SyntheticComputability.Synthetic.Infinite]
Infinite [library]
infinite_path_to_infinite [lemma, in SyntheticComputability.Axioms.kleenetree]
infinite_path [definition, in SyntheticComputability.Axioms.kleenetree]
infinite_tree [definition, in SyntheticComputability.Axioms.kleenetree]
inf_semi_decidable [definition, in SyntheticComputability.Synthetic.Definitions]
inf_enumerable [definition, in SyntheticComputability.Synthetic.Definitions]
inf_decidable [definition, in SyntheticComputability.Synthetic.Definitions]
inf_path_iff_inf [lemma, in SyntheticComputability.Axioms.kleenetree]
inf_to_longest [lemma, in SyntheticComputability.Axioms.kleenetree]
inf_T' [lemma, in SyntheticComputability.Axioms.kleenetree]
inf_to_enumerator [instance, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
inf_list_enumerable__T [definition, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
Inf.f' [variable, in SyntheticComputability.Synthetic.Infinite]
Inf.Gen [section, in SyntheticComputability.Synthetic.Infinite]
Inf.Gen.f [variable, in SyntheticComputability.Synthetic.Infinite]
Inf.Gen.Hf [variable, in SyntheticComputability.Synthetic.Infinite]
Inf.Gen.Hfp [variable, in SyntheticComputability.Synthetic.Infinite]
Inf.Hf' [variable, in SyntheticComputability.Synthetic.Infinite]
Inf.Hg [variable, in SyntheticComputability.Synthetic.Infinite]
Inf.HX [variable, in SyntheticComputability.Synthetic.Infinite]
Inf.p [variable, in SyntheticComputability.Synthetic.Infinite]
Inf.X [variable, in SyntheticComputability.Synthetic.Infinite]
injective [definition, in SyntheticComputability.Synthetic.Infinite]
inspect_opt [lemma, in SyntheticComputability.Axioms.principles]
in_concat_iff [lemma, in SyntheticComputability.Shared.ListAutomation]
in_filter_iff [lemma, in SyntheticComputability.Shared.FilterFacts]
In_cumul [lemma, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
IP [definition, in SyntheticComputability.Axioms.principles]
is_true [definition, in SyntheticComputability.Shared.Dec]
is_tree_T' [lemma, in SyntheticComputability.Axioms.kleenetree]
is_infinite_tree [definition, in SyntheticComputability.Axioms.kleenetree]
is_tree_subtree_at_from_inf [lemma, in SyntheticComputability.Axioms.kleenetree]
is_tree_subtree_at [lemma, in SyntheticComputability.Axioms.kleenetree]
is_tree [record, in SyntheticComputability.Axioms.kleenetree]
Is_true_neg_iff [lemma, in SyntheticComputability.Axioms.kleenetree]
Is_true_iff [lemma, in SyntheticComputability.Axioms.kleenetree]
J
join [definition, in SyntheticComputability.Synthetic.reductions]K
K [definition, in SyntheticComputability.Synthetic.reductions]kleenetree [library]
Kleene_inf_exit [projection, in SyntheticComputability.Axioms.kleenetree]
Kleene_infinite [projection, in SyntheticComputability.Axioms.kleenetree]
Kleene_T [projection, in SyntheticComputability.Axioms.kleenetree]
Kleene_tree [record, in SyntheticComputability.Axioms.kleenetree]
KS [definition, in SyntheticComputability.Axioms.principles]
KS_LLPO_to_DGP [lemma, in SyntheticComputability.Axioms.principles]
KS_WLPO_to_WLEM [lemma, in SyntheticComputability.Axioms.principles]
KS_LPO_to_LEM [lemma, in SyntheticComputability.Axioms.principles]
KT [definition, in SyntheticComputability.Axioms.kleenetree]
KT_FAN_contra [lemma, in SyntheticComputability.Axioms.kleenetree]
KT_WKL_contra [lemma, in SyntheticComputability.Axioms.kleenetree]
KT_to_Homeo_N_nat_bool [lemma, in SyntheticComputability.Axioms.baire_cantor]
KT_iff_Homeo_N_nat_bool [lemma, in SyntheticComputability.Axioms.baire_cantor]
KT_inj_enum_leafs [lemma, in SyntheticComputability.Axioms.baire_cantor]
K_forall_undec [lemma, in SyntheticComputability.Axioms.halting]
K_nat_equiv_compl [lemma, in SyntheticComputability.Axioms.halting]
K_nat_equiv [lemma, in SyntheticComputability.Axioms.halting]
K_nat [definition, in SyntheticComputability.Axioms.halting]
K_compl_undec [lemma, in SyntheticComputability.Axioms.halting]
K0 [definition, in SyntheticComputability.Axioms.halting]
K0_red_K [lemma, in SyntheticComputability.Axioms.halting]
K0_enum [lemma, in SyntheticComputability.Axioms.halting]
K0_compl_undec [lemma, in SyntheticComputability.Axioms.halting]
K0_undec [lemma, in SyntheticComputability.Axioms.halting]
K0_enumerable [lemma, in SyntheticComputability.Axioms.halting]
L
leaf [definition, in SyntheticComputability.Axioms.baire_cantor]leaf_prefix [lemma, in SyntheticComputability.Axioms.baire_cantor]
least [definition, in SyntheticComputability.Axioms.axioms]
least_ex [lemma, in SyntheticComputability.Axioms.principles]
LEM [definition, in SyntheticComputability.Axioms.principles]
LEM_WKL_KT [lemma, in SyntheticComputability.Axioms.kleenetree]
LEM_FAN_KT [lemma, in SyntheticComputability.Axioms.kleenetree]
LEM_to_KS [lemma, in SyntheticComputability.Axioms.principles]
LEM_to_LPO [lemma, in SyntheticComputability.Axioms.principles]
LEM_to_IP [lemma, in SyntheticComputability.Axioms.principles]
LEM_to_DGP [lemma, in SyntheticComputability.Axioms.principles]
length_inv [lemma, in SyntheticComputability.Axioms.kleenetree]
le_f [definition, in SyntheticComputability.Synthetic.Infinite]
listable [definition, in SyntheticComputability.Axioms.kleenetree]
listable_lt [lemma, in SyntheticComputability.Axioms.kleenetree]
listable_has_max [lemma, in SyntheticComputability.Axioms.kleenetree]
listable_prefix [lemma, in SyntheticComputability.Axioms.kleenetree]
listable_list_length_lt [lemma, in SyntheticComputability.Axioms.kleenetree]
listable_list_length [lemma, in SyntheticComputability.Axioms.kleenetree]
listable_exists_dec [lemma, in SyntheticComputability.Axioms.kleenetree]
listable_forall_dec [lemma, in SyntheticComputability.Axioms.kleenetree]
listable_list_length_lt [lemma, in SyntheticComputability.Axioms.baire_cantor]
ListAutomation [library]
ListEnumerabilityFacts [library]
list_in_dec [instance, in SyntheticComputability.Shared.ListAutomation]
list_eq_dec [instance, in SyntheticComputability.Shared.Dec]
list_enumerator_to_cumul [lemma, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
list_enumerable__T_enumerable [lemma, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
list_enumerable_enumerable [lemma, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
list_enumerator_enumerator [lemma, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
list_enumerator_to_enumerator [lemma, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
list_enumerable__T [definition, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
list_enumerator__T [abbreviation, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
list_enumerator__T' [definition, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
list_enumerable [definition, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
list_enumerator [definition, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
LL [definition, in SyntheticComputability.Synthetic.Infinite]
LLPO [definition, in SyntheticComputability.Axioms.principles]
LLPO_coS_AC_on_to_coS_AC_on_weak [lemma, in SyntheticComputability.Axioms.kleenetree]
LLPO_LLPO_tree_iff [lemma, in SyntheticComputability.Axioms.kleenetree]
LLPO_tree [definition, in SyntheticComputability.Axioms.kleenetree]
LLPO_split_to_LLPO [lemma, in SyntheticComputability.Axioms.principles]
LLPO_iff_DGP_sdec [lemma, in SyntheticComputability.Axioms.principles]
LLPO_to_DM_Sigma_0_1 [lemma, in SyntheticComputability.Axioms.principles]
LLPO_split [definition, in SyntheticComputability.Axioms.principles]
LL_F [lemma, in SyntheticComputability.Synthetic.Infinite]
LL_f [lemma, in SyntheticComputability.Synthetic.Infinite]
LL_cum [lemma, in SyntheticComputability.Synthetic.Infinite]
lookup_map [lemma, in SyntheticComputability.Axioms.kleenetree]
LPL [definition, in SyntheticComputability.Axioms.kleenetree]
LPO [definition, in SyntheticComputability.Axioms.principles]
LPO_tree_iff [lemma, in SyntheticComputability.Axioms.kleenetree]
LPO_tree [definition, in SyntheticComputability.Axioms.kleenetree]
LPO_to_MP [lemma, in SyntheticComputability.Axioms.principles]
LPO_MP_WLPO_iff [lemma, in SyntheticComputability.Axioms.principles]
LPO_semidecidable_iff [lemma, in SyntheticComputability.Axioms.principles]
LPO_semidecidable [definition, in SyntheticComputability.Axioms.principles]
LPO_to_WLPO [lemma, in SyntheticComputability.Axioms.principles]
lt_acc [lemma, in SyntheticComputability.Synthetic.Infinite]
LX [definition, in SyntheticComputability.Synthetic.Infinite]
LX_p [lemma, in SyntheticComputability.Synthetic.Infinite]
LX_NoDup [lemma, in SyntheticComputability.Synthetic.Infinite]
LX_el [lemma, in SyntheticComputability.Synthetic.Infinite]
LX_len [lemma, in SyntheticComputability.Synthetic.Infinite]
L_T [definition, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
L_list_cumulative [lemma, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
L_list [definition, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
L_list_def.L [variable, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
L_list_def [section, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
M
map_nth_seq [lemma, in SyntheticComputability.Axioms.baire_cantor]map_seq_eq [lemma, in SyntheticComputability.Axioms.baire_cantor]
max_list_spec [lemma, in SyntheticComputability.Axioms.principles]
max_list_with_spec [lemma, in SyntheticComputability.Axioms.principles]
max_list_spec' [lemma, in SyntheticComputability.Axioms.principles]
max_list_with_spec' [lemma, in SyntheticComputability.Axioms.principles]
max_list_incl [lemma, in SyntheticComputability.Axioms.baire_cantor]
mkpart [definition, in SyntheticComputability.Shared.partial]
mkpart_hasvalue [lemma, in SyntheticComputability.Shared.partial]
mkpart_hasvalue2 [lemma, in SyntheticComputability.Shared.partial]
mkpart_ter [lemma, in SyntheticComputability.Shared.partial]
mkpart_hasvalue1 [lemma, in SyntheticComputability.Shared.partial]
model_of_computation [record, in SyntheticComputability.Axioms.axioms]
modulus [definition, in SyntheticComputability.Axioms.baire_cantor]
monotonic [definition, in SyntheticComputability.Shared.partial]
monotonic_agnostic [lemma, in SyntheticComputability.Shared.partial]
MoreEnumerabilityFacts [library]
MP [definition, in SyntheticComputability.Axioms.principles]
MP_tree_iff' [lemma, in SyntheticComputability.Axioms.kleenetree]
MP_tree' [definition, in SyntheticComputability.Axioms.kleenetree]
MP_tree_iff [lemma, in SyntheticComputability.Axioms.kleenetree]
MP_tree [definition, in SyntheticComputability.Axioms.kleenetree]
MP_cosdec_to_sdec [lemma, in SyntheticComputability.Axioms.principles]
MP_iff_sdec_weak_total [lemma, in SyntheticComputability.Axioms.principles]
MP_semidecidable_to_Post_logical [lemma, in SyntheticComputability.Axioms.principles]
MP_to_MP_semidecidable [lemma, in SyntheticComputability.Axioms.principles]
MP_IP_LPO [lemma, in SyntheticComputability.Axioms.principles]
MP_semidecidable [definition, in SyntheticComputability.Axioms.principles]
mu [projection, in SyntheticComputability.Shared.partial]
mu_nat_dec [definition, in SyntheticComputability.Axioms.axioms]
mu_nat [lemma, in SyntheticComputability.Axioms.axioms]
mu_ter [lemma, in SyntheticComputability.Shared.partial]
mu_hasvalue [projection, in SyntheticComputability.Shared.partial]
mu_nat_min [lemma, in SyntheticComputability.Shared.partial]
mu_nat [definition, in SyntheticComputability.Shared.partial]
mu_nat_spec [definition, in SyntheticComputability.Shared.prelim]
mu_nat [definition, in SyntheticComputability.Shared.prelim]
mu_nat_p_irrel [lemma, in SyntheticComputability.Shared.prelim]
mu_nat_p_least [lemma, in SyntheticComputability.Shared.prelim]
mu_nat_p_min [lemma, in SyntheticComputability.Shared.prelim]
mu_nat_p [definition, in SyntheticComputability.Shared.prelim]
N
nat_equiv [instance, in SyntheticComputability.Shared.equiv_on]nat_enum [definition, in SyntheticComputability.Synthetic.EnumerabilityFacts]
nat_eq_dec [instance, in SyntheticComputability.Shared.Dec]
neg_neg_XM [lemma, in SyntheticComputability.Axioms.principles]
nil_no_leaf [lemma, in SyntheticComputability.Axioms.baire_cantor]
not_dec [instance, in SyntheticComputability.Shared.Dec]
not_bounded_infinite_iff [lemma, in SyntheticComputability.Axioms.kleenetree]
not_bounded_infinite [lemma, in SyntheticComputability.Axioms.kleenetree]
not_bounded_infinite' [lemma, in SyntheticComputability.Axioms.kleenetree]
nth [abbreviation, in SyntheticComputability.Axioms.baire_cantor]
nth_sig [lemma, in SyntheticComputability.Axioms.baire_cantor]
nxt [definition, in SyntheticComputability.Axioms.baire_cantor]
nxt_iter [lemma, in SyntheticComputability.Axioms.baire_cantor]
O
ofenum [definition, in SyntheticComputability.Axioms.axioms]ofenum_ter [lemma, in SyntheticComputability.Axioms.axioms]
ofenum_spec [lemma, in SyntheticComputability.Axioms.axioms]
ofenum_ter_iff [lemma, in SyntheticComputability.Axioms.axioms]
option_enum [definition, in SyntheticComputability.Synthetic.EnumerabilityFacts]
option_eq_dec [instance, in SyntheticComputability.Shared.Dec]
or_dec [instance, in SyntheticComputability.Shared.Dec]
P
par [projection, in SyntheticComputability.Shared.partial]part [projection, in SyntheticComputability.Shared.partial]
partial [library]
partiality [record, in SyntheticComputability.Shared.partial]
partial_to_total [lemma, in SyntheticComputability.Axioms.axioms]
part_equiv_Equivalence [instance, in SyntheticComputability.Shared.partial]
par_hasvalue3 [projection, in SyntheticComputability.Shared.partial]
par_hasvalue2 [projection, in SyntheticComputability.Shared.partial]
par_hasvalue1 [projection, in SyntheticComputability.Shared.partial]
path_wellfounded_contra [lemma, in SyntheticComputability.Axioms.kleenetree]
PEM [definition, in SyntheticComputability.Synthetic.reductions]
Pext [definition, in SyntheticComputability.Axioms.principles]
Pext_to_PI [lemma, in SyntheticComputability.Axioms.principles]
PFP [definition, in SyntheticComputability.Axioms.principles]
PI [definition, in SyntheticComputability.Axioms.principles]
Post [definition, in SyntheticComputability.Axioms.principles]
Post_to_MP [lemma, in SyntheticComputability.Axioms.principles]
Post_logical_to_Post [lemma, in SyntheticComputability.Axioms.principles]
Post_logical [definition, in SyntheticComputability.Axioms.principles]
prefixes_inv [lemma, in SyntheticComputability.Axioms.kleenetree]
prefix_length_eq [lemma, in SyntheticComputability.Axioms.kleenetree]
prefix_take_iff [lemma, in SyntheticComputability.Axioms.baire_cantor]
prelim [library]
principles [library]
prod_enum [definition, in SyntheticComputability.Synthetic.EnumerabilityFacts]
prod_eq_dec [instance, in SyntheticComputability.Shared.Dec]
projection [lemma, in SyntheticComputability.Synthetic.EnumerabilityFacts]
projection' [lemma, in SyntheticComputability.Synthetic.EnumerabilityFacts]
Proper_decidable [instance, in SyntheticComputability.Synthetic.DecidabilityFacts]
Proper_decides [instance, in SyntheticComputability.Synthetic.DecidabilityFacts]
Prop_equiv [instance, in SyntheticComputability.Shared.equiv_on]
R
reduces_m [definition, in SyntheticComputability.Synthetic.reductions]ReducibilityTransport [library]
reductions [library]
red_m_transports_stable [lemma, in SyntheticComputability.Synthetic.reductions]
red_m_decidable_nontriv [lemma, in SyntheticComputability.Synthetic.reductions]
red_m_join_least [lemma, in SyntheticComputability.Synthetic.reductions]
red_m_join_q [lemma, in SyntheticComputability.Synthetic.reductions]
red_m_join_p [lemma, in SyntheticComputability.Synthetic.reductions]
red_m_compl_compl_PEM_3 [lemma, in SyntheticComputability.Synthetic.reductions]
red_m_compl_compl_PEM_2 [lemma, in SyntheticComputability.Synthetic.reductions]
red_m_compl_compl_PEM [lemma, in SyntheticComputability.Synthetic.reductions]
red_m_complement [lemma, in SyntheticComputability.Synthetic.reductions]
red_m_transports [lemma, in SyntheticComputability.Synthetic.reductions]
red_m_transitive [lemma, in SyntheticComputability.Synthetic.reductions]
red_m_reflexive [instance, in SyntheticComputability.Synthetic.reductions]
red_m [definition, in SyntheticComputability.Synthetic.reductions]
reflects [definition, in SyntheticComputability.Synthetic.Definitions]
reflects_prv_iff [lemma, in SyntheticComputability.Synthetic.DecidabilityFacts]
reflects_prv [lemma, in SyntheticComputability.Synthetic.DecidabilityFacts]
reflects_disj [lemma, in SyntheticComputability.Synthetic.DecidabilityFacts]
reflects_conj [lemma, in SyntheticComputability.Synthetic.DecidabilityFacts]
reflects_not [lemma, in SyntheticComputability.Synthetic.DecidabilityFacts]
reflects_cases [lemma, in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
ret [projection, in SyntheticComputability.Shared.partial]
retract [definition, in SyntheticComputability.Synthetic.EnumerabilityFacts]
retraction [abbreviation, in SyntheticComputability.Synthetic.EnumerabilityFacts]
retraction' [definition, in SyntheticComputability.Synthetic.EnumerabilityFacts]
ret_hasvalue_inv [lemma, in SyntheticComputability.Shared.partial]
ret_hasvalue [projection, in SyntheticComputability.Shared.partial]
Reverse_Induction [section, in SyntheticComputability.Axioms.kleenetree]
rev_rect [lemma, in SyntheticComputability.Axioms.kleenetree]
rev_list_rect [lemma, in SyntheticComputability.Axioms.kleenetree]
S
sdec_compute_lor [lemma, in SyntheticComputability.Synthetic.SemiDecidabilityFacts]sec_enum [lemma, in SyntheticComputability.Axioms.halting]
SemiDecidabilityFacts [library]
semidecidable_red [lemma, in SyntheticComputability.Synthetic.ReducibilityTransport]
semi_decidable_red_K_iff [lemma, in SyntheticComputability.Synthetic.reductions]
semi_decidable_enumerable [lemma, in SyntheticComputability.Synthetic.EnumerabilityFacts]
semi_decidable [definition, in SyntheticComputability.Synthetic.Definitions]
semi_decider [definition, in SyntheticComputability.Synthetic.Definitions]
semi_decidable_K [lemma, in SyntheticComputability.Axioms.halting]
semi_decidable_ext [lemma, in SyntheticComputability.Axioms.principles]
semi_decidable_AC [lemma, in SyntheticComputability.Axioms.principles]
semi_decidable_projection_iff [lemma, in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
semi_decidable_and [lemma, in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
semi_decidable_or [lemma, in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
semi_decidable_impl [lemma, in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
seval [projection, in SyntheticComputability.Shared.partial]
seval_hasvalue [projection, in SyntheticComputability.Shared.partial]
seval_mono [projection, in SyntheticComputability.Shared.partial]
size_generating [lemma, in SyntheticComputability.Axioms.baire_cantor]
stable [abbreviation, in SyntheticComputability.Synthetic.DecidabilityFacts]
stable [definition, in SyntheticComputability.Synthetic.reductions]
subtree_at [definition, in SyntheticComputability.Axioms.kleenetree]
sub_dec [lemma, in SyntheticComputability.Synthetic.Infinite]
sum_eq_dec [instance, in SyntheticComputability.Shared.Dec]
surjection_wrt [definition, in SyntheticComputability.Shared.equiv_on]
T
T [projection, in SyntheticComputability.Axioms.axioms]take_prefix [lemma, in SyntheticComputability.Axioms.kleenetree]
take_length_ℓ [lemma, in SyntheticComputability.Axioms.baire_cantor]
take_prefix [lemma, in SyntheticComputability.Axioms.baire_cantor]
take_take [lemma, in SyntheticComputability.Axioms.baire_cantor]
take_seq [lemma, in SyntheticComputability.Axioms.baire_cantor]
take_map [lemma, in SyntheticComputability.Axioms.baire_cantor]
toenum [definition, in SyntheticComputability.Axioms.axioms]
toenum_spec [lemma, in SyntheticComputability.Axioms.axioms]
total_list [lemma, in SyntheticComputability.Axioms.principles]
to_dec [lemma, in SyntheticComputability.Shared.ListAutomation]
to_Homeo_M_bool_nat [lemma, in SyntheticComputability.Axioms.baire_cantor]
to_Homeo_M_nat_bool [lemma, in SyntheticComputability.Axioms.baire_cantor]
to_cumul_spec [lemma, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
to_cumul_cumulative [lemma, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
to_cumul [definition, in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
tree [record, in SyntheticComputability.Axioms.kleenetree]
tree_from_f_bounded_iff_wf [lemma, in SyntheticComputability.Axioms.kleenetree]
tree_from_f_bounded_iff [lemma, in SyntheticComputability.Axioms.kleenetree]
tree_from [definition, in SyntheticComputability.Axioms.kleenetree]
tree_nil [lemma, in SyntheticComputability.Axioms.kleenetree]
tree_is_tree [projection, in SyntheticComputability.Axioms.kleenetree]
tree_T [projection, in SyntheticComputability.Axioms.kleenetree]
tree_dec [projection, in SyntheticComputability.Axioms.kleenetree]
tree_p [projection, in SyntheticComputability.Axioms.kleenetree]
tree_inhab [projection, in SyntheticComputability.Axioms.kleenetree]
True_eq_dec [instance, in SyntheticComputability.Shared.Dec]
True_dec [instance, in SyntheticComputability.Shared.Dec]
T_func_in_n [lemma, in SyntheticComputability.Axioms.axioms]
T_mono [projection, in SyntheticComputability.Axioms.axioms]
T_inf_sdec_iff [lemma, in SyntheticComputability.Axioms.kleenetree]
T_inf_sdec_iff' [lemma, in SyntheticComputability.Axioms.kleenetree]
T_inf_sdec [definition, in SyntheticComputability.Axioms.kleenetree]
T_K [definition, in SyntheticComputability.Axioms.kleenetree]
T' [definition, in SyntheticComputability.Axioms.kleenetree]
U
undef [projection, in SyntheticComputability.Shared.partial]undef_hasvalue [projection, in SyntheticComputability.Shared.partial]
unembed [definition, in SyntheticComputability.Shared.embed_nat]
unembedP [lemma, in SyntheticComputability.Shared.embed_nat]
unit_enum [definition, in SyntheticComputability.Synthetic.EnumerabilityFacts]
unit_eq_dec [instance, in SyntheticComputability.Shared.Dec]
Unnamed_thm2 [definition, in SyntheticComputability.Axioms.principles]
Unnamed_thm1 [definition, in SyntheticComputability.Axioms.principles]
Unnamed_thm0 [definition, in SyntheticComputability.Axioms.principles]
Unnamed_thm [definition, in SyntheticComputability.Axioms.principles]
upper_semi_lattice.q [variable, in SyntheticComputability.Synthetic.reductions]
upper_semi_lattice.p [variable, in SyntheticComputability.Synthetic.reductions]
upper_semi_lattice [section, in SyntheticComputability.Synthetic.reductions]
W
W [abbreviation, in SyntheticComputability.Axioms.axioms]W [definition, in SyntheticComputability.Axioms.axioms]
W [abbreviation, in SyntheticComputability.Axioms.halting]
WC_N_to_Cont [lemma, in SyntheticComputability.Axioms.principles]
WC_N_CT_inc [lemma, in SyntheticComputability.Axioms.principles]
WC_N [definition, in SyntheticComputability.Axioms.principles]
wellfounded_tree [definition, in SyntheticComputability.Axioms.kleenetree]
WKL [definition, in SyntheticComputability.Axioms.kleenetree]
WKL_to_coS_AC_on_nat_bool [lemma, in SyntheticComputability.Axioms.kleenetree]
WKL_to_LLPO [lemma, in SyntheticComputability.Axioms.kleenetree]
WKL_to_FAN [lemma, in SyntheticComputability.Axioms.kleenetree]
WKL_to_LPL.T [variable, in SyntheticComputability.Axioms.kleenetree]
WKL_to_LPL [section, in SyntheticComputability.Axioms.kleenetree]
WLEM [definition, in SyntheticComputability.Axioms.principles]
WLEM_to_WLPO [lemma, in SyntheticComputability.Axioms.principles]
WLPO [definition, in SyntheticComputability.Axioms.principles]
WLPO_tree_iff [lemma, in SyntheticComputability.Axioms.kleenetree]
WLPO_tree [definition, in SyntheticComputability.Axioms.kleenetree]
WLPO_PFP_LLPO_iff [lemma, in SyntheticComputability.Axioms.principles]
WLPO_cosemidecidable_iff [lemma, in SyntheticComputability.Axioms.principles]
WLPO_cosemidecidable [definition, in SyntheticComputability.Axioms.principles]
WLPO_semidecidable_iff [lemma, in SyntheticComputability.Axioms.principles]
WLPO_semidecidable [definition, in SyntheticComputability.Axioms.principles]
WO [section, in SyntheticComputability.Axioms.axioms]
WO.f [variable, in SyntheticComputability.Axioms.axioms]
W_self_enumerable [lemma, in SyntheticComputability.Axioms.axioms]
W_spec [lemma, in SyntheticComputability.Axioms.halting]
X
X_gen [lemma, in SyntheticComputability.Synthetic.Infinite]other
∑ _ .. _ , _ (type_scope) [notation, in SyntheticComputability.Shared.prelim]_ ≡ₘ _ [notation, in SyntheticComputability.Synthetic.reductions]
_ ⪯ₘ _ [notation, in SyntheticComputability.Synthetic.reductions]
_ el _ [notation, in SyntheticComputability.Shared.ListAutomation]
_ ≡{ _ } _ [notation, in SyntheticComputability.Shared.equiv_on]
_ ∼ _ [notation, in SyntheticComputability.Axioms.axioms]
_ ≡{ran} _ [notation, in SyntheticComputability.Synthetic.EnumerabilityFacts]
_ ↛ _ [notation, in SyntheticComputability.Shared.partial]
_ =! _ [notation, in SyntheticComputability.Shared.partial]
eq_dec _ [notation, in SyntheticComputability.Shared.Dec]
fun! ⟨ _ , _ ⟩ => _ [notation, in SyntheticComputability.Shared.prelim]
if! _ is _ then _ else _ [notation, in SyntheticComputability.Shared.prelim]
( _ × _ × .. × _ ) [notation, in SyntheticComputability.Shared.ListAutomation]
[ _ | _ ∈ _ ] [notation, in SyntheticComputability.Shared.ListAutomation]
[ _ | _ ∈ _ , _ ] [notation, in SyntheticComputability.Shared.ListAutomation]
⟨ _ , _ ⟩ [notation, in SyntheticComputability.Axioms.axioms]
φ [definition, in SyntheticComputability.Axioms.axioms]
φ [abbreviation, in SyntheticComputability.Axioms.halting]
φ_spec [abbreviation, in SyntheticComputability.Axioms.halting]
ℓ_sig_prf [lemma, in SyntheticComputability.Axioms.baire_cantor]
ℓ_sig [lemma, in SyntheticComputability.Axioms.baire_cantor]
ℓ_leaf [lemma, in SyntheticComputability.Axioms.baire_cantor]
Notation Index
E
⟨ _ , _ ⟩ [in SyntheticComputability.Shared.embed_nat]F
_ <<= _ [in SyntheticComputability.Shared.FilterFacts]_ el _ [in SyntheticComputability.Shared.FilterFacts]
other
∑ _ .. _ , _ (type_scope) [in SyntheticComputability.Shared.prelim]_ ≡ₘ _ [in SyntheticComputability.Synthetic.reductions]
_ ⪯ₘ _ [in SyntheticComputability.Synthetic.reductions]
_ el _ [in SyntheticComputability.Shared.ListAutomation]
_ ≡{ _ } _ [in SyntheticComputability.Shared.equiv_on]
_ ∼ _ [in SyntheticComputability.Axioms.axioms]
_ ≡{ran} _ [in SyntheticComputability.Synthetic.EnumerabilityFacts]
_ ↛ _ [in SyntheticComputability.Shared.partial]
_ =! _ [in SyntheticComputability.Shared.partial]
eq_dec _ [in SyntheticComputability.Shared.Dec]
fun! ⟨ _ , _ ⟩ => _ [in SyntheticComputability.Shared.prelim]
if! _ is _ then _ else _ [in SyntheticComputability.Shared.prelim]
( _ × _ × .. × _ ) [in SyntheticComputability.Shared.ListAutomation]
[ _ | _ ∈ _ ] [in SyntheticComputability.Shared.ListAutomation]
[ _ | _ ∈ _ , _ ] [in SyntheticComputability.Shared.ListAutomation]
⟨ _ , _ ⟩ [in SyntheticComputability.Axioms.axioms]
Module Index
E
EmbedNatNotations [in SyntheticComputability.Shared.embed_nat]Variable Index
A
assm_part.G [in SyntheticComputability.Axioms.axioms]assm_part.F [in SyntheticComputability.Axioms.axioms]
assm_EA'.ax [in SyntheticComputability.Axioms.axioms]
assm.ax [in SyntheticComputability.Axioms.halting]
C
Cantor.A [in SyntheticComputability.Axioms.axioms]Cantor.g [in SyntheticComputability.Axioms.axioms]
CT_wrong.model [in SyntheticComputability.Axioms.principles]
E
enumerator_list_enumerator.e [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]enumerator_list_enumerator.T [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator.X [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator.T [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator.e [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator.p [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enumerator_list_enumerator.X [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
F
Filter.X [in SyntheticComputability.Shared.FilterFacts]fix_enum.e_enum [in SyntheticComputability.Axioms.kleenetree]
fix_enum.e [in SyntheticComputability.Axioms.kleenetree]
fix_tree.ℓ_injective [in SyntheticComputability.Axioms.baire_cantor]
fix_tree.enumerable_leafs [in SyntheticComputability.Axioms.baire_cantor]
fix_tree.ℓ [in SyntheticComputability.Axioms.baire_cantor]
fix_tree.T_K [in SyntheticComputability.Axioms.baire_cantor]
I
Inf.f' [in SyntheticComputability.Synthetic.Infinite]Inf.Gen.f [in SyntheticComputability.Synthetic.Infinite]
Inf.Gen.Hf [in SyntheticComputability.Synthetic.Infinite]
Inf.Gen.Hfp [in SyntheticComputability.Synthetic.Infinite]
Inf.Hf' [in SyntheticComputability.Synthetic.Infinite]
Inf.Hg [in SyntheticComputability.Synthetic.Infinite]
Inf.HX [in SyntheticComputability.Synthetic.Infinite]
Inf.p [in SyntheticComputability.Synthetic.Infinite]
Inf.X [in SyntheticComputability.Synthetic.Infinite]
L
L_list_def.L [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]U
upper_semi_lattice.q [in SyntheticComputability.Synthetic.reductions]upper_semi_lattice.p [in SyntheticComputability.Synthetic.reductions]
W
WKL_to_LPL.T [in SyntheticComputability.Axioms.kleenetree]WO.f [in SyntheticComputability.Axioms.axioms]
Library Index
A
axiomsB
baire_cantorD
DecDecidabilityFacts
Definitions
E
embed_natEnumerabilityFacts
equiv_on
F
FilterFactsH
haltingI
InfiniteK
kleenetreeL
ListAutomationListEnumerabilityFacts
M
MoreEnumerabilityFactsP
partialprelim
principles
R
ReducibilityTransportreductions
S
SemiDecidabilityFactsLemma Index
A
AC_0_0_LPO_incompat [in SyntheticComputability.Axioms.principles]AC_0_0_LPO_incompat' [in SyntheticComputability.Axioms.principles]
AC_1_0_Fext_incompat [in SyntheticComputability.Axioms.principles]
AC_1_0_Fext [in SyntheticComputability.Axioms.principles]
AC_rel_to_ADC [in SyntheticComputability.Axioms.principles]
ADC_on'_iff [in SyntheticComputability.Axioms.principles]
app_sum_list_with [in SyntheticComputability.Axioms.baire_cantor]
AUC_to_dec [in SyntheticComputability.Axioms.principles]
B
bounded_longest_path [in SyntheticComputability.Axioms.kleenetree]bounded_to_wellfounded [in SyntheticComputability.Axioms.kleenetree]
bounded_tree_iff [in SyntheticComputability.Axioms.kleenetree]
bounded_iff [in SyntheticComputability.Axioms.kleenetree]
bounded_infinite_contra [in SyntheticComputability.Axioms.kleenetree]
C
Cantor [in SyntheticComputability.Axioms.axioms]computes_ext [in SyntheticComputability.Axioms.axioms]
continuous_G [in SyntheticComputability.Axioms.baire_cantor]
continuous_F [in SyntheticComputability.Axioms.baire_cantor]
coS_ADC_on_weak_to_WKL [in SyntheticComputability.Axioms.kleenetree]
cos_AC_on_weak_to_coS_ADC_on_weak [in SyntheticComputability.Axioms.kleenetree]
countable_enumerable [in SyntheticComputability.Synthetic.EnumerabilityFacts]
countable_discrete [in SyntheticComputability.Synthetic.EnumerabilityFacts]
co_semi_decidable_iff [in SyntheticComputability.Axioms.kleenetree]
co_semi_decidable_stable [in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
co_semi_decidable_and [in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
co_semi_decidable_impl [in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
CTP_to_CT [in SyntheticComputability.Axioms.axioms]
CT_to_EPF [in SyntheticComputability.Axioms.axioms]
CT_to_EPF' [in SyntheticComputability.Axioms.axioms]
CT_to_EA [in SyntheticComputability.Axioms.axioms]
CT_to_EA' [in SyntheticComputability.Axioms.axioms]
CT_Sigma_wrong [in SyntheticComputability.Axioms.principles]
cumul_spec [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
cumul_spec__T [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
cumul_In [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
cum_ge' [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
cum_ge [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
D
decidable_stable [in SyntheticComputability.Synthetic.DecidabilityFacts]decidable_iff [in SyntheticComputability.Synthetic.DecidabilityFacts]
decidable_decidme [in SyntheticComputability.Synthetic.DecidabilityFacts]
decidable_length_T [in SyntheticComputability.Axioms.kleenetree]
decidable_stable [in SyntheticComputability.Axioms.kleenetree]
decidable_AC [in SyntheticComputability.Axioms.principles]
decidable_compl_semi_decidable [in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
decidable_semi_decidable [in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
decider_decide [in SyntheticComputability.Synthetic.DecidabilityFacts]
dec_disj [in SyntheticComputability.Synthetic.DecidabilityFacts]
dec_conj [in SyntheticComputability.Synthetic.DecidabilityFacts]
dec_compl [in SyntheticComputability.Synthetic.DecidabilityFacts]
dec_inf_decidable [in SyntheticComputability.Synthetic.DecidabilityFacts]
dec_count_enum' [in SyntheticComputability.Synthetic.EnumerabilityFacts]
dec_count_enum [in SyntheticComputability.Synthetic.EnumerabilityFacts]
dec_transfer [in SyntheticComputability.Shared.Dec]
dec_DM_impl [in SyntheticComputability.Shared.Dec]
dec_DM_and [in SyntheticComputability.Shared.Dec]
dec_DN [in SyntheticComputability.Shared.Dec]
Dec_false [in SyntheticComputability.Shared.Dec]
Dec_true [in SyntheticComputability.Shared.Dec]
Dec_auto [in SyntheticComputability.Shared.Dec]
Dec_reflect [in SyntheticComputability.Shared.Dec]
dec_to_enum [in SyntheticComputability.Axioms.halting]
dec_bounded_quant [in SyntheticComputability.Axioms.principles]
DGP_to_WLEM [in SyntheticComputability.Axioms.principles]
Diaconescu [in SyntheticComputability.Axioms.principles]
diag [in SyntheticComputability.Axioms.kleenetree]
discrete_list [in SyntheticComputability.Synthetic.DecidabilityFacts]
discrete_option [in SyntheticComputability.Synthetic.DecidabilityFacts]
discrete_sum [in SyntheticComputability.Synthetic.DecidabilityFacts]
discrete_prod [in SyntheticComputability.Synthetic.DecidabilityFacts]
discrete_nat_nat [in SyntheticComputability.Synthetic.DecidabilityFacts]
discrete_nat [in SyntheticComputability.Synthetic.DecidabilityFacts]
discrete_bool [in SyntheticComputability.Synthetic.DecidabilityFacts]
discrete_iff [in SyntheticComputability.Synthetic.DecidabilityFacts]
DM_Sigma_0_1_to_LLPO_split [in SyntheticComputability.Axioms.principles]
DM_Sigma_0_1_iff_totality [in SyntheticComputability.Axioms.principles]
DM_Sigma_0_1_iff_DM_sdec [in SyntheticComputability.Axioms.principles]
DNE_sdec_to_cosdec [in SyntheticComputability.Axioms.principles]
drop_lookup_iff [in SyntheticComputability.Axioms.baire_cantor]
d_co_semi_decidable_impl [in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
d_semi_decidable_impl [in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
E
EA_to_EPF [in SyntheticComputability.Axioms.axioms]EA_to_EA' [in SyntheticComputability.Axioms.axioms]
EA_to_EA'_prf [in SyntheticComputability.Axioms.axioms]
embedP [in SyntheticComputability.Shared.embed_nat]
enumerable_disj [in SyntheticComputability.Synthetic.MoreEnumerabilityFacts]
enumerable_conj [in SyntheticComputability.Synthetic.MoreEnumerabilityFacts]
enumerable_enum [in SyntheticComputability.Synthetic.MoreEnumerabilityFacts]
enumerable_red [in SyntheticComputability.Synthetic.ReducibilityTransport]
enumerable_graph' [in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerable_discrete_countable [in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerable_graph [in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerable_enumerable_T [in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerable_semi_decidable [in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerable_red_K_iff [in SyntheticComputability.Axioms.halting]
enumerable_W [in SyntheticComputability.Axioms.halting]
enumerable_code [in SyntheticComputability.Axioms.principles]
enumerable_AC [in SyntheticComputability.Axioms.principles]
enumerable_leaf [in SyntheticComputability.Axioms.baire_cantor]
enumerable_enum [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enumerable_list [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enumerable__T_list_enumerable [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enumerable_list_enumerable [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enumerates_ext [in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerator_enumerable [in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerator__T_option [in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerator__T_prod [in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerator__T_bool [in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerator__T_unit [in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerator__T_nat [in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerator__T_list [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enumerator_to_list_enumerator [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enum_length [in SyntheticComputability.Axioms.baire_cantor]
enum_enumT [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
EPF_to_EPF_bool [in SyntheticComputability.Axioms.axioms]
EPF_to_EA [in SyntheticComputability.Axioms.axioms]
EPF_to_CT [in SyntheticComputability.Axioms.axioms]
equiv_on_eq [in SyntheticComputability.Axioms.baire_cantor]
exists_leaf [in SyntheticComputability.Axioms.baire_cantor]
F
Fext_hProp_wdisj [in SyntheticComputability.Axioms.principles]Fext_hProp_disj [in SyntheticComputability.Axioms.principles]
Fext_hProp_neg [in SyntheticComputability.Axioms.principles]
filter_comm [in SyntheticComputability.Shared.FilterFacts]
filter_and [in SyntheticComputability.Shared.FilterFacts]
filter_pq_eq [in SyntheticComputability.Shared.FilterFacts]
filter_pq_mono [in SyntheticComputability.Shared.FilterFacts]
filter_fst' [in SyntheticComputability.Shared.FilterFacts]
filter_fst [in SyntheticComputability.Shared.FilterFacts]
filter_app [in SyntheticComputability.Shared.FilterFacts]
filter_id [in SyntheticComputability.Shared.FilterFacts]
filter_mono [in SyntheticComputability.Shared.FilterFacts]
filter_incl [in SyntheticComputability.Shared.FilterFacts]
forall_neg_exists_iff [in SyntheticComputability.Axioms.principles]
forall_neg_exists_iff [in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
F_sur [in SyntheticComputability.Synthetic.Infinite]
F_p [in SyntheticComputability.Synthetic.Infinite]
F_inj [in SyntheticComputability.Synthetic.Infinite]
F_inj' [in SyntheticComputability.Synthetic.Infinite]
F_lt [in SyntheticComputability.Synthetic.Infinite]
F_el [in SyntheticComputability.Synthetic.Infinite]
F_nel [in SyntheticComputability.Synthetic.Infinite]
f_sur [in SyntheticComputability.Synthetic.Infinite]
F_ext [in SyntheticComputability.Axioms.baire_cantor]
F_find_pref_ext [in SyntheticComputability.Axioms.baire_cantor]
F_G_inv [in SyntheticComputability.Axioms.baire_cantor]
F_surj [in SyntheticComputability.Axioms.baire_cantor]
F_inv [in SyntheticComputability.Axioms.baire_cantor]
F_find_pref [in SyntheticComputability.Axioms.baire_cantor]
F_inj [in SyntheticComputability.Axioms.baire_cantor]
F_inj_help [in SyntheticComputability.Axioms.baire_cantor]
F'_length_g [in SyntheticComputability.Axioms.baire_cantor]
F'_eq_lt [in SyntheticComputability.Axioms.baire_cantor]
F'_prefix [in SyntheticComputability.Axioms.baire_cantor]
F'_length [in SyntheticComputability.Axioms.baire_cantor]
F'_offset [in SyntheticComputability.Axioms.baire_cantor]
G
gen [in SyntheticComputability.Synthetic.Infinite]gen_le_f [in SyntheticComputability.Synthetic.Infinite]
gen_spec [in SyntheticComputability.Synthetic.Infinite]
G_zero [in SyntheticComputability.Axioms.axioms]
G_sig [in SyntheticComputability.Axioms.axioms]
G_inv [in SyntheticComputability.Axioms.baire_cantor]
H
help [in SyntheticComputability.Axioms.baire_cantor]Homeo_M_Cantor_Baire_to_KT [in SyntheticComputability.Axioms.baire_cantor]
hProp_disj [in SyntheticComputability.Axioms.principles]
I
infinite_path_to_infinite [in SyntheticComputability.Axioms.kleenetree]inf_path_iff_inf [in SyntheticComputability.Axioms.kleenetree]
inf_to_longest [in SyntheticComputability.Axioms.kleenetree]
inf_T' [in SyntheticComputability.Axioms.kleenetree]
inspect_opt [in SyntheticComputability.Axioms.principles]
in_concat_iff [in SyntheticComputability.Shared.ListAutomation]
in_filter_iff [in SyntheticComputability.Shared.FilterFacts]
In_cumul [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
is_tree_T' [in SyntheticComputability.Axioms.kleenetree]
is_tree_subtree_at_from_inf [in SyntheticComputability.Axioms.kleenetree]
is_tree_subtree_at [in SyntheticComputability.Axioms.kleenetree]
Is_true_neg_iff [in SyntheticComputability.Axioms.kleenetree]
Is_true_iff [in SyntheticComputability.Axioms.kleenetree]
K
KS_LLPO_to_DGP [in SyntheticComputability.Axioms.principles]KS_WLPO_to_WLEM [in SyntheticComputability.Axioms.principles]
KS_LPO_to_LEM [in SyntheticComputability.Axioms.principles]
KT_FAN_contra [in SyntheticComputability.Axioms.kleenetree]
KT_WKL_contra [in SyntheticComputability.Axioms.kleenetree]
KT_to_Homeo_N_nat_bool [in SyntheticComputability.Axioms.baire_cantor]
KT_iff_Homeo_N_nat_bool [in SyntheticComputability.Axioms.baire_cantor]
KT_inj_enum_leafs [in SyntheticComputability.Axioms.baire_cantor]
K_forall_undec [in SyntheticComputability.Axioms.halting]
K_nat_equiv_compl [in SyntheticComputability.Axioms.halting]
K_nat_equiv [in SyntheticComputability.Axioms.halting]
K_compl_undec [in SyntheticComputability.Axioms.halting]
K0_red_K [in SyntheticComputability.Axioms.halting]
K0_enum [in SyntheticComputability.Axioms.halting]
K0_compl_undec [in SyntheticComputability.Axioms.halting]
K0_undec [in SyntheticComputability.Axioms.halting]
K0_enumerable [in SyntheticComputability.Axioms.halting]
L
leaf_prefix [in SyntheticComputability.Axioms.baire_cantor]least_ex [in SyntheticComputability.Axioms.principles]
LEM_WKL_KT [in SyntheticComputability.Axioms.kleenetree]
LEM_FAN_KT [in SyntheticComputability.Axioms.kleenetree]
LEM_to_KS [in SyntheticComputability.Axioms.principles]
LEM_to_LPO [in SyntheticComputability.Axioms.principles]
LEM_to_IP [in SyntheticComputability.Axioms.principles]
LEM_to_DGP [in SyntheticComputability.Axioms.principles]
length_inv [in SyntheticComputability.Axioms.kleenetree]
listable_lt [in SyntheticComputability.Axioms.kleenetree]
listable_has_max [in SyntheticComputability.Axioms.kleenetree]
listable_prefix [in SyntheticComputability.Axioms.kleenetree]
listable_list_length_lt [in SyntheticComputability.Axioms.kleenetree]
listable_list_length [in SyntheticComputability.Axioms.kleenetree]
listable_exists_dec [in SyntheticComputability.Axioms.kleenetree]
listable_forall_dec [in SyntheticComputability.Axioms.kleenetree]
listable_list_length_lt [in SyntheticComputability.Axioms.baire_cantor]
list_enumerator_to_cumul [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
list_enumerable__T_enumerable [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
list_enumerable_enumerable [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
list_enumerator_enumerator [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
list_enumerator_to_enumerator [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
LLPO_coS_AC_on_to_coS_AC_on_weak [in SyntheticComputability.Axioms.kleenetree]
LLPO_LLPO_tree_iff [in SyntheticComputability.Axioms.kleenetree]
LLPO_split_to_LLPO [in SyntheticComputability.Axioms.principles]
LLPO_iff_DGP_sdec [in SyntheticComputability.Axioms.principles]
LLPO_to_DM_Sigma_0_1 [in SyntheticComputability.Axioms.principles]
LL_F [in SyntheticComputability.Synthetic.Infinite]
LL_f [in SyntheticComputability.Synthetic.Infinite]
LL_cum [in SyntheticComputability.Synthetic.Infinite]
lookup_map [in SyntheticComputability.Axioms.kleenetree]
LPO_tree_iff [in SyntheticComputability.Axioms.kleenetree]
LPO_to_MP [in SyntheticComputability.Axioms.principles]
LPO_MP_WLPO_iff [in SyntheticComputability.Axioms.principles]
LPO_semidecidable_iff [in SyntheticComputability.Axioms.principles]
LPO_to_WLPO [in SyntheticComputability.Axioms.principles]
lt_acc [in SyntheticComputability.Synthetic.Infinite]
LX_p [in SyntheticComputability.Synthetic.Infinite]
LX_NoDup [in SyntheticComputability.Synthetic.Infinite]
LX_el [in SyntheticComputability.Synthetic.Infinite]
LX_len [in SyntheticComputability.Synthetic.Infinite]
L_list_cumulative [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
M
map_nth_seq [in SyntheticComputability.Axioms.baire_cantor]map_seq_eq [in SyntheticComputability.Axioms.baire_cantor]
max_list_spec [in SyntheticComputability.Axioms.principles]
max_list_with_spec [in SyntheticComputability.Axioms.principles]
max_list_spec' [in SyntheticComputability.Axioms.principles]
max_list_with_spec' [in SyntheticComputability.Axioms.principles]
max_list_incl [in SyntheticComputability.Axioms.baire_cantor]
mkpart_hasvalue [in SyntheticComputability.Shared.partial]
mkpart_hasvalue2 [in SyntheticComputability.Shared.partial]
mkpart_ter [in SyntheticComputability.Shared.partial]
mkpart_hasvalue1 [in SyntheticComputability.Shared.partial]
monotonic_agnostic [in SyntheticComputability.Shared.partial]
MP_tree_iff' [in SyntheticComputability.Axioms.kleenetree]
MP_tree_iff [in SyntheticComputability.Axioms.kleenetree]
MP_cosdec_to_sdec [in SyntheticComputability.Axioms.principles]
MP_iff_sdec_weak_total [in SyntheticComputability.Axioms.principles]
MP_semidecidable_to_Post_logical [in SyntheticComputability.Axioms.principles]
MP_to_MP_semidecidable [in SyntheticComputability.Axioms.principles]
MP_IP_LPO [in SyntheticComputability.Axioms.principles]
mu_nat [in SyntheticComputability.Axioms.axioms]
mu_ter [in SyntheticComputability.Shared.partial]
mu_nat_min [in SyntheticComputability.Shared.partial]
mu_nat_p_irrel [in SyntheticComputability.Shared.prelim]
mu_nat_p_least [in SyntheticComputability.Shared.prelim]
mu_nat_p_min [in SyntheticComputability.Shared.prelim]
N
neg_neg_XM [in SyntheticComputability.Axioms.principles]nil_no_leaf [in SyntheticComputability.Axioms.baire_cantor]
not_bounded_infinite_iff [in SyntheticComputability.Axioms.kleenetree]
not_bounded_infinite [in SyntheticComputability.Axioms.kleenetree]
not_bounded_infinite' [in SyntheticComputability.Axioms.kleenetree]
nth_sig [in SyntheticComputability.Axioms.baire_cantor]
nxt_iter [in SyntheticComputability.Axioms.baire_cantor]
O
ofenum_ter [in SyntheticComputability.Axioms.axioms]ofenum_spec [in SyntheticComputability.Axioms.axioms]
ofenum_ter_iff [in SyntheticComputability.Axioms.axioms]
P
partial_to_total [in SyntheticComputability.Axioms.axioms]path_wellfounded_contra [in SyntheticComputability.Axioms.kleenetree]
Pext_to_PI [in SyntheticComputability.Axioms.principles]
Post_to_MP [in SyntheticComputability.Axioms.principles]
Post_logical_to_Post [in SyntheticComputability.Axioms.principles]
prefixes_inv [in SyntheticComputability.Axioms.kleenetree]
prefix_length_eq [in SyntheticComputability.Axioms.kleenetree]
prefix_take_iff [in SyntheticComputability.Axioms.baire_cantor]
projection [in SyntheticComputability.Synthetic.EnumerabilityFacts]
projection' [in SyntheticComputability.Synthetic.EnumerabilityFacts]
R
red_m_transports_stable [in SyntheticComputability.Synthetic.reductions]red_m_decidable_nontriv [in SyntheticComputability.Synthetic.reductions]
red_m_join_least [in SyntheticComputability.Synthetic.reductions]
red_m_join_q [in SyntheticComputability.Synthetic.reductions]
red_m_join_p [in SyntheticComputability.Synthetic.reductions]
red_m_compl_compl_PEM_3 [in SyntheticComputability.Synthetic.reductions]
red_m_compl_compl_PEM_2 [in SyntheticComputability.Synthetic.reductions]
red_m_compl_compl_PEM [in SyntheticComputability.Synthetic.reductions]
red_m_complement [in SyntheticComputability.Synthetic.reductions]
red_m_transports [in SyntheticComputability.Synthetic.reductions]
red_m_transitive [in SyntheticComputability.Synthetic.reductions]
reflects_prv_iff [in SyntheticComputability.Synthetic.DecidabilityFacts]
reflects_prv [in SyntheticComputability.Synthetic.DecidabilityFacts]
reflects_disj [in SyntheticComputability.Synthetic.DecidabilityFacts]
reflects_conj [in SyntheticComputability.Synthetic.DecidabilityFacts]
reflects_not [in SyntheticComputability.Synthetic.DecidabilityFacts]
reflects_cases [in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
ret_hasvalue_inv [in SyntheticComputability.Shared.partial]
rev_rect [in SyntheticComputability.Axioms.kleenetree]
rev_list_rect [in SyntheticComputability.Axioms.kleenetree]
S
sdec_compute_lor [in SyntheticComputability.Synthetic.SemiDecidabilityFacts]sec_enum [in SyntheticComputability.Axioms.halting]
semidecidable_red [in SyntheticComputability.Synthetic.ReducibilityTransport]
semi_decidable_red_K_iff [in SyntheticComputability.Synthetic.reductions]
semi_decidable_enumerable [in SyntheticComputability.Synthetic.EnumerabilityFacts]
semi_decidable_K [in SyntheticComputability.Axioms.halting]
semi_decidable_ext [in SyntheticComputability.Axioms.principles]
semi_decidable_AC [in SyntheticComputability.Axioms.principles]
semi_decidable_projection_iff [in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
semi_decidable_and [in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
semi_decidable_or [in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
semi_decidable_impl [in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
size_generating [in SyntheticComputability.Axioms.baire_cantor]
sub_dec [in SyntheticComputability.Synthetic.Infinite]
T
take_prefix [in SyntheticComputability.Axioms.kleenetree]take_length_ℓ [in SyntheticComputability.Axioms.baire_cantor]
take_prefix [in SyntheticComputability.Axioms.baire_cantor]
take_take [in SyntheticComputability.Axioms.baire_cantor]
take_seq [in SyntheticComputability.Axioms.baire_cantor]
take_map [in SyntheticComputability.Axioms.baire_cantor]
toenum_spec [in SyntheticComputability.Axioms.axioms]
total_list [in SyntheticComputability.Axioms.principles]
to_dec [in SyntheticComputability.Shared.ListAutomation]
to_Homeo_M_bool_nat [in SyntheticComputability.Axioms.baire_cantor]
to_Homeo_M_nat_bool [in SyntheticComputability.Axioms.baire_cantor]
to_cumul_spec [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
to_cumul_cumulative [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
tree_from_f_bounded_iff_wf [in SyntheticComputability.Axioms.kleenetree]
tree_from_f_bounded_iff [in SyntheticComputability.Axioms.kleenetree]
tree_nil [in SyntheticComputability.Axioms.kleenetree]
T_func_in_n [in SyntheticComputability.Axioms.axioms]
T_inf_sdec_iff [in SyntheticComputability.Axioms.kleenetree]
T_inf_sdec_iff' [in SyntheticComputability.Axioms.kleenetree]
U
unembedP [in SyntheticComputability.Shared.embed_nat]W
WC_N_to_Cont [in SyntheticComputability.Axioms.principles]WC_N_CT_inc [in SyntheticComputability.Axioms.principles]
WKL_to_coS_AC_on_nat_bool [in SyntheticComputability.Axioms.kleenetree]
WKL_to_LLPO [in SyntheticComputability.Axioms.kleenetree]
WKL_to_FAN [in SyntheticComputability.Axioms.kleenetree]
WLEM_to_WLPO [in SyntheticComputability.Axioms.principles]
WLPO_tree_iff [in SyntheticComputability.Axioms.kleenetree]
WLPO_PFP_LLPO_iff [in SyntheticComputability.Axioms.principles]
WLPO_cosemidecidable_iff [in SyntheticComputability.Axioms.principles]
WLPO_semidecidable_iff [in SyntheticComputability.Axioms.principles]
W_self_enumerable [in SyntheticComputability.Axioms.axioms]
W_spec [in SyntheticComputability.Axioms.halting]
X
X_gen [in SyntheticComputability.Synthetic.Infinite]other
ℓ_sig_prf [in SyntheticComputability.Axioms.baire_cantor]ℓ_sig [in SyntheticComputability.Axioms.baire_cantor]
ℓ_leaf [in SyntheticComputability.Axioms.baire_cantor]
Constructor Index
E
EqType [in SyntheticComputability.Shared.Dec]G
GI [in SyntheticComputability.Axioms.axioms]Projection Index
B
bind [in SyntheticComputability.Shared.partial]bind_hasvalue [in SyntheticComputability.Shared.partial]
E
eqType_dec [in SyntheticComputability.Shared.Dec]eqType_X [in SyntheticComputability.Shared.Dec]
equiv_rel_is_equiv [in SyntheticComputability.Shared.equiv_on]
equiv_rel [in SyntheticComputability.Shared.equiv_on]
H
hasvalue [in SyntheticComputability.Shared.partial]hasvalue_det [in SyntheticComputability.Shared.partial]
K
Kleene_inf_exit [in SyntheticComputability.Axioms.kleenetree]Kleene_infinite [in SyntheticComputability.Axioms.kleenetree]
Kleene_T [in SyntheticComputability.Axioms.kleenetree]
M
mu [in SyntheticComputability.Shared.partial]mu_hasvalue [in SyntheticComputability.Shared.partial]
P
par [in SyntheticComputability.Shared.partial]part [in SyntheticComputability.Shared.partial]
par_hasvalue3 [in SyntheticComputability.Shared.partial]
par_hasvalue2 [in SyntheticComputability.Shared.partial]
par_hasvalue1 [in SyntheticComputability.Shared.partial]
R
ret [in SyntheticComputability.Shared.partial]ret_hasvalue [in SyntheticComputability.Shared.partial]
S
seval [in SyntheticComputability.Shared.partial]seval_hasvalue [in SyntheticComputability.Shared.partial]
seval_mono [in SyntheticComputability.Shared.partial]
T
T [in SyntheticComputability.Axioms.axioms]tree_is_tree [in SyntheticComputability.Axioms.kleenetree]
tree_T [in SyntheticComputability.Axioms.kleenetree]
tree_dec [in SyntheticComputability.Axioms.kleenetree]
tree_p [in SyntheticComputability.Axioms.kleenetree]
tree_inhab [in SyntheticComputability.Axioms.kleenetree]
T_mono [in SyntheticComputability.Axioms.axioms]
U
undef [in SyntheticComputability.Shared.partial]undef_hasvalue [in SyntheticComputability.Shared.partial]
Inductive Index
G
G [in SyntheticComputability.Axioms.axioms]Instance Index
A
and_dec [in SyntheticComputability.Shared.Dec]B
bool_equiv [in SyntheticComputability.Shared.equiv_on]bool_eq_dec [in SyntheticComputability.Shared.Dec]
E
el_dec [in SyntheticComputability.Synthetic.Infinite]Empty_set_eq_dec [in SyntheticComputability.Shared.Dec]
enumerator__T_of_list [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
enumerator__T_to_list [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
equiv_part [in SyntheticComputability.Axioms.axioms]
equiv_ran [in SyntheticComputability.Synthetic.EnumerabilityFacts]
ext_equiv [in SyntheticComputability.Shared.equiv_on]
F
False_eq_dec [in SyntheticComputability.Shared.Dec]False_dec [in SyntheticComputability.Shared.Dec]
I
iff_dec [in SyntheticComputability.Shared.Dec]impl_dec [in SyntheticComputability.Shared.Dec]
inf_to_enumerator [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
L
list_in_dec [in SyntheticComputability.Shared.ListAutomation]list_eq_dec [in SyntheticComputability.Shared.Dec]
N
nat_equiv [in SyntheticComputability.Shared.equiv_on]nat_eq_dec [in SyntheticComputability.Shared.Dec]
not_dec [in SyntheticComputability.Shared.Dec]
O
option_eq_dec [in SyntheticComputability.Shared.Dec]or_dec [in SyntheticComputability.Shared.Dec]
P
part_equiv_Equivalence [in SyntheticComputability.Shared.partial]prod_eq_dec [in SyntheticComputability.Shared.Dec]
Proper_decidable [in SyntheticComputability.Synthetic.DecidabilityFacts]
Proper_decides [in SyntheticComputability.Synthetic.DecidabilityFacts]
Prop_equiv [in SyntheticComputability.Shared.equiv_on]
R
red_m_reflexive [in SyntheticComputability.Synthetic.reductions]S
sum_eq_dec [in SyntheticComputability.Shared.Dec]T
True_eq_dec [in SyntheticComputability.Shared.Dec]True_dec [in SyntheticComputability.Shared.Dec]
U
unit_eq_dec [in SyntheticComputability.Shared.Dec]Section Index
A
assm [in SyntheticComputability.Axioms.halting]assm_part [in SyntheticComputability.Axioms.axioms]
assm_EA' [in SyntheticComputability.Axioms.axioms]
assm_model_of_computation [in SyntheticComputability.Axioms.axioms]
assume_part [in SyntheticComputability.Shared.partial]
C
Cantor [in SyntheticComputability.Axioms.axioms]CT_wrong [in SyntheticComputability.Axioms.principles]
E
enumerator_list_enumerator [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]enumerator_list_enumerator [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
F
Filter [in SyntheticComputability.Shared.FilterFacts]fix_enum [in SyntheticComputability.Axioms.kleenetree]
fix_tree [in SyntheticComputability.Axioms.baire_cantor]
I
Inf [in SyntheticComputability.Synthetic.Infinite]Inf.Gen [in SyntheticComputability.Synthetic.Infinite]
L
L_list_def [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]R
Reverse_Induction [in SyntheticComputability.Axioms.kleenetree]U
upper_semi_lattice [in SyntheticComputability.Synthetic.reductions]W
WKL_to_LPL [in SyntheticComputability.Axioms.kleenetree]WO [in SyntheticComputability.Axioms.axioms]
Abbreviation Index
C
cumul [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]E
enumerator__T [in SyntheticComputability.Synthetic.EnumerabilityFacts]L
list_enumerator__T [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]N
nth [in SyntheticComputability.Axioms.baire_cantor]R
retraction [in SyntheticComputability.Synthetic.EnumerabilityFacts]S
stable [in SyntheticComputability.Synthetic.DecidabilityFacts]W
W [in SyntheticComputability.Axioms.axioms]W [in SyntheticComputability.Axioms.halting]
other
φ [in SyntheticComputability.Axioms.halting]φ_spec [in SyntheticComputability.Axioms.halting]
Definition Index
A
AC [in SyntheticComputability.Axioms.principles]ACC [in SyntheticComputability.Axioms.principles]
AC_1_0 [in SyntheticComputability.Axioms.principles]
AC_0_0 [in SyntheticComputability.Axioms.principles]
AC_on [in SyntheticComputability.Axioms.principles]
ADC [in SyntheticComputability.Axioms.principles]
ADC_on' [in SyntheticComputability.Axioms.principles]
ADC_on [in SyntheticComputability.Axioms.principles]
agnostic [in SyntheticComputability.Shared.partial]
AUC_on [in SyntheticComputability.Axioms.principles]
B
bool_enum [in SyntheticComputability.Synthetic.EnumerabilityFacts]bounded_tree' [in SyntheticComputability.Axioms.kleenetree]
bounded_tree [in SyntheticComputability.Axioms.kleenetree]
C
compl [in SyntheticComputability.Synthetic.reductions]compl [in SyntheticComputability.Synthetic.Definitions]
Cont [in SyntheticComputability.Axioms.principles]
continuous [in SyntheticComputability.Axioms.baire_cantor]
coS_ADC_on_weak [in SyntheticComputability.Axioms.kleenetree]
coS_AC_on_weak [in SyntheticComputability.Axioms.kleenetree]
coS_AC_on [in SyntheticComputability.Axioms.kleenetree]
countable [in SyntheticComputability.Synthetic.EnumerabilityFacts]
co_semi_decidable [in SyntheticComputability.Synthetic.SemiDecidabilityFacts]
CT [in SyntheticComputability.Axioms.axioms]
CTP [in SyntheticComputability.Axioms.axioms]
CT_Sigma [in SyntheticComputability.Axioms.principles]
cumulative [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
D
D [in SyntheticComputability.Axioms.kleenetree]d [in SyntheticComputability.Axioms.kleenetree]
Dec [in SyntheticComputability.Shared.Dec]
dec [in SyntheticComputability.Shared.Dec]
decidable [in SyntheticComputability.Synthetic.Definitions]
decider [in SyntheticComputability.Synthetic.Definitions]
DGP [in SyntheticComputability.Axioms.principles]
DGP_sdec [in SyntheticComputability.Axioms.principles]
discrete [in SyntheticComputability.Synthetic.DecidabilityFacts]
DM_sdec [in SyntheticComputability.Axioms.principles]
DM_Sigma_0_1 [in SyntheticComputability.Axioms.principles]
DNE [in SyntheticComputability.Axioms.principles]
dummy [in SyntheticComputability.Synthetic.Infinite]
E
e [in SyntheticComputability.Axioms.axioms]EA [in SyntheticComputability.Axioms.axioms]
EA' [in SyntheticComputability.Axioms.axioms]
el_T [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
embed [in SyntheticComputability.Shared.embed_nat]
enumerable [in SyntheticComputability.Synthetic.Definitions]
enumerable__T [in SyntheticComputability.Synthetic.EnumerabilityFacts]
enumerator [in SyntheticComputability.Synthetic.Definitions]
enumerator__T' [in SyntheticComputability.Synthetic.EnumerabilityFacts]
EPF [in SyntheticComputability.Axioms.axioms]
EPF_bool [in SyntheticComputability.Axioms.axioms]
eval [in SyntheticComputability.Shared.partial]
eval_hasvalue [in SyntheticComputability.Shared.partial]
eval' [in SyntheticComputability.Shared.partial]
extend [in SyntheticComputability.Axioms.baire_cantor]
F
F [in SyntheticComputability.Synthetic.Infinite]f [in SyntheticComputability.Synthetic.Infinite]
F [in SyntheticComputability.Axioms.baire_cantor]
FAN [in SyntheticComputability.Axioms.kleenetree]
Fext [in SyntheticComputability.Axioms.principles]
F' [in SyntheticComputability.Axioms.baire_cantor]
G
G [in SyntheticComputability.Axioms.baire_cantor]generating [in SyntheticComputability.Synthetic.Infinite]
gen' [in SyntheticComputability.Synthetic.Infinite]
H
Homeo_M [in SyntheticComputability.Axioms.baire_cantor]hProp [in SyntheticComputability.Axioms.principles]
I
inconsistent [in SyntheticComputability.Axioms.kleenetree]infinite [in SyntheticComputability.Synthetic.Infinite]
infinite_path [in SyntheticComputability.Axioms.kleenetree]
infinite_tree [in SyntheticComputability.Axioms.kleenetree]
inf_semi_decidable [in SyntheticComputability.Synthetic.Definitions]
inf_enumerable [in SyntheticComputability.Synthetic.Definitions]
inf_decidable [in SyntheticComputability.Synthetic.Definitions]
inf_list_enumerable__T [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
injective [in SyntheticComputability.Synthetic.Infinite]
IP [in SyntheticComputability.Axioms.principles]
is_true [in SyntheticComputability.Shared.Dec]
is_infinite_tree [in SyntheticComputability.Axioms.kleenetree]
J
join [in SyntheticComputability.Synthetic.reductions]K
K [in SyntheticComputability.Synthetic.reductions]KS [in SyntheticComputability.Axioms.principles]
KT [in SyntheticComputability.Axioms.kleenetree]
K_nat [in SyntheticComputability.Axioms.halting]
K0 [in SyntheticComputability.Axioms.halting]
L
leaf [in SyntheticComputability.Axioms.baire_cantor]least [in SyntheticComputability.Axioms.axioms]
LEM [in SyntheticComputability.Axioms.principles]
le_f [in SyntheticComputability.Synthetic.Infinite]
listable [in SyntheticComputability.Axioms.kleenetree]
list_enumerable__T [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
list_enumerator__T' [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
list_enumerable [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
list_enumerator [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
LL [in SyntheticComputability.Synthetic.Infinite]
LLPO [in SyntheticComputability.Axioms.principles]
LLPO_tree [in SyntheticComputability.Axioms.kleenetree]
LLPO_split [in SyntheticComputability.Axioms.principles]
LPL [in SyntheticComputability.Axioms.kleenetree]
LPO [in SyntheticComputability.Axioms.principles]
LPO_tree [in SyntheticComputability.Axioms.kleenetree]
LPO_semidecidable [in SyntheticComputability.Axioms.principles]
LX [in SyntheticComputability.Synthetic.Infinite]
L_T [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
L_list [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
M
mkpart [in SyntheticComputability.Shared.partial]modulus [in SyntheticComputability.Axioms.baire_cantor]
monotonic [in SyntheticComputability.Shared.partial]
MP [in SyntheticComputability.Axioms.principles]
MP_tree' [in SyntheticComputability.Axioms.kleenetree]
MP_tree [in SyntheticComputability.Axioms.kleenetree]
MP_semidecidable [in SyntheticComputability.Axioms.principles]
mu_nat_dec [in SyntheticComputability.Axioms.axioms]
mu_nat [in SyntheticComputability.Shared.partial]
mu_nat_spec [in SyntheticComputability.Shared.prelim]
mu_nat [in SyntheticComputability.Shared.prelim]
mu_nat_p [in SyntheticComputability.Shared.prelim]
N
nat_enum [in SyntheticComputability.Synthetic.EnumerabilityFacts]nxt [in SyntheticComputability.Axioms.baire_cantor]
O
ofenum [in SyntheticComputability.Axioms.axioms]option_enum [in SyntheticComputability.Synthetic.EnumerabilityFacts]
P
PEM [in SyntheticComputability.Synthetic.reductions]Pext [in SyntheticComputability.Axioms.principles]
PFP [in SyntheticComputability.Axioms.principles]
PI [in SyntheticComputability.Axioms.principles]
Post [in SyntheticComputability.Axioms.principles]
Post_logical [in SyntheticComputability.Axioms.principles]
prod_enum [in SyntheticComputability.Synthetic.EnumerabilityFacts]
R
reduces_m [in SyntheticComputability.Synthetic.reductions]red_m [in SyntheticComputability.Synthetic.reductions]
reflects [in SyntheticComputability.Synthetic.Definitions]
retract [in SyntheticComputability.Synthetic.EnumerabilityFacts]
retraction' [in SyntheticComputability.Synthetic.EnumerabilityFacts]
S
semi_decidable [in SyntheticComputability.Synthetic.Definitions]semi_decider [in SyntheticComputability.Synthetic.Definitions]
stable [in SyntheticComputability.Synthetic.reductions]
subtree_at [in SyntheticComputability.Axioms.kleenetree]
surjection_wrt [in SyntheticComputability.Shared.equiv_on]
T
toenum [in SyntheticComputability.Axioms.axioms]to_cumul [in SyntheticComputability.Synthetic.ListEnumerabilityFacts]
tree_from [in SyntheticComputability.Axioms.kleenetree]
T_inf_sdec [in SyntheticComputability.Axioms.kleenetree]
T_K [in SyntheticComputability.Axioms.kleenetree]
T' [in SyntheticComputability.Axioms.kleenetree]
U
unembed [in SyntheticComputability.Shared.embed_nat]unit_enum [in SyntheticComputability.Synthetic.EnumerabilityFacts]
Unnamed_thm2 [in SyntheticComputability.Axioms.principles]
Unnamed_thm1 [in SyntheticComputability.Axioms.principles]
Unnamed_thm0 [in SyntheticComputability.Axioms.principles]
Unnamed_thm [in SyntheticComputability.Axioms.principles]
W
W [in SyntheticComputability.Axioms.axioms]WC_N [in SyntheticComputability.Axioms.principles]
wellfounded_tree [in SyntheticComputability.Axioms.kleenetree]
WKL [in SyntheticComputability.Axioms.kleenetree]
WLEM [in SyntheticComputability.Axioms.principles]
WLPO [in SyntheticComputability.Axioms.principles]
WLPO_tree [in SyntheticComputability.Axioms.kleenetree]
WLPO_cosemidecidable [in SyntheticComputability.Axioms.principles]
WLPO_semidecidable [in SyntheticComputability.Axioms.principles]
other
φ [in SyntheticComputability.Axioms.axioms]Record Index
E
eqType [in SyntheticComputability.Shared.Dec]equiv_on [in SyntheticComputability.Shared.equiv_on]
I
is_tree [in SyntheticComputability.Axioms.kleenetree]K
Kleene_tree [in SyntheticComputability.Axioms.kleenetree]M
model_of_computation [in SyntheticComputability.Axioms.axioms]P
partiality [in SyntheticComputability.Shared.partial]T
tree [in SyntheticComputability.Axioms.kleenetree]| 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 | (686 entries) |
| Notation 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 | (19 entries) |
| Module 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 | (1 entry) |
| Variable 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 | (35 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 | (21 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 | (349 entries) |
| Constructor 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 | (2 entries) |
| Projection 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 | (32 entries) |
| Inductive 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 | (1 entry) |
| Instance 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 | (32 entries) |
| Section 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 | (19 entries) |
| Abbreviation 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 | (10 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 | (158 entries) |
| Record 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) |