| 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 | (741 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 | (1 entry) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (71 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 | (21 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 | (444 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 | (51 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 | (8 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 | (25 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 | (15 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 | (105 entries) |
Global Index
A
add [definition, in CanonBDDs.canonicite.Finite_sets]addQinterSx_addQxinterS [lemma, in CanonBDDs.canonicite.Finite_sets]
addQxinterS_QinterS [lemma, in CanonBDDs.canonicite.Finite_sets]
addQxinterS_addQinterSx [lemma, in CanonBDDs.canonicite.Finite_sets]
add_soustr_xy [lemma, in CanonBDDs.canonicite.Finite_sets]
add_soustr_1 [lemma, in CanonBDDs.canonicite.Finite_sets]
add_soustr_2 [lemma, in CanonBDDs.canonicite.Finite_sets]
add_inh [lemma, in CanonBDDs.canonicite.Finite_sets]
add_in_or_eq [lemma, in CanonBDDs.canonicite.Finite_sets]
all_ [definition, in CanonBDDs.canonicite.Finite_sets]
ANd [constructor, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
AND [definition, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
And_BDT [lemma, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
And_BDT_overloaded [lemma, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
And_BDT_b1_One [lemma, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
And_BDT_b1_Zero [lemma, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
And_BDT_One_b2 [lemma, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
And_BDT_Zero_b2 [lemma, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Anil_lowest [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
anti_symetry [definition, in CanonBDDs.canonicite.Finite_sets]
anti_symetry [definition, in CanonBDDs.canonicite.Order]
Assign [definition, in CanonBDDs.canonicite.Boolean_functions]
Assign [definition, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Assignment_of [definition, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Assign_of_sub_eq [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Assign_of_sub [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Assign_of_cons_eq [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Assign_of_cons [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Assign_n_finite [lemma, in CanonBDDs.canonicite.Boolean_functions]
Assign_k_finite [lemma, in CanonBDDs.canonicite.Boolean_functions]
Assign_gt [definition, in CanonBDDs.canonicite.Boolean_functions]
Assign_subst [axiom, in CanonBDDs.canonicite.Boolean_functions]
Assign_eq_trans [lemma, in CanonBDDs.canonicite.Boolean_functions]
Assign_eq_sym [lemma, in CanonBDDs.canonicite.Boolean_functions]
Assign_eq_refl [lemma, in CanonBDDs.canonicite.Boolean_functions]
Assign_eq [inductive, in CanonBDDs.canonicite.Boolean_functions]
Assign_n_inhabited [lemma, in CanonBDDs.canonicite.Boolean_functions]
Ass_of_well_defined [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Ass_eq_trans [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Ass_eq_sym [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Ass_eq_refl [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Ass_eq [definition, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
A_Dep_xi_dec [lemma, in CanonBDDs.canonicite.Boolean_functions]
B
BDT [inductive, in CanonBDDs.rauzy.algorithme1.BDTs]BDT [inductive, in CanonBDDs.canonicite.BDTs]
BDTs [library]
BDTs [library]
BDT_matching2 [lemma, in CanonBDDs.rauzy.algorithme1.Inductions]
BDT_matching1 [lemma, in CanonBDDs.rauzy.algorithme1.Inductions]
BDT_iso_BDF_eq [lemma, in CanonBDDs.canonicite.BDTs]
BDT_eq_node [constructor, in CanonBDDs.canonicite.BDTs]
BDT_eq_1 [constructor, in CanonBDDs.canonicite.BDTs]
BDT_eq_0 [constructor, in CanonBDDs.canonicite.BDTs]
BDT_eq [inductive, in CanonBDDs.canonicite.BDTs]
BDT2_of_One [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
BDT2_of_Zero [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
BF [definition, in CanonBDDs.canonicite.Boolean_functions]
BF [definition, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
BF_eq_Mon_Mon [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
BF_eq_same_dep_var [lemma, in CanonBDDs.canonicite.Boolean_functions]
BF_eq_Restr [lemma, in CanonBDDs.canonicite.Boolean_functions]
BF_eq_congr [lemma, in CanonBDDs.canonicite.Boolean_functions]
BF_eq_trans [lemma, in CanonBDDs.canonicite.Boolean_functions]
BF_eq_sym [lemma, in CanonBDDs.canonicite.Boolean_functions]
BF_eq_refl [lemma, in CanonBDDs.canonicite.Boolean_functions]
BF_eq [definition, in CanonBDDs.canonicite.Boolean_functions]
BF_eq_congruence_op3 [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
BF_eq_congruence_op1 [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
BF_eq_congruence_op2 [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
BF_eq_trans [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
BF_eq_sym [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
BF_eq_refl [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
BF_eq [definition, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Boolean [definition, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Boolean_OR [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Boolean_AND [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Boolean_functions [library]
Boolean_functions [library]
Bool_exp [inductive, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Bottom_implicant [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
b1_W_One [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
b1_W_Zero [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
C
Canonicity [library]Canonicity_Boolexp [lemma, in CanonBDDs.rauzy.algorithme1.Canonicity]
Canonicity_BF [lemma, in CanonBDDs.rauzy.algorithme1.Canonicity]
Canonicity_BDT_BF [lemma, in CanonBDDs.canonicite.Canonicity_BDT]
Canonicity_BF_BDT [lemma, in CanonBDDs.canonicite.Canonicity_BDT]
Canonicity_BDT [library]
cardinal [inductive, in CanonBDDs.canonicite.Finite_sets]
cardinalO_empty [lemma, in CanonBDDs.canonicite.Finite_sets]
cardinal_finite [lemma, in CanonBDDs.canonicite.Finite_sets]
cardinal_inv [lemma, in CanonBDDs.canonicite.Finite_sets]
CardO_cst_fct [lemma, in CanonBDDs.canonicite.Boolean_functions]
CardO_no_Dep_Var [lemma, in CanonBDDs.canonicite.Boolean_functions]
CardSk_Card_Restr [lemma, in CanonBDDs.canonicite.Boolean_functions]
CardSk_Greatest [lemma, in CanonBDDs.canonicite.Boolean_functions]
Card_gtO_exist_greatest [lemma, in CanonBDDs.canonicite.Finite_sets]
card_soustr_1 [lemma, in CanonBDDs.canonicite.Finite_sets]
card_add [constructor, in CanonBDDs.canonicite.Finite_sets]
card_empty [constructor, in CanonBDDs.canonicite.Finite_sets]
Cases_Assign_i [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Case_recursion.HDw [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Case_recursion.HOw [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Case_recursion.w [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Case_recursion.HDpr [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Case_recursion.HDpl [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Case_recursion.HOpr [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Case_recursion.HOpl [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Case_recursion.pr [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Case_recursion.pl [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Case_recursion.HO [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Case_recursion.r [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Case_recursion.l [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Case_recursion.i [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Case_recursion [section, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
case_right [constructor, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
case_middle [constructor, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
case_left [constructor, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Case3 [inductive, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Choice [definition, in CanonBDDs.rauzy.algorithme1.BDTs]
Choices_eq_bdts_eq [lemma, in CanonBDDs.rauzy.algorithme1.Canonicity]
Choice_Fun_eq_Fun_Choice [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
Choice_dim_decrease [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
Choice_right [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
Choice_left [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
Choice_invariant [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
Classic [axiom, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Commutative_orb [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Commutative_andb [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Commutative_OR [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Commutative_AND [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Commute_Frestr_IF [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Commute_if_bool_op2 [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Commute_if_not [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Compar [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Complete [definition, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
complete_induction [lemma, in CanonBDDs.canonicite.Complete_induction]
Complete_induction [library]
Completness [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Components_eq_nodes_eq [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
Cons [definition, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Constant_fct_inv [lemma, in CanonBDDs.canonicite.Boolean_functions]
Constant_fct [inductive, in CanonBDDs.canonicite.Boolean_functions]
Cons_of_non_depvar [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Cons_equal_head_equal [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Cons_ordered [constructor, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Contra [lemma, in CanonBDDs.canonicite.Prelude0]
Contra [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Correct [definition, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Correctness [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Corr_hl_Corr_node [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
course_of_values [lemma, in CanonBDDs.canonicite.Complete_induction]
Cpl [definition, in CanonBDDs.rauzy.algorithme1.Inductions]
Cst_fct_Fzero_Fone [lemma, in CanonBDDs.canonicite.Canonicity_BDT]
Cst_Ass [definition, in CanonBDDs.canonicite.Boolean_functions]
D
decidable [inductive, in CanonBDDs.canonicite.Finite_sets]decidable_finite [lemma, in CanonBDDs.canonicite.Finite_sets]
decidable_on [inductive, in CanonBDDs.canonicite.Finite_sets]
Decrease_n1n2_n1l2 [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
Decrease_n1n2_n1h2 [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
Decrease_n1n2_l1l2 [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
Decrease_n1n2_h1h2 [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
Decrease_n1n2_l1n2 [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
Decrease_n1n2_h1n2 [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
Decrease_induction1.HO2 [variable, in CanonBDDs.rauzy.algorithme1.BDTs]
Decrease_induction1.l2 [variable, in CanonBDDs.rauzy.algorithme1.BDTs]
Decrease_induction1.h2 [variable, in CanonBDDs.rauzy.algorithme1.BDTs]
Decrease_induction1.HO1 [variable, in CanonBDDs.rauzy.algorithme1.BDTs]
Decrease_induction1.l1 [variable, in CanonBDDs.rauzy.algorithme1.BDTs]
Decrease_induction1.h1 [variable, in CanonBDDs.rauzy.algorithme1.BDTs]
Decrease_induction1.i2 [variable, in CanonBDDs.rauzy.algorithme1.BDTs]
Decrease_induction1.i1 [variable, in CanonBDDs.rauzy.algorithme1.BDTs]
Decrease_induction1 [section, in CanonBDDs.rauzy.algorithme1.BDTs]
dec_addQx_dec_Q [lemma, in CanonBDDs.canonicite.Finite_sets]
Def_greatest [constructor, in CanonBDDs.canonicite.Finite_sets]
Def_dec_on [constructor, in CanonBDDs.canonicite.Finite_sets]
Def_dec [constructor, in CanonBDDs.canonicite.Finite_sets]
Def_inh [constructor, in CanonBDDs.canonicite.Finite_sets]
Def_set_eq [constructor, in CanonBDDs.canonicite.Finite_sets]
Def_notImplicant [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
Def_Implicant [constructor, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
Def_cst_fct [constructor, in CanonBDDs.canonicite.Boolean_functions]
Def_GreatestDV [constructor, in CanonBDDs.canonicite.Boolean_functions]
Def_Assign_eq [constructor, in CanonBDDs.canonicite.Boolean_functions]
deMorgan_or_not [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
deMorgan_not_and [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
deMorgan_and_not [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
deMorgan_not_or [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Denote [definition, in CanonBDDs.canonicite.BDTs]
Denote_true_false [lemma, in CanonBDDs.canonicite.Canonicity_BDT]
Denote_inv_OBDT [lemma, in CanonBDDs.canonicite.BDTs]
Denote_inv_eq [lemma, in CanonBDDs.canonicite.BDTs]
Dep_Restrf_incl_Depf [lemma, in CanonBDDs.canonicite.Boolean_functions]
Dep_set_finite [lemma, in CanonBDDs.canonicite.Boolean_functions]
Dep_set_decidable [lemma, in CanonBDDs.canonicite.Boolean_functions]
Dep_set [definition, in CanonBDDs.canonicite.Boolean_functions]
Dep_Restr_f_Dep_f [lemma, in CanonBDDs.canonicite.Boolean_functions]
Dep_Var [definition, in CanonBDDs.canonicite.Boolean_functions]
Dep_Var [definition, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
dim [inductive, in CanonBDDs.rauzy.algorithme1.BDTs]
Dim [definition, in CanonBDDs.rauzy.algorithme1.BDTs]
dimension [inductive, in CanonBDDs.canonicite.BDTs]
Dimension [definition, in CanonBDDs.canonicite.BDTs]
Dim_is_depvar_max [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
Dim_gt_O_node_decomposition [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
Dim_node_gt_O [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
dim_node_dim_sons [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
dim_Dim [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
dim_node [constructor, in CanonBDDs.rauzy.algorithme1.BDTs]
dim_one [constructor, in CanonBDDs.rauzy.algorithme1.BDTs]
dim_zero [constructor, in CanonBDDs.rauzy.algorithme1.BDTs]
Dim_highest_var_of_prime [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Dim_is_Greatest_Dep_Var [lemma, in CanonBDDs.canonicite.BDTs]
Dim_node_Dim_bl [lemma, in CanonBDDs.canonicite.BDTs]
Dim_node_Dim_bh [lemma, in CanonBDDs.canonicite.BDTs]
Dim_le_n [lemma, in CanonBDDs.canonicite.BDTs]
dim_Dim [lemma, in CanonBDDs.canonicite.BDTs]
dim_inv [variable, in CanonBDDs.canonicite.BDTs]
dim_functional [lemma, in CanonBDDs.canonicite.BDTs]
dim_node [constructor, in CanonBDDs.canonicite.BDTs]
dim_one [constructor, in CanonBDDs.canonicite.BDTs]
dim_zero [constructor, in CanonBDDs.canonicite.BDTs]
Divides [definition, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Divides_implic_implic [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
Divides_Inf [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
Divides_cons_divides_tail [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Divides_tail_divides_cons [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Divides_Nil_is_Nil [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Divides_p_cons_ip [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Divides_trans [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Divides_reflexive [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Div_div_ass_eq [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
E
empty [definition, in CanonBDDs.canonicite.Finite_sets]empty_union_P [lemma, in CanonBDDs.canonicite.Finite_sets]
Empty_is_Nil [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
eq_add [lemma, in CanonBDDs.canonicite.Finite_sets]
eq_BDT_decidable [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
eq_Max [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
eq_O_or_gt_O [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
eq_decidable [definition, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
eq_bool_dec [lemma, in CanonBDDs.canonicite.Prelude1]
eq_Var_eq_values [lemma, in CanonBDDs.canonicite.Boolean_functions]
eq_if_false_g [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
eq_if_true_f [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
eq_f_iff [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
eq_Fi_if_i [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
eq_Var_dec [lemma, in CanonBDDs.canonicite.Vars]
eq_Var_trans [lemma, in CanonBDDs.canonicite.Vars]
eq_Var_sym [lemma, in CanonBDDs.canonicite.Vars]
eq_Var_refl [lemma, in CanonBDDs.canonicite.Vars]
eq_Var_same_order [lemma, in CanonBDDs.canonicite.Vars]
eq_Var [definition, in CanonBDDs.canonicite.Vars]
excluded_middle [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Existence [lemma, in CanonBDDs.canonicite.Canonicity_BDT]
Existence [lemma, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Existence_Op_W [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Existence_BDT2 [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Existence_Not_BDT [lemma, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Exist_DepO [lemma, in CanonBDDs.canonicite.Canonicity_BDT]
Exist_dim [lemma, in CanonBDDs.canonicite.BDTs]
extensionality [axiom, in CanonBDDs.canonicite.Finite_sets]
Extensionality_Assignments [axiom, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
F
f [definition, in CanonBDDs.rauzy.algorithme1.Inductions]F [definition, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Fa [constructor, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
FALSE [definition, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
FALSE_neutral_OR [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
FALSE_absorb_AND [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
FB12 [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
FB12bis [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Fcst [definition, in CanonBDDs.canonicite.Boolean_functions]
Fcst [definition, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Fcst_monotonic [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
Fcst_no_depvar [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
finite [inductive, in CanonBDDs.canonicite.Finite_sets]
finite_image [lemma, in CanonBDDs.canonicite.Finite_sets]
finite_union [lemma, in CanonBDDs.canonicite.Finite_sets]
finite_decidable [lemma, in CanonBDDs.canonicite.Finite_sets]
finite_cardinal [lemma, in CanonBDDs.canonicite.Finite_sets]
finite_add [constructor, in CanonBDDs.canonicite.Finite_sets]
finite_empty [constructor, in CanonBDDs.canonicite.Finite_sets]
Finite_sets [library]
Formula_to_BDT [library]
Frestr [definition, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Frestr_Fi_j [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Frestr_Fi_false [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Frestr_Fi_true [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Frestr_Fi_i_b [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
FShannon_expansion [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Fun [definition, in CanonBDDs.rauzy.algorithme1.BDTs]
Fun [definition, in CanonBDDs.canonicite.BDTs]
Fun_eq_Fun_choice_eq [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
Fun_sons_dim_nondep [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
Fun_node_case_right [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
Fun_node_case_left [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
Fun_eq_OBDT_eq [lemma, in CanonBDDs.canonicite.BDTs]
Fun_Bexp [definition, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
f_Restr_f [lemma, in CanonBDDs.canonicite.Boolean_functions]
F_eq_Frestr_eq [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
G
greatest [inductive, in CanonBDDs.canonicite.Finite_sets]Greatest_Dep_Var [inductive, in CanonBDDs.canonicite.Boolean_functions]
Gst_Dep_Var_inv_Greatest [lemma, in CanonBDDs.canonicite.Boolean_functions]
Gst_Dep_Var_inv_Dep [lemma, in CanonBDDs.canonicite.Boolean_functions]
Gt_dim_out_of_solution [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
gt_mn_gt_Max_mn [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
gt_Max [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
gt_le_weak [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
gt_neq [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
gt_lt [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
gt_Var [definition, in CanonBDDs.canonicite.Vars]
H
Head [definition, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]Head_sub_ordered [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Head_of_solution_le_dim [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Head_max_of_ordered_path [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Head_of_p_in_p [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
I
IF_ [definition, in CanonBDDs.rauzy.algorithme1.Boolean_functions]Im [definition, in CanonBDDs.canonicite.Finite_sets]
Implicant [inductive, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
Implicants_TRUE [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
Impl_Sons.HO [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
Impl_Sons.l [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
Impl_Sons.h [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
Impl_Sons.i [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
Impl_Sons [section, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
Impl_Node.l [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
Impl_Node.h [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
Impl_Node.i [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
Impl_Node [section, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
Im_add [lemma, in CanonBDDs.canonicite.Finite_sets]
In [definition, in CanonBDDs.canonicite.Finite_sets]
incl [definition, in CanonBDDs.canonicite.Finite_sets]
incl_st_card_lt [lemma, in CanonBDDs.canonicite.Finite_sets]
incl_st_add_soustr [lemma, in CanonBDDs.canonicite.Finite_sets]
incl_soustr_add_r [lemma, in CanonBDDs.canonicite.Finite_sets]
incl_soustr_add_l [lemma, in CanonBDDs.canonicite.Finite_sets]
incl_soustr [lemma, in CanonBDDs.canonicite.Finite_sets]
incl_soustr_in [lemma, in CanonBDDs.canonicite.Finite_sets]
incl_st_add_x [lemma, in CanonBDDs.canonicite.Finite_sets]
incl_add_x [lemma, in CanonBDDs.canonicite.Finite_sets]
incl_add [lemma, in CanonBDDs.canonicite.Finite_sets]
incl_Q_add [lemma, in CanonBDDs.canonicite.Finite_sets]
incl_empty [lemma, in CanonBDDs.canonicite.Finite_sets]
incl_allV [lemma, in CanonBDDs.canonicite.Finite_sets]
incl_trans [lemma, in CanonBDDs.canonicite.Finite_sets]
incl_refl [lemma, in CanonBDDs.canonicite.Finite_sets]
incl_st [definition, in CanonBDDs.canonicite.Finite_sets]
incl_nil_eq [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Inductions [library]
Induction1 [lemma, in CanonBDDs.rauzy.algorithme1.Inductions]
Induction1_prop [axiom, in CanonBDDs.rauzy.algorithme1.Inductions]
Induction1' [lemma, in CanonBDDs.rauzy.algorithme1.Inductions]
Induction2 [lemma, in CanonBDDs.rauzy.algorithme1.Inductions]
ind1_ind2 [lemma, in CanonBDDs.rauzy.algorithme1.Inductions]
Inf [definition, in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
Inf_trans [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
Inf_refl [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
inhabited [inductive, in CanonBDDs.canonicite.Finite_sets]
inh_card_gt_O [lemma, in CanonBDDs.canonicite.Finite_sets]
inter [definition, in CanonBDDs.canonicite.Finite_sets]
Intervals [section, in CanonBDDs.canonicite.Vars]
Intervals.n [variable, in CanonBDDs.canonicite.Vars]
inter_intro [lemma, in CanonBDDs.canonicite.Finite_sets]
inter_incl_r [lemma, in CanonBDDs.canonicite.Finite_sets]
inter_incl_l [lemma, in CanonBDDs.canonicite.Finite_sets]
inv_greatest_R [lemma, in CanonBDDs.canonicite.Finite_sets]
inv_greatest_In [lemma, in CanonBDDs.canonicite.Finite_sets]
inv_inh_addQx [lemma, in CanonBDDs.canonicite.Finite_sets]
inv_dec_on [lemma, in CanonBDDs.canonicite.Finite_sets]
inv_OBDT_neq [definition, in CanonBDDs.rauzy.algorithme1.BDTs]
inv_OBDT_order [definition, in CanonBDDs.rauzy.algorithme1.BDTs]
inv_OBDT_dim [definition, in CanonBDDs.rauzy.algorithme1.BDTs]
Inv_Assignment_of_false [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Inv_Assignment_of_true [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Inv_Solution [definition, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
inv_Ordered [definition, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
inv_notImplicant [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
inv_Implicant [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
inv_OBDT_bh [definition, in CanonBDDs.canonicite.BDTs]
inv_OBDT_bl [definition, in CanonBDDs.canonicite.BDTs]
inv_OBDT_eq [definition, in CanonBDDs.canonicite.BDTs]
inv_OBDT_Order [definition, in CanonBDDs.canonicite.BDTs]
inv_BDT_eq_node [lemma, in CanonBDDs.canonicite.BDTs]
inv_BDT_eq [definition, in CanonBDDs.canonicite.BDTs]
In_not_In_sym [lemma, in CanonBDDs.canonicite.Finite_sets]
In_not_In [lemma, in CanonBDDs.canonicite.Finite_sets]
in_add_x [lemma, in CanonBDDs.canonicite.Finite_sets]
in_allV [lemma, in CanonBDDs.canonicite.Finite_sets]
in_empty [lemma, in CanonBDDs.canonicite.Finite_sets]
in_Q_add [lemma, in CanonBDDs.canonicite.Finite_sets]
In_list_dec [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
I_out_of_Sub_ip [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
I_of_cons_ip [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
J
jofp_jofsub_ip [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]L
La_4bis [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]Lb_4bis [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Lc_4bis [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
LC2_C_fac1 [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
LC2_S_fac1 [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Ld_4bis [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Le_4bis [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
le_Max [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
le_dec [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
le_ne_gt [lemma, in CanonBDDs.canonicite.Prelude1]
le_nSm_le_nm_or_eq [lemma, in CanonBDDs.canonicite.Prelude1]
le_dec_0 [lemma, in CanonBDDs.canonicite.Prelude1]
le_split [lemma, in CanonBDDs.canonicite.Complete_induction]
le_Var_total_order [lemma, in CanonBDDs.canonicite.Vars]
le_or_gt_Var [lemma, in CanonBDDs.canonicite.Vars]
le_Var [definition, in CanonBDDs.canonicite.Vars]
Lower [definition, in CanonBDDs.rauzy.algorithme1.Inductions]
Lower_well_founded [lemma, in CanonBDDs.rauzy.algorithme1.Inductions]
LP2 [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
lt_gt [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
lt_hereditary [definition, in CanonBDDs.canonicite.Complete_induction]
LT1 [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
L_Dep_Var2 [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
L_Dep_Var1 [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
L_Assign3 [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
L_Assign2 [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
L_Assign1 [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
L1 [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
L1 [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
L10 [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
L11 [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
L12 [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
L13 [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
L14 [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
L14bis [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
L15 [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
L2 [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
L4 [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
L4bis [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
L40 [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
L5 [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
L5bis [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
L8 [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
L80 [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
L9 [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
M
Max [definition, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]Maxdim [definition, in CanonBDDs.rauzy.algorithme1.BDTs]
Max_mon_middle [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Max_mon_right [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Max_mon_left [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Max_sym [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Max_le [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Measure_decrease [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
Monotonic [definition, in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
Monotony [library]
Mon_node_Mon_sons [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
Mon_Frestr_Mon [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
Morgan_and_not [lemma, in CanonBDDs.canonicite.Prelude0]
Morgan_or [lemma, in CanonBDDs.canonicite.Prelude0]
N
n [axiom, in CanonBDDs.canonicite.Canonicity_BDT]nat_wf_ind [lemma, in CanonBDDs.canonicite.Complete_induction]
neq_right_neq_BDTs [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
neq_left_neq_BDTs [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
neq_vars_neq_BDTs [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
neq_Node_Zero [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
neq_Node_One [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
neq_One_Zero [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
neq_Zero_One [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
ne_Fone_Fzero [lemma, in CanonBDDs.canonicite.BDTs]
ne_Fzero_Fone [lemma, in CanonBDDs.canonicite.BDTs]
ne_node_one [lemma, in CanonBDDs.canonicite.BDTs]
ne_node_zero [lemma, in CanonBDDs.canonicite.BDTs]
ne_one_node [lemma, in CanonBDDs.canonicite.BDTs]
ne_one_zero [lemma, in CanonBDDs.canonicite.BDTs]
ne_zero_node [lemma, in CanonBDDs.canonicite.BDTs]
ne_zero_one [lemma, in CanonBDDs.canonicite.BDTs]
Nil [definition, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Nil_only_prime_of_TRUE [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Nil_prime_of_TRUE [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Nil_ordered [constructor, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Nil_divides_all [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Nil_or_not_Nil [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Nil_or_cons [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
nil_included_all [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Node [constructor, in CanonBDDs.rauzy.algorithme1.BDTs]
node [constructor, in CanonBDDs.canonicite.BDTs]
node_exist [constructor, in CanonBDDs.rauzy.algorithme1.BDTs]
node_decomposition [inductive, in CanonBDDs.rauzy.algorithme1.BDTs]
Node_W_Node_i2_gt_i1 [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Node_W_Node_i1_eq_i2 [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Node_W_Node_i1_eq_i2_neq [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Node_W_Node_i1_eq_i2_eq [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Node_W_Node_i1_gt_i2 [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Node_W_Node_i1_gt_i2_neq [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Node_W_Node_i1_gt_i2_eq [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Node_to_Sons.p [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Node_to_Sons.HO [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Node_to_Sons.l [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Node_to_Sons.h [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Node_to_Sons.i [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Node_to_Sons [section, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
node_exist [constructor, in CanonBDDs.canonicite.BDTs]
node_decomposition [inductive, in CanonBDDs.canonicite.BDTs]
Not [constructor, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
NOT [definition, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
notall_existnot_singleton [lemma, in CanonBDDs.canonicite.Finite_sets]
notall_addQx_notall_Q [lemma, in CanonBDDs.canonicite.Finite_sets]
notP_notinterPQ [lemma, in CanonBDDs.canonicite.Finite_sets]
notQ_notinterPQ [lemma, in CanonBDDs.canonicite.Finite_sets]
not_All_Exist_not [lemma, in CanonBDDs.canonicite.Finite_sets]
not_Exist_All_not [lemma, in CanonBDDs.canonicite.Finite_sets]
not_In_soustr_eq [lemma, in CanonBDDs.canonicite.Finite_sets]
not_In_soustr [lemma, in CanonBDDs.canonicite.Finite_sets]
Not_of_cons_ip [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
not_all_exist_not [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Not_BDT [lemma, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
No_prime_FALSE [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
No_solution_Zero [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
No_implicant_FALSE [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
no_Dep_Var_Cstk [lemma, in CanonBDDs.canonicite.Boolean_functions]
O
OBDT [inductive, in CanonBDDs.rauzy.algorithme1.BDTs]OBDT [inductive, in CanonBDDs.canonicite.BDTs]
Of [definition, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Of_sub_pi_of_p [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Of_cons_ip_of_p [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Of_p_of_cons_ip [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Of_path_dec [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
One [constructor, in CanonBDDs.rauzy.algorithme1.BDTs]
one [constructor, in CanonBDDs.canonicite.BDTs]
One_W_Node [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
onQ_not_All_Exist_not [lemma, in CanonBDDs.canonicite.Finite_sets]
Operator_W [library]
Op2_BDT_overloaded [lemma, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Or [constructor, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
OR [definition, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
order [definition, in CanonBDDs.canonicite.Finite_sets]
Order [definition, in CanonBDDs.canonicite.Vars]
order [definition, in CanonBDDs.canonicite.Order]
Order [library]
Ordered [inductive, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Ordered_node_ordered_restr [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
ordered_node_ordered_sons [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
ordered_node_a_son_neq_zero [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
ordered_node_neq_sons [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
Ordered_p_ordered_sub_pi [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Ordered_divisor_of_cons_ip [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Ordered_paths_eq [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Ordered_cons_ordered_tail [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Ordering_surj [lemma, in CanonBDDs.canonicite.Vars]
order_node [constructor, in CanonBDDs.rauzy.algorithme1.BDTs]
order_1 [constructor, in CanonBDDs.rauzy.algorithme1.BDTs]
order_0 [constructor, in CanonBDDs.rauzy.algorithme1.BDTs]
order_node [constructor, in CanonBDDs.canonicite.BDTs]
order_1 [constructor, in CanonBDDs.canonicite.BDTs]
order_0 [constructor, in CanonBDDs.canonicite.BDTs]
Order_S [lemma, in CanonBDDs.canonicite.Vars]
Order_gt_O [lemma, in CanonBDDs.canonicite.Vars]
Order_le_n [lemma, in CanonBDDs.canonicite.Vars]
Or_BDT [lemma, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Or_BDT_overloaded [lemma, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Or_BDT_b1_One [lemma, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Or_BDT_b1_Zero [lemma, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Or_BDT_One_b2 [lemma, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Or_BDT_Zero_b2 [lemma, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Outof_p_outof_sub_ip [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
P
Path [definition, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]Prelude_Paths [library]
Prelude_Primes [library]
Prelude_Implicants [library]
Prelude_BDT [library]
Prelude0 [library]
Prelude1 [library]
Prime [definition, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Primes [library]
Prime_exists [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Prime_h_prime_node [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Prime_l_prime_node [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Prime_h_cons_ip_ordered [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Prime_ordered [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Prime_implicant [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Proof_irrelevance [axiom, in CanonBDDs.canonicite.Vars]
Pr1 [definition, in CanonBDDs.rauzy.algorithme1.Inductions]
Pr2 [definition, in CanonBDDs.rauzy.algorithme1.Inductions]
Pth_ord9 [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Pth_ord8 [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
P_dec_AllP_dec [lemma, in CanonBDDs.canonicite.Finite_sets]
P_dec_on_Q_AllP_dec_on_Q [lemma, in CanonBDDs.canonicite.Finite_sets]
P_union_empty [lemma, in CanonBDDs.canonicite.Finite_sets]
p_inv_OBDT_neq [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
p_inv_OBDT_order [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
p_inv_OBDT_dim [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
p_inv_Solution [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
p_inv_Ordered [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
P_notnotP [lemma, in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
p_inv_OBDT_bh [lemma, in CanonBDDs.canonicite.BDTs]
p_inv_OBDT_bl [lemma, in CanonBDDs.canonicite.BDTs]
p_inv_OBDT_eq [lemma, in CanonBDDs.canonicite.BDTs]
p_inv_OBDT_order [lemma, in CanonBDDs.canonicite.BDTs]
p_inv_BDT_eq [lemma, in CanonBDDs.canonicite.BDTs]
p_dim_inv [lemma, in CanonBDDs.canonicite.BDTs]
Q
QinterS_addQxinterS [lemma, in CanonBDDs.canonicite.Finite_sets]R
R [definition, in CanonBDDs.rauzy.algorithme1.Inductions]Recursion_W.Greater_i2.Hgt [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.Greater_i2 [section, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.Equal_i1_i2.Hl [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.Equal_i1_i2.bl [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.Equal_i1_i2.Hh [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.Equal_i1_i2.bh [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.Equal_i1_i2.Heq_dims [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.Equal_i1_i2 [section, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.Greater_i1.Hl [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.Greater_i1.bl [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.Greater_i1.Hh [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.Greater_i1.bh [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.Greater_i1.Hgt [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.Greater_i1 [section, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.Hmon [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.HO2 [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.HO1 [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.l2 [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.l1 [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.h2 [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.h1 [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.i2 [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.i1 [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W [section, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
reflexivity [definition, in CanonBDDs.canonicite.Finite_sets]
reflexivity [definition, in CanonBDDs.canonicite.Order]
Restr [definition, in CanonBDDs.canonicite.Boolean_functions]
Restr_le_n_Fcst [lemma, in CanonBDDs.canonicite.Boolean_functions]
Restr_le_k_Restr_le_Sk [lemma, in CanonBDDs.canonicite.Boolean_functions]
Restr_le [definition, in CanonBDDs.canonicite.Boolean_functions]
Restr_xi_Restr_xj [lemma, in CanonBDDs.canonicite.Boolean_functions]
Restr_xi_Restr_xi [lemma, in CanonBDDs.canonicite.Boolean_functions]
Restr_node_Restr_high [lemma, in CanonBDDs.canonicite.BDTs]
Restr_node_Restr_low [lemma, in CanonBDDs.canonicite.BDTs]
Restr_Fcst [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Result_Ordered [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Rp [definition, in CanonBDDs.rauzy.algorithme1.Inductions]
S
same_order_eq_Var [lemma, in CanonBDDs.canonicite.Vars]set [definition, in CanonBDDs.canonicite.Finite_sets]
sets [section, in CanonBDDs.canonicite.Finite_sets]
sets.Add [section, in CanonBDDs.canonicite.Finite_sets]
sets.Add.Q [variable, in CanonBDDs.canonicite.Finite_sets]
sets.Add.x [variable, in CanonBDDs.canonicite.Finite_sets]
sets.Add.y [variable, in CanonBDDs.canonicite.Finite_sets]
sets.Greatest [section, in CanonBDDs.canonicite.Finite_sets]
sets.Greatest.R_total_order [variable, in CanonBDDs.canonicite.Finite_sets]
sets.inv_card [variable, in CanonBDDs.canonicite.Finite_sets]
sets.R [variable, in CanonBDDs.canonicite.Finite_sets]
sets.V [variable, in CanonBDDs.canonicite.Finite_sets]
sets.V_eq [variable, in CanonBDDs.canonicite.Finite_sets]
set_eq_trans [lemma, in CanonBDDs.canonicite.Finite_sets]
set_eq_sym [lemma, in CanonBDDs.canonicite.Finite_sets]
set_eq_refl [lemma, in CanonBDDs.canonicite.Finite_sets]
set_eq_inv [lemma, in CanonBDDs.canonicite.Finite_sets]
set_eq [inductive, in CanonBDDs.canonicite.Finite_sets]
Shannon_expansion [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
Shtree_Not [lemma, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Shtree_Or [lemma, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Shtree_And [lemma, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Shtree_Var [lemma, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Shtree_Fa [lemma, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Shtree_Tr [lemma, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Sh_exp_dim [lemma, in CanonBDDs.rauzy.algorithme1.BDTs]
Sh_tree_of [definition, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
singlx [lemma, in CanonBDDs.canonicite.Finite_sets]
Solution [inductive, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Solution_OBDT_ordered [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Solution_of_One_is_Nil [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Sol_Right [constructor, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Sol_Left [constructor, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Sol_One [constructor, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Sons_to_Node.p [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Sons_to_Node.HO [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Sons_to_Node.l [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Sons_to_Node.h [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Sons_to_Node.i [variable, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Sons_to_Node [section, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Sound [definition, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Soundness [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Soundness_left [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Soundness_left_smallest_out [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Soundness_left_smallest_in [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Soundness_left_smallest_order [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Soundness_left_impl [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Soundness_right [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
soustr [definition, in CanonBDDs.canonicite.Finite_sets]
still_in_soustr [lemma, in CanonBDDs.canonicite.Finite_sets]
Sub [definition, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Sub_of_non_depvar [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
T
Tail_exists_with_dim_head [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]Tail_exists [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Tautology [definition, in CanonBDDs.rauzy.algorithme1.Canonicity]
Tautology_decidable [lemma, in CanonBDDs.rauzy.algorithme1.Canonicity]
totality [definition, in CanonBDDs.canonicite.Finite_sets]
totality [definition, in CanonBDDs.canonicite.Order]
total_order [definition, in CanonBDDs.canonicite.Finite_sets]
total_order [definition, in CanonBDDs.canonicite.Order]
Tr [constructor, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
transitivity [definition, in CanonBDDs.canonicite.Finite_sets]
transitivity [definition, in CanonBDDs.canonicite.Order]
TRUE [definition, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
TRUE_neq_FALSE [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
TRUE_absorb_OR [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
TRUE_neutral_AND [lemma, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
U
union [definition, in CanonBDDs.canonicite.Finite_sets]union_add [lemma, in CanonBDDs.canonicite.Finite_sets]
union_sym [lemma, in CanonBDDs.canonicite.Finite_sets]
Uniqueness [lemma, in CanonBDDs.rauzy.algorithme1.Canonicity]
Uniqueness [lemma, in CanonBDDs.canonicite.Canonicity_BDT]
Unique_One [lemma, in CanonBDDs.rauzy.algorithme1.Canonicity]
Unique_Zero [lemma, in CanonBDDs.rauzy.algorithme1.Canonicity]
Upd [definition, in CanonBDDs.canonicite.Boolean_functions]
Upd [definition, in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Upd_preserves_Inf [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
Upd_xi_xj [lemma, in CanonBDDs.canonicite.Boolean_functions]
Upd_le_O_Id [lemma, in CanonBDDs.canonicite.Boolean_functions]
Upd_le_n_Cst [lemma, in CanonBDDs.canonicite.Boolean_functions]
Upd_le [definition, in CanonBDDs.canonicite.Boolean_functions]
Upd' [definition, in CanonBDDs.canonicite.Boolean_functions]
V
Var [constructor, in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]Var [inductive, in CanonBDDs.canonicite.Vars]
Vars [library]
Varset [definition, in CanonBDDs.canonicite.Vars]
Vars_prime_le_dim [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
vars_sup_dim_non_dep2 [lemma, in CanonBDDs.canonicite.BDTs]
vars_sup_dim_non_dep [lemma, in CanonBDDs.canonicite.BDTs]
Var_n_finite [lemma, in CanonBDDs.canonicite.Vars]
Var_k_finite [lemma, in CanonBDDs.canonicite.Vars]
Var_le [definition, in CanonBDDs.canonicite.Vars]
Var_intro [constructor, in CanonBDDs.canonicite.Vars]
VR [section, in CanonBDDs.canonicite.Order]
VR.R [variable, in CanonBDDs.canonicite.Order]
VR.V [variable, in CanonBDDs.canonicite.Order]
VR.V_eq [variable, in CanonBDDs.canonicite.Order]
V_decidable [axiom, in CanonBDDs.canonicite.Finite_sets]
W
Wf_ind1 [lemma, in CanonBDDs.rauzy.algorithme1.Inductions]W_correct [definition, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
W_complete [definition, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
W_sound [definition, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
X
xi_non_dep_Restr_xi [lemma, in CanonBDDs.canonicite.Boolean_functions]xi_non_dep_Restr_xi_Id [lemma, in CanonBDDs.canonicite.Boolean_functions]
Z
Zero [constructor, in CanonBDDs.rauzy.algorithme1.BDTs]zero [constructor, in CanonBDDs.canonicite.BDTs]
Zero_W_Node [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Zero_complete [lemma, in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
other
IF _ then _ else _ [notation, in CanonBDDs.rauzy.algorithme1.Boolean_functions]Notation Index
other
IF _ then _ else _ [in CanonBDDs.rauzy.algorithme1.Boolean_functions]Variable Index
C
Case_recursion.HDw [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]Case_recursion.HOw [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Case_recursion.w [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Case_recursion.HDpr [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Case_recursion.HDpl [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Case_recursion.HOpr [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Case_recursion.HOpl [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Case_recursion.pr [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Case_recursion.pl [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Case_recursion.HO [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Case_recursion.r [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Case_recursion.l [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Case_recursion.i [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
D
Decrease_induction1.HO2 [in CanonBDDs.rauzy.algorithme1.BDTs]Decrease_induction1.l2 [in CanonBDDs.rauzy.algorithme1.BDTs]
Decrease_induction1.h2 [in CanonBDDs.rauzy.algorithme1.BDTs]
Decrease_induction1.HO1 [in CanonBDDs.rauzy.algorithme1.BDTs]
Decrease_induction1.l1 [in CanonBDDs.rauzy.algorithme1.BDTs]
Decrease_induction1.h1 [in CanonBDDs.rauzy.algorithme1.BDTs]
Decrease_induction1.i2 [in CanonBDDs.rauzy.algorithme1.BDTs]
Decrease_induction1.i1 [in CanonBDDs.rauzy.algorithme1.BDTs]
dim_inv [in CanonBDDs.canonicite.BDTs]
I
Impl_Sons.HO [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]Impl_Sons.l [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
Impl_Sons.h [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
Impl_Sons.i [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
Impl_Node.l [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
Impl_Node.h [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
Impl_Node.i [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
Intervals.n [in CanonBDDs.canonicite.Vars]
N
Node_to_Sons.p [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]Node_to_Sons.HO [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Node_to_Sons.l [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Node_to_Sons.h [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Node_to_Sons.i [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
R
Recursion_W.Greater_i2.Hgt [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]Recursion_W.Equal_i1_i2.Hl [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.Equal_i1_i2.bl [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.Equal_i1_i2.Hh [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.Equal_i1_i2.bh [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.Equal_i1_i2.Heq_dims [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.Greater_i1.Hl [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.Greater_i1.bl [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.Greater_i1.Hh [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.Greater_i1.bh [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.Greater_i1.Hgt [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.Hmon [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.HO2 [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.HO1 [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.l2 [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.l1 [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.h2 [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.h1 [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.i2 [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.i1 [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
S
sets.Add.Q [in CanonBDDs.canonicite.Finite_sets]sets.Add.x [in CanonBDDs.canonicite.Finite_sets]
sets.Add.y [in CanonBDDs.canonicite.Finite_sets]
sets.Greatest.R_total_order [in CanonBDDs.canonicite.Finite_sets]
sets.inv_card [in CanonBDDs.canonicite.Finite_sets]
sets.R [in CanonBDDs.canonicite.Finite_sets]
sets.V [in CanonBDDs.canonicite.Finite_sets]
sets.V_eq [in CanonBDDs.canonicite.Finite_sets]
Sons_to_Node.p [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Sons_to_Node.HO [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Sons_to_Node.l [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Sons_to_Node.h [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Sons_to_Node.i [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
V
VR.R [in CanonBDDs.canonicite.Order]VR.V [in CanonBDDs.canonicite.Order]
VR.V_eq [in CanonBDDs.canonicite.Order]
Library Index
B
BDTsBDTs
Boolean_functions
Boolean_functions
C
CanonicityCanonicity_BDT
Complete_induction
F
Finite_setsFormula_to_BDT
I
InductionsM
MonotonyO
Operator_WOrder
P
Prelude_PathsPrelude_Primes
Prelude_Implicants
Prelude_BDT
Prelude0
Prelude1
Primes
V
VarsLemma Index
A
addQinterSx_addQxinterS [in CanonBDDs.canonicite.Finite_sets]addQxinterS_QinterS [in CanonBDDs.canonicite.Finite_sets]
addQxinterS_addQinterSx [in CanonBDDs.canonicite.Finite_sets]
add_soustr_xy [in CanonBDDs.canonicite.Finite_sets]
add_soustr_1 [in CanonBDDs.canonicite.Finite_sets]
add_soustr_2 [in CanonBDDs.canonicite.Finite_sets]
add_inh [in CanonBDDs.canonicite.Finite_sets]
add_in_or_eq [in CanonBDDs.canonicite.Finite_sets]
And_BDT [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
And_BDT_overloaded [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
And_BDT_b1_One [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
And_BDT_b1_Zero [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
And_BDT_One_b2 [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
And_BDT_Zero_b2 [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Anil_lowest [in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
Assign_of_sub_eq [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Assign_of_sub [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Assign_of_cons_eq [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Assign_of_cons [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Assign_n_finite [in CanonBDDs.canonicite.Boolean_functions]
Assign_k_finite [in CanonBDDs.canonicite.Boolean_functions]
Assign_eq_trans [in CanonBDDs.canonicite.Boolean_functions]
Assign_eq_sym [in CanonBDDs.canonicite.Boolean_functions]
Assign_eq_refl [in CanonBDDs.canonicite.Boolean_functions]
Assign_n_inhabited [in CanonBDDs.canonicite.Boolean_functions]
Ass_of_well_defined [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Ass_eq_trans [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Ass_eq_sym [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Ass_eq_refl [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
A_Dep_xi_dec [in CanonBDDs.canonicite.Boolean_functions]
B
BDT_matching2 [in CanonBDDs.rauzy.algorithme1.Inductions]BDT_matching1 [in CanonBDDs.rauzy.algorithme1.Inductions]
BDT_iso_BDF_eq [in CanonBDDs.canonicite.BDTs]
BDT2_of_One [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
BDT2_of_Zero [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
BF_eq_Mon_Mon [in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
BF_eq_same_dep_var [in CanonBDDs.canonicite.Boolean_functions]
BF_eq_Restr [in CanonBDDs.canonicite.Boolean_functions]
BF_eq_congr [in CanonBDDs.canonicite.Boolean_functions]
BF_eq_trans [in CanonBDDs.canonicite.Boolean_functions]
BF_eq_sym [in CanonBDDs.canonicite.Boolean_functions]
BF_eq_refl [in CanonBDDs.canonicite.Boolean_functions]
BF_eq_congruence_op3 [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
BF_eq_congruence_op1 [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
BF_eq_congruence_op2 [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
BF_eq_trans [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
BF_eq_sym [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
BF_eq_refl [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Boolean_OR [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Boolean_AND [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Bottom_implicant [in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
b1_W_One [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
b1_W_Zero [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
C
Canonicity_Boolexp [in CanonBDDs.rauzy.algorithme1.Canonicity]Canonicity_BF [in CanonBDDs.rauzy.algorithme1.Canonicity]
Canonicity_BDT_BF [in CanonBDDs.canonicite.Canonicity_BDT]
Canonicity_BF_BDT [in CanonBDDs.canonicite.Canonicity_BDT]
cardinalO_empty [in CanonBDDs.canonicite.Finite_sets]
cardinal_finite [in CanonBDDs.canonicite.Finite_sets]
cardinal_inv [in CanonBDDs.canonicite.Finite_sets]
CardO_cst_fct [in CanonBDDs.canonicite.Boolean_functions]
CardO_no_Dep_Var [in CanonBDDs.canonicite.Boolean_functions]
CardSk_Card_Restr [in CanonBDDs.canonicite.Boolean_functions]
CardSk_Greatest [in CanonBDDs.canonicite.Boolean_functions]
Card_gtO_exist_greatest [in CanonBDDs.canonicite.Finite_sets]
card_soustr_1 [in CanonBDDs.canonicite.Finite_sets]
Cases_Assign_i [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Choices_eq_bdts_eq [in CanonBDDs.rauzy.algorithme1.Canonicity]
Choice_Fun_eq_Fun_Choice [in CanonBDDs.rauzy.algorithme1.BDTs]
Choice_dim_decrease [in CanonBDDs.rauzy.algorithme1.BDTs]
Choice_right [in CanonBDDs.rauzy.algorithme1.BDTs]
Choice_left [in CanonBDDs.rauzy.algorithme1.BDTs]
Choice_invariant [in CanonBDDs.rauzy.algorithme1.BDTs]
Commutative_orb [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Commutative_andb [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Commutative_OR [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Commutative_AND [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Commute_Frestr_IF [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Commute_if_bool_op2 [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Commute_if_not [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Compar [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
complete_induction [in CanonBDDs.canonicite.Complete_induction]
Completness [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Components_eq_nodes_eq [in CanonBDDs.rauzy.algorithme1.BDTs]
Constant_fct_inv [in CanonBDDs.canonicite.Boolean_functions]
Cons_of_non_depvar [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Cons_equal_head_equal [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Contra [in CanonBDDs.canonicite.Prelude0]
Contra [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Correctness [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Corr_hl_Corr_node [in CanonBDDs.rauzy.algorithme1.BDTs]
course_of_values [in CanonBDDs.canonicite.Complete_induction]
Cst_fct_Fzero_Fone [in CanonBDDs.canonicite.Canonicity_BDT]
D
decidable_finite [in CanonBDDs.canonicite.Finite_sets]Decrease_n1n2_n1l2 [in CanonBDDs.rauzy.algorithme1.BDTs]
Decrease_n1n2_n1h2 [in CanonBDDs.rauzy.algorithme1.BDTs]
Decrease_n1n2_l1l2 [in CanonBDDs.rauzy.algorithme1.BDTs]
Decrease_n1n2_h1h2 [in CanonBDDs.rauzy.algorithme1.BDTs]
Decrease_n1n2_l1n2 [in CanonBDDs.rauzy.algorithme1.BDTs]
Decrease_n1n2_h1n2 [in CanonBDDs.rauzy.algorithme1.BDTs]
dec_addQx_dec_Q [in CanonBDDs.canonicite.Finite_sets]
Def_notImplicant [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
deMorgan_or_not [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
deMorgan_not_and [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
deMorgan_and_not [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
deMorgan_not_or [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Denote_true_false [in CanonBDDs.canonicite.Canonicity_BDT]
Denote_inv_OBDT [in CanonBDDs.canonicite.BDTs]
Denote_inv_eq [in CanonBDDs.canonicite.BDTs]
Dep_Restrf_incl_Depf [in CanonBDDs.canonicite.Boolean_functions]
Dep_set_finite [in CanonBDDs.canonicite.Boolean_functions]
Dep_set_decidable [in CanonBDDs.canonicite.Boolean_functions]
Dep_Restr_f_Dep_f [in CanonBDDs.canonicite.Boolean_functions]
Dim_is_depvar_max [in CanonBDDs.rauzy.algorithme1.BDTs]
Dim_gt_O_node_decomposition [in CanonBDDs.rauzy.algorithme1.BDTs]
Dim_node_gt_O [in CanonBDDs.rauzy.algorithme1.BDTs]
dim_node_dim_sons [in CanonBDDs.rauzy.algorithme1.BDTs]
dim_Dim [in CanonBDDs.rauzy.algorithme1.BDTs]
Dim_highest_var_of_prime [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Dim_is_Greatest_Dep_Var [in CanonBDDs.canonicite.BDTs]
Dim_node_Dim_bl [in CanonBDDs.canonicite.BDTs]
Dim_node_Dim_bh [in CanonBDDs.canonicite.BDTs]
Dim_le_n [in CanonBDDs.canonicite.BDTs]
dim_Dim [in CanonBDDs.canonicite.BDTs]
dim_functional [in CanonBDDs.canonicite.BDTs]
Divides_implic_implic [in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
Divides_Inf [in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
Divides_cons_divides_tail [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Divides_tail_divides_cons [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Divides_Nil_is_Nil [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Divides_p_cons_ip [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Divides_trans [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Divides_reflexive [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Div_div_ass_eq [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
E
empty_union_P [in CanonBDDs.canonicite.Finite_sets]Empty_is_Nil [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
eq_add [in CanonBDDs.canonicite.Finite_sets]
eq_BDT_decidable [in CanonBDDs.rauzy.algorithme1.BDTs]
eq_Max [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
eq_O_or_gt_O [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
eq_bool_dec [in CanonBDDs.canonicite.Prelude1]
eq_Var_eq_values [in CanonBDDs.canonicite.Boolean_functions]
eq_if_false_g [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
eq_if_true_f [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
eq_f_iff [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
eq_Fi_if_i [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
eq_Var_dec [in CanonBDDs.canonicite.Vars]
eq_Var_trans [in CanonBDDs.canonicite.Vars]
eq_Var_sym [in CanonBDDs.canonicite.Vars]
eq_Var_refl [in CanonBDDs.canonicite.Vars]
eq_Var_same_order [in CanonBDDs.canonicite.Vars]
excluded_middle [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Existence [in CanonBDDs.canonicite.Canonicity_BDT]
Existence [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Existence_Op_W [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Existence_BDT2 [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Existence_Not_BDT [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Exist_DepO [in CanonBDDs.canonicite.Canonicity_BDT]
Exist_dim [in CanonBDDs.canonicite.BDTs]
F
FALSE_neutral_OR [in CanonBDDs.rauzy.algorithme1.Boolean_functions]FALSE_absorb_AND [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
FB12 [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
FB12bis [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Fcst_monotonic [in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
Fcst_no_depvar [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
finite_image [in CanonBDDs.canonicite.Finite_sets]
finite_union [in CanonBDDs.canonicite.Finite_sets]
finite_decidable [in CanonBDDs.canonicite.Finite_sets]
finite_cardinal [in CanonBDDs.canonicite.Finite_sets]
Frestr_Fi_j [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Frestr_Fi_false [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Frestr_Fi_true [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Frestr_Fi_i_b [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
FShannon_expansion [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Fun_eq_Fun_choice_eq [in CanonBDDs.rauzy.algorithme1.BDTs]
Fun_sons_dim_nondep [in CanonBDDs.rauzy.algorithme1.BDTs]
Fun_node_case_right [in CanonBDDs.rauzy.algorithme1.BDTs]
Fun_node_case_left [in CanonBDDs.rauzy.algorithme1.BDTs]
Fun_eq_OBDT_eq [in CanonBDDs.canonicite.BDTs]
f_Restr_f [in CanonBDDs.canonicite.Boolean_functions]
F_eq_Frestr_eq [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
G
Gst_Dep_Var_inv_Greatest [in CanonBDDs.canonicite.Boolean_functions]Gst_Dep_Var_inv_Dep [in CanonBDDs.canonicite.Boolean_functions]
Gt_dim_out_of_solution [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
gt_mn_gt_Max_mn [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
gt_Max [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
gt_le_weak [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
gt_neq [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
gt_lt [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
H
Head_sub_ordered [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]Head_of_solution_le_dim [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Head_max_of_ordered_path [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Head_of_p_in_p [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
I
Implicants_TRUE [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]Im_add [in CanonBDDs.canonicite.Finite_sets]
incl_st_card_lt [in CanonBDDs.canonicite.Finite_sets]
incl_st_add_soustr [in CanonBDDs.canonicite.Finite_sets]
incl_soustr_add_r [in CanonBDDs.canonicite.Finite_sets]
incl_soustr_add_l [in CanonBDDs.canonicite.Finite_sets]
incl_soustr [in CanonBDDs.canonicite.Finite_sets]
incl_soustr_in [in CanonBDDs.canonicite.Finite_sets]
incl_st_add_x [in CanonBDDs.canonicite.Finite_sets]
incl_add_x [in CanonBDDs.canonicite.Finite_sets]
incl_add [in CanonBDDs.canonicite.Finite_sets]
incl_Q_add [in CanonBDDs.canonicite.Finite_sets]
incl_empty [in CanonBDDs.canonicite.Finite_sets]
incl_allV [in CanonBDDs.canonicite.Finite_sets]
incl_trans [in CanonBDDs.canonicite.Finite_sets]
incl_refl [in CanonBDDs.canonicite.Finite_sets]
incl_nil_eq [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Induction1 [in CanonBDDs.rauzy.algorithme1.Inductions]
Induction1' [in CanonBDDs.rauzy.algorithme1.Inductions]
Induction2 [in CanonBDDs.rauzy.algorithme1.Inductions]
ind1_ind2 [in CanonBDDs.rauzy.algorithme1.Inductions]
Inf_trans [in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
Inf_refl [in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
inh_card_gt_O [in CanonBDDs.canonicite.Finite_sets]
inter_intro [in CanonBDDs.canonicite.Finite_sets]
inter_incl_r [in CanonBDDs.canonicite.Finite_sets]
inter_incl_l [in CanonBDDs.canonicite.Finite_sets]
inv_greatest_R [in CanonBDDs.canonicite.Finite_sets]
inv_greatest_In [in CanonBDDs.canonicite.Finite_sets]
inv_inh_addQx [in CanonBDDs.canonicite.Finite_sets]
inv_dec_on [in CanonBDDs.canonicite.Finite_sets]
Inv_Assignment_of_false [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Inv_Assignment_of_true [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
inv_notImplicant [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
inv_Implicant [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
inv_BDT_eq_node [in CanonBDDs.canonicite.BDTs]
In_not_In_sym [in CanonBDDs.canonicite.Finite_sets]
In_not_In [in CanonBDDs.canonicite.Finite_sets]
in_add_x [in CanonBDDs.canonicite.Finite_sets]
in_allV [in CanonBDDs.canonicite.Finite_sets]
in_empty [in CanonBDDs.canonicite.Finite_sets]
in_Q_add [in CanonBDDs.canonicite.Finite_sets]
In_list_dec [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
I_out_of_Sub_ip [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
I_of_cons_ip [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
J
jofp_jofsub_ip [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]L
La_4bis [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]Lb_4bis [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Lc_4bis [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
LC2_C_fac1 [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
LC2_S_fac1 [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Ld_4bis [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Le_4bis [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
le_Max [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
le_dec [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
le_ne_gt [in CanonBDDs.canonicite.Prelude1]
le_nSm_le_nm_or_eq [in CanonBDDs.canonicite.Prelude1]
le_dec_0 [in CanonBDDs.canonicite.Prelude1]
le_split [in CanonBDDs.canonicite.Complete_induction]
le_Var_total_order [in CanonBDDs.canonicite.Vars]
le_or_gt_Var [in CanonBDDs.canonicite.Vars]
Lower_well_founded [in CanonBDDs.rauzy.algorithme1.Inductions]
LP2 [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
lt_gt [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
LT1 [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
L_Dep_Var2 [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
L_Dep_Var1 [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
L_Assign3 [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
L_Assign2 [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
L_Assign1 [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
L1 [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
L1 [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
L10 [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
L11 [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
L12 [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
L13 [in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
L14 [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
L14bis [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
L15 [in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
L2 [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
L4 [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
L4bis [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
L40 [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
L5 [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
L5bis [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
L8 [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
L80 [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
L9 [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
M
Max_mon_middle [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]Max_mon_right [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Max_mon_left [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Max_sym [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Max_le [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Measure_decrease [in CanonBDDs.rauzy.algorithme1.BDTs]
Mon_node_Mon_sons [in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
Mon_Frestr_Mon [in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
Morgan_and_not [in CanonBDDs.canonicite.Prelude0]
Morgan_or [in CanonBDDs.canonicite.Prelude0]
N
nat_wf_ind [in CanonBDDs.canonicite.Complete_induction]neq_right_neq_BDTs [in CanonBDDs.rauzy.algorithme1.BDTs]
neq_left_neq_BDTs [in CanonBDDs.rauzy.algorithme1.BDTs]
neq_vars_neq_BDTs [in CanonBDDs.rauzy.algorithme1.BDTs]
neq_Node_Zero [in CanonBDDs.rauzy.algorithme1.BDTs]
neq_Node_One [in CanonBDDs.rauzy.algorithme1.BDTs]
neq_One_Zero [in CanonBDDs.rauzy.algorithme1.BDTs]
neq_Zero_One [in CanonBDDs.rauzy.algorithme1.BDTs]
ne_Fone_Fzero [in CanonBDDs.canonicite.BDTs]
ne_Fzero_Fone [in CanonBDDs.canonicite.BDTs]
ne_node_one [in CanonBDDs.canonicite.BDTs]
ne_node_zero [in CanonBDDs.canonicite.BDTs]
ne_one_node [in CanonBDDs.canonicite.BDTs]
ne_one_zero [in CanonBDDs.canonicite.BDTs]
ne_zero_node [in CanonBDDs.canonicite.BDTs]
ne_zero_one [in CanonBDDs.canonicite.BDTs]
Nil_only_prime_of_TRUE [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Nil_prime_of_TRUE [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Nil_divides_all [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Nil_or_not_Nil [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Nil_or_cons [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
nil_included_all [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Node_W_Node_i2_gt_i1 [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Node_W_Node_i1_eq_i2 [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Node_W_Node_i1_eq_i2_neq [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Node_W_Node_i1_eq_i2_eq [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Node_W_Node_i1_gt_i2 [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Node_W_Node_i1_gt_i2_neq [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Node_W_Node_i1_gt_i2_eq [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
notall_existnot_singleton [in CanonBDDs.canonicite.Finite_sets]
notall_addQx_notall_Q [in CanonBDDs.canonicite.Finite_sets]
notP_notinterPQ [in CanonBDDs.canonicite.Finite_sets]
notQ_notinterPQ [in CanonBDDs.canonicite.Finite_sets]
not_All_Exist_not [in CanonBDDs.canonicite.Finite_sets]
not_Exist_All_not [in CanonBDDs.canonicite.Finite_sets]
not_In_soustr_eq [in CanonBDDs.canonicite.Finite_sets]
not_In_soustr [in CanonBDDs.canonicite.Finite_sets]
Not_of_cons_ip [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
not_all_exist_not [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Not_BDT [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
No_prime_FALSE [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
No_solution_Zero [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
No_implicant_FALSE [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
no_Dep_Var_Cstk [in CanonBDDs.canonicite.Boolean_functions]
O
Of_sub_pi_of_p [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]Of_cons_ip_of_p [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Of_p_of_cons_ip [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Of_path_dec [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
One_W_Node [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
onQ_not_All_Exist_not [in CanonBDDs.canonicite.Finite_sets]
Op2_BDT_overloaded [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Ordered_node_ordered_restr [in CanonBDDs.rauzy.algorithme1.BDTs]
ordered_node_ordered_sons [in CanonBDDs.rauzy.algorithme1.BDTs]
ordered_node_a_son_neq_zero [in CanonBDDs.rauzy.algorithme1.BDTs]
ordered_node_neq_sons [in CanonBDDs.rauzy.algorithme1.BDTs]
Ordered_p_ordered_sub_pi [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Ordered_divisor_of_cons_ip [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Ordered_paths_eq [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Ordered_cons_ordered_tail [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Ordering_surj [in CanonBDDs.canonicite.Vars]
Order_S [in CanonBDDs.canonicite.Vars]
Order_gt_O [in CanonBDDs.canonicite.Vars]
Order_le_n [in CanonBDDs.canonicite.Vars]
Or_BDT [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Or_BDT_overloaded [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Or_BDT_b1_One [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Or_BDT_b1_Zero [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Or_BDT_One_b2 [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Or_BDT_Zero_b2 [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Outof_p_outof_sub_ip [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
P
Prime_exists [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]Prime_h_prime_node [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Prime_l_prime_node [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Prime_h_cons_ip_ordered [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Prime_ordered [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Prime_implicant [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Pth_ord9 [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Pth_ord8 [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
P_dec_AllP_dec [in CanonBDDs.canonicite.Finite_sets]
P_dec_on_Q_AllP_dec_on_Q [in CanonBDDs.canonicite.Finite_sets]
P_union_empty [in CanonBDDs.canonicite.Finite_sets]
p_inv_OBDT_neq [in CanonBDDs.rauzy.algorithme1.BDTs]
p_inv_OBDT_order [in CanonBDDs.rauzy.algorithme1.BDTs]
p_inv_OBDT_dim [in CanonBDDs.rauzy.algorithme1.BDTs]
p_inv_Solution [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
p_inv_Ordered [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
P_notnotP [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
p_inv_OBDT_bh [in CanonBDDs.canonicite.BDTs]
p_inv_OBDT_bl [in CanonBDDs.canonicite.BDTs]
p_inv_OBDT_eq [in CanonBDDs.canonicite.BDTs]
p_inv_OBDT_order [in CanonBDDs.canonicite.BDTs]
p_inv_BDT_eq [in CanonBDDs.canonicite.BDTs]
p_dim_inv [in CanonBDDs.canonicite.BDTs]
Q
QinterS_addQxinterS [in CanonBDDs.canonicite.Finite_sets]R
Restr_le_n_Fcst [in CanonBDDs.canonicite.Boolean_functions]Restr_le_k_Restr_le_Sk [in CanonBDDs.canonicite.Boolean_functions]
Restr_xi_Restr_xj [in CanonBDDs.canonicite.Boolean_functions]
Restr_xi_Restr_xi [in CanonBDDs.canonicite.Boolean_functions]
Restr_node_Restr_high [in CanonBDDs.canonicite.BDTs]
Restr_node_Restr_low [in CanonBDDs.canonicite.BDTs]
Restr_Fcst [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Result_Ordered [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
S
same_order_eq_Var [in CanonBDDs.canonicite.Vars]set_eq_trans [in CanonBDDs.canonicite.Finite_sets]
set_eq_sym [in CanonBDDs.canonicite.Finite_sets]
set_eq_refl [in CanonBDDs.canonicite.Finite_sets]
set_eq_inv [in CanonBDDs.canonicite.Finite_sets]
Shannon_expansion [in CanonBDDs.rauzy.algorithme1.BDTs]
Shtree_Not [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Shtree_Or [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Shtree_And [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Shtree_Var [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Shtree_Fa [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Shtree_Tr [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Sh_exp_dim [in CanonBDDs.rauzy.algorithme1.BDTs]
singlx [in CanonBDDs.canonicite.Finite_sets]
Solution_OBDT_ordered [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Solution_of_One_is_Nil [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Soundness [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Soundness_left [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Soundness_left_smallest_out [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Soundness_left_smallest_in [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Soundness_left_smallest_order [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Soundness_left_impl [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Soundness_right [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
still_in_soustr [in CanonBDDs.canonicite.Finite_sets]
Sub_of_non_depvar [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
T
Tail_exists_with_dim_head [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]Tail_exists [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Tautology_decidable [in CanonBDDs.rauzy.algorithme1.Canonicity]
TRUE_neq_FALSE [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
TRUE_absorb_OR [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
TRUE_neutral_AND [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
U
union_add [in CanonBDDs.canonicite.Finite_sets]union_sym [in CanonBDDs.canonicite.Finite_sets]
Uniqueness [in CanonBDDs.rauzy.algorithme1.Canonicity]
Uniqueness [in CanonBDDs.canonicite.Canonicity_BDT]
Unique_One [in CanonBDDs.rauzy.algorithme1.Canonicity]
Unique_Zero [in CanonBDDs.rauzy.algorithme1.Canonicity]
Upd_preserves_Inf [in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
Upd_xi_xj [in CanonBDDs.canonicite.Boolean_functions]
Upd_le_O_Id [in CanonBDDs.canonicite.Boolean_functions]
Upd_le_n_Cst [in CanonBDDs.canonicite.Boolean_functions]
V
Vars_prime_le_dim [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]vars_sup_dim_non_dep2 [in CanonBDDs.canonicite.BDTs]
vars_sup_dim_non_dep [in CanonBDDs.canonicite.BDTs]
Var_n_finite [in CanonBDDs.canonicite.Vars]
Var_k_finite [in CanonBDDs.canonicite.Vars]
W
Wf_ind1 [in CanonBDDs.rauzy.algorithme1.Inductions]X
xi_non_dep_Restr_xi [in CanonBDDs.canonicite.Boolean_functions]xi_non_dep_Restr_xi_Id [in CanonBDDs.canonicite.Boolean_functions]
Z
Zero_W_Node [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]Zero_complete [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Constructor Index
A
ANd [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]B
BDT_eq_node [in CanonBDDs.canonicite.BDTs]BDT_eq_1 [in CanonBDDs.canonicite.BDTs]
BDT_eq_0 [in CanonBDDs.canonicite.BDTs]
C
card_add [in CanonBDDs.canonicite.Finite_sets]card_empty [in CanonBDDs.canonicite.Finite_sets]
case_right [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
case_middle [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
case_left [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Cons_ordered [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
D
Def_greatest [in CanonBDDs.canonicite.Finite_sets]Def_dec_on [in CanonBDDs.canonicite.Finite_sets]
Def_dec [in CanonBDDs.canonicite.Finite_sets]
Def_inh [in CanonBDDs.canonicite.Finite_sets]
Def_set_eq [in CanonBDDs.canonicite.Finite_sets]
Def_Implicant [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
Def_cst_fct [in CanonBDDs.canonicite.Boolean_functions]
Def_GreatestDV [in CanonBDDs.canonicite.Boolean_functions]
Def_Assign_eq [in CanonBDDs.canonicite.Boolean_functions]
dim_node [in CanonBDDs.rauzy.algorithme1.BDTs]
dim_one [in CanonBDDs.rauzy.algorithme1.BDTs]
dim_zero [in CanonBDDs.rauzy.algorithme1.BDTs]
dim_node [in CanonBDDs.canonicite.BDTs]
dim_one [in CanonBDDs.canonicite.BDTs]
dim_zero [in CanonBDDs.canonicite.BDTs]
F
Fa [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]finite_add [in CanonBDDs.canonicite.Finite_sets]
finite_empty [in CanonBDDs.canonicite.Finite_sets]
N
Nil_ordered [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]Node [in CanonBDDs.rauzy.algorithme1.BDTs]
node [in CanonBDDs.canonicite.BDTs]
node_exist [in CanonBDDs.rauzy.algorithme1.BDTs]
node_exist [in CanonBDDs.canonicite.BDTs]
Not [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
O
One [in CanonBDDs.rauzy.algorithme1.BDTs]one [in CanonBDDs.canonicite.BDTs]
Or [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
order_node [in CanonBDDs.rauzy.algorithme1.BDTs]
order_1 [in CanonBDDs.rauzy.algorithme1.BDTs]
order_0 [in CanonBDDs.rauzy.algorithme1.BDTs]
order_node [in CanonBDDs.canonicite.BDTs]
order_1 [in CanonBDDs.canonicite.BDTs]
order_0 [in CanonBDDs.canonicite.BDTs]
S
Sol_Right [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]Sol_Left [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Sol_One [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
T
Tr [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]V
Var [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]Var_intro [in CanonBDDs.canonicite.Vars]
Z
Zero [in CanonBDDs.rauzy.algorithme1.BDTs]zero [in CanonBDDs.canonicite.BDTs]
Axiom Index
A
Assign_subst [in CanonBDDs.canonicite.Boolean_functions]C
Classic [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]E
extensionality [in CanonBDDs.canonicite.Finite_sets]Extensionality_Assignments [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
I
Induction1_prop [in CanonBDDs.rauzy.algorithme1.Inductions]N
n [in CanonBDDs.canonicite.Canonicity_BDT]P
Proof_irrelevance [in CanonBDDs.canonicite.Vars]V
V_decidable [in CanonBDDs.canonicite.Finite_sets]Inductive Index
A
Assign_eq [in CanonBDDs.canonicite.Boolean_functions]B
BDT [in CanonBDDs.rauzy.algorithme1.BDTs]BDT [in CanonBDDs.canonicite.BDTs]
BDT_eq [in CanonBDDs.canonicite.BDTs]
Bool_exp [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
C
cardinal [in CanonBDDs.canonicite.Finite_sets]Case3 [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
Constant_fct [in CanonBDDs.canonicite.Boolean_functions]
D
decidable [in CanonBDDs.canonicite.Finite_sets]decidable_on [in CanonBDDs.canonicite.Finite_sets]
dim [in CanonBDDs.rauzy.algorithme1.BDTs]
dimension [in CanonBDDs.canonicite.BDTs]
F
finite [in CanonBDDs.canonicite.Finite_sets]G
greatest [in CanonBDDs.canonicite.Finite_sets]Greatest_Dep_Var [in CanonBDDs.canonicite.Boolean_functions]
I
Implicant [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]inhabited [in CanonBDDs.canonicite.Finite_sets]
N
node_decomposition [in CanonBDDs.rauzy.algorithme1.BDTs]node_decomposition [in CanonBDDs.canonicite.BDTs]
O
OBDT [in CanonBDDs.rauzy.algorithme1.BDTs]OBDT [in CanonBDDs.canonicite.BDTs]
Ordered [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
S
set_eq [in CanonBDDs.canonicite.Finite_sets]Solution [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
V
Var [in CanonBDDs.canonicite.Vars]Section Index
C
Case_recursion [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]D
Decrease_induction1 [in CanonBDDs.rauzy.algorithme1.BDTs]I
Impl_Sons [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]Impl_Node [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Implicants]
Intervals [in CanonBDDs.canonicite.Vars]
N
Node_to_Sons [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]R
Recursion_W.Greater_i2 [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]Recursion_W.Equal_i1_i2 [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W.Greater_i1 [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
Recursion_W [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
S
sets [in CanonBDDs.canonicite.Finite_sets]sets.Add [in CanonBDDs.canonicite.Finite_sets]
sets.Greatest [in CanonBDDs.canonicite.Finite_sets]
Sons_to_Node [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
V
VR [in CanonBDDs.canonicite.Order]Definition Index
A
add [in CanonBDDs.canonicite.Finite_sets]all_ [in CanonBDDs.canonicite.Finite_sets]
AND [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
anti_symetry [in CanonBDDs.canonicite.Finite_sets]
anti_symetry [in CanonBDDs.canonicite.Order]
Assign [in CanonBDDs.canonicite.Boolean_functions]
Assign [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Assignment_of [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Assign_gt [in CanonBDDs.canonicite.Boolean_functions]
Ass_eq [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
B
BF [in CanonBDDs.canonicite.Boolean_functions]BF [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
BF_eq [in CanonBDDs.canonicite.Boolean_functions]
BF_eq [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Boolean [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
C
Choice [in CanonBDDs.rauzy.algorithme1.BDTs]Complete [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Cons [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
Correct [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
Cpl [in CanonBDDs.rauzy.algorithme1.Inductions]
Cst_Ass [in CanonBDDs.canonicite.Boolean_functions]
D
Denote [in CanonBDDs.canonicite.BDTs]Dep_set [in CanonBDDs.canonicite.Boolean_functions]
Dep_Var [in CanonBDDs.canonicite.Boolean_functions]
Dep_Var [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Dim [in CanonBDDs.rauzy.algorithme1.BDTs]
Dimension [in CanonBDDs.canonicite.BDTs]
Divides [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
E
empty [in CanonBDDs.canonicite.Finite_sets]eq_decidable [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]
eq_Var [in CanonBDDs.canonicite.Vars]
F
f [in CanonBDDs.rauzy.algorithme1.Inductions]F [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
FALSE [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Fcst [in CanonBDDs.canonicite.Boolean_functions]
Fcst [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Frestr [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Fun [in CanonBDDs.rauzy.algorithme1.BDTs]
Fun [in CanonBDDs.canonicite.BDTs]
Fun_Bexp [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
G
gt_Var [in CanonBDDs.canonicite.Vars]H
Head [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]I
IF_ [in CanonBDDs.rauzy.algorithme1.Boolean_functions]Im [in CanonBDDs.canonicite.Finite_sets]
In [in CanonBDDs.canonicite.Finite_sets]
incl [in CanonBDDs.canonicite.Finite_sets]
incl_st [in CanonBDDs.canonicite.Finite_sets]
Inf [in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
inter [in CanonBDDs.canonicite.Finite_sets]
inv_OBDT_neq [in CanonBDDs.rauzy.algorithme1.BDTs]
inv_OBDT_order [in CanonBDDs.rauzy.algorithme1.BDTs]
inv_OBDT_dim [in CanonBDDs.rauzy.algorithme1.BDTs]
Inv_Solution [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
inv_Ordered [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
inv_OBDT_bh [in CanonBDDs.canonicite.BDTs]
inv_OBDT_bl [in CanonBDDs.canonicite.BDTs]
inv_OBDT_eq [in CanonBDDs.canonicite.BDTs]
inv_OBDT_Order [in CanonBDDs.canonicite.BDTs]
inv_BDT_eq [in CanonBDDs.canonicite.BDTs]
L
le_Var [in CanonBDDs.canonicite.Vars]Lower [in CanonBDDs.rauzy.algorithme1.Inductions]
lt_hereditary [in CanonBDDs.canonicite.Complete_induction]
M
Max [in CanonBDDs.rauzy.algorithme1.Prelude_BDT]Maxdim [in CanonBDDs.rauzy.algorithme1.BDTs]
Monotonic [in CanonBDDs.rauzy.algorithmes_2_et_3.Monotony]
N
Nil [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]NOT [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
O
Of [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]OR [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
order [in CanonBDDs.canonicite.Finite_sets]
Order [in CanonBDDs.canonicite.Vars]
order [in CanonBDDs.canonicite.Order]
P
Path [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]Prime [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Primes]
Pr1 [in CanonBDDs.rauzy.algorithme1.Inductions]
Pr2 [in CanonBDDs.rauzy.algorithme1.Inductions]
R
R [in CanonBDDs.rauzy.algorithme1.Inductions]reflexivity [in CanonBDDs.canonicite.Finite_sets]
reflexivity [in CanonBDDs.canonicite.Order]
Restr [in CanonBDDs.canonicite.Boolean_functions]
Restr_le [in CanonBDDs.canonicite.Boolean_functions]
Rp [in CanonBDDs.rauzy.algorithme1.Inductions]
S
set [in CanonBDDs.canonicite.Finite_sets]Sh_tree_of [in CanonBDDs.rauzy.algorithme1.Formula_to_BDT]
Sound [in CanonBDDs.rauzy.algorithmes_2_et_3.Primes]
soustr [in CanonBDDs.canonicite.Finite_sets]
Sub [in CanonBDDs.rauzy.algorithmes_2_et_3.Prelude_Paths]
T
Tautology [in CanonBDDs.rauzy.algorithme1.Canonicity]totality [in CanonBDDs.canonicite.Finite_sets]
totality [in CanonBDDs.canonicite.Order]
total_order [in CanonBDDs.canonicite.Finite_sets]
total_order [in CanonBDDs.canonicite.Order]
transitivity [in CanonBDDs.canonicite.Finite_sets]
transitivity [in CanonBDDs.canonicite.Order]
TRUE [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
U
union [in CanonBDDs.canonicite.Finite_sets]Upd [in CanonBDDs.canonicite.Boolean_functions]
Upd [in CanonBDDs.rauzy.algorithme1.Boolean_functions]
Upd_le [in CanonBDDs.canonicite.Boolean_functions]
Upd' [in CanonBDDs.canonicite.Boolean_functions]
V
Varset [in CanonBDDs.canonicite.Vars]Var_le [in CanonBDDs.canonicite.Vars]
W
W_correct [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]W_complete [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
W_sound [in CanonBDDs.rauzy.algorithmes_2_et_3.Operator_W]
| 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 | (741 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 | (1 entry) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (71 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 | (21 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 | (444 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 | (51 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 | (8 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 | (25 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 | (15 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 | (105 entries) |