| 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 | (2135 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 | (53 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 | (81 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 | (181 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 | (45 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 | (676 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 | (160 entries) |
| Axiom 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 | (55 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 | (28 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 | (139 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 | (110 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) |
| 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 | (97 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 | (315 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 | (40 entries) |
Global Index
A
add_cardinal [lemma, in ATBR.DKA_StateSetSets]add_classes_empty [lemma, in ATBR.DKA_StateSetSets]
add_classes [definition, in ATBR.DKA_StateSetSets]
add_valid [lemma, in ATBR.DKA_Epsilon]
add_continuation_4r [lemma, in ATBR.Monoid]
add_continuation_3r [lemma, in ATBR.Monoid]
add_continuation_2r [lemma, in ATBR.Monoid]
add_continuation_1r [lemma, in ATBR.Monoid]
add_continuation_4l [lemma, in ATBR.Monoid]
add_continuation_3l [lemma, in ATBR.Monoid]
add_continuation_2l [lemma, in ATBR.Monoid]
add_continuation_1l [lemma, in ATBR.Monoid]
add_continuationl [lemma, in ATBR.Monoid]
add_continuation_4 [lemma, in ATBR.Monoid]
add_continuation_3 [lemma, in ATBR.Monoid]
add_continuation_2 [lemma, in ATBR.Monoid]
add_continuation_1 [lemma, in ATBR.Monoid]
add_continuation [lemma, in ATBR.Monoid]
add_pair [definition, in ATBR.Utils_WF]
add_pair.T [variable, in ATBR.Utils_WF]
add_pair [section, in ATBR.Utils_WF]
add_lists_sameclass [lemma, in ATBR.DKA_DFA_Equiv]
add_lists_S [lemma, in ATBR.DKA_DFA_Equiv]
add_lists [definition, in ATBR.DKA_DFA_Equiv]
add_incr [lemma, in ATBR.DKA_DFA_Equiv]
Alg [section, in ATBR.DKA_Definitions]
Algebraic [module, in ATBR.DKA_Construction]
algebraic_rt_closure [lemma, in ATBR.DKA_Epsilon]
algebraic_correctness [lemma, in ATBR.DKA_Epsilon]
algebraic_lemmas [section, in ATBR.DKA_Epsilon]
Algebraic.add [definition, in ATBR.DKA_Construction]
Algebraic.add_zero [lemma, in ATBR.DKA_Construction]
Algebraic.add_plus [lemma, in ATBR.DKA_Construction]
Algebraic.add_comm [lemma, in ATBR.DKA_Construction]
Algebraic.add_compat [instance, in ATBR.DKA_Construction]
Algebraic.add_compat' [instance, in ATBR.DKA_Construction]
Algebraic.add_var [definition, in ATBR.DKA_Construction]
Algebraic.add_one [definition, in ATBR.DKA_Construction]
Algebraic.belong [abbreviation, in ATBR.DKA_Construction]
Algebraic.belong_build [lemma, in ATBR.DKA_Construction]
Algebraic.belong_add_var [lemma, in ATBR.DKA_Construction]
Algebraic.belong_add_one [lemma, in ATBR.DKA_Construction]
Algebraic.belong_add [lemma, in ATBR.DKA_Construction]
Algebraic.belong_incr' [lemma, in ATBR.DKA_Construction]
Algebraic.belong_incr [lemma, in ATBR.DKA_Construction]
Algebraic.build [definition, in ATBR.DKA_Construction]
Algebraic.build_correct [lemma, in ATBR.DKA_Construction]
Algebraic.build_add [lemma, in ATBR.DKA_Construction]
Algebraic.build_compat [instance, in ATBR.DKA_Construction]
Algebraic.construction_correct [lemma, in ATBR.DKA_Construction]
Algebraic.delta [projection, in ATBR.DKA_Construction]
Algebraic.empty [definition, in ATBR.DKA_Construction]
Algebraic.equal [inductive, in ATBR.DKA_Construction]
Algebraic.equal_equiv [instance, in ATBR.DKA_Construction]
Algebraic.equal_refl [constructor, in ATBR.DKA_Construction]
Algebraic.eval [definition, in ATBR.DKA_Construction]
Algebraic.eval_star [lemma, in ATBR.DKA_Construction]
Algebraic.eval_dot [lemma, in ATBR.DKA_Construction]
Algebraic.eval_master_theorem [lemma, in ATBR.DKA_Construction]
Algebraic.eval_select_block [lemma, in ATBR.DKA_Construction]
Algebraic.eval_compat [instance, in ATBR.DKA_Construction]
Algebraic.incr [definition, in ATBR.DKA_Construction]
Algebraic.incr_add [lemma, in ATBR.DKA_Construction]
Algebraic.incr_compat [instance, in ATBR.DKA_Construction]
Algebraic.mk [constructor, in ATBR.DKA_Construction]
Algebraic.pre_MAUT [record, in ATBR.DKA_Construction]
Algebraic.protect [section, in ATBR.DKA_Construction]
Algebraic.size [projection, in ATBR.DKA_Construction]
Algebraic.to_MAUT_compat [instance, in ATBR.DKA_Construction]
Algebraic.to_MAUT [definition, in ATBR.DKA_Construction]
Algebraic.X_to_MAUT [definition, in ATBR.DKA_Construction]
_ [=0=] _ [notation, in ATBR.DKA_Construction]
andb_true_iff [lemma, in ATBR.BoolView]
andb_false_iff [lemma, in ATBR.BoolView]
and_neutral_left [lemma, in ATBR.DKA_Merge]
apply [definition, in ATBR.Common]
approx [definition, in ATBR.DKA_Epsilon]
ATBR [library]
ATBR_Matrices [library]
a_star_a_leq_star_a [lemma, in ATBR.KleeneAlgebra]
a_star_a_leq_star_a_a [lemma, in ATBR.KleeneAlgebra]
a_leq_star_a [lemma, in ATBR.KleeneAlgebra]
B
below [abbreviation, in ATBR.DKA_Definitions]below_max_pi1 [lemma, in ATBR.DKA_Merge]
below_max_pi0 [lemma, in ATBR.DKA_Merge]
below0_empty [lemma, in ATBR.DKA_StateSetSets]
BoolView [library]
bool_prop_iff [lemma, in ATBR.BoolView]
bool_dec' [lemma, in ATBR.DKA_Epsilon]
bounded [lemma, in ATBR.DKA_Epsilon]
bounded [lemma, in ATBR.DKA_Determinisation]
bounded [lemma, in ATBR.DKA_Construction]
bounded_change_initial [lemma, in ATBR.DKA_DFA_Equiv]
bounded_word [definition, in ATBR.DKA_DFA_Language]
bounded_delta_set [lemma, in ATBR.DKA_Determinisation]
box [constructor, in ATBR.MxGraph]
box_compat [instance, in ATBR.MxGraph]
BubbleSort [lemma, in ATBR.ChurchRosser]
build_combine [definition, in ATBR.DKA_DFA_Equiv]
build_star_destruct_right [lemma, in ATBR.MxKleeneAlgebra]
build_star_destruct_left [lemma, in ATBR.MxKleeneAlgebra]
build_star_make_left [lemma, in ATBR.MxKleeneAlgebra]
build_store_correct [lemma, in ATBR.DKA_Determinisation]
build_store_spec [lemma, in ATBR.DKA_Determinisation]
build_store [definition, in ATBR.DKA_Determinisation]
build_max_label [lemma, in ATBR.DKA_Construction]
C
cardinal_domain [lemma, in ATBR.DKA_StateSetSets]card_pset [lemma, in ATBR.DKA_StateSetSets]
cfi_measure [projection, in ATBR.DKA_DFA_Equiv]
cfi_le [projection, in ATBR.DKA_DFA_Equiv]
cfi_prog [projection, in ATBR.DKA_DFA_Equiv]
ChurchRosser [definition, in ATBR.ChurchRosser_Points_vs_Algebraic]
ChurchRosser [library]
ChurchRosser_Points_vs_Algebraic [library]
CISR_SL [projection, in ATBR.Classes]
CISR_ISR [instance, in ATBR.Converse]
ci_sameclass [projection, in ATBR.DKA_DFA_Equiv]
ci_measure [projection, in ATBR.DKA_DFA_Equiv]
ci_le [projection, in ATBR.DKA_DFA_Equiv]
ci_prog [projection, in ATBR.DKA_DFA_Equiv]
CKA_CISR [projection, in ATBR.Classes]
CKA_KA [instance, in ATBR.Converse]
classes [definition, in ATBR.DKA_StateSetSets]
Classes [library]
classes_union_strict [lemma, in ATBR.DKA_StateSetSets]
classes_compat [lemma, in ATBR.DKA_StateSetSets]
clean [abbreviation, in ATBR.DecideKleeneAlgebra]
clean [abbreviation, in ATBR.DKA_CheckLabels]
cnl_cons [constructor, in ATBR.DKA_DFA_Equiv]
cnl_nil [constructor, in ATBR.DKA_DFA_Equiv]
collect [definition, in ATBR.DKA_CheckLabels]
collect_ssf [lemma, in ATBR.DKA_CheckLabels]
collect_ssf_remove [lemma, in ATBR.DKA_CheckLabels]
collect_idem [lemma, in ATBR.DKA_CheckLabels]
collect_com [lemma, in ATBR.DKA_CheckLabels]
collect_incr_1 [lemma, in ATBR.DKA_CheckLabels]
collect_incr_2 [lemma, in ATBR.DKA_CheckLabels]
collect_compat' [definition, in ATBR.DKA_CheckLabels]
collect_compat [instance, in ATBR.DKA_CheckLabels]
collect_max_label [lemma, in ATBR.DKA_Construction]
comb [definition, in ATBR.DKA_DFA_Equiv]
comb [section, in ATBR.DKA_DFA_Equiv]
combine_no_length [inductive, in ATBR.DKA_DFA_Equiv]
comb_aux [definition, in ATBR.DKA_DFA_Equiv]
_ +++ _ [notation, in ATBR.DKA_DFA_Equiv]
Common [library]
comm_iter_right [lemma, in ATBR.KleeneAlgebra]
comm_iter_left [lemma, in ATBR.KleeneAlgebra]
comp [definition, in ATBR.Model_StdRelations]
comp [definition, in ATBR.Common]
compare_spec_gt [constructor, in ATBR.BoolView]
compare_spec_eq [constructor, in ATBR.BoolView]
compare_spec_lt [constructor, in ATBR.BoolView]
compare_spec [inductive, in ATBR.BoolView]
compare_compat [lemma, in ATBR.DKA_Merge]
compare_DFAs [definition, in ATBR.DKA_Merge]
compare_sum_xif_zero [lemma, in ATBR.SemiLattice]
compat_negsplit [lemma, in ATBR.DKA_StateSetSets]
compat_split [lemma, in ATBR.DKA_StateSetSets]
complete [lemma, in ATBR.DKA_CheckLabels]
complete [definition, in ATBR.DKA_DFA_Equiv]
completeness [lemma, in ATBR.DKA_DFA_Equiv]
completeness [section, in ATBR.DKA_DFA_Equiv]
completeness.A [variable, in ATBR.DKA_DFA_Equiv]
completeness.HA [variable, in ATBR.DKA_DFA_Equiv]
completeness.Hi [variable, in ATBR.DKA_DFA_Equiv]
completeness.Hj [variable, in ATBR.DKA_DFA_Equiv]
completeness.i [variable, in ATBR.DKA_DFA_Equiv]
completeness.j [variable, in ATBR.DKA_DFA_Equiv]
complete_WF [instance, in ATBR.DKA_DFA_Equiv]
complete_compat_left [lemma, in ATBR.DKA_DFA_Equiv]
complete_incr_left [lemma, in ATBR.DKA_DFA_Equiv]
complete_incr [lemma, in ATBR.DKA_DFA_Equiv]
Concrete [section, in ATBR.Examples]
Concrete [module, in ATBR.DKA_Construction]
Concrete' [section, in ATBR.Examples]
Concrete'.A [variable, in ATBR.Examples]
Concrete'.R [variable, in ATBR.Examples]
Concrete'.S [variable, in ATBR.Examples]
Concrete.A [variable, in ATBR.Examples]
Concrete.add_var [definition, in ATBR.DKA_Construction]
Concrete.add_one [definition, in ATBR.DKA_Construction]
Concrete.augment [definition, in ATBR.DKA_Construction]
Concrete.augment_var [definition, in ATBR.DKA_Construction]
Concrete.build [definition, in ATBR.DKA_Construction]
Concrete.deltamap [projection, in ATBR.DKA_Construction]
Concrete.empty [definition, in ATBR.DKA_Construction]
Concrete.epsilonmap [projection, in ATBR.DKA_Construction]
Concrete.incr [definition, in ATBR.DKA_Construction]
Concrete.max_label [projection, in ATBR.DKA_Construction]
Concrete.mk [constructor, in ATBR.DKA_Construction]
Concrete.pre_eNFA [record, in ATBR.DKA_Construction]
Concrete.R [variable, in ATBR.Examples]
Concrete.S [variable, in ATBR.Examples]
Concrete.size [projection, in ATBR.DKA_Construction]
Concrete.X_to_eNFA [definition, in ATBR.DKA_Construction]
constant [definition, in ATBR.Examples]
contains_one_false_strict [lemma, in ATBR.StrictStarForm]
contains_one_correct [lemma, in ATBR.StrictStarForm]
contains_one [definition, in ATBR.StrictStarForm]
conv [projection, in ATBR.Classes]
Converse [library]
ConverseIdemSemiRing [record, in ATBR.Classes]
ConverseKleeneAlgebra [record, in ATBR.Classes]
Converse_Op [record, in ATBR.Classes]
conv_plus [projection, in ATBR.Classes]
conv_dot [projection, in ATBR.Classes]
conv_invol [projection, in ATBR.Classes]
conv_compat [projection, in ATBR.Classes]
conv_star [lemma, in ATBR.Converse]
conv_incr' [lemma, in ATBR.Converse]
conv_incr [instance, in ATBR.Converse]
conv_zero [lemma, in ATBR.Converse]
conv_one [lemma, in ATBR.Converse]
conv_compat' [lemma, in ATBR.Converse]
correct [lemma, in ATBR.DKA_Epsilon]
correct [lemma, in ATBR.DKA_Merge]
correct [lemma, in ATBR.DKA_DFA_Equiv]
correct [lemma, in ATBR.DKA_Determinisation]
correct [lemma, in ATBR.DKA_Construction]
correction [section, in ATBR.Force]
correction.T [variable, in ATBR.Force]
correctness [section, in ATBR.DKA_DFA_Equiv]
Correctness [module, in ATBR.DKA_Construction]
correctness.A [variable, in ATBR.DKA_DFA_Equiv]
Correctness.belong [abbreviation, in ATBR.DKA_Construction]
Correctness.belong_build [lemma, in ATBR.DKA_Construction]
Correctness.belong_add_var [lemma, in ATBR.DKA_Construction]
Correctness.belong_add_one [lemma, in ATBR.DKA_Construction]
Correctness.belong_incr' [lemma, in ATBR.DKA_Construction]
Correctness.belong_incr [lemma, in ATBR.DKA_Construction]
Correctness.bounded [record, in ATBR.DKA_Construction]
Correctness.bounded_empty [lemma, in ATBR.DKA_Construction]
Correctness.bounded_build [lemma, in ATBR.DKA_Construction]
Correctness.bounded_add_var [lemma, in ATBR.DKA_Construction]
Correctness.bounded_add_one [lemma, in ATBR.DKA_Construction]
Correctness.bounded_incr [lemma, in ATBR.DKA_Construction]
Correctness.bounded_eps [projection, in ATBR.DKA_Construction]
Correctness.bounded_delta [projection, in ATBR.DKA_Construction]
Correctness.commute_build_empty [lemma, in ATBR.DKA_Construction]
Correctness.commute_empty [lemma, in ATBR.DKA_Construction]
Correctness.commute_build [lemma, in ATBR.DKA_Construction]
Correctness.commute_incr [lemma, in ATBR.DKA_Construction]
Correctness.commute_add_var [lemma, in ATBR.DKA_Construction]
Correctness.commute_add_one [lemma, in ATBR.DKA_Construction]
Correctness.constructions_equiv [lemma, in ATBR.DKA_Construction]
correctness.Correction [section, in ATBR.DKA_DFA_Equiv]
correctness.Correction.Hi' [variable, in ATBR.DKA_DFA_Equiv]
correctness.Correction.Hj' [variable, in ATBR.DKA_DFA_Equiv]
correctness.Correction.i' [variable, in ATBR.DKA_DFA_Equiv]
correctness.Correction.j' [variable, in ATBR.DKA_DFA_Equiv]
correctness.Correction.tarjan [variable, in ATBR.DKA_DFA_Equiv]
correctness.Correction._H [variable, in ATBR.DKA_DFA_Equiv]
_ =T= _ [notation, in ATBR.DKA_DFA_Equiv]
_ =&&= _ [notation, in ATBR.DKA_DFA_Equiv]
Correctness.delta [definition, in ATBR.DKA_Construction]
Correctness.deltabrel [definition, in ATBR.DKA_Construction]
Correctness.deltabrel_add_var [lemma, in ATBR.DKA_Construction]
Correctness.deltafun [definition, in ATBR.DKA_Construction]
Correctness.delta_add_var [lemma, in ATBR.DKA_Construction]
Correctness.epsilon [definition, in ATBR.DKA_Construction]
Correctness.epsilonbrel [definition, in ATBR.DKA_Construction]
Correctness.epsilonbrel_add_one [lemma, in ATBR.DKA_Construction]
Correctness.epsilonfun [definition, in ATBR.DKA_Construction]
Correctness.epsilon_rt_build [lemma, in ATBR.DKA_Construction]
Correctness.epsilon_rt_incr [lemma, in ATBR.DKA_Construction]
Correctness.epsilon_rt_add_one [lemma, in ATBR.DKA_Construction]
Correctness.epsilon_t_add_one [lemma, in ATBR.DKA_Construction]
Correctness.epsilon_empty [lemma, in ATBR.DKA_Construction]
Correctness.epsilon_incr [lemma, in ATBR.DKA_Construction]
Correctness.epsilon_add_var [lemma, in ATBR.DKA_Construction]
Correctness.epsilon_add_one [lemma, in ATBR.DKA_Construction]
Correctness.epsilon_rt [abbreviation, in ATBR.DKA_Construction]
Correctness.epsilon_t [abbreviation, in ATBR.DKA_Construction]
correctness.Hbounds [variable, in ATBR.DKA_DFA_Equiv]
Correctness.labelling_add_var [lemma, in ATBR.DKA_Construction]
Correctness.labelling_crop [lemma, in ATBR.DKA_Construction]
Correctness.labelling_empty [lemma, in ATBR.DKA_Construction]
Correctness.labelling_S [lemma, in ATBR.DKA_Construction]
Correctness.leb_S [lemma, in ATBR.DKA_Construction]
Correctness.not_epsilon_rt_incr_right [lemma, in ATBR.DKA_Construction]
Correctness.not_epsilon_rt_incr_left [lemma, in ATBR.DKA_Construction]
Correctness.not_true_eq_false [lemma, in ATBR.DKA_Construction]
Correctness.preNFA_to_preMAUT [definition, in ATBR.DKA_Construction]
Correctness.protect [section, in ATBR.DKA_Construction]
Correctness.psurj [lemma, in ATBR.DKA_Construction]
Correctness.rt_t [lemma, in ATBR.DKA_Construction]
Correctness.t_rt [lemma, in ATBR.DKA_Construction]
Correctness.wf [definition, in ATBR.DKA_Construction]
Correctness.wf_empty [lemma, in ATBR.DKA_Construction]
Correctness.wf_build [lemma, in ATBR.DKA_Construction]
Correctness.wf_add_one [lemma, in ATBR.DKA_Construction]
correct_ind_idem [lemma, in ATBR.DKA_DFA_Equiv]
correct_fold_ind [record, in ATBR.DKA_DFA_Equiv]
correct_ind [record, in ATBR.DKA_DFA_Equiv]
CounterExample [inductive, in ATBR.DecideKleeneAlgebra]
counter_exemple_equiv [lemma, in ATBR.DKA_DFA_Equiv]
counter_exemple_loop [lemma, in ATBR.DKA_DFA_Equiv]
CR_algebra.S [variable, in ATBR.ChurchRosser_Points_vs_Algebraic]
CR_algebra.R [variable, in ATBR.ChurchRosser_Points_vs_Algebraic]
CR_algebra.A [variable, in ATBR.ChurchRosser_Points_vs_Algebraic]
CR_algebra [section, in ATBR.ChurchRosser_Points_vs_Algebraic]
_ + _ [notation, in ATBR.ChurchRosser_Points_vs_Algebraic]
_ # [notation, in ATBR.ChurchRosser_Points_vs_Algebraic]
CR_points.S [variable, in ATBR.ChurchRosser_Points_vs_Algebraic]
CR_points.R [variable, in ATBR.ChurchRosser_Points_vs_Algebraic]
CR_points.P [variable, in ATBR.ChurchRosser_Points_vs_Algebraic]
CR_points [section, in ATBR.ChurchRosser_Points_vs_Algebraic]
D
d [abbreviation, in ATBR.DKA_Determinisation]DecideKleeneAlgebra [library]
decide_kleene [definition, in ATBR.DecideKleeneAlgebra]
decomp_dot_leq_right [lemma, in ATBR.MxKleeneAlgebra]
decomp_dot_leq_left [lemma, in ATBR.MxKleeneAlgebra]
Def [section, in ATBR.Model_Relations]
Def [section, in ATBR.Model_StdRelations]
Def [section, in ATBR.Model_Languages]
defined [definition, in ATBR.DKA_Determinisation]
Defs [section, in ATBR.MxSemiRing]
Defs [section, in ATBR.MxFunctors]
Defs [section, in ATBR.Functors]
Defs [section, in ATBR.MxSemiLattice]
Defs [section, in ATBR.MxKleeneAlgebra]
Defs [section, in ATBR.MxGraph]
Defs.A [variable, in ATBR.MxSemiRing]
Defs.A [variable, in ATBR.MxFunctors]
Defs.A [variable, in ATBR.MxSemiLattice]
Defs.A [variable, in ATBR.MxKleeneAlgebra]
Defs.A [variable, in ATBR.MxGraph]
Defs.F [variable, in ATBR.MxFunctors]
Defs.SLfunct [section, in ATBR.Functors]
delta [abbreviation, in ATBR.DKA_DFA_Equiv]
delta [abbreviation, in ATBR.DKA_Determinisation]
Delta [abbreviation, in ATBR.DKA_Determinisation]
delta_bounded [lemma, in ATBR.DKA_Epsilon]
delta_set [definition, in ATBR.DKA_Determinisation]
delta' [definition, in ATBR.DKA_Determinisation]
delta'_below [lemma, in ATBR.DKA_Determinisation]
DFA [module, in ATBR.DKA_Definitions]
DFA_language [definition, in ATBR.DKA_DFA_Language]
DFA.belong [abbreviation, in ATBR.DKA_Definitions]
DFA.bounded [record, in ATBR.DKA_Definitions]
DFA.bounded_finaux [projection, in ATBR.DKA_Definitions]
DFA.bounded_initial [projection, in ATBR.DKA_Definitions]
DFA.bounded_delta [projection, in ATBR.DKA_Definitions]
DFA.change_initial [definition, in ATBR.DKA_Definitions]
DFA.delta [projection, in ATBR.DKA_Definitions]
DFA.eval [definition, in ATBR.DKA_Definitions]
DFA.finaux [projection, in ATBR.DKA_Definitions]
DFA.initial [projection, in ATBR.DKA_Definitions]
DFA.max_label [projection, in ATBR.DKA_Definitions]
DFA.mk [constructor, in ATBR.DKA_Definitions]
DFA.setbelong [abbreviation, in ATBR.DKA_Definitions]
DFA.size [projection, in ATBR.DKA_Definitions]
DFA.t [record, in ATBR.DKA_Definitions]
DFA.to_MAUT [definition, in ATBR.DKA_Definitions]
diag [definition, in ATBR.DKA_DFA_Equiv]
diag_empty [lemma, in ATBR.DKA_DFA_Equiv]
diag_ok [lemma, in ATBR.DKA_DFA_Equiv]
diag_compat_left [lemma, in ATBR.DKA_DFA_Equiv]
diag_compat [instance, in ATBR.DKA_DFA_Equiv]
DifferentAtomSets [constructor, in ATBR.DecideKleeneAlgebra]
DISJOINTSETS [module, in ATBR.DisjointSets]
DisjointSets [library]
DISJOINTSETS.class_of [axiom, in ATBR.DisjointSets]
DISJOINTSETS.empty [axiom, in ATBR.DisjointSets]
DISJOINTSETS.empty_WF [instance, in ATBR.DisjointSets]
DISJOINTSETS.equiv [axiom, in ATBR.DisjointSets]
DISJOINTSETS.equiv_WF [instance, in ATBR.DisjointSets]
DISJOINTSETS.IsWF [axiom, in ATBR.DisjointSets]
DISJOINTSETS.sameclass [axiom, in ATBR.DisjointSets]
DISJOINTSETS.sameclass_class_of [axiom, in ATBR.DisjointSets]
DISJOINTSETS.sameclass_union [axiom, in ATBR.DisjointSets]
DISJOINTSETS.sameclass_empty [axiom, in ATBR.DisjointSets]
DISJOINTSETS.sameclass_Equivalence [instance, in ATBR.DisjointSets]
DISJOINTSETS.sameclass_equiv [axiom, in ATBR.DisjointSets]
DISJOINTSETS.T [axiom, in ATBR.DisjointSets]
DISJOINTSETS.test_and_unify_eq [axiom, in ATBR.DisjointSets]
DISJOINTSETS.test_and_unify_WF [instance, in ATBR.DisjointSets]
DISJOINTSETS.test_and_unify [axiom, in ATBR.DisjointSets]
DISJOINTSETS.union [axiom, in ATBR.DisjointSets]
DISJOINTSETS.union_WF [instance, in ATBR.DisjointSets]
DISJOINTSETS.wf [projection, in ATBR.DisjointSets]
DISJOINTSETS.WF [record, in ATBR.DisjointSets]
DKA_Definitions [library]
DKA_Merge [library]
DKA_Epsilon [library]
DKA_DFA_Language [library]
DKA_CheckLabels [library]
DKA_Construction [library]
DKA_DFA_Equiv [library]
DKA_StateSetSets [library]
DKA_Determinisation [library]
dk_erase_correct [lemma, in ATBR.DecideKleeneAlgebra]
domain [definition, in ATBR.DKA_StateSetSets]
domain [section, in ATBR.DKA_StateSetSets]
domain_spec [lemma, in ATBR.DKA_StateSetSets]
domain.T [variable, in ATBR.DKA_StateSetSets]
dot [projection, in ATBR.Classes]
dot [projection, in ATBR.StrictKleeneAlgebra]
dot_scal_right_blocks [lemma, in ATBR.MxSemiRing]
dot_scal_right_dot [lemma, in ATBR.MxSemiRing]
dot_scal_right_zero [lemma, in ATBR.MxSemiRing]
dot_scal_right_one [lemma, in ATBR.MxSemiRing]
dot_scal_right_is_dot [lemma, in ATBR.MxSemiRing]
dot_scal_left_blocks [lemma, in ATBR.MxSemiRing]
dot_scal_left_dot [lemma, in ATBR.MxSemiRing]
dot_scal_left_zero [lemma, in ATBR.MxSemiRing]
dot_scal_left_one [lemma, in ATBR.MxSemiRing]
dot_scal_left_is_dot [lemma, in ATBR.MxSemiRing]
dot_scal_left_compat [instance, in ATBR.MxSemiRing]
dot_scal_right_compat [instance, in ATBR.MxSemiRing]
dot_scal_left [definition, in ATBR.MxSemiRing]
dot_scal_right [definition, in ATBR.MxSemiRing]
dot_distr_left_c [projection, in ATBR.Classes]
dot_ann_left_c [projection, in ATBR.Classes]
dot_neutral_left_c [projection, in ATBR.Classes]
dot_assoc_c [projection, in ATBR.Classes]
dot_compat_c [projection, in ATBR.Classes]
dot_distr_right [projection, in ATBR.Classes]
dot_distr_left [projection, in ATBR.Classes]
dot_ann_right [projection, in ATBR.Classes]
dot_ann_left [projection, in ATBR.Classes]
dot_neutral_right [projection, in ATBR.Classes]
dot_neutral_left [projection, in ATBR.Classes]
dot_assoc [projection, in ATBR.Classes]
dot_compat [projection, in ATBR.Classes]
dot_distr_right [projection, in ATBR.StrictKleeneAlgebra]
dot_distr_left [projection, in ATBR.StrictKleeneAlgebra]
dot_neutral_right [projection, in ATBR.StrictKleeneAlgebra]
dot_neutral_left [projection, in ATBR.StrictKleeneAlgebra]
dot_assoc [projection, in ATBR.StrictKleeneAlgebra]
dot_compat [projection, in ATBR.StrictKleeneAlgebra]
dot_xif [lemma, in ATBR.Monoid]
dot_incr_temp [instance, in ATBR.Monoid]
dot_xif_zero [lemma, in ATBR.SemiRing]
dot_incr [instance, in ATBR.SemiRing]
dot_boolxif_right [lemma, in ATBR.DKA_DFA_Language]
dot_xifzero_right [lemma, in ATBR.DKA_DFA_Language]
dot_boolxif_left [lemma, in ATBR.DKA_DFA_Language]
dot_xifzero_left [lemma, in ATBR.DKA_DFA_Language]
dot' [definition, in ATBR.StrictStarForm]
dot'_dot [lemma, in ATBR.StrictStarForm]
DS [module, in ATBR.DKA_StateSetSets]
DSUtils [module, in ATBR.DisjointSets]
DSUtils [module, in ATBR.DKA_StateSetSets]
DSUtils.class_of_injective [lemma, in ATBR.DisjointSets]
DSUtils.class_of_union_1 [lemma, in ATBR.DisjointSets]
DSUtils.class_of_compat' [lemma, in ATBR.DisjointSets]
DSUtils.class_of_compat [instance, in ATBR.DisjointSets]
DSUtils.class_of_union_2 [lemma, in ATBR.DisjointSets]
DSUtils.class_of_union [lemma, in ATBR.DisjointSets]
DSUtils.class_of_empty [lemma, in ATBR.DisjointSets]
DSUtils.compat_union_eq [lemma, in ATBR.DisjointSets]
DSUtils.eq [definition, in ATBR.DisjointSets]
DSUtils.eq_union [lemma, in ATBR.DisjointSets]
DSUtils.eq_Equivalence [instance, in ATBR.DisjointSets]
DSUtils.in_class_of_self [lemma, in ATBR.DisjointSets]
DSUtils.le [definition, in ATBR.DisjointSets]
DSUtils.le_incr [lemma, in ATBR.DisjointSets]
DSUtils.le_union [lemma, in ATBR.DisjointSets]
DSUtils.le_PreOrder [instance, in ATBR.DisjointSets]
DSUtils.Notations [module, in ATBR.DisjointSets]
_
_ [=T=] _ [notation, in ATBR.DisjointSets]
{{ _ }} [notation, in ATBR.DisjointSets]
DSUtils.NU [module, in ATBR.DisjointSets]
DSUtils.sameclass_spec [lemma, in ATBR.DisjointSets]
DSUtils.sameclass_compat' [instance, in ATBR.DisjointSets]
DSUtils.sameclass_compat [instance, in ATBR.DisjointSets]
Dual [module, in ATBR.Classes]
Dual [module, in ATBR.KleeneAlgebra]
Dual.Converse_Op [instance, in ATBR.Classes]
Dual.Graph [instance, in ATBR.Classes]
Dual.IdemSemiRing [instance, in ATBR.Classes]
Dual.KleeneAlgebra [instance, in ATBR.KleeneAlgebra]
Dual.Monoid [instance, in ATBR.Classes]
Dual.Monoid_Ops [instance, in ATBR.Classes]
Dual.Protect [section, in ATBR.Classes]
Dual.Protect [section, in ATBR.KleeneAlgebra]
Dual.SemiLattice [instance, in ATBR.Classes]
Dual.SemiLattice_Ops [instance, in ATBR.Classes]
Dual.Star_Op [instance, in ATBR.Classes]
E
e [section, in ATBR.DKA_DFA_Equiv]empty [definition, in ATBR.Model_StdRelations]
eNFA [module, in ATBR.DKA_Definitions]
eNFA_to_NFA [definition, in ATBR.DKA_Epsilon]
eNFA.belong [abbreviation, in ATBR.DKA_Definitions]
eNFA.bounded [record, in ATBR.DKA_Definitions]
eNFA.bounded_final [projection, in ATBR.DKA_Definitions]
eNFA.bounded_initial [projection, in ATBR.DKA_Definitions]
eNFA.bounded_eps [projection, in ATBR.DKA_Definitions]
eNFA.bounded_delta [projection, in ATBR.DKA_Definitions]
eNFA.delta [definition, in ATBR.DKA_Definitions]
eNFA.deltamap [projection, in ATBR.DKA_Definitions]
eNFA.epsilon [projection, in ATBR.DKA_Definitions]
eNFA.eval [definition, in ATBR.DKA_Definitions]
eNFA.final [projection, in ATBR.DKA_Definitions]
eNFA.initial [projection, in ATBR.DKA_Definitions]
eNFA.max_label [projection, in ATBR.DKA_Definitions]
eNFA.mk [constructor, in ATBR.DKA_Definitions]
eNFA.setbelong [abbreviation, in ATBR.DKA_Definitions]
eNFA.size [projection, in ATBR.DKA_Definitions]
eNFA.t [record, in ATBR.DKA_Definitions]
eNFA.to_MAUT [definition, in ATBR.DKA_Definitions]
eNFA.well_founded [definition, in ATBR.DKA_Definitions]
Env [record, in ATBR.Reification]
env [constructor, in ATBR.Reification]
eqd [definition, in ATBR.Reification]
eqd_inj [lemma, in ATBR.Reification]
equal [projection, in ATBR.Classes]
equal [section, in ATBR.Graph]
equal_ [projection, in ATBR.Classes]
equal_geq [instance, in ATBR.Graph]
equal_leq [instance, in ATBR.Graph]
equal_refl_f2t [lemma, in ATBR.Graph]
equal_refl_f1t [lemma, in ATBR.Graph]
equal_refl_f2 [lemma, in ATBR.Graph]
equal_refl_f1 [lemma, in ATBR.Graph]
equal_trans [lemma, in ATBR.Graph]
equal_sym [lemma, in ATBR.Graph]
equal_refl [lemma, in ATBR.Graph]
equal_collect [lemma, in ATBR.DKA_CheckLabels]
equal.A [variable, in ATBR.Graph]
equal.B [variable, in ATBR.Graph]
equiv [definition, in ATBR.DKA_DFA_Equiv]
equivalent [definition, in ATBR.DKA_DFA_Equiv]
equiv_filter [lemma, in ATBR.DKA_Definitions]
eq_not_negb [lemma, in ATBR.BoolView]
eq_nat_bool_refl [lemma, in ATBR.BoolView]
eq_nat_bool_false [lemma, in ATBR.BoolView]
eq_nat_bool_true [lemma, in ATBR.BoolView]
eq_bool_view [instance, in ATBR.BoolView]
eq_bool_spec [lemma, in ATBR.BoolView]
eq_bool_bool [definition, in ATBR.BoolView]
eq_pos_view [instance, in ATBR.BoolView]
eq_pos_spec [lemma, in ATBR.BoolView]
eq_pos_bool [definition, in ATBR.BoolView]
eq_nat_view [instance, in ATBR.BoolView]
eq_nat_spec [lemma, in ATBR.BoolView]
eq_nat_bool [definition, in ATBR.BoolView]
eq_label_bool [abbreviation, in ATBR.DKA_Definitions]
eq_state_bool [abbreviation, in ATBR.DKA_Definitions]
eq_to_Meq [lemma, in ATBR.MxGraph]
eval_right [lemma, in ATBR.DKA_Merge]
eval_left [lemma, in ATBR.DKA_Merge]
eval_change_initial [lemma, in ATBR.DKA_DFA_Equiv]
example [lemma, in ATBR.Examples]
Examples [library]
extends [record, in ATBR.DKA_Determinisation]
e_next [projection, in ATBR.DKA_Determinisation]
e_table [projection, in ATBR.DKA_Determinisation]
e_invariant [projection, in ATBR.DKA_Determinisation]
e.A [variable, in ATBR.DKA_DFA_Equiv]
e.d [variable, in ATBR.DKA_DFA_Equiv]
e.f [variable, in ATBR.DKA_DFA_Equiv]
e.final [variable, in ATBR.DKA_DFA_Equiv]
e.m [variable, in ATBR.DKA_DFA_Equiv]
F
F [section, in ATBR.StrictKleeneAlgebra]faithful [lemma, in ATBR.StrictKleeneAlgebra]
faithful [definition, in ATBR.Functors]
final [abbreviation, in ATBR.DKA_DFA_Equiv]
final_compat [lemma, in ATBR.DKA_Determinisation]
finaux [abbreviation, in ATBR.DKA_Determinisation]
Fix_induction [lemma, in ATBR.Utils_WF]
Fix_induction.IH [variable, in ATBR.Utils_WF]
Fix_induction.P [variable, in ATBR.Utils_WF]
Fix_induction.F [variable, in ATBR.Utils_WF]
Fix_induction.T [variable, in ATBR.Utils_WF]
Fix_induction.Hwf [variable, in ATBR.Utils_WF]
Fix_induction.R [variable, in ATBR.Utils_WF]
Fix_induction.A [variable, in ATBR.Utils_WF]
Fix_induction [section, in ATBR.Utils_WF]
FMapHide [module, in ATBR.MyFSets]
fold_labels [abbreviation, in ATBR.DKA_Definitions]
fold_states [abbreviation, in ATBR.DKA_Definitions]
fold' [section, in ATBR.DKA_Epsilon]
fold'.A [variable, in ATBR.DKA_Epsilon]
force [section, in ATBR.Force]
Force [library]
force_rec_rec [lemma, in ATBR.Force]
force_rec [definition, in ATBR.Force]
force.f [variable, in ATBR.Force]
force.T [variable, in ATBR.Force]
force2 [section, in ATBR.Force]
force2.f [variable, in ATBR.Force]
force2.m [variable, in ATBR.Force]
force2.n [variable, in ATBR.Force]
force2.T [variable, in ATBR.Force]
FSetHide [module, in ATBR.MyFSets]
FSumDef [section, in ATBR.SemiLattice]
FSumDef.A [variable, in ATBR.SemiLattice]
FSumDef.B [variable, in ATBR.SemiLattice]
fT [projection, in ATBR.Functors]
full [definition, in ATBR.Functors]
Fun [abbreviation, in ATBR.Utils_WF]
functor [record, in ATBR.Functors]
Functors [library]
functor_mx_to_scal [lemma, in ATBR.MxFunctors]
functor_mx_of_scal [lemma, in ATBR.MxFunctors]
functor_mx_sub [lemma, in ATBR.MxFunctors]
functor_mx_blocks [lemma, in ATBR.MxFunctors]
functor_star [projection, in ATBR.Functors]
functor_star_leq [lemma, in ATBR.Functors]
functor_sum [lemma, in ATBR.Functors]
functor_incr [lemma, in ATBR.Functors]
functor_zero [projection, in ATBR.Functors]
functor_plus [projection, in ATBR.Functors]
functor_one [projection, in ATBR.Functors]
functor_dot [projection, in ATBR.Functors]
functor_compat [projection, in ATBR.Functors]
functor_xif [lemma, in ATBR.DKA_DFA_Language]
fun_xif [lemma, in ATBR.Graph]
fX [projection, in ATBR.Functors]
G
get [definition, in ATBR.MxGraph]Graph [record, in ATBR.Classes]
Graph [library]
graph_functor [record, in ATBR.Functors]
guard [definition, in ATBR.Utils_WF]
H
Hindley_Rosen_confluent_union [lemma, in ATBR.ChurchRosser]Hindley_Rosen_union [lemma, in ATBR.ChurchRosser]
Hindley_Rosen [lemma, in ATBR.ChurchRosser]
I
id [definition, in ATBR.Force]IdemSemiRing [record, in ATBR.Classes]
id_notid [lemma, in ATBR.Force]
id_id [lemma, in ATBR.Force]
id2 [definition, in ATBR.Force]
id2_id [lemma, in ATBR.Force]
incl_wf [lemma, in ATBR.Utils_WF]
infty [abbreviation, in ATBR.Model_MinPlus]
inf_def [lemma, in ATBR.SemiLattice]
inf_leq [lemma, in ATBR.DKA_Construction]
initial_store [definition, in ATBR.DKA_Determinisation]
initiaux [abbreviation, in ATBR.DKA_Determinisation]
inj [definition, in ATBR.StrictKleeneAlgebra]
invariant [record, in ATBR.DKA_DFA_Equiv]
invariant [record, in ATBR.DKA_Determinisation]
invariant_empty [lemma, in ATBR.DKA_DFA_Equiv]
invariant_prog [lemma, in ATBR.DKA_DFA_Equiv]
invariant_idem [lemma, in ATBR.DKA_DFA_Equiv]
invariant_build_store [lemma, in ATBR.DKA_Determinisation]
invariant_initial_store [lemma, in ATBR.DKA_Determinisation]
in_classes_empty_below [lemma, in ATBR.DKA_StateSetSets]
in_classes [lemma, in ATBR.DKA_StateSetSets]
in_union [lemma, in ATBR.DKA_DFA_Equiv]
in_delta_set [lemma, in ATBR.DKA_Determinisation]
ISR [section, in ATBR.Converse]
ISR_SemiLattice [projection, in ATBR.Classes]
ISR_Monoid [projection, in ATBR.Classes]
iter [definition, in ATBR.Monoid]
iter_compat [lemma, in ATBR.Monoid]
iter_swap2 [lemma, in ATBR.Monoid]
iter_swap [lemma, in ATBR.Monoid]
iter_split [lemma, in ATBR.Monoid]
iter_once [lemma, in ATBR.Monoid]
iter_equivalence [lemma, in ATBR.DKA_Definitions]
i_final [projection, in ATBR.DKA_DFA_Equiv]
i_wf_tarjan [projection, in ATBR.DKA_DFA_Equiv]
i_delta [projection, in ATBR.DKA_Determinisation]
i_table_size [projection, in ATBR.DKA_Determinisation]
i_table_surj [projection, in ATBR.DKA_Determinisation]
i_table_inj [projection, in ATBR.DKA_Determinisation]
i_table_wf [projection, in ATBR.DKA_Determinisation]
K
KA [module, in ATBR.Reification]KA [section, in ATBR.Converse]
KA_ISR [projection, in ATBR.Classes]
KA.dot [constructor, in ATBR.Reification]
KA.eval [definition, in ATBR.Reification]
KA.one [constructor, in ATBR.Reification]
KA.plus [constructor, in ATBR.Reification]
KA.S [section, in ATBR.Reification]
KA.star [constructor, in ATBR.Reification]
KA.var [constructor, in ATBR.Reification]
KA.X [inductive, in ATBR.Reification]
KA.zero [constructor, in ATBR.Reification]
KleeneAlgebra [record, in ATBR.Classes]
KleeneAlgebra [library]
kleene_semiring [projection, in ATBR.Functors]
kleene_functor [record, in ATBR.Functors]
Kozen94 [lemma, in ATBR.DecideKleeneAlgebra]
kt [abbreviation, in ATBR.DKA_DFA_Equiv]
L
label [abbreviation, in ATBR.DKA_Definitions]Label [module, in ATBR.DKA_Definitions]
labelling [definition, in ATBR.DKA_Definitions]
lang [definition, in ATBR.Model_Languages]
language [abbreviation, in ATBR.DKA_DFA_Language]
language_DFA_eval [lemma, in ATBR.DKA_DFA_Language]
lang_KleeneAlgebra [definition, in ATBR.Model_Languages]
lang_ConverseKleeneAlgebra [instance, in ATBR.Model_Languages]
lang_Union_spec [lemma, in ATBR.Model_Languages]
lang_leq [lemma, in ATBR.Model_Languages]
lang_IdemSemiRing [definition, in ATBR.Model_Languages]
lang_ConverseSemiRing [instance, in ATBR.Model_Languages]
lang_SemiLattice [instance, in ATBR.Model_Languages]
lang_Converse_Op [instance, in ATBR.Model_Languages]
lang_Star_Op [instance, in ATBR.Model_Languages]
lang_Monoid_Ops [instance, in ATBR.Model_Languages]
lang_SemiLattice_Ops [instance, in ATBR.Model_Languages]
lang_Graph [instance, in ATBR.Model_Languages]
lang_star [definition, in ATBR.Model_Languages]
lang_iter [definition, in ATBR.Model_Languages]
lang_top [definition, in ATBR.Model_Languages]
lang_empty [definition, in ATBR.Model_Languages]
lang_id [definition, in ATBR.Model_Languages]
lang_conv [definition, in ATBR.Model_Languages]
lang_comp [definition, in ATBR.Model_Languages]
lang_inter [definition, in ATBR.Model_Languages]
lang_Union [definition, in ATBR.Model_Languages]
lang_union [definition, in ATBR.Model_Languages]
lang_equal [definition, in ATBR.Model_Languages]
lang_sum [lemma, in ATBR.DKA_DFA_Language]
left_filter [lemma, in ATBR.DKA_Definitions]
leq [section, in ATBR.Graph]
leq_antisym [definition, in ATBR.Graph]
leq_trans [instance, in ATBR.Graph]
leq_refl [instance, in ATBR.Graph]
leq_lang_Union [lemma, in ATBR.Model_Languages]
leq_zero_plus [lemma, in ATBR.DKA_DFA_Equiv]
leq_sum [lemma, in ATBR.SemiLattice]
leq_destruct_plus [lemma, in ATBR.SemiLattice]
leq_mx_lang_Union [lemma, in ATBR.DKA_DFA_Language]
leq.A [variable, in ATBR.Graph]
leq.B [variable, in ATBR.Graph]
lexico [inductive, in ATBR.Utils_WF]
lexico [section, in ATBR.Utils_WF]
lexico_incl_wf [lemma, in ATBR.Utils_WF]
lexico_wf [lemma, in ATBR.Utils_WF]
lexico_right [constructor, in ATBR.Utils_WF]
lexico_left [constructor, in ATBR.Utils_WF]
lexico.A [variable, in ATBR.Utils_WF]
lexico.B [variable, in ATBR.Utils_WF]
lexico.HR [variable, in ATBR.Utils_WF]
lexico.HS [variable, in ATBR.Utils_WF]
lexico.R [variable, in ATBR.Utils_WF]
lexico.S [variable, in ATBR.Utils_WF]
le_lt_bool_refl [lemma, in ATBR.BoolView]
le_lt_bool_false [lemma, in ATBR.BoolView]
le_lt_bool_true [lemma, in ATBR.BoolView]
le_nat_view [instance, in ATBR.BoolView]
le_nat_spec [lemma, in ATBR.BoolView]
le_lt_bool [definition, in ATBR.BoolView]
le_proxy [lemma, in ATBR.DKA_DFA_Equiv]
le_antisym [lemma, in ATBR.DKA_Construction]
linearfix [definition, in ATBR.Utils_WF]
linearfix_plus [lemma, in ATBR.Utils_WF]
linearfix_compat [instance, in ATBR.Utils_WF]
ListOrderedTypeAlt [module, in ATBR.MyFSets]
ListOrderedTypeAlt.compare [definition, in ATBR.MyFSets]
ListOrderedTypeAlt.compare_trans [lemma, in ATBR.MyFSets]
ListOrderedTypeAlt.compare_sym [lemma, in ATBR.MyFSets]
ListOrderedTypeAlt.reflect [lemma, in ATBR.MyFSets]
ListOrderedTypeAlt.t [definition, in ATBR.MyFSets]
LMX [abbreviation, in ATBR.DKA_DFA_Language]
Load [module, in ATBR.Model_Relations]
Load [module, in ATBR.Model_StdRelations]
Load [module, in ATBR.Model_Languages]
Load [module, in ATBR.Model_MinPlus]
Load.LMX [abbreviation, in ATBR.Model_Languages]
Load.LX [abbreviation, in ATBR.Model_Languages]
loop [definition, in ATBR.DKA_DFA_Equiv]
loop_correct [lemma, in ATBR.DKA_DFA_Equiv]
lt_state_bool [abbreviation, in ATBR.DKA_Definitions]
lt_n_1 [lemma, in ATBR.MxGraph]
LX [abbreviation, in ATBR.Model_Languages]
M
map_transitive_closure.Hwf [variable, in ATBR.DKA_Epsilon]map_transitive_closure.R [variable, in ATBR.DKA_Epsilon]
map_transitive_closure.f [variable, in ATBR.DKA_Epsilon]
map_transitive_closure [section, in ATBR.DKA_Epsilon]
Matrices [section, in ATBR.Examples]
Matrices.A [variable, in ATBR.Examples]
MAUT [module, in ATBR.DKA_Definitions]
MAUT.delta [projection, in ATBR.DKA_Definitions]
MAUT.equal [inductive, in ATBR.DKA_Definitions]
MAUT.equal_equiv [instance, in ATBR.DKA_Definitions]
MAUT.equal_refl [constructor, in ATBR.DKA_Definitions]
MAUT.eval [definition, in ATBR.DKA_Definitions]
MAUT.eval_compat [instance, in ATBR.DKA_Definitions]
MAUT.final [projection, in ATBR.DKA_Definitions]
MAUT.initial [projection, in ATBR.DKA_Definitions]
MAUT.mk [constructor, in ATBR.DKA_Definitions]
MAUT.size [projection, in ATBR.DKA_Definitions]
MAUT.t [record, in ATBR.DKA_Definitions]
_ [==] _ [notation, in ATBR.DKA_Definitions]
max_label [abbreviation, in ATBR.DKA_Determinisation]
max_label_X_to_eNFA [lemma, in ATBR.DKA_Construction]
max_label_collect [lemma, in ATBR.DKA_Construction]
max_label_incr [lemma, in ATBR.DKA_Construction]
max_label_add_var [lemma, in ATBR.DKA_Construction]
max_label_add_one [lemma, in ATBR.DKA_Construction]
measure [definition, in ATBR.DKA_StateSetSets]
measure [abbreviation, in ATBR.DKA_DFA_Equiv]
measure_union_strict [lemma, in ATBR.DKA_StateSetSets]
measure_empty [lemma, in ATBR.DKA_StateSetSets]
measure_union_idem [lemma, in ATBR.DKA_StateSetSets]
measure_compat [lemma, in ATBR.DKA_StateSetSets]
mem_set_closure [lemma, in ATBR.DKA_Epsilon]
mem_table_finals [lemma, in ATBR.DKA_Determinisation]
Meq_to_eq [lemma, in ATBR.MxGraph]
merge_bounded [lemma, in ATBR.DKA_Merge]
merge_DFAs [definition, in ATBR.DKA_Merge]
MG1 [abbreviation, in ATBR.MxFunctors]
MG2 [abbreviation, in ATBR.MxFunctors]
ml [abbreviation, in ATBR.DKA_DFA_Equiv]
Model_Relations [library]
Model_RegExp [library]
Model_StdRelations [library]
Model_Languages [library]
Model_MinPlus [library]
Monoid [record, in ATBR.Classes]
Monoid [library]
Monoid_Ops [record, in ATBR.Classes]
monoid_rewrite_leq [section, in ATBR.Monoid]
monoid_rewrite_equal [section, in ATBR.Monoid]
monoid_graph_functor [projection, in ATBR.Functors]
monoid_functor [record, in ATBR.Functors]
move_star2 [lemma, in ATBR.KleeneAlgebra]
move_star [lemma, in ATBR.KleeneAlgebra]
mp_KleeneAlgebra [definition, in ATBR.Model_MinPlus]
mp_ConverseKleeneAlgebra [instance, in ATBR.Model_MinPlus]
mp_IdemSemiRing [definition, in ATBR.Model_MinPlus]
mp_ConverseSemiRing [instance, in ATBR.Model_MinPlus]
mp_SemiLattice [instance, in ATBR.Model_MinPlus]
mp_Converse_Op [instance, in ATBR.Model_MinPlus]
mp_Star_Op [instance, in ATBR.Model_MinPlus]
mp_Monoid_Ops [instance, in ATBR.Model_MinPlus]
mp_SemiLattice_Ops [instance, in ATBR.Model_MinPlus]
mp_Graph [instance, in ATBR.Model_MinPlus]
mp_star [definition, in ATBR.Model_MinPlus]
mp_empty [definition, in ATBR.Model_MinPlus]
mp_id [definition, in ATBR.Model_MinPlus]
mp_conv [definition, in ATBR.Model_MinPlus]
mp_comp [definition, in ATBR.Model_MinPlus]
mp_union [definition, in ATBR.Model_MinPlus]
MX [abbreviation, in ATBR.MxSemiRing]
MX [abbreviation, in ATBR.MxSemiRing]
MX [abbreviation, in ATBR.MxSemiRing]
MX [abbreviation, in ATBR.MxSemiLattice]
MX [abbreviation, in ATBR.MxSemiLattice]
MX [abbreviation, in ATBR.MxKleeneAlgebra]
MX [abbreviation, in ATBR.MxKleeneAlgebra]
MX [abbreviation, in ATBR.MxGraph]
MX [inductive, in ATBR.MxGraph]
MX [abbreviation, in ATBR.Examples]
mxF [definition, in ATBR.MxFunctors]
MxFunctors [library]
MxGraph [library]
mxgraph_functor [instance, in ATBR.MxFunctors]
MxKleeneAlgebra [library]
mxkleene_functor [instance, in ATBR.MxFunctors]
MxSemiLattice [library]
mxsemilattice_functor [instance, in ATBR.MxFunctors]
MxSemiRing [library]
mxsemiring_functor [instance, in ATBR.MxFunctors]
mx_point_center [lemma, in ATBR.MxSemiRing]
mx_point_one_left [lemma, in ATBR.MxSemiRing]
mx_point_dot_zero [lemma, in ATBR.MxSemiRing]
mx_point_dot [lemma, in ATBR.MxSemiRing]
mx_to_scal_one [lemma, in ATBR.MxSemiRing]
mx_to_scal_dot [lemma, in ATBR.MxSemiRing]
mx_of_scal_one [lemma, in ATBR.MxSemiRing]
mx_of_scal_dot [lemma, in ATBR.MxSemiRing]
mx_blocks_one [lemma, in ATBR.MxSemiRing]
mx_blocks_dot [lemma, in ATBR.MxSemiRing]
mx_equal [abbreviation, in ATBR.MxSemiRing]
mx_equal [abbreviation, in ATBR.MxSemiRing]
mx_one_ [abbreviation, in ATBR.MxSemiRing]
mx_dot_ [abbreviation, in ATBR.MxSemiRing]
mx_SemiRing [instance, in ATBR.MxSemiRing]
mx_Monoid [instance, in ATBR.MxSemiRing]
mx_dot_neutral_right [lemma, in ATBR.MxSemiRing]
mx_dot_neutral_left [lemma, in ATBR.MxSemiRing]
mx_dot_assoc [lemma, in ATBR.MxSemiRing]
mx_bool [definition, in ATBR.MxSemiRing]
mx_Monoid_Ops [instance, in ATBR.MxSemiRing]
mx_one [definition, in ATBR.MxSemiRing]
mx_dot [definition, in ATBR.MxSemiRing]
mx_equal [abbreviation, in ATBR.MxSemiRing]
mx_point_compat [instance, in ATBR.MxSemiLattice]
mx_point_blocks11 [lemma, in ATBR.MxSemiLattice]
mx_point_blocks10 [lemma, in ATBR.MxSemiLattice]
mx_point_blocks01 [lemma, in ATBR.MxSemiLattice]
mx_point_blocks00 [lemma, in ATBR.MxSemiLattice]
mx_point_scal [lemma, in ATBR.MxSemiLattice]
mx_point_plus [lemma, in ATBR.MxSemiLattice]
mx_point_zero [lemma, in ATBR.MxSemiLattice]
mx_blocks_leq [lemma, in ATBR.MxSemiLattice]
mx_blocks_sum [lemma, in ATBR.MxSemiLattice]
mx_to_scal_zero [lemma, in ATBR.MxSemiLattice]
mx_to_scal_plus [lemma, in ATBR.MxSemiLattice]
mx_of_scal_zero [lemma, in ATBR.MxSemiLattice]
mx_of_scal_plus [lemma, in ATBR.MxSemiLattice]
mx_sub_plus [lemma, in ATBR.MxSemiLattice]
mx_blocks_incr [instance, in ATBR.MxSemiLattice]
mx_blocks_zero [lemma, in ATBR.MxSemiLattice]
mx_blocks_plus [lemma, in ATBR.MxSemiLattice]
mx_leq [abbreviation, in ATBR.MxSemiLattice]
mx_equal [abbreviation, in ATBR.MxSemiLattice]
mx_leq_ [abbreviation, in ATBR.MxSemiLattice]
mx_SemiLattice [instance, in ATBR.MxSemiLattice]
mx_point [definition, in ATBR.MxSemiLattice]
mx_SemiLattice_Ops [instance, in ATBR.MxSemiLattice]
mx_zero [definition, in ATBR.MxSemiLattice]
mx_plus [definition, in ATBR.MxSemiLattice]
mx_equal [abbreviation, in ATBR.MxSemiLattice]
mx_of_scal_star [lemma, in ATBR.MxKleeneAlgebra]
mx_to_scal_star [lemma, in ATBR.MxKleeneAlgebra]
mx_blocks_star_diagonal [lemma, in ATBR.MxKleeneAlgebra]
mx_blocks_star_trigonal [lemma, in ATBR.MxKleeneAlgebra]
mx_blocks_star [lemma, in ATBR.MxKleeneAlgebra]
mx_blocks_star' [lemma, in ATBR.MxKleeneAlgebra]
mx_KleeneAlgebra [instance, in ATBR.MxKleeneAlgebra]
mx_star_destruct_right [lemma, in ATBR.MxKleeneAlgebra]
mx_star_block_destruct_left [lemma, in ATBR.MxKleeneAlgebra]
mx_star_destruct_left [lemma, in ATBR.MxKleeneAlgebra]
mx_star_block_make_left [lemma, in ATBR.MxKleeneAlgebra]
mx_star_make_left [lemma, in ATBR.MxKleeneAlgebra]
mx_star_compat [lemma, in ATBR.MxKleeneAlgebra]
mx_Star_Op [instance, in ATBR.MxKleeneAlgebra]
mx_leq [abbreviation, in ATBR.MxKleeneAlgebra]
mx_equal [abbreviation, in ATBR.MxKleeneAlgebra]
mx_star_block [definition, in ATBR.MxKleeneAlgebra]
mx_leq [abbreviation, in ATBR.MxKleeneAlgebra]
mx_equal [abbreviation, in ATBR.MxKleeneAlgebra]
mx_star_charac [lemma, in ATBR.DKA_DFA_Language]
mx_lang_Union_spec [lemma, in ATBR.DKA_DFA_Language]
mx_lang_Union [definition, in ATBR.DKA_DFA_Language]
mx_leq_pointwise [lemma, in ATBR.DKA_DFA_Language]
mx_transpose_blocks [lemma, in ATBR.MxGraph]
mx_transpose_compat [instance, in ATBR.MxGraph]
mx_transpose [definition, in ATBR.MxGraph]
mx_to_scal_from_scal [lemma, in ATBR.MxGraph]
mx_to_scal_compat [instance, in ATBR.MxGraph]
mx_of_scal_compat [instance, in ATBR.MxGraph]
mx_to_scal [definition, in ATBR.MxGraph]
mx_of_scal [definition, in ATBR.MxGraph]
mx_blocks_degenerate_11 [lemma, in ATBR.MxGraph]
mx_blocks_degenerate_00 [lemma, in ATBR.MxGraph]
mx_blocks_equal [lemma, in ATBR.MxGraph]
mx_block_11 [lemma, in ATBR.MxGraph]
mx_block_10 [lemma, in ATBR.MxGraph]
mx_block_01 [lemma, in ATBR.MxGraph]
mx_block_00 [lemma, in ATBR.MxGraph]
mx_decompose_blocks [lemma, in ATBR.MxGraph]
mx_blocks_compat [instance, in ATBR.MxGraph]
mx_blocks [definition, in ATBR.MxGraph]
mx_sub11_compat [instance, in ATBR.MxGraph]
mx_sub10_compat [instance, in ATBR.MxGraph]
mx_sub01_compat [instance, in ATBR.MxGraph]
mx_sub00_compat [instance, in ATBR.MxGraph]
mx_sub11 [definition, in ATBR.MxGraph]
mx_sub10 [definition, in ATBR.MxGraph]
mx_sub01 [definition, in ATBR.MxGraph]
mx_sub00 [definition, in ATBR.MxGraph]
mx_sub [definition, in ATBR.MxGraph]
mx_force_compat [instance, in ATBR.MxGraph]
mx_force_id [lemma, in ATBR.MxGraph]
mx_noprint [definition, in ATBR.MxGraph]
mx_print [definition, in ATBR.MxGraph]
mx_force [definition, in ATBR.MxGraph]
mx_equal_compat [lemma, in ATBR.MxGraph]
mx_equal [abbreviation, in ATBR.MxGraph]
mx_equal_ [abbreviation, in ATBR.MxGraph]
MX_ [abbreviation, in ATBR.MxGraph]
mx_equal_at_equal [lemma, in ATBR.MxGraph]
mx_equal_at [definition, in ATBR.MxGraph]
mx_equal' [lemma, in ATBR.MxGraph]
mx_Graph [instance, in ATBR.MxGraph]
mx_equal [definition, in ATBR.MxGraph]
MyFMapProperties [library]
MyFSetProperties [library]
MyFSets [library]
MyMapProps [module, in ATBR.MyFMapProperties]
MyMapProps.find_view [instance, in ATBR.MyFMapProperties]
MyMapProps.find_spec [lemma, in ATBR.MyFMapProperties]
MyMapProps.find_spec_2 [constructor, in ATBR.MyFMapProperties]
MyMapProps.find_spec_1 [constructor, in ATBR.MyFMapProperties]
MyMapProps.find_spec_ind [inductive, in ATBR.MyFMapProperties]
MyMapProps.in_add_2 [lemma, in ATBR.MyFMapProperties]
MyMapProps.in_add_1 [lemma, in ATBR.MyFMapProperties]
MyMapProps.mapsto_in [lemma, in ATBR.MyFMapProperties]
MySetProps [module, in ATBR.MyFSetProperties]
MySetProps.Dec [module, in ATBR.MyFSetProperties]
MySetProps.elements [section, in ATBR.MyFSetProperties]
MySetProps.elements_fold [lemma, in ATBR.MyFSetProperties]
MySetProps.EqProps [module, in ATBR.MyFSetProperties]
MySetProps.exists_fold [lemma, in ATBR.MyFSetProperties]
MySetProps.exists_fold' [lemma, in ATBR.MyFSetProperties]
MySetProps.exists_empty [lemma, in ATBR.MyFSetProperties]
MySetProps.exists_add [lemma, in ATBR.MyFSetProperties]
MySetProps.exists_compat [lemma, in ATBR.MyFSetProperties]
MySetProps.exists_.Hcompat [variable, in ATBR.MyFSetProperties]
MySetProps.exists_.f [variable, in ATBR.MyFSetProperties]
MySetProps.exists_ [section, in ATBR.MyFSetProperties]
MySetProps.Facts [module, in ATBR.MyFSetProperties]
MySetProps.fold_compat [lemma, in ATBR.MyFSetProperties]
MySetProps.fold_left_id [lemma, in ATBR.MyFSetProperties]
MySetProps.fold_rec_bis' [lemma, in ATBR.MyFSetProperties]
MySetProps.fold_add_above [lemma, in ATBR.MyFSetProperties]
MySetProps.fold_add_below [lemma, in ATBR.MyFSetProperties]
MySetProps.fold_empty [lemma, in ATBR.MyFSetProperties]
MySetProps.lcons [constructor, in ATBR.MyFSetProperties]
MySetProps.lconsa [constructor, in ATBR.MyFSetProperties]
MySetProps.ListViewAbove [section, in ATBR.MyFSetProperties]
MySetProps.ListViewAbove.i [section, in ATBR.MyFSetProperties]
MySetProps.ListViewAbove.i.a [variable, in ATBR.MyFSetProperties]
MySetProps.ListViewAbove.i.f [variable, in ATBR.MyFSetProperties]
MySetProps.ListViewAbove.i.P [variable, in ATBR.MyFSetProperties]
MySetProps.ListViewBelow [section, in ATBR.MyFSetProperties]
MySetProps.lnil [constructor, in ATBR.MyFSetProperties]
MySetProps.lnila [constructor, in ATBR.MyFSetProperties]
MySetProps.lVA [definition, in ATBR.MyFSetProperties]
MySetProps.lva [inductive, in ATBR.MyFSetProperties]
MySetProps.lva_iter [lemma, in ATBR.MyFSetProperties]
MySetProps.lVB [definition, in ATBR.MyFSetProperties]
MySetProps.lvb [inductive, in ATBR.MyFSetProperties]
MySetProps.lvb_iter [definition, in ATBR.MyFSetProperties]
MySetProps.mem_false_not_in [lemma, in ATBR.MyFSetProperties]
MySetProps.mem_type_view [instance, in ATBR.MyFSetProperties]
MySetProps.mem_spec [lemma, in ATBR.MyFSetProperties]
MySetProps.mem_add [lemma, in ATBR.MyFSetProperties]
MySetProps.MyFold [section, in ATBR.MyFSetProperties]
MySetProps.MyFold.A [variable, in ATBR.MyFSetProperties]
MySetProps.MyFold.eqA [variable, in ATBR.MyFSetProperties]
MySetProps.MyFold.equivalence_eqA [variable, in ATBR.MyFSetProperties]
MySetProps.MyFold.f [variable, in ATBR.MyFSetProperties]
MySetProps.MyFold.fold_rec_bis.P [variable, in ATBR.MyFSetProperties]
MySetProps.MyFold.fold_rec_bis [section, in ATBR.MyFSetProperties]
MySetProps.MyFold.Hcompat [variable, in ATBR.MyFSetProperties]
MySetProps.OrdProps [module, in ATBR.MyFSetProperties]
MySetProps.Props [module, in ATBR.MyFSetProperties]
MySetProps.set_induction_above [definition, in ATBR.MyFSetProperties]
MySetProps.set_induction_below [definition, in ATBR.MyFSetProperties]
N
Nat_as_OT [module, in ATBR.MyFSets]Nat_as_OTA.reflect [lemma, in ATBR.MyFSets]
Nat_as_OTA.compare_trans [lemma, in ATBR.MyFSets]
Nat_as_OTA.compare_sym [lemma, in ATBR.MyFSets]
Nat_as_OTA.compare [definition, in ATBR.MyFSets]
Nat_as_OTA.t [definition, in ATBR.MyFSets]
Nat_as_OTA [module, in ATBR.MyFSets]
nat_of_state [abbreviation, in ATBR.DKA_Definitions]
negb_false [lemma, in ATBR.BoolView]
negb_true [lemma, in ATBR.BoolView]
NFA [module, in ATBR.DKA_Definitions]
NFA_to_DFA [definition, in ATBR.DKA_Determinisation]
NFA.belong [abbreviation, in ATBR.DKA_Definitions]
NFA.bounded [record, in ATBR.DKA_Definitions]
NFA.bounded_finaux [projection, in ATBR.DKA_Definitions]
NFA.bounded_initiaux [projection, in ATBR.DKA_Definitions]
NFA.bounded_delta [projection, in ATBR.DKA_Definitions]
NFA.change_initial [definition, in ATBR.DKA_Definitions]
NFA.delta [projection, in ATBR.DKA_Definitions]
NFA.eval [definition, in ATBR.DKA_Definitions]
NFA.finaux [projection, in ATBR.DKA_Definitions]
NFA.initiaux [projection, in ATBR.DKA_Definitions]
NFA.max_label [projection, in ATBR.DKA_Definitions]
NFA.mk [constructor, in ATBR.DKA_Definitions]
NFA.setbelong [abbreviation, in ATBR.DKA_Definitions]
NFA.size [projection, in ATBR.DKA_Definitions]
NFA.t [record, in ATBR.DKA_Definitions]
NFA.to_MAUT [definition, in ATBR.DKA_Definitions]
non_strict_not_strict [lemma, in ATBR.StrictStarForm]
non_strict_plus_r [constructor, in ATBR.StrictStarForm]
non_strict_plus_l [constructor, in ATBR.StrictStarForm]
non_strict_dot [constructor, in ATBR.StrictStarForm]
non_strict_star [constructor, in ATBR.StrictStarForm]
non_strict_one [constructor, in ATBR.StrictStarForm]
non_strict [inductive, in ATBR.StrictStarForm]
NotGeq [constructor, in ATBR.DecideKleeneAlgebra]
NotLeq [constructor, in ATBR.DecideKleeneAlgebra]
ns [abbreviation, in ATBR.DKA_Epsilon]
nth [definition, in ATBR.Force]
nth_force_rec' [lemma, in ATBR.Force]
nth_force_rec [lemma, in ATBR.Force]
NUM [module, in ATBR.Numbers]
Numbers [library]
numota_of_nat [definition, in ATBR.DKA_Definitions]
NumSetEqual_refl [lemma, in ATBR.DKA_CheckLabels]
NumUtils [module, in ATBR.Numbers]
NumUtils.eqb_eq_nat_bool [lemma, in ATBR.Numbers]
NumUtils.eqb_refl [lemma, in ATBR.Numbers]
NumUtils.eqb_false [lemma, in ATBR.Numbers]
NumUtils.eqb_true [lemma, in ATBR.Numbers]
NumUtils.eqb_view [instance, in ATBR.Numbers]
NumUtils.eq_num_dec [lemma, in ATBR.Numbers]
NumUtils.eq_nat_spec [lemma, in ATBR.Numbers]
NumUtils.fold_num_compat [instance, in ATBR.Numbers]
NumUtils.fold_num_compat' [instance, in ATBR.Numbers]
NumUtils.leb_refl [lemma, in ATBR.Numbers]
NumUtils.leb_false [lemma, in ATBR.Numbers]
NumUtils.leb_true [lemma, in ATBR.Numbers]
NumUtils.leb_view [instance, in ATBR.Numbers]
NumUtils.le_antisym [lemma, in ATBR.Numbers]
NumUtils.le_preorder [instance, in ATBR.Numbers]
NumUtils.ltb_false [lemma, in ATBR.Numbers]
NumUtils.ltb_true [lemma, in ATBR.Numbers]
NumUtils.ltb_view [instance, in ATBR.Numbers]
NumUtils.lt_transitive [instance, in ATBR.Numbers]
NumUtils.nat_of_num_comm [lemma, in ATBR.Numbers]
NumUtils.NumMapProps [module, in ATBR.Numbers]
NumUtils.numseteqb_eq_nat_bool [lemma, in ATBR.Numbers]
NumUtils.NumSetProps [module, in ATBR.Numbers]
NumUtils.num_of_nat_comm [lemma, in ATBR.Numbers]
NumUtils.num_peano_rec [lemma, in ATBR.Numbers]
NumUtils.pi0_inj [lemma, in ATBR.Numbers]
NumUtils.pi1_inj [lemma, in ATBR.Numbers]
_ <= _ (num_scope) [notation, in ATBR.Numbers]
_ < _ (num_scope) [notation, in ATBR.Numbers]
7 (num_scope) [notation, in ATBR.Numbers]
5 (num_scope) [notation, in ATBR.Numbers]
3 (num_scope) [notation, in ATBR.Numbers]
2 (num_scope) [notation, in ATBR.Numbers]
1 (num_scope) [notation, in ATBR.Numbers]
0 (num_scope) [notation, in ATBR.Numbers]
NUM.code [axiom, in ATBR.Numbers]
NUM.compare [axiom, in ATBR.Numbers]
NUM.compare_spec [axiom, in ATBR.Numbers]
NUM.eqb [axiom, in ATBR.Numbers]
NUM.eq_spec [axiom, in ATBR.Numbers]
NUM.fold_num_sum_S [axiom, in ATBR.Numbers]
NUM.fold_num_sum_O [axiom, in ATBR.Numbers]
NUM.fold_num_S [axiom, in ATBR.Numbers]
NUM.fold_num_O [axiom, in ATBR.Numbers]
NUM.fold_num_sum [axiom, in ATBR.Numbers]
NUM.fold_num [axiom, in ATBR.Numbers]
NUM.id_nat [axiom, in ATBR.Numbers]
NUM.id_num [axiom, in ATBR.Numbers]
NUM.le [axiom, in ATBR.Numbers]
NUM.leb [axiom, in ATBR.Numbers]
NUM.le_nat_spec [axiom, in ATBR.Numbers]
NUM.le_spec [axiom, in ATBR.Numbers]
NUM.lt [axiom, in ATBR.Numbers]
NUM.ltb [axiom, in ATBR.Numbers]
NUM.lt_pi1 [axiom, in ATBR.Numbers]
NUM.lt_pi0 [axiom, in ATBR.Numbers]
NUM.lt_nat_spec [axiom, in ATBR.Numbers]
NUM.lt_spec [axiom, in ATBR.Numbers]
NUM.map_eq_spec [axiom, in ATBR.Numbers]
NUM.match_pi1 [axiom, in ATBR.Numbers]
NUM.match_pi0 [axiom, in ATBR.Numbers]
NUM.max [axiom, in ATBR.Numbers]
NUM.max_spec [axiom, in ATBR.Numbers]
NUM.nat_of_num [axiom, in ATBR.Numbers]
NUM.num [axiom, in ATBR.Numbers]
NUM.NumMap [module, in ATBR.Numbers]
NUM.NumOTA [module, in ATBR.Numbers]
NUM.NumSet [module, in ATBR.Numbers]
NUM.num_of_nat [axiom, in ATBR.Numbers]
NUM.pimatch [axiom, in ATBR.Numbers]
NUM.pi0 [axiom, in ATBR.Numbers]
NUM.pi1 [axiom, in ATBR.Numbers]
NUM.S [axiom, in ATBR.Numbers]
NUM.set_eq_spec [axiom, in ATBR.Numbers]
NUM.S_nat_spec [axiom, in ATBR.Numbers]
_ <= _ [notation, in ATBR.Numbers]
_ < _ [notation, in ATBR.Numbers]
0 [notation, in ATBR.Numbers]
O
oe [section, in ATBR.StrictKleeneAlgebra]oequal [inductive, in ATBR.StrictKleeneAlgebra]
oequal_equivalence [lemma, in ATBR.StrictKleeneAlgebra]
oe_none [constructor, in ATBR.StrictKleeneAlgebra]
oe_some [constructor, in ATBR.StrictKleeneAlgebra]
oe.A [variable, in ATBR.StrictKleeneAlgebra]
oe.HR [variable, in ATBR.StrictKleeneAlgebra]
oe.R [variable, in ATBR.StrictKleeneAlgebra]
oGraph [instance, in ATBR.StrictKleeneAlgebra]
oIdemSemiRing [instance, in ATBR.StrictKleeneAlgebra]
oKleeneAlgebra [instance, in ATBR.StrictKleeneAlgebra]
oMonoid [instance, in ATBR.StrictKleeneAlgebra]
oMonoid_Ops [instance, in ATBR.StrictKleeneAlgebra]
onat [definition, in ATBR.Model_MinPlus]
one [projection, in ATBR.Classes]
one [projection, in ATBR.StrictKleeneAlgebra]
one_leq_star_a [lemma, in ATBR.KleeneAlgebra]
Ops [section, in ATBR.Classes]
optionset_to_set [definition, in ATBR.DKA_Definitions]
orb_true_iff [lemma, in ATBR.BoolView]
orb_false_iff [lemma, in ATBR.BoolView]
OrderedTypeAlt [module, in ATBR.MyFSets]
OrderedTypeAlt.compare [axiom, in ATBR.MyFSets]
OrderedTypeAlt.compare_trans [axiom, in ATBR.MyFSets]
OrderedTypeAlt.compare_sym [axiom, in ATBR.MyFSets]
OrderedTypeAlt.reflect [axiom, in ATBR.MyFSets]
OrderedTypeAlt.t [axiom, in ATBR.MyFSets]
_ ?= _ [notation, in ATBR.MyFSets]
OrderedType_from_Alt.eq_dec [definition, in ATBR.MyFSets]
OrderedType_from_Alt.compare [definition, in ATBR.MyFSets]
OrderedType_from_Alt.lt_not_eq [lemma, in ATBR.MyFSets]
OrderedType_from_Alt.lt_trans [definition, in ATBR.MyFSets]
OrderedType_from_Alt.eq_trans [definition, in ATBR.MyFSets]
OrderedType_from_Alt.eq_sym [lemma, in ATBR.MyFSets]
OrderedType_from_Alt.eq_refl [lemma, in ATBR.MyFSets]
OrderedType_from_Alt.lt [definition, in ATBR.MyFSets]
OrderedType_from_Alt.eq [definition, in ATBR.MyFSets]
OrderedType_from_Alt.t [definition, in ATBR.MyFSets]
OrderedType_from_Alt [module, in ATBR.MyFSets]
oSemiLattice [instance, in ATBR.StrictKleeneAlgebra]
oSemiLattice_Ops [instance, in ATBR.StrictKleeneAlgebra]
oStar_Op [instance, in ATBR.StrictKleeneAlgebra]
P
Pack [record, in ATBR.Reification]pack [constructor, in ATBR.Reification]
PairOrderedType [module, in ATBR.MyFSets]
PairOrderedTypeAlt [module, in ATBR.MyFSets]
PairOrderedTypeAlt.compare [definition, in ATBR.MyFSets]
PairOrderedTypeAlt.compare_trans [lemma, in ATBR.MyFSets]
PairOrderedTypeAlt.compare_sym [lemma, in ATBR.MyFSets]
PairOrderedTypeAlt.reflect [lemma, in ATBR.MyFSets]
PairOrderedTypeAlt.t [definition, in ATBR.MyFSets]
PairOrderedType.P [module, in ATBR.MyFSets]
plus [projection, in ATBR.Classes]
plus [projection, in ATBR.StrictKleeneAlgebra]
plus_com [projection, in ATBR.Classes]
plus_assoc [projection, in ATBR.Classes]
plus_idem [projection, in ATBR.Classes]
plus_neutral_left [projection, in ATBR.Classes]
plus_compat [projection, in ATBR.Classes]
plus_com [projection, in ATBR.StrictKleeneAlgebra]
plus_assoc [projection, in ATBR.StrictKleeneAlgebra]
plus_idem [projection, in ATBR.StrictKleeneAlgebra]
plus_compat [projection, in ATBR.StrictKleeneAlgebra]
plus_but_one [definition, in ATBR.StrictStarForm]
plus_xif [lemma, in ATBR.SemiLattice]
plus_incr [instance, in ATBR.SemiLattice]
plus_destruct_leq [lemma, in ATBR.SemiLattice]
plus_make_right [lemma, in ATBR.SemiLattice]
plus_make_left [lemma, in ATBR.SemiLattice]
plus_neutral_right [lemma, in ATBR.SemiLattice]
plus_minus [lemma, in ATBR.MxGraph]
PosDisjointSets [module, in ATBR.DisjointSets]
PosDisjointSets.boundage [lemma, in ATBR.DisjointSets]
PosDisjointSets.boundage_link [lemma, in ATBR.DisjointSets]
PosDisjointSets.bounded [definition, in ATBR.DisjointSets]
PosDisjointSets.class_of_In_repr' [lemma, in ATBR.DisjointSets]
PosDisjointSets.class_of_In_repr [lemma, in ATBR.DisjointSets]
PosDisjointSets.class_of_In_MapsTo' [lemma, in ATBR.DisjointSets]
PosDisjointSets.class_of_In_MapsTo [lemma, in ATBR.DisjointSets]
PosDisjointSets.class_of_Equal_repr [lemma, in ATBR.DisjointSets]
PosDisjointSets.class_of_Equal_MapsTo [lemma, in ATBR.DisjointSets]
PosDisjointSets.class_of [definition, in ATBR.DisjointSets]
PosDisjointSets.class_of' [definition, in ATBR.DisjointSets]
PosDisjointSets.D [inductive, in ATBR.DisjointSets]
PosDisjointSets.DO [constructor, in ATBR.DisjointSets]
PosDisjointSets.DO_inv_In [lemma, in ATBR.DisjointSets]
PosDisjointSets.DS [constructor, in ATBR.DisjointSets]
PosDisjointSets.D_link_ex [lemma, in ATBR.DisjointSets]
PosDisjointSets.D_update_ex [lemma, in ATBR.DisjointSets]
PosDisjointSets.D_update [lemma, in ATBR.DisjointSets]
PosDisjointSets.D_inj [lemma, in ATBR.DisjointSets]
PosDisjointSets.D_succ [lemma, in ATBR.DisjointSets]
PosDisjointSets.D_inv_n [lemma, in ATBR.DisjointSets]
PosDisjointSets.D_repr [lemma, in ATBR.DisjointSets]
PosDisjointSets.empty [definition, in ATBR.DisjointSets]
PosDisjointSets.empty_WF [instance, in ATBR.DisjointSets]
PosDisjointSets.Equiv [definition, in ATBR.DisjointSets]
PosDisjointSets.equiv [definition, in ATBR.DisjointSets]
PosDisjointSets.equiv_reflexive_false [lemma, in ATBR.DisjointSets]
PosDisjointSets.Equiv_compat [instance, in ATBR.DisjointSets]
PosDisjointSets.Equiv_empty [lemma, in ATBR.DisjointSets]
PosDisjointSets.equiv_WF [instance, in ATBR.DisjointSets]
PosDisjointSets.eq_num [definition, in ATBR.DisjointSets]
PosDisjointSets.FEquiv [definition, in ATBR.DisjointSets]
PosDisjointSets.FEquiv_eq [instance, in ATBR.DisjointSets]
PosDisjointSets.FEquiv_D [lemma, in ATBR.DisjointSets]
PosDisjointSets.find [definition, in ATBR.DisjointSets]
PosDisjointSets.find_WF [instance, in ATBR.DisjointSets]
PosDisjointSets.find_spec [lemma, in ATBR.DisjointSets]
PosDisjointSets.find_spec_1 [constructor, in ATBR.DisjointSets]
PosDisjointSets.find_spec_decl [inductive, in ATBR.DisjointSets]
PosDisjointSets.find_equiv [lemma, in ATBR.DisjointSets]
PosDisjointSets.find_aux [definition, in ATBR.DisjointSets]
PosDisjointSets.get_rank [definition, in ATBR.DisjointSets]
PosDisjointSets.IsWF [definition, in ATBR.DisjointSets]
PosDisjointSets.link [definition, in ATBR.DisjointSets]
PosDisjointSets.link_WF [instance, in ATBR.DisjointSets]
PosDisjointSets.link_main_lemma [lemma, in ATBR.DisjointSets]
PosDisjointSets.link_lemma_2 [lemma, in ATBR.DisjointSets]
PosDisjointSets.link_lemma_1 [lemma, in ATBR.DisjointSets]
PosDisjointSets.MapsTo_sameclass [lemma, in ATBR.DisjointSets]
PosDisjointSets.num [definition, in ATBR.DisjointSets]
PosDisjointSets.NumMap_Equal_Empty_empty [lemma, in ATBR.DisjointSets]
PosDisjointSets.NumMap_fold_compat [lemma, in ATBR.DisjointSets]
PosDisjointSets.p [projection, in ATBR.DisjointSets]
PosDisjointSets.protect [section, in ATBR.DisjointSets]
PosDisjointSets.protect.Equiv [section, in ATBR.DisjointSets]
PosDisjointSets.protect.find_aux [section, in ATBR.DisjointSets]
PosDisjointSets.protect.link [section, in ATBR.DisjointSets]
PosDisjointSets.protect.link.a [variable, in ATBR.DisjointSets]
PosDisjointSets.protect.link.a_diff_b [variable, in ATBR.DisjointSets]
PosDisjointSets.protect.link.b [variable, in ATBR.DisjointSets]
PosDisjointSets.protect.link.repr_b [variable, in ATBR.DisjointSets]
PosDisjointSets.protect.link.repr_a [variable, in ATBR.DisjointSets]
PosDisjointSets.protect.link.t [variable, in ATBR.DisjointSets]
PosDisjointSets.protect.repr [section, in ATBR.DisjointSets]
PosDisjointSets.protect.repr.t [variable, in ATBR.DisjointSets]
PosDisjointSets.protect.update [section, in ATBR.DisjointSets]
PosDisjointSets.protect.update.a [variable, in ATBR.DisjointSets]
PosDisjointSets.protect.update.a_repr_b [variable, in ATBR.DisjointSets]
PosDisjointSets.protect.update.a_diff_b [variable, in ATBR.DisjointSets]
PosDisjointSets.protect.update.b [variable, in ATBR.DisjointSets]
PosDisjointSets.protect.update.t [variable, in ATBR.DisjointSets]
PosDisjointSets.protect.WF [section, in ATBR.DisjointSets]
_ [ _ >- _ ] [notation, in ATBR.DisjointSets]
_ [ _ ] [notation, in ATBR.DisjointSets]
[] [notation, in ATBR.DisjointSets]
PosDisjointSets.rank [projection, in ATBR.DisjointSets]
PosDisjointSets.repr [inductive, in ATBR.DisjointSets]
PosDisjointSets.repr_helper [lemma, in ATBR.DisjointSets]
PosDisjointSets.repr_inv_upd [lemma, in ATBR.DisjointSets]
PosDisjointSets.repr_x_inv_upd [lemma, in ATBR.DisjointSets]
PosDisjointSets.repr_update_fwd [lemma, in ATBR.DisjointSets]
PosDisjointSets.repr_compat [instance, in ATBR.DisjointSets]
PosDisjointSets.repr_D [lemma, in ATBR.DisjointSets]
PosDisjointSets.repr_idem [lemma, in ATBR.DisjointSets]
PosDisjointSets.repr_inj_idem [lemma, in ATBR.DisjointSets]
PosDisjointSets.repr_inv_In [lemma, in ATBR.DisjointSets]
PosDisjointSets.repr_inj_right [lemma, in ATBR.DisjointSets]
PosDisjointSets.repr_zero_inv [lemma, in ATBR.DisjointSets]
PosDisjointSets.rsucc [constructor, in ATBR.DisjointSets]
PosDisjointSets.rzero [constructor, in ATBR.DisjointSets]
PosDisjointSets.S [abbreviation, in ATBR.DisjointSets]
PosDisjointSets.sameclass [definition, in ATBR.DisjointSets]
PosDisjointSets.sameclass_class_of [lemma, in ATBR.DisjointSets]
PosDisjointSets.sameclass_equiv' [lemma, in ATBR.DisjointSets]
PosDisjointSets.sameclass_find [lemma, in ATBR.DisjointSets]
PosDisjointSets.sameclass_equiv [lemma, in ATBR.DisjointSets]
PosDisjointSets.sameclass_union [lemma, in ATBR.DisjointSets]
PosDisjointSets.sameclass_Equivalence [instance, in ATBR.DisjointSets]
PosDisjointSets.sameclass_empty [lemma, in ATBR.DisjointSets]
PosDisjointSets.size [projection, in ATBR.DisjointSets]
PosDisjointSets.T [definition, in ATBR.DisjointSets]
PosDisjointSets.test_and_unify_eq [lemma, in ATBR.DisjointSets]
PosDisjointSets.test_and_unify_WF [instance, in ATBR.DisjointSets]
PosDisjointSets.test_and_unify [definition, in ATBR.DisjointSets]
PosDisjointSets.UF [record, in ATBR.DisjointSets]
PosDisjointSets.union [definition, in ATBR.DisjointSets]
PosDisjointSets.union_WF [instance, in ATBR.DisjointSets]
PosDisjointSets.update_equiv [lemma, in ATBR.DisjointSets]
PosDisjointSets.update_In [lemma, in ATBR.DisjointSets]
PosDisjointSets.wf [projection, in ATBR.DisjointSets]
PosDisjointSets.WF [record, in ATBR.DisjointSets]
PosDisjointSets.Z [module, in ATBR.DisjointSets]
Positive [module, in ATBR.Numbers]
PositiveUtils [module, in ATBR.Numbers]
positive_size [lemma, in ATBR.DKA_Determinisation]
Positive.code [definition, in ATBR.Numbers]
Positive.compare [definition, in ATBR.Numbers]
Positive.compare_spec [lemma, in ATBR.Numbers]
Positive.enc [definition, in ATBR.Numbers]
Positive.eqb [definition, in ATBR.Numbers]
Positive.eq_spec [definition, in ATBR.Numbers]
Positive.fold_num_sum_S [lemma, in ATBR.Numbers]
Positive.fold_num_sum_O [lemma, in ATBR.Numbers]
Positive.fold_num_S [lemma, in ATBR.Numbers]
Positive.fold_num_O [lemma, in ATBR.Numbers]
Positive.fold_num_sum [definition, in ATBR.Numbers]
Positive.fold_num [definition, in ATBR.Numbers]
Positive.id_nat [lemma, in ATBR.Numbers]
Positive.id_num [lemma, in ATBR.Numbers]
Positive.le [definition, in ATBR.Numbers]
Positive.leb [definition, in ATBR.Numbers]
Positive.le_nat_spec [lemma, in ATBR.Numbers]
Positive.le_spec [lemma, in ATBR.Numbers]
Positive.lt [definition, in ATBR.Numbers]
Positive.ltb [definition, in ATBR.Numbers]
Positive.lt_pi1 [lemma, in ATBR.Numbers]
Positive.lt_pi0 [lemma, in ATBR.Numbers]
Positive.lt_nat_spec [lemma, in ATBR.Numbers]
Positive.lt_spec [lemma, in ATBR.Numbers]
Positive.map_eq_spec [lemma, in ATBR.Numbers]
Positive.match_pi1 [lemma, in ATBR.Numbers]
Positive.match_pi0 [lemma, in ATBR.Numbers]
Positive.max [definition, in ATBR.Numbers]
Positive.max_spec [lemma, in ATBR.Numbers]
Positive.nat_of_num [definition, in ATBR.Numbers]
Positive.num [definition, in ATBR.Numbers]
Positive.NumMap [module, in ATBR.Numbers]
Positive.NumMap' [module, in ATBR.Numbers]
Positive.NumOTA [module, in ATBR.Numbers]
Positive.NumSet [module, in ATBR.Numbers]
Positive.NumSet' [module, in ATBR.Numbers]
Positive.num_of_nat [definition, in ATBR.Numbers]
Positive.pcompare_prop [lemma, in ATBR.Numbers]
Positive.PeanoView_sum_iter [definition, in ATBR.Numbers]
Positive.pimatch [definition, in ATBR.Numbers]
Positive.pi0 [definition, in ATBR.Numbers]
Positive.pi1 [definition, in ATBR.Numbers]
Positive.S [definition, in ATBR.Numbers]
Positive.set_eq_spec [lemma, in ATBR.Numbers]
Positive.S_nat_spec [lemma, in ATBR.Numbers]
Positive.triangle [definition, in ATBR.Numbers]
Pos_as_OT [module, in ATBR.MyFSets]
Pos_as_OTA.reflect [lemma, in ATBR.MyFSets]
Pos_as_OTA.compare_trans [lemma, in ATBR.MyFSets]
Pos_as_OTA.compare_sym [lemma, in ATBR.MyFSets]
Pos_as_OTA.compare [definition, in ATBR.MyFSets]
Pos_as_OTA.t [definition, in ATBR.MyFSets]
Pos_as_OTA [module, in ATBR.MyFSets]
pos_eq_dec [lemma, in ATBR.Reification]
power [definition, in ATBR.Utils_WF]
powerfix [definition, in ATBR.Utils_WF]
powerfix [section, in ATBR.Utils_WF]
powerfix_invariant' [lemma, in ATBR.Utils_WF]
powerfix_linearfix [lemma, in ATBR.Utils_WF]
powerfix_compat [instance, in ATBR.Utils_WF]
powerfix' [definition, in ATBR.Utils_WF]
powerfix'_invariant' [lemma, in ATBR.Utils_WF]
powerfix'_linearfix [lemma, in ATBR.Utils_WF]
powerfix'_compat [instance, in ATBR.Utils_WF]
powerfix.A [variable, in ATBR.Utils_WF]
powerfix.B [variable, in ATBR.Utils_WF]
powerfix.invariant [section, in ATBR.Utils_WF]
powerfix.invariant.HP [variable, in ATBR.Utils_WF]
powerfix.invariant.P [variable, in ATBR.Utils_WF]
powerfix.linear_carac.Hf [variable, in ATBR.Utils_WF]
powerfix.linear_carac.f [variable, in ATBR.Utils_WF]
powerfix.linear_carac [section, in ATBR.Utils_WF]
power_positive [lemma, in ATBR.Utils_WF]
PreDefs [section, in ATBR.MxKleeneAlgebra]
PreDefs.A [variable, in ATBR.MxKleeneAlgebra]
preorder_prog [instance, in ATBR.DKA_DFA_Equiv]
preserve_max_label [lemma, in ATBR.DKA_Epsilon]
preserve_max_label [lemma, in ATBR.DKA_Determinisation]
print [definition, in ATBR.Force]
print2 [definition, in ATBR.Force]
prog [definition, in ATBR.DKA_DFA_Equiv]
Props [section, in ATBR.SemiRing]
Props [section, in ATBR.MxSemiLattice]
Props [section, in ATBR.MxGraph]
Props.A [variable, in ATBR.MxSemiLattice]
Props.A [variable, in ATBR.MxGraph]
Props.Blocks [section, in ATBR.MxGraph]
Props.Blocks.m [variable, in ATBR.MxGraph]
Props.Blocks.n [variable, in ATBR.MxGraph]
Props.Blocks.Proj [section, in ATBR.MxGraph]
Props.Blocks.Proj.a [variable, in ATBR.MxGraph]
Props.Blocks.Proj.b [variable, in ATBR.MxGraph]
Props.Blocks.Proj.c [variable, in ATBR.MxGraph]
Props.Blocks.Proj.d [variable, in ATBR.MxGraph]
Props.Blocks.x [variable, in ATBR.MxGraph]
Props.Blocks.y [variable, in ATBR.MxGraph]
Props.Subs [section, in ATBR.MxGraph]
Props.Subs.Def [section, in ATBR.MxGraph]
Props.Subs.Def.M [variable, in ATBR.MxGraph]
Props.Subs.m [variable, in ATBR.MxGraph]
Props.Subs.n [variable, in ATBR.MxGraph]
Props.Subs.x [variable, in ATBR.MxGraph]
Props.Subs.y [variable, in ATBR.MxGraph]
Props0 [section, in ATBR.KleeneAlgebra]
Props1 [section, in ATBR.MxSemiRing]
Props1 [section, in ATBR.Monoid]
Props1 [section, in ATBR.ChurchRosser]
Props1 [section, in ATBR.SemiLattice]
Props1 [section, in ATBR.KleeneAlgebra]
Props1.A [variable, in ATBR.MxSemiRing]
Props1.A [variable, in ATBR.Monoid]
Props1.A [variable, in ATBR.SemiLattice]
Props1.A [variable, in ATBR.KleeneAlgebra]
Props1.B [variable, in ATBR.Monoid]
Props1.B [variable, in ATBR.SemiLattice]
Props1.C [variable, in ATBR.Monoid]
_ ^+ [notation, in ATBR.ChurchRosser]
Props2 [section, in ATBR.MxSemiRing]
Props2 [section, in ATBR.ChurchRosser]
Props2 [section, in ATBR.KleeneAlgebra]
Props2.A [variable, in ATBR.MxSemiRing]
Props2.A [variable, in ATBR.KleeneAlgebra]
Props3 [section, in ATBR.KleeneAlgebra]
Props4 [section, in ATBR.KleeneAlgebra]
prop_star_destruct_right [definition, in ATBR.MxKleeneAlgebra]
prop_star_destruct_left [definition, in ATBR.MxKleeneAlgebra]
prop_star_make_left [definition, in ATBR.MxKleeneAlgebra]
protect [section, in ATBR.DKA_StateSetSets]
protect [section, in ATBR.Model_MinPlus]
protect [section, in ATBR.DKA_CheckLabels]
protect [section, in ATBR.DKA_DFA_Language]
protect.accept [section, in ATBR.DKA_DFA_Language]
protect.accept.A [variable, in ATBR.DKA_DFA_Language]
protect.s [section, in ATBR.DKA_DFA_Language]
protect.s.I [variable, in ATBR.DKA_DFA_Language]
protect.s.M [variable, in ATBR.DKA_DFA_Language]
protect.s.m [variable, in ATBR.DKA_DFA_Language]
protect.s.n [variable, in ATBR.DKA_DFA_Language]
R
read [definition, in ATBR.DKA_DFA_Language]read_app [lemma, in ATBR.DKA_DFA_Language]
reflexive_extends [lemma, in ATBR.DKA_Determinisation]
RegExp [module, in ATBR.Model_RegExp]
RegExp.Clean [module, in ATBR.Model_RegExp]
RegExp.Clean.clean_star [lemma, in ATBR.Model_RegExp]
RegExp.Clean.clean_plus [lemma, in ATBR.Model_RegExp]
RegExp.Clean.clean_dot [lemma, in ATBR.Model_RegExp]
RegExp.Clean.correct [lemma, in ATBR.Model_RegExp]
RegExp.Clean.equal_rewrite_zero_equiv [lemma, in ATBR.Model_RegExp]
RegExp.Clean.rewrite [definition, in ATBR.Model_RegExp]
RegExp.Clean.rewrite_idem [lemma, in ATBR.Model_RegExp]
RegExp.Clean.S [section, in ATBR.Model_RegExp]
RegExp.Clean.S.cleaning_star [variable, in ATBR.Model_RegExp]
RegExp.Clean.S.cleaning_plus [variable, in ATBR.Model_RegExp]
RegExp.Clean.S.cleaning_dot [variable, in ATBR.Model_RegExp]
RegExp.Def [section, in ATBR.Model_RegExp]
RegExp.dot [constructor, in ATBR.Model_RegExp]
RegExp.dot_compat [constructor, in ATBR.Model_RegExp]
RegExp.dot_distr_right [constructor, in ATBR.Model_RegExp]
RegExp.dot_distr_left [constructor, in ATBR.Model_RegExp]
RegExp.dot_ann_right [constructor, in ATBR.Model_RegExp]
RegExp.dot_ann_left [constructor, in ATBR.Model_RegExp]
RegExp.dot_neutral_right [constructor, in ATBR.Model_RegExp]
RegExp.dot_neutral_left [constructor, in ATBR.Model_RegExp]
RegExp.dot_assoc [constructor, in ATBR.Model_RegExp]
RegExp.equal [inductive, in ATBR.Model_RegExp]
RegExp.equal_refl [lemma, in ATBR.Model_RegExp]
RegExp.equal_sym [constructor, in ATBR.Model_RegExp]
RegExp.equal_trans [constructor, in ATBR.Model_RegExp]
RegExp.Is_one [lemma, in ATBR.Model_RegExp]
RegExp.Is_zero [lemma, in ATBR.Model_RegExp]
RegExp.is_one [definition, in ATBR.Model_RegExp]
RegExp.is_zero [definition, in ATBR.Model_RegExp]
RegExp.Load [module, in ATBR.Model_RegExp]
RegExp.Load.KMX [abbreviation, in ATBR.Model_RegExp]
RegExp.Load.regex [abbreviation, in ATBR.Model_RegExp]
RegExp.Load.tt [abbreviation, in ATBR.Model_RegExp]
RegExp.Load.var [abbreviation, in ATBR.Model_RegExp]
RegExp.one [constructor, in ATBR.Model_RegExp]
RegExp.plus [constructor, in ATBR.Model_RegExp]
RegExp.plus_compat [constructor, in ATBR.Model_RegExp]
RegExp.plus_com [constructor, in ATBR.Model_RegExp]
RegExp.plus_assoc [constructor, in ATBR.Model_RegExp]
RegExp.plus_idem [constructor, in ATBR.Model_RegExp]
RegExp.plus_neutral_left [constructor, in ATBR.Model_RegExp]
RegExp.refl_var [constructor, in ATBR.Model_RegExp]
RegExp.refl_zero [constructor, in ATBR.Model_RegExp]
RegExp.refl_one [constructor, in ATBR.Model_RegExp]
RegExp.regex [inductive, in ATBR.Model_RegExp]
RegExp.re_KleeneAlgebra [instance, in ATBR.Model_RegExp]
RegExp.re_SemiRing [instance, in ATBR.Model_RegExp]
RegExp.re_Monoid [instance, in ATBR.Model_RegExp]
RegExp.re_SemiLattice [instance, in ATBR.Model_RegExp]
RegExp.re_Star_Op [instance, in ATBR.Model_RegExp]
RegExp.re_Monoid_Ops [instance, in ATBR.Model_RegExp]
RegExp.re_SemiLattice_Ops [instance, in ATBR.Model_RegExp]
RegExp.re_Graph [instance, in ATBR.Model_RegExp]
RegExp.star [constructor, in ATBR.Model_RegExp]
RegExp.star_compat [constructor, in ATBR.Model_RegExp]
RegExp.star_destruct_right [constructor, in ATBR.Model_RegExp]
RegExp.star_destruct_left [constructor, in ATBR.Model_RegExp]
RegExp.star_make_right [constructor, in ATBR.Model_RegExp]
RegExp.star_make_left [constructor, in ATBR.Model_RegExp]
RegExp.Untype [module, in ATBR.Model_RegExp]
RegExp.Untype.and_idem [lemma, in ATBR.Model_RegExp]
RegExp.Untype.clean [abbreviation, in ATBR.Model_RegExp]
RegExp.Untype.equal_eval [lemma, in ATBR.Model_RegExp]
RegExp.Untype.equal_to_sequal [lemma, in ATBR.Model_RegExp]
RegExp.Untype.erase [definition, in ATBR.Model_RegExp]
RegExp.Untype.erase_faithful [lemma, in ATBR.Model_RegExp]
RegExp.Untype.eval [inductive, in ATBR.Model_RegExp]
RegExp.Untype.eval_sequal [lemma, in ATBR.Model_RegExp]
RegExp.Untype.eval_inj [lemma, in ATBR.Model_RegExp]
RegExp.Untype.eval_clean [lemma, in ATBR.Model_RegExp]
RegExp.Untype.eval_clean_zero [lemma, in ATBR.Model_RegExp]
RegExp.Untype.eval_type_inj_right [lemma, in ATBR.Model_RegExp]
RegExp.Untype.eval_type_inj_left [lemma, in ATBR.Model_RegExp]
RegExp.Untype.eval_var_inv [lemma, in ATBR.Model_RegExp]
RegExp.Untype.eval_star_inv [lemma, in ATBR.Model_RegExp]
RegExp.Untype.eval_zero_inv [lemma, in ATBR.Model_RegExp]
RegExp.Untype.eval_plus_inv [lemma, in ATBR.Model_RegExp]
RegExp.Untype.eval_one_inv [lemma, in ATBR.Model_RegExp]
RegExp.Untype.eval_dot_inv [lemma, in ATBR.Model_RegExp]
RegExp.Untype.eval_erase_feval [lemma, in ATBR.Model_RegExp]
RegExp.Untype.e_var [constructor, in ATBR.Model_RegExp]
RegExp.Untype.e_star [constructor, in ATBR.Model_RegExp]
RegExp.Untype.e_plus [constructor, in ATBR.Model_RegExp]
RegExp.Untype.e_dot [constructor, in ATBR.Model_RegExp]
RegExp.Untype.e_zero [constructor, in ATBR.Model_RegExp]
RegExp.Untype.e_one [constructor, in ATBR.Model_RegExp]
RegExp.Untype.feval [abbreviation, in ATBR.Model_RegExp]
RegExp.Untype.normalizer [lemma, in ATBR.Model_RegExp]
RegExp.Untype.protect [section, in ATBR.Model_RegExp]
RegExp.Untype.protect.erase [section, in ATBR.Model_RegExp]
RegExp.Untype.protect.faithful [section, in ATBR.Model_RegExp]
RegExp.Untype.sequal [inductive, in ATBR.Model_RegExp]
RegExp.Untype.sequal_clean_zero_equiv [lemma, in ATBR.Model_RegExp]
RegExp.Untype.sequal_refl [lemma, in ATBR.Model_RegExp]
RegExp.Untype.sequal_equal [lemma, in ATBR.Model_RegExp]
RegExp.Untype.sequal_sym [constructor, in ATBR.Model_RegExp]
RegExp.Untype.sequal_trans [constructor, in ATBR.Model_RegExp]
RegExp.Untype.sequal_star_compat [constructor, in ATBR.Model_RegExp]
RegExp.Untype.sequal_plus_compat [constructor, in ATBR.Model_RegExp]
RegExp.Untype.sequal_dot_compat [constructor, in ATBR.Model_RegExp]
RegExp.Untype.sequal_star_destruct_right [constructor, in ATBR.Model_RegExp]
RegExp.Untype.sequal_star_destruct_left [constructor, in ATBR.Model_RegExp]
RegExp.Untype.sequal_star_make_right [constructor, in ATBR.Model_RegExp]
RegExp.Untype.sequal_star_make_left [constructor, in ATBR.Model_RegExp]
RegExp.Untype.sequal_plus_com [constructor, in ATBR.Model_RegExp]
RegExp.Untype.sequal_plus_idem [constructor, in ATBR.Model_RegExp]
RegExp.Untype.sequal_plus_assoc [constructor, in ATBR.Model_RegExp]
RegExp.Untype.sequal_dot_distr_right [constructor, in ATBR.Model_RegExp]
RegExp.Untype.sequal_dot_distr_left [constructor, in ATBR.Model_RegExp]
RegExp.Untype.sequal_dot_neutral_right [constructor, in ATBR.Model_RegExp]
RegExp.Untype.sequal_dot_neutral_left [constructor, in ATBR.Model_RegExp]
RegExp.Untype.sequal_dot_assoc [constructor, in ATBR.Model_RegExp]
RegExp.Untype.sequal_refl_var [constructor, in ATBR.Model_RegExp]
RegExp.Untype.sequal_refl_zero [constructor, in ATBR.Model_RegExp]
RegExp.Untype.sequal_refl_one [constructor, in ATBR.Model_RegExp]
RegExp.var [constructor, in ATBR.Model_RegExp]
RegExp.zero [constructor, in ATBR.Model_RegExp]
regex_language_kleene_functor [instance, in ATBR.DKA_DFA_Language]
regex_language_graph_functor [instance, in ATBR.DKA_DFA_Language]
regex_language_f [definition, in ATBR.DKA_DFA_Language]
regex_language [definition, in ATBR.DKA_DFA_Language]
Reification [library]
rel [definition, in ATBR.Model_Relations]
rel_KleeneAlgebra [definition, in ATBR.Model_Relations]
rel_ConverseKleeneAlgebra [instance, in ATBR.Model_Relations]
rel_leq [lemma, in ATBR.Model_Relations]
rel_IdemSemiRing [definition, in ATBR.Model_Relations]
rel_ConverseSemiRing [instance, in ATBR.Model_Relations]
rel_SemiLattice [instance, in ATBR.Model_Relations]
rel_Converse_Op [instance, in ATBR.Model_Relations]
rel_Star_Op [instance, in ATBR.Model_Relations]
rel_Monoid_Ops [instance, in ATBR.Model_Relations]
rel_SemiLattice_Ops [instance, in ATBR.Model_Relations]
rel_Graph [instance, in ATBR.Model_Relations]
rel_star [definition, in ATBR.Model_Relations]
rel_iter [definition, in ATBR.Model_Relations]
rel_top [definition, in ATBR.Model_Relations]
rel_empty [definition, in ATBR.Model_Relations]
rel_id [definition, in ATBR.Model_Relations]
rel_conv [definition, in ATBR.Model_Relations]
rel_comp [definition, in ATBR.Model_Relations]
rel_inter [definition, in ATBR.Model_Relations]
rel_union [definition, in ATBR.Model_Relations]
rel_equal [definition, in ATBR.Model_Relations]
rel_KleeneAlgebra [definition, in ATBR.Model_StdRelations]
rel_ConverseKleeneAlgebra [instance, in ATBR.Model_StdRelations]
rel_leq [lemma, in ATBR.Model_StdRelations]
rel_IdemSemiRing [definition, in ATBR.Model_StdRelations]
rel_ConverseSemiRing [instance, in ATBR.Model_StdRelations]
rel_SemiLattice [instance, in ATBR.Model_StdRelations]
rel_Converse_Op [instance, in ATBR.Model_StdRelations]
rel_Star_Op [instance, in ATBR.Model_StdRelations]
rel_Monoid_Ops [instance, in ATBR.Model_StdRelations]
rel_SemiLattice_Ops [instance, in ATBR.Model_StdRelations]
rel_Graph [instance, in ATBR.Model_StdRelations]
rel_to_wf [lemma, in ATBR.Utils_WF]
rel_to_intro [constructor, in ATBR.Utils_WF]
rel_to [inductive, in ATBR.Utils_WF]
rel_of_wf [lemma, in ATBR.Utils_WF]
rel_of [definition, in ATBR.Utils_WF]
remove [definition, in ATBR.StrictStarForm]
remove_strict [lemma, in ATBR.StrictStarForm]
remove_nf [lemma, in ATBR.StrictStarForm]
rem_cardinal_lt [lemma, in ATBR.DKA_StateSetSets]
rho [abbreviation, in ATBR.DKA_Determinisation]
rho_theta [lemma, in ATBR.DKA_Determinisation]
right_filter [lemma, in ATBR.DKA_Definitions]
rt_closure_bounded [lemma, in ATBR.DKA_Epsilon]
rt_closure_star [lemma, in ATBR.DKA_Epsilon]
rt_closure_spec [lemma, in ATBR.DKA_Epsilon]
rt_closure_prespec [lemma, in ATBR.DKA_Epsilon]
rt_closure_aux'_spec [lemma, in ATBR.DKA_Epsilon]
rt_closure_aux_spec [lemma, in ATBR.DKA_Epsilon]
rt_closure [definition, in ATBR.DKA_Epsilon]
rt_closure_aux' [definition, in ATBR.DKA_Epsilon]
rt_closure_aux [definition, in ATBR.DKA_Epsilon]
S
S [section, in ATBR.DKA_Merge]S [section, in ATBR.Reification]
S [section, in ATBR.DKA_Determinisation]
same_labels_ssf [lemma, in ATBR.DKA_CheckLabels]
same_labels [definition, in ATBR.DKA_CheckLabels]
same_labels_max_label [lemma, in ATBR.DKA_Construction]
select [definition, in ATBR.DKA_DFA_Equiv]
semicomm_iter_left [lemma, in ATBR.KleeneAlgebra]
semicomm_iter_right [lemma, in ATBR.KleeneAlgebra]
SemiConfluence_is_ChurchRosser [lemma, in ATBR.ChurchRosser]
SemiConfluence_is_WeakConfluence [lemma, in ATBR.ChurchRosser]
SemiLattice [record, in ATBR.Classes]
SemiLattice [library]
SemiLattice_Ops [record, in ATBR.Classes]
semilattice_graph_functor [projection, in ATBR.Functors]
semilattice_functor [record, in ATBR.Functors]
Semiring [module, in ATBR.Reification]
SemiRing [library]
semiring_semilattice_functor [projection, in ATBR.Functors]
semiring_monoid_functor [projection, in ATBR.Functors]
semiring_functor [record, in ATBR.Functors]
Semiring.dot [constructor, in ATBR.Reification]
Semiring.eval [definition, in ATBR.Reification]
Semiring.one [constructor, in ATBR.Reification]
Semiring.plus [constructor, in ATBR.Reification]
Semiring.S [section, in ATBR.Reification]
Semiring.var [constructor, in ATBR.Reification]
Semiring.X [inductive, in ATBR.Reification]
Semiring.zero [constructor, in ATBR.Reification]
semi_invert_right [lemma, in ATBR.SemiRing]
semi_invert_left [lemma, in ATBR.SemiRing]
setbelow [definition, in ATBR.DKA_Definitions]
Setting [section, in ATBR.Examples]
set_closure [definition, in ATBR.DKA_Epsilon]
sigma [definition, in ATBR.Reification]
sigma_empty [definition, in ATBR.Reification]
sigma_add [definition, in ATBR.Reification]
sigma_get [definition, in ATBR.Reification]
simpl_regex_language [lemma, in ATBR.DKA_DFA_Language]
simulation [lemma, in ATBR.DKA_DFA_Equiv]
size [abbreviation, in ATBR.DKA_DFA_Equiv]
size [abbreviation, in ATBR.DKA_Determinisation]
size' [abbreviation, in ATBR.DKA_Determinisation]
SKA_Ops [record, in ATBR.StrictKleeneAlgebra]
SMX [abbreviation, in ATBR.MxKleeneAlgebra]
SMX [abbreviation, in ATBR.MxKleeneAlgebra]
sn [abbreviation, in ATBR.DKA_Epsilon]
square_triangular_blocks [lemma, in ATBR.Examples]
square_constant [lemma, in ATBR.Examples]
src [definition, in ATBR.Reification]
src_p [projection, in ATBR.Reification]
ssf [definition, in ATBR.StrictStarForm]
ssf_complete [lemma, in ATBR.StrictStarForm]
ssf_correct' [lemma, in ATBR.StrictStarForm]
ssf_correct [lemma, in ATBR.StrictStarForm]
ssf_dot [constructor, in ATBR.StrictStarForm]
ssf_plus [constructor, in ATBR.StrictStarForm]
ssf_star [constructor, in ATBR.StrictStarForm]
ssf_var [constructor, in ATBR.StrictStarForm]
ssf_one [constructor, in ATBR.StrictStarForm]
ssf_zero [constructor, in ATBR.StrictStarForm]
sssm [section, in ATBR.DKA_StateSetSets]
sssm.f [variable, in ATBR.DKA_StateSetSets]
sssm.Hf [variable, in ATBR.DKA_StateSetSets]
sssm.t0 [variable, in ATBR.DKA_StateSetSets]
star [projection, in ATBR.Classes]
star [projection, in ATBR.StrictKleeneAlgebra]
star_destruct_left_c [projection, in ATBR.Classes]
star_make_left_c [projection, in ATBR.Classes]
star_destruct_right [projection, in ATBR.Classes]
star_destruct_left [projection, in ATBR.Classes]
star_make_left [projection, in ATBR.Classes]
Star_Op [record, in ATBR.Classes]
star_destruct_left_old' [lemma, in ATBR.Converse]
star_destruct_right [projection, in ATBR.StrictKleeneAlgebra]
star_destruct_left [projection, in ATBR.StrictKleeneAlgebra]
star_make_left [projection, in ATBR.StrictKleeneAlgebra]
star_plus_star [lemma, in ATBR.ChurchRosser]
star_plus_one [lemma, in ATBR.ChurchRosser]
star_remove [lemma, in ATBR.StrictStarForm]
star_plus_star_dot [lemma, in ATBR.StrictStarForm]
star_dot_leq_star_plus [lemma, in ATBR.StrictStarForm]
star_plus_but_one [lemma, in ATBR.StrictStarForm]
star_plus_star [lemma, in ATBR.StrictStarForm]
star_plus_star_1 [lemma, in ATBR.StrictStarForm]
star_plus_one [lemma, in ATBR.StrictStarForm]
star_rec [definition, in ATBR.MxKleeneAlgebra]
star_build [definition, in ATBR.MxKleeneAlgebra]
star_distr [lemma, in ATBR.KleeneAlgebra]
star_idem [lemma, in ATBR.KleeneAlgebra]
star_trans [lemma, in ATBR.KleeneAlgebra]
star_make_right [lemma, in ATBR.KleeneAlgebra]
star_a_a_leq_star_a [lemma, in ATBR.KleeneAlgebra]
star_zero [lemma, in ATBR.KleeneAlgebra]
star_one [lemma, in ATBR.KleeneAlgebra]
star_mon_is_one [lemma, in ATBR.KleeneAlgebra]
star_compat [instance, in ATBR.KleeneAlgebra]
star_incr [instance, in ATBR.KleeneAlgebra]
star_destruct_left_one [lemma, in ATBR.KleeneAlgebra]
star_destruct_right_one [lemma, in ATBR.KleeneAlgebra]
star_destruct_left_old [lemma, in ATBR.KleeneAlgebra]
star_destruct_right_old [lemma, in ATBR.KleeneAlgebra]
star_distr [lemma, in ATBR.Examples]
star' [definition, in ATBR.StrictStarForm]
star'_star [lemma, in ATBR.StrictStarForm]
state [abbreviation, in ATBR.DKA_Definitions]
StateLabel [module, in ATBR.DKA_Definitions]
statelabelmap [abbreviation, in ATBR.DKA_Definitions]
StateLabelMap [module, in ATBR.DKA_Definitions]
StateLabelMapProps [module, in ATBR.DKA_Definitions]
statelabelmap_set_to_fun [definition, in ATBR.DKA_Epsilon]
statelabelmap_set_to_fun [definition, in ATBR.DKA_Construction]
StateLabelMap' [module, in ATBR.DKA_Definitions]
statemap [abbreviation, in ATBR.DKA_Definitions]
StateMap [module, in ATBR.DKA_Definitions]
statemapelt_of_nat [definition, in ATBR.DKA_Definitions]
StateMapProps [module, in ATBR.DKA_Definitions]
statemap_set_to_fun [definition, in ATBR.DKA_Definitions]
stateset [abbreviation, in ATBR.DKA_Definitions]
StateSet [module, in ATBR.DKA_Definitions]
statesetelt_of_nat [definition, in ATBR.DKA_Definitions]
statesetmap [abbreviation, in ATBR.DKA_StateSetSets]
StateSetMap [module, in ATBR.DKA_StateSetSets]
StateSetMapProps [module, in ATBR.DKA_StateSetSets]
StateSetMap' [module, in ATBR.DKA_StateSetSets]
StateSetProps [module, in ATBR.DKA_Definitions]
statesetset [abbreviation, in ATBR.DKA_StateSetSets]
StateSetSet [module, in ATBR.DKA_StateSetSets]
StateSetSetProps [module, in ATBR.DKA_StateSetSets]
statesetset_map_cardinal [lemma, in ATBR.DKA_StateSetSets]
statesetset_map_in [lemma, in ATBR.DKA_StateSetSets]
statesetset_map [definition, in ATBR.DKA_StateSetSets]
StateSetSet' [module, in ATBR.DKA_StateSetSets]
stateset_fold_rec_bis [lemma, in ATBR.DKA_Epsilon]
stateset_fold [definition, in ATBR.DKA_Epsilon]
state_of_nat [abbreviation, in ATBR.DKA_Definitions]
step [definition, in ATBR.DKA_Epsilon]
step [definition, in ATBR.DKA_Determinisation]
steps [definition, in ATBR.DKA_Epsilon]
steps [definition, in ATBR.DKA_Determinisation]
steps_correct [lemma, in ATBR.DKA_Determinisation]
step_compat [instance, in ATBR.DKA_Determinisation]
step' [definition, in ATBR.DKA_Determinisation]
Store [abbreviation, in ATBR.DKA_Determinisation]
store_size_bound [lemma, in ATBR.DKA_Determinisation]
strict [inductive, in ATBR.StrictStarForm]
StrictKleeneAlgebra [record, in ATBR.StrictKleeneAlgebra]
StrictKleeneAlgebra [library]
StrictStarForm [library]
strict_star_form [inductive, in ATBR.StrictStarForm]
strict_dot_r [constructor, in ATBR.StrictStarForm]
strict_dot_l [constructor, in ATBR.StrictStarForm]
strict_plus [constructor, in ATBR.StrictStarForm]
strict_var [constructor, in ATBR.StrictStarForm]
strict_zero [constructor, in ATBR.StrictStarForm]
Structures [section, in ATBR.Classes]
sum [definition, in ATBR.SemiLattice]
sum_collapse' [lemma, in ATBR.DKA_Merge]
sum_distr_left [lemma, in ATBR.SemiRing]
sum_distr_right [lemma, in ATBR.SemiRing]
sum_fixed_xif_zero [lemma, in ATBR.SemiLattice]
sum_incr' [instance, in ATBR.SemiLattice]
sum_incr [lemma, in ATBR.SemiLattice]
sum_collapse [lemma, in ATBR.SemiLattice]
sum_constant [lemma, in ATBR.SemiLattice]
sum_plus [lemma, in ATBR.SemiLattice]
sum_leq [lemma, in ATBR.SemiLattice]
sum_inversion [lemma, in ATBR.SemiLattice]
sum_shift [lemma, in ATBR.SemiLattice]
sum_cut_nth [lemma, in ATBR.SemiLattice]
sum_cut_fun [lemma, in ATBR.SemiLattice]
sum_cut [lemma, in ATBR.SemiLattice]
sum_fun_zero [lemma, in ATBR.SemiLattice]
sum_zero [lemma, in ATBR.SemiLattice]
sum_compat' [instance, in ATBR.SemiLattice]
sum_compat [lemma, in ATBR.SemiLattice]
sum_enter_right [lemma, in ATBR.SemiLattice]
sum_enter_left [lemma, in ATBR.SemiLattice]
sum_empty [lemma, in ATBR.SemiLattice]
sup_def [lemma, in ATBR.SemiLattice]
switch [lemma, in ATBR.SemiLattice]
S.A [variable, in ATBR.DKA_Determinisation]
S.equiv [variable, in ATBR.DKA_Merge]
S.equiv_correct [variable, in ATBR.DKA_Merge]
S.HA [variable, in ATBR.DKA_Determinisation]
S.T [variable, in ATBR.DKA_Merge]
_ %s [notation, in ATBR.DKA_Determinisation]
_ %d [notation, in ATBR.DKA_Determinisation]
_ %t [notation, in ATBR.DKA_Determinisation]
T
T [projection, in ATBR.Classes]table [abbreviation, in ATBR.DKA_Determinisation]
Table [abbreviation, in ATBR.DKA_Determinisation]
table_finals_complete [lemma, in ATBR.DKA_Determinisation]
table_finals_correct [lemma, in ATBR.DKA_Determinisation]
table_finals [definition, in ATBR.DKA_Determinisation]
Tactics [section, in ATBR.Examples]
Tactics.DKA [section, in ATBR.Examples]
Tactics.DKA.a [variable, in ATBR.Examples]
Tactics.DKA.A [variable, in ATBR.Examples]
Tactics.DKA.b [variable, in ATBR.Examples]
Tactics.DKA.B [variable, in ATBR.Examples]
Tactics.DKA.c [variable, in ATBR.Examples]
Tactics.DKA.d [variable, in ATBR.Examples]
Tactics.DKA.e [variable, in ATBR.Examples]
Tactics.ISR [section, in ATBR.Examples]
Tactics.ISR.a [variable, in ATBR.Examples]
Tactics.ISR.A [variable, in ATBR.Examples]
Tactics.ISR.b [variable, in ATBR.Examples]
Tactics.ISR.B [variable, in ATBR.Examples]
Tactics.ISR.c [variable, in ATBR.Examples]
Tactics.ISR.d [variable, in ATBR.Examples]
tarjan_wf [instance, in ATBR.DKA_DFA_Equiv]
tarjan_correct [lemma, in ATBR.DKA_DFA_Equiv]
tarjan_equiv_true [lemma, in ATBR.DKA_DFA_Equiv]
terminates [definition, in ATBR.DKA_Epsilon]
tgt [definition, in ATBR.Reification]
tgt_p [projection, in ATBR.Reification]
theta [definition, in ATBR.DKA_Determinisation]
theta_0 [lemma, in ATBR.DKA_Determinisation]
theta_delta' [lemma, in ATBR.DKA_Determinisation]
theta_below [lemma, in ATBR.DKA_Determinisation]
theta_rho [lemma, in ATBR.DKA_Determinisation]
transitive_extends [instance, in ATBR.DKA_Determinisation]
translate_correct [lemma, in ATBR.DecideKleeneAlgebra]
translate_ce [definition, in ATBR.DecideKleeneAlgebra]
typ [projection, in ATBR.Reification]
type_view [projection, in ATBR.BoolView]
type_view_ty [projection, in ATBR.BoolView]
Type_View [record, in ATBR.BoolView]
T_refl [lemma, in ATBR.DKA_DFA_Equiv]
T_finaux [lemma, in ATBR.DKA_DFA_Equiv]
T_true [lemma, in ATBR.DKA_DFA_Equiv]
U
U [module, in ATBR.SemiRing]Unnamed_thm [definition, in ATBR.ChurchRosser_Points_vs_Algebraic]
Unnamed_thm15 [definition, in ATBR.Examples]
Unnamed_thm14 [definition, in ATBR.Examples]
Unnamed_thm13 [definition, in ATBR.Examples]
Unnamed_thm12 [definition, in ATBR.Examples]
Unnamed_thm11 [definition, in ATBR.Examples]
Unnamed_thm10 [definition, in ATBR.Examples]
Unnamed_thm9 [definition, in ATBR.Examples]
Unnamed_thm8 [definition, in ATBR.Examples]
Unnamed_thm7 [definition, in ATBR.Examples]
Unnamed_thm6 [definition, in ATBR.Examples]
Unnamed_thm5 [definition, in ATBR.Examples]
Unnamed_thm4 [definition, in ATBR.Examples]
Unnamed_thm3 [definition, in ATBR.Examples]
Unnamed_thm2 [definition, in ATBR.Examples]
Unnamed_thm1 [definition, in ATBR.Examples]
Unnamed_thm0 [definition, in ATBR.Examples]
Unnamed_thm [definition, in ATBR.Examples]
unpack [projection, in ATBR.Reification]
Utils_WF [library]
U.and_idem [lemma, in ATBR.SemiRing]
U.cdot [definition, in ATBR.SemiRing]
U.cdot_correct [lemma, in ATBR.SemiRing]
U.clean_assoc_correct [lemma, in ATBR.SemiRing]
U.clean_assoc_aux [lemma, in ATBR.SemiRing]
U.clean_correct [lemma, in ATBR.SemiRing]
U.clean_prod [definition, in ATBR.SemiRing]
U.clean_sum [definition, in ATBR.SemiRing]
U.clean0 [definition, in ATBR.SemiRing]
U.clean0_idem [lemma, in ATBR.SemiRing]
U.clean0_correct [lemma, in ATBR.SemiRing]
U.clean1 [definition, in ATBR.SemiRing]
U.clean1_correct [lemma, in ATBR.SemiRing]
U.correctness [section, in ATBR.SemiRing]
U.cplus [definition, in ATBR.SemiRing]
U.cplus_correct [lemma, in ATBR.SemiRing]
U.decide [definition, in ATBR.SemiRing]
U.decide_typed [lemma, in ATBR.SemiRing]
U.decide_correct [lemma, in ATBR.SemiRing]
U.dot [constructor, in ATBR.SemiRing]
U.dot_compat_free [instance, in ATBR.SemiRing]
U.dot_compat [constructor, in ATBR.SemiRing]
U.dot_distr_right [constructor, in ATBR.SemiRing]
U.dot_distr_left [constructor, in ATBR.SemiRing]
U.dot_ann_right [constructor, in ATBR.SemiRing]
U.dot_ann_left [constructor, in ATBR.SemiRing]
U.dot_neutral_right [constructor, in ATBR.SemiRing]
U.dot_neutral_left [constructor, in ATBR.SemiRing]
U.dot_assoc [constructor, in ATBR.SemiRing]
U.equal [inductive, in ATBR.SemiRing]
U.equal_eval [lemma, in ATBR.SemiRing]
U.equal_to_sequal [lemma, in ATBR.SemiRing]
U.equal_clean_zero_equiv [lemma, in ATBR.SemiRing]
U.equal_refl [lemma, in ATBR.SemiRing]
U.equal_sym [constructor, in ATBR.SemiRing]
U.equal_trans [constructor, in ATBR.SemiRing]
U.equivalence_equal [instance, in ATBR.SemiRing]
U.erase [definition, in ATBR.SemiRing]
U.erase [section, in ATBR.SemiRing]
U.erase_faithful [lemma, in ATBR.SemiRing]
U.eval [inductive, in ATBR.SemiRing]
U.eval_sequal [lemma, in ATBR.SemiRing]
U.eval_inj [lemma, in ATBR.SemiRing]
U.eval_clean [lemma, in ATBR.SemiRing]
U.eval_clean_zero [lemma, in ATBR.SemiRing]
U.eval_type_inj_right [lemma, in ATBR.SemiRing]
U.eval_type_inj_left [lemma, in ATBR.SemiRing]
U.eval_var_inv [lemma, in ATBR.SemiRing]
U.eval_zero_inv [lemma, in ATBR.SemiRing]
U.eval_plus_inv [lemma, in ATBR.SemiRing]
U.eval_one_inv [lemma, in ATBR.SemiRing]
U.eval_dot_inv [lemma, in ATBR.SemiRing]
U.eval_erase_feval [lemma, in ATBR.SemiRing]
U.e_var [constructor, in ATBR.SemiRing]
U.e_plus [constructor, in ATBR.SemiRing]
U.e_dot [constructor, in ATBR.SemiRing]
U.e_zero [constructor, in ATBR.SemiRing]
U.e_one [constructor, in ATBR.SemiRing]
U.faithful [section, in ATBR.SemiRing]
U.fdot [definition, in ATBR.SemiRing]
U.feval [abbreviation, in ATBR.SemiRing]
U.fplus [definition, in ATBR.SemiRing]
U.Hdc [lemma, in ATBR.SemiRing]
U.Hpc [lemma, in ATBR.SemiRing]
U.Hpt [lemma, in ATBR.SemiRing]
U.Is_one [lemma, in ATBR.SemiRing]
U.Is_zero [lemma, in ATBR.SemiRing]
U.is_one [definition, in ATBR.SemiRing]
U.is_zero [definition, in ATBR.SemiRing]
U.lambda_and_r [lemma, in ATBR.SemiRing]
U.lambda_and_l [lemma, in ATBR.SemiRing]
U.norm [definition, in ATBR.SemiRing]
U.normalizer [lemma, in ATBR.SemiRing]
U.normalize_aux [lemma, in ATBR.SemiRing]
U.norm_correct [lemma, in ATBR.SemiRing]
U.norm_aux' [definition, in ATBR.SemiRing]
U.norm_aux [definition, in ATBR.SemiRing]
U.one [constructor, in ATBR.SemiRing]
U.plus [constructor, in ATBR.SemiRing]
U.plus_compat_free [instance, in ATBR.SemiRing]
U.plus_compat [constructor, in ATBR.SemiRing]
U.plus_com [constructor, in ATBR.SemiRing]
U.plus_assoc [constructor, in ATBR.SemiRing]
U.plus_idem [constructor, in ATBR.SemiRing]
U.plus_neutral_left [constructor, in ATBR.SemiRing]
U.refl_var [constructor, in ATBR.SemiRing]
U.refl_zero [constructor, in ATBR.SemiRing]
U.refl_one [constructor, in ATBR.SemiRing]
U.S [abbreviation, in ATBR.SemiRing]
U.sequal [inductive, in ATBR.SemiRing]
U.sequal_clean_zero_equiv [lemma, in ATBR.SemiRing]
U.sequal_refl [lemma, in ATBR.SemiRing]
U.sequal_equal [lemma, in ATBR.SemiRing]
U.sequal_sym [constructor, in ATBR.SemiRing]
U.sequal_trans [constructor, in ATBR.SemiRing]
U.sequal_plus_compat [constructor, in ATBR.SemiRing]
U.sequal_dot_compat [constructor, in ATBR.SemiRing]
U.sequal_plus_com [constructor, in ATBR.SemiRing]
U.sequal_plus_idem [constructor, in ATBR.SemiRing]
U.sequal_plus_assoc [constructor, in ATBR.SemiRing]
U.sequal_dot_distr_right [constructor, in ATBR.SemiRing]
U.sequal_dot_distr_left [constructor, in ATBR.SemiRing]
U.sequal_dot_neutral_right [constructor, in ATBR.SemiRing]
U.sequal_dot_neutral_left [constructor, in ATBR.SemiRing]
U.sequal_dot_assoc [constructor, in ATBR.SemiRing]
U.sequal_refl_var [constructor, in ATBR.SemiRing]
U.sequal_refl_zero [constructor, in ATBR.SemiRing]
U.sequal_refl_one [constructor, in ATBR.SemiRing]
U.size [definition, in ATBR.SemiRing]
U.var [constructor, in ATBR.SemiRing]
U.VLSet [module, in ATBR.SemiRing]
U.VLSetProps [module, in ATBR.SemiRing]
U.VLSet_to_X_compat [lemma, in ATBR.SemiRing]
U.VLSet_add [lemma, in ATBR.SemiRing]
U.VLSet_to_X [definition, in ATBR.SemiRing]
U.VLSet' [module, in ATBR.SemiRing]
U.VLst [module, in ATBR.SemiRing]
U.VLstA [module, in ATBR.SemiRing]
U.VLst_to_X_compat [lemma, in ATBR.SemiRing]
U.VLst_add [lemma, in ATBR.SemiRing]
U.VLst_to_X [definition, in ATBR.SemiRing]
U.X [inductive, in ATBR.SemiRing]
U.X_to_VLSet [definition, in ATBR.SemiRing]
U.zero [constructor, in ATBR.SemiRing]
V
val [projection, in ATBR.Reification]valid [definition, in ATBR.DKA_Epsilon]
valid [lemma, in ATBR.DKA_DFA_Equiv]
W
WeakConfluence [definition, in ATBR.ChurchRosser_Points_vs_Algebraic]WeakConfluence_is_ChurchRosser_plus [lemma, in ATBR.ChurchRosser]
WeakConfluence_is_ChurchRosser [lemma, in ATBR.ChurchRosser]
WeakConfluence_is_ChurchRosser3 [lemma, in ATBR.ChurchRosser_Points_vs_Algebraic]
WeakConfluence_is_ChurchRosser2 [lemma, in ATBR.ChurchRosser_Points_vs_Algebraic]
WeakConfluence_is_ChurchRosser1 [lemma, in ATBR.ChurchRosser_Points_vs_Algebraic]
WeakConfluence_is_ChurchRosser0' [lemma, in ATBR.ChurchRosser_Points_vs_Algebraic]
WeakConfluence_is_ChurchRosser0 [lemma, in ATBR.ChurchRosser_Points_vs_Algebraic]
well_founded [lemma, in ATBR.DKA_Construction]
wf_add_pair [lemma, in ATBR.Utils_WF]
wf_lexico_incl.H [variable, in ATBR.Utils_WF]
wf_lexico_incl.R [variable, in ATBR.Utils_WF]
wf_lexico_incl.HRB [variable, in ATBR.Utils_WF]
wf_lexico_incl.HRA [variable, in ATBR.Utils_WF]
wf_lexico_incl.RB [variable, in ATBR.Utils_WF]
wf_lexico_incl.RA [variable, in ATBR.Utils_WF]
wf_lexico_incl.f [variable, in ATBR.Utils_WF]
wf_lexico_incl.B [variable, in ATBR.Utils_WF]
wf_lexico_incl.A [variable, in ATBR.Utils_WF]
wf_lexico_incl.U [variable, in ATBR.Utils_WF]
wf_lexico_incl [section, in ATBR.Utils_WF]
wf_to.HR [variable, in ATBR.Utils_WF]
wf_to.R [variable, in ATBR.Utils_WF]
wf_to.f [variable, in ATBR.Utils_WF]
wf_to.V [variable, in ATBR.Utils_WF]
wf_to.U [variable, in ATBR.Utils_WF]
wf_to [section, in ATBR.Utils_WF]
wf_of.HR [variable, in ATBR.Utils_WF]
wf_of.R [variable, in ATBR.Utils_WF]
wf_of.f [variable, in ATBR.Utils_WF]
wf_of.V [variable, in ATBR.Utils_WF]
wf_of.U [variable, in ATBR.Utils_WF]
wf_of [section, in ATBR.Utils_WF]
wf_incl.H [variable, in ATBR.Utils_WF]
wf_incl.R [variable, in ATBR.Utils_WF]
wf_incl.HS [variable, in ATBR.Utils_WF]
wf_incl.S [variable, in ATBR.Utils_WF]
wf_incl.A [variable, in ATBR.Utils_WF]
wf_incl [section, in ATBR.Utils_WF]
word [definition, in ATBR.DecideKleeneAlgebra]
Word [abbreviation, in ATBR.DKA_DFA_Language]
wsemicomm_iter_left [lemma, in ATBR.KleeneAlgebra]
wsemicomm_iter_right [lemma, in ATBR.KleeneAlgebra]
X
X [projection, in ATBR.Classes]X [abbreviation, in ATBR.MxKleeneAlgebra]
X [abbreviation, in ATBR.MxKleeneAlgebra]
X [abbreviation, in ATBR.MxGraph]
X [abbreviation, in ATBR.Examples]
xif [definition, in ATBR.Graph]
xif_negb [lemma, in ATBR.Graph]
xif_xif_or [lemma, in ATBR.Graph]
xif_xif_and [lemma, in ATBR.Graph]
xif_idem' [lemma, in ATBR.Graph]
xif_idem [lemma, in ATBR.Graph]
xif_true [lemma, in ATBR.Graph]
xif_false [lemma, in ATBR.Graph]
xif_spec [lemma, in ATBR.Graph]
xif_compat [instance, in ATBR.Graph]
xif_bool_incr [lemma, in ATBR.DKA_Epsilon]
xif_dot [lemma, in ATBR.Monoid]
xif_sum_zero [lemma, in ATBR.SemiLattice]
xif_plus [lemma, in ATBR.SemiLattice]
X_to_DFA_labels [lemma, in ATBR.DecideKleeneAlgebra]
X_to_DFA_bounded [lemma, in ATBR.DecideKleeneAlgebra]
X_to_DFA_correct [lemma, in ATBR.DecideKleeneAlgebra]
X_to_DFA [definition, in ATBR.DecideKleeneAlgebra]
X_to_eNFA [definition, in ATBR.DKA_Construction]
Z
zero [projection, in ATBR.Classes]zero_leq [lemma, in ATBR.DKA_DFA_Equiv]
zero_inf [lemma, in ATBR.SemiLattice]
other
_ *' _ (A_scope) [notation, in ATBR.MxSemiRing]_ '* _ (A_scope) [notation, in ATBR.MxSemiRing]
0 (A_scope) [notation, in ATBR.Classes]
1 (A_scope) [notation, in ATBR.Classes]
_ ` (A_scope) [notation, in ATBR.Classes]
_ # (A_scope) [notation, in ATBR.Classes]
_ + _ (A_scope) [notation, in ATBR.Classes]
_ * _ (A_scope) [notation, in ATBR.Classes]
_ <== _ (A_scope) [notation, in ATBR.Classes]
_ == _ (A_scope) [notation, in ATBR.Classes]
_ <== [ _ , _ ] _ (A_scope) [notation, in ATBR.MxSemiLattice]
_ == [ _ , _ ] _ (A_scope) [notation, in ATBR.MxGraph]
! _ (A_scope) [notation, in ATBR.MxGraph]
1 (SA_scope) [notation, in ATBR.StrictKleeneAlgebra]
_ # (SA_scope) [notation, in ATBR.StrictKleeneAlgebra]
_ + _ (SA_scope) [notation, in ATBR.StrictKleeneAlgebra]
_ * _ (SA_scope) [notation, in ATBR.StrictKleeneAlgebra]
_ <== _ (SA_scope) [notation, in ATBR.StrictKleeneAlgebra]
_ == _ (SA_scope) [notation, in ATBR.StrictKleeneAlgebra]
_ [=] _ [notation, in ATBR.Reification]
_ >> _ [notation, in ATBR.Common]
_ [=] _ [notation, in ATBR.DKA_CheckLabels]
_ +++ _ [notation, in ATBR.DKA_DFA_Equiv]
_ [=0=] _ [notation, in ATBR.DKA_Construction]
Notation Index
A
_ [=0=] _ [in ATBR.DKA_Construction]C
_ +++ _ [in ATBR.DKA_DFA_Equiv]_ =T= _ [in ATBR.DKA_DFA_Equiv]
_ =&&= _ [in ATBR.DKA_DFA_Equiv]
_ + _ [in ATBR.ChurchRosser_Points_vs_Algebraic]
_ # [in ATBR.ChurchRosser_Points_vs_Algebraic]
D
__ [=T=] _ [in ATBR.DisjointSets]
{{ _ }} [in ATBR.DisjointSets]
M
_ [==] _ [in ATBR.DKA_Definitions]N
_ <= _ (num_scope) [in ATBR.Numbers]_ < _ (num_scope) [in ATBR.Numbers]
7 (num_scope) [in ATBR.Numbers]
5 (num_scope) [in ATBR.Numbers]
3 (num_scope) [in ATBR.Numbers]
2 (num_scope) [in ATBR.Numbers]
1 (num_scope) [in ATBR.Numbers]
0 (num_scope) [in ATBR.Numbers]
_ <= _ [in ATBR.Numbers]
_ < _ [in ATBR.Numbers]
0 [in ATBR.Numbers]
O
_ ?= _ [in ATBR.MyFSets]P
_ [ _ >- _ ] [in ATBR.DisjointSets]_ [ _ ] [in ATBR.DisjointSets]
[] [in ATBR.DisjointSets]
_ ^+ [in ATBR.ChurchRosser]
S
_ %s [in ATBR.DKA_Determinisation]_ %d [in ATBR.DKA_Determinisation]
_ %t [in ATBR.DKA_Determinisation]
other
_ *' _ (A_scope) [in ATBR.MxSemiRing]_ '* _ (A_scope) [in ATBR.MxSemiRing]
0 (A_scope) [in ATBR.Classes]
1 (A_scope) [in ATBR.Classes]
_ ` (A_scope) [in ATBR.Classes]
_ # (A_scope) [in ATBR.Classes]
_ + _ (A_scope) [in ATBR.Classes]
_ * _ (A_scope) [in ATBR.Classes]
_ <== _ (A_scope) [in ATBR.Classes]
_ == _ (A_scope) [in ATBR.Classes]
_ <== [ _ , _ ] _ (A_scope) [in ATBR.MxSemiLattice]
_ == [ _ , _ ] _ (A_scope) [in ATBR.MxGraph]
! _ (A_scope) [in ATBR.MxGraph]
1 (SA_scope) [in ATBR.StrictKleeneAlgebra]
_ # (SA_scope) [in ATBR.StrictKleeneAlgebra]
_ + _ (SA_scope) [in ATBR.StrictKleeneAlgebra]
_ * _ (SA_scope) [in ATBR.StrictKleeneAlgebra]
_ <== _ (SA_scope) [in ATBR.StrictKleeneAlgebra]
_ == _ (SA_scope) [in ATBR.StrictKleeneAlgebra]
_ [=] _ [in ATBR.Reification]
_ >> _ [in ATBR.Common]
_ [=] _ [in ATBR.DKA_CheckLabels]
_ +++ _ [in ATBR.DKA_DFA_Equiv]
_ [=0=] _ [in ATBR.DKA_Construction]
Module Index
A
Algebraic [in ATBR.DKA_Construction]C
Concrete [in ATBR.DKA_Construction]Correctness [in ATBR.DKA_Construction]
D
DFA [in ATBR.DKA_Definitions]DISJOINTSETS [in ATBR.DisjointSets]
DS [in ATBR.DKA_StateSetSets]
DSUtils [in ATBR.DisjointSets]
DSUtils [in ATBR.DKA_StateSetSets]
DSUtils.Notations [in ATBR.DisjointSets]
DSUtils.NU [in ATBR.DisjointSets]
Dual [in ATBR.Classes]
Dual [in ATBR.KleeneAlgebra]
E
eNFA [in ATBR.DKA_Definitions]F
FMapHide [in ATBR.MyFSets]FSetHide [in ATBR.MyFSets]
K
KA [in ATBR.Reification]L
Label [in ATBR.DKA_Definitions]ListOrderedTypeAlt [in ATBR.MyFSets]
Load [in ATBR.Model_Relations]
Load [in ATBR.Model_StdRelations]
Load [in ATBR.Model_Languages]
Load [in ATBR.Model_MinPlus]
M
MAUT [in ATBR.DKA_Definitions]MyMapProps [in ATBR.MyFMapProperties]
MySetProps [in ATBR.MyFSetProperties]
MySetProps.Dec [in ATBR.MyFSetProperties]
MySetProps.EqProps [in ATBR.MyFSetProperties]
MySetProps.Facts [in ATBR.MyFSetProperties]
MySetProps.OrdProps [in ATBR.MyFSetProperties]
MySetProps.Props [in ATBR.MyFSetProperties]
N
Nat_as_OT [in ATBR.MyFSets]Nat_as_OTA [in ATBR.MyFSets]
NFA [in ATBR.DKA_Definitions]
NUM [in ATBR.Numbers]
NumUtils [in ATBR.Numbers]
NumUtils.NumMapProps [in ATBR.Numbers]
NumUtils.NumSetProps [in ATBR.Numbers]
NUM.NumMap [in ATBR.Numbers]
NUM.NumOTA [in ATBR.Numbers]
NUM.NumSet [in ATBR.Numbers]
O
OrderedTypeAlt [in ATBR.MyFSets]OrderedType_from_Alt [in ATBR.MyFSets]
P
PairOrderedType [in ATBR.MyFSets]PairOrderedTypeAlt [in ATBR.MyFSets]
PairOrderedType.P [in ATBR.MyFSets]
PosDisjointSets [in ATBR.DisjointSets]
PosDisjointSets.Z [in ATBR.DisjointSets]
Positive [in ATBR.Numbers]
PositiveUtils [in ATBR.Numbers]
Positive.NumMap [in ATBR.Numbers]
Positive.NumMap' [in ATBR.Numbers]
Positive.NumOTA [in ATBR.Numbers]
Positive.NumSet [in ATBR.Numbers]
Positive.NumSet' [in ATBR.Numbers]
Pos_as_OT [in ATBR.MyFSets]
Pos_as_OTA [in ATBR.MyFSets]
R
RegExp [in ATBR.Model_RegExp]RegExp.Clean [in ATBR.Model_RegExp]
RegExp.Load [in ATBR.Model_RegExp]
RegExp.Untype [in ATBR.Model_RegExp]
S
Semiring [in ATBR.Reification]StateLabel [in ATBR.DKA_Definitions]
StateLabelMap [in ATBR.DKA_Definitions]
StateLabelMapProps [in ATBR.DKA_Definitions]
StateLabelMap' [in ATBR.DKA_Definitions]
StateMap [in ATBR.DKA_Definitions]
StateMapProps [in ATBR.DKA_Definitions]
StateSet [in ATBR.DKA_Definitions]
StateSetMap [in ATBR.DKA_StateSetSets]
StateSetMapProps [in ATBR.DKA_StateSetSets]
StateSetMap' [in ATBR.DKA_StateSetSets]
StateSetProps [in ATBR.DKA_Definitions]
StateSetSet [in ATBR.DKA_StateSetSets]
StateSetSetProps [in ATBR.DKA_StateSetSets]
StateSetSet' [in ATBR.DKA_StateSetSets]
U
U [in ATBR.SemiRing]U.VLSet [in ATBR.SemiRing]
U.VLSetProps [in ATBR.SemiRing]
U.VLSet' [in ATBR.SemiRing]
U.VLst [in ATBR.SemiRing]
U.VLstA [in ATBR.SemiRing]
Variable Index
A
add_pair.T [in ATBR.Utils_WF]C
completeness.A [in ATBR.DKA_DFA_Equiv]completeness.HA [in ATBR.DKA_DFA_Equiv]
completeness.Hi [in ATBR.DKA_DFA_Equiv]
completeness.Hj [in ATBR.DKA_DFA_Equiv]
completeness.i [in ATBR.DKA_DFA_Equiv]
completeness.j [in ATBR.DKA_DFA_Equiv]
Concrete'.A [in ATBR.Examples]
Concrete'.R [in ATBR.Examples]
Concrete'.S [in ATBR.Examples]
Concrete.A [in ATBR.Examples]
Concrete.R [in ATBR.Examples]
Concrete.S [in ATBR.Examples]
correction.T [in ATBR.Force]
correctness.A [in ATBR.DKA_DFA_Equiv]
correctness.Correction.Hi' [in ATBR.DKA_DFA_Equiv]
correctness.Correction.Hj' [in ATBR.DKA_DFA_Equiv]
correctness.Correction.i' [in ATBR.DKA_DFA_Equiv]
correctness.Correction.j' [in ATBR.DKA_DFA_Equiv]
correctness.Correction.tarjan [in ATBR.DKA_DFA_Equiv]
correctness.Correction._H [in ATBR.DKA_DFA_Equiv]
correctness.Hbounds [in ATBR.DKA_DFA_Equiv]
CR_algebra.S [in ATBR.ChurchRosser_Points_vs_Algebraic]
CR_algebra.R [in ATBR.ChurchRosser_Points_vs_Algebraic]
CR_algebra.A [in ATBR.ChurchRosser_Points_vs_Algebraic]
CR_points.S [in ATBR.ChurchRosser_Points_vs_Algebraic]
CR_points.R [in ATBR.ChurchRosser_Points_vs_Algebraic]
CR_points.P [in ATBR.ChurchRosser_Points_vs_Algebraic]
D
Defs.A [in ATBR.MxSemiRing]Defs.A [in ATBR.MxFunctors]
Defs.A [in ATBR.MxSemiLattice]
Defs.A [in ATBR.MxKleeneAlgebra]
Defs.A [in ATBR.MxGraph]
Defs.F [in ATBR.MxFunctors]
domain.T [in ATBR.DKA_StateSetSets]
E
equal.A [in ATBR.Graph]equal.B [in ATBR.Graph]
e.A [in ATBR.DKA_DFA_Equiv]
e.d [in ATBR.DKA_DFA_Equiv]
e.f [in ATBR.DKA_DFA_Equiv]
e.final [in ATBR.DKA_DFA_Equiv]
e.m [in ATBR.DKA_DFA_Equiv]
F
Fix_induction.IH [in ATBR.Utils_WF]Fix_induction.P [in ATBR.Utils_WF]
Fix_induction.F [in ATBR.Utils_WF]
Fix_induction.T [in ATBR.Utils_WF]
Fix_induction.Hwf [in ATBR.Utils_WF]
Fix_induction.R [in ATBR.Utils_WF]
Fix_induction.A [in ATBR.Utils_WF]
fold'.A [in ATBR.DKA_Epsilon]
force.f [in ATBR.Force]
force.T [in ATBR.Force]
force2.f [in ATBR.Force]
force2.m [in ATBR.Force]
force2.n [in ATBR.Force]
force2.T [in ATBR.Force]
FSumDef.A [in ATBR.SemiLattice]
FSumDef.B [in ATBR.SemiLattice]
L
leq.A [in ATBR.Graph]leq.B [in ATBR.Graph]
lexico.A [in ATBR.Utils_WF]
lexico.B [in ATBR.Utils_WF]
lexico.HR [in ATBR.Utils_WF]
lexico.HS [in ATBR.Utils_WF]
lexico.R [in ATBR.Utils_WF]
lexico.S [in ATBR.Utils_WF]
M
map_transitive_closure.Hwf [in ATBR.DKA_Epsilon]map_transitive_closure.R [in ATBR.DKA_Epsilon]
map_transitive_closure.f [in ATBR.DKA_Epsilon]
Matrices.A [in ATBR.Examples]
MySetProps.exists_.Hcompat [in ATBR.MyFSetProperties]
MySetProps.exists_.f [in ATBR.MyFSetProperties]
MySetProps.ListViewAbove.i.a [in ATBR.MyFSetProperties]
MySetProps.ListViewAbove.i.f [in ATBR.MyFSetProperties]
MySetProps.ListViewAbove.i.P [in ATBR.MyFSetProperties]
MySetProps.MyFold.A [in ATBR.MyFSetProperties]
MySetProps.MyFold.eqA [in ATBR.MyFSetProperties]
MySetProps.MyFold.equivalence_eqA [in ATBR.MyFSetProperties]
MySetProps.MyFold.f [in ATBR.MyFSetProperties]
MySetProps.MyFold.fold_rec_bis.P [in ATBR.MyFSetProperties]
MySetProps.MyFold.Hcompat [in ATBR.MyFSetProperties]
O
oe.A [in ATBR.StrictKleeneAlgebra]oe.HR [in ATBR.StrictKleeneAlgebra]
oe.R [in ATBR.StrictKleeneAlgebra]
P
PosDisjointSets.protect.link.a [in ATBR.DisjointSets]PosDisjointSets.protect.link.a_diff_b [in ATBR.DisjointSets]
PosDisjointSets.protect.link.b [in ATBR.DisjointSets]
PosDisjointSets.protect.link.repr_b [in ATBR.DisjointSets]
PosDisjointSets.protect.link.repr_a [in ATBR.DisjointSets]
PosDisjointSets.protect.link.t [in ATBR.DisjointSets]
PosDisjointSets.protect.repr.t [in ATBR.DisjointSets]
PosDisjointSets.protect.update.a [in ATBR.DisjointSets]
PosDisjointSets.protect.update.a_repr_b [in ATBR.DisjointSets]
PosDisjointSets.protect.update.a_diff_b [in ATBR.DisjointSets]
PosDisjointSets.protect.update.b [in ATBR.DisjointSets]
PosDisjointSets.protect.update.t [in ATBR.DisjointSets]
powerfix.A [in ATBR.Utils_WF]
powerfix.B [in ATBR.Utils_WF]
powerfix.invariant.HP [in ATBR.Utils_WF]
powerfix.invariant.P [in ATBR.Utils_WF]
powerfix.linear_carac.Hf [in ATBR.Utils_WF]
powerfix.linear_carac.f [in ATBR.Utils_WF]
PreDefs.A [in ATBR.MxKleeneAlgebra]
Props.A [in ATBR.MxSemiLattice]
Props.A [in ATBR.MxGraph]
Props.Blocks.m [in ATBR.MxGraph]
Props.Blocks.n [in ATBR.MxGraph]
Props.Blocks.Proj.a [in ATBR.MxGraph]
Props.Blocks.Proj.b [in ATBR.MxGraph]
Props.Blocks.Proj.c [in ATBR.MxGraph]
Props.Blocks.Proj.d [in ATBR.MxGraph]
Props.Blocks.x [in ATBR.MxGraph]
Props.Blocks.y [in ATBR.MxGraph]
Props.Subs.Def.M [in ATBR.MxGraph]
Props.Subs.m [in ATBR.MxGraph]
Props.Subs.n [in ATBR.MxGraph]
Props.Subs.x [in ATBR.MxGraph]
Props.Subs.y [in ATBR.MxGraph]
Props1.A [in ATBR.MxSemiRing]
Props1.A [in ATBR.Monoid]
Props1.A [in ATBR.SemiLattice]
Props1.A [in ATBR.KleeneAlgebra]
Props1.B [in ATBR.Monoid]
Props1.B [in ATBR.SemiLattice]
Props1.C [in ATBR.Monoid]
Props2.A [in ATBR.MxSemiRing]
Props2.A [in ATBR.KleeneAlgebra]
protect.accept.A [in ATBR.DKA_DFA_Language]
protect.s.I [in ATBR.DKA_DFA_Language]
protect.s.M [in ATBR.DKA_DFA_Language]
protect.s.m [in ATBR.DKA_DFA_Language]
protect.s.n [in ATBR.DKA_DFA_Language]
R
RegExp.Clean.S.cleaning_star [in ATBR.Model_RegExp]RegExp.Clean.S.cleaning_plus [in ATBR.Model_RegExp]
RegExp.Clean.S.cleaning_dot [in ATBR.Model_RegExp]
S
sssm.f [in ATBR.DKA_StateSetSets]sssm.Hf [in ATBR.DKA_StateSetSets]
sssm.t0 [in ATBR.DKA_StateSetSets]
S.A [in ATBR.DKA_Determinisation]
S.equiv [in ATBR.DKA_Merge]
S.equiv_correct [in ATBR.DKA_Merge]
S.HA [in ATBR.DKA_Determinisation]
S.T [in ATBR.DKA_Merge]
T
Tactics.DKA.a [in ATBR.Examples]Tactics.DKA.A [in ATBR.Examples]
Tactics.DKA.b [in ATBR.Examples]
Tactics.DKA.B [in ATBR.Examples]
Tactics.DKA.c [in ATBR.Examples]
Tactics.DKA.d [in ATBR.Examples]
Tactics.DKA.e [in ATBR.Examples]
Tactics.ISR.a [in ATBR.Examples]
Tactics.ISR.A [in ATBR.Examples]
Tactics.ISR.b [in ATBR.Examples]
Tactics.ISR.B [in ATBR.Examples]
Tactics.ISR.c [in ATBR.Examples]
Tactics.ISR.d [in ATBR.Examples]
W
wf_lexico_incl.H [in ATBR.Utils_WF]wf_lexico_incl.R [in ATBR.Utils_WF]
wf_lexico_incl.HRB [in ATBR.Utils_WF]
wf_lexico_incl.HRA [in ATBR.Utils_WF]
wf_lexico_incl.RB [in ATBR.Utils_WF]
wf_lexico_incl.RA [in ATBR.Utils_WF]
wf_lexico_incl.f [in ATBR.Utils_WF]
wf_lexico_incl.B [in ATBR.Utils_WF]
wf_lexico_incl.A [in ATBR.Utils_WF]
wf_lexico_incl.U [in ATBR.Utils_WF]
wf_to.HR [in ATBR.Utils_WF]
wf_to.R [in ATBR.Utils_WF]
wf_to.f [in ATBR.Utils_WF]
wf_to.V [in ATBR.Utils_WF]
wf_to.U [in ATBR.Utils_WF]
wf_of.HR [in ATBR.Utils_WF]
wf_of.R [in ATBR.Utils_WF]
wf_of.f [in ATBR.Utils_WF]
wf_of.V [in ATBR.Utils_WF]
wf_of.U [in ATBR.Utils_WF]
wf_incl.H [in ATBR.Utils_WF]
wf_incl.R [in ATBR.Utils_WF]
wf_incl.HS [in ATBR.Utils_WF]
wf_incl.S [in ATBR.Utils_WF]
wf_incl.A [in ATBR.Utils_WF]
Library Index
A
ATBRATBR_Matrices
B
BoolViewC
ChurchRosserChurchRosser_Points_vs_Algebraic
Classes
Common
Converse
D
DecideKleeneAlgebraDisjointSets
DKA_Definitions
DKA_Merge
DKA_Epsilon
DKA_DFA_Language
DKA_CheckLabels
DKA_Construction
DKA_DFA_Equiv
DKA_StateSetSets
DKA_Determinisation
E
ExamplesF
ForceFunctors
G
GraphK
KleeneAlgebraM
Model_RelationsModel_RegExp
Model_StdRelations
Model_Languages
Model_MinPlus
Monoid
MxFunctors
MxGraph
MxKleeneAlgebra
MxSemiLattice
MxSemiRing
MyFMapProperties
MyFSetProperties
MyFSets
N
NumbersR
ReificationS
SemiLatticeSemiRing
StrictKleeneAlgebra
StrictStarForm
U
Utils_WFLemma Index
A
add_cardinal [in ATBR.DKA_StateSetSets]add_classes_empty [in ATBR.DKA_StateSetSets]
add_valid [in ATBR.DKA_Epsilon]
add_continuation_4r [in ATBR.Monoid]
add_continuation_3r [in ATBR.Monoid]
add_continuation_2r [in ATBR.Monoid]
add_continuation_1r [in ATBR.Monoid]
add_continuation_4l [in ATBR.Monoid]
add_continuation_3l [in ATBR.Monoid]
add_continuation_2l [in ATBR.Monoid]
add_continuation_1l [in ATBR.Monoid]
add_continuationl [in ATBR.Monoid]
add_continuation_4 [in ATBR.Monoid]
add_continuation_3 [in ATBR.Monoid]
add_continuation_2 [in ATBR.Monoid]
add_continuation_1 [in ATBR.Monoid]
add_continuation [in ATBR.Monoid]
add_lists_sameclass [in ATBR.DKA_DFA_Equiv]
add_lists_S [in ATBR.DKA_DFA_Equiv]
add_incr [in ATBR.DKA_DFA_Equiv]
algebraic_rt_closure [in ATBR.DKA_Epsilon]
algebraic_correctness [in ATBR.DKA_Epsilon]
Algebraic.add_zero [in ATBR.DKA_Construction]
Algebraic.add_plus [in ATBR.DKA_Construction]
Algebraic.add_comm [in ATBR.DKA_Construction]
Algebraic.belong_build [in ATBR.DKA_Construction]
Algebraic.belong_add_var [in ATBR.DKA_Construction]
Algebraic.belong_add_one [in ATBR.DKA_Construction]
Algebraic.belong_add [in ATBR.DKA_Construction]
Algebraic.belong_incr' [in ATBR.DKA_Construction]
Algebraic.belong_incr [in ATBR.DKA_Construction]
Algebraic.build_correct [in ATBR.DKA_Construction]
Algebraic.build_add [in ATBR.DKA_Construction]
Algebraic.construction_correct [in ATBR.DKA_Construction]
Algebraic.eval_star [in ATBR.DKA_Construction]
Algebraic.eval_dot [in ATBR.DKA_Construction]
Algebraic.eval_master_theorem [in ATBR.DKA_Construction]
Algebraic.eval_select_block [in ATBR.DKA_Construction]
Algebraic.incr_add [in ATBR.DKA_Construction]
andb_true_iff [in ATBR.BoolView]
andb_false_iff [in ATBR.BoolView]
and_neutral_left [in ATBR.DKA_Merge]
a_star_a_leq_star_a [in ATBR.KleeneAlgebra]
a_star_a_leq_star_a_a [in ATBR.KleeneAlgebra]
a_leq_star_a [in ATBR.KleeneAlgebra]
B
below_max_pi1 [in ATBR.DKA_Merge]below_max_pi0 [in ATBR.DKA_Merge]
below0_empty [in ATBR.DKA_StateSetSets]
bool_prop_iff [in ATBR.BoolView]
bool_dec' [in ATBR.DKA_Epsilon]
bounded [in ATBR.DKA_Epsilon]
bounded [in ATBR.DKA_Determinisation]
bounded [in ATBR.DKA_Construction]
bounded_change_initial [in ATBR.DKA_DFA_Equiv]
bounded_delta_set [in ATBR.DKA_Determinisation]
BubbleSort [in ATBR.ChurchRosser]
build_star_destruct_right [in ATBR.MxKleeneAlgebra]
build_star_destruct_left [in ATBR.MxKleeneAlgebra]
build_star_make_left [in ATBR.MxKleeneAlgebra]
build_store_correct [in ATBR.DKA_Determinisation]
build_store_spec [in ATBR.DKA_Determinisation]
build_max_label [in ATBR.DKA_Construction]
C
cardinal_domain [in ATBR.DKA_StateSetSets]card_pset [in ATBR.DKA_StateSetSets]
classes_union_strict [in ATBR.DKA_StateSetSets]
classes_compat [in ATBR.DKA_StateSetSets]
collect_ssf [in ATBR.DKA_CheckLabels]
collect_ssf_remove [in ATBR.DKA_CheckLabels]
collect_idem [in ATBR.DKA_CheckLabels]
collect_com [in ATBR.DKA_CheckLabels]
collect_incr_1 [in ATBR.DKA_CheckLabels]
collect_incr_2 [in ATBR.DKA_CheckLabels]
collect_max_label [in ATBR.DKA_Construction]
comm_iter_right [in ATBR.KleeneAlgebra]
comm_iter_left [in ATBR.KleeneAlgebra]
compare_compat [in ATBR.DKA_Merge]
compare_sum_xif_zero [in ATBR.SemiLattice]
compat_negsplit [in ATBR.DKA_StateSetSets]
compat_split [in ATBR.DKA_StateSetSets]
complete [in ATBR.DKA_CheckLabels]
completeness [in ATBR.DKA_DFA_Equiv]
complete_compat_left [in ATBR.DKA_DFA_Equiv]
complete_incr_left [in ATBR.DKA_DFA_Equiv]
complete_incr [in ATBR.DKA_DFA_Equiv]
contains_one_false_strict [in ATBR.StrictStarForm]
contains_one_correct [in ATBR.StrictStarForm]
conv_star [in ATBR.Converse]
conv_incr' [in ATBR.Converse]
conv_zero [in ATBR.Converse]
conv_one [in ATBR.Converse]
conv_compat' [in ATBR.Converse]
correct [in ATBR.DKA_Epsilon]
correct [in ATBR.DKA_Merge]
correct [in ATBR.DKA_DFA_Equiv]
correct [in ATBR.DKA_Determinisation]
correct [in ATBR.DKA_Construction]
Correctness.belong_build [in ATBR.DKA_Construction]
Correctness.belong_add_var [in ATBR.DKA_Construction]
Correctness.belong_add_one [in ATBR.DKA_Construction]
Correctness.belong_incr' [in ATBR.DKA_Construction]
Correctness.belong_incr [in ATBR.DKA_Construction]
Correctness.bounded_empty [in ATBR.DKA_Construction]
Correctness.bounded_build [in ATBR.DKA_Construction]
Correctness.bounded_add_var [in ATBR.DKA_Construction]
Correctness.bounded_add_one [in ATBR.DKA_Construction]
Correctness.bounded_incr [in ATBR.DKA_Construction]
Correctness.commute_build_empty [in ATBR.DKA_Construction]
Correctness.commute_empty [in ATBR.DKA_Construction]
Correctness.commute_build [in ATBR.DKA_Construction]
Correctness.commute_incr [in ATBR.DKA_Construction]
Correctness.commute_add_var [in ATBR.DKA_Construction]
Correctness.commute_add_one [in ATBR.DKA_Construction]
Correctness.constructions_equiv [in ATBR.DKA_Construction]
Correctness.deltabrel_add_var [in ATBR.DKA_Construction]
Correctness.delta_add_var [in ATBR.DKA_Construction]
Correctness.epsilonbrel_add_one [in ATBR.DKA_Construction]
Correctness.epsilon_rt_build [in ATBR.DKA_Construction]
Correctness.epsilon_rt_incr [in ATBR.DKA_Construction]
Correctness.epsilon_rt_add_one [in ATBR.DKA_Construction]
Correctness.epsilon_t_add_one [in ATBR.DKA_Construction]
Correctness.epsilon_empty [in ATBR.DKA_Construction]
Correctness.epsilon_incr [in ATBR.DKA_Construction]
Correctness.epsilon_add_var [in ATBR.DKA_Construction]
Correctness.epsilon_add_one [in ATBR.DKA_Construction]
Correctness.labelling_add_var [in ATBR.DKA_Construction]
Correctness.labelling_crop [in ATBR.DKA_Construction]
Correctness.labelling_empty [in ATBR.DKA_Construction]
Correctness.labelling_S [in ATBR.DKA_Construction]
Correctness.leb_S [in ATBR.DKA_Construction]
Correctness.not_epsilon_rt_incr_right [in ATBR.DKA_Construction]
Correctness.not_epsilon_rt_incr_left [in ATBR.DKA_Construction]
Correctness.not_true_eq_false [in ATBR.DKA_Construction]
Correctness.psurj [in ATBR.DKA_Construction]
Correctness.rt_t [in ATBR.DKA_Construction]
Correctness.t_rt [in ATBR.DKA_Construction]
Correctness.wf_empty [in ATBR.DKA_Construction]
Correctness.wf_build [in ATBR.DKA_Construction]
Correctness.wf_add_one [in ATBR.DKA_Construction]
correct_ind_idem [in ATBR.DKA_DFA_Equiv]
counter_exemple_equiv [in ATBR.DKA_DFA_Equiv]
counter_exemple_loop [in ATBR.DKA_DFA_Equiv]
D
decomp_dot_leq_right [in ATBR.MxKleeneAlgebra]decomp_dot_leq_left [in ATBR.MxKleeneAlgebra]
delta_bounded [in ATBR.DKA_Epsilon]
delta'_below [in ATBR.DKA_Determinisation]
diag_empty [in ATBR.DKA_DFA_Equiv]
diag_ok [in ATBR.DKA_DFA_Equiv]
diag_compat_left [in ATBR.DKA_DFA_Equiv]
dk_erase_correct [in ATBR.DecideKleeneAlgebra]
domain_spec [in ATBR.DKA_StateSetSets]
dot_scal_right_blocks [in ATBR.MxSemiRing]
dot_scal_right_dot [in ATBR.MxSemiRing]
dot_scal_right_zero [in ATBR.MxSemiRing]
dot_scal_right_one [in ATBR.MxSemiRing]
dot_scal_right_is_dot [in ATBR.MxSemiRing]
dot_scal_left_blocks [in ATBR.MxSemiRing]
dot_scal_left_dot [in ATBR.MxSemiRing]
dot_scal_left_zero [in ATBR.MxSemiRing]
dot_scal_left_one [in ATBR.MxSemiRing]
dot_scal_left_is_dot [in ATBR.MxSemiRing]
dot_xif [in ATBR.Monoid]
dot_xif_zero [in ATBR.SemiRing]
dot_boolxif_right [in ATBR.DKA_DFA_Language]
dot_xifzero_right [in ATBR.DKA_DFA_Language]
dot_boolxif_left [in ATBR.DKA_DFA_Language]
dot_xifzero_left [in ATBR.DKA_DFA_Language]
dot'_dot [in ATBR.StrictStarForm]
DSUtils.class_of_injective [in ATBR.DisjointSets]
DSUtils.class_of_union_1 [in ATBR.DisjointSets]
DSUtils.class_of_compat' [in ATBR.DisjointSets]
DSUtils.class_of_union_2 [in ATBR.DisjointSets]
DSUtils.class_of_union [in ATBR.DisjointSets]
DSUtils.class_of_empty [in ATBR.DisjointSets]
DSUtils.compat_union_eq [in ATBR.DisjointSets]
DSUtils.eq_union [in ATBR.DisjointSets]
DSUtils.in_class_of_self [in ATBR.DisjointSets]
DSUtils.le_incr [in ATBR.DisjointSets]
DSUtils.le_union [in ATBR.DisjointSets]
DSUtils.sameclass_spec [in ATBR.DisjointSets]
E
eqd_inj [in ATBR.Reification]equal_refl_f2t [in ATBR.Graph]
equal_refl_f1t [in ATBR.Graph]
equal_refl_f2 [in ATBR.Graph]
equal_refl_f1 [in ATBR.Graph]
equal_trans [in ATBR.Graph]
equal_sym [in ATBR.Graph]
equal_refl [in ATBR.Graph]
equal_collect [in ATBR.DKA_CheckLabels]
equiv_filter [in ATBR.DKA_Definitions]
eq_not_negb [in ATBR.BoolView]
eq_nat_bool_refl [in ATBR.BoolView]
eq_nat_bool_false [in ATBR.BoolView]
eq_nat_bool_true [in ATBR.BoolView]
eq_bool_spec [in ATBR.BoolView]
eq_pos_spec [in ATBR.BoolView]
eq_nat_spec [in ATBR.BoolView]
eq_to_Meq [in ATBR.MxGraph]
eval_right [in ATBR.DKA_Merge]
eval_left [in ATBR.DKA_Merge]
eval_change_initial [in ATBR.DKA_DFA_Equiv]
example [in ATBR.Examples]
F
faithful [in ATBR.StrictKleeneAlgebra]final_compat [in ATBR.DKA_Determinisation]
Fix_induction [in ATBR.Utils_WF]
force_rec_rec [in ATBR.Force]
functor_mx_to_scal [in ATBR.MxFunctors]
functor_mx_of_scal [in ATBR.MxFunctors]
functor_mx_sub [in ATBR.MxFunctors]
functor_mx_blocks [in ATBR.MxFunctors]
functor_star_leq [in ATBR.Functors]
functor_sum [in ATBR.Functors]
functor_incr [in ATBR.Functors]
functor_xif [in ATBR.DKA_DFA_Language]
fun_xif [in ATBR.Graph]
H
Hindley_Rosen_confluent_union [in ATBR.ChurchRosser]Hindley_Rosen_union [in ATBR.ChurchRosser]
Hindley_Rosen [in ATBR.ChurchRosser]
I
id_notid [in ATBR.Force]id_id [in ATBR.Force]
id2_id [in ATBR.Force]
incl_wf [in ATBR.Utils_WF]
inf_def [in ATBR.SemiLattice]
inf_leq [in ATBR.DKA_Construction]
invariant_empty [in ATBR.DKA_DFA_Equiv]
invariant_prog [in ATBR.DKA_DFA_Equiv]
invariant_idem [in ATBR.DKA_DFA_Equiv]
invariant_build_store [in ATBR.DKA_Determinisation]
invariant_initial_store [in ATBR.DKA_Determinisation]
in_classes_empty_below [in ATBR.DKA_StateSetSets]
in_classes [in ATBR.DKA_StateSetSets]
in_union [in ATBR.DKA_DFA_Equiv]
in_delta_set [in ATBR.DKA_Determinisation]
iter_compat [in ATBR.Monoid]
iter_swap2 [in ATBR.Monoid]
iter_swap [in ATBR.Monoid]
iter_split [in ATBR.Monoid]
iter_once [in ATBR.Monoid]
iter_equivalence [in ATBR.DKA_Definitions]
K
Kozen94 [in ATBR.DecideKleeneAlgebra]L
language_DFA_eval [in ATBR.DKA_DFA_Language]lang_Union_spec [in ATBR.Model_Languages]
lang_leq [in ATBR.Model_Languages]
lang_sum [in ATBR.DKA_DFA_Language]
left_filter [in ATBR.DKA_Definitions]
leq_lang_Union [in ATBR.Model_Languages]
leq_zero_plus [in ATBR.DKA_DFA_Equiv]
leq_sum [in ATBR.SemiLattice]
leq_destruct_plus [in ATBR.SemiLattice]
leq_mx_lang_Union [in ATBR.DKA_DFA_Language]
lexico_incl_wf [in ATBR.Utils_WF]
lexico_wf [in ATBR.Utils_WF]
le_lt_bool_refl [in ATBR.BoolView]
le_lt_bool_false [in ATBR.BoolView]
le_lt_bool_true [in ATBR.BoolView]
le_nat_spec [in ATBR.BoolView]
le_proxy [in ATBR.DKA_DFA_Equiv]
le_antisym [in ATBR.DKA_Construction]
linearfix_plus [in ATBR.Utils_WF]
ListOrderedTypeAlt.compare_trans [in ATBR.MyFSets]
ListOrderedTypeAlt.compare_sym [in ATBR.MyFSets]
ListOrderedTypeAlt.reflect [in ATBR.MyFSets]
loop_correct [in ATBR.DKA_DFA_Equiv]
lt_n_1 [in ATBR.MxGraph]
M
max_label_X_to_eNFA [in ATBR.DKA_Construction]max_label_collect [in ATBR.DKA_Construction]
max_label_incr [in ATBR.DKA_Construction]
max_label_add_var [in ATBR.DKA_Construction]
max_label_add_one [in ATBR.DKA_Construction]
measure_union_strict [in ATBR.DKA_StateSetSets]
measure_empty [in ATBR.DKA_StateSetSets]
measure_union_idem [in ATBR.DKA_StateSetSets]
measure_compat [in ATBR.DKA_StateSetSets]
mem_set_closure [in ATBR.DKA_Epsilon]
mem_table_finals [in ATBR.DKA_Determinisation]
Meq_to_eq [in ATBR.MxGraph]
merge_bounded [in ATBR.DKA_Merge]
move_star2 [in ATBR.KleeneAlgebra]
move_star [in ATBR.KleeneAlgebra]
mx_point_center [in ATBR.MxSemiRing]
mx_point_one_left [in ATBR.MxSemiRing]
mx_point_dot_zero [in ATBR.MxSemiRing]
mx_point_dot [in ATBR.MxSemiRing]
mx_to_scal_one [in ATBR.MxSemiRing]
mx_to_scal_dot [in ATBR.MxSemiRing]
mx_of_scal_one [in ATBR.MxSemiRing]
mx_of_scal_dot [in ATBR.MxSemiRing]
mx_blocks_one [in ATBR.MxSemiRing]
mx_blocks_dot [in ATBR.MxSemiRing]
mx_dot_neutral_right [in ATBR.MxSemiRing]
mx_dot_neutral_left [in ATBR.MxSemiRing]
mx_dot_assoc [in ATBR.MxSemiRing]
mx_point_blocks11 [in ATBR.MxSemiLattice]
mx_point_blocks10 [in ATBR.MxSemiLattice]
mx_point_blocks01 [in ATBR.MxSemiLattice]
mx_point_blocks00 [in ATBR.MxSemiLattice]
mx_point_scal [in ATBR.MxSemiLattice]
mx_point_plus [in ATBR.MxSemiLattice]
mx_point_zero [in ATBR.MxSemiLattice]
mx_blocks_leq [in ATBR.MxSemiLattice]
mx_blocks_sum [in ATBR.MxSemiLattice]
mx_to_scal_zero [in ATBR.MxSemiLattice]
mx_to_scal_plus [in ATBR.MxSemiLattice]
mx_of_scal_zero [in ATBR.MxSemiLattice]
mx_of_scal_plus [in ATBR.MxSemiLattice]
mx_sub_plus [in ATBR.MxSemiLattice]
mx_blocks_zero [in ATBR.MxSemiLattice]
mx_blocks_plus [in ATBR.MxSemiLattice]
mx_of_scal_star [in ATBR.MxKleeneAlgebra]
mx_to_scal_star [in ATBR.MxKleeneAlgebra]
mx_blocks_star_diagonal [in ATBR.MxKleeneAlgebra]
mx_blocks_star_trigonal [in ATBR.MxKleeneAlgebra]
mx_blocks_star [in ATBR.MxKleeneAlgebra]
mx_blocks_star' [in ATBR.MxKleeneAlgebra]
mx_star_destruct_right [in ATBR.MxKleeneAlgebra]
mx_star_block_destruct_left [in ATBR.MxKleeneAlgebra]
mx_star_destruct_left [in ATBR.MxKleeneAlgebra]
mx_star_block_make_left [in ATBR.MxKleeneAlgebra]
mx_star_make_left [in ATBR.MxKleeneAlgebra]
mx_star_compat [in ATBR.MxKleeneAlgebra]
mx_star_charac [in ATBR.DKA_DFA_Language]
mx_lang_Union_spec [in ATBR.DKA_DFA_Language]
mx_leq_pointwise [in ATBR.DKA_DFA_Language]
mx_transpose_blocks [in ATBR.MxGraph]
mx_to_scal_from_scal [in ATBR.MxGraph]
mx_blocks_degenerate_11 [in ATBR.MxGraph]
mx_blocks_degenerate_00 [in ATBR.MxGraph]
mx_blocks_equal [in ATBR.MxGraph]
mx_block_11 [in ATBR.MxGraph]
mx_block_10 [in ATBR.MxGraph]
mx_block_01 [in ATBR.MxGraph]
mx_block_00 [in ATBR.MxGraph]
mx_decompose_blocks [in ATBR.MxGraph]
mx_force_id [in ATBR.MxGraph]
mx_equal_compat [in ATBR.MxGraph]
mx_equal_at_equal [in ATBR.MxGraph]
mx_equal' [in ATBR.MxGraph]
MyMapProps.find_spec [in ATBR.MyFMapProperties]
MyMapProps.in_add_2 [in ATBR.MyFMapProperties]
MyMapProps.in_add_1 [in ATBR.MyFMapProperties]
MyMapProps.mapsto_in [in ATBR.MyFMapProperties]
MySetProps.elements_fold [in ATBR.MyFSetProperties]
MySetProps.exists_fold [in ATBR.MyFSetProperties]
MySetProps.exists_fold' [in ATBR.MyFSetProperties]
MySetProps.exists_empty [in ATBR.MyFSetProperties]
MySetProps.exists_add [in ATBR.MyFSetProperties]
MySetProps.exists_compat [in ATBR.MyFSetProperties]
MySetProps.fold_compat [in ATBR.MyFSetProperties]
MySetProps.fold_left_id [in ATBR.MyFSetProperties]
MySetProps.fold_rec_bis' [in ATBR.MyFSetProperties]
MySetProps.fold_add_above [in ATBR.MyFSetProperties]
MySetProps.fold_add_below [in ATBR.MyFSetProperties]
MySetProps.fold_empty [in ATBR.MyFSetProperties]
MySetProps.lva_iter [in ATBR.MyFSetProperties]
MySetProps.mem_false_not_in [in ATBR.MyFSetProperties]
MySetProps.mem_spec [in ATBR.MyFSetProperties]
MySetProps.mem_add [in ATBR.MyFSetProperties]
N
Nat_as_OTA.reflect [in ATBR.MyFSets]Nat_as_OTA.compare_trans [in ATBR.MyFSets]
Nat_as_OTA.compare_sym [in ATBR.MyFSets]
negb_false [in ATBR.BoolView]
negb_true [in ATBR.BoolView]
non_strict_not_strict [in ATBR.StrictStarForm]
nth_force_rec' [in ATBR.Force]
nth_force_rec [in ATBR.Force]
NumSetEqual_refl [in ATBR.DKA_CheckLabels]
NumUtils.eqb_eq_nat_bool [in ATBR.Numbers]
NumUtils.eqb_refl [in ATBR.Numbers]
NumUtils.eqb_false [in ATBR.Numbers]
NumUtils.eqb_true [in ATBR.Numbers]
NumUtils.eq_num_dec [in ATBR.Numbers]
NumUtils.eq_nat_spec [in ATBR.Numbers]
NumUtils.leb_refl [in ATBR.Numbers]
NumUtils.leb_false [in ATBR.Numbers]
NumUtils.leb_true [in ATBR.Numbers]
NumUtils.le_antisym [in ATBR.Numbers]
NumUtils.ltb_false [in ATBR.Numbers]
NumUtils.ltb_true [in ATBR.Numbers]
NumUtils.nat_of_num_comm [in ATBR.Numbers]
NumUtils.numseteqb_eq_nat_bool [in ATBR.Numbers]
NumUtils.num_of_nat_comm [in ATBR.Numbers]
NumUtils.num_peano_rec [in ATBR.Numbers]
NumUtils.pi0_inj [in ATBR.Numbers]
NumUtils.pi1_inj [in ATBR.Numbers]
O
oequal_equivalence [in ATBR.StrictKleeneAlgebra]one_leq_star_a [in ATBR.KleeneAlgebra]
orb_true_iff [in ATBR.BoolView]
orb_false_iff [in ATBR.BoolView]
OrderedType_from_Alt.lt_not_eq [in ATBR.MyFSets]
OrderedType_from_Alt.eq_sym [in ATBR.MyFSets]
OrderedType_from_Alt.eq_refl [in ATBR.MyFSets]
P
PairOrderedTypeAlt.compare_trans [in ATBR.MyFSets]PairOrderedTypeAlt.compare_sym [in ATBR.MyFSets]
PairOrderedTypeAlt.reflect [in ATBR.MyFSets]
plus_xif [in ATBR.SemiLattice]
plus_destruct_leq [in ATBR.SemiLattice]
plus_make_right [in ATBR.SemiLattice]
plus_make_left [in ATBR.SemiLattice]
plus_neutral_right [in ATBR.SemiLattice]
plus_minus [in ATBR.MxGraph]
PosDisjointSets.boundage [in ATBR.DisjointSets]
PosDisjointSets.boundage_link [in ATBR.DisjointSets]
PosDisjointSets.class_of_In_repr' [in ATBR.DisjointSets]
PosDisjointSets.class_of_In_repr [in ATBR.DisjointSets]
PosDisjointSets.class_of_In_MapsTo' [in ATBR.DisjointSets]
PosDisjointSets.class_of_In_MapsTo [in ATBR.DisjointSets]
PosDisjointSets.class_of_Equal_repr [in ATBR.DisjointSets]
PosDisjointSets.class_of_Equal_MapsTo [in ATBR.DisjointSets]
PosDisjointSets.DO_inv_In [in ATBR.DisjointSets]
PosDisjointSets.D_link_ex [in ATBR.DisjointSets]
PosDisjointSets.D_update_ex [in ATBR.DisjointSets]
PosDisjointSets.D_update [in ATBR.DisjointSets]
PosDisjointSets.D_inj [in ATBR.DisjointSets]
PosDisjointSets.D_succ [in ATBR.DisjointSets]
PosDisjointSets.D_inv_n [in ATBR.DisjointSets]
PosDisjointSets.D_repr [in ATBR.DisjointSets]
PosDisjointSets.equiv_reflexive_false [in ATBR.DisjointSets]
PosDisjointSets.Equiv_empty [in ATBR.DisjointSets]
PosDisjointSets.FEquiv_D [in ATBR.DisjointSets]
PosDisjointSets.find_spec [in ATBR.DisjointSets]
PosDisjointSets.find_equiv [in ATBR.DisjointSets]
PosDisjointSets.link_main_lemma [in ATBR.DisjointSets]
PosDisjointSets.link_lemma_2 [in ATBR.DisjointSets]
PosDisjointSets.link_lemma_1 [in ATBR.DisjointSets]
PosDisjointSets.MapsTo_sameclass [in ATBR.DisjointSets]
PosDisjointSets.NumMap_Equal_Empty_empty [in ATBR.DisjointSets]
PosDisjointSets.NumMap_fold_compat [in ATBR.DisjointSets]
PosDisjointSets.repr_helper [in ATBR.DisjointSets]
PosDisjointSets.repr_inv_upd [in ATBR.DisjointSets]
PosDisjointSets.repr_x_inv_upd [in ATBR.DisjointSets]
PosDisjointSets.repr_update_fwd [in ATBR.DisjointSets]
PosDisjointSets.repr_D [in ATBR.DisjointSets]
PosDisjointSets.repr_idem [in ATBR.DisjointSets]
PosDisjointSets.repr_inj_idem [in ATBR.DisjointSets]
PosDisjointSets.repr_inv_In [in ATBR.DisjointSets]
PosDisjointSets.repr_inj_right [in ATBR.DisjointSets]
PosDisjointSets.repr_zero_inv [in ATBR.DisjointSets]
PosDisjointSets.sameclass_class_of [in ATBR.DisjointSets]
PosDisjointSets.sameclass_equiv' [in ATBR.DisjointSets]
PosDisjointSets.sameclass_find [in ATBR.DisjointSets]
PosDisjointSets.sameclass_equiv [in ATBR.DisjointSets]
PosDisjointSets.sameclass_union [in ATBR.DisjointSets]
PosDisjointSets.sameclass_empty [in ATBR.DisjointSets]
PosDisjointSets.test_and_unify_eq [in ATBR.DisjointSets]
PosDisjointSets.update_equiv [in ATBR.DisjointSets]
PosDisjointSets.update_In [in ATBR.DisjointSets]
positive_size [in ATBR.DKA_Determinisation]
Positive.compare_spec [in ATBR.Numbers]
Positive.fold_num_sum_S [in ATBR.Numbers]
Positive.fold_num_sum_O [in ATBR.Numbers]
Positive.fold_num_S [in ATBR.Numbers]
Positive.fold_num_O [in ATBR.Numbers]
Positive.id_nat [in ATBR.Numbers]
Positive.id_num [in ATBR.Numbers]
Positive.le_nat_spec [in ATBR.Numbers]
Positive.le_spec [in ATBR.Numbers]
Positive.lt_pi1 [in ATBR.Numbers]
Positive.lt_pi0 [in ATBR.Numbers]
Positive.lt_nat_spec [in ATBR.Numbers]
Positive.lt_spec [in ATBR.Numbers]
Positive.map_eq_spec [in ATBR.Numbers]
Positive.match_pi1 [in ATBR.Numbers]
Positive.match_pi0 [in ATBR.Numbers]
Positive.max_spec [in ATBR.Numbers]
Positive.pcompare_prop [in ATBR.Numbers]
Positive.set_eq_spec [in ATBR.Numbers]
Positive.S_nat_spec [in ATBR.Numbers]
Pos_as_OTA.reflect [in ATBR.MyFSets]
Pos_as_OTA.compare_trans [in ATBR.MyFSets]
Pos_as_OTA.compare_sym [in ATBR.MyFSets]
pos_eq_dec [in ATBR.Reification]
powerfix_invariant' [in ATBR.Utils_WF]
powerfix_linearfix [in ATBR.Utils_WF]
powerfix'_invariant' [in ATBR.Utils_WF]
powerfix'_linearfix [in ATBR.Utils_WF]
power_positive [in ATBR.Utils_WF]
preserve_max_label [in ATBR.DKA_Epsilon]
preserve_max_label [in ATBR.DKA_Determinisation]
R
read_app [in ATBR.DKA_DFA_Language]reflexive_extends [in ATBR.DKA_Determinisation]
RegExp.Clean.clean_star [in ATBR.Model_RegExp]
RegExp.Clean.clean_plus [in ATBR.Model_RegExp]
RegExp.Clean.clean_dot [in ATBR.Model_RegExp]
RegExp.Clean.correct [in ATBR.Model_RegExp]
RegExp.Clean.equal_rewrite_zero_equiv [in ATBR.Model_RegExp]
RegExp.Clean.rewrite_idem [in ATBR.Model_RegExp]
RegExp.equal_refl [in ATBR.Model_RegExp]
RegExp.Is_one [in ATBR.Model_RegExp]
RegExp.Is_zero [in ATBR.Model_RegExp]
RegExp.Untype.and_idem [in ATBR.Model_RegExp]
RegExp.Untype.equal_eval [in ATBR.Model_RegExp]
RegExp.Untype.equal_to_sequal [in ATBR.Model_RegExp]
RegExp.Untype.erase_faithful [in ATBR.Model_RegExp]
RegExp.Untype.eval_sequal [in ATBR.Model_RegExp]
RegExp.Untype.eval_inj [in ATBR.Model_RegExp]
RegExp.Untype.eval_clean [in ATBR.Model_RegExp]
RegExp.Untype.eval_clean_zero [in ATBR.Model_RegExp]
RegExp.Untype.eval_type_inj_right [in ATBR.Model_RegExp]
RegExp.Untype.eval_type_inj_left [in ATBR.Model_RegExp]
RegExp.Untype.eval_var_inv [in ATBR.Model_RegExp]
RegExp.Untype.eval_star_inv [in ATBR.Model_RegExp]
RegExp.Untype.eval_zero_inv [in ATBR.Model_RegExp]
RegExp.Untype.eval_plus_inv [in ATBR.Model_RegExp]
RegExp.Untype.eval_one_inv [in ATBR.Model_RegExp]
RegExp.Untype.eval_dot_inv [in ATBR.Model_RegExp]
RegExp.Untype.eval_erase_feval [in ATBR.Model_RegExp]
RegExp.Untype.normalizer [in ATBR.Model_RegExp]
RegExp.Untype.sequal_clean_zero_equiv [in ATBR.Model_RegExp]
RegExp.Untype.sequal_refl [in ATBR.Model_RegExp]
RegExp.Untype.sequal_equal [in ATBR.Model_RegExp]
rel_leq [in ATBR.Model_Relations]
rel_leq [in ATBR.Model_StdRelations]
rel_to_wf [in ATBR.Utils_WF]
rel_of_wf [in ATBR.Utils_WF]
remove_strict [in ATBR.StrictStarForm]
remove_nf [in ATBR.StrictStarForm]
rem_cardinal_lt [in ATBR.DKA_StateSetSets]
rho_theta [in ATBR.DKA_Determinisation]
right_filter [in ATBR.DKA_Definitions]
rt_closure_bounded [in ATBR.DKA_Epsilon]
rt_closure_star [in ATBR.DKA_Epsilon]
rt_closure_spec [in ATBR.DKA_Epsilon]
rt_closure_prespec [in ATBR.DKA_Epsilon]
rt_closure_aux'_spec [in ATBR.DKA_Epsilon]
rt_closure_aux_spec [in ATBR.DKA_Epsilon]
S
same_labels_ssf [in ATBR.DKA_CheckLabels]same_labels_max_label [in ATBR.DKA_Construction]
semicomm_iter_left [in ATBR.KleeneAlgebra]
semicomm_iter_right [in ATBR.KleeneAlgebra]
SemiConfluence_is_ChurchRosser [in ATBR.ChurchRosser]
SemiConfluence_is_WeakConfluence [in ATBR.ChurchRosser]
semi_invert_right [in ATBR.SemiRing]
semi_invert_left [in ATBR.SemiRing]
simpl_regex_language [in ATBR.DKA_DFA_Language]
simulation [in ATBR.DKA_DFA_Equiv]
square_triangular_blocks [in ATBR.Examples]
square_constant [in ATBR.Examples]
ssf_complete [in ATBR.StrictStarForm]
ssf_correct' [in ATBR.StrictStarForm]
ssf_correct [in ATBR.StrictStarForm]
star_destruct_left_old' [in ATBR.Converse]
star_plus_star [in ATBR.ChurchRosser]
star_plus_one [in ATBR.ChurchRosser]
star_remove [in ATBR.StrictStarForm]
star_plus_star_dot [in ATBR.StrictStarForm]
star_dot_leq_star_plus [in ATBR.StrictStarForm]
star_plus_but_one [in ATBR.StrictStarForm]
star_plus_star [in ATBR.StrictStarForm]
star_plus_star_1 [in ATBR.StrictStarForm]
star_plus_one [in ATBR.StrictStarForm]
star_distr [in ATBR.KleeneAlgebra]
star_idem [in ATBR.KleeneAlgebra]
star_trans [in ATBR.KleeneAlgebra]
star_make_right [in ATBR.KleeneAlgebra]
star_a_a_leq_star_a [in ATBR.KleeneAlgebra]
star_zero [in ATBR.KleeneAlgebra]
star_one [in ATBR.KleeneAlgebra]
star_mon_is_one [in ATBR.KleeneAlgebra]
star_destruct_left_one [in ATBR.KleeneAlgebra]
star_destruct_right_one [in ATBR.KleeneAlgebra]
star_destruct_left_old [in ATBR.KleeneAlgebra]
star_destruct_right_old [in ATBR.KleeneAlgebra]
star_distr [in ATBR.Examples]
star'_star [in ATBR.StrictStarForm]
statesetset_map_cardinal [in ATBR.DKA_StateSetSets]
statesetset_map_in [in ATBR.DKA_StateSetSets]
stateset_fold_rec_bis [in ATBR.DKA_Epsilon]
steps_correct [in ATBR.DKA_Determinisation]
store_size_bound [in ATBR.DKA_Determinisation]
sum_collapse' [in ATBR.DKA_Merge]
sum_distr_left [in ATBR.SemiRing]
sum_distr_right [in ATBR.SemiRing]
sum_fixed_xif_zero [in ATBR.SemiLattice]
sum_incr [in ATBR.SemiLattice]
sum_collapse [in ATBR.SemiLattice]
sum_constant [in ATBR.SemiLattice]
sum_plus [in ATBR.SemiLattice]
sum_leq [in ATBR.SemiLattice]
sum_inversion [in ATBR.SemiLattice]
sum_shift [in ATBR.SemiLattice]
sum_cut_nth [in ATBR.SemiLattice]
sum_cut_fun [in ATBR.SemiLattice]
sum_cut [in ATBR.SemiLattice]
sum_fun_zero [in ATBR.SemiLattice]
sum_zero [in ATBR.SemiLattice]
sum_compat [in ATBR.SemiLattice]
sum_enter_right [in ATBR.SemiLattice]
sum_enter_left [in ATBR.SemiLattice]
sum_empty [in ATBR.SemiLattice]
sup_def [in ATBR.SemiLattice]
switch [in ATBR.SemiLattice]
T
table_finals_complete [in ATBR.DKA_Determinisation]table_finals_correct [in ATBR.DKA_Determinisation]
tarjan_correct [in ATBR.DKA_DFA_Equiv]
tarjan_equiv_true [in ATBR.DKA_DFA_Equiv]
theta_0 [in ATBR.DKA_Determinisation]
theta_delta' [in ATBR.DKA_Determinisation]
theta_below [in ATBR.DKA_Determinisation]
theta_rho [in ATBR.DKA_Determinisation]
translate_correct [in ATBR.DecideKleeneAlgebra]
T_refl [in ATBR.DKA_DFA_Equiv]
T_finaux [in ATBR.DKA_DFA_Equiv]
T_true [in ATBR.DKA_DFA_Equiv]
U
U.and_idem [in ATBR.SemiRing]U.cdot_correct [in ATBR.SemiRing]
U.clean_assoc_correct [in ATBR.SemiRing]
U.clean_assoc_aux [in ATBR.SemiRing]
U.clean_correct [in ATBR.SemiRing]
U.clean0_idem [in ATBR.SemiRing]
U.clean0_correct [in ATBR.SemiRing]
U.clean1_correct [in ATBR.SemiRing]
U.cplus_correct [in ATBR.SemiRing]
U.decide_typed [in ATBR.SemiRing]
U.decide_correct [in ATBR.SemiRing]
U.equal_eval [in ATBR.SemiRing]
U.equal_to_sequal [in ATBR.SemiRing]
U.equal_clean_zero_equiv [in ATBR.SemiRing]
U.equal_refl [in ATBR.SemiRing]
U.erase_faithful [in ATBR.SemiRing]
U.eval_sequal [in ATBR.SemiRing]
U.eval_inj [in ATBR.SemiRing]
U.eval_clean [in ATBR.SemiRing]
U.eval_clean_zero [in ATBR.SemiRing]
U.eval_type_inj_right [in ATBR.SemiRing]
U.eval_type_inj_left [in ATBR.SemiRing]
U.eval_var_inv [in ATBR.SemiRing]
U.eval_zero_inv [in ATBR.SemiRing]
U.eval_plus_inv [in ATBR.SemiRing]
U.eval_one_inv [in ATBR.SemiRing]
U.eval_dot_inv [in ATBR.SemiRing]
U.eval_erase_feval [in ATBR.SemiRing]
U.Hdc [in ATBR.SemiRing]
U.Hpc [in ATBR.SemiRing]
U.Hpt [in ATBR.SemiRing]
U.Is_one [in ATBR.SemiRing]
U.Is_zero [in ATBR.SemiRing]
U.lambda_and_r [in ATBR.SemiRing]
U.lambda_and_l [in ATBR.SemiRing]
U.normalizer [in ATBR.SemiRing]
U.normalize_aux [in ATBR.SemiRing]
U.norm_correct [in ATBR.SemiRing]
U.sequal_clean_zero_equiv [in ATBR.SemiRing]
U.sequal_refl [in ATBR.SemiRing]
U.sequal_equal [in ATBR.SemiRing]
U.VLSet_to_X_compat [in ATBR.SemiRing]
U.VLSet_add [in ATBR.SemiRing]
U.VLst_to_X_compat [in ATBR.SemiRing]
U.VLst_add [in ATBR.SemiRing]
V
valid [in ATBR.DKA_DFA_Equiv]W
WeakConfluence_is_ChurchRosser_plus [in ATBR.ChurchRosser]WeakConfluence_is_ChurchRosser [in ATBR.ChurchRosser]
WeakConfluence_is_ChurchRosser3 [in ATBR.ChurchRosser_Points_vs_Algebraic]
WeakConfluence_is_ChurchRosser2 [in ATBR.ChurchRosser_Points_vs_Algebraic]
WeakConfluence_is_ChurchRosser1 [in ATBR.ChurchRosser_Points_vs_Algebraic]
WeakConfluence_is_ChurchRosser0' [in ATBR.ChurchRosser_Points_vs_Algebraic]
WeakConfluence_is_ChurchRosser0 [in ATBR.ChurchRosser_Points_vs_Algebraic]
well_founded [in ATBR.DKA_Construction]
wf_add_pair [in ATBR.Utils_WF]
wsemicomm_iter_left [in ATBR.KleeneAlgebra]
wsemicomm_iter_right [in ATBR.KleeneAlgebra]
X
xif_negb [in ATBR.Graph]xif_xif_or [in ATBR.Graph]
xif_xif_and [in ATBR.Graph]
xif_idem' [in ATBR.Graph]
xif_idem [in ATBR.Graph]
xif_true [in ATBR.Graph]
xif_false [in ATBR.Graph]
xif_spec [in ATBR.Graph]
xif_bool_incr [in ATBR.DKA_Epsilon]
xif_dot [in ATBR.Monoid]
xif_sum_zero [in ATBR.SemiLattice]
xif_plus [in ATBR.SemiLattice]
X_to_DFA_labels [in ATBR.DecideKleeneAlgebra]
X_to_DFA_bounded [in ATBR.DecideKleeneAlgebra]
X_to_DFA_correct [in ATBR.DecideKleeneAlgebra]
Z
zero_leq [in ATBR.DKA_DFA_Equiv]zero_inf [in ATBR.SemiLattice]
Constructor Index
A
Algebraic.equal_refl [in ATBR.DKA_Construction]Algebraic.mk [in ATBR.DKA_Construction]
B
box [in ATBR.MxGraph]C
cnl_cons [in ATBR.DKA_DFA_Equiv]cnl_nil [in ATBR.DKA_DFA_Equiv]
compare_spec_gt [in ATBR.BoolView]
compare_spec_eq [in ATBR.BoolView]
compare_spec_lt [in ATBR.BoolView]
Concrete.mk [in ATBR.DKA_Construction]
D
DFA.mk [in ATBR.DKA_Definitions]DifferentAtomSets [in ATBR.DecideKleeneAlgebra]
E
eNFA.mk [in ATBR.DKA_Definitions]env [in ATBR.Reification]
K
KA.dot [in ATBR.Reification]KA.one [in ATBR.Reification]
KA.plus [in ATBR.Reification]
KA.star [in ATBR.Reification]
KA.var [in ATBR.Reification]
KA.zero [in ATBR.Reification]
L
lexico_right [in ATBR.Utils_WF]lexico_left [in ATBR.Utils_WF]
M
MAUT.equal_refl [in ATBR.DKA_Definitions]MAUT.mk [in ATBR.DKA_Definitions]
MyMapProps.find_spec_2 [in ATBR.MyFMapProperties]
MyMapProps.find_spec_1 [in ATBR.MyFMapProperties]
MySetProps.lcons [in ATBR.MyFSetProperties]
MySetProps.lconsa [in ATBR.MyFSetProperties]
MySetProps.lnil [in ATBR.MyFSetProperties]
MySetProps.lnila [in ATBR.MyFSetProperties]
N
NFA.mk [in ATBR.DKA_Definitions]non_strict_plus_r [in ATBR.StrictStarForm]
non_strict_plus_l [in ATBR.StrictStarForm]
non_strict_dot [in ATBR.StrictStarForm]
non_strict_star [in ATBR.StrictStarForm]
non_strict_one [in ATBR.StrictStarForm]
NotGeq [in ATBR.DecideKleeneAlgebra]
NotLeq [in ATBR.DecideKleeneAlgebra]
O
oe_none [in ATBR.StrictKleeneAlgebra]oe_some [in ATBR.StrictKleeneAlgebra]
P
pack [in ATBR.Reification]PosDisjointSets.DO [in ATBR.DisjointSets]
PosDisjointSets.DS [in ATBR.DisjointSets]
PosDisjointSets.find_spec_1 [in ATBR.DisjointSets]
PosDisjointSets.rsucc [in ATBR.DisjointSets]
PosDisjointSets.rzero [in ATBR.DisjointSets]
R
RegExp.dot [in ATBR.Model_RegExp]RegExp.dot_compat [in ATBR.Model_RegExp]
RegExp.dot_distr_right [in ATBR.Model_RegExp]
RegExp.dot_distr_left [in ATBR.Model_RegExp]
RegExp.dot_ann_right [in ATBR.Model_RegExp]
RegExp.dot_ann_left [in ATBR.Model_RegExp]
RegExp.dot_neutral_right [in ATBR.Model_RegExp]
RegExp.dot_neutral_left [in ATBR.Model_RegExp]
RegExp.dot_assoc [in ATBR.Model_RegExp]
RegExp.equal_sym [in ATBR.Model_RegExp]
RegExp.equal_trans [in ATBR.Model_RegExp]
RegExp.one [in ATBR.Model_RegExp]
RegExp.plus [in ATBR.Model_RegExp]
RegExp.plus_compat [in ATBR.Model_RegExp]
RegExp.plus_com [in ATBR.Model_RegExp]
RegExp.plus_assoc [in ATBR.Model_RegExp]
RegExp.plus_idem [in ATBR.Model_RegExp]
RegExp.plus_neutral_left [in ATBR.Model_RegExp]
RegExp.refl_var [in ATBR.Model_RegExp]
RegExp.refl_zero [in ATBR.Model_RegExp]
RegExp.refl_one [in ATBR.Model_RegExp]
RegExp.star [in ATBR.Model_RegExp]
RegExp.star_compat [in ATBR.Model_RegExp]
RegExp.star_destruct_right [in ATBR.Model_RegExp]
RegExp.star_destruct_left [in ATBR.Model_RegExp]
RegExp.star_make_right [in ATBR.Model_RegExp]
RegExp.star_make_left [in ATBR.Model_RegExp]
RegExp.Untype.e_var [in ATBR.Model_RegExp]
RegExp.Untype.e_star [in ATBR.Model_RegExp]
RegExp.Untype.e_plus [in ATBR.Model_RegExp]
RegExp.Untype.e_dot [in ATBR.Model_RegExp]
RegExp.Untype.e_zero [in ATBR.Model_RegExp]
RegExp.Untype.e_one [in ATBR.Model_RegExp]
RegExp.Untype.sequal_sym [in ATBR.Model_RegExp]
RegExp.Untype.sequal_trans [in ATBR.Model_RegExp]
RegExp.Untype.sequal_star_compat [in ATBR.Model_RegExp]
RegExp.Untype.sequal_plus_compat [in ATBR.Model_RegExp]
RegExp.Untype.sequal_dot_compat [in ATBR.Model_RegExp]
RegExp.Untype.sequal_star_destruct_right [in ATBR.Model_RegExp]
RegExp.Untype.sequal_star_destruct_left [in ATBR.Model_RegExp]
RegExp.Untype.sequal_star_make_right [in ATBR.Model_RegExp]
RegExp.Untype.sequal_star_make_left [in ATBR.Model_RegExp]
RegExp.Untype.sequal_plus_com [in ATBR.Model_RegExp]
RegExp.Untype.sequal_plus_idem [in ATBR.Model_RegExp]
RegExp.Untype.sequal_plus_assoc [in ATBR.Model_RegExp]
RegExp.Untype.sequal_dot_distr_right [in ATBR.Model_RegExp]
RegExp.Untype.sequal_dot_distr_left [in ATBR.Model_RegExp]
RegExp.Untype.sequal_dot_neutral_right [in ATBR.Model_RegExp]
RegExp.Untype.sequal_dot_neutral_left [in ATBR.Model_RegExp]
RegExp.Untype.sequal_dot_assoc [in ATBR.Model_RegExp]
RegExp.Untype.sequal_refl_var [in ATBR.Model_RegExp]
RegExp.Untype.sequal_refl_zero [in ATBR.Model_RegExp]
RegExp.Untype.sequal_refl_one [in ATBR.Model_RegExp]
RegExp.var [in ATBR.Model_RegExp]
RegExp.zero [in ATBR.Model_RegExp]
rel_to_intro [in ATBR.Utils_WF]
S
Semiring.dot [in ATBR.Reification]Semiring.one [in ATBR.Reification]
Semiring.plus [in ATBR.Reification]
Semiring.var [in ATBR.Reification]
Semiring.zero [in ATBR.Reification]
ssf_dot [in ATBR.StrictStarForm]
ssf_plus [in ATBR.StrictStarForm]
ssf_star [in ATBR.StrictStarForm]
ssf_var [in ATBR.StrictStarForm]
ssf_one [in ATBR.StrictStarForm]
ssf_zero [in ATBR.StrictStarForm]
strict_dot_r [in ATBR.StrictStarForm]
strict_dot_l [in ATBR.StrictStarForm]
strict_plus [in ATBR.StrictStarForm]
strict_var [in ATBR.StrictStarForm]
strict_zero [in ATBR.StrictStarForm]
U
U.dot [in ATBR.SemiRing]U.dot_compat [in ATBR.SemiRing]
U.dot_distr_right [in ATBR.SemiRing]
U.dot_distr_left [in ATBR.SemiRing]
U.dot_ann_right [in ATBR.SemiRing]
U.dot_ann_left [in ATBR.SemiRing]
U.dot_neutral_right [in ATBR.SemiRing]
U.dot_neutral_left [in ATBR.SemiRing]
U.dot_assoc [in ATBR.SemiRing]
U.equal_sym [in ATBR.SemiRing]
U.equal_trans [in ATBR.SemiRing]
U.e_var [in ATBR.SemiRing]
U.e_plus [in ATBR.SemiRing]
U.e_dot [in ATBR.SemiRing]
U.e_zero [in ATBR.SemiRing]
U.e_one [in ATBR.SemiRing]
U.one [in ATBR.SemiRing]
U.plus [in ATBR.SemiRing]
U.plus_compat [in ATBR.SemiRing]
U.plus_com [in ATBR.SemiRing]
U.plus_assoc [in ATBR.SemiRing]
U.plus_idem [in ATBR.SemiRing]
U.plus_neutral_left [in ATBR.SemiRing]
U.refl_var [in ATBR.SemiRing]
U.refl_zero [in ATBR.SemiRing]
U.refl_one [in ATBR.SemiRing]
U.sequal_sym [in ATBR.SemiRing]
U.sequal_trans [in ATBR.SemiRing]
U.sequal_plus_compat [in ATBR.SemiRing]
U.sequal_dot_compat [in ATBR.SemiRing]
U.sequal_plus_com [in ATBR.SemiRing]
U.sequal_plus_idem [in ATBR.SemiRing]
U.sequal_plus_assoc [in ATBR.SemiRing]
U.sequal_dot_distr_right [in ATBR.SemiRing]
U.sequal_dot_distr_left [in ATBR.SemiRing]
U.sequal_dot_neutral_right [in ATBR.SemiRing]
U.sequal_dot_neutral_left [in ATBR.SemiRing]
U.sequal_dot_assoc [in ATBR.SemiRing]
U.sequal_refl_var [in ATBR.SemiRing]
U.sequal_refl_zero [in ATBR.SemiRing]
U.sequal_refl_one [in ATBR.SemiRing]
U.var [in ATBR.SemiRing]
U.zero [in ATBR.SemiRing]
Axiom Index
D
DISJOINTSETS.class_of [in ATBR.DisjointSets]DISJOINTSETS.empty [in ATBR.DisjointSets]
DISJOINTSETS.equiv [in ATBR.DisjointSets]
DISJOINTSETS.IsWF [in ATBR.DisjointSets]
DISJOINTSETS.sameclass [in ATBR.DisjointSets]
DISJOINTSETS.sameclass_class_of [in ATBR.DisjointSets]
DISJOINTSETS.sameclass_union [in ATBR.DisjointSets]
DISJOINTSETS.sameclass_empty [in ATBR.DisjointSets]
DISJOINTSETS.sameclass_equiv [in ATBR.DisjointSets]
DISJOINTSETS.T [in ATBR.DisjointSets]
DISJOINTSETS.test_and_unify_eq [in ATBR.DisjointSets]
DISJOINTSETS.test_and_unify [in ATBR.DisjointSets]
DISJOINTSETS.union [in ATBR.DisjointSets]
N
NUM.code [in ATBR.Numbers]NUM.compare [in ATBR.Numbers]
NUM.compare_spec [in ATBR.Numbers]
NUM.eqb [in ATBR.Numbers]
NUM.eq_spec [in ATBR.Numbers]
NUM.fold_num_sum_S [in ATBR.Numbers]
NUM.fold_num_sum_O [in ATBR.Numbers]
NUM.fold_num_S [in ATBR.Numbers]
NUM.fold_num_O [in ATBR.Numbers]
NUM.fold_num_sum [in ATBR.Numbers]
NUM.fold_num [in ATBR.Numbers]
NUM.id_nat [in ATBR.Numbers]
NUM.id_num [in ATBR.Numbers]
NUM.le [in ATBR.Numbers]
NUM.leb [in ATBR.Numbers]
NUM.le_nat_spec [in ATBR.Numbers]
NUM.le_spec [in ATBR.Numbers]
NUM.lt [in ATBR.Numbers]
NUM.ltb [in ATBR.Numbers]
NUM.lt_pi1 [in ATBR.Numbers]
NUM.lt_pi0 [in ATBR.Numbers]
NUM.lt_nat_spec [in ATBR.Numbers]
NUM.lt_spec [in ATBR.Numbers]
NUM.map_eq_spec [in ATBR.Numbers]
NUM.match_pi1 [in ATBR.Numbers]
NUM.match_pi0 [in ATBR.Numbers]
NUM.max [in ATBR.Numbers]
NUM.max_spec [in ATBR.Numbers]
NUM.nat_of_num [in ATBR.Numbers]
NUM.num [in ATBR.Numbers]
NUM.num_of_nat [in ATBR.Numbers]
NUM.pimatch [in ATBR.Numbers]
NUM.pi0 [in ATBR.Numbers]
NUM.pi1 [in ATBR.Numbers]
NUM.S [in ATBR.Numbers]
NUM.set_eq_spec [in ATBR.Numbers]
NUM.S_nat_spec [in ATBR.Numbers]
O
OrderedTypeAlt.compare [in ATBR.MyFSets]OrderedTypeAlt.compare_trans [in ATBR.MyFSets]
OrderedTypeAlt.compare_sym [in ATBR.MyFSets]
OrderedTypeAlt.reflect [in ATBR.MyFSets]
OrderedTypeAlt.t [in ATBR.MyFSets]
Inductive Index
A
Algebraic.equal [in ATBR.DKA_Construction]C
combine_no_length [in ATBR.DKA_DFA_Equiv]compare_spec [in ATBR.BoolView]
CounterExample [in ATBR.DecideKleeneAlgebra]
K
KA.X [in ATBR.Reification]L
lexico [in ATBR.Utils_WF]M
MAUT.equal [in ATBR.DKA_Definitions]MX [in ATBR.MxGraph]
MyMapProps.find_spec_ind [in ATBR.MyFMapProperties]
MySetProps.lva [in ATBR.MyFSetProperties]
MySetProps.lvb [in ATBR.MyFSetProperties]
N
non_strict [in ATBR.StrictStarForm]O
oequal [in ATBR.StrictKleeneAlgebra]P
PosDisjointSets.D [in ATBR.DisjointSets]PosDisjointSets.find_spec_decl [in ATBR.DisjointSets]
PosDisjointSets.repr [in ATBR.DisjointSets]
R
RegExp.equal [in ATBR.Model_RegExp]RegExp.regex [in ATBR.Model_RegExp]
RegExp.Untype.eval [in ATBR.Model_RegExp]
RegExp.Untype.sequal [in ATBR.Model_RegExp]
rel_to [in ATBR.Utils_WF]
S
Semiring.X [in ATBR.Reification]strict [in ATBR.StrictStarForm]
strict_star_form [in ATBR.StrictStarForm]
U
U.equal [in ATBR.SemiRing]U.eval [in ATBR.SemiRing]
U.sequal [in ATBR.SemiRing]
U.X [in ATBR.SemiRing]
Projection Index
A
Algebraic.delta [in ATBR.DKA_Construction]Algebraic.size [in ATBR.DKA_Construction]
C
cfi_measure [in ATBR.DKA_DFA_Equiv]cfi_le [in ATBR.DKA_DFA_Equiv]
cfi_prog [in ATBR.DKA_DFA_Equiv]
CISR_SL [in ATBR.Classes]
ci_sameclass [in ATBR.DKA_DFA_Equiv]
ci_measure [in ATBR.DKA_DFA_Equiv]
ci_le [in ATBR.DKA_DFA_Equiv]
ci_prog [in ATBR.DKA_DFA_Equiv]
CKA_CISR [in ATBR.Classes]
Concrete.deltamap [in ATBR.DKA_Construction]
Concrete.epsilonmap [in ATBR.DKA_Construction]
Concrete.max_label [in ATBR.DKA_Construction]
Concrete.size [in ATBR.DKA_Construction]
conv [in ATBR.Classes]
conv_plus [in ATBR.Classes]
conv_dot [in ATBR.Classes]
conv_invol [in ATBR.Classes]
conv_compat [in ATBR.Classes]
Correctness.bounded_eps [in ATBR.DKA_Construction]
Correctness.bounded_delta [in ATBR.DKA_Construction]
D
DFA.bounded_finaux [in ATBR.DKA_Definitions]DFA.bounded_initial [in ATBR.DKA_Definitions]
DFA.bounded_delta [in ATBR.DKA_Definitions]
DFA.delta [in ATBR.DKA_Definitions]
DFA.finaux [in ATBR.DKA_Definitions]
DFA.initial [in ATBR.DKA_Definitions]
DFA.max_label [in ATBR.DKA_Definitions]
DFA.size [in ATBR.DKA_Definitions]
DISJOINTSETS.wf [in ATBR.DisjointSets]
dot [in ATBR.Classes]
dot [in ATBR.StrictKleeneAlgebra]
dot_distr_left_c [in ATBR.Classes]
dot_ann_left_c [in ATBR.Classes]
dot_neutral_left_c [in ATBR.Classes]
dot_assoc_c [in ATBR.Classes]
dot_compat_c [in ATBR.Classes]
dot_distr_right [in ATBR.Classes]
dot_distr_left [in ATBR.Classes]
dot_ann_right [in ATBR.Classes]
dot_ann_left [in ATBR.Classes]
dot_neutral_right [in ATBR.Classes]
dot_neutral_left [in ATBR.Classes]
dot_assoc [in ATBR.Classes]
dot_compat [in ATBR.Classes]
dot_distr_right [in ATBR.StrictKleeneAlgebra]
dot_distr_left [in ATBR.StrictKleeneAlgebra]
dot_neutral_right [in ATBR.StrictKleeneAlgebra]
dot_neutral_left [in ATBR.StrictKleeneAlgebra]
dot_assoc [in ATBR.StrictKleeneAlgebra]
dot_compat [in ATBR.StrictKleeneAlgebra]
E
eNFA.bounded_final [in ATBR.DKA_Definitions]eNFA.bounded_initial [in ATBR.DKA_Definitions]
eNFA.bounded_eps [in ATBR.DKA_Definitions]
eNFA.bounded_delta [in ATBR.DKA_Definitions]
eNFA.deltamap [in ATBR.DKA_Definitions]
eNFA.epsilon [in ATBR.DKA_Definitions]
eNFA.final [in ATBR.DKA_Definitions]
eNFA.initial [in ATBR.DKA_Definitions]
eNFA.max_label [in ATBR.DKA_Definitions]
eNFA.size [in ATBR.DKA_Definitions]
equal [in ATBR.Classes]
equal_ [in ATBR.Classes]
e_next [in ATBR.DKA_Determinisation]
e_table [in ATBR.DKA_Determinisation]
e_invariant [in ATBR.DKA_Determinisation]
F
fT [in ATBR.Functors]functor_star [in ATBR.Functors]
functor_zero [in ATBR.Functors]
functor_plus [in ATBR.Functors]
functor_one [in ATBR.Functors]
functor_dot [in ATBR.Functors]
functor_compat [in ATBR.Functors]
fX [in ATBR.Functors]
I
ISR_SemiLattice [in ATBR.Classes]ISR_Monoid [in ATBR.Classes]
i_final [in ATBR.DKA_DFA_Equiv]
i_wf_tarjan [in ATBR.DKA_DFA_Equiv]
i_delta [in ATBR.DKA_Determinisation]
i_table_size [in ATBR.DKA_Determinisation]
i_table_surj [in ATBR.DKA_Determinisation]
i_table_inj [in ATBR.DKA_Determinisation]
i_table_wf [in ATBR.DKA_Determinisation]
K
KA_ISR [in ATBR.Classes]kleene_semiring [in ATBR.Functors]
M
MAUT.delta [in ATBR.DKA_Definitions]MAUT.final [in ATBR.DKA_Definitions]
MAUT.initial [in ATBR.DKA_Definitions]
MAUT.size [in ATBR.DKA_Definitions]
monoid_graph_functor [in ATBR.Functors]
N
NFA.bounded_finaux [in ATBR.DKA_Definitions]NFA.bounded_initiaux [in ATBR.DKA_Definitions]
NFA.bounded_delta [in ATBR.DKA_Definitions]
NFA.delta [in ATBR.DKA_Definitions]
NFA.finaux [in ATBR.DKA_Definitions]
NFA.initiaux [in ATBR.DKA_Definitions]
NFA.max_label [in ATBR.DKA_Definitions]
NFA.size [in ATBR.DKA_Definitions]
O
one [in ATBR.Classes]one [in ATBR.StrictKleeneAlgebra]
P
plus [in ATBR.Classes]plus [in ATBR.StrictKleeneAlgebra]
plus_com [in ATBR.Classes]
plus_assoc [in ATBR.Classes]
plus_idem [in ATBR.Classes]
plus_neutral_left [in ATBR.Classes]
plus_compat [in ATBR.Classes]
plus_com [in ATBR.StrictKleeneAlgebra]
plus_assoc [in ATBR.StrictKleeneAlgebra]
plus_idem [in ATBR.StrictKleeneAlgebra]
plus_compat [in ATBR.StrictKleeneAlgebra]
PosDisjointSets.p [in ATBR.DisjointSets]
PosDisjointSets.rank [in ATBR.DisjointSets]
PosDisjointSets.size [in ATBR.DisjointSets]
PosDisjointSets.wf [in ATBR.DisjointSets]
S
semilattice_graph_functor [in ATBR.Functors]semiring_semilattice_functor [in ATBR.Functors]
semiring_monoid_functor [in ATBR.Functors]
src_p [in ATBR.Reification]
star [in ATBR.Classes]
star [in ATBR.StrictKleeneAlgebra]
star_destruct_left_c [in ATBR.Classes]
star_make_left_c [in ATBR.Classes]
star_destruct_right [in ATBR.Classes]
star_destruct_left [in ATBR.Classes]
star_make_left [in ATBR.Classes]
star_destruct_right [in ATBR.StrictKleeneAlgebra]
star_destruct_left [in ATBR.StrictKleeneAlgebra]
star_make_left [in ATBR.StrictKleeneAlgebra]
T
T [in ATBR.Classes]tgt_p [in ATBR.Reification]
typ [in ATBR.Reification]
type_view [in ATBR.BoolView]
type_view_ty [in ATBR.BoolView]
U
unpack [in ATBR.Reification]V
val [in ATBR.Reification]X
X [in ATBR.Classes]Z
zero [in ATBR.Classes]Section Index
A
add_pair [in ATBR.Utils_WF]Alg [in ATBR.DKA_Definitions]
algebraic_lemmas [in ATBR.DKA_Epsilon]
Algebraic.protect [in ATBR.DKA_Construction]
C
comb [in ATBR.DKA_DFA_Equiv]completeness [in ATBR.DKA_DFA_Equiv]
Concrete [in ATBR.Examples]
Concrete' [in ATBR.Examples]
correction [in ATBR.Force]
correctness [in ATBR.DKA_DFA_Equiv]
correctness.Correction [in ATBR.DKA_DFA_Equiv]
Correctness.protect [in ATBR.DKA_Construction]
CR_algebra [in ATBR.ChurchRosser_Points_vs_Algebraic]
CR_points [in ATBR.ChurchRosser_Points_vs_Algebraic]
D
Def [in ATBR.Model_Relations]Def [in ATBR.Model_StdRelations]
Def [in ATBR.Model_Languages]
Defs [in ATBR.MxSemiRing]
Defs [in ATBR.MxFunctors]
Defs [in ATBR.Functors]
Defs [in ATBR.MxSemiLattice]
Defs [in ATBR.MxKleeneAlgebra]
Defs [in ATBR.MxGraph]
Defs.SLfunct [in ATBR.Functors]
domain [in ATBR.DKA_StateSetSets]
Dual.Protect [in ATBR.Classes]
Dual.Protect [in ATBR.KleeneAlgebra]
E
e [in ATBR.DKA_DFA_Equiv]equal [in ATBR.Graph]
F
F [in ATBR.StrictKleeneAlgebra]Fix_induction [in ATBR.Utils_WF]
fold' [in ATBR.DKA_Epsilon]
force [in ATBR.Force]
force2 [in ATBR.Force]
FSumDef [in ATBR.SemiLattice]
I
ISR [in ATBR.Converse]K
KA [in ATBR.Converse]KA.S [in ATBR.Reification]
L
leq [in ATBR.Graph]lexico [in ATBR.Utils_WF]
M
map_transitive_closure [in ATBR.DKA_Epsilon]Matrices [in ATBR.Examples]
monoid_rewrite_leq [in ATBR.Monoid]
monoid_rewrite_equal [in ATBR.Monoid]
MySetProps.elements [in ATBR.MyFSetProperties]
MySetProps.exists_ [in ATBR.MyFSetProperties]
MySetProps.ListViewAbove [in ATBR.MyFSetProperties]
MySetProps.ListViewAbove.i [in ATBR.MyFSetProperties]
MySetProps.ListViewBelow [in ATBR.MyFSetProperties]
MySetProps.MyFold [in ATBR.MyFSetProperties]
MySetProps.MyFold.fold_rec_bis [in ATBR.MyFSetProperties]
O
oe [in ATBR.StrictKleeneAlgebra]Ops [in ATBR.Classes]
P
PosDisjointSets.protect [in ATBR.DisjointSets]PosDisjointSets.protect.Equiv [in ATBR.DisjointSets]
PosDisjointSets.protect.find_aux [in ATBR.DisjointSets]
PosDisjointSets.protect.link [in ATBR.DisjointSets]
PosDisjointSets.protect.repr [in ATBR.DisjointSets]
PosDisjointSets.protect.update [in ATBR.DisjointSets]
PosDisjointSets.protect.WF [in ATBR.DisjointSets]
powerfix [in ATBR.Utils_WF]
powerfix.invariant [in ATBR.Utils_WF]
powerfix.linear_carac [in ATBR.Utils_WF]
PreDefs [in ATBR.MxKleeneAlgebra]
Props [in ATBR.SemiRing]
Props [in ATBR.MxSemiLattice]
Props [in ATBR.MxGraph]
Props.Blocks [in ATBR.MxGraph]
Props.Blocks.Proj [in ATBR.MxGraph]
Props.Subs [in ATBR.MxGraph]
Props.Subs.Def [in ATBR.MxGraph]
Props0 [in ATBR.KleeneAlgebra]
Props1 [in ATBR.MxSemiRing]
Props1 [in ATBR.Monoid]
Props1 [in ATBR.ChurchRosser]
Props1 [in ATBR.SemiLattice]
Props1 [in ATBR.KleeneAlgebra]
Props2 [in ATBR.MxSemiRing]
Props2 [in ATBR.ChurchRosser]
Props2 [in ATBR.KleeneAlgebra]
Props3 [in ATBR.KleeneAlgebra]
Props4 [in ATBR.KleeneAlgebra]
protect [in ATBR.DKA_StateSetSets]
protect [in ATBR.Model_MinPlus]
protect [in ATBR.DKA_CheckLabels]
protect [in ATBR.DKA_DFA_Language]
protect.accept [in ATBR.DKA_DFA_Language]
protect.s [in ATBR.DKA_DFA_Language]
R
RegExp.Clean.S [in ATBR.Model_RegExp]RegExp.Def [in ATBR.Model_RegExp]
RegExp.Untype.protect [in ATBR.Model_RegExp]
RegExp.Untype.protect.erase [in ATBR.Model_RegExp]
RegExp.Untype.protect.faithful [in ATBR.Model_RegExp]
S
S [in ATBR.DKA_Merge]S [in ATBR.Reification]
S [in ATBR.DKA_Determinisation]
Semiring.S [in ATBR.Reification]
Setting [in ATBR.Examples]
sssm [in ATBR.DKA_StateSetSets]
Structures [in ATBR.Classes]
T
Tactics [in ATBR.Examples]Tactics.DKA [in ATBR.Examples]
Tactics.ISR [in ATBR.Examples]
U
U.correctness [in ATBR.SemiRing]U.erase [in ATBR.SemiRing]
U.faithful [in ATBR.SemiRing]
W
wf_lexico_incl [in ATBR.Utils_WF]wf_to [in ATBR.Utils_WF]
wf_of [in ATBR.Utils_WF]
wf_incl [in ATBR.Utils_WF]
Instance Index
A
Algebraic.add_compat [in ATBR.DKA_Construction]Algebraic.add_compat' [in ATBR.DKA_Construction]
Algebraic.build_compat [in ATBR.DKA_Construction]
Algebraic.equal_equiv [in ATBR.DKA_Construction]
Algebraic.eval_compat [in ATBR.DKA_Construction]
Algebraic.incr_compat [in ATBR.DKA_Construction]
Algebraic.to_MAUT_compat [in ATBR.DKA_Construction]
B
box_compat [in ATBR.MxGraph]C
CISR_ISR [in ATBR.Converse]CKA_KA [in ATBR.Converse]
collect_compat [in ATBR.DKA_CheckLabels]
complete_WF [in ATBR.DKA_DFA_Equiv]
conv_incr [in ATBR.Converse]
D
diag_compat [in ATBR.DKA_DFA_Equiv]DISJOINTSETS.empty_WF [in ATBR.DisjointSets]
DISJOINTSETS.equiv_WF [in ATBR.DisjointSets]
DISJOINTSETS.sameclass_Equivalence [in ATBR.DisjointSets]
DISJOINTSETS.test_and_unify_WF [in ATBR.DisjointSets]
DISJOINTSETS.union_WF [in ATBR.DisjointSets]
dot_scal_left_compat [in ATBR.MxSemiRing]
dot_scal_right_compat [in ATBR.MxSemiRing]
dot_incr_temp [in ATBR.Monoid]
dot_incr [in ATBR.SemiRing]
DSUtils.class_of_compat [in ATBR.DisjointSets]
DSUtils.eq_Equivalence [in ATBR.DisjointSets]
DSUtils.le_PreOrder [in ATBR.DisjointSets]
DSUtils.sameclass_compat' [in ATBR.DisjointSets]
DSUtils.sameclass_compat [in ATBR.DisjointSets]
Dual.Converse_Op [in ATBR.Classes]
Dual.Graph [in ATBR.Classes]
Dual.IdemSemiRing [in ATBR.Classes]
Dual.KleeneAlgebra [in ATBR.KleeneAlgebra]
Dual.Monoid [in ATBR.Classes]
Dual.Monoid_Ops [in ATBR.Classes]
Dual.SemiLattice [in ATBR.Classes]
Dual.SemiLattice_Ops [in ATBR.Classes]
Dual.Star_Op [in ATBR.Classes]
E
equal_geq [in ATBR.Graph]equal_leq [in ATBR.Graph]
eq_bool_view [in ATBR.BoolView]
eq_pos_view [in ATBR.BoolView]
eq_nat_view [in ATBR.BoolView]
L
lang_ConverseKleeneAlgebra [in ATBR.Model_Languages]lang_ConverseSemiRing [in ATBR.Model_Languages]
lang_SemiLattice [in ATBR.Model_Languages]
lang_Converse_Op [in ATBR.Model_Languages]
lang_Star_Op [in ATBR.Model_Languages]
lang_Monoid_Ops [in ATBR.Model_Languages]
lang_SemiLattice_Ops [in ATBR.Model_Languages]
lang_Graph [in ATBR.Model_Languages]
leq_trans [in ATBR.Graph]
leq_refl [in ATBR.Graph]
le_nat_view [in ATBR.BoolView]
linearfix_compat [in ATBR.Utils_WF]
M
MAUT.equal_equiv [in ATBR.DKA_Definitions]MAUT.eval_compat [in ATBR.DKA_Definitions]
mp_ConverseKleeneAlgebra [in ATBR.Model_MinPlus]
mp_ConverseSemiRing [in ATBR.Model_MinPlus]
mp_SemiLattice [in ATBR.Model_MinPlus]
mp_Converse_Op [in ATBR.Model_MinPlus]
mp_Star_Op [in ATBR.Model_MinPlus]
mp_Monoid_Ops [in ATBR.Model_MinPlus]
mp_SemiLattice_Ops [in ATBR.Model_MinPlus]
mp_Graph [in ATBR.Model_MinPlus]
mxgraph_functor [in ATBR.MxFunctors]
mxkleene_functor [in ATBR.MxFunctors]
mxsemilattice_functor [in ATBR.MxFunctors]
mxsemiring_functor [in ATBR.MxFunctors]
mx_SemiRing [in ATBR.MxSemiRing]
mx_Monoid [in ATBR.MxSemiRing]
mx_Monoid_Ops [in ATBR.MxSemiRing]
mx_point_compat [in ATBR.MxSemiLattice]
mx_blocks_incr [in ATBR.MxSemiLattice]
mx_SemiLattice [in ATBR.MxSemiLattice]
mx_SemiLattice_Ops [in ATBR.MxSemiLattice]
mx_KleeneAlgebra [in ATBR.MxKleeneAlgebra]
mx_Star_Op [in ATBR.MxKleeneAlgebra]
mx_transpose_compat [in ATBR.MxGraph]
mx_to_scal_compat [in ATBR.MxGraph]
mx_of_scal_compat [in ATBR.MxGraph]
mx_blocks_compat [in ATBR.MxGraph]
mx_sub11_compat [in ATBR.MxGraph]
mx_sub10_compat [in ATBR.MxGraph]
mx_sub01_compat [in ATBR.MxGraph]
mx_sub00_compat [in ATBR.MxGraph]
mx_force_compat [in ATBR.MxGraph]
mx_Graph [in ATBR.MxGraph]
MyMapProps.find_view [in ATBR.MyFMapProperties]
MySetProps.mem_type_view [in ATBR.MyFSetProperties]
N
NumUtils.eqb_view [in ATBR.Numbers]NumUtils.fold_num_compat [in ATBR.Numbers]
NumUtils.fold_num_compat' [in ATBR.Numbers]
NumUtils.leb_view [in ATBR.Numbers]
NumUtils.le_preorder [in ATBR.Numbers]
NumUtils.ltb_view [in ATBR.Numbers]
NumUtils.lt_transitive [in ATBR.Numbers]
O
oGraph [in ATBR.StrictKleeneAlgebra]oIdemSemiRing [in ATBR.StrictKleeneAlgebra]
oKleeneAlgebra [in ATBR.StrictKleeneAlgebra]
oMonoid [in ATBR.StrictKleeneAlgebra]
oMonoid_Ops [in ATBR.StrictKleeneAlgebra]
oSemiLattice [in ATBR.StrictKleeneAlgebra]
oSemiLattice_Ops [in ATBR.StrictKleeneAlgebra]
oStar_Op [in ATBR.StrictKleeneAlgebra]
P
plus_incr [in ATBR.SemiLattice]PosDisjointSets.empty_WF [in ATBR.DisjointSets]
PosDisjointSets.Equiv_compat [in ATBR.DisjointSets]
PosDisjointSets.equiv_WF [in ATBR.DisjointSets]
PosDisjointSets.FEquiv_eq [in ATBR.DisjointSets]
PosDisjointSets.find_WF [in ATBR.DisjointSets]
PosDisjointSets.link_WF [in ATBR.DisjointSets]
PosDisjointSets.repr_compat [in ATBR.DisjointSets]
PosDisjointSets.sameclass_Equivalence [in ATBR.DisjointSets]
PosDisjointSets.test_and_unify_WF [in ATBR.DisjointSets]
PosDisjointSets.union_WF [in ATBR.DisjointSets]
powerfix_compat [in ATBR.Utils_WF]
powerfix'_compat [in ATBR.Utils_WF]
preorder_prog [in ATBR.DKA_DFA_Equiv]
R
RegExp.re_KleeneAlgebra [in ATBR.Model_RegExp]RegExp.re_SemiRing [in ATBR.Model_RegExp]
RegExp.re_Monoid [in ATBR.Model_RegExp]
RegExp.re_SemiLattice [in ATBR.Model_RegExp]
RegExp.re_Star_Op [in ATBR.Model_RegExp]
RegExp.re_Monoid_Ops [in ATBR.Model_RegExp]
RegExp.re_SemiLattice_Ops [in ATBR.Model_RegExp]
RegExp.re_Graph [in ATBR.Model_RegExp]
regex_language_kleene_functor [in ATBR.DKA_DFA_Language]
regex_language_graph_functor [in ATBR.DKA_DFA_Language]
rel_ConverseKleeneAlgebra [in ATBR.Model_Relations]
rel_ConverseSemiRing [in ATBR.Model_Relations]
rel_SemiLattice [in ATBR.Model_Relations]
rel_Converse_Op [in ATBR.Model_Relations]
rel_Star_Op [in ATBR.Model_Relations]
rel_Monoid_Ops [in ATBR.Model_Relations]
rel_SemiLattice_Ops [in ATBR.Model_Relations]
rel_Graph [in ATBR.Model_Relations]
rel_ConverseKleeneAlgebra [in ATBR.Model_StdRelations]
rel_ConverseSemiRing [in ATBR.Model_StdRelations]
rel_SemiLattice [in ATBR.Model_StdRelations]
rel_Converse_Op [in ATBR.Model_StdRelations]
rel_Star_Op [in ATBR.Model_StdRelations]
rel_Monoid_Ops [in ATBR.Model_StdRelations]
rel_SemiLattice_Ops [in ATBR.Model_StdRelations]
rel_Graph [in ATBR.Model_StdRelations]
S
star_compat [in ATBR.KleeneAlgebra]star_incr [in ATBR.KleeneAlgebra]
step_compat [in ATBR.DKA_Determinisation]
sum_incr' [in ATBR.SemiLattice]
sum_compat' [in ATBR.SemiLattice]
T
tarjan_wf [in ATBR.DKA_DFA_Equiv]transitive_extends [in ATBR.DKA_Determinisation]
U
U.dot_compat_free [in ATBR.SemiRing]U.equivalence_equal [in ATBR.SemiRing]
U.plus_compat_free [in ATBR.SemiRing]
X
xif_compat [in ATBR.Graph]Abbreviation Index
A
Algebraic.belong [in ATBR.DKA_Construction]B
below [in ATBR.DKA_Definitions]C
clean [in ATBR.DecideKleeneAlgebra]clean [in ATBR.DKA_CheckLabels]
Correctness.belong [in ATBR.DKA_Construction]
Correctness.epsilon_rt [in ATBR.DKA_Construction]
Correctness.epsilon_t [in ATBR.DKA_Construction]
D
d [in ATBR.DKA_Determinisation]delta [in ATBR.DKA_DFA_Equiv]
delta [in ATBR.DKA_Determinisation]
Delta [in ATBR.DKA_Determinisation]
DFA.belong [in ATBR.DKA_Definitions]
DFA.setbelong [in ATBR.DKA_Definitions]
E
eNFA.belong [in ATBR.DKA_Definitions]eNFA.setbelong [in ATBR.DKA_Definitions]
eq_label_bool [in ATBR.DKA_Definitions]
eq_state_bool [in ATBR.DKA_Definitions]
F
final [in ATBR.DKA_DFA_Equiv]finaux [in ATBR.DKA_Determinisation]
fold_labels [in ATBR.DKA_Definitions]
fold_states [in ATBR.DKA_Definitions]
Fun [in ATBR.Utils_WF]
I
infty [in ATBR.Model_MinPlus]initiaux [in ATBR.DKA_Determinisation]
K
kt [in ATBR.DKA_DFA_Equiv]L
label [in ATBR.DKA_Definitions]language [in ATBR.DKA_DFA_Language]
LMX [in ATBR.DKA_DFA_Language]
Load.LMX [in ATBR.Model_Languages]
Load.LX [in ATBR.Model_Languages]
lt_state_bool [in ATBR.DKA_Definitions]
LX [in ATBR.Model_Languages]
M
max_label [in ATBR.DKA_Determinisation]measure [in ATBR.DKA_DFA_Equiv]
MG1 [in ATBR.MxFunctors]
MG2 [in ATBR.MxFunctors]
ml [in ATBR.DKA_DFA_Equiv]
MX [in ATBR.MxSemiRing]
MX [in ATBR.MxSemiRing]
MX [in ATBR.MxSemiRing]
MX [in ATBR.MxSemiLattice]
MX [in ATBR.MxSemiLattice]
MX [in ATBR.MxKleeneAlgebra]
MX [in ATBR.MxKleeneAlgebra]
MX [in ATBR.MxGraph]
MX [in ATBR.Examples]
mx_equal [in ATBR.MxSemiRing]
mx_equal [in ATBR.MxSemiRing]
mx_one_ [in ATBR.MxSemiRing]
mx_dot_ [in ATBR.MxSemiRing]
mx_equal [in ATBR.MxSemiRing]
mx_leq [in ATBR.MxSemiLattice]
mx_equal [in ATBR.MxSemiLattice]
mx_leq_ [in ATBR.MxSemiLattice]
mx_equal [in ATBR.MxSemiLattice]
mx_leq [in ATBR.MxKleeneAlgebra]
mx_equal [in ATBR.MxKleeneAlgebra]
mx_leq [in ATBR.MxKleeneAlgebra]
mx_equal [in ATBR.MxKleeneAlgebra]
mx_equal [in ATBR.MxGraph]
mx_equal_ [in ATBR.MxGraph]
MX_ [in ATBR.MxGraph]
N
nat_of_state [in ATBR.DKA_Definitions]NFA.belong [in ATBR.DKA_Definitions]
NFA.setbelong [in ATBR.DKA_Definitions]
ns [in ATBR.DKA_Epsilon]
P
PosDisjointSets.S [in ATBR.DisjointSets]R
RegExp.Load.KMX [in ATBR.Model_RegExp]RegExp.Load.regex [in ATBR.Model_RegExp]
RegExp.Load.tt [in ATBR.Model_RegExp]
RegExp.Load.var [in ATBR.Model_RegExp]
RegExp.Untype.clean [in ATBR.Model_RegExp]
RegExp.Untype.feval [in ATBR.Model_RegExp]
rho [in ATBR.DKA_Determinisation]
S
size [in ATBR.DKA_DFA_Equiv]size [in ATBR.DKA_Determinisation]
size' [in ATBR.DKA_Determinisation]
SMX [in ATBR.MxKleeneAlgebra]
SMX [in ATBR.MxKleeneAlgebra]
sn [in ATBR.DKA_Epsilon]
state [in ATBR.DKA_Definitions]
statelabelmap [in ATBR.DKA_Definitions]
statemap [in ATBR.DKA_Definitions]
stateset [in ATBR.DKA_Definitions]
statesetmap [in ATBR.DKA_StateSetSets]
statesetset [in ATBR.DKA_StateSetSets]
state_of_nat [in ATBR.DKA_Definitions]
Store [in ATBR.DKA_Determinisation]
T
table [in ATBR.DKA_Determinisation]Table [in ATBR.DKA_Determinisation]
U
U.feval [in ATBR.SemiRing]U.S [in ATBR.SemiRing]
W
Word [in ATBR.DKA_DFA_Language]X
X [in ATBR.MxKleeneAlgebra]X [in ATBR.MxKleeneAlgebra]
X [in ATBR.MxGraph]
X [in ATBR.Examples]
Definition Index
A
add_classes [in ATBR.DKA_StateSetSets]add_pair [in ATBR.Utils_WF]
add_lists [in ATBR.DKA_DFA_Equiv]
Algebraic.add [in ATBR.DKA_Construction]
Algebraic.add_var [in ATBR.DKA_Construction]
Algebraic.add_one [in ATBR.DKA_Construction]
Algebraic.build [in ATBR.DKA_Construction]
Algebraic.empty [in ATBR.DKA_Construction]
Algebraic.eval [in ATBR.DKA_Construction]
Algebraic.incr [in ATBR.DKA_Construction]
Algebraic.to_MAUT [in ATBR.DKA_Construction]
Algebraic.X_to_MAUT [in ATBR.DKA_Construction]
apply [in ATBR.Common]
approx [in ATBR.DKA_Epsilon]
B
bounded_word [in ATBR.DKA_DFA_Language]build_combine [in ATBR.DKA_DFA_Equiv]
build_store [in ATBR.DKA_Determinisation]
C
ChurchRosser [in ATBR.ChurchRosser_Points_vs_Algebraic]classes [in ATBR.DKA_StateSetSets]
collect [in ATBR.DKA_CheckLabels]
collect_compat' [in ATBR.DKA_CheckLabels]
comb [in ATBR.DKA_DFA_Equiv]
comb_aux [in ATBR.DKA_DFA_Equiv]
comp [in ATBR.Model_StdRelations]
comp [in ATBR.Common]
compare_DFAs [in ATBR.DKA_Merge]
complete [in ATBR.DKA_DFA_Equiv]
Concrete.add_var [in ATBR.DKA_Construction]
Concrete.add_one [in ATBR.DKA_Construction]
Concrete.augment [in ATBR.DKA_Construction]
Concrete.augment_var [in ATBR.DKA_Construction]
Concrete.build [in ATBR.DKA_Construction]
Concrete.empty [in ATBR.DKA_Construction]
Concrete.incr [in ATBR.DKA_Construction]
Concrete.X_to_eNFA [in ATBR.DKA_Construction]
constant [in ATBR.Examples]
contains_one [in ATBR.StrictStarForm]
Correctness.delta [in ATBR.DKA_Construction]
Correctness.deltabrel [in ATBR.DKA_Construction]
Correctness.deltafun [in ATBR.DKA_Construction]
Correctness.epsilon [in ATBR.DKA_Construction]
Correctness.epsilonbrel [in ATBR.DKA_Construction]
Correctness.epsilonfun [in ATBR.DKA_Construction]
Correctness.preNFA_to_preMAUT [in ATBR.DKA_Construction]
Correctness.wf [in ATBR.DKA_Construction]
D
decide_kleene [in ATBR.DecideKleeneAlgebra]defined [in ATBR.DKA_Determinisation]
delta_set [in ATBR.DKA_Determinisation]
delta' [in ATBR.DKA_Determinisation]
DFA_language [in ATBR.DKA_DFA_Language]
DFA.change_initial [in ATBR.DKA_Definitions]
DFA.eval [in ATBR.DKA_Definitions]
DFA.to_MAUT [in ATBR.DKA_Definitions]
diag [in ATBR.DKA_DFA_Equiv]
domain [in ATBR.DKA_StateSetSets]
dot_scal_left [in ATBR.MxSemiRing]
dot_scal_right [in ATBR.MxSemiRing]
dot' [in ATBR.StrictStarForm]
DSUtils.eq [in ATBR.DisjointSets]
DSUtils.le [in ATBR.DisjointSets]
E
empty [in ATBR.Model_StdRelations]eNFA_to_NFA [in ATBR.DKA_Epsilon]
eNFA.delta [in ATBR.DKA_Definitions]
eNFA.eval [in ATBR.DKA_Definitions]
eNFA.to_MAUT [in ATBR.DKA_Definitions]
eNFA.well_founded [in ATBR.DKA_Definitions]
eqd [in ATBR.Reification]
equiv [in ATBR.DKA_DFA_Equiv]
equivalent [in ATBR.DKA_DFA_Equiv]
eq_bool_bool [in ATBR.BoolView]
eq_pos_bool [in ATBR.BoolView]
eq_nat_bool [in ATBR.BoolView]
F
faithful [in ATBR.Functors]force_rec [in ATBR.Force]
full [in ATBR.Functors]
G
get [in ATBR.MxGraph]guard [in ATBR.Utils_WF]
I
id [in ATBR.Force]id2 [in ATBR.Force]
initial_store [in ATBR.DKA_Determinisation]
inj [in ATBR.StrictKleeneAlgebra]
iter [in ATBR.Monoid]
K
KA.eval [in ATBR.Reification]L
labelling [in ATBR.DKA_Definitions]lang [in ATBR.Model_Languages]
lang_KleeneAlgebra [in ATBR.Model_Languages]
lang_IdemSemiRing [in ATBR.Model_Languages]
lang_star [in ATBR.Model_Languages]
lang_iter [in ATBR.Model_Languages]
lang_top [in ATBR.Model_Languages]
lang_empty [in ATBR.Model_Languages]
lang_id [in ATBR.Model_Languages]
lang_conv [in ATBR.Model_Languages]
lang_comp [in ATBR.Model_Languages]
lang_inter [in ATBR.Model_Languages]
lang_Union [in ATBR.Model_Languages]
lang_union [in ATBR.Model_Languages]
lang_equal [in ATBR.Model_Languages]
leq_antisym [in ATBR.Graph]
le_lt_bool [in ATBR.BoolView]
linearfix [in ATBR.Utils_WF]
ListOrderedTypeAlt.compare [in ATBR.MyFSets]
ListOrderedTypeAlt.t [in ATBR.MyFSets]
loop [in ATBR.DKA_DFA_Equiv]
M
MAUT.eval [in ATBR.DKA_Definitions]measure [in ATBR.DKA_StateSetSets]
merge_DFAs [in ATBR.DKA_Merge]
mp_KleeneAlgebra [in ATBR.Model_MinPlus]
mp_IdemSemiRing [in ATBR.Model_MinPlus]
mp_star [in ATBR.Model_MinPlus]
mp_empty [in ATBR.Model_MinPlus]
mp_id [in ATBR.Model_MinPlus]
mp_conv [in ATBR.Model_MinPlus]
mp_comp [in ATBR.Model_MinPlus]
mp_union [in ATBR.Model_MinPlus]
mxF [in ATBR.MxFunctors]
mx_bool [in ATBR.MxSemiRing]
mx_one [in ATBR.MxSemiRing]
mx_dot [in ATBR.MxSemiRing]
mx_point [in ATBR.MxSemiLattice]
mx_zero [in ATBR.MxSemiLattice]
mx_plus [in ATBR.MxSemiLattice]
mx_star_block [in ATBR.MxKleeneAlgebra]
mx_lang_Union [in ATBR.DKA_DFA_Language]
mx_transpose [in ATBR.MxGraph]
mx_to_scal [in ATBR.MxGraph]
mx_of_scal [in ATBR.MxGraph]
mx_blocks [in ATBR.MxGraph]
mx_sub11 [in ATBR.MxGraph]
mx_sub10 [in ATBR.MxGraph]
mx_sub01 [in ATBR.MxGraph]
mx_sub00 [in ATBR.MxGraph]
mx_sub [in ATBR.MxGraph]
mx_noprint [in ATBR.MxGraph]
mx_print [in ATBR.MxGraph]
mx_force [in ATBR.MxGraph]
mx_equal_at [in ATBR.MxGraph]
mx_equal [in ATBR.MxGraph]
MySetProps.lVA [in ATBR.MyFSetProperties]
MySetProps.lVB [in ATBR.MyFSetProperties]
MySetProps.lvb_iter [in ATBR.MyFSetProperties]
MySetProps.set_induction_above [in ATBR.MyFSetProperties]
MySetProps.set_induction_below [in ATBR.MyFSetProperties]
N
Nat_as_OTA.compare [in ATBR.MyFSets]Nat_as_OTA.t [in ATBR.MyFSets]
NFA_to_DFA [in ATBR.DKA_Determinisation]
NFA.change_initial [in ATBR.DKA_Definitions]
NFA.eval [in ATBR.DKA_Definitions]
NFA.to_MAUT [in ATBR.DKA_Definitions]
nth [in ATBR.Force]
numota_of_nat [in ATBR.DKA_Definitions]
O
onat [in ATBR.Model_MinPlus]optionset_to_set [in ATBR.DKA_Definitions]
OrderedType_from_Alt.eq_dec [in ATBR.MyFSets]
OrderedType_from_Alt.compare [in ATBR.MyFSets]
OrderedType_from_Alt.lt_trans [in ATBR.MyFSets]
OrderedType_from_Alt.eq_trans [in ATBR.MyFSets]
OrderedType_from_Alt.lt [in ATBR.MyFSets]
OrderedType_from_Alt.eq [in ATBR.MyFSets]
OrderedType_from_Alt.t [in ATBR.MyFSets]
P
PairOrderedTypeAlt.compare [in ATBR.MyFSets]PairOrderedTypeAlt.t [in ATBR.MyFSets]
plus_but_one [in ATBR.StrictStarForm]
PosDisjointSets.bounded [in ATBR.DisjointSets]
PosDisjointSets.class_of [in ATBR.DisjointSets]
PosDisjointSets.class_of' [in ATBR.DisjointSets]
PosDisjointSets.empty [in ATBR.DisjointSets]
PosDisjointSets.Equiv [in ATBR.DisjointSets]
PosDisjointSets.equiv [in ATBR.DisjointSets]
PosDisjointSets.eq_num [in ATBR.DisjointSets]
PosDisjointSets.FEquiv [in ATBR.DisjointSets]
PosDisjointSets.find [in ATBR.DisjointSets]
PosDisjointSets.find_aux [in ATBR.DisjointSets]
PosDisjointSets.get_rank [in ATBR.DisjointSets]
PosDisjointSets.IsWF [in ATBR.DisjointSets]
PosDisjointSets.link [in ATBR.DisjointSets]
PosDisjointSets.num [in ATBR.DisjointSets]
PosDisjointSets.sameclass [in ATBR.DisjointSets]
PosDisjointSets.T [in ATBR.DisjointSets]
PosDisjointSets.test_and_unify [in ATBR.DisjointSets]
PosDisjointSets.union [in ATBR.DisjointSets]
Positive.code [in ATBR.Numbers]
Positive.compare [in ATBR.Numbers]
Positive.enc [in ATBR.Numbers]
Positive.eqb [in ATBR.Numbers]
Positive.eq_spec [in ATBR.Numbers]
Positive.fold_num_sum [in ATBR.Numbers]
Positive.fold_num [in ATBR.Numbers]
Positive.le [in ATBR.Numbers]
Positive.leb [in ATBR.Numbers]
Positive.lt [in ATBR.Numbers]
Positive.ltb [in ATBR.Numbers]
Positive.max [in ATBR.Numbers]
Positive.nat_of_num [in ATBR.Numbers]
Positive.num [in ATBR.Numbers]
Positive.num_of_nat [in ATBR.Numbers]
Positive.PeanoView_sum_iter [in ATBR.Numbers]
Positive.pimatch [in ATBR.Numbers]
Positive.pi0 [in ATBR.Numbers]
Positive.pi1 [in ATBR.Numbers]
Positive.S [in ATBR.Numbers]
Positive.triangle [in ATBR.Numbers]
Pos_as_OTA.compare [in ATBR.MyFSets]
Pos_as_OTA.t [in ATBR.MyFSets]
power [in ATBR.Utils_WF]
powerfix [in ATBR.Utils_WF]
powerfix' [in ATBR.Utils_WF]
print [in ATBR.Force]
print2 [in ATBR.Force]
prog [in ATBR.DKA_DFA_Equiv]
prop_star_destruct_right [in ATBR.MxKleeneAlgebra]
prop_star_destruct_left [in ATBR.MxKleeneAlgebra]
prop_star_make_left [in ATBR.MxKleeneAlgebra]
R
read [in ATBR.DKA_DFA_Language]RegExp.Clean.rewrite [in ATBR.Model_RegExp]
RegExp.is_one [in ATBR.Model_RegExp]
RegExp.is_zero [in ATBR.Model_RegExp]
RegExp.Untype.erase [in ATBR.Model_RegExp]
regex_language_f [in ATBR.DKA_DFA_Language]
regex_language [in ATBR.DKA_DFA_Language]
rel [in ATBR.Model_Relations]
rel_KleeneAlgebra [in ATBR.Model_Relations]
rel_IdemSemiRing [in ATBR.Model_Relations]
rel_star [in ATBR.Model_Relations]
rel_iter [in ATBR.Model_Relations]
rel_top [in ATBR.Model_Relations]
rel_empty [in ATBR.Model_Relations]
rel_id [in ATBR.Model_Relations]
rel_conv [in ATBR.Model_Relations]
rel_comp [in ATBR.Model_Relations]
rel_inter [in ATBR.Model_Relations]
rel_union [in ATBR.Model_Relations]
rel_equal [in ATBR.Model_Relations]
rel_KleeneAlgebra [in ATBR.Model_StdRelations]
rel_IdemSemiRing [in ATBR.Model_StdRelations]
rel_of [in ATBR.Utils_WF]
remove [in ATBR.StrictStarForm]
rt_closure [in ATBR.DKA_Epsilon]
rt_closure_aux' [in ATBR.DKA_Epsilon]
rt_closure_aux [in ATBR.DKA_Epsilon]
S
same_labels [in ATBR.DKA_CheckLabels]select [in ATBR.DKA_DFA_Equiv]
Semiring.eval [in ATBR.Reification]
setbelow [in ATBR.DKA_Definitions]
set_closure [in ATBR.DKA_Epsilon]
sigma [in ATBR.Reification]
sigma_empty [in ATBR.Reification]
sigma_add [in ATBR.Reification]
sigma_get [in ATBR.Reification]
src [in ATBR.Reification]
ssf [in ATBR.StrictStarForm]
star_rec [in ATBR.MxKleeneAlgebra]
star_build [in ATBR.MxKleeneAlgebra]
star' [in ATBR.StrictStarForm]
statelabelmap_set_to_fun [in ATBR.DKA_Epsilon]
statelabelmap_set_to_fun [in ATBR.DKA_Construction]
statemapelt_of_nat [in ATBR.DKA_Definitions]
statemap_set_to_fun [in ATBR.DKA_Definitions]
statesetelt_of_nat [in ATBR.DKA_Definitions]
statesetset_map [in ATBR.DKA_StateSetSets]
stateset_fold [in ATBR.DKA_Epsilon]
step [in ATBR.DKA_Epsilon]
step [in ATBR.DKA_Determinisation]
steps [in ATBR.DKA_Epsilon]
steps [in ATBR.DKA_Determinisation]
step' [in ATBR.DKA_Determinisation]
sum [in ATBR.SemiLattice]
T
table_finals [in ATBR.DKA_Determinisation]terminates [in ATBR.DKA_Epsilon]
tgt [in ATBR.Reification]
theta [in ATBR.DKA_Determinisation]
translate_ce [in ATBR.DecideKleeneAlgebra]
U
Unnamed_thm [in ATBR.ChurchRosser_Points_vs_Algebraic]Unnamed_thm15 [in ATBR.Examples]
Unnamed_thm14 [in ATBR.Examples]
Unnamed_thm13 [in ATBR.Examples]
Unnamed_thm12 [in ATBR.Examples]
Unnamed_thm11 [in ATBR.Examples]
Unnamed_thm10 [in ATBR.Examples]
Unnamed_thm9 [in ATBR.Examples]
Unnamed_thm8 [in ATBR.Examples]
Unnamed_thm7 [in ATBR.Examples]
Unnamed_thm6 [in ATBR.Examples]
Unnamed_thm5 [in ATBR.Examples]
Unnamed_thm4 [in ATBR.Examples]
Unnamed_thm3 [in ATBR.Examples]
Unnamed_thm2 [in ATBR.Examples]
Unnamed_thm1 [in ATBR.Examples]
Unnamed_thm0 [in ATBR.Examples]
Unnamed_thm [in ATBR.Examples]
U.cdot [in ATBR.SemiRing]
U.clean_prod [in ATBR.SemiRing]
U.clean_sum [in ATBR.SemiRing]
U.clean0 [in ATBR.SemiRing]
U.clean1 [in ATBR.SemiRing]
U.cplus [in ATBR.SemiRing]
U.decide [in ATBR.SemiRing]
U.erase [in ATBR.SemiRing]
U.fdot [in ATBR.SemiRing]
U.fplus [in ATBR.SemiRing]
U.is_one [in ATBR.SemiRing]
U.is_zero [in ATBR.SemiRing]
U.norm [in ATBR.SemiRing]
U.norm_aux' [in ATBR.SemiRing]
U.norm_aux [in ATBR.SemiRing]
U.size [in ATBR.SemiRing]
U.VLSet_to_X [in ATBR.SemiRing]
U.VLst_to_X [in ATBR.SemiRing]
U.X_to_VLSet [in ATBR.SemiRing]
V
valid [in ATBR.DKA_Epsilon]W
WeakConfluence [in ATBR.ChurchRosser_Points_vs_Algebraic]word [in ATBR.DecideKleeneAlgebra]
X
xif [in ATBR.Graph]X_to_DFA [in ATBR.DecideKleeneAlgebra]
X_to_eNFA [in ATBR.DKA_Construction]
Record Index
A
Algebraic.pre_MAUT [in ATBR.DKA_Construction]C
Concrete.pre_eNFA [in ATBR.DKA_Construction]ConverseIdemSemiRing [in ATBR.Classes]
ConverseKleeneAlgebra [in ATBR.Classes]
Converse_Op [in ATBR.Classes]
Correctness.bounded [in ATBR.DKA_Construction]
correct_fold_ind [in ATBR.DKA_DFA_Equiv]
correct_ind [in ATBR.DKA_DFA_Equiv]
D
DFA.bounded [in ATBR.DKA_Definitions]DFA.t [in ATBR.DKA_Definitions]
DISJOINTSETS.WF [in ATBR.DisjointSets]
E
eNFA.bounded [in ATBR.DKA_Definitions]eNFA.t [in ATBR.DKA_Definitions]
Env [in ATBR.Reification]
extends [in ATBR.DKA_Determinisation]
F
functor [in ATBR.Functors]G
Graph [in ATBR.Classes]graph_functor [in ATBR.Functors]
I
IdemSemiRing [in ATBR.Classes]invariant [in ATBR.DKA_DFA_Equiv]
invariant [in ATBR.DKA_Determinisation]
K
KleeneAlgebra [in ATBR.Classes]kleene_functor [in ATBR.Functors]
M
MAUT.t [in ATBR.DKA_Definitions]Monoid [in ATBR.Classes]
Monoid_Ops [in ATBR.Classes]
monoid_functor [in ATBR.Functors]
N
NFA.bounded [in ATBR.DKA_Definitions]NFA.t [in ATBR.DKA_Definitions]
P
Pack [in ATBR.Reification]PosDisjointSets.UF [in ATBR.DisjointSets]
PosDisjointSets.WF [in ATBR.DisjointSets]
S
SemiLattice [in ATBR.Classes]SemiLattice_Ops [in ATBR.Classes]
semilattice_functor [in ATBR.Functors]
semiring_functor [in ATBR.Functors]
SKA_Ops [in ATBR.StrictKleeneAlgebra]
Star_Op [in ATBR.Classes]
StrictKleeneAlgebra [in ATBR.StrictKleeneAlgebra]
T
Type_View [in ATBR.BoolView]| 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 | (2135 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 | (53 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 | (81 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 | (181 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 | (45 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 | (676 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 | (160 entries) |
| Axiom 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 | (55 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 | (28 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 | (139 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 | (110 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) |
| 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 | (97 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 | (315 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 | (40 entries) |