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 (504 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 (18 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 (18 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 (13 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 (273 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 (22 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)
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 (12 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 (36 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 (104 entries)

Global Index

A

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


B

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


C

C [definition, in Choose]
C [definition, in L]
card [definition, in Preliminaries]
Cardinality [section, in Preliminaries]
Cardinality.X [variable, in Preliminaries]
card_equi_proper [instance, in Preliminaries]
card_0 [lemma, in Preliminaries]
card_cons_rem [lemma, in Preliminaries]
card_cons [lemma, in Preliminaries]
card_ex [lemma, in Preliminaries]
card_or [lemma, in Preliminaries]
card_lt [lemma, in Preliminaries]
card_equi [lemma, in Preliminaries]
card_eq [lemma, in Preliminaries]
card_le [lemma, in Preliminaries]
cChoice [definition, in Interpreter]
Choose [library]
church_rosser [lemma, in L]
cLam [definition, in InterpreterResults]
closed [definition, in L]
Closed [definition, in Rice]
closed_app [lemma, in L]
closed_subst [lemma, in L]
closed_under_proc [definition, in Rice]
complement [definition, in DecidableRecognisable]
complete_induction [lemma, in Preliminaries]
computable_eva [lemma, in Interpreter]
confluence [lemma, in L]
Cons [definition, in Enumerable]
cons_equi_proper [instance, in Preliminaries]
Cons_correct [lemma, in Enumerable]
convert [definition, in L]
convert' [definition, in L]
C_sound [lemma, in Choose]
C_complete [lemma, in Choose]


D

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


E

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


F

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


H

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


I

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


L

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


M

Map [definition, in Enumerable]
Map_correct [lemma, in Enumerable]
Markov [library]
Markov_Eva_to_Post [lemma, in Markov]
Markov_Sat_to_Eva [lemma, in Markov]
Markov_Post_to_Sat [lemma, in Markov]
Markov_Eva [definition, in Markov]
Markov_Sat [definition, in Markov]
Markov_Post [definition, in Markov]
Mul [definition, in Extras]
Mul_correct [lemma, in Extras]


N

N [definition, in Encodings]
nat_le_dec [instance, in Preliminaries]
nat_eq_dec [instance, in Preliminaries]
Nil [definition, in Enumerable]
none [definition, in InterpreterResults]
none_equiv_some [lemma, in InterpreterResults]
none_correct [lemma, in InterpreterResults]
not_dec [instance, in Preliminaries]
Nth [definition, in Enumerable]
nth_error_none [lemma, in Preliminaries]
Nth_correct [lemma, in Enumerable]
N_correct [lemma, in Encodings]


O

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


P

parametric_confluence [lemma, in L]
parametric_semi_confluence [lemma, in L]
pi [definition, in DecidableRecognisable]
Por [library]
pos [definition, in Preliminaries]
pos [section, in Preliminaries]
Post [lemma, in Por]
pos_elAt [lemma, in Preliminaries]
_ .[ _ ] [notation, in Preliminaries]
Pred [definition, in Extras]
Pred_correct [lemma, in Extras]
Preliminaries [library]
proc [definition, in L]
proc_lam [lemma, in Tactics]
proc_closed [lemma, in Tactics]


Q

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


R

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


S

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


T

T [definition, in L]
Tactics [library]
tcompl [definition, in DecidableRecognisable]
tenc [definition, in Encodings]
tenc_inj [lemma, in Encodings]
tenc_injective [lemma, in Encodings]
tenc_proc [lemma, in Encodings]
term [inductive, in L]
term_eq_bool [definition, in Enumerable]
term_eq_dec [instance, in L]
test [definition, in Choose]
tintersection [definition, in DecidableRecognisable]
tlenc [definition, in Enumerable]
tlenc_proc [lemma, in Enumerable]
totality [lemma, in InterpreterResults]
totality_hard [lemma, in InterpreterResults]
triangle [lemma, in L]
True_dec [instance, in Preliminaries]
TT [definition, in Enumerable]
TT_correct [lemma, in Enumerable]
TT_S [lemma, in Enumerable]
tunion [definition, in DecidableRecognisable]
T_longenough [lemma, in Enumerable]
T_exhaustive [lemma, in Enumerable]
T_lambda [lemma, in Enumerable]
T_el_ge [lemma, in Enumerable]
T_app [lemma, in Enumerable]
T_var [lemma, in Enumerable]
T_ge [lemma, in Enumerable]
T_S [lemma, in Enumerable]
T_enum [definition, in Enumerable]
T_equiv_F [lemma, in Encodings]


U

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


V

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


Z

Zero [definition, in Encodings]


other

_ === _ [notation, in Preliminaries]
_ <<= _ [notation, in Preliminaries]
_ el _ [notation, in Preliminaries]
_ .[ _ ] [notation, in Enumerable]
_ ≡ _ [notation, in L]
_ ≻^+ _ [notation, in L]
_ ▷^ _ _ [notation, in L]
_ ≻^ _ _ [notation, in L]
_ ≻* _ [notation, in L]
_ ≻ _ [notation, in L]
_ ▷ _ [notation, in L]
_ ≈ _ [notation, in Rice]
eq_dec _ [notation, in Preliminaries]
! _ [notation, in L]
.\ _ , .. , _ ; _ [notation, in L]
| _ | [notation, in Preliminaries]
λ _ , .. , _ ; _ [notation, in L]



Notation Index

P

_ .[ _ ] [in Preliminaries]


other

_ === _ [in Preliminaries]
_ <<= _ [in Preliminaries]
_ el _ [in Preliminaries]
_ .[ _ ] [in Enumerable]
_ ≡ _ [in L]
_ ≻^+ _ [in L]
_ ▷^ _ _ [in L]
_ ≻^ _ _ [in L]
_ ≻* _ [in L]
_ ≻ _ [in L]
_ ▷ _ [in L]
_ ≈ _ [in Rice]
eq_dec _ [in Preliminaries]
! _ [in L]
.\ _ , .. , _ ; _ [in L]
| _ | [in Preliminaries]
λ _ , .. , _ ; _ [in L]



Variable Index

C

Cardinality.X [in Preliminaries]


D

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


E

Equi.X [in Preliminaries]


F

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


I

Inclusion.X [in Preliminaries]


R

Removal.X [in Preliminaries]


U

Undup.X [in Preliminaries]



Library Index

C

Choose


D

DecidableRecognisable


E

Encodings
Enumerable
Extras


I

Interpreter
InterpreterResults


L

L


M

Markov


P

Por
Preliminaries


R

Rice


T

Tactics



Lemma Index

A

Add_correct [in Encodings]
AppCross_correct [in Enumerable]
AppCross_cls [in Enumerable]
appCross_correct [in Enumerable]
Append_correct [in Enumerable]
App_correct [in Encodings]
app_eva [in L]
app_closed [in L]


B

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


C

card_0 [in Preliminaries]
card_cons_rem [in Preliminaries]
card_cons [in Preliminaries]
card_ex [in Preliminaries]
card_or [in Preliminaries]
card_lt [in Preliminaries]
card_equi [in Preliminaries]
card_eq [in Preliminaries]
card_le [in Preliminaries]
church_rosser [in L]
closed_app [in L]
closed_subst [in L]
complete_induction [in Preliminaries]
computable_eva [in Interpreter]
confluence [in L]
Cons_correct [in Enumerable]
C_sound [in Choose]
C_complete [in Choose]


D

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


E

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


F

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


H

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


I

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


L

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


M

Map_correct [in Enumerable]
Markov_Eva_to_Post [in Markov]
Markov_Sat_to_Eva [in Markov]
Markov_Post_to_Sat [in Markov]
Mul_correct [in Extras]


N

none_equiv_some [in InterpreterResults]
none_correct [in InterpreterResults]
nth_error_none [in Preliminaries]
Nth_correct [in Enumerable]
N_correct [in Encodings]


O

oenc_inj [in InterpreterResults]
oenc_correct_some [in InterpreterResults]
oenc_lambda [in InterpreterResults]
oenc_cls [in InterpreterResults]
O_sound [in Por]
O_complete [in Por]
O_rec [in Por]


P

parametric_confluence [in L]
parametric_semi_confluence [in L]
Post [in Por]
pos_elAt [in Preliminaries]
Pred_correct [in Extras]
proc_lam [in Tactics]
proc_closed [in Tactics]


Q

Q_correct [in Encodings]


R

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


S

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


T

tenc_inj [in Encodings]
tenc_injective [in Encodings]
tenc_proc [in Encodings]
tlenc_proc [in Enumerable]
totality [in InterpreterResults]
totality_hard [in InterpreterResults]
triangle [in L]
TT_correct [in Enumerable]
TT_S [in Enumerable]
T_longenough [in Enumerable]
T_exhaustive [in Enumerable]
T_lambda [in Enumerable]
T_el_ge [in Enumerable]
T_app [in Enumerable]
T_var [in Enumerable]
T_ge [in Enumerable]
T_S [in Enumerable]
T_equiv_F [in Encodings]


U

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


V

Var_correct [in Encodings]



Constructor Index

A

app [in L]


B

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


D

dupfreeC [in Preliminaries]
dupfreeN [in Preliminaries]


E

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


L

lambda [in L]


S

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


V

var [in L]



Inductive Index

B

bterm [in L]


D

dupfree [in Preliminaries]


E

equiv [in L]
evaluates [in L]


S

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


T

term [in L]



Section Index

C

Cardinality [in Preliminaries]


D

Dupfree [in Preliminaries]
DupfreeLength [in Preliminaries]


E

Equi [in Preliminaries]


F

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


I

Inclusion [in Preliminaries]


P

pos [in Preliminaries]


R

Removal [in Preliminaries]


U

Undup [in Preliminaries]



Instance Index

A

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


B

bool_eq_dec [in Preliminaries]


C

card_equi_proper [in Preliminaries]
cons_equi_proper [in Preliminaries]


E

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


F

False_dec [in Preliminaries]


I

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


L

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


N

nat_le_dec [in Preliminaries]
nat_eq_dec [in Preliminaries]
not_dec [in Preliminaries]


O

or_dec [in Preliminaries]


S

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


T

term_eq_dec [in L]
True_dec [in Preliminaries]



Definition Index

A

Add [in Encodings]
App [in Encodings]
AppCross [in Enumerable]
appCross [in Enumerable]
Append [in Enumerable]


B

benc [in Encodings]
bound [in L]
Bound [in Rice]


C

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


D

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


E

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


F

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


H

H [in Choose]
H [in Por]
H [in InterpreterResults]


I

I [in L]
inclp [in Preliminaries]
intersection [in DecidableRecognisable]


L

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


M

Map [in Enumerable]
Markov_Eva [in Markov]
Markov_Sat [in Markov]
Markov_Post [in Markov]
Mul [in Extras]


N

N [in Encodings]
Nil [in Enumerable]
none [in InterpreterResults]
Nth [in Enumerable]


O

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


P

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


Q

Q [in Encodings]


R

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


S

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


T

T [in L]
tcompl [in DecidableRecognisable]
tenc [in Encodings]
term_eq_bool [in Enumerable]
test [in Choose]
tintersection [in DecidableRecognisable]
tlenc [in Enumerable]
TT [in Enumerable]
tunion [in DecidableRecognisable]
T_enum [in Enumerable]


U

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


V

Var [in Encodings]


Z

Zero [in Encodings]



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 (504 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 (18 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 (18 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 (13 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 (273 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 (22 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)
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 (12 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 (36 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 (104 entries)