| 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 | (357 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 | (8 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 | (173 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 | (98 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 | (14 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 | (21 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (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 | (24 entries) |
Global Index
A
abs [abbreviation, in Semantics]abs_to_proc [lemma, in HoweSound]
abs_parr [definition, in Semantics]
abs_parl [definition, in Semantics]
appl [definition, in Semantics]
appr [definition, in Semantics]
B
beta_exp [axiom, in HOASSyntax]bind [definition, in HOASSyntax]
Binders [library]
bind_mapV_comp [lemma, in HOASSyntax]
bind_bind [lemma, in HOASSyntax]
bind_mapV [lemma, in HOASSyntax]
bind_proc0 [lemma, in HOASSyntax]
bind_return' [lemma, in HOASSyntax]
bind_return [lemma, in HOASSyntax]
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]
C
cnew_unique [lemma, in Semantics]cnew_rename [lemma, in Semantics]
cnew_notin_rev [lemma, in Semantics]
cnew_notin [lemma, in Semantics]
cnew_nu [constructor, in Semantics]
cnew_no_extr [constructor, in Semantics]
cnew_extr [constructor, in Semantics]
comp_bisim_is_bisim [lemma, in Bisimulation]
comp_sim_is_sim [lemma, in Bisimulation]
comp_assoc [lemma, in Bisimulation]
comp_trans [lemma, in Bisimulation]
comp_rel [definition, in Bisimulation]
conc [inductive, in Semantics]
conc_to_proc [lemma, in HoweSound]
conc_notin_arg [lemma, in Semantics]
conc_unused_arg [lemma, in Semantics]
conc_notin_rename [lemma, in Semantics]
conc_notin_rename' [lemma, in Semantics]
conc_new [inductive, in Semantics]
conc_parr [definition, in Semantics]
conc_parl [definition, in Semantics]
conc_wf [definition, in Semantics]
conc_unsat [axiom, in Semantics]
conc_ho_ho_beta_exp [axiom, in Semantics]
conc_ho_beta_exp [axiom, in Semantics]
conc_beta_exp [axiom, in Semantics]
conc_ext [axiom, in Semantics]
conc_notin_ho [definition, in Semantics]
conc_notin [inductive, in Semantics]
conc_nu [constructor, in Semantics]
conc_def [constructor, in Semantics]
cwf_aux_change [lemma, in Semantics]
cwf_include [lemma, in Semantics]
cwf_new [lemma, in Semantics]
cwf_aux_rename [lemma, in Semantics]
cwf_parr [lemma, in Semantics]
cwf_parl [lemma, in Semantics]
cwf_nu [constructor, in Semantics]
cwf_def [constructor, in Semantics]
cwf_aux [inductive, in Semantics]
D
dec_cnew [lemma, in Semantics]dec_name [axiom, in HOASSyntax]
E
equal_f [lemma, in Semantics]exists_pull [lemma, in HoweSound]
exists_pull' [lemma, in HoweSound]
exists_sname [lemma, in Semantics]
exists_cnew [lemma, in Semantics]
exists_cnew' [lemma, in Semantics]
exists_szc [lemma, in Semantics]
exists_sz [lemma, in HOASSyntax]
F
fun_ho_beta_exp [axiom, in Bisimulation]fun_beta_exp [axiom, in Bisimulation]
H
HOASSyntax [library]howe [inductive, in Howe]
Howe [library]
HoweSound [library]
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_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'_rename [lemma, in Howe]
howe'_implies_howe [lemma, in Howe]
howe'_ind_size [lemma, in Howe]
ho_ho_beta_exp [axiom, in HOASSyntax]
ho_beta_exp [axiom, in HOASSyntax]
I
id_bisim_bisim [lemma, in Bisimulation]id_bisim [definition, in Bisimulation]
incV [inductive, in Binders]
incV_map [definition, in Binders]
isin [inductive, in HOASSyntax]
isinV [inductive, in HOASSyntax]
isinV_rename [lemma, in HOASSyntax]
isinV_rename' [lemma, in HOASSyntax]
isinV_nu [constructor, in HOASSyntax]
isinV_par2 [constructor, in HOASSyntax]
isinV_par1 [constructor, in HOASSyntax]
isinV_snd2 [constructor, in HOASSyntax]
isinV_snd1 [constructor, in HOASSyntax]
isinV_inp [constructor, in HOASSyntax]
isinV_var [constructor, in HOASSyntax]
isin_arg [lemma, in HOASSyntax]
isin_arg' [lemma, in HOASSyntax]
isin_notin_dec [lemma, in HOASSyntax]
isin_rename [lemma, in HOASSyntax]
isin_rename' [lemma, in HOASSyntax]
isin_not_notin [lemma, in HOASSyntax]
isin_nu [constructor, in HOASSyntax]
isin_par2 [constructor, in HOASSyntax]
isin_par1 [constructor, in HOASSyntax]
isin_snd_name [constructor, in HOASSyntax]
isin_snd2 [constructor, in HOASSyntax]
isin_snd1 [constructor, in HOASSyntax]
isin_inp_name [constructor, in HOASSyntax]
isin_inp [constructor, in HOASSyntax]
L
LibDefaultSimp [library]liftV [definition, in HOASSyntax]
listproc [definition, in HOASSyntax]
listproc_in [lemma, in HOASSyntax]
list_in_proc_change [lemma, in Semantics]
list_in_proc_rename [lemma, in Semantics]
list_of_conc [lemma, in Semantics]
list_in_proc_rec [constructor, in Semantics]
list_in_proc_nil [constructor, in Semantics]
list_in_proc [inductive, in Semantics]
list_of_proc [lemma, in HOASSyntax]
lpseudo_sim [abbreviation, in HoweSound]
ltsabs [inductive, in Semantics]
ltsabs_notin_label [lemma, in Semantics]
ltsabs_unused_arg [lemma, in Semantics]
ltsabs_notin_ho [lemma, in Semantics]
ltsabs_notin [lemma, in Semantics]
ltsabs_rename [lemma, in Semantics]
ltsa_new [constructor, in Semantics]
ltsa_parr [constructor, in Semantics]
ltsa_parl [constructor, in Semantics]
ltsa_inp [constructor, in Semantics]
ltsconc [inductive, in Semantics]
ltsconc_notin_label [lemma, in Semantics]
ltsconc_unused_arg [lemma, in Semantics]
ltsconc_notin_ho [lemma, in Semantics]
ltsconc_notin [lemma, in Semantics]
ltsconc_rename [lemma, in Semantics]
ltsc_new [constructor, in Semantics]
ltsc_parr [constructor, in Semantics]
ltsc_parl [constructor, in Semantics]
ltsc_out [constructor, in Semantics]
ltsproc [inductive, in Semantics]
ltsproc_unused_arg [lemma, in Semantics]
ltsproc_notin_ho [lemma, in Semantics]
ltsproc_notin [lemma, in Semantics]
ltsproc_rename [lemma, in Semantics]
ltsp_taur [constructor, in Semantics]
ltsp_taul [constructor, in Semantics]
ltsp_new [constructor, in Semantics]
ltsp_parr [constructor, in Semantics]
ltsp_parl [constructor, in Semantics]
lts_conc_wf [lemma, in Semantics]
lts_taur' [lemma, in Semantics]
lts_taul' [lemma, in Semantics]
M
mapV [definition, in HOASSyntax]mapV_mapV [lemma, in HOASSyntax]
mapV_id [lemma, in HOASSyntax]
N
name [axiom, in HOASSyntax]nc_parr_rev [lemma, in Semantics]
nc_parr [lemma, in Semantics]
nc_parl_rev [lemma, in Semantics]
nc_parl [lemma, in Semantics]
nc_nu [constructor, in Semantics]
nc_def [constructor, in Semantics]
neq_symmetry [lemma, in Semantics]
notin [inductive, in HOASSyntax]
notin_appl [lemma, in Semantics]
notin_appr [lemma, in Semantics]
notin_bind_rev [lemma, in HOASSyntax]
notin_bind [lemma, in HOASSyntax]
notin_mapV_rev [lemma, in HOASSyntax]
notin_mapV [lemma, in HOASSyntax]
notin_arg [lemma, in HOASSyntax]
notin_rename [lemma, in HOASSyntax]
notin_rename' [lemma, in HOASSyntax]
notin_not_isin [lemma, in HOASSyntax]
notin_ho [definition, in HOASSyntax]
notin_nu [constructor, in HOASSyntax]
notin_par [constructor, in HOASSyntax]
notin_snd [constructor, in HOASSyntax]
notin_inp [constructor, in HOASSyntax]
notin_nil [constructor, in HOASSyntax]
notin_var [constructor, in HOASSyntax]
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_extension [definition, in Bisimulation]
P
PO [abbreviation, in HOASSyntax]proc [inductive, in HOASSyntax]
proc_ext [axiom, in HOASSyntax]
proc0 [abbreviation, in HOASSyntax]
proc1 [abbreviation, in HOASSyntax]
pr_nil [constructor, in HOASSyntax]
pr_nu [constructor, in HOASSyntax]
pr_par [constructor, in HOASSyntax]
pr_snd [constructor, in HOASSyntax]
pr_inp [constructor, in HOASSyntax]
pr_var [constructor, in HOASSyntax]
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]
pull [inductive, in HoweSound]
pull_conc_wf [lemma, in HoweSound]
pull_rename [lemma, in HoweSound]
pull_size [lemma, in HoweSound]
pull_conc_new [lemma, in HoweSound]
pull_nunu [constructor, in HoweSound]
pull_nudef [constructor, in HoweSound]
R
rel_renamed [inductive, in Bisimulation]rename_compatible [definition, in Bisimulation]
Rincl [abbreviation, in Bisimulation]
Rincl_sc0_howe [lemma, in HoweSound]
rrenamed_def [constructor, in Bisimulation]
rrenamed_base [constructor, in Bisimulation]
S
sc_F_nuC_nuFC [lemma, in Struct_congr]sc_nuF_C_nuFC [lemma, in Struct_congr]
sc_F_CP_FC_P [lemma, in Struct_congr]
sc_F_PC_FC_P [lemma, in Struct_congr]
sc_PF_C_FC_P [lemma, in Struct_congr]
sc_FP_C_FC_P [lemma, in Struct_congr]
sc_F_newCQ_F_newC_Q [lemma, in Struct_congr]
sc_F_newCQ_F_newC_Q' [lemma, in Struct_congr]
sc_F_newPC_F_nuP_C [lemma, in Struct_congr]
sc_F_newPC_F_nuP_C' [lemma, in Struct_congr]
sc_nuFC_nuF_C [lemma, in Struct_congr]
sc_nuFC_nuF_C' [lemma, in Struct_congr]
sc_nuCF_newC_F [lemma, in Struct_congr]
sc_rename [lemma, in Struct_congr]
sc_appl_appr [lemma, in Struct_congr]
sc_appr_appl [lemma, in Struct_congr]
sc_bind [lemma, in Struct_congr]
sc_bind' [lemma, in Struct_congr]
sc_liftV [lemma, in Struct_congr]
sc_mapV [lemma, in Struct_congr]
sc_symmetric [lemma, in Struct_congr]
sc_refl [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 [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 [abbreviation, in Struct_congr]
Semantics [library]
sep [lemma, in HOASSyntax]
shiftV [abbreviation, in HOASSyntax]
shiftV1 [abbreviation, in HOASSyntax]
simulation [definition, in Bisimulation]
simulation_up_to_sc_howe [lemma, in HoweSound]
simulation_rel_renamed [lemma, in Bisimulation]
simulation_up_to_sc [definition, in Struct_congr]
sim_sym_imply_bisim [lemma, in Bisimulation]
size [inductive, in HOASSyntax]
sizec [inductive, in Semantics]
sizec_rename [lemma, in Semantics]
size_rename [lemma, in HOASSyntax]
sn_not_eq [constructor, in Semantics]
sn_eq [constructor, in Semantics]
struct_congr_bisim [lemma, in Struct_congr]
struct_congr_sim [lemma, in Struct_congr]
struct_congr_sim' [lemma, in Struct_congr]
struct_congr_ind' [lemma, in Struct_congr]
struct_congr [inductive, in Struct_congr]
Struct_congr [library]
subst [abbreviation, in HOASSyntax]
subst_name [inductive, in Semantics]
subst_shift [lemma, in HOASSyntax]
subst_func [definition, in HOASSyntax]
szc_nu [constructor, in Semantics]
szc_def [constructor, in Semantics]
sz_nu [constructor, in HOASSyntax]
sz_par [constructor, in HOASSyntax]
sz_out [constructor, in HOASSyntax]
sz_inp [constructor, in HOASSyntax]
sz_nil [constructor, in HOASSyntax]
sz_var [constructor, in HOASSyntax]
T
test_conc [abbreviation, in Bisimulation]test_abs [abbreviation, in Bisimulation]
test_proc [abbreviation, in Bisimulation]
transp_bisim_is_bisim [lemma, in Bisimulation]
two_unused_args [lemma, in Semantics]
U
union_sim_is_sim [lemma, in Bisimulation]unsat [axiom, in HOASSyntax]
unsat_lpc [lemma, in Semantics]
unsat_pc [lemma, in Semantics]
unsat_proc_of_conc [lemma, in Semantics]
unsat_lc [lemma, in Semantics]
unsat_list [lemma, in HOASSyntax]
unsat_lp [lemma, in HOASSyntax]
unused_arg [lemma, in HOASSyntax]
up_to_sc_sound [lemma, in Struct_congr]
up_to_sc_sim [lemma, in Struct_congr]
V
VS [constructor, in Binders]VZ [constructor, in Binders]
other
_ ° _ [notation, in Bisimulation]_ // _ [notation, in HOASSyntax]
_ !( _ ) _ [notation, in HOASSyntax]
_ ? _ [notation, in HOASSyntax]
nu _ [notation, in HOASSyntax]
Notation Index
other
_ ° _ [in Bisimulation]_ // _ [in HOASSyntax]
_ !( _ ) _ [in HOASSyntax]
_ ? _ [in HOASSyntax]
nu _ [in HOASSyntax]
Library Index
B
BindersBisimulation
H
HOASSyntaxHowe
HoweSound
L
LibDefaultSimpS
SemanticsStruct_congr
Lemma Index
A
abs_to_proc [in HoweSound]B
bind_mapV_comp [in HOASSyntax]bind_bind [in HOASSyntax]
bind_mapV [in HOASSyntax]
bind_proc0 [in HOASSyntax]
bind_return' [in HOASSyntax]
bind_return [in HOASSyntax]
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]
C
cnew_unique [in Semantics]cnew_rename [in Semantics]
cnew_notin_rev [in Semantics]
cnew_notin [in Semantics]
comp_bisim_is_bisim [in Bisimulation]
comp_sim_is_sim [in Bisimulation]
comp_assoc [in Bisimulation]
comp_trans [in Bisimulation]
conc_to_proc [in HoweSound]
conc_notin_arg [in Semantics]
conc_unused_arg [in Semantics]
conc_notin_rename [in Semantics]
conc_notin_rename' [in Semantics]
cwf_aux_change [in Semantics]
cwf_include [in Semantics]
cwf_new [in Semantics]
cwf_aux_rename [in Semantics]
cwf_parr [in Semantics]
cwf_parl [in Semantics]
D
dec_cnew [in Semantics]E
equal_f [in Semantics]exists_pull [in HoweSound]
exists_pull' [in HoweSound]
exists_sname [in Semantics]
exists_cnew [in Semantics]
exists_cnew' [in Semantics]
exists_szc [in Semantics]
exists_sz [in HOASSyntax]
H
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_oe [in Howe]
howe_refl [in Howe]
howe_rename [in Howe]
howe_implies_howe' [in Howe]
howe'_rename [in Howe]
howe'_implies_howe [in Howe]
howe'_ind_size [in Howe]
I
id_bisim_bisim [in Bisimulation]isinV_rename [in HOASSyntax]
isinV_rename' [in HOASSyntax]
isin_arg [in HOASSyntax]
isin_arg' [in HOASSyntax]
isin_notin_dec [in HOASSyntax]
isin_rename [in HOASSyntax]
isin_rename' [in HOASSyntax]
isin_not_notin [in HOASSyntax]
L
listproc_in [in HOASSyntax]list_in_proc_change [in Semantics]
list_in_proc_rename [in Semantics]
list_of_conc [in Semantics]
list_of_proc [in HOASSyntax]
ltsabs_notin_label [in Semantics]
ltsabs_unused_arg [in Semantics]
ltsabs_notin_ho [in Semantics]
ltsabs_notin [in Semantics]
ltsabs_rename [in Semantics]
ltsconc_notin_label [in Semantics]
ltsconc_unused_arg [in Semantics]
ltsconc_notin_ho [in Semantics]
ltsconc_notin [in Semantics]
ltsconc_rename [in Semantics]
ltsproc_unused_arg [in Semantics]
ltsproc_notin_ho [in Semantics]
ltsproc_notin [in Semantics]
ltsproc_rename [in Semantics]
lts_conc_wf [in Semantics]
lts_taur' [in Semantics]
lts_taul' [in Semantics]
M
mapV_mapV [in HOASSyntax]mapV_id [in HOASSyntax]
N
nc_parr_rev [in Semantics]nc_parr [in Semantics]
nc_parl_rev [in Semantics]
nc_parl [in Semantics]
neq_symmetry [in Semantics]
notin_appl [in Semantics]
notin_appr [in Semantics]
notin_bind_rev [in HOASSyntax]
notin_bind [in HOASSyntax]
notin_mapV_rev [in HOASSyntax]
notin_mapV [in HOASSyntax]
notin_arg [in HOASSyntax]
notin_rename [in HOASSyntax]
notin_rename' [in HOASSyntax]
notin_not_isin [in HOASSyntax]
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]
P
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]
pull_conc_wf [in HoweSound]
pull_rename [in HoweSound]
pull_size [in HoweSound]
pull_conc_new [in HoweSound]
R
Rincl_sc0_howe [in HoweSound]S
sc_F_nuC_nuFC [in Struct_congr]sc_nuF_C_nuFC [in Struct_congr]
sc_F_CP_FC_P [in Struct_congr]
sc_F_PC_FC_P [in Struct_congr]
sc_PF_C_FC_P [in Struct_congr]
sc_FP_C_FC_P [in Struct_congr]
sc_F_newCQ_F_newC_Q [in Struct_congr]
sc_F_newCQ_F_newC_Q' [in Struct_congr]
sc_F_newPC_F_nuP_C [in Struct_congr]
sc_F_newPC_F_nuP_C' [in Struct_congr]
sc_nuFC_nuF_C [in Struct_congr]
sc_nuFC_nuF_C' [in Struct_congr]
sc_nuCF_newC_F [in Struct_congr]
sc_rename [in Struct_congr]
sc_appl_appr [in Struct_congr]
sc_appr_appl [in Struct_congr]
sc_bind [in Struct_congr]
sc_bind' [in Struct_congr]
sc_liftV [in Struct_congr]
sc_mapV [in Struct_congr]
sc_symmetric [in Struct_congr]
sc_refl [in Struct_congr]
sep [in HOASSyntax]
simulation_up_to_sc_howe [in HoweSound]
simulation_rel_renamed [in Bisimulation]
sim_sym_imply_bisim [in Bisimulation]
sizec_rename [in Semantics]
size_rename [in HOASSyntax]
struct_congr_bisim [in Struct_congr]
struct_congr_sim [in Struct_congr]
struct_congr_sim' [in Struct_congr]
struct_congr_ind' [in Struct_congr]
subst_shift [in HOASSyntax]
T
transp_bisim_is_bisim [in Bisimulation]two_unused_args [in Semantics]
U
union_sim_is_sim [in Bisimulation]unsat_lpc [in Semantics]
unsat_pc [in Semantics]
unsat_proc_of_conc [in Semantics]
unsat_lc [in Semantics]
unsat_list [in HOASSyntax]
unsat_lp [in HOASSyntax]
unused_arg [in HOASSyntax]
up_to_sc_sound [in Struct_congr]
up_to_sc_sim [in Struct_congr]
Constructor Index
C
cnew_nu [in Semantics]cnew_no_extr [in Semantics]
cnew_extr [in Semantics]
conc_nu [in Semantics]
conc_def [in Semantics]
cwf_nu [in Semantics]
cwf_def [in Semantics]
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
isinV_nu [in HOASSyntax]isinV_par2 [in HOASSyntax]
isinV_par1 [in HOASSyntax]
isinV_snd2 [in HOASSyntax]
isinV_snd1 [in HOASSyntax]
isinV_inp [in HOASSyntax]
isinV_var [in HOASSyntax]
isin_nu [in HOASSyntax]
isin_par2 [in HOASSyntax]
isin_par1 [in HOASSyntax]
isin_snd_name [in HOASSyntax]
isin_snd2 [in HOASSyntax]
isin_snd1 [in HOASSyntax]
isin_inp_name [in HOASSyntax]
isin_inp [in HOASSyntax]
L
list_in_proc_rec [in Semantics]list_in_proc_nil [in Semantics]
ltsa_new [in Semantics]
ltsa_parr [in Semantics]
ltsa_parl [in Semantics]
ltsa_inp [in Semantics]
ltsc_new [in Semantics]
ltsc_parr [in Semantics]
ltsc_parl [in Semantics]
ltsc_out [in Semantics]
ltsp_taur [in Semantics]
ltsp_taul [in Semantics]
ltsp_new [in Semantics]
ltsp_parr [in Semantics]
ltsp_parl [in Semantics]
N
nc_nu [in Semantics]nc_def [in Semantics]
notin_nu [in HOASSyntax]
notin_par [in HOASSyntax]
notin_snd [in HOASSyntax]
notin_inp [in HOASSyntax]
notin_nil [in HOASSyntax]
notin_var [in HOASSyntax]
P
pr_nil [in HOASSyntax]pr_nu [in HOASSyntax]
pr_par [in HOASSyntax]
pr_snd [in HOASSyntax]
pr_inp [in HOASSyntax]
pr_var [in HOASSyntax]
pull_nunu [in HoweSound]
pull_nudef [in HoweSound]
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 [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]
sn_not_eq [in Semantics]
sn_eq [in Semantics]
szc_nu [in Semantics]
szc_def [in Semantics]
sz_nu [in HOASSyntax]
sz_par [in HOASSyntax]
sz_out [in HOASSyntax]
sz_inp [in HOASSyntax]
sz_nil [in HOASSyntax]
sz_var [in HOASSyntax]
V
VS [in Binders]VZ [in Binders]
Axiom Index
B
beta_exp [in HOASSyntax]C
conc_unsat [in Semantics]conc_ho_ho_beta_exp [in Semantics]
conc_ho_beta_exp [in Semantics]
conc_beta_exp [in Semantics]
conc_ext [in Semantics]
D
dec_name [in HOASSyntax]F
fun_ho_beta_exp [in Bisimulation]fun_beta_exp [in Bisimulation]
H
ho_ho_beta_exp [in HOASSyntax]ho_beta_exp [in HOASSyntax]
N
name [in HOASSyntax]P
proc_ext [in HOASSyntax]U
unsat [in HOASSyntax]Inductive Index
C
conc [in Semantics]conc_new [in Semantics]
conc_notin [in Semantics]
cwf_aux [in Semantics]
H
howe [in Howe]howe' [in Howe]
I
incV [in Binders]isin [in HOASSyntax]
isinV [in HOASSyntax]
L
list_in_proc [in Semantics]ltsabs [in Semantics]
ltsconc [in Semantics]
ltsproc [in Semantics]
N
notin [in HOASSyntax]P
proc [in HOASSyntax]pull [in HoweSound]
R
rel_renamed [in Bisimulation]S
size [in HOASSyntax]sizec [in Semantics]
struct_congr [in Struct_congr]
subst_name [in Semantics]
Abbreviation Index
A
abs [in Semantics]L
lpseudo_sim [in HoweSound]P
PO [in HOASSyntax]proc0 [in HOASSyntax]
proc1 [in HOASSyntax]
pseudo_sim [in HoweSound]
R
Rincl [in Bisimulation]S
sc0 [in Struct_congr]shiftV [in HOASSyntax]
shiftV1 [in HOASSyntax]
subst [in HOASSyntax]
T
test_conc [in Bisimulation]test_abs [in Bisimulation]
test_proc [in Bisimulation]
Definition Index
A
abs_parr [in Semantics]abs_parl [in Semantics]
appl [in Semantics]
appr [in Semantics]
B
bind [in HOASSyntax]bisimilarity [in Bisimulation]
bisimulation [in Bisimulation]
bisimulation_up_to_sc [in Struct_congr]
C
comp_rel [in Bisimulation]conc_parr [in Semantics]
conc_parl [in Semantics]
conc_wf [in Semantics]
conc_notin_ho [in Semantics]
I
id_bisim [in Bisimulation]incV_map [in Binders]
L
liftV [in HOASSyntax]listproc [in HOASSyntax]
M
mapV [in HOASSyntax]N
notin_ho [in HOASSyntax]O
open_extension [in Bisimulation]R
rename_compatible [in Bisimulation]S
simulation [in Bisimulation]simulation_up_to_sc [in Struct_congr]
subst_func [in HOASSyntax]
| 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 | (357 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 | (8 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 | (173 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 | (98 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 | (14 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 | (21 entries) |
| Abbreviation Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (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 | (24 entries) |
This page has been generated by coqdoc