| 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 | (1611 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 | (35 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (22 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 | (30 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 | (1098 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 | (126 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 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 | (48 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 | (2 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 | (28 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (17 entries) |
| 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 | (199 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 | (1 entry) |
Global Index
A
AA [constructor, in HOC04DefLTS]Abs [definition, in HOC01Defs]
AbsPar1 [constructor, in HOC04DefLTS]
AbsPar2 [constructor, in HOC04DefLTS]
AbsPure [constructor, in HOC04DefLTS]
abstraction [inductive, in HOC04DefLTS]
Abs_from_Receive_spec [lemma, in HOC22Decidability]
Abs_from_Receive [definition, in HOC22Decidability]
abs_subst [definition, in HOC22Decidability]
abs_not_prime [lemma, in HOC25Axiomatization]
Abs_eq [lemma, in HOC03CanonicalLemmas]
abs_wfcgr_no_nil [lemma, in HOC10CongrLemmas]
abs_wfcgr_inv [lemma, in HOC10CongrLemmas]
abs_core_wfcgr [lemma, in HOC10CongrLemmas]
act1_tau [lemma, in HOC11TransLemmas]
act1_rem [lemma, in HOC11TransLemmas]
act1_out [lemma, in HOC11TransLemmas]
act1_in [lemma, in HOC11TransLemmas]
act2_tau [lemma, in HOC11TransLemmas]
act2_rem [lemma, in HOC11TransLemmas]
act2_out [lemma, in HOC11TransLemmas]
act2_in [lemma, in HOC11TransLemmas]
agent [inductive, in HOC04DefLTS]
AP [constructor, in HOC04DefLTS]
async_barbed_to_order_oiv [lemma, in HOC27BarbedRevisited]
async_barbed_out_1 [lemma, in HOC27BarbedRevisited]
async_barbed_out_normal_early [lemma, in HOC27BarbedRevisited]
async_barbed_swap [lemma, in HOC27BarbedRevisited]
async_barbed_swap_fresh [lemma, in HOC27BarbedRevisited]
async_barbed_congr_abs_inv [lemma, in HOC27BarbedRevisited]
async_barbed_congr_send_inv [lemma, in HOC27BarbedRevisited]
async_barbed_congr_par [lemma, in HOC27BarbedRevisited]
async_barbed_congr_par_r [lemma, in HOC27BarbedRevisited]
async_barbed_congr_par_l [lemma, in HOC27BarbedRevisited]
async_barbed_congr_abs [lemma, in HOC27BarbedRevisited]
async_barbed_congr_send [lemma, in HOC27BarbedRevisited]
async_barbed_congr_par_assoc_r [lemma, in HOC27BarbedRevisited]
async_barbed_congr_par_assoc_l [lemma, in HOC27BarbedRevisited]
async_barbed_congr_par_com [lemma, in HOC27BarbedRevisited]
async_barbed_congr_nil_r [lemma, in HOC27BarbedRevisited]
async_barbed_congr_nil_l [lemma, in HOC27BarbedRevisited]
async_barbed_refl [instance, in HOC27BarbedRevisited]
async_barbed_trans [instance, in HOC20Barbed]
async_barbed_out_barb_preserving [lemma, in HOC20Barbed]
async_barbed_context_closed [lemma, in HOC20Barbed]
async_barbed_tau [lemma, in HOC20Barbed]
async_barbed_sym [instance, in HOC20Barbed]
async_barbed [definition, in HOC20Barbed]
async_barbed_relation [definition, in HOC20Barbed]
aux [library]
aux_fresh_rem [lemma, in HOC19Coincide]
B
Basic [section, in LibFsetExt]Basic.A [variable, in LibFsetExt]
bio [definition, in HOC22Decidability]
bio_ok [lemma, in HOC22Decidability]
bio_aux_ok2 [lemma, in HOC22Decidability]
bio_aux_ok1 [lemma, in HOC22Decidability]
bio_aux [definition, in HOC22Decidability]
C
CAbs [constructor, in HOC20Barbed]CAbs [constructor, in HOC04DefLTS]
CAbsPar1 [constructor, in HOC04DefLTS]
CAbsPar2 [constructor, in HOC04DefLTS]
cfresh_NORbis [lemma, in HOC17NORbis]
cfresh_send_nil [lemma, in HOC02BaseLemmas]
cfresh_nil [lemma, in HOC02BaseLemmas]
cfresh_par_iff [lemma, in HOC02BaseLemmas]
cfresh_gvar [lemma, in HOC02BaseLemmas]
cfresh_lvar [lemma, in HOC02BaseLemmas]
cfresh_receive [lemma, in HOC02BaseLemmas]
cfresh_send [lemma, in HOC02BaseLemmas]
cfresh_iter_abs_par [lemma, in HOC18ONORbis]
cfresh_ONORbis [lemma, in HOC18ONORbis]
chan [definition, in HOC01Defs]
change_channel [lemma, in HOC15HObis]
change_NOR_channel [lemma, in HOC17NORbis]
chan_gen_spec [lemma, in HOC01Defs]
chan_gen [definition, in HOC01Defs]
chan_gen_list_spec [lemma, in HOC01Defs]
chan_gen_list [definition, in HOC01Defs]
CHole [constructor, in HOC20Barbed]
CHS [definition, in HOC01Defs]
CHSs [definition, in HOC01Defs]
closed_relation [definition, in HOC13Bisimulations]
closed_proc_list_wfp [definition, in HOC05WFProcesses]
closed_proc_list [definition, in HOC01Defs]
closed_process [definition, in HOC01Defs]
combine_count_2_snd [lemma, in LibListExt]
combine_count_2_fst [lemma, in LibListExt]
combine_remdup_count_snd [lemma, in LibListExt]
combine_remdup_count_fst [lemma, in LibListExt]
combine_remdup_snd [lemma, in LibListExt]
combine_remdup_snd_iff [lemma, in LibListExt]
combine_remdup_fst_iff [lemma, in LibListExt]
combine_exists_snd [lemma, in LibListExt]
combine_exists_fst [lemma, in LibListExt]
combine_nodup_pair_unique_snd [lemma, in LibListExt]
combine_nodup_pair_unique_fst [lemma, in LibListExt]
combine_equal_inv [lemma, in LibListExt]
combine_equal_inv_r [lemma, in LibListExt]
combine_equal_inv_l [lemma, in LibListExt]
combine_inv [lemma, in LibListExt]
combine_split [lemma, in LibListExt]
completeness_lr [lemma, in HOC25Axiomatization]
components [definition, in HOC24PreCompleteness]
components_eq_nil [lemma, in HOC24PreCompleteness]
components_eq_par [lemma, in HOC24PreCompleteness]
components_eq_gvar [lemma, in HOC24PreCompleteness]
components_eq_abs [lemma, in HOC24PreCompleteness]
components_eq_send [lemma, in HOC24PreCompleteness]
components_eq [lemma, in HOC24PreCompleteness]
components_wfp_prod [lemma, in HOC25Axiomatization]
CONbis [definition, in HOC13Bisimulations]
CONbisC [definition, in HOC13Bisimulations]
CONbisC_closed [lemma, in HOC16CONbis]
CONbisC_out_context [lemma, in HOC16CONbis]
CONbisC_tau [lemma, in HOC16CONbis]
CONbisC_sym [lemma, in HOC16CONbis]
CONbisC_out_normal [lemma, in HOC19Coincide]
CONbisC_in_normal [lemma, in HOC19Coincide]
CONbisE [definition, in HOC13Bisimulations]
CONbisE_NORbisE [lemma, in HOC19Coincide]
CONbis_closed [lemma, in HOC16CONbis]
CONbis_out_context [lemma, in HOC16CONbis]
CONbis_tau [lemma, in HOC16CONbis]
CONbis_sym [lemma, in HOC16CONbis]
CONbis_NORbis [lemma, in HOC19Coincide]
CONbis_CONbis [lemma, in HOC19Coincide]
congr_async_barbed [lemma, in HOC27BarbedRevisited]
congr_async_barbed_relation [lemma, in HOC27BarbedRevisited]
congr_out_barb_preserving [lemma, in HOC27BarbedRevisited]
congr_context_closed [lemma, in HOC27BarbedRevisited]
congr_CONbisimulation [lemma, in HOC13Bisimulations]
congr_ONORbisimulation [lemma, in HOC13Bisimulations]
congr_NORbisimulation [lemma, in HOC13Bisimulations]
congr_HObisimulation [lemma, in HOC13Bisimulations]
congr_IObisimulation [lemma, in HOC13Bisimulations]
congr_out_context [lemma, in HOC13Bisimulations]
congr_out_context_strong [lemma, in HOC13Bisimulations]
congr_closed [lemma, in HOC13Bisimulations]
congr_in_normal [lemma, in HOC13Bisimulations]
congr_out_normal [lemma, in HOC13Bisimulations]
congr_out_normal_strong [lemma, in HOC13Bisimulations]
congr_tau [lemma, in HOC13Bisimulations]
congr_rem [lemma, in HOC13Bisimulations]
congr_out [lemma, in HOC13Bisimulations]
congr_in [lemma, in HOC13Bisimulations]
congr_in_strong [lemma, in HOC13Bisimulations]
congr_swap [lemma, in HOC10CongrLemmas]
congr_IObis [lemma, in HOC14IObis]
const_abs_decidable [instance, in HOC04DefLTS]
const_abs_dec [definition, in HOC04DefLTS]
const_abs [inductive, in HOC04DefLTS]
context [inductive, in HOC20Barbed]
Context_bisimulation [definition, in HOC13Bisimulations]
context_closed [definition, in HOC20Barbed]
Core [definition, in HOC10CongrLemmas]
core_remove_par_nils [lemma, in HOC24PreCompleteness]
core_none_char [lemma, in HOC24PreCompleteness]
core_remove_nil_invariant [lemma, in HOC24PreCompleteness]
core_norm_full_none [lemma, in HOC25Axiomatization]
core_norm_full_gvar [lemma, in HOC25Axiomatization]
core_norm_full_send [lemma, in HOC25Axiomatization]
core_par_assoc_r [lemma, in HOC10CongrLemmas]
core_par_assoc_l [lemma, in HOC10CongrLemmas]
core_par_com [lemma, in HOC10CongrLemmas]
core_par_sizeP_0 [lemma, in HOC10CongrLemmas]
core_eq_par [lemma, in HOC10CongrLemmas]
core_eq_nil [lemma, in HOC10CongrLemmas]
core_eq_gvar [lemma, in HOC10CongrLemmas]
core_eq_abs [lemma, in HOC10CongrLemmas]
core_eq_send [lemma, in HOC10CongrLemmas]
Core_eq [lemma, in HOC10CongrLemmas]
Count [section, in LibListExt]
count [definition, in LibListExt]
count_length [lemma, in LibListExt]
count_removeOne_neg [lemma, in LibListExt]
count_removeOne_pos [lemma, in LibListExt]
count_app_plus [lemma, in LibListExt]
count_Mem [lemma, in LibListExt]
count_cons_cancel [lemma, in LibListExt]
count_cons_pos [lemma, in LibListExt]
count_nil [lemma, in LibListExt]
Count.A [variable, in LibListExt]
CParL [constructor, in HOC20Barbed]
CParR [constructor, in HOC20Barbed]
cp_subst_dist [lemma, in HOC11TransLemmas]
cp_trans_tau [lemma, in HOC09GVLemmas]
cp_trans_out [lemma, in HOC09GVLemmas]
cp_trans_in [lemma, in HOC09GVLemmas]
cp_abs [lemma, in HOC09GVLemmas]
cp_par [lemma, in HOC09GVLemmas]
CSend [constructor, in HOC20Barbed]
D
dec_nf_classic [instance, in HOC25Axiomatization]deep_prime_decomposition_unique [lemma, in HOC24PreCompleteness]
deep_prime_decomposition_exists [lemma, in HOC24PreCompleteness]
deep_prime_decomposition [definition, in HOC24PreCompleteness]
Defs [section, in LibListExt]
Defs.A [variable, in LibListExt]
Defs.B [variable, in LibListExt]
dpd [definition, in HOC24PreCompleteness]
dpd_remove_par_nils [lemma, in HOC24PreCompleteness]
dpd_components_prime [lemma, in HOC24PreCompleteness]
dpd_congr_invariant [lemma, in HOC24PreCompleteness]
dpd_equiv_par_nil [lemma, in HOC24PreCompleteness]
dpd_remove_nil_congr [lemma, in HOC24PreCompleteness]
dpd_implies_pd [lemma, in HOC24PreCompleteness]
dpd_eq_abs [lemma, in HOC24PreCompleteness]
dpd_gswap [lemma, in HOC24PreCompleteness]
dpd_eq_nil [lemma, in HOC24PreCompleteness]
dpd_eq_par [lemma, in HOC24PreCompleteness]
dpd_eq_gvar [lemma, in HOC24PreCompleteness]
dpd_eq_send [lemma, in HOC24PreCompleteness]
dpd_eq [lemma, in HOC24PreCompleteness]
dpd_wfp_prod_app [lemma, in HOC25Axiomatization]
dpd_components_normal_form [lemma, in HOC25Axiomatization]
dpd_normal_form [lemma, in HOC25Axiomatization]
dpd_no_red_base [lemma, in HOC25Axiomatization]
E
E [definition, in HOC02BaseLemmas]ECngr [constructor, in HOC25Axiomatization]
ECore [constructor, in HOC25Axiomatization]
empty_dec [lemma, in LibFsetExt]
EParLeft [constructor, in HOC25Axiomatization]
EParRight [constructor, in HOC25Axiomatization]
EReceive [constructor, in HOC25Axiomatization]
ESend [constructor, in HOC25Axiomatization]
ESym [constructor, in HOC25Axiomatization]
ETrans [constructor, in HOC25Axiomatization]
extended_congruence [inductive, in HOC25Axiomatization]
ext_cgr_red [lemma, in HOC25Axiomatization]
ext_cgr_trans [instance, in HOC25Axiomatization]
ext_cgr_sym [instance, in HOC25Axiomatization]
ext_cgr_refl [instance, in HOC25Axiomatization]
ext_cgr_asymmetric [lemma, in HOC25Axiomatization]
ext_cgr_irreflexive [lemma, in HOC25Axiomatization]
ext_cgr_full_measure [lemma, in HOC25Axiomatization]
ext_cgr_step_measure [lemma, in HOC25Axiomatization]
ext_cgr_full_remove_par_nils [lemma, in HOC25Axiomatization]
ext_cgr_step_remove_par_nils [lemma, in HOC25Axiomatization]
ext_cgr_full_remove_par_nils_rr_lr [lemma, in HOC25Axiomatization]
ext_cgr_step_remove_par_nils_rr_eq [lemma, in HOC25Axiomatization]
ext_cgr_full [definition, in HOC25Axiomatization]
ext_cgr_step [definition, in HOC25Axiomatization]
ex_fresh_gvar [lemma, in HOC01Defs]
E_subst_inv [lemma, in HOC02BaseLemmas]
F
f [definition, in HOC03CanonicalLemmas]false_trans_rem [lemma, in HOC11TransLemmas]
false_trans_out [lemma, in HOC11TransLemmas]
false_trans_in [lemma, in HOC11TransLemmas]
fill [definition, in HOC20Barbed]
find_fresh_chan_n [lemma, in HOC01Defs]
find_fresh_chan [lemma, in HOC01Defs]
find_fresh [lemma, in HOC01Defs]
Forall_subset [lemma, in LibListExt]
Forall_mem [lemma, in LibListExt]
Forall_forall [lemma, in LibListExt]
Forall_Mem [lemma, in LibListExt]
fresh_gvar_swap_chan [lemma, in HOC09GVLemmas]
fresh_LV [lemma, in HOC02BaseLemmas]
fresh_GV [lemma, in HOC02BaseLemmas]
fresh_iter_abs_par [lemma, in HOC18ONORbis]
fresh_CHSs [lemma, in HOC01Defs]
fresh_chan_decidable [instance, in HOC01Defs]
fresh_chan_dec [definition, in HOC01Defs]
fresh_chan [definition, in HOC01Defs]
fresh_set [lemma, in HOC01Defs]
fresh_lvar_decidable [instance, in HOC01Defs]
fresh_lvar_dec [definition, in HOC01Defs]
fresh_lvar [definition, in HOC01Defs]
fresh_gvar_decidable [instance, in HOC01Defs]
fresh_gvar_dec [definition, in HOC01Defs]
fresh_gvar [definition, in HOC01Defs]
FromList [section, in LibFsetExt]
FromList.A [variable, in LibFsetExt]
from_to_list_union [lemma, in LibListExt]
from_to_list [axiom, in LibListExt]
from_list_rem1 [lemma, in LibListExt]
from_list_app [lemma, in LibFsetExt]
from_list_base [lemma, in LibFsetExt]
from_list_spec [lemma, in LibFsetExt]
from_list_notin [lemma, in LibFsetExt]
from_union_to_rem [lemma, in LibFsetExt]
from_rem_to_union [lemma, in LibFsetExt]
fset_nodup [lemma, in LibListExt]
fset_eq_sub [lemma, in LibFsetExt]
fset_neq [lemma, in LibFsetExt]
fset_extens_iff [axiom, in LibFsetExt]
fst_split [lemma, in LibListExt]
fst_split_step [lemma, in LibListExt]
fst_split_cons [lemma, in LibListExt]
f_is_good [lemma, in HOC03CanonicalLemmas]
G
get_Abs_from_Receive [lemma, in HOC22Decidability]get_components [definition, in HOC25Axiomatization]
get_ins_wfp_prod_app [lemma, in HOC25Axiomatization]
get_outs_wfp_prod_app [lemma, in HOC25Axiomatization]
get_vars_wfp_prod_app [lemma, in HOC25Axiomatization]
get_ins_sizeP [lemma, in HOC25Axiomatization]
get_outs_sizeP [lemma, in HOC25Axiomatization]
get_vars_sizeP [lemma, in HOC25Axiomatization]
get_ins_spec [lemma, in HOC25Axiomatization]
get_ins_eq_nil [lemma, in HOC25Axiomatization]
get_ins_eq_par [lemma, in HOC25Axiomatization]
get_ins_eq_gvar [lemma, in HOC25Axiomatization]
get_ins_eq_abs [lemma, in HOC25Axiomatization]
get_ins_eq_send [lemma, in HOC25Axiomatization]
get_ins_eq [lemma, in HOC25Axiomatization]
get_ins [definition, in HOC25Axiomatization]
get_outs_spec [lemma, in HOC25Axiomatization]
get_outs_eq_nil [lemma, in HOC25Axiomatization]
get_outs_eq_par [lemma, in HOC25Axiomatization]
get_outs_eq_gvar [lemma, in HOC25Axiomatization]
get_outs_eq_abs [lemma, in HOC25Axiomatization]
get_outs_eq_send [lemma, in HOC25Axiomatization]
get_outs_eq [lemma, in HOC25Axiomatization]
get_outs [definition, in HOC25Axiomatization]
get_vars_spec [lemma, in HOC25Axiomatization]
get_vars_eq_nil [lemma, in HOC25Axiomatization]
get_vars_eq_par [lemma, in HOC25Axiomatization]
get_vars_eq_gvar [lemma, in HOC25Axiomatization]
get_vars_eq_abs [lemma, in HOC25Axiomatization]
get_vars_eq_send [lemma, in HOC25Axiomatization]
get_vars_eq [lemma, in HOC25Axiomatization]
get_vars [definition, in HOC25Axiomatization]
gfresh_E_empty [lemma, in HOC02BaseLemmas]
gfresh_subst_involutive [lemma, in HOC02BaseLemmas]
gfresh_subst_is_swap [lemma, in HOC02BaseLemmas]
gfresh_swap_inv [lemma, in HOC02BaseLemmas]
gfresh_swap_rewrite [lemma, in HOC02BaseLemmas]
gfresh_subst_rewrite [lemma, in HOC02BaseLemmas]
gfresh_in_self_subst [lemma, in HOC02BaseLemmas]
gfresh_in_lsubst_p_q [lemma, in HOC02BaseLemmas]
gfresh_in_subst_p_q [lemma, in HOC02BaseLemmas]
gfresh_from_lsubst [lemma, in HOC02BaseLemmas]
gfresh_from_subst [lemma, in HOC02BaseLemmas]
gfresh_nil [lemma, in HOC02BaseLemmas]
gfresh_par_iff [lemma, in HOC02BaseLemmas]
gfresh_gvar [lemma, in HOC02BaseLemmas]
gfresh_lvar [lemma, in HOC02BaseLemmas]
gfresh_receive [lemma, in HOC02BaseLemmas]
gfresh_send [lemma, in HOC02BaseLemmas]
gfresh_ONORbis [lemma, in HOC18ONORbis]
gfresh_IObis [lemma, in HOC14IObis]
good [definition, in HOC03CanonicalLemmas]
GoodF [definition, in HOC03CanonicalLemmas]
GoodFresh [lemma, in HOC03CanonicalLemmas]
GoodFresh_iff [lemma, in HOC03CanonicalLemmas]
Good_chan_swap [lemma, in HOC03CanonicalLemmas]
Good0 [lemma, in HOC03CanonicalLemmas]
guarded [inductive, in HOC12Guarded]
guarded_decidable [instance, in HOC12Guarded]
guarded_size_unguardedX [lemma, in HOC12Guarded]
guarded_proc [definition, in HOC12Guarded]
guarding_HObisE [lemma, in HOC15HObis]
GuGvar [constructor, in HOC12Guarded]
GuNil [constructor, in HOC12Guarded]
GuPar [constructor, in HOC12Guarded]
GuReceive [constructor, in HOC12Guarded]
GuSend [constructor, in HOC12Guarded]
GV [definition, in HOC01Defs]
Gvar [constructor, in HOC01Defs]
gvar_wfcgr_inv [lemma, in HOC10CongrLemmas]
gvar_core_wfcgr [lemma, in HOC10CongrLemmas]
gvar_list [definition, in HOC01Defs]
GV_union_included [lemma, in HOC22Decidability]
GV_union [definition, in HOC22Decidability]
GV_trans_tau [lemma, in HOC09GVLemmas]
GV_trans_rem2 [lemma, in HOC09GVLemmas]
GV_trans_rem1 [lemma, in HOC09GVLemmas]
GV_trans_out [lemma, in HOC09GVLemmas]
GV_trans_in_sub [lemma, in HOC09GVLemmas]
GV_trans_in [lemma, in HOC09GVLemmas]
GV_trans_in_const [lemma, in HOC09GVLemmas]
GV_subst_cp [lemma, in HOC09GVLemmas]
GV_swap_chan [lemma, in HOC09GVLemmas]
GV_swap [lemma, in HOC09GVLemmas]
GV_subst [lemma, in HOC02BaseLemmas]
GV_set [definition, in HOC01Defs]
H
has_top_nil_num_of_pars_ordered [lemma, in HOC25Axiomatization]has_top_nil_sizeP_0 [lemma, in HOC25Axiomatization]
has_top_nil_ordered [lemma, in HOC25Axiomatization]
has_top_nil_get_ins [lemma, in HOC25Axiomatization]
has_top_nil_get_outs [lemma, in HOC25Axiomatization]
has_top_nil_get_vars [lemma, in HOC25Axiomatization]
has_top_nil_wfp_prod_app [lemma, in HOC25Axiomatization]
has_free_par_nil_par [lemma, in HOC25Axiomatization]
has_free_par_nil_abs [lemma, in HOC10CongrLemmas]
has_free_par_nil_lsubst [lemma, in HOC10CongrLemmas]
has_top_has_free_nil [lemma, in HOC10CongrLemmas]
has_free_par_nil [definition, in HOC10CongrLemmas]
has_top_nil_sizeP_0 [lemma, in HOC10CongrLemmas]
has_top_nil_eq_nil [lemma, in HOC10CongrLemmas]
has_top_nil_eq_par [lemma, in HOC10CongrLemmas]
has_top_nil_eq_gvar [lemma, in HOC10CongrLemmas]
has_top_nil_eq_abs [lemma, in HOC10CongrLemmas]
has_top_nil_eq_send [lemma, in HOC10CongrLemmas]
has_top_nil_eq [lemma, in HOC10CongrLemmas]
has_top_nil [definition, in HOC10CongrLemmas]
height_fun [definition, in HOC01Defs]
HigherOrder_bisimulation [definition, in HOC13Bisimulations]
HObicC_var [lemma, in HOC15HObis]
HObis [definition, in HOC13Bisimulations]
HObisC [definition, in HOC13Bisimulations]
HObisC_trans [lemma, in HOC15HObis]
HObisC_closed [lemma, in HOC15HObis]
HObisC_out [lemma, in HOC15HObis]
HObisC_tau [lemma, in HOC15HObis]
HObisC_sym [lemma, in HOC15HObis]
HObisC_out_context [lemma, in HOC19Coincide]
HObisE [definition, in HOC13Bisimulations]
HObisE_Msubst [lemma, in HOC15HObis]
HObisE_subst [lemma, in HOC15HObis]
HObisE_sym [lemma, in HOC15HObis]
HObisE_equiv [lemma, in HOC15HObis]
HObisE_CONbisE [lemma, in HOC19Coincide]
HObisE_unguardeds_eq [lemma, in HOC19Coincide]
HObisE_IObis [lemma, in HOC19Coincide]
HObisR_r [lemma, in HOC15HObis]
HObisR_ch [lemma, in HOC15HObis]
HObis_congr_send [lemma, in HOC15HObis]
HObis_congr_abs [lemma, in HOC15HObis]
HObis_congr_par_nil [lemma, in HOC15HObis]
HObis_is_eq_rel [instance, in HOC15HObis]
HObis_trans [lemma, in HOC15HObis]
HObis_congr_receive [lemma, in HOC15HObis]
HObis_closed [lemma, in HOC15HObis]
HObis_out [lemma, in HOC15HObis]
HObis_tau [lemma, in HOC15HObis]
HObis_sym [lemma, in HOC15HObis]
HObis_refl [lemma, in HOC15HObis]
HObis_CONbis [lemma, in HOC19Coincide]
HObis_IObis [lemma, in HOC19Coincide]
HObis_HObis [lemma, in HOC19Coincide]
HOCore_Sound_Complete [lemma, in HOC25Axiomatization]
HOC01Defs [library]
HOC02BaseLemmas [library]
HOC03CanonicalLemmas [library]
HOC04DefLTS [library]
HOC05WFProcesses [library]
HOC06FreshLemmas [library]
HOC07SizeLemmas [library]
HOC08SubstLemmas [library]
HOC09GVLemmas [library]
HOC10CongrLemmas [library]
HOC11TransLemmas [library]
HOC12Guarded [library]
HOC13Bisimulations [library]
HOC14IObis [library]
HOC15HObis [library]
HOC16CONbis [library]
HOC17NORbis [library]
HOC18ONORbis [library]
HOC19Coincide [library]
HOC20Barbed [library]
HOC21Coinductive [library]
HOC22Decidability [library]
HOC23PrimeDecomposition [library]
HOC24PreCompleteness [library]
HOC25Axiomatization [library]
HOC26EarlyBisimulation [library]
HOC27BarbedRevisited [library]
HO_HOE [lemma, in HOC15HObis]
I
inhabited_var_wfprocess [instance, in HOC22Decidability]inst_abs_subst_eq [lemma, in HOC22Decidability]
Inter [section, in LibFsetExt]
inter_empty_subset [lemma, in LibFsetExt]
inter_not_empty_exists [lemma, in LibFsetExt]
inter_remove [lemma, in LibFsetExt]
inter_union [lemma, in LibFsetExt]
Inter.A [variable, in LibFsetExt]
in_relation_up_to [definition, in HOC13Bisimulations]
in_normal_relation [definition, in HOC13Bisimulations]
in_full_relation [definition, in HOC13Bisimulations]
in_relation [definition, in HOC13Bisimulations]
in_der_ok_lr [lemma, in HOC22Decidability]
in_der_ok_rl [lemma, in HOC22Decidability]
in_der [definition, in HOC22Decidability]
in_der_aux_eq [lemma, in HOC22Decidability]
in_der_aux [definition, in HOC22Decidability]
in_nor_forall_exists [lemma, in HOC17NORbis]
in_normal_relation_ex [definition, in HOC17NORbis]
in_and_notin [lemma, in LibFsetExt]
in_ex_relation_step [definition, in HOC21Coinductive]
in_relation_step [definition, in HOC21Coinductive]
in_barb_preserving [definition, in HOC20Barbed]
in_normal_relation_early [definition, in HOC26EarlyBisimulation]
in_relation_early [definition, in HOC26EarlyBisimulation]
in_up_to_forall_exists [lemma, in HOC14IObis]
in_full_forall [lemma, in HOC14IObis]
in_forall_exists [lemma, in HOC14IObis]
in_relation_ex_up_to [definition, in HOC14IObis]
in_relation_ex [definition, in HOC14IObis]
in_R_HO_IO [lemma, in HOC19Coincide]
IObis [definition, in HOC13Bisimulations]
IObisC [inductive, in HOC21Coinductive]
IObisC_ex_equivalence [instance, in HOC21Coinductive]
IObisC_ex_eq_IObisI_ex [lemma, in HOC21Coinductive]
IObisC_ex [inductive, in HOC21Coinductive]
IObisC_equivalence [instance, in HOC21Coinductive]
IObisC_eq_IObisI [lemma, in HOC21Coinductive]
IObisI [inductive, in HOC21Coinductive]
IObisIAux [inductive, in HOC21Coinductive]
IObisIAux_ex [inductive, in HOC21Coinductive]
IObisim_ex_up_to_IObisim_up_to_when_swap [lemma, in HOC14IObis]
IObisim_ex_IObisim_when_swap [lemma, in HOC14IObis]
IObisI_ex_eq_IObis_ex [lemma, in HOC21Coinductive]
IObisI_ex_var [lemma, in HOC21Coinductive]
IObisI_ex_out [lemma, in HOC21Coinductive]
IObisI_ex_in_ex [lemma, in HOC21Coinductive]
IObisI_ex_sym [lemma, in HOC21Coinductive]
IObisI_ex [inductive, in HOC21Coinductive]
IObisI_eq_IObis [lemma, in HOC21Coinductive]
IObisI_var [lemma, in HOC21Coinductive]
IObisI_out [lemma, in HOC21Coinductive]
IObisI_in [lemma, in HOC21Coinductive]
IObisI_sym [lemma, in HOC21Coinductive]
IObis_up_to [definition, in HOC13Bisimulations]
IObis_decidable [lemma, in HOC22Decidability]
IObis_constructive_decidable [lemma, in HOC22Decidability]
IObis_cancellation [lemma, in HOC23PrimeDecomposition]
IObis_wfcgr_nil_iff [lemma, in HOC24PreCompleteness]
IObis_abs_inv_body [lemma, in HOC25Axiomatization]
IObis_abs_inv_var [lemma, in HOC25Axiomatization]
IObis_abs_inv_ch [lemma, in HOC25Axiomatization]
IObis_cancellation_stronger [lemma, in HOC25Axiomatization]
IObis_ex_eq_IObisC_ex [lemma, in HOC21Coinductive]
IObis_eq_IObisC [lemma, in HOC21Coinductive]
IObis_async_barbed_lr [lemma, in HOC20Barbed]
IObis_eIObis [lemma, in HOC26EarlyBisimulation]
IObis_early [definition, in HOC26EarlyBisimulation]
IObis_in_full [lemma, in HOC14IObis]
IObis_unguardeds_eq [lemma, in HOC14IObis]
IObis_tau [lemma, in HOC14IObis]
IObis_subst [lemma, in HOC14IObis]
IObis_subst2 [lemma, in HOC14IObis]
IObis_subst1 [lemma, in HOC14IObis]
IObis_congr_par [lemma, in HOC14IObis]
IObis_par_assoc_r [lemma, in HOC14IObis]
IObis_par_assoc_l [lemma, in HOC14IObis]
IObis_congr_par_com [lemma, in HOC14IObis]
IObis_congr_nil_r [lemma, in HOC14IObis]
IObis_congr_nil_l [lemma, in HOC14IObis]
IObis_congr_par1 [lemma, in HOC14IObis]
IObis_congr_abs [lemma, in HOC14IObis]
IObis_congr_send [lemma, in HOC14IObis]
IObis_ex_up_to_IObis_up_to [lemma, in HOC14IObis]
IObis_IObis_ex [lemma, in HOC14IObis]
IObis_full [definition, in HOC14IObis]
IObis_ex_up_to [definition, in HOC14IObis]
IObis_ex [definition, in HOC14IObis]
IObis_sizeP_eq [lemma, in HOC14IObis]
IObis_size_unguardedX [lemma, in HOC14IObis]
IObis_swap [lemma, in HOC14IObis]
IObis_up_to_cgr_IObis [lemma, in HOC14IObis]
IObis_up_to_IObis [lemma, in HOC14IObis]
IObis_is_eq_rel [instance, in HOC14IObis]
IObis_trans [lemma, in HOC14IObis]
IObis_var [lemma, in HOC14IObis]
IObis_out [lemma, in HOC14IObis]
IObis_in [lemma, in HOC14IObis]
IObis_sym [lemma, in HOC14IObis]
IObis_refl [lemma, in HOC14IObis]
IObis_HObis_cp [lemma, in HOC19Coincide]
IObis_RHOIO [lemma, in HOC19Coincide]
IObis_HObisE [lemma, in HOC19Coincide]
IObis_HObis [lemma, in HOC19Coincide]
IObis_congr_pipe [lemma, in HOC19Coincide]
IObis_closed [lemma, in HOC19Coincide]
IObis_IObis [lemma, in HOC19Coincide]
IOCIAMain [constructor, in HOC21Coinductive]
IOCIAMain_ex [constructor, in HOC21Coinductive]
IOCIMain [constructor, in HOC21Coinductive]
IOCIMain_ex [constructor, in HOC21Coinductive]
IOCMain [constructor, in HOC21Coinductive]
IOCMain_ex [constructor, in HOC21Coinductive]
IO_bisimulation_up_to [definition, in HOC13Bisimulations]
IO_bisimulation [definition, in HOC13Bisimulations]
IO_pw_wfp_prod [lemma, in HOC23PrimeDecomposition]
IO_pw_len [lemma, in HOC23PrimeDecomposition]
IO_pointwise [definition, in HOC23PrimeDecomposition]
IO_ex_IO_RCancel [lemma, in HOC23PrimeDecomposition]
IO_pointwise_IObis [lemma, in HOC25Axiomatization]
io_extcgr_full [lemma, in HOC25Axiomatization]
io_extcgr_step [lemma, in HOC25Axiomatization]
io_norm_full [lemma, in HOC25Axiomatization]
io_norm_step [lemma, in HOC25Axiomatization]
io_nf_no_rem [lemma, in HOC25Axiomatization]
io_nf_no_out [lemma, in HOC25Axiomatization]
io_nf_cgr [constructor, in HOC25Axiomatization]
io_nf_sym_base_nil [constructor, in HOC25Axiomatization]
io_nf_sym_base [constructor, in HOC25Axiomatization]
io_nf_base [constructor, in HOC25Axiomatization]
io_nf_base_nil [constructor, in HOC25Axiomatization]
IO_bisimulation_early [definition, in HOC26EarlyBisimulation]
IO_bisimulation_full [definition, in HOC14IObis]
IO_bisimulation_ex_up_to [definition, in HOC14IObis]
IO_bisimulation_ex [definition, in HOC14IObis]
IO_bisimulation_up_to_refl [lemma, in HOC14IObis]
iter_abs_par_fiddle [lemma, in HOC18ONORbis]
iter_abs_par_congr [lemma, in HOC18ONORbis]
iter_abs_par_abs [definition, in HOC18ONORbis]
iter_abs_par [definition, in HOC18ONORbis]
L
label [inductive, in HOC04DefLTS]LabIn [constructor, in HOC04DefLTS]
LabOut [constructor, in HOC04DefLTS]
LabRem [constructor, in HOC04DefLTS]
leave [definition, in HOC05WFProcesses]
leave_ex [lemma, in HOC05WFProcesses]
leave_not_fresh [lemma, in HOC05WFProcesses]
leave_red_set [lemma, in HOC05WFProcesses]
leave_nodup_r [lemma, in HOC05WFProcesses]
leave_inv_r [lemma, in HOC05WFProcesses]
leave_inv [lemma, in HOC05WFProcesses]
leave_permut_fst [lemma, in HOC19Coincide]
left413 [lemma, in HOC15HObis]
left413NOR [lemma, in HOC17NORbis]
lemma415 [lemma, in HOC18ONORbis]
lemma415a [lemma, in HOC18ONORbis]
lemma415b [lemma, in HOC18ONORbis]
lengthn [lemma, in LibListExt]
length_swap_names [lemma, in HOC17NORbis]
length_combine [lemma, in LibListExt]
length_rem1 [lemma, in LibListExt]
length_app_inv [lemma, in LibListExt]
length0 [lemma, in LibListExt]
lfresh_in_subst_p_q [lemma, in HOC02BaseLemmas]
lfresh_subst_rewrite [lemma, in HOC02BaseLemmas]
lfresh_nil [lemma, in HOC02BaseLemmas]
lfresh_par_iff [lemma, in HOC02BaseLemmas]
lfresh_gvar [lemma, in HOC02BaseLemmas]
lfresh_lvar [lemma, in HOC02BaseLemmas]
lfresh_receive [lemma, in HOC02BaseLemmas]
lfresh_send [lemma, in HOC02BaseLemmas]
LibFsetExt [library]
LibListExt [library]
ListBasic [section, in LibListExt]
ListBasic.A [variable, in LibListExt]
list_exists_min [lemma, in HOC23PrimeDecomposition]
list_sum_app [lemma, in HOC25Axiomatization]
list_sum_cons [lemma, in HOC25Axiomatization]
list_sum_nil [lemma, in HOC25Axiomatization]
list_sum [definition, in HOC25Axiomatization]
list_proc [definition, in HOC05WFProcesses]
list_subset_combine_in [lemma, in HOC19Coincide]
list_subset_subset [lemma, in HOC19Coincide]
list_subset_nodup_snd [lemma, in HOC19Coincide]
list_subset_nodup_fst [lemma, in HOC19Coincide]
list_subset_Forall_snd [lemma, in HOC19Coincide]
list_subset_Forall_fst [lemma, in HOC19Coincide]
list_subset_in_set_inv [lemma, in HOC19Coincide]
list_subset_in_set [lemma, in HOC19Coincide]
list_subset_in_snd [lemma, in HOC19Coincide]
list_subset_in_fst [lemma, in HOC19Coincide]
list_subset [definition, in HOC19Coincide]
lsubst [definition, in HOC01Defs]
lsubst_decomposition_g [lemma, in HOC02BaseLemmas]
lt_decidable [instance, in aux]
lt_dec [definition, in aux]
LV [definition, in HOC01Defs]
Lvar [constructor, in HOC01Defs]
lvar [definition, in HOC01Defs]
LV_subst [lemma, in HOC02BaseLemmas]
M
max [definition, in aux]maxassoc [lemma, in aux]
maxcomm [lemma, in aux]
max0 [lemma, in aux]
max0neutrall [lemma, in aux]
max0neutralr [lemma, in aux]
measure_induction_set [lemma, in HOC25Axiomatization]
mem_of_permuts [lemma, in LibListExt]
mem_fst_split_remdup [lemma, in LibListExt]
mem_comb [lemma, in LibListExt]
mem_rem1_r [lemma, in LibListExt]
mem_rem1_l [lemma, in LibListExt]
mem_app_inv2 [lemma, in LibListExt]
mem_app_inv1 [lemma, in LibListExt]
mem_len_pos [lemma, in LibListExt]
mem_remdup_iff [lemma, in LibListExt]
mem_remdup [lemma, in LibListExt]
Mem_var_decidable [instance, in LibListExt]
Mem_dec [definition, in LibListExt]
min_same [lemma, in aux]
mkWfP [constructor, in HOC03CanonicalLemmas]
my_wf_ind [lemma, in HOC03CanonicalLemmas]
N
NCore [constructor, in HOC25Axiomatization]NCoreNil [constructor, in HOC25Axiomatization]
nested_abs_monotonous [lemma, in HOC25Axiomatization]
nested_abs_eq_abs [lemma, in HOC25Axiomatization]
nested_abs_gsubst [lemma, in HOC25Axiomatization]
nested_abs_eq_nil [lemma, in HOC25Axiomatization]
nested_abs_eq_gvar [lemma, in HOC25Axiomatization]
nested_abs_eq_par [lemma, in HOC25Axiomatization]
nested_abs_eq_send [lemma, in HOC25Axiomatization]
nested_abs_eq [lemma, in HOC25Axiomatization]
nested_abs [definition, in HOC25Axiomatization]
nf_cannot_reduce [lemma, in HOC25Axiomatization]
nf_cannot_reduce_rl [lemma, in HOC25Axiomatization]
nf_cannot_reduce_lr [lemma, in HOC25Axiomatization]
nf_congr_invariant [lemma, in HOC25Axiomatization]
nf_equiv_par_nil [lemma, in HOC25Axiomatization]
nf_remove_nil_congr [lemma, in HOC25Axiomatization]
nf_no_par_nil [lemma, in HOC25Axiomatization]
nf_abs_eq [lemma, in HOC25Axiomatization]
nf_cannot_reduce_basic [lemma, in HOC25Axiomatization]
nf_swap_invariant [lemma, in HOC25Axiomatization]
nf_Nil [constructor, in HOC25Axiomatization]
nf_Par [constructor, in HOC25Axiomatization]
nf_Gvar [constructor, in HOC25Axiomatization]
nf_Abs [constructor, in HOC25Axiomatization]
nf_Send [constructor, in HOC25Axiomatization]
Nil [constructor, in HOC01Defs]
nil_process_char [lemma, in HOC10CongrLemmas]
NoDup [section, in LibListExt]
noDup [definition, in LibListExt]
nodup_swap_names [lemma, in HOC17NORbis]
nodup_tolist [axiom, in LibListExt]
noDup_snd_remDup_combine [lemma, in LibListExt]
noDup_fst_remDup_combine [lemma, in LibListExt]
nodup_combine_snd [lemma, in LibListExt]
nodup_combine_fst [lemma, in LibListExt]
nodup_app_iff [lemma, in LibListExt]
nodup_count [lemma, in LibListExt]
nodup_app_comm [lemma, in LibListExt]
nodup_app_comm_step [lemma, in LibListExt]
nodup_app_inv [lemma, in LibListExt]
nodup_rem1 [lemma, in LibListExt]
nodup_middle [lemma, in LibListExt]
nodup_remdup [lemma, in LibListExt]
NoDup.A [variable, in LibListExt]
none_core_wfcgr [lemma, in HOC10CongrLemmas]
NORbis [definition, in HOC13Bisimulations]
NORbisC [definition, in HOC13Bisimulations]
NORbisC_ex [definition, in HOC17NORbis]
NORbisC_in_normal [lemma, in HOC17NORbis]
NORbisC_out_normal [lemma, in HOC17NORbis]
NORbisC_tau [lemma, in HOC17NORbis]
NORbisC_sym [lemma, in HOC17NORbis]
NORbisC_eNORbisC [lemma, in HOC26EarlyBisimulation]
NORbisC_early [definition, in HOC26EarlyBisimulation]
NORbisC_ex_NORbisC_ex_ex [lemma, in HOC26EarlyBisimulation]
NORbisC_ex_ex [definition, in HOC26EarlyBisimulation]
NORbisE [definition, in HOC13Bisimulations]
NORbisE_ONE_ON [lemma, in HOC17NORbis]
NORbisE_ch_swap [lemma, in HOC17NORbis]
NORbisE_equiv [lemma, in HOC17NORbis]
NORbisE_ONORbis [lemma, in HOC19Coincide]
NORbisE_var [lemma, in HOC19Coincide]
NORbisE_tau [lemma, in HOC19Coincide]
NORbisE_in [lemma, in HOC19Coincide]
NORbisE_out_normal [lemma, in HOC19Coincide]
NORbisE_sym [lemma, in HOC19Coincide]
NORbis_in_par [lemma, in HOC17NORbis]
NORbis_exR_ch2 [lemma, in HOC17NORbis]
NORbis_congr_abs [lemma, in HOC17NORbis]
NORbis_ex_R_r [lemma, in HOC17NORbis]
NORbis_NORbis_ex [lemma, in HOC17NORbis]
NORbis_ex_in_normal_ex [lemma, in HOC17NORbis]
NORbis_ex [definition, in HOC17NORbis]
Norbis_ch_chan [lemma, in HOC17NORbis]
NORbis_ch_swap [lemma, in HOC17NORbis]
NORbis_in_normal [lemma, in HOC17NORbis]
NORbis_out_normal [lemma, in HOC17NORbis]
NORbis_tau [lemma, in HOC17NORbis]
NORbis_sym [lemma, in HOC17NORbis]
NORbis_early [definition, in HOC26EarlyBisimulation]
NORbis_ex_ex [definition, in HOC26EarlyBisimulation]
NORbis_trans [lemma, in HOC19Coincide]
NORbis_congr_par_nil [lemma, in HOC19Coincide]
NORbis_NORbis [lemma, in HOC19Coincide]
normalization_stops [lemma, in HOC25Axiomatization]
Normal_bisimulation [definition, in HOC13Bisimulations]
Normal_bisimulation_ex [definition, in HOC17NORbis]
normal_form_IObis_wfcgr_eq [lemma, in HOC25Axiomatization]
normal_form_wfp_prod_app [lemma, in HOC25Axiomatization]
normal_form [inductive, in HOC25Axiomatization]
Normal_bisimulation_early [definition, in HOC26EarlyBisimulation]
Normal_bisimulation_ex_ex [definition, in HOC26EarlyBisimulation]
norm_full_measure [lemma, in HOC25Axiomatization]
norm_step_measure [lemma, in HOC25Axiomatization]
norm_step_abs_char [lemma, in HOC25Axiomatization]
norm_full_sizeP_eq [lemma, in HOC25Axiomatization]
norm_step_sizeP_eq [lemma, in HOC25Axiomatization]
norm_full_sizeP [lemma, in HOC25Axiomatization]
norm_step_sizeP [lemma, in HOC25Axiomatization]
norm_full_par_r [lemma, in HOC25Axiomatization]
norm_full_par_l [lemma, in HOC25Axiomatization]
norm_full_abs [lemma, in HOC25Axiomatization]
norm_full_send [lemma, in HOC25Axiomatization]
norm_full [definition, in HOC25Axiomatization]
norm_step [inductive, in HOC25Axiomatization]
notin_remove [lemma, in LibFsetExt]
not_prime_nil [lemma, in HOC23PrimeDecomposition]
no_wfcgr_nil_gvar [lemma, in HOC10CongrLemmas]
no_wfcgr_nil_abs [lemma, in HOC10CongrLemmas]
no_wfcgr_nil_send [lemma, in HOC10CongrLemmas]
no_wfcgr_gvar_nil [lemma, in HOC10CongrLemmas]
no_wfcgr_gvar_abs [lemma, in HOC10CongrLemmas]
no_wfcgr_gvar_send [lemma, in HOC10CongrLemmas]
no_wfcgr_abs_nil [lemma, in HOC10CongrLemmas]
no_wfcgr_abs_gvar [lemma, in HOC10CongrLemmas]
no_wfcgr_abs_send [lemma, in HOC10CongrLemmas]
no_wfcgr_send_nil [lemma, in HOC10CongrLemmas]
no_wfcgr_send_gvar [lemma, in HOC10CongrLemmas]
no_wfcgr_send_abs [lemma, in HOC10CongrLemmas]
NParLeft [constructor, in HOC25Axiomatization]
NParRight [constructor, in HOC25Axiomatization]
NReceive [constructor, in HOC25Axiomatization]
NSend [constructor, in HOC25Axiomatization]
num_of_pars_eq [lemma, in HOC25Axiomatization]
num_of_pars_ordered [lemma, in HOC25Axiomatization]
num_of_pars_ordered_le [lemma, in HOC25Axiomatization]
num_of_pars_ordered_par_eq [lemma, in HOC25Axiomatization]
num_of_pars_ordered_par [lemma, in HOC25Axiomatization]
num_of_pars_cancel_b [lemma, in HOC25Axiomatization]
num_of_pars_cancel_f [lemma, in HOC25Axiomatization]
num_of_pars_wfp_prod_app_eq [lemma, in HOC25Axiomatization]
num_of_pars_wfp_prod_app [lemma, in HOC25Axiomatization]
num_of_pars_aux_1 [lemma, in HOC25Axiomatization]
num_of_pars_wfp_prod_app_comm [lemma, in HOC25Axiomatization]
num_of_pars [definition, in HOC25Axiomatization]
num_var_wfcgr [lemma, in HOC10CongrLemmas]
num_var [definition, in HOC10CongrLemmas]
num_abs_wfcgr [lemma, in HOC10CongrLemmas]
num_abs [definition, in HOC10CongrLemmas]
num_send_wfcgr [lemma, in HOC10CongrLemmas]
num_send [definition, in HOC10CongrLemmas]
O
ONORbis [definition, in HOC13Bisimulations]ONORbis_up_to [definition, in HOC13Bisimulations]
ONORbis_up_to_cgr_ONORbis [lemma, in HOC18ONORbis]
ONORbis_up_to_ONORbis [lemma, in HOC18ONORbis]
ONORbis_is_eq_rel [instance, in HOC18ONORbis]
ONORbis_trans [lemma, in HOC18ONORbis]
ONORbis_ex [definition, in HOC18ONORbis]
ONORbis_var [lemma, in HOC18ONORbis]
ONORbis_in [lemma, in HOC18ONORbis]
ONORbis_out_normal_ex [lemma, in HOC18ONORbis]
ONORbis_out_normal [lemma, in HOC18ONORbis]
ONORbis_tau [lemma, in HOC18ONORbis]
ONORbis_sym [lemma, in HOC18ONORbis]
ONORbis_refl [lemma, in HOC18ONORbis]
ONORbis_IObis [lemma, in HOC19Coincide]
ONORbis_out [lemma, in HOC19Coincide]
ONORbis_ONORbis [lemma, in HOC19Coincide]
ONOR_RON [lemma, in HOC18ONORbis]
ONOR_ONOR_ex [lemma, in HOC18ONORbis]
OpenNormal_bisimulation_up_to [definition, in HOC13Bisimulations]
OpenNormal_bisimulation [definition, in HOC13Bisimulations]
OpenNormal_bisimulation_ex [definition, in HOC18ONORbis]
ordered [definition, in HOC25Axiomatization]
ordered_nf_invariant [lemma, in HOC25Axiomatization]
ordered_dpd_invariant [lemma, in HOC25Axiomatization]
ordered_par_nil_r [lemma, in HOC25Axiomatization]
ordered_par_nil_l [lemma, in HOC25Axiomatization]
ordered_par [lemma, in HOC25Axiomatization]
ordered_wfcgr [lemma, in HOC25Axiomatization]
order_oiv_cfresh_iff [lemma, in HOC27BarbedRevisited]
order_oiv_async_barbed [lemma, in HOC27BarbedRevisited]
order_oiv_wfcgr [lemma, in HOC27BarbedRevisited]
order_oiv [definition, in HOC27BarbedRevisited]
out_normal_relation_up_to [definition, in HOC13Bisimulations]
out_relation_up_to [definition, in HOC13Bisimulations]
out_context_relation [definition, in HOC13Bisimulations]
out_normal_relation [definition, in HOC13Bisimulations]
out_relation [definition, in HOC13Bisimulations]
out_der_ok [lemma, in HOC22Decidability]
out_der [definition, in HOC22Decidability]
out_der_aux_eq [lemma, in HOC22Decidability]
out_der_aux [definition, in HOC22Decidability]
out_nor_forall_exists [lemma, in HOC17NORbis]
out_normal_relation_ex [definition, in HOC17NORbis]
out_relation_step [definition, in HOC21Coinductive]
out_barb_preserving [definition, in HOC20Barbed]
out_context_relation_early [definition, in HOC26EarlyBisimulation]
out_normal_relation_early [definition, in HOC26EarlyBisimulation]
out_R_HO_IO [lemma, in HOC19Coincide]
P
Par [constructor, in HOC01Defs]par_nil_sizeP_not_0 [lemma, in HOC25Axiomatization]
par_ag2 [definition, in HOC04DefLTS]
par_ag1 [definition, in HOC04DefLTS]
peano_induction_type [lemma, in HOC25Axiomatization]
perform_input [definition, in HOC20Barbed]
perform_output [definition, in HOC20Barbed]
Permutation [section, in LibListExt]
Permutation.A [variable, in LibListExt]
Permutation.B [variable, in LibListExt]
Permutation2 [section, in LibListExt]
Permutation2.A [variable, in LibListExt]
Permutation2.B [variable, in LibListExt]
permuted_subst [lemma, in HOC15HObis]
permute_pipe [lemma, in HOC15HObis]
permute_subst_order [lemma, in HOC15HObis]
permute_NOR_pipe [lemma, in HOC17NORbis]
permut_subst [lemma, in HOC15HObis]
permut_to_list [lemma, in LibListExt]
permut_inv_r [lemma, in LibListExt]
permut_inv_l [lemma, in LibListExt]
permut_exists2 [lemma, in LibListExt]
permut_exists [lemma, in LibListExt]
permut_ndfl [lemma, in LibListExt]
permut_nodup [lemma, in LibListExt]
permut_combine [lemma, in LibListExt]
permut_combine_step [lemma, in LibListExt]
permut_remN_r [lemma, in LibListExt]
permut_remN_mem [lemma, in LibListExt]
permut_rem1_lr [lemma, in LibListExt]
permut_rem1_l [lemma, in LibListExt]
permut_rem1_r [lemma, in LibListExt]
permut_cons_rem1 [lemma, in LibListExt]
permut_cons_iff [lemma, in LibListExt]
permut_count_forall [lemma, in LibListExt]
permut_mem_exists [lemma, in LibListExt]
permut_flip_first_two [lemma, in LibListExt]
permut_of_nil [lemma, in LibListExt]
permut_count [lemma, in LibListExt]
permut_from_list [lemma, in LibListExt]
permut_mem [lemma, in LibListExt]
permut_len [lemma, in LibListExt]
piping_HOext [lemma, in HOC15HObis]
pre_lemma413 [lemma, in HOC15HObis]
pre_lemma413NOR [lemma, in HOC17NORbis]
prime [definition, in HOC23PrimeDecomposition]
prime_gvar [lemma, in HOC23PrimeDecomposition]
prime_send [lemma, in HOC23PrimeDecomposition]
prime_decomposition_unique [lemma, in HOC23PrimeDecomposition]
prime_decomposition_exists [lemma, in HOC23PrimeDecomposition]
prime_decomposition_IO [lemma, in HOC23PrimeDecomposition]
prime_decomposition [definition, in HOC23PrimeDecomposition]
prime_remove [lemma, in HOC23PrimeDecomposition]
prime_out [lemma, in HOC23PrimeDecomposition]
prime_in [lemma, in HOC23PrimeDecomposition]
prime_parallel [lemma, in HOC23PrimeDecomposition]
prime_IO [lemma, in HOC23PrimeDecomposition]
prime_characterization [lemma, in HOC24PreCompleteness]
prime_in_dpd [lemma, in HOC24PreCompleteness]
prime_gswap [lemma, in HOC24PreCompleteness]
prime_characterization [lemma, in HOC25Axiomatization]
proc [projection, in HOC03CanonicalLemmas]
process [inductive, in HOC01Defs]
process_eq_decidable [instance, in HOC01Defs]
prod [definition, in HOC01Defs]
R
Rabs [constructor, in HOC15HObis]Rabs [constructor, in HOC14IObis]
Rbase [constructor, in HOC18ONORbis]
Rbis [constructor, in HOC15HObis]
Rbis [constructor, in HOC14IObis]
RCancel [inductive, in HOC23PrimeDecomposition]
RCancel_IObis [lemma, in HOC23PrimeDecomposition]
RCancel_step_forward [lemma, in HOC23PrimeDecomposition]
RCMain [constructor, in HOC23PrimeDecomposition]
Receive [constructor, in HOC01Defs]
RelWfP [definition, in HOC05WFProcesses]
RemDup [section, in LibListExt]
remDup [definition, in LibListExt]
remdup_eq_fl [lemma, in LibListExt]
remdup_inv [lemma, in LibListExt]
RemDup.A [variable, in LibListExt]
remN_to_list_perm [lemma, in LibListExt]
remN_same_perm [lemma, in LibListExt]
Remove [section, in LibFsetExt]
removeN [definition, in LibListExt]
RemoveOne [section, in LibListExt]
removeOne [definition, in LibListExt]
RemoveOne.A [variable, in LibListExt]
remove_par_nils_size [lemma, in HOC24PreCompleteness]
remove_par_nils_wfp_prod_repeat_abs [lemma, in HOC24PreCompleteness]
remove_par_nils_sizeP [lemma, in HOC24PreCompleteness]
remove_par_nils_wfcgr [lemma, in HOC24PreCompleteness]
remove_nil_wfcgr [lemma, in HOC24PreCompleteness]
remove_nil_wfcgr_step [lemma, in HOC24PreCompleteness]
remove_nil_no_par_nil [lemma, in HOC24PreCompleteness]
remove_par_nils_sizeP_0 [lemma, in HOC24PreCompleteness]
remove_par_nils_eq_abs [lemma, in HOC24PreCompleteness]
remove_par_nils_swap [lemma, in HOC24PreCompleteness]
remove_par_nils_fresh [lemma, in HOC24PreCompleteness]
remove_par_nils_eq_par [lemma, in HOC24PreCompleteness]
remove_par_nils_eq_nil [lemma, in HOC24PreCompleteness]
remove_par_nils_eq_gvar [lemma, in HOC24PreCompleteness]
remove_par_nils_eq_send [lemma, in HOC24PreCompleteness]
remove_par_nils_eq [lemma, in HOC24PreCompleteness]
remove_par_nils [definition, in HOC24PreCompleteness]
remove_par_nils_absorb [lemma, in HOC25Axiomatization]
remove_par_nils_red [lemma, in HOC25Axiomatization]
remove_union_comm [lemma, in LibFsetExt]
remove_union_distr [lemma, in LibFsetExt]
remove_union [lemma, in LibFsetExt]
remove_from_empty [lemma, in LibFsetExt]
remove_empty [lemma, in LibFsetExt]
remove_same [lemma, in LibFsetExt]
remove_comm [lemma, in LibFsetExt]
remove_in_subsets [lemma, in LibFsetExt]
remove_while_notin [lemma, in LibFsetExt]
Remove.A [variable, in LibFsetExt]
rem_union_cancel [lemma, in LibFsetExt]
rem1_to_list_perm [lemma, in LibListExt]
rem1_permuts [lemma, in LibListExt]
rem1_remN_comm [lemma, in LibListExt]
rem1_mem_comm [lemma, in LibListExt]
rem1_comm [lemma, in LibListExt]
rem1_notin_list [lemma, in LibListExt]
repeat [definition, in HOC01Defs]
repeat_Mem_in [lemma, in HOC01Defs]
repeat_from_list_n [lemma, in HOC01Defs]
repeat_length [lemma, in HOC01Defs]
RHOIO [constructor, in HOC19Coincide]
right413 [lemma, in HOC15HObis]
right413NOR [lemma, in HOC17NORbis]
Rnrefl [constructor, in HOC15HObis]
Rn1 [constructor, in HOC15HObis]
Rn2 [constructor, in HOC15HObis]
RON [inductive, in HOC18ONORbis]
RON_Main [constructor, in HOC18ONORbis]
Rp1 [constructor, in HOC14IObis]
Rp1refl [constructor, in HOC14IObis]
Rr [constructor, in HOC17NORbis]
Rrefl [constructor, in HOC15HObis]
Rrefl [constructor, in HOC14IObis]
Rs [constructor, in HOC15HObis]
Rs [constructor, in HOC14IObis]
Rsb [constructor, in HOC14IObis]
Rsbis [constructor, in HOC15HObis]
Rsbis [constructor, in HOC14IObis]
RsN [constructor, in HOC15HObis]
RsN [constructor, in HOC14IObis]
Rsw [constructor, in HOC17NORbis]
Rsw [constructor, in HOC14IObis]
Rswap [constructor, in HOC17NORbis]
Rswap [constructor, in HOC14IObis]
Rswapm [constructor, in HOC18ONORbis]
RswapX [constructor, in HOC18ONORbis]
RswCh [constructor, in HOC17NORbis]
Rswr [constructor, in HOC17NORbis]
Rswr [constructor, in HOC14IObis]
Rtrans [constructor, in HOC15HObis]
Rtrans [constructor, in HOC14IObis]
RtransNOR [constructor, in HOC19Coincide]
Rtrans_ab [constructor, in HOC20Barbed]
Rtrans_on [constructor, in HOC18ONORbis]
R_send [inductive, in HOC15HObis]
R_receive [inductive, in HOC15HObis]
R_nil [inductive, in HOC15HObis]
R_trans [inductive, in HOC15HObis]
R_r_bis [constructor, in HOC15HObis]
R_r_base [constructor, in HOC15HObis]
R_r [inductive, in HOC15HObis]
R_ch_bis [constructor, in HOC15HObis]
R_ch_base [constructor, in HOC15HObis]
R_ch [inductive, in HOC15HObis]
R_refl [inductive, in HOC15HObis]
R_Swap2 [inductive, in HOC17NORbis]
R_ch2_bis [constructor, in HOC17NORbis]
R_ch2_base [constructor, in HOC17NORbis]
R_ch2 [inductive, in HOC17NORbis]
R_r2_bis [constructor, in HOC17NORbis]
R_r2_base [constructor, in HOC17NORbis]
R_r2 [inductive, in HOC17NORbis]
R_Swap [inductive, in HOC17NORbis]
R_swap [inductive, in HOC17NORbis]
R_io_nf_IObis [lemma, in HOC25Axiomatization]
R_io_nf [inductive, in HOC25Axiomatization]
R_trans_ab [inductive, in HOC20Barbed]
R_ONORbis_up_to_up_to_R_ONORbis_ex [lemma, in HOC18ONORbis]
R_trans_on [inductive, in HOC18ONORbis]
R_Swap_All [inductive, in HOC18ONORbis]
R_subst [inductive, in HOC14IObis]
R_par1 [inductive, in HOC14IObis]
R_abs [inductive, in HOC14IObis]
R_send [inductive, in HOC14IObis]
R_swap2 [inductive, in HOC14IObis]
R_swap_IObis [lemma, in HOC14IObis]
R_swap [inductive, in HOC14IObis]
R_IObis_up_to_up_to_R_IObis [lemma, in HOC14IObis]
R_trans [inductive, in HOC14IObis]
R_refl [inductive, in HOC14IObis]
R_transNOR [inductive, in HOC19Coincide]
R_HO_IO [inductive, in HOC19Coincide]
S
Send [constructor, in HOC01Defs]send_separation [lemma, in HOC25Axiomatization]
send_wfcgr_no_nil [lemma, in HOC10CongrLemmas]
send_wfcgr_inv [lemma, in HOC10CongrLemmas]
send_core_wfcgr [lemma, in HOC10CongrLemmas]
singleton_union [lemma, in LibFsetExt]
singleton_absurd [lemma, in LibFsetExt]
size [definition, in HOC01Defs]
sizeAbs [definition, in HOC04DefLTS]
sizeCh [definition, in HOC01Defs]
sizeCh_out_eq [lemma, in HOC07SizeLemmas]
sizeCh_out_neq [lemma, in HOC07SizeLemmas]
sizeCh_in_eq [lemma, in HOC07SizeLemmas]
sizeCh_in_neq [lemma, in HOC07SizeLemmas]
sizeCh_subst [lemma, in HOC07SizeLemmas]
sizeCh_out_nfr [lemma, in HOC07SizeLemmas]
sizeCh_in_nfr [lemma, in HOC07SizeLemmas]
sizeCh_neq [lemma, in HOC07SizeLemmas]
sizeCh_cfresh [lemma, in HOC07SizeLemmas]
sizeCh_CHS [lemma, in HOC07SizeLemmas]
sizeCh_NORbis [lemma, in HOC17NORbis]
sizeCh_wfcgr [lemma, in HOC10CongrLemmas]
sizeCh_ONORbis [lemma, in HOC18ONORbis]
sizeO [definition, in HOC18ONORbis]
sizeO_remove [lemma, in HOC18ONORbis]
sizeO_out [lemma, in HOC18ONORbis]
sizeO_in [lemma, in HOC18ONORbis]
sizeO_subst [lemma, in HOC18ONORbis]
sizeP [definition, in HOC01Defs]
sizeP_remove [lemma, in HOC07SizeLemmas]
sizeP_out [lemma, in HOC07SizeLemmas]
sizeP_in [lemma, in HOC07SizeLemmas]
sizeP_swap [lemma, in HOC07SizeLemmas]
sizeP_subst [lemma, in HOC02BaseLemmas]
sizeP_0_congr_nil [lemma, in HOC18ONORbis]
sizeX [definition, in HOC01Defs]
sizeX_Ch [lemma, in HOC07SizeLemmas]
sizeX_2_sizeX [lemma, in HOC07SizeLemmas]
sizeX_remove [lemma, in HOC07SizeLemmas]
sizeX_out [lemma, in HOC07SizeLemmas]
sizeX_in [lemma, in HOC07SizeLemmas]
sizeX_subst [lemma, in HOC07SizeLemmas]
sizeX_subst2_cp [lemma, in HOC07SizeLemmas]
sizeX_subst1_cp [lemma, in HOC07SizeLemmas]
sizeX_cp [lemma, in HOC07SizeLemmas]
sizeX_gfresh [lemma, in HOC07SizeLemmas]
sizeX_GV [lemma, in HOC07SizeLemmas]
sizeX_wfcgr [lemma, in HOC10CongrLemmas]
sizeX_subst_fresh [lemma, in HOC10CongrLemmas]
sizeX_ONORbis [lemma, in HOC18ONORbis]
sizeX_IObis [lemma, in HOC14IObis]
size_remove [lemma, in HOC07SizeLemmas]
size_out [lemma, in HOC07SizeLemmas]
size_in [lemma, in HOC07SizeLemmas]
size_swap [lemma, in HOC07SizeLemmas]
size_unguardedX_remove [lemma, in HOC12Guarded]
size_unguardedX [definition, in HOC12Guarded]
size_lsubst [lemma, in HOC02BaseLemmas]
size_subst [lemma, in HOC02BaseLemmas]
snd_split [lemma, in LibListExt]
snd_split_step [lemma, in LibListExt]
snd_split_cons [lemma, in LibListExt]
SplitCombine [section, in LibListExt]
SplitCombine.A [variable, in LibListExt]
SplitCombine.B [variable, in LibListExt]
split_combine_fs [lemma, in LibListExt]
split_length_r [lemma, in LibListExt]
split_length_l [lemma, in LibListExt]
split_spec [lemma, in LibListExt]
SubLists [section, in LibListExt]
sublists_3 [lemma, in LibListExt]
sublists_2 [lemma, in LibListExt]
sublists_r [lemma, in LibListExt]
sublists_l [lemma, in LibListExt]
SubLists.A [variable, in LibListExt]
SubLists.B [variable, in LibListExt]
Subset [section, in LibFsetExt]
subset_union_r [lemma, in LibFsetExt]
subset_of_empty [lemma, in LibFsetExt]
Subset.A [variable, in LibFsetExt]
subst [definition, in HOC01Defs]
substs_commute_lg [lemma, in HOC02BaseLemmas]
substs_commute_gg [lemma, in HOC02BaseLemmas]
subst_on_Abs [lemma, in HOC03CanonicalLemmas]
subst_nil_eq [lemma, in HOC10CongrLemmas]
subst_on_swap [lemma, in HOC02BaseLemmas]
subst_on_subst [lemma, in HOC02BaseLemmas]
subst_on_subst_same [lemma, in HOC02BaseLemmas]
subst_decomposition_g [lemma, in HOC02BaseLemmas]
subst_decomposition_l [lemma, in HOC02BaseLemmas]
subst_lvar_equal [lemma, in HOC02BaseLemmas]
subst_lvar_idem [lemma, in HOC02BaseLemmas]
subst_gvar_equal [lemma, in HOC02BaseLemmas]
subst_gvar_idem [lemma, in HOC02BaseLemmas]
subst_eq_rewrite [lemma, in HOC05WFProcesses]
swap [definition, in HOC01Defs]
swap_chans_names [lemma, in HOC17NORbis]
swap_chans_Msubst_comm [lemma, in HOC17NORbis]
swap_channels [definition, in HOC17NORbis]
swap_names [definition, in HOC17NORbis]
swap_name_right [lemma, in HOC08SubstLemmas]
swap_name_left [lemma, in HOC08SubstLemmas]
swap_chan_on_subst [lemma, in HOC02BaseLemmas]
swap_on_subst [lemma, in HOC02BaseLemmas]
swap_chan_involutive [lemma, in HOC02BaseLemmas]
swap_name_involutive [lemma, in HOC02BaseLemmas]
swap_chan_sym [lemma, in HOC02BaseLemmas]
swap_chan_equal [lemma, in HOC02BaseLemmas]
swap_name_equal [lemma, in HOC02BaseLemmas]
swap_sym [lemma, in HOC02BaseLemmas]
swap_involutive [lemma, in HOC02BaseLemmas]
swap_gvar_involutive [lemma, in HOC02BaseLemmas]
swap_gvar_equal_iff [lemma, in HOC02BaseLemmas]
swap_equal [lemma, in HOC02BaseLemmas]
swap_gvar_equal [lemma, in HOC02BaseLemmas]
swap_gvar_right [lemma, in HOC02BaseLemmas]
swap_gvar_left [lemma, in HOC02BaseLemmas]
swap_relation [definition, in HOC14IObis]
swap_chan [definition, in HOC01Defs]
swap_name [definition, in HOC01Defs]
swap_gvar [definition, in HOC01Defs]
T
take_drop_nth [lemma, in LibListExt]Tau [constructor, in HOC04DefLTS]
tau_relation_up_to [definition, in HOC13Bisimulations]
tau_relation [definition, in HOC13Bisimulations]
ToList [section, in LibListExt]
ToList.A [variable, in LibListExt]
top_channels [definition, in HOC10CongrLemmas]
to_list_cons_union [lemma, in LibListExt]
to_from_list [axiom, in LibListExt]
to_list [axiom, in LibListExt]
TrAct1 [constructor, in HOC04DefLTS]
TrAct2 [constructor, in HOC04DefLTS]
transition [inductive, in HOC04DefLTS]
transitive_closure_equal [lemma, in HOC25Axiomatization]
trans_CHS [lemma, in HOC11TransLemmas]
trans_GV [lemma, in HOC11TransLemmas]
trans_out_wfcgr [lemma, in HOC24PreCompleteness]
trans_rem_wfcgr [lemma, in HOC24PreCompleteness]
trans_clos_trans_1n [instance, in HOC25Axiomatization]
trans_ext_cgr_full [instance, in HOC25Axiomatization]
trans_norm_full [instance, in HOC25Axiomatization]
trans_iter_abs_par_rem [lemma, in HOC18ONORbis]
trans_iter_abs_par_inst_abs [lemma, in HOC18ONORbis]
trans_iter_abs_par_in [lemma, in HOC18ONORbis]
trans_iter_abs_par_out [lemma, in HOC18ONORbis]
trans_iter_abs_par_tau [lemma, in HOC18ONORbis]
TrIn [constructor, in HOC04DefLTS]
TrOut [constructor, in HOC04DefLTS]
TrRem [constructor, in HOC04DefLTS]
TrTau1 [constructor, in HOC04DefLTS]
TrTau2 [constructor, in HOC04DefLTS]
U
unguardeds [definition, in HOC12Guarded]unguardeds_cp [lemma, in HOC12Guarded]
unguardeds_invariant [lemma, in HOC12Guarded]
unguardeds_spec [lemma, in HOC12Guarded]
Union [section, in LibFsetExt]
union_not_empty [lemma, in LibFsetExt]
union_inv [lemma, in LibFsetExt]
union_subset [lemma, in LibFsetExt]
union_empty [lemma, in LibFsetExt]
union_already_in [lemma, in LibFsetExt]
Union.A [variable, in LibFsetExt]
UpTo [constructor, in HOC13Bisimulations]
up_to_eq [lemma, in HOC13Bisimulations]
up_to [inductive, in HOC13Bisimulations]
V
var_relation_up_to [definition, in HOC13Bisimulations]var_relation [definition, in HOC13Bisimulations]
var_relation_step [definition, in HOC21Coinductive]
var_R_HO_IO [lemma, in HOC19Coincide]
W
wf [inductive, in HOC03CanonicalLemmas]WfAbs [constructor, in HOC03CanonicalLemmas]
wfcgr [definition, in HOC10CongrLemmas]
WfCgrAbs [constructor, in HOC10CongrLemmas]
WfCgrPar [constructor, in HOC10CongrLemmas]
WfCgrPar_assoc2 [constructor, in HOC10CongrLemmas]
WfCgrPar_assoc1 [constructor, in HOC10CongrLemmas]
WfCgrPar_com [constructor, in HOC10CongrLemmas]
WfCgrPar_nil2 [constructor, in HOC10CongrLemmas]
WfCgrPar_nil1 [constructor, in HOC10CongrLemmas]
WfCgrRefl [constructor, in HOC10CongrLemmas]
WfCgrSend [constructor, in HOC10CongrLemmas]
wfcgr_tr_in [lemma, in HOC27BarbedRevisited]
wfcgr_size_remove_nil [lemma, in HOC24PreCompleteness]
wfcgr_abs_par_has_nil [lemma, in HOC24PreCompleteness]
wfcgr_gvar_par_has_nil [lemma, in HOC24PreCompleteness]
wfcgr_send_par_has_nil [lemma, in HOC24PreCompleteness]
wfcgr_nil_has_top_nil [lemma, in HOC24PreCompleteness]
wfcgr_measure [lemma, in HOC25Axiomatization]
wfcgr_exists_no_free_par_nil [lemma, in HOC10CongrLemmas]
wfcgr_abs_chan_eq [lemma, in HOC10CongrLemmas]
wfcgr_send_chan_eq [lemma, in HOC10CongrLemmas]
wfcgr_top_chan [lemma, in HOC10CongrLemmas]
wfcgr_top_chan_base [lemma, in HOC10CongrLemmas]
wfcgr_alt_freshCh [lemma, in HOC10CongrLemmas]
wfcgr_freshCh_step [lemma, in HOC10CongrLemmas]
wfcgr_inst_Abs [lemma, in HOC10CongrLemmas]
wfcgr_fresh [lemma, in HOC10CongrLemmas]
wfcgr_fresh_step [lemma, in HOC10CongrLemmas]
wfcgr_subst [lemma, in HOC10CongrLemmas]
wfcgr_subst2 [lemma, in HOC10CongrLemmas]
wfcgr_subst2_step [lemma, in HOC10CongrLemmas]
wfcgr_subst1 [lemma, in HOC10CongrLemmas]
wfcgr_subst1_step [lemma, in HOC10CongrLemmas]
wfcgr_sizeP [lemma, in HOC10CongrLemmas]
wfcgr_par_assoc_r [lemma, in HOC10CongrLemmas]
wfcgr_par_assoc_l [lemma, in HOC10CongrLemmas]
wfcgr_par_com [lemma, in HOC10CongrLemmas]
wfcgr_nil_r [lemma, in HOC10CongrLemmas]
wfcgr_nil_l [lemma, in HOC10CongrLemmas]
wfcgr_par [lemma, in HOC10CongrLemmas]
wfcgr_par2 [lemma, in HOC10CongrLemmas]
wfcgr_par1 [lemma, in HOC10CongrLemmas]
wfcgr_abs [lemma, in HOC10CongrLemmas]
wfcgr_send [lemma, in HOC10CongrLemmas]
wfcgr_f_inv [lemma, in HOC10CongrLemmas]
wfcgr_step_f_inv [lemma, in HOC10CongrLemmas]
wfcgr_is_eq_rel [instance, in HOC10CongrLemmas]
wfcgr_step_sym [instance, in HOC10CongrLemmas]
wfcgr_step_refl [instance, in HOC10CongrLemmas]
wfcgr_step [inductive, in HOC10CongrLemmas]
WfGvar [constructor, in HOC03CanonicalLemmas]
WfNil [constructor, in HOC03CanonicalLemmas]
WfPar [constructor, in HOC03CanonicalLemmas]
wfprocess [record, in HOC03CanonicalLemmas]
wfprocess_prime_separation [lemma, in HOC23PrimeDecomposition]
wfprocess_list_prime_separation [lemma, in HOC23PrimeDecomposition]
wfprocess_exists_list_prime_nf [lemma, in HOC25Axiomatization]
wfprocess_eq [lemma, in HOC03CanonicalLemmas]
wfp_sizeP_nil [lemma, in HOC07SizeLemmas]
wfp_sizeP_par [lemma, in HOC07SizeLemmas]
wfp_sizeP_gvar [lemma, in HOC07SizeLemmas]
wfp_sizeP_abs [lemma, in HOC07SizeLemmas]
wfp_sizeP_send [lemma, in HOC07SizeLemmas]
wfp_size_nil [lemma, in HOC07SizeLemmas]
wfp_size_par [lemma, in HOC07SizeLemmas]
wfp_size_gvar [lemma, in HOC07SizeLemmas]
wfp_size_abs [lemma, in HOC07SizeLemmas]
wfp_size_send [lemma, in HOC07SizeLemmas]
wfp_trans_out_is_rem [lemma, in HOC11TransLemmas]
wfp_trans_rem_is_out [lemma, in HOC11TransLemmas]
wfp_trans_Msubst_name_tau [lemma, in HOC11TransLemmas]
wfp_trans_subst_name_tau [lemma, in HOC11TransLemmas]
wfp_trans_out_ex_subst [lemma, in HOC11TransLemmas]
wfp_trans_Msubst_tau [lemma, in HOC11TransLemmas]
wfp_trans_subst_tau [lemma, in HOC11TransLemmas]
wfp_subst_both [lemma, in HOC11TransLemmas]
wfp_cswap_fresh_trans_out [lemma, in HOC11TransLemmas]
wfp_swap_fresh_trans_out [lemma, in HOC11TransLemmas]
wfp_inst_chan_swap [lemma, in HOC11TransLemmas]
wfp_inst_swap [lemma, in HOC11TransLemmas]
wfp_inst_subst [lemma, in HOC11TransLemmas]
wfp_trans_subst_rem [lemma, in HOC11TransLemmas]
wfp_trans_Msubst_out [lemma, in HOC11TransLemmas]
wfp_trans_subst_out [lemma, in HOC11TransLemmas]
wfp_trans_Msubst_name_out [lemma, in HOC11TransLemmas]
wfp_trans_subst_name_out [lemma, in HOC11TransLemmas]
wfp_trans_Msubst_name_in [lemma, in HOC11TransLemmas]
wfp_trans_subst_name_in [lemma, in HOC11TransLemmas]
wfp_trans_Msubst_in [lemma, in HOC11TransLemmas]
wfp_trans_subst_in [lemma, in HOC11TransLemmas]
wfp_trans_swap_chan_tau [lemma, in HOC11TransLemmas]
wfp_trans_swap_tau [lemma, in HOC11TransLemmas]
wfp_trans_swap_chan_rem [lemma, in HOC11TransLemmas]
wfp_trans_swap_rem [lemma, in HOC11TransLemmas]
wfp_trans_swap_chan_out [lemma, in HOC11TransLemmas]
wfp_trans_swap_out [lemma, in HOC11TransLemmas]
wfp_trans_swap_chan_in [lemma, in HOC11TransLemmas]
wfp_trans_swap_inst_Abs_eq [lemma, in HOC11TransLemmas]
wfp_trans_swap_in [lemma, in HOC11TransLemmas]
wfp_decomposition_tau2 [lemma, in HOC11TransLemmas]
wfp_decomposition_tau1 [lemma, in HOC11TransLemmas]
wfp_agent_tau [lemma, in HOC11TransLemmas]
wfp_agent_rem [lemma, in HOC11TransLemmas]
wfp_agent_out [lemma, in HOC11TransLemmas]
wfp_agent_in [lemma, in HOC11TransLemmas]
wfp_unguarded_remove_iff [lemma, in HOC12Guarded]
wfp_unguardeds_cp_subst [lemma, in HOC12Guarded]
wfp_guarded_subst_trans_in [lemma, in HOC12Guarded]
wfp_guarded_remove [lemma, in HOC12Guarded]
wfp_guarded_remove_subst [lemma, in HOC12Guarded]
wfp_guarded_subst_trans_remove [lemma, in HOC12Guarded]
wfp_guarded_subst_trans_out [lemma, in HOC12Guarded]
wfp_guarded_out [lemma, in HOC12Guarded]
wfp_remove_congr [lemma, in HOC12Guarded]
wfp_not_guarded_unguarded [lemma, in HOC12Guarded]
wfp_prod_Var_par_app [lemma, in HOC23PrimeDecomposition]
wfp_prod_Var_app [lemma, in HOC23PrimeDecomposition]
wfp_prod_Var_cons [lemma, in HOC23PrimeDecomposition]
wfp_prod_Var [definition, in HOC23PrimeDecomposition]
wfp_prod_Out_par_app [lemma, in HOC23PrimeDecomposition]
wfp_prod_Out_app [lemma, in HOC23PrimeDecomposition]
wfp_prod_Out_cons [lemma, in HOC23PrimeDecomposition]
wfp_prod_Out [definition, in HOC23PrimeDecomposition]
wfp_prod_In_par_app [lemma, in HOC23PrimeDecomposition]
wfp_prod_In_app [lemma, in HOC23PrimeDecomposition]
wfp_prod_In_cons [lemma, in HOC23PrimeDecomposition]
wfp_prod_In [definition, in HOC23PrimeDecomposition]
wfp_prod_rem_compat [lemma, in HOC23PrimeDecomposition]
wfp_prod_out_compat [lemma, in HOC23PrimeDecomposition]
wfp_prod_in_compat [lemma, in HOC23PrimeDecomposition]
wfp_prod_sizeP_mem [lemma, in HOC23PrimeDecomposition]
wfp_prod_trans_in [lemma, in HOC23PrimeDecomposition]
wfp_prod_trans_out [lemma, in HOC23PrimeDecomposition]
wfp_prod_trans_rem [lemma, in HOC23PrimeDecomposition]
wfp_prod_IO_permut [lemma, in HOC23PrimeDecomposition]
wfp_prod_wfcgr_permut [lemma, in HOC23PrimeDecomposition]
wfp_prod_IO_app [lemma, in HOC23PrimeDecomposition]
wfp_prod_cons_wfp_sizeP [lemma, in HOC23PrimeDecomposition]
wfp_prod_cons_inv [lemma, in HOC23PrimeDecomposition]
wfp_prod_cons [lemma, in HOC23PrimeDecomposition]
wfp_prod [definition, in HOC23PrimeDecomposition]
wfp_sizeP_0_IO_nil [lemma, in HOC23PrimeDecomposition]
wfp_prod_components_lr [lemma, in HOC24PreCompleteness]
wfp_prod_repeat_swap [lemma, in HOC24PreCompleteness]
wfp_subst_X_prod_repeat_Abs [lemma, in HOC24PreCompleteness]
wfp_prod_repeat_subst [lemma, in HOC24PreCompleteness]
wfp_prod_repeat_SS [lemma, in HOC24PreCompleteness]
wfp_repeat [definition, in HOC24PreCompleteness]
wfp_sizeP_swap [lemma, in HOC24PreCompleteness]
wfp_sizeP_size [lemma, in HOC24PreCompleteness]
wfp_prod_in [lemma, in HOC25Axiomatization]
wfp_prod_fresh [lemma, in HOC25Axiomatization]
wfp_num_of_pars [definition, in HOC25Axiomatization]
wfp_sizeP_ordered_eq [lemma, in HOC25Axiomatization]
wfp_prod_app_wfp_sizeP [lemma, in HOC25Axiomatization]
wfp_size_ordered_le [lemma, in HOC25Axiomatization]
wfp_size_wfp_prod_lt [lemma, in HOC25Axiomatization]
wfp_size_wfp_prod_app [lemma, in HOC25Axiomatization]
wfp_prod_wfcgr_app [lemma, in HOC25Axiomatization]
wfp_prod_wfcgr_cons [lemma, in HOC25Axiomatization]
wfp_ind_set [lemma, in HOC25Axiomatization]
wfp_ind_gen [lemma, in HOC03CanonicalLemmas]
wfp_ind [lemma, in HOC03CanonicalLemmas]
wfp_sizeP [definition, in HOC03CanonicalLemmas]
wfp_size [definition, in HOC03CanonicalLemmas]
wfp_subst [definition, in HOC03CanonicalLemmas]
wfp_Nil [definition, in HOC03CanonicalLemmas]
wfp_Par [definition, in HOC03CanonicalLemmas]
wfp_Gvar [definition, in HOC03CanonicalLemmas]
wfp_Abs [definition, in HOC03CanonicalLemmas]
wfp_Send [definition, in HOC03CanonicalLemmas]
wfp_swap_nil_eq [lemma, in HOC10CongrLemmas]
wfp_sizeP_0_wfcgr_nil [lemma, in HOC10CongrLemmas]
wfp_Msubst_invariant_permut [lemma, in HOC08SubstLemmas]
wfp_closed_proc_permut [lemma, in HOC08SubstLemmas]
wfp_subst_on_inst_Abs2 [lemma, in HOC08SubstLemmas]
wfp_subst_on_inst_Abs [lemma, in HOC08SubstLemmas]
wfp_mult_sub_Abs [lemma, in HOC08SubstLemmas]
wfp_mult_sub_par [lemma, in HOC08SubstLemmas]
wfp_mult_sub_commute3 [lemma, in HOC08SubstLemmas]
wfp_mult_sub_commute1 [lemma, in HOC08SubstLemmas]
wfp_mult_sub_separate2 [lemma, in HOC08SubstLemmas]
wfp_mult_sub_commute [lemma, in HOC08SubstLemmas]
wfp_subst_on_pipe [lemma, in HOC08SubstLemmas]
wfp_subst_comm_cp [lemma, in HOC08SubstLemmas]
wfp_swap_chan_on_subst1 [lemma, in HOC08SubstLemmas]
wfp_fresh_chan_swap [lemma, in HOC08SubstLemmas]
wfp_fresh_Msubst_lemma [lemma, in HOC08SubstLemmas]
wfp_subst_on_subst_same [lemma, in HOC08SubstLemmas]
wfp_gfresh_swap_rewrite [lemma, in HOC08SubstLemmas]
wfp_subst_on_swap [lemma, in HOC08SubstLemmas]
wfp_swap_on_subst [lemma, in HOC08SubstLemmas]
wfp_swap_chan_on_subst [lemma, in HOC08SubstLemmas]
wfp_swap_equal [lemma, in HOC08SubstLemmas]
wfp_swap_chan_equal [lemma, in HOC08SubstLemmas]
wfp_closed_pipe [lemma, in HOC09GVLemmas]
wfp_GV_pipe_nil [lemma, in HOC09GVLemmas]
wfp_GV_pipe_par [lemma, in HOC09GVLemmas]
wfp_GV_pipe_gvar2 [lemma, in HOC09GVLemmas]
wfp_GV_pipe_gvar1 [lemma, in HOC09GVLemmas]
wfp_GV_pipe_abs2 [lemma, in HOC09GVLemmas]
wfp_GV_pipe_abs1 [lemma, in HOC09GVLemmas]
wfp_GV_pipe_send [lemma, in HOC09GVLemmas]
wfp_GV_pipe_ch [lemma, in HOC09GVLemmas]
wfp_GV_Abs [lemma, in HOC09GVLemmas]
wfp_Msubst_subst_subset [lemma, in HOC09GVLemmas]
wfp_GV_Msubst_cp [lemma, in HOC09GVLemmas]
wfp_subst_eq_rewrite [lemma, in HOC05WFProcesses]
wfp_trans_in_abs_eq [lemma, in HOC05WFProcesses]
wfp_trans_in_chan_eq [lemma, in HOC05WFProcesses]
wfp_eq_subst_abs3 [lemma, in HOC05WFProcesses]
wfp_eq_subst_abs2 [lemma, in HOC05WFProcesses]
wfp_eq_subst_abs1 [lemma, in HOC05WFProcesses]
wfp_Abs_equal [lemma, in HOC05WFProcesses]
wfp_Abs_eq [lemma, in HOC05WFProcesses]
wfp_subst_lvar_XY [lemma, in HOC05WFProcesses]
wfp_subst_lvar [lemma, in HOC05WFProcesses]
wfp_par2_extract [lemma, in HOC05WFProcesses]
wfp_par1_extract [lemma, in HOC05WFProcesses]
wfp_prod_repeat_S [lemma, in HOC05WFProcesses]
wfp_prod_repeat_0 [lemma, in HOC05WFProcesses]
wfp_subst_decomposition_g [lemma, in HOC05WFProcesses]
wfp_subst_on_subst [lemma, in HOC05WFProcesses]
wfp_substs_commute_gg [lemma, in HOC05WFProcesses]
wfp_gfresh_subst_is_swap [lemma, in HOC05WFProcesses]
wfp_subst_gvar_idem [lemma, in HOC05WFProcesses]
wfp_gfresh_subst_rewrite [lemma, in HOC05WFProcesses]
wfp_fresh_Msubst1 [lemma, in HOC05WFProcesses]
wfp_eq_swap_chan_nil [lemma, in HOC05WFProcesses]
wfp_eq_swap_chan_par [lemma, in HOC05WFProcesses]
wfp_eq_swap_chan_gvar [lemma, in HOC05WFProcesses]
wfp_eq_swap_chan_abs [lemma, in HOC05WFProcesses]
wfp_eq_swap_chan_send [lemma, in HOC05WFProcesses]
wfp_eq_subst_nil [lemma, in HOC05WFProcesses]
wfp_eq_subst_par [lemma, in HOC05WFProcesses]
wfp_eq_subst_gvar [lemma, in HOC05WFProcesses]
wfp_eq_subst_send [lemma, in HOC05WFProcesses]
wfp_swap_chan_involutive [lemma, in HOC05WFProcesses]
wfp_eq_swap_nil [lemma, in HOC05WFProcesses]
wfp_eq_swap_par [lemma, in HOC05WFProcesses]
wfp_eq_swap_gvar [lemma, in HOC05WFProcesses]
wfp_eq_swap_abs [lemma, in HOC05WFProcesses]
wfp_eq_swap_send [lemma, in HOC05WFProcesses]
wfp_swap_involutive [lemma, in HOC05WFProcesses]
wfp_swap_sym [lemma, in HOC05WFProcesses]
wfp_permut_opl_iff [lemma, in HOC05WFProcesses]
wfp_opl_mem_combine_iff [lemma, in HOC05WFProcesses]
wfp_opl_mem [lemma, in HOC05WFProcesses]
wfp_Forall_cfresh_neq [lemma, in HOC05WFProcesses]
wfp_opl_app_ex [lemma, in HOC05WFProcesses]
wfp_opl_base [lemma, in HOC05WFProcesses]
wfp_permut_opl [lemma, in HOC05WFProcesses]
wfp_rem1_opl [lemma, in HOC05WFProcesses]
wfp_nodup_opl [lemma, in HOC05WFProcesses]
wfp_mem_opl [lemma, in HOC05WFProcesses]
wfp_mem_opl_inv [lemma, in HOC05WFProcesses]
wfp_opl_inv [lemma, in HOC05WFProcesses]
wfp_opl_app [lemma, in HOC05WFProcesses]
wfp_cpl_opl [lemma, in HOC05WFProcesses]
wfp_length_opl [lemma, in HOC05WFProcesses]
wfp_out_proc_list [definition, in HOC05WFProcesses]
wfp_multisubst_to_subst_tail [lemma, in HOC05WFProcesses]
wfp_multisubst_to_subst [lemma, in HOC05WFProcesses]
wfp_pipe_to_Abs [lemma, in HOC05WFProcesses]
wfp_pipe_eq_nil [lemma, in HOC05WFProcesses]
wfp_find_fresh_chan [lemma, in HOC05WFProcesses]
wfp_cpl_app_inv [lemma, in HOC05WFProcesses]
wfp_permut_cp_list [lemma, in HOC05WFProcesses]
wfp_cpl_cpl [lemma, in HOC05WFProcesses]
wfp_cpl_forall [lemma, in HOC05WFProcesses]
wfp_prod_repeat [definition, in HOC05WFProcesses]
wfp_swap_chan [definition, in HOC05WFProcesses]
wfp_swap [definition, in HOC05WFProcesses]
wfp_multisubst [definition, in HOC05WFProcesses]
wfp_pipe [definition, in HOC05WFProcesses]
wfp_list_proc_len [lemma, in HOC05WFProcesses]
wfp_inst_Abs [definition, in HOC04DefLTS]
wfp_cfresh_out_inv [lemma, in HOC06FreshLemmas]
wfp_cfresh_Msubst1 [lemma, in HOC06FreshLemmas]
wfp_cfresh_tau [lemma, in HOC06FreshLemmas]
wfp_cfresh_rem [lemma, in HOC06FreshLemmas]
wfp_cfresh_out [lemma, in HOC06FreshLemmas]
wfp_cfresh_in [lemma, in HOC06FreshLemmas]
wfp_fresh_inst_Abs [lemma, in HOC06FreshLemmas]
wfp_fresh_gvar_cswap [lemma, in HOC06FreshLemmas]
wfp_fresh_chan_gswap [lemma, in HOC06FreshLemmas]
wfp_fresh_chan_cswap [lemma, in HOC06FreshLemmas]
wfp_fresh_Msubst [lemma, in HOC06FreshLemmas]
wfp_fresh_cp [lemma, in HOC06FreshLemmas]
wfp_cfresh_subst_from2 [lemma, in HOC06FreshLemmas]
wfp_cfresh_msubst_from [lemma, in HOC06FreshLemmas]
wfp_cfresh_subst_from1 [lemma, in HOC06FreshLemmas]
wfp_cfresh_subst_in [lemma, in HOC06FreshLemmas]
wfp_cfresh_swap_inv [lemma, in HOC06FreshLemmas]
wfp_cfresh_pipe_cons [lemma, in HOC06FreshLemmas]
wfp_cfresh_pipe [lemma, in HOC06FreshLemmas]
wfp_cfresh_Abs [lemma, in HOC06FreshLemmas]
wfp_cfresh_par_iff [lemma, in HOC06FreshLemmas]
wfp_gfresh_Abs [lemma, in HOC06FreshLemmas]
wfp_sizeP_out_S_tr [lemma, in HOC18ONORbis]
wfp_sizeP_out [definition, in HOC18ONORbis]
wfp_sizeO [definition, in HOC18ONORbis]
wfp_sizeP_S_tr [lemma, in HOC14IObis]
wfp_guarded_IObis [lemma, in HOC14IObis]
WfSend [constructor, in HOC03CanonicalLemmas]
wf_characterize_set [lemma, in HOC25Axiomatization]
wf_decidable [instance, in HOC03CanonicalLemmas]
wf_characterize [lemma, in HOC03CanonicalLemmas]
wf_cond [projection, in HOC03CanonicalLemmas]
wf_receive_part1 [lemma, in HOC03CanonicalLemmas]
wf_receive [lemma, in HOC03CanonicalLemmas]
wf_subst [lemma, in HOC03CanonicalLemmas]
wf_ind_gen [lemma, in HOC03CanonicalLemmas]
wf_prod_repeat [lemma, in HOC03CanonicalLemmas]
wf_chan_swap [lemma, in HOC03CanonicalLemmas]
wf_swapping [lemma, in HOC03CanonicalLemmas]
wf_par2 [lemma, in HOC03CanonicalLemmas]
wf_par1 [lemma, in HOC03CanonicalLemmas]
wf_lfresh [lemma, in HOC03CanonicalLemmas]
wf_LV [lemma, in HOC03CanonicalLemmas]
wf_send [lemma, in HOC03CanonicalLemmas]
X
xEGood [lemma, in HOC03CanonicalLemmas]XHE [definition, in HOC03CanonicalLemmas]
XHE_GoodF [lemma, in HOC03CanonicalLemmas]
XHF [definition, in HOC03CanonicalLemmas]
XHF_GoodF [lemma, in HOC03CanonicalLemmas]
XHP [definition, in HOC03CanonicalLemmas]
XHP_GoodF [lemma, in HOC03CanonicalLemmas]
X_der_ok [lemma, in HOC22Decidability]
X_der [definition, in HOC22Decidability]
X_der_aux_eq [lemma, in HOC22Decidability]
X_der_aux [definition, in HOC22Decidability]
other
_ ≈*NOR _ [notation, in HOC13Bisimulations]_ ≈*CON _ [notation, in HOC13Bisimulations]
_ ≈*HO _ [notation, in HOC13Bisimulations]
_ ≈ONOR _ [notation, in HOC13Bisimulations]
_ ≈NOR _ [notation, in HOC13Bisimulations]
_ ≈CON _ [notation, in HOC13Bisimulations]
_ ≈HO _ [notation, in HOC13Bisimulations]
_ ≈ _ [notation, in HOC13Bisimulations]
_ ≡E _ [notation, in HOC25Axiomatization]
_ -≡->* _ [notation, in HOC25Axiomatization]
_ -≡-> _ [notation, in HOC25Axiomatization]
_ --->* _ [notation, in HOC25Axiomatization]
_ ---> _ [notation, in HOC25Axiomatization]
_ ≡* _ [notation, in HOC10CongrLemmas]
_ ≡ _ [notation, in HOC10CongrLemmas]
_ ≈ei _ [notation, in HOC21Coinductive]
_ ≈ec _ [notation, in HOC21Coinductive]
_ ≈i _ [notation, in HOC21Coinductive]
_ ≈c _ [notation, in HOC21Coinductive]
_ e≈NOR _ [notation, in HOC26EarlyBisimulation]
_ e≈ _ [notation, in HOC26EarlyBisimulation]
_ ### _ [notation, in HOC01Defs]
_ ## _ [notation, in HOC01Defs]
_ # _ [notation, in HOC01Defs]
@@ _ [notation, in HOC12Guarded]
[ _ ] _ [notation, in HOC05WFProcesses]
[ _ /// _ ] _ [notation, in HOC01Defs]
[ _ // _ ] _ [notation, in HOC01Defs]
^ _ [notation, in HOC01Defs]
{{ _ -- _ ->> _ }} [notation, in HOC04DefLTS]
{{ _ , _ }} _ [notation, in HOC01Defs]
{{[ _ , _ ]}} _ [notation, in HOC01Defs]
{{| _ , _ |}} _ [notation, in HOC01Defs]
| _ , _ | _ [notation, in HOC01Defs]
¬¬ _ [notation, in HOC05WFProcesses]
Notation Index
other
_ ≈*NOR _ [in HOC13Bisimulations]_ ≈*CON _ [in HOC13Bisimulations]
_ ≈*HO _ [in HOC13Bisimulations]
_ ≈ONOR _ [in HOC13Bisimulations]
_ ≈NOR _ [in HOC13Bisimulations]
_ ≈CON _ [in HOC13Bisimulations]
_ ≈HO _ [in HOC13Bisimulations]
_ ≈ _ [in HOC13Bisimulations]
_ ≡E _ [in HOC25Axiomatization]
_ -≡->* _ [in HOC25Axiomatization]
_ -≡-> _ [in HOC25Axiomatization]
_ --->* _ [in HOC25Axiomatization]
_ ---> _ [in HOC25Axiomatization]
_ ≡* _ [in HOC10CongrLemmas]
_ ≡ _ [in HOC10CongrLemmas]
_ ≈ei _ [in HOC21Coinductive]
_ ≈ec _ [in HOC21Coinductive]
_ ≈i _ [in HOC21Coinductive]
_ ≈c _ [in HOC21Coinductive]
_ e≈NOR _ [in HOC26EarlyBisimulation]
_ e≈ _ [in HOC26EarlyBisimulation]
_ ### _ [in HOC01Defs]
_ ## _ [in HOC01Defs]
_ # _ [in HOC01Defs]
@@ _ [in HOC12Guarded]
[ _ ] _ [in HOC05WFProcesses]
[ _ /// _ ] _ [in HOC01Defs]
[ _ // _ ] _ [in HOC01Defs]
^ _ [in HOC01Defs]
{{ _ -- _ ->> _ }} [in HOC04DefLTS]
{{ _ , _ }} _ [in HOC01Defs]
{{[ _ , _ ]}} _ [in HOC01Defs]
{{| _ , _ |}} _ [in HOC01Defs]
| _ , _ | _ [in HOC01Defs]
¬¬ _ [in HOC05WFProcesses]
Variable Index
B
Basic.A [in LibFsetExt]C
Count.A [in LibListExt]D
Defs.A [in LibListExt]Defs.B [in LibListExt]
F
FromList.A [in LibFsetExt]I
Inter.A [in LibFsetExt]L
ListBasic.A [in LibListExt]N
NoDup.A [in LibListExt]P
Permutation.A [in LibListExt]Permutation.B [in LibListExt]
Permutation2.A [in LibListExt]
Permutation2.B [in LibListExt]
R
RemDup.A [in LibListExt]RemoveOne.A [in LibListExt]
Remove.A [in LibFsetExt]
S
SplitCombine.A [in LibListExt]SplitCombine.B [in LibListExt]
SubLists.A [in LibListExt]
SubLists.B [in LibListExt]
Subset.A [in LibFsetExt]
T
ToList.A [in LibListExt]U
Union.A [in LibFsetExt]Library Index
A
auxH
HOC01DefsHOC02BaseLemmas
HOC03CanonicalLemmas
HOC04DefLTS
HOC05WFProcesses
HOC06FreshLemmas
HOC07SizeLemmas
HOC08SubstLemmas
HOC09GVLemmas
HOC10CongrLemmas
HOC11TransLemmas
HOC12Guarded
HOC13Bisimulations
HOC14IObis
HOC15HObis
HOC16CONbis
HOC17NORbis
HOC18ONORbis
HOC19Coincide
HOC20Barbed
HOC21Coinductive
HOC22Decidability
HOC23PrimeDecomposition
HOC24PreCompleteness
HOC25Axiomatization
HOC26EarlyBisimulation
HOC27BarbedRevisited
L
LibFsetExtLibListExt
Lemma Index
A
Abs_from_Receive_spec [in HOC22Decidability]abs_not_prime [in HOC25Axiomatization]
Abs_eq [in HOC03CanonicalLemmas]
abs_wfcgr_no_nil [in HOC10CongrLemmas]
abs_wfcgr_inv [in HOC10CongrLemmas]
abs_core_wfcgr [in HOC10CongrLemmas]
act1_tau [in HOC11TransLemmas]
act1_rem [in HOC11TransLemmas]
act1_out [in HOC11TransLemmas]
act1_in [in HOC11TransLemmas]
act2_tau [in HOC11TransLemmas]
act2_rem [in HOC11TransLemmas]
act2_out [in HOC11TransLemmas]
act2_in [in HOC11TransLemmas]
async_barbed_to_order_oiv [in HOC27BarbedRevisited]
async_barbed_out_1 [in HOC27BarbedRevisited]
async_barbed_out_normal_early [in HOC27BarbedRevisited]
async_barbed_swap [in HOC27BarbedRevisited]
async_barbed_swap_fresh [in HOC27BarbedRevisited]
async_barbed_congr_abs_inv [in HOC27BarbedRevisited]
async_barbed_congr_send_inv [in HOC27BarbedRevisited]
async_barbed_congr_par [in HOC27BarbedRevisited]
async_barbed_congr_par_r [in HOC27BarbedRevisited]
async_barbed_congr_par_l [in HOC27BarbedRevisited]
async_barbed_congr_abs [in HOC27BarbedRevisited]
async_barbed_congr_send [in HOC27BarbedRevisited]
async_barbed_congr_par_assoc_r [in HOC27BarbedRevisited]
async_barbed_congr_par_assoc_l [in HOC27BarbedRevisited]
async_barbed_congr_par_com [in HOC27BarbedRevisited]
async_barbed_congr_nil_r [in HOC27BarbedRevisited]
async_barbed_congr_nil_l [in HOC27BarbedRevisited]
async_barbed_out_barb_preserving [in HOC20Barbed]
async_barbed_context_closed [in HOC20Barbed]
async_barbed_tau [in HOC20Barbed]
aux_fresh_rem [in HOC19Coincide]
B
bio_ok [in HOC22Decidability]bio_aux_ok2 [in HOC22Decidability]
bio_aux_ok1 [in HOC22Decidability]
C
cfresh_NORbis [in HOC17NORbis]cfresh_send_nil [in HOC02BaseLemmas]
cfresh_nil [in HOC02BaseLemmas]
cfresh_par_iff [in HOC02BaseLemmas]
cfresh_gvar [in HOC02BaseLemmas]
cfresh_lvar [in HOC02BaseLemmas]
cfresh_receive [in HOC02BaseLemmas]
cfresh_send [in HOC02BaseLemmas]
cfresh_iter_abs_par [in HOC18ONORbis]
cfresh_ONORbis [in HOC18ONORbis]
change_channel [in HOC15HObis]
change_NOR_channel [in HOC17NORbis]
chan_gen_spec [in HOC01Defs]
chan_gen_list_spec [in HOC01Defs]
combine_count_2_snd [in LibListExt]
combine_count_2_fst [in LibListExt]
combine_remdup_count_snd [in LibListExt]
combine_remdup_count_fst [in LibListExt]
combine_remdup_snd [in LibListExt]
combine_remdup_snd_iff [in LibListExt]
combine_remdup_fst_iff [in LibListExt]
combine_exists_snd [in LibListExt]
combine_exists_fst [in LibListExt]
combine_nodup_pair_unique_snd [in LibListExt]
combine_nodup_pair_unique_fst [in LibListExt]
combine_equal_inv [in LibListExt]
combine_equal_inv_r [in LibListExt]
combine_equal_inv_l [in LibListExt]
combine_inv [in LibListExt]
combine_split [in LibListExt]
completeness_lr [in HOC25Axiomatization]
components_eq_nil [in HOC24PreCompleteness]
components_eq_par [in HOC24PreCompleteness]
components_eq_gvar [in HOC24PreCompleteness]
components_eq_abs [in HOC24PreCompleteness]
components_eq_send [in HOC24PreCompleteness]
components_eq [in HOC24PreCompleteness]
components_wfp_prod [in HOC25Axiomatization]
CONbisC_closed [in HOC16CONbis]
CONbisC_out_context [in HOC16CONbis]
CONbisC_tau [in HOC16CONbis]
CONbisC_sym [in HOC16CONbis]
CONbisC_out_normal [in HOC19Coincide]
CONbisC_in_normal [in HOC19Coincide]
CONbisE_NORbisE [in HOC19Coincide]
CONbis_closed [in HOC16CONbis]
CONbis_out_context [in HOC16CONbis]
CONbis_tau [in HOC16CONbis]
CONbis_sym [in HOC16CONbis]
CONbis_NORbis [in HOC19Coincide]
CONbis_CONbis [in HOC19Coincide]
congr_async_barbed [in HOC27BarbedRevisited]
congr_async_barbed_relation [in HOC27BarbedRevisited]
congr_out_barb_preserving [in HOC27BarbedRevisited]
congr_context_closed [in HOC27BarbedRevisited]
congr_CONbisimulation [in HOC13Bisimulations]
congr_ONORbisimulation [in HOC13Bisimulations]
congr_NORbisimulation [in HOC13Bisimulations]
congr_HObisimulation [in HOC13Bisimulations]
congr_IObisimulation [in HOC13Bisimulations]
congr_out_context [in HOC13Bisimulations]
congr_out_context_strong [in HOC13Bisimulations]
congr_closed [in HOC13Bisimulations]
congr_in_normal [in HOC13Bisimulations]
congr_out_normal [in HOC13Bisimulations]
congr_out_normal_strong [in HOC13Bisimulations]
congr_tau [in HOC13Bisimulations]
congr_rem [in HOC13Bisimulations]
congr_out [in HOC13Bisimulations]
congr_in [in HOC13Bisimulations]
congr_in_strong [in HOC13Bisimulations]
congr_swap [in HOC10CongrLemmas]
congr_IObis [in HOC14IObis]
core_remove_par_nils [in HOC24PreCompleteness]
core_none_char [in HOC24PreCompleteness]
core_remove_nil_invariant [in HOC24PreCompleteness]
core_norm_full_none [in HOC25Axiomatization]
core_norm_full_gvar [in HOC25Axiomatization]
core_norm_full_send [in HOC25Axiomatization]
core_par_assoc_r [in HOC10CongrLemmas]
core_par_assoc_l [in HOC10CongrLemmas]
core_par_com [in HOC10CongrLemmas]
core_par_sizeP_0 [in HOC10CongrLemmas]
core_eq_par [in HOC10CongrLemmas]
core_eq_nil [in HOC10CongrLemmas]
core_eq_gvar [in HOC10CongrLemmas]
core_eq_abs [in HOC10CongrLemmas]
core_eq_send [in HOC10CongrLemmas]
Core_eq [in HOC10CongrLemmas]
count_length [in LibListExt]
count_removeOne_neg [in LibListExt]
count_removeOne_pos [in LibListExt]
count_app_plus [in LibListExt]
count_Mem [in LibListExt]
count_cons_cancel [in LibListExt]
count_cons_pos [in LibListExt]
count_nil [in LibListExt]
cp_subst_dist [in HOC11TransLemmas]
cp_trans_tau [in HOC09GVLemmas]
cp_trans_out [in HOC09GVLemmas]
cp_trans_in [in HOC09GVLemmas]
cp_abs [in HOC09GVLemmas]
cp_par [in HOC09GVLemmas]
D
deep_prime_decomposition_unique [in HOC24PreCompleteness]deep_prime_decomposition_exists [in HOC24PreCompleteness]
dpd_remove_par_nils [in HOC24PreCompleteness]
dpd_components_prime [in HOC24PreCompleteness]
dpd_congr_invariant [in HOC24PreCompleteness]
dpd_equiv_par_nil [in HOC24PreCompleteness]
dpd_remove_nil_congr [in HOC24PreCompleteness]
dpd_implies_pd [in HOC24PreCompleteness]
dpd_eq_abs [in HOC24PreCompleteness]
dpd_gswap [in HOC24PreCompleteness]
dpd_eq_nil [in HOC24PreCompleteness]
dpd_eq_par [in HOC24PreCompleteness]
dpd_eq_gvar [in HOC24PreCompleteness]
dpd_eq_send [in HOC24PreCompleteness]
dpd_eq [in HOC24PreCompleteness]
dpd_wfp_prod_app [in HOC25Axiomatization]
dpd_components_normal_form [in HOC25Axiomatization]
dpd_normal_form [in HOC25Axiomatization]
dpd_no_red_base [in HOC25Axiomatization]
E
empty_dec [in LibFsetExt]ext_cgr_red [in HOC25Axiomatization]
ext_cgr_asymmetric [in HOC25Axiomatization]
ext_cgr_irreflexive [in HOC25Axiomatization]
ext_cgr_full_measure [in HOC25Axiomatization]
ext_cgr_step_measure [in HOC25Axiomatization]
ext_cgr_full_remove_par_nils [in HOC25Axiomatization]
ext_cgr_step_remove_par_nils [in HOC25Axiomatization]
ext_cgr_full_remove_par_nils_rr_lr [in HOC25Axiomatization]
ext_cgr_step_remove_par_nils_rr_eq [in HOC25Axiomatization]
ex_fresh_gvar [in HOC01Defs]
E_subst_inv [in HOC02BaseLemmas]
F
false_trans_rem [in HOC11TransLemmas]false_trans_out [in HOC11TransLemmas]
false_trans_in [in HOC11TransLemmas]
find_fresh_chan_n [in HOC01Defs]
find_fresh_chan [in HOC01Defs]
find_fresh [in HOC01Defs]
Forall_subset [in LibListExt]
Forall_mem [in LibListExt]
Forall_forall [in LibListExt]
Forall_Mem [in LibListExt]
fresh_gvar_swap_chan [in HOC09GVLemmas]
fresh_LV [in HOC02BaseLemmas]
fresh_GV [in HOC02BaseLemmas]
fresh_iter_abs_par [in HOC18ONORbis]
fresh_CHSs [in HOC01Defs]
fresh_set [in HOC01Defs]
from_to_list_union [in LibListExt]
from_list_rem1 [in LibListExt]
from_list_app [in LibFsetExt]
from_list_base [in LibFsetExt]
from_list_spec [in LibFsetExt]
from_list_notin [in LibFsetExt]
from_union_to_rem [in LibFsetExt]
from_rem_to_union [in LibFsetExt]
fset_nodup [in LibListExt]
fset_eq_sub [in LibFsetExt]
fset_neq [in LibFsetExt]
fst_split [in LibListExt]
fst_split_step [in LibListExt]
fst_split_cons [in LibListExt]
f_is_good [in HOC03CanonicalLemmas]
G
get_Abs_from_Receive [in HOC22Decidability]get_ins_wfp_prod_app [in HOC25Axiomatization]
get_outs_wfp_prod_app [in HOC25Axiomatization]
get_vars_wfp_prod_app [in HOC25Axiomatization]
get_ins_sizeP [in HOC25Axiomatization]
get_outs_sizeP [in HOC25Axiomatization]
get_vars_sizeP [in HOC25Axiomatization]
get_ins_spec [in HOC25Axiomatization]
get_ins_eq_nil [in HOC25Axiomatization]
get_ins_eq_par [in HOC25Axiomatization]
get_ins_eq_gvar [in HOC25Axiomatization]
get_ins_eq_abs [in HOC25Axiomatization]
get_ins_eq_send [in HOC25Axiomatization]
get_ins_eq [in HOC25Axiomatization]
get_outs_spec [in HOC25Axiomatization]
get_outs_eq_nil [in HOC25Axiomatization]
get_outs_eq_par [in HOC25Axiomatization]
get_outs_eq_gvar [in HOC25Axiomatization]
get_outs_eq_abs [in HOC25Axiomatization]
get_outs_eq_send [in HOC25Axiomatization]
get_outs_eq [in HOC25Axiomatization]
get_vars_spec [in HOC25Axiomatization]
get_vars_eq_nil [in HOC25Axiomatization]
get_vars_eq_par [in HOC25Axiomatization]
get_vars_eq_gvar [in HOC25Axiomatization]
get_vars_eq_abs [in HOC25Axiomatization]
get_vars_eq_send [in HOC25Axiomatization]
get_vars_eq [in HOC25Axiomatization]
gfresh_E_empty [in HOC02BaseLemmas]
gfresh_subst_involutive [in HOC02BaseLemmas]
gfresh_subst_is_swap [in HOC02BaseLemmas]
gfresh_swap_inv [in HOC02BaseLemmas]
gfresh_swap_rewrite [in HOC02BaseLemmas]
gfresh_subst_rewrite [in HOC02BaseLemmas]
gfresh_in_self_subst [in HOC02BaseLemmas]
gfresh_in_lsubst_p_q [in HOC02BaseLemmas]
gfresh_in_subst_p_q [in HOC02BaseLemmas]
gfresh_from_lsubst [in HOC02BaseLemmas]
gfresh_from_subst [in HOC02BaseLemmas]
gfresh_nil [in HOC02BaseLemmas]
gfresh_par_iff [in HOC02BaseLemmas]
gfresh_gvar [in HOC02BaseLemmas]
gfresh_lvar [in HOC02BaseLemmas]
gfresh_receive [in HOC02BaseLemmas]
gfresh_send [in HOC02BaseLemmas]
gfresh_ONORbis [in HOC18ONORbis]
gfresh_IObis [in HOC14IObis]
GoodFresh [in HOC03CanonicalLemmas]
GoodFresh_iff [in HOC03CanonicalLemmas]
Good_chan_swap [in HOC03CanonicalLemmas]
Good0 [in HOC03CanonicalLemmas]
guarded_size_unguardedX [in HOC12Guarded]
guarding_HObisE [in HOC15HObis]
gvar_wfcgr_inv [in HOC10CongrLemmas]
gvar_core_wfcgr [in HOC10CongrLemmas]
GV_union_included [in HOC22Decidability]
GV_trans_tau [in HOC09GVLemmas]
GV_trans_rem2 [in HOC09GVLemmas]
GV_trans_rem1 [in HOC09GVLemmas]
GV_trans_out [in HOC09GVLemmas]
GV_trans_in_sub [in HOC09GVLemmas]
GV_trans_in [in HOC09GVLemmas]
GV_trans_in_const [in HOC09GVLemmas]
GV_subst_cp [in HOC09GVLemmas]
GV_swap_chan [in HOC09GVLemmas]
GV_swap [in HOC09GVLemmas]
GV_subst [in HOC02BaseLemmas]
H
has_top_nil_num_of_pars_ordered [in HOC25Axiomatization]has_top_nil_sizeP_0 [in HOC25Axiomatization]
has_top_nil_ordered [in HOC25Axiomatization]
has_top_nil_get_ins [in HOC25Axiomatization]
has_top_nil_get_outs [in HOC25Axiomatization]
has_top_nil_get_vars [in HOC25Axiomatization]
has_top_nil_wfp_prod_app [in HOC25Axiomatization]
has_free_par_nil_par [in HOC25Axiomatization]
has_free_par_nil_abs [in HOC10CongrLemmas]
has_free_par_nil_lsubst [in HOC10CongrLemmas]
has_top_has_free_nil [in HOC10CongrLemmas]
has_top_nil_sizeP_0 [in HOC10CongrLemmas]
has_top_nil_eq_nil [in HOC10CongrLemmas]
has_top_nil_eq_par [in HOC10CongrLemmas]
has_top_nil_eq_gvar [in HOC10CongrLemmas]
has_top_nil_eq_abs [in HOC10CongrLemmas]
has_top_nil_eq_send [in HOC10CongrLemmas]
has_top_nil_eq [in HOC10CongrLemmas]
HObicC_var [in HOC15HObis]
HObisC_trans [in HOC15HObis]
HObisC_closed [in HOC15HObis]
HObisC_out [in HOC15HObis]
HObisC_tau [in HOC15HObis]
HObisC_sym [in HOC15HObis]
HObisC_out_context [in HOC19Coincide]
HObisE_Msubst [in HOC15HObis]
HObisE_subst [in HOC15HObis]
HObisE_sym [in HOC15HObis]
HObisE_equiv [in HOC15HObis]
HObisE_CONbisE [in HOC19Coincide]
HObisE_unguardeds_eq [in HOC19Coincide]
HObisE_IObis [in HOC19Coincide]
HObisR_r [in HOC15HObis]
HObisR_ch [in HOC15HObis]
HObis_congr_send [in HOC15HObis]
HObis_congr_abs [in HOC15HObis]
HObis_congr_par_nil [in HOC15HObis]
HObis_trans [in HOC15HObis]
HObis_congr_receive [in HOC15HObis]
HObis_closed [in HOC15HObis]
HObis_out [in HOC15HObis]
HObis_tau [in HOC15HObis]
HObis_sym [in HOC15HObis]
HObis_refl [in HOC15HObis]
HObis_CONbis [in HOC19Coincide]
HObis_IObis [in HOC19Coincide]
HObis_HObis [in HOC19Coincide]
HOCore_Sound_Complete [in HOC25Axiomatization]
HO_HOE [in HOC15HObis]
I
inst_abs_subst_eq [in HOC22Decidability]inter_empty_subset [in LibFsetExt]
inter_not_empty_exists [in LibFsetExt]
inter_remove [in LibFsetExt]
inter_union [in LibFsetExt]
in_der_ok_lr [in HOC22Decidability]
in_der_ok_rl [in HOC22Decidability]
in_der_aux_eq [in HOC22Decidability]
in_nor_forall_exists [in HOC17NORbis]
in_and_notin [in LibFsetExt]
in_up_to_forall_exists [in HOC14IObis]
in_full_forall [in HOC14IObis]
in_forall_exists [in HOC14IObis]
in_R_HO_IO [in HOC19Coincide]
IObisC_ex_eq_IObisI_ex [in HOC21Coinductive]
IObisC_eq_IObisI [in HOC21Coinductive]
IObisim_ex_up_to_IObisim_up_to_when_swap [in HOC14IObis]
IObisim_ex_IObisim_when_swap [in HOC14IObis]
IObisI_ex_eq_IObis_ex [in HOC21Coinductive]
IObisI_ex_var [in HOC21Coinductive]
IObisI_ex_out [in HOC21Coinductive]
IObisI_ex_in_ex [in HOC21Coinductive]
IObisI_ex_sym [in HOC21Coinductive]
IObisI_eq_IObis [in HOC21Coinductive]
IObisI_var [in HOC21Coinductive]
IObisI_out [in HOC21Coinductive]
IObisI_in [in HOC21Coinductive]
IObisI_sym [in HOC21Coinductive]
IObis_decidable [in HOC22Decidability]
IObis_constructive_decidable [in HOC22Decidability]
IObis_cancellation [in HOC23PrimeDecomposition]
IObis_wfcgr_nil_iff [in HOC24PreCompleteness]
IObis_abs_inv_body [in HOC25Axiomatization]
IObis_abs_inv_var [in HOC25Axiomatization]
IObis_abs_inv_ch [in HOC25Axiomatization]
IObis_cancellation_stronger [in HOC25Axiomatization]
IObis_ex_eq_IObisC_ex [in HOC21Coinductive]
IObis_eq_IObisC [in HOC21Coinductive]
IObis_async_barbed_lr [in HOC20Barbed]
IObis_eIObis [in HOC26EarlyBisimulation]
IObis_in_full [in HOC14IObis]
IObis_unguardeds_eq [in HOC14IObis]
IObis_tau [in HOC14IObis]
IObis_subst [in HOC14IObis]
IObis_subst2 [in HOC14IObis]
IObis_subst1 [in HOC14IObis]
IObis_congr_par [in HOC14IObis]
IObis_par_assoc_r [in HOC14IObis]
IObis_par_assoc_l [in HOC14IObis]
IObis_congr_par_com [in HOC14IObis]
IObis_congr_nil_r [in HOC14IObis]
IObis_congr_nil_l [in HOC14IObis]
IObis_congr_par1 [in HOC14IObis]
IObis_congr_abs [in HOC14IObis]
IObis_congr_send [in HOC14IObis]
IObis_ex_up_to_IObis_up_to [in HOC14IObis]
IObis_IObis_ex [in HOC14IObis]
IObis_sizeP_eq [in HOC14IObis]
IObis_size_unguardedX [in HOC14IObis]
IObis_swap [in HOC14IObis]
IObis_up_to_cgr_IObis [in HOC14IObis]
IObis_up_to_IObis [in HOC14IObis]
IObis_trans [in HOC14IObis]
IObis_var [in HOC14IObis]
IObis_out [in HOC14IObis]
IObis_in [in HOC14IObis]
IObis_sym [in HOC14IObis]
IObis_refl [in HOC14IObis]
IObis_HObis_cp [in HOC19Coincide]
IObis_RHOIO [in HOC19Coincide]
IObis_HObisE [in HOC19Coincide]
IObis_HObis [in HOC19Coincide]
IObis_congr_pipe [in HOC19Coincide]
IObis_closed [in HOC19Coincide]
IObis_IObis [in HOC19Coincide]
IO_pw_wfp_prod [in HOC23PrimeDecomposition]
IO_pw_len [in HOC23PrimeDecomposition]
IO_ex_IO_RCancel [in HOC23PrimeDecomposition]
IO_pointwise_IObis [in HOC25Axiomatization]
io_extcgr_full [in HOC25Axiomatization]
io_extcgr_step [in HOC25Axiomatization]
io_norm_full [in HOC25Axiomatization]
io_norm_step [in HOC25Axiomatization]
io_nf_no_rem [in HOC25Axiomatization]
io_nf_no_out [in HOC25Axiomatization]
IO_bisimulation_up_to_refl [in HOC14IObis]
iter_abs_par_fiddle [in HOC18ONORbis]
iter_abs_par_congr [in HOC18ONORbis]
L
leave_ex [in HOC05WFProcesses]leave_not_fresh [in HOC05WFProcesses]
leave_red_set [in HOC05WFProcesses]
leave_nodup_r [in HOC05WFProcesses]
leave_inv_r [in HOC05WFProcesses]
leave_inv [in HOC05WFProcesses]
leave_permut_fst [in HOC19Coincide]
left413 [in HOC15HObis]
left413NOR [in HOC17NORbis]
lemma415 [in HOC18ONORbis]
lemma415a [in HOC18ONORbis]
lemma415b [in HOC18ONORbis]
lengthn [in LibListExt]
length_swap_names [in HOC17NORbis]
length_combine [in LibListExt]
length_rem1 [in LibListExt]
length_app_inv [in LibListExt]
length0 [in LibListExt]
lfresh_in_subst_p_q [in HOC02BaseLemmas]
lfresh_subst_rewrite [in HOC02BaseLemmas]
lfresh_nil [in HOC02BaseLemmas]
lfresh_par_iff [in HOC02BaseLemmas]
lfresh_gvar [in HOC02BaseLemmas]
lfresh_lvar [in HOC02BaseLemmas]
lfresh_receive [in HOC02BaseLemmas]
lfresh_send [in HOC02BaseLemmas]
list_exists_min [in HOC23PrimeDecomposition]
list_sum_app [in HOC25Axiomatization]
list_sum_cons [in HOC25Axiomatization]
list_sum_nil [in HOC25Axiomatization]
list_subset_combine_in [in HOC19Coincide]
list_subset_subset [in HOC19Coincide]
list_subset_nodup_snd [in HOC19Coincide]
list_subset_nodup_fst [in HOC19Coincide]
list_subset_Forall_snd [in HOC19Coincide]
list_subset_Forall_fst [in HOC19Coincide]
list_subset_in_set_inv [in HOC19Coincide]
list_subset_in_set [in HOC19Coincide]
list_subset_in_snd [in HOC19Coincide]
list_subset_in_fst [in HOC19Coincide]
lsubst_decomposition_g [in HOC02BaseLemmas]
LV_subst [in HOC02BaseLemmas]
M
maxassoc [in aux]maxcomm [in aux]
max0 [in aux]
max0neutrall [in aux]
max0neutralr [in aux]
measure_induction_set [in HOC25Axiomatization]
mem_of_permuts [in LibListExt]
mem_fst_split_remdup [in LibListExt]
mem_comb [in LibListExt]
mem_rem1_r [in LibListExt]
mem_rem1_l [in LibListExt]
mem_app_inv2 [in LibListExt]
mem_app_inv1 [in LibListExt]
mem_len_pos [in LibListExt]
mem_remdup_iff [in LibListExt]
mem_remdup [in LibListExt]
min_same [in aux]
my_wf_ind [in HOC03CanonicalLemmas]
N
nested_abs_monotonous [in HOC25Axiomatization]nested_abs_eq_abs [in HOC25Axiomatization]
nested_abs_gsubst [in HOC25Axiomatization]
nested_abs_eq_nil [in HOC25Axiomatization]
nested_abs_eq_gvar [in HOC25Axiomatization]
nested_abs_eq_par [in HOC25Axiomatization]
nested_abs_eq_send [in HOC25Axiomatization]
nested_abs_eq [in HOC25Axiomatization]
nf_cannot_reduce [in HOC25Axiomatization]
nf_cannot_reduce_rl [in HOC25Axiomatization]
nf_cannot_reduce_lr [in HOC25Axiomatization]
nf_congr_invariant [in HOC25Axiomatization]
nf_equiv_par_nil [in HOC25Axiomatization]
nf_remove_nil_congr [in HOC25Axiomatization]
nf_no_par_nil [in HOC25Axiomatization]
nf_abs_eq [in HOC25Axiomatization]
nf_cannot_reduce_basic [in HOC25Axiomatization]
nf_swap_invariant [in HOC25Axiomatization]
nil_process_char [in HOC10CongrLemmas]
nodup_swap_names [in HOC17NORbis]
noDup_snd_remDup_combine [in LibListExt]
noDup_fst_remDup_combine [in LibListExt]
nodup_combine_snd [in LibListExt]
nodup_combine_fst [in LibListExt]
nodup_app_iff [in LibListExt]
nodup_count [in LibListExt]
nodup_app_comm [in LibListExt]
nodup_app_comm_step [in LibListExt]
nodup_app_inv [in LibListExt]
nodup_rem1 [in LibListExt]
nodup_middle [in LibListExt]
nodup_remdup [in LibListExt]
none_core_wfcgr [in HOC10CongrLemmas]
NORbisC_in_normal [in HOC17NORbis]
NORbisC_out_normal [in HOC17NORbis]
NORbisC_tau [in HOC17NORbis]
NORbisC_sym [in HOC17NORbis]
NORbisC_eNORbisC [in HOC26EarlyBisimulation]
NORbisC_ex_NORbisC_ex_ex [in HOC26EarlyBisimulation]
NORbisE_ONE_ON [in HOC17NORbis]
NORbisE_ch_swap [in HOC17NORbis]
NORbisE_equiv [in HOC17NORbis]
NORbisE_ONORbis [in HOC19Coincide]
NORbisE_var [in HOC19Coincide]
NORbisE_tau [in HOC19Coincide]
NORbisE_in [in HOC19Coincide]
NORbisE_out_normal [in HOC19Coincide]
NORbisE_sym [in HOC19Coincide]
NORbis_in_par [in HOC17NORbis]
NORbis_exR_ch2 [in HOC17NORbis]
NORbis_congr_abs [in HOC17NORbis]
NORbis_ex_R_r [in HOC17NORbis]
NORbis_NORbis_ex [in HOC17NORbis]
NORbis_ex_in_normal_ex [in HOC17NORbis]
Norbis_ch_chan [in HOC17NORbis]
NORbis_ch_swap [in HOC17NORbis]
NORbis_in_normal [in HOC17NORbis]
NORbis_out_normal [in HOC17NORbis]
NORbis_tau [in HOC17NORbis]
NORbis_sym [in HOC17NORbis]
NORbis_trans [in HOC19Coincide]
NORbis_congr_par_nil [in HOC19Coincide]
NORbis_NORbis [in HOC19Coincide]
normalization_stops [in HOC25Axiomatization]
normal_form_IObis_wfcgr_eq [in HOC25Axiomatization]
normal_form_wfp_prod_app [in HOC25Axiomatization]
norm_full_measure [in HOC25Axiomatization]
norm_step_measure [in HOC25Axiomatization]
norm_step_abs_char [in HOC25Axiomatization]
norm_full_sizeP_eq [in HOC25Axiomatization]
norm_step_sizeP_eq [in HOC25Axiomatization]
norm_full_sizeP [in HOC25Axiomatization]
norm_step_sizeP [in HOC25Axiomatization]
norm_full_par_r [in HOC25Axiomatization]
norm_full_par_l [in HOC25Axiomatization]
norm_full_abs [in HOC25Axiomatization]
norm_full_send [in HOC25Axiomatization]
notin_remove [in LibFsetExt]
not_prime_nil [in HOC23PrimeDecomposition]
no_wfcgr_nil_gvar [in HOC10CongrLemmas]
no_wfcgr_nil_abs [in HOC10CongrLemmas]
no_wfcgr_nil_send [in HOC10CongrLemmas]
no_wfcgr_gvar_nil [in HOC10CongrLemmas]
no_wfcgr_gvar_abs [in HOC10CongrLemmas]
no_wfcgr_gvar_send [in HOC10CongrLemmas]
no_wfcgr_abs_nil [in HOC10CongrLemmas]
no_wfcgr_abs_gvar [in HOC10CongrLemmas]
no_wfcgr_abs_send [in HOC10CongrLemmas]
no_wfcgr_send_nil [in HOC10CongrLemmas]
no_wfcgr_send_gvar [in HOC10CongrLemmas]
no_wfcgr_send_abs [in HOC10CongrLemmas]
num_of_pars_eq [in HOC25Axiomatization]
num_of_pars_ordered [in HOC25Axiomatization]
num_of_pars_ordered_le [in HOC25Axiomatization]
num_of_pars_ordered_par_eq [in HOC25Axiomatization]
num_of_pars_ordered_par [in HOC25Axiomatization]
num_of_pars_cancel_b [in HOC25Axiomatization]
num_of_pars_cancel_f [in HOC25Axiomatization]
num_of_pars_wfp_prod_app_eq [in HOC25Axiomatization]
num_of_pars_wfp_prod_app [in HOC25Axiomatization]
num_of_pars_aux_1 [in HOC25Axiomatization]
num_of_pars_wfp_prod_app_comm [in HOC25Axiomatization]
num_var_wfcgr [in HOC10CongrLemmas]
num_abs_wfcgr [in HOC10CongrLemmas]
num_send_wfcgr [in HOC10CongrLemmas]
O
ONORbis_up_to_cgr_ONORbis [in HOC18ONORbis]ONORbis_up_to_ONORbis [in HOC18ONORbis]
ONORbis_trans [in HOC18ONORbis]
ONORbis_var [in HOC18ONORbis]
ONORbis_in [in HOC18ONORbis]
ONORbis_out_normal_ex [in HOC18ONORbis]
ONORbis_out_normal [in HOC18ONORbis]
ONORbis_tau [in HOC18ONORbis]
ONORbis_sym [in HOC18ONORbis]
ONORbis_refl [in HOC18ONORbis]
ONORbis_IObis [in HOC19Coincide]
ONORbis_out [in HOC19Coincide]
ONORbis_ONORbis [in HOC19Coincide]
ONOR_RON [in HOC18ONORbis]
ONOR_ONOR_ex [in HOC18ONORbis]
ordered_nf_invariant [in HOC25Axiomatization]
ordered_dpd_invariant [in HOC25Axiomatization]
ordered_par_nil_r [in HOC25Axiomatization]
ordered_par_nil_l [in HOC25Axiomatization]
ordered_par [in HOC25Axiomatization]
ordered_wfcgr [in HOC25Axiomatization]
order_oiv_cfresh_iff [in HOC27BarbedRevisited]
order_oiv_async_barbed [in HOC27BarbedRevisited]
order_oiv_wfcgr [in HOC27BarbedRevisited]
out_der_ok [in HOC22Decidability]
out_der_aux_eq [in HOC22Decidability]
out_nor_forall_exists [in HOC17NORbis]
out_R_HO_IO [in HOC19Coincide]
P
par_nil_sizeP_not_0 [in HOC25Axiomatization]peano_induction_type [in HOC25Axiomatization]
permuted_subst [in HOC15HObis]
permute_pipe [in HOC15HObis]
permute_subst_order [in HOC15HObis]
permute_NOR_pipe [in HOC17NORbis]
permut_subst [in HOC15HObis]
permut_to_list [in LibListExt]
permut_inv_r [in LibListExt]
permut_inv_l [in LibListExt]
permut_exists2 [in LibListExt]
permut_exists [in LibListExt]
permut_ndfl [in LibListExt]
permut_nodup [in LibListExt]
permut_combine [in LibListExt]
permut_combine_step [in LibListExt]
permut_remN_r [in LibListExt]
permut_remN_mem [in LibListExt]
permut_rem1_lr [in LibListExt]
permut_rem1_l [in LibListExt]
permut_rem1_r [in LibListExt]
permut_cons_rem1 [in LibListExt]
permut_cons_iff [in LibListExt]
permut_count_forall [in LibListExt]
permut_mem_exists [in LibListExt]
permut_flip_first_two [in LibListExt]
permut_of_nil [in LibListExt]
permut_count [in LibListExt]
permut_from_list [in LibListExt]
permut_mem [in LibListExt]
permut_len [in LibListExt]
piping_HOext [in HOC15HObis]
pre_lemma413 [in HOC15HObis]
pre_lemma413NOR [in HOC17NORbis]
prime_gvar [in HOC23PrimeDecomposition]
prime_send [in HOC23PrimeDecomposition]
prime_decomposition_unique [in HOC23PrimeDecomposition]
prime_decomposition_exists [in HOC23PrimeDecomposition]
prime_decomposition_IO [in HOC23PrimeDecomposition]
prime_remove [in HOC23PrimeDecomposition]
prime_out [in HOC23PrimeDecomposition]
prime_in [in HOC23PrimeDecomposition]
prime_parallel [in HOC23PrimeDecomposition]
prime_IO [in HOC23PrimeDecomposition]
prime_characterization [in HOC24PreCompleteness]
prime_in_dpd [in HOC24PreCompleteness]
prime_gswap [in HOC24PreCompleteness]
prime_characterization [in HOC25Axiomatization]
R
RCancel_IObis [in HOC23PrimeDecomposition]RCancel_step_forward [in HOC23PrimeDecomposition]
remdup_eq_fl [in LibListExt]
remdup_inv [in LibListExt]
remN_to_list_perm [in LibListExt]
remN_same_perm [in LibListExt]
remove_par_nils_size [in HOC24PreCompleteness]
remove_par_nils_wfp_prod_repeat_abs [in HOC24PreCompleteness]
remove_par_nils_sizeP [in HOC24PreCompleteness]
remove_par_nils_wfcgr [in HOC24PreCompleteness]
remove_nil_wfcgr [in HOC24PreCompleteness]
remove_nil_wfcgr_step [in HOC24PreCompleteness]
remove_nil_no_par_nil [in HOC24PreCompleteness]
remove_par_nils_sizeP_0 [in HOC24PreCompleteness]
remove_par_nils_eq_abs [in HOC24PreCompleteness]
remove_par_nils_swap [in HOC24PreCompleteness]
remove_par_nils_fresh [in HOC24PreCompleteness]
remove_par_nils_eq_par [in HOC24PreCompleteness]
remove_par_nils_eq_nil [in HOC24PreCompleteness]
remove_par_nils_eq_gvar [in HOC24PreCompleteness]
remove_par_nils_eq_send [in HOC24PreCompleteness]
remove_par_nils_eq [in HOC24PreCompleteness]
remove_par_nils_absorb [in HOC25Axiomatization]
remove_par_nils_red [in HOC25Axiomatization]
remove_union_comm [in LibFsetExt]
remove_union_distr [in LibFsetExt]
remove_union [in LibFsetExt]
remove_from_empty [in LibFsetExt]
remove_empty [in LibFsetExt]
remove_same [in LibFsetExt]
remove_comm [in LibFsetExt]
remove_in_subsets [in LibFsetExt]
remove_while_notin [in LibFsetExt]
rem_union_cancel [in LibFsetExt]
rem1_to_list_perm [in LibListExt]
rem1_permuts [in LibListExt]
rem1_remN_comm [in LibListExt]
rem1_mem_comm [in LibListExt]
rem1_comm [in LibListExt]
rem1_notin_list [in LibListExt]
repeat_Mem_in [in HOC01Defs]
repeat_from_list_n [in HOC01Defs]
repeat_length [in HOC01Defs]
right413 [in HOC15HObis]
right413NOR [in HOC17NORbis]
R_io_nf_IObis [in HOC25Axiomatization]
R_ONORbis_up_to_up_to_R_ONORbis_ex [in HOC18ONORbis]
R_swap_IObis [in HOC14IObis]
R_IObis_up_to_up_to_R_IObis [in HOC14IObis]
S
send_separation [in HOC25Axiomatization]send_wfcgr_no_nil [in HOC10CongrLemmas]
send_wfcgr_inv [in HOC10CongrLemmas]
send_core_wfcgr [in HOC10CongrLemmas]
singleton_union [in LibFsetExt]
singleton_absurd [in LibFsetExt]
sizeCh_out_eq [in HOC07SizeLemmas]
sizeCh_out_neq [in HOC07SizeLemmas]
sizeCh_in_eq [in HOC07SizeLemmas]
sizeCh_in_neq [in HOC07SizeLemmas]
sizeCh_subst [in HOC07SizeLemmas]
sizeCh_out_nfr [in HOC07SizeLemmas]
sizeCh_in_nfr [in HOC07SizeLemmas]
sizeCh_neq [in HOC07SizeLemmas]
sizeCh_cfresh [in HOC07SizeLemmas]
sizeCh_CHS [in HOC07SizeLemmas]
sizeCh_NORbis [in HOC17NORbis]
sizeCh_wfcgr [in HOC10CongrLemmas]
sizeCh_ONORbis [in HOC18ONORbis]
sizeO_remove [in HOC18ONORbis]
sizeO_out [in HOC18ONORbis]
sizeO_in [in HOC18ONORbis]
sizeO_subst [in HOC18ONORbis]
sizeP_remove [in HOC07SizeLemmas]
sizeP_out [in HOC07SizeLemmas]
sizeP_in [in HOC07SizeLemmas]
sizeP_swap [in HOC07SizeLemmas]
sizeP_subst [in HOC02BaseLemmas]
sizeP_0_congr_nil [in HOC18ONORbis]
sizeX_Ch [in HOC07SizeLemmas]
sizeX_2_sizeX [in HOC07SizeLemmas]
sizeX_remove [in HOC07SizeLemmas]
sizeX_out [in HOC07SizeLemmas]
sizeX_in [in HOC07SizeLemmas]
sizeX_subst [in HOC07SizeLemmas]
sizeX_subst2_cp [in HOC07SizeLemmas]
sizeX_subst1_cp [in HOC07SizeLemmas]
sizeX_cp [in HOC07SizeLemmas]
sizeX_gfresh [in HOC07SizeLemmas]
sizeX_GV [in HOC07SizeLemmas]
sizeX_wfcgr [in HOC10CongrLemmas]
sizeX_subst_fresh [in HOC10CongrLemmas]
sizeX_ONORbis [in HOC18ONORbis]
sizeX_IObis [in HOC14IObis]
size_remove [in HOC07SizeLemmas]
size_out [in HOC07SizeLemmas]
size_in [in HOC07SizeLemmas]
size_swap [in HOC07SizeLemmas]
size_unguardedX_remove [in HOC12Guarded]
size_lsubst [in HOC02BaseLemmas]
size_subst [in HOC02BaseLemmas]
snd_split [in LibListExt]
snd_split_step [in LibListExt]
snd_split_cons [in LibListExt]
split_combine_fs [in LibListExt]
split_length_r [in LibListExt]
split_length_l [in LibListExt]
split_spec [in LibListExt]
sublists_3 [in LibListExt]
sublists_2 [in LibListExt]
sublists_r [in LibListExt]
sublists_l [in LibListExt]
subset_union_r [in LibFsetExt]
subset_of_empty [in LibFsetExt]
substs_commute_lg [in HOC02BaseLemmas]
substs_commute_gg [in HOC02BaseLemmas]
subst_on_Abs [in HOC03CanonicalLemmas]
subst_nil_eq [in HOC10CongrLemmas]
subst_on_swap [in HOC02BaseLemmas]
subst_on_subst [in HOC02BaseLemmas]
subst_on_subst_same [in HOC02BaseLemmas]
subst_decomposition_g [in HOC02BaseLemmas]
subst_decomposition_l [in HOC02BaseLemmas]
subst_lvar_equal [in HOC02BaseLemmas]
subst_lvar_idem [in HOC02BaseLemmas]
subst_gvar_equal [in HOC02BaseLemmas]
subst_gvar_idem [in HOC02BaseLemmas]
subst_eq_rewrite [in HOC05WFProcesses]
swap_chans_names [in HOC17NORbis]
swap_chans_Msubst_comm [in HOC17NORbis]
swap_name_right [in HOC08SubstLemmas]
swap_name_left [in HOC08SubstLemmas]
swap_chan_on_subst [in HOC02BaseLemmas]
swap_on_subst [in HOC02BaseLemmas]
swap_chan_involutive [in HOC02BaseLemmas]
swap_name_involutive [in HOC02BaseLemmas]
swap_chan_sym [in HOC02BaseLemmas]
swap_chan_equal [in HOC02BaseLemmas]
swap_name_equal [in HOC02BaseLemmas]
swap_sym [in HOC02BaseLemmas]
swap_involutive [in HOC02BaseLemmas]
swap_gvar_involutive [in HOC02BaseLemmas]
swap_gvar_equal_iff [in HOC02BaseLemmas]
swap_equal [in HOC02BaseLemmas]
swap_gvar_equal [in HOC02BaseLemmas]
swap_gvar_right [in HOC02BaseLemmas]
swap_gvar_left [in HOC02BaseLemmas]
T
take_drop_nth [in LibListExt]to_list_cons_union [in LibListExt]
transitive_closure_equal [in HOC25Axiomatization]
trans_CHS [in HOC11TransLemmas]
trans_GV [in HOC11TransLemmas]
trans_out_wfcgr [in HOC24PreCompleteness]
trans_rem_wfcgr [in HOC24PreCompleteness]
trans_iter_abs_par_rem [in HOC18ONORbis]
trans_iter_abs_par_inst_abs [in HOC18ONORbis]
trans_iter_abs_par_in [in HOC18ONORbis]
trans_iter_abs_par_out [in HOC18ONORbis]
trans_iter_abs_par_tau [in HOC18ONORbis]
U
unguardeds_cp [in HOC12Guarded]unguardeds_invariant [in HOC12Guarded]
unguardeds_spec [in HOC12Guarded]
union_not_empty [in LibFsetExt]
union_inv [in LibFsetExt]
union_subset [in LibFsetExt]
union_empty [in LibFsetExt]
union_already_in [in LibFsetExt]
up_to_eq [in HOC13Bisimulations]
V
var_R_HO_IO [in HOC19Coincide]W
wfcgr_tr_in [in HOC27BarbedRevisited]wfcgr_size_remove_nil [in HOC24PreCompleteness]
wfcgr_abs_par_has_nil [in HOC24PreCompleteness]
wfcgr_gvar_par_has_nil [in HOC24PreCompleteness]
wfcgr_send_par_has_nil [in HOC24PreCompleteness]
wfcgr_nil_has_top_nil [in HOC24PreCompleteness]
wfcgr_measure [in HOC25Axiomatization]
wfcgr_exists_no_free_par_nil [in HOC10CongrLemmas]
wfcgr_abs_chan_eq [in HOC10CongrLemmas]
wfcgr_send_chan_eq [in HOC10CongrLemmas]
wfcgr_top_chan [in HOC10CongrLemmas]
wfcgr_top_chan_base [in HOC10CongrLemmas]
wfcgr_alt_freshCh [in HOC10CongrLemmas]
wfcgr_freshCh_step [in HOC10CongrLemmas]
wfcgr_inst_Abs [in HOC10CongrLemmas]
wfcgr_fresh [in HOC10CongrLemmas]
wfcgr_fresh_step [in HOC10CongrLemmas]
wfcgr_subst [in HOC10CongrLemmas]
wfcgr_subst2 [in HOC10CongrLemmas]
wfcgr_subst2_step [in HOC10CongrLemmas]
wfcgr_subst1 [in HOC10CongrLemmas]
wfcgr_subst1_step [in HOC10CongrLemmas]
wfcgr_sizeP [in HOC10CongrLemmas]
wfcgr_par_assoc_r [in HOC10CongrLemmas]
wfcgr_par_assoc_l [in HOC10CongrLemmas]
wfcgr_par_com [in HOC10CongrLemmas]
wfcgr_nil_r [in HOC10CongrLemmas]
wfcgr_nil_l [in HOC10CongrLemmas]
wfcgr_par [in HOC10CongrLemmas]
wfcgr_par2 [in HOC10CongrLemmas]
wfcgr_par1 [in HOC10CongrLemmas]
wfcgr_abs [in HOC10CongrLemmas]
wfcgr_send [in HOC10CongrLemmas]
wfcgr_f_inv [in HOC10CongrLemmas]
wfcgr_step_f_inv [in HOC10CongrLemmas]
wfprocess_prime_separation [in HOC23PrimeDecomposition]
wfprocess_list_prime_separation [in HOC23PrimeDecomposition]
wfprocess_exists_list_prime_nf [in HOC25Axiomatization]
wfprocess_eq [in HOC03CanonicalLemmas]
wfp_sizeP_nil [in HOC07SizeLemmas]
wfp_sizeP_par [in HOC07SizeLemmas]
wfp_sizeP_gvar [in HOC07SizeLemmas]
wfp_sizeP_abs [in HOC07SizeLemmas]
wfp_sizeP_send [in HOC07SizeLemmas]
wfp_size_nil [in HOC07SizeLemmas]
wfp_size_par [in HOC07SizeLemmas]
wfp_size_gvar [in HOC07SizeLemmas]
wfp_size_abs [in HOC07SizeLemmas]
wfp_size_send [in HOC07SizeLemmas]
wfp_trans_out_is_rem [in HOC11TransLemmas]
wfp_trans_rem_is_out [in HOC11TransLemmas]
wfp_trans_Msubst_name_tau [in HOC11TransLemmas]
wfp_trans_subst_name_tau [in HOC11TransLemmas]
wfp_trans_out_ex_subst [in HOC11TransLemmas]
wfp_trans_Msubst_tau [in HOC11TransLemmas]
wfp_trans_subst_tau [in HOC11TransLemmas]
wfp_subst_both [in HOC11TransLemmas]
wfp_cswap_fresh_trans_out [in HOC11TransLemmas]
wfp_swap_fresh_trans_out [in HOC11TransLemmas]
wfp_inst_chan_swap [in HOC11TransLemmas]
wfp_inst_swap [in HOC11TransLemmas]
wfp_inst_subst [in HOC11TransLemmas]
wfp_trans_subst_rem [in HOC11TransLemmas]
wfp_trans_Msubst_out [in HOC11TransLemmas]
wfp_trans_subst_out [in HOC11TransLemmas]
wfp_trans_Msubst_name_out [in HOC11TransLemmas]
wfp_trans_subst_name_out [in HOC11TransLemmas]
wfp_trans_Msubst_name_in [in HOC11TransLemmas]
wfp_trans_subst_name_in [in HOC11TransLemmas]
wfp_trans_Msubst_in [in HOC11TransLemmas]
wfp_trans_subst_in [in HOC11TransLemmas]
wfp_trans_swap_chan_tau [in HOC11TransLemmas]
wfp_trans_swap_tau [in HOC11TransLemmas]
wfp_trans_swap_chan_rem [in HOC11TransLemmas]
wfp_trans_swap_rem [in HOC11TransLemmas]
wfp_trans_swap_chan_out [in HOC11TransLemmas]
wfp_trans_swap_out [in HOC11TransLemmas]
wfp_trans_swap_chan_in [in HOC11TransLemmas]
wfp_trans_swap_inst_Abs_eq [in HOC11TransLemmas]
wfp_trans_swap_in [in HOC11TransLemmas]
wfp_decomposition_tau2 [in HOC11TransLemmas]
wfp_decomposition_tau1 [in HOC11TransLemmas]
wfp_agent_tau [in HOC11TransLemmas]
wfp_agent_rem [in HOC11TransLemmas]
wfp_agent_out [in HOC11TransLemmas]
wfp_agent_in [in HOC11TransLemmas]
wfp_unguarded_remove_iff [in HOC12Guarded]
wfp_unguardeds_cp_subst [in HOC12Guarded]
wfp_guarded_subst_trans_in [in HOC12Guarded]
wfp_guarded_remove [in HOC12Guarded]
wfp_guarded_remove_subst [in HOC12Guarded]
wfp_guarded_subst_trans_remove [in HOC12Guarded]
wfp_guarded_subst_trans_out [in HOC12Guarded]
wfp_guarded_out [in HOC12Guarded]
wfp_remove_congr [in HOC12Guarded]
wfp_not_guarded_unguarded [in HOC12Guarded]
wfp_prod_Var_par_app [in HOC23PrimeDecomposition]
wfp_prod_Var_app [in HOC23PrimeDecomposition]
wfp_prod_Var_cons [in HOC23PrimeDecomposition]
wfp_prod_Out_par_app [in HOC23PrimeDecomposition]
wfp_prod_Out_app [in HOC23PrimeDecomposition]
wfp_prod_Out_cons [in HOC23PrimeDecomposition]
wfp_prod_In_par_app [in HOC23PrimeDecomposition]
wfp_prod_In_app [in HOC23PrimeDecomposition]
wfp_prod_In_cons [in HOC23PrimeDecomposition]
wfp_prod_rem_compat [in HOC23PrimeDecomposition]
wfp_prod_out_compat [in HOC23PrimeDecomposition]
wfp_prod_in_compat [in HOC23PrimeDecomposition]
wfp_prod_sizeP_mem [in HOC23PrimeDecomposition]
wfp_prod_trans_in [in HOC23PrimeDecomposition]
wfp_prod_trans_out [in HOC23PrimeDecomposition]
wfp_prod_trans_rem [in HOC23PrimeDecomposition]
wfp_prod_IO_permut [in HOC23PrimeDecomposition]
wfp_prod_wfcgr_permut [in HOC23PrimeDecomposition]
wfp_prod_IO_app [in HOC23PrimeDecomposition]
wfp_prod_cons_wfp_sizeP [in HOC23PrimeDecomposition]
wfp_prod_cons_inv [in HOC23PrimeDecomposition]
wfp_prod_cons [in HOC23PrimeDecomposition]
wfp_sizeP_0_IO_nil [in HOC23PrimeDecomposition]
wfp_prod_components_lr [in HOC24PreCompleteness]
wfp_prod_repeat_swap [in HOC24PreCompleteness]
wfp_subst_X_prod_repeat_Abs [in HOC24PreCompleteness]
wfp_prod_repeat_subst [in HOC24PreCompleteness]
wfp_prod_repeat_SS [in HOC24PreCompleteness]
wfp_sizeP_swap [in HOC24PreCompleteness]
wfp_sizeP_size [in HOC24PreCompleteness]
wfp_prod_in [in HOC25Axiomatization]
wfp_prod_fresh [in HOC25Axiomatization]
wfp_sizeP_ordered_eq [in HOC25Axiomatization]
wfp_prod_app_wfp_sizeP [in HOC25Axiomatization]
wfp_size_ordered_le [in HOC25Axiomatization]
wfp_size_wfp_prod_lt [in HOC25Axiomatization]
wfp_size_wfp_prod_app [in HOC25Axiomatization]
wfp_prod_wfcgr_app [in HOC25Axiomatization]
wfp_prod_wfcgr_cons [in HOC25Axiomatization]
wfp_ind_set [in HOC25Axiomatization]
wfp_ind_gen [in HOC03CanonicalLemmas]
wfp_ind [in HOC03CanonicalLemmas]
wfp_swap_nil_eq [in HOC10CongrLemmas]
wfp_sizeP_0_wfcgr_nil [in HOC10CongrLemmas]
wfp_Msubst_invariant_permut [in HOC08SubstLemmas]
wfp_closed_proc_permut [in HOC08SubstLemmas]
wfp_subst_on_inst_Abs2 [in HOC08SubstLemmas]
wfp_subst_on_inst_Abs [in HOC08SubstLemmas]
wfp_mult_sub_Abs [in HOC08SubstLemmas]
wfp_mult_sub_par [in HOC08SubstLemmas]
wfp_mult_sub_commute3 [in HOC08SubstLemmas]
wfp_mult_sub_commute1 [in HOC08SubstLemmas]
wfp_mult_sub_separate2 [in HOC08SubstLemmas]
wfp_mult_sub_commute [in HOC08SubstLemmas]
wfp_subst_on_pipe [in HOC08SubstLemmas]
wfp_subst_comm_cp [in HOC08SubstLemmas]
wfp_swap_chan_on_subst1 [in HOC08SubstLemmas]
wfp_fresh_chan_swap [in HOC08SubstLemmas]
wfp_fresh_Msubst_lemma [in HOC08SubstLemmas]
wfp_subst_on_subst_same [in HOC08SubstLemmas]
wfp_gfresh_swap_rewrite [in HOC08SubstLemmas]
wfp_subst_on_swap [in HOC08SubstLemmas]
wfp_swap_on_subst [in HOC08SubstLemmas]
wfp_swap_chan_on_subst [in HOC08SubstLemmas]
wfp_swap_equal [in HOC08SubstLemmas]
wfp_swap_chan_equal [in HOC08SubstLemmas]
wfp_closed_pipe [in HOC09GVLemmas]
wfp_GV_pipe_nil [in HOC09GVLemmas]
wfp_GV_pipe_par [in HOC09GVLemmas]
wfp_GV_pipe_gvar2 [in HOC09GVLemmas]
wfp_GV_pipe_gvar1 [in HOC09GVLemmas]
wfp_GV_pipe_abs2 [in HOC09GVLemmas]
wfp_GV_pipe_abs1 [in HOC09GVLemmas]
wfp_GV_pipe_send [in HOC09GVLemmas]
wfp_GV_pipe_ch [in HOC09GVLemmas]
wfp_GV_Abs [in HOC09GVLemmas]
wfp_Msubst_subst_subset [in HOC09GVLemmas]
wfp_GV_Msubst_cp [in HOC09GVLemmas]
wfp_subst_eq_rewrite [in HOC05WFProcesses]
wfp_trans_in_abs_eq [in HOC05WFProcesses]
wfp_trans_in_chan_eq [in HOC05WFProcesses]
wfp_eq_subst_abs3 [in HOC05WFProcesses]
wfp_eq_subst_abs2 [in HOC05WFProcesses]
wfp_eq_subst_abs1 [in HOC05WFProcesses]
wfp_Abs_equal [in HOC05WFProcesses]
wfp_Abs_eq [in HOC05WFProcesses]
wfp_subst_lvar_XY [in HOC05WFProcesses]
wfp_subst_lvar [in HOC05WFProcesses]
wfp_par2_extract [in HOC05WFProcesses]
wfp_par1_extract [in HOC05WFProcesses]
wfp_prod_repeat_S [in HOC05WFProcesses]
wfp_prod_repeat_0 [in HOC05WFProcesses]
wfp_subst_decomposition_g [in HOC05WFProcesses]
wfp_subst_on_subst [in HOC05WFProcesses]
wfp_substs_commute_gg [in HOC05WFProcesses]
wfp_gfresh_subst_is_swap [in HOC05WFProcesses]
wfp_subst_gvar_idem [in HOC05WFProcesses]
wfp_gfresh_subst_rewrite [in HOC05WFProcesses]
wfp_fresh_Msubst1 [in HOC05WFProcesses]
wfp_eq_swap_chan_nil [in HOC05WFProcesses]
wfp_eq_swap_chan_par [in HOC05WFProcesses]
wfp_eq_swap_chan_gvar [in HOC05WFProcesses]
wfp_eq_swap_chan_abs [in HOC05WFProcesses]
wfp_eq_swap_chan_send [in HOC05WFProcesses]
wfp_eq_subst_nil [in HOC05WFProcesses]
wfp_eq_subst_par [in HOC05WFProcesses]
wfp_eq_subst_gvar [in HOC05WFProcesses]
wfp_eq_subst_send [in HOC05WFProcesses]
wfp_swap_chan_involutive [in HOC05WFProcesses]
wfp_eq_swap_nil [in HOC05WFProcesses]
wfp_eq_swap_par [in HOC05WFProcesses]
wfp_eq_swap_gvar [in HOC05WFProcesses]
wfp_eq_swap_abs [in HOC05WFProcesses]
wfp_eq_swap_send [in HOC05WFProcesses]
wfp_swap_involutive [in HOC05WFProcesses]
wfp_swap_sym [in HOC05WFProcesses]
wfp_permut_opl_iff [in HOC05WFProcesses]
wfp_opl_mem_combine_iff [in HOC05WFProcesses]
wfp_opl_mem [in HOC05WFProcesses]
wfp_Forall_cfresh_neq [in HOC05WFProcesses]
wfp_opl_app_ex [in HOC05WFProcesses]
wfp_opl_base [in HOC05WFProcesses]
wfp_permut_opl [in HOC05WFProcesses]
wfp_rem1_opl [in HOC05WFProcesses]
wfp_nodup_opl [in HOC05WFProcesses]
wfp_mem_opl [in HOC05WFProcesses]
wfp_mem_opl_inv [in HOC05WFProcesses]
wfp_opl_inv [in HOC05WFProcesses]
wfp_opl_app [in HOC05WFProcesses]
wfp_cpl_opl [in HOC05WFProcesses]
wfp_length_opl [in HOC05WFProcesses]
wfp_multisubst_to_subst_tail [in HOC05WFProcesses]
wfp_multisubst_to_subst [in HOC05WFProcesses]
wfp_pipe_to_Abs [in HOC05WFProcesses]
wfp_pipe_eq_nil [in HOC05WFProcesses]
wfp_find_fresh_chan [in HOC05WFProcesses]
wfp_cpl_app_inv [in HOC05WFProcesses]
wfp_permut_cp_list [in HOC05WFProcesses]
wfp_cpl_cpl [in HOC05WFProcesses]
wfp_cpl_forall [in HOC05WFProcesses]
wfp_list_proc_len [in HOC05WFProcesses]
wfp_cfresh_out_inv [in HOC06FreshLemmas]
wfp_cfresh_Msubst1 [in HOC06FreshLemmas]
wfp_cfresh_tau [in HOC06FreshLemmas]
wfp_cfresh_rem [in HOC06FreshLemmas]
wfp_cfresh_out [in HOC06FreshLemmas]
wfp_cfresh_in [in HOC06FreshLemmas]
wfp_fresh_inst_Abs [in HOC06FreshLemmas]
wfp_fresh_gvar_cswap [in HOC06FreshLemmas]
wfp_fresh_chan_gswap [in HOC06FreshLemmas]
wfp_fresh_chan_cswap [in HOC06FreshLemmas]
wfp_fresh_Msubst [in HOC06FreshLemmas]
wfp_fresh_cp [in HOC06FreshLemmas]
wfp_cfresh_subst_from2 [in HOC06FreshLemmas]
wfp_cfresh_msubst_from [in HOC06FreshLemmas]
wfp_cfresh_subst_from1 [in HOC06FreshLemmas]
wfp_cfresh_subst_in [in HOC06FreshLemmas]
wfp_cfresh_swap_inv [in HOC06FreshLemmas]
wfp_cfresh_pipe_cons [in HOC06FreshLemmas]
wfp_cfresh_pipe [in HOC06FreshLemmas]
wfp_cfresh_Abs [in HOC06FreshLemmas]
wfp_cfresh_par_iff [in HOC06FreshLemmas]
wfp_gfresh_Abs [in HOC06FreshLemmas]
wfp_sizeP_out_S_tr [in HOC18ONORbis]
wfp_sizeP_S_tr [in HOC14IObis]
wfp_guarded_IObis [in HOC14IObis]
wf_characterize_set [in HOC25Axiomatization]
wf_characterize [in HOC03CanonicalLemmas]
wf_receive_part1 [in HOC03CanonicalLemmas]
wf_receive [in HOC03CanonicalLemmas]
wf_subst [in HOC03CanonicalLemmas]
wf_ind_gen [in HOC03CanonicalLemmas]
wf_prod_repeat [in HOC03CanonicalLemmas]
wf_chan_swap [in HOC03CanonicalLemmas]
wf_swapping [in HOC03CanonicalLemmas]
wf_par2 [in HOC03CanonicalLemmas]
wf_par1 [in HOC03CanonicalLemmas]
wf_lfresh [in HOC03CanonicalLemmas]
wf_LV [in HOC03CanonicalLemmas]
wf_send [in HOC03CanonicalLemmas]
X
xEGood [in HOC03CanonicalLemmas]XHE_GoodF [in HOC03CanonicalLemmas]
XHF_GoodF [in HOC03CanonicalLemmas]
XHP_GoodF [in HOC03CanonicalLemmas]
X_der_ok [in HOC22Decidability]
X_der_aux_eq [in HOC22Decidability]
Constructor Index
A
AA [in HOC04DefLTS]AbsPar1 [in HOC04DefLTS]
AbsPar2 [in HOC04DefLTS]
AbsPure [in HOC04DefLTS]
AP [in HOC04DefLTS]
C
CAbs [in HOC20Barbed]CAbs [in HOC04DefLTS]
CAbsPar1 [in HOC04DefLTS]
CAbsPar2 [in HOC04DefLTS]
CHole [in HOC20Barbed]
CParL [in HOC20Barbed]
CParR [in HOC20Barbed]
CSend [in HOC20Barbed]
E
ECngr [in HOC25Axiomatization]ECore [in HOC25Axiomatization]
EParLeft [in HOC25Axiomatization]
EParRight [in HOC25Axiomatization]
EReceive [in HOC25Axiomatization]
ESend [in HOC25Axiomatization]
ESym [in HOC25Axiomatization]
ETrans [in HOC25Axiomatization]
G
GuGvar [in HOC12Guarded]GuNil [in HOC12Guarded]
GuPar [in HOC12Guarded]
GuReceive [in HOC12Guarded]
GuSend [in HOC12Guarded]
Gvar [in HOC01Defs]
I
IOCIAMain [in HOC21Coinductive]IOCIAMain_ex [in HOC21Coinductive]
IOCIMain [in HOC21Coinductive]
IOCIMain_ex [in HOC21Coinductive]
IOCMain [in HOC21Coinductive]
IOCMain_ex [in HOC21Coinductive]
io_nf_cgr [in HOC25Axiomatization]
io_nf_sym_base_nil [in HOC25Axiomatization]
io_nf_sym_base [in HOC25Axiomatization]
io_nf_base [in HOC25Axiomatization]
io_nf_base_nil [in HOC25Axiomatization]
L
LabIn [in HOC04DefLTS]LabOut [in HOC04DefLTS]
LabRem [in HOC04DefLTS]
Lvar [in HOC01Defs]
M
mkWfP [in HOC03CanonicalLemmas]N
NCore [in HOC25Axiomatization]NCoreNil [in HOC25Axiomatization]
nf_Nil [in HOC25Axiomatization]
nf_Par [in HOC25Axiomatization]
nf_Gvar [in HOC25Axiomatization]
nf_Abs [in HOC25Axiomatization]
nf_Send [in HOC25Axiomatization]
Nil [in HOC01Defs]
NParLeft [in HOC25Axiomatization]
NParRight [in HOC25Axiomatization]
NReceive [in HOC25Axiomatization]
NSend [in HOC25Axiomatization]
P
Par [in HOC01Defs]R
Rabs [in HOC15HObis]Rabs [in HOC14IObis]
Rbase [in HOC18ONORbis]
Rbis [in HOC15HObis]
Rbis [in HOC14IObis]
RCMain [in HOC23PrimeDecomposition]
Receive [in HOC01Defs]
RHOIO [in HOC19Coincide]
Rnrefl [in HOC15HObis]
Rn1 [in HOC15HObis]
Rn2 [in HOC15HObis]
RON_Main [in HOC18ONORbis]
Rp1 [in HOC14IObis]
Rp1refl [in HOC14IObis]
Rr [in HOC17NORbis]
Rrefl [in HOC15HObis]
Rrefl [in HOC14IObis]
Rs [in HOC15HObis]
Rs [in HOC14IObis]
Rsb [in HOC14IObis]
Rsbis [in HOC15HObis]
Rsbis [in HOC14IObis]
RsN [in HOC15HObis]
RsN [in HOC14IObis]
Rsw [in HOC17NORbis]
Rsw [in HOC14IObis]
Rswap [in HOC17NORbis]
Rswap [in HOC14IObis]
Rswapm [in HOC18ONORbis]
RswapX [in HOC18ONORbis]
RswCh [in HOC17NORbis]
Rswr [in HOC17NORbis]
Rswr [in HOC14IObis]
Rtrans [in HOC15HObis]
Rtrans [in HOC14IObis]
RtransNOR [in HOC19Coincide]
Rtrans_ab [in HOC20Barbed]
Rtrans_on [in HOC18ONORbis]
R_r_bis [in HOC15HObis]
R_r_base [in HOC15HObis]
R_ch_bis [in HOC15HObis]
R_ch_base [in HOC15HObis]
R_ch2_bis [in HOC17NORbis]
R_ch2_base [in HOC17NORbis]
R_r2_bis [in HOC17NORbis]
R_r2_base [in HOC17NORbis]
S
Send [in HOC01Defs]T
Tau [in HOC04DefLTS]TrAct1 [in HOC04DefLTS]
TrAct2 [in HOC04DefLTS]
TrIn [in HOC04DefLTS]
TrOut [in HOC04DefLTS]
TrRem [in HOC04DefLTS]
TrTau1 [in HOC04DefLTS]
TrTau2 [in HOC04DefLTS]
U
UpTo [in HOC13Bisimulations]W
WfAbs [in HOC03CanonicalLemmas]WfCgrAbs [in HOC10CongrLemmas]
WfCgrPar [in HOC10CongrLemmas]
WfCgrPar_assoc2 [in HOC10CongrLemmas]
WfCgrPar_assoc1 [in HOC10CongrLemmas]
WfCgrPar_com [in HOC10CongrLemmas]
WfCgrPar_nil2 [in HOC10CongrLemmas]
WfCgrPar_nil1 [in HOC10CongrLemmas]
WfCgrRefl [in HOC10CongrLemmas]
WfCgrSend [in HOC10CongrLemmas]
WfGvar [in HOC03CanonicalLemmas]
WfNil [in HOC03CanonicalLemmas]
WfPar [in HOC03CanonicalLemmas]
WfSend [in HOC03CanonicalLemmas]
Axiom Index
F
from_to_list [in LibListExt]fset_extens_iff [in LibFsetExt]
N
nodup_tolist [in LibListExt]T
to_from_list [in LibListExt]to_list [in LibListExt]
Inductive Index
A
abstraction [in HOC04DefLTS]agent [in HOC04DefLTS]
C
const_abs [in HOC04DefLTS]context [in HOC20Barbed]
E
extended_congruence [in HOC25Axiomatization]G
guarded [in HOC12Guarded]I
IObisC [in HOC21Coinductive]IObisC_ex [in HOC21Coinductive]
IObisI [in HOC21Coinductive]
IObisIAux [in HOC21Coinductive]
IObisIAux_ex [in HOC21Coinductive]
IObisI_ex [in HOC21Coinductive]
L
label [in HOC04DefLTS]N
normal_form [in HOC25Axiomatization]norm_step [in HOC25Axiomatization]
P
process [in HOC01Defs]R
RCancel [in HOC23PrimeDecomposition]RON [in HOC18ONORbis]
R_send [in HOC15HObis]
R_receive [in HOC15HObis]
R_nil [in HOC15HObis]
R_trans [in HOC15HObis]
R_r [in HOC15HObis]
R_ch [in HOC15HObis]
R_refl [in HOC15HObis]
R_Swap2 [in HOC17NORbis]
R_ch2 [in HOC17NORbis]
R_r2 [in HOC17NORbis]
R_Swap [in HOC17NORbis]
R_swap [in HOC17NORbis]
R_io_nf [in HOC25Axiomatization]
R_trans_ab [in HOC20Barbed]
R_trans_on [in HOC18ONORbis]
R_Swap_All [in HOC18ONORbis]
R_subst [in HOC14IObis]
R_par1 [in HOC14IObis]
R_abs [in HOC14IObis]
R_send [in HOC14IObis]
R_swap2 [in HOC14IObis]
R_swap [in HOC14IObis]
R_trans [in HOC14IObis]
R_refl [in HOC14IObis]
R_transNOR [in HOC19Coincide]
R_HO_IO [in HOC19Coincide]
T
transition [in HOC04DefLTS]U
up_to [in HOC13Bisimulations]W
wf [in HOC03CanonicalLemmas]wfcgr_step [in HOC10CongrLemmas]
Projection Index
P
proc [in HOC03CanonicalLemmas]W
wf_cond [in HOC03CanonicalLemmas]Instance Index
A
async_barbed_refl [in HOC27BarbedRevisited]async_barbed_trans [in HOC20Barbed]
async_barbed_sym [in HOC20Barbed]
C
const_abs_decidable [in HOC04DefLTS]D
dec_nf_classic [in HOC25Axiomatization]E
ext_cgr_trans [in HOC25Axiomatization]ext_cgr_sym [in HOC25Axiomatization]
ext_cgr_refl [in HOC25Axiomatization]
F
fresh_chan_decidable [in HOC01Defs]fresh_lvar_decidable [in HOC01Defs]
fresh_gvar_decidable [in HOC01Defs]
G
guarded_decidable [in HOC12Guarded]H
HObis_is_eq_rel [in HOC15HObis]I
inhabited_var_wfprocess [in HOC22Decidability]IObisC_ex_equivalence [in HOC21Coinductive]
IObisC_equivalence [in HOC21Coinductive]
IObis_is_eq_rel [in HOC14IObis]
L
lt_decidable [in aux]M
Mem_var_decidable [in LibListExt]O
ONORbis_is_eq_rel [in HOC18ONORbis]P
process_eq_decidable [in HOC01Defs]T
trans_clos_trans_1n [in HOC25Axiomatization]trans_ext_cgr_full [in HOC25Axiomatization]
trans_norm_full [in HOC25Axiomatization]
W
wfcgr_is_eq_rel [in HOC10CongrLemmas]wfcgr_step_sym [in HOC10CongrLemmas]
wfcgr_step_refl [in HOC10CongrLemmas]
wf_decidable [in HOC03CanonicalLemmas]
Section Index
B
Basic [in LibFsetExt]C
Count [in LibListExt]D
Defs [in LibListExt]F
FromList [in LibFsetExt]I
Inter [in LibFsetExt]L
ListBasic [in LibListExt]N
NoDup [in LibListExt]P
Permutation [in LibListExt]Permutation2 [in LibListExt]
R
RemDup [in LibListExt]Remove [in LibFsetExt]
RemoveOne [in LibListExt]
S
SplitCombine [in LibListExt]SubLists [in LibListExt]
Subset [in LibFsetExt]
T
ToList [in LibListExt]U
Union [in LibFsetExt]Definition Index
A
Abs [in HOC01Defs]Abs_from_Receive [in HOC22Decidability]
abs_subst [in HOC22Decidability]
async_barbed [in HOC20Barbed]
async_barbed_relation [in HOC20Barbed]
B
bio [in HOC22Decidability]bio_aux [in HOC22Decidability]
C
chan [in HOC01Defs]chan_gen [in HOC01Defs]
chan_gen_list [in HOC01Defs]
CHS [in HOC01Defs]
CHSs [in HOC01Defs]
closed_relation [in HOC13Bisimulations]
closed_proc_list_wfp [in HOC05WFProcesses]
closed_proc_list [in HOC01Defs]
closed_process [in HOC01Defs]
components [in HOC24PreCompleteness]
CONbis [in HOC13Bisimulations]
CONbisC [in HOC13Bisimulations]
CONbisE [in HOC13Bisimulations]
const_abs_dec [in HOC04DefLTS]
Context_bisimulation [in HOC13Bisimulations]
context_closed [in HOC20Barbed]
Core [in HOC10CongrLemmas]
count [in LibListExt]
D
deep_prime_decomposition [in HOC24PreCompleteness]dpd [in HOC24PreCompleteness]
E
E [in HOC02BaseLemmas]ext_cgr_full [in HOC25Axiomatization]
ext_cgr_step [in HOC25Axiomatization]
F
f [in HOC03CanonicalLemmas]fill [in HOC20Barbed]
fresh_chan_dec [in HOC01Defs]
fresh_chan [in HOC01Defs]
fresh_lvar_dec [in HOC01Defs]
fresh_lvar [in HOC01Defs]
fresh_gvar_dec [in HOC01Defs]
fresh_gvar [in HOC01Defs]
G
get_components [in HOC25Axiomatization]get_ins [in HOC25Axiomatization]
get_outs [in HOC25Axiomatization]
get_vars [in HOC25Axiomatization]
good [in HOC03CanonicalLemmas]
GoodF [in HOC03CanonicalLemmas]
guarded_proc [in HOC12Guarded]
GV [in HOC01Defs]
gvar_list [in HOC01Defs]
GV_union [in HOC22Decidability]
GV_set [in HOC01Defs]
H
has_free_par_nil [in HOC10CongrLemmas]has_top_nil [in HOC10CongrLemmas]
height_fun [in HOC01Defs]
HigherOrder_bisimulation [in HOC13Bisimulations]
HObis [in HOC13Bisimulations]
HObisC [in HOC13Bisimulations]
HObisE [in HOC13Bisimulations]
I
in_relation_up_to [in HOC13Bisimulations]in_normal_relation [in HOC13Bisimulations]
in_full_relation [in HOC13Bisimulations]
in_relation [in HOC13Bisimulations]
in_der [in HOC22Decidability]
in_der_aux [in HOC22Decidability]
in_normal_relation_ex [in HOC17NORbis]
in_ex_relation_step [in HOC21Coinductive]
in_relation_step [in HOC21Coinductive]
in_barb_preserving [in HOC20Barbed]
in_normal_relation_early [in HOC26EarlyBisimulation]
in_relation_early [in HOC26EarlyBisimulation]
in_relation_ex_up_to [in HOC14IObis]
in_relation_ex [in HOC14IObis]
IObis [in HOC13Bisimulations]
IObis_up_to [in HOC13Bisimulations]
IObis_early [in HOC26EarlyBisimulation]
IObis_full [in HOC14IObis]
IObis_ex_up_to [in HOC14IObis]
IObis_ex [in HOC14IObis]
IO_bisimulation_up_to [in HOC13Bisimulations]
IO_bisimulation [in HOC13Bisimulations]
IO_pointwise [in HOC23PrimeDecomposition]
IO_bisimulation_early [in HOC26EarlyBisimulation]
IO_bisimulation_full [in HOC14IObis]
IO_bisimulation_ex_up_to [in HOC14IObis]
IO_bisimulation_ex [in HOC14IObis]
iter_abs_par_abs [in HOC18ONORbis]
iter_abs_par [in HOC18ONORbis]
L
leave [in HOC05WFProcesses]list_sum [in HOC25Axiomatization]
list_proc [in HOC05WFProcesses]
list_subset [in HOC19Coincide]
lsubst [in HOC01Defs]
lt_dec [in aux]
LV [in HOC01Defs]
lvar [in HOC01Defs]
M
max [in aux]Mem_dec [in LibListExt]
N
nested_abs [in HOC25Axiomatization]noDup [in LibListExt]
NORbis [in HOC13Bisimulations]
NORbisC [in HOC13Bisimulations]
NORbisC_ex [in HOC17NORbis]
NORbisC_early [in HOC26EarlyBisimulation]
NORbisC_ex_ex [in HOC26EarlyBisimulation]
NORbisE [in HOC13Bisimulations]
NORbis_ex [in HOC17NORbis]
NORbis_early [in HOC26EarlyBisimulation]
NORbis_ex_ex [in HOC26EarlyBisimulation]
Normal_bisimulation [in HOC13Bisimulations]
Normal_bisimulation_ex [in HOC17NORbis]
Normal_bisimulation_early [in HOC26EarlyBisimulation]
Normal_bisimulation_ex_ex [in HOC26EarlyBisimulation]
norm_full [in HOC25Axiomatization]
num_of_pars [in HOC25Axiomatization]
num_var [in HOC10CongrLemmas]
num_abs [in HOC10CongrLemmas]
num_send [in HOC10CongrLemmas]
O
ONORbis [in HOC13Bisimulations]ONORbis_up_to [in HOC13Bisimulations]
ONORbis_ex [in HOC18ONORbis]
OpenNormal_bisimulation_up_to [in HOC13Bisimulations]
OpenNormal_bisimulation [in HOC13Bisimulations]
OpenNormal_bisimulation_ex [in HOC18ONORbis]
ordered [in HOC25Axiomatization]
order_oiv [in HOC27BarbedRevisited]
out_normal_relation_up_to [in HOC13Bisimulations]
out_relation_up_to [in HOC13Bisimulations]
out_context_relation [in HOC13Bisimulations]
out_normal_relation [in HOC13Bisimulations]
out_relation [in HOC13Bisimulations]
out_der [in HOC22Decidability]
out_der_aux [in HOC22Decidability]
out_normal_relation_ex [in HOC17NORbis]
out_relation_step [in HOC21Coinductive]
out_barb_preserving [in HOC20Barbed]
out_context_relation_early [in HOC26EarlyBisimulation]
out_normal_relation_early [in HOC26EarlyBisimulation]
P
par_ag2 [in HOC04DefLTS]par_ag1 [in HOC04DefLTS]
perform_input [in HOC20Barbed]
perform_output [in HOC20Barbed]
prime [in HOC23PrimeDecomposition]
prime_decomposition [in HOC23PrimeDecomposition]
prod [in HOC01Defs]
R
RelWfP [in HOC05WFProcesses]remDup [in LibListExt]
removeN [in LibListExt]
removeOne [in LibListExt]
remove_par_nils [in HOC24PreCompleteness]
repeat [in HOC01Defs]
S
size [in HOC01Defs]sizeAbs [in HOC04DefLTS]
sizeCh [in HOC01Defs]
sizeO [in HOC18ONORbis]
sizeP [in HOC01Defs]
sizeX [in HOC01Defs]
size_unguardedX [in HOC12Guarded]
subst [in HOC01Defs]
swap [in HOC01Defs]
swap_channels [in HOC17NORbis]
swap_names [in HOC17NORbis]
swap_relation [in HOC14IObis]
swap_chan [in HOC01Defs]
swap_name [in HOC01Defs]
swap_gvar [in HOC01Defs]
T
tau_relation_up_to [in HOC13Bisimulations]tau_relation [in HOC13Bisimulations]
top_channels [in HOC10CongrLemmas]
U
unguardeds [in HOC12Guarded]V
var_relation_up_to [in HOC13Bisimulations]var_relation [in HOC13Bisimulations]
var_relation_step [in HOC21Coinductive]
W
wfcgr [in HOC10CongrLemmas]wfp_prod_Var [in HOC23PrimeDecomposition]
wfp_prod_Out [in HOC23PrimeDecomposition]
wfp_prod_In [in HOC23PrimeDecomposition]
wfp_prod [in HOC23PrimeDecomposition]
wfp_repeat [in HOC24PreCompleteness]
wfp_num_of_pars [in HOC25Axiomatization]
wfp_sizeP [in HOC03CanonicalLemmas]
wfp_size [in HOC03CanonicalLemmas]
wfp_subst [in HOC03CanonicalLemmas]
wfp_Nil [in HOC03CanonicalLemmas]
wfp_Par [in HOC03CanonicalLemmas]
wfp_Gvar [in HOC03CanonicalLemmas]
wfp_Abs [in HOC03CanonicalLemmas]
wfp_Send [in HOC03CanonicalLemmas]
wfp_out_proc_list [in HOC05WFProcesses]
wfp_prod_repeat [in HOC05WFProcesses]
wfp_swap_chan [in HOC05WFProcesses]
wfp_swap [in HOC05WFProcesses]
wfp_multisubst [in HOC05WFProcesses]
wfp_pipe [in HOC05WFProcesses]
wfp_inst_Abs [in HOC04DefLTS]
wfp_sizeP_out [in HOC18ONORbis]
wfp_sizeO [in HOC18ONORbis]
X
XHE [in HOC03CanonicalLemmas]XHF [in HOC03CanonicalLemmas]
XHP [in HOC03CanonicalLemmas]
X_der [in HOC22Decidability]
X_der_aux [in HOC22Decidability]
Record Index
W
wfprocess [in HOC03CanonicalLemmas]| 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 | (1611 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 | (35 entries) |
| Variable Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (22 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 | (30 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 | (1098 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 | (126 entries) |
| Axiom Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (5 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 | (48 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 | (2 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 | (28 entries) |
| Section Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (17 entries) |
| 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 | (199 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 | (1 entry) |
This page has been generated by coqdoc