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 (541 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 (17 entries)
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 (30 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 (14 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 (281 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 (23 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 (4 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 (8 entries)
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 (37 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 (15 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 (110 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 (2 entries)

Global Index

A

Add [definition, in L.Encodings]
Add_correct [lemma, in L.Encodings]
and_dec [instance, in L.Preliminaries]
App [definition, in L.Encodings]
app [constructor, in L.L]
Append [definition, in L.Enumerable]
Append_correct [lemma, in L.Enumerable]
App_correct [lemma, in L.Encodings]
app_equiv [instance, in L.L]
app_eva [lemma, in L.L]
app_closed [lemma, in L.L]
app_equi_proper [instance, in L.Preliminaries]


B

bapp [constructor, in L.L]
benc [definition, in L.Encodings]
benc_proc [lemma, in L.Encodings]
beta [lemma, in L.Tactics]
beta [definition, in L.Enumerable]
blambda [constructor, in L.L]
bool_eq_dec [instance, in L.Preliminaries]
bound [definition, in L.L]
Bound [definition, in L.Rice]
bound_subst [lemma, in L.L]
bound_closed_k [lemma, in L.L]
bound_ge [lemma, in L.L]
Bound_correct [lemma, in L.Rice]
bter [constructor, in L.L]
bterm [inductive, in L.L]
bvar [constructor, in L.L]


C

C [definition, in L.L]
C [definition, in L.Choose]
card [definition, in L.Preliminaries]
Cardinality [section, in L.Preliminaries]
Cardinality.X [variable, in L.Preliminaries]
card_equi_proper [instance, in L.Preliminaries]
card_0 [lemma, in L.Preliminaries]
card_cons_rem [lemma, in L.Preliminaries]
card_cons [lemma, in L.Preliminaries]
card_ex [lemma, in L.Preliminaries]
card_or [lemma, in L.Preliminaries]
card_lt [lemma, in L.Preliminaries]
card_equi [lemma, in L.Preliminaries]
card_eq [lemma, in L.Preliminaries]
card_le [lemma, in L.Preliminaries]
cChoice [definition, in L.Interpreter]
Choose [library]
church_rosser [lemma, in L.L]
cLam [definition, in L.InterpreterResults]
closed [definition, in L.L]
Closed [definition, in L.Rice]
closed_app [lemma, in L.L]
closed_subst [lemma, in L.L]
closed_under_proc [definition, in L.Rice]
complement [definition, in L.DecidableRecognisable]
complete_induction [lemma, in L.Preliminaries]
computable_fun [definition, in L.Reduction]
computable_gen [definition, in L.Reduction]
computable_eva [lemma, in L.Interpreter]
confluence [lemma, in L.L]
Cons [definition, in L.Enumerable]
cons_equi_proper [instance, in L.Preliminaries]
Cons_correct [lemma, in L.Enumerable]
convert [definition, in L.L]
convert' [definition, in L.L]
countable [record, in L.Enumerable]
Countable [constructor, in L.Enumerable]
cumulative [definition, in L.Enumerable]
cum_L [lemma, in L.Enumerable]
cum_nth_eq [lemma, in L.Enumerable]
cum_nth [lemma, in L.Enumerable]
cum_ge' [lemma, in L.Enumerable]
cum_ge [lemma, in L.Enumerable]
cum_nth_ex [lemma, in L.Enumerable]
cum_length [lemma, in L.Enumerable]
C_sound [lemma, in L.Choose]
C_complete [lemma, in L.Choose]


D

D [definition, in L.L]
DA [lemma, in L.Markov]
dec [definition, in L.Preliminaries]
decidable [definition, in L.DecidableRecognisable]
DecidableRecognisable [library]
decidable_complement [lemma, in L.DecidableRecognisable]
decidable_union [lemma, in L.DecidableRecognisable]
decidable_intersection [lemma, in L.DecidableRecognisable]
decidable_spec [lemma, in L.DecidableRecognisable]
decidable_full [lemma, in L.Extras]
decidable_empty [lemma, in L.Extras]
decidable_finite [lemma, in L.Extras]
decidable_ext [lemma, in L.Extras]
decidable_dec [lemma, in L.Interpreter]
decidable_proc [lemma, in L.Rice]
decidable_lam [lemma, in L.Rice]
decidable_closed [lemma, in L.Rice]
decides [definition, in L.DecidableRecognisable]
decision [definition, in L.Preliminaries]
decode [definition, in L.Interpreter]
decode_correct2 [lemma, in L.Interpreter]
decode_correct [lemma, in L.Interpreter]
dec_rec [lemma, in L.DecidableRecognisable]
dec_recognisable [lemma, in L.DecidableRecognisable]
dec_pdec [lemma, in L.Interpreter]
dec_prop_iff [lemma, in L.Preliminaries]
dec_DM_impl [lemma, in L.Preliminaries]
dec_DM_and [lemma, in L.Preliminaries]
dec_DN [lemma, in L.Preliminaries]
dec_total [lemma, in L.Rice]
Dupfree [section, in L.Preliminaries]
dupfree [inductive, in L.Preliminaries]
dupfreeC [constructor, in L.Preliminaries]
DupfreeLength [section, in L.Preliminaries]
DupfreeLength.X [variable, in L.Preliminaries]
dupfreeN [constructor, in L.Preliminaries]
dupfree_equi [lemma, in L.Preliminaries]
dupfree_ex [lemma, in L.Preliminaries]
dupfree_lt [lemma, in L.Preliminaries]
dupfree_eq [lemma, in L.Preliminaries]
dupfree_le [lemma, in L.Preliminaries]
dupfree_reorder [lemma, in L.Preliminaries]
dupfree_undup [lemma, in L.Preliminaries]
dupfree_dec [lemma, in L.Preliminaries]
dupfree_filter [lemma, in L.Preliminaries]
dupfree_map [lemma, in L.Preliminaries]
dupfree_inv [lemma, in L.Preliminaries]
Dupfree.X [variable, in L.Preliminaries]
D_pi [lemma, in L.Rice]


E

E [definition, in L.InterpreterResults]
el_pos [lemma, in L.Preliminaries]
enc [definition, in L.Encodings]
Encodings [library]
enc_inj [lemma, in L.Encodings]
enc_injective [lemma, in L.Encodings]
enc_proc [lemma, in L.Encodings]
enum [definition, in L.Enumerable]
EnumCount [section, in L.Enumerable]
EnumCount.beta [variable, in L.Enumerable]
EnumCount.Cumulative [section, in L.Enumerable]
EnumCount.Cumulative.cum [variable, in L.Enumerable]
EnumCount.Cumulative.L [variable, in L.Enumerable]
EnumCount.d [variable, in L.Enumerable]
EnumCount.L [variable, in L.Enumerable]
EnumCount.X [variable, in L.Enumerable]
enumerable [definition, in L.Enumerable]
Enumerable [library]
enumerable_all [lemma, in L.Enumerable]
enumerable_recognisable [lemma, in L.Enumerable]
enum_term [lemma, in L.Enumerable]
enum_count [lemma, in L.Enumerable]
Eq [definition, in L.Enumerable]
EqN [definition, in L.InterpreterResults]
EqN_correct [lemma, in L.InterpreterResults]
eqRef [constructor, in L.L]
eqStep [constructor, in L.L]
eqSym [constructor, in L.L]
eqTrans [constructor, in L.L]
Equi [section, in L.Preliminaries]
equi [definition, in L.Preliminaries]
equiv [inductive, in L.L]
equiv_spec_decidable [lemma, in L.DecidableRecognisable]
equiv_eva [lemma, in L.L]
equiv_evaluates [lemma, in L.L]
equiv_star_lam [lemma, in L.L]
equiv_Equivalence [instance, in L.L]
equiv_trans_r [lemma, in L.Tactics]
equiv_trans_l [lemma, in L.Tactics]
equiv_R_trans [lemma, in L.Tactics]
equiv_eval [lemma, in L.Interpreter]
equiv_semantic [lemma, in L.Rice]
equi_rotate [lemma, in L.Preliminaries]
equi_shift [lemma, in L.Preliminaries]
equi_swap [lemma, in L.Preliminaries]
equi_dup [lemma, in L.Preliminaries]
equi_push [lemma, in L.Preliminaries]
equi_Equivalence [instance, in L.Preliminaries]
Equi.X [variable, in L.Preliminaries]
eq_dec_string [instance, in L.L]
Eq_correct [lemma, in L.Enumerable]
Eq_correct' [lemma, in L.Enumerable]
eva [definition, in L.L]
eval [definition, in L.Interpreter]
evaluates [inductive, in L.L]
evaluatesin [definition, in L.L]
evaluatesin_equiv_subrelation [instance, in L.L]
evaluates_equiv_subrelation [instance, in L.L]
evaluates_proper [instance, in L.L]
evaluates_equiv [lemma, in L.L]
evaluates_star [lemma, in L.L]
evaluates_D [lemma, in L.L]
evaluates_closed [lemma, in L.L]
evaluates_bound [lemma, in L.L]
evaluates_abst [lemma, in L.L]
evaluates_app [constructor, in L.L]
evaluates_lam [constructor, in L.L]
evaluates_eval [lemma, in L.Interpreter]
eval_lambda [lemma, in L.Interpreter]
eval_equiv [lemma, in L.Interpreter]
eval_evaluates [lemma, in L.Interpreter]
eval_step [lemma, in L.Interpreter]
eval_S [lemma, in L.Interpreter]
eva_dec [lemma, in L.DecidableRecognisable]
eva_red [lemma, in L.Reduction]
eva_proper [instance, in L.L]
eva_D [lemma, in L.L]
eva_Omega [lemma, in L.L]
exh_L [lemma, in L.Enumerable]
Extras [library]
E_complete [lemma, in L.InterpreterResults]
E_sound [lemma, in L.InterpreterResults]
E_S [lemma, in L.InterpreterResults]
E_correct [lemma, in L.InterpreterResults]
E_rec_app_Sn_3 [lemma, in L.InterpreterResults]
E_rec_app_Sn_2 [lemma, in L.InterpreterResults]
E_rec_app_Sn_1 [lemma, in L.InterpreterResults]


F

f [projection, in L.Reduction]
F [definition, in L.L]
False_dec [instance, in L.Preliminaries]
filter [definition, in L.Preliminaries]
FilterLemmas [section, in L.Preliminaries]
FilterLemmas.p [variable, in L.Preliminaries]
FilterLemmas.X [variable, in L.Preliminaries]
filter_fst' [lemma, in L.Preliminaries]
filter_app [lemma, in L.Preliminaries]
filter_fst [lemma, in L.Preliminaries]
filter_mono [lemma, in L.Preliminaries]
filter_incl [lemma, in L.Preliminaries]
finite [definition, in L.Extras]
FirstFixedPoint [lemma, in L.Extras]
fix_u.test_u [variable, in L.Choose]
fix_u.proc_u [variable, in L.Choose]
fix_u.u [variable, in L.Choose]
fix_u [section, in L.Choose]
Fix_X.enc_proc [variable, in L.Enumerable]
Fix_X.enc [variable, in L.Enumerable]
Fix_X.X [variable, in L.Enumerable]
Fix_X [section, in L.Enumerable]
Fix_f.total_u [variable, in L.Enumerable]
Fix_f.proc_u [variable, in L.Enumerable]
Fix_f.u [variable, in L.Enumerable]
Fix_f [section, in L.Enumerable]
f_comp [projection, in L.Reduction]
f_red [projection, in L.Reduction]
F_correct [lemma, in L.L]
F_eva [lemma, in L.L]


H

H [definition, in L.Por]
H [definition, in L.Choose]
H [definition, in L.InterpreterResults]
H_inv [lemma, in L.Por]
H_test [lemma, in L.Por]
H_rec [lemma, in L.Por]
H_proc [lemma, in L.Por]
H_correct [lemma, in L.Choose]
H_0_n [lemma, in L.Choose]
H_n_Sn [lemma, in L.Choose]
H_ok [lemma, in L.Choose]
H_rec [lemma, in L.Choose]
H_proc [lemma, in L.InterpreterResults]
H_inv [lemma, in L.InterpreterResults]
H_test [lemma, in L.InterpreterResults]
H_test [lemma, in L.Enumerable]
H_proc [lemma, in L.Enumerable]
H_rec [lemma, in L.Enumerable]


I

I [definition, in L.L]
iff_dec [instance, in L.Preliminaries]
impl_dec [instance, in L.Preliminaries]
inclp [definition, in L.Preliminaries]
Inclusion [section, in L.Preliminaries]
Inclusion.X [variable, in L.Preliminaries]
incl_preorder [instance, in L.Preliminaries]
incl_equi_proper [instance, in L.Preliminaries]
incl_lrcons [lemma, in L.Preliminaries]
incl_rcons [lemma, in L.Preliminaries]
incl_lcons [lemma, in L.Preliminaries]
incl_shift [lemma, in L.Preliminaries]
incl_nil_eq [lemma, in L.Preliminaries]
incl_map [lemma, in L.Preliminaries]
incl_nil [lemma, in L.Preliminaries]
Inj [definition, in L.Enumerable]
Interpreter [library]
InterpreterResults [library]
intersection [definition, in L.DecidableRecognisable]
in_rem_iff [lemma, in L.Preliminaries]
in_filter_iff [lemma, in L.Preliminaries]
in_equi_proper [instance, in L.Preliminaries]
in_cons_neq [lemma, in L.Preliminaries]
in_sing [lemma, in L.Preliminaries]
I_neq_Omega [lemma, in L.L]


L

L [definition, in L.Enumerable]
L [library]
Lam [definition, in L.Encodings]
lam [definition, in L.L]
lambda [constructor, in L.L]
Lambda [definition, in L.Rice]
lambda_lam [lemma, in L.L]
Lambda_correct [lemma, in L.Rice]
Lam_correct [lemma, in L.Encodings]
Leb [definition, in L.Rice]
Leb_correct [lemma, in L.Rice]
lenc [definition, in L.Enumerable]
lenc_proc [lemma, in L.Enumerable]
list_cc [lemma, in L.Preliminaries]
list_exists_DM [lemma, in L.Preliminaries]
list_exists_dec [instance, in L.Preliminaries]
list_forall_dec [instance, in L.Preliminaries]
list_sigma_forall [lemma, in L.Preliminaries]
list_in_dec [instance, in L.Preliminaries]
list_eq_dec [instance, in L.Preliminaries]
list_cycle [lemma, in L.Preliminaries]
Lt [definition, in L.Rice]
Lt_correct [lemma, in L.Rice]
L_computable_computable [lemma, in L.Interpreter]
L_term_correct [lemma, in L.Enumerable]
L_term [definition, in L.Enumerable]


M

Map [definition, in L.Enumerable]
MapProduct [section, in L.Preliminaries]
MapProduct.f [variable, in L.Preliminaries]
MapProduct.X [variable, in L.Preliminaries]
MapProduct.Y [variable, in L.Preliminaries]
MapProduct.Z [variable, in L.Preliminaries]
map_pro_in [lemma, in L.Preliminaries]
map_pro [definition, in L.Preliminaries]
Map_pro_correct [lemma, in L.Enumerable]
Map_pro [definition, in L.Enumerable]
Map_correct [lemma, in L.Enumerable]
Markov [library]
Markov_Eva_to_Post [lemma, in L.Markov]
Markov_Sat_to_Eva [lemma, in L.Markov]
Markov_Post_to_Sat [lemma, in L.Markov]
Markov_Eva [definition, in L.Markov]
Markov_Sat [definition, in L.Markov]
Markov_Post [definition, in L.Markov]
mreducible [record, in L.Reduction]
mreducible_empty [lemma, in L.Reduction]
mreducible_full [lemma, in L.Reduction]
mreducible_recognisable [lemma, in L.Reduction]
mreducible_red [lemma, in L.Reduction]
mreducible_dec [lemma, in L.Reduction]
mreducible_comp_conv [lemma, in L.Reduction]
mreducible_comp [lemma, in L.Reduction]
mreducible_ext [lemma, in L.Reduction]
mreducible_preorder [instance, in L.Reduction]
mreducible_sane [lemma, in L.Reduction]
Mul [definition, in L.Extras]
Mul_correct [lemma, in L.Extras]


N

N [definition, in L.Encodings]
nat_le_dec [instance, in L.Preliminaries]
nat_eq_dec [instance, in L.Preliminaries]
Nil [definition, in L.Enumerable]
none [definition, in L.InterpreterResults]
none_equiv_some [lemma, in L.InterpreterResults]
none_correct [lemma, in L.InterpreterResults]
not_dec [instance, in L.Preliminaries]
nth [definition, in L.Preliminaries]
Nth [definition, in L.Enumerable]
nth_app_l [lemma, in L.Preliminaries]
nth_length [lemma, in L.Preliminaries]
Nth_correct [lemma, in L.Enumerable]
N_correct [lemma, in L.Encodings]


O

O [definition, in L.Por]
oenc [definition, in L.InterpreterResults]
oenc_inj [lemma, in L.InterpreterResults]
oenc_correct_some [lemma, in L.InterpreterResults]
oenc_lambda [lemma, in L.InterpreterResults]
oenc_cls [lemma, in L.InterpreterResults]
OfNat [definition, in L.Enumerable]
OfNat_correct [lemma, in L.Enumerable]
ok [definition, in L.Choose]
Omega [definition, in L.L]
omega [definition, in L.L]
onatenc [definition, in L.Enumerable]
or_dec [instance, in L.Preliminaries]
O_sound [lemma, in L.Por]
O_complete [lemma, in L.Por]
O_rec [lemma, in L.Por]


P

parametric_confluence [lemma, in L.L]
parametric_semi_confluence [lemma, in L.L]
pi [definition, in L.DecidableRecognisable]
Por [library]
pos [definition, in L.Preliminaries]
Positions [section, in L.Preliminaries]
Positions.d [variable, in L.Preliminaries]
Positions.X [variable, in L.Preliminaries]
Post [lemma, in L.Por]
pos_nth [lemma, in L.Preliminaries]
preceq_lub [lemma, in L.Reduction]
Pred [definition, in L.Extras]
Pred_correct [lemma, in L.Extras]
Preliminaries [library]
proc [definition, in L.L]
proc_lam [lemma, in L.Tactics]
proc_closed [lemma, in L.Tactics]


Q

Q [definition, in L.Encodings]
Q_correct [lemma, in L.Encodings]


R

R [definition, in L.Enumerable]
Re [definition, in L.Enumerable]
recinter [definition, in L.DecidableRecognisable]
recinter_correct [lemma, in L.DecidableRecognisable]
recognisable [definition, in L.DecidableRecognisable]
recognisable_intersection [lemma, in L.DecidableRecognisable]
recognisable_iff [lemma, in L.Reduction]
recognisable_union [lemma, in L.Por]
recognisable_eva [lemma, in L.InterpreterResults]
recognisable_range_total [lemma, in L.Enumerable]
recognisable_enumerable [lemma, in L.Enumerable]
rec_total_proc [lemma, in L.Rice]
rec_total_cls [lemma, in L.Rice]
rec_total [lemma, in L.Rice]
Reduction [lemma, in L.Rice]
Reduction [library]
rem [definition, in L.Preliminaries]
Removal [section, in L.Preliminaries]
Removal.X [variable, in L.Preliminaries]
rem_fst' [lemma, in L.Preliminaries]
rem_fst [lemma, in L.Preliminaries]
rem_equi [lemma, in L.Preliminaries]
rem_app [lemma, in L.Preliminaries]
rem_neq [lemma, in L.Preliminaries]
rem_in [lemma, in L.Preliminaries]
rem_cons' [lemma, in L.Preliminaries]
rem_cons [lemma, in L.Preliminaries]
rem_mono [lemma, in L.Preliminaries]
rem_incl [lemma, in L.Preliminaries]
rem_not_in [lemma, in L.Preliminaries]
Re_complete [lemma, in L.Enumerable]
Re_sound [lemma, in L.Enumerable]
Re_proc [lemma, in L.Enumerable]
re_exists [lemma, in L.Markov]
rho [definition, in L.L]
rho_correct [lemma, in L.L]
rho_closed [lemma, in L.L]
rho_lam [lemma, in L.L]
rho_correct [lemma, in L.Tactics]
Rice [lemma, in L.Rice]
Rice [library]
Rice_Theorem [lemma, in L.Rice]
Rice_pi [lemma, in L.Rice]
R_surjective [projection, in L.Enumerable]


S

satis [definition, in L.Choose]
Scott [lemma, in L.DecidableRecognisable]
SecondFixedPoint [lemma, in L.DecidableRecognisable]
semantic [definition, in L.Rice]
sim [definition, in L.Enumerable]
sim2 [definition, in L.Enumerable]
size [definition, in L.L]
size_induction [lemma, in L.Preliminaries]
some [definition, in L.InterpreterResults]
some_correct_r [lemma, in L.InterpreterResults]
some_correct [lemma, in L.InterpreterResults]
star [inductive, in L.L]
star_equiv_subrelation [instance, in L.L]
star_equiv [lemma, in L.L]
star_PreOrder [instance, in L.L]
star_evaluates [lemma, in L.L]
star_stepn [lemma, in L.L]
star_app [instance, in L.L]
star_trans [instance, in L.L]
star_step [constructor, in L.L]
star_refl [constructor, in L.L]
star_trans_r [lemma, in L.Tactics]
star_trans_l [lemma, in L.Tactics]
step [inductive, in L.L]
stepApp [constructor, in L.L]
stepAppL [constructor, in L.L]
stepAppR [constructor, in L.L]
stepn [inductive, in L.L]
stepn_plus [lemma, in L.L]
stepn_step [constructor, in L.L]
stepn_refl [constructor, in L.L]
stepplus [definition, in L.L]
stepplus_star_stepplus [lemma, in L.L]
stepplus_equiv_subrelation [instance, in L.L]
stepplus_star_subrelation [instance, in L.L]
stepplus_stepn [lemma, in L.L]
steps_evaluates [lemma, in L.L]
step_star_subrelation [instance, in L.L]
step_evaluates [lemma, in L.L]
subst [definition, in L.L]
Subst [definition, in L.InterpreterResults]
Subst_correct [lemma, in L.InterpreterResults]
Succ [definition, in L.Encodings]
Succ_correct [lemma, in L.Encodings]


T

T [definition, in L.L]
Tactics [library]
tcompl [definition, in L.DecidableRecognisable]
tenc [definition, in L.Encodings]
tenc_inj [lemma, in L.Encodings]
tenc_injective [lemma, in L.Encodings]
tenc_proc [lemma, in L.Encodings]
term [inductive, in L.L]
term_eq_dec [instance, in L.L]
term_eq_bool [definition, in L.Enumerable]
test [definition, in L.Choose]
tintersection [definition, in L.DecidableRecognisable]
totality [lemma, in L.InterpreterResults]
totality_hard [lemma, in L.InterpreterResults]
triangle [lemma, in L.L]
True_dec [instance, in L.Preliminaries]
tunion [definition, in L.DecidableRecognisable]
T_equiv_F [lemma, in L.Encodings]


U

U [definition, in L.InterpreterResults]
undecidable_russell [lemma, in L.DecidableRecognisable]
undup [definition, in L.Preliminaries]
Undup [section, in L.Preliminaries]
undup_idempotent [lemma, in L.Preliminaries]
undup_eq [lemma, in L.Preliminaries]
undup_equi [lemma, in L.Preliminaries]
undup_incl [lemma, in L.Preliminaries]
undup_fp_equi [lemma, in L.Preliminaries]
Undup.X [variable, in L.Preliminaries]
unenc [definition, in L.Interpreter]
unenc_correct2 [lemma, in L.Interpreter]
unenc_correct [lemma, in L.Interpreter]
uniform_confluence [lemma, in L.L]
union [definition, in L.DecidableRecognisable]
unique_normal_forms [lemma, in L.L]
unique_step_index [lemma, in L.L]
unrecognisable_russell [lemma, in L.Rice]
U_eva [lemma, in L.InterpreterResults]
U_sound [lemma, in L.InterpreterResults]
U_complete [lemma, in L.InterpreterResults]
U_rec [lemma, in L.InterpreterResults]


V

Var [definition, in L.Encodings]
var [constructor, in L.L]
Var_correct [lemma, in L.Encodings]


Y

Y [definition, in L.Tactics]
Y_spec [lemma, in L.Tactics]


Z

Zero [definition, in L.Encodings]


other

_ ⪯ _ [notation, in L.Reduction]
_ ≡ _ [notation, in L.L]
_ ≻^+ _ [notation, in L.L]
_ â–·^ _ _ [notation, in L.L]
_ ≻^ _ _ [notation, in L.L]
_ ≻* _ [notation, in L.L]
_ ≻ _ [notation, in L.L]
_ â–· _ [notation, in L.L]
_ === _ [notation, in L.Preliminaries]
_ <<= _ [notation, in L.Preliminaries]
_ el _ [notation, in L.Preliminaries]
_ ≈ _ [notation, in L.Rice]
eq_dec _ [notation, in L.Preliminaries]
! _ [notation, in L.L]
.\ _ , .. , _ ; _ [notation, in L.L]
| _ | [notation, in L.Preliminaries]
λ _ , .. , _ ; _ [notation, in L.L]


Notation Index

other

_ ⪯ _ [in L.Reduction]
_ ≡ _ [in L.L]
_ ≻^+ _ [in L.L]
_ â–·^ _ _ [in L.L]
_ ≻^ _ _ [in L.L]
_ ≻* _ [in L.L]
_ ≻ _ [in L.L]
_ â–· _ [in L.L]
_ === _ [in L.Preliminaries]
_ <<= _ [in L.Preliminaries]
_ el _ [in L.Preliminaries]
_ ≈ _ [in L.Rice]
eq_dec _ [in L.Preliminaries]
! _ [in L.L]
.\ _ , .. , _ ; _ [in L.L]
| _ | [in L.Preliminaries]
λ _ , .. , _ ; _ [in L.L]


Variable Index

C

Cardinality.X [in L.Preliminaries]


D

DupfreeLength.X [in L.Preliminaries]
Dupfree.X [in L.Preliminaries]


E

EnumCount.beta [in L.Enumerable]
EnumCount.Cumulative.cum [in L.Enumerable]
EnumCount.Cumulative.L [in L.Enumerable]
EnumCount.d [in L.Enumerable]
EnumCount.L [in L.Enumerable]
EnumCount.X [in L.Enumerable]
Equi.X [in L.Preliminaries]


F

FilterLemmas.p [in L.Preliminaries]
FilterLemmas.X [in L.Preliminaries]
fix_u.test_u [in L.Choose]
fix_u.proc_u [in L.Choose]
fix_u.u [in L.Choose]
Fix_X.enc_proc [in L.Enumerable]
Fix_X.enc [in L.Enumerable]
Fix_X.X [in L.Enumerable]
Fix_f.total_u [in L.Enumerable]
Fix_f.proc_u [in L.Enumerable]
Fix_f.u [in L.Enumerable]


I

Inclusion.X [in L.Preliminaries]


M

MapProduct.f [in L.Preliminaries]
MapProduct.X [in L.Preliminaries]
MapProduct.Y [in L.Preliminaries]
MapProduct.Z [in L.Preliminaries]


P

Positions.d [in L.Preliminaries]
Positions.X [in L.Preliminaries]


R

Removal.X [in L.Preliminaries]


U

Undup.X [in L.Preliminaries]


Library Index

C

Choose


D

DecidableRecognisable


E

Encodings
Enumerable
Extras


I

Interpreter
InterpreterResults


L

L


M

Markov


P

Por
Preliminaries


R

Reduction
Rice


T

Tactics


Lemma Index

A

Add_correct [in L.Encodings]
Append_correct [in L.Enumerable]
App_correct [in L.Encodings]
app_eva [in L.L]
app_closed [in L.L]


B

benc_proc [in L.Encodings]
beta [in L.Tactics]
bound_subst [in L.L]
bound_closed_k [in L.L]
bound_ge [in L.L]
Bound_correct [in L.Rice]


C

card_0 [in L.Preliminaries]
card_cons_rem [in L.Preliminaries]
card_cons [in L.Preliminaries]
card_ex [in L.Preliminaries]
card_or [in L.Preliminaries]
card_lt [in L.Preliminaries]
card_equi [in L.Preliminaries]
card_eq [in L.Preliminaries]
card_le [in L.Preliminaries]
church_rosser [in L.L]
closed_app [in L.L]
closed_subst [in L.L]
complete_induction [in L.Preliminaries]
computable_eva [in L.Interpreter]
confluence [in L.L]
Cons_correct [in L.Enumerable]
cum_L [in L.Enumerable]
cum_nth_eq [in L.Enumerable]
cum_nth [in L.Enumerable]
cum_ge' [in L.Enumerable]
cum_ge [in L.Enumerable]
cum_nth_ex [in L.Enumerable]
cum_length [in L.Enumerable]
C_sound [in L.Choose]
C_complete [in L.Choose]


D

DA [in L.Markov]
decidable_complement [in L.DecidableRecognisable]
decidable_union [in L.DecidableRecognisable]
decidable_intersection [in L.DecidableRecognisable]
decidable_spec [in L.DecidableRecognisable]
decidable_full [in L.Extras]
decidable_empty [in L.Extras]
decidable_finite [in L.Extras]
decidable_ext [in L.Extras]
decidable_dec [in L.Interpreter]
decidable_proc [in L.Rice]
decidable_lam [in L.Rice]
decidable_closed [in L.Rice]
decode_correct2 [in L.Interpreter]
decode_correct [in L.Interpreter]
dec_rec [in L.DecidableRecognisable]
dec_recognisable [in L.DecidableRecognisable]
dec_pdec [in L.Interpreter]
dec_prop_iff [in L.Preliminaries]
dec_DM_impl [in L.Preliminaries]
dec_DM_and [in L.Preliminaries]
dec_DN [in L.Preliminaries]
dec_total [in L.Rice]
dupfree_equi [in L.Preliminaries]
dupfree_ex [in L.Preliminaries]
dupfree_lt [in L.Preliminaries]
dupfree_eq [in L.Preliminaries]
dupfree_le [in L.Preliminaries]
dupfree_reorder [in L.Preliminaries]
dupfree_undup [in L.Preliminaries]
dupfree_dec [in L.Preliminaries]
dupfree_filter [in L.Preliminaries]
dupfree_map [in L.Preliminaries]
dupfree_inv [in L.Preliminaries]
D_pi [in L.Rice]


E

el_pos [in L.Preliminaries]
enc_inj [in L.Encodings]
enc_injective [in L.Encodings]
enc_proc [in L.Encodings]
enumerable_all [in L.Enumerable]
enumerable_recognisable [in L.Enumerable]
enum_term [in L.Enumerable]
enum_count [in L.Enumerable]
EqN_correct [in L.InterpreterResults]
equiv_spec_decidable [in L.DecidableRecognisable]
equiv_eva [in L.L]
equiv_evaluates [in L.L]
equiv_star_lam [in L.L]
equiv_trans_r [in L.Tactics]
equiv_trans_l [in L.Tactics]
equiv_R_trans [in L.Tactics]
equiv_eval [in L.Interpreter]
equiv_semantic [in L.Rice]
equi_rotate [in L.Preliminaries]
equi_shift [in L.Preliminaries]
equi_swap [in L.Preliminaries]
equi_dup [in L.Preliminaries]
equi_push [in L.Preliminaries]
Eq_correct [in L.Enumerable]
Eq_correct' [in L.Enumerable]
evaluates_equiv [in L.L]
evaluates_star [in L.L]
evaluates_D [in L.L]
evaluates_closed [in L.L]
evaluates_bound [in L.L]
evaluates_abst [in L.L]
evaluates_eval [in L.Interpreter]
eval_lambda [in L.Interpreter]
eval_equiv [in L.Interpreter]
eval_evaluates [in L.Interpreter]
eval_step [in L.Interpreter]
eval_S [in L.Interpreter]
eva_dec [in L.DecidableRecognisable]
eva_red [in L.Reduction]
eva_D [in L.L]
eva_Omega [in L.L]
exh_L [in L.Enumerable]
E_complete [in L.InterpreterResults]
E_sound [in L.InterpreterResults]
E_S [in L.InterpreterResults]
E_correct [in L.InterpreterResults]
E_rec_app_Sn_3 [in L.InterpreterResults]
E_rec_app_Sn_2 [in L.InterpreterResults]
E_rec_app_Sn_1 [in L.InterpreterResults]


F

filter_fst' [in L.Preliminaries]
filter_app [in L.Preliminaries]
filter_fst [in L.Preliminaries]
filter_mono [in L.Preliminaries]
filter_incl [in L.Preliminaries]
FirstFixedPoint [in L.Extras]
F_correct [in L.L]
F_eva [in L.L]


H

H_inv [in L.Por]
H_test [in L.Por]
H_rec [in L.Por]
H_proc [in L.Por]
H_correct [in L.Choose]
H_0_n [in L.Choose]
H_n_Sn [in L.Choose]
H_ok [in L.Choose]
H_rec [in L.Choose]
H_proc [in L.InterpreterResults]
H_inv [in L.InterpreterResults]
H_test [in L.InterpreterResults]
H_test [in L.Enumerable]
H_proc [in L.Enumerable]
H_rec [in L.Enumerable]


I

incl_lrcons [in L.Preliminaries]
incl_rcons [in L.Preliminaries]
incl_lcons [in L.Preliminaries]
incl_shift [in L.Preliminaries]
incl_nil_eq [in L.Preliminaries]
incl_map [in L.Preliminaries]
incl_nil [in L.Preliminaries]
in_rem_iff [in L.Preliminaries]
in_filter_iff [in L.Preliminaries]
in_cons_neq [in L.Preliminaries]
in_sing [in L.Preliminaries]
I_neq_Omega [in L.L]


L

lambda_lam [in L.L]
Lambda_correct [in L.Rice]
Lam_correct [in L.Encodings]
Leb_correct [in L.Rice]
lenc_proc [in L.Enumerable]
list_cc [in L.Preliminaries]
list_exists_DM [in L.Preliminaries]
list_sigma_forall [in L.Preliminaries]
list_cycle [in L.Preliminaries]
Lt_correct [in L.Rice]
L_computable_computable [in L.Interpreter]
L_term_correct [in L.Enumerable]


M

map_pro_in [in L.Preliminaries]
Map_pro_correct [in L.Enumerable]
Map_correct [in L.Enumerable]
Markov_Eva_to_Post [in L.Markov]
Markov_Sat_to_Eva [in L.Markov]
Markov_Post_to_Sat [in L.Markov]
mreducible_empty [in L.Reduction]
mreducible_full [in L.Reduction]
mreducible_recognisable [in L.Reduction]
mreducible_red [in L.Reduction]
mreducible_dec [in L.Reduction]
mreducible_comp_conv [in L.Reduction]
mreducible_comp [in L.Reduction]
mreducible_ext [in L.Reduction]
mreducible_sane [in L.Reduction]
Mul_correct [in L.Extras]


N

none_equiv_some [in L.InterpreterResults]
none_correct [in L.InterpreterResults]
nth_app_l [in L.Preliminaries]
nth_length [in L.Preliminaries]
Nth_correct [in L.Enumerable]
N_correct [in L.Encodings]


O

oenc_inj [in L.InterpreterResults]
oenc_correct_some [in L.InterpreterResults]
oenc_lambda [in L.InterpreterResults]
oenc_cls [in L.InterpreterResults]
OfNat_correct [in L.Enumerable]
O_sound [in L.Por]
O_complete [in L.Por]
O_rec [in L.Por]


P

parametric_confluence [in L.L]
parametric_semi_confluence [in L.L]
Post [in L.Por]
pos_nth [in L.Preliminaries]
preceq_lub [in L.Reduction]
Pred_correct [in L.Extras]
proc_lam [in L.Tactics]
proc_closed [in L.Tactics]


Q

Q_correct [in L.Encodings]


R

recinter_correct [in L.DecidableRecognisable]
recognisable_intersection [in L.DecidableRecognisable]
recognisable_iff [in L.Reduction]
recognisable_union [in L.Por]
recognisable_eva [in L.InterpreterResults]
recognisable_range_total [in L.Enumerable]
recognisable_enumerable [in L.Enumerable]
rec_total_proc [in L.Rice]
rec_total_cls [in L.Rice]
rec_total [in L.Rice]
Reduction [in L.Rice]
rem_fst' [in L.Preliminaries]
rem_fst [in L.Preliminaries]
rem_equi [in L.Preliminaries]
rem_app [in L.Preliminaries]
rem_neq [in L.Preliminaries]
rem_in [in L.Preliminaries]
rem_cons' [in L.Preliminaries]
rem_cons [in L.Preliminaries]
rem_mono [in L.Preliminaries]
rem_incl [in L.Preliminaries]
rem_not_in [in L.Preliminaries]
Re_complete [in L.Enumerable]
Re_sound [in L.Enumerable]
Re_proc [in L.Enumerable]
re_exists [in L.Markov]
rho_correct [in L.L]
rho_closed [in L.L]
rho_lam [in L.L]
rho_correct [in L.Tactics]
Rice [in L.Rice]
Rice_Theorem [in L.Rice]
Rice_pi [in L.Rice]


S

Scott [in L.DecidableRecognisable]
SecondFixedPoint [in L.DecidableRecognisable]
size_induction [in L.Preliminaries]
some_correct_r [in L.InterpreterResults]
some_correct [in L.InterpreterResults]
star_equiv [in L.L]
star_evaluates [in L.L]
star_stepn [in L.L]
star_trans_r [in L.Tactics]
star_trans_l [in L.Tactics]
stepn_plus [in L.L]
stepplus_star_stepplus [in L.L]
stepplus_stepn [in L.L]
steps_evaluates [in L.L]
step_evaluates [in L.L]
Subst_correct [in L.InterpreterResults]
Succ_correct [in L.Encodings]


T

tenc_inj [in L.Encodings]
tenc_injective [in L.Encodings]
tenc_proc [in L.Encodings]
totality [in L.InterpreterResults]
totality_hard [in L.InterpreterResults]
triangle [in L.L]
T_equiv_F [in L.Encodings]


U

undecidable_russell [in L.DecidableRecognisable]
undup_idempotent [in L.Preliminaries]
undup_eq [in L.Preliminaries]
undup_equi [in L.Preliminaries]
undup_incl [in L.Preliminaries]
undup_fp_equi [in L.Preliminaries]
unenc_correct2 [in L.Interpreter]
unenc_correct [in L.Interpreter]
uniform_confluence [in L.L]
unique_normal_forms [in L.L]
unique_step_index [in L.L]
unrecognisable_russell [in L.Rice]
U_eva [in L.InterpreterResults]
U_sound [in L.InterpreterResults]
U_complete [in L.InterpreterResults]
U_rec [in L.InterpreterResults]


V

Var_correct [in L.Encodings]


Y

Y_spec [in L.Tactics]


Constructor Index

A

app [in L.L]


B

bapp [in L.L]
blambda [in L.L]
bter [in L.L]
bvar [in L.L]


C

Countable [in L.Enumerable]


D

dupfreeC [in L.Preliminaries]
dupfreeN [in L.Preliminaries]


E

eqRef [in L.L]
eqStep [in L.L]
eqSym [in L.L]
eqTrans [in L.L]
evaluates_app [in L.L]
evaluates_lam [in L.L]


L

lambda [in L.L]


S

star_step [in L.L]
star_refl [in L.L]
stepApp [in L.L]
stepAppL [in L.L]
stepAppR [in L.L]
stepn_step [in L.L]
stepn_refl [in L.L]


V

var [in L.L]


Projection Index

F

f [in L.Reduction]
f_comp [in L.Reduction]
f_red [in L.Reduction]


R

R_surjective [in L.Enumerable]


Inductive Index

B

bterm [in L.L]


D

dupfree [in L.Preliminaries]


E

equiv [in L.L]
evaluates [in L.L]


S

star [in L.L]
step [in L.L]
stepn [in L.L]


T

term [in L.L]


Instance Index

A

and_dec [in L.Preliminaries]
app_equiv [in L.L]
app_equi_proper [in L.Preliminaries]


B

bool_eq_dec [in L.Preliminaries]


C

card_equi_proper [in L.Preliminaries]
cons_equi_proper [in L.Preliminaries]


E

equiv_Equivalence [in L.L]
equi_Equivalence [in L.Preliminaries]
eq_dec_string [in L.L]
evaluatesin_equiv_subrelation [in L.L]
evaluates_equiv_subrelation [in L.L]
evaluates_proper [in L.L]
eva_proper [in L.L]


F

False_dec [in L.Preliminaries]


I

iff_dec [in L.Preliminaries]
impl_dec [in L.Preliminaries]
incl_preorder [in L.Preliminaries]
incl_equi_proper [in L.Preliminaries]
in_equi_proper [in L.Preliminaries]


L

list_exists_dec [in L.Preliminaries]
list_forall_dec [in L.Preliminaries]
list_in_dec [in L.Preliminaries]
list_eq_dec [in L.Preliminaries]


M

mreducible_preorder [in L.Reduction]


N

nat_le_dec [in L.Preliminaries]
nat_eq_dec [in L.Preliminaries]
not_dec [in L.Preliminaries]


O

or_dec [in L.Preliminaries]


S

star_equiv_subrelation [in L.L]
star_PreOrder [in L.L]
star_app [in L.L]
star_trans [in L.L]
stepplus_equiv_subrelation [in L.L]
stepplus_star_subrelation [in L.L]
step_star_subrelation [in L.L]


T

term_eq_dec [in L.L]
True_dec [in L.Preliminaries]


Section Index

C

Cardinality [in L.Preliminaries]


D

Dupfree [in L.Preliminaries]
DupfreeLength [in L.Preliminaries]


E

EnumCount [in L.Enumerable]
EnumCount.Cumulative [in L.Enumerable]
Equi [in L.Preliminaries]


F

FilterLemmas [in L.Preliminaries]
fix_u [in L.Choose]
Fix_X [in L.Enumerable]
Fix_f [in L.Enumerable]


I

Inclusion [in L.Preliminaries]


M

MapProduct [in L.Preliminaries]


P

Positions [in L.Preliminaries]


R

Removal [in L.Preliminaries]


U

Undup [in L.Preliminaries]


Definition Index

A

Add [in L.Encodings]
App [in L.Encodings]
Append [in L.Enumerable]


B

benc [in L.Encodings]
beta [in L.Enumerable]
bound [in L.L]
Bound [in L.Rice]


C

C [in L.L]
C [in L.Choose]
card [in L.Preliminaries]
cChoice [in L.Interpreter]
cLam [in L.InterpreterResults]
closed [in L.L]
Closed [in L.Rice]
closed_under_proc [in L.Rice]
complement [in L.DecidableRecognisable]
computable_fun [in L.Reduction]
computable_gen [in L.Reduction]
Cons [in L.Enumerable]
convert [in L.L]
convert' [in L.L]
cumulative [in L.Enumerable]


D

D [in L.L]
dec [in L.Preliminaries]
decidable [in L.DecidableRecognisable]
decides [in L.DecidableRecognisable]
decision [in L.Preliminaries]
decode [in L.Interpreter]


E

E [in L.InterpreterResults]
enc [in L.Encodings]
enum [in L.Enumerable]
enumerable [in L.Enumerable]
Eq [in L.Enumerable]
EqN [in L.InterpreterResults]
equi [in L.Preliminaries]
eva [in L.L]
eval [in L.Interpreter]
evaluatesin [in L.L]


F

F [in L.L]
filter [in L.Preliminaries]
finite [in L.Extras]


H

H [in L.Por]
H [in L.Choose]
H [in L.InterpreterResults]


I

I [in L.L]
inclp [in L.Preliminaries]
Inj [in L.Enumerable]
intersection [in L.DecidableRecognisable]


L

L [in L.Enumerable]
Lam [in L.Encodings]
lam [in L.L]
Lambda [in L.Rice]
Leb [in L.Rice]
lenc [in L.Enumerable]
Lt [in L.Rice]
L_term [in L.Enumerable]


M

Map [in L.Enumerable]
map_pro [in L.Preliminaries]
Map_pro [in L.Enumerable]
Markov_Eva [in L.Markov]
Markov_Sat [in L.Markov]
Markov_Post [in L.Markov]
Mul [in L.Extras]


N

N [in L.Encodings]
Nil [in L.Enumerable]
none [in L.InterpreterResults]
nth [in L.Preliminaries]
Nth [in L.Enumerable]


O

O [in L.Por]
oenc [in L.InterpreterResults]
OfNat [in L.Enumerable]
ok [in L.Choose]
Omega [in L.L]
omega [in L.L]
onatenc [in L.Enumerable]


P

pi [in L.DecidableRecognisable]
pos [in L.Preliminaries]
Pred [in L.Extras]
proc [in L.L]


Q

Q [in L.Encodings]


R

R [in L.Enumerable]
Re [in L.Enumerable]
recinter [in L.DecidableRecognisable]
recognisable [in L.DecidableRecognisable]
rem [in L.Preliminaries]
rho [in L.L]


S

satis [in L.Choose]
semantic [in L.Rice]
sim [in L.Enumerable]
sim2 [in L.Enumerable]
size [in L.L]
some [in L.InterpreterResults]
stepplus [in L.L]
subst [in L.L]
Subst [in L.InterpreterResults]
Succ [in L.Encodings]


T

T [in L.L]
tcompl [in L.DecidableRecognisable]
tenc [in L.Encodings]
term_eq_bool [in L.Enumerable]
test [in L.Choose]
tintersection [in L.DecidableRecognisable]
tunion [in L.DecidableRecognisable]


U

U [in L.InterpreterResults]
undup [in L.Preliminaries]
unenc [in L.Interpreter]
union [in L.DecidableRecognisable]


V

Var [in L.Encodings]


Y

Y [in L.Tactics]


Z

Zero [in L.Encodings]


Record Index

C

countable [in L.Enumerable]


M

mreducible [in L.Reduction]


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 (541 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 (17 entries)
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 (30 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 (14 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 (281 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 (23 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 (4 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 (8 entries)
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 (37 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 (15 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 (110 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 (2 entries)