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 (593 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 (32 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1 entry)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (21 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 (19 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 (225 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 (31 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 (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 (15 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 (139 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (21 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 (2 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (71 entries)
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

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


B

Base [library]
bij_ren_is_decidable_inj_ren [lemma, in HOcore.Ren]
bij_ren_clos_symmetric [instance, in HOcore.Ren]
bij_ren_clos_mono [instance, in HOcore.Ren]
bij_ren_clos [definition, in HOcore.Ren]
bij_ren [definition, in HOcore.Ren]
Bis [library]
BisCongr [library]
BisDecInjRen [library]
BisSubstit [library]
bool_eq_dec [instance, in Base.Base]
bot2 [abbreviation, in HOcore.Prelim]


C

card [definition, in Base.Base]
Cardinality [section, in Base.Base]
Cardinality.X [variable, in Base.Base]
card_equi_proper [instance, in Base.Base]
card_or [lemma, in Base.Base]
card_lt [lemma, in Base.Base]
card_equi [lemma, in Base.Base]
card_ex [lemma, in Base.Base]
card_0 [lemma, in Base.Base]
card_cons_rem [lemma, in Base.Base]
card_eq [lemma, in Base.Base]
card_le [lemma, in Base.Base]
card_not_in_rem [lemma, in Base.Base]
card_in_rem [lemma, in Base.Base]
chan [definition, in HOcore.HoCore]
companion [definition, in HOcore.Compat]
companion_sound [lemma, in HOcore.Compat]
companion_correct [lemma, in HOcore.Compat]
companion_semi_idemp [lemma, in HOcore.Compat]
companion_compat [instance, in HOcore.Compat]
companion_mono [instance, in HOcore.Compat]
Compat [record, in HOcore.Compat]
Compat [inductive, in HOcore.Compat]
Compat [section, in HOcore.Compat]
Compat [library]
compat_impl_sound [lemma, in HOcore.Compat]
compat_impl_congruence [lemma, in HOcore.Compat]
Compat.CompatImplSound [section, in HOcore.Compat]
CompleteLattice [section, in HOcore.ComplLat]
CompleteLattice.Map [section, in HOcore.ComplLat]
CompleteLattice.PreservMonoidProperties [section, in HOcore.ComplLat]
_ °^ _ [notation, in HOcore.ComplLat]
_ ° _ [notation, in HOcore.ComplLat]
_ /2\^ _ [notation, in HOcore.ComplLat]
_ /2\ _ [notation, in HOcore.ComplLat]
_ \2/^ _ [notation, in HOcore.ComplLat]
_ =2=^ _ [notation, in HOcore.ComplLat]
_ <2=^ _ [notation, in HOcore.ComplLat]
_ =2= _ [notation, in HOcore.ComplLat]
ComplLat [library]
compose_preserv_ext [instance, in HOcore.ComplLat]
compose_preserv_symmetric_fun [instance, in HOcore.ComplLat]
compose_with_ext_is_superset [lemma, in HOcore.ComplLat]
compose_preserv_mono [instance, in HOcore.ComplLat]
compose_preserv_compat [lemma, in HOcore.Compat]
comp_preserv_bij_ren [lemma, in HOcore.Ren]
CondClos [record, in HOcore.CondClos]
CondClos [inductive, in HOcore.CondClos]
CondClos [section, in HOcore.CondClos]
CondClos [library]
cond_clos_impl_congruence [lemma, in HOcore.CondClos]
cond_compat [projection, in HOcore.CondClos]
cond_compat [constructor, in HOcore.CondClos]
cond_clos_of_increasing_impl_congruence [lemma, in HOcore.BisCongr]
cond_compat [projection, in HOcore.Compat]
cond_compat [constructor, in HOcore.Compat]
CongrCondClos [record, in HOcore.BisCongr]
CongrCondClos [inductive, in HOcore.BisCongr]
CongrCondClos [section, in HOcore.BisCongr]
congruence [definition, in HOcore.ComplLat]
congr_cond_clos_impl_cond_clos [instance, in HOcore.BisCongr]
congr_cond_clos [projection, in HOcore.BisCongr]
congr_cond_clos [constructor, in HOcore.BisCongr]
const_to_postfp_cond_clos [instance, in HOcore.CondClos]
const_top2_sym [instance, in HOcore.ComplLat]
const_bot2_sym [instance, in HOcore.ComplLat]
const_sym [instance, in HOcore.ComplLat]
const_to_x_mono [instance, in HOcore.ComplLat]
const_to_postfp_compat [instance, in HOcore.Compat]
cons_equi_proper [instance, in Base.Base]
cons_incl_proper [instance, in Base.Base]
contexts_have_single_zero [lemma, in HOcore.InclIoMultiBisIoCxtBis]
contexts_maintain_var_occurrence [lemma, in HOcore.InclIoMultiBisIoCxtBis]
contexts_decrease_var_occurrence [lemma, in HOcore.InclIoMultiBisIoCxtBis]
context_clos_congruent_for_s_io_cxt_sym [lemma, in HOcore.IoCxtBis]
context_clos [definition, in HOcore.IoCxtBis]
context_fill_step_var_cxt [lemma, in HOcore.Subst]
correct [definition, in HOcore.ComplLat]
count [definition, in HOcore.Multiset]


D

dec [definition, in Base.Base]
decidable_inj_ren_comp_bij_ren_is_decidable_inj_ren [lemma, in HOcore.Ren]
decidable_inj_ren_is_inj_ren [lemma, in HOcore.Ren]
decidable_inj_ren_clos_ext [instance, in HOcore.Ren]
decidable_inj_ren_clos_symmetric [instance, in HOcore.Ren]
decidable_inj_ren_clos_mono [instance, in HOcore.Ren]
decidable_inj_ren_clos [definition, in HOcore.Ren]
decidable_inj_ren [definition, in HOcore.Ren]
decision [definition, in Base.Base]
decreasify [definition, in HOcore.ComplLat]
decreasify_preserv_mono [instance, in HOcore.ComplLat]
decreasing_g_up_preserv_cond_clos [instance, in HOcore.CondClos]
decreasing_subset [lemma, in HOcore.ComplLat]
dec_prop_iff [lemma, in Base.Base]
dec_DM_impl [lemma, in Base.Base]
dec_DM_and [lemma, in Base.Base]
dec_DN [lemma, in Base.Base]
disjoint [definition, in Base.Base]
disjoint_app [lemma, in Base.Base]
disjoint_cons [lemma, in Base.Base]
disjoint_nil' [lemma, in Base.Base]
disjoint_nil [lemma, in Base.Base]
disjoint_incl [lemma, in Base.Base]
disjoint_symm [lemma, in Base.Base]
disjoint_forall [lemma, in Base.Base]
DM_exists [lemma, in Base.Base]
DM_or [lemma, in Base.Base]
Dupfree [section, in Base.Base]
dupfree [inductive, in Base.Base]
dupfreeC [constructor, in Base.Base]
dupfreeN [constructor, in Base.Base]
dupfree_inv [definition, in Base.Base]
dupfree_in_power [lemma, in Base.Base]
dupfree_power [lemma, in Base.Base]
dupfree_undup [lemma, in Base.Base]
dupfree_card [lemma, in Base.Base]
dupfree_dec [lemma, in Base.Base]
dupfree_filter [lemma, in Base.Base]
dupfree_map [lemma, in Base.Base]
dupfree_app [lemma, in Base.Base]
dupfree_cons [lemma, in Base.Base]
Dupfree.X [variable, in Base.Base]


E

Equi [section, in Base.Base]
equi [definition, in Base.Base]
equi_rotate [lemma, in Base.Base]
equi_shift [lemma, in Base.Base]
equi_swap [lemma, in Base.Base]
equi_dup [lemma, in Base.Base]
equi_push [lemma, in Base.Base]
equi_Equivalence [instance, in Base.Base]
Equi.X [variable, in Base.Base]
ext [projection, in HOcore.ComplLat]
Ext [record, in HOcore.ComplLat]
ext [constructor, in HOcore.ComplLat]
Ext [inductive, in HOcore.ComplLat]


F

False_dec [instance, in Base.Base]
FCI [module, in Base.Base]
FCI.C [definition, in Base.Base]
FCI.closure [lemma, in Base.Base]
FCI.F [definition, in Base.Base]
FCI.FCI [section, in Base.Base]
FCI.FCI.step [variable, in Base.Base]
FCI.FCI.V [variable, in Base.Base]
FCI.FCI.X [variable, in Base.Base]
FCI.fp [lemma, in Base.Base]
FCI.incl [lemma, in Base.Base]
FCI.ind [lemma, in Base.Base]
FCI.it_incl [lemma, in Base.Base]
FCI.pick [lemma, in Base.Base]
filter [definition, in Base.Base]
FilterComm [section, in Base.Base]
FilterComm.p [variable, in Base.Base]
FilterComm.q [variable, in Base.Base]
FilterComm.X [variable, in Base.Base]
FilterLemmas [section, in Base.Base]
FilterLemmas_pq.q [variable, in Base.Base]
FilterLemmas_pq.p [variable, in Base.Base]
FilterLemmas_pq.X [variable, in Base.Base]
FilterLemmas_pq [section, in Base.Base]
FilterLemmas.p [variable, in Base.Base]
FilterLemmas.X [variable, in Base.Base]
filter_comm [lemma, in Base.Base]
filter_and [lemma, in Base.Base]
filter_pq_eq [lemma, in Base.Base]
filter_pq_mono [lemma, in Base.Base]
filter_fst' [lemma, in Base.Base]
filter_fst [lemma, in Base.Base]
filter_app [lemma, in Base.Base]
filter_id [lemma, in Base.Base]
filter_mono [lemma, in Base.Base]
filter_incl [lemma, in Base.Base]
fin_sum_lemma [lemma, in HOcore.Multiset]
fin_sum_add [lemma, in HOcore.Multiset]
fin_sum_reduce [lemma, in HOcore.Multiset]
fin_sum [definition, in HOcore.Multiset]
FP [definition, in Base.Base]
f_reach_cond_clos_for_s_var_multi [lemma, in HOcore.InclIoMultiBisIoCxtBis]
f_reach_cond_clos_for_s_ho_in [lemma, in HOcore.InclIoMultiBisIoCxtBis]
f_reach_cond_clos_for_s_ho_out [lemma, in HOcore.InclIoMultiBisIoCxtBis]
f_reach_sym [instance, in HOcore.InclIoMultiBisIoCxtBis]
f_reach_mono [instance, in HOcore.InclIoMultiBisIoCxtBis]
f_reach [definition, in HOcore.InclIoMultiBisIoCxtBis]


H

HoCore [library]
ho_in_substit_cond_clos [instance, in HOcore.BisSubstit]
ho_out_substit_cond_clos [instance, in HOcore.BisSubstit]


I

Ids_process [instance, in HOcore.HoCore]
id_cond_clos [instance, in HOcore.CondClos]
id_decidable_inj_ren [lemma, in HOcore.Ren]
id_sym [instance, in HOcore.ComplLat]
id_mono [instance, in HOcore.ComplLat]
id_compat [instance, in HOcore.Compat]
iff_dec [instance, in Base.Base]
impl_dec [instance, in Base.Base]
InclIoCxtBisIoRemBis [library]
InclIoMultiBisIoCxtBis [library]
InclIoRemBisIoMultiBis [library]
inclp [definition, in Base.Base]
Inclusion [section, in Base.Base]
Inclusion.X [variable, in Base.Base]
incl_equi_proper [instance, in Base.Base]
incl_preorder [instance, in Base.Base]
incl_app_left [lemma, in Base.Base]
incl_lrcons [lemma, in Base.Base]
incl_rcons [lemma, in Base.Base]
incl_sing [lemma, in Base.Base]
incl_lcons [lemma, in Base.Base]
incl_shift [lemma, in Base.Base]
incl_nil_eq [lemma, in Base.Base]
incl_map [lemma, in Base.Base]
incl_nil [lemma, in Base.Base]
increasify [definition, in HOcore.ComplLat]
increasify_impl_ext [instance, in HOcore.ComplLat]
increasify_preserv_sym [instance, in HOcore.ComplLat]
increasify_preserv_mono [instance, in HOcore.ComplLat]
increasing_g_lo_preserv_cond_clos [instance, in HOcore.CondClos]
inj_ren_inv_var [lemma, in HOcore.Ren]
inj_ren_inv [lemma, in HOcore.Ren]
inj_ren_clos_symmetric [instance, in HOcore.Ren]
inj_ren_clos [definition, in HOcore.Ren]
inj_ren_clos_compat_for_s_var_multi [instance, in HOcore.BisDecInjRen]
inj_ren_clos_compat_for_s_var_cxt [instance, in HOcore.BisDecInjRen]
inj_ren_clos_compat_for_s_ho_in [instance, in HOcore.BisDecInjRen]
inj_ren_clos_compat_for_s_ho_out [instance, in HOcore.BisDecInjRen]
instantiate' [definition, in HOcore.HoCore]
intersect [definition, in HOcore.ComplLat]
intersect_fun_bin_preserv_cond_clos [instance, in HOcore.CondClos]
intersect_fun_bin_preserv_preserv_monoid_trans [instance, in HOcore.ComplLat]
intersect_fun_bin_preserv_preserv_monoid_refl [instance, in HOcore.ComplLat]
intersect_postfp_iff_postfp_in_every_member [lemma, in HOcore.ComplLat]
intersect_fun_bin_preserv_mono [instance, in HOcore.ComplLat]
intersect_fun_bin [definition, in HOcore.ComplLat]
intersect_bin [definition, in HOcore.ComplLat]
intersect_fun_preserv_mono [definition, in HOcore.ComplLat]
intersect_fun_subset_member [lemma, in HOcore.ComplLat]
intersect_fun [definition, in HOcore.ComplLat]
intersect_fun_bin_preserv_compat [instance, in HOcore.Compat]
in_rem_iff [lemma, in Base.Base]
in_filter_iff [lemma, in Base.Base]
in_equi_proper [instance, in Base.Base]
in_incl_proper [instance, in Base.Base]
in_cons_neq [lemma, in Base.Base]
in_sing [lemma, in Base.Base]
IoCxtBis [library]
IoMultiBis [library]
io_rem_bis_subset_io_multi_bis [lemma, in HOcore.InclIoRemBisIoMultiBis]
io_cxt_bis_subset_io_rem_bis [lemma, in HOcore.InclIoCxtBisIoRemBis]
io_multi_bis_subset_io_cxt_bis [lemma, in HOcore.InclIoMultiBisIoCxtBis]
it [definition, in Base.Base]
Iteration [section, in Base.Base]
Iteration.f [variable, in Base.Base]
Iteration.X [variable, in Base.Base]
it_fp [lemma, in Base.Base]
it_ind [lemma, in Base.Base]


K

knaster_tarski [lemma, in HOcore.ComplLat]


L

lifted_has_no_zero [lemma, in HOcore.InclIoMultiBisIoCxtBis]
lifted_iff_nonlifted [lemma, in HOcore.InclIoMultiBisIoCxtBis]
list_cc [lemma, in Base.Base]
list_exists_not_incl [lemma, in Base.Base]
list_exists_DM [lemma, in Base.Base]
list_exists_dec [instance, in Base.Base]
list_forall_dec [instance, in Base.Base]
list_sigma_forall [lemma, in Base.Base]
list_in_dec [instance, in Base.Base]
list_eq_dec [instance, in Base.Base]
list_cycle [lemma, in Base.Base]


M

Membership [section, in Base.Base]
Membership.X [variable, in Base.Base]
member_subset_union_fun [lemma, in HOcore.ComplLat]
minus_one [definition, in HOcore.Ren]
mle [definition, in HOcore.Multiset]
mle_impl_less_equal_fin_sums [lemma, in HOcore.Multiset]
mono [projection, in HOcore.ComplLat]
Mono [record, in HOcore.ComplLat]
mono [constructor, in HOcore.ComplLat]
Mono [inductive, in HOcore.ComplLat]
monotone2 [definition, in HOcore.ComplLat]
monotonize [definition, in HOcore.ComplLat]
monotonized_mono [instance, in HOcore.ComplLat]
monotonize_extensive [lemma, in HOcore.ComplLat]
monotonize_compat [lemma, in HOcore.Compat]
mult [definition, in HOcore.Multiset]
multiset [definition, in HOcore.Multiset]
Multiset [library]
multi_congr_s_io_cxt_sym [lemma, in HOcore.IoCxtBis]
multi_context_clos [definition, in HOcore.IoCxtBis]
mult_reduce_alien [lemma, in HOcore.Multiset]
mult_reduce_member [lemma, in HOcore.Multiset]


N

nat_dec [definition, in HOcore.Multiset]
nat_le_dec [instance, in Base.Base]
nat_eq_dec [instance, in Base.Base]
Nil [constructor, in HOcore.HoCore]
nil_step_then_unguarded_var [lemma, in HOcore.InclIoRemBisIoMultiBis]
not_in_cons [lemma, in Base.Base]
not_dec [instance, in Base.Base]
nu [definition, in HOcore.ComplLat]
nu_of_s_io_cxt_sym_is_closed_under_var_bis_f [lemma, in HOcore.IoCxtBis]
nu_of_s_io_rem_sym_is_closed_under_s_var_multi [lemma, in HOcore.InclIoRemBisIoMultiBis]
nu_of_io_cxt_bis_f_is_closed_under_s_var_rem [lemma, in HOcore.InclIoCxtBisIoRemBis]
nu_is_prefp [lemma, in HOcore.ComplLat]
nu_is_postfp [lemma, in HOcore.ComplLat]
nu_of_s_io_multi_sym_is_closed_under_s_var_cxt [lemma, in HOcore.InclIoMultiBisIoCxtBis]
nu_of_s_io_multi_sym_reach_closed [lemma, in HOcore.InclIoMultiBisIoCxtBis]


O

or_dec [instance, in Base.Base]


P

Par [constructor, in HOcore.HoCore]
par_clos_congruent_for_s_io_cxt_sym [lemma, in HOcore.IoCxtBis]
par_clos_sym [instance, in HOcore.BisCongr]
par_clos_mono [instance, in HOcore.BisCongr]
par_clos [definition, in HOcore.BisCongr]
postfp [definition, in HOcore.ComplLat]
postfp_subset_nu [lemma, in HOcore.ComplLat]
power [definition, in Base.Base]
PowerRep [section, in Base.Base]
PowerRep.X [variable, in Base.Base]
power_extensional [lemma, in Base.Base]
power_nil [lemma, in Base.Base]
power_incl [lemma, in Base.Base]
prefp [definition, in HOcore.ComplLat]
Prelim [library]
PreservMonoidRefl [record, in HOcore.ComplLat]
PreservMonoidRefl [inductive, in HOcore.ComplLat]
PreservMonoidTrans [record, in HOcore.ComplLat]
PreservMonoidTrans [inductive, in HOcore.ComplLat]
preserv_trans_impl_rel_comp_fun_preserv_cond_clos [instance, in HOcore.CondClos]
preserv_monoid_trans_impl_nu_is_transitive [lemma, in HOcore.ComplLat]
preserv_monoid_refl_impl_nu_is_reflexive' [lemma, in HOcore.ComplLat]
preserv_monoid_refl_impl_nu_is_reflexive [lemma, in HOcore.ComplLat]
preserv_monoid_trans_impl_rel_comp_preserv_postfp [lemma, in HOcore.ComplLat]
preserv_monoid_trans [projection, in HOcore.ComplLat]
preserv_monoid_trans [constructor, in HOcore.ComplLat]
preserv_monoid_refl [projection, in HOcore.ComplLat]
preserv_monoid_refl [constructor, in HOcore.ComplLat]
preserv_trans_impl_rel_comp_fun_preserv_compat [instance, in HOcore.Compat]
process [inductive, in HOcore.HoCore]


R

Receive [constructor, in HOcore.HoCore]
receive_clos_congruent_for_s_io_cxt_sym [lemma, in HOcore.IoCxtBis]
receive_clos_sym [instance, in HOcore.BisCongr]
receive_clos_mono [instance, in HOcore.BisCongr]
receive_clos [definition, in HOcore.BisCongr]
refl_clos_sym [instance, in HOcore.ComplLat]
refl_clos_mono [instance, in HOcore.ComplLat]
refl_clos [definition, in HOcore.ComplLat]
rel_comp_fun_preserv_mono [instance, in HOcore.ComplLat]
rel_comp_fun [definition, in HOcore.ComplLat]
rel_comp_into_transp [lemma, in HOcore.ComplLat]
rel_comp_mono [lemma, in HOcore.ComplLat]
rel_comp_mono_right [lemma, in HOcore.ComplLat]
rel_comp_mono_left [lemma, in HOcore.ComplLat]
rel_comp [definition, in HOcore.ComplLat]
rel_incl_impl_transp_rel_incl [lemma, in HOcore.ComplLat]
rel_fun_equiv_intersect_fun_bin_morphism [instance, in HOcore.ComplLat]
rel_fun_equiv_equivalence [instance, in HOcore.ComplLat]
rel_fun_equiv_trans [lemma, in HOcore.ComplLat]
rel_fun_equiv_sym [lemma, in HOcore.ComplLat]
rel_fun_equiv_refl [lemma, in HOcore.ComplLat]
rel_fun_equiv [definition, in HOcore.ComplLat]
rel_fun_incl_trans [lemma, in HOcore.ComplLat]
rel_fun_incl [definition, in HOcore.ComplLat]
rel_equiv_equivalence [instance, in HOcore.ComplLat]
rel_equiv_trans [lemma, in HOcore.ComplLat]
rel_equiv_sym [lemma, in HOcore.ComplLat]
rel_equiv_refl [lemma, in HOcore.ComplLat]
rel_equiv [definition, in HOcore.ComplLat]
rem [definition, in Base.Base]
Removal [section, in Base.Base]
Removal.X [variable, in Base.Base]
rem_inclr [lemma, in Base.Base]
rem_reorder [lemma, in Base.Base]
rem_id [lemma, in Base.Base]
rem_fst' [lemma, in Base.Base]
rem_fst [lemma, in Base.Base]
rem_comm [lemma, in Base.Base]
rem_equi [lemma, in Base.Base]
rem_app' [lemma, in Base.Base]
rem_app [lemma, in Base.Base]
rem_neq [lemma, in Base.Base]
rem_in [lemma, in Base.Base]
rem_cons' [lemma, in Base.Base]
rem_cons [lemma, in Base.Base]
rem_mono [lemma, in Base.Base]
rem_incl [lemma, in Base.Base]
rem_not_in [lemma, in Base.Base]
Ren [library]
Rename_process [instance, in HOcore.HoCore]
renaming_preserv_count [lemma, in HOcore.Multiset]
rep [definition, in Base.Base]
rep_dupfree [lemma, in Base.Base]
rep_idempotent [lemma, in Base.Base]
rep_injective [lemma, in Base.Base]
rep_eq [lemma, in Base.Base]
rep_eq' [lemma, in Base.Base]
rep_mono [lemma, in Base.Base]
rep_equi [lemma, in Base.Base]
rep_in [lemma, in Base.Base]
rep_incl [lemma, in Base.Base]
rep_power [lemma, in Base.Base]


S

Send [constructor, in HOcore.HoCore]
send_clos_congruent_for_s_io_cxt_sym [lemma, in HOcore.IoCxtBis]
send_clos_sym [instance, in HOcore.BisCongr]
send_clos_mono [instance, in HOcore.BisCongr]
send_clos [definition, in HOcore.BisCongr]
shift_decidable_inj_ren [lemma, in HOcore.Ren]
size_recursion [lemma, in Base.Base]
sound [definition, in HOcore.ComplLat]
sound_impl_correct_for_mono [lemma, in HOcore.ComplLat]
step_var_rem_decreases_var_occurrence [lemma, in HOcore.InclIoRemBisIoMultiBis]
step_var_cxt_impl_step_var_rem [lemma, in HOcore.InclIoCxtBisIoRemBis]
step_var_rem_impl_step_var_cxt [lemma, in HOcore.InclIoCxtBisIoRemBis]
step_var_cxt_preserv_ren [lemma, in HOcore.Ren]
step_tau_preserv_ren [lemma, in HOcore.Ren]
step_in_preserv_ren [lemma, in HOcore.Ren]
step_out_preserv_ren [lemma, in HOcore.Ren]
step_then_unguarded_var [lemma, in HOcore.InclIoMultiBisIoCxtBis]
step_var_cxt_inv_subst [lemma, in HOcore.Subst]
step_in_inv_subst [lemma, in HOcore.Subst]
step_out_inv_subst [lemma, in HOcore.Subst]
step_tau_propagation_cxt [lemma, in HOcore.Subst]
step_in_propagation_cxt [lemma, in HOcore.Subst]
step_out_propagation_cxt [lemma, in HOcore.Subst]
step_var_cxt_substit_ren [lemma, in HOcore.Subst]
step_tau_substit [lemma, in HOcore.Subst]
step_in_substit [lemma, in HOcore.Subst]
step_out_substit [lemma, in HOcore.Subst]
step_var_rem [inductive, in HOcore.HoCore]
step_var_cxt [inductive, in HOcore.HoCore]
step_tau [inductive, in HOcore.HoCore]
step_in [inductive, in HOcore.HoCore]
step_out [inductive, in HOcore.HoCore]
StInParL [constructor, in HOcore.HoCore]
StInParR [constructor, in HOcore.HoCore]
StInReceive [constructor, in HOcore.HoCore]
StOutParL [constructor, in HOcore.HoCore]
StOutParR [constructor, in HOcore.HoCore]
StOutSend [constructor, in HOcore.HoCore]
StTauParL [constructor, in HOcore.HoCore]
StTauParR [constructor, in HOcore.HoCore]
StTauSynL [constructor, in HOcore.HoCore]
StTauSynR [constructor, in HOcore.HoCore]
StVarCxt [constructor, in HOcore.HoCore]
StVarCxtParL [constructor, in HOcore.HoCore]
StVarCxtParR [constructor, in HOcore.HoCore]
StVarRemParL [constructor, in HOcore.HoCore]
StVarRemParR [constructor, in HOcore.HoCore]
StVarRemRem [constructor, in HOcore.HoCore]
Subst [library]
SubstLemmas_process [instance, in HOcore.HoCore]
subst_clos_ext [instance, in HOcore.Subst]
subst_clos_symmetric [instance, in HOcore.Subst]
subst_clos_mono [instance, in HOcore.Subst]
subst_clos [definition, in HOcore.Subst]
Subst_process [instance, in HOcore.HoCore]
SymFun [record, in HOcore.ComplLat]
SymFun [inductive, in HOcore.ComplLat]
symmetrize_fun_preserv_cond_clos_when_f_sym [instance, in HOcore.CondClos]
symmetrize_fun_preserv_preserv_monoid_trans [instance, in HOcore.ComplLat]
symmetrize_fun_preserv_preserv_monoid_refl [instance, in HOcore.ComplLat]
symmetrize_fun_preserv_mono [instance, in HOcore.ComplLat]
symmetrize_fun_correct [instance, in HOcore.ComplLat]
symmetrize_fun [definition, in HOcore.ComplLat]
symmetrize_fun_preserv_compat_when_f_sym [instance, in HOcore.Compat]
sym_f_impl_sym_nu [lemma, in HOcore.ComplLat]
sym_fun [projection, in HOcore.ComplLat]
sym_fun [constructor, in HOcore.ComplLat]
s_io_cxt_sym_substit [lemma, in HOcore.IoCxtBis]
s_io_cxt_sym_closed_under_decidable_inj_ren [lemma, in HOcore.IoCxtBis]
s_var_multi_preserv_monoid_trans [instance, in HOcore.Bis]
s_var_cxt_preserv_monoid_trans [instance, in HOcore.Bis]
s_ho_in_preserv_monoid_trans [instance, in HOcore.Bis]
s_ho_out_preserv_monoid_trans [instance, in HOcore.Bis]
s_tau_preserv_monoid_trans [instance, in HOcore.Bis]
s_var_multi_preserv_monoid_refl [instance, in HOcore.Bis]
s_var_cxt_preserv_monoid_refl [instance, in HOcore.Bis]
s_ho_in_preserv_monoid_refl [instance, in HOcore.Bis]
s_ho_out_preserv_monoid_refl [instance, in HOcore.Bis]
s_tau_preserv_monoid_refl [instance, in HOcore.Bis]
s_io_cxt_sym_mono [instance, in HOcore.Bis]
s_io_cxt_mono [instance, in HOcore.Bis]
s_var_multi_mono [instance, in HOcore.Bis]
s_var_cxt_mono [instance, in HOcore.Bis]
s_var_rem_mono [instance, in HOcore.Bis]
s_ho_in_mono [instance, in HOcore.Bis]
s_ho_out_mono [instance, in HOcore.Bis]
s_tau_mono [instance, in HOcore.Bis]
s_var_multi [definition, in HOcore.Bis]
s_var_rem [definition, in HOcore.Bis]
s_var_cxt [definition, in HOcore.Bis]
s_ho_in [definition, in HOcore.Bis]
s_ho_out [definition, in HOcore.Bis]
s_tau [definition, in HOcore.Bis]
s_io_multi_sym_closed_under_decidable_inj_ren [lemma, in HOcore.IoMultiBis]
s_var_multi_fulfills_cond_compat_for_par_clos [instance, in HOcore.BisCongr]
s_var_cxt_fulfills_cond_compat_for_par_clos [instance, in HOcore.BisCongr]
s_ho_in_fulfills_cond_compat_for_par_clos [instance, in HOcore.BisCongr]
s_ho_out_fulfills_cond_compat_for_par_clos [instance, in HOcore.BisCongr]
s_var_multi_fulfills_cond_compat_for_receive_clos [instance, in HOcore.BisCongr]
s_var_cxt_fulfills_cond_compat_for_receive_clos [instance, in HOcore.BisCongr]
s_ho_in_fulfills_cond_compat_for_receive_clos [instance, in HOcore.BisCongr]
s_ho_out_fulfills_cond_compat_for_receive_clos [instance, in HOcore.BisCongr]
s_var_multi_fulfills_cond_compat_for_send_clos [instance, in HOcore.BisCongr]
s_var_cxt_fulfills_cond_compat_for_send_clos [instance, in HOcore.BisCongr]
s_ho_in_fulfills_cond_compat_for_send_clos [instance, in HOcore.BisCongr]
s_ho_out_fulfills_cond_compat_for_send_clos [instance, in HOcore.BisCongr]


T

top2 [abbreviation, in HOcore.Prelim]
transp_fun_preserv_cond_clos_when_f_sym [instance, in HOcore.CondClos]
transp_fun_bin_preserv_cond_clos [instance, in HOcore.CondClos]
transp_into_rel_comp [lemma, in HOcore.ComplLat]
transp_fun_distributes_over_compose [lemma, in HOcore.ComplLat]
transp_fun_distributes_over_intersect_fun_bin [lemma, in HOcore.ComplLat]
transp_fun_preserv_mono [instance, in HOcore.ComplLat]
transp_fun [definition, in HOcore.ComplLat]
transp_into_union [lemma, in HOcore.ComplLat]
transp_rel_incl_impl_rel_incl [lemma, in HOcore.ComplLat]
transp_mono [instance, in HOcore.ComplLat]
transp_fun_preserv_compat_when_f_sym [instance, in HOcore.Compat]
transp_fun_bin_preserv_compat [instance, in HOcore.Compat]
True_dec [instance, in Base.Base]


U

undup [definition, in Base.Base]
Undup [section, in Base.Base]
undup_idempotent [lemma, in Base.Base]
undup_id [lemma, in Base.Base]
undup_equi [lemma, in Base.Base]
undup_incl [lemma, in Base.Base]
undup_id_equi [lemma, in Base.Base]
Undup.X [variable, in Base.Base]
unguarded_var_then_nil_step [lemma, in HOcore.InclIoRemBisIoMultiBis]
unguarded_var_then_step [lemma, in HOcore.InclIoMultiBisIoCxtBis]
union [definition, in HOcore.ComplLat]
union_fun_bin_preserv_cond_clos [instance, in HOcore.CondClos]
union_mult [lemma, in HOcore.Multiset]
union_fun_bin_preserv_ext_left [instance, in HOcore.ComplLat]
union_fun_bin_preserv_sym_fun [instance, in HOcore.ComplLat]
union_into_transp [lemma, in HOcore.ComplLat]
union_fun_bin_preserv_mono [instance, in HOcore.ComplLat]
union_fun_bin [definition, in HOcore.ComplLat]
union_fun [definition, in HOcore.ComplLat]
union_fun_bin_preserv_compat [instance, in HOcore.Compat]
upren_preserv_bij [lemma, in HOcore.Ren]
upren_preserv_dec_inj_ren [lemma, in HOcore.Ren]
upren_preserv_inj [lemma, in HOcore.Ren]
UpToNu [section, in HOcore.UpToNu]
UpToNu [library]
up_to_io_bisimilarity_sound [lemma, in HOcore.IoCxtBis]
up_to_io_bisimilarity_sound [lemma, in HOcore.IoMultiBis]
up_to_nu_f_is_nu_f_compat [instance, in HOcore.UpToNu]
up_to_nu_preserv_symmetric_fun [instance, in HOcore.UpToNu]
up_to_nu_preserv_mono [instance, in HOcore.UpToNu]
up_to_nu [definition, in HOcore.UpToNu]


V

Var [constructor, in HOcore.HoCore]
var_and_in_can_be_combined [lemma, in HOcore.InclIoMultiBisIoCxtBis]
var_and_out_can_be_combined [lemma, in HOcore.InclIoMultiBisIoCxtBis]
var_then_in_step_can_be_reversed [lemma, in HOcore.InclIoMultiBisIoCxtBis]
var_then_out_step_can_be_reversed [lemma, in HOcore.InclIoMultiBisIoCxtBis]
var_then_out_step_impl_lifted_output [lemma, in HOcore.InclIoMultiBisIoCxtBis]
var_implication [lemma, in HOcore.InclIoMultiBisIoCxtBis]
var_multi_substit_cond_clos [instance, in HOcore.BisSubstit]
var_substit_cond_clos [instance, in HOcore.BisSubstit]


other

_ °^ _ [notation, in HOcore.ComplLat]
_ ° _ [notation, in HOcore.ComplLat]
_ \2/^ _ [notation, in HOcore.ComplLat]
_ /2\^ _ [notation, in HOcore.ComplLat]
_ /2\ _ [notation, in HOcore.ComplLat]
_ =2=^ _ [notation, in HOcore.ComplLat]
_ <2=^ _ [notation, in HOcore.ComplLat]
_ °° _ [notation, in HOcore.ComplLat]
_ =2= _ [notation, in HOcore.ComplLat]
_ \2/ _ [notation, in HOcore.Prelim]
_ <2= _ [notation, in HOcore.Prelim]
_ °° _ [notation, in HOcore.Prelim]
_ === _ [notation, in Base.Base]
_ <<= _ [notation, in Base.Base]
_ el _ [notation, in Base.Base]
eq_dec _ [notation, in Base.Base]
s_io_rem_sym [notation, in HOcore.Bis]
s_io_rem [notation, in HOcore.Bis]
s_io_multi_sym [notation, in HOcore.Bis]
s_io_multi [notation, in HOcore.Bis]
s_io_cxt_sym [notation, in HOcore.Bis]
s_io_cxt [notation, in HOcore.Bis]
s_tau_sym [notation, in HOcore.Bis]
| _ | [notation, in Base.Base]



Notation Index

C

_ °^ _ [in HOcore.ComplLat]
_ ° _ [in HOcore.ComplLat]
_ /2\^ _ [in HOcore.ComplLat]
_ /2\ _ [in HOcore.ComplLat]
_ \2/^ _ [in HOcore.ComplLat]
_ =2=^ _ [in HOcore.ComplLat]
_ <2=^ _ [in HOcore.ComplLat]
_ =2= _ [in HOcore.ComplLat]


other

_ °^ _ [in HOcore.ComplLat]
_ ° _ [in HOcore.ComplLat]
_ \2/^ _ [in HOcore.ComplLat]
_ /2\^ _ [in HOcore.ComplLat]
_ /2\ _ [in HOcore.ComplLat]
_ =2=^ _ [in HOcore.ComplLat]
_ <2=^ _ [in HOcore.ComplLat]
_ °° _ [in HOcore.ComplLat]
_ =2= _ [in HOcore.ComplLat]
_ \2/ _ [in HOcore.Prelim]
_ <2= _ [in HOcore.Prelim]
_ °° _ [in HOcore.Prelim]
_ === _ [in Base.Base]
_ <<= _ [in Base.Base]
_ el _ [in Base.Base]
eq_dec _ [in Base.Base]
s_io_rem_sym [in HOcore.Bis]
s_io_rem [in HOcore.Bis]
s_io_multi_sym [in HOcore.Bis]
s_io_multi [in HOcore.Bis]
s_io_cxt_sym [in HOcore.Bis]
s_io_cxt [in HOcore.Bis]
s_tau_sym [in HOcore.Bis]
| _ | [in Base.Base]



Module Index

F

FCI [in Base.Base]



Variable Index

C

Cardinality.X [in Base.Base]


D

Dupfree.X [in Base.Base]


E

Equi.X [in Base.Base]


F

FCI.FCI.step [in Base.Base]
FCI.FCI.V [in Base.Base]
FCI.FCI.X [in Base.Base]
FilterComm.p [in Base.Base]
FilterComm.q [in Base.Base]
FilterComm.X [in Base.Base]
FilterLemmas_pq.q [in Base.Base]
FilterLemmas_pq.p [in Base.Base]
FilterLemmas_pq.X [in Base.Base]
FilterLemmas.p [in Base.Base]
FilterLemmas.X [in Base.Base]


I

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


M

Membership.X [in Base.Base]


P

PowerRep.X [in Base.Base]


R

Removal.X [in Base.Base]


U

Undup.X [in Base.Base]



Library Index

B

Base
Bis
BisCongr
BisDecInjRen
BisSubstit


C

Compat
ComplLat
CondClos


H

HoCore


I

InclIoCxtBisIoRemBis
InclIoMultiBisIoCxtBis
InclIoRemBisIoMultiBis
IoCxtBis
IoMultiBis


M

Multiset


P

Prelim


R

Ren


S

Subst


U

UpToNu



Lemma Index

B

bij_ren_is_decidable_inj_ren [in HOcore.Ren]


C

card_or [in Base.Base]
card_lt [in Base.Base]
card_equi [in Base.Base]
card_ex [in Base.Base]
card_0 [in Base.Base]
card_cons_rem [in Base.Base]
card_eq [in Base.Base]
card_le [in Base.Base]
card_not_in_rem [in Base.Base]
card_in_rem [in Base.Base]
companion_sound [in HOcore.Compat]
companion_correct [in HOcore.Compat]
companion_semi_idemp [in HOcore.Compat]
compat_impl_sound [in HOcore.Compat]
compat_impl_congruence [in HOcore.Compat]
compose_with_ext_is_superset [in HOcore.ComplLat]
compose_preserv_compat [in HOcore.Compat]
comp_preserv_bij_ren [in HOcore.Ren]
cond_clos_impl_congruence [in HOcore.CondClos]
cond_clos_of_increasing_impl_congruence [in HOcore.BisCongr]
contexts_have_single_zero [in HOcore.InclIoMultiBisIoCxtBis]
contexts_maintain_var_occurrence [in HOcore.InclIoMultiBisIoCxtBis]
contexts_decrease_var_occurrence [in HOcore.InclIoMultiBisIoCxtBis]
context_clos_congruent_for_s_io_cxt_sym [in HOcore.IoCxtBis]
context_fill_step_var_cxt [in HOcore.Subst]


D

decidable_inj_ren_comp_bij_ren_is_decidable_inj_ren [in HOcore.Ren]
decidable_inj_ren_is_inj_ren [in HOcore.Ren]
decreasing_subset [in HOcore.ComplLat]
dec_prop_iff [in Base.Base]
dec_DM_impl [in Base.Base]
dec_DM_and [in Base.Base]
dec_DN [in Base.Base]
disjoint_app [in Base.Base]
disjoint_cons [in Base.Base]
disjoint_nil' [in Base.Base]
disjoint_nil [in Base.Base]
disjoint_incl [in Base.Base]
disjoint_symm [in Base.Base]
disjoint_forall [in Base.Base]
DM_exists [in Base.Base]
DM_or [in Base.Base]
dupfree_in_power [in Base.Base]
dupfree_power [in Base.Base]
dupfree_undup [in Base.Base]
dupfree_card [in Base.Base]
dupfree_dec [in Base.Base]
dupfree_filter [in Base.Base]
dupfree_map [in Base.Base]
dupfree_app [in Base.Base]
dupfree_cons [in Base.Base]


E

equi_rotate [in Base.Base]
equi_shift [in Base.Base]
equi_swap [in Base.Base]
equi_dup [in Base.Base]
equi_push [in Base.Base]


F

FCI.closure [in Base.Base]
FCI.fp [in Base.Base]
FCI.incl [in Base.Base]
FCI.ind [in Base.Base]
FCI.it_incl [in Base.Base]
FCI.pick [in Base.Base]
filter_comm [in Base.Base]
filter_and [in Base.Base]
filter_pq_eq [in Base.Base]
filter_pq_mono [in Base.Base]
filter_fst' [in Base.Base]
filter_fst [in Base.Base]
filter_app [in Base.Base]
filter_id [in Base.Base]
filter_mono [in Base.Base]
filter_incl [in Base.Base]
fin_sum_lemma [in HOcore.Multiset]
fin_sum_add [in HOcore.Multiset]
fin_sum_reduce [in HOcore.Multiset]
f_reach_cond_clos_for_s_var_multi [in HOcore.InclIoMultiBisIoCxtBis]
f_reach_cond_clos_for_s_ho_in [in HOcore.InclIoMultiBisIoCxtBis]
f_reach_cond_clos_for_s_ho_out [in HOcore.InclIoMultiBisIoCxtBis]


I

id_decidable_inj_ren [in HOcore.Ren]
incl_app_left [in Base.Base]
incl_lrcons [in Base.Base]
incl_rcons [in Base.Base]
incl_sing [in Base.Base]
incl_lcons [in Base.Base]
incl_shift [in Base.Base]
incl_nil_eq [in Base.Base]
incl_map [in Base.Base]
incl_nil [in Base.Base]
inj_ren_inv_var [in HOcore.Ren]
inj_ren_inv [in HOcore.Ren]
intersect_postfp_iff_postfp_in_every_member [in HOcore.ComplLat]
intersect_fun_subset_member [in HOcore.ComplLat]
in_rem_iff [in Base.Base]
in_filter_iff [in Base.Base]
in_cons_neq [in Base.Base]
in_sing [in Base.Base]
io_rem_bis_subset_io_multi_bis [in HOcore.InclIoRemBisIoMultiBis]
io_cxt_bis_subset_io_rem_bis [in HOcore.InclIoCxtBisIoRemBis]
io_multi_bis_subset_io_cxt_bis [in HOcore.InclIoMultiBisIoCxtBis]
it_fp [in Base.Base]
it_ind [in Base.Base]


K

knaster_tarski [in HOcore.ComplLat]


L

lifted_has_no_zero [in HOcore.InclIoMultiBisIoCxtBis]
lifted_iff_nonlifted [in HOcore.InclIoMultiBisIoCxtBis]
list_cc [in Base.Base]
list_exists_not_incl [in Base.Base]
list_exists_DM [in Base.Base]
list_sigma_forall [in Base.Base]
list_cycle [in Base.Base]


M

member_subset_union_fun [in HOcore.ComplLat]
mle_impl_less_equal_fin_sums [in HOcore.Multiset]
monotonize_extensive [in HOcore.ComplLat]
monotonize_compat [in HOcore.Compat]
multi_congr_s_io_cxt_sym [in HOcore.IoCxtBis]
mult_reduce_alien [in HOcore.Multiset]
mult_reduce_member [in HOcore.Multiset]


N

nil_step_then_unguarded_var [in HOcore.InclIoRemBisIoMultiBis]
not_in_cons [in Base.Base]
nu_of_s_io_cxt_sym_is_closed_under_var_bis_f [in HOcore.IoCxtBis]
nu_of_s_io_rem_sym_is_closed_under_s_var_multi [in HOcore.InclIoRemBisIoMultiBis]
nu_of_io_cxt_bis_f_is_closed_under_s_var_rem [in HOcore.InclIoCxtBisIoRemBis]
nu_is_prefp [in HOcore.ComplLat]
nu_is_postfp [in HOcore.ComplLat]
nu_of_s_io_multi_sym_is_closed_under_s_var_cxt [in HOcore.InclIoMultiBisIoCxtBis]
nu_of_s_io_multi_sym_reach_closed [in HOcore.InclIoMultiBisIoCxtBis]


P

par_clos_congruent_for_s_io_cxt_sym [in HOcore.IoCxtBis]
postfp_subset_nu [in HOcore.ComplLat]
power_extensional [in Base.Base]
power_nil [in Base.Base]
power_incl [in Base.Base]
preserv_monoid_trans_impl_nu_is_transitive [in HOcore.ComplLat]
preserv_monoid_refl_impl_nu_is_reflexive' [in HOcore.ComplLat]
preserv_monoid_refl_impl_nu_is_reflexive [in HOcore.ComplLat]
preserv_monoid_trans_impl_rel_comp_preserv_postfp [in HOcore.ComplLat]


R

receive_clos_congruent_for_s_io_cxt_sym [in HOcore.IoCxtBis]
rel_comp_into_transp [in HOcore.ComplLat]
rel_comp_mono [in HOcore.ComplLat]
rel_comp_mono_right [in HOcore.ComplLat]
rel_comp_mono_left [in HOcore.ComplLat]
rel_incl_impl_transp_rel_incl [in HOcore.ComplLat]
rel_fun_equiv_trans [in HOcore.ComplLat]
rel_fun_equiv_sym [in HOcore.ComplLat]
rel_fun_equiv_refl [in HOcore.ComplLat]
rel_fun_incl_trans [in HOcore.ComplLat]
rel_equiv_trans [in HOcore.ComplLat]
rel_equiv_sym [in HOcore.ComplLat]
rel_equiv_refl [in HOcore.ComplLat]
rem_inclr [in Base.Base]
rem_reorder [in Base.Base]
rem_id [in Base.Base]
rem_fst' [in Base.Base]
rem_fst [in Base.Base]
rem_comm [in Base.Base]
rem_equi [in Base.Base]
rem_app' [in Base.Base]
rem_app [in Base.Base]
rem_neq [in Base.Base]
rem_in [in Base.Base]
rem_cons' [in Base.Base]
rem_cons [in Base.Base]
rem_mono [in Base.Base]
rem_incl [in Base.Base]
rem_not_in [in Base.Base]
renaming_preserv_count [in HOcore.Multiset]
rep_dupfree [in Base.Base]
rep_idempotent [in Base.Base]
rep_injective [in Base.Base]
rep_eq [in Base.Base]
rep_eq' [in Base.Base]
rep_mono [in Base.Base]
rep_equi [in Base.Base]
rep_in [in Base.Base]
rep_incl [in Base.Base]
rep_power [in Base.Base]


S

send_clos_congruent_for_s_io_cxt_sym [in HOcore.IoCxtBis]
shift_decidable_inj_ren [in HOcore.Ren]
size_recursion [in Base.Base]
sound_impl_correct_for_mono [in HOcore.ComplLat]
step_var_rem_decreases_var_occurrence [in HOcore.InclIoRemBisIoMultiBis]
step_var_cxt_impl_step_var_rem [in HOcore.InclIoCxtBisIoRemBis]
step_var_rem_impl_step_var_cxt [in HOcore.InclIoCxtBisIoRemBis]
step_var_cxt_preserv_ren [in HOcore.Ren]
step_tau_preserv_ren [in HOcore.Ren]
step_in_preserv_ren [in HOcore.Ren]
step_out_preserv_ren [in HOcore.Ren]
step_then_unguarded_var [in HOcore.InclIoMultiBisIoCxtBis]
step_var_cxt_inv_subst [in HOcore.Subst]
step_in_inv_subst [in HOcore.Subst]
step_out_inv_subst [in HOcore.Subst]
step_tau_propagation_cxt [in HOcore.Subst]
step_in_propagation_cxt [in HOcore.Subst]
step_out_propagation_cxt [in HOcore.Subst]
step_var_cxt_substit_ren [in HOcore.Subst]
step_tau_substit [in HOcore.Subst]
step_in_substit [in HOcore.Subst]
step_out_substit [in HOcore.Subst]
sym_f_impl_sym_nu [in HOcore.ComplLat]
s_io_cxt_sym_substit [in HOcore.IoCxtBis]
s_io_cxt_sym_closed_under_decidable_inj_ren [in HOcore.IoCxtBis]
s_io_multi_sym_closed_under_decidable_inj_ren [in HOcore.IoMultiBis]


T

transp_into_rel_comp [in HOcore.ComplLat]
transp_fun_distributes_over_compose [in HOcore.ComplLat]
transp_fun_distributes_over_intersect_fun_bin [in HOcore.ComplLat]
transp_into_union [in HOcore.ComplLat]
transp_rel_incl_impl_rel_incl [in HOcore.ComplLat]


U

undup_idempotent [in Base.Base]
undup_id [in Base.Base]
undup_equi [in Base.Base]
undup_incl [in Base.Base]
undup_id_equi [in Base.Base]
unguarded_var_then_nil_step [in HOcore.InclIoRemBisIoMultiBis]
unguarded_var_then_step [in HOcore.InclIoMultiBisIoCxtBis]
union_mult [in HOcore.Multiset]
union_into_transp [in HOcore.ComplLat]
upren_preserv_bij [in HOcore.Ren]
upren_preserv_dec_inj_ren [in HOcore.Ren]
upren_preserv_inj [in HOcore.Ren]
up_to_io_bisimilarity_sound [in HOcore.IoCxtBis]
up_to_io_bisimilarity_sound [in HOcore.IoMultiBis]


V

var_and_in_can_be_combined [in HOcore.InclIoMultiBisIoCxtBis]
var_and_out_can_be_combined [in HOcore.InclIoMultiBisIoCxtBis]
var_then_in_step_can_be_reversed [in HOcore.InclIoMultiBisIoCxtBis]
var_then_out_step_can_be_reversed [in HOcore.InclIoMultiBisIoCxtBis]
var_then_out_step_impl_lifted_output [in HOcore.InclIoMultiBisIoCxtBis]
var_implication [in HOcore.InclIoMultiBisIoCxtBis]



Constructor Index

C

cond_compat [in HOcore.CondClos]
cond_compat [in HOcore.Compat]
congr_cond_clos [in HOcore.BisCongr]


D

dupfreeC [in Base.Base]
dupfreeN [in Base.Base]


E

ext [in HOcore.ComplLat]


M

mono [in HOcore.ComplLat]


N

Nil [in HOcore.HoCore]


P

Par [in HOcore.HoCore]
preserv_monoid_trans [in HOcore.ComplLat]
preserv_monoid_refl [in HOcore.ComplLat]


R

Receive [in HOcore.HoCore]


S

Send [in HOcore.HoCore]
StInParL [in HOcore.HoCore]
StInParR [in HOcore.HoCore]
StInReceive [in HOcore.HoCore]
StOutParL [in HOcore.HoCore]
StOutParR [in HOcore.HoCore]
StOutSend [in HOcore.HoCore]
StTauParL [in HOcore.HoCore]
StTauParR [in HOcore.HoCore]
StTauSynL [in HOcore.HoCore]
StTauSynR [in HOcore.HoCore]
StVarCxt [in HOcore.HoCore]
StVarCxtParL [in HOcore.HoCore]
StVarCxtParR [in HOcore.HoCore]
StVarRemParL [in HOcore.HoCore]
StVarRemParR [in HOcore.HoCore]
StVarRemRem [in HOcore.HoCore]
sym_fun [in HOcore.ComplLat]


V

Var [in HOcore.HoCore]



Projection Index

C

cond_compat [in HOcore.CondClos]
cond_compat [in HOcore.Compat]
congr_cond_clos [in HOcore.BisCongr]


E

ext [in HOcore.ComplLat]


M

mono [in HOcore.ComplLat]


P

preserv_monoid_trans [in HOcore.ComplLat]
preserv_monoid_refl [in HOcore.ComplLat]


S

sym_fun [in HOcore.ComplLat]



Inductive Index

C

Compat [in HOcore.Compat]
CondClos [in HOcore.CondClos]
CongrCondClos [in HOcore.BisCongr]


D

dupfree [in Base.Base]


E

Ext [in HOcore.ComplLat]


M

Mono [in HOcore.ComplLat]


P

PreservMonoidRefl [in HOcore.ComplLat]
PreservMonoidTrans [in HOcore.ComplLat]
process [in HOcore.HoCore]


S

step_var_rem [in HOcore.HoCore]
step_var_cxt [in HOcore.HoCore]
step_tau [in HOcore.HoCore]
step_in [in HOcore.HoCore]
step_out [in HOcore.HoCore]
SymFun [in HOcore.ComplLat]



Instance Index

A

and_dec [in Base.Base]
app_equi_proper [in Base.Base]
app_incl_proper [in Base.Base]


B

bij_ren_clos_symmetric [in HOcore.Ren]
bij_ren_clos_mono [in HOcore.Ren]
bool_eq_dec [in Base.Base]


C

card_equi_proper [in Base.Base]
companion_compat [in HOcore.Compat]
companion_mono [in HOcore.Compat]
compose_preserv_ext [in HOcore.ComplLat]
compose_preserv_symmetric_fun [in HOcore.ComplLat]
compose_preserv_mono [in HOcore.ComplLat]
congr_cond_clos_impl_cond_clos [in HOcore.BisCongr]
const_to_postfp_cond_clos [in HOcore.CondClos]
const_top2_sym [in HOcore.ComplLat]
const_bot2_sym [in HOcore.ComplLat]
const_sym [in HOcore.ComplLat]
const_to_x_mono [in HOcore.ComplLat]
const_to_postfp_compat [in HOcore.Compat]
cons_equi_proper [in Base.Base]
cons_incl_proper [in Base.Base]


D

decidable_inj_ren_clos_ext [in HOcore.Ren]
decidable_inj_ren_clos_symmetric [in HOcore.Ren]
decidable_inj_ren_clos_mono [in HOcore.Ren]
decreasify_preserv_mono [in HOcore.ComplLat]
decreasing_g_up_preserv_cond_clos [in HOcore.CondClos]


E

equi_Equivalence [in Base.Base]


F

False_dec [in Base.Base]
f_reach_sym [in HOcore.InclIoMultiBisIoCxtBis]
f_reach_mono [in HOcore.InclIoMultiBisIoCxtBis]


H

ho_in_substit_cond_clos [in HOcore.BisSubstit]
ho_out_substit_cond_clos [in HOcore.BisSubstit]


I

Ids_process [in HOcore.HoCore]
id_cond_clos [in HOcore.CondClos]
id_sym [in HOcore.ComplLat]
id_mono [in HOcore.ComplLat]
id_compat [in HOcore.Compat]
iff_dec [in Base.Base]
impl_dec [in Base.Base]
incl_equi_proper [in Base.Base]
incl_preorder [in Base.Base]
increasify_impl_ext [in HOcore.ComplLat]
increasify_preserv_sym [in HOcore.ComplLat]
increasify_preserv_mono [in HOcore.ComplLat]
increasing_g_lo_preserv_cond_clos [in HOcore.CondClos]
inj_ren_clos_symmetric [in HOcore.Ren]
inj_ren_clos_compat_for_s_var_multi [in HOcore.BisDecInjRen]
inj_ren_clos_compat_for_s_var_cxt [in HOcore.BisDecInjRen]
inj_ren_clos_compat_for_s_ho_in [in HOcore.BisDecInjRen]
inj_ren_clos_compat_for_s_ho_out [in HOcore.BisDecInjRen]
intersect_fun_bin_preserv_cond_clos [in HOcore.CondClos]
intersect_fun_bin_preserv_preserv_monoid_trans [in HOcore.ComplLat]
intersect_fun_bin_preserv_preserv_monoid_refl [in HOcore.ComplLat]
intersect_fun_bin_preserv_mono [in HOcore.ComplLat]
intersect_fun_bin_preserv_compat [in HOcore.Compat]
in_equi_proper [in Base.Base]
in_incl_proper [in Base.Base]


L

list_exists_dec [in Base.Base]
list_forall_dec [in Base.Base]
list_in_dec [in Base.Base]
list_eq_dec [in Base.Base]


M

monotonized_mono [in HOcore.ComplLat]


N

nat_le_dec [in Base.Base]
nat_eq_dec [in Base.Base]
not_dec [in Base.Base]


O

or_dec [in Base.Base]


P

par_clos_sym [in HOcore.BisCongr]
par_clos_mono [in HOcore.BisCongr]
preserv_trans_impl_rel_comp_fun_preserv_cond_clos [in HOcore.CondClos]
preserv_trans_impl_rel_comp_fun_preserv_compat [in HOcore.Compat]


R

receive_clos_sym [in HOcore.BisCongr]
receive_clos_mono [in HOcore.BisCongr]
refl_clos_sym [in HOcore.ComplLat]
refl_clos_mono [in HOcore.ComplLat]
rel_comp_fun_preserv_mono [in HOcore.ComplLat]
rel_fun_equiv_intersect_fun_bin_morphism [in HOcore.ComplLat]
rel_fun_equiv_equivalence [in HOcore.ComplLat]
rel_equiv_equivalence [in HOcore.ComplLat]
Rename_process [in HOcore.HoCore]


S

send_clos_sym [in HOcore.BisCongr]
send_clos_mono [in HOcore.BisCongr]
SubstLemmas_process [in HOcore.HoCore]
subst_clos_ext [in HOcore.Subst]
subst_clos_symmetric [in HOcore.Subst]
subst_clos_mono [in HOcore.Subst]
Subst_process [in HOcore.HoCore]
symmetrize_fun_preserv_cond_clos_when_f_sym [in HOcore.CondClos]
symmetrize_fun_preserv_preserv_monoid_trans [in HOcore.ComplLat]
symmetrize_fun_preserv_preserv_monoid_refl [in HOcore.ComplLat]
symmetrize_fun_preserv_mono [in HOcore.ComplLat]
symmetrize_fun_correct [in HOcore.ComplLat]
symmetrize_fun_preserv_compat_when_f_sym [in HOcore.Compat]
s_var_multi_preserv_monoid_trans [in HOcore.Bis]
s_var_cxt_preserv_monoid_trans [in HOcore.Bis]
s_ho_in_preserv_monoid_trans [in HOcore.Bis]
s_ho_out_preserv_monoid_trans [in HOcore.Bis]
s_tau_preserv_monoid_trans [in HOcore.Bis]
s_var_multi_preserv_monoid_refl [in HOcore.Bis]
s_var_cxt_preserv_monoid_refl [in HOcore.Bis]
s_ho_in_preserv_monoid_refl [in HOcore.Bis]
s_ho_out_preserv_monoid_refl [in HOcore.Bis]
s_tau_preserv_monoid_refl [in HOcore.Bis]
s_io_cxt_sym_mono [in HOcore.Bis]
s_io_cxt_mono [in HOcore.Bis]
s_var_multi_mono [in HOcore.Bis]
s_var_cxt_mono [in HOcore.Bis]
s_var_rem_mono [in HOcore.Bis]
s_ho_in_mono [in HOcore.Bis]
s_ho_out_mono [in HOcore.Bis]
s_tau_mono [in HOcore.Bis]
s_var_multi_fulfills_cond_compat_for_par_clos [in HOcore.BisCongr]
s_var_cxt_fulfills_cond_compat_for_par_clos [in HOcore.BisCongr]
s_ho_in_fulfills_cond_compat_for_par_clos [in HOcore.BisCongr]
s_ho_out_fulfills_cond_compat_for_par_clos [in HOcore.BisCongr]
s_var_multi_fulfills_cond_compat_for_receive_clos [in HOcore.BisCongr]
s_var_cxt_fulfills_cond_compat_for_receive_clos [in HOcore.BisCongr]
s_ho_in_fulfills_cond_compat_for_receive_clos [in HOcore.BisCongr]
s_ho_out_fulfills_cond_compat_for_receive_clos [in HOcore.BisCongr]
s_var_multi_fulfills_cond_compat_for_send_clos [in HOcore.BisCongr]
s_var_cxt_fulfills_cond_compat_for_send_clos [in HOcore.BisCongr]
s_ho_in_fulfills_cond_compat_for_send_clos [in HOcore.BisCongr]
s_ho_out_fulfills_cond_compat_for_send_clos [in HOcore.BisCongr]


T

transp_fun_preserv_cond_clos_when_f_sym [in HOcore.CondClos]
transp_fun_bin_preserv_cond_clos [in HOcore.CondClos]
transp_fun_preserv_mono [in HOcore.ComplLat]
transp_mono [in HOcore.ComplLat]
transp_fun_preserv_compat_when_f_sym [in HOcore.Compat]
transp_fun_bin_preserv_compat [in HOcore.Compat]
True_dec [in Base.Base]


U

union_fun_bin_preserv_cond_clos [in HOcore.CondClos]
union_fun_bin_preserv_ext_left [in HOcore.ComplLat]
union_fun_bin_preserv_sym_fun [in HOcore.ComplLat]
union_fun_bin_preserv_mono [in HOcore.ComplLat]
union_fun_bin_preserv_compat [in HOcore.Compat]
up_to_nu_f_is_nu_f_compat [in HOcore.UpToNu]
up_to_nu_preserv_symmetric_fun [in HOcore.UpToNu]
up_to_nu_preserv_mono [in HOcore.UpToNu]


V

var_multi_substit_cond_clos [in HOcore.BisSubstit]
var_substit_cond_clos [in HOcore.BisSubstit]



Section Index

C

Cardinality [in Base.Base]
Compat [in HOcore.Compat]
Compat.CompatImplSound [in HOcore.Compat]
CompleteLattice [in HOcore.ComplLat]
CompleteLattice.Map [in HOcore.ComplLat]
CompleteLattice.PreservMonoidProperties [in HOcore.ComplLat]
CondClos [in HOcore.CondClos]
CongrCondClos [in HOcore.BisCongr]


D

Dupfree [in Base.Base]


E

Equi [in Base.Base]


F

FCI.FCI [in Base.Base]
FilterComm [in Base.Base]
FilterLemmas [in Base.Base]
FilterLemmas_pq [in Base.Base]


I

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


M

Membership [in Base.Base]


P

PowerRep [in Base.Base]


R

Removal [in Base.Base]


U

Undup [in Base.Base]
UpToNu [in HOcore.UpToNu]



Abbreviation Index

B

bot2 [in HOcore.Prelim]


T

top2 [in HOcore.Prelim]



Definition Index

B

bij_ren_clos [in HOcore.Ren]
bij_ren [in HOcore.Ren]


C

card [in Base.Base]
chan [in HOcore.HoCore]
companion [in HOcore.Compat]
congruence [in HOcore.ComplLat]
context_clos [in HOcore.IoCxtBis]
correct [in HOcore.ComplLat]
count [in HOcore.Multiset]


D

dec [in Base.Base]
decidable_inj_ren_clos [in HOcore.Ren]
decidable_inj_ren [in HOcore.Ren]
decision [in Base.Base]
decreasify [in HOcore.ComplLat]
disjoint [in Base.Base]
dupfree_inv [in Base.Base]


E

equi [in Base.Base]


F

FCI.C [in Base.Base]
FCI.F [in Base.Base]
filter [in Base.Base]
fin_sum [in HOcore.Multiset]
FP [in Base.Base]
f_reach [in HOcore.InclIoMultiBisIoCxtBis]


I

inclp [in Base.Base]
increasify [in HOcore.ComplLat]
inj_ren_clos [in HOcore.Ren]
instantiate' [in HOcore.HoCore]
intersect [in HOcore.ComplLat]
intersect_fun_bin [in HOcore.ComplLat]
intersect_bin [in HOcore.ComplLat]
intersect_fun_preserv_mono [in HOcore.ComplLat]
intersect_fun [in HOcore.ComplLat]
it [in Base.Base]


M

minus_one [in HOcore.Ren]
mle [in HOcore.Multiset]
monotone2 [in HOcore.ComplLat]
monotonize [in HOcore.ComplLat]
mult [in HOcore.Multiset]
multiset [in HOcore.Multiset]
multi_context_clos [in HOcore.IoCxtBis]


N

nat_dec [in HOcore.Multiset]
nu [in HOcore.ComplLat]


P

par_clos [in HOcore.BisCongr]
postfp [in HOcore.ComplLat]
power [in Base.Base]
prefp [in HOcore.ComplLat]


R

receive_clos [in HOcore.BisCongr]
refl_clos [in HOcore.ComplLat]
rel_comp_fun [in HOcore.ComplLat]
rel_comp [in HOcore.ComplLat]
rel_fun_equiv [in HOcore.ComplLat]
rel_fun_incl [in HOcore.ComplLat]
rel_equiv [in HOcore.ComplLat]
rem [in Base.Base]
rep [in Base.Base]


S

send_clos [in HOcore.BisCongr]
sound [in HOcore.ComplLat]
subst_clos [in HOcore.Subst]
symmetrize_fun [in HOcore.ComplLat]
s_var_multi [in HOcore.Bis]
s_var_rem [in HOcore.Bis]
s_var_cxt [in HOcore.Bis]
s_ho_in [in HOcore.Bis]
s_ho_out [in HOcore.Bis]
s_tau [in HOcore.Bis]


T

transp_fun [in HOcore.ComplLat]


U

undup [in Base.Base]
union [in HOcore.ComplLat]
union_fun_bin [in HOcore.ComplLat]
union_fun [in HOcore.ComplLat]
up_to_nu [in HOcore.UpToNu]



Record Index

C

Compat [in HOcore.Compat]
CondClos [in HOcore.CondClos]
CongrCondClos [in HOcore.BisCongr]


E

Ext [in HOcore.ComplLat]


M

Mono [in HOcore.ComplLat]


P

PreservMonoidRefl [in HOcore.ComplLat]
PreservMonoidTrans [in HOcore.ComplLat]


S

SymFun [in HOcore.ComplLat]



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 (593 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 (32 entries)
Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (1 entry)
Variable Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (21 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 (19 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 (225 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 (31 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 (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 (15 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 (139 entries)
Section Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (21 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 (2 entries)
Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ other (71 entries)
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)