| 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
BaseBis
BisCongr
BisDecInjRen
BisSubstit
C
CompatComplLat
CondClos
H
HoCoreI
InclIoCxtBisIoRemBisInclIoMultiBisIoCxtBis
InclIoRemBisIoMultiBis
IoCxtBis
IoMultiBis
M
MultisetP
PrelimR
RenS
SubstU
UpToNuLemma 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) |