| 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 | (435 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 | (10 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 | (7 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 | (274 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 | (70 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 | (13 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 | (1 entry) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 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 | (47 entries) |
Global Index
A
abs [abbreviation, in Nom_Semantics]abs_to_proc [lemma, in Nom_HoweSound]
add_swap_fs_2 [lemma, in Nom_Swap_fs]
add_swap_fs [lemma, in Nom_Swap_fs]
aeq [inductive, in Nom_Syntax]
aeq_subst [lemma, in Nom_Syntax]
aeq_bind_2 [lemma, in Nom_Syntax]
aeq_bind_1 [lemma, in Nom_Syntax]
aeq_bind_3 [lemma, in Nom_Syntax]
aeq_swap_cut_notin [lemma, in Nom_Syntax]
aeq_shiftV [lemma, in Nom_Syntax]
aeq_mapV [lemma, in Nom_Syntax]
aeq_trans [lemma, in Nom_Syntax]
aeq_swap_indep [lemma, in Nom_Syntax]
aeq_sym [lemma, in Nom_Syntax]
aeq_fn [lemma, in Nom_Syntax]
aeq_swap [lemma, in Nom_Syntax]
aeq_refl [lemma, in Nom_Syntax]
aeq_nil [constructor, in Nom_Syntax]
aeq_nu_diff [constructor, in Nom_Syntax]
aeq_nu_same [constructor, in Nom_Syntax]
aeq_par [constructor, in Nom_Syntax]
aeq_snd [constructor, in Nom_Syntax]
aeq_inp [constructor, in Nom_Syntax]
aeq_var [constructor, in Nom_Syntax]
aeq_bisimulation [lemma, in Nom_Bisimulation]
aeq_lts_2 [lemma, in Nom_Semantics]
aeq_lts [lemma, in Nom_Semantics]
aeq_parr [lemma, in Nom_Semantics]
aeq_parl [lemma, in Nom_Semantics]
aeq_new_2 [lemma, in Nom_Semantics]
aeq_conc_new_2 [lemma, in Nom_Semantics]
aeq_new [lemma, in Nom_Semantics]
aeq_conc_new [lemma, in Nom_Semantics]
aeq_swap_new_aux [lemma, in Nom_Semantics]
aeq_appl [lemma, in Nom_Semantics]
aeq_appr [lemma, in Nom_Semantics]
aeq_conc_parr [lemma, in Nom_Semantics]
aeq_conc_parl [lemma, in Nom_Semantics]
aeq_conc_wf [lemma, in Nom_Semantics]
aeq_agent_trans [lemma, in Nom_Semantics]
aeq_agent_swap_indep [lemma, in Nom_Semantics]
aeq_agent_sym [lemma, in Nom_Semantics]
aeq_agent_fn [lemma, in Nom_Semantics]
aeq_agent_swap [lemma, in Nom_Semantics]
aeq_agent_refl [lemma, in Nom_Semantics]
aeq_agent_conc [constructor, in Nom_Semantics]
aeq_agent_abs [constructor, in Nom_Semantics]
aeq_agent_proc [constructor, in Nom_Semantics]
aeq_agent [inductive, in Nom_Semantics]
aeq_genNu [lemma, in Nom_Semantics]
aeq_conc_convert [lemma, in Nom_Semantics]
aeq_conc_trans [lemma, in Nom_Semantics]
aeq_conc_swap_indep [lemma, in Nom_Semantics]
aeq_conc_sym [lemma, in Nom_Semantics]
aeq_conc_swap [lemma, in Nom_Semantics]
aeq_conc_refl [lemma, in Nom_Semantics]
aeq_conc_cons_2 [constructor, in Nom_Semantics]
aeq_conc_cons_1 [constructor, in Nom_Semantics]
aeq_conc_nil [constructor, in Nom_Semantics]
aeq_conc [inductive, in Nom_Semantics]
agent [inductive, in Nom_Semantics]
ag_conc [constructor, in Nom_Semantics]
ag_abs [constructor, in Nom_Semantics]
ag_proc [constructor, in Nom_Semantics]
appl [definition, in Nom_Semantics]
appr [definition, in Nom_Semantics]
B
bind [definition, in Nom_Syntax]bind_mapV_comp [lemma, in Nom_Syntax]
bind_bind [lemma, in Nom_Syntax]
bind_mapV [lemma, in Nom_Syntax]
bind_return' [lemma, in Nom_Syntax]
bind_return [lemma, in Nom_Syntax]
bind_size [lemma, in Nom_Syntax]
bind_rec [definition, in Nom_Syntax]
bind_para_simpl [lemma, in Nom_Struct_congr]
bisimilarity [definition, in Nom_Bisimulation]
bisimilarity_howe [lemma, in Nom_HoweSound]
bisimulation [definition, in Nom_Bisimulation]
bisimulation_tclos_howe [lemma, in Nom_HoweSound]
bisimulation_up_to_sc [definition, in Nom_Struct_congr]
bisim_swap [lemma, in Nom_Bisimulation]
bisim_aeq [lemma, in Nom_Bisimulation]
bisim_exists_sym_rel_mod_aeq [lemma, in Nom_Bisimulation]
bisim_is_bisimulation [lemma, in Nom_Bisimulation]
bisim_refl [lemma, in Nom_Bisimulation]
bisim_trans [lemma, in Nom_Bisimulation]
bisim_sym [lemma, in Nom_Bisimulation]
C
comp_bisim_is_bisim [lemma, in Nom_Bisimulation]comp_sim_is_sim [lemma, in Nom_Bisimulation]
comp_assoc [lemma, in Nom_Bisimulation]
comp_trans [lemma, in Nom_Bisimulation]
comp_rel [definition, in Nom_Bisimulation]
conc [inductive, in Nom_Semantics]
conc_to_proc [lemma, in Nom_HoweSound]
conc_parr_wf [lemma, in Nom_Semantics]
conc_parl_wf [lemma, in Nom_Semantics]
conc_new_wf [lemma, in Nom_Semantics]
conc_convert_wf [lemma, in Nom_Semantics]
conc_convert_indep_wf [lemma, in Nom_Semantics]
conc_new [definition, in Nom_Semantics]
conc_parr [definition, in Nom_Semantics]
conc_parl [definition, in Nom_Semantics]
conc_convert [definition, in Nom_Semantics]
conc_convert_aux [definition, in Nom_Semantics]
conc_wf [definition, in Nom_Semantics]
conc_def [constructor, in Nom_Semantics]
D
diff [definition, in Nom_Swap_fs]diff_swap_fs [lemma, in Nom_Swap_fs]
E
empty_swap_fs [lemma, in Nom_Swap_fs]Equal [definition, in Nom_Swap_fs]
equal_empty_swap_fs' [lemma, in Nom_Swap_fs]
equal_empty_swap_fs [lemma, in Nom_Swap_fs]
F
fn [definition, in Nom_Syntax]fnsaxp [lemma, in Nom_Syntax]
fn_subst [lemma, in Nom_Syntax]
fn_bind [lemma, in Nom_Syntax]
fn_shiftV [lemma, in Nom_Syntax]
fn_mapV [lemma, in Nom_Syntax]
fn_swap_fs [lemma, in Nom_Syntax]
fn_sc [lemma, in Nom_Struct_congr]
fn_aeq_conc_3 [lemma, in Nom_Semantics]
fn_aeq_conc_2 [lemma, in Nom_Semantics]
fn_aeq_conc_1 [lemma, in Nom_Semantics]
fn_ag_conc_swap_fs [lemma, in Nom_Semantics]
fn_ag_swap_fs [lemma, in Nom_Semantics]
fn_lab_swap_fs [lemma, in Nom_Semantics]
fn_parr [lemma, in Nom_Semantics]
fn_parl [lemma, in Nom_Semantics]
fn_appl [lemma, in Nom_Semantics]
fn_appr [lemma, in Nom_Semantics]
fn_new [lemma, in Nom_Semantics]
fn_conc_new [lemma, in Nom_Semantics]
fn_genNu [lemma, in Nom_Semantics]
fn_conc_convert_2 [lemma, in Nom_Semantics]
fn_conc_convert_1 [lemma, in Nom_Semantics]
fn_conc_convert_0' [lemma, in Nom_Semantics]
fn_conc_convert_0 [lemma, in Nom_Semantics]
fn_agent [definition, in Nom_Semantics]
fn_lab [definition, in Nom_Semantics]
fold_swap_c [lemma, in Nom_Semantics]
fold_conc_convert [lemma, in Nom_Semantics]
G
genNu [definition, in Nom_Semantics]H
howe [inductive, in Nom_Howe]howe_subst [lemma, in Nom_Howe]
howe_bind [lemma, in Nom_Howe]
howe_mapV [lemma, in Nom_Howe]
howe_sym [lemma, in Nom_Howe]
howe_clos_trans_nu [lemma, in Nom_Howe]
howe_clos_trans_nu_same [lemma, in Nom_Howe]
howe_clos_trans_out [lemma, in Nom_Howe]
howe_clos_trans_inp [lemma, in Nom_Howe]
howe_clos_trans_par [lemma, in Nom_Howe]
howe_oe [lemma, in Nom_Howe]
howe_aeq [lemma, in Nom_Howe]
howe_genNu [lemma, in Nom_Howe]
howe_refl [lemma, in Nom_Howe]
howe_implies_howe' [lemma, in Nom_Howe]
howe_nu_aeq [lemma, in Nom_Howe]
howe_nu_same [lemma, in Nom_Howe]
howe_nu' [constructor, in Nom_Howe]
howe_out' [constructor, in Nom_Howe]
howe_inp' [constructor, in Nom_Howe]
howe_par' [constructor, in Nom_Howe]
howe_var' [constructor, in Nom_Howe]
howe_nil' [constructor, in Nom_Howe]
howe_comp' [constructor, in Nom_Howe]
howe_nu [constructor, in Nom_Howe]
howe_out [constructor, in Nom_Howe]
howe_inp [constructor, in Nom_Howe]
howe_par [constructor, in Nom_Howe]
howe_var [constructor, in Nom_Howe]
howe_nil [constructor, in Nom_Howe]
howe_comp [constructor, in Nom_Howe]
howe' [inductive, in Nom_Howe]
howe'_bind [lemma, in Nom_Howe]
howe'_swap [lemma, in Nom_Howe]
howe'_refl [lemma, in Nom_Howe]
howe'_implies_howe [lemma, in Nom_Howe]
howe'_ind_size [lemma, in Nom_Howe]
howe'_nu_same [lemma, in Nom_Howe]
I
incV [inductive, in Nom_Syntax]incV_map [definition, in Nom_Syntax]
inp [constructor, in Nom_Semantics]
inter [definition, in Nom_Swap_fs]
inter_swap_fs [lemma, in Nom_Swap_fs]
L
label [inductive, in Nom_Semantics]late_implies_sim [lemma, in Nom_Bisimulation]
lemma_swap_bind_and_aeq_bind_2 [lemma, in Nom_Syntax]
liftV [definition, in Nom_Syntax]
list_to_fs_2 [lemma, in Nom_Semantics]
list_to_fs_1_aux [lemma, in Nom_Semantics]
list_to_fs [definition, in Nom_Semantics]
lpseudo_sim [abbreviation, in Nom_HoweSound]
lts [inductive, in Nom_Semantics]
lts_conc_wf [lemma, in Nom_Semantics]
lts_fn [lemma, in Nom_Semantics]
lts_out_conc [lemma, in Nom_Semantics]
lts_inp_abs [lemma, in Nom_Semantics]
lts_tau_proc [lemma, in Nom_Semantics]
lts_new' [lemma, in Nom_Semantics]
lts_taur' [lemma, in Nom_Semantics]
lts_taul' [lemma, in Nom_Semantics]
lts_parr' [lemma, in Nom_Semantics]
lts_parl' [lemma, in Nom_Semantics]
lts_taur [constructor, in Nom_Semantics]
lts_taul [constructor, in Nom_Semantics]
lts_new [constructor, in Nom_Semantics]
lts_parr [constructor, in Nom_Semantics]
lts_parl [constructor, in Nom_Semantics]
lts_inp [constructor, in Nom_Semantics]
lts_out [constructor, in Nom_Semantics]
M
mapV [definition, in Nom_Syntax]mapV_mapV [lemma, in Nom_Syntax]
mapV_id [lemma, in Nom_Syntax]
mod_aeq_oe [lemma, in Nom_Bisimulation]
mod_swap [definition, in Nom_Bisimulation]
mod_aeq [definition, in Nom_Bisimulation]
mod_aeq_left_howe' [lemma, in Nom_Howe]
mod_aeq_howe [lemma, in Nom_Howe]
morphism_aeq_appl_indep [lemma, in Nom_Semantics]
morphism_aeq_appr_indep [lemma, in Nom_Semantics]
morphism_aeq_conc_parr_indep [lemma, in Nom_Semantics]
morphism_aeq_conc_parl_indep [lemma, in Nom_Semantics]
N
name [definition, in Nom_Syntax]names [definition, in Nom_Syntax]
new [definition, in Nom_Semantics]
NoDup_swap_fs [lemma, in Nom_Semantics]
Nom_Struct_congr [library]
Nom_Syntax [library]
Nom_Swap_fs [library]
Nom_Semantics [library]
Nom_Bisimulation [library]
Nom_Howe [library]
Nom_HoweSound [library]
notin_fn_equivariance [lemma, in Nom_Syntax]
notin_fn_notin_fnlab [lemma, in Nom_Semantics]
O
oe_swap [lemma, in Nom_Bisimulation]oe_proc0 [lemma, in Nom_Bisimulation]
oe_bind [lemma, in Nom_Bisimulation]
oe_mapV [lemma, in Nom_Bisimulation]
oe_trans [lemma, in Nom_Bisimulation]
oe_sym [lemma, in Nom_Bisimulation]
oe_refl [lemma, in Nom_Bisimulation]
oe_sc0 [lemma, in Nom_Struct_congr]
open_extension [definition, in Nom_Bisimulation]
out [constructor, in Nom_Semantics]
P
parl [definition, in Nom_Semantics]parr [definition, in Nom_Semantics]
PO [abbreviation, in Nom_Syntax]
proc [inductive, in Nom_Syntax]
proc0 [abbreviation, in Nom_Syntax]
proc1 [abbreviation, in Nom_Syntax]
pr_nil [constructor, in Nom_Syntax]
pr_nu [constructor, in Nom_Syntax]
pr_par [constructor, in Nom_Syntax]
pr_snd [constructor, in Nom_Syntax]
pr_inp [constructor, in Nom_Syntax]
pr_var [constructor, in Nom_Syntax]
pseudo_tau' [lemma, in Nom_HoweSound]
pseudo_sim_sim [lemma, in Nom_HoweSound]
pseudo_sim_sim' [lemma, in Nom_HoweSound]
pseudo_sim_in [lemma, in Nom_HoweSound]
pseudo_out_first [lemma, in Nom_HoweSound]
pseudo_sim_out [lemma, in Nom_HoweSound]
pseudo_inp_conc [lemma, in Nom_HoweSound]
pseudo_inp_first [lemma, in Nom_HoweSound]
pseudo_sim_equiv [lemma, in Nom_HoweSound]
pseudo_sim' [abbreviation, in Nom_HoweSound]
pseudo_sim [abbreviation, in Nom_HoweSound]
R
remove_diff_add [lemma, in Nom_Swap_fs]remove_swap_fs_2 [lemma, in Nom_Swap_fs]
remove_swap_fs [lemma, in Nom_Swap_fs]
Rincl [abbreviation, in Nom_Bisimulation]
Rincl_sc0_howe [lemma, in Nom_HoweSound]
S
sc_appr_conc_parr [lemma, in Nom_Struct_congr]sc_appr_conc_parl [lemma, in Nom_Struct_congr]
sc_appr_par_shift_left [lemma, in Nom_Struct_congr]
sc_appr_par_shift_right [lemma, in Nom_Struct_congr]
sc_appr_nu_indep_right [lemma, in Nom_Struct_congr]
sc_appr_nu_indep_left [lemma, in Nom_Struct_congr]
sc_appr_appl [lemma, in Nom_Struct_congr]
sc_scope_genNu [lemma, in Nom_Struct_congr]
sc_nu_genNu [lemma, in Nom_Struct_congr]
sc_bind [lemma, in Nom_Struct_congr]
sc_bind_2 [lemma, in Nom_Struct_congr]
sc_bind_1 [lemma, in Nom_Struct_congr]
sc_liftV [lemma, in Nom_Struct_congr]
sc_mapV [lemma, in Nom_Struct_congr]
sc_genNu [lemma, in Nom_Struct_congr]
sc_symmetric [lemma, in Nom_Struct_congr]
sc_refl [lemma, in Nom_Struct_congr]
sc_trans [constructor, in Nom_Struct_congr]
sc_aeq [constructor, in Nom_Struct_congr]
sc_nu [constructor, in Nom_Struct_congr]
sc_out [constructor, in Nom_Struct_congr]
sc_inp [constructor, in Nom_Struct_congr]
sc_par [constructor, in Nom_Struct_congr]
sc_var [constructor, in Nom_Struct_congr]
sc_nil [constructor, in Nom_Struct_congr]
sc_nu_nu [constructor, in Nom_Struct_congr]
sc_nu_nil_rev [constructor, in Nom_Struct_congr]
sc_nu_nil [constructor, in Nom_Struct_congr]
sc_scope_rev [constructor, in Nom_Struct_congr]
sc_scope [constructor, in Nom_Struct_congr]
sc_par_nil_conv [constructor, in Nom_Struct_congr]
sc_par_nil [constructor, in Nom_Struct_congr]
sc_par_comm [constructor, in Nom_Struct_congr]
sc_par_assoc_rev [constructor, in Nom_Struct_congr]
sc_par_assoc [constructor, in Nom_Struct_congr]
sc0 [definition, in Nom_Struct_congr]
sc0_refl [lemma, in Nom_Struct_congr]
sc0_sym [lemma, in Nom_Struct_congr]
sc0_trans [lemma, in Nom_Struct_congr]
shiftV [abbreviation, in Nom_Syntax]
shiftV1 [abbreviation, in Nom_Syntax]
shuffle_swap [lemma, in Nom_Syntax]
shuffle_swap_list [lemma, in Nom_Semantics]
simulation [definition, in Nom_Bisimulation]
simulation_late [definition, in Nom_Bisimulation]
simulation_up_to_sc_howe [lemma, in Nom_HoweSound]
simulation_up_to_sc [definition, in Nom_Struct_congr]
sim_tclosure [lemma, in Nom_Bisimulation]
sim_sym_imply_bisim [lemma, in Nom_Bisimulation]
sim_test_sym [lemma, in Nom_Bisimulation]
sim_test_trans [lemma, in Nom_Bisimulation]
sim_test [inductive, in Nom_Bisimulation]
size [definition, in Nom_Syntax]
size_induction [lemma, in Nom_Syntax]
struct_congr_bisim [lemma, in Nom_Struct_congr]
struct_congr_sim [lemma, in Nom_Struct_congr]
struct_congr_sim' [lemma, in Nom_Struct_congr]
struct_congr [inductive, in Nom_Struct_congr]
st_conc [constructor, in Nom_Bisimulation]
st_abs [constructor, in Nom_Bisimulation]
st_proc [constructor, in Nom_Bisimulation]
subrel_aeq_sc [instance, in Nom_Struct_congr]
subst [definition, in Nom_Syntax]
subst_par [lemma, in Nom_Syntax]
subst_nu_indep [lemma, in Nom_Syntax]
subst_shift [lemma, in Nom_Syntax]
subst_func [definition, in Nom_Syntax]
swap [definition, in Nom_Syntax]
swap_subst [lemma, in Nom_Syntax]
swap_bind_f_indep [lemma, in Nom_Syntax]
swap_bind [lemma, in Nom_Syntax]
swap_shiftV [lemma, in Nom_Syntax]
swap_mapV [lemma, in Nom_Syntax]
swap_size_eq [lemma, in Nom_Syntax]
swap_morphism' [lemma, in Nom_Syntax]
swap_fn_indep [lemma, in Nom_Syntax]
swap_indep [lemma, in Nom_Syntax]
swap_equivariance [lemma, in Nom_Syntax]
swap_invo [lemma, in Nom_Syntax]
swap_sym [lemma, in Nom_Syntax]
swap_id [lemma, in Nom_Syntax]
swap_struct_congr' [lemma, in Nom_Struct_congr]
swap_struct_congr [lemma, in Nom_Struct_congr]
swap_fs_morphism' [lemma, in Nom_Swap_fs]
swap_fs_mon_left' [lemma, in Nom_Swap_fs]
swap_fs_mon_left [lemma, in Nom_Swap_fs]
swap_fs_monotone' [lemma, in Nom_Swap_fs]
swap_fs_monotone [lemma, in Nom_Swap_fs]
swap_fs_invo [lemma, in Nom_Swap_fs]
swap_fs_sym [lemma, in Nom_Swap_fs]
swap_fs_id [lemma, in Nom_Swap_fs]
swap_fs_notin [lemma, in Nom_Swap_fs]
swap_fs_in [lemma, in Nom_Swap_fs]
swap_fs_4' [lemma, in Nom_Swap_fs]
swap_fs_3' [lemma, in Nom_Swap_fs]
swap_fs_4 [lemma, in Nom_Swap_fs]
swap_fs_3 [lemma, in Nom_Swap_fs]
swap_fs_2' [lemma, in Nom_Swap_fs]
swap_fs_2 [lemma, in Nom_Swap_fs]
swap_fs_1' [lemma, in Nom_Swap_fs]
swap_fs_1 [lemma, in Nom_Swap_fs]
swap_fs [definition, in Nom_Swap_fs]
swap_aux_r [lemma, in Nom_Swap_fs]
swap_aux_l [lemma, in Nom_Swap_fs]
swap_aux_inj [lemma, in Nom_Swap_fs]
swap_aux_equivariance [lemma, in Nom_Swap_fs]
swap_aux_invo [lemma, in Nom_Swap_fs]
swap_aux [definition, in Nom_Swap_fs]
swap_lts [lemma, in Nom_Semantics]
swap_parr [lemma, in Nom_Semantics]
swap_parl [lemma, in Nom_Semantics]
swap_new [lemma, in Nom_Semantics]
swap_conc_new [lemma, in Nom_Semantics]
swap_appl [lemma, in Nom_Semantics]
swap_appr [lemma, in Nom_Semantics]
swap_conc_parr [lemma, in Nom_Semantics]
swap_conc_parl [lemma, in Nom_Semantics]
swap_conc_wf [lemma, in Nom_Semantics]
swap_genNu [lemma, in Nom_Semantics]
swap_ag_indep [lemma, in Nom_Semantics]
swap_ag_equivariance [lemma, in Nom_Semantics]
swap_ag_sym [lemma, in Nom_Semantics]
swap_ag_invo [lemma, in Nom_Semantics]
swap_ag_id [lemma, in Nom_Semantics]
swap_ag [definition, in Nom_Semantics]
swap_c_invo [lemma, in Nom_Semantics]
swap_c [definition, in Nom_Semantics]
swap_list_to_fs [lemma, in Nom_Semantics]
swap_list_notin [lemma, in Nom_Semantics]
swap_list_indep [lemma, in Nom_Semantics]
swap_list_equivariance [lemma, in Nom_Semantics]
swap_list_sym [lemma, in Nom_Semantics]
swap_list_invo [lemma, in Nom_Semantics]
swap_list_id [lemma, in Nom_Semantics]
swap_list [definition, in Nom_Semantics]
swap_lab_in_iff [lemma, in Nom_Semantics]
swap_lab_notin [lemma, in Nom_Semantics]
swap_lab [definition, in Nom_Semantics]
T
tau [constructor, in Nom_Semantics]test_conc [abbreviation, in Nom_Bisimulation]
test_abs [abbreviation, in Nom_Bisimulation]
test_proc [abbreviation, in Nom_Bisimulation]
transp_bisim_is_bisim [lemma, in Nom_Bisimulation]
U
union_sim_is_sim [lemma, in Nom_Bisimulation]union_swap_fs [lemma, in Nom_Swap_fs]
unsimpl_swap_nu [lemma, in Nom_Syntax]
up_to_sc_sound [lemma, in Nom_Struct_congr]
up_to_sc_sim [lemma, in Nom_Struct_congr]
V
VS [constructor, in Nom_Syntax]VZ [constructor, in Nom_Syntax]
other
_ =A= _ [notation, in Nom_Syntax]_ // _ [notation, in Nom_Syntax]
_ !( _ ) _ [notation, in Nom_Syntax]
_ ? _ [notation, in Nom_Syntax]
_ ° _ [notation, in Nom_Bisimulation]
_ =sc0= _ [notation, in Nom_Struct_congr]
_ =sc= _ [notation, in Nom_Struct_congr]
_ =Ag= _ [notation, in Nom_Semantics]
_ =Ac= _ [notation, in Nom_Semantics]
nu _ , _ [notation, in Nom_Syntax]
Notation Index
other
_ =A= _ [in Nom_Syntax]_ // _ [in Nom_Syntax]
_ !( _ ) _ [in Nom_Syntax]
_ ? _ [in Nom_Syntax]
_ ° _ [in Nom_Bisimulation]
_ =sc0= _ [in Nom_Struct_congr]
_ =sc= _ [in Nom_Struct_congr]
_ =Ag= _ [in Nom_Semantics]
_ =Ac= _ [in Nom_Semantics]
nu _ , _ [in Nom_Syntax]
Library Index
N
Nom_Struct_congrNom_Syntax
Nom_Swap_fs
Nom_Semantics
Nom_Bisimulation
Nom_Howe
Nom_HoweSound
Lemma Index
A
abs_to_proc [in Nom_HoweSound]add_swap_fs_2 [in Nom_Swap_fs]
add_swap_fs [in Nom_Swap_fs]
aeq_subst [in Nom_Syntax]
aeq_bind_2 [in Nom_Syntax]
aeq_bind_1 [in Nom_Syntax]
aeq_bind_3 [in Nom_Syntax]
aeq_swap_cut_notin [in Nom_Syntax]
aeq_shiftV [in Nom_Syntax]
aeq_mapV [in Nom_Syntax]
aeq_trans [in Nom_Syntax]
aeq_swap_indep [in Nom_Syntax]
aeq_sym [in Nom_Syntax]
aeq_fn [in Nom_Syntax]
aeq_swap [in Nom_Syntax]
aeq_refl [in Nom_Syntax]
aeq_bisimulation [in Nom_Bisimulation]
aeq_lts_2 [in Nom_Semantics]
aeq_lts [in Nom_Semantics]
aeq_parr [in Nom_Semantics]
aeq_parl [in Nom_Semantics]
aeq_new_2 [in Nom_Semantics]
aeq_conc_new_2 [in Nom_Semantics]
aeq_new [in Nom_Semantics]
aeq_conc_new [in Nom_Semantics]
aeq_swap_new_aux [in Nom_Semantics]
aeq_appl [in Nom_Semantics]
aeq_appr [in Nom_Semantics]
aeq_conc_parr [in Nom_Semantics]
aeq_conc_parl [in Nom_Semantics]
aeq_conc_wf [in Nom_Semantics]
aeq_agent_trans [in Nom_Semantics]
aeq_agent_swap_indep [in Nom_Semantics]
aeq_agent_sym [in Nom_Semantics]
aeq_agent_fn [in Nom_Semantics]
aeq_agent_swap [in Nom_Semantics]
aeq_agent_refl [in Nom_Semantics]
aeq_genNu [in Nom_Semantics]
aeq_conc_convert [in Nom_Semantics]
aeq_conc_trans [in Nom_Semantics]
aeq_conc_swap_indep [in Nom_Semantics]
aeq_conc_sym [in Nom_Semantics]
aeq_conc_swap [in Nom_Semantics]
aeq_conc_refl [in Nom_Semantics]
B
bind_mapV_comp [in Nom_Syntax]bind_bind [in Nom_Syntax]
bind_mapV [in Nom_Syntax]
bind_return' [in Nom_Syntax]
bind_return [in Nom_Syntax]
bind_size [in Nom_Syntax]
bind_para_simpl [in Nom_Struct_congr]
bisimilarity_howe [in Nom_HoweSound]
bisimulation_tclos_howe [in Nom_HoweSound]
bisim_swap [in Nom_Bisimulation]
bisim_aeq [in Nom_Bisimulation]
bisim_exists_sym_rel_mod_aeq [in Nom_Bisimulation]
bisim_is_bisimulation [in Nom_Bisimulation]
bisim_refl [in Nom_Bisimulation]
bisim_trans [in Nom_Bisimulation]
bisim_sym [in Nom_Bisimulation]
C
comp_bisim_is_bisim [in Nom_Bisimulation]comp_sim_is_sim [in Nom_Bisimulation]
comp_assoc [in Nom_Bisimulation]
comp_trans [in Nom_Bisimulation]
conc_to_proc [in Nom_HoweSound]
conc_parr_wf [in Nom_Semantics]
conc_parl_wf [in Nom_Semantics]
conc_new_wf [in Nom_Semantics]
conc_convert_wf [in Nom_Semantics]
conc_convert_indep_wf [in Nom_Semantics]
D
diff_swap_fs [in Nom_Swap_fs]E
empty_swap_fs [in Nom_Swap_fs]equal_empty_swap_fs' [in Nom_Swap_fs]
equal_empty_swap_fs [in Nom_Swap_fs]
F
fnsaxp [in Nom_Syntax]fn_subst [in Nom_Syntax]
fn_bind [in Nom_Syntax]
fn_shiftV [in Nom_Syntax]
fn_mapV [in Nom_Syntax]
fn_swap_fs [in Nom_Syntax]
fn_sc [in Nom_Struct_congr]
fn_aeq_conc_3 [in Nom_Semantics]
fn_aeq_conc_2 [in Nom_Semantics]
fn_aeq_conc_1 [in Nom_Semantics]
fn_ag_conc_swap_fs [in Nom_Semantics]
fn_ag_swap_fs [in Nom_Semantics]
fn_lab_swap_fs [in Nom_Semantics]
fn_parr [in Nom_Semantics]
fn_parl [in Nom_Semantics]
fn_appl [in Nom_Semantics]
fn_appr [in Nom_Semantics]
fn_new [in Nom_Semantics]
fn_conc_new [in Nom_Semantics]
fn_genNu [in Nom_Semantics]
fn_conc_convert_2 [in Nom_Semantics]
fn_conc_convert_1 [in Nom_Semantics]
fn_conc_convert_0' [in Nom_Semantics]
fn_conc_convert_0 [in Nom_Semantics]
fold_swap_c [in Nom_Semantics]
fold_conc_convert [in Nom_Semantics]
H
howe_subst [in Nom_Howe]howe_bind [in Nom_Howe]
howe_mapV [in Nom_Howe]
howe_sym [in Nom_Howe]
howe_clos_trans_nu [in Nom_Howe]
howe_clos_trans_nu_same [in Nom_Howe]
howe_clos_trans_out [in Nom_Howe]
howe_clos_trans_inp [in Nom_Howe]
howe_clos_trans_par [in Nom_Howe]
howe_oe [in Nom_Howe]
howe_aeq [in Nom_Howe]
howe_genNu [in Nom_Howe]
howe_refl [in Nom_Howe]
howe_implies_howe' [in Nom_Howe]
howe_nu_aeq [in Nom_Howe]
howe_nu_same [in Nom_Howe]
howe'_bind [in Nom_Howe]
howe'_swap [in Nom_Howe]
howe'_refl [in Nom_Howe]
howe'_implies_howe [in Nom_Howe]
howe'_ind_size [in Nom_Howe]
howe'_nu_same [in Nom_Howe]
I
inter_swap_fs [in Nom_Swap_fs]L
late_implies_sim [in Nom_Bisimulation]lemma_swap_bind_and_aeq_bind_2 [in Nom_Syntax]
list_to_fs_2 [in Nom_Semantics]
list_to_fs_1_aux [in Nom_Semantics]
lts_conc_wf [in Nom_Semantics]
lts_fn [in Nom_Semantics]
lts_out_conc [in Nom_Semantics]
lts_inp_abs [in Nom_Semantics]
lts_tau_proc [in Nom_Semantics]
lts_new' [in Nom_Semantics]
lts_taur' [in Nom_Semantics]
lts_taul' [in Nom_Semantics]
lts_parr' [in Nom_Semantics]
lts_parl' [in Nom_Semantics]
M
mapV_mapV [in Nom_Syntax]mapV_id [in Nom_Syntax]
mod_aeq_oe [in Nom_Bisimulation]
mod_aeq_left_howe' [in Nom_Howe]
mod_aeq_howe [in Nom_Howe]
morphism_aeq_appl_indep [in Nom_Semantics]
morphism_aeq_appr_indep [in Nom_Semantics]
morphism_aeq_conc_parr_indep [in Nom_Semantics]
morphism_aeq_conc_parl_indep [in Nom_Semantics]
N
NoDup_swap_fs [in Nom_Semantics]notin_fn_equivariance [in Nom_Syntax]
notin_fn_notin_fnlab [in Nom_Semantics]
O
oe_swap [in Nom_Bisimulation]oe_proc0 [in Nom_Bisimulation]
oe_bind [in Nom_Bisimulation]
oe_mapV [in Nom_Bisimulation]
oe_trans [in Nom_Bisimulation]
oe_sym [in Nom_Bisimulation]
oe_refl [in Nom_Bisimulation]
oe_sc0 [in Nom_Struct_congr]
P
pseudo_tau' [in Nom_HoweSound]pseudo_sim_sim [in Nom_HoweSound]
pseudo_sim_sim' [in Nom_HoweSound]
pseudo_sim_in [in Nom_HoweSound]
pseudo_out_first [in Nom_HoweSound]
pseudo_sim_out [in Nom_HoweSound]
pseudo_inp_conc [in Nom_HoweSound]
pseudo_inp_first [in Nom_HoweSound]
pseudo_sim_equiv [in Nom_HoweSound]
R
remove_diff_add [in Nom_Swap_fs]remove_swap_fs_2 [in Nom_Swap_fs]
remove_swap_fs [in Nom_Swap_fs]
Rincl_sc0_howe [in Nom_HoweSound]
S
sc_appr_conc_parr [in Nom_Struct_congr]sc_appr_conc_parl [in Nom_Struct_congr]
sc_appr_par_shift_left [in Nom_Struct_congr]
sc_appr_par_shift_right [in Nom_Struct_congr]
sc_appr_nu_indep_right [in Nom_Struct_congr]
sc_appr_nu_indep_left [in Nom_Struct_congr]
sc_appr_appl [in Nom_Struct_congr]
sc_scope_genNu [in Nom_Struct_congr]
sc_nu_genNu [in Nom_Struct_congr]
sc_bind [in Nom_Struct_congr]
sc_bind_2 [in Nom_Struct_congr]
sc_bind_1 [in Nom_Struct_congr]
sc_liftV [in Nom_Struct_congr]
sc_mapV [in Nom_Struct_congr]
sc_genNu [in Nom_Struct_congr]
sc_symmetric [in Nom_Struct_congr]
sc_refl [in Nom_Struct_congr]
sc0_refl [in Nom_Struct_congr]
sc0_sym [in Nom_Struct_congr]
sc0_trans [in Nom_Struct_congr]
shuffle_swap [in Nom_Syntax]
shuffle_swap_list [in Nom_Semantics]
simulation_up_to_sc_howe [in Nom_HoweSound]
sim_tclosure [in Nom_Bisimulation]
sim_sym_imply_bisim [in Nom_Bisimulation]
sim_test_sym [in Nom_Bisimulation]
sim_test_trans [in Nom_Bisimulation]
size_induction [in Nom_Syntax]
struct_congr_bisim [in Nom_Struct_congr]
struct_congr_sim [in Nom_Struct_congr]
struct_congr_sim' [in Nom_Struct_congr]
subst_par [in Nom_Syntax]
subst_nu_indep [in Nom_Syntax]
subst_shift [in Nom_Syntax]
swap_subst [in Nom_Syntax]
swap_bind_f_indep [in Nom_Syntax]
swap_bind [in Nom_Syntax]
swap_shiftV [in Nom_Syntax]
swap_mapV [in Nom_Syntax]
swap_size_eq [in Nom_Syntax]
swap_morphism' [in Nom_Syntax]
swap_fn_indep [in Nom_Syntax]
swap_indep [in Nom_Syntax]
swap_equivariance [in Nom_Syntax]
swap_invo [in Nom_Syntax]
swap_sym [in Nom_Syntax]
swap_id [in Nom_Syntax]
swap_struct_congr' [in Nom_Struct_congr]
swap_struct_congr [in Nom_Struct_congr]
swap_fs_morphism' [in Nom_Swap_fs]
swap_fs_mon_left' [in Nom_Swap_fs]
swap_fs_mon_left [in Nom_Swap_fs]
swap_fs_monotone' [in Nom_Swap_fs]
swap_fs_monotone [in Nom_Swap_fs]
swap_fs_invo [in Nom_Swap_fs]
swap_fs_sym [in Nom_Swap_fs]
swap_fs_id [in Nom_Swap_fs]
swap_fs_notin [in Nom_Swap_fs]
swap_fs_in [in Nom_Swap_fs]
swap_fs_4' [in Nom_Swap_fs]
swap_fs_3' [in Nom_Swap_fs]
swap_fs_4 [in Nom_Swap_fs]
swap_fs_3 [in Nom_Swap_fs]
swap_fs_2' [in Nom_Swap_fs]
swap_fs_2 [in Nom_Swap_fs]
swap_fs_1' [in Nom_Swap_fs]
swap_fs_1 [in Nom_Swap_fs]
swap_aux_r [in Nom_Swap_fs]
swap_aux_l [in Nom_Swap_fs]
swap_aux_inj [in Nom_Swap_fs]
swap_aux_equivariance [in Nom_Swap_fs]
swap_aux_invo [in Nom_Swap_fs]
swap_lts [in Nom_Semantics]
swap_parr [in Nom_Semantics]
swap_parl [in Nom_Semantics]
swap_new [in Nom_Semantics]
swap_conc_new [in Nom_Semantics]
swap_appl [in Nom_Semantics]
swap_appr [in Nom_Semantics]
swap_conc_parr [in Nom_Semantics]
swap_conc_parl [in Nom_Semantics]
swap_conc_wf [in Nom_Semantics]
swap_genNu [in Nom_Semantics]
swap_ag_indep [in Nom_Semantics]
swap_ag_equivariance [in Nom_Semantics]
swap_ag_sym [in Nom_Semantics]
swap_ag_invo [in Nom_Semantics]
swap_ag_id [in Nom_Semantics]
swap_c_invo [in Nom_Semantics]
swap_list_to_fs [in Nom_Semantics]
swap_list_notin [in Nom_Semantics]
swap_list_indep [in Nom_Semantics]
swap_list_equivariance [in Nom_Semantics]
swap_list_sym [in Nom_Semantics]
swap_list_invo [in Nom_Semantics]
swap_list_id [in Nom_Semantics]
swap_lab_in_iff [in Nom_Semantics]
swap_lab_notin [in Nom_Semantics]
T
transp_bisim_is_bisim [in Nom_Bisimulation]U
union_sim_is_sim [in Nom_Bisimulation]union_swap_fs [in Nom_Swap_fs]
unsimpl_swap_nu [in Nom_Syntax]
up_to_sc_sound [in Nom_Struct_congr]
up_to_sc_sim [in Nom_Struct_congr]
Constructor Index
A
aeq_nil [in Nom_Syntax]aeq_nu_diff [in Nom_Syntax]
aeq_nu_same [in Nom_Syntax]
aeq_par [in Nom_Syntax]
aeq_snd [in Nom_Syntax]
aeq_inp [in Nom_Syntax]
aeq_var [in Nom_Syntax]
aeq_agent_conc [in Nom_Semantics]
aeq_agent_abs [in Nom_Semantics]
aeq_agent_proc [in Nom_Semantics]
aeq_conc_cons_2 [in Nom_Semantics]
aeq_conc_cons_1 [in Nom_Semantics]
aeq_conc_nil [in Nom_Semantics]
ag_conc [in Nom_Semantics]
ag_abs [in Nom_Semantics]
ag_proc [in Nom_Semantics]
C
conc_def [in Nom_Semantics]H
howe_nu' [in Nom_Howe]howe_out' [in Nom_Howe]
howe_inp' [in Nom_Howe]
howe_par' [in Nom_Howe]
howe_var' [in Nom_Howe]
howe_nil' [in Nom_Howe]
howe_comp' [in Nom_Howe]
howe_nu [in Nom_Howe]
howe_out [in Nom_Howe]
howe_inp [in Nom_Howe]
howe_par [in Nom_Howe]
howe_var [in Nom_Howe]
howe_nil [in Nom_Howe]
howe_comp [in Nom_Howe]
I
inp [in Nom_Semantics]L
lts_taur [in Nom_Semantics]lts_taul [in Nom_Semantics]
lts_new [in Nom_Semantics]
lts_parr [in Nom_Semantics]
lts_parl [in Nom_Semantics]
lts_inp [in Nom_Semantics]
lts_out [in Nom_Semantics]
O
out [in Nom_Semantics]P
pr_nil [in Nom_Syntax]pr_nu [in Nom_Syntax]
pr_par [in Nom_Syntax]
pr_snd [in Nom_Syntax]
pr_inp [in Nom_Syntax]
pr_var [in Nom_Syntax]
S
sc_trans [in Nom_Struct_congr]sc_aeq [in Nom_Struct_congr]
sc_nu [in Nom_Struct_congr]
sc_out [in Nom_Struct_congr]
sc_inp [in Nom_Struct_congr]
sc_par [in Nom_Struct_congr]
sc_var [in Nom_Struct_congr]
sc_nil [in Nom_Struct_congr]
sc_nu_nu [in Nom_Struct_congr]
sc_nu_nil_rev [in Nom_Struct_congr]
sc_nu_nil [in Nom_Struct_congr]
sc_scope_rev [in Nom_Struct_congr]
sc_scope [in Nom_Struct_congr]
sc_par_nil_conv [in Nom_Struct_congr]
sc_par_nil [in Nom_Struct_congr]
sc_par_comm [in Nom_Struct_congr]
sc_par_assoc_rev [in Nom_Struct_congr]
sc_par_assoc [in Nom_Struct_congr]
st_conc [in Nom_Bisimulation]
st_abs [in Nom_Bisimulation]
st_proc [in Nom_Bisimulation]
T
tau [in Nom_Semantics]V
VS [in Nom_Syntax]VZ [in Nom_Syntax]
Inductive Index
A
aeq [in Nom_Syntax]aeq_agent [in Nom_Semantics]
aeq_conc [in Nom_Semantics]
agent [in Nom_Semantics]
C
conc [in Nom_Semantics]H
howe [in Nom_Howe]howe' [in Nom_Howe]
I
incV [in Nom_Syntax]L
label [in Nom_Semantics]lts [in Nom_Semantics]
P
proc [in Nom_Syntax]S
sim_test [in Nom_Bisimulation]struct_congr [in Nom_Struct_congr]
Instance Index
S
subrel_aeq_sc [in Nom_Struct_congr]Abbreviation Index
A
abs [in Nom_Semantics]L
lpseudo_sim [in Nom_HoweSound]P
PO [in Nom_Syntax]proc0 [in Nom_Syntax]
proc1 [in Nom_Syntax]
pseudo_sim' [in Nom_HoweSound]
pseudo_sim [in Nom_HoweSound]
R
Rincl [in Nom_Bisimulation]S
shiftV [in Nom_Syntax]shiftV1 [in Nom_Syntax]
T
test_conc [in Nom_Bisimulation]test_abs [in Nom_Bisimulation]
test_proc [in Nom_Bisimulation]
Definition Index
A
appl [in Nom_Semantics]appr [in Nom_Semantics]
B
bind [in Nom_Syntax]bind_rec [in Nom_Syntax]
bisimilarity [in Nom_Bisimulation]
bisimulation [in Nom_Bisimulation]
bisimulation_up_to_sc [in Nom_Struct_congr]
C
comp_rel [in Nom_Bisimulation]conc_new [in Nom_Semantics]
conc_parr [in Nom_Semantics]
conc_parl [in Nom_Semantics]
conc_convert [in Nom_Semantics]
conc_convert_aux [in Nom_Semantics]
conc_wf [in Nom_Semantics]
D
diff [in Nom_Swap_fs]E
Equal [in Nom_Swap_fs]F
fn [in Nom_Syntax]fn_agent [in Nom_Semantics]
fn_lab [in Nom_Semantics]
G
genNu [in Nom_Semantics]I
incV_map [in Nom_Syntax]inter [in Nom_Swap_fs]
L
liftV [in Nom_Syntax]list_to_fs [in Nom_Semantics]
M
mapV [in Nom_Syntax]mod_swap [in Nom_Bisimulation]
mod_aeq [in Nom_Bisimulation]
N
name [in Nom_Syntax]names [in Nom_Syntax]
new [in Nom_Semantics]
O
open_extension [in Nom_Bisimulation]P
parl [in Nom_Semantics]parr [in Nom_Semantics]
S
sc0 [in Nom_Struct_congr]simulation [in Nom_Bisimulation]
simulation_late [in Nom_Bisimulation]
simulation_up_to_sc [in Nom_Struct_congr]
size [in Nom_Syntax]
subst [in Nom_Syntax]
subst_func [in Nom_Syntax]
swap [in Nom_Syntax]
swap_fs [in Nom_Swap_fs]
swap_aux [in Nom_Swap_fs]
swap_ag [in Nom_Semantics]
swap_c [in Nom_Semantics]
swap_list [in Nom_Semantics]
swap_lab [in Nom_Semantics]
| 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 | (435 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 | (10 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 | (7 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 | (274 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 | (70 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 | (13 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 | (1 entry) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (13 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 | (47 entries) |
This page has been generated by coqdoc