| 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 | (850 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 | (81 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (56 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (366 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 | (41 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (18 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (115 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (17 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19 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 | (102 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |
Global Index
A
all_subsets_nodup [lemma, in Obs.list_tools]an [projection, in Obs.fan]
andb_prop_iff [lemma, in Obs.decidable_prop]
and_Join [lemma, in Obs.laws]
anticlique [library]
anticlique_choose_clique [lemma, in Obs.anticlique]
anticlique_inf_or_cntrex [lemma, in Obs.anticlique]
anticlique_dec_inf [instance, in Obs.anticlique]
an_spec [projection, in Obs.fan]
app_comm [lemma, in Obs.list_tools]
app_idem [lemma, in Obs.list_tools]
app_eq_length_app [lemma, in Obs.list_tools]
atTop [definition, in Obs.product]
auxiliary [lemma, in Obs.product]
Ax_impl_eq [instance, in Obs.equiv_obs]
axΩ [abbreviation, in Obs.anticlique]
axΩ_sound [lemma, in Obs.anticlique]
B
Boolean [instance, in Obs.decidable_prop]C
choose_clique_aux [lemma, in Obs.product]choose_clique_sat_dec [lemma, in Obs.sem_obs]
choose_clique [definition, in Obs.sem_obs]
clique [record, in Obs.coherence_graph]
cliques_at_most_one_elt [lemma, in Obs.anticlique]
clique_sat_iff_fsat_proj [lemma, in Obs.fin_sem_obs]
cnf_support_incl [lemma, in Obs.product]
cnf_support_proper [instance, in Obs.product]
cnf_support_proper_incl [instance, in Obs.product]
cnf_to_dnf_equiv [lemma, in Obs.product]
cnf_to_dnf_support [lemma, in Obs.product]
cnf_to_dnf [definition, in Obs.product]
cnf_support [definition, in Obs.product]
coh [projection, in Obs.coherence_graph]
coherence_graph [library]
coh_sym [projection, in Obs.coherence_graph]
coh_refl [projection, in Obs.coherence_graph]
coh_ij [constructor, in Obs.product]
coh_i [constructor, in Obs.product]
coh𝒢 [inductive, in Obs.product]
coh𝒢_sym [lemma, in Obs.product]
coh𝒢_refl [lemma, in Obs.product]
coh𝒢_sind [definition, in Obs.product]
coh𝒢_ind [definition, in Obs.product]
combine [section, in Obs.list_tools]
combine_split [lemma, in Obs.list_tools]
combine_app [lemma, in Obs.list_tools]
combine_snd [lemma, in Obs.list_tools]
combine_fst [lemma, in Obs.list_tools]
combine.A [variable, in Obs.list_tools]
combine.B [variable, in Obs.list_tools]
combine.l [variable, in Obs.list_tools]
combine.l1 [variable, in Obs.list_tools]
combine.l2 [variable, in Obs.list_tools]
combine.l3 [variable, in Obs.list_tools]
combine.l4 [variable, in Obs.list_tools]
combine.same_length [variable, in Obs.list_tools]
_ ⊗ _ [notation, in Obs.list_tools]
compat_dec [instance, in Obs.coherence_graph]
compat_are_coh [lemma, in Obs.coherence_graph]
completeness_anticlique_eq [lemma, in Obs.anticlique]
completeness_anticlique [lemma, in Obs.anticlique]
complete_inf__Ω [lemma, in Obs.anticlique]
Conj [definition, in Obs.fan]
conj_interp [definition, in Obs.product]
Conj_spec [lemma, in Obs.fan]
D
decidable [section, in Obs.decidable_prop]DecidableGraph [record, in Obs.coherence_graph]
DecidableProp [record, in Obs.decidable_prop]
DecidableProp [inductive, in Obs.decidable_prop]
DecidableProp_equiv_prop [instance, in Obs.decidable_prop]
DecidableProp_exists_bnd [instance, in Obs.decidable_prop]
DecidableProp_forall_bnd [instance, in Obs.decidable_prop]
DecidableProp_iff [instance, in Obs.decidable_prop]
DecidableProp_impl [instance, in Obs.decidable_prop]
DecidableProp_disj [instance, in Obs.decidable_prop]
DecidableProp_conj [instance, in Obs.decidable_prop]
DecidableProp_neg [instance, in Obs.decidable_prop]
DecidableProp_Eq [instance, in Obs.decidable_prop]
DecidableProp_Equiv [instance, in Obs.list_dec]
DecidableProp_Incl [instance, in Obs.list_dec]
DecidableProp_In [instance, in Obs.list_dec]
decidable_incompatible_with_fcliques [lemma, in Obs.coherence_graph]
decidable_incompatible_f [instance, in Obs.coherence_graph]
decidable_is_coherent [instance, in Obs.coherence_graph]
decidable_incoh [instance, in Obs.coherence_graph]
decidable_graph.decG [variable, in Obs.coherence_graph]
decidable_graph.G [variable, in Obs.coherence_graph]
decidable_graph [section, in Obs.coherence_graph]
decidable_vertex [projection, in Obs.coherence_graph]
decidable_set [record, in Obs.decidable_prop]
decidable_prop [library]
decidable.D [variable, in Obs.decidable_prop]
decidable.X [variable, in Obs.decidable_prop]
decidale_coh [projection, in Obs.coherence_graph]
decomposition [lemma, in Obs.list_dec]
decomp_unambiguous [lemma, in Obs.list_dec]
decomp_unique [lemma, in Obs.list_dec]
dec_prop [projection, in Obs.decidable_prop]
dec_prop [constructor, in Obs.decidable_prop]
dec_option [instance, in Obs.decidable_prop]
dec_sum [instance, in Obs.decidable_prop]
dec_prod [instance, in Obs.decidable_prop]
dec_compat_proj [lemma, in Obs.product]
dec_in_proj [lemma, in Obs.product]
dec_ssmaller_impl_dec_sequiv [lemma, in Obs.sem_obs]
dec_sequiv_impl_dec_ssmaller [lemma, in Obs.sem_obs]
dec_ssmaller_impl_dec_fsat [lemma, in Obs.sem_obs]
dec_fsat_impl_dec_ssmaller [lemma, in Obs.sem_obs]
_ − _ [notation, in Obs.list_dec]
_ ∩ _ [notation, in Obs.list_dec]
_ ⊖ _ [notation, in Obs.list_dec]
_ ∖ _ [notation, in Obs.list_dec]
{{ _ }} [notation, in Obs.list_dec]
dec_list [instance, in Obs.list_dec]
dec_list.dec_A [variable, in Obs.list_dec]
dec_list.A [variable, in Obs.list_dec]
dec_list [section, in Obs.list_dec]
dec_sat [instance, in Obs.anticlique]
dec_inf__Ω [instance, in Obs.anticlique]
decΩ [instance, in Obs.anticlique]
dec𝒢 [instance, in Obs.product]
difference [definition, in Obs.list_dec]
difference_intersect [lemma, in Obs.list_dec]
difference_incl [lemma, in Obs.list_dec]
difference_nil [lemma, in Obs.list_dec]
difference_inter_l [lemma, in Obs.list_dec]
difference_inter_r [lemma, in Obs.list_dec]
difference_app_r [lemma, in Obs.list_dec]
difference_app_l [lemma, in Obs.list_dec]
difference_right_subs [lemma, in Obs.list_dec]
difference_proper_inf [instance, in Obs.list_dec]
difference_proper [instance, in Obs.list_dec]
difference_spec [lemma, in Obs.list_dec]
disj_interp [definition, in Obs.product]
dnf_support_incl [lemma, in Obs.product]
dnf_support_proper [instance, in Obs.product]
dnf_support_proper_incl [instance, in Obs.product]
dnf_to_cnf_equiv [lemma, in Obs.product]
dnf_to_cnf_support [lemma, in Obs.product]
dnf_to_cnf [definition, in Obs.product]
dnf_support [definition, in Obs.product]
E
empt [definition, in Obs.coherence_graph]empt_max [lemma, in Obs.coherence_graph]
empt_spec [lemma, in Obs.coherence_graph]
eo_Meet_impl [lemma, in Obs.laws]
eo_impl_Join [lemma, in Obs.laws]
eo_inf_in_Meet [lemma, in Obs.laws]
eo_inf_in_Join [lemma, in Obs.laws]
eo_top_impl [lemma, in Obs.laws]
eo_contradict [lemma, in Obs.laws]
eo_eq_bot_iff_inf_bot [lemma, in Obs.laws]
eo_eq_top_iff_top_inf [lemma, in Obs.laws]
eo_inf_bot [lemma, in Obs.laws]
eo_inf_top [lemma, in Obs.laws]
eo_impl_distr_left [lemma, in Obs.laws]
eo_distr2 [lemma, in Obs.laws]
eo_distr1 [lemma, in Obs.laws]
eo_curry [lemma, in Obs.laws]
eo_heyting [lemma, in Obs.laws]
eo_inf_o_impl [lemma, in Obs.laws]
eo_impl_mp [lemma, in Obs.laws]
eo_inf_impl_concl [lemma, in Obs.laws]
eo_inf_impl_right_mon [lemma, in Obs.laws]
eo_inf_and_right [lemma, in Obs.laws]
eo_inf_and_left [lemma, in Obs.laws]
eo_inf_or_right [lemma, in Obs.laws]
eo_inf_or_left [lemma, in Obs.laws]
eo_inf_and_r [lemma, in Obs.laws]
eo_inf_and_l [lemma, in Obs.laws]
eo_inf_or_r [lemma, in Obs.laws]
eo_inf_or_l [lemma, in Obs.laws]
eo_inf_o_and [lemma, in Obs.laws]
eo_or_idem [lemma, in Obs.laws]
eo_and_idem [lemma, in Obs.laws]
eo_or_top [lemma, in Obs.laws]
eo_and_bot [lemma, in Obs.laws]
eo_impl_distr [lemma, in Obs.laws]
eo_impl_concl [lemma, in Obs.laws]
eo_impl_premise [lemma, in Obs.laws]
eo_tauto [lemma, in Obs.laws]
eo_abs2 [lemma, in Obs.laws]
eo_abs1 [lemma, in Obs.laws]
eo_or_bot [lemma, in Obs.laws]
eo_or_comm [lemma, in Obs.laws]
eo_or_ass [lemma, in Obs.laws]
eo_and_top [lemma, in Obs.laws]
eo_and_comm [lemma, in Obs.laws]
eo_and_ass [lemma, in Obs.laws]
eo_ax [constructor, in Obs.equiv_obs]
eo_impl [constructor, in Obs.equiv_obs]
eo_and [constructor, in Obs.equiv_obs]
eo_or [constructor, in Obs.equiv_obs]
eo_trans [constructor, in Obs.equiv_obs]
eo_sym [constructor, in Obs.equiv_obs]
eo_re [constructor, in Obs.equiv_obs]
eo_prod_impl [lemma, in Obs.product]
eo_sound [lemma, in Obs.sem_obs]
eo_ax_complete [lemma, in Obs.fan]
eo_inf_dec [lemma, in Obs.fan]
eo_inf_complete [lemma, in Obs.fan]
eo_fan_clique_neg [lemma, in Obs.fan]
eo_Ω_neg [lemma, in Obs.anticlique]
eo_Ω_top' [lemma, in Obs.anticlique]
equal_list_spec [lemma, in Obs.list_dec]
equal_list [definition, in Obs.list_dec]
equivalent [definition, in Obs.list_tools]
equivalentb [definition, in Obs.list_dec]
equivalentb_spec [lemma, in Obs.list_dec]
equivalent_lift_prod_Proper [instance, in Obs.list_tools]
equivalent_flat_map_Proper [instance, in Obs.list_tools]
equivalent_rev_Proper [instance, in Obs.list_tools]
equivalent_cons_Proper [instance, in Obs.list_tools]
equivalent_app_Proper [instance, in Obs.list_tools]
equivalent_Equivalence [instance, in Obs.list_tools]
equiv_obs_equiv [instance, in Obs.equiv_obs]
equiv_Obs_sind [definition, in Obs.equiv_obs]
equiv_Obs_ind [definition, in Obs.equiv_obs]
equiv_Obs [inductive, in Obs.equiv_obs]
equiv_obs [library]
eqX [projection, in Obs.decidable_prop]
eqX_refl [lemma, in Obs.decidable_prop]
eqX_false [lemma, in Obs.decidable_prop]
eqX_correct [lemma, in Obs.decidable_prop]
eqX_eq [projection, in Obs.decidable_prop]
eq_shuffles [lemma, in Obs.list_tools]
eq_fcliques [abbreviation, in Obs.coherence_graph]
eq_obs_inf_obs [lemma, in Obs.laws]
eq_axΩ_sound [lemma, in Obs.anticlique]
eq𝒱 [definition, in Obs.product]
eq𝒱_proj2 [lemma, in Obs.product]
eq𝒱_proj1 [lemma, in Obs.product]
F
FAN [abbreviation, in Obs.fan]fan [library]
FanGraph [record, in Obs.fan]
fan_choose_clique [lemma, in Obs.fan]
FAN_sound [lemma, in Obs.fan]
FAN_Obs [instance, in Obs.fan]
fan_ax_sind [definition, in Obs.fan]
fan_ax_ind [definition, in Obs.fan]
fan_clique_neg [constructor, in Obs.fan]
fan_ax [inductive, in Obs.fan]
fcic [definition, in Obs.coherence_graph]
fcic_None [lemma, in Obs.coherence_graph]
fcic_Some [lemma, in Obs.coherence_graph]
fcliques [definition, in Obs.coherence_graph]
fcliques_coherent [lemma, in Obs.coherence_graph]
fcliques_sat_iff_fsat [lemma, in Obs.fin_sem_obs]
fcmem [definition, in Obs.coherence_graph]
fcmem_coh [lemma, in Obs.coherence_graph]
fc_to_clique_iff [lemma, in Obs.coherence_graph]
fc_to_clique_proper_eq [instance, in Obs.coherence_graph]
fc_to_clique_proper [instance, in Obs.coherence_graph]
fc_to_clique_spec [lemma, in Obs.coherence_graph]
fc_to_clique [definition, in Obs.coherence_graph]
filter_equivalent_Proper [instance, in Obs.list_tools]
filter_incl_Proper [instance, in Obs.list_tools]
filter_nil [lemma, in Obs.list_tools]
filter_NoDup [lemma, in Obs.list_tools]
filter_true [lemma, in Obs.list_tools]
filter_ext [lemma, in Obs.list_tools]
filter_ext_In [lemma, in Obs.list_tools]
filter_map [lemma, in Obs.list_tools]
filter_length_lt [lemma, in Obs.list_tools]
filter_length_eq [lemma, in Obs.list_tools]
filter_length [lemma, in Obs.list_tools]
filter_app [lemma, in Obs.list_tools]
fincompatible [definition, in Obs.coherence_graph]
fincompatible_eq [instance, in Obs.coherence_graph]
fincompatible_inf [instance, in Obs.coherence_graph]
fincompatible_incompatible [lemma, in Obs.coherence_graph]
_ @@ _ [notation, in Obs.coherence_graph]
_ ↯↯ _ [notation, in Obs.coherence_graph]
! [notation, in Obs.coherence_graph]
_ ⊃f _ [notation, in Obs.coherence_graph]
finite_cliques.decG [variable, in Obs.coherence_graph]
finite_cliques.G [variable, in Obs.coherence_graph]
finite_cliques [section, in Obs.coherence_graph]
finSat [instance, in Obs.fin_sem_obs]
finsat [definition, in Obs.fan]
finsat_spec [lemma, in Obs.fan]
fin_sem_obs [library]
fjoins [definition, in Obs.coherence_graph]
fjoins_iff_joins [lemma, in Obs.coherence_graph]
fjoins_proper [instance, in Obs.coherence_graph]
flat_map_Join [lemma, in Obs.laws]
flat_map_Meet [lemma, in Obs.laws]
flip [definition, in Obs.list_tools]
flip [section, in Obs.list_tools]
flip_proj2 [lemma, in Obs.list_tools]
flip_proj1 [lemma, in Obs.list_tools]
flip_app [lemma, in Obs.list_tools]
flip_involutive [lemma, in Obs.list_tools]
flip.A [variable, in Obs.list_tools]
flip.B [variable, in Obs.list_tools]
flip.l [variable, in Obs.list_tools]
flip.m [variable, in Obs.list_tools]
_ ` [notation, in Obs.list_tools]
forallb_ext [lemma, in Obs.list_tools]
forallb_ext_In [lemma, in Obs.list_tools]
forallb_false_exists [lemma, in Obs.list_tools]
forall_existsb [lemma, in Obs.list_tools]
fsat_impl [lemma, in Obs.fin_sem_obs]
fsat_conj [lemma, in Obs.fin_sem_obs]
fsat_disj [lemma, in Obs.fin_sem_obs]
fsat_at [lemma, in Obs.fin_sem_obs]
fsat_bot [lemma, in Obs.fin_sem_obs]
fsat_top [lemma, in Obs.fin_sem_obs]
G
Graph [record, in Obs.coherence_graph]H
HA_A [lemma, in Obs.laws]ha_ax_sind [definition, in Obs.equiv_obs]
ha_ax_ind [definition, in Obs.equiv_obs]
ha_impl_distr [constructor, in Obs.equiv_obs]
ha_impl_concl [constructor, in Obs.equiv_obs]
ha_impl_premise [constructor, in Obs.equiv_obs]
ha_tauto [constructor, in Obs.equiv_obs]
ha_abs2 [constructor, in Obs.equiv_obs]
ha_abs1 [constructor, in Obs.equiv_obs]
ha_or_bot [constructor, in Obs.equiv_obs]
ha_or_comm [constructor, in Obs.equiv_obs]
ha_or_ass [constructor, in Obs.equiv_obs]
ha_and_top [constructor, in Obs.equiv_obs]
ha_and_comm [constructor, in Obs.equiv_obs]
ha_and_ass [constructor, in Obs.equiv_obs]
ha_ax [inductive, in Obs.equiv_obs]
ha_sound [lemma, in Obs.sem_obs]
I
impl_Join [lemma, in Obs.laws]impl_lst_spec [lemma, in Obs.fin_sem_obs]
impl_lst [definition, in Obs.fin_sem_obs]
impl_disj_cliques [lemma, in Obs.fan]
impl_disj [lemma, in Obs.fan]
impl_cliques [lemma, in Obs.fan]
inb [definition, in Obs.list_dec]
inb_dec [lemma, in Obs.list_dec]
inb_false [lemma, in Obs.list_dec]
inb_spec [lemma, in Obs.list_dec]
inclb [definition, in Obs.list_dec]
inclb_correct [lemma, in Obs.list_dec]
incl_cons_disj' [lemma, in Obs.list_tools]
incl_cons_disj [lemma, in Obs.list_tools]
incl_split [lemma, in Obs.list_tools]
incl_app_split [lemma, in Obs.list_tools]
incl_app_or [lemma, in Obs.list_tools]
incl_nil [lemma, in Obs.list_tools]
incl_lift_prod_Proper [instance, in Obs.list_tools]
incl_flat_map_Proper [instance, in Obs.list_tools]
incl_rev_Proper [instance, in Obs.list_tools]
incl_cons_Proper [instance, in Obs.list_tools]
incl_app_Proper [instance, in Obs.list_tools]
incl_PartialOrder [instance, in Obs.list_tools]
incl_PreOrder [instance, in Obs.list_tools]
incl_map [lemma, in Obs.list_tools]
incl_sem_iff_incl_fin_sem [lemma, in Obs.fin_sem_obs]
incoh [definition, in Obs.coherence_graph]
incoh_sym [instance, in Obs.coherence_graph]
incoh_irrefl [instance, in Obs.coherence_graph]
incoh_iff_same_component_and_incoh [lemma, in Obs.product]
incompat [projection, in Obs.coherence_graph]
incompatible [definition, in Obs.coherence_graph]
incompatible_or_joins_f [lemma, in Obs.coherence_graph]
incompatible_eq [instance, in Obs.coherence_graph]
incompatible_inf [instance, in Obs.coherence_graph]
incompatible_incompat [lemma, in Obs.coherence_graph]
incompat_dec [instance, in Obs.coherence_graph]
incompat_are_incoh [lemma, in Obs.coherence_graph]
incompat_None [projection, in Obs.coherence_graph]
incompat_Some [projection, in Obs.coherence_graph]
incompat_project [definition, in Obs.product]
incompat_inject [definition, in Obs.product]
inf_fcliques [abbreviation, in Obs.coherence_graph]
inf_fcliques [abbreviation, in Obs.coherence_graph]
inf_cliques [abbreviation, in Obs.coherence_graph]
inf_clique_compat [lemma, in Obs.coherence_graph]
inf_cliques [abbreviation, in Obs.coherence_graph]
inf_obs_partialorder [instance, in Obs.laws]
inf_obs_preorder [instance, in Obs.laws]
inf_obs [definition, in Obs.equiv_obs]
inf_axΩ_sound [lemma, in Obs.anticlique]
inf__Ω [definition, in Obs.anticlique]
inject [definition, in Obs.product]
inject_i_incompat [lemma, in Obs.product]
inject_i_member [lemma, in Obs.product]
insert [definition, in Obs.list_tools]
insert_spec [lemma, in Obs.list_tools]
insert_map [lemma, in Obs.list_dec]
interect_nil [lemma, in Obs.list_dec]
intersect [definition, in Obs.list_dec]
intersect_incl [lemma, in Obs.list_dec]
intersect_meet_l [lemma, in Obs.list_dec]
intersect_comm [lemma, in Obs.list_dec]
intersect_ass [lemma, in Obs.list_dec]
intersect_app_r [lemma, in Obs.list_dec]
intersect_app_l [lemma, in Obs.list_dec]
intersect_proper [instance, in Obs.list_dec]
intersect_proper_incl [instance, in Obs.list_dec]
intersect_spec [lemma, in Obs.list_dec]
In_shuffles [lemma, in Obs.list_tools]
In_equivalent_Proper [instance, in Obs.list_tools]
In_incl_Proper [instance, in Obs.list_tools]
In_flip [lemma, in Obs.list_tools]
in_concat [lemma, in Obs.list_tools]
in_cons_iff [lemma, in Obs.list_dec]
In_undup [lemma, in Obs.list_dec]
In_dec [lemma, in Obs.list_dec]
irrefl_fincompatible [instance, in Obs.coherence_graph]
irrefl_incompatible [instance, in Obs.coherence_graph]
is_coherent_project_list [lemma, in Obs.coherence_graph]
is_coherent [definition, in Obs.coherence_graph]
Is_true_iff_eq_true [lemma, in Obs.decidable_prop]
Is_true_dec [instance, in Obs.decidable_prop]
Is_true_test [lemma, in Obs.decidable_prop]
J
jleft [constructor, in Obs.equiv_obs]join [inductive, in Obs.equiv_obs]
Join [definition, in Obs.syntax_obs]
joins [definition, in Obs.coherence_graph]
joins_is_meet_f [lemma, in Obs.coherence_graph]
joins_is_meet [lemma, in Obs.coherence_graph]
joins_proper [instance, in Obs.coherence_graph]
Join_map_equiv_pointwise [lemma, in Obs.laws]
Join_equiv [instance, in Obs.laws]
Join_monotone [instance, in Obs.laws]
Join_and_Join [lemma, in Obs.laws]
Join_app [lemma, in Obs.laws]
join_proper_right [instance, in Obs.equiv_obs]
join_proper_left [instance, in Obs.equiv_obs]
join_sind [definition, in Obs.equiv_obs]
join_ind [definition, in Obs.equiv_obs]
join_project' [lemma, in Obs.product]
join_project [lemma, in Obs.product]
join__f [definition, in Obs.fan]
jright [constructor, in Obs.equiv_obs]
L
laws [library]length_app_tail [lemma, in Obs.list_tools]
length_app [lemma, in Obs.list_tools]
length_sum_filter [lemma, in Obs.list_dec]
len_rev_induction [lemma, in Obs.list_tools]
len_induction [lemma, in Obs.list_tools]
Levi [lemma, in Obs.list_tools]
Levi_strict [lemma, in Obs.list_tools]
le_plus_Proper [instance, in Obs.list_tools]
lift_prod_spec [lemma, in Obs.list_tools]
lift_prod [definition, in Obs.list_tools]
lists_of_length_spec [lemma, in Obs.list_tools]
lists_of_length [definition, in Obs.list_tools]
list_tools [library]
list_dec [library]
lt_plus_Proper [instance, in Obs.list_tools]
M
mapNF [definition, in Obs.product]map_eq_equivalent [lemma, in Obs.list_tools]
map_ext_in_iff [lemma, in Obs.list_tools]
map_bij [lemma, in Obs.list_tools]
map_eq_id [lemma, in Obs.list_tools]
map_equivalent_Proper [instance, in Obs.list_tools]
map_incl_Proper [instance, in Obs.list_tools]
map_app_inverse [lemma, in Obs.list_tools]
map_undup_inj [lemma, in Obs.list_dec]
map_undup_id [lemma, in Obs.list_dec]
Meet [definition, in Obs.syntax_obs]
Meet_impl [lemma, in Obs.laws]
Meet_map_equiv_pointwise [lemma, in Obs.laws]
Meet_equiv [instance, in Obs.laws]
Meet_monotone [instance, in Obs.laws]
Meet_or_Meet [lemma, in Obs.laws]
Meet_app [lemma, in Obs.laws]
Meet_not_and_sgl_in [lemma, in Obs.anticlique]
Meet_not_and_sgl_not_in [lemma, in Obs.anticlique]
member [projection, in Obs.coherence_graph]
members_are_coh [projection, in Obs.coherence_graph]
mem_is_sgl [lemma, in Obs.anticlique]
mix [definition, in Obs.list_tools]
mix [section, in Obs.list_tools]
mix_app [lemma, in Obs.list_tools]
mix_snd [lemma, in Obs.list_tools]
mix_fst [lemma, in Obs.list_tools]
mix.A [variable, in Obs.list_tools]
mix.B [variable, in Obs.list_tools]
mix.same_length [variable, in Obs.list_tools]
mix.s1 [variable, in Obs.list_tools]
mix.s2 [variable, in Obs.list_tools]
mix.s3 [variable, in Obs.list_tools]
mix.s4 [variable, in Obs.list_tools]
_ ⋈ _ [notation, in Obs.list_tools]
N
NatNum [instance, in Obs.decidable_prop]nb [abbreviation, in Obs.list_dec]
nb [abbreviation, in Obs.list_dec]
nb_map [lemma, in Obs.list_dec]
nb_cons_eq [lemma, in Obs.list_dec]
nb_cons_neq [lemma, in Obs.list_dec]
nb_inv_nil [lemma, in Obs.list_dec]
nb_not_In [lemma, in Obs.list_dec]
nb_In [lemma, in Obs.list_dec]
nb_nil [lemma, in Obs.list_dec]
nb_count_occ [lemma, in Obs.list_dec]
neg_top'_is_bot [lemma, in Obs.anticlique]
neg_neg_axΩ [lemma, in Obs.anticlique]
NF [definition, in Obs.product]
nf [definition, in Obs.fan]
nf_spec [lemma, in Obs.fan]
nil_or_last [lemma, in Obs.list_tools]
node [constructor, in Obs.product]
NoDupb [definition, in Obs.list_dec]
NoDupb_NoDup [lemma, in Obs.list_dec]
NoDup_shuffles [lemma, in Obs.list_tools]
NoDup_app [lemma, in Obs.list_tools]
NoDup_app_inv [lemma, in Obs.list_tools]
NoDup_remove_3 [lemma, in Obs.list_tools]
NoDup_nb' [lemma, in Obs.list_dec]
NoDup_nb [lemma, in Obs.list_dec]
NoDup_length [lemma, in Obs.list_dec]
NoDup_rev [lemma, in Obs.list_dec]
NoDup_undup_eq [lemma, in Obs.list_dec]
NoDup_undup [lemma, in Obs.list_dec]
normal_form_eq [lemma, in Obs.product]
normal_form_sup [lemma, in Obs.product]
normal_form [definition, in Obs.product]
notations [library]
not_nil_add [lemma, in Obs.list_tools]
not_incompatible_is_joins_f [lemma, in Obs.coherence_graph]
not_incompatible_is_joins [lemma, in Obs.coherence_graph]
O
O [abbreviation, in Obs.equiv_obs]Obs [abbreviation, in Obs.equiv_obs]
observation [inductive, in Obs.syntax_obs]
observation_sind [definition, in Obs.syntax_obs]
observation_rec [definition, in Obs.syntax_obs]
observation_ind [definition, in Obs.syntax_obs]
observation_rect [definition, in Obs.syntax_obs]
obs_Join [lemma, in Obs.laws]
obs_Meet [lemma, in Obs.laws]
obs_meet [lemma, in Obs.laws]
obs_join [lemma, in Obs.laws]
obs_clique_obs [constructor, in Obs.equiv_obs]
obs_clique_impl [constructor, in Obs.equiv_obs]
obs_ax_sind [definition, in Obs.equiv_obs]
obs_ax_ind [definition, in Obs.equiv_obs]
obs_incoh [constructor, in Obs.equiv_obs]
obs_ax [inductive, in Obs.equiv_obs]
Obs_sound [lemma, in Obs.sem_obs]
Obs__Ω [definition, in Obs.anticlique]
Obs' [abbreviation, in Obs.equiv_obs]
obs'_ax_sind [definition, in Obs.equiv_obs]
obs'_ax_ind [definition, in Obs.equiv_obs]
obs'_ax [inductive, in Obs.equiv_obs]
Obs'_sound [lemma, in Obs.sem_obs]
obs𝖦_to_𝒯_proper_inf [instance, in Obs.product]
obs𝖦_to_𝒯_proper [instance, in Obs.product]
obs𝖦_to_𝒯_sat [lemma, in Obs.product]
obs𝖦_to_𝒯 [definition, in Obs.product]
orb_prop_iff [lemma, in Obs.decidable_prop]
or_Meet [lemma, in Obs.laws]
o_impl_inf [instance, in Obs.laws]
o_and_inf [instance, in Obs.laws]
o_or_inf [instance, in Obs.laws]
o_impl_equiv [instance, in Obs.equiv_obs]
o_or_equiv [instance, in Obs.equiv_obs]
o_and_equiv [instance, in Obs.equiv_obs]
o_impl [constructor, in Obs.syntax_obs]
o_and [constructor, in Obs.syntax_obs]
o_or [constructor, in Obs.syntax_obs]
o_obs [constructor, in Obs.syntax_obs]
o_false [constructor, in Obs.syntax_obs]
o_true [constructor, in Obs.syntax_obs]
P
pad [definition, in Obs.list_tools]pad_contents [lemma, in Obs.list_tools]
pairs [definition, in Obs.list_tools]
pairs_spec [lemma, in Obs.list_tools]
PartialOrder_subrelation [instance, in Obs.notations]
prj1 [abbreviation, in Obs.list_tools]
prj2 [abbreviation, in Obs.list_tools]
product [library]
product_choose_clique [lemma, in Obs.product]
product_sat_dec [instance, in Obs.product]
prod_ax_sind [definition, in Obs.product]
prod_ax_ind [definition, in Obs.product]
prod_impl [constructor, in Obs.product]
prod_idx [constructor, in Obs.product]
prod_ax [inductive, in Obs.product]
project [definition, in Obs.coherence_graph]
project [definition, in Obs.product]
project_proper_inf [instance, in Obs.coherence_graph]
project_proper [instance, in Obs.coherence_graph]
project_project [lemma, in Obs.coherence_graph]
project_max [lemma, in Obs.coherence_graph]
project_larger [lemma, in Obs.coherence_graph]
project_incl [lemma, in Obs.coherence_graph]
project_spec [lemma, in Obs.coherence_graph]
project_proof [lemma, in Obs.coherence_graph]
project_list [definition, in Obs.coherence_graph]
project_inject [lemma, in Obs.product]
project_spec [lemma, in Obs.product]
proj_length [lemma, in Obs.list_tools]
R
rev_equivalent [lemma, in Obs.list_tools]rev_induction [lemma, in Obs.list_tools]
rm [definition, in Obs.list_dec]
rmfst [definition, in Obs.list_dec]
rmfst_flip [lemma, in Obs.list_dec]
rmfst_app_dec [lemma, in Obs.list_dec]
rmfst_comm [lemma, in Obs.list_dec]
rmfst_decr [lemma, in Obs.list_dec]
rmfst_in [lemma, in Obs.list_dec]
rmfst_notin [lemma, in Obs.list_dec]
rm_notin [lemma, in Obs.list_dec]
rm_incl_Proper [instance, in Obs.list_dec]
rm_equivalent_Proper [instance, in Obs.list_dec]
rm_equiv [lemma, in Obs.list_dec]
rm_In [lemma, in Obs.list_dec]
S
s [section, in Obs.coherence_graph]s [section, in Obs.laws]
s [section, in Obs.equiv_obs]
s [section, in Obs.fin_sem_obs]
s [section, in Obs.product]
s [section, in Obs.sem_obs]
s [section, in Obs.fan]
s [section, in Obs.anticlique]
satClique [instance, in Obs.coherence_graph]
Satisfaction [record, in Obs.notations]
Satisfaction [inductive, in Obs.notations]
satisfies [projection, in Obs.notations]
satisfies [constructor, in Obs.notations]
satisfies_Meet [lemma, in Obs.sem_obs]
satisfies_Join [lemma, in Obs.sem_obs]
satisfies_inf [instance, in Obs.sem_obs]
satisfies_inf [instance, in Obs.notations]
satisfies_proper [instance, in Obs.notations]
satObs [instance, in Obs.sem_obs]
satObs_proper [instance, in Obs.sem_obs]
sat_impl [lemma, in Obs.sem_obs]
sat_conj [lemma, in Obs.sem_obs]
sat_disj [lemma, in Obs.sem_obs]
sat_at [lemma, in Obs.sem_obs]
sat_bot [lemma, in Obs.sem_obs]
sat_top [lemma, in Obs.sem_obs]
sat_iff_inf_finsat [lemma, in Obs.fan]
sat__Ω [instance, in Obs.anticlique]
SemEquiv [section, in Obs.notations]
SemEquiv.A [variable, in Obs.notations]
SemEquiv.B [variable, in Obs.notations]
SemEquiv.sat [variable, in Obs.notations]
_ ≲ _ [notation, in Obs.notations]
_ ≃ _ [notation, in Obs.notations]
sem_bij_to_Obs__Ω [lemma, in Obs.anticlique]
sem_obs [library]
sequiv [definition, in Obs.notations]
sequiv_Equiv [instance, in Obs.notations]
sgl [abbreviation, in Obs.coherence_graph]
sgl [abbreviation, in Obs.coherence_graph]
sglf_proof [lemma, in Obs.coherence_graph]
sgl_spec [lemma, in Obs.coherence_graph]
sgl__f [definition, in Obs.coherence_graph]
shuffle [section, in Obs.list_tools]
shuffles [definition, in Obs.list_tools]
shuffles_length [lemma, in Obs.list_tools]
shuffles_nodup [lemma, in Obs.list_tools]
shuffles_equiv [lemma, in Obs.list_tools]
shuffles_map [lemma, in Obs.list_dec]
shuffles_spec [lemma, in Obs.list_dec]
shuffle.A [variable, in Obs.list_tools]
singleton_is_coherent [lemma, in Obs.coherence_graph]
size [projection, in Obs.notations]
Size [record, in Obs.notations]
size [constructor, in Obs.notations]
Size [inductive, in Obs.notations]
SizeApp [lemma, in Obs.list_tools]
SizeCons [lemma, in Obs.list_tools]
SizeLength [lemma, in Obs.list_tools]
SizeList [instance, in Obs.list_tools]
SizeMap [lemma, in Obs.list_tools]
SizeNil [lemma, in Obs.list_tools]
sound_τ_sat__Ω [lemma, in Obs.anticlique]
split_word [lemma, in Obs.list_tools]
split_fst [lemma, in Obs.list_tools]
split_snd [lemma, in Obs.list_tools]
split_app_unambiguous [lemma, in Obs.list_dec]
ssmaller [definition, in Obs.notations]
ssmaller_PartialOrder [instance, in Obs.notations]
ssmaller_PreOrder [instance, in Obs.notations]
subsets [definition, in Obs.list_tools]
subsets_NoDup [lemma, in Obs.list_tools]
subsets_spec [lemma, in Obs.list_tools]
subsets_In [lemma, in Obs.list_tools]
sum [definition, in Obs.list_tools]
sum_filter [lemma, in Obs.list_tools]
sum_lt [lemma, in Obs.list_tools]
sum_le [lemma, in Obs.list_tools]
sum_zero_in [lemma, in Obs.list_tools]
sum_add_distr [lemma, in Obs.list_tools]
sum_add [lemma, in Obs.list_tools]
sum_ext_In [lemma, in Obs.list_tools]
sum_ext [lemma, in Obs.list_tools]
sum_incr [lemma, in Obs.list_tools]
sum_eq_ND [lemma, in Obs.list_tools]
sum_incl_ND [lemma, in Obs.list_tools]
sum_app [lemma, in Obs.list_tools]
sum_incr_0_right [lemma, in Obs.list_dec]
sum_incr_0_left [lemma, in Obs.list_dec]
sup [definition, in Obs.product]
support [definition, in Obs.fin_sem_obs]
support_dominates_sem [lemma, in Obs.fin_sem_obs]
sym_fincompatible [instance, in Obs.coherence_graph]
sym_incompatible [instance, in Obs.coherence_graph]
syntax_obs [library]
s.A [variable, in Obs.laws]
s.a__o [variable, in Obs.anticlique]
s.choose_clique_𝖦 [variable, in Obs.product]
s.decG [variable, in Obs.laws]
s.decG [variable, in Obs.equiv_obs]
s.decG [variable, in Obs.fin_sem_obs]
s.decG [variable, in Obs.sem_obs]
s.decG [variable, in Obs.fan]
s.decIdx [variable, in Obs.product]
s.decV [variable, in Obs.anticlique]
s.dec𝖦 [variable, in Obs.product]
s.fanG [variable, in Obs.fin_sem_obs]
s.FanG [variable, in Obs.fan]
s.G [variable, in Obs.coherence_graph]
s.G [variable, in Obs.laws]
s.G [variable, in Obs.equiv_obs]
s.G [variable, in Obs.fin_sem_obs]
s.G [variable, in Obs.sem_obs]
s.G [variable, in Obs.fan]
s.Idx [variable, in Obs.product]
s.infiniteV [variable, in Obs.anticlique]
s.V [variable, in Obs.anticlique]
_ ↯ _ [notation, in Obs.coherence_graph]
_ ⊃ _ [notation, in Obs.coherence_graph]
_ ∝ _ [notation, in Obs.coherence_graph]
_ ⋊ _ [notation, in Obs.coherence_graph]
_ ⌣ _ [notation, in Obs.coherence_graph]
_ ⁐ _ [notation, in Obs.coherence_graph]
_ =obs' _ [notation, in Obs.equiv_obs]
_ =obs _ [notation, in Obs.equiv_obs]
_ =ha _ [notation, in Obs.equiv_obs]
_ (+) _ [notation, in Obs.equiv_obs]
_ ⊢ _ ≦ _ [notation, in Obs.equiv_obs]
_ ⊢ _ ≡ _ [notation, in Obs.equiv_obs]
_ =𝒜 _ [notation, in Obs.product]
_ .{ _ } [notation, in Obs.product]
_ ⇂ _ [notation, in Obs.product]
_ @ _ [notation, in Obs.product]
_ @' _ [notation, in Obs.product]
_ =fan _ [notation, in Obs.fan]
_ =Ω _ [notation, in Obs.anticlique]
A⁺ [notation, in Obs.laws]
⊤' [notation, in Obs.anticlique]
⎣ _ ⎦ [notation, in Obs.fin_sem_obs]
s.𝖠 [variable, in Obs.product]
s.𝖠_complete [variable, in Obs.product]
s.𝖦 [variable, in Obs.product]
T
termVect [definition, in Obs.product]test [definition, in Obs.decidable_prop]
test_spec [lemma, in Obs.decidable_prop]
test_Is_true [lemma, in Obs.decidable_prop]
test_reflect [lemma, in Obs.decidable_prop]
top'_or_neg [lemma, in Obs.anticlique]
top'_not_a [lemma, in Obs.anticlique]
top'_a [lemma, in Obs.anticlique]
to_Obs__Ω [definition, in Obs.anticlique]
U
undup [definition, in Obs.list_dec]undup_equivalent_Proper [instance, in Obs.list_dec]
undup_incl_Proper [instance, in Obs.list_dec]
undup_equivalent [lemma, in Obs.list_dec]
undup_length [lemma, in Obs.list_dec]
Unnamed_thm [definition, in Obs.decidable_prop]
V
V [abbreviation, in Obs.product]var_clique [lemma, in Obs.laws]
vertex [projection, in Obs.coherence_graph]
V' [definition, in Obs.anticlique]
W
weak_excluded_middle [lemma, in Obs.anticlique]X
X_dec [lemma, in Obs.decidable_prop]other
_ ≈ _ [notation, in Obs.list_tools]_ ` [notation, in Obs.list_tools]
_ ⋈ _ [notation, in Obs.list_tools]
_ ⊗ _ [notation, in Obs.list_tools]
_ :> _ [notation, in Obs.list_tools]
_ ∈ _ [notation, in Obs.list_tools]
_ ⊆ _ [notation, in Obs.list_tools]
_ ⊃f _ [notation, in Obs.coherence_graph]
_ ↯↯ _ [notation, in Obs.coherence_graph]
_ @@ _ [notation, in Obs.coherence_graph]
_ ⊃ _ [notation, in Obs.coherence_graph]
_ ↯ _ [notation, in Obs.coherence_graph]
_ ∝ _ [notation, in Obs.coherence_graph]
_ ⋊ _ [notation, in Obs.coherence_graph]
_ ⌣ _ [notation, in Obs.coherence_graph]
_ ⁐ _ [notation, in Obs.coherence_graph]
_ =?= _ [notation, in Obs.decidable_prop]
_ =obs' _ [notation, in Obs.equiv_obs]
_ =obs _ [notation, in Obs.equiv_obs]
_ =ha _ [notation, in Obs.equiv_obs]
_ (+) _ [notation, in Obs.equiv_obs]
_ ⊢ _ ≦ _ [notation, in Obs.equiv_obs]
_ ⊢ _ ≡ _ [notation, in Obs.equiv_obs]
_ ⊨ _ [notation, in Obs.sem_obs]
_ − _ [notation, in Obs.list_dec]
_ ∩ _ [notation, in Obs.list_dec]
_ ⊖ _ [notation, in Obs.list_dec]
_ ∖ _ [notation, in Obs.list_dec]
_ → _ [notation, in Obs.syntax_obs]
_ ⟑ _ [notation, in Obs.syntax_obs]
_ ⟇ _ [notation, in Obs.syntax_obs]
_ ≃ _ [notation, in Obs.notations]
_ ≲ _ [notation, in Obs.notations]
_ ⊨ _ [notation, in Obs.notations]
_ ⊕ _ [notation, in Obs.notations]
_ ∘ _ [notation, in Obs.notations]
! [notation, in Obs.coherence_graph]
$ _ [notation, in Obs.notations]
{{ _ }} [notation, in Obs.list_dec]
⊤o [notation, in Obs.syntax_obs]
⊥o [notation, in Obs.syntax_obs]
⋀ [notation, in Obs.syntax_obs]
⋁ [notation, in Obs.syntax_obs]
⎢ _ ⎥ [notation, in Obs.notations]
⦑ _ ⦒ [notation, in Obs.syntax_obs]
Ω [instance, in Obs.anticlique]
Ω_ax_sind [definition, in Obs.anticlique]
Ω_ax_ind [definition, in Obs.anticlique]
Ω_neg [constructor, in Obs.anticlique]
Ω_top' [constructor, in Obs.anticlique]
Ω_ax [inductive, in Obs.anticlique]
ζ [definition, in Obs.anticlique]
ζ_ξ [lemma, in Obs.anticlique]
ζ_empt [lemma, in Obs.anticlique]
ζ_sgl [lemma, in Obs.anticlique]
ζ_None [lemma, in Obs.anticlique]
ζ_Some [lemma, in Obs.anticlique]
ξ [definition, in Obs.anticlique]
ξ_to_Obs__Ω [lemma, in Obs.anticlique]
ξ_ζ [lemma, in Obs.anticlique]
π [definition, in Obs.syntax_obs]
π_proper [instance, in Obs.laws]
π_spec [lemma, in Obs.sem_obs]
τ [definition, in Obs.anticlique]
τ_to_Obs__Ω [lemma, in Obs.anticlique]
τ_impl__Ω [lemma, in Obs.anticlique]
τ_neg__Ω [lemma, in Obs.anticlique]
τ_meet__Ω [lemma, in Obs.anticlique]
τ_join__Ω [lemma, in Obs.anticlique]
τ_proper_inf__Ω [instance, in Obs.anticlique]
τ_ξ [lemma, in Obs.anticlique]
τ_ζ [lemma, in Obs.anticlique]
𝒜 [abbreviation, in Obs.product]
𝒜_complete [lemma, in Obs.product]
𝒜_sound [lemma, in Obs.product]
𝒢 [instance, in Obs.product]
𝒯 [definition, in Obs.product]
𝒱 [inductive, in Obs.product]
𝒱_sind [definition, in Obs.product]
𝒱_rec [definition, in Obs.product]
𝒱_ind [definition, in Obs.product]
𝒱_rect [definition, in Obs.product]
𝖠_complete_inf [lemma, in Obs.product]
𝖳 [abbreviation, in Obs.product]
Notation Index
C
_ ⊗ _ [in Obs.list_tools]D
_ − _ [in Obs.list_dec]_ ∩ _ [in Obs.list_dec]
_ ⊖ _ [in Obs.list_dec]
_ ∖ _ [in Obs.list_dec]
{{ _ }} [in Obs.list_dec]
F
_ @@ _ [in Obs.coherence_graph]_ ↯↯ _ [in Obs.coherence_graph]
! [in Obs.coherence_graph]
_ ⊃f _ [in Obs.coherence_graph]
_ ` [in Obs.list_tools]
M
_ ⋈ _ [in Obs.list_tools]S
_ ≲ _ [in Obs.notations]_ ≃ _ [in Obs.notations]
_ ↯ _ [in Obs.coherence_graph]
_ ⊃ _ [in Obs.coherence_graph]
_ ∝ _ [in Obs.coherence_graph]
_ ⋊ _ [in Obs.coherence_graph]
_ ⌣ _ [in Obs.coherence_graph]
_ ⁐ _ [in Obs.coherence_graph]
_ =obs' _ [in Obs.equiv_obs]
_ =obs _ [in Obs.equiv_obs]
_ =ha _ [in Obs.equiv_obs]
_ (+) _ [in Obs.equiv_obs]
_ ⊢ _ ≦ _ [in Obs.equiv_obs]
_ ⊢ _ ≡ _ [in Obs.equiv_obs]
_ =𝒜 _ [in Obs.product]
_ .{ _ } [in Obs.product]
_ ⇂ _ [in Obs.product]
_ @ _ [in Obs.product]
_ @' _ [in Obs.product]
_ =fan _ [in Obs.fan]
_ =Ω _ [in Obs.anticlique]
A⁺ [in Obs.laws]
⊤' [in Obs.anticlique]
⎣ _ ⎦ [in Obs.fin_sem_obs]
other
_ ≈ _ [in Obs.list_tools]_ ` [in Obs.list_tools]
_ ⋈ _ [in Obs.list_tools]
_ ⊗ _ [in Obs.list_tools]
_ :> _ [in Obs.list_tools]
_ ∈ _ [in Obs.list_tools]
_ ⊆ _ [in Obs.list_tools]
_ ⊃f _ [in Obs.coherence_graph]
_ ↯↯ _ [in Obs.coherence_graph]
_ @@ _ [in Obs.coherence_graph]
_ ⊃ _ [in Obs.coherence_graph]
_ ↯ _ [in Obs.coherence_graph]
_ ∝ _ [in Obs.coherence_graph]
_ ⋊ _ [in Obs.coherence_graph]
_ ⌣ _ [in Obs.coherence_graph]
_ ⁐ _ [in Obs.coherence_graph]
_ =?= _ [in Obs.decidable_prop]
_ =obs' _ [in Obs.equiv_obs]
_ =obs _ [in Obs.equiv_obs]
_ =ha _ [in Obs.equiv_obs]
_ (+) _ [in Obs.equiv_obs]
_ ⊢ _ ≦ _ [in Obs.equiv_obs]
_ ⊢ _ ≡ _ [in Obs.equiv_obs]
_ ⊨ _ [in Obs.sem_obs]
_ − _ [in Obs.list_dec]
_ ∩ _ [in Obs.list_dec]
_ ⊖ _ [in Obs.list_dec]
_ ∖ _ [in Obs.list_dec]
_ → _ [in Obs.syntax_obs]
_ ⟑ _ [in Obs.syntax_obs]
_ ⟇ _ [in Obs.syntax_obs]
_ ≃ _ [in Obs.notations]
_ ≲ _ [in Obs.notations]
_ ⊨ _ [in Obs.notations]
_ ⊕ _ [in Obs.notations]
_ ∘ _ [in Obs.notations]
! [in Obs.coherence_graph]
$ _ [in Obs.notations]
{{ _ }} [in Obs.list_dec]
⊤o [in Obs.syntax_obs]
⊥o [in Obs.syntax_obs]
⋀ [in Obs.syntax_obs]
⋁ [in Obs.syntax_obs]
⎢ _ ⎥ [in Obs.notations]
⦑ _ ⦒ [in Obs.syntax_obs]
Variable Index
C
combine.A [in Obs.list_tools]combine.B [in Obs.list_tools]
combine.l [in Obs.list_tools]
combine.l1 [in Obs.list_tools]
combine.l2 [in Obs.list_tools]
combine.l3 [in Obs.list_tools]
combine.l4 [in Obs.list_tools]
combine.same_length [in Obs.list_tools]
D
decidable_graph.decG [in Obs.coherence_graph]decidable_graph.G [in Obs.coherence_graph]
decidable.D [in Obs.decidable_prop]
decidable.X [in Obs.decidable_prop]
dec_list.dec_A [in Obs.list_dec]
dec_list.A [in Obs.list_dec]
F
finite_cliques.decG [in Obs.coherence_graph]finite_cliques.G [in Obs.coherence_graph]
flip.A [in Obs.list_tools]
flip.B [in Obs.list_tools]
flip.l [in Obs.list_tools]
flip.m [in Obs.list_tools]
M
mix.A [in Obs.list_tools]mix.B [in Obs.list_tools]
mix.same_length [in Obs.list_tools]
mix.s1 [in Obs.list_tools]
mix.s2 [in Obs.list_tools]
mix.s3 [in Obs.list_tools]
mix.s4 [in Obs.list_tools]
S
SemEquiv.A [in Obs.notations]SemEquiv.B [in Obs.notations]
SemEquiv.sat [in Obs.notations]
shuffle.A [in Obs.list_tools]
s.A [in Obs.laws]
s.a__o [in Obs.anticlique]
s.choose_clique_𝖦 [in Obs.product]
s.decG [in Obs.laws]
s.decG [in Obs.equiv_obs]
s.decG [in Obs.fin_sem_obs]
s.decG [in Obs.sem_obs]
s.decG [in Obs.fan]
s.decIdx [in Obs.product]
s.decV [in Obs.anticlique]
s.dec𝖦 [in Obs.product]
s.fanG [in Obs.fin_sem_obs]
s.FanG [in Obs.fan]
s.G [in Obs.coherence_graph]
s.G [in Obs.laws]
s.G [in Obs.equiv_obs]
s.G [in Obs.fin_sem_obs]
s.G [in Obs.sem_obs]
s.G [in Obs.fan]
s.Idx [in Obs.product]
s.infiniteV [in Obs.anticlique]
s.V [in Obs.anticlique]
s.𝖠 [in Obs.product]
s.𝖠_complete [in Obs.product]
s.𝖦 [in Obs.product]
Library Index
A
anticliqueC
coherence_graphD
decidable_propE
equiv_obsF
fanfin_sem_obs
L
lawslist_tools
list_dec
N
notationsP
productS
sem_obssyntax_obs
Lemma Index
A
all_subsets_nodup [in Obs.list_tools]andb_prop_iff [in Obs.decidable_prop]
and_Join [in Obs.laws]
anticlique_choose_clique [in Obs.anticlique]
anticlique_inf_or_cntrex [in Obs.anticlique]
app_comm [in Obs.list_tools]
app_idem [in Obs.list_tools]
app_eq_length_app [in Obs.list_tools]
auxiliary [in Obs.product]
axΩ_sound [in Obs.anticlique]
C
choose_clique_aux [in Obs.product]choose_clique_sat_dec [in Obs.sem_obs]
cliques_at_most_one_elt [in Obs.anticlique]
clique_sat_iff_fsat_proj [in Obs.fin_sem_obs]
cnf_support_incl [in Obs.product]
cnf_to_dnf_equiv [in Obs.product]
cnf_to_dnf_support [in Obs.product]
coh𝒢_sym [in Obs.product]
coh𝒢_refl [in Obs.product]
combine_split [in Obs.list_tools]
combine_app [in Obs.list_tools]
combine_snd [in Obs.list_tools]
combine_fst [in Obs.list_tools]
compat_are_coh [in Obs.coherence_graph]
completeness_anticlique_eq [in Obs.anticlique]
completeness_anticlique [in Obs.anticlique]
complete_inf__Ω [in Obs.anticlique]
Conj_spec [in Obs.fan]
D
decidable_incompatible_with_fcliques [in Obs.coherence_graph]decomposition [in Obs.list_dec]
decomp_unambiguous [in Obs.list_dec]
decomp_unique [in Obs.list_dec]
dec_compat_proj [in Obs.product]
dec_in_proj [in Obs.product]
dec_ssmaller_impl_dec_sequiv [in Obs.sem_obs]
dec_sequiv_impl_dec_ssmaller [in Obs.sem_obs]
dec_ssmaller_impl_dec_fsat [in Obs.sem_obs]
dec_fsat_impl_dec_ssmaller [in Obs.sem_obs]
difference_intersect [in Obs.list_dec]
difference_incl [in Obs.list_dec]
difference_nil [in Obs.list_dec]
difference_inter_l [in Obs.list_dec]
difference_inter_r [in Obs.list_dec]
difference_app_r [in Obs.list_dec]
difference_app_l [in Obs.list_dec]
difference_right_subs [in Obs.list_dec]
difference_spec [in Obs.list_dec]
dnf_support_incl [in Obs.product]
dnf_to_cnf_equiv [in Obs.product]
dnf_to_cnf_support [in Obs.product]
E
empt_max [in Obs.coherence_graph]empt_spec [in Obs.coherence_graph]
eo_Meet_impl [in Obs.laws]
eo_impl_Join [in Obs.laws]
eo_inf_in_Meet [in Obs.laws]
eo_inf_in_Join [in Obs.laws]
eo_top_impl [in Obs.laws]
eo_contradict [in Obs.laws]
eo_eq_bot_iff_inf_bot [in Obs.laws]
eo_eq_top_iff_top_inf [in Obs.laws]
eo_inf_bot [in Obs.laws]
eo_inf_top [in Obs.laws]
eo_impl_distr_left [in Obs.laws]
eo_distr2 [in Obs.laws]
eo_distr1 [in Obs.laws]
eo_curry [in Obs.laws]
eo_heyting [in Obs.laws]
eo_inf_o_impl [in Obs.laws]
eo_impl_mp [in Obs.laws]
eo_inf_impl_concl [in Obs.laws]
eo_inf_impl_right_mon [in Obs.laws]
eo_inf_and_right [in Obs.laws]
eo_inf_and_left [in Obs.laws]
eo_inf_or_right [in Obs.laws]
eo_inf_or_left [in Obs.laws]
eo_inf_and_r [in Obs.laws]
eo_inf_and_l [in Obs.laws]
eo_inf_or_r [in Obs.laws]
eo_inf_or_l [in Obs.laws]
eo_inf_o_and [in Obs.laws]
eo_or_idem [in Obs.laws]
eo_and_idem [in Obs.laws]
eo_or_top [in Obs.laws]
eo_and_bot [in Obs.laws]
eo_impl_distr [in Obs.laws]
eo_impl_concl [in Obs.laws]
eo_impl_premise [in Obs.laws]
eo_tauto [in Obs.laws]
eo_abs2 [in Obs.laws]
eo_abs1 [in Obs.laws]
eo_or_bot [in Obs.laws]
eo_or_comm [in Obs.laws]
eo_or_ass [in Obs.laws]
eo_and_top [in Obs.laws]
eo_and_comm [in Obs.laws]
eo_and_ass [in Obs.laws]
eo_prod_impl [in Obs.product]
eo_sound [in Obs.sem_obs]
eo_ax_complete [in Obs.fan]
eo_inf_dec [in Obs.fan]
eo_inf_complete [in Obs.fan]
eo_fan_clique_neg [in Obs.fan]
eo_Ω_neg [in Obs.anticlique]
eo_Ω_top' [in Obs.anticlique]
equal_list_spec [in Obs.list_dec]
equivalentb_spec [in Obs.list_dec]
eqX_refl [in Obs.decidable_prop]
eqX_false [in Obs.decidable_prop]
eqX_correct [in Obs.decidable_prop]
eq_shuffles [in Obs.list_tools]
eq_obs_inf_obs [in Obs.laws]
eq_axΩ_sound [in Obs.anticlique]
eq𝒱_proj2 [in Obs.product]
eq𝒱_proj1 [in Obs.product]
F
fan_choose_clique [in Obs.fan]FAN_sound [in Obs.fan]
fcic_None [in Obs.coherence_graph]
fcic_Some [in Obs.coherence_graph]
fcliques_coherent [in Obs.coherence_graph]
fcliques_sat_iff_fsat [in Obs.fin_sem_obs]
fcmem_coh [in Obs.coherence_graph]
fc_to_clique_iff [in Obs.coherence_graph]
fc_to_clique_spec [in Obs.coherence_graph]
filter_nil [in Obs.list_tools]
filter_NoDup [in Obs.list_tools]
filter_true [in Obs.list_tools]
filter_ext [in Obs.list_tools]
filter_ext_In [in Obs.list_tools]
filter_map [in Obs.list_tools]
filter_length_lt [in Obs.list_tools]
filter_length_eq [in Obs.list_tools]
filter_length [in Obs.list_tools]
filter_app [in Obs.list_tools]
fincompatible_incompatible [in Obs.coherence_graph]
finsat_spec [in Obs.fan]
fjoins_iff_joins [in Obs.coherence_graph]
flat_map_Join [in Obs.laws]
flat_map_Meet [in Obs.laws]
flip_proj2 [in Obs.list_tools]
flip_proj1 [in Obs.list_tools]
flip_app [in Obs.list_tools]
flip_involutive [in Obs.list_tools]
forallb_ext [in Obs.list_tools]
forallb_ext_In [in Obs.list_tools]
forallb_false_exists [in Obs.list_tools]
forall_existsb [in Obs.list_tools]
fsat_impl [in Obs.fin_sem_obs]
fsat_conj [in Obs.fin_sem_obs]
fsat_disj [in Obs.fin_sem_obs]
fsat_at [in Obs.fin_sem_obs]
fsat_bot [in Obs.fin_sem_obs]
fsat_top [in Obs.fin_sem_obs]
H
HA_A [in Obs.laws]ha_sound [in Obs.sem_obs]
I
impl_Join [in Obs.laws]impl_lst_spec [in Obs.fin_sem_obs]
impl_disj_cliques [in Obs.fan]
impl_disj [in Obs.fan]
impl_cliques [in Obs.fan]
inb_dec [in Obs.list_dec]
inb_false [in Obs.list_dec]
inb_spec [in Obs.list_dec]
inclb_correct [in Obs.list_dec]
incl_cons_disj' [in Obs.list_tools]
incl_cons_disj [in Obs.list_tools]
incl_split [in Obs.list_tools]
incl_app_split [in Obs.list_tools]
incl_app_or [in Obs.list_tools]
incl_nil [in Obs.list_tools]
incl_map [in Obs.list_tools]
incl_sem_iff_incl_fin_sem [in Obs.fin_sem_obs]
incoh_iff_same_component_and_incoh [in Obs.product]
incompatible_or_joins_f [in Obs.coherence_graph]
incompatible_incompat [in Obs.coherence_graph]
incompat_are_incoh [in Obs.coherence_graph]
inf_clique_compat [in Obs.coherence_graph]
inf_axΩ_sound [in Obs.anticlique]
inject_i_incompat [in Obs.product]
inject_i_member [in Obs.product]
insert_spec [in Obs.list_tools]
insert_map [in Obs.list_dec]
interect_nil [in Obs.list_dec]
intersect_incl [in Obs.list_dec]
intersect_meet_l [in Obs.list_dec]
intersect_comm [in Obs.list_dec]
intersect_ass [in Obs.list_dec]
intersect_app_r [in Obs.list_dec]
intersect_app_l [in Obs.list_dec]
intersect_spec [in Obs.list_dec]
In_shuffles [in Obs.list_tools]
In_flip [in Obs.list_tools]
in_concat [in Obs.list_tools]
in_cons_iff [in Obs.list_dec]
In_undup [in Obs.list_dec]
In_dec [in Obs.list_dec]
is_coherent_project_list [in Obs.coherence_graph]
Is_true_iff_eq_true [in Obs.decidable_prop]
Is_true_test [in Obs.decidable_prop]
J
joins_is_meet_f [in Obs.coherence_graph]joins_is_meet [in Obs.coherence_graph]
Join_map_equiv_pointwise [in Obs.laws]
Join_and_Join [in Obs.laws]
Join_app [in Obs.laws]
join_project' [in Obs.product]
join_project [in Obs.product]
L
length_app_tail [in Obs.list_tools]length_app [in Obs.list_tools]
length_sum_filter [in Obs.list_dec]
len_rev_induction [in Obs.list_tools]
len_induction [in Obs.list_tools]
Levi [in Obs.list_tools]
Levi_strict [in Obs.list_tools]
lift_prod_spec [in Obs.list_tools]
lists_of_length_spec [in Obs.list_tools]
M
map_eq_equivalent [in Obs.list_tools]map_ext_in_iff [in Obs.list_tools]
map_bij [in Obs.list_tools]
map_eq_id [in Obs.list_tools]
map_app_inverse [in Obs.list_tools]
map_undup_inj [in Obs.list_dec]
map_undup_id [in Obs.list_dec]
Meet_impl [in Obs.laws]
Meet_map_equiv_pointwise [in Obs.laws]
Meet_or_Meet [in Obs.laws]
Meet_app [in Obs.laws]
Meet_not_and_sgl_in [in Obs.anticlique]
Meet_not_and_sgl_not_in [in Obs.anticlique]
mem_is_sgl [in Obs.anticlique]
mix_app [in Obs.list_tools]
mix_snd [in Obs.list_tools]
mix_fst [in Obs.list_tools]
N
nb_map [in Obs.list_dec]nb_cons_eq [in Obs.list_dec]
nb_cons_neq [in Obs.list_dec]
nb_inv_nil [in Obs.list_dec]
nb_not_In [in Obs.list_dec]
nb_In [in Obs.list_dec]
nb_nil [in Obs.list_dec]
nb_count_occ [in Obs.list_dec]
neg_top'_is_bot [in Obs.anticlique]
neg_neg_axΩ [in Obs.anticlique]
nf_spec [in Obs.fan]
nil_or_last [in Obs.list_tools]
NoDupb_NoDup [in Obs.list_dec]
NoDup_shuffles [in Obs.list_tools]
NoDup_app [in Obs.list_tools]
NoDup_app_inv [in Obs.list_tools]
NoDup_remove_3 [in Obs.list_tools]
NoDup_nb' [in Obs.list_dec]
NoDup_nb [in Obs.list_dec]
NoDup_length [in Obs.list_dec]
NoDup_rev [in Obs.list_dec]
NoDup_undup_eq [in Obs.list_dec]
NoDup_undup [in Obs.list_dec]
normal_form_eq [in Obs.product]
normal_form_sup [in Obs.product]
not_nil_add [in Obs.list_tools]
not_incompatible_is_joins_f [in Obs.coherence_graph]
not_incompatible_is_joins [in Obs.coherence_graph]
O
obs_Join [in Obs.laws]obs_Meet [in Obs.laws]
obs_meet [in Obs.laws]
obs_join [in Obs.laws]
Obs_sound [in Obs.sem_obs]
Obs'_sound [in Obs.sem_obs]
obs𝖦_to_𝒯_sat [in Obs.product]
orb_prop_iff [in Obs.decidable_prop]
or_Meet [in Obs.laws]
P
pad_contents [in Obs.list_tools]pairs_spec [in Obs.list_tools]
product_choose_clique [in Obs.product]
project_project [in Obs.coherence_graph]
project_max [in Obs.coherence_graph]
project_larger [in Obs.coherence_graph]
project_incl [in Obs.coherence_graph]
project_spec [in Obs.coherence_graph]
project_proof [in Obs.coherence_graph]
project_inject [in Obs.product]
project_spec [in Obs.product]
proj_length [in Obs.list_tools]
R
rev_equivalent [in Obs.list_tools]rev_induction [in Obs.list_tools]
rmfst_flip [in Obs.list_dec]
rmfst_app_dec [in Obs.list_dec]
rmfst_comm [in Obs.list_dec]
rmfst_decr [in Obs.list_dec]
rmfst_in [in Obs.list_dec]
rmfst_notin [in Obs.list_dec]
rm_notin [in Obs.list_dec]
rm_equiv [in Obs.list_dec]
rm_In [in Obs.list_dec]
S
satisfies_Meet [in Obs.sem_obs]satisfies_Join [in Obs.sem_obs]
sat_impl [in Obs.sem_obs]
sat_conj [in Obs.sem_obs]
sat_disj [in Obs.sem_obs]
sat_at [in Obs.sem_obs]
sat_bot [in Obs.sem_obs]
sat_top [in Obs.sem_obs]
sat_iff_inf_finsat [in Obs.fan]
sem_bij_to_Obs__Ω [in Obs.anticlique]
sglf_proof [in Obs.coherence_graph]
sgl_spec [in Obs.coherence_graph]
shuffles_length [in Obs.list_tools]
shuffles_nodup [in Obs.list_tools]
shuffles_equiv [in Obs.list_tools]
shuffles_map [in Obs.list_dec]
shuffles_spec [in Obs.list_dec]
singleton_is_coherent [in Obs.coherence_graph]
SizeApp [in Obs.list_tools]
SizeCons [in Obs.list_tools]
SizeLength [in Obs.list_tools]
SizeMap [in Obs.list_tools]
SizeNil [in Obs.list_tools]
sound_τ_sat__Ω [in Obs.anticlique]
split_word [in Obs.list_tools]
split_fst [in Obs.list_tools]
split_snd [in Obs.list_tools]
split_app_unambiguous [in Obs.list_dec]
subsets_NoDup [in Obs.list_tools]
subsets_spec [in Obs.list_tools]
subsets_In [in Obs.list_tools]
sum_filter [in Obs.list_tools]
sum_lt [in Obs.list_tools]
sum_le [in Obs.list_tools]
sum_zero_in [in Obs.list_tools]
sum_add_distr [in Obs.list_tools]
sum_add [in Obs.list_tools]
sum_ext_In [in Obs.list_tools]
sum_ext [in Obs.list_tools]
sum_incr [in Obs.list_tools]
sum_eq_ND [in Obs.list_tools]
sum_incl_ND [in Obs.list_tools]
sum_app [in Obs.list_tools]
sum_incr_0_right [in Obs.list_dec]
sum_incr_0_left [in Obs.list_dec]
support_dominates_sem [in Obs.fin_sem_obs]
T
test_spec [in Obs.decidable_prop]test_Is_true [in Obs.decidable_prop]
test_reflect [in Obs.decidable_prop]
top'_or_neg [in Obs.anticlique]
top'_not_a [in Obs.anticlique]
top'_a [in Obs.anticlique]
U
undup_equivalent [in Obs.list_dec]undup_length [in Obs.list_dec]
V
var_clique [in Obs.laws]W
weak_excluded_middle [in Obs.anticlique]X
X_dec [in Obs.decidable_prop]other
ζ_ξ [in Obs.anticlique]ζ_empt [in Obs.anticlique]
ζ_sgl [in Obs.anticlique]
ζ_None [in Obs.anticlique]
ζ_Some [in Obs.anticlique]
ξ_to_Obs__Ω [in Obs.anticlique]
ξ_ζ [in Obs.anticlique]
π_spec [in Obs.sem_obs]
τ_to_Obs__Ω [in Obs.anticlique]
τ_impl__Ω [in Obs.anticlique]
τ_neg__Ω [in Obs.anticlique]
τ_meet__Ω [in Obs.anticlique]
τ_join__Ω [in Obs.anticlique]
τ_ξ [in Obs.anticlique]
τ_ζ [in Obs.anticlique]
𝒜_complete [in Obs.product]
𝒜_sound [in Obs.product]
𝖠_complete_inf [in Obs.product]
Constructor Index
C
coh_ij [in Obs.product]coh_i [in Obs.product]
D
dec_prop [in Obs.decidable_prop]E
eo_ax [in Obs.equiv_obs]eo_impl [in Obs.equiv_obs]
eo_and [in Obs.equiv_obs]
eo_or [in Obs.equiv_obs]
eo_trans [in Obs.equiv_obs]
eo_sym [in Obs.equiv_obs]
eo_re [in Obs.equiv_obs]
F
fan_clique_neg [in Obs.fan]H
ha_impl_distr [in Obs.equiv_obs]ha_impl_concl [in Obs.equiv_obs]
ha_impl_premise [in Obs.equiv_obs]
ha_tauto [in Obs.equiv_obs]
ha_abs2 [in Obs.equiv_obs]
ha_abs1 [in Obs.equiv_obs]
ha_or_bot [in Obs.equiv_obs]
ha_or_comm [in Obs.equiv_obs]
ha_or_ass [in Obs.equiv_obs]
ha_and_top [in Obs.equiv_obs]
ha_and_comm [in Obs.equiv_obs]
ha_and_ass [in Obs.equiv_obs]
J
jleft [in Obs.equiv_obs]jright [in Obs.equiv_obs]
N
node [in Obs.product]O
obs_clique_obs [in Obs.equiv_obs]obs_clique_impl [in Obs.equiv_obs]
obs_incoh [in Obs.equiv_obs]
o_impl [in Obs.syntax_obs]
o_and [in Obs.syntax_obs]
o_or [in Obs.syntax_obs]
o_obs [in Obs.syntax_obs]
o_false [in Obs.syntax_obs]
o_true [in Obs.syntax_obs]
P
prod_impl [in Obs.product]prod_idx [in Obs.product]
S
satisfies [in Obs.notations]size [in Obs.notations]
other
Ω_neg [in Obs.anticlique]Ω_top' [in Obs.anticlique]
Projection Index
A
an [in Obs.fan]an_spec [in Obs.fan]
C
coh [in Obs.coherence_graph]coh_sym [in Obs.coherence_graph]
coh_refl [in Obs.coherence_graph]
D
decidable_vertex [in Obs.coherence_graph]decidale_coh [in Obs.coherence_graph]
dec_prop [in Obs.decidable_prop]
E
eqX [in Obs.decidable_prop]eqX_eq [in Obs.decidable_prop]
I
incompat [in Obs.coherence_graph]incompat_None [in Obs.coherence_graph]
incompat_Some [in Obs.coherence_graph]
M
member [in Obs.coherence_graph]members_are_coh [in Obs.coherence_graph]
S
satisfies [in Obs.notations]size [in Obs.notations]
V
vertex [in Obs.coherence_graph]Inductive Index
C
coh𝒢 [in Obs.product]D
DecidableProp [in Obs.decidable_prop]E
equiv_Obs [in Obs.equiv_obs]F
fan_ax [in Obs.fan]H
ha_ax [in Obs.equiv_obs]J
join [in Obs.equiv_obs]O
observation [in Obs.syntax_obs]obs_ax [in Obs.equiv_obs]
obs'_ax [in Obs.equiv_obs]
P
prod_ax [in Obs.product]S
Satisfaction [in Obs.notations]Size [in Obs.notations]
other
Ω_ax [in Obs.anticlique]𝒱 [in Obs.product]
Instance Index
A
anticlique_dec_inf [in Obs.anticlique]Ax_impl_eq [in Obs.equiv_obs]
B
Boolean [in Obs.decidable_prop]C
cnf_support_proper [in Obs.product]cnf_support_proper_incl [in Obs.product]
compat_dec [in Obs.coherence_graph]
D
DecidableProp_equiv_prop [in Obs.decidable_prop]DecidableProp_exists_bnd [in Obs.decidable_prop]
DecidableProp_forall_bnd [in Obs.decidable_prop]
DecidableProp_iff [in Obs.decidable_prop]
DecidableProp_impl [in Obs.decidable_prop]
DecidableProp_disj [in Obs.decidable_prop]
DecidableProp_conj [in Obs.decidable_prop]
DecidableProp_neg [in Obs.decidable_prop]
DecidableProp_Eq [in Obs.decidable_prop]
DecidableProp_Equiv [in Obs.list_dec]
DecidableProp_Incl [in Obs.list_dec]
DecidableProp_In [in Obs.list_dec]
decidable_incompatible_f [in Obs.coherence_graph]
decidable_is_coherent [in Obs.coherence_graph]
decidable_incoh [in Obs.coherence_graph]
dec_option [in Obs.decidable_prop]
dec_sum [in Obs.decidable_prop]
dec_prod [in Obs.decidable_prop]
dec_list [in Obs.list_dec]
dec_sat [in Obs.anticlique]
dec_inf__Ω [in Obs.anticlique]
decΩ [in Obs.anticlique]
dec𝒢 [in Obs.product]
difference_proper_inf [in Obs.list_dec]
difference_proper [in Obs.list_dec]
dnf_support_proper [in Obs.product]
dnf_support_proper_incl [in Obs.product]
E
equivalent_lift_prod_Proper [in Obs.list_tools]equivalent_flat_map_Proper [in Obs.list_tools]
equivalent_rev_Proper [in Obs.list_tools]
equivalent_cons_Proper [in Obs.list_tools]
equivalent_app_Proper [in Obs.list_tools]
equivalent_Equivalence [in Obs.list_tools]
equiv_obs_equiv [in Obs.equiv_obs]
F
FAN_Obs [in Obs.fan]fc_to_clique_proper_eq [in Obs.coherence_graph]
fc_to_clique_proper [in Obs.coherence_graph]
filter_equivalent_Proper [in Obs.list_tools]
filter_incl_Proper [in Obs.list_tools]
fincompatible_eq [in Obs.coherence_graph]
fincompatible_inf [in Obs.coherence_graph]
finSat [in Obs.fin_sem_obs]
fjoins_proper [in Obs.coherence_graph]
I
incl_lift_prod_Proper [in Obs.list_tools]incl_flat_map_Proper [in Obs.list_tools]
incl_rev_Proper [in Obs.list_tools]
incl_cons_Proper [in Obs.list_tools]
incl_app_Proper [in Obs.list_tools]
incl_PartialOrder [in Obs.list_tools]
incl_PreOrder [in Obs.list_tools]
incoh_sym [in Obs.coherence_graph]
incoh_irrefl [in Obs.coherence_graph]
incompatible_eq [in Obs.coherence_graph]
incompatible_inf [in Obs.coherence_graph]
incompat_dec [in Obs.coherence_graph]
inf_obs_partialorder [in Obs.laws]
inf_obs_preorder [in Obs.laws]
intersect_proper [in Obs.list_dec]
intersect_proper_incl [in Obs.list_dec]
In_equivalent_Proper [in Obs.list_tools]
In_incl_Proper [in Obs.list_tools]
irrefl_fincompatible [in Obs.coherence_graph]
irrefl_incompatible [in Obs.coherence_graph]
Is_true_dec [in Obs.decidable_prop]
J
joins_proper [in Obs.coherence_graph]Join_equiv [in Obs.laws]
Join_monotone [in Obs.laws]
join_proper_right [in Obs.equiv_obs]
join_proper_left [in Obs.equiv_obs]
L
le_plus_Proper [in Obs.list_tools]lt_plus_Proper [in Obs.list_tools]
M
map_equivalent_Proper [in Obs.list_tools]map_incl_Proper [in Obs.list_tools]
Meet_equiv [in Obs.laws]
Meet_monotone [in Obs.laws]
N
NatNum [in Obs.decidable_prop]O
obs𝖦_to_𝒯_proper_inf [in Obs.product]obs𝖦_to_𝒯_proper [in Obs.product]
o_impl_inf [in Obs.laws]
o_and_inf [in Obs.laws]
o_or_inf [in Obs.laws]
o_impl_equiv [in Obs.equiv_obs]
o_or_equiv [in Obs.equiv_obs]
o_and_equiv [in Obs.equiv_obs]
P
PartialOrder_subrelation [in Obs.notations]product_sat_dec [in Obs.product]
project_proper_inf [in Obs.coherence_graph]
project_proper [in Obs.coherence_graph]
R
rm_incl_Proper [in Obs.list_dec]rm_equivalent_Proper [in Obs.list_dec]
S
satClique [in Obs.coherence_graph]satisfies_inf [in Obs.sem_obs]
satisfies_inf [in Obs.notations]
satisfies_proper [in Obs.notations]
satObs [in Obs.sem_obs]
satObs_proper [in Obs.sem_obs]
sat__Ω [in Obs.anticlique]
sequiv_Equiv [in Obs.notations]
SizeList [in Obs.list_tools]
ssmaller_PartialOrder [in Obs.notations]
ssmaller_PreOrder [in Obs.notations]
sym_fincompatible [in Obs.coherence_graph]
sym_incompatible [in Obs.coherence_graph]
U
undup_equivalent_Proper [in Obs.list_dec]undup_incl_Proper [in Obs.list_dec]
other
Ω [in Obs.anticlique]π_proper [in Obs.laws]
τ_proper_inf__Ω [in Obs.anticlique]
𝒢 [in Obs.product]
Section Index
C
combine [in Obs.list_tools]D
decidable [in Obs.decidable_prop]decidable_graph [in Obs.coherence_graph]
dec_list [in Obs.list_dec]
F
finite_cliques [in Obs.coherence_graph]flip [in Obs.list_tools]
M
mix [in Obs.list_tools]S
s [in Obs.coherence_graph]s [in Obs.laws]
s [in Obs.equiv_obs]
s [in Obs.fin_sem_obs]
s [in Obs.product]
s [in Obs.sem_obs]
s [in Obs.fan]
s [in Obs.anticlique]
SemEquiv [in Obs.notations]
shuffle [in Obs.list_tools]
Abbreviation Index
A
axΩ [in Obs.anticlique]E
eq_fcliques [in Obs.coherence_graph]F
FAN [in Obs.fan]I
inf_fcliques [in Obs.coherence_graph]inf_fcliques [in Obs.coherence_graph]
inf_cliques [in Obs.coherence_graph]
inf_cliques [in Obs.coherence_graph]
N
nb [in Obs.list_dec]nb [in Obs.list_dec]
O
O [in Obs.equiv_obs]Obs [in Obs.equiv_obs]
Obs' [in Obs.equiv_obs]
P
prj1 [in Obs.list_tools]prj2 [in Obs.list_tools]
S
sgl [in Obs.coherence_graph]sgl [in Obs.coherence_graph]
V
V [in Obs.product]other
𝒜 [in Obs.product]𝖳 [in Obs.product]
Definition Index
A
atTop [in Obs.product]C
choose_clique [in Obs.sem_obs]cnf_to_dnf [in Obs.product]
cnf_support [in Obs.product]
coh𝒢_sind [in Obs.product]
coh𝒢_ind [in Obs.product]
Conj [in Obs.fan]
conj_interp [in Obs.product]
D
difference [in Obs.list_dec]disj_interp [in Obs.product]
dnf_to_cnf [in Obs.product]
dnf_support [in Obs.product]
E
empt [in Obs.coherence_graph]equal_list [in Obs.list_dec]
equivalent [in Obs.list_tools]
equivalentb [in Obs.list_dec]
equiv_Obs_sind [in Obs.equiv_obs]
equiv_Obs_ind [in Obs.equiv_obs]
eq𝒱 [in Obs.product]
F
fan_ax_sind [in Obs.fan]fan_ax_ind [in Obs.fan]
fcic [in Obs.coherence_graph]
fcliques [in Obs.coherence_graph]
fcmem [in Obs.coherence_graph]
fc_to_clique [in Obs.coherence_graph]
fincompatible [in Obs.coherence_graph]
finsat [in Obs.fan]
fjoins [in Obs.coherence_graph]
flip [in Obs.list_tools]
H
ha_ax_sind [in Obs.equiv_obs]ha_ax_ind [in Obs.equiv_obs]
I
impl_lst [in Obs.fin_sem_obs]inb [in Obs.list_dec]
inclb [in Obs.list_dec]
incoh [in Obs.coherence_graph]
incompatible [in Obs.coherence_graph]
incompat_project [in Obs.product]
incompat_inject [in Obs.product]
inf_obs [in Obs.equiv_obs]
inf__Ω [in Obs.anticlique]
inject [in Obs.product]
insert [in Obs.list_tools]
intersect [in Obs.list_dec]
is_coherent [in Obs.coherence_graph]
J
Join [in Obs.syntax_obs]joins [in Obs.coherence_graph]
join_sind [in Obs.equiv_obs]
join_ind [in Obs.equiv_obs]
join__f [in Obs.fan]
L
lift_prod [in Obs.list_tools]lists_of_length [in Obs.list_tools]
M
mapNF [in Obs.product]Meet [in Obs.syntax_obs]
mix [in Obs.list_tools]
N
NF [in Obs.product]nf [in Obs.fan]
NoDupb [in Obs.list_dec]
normal_form [in Obs.product]
O
observation_sind [in Obs.syntax_obs]observation_rec [in Obs.syntax_obs]
observation_ind [in Obs.syntax_obs]
observation_rect [in Obs.syntax_obs]
obs_ax_sind [in Obs.equiv_obs]
obs_ax_ind [in Obs.equiv_obs]
Obs__Ω [in Obs.anticlique]
obs'_ax_sind [in Obs.equiv_obs]
obs'_ax_ind [in Obs.equiv_obs]
obs𝖦_to_𝒯 [in Obs.product]
P
pad [in Obs.list_tools]pairs [in Obs.list_tools]
prod_ax_sind [in Obs.product]
prod_ax_ind [in Obs.product]
project [in Obs.coherence_graph]
project [in Obs.product]
project_list [in Obs.coherence_graph]
R
rm [in Obs.list_dec]rmfst [in Obs.list_dec]
S
sequiv [in Obs.notations]sgl__f [in Obs.coherence_graph]
shuffles [in Obs.list_tools]
ssmaller [in Obs.notations]
subsets [in Obs.list_tools]
sum [in Obs.list_tools]
sup [in Obs.product]
support [in Obs.fin_sem_obs]
T
termVect [in Obs.product]test [in Obs.decidable_prop]
to_Obs__Ω [in Obs.anticlique]
U
undup [in Obs.list_dec]Unnamed_thm [in Obs.decidable_prop]
V
V' [in Obs.anticlique]other
Ω_ax_sind [in Obs.anticlique]Ω_ax_ind [in Obs.anticlique]
ζ [in Obs.anticlique]
ξ [in Obs.anticlique]
π [in Obs.syntax_obs]
τ [in Obs.anticlique]
𝒯 [in Obs.product]
𝒱_sind [in Obs.product]
𝒱_rec [in Obs.product]
𝒱_ind [in Obs.product]
𝒱_rect [in Obs.product]
Record Index
C
clique [in Obs.coherence_graph]D
DecidableGraph [in Obs.coherence_graph]DecidableProp [in Obs.decidable_prop]
decidable_set [in Obs.decidable_prop]
F
FanGraph [in Obs.fan]G
Graph [in Obs.coherence_graph]S
Satisfaction [in Obs.notations]Size [in Obs.notations]
| 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 | (850 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 | (81 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (56 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 entries) |
| Lemma Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (366 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 | (41 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (18 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (14 entries) |
| Instance Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (115 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (17 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (19 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 | (102 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (8 entries) |
This page has been generated by coqdoc