| 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 | (425 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 | (5 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 | (10 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 | (254 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 | (69 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15 entries) |
| 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 | (14 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 | (58 entries) |
Global Index
A
abs [inductive, in Semantics]abs_to_proc [lemma, in HoweSound]
abs_new [definition, in Semantics]
abs_parr [definition, in Semantics]
abs_parl [definition, in Semantics]
abs_def [constructor, in Semantics]
agent [inductive, in Semantics]
ag_conc [constructor, in Semantics]
ag_abs [constructor, in Semantics]
ag_proc [constructor, in Semantics]
amapN [definition, in Semantics]
amapN_open [lemma, in LNSemantics]
appl [definition, in Semantics]
appr [definition, in Semantics]
appr_open [lemma, in LNSemantics]
app_open [lemma, in LNSemantics]
asubst [definition, in Semantics]
B
bind [definition, in Syntax]Binders [library]
bind_mapV_comp [lemma, in Syntax]
bind_bind [lemma, in Syntax]
bind_mapN [lemma, in Syntax]
bind_mapV [lemma, in Syntax]
bind_proc0 [lemma, in Syntax]
bind_return' [lemma, in Syntax]
bind_return [lemma, in Syntax]
bind_close' [lemma, in LNProperties]
bind_open [lemma, in LNProperties]
bind_open' [lemma, in LNProperties]
bisimilarity [definition, in Bisimulation]
bisimilarity_howe [lemma, in HoweSound]
bisimulation [definition, in Bisimulation]
Bisimulation [library]
bisimulation_tclos_howe [lemma, in HoweSound]
bisimulation_up_to_sc [definition, in Struct_congr]
bisim_rename_compatible [lemma, in Bisimulation]
bisim_exists_sym_rel [lemma, in Bisimulation]
bisim_is_bisimulation [lemma, in Bisimulation]
bisim_refl [lemma, in Bisimulation]
bisim_trans [lemma, in Bisimulation]
bisim_sym [lemma, in Bisimulation]
bn [definition, in Syntax]
bn_agent_new [lemma, in LNSemantics]
bn_agent_open [lemma, in LNSemantics]
bn_agent [definition, in Semantics]
bn_subst [lemma, in LNProperties]
bn_bind [lemma, in LNProperties]
bn_bind' [lemma, in LNProperties]
bn_mapV [lemma, in LNProperties]
bn_close_sub [lemma, in LNProperties]
bn_close_in [lemma, in LNProperties]
bn_mapN [lemma, in LNProperties]
bn_close [lemma, in LNProperties]
bn_open [lemma, in LNProperties]
body [definition, in LNProperties]
b_name [constructor, in Binders]
C
close [definition, in Syntax]close_genNu [lemma, in LNSemantics]
close_subst [lemma, in LNProperties]
close_id [lemma, in LNProperties]
close_close [lemma, in LNProperties]
close_open_neq [lemma, in LNProperties]
close_open [lemma, in LNProperties]
clusterfuck [lemma, in Struct_congr]
cmapN [definition, in Semantics]
comp [definition, in Binders]
compK_permutK_gt [lemma, in Binders]
compK_permutK_leb [lemma, in Binders]
comp_assoc [lemma, in Utils]
comp_trans [lemma, in Utils]
comp_rel [definition, in Utils]
comp_bisim_is_bisim [lemma, in Bisimulation]
comp_sim_is_sim [lemma, in Bisimulation]
conc [inductive, in Semantics]
conc_to_proc [lemma, in HoweSound]
conc_new [definition, in Semantics]
conc_parr [definition, in Semantics]
conc_parl [definition, in Semantics]
conc_wf [definition, in Semantics]
conc_def [constructor, in Semantics]
D
decomp [definition, in LNProperties]decomp_agent [lemma, in LNSemantics]
decomp_agent_gen [lemma, in LNSemantics]
decomp_f [definition, in LNProperties]
decomp_proc [lemma, in LNProperties]
decomp_proc_gen [lemma, in LNProperties]
down [definition, in Semantics]
down_id [lemma, in LNSemantics]
down_fset_empty_rev [lemma, in Syntax]
down_fset_empty [lemma, in Syntax]
down_fset_spec' [lemma, in Syntax]
down_fset_spec [lemma, in Syntax]
down_fset [definition, in Syntax]
F
filter_fset_spec [lemma, in Utils]filter_fset [definition, in Utils]
fmapN [definition, in Semantics]
fn [definition, in Syntax]
fn_subst_lab [lemma, in LNSemantics]
fn_parr [lemma, in LNSemantics]
fn_parl [lemma, in LNSemantics]
fn_appr_appl [lemma, in LNSemantics]
fn_agent_new [lemma, in LNSemantics]
fn_agent_amapN [lemma, in LNSemantics]
fn_agent_open_sub [lemma, in LNSemantics]
fn_agent_open [lemma, in LNSemantics]
fn_genNu [lemma, in LNSemantics]
fn_agent [definition, in Semantics]
fn_lab [definition, in Semantics]
fn_open_list_sub [lemma, in LNProperties]
fn_subst [lemma, in LNProperties]
fn_bind [lemma, in LNProperties]
fn_bind' [lemma, in LNProperties]
fn_mapN [lemma, in LNProperties]
fn_mapV [lemma, in LNProperties]
fn_close [lemma, in LNProperties]
fn_agent_open_rev [lemma, in LNProperties]
fn_open_rev [lemma, in LNProperties]
fn_open_sub [lemma, in LNProperties]
fn_open_in [lemma, in LNProperties]
fn_open [lemma, in LNProperties]
fresh_sub [lemma, in Utils]
fresh_single_notin_rev [lemma, in Utils]
from_list_spec [lemma, in Utils]
from_list_to_list [lemma, in Utils]
fset_extens_rev [lemma, in Utils]
fshiftN [definition, in Semantics]
f_name [constructor, in Binders]
G
genNu [definition, in Semantics]H
howe [inductive, in Howe]Howe [library]
HoweSound [library]
howe_open_list [lemma, in Howe]
howe_subst [lemma, in Howe]
howe_bind [lemma, in Howe]
howe_bind' [lemma, in Howe]
howe_mapV [lemma, in Howe]
howe_sym [lemma, in Howe]
howe_clos_trans_nu [lemma, in Howe]
howe_clos_trans_out [lemma, in Howe]
howe_clos_trans_inp [lemma, in Howe]
howe_clos_trans_par [lemma, in Howe]
howe_implies_proc [lemma, in Howe]
howe_oe [lemma, in Howe]
howe_refl [lemma, in Howe]
howe_rename [lemma, in Howe]
howe_implies_howe' [lemma, in Howe]
howe_nu' [constructor, in Howe]
howe_out' [constructor, in Howe]
howe_inp' [constructor, in Howe]
howe_par' [constructor, in Howe]
howe_var' [constructor, in Howe]
howe_nil' [constructor, in Howe]
howe_comp' [constructor, in Howe]
howe_nu [constructor, in Howe]
howe_out [constructor, in Howe]
howe_inp [constructor, in Howe]
howe_par [constructor, in Howe]
howe_var [constructor, in Howe]
howe_nil [constructor, in Howe]
howe_comp [constructor, in Howe]
howe' [inductive, in Howe]
howe'_implies_howe [lemma, in Howe]
howe'_rename [lemma, in Howe]
howe'_implies_proc [lemma, in Howe]
howe'_ind_size [lemma, in Howe]
I
id_bisim_bisim [lemma, in Bisimulation]id_bisim [definition, in Bisimulation]
incV [inductive, in Binders]
incV_map [definition, in Binders]
inp [constructor, in Semantics]
is_proc_app [lemma, in LNSemantics]
is_agent_bn_rev [lemma, in LNSemantics]
is_agent_bn [lemma, in LNSemantics]
is_agent_amapN [lemma, in LNSemantics]
is_proc_genNu [lemma, in LNSemantics]
is_proc [inductive, in Syntax]
is_proc_Rel [definition, in Bisimulation]
is_proc_sc [lemma, in Struct_congr]
is_agent [definition, in Semantics]
is_proc_open_list [lemma, in LNProperties]
is_proc_rename [lemma, in LNProperties]
is_proc_bind [lemma, in LNProperties]
is_proc_mapN [lemma, in LNProperties]
is_proc_mapV [lemma, in LNProperties]
is_proc_open_close [lemma, in LNProperties]
is_proc_open [lemma, in LNProperties]
is_proc_bn_rev [lemma, in LNProperties]
is_proc_bn [lemma, in LNProperties]
L
label [inductive, in Semantics]late_implies_sim [lemma, in Bisimulation]
liftN [definition, in Binders]
liftN_preserves_injectivity [lemma, in Binders]
liftN_plus_n [lemma, in Binders]
liftN_0 [lemma, in Binders]
liftN_liftN [lemma, in Binders]
liftN_S [lemma, in Binders]
liftV [definition, in Syntax]
LNProperties [library]
LNSemantics [library]
lpseudo_sim [abbreviation, in HoweSound]
lts [inductive, in Semantics]
lts_open [lemma, in LNSemantics]
lts_rename [lemma, in LNSemantics]
lts_fn [lemma, in LNSemantics]
lts_is_proc [lemma, in LNSemantics]
lts_conc_wf [lemma, in LNSemantics]
lts_out_conc [lemma, in Semantics]
lts_inp_abs [lemma, in Semantics]
lts_tau_proc [lemma, in Semantics]
lts_new' [lemma, in Semantics]
lts_taur' [lemma, in Semantics]
lts_taul' [lemma, in Semantics]
lts_parr' [lemma, in Semantics]
lts_parl' [lemma, in Semantics]
lts_taur [constructor, in Semantics]
lts_taul [constructor, in Semantics]
lts_new [constructor, in Semantics]
lts_parr [constructor, in Semantics]
lts_parl [constructor, in Semantics]
lts_inp [constructor, in Semantics]
lts_out [constructor, in Semantics]
M
mapN [definition, in Syntax]mapN_eq_on_bn [lemma, in LNSemantics]
mapN_genNu [lemma, in LNSemantics]
mapN_mapN [lemma, in Syntax]
mapN_id' [lemma, in Syntax]
mapN_id [lemma, in Syntax]
mapN_close [lemma, in LNProperties]
mapN_open [lemma, in LNProperties]
mapN_open_gen [lemma, in LNProperties]
mapV [definition, in Syntax]
mapV_mapN [lemma, in Syntax]
mapV_mapV [lemma, in Syntax]
mapV_id [lemma, in Syntax]
mapV_open [lemma, in LNProperties]
mapV_close [lemma, in LNProperties]
map_singleton [lemma, in Utils]
map_union [lemma, in Utils]
map_fset_empty [lemma, in Utils]
map_fset_spec [lemma, in Utils]
map_fset [definition, in Utils]
mem_map_rev [lemma, in Utils]
minus_one_list [lemma, in Syntax]
N
name [inductive, in Binders]new [definition, in Semantics]
new_open_agent [lemma, in LNSemantics]
notin_fn_notin_fnlab [lemma, in LNSemantics]
nu_nu_conc [lemma, in Struct_congr]
nu_genNu [lemma, in Semantics]
O
oe_rename [lemma, in Bisimulation]oe_proc0 [lemma, in Bisimulation]
oe_bind [lemma, in Bisimulation]
oe_mapV [lemma, in Bisimulation]
oe_trans [lemma, in Bisimulation]
oe_sym [lemma, in Bisimulation]
oe_refl [lemma, in Bisimulation]
oe_sc0 [lemma, in Struct_congr]
open [definition, in Syntax]
open_agent_open_agent [lemma, in LNSemantics]
open_agent_id [lemma, in LNSemantics]
open_agent_injective [lemma, in LNSemantics]
open_genNu [lemma, in LNSemantics]
open_extension [definition, in Bisimulation]
open_agent [definition, in Semantics]
open_open_list [lemma, in LNProperties]
open_list_subst [lemma, in LNProperties]
open_list_bind [lemma, in LNProperties]
open_list_par [lemma, in LNProperties]
open_list_id [lemma, in LNProperties]
open_list [definition, in LNProperties]
open_subst [lemma, in LNProperties]
open_id [lemma, in LNProperties]
open_close [lemma, in LNProperties]
open_close_gen [lemma, in LNProperties]
open_open [lemma, in LNProperties]
open_injective [lemma, in LNProperties]
out [constructor, in Semantics]
P
parl [definition, in Semantics]parl_open [lemma, in LNSemantics]
parr [definition, in Semantics]
parr_open [lemma, in LNSemantics]
permut [definition, in Binders]
permut_id [lemma, in Binders]
permut_injective [lemma, in Binders]
permut_gt [lemma, in Binders]
permut_ltb [lemma, in Binders]
permut_0 [lemma, in Binders]
permut_shiftN [lemma, in LNProperties]
PO [abbreviation, in Syntax]
proc [inductive, in Syntax]
proc_nil [constructor, in Syntax]
proc_nu [constructor, in Syntax]
proc_par [constructor, in Syntax]
proc_out [constructor, in Syntax]
proc_inp [constructor, in Syntax]
proc_var [constructor, in Syntax]
proc0 [abbreviation, in Syntax]
proc1 [abbreviation, in Syntax]
pr_nil [constructor, in Syntax]
pr_nu [constructor, in Syntax]
pr_par [constructor, in Syntax]
pr_snd [constructor, in Syntax]
pr_inp [constructor, in Syntax]
pr_var [constructor, in Syntax]
pseudo_tau [lemma, in HoweSound]
pseudo_sim_sim [lemma, in HoweSound]
pseudo_sim_sim' [lemma, in HoweSound]
pseudo_sim_in [lemma, in HoweSound]
pseudo_out_first [lemma, in HoweSound]
pseudo_sim_out [lemma, in HoweSound]
pseudo_inp_conc [lemma, in HoweSound]
pseudo_inp_first [lemma, in HoweSound]
pseudo_sim [abbreviation, in HoweSound]
R
refl0 [abbreviation, in HoweSound]rel_renamed [inductive, in Bisimulation]
remove_subset_union [lemma, in Utils]
remove_singleton_neq [lemma, in Utils]
remove_singleton [lemma, in Utils]
rename_compatible [definition, in Bisimulation]
Rincl [abbreviation, in Utils]
Rincl_sc0_howe [lemma, in HoweSound]
rrenamed_def [constructor, in Bisimulation]
rrenamed_base [constructor, in Bisimulation]
S
sc_F_newC [lemma, in Struct_congr]sc_newF_C [lemma, in Struct_congr]
sc_appr_appl [lemma, in Struct_congr]
sc_nu_nu_permut [lemma, in Struct_congr]
sc_nuK_permut1 [lemma, in Struct_congr]
sc_nuK_compL_permutK [lemma, in Struct_congr]
sc_appr_new_abs [lemma, in Struct_congr]
sc_appl_new_conc [lemma, in Struct_congr]
sc_new_shift_A [lemma, in Struct_congr]
sc_new_A_shift [lemma, in Struct_congr]
sc_scope_genNu' [lemma, in Struct_congr]
sc_scope_genNu [lemma, in Struct_congr]
sc_nuK_permutK [lemma, in Struct_congr]
sc_bind [lemma, in Struct_congr]
sc_bind' [lemma, in Struct_congr]
sc_liftV [lemma, in Struct_congr]
sc_mapN [lemma, in Struct_congr]
sc_mapV [lemma, in Struct_congr]
sc_open_rev [lemma, in Struct_congr]
sc_close [lemma, in Struct_congr]
sc_genNu [lemma, in Struct_congr]
sc_symmetric [lemma, in Struct_congr]
sc_refl [lemma, in Struct_congr]
sc_nu' [lemma, in Struct_congr]
sc_open [lemma, in Struct_congr]
sc_trans [constructor, in Struct_congr]
sc_nu [constructor, in Struct_congr]
sc_out [constructor, in Struct_congr]
sc_inp [constructor, in Struct_congr]
sc_par [constructor, in Struct_congr]
sc_var [constructor, in Struct_congr]
sc_nil [constructor, in Struct_congr]
sc_nu_nu_rev [constructor, in Struct_congr]
sc_nu_nu [constructor, in Struct_congr]
sc_nu_nil_rev [constructor, in Struct_congr]
sc_nu_nil [constructor, in Struct_congr]
sc_scope_rev [constructor, in Struct_congr]
sc_scope [constructor, in Struct_congr]
sc_par_nil_conv [constructor, in Struct_congr]
sc_par_nil [constructor, in Struct_congr]
sc_par_comm [constructor, in Struct_congr]
sc_par_assoc_rev [constructor, in Struct_congr]
sc_par_assoc [constructor, in Struct_congr]
sc0 [inductive, in Struct_congr]
sc0_refl [lemma, in Struct_congr]
sc0_sym [lemma, in Struct_congr]
sc0_trans [lemma, in Struct_congr]
sc0_def [constructor, in Struct_congr]
Semantics [library]
shiftN [abbreviation, in Syntax]
shiftN_injective [lemma, in Binders]
shiftV [abbreviation, in Syntax]
shiftV1 [abbreviation, in Syntax]
simulation [definition, in Bisimulation]
simulation_up_to_sc_howe [lemma, in HoweSound]
simulation_rel_renamed [lemma, in Bisimulation]
simulation_late [definition, in Bisimulation]
simulation_up_to_sc [definition, in Struct_congr]
sim_sym_imply_bisim [lemma, in Bisimulation]
sim_test_sym [lemma, in Bisimulation]
sim_test_trans [lemma, in Bisimulation]
sim_test [inductive, in Bisimulation]
size [definition, in Syntax]
size_induction [lemma, in Syntax]
size_open [lemma, in LNProperties]
struct_congr_bisim [lemma, in Struct_congr]
struct_congr_sim [lemma, in Struct_congr]
struct_congr_sim' [lemma, in Struct_congr]
struct_congr [inductive, in Struct_congr]
Struct_congr [library]
st_conc [constructor, in Bisimulation]
st_abs [constructor, in Bisimulation]
st_proc [constructor, in Bisimulation]
subset_trans [lemma, in Utils]
subst [abbreviation, in Syntax]
subst_lab_rename [lemma, in LNSemantics]
subst_lab_inv [lemma, in LNSemantics]
subst_lab_id [lemma, in LNSemantics]
subst_lab [definition, in LNSemantics]
subst_shift [lemma, in Syntax]
subst_mapN [lemma, in Syntax]
subst_func [definition, in Syntax]
Syntax [library]
T
tau [constructor, in Semantics]tclosure_howe_implies_proc [lemma, in Howe]
test_conc [abbreviation, in Bisimulation]
test_abs [abbreviation, in Bisimulation]
test_proc [abbreviation, in Bisimulation]
to_list_empty [lemma, in Utils]
to_list [definition, in Utils]
transp_bisim_is_bisim [lemma, in Bisimulation]
U
union_sim_is_sim [lemma, in Bisimulation]up_to_sc_sound [lemma, in Struct_congr]
up_to_sc_sim [lemma, in Struct_congr]
Utils [library]
V
VS [constructor, in Binders]VZ [constructor, in Binders]
other
_ ° _ [notation, in Utils]_ // _ [notation, in Syntax]
_ !( _ ) _ [notation, in Syntax]
_ ? _ [notation, in Syntax]
nu _ [notation, in Syntax]
Notation Index
other
_ ° _ [in Utils]_ // _ [in Syntax]
_ !( _ ) _ [in Syntax]
_ ? _ [in Syntax]
nu _ [in Syntax]
Library Index
B
BindersBisimulation
H
HoweHoweSound
L
LNPropertiesLNSemantics
S
SemanticsStruct_congr
Syntax
U
UtilsLemma Index
A
abs_to_proc [in HoweSound]amapN_open [in LNSemantics]
appr_open [in LNSemantics]
app_open [in LNSemantics]
B
bind_mapV_comp [in Syntax]bind_bind [in Syntax]
bind_mapN [in Syntax]
bind_mapV [in Syntax]
bind_proc0 [in Syntax]
bind_return' [in Syntax]
bind_return [in Syntax]
bind_close' [in LNProperties]
bind_open [in LNProperties]
bind_open' [in LNProperties]
bisimilarity_howe [in HoweSound]
bisimulation_tclos_howe [in HoweSound]
bisim_rename_compatible [in Bisimulation]
bisim_exists_sym_rel [in Bisimulation]
bisim_is_bisimulation [in Bisimulation]
bisim_refl [in Bisimulation]
bisim_trans [in Bisimulation]
bisim_sym [in Bisimulation]
bn_agent_new [in LNSemantics]
bn_agent_open [in LNSemantics]
bn_subst [in LNProperties]
bn_bind [in LNProperties]
bn_bind' [in LNProperties]
bn_mapV [in LNProperties]
bn_close_sub [in LNProperties]
bn_close_in [in LNProperties]
bn_mapN [in LNProperties]
bn_close [in LNProperties]
bn_open [in LNProperties]
C
close_genNu [in LNSemantics]close_subst [in LNProperties]
close_id [in LNProperties]
close_close [in LNProperties]
close_open_neq [in LNProperties]
close_open [in LNProperties]
clusterfuck [in Struct_congr]
compK_permutK_gt [in Binders]
compK_permutK_leb [in Binders]
comp_assoc [in Utils]
comp_trans [in Utils]
comp_bisim_is_bisim [in Bisimulation]
comp_sim_is_sim [in Bisimulation]
conc_to_proc [in HoweSound]
D
decomp_agent [in LNSemantics]decomp_agent_gen [in LNSemantics]
decomp_proc [in LNProperties]
decomp_proc_gen [in LNProperties]
down_id [in LNSemantics]
down_fset_empty_rev [in Syntax]
down_fset_empty [in Syntax]
down_fset_spec' [in Syntax]
down_fset_spec [in Syntax]
F
filter_fset_spec [in Utils]fn_subst_lab [in LNSemantics]
fn_parr [in LNSemantics]
fn_parl [in LNSemantics]
fn_appr_appl [in LNSemantics]
fn_agent_new [in LNSemantics]
fn_agent_amapN [in LNSemantics]
fn_agent_open_sub [in LNSemantics]
fn_agent_open [in LNSemantics]
fn_genNu [in LNSemantics]
fn_open_list_sub [in LNProperties]
fn_subst [in LNProperties]
fn_bind [in LNProperties]
fn_bind' [in LNProperties]
fn_mapN [in LNProperties]
fn_mapV [in LNProperties]
fn_close [in LNProperties]
fn_agent_open_rev [in LNProperties]
fn_open_rev [in LNProperties]
fn_open_sub [in LNProperties]
fn_open_in [in LNProperties]
fn_open [in LNProperties]
fresh_sub [in Utils]
fresh_single_notin_rev [in Utils]
from_list_spec [in Utils]
from_list_to_list [in Utils]
fset_extens_rev [in Utils]
H
howe_open_list [in Howe]howe_subst [in Howe]
howe_bind [in Howe]
howe_bind' [in Howe]
howe_mapV [in Howe]
howe_sym [in Howe]
howe_clos_trans_nu [in Howe]
howe_clos_trans_out [in Howe]
howe_clos_trans_inp [in Howe]
howe_clos_trans_par [in Howe]
howe_implies_proc [in Howe]
howe_oe [in Howe]
howe_refl [in Howe]
howe_rename [in Howe]
howe_implies_howe' [in Howe]
howe'_implies_howe [in Howe]
howe'_rename [in Howe]
howe'_implies_proc [in Howe]
howe'_ind_size [in Howe]
I
id_bisim_bisim [in Bisimulation]is_proc_app [in LNSemantics]
is_agent_bn_rev [in LNSemantics]
is_agent_bn [in LNSemantics]
is_agent_amapN [in LNSemantics]
is_proc_genNu [in LNSemantics]
is_proc_sc [in Struct_congr]
is_proc_open_list [in LNProperties]
is_proc_rename [in LNProperties]
is_proc_bind [in LNProperties]
is_proc_mapN [in LNProperties]
is_proc_mapV [in LNProperties]
is_proc_open_close [in LNProperties]
is_proc_open [in LNProperties]
is_proc_bn_rev [in LNProperties]
is_proc_bn [in LNProperties]
L
late_implies_sim [in Bisimulation]liftN_preserves_injectivity [in Binders]
liftN_plus_n [in Binders]
liftN_0 [in Binders]
liftN_liftN [in Binders]
liftN_S [in Binders]
lts_open [in LNSemantics]
lts_rename [in LNSemantics]
lts_fn [in LNSemantics]
lts_is_proc [in LNSemantics]
lts_conc_wf [in LNSemantics]
lts_out_conc [in Semantics]
lts_inp_abs [in Semantics]
lts_tau_proc [in Semantics]
lts_new' [in Semantics]
lts_taur' [in Semantics]
lts_taul' [in Semantics]
lts_parr' [in Semantics]
lts_parl' [in Semantics]
M
mapN_eq_on_bn [in LNSemantics]mapN_genNu [in LNSemantics]
mapN_mapN [in Syntax]
mapN_id' [in Syntax]
mapN_id [in Syntax]
mapN_close [in LNProperties]
mapN_open [in LNProperties]
mapN_open_gen [in LNProperties]
mapV_mapN [in Syntax]
mapV_mapV [in Syntax]
mapV_id [in Syntax]
mapV_open [in LNProperties]
mapV_close [in LNProperties]
map_singleton [in Utils]
map_union [in Utils]
map_fset_empty [in Utils]
map_fset_spec [in Utils]
mem_map_rev [in Utils]
minus_one_list [in Syntax]
N
new_open_agent [in LNSemantics]notin_fn_notin_fnlab [in LNSemantics]
nu_nu_conc [in Struct_congr]
nu_genNu [in Semantics]
O
oe_rename [in Bisimulation]oe_proc0 [in Bisimulation]
oe_bind [in Bisimulation]
oe_mapV [in Bisimulation]
oe_trans [in Bisimulation]
oe_sym [in Bisimulation]
oe_refl [in Bisimulation]
oe_sc0 [in Struct_congr]
open_agent_open_agent [in LNSemantics]
open_agent_id [in LNSemantics]
open_agent_injective [in LNSemantics]
open_genNu [in LNSemantics]
open_open_list [in LNProperties]
open_list_subst [in LNProperties]
open_list_bind [in LNProperties]
open_list_par [in LNProperties]
open_list_id [in LNProperties]
open_subst [in LNProperties]
open_id [in LNProperties]
open_close [in LNProperties]
open_close_gen [in LNProperties]
open_open [in LNProperties]
open_injective [in LNProperties]
P
parl_open [in LNSemantics]parr_open [in LNSemantics]
permut_id [in Binders]
permut_injective [in Binders]
permut_gt [in Binders]
permut_ltb [in Binders]
permut_0 [in Binders]
permut_shiftN [in LNProperties]
pseudo_tau [in HoweSound]
pseudo_sim_sim [in HoweSound]
pseudo_sim_sim' [in HoweSound]
pseudo_sim_in [in HoweSound]
pseudo_out_first [in HoweSound]
pseudo_sim_out [in HoweSound]
pseudo_inp_conc [in HoweSound]
pseudo_inp_first [in HoweSound]
R
remove_subset_union [in Utils]remove_singleton_neq [in Utils]
remove_singleton [in Utils]
Rincl_sc0_howe [in HoweSound]
S
sc_F_newC [in Struct_congr]sc_newF_C [in Struct_congr]
sc_appr_appl [in Struct_congr]
sc_nu_nu_permut [in Struct_congr]
sc_nuK_permut1 [in Struct_congr]
sc_nuK_compL_permutK [in Struct_congr]
sc_appr_new_abs [in Struct_congr]
sc_appl_new_conc [in Struct_congr]
sc_new_shift_A [in Struct_congr]
sc_new_A_shift [in Struct_congr]
sc_scope_genNu' [in Struct_congr]
sc_scope_genNu [in Struct_congr]
sc_nuK_permutK [in Struct_congr]
sc_bind [in Struct_congr]
sc_bind' [in Struct_congr]
sc_liftV [in Struct_congr]
sc_mapN [in Struct_congr]
sc_mapV [in Struct_congr]
sc_open_rev [in Struct_congr]
sc_close [in Struct_congr]
sc_genNu [in Struct_congr]
sc_symmetric [in Struct_congr]
sc_refl [in Struct_congr]
sc_nu' [in Struct_congr]
sc_open [in Struct_congr]
sc0_refl [in Struct_congr]
sc0_sym [in Struct_congr]
sc0_trans [in Struct_congr]
shiftN_injective [in Binders]
simulation_up_to_sc_howe [in HoweSound]
simulation_rel_renamed [in Bisimulation]
sim_sym_imply_bisim [in Bisimulation]
sim_test_sym [in Bisimulation]
sim_test_trans [in Bisimulation]
size_induction [in Syntax]
size_open [in LNProperties]
struct_congr_bisim [in Struct_congr]
struct_congr_sim [in Struct_congr]
struct_congr_sim' [in Struct_congr]
subset_trans [in Utils]
subst_lab_rename [in LNSemantics]
subst_lab_inv [in LNSemantics]
subst_lab_id [in LNSemantics]
subst_shift [in Syntax]
subst_mapN [in Syntax]
T
tclosure_howe_implies_proc [in Howe]to_list_empty [in Utils]
transp_bisim_is_bisim [in Bisimulation]
U
union_sim_is_sim [in Bisimulation]up_to_sc_sound [in Struct_congr]
up_to_sc_sim [in Struct_congr]
Constructor Index
A
abs_def [in Semantics]ag_conc [in Semantics]
ag_abs [in Semantics]
ag_proc [in Semantics]
B
b_name [in Binders]C
conc_def [in Semantics]F
f_name [in Binders]H
howe_nu' [in Howe]howe_out' [in Howe]
howe_inp' [in Howe]
howe_par' [in Howe]
howe_var' [in Howe]
howe_nil' [in Howe]
howe_comp' [in Howe]
howe_nu [in Howe]
howe_out [in Howe]
howe_inp [in Howe]
howe_par [in Howe]
howe_var [in Howe]
howe_nil [in Howe]
howe_comp [in Howe]
I
inp [in Semantics]L
lts_taur [in Semantics]lts_taul [in Semantics]
lts_new [in Semantics]
lts_parr [in Semantics]
lts_parl [in Semantics]
lts_inp [in Semantics]
lts_out [in Semantics]
O
out [in Semantics]P
proc_nil [in Syntax]proc_nu [in Syntax]
proc_par [in Syntax]
proc_out [in Syntax]
proc_inp [in Syntax]
proc_var [in Syntax]
pr_nil [in Syntax]
pr_nu [in Syntax]
pr_par [in Syntax]
pr_snd [in Syntax]
pr_inp [in Syntax]
pr_var [in Syntax]
R
rrenamed_def [in Bisimulation]rrenamed_base [in Bisimulation]
S
sc_trans [in Struct_congr]sc_nu [in Struct_congr]
sc_out [in Struct_congr]
sc_inp [in Struct_congr]
sc_par [in Struct_congr]
sc_var [in Struct_congr]
sc_nil [in Struct_congr]
sc_nu_nu_rev [in Struct_congr]
sc_nu_nu [in Struct_congr]
sc_nu_nil_rev [in Struct_congr]
sc_nu_nil [in Struct_congr]
sc_scope_rev [in Struct_congr]
sc_scope [in Struct_congr]
sc_par_nil_conv [in Struct_congr]
sc_par_nil [in Struct_congr]
sc_par_comm [in Struct_congr]
sc_par_assoc_rev [in Struct_congr]
sc_par_assoc [in Struct_congr]
sc0_def [in Struct_congr]
st_conc [in Bisimulation]
st_abs [in Bisimulation]
st_proc [in Bisimulation]
T
tau [in Semantics]V
VS [in Binders]VZ [in Binders]
Inductive Index
A
abs [in Semantics]agent [in Semantics]
C
conc [in Semantics]H
howe [in Howe]howe' [in Howe]
I
incV [in Binders]is_proc [in Syntax]
L
label [in Semantics]lts [in Semantics]
N
name [in Binders]P
proc [in Syntax]R
rel_renamed [in Bisimulation]S
sc0 [in Struct_congr]sim_test [in Bisimulation]
struct_congr [in Struct_congr]
Abbreviation Index
L
lpseudo_sim [in HoweSound]P
PO [in Syntax]proc0 [in Syntax]
proc1 [in Syntax]
pseudo_sim [in HoweSound]
R
refl0 [in HoweSound]Rincl [in Utils]
S
shiftN [in Syntax]shiftV [in Syntax]
shiftV1 [in Syntax]
subst [in Syntax]
T
test_conc [in Bisimulation]test_abs [in Bisimulation]
test_proc [in Bisimulation]
Definition Index
A
abs_new [in Semantics]abs_parr [in Semantics]
abs_parl [in Semantics]
amapN [in Semantics]
appl [in Semantics]
appr [in Semantics]
asubst [in Semantics]
B
bind [in Syntax]bisimilarity [in Bisimulation]
bisimulation [in Bisimulation]
bisimulation_up_to_sc [in Struct_congr]
bn [in Syntax]
bn_agent [in Semantics]
body [in LNProperties]
C
close [in Syntax]cmapN [in Semantics]
comp [in Binders]
comp_rel [in Utils]
conc_new [in Semantics]
conc_parr [in Semantics]
conc_parl [in Semantics]
conc_wf [in Semantics]
D
decomp [in LNProperties]decomp_f [in LNProperties]
down [in Semantics]
down_fset [in Syntax]
F
filter_fset [in Utils]fmapN [in Semantics]
fn [in Syntax]
fn_agent [in Semantics]
fn_lab [in Semantics]
fshiftN [in Semantics]
G
genNu [in Semantics]I
id_bisim [in Bisimulation]incV_map [in Binders]
is_proc_Rel [in Bisimulation]
is_agent [in Semantics]
L
liftN [in Binders]liftV [in Syntax]
M
mapN [in Syntax]mapV [in Syntax]
map_fset [in Utils]
N
new [in Semantics]O
open [in Syntax]open_extension [in Bisimulation]
open_agent [in Semantics]
open_list [in LNProperties]
P
parl [in Semantics]parr [in Semantics]
permut [in Binders]
R
rename_compatible [in Bisimulation]S
simulation [in Bisimulation]simulation_late [in Bisimulation]
simulation_up_to_sc [in Struct_congr]
size [in Syntax]
subst_lab [in LNSemantics]
subst_func [in Syntax]
T
to_list [in Utils]| 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 | (425 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 | (5 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 | (10 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 | (254 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 | (69 entries) |
| Inductive Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (15 entries) |
| 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 | (14 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 | (58 entries) |
This page has been generated by coqdoc