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 (2173 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 (67 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 (7 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (90 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 (48 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 (882 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 (144 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 (44 entries)
Projection 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 (127 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 (155 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 (57 entries)
Abbreviation 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 (110 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 (408 entries)
Record 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 (34 entries)

Global Index

A

AA [definition, in RelationAlgebra.level]
ab_to_hoare [lemma, in RelationAlgebra.kat_tac]
ab'_to_hoare [lemma, in RelationAlgebra.kat_tac]
aff [definition, in RelationAlgebra.paterson]
aff [constructor, in RelationAlgebra.imp]
aff_ite [lemma, in RelationAlgebra.imp]
aff_comm [lemma, in RelationAlgebra.imp]
aff_idem [lemma, in RelationAlgebra.imp]
aff_stack [lemma, in RelationAlgebra.imp]
AL [definition, in RelationAlgebra.level]
andb_dot [lemma, in RelationAlgebra.boolean]
antisym [lemma, in RelationAlgebra.lattice]
antisymmetric [projection, in RelationAlgebra.relalg]
antisymmetric [constructor, in RelationAlgebra.relalg]
antisymmetric_cnv [instance, in RelationAlgebra.relalg]
apply [definition, in RelationAlgebra.common]
assert_false [definition, in RelationAlgebra.common]
Atom [abbreviation, in RelationAlgebra.ugregex]
Atom [abbreviation, in RelationAlgebra.kat_completeness]
Atom [abbreviation, in RelationAlgebra.kat_untyping]
Atom [abbreviation, in RelationAlgebra.atoms]
atom [definition, in RelationAlgebra.atoms]
Atom [abbreviation, in RelationAlgebra.gregex]
Atom [abbreviation, in RelationAlgebra.glang]
Atom [abbreviation, in RelationAlgebra.ugregex_dec]
atoms [library]
atom_to_word [definition, in RelationAlgebra.kat_completeness]
atom_lattice_atom [lemma, in RelationAlgebra.relalg]
atom_points [lemma, in RelationAlgebra.relalg]
atom_mono [lemma, in RelationAlgebra.relalg]
atom_transitive [instance, in RelationAlgebra.relalg]
atom_of_points [lemma, in RelationAlgebra.relalg]
atom_of_points_aux [lemma, in RelationAlgebra.relalg]
atom_cnv [instance, in RelationAlgebra.relalg]
atom_univalent [instance, in RelationAlgebra.relalg]
atom_injective [instance, in RelationAlgebra.relalg]
atom_nonempty [projection, in RelationAlgebra.relalg]
atom_props.n [variable, in RelationAlgebra.atoms]
atom_props [section, in RelationAlgebra.atoms]
atom_xI [lemma, in RelationAlgebra.atoms]
atom_xO [lemma, in RelationAlgebra.atoms]
atom_single_atom [lemma, in RelationAlgebra.traces]
a_top_a [lemma, in RelationAlgebra.relalg]
a_top_a_aux [lemma, in RelationAlgebra.relalg]
a_top_a' [projection, in RelationAlgebra.relalg]
a'_top_a [projection, in RelationAlgebra.relalg]


B

BDL [definition, in RelationAlgebra.level]
below_I [definition, in RelationAlgebra.ugregex_dec]
BKA [definition, in RelationAlgebra.level]
bka_to_kat.laws [lemma, in RelationAlgebra.kat_tac]
bka_to_kat.ops [definition, in RelationAlgebra.kat_tac]
bka_to_kat [module, in RelationAlgebra.kat_tac]
BL [definition, in RelationAlgebra.level]
blk_mx_0 [lemma, in RelationAlgebra.matrix_ext]
blk_mx' [lemma, in RelationAlgebra.matrix]
blk_mx_weq [instance, in RelationAlgebra.matrix]
blk_mx_leq [instance, in RelationAlgebra.matrix]
blk_mx [definition, in RelationAlgebra.matrix]
bmx [abbreviation, in RelationAlgebra.bmx]
bmx [library]
bmx_str_clot [lemma, in RelationAlgebra.bmx]
bmx_str_str [lemma, in RelationAlgebra.bmx]
bmx_top_1 [lemma, in RelationAlgebra.bmx]
bmx_str [definition, in RelationAlgebra.bmx]
boolean [library]
bool_of_sumbool [definition, in RelationAlgebra.common]
bool_compare_spec [lemma, in RelationAlgebra.comparisons]
bool_compare [definition, in RelationAlgebra.comparisons]
bool_laws [instance, in RelationAlgebra.boolean]
bool_ops [definition, in RelationAlgebra.boolean]
bool_tt [constructor, in RelationAlgebra.boolean]
bool_unit [inductive, in RelationAlgebra.boolean]
bool_lattice_laws [instance, in RelationAlgebra.boolean]
bool_lattice_ops [definition, in RelationAlgebra.boolean]
bool' [abbreviation, in RelationAlgebra.boolean]
bot [projection, in RelationAlgebra.lattice]
BOT [definition, in RelationAlgebra.level]
bpqc_to_hoare [lemma, in RelationAlgebra.kat_tac]
bsl [section, in RelationAlgebra.matrix]
BSL [definition, in RelationAlgebra.level]
bstep [definition, in RelationAlgebra.paterson]
bstep [definition, in RelationAlgebra.imp]
bstep_eq [lemma, in RelationAlgebra.imp]
bstep' [inductive, in RelationAlgebra.imp]
bsub_mx [definition, in RelationAlgebra.matrix]


C

cap [projection, in RelationAlgebra.lattice]
CAP [definition, in RelationAlgebra.level]
capA [lemma, in RelationAlgebra.lattice]
capbx [lemma, in RelationAlgebra.lattice]
capC [lemma, in RelationAlgebra.lattice]
capcup [lemma, in RelationAlgebra.lattice]
capcup_ [lemma, in RelationAlgebra.lattice]
capcup' [lemma, in RelationAlgebra.lattice]
capdotx [projection, in RelationAlgebra.monoid]
capI [lemma, in RelationAlgebra.lattice]
capneg [projection, in RelationAlgebra.lattice]
capsupx [lemma, in RelationAlgebra.sups]
captx [lemma, in RelationAlgebra.lattice]
capxb [lemma, in RelationAlgebra.lattice]
capxdot [lemma, in RelationAlgebra.monoid]
capxsup [lemma, in RelationAlgebra.sups]
capxt [lemma, in RelationAlgebra.lattice]
cap_weq [instance, in RelationAlgebra.lattice]
cap_leq [instance, in RelationAlgebra.lattice]
cap_spec [projection, in RelationAlgebra.lattice]
cap_var_atom [lemma, in RelationAlgebra.atoms]
cap' [definition, in RelationAlgebra.normalisation]
cap'cap [lemma, in RelationAlgebra.normalisation]
cap'_level [lemma, in RelationAlgebra.normalisation]
car [projection, in RelationAlgebra.lattice]
carr [projection, in RelationAlgebra.comparisons]
cast [definition, in RelationAlgebra.syntax]
cast_eq [lemma, in RelationAlgebra.syntax]
catch_leq [lemma, in RelationAlgebra.monoid]
catch_weq [lemma, in RelationAlgebra.monoid]
catch_ka_weq [lemma, in RelationAlgebra.kat_tac]
catch_kat_weq [lemma, in RelationAlgebra.kat_tac]
cbsl [section, in RelationAlgebra.matrix]
CKA [definition, in RelationAlgebra.level]
clean [definition, in RelationAlgebra.kat_completeness]
clean [definition, in RelationAlgebra.untyping]
clean [section, in RelationAlgebra.untyping]
clean_hat [lemma, in RelationAlgebra.kat_completeness]
clean_str' [lemma, in RelationAlgebra.kat_completeness]
clean_inner_dot [lemma, in RelationAlgebra.kat_completeness]
clean_one' [lemma, in RelationAlgebra.kat_completeness]
clean_dot' [lemma, in RelationAlgebra.kat_completeness]
clean_elem_var [lemma, in RelationAlgebra.kat_completeness]
clean_pred [lemma, in RelationAlgebra.kat_completeness]
clean_map [lemma, in RelationAlgebra.kat_completeness]
clean_sup [lemma, in RelationAlgebra.kat_completeness]
clean_single [lemma, in RelationAlgebra.kat_completeness]
clean_cup [lemma, in RelationAlgebra.kat_completeness]
clean_bot [lemma, in RelationAlgebra.kat_completeness]
clean_erase [lemma, in RelationAlgebra.untyping]
clean_factorise_leq [lemma, in RelationAlgebra.untyping]
clean_factorise_leq_weq [lemma, in RelationAlgebra.untyping]
clean_idem [lemma, in RelationAlgebra.untyping]
clean_leq_0 [lemma, in RelationAlgebra.untyping]
clean_leq_weq_0 [lemma, in RelationAlgebra.untyping]
clean_weq [lemma, in RelationAlgebra.untyping]
clean_0_level [lemma, in RelationAlgebra.untyping]
clean_level [lemma, in RelationAlgebra.untyping]
clean_spec [lemma, in RelationAlgebra.untyping]
clean.s [variable, in RelationAlgebra.untyping]
clean.t [variable, in RelationAlgebra.untyping]
clean1 [definition, in RelationAlgebra.kat_completeness]
clot_snoc [lemma, in RelationAlgebra.bmx]
clot_app [lemma, in RelationAlgebra.bmx]
clot_cons [constructor, in RelationAlgebra.bmx]
clot_nil [constructor, in RelationAlgebra.bmx]
cmp [projection, in RelationAlgebra.comparisons]
cmpType [record, in RelationAlgebra.comparisons]
cmp_letter [definition, in RelationAlgebra.kat_completeness]
cmp_list [definition, in RelationAlgebra.comparisons]
cmp_sum [definition, in RelationAlgebra.comparisons]
cmp_pair [definition, in RelationAlgebra.comparisons]
cmp_bool [definition, in RelationAlgebra.comparisons]
cmp_nat [definition, in RelationAlgebra.comparisons]
cmp_eq_rect_eq [lemma, in RelationAlgebra.comparisons]
cmp_eq_dep_eq [lemma, in RelationAlgebra.comparisons]
cmp_dec [lemma, in RelationAlgebra.comparisons]
cmp_refl [lemma, in RelationAlgebra.comparisons]
cmp_eq [lemma, in RelationAlgebra.comparisons]
cmp_id [definition, in RelationAlgebra.comparisons]
cmp_spec [lemma, in RelationAlgebra.comparisons]
cmp_ord [definition, in RelationAlgebra.ordinal]
cmp_expr [definition, in RelationAlgebra.syntax]
cmp_expr [definition, in RelationAlgebra.lsyntax]
cmp_pos [definition, in RelationAlgebra.positives]
cnv [projection, in RelationAlgebra.monoid]
CNV [definition, in RelationAlgebra.level]
cnvcap [lemma, in RelationAlgebra.monoid]
cnvdot [lemma, in RelationAlgebra.monoid]
cnvdot_ [projection, in RelationAlgebra.monoid]
cnvitr [lemma, in RelationAlgebra.kleene]
cnvldv [lemma, in RelationAlgebra.monoid]
cnvneg [lemma, in RelationAlgebra.monoid]
cnvpls [lemma, in RelationAlgebra.monoid]
cnvrdv [lemma, in RelationAlgebra.monoid]
cnvstr [lemma, in RelationAlgebra.kleene]
cnvstr_ [lemma, in RelationAlgebra.monoid]
cnvsum [lemma, in RelationAlgebra.sums]
cnvtop [lemma, in RelationAlgebra.monoid]
cnv_ext [lemma, in RelationAlgebra.monoid]
cnv_weq_iff' [lemma, in RelationAlgebra.monoid]
cnv_weq_iff [lemma, in RelationAlgebra.monoid]
cnv_leq_iff' [lemma, in RelationAlgebra.monoid]
cnv_leq_iff [lemma, in RelationAlgebra.monoid]
cnv_weq [instance, in RelationAlgebra.monoid]
cnv_ext_ [projection, in RelationAlgebra.monoid]
cnv_leq [projection, in RelationAlgebra.monoid]
cnv_invol [projection, in RelationAlgebra.monoid]
cnv' [definition, in RelationAlgebra.normalisation]
cnv'cnv [lemma, in RelationAlgebra.normalisation]
cnv'_level [lemma, in RelationAlgebra.normalisation]
cnv0 [lemma, in RelationAlgebra.monoid]
cnv1 [lemma, in RelationAlgebra.monoid]
col_mx_cup [lemma, in RelationAlgebra.matrix]
col_mx_leq_iff [lemma, in RelationAlgebra.matrix]
col_mx_weq [instance, in RelationAlgebra.matrix]
col_mx_leq [instance, in RelationAlgebra.matrix]
col_mx [definition, in RelationAlgebra.matrix]
common [library]
comm4 [lemma, in RelationAlgebra.lattice]
compare_letter_spec [lemma, in RelationAlgebra.kat_completeness]
compare_letter [definition, in RelationAlgebra.kat_completeness]
compare_lex_eq [lemma, in RelationAlgebra.comparisons]
compare_gt [constructor, in RelationAlgebra.comparisons]
compare_lt [constructor, in RelationAlgebra.comparisons]
compare_eq [constructor, in RelationAlgebra.comparisons]
compare_spec [inductive, in RelationAlgebra.comparisons]
comparisons [library]
compiler_opts [library]
cp_c [lemma, in RelationAlgebra.kat_tac]
cup [projection, in RelationAlgebra.lattice]
CUP [definition, in RelationAlgebra.level]
cupA [lemma, in RelationAlgebra.lattice]
cupbx [lemma, in RelationAlgebra.lattice]
cupC [lemma, in RelationAlgebra.lattice]
cupcap [lemma, in RelationAlgebra.lattice]
cupcap_ [projection, in RelationAlgebra.lattice]
cupcap' [lemma, in RelationAlgebra.lattice]
cupI [lemma, in RelationAlgebra.lattice]
cupneg [projection, in RelationAlgebra.lattice]
cuptx [lemma, in RelationAlgebra.lattice]
cupxb [lemma, in RelationAlgebra.lattice]
cupxt [lemma, in RelationAlgebra.lattice]
cup_weq [instance, in RelationAlgebra.lattice]
cup_leq [instance, in RelationAlgebra.lattice]
cup_spec [projection, in RelationAlgebra.lattice]
cup_var_atom [lemma, in RelationAlgebra.atoms]


D

d [section, in RelationAlgebra.matrix]
DAL [definition, in RelationAlgebra.level]
dead_code' [lemma, in RelationAlgebra.imp]
dead_code [lemma, in RelationAlgebra.imp]
decomp_expr [lemma, in RelationAlgebra.atoms]
decomp_top [lemma, in RelationAlgebra.atoms]
dedekind [lemma, in RelationAlgebra.relalg]
del [abbreviation, in RelationAlgebra.paterson]
denum [library]
deriv [definition, in RelationAlgebra.ugregex]
deriv [definition, in RelationAlgebra.regex]
derivs [definition, in RelationAlgebra.regex]
derivs_weq [instance, in RelationAlgebra.regex]
derivs_leq [instance, in RelationAlgebra.regex]
deriv_traces [lemma, in RelationAlgebra.ugregex]
deriv_sup [lemma, in RelationAlgebra.ugregex]
deriv_eval [lemma, in RelationAlgebra.nfa]
deriv_sup [lemma, in RelationAlgebra.regex]
deriv_01 [lemma, in RelationAlgebra.regex]
deriv_weq [instance, in RelationAlgebra.regex]
deriv_leq [instance, in RelationAlgebra.regex]
deriv_cancel [lemma, in RelationAlgebra.regex]
deriv_01_mx [lemma, in RelationAlgebra.rmx]
deriv_mx_str_strict [lemma, in RelationAlgebra.rmx]
deriv_mx_weq [instance, in RelationAlgebra.rmx]
deriv_mx_dot [lemma, in RelationAlgebra.rmx]
deriv_mx_pls [lemma, in RelationAlgebra.rmx]
deriv_mx [abbreviation, in RelationAlgebra.rmx]
deriv_out [lemma, in RelationAlgebra.ugregex_dec]
deriv_vars [lemma, in RelationAlgebra.ugregex_dec]
deriv_eq [lemma, in RelationAlgebra.ugregex_dec]
deriv'_vars [lemma, in RelationAlgebra.ugregex_dec]
deriv'_eq [lemma, in RelationAlgebra.ugregex_dec]
det [definition, in RelationAlgebra.ka_completeness]
det [section, in RelationAlgebra.ka_completeness]
det_Xv [lemma, in RelationAlgebra.ka_completeness]
det_MX [lemma, in RelationAlgebra.ka_completeness]
det_uX [lemma, in RelationAlgebra.ka_completeness]
det.Hnfa [variable, in RelationAlgebra.ka_completeness]
det.M_ [variable, in RelationAlgebra.ka_completeness]
det.nfa [variable, in RelationAlgebra.ka_completeness]
det.T_ [variable, in RelationAlgebra.ka_completeness]
det.vars' [variable, in RelationAlgebra.ka_completeness]
det.X [variable, in RelationAlgebra.ka_completeness]
dfa [definition, in RelationAlgebra.ka_completeness]
dfa [module, in RelationAlgebra.nfa]
dfa [library]
dfa_complete_leq [lemma, in RelationAlgebra.ka_completeness]
dfa.eval_lang [lemma, in RelationAlgebra.nfa]
dfa.is_nfa_nfa [lemma, in RelationAlgebra.nfa]
dfa.nfa_lang [lemma, in RelationAlgebra.nfa]
dfa.to_nfa [definition, in RelationAlgebra.nfa]
_ @ _ [notation, in RelationAlgebra.nfa]
diff [definition, in RelationAlgebra.dfa]
diff [section, in RelationAlgebra.dfa]
diff_spec [lemma, in RelationAlgebra.dfa]
diff.A [variable, in RelationAlgebra.dfa]
diff.B [variable, in RelationAlgebra.dfa]
dirac [definition, in RelationAlgebra.kat_completeness]
dirac_refl [lemma, in RelationAlgebra.kat_completeness]
disjoint_vect_ext [lemma, in RelationAlgebra.relalg]
disjoint_vect_iff' [lemma, in RelationAlgebra.relalg]
disjoint_vect_iff [lemma, in RelationAlgebra.relalg]
disjoint_id [lemma, in RelationAlgebra.relalg]
DIV [definition, in RelationAlgebra.level]
DL [definition, in RelationAlgebra.level]
dont_read [definition, in RelationAlgebra.paterson]
dot [projection, in RelationAlgebra.monoid]
dotA [projection, in RelationAlgebra.monoid]
dotcapx [lemma, in RelationAlgebra.monoid]
dotplsx [lemma, in RelationAlgebra.monoid]
dotplsx_ [projection, in RelationAlgebra.monoid]
dotsumx [lemma, in RelationAlgebra.sums]
dottx [lemma, in RelationAlgebra.relalg]
dotxcap [lemma, in RelationAlgebra.monoid]
dotxpls [lemma, in RelationAlgebra.monoid]
dotxpls_ [projection, in RelationAlgebra.monoid]
dotxsum [lemma, in RelationAlgebra.sums]
dotxt [lemma, in RelationAlgebra.relalg]
dotx0 [lemma, in RelationAlgebra.monoid]
dotx0_ [projection, in RelationAlgebra.monoid]
dotx1 [lemma, in RelationAlgebra.monoid]
dotx1_ [projection, in RelationAlgebra.monoid]
dot_weq [instance, in RelationAlgebra.monoid]
dot_leq [instance, in RelationAlgebra.monoid]
dot_leq_ [projection, in RelationAlgebra.monoid]
dot_cap_injective [lemma, in RelationAlgebra.relalg]
dot_neg_point [lemma, in RelationAlgebra.relalg]
dot_neg_surj [lemma, in RelationAlgebra.relalg]
dot_neg_inj [lemma, in RelationAlgebra.relalg]
dot_univalent_cap [lemma, in RelationAlgebra.relalg]
dot_mono [lemma, in RelationAlgebra.relalg]
dot_ofboolx [lemma, in RelationAlgebra.boolean]
dot_l_weq [lemma, in RelationAlgebra.normalisation]
dot_r_level [lemma, in RelationAlgebra.normalisation]
dot_l_level [lemma, in RelationAlgebra.normalisation]
dot_r [definition, in RelationAlgebra.normalisation]
dot_l [definition, in RelationAlgebra.normalisation]
dot' [definition, in RelationAlgebra.normalisation]
dot'dot [lemma, in RelationAlgebra.normalisation]
dot'_level [lemma, in RelationAlgebra.normalisation]
dot0x [lemma, in RelationAlgebra.monoid]
dot0x_ [projection, in RelationAlgebra.monoid]
dot1x [projection, in RelationAlgebra.monoid]
double [definition, in RelationAlgebra.common]
dset [definition, in RelationAlgebra.rel]
dual [definition, in RelationAlgebra.lattice]
dual [definition, in RelationAlgebra.monoid]
dual [definition, in RelationAlgebra.kat]
dual [definition, in RelationAlgebra.level]
dualize [lemma, in RelationAlgebra.lattice]
dualize [lemma, in RelationAlgebra.monoid]
dualize [lemma, in RelationAlgebra.kat]
dual_laws [lemma, in RelationAlgebra.lattice]
dual_laws [lemma, in RelationAlgebra.monoid]
dual_laws [lemma, in RelationAlgebra.kat]


E

E [section, in RelationAlgebra.ka_completeness]
e [section, in RelationAlgebra.untyping]
e [section, in RelationAlgebra.positives]
elang [abbreviation, in RelationAlgebra.regex]
elim_hoare_hypotheses_leq [lemma, in RelationAlgebra.kat_tac]
elim_hoare_hypotheses_weq [lemma, in RelationAlgebra.kat_tac]
empty [definition, in RelationAlgebra.dfa]
empty_atom_dot [lemma, in RelationAlgebra.kat_completeness]
empty_atom_cap [lemma, in RelationAlgebra.atoms]
empty_dec [lemma, in RelationAlgebra.dfa]
empty_lang2 [lemma, in RelationAlgebra.dfa]
empty_lang1 [lemma, in RelationAlgebra.dfa]
empty_dec.i [variable, in RelationAlgebra.dfa]
empty_dec.A [variable, in RelationAlgebra.dfa]
empty_dec [section, in RelationAlgebra.dfa]
eps [abbreviation, in RelationAlgebra.regex]
epsilon [definition, in RelationAlgebra.ugregex]
epsilon [definition, in RelationAlgebra.regex]
epsilon_iff_lang_nil [lemma, in RelationAlgebra.ugregex]
epsilon_pred [definition, in RelationAlgebra.ugregex]
epsilon_eval [lemma, in RelationAlgebra.nfa]
epsilon_iff_lang_nil [lemma, in RelationAlgebra.regex]
epsilon_iff_reflexive_eps [lemma, in RelationAlgebra.regex]
epsilon_reflexive [lemma, in RelationAlgebra.regex]
epsilon_deriv_pure [lemma, in RelationAlgebra.regex]
epsilon_pure [lemma, in RelationAlgebra.regex]
epsilon_weq [instance, in RelationAlgebra.regex]
epsilon_leq [instance, in RelationAlgebra.regex]
epsilon_eval [lemma, in RelationAlgebra.regex]
epsilon_deriv_pure_mx [lemma, in RelationAlgebra.rmx]
epsilon_mx_pure [lemma, in RelationAlgebra.rmx]
epsilon_mx_str [lemma, in RelationAlgebra.rmx]
epsilon_mx_weq [instance, in RelationAlgebra.rmx]
epsilon_mx_dot [lemma, in RelationAlgebra.rmx]
epsilon_sup [lemma, in RelationAlgebra.rmx]
epsilon_mx_pls [lemma, in RelationAlgebra.rmx]
epsilon_mx [definition, in RelationAlgebra.rmx]
epsilon' [definition, in RelationAlgebra.ugregex_dec]
epsilon'_eq [lemma, in RelationAlgebra.ugregex_dec]
eqb [definition, in RelationAlgebra.paterson]
eqb [projection, in RelationAlgebra.comparisons]
eqb_false [lemma, in RelationAlgebra.paterson]
eqb_spec [lemma, in RelationAlgebra.paterson]
eqb_list_spec [lemma, in RelationAlgebra.comparisons]
eqb_list [definition, in RelationAlgebra.comparisons]
eqb_sum_spec [lemma, in RelationAlgebra.comparisons]
eqb_sum [definition, in RelationAlgebra.comparisons]
eqb_pair_spec [lemma, in RelationAlgebra.comparisons]
eqb_pair [definition, in RelationAlgebra.comparisons]
eqb_bool_spec [lemma, in RelationAlgebra.comparisons]
eqb_bool [definition, in RelationAlgebra.comparisons]
eqb_nat_spec [lemma, in RelationAlgebra.comparisons]
eqb_nat [definition, in RelationAlgebra.comparisons]
eqb_sym [lemma, in RelationAlgebra.comparisons]
eqb_refl [lemma, in RelationAlgebra.comparisons]
eqb_eq [lemma, in RelationAlgebra.comparisons]
eqb_spec [lemma, in RelationAlgebra.comparisons]
eqb_of_compare_spec [lemma, in RelationAlgebra.comparisons]
eqb_of_compare [definition, in RelationAlgebra.comparisons]
eqb_ord_rrshift [lemma, in RelationAlgebra.ordinal]
eqb_ord_rlshift [lemma, in RelationAlgebra.ordinal]
eqb_ord_lrshift [lemma, in RelationAlgebra.ordinal]
eqb_ord_spec [lemma, in RelationAlgebra.ordinal]
eqb_ord [definition, in RelationAlgebra.ordinal]
eqb_pos_spec [lemma, in RelationAlgebra.positives]
eqb_pos [definition, in RelationAlgebra.positives]
eqb_kat_correct [lemma, in RelationAlgebra.ugregex_dec]
eqb_kat [definition, in RelationAlgebra.ugregex_dec]
eq_app_dot [lemma, in RelationAlgebra.lang]
eq_bool_iff [lemma, in RelationAlgebra.common]
eq_9' [lemma, in RelationAlgebra.paterson]
eq_6' [lemma, in RelationAlgebra.paterson]
eq_9 [lemma, in RelationAlgebra.paterson]
eq_8 [lemma, in RelationAlgebra.paterson]
eq_7 [lemma, in RelationAlgebra.paterson]
eq_6 [lemma, in RelationAlgebra.paterson]
eq_ord [lemma, in RelationAlgebra.ordinal]
erase [definition, in RelationAlgebra.untyping]
erase_faithful_weq [lemma, in RelationAlgebra.untyping]
erase_faithful_leq [lemma, in RelationAlgebra.untyping]
erase_0 [lemma, in RelationAlgebra.untyping]
erase_faithful_leq_clean [lemma, in RelationAlgebra.untyping]
esubst [definition, in RelationAlgebra.imp]
euclid_unique [lemma, in RelationAlgebra.pair]
eval [definition, in RelationAlgebra.paterson]
eval [definition, in RelationAlgebra.kat_reification]
eval [definition, in RelationAlgebra.nfa]
eval [definition, in RelationAlgebra.syntax]
eval [definition, in RelationAlgebra.lsyntax]
eval [definition, in RelationAlgebra.gregex]
eval [inductive, in RelationAlgebra.untyping]
eval_update [lemma, in RelationAlgebra.paterson]
eval_atom [lemma, in RelationAlgebra.atoms]
eval_mem_cup [lemma, in RelationAlgebra.atoms]
eval_mem_cap [lemma, in RelationAlgebra.atoms]
eval_dfa [lemma, in RelationAlgebra.ka_completeness]
eval_det [lemma, in RelationAlgebra.ka_completeness]
eval_nfa [lemma, in RelationAlgebra.ka_completeness]
eval_lang [lemma, in RelationAlgebra.nfa]
eval_deriv [lemma, in RelationAlgebra.regex]
eval_var [lemma, in RelationAlgebra.lsyntax]
eval_inf [lemma, in RelationAlgebra.lsyntax]
eval_sup [lemma, in RelationAlgebra.lsyntax]
eval_erase [lemma, in RelationAlgebra.untyping]
eval_fun [lemma, in RelationAlgebra.untyping]
eval_types_r [lemma, in RelationAlgebra.untyping]
eval_types_l [lemma, in RelationAlgebra.untyping]
eval_types [lemma, in RelationAlgebra.untyping]
eval_var [lemma, in RelationAlgebra.untyping]
eval_str [lemma, in RelationAlgebra.untyping]
eval_itr [lemma, in RelationAlgebra.untyping]
eval_one [lemma, in RelationAlgebra.untyping]
eval_var' [lemma, in RelationAlgebra.untyping]
eval_str' [lemma, in RelationAlgebra.untyping]
eval_itr' [lemma, in RelationAlgebra.untyping]
eval_one' [lemma, in RelationAlgebra.untyping]
eval_cnv [lemma, in RelationAlgebra.untyping]
eval_dot [lemma, in RelationAlgebra.untyping]
eval_pls [lemma, in RelationAlgebra.untyping]
ev_var [constructor, in RelationAlgebra.untyping]
ev_cnv [constructor, in RelationAlgebra.untyping]
ev_str [constructor, in RelationAlgebra.untyping]
ev_itr [constructor, in RelationAlgebra.untyping]
ev_dot [constructor, in RelationAlgebra.untyping]
ev_pls [constructor, in RelationAlgebra.untyping]
ev_one [constructor, in RelationAlgebra.untyping]
expand [lemma, in RelationAlgebra.regex]
expand_pure [lemma, in RelationAlgebra.regex]
expand_simple [lemma, in RelationAlgebra.regex]
expand_01 [lemma, in RelationAlgebra.regex]
expand_simple_mx [lemma, in RelationAlgebra.rmx]
expand_01_mx [lemma, in RelationAlgebra.rmx]
expand' [lemma, in RelationAlgebra.regex]
expr [inductive, in RelationAlgebra.paterson]
expr [abbreviation, in RelationAlgebra.normalisation]
expr [abbreviation, in RelationAlgebra.syntax]
expr [inductive, in RelationAlgebra.syntax]
expr [inductive, in RelationAlgebra.lsyntax]
expr [abbreviation, in RelationAlgebra.untyping]
expr [abbreviation, in RelationAlgebra.untyping]
expr_lattice_laws [instance, in RelationAlgebra.paterson]
expr_lattice_ops [definition, in RelationAlgebra.paterson]
expr_leq_or_weq_correct [lemma, in RelationAlgebra.normalisation]
expr_leq_or_weq [definition, in RelationAlgebra.normalisation]
expr_leq_correct [lemma, in RelationAlgebra.normalisation]
expr_leq_correct_dep [lemma, in RelationAlgebra.normalisation]
expr_leq [definition, in RelationAlgebra.normalisation]
expr_compare_ [definition, in RelationAlgebra.syntax]
expr_compare_spec [lemma, in RelationAlgebra.syntax]
expr_compare_eq [lemma, in RelationAlgebra.syntax]
expr_compare_eq_dep [lemma, in RelationAlgebra.syntax]
expr_compare [definition, in RelationAlgebra.syntax]
expr_cmp.t [variable, in RelationAlgebra.syntax]
expr_cmp.s [variable, in RelationAlgebra.syntax]
expr_cmp [section, in RelationAlgebra.syntax]
expr_ [abbreviation, in RelationAlgebra.syntax]
expr_laws [instance, in RelationAlgebra.syntax]
expr_lattice_laws [instance, in RelationAlgebra.syntax]
expr_ops [definition, in RelationAlgebra.syntax]
expr_lattice_ops [definition, in RelationAlgebra.syntax]
expr_compare_spec [lemma, in RelationAlgebra.lsyntax]
expr_compare [definition, in RelationAlgebra.lsyntax]
expr_cmp [section, in RelationAlgebra.lsyntax]
expr_ [abbreviation, in RelationAlgebra.lsyntax]
expr_laws [instance, in RelationAlgebra.lsyntax]
expr_ops [definition, in RelationAlgebra.lsyntax]
expr_leq_weq_ind [lemma, in RelationAlgebra.untyping]
expr_ind_eval [lemma, in RelationAlgebra.untyping]
expr_ind [definition, in RelationAlgebra.untyping]
expr3 [abbreviation, in RelationAlgebra.kat_completeness]
ext_weq_4' [lemma, in RelationAlgebra.rewriting]
ext_weq_3' [lemma, in RelationAlgebra.rewriting]
ext_weq_2' [lemma, in RelationAlgebra.rewriting]
ext_leq_4' [lemma, in RelationAlgebra.rewriting]
ext_leq_3' [lemma, in RelationAlgebra.rewriting]
ext_leq_2' [lemma, in RelationAlgebra.rewriting]
ext_weq_4 [lemma, in RelationAlgebra.rewriting]
ext_weq_3 [lemma, in RelationAlgebra.rewriting]
ext_weq_2 [lemma, in RelationAlgebra.rewriting]
ext_leq_4 [lemma, in RelationAlgebra.rewriting]
ext_leq_3 [lemma, in RelationAlgebra.rewriting]
ext_leq_2 [lemma, in RelationAlgebra.rewriting]
e_top [constructor, in RelationAlgebra.paterson]
e_bot [constructor, in RelationAlgebra.paterson]
e_neg [constructor, in RelationAlgebra.paterson]
e_cup [constructor, in RelationAlgebra.paterson]
e_cap [constructor, in RelationAlgebra.paterson]
e_var [constructor, in RelationAlgebra.paterson]
e_var [definition, in RelationAlgebra.kat_reification]
e_inj [definition, in RelationAlgebra.kat_reification]
e_top' [definition, in RelationAlgebra.atoms]
e_weq_weaken [lemma, in RelationAlgebra.syntax]
e_leq_weaken [lemma, in RelationAlgebra.syntax]
e_weq [definition, in RelationAlgebra.syntax]
e_leq [definition, in RelationAlgebra.syntax]
e_level [definition, in RelationAlgebra.syntax]
e_var [constructor, in RelationAlgebra.syntax]
e_rdv [constructor, in RelationAlgebra.syntax]
e_ldv [constructor, in RelationAlgebra.syntax]
e_cnv [constructor, in RelationAlgebra.syntax]
e_str [constructor, in RelationAlgebra.syntax]
e_itr [constructor, in RelationAlgebra.syntax]
e_dot [constructor, in RelationAlgebra.syntax]
e_neg [constructor, in RelationAlgebra.syntax]
e_cap [constructor, in RelationAlgebra.syntax]
e_pls [constructor, in RelationAlgebra.syntax]
e_one [constructor, in RelationAlgebra.syntax]
e_top [constructor, in RelationAlgebra.syntax]
e_zer [constructor, in RelationAlgebra.syntax]
e_weq [definition, in RelationAlgebra.lsyntax]
e_leq [definition, in RelationAlgebra.lsyntax]
e_level [definition, in RelationAlgebra.lsyntax]
e_var [constructor, in RelationAlgebra.lsyntax]
e_neg [constructor, in RelationAlgebra.lsyntax]
e_cap [constructor, in RelationAlgebra.lsyntax]
e_cup [constructor, in RelationAlgebra.lsyntax]
e_top [constructor, in RelationAlgebra.lsyntax]
e_bot [constructor, in RelationAlgebra.lsyntax]
e_cnv_weq [lemma, in RelationAlgebra.untyping]
e_str_weq [lemma, in RelationAlgebra.untyping]
e_itr_weq [lemma, in RelationAlgebra.untyping]
e_dot_weq [lemma, in RelationAlgebra.untyping]
e_pls_weq [lemma, in RelationAlgebra.untyping]
e_cnv' [definition, in RelationAlgebra.untyping]
e_str' [definition, in RelationAlgebra.untyping]
e_itr' [definition, in RelationAlgebra.untyping]
e_dot' [definition, in RelationAlgebra.untyping]
e_pls' [definition, in RelationAlgebra.untyping]
E.A [variable, in RelationAlgebra.ka_completeness]
e.A [variable, in RelationAlgebra.positives]
E.B [variable, in RelationAlgebra.ka_completeness]
E.HAB [variable, in RelationAlgebra.ka_completeness]
E.Hvars [variable, in RelationAlgebra.ka_completeness]
e.l [section, in RelationAlgebra.untyping]
e.l.l [variable, in RelationAlgebra.untyping]
e.s [variable, in RelationAlgebra.untyping]
e.t [variable, in RelationAlgebra.untyping]


F

factors [library]
Fix [module, in RelationAlgebra.lset]
Fix.lset_ops [definition, in RelationAlgebra.lset]
flip [abbreviation, in RelationAlgebra.common]
fn_neg [projection, in RelationAlgebra.lattice]
fn_top [projection, in RelationAlgebra.lattice]
fn_bot [projection, in RelationAlgebra.lattice]
fn_cap [projection, in RelationAlgebra.lattice]
fn_cup [projection, in RelationAlgebra.lattice]
fn_weq [projection, in RelationAlgebra.lattice]
fn_leq [projection, in RelationAlgebra.lattice]
fn_rdv [projection, in RelationAlgebra.monoid]
fn_ldv [projection, in RelationAlgebra.monoid]
fn_cnv [projection, in RelationAlgebra.monoid]
fn_str [projection, in RelationAlgebra.monoid]
fn_itr [projection, in RelationAlgebra.monoid]
fn_one [projection, in RelationAlgebra.monoid]
fn_dot [projection, in RelationAlgebra.monoid]
fn_morphism [projection, in RelationAlgebra.monoid]
fold_loop [lemma, in RelationAlgebra.imp]
fold_loop_aux_spec [lemma, in RelationAlgebra.ugregex_dec]
free [definition, in RelationAlgebra.paterson]
free_subst [lemma, in RelationAlgebra.paterson]
frel [definition, in RelationAlgebra.rel]
frel_weq [instance, in RelationAlgebra.rel]
frel_comp [lemma, in RelationAlgebra.rel]
fresh [definition, in RelationAlgebra.imp]
from_above [lemma, in RelationAlgebra.lattice]
from_below [lemma, in RelationAlgebra.lattice]
fst [definition, in RelationAlgebra.kat_completeness]
Fun [abbreviation, in RelationAlgebra.powerfix]
functor [record, in RelationAlgebra.monoid]
f_sup_eq [lemma, in RelationAlgebra.sups]
f_sup_weq [lemma, in RelationAlgebra.sups]
f' [constructor, in RelationAlgebra.paterson]


G

G [abbreviation, in RelationAlgebra.kat_completeness]
G [module, in RelationAlgebra.kat_completeness]
gc [definition, in RelationAlgebra.paterson]
gc_correct [lemma, in RelationAlgebra.paterson]
gen_point [lemma, in RelationAlgebra.relalg]
gerase [definition, in RelationAlgebra.kat_untyping]
gerase_weq [lemma, in RelationAlgebra.kat_untyping]
get [definition, in RelationAlgebra.paterson]
get_mk_ord [lemma, in RelationAlgebra.denum]
get_ord [definition, in RelationAlgebra.denum]
get_mk_nat [lemma, in RelationAlgebra.denum]
get_nat [definition, in RelationAlgebra.denum]
get_mk_pair [lemma, in RelationAlgebra.denum]
get_pair [definition, in RelationAlgebra.denum]
get_mk_sum [lemma, in RelationAlgebra.denum]
get_sum [definition, in RelationAlgebra.denum]
get_set' [lemma, in RelationAlgebra.paterson]
get_set [lemma, in RelationAlgebra.paterson]
geval [definition, in RelationAlgebra.kat_completeness]
geval_lst [lemma, in RelationAlgebra.kat_completeness]
geval_fst [lemma, in RelationAlgebra.kat_completeness]
geval_dot [lemma, in RelationAlgebra.kat_completeness]
gl [definition, in RelationAlgebra.kat_completeness]
glang [abbreviation, in RelationAlgebra.kat_completeness]
glang [abbreviation, in RelationAlgebra.kat_untyping]
glang [abbreviation, in RelationAlgebra.gregex]
glang [library]
glang_kat_laws [instance, in RelationAlgebra.glang]
glang_kat_ops [definition, in RelationAlgebra.glang]
glang_inj [definition, in RelationAlgebra.glang]
gl_itr [lemma, in RelationAlgebra.kat_completeness]
gl_nildot [lemma, in RelationAlgebra.kat_completeness]
gl_dot [lemma, in RelationAlgebra.kat_completeness]
gl_single' [lemma, in RelationAlgebra.kat_completeness]
gl_atom [lemma, in RelationAlgebra.kat_completeness]
gl_sup [lemma, in RelationAlgebra.kat_completeness]
gl_cup [lemma, in RelationAlgebra.kat_completeness]
gl_bot [lemma, in RelationAlgebra.kat_completeness]
gl_weq [instance, in RelationAlgebra.kat_completeness]
gl_leq [instance, in RelationAlgebra.kat_completeness]
gregex [abbreviation, in RelationAlgebra.kat_completeness]
gregex [abbreviation, in RelationAlgebra.kat_untyping]
gregex [inductive, in RelationAlgebra.gregex]
gregex [library]
gregex_kat_laws [instance, in RelationAlgebra.gregex]
gregex_monoid_laws [instance, in RelationAlgebra.gregex]
gregex_lattice_laws [instance, in RelationAlgebra.gregex]
gregex_kat_ops [definition, in RelationAlgebra.gregex]
gregex_monoid_ops [definition, in RelationAlgebra.gregex]
gregex_lattice_ops [definition, in RelationAlgebra.gregex]
guard [inductive, in RelationAlgebra.kat_completeness]
guards [abbreviation, in RelationAlgebra.kat_completeness]
gword [abbreviation, in RelationAlgebra.kat_completeness]
gword_tapp [lemma, in RelationAlgebra.kat_completeness]
gword_to_word_cut [lemma, in RelationAlgebra.kat_completeness]
gword_to_word' [definition, in RelationAlgebra.kat_completeness]
gword_to_word [definition, in RelationAlgebra.kat_completeness]
G_hat [lemma, in RelationAlgebra.kat_completeness]
G_clean [lemma, in RelationAlgebra.kat_completeness]
g_str' [definition, in RelationAlgebra.kat_completeness]
g_inner_dot [definition, in RelationAlgebra.kat_completeness]
g_dot' [definition, in RelationAlgebra.kat_completeness]
g_dot1 [definition, in RelationAlgebra.kat_completeness]
g_var' [definition, in RelationAlgebra.kat_completeness]
g_one' [definition, in RelationAlgebra.kat_completeness]
g_prd' [definition, in RelationAlgebra.kat_completeness]
g_elem [constructor, in RelationAlgebra.kat_completeness]
g_pred [constructor, in RelationAlgebra.kat_completeness]
g_atom [abbreviation, in RelationAlgebra.kat_completeness]
g_atom [abbreviation, in RelationAlgebra.gregex]
g_weq [definition, in RelationAlgebra.gregex]
g_leq [definition, in RelationAlgebra.gregex]
g_str [definition, in RelationAlgebra.gregex]
g_one [definition, in RelationAlgebra.gregex]
g_itr [constructor, in RelationAlgebra.gregex]
g_dot [constructor, in RelationAlgebra.gregex]
g_pls [constructor, in RelationAlgebra.gregex]
g_var [constructor, in RelationAlgebra.gregex]
g_prd [constructor, in RelationAlgebra.gregex]
g_zer [constructor, in RelationAlgebra.gregex]
g' [constructor, in RelationAlgebra.paterson]


H

h [section, in RelationAlgebra.matrix_ext]
has_div [projection, in RelationAlgebra.level]
has_neg [projection, in RelationAlgebra.level]
has_cnv [projection, in RelationAlgebra.level]
has_str [projection, in RelationAlgebra.level]
has_top [projection, in RelationAlgebra.level]
has_cap [projection, in RelationAlgebra.level]
has_bot [projection, in RelationAlgebra.level]
has_cup [projection, in RelationAlgebra.level]
hat [definition, in RelationAlgebra.kat_completeness]
Hoare [abbreviation, in RelationAlgebra.imp]
Hoare_eq [lemma, in RelationAlgebra.imp]


I

i [section, in RelationAlgebra.rel]
I [abbreviation, in RelationAlgebra.syntax]
I [abbreviation, in RelationAlgebra.syntax]
I [abbreviation, in RelationAlgebra.gregex]
idem_atom_dot [lemma, in RelationAlgebra.kat_completeness]
idx [definition, in RelationAlgebra.kat_reification]
Idx [abbreviation, in RelationAlgebra.kat_reification]
imp [library]
impl [abbreviation, in RelationAlgebra.common]
inf [section, in RelationAlgebra.sups]
inf [abbreviation, in RelationAlgebra.sups]
inf_singleton [lemma, in RelationAlgebra.sups]
inf_spec [lemma, in RelationAlgebra.sups]
inf_leq [instance, in RelationAlgebra.sups]
inj [projection, in RelationAlgebra.kat]
injective [projection, in RelationAlgebra.relalg]
injective [constructor, in RelationAlgebra.relalg]
injective_cnv [instance, in RelationAlgebra.relalg]
inj_cup [lemma, in RelationAlgebra.kat]
inj_bot [lemma, in RelationAlgebra.kat]
inj_weq [instance, in RelationAlgebra.kat]
inj_leq [instance, in RelationAlgebra.kat]
inj_cap [projection, in RelationAlgebra.kat]
inj_top [projection, in RelationAlgebra.kat]
inj_sup [lemma, in RelationAlgebra.gregex]
inj_leq [definition, in RelationAlgebra.gregex]
inj_weq [definition, in RelationAlgebra.gregex]
inj_top [definition, in RelationAlgebra.gregex]
inj_cap [definition, in RelationAlgebra.gregex]
inj_bot [definition, in RelationAlgebra.gregex]
inj_cup [definition, in RelationAlgebra.gregex]
insert [definition, in RelationAlgebra.lset]
insert_app [lemma, in RelationAlgebra.lset]
insert_union [lemma, in RelationAlgebra.lset]
insert_pls_pls [lemma, in RelationAlgebra.normalisation]
insert_pls_level [lemma, in RelationAlgebra.normalisation]
insert_pls [definition, in RelationAlgebra.normalisation]
in_singleton [lemma, in RelationAlgebra.lset]
in_idx [lemma, in RelationAlgebra.kat_reification]
in_seq [lemma, in RelationAlgebra.ordinal]
in_sup [lemma, in RelationAlgebra.sups]
In_cons [lemma, in RelationAlgebra.ugregex_dec]
io [constructor, in RelationAlgebra.paterson]
irreflexive [projection, in RelationAlgebra.relalg]
irreflexive [constructor, in RelationAlgebra.relalg]
irreflexive_cnv [instance, in RelationAlgebra.relalg]
irreflexive' [lemma, in RelationAlgebra.relalg]
is_true_sumbool [lemma, in RelationAlgebra.common]
is_symmetric_neg1 [instance, in RelationAlgebra.relalg]
is_order_weq [instance, in RelationAlgebra.relalg]
is_preorder_weq [instance, in RelationAlgebra.relalg]
is_per_weq [instance, in RelationAlgebra.relalg]
is_mapping_weq [instance, in RelationAlgebra.relalg]
is_atom_weq [instance, in RelationAlgebra.relalg]
is_point_weq [instance, in RelationAlgebra.relalg]
is_nonempty_weq [instance, in RelationAlgebra.relalg]
is_vector_weq [instance, in RelationAlgebra.relalg]
is_total_weq [instance, in RelationAlgebra.relalg]
is_surjective_weq [instance, in RelationAlgebra.relalg]
is_injective_weq [instance, in RelationAlgebra.relalg]
is_univalent_weq [instance, in RelationAlgebra.relalg]
is_antisymmetric_weq [instance, in RelationAlgebra.relalg]
is_symmetric_weq [instance, in RelationAlgebra.relalg]
is_linear_weq [instance, in RelationAlgebra.relalg]
is_transitive_weq [instance, in RelationAlgebra.relalg]
is_irreflexive_weq [instance, in RelationAlgebra.relalg]
is_reflexive_weq [instance, in RelationAlgebra.relalg]
is_order [record, in RelationAlgebra.relalg]
is_preorder [record, in RelationAlgebra.relalg]
is_per [record, in RelationAlgebra.relalg]
is_mapping [record, in RelationAlgebra.relalg]
is_atom [record, in RelationAlgebra.relalg]
is_point [record, in RelationAlgebra.relalg]
is_vector [record, in RelationAlgebra.relalg]
is_vector [inductive, in RelationAlgebra.relalg]
is_total [record, in RelationAlgebra.relalg]
is_total [inductive, in RelationAlgebra.relalg]
is_surjective [record, in RelationAlgebra.relalg]
is_surjective [inductive, in RelationAlgebra.relalg]
is_injective [record, in RelationAlgebra.relalg]
is_injective [inductive, in RelationAlgebra.relalg]
is_univalent [record, in RelationAlgebra.relalg]
is_univalent [inductive, in RelationAlgebra.relalg]
is_antisymmetric [record, in RelationAlgebra.relalg]
is_antisymmetric [inductive, in RelationAlgebra.relalg]
is_symmetric [record, in RelationAlgebra.relalg]
is_symmetric [inductive, in RelationAlgebra.relalg]
is_linear [record, in RelationAlgebra.relalg]
is_linear [inductive, in RelationAlgebra.relalg]
is_transitive [record, in RelationAlgebra.relalg]
is_transitive [inductive, in RelationAlgebra.relalg]
is_irreflexive [record, in RelationAlgebra.relalg]
is_irreflexive [inductive, in RelationAlgebra.relalg]
is_reflexive [record, in RelationAlgebra.relalg]
is_reflexive [inductive, in RelationAlgebra.relalg]
is_nonempty' [abbreviation, in RelationAlgebra.relalg]
is_nonempty [record, in RelationAlgebra.relalg]
is_nonempty [inductive, in RelationAlgebra.relalg]
is_true_leq [instance, in RelationAlgebra.boolean]
is_true_inf [lemma, in RelationAlgebra.boolean]
is_true_sup [lemma, in RelationAlgebra.boolean]
is_nfa_nfa [lemma, in RelationAlgebra.ka_completeness]
is_typed [lemma, in RelationAlgebra.traces]
is_enfa [definition, in RelationAlgebra.nfa]
is_nfa [definition, in RelationAlgebra.nfa]
is_top_spec [lemma, in RelationAlgebra.syntax]
is_zer_spec [lemma, in RelationAlgebra.syntax]
is_case_false [constructor, in RelationAlgebra.syntax]
is_case_true [constructor, in RelationAlgebra.syntax]
is_case [inductive, in RelationAlgebra.syntax]
is_top [definition, in RelationAlgebra.syntax]
is_zer [definition, in RelationAlgebra.syntax]
is_pure_pure_part [lemma, in RelationAlgebra.regex]
is_01_simple [lemma, in RelationAlgebra.regex]
is_01_ofbool [lemma, in RelationAlgebra.regex]
is_pure_dot [constructor, in RelationAlgebra.regex]
is_pure_pls [constructor, in RelationAlgebra.regex]
is_pure_var [constructor, in RelationAlgebra.regex]
is_pure_zer [constructor, in RelationAlgebra.regex]
is_pure [inductive, in RelationAlgebra.regex]
is_simple_str [constructor, in RelationAlgebra.regex]
is_simple_dot [constructor, in RelationAlgebra.regex]
is_simple_pls [constructor, in RelationAlgebra.regex]
is_simple_var [constructor, in RelationAlgebra.regex]
is_simple_one [constructor, in RelationAlgebra.regex]
is_simple_zer [constructor, in RelationAlgebra.regex]
is_simple [inductive, in RelationAlgebra.regex]
is_01_str [constructor, in RelationAlgebra.regex]
is_01_dot [constructor, in RelationAlgebra.regex]
is_01_pls [constructor, in RelationAlgebra.regex]
is_01_one [constructor, in RelationAlgebra.regex]
is_01_zer [constructor, in RelationAlgebra.regex]
is_01 [inductive, in RelationAlgebra.regex]
is_zer_erase [lemma, in RelationAlgebra.untyping]
is_zer_level [lemma, in RelationAlgebra.untyping]
is_zer_clean [lemma, in RelationAlgebra.untyping]
is_clean [definition, in RelationAlgebra.untyping]
is_01_mx_to_row [lemma, in RelationAlgebra.rmx]
is_pure_pure_part_mx [lemma, in RelationAlgebra.rmx]
is_pure_mx_dot [lemma, in RelationAlgebra.rmx]
is_pure_mx_pls [lemma, in RelationAlgebra.rmx]
is_pure_mx_var [lemma, in RelationAlgebra.rmx]
is_pure_mx_zer [lemma, in RelationAlgebra.rmx]
is_simple_mx_dot [lemma, in RelationAlgebra.rmx]
is_simple_mx_pls [lemma, in RelationAlgebra.rmx]
is_simple_mx_var [lemma, in RelationAlgebra.rmx]
is_01_simple_mx [lemma, in RelationAlgebra.rmx]
is_01_mx_epsilon [lemma, in RelationAlgebra.rmx]
is_01_mx_str [lemma, in RelationAlgebra.rmx]
is_01_mx_sub11 [lemma, in RelationAlgebra.rmx]
is_01_mx_sub10 [lemma, in RelationAlgebra.rmx]
is_01_mx_sub01 [lemma, in RelationAlgebra.rmx]
is_01_mx_sub00 [lemma, in RelationAlgebra.rmx]
is_01_scal_mx [lemma, in RelationAlgebra.rmx]
is_01_mx_scal [lemma, in RelationAlgebra.rmx]
is_01_mx_dot [lemma, in RelationAlgebra.rmx]
is_01_mx_cup [lemma, in RelationAlgebra.rmx]
is_01_mx_one [lemma, in RelationAlgebra.rmx]
is_01_mx_zer [lemma, in RelationAlgebra.rmx]
is_pure_sup [lemma, in RelationAlgebra.rmx]
is_simple_sup [lemma, in RelationAlgebra.rmx]
is_01_sup [lemma, in RelationAlgebra.rmx]
is_pure_mx [abbreviation, in RelationAlgebra.rmx]
is_simple_mx [abbreviation, in RelationAlgebra.rmx]
is_01_mx [abbreviation, in RelationAlgebra.rmx]
ite [constructor, in RelationAlgebra.imp]
iter [definition, in RelationAlgebra.lang]
iter [definition, in RelationAlgebra.rel]
itr [projection, in RelationAlgebra.monoid]
itrtop [lemma, in RelationAlgebra.kleene]
itr_str_r [lemma, in RelationAlgebra.monoid]
itr_move [lemma, in RelationAlgebra.monoid]
itr_str_l [projection, in RelationAlgebra.monoid]
itr_aea [lemma, in RelationAlgebra.kleene]
itr_dot [lemma, in RelationAlgebra.kleene]
itr_move [lemma, in RelationAlgebra.kleene]
itr_invol [lemma, in RelationAlgebra.kleene]
itr_trans [lemma, in RelationAlgebra.kleene]
itr_pls_itr [lemma, in RelationAlgebra.kleene]
itr_snoc [lemma, in RelationAlgebra.kleene]
itr_cons [lemma, in RelationAlgebra.kleene]
itr_ext [lemma, in RelationAlgebra.kleene]
itr_weq [instance, in RelationAlgebra.kleene]
itr_leq [instance, in RelationAlgebra.kleene]
itr_ind_r [lemma, in RelationAlgebra.kleene]
itr_ind_l1 [lemma, in RelationAlgebra.kleene]
itr_ind_l [lemma, in RelationAlgebra.kleene]
itr_transitive [lemma, in RelationAlgebra.relalg]
itr' [definition, in RelationAlgebra.normalisation]
itr'itr [lemma, in RelationAlgebra.normalisation]
itr'_level [lemma, in RelationAlgebra.normalisation]
itr0 [lemma, in RelationAlgebra.kleene]
itr1 [lemma, in RelationAlgebra.kleene]
i.n [variable, in RelationAlgebra.rel]
i.x [variable, in RelationAlgebra.rel]


J

j [section, in RelationAlgebra.kat_tac]
join_leq [lemma, in RelationAlgebra.kat_tac]
j.Pred [variable, in RelationAlgebra.kat_tac]
j.src [variable, in RelationAlgebra.kat_tac]
j.tgt [variable, in RelationAlgebra.kat_tac]


K

ka [section, in RelationAlgebra.matrix]
KA [definition, in RelationAlgebra.level]
kar [projection, in RelationAlgebra.kat]
kar_BKA [projection, in RelationAlgebra.kat]
kat [library]
kat_dec [lemma, in RelationAlgebra.kat_completeness]
kat_reduces_to_ka [lemma, in RelationAlgebra.kat_completeness]
kat_correct_complete_leq [lemma, in RelationAlgebra.kat_completeness]
kat_correct_complete_weq [lemma, in RelationAlgebra.kat_completeness]
kat_complete_leq [lemma, in RelationAlgebra.kat_completeness]
kat_complete_weq [lemma, in RelationAlgebra.kat_completeness]
kat_expr [definition, in RelationAlgebra.kat_reification]
kat_weq_dec [lemma, in RelationAlgebra.kat_tac]
kat_untype_weq [lemma, in RelationAlgebra.kat_tac]
kat_untyping [library]
kat_reification [library]
kat_tac [library]
kat_completeness [library]
ka_weq_dec [lemma, in RelationAlgebra.ka_completeness]
ka_leq_dec [lemma, in RelationAlgebra.ka_completeness]
ka_correct_complete_weq [lemma, in RelationAlgebra.ka_completeness]
ka_correct_complete_leq [lemma, in RelationAlgebra.ka_completeness]
ka_complete_weq [lemma, in RelationAlgebra.ka_completeness]
ka_complete_leq [lemma, in RelationAlgebra.ka_completeness]
ka_completeness [library]
ka.build [section, in RelationAlgebra.matrix]
ka.build.m [variable, in RelationAlgebra.matrix]
ka.build.n [variable, in RelationAlgebra.matrix]
ka.build.sm [variable, in RelationAlgebra.matrix]
ka.build.sn [variable, in RelationAlgebra.matrix]
kernel_refl_antisym [lemma, in RelationAlgebra.relalg]
Kleene [lemma, in RelationAlgebra.ka_completeness]
kleene [library]


L

l [section, in RelationAlgebra.lang]
l [section, in RelationAlgebra.ugregex]
l [section, in RelationAlgebra.comparisons]
l [section, in RelationAlgebra.traces]
l [section, in RelationAlgebra.ugregex_dec]
landb_spec [lemma, in RelationAlgebra.common]
lang [definition, in RelationAlgebra.lang]
lang [definition, in RelationAlgebra.ugregex]
lang [abbreviation, in RelationAlgebra.kat_completeness]
lang [definition, in RelationAlgebra.nfa]
lang [definition, in RelationAlgebra.regex]
lang [definition, in RelationAlgebra.gregex]
lang [definition, in RelationAlgebra.dfa]
lang [abbreviation, in RelationAlgebra.ugregex_dec]
lang [library]
lang_deriv_str [lemma, in RelationAlgebra.lang]
lang_deriv_dot_2 [lemma, in RelationAlgebra.lang]
lang_deriv_dot_1 [lemma, in RelationAlgebra.lang]
lang_deriv_pls [lemma, in RelationAlgebra.lang]
lang_deriv_1 [lemma, in RelationAlgebra.lang]
lang_deriv_0 [lemma, in RelationAlgebra.lang]
lang_deriv [definition, in RelationAlgebra.lang]
lang_dot_nil [lemma, in RelationAlgebra.lang]
lang_laws [instance, in RelationAlgebra.lang]
lang_iter_S [lemma, in RelationAlgebra.lang]
lang_dot_leq [lemma, in RelationAlgebra.lang]
lang_dotx1 [lemma, in RelationAlgebra.lang]
lang_dotA [lemma, in RelationAlgebra.lang]
lang_ops [definition, in RelationAlgebra.lang]
lang_str [definition, in RelationAlgebra.lang]
lang_itr [definition, in RelationAlgebra.lang]
lang_cnv [definition, in RelationAlgebra.lang]
lang_one [definition, in RelationAlgebra.lang]
lang_rdv [definition, in RelationAlgebra.lang]
lang_ldv [definition, in RelationAlgebra.lang]
lang_dot [definition, in RelationAlgebra.lang]
lang_lattice_laws [instance, in RelationAlgebra.lang]
lang_lattice_ops [definition, in RelationAlgebra.lang]
lang_tt [constructor, in RelationAlgebra.lang]
lang_unit [inductive, in RelationAlgebra.lang]
lang_lang' [lemma, in RelationAlgebra.ugregex]
lang_sup [lemma, in RelationAlgebra.ugregex]
lang_weq [instance, in RelationAlgebra.ugregex]
lang_leq [instance, in RelationAlgebra.ugregex]
lang_ofbool [lemma, in RelationAlgebra.ugregex]
lang_1 [lemma, in RelationAlgebra.ugregex]
lang_0 [lemma, in RelationAlgebra.ugregex]
lang_empty [lemma, in RelationAlgebra.nfa]
lang_weq' [instance, in RelationAlgebra.nfa]
lang_weq [instance, in RelationAlgebra.nfa]
lang_leq [instance, in RelationAlgebra.nfa]
lang_itr [lemma, in RelationAlgebra.regex]
lang_dot [lemma, in RelationAlgebra.regex]
lang_sup [lemma, in RelationAlgebra.regex]
lang_pls [lemma, in RelationAlgebra.regex]
lang_var [lemma, in RelationAlgebra.regex]
lang_1 [lemma, in RelationAlgebra.regex]
lang_0 [lemma, in RelationAlgebra.regex]
lang_eval [lemma, in RelationAlgebra.regex]
lang_weq [instance, in RelationAlgebra.regex]
lang_leq [instance, in RelationAlgebra.regex]
lang_atom [lemma, in RelationAlgebra.gregex]
lang_sup [lemma, in RelationAlgebra.gregex]
lang_itr [lemma, in RelationAlgebra.gregex]
lang_dot [lemma, in RelationAlgebra.gregex]
lang_pls [lemma, in RelationAlgebra.gregex]
lang_1 [lemma, in RelationAlgebra.gregex]
lang_0 [lemma, in RelationAlgebra.gregex]
lang_weq [instance, in RelationAlgebra.gregex]
lang_leq [instance, in RelationAlgebra.gregex]
lang_incl_dec [lemma, in RelationAlgebra.dfa]
lang' [abbreviation, in RelationAlgebra.lang]
lang' [abbreviation, in RelationAlgebra.lang]
lang' [definition, in RelationAlgebra.ugregex]
lang'_weq [lemma, in RelationAlgebra.ugregex]
latom [abbreviation, in RelationAlgebra.kat_completeness]
lattice [library]
lattice_laws [projection, in RelationAlgebra.monoid]
laws [record, in RelationAlgebra.lattice]
laws [record, in RelationAlgebra.monoid]
laws [record, in RelationAlgebra.kat]
laws_of_injective_morphism [lemma, in RelationAlgebra.lattice]
laws_of_faithful_functor [lemma, in RelationAlgebra.monoid]
ldv [projection, in RelationAlgebra.monoid]
ldv_weq [instance, in RelationAlgebra.monoid]
ldv_leq [instance, in RelationAlgebra.monoid]
ldv_xx [lemma, in RelationAlgebra.monoid]
ldv_trans [lemma, in RelationAlgebra.monoid]
ldv_cancel [lemma, in RelationAlgebra.monoid]
ldv_spec [projection, in RelationAlgebra.monoid]
ldv_unfold [lemma, in RelationAlgebra.factors]
ldv_rdv [lemma, in RelationAlgebra.factors]
ldv_xt [lemma, in RelationAlgebra.factors]
ldv_0x [lemma, in RelationAlgebra.factors]
ldv_1x [lemma, in RelationAlgebra.factors]
ldv_xdot [lemma, in RelationAlgebra.factors]
ldv_dotx [lemma, in RelationAlgebra.factors]
leb_plus_r [lemma, in RelationAlgebra.ordinal]
lemma_3 [lemma, in RelationAlgebra.compiler_opts]
lemma_2 [lemma, in RelationAlgebra.compiler_opts]
lemma_1'' [lemma, in RelationAlgebra.compiler_opts]
lemma_1' [lemma, in RelationAlgebra.compiler_opts]
lemma_1 [lemma, in RelationAlgebra.compiler_opts]
leq [projection, in RelationAlgebra.lattice]
leq_or_weq_weq [lemma, in RelationAlgebra.lattice]
leq_or_weq [definition, in RelationAlgebra.lattice]
leq_cup_neg' [lemma, in RelationAlgebra.lattice]
leq_cup_neg [lemma, in RelationAlgebra.lattice]
leq_cap_neg' [lemma, in RelationAlgebra.lattice]
leq_cap_neg [lemma, in RelationAlgebra.lattice]
leq_iff_cap [lemma, in RelationAlgebra.lattice]
leq_cap_r [lemma, in RelationAlgebra.lattice]
leq_cap_l [lemma, in RelationAlgebra.lattice]
leq_iff_cup [lemma, in RelationAlgebra.lattice]
leq_cup_r [lemma, in RelationAlgebra.lattice]
leq_cup_l [lemma, in RelationAlgebra.lattice]
leq_tx_iff [lemma, in RelationAlgebra.lattice]
leq_xt [lemma, in RelationAlgebra.lattice]
leq_xb_iff [lemma, in RelationAlgebra.lattice]
leq_bx [lemma, in RelationAlgebra.lattice]
leq_capx [lemma, in RelationAlgebra.lattice]
leq_xcap [lemma, in RelationAlgebra.lattice]
leq_xcup [lemma, in RelationAlgebra.lattice]
leq_cupx [lemma, in RelationAlgebra.lattice]
leq_Transitive [instance, in RelationAlgebra.lattice]
leq_Reflexive [instance, in RelationAlgebra.lattice]
leq_weq_iff [instance, in RelationAlgebra.lattice]
leq_xt_ [projection, in RelationAlgebra.lattice]
leq_bx_ [projection, in RelationAlgebra.lattice]
leq_PreOrder [projection, in RelationAlgebra.lattice]
leq_ldv [lemma, in RelationAlgebra.monoid]
leq_pxq [lemma, in RelationAlgebra.relalg]
leq_xyp [lemma, in RelationAlgebra.relalg]
leq_rdv [lemma, in RelationAlgebra.factors]
leq_ind [lemma, in RelationAlgebra.regex]
leq_infx' [lemma, in RelationAlgebra.sups]
leq_infx [lemma, in RelationAlgebra.sups]
leq_xinf [lemma, in RelationAlgebra.sups]
leq_xsup' [lemma, in RelationAlgebra.sups]
leq_xsup [lemma, in RelationAlgebra.sups]
leq_supx [lemma, in RelationAlgebra.sups]
letter [inductive, in RelationAlgebra.kat_completeness]
level [record, in RelationAlgebra.level]
level [library]
levels [section, in RelationAlgebra.level]
0 [notation, in RelationAlgebra.level]
1 [notation, in RelationAlgebra.level]
level_erase [lemma, in RelationAlgebra.untyping]
lex [abbreviation, in RelationAlgebra.comparisons]
lex_spec [lemma, in RelationAlgebra.comparisons]
le_bool [definition, in RelationAlgebra.common]
le_bool_spec [lemma, in RelationAlgebra.common]
linear [projection, in RelationAlgebra.relalg]
linear [constructor, in RelationAlgebra.relalg]
linearfix [definition, in RelationAlgebra.powerfix]
linearfix_double [lemma, in RelationAlgebra.powerfix]
linearfix_S [lemma, in RelationAlgebra.powerfix]
list_compare_spec [lemma, in RelationAlgebra.comparisons]
list_compare [definition, in RelationAlgebra.comparisons]
loc [inductive, in RelationAlgebra.paterson]
loop [definition, in RelationAlgebra.ugregex_dec]
loop_aux_spec [lemma, in RelationAlgebra.ugregex_dec]
loop_aux [definition, in RelationAlgebra.ugregex_dec]
lorb_spec [lemma, in RelationAlgebra.common]
lower [record, in RelationAlgebra.level]
lower [inductive, in RelationAlgebra.level]
lower_lattice_laws [lemma, in RelationAlgebra.lattice]
lower_laws [lemma, in RelationAlgebra.monoid]
lower_mergex [lemma, in RelationAlgebra.level]
lower_xmerge [lemma, in RelationAlgebra.level]
lower_trans [instance, in RelationAlgebra.level]
lower_refl [instance, in RelationAlgebra.level]
lower_spec [lemma, in RelationAlgebra.level]
lower_bot [lemma, in RelationAlgebra.untyping]
lp [definition, in RelationAlgebra.kat_completeness]
lset [library]
lset_laws [instance, in RelationAlgebra.lset]
lset_ops [definition, in RelationAlgebra.lset]
lset_ops [definition, in RelationAlgebra.matrix]
lshift [definition, in RelationAlgebra.ordinal]
lst [definition, in RelationAlgebra.kat_completeness]
lsub_mx [definition, in RelationAlgebra.matrix]
lsyntax [library]
ltb [definition, in RelationAlgebra.ordinal]
ltb_lt [lemma, in RelationAlgebra.pair]
ltb_ind [lemma, in RelationAlgebra.ordinal]
ltb_minus [lemma, in RelationAlgebra.ordinal]
ltb_plus_r [lemma, in RelationAlgebra.ordinal]
ltb_plus_l [lemma, in RelationAlgebra.ordinal]
lt_ge_dec [definition, in RelationAlgebra.ordinal]
lt_n_1 [lemma, in RelationAlgebra.ordinal]
l_var [constructor, in RelationAlgebra.kat_completeness]
l_neg [constructor, in RelationAlgebra.kat_completeness]
l_pos [constructor, in RelationAlgebra.kat_completeness]
l.A [variable, in RelationAlgebra.comparisons]
l.a [section, in RelationAlgebra.ugregex_dec]
l.a.A [variable, in RelationAlgebra.ugregex_dec]
l.a.I [variable, in RelationAlgebra.ugregex_dec]
l.l [section, in RelationAlgebra.traces]
l.l.m [variable, in RelationAlgebra.traces]
l.l.n [variable, in RelationAlgebra.traces]
l.Pred [variable, in RelationAlgebra.ugregex]
l.Pred [variable, in RelationAlgebra.ugregex_dec]
l.src [variable, in RelationAlgebra.traces]
l.State [variable, in RelationAlgebra.traces]
l.tgt [variable, in RelationAlgebra.traces]
l.X [variable, in RelationAlgebra.lang]


M

m [section, in RelationAlgebra.lset]
M [abbreviation, in RelationAlgebra.ka_completeness]
m [section, in RelationAlgebra.matrix]
M [projection, in RelationAlgebra.nfa]
M [projection, in RelationAlgebra.dfa]
mapping_cnv [instance, in RelationAlgebra.relalg]
mapping_total [projection, in RelationAlgebra.relalg]
mapping_univalent [projection, in RelationAlgebra.relalg]
map_compat [instance, in RelationAlgebra.lset]
map_weq [instance, in RelationAlgebra.lset]
map_leq [instance, in RelationAlgebra.lset]
map_sup [lemma, in RelationAlgebra.sups]
matrix [library]
matrix_ext [library]
mem_of_row [lemma, in RelationAlgebra.rmx]
merge [definition, in RelationAlgebra.level]
merge_lower [instance, in RelationAlgebra.level]
merge_spec [lemma, in RelationAlgebra.level]
MIN [definition, in RelationAlgebra.level]
mk [definition, in RelationAlgebra.pair]
mk [constructor, in RelationAlgebra.nfa]
mk [constructor, in RelationAlgebra.dfa]
mkpi12 [lemma, in RelationAlgebra.pair]
mk_ops [constructor, in RelationAlgebra.lattice]
mk_ord [definition, in RelationAlgebra.denum]
mk_nat [definition, in RelationAlgebra.denum]
mk_pair [definition, in RelationAlgebra.denum]
mk_sum [definition, in RelationAlgebra.denum]
mk_ops [constructor, in RelationAlgebra.monoid]
mk_simple_cmp [definition, in RelationAlgebra.comparisons]
mk_cmp [constructor, in RelationAlgebra.comparisons]
mk_lt [lemma, in RelationAlgebra.pair]
mk_ops [constructor, in RelationAlgebra.kat]
mk_lower [projection, in RelationAlgebra.level]
mk_lower [constructor, in RelationAlgebra.level]
mk_level [constructor, in RelationAlgebra.level]
mm_bool_Prop [instance, in RelationAlgebra.boolean]
monoid [library]
mor [projection, in RelationAlgebra.monoid]
morphism [record, in RelationAlgebra.lattice]
mor_inj [projection, in RelationAlgebra.kat]
move [library]
Ms [definition, in RelationAlgebra.dfa]
mx [abbreviation, in RelationAlgebra.matrix]
mx [abbreviation, in RelationAlgebra.matrix]
mx [abbreviation, in RelationAlgebra.matrix]
mx [abbreviation, in RelationAlgebra.matrix]
mx [abbreviation, in RelationAlgebra.matrix]
mx [definition, in RelationAlgebra.matrix]
mx_map_fun [lemma, in RelationAlgebra.matrix_ext]
mx_dot_kfun1 [lemma, in RelationAlgebra.matrix_ext]
mx_dot_fun [lemma, in RelationAlgebra.matrix_ext]
mx_fun [definition, in RelationAlgebra.matrix_ext]
mx_map_scal [lemma, in RelationAlgebra.matrix_ext]
mx_map_blk [lemma, in RelationAlgebra.matrix_ext]
mx_map_weq [instance, in RelationAlgebra.matrix_ext]
mx_map_leq [instance, in RelationAlgebra.matrix_ext]
mx_map [definition, in RelationAlgebra.matrix_ext]
mx_str_ind' [lemma, in RelationAlgebra.matrix_ext]
mx_str_ind [lemma, in RelationAlgebra.matrix_ext]
mx_str_1 [lemma, in RelationAlgebra.matrix_ext]
mx_str_diagonal [lemma, in RelationAlgebra.matrix_ext]
mx_str_trigonal [lemma, in RelationAlgebra.matrix_ext]
mx_str_blk [lemma, in RelationAlgebra.matrix_ext]
mx_str_blk' [lemma, in RelationAlgebra.matrix_ext]
mx_bka_laws [instance, in RelationAlgebra.matrix_ext]
mx_sub11_blk [lemma, in RelationAlgebra.matrix_ext]
mx_sub10_blk [lemma, in RelationAlgebra.matrix_ext]
mx_sub01_blk [lemma, in RelationAlgebra.matrix_ext]
mx_sub00_blk [lemma, in RelationAlgebra.matrix_ext]
mx_rsub_row [lemma, in RelationAlgebra.matrix_ext]
mx_lsub_row [lemma, in RelationAlgebra.matrix_ext]
mx_bsub_col [lemma, in RelationAlgebra.matrix_ext]
mx_tsub_col [lemma, in RelationAlgebra.matrix_ext]
mx_scal_str [lemma, in RelationAlgebra.matrix_ext]
mx_scal_dot [lemma, in RelationAlgebra.matrix_ext]
mx_scal_pls [lemma, in RelationAlgebra.matrix_ext]
mx_scal_one [lemma, in RelationAlgebra.matrix_ext]
mx_scal_zer [lemma, in RelationAlgebra.matrix_ext]
mx_scal_weq [instance, in RelationAlgebra.matrix_ext]
mx_scal_leq [instance, in RelationAlgebra.matrix_ext]
mx_laws [instance, in RelationAlgebra.matrix]
mx_div_level [lemma, in RelationAlgebra.matrix]
mx_level [definition, in RelationAlgebra.matrix]
mx_str_ind_r [lemma, in RelationAlgebra.matrix]
mx_str_ind_l [lemma, in RelationAlgebra.matrix]
mx_str_cons [lemma, in RelationAlgebra.matrix]
mx_str_refl [lemma, in RelationAlgebra.matrix]
mx_str_unfold_l [lemma, in RelationAlgebra.matrix]
mx_str_build_ind_r [lemma, in RelationAlgebra.matrix]
mx_str_build_ind_l [lemma, in RelationAlgebra.matrix]
mx_str_build_unfold_l [lemma, in RelationAlgebra.matrix]
mx_cnv_ext [lemma, in RelationAlgebra.matrix]
mx_cnv_leq [lemma, in RelationAlgebra.matrix]
mx_cnv_invol [lemma, in RelationAlgebra.matrix]
mx_cnvdot_ [lemma, in RelationAlgebra.matrix]
mx_dot_blk [lemma, in RelationAlgebra.matrix]
mx_dot_rowcol [lemma, in RelationAlgebra.matrix]
mx_dot_colrow [lemma, in RelationAlgebra.matrix]
mx_dot_xrow [lemma, in RelationAlgebra.matrix]
mx_dot_colx [lemma, in RelationAlgebra.matrix]
mx_bsl_laws [instance, in RelationAlgebra.matrix]
mx_dotx0_ [lemma, in RelationAlgebra.matrix]
mx_dot0x_ [lemma, in RelationAlgebra.matrix]
mx_dotxpls_ [lemma, in RelationAlgebra.matrix]
mx_dotplsx_ [lemma, in RelationAlgebra.matrix]
mx_dot_leq [lemma, in RelationAlgebra.matrix]
mx_dotx1 [lemma, in RelationAlgebra.matrix]
mx_dot1x [lemma, in RelationAlgebra.matrix]
mx_dotA [lemma, in RelationAlgebra.matrix]
mx_ops [definition, in RelationAlgebra.matrix]
mx_itr [definition, in RelationAlgebra.matrix]
mx_str [definition, in RelationAlgebra.matrix]
mx_str_build [definition, in RelationAlgebra.matrix]
mx_cnv [definition, in RelationAlgebra.matrix]
mx_rdv [definition, in RelationAlgebra.matrix]
mx_ldv [definition, in RelationAlgebra.matrix]
mx_dot [definition, in RelationAlgebra.matrix]
mx_one [definition, in RelationAlgebra.matrix]
mx_scal [definition, in RelationAlgebra.matrix]
mx_sup [lemma, in RelationAlgebra.matrix]
mx_lattice_laws [instance, in RelationAlgebra.matrix]
mx_lattice_ops [definition, in RelationAlgebra.matrix]
mx_forall_blk [lemma, in RelationAlgebra.rmx]
mx_forall_col [lemma, in RelationAlgebra.rmx]
mx_forall_row [lemma, in RelationAlgebra.rmx]
mx_forall [definition, in RelationAlgebra.rmx]
mx_vars_full [lemma, in RelationAlgebra.rmx]
mx_vars [definition, in RelationAlgebra.rmx]
M_sum [lemma, in RelationAlgebra.ka_completeness]
m.u [variable, in RelationAlgebra.matrix]
m.X [variable, in RelationAlgebra.matrix]
_ ** _ [notation, in RelationAlgebra.matrix]


N

n [abbreviation, in RelationAlgebra.ka_completeness]
n [section, in RelationAlgebra.normalisation]
n [projection, in RelationAlgebra.nfa]
N [constructor, in RelationAlgebra.positives]
n [projection, in RelationAlgebra.dfa]
nat_compare_spec [lemma, in RelationAlgebra.comparisons]
nat_compare [definition, in RelationAlgebra.comparisons]
nat_of_ord [projection, in RelationAlgebra.ordinal]
nat_ind_2 [lemma, in RelationAlgebra.ordinal]
neg [projection, in RelationAlgebra.lattice]
NEG [definition, in RelationAlgebra.level]
negbot [lemma, in RelationAlgebra.lattice]
negb_spec [lemma, in RelationAlgebra.common]
negcap [lemma, in RelationAlgebra.lattice]
negcap' [lemma, in RelationAlgebra.lattice]
negcup [lemma, in RelationAlgebra.lattice]
negneg [lemma, in RelationAlgebra.lattice]
negtop [lemma, in RelationAlgebra.lattice]
neg_weq_iff'' [lemma, in RelationAlgebra.lattice]
neg_weq_iff' [lemma, in RelationAlgebra.lattice]
neg_weq_iff [lemma, in RelationAlgebra.lattice]
neg_leq_iff'' [lemma, in RelationAlgebra.lattice]
neg_leq_iff' [lemma, in RelationAlgebra.lattice]
neg_leq_iff [lemma, in RelationAlgebra.lattice]
neg_weq [instance, in RelationAlgebra.lattice]
neg_leq [instance, in RelationAlgebra.lattice]
neg_unique [lemma, in RelationAlgebra.lattice]
neg_unique' [lemma, in RelationAlgebra.lattice]
neqb_spec [lemma, in RelationAlgebra.paterson]
nfa [definition, in RelationAlgebra.ka_completeness]
nfa [library]
nonempty [projection, in RelationAlgebra.relalg]
nonempty [constructor, in RelationAlgebra.relalg]
nonempty_cnv [instance, in RelationAlgebra.relalg]
nonempty_cod [lemma, in RelationAlgebra.relalg]
nonempty_dom [lemma, in RelationAlgebra.relalg]
norm [definition, in RelationAlgebra.normalisation]
normalisation [library]
norm_weq [lemma, in RelationAlgebra.normalisation]
norm_level [lemma, in RelationAlgebra.normalisation]
n.distribute [variable, in RelationAlgebra.normalisation]
n.s [variable, in RelationAlgebra.normalisation]
n.t [variable, in RelationAlgebra.normalisation]


O

O [constructor, in RelationAlgebra.paterson]
o [definition, in RelationAlgebra.kat_completeness]
ob [projection, in RelationAlgebra.monoid]
obind [definition, in RelationAlgebra.ugregex_dec]
ofbool [definition, in RelationAlgebra.monoid]
ofbool [abbreviation, in RelationAlgebra.boolean]
ofbool [section, in RelationAlgebra.boolean]
ofbool_leq [instance, in RelationAlgebra.boolean]
ofold [definition, in RelationAlgebra.ugregex_dec]
of_row [definition, in RelationAlgebra.rmx]
one [projection, in RelationAlgebra.monoid]
one_blk_mx [lemma, in RelationAlgebra.matrix]
ops [record, in RelationAlgebra.lattice]
ops [record, in RelationAlgebra.monoid]
ops [record, in RelationAlgebra.kat]
opti_3_11 [lemma, in RelationAlgebra.compiler_opts]
opti_3_10' [lemma, in RelationAlgebra.compiler_opts]
opti_3_10'i [lemma, in RelationAlgebra.compiler_opts]
opti_3_9 [lemma, in RelationAlgebra.compiler_opts]
opti_3_8 [lemma, in RelationAlgebra.compiler_opts]
opti_3_5 [lemma, in RelationAlgebra.compiler_opts]
opti_3_4ii [lemma, in RelationAlgebra.compiler_opts]
opti_3_4i [lemma, in RelationAlgebra.compiler_opts]
opti_3_3 [lemma, in RelationAlgebra.compiler_opts]
opti_3_2 [lemma, in RelationAlgebra.compiler_opts]
opti_3_1_b [lemma, in RelationAlgebra.compiler_opts]
opti_3_1_a [lemma, in RelationAlgebra.compiler_opts]
op_leq_weq_2 [lemma, in RelationAlgebra.lattice]
op_leq_weq_1 [lemma, in RelationAlgebra.lattice]
orb_pls [lemma, in RelationAlgebra.boolean]
ord [record, in RelationAlgebra.ordinal]
Ord [constructor, in RelationAlgebra.ordinal]
order_cnv [instance, in RelationAlgebra.relalg]
ordinal [library]
ordS [definition, in RelationAlgebra.ordinal]
ord_nm_lt_O_n [lemma, in RelationAlgebra.pair]
ord_ind' [lemma, in RelationAlgebra.ordinal]
ord_0_empty [lemma, in RelationAlgebra.ordinal]
ord_compare_spec [lemma, in RelationAlgebra.ordinal]
ord_compare [definition, in RelationAlgebra.ordinal]
ord_lt [projection, in RelationAlgebra.ordinal]
ord_antisymmetric [projection, in RelationAlgebra.relalg]
ord_preorder [projection, in RelationAlgebra.relalg]
ord0 [definition, in RelationAlgebra.ordinal]
ord0_unique [lemma, in RelationAlgebra.ordinal]
o_inj [lemma, in RelationAlgebra.kat_completeness]
o_level [lemma, in RelationAlgebra.kat_completeness]
o_sup [lemma, in RelationAlgebra.kat_completeness]
o_npred_level [lemma, in RelationAlgebra.kat_completeness]
o_pred_level [lemma, in RelationAlgebra.kat_completeness]
o_npred [definition, in RelationAlgebra.kat_completeness]
o_pred [definition, in RelationAlgebra.kat_completeness]
o' [definition, in RelationAlgebra.kat_completeness]
o'o [lemma, in RelationAlgebra.kat_completeness]
o'o_npred [lemma, in RelationAlgebra.kat_completeness]
o'o_pred [lemma, in RelationAlgebra.kat_completeness]
o'_weq [lemma, in RelationAlgebra.kat_completeness]


P

p [section, in RelationAlgebra.comparisons]
Pack [record, in RelationAlgebra.syntax]
pack [constructor, in RelationAlgebra.syntax]
packed_eval [definition, in RelationAlgebra.syntax]
pair [library]
pair_compare_spec [lemma, in RelationAlgebra.comparisons]
pair_compare [definition, in RelationAlgebra.comparisons]
Paterson [lemma, in RelationAlgebra.paterson]
paterson [library]
pbcq_to_hoare [lemma, in RelationAlgebra.kat_tac]
pc_c [lemma, in RelationAlgebra.kat_tac]
pderiv [definition, in RelationAlgebra.ugregex_dec]
pderiv' [definition, in RelationAlgebra.ugregex_dec]
per_transitive [projection, in RelationAlgebra.relalg]
per_symmetric [projection, in RelationAlgebra.relalg]
pi1 [definition, in RelationAlgebra.pair]
pi1mk [lemma, in RelationAlgebra.pair]
pi2 [definition, in RelationAlgebra.pair]
pi2mk [lemma, in RelationAlgebra.pair]
pl [definition, in RelationAlgebra.kat_completeness]
plp [lemma, in RelationAlgebra.kat_completeness]
pls' [definition, in RelationAlgebra.normalisation]
pls'pls [lemma, in RelationAlgebra.normalisation]
pls'x0 [lemma, in RelationAlgebra.normalisation]
pls'x0_level [lemma, in RelationAlgebra.normalisation]
pls'_level [lemma, in RelationAlgebra.normalisation]
point_a'_top [lemma, in RelationAlgebra.relalg]
point_a_top [lemma, in RelationAlgebra.relalg]
point_lattice_atom [lemma, in RelationAlgebra.relalg]
point_surjective [instance, in RelationAlgebra.relalg]
point_nonempty [projection, in RelationAlgebra.relalg]
point_injective [projection, in RelationAlgebra.relalg]
point_vector [projection, in RelationAlgebra.relalg]
positives [library]
pos_compare_spec [lemma, in RelationAlgebra.positives]
pos_compare [definition, in RelationAlgebra.positives]
powerfix [definition, in RelationAlgebra.powerfix]
powerfix [section, in RelationAlgebra.powerfix]
powerfix [library]
powerfix_invariant [lemma, in RelationAlgebra.powerfix]
powerfix_linearfix [lemma, in RelationAlgebra.powerfix]
powerfix' [definition, in RelationAlgebra.powerfix]
powerfix'_linearfix [lemma, in RelationAlgebra.powerfix]
powerfix.A [variable, in RelationAlgebra.powerfix]
powerfix.B [variable, in RelationAlgebra.powerfix]
powerfix.invariant [section, in RelationAlgebra.powerfix]
powerfix.invariant.P [variable, in RelationAlgebra.powerfix]
powerfix.linear_carac.f [variable, in RelationAlgebra.powerfix]
powerfix.linear_carac [section, in RelationAlgebra.powerfix]
pow2 [definition, in RelationAlgebra.common]
pow2_S [lemma, in RelationAlgebra.powerfix]
Pred [abbreviation, in RelationAlgebra.kat_reification]
pred [abbreviation, in RelationAlgebra.kat_untyping]
pred_pow2_Sn [lemma, in RelationAlgebra.powerfix]
preorder_str [instance, in RelationAlgebra.relalg]
preorder_cnv [instance, in RelationAlgebra.relalg]
pre_transitive [projection, in RelationAlgebra.relalg]
pre_reflexive [projection, in RelationAlgebra.relalg]
prog [inductive, in RelationAlgebra.paterson]
prog [inductive, in RelationAlgebra.imp]
prog [definition, in RelationAlgebra.ugregex_dec]
prog_kat_laws [instance, in RelationAlgebra.paterson]
prog_lattice_laws [instance, in RelationAlgebra.paterson]
prog_monoid_laws [instance, in RelationAlgebra.paterson]
prog_kat_ops [definition, in RelationAlgebra.paterson]
prog_monoid_ops [definition, in RelationAlgebra.paterson]
prog_lattice_ops [definition, in RelationAlgebra.paterson]
prog_correct [lemma, in RelationAlgebra.ugregex_dec]
prog_loop [lemma, in RelationAlgebra.ugregex_dec]
prog_x_leq [lemma, in RelationAlgebra.ugregex_dec]
prog_cup_x [lemma, in RelationAlgebra.ugregex_dec]
prog' [abbreviation, in RelationAlgebra.paterson]
prop [library]
proper_weq_leq_iff [lemma, in RelationAlgebra.relalg]
props [section, in RelationAlgebra.relalg]
Prop_lattice_laws [instance, in RelationAlgebra.prop]
Prop_lattice_ops [definition, in RelationAlgebra.prop]
pure_part [definition, in RelationAlgebra.regex]
pure_part_mx [definition, in RelationAlgebra.rmx]
pwr [abbreviation, in RelationAlgebra.common]
pw_laws [instance, in RelationAlgebra.lattice]
pw_ops [definition, in RelationAlgebra.lattice]
pw0 [definition, in RelationAlgebra.lattice]
pw1 [definition, in RelationAlgebra.lattice]
pw2 [definition, in RelationAlgebra.lattice]
p_pls [constructor, in RelationAlgebra.paterson]
p_dot [constructor, in RelationAlgebra.paterson]
p_str [constructor, in RelationAlgebra.paterson]
p_aff [constructor, in RelationAlgebra.paterson]
p_tst [constructor, in RelationAlgebra.paterson]
p_var [definition, in RelationAlgebra.kat_reification]
P_sup [lemma, in RelationAlgebra.sups]
p' [constructor, in RelationAlgebra.paterson]
p.A [variable, in RelationAlgebra.comparisons]
p.B [variable, in RelationAlgebra.comparisons]


Q

qcp_to_hoare [lemma, in RelationAlgebra.kat_tac]
qpc_to_hoare [lemma, in RelationAlgebra.kat_tac]


R

R [abbreviation, in RelationAlgebra.kat_completeness]
R [module, in RelationAlgebra.kat_completeness]
R [definition, in RelationAlgebra.ka_completeness]
ra [lemma, in RelationAlgebra.normalisation]
ra_normalise [lemma, in RelationAlgebra.normalisation]
rdv [projection, in RelationAlgebra.monoid]
rdv_weq [instance, in RelationAlgebra.monoid]
rdv_leq [instance, in RelationAlgebra.monoid]
rdv_spec [projection, in RelationAlgebra.monoid]
rdv_unfold [lemma, in RelationAlgebra.factors]
rdv_trans [lemma, in RelationAlgebra.factors]
rdv_xt [lemma, in RelationAlgebra.factors]
rdv_0x [lemma, in RelationAlgebra.factors]
rdv_1x [lemma, in RelationAlgebra.factors]
rdv_xx [lemma, in RelationAlgebra.factors]
rdv_xdot [lemma, in RelationAlgebra.factors]
rdv_dotx [lemma, in RelationAlgebra.factors]
rdv_cancel [lemma, in RelationAlgebra.factors]
reflect [inductive, in RelationAlgebra.comparisons]
reflect_f [constructor, in RelationAlgebra.comparisons]
reflect_t [constructor, in RelationAlgebra.comparisons]
reflexive [projection, in RelationAlgebra.relalg]
reflexive [constructor, in RelationAlgebra.relalg]
reflexive_itr [instance, in RelationAlgebra.relalg]
reflexive_cnv [instance, in RelationAlgebra.relalg]
regex [inductive, in RelationAlgebra.regex]
regex [library]
regex_lattice_laws [instance, in RelationAlgebra.regex]
regex_laws [instance, in RelationAlgebra.regex]
regex_ops [definition, in RelationAlgebra.regex]
regex_tt [constructor, in RelationAlgebra.regex]
regex_unit [inductive, in RelationAlgebra.regex]
regex_lattice_ops [definition, in RelationAlgebra.regex]
regex' [abbreviation, in RelationAlgebra.regex]
rel [definition, in RelationAlgebra.rel]
rel [library]
relalg [library]
rel_kat_laws [instance, in RelationAlgebra.rel]
rel_kat_ops [definition, in RelationAlgebra.rel]
rel_inj [definition, in RelationAlgebra.rel]
rel_monoid_laws [instance, in RelationAlgebra.rel]
rel_monoid_ops [definition, in RelationAlgebra.rel]
rel_itr [definition, in RelationAlgebra.rel]
rel_str [definition, in RelationAlgebra.rel]
rel_rdv [definition, in RelationAlgebra.rel]
rel_ldv [definition, in RelationAlgebra.rel]
rel_cnv [definition, in RelationAlgebra.rel]
rel_dot [definition, in RelationAlgebra.rel]
rel_lattice_laws [instance, in RelationAlgebra.rel]
rel_lattice_ops [definition, in RelationAlgebra.rel]
rel_mem_spec [lemma, in RelationAlgebra.ugregex_dec]
rel_empty [abbreviation, in RelationAlgebra.ugregex_dec]
rel_insert [abbreviation, in RelationAlgebra.ugregex_dec]
rel_mem [definition, in RelationAlgebra.ugregex_dec]
remove [definition, in RelationAlgebra.normalisation]
remove_spec' [lemma, in RelationAlgebra.normalisation]
remove_spec_dep' [lemma, in RelationAlgebra.normalisation]
remove_spec [lemma, in RelationAlgebra.normalisation]
remove_spec_dep [lemma, in RelationAlgebra.normalisation]
remove_level [lemma, in RelationAlgebra.normalisation]
reroot [definition, in RelationAlgebra.dfa]
reroot_id [lemma, in RelationAlgebra.dfa]
restrict [abbreviation, in RelationAlgebra.kat_untyping]
restrict [definition, in RelationAlgebra.traces]
restrict_single [lemma, in RelationAlgebra.traces]
restrict_inj [lemma, in RelationAlgebra.traces]
restrict_itr [lemma, in RelationAlgebra.traces]
restrict_iter [lemma, in RelationAlgebra.traces]
restrict_dot [lemma, in RelationAlgebra.traces]
restrict_pls [lemma, in RelationAlgebra.traces]
restrict_1 [lemma, in RelationAlgebra.traces]
restrict_0 [lemma, in RelationAlgebra.traces]
restrict_weq [instance, in RelationAlgebra.traces]
restrict_leq [instance, in RelationAlgebra.traces]
rev [definition, in RelationAlgebra.traces]
rewriting [library]
re_ind_eval [lemma, in RelationAlgebra.regex]
re_ind [definition, in RelationAlgebra.regex]
rmov_inj [lemma, in RelationAlgebra.move]
rmov_x_neg [lemma, in RelationAlgebra.move]
rmov_x_cup [lemma, in RelationAlgebra.move]
rmov_x_cap [lemma, in RelationAlgebra.move]
rmov_x_0 [lemma, in RelationAlgebra.move]
rmov_x_1 [lemma, in RelationAlgebra.move]
rmov_x_dot [lemma, in RelationAlgebra.move]
rmov_x_pls [lemma, in RelationAlgebra.move]
rmov_x_itr [lemma, in RelationAlgebra.move]
rmov_x_str [lemma, in RelationAlgebra.move]
rmx [abbreviation, in RelationAlgebra.rmx]
rmx [library]
rmx_laws [instance, in RelationAlgebra.rmx]
rmx_lattice_laws [instance, in RelationAlgebra.rmx]
row_mx_cup [lemma, in RelationAlgebra.matrix]
row_mx_leq_iff [lemma, in RelationAlgebra.matrix]
row_mx_weq [instance, in RelationAlgebra.matrix]
row_mx_leq [instance, in RelationAlgebra.matrix]
row_mx [definition, in RelationAlgebra.matrix]
rshift [definition, in RelationAlgebra.ordinal]
rsub_mx [definition, in RelationAlgebra.matrix]
rt_clot_S_S [lemma, in RelationAlgebra.bmx]
rt_clot [inductive, in RelationAlgebra.bmx]
rule_whl' [lemma, in RelationAlgebra.imp]
rule_aff [lemma, in RelationAlgebra.imp]
rule_whl [lemma, in RelationAlgebra.imp]
rule_ite [lemma, in RelationAlgebra.imp]
rule_seq [lemma, in RelationAlgebra.imp]
rule_skp [lemma, in RelationAlgebra.imp]
R_lang_atom [lemma, in RelationAlgebra.kat_completeness]
R_u [lemma, in RelationAlgebra.ka_completeness]
R_M [lemma, in RelationAlgebra.ka_completeness]
R_v [lemma, in RelationAlgebra.ka_completeness]
r_weq [definition, in RelationAlgebra.regex]
r_leq [definition, in RelationAlgebra.regex]
r_itr [definition, in RelationAlgebra.regex]
r_var [constructor, in RelationAlgebra.regex]
r_str [constructor, in RelationAlgebra.regex]
r_dot [constructor, in RelationAlgebra.regex]
r_pls [constructor, in RelationAlgebra.regex]
r_one [constructor, in RelationAlgebra.regex]
r_zer [constructor, in RelationAlgebra.regex]


S

s [section, in RelationAlgebra.paterson]
s [section, in RelationAlgebra.kat_completeness]
s [section, in RelationAlgebra.kat_reification]
s [section, in RelationAlgebra.comparisons]
s [section, in RelationAlgebra.kat_untyping]
s [section, in RelationAlgebra.kat]
s [abbreviation, in RelationAlgebra.matrix]
s [section, in RelationAlgebra.syntax]
s [section, in RelationAlgebra.lsyntax]
s [section, in RelationAlgebra.gregex]
s [section, in RelationAlgebra.imp]
s [section, in RelationAlgebra.glang]
s [section, in RelationAlgebra.sups]
same_value [lemma, in RelationAlgebra.paterson]
scal_mx_map [lemma, in RelationAlgebra.matrix_ext]
scal_mx_weq [instance, in RelationAlgebra.matrix_ext]
scal_mx_leq [instance, in RelationAlgebra.matrix_ext]
scal_mx [definition, in RelationAlgebra.matrix]
Schroeder_r [lemma, in RelationAlgebra.monoid]
Schroeder_l [lemma, in RelationAlgebra.monoid]
Schroeder_ [lemma, in RelationAlgebra.monoid]
seq [definition, in RelationAlgebra.ordinal]
seq [constructor, in RelationAlgebra.imp]
seq_cut [lemma, in RelationAlgebra.ordinal]
seq_double [lemma, in RelationAlgebra.atoms]
set [definition, in RelationAlgebra.paterson]
set [module, in RelationAlgebra.ordinal]
set_set' [lemma, in RelationAlgebra.paterson]
set_set [lemma, in RelationAlgebra.paterson]
set.app' [definition, in RelationAlgebra.ordinal]
set.ext [lemma, in RelationAlgebra.ordinal]
set.ext' [lemma, in RelationAlgebra.ordinal]
set.mem [definition, in RelationAlgebra.ordinal]
set.mem_xI_S [lemma, in RelationAlgebra.ordinal]
set.mem_xI_0 [lemma, in RelationAlgebra.ordinal]
set.mem_xO_S [lemma, in RelationAlgebra.ordinal]
set.mem_xO_0 [lemma, in RelationAlgebra.ordinal]
set.mem_of_fun [lemma, in RelationAlgebra.ordinal]
set.mem_of_fun' [lemma, in RelationAlgebra.ordinal]
set.mem' [definition, in RelationAlgebra.ordinal]
set.od [definition, in RelationAlgebra.ordinal]
set.od_inj [lemma, in RelationAlgebra.ordinal]
set.od_bound [lemma, in RelationAlgebra.ordinal]
set.od_xI [lemma, in RelationAlgebra.ordinal]
set.od_xO [lemma, in RelationAlgebra.ordinal]
set.of_fun [definition, in RelationAlgebra.ordinal]
set.of_fun_bound [lemma, in RelationAlgebra.ordinal]
set.of_fun' [definition, in RelationAlgebra.ordinal]
set.xI [definition, in RelationAlgebra.ordinal]
set.xI_S [lemma, in RelationAlgebra.ordinal]
set.xI_0 [lemma, in RelationAlgebra.ordinal]
set.xI_bound [lemma, in RelationAlgebra.ordinal]
set.xI' [definition, in RelationAlgebra.ordinal]
set.xO [definition, in RelationAlgebra.ordinal]
set.xO_S [lemma, in RelationAlgebra.ordinal]
set.xO_0 [lemma, in RelationAlgebra.ordinal]
set.xO_bound [lemma, in RelationAlgebra.ordinal]
set.xO' [definition, in RelationAlgebra.ordinal]
Sigma [abbreviation, in RelationAlgebra.ugregex]
Sigma [abbreviation, in RelationAlgebra.kat_completeness]
Sigma [abbreviation, in RelationAlgebra.kat_reification]
Sigma [abbreviation, in RelationAlgebra.kat_untyping]
Sigma [abbreviation, in RelationAlgebra.traces]
sigma [definition, in RelationAlgebra.regex]
Sigma [abbreviation, in RelationAlgebra.gregex]
Sigma [abbreviation, in RelationAlgebra.glang]
sigma [inductive, in RelationAlgebra.positives]
Sigma [abbreviation, in RelationAlgebra.kat_tac]
Sigma [abbreviation, in RelationAlgebra.ugregex_dec]
sigma_add [definition, in RelationAlgebra.positives]
sigma_get [definition, in RelationAlgebra.positives]
sigma_empty [constructor, in RelationAlgebra.positives]
skp [constructor, in RelationAlgebra.imp]
SL [definition, in RelationAlgebra.level]
split [definition, in RelationAlgebra.ordinal]
split_ordS [lemma, in RelationAlgebra.ordinal]
split_ord0 [lemma, in RelationAlgebra.ordinal]
split_rshift [lemma, in RelationAlgebra.ordinal]
split_lshift [lemma, in RelationAlgebra.ordinal]
split_spec [lemma, in RelationAlgebra.ordinal]
split_r [constructor, in RelationAlgebra.ordinal]
split_l [constructor, in RelationAlgebra.ordinal]
split_case [inductive, in RelationAlgebra.ordinal]
src [projection, in RelationAlgebra.syntax]
src_ [definition, in RelationAlgebra.syntax]
src' [definition, in RelationAlgebra.kat_completeness]
state [record, in RelationAlgebra.paterson]
step [definition, in RelationAlgebra.dfa]
steps [definition, in RelationAlgebra.dfa]
steps_least [lemma, in RelationAlgebra.dfa]
steps_snoc [lemma, in RelationAlgebra.dfa]
steps_refl [lemma, in RelationAlgebra.dfa]
str [projection, in RelationAlgebra.monoid]
STR [definition, in RelationAlgebra.level]
strtop [lemma, in RelationAlgebra.kleene]
str_ind_r [lemma, in RelationAlgebra.monoid]
str_ldv_ [lemma, in RelationAlgebra.monoid]
str_itr [lemma, in RelationAlgebra.monoid]
str_unfold_l [lemma, in RelationAlgebra.monoid]
str_snoc [lemma, in RelationAlgebra.monoid]
str_weq [instance, in RelationAlgebra.monoid]
str_leq [instance, in RelationAlgebra.monoid]
str_ind_l1 [lemma, in RelationAlgebra.monoid]
str_ind_l' [lemma, in RelationAlgebra.monoid]
str_ext [lemma, in RelationAlgebra.monoid]
str_ind_r_ [projection, in RelationAlgebra.monoid]
str_ind_l [projection, in RelationAlgebra.monoid]
str_cons [projection, in RelationAlgebra.monoid]
str_refl [projection, in RelationAlgebra.monoid]
str_dot_refl [lemma, in RelationAlgebra.kleene]
str_weq1 [lemma, in RelationAlgebra.kleene]
str_pls1x [lemma, in RelationAlgebra.kleene]
str_pls_str [lemma, in RelationAlgebra.kleene]
str_pls' [lemma, in RelationAlgebra.kleene]
str_pls [lemma, in RelationAlgebra.kleene]
str_invol [lemma, in RelationAlgebra.kleene]
str_trans [lemma, in RelationAlgebra.kleene]
str_unique' [lemma, in RelationAlgebra.kleene]
str_unique [lemma, in RelationAlgebra.kleene]
str_dot [lemma, in RelationAlgebra.kleene]
str_move [lemma, in RelationAlgebra.kleene]
str_move_r [lemma, in RelationAlgebra.kleene]
str_move_l [lemma, in RelationAlgebra.kleene]
str_unfold_r [lemma, in RelationAlgebra.kleene]
str_ind_r1 [lemma, in RelationAlgebra.kleene]
str_ind_r' [lemma, in RelationAlgebra.kleene]
str_transitive [lemma, in RelationAlgebra.relalg]
str_inj [lemma, in RelationAlgebra.kat]
str_rdv [lemma, in RelationAlgebra.factors]
str_ldv [lemma, in RelationAlgebra.factors]
str_eps [lemma, in RelationAlgebra.regex]
str' [definition, in RelationAlgebra.normalisation]
str'str [lemma, in RelationAlgebra.normalisation]
str'_level [lemma, in RelationAlgebra.normalisation]
str0 [lemma, in RelationAlgebra.kleene]
str1 [lemma, in RelationAlgebra.kleene]
subst [definition, in RelationAlgebra.paterson]
subst [definition, in RelationAlgebra.imp]
subst_free [lemma, in RelationAlgebra.paterson]
sub00_mx [definition, in RelationAlgebra.matrix]
sub01_mx [definition, in RelationAlgebra.matrix]
sub10_mx [definition, in RelationAlgebra.matrix]
sub11_mx [definition, in RelationAlgebra.matrix]
sumbool_iff [lemma, in RelationAlgebra.common]
sumbool_true [lemma, in RelationAlgebra.common]
sums [library]
sum_atoms [lemma, in RelationAlgebra.kat_completeness]
sum_compare_spec [lemma, in RelationAlgebra.comparisons]
sum_compare [definition, in RelationAlgebra.comparisons]
sup [definition, in RelationAlgebra.sups]
supcup [lemma, in RelationAlgebra.sups]
sups [library]
sup_sup [lemma, in RelationAlgebra.sups]
sup_cut [lemma, in RelationAlgebra.sups]
sup_map [lemma, in RelationAlgebra.sups]
sup_swap [lemma, in RelationAlgebra.sups]
sup_b [lemma, in RelationAlgebra.sups]
sup_weq' [lemma, in RelationAlgebra.sups]
sup_leq' [lemma, in RelationAlgebra.sups]
sup_weq [instance, in RelationAlgebra.sups]
sup_leq [instance, in RelationAlgebra.sups]
sup_singleton [lemma, in RelationAlgebra.sups]
sup_app [lemma, in RelationAlgebra.sups]
sup_spec [lemma, in RelationAlgebra.sups]
surjective [projection, in RelationAlgebra.relalg]
surjective [constructor, in RelationAlgebra.relalg]
surjective_injective_antisym [lemma, in RelationAlgebra.relalg]
surjective_cnv [instance, in RelationAlgebra.relalg]
surjective_tx [lemma, in RelationAlgebra.relalg]
symmetric [lemma, in RelationAlgebra.relalg]
symmetric_itr [instance, in RelationAlgebra.relalg]
symmetric_str [instance, in RelationAlgebra.relalg]
symmetric_cnv [instance, in RelationAlgebra.relalg]
symmetric_ [projection, in RelationAlgebra.relalg]
symmetric_ [constructor, in RelationAlgebra.relalg]
syntax [library]
syntax_eval_id [lemma, in RelationAlgebra.untyping]
s_whl_tt [constructor, in RelationAlgebra.imp]
s_whl_ff [constructor, in RelationAlgebra.imp]
s_ite_tt [constructor, in RelationAlgebra.imp]
s_ite_ff [constructor, in RelationAlgebra.imp]
s_seq [constructor, in RelationAlgebra.imp]
s_aff [constructor, in RelationAlgebra.imp]
s_skp [constructor, in RelationAlgebra.imp]
s' [definition, in RelationAlgebra.kat_reification]
s.A [variable, in RelationAlgebra.comparisons]
s.A [variable, in RelationAlgebra.syntax]
s.A [variable, in RelationAlgebra.lsyntax]
s.B [variable, in RelationAlgebra.comparisons]
s.e [section, in RelationAlgebra.kat_reification]
s.e [section, in RelationAlgebra.syntax]
s.e [section, in RelationAlgebra.lsyntax]
s.e [section, in RelationAlgebra.gregex]
s.e.f [variable, in RelationAlgebra.syntax]
s.e.f [variable, in RelationAlgebra.lsyntax]
s.e.fo [variable, in RelationAlgebra.gregex]
s.e.fp [variable, in RelationAlgebra.kat_reification]
s.e.fp [variable, in RelationAlgebra.gregex]
s.e.fs [variable, in RelationAlgebra.gregex]
s.ff [variable, in RelationAlgebra.paterson]
s.gg [variable, in RelationAlgebra.paterson]
s.i [section, in RelationAlgebra.sups]
s.l [section, in RelationAlgebra.syntax]
s.l [section, in RelationAlgebra.lsyntax]
s.loc [variable, in RelationAlgebra.imp]
s.l.l [variable, in RelationAlgebra.syntax]
s.l.l [variable, in RelationAlgebra.lsyntax]
s.n [section, in RelationAlgebra.kat_completeness]
s.n [variable, in RelationAlgebra.kat]
s.n.n [variable, in RelationAlgebra.kat_completeness]
s.pp [variable, in RelationAlgebra.paterson]
s.pred [variable, in RelationAlgebra.kat_completeness]
s.Pred [variable, in RelationAlgebra.kat_untyping]
s.pred [variable, in RelationAlgebra.gregex]
s.pred [variable, in RelationAlgebra.glang]
s.s [variable, in RelationAlgebra.syntax]
s.src [variable, in RelationAlgebra.kat_completeness]
s.src [variable, in RelationAlgebra.kat_untyping]
s.src [variable, in RelationAlgebra.gregex]
s.src [variable, in RelationAlgebra.glang]
s.state [variable, in RelationAlgebra.imp]
s.t [variable, in RelationAlgebra.syntax]
s.tgt [variable, in RelationAlgebra.kat_completeness]
s.tgt [variable, in RelationAlgebra.kat_untyping]
s.tgt [variable, in RelationAlgebra.gregex]
s.tgt [variable, in RelationAlgebra.glang]
s.update [variable, in RelationAlgebra.imp]
s.update_comm [variable, in RelationAlgebra.imp]
s.update_twice [variable, in RelationAlgebra.imp]
_ ;; _ (imp_scope) [notation, in RelationAlgebra.imp]
_ <- _ (imp_scope) [notation, in RelationAlgebra.imp]
_ ; _ (ra_terms) [notation, in RelationAlgebra.paterson]
_ <- _ [notation, in RelationAlgebra.paterson]
_ ~ _ [notation, in RelationAlgebra.imp]


T

t [record, in RelationAlgebra.nfa]
t [record, in RelationAlgebra.dfa]
tapp [inductive, in RelationAlgebra.traces]
tapp_typed [lemma, in RelationAlgebra.traces]
tapp_x_nil_eq [lemma, in RelationAlgebra.traces]
tapp_nil_x_eq [lemma, in RelationAlgebra.traces]
tapp_cat [lemma, in RelationAlgebra.traces]
tapp_x_nil [lemma, in RelationAlgebra.traces]
tapp_nil_x [lemma, in RelationAlgebra.traces]
tapp_tail [lemma, in RelationAlgebra.traces]
tapp_head [lemma, in RelationAlgebra.traces]
tapp_tail_head [lemma, in RelationAlgebra.traces]
tapp_bounds [lemma, in RelationAlgebra.traces]
tapp_ass' [lemma, in RelationAlgebra.traces]
tapp_ass [lemma, in RelationAlgebra.traces]
tapp_cons_x [constructor, in RelationAlgebra.traces]
tapp_nil_cons [constructor, in RelationAlgebra.traces]
tapp_nil_nil [constructor, in RelationAlgebra.traces]
tatom [definition, in RelationAlgebra.traces]
tcons [constructor, in RelationAlgebra.traces]
test [abbreviation, in RelationAlgebra.paterson]
test [abbreviation, in RelationAlgebra.kat_completeness]
teval [abbreviation, in RelationAlgebra.kat_completeness]
teval_hat [lemma, in RelationAlgebra.kat_completeness]
teval_str [lemma, in RelationAlgebra.kat_completeness]
teval_xitr [lemma, in RelationAlgebra.kat_completeness]
teval_inner_dot [lemma, in RelationAlgebra.kat_completeness]
teval_dot [lemma, in RelationAlgebra.kat_completeness]
teval_var [lemma, in RelationAlgebra.kat_completeness]
teval_one [lemma, in RelationAlgebra.kat_completeness]
teval_prd [lemma, in RelationAlgebra.kat_completeness]
tglang_kat_laws [instance, in RelationAlgebra.glang]
tglang_kat_ops [definition, in RelationAlgebra.glang]
tglang_inj [definition, in RelationAlgebra.glang]
tgt [projection, in RelationAlgebra.syntax]
tgt_ [definition, in RelationAlgebra.syntax]
tgt' [definition, in RelationAlgebra.kat_completeness]
thead [definition, in RelationAlgebra.traces]
Thompson [module, in RelationAlgebra.ka_completeness]
Thompson.correct [lemma, in RelationAlgebra.ka_completeness]
Thompson.cst [definition, in RelationAlgebra.ka_completeness]
Thompson.dot [definition, in RelationAlgebra.ka_completeness]
Thompson.enfa [definition, in RelationAlgebra.ka_completeness]
Thompson.eval_str [lemma, in RelationAlgebra.ka_completeness]
Thompson.eval_itr [lemma, in RelationAlgebra.ka_completeness]
Thompson.eval_dot [lemma, in RelationAlgebra.ka_completeness]
Thompson.eval_pls [lemma, in RelationAlgebra.ka_completeness]
Thompson.eval_one [lemma, in RelationAlgebra.ka_completeness]
Thompson.eval_cst [lemma, in RelationAlgebra.ka_completeness]
Thompson.eval_zer [lemma, in RelationAlgebra.ka_completeness]
Thompson.is_enfa [lemma, in RelationAlgebra.ka_completeness]
Thompson.itr [definition, in RelationAlgebra.ka_completeness]
Thompson.one [definition, in RelationAlgebra.ka_completeness]
Thompson.pls [definition, in RelationAlgebra.ka_completeness]
Thompson.str [definition, in RelationAlgebra.ka_completeness]
Thompson.zer [definition, in RelationAlgebra.ka_completeness]
tinj [definition, in RelationAlgebra.traces]
tnil [constructor, in RelationAlgebra.traces]
tod [abbreviation, in RelationAlgebra.ugregex_dec]
top [projection, in RelationAlgebra.lattice]
top [abbreviation, in RelationAlgebra.syntax]
TOP [definition, in RelationAlgebra.level]
top_nonempty [lemma, in RelationAlgebra.relalg]
top_mnn [lemma, in RelationAlgebra.relalg]
top_nnm [lemma, in RelationAlgebra.relalg]
top' [abbreviation, in RelationAlgebra.monoid]
total [projection, in RelationAlgebra.relalg]
total [constructor, in RelationAlgebra.relalg]
total_xt [lemma, in RelationAlgebra.relalg]
total_cnv [instance, in RelationAlgebra.relalg]
to_gregex_weq [lemma, in RelationAlgebra.kat_reification]
to_gregex_eval [lemma, in RelationAlgebra.kat_reification]
to_gregex [definition, in RelationAlgebra.kat_reification]
to_blk_mx [lemma, in RelationAlgebra.matrix]
to_row_mx [lemma, in RelationAlgebra.matrix]
to_col_mx [lemma, in RelationAlgebra.matrix]
to_expr [definition, in RelationAlgebra.regex]
to_row [definition, in RelationAlgebra.rmx]
trace [inductive, in RelationAlgebra.traces]
traces [definition, in RelationAlgebra.traces]
traces [library]
traces_deriv_single [lemma, in RelationAlgebra.traces]
traces_deriv_inj [lemma, in RelationAlgebra.traces]
traces_deriv_itr [lemma, in RelationAlgebra.traces]
traces_deriv_dot_2 [lemma, in RelationAlgebra.traces]
traces_deriv_dot_1 [lemma, in RelationAlgebra.traces]
traces_deriv_pls [lemma, in RelationAlgebra.traces]
traces_deriv_1 [lemma, in RelationAlgebra.traces]
traces_deriv_0 [lemma, in RelationAlgebra.traces]
traces_deriv [definition, in RelationAlgebra.traces]
traces_dot_nil [lemma, in RelationAlgebra.traces]
traces_monoid_laws [instance, in RelationAlgebra.traces]
traces_iter_S [lemma, in RelationAlgebra.traces]
traces_dot1x [lemma, in RelationAlgebra.traces]
traces_dotx1 [lemma, in RelationAlgebra.traces]
traces_dot_leq [lemma, in RelationAlgebra.traces]
traces_dotA [lemma, in RelationAlgebra.traces]
traces_monoid_ops [definition, in RelationAlgebra.traces]
traces_str [definition, in RelationAlgebra.traces]
traces_itr [definition, in RelationAlgebra.traces]
traces_iter [definition, in RelationAlgebra.traces]
traces_cnv [definition, in RelationAlgebra.traces]
traces_one [definition, in RelationAlgebra.traces]
traces_rdv [definition, in RelationAlgebra.traces]
traces_ldv [definition, in RelationAlgebra.traces]
traces_dot [definition, in RelationAlgebra.traces]
traces_tt [constructor, in RelationAlgebra.traces]
traces_unit [inductive, in RelationAlgebra.traces]
traces_lattice_laws [instance, in RelationAlgebra.traces]
traces_lattice_ops [definition, in RelationAlgebra.traces]
traces' [abbreviation, in RelationAlgebra.traces]
traces' [abbreviation, in RelationAlgebra.traces]
transfers [definition, in RelationAlgebra.matrix]
transitive [projection, in RelationAlgebra.relalg]
transitive [constructor, in RelationAlgebra.relalg]
transitive_itr [instance, in RelationAlgebra.relalg]
transitive_cnv [instance, in RelationAlgebra.relalg]
tsingle [definition, in RelationAlgebra.traces]
tsingle' [definition, in RelationAlgebra.traces]
tsnoc [definition, in RelationAlgebra.traces]
tst [projection, in RelationAlgebra.kat]
tst_BL [projection, in RelationAlgebra.kat]
tsub_mx [definition, in RelationAlgebra.matrix]
tt [abbreviation, in RelationAlgebra.lang]
tt [abbreviation, in RelationAlgebra.ugregex]
tt [abbreviation, in RelationAlgebra.traces]
tt [abbreviation, in RelationAlgebra.ugregex_dec]
ttail [definition, in RelationAlgebra.traces]
ttcons [constructor, in RelationAlgebra.traces]
ttinj [definition, in RelationAlgebra.traces]
ttnil [constructor, in RelationAlgebra.traces]
ttraces [definition, in RelationAlgebra.traces]
ttraces_monoid_laws [instance, in RelationAlgebra.traces]
ttraces_monoid_ops [definition, in RelationAlgebra.traces]
ttraces_str [definition, in RelationAlgebra.traces]
ttraces_itr [definition, in RelationAlgebra.traces]
ttraces_iter [definition, in RelationAlgebra.traces]
ttraces_cnv [definition, in RelationAlgebra.traces]
ttraces_one [definition, in RelationAlgebra.traces]
ttraces_rdv [definition, in RelationAlgebra.traces]
ttraces_ldv [definition, in RelationAlgebra.traces]
ttraces_dot [definition, in RelationAlgebra.traces]
ttraces_lattice_laws [instance, in RelationAlgebra.traces]
ttraces_lattice_ops [definition, in RelationAlgebra.traces]
ttraces_top [definition, in RelationAlgebra.traces]
ttraces_bot [definition, in RelationAlgebra.traces]
ttraces_neg [definition, in RelationAlgebra.traces]
ttraces_cap [definition, in RelationAlgebra.traces]
ttraces_cup [definition, in RelationAlgebra.traces]
ttraces_weq [definition, in RelationAlgebra.traces]
ttraces_leq [definition, in RelationAlgebra.traces]
ttraces' [abbreviation, in RelationAlgebra.traces]
ttsingle [definition, in RelationAlgebra.traces]
two_loops [lemma, in RelationAlgebra.imp]
tx_surjective [lemma, in RelationAlgebra.relalg]
typed [abbreviation, in RelationAlgebra.kat_untyping]
typed [inductive, in RelationAlgebra.traces]
typed_uglang_gerase [lemma, in RelationAlgebra.kat_untyping]
typed' [definition, in RelationAlgebra.traces]
typed'_single [lemma, in RelationAlgebra.traces]
typed'_str [lemma, in RelationAlgebra.traces]
typed'_itr [lemma, in RelationAlgebra.traces]
typed'_iter [lemma, in RelationAlgebra.traces]
typed'_inj [lemma, in RelationAlgebra.traces]
typed'_one [lemma, in RelationAlgebra.traces]
typed'_dot [lemma, in RelationAlgebra.traces]
typed'_cap [lemma, in RelationAlgebra.traces]
typed'_cup [lemma, in RelationAlgebra.traces]
typed'_bot [lemma, in RelationAlgebra.traces]
t' [definition, in RelationAlgebra.kat_reification]


U

u [abbreviation, in RelationAlgebra.ka_completeness]
U [abbreviation, in RelationAlgebra.matrix]
U [abbreviation, in RelationAlgebra.matrix]
U [abbreviation, in RelationAlgebra.matrix]
U [abbreviation, in RelationAlgebra.matrix]
u [projection, in RelationAlgebra.nfa]
u [projection, in RelationAlgebra.dfa]
uexpr [abbreviation, in RelationAlgebra.untyping]
uexpr3 [abbreviation, in RelationAlgebra.kat_completeness]
uglang [abbreviation, in RelationAlgebra.ugregex]
uglang [abbreviation, in RelationAlgebra.kat_untyping]
uglang [abbreviation, in RelationAlgebra.ugregex_dec]
uglang_gerase [lemma, in RelationAlgebra.kat_untyping]
ugregex [inductive, in RelationAlgebra.ugregex]
ugregex [abbreviation, in RelationAlgebra.kat_untyping]
ugregex [abbreviation, in RelationAlgebra.ugregex_dec]
ugregex [library]
ugregex_cmp [definition, in RelationAlgebra.ugregex]
ugregex_compare_spec [lemma, in RelationAlgebra.ugregex]
ugregex_compare [definition, in RelationAlgebra.ugregex]
ugregex_lattice_laws [instance, in RelationAlgebra.ugregex]
ugregex_monoid_laws [instance, in RelationAlgebra.ugregex]
ugregex_monoid_ops [definition, in RelationAlgebra.ugregex]
ugregex_tt [constructor, in RelationAlgebra.ugregex]
ugregex_unit [inductive, in RelationAlgebra.ugregex]
ugregex_lattice_ops [definition, in RelationAlgebra.ugregex]
ugregex_dec [library]
ugregex' [abbreviation, in RelationAlgebra.ugregex]
UIP_cmp [lemma, in RelationAlgebra.comparisons]
union [definition, in RelationAlgebra.lset]
union_app [lemma, in RelationAlgebra.lset]
univalent [projection, in RelationAlgebra.relalg]
univalent [constructor, in RelationAlgebra.relalg]
univalent_antisym [lemma, in RelationAlgebra.relalg]
univalent_cnv [instance, in RelationAlgebra.relalg]
untype_glang [lemma, in RelationAlgebra.kat_untyping]
untyping [library]
upd [abbreviation, in RelationAlgebra.paterson]
upd [abbreviation, in RelationAlgebra.imp]
update [definition, in RelationAlgebra.paterson]
u_weq [definition, in RelationAlgebra.ugregex]
u_leq [definition, in RelationAlgebra.ugregex]
u_str [definition, in RelationAlgebra.ugregex]
u_one [definition, in RelationAlgebra.ugregex]
u_zer [definition, in RelationAlgebra.ugregex]
u_itr [constructor, in RelationAlgebra.ugregex]
u_dot [constructor, in RelationAlgebra.ugregex]
u_pls [constructor, in RelationAlgebra.ugregex]
u_prd [constructor, in RelationAlgebra.ugregex]
u_var [constructor, in RelationAlgebra.ugregex]
u_laws [instance, in RelationAlgebra.untyping]
u_lattice_laws [instance, in RelationAlgebra.untyping]
u_ops [definition, in RelationAlgebra.untyping]
u_lattice_ops [definition, in RelationAlgebra.untyping]
u_weq [definition, in RelationAlgebra.untyping]
u_leq [definition, in RelationAlgebra.untyping]


V

v [definition, in RelationAlgebra.kat_completeness]
v [inductive, in RelationAlgebra.kat_reification]
v [abbreviation, in RelationAlgebra.ka_completeness]
v [projection, in RelationAlgebra.nfa]
v [projection, in RelationAlgebra.dfa]
val [projection, in RelationAlgebra.syntax]
var [definition, in RelationAlgebra.kat_reification]
var [definition, in RelationAlgebra.regex]
vars [definition, in RelationAlgebra.kat_reification]
vars [abbreviation, in RelationAlgebra.ka_completeness]
vars [definition, in RelationAlgebra.regex]
vars [definition, in RelationAlgebra.lsyntax]
vars [projection, in RelationAlgebra.dfa]
vars [definition, in RelationAlgebra.ugregex_dec]
vector [projection, in RelationAlgebra.relalg]
vector [constructor, in RelationAlgebra.relalg]
vector_cap [instance, in RelationAlgebra.relalg]
vector' [lemma, in RelationAlgebra.relalg]
vio [projection, in RelationAlgebra.paterson]
v_sup [lemma, in RelationAlgebra.kat_completeness]
v_add [definition, in RelationAlgebra.kat_reification]
v_get [definition, in RelationAlgebra.kat_reification]
v_N [constructor, in RelationAlgebra.kat_reification]
v_L [constructor, in RelationAlgebra.kat_reification]
v1 [projection, in RelationAlgebra.paterson]
v2 [projection, in RelationAlgebra.paterson]
v3 [projection, in RelationAlgebra.paterson]
v4 [projection, in RelationAlgebra.paterson]


W

w [definition, in RelationAlgebra.kat_completeness]
weakening [lemma, in RelationAlgebra.imp]
weq [projection, in RelationAlgebra.lattice]
weq_Symmetric [instance, in RelationAlgebra.lattice]
weq_Transitive [instance, in RelationAlgebra.lattice]
weq_Reflexive [instance, in RelationAlgebra.lattice]
weq_geq [instance, in RelationAlgebra.lattice]
weq_leq [instance, in RelationAlgebra.lattice]
weq_Equivalence [instance, in RelationAlgebra.lattice]
weq_spec [projection, in RelationAlgebra.lattice]
whl [constructor, in RelationAlgebra.imp]
word [abbreviation, in RelationAlgebra.kat_completeness]
wrong_rule_whl [lemma, in RelationAlgebra.imp]
wvo_uo [lemma, in RelationAlgebra.kat_completeness]
wv_u [lemma, in RelationAlgebra.kat_completeness]
w_weq [lemma, in RelationAlgebra.kat_completeness]


X

xitr [definition, in RelationAlgebra.kat_completeness]
xpair [definition, in RelationAlgebra.denum]
xt_total [lemma, in RelationAlgebra.relalg]


Y

y1 [constructor, in RelationAlgebra.paterson]
y2 [constructor, in RelationAlgebra.paterson]
y3 [constructor, in RelationAlgebra.paterson]
y4 [constructor, in RelationAlgebra.paterson]


Z

zer [abbreviation, in RelationAlgebra.monoid]


other

_ o- _ (ast_scope) [notation, in RelationAlgebra.syntax]
_ -o _ (ast_scope) [notation, in RelationAlgebra.syntax]
! _ (ast_scope) [notation, in RelationAlgebra.syntax]
_ ^* (ast_scope) [notation, in RelationAlgebra.syntax]
_ ` (ast_scope) [notation, in RelationAlgebra.syntax]
_ ^+ (ast_scope) [notation, in RelationAlgebra.syntax]
0 (ast_scope) [notation, in RelationAlgebra.syntax]
1 (ast_scope) [notation, in RelationAlgebra.syntax]
_ * _ (ast_scope) [notation, in RelationAlgebra.syntax]
_ ^ _ (ast_scope) [notation, in RelationAlgebra.syntax]
_ + _ (ast_scope) [notation, in RelationAlgebra.syntax]
! _ (last_scope) [notation, in RelationAlgebra.lsyntax]
_ \cap _ (last_scope) [notation, in RelationAlgebra.lsyntax]
_ \cup _ (last_scope) [notation, in RelationAlgebra.lsyntax]
_ + _ (level_scope) [notation, in RelationAlgebra.level]
_ <=[ _ ]= _ (ra_scope) [notation, in RelationAlgebra.lattice]
! _ (ra_terms) [notation, in RelationAlgebra.lattice]
_ \cap _ (ra_terms) [notation, in RelationAlgebra.lattice]
_ \cup _ (ra_terms) [notation, in RelationAlgebra.lattice]
_ == _ (ra_scope) [notation, in RelationAlgebra.lattice]
_ <== _ (ra_scope) [notation, in RelationAlgebra.lattice]
_ ; _ (ra_terms) [notation, in RelationAlgebra.move]
_ ^op (ra_scope) [notation, in RelationAlgebra.monoid]
_ o- _ (ra_terms) [notation, in RelationAlgebra.monoid]
_ -o _ (ra_terms) [notation, in RelationAlgebra.monoid]
_ ^* (ra_terms) [notation, in RelationAlgebra.monoid]
_ ^+ (ra_terms) [notation, in RelationAlgebra.monoid]
_ ` (ra_terms) [notation, in RelationAlgebra.monoid]
0 (ra_terms) [notation, in RelationAlgebra.monoid]
1 (ra_terms) [notation, in RelationAlgebra.monoid]
_ ^ _ (ra_terms) [notation, in RelationAlgebra.monoid]
_ + _ (ra_terms) [notation, in RelationAlgebra.monoid]
_ * _ (ra_terms) [notation, in RelationAlgebra.monoid]
[ _ ] (ra_terms) [notation, in RelationAlgebra.kat]
_ ==_[ _ ] _ (ra_scope) [notation, in RelationAlgebra.syntax]
_ <==_[ _ ] _ (ra_scope) [notation, in RelationAlgebra.syntax]
_ ; _ (ra_terms) [notation, in RelationAlgebra.compiler_opts]
_ ==_[ _ ] _ (ra_scope) [notation, in RelationAlgebra.lsyntax]
_ <==_[ _ ] _ (ra_scope) [notation, in RelationAlgebra.lsyntax]
_ << _ (ra_scope) [notation, in RelationAlgebra.level]
\sum_ ( _ < _ ) _ (ra_terms) [notation, in RelationAlgebra.sums]
\sum_ ( _ \in _ ) _ (ra_terms) [notation, in RelationAlgebra.sums]
\inf_ ( _ < _ ) _ (ra_terms) [notation, in RelationAlgebra.sups]
\inf_ ( _ \in _ ) _ (ra_terms) [notation, in RelationAlgebra.sups]
\sup_ ( _ < _ ) _ (ra_terms) [notation, in RelationAlgebra.sups]
\sup_ ( _ \in _ ) _ (ra_terms) [notation, in RelationAlgebra.sups]
_ ||| _ [notation, in RelationAlgebra.common]
_ &&& _ [notation, in RelationAlgebra.common]
_ <<< _ [notation, in RelationAlgebra.common]
_ <= _ [notation, in RelationAlgebra.ordinal]
_ < _ [notation, in RelationAlgebra.ordinal]
_ ^v [notation, in RelationAlgebra.nfa]
_ ^M [notation, in RelationAlgebra.nfa]
_ ^u [notation, in RelationAlgebra.nfa]
_ ^v [notation, in RelationAlgebra.dfa]
_ ^M [notation, in RelationAlgebra.dfa]
_ ^u [notation, in RelationAlgebra.dfa]
[ _ :cmp] [notation, in RelationAlgebra.comparisons]



Notation Index

D

_ @ _ [in RelationAlgebra.nfa]


L

0 [in RelationAlgebra.level]
1 [in RelationAlgebra.level]


M

_ ** _ [in RelationAlgebra.matrix]


S

_ ;; _ (imp_scope) [in RelationAlgebra.imp]
_ <- _ (imp_scope) [in RelationAlgebra.imp]
_ ; _ (ra_terms) [in RelationAlgebra.paterson]
_ <- _ [in RelationAlgebra.paterson]
_ ~ _ [in RelationAlgebra.imp]


other

_ o- _ (ast_scope) [in RelationAlgebra.syntax]
_ -o _ (ast_scope) [in RelationAlgebra.syntax]
! _ (ast_scope) [in RelationAlgebra.syntax]
_ ^* (ast_scope) [in RelationAlgebra.syntax]
_ ` (ast_scope) [in RelationAlgebra.syntax]
_ ^+ (ast_scope) [in RelationAlgebra.syntax]
0 (ast_scope) [in RelationAlgebra.syntax]
1 (ast_scope) [in RelationAlgebra.syntax]
_ * _ (ast_scope) [in RelationAlgebra.syntax]
_ ^ _ (ast_scope) [in RelationAlgebra.syntax]
_ + _ (ast_scope) [in RelationAlgebra.syntax]
! _ (last_scope) [in RelationAlgebra.lsyntax]
_ \cap _ (last_scope) [in RelationAlgebra.lsyntax]
_ \cup _ (last_scope) [in RelationAlgebra.lsyntax]
_ + _ (level_scope) [in RelationAlgebra.level]
_ <=[ _ ]= _ (ra_scope) [in RelationAlgebra.lattice]
! _ (ra_terms) [in RelationAlgebra.lattice]
_ \cap _ (ra_terms) [in RelationAlgebra.lattice]
_ \cup _ (ra_terms) [in RelationAlgebra.lattice]
_ == _ (ra_scope) [in RelationAlgebra.lattice]
_ <== _ (ra_scope) [in RelationAlgebra.lattice]
_ ; _ (ra_terms) [in RelationAlgebra.move]
_ ^op (ra_scope) [in RelationAlgebra.monoid]
_ o- _ (ra_terms) [in RelationAlgebra.monoid]
_ -o _ (ra_terms) [in RelationAlgebra.monoid]
_ ^* (ra_terms) [in RelationAlgebra.monoid]
_ ^+ (ra_terms) [in RelationAlgebra.monoid]
_ ` (ra_terms) [in RelationAlgebra.monoid]
0 (ra_terms) [in RelationAlgebra.monoid]
1 (ra_terms) [in RelationAlgebra.monoid]
_ ^ _ (ra_terms) [in RelationAlgebra.monoid]
_ + _ (ra_terms) [in RelationAlgebra.monoid]
_ * _ (ra_terms) [in RelationAlgebra.monoid]
[ _ ] (ra_terms) [in RelationAlgebra.kat]
_ ==_[ _ ] _ (ra_scope) [in RelationAlgebra.syntax]
_ <==_[ _ ] _ (ra_scope) [in RelationAlgebra.syntax]
_ ; _ (ra_terms) [in RelationAlgebra.compiler_opts]
_ ==_[ _ ] _ (ra_scope) [in RelationAlgebra.lsyntax]
_ <==_[ _ ] _ (ra_scope) [in RelationAlgebra.lsyntax]
_ << _ (ra_scope) [in RelationAlgebra.level]
\sum_ ( _ < _ ) _ (ra_terms) [in RelationAlgebra.sums]
\sum_ ( _ \in _ ) _ (ra_terms) [in RelationAlgebra.sums]
\inf_ ( _ < _ ) _ (ra_terms) [in RelationAlgebra.sups]
\inf_ ( _ \in _ ) _ (ra_terms) [in RelationAlgebra.sups]
\sup_ ( _ < _ ) _ (ra_terms) [in RelationAlgebra.sups]
\sup_ ( _ \in _ ) _ (ra_terms) [in RelationAlgebra.sups]
_ ||| _ [in RelationAlgebra.common]
_ &&& _ [in RelationAlgebra.common]
_ <<< _ [in RelationAlgebra.common]
_ <= _ [in RelationAlgebra.ordinal]
_ < _ [in RelationAlgebra.ordinal]
_ ^v [in RelationAlgebra.nfa]
_ ^M [in RelationAlgebra.nfa]
_ ^u [in RelationAlgebra.nfa]
_ ^v [in RelationAlgebra.dfa]
_ ^M [in RelationAlgebra.dfa]
_ ^u [in RelationAlgebra.dfa]
[ _ :cmp] [in RelationAlgebra.comparisons]



Module Index

B

bka_to_kat [in RelationAlgebra.kat_tac]


D

dfa [in RelationAlgebra.nfa]


F

Fix [in RelationAlgebra.lset]


G

G [in RelationAlgebra.kat_completeness]


R

R [in RelationAlgebra.kat_completeness]


S

set [in RelationAlgebra.ordinal]


T

Thompson [in RelationAlgebra.ka_completeness]



Variable Index

A

atom_props.n [in RelationAlgebra.atoms]


C

clean.s [in RelationAlgebra.untyping]
clean.t [in RelationAlgebra.untyping]


D

det.Hnfa [in RelationAlgebra.ka_completeness]
det.M_ [in RelationAlgebra.ka_completeness]
det.nfa [in RelationAlgebra.ka_completeness]
det.T_ [in RelationAlgebra.ka_completeness]
det.vars' [in RelationAlgebra.ka_completeness]
det.X [in RelationAlgebra.ka_completeness]
diff.A [in RelationAlgebra.dfa]
diff.B [in RelationAlgebra.dfa]


E

empty_dec.i [in RelationAlgebra.dfa]
empty_dec.A [in RelationAlgebra.dfa]
expr_cmp.t [in RelationAlgebra.syntax]
expr_cmp.s [in RelationAlgebra.syntax]
E.A [in RelationAlgebra.ka_completeness]
e.A [in RelationAlgebra.positives]
E.B [in RelationAlgebra.ka_completeness]
E.HAB [in RelationAlgebra.ka_completeness]
E.Hvars [in RelationAlgebra.ka_completeness]
e.l.l [in RelationAlgebra.untyping]
e.s [in RelationAlgebra.untyping]
e.t [in RelationAlgebra.untyping]


I

i.n [in RelationAlgebra.rel]
i.x [in RelationAlgebra.rel]


J

j.Pred [in RelationAlgebra.kat_tac]
j.src [in RelationAlgebra.kat_tac]
j.tgt [in RelationAlgebra.kat_tac]


K

ka.build.m [in RelationAlgebra.matrix]
ka.build.n [in RelationAlgebra.matrix]
ka.build.sm [in RelationAlgebra.matrix]
ka.build.sn [in RelationAlgebra.matrix]


L

l.A [in RelationAlgebra.comparisons]
l.a.A [in RelationAlgebra.ugregex_dec]
l.a.I [in RelationAlgebra.ugregex_dec]
l.l.m [in RelationAlgebra.traces]
l.l.n [in RelationAlgebra.traces]
l.Pred [in RelationAlgebra.ugregex]
l.Pred [in RelationAlgebra.ugregex_dec]
l.src [in RelationAlgebra.traces]
l.State [in RelationAlgebra.traces]
l.tgt [in RelationAlgebra.traces]
l.X [in RelationAlgebra.lang]


M

m.u [in RelationAlgebra.matrix]
m.X [in RelationAlgebra.matrix]


N

n.distribute [in RelationAlgebra.normalisation]
n.s [in RelationAlgebra.normalisation]
n.t [in RelationAlgebra.normalisation]


P

powerfix.A [in RelationAlgebra.powerfix]
powerfix.B [in RelationAlgebra.powerfix]
powerfix.invariant.P [in RelationAlgebra.powerfix]
powerfix.linear_carac.f [in RelationAlgebra.powerfix]
p.A [in RelationAlgebra.comparisons]
p.B [in RelationAlgebra.comparisons]


S

s.A [in RelationAlgebra.comparisons]
s.A [in RelationAlgebra.syntax]
s.A [in RelationAlgebra.lsyntax]
s.B [in RelationAlgebra.comparisons]
s.e.f [in RelationAlgebra.syntax]
s.e.f [in RelationAlgebra.lsyntax]
s.e.fo [in RelationAlgebra.gregex]
s.e.fp [in RelationAlgebra.kat_reification]
s.e.fp [in RelationAlgebra.gregex]
s.e.fs [in RelationAlgebra.gregex]
s.ff [in RelationAlgebra.paterson]
s.gg [in RelationAlgebra.paterson]
s.loc [in RelationAlgebra.imp]
s.l.l [in RelationAlgebra.syntax]
s.l.l [in RelationAlgebra.lsyntax]
s.n [in RelationAlgebra.kat]
s.n.n [in RelationAlgebra.kat_completeness]
s.pp [in RelationAlgebra.paterson]
s.pred [in RelationAlgebra.kat_completeness]
s.Pred [in RelationAlgebra.kat_untyping]
s.pred [in RelationAlgebra.gregex]
s.pred [in RelationAlgebra.glang]
s.s [in RelationAlgebra.syntax]
s.src [in RelationAlgebra.kat_completeness]
s.src [in RelationAlgebra.kat_untyping]
s.src [in RelationAlgebra.gregex]
s.src [in RelationAlgebra.glang]
s.state [in RelationAlgebra.imp]
s.t [in RelationAlgebra.syntax]
s.tgt [in RelationAlgebra.kat_completeness]
s.tgt [in RelationAlgebra.kat_untyping]
s.tgt [in RelationAlgebra.gregex]
s.tgt [in RelationAlgebra.glang]
s.update [in RelationAlgebra.imp]
s.update_comm [in RelationAlgebra.imp]
s.update_twice [in RelationAlgebra.imp]



Library Index

A

atoms


B

bmx
boolean


C

common
comparisons
compiler_opts


D

denum
dfa


F

factors


G

glang
gregex


I

imp


K

kat
kat_untyping
kat_reification
kat_tac
kat_completeness
ka_completeness
kleene


L

lang
lattice
level
lset
lsyntax


M

matrix
matrix_ext
monoid
move


N

nfa
normalisation


O

ordinal


P

pair
paterson
positives
powerfix
prop


R

regex
rel
relalg
rewriting
rmx


S

sums
sups
syntax


T

traces


U

ugregex
ugregex_dec
untyping



Lemma Index

A

ab_to_hoare [in RelationAlgebra.kat_tac]
ab'_to_hoare [in RelationAlgebra.kat_tac]
aff_ite [in RelationAlgebra.imp]
aff_comm [in RelationAlgebra.imp]
aff_idem [in RelationAlgebra.imp]
aff_stack [in RelationAlgebra.imp]
andb_dot [in RelationAlgebra.boolean]
antisym [in RelationAlgebra.lattice]
atom_lattice_atom [in RelationAlgebra.relalg]
atom_points [in RelationAlgebra.relalg]
atom_mono [in RelationAlgebra.relalg]
atom_of_points [in RelationAlgebra.relalg]
atom_of_points_aux [in RelationAlgebra.relalg]
atom_xI [in RelationAlgebra.atoms]
atom_xO [in RelationAlgebra.atoms]
atom_single_atom [in RelationAlgebra.traces]
a_top_a [in RelationAlgebra.relalg]
a_top_a_aux [in RelationAlgebra.relalg]


B

bka_to_kat.laws [in RelationAlgebra.kat_tac]
blk_mx_0 [in RelationAlgebra.matrix_ext]
blk_mx' [in RelationAlgebra.matrix]
bmx_str_clot [in RelationAlgebra.bmx]
bmx_str_str [in RelationAlgebra.bmx]
bmx_top_1 [in RelationAlgebra.bmx]
bool_compare_spec [in RelationAlgebra.comparisons]
bpqc_to_hoare [in RelationAlgebra.kat_tac]
bstep_eq [in RelationAlgebra.imp]


C

capA [in RelationAlgebra.lattice]
capbx [in RelationAlgebra.lattice]
capC [in RelationAlgebra.lattice]
capcup [in RelationAlgebra.lattice]
capcup_ [in RelationAlgebra.lattice]
capcup' [in RelationAlgebra.lattice]
capI [in RelationAlgebra.lattice]
capsupx [in RelationAlgebra.sups]
captx [in RelationAlgebra.lattice]
capxb [in RelationAlgebra.lattice]
capxdot [in RelationAlgebra.monoid]
capxsup [in RelationAlgebra.sups]
capxt [in RelationAlgebra.lattice]
cap_var_atom [in RelationAlgebra.atoms]
cap'cap [in RelationAlgebra.normalisation]
cap'_level [in RelationAlgebra.normalisation]
cast_eq [in RelationAlgebra.syntax]
catch_leq [in RelationAlgebra.monoid]
catch_weq [in RelationAlgebra.monoid]
catch_ka_weq [in RelationAlgebra.kat_tac]
catch_kat_weq [in RelationAlgebra.kat_tac]
clean_hat [in RelationAlgebra.kat_completeness]
clean_str' [in RelationAlgebra.kat_completeness]
clean_inner_dot [in RelationAlgebra.kat_completeness]
clean_one' [in RelationAlgebra.kat_completeness]
clean_dot' [in RelationAlgebra.kat_completeness]
clean_elem_var [in RelationAlgebra.kat_completeness]
clean_pred [in RelationAlgebra.kat_completeness]
clean_map [in RelationAlgebra.kat_completeness]
clean_sup [in RelationAlgebra.kat_completeness]
clean_single [in RelationAlgebra.kat_completeness]
clean_cup [in RelationAlgebra.kat_completeness]
clean_bot [in RelationAlgebra.kat_completeness]
clean_erase [in RelationAlgebra.untyping]
clean_factorise_leq [in RelationAlgebra.untyping]
clean_factorise_leq_weq [in RelationAlgebra.untyping]
clean_idem [in RelationAlgebra.untyping]
clean_leq_0 [in RelationAlgebra.untyping]
clean_leq_weq_0 [in RelationAlgebra.untyping]
clean_weq [in RelationAlgebra.untyping]
clean_0_level [in RelationAlgebra.untyping]
clean_level [in RelationAlgebra.untyping]
clean_spec [in RelationAlgebra.untyping]
clot_snoc [in RelationAlgebra.bmx]
clot_app [in RelationAlgebra.bmx]
cmp_eq_rect_eq [in RelationAlgebra.comparisons]
cmp_eq_dep_eq [in RelationAlgebra.comparisons]
cmp_dec [in RelationAlgebra.comparisons]
cmp_refl [in RelationAlgebra.comparisons]
cmp_eq [in RelationAlgebra.comparisons]
cmp_spec [in RelationAlgebra.comparisons]
cnvcap [in RelationAlgebra.monoid]
cnvdot [in RelationAlgebra.monoid]
cnvitr [in RelationAlgebra.kleene]
cnvldv [in RelationAlgebra.monoid]
cnvneg [in RelationAlgebra.monoid]
cnvpls [in RelationAlgebra.monoid]
cnvrdv [in RelationAlgebra.monoid]
cnvstr [in RelationAlgebra.kleene]
cnvstr_ [in RelationAlgebra.monoid]
cnvsum [in RelationAlgebra.sums]
cnvtop [in RelationAlgebra.monoid]
cnv_ext [in RelationAlgebra.monoid]
cnv_weq_iff' [in RelationAlgebra.monoid]
cnv_weq_iff [in RelationAlgebra.monoid]
cnv_leq_iff' [in RelationAlgebra.monoid]
cnv_leq_iff [in RelationAlgebra.monoid]
cnv'cnv [in RelationAlgebra.normalisation]
cnv'_level [in RelationAlgebra.normalisation]
cnv0 [in RelationAlgebra.monoid]
cnv1 [in RelationAlgebra.monoid]
col_mx_cup [in RelationAlgebra.matrix]
col_mx_leq_iff [in RelationAlgebra.matrix]
comm4 [in RelationAlgebra.lattice]
compare_letter_spec [in RelationAlgebra.kat_completeness]
compare_lex_eq [in RelationAlgebra.comparisons]
cp_c [in RelationAlgebra.kat_tac]
cupA [in RelationAlgebra.lattice]
cupbx [in RelationAlgebra.lattice]
cupC [in RelationAlgebra.lattice]
cupcap [in RelationAlgebra.lattice]
cupcap' [in RelationAlgebra.lattice]
cupI [in RelationAlgebra.lattice]
cuptx [in RelationAlgebra.lattice]
cupxb [in RelationAlgebra.lattice]
cupxt [in RelationAlgebra.lattice]
cup_var_atom [in RelationAlgebra.atoms]


D

dead_code' [in RelationAlgebra.imp]
dead_code [in RelationAlgebra.imp]
decomp_expr [in RelationAlgebra.atoms]
decomp_top [in RelationAlgebra.atoms]
dedekind [in RelationAlgebra.relalg]
deriv_traces [in RelationAlgebra.ugregex]
deriv_sup [in RelationAlgebra.ugregex]
deriv_eval [in RelationAlgebra.nfa]
deriv_sup [in RelationAlgebra.regex]
deriv_01 [in RelationAlgebra.regex]
deriv_cancel [in RelationAlgebra.regex]
deriv_01_mx [in RelationAlgebra.rmx]
deriv_mx_str_strict [in RelationAlgebra.rmx]
deriv_mx_dot [in RelationAlgebra.rmx]
deriv_mx_pls [in RelationAlgebra.rmx]
deriv_out [in RelationAlgebra.ugregex_dec]
deriv_vars [in RelationAlgebra.ugregex_dec]
deriv_eq [in RelationAlgebra.ugregex_dec]
deriv'_vars [in RelationAlgebra.ugregex_dec]
deriv'_eq [in RelationAlgebra.ugregex_dec]
det_Xv [in RelationAlgebra.ka_completeness]
det_MX [in RelationAlgebra.ka_completeness]
det_uX [in RelationAlgebra.ka_completeness]
dfa_complete_leq [in RelationAlgebra.ka_completeness]
dfa.eval_lang [in RelationAlgebra.nfa]
dfa.is_nfa_nfa [in RelationAlgebra.nfa]
dfa.nfa_lang [in RelationAlgebra.nfa]
diff_spec [in RelationAlgebra.dfa]
dirac_refl [in RelationAlgebra.kat_completeness]
disjoint_vect_ext [in RelationAlgebra.relalg]
disjoint_vect_iff' [in RelationAlgebra.relalg]
disjoint_vect_iff [in RelationAlgebra.relalg]
disjoint_id [in RelationAlgebra.relalg]
dotcapx [in RelationAlgebra.monoid]
dotplsx [in RelationAlgebra.monoid]
dotsumx [in RelationAlgebra.sums]
dottx [in RelationAlgebra.relalg]
dotxcap [in RelationAlgebra.monoid]
dotxpls [in RelationAlgebra.monoid]
dotxsum [in RelationAlgebra.sums]
dotxt [in RelationAlgebra.relalg]
dotx0 [in RelationAlgebra.monoid]
dotx1 [in RelationAlgebra.monoid]
dot_cap_injective [in RelationAlgebra.relalg]
dot_neg_point [in RelationAlgebra.relalg]
dot_neg_surj [in RelationAlgebra.relalg]
dot_neg_inj [in RelationAlgebra.relalg]
dot_univalent_cap [in RelationAlgebra.relalg]
dot_mono [in RelationAlgebra.relalg]
dot_ofboolx [in RelationAlgebra.boolean]
dot_l_weq [in RelationAlgebra.normalisation]
dot_r_level [in RelationAlgebra.normalisation]
dot_l_level [in RelationAlgebra.normalisation]
dot'dot [in RelationAlgebra.normalisation]
dot'_level [in RelationAlgebra.normalisation]
dot0x [in RelationAlgebra.monoid]
dualize [in RelationAlgebra.lattice]
dualize [in RelationAlgebra.monoid]
dualize [in RelationAlgebra.kat]
dual_laws [in RelationAlgebra.lattice]
dual_laws [in RelationAlgebra.monoid]
dual_laws [in RelationAlgebra.kat]


E

elim_hoare_hypotheses_leq [in RelationAlgebra.kat_tac]
elim_hoare_hypotheses_weq [in RelationAlgebra.kat_tac]
empty_atom_dot [in RelationAlgebra.kat_completeness]
empty_atom_cap [in RelationAlgebra.atoms]
empty_dec [in RelationAlgebra.dfa]
empty_lang2 [in RelationAlgebra.dfa]
empty_lang1 [in RelationAlgebra.dfa]
epsilon_iff_lang_nil [in RelationAlgebra.ugregex]
epsilon_eval [in RelationAlgebra.nfa]
epsilon_iff_lang_nil [in RelationAlgebra.regex]
epsilon_iff_reflexive_eps [in RelationAlgebra.regex]
epsilon_reflexive [in RelationAlgebra.regex]
epsilon_deriv_pure [in RelationAlgebra.regex]
epsilon_pure [in RelationAlgebra.regex]
epsilon_eval [in RelationAlgebra.regex]
epsilon_deriv_pure_mx [in RelationAlgebra.rmx]
epsilon_mx_pure [in RelationAlgebra.rmx]
epsilon_mx_str [in RelationAlgebra.rmx]
epsilon_mx_dot [in RelationAlgebra.rmx]
epsilon_sup [in RelationAlgebra.rmx]
epsilon_mx_pls [in RelationAlgebra.rmx]
epsilon'_eq [in RelationAlgebra.ugregex_dec]
eqb_false [in RelationAlgebra.paterson]
eqb_spec [in RelationAlgebra.paterson]
eqb_list_spec [in RelationAlgebra.comparisons]
eqb_sum_spec [in RelationAlgebra.comparisons]
eqb_pair_spec [in RelationAlgebra.comparisons]
eqb_bool_spec [in RelationAlgebra.comparisons]
eqb_nat_spec [in RelationAlgebra.comparisons]
eqb_sym [in RelationAlgebra.comparisons]
eqb_refl [in RelationAlgebra.comparisons]
eqb_eq [in RelationAlgebra.comparisons]
eqb_spec [in RelationAlgebra.comparisons]
eqb_of_compare_spec [in RelationAlgebra.comparisons]
eqb_ord_rrshift [in RelationAlgebra.ordinal]
eqb_ord_rlshift [in RelationAlgebra.ordinal]
eqb_ord_lrshift [in RelationAlgebra.ordinal]
eqb_ord_spec [in RelationAlgebra.ordinal]
eqb_pos_spec [in RelationAlgebra.positives]
eqb_kat_correct [in RelationAlgebra.ugregex_dec]
eq_app_dot [in RelationAlgebra.lang]
eq_bool_iff [in RelationAlgebra.common]
eq_9' [in RelationAlgebra.paterson]
eq_6' [in RelationAlgebra.paterson]
eq_9 [in RelationAlgebra.paterson]
eq_8 [in RelationAlgebra.paterson]
eq_7 [in RelationAlgebra.paterson]
eq_6 [in RelationAlgebra.paterson]
eq_ord [in RelationAlgebra.ordinal]
erase_faithful_weq [in RelationAlgebra.untyping]
erase_faithful_leq [in RelationAlgebra.untyping]
erase_0 [in RelationAlgebra.untyping]
erase_faithful_leq_clean [in RelationAlgebra.untyping]
euclid_unique [in RelationAlgebra.pair]
eval_update [in RelationAlgebra.paterson]
eval_atom [in RelationAlgebra.atoms]
eval_mem_cup [in RelationAlgebra.atoms]
eval_mem_cap [in RelationAlgebra.atoms]
eval_dfa [in RelationAlgebra.ka_completeness]
eval_det [in RelationAlgebra.ka_completeness]
eval_nfa [in RelationAlgebra.ka_completeness]
eval_lang [in RelationAlgebra.nfa]
eval_deriv [in RelationAlgebra.regex]
eval_var [in RelationAlgebra.lsyntax]
eval_inf [in RelationAlgebra.lsyntax]
eval_sup [in RelationAlgebra.lsyntax]
eval_erase [in RelationAlgebra.untyping]
eval_fun [in RelationAlgebra.untyping]
eval_types_r [in RelationAlgebra.untyping]
eval_types_l [in RelationAlgebra.untyping]
eval_types [in RelationAlgebra.untyping]
eval_var [in RelationAlgebra.untyping]
eval_str [in RelationAlgebra.untyping]
eval_itr [in RelationAlgebra.untyping]
eval_one [in RelationAlgebra.untyping]
eval_var' [in RelationAlgebra.untyping]
eval_str' [in RelationAlgebra.untyping]
eval_itr' [in RelationAlgebra.untyping]
eval_one' [in RelationAlgebra.untyping]
eval_cnv [in RelationAlgebra.untyping]
eval_dot [in RelationAlgebra.untyping]
eval_pls [in RelationAlgebra.untyping]
expand [in RelationAlgebra.regex]
expand_pure [in RelationAlgebra.regex]
expand_simple [in RelationAlgebra.regex]
expand_01 [in RelationAlgebra.regex]
expand_simple_mx [in RelationAlgebra.rmx]
expand_01_mx [in RelationAlgebra.rmx]
expand' [in RelationAlgebra.regex]
expr_leq_or_weq_correct [in RelationAlgebra.normalisation]
expr_leq_correct [in RelationAlgebra.normalisation]
expr_leq_correct_dep [in RelationAlgebra.normalisation]
expr_compare_spec [in RelationAlgebra.syntax]
expr_compare_eq [in RelationAlgebra.syntax]
expr_compare_eq_dep [in RelationAlgebra.syntax]
expr_compare_spec [in RelationAlgebra.lsyntax]
expr_leq_weq_ind [in RelationAlgebra.untyping]
expr_ind_eval [in RelationAlgebra.untyping]
ext_weq_4' [in RelationAlgebra.rewriting]
ext_weq_3' [in RelationAlgebra.rewriting]
ext_weq_2' [in RelationAlgebra.rewriting]
ext_leq_4' [in RelationAlgebra.rewriting]
ext_leq_3' [in RelationAlgebra.rewriting]
ext_leq_2' [in RelationAlgebra.rewriting]
ext_weq_4 [in RelationAlgebra.rewriting]
ext_weq_3 [in RelationAlgebra.rewriting]
ext_weq_2 [in RelationAlgebra.rewriting]
ext_leq_4 [in RelationAlgebra.rewriting]
ext_leq_3 [in RelationAlgebra.rewriting]
ext_leq_2 [in RelationAlgebra.rewriting]
e_weq_weaken [in RelationAlgebra.syntax]
e_leq_weaken [in RelationAlgebra.syntax]
e_cnv_weq [in RelationAlgebra.untyping]
e_str_weq [in RelationAlgebra.untyping]
e_itr_weq [in RelationAlgebra.untyping]
e_dot_weq [in RelationAlgebra.untyping]
e_pls_weq [in RelationAlgebra.untyping]


F

fold_loop [in RelationAlgebra.imp]
fold_loop_aux_spec [in RelationAlgebra.ugregex_dec]
free_subst [in RelationAlgebra.paterson]
frel_comp [in RelationAlgebra.rel]
from_above [in RelationAlgebra.lattice]
from_below [in RelationAlgebra.lattice]
f_sup_eq [in RelationAlgebra.sups]
f_sup_weq [in RelationAlgebra.sups]


G

gc_correct [in RelationAlgebra.paterson]
gen_point [in RelationAlgebra.relalg]
gerase_weq [in RelationAlgebra.kat_untyping]
get_mk_ord [in RelationAlgebra.denum]
get_mk_nat [in RelationAlgebra.denum]
get_mk_pair [in RelationAlgebra.denum]
get_mk_sum [in RelationAlgebra.denum]
get_set' [in RelationAlgebra.paterson]
get_set [in RelationAlgebra.paterson]
geval_lst [in RelationAlgebra.kat_completeness]
geval_fst [in RelationAlgebra.kat_completeness]
geval_dot [in RelationAlgebra.kat_completeness]
gl_itr [in RelationAlgebra.kat_completeness]
gl_nildot [in RelationAlgebra.kat_completeness]
gl_dot [in RelationAlgebra.kat_completeness]
gl_single' [in RelationAlgebra.kat_completeness]
gl_atom [in RelationAlgebra.kat_completeness]
gl_sup [in RelationAlgebra.kat_completeness]
gl_cup [in RelationAlgebra.kat_completeness]
gl_bot [in RelationAlgebra.kat_completeness]
gword_tapp [in RelationAlgebra.kat_completeness]
gword_to_word_cut [in RelationAlgebra.kat_completeness]
G_hat [in RelationAlgebra.kat_completeness]
G_clean [in RelationAlgebra.kat_completeness]


H

Hoare_eq [in RelationAlgebra.imp]


I

idem_atom_dot [in RelationAlgebra.kat_completeness]
inf_singleton [in RelationAlgebra.sups]
inf_spec [in RelationAlgebra.sups]
inj_cup [in RelationAlgebra.kat]
inj_bot [in RelationAlgebra.kat]
inj_sup [in RelationAlgebra.gregex]
insert_app [in RelationAlgebra.lset]
insert_union [in RelationAlgebra.lset]
insert_pls_pls [in RelationAlgebra.normalisation]
insert_pls_level [in RelationAlgebra.normalisation]
in_singleton [in RelationAlgebra.lset]
in_idx [in RelationAlgebra.kat_reification]
in_seq [in RelationAlgebra.ordinal]
in_sup [in RelationAlgebra.sups]
In_cons [in RelationAlgebra.ugregex_dec]
irreflexive' [in RelationAlgebra.relalg]
is_true_sumbool [in RelationAlgebra.common]
is_true_inf [in RelationAlgebra.boolean]
is_true_sup [in RelationAlgebra.boolean]
is_nfa_nfa [in RelationAlgebra.ka_completeness]
is_typed [in RelationAlgebra.traces]
is_top_spec [in RelationAlgebra.syntax]
is_zer_spec [in RelationAlgebra.syntax]
is_pure_pure_part [in RelationAlgebra.regex]
is_01_simple [in RelationAlgebra.regex]
is_01_ofbool [in RelationAlgebra.regex]
is_zer_erase [in RelationAlgebra.untyping]
is_zer_level [in RelationAlgebra.untyping]
is_zer_clean [in RelationAlgebra.untyping]
is_01_mx_to_row [in RelationAlgebra.rmx]
is_pure_pure_part_mx [in RelationAlgebra.rmx]
is_pure_mx_dot [in RelationAlgebra.rmx]
is_pure_mx_pls [in RelationAlgebra.rmx]
is_pure_mx_var [in RelationAlgebra.rmx]
is_pure_mx_zer [in RelationAlgebra.rmx]
is_simple_mx_dot [in RelationAlgebra.rmx]
is_simple_mx_pls [in RelationAlgebra.rmx]
is_simple_mx_var [in RelationAlgebra.rmx]
is_01_simple_mx [in RelationAlgebra.rmx]
is_01_mx_epsilon [in RelationAlgebra.rmx]
is_01_mx_str [in RelationAlgebra.rmx]
is_01_mx_sub11 [in RelationAlgebra.rmx]
is_01_mx_sub10 [in RelationAlgebra.rmx]
is_01_mx_sub01 [in RelationAlgebra.rmx]
is_01_mx_sub00 [in RelationAlgebra.rmx]
is_01_scal_mx [in RelationAlgebra.rmx]
is_01_mx_scal [in RelationAlgebra.rmx]
is_01_mx_dot [in RelationAlgebra.rmx]
is_01_mx_cup [in RelationAlgebra.rmx]
is_01_mx_one [in RelationAlgebra.rmx]
is_01_mx_zer [in RelationAlgebra.rmx]
is_pure_sup [in RelationAlgebra.rmx]
is_simple_sup [in RelationAlgebra.rmx]
is_01_sup [in RelationAlgebra.rmx]
itrtop [in RelationAlgebra.kleene]
itr_str_r [in RelationAlgebra.monoid]
itr_move [in RelationAlgebra.monoid]
itr_aea [in RelationAlgebra.kleene]
itr_dot [in RelationAlgebra.kleene]
itr_move [in RelationAlgebra.kleene]
itr_invol [in RelationAlgebra.kleene]
itr_trans [in RelationAlgebra.kleene]
itr_pls_itr [in RelationAlgebra.kleene]
itr_snoc [in RelationAlgebra.kleene]
itr_cons [in RelationAlgebra.kleene]
itr_ext [in RelationAlgebra.kleene]
itr_ind_r [in RelationAlgebra.kleene]
itr_ind_l1 [in RelationAlgebra.kleene]
itr_ind_l [in RelationAlgebra.kleene]
itr_transitive [in RelationAlgebra.relalg]
itr'itr [in RelationAlgebra.normalisation]
itr'_level [in RelationAlgebra.normalisation]
itr0 [in RelationAlgebra.kleene]
itr1 [in RelationAlgebra.kleene]


J

join_leq [in RelationAlgebra.kat_tac]


K

kat_dec [in RelationAlgebra.kat_completeness]
kat_reduces_to_ka [in RelationAlgebra.kat_completeness]
kat_correct_complete_leq [in RelationAlgebra.kat_completeness]
kat_correct_complete_weq [in RelationAlgebra.kat_completeness]
kat_complete_leq [in RelationAlgebra.kat_completeness]
kat_complete_weq [in RelationAlgebra.kat_completeness]
kat_weq_dec [in RelationAlgebra.kat_tac]
kat_untype_weq [in RelationAlgebra.kat_tac]
ka_weq_dec [in RelationAlgebra.ka_completeness]
ka_leq_dec [in RelationAlgebra.ka_completeness]
ka_correct_complete_weq [in RelationAlgebra.ka_completeness]
ka_correct_complete_leq [in RelationAlgebra.ka_completeness]
ka_complete_weq [in RelationAlgebra.ka_completeness]
ka_complete_leq [in RelationAlgebra.ka_completeness]
kernel_refl_antisym [in RelationAlgebra.relalg]
Kleene [in RelationAlgebra.ka_completeness]


L

landb_spec [in RelationAlgebra.common]
lang_deriv_str [in RelationAlgebra.lang]
lang_deriv_dot_2 [in RelationAlgebra.lang]
lang_deriv_dot_1 [in RelationAlgebra.lang]
lang_deriv_pls [in RelationAlgebra.lang]
lang_deriv_1 [in RelationAlgebra.lang]
lang_deriv_0 [in RelationAlgebra.lang]
lang_dot_nil [in RelationAlgebra.lang]
lang_iter_S [in RelationAlgebra.lang]
lang_dot_leq [in RelationAlgebra.lang]
lang_dotx1 [in RelationAlgebra.lang]
lang_dotA [in RelationAlgebra.lang]
lang_lang' [in RelationAlgebra.ugregex]
lang_sup [in RelationAlgebra.ugregex]
lang_ofbool [in RelationAlgebra.ugregex]
lang_1 [in RelationAlgebra.ugregex]
lang_0 [in RelationAlgebra.ugregex]
lang_empty [in RelationAlgebra.nfa]
lang_itr [in RelationAlgebra.regex]
lang_dot [in RelationAlgebra.regex]
lang_sup [in RelationAlgebra.regex]
lang_pls [in RelationAlgebra.regex]
lang_var [in RelationAlgebra.regex]
lang_1 [in RelationAlgebra.regex]
lang_0 [in RelationAlgebra.regex]
lang_eval [in RelationAlgebra.regex]
lang_atom [in RelationAlgebra.gregex]
lang_sup [in RelationAlgebra.gregex]
lang_itr [in RelationAlgebra.gregex]
lang_dot [in RelationAlgebra.gregex]
lang_pls [in RelationAlgebra.gregex]
lang_1 [in RelationAlgebra.gregex]
lang_0 [in RelationAlgebra.gregex]
lang_incl_dec [in RelationAlgebra.dfa]
lang'_weq [in RelationAlgebra.ugregex]
laws_of_injective_morphism [in RelationAlgebra.lattice]
laws_of_faithful_functor [in RelationAlgebra.monoid]
ldv_xx [in RelationAlgebra.monoid]
ldv_trans [in RelationAlgebra.monoid]
ldv_cancel [in RelationAlgebra.monoid]
ldv_unfold [in RelationAlgebra.factors]
ldv_rdv [in RelationAlgebra.factors]
ldv_xt [in RelationAlgebra.factors]
ldv_0x [in RelationAlgebra.factors]
ldv_1x [in RelationAlgebra.factors]
ldv_xdot [in RelationAlgebra.factors]
ldv_dotx [in RelationAlgebra.factors]
leb_plus_r [in RelationAlgebra.ordinal]
lemma_3 [in RelationAlgebra.compiler_opts]
lemma_2 [in RelationAlgebra.compiler_opts]
lemma_1'' [in RelationAlgebra.compiler_opts]
lemma_1' [in RelationAlgebra.compiler_opts]
lemma_1 [in RelationAlgebra.compiler_opts]
leq_or_weq_weq [in RelationAlgebra.lattice]
leq_cup_neg' [in RelationAlgebra.lattice]
leq_cup_neg [in RelationAlgebra.lattice]
leq_cap_neg' [in RelationAlgebra.lattice]
leq_cap_neg [in RelationAlgebra.lattice]
leq_iff_cap [in RelationAlgebra.lattice]
leq_cap_r [in RelationAlgebra.lattice]
leq_cap_l [in RelationAlgebra.lattice]
leq_iff_cup [in RelationAlgebra.lattice]
leq_cup_r [in RelationAlgebra.lattice]
leq_cup_l [in RelationAlgebra.lattice]
leq_tx_iff [in RelationAlgebra.lattice]
leq_xt [in RelationAlgebra.lattice]
leq_xb_iff [in RelationAlgebra.lattice]
leq_bx [in RelationAlgebra.lattice]
leq_capx [in RelationAlgebra.lattice]
leq_xcap [in RelationAlgebra.lattice]
leq_xcup [in RelationAlgebra.lattice]
leq_cupx [in RelationAlgebra.lattice]
leq_ldv [in RelationAlgebra.monoid]
leq_pxq [in RelationAlgebra.relalg]
leq_xyp [in RelationAlgebra.relalg]
leq_rdv [in RelationAlgebra.factors]
leq_ind [in RelationAlgebra.regex]
leq_infx' [in RelationAlgebra.sups]
leq_infx [in RelationAlgebra.sups]
leq_xinf [in RelationAlgebra.sups]
leq_xsup' [in RelationAlgebra.sups]
leq_xsup [in RelationAlgebra.sups]
leq_supx [in RelationAlgebra.sups]
level_erase [in RelationAlgebra.untyping]
lex_spec [in RelationAlgebra.comparisons]
le_bool_spec [in RelationAlgebra.common]
linearfix_double [in RelationAlgebra.powerfix]
linearfix_S [in RelationAlgebra.powerfix]
list_compare_spec [in RelationAlgebra.comparisons]
loop_aux_spec [in RelationAlgebra.ugregex_dec]
lorb_spec [in RelationAlgebra.common]
lower_lattice_laws [in RelationAlgebra.lattice]
lower_laws [in RelationAlgebra.monoid]
lower_mergex [in RelationAlgebra.level]
lower_xmerge [in RelationAlgebra.level]
lower_spec [in RelationAlgebra.level]
lower_bot [in RelationAlgebra.untyping]
ltb_lt [in RelationAlgebra.pair]
ltb_ind [in RelationAlgebra.ordinal]
ltb_minus [in RelationAlgebra.ordinal]
ltb_plus_r [in RelationAlgebra.ordinal]
ltb_plus_l [in RelationAlgebra.ordinal]
lt_n_1 [in RelationAlgebra.ordinal]


M

map_sup [in RelationAlgebra.sups]
mem_of_row [in RelationAlgebra.rmx]
merge_spec [in RelationAlgebra.level]
mkpi12 [in RelationAlgebra.pair]
mk_lt [in RelationAlgebra.pair]
mx_map_fun [in RelationAlgebra.matrix_ext]
mx_dot_kfun1 [in RelationAlgebra.matrix_ext]
mx_dot_fun [in RelationAlgebra.matrix_ext]
mx_map_scal [in RelationAlgebra.matrix_ext]
mx_map_blk [in RelationAlgebra.matrix_ext]
mx_str_ind' [in RelationAlgebra.matrix_ext]
mx_str_ind [in RelationAlgebra.matrix_ext]
mx_str_1 [in RelationAlgebra.matrix_ext]
mx_str_diagonal [in RelationAlgebra.matrix_ext]
mx_str_trigonal [in RelationAlgebra.matrix_ext]
mx_str_blk [in RelationAlgebra.matrix_ext]
mx_str_blk' [in RelationAlgebra.matrix_ext]
mx_sub11_blk [in RelationAlgebra.matrix_ext]
mx_sub10_blk [in RelationAlgebra.matrix_ext]
mx_sub01_blk [in RelationAlgebra.matrix_ext]
mx_sub00_blk [in RelationAlgebra.matrix_ext]
mx_rsub_row [in RelationAlgebra.matrix_ext]
mx_lsub_row [in RelationAlgebra.matrix_ext]
mx_bsub_col [in RelationAlgebra.matrix_ext]
mx_tsub_col [in RelationAlgebra.matrix_ext]
mx_scal_str [in RelationAlgebra.matrix_ext]
mx_scal_dot [in RelationAlgebra.matrix_ext]
mx_scal_pls [in RelationAlgebra.matrix_ext]
mx_scal_one [in RelationAlgebra.matrix_ext]
mx_scal_zer [in RelationAlgebra.matrix_ext]
mx_div_level [in RelationAlgebra.matrix]
mx_str_ind_r [in RelationAlgebra.matrix]
mx_str_ind_l [in RelationAlgebra.matrix]
mx_str_cons [in RelationAlgebra.matrix]
mx_str_refl [in RelationAlgebra.matrix]
mx_str_unfold_l [in RelationAlgebra.matrix]
mx_str_build_ind_r [in RelationAlgebra.matrix]
mx_str_build_ind_l [in RelationAlgebra.matrix]
mx_str_build_unfold_l [in RelationAlgebra.matrix]
mx_cnv_ext [in RelationAlgebra.matrix]
mx_cnv_leq [in RelationAlgebra.matrix]
mx_cnv_invol [in RelationAlgebra.matrix]
mx_cnvdot_ [in RelationAlgebra.matrix]
mx_dot_blk [in RelationAlgebra.matrix]
mx_dot_rowcol [in RelationAlgebra.matrix]
mx_dot_colrow [in RelationAlgebra.matrix]
mx_dot_xrow [in RelationAlgebra.matrix]
mx_dot_colx [in RelationAlgebra.matrix]
mx_dotx0_ [in RelationAlgebra.matrix]
mx_dot0x_ [in RelationAlgebra.matrix]
mx_dotxpls_ [in RelationAlgebra.matrix]
mx_dotplsx_ [in RelationAlgebra.matrix]
mx_dot_leq [in RelationAlgebra.matrix]
mx_dotx1 [in RelationAlgebra.matrix]
mx_dot1x [in RelationAlgebra.matrix]
mx_dotA [in RelationAlgebra.matrix]
mx_sup [in RelationAlgebra.matrix]
mx_forall_blk [in RelationAlgebra.rmx]
mx_forall_col [in RelationAlgebra.rmx]
mx_forall_row [in RelationAlgebra.rmx]
mx_vars_full [in RelationAlgebra.rmx]
M_sum [in RelationAlgebra.ka_completeness]


N

nat_compare_spec [in RelationAlgebra.comparisons]
nat_ind_2 [in RelationAlgebra.ordinal]
negbot [in RelationAlgebra.lattice]
negb_spec [in RelationAlgebra.common]
negcap [in RelationAlgebra.lattice]
negcap' [in RelationAlgebra.lattice]
negcup [in RelationAlgebra.lattice]
negneg [in RelationAlgebra.lattice]
negtop [in RelationAlgebra.lattice]
neg_weq_iff'' [in RelationAlgebra.lattice]
neg_weq_iff' [in RelationAlgebra.lattice]
neg_weq_iff [in RelationAlgebra.lattice]
neg_leq_iff'' [in RelationAlgebra.lattice]
neg_leq_iff' [in RelationAlgebra.lattice]
neg_leq_iff [in RelationAlgebra.lattice]
neg_unique [in RelationAlgebra.lattice]
neg_unique' [in RelationAlgebra.lattice]
neqb_spec [in RelationAlgebra.paterson]
nonempty_cod [in RelationAlgebra.relalg]
nonempty_dom [in RelationAlgebra.relalg]
norm_weq [in RelationAlgebra.normalisation]
norm_level [in RelationAlgebra.normalisation]


O

one_blk_mx [in RelationAlgebra.matrix]
opti_3_11 [in RelationAlgebra.compiler_opts]
opti_3_10' [in RelationAlgebra.compiler_opts]
opti_3_10'i [in RelationAlgebra.compiler_opts]
opti_3_9 [in RelationAlgebra.compiler_opts]
opti_3_8 [in RelationAlgebra.compiler_opts]
opti_3_5 [in RelationAlgebra.compiler_opts]
opti_3_4ii [in RelationAlgebra.compiler_opts]
opti_3_4i [in RelationAlgebra.compiler_opts]
opti_3_3 [in RelationAlgebra.compiler_opts]
opti_3_2 [in RelationAlgebra.compiler_opts]
opti_3_1_b [in RelationAlgebra.compiler_opts]
opti_3_1_a [in RelationAlgebra.compiler_opts]
op_leq_weq_2 [in RelationAlgebra.lattice]
op_leq_weq_1 [in RelationAlgebra.lattice]
orb_pls [in RelationAlgebra.boolean]
ord_nm_lt_O_n [in RelationAlgebra.pair]
ord_ind' [in RelationAlgebra.ordinal]
ord_0_empty [in RelationAlgebra.ordinal]
ord_compare_spec [in RelationAlgebra.ordinal]
ord0_unique [in RelationAlgebra.ordinal]
o_inj [in RelationAlgebra.kat_completeness]
o_level [in RelationAlgebra.kat_completeness]
o_sup [in RelationAlgebra.kat_completeness]
o_npred_level [in RelationAlgebra.kat_completeness]
o_pred_level [in RelationAlgebra.kat_completeness]
o'o [in RelationAlgebra.kat_completeness]
o'o_npred [in RelationAlgebra.kat_completeness]
o'o_pred [in RelationAlgebra.kat_completeness]
o'_weq [in RelationAlgebra.kat_completeness]


P

pair_compare_spec [in RelationAlgebra.comparisons]
Paterson [in RelationAlgebra.paterson]
pbcq_to_hoare [in RelationAlgebra.kat_tac]
pc_c [in RelationAlgebra.kat_tac]
pi1mk [in RelationAlgebra.pair]
pi2mk [in RelationAlgebra.pair]
plp [in RelationAlgebra.kat_completeness]
pls'pls [in RelationAlgebra.normalisation]
pls'x0 [in RelationAlgebra.normalisation]
pls'x0_level [in RelationAlgebra.normalisation]
pls'_level [in RelationAlgebra.normalisation]
point_a'_top [in RelationAlgebra.relalg]
point_a_top [in RelationAlgebra.relalg]
point_lattice_atom [in RelationAlgebra.relalg]
pos_compare_spec [in RelationAlgebra.positives]
powerfix_invariant [in RelationAlgebra.powerfix]
powerfix_linearfix [in RelationAlgebra.powerfix]
powerfix'_linearfix [in RelationAlgebra.powerfix]
pow2_S [in RelationAlgebra.powerfix]
pred_pow2_Sn [in RelationAlgebra.powerfix]
prog_correct [in RelationAlgebra.ugregex_dec]
prog_loop [in RelationAlgebra.ugregex_dec]
prog_x_leq [in RelationAlgebra.ugregex_dec]
prog_cup_x [in RelationAlgebra.ugregex_dec]
proper_weq_leq_iff [in RelationAlgebra.relalg]
P_sup [in RelationAlgebra.sups]


Q

qcp_to_hoare [in RelationAlgebra.kat_tac]
qpc_to_hoare [in RelationAlgebra.kat_tac]


R

ra [in RelationAlgebra.normalisation]
ra_normalise [in RelationAlgebra.normalisation]
rdv_unfold [in RelationAlgebra.factors]
rdv_trans [in RelationAlgebra.factors]
rdv_xt [in RelationAlgebra.factors]
rdv_0x [in RelationAlgebra.factors]
rdv_1x [in RelationAlgebra.factors]
rdv_xx [in RelationAlgebra.factors]
rdv_xdot [in RelationAlgebra.factors]
rdv_dotx [in RelationAlgebra.factors]
rdv_cancel [in RelationAlgebra.factors]
rel_mem_spec [in RelationAlgebra.ugregex_dec]
remove_spec' [in RelationAlgebra.normalisation]
remove_spec_dep' [in RelationAlgebra.normalisation]
remove_spec [in RelationAlgebra.normalisation]
remove_spec_dep [in RelationAlgebra.normalisation]
remove_level [in RelationAlgebra.normalisation]
reroot_id [in RelationAlgebra.dfa]
restrict_single [in RelationAlgebra.traces]
restrict_inj [in RelationAlgebra.traces]
restrict_itr [in RelationAlgebra.traces]
restrict_iter [in RelationAlgebra.traces]
restrict_dot [in RelationAlgebra.traces]
restrict_pls [in RelationAlgebra.traces]
restrict_1 [in RelationAlgebra.traces]
restrict_0 [in RelationAlgebra.traces]
re_ind_eval [in RelationAlgebra.regex]
rmov_inj [in RelationAlgebra.move]
rmov_x_neg [in RelationAlgebra.move]
rmov_x_cup [in RelationAlgebra.move]
rmov_x_cap [in RelationAlgebra.move]
rmov_x_0 [in RelationAlgebra.move]
rmov_x_1 [in RelationAlgebra.move]
rmov_x_dot [in RelationAlgebra.move]
rmov_x_pls [in RelationAlgebra.move]
rmov_x_itr [in RelationAlgebra.move]
rmov_x_str [in RelationAlgebra.move]
row_mx_cup [in RelationAlgebra.matrix]
row_mx_leq_iff [in RelationAlgebra.matrix]
rt_clot_S_S [in RelationAlgebra.bmx]
rule_whl' [in RelationAlgebra.imp]
rule_aff [in RelationAlgebra.imp]
rule_whl [in RelationAlgebra.imp]
rule_ite [in RelationAlgebra.imp]
rule_seq [in RelationAlgebra.imp]
rule_skp [in RelationAlgebra.imp]
R_lang_atom [in RelationAlgebra.kat_completeness]
R_u [in RelationAlgebra.ka_completeness]
R_M [in RelationAlgebra.ka_completeness]
R_v [in RelationAlgebra.ka_completeness]


S

same_value [in RelationAlgebra.paterson]
scal_mx_map [in RelationAlgebra.matrix_ext]
Schroeder_r [in RelationAlgebra.monoid]
Schroeder_l [in RelationAlgebra.monoid]
Schroeder_ [in RelationAlgebra.monoid]
seq_cut [in RelationAlgebra.ordinal]
seq_double [in RelationAlgebra.atoms]
set_set' [in RelationAlgebra.paterson]
set_set [in RelationAlgebra.paterson]
set.ext [in RelationAlgebra.ordinal]
set.ext' [in RelationAlgebra.ordinal]
set.mem_xI_S [in RelationAlgebra.ordinal]
set.mem_xI_0 [in RelationAlgebra.ordinal]
set.mem_xO_S [in RelationAlgebra.ordinal]
set.mem_xO_0 [in RelationAlgebra.ordinal]
set.mem_of_fun [in RelationAlgebra.ordinal]
set.mem_of_fun' [in RelationAlgebra.ordinal]
set.od_inj [in RelationAlgebra.ordinal]
set.od_bound [in RelationAlgebra.ordinal]
set.od_xI [in RelationAlgebra.ordinal]
set.od_xO [in RelationAlgebra.ordinal]
set.of_fun_bound [in RelationAlgebra.ordinal]
set.xI_S [in RelationAlgebra.ordinal]
set.xI_0 [in RelationAlgebra.ordinal]
set.xI_bound [in RelationAlgebra.ordinal]
set.xO_S [in RelationAlgebra.ordinal]
set.xO_0 [in RelationAlgebra.ordinal]
set.xO_bound [in RelationAlgebra.ordinal]
split_ordS [in RelationAlgebra.ordinal]
split_ord0 [in RelationAlgebra.ordinal]
split_rshift [in RelationAlgebra.ordinal]
split_lshift [in RelationAlgebra.ordinal]
split_spec [in RelationAlgebra.ordinal]
steps_least [in RelationAlgebra.dfa]
steps_snoc [in RelationAlgebra.dfa]
steps_refl [in RelationAlgebra.dfa]
strtop [in RelationAlgebra.kleene]
str_ind_r [in RelationAlgebra.monoid]
str_ldv_ [in RelationAlgebra.monoid]
str_itr [in RelationAlgebra.monoid]
str_unfold_l [in RelationAlgebra.monoid]
str_snoc [in RelationAlgebra.monoid]
str_ind_l1 [in RelationAlgebra.monoid]
str_ind_l' [in RelationAlgebra.monoid]
str_ext [in RelationAlgebra.monoid]
str_dot_refl [in RelationAlgebra.kleene]
str_weq1 [in RelationAlgebra.kleene]
str_pls1x [in RelationAlgebra.kleene]
str_pls_str [in RelationAlgebra.kleene]
str_pls' [in RelationAlgebra.kleene]
str_pls [in RelationAlgebra.kleene]
str_invol [in RelationAlgebra.kleene]
str_trans [in RelationAlgebra.kleene]
str_unique' [in RelationAlgebra.kleene]
str_unique [in RelationAlgebra.kleene]
str_dot [in RelationAlgebra.kleene]
str_move [in RelationAlgebra.kleene]
str_move_r [in RelationAlgebra.kleene]
str_move_l [in RelationAlgebra.kleene]
str_unfold_r [in RelationAlgebra.kleene]
str_ind_r1 [in RelationAlgebra.kleene]
str_ind_r' [in RelationAlgebra.kleene]
str_transitive [in RelationAlgebra.relalg]
str_inj [in RelationAlgebra.kat]
str_rdv [in RelationAlgebra.factors]
str_ldv [in RelationAlgebra.factors]
str_eps [in RelationAlgebra.regex]
str'str [in RelationAlgebra.normalisation]
str'_level [in RelationAlgebra.normalisation]
str0 [in RelationAlgebra.kleene]
str1 [in RelationAlgebra.kleene]
subst_free [in RelationAlgebra.paterson]
sumbool_iff [in RelationAlgebra.common]
sumbool_true [in RelationAlgebra.common]
sum_atoms [in RelationAlgebra.kat_completeness]
sum_compare_spec [in RelationAlgebra.comparisons]
supcup [in RelationAlgebra.sups]
sup_sup [in RelationAlgebra.sups]
sup_cut [in RelationAlgebra.sups]
sup_map [in RelationAlgebra.sups]
sup_swap [in RelationAlgebra.sups]
sup_b [in RelationAlgebra.sups]
sup_weq' [in RelationAlgebra.sups]
sup_leq' [in RelationAlgebra.sups]
sup_singleton [in RelationAlgebra.sups]
sup_app [in RelationAlgebra.sups]
sup_spec [in RelationAlgebra.sups]
surjective_injective_antisym [in RelationAlgebra.relalg]
surjective_tx [in RelationAlgebra.relalg]
symmetric [in RelationAlgebra.relalg]
syntax_eval_id [in RelationAlgebra.untyping]


T

tapp_typed [in RelationAlgebra.traces]
tapp_x_nil_eq [in RelationAlgebra.traces]
tapp_nil_x_eq [in RelationAlgebra.traces]
tapp_cat [in RelationAlgebra.traces]
tapp_x_nil [in RelationAlgebra.traces]
tapp_nil_x [in RelationAlgebra.traces]
tapp_tail [in RelationAlgebra.traces]
tapp_head [in RelationAlgebra.traces]
tapp_tail_head [in RelationAlgebra.traces]
tapp_bounds [in RelationAlgebra.traces]
tapp_ass' [in RelationAlgebra.traces]
tapp_ass [in RelationAlgebra.traces]
teval_hat [in RelationAlgebra.kat_completeness]
teval_str [in RelationAlgebra.kat_completeness]
teval_xitr [in RelationAlgebra.kat_completeness]
teval_inner_dot [in RelationAlgebra.kat_completeness]
teval_dot [in RelationAlgebra.kat_completeness]
teval_var [in RelationAlgebra.kat_completeness]
teval_one [in RelationAlgebra.kat_completeness]
teval_prd [in RelationAlgebra.kat_completeness]
Thompson.correct [in RelationAlgebra.ka_completeness]
Thompson.eval_str [in RelationAlgebra.ka_completeness]
Thompson.eval_itr [in RelationAlgebra.ka_completeness]
Thompson.eval_dot [in RelationAlgebra.ka_completeness]
Thompson.eval_pls [in RelationAlgebra.ka_completeness]
Thompson.eval_one [in RelationAlgebra.ka_completeness]
Thompson.eval_cst [in RelationAlgebra.ka_completeness]
Thompson.eval_zer [in RelationAlgebra.ka_completeness]
Thompson.is_enfa [in RelationAlgebra.ka_completeness]
top_nonempty [in RelationAlgebra.relalg]
top_mnn [in RelationAlgebra.relalg]
top_nnm [in RelationAlgebra.relalg]
total_xt [in RelationAlgebra.relalg]
to_gregex_weq [in RelationAlgebra.kat_reification]
to_gregex_eval [in RelationAlgebra.kat_reification]
to_blk_mx [in RelationAlgebra.matrix]
to_row_mx [in RelationAlgebra.matrix]
to_col_mx [in RelationAlgebra.matrix]
traces_deriv_single [in RelationAlgebra.traces]
traces_deriv_inj [in RelationAlgebra.traces]
traces_deriv_itr [in RelationAlgebra.traces]
traces_deriv_dot_2 [in RelationAlgebra.traces]
traces_deriv_dot_1 [in RelationAlgebra.traces]
traces_deriv_pls [in RelationAlgebra.traces]
traces_deriv_1 [in RelationAlgebra.traces]
traces_deriv_0 [in RelationAlgebra.traces]
traces_dot_nil [in RelationAlgebra.traces]
traces_iter_S [in RelationAlgebra.traces]
traces_dot1x [in RelationAlgebra.traces]
traces_dotx1 [in RelationAlgebra.traces]
traces_dot_leq [in RelationAlgebra.traces]
traces_dotA [in RelationAlgebra.traces]
two_loops [in RelationAlgebra.imp]
tx_surjective [in RelationAlgebra.relalg]
typed_uglang_gerase [in RelationAlgebra.kat_untyping]
typed'_single [in RelationAlgebra.traces]
typed'_str [in RelationAlgebra.traces]
typed'_itr [in RelationAlgebra.traces]
typed'_iter [in RelationAlgebra.traces]
typed'_inj [in RelationAlgebra.traces]
typed'_one [in RelationAlgebra.traces]
typed'_dot [in RelationAlgebra.traces]
typed'_cap [in RelationAlgebra.traces]
typed'_cup [in RelationAlgebra.traces]
typed'_bot [in RelationAlgebra.traces]


U

uglang_gerase [in RelationAlgebra.kat_untyping]
ugregex_compare_spec [in RelationAlgebra.ugregex]
UIP_cmp [in RelationAlgebra.comparisons]
union_app [in RelationAlgebra.lset]
univalent_antisym [in RelationAlgebra.relalg]
untype_glang [in RelationAlgebra.kat_untyping]


V

vector' [in RelationAlgebra.relalg]
v_sup [in RelationAlgebra.kat_completeness]


W

weakening [in RelationAlgebra.imp]
wrong_rule_whl [in RelationAlgebra.imp]
wvo_uo [in RelationAlgebra.kat_completeness]
wv_u [in RelationAlgebra.kat_completeness]
w_weq [in RelationAlgebra.kat_completeness]


X

xt_total [in RelationAlgebra.relalg]



Constructor Index

A

aff [in RelationAlgebra.imp]
antisymmetric [in RelationAlgebra.relalg]


B

bool_tt [in RelationAlgebra.boolean]


C

clot_cons [in RelationAlgebra.bmx]
clot_nil [in RelationAlgebra.bmx]
compare_gt [in RelationAlgebra.comparisons]
compare_lt [in RelationAlgebra.comparisons]
compare_eq [in RelationAlgebra.comparisons]


E

ev_var [in RelationAlgebra.untyping]
ev_cnv [in RelationAlgebra.untyping]
ev_str [in RelationAlgebra.untyping]
ev_itr [in RelationAlgebra.untyping]
ev_dot [in RelationAlgebra.untyping]
ev_pls [in RelationAlgebra.untyping]
ev_one [in RelationAlgebra.untyping]
e_top [in RelationAlgebra.paterson]
e_bot [in RelationAlgebra.paterson]
e_neg [in RelationAlgebra.paterson]
e_cup [in RelationAlgebra.paterson]
e_cap [in RelationAlgebra.paterson]
e_var [in RelationAlgebra.paterson]
e_var [in RelationAlgebra.syntax]
e_rdv [in RelationAlgebra.syntax]
e_ldv [in RelationAlgebra.syntax]
e_cnv [in RelationAlgebra.syntax]
e_str [in RelationAlgebra.syntax]
e_itr [in RelationAlgebra.syntax]
e_dot [in RelationAlgebra.syntax]
e_neg [in RelationAlgebra.syntax]
e_cap [in RelationAlgebra.syntax]
e_pls [in RelationAlgebra.syntax]
e_one [in RelationAlgebra.syntax]
e_top [in RelationAlgebra.syntax]
e_zer [in RelationAlgebra.syntax]
e_var [in RelationAlgebra.lsyntax]
e_neg [in RelationAlgebra.lsyntax]
e_cap [in RelationAlgebra.lsyntax]
e_cup [in RelationAlgebra.lsyntax]
e_top [in RelationAlgebra.lsyntax]
e_bot [in RelationAlgebra.lsyntax]


F

f' [in RelationAlgebra.paterson]


G

g_elem [in RelationAlgebra.kat_completeness]
g_pred [in RelationAlgebra.kat_completeness]
g_itr [in RelationAlgebra.gregex]
g_dot [in RelationAlgebra.gregex]
g_pls [in RelationAlgebra.gregex]
g_var [in RelationAlgebra.gregex]
g_prd [in RelationAlgebra.gregex]
g_zer [in RelationAlgebra.gregex]
g' [in RelationAlgebra.paterson]


I

injective [in RelationAlgebra.relalg]
io [in RelationAlgebra.paterson]
irreflexive [in RelationAlgebra.relalg]
is_case_false [in RelationAlgebra.syntax]
is_case_true [in RelationAlgebra.syntax]
is_pure_dot [in RelationAlgebra.regex]
is_pure_pls [in RelationAlgebra.regex]
is_pure_var [in RelationAlgebra.regex]
is_pure_zer [in RelationAlgebra.regex]
is_simple_str [in RelationAlgebra.regex]
is_simple_dot [in RelationAlgebra.regex]
is_simple_pls [in RelationAlgebra.regex]
is_simple_var [in RelationAlgebra.regex]
is_simple_one [in RelationAlgebra.regex]
is_simple_zer [in RelationAlgebra.regex]
is_01_str [in RelationAlgebra.regex]
is_01_dot [in RelationAlgebra.regex]
is_01_pls [in RelationAlgebra.regex]
is_01_one [in RelationAlgebra.regex]
is_01_zer [in RelationAlgebra.regex]
ite [in RelationAlgebra.imp]


L

lang_tt [in RelationAlgebra.lang]
linear [in RelationAlgebra.relalg]
l_var [in RelationAlgebra.kat_completeness]
l_neg [in RelationAlgebra.kat_completeness]
l_pos [in RelationAlgebra.kat_completeness]


M

mk [in RelationAlgebra.nfa]
mk [in RelationAlgebra.dfa]
mk_ops [in RelationAlgebra.lattice]
mk_ops [in RelationAlgebra.monoid]
mk_cmp [in RelationAlgebra.comparisons]
mk_ops [in RelationAlgebra.kat]
mk_lower [in RelationAlgebra.level]
mk_level [in RelationAlgebra.level]


N

N [in RelationAlgebra.positives]
nonempty [in RelationAlgebra.relalg]


O

O [in RelationAlgebra.paterson]
Ord [in RelationAlgebra.ordinal]


P

pack [in RelationAlgebra.syntax]
p_pls [in RelationAlgebra.paterson]
p_dot [in RelationAlgebra.paterson]
p_str [in RelationAlgebra.paterson]
p_aff [in RelationAlgebra.paterson]
p_tst [in RelationAlgebra.paterson]
p' [in RelationAlgebra.paterson]


R

reflect_f [in RelationAlgebra.comparisons]
reflect_t [in RelationAlgebra.comparisons]
reflexive [in RelationAlgebra.relalg]
regex_tt [in RelationAlgebra.regex]
r_var [in RelationAlgebra.regex]
r_str [in RelationAlgebra.regex]
r_dot [in RelationAlgebra.regex]
r_pls [in RelationAlgebra.regex]
r_one [in RelationAlgebra.regex]
r_zer [in RelationAlgebra.regex]


S

seq [in RelationAlgebra.imp]
sigma_empty [in RelationAlgebra.positives]
skp [in RelationAlgebra.imp]
split_r [in RelationAlgebra.ordinal]
split_l [in RelationAlgebra.ordinal]
surjective [in RelationAlgebra.relalg]
symmetric_ [in RelationAlgebra.relalg]
s_whl_tt [in RelationAlgebra.imp]
s_whl_ff [in RelationAlgebra.imp]
s_ite_tt [in RelationAlgebra.imp]
s_ite_ff [in RelationAlgebra.imp]
s_seq [in RelationAlgebra.imp]
s_aff [in RelationAlgebra.imp]
s_skp [in RelationAlgebra.imp]


T

tapp_cons_x [in RelationAlgebra.traces]
tapp_nil_cons [in RelationAlgebra.traces]
tapp_nil_nil [in RelationAlgebra.traces]
tcons [in RelationAlgebra.traces]
tnil [in RelationAlgebra.traces]
total [in RelationAlgebra.relalg]
traces_tt [in RelationAlgebra.traces]
transitive [in RelationAlgebra.relalg]
ttcons [in RelationAlgebra.traces]
ttnil [in RelationAlgebra.traces]


U

ugregex_tt [in RelationAlgebra.ugregex]
univalent [in RelationAlgebra.relalg]
u_itr [in RelationAlgebra.ugregex]
u_dot [in RelationAlgebra.ugregex]
u_pls [in RelationAlgebra.ugregex]
u_prd [in RelationAlgebra.ugregex]
u_var [in RelationAlgebra.ugregex]


V

vector [in RelationAlgebra.relalg]
v_N [in RelationAlgebra.kat_reification]
v_L [in RelationAlgebra.kat_reification]


W

whl [in RelationAlgebra.imp]


Y

y1 [in RelationAlgebra.paterson]
y2 [in RelationAlgebra.paterson]
y3 [in RelationAlgebra.paterson]
y4 [in RelationAlgebra.paterson]



Inductive Index

B

bool_unit [in RelationAlgebra.boolean]
bstep' [in RelationAlgebra.imp]


C

compare_spec [in RelationAlgebra.comparisons]


E

eval [in RelationAlgebra.untyping]
expr [in RelationAlgebra.paterson]
expr [in RelationAlgebra.syntax]
expr [in RelationAlgebra.lsyntax]


G

gregex [in RelationAlgebra.gregex]
guard [in RelationAlgebra.kat_completeness]


I

is_vector [in RelationAlgebra.relalg]
is_total [in RelationAlgebra.relalg]
is_surjective [in RelationAlgebra.relalg]
is_injective [in RelationAlgebra.relalg]
is_univalent [in RelationAlgebra.relalg]
is_antisymmetric [in RelationAlgebra.relalg]
is_symmetric [in RelationAlgebra.relalg]
is_linear [in RelationAlgebra.relalg]
is_transitive [in RelationAlgebra.relalg]
is_irreflexive [in RelationAlgebra.relalg]
is_reflexive [in RelationAlgebra.relalg]
is_nonempty [in RelationAlgebra.relalg]
is_case [in RelationAlgebra.syntax]
is_pure [in RelationAlgebra.regex]
is_simple [in RelationAlgebra.regex]
is_01 [in RelationAlgebra.regex]


L

lang_unit [in RelationAlgebra.lang]
letter [in RelationAlgebra.kat_completeness]
loc [in RelationAlgebra.paterson]
lower [in RelationAlgebra.level]


P

prog [in RelationAlgebra.paterson]
prog [in RelationAlgebra.imp]


R

reflect [in RelationAlgebra.comparisons]
regex [in RelationAlgebra.regex]
regex_unit [in RelationAlgebra.regex]
rt_clot [in RelationAlgebra.bmx]


S

sigma [in RelationAlgebra.positives]
split_case [in RelationAlgebra.ordinal]


T

tapp [in RelationAlgebra.traces]
trace [in RelationAlgebra.traces]
traces_unit [in RelationAlgebra.traces]
typed [in RelationAlgebra.traces]


U

ugregex [in RelationAlgebra.ugregex]
ugregex_unit [in RelationAlgebra.ugregex]


V

v [in RelationAlgebra.kat_reification]



Projection Index

A

antisymmetric [in RelationAlgebra.relalg]
atom_nonempty [in RelationAlgebra.relalg]
a_top_a' [in RelationAlgebra.relalg]
a'_top_a [in RelationAlgebra.relalg]


B

bot [in RelationAlgebra.lattice]


C

cap [in RelationAlgebra.lattice]
capdotx [in RelationAlgebra.monoid]
capneg [in RelationAlgebra.lattice]
cap_spec [in RelationAlgebra.lattice]
car [in RelationAlgebra.lattice]
carr [in RelationAlgebra.comparisons]
cmp [in RelationAlgebra.comparisons]
cnv [in RelationAlgebra.monoid]
cnvdot_ [in RelationAlgebra.monoid]
cnv_ext_ [in RelationAlgebra.monoid]
cnv_leq [in RelationAlgebra.monoid]
cnv_invol [in RelationAlgebra.monoid]
cup [in RelationAlgebra.lattice]
cupcap_ [in RelationAlgebra.lattice]
cupneg [in RelationAlgebra.lattice]
cup_spec [in RelationAlgebra.lattice]


D

dot [in RelationAlgebra.monoid]
dotA [in RelationAlgebra.monoid]
dotplsx_ [in RelationAlgebra.monoid]
dotxpls_ [in RelationAlgebra.monoid]
dotx0_ [in RelationAlgebra.monoid]
dotx1_ [in RelationAlgebra.monoid]
dot_leq_ [in RelationAlgebra.monoid]
dot0x_ [in RelationAlgebra.monoid]
dot1x [in RelationAlgebra.monoid]


E

eqb [in RelationAlgebra.comparisons]


F

fn_neg [in RelationAlgebra.lattice]
fn_top [in RelationAlgebra.lattice]
fn_bot [in RelationAlgebra.lattice]
fn_cap [in RelationAlgebra.lattice]
fn_cup [in RelationAlgebra.lattice]
fn_weq [in RelationAlgebra.lattice]
fn_leq [in RelationAlgebra.lattice]
fn_rdv [in RelationAlgebra.monoid]
fn_ldv [in RelationAlgebra.monoid]
fn_cnv [in RelationAlgebra.monoid]
fn_str [in RelationAlgebra.monoid]
fn_itr [in RelationAlgebra.monoid]
fn_one [in RelationAlgebra.monoid]
fn_dot [in RelationAlgebra.monoid]
fn_morphism [in RelationAlgebra.monoid]


H

has_div [in RelationAlgebra.level]
has_neg [in RelationAlgebra.level]
has_cnv [in RelationAlgebra.level]
has_str [in RelationAlgebra.level]
has_top [in RelationAlgebra.level]
has_cap [in RelationAlgebra.level]
has_bot [in RelationAlgebra.level]
has_cup [in RelationAlgebra.level]


I

inj [in RelationAlgebra.kat]
injective [in RelationAlgebra.relalg]
inj_cap [in RelationAlgebra.kat]
inj_top [in RelationAlgebra.kat]
irreflexive [in RelationAlgebra.relalg]
itr [in RelationAlgebra.monoid]
itr_str_l [in RelationAlgebra.monoid]


K

kar [in RelationAlgebra.kat]
kar_BKA [in RelationAlgebra.kat]


L

lattice_laws [in RelationAlgebra.monoid]
ldv [in RelationAlgebra.monoid]
ldv_spec [in RelationAlgebra.monoid]
leq [in RelationAlgebra.lattice]
leq_xt_ [in RelationAlgebra.lattice]
leq_bx_ [in RelationAlgebra.lattice]
leq_PreOrder [in RelationAlgebra.lattice]
linear [in RelationAlgebra.relalg]


M

M [in RelationAlgebra.nfa]
M [in RelationAlgebra.dfa]
mapping_total [in RelationAlgebra.relalg]
mapping_univalent [in RelationAlgebra.relalg]
mk_lower [in RelationAlgebra.level]
mor [in RelationAlgebra.monoid]
mor_inj [in RelationAlgebra.kat]


N

n [in RelationAlgebra.nfa]
n [in RelationAlgebra.dfa]
nat_of_ord [in RelationAlgebra.ordinal]
neg [in RelationAlgebra.lattice]
nonempty [in RelationAlgebra.relalg]


O

ob [in RelationAlgebra.monoid]
one [in RelationAlgebra.monoid]
ord_lt [in RelationAlgebra.ordinal]
ord_antisymmetric [in RelationAlgebra.relalg]
ord_preorder [in RelationAlgebra.relalg]


P

per_transitive [in RelationAlgebra.relalg]
per_symmetric [in RelationAlgebra.relalg]
point_nonempty [in RelationAlgebra.relalg]
point_injective [in RelationAlgebra.relalg]
point_vector [in RelationAlgebra.relalg]
pre_transitive [in RelationAlgebra.relalg]
pre_reflexive [in RelationAlgebra.relalg]


R

rdv [in RelationAlgebra.monoid]
rdv_spec [in RelationAlgebra.monoid]
reflexive [in RelationAlgebra.relalg]


S

src [in RelationAlgebra.syntax]
str [in RelationAlgebra.monoid]
str_ind_r_ [in RelationAlgebra.monoid]
str_ind_l [in RelationAlgebra.monoid]
str_cons [in RelationAlgebra.monoid]
str_refl [in RelationAlgebra.monoid]
surjective [in RelationAlgebra.relalg]
symmetric_ [in RelationAlgebra.relalg]


T

tgt [in RelationAlgebra.syntax]
top [in RelationAlgebra.lattice]
total [in RelationAlgebra.relalg]
transitive [in RelationAlgebra.relalg]
tst [in RelationAlgebra.kat]
tst_BL [in RelationAlgebra.kat]


U

u [in RelationAlgebra.nfa]
u [in RelationAlgebra.dfa]
univalent [in RelationAlgebra.relalg]


V

v [in RelationAlgebra.nfa]
v [in RelationAlgebra.dfa]
val [in RelationAlgebra.syntax]
vars [in RelationAlgebra.dfa]
vector [in RelationAlgebra.relalg]
vio [in RelationAlgebra.paterson]
v1 [in RelationAlgebra.paterson]
v2 [in RelationAlgebra.paterson]
v3 [in RelationAlgebra.paterson]
v4 [in RelationAlgebra.paterson]


W

weq [in RelationAlgebra.lattice]
weq_spec [in RelationAlgebra.lattice]



Instance Index

A

antisymmetric_cnv [in RelationAlgebra.relalg]
atom_transitive [in RelationAlgebra.relalg]
atom_cnv [in RelationAlgebra.relalg]
atom_univalent [in RelationAlgebra.relalg]
atom_injective [in RelationAlgebra.relalg]


B

blk_mx_weq [in RelationAlgebra.matrix]
blk_mx_leq [in RelationAlgebra.matrix]
bool_laws [in RelationAlgebra.boolean]
bool_lattice_laws [in RelationAlgebra.boolean]


C

cap_weq [in RelationAlgebra.lattice]
cap_leq [in RelationAlgebra.lattice]
cnv_weq [in RelationAlgebra.monoid]
col_mx_weq [in RelationAlgebra.matrix]
col_mx_leq [in RelationAlgebra.matrix]
cup_weq [in RelationAlgebra.lattice]
cup_leq [in RelationAlgebra.lattice]


D

derivs_weq [in RelationAlgebra.regex]
derivs_leq [in RelationAlgebra.regex]
deriv_weq [in RelationAlgebra.regex]
deriv_leq [in RelationAlgebra.regex]
deriv_mx_weq [in RelationAlgebra.rmx]
dot_weq [in RelationAlgebra.monoid]
dot_leq [in RelationAlgebra.monoid]


E

epsilon_weq [in RelationAlgebra.regex]
epsilon_leq [in RelationAlgebra.regex]
epsilon_mx_weq [in RelationAlgebra.rmx]
expr_lattice_laws [in RelationAlgebra.paterson]
expr_laws [in RelationAlgebra.syntax]
expr_lattice_laws [in RelationAlgebra.syntax]
expr_laws [in RelationAlgebra.lsyntax]


F

frel_weq [in RelationAlgebra.rel]


G

glang_kat_laws [in RelationAlgebra.glang]
gl_weq [in RelationAlgebra.kat_completeness]
gl_leq [in RelationAlgebra.kat_completeness]
gregex_kat_laws [in RelationAlgebra.gregex]
gregex_monoid_laws [in RelationAlgebra.gregex]
gregex_lattice_laws [in RelationAlgebra.gregex]


I

inf_leq [in RelationAlgebra.sups]
injective_cnv [in RelationAlgebra.relalg]
inj_weq [in RelationAlgebra.kat]
inj_leq [in RelationAlgebra.kat]
irreflexive_cnv [in RelationAlgebra.relalg]
is_symmetric_neg1 [in RelationAlgebra.relalg]
is_order_weq [in RelationAlgebra.relalg]
is_preorder_weq [in RelationAlgebra.relalg]
is_per_weq [in RelationAlgebra.relalg]
is_mapping_weq [in RelationAlgebra.relalg]
is_atom_weq [in RelationAlgebra.relalg]
is_point_weq [in RelationAlgebra.relalg]
is_nonempty_weq [in RelationAlgebra.relalg]
is_vector_weq [in RelationAlgebra.relalg]
is_total_weq [in RelationAlgebra.relalg]
is_surjective_weq [in RelationAlgebra.relalg]
is_injective_weq [in RelationAlgebra.relalg]
is_univalent_weq [in RelationAlgebra.relalg]
is_antisymmetric_weq [in RelationAlgebra.relalg]
is_symmetric_weq [in RelationAlgebra.relalg]
is_linear_weq [in RelationAlgebra.relalg]
is_transitive_weq [in RelationAlgebra.relalg]
is_irreflexive_weq [in RelationAlgebra.relalg]
is_reflexive_weq [in RelationAlgebra.relalg]
is_true_leq [in RelationAlgebra.boolean]
itr_weq [in RelationAlgebra.kleene]
itr_leq [in RelationAlgebra.kleene]


L

lang_laws [in RelationAlgebra.lang]
lang_lattice_laws [in RelationAlgebra.lang]
lang_weq [in RelationAlgebra.ugregex]
lang_leq [in RelationAlgebra.ugregex]
lang_weq' [in RelationAlgebra.nfa]
lang_weq [in RelationAlgebra.nfa]
lang_leq [in RelationAlgebra.nfa]
lang_weq [in RelationAlgebra.regex]
lang_leq [in RelationAlgebra.regex]
lang_weq [in RelationAlgebra.gregex]
lang_leq [in RelationAlgebra.gregex]
ldv_weq [in RelationAlgebra.monoid]
ldv_leq [in RelationAlgebra.monoid]
leq_Transitive [in RelationAlgebra.lattice]
leq_Reflexive [in RelationAlgebra.lattice]
leq_weq_iff [in RelationAlgebra.lattice]
lower_trans [in RelationAlgebra.level]
lower_refl [in RelationAlgebra.level]
lset_laws [in RelationAlgebra.lset]


M

mapping_cnv [in RelationAlgebra.relalg]
map_compat [in RelationAlgebra.lset]
map_weq [in RelationAlgebra.lset]
map_leq [in RelationAlgebra.lset]
merge_lower [in RelationAlgebra.level]
mm_bool_Prop [in RelationAlgebra.boolean]
mx_map_weq [in RelationAlgebra.matrix_ext]
mx_map_leq [in RelationAlgebra.matrix_ext]
mx_bka_laws [in RelationAlgebra.matrix_ext]
mx_scal_weq [in RelationAlgebra.matrix_ext]
mx_scal_leq [in RelationAlgebra.matrix_ext]
mx_laws [in RelationAlgebra.matrix]
mx_bsl_laws [in RelationAlgebra.matrix]
mx_lattice_laws [in RelationAlgebra.matrix]


N

neg_weq [in RelationAlgebra.lattice]
neg_leq [in RelationAlgebra.lattice]
nonempty_cnv [in RelationAlgebra.relalg]


O

ofbool_leq [in RelationAlgebra.boolean]
order_cnv [in RelationAlgebra.relalg]


P

point_surjective [in RelationAlgebra.relalg]
preorder_str [in RelationAlgebra.relalg]
preorder_cnv [in RelationAlgebra.relalg]
prog_kat_laws [in RelationAlgebra.paterson]
prog_lattice_laws [in RelationAlgebra.paterson]
prog_monoid_laws [in RelationAlgebra.paterson]
Prop_lattice_laws [in RelationAlgebra.prop]
pw_laws [in RelationAlgebra.lattice]


R

rdv_weq [in RelationAlgebra.monoid]
rdv_leq [in RelationAlgebra.monoid]
reflexive_itr [in RelationAlgebra.relalg]
reflexive_cnv [in RelationAlgebra.relalg]
regex_lattice_laws [in RelationAlgebra.regex]
regex_laws [in RelationAlgebra.regex]
rel_kat_laws [in RelationAlgebra.rel]
rel_monoid_laws [in RelationAlgebra.rel]
rel_lattice_laws [in RelationAlgebra.rel]
restrict_weq [in RelationAlgebra.traces]
restrict_leq [in RelationAlgebra.traces]
rmx_laws [in RelationAlgebra.rmx]
rmx_lattice_laws [in RelationAlgebra.rmx]
row_mx_weq [in RelationAlgebra.matrix]
row_mx_leq [in RelationAlgebra.matrix]


S

scal_mx_weq [in RelationAlgebra.matrix_ext]
scal_mx_leq [in RelationAlgebra.matrix_ext]
str_weq [in RelationAlgebra.monoid]
str_leq [in RelationAlgebra.monoid]
sup_weq [in RelationAlgebra.sups]
sup_leq [in RelationAlgebra.sups]
surjective_cnv [in RelationAlgebra.relalg]
symmetric_itr [in RelationAlgebra.relalg]
symmetric_str [in RelationAlgebra.relalg]
symmetric_cnv [in RelationAlgebra.relalg]


T

tglang_kat_laws [in RelationAlgebra.glang]
total_cnv [in RelationAlgebra.relalg]
traces_monoid_laws [in RelationAlgebra.traces]
traces_lattice_laws [in RelationAlgebra.traces]
transitive_itr [in RelationAlgebra.relalg]
transitive_cnv [in RelationAlgebra.relalg]
ttraces_monoid_laws [in RelationAlgebra.traces]
ttraces_lattice_laws [in RelationAlgebra.traces]


U

ugregex_lattice_laws [in RelationAlgebra.ugregex]
ugregex_monoid_laws [in RelationAlgebra.ugregex]
univalent_cnv [in RelationAlgebra.relalg]
u_laws [in RelationAlgebra.untyping]
u_lattice_laws [in RelationAlgebra.untyping]


V

vector_cap [in RelationAlgebra.relalg]


W

weq_Symmetric [in RelationAlgebra.lattice]
weq_Transitive [in RelationAlgebra.lattice]
weq_Reflexive [in RelationAlgebra.lattice]
weq_geq [in RelationAlgebra.lattice]
weq_leq [in RelationAlgebra.lattice]
weq_Equivalence [in RelationAlgebra.lattice]



Section Index

A

atom_props [in RelationAlgebra.atoms]


B

bsl [in RelationAlgebra.matrix]


C

cbsl [in RelationAlgebra.matrix]
clean [in RelationAlgebra.untyping]


D

d [in RelationAlgebra.matrix]
det [in RelationAlgebra.ka_completeness]
diff [in RelationAlgebra.dfa]


E

E [in RelationAlgebra.ka_completeness]
e [in RelationAlgebra.untyping]
e [in RelationAlgebra.positives]
empty_dec [in RelationAlgebra.dfa]
expr_cmp [in RelationAlgebra.syntax]
expr_cmp [in RelationAlgebra.lsyntax]
e.l [in RelationAlgebra.untyping]


H

h [in RelationAlgebra.matrix_ext]


I

i [in RelationAlgebra.rel]
inf [in RelationAlgebra.sups]


J

j [in RelationAlgebra.kat_tac]


K

ka [in RelationAlgebra.matrix]
ka.build [in RelationAlgebra.matrix]


L

l [in RelationAlgebra.lang]
l [in RelationAlgebra.ugregex]
l [in RelationAlgebra.comparisons]
l [in RelationAlgebra.traces]
l [in RelationAlgebra.ugregex_dec]
levels [in RelationAlgebra.level]
l.a [in RelationAlgebra.ugregex_dec]
l.l [in RelationAlgebra.traces]


M

m [in RelationAlgebra.lset]
m [in RelationAlgebra.matrix]


N

n [in RelationAlgebra.normalisation]


O

ofbool [in RelationAlgebra.boolean]


P

p [in RelationAlgebra.comparisons]
powerfix [in RelationAlgebra.powerfix]
powerfix.invariant [in RelationAlgebra.powerfix]
powerfix.linear_carac [in RelationAlgebra.powerfix]
props [in RelationAlgebra.relalg]


S

s [in RelationAlgebra.paterson]
s [in RelationAlgebra.kat_completeness]
s [in RelationAlgebra.kat_reification]
s [in RelationAlgebra.comparisons]
s [in RelationAlgebra.kat_untyping]
s [in RelationAlgebra.kat]
s [in RelationAlgebra.syntax]
s [in RelationAlgebra.lsyntax]
s [in RelationAlgebra.gregex]
s [in RelationAlgebra.imp]
s [in RelationAlgebra.glang]
s [in RelationAlgebra.sups]
s.e [in RelationAlgebra.kat_reification]
s.e [in RelationAlgebra.syntax]
s.e [in RelationAlgebra.lsyntax]
s.e [in RelationAlgebra.gregex]
s.i [in RelationAlgebra.sups]
s.l [in RelationAlgebra.syntax]
s.l [in RelationAlgebra.lsyntax]
s.n [in RelationAlgebra.kat_completeness]



Abbreviation Index

A

Atom [in RelationAlgebra.ugregex]
Atom [in RelationAlgebra.kat_completeness]
Atom [in RelationAlgebra.kat_untyping]
Atom [in RelationAlgebra.atoms]
Atom [in RelationAlgebra.gregex]
Atom [in RelationAlgebra.glang]
Atom [in RelationAlgebra.ugregex_dec]


B

bmx [in RelationAlgebra.bmx]
bool' [in RelationAlgebra.boolean]


D

del [in RelationAlgebra.paterson]
deriv_mx [in RelationAlgebra.rmx]


E

elang [in RelationAlgebra.regex]
eps [in RelationAlgebra.regex]
expr [in RelationAlgebra.normalisation]
expr [in RelationAlgebra.syntax]
expr [in RelationAlgebra.untyping]
expr [in RelationAlgebra.untyping]
expr_ [in RelationAlgebra.syntax]
expr_ [in RelationAlgebra.lsyntax]
expr3 [in RelationAlgebra.kat_completeness]


F

flip [in RelationAlgebra.common]
Fun [in RelationAlgebra.powerfix]


G

G [in RelationAlgebra.kat_completeness]
glang [in RelationAlgebra.kat_completeness]
glang [in RelationAlgebra.kat_untyping]
glang [in RelationAlgebra.gregex]
gregex [in RelationAlgebra.kat_completeness]
gregex [in RelationAlgebra.kat_untyping]
guards [in RelationAlgebra.kat_completeness]
gword [in RelationAlgebra.kat_completeness]
g_atom [in RelationAlgebra.kat_completeness]
g_atom [in RelationAlgebra.gregex]


H

Hoare [in RelationAlgebra.imp]


I

I [in RelationAlgebra.syntax]
I [in RelationAlgebra.syntax]
I [in RelationAlgebra.gregex]
Idx [in RelationAlgebra.kat_reification]
impl [in RelationAlgebra.common]
inf [in RelationAlgebra.sups]
is_nonempty' [in RelationAlgebra.relalg]
is_pure_mx [in RelationAlgebra.rmx]
is_simple_mx [in RelationAlgebra.rmx]
is_01_mx [in RelationAlgebra.rmx]


L

lang [in RelationAlgebra.kat_completeness]
lang [in RelationAlgebra.ugregex_dec]
lang' [in RelationAlgebra.lang]
lang' [in RelationAlgebra.lang]
latom [in RelationAlgebra.kat_completeness]
lex [in RelationAlgebra.comparisons]


M

M [in RelationAlgebra.ka_completeness]
mx [in RelationAlgebra.matrix]
mx [in RelationAlgebra.matrix]
mx [in RelationAlgebra.matrix]
mx [in RelationAlgebra.matrix]
mx [in RelationAlgebra.matrix]


N

n [in RelationAlgebra.ka_completeness]


O

ofbool [in RelationAlgebra.boolean]


P

Pred [in RelationAlgebra.kat_reification]
pred [in RelationAlgebra.kat_untyping]
prog' [in RelationAlgebra.paterson]
pwr [in RelationAlgebra.common]


R

R [in RelationAlgebra.kat_completeness]
regex' [in RelationAlgebra.regex]
rel_empty [in RelationAlgebra.ugregex_dec]
rel_insert [in RelationAlgebra.ugregex_dec]
restrict [in RelationAlgebra.kat_untyping]
rmx [in RelationAlgebra.rmx]


S

s [in RelationAlgebra.matrix]
Sigma [in RelationAlgebra.ugregex]
Sigma [in RelationAlgebra.kat_completeness]
Sigma [in RelationAlgebra.kat_reification]
Sigma [in RelationAlgebra.kat_untyping]
Sigma [in RelationAlgebra.traces]
Sigma [in RelationAlgebra.gregex]
Sigma [in RelationAlgebra.glang]
Sigma [in RelationAlgebra.kat_tac]
Sigma [in RelationAlgebra.ugregex_dec]


T

test [in RelationAlgebra.paterson]
test [in RelationAlgebra.kat_completeness]
teval [in RelationAlgebra.kat_completeness]
tod [in RelationAlgebra.ugregex_dec]
top [in RelationAlgebra.syntax]
top' [in RelationAlgebra.monoid]
traces' [in RelationAlgebra.traces]
traces' [in RelationAlgebra.traces]
tt [in RelationAlgebra.lang]
tt [in RelationAlgebra.ugregex]
tt [in RelationAlgebra.traces]
tt [in RelationAlgebra.ugregex_dec]
ttraces' [in RelationAlgebra.traces]
typed [in RelationAlgebra.kat_untyping]


U

u [in RelationAlgebra.ka_completeness]
U [in RelationAlgebra.matrix]
U [in RelationAlgebra.matrix]
U [in RelationAlgebra.matrix]
U [in RelationAlgebra.matrix]
uexpr [in RelationAlgebra.untyping]
uexpr3 [in RelationAlgebra.kat_completeness]
uglang [in RelationAlgebra.ugregex]
uglang [in RelationAlgebra.kat_untyping]
uglang [in RelationAlgebra.ugregex_dec]
ugregex [in RelationAlgebra.kat_untyping]
ugregex [in RelationAlgebra.ugregex_dec]
ugregex' [in RelationAlgebra.ugregex]
upd [in RelationAlgebra.paterson]
upd [in RelationAlgebra.imp]


V

v [in RelationAlgebra.ka_completeness]
vars [in RelationAlgebra.ka_completeness]


W

word [in RelationAlgebra.kat_completeness]


Z

zer [in RelationAlgebra.monoid]



Definition Index

A

AA [in RelationAlgebra.level]
aff [in RelationAlgebra.paterson]
AL [in RelationAlgebra.level]
apply [in RelationAlgebra.common]
assert_false [in RelationAlgebra.common]
atom [in RelationAlgebra.atoms]
atom_to_word [in RelationAlgebra.kat_completeness]


B

BDL [in RelationAlgebra.level]
below_I [in RelationAlgebra.ugregex_dec]
BKA [in RelationAlgebra.level]
bka_to_kat.ops [in RelationAlgebra.kat_tac]
BL [in RelationAlgebra.level]
blk_mx [in RelationAlgebra.matrix]
bmx_str [in RelationAlgebra.bmx]
bool_of_sumbool [in RelationAlgebra.common]
bool_compare [in RelationAlgebra.comparisons]
bool_ops [in RelationAlgebra.boolean]
bool_lattice_ops [in RelationAlgebra.boolean]
BOT [in RelationAlgebra.level]
BSL [in RelationAlgebra.level]
bstep [in RelationAlgebra.paterson]
bstep [in RelationAlgebra.imp]
bsub_mx [in RelationAlgebra.matrix]


C

CAP [in RelationAlgebra.level]
cap' [in RelationAlgebra.normalisation]
cast [in RelationAlgebra.syntax]
CKA [in RelationAlgebra.level]
clean [in RelationAlgebra.kat_completeness]
clean [in RelationAlgebra.untyping]
clean1 [in RelationAlgebra.kat_completeness]
cmp_letter [in RelationAlgebra.kat_completeness]
cmp_list [in RelationAlgebra.comparisons]
cmp_sum [in RelationAlgebra.comparisons]
cmp_pair [in RelationAlgebra.comparisons]
cmp_bool [in RelationAlgebra.comparisons]
cmp_nat [in RelationAlgebra.comparisons]
cmp_id [in RelationAlgebra.comparisons]
cmp_ord [in RelationAlgebra.ordinal]
cmp_expr [in RelationAlgebra.syntax]
cmp_expr [in RelationAlgebra.lsyntax]
cmp_pos [in RelationAlgebra.positives]
CNV [in RelationAlgebra.level]
cnv' [in RelationAlgebra.normalisation]
col_mx [in RelationAlgebra.matrix]
compare_letter [in RelationAlgebra.kat_completeness]
CUP [in RelationAlgebra.level]


D

DAL [in RelationAlgebra.level]
deriv [in RelationAlgebra.ugregex]
deriv [in RelationAlgebra.regex]
derivs [in RelationAlgebra.regex]
det [in RelationAlgebra.ka_completeness]
dfa [in RelationAlgebra.ka_completeness]
dfa.to_nfa [in RelationAlgebra.nfa]
diff [in RelationAlgebra.dfa]
dirac [in RelationAlgebra.kat_completeness]
DIV [in RelationAlgebra.level]
DL [in RelationAlgebra.level]
dont_read [in RelationAlgebra.paterson]
dot_r [in RelationAlgebra.normalisation]
dot_l [in RelationAlgebra.normalisation]
dot' [in RelationAlgebra.normalisation]
double [in RelationAlgebra.common]
dset [in RelationAlgebra.rel]
dual [in RelationAlgebra.lattice]
dual [in RelationAlgebra.monoid]
dual [in RelationAlgebra.kat]
dual [in RelationAlgebra.level]


E

empty [in RelationAlgebra.dfa]
epsilon [in RelationAlgebra.ugregex]
epsilon [in RelationAlgebra.regex]
epsilon_pred [in RelationAlgebra.ugregex]
epsilon_mx [in RelationAlgebra.rmx]
epsilon' [in RelationAlgebra.ugregex_dec]
eqb [in RelationAlgebra.paterson]
eqb_list [in RelationAlgebra.comparisons]
eqb_sum [in RelationAlgebra.comparisons]
eqb_pair [in RelationAlgebra.comparisons]
eqb_bool [in RelationAlgebra.comparisons]
eqb_nat [in RelationAlgebra.comparisons]
eqb_of_compare [in RelationAlgebra.comparisons]
eqb_ord [in RelationAlgebra.ordinal]
eqb_pos [in RelationAlgebra.positives]
eqb_kat [in RelationAlgebra.ugregex_dec]
erase [in RelationAlgebra.untyping]
esubst [in RelationAlgebra.imp]
eval [in RelationAlgebra.paterson]
eval [in RelationAlgebra.kat_reification]
eval [in RelationAlgebra.nfa]
eval [in RelationAlgebra.syntax]
eval [in RelationAlgebra.lsyntax]
eval [in RelationAlgebra.gregex]
expr_lattice_ops [in RelationAlgebra.paterson]
expr_leq_or_weq [in RelationAlgebra.normalisation]
expr_leq [in RelationAlgebra.normalisation]
expr_compare_ [in RelationAlgebra.syntax]
expr_compare [in RelationAlgebra.syntax]
expr_ops [in RelationAlgebra.syntax]
expr_lattice_ops [in RelationAlgebra.syntax]
expr_compare [in RelationAlgebra.lsyntax]
expr_ops [in RelationAlgebra.lsyntax]
expr_ind [in RelationAlgebra.untyping]
e_var [in RelationAlgebra.kat_reification]
e_inj [in RelationAlgebra.kat_reification]
e_top' [in RelationAlgebra.atoms]
e_weq [in RelationAlgebra.syntax]
e_leq [in RelationAlgebra.syntax]
e_level [in RelationAlgebra.syntax]
e_weq [in RelationAlgebra.lsyntax]
e_leq [in RelationAlgebra.lsyntax]
e_level [in RelationAlgebra.lsyntax]
e_cnv' [in RelationAlgebra.untyping]
e_str' [in RelationAlgebra.untyping]
e_itr' [in RelationAlgebra.untyping]
e_dot' [in RelationAlgebra.untyping]
e_pls' [in RelationAlgebra.untyping]


F

Fix.lset_ops [in RelationAlgebra.lset]
free [in RelationAlgebra.paterson]
frel [in RelationAlgebra.rel]
fresh [in RelationAlgebra.imp]
fst [in RelationAlgebra.kat_completeness]


G

gc [in RelationAlgebra.paterson]
gerase [in RelationAlgebra.kat_untyping]
get [in RelationAlgebra.paterson]
get_ord [in RelationAlgebra.denum]
get_nat [in RelationAlgebra.denum]
get_pair [in RelationAlgebra.denum]
get_sum [in RelationAlgebra.denum]
geval [in RelationAlgebra.kat_completeness]
gl [in RelationAlgebra.kat_completeness]
glang_kat_ops [in RelationAlgebra.glang]
glang_inj [in RelationAlgebra.glang]
gregex_kat_ops [in RelationAlgebra.gregex]
gregex_monoid_ops [in RelationAlgebra.gregex]
gregex_lattice_ops [in RelationAlgebra.gregex]
gword_to_word' [in RelationAlgebra.kat_completeness]
gword_to_word [in RelationAlgebra.kat_completeness]
g_str' [in RelationAlgebra.kat_completeness]
g_inner_dot [in RelationAlgebra.kat_completeness]
g_dot' [in RelationAlgebra.kat_completeness]
g_dot1 [in RelationAlgebra.kat_completeness]
g_var' [in RelationAlgebra.kat_completeness]
g_one' [in RelationAlgebra.kat_completeness]
g_prd' [in RelationAlgebra.kat_completeness]
g_weq [in RelationAlgebra.gregex]
g_leq [in RelationAlgebra.gregex]
g_str [in RelationAlgebra.gregex]
g_one [in RelationAlgebra.gregex]


H

hat [in RelationAlgebra.kat_completeness]


I

idx [in RelationAlgebra.kat_reification]
inj_leq [in RelationAlgebra.gregex]
inj_weq [in RelationAlgebra.gregex]
inj_top [in RelationAlgebra.gregex]
inj_cap [in RelationAlgebra.gregex]
inj_bot [in RelationAlgebra.gregex]
inj_cup [in RelationAlgebra.gregex]
insert [in RelationAlgebra.lset]
insert_pls [in RelationAlgebra.normalisation]
is_enfa [in RelationAlgebra.nfa]
is_nfa [in RelationAlgebra.nfa]
is_top [in RelationAlgebra.syntax]
is_zer [in RelationAlgebra.syntax]
is_clean [in RelationAlgebra.untyping]
iter [in RelationAlgebra.lang]
iter [in RelationAlgebra.rel]
itr' [in RelationAlgebra.normalisation]


K

KA [in RelationAlgebra.level]
kat_expr [in RelationAlgebra.kat_reification]


L

lang [in RelationAlgebra.lang]
lang [in RelationAlgebra.ugregex]
lang [in RelationAlgebra.nfa]
lang [in RelationAlgebra.regex]
lang [in RelationAlgebra.gregex]
lang [in RelationAlgebra.dfa]
lang_deriv [in RelationAlgebra.lang]
lang_ops [in RelationAlgebra.lang]
lang_str [in RelationAlgebra.lang]
lang_itr [in RelationAlgebra.lang]
lang_cnv [in RelationAlgebra.lang]
lang_one [in RelationAlgebra.lang]
lang_rdv [in RelationAlgebra.lang]
lang_ldv [in RelationAlgebra.lang]
lang_dot [in RelationAlgebra.lang]
lang_lattice_ops [in RelationAlgebra.lang]
lang' [in RelationAlgebra.ugregex]
leq_or_weq [in RelationAlgebra.lattice]
le_bool [in RelationAlgebra.common]
linearfix [in RelationAlgebra.powerfix]
list_compare [in RelationAlgebra.comparisons]
loop [in RelationAlgebra.ugregex_dec]
loop_aux [in RelationAlgebra.ugregex_dec]
lp [in RelationAlgebra.kat_completeness]
lset_ops [in RelationAlgebra.lset]
lset_ops [in RelationAlgebra.matrix]
lshift [in RelationAlgebra.ordinal]
lst [in RelationAlgebra.kat_completeness]
lsub_mx [in RelationAlgebra.matrix]
ltb [in RelationAlgebra.ordinal]
lt_ge_dec [in RelationAlgebra.ordinal]


M

merge [in RelationAlgebra.level]
MIN [in RelationAlgebra.level]
mk [in RelationAlgebra.pair]
mk_ord [in RelationAlgebra.denum]
mk_nat [in RelationAlgebra.denum]
mk_pair [in RelationAlgebra.denum]
mk_sum [in RelationAlgebra.denum]
mk_simple_cmp [in RelationAlgebra.comparisons]
Ms [in RelationAlgebra.dfa]
mx [in RelationAlgebra.matrix]
mx_fun [in RelationAlgebra.matrix_ext]
mx_map [in RelationAlgebra.matrix_ext]
mx_level [in RelationAlgebra.matrix]
mx_ops [in RelationAlgebra.matrix]
mx_itr [in RelationAlgebra.matrix]
mx_str [in RelationAlgebra.matrix]
mx_str_build [in RelationAlgebra.matrix]
mx_cnv [in RelationAlgebra.matrix]
mx_rdv [in RelationAlgebra.matrix]
mx_ldv [in RelationAlgebra.matrix]
mx_dot [in RelationAlgebra.matrix]
mx_one [in RelationAlgebra.matrix]
mx_scal [in RelationAlgebra.matrix]
mx_lattice_ops [in RelationAlgebra.matrix]
mx_forall [in RelationAlgebra.rmx]
mx_vars [in RelationAlgebra.rmx]


N

nat_compare [in RelationAlgebra.comparisons]
NEG [in RelationAlgebra.level]
nfa [in RelationAlgebra.ka_completeness]
norm [in RelationAlgebra.normalisation]


O

o [in RelationAlgebra.kat_completeness]
obind [in RelationAlgebra.ugregex_dec]
ofbool [in RelationAlgebra.monoid]
ofold [in RelationAlgebra.ugregex_dec]
of_row [in RelationAlgebra.rmx]
ordS [in RelationAlgebra.ordinal]
ord_compare [in RelationAlgebra.ordinal]
ord0 [in RelationAlgebra.ordinal]
o_npred [in RelationAlgebra.kat_completeness]
o_pred [in RelationAlgebra.kat_completeness]
o' [in RelationAlgebra.kat_completeness]


P

packed_eval [in RelationAlgebra.syntax]
pair_compare [in RelationAlgebra.comparisons]
pderiv [in RelationAlgebra.ugregex_dec]
pderiv' [in RelationAlgebra.ugregex_dec]
pi1 [in RelationAlgebra.pair]
pi2 [in RelationAlgebra.pair]
pl [in RelationAlgebra.kat_completeness]
pls' [in RelationAlgebra.normalisation]
pos_compare [in RelationAlgebra.positives]
powerfix [in RelationAlgebra.powerfix]
powerfix' [in RelationAlgebra.powerfix]
pow2 [in RelationAlgebra.common]
prog [in RelationAlgebra.ugregex_dec]
prog_kat_ops [in RelationAlgebra.paterson]
prog_monoid_ops [in RelationAlgebra.paterson]
prog_lattice_ops [in RelationAlgebra.paterson]
Prop_lattice_ops [in RelationAlgebra.prop]
pure_part [in RelationAlgebra.regex]
pure_part_mx [in RelationAlgebra.rmx]
pw_ops [in RelationAlgebra.lattice]
pw0 [in RelationAlgebra.lattice]
pw1 [in RelationAlgebra.lattice]
pw2 [in RelationAlgebra.lattice]
p_var [in RelationAlgebra.kat_reification]


R

R [in RelationAlgebra.ka_completeness]
regex_ops [in RelationAlgebra.regex]
regex_lattice_ops [in RelationAlgebra.regex]
rel [in RelationAlgebra.rel]
rel_kat_ops [in RelationAlgebra.rel]
rel_inj [in RelationAlgebra.rel]
rel_monoid_ops [in RelationAlgebra.rel]
rel_itr [in RelationAlgebra.rel]
rel_str [in RelationAlgebra.rel]
rel_rdv [in RelationAlgebra.rel]
rel_ldv [in RelationAlgebra.rel]
rel_cnv [in RelationAlgebra.rel]
rel_dot [in RelationAlgebra.rel]
rel_lattice_ops [in RelationAlgebra.rel]
rel_mem [in RelationAlgebra.ugregex_dec]
remove [in RelationAlgebra.normalisation]
reroot [in RelationAlgebra.dfa]
restrict [in RelationAlgebra.traces]
rev [in RelationAlgebra.traces]
re_ind [in RelationAlgebra.regex]
row_mx [in RelationAlgebra.matrix]
rshift [in RelationAlgebra.ordinal]
rsub_mx [in RelationAlgebra.matrix]
r_weq [in RelationAlgebra.regex]
r_leq [in RelationAlgebra.regex]
r_itr [in RelationAlgebra.regex]


S

scal_mx [in RelationAlgebra.matrix]
seq [in RelationAlgebra.ordinal]
set [in RelationAlgebra.paterson]
set.app' [in RelationAlgebra.ordinal]
set.mem [in RelationAlgebra.ordinal]
set.mem' [in RelationAlgebra.ordinal]
set.od [in RelationAlgebra.ordinal]
set.of_fun [in RelationAlgebra.ordinal]
set.of_fun' [in RelationAlgebra.ordinal]
set.xI [in RelationAlgebra.ordinal]
set.xI' [in RelationAlgebra.ordinal]
set.xO [in RelationAlgebra.ordinal]
set.xO' [in RelationAlgebra.ordinal]
sigma [in RelationAlgebra.regex]
sigma_add [in RelationAlgebra.positives]
sigma_get [in RelationAlgebra.positives]
SL [in RelationAlgebra.level]
split [in RelationAlgebra.ordinal]
src_ [in RelationAlgebra.syntax]
src' [in RelationAlgebra.kat_completeness]
step [in RelationAlgebra.dfa]
steps [in RelationAlgebra.dfa]
STR [in RelationAlgebra.level]
str' [in RelationAlgebra.normalisation]
subst [in RelationAlgebra.paterson]
subst [in RelationAlgebra.imp]
sub00_mx [in RelationAlgebra.matrix]
sub01_mx [in RelationAlgebra.matrix]
sub10_mx [in RelationAlgebra.matrix]
sub11_mx [in RelationAlgebra.matrix]
sum_compare [in RelationAlgebra.comparisons]
sup [in RelationAlgebra.sups]
s' [in RelationAlgebra.kat_reification]


T

tatom [in RelationAlgebra.traces]
tglang_kat_ops [in RelationAlgebra.glang]
tglang_inj [in RelationAlgebra.glang]
tgt_ [in RelationAlgebra.syntax]
tgt' [in RelationAlgebra.kat_completeness]
thead [in RelationAlgebra.traces]
Thompson.cst [in RelationAlgebra.ka_completeness]
Thompson.dot [in RelationAlgebra.ka_completeness]
Thompson.enfa [in RelationAlgebra.ka_completeness]
Thompson.itr [in RelationAlgebra.ka_completeness]
Thompson.one [in RelationAlgebra.ka_completeness]
Thompson.pls [in RelationAlgebra.ka_completeness]
Thompson.str [in RelationAlgebra.ka_completeness]
Thompson.zer [in RelationAlgebra.ka_completeness]
tinj [in RelationAlgebra.traces]
TOP [in RelationAlgebra.level]
to_gregex [in RelationAlgebra.kat_reification]
to_expr [in RelationAlgebra.regex]
to_row [in RelationAlgebra.rmx]
traces [in RelationAlgebra.traces]
traces_deriv [in RelationAlgebra.traces]
traces_monoid_ops [in RelationAlgebra.traces]
traces_str [in RelationAlgebra.traces]
traces_itr [in RelationAlgebra.traces]
traces_iter [in RelationAlgebra.traces]
traces_cnv [in RelationAlgebra.traces]
traces_one [in RelationAlgebra.traces]
traces_rdv [in RelationAlgebra.traces]
traces_ldv [in RelationAlgebra.traces]
traces_dot [in RelationAlgebra.traces]
traces_lattice_ops [in RelationAlgebra.traces]
transfers [in RelationAlgebra.matrix]
tsingle [in RelationAlgebra.traces]
tsingle' [in RelationAlgebra.traces]
tsnoc [in RelationAlgebra.traces]
tsub_mx [in RelationAlgebra.matrix]
ttail [in RelationAlgebra.traces]
ttinj [in RelationAlgebra.traces]
ttraces [in RelationAlgebra.traces]
ttraces_monoid_ops [in RelationAlgebra.traces]
ttraces_str [in RelationAlgebra.traces]
ttraces_itr [in RelationAlgebra.traces]
ttraces_iter [in RelationAlgebra.traces]
ttraces_cnv [in RelationAlgebra.traces]
ttraces_one [in RelationAlgebra.traces]
ttraces_rdv [in RelationAlgebra.traces]
ttraces_ldv [in RelationAlgebra.traces]
ttraces_dot [in RelationAlgebra.traces]
ttraces_lattice_ops [in RelationAlgebra.traces]
ttraces_top [in RelationAlgebra.traces]
ttraces_bot [in RelationAlgebra.traces]
ttraces_neg [in RelationAlgebra.traces]
ttraces_cap [in RelationAlgebra.traces]
ttraces_cup [in RelationAlgebra.traces]
ttraces_weq [in RelationAlgebra.traces]
ttraces_leq [in RelationAlgebra.traces]
ttsingle [in RelationAlgebra.traces]
typed' [in RelationAlgebra.traces]
t' [in RelationAlgebra.kat_reification]


U

ugregex_cmp [in RelationAlgebra.ugregex]
ugregex_compare [in RelationAlgebra.ugregex]
ugregex_monoid_ops [in RelationAlgebra.ugregex]
ugregex_lattice_ops [in RelationAlgebra.ugregex]
union [in RelationAlgebra.lset]
update [in RelationAlgebra.paterson]
u_weq [in RelationAlgebra.ugregex]
u_leq [in RelationAlgebra.ugregex]
u_str [in RelationAlgebra.ugregex]
u_one [in RelationAlgebra.ugregex]
u_zer [in RelationAlgebra.ugregex]
u_ops [in RelationAlgebra.untyping]
u_lattice_ops [in RelationAlgebra.untyping]
u_weq [in RelationAlgebra.untyping]
u_leq [in RelationAlgebra.untyping]


V

v [in RelationAlgebra.kat_completeness]
var [in RelationAlgebra.kat_reification]
var [in RelationAlgebra.regex]
vars [in RelationAlgebra.kat_reification]
vars [in RelationAlgebra.regex]
vars [in RelationAlgebra.lsyntax]
vars [in RelationAlgebra.ugregex_dec]
v_add [in RelationAlgebra.kat_reification]
v_get [in RelationAlgebra.kat_reification]


W

w [in RelationAlgebra.kat_completeness]


X

xitr [in RelationAlgebra.kat_completeness]
xpair [in RelationAlgebra.denum]



Record Index

C

cmpType [in RelationAlgebra.comparisons]


F

functor [in RelationAlgebra.monoid]


I

is_order [in RelationAlgebra.relalg]
is_preorder [in RelationAlgebra.relalg]
is_per [in RelationAlgebra.relalg]
is_mapping [in RelationAlgebra.relalg]
is_atom [in RelationAlgebra.relalg]
is_point [in RelationAlgebra.relalg]
is_vector [in RelationAlgebra.relalg]
is_total [in RelationAlgebra.relalg]
is_surjective [in RelationAlgebra.relalg]
is_injective [in RelationAlgebra.relalg]
is_univalent [in RelationAlgebra.relalg]
is_antisymmetric [in RelationAlgebra.relalg]
is_symmetric [in RelationAlgebra.relalg]
is_linear [in RelationAlgebra.relalg]
is_transitive [in RelationAlgebra.relalg]
is_irreflexive [in RelationAlgebra.relalg]
is_reflexive [in RelationAlgebra.relalg]
is_nonempty [in RelationAlgebra.relalg]


L

laws [in RelationAlgebra.lattice]
laws [in RelationAlgebra.monoid]
laws [in RelationAlgebra.kat]
level [in RelationAlgebra.level]
lower [in RelationAlgebra.level]


M

morphism [in RelationAlgebra.lattice]


O

ops [in RelationAlgebra.lattice]
ops [in RelationAlgebra.monoid]
ops [in RelationAlgebra.kat]
ord [in RelationAlgebra.ordinal]


P

Pack [in RelationAlgebra.syntax]


S

state [in RelationAlgebra.paterson]


T

t [in RelationAlgebra.nfa]
t [in RelationAlgebra.dfa]



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 (2173 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 (67 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 (7 entries)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (90 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 (48 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 (882 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 (144 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 (44 entries)
Projection 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 (127 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 (155 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 (57 entries)
Abbreviation 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 (110 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 (408 entries)
Record 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 (34 entries)

This page has been generated by coqdoc