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 | (489 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 | (5 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 | (27 entries) |

Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |

Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (263 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 | (29 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 | (14 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 | (48 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 | (18 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 | (71 entries) |

# Global Index

## A

and_dec [instance, in CFG.Base]app_equi_proper [instance, in CFG.Base]

app_incl_proper [instance, in CFG.Base]

## B

Base [library]bin [definition, in CFG.Binarize]

Binarize [library]

binary [definition, in CFG.Binarize]

binary_unit [lemma, in CFG.Chomsky]

binary_elimE [lemma, in CFG.Chomsky]

binary_sep [lemma, in CFG.Chomsky]

bin_language [lemma, in CFG.Binarize]

bin_der_equiv [lemma, in CFG.Binarize]

bin_binary [lemma, in CFG.Binarize]

bin_dom [lemma, in CFG.Chomsky]

bool_eq_dec [instance, in CFG.Base]

## C

card [definition, in CFG.Base]Cardinality [section, in CFG.Base]

Cardinality.X [variable, in CFG.Base]

card_equi_proper [instance, in CFG.Base]

card_or [lemma, in CFG.Base]

card_lt [lemma, in CFG.Base]

card_equi [lemma, in CFG.Base]

card_ex [lemma, in CFG.Base]

card_0 [lemma, in CFG.Base]

card_cons_rem [lemma, in CFG.Base]

card_eq [lemma, in CFG.Base]

card_le [lemma, in CFG.Base]

card_not_in_rem [lemma, in CFG.Base]

card_in_rem [lemma, in CFG.Base]

charfree [definition, in CFG.Separate]

chomsky [definition, in CFG.Chomsky]

Chomsky [library]

chomsky_normalform [lemma, in CFG.Chomsky]

closure [definition, in CFG.ElimE]

closure_slist [lemma, in CFG.ElimE]

concat [definition, in CFG.Lists]

concat_split [lemma, in CFG.Lists]

cons_equi_proper [instance, in CFG.Base]

cons_incl_proper [instance, in CFG.Base]

count_decr [lemma, in CFG.Binarize]

count_bin [definition, in CFG.Binarize]

count_decr [lemma, in CFG.Separate]

count_sep_decr [lemma, in CFG.Separate]

count_chars_decr [lemma, in CFG.Separate]

count_chars_split [lemma, in CFG.Separate]

count_sep_substL [lemma, in CFG.Separate]

count_chars_substL [lemma, in CFG.Separate]

count_sep_split [lemma, in CFG.Separate]

count_sep [definition, in CFG.Separate]

count_chars [definition, in CFG.Separate]

## D

dec [definition, in CFG.Base]decision [definition, in CFG.Base]

dec_charfree [instance, in CFG.Separate]

dec_prop_iff [lemma, in CFG.Base]

dec_DM_impl [lemma, in CFG.Base]

dec_DM_and [lemma, in CFG.Base]

dec_DN [lemma, in CFG.Base]

Dec_Emptys.G [variable, in CFG.Dec_Empty]

Dec_Emptys [section, in CFG.Dec_Empty]

Dec_Word.u [variable, in CFG.Dec_Word]

Dec_Word.G [variable, in CFG.Dec_Word]

Dec_Word [section, in CFG.Dec_Word]

Dec_Word [library]

Dec_Empty [library]

Definitions [library]

delE [definition, in CFG.ElimE]

DelE [section, in CFG.ElimE]

delE_der_equiv [lemma, in CFG.ElimE]

delE_rules [lemma, in CFG.ElimE]

delE_preserveG [lemma, in CFG.ElimE]

delE_efree [lemma, in CFG.ElimE]

DelE.G [variable, in CFG.ElimE]

der [inductive, in CFG.Derivation]

derE_nullable [lemma, in CFG.ElimE]

derf [inductive, in CFG.Derivation]

derfelimU_derfG [lemma, in CFG.ElimU]

derfG_derfelimU [lemma, in CFG.ElimU]

derf_der_equiv [lemma, in CFG.Derivation]

derf_derT [lemma, in CFG.Derivation]

derf_trans [lemma, in CFG.Derivation]

derf_split [lemma, in CFG.Derivation]

derf_concat [lemma, in CFG.Derivation]

derf_productive [lemma, in CFG.Dec_Empty]

derf_DW [lemma, in CFG.Dec_Word]

derI [inductive, in CFG.Derivation]

derIRefl [constructor, in CFG.Derivation]

derIRule [constructor, in CFG.Derivation]

derITrans [constructor, in CFG.Derivation]

Derivation [library]

derI_derf [lemma, in CFG.Derivation]

derL [inductive, in CFG.Derivation]

derL_der_equiv [lemma, in CFG.Derivation]

derT [inductive, in CFG.Derivation]

derTRefl [constructor, in CFG.Derivation]

derTRule [constructor, in CFG.Derivation]

derTTrans [constructor, in CFG.Derivation]

derT_concat [lemma, in CFG.Derivation]

derT_trans [lemma, in CFG.Derivation]

derT_derI [lemma, in CFG.Derivation]

derT_der_equiv [lemma, in CFG.Derivation]

derT_slist [lemma, in CFG.ElimE]

der_equiv_G [lemma, in CFG.Derivation]

der_subset [lemma, in CFG.Derivation]

der_G_inlL [lemma, in CFG.Inlining]

der_inlL_G [lemma, in CFG.Inlining]

der_inlL_G' [lemma, in CFG.Inlining]

der_substG_G_equiv [lemma, in CFG.Inlining]

der_G_substG [lemma, in CFG.Inlining]

der_G_substG' [lemma, in CFG.Inlining]

der_substG_G [lemma, in CFG.Inlining]

der_dec [instance, in CFG.Dec_Word]

der_G_delE [lemma, in CFG.ElimE]

der_eclosure_equiv [lemma, in CFG.ElimE]

disjoint [definition, in CFG.Base]

disjoint_cons [lemma, in CFG.Base]

disjoint_forall [lemma, in CFG.Base]

disjoint_incl [lemma, in CFG.Base]

disjoint_symm [lemma, in CFG.Base]

disjoint_nil' [lemma, in CFG.Base]

disjoint_nil [lemma, in CFG.Base]

dom [definition, in CFG.Symbols]

domG_rule [lemma, in CFG.Symbols]

domV [definition, in CFG.ElimU]

domVG_rule [lemma, in CFG.ElimU]

dom_domV [lemma, in CFG.ElimU]

dom_subset [lemma, in CFG.Symbols]

Dupfree [section, in CFG.Base]

dupfree [inductive, in CFG.Base]

dupfreeC [constructor, in CFG.Base]

dupfreeN [constructor, in CFG.Base]

dupfree_inv [definition, in CFG.Base]

dupfree_in_power [lemma, in CFG.Base]

dupfree_power [lemma, in CFG.Base]

dupfree_undup [lemma, in CFG.Base]

dupfree_card [lemma, in CFG.Base]

dupfree_dec [lemma, in CFG.Base]

dupfree_filter [lemma, in CFG.Base]

dupfree_map [lemma, in CFG.Base]

dupfree_app [lemma, in CFG.Base]

dupfree_cons [lemma, in CFG.Base]

Dupfree.X [variable, in CFG.Base]

DW [definition, in CFG.Dec_Word]

DW_der_equiv [lemma, in CFG.Dec_Word]

DW_der_equiv' [lemma, in CFG.Dec_Word]

DW_derf' [lemma, in CFG.Dec_Word]

## E

eclosed [definition, in CFG.ElimE]eclosed_eclosure [lemma, in CFG.ElimE]

eclosure [definition, in CFG.ElimE]

EClosure [section, in CFG.ElimE]

eclosure_der [lemma, in CFG.ElimE]

EClosure.G [variable, in CFG.ElimE]

efree [definition, in CFG.ElimE]

efree_unit [lemma, in CFG.Chomsky]

efree_elimE [lemma, in CFG.ElimE]

elimE [definition, in CFG.ElimE]

ElimE [library]

elimE_language [lemma, in CFG.ElimE]

elimU [definition, in CFG.ElimU]

ElimU [library]

elimU_der_equiv [lemma, in CFG.ElimU]

elimU_corr3 [lemma, in CFG.ElimU]

elimU_corr3' [lemma, in CFG.ElimU]

elimU_corr2 [lemma, in CFG.ElimU]

elimU_corr [lemma, in CFG.ElimU]

Equi [section, in CFG.Base]

equi [definition, in CFG.Base]

equi_rotate [lemma, in CFG.Base]

equi_shift [lemma, in CFG.Base]

equi_swap [lemma, in CFG.Base]

equi_dup [lemma, in CFG.Base]

equi_push [lemma, in CFG.Base]

equi_Equivalence [instance, in CFG.Base]

Equi.X [variable, in CFG.Base]

eq_dec_prod [instance, in CFG.Lists]

excluded_unit [lemma, in CFG.Chomsky]

excluded_free [lemma, in CFG.Chomsky]

exists_phrase_dec [instance, in CFG.Definitions]

exists_rule_dec [instance, in CFG.Definitions]

exists_dec [instance, in CFG.Dec_Empty]

## F

False_dec [instance, in CFG.Base]FCI [module, in CFG.Base]

FCI.C [definition, in CFG.Base]

FCI.closure [lemma, in CFG.Base]

FCI.F [definition, in CFG.Base]

FCI.FCI [section, in CFG.Base]

FCI.FCI.step [variable, in CFG.Base]

FCI.FCI.V [variable, in CFG.Base]

FCI.FCI.X [variable, in CFG.Base]

FCI.fp [lemma, in CFG.Base]

FCI.incl [lemma, in CFG.Base]

FCI.ind [lemma, in CFG.Base]

FCI.it_incl [lemma, in CFG.Base]

FCI.pick [lemma, in CFG.Base]

fCons [constructor, in CFG.Derivation]

filter [definition, in CFG.Base]

FilterComm [section, in CFG.Base]

FilterComm.p [variable, in CFG.Base]

FilterComm.q [variable, in CFG.Base]

FilterComm.X [variable, in CFG.Base]

FilterLemmas [section, in CFG.Base]

FilterLemmas_pq.q [variable, in CFG.Base]

FilterLemmas_pq.p [variable, in CFG.Base]

FilterLemmas_pq.X [variable, in CFG.Base]

FilterLemmas_pq [section, in CFG.Base]

FilterLemmas.p [variable, in CFG.Base]

FilterLemmas.X [variable, in CFG.Base]

filter_rule_dec [instance, in CFG.Definitions]

filter_comm [lemma, in CFG.Base]

filter_and [lemma, in CFG.Base]

filter_pq_eq [lemma, in CFG.Base]

filter_pq_mono [lemma, in CFG.Base]

filter_fst' [lemma, in CFG.Base]

filter_fst [lemma, in CFG.Base]

filter_app [lemma, in CFG.Base]

filter_id [lemma, in CFG.Base]

filter_mono [lemma, in CFG.Base]

filter_incl [lemma, in CFG.Base]

filter_prod_dec [instance, in CFG.Lists]

FP [definition, in CFG.Base]

fp_binary [lemma, in CFG.Binarize]

fp_bin [lemma, in CFG.Binarize]

fp_uniform [lemma, in CFG.Separate]

fp_sep [lemma, in CFG.Separate]

fRefl [constructor, in CFG.Derivation]

fresh [definition, in CFG.Symbols]

fresh_symbs [lemma, in CFG.Symbols]

fRule [constructor, in CFG.Derivation]

fsts [definition, in CFG.Lists]

fsts_split [lemma, in CFG.Lists]

fsts_comb_corr [lemma, in CFG.Dec_Word]

fsts_comb_corr2 [lemma, in CFG.Dec_Word]

fsts_comb_corr1 [lemma, in CFG.Dec_Word]

fsts_comb [definition, in CFG.Dec_Word]

## G

gDer [constructor, in CFG.Derivation]getNat [definition, in CFG.Symbols]

grammar [definition, in CFG.Definitions]

## I

iff_dec [instance, in CFG.Base]impl_dec [instance, in CFG.Base]

inclp [definition, in CFG.Base]

Inclusion [section, in CFG.Base]

Inclusion.X [variable, in CFG.Base]

incl_equi_proper [instance, in CFG.Base]

incl_preorder [instance, in CFG.Base]

incl_app_left [lemma, in CFG.Base]

incl_lrcons [lemma, in CFG.Base]

incl_rcons [lemma, in CFG.Base]

incl_sing [lemma, in CFG.Base]

incl_lcons [lemma, in CFG.Base]

incl_shift [lemma, in CFG.Base]

incl_nil_eq [lemma, in CFG.Base]

incl_map [lemma, in CFG.Base]

incl_nil [lemma, in CFG.Base]

inlinable [inductive, in CFG.Inlining]

inlinable_cons [lemma, in CFG.Inlining]

Inlining [library]

inlL [definition, in CFG.Inlining]

inlL_langauge_equiv [lemma, in CFG.Inlining]

inlL_dom [lemma, in CFG.Inlining]

inlL_skip [lemma, in CFG.Inlining]

inl_language_equiv [lemma, in CFG.Inlining]

inN [constructor, in CFG.Inlining]

inR [constructor, in CFG.Inlining]

in_substG_der [lemma, in CFG.Inlining]

in_rem_iff [lemma, in CFG.Base]

in_filter_iff [lemma, in CFG.Base]

in_equi_proper [instance, in CFG.Base]

in_incl_proper [instance, in CFG.Base]

in_cons_neq [lemma, in CFG.Base]

in_sing [lemma, in CFG.Base]

it [definition, in CFG.Base]

item [definition, in CFG.Dec_Word]

items [definition, in CFG.Dec_Word]

items_refl [lemma, in CFG.Dec_Word]

Iteration [section, in CFG.Base]

Iteration.f [variable, in CFG.Base]

Iteration.X [variable, in CFG.Base]

it_fp [lemma, in CFG.Base]

it_ind [lemma, in CFG.Base]

## L

language [definition, in CFG.Derivation]language_normalform [lemma, in CFG.Chomsky]

lang_dec [instance, in CFG.Dec_Word]

Lists [library]

list_cc [lemma, in CFG.Base]

list_exists_not_incl [lemma, in CFG.Base]

list_exists_DM [lemma, in CFG.Base]

list_exists_dec [instance, in CFG.Base]

list_forall_dec [instance, in CFG.Base]

list_sigma_forall [lemma, in CFG.Base]

list_in_dec [instance, in CFG.Base]

list_eq_dec [instance, in CFG.Base]

list_cycle [lemma, in CFG.Base]

list_unit [lemma, in CFG.Lists]

## M

maxSymb [definition, in CFG.Symbols]maxSymbRule [definition, in CFG.Symbols]

maxSymbRule_corr [lemma, in CFG.Symbols]

maxSymb_corr [lemma, in CFG.Symbols]

Membership [section, in CFG.Base]

Membership.X [variable, in CFG.Base]

## N

N [definition, in CFG.ElimU]nat_le_dec [instance, in CFG.Base]

nat_eq_dec [instance, in CFG.Base]

normalize [definition, in CFG.Chomsky]

not_in_cons [lemma, in CFG.Base]

not_dec [instance, in CFG.Base]

Null [constructor, in CFG.ElimE]

nullable [inductive, in CFG.ElimE]

nullable_eclosure [lemma, in CFG.ElimE]

nullable_dec [instance, in CFG.ElimE]

nullable_derE_equi [lemma, in CFG.ElimE]

nullable_derE [lemma, in CFG.ElimE]

## O

or_dec [instance, in CFG.Base]## P

P [definition, in CFG.Dec_Empty]phrase [definition, in CFG.Definitions]

phrase_char_dec [instance, in CFG.Definitions]

phrase_var_dec [instance, in CFG.Definitions]

pickChar [lemma, in CFG.Separate]

pickCharRule [lemma, in CFG.Separate]

pickFresh [lemma, in CFG.Symbols]

power [definition, in CFG.Base]

PowerRep [section, in CFG.Base]

PowerRep.X [variable, in CFG.Base]

power_extensional [lemma, in CFG.Base]

power_nil [lemma, in CFG.Base]

power_incl [lemma, in CFG.Base]

product [definition, in CFG.Lists]

productive [inductive, in CFG.Dec_Empty]

productive_dec [instance, in CFG.Dec_Empty]

productive_P [lemma, in CFG.Dec_Empty]

productive_derWord_equi [lemma, in CFG.Dec_Empty]

productive_derf [lemma, in CFG.Dec_Empty]

prod_corr [lemma, in CFG.Lists]

prod_corr2 [lemma, in CFG.Lists]

prod_corr1 [lemma, in CFG.Lists]

P_productive_equiv [lemma, in CFG.Dec_Empty]

P_productive [lemma, in CFG.Dec_Empty]

## R

R [constructor, in CFG.Definitions]ran [definition, in CFG.Symbols]

ranG_rule [lemma, in CFG.Symbols]

ran_elimU_G [lemma, in CFG.ElimU]

rDer [constructor, in CFG.Derivation]

rem [definition, in CFG.Base]

Removal [section, in CFG.Base]

Removal.X [variable, in CFG.Base]

rem_inclr [lemma, in CFG.Base]

rem_reorder [lemma, in CFG.Base]

rem_id [lemma, in CFG.Base]

rem_fst' [lemma, in CFG.Base]

rem_fst [lemma, in CFG.Base]

rem_comm [lemma, in CFG.Base]

rem_equi [lemma, in CFG.Base]

rem_app' [lemma, in CFG.Base]

rem_app [lemma, in CFG.Base]

rem_neq [lemma, in CFG.Base]

rem_in [lemma, in CFG.Base]

rem_cons' [lemma, in CFG.Base]

rem_cons [lemma, in CFG.Base]

rem_mono [lemma, in CFG.Base]

rem_incl [lemma, in CFG.Base]

rem_not_in [lemma, in CFG.Base]

rep [definition, in CFG.Base]

replN [constructor, in CFG.Derivation]

rep_dupfree [lemma, in CFG.Base]

rep_idempotent [lemma, in CFG.Base]

rep_injective [lemma, in CFG.Base]

rep_eq [lemma, in CFG.Base]

rep_eq' [lemma, in CFG.Base]

rep_mono [lemma, in CFG.Base]

rep_equi [lemma, in CFG.Base]

rep_in [lemma, in CFG.Base]

rep_incl [lemma, in CFG.Base]

rep_power [lemma, in CFG.Base]

rule [inductive, in CFG.Definitions]

rules [definition, in CFG.ElimU]

rule_domVG [lemma, in CFG.ElimU]

rule_eq_dec [instance, in CFG.Definitions]

rule_ranG [lemma, in CFG.Symbols]

rule_domG [lemma, in CFG.Symbols]

## S

sDer [constructor, in CFG.Derivation]segment [definition, in CFG.Lists]

segment_trans [lemma, in CFG.Lists]

segment_refl [lemma, in CFG.Lists]

segment_nil [lemma, in CFG.Lists]

segms [definition, in CFG.Lists]

segms_corr [lemma, in CFG.Lists]

segms_corr2 [lemma, in CFG.Lists]

segms_corr1 [lemma, in CFG.Lists]

sep [definition, in CFG.Separate]

Separate [library]

sep_language [lemma, in CFG.Separate]

sep_der_equiv [lemma, in CFG.Separate]

sep_uniform [lemma, in CFG.Separate]

size_recursion [lemma, in CFG.Base]

sless [definition, in CFG.Symbols]

sless_monotone [lemma, in CFG.Symbols]

sless_dec [instance, in CFG.Symbols]

sless' [definition, in CFG.Symbols]

slist [inductive, in CFG.Lists]

slists [definition, in CFG.Lists]

slists_slist [lemma, in CFG.Lists]

slist_pred [lemma, in CFG.Lists]

slist_length [lemma, in CFG.Lists]

slist_subsumes [lemma, in CFG.Lists]

slist_split [lemma, in CFG.Lists]

slist_inv [lemma, in CFG.Lists]

slist_equiv_pred [lemma, in CFG.Lists]

slist_append [lemma, in CFG.Lists]

slist_trans [lemma, in CFG.Lists]

slist_id [lemma, in CFG.Lists]

slist_closure_equiv [lemma, in CFG.ElimE]

slist_closure [lemma, in CFG.ElimE]

snds [definition, in CFG.Lists]

snds_split [lemma, in CFG.Lists]

splitList_dec [instance, in CFG.Lists]

step [definition, in CFG.Binarize]

step [definition, in CFG.Separate]

step [definition, in CFG.ElimU]

step [definition, in CFG.Dec_Empty]

step [definition, in CFG.Dec_Word]

step_dom [lemma, in CFG.Binarize]

step_der_equiv [lemma, in CFG.Binarize]

step_or [lemma, in CFG.Binarize]

step_dom [lemma, in CFG.Separate]

step_der_equiv [lemma, in CFG.Separate]

step_dec [instance, in CFG.ElimU]

step_dec' [instance, in CFG.ElimU]

step_dec [instance, in CFG.Dec_Empty]

step_dec [instance, in CFG.Dec_Word]

step_dec' [instance, in CFG.Dec_Word]

step' [definition, in CFG.Binarize]

subcons [constructor, in CFG.Lists]

subconsp [constructor, in CFG.Lists]

subnil [constructor, in CFG.Lists]

substG [definition, in CFG.Inlining]

substG_der_equiv [lemma, in CFG.Separate]

substG_dom [lemma, in CFG.Inlining]

substG_inG [lemma, in CFG.Inlining]

substG_undo [lemma, in CFG.Inlining]

substG_skip [lemma, in CFG.Inlining]

substG_skipRule [lemma, in CFG.Inlining]

substG_split [lemma, in CFG.Inlining]

substG_preservesLength [lemma, in CFG.Chomsky]

substL [definition, in CFG.Lists]

substL_der [lemma, in CFG.Inlining]

substL_undo [lemma, in CFG.Lists]

substL_length_unit [lemma, in CFG.Lists]

substL_skip [lemma, in CFG.Lists]

substL_split [lemma, in CFG.Lists]

symbol [inductive, in CFG.Definitions]

Symbols [library]

symbol_ter_dec [instance, in CFG.Definitions]

symbol_eq_dec [instance, in CFG.Definitions]

symbs [definition, in CFG.Symbols]

symbs_der [lemma, in CFG.Derivation]

symbs_subset [lemma, in CFG.Symbols]

symbs_inv [lemma, in CFG.Symbols]

symbs_dom [lemma, in CFG.Symbols]

## T

T [constructor, in CFG.Definitions]ter [inductive, in CFG.Definitions]

terminal [definition, in CFG.Derivation]

terminal_split [lemma, in CFG.Derivation]

TProd [constructor, in CFG.Dec_Empty]

True_dec [instance, in CFG.Base]

Ts [constructor, in CFG.Definitions]

## U

undup [definition, in CFG.Base]Undup [section, in CFG.Base]

undup_idempotent [lemma, in CFG.Base]

undup_id [lemma, in CFG.Base]

undup_equi [lemma, in CFG.Base]

undup_incl [lemma, in CFG.Base]

undup_id_equi [lemma, in CFG.Base]

Undup.X [variable, in CFG.Base]

uniform [definition, in CFG.Separate]

unitfree [definition, in CFG.ElimU]

unitfree_elimU [lemma, in CFG.ElimU]

unitfree_elimU' [lemma, in CFG.ElimU]

UnitRules [section, in CFG.ElimU]

UnitRules.G [variable, in CFG.ElimU]

unit_language [lemma, in CFG.ElimU]

## V

V [constructor, in CFG.Definitions]var [inductive, in CFG.Definitions]

var_eq_dec [instance, in CFG.Definitions]

vDer [constructor, in CFG.Derivation]

VProd [constructor, in CFG.Dec_Empty]

Vs [constructor, in CFG.Definitions]

## other

_ === _ [notation, in CFG.Base]_ <<= _ [notation, in CFG.Base]

_ el _ [notation, in CFG.Base]

eq_dec _ [notation, in CFG.Base]

| _ | [notation, in CFG.Base]

# Notation Index

## other

_ === _ [in CFG.Base]_ <<= _ [in CFG.Base]

_ el _ [in CFG.Base]

eq_dec _ [in CFG.Base]

| _ | [in CFG.Base]

# Module Index

## F

FCI [in CFG.Base]# Variable Index

## C

Cardinality.X [in CFG.Base]## D

Dec_Emptys.G [in CFG.Dec_Empty]Dec_Word.u [in CFG.Dec_Word]

Dec_Word.G [in CFG.Dec_Word]

DelE.G [in CFG.ElimE]

Dupfree.X [in CFG.Base]

## E

EClosure.G [in CFG.ElimE]Equi.X [in CFG.Base]

## F

FCI.FCI.step [in CFG.Base]FCI.FCI.V [in CFG.Base]

FCI.FCI.X [in CFG.Base]

FilterComm.p [in CFG.Base]

FilterComm.q [in CFG.Base]

FilterComm.X [in CFG.Base]

FilterLemmas_pq.q [in CFG.Base]

FilterLemmas_pq.p [in CFG.Base]

FilterLemmas_pq.X [in CFG.Base]

FilterLemmas.p [in CFG.Base]

FilterLemmas.X [in CFG.Base]

## I

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

Iteration.X [in CFG.Base]

## M

Membership.X [in CFG.Base]## P

PowerRep.X [in CFG.Base]## R

Removal.X [in CFG.Base]## U

Undup.X [in CFG.Base]UnitRules.G [in CFG.ElimU]

# Library Index

## B

BaseBinarize

## C

Chomsky## D

Dec_WordDec_Empty

Definitions

Derivation

## E

ElimEElimU

## I

Inlining## L

Lists## S

SeparateSymbols

# Lemma Index

## B

binary_unit [in CFG.Chomsky]binary_elimE [in CFG.Chomsky]

binary_sep [in CFG.Chomsky]

bin_language [in CFG.Binarize]

bin_der_equiv [in CFG.Binarize]

bin_binary [in CFG.Binarize]

bin_dom [in CFG.Chomsky]

## C

card_or [in CFG.Base]card_lt [in CFG.Base]

card_equi [in CFG.Base]

card_ex [in CFG.Base]

card_0 [in CFG.Base]

card_cons_rem [in CFG.Base]

card_eq [in CFG.Base]

card_le [in CFG.Base]

card_not_in_rem [in CFG.Base]

card_in_rem [in CFG.Base]

chomsky_normalform [in CFG.Chomsky]

closure_slist [in CFG.ElimE]

concat_split [in CFG.Lists]

count_decr [in CFG.Binarize]

count_decr [in CFG.Separate]

count_sep_decr [in CFG.Separate]

count_chars_decr [in CFG.Separate]

count_chars_split [in CFG.Separate]

count_sep_substL [in CFG.Separate]

count_chars_substL [in CFG.Separate]

count_sep_split [in CFG.Separate]

## D

dec_prop_iff [in CFG.Base]dec_DM_impl [in CFG.Base]

dec_DM_and [in CFG.Base]

dec_DN [in CFG.Base]

delE_der_equiv [in CFG.ElimE]

delE_rules [in CFG.ElimE]

delE_preserveG [in CFG.ElimE]

delE_efree [in CFG.ElimE]

derE_nullable [in CFG.ElimE]

derfelimU_derfG [in CFG.ElimU]

derfG_derfelimU [in CFG.ElimU]

derf_der_equiv [in CFG.Derivation]

derf_derT [in CFG.Derivation]

derf_trans [in CFG.Derivation]

derf_split [in CFG.Derivation]

derf_concat [in CFG.Derivation]

derf_productive [in CFG.Dec_Empty]

derf_DW [in CFG.Dec_Word]

derI_derf [in CFG.Derivation]

derL_der_equiv [in CFG.Derivation]

derT_concat [in CFG.Derivation]

derT_trans [in CFG.Derivation]

derT_derI [in CFG.Derivation]

derT_der_equiv [in CFG.Derivation]

derT_slist [in CFG.ElimE]

der_equiv_G [in CFG.Derivation]

der_subset [in CFG.Derivation]

der_G_inlL [in CFG.Inlining]

der_inlL_G [in CFG.Inlining]

der_inlL_G' [in CFG.Inlining]

der_substG_G_equiv [in CFG.Inlining]

der_G_substG [in CFG.Inlining]

der_G_substG' [in CFG.Inlining]

der_substG_G [in CFG.Inlining]

der_G_delE [in CFG.ElimE]

der_eclosure_equiv [in CFG.ElimE]

disjoint_cons [in CFG.Base]

disjoint_forall [in CFG.Base]

disjoint_incl [in CFG.Base]

disjoint_symm [in CFG.Base]

disjoint_nil' [in CFG.Base]

disjoint_nil [in CFG.Base]

domG_rule [in CFG.Symbols]

domVG_rule [in CFG.ElimU]

dom_domV [in CFG.ElimU]

dom_subset [in CFG.Symbols]

dupfree_in_power [in CFG.Base]

dupfree_power [in CFG.Base]

dupfree_undup [in CFG.Base]

dupfree_card [in CFG.Base]

dupfree_dec [in CFG.Base]

dupfree_filter [in CFG.Base]

dupfree_map [in CFG.Base]

dupfree_app [in CFG.Base]

dupfree_cons [in CFG.Base]

DW_der_equiv [in CFG.Dec_Word]

DW_der_equiv' [in CFG.Dec_Word]

DW_derf' [in CFG.Dec_Word]

## E

eclosed_eclosure [in CFG.ElimE]eclosure_der [in CFG.ElimE]

efree_unit [in CFG.Chomsky]

efree_elimE [in CFG.ElimE]

elimE_language [in CFG.ElimE]

elimU_der_equiv [in CFG.ElimU]

elimU_corr3 [in CFG.ElimU]

elimU_corr3' [in CFG.ElimU]

elimU_corr2 [in CFG.ElimU]

elimU_corr [in CFG.ElimU]

equi_rotate [in CFG.Base]

equi_shift [in CFG.Base]

equi_swap [in CFG.Base]

equi_dup [in CFG.Base]

equi_push [in CFG.Base]

excluded_unit [in CFG.Chomsky]

excluded_free [in CFG.Chomsky]

## F

FCI.closure [in CFG.Base]FCI.fp [in CFG.Base]

FCI.incl [in CFG.Base]

FCI.ind [in CFG.Base]

FCI.it_incl [in CFG.Base]

FCI.pick [in CFG.Base]

filter_comm [in CFG.Base]

filter_and [in CFG.Base]

filter_pq_eq [in CFG.Base]

filter_pq_mono [in CFG.Base]

filter_fst' [in CFG.Base]

filter_fst [in CFG.Base]

filter_app [in CFG.Base]

filter_id [in CFG.Base]

filter_mono [in CFG.Base]

filter_incl [in CFG.Base]

fp_binary [in CFG.Binarize]

fp_bin [in CFG.Binarize]

fp_uniform [in CFG.Separate]

fp_sep [in CFG.Separate]

fresh_symbs [in CFG.Symbols]

fsts_split [in CFG.Lists]

fsts_comb_corr [in CFG.Dec_Word]

fsts_comb_corr2 [in CFG.Dec_Word]

fsts_comb_corr1 [in CFG.Dec_Word]

## I

incl_app_left [in CFG.Base]incl_lrcons [in CFG.Base]

incl_rcons [in CFG.Base]

incl_sing [in CFG.Base]

incl_lcons [in CFG.Base]

incl_shift [in CFG.Base]

incl_nil_eq [in CFG.Base]

incl_map [in CFG.Base]

incl_nil [in CFG.Base]

inlinable_cons [in CFG.Inlining]

inlL_langauge_equiv [in CFG.Inlining]

inlL_dom [in CFG.Inlining]

inlL_skip [in CFG.Inlining]

inl_language_equiv [in CFG.Inlining]

in_substG_der [in CFG.Inlining]

in_rem_iff [in CFG.Base]

in_filter_iff [in CFG.Base]

in_cons_neq [in CFG.Base]

in_sing [in CFG.Base]

items_refl [in CFG.Dec_Word]

it_fp [in CFG.Base]

it_ind [in CFG.Base]

## L

language_normalform [in CFG.Chomsky]list_cc [in CFG.Base]

list_exists_not_incl [in CFG.Base]

list_exists_DM [in CFG.Base]

list_sigma_forall [in CFG.Base]

list_cycle [in CFG.Base]

list_unit [in CFG.Lists]

## M

maxSymbRule_corr [in CFG.Symbols]maxSymb_corr [in CFG.Symbols]

## N

not_in_cons [in CFG.Base]nullable_eclosure [in CFG.ElimE]

nullable_derE_equi [in CFG.ElimE]

nullable_derE [in CFG.ElimE]

## P

pickChar [in CFG.Separate]pickCharRule [in CFG.Separate]

pickFresh [in CFG.Symbols]

power_extensional [in CFG.Base]

power_nil [in CFG.Base]

power_incl [in CFG.Base]

productive_P [in CFG.Dec_Empty]

productive_derWord_equi [in CFG.Dec_Empty]

productive_derf [in CFG.Dec_Empty]

prod_corr [in CFG.Lists]

prod_corr2 [in CFG.Lists]

prod_corr1 [in CFG.Lists]

P_productive_equiv [in CFG.Dec_Empty]

P_productive [in CFG.Dec_Empty]

## R

ranG_rule [in CFG.Symbols]ran_elimU_G [in CFG.ElimU]

rem_inclr [in CFG.Base]

rem_reorder [in CFG.Base]

rem_id [in CFG.Base]

rem_fst' [in CFG.Base]

rem_fst [in CFG.Base]

rem_comm [in CFG.Base]

rem_equi [in CFG.Base]

rem_app' [in CFG.Base]

rem_app [in CFG.Base]

rem_neq [in CFG.Base]

rem_in [in CFG.Base]

rem_cons' [in CFG.Base]

rem_cons [in CFG.Base]

rem_mono [in CFG.Base]

rem_incl [in CFG.Base]

rem_not_in [in CFG.Base]

rep_dupfree [in CFG.Base]

rep_idempotent [in CFG.Base]

rep_injective [in CFG.Base]

rep_eq [in CFG.Base]

rep_eq' [in CFG.Base]

rep_mono [in CFG.Base]

rep_equi [in CFG.Base]

rep_in [in CFG.Base]

rep_incl [in CFG.Base]

rep_power [in CFG.Base]

rule_domVG [in CFG.ElimU]

rule_ranG [in CFG.Symbols]

rule_domG [in CFG.Symbols]

## S

segment_trans [in CFG.Lists]segment_refl [in CFG.Lists]

segment_nil [in CFG.Lists]

segms_corr [in CFG.Lists]

segms_corr2 [in CFG.Lists]

segms_corr1 [in CFG.Lists]

sep_language [in CFG.Separate]

sep_der_equiv [in CFG.Separate]

sep_uniform [in CFG.Separate]

size_recursion [in CFG.Base]

sless_monotone [in CFG.Symbols]

slists_slist [in CFG.Lists]

slist_pred [in CFG.Lists]

slist_length [in CFG.Lists]

slist_subsumes [in CFG.Lists]

slist_split [in CFG.Lists]

slist_inv [in CFG.Lists]

slist_equiv_pred [in CFG.Lists]

slist_append [in CFG.Lists]

slist_trans [in CFG.Lists]

slist_id [in CFG.Lists]

slist_closure_equiv [in CFG.ElimE]

slist_closure [in CFG.ElimE]

snds_split [in CFG.Lists]

step_dom [in CFG.Binarize]

step_der_equiv [in CFG.Binarize]

step_or [in CFG.Binarize]

step_dom [in CFG.Separate]

step_der_equiv [in CFG.Separate]

substG_der_equiv [in CFG.Separate]

substG_dom [in CFG.Inlining]

substG_inG [in CFG.Inlining]

substG_undo [in CFG.Inlining]

substG_skip [in CFG.Inlining]

substG_skipRule [in CFG.Inlining]

substG_split [in CFG.Inlining]

substG_preservesLength [in CFG.Chomsky]

substL_der [in CFG.Inlining]

substL_undo [in CFG.Lists]

substL_length_unit [in CFG.Lists]

substL_skip [in CFG.Lists]

substL_split [in CFG.Lists]

symbs_der [in CFG.Derivation]

symbs_subset [in CFG.Symbols]

symbs_inv [in CFG.Symbols]

symbs_dom [in CFG.Symbols]

## T

terminal_split [in CFG.Derivation]## U

undup_idempotent [in CFG.Base]undup_id [in CFG.Base]

undup_equi [in CFG.Base]

undup_incl [in CFG.Base]

undup_id_equi [in CFG.Base]

unitfree_elimU [in CFG.ElimU]

unitfree_elimU' [in CFG.ElimU]

unit_language [in CFG.ElimU]

# Constructor Index

## D

derIRefl [in CFG.Derivation]derIRule [in CFG.Derivation]

derITrans [in CFG.Derivation]

derTRefl [in CFG.Derivation]

derTRule [in CFG.Derivation]

derTTrans [in CFG.Derivation]

dupfreeC [in CFG.Base]

dupfreeN [in CFG.Base]

## F

fCons [in CFG.Derivation]fRefl [in CFG.Derivation]

fRule [in CFG.Derivation]

## G

gDer [in CFG.Derivation]## I

inN [in CFG.Inlining]inR [in CFG.Inlining]

## N

Null [in CFG.ElimE]## R

R [in CFG.Definitions]rDer [in CFG.Derivation]

replN [in CFG.Derivation]

## S

sDer [in CFG.Derivation]subcons [in CFG.Lists]

subconsp [in CFG.Lists]

subnil [in CFG.Lists]

## T

T [in CFG.Definitions]TProd [in CFG.Dec_Empty]

Ts [in CFG.Definitions]

## V

V [in CFG.Definitions]vDer [in CFG.Derivation]

VProd [in CFG.Dec_Empty]

Vs [in CFG.Definitions]

# Inductive Index

## D

der [in CFG.Derivation]derf [in CFG.Derivation]

derI [in CFG.Derivation]

derL [in CFG.Derivation]

derT [in CFG.Derivation]

dupfree [in CFG.Base]

## I

inlinable [in CFG.Inlining]## N

nullable [in CFG.ElimE]## P

productive [in CFG.Dec_Empty]## R

rule [in CFG.Definitions]## S

slist [in CFG.Lists]symbol [in CFG.Definitions]

## T

ter [in CFG.Definitions]## V

var [in CFG.Definitions]# Instance Index

## A

and_dec [in CFG.Base]app_equi_proper [in CFG.Base]

app_incl_proper [in CFG.Base]

## B

bool_eq_dec [in CFG.Base]## C

card_equi_proper [in CFG.Base]cons_equi_proper [in CFG.Base]

cons_incl_proper [in CFG.Base]

## D

dec_charfree [in CFG.Separate]der_dec [in CFG.Dec_Word]

## E

equi_Equivalence [in CFG.Base]eq_dec_prod [in CFG.Lists]

exists_phrase_dec [in CFG.Definitions]

exists_rule_dec [in CFG.Definitions]

exists_dec [in CFG.Dec_Empty]

## F

False_dec [in CFG.Base]filter_rule_dec [in CFG.Definitions]

filter_prod_dec [in CFG.Lists]

## I

iff_dec [in CFG.Base]impl_dec [in CFG.Base]

incl_equi_proper [in CFG.Base]

incl_preorder [in CFG.Base]

in_equi_proper [in CFG.Base]

in_incl_proper [in CFG.Base]

## L

lang_dec [in CFG.Dec_Word]list_exists_dec [in CFG.Base]

list_forall_dec [in CFG.Base]

list_in_dec [in CFG.Base]

list_eq_dec [in CFG.Base]

## N

nat_le_dec [in CFG.Base]nat_eq_dec [in CFG.Base]

not_dec [in CFG.Base]

nullable_dec [in CFG.ElimE]

## O

or_dec [in CFG.Base]## P

phrase_char_dec [in CFG.Definitions]phrase_var_dec [in CFG.Definitions]

productive_dec [in CFG.Dec_Empty]

## R

rule_eq_dec [in CFG.Definitions]## S

sless_dec [in CFG.Symbols]splitList_dec [in CFG.Lists]

step_dec [in CFG.ElimU]

step_dec' [in CFG.ElimU]

step_dec [in CFG.Dec_Empty]

step_dec [in CFG.Dec_Word]

step_dec' [in CFG.Dec_Word]

symbol_ter_dec [in CFG.Definitions]

symbol_eq_dec [in CFG.Definitions]

## T

True_dec [in CFG.Base]## V

var_eq_dec [in CFG.Definitions]# Section Index

## C

Cardinality [in CFG.Base]## D

Dec_Emptys [in CFG.Dec_Empty]Dec_Word [in CFG.Dec_Word]

DelE [in CFG.ElimE]

Dupfree [in CFG.Base]

## E

EClosure [in CFG.ElimE]Equi [in CFG.Base]

## F

FCI.FCI [in CFG.Base]FilterComm [in CFG.Base]

FilterLemmas [in CFG.Base]

FilterLemmas_pq [in CFG.Base]

## I

Inclusion [in CFG.Base]Iteration [in CFG.Base]

## M

Membership [in CFG.Base]## P

PowerRep [in CFG.Base]## R

Removal [in CFG.Base]## U

Undup [in CFG.Base]UnitRules [in CFG.ElimU]

# Definition Index

## B

bin [in CFG.Binarize]binary [in CFG.Binarize]

## C

card [in CFG.Base]charfree [in CFG.Separate]

chomsky [in CFG.Chomsky]

closure [in CFG.ElimE]

concat [in CFG.Lists]

count_bin [in CFG.Binarize]

count_sep [in CFG.Separate]

count_chars [in CFG.Separate]

## D

dec [in CFG.Base]decision [in CFG.Base]

delE [in CFG.ElimE]

disjoint [in CFG.Base]

dom [in CFG.Symbols]

domV [in CFG.ElimU]

dupfree_inv [in CFG.Base]

DW [in CFG.Dec_Word]

## E

eclosed [in CFG.ElimE]eclosure [in CFG.ElimE]

efree [in CFG.ElimE]

elimE [in CFG.ElimE]

elimU [in CFG.ElimU]

equi [in CFG.Base]

## F

FCI.C [in CFG.Base]FCI.F [in CFG.Base]

filter [in CFG.Base]

FP [in CFG.Base]

fresh [in CFG.Symbols]

fsts [in CFG.Lists]

fsts_comb [in CFG.Dec_Word]

## G

getNat [in CFG.Symbols]grammar [in CFG.Definitions]

## I

inclp [in CFG.Base]inlL [in CFG.Inlining]

it [in CFG.Base]

item [in CFG.Dec_Word]

items [in CFG.Dec_Word]

## L

language [in CFG.Derivation]## M

maxSymb [in CFG.Symbols]maxSymbRule [in CFG.Symbols]

## N

N [in CFG.ElimU]normalize [in CFG.Chomsky]

## P

P [in CFG.Dec_Empty]phrase [in CFG.Definitions]

power [in CFG.Base]

product [in CFG.Lists]

## R

ran [in CFG.Symbols]rem [in CFG.Base]

rep [in CFG.Base]

rules [in CFG.ElimU]

## S

segment [in CFG.Lists]segms [in CFG.Lists]

sep [in CFG.Separate]

sless [in CFG.Symbols]

sless' [in CFG.Symbols]

slists [in CFG.Lists]

snds [in CFG.Lists]

step [in CFG.Binarize]

step [in CFG.Separate]

step [in CFG.ElimU]

step [in CFG.Dec_Empty]

step [in CFG.Dec_Word]

step' [in CFG.Binarize]

substG [in CFG.Inlining]

substL [in CFG.Lists]

symbs [in CFG.Symbols]

## T

terminal [in CFG.Derivation]## U

undup [in CFG.Base]uniform [in CFG.Separate]

unitfree [in CFG.ElimU]

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 | (489 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 | (5 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 | (27 entries) |

Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |

Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (263 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 | (29 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 | (14 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 | (48 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 | (18 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 | (71 entries) |