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

LLC

LC_eval

LexSizeInduction

## S

SKvSKvAbstraction

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