| 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
ARSB
BaseL
LLC
LC_eval
LexSizeInduction
S
SKvSKvAbstraction
SKvTactics
U
UnifConflLemma 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