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 (574 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 (30 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 (26 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 (10 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 (293 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 (56 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 (17 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 (50 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 (17 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 (74 entries)

Global Index

A

abs [definition, in SKvAbstraction]
absInj [lemma, in SKvAbstraction]
abs_lambda_equiv [lemma, in SKvAbstraction]
abs_nonLambda_continue [lemma, in SKvAbstraction]
abs_step_prefix [lemma, in SKvAbstraction]
abs_inv_size_val [lemma, in SKvAbstraction]
abs_inv_correct [lemma, in SKvAbstraction]
abs_inv [definition, in SKvAbstraction]
abs_no_Ss [lemma, in SKvAbstraction]
abs_no_S [lemma, in SKvAbstraction]
abs_no_K [lemma, in SKvAbstraction]
abs_no_var [lemma, in SKvAbstraction]
abs_sound [lemma, in SKvAbstraction]
abs_sound_pow [lemma, in SKvAbstraction]
abs_varClosed_iff [lemma, in SKvAbstraction]
abs_closed_eq [lemma, in SKvAbstraction]
abs_maxValue [lemma, in SKvAbstraction]
admissible [inductive, in LC]
admissible_step_proper [instance, in LC]
admissible_star [lemma, in LC]
admissible_step [lemma, in LC]
and_dec [instance, in Base]
app [constructor, in SKv]
app [constructor, in L]
app [constructor, in LC]
app_closed [lemma, in L]
app_equi_proper [instance, in Base]
ARS [library]


B

bapp [constructor, in L]
Base [library]
blam [constructor, in L]
bool_eq_dec [instance, in Base]
bter [constructor, in L]
bterm [inductive, in L]
bvar [constructor, in L]


C

C [definition, in SKvAbstraction]
card [definition, in Base]
Cardinality [section, in Base]
Cardinality.X [variable, in Base]
card_equi_proper [instance, in Base]
card_0 [lemma, in Base]
card_cons_rem [lemma, in Base]
card_cons [lemma, in Base]
card_ex [lemma, in Base]
card_or [lemma, in Base]
card_lt [lemma, in Base]
card_equi [lemma, in Base]
card_eq [lemma, in Base]
card_le [lemma, in Base]
church_rosser [lemma, in L]
church_rosser [definition, in ARS]
CInj [lemma, in SKvAbstraction]
clapp [constructor, in SKv]
clK [constructor, in SKv]
clos [constructor, in LC]
closed [inductive, in SKv]
closed [definition, in L]
closed_varClosed [lemma, in SKv]
closed_app [lemma, in SKv]
closed_dec [instance, in SKv]
closed_star [lemma, in L]
closed_step [lemma, in L]
closed_subst [lemma, in L]
closed_dec [instance, in L]
closed_app [lemma, in L]
closed_dclosed [lemma, in L]
closed_dcl [lemma, in L]
closed_k_dclosed [lemma, in L]
closed_r [lemma, in L]
closed_l [lemma, in L]
closed_dcl_x [lemma, in SKvTactics]
clS [constructor, in SKv]
comb_proc_red [lemma, in L]
complete_induction [lemma, in Base]
comp_eqb_spec [definition, in LC]
comp_eqb [definition, in LC]
confluence [lemma, in L]
confluent [definition, in ARS]
confluent_CR [lemma, in ARS]
cons_equi_proper [instance, in Base]
converges [definition, in L]
converges_proper [instance, in L]
converges_equiv [lemma, in L]
convert [definition, in L]
convert' [definition, in L]
C_eval_iff [lemma, in SKvAbstraction]
C_equiv_iff [lemma, in SKvAbstraction]
C_complete_equiv [lemma, in SKvAbstraction]
C_complete [lemma, in SKvAbstraction]
C_eval_complete [lemma, in SKvAbstraction]
C_eval_pullback [lemma, in SKvAbstraction]
C_star_prefix [lemma, in SKvAbstraction]
C_step_prefix [lemma, in SKvAbstraction]
C_step_app [lemma, in SKvAbstraction]
C_inv_correct [lemma, in SKvAbstraction]
C_eval_sound [lemma, in SKvAbstraction]
C_sound_equiv [lemma, in SKvAbstraction]
C_value_iff [lemma, in SKvAbstraction]
C_sound [lemma, in SKvAbstraction]
C_sound_pow [lemma, in SKvAbstraction]
C_near_value [lemma, in SKvAbstraction]
C_lam_value [lemma, in SKvAbstraction]
C_closed_if [lemma, in SKvAbstraction]
C_closed [lemma, in SKvAbstraction]
C_closed_varClosed [lemma, in SKvAbstraction]
C_dclosed_iff [lemma, in SKvAbstraction]


D

dclApp [constructor, in L]
dcllam [constructor, in L]
dclosed [inductive, in L]
dclosedApp_iff [lemma, in L]
dclosedLam_iff [lemma, in L]
dclosedVar_iff [lemma, in L]
dclosed_dec [instance, in L]
dclosed_closed [lemma, in L]
dclosed_gt [lemma, in L]
dclosed_ge [lemma, in L]
dclosed_closed_k [lemma, in L]
dclvar [constructor, in L]
dec [definition, in Base]
decision [definition, in Base]
dec_prop_iff [lemma, in Base]
dec_DM_impl [lemma, in Base]
dec_DM_and [lemma, in Base]
dec_DN [lemma, in Base]
diamond [definition, in ARS]
diamond_to_confluent [lemma, in ARS]
diamond_to_semi_confluent [lemma, in ARS]
disjoint [definition, in Base]
disjoint_cons [lemma, in Base]
disjoint_forall [lemma, in Base]
Dupfree [section, in Base]
dupfree [inductive, in Base]
dupfreeC [constructor, in Base]
DupfreeLength [section, in Base]
DupfreeLength.X [variable, in Base]
dupfreeN [constructor, in Base]
dupfree_elAt [lemma, in Base]
dupfree_in_power [lemma, in Base]
dupfree_power [lemma, in Base]
dupfree_equi [lemma, in Base]
dupfree_ex [lemma, in Base]
dupfree_lt [lemma, in Base]
dupfree_eq [lemma, in Base]
dupfree_le [lemma, in Base]
dupfree_reorder [lemma, in Base]
dupfree_undup [lemma, in Base]
dupfree_dec [lemma, in Base]
dupfree_filter [lemma, in Base]
dupfree_map [lemma, in Base]
dupfree_app [lemma, in Base]
dupfree_inv [lemma, in Base]
Dupfree.X [variable, in Base]


E

ecl [inductive, in ARS]
eclC [constructor, in ARS]
eclR [constructor, in ARS]
eclS [constructor, in ARS]
ecl_equivalence [instance, in ARS]
ecl_sym [lemma, in ARS]
ecl_trans [lemma, in ARS]
elAt [definition, in Base]
elAt_el [lemma, in Base]
elAt_app [lemma, in Base]
el_elAt [lemma, in Base]
el_pos [lemma, in Base]
emptEnv [lemma, in LC]
emptEnv_admissible [lemma, in LC]
eqApp [lemma, in L]
eqAppL [lemma, in SKv]
eqAppR [lemma, in SKv]
eqRef [constructor, in L]
eqStarT [lemma, in L]
eqStep [constructor, in L]
eqSym [constructor, in L]
eqTrans [constructor, in L]
Equi [section, in Base]
equi [definition, in Base]
equiv [inductive, in L]
equiv_value_eq [lemma, in SKv]
equiv_value [lemma, in SKv]
equiv_app_proper [instance, in SKv]
equiv_app_proper [instance, in L]
equiv_lambda [lemma, in L]
equiv_ecl [lemma, in L]
equiv_Equivalence [instance, in L]
equi_rotate [lemma, in Base]
equi_shift [lemma, in Base]
equi_swap [lemma, in Base]
equi_dup [lemma, in Base]
equi_push [lemma, in Base]
equi_Equivalence [instance, in Base]
Equi.X [variable, in Base]
eq_dec_string [instance, in L]
Eta [lemma, in L]
eval [definition, in SKv]
eval [definition, in L]
eval [definition, in LC]
evalBeta [definition, in LC_eval]
evalLC [definition, in LC_eval]
eval_iff [lemma, in SKv]


F

False_dec [instance, in Base]
FCI [module, in Base]
FCI.C [definition, in Base]
FCI.closure [lemma, in Base]
FCI.F [definition, in Base]
FCI.FCI [section, in Base]
FCI.FCI.step [variable, in Base]
FCI.FCI.V [variable, in Base]
FCI.FCI.X [variable, in Base]
FCI.fp [lemma, in Base]
FCI.incl [lemma, in Base]
FCI.ind [lemma, in Base]
FCI.it_incl [lemma, in Base]
FCI.pick [lemma, in Base]
filter [definition, in Base]
FilterComm [section, in Base]
FilterComm.p [variable, in Base]
FilterComm.q [variable, in Base]
FilterComm.X [variable, in Base]
FilterLemmas [section, in Base]
FilterLemmas_pq.q [variable, in Base]
FilterLemmas_pq.p [variable, in Base]
FilterLemmas_pq.X [variable, in Base]
FilterLemmas_pq [section, in Base]
FilterLemmas.p [variable, in Base]
FilterLemmas.X [variable, in Base]
filter_comm [lemma, in Base]
filter_and [lemma, in Base]
filter_pq_eq [lemma, in Base]
filter_pq_mono [lemma, in Base]
filter_fst' [lemma, in Base]
filter_app [lemma, in Base]
filter_fst [lemma, in Base]
filter_mono [lemma, in Base]
filter_incl [lemma, in Base]
FixX [section, in UnifConfl]
FixX [section, in ARS]
FixX.R [variable, in UnifConfl]
FixX.UC [section, in UnifConfl]
FixX.UC.UC [variable, in UnifConfl]
FixX.X [variable, in UnifConfl]
FixX.X [variable, in ARS]
_ >^ _ [notation, in UnifConfl]
_ >> _ [notation, in UnifConfl]
flatten [definition, in SKvAbstraction]
flattenInj [lemma, in SKvAbstraction]
flattenInv_size [lemma, in SKvAbstraction]
flattenInv_correct [lemma, in SKvAbstraction]
flatten_inv [definition, in SKvAbstraction]
flatten_subst_commute [lemma, in SKvAbstraction]
flatten_subst_varClosed [lemma, in SKvAbstraction]
flatten_varClosed_iff [lemma, in SKvAbstraction]
flatten_closed_idem [lemma, in SKvAbstraction]
flatten_value [lemma, in SKvAbstraction]
FP [definition, in Base]
freeLvwVar_dec [instance, in SKv]
functional [definition, in ARS]


I

I [definition, in SKv]
I [definition, in L]
iff_dec [instance, in Base]
impl_dec [instance, in Base]
inclp [definition, in Base]
Inclusion [section, in Base]
Inclusion.X [variable, in Base]
incl_preorder [instance, in Base]
incl_equi_proper [instance, in Base]
incl_lrcons [lemma, in Base]
incl_rcons [lemma, in Base]
incl_lcons [lemma, in Base]
incl_shift [lemma, in Base]
incl_nil_eq [lemma, in Base]
incl_map [lemma, in Base]
incl_nil [lemma, in Base]
in_rem_iff [lemma, in Base]
in_filter_iff [lemma, in Base]
in_equi_proper [instance, in Base]
in_cons_neq [lemma, in Base]
in_sing [lemma, in Base]
irred [definition, in UnifConfl]
irred_appR [lemma, in SKv]
irred_appL [lemma, in SKv]
irred_iff [lemma, in L]
irred_pow [lemma, in UnifConfl]
it [definition, in Base]
Iteration [section, in Base]
Iteration.f [variable, in Base]
Iteration.X [variable, in Base]
it_fp [lemma, in Base]
it_ind [lemma, in Base]
I_closed [lemma, in SKv]
I_value [lemma, in SKv]


J

joinable [definition, in ARS]


K

K [constructor, in SKv]
K [definition, in L]


L

L [library]
lam [constructor, in L]
lambda [definition, in L]
lambda_dec [instance, in L]
lambda_lam [lemma, in L]
LC [library]
LC_UC [lemma, in LC]
LC_eq_dec [instance, in LC]
LC_eval [library]
LexSizeInduction [library]
lex_size_induction [definition, in LexSizeInduction]
lex_size_lt_wf [lemma, in LexSizeInduction]
lex_size_lt [definition, in LexSizeInduction]
list_cc [lemma, in Base]
list_exists_DM [lemma, in Base]
list_exists_dec [instance, in Base]
list_forall_dec [instance, in Base]
list_sigma_forall [lemma, in Base]
list_in_dec [instance, in Base]
list_eq_dec [instance, in Base]
list_cycle [lemma, in Base]
lSize [definition, in SKvAbstraction]
Lstep_complete_star [lemma, in LC]


M

maxValue [definition, in SKv]
maxValueSubst [lemma, in SKv]
maxValue_Value [lemma, in SKv]


N

nat_le_dec [instance, in Base]
nat_eq_dec [instance, in Base]
normal_value [lemma, in SKv]
not_dec [instance, in Base]
nth_error_none [lemma, in Base]


O

Omega [definition, in L]
omega [definition, in L]
or_dec [instance, in Base]


P

pos [definition, in Base]
pos [section, in Base]
pos_elAt [lemma, in Base]
pos.X [variable, in Base]
_ .[ _ ] [notation, in Base]
pow [definition, in ARS]
power [definition, in Base]
PowerRep [section, in Base]
PowerRep.X [variable, in Base]
power_extensional [lemma, in Base]
power_nil [lemma, in Base]
power_incl [lemma, in Base]
powSk [lemma, in L]
pow_decompose [lemma, in SKv]
pow_trans_lam [lemma, in L]
pow_trans_lam' [lemma, in L]
pow_star_subrelation [instance, in ARS]
pow_add [lemma, in ARS]
pow_star [lemma, in ARS]
pow_app [lemma, in LC]
pow_app_r [lemma, in LC]
pow_app_l [lemma, in LC]
proc [definition, in L]
proc_dec [lemma, in L]
proc_lambda [lemma, in SKvTactics]
proc_closed [lemma, in SKvTactics]
prod_eq_dec [instance, in Base]
pSubst [definition, in LC]
pSubst_closed [lemma, in LC]
pSubst_dclosed [lemma, in LC]
pSubst_cons [lemma, in LC]
pSubst_nil [lemma, in LC]


R

R [definition, in L]
r [definition, in L]
rcomp [definition, in ARS]
rcomp_1 [lemma, in ARS]
reflexive [definition, in ARS]
rem [definition, in Base]
Removal [section, in Base]
Removal.X [variable, in Base]
rem_fst' [lemma, in Base]
rem_fst [lemma, in Base]
rem_comm [lemma, in Base]
rem_equi [lemma, in Base]
rem_app' [lemma, in Base]
rem_app [lemma, in Base]
rem_neq [lemma, in Base]
rem_in [lemma, in Base]
rem_cons' [lemma, in Base]
rem_cons [lemma, in Base]
rem_mono [lemma, in Base]
rem_incl [lemma, in Base]
rem_not_in [lemma, in Base]
rep [definition, in Base]
rep_dupfree [lemma, in Base]
rep_idempotent [lemma, in Base]
rep_injective [lemma, in Base]
rep_eq [lemma, in Base]
rep_eq' [lemma, in Base]
rep_mono [lemma, in Base]
rep_equi [lemma, in Base]
rep_in [lemma, in Base]
rep_incl [lemma, in Base]
rep_power [lemma, in Base]
rho [definition, in L]
R_ecl_subrelation [instance, in ARS]
R_star_subrelation [instance, in ARS]


S

S [constructor, in SKv]
semi_confluent_confluent [lemma, in ARS]
semi_confluent [definition, in ARS]
simplified [definition, in LC]
simplified_real_step [lemma, in LC]
simplify [definition, in LC]
simplify_admissible [lemma, in LC]
simplify_simplified [lemma, in LC]
simplify_translate [lemma, in LC]
simplify_sound [lemma, in LC]
simplify' [definition, in LC]
simplify'_simplified [lemma, in LC]
simplify'_translate [lemma, in LC]
simplify'_translate_var' [lemma, in LC]
simplify'_sound [lemma, in LC]
simulation [lemma, in LC]
simulation' [lemma, in LC]
size [definition, in SKv]
size [definition, in L]
size_induction [lemma, in Base]
SKv [library]
SKvAbstraction [library]
SKvTactics [library]
SKv_eq_dec [instance, in SKv]
SK_church_rosser [lemma, in SKv]
SK_UC [lemma, in SKv]
star [inductive, in ARS]
starC [constructor, in ARS]
starR [constructor, in ARS]
starStepL [lemma, in SKv]
starStepR [lemma, in SKv]
star_closed [lemma, in SKv]
star_value [lemma, in SKv]
star_app_proper [instance, in SKv]
star_equiv_subrelation [instance, in L]
star_equiv [lemma, in L]
star_closed_proper [instance, in L]
star_step_app_proper [instance, in L]
star_trans_r [lemma, in L]
star_trans_l [lemma, in L]
star_ecl_subrelation [instance, in ARS]
star_PreOrder [instance, in ARS]
star_ecl [lemma, in ARS]
star_pow [lemma, in ARS]
star_trans [lemma, in ARS]
star_simpl_ind [lemma, in ARS]
star_step_app_proper [instance, in LC]
star_app_r [lemma, in LC]
star_app_l [lemma, in LC]
step [inductive, in SKv]
step [inductive, in L]
step [inductive, in LC]
stepApp [constructor, in L]
stepApp [constructor, in LC]
stepAppL [constructor, in SKv]
stepAppL [constructor, in L]
stepAppL [constructor, in LC]
stepAppR [constructor, in SKv]
stepAppR [constructor, in L]
stepAppR [constructor, in LC]
stepBeta [constructor, in LC]
stepK [constructor, in SKv]
stepS [constructor, in SKv]
stepVar [constructor, in LC]
step_closed [lemma, in SKv]
step_pow_app [lemma, in SKv]
step_pow_app_r [lemma, in SKv]
step_pow_app_l [lemma, in SKv]
step_equiv_subrelation [instance, in L]
step_star [lemma, in L]
step_value [lemma, in L]
step_pow_app [lemma, in L]
step_pow_app_r [lemma, in L]
step_pow_app_l [lemma, in L]
subst [definition, in SKv]
subst [definition, in L]
subst_free_iff [lemma, in SKv]
subst_C_commute [lemma, in SKvAbstraction]
subst_abs_commute [lemma, in SKvAbstraction]
symmetric [definition, in ARS]


T

term [inductive, in SKv]
term [inductive, in L]
term [inductive, in LC]
term_eq_dec_proc [definition, in L]
term_eq_dec [instance, in L]
term_ind_deep [definition, in LC]
term_rec_deep' [definition, in LC]
transitive [definition, in ARS]
translate [definition, in LC]
translate_complete [lemma, in LC]
translate_complete_param [lemma, in LC]
translate_lambda_iff [lemma, in LC]
translate_irstep_iff [lemma, in LC]
translate_simplified_complete [lemma, in LC]
translate_lam [lemma, in LC]
translate_sound [lemma, in LC]
translate_sound_step [lemma, in LC]
translate_map_closed [lemma, in LC]
translate_closed [lemma, in LC]
True_dec [instance, in Base]


U

UC_niehren_iff [lemma, in UnifConfl]
UC_niehren [definition, in UnifConfl]
UC_confluent [lemma, in UnifConfl]
UC_DC [lemma, in UnifConfl]
UD_UC [lemma, in UnifConfl]
undup [definition, in Base]
Undup [section, in Base]
undup_idempotent [lemma, in Base]
undup_eq [lemma, in Base]
undup_equi [lemma, in Base]
undup_incl [lemma, in Base]
undup_fp_equi [lemma, in Base]
Undup.X [variable, in Base]
UnifConfl [library]
uniformly_semi_confluent [lemma, in UnifConfl]
uniformly_confluent [definition, in UnifConfl]
uniform_confluence [lemma, in L]
uniform_diamond [definition, in UnifConfl]
unif_unique [lemma, in UnifConfl]
unif_pow_normal [lemma, in UnifConfl]
unif_pow_normal_part [lemma, in UnifConfl]
unique_normal_forms [lemma, in L]


V

validLCApp [constructor, in LC]
validLCclos [constructor, in LC]
valK [constructor, in SKv]
valK1 [constructor, in SKv]
valS [constructor, in SKv]
valS1 [constructor, in SKv]
value [inductive, in SKv]
value [inductive, in LC]
valueLam [constructor, in LC]
valueSubst [lemma, in SKv]
valueSubst_iff [lemma, in SKv]
value_step_unique [lemma, in SKv]
value_irred [lemma, in SKv]
value_dec [instance, in SKv]
value_iff_irred [lemma, in LC]
value_irred [lemma, in LC]
value_dec [instance, in LC]
valVar [constructor, in SKv]
valX2 [constructor, in SKv]
var [constructor, in SKv]
var [constructor, in L]
var [constructor, in LC]
varClosed [inductive, in SKv]
varClosedApp [constructor, in SKv]
varClosedApp_iff [lemma, in SKv]
varClosedK [constructor, in SKv]
varClosedS [constructor, in SKv]
varClosedVar [constructor, in SKv]
varClosedVar_iff [lemma, in SKv]
varClosed_closed [lemma, in SKv]
var_not_closed [lemma, in L]


other

_ >[]^ _ (LC_scope) [notation, in LC]
_ >[]* _ (LC_scope) [notation, in LC]
_ >[]> _ (LC_scope) [notation, in LC]
# _ (LC_scope) [notation, in LC]
# _ (L_scope) [notation, in L]
# _ (SKv_scope) [notation, in SKv]
_ =*= _ [notation, in SKv]
_ >>^ _ [notation, in SKv]
_ >>* _ [notation, in SKv]
_ >>> _ [notation, in SKv]
_ == _ [notation, in L]
_ >* _ [notation, in L]
_ >^ _ [notation, in L]
_ >> _ [notation, in L]
_ =2 _ [notation, in ARS]
_ <=2 _ [notation, in ARS]
_ =1 _ [notation, in ARS]
_ <=1 _ [notation, in ARS]
_ === _ [notation, in Base]
_ <<= _ [notation, in Base]
_ el _ [notation, in Base]
eq_dec _ [notation, in Base]
!! _ [notation, in L]
(λ _ ) [notation, in L]
.\ _ , .. , _ ; _ [notation, in L]
| _ | [notation, in Base]
λ _ , .. , _ ; _ [notation, in L]



Notation Index

F

_ >^ _ [in UnifConfl]
_ >> _ [in UnifConfl]


P

_ .[ _ ] [in Base]


other

_ >[]^ _ (LC_scope) [in LC]
_ >[]* _ (LC_scope) [in LC]
_ >[]> _ (LC_scope) [in LC]
# _ (LC_scope) [in LC]
# _ (L_scope) [in L]
# _ (SKv_scope) [in SKv]
_ =*= _ [in SKv]
_ >>^ _ [in SKv]
_ >>* _ [in SKv]
_ >>> _ [in SKv]
_ == _ [in L]
_ >* _ [in L]
_ >^ _ [in L]
_ >> _ [in L]
_ =2 _ [in ARS]
_ <=2 _ [in ARS]
_ =1 _ [in ARS]
_ <=1 _ [in ARS]
_ === _ [in Base]
_ <<= _ [in Base]
_ el _ [in Base]
eq_dec _ [in Base]
!! _ [in L]
(λ _ ) [in L]
.\ _ , .. , _ ; _ [in L]
| _ | [in Base]
λ _ , .. , _ ; _ [in L]



Module Index

F

FCI [in Base]



Variable Index

C

Cardinality.X [in Base]


D

DupfreeLength.X [in Base]
Dupfree.X [in Base]


E

Equi.X [in Base]


F

FCI.FCI.step [in Base]
FCI.FCI.V [in Base]
FCI.FCI.X [in Base]
FilterComm.p [in Base]
FilterComm.q [in Base]
FilterComm.X [in Base]
FilterLemmas_pq.q [in Base]
FilterLemmas_pq.p [in Base]
FilterLemmas_pq.X [in Base]
FilterLemmas.p [in Base]
FilterLemmas.X [in Base]
FixX.R [in UnifConfl]
FixX.UC.UC [in UnifConfl]
FixX.X [in UnifConfl]
FixX.X [in ARS]


I

Inclusion.X [in Base]
Iteration.f [in Base]
Iteration.X [in Base]


P

pos.X [in Base]
PowerRep.X [in Base]


R

Removal.X [in Base]


U

Undup.X [in Base]



Library Index

A

ARS


B

Base


L

L
LC
LC_eval
LexSizeInduction


S

SKv
SKvAbstraction
SKvTactics


U

UnifConfl



Lemma Index

A

absInj [in SKvAbstraction]
abs_lambda_equiv [in SKvAbstraction]
abs_nonLambda_continue [in SKvAbstraction]
abs_step_prefix [in SKvAbstraction]
abs_inv_size_val [in SKvAbstraction]
abs_inv_correct [in SKvAbstraction]
abs_no_Ss [in SKvAbstraction]
abs_no_S [in SKvAbstraction]
abs_no_K [in SKvAbstraction]
abs_no_var [in SKvAbstraction]
abs_sound [in SKvAbstraction]
abs_sound_pow [in SKvAbstraction]
abs_varClosed_iff [in SKvAbstraction]
abs_closed_eq [in SKvAbstraction]
abs_maxValue [in SKvAbstraction]
admissible_star [in LC]
admissible_step [in LC]
app_closed [in L]


C

card_0 [in Base]
card_cons_rem [in Base]
card_cons [in Base]
card_ex [in Base]
card_or [in Base]
card_lt [in Base]
card_equi [in Base]
card_eq [in Base]
card_le [in Base]
church_rosser [in L]
CInj [in SKvAbstraction]
closed_varClosed [in SKv]
closed_app [in SKv]
closed_star [in L]
closed_step [in L]
closed_subst [in L]
closed_app [in L]
closed_dclosed [in L]
closed_dcl [in L]
closed_k_dclosed [in L]
closed_r [in L]
closed_l [in L]
closed_dcl_x [in SKvTactics]
comb_proc_red [in L]
complete_induction [in Base]
confluence [in L]
confluent_CR [in ARS]
converges_equiv [in L]
C_eval_iff [in SKvAbstraction]
C_equiv_iff [in SKvAbstraction]
C_complete_equiv [in SKvAbstraction]
C_complete [in SKvAbstraction]
C_eval_complete [in SKvAbstraction]
C_eval_pullback [in SKvAbstraction]
C_star_prefix [in SKvAbstraction]
C_step_prefix [in SKvAbstraction]
C_step_app [in SKvAbstraction]
C_inv_correct [in SKvAbstraction]
C_eval_sound [in SKvAbstraction]
C_sound_equiv [in SKvAbstraction]
C_value_iff [in SKvAbstraction]
C_sound [in SKvAbstraction]
C_sound_pow [in SKvAbstraction]
C_near_value [in SKvAbstraction]
C_lam_value [in SKvAbstraction]
C_closed_if [in SKvAbstraction]
C_closed [in SKvAbstraction]
C_closed_varClosed [in SKvAbstraction]
C_dclosed_iff [in SKvAbstraction]


D

dclosedApp_iff [in L]
dclosedLam_iff [in L]
dclosedVar_iff [in L]
dclosed_closed [in L]
dclosed_gt [in L]
dclosed_ge [in L]
dclosed_closed_k [in L]
dec_prop_iff [in Base]
dec_DM_impl [in Base]
dec_DM_and [in Base]
dec_DN [in Base]
diamond_to_confluent [in ARS]
diamond_to_semi_confluent [in ARS]
disjoint_cons [in Base]
disjoint_forall [in Base]
dupfree_elAt [in Base]
dupfree_in_power [in Base]
dupfree_power [in Base]
dupfree_equi [in Base]
dupfree_ex [in Base]
dupfree_lt [in Base]
dupfree_eq [in Base]
dupfree_le [in Base]
dupfree_reorder [in Base]
dupfree_undup [in Base]
dupfree_dec [in Base]
dupfree_filter [in Base]
dupfree_map [in Base]
dupfree_app [in Base]
dupfree_inv [in Base]


E

ecl_sym [in ARS]
ecl_trans [in ARS]
elAt_el [in Base]
elAt_app [in Base]
el_elAt [in Base]
el_pos [in Base]
emptEnv [in LC]
emptEnv_admissible [in LC]
eqApp [in L]
eqAppL [in SKv]
eqAppR [in SKv]
eqStarT [in L]
equiv_value_eq [in SKv]
equiv_value [in SKv]
equiv_lambda [in L]
equiv_ecl [in L]
equi_rotate [in Base]
equi_shift [in Base]
equi_swap [in Base]
equi_dup [in Base]
equi_push [in Base]
Eta [in L]
eval_iff [in SKv]


F

FCI.closure [in Base]
FCI.fp [in Base]
FCI.incl [in Base]
FCI.ind [in Base]
FCI.it_incl [in Base]
FCI.pick [in Base]
filter_comm [in Base]
filter_and [in Base]
filter_pq_eq [in Base]
filter_pq_mono [in Base]
filter_fst' [in Base]
filter_app [in Base]
filter_fst [in Base]
filter_mono [in Base]
filter_incl [in Base]
flattenInj [in SKvAbstraction]
flattenInv_size [in SKvAbstraction]
flattenInv_correct [in SKvAbstraction]
flatten_subst_commute [in SKvAbstraction]
flatten_subst_varClosed [in SKvAbstraction]
flatten_varClosed_iff [in SKvAbstraction]
flatten_closed_idem [in SKvAbstraction]
flatten_value [in SKvAbstraction]


I

incl_lrcons [in Base]
incl_rcons [in Base]
incl_lcons [in Base]
incl_shift [in Base]
incl_nil_eq [in Base]
incl_map [in Base]
incl_nil [in Base]
in_rem_iff [in Base]
in_filter_iff [in Base]
in_cons_neq [in Base]
in_sing [in Base]
irred_appR [in SKv]
irred_appL [in SKv]
irred_iff [in L]
irred_pow [in UnifConfl]
it_fp [in Base]
it_ind [in Base]
I_closed [in SKv]
I_value [in SKv]


L

lambda_lam [in L]
LC_UC [in LC]
lex_size_lt_wf [in LexSizeInduction]
list_cc [in Base]
list_exists_DM [in Base]
list_sigma_forall [in Base]
list_cycle [in Base]
Lstep_complete_star [in LC]


M

maxValueSubst [in SKv]
maxValue_Value [in SKv]


N

normal_value [in SKv]
nth_error_none [in Base]


P

pos_elAt [in Base]
power_extensional [in Base]
power_nil [in Base]
power_incl [in Base]
powSk [in L]
pow_decompose [in SKv]
pow_trans_lam [in L]
pow_trans_lam' [in L]
pow_add [in ARS]
pow_star [in ARS]
pow_app [in LC]
pow_app_r [in LC]
pow_app_l [in LC]
proc_dec [in L]
proc_lambda [in SKvTactics]
proc_closed [in SKvTactics]
pSubst_closed [in LC]
pSubst_dclosed [in LC]
pSubst_cons [in LC]
pSubst_nil [in LC]


R

rcomp_1 [in ARS]
rem_fst' [in Base]
rem_fst [in Base]
rem_comm [in Base]
rem_equi [in Base]
rem_app' [in Base]
rem_app [in Base]
rem_neq [in Base]
rem_in [in Base]
rem_cons' [in Base]
rem_cons [in Base]
rem_mono [in Base]
rem_incl [in Base]
rem_not_in [in Base]
rep_dupfree [in Base]
rep_idempotent [in Base]
rep_injective [in Base]
rep_eq [in Base]
rep_eq' [in Base]
rep_mono [in Base]
rep_equi [in Base]
rep_in [in Base]
rep_incl [in Base]
rep_power [in Base]


S

semi_confluent_confluent [in ARS]
simplified_real_step [in LC]
simplify_admissible [in LC]
simplify_simplified [in LC]
simplify_translate [in LC]
simplify_sound [in LC]
simplify'_simplified [in LC]
simplify'_translate [in LC]
simplify'_translate_var' [in LC]
simplify'_sound [in LC]
simulation [in LC]
simulation' [in LC]
size_induction [in Base]
SK_church_rosser [in SKv]
SK_UC [in SKv]
starStepL [in SKv]
starStepR [in SKv]
star_closed [in SKv]
star_value [in SKv]
star_equiv [in L]
star_trans_r [in L]
star_trans_l [in L]
star_ecl [in ARS]
star_pow [in ARS]
star_trans [in ARS]
star_simpl_ind [in ARS]
star_app_r [in LC]
star_app_l [in LC]
step_closed [in SKv]
step_pow_app [in SKv]
step_pow_app_r [in SKv]
step_pow_app_l [in SKv]
step_star [in L]
step_value [in L]
step_pow_app [in L]
step_pow_app_r [in L]
step_pow_app_l [in L]
subst_free_iff [in SKv]
subst_C_commute [in SKvAbstraction]
subst_abs_commute [in SKvAbstraction]


T

translate_complete [in LC]
translate_complete_param [in LC]
translate_lambda_iff [in LC]
translate_irstep_iff [in LC]
translate_simplified_complete [in LC]
translate_lam [in LC]
translate_sound [in LC]
translate_sound_step [in LC]
translate_map_closed [in LC]
translate_closed [in LC]


U

UC_niehren_iff [in UnifConfl]
UC_confluent [in UnifConfl]
UC_DC [in UnifConfl]
UD_UC [in UnifConfl]
undup_idempotent [in Base]
undup_eq [in Base]
undup_equi [in Base]
undup_incl [in Base]
undup_fp_equi [in Base]
uniformly_semi_confluent [in UnifConfl]
uniform_confluence [in L]
unif_unique [in UnifConfl]
unif_pow_normal [in UnifConfl]
unif_pow_normal_part [in UnifConfl]
unique_normal_forms [in L]


V

valueSubst [in SKv]
valueSubst_iff [in SKv]
value_step_unique [in SKv]
value_irred [in SKv]
value_iff_irred [in LC]
value_irred [in LC]
varClosedApp_iff [in SKv]
varClosedVar_iff [in SKv]
varClosed_closed [in SKv]
var_not_closed [in L]



Constructor Index

A

app [in SKv]
app [in L]
app [in LC]


B

bapp [in L]
blam [in L]
bter [in L]
bvar [in L]


C

clapp [in SKv]
clK [in SKv]
clos [in LC]
clS [in SKv]


D

dclApp [in L]
dcllam [in L]
dclvar [in L]
dupfreeC [in Base]
dupfreeN [in Base]


E

eclC [in ARS]
eclR [in ARS]
eclS [in ARS]
eqRef [in L]
eqStep [in L]
eqSym [in L]
eqTrans [in L]


K

K [in SKv]


L

lam [in L]


S

S [in SKv]
starC [in ARS]
starR [in ARS]
stepApp [in L]
stepApp [in LC]
stepAppL [in SKv]
stepAppL [in L]
stepAppL [in LC]
stepAppR [in SKv]
stepAppR [in L]
stepAppR [in LC]
stepBeta [in LC]
stepK [in SKv]
stepS [in SKv]
stepVar [in LC]


V

validLCApp [in LC]
validLCclos [in LC]
valK [in SKv]
valK1 [in SKv]
valS [in SKv]
valS1 [in SKv]
valueLam [in LC]
valVar [in SKv]
valX2 [in SKv]
var [in SKv]
var [in L]
var [in LC]
varClosedApp [in SKv]
varClosedK [in SKv]
varClosedS [in SKv]
varClosedVar [in SKv]



Inductive Index

A

admissible [in LC]


B

bterm [in L]


C

closed [in SKv]


D

dclosed [in L]
dupfree [in Base]


E

ecl [in ARS]
equiv [in L]


S

star [in ARS]
step [in SKv]
step [in L]
step [in LC]


T

term [in SKv]
term [in L]
term [in LC]


V

value [in SKv]
value [in LC]
varClosed [in SKv]



Instance Index

A

admissible_step_proper [in LC]
and_dec [in Base]
app_equi_proper [in Base]


B

bool_eq_dec [in Base]


C

card_equi_proper [in Base]
closed_dec [in SKv]
closed_dec [in L]
cons_equi_proper [in Base]
converges_proper [in L]


D

dclosed_dec [in L]


E

ecl_equivalence [in ARS]
equiv_app_proper [in SKv]
equiv_app_proper [in L]
equiv_Equivalence [in L]
equi_Equivalence [in Base]
eq_dec_string [in L]


F

False_dec [in Base]
freeLvwVar_dec [in SKv]


I

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


L

lambda_dec [in L]
LC_eq_dec [in LC]
list_exists_dec [in Base]
list_forall_dec [in Base]
list_in_dec [in Base]
list_eq_dec [in Base]


N

nat_le_dec [in Base]
nat_eq_dec [in Base]
not_dec [in Base]


O

or_dec [in Base]


P

pow_star_subrelation [in ARS]
prod_eq_dec [in Base]


R

R_ecl_subrelation [in ARS]
R_star_subrelation [in ARS]


S

SKv_eq_dec [in SKv]
star_app_proper [in SKv]
star_equiv_subrelation [in L]
star_closed_proper [in L]
star_step_app_proper [in L]
star_ecl_subrelation [in ARS]
star_PreOrder [in ARS]
star_step_app_proper [in LC]
step_equiv_subrelation [in L]


T

term_eq_dec [in L]
True_dec [in Base]


V

value_dec [in SKv]
value_dec [in LC]



Section Index

C

Cardinality [in Base]


D

Dupfree [in Base]
DupfreeLength [in Base]


E

Equi [in Base]


F

FCI.FCI [in Base]
FilterComm [in Base]
FilterLemmas [in Base]
FilterLemmas_pq [in Base]
FixX [in UnifConfl]
FixX [in ARS]
FixX.UC [in UnifConfl]


I

Inclusion [in Base]
Iteration [in Base]


P

pos [in Base]
PowerRep [in Base]


R

Removal [in Base]


U

Undup [in Base]



Definition Index

A

abs [in SKvAbstraction]
abs_inv [in SKvAbstraction]


C

C [in SKvAbstraction]
card [in Base]
church_rosser [in ARS]
closed [in L]
comp_eqb_spec [in LC]
comp_eqb [in LC]
confluent [in ARS]
converges [in L]
convert [in L]
convert' [in L]


D

dec [in Base]
decision [in Base]
diamond [in ARS]
disjoint [in Base]


E

elAt [in Base]
equi [in Base]
eval [in SKv]
eval [in L]
eval [in LC]
evalBeta [in LC_eval]
evalLC [in LC_eval]


F

FCI.C [in Base]
FCI.F [in Base]
filter [in Base]
flatten [in SKvAbstraction]
flatten_inv [in SKvAbstraction]
FP [in Base]
functional [in ARS]


I

I [in SKv]
I [in L]
inclp [in Base]
irred [in UnifConfl]
it [in Base]


J

joinable [in ARS]


K

K [in L]


L

lambda [in L]
lex_size_induction [in LexSizeInduction]
lex_size_lt [in LexSizeInduction]
lSize [in SKvAbstraction]


M

maxValue [in SKv]


O

Omega [in L]
omega [in L]


P

pos [in Base]
pow [in ARS]
power [in Base]
proc [in L]
pSubst [in LC]


R

R [in L]
r [in L]
rcomp [in ARS]
reflexive [in ARS]
rem [in Base]
rep [in Base]
rho [in L]


S

semi_confluent [in ARS]
simplified [in LC]
simplify [in LC]
simplify' [in LC]
size [in SKv]
size [in L]
subst [in SKv]
subst [in L]
symmetric [in ARS]


T

term_eq_dec_proc [in L]
term_ind_deep [in LC]
term_rec_deep' [in LC]
transitive [in ARS]
translate [in LC]


U

UC_niehren [in UnifConfl]
undup [in Base]
uniformly_confluent [in UnifConfl]
uniform_diamond [in UnifConfl]



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 (574 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 (30 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 (26 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 (10 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 (293 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 (56 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 (17 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 (50 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 (17 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 (74 entries)

This page has been generated by coqdoc