| 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 | (608 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 | (17 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (24 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 | (15 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 | (13 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 | (114 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 | (236 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 | (74 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) |
| 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 | (4 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 | (25 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (71 entries) |
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]
add [abbreviation, in MyFset]
agent [inductive, in Semantics]
ag_conc [constructor, in Semantics]
ag_abs [constructor, in Semantics]
ag_proc [constructor, in Semantics]
amapN [definition, in Semantics]
amapN_parr [lemma, in Semantics]
amapN_parl [lemma, in Semantics]
amapN_new [lemma, in Semantics]
amapN_subset [lemma, in Semantics]
amapN_eq_on_fn [lemma, in Semantics]
amapN_id [lemma, in Semantics]
amapN_amapN [lemma, in Semantics]
appl [definition, in Semantics]
appr [definition, in Semantics]
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_eq_on_fv [lemma, in Bisimulation]
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
cardinal [abbreviation, in MyFset]card_In [lemma, in Bisimulation]
card_max [lemma, in Bisimulation]
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_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_new [definition, in Semantics]
conc_parr [definition, in Semantics]
conc_parl [definition, in Semantics]
conc_wf [definition, in Semantics]
conc_def [constructor, in Semantics]
CoqFSetDecide [library]
CoqFSetInterface [library]
D
Decide [module, in CoqFSetDecide]diff [abbreviation, in MyFset]
down [definition, in Semantics]
Down [inductive, in Bisimulation]
downfs [definition, in Syntax]
downfs_empty_rev [lemma, in Syntax]
downfs_empty [lemma, in Syntax]
downfs_0_spec [lemma, in Syntax]
downfs_spec [lemma, in Syntax]
downV [definition, in Bisimulation]
down_lab [definition, in Semantics]
Down_finite [lemma, in Bisimulation]
Down_empty [lemma, in Bisimulation]
Down_def [constructor, in Bisimulation]
E
empty [abbreviation, in MyFset]F
filter [abbreviation, in MyFset]filter_union [lemma, in MyFset]
filter_subset [lemma, in MyFset]
filter_id [lemma, in MyFset]
fmapN [definition, in Semantics]
fn [definition, in Syntax]
fn_subst [lemma, in Syntax]
fn_bind [lemma, in Syntax]
fn_bind' [lemma, in Syntax]
fn_mapN [lemma, in Syntax]
fn_mapV [lemma, in Syntax]
fn_parr [lemma, in Semantics]
fn_parl [lemma, in Semantics]
fn_appr_subset [lemma, in Semantics]
fn_C_par [lemma, in Semantics]
fn_appr_appl [lemma, in Semantics]
fn_agent_new [lemma, in Semantics]
fn_agent_amapN [lemma, in Semantics]
fn_genNu [lemma, in Semantics]
fn_agent [definition, in Semantics]
fn_lab [definition, in Semantics]
fresh_above_n [lemma, in Bisimulation]
FSetExtra [library]
FSetWeakNotin [library]
fshiftN [definition, in Semantics]
fv [definition, in Bisimulation]
fv_finite [lemma, in Bisimulation]
G
genNu [definition, in Semantics]genNu_fold [lemma, in Semantics]
H
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_genNu [lemma, in Howe]
howe_mapN [lemma, in Howe]
howe_oe [lemma, in Howe]
howe_refl [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'_mapN [lemma, in Howe]
howe'_implies_howe [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]
IndexSetDecide [module, in MyFset]
IndexSetFacts [module, in MyFset]
IndexSetImpl [module, in MyFset]
IndexSetNotin [module, in MyFset]
IndexSetProperties [module, in MyFset]
indices [abbreviation, in MyFset]
injective_cardinal [lemma, in Bisimulation]
inp [constructor, in Semantics]
inter [abbreviation, in MyFset]
invert_f_subs [lemma, in Bisimulation]
invert_f_proc [lemma, in Bisimulation]
L
label [inductive, in Semantics]late_implies_sim [lemma, in Bisimulation]
LibDefaultSimp [library]
liftN [definition, in Binders]
liftN_preserves_injectivity [lemma, in Binders]
liftN_0 [lemma, in Binders]
liftN_liftN [lemma, in Binders]
liftN_S [lemma, in Binders]
liftV [definition, in Syntax]
lmapN [definition, in Semantics]
lpseudo_sim [abbreviation, in HoweSound]
lts [inductive, in Semantics]
lts_fn [lemma, in Semantics]
lts_conc_wf [lemma, in Semantics]
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
Make [module, in FSetExtra]make_In [definition, in Bisimulation]
Make.disjoint [definition, in FSetExtra]
Make.fresh_list [definition, in FSetExtra]
Make.notin [definition, in FSetExtra]
map [definition, in MyFset]
mapN [definition, in Syntax]
mapN_mapN [lemma, in Syntax]
mapN_id' [lemma, in Syntax]
mapN_id [lemma, in Syntax]
mapN_lts_rev [lemma, in Semantics]
mapN_lts [lemma, in Semantics]
mapN_appr [lemma, in Semantics]
mapN_appl [lemma, in Semantics]
mapN_eq_on_fn_rev [lemma, in Semantics]
mapN_eq_on_fn [lemma, in Semantics]
mapN_concwf [lemma, in Semantics]
mapN_genNu [lemma, in Semantics]
mapV [definition, in Syntax]
mapV_mapN [lemma, in Syntax]
mapV_mapV [lemma, in Syntax]
mapV_id [lemma, in Syntax]
map_inter [lemma, in MyFset]
map_eq [lemma, in MyFset]
map_subset [lemma, in MyFset]
map_union [lemma, in MyFset]
map_singleton [lemma, in MyFset]
map_empty [lemma, in MyFset]
map_id [lemma, in MyFset]
map_spec [lemma, in MyFset]
max_elt_spec_empty [lemma, in MyFset]
max_elt_spec [lemma, in MyFset]
max_elt [abbreviation, in MyFset]
max_In_S [lemma, in Bisimulation]
MyFset [library]
N
name [definition, in Binders]new [definition, in Semantics]
Notin_fun.test_solve_notin_7 [lemma, in FSetWeakNotin]
Notin_fun.test_solve_notin_6 [lemma, in FSetWeakNotin]
Notin_fun.test_solve_notin_5 [lemma, in FSetWeakNotin]
Notin_fun.test_solve_notin_4 [lemma, in FSetWeakNotin]
Notin_fun.test_solve_notin_3 [lemma, in FSetWeakNotin]
Notin_fun.test_solve_notin_2 [lemma, in FSetWeakNotin]
Notin_fun.test_solve_notin_1 [lemma, in FSetWeakNotin]
Notin_fun.notin_diff_3 [lemma, in FSetWeakNotin]
Notin_fun.notin_diff_2 [lemma, in FSetWeakNotin]
Notin_fun.notin_diff_1 [lemma, in FSetWeakNotin]
Notin_fun.notin_inter_3 [lemma, in FSetWeakNotin]
Notin_fun.notin_inter_2 [lemma, in FSetWeakNotin]
Notin_fun.notin_inter_1 [lemma, in FSetWeakNotin]
Notin_fun.notin_union_3 [lemma, in FSetWeakNotin]
Notin_fun.notin_union_2 [lemma, in FSetWeakNotin]
Notin_fun.notin_union_1 [lemma, in FSetWeakNotin]
Notin_fun.notin_remove_3' [lemma, in FSetWeakNotin]
Notin_fun.notin_remove_3 [lemma, in FSetWeakNotin]
Notin_fun.notin_remove_2 [lemma, in FSetWeakNotin]
Notin_fun.notin_remove_1 [lemma, in FSetWeakNotin]
Notin_fun.notin_singleton_2 [lemma, in FSetWeakNotin]
Notin_fun.notin_singleton_1' [lemma, in FSetWeakNotin]
Notin_fun.notin_singleton_1 [lemma, in FSetWeakNotin]
Notin_fun.notin_add_3 [lemma, in FSetWeakNotin]
Notin_fun.notin_add_2 [lemma, in FSetWeakNotin]
Notin_fun.notin_add_1' [lemma, in FSetWeakNotin]
Notin_fun.notin_add_1 [lemma, in FSetWeakNotin]
Notin_fun.notin_empty_1 [lemma, in FSetWeakNotin]
Notin_fun.Lemmas.s' [variable, in FSetWeakNotin]
Notin_fun.Lemmas.s [variable, in FSetWeakNotin]
Notin_fun.Lemmas.y [variable, in FSetWeakNotin]
Notin_fun.Lemmas.x [variable, in FSetWeakNotin]
Notin_fun.Lemmas [section, in FSetWeakNotin]
Notin_fun.D [module, in FSetWeakNotin]
Notin_fun [module, in FSetWeakNotin]
nu_nu_conc [lemma, in Struct_congr]
nu_genNu [lemma, in Semantics]
O
oe_sc0 [lemma, in Struct_congr]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]
open_extension [definition, in Bisimulation]
out [constructor, in Semantics]
P
parl [definition, in Semantics]parr [definition, in Semantics]
permut [definition, in Binders]
permut_shiftN [lemma, in Syntax]
PO [abbreviation, in Syntax]
proc [inductive, 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
rel_renamed [inductive, in Bisimulation]remove [abbreviation, in MyFset]
rename_compatible [definition, in Bisimulation]
renaming [lemma, in Bisimulation]
renaming_subs [lemma, in Bisimulation]
renaming_proc [lemma, in Bisimulation]
renaming_sets [lemma, in Bisimulation]
restricted_fn [lemma, in Bisimulation]
Rincl [abbreviation, in Bisimulation]
Rincl_sc0_howe [lemma, in HoweSound]
rrenamed_def [constructor, in Bisimulation]
rrenamed_base [constructor, in Bisimulation]
S
S [module, in CoqFSetInterface]sc_nu_nu_permut [lemma, in Struct_congr]
sc_nuK_permut1 [lemma, in Struct_congr]
sc_nuK_compL_permutK [lemma, in Struct_congr]
sc_appl_appr [lemma, in Struct_congr]
sc_appr_appl [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_genNu [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_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 [abbreviation, in Struct_congr]
Sdep [module, in CoqFSetInterface]
Sdep.add [axiom, in CoqFSetInterface]
Sdep.Add [definition, in CoqFSetInterface]
Sdep.cardinal [axiom, in CoqFSetInterface]
Sdep.choose [axiom, in CoqFSetInterface]
Sdep.choose_equal [axiom, in CoqFSetInterface]
Sdep.compare [axiom, in CoqFSetInterface]
Sdep.diff [axiom, in CoqFSetInterface]
Sdep.E [module, in CoqFSetInterface]
Sdep.elements [axiom, in CoqFSetInterface]
Sdep.elt [definition, in CoqFSetInterface]
Sdep.empty [axiom, in CoqFSetInterface]
Sdep.Empty [definition, in CoqFSetInterface]
Sdep.eq [definition, in CoqFSetInterface]
Sdep.equal [axiom, in CoqFSetInterface]
Sdep.Equal [definition, in CoqFSetInterface]
Sdep.eq_In [axiom, in CoqFSetInterface]
Sdep.eq_trans [axiom, in CoqFSetInterface]
Sdep.eq_sym [axiom, in CoqFSetInterface]
Sdep.eq_refl [axiom, in CoqFSetInterface]
Sdep.Exists [definition, in CoqFSetInterface]
Sdep.exists_ [axiom, in CoqFSetInterface]
Sdep.filter [axiom, in CoqFSetInterface]
Sdep.fold [axiom, in CoqFSetInterface]
Sdep.for_all [axiom, in CoqFSetInterface]
Sdep.For_all [definition, in CoqFSetInterface]
Sdep.In [axiom, in CoqFSetInterface]
Sdep.inter [axiom, in CoqFSetInterface]
Sdep.is_empty [axiom, in CoqFSetInterface]
Sdep.lt [axiom, in CoqFSetInterface]
Sdep.lt_not_eq [axiom, in CoqFSetInterface]
Sdep.lt_trans [axiom, in CoqFSetInterface]
Sdep.max_elt [axiom, in CoqFSetInterface]
Sdep.mem [axiom, in CoqFSetInterface]
Sdep.min_elt [axiom, in CoqFSetInterface]
Sdep.partition [axiom, in CoqFSetInterface]
Sdep.remove [axiom, in CoqFSetInterface]
Sdep.singleton [axiom, in CoqFSetInterface]
Sdep.subset [axiom, in CoqFSetInterface]
Sdep.Subset [definition, in CoqFSetInterface]
Sdep.t [axiom, in CoqFSetInterface]
Sdep.union [axiom, in CoqFSetInterface]
_ [=] _ [notation, in CoqFSetInterface]
Semantics [library]
set_lift [lemma, in Bisimulation]
Sfun [module, in CoqFSetInterface]
Sfun [module, in FSetExtra]
Sfun.choose_3 [axiom, in CoqFSetInterface]
Sfun.compare [axiom, in CoqFSetInterface]
Sfun.disjoint [definition, in FSetExtra]
Sfun.elements_3 [axiom, in CoqFSetInterface]
Sfun.fresh_list [definition, in FSetExtra]
Sfun.lt [axiom, in CoqFSetInterface]
Sfun.lt_not_eq [axiom, in CoqFSetInterface]
Sfun.lt_trans [axiom, in CoqFSetInterface]
Sfun.max_elt_3 [axiom, in CoqFSetInterface]
Sfun.max_elt_2 [axiom, in CoqFSetInterface]
Sfun.max_elt_1 [axiom, in CoqFSetInterface]
Sfun.max_elt [axiom, in CoqFSetInterface]
Sfun.min_elt_3 [axiom, in CoqFSetInterface]
Sfun.min_elt_2 [axiom, in CoqFSetInterface]
Sfun.min_elt_1 [axiom, in CoqFSetInterface]
Sfun.min_elt [axiom, in CoqFSetInterface]
Sfun.notin [definition, in FSetExtra]
Sfun.Spec [section, in CoqFSetInterface]
Sfun.Spec.s [variable, in CoqFSetInterface]
Sfun.Spec.s' [variable, in CoqFSetInterface]
Sfun.Spec.s'' [variable, in CoqFSetInterface]
Sfun.Spec.x [variable, in CoqFSetInterface]
Sfun.Spec.y [variable, in CoqFSetInterface]
shiftN [abbreviation, in Syntax]
shiftN_injective [lemma, in Binders]
shiftN_mapN [lemma, in Semantics]
shiftV [abbreviation, in Syntax]
shiftV1 [abbreviation, in Syntax]
simulation [definition, in Bisimulation]
simulation_up_to_sc_howe [lemma, in HoweSound]
simulation_up_to_sc [definition, in Struct_congr]
simulation_rel_renamed [lemma, in Bisimulation]
simulation_late [definition, in Bisimulation]
sim_sym_imply_bisim [lemma, in Bisimulation]
sim_test_sym [lemma, in Bisimulation]
sim_test_trans [lemma, in Bisimulation]
sim_test [inductive, in Bisimulation]
singleton [abbreviation, in MyFset]
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 MyFset]
subst [abbreviation, in Syntax]
subst_shift [lemma, in Syntax]
subst_mapN [lemma, in Syntax]
subst_func [definition, in Syntax]
Syntax [library]
s_restr [definition, in Bisimulation]
S.E [module, in CoqFSetInterface]
T
tau [constructor, in Semantics]test_conc [abbreviation, in Bisimulation]
test_abs [abbreviation, in Bisimulation]
test_proc [abbreviation, in Bisimulation]
transp_bisim_is_bisim [lemma, in Bisimulation]
U
union [abbreviation, in MyFset]union_sim_is_sim [lemma, in Bisimulation]
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]
W
WDecide [module, in CoqFSetDecide]WDecide_fun.FSetDecideTestCases.test_sweirich [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir_4 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir_3 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir_2 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.function_test_2 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.function_test_1 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_too_complex [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.eq_chain_test [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_set_ops_1 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_iff_conj [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_not_In_conj [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_not_In_disj [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_disjunction [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_Subset_add_remove [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_add_In [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_In_singleton [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_neq_trans_2 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_neq_trans_1 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_trans_2 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_trans_1 [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases [module, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.dec_eq [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.dec_In [lemma, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.Equal_FSet_Prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.Subset_FSet_Prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.Empty_FSet_Prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.elt_FSet_Prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.FSet_Prop [inductive, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.not_elt_prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.impl_elt_prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.disj_elt_prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.conj_elt_prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.False_elt_prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.True_elt_prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.In_elt_prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.eq_elt_prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.eq_Prop [constructor, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.FSet_elt_Prop [inductive, in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary [module, in CoqFSetDecide]
WDecide_fun.FSetLogicalFacts.test_pull [lemma, in CoqFSetDecide]
WDecide_fun.FSetLogicalFacts.test_push [lemma, in CoqFSetDecide]
WDecide_fun.FSetLogicalFacts [module, in CoqFSetDecide]
WDecide_fun.F [module, in CoqFSetDecide]
WDecide_fun [module, in CoqFSetDecide]
WS [module, in CoqFSetInterface]
WSfun [module, in CoqFSetInterface]
WSfun.add [axiom, in CoqFSetInterface]
WSfun.add_3 [axiom, in CoqFSetInterface]
WSfun.add_2 [axiom, in CoqFSetInterface]
WSfun.add_1 [axiom, in CoqFSetInterface]
WSfun.cardinal [axiom, in CoqFSetInterface]
WSfun.cardinal_1 [axiom, in CoqFSetInterface]
WSfun.choose [axiom, in CoqFSetInterface]
WSfun.choose_2 [axiom, in CoqFSetInterface]
WSfun.choose_1 [axiom, in CoqFSetInterface]
WSfun.diff [axiom, in CoqFSetInterface]
WSfun.diff_3 [axiom, in CoqFSetInterface]
WSfun.diff_2 [axiom, in CoqFSetInterface]
WSfun.diff_1 [axiom, in CoqFSetInterface]
WSfun.elements [axiom, in CoqFSetInterface]
WSfun.elements_3w [axiom, in CoqFSetInterface]
WSfun.elements_2 [axiom, in CoqFSetInterface]
WSfun.elements_1 [axiom, in CoqFSetInterface]
WSfun.elt [definition, in CoqFSetInterface]
WSfun.empty [axiom, in CoqFSetInterface]
WSfun.Empty [definition, in CoqFSetInterface]
WSfun.empty_1 [axiom, in CoqFSetInterface]
WSfun.eq [definition, in CoqFSetInterface]
WSfun.equal [axiom, in CoqFSetInterface]
WSfun.Equal [definition, in CoqFSetInterface]
WSfun.equal_2 [axiom, in CoqFSetInterface]
WSfun.equal_1 [axiom, in CoqFSetInterface]
WSfun.eq_trans [axiom, in CoqFSetInterface]
WSfun.eq_sym [axiom, in CoqFSetInterface]
WSfun.eq_refl [axiom, in CoqFSetInterface]
WSfun.eq_dec [axiom, in CoqFSetInterface]
WSfun.Exists [definition, in CoqFSetInterface]
WSfun.exists_2 [axiom, in CoqFSetInterface]
WSfun.exists_1 [axiom, in CoqFSetInterface]
WSfun.exists_ [axiom, in CoqFSetInterface]
WSfun.filter [axiom, in CoqFSetInterface]
WSfun.filter_3 [axiom, in CoqFSetInterface]
WSfun.filter_2 [axiom, in CoqFSetInterface]
WSfun.filter_1 [axiom, in CoqFSetInterface]
WSfun.fold [axiom, in CoqFSetInterface]
WSfun.fold_1 [axiom, in CoqFSetInterface]
WSfun.for_all_2 [axiom, in CoqFSetInterface]
WSfun.for_all_1 [axiom, in CoqFSetInterface]
WSfun.for_all [axiom, in CoqFSetInterface]
WSfun.For_all [definition, in CoqFSetInterface]
WSfun.In [axiom, in CoqFSetInterface]
WSfun.inter [axiom, in CoqFSetInterface]
WSfun.inter_3 [axiom, in CoqFSetInterface]
WSfun.inter_2 [axiom, in CoqFSetInterface]
WSfun.inter_1 [axiom, in CoqFSetInterface]
WSfun.In_1 [axiom, in CoqFSetInterface]
WSfun.is_empty_2 [axiom, in CoqFSetInterface]
WSfun.is_empty_1 [axiom, in CoqFSetInterface]
WSfun.is_empty [axiom, in CoqFSetInterface]
WSfun.mem [axiom, in CoqFSetInterface]
WSfun.mem_2 [axiom, in CoqFSetInterface]
WSfun.mem_1 [axiom, in CoqFSetInterface]
WSfun.partition [axiom, in CoqFSetInterface]
WSfun.partition_2 [axiom, in CoqFSetInterface]
WSfun.partition_1 [axiom, in CoqFSetInterface]
WSfun.remove [axiom, in CoqFSetInterface]
WSfun.remove_3 [axiom, in CoqFSetInterface]
WSfun.remove_2 [axiom, in CoqFSetInterface]
WSfun.remove_1 [axiom, in CoqFSetInterface]
WSfun.singleton [axiom, in CoqFSetInterface]
WSfun.singleton_2 [axiom, in CoqFSetInterface]
WSfun.singleton_1 [axiom, in CoqFSetInterface]
WSfun.Spec [section, in CoqFSetInterface]
WSfun.Spec.Filter [section, in CoqFSetInterface]
WSfun.Spec.Filter.f [variable, in CoqFSetInterface]
WSfun.Spec.s [variable, in CoqFSetInterface]
WSfun.Spec.s' [variable, in CoqFSetInterface]
WSfun.Spec.s'' [variable, in CoqFSetInterface]
WSfun.Spec.x [variable, in CoqFSetInterface]
WSfun.Spec.y [variable, in CoqFSetInterface]
WSfun.subset [axiom, in CoqFSetInterface]
WSfun.Subset [definition, in CoqFSetInterface]
WSfun.subset_2 [axiom, in CoqFSetInterface]
WSfun.subset_1 [axiom, in CoqFSetInterface]
WSfun.t [axiom, in CoqFSetInterface]
WSfun.union [axiom, in CoqFSetInterface]
WSfun.union_3 [axiom, in CoqFSetInterface]
WSfun.union_2 [axiom, in CoqFSetInterface]
WSfun.union_1 [axiom, in CoqFSetInterface]
_ [<=] _ [notation, in CoqFSetInterface]
_ [=] _ [notation, in CoqFSetInterface]
WS.E [module, in CoqFSetInterface]
other
_ \n _ (set_scope) [notation, in MyFset]_ \- _ (set_scope) [notation, in MyFset]
_ \u _ (set_scope) [notation, in MyFset]
_ \notin _ (set_scope) [notation, in MyFset]
_ \in _ (set_scope) [notation, in MyFset]
\{ _ } (set_scope) [notation, in MyFset]
\{} (set_scope) [notation, in MyFset]
_ \c _ (set_scope) [notation, in MyFset]
_ [=] _ (set_scope) [notation, in MyFset]
_ // _ [notation, in Syntax]
_ !( _ ) _ [notation, in Syntax]
_ ? _ [notation, in Syntax]
_ ° _ [notation, in Bisimulation]
nu _ [notation, in Syntax]
Notation Index
S
_ [=] _ [in CoqFSetInterface]W
_ [<=] _ [in CoqFSetInterface]_ [=] _ [in CoqFSetInterface]
other
_ \n _ (set_scope) [in MyFset]_ \- _ (set_scope) [in MyFset]
_ \u _ (set_scope) [in MyFset]
_ \notin _ (set_scope) [in MyFset]
_ \in _ (set_scope) [in MyFset]
\{ _ } (set_scope) [in MyFset]
\{} (set_scope) [in MyFset]
_ \c _ (set_scope) [in MyFset]
_ [=] _ (set_scope) [in MyFset]
_ // _ [in Syntax]
_ !( _ ) _ [in Syntax]
_ ? _ [in Syntax]
_ ° _ [in Bisimulation]
nu _ [in Syntax]
Module Index
D
Decide [in CoqFSetDecide]I
IndexSetDecide [in MyFset]IndexSetFacts [in MyFset]
IndexSetImpl [in MyFset]
IndexSetNotin [in MyFset]
IndexSetProperties [in MyFset]
M
Make [in FSetExtra]N
Notin_fun.D [in FSetWeakNotin]Notin_fun [in FSetWeakNotin]
S
S [in CoqFSetInterface]Sdep [in CoqFSetInterface]
Sdep.E [in CoqFSetInterface]
Sfun [in CoqFSetInterface]
Sfun [in FSetExtra]
S.E [in CoqFSetInterface]
W
WDecide [in CoqFSetDecide]WDecide_fun.FSetDecideTestCases [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary [in CoqFSetDecide]
WDecide_fun.FSetLogicalFacts [in CoqFSetDecide]
WDecide_fun.F [in CoqFSetDecide]
WDecide_fun [in CoqFSetDecide]
WS [in CoqFSetInterface]
WSfun [in CoqFSetInterface]
WS.E [in CoqFSetInterface]
Variable Index
N
Notin_fun.Lemmas.s' [in FSetWeakNotin]Notin_fun.Lemmas.s [in FSetWeakNotin]
Notin_fun.Lemmas.y [in FSetWeakNotin]
Notin_fun.Lemmas.x [in FSetWeakNotin]
S
Sfun.Spec.s [in CoqFSetInterface]Sfun.Spec.s' [in CoqFSetInterface]
Sfun.Spec.s'' [in CoqFSetInterface]
Sfun.Spec.x [in CoqFSetInterface]
Sfun.Spec.y [in CoqFSetInterface]
W
WSfun.Spec.Filter.f [in CoqFSetInterface]WSfun.Spec.s [in CoqFSetInterface]
WSfun.Spec.s' [in CoqFSetInterface]
WSfun.Spec.s'' [in CoqFSetInterface]
WSfun.Spec.x [in CoqFSetInterface]
WSfun.Spec.y [in CoqFSetInterface]
Library Index
B
BindersBisimulation
C
CoqFSetDecideCoqFSetInterface
F
FSetExtraFSetWeakNotin
H
HoweHoweSound
L
LibDefaultSimpM
MyFsetS
SemanticsStruct_congr
Syntax
Axiom Index
S
Sdep.add [in CoqFSetInterface]Sdep.cardinal [in CoqFSetInterface]
Sdep.choose [in CoqFSetInterface]
Sdep.choose_equal [in CoqFSetInterface]
Sdep.compare [in CoqFSetInterface]
Sdep.diff [in CoqFSetInterface]
Sdep.elements [in CoqFSetInterface]
Sdep.empty [in CoqFSetInterface]
Sdep.equal [in CoqFSetInterface]
Sdep.eq_In [in CoqFSetInterface]
Sdep.eq_trans [in CoqFSetInterface]
Sdep.eq_sym [in CoqFSetInterface]
Sdep.eq_refl [in CoqFSetInterface]
Sdep.exists_ [in CoqFSetInterface]
Sdep.filter [in CoqFSetInterface]
Sdep.fold [in CoqFSetInterface]
Sdep.for_all [in CoqFSetInterface]
Sdep.In [in CoqFSetInterface]
Sdep.inter [in CoqFSetInterface]
Sdep.is_empty [in CoqFSetInterface]
Sdep.lt [in CoqFSetInterface]
Sdep.lt_not_eq [in CoqFSetInterface]
Sdep.lt_trans [in CoqFSetInterface]
Sdep.max_elt [in CoqFSetInterface]
Sdep.mem [in CoqFSetInterface]
Sdep.min_elt [in CoqFSetInterface]
Sdep.partition [in CoqFSetInterface]
Sdep.remove [in CoqFSetInterface]
Sdep.singleton [in CoqFSetInterface]
Sdep.subset [in CoqFSetInterface]
Sdep.t [in CoqFSetInterface]
Sdep.union [in CoqFSetInterface]
Sfun.choose_3 [in CoqFSetInterface]
Sfun.compare [in CoqFSetInterface]
Sfun.elements_3 [in CoqFSetInterface]
Sfun.lt [in CoqFSetInterface]
Sfun.lt_not_eq [in CoqFSetInterface]
Sfun.lt_trans [in CoqFSetInterface]
Sfun.max_elt_3 [in CoqFSetInterface]
Sfun.max_elt_2 [in CoqFSetInterface]
Sfun.max_elt_1 [in CoqFSetInterface]
Sfun.max_elt [in CoqFSetInterface]
Sfun.min_elt_3 [in CoqFSetInterface]
Sfun.min_elt_2 [in CoqFSetInterface]
Sfun.min_elt_1 [in CoqFSetInterface]
Sfun.min_elt [in CoqFSetInterface]
W
WSfun.add [in CoqFSetInterface]WSfun.add_3 [in CoqFSetInterface]
WSfun.add_2 [in CoqFSetInterface]
WSfun.add_1 [in CoqFSetInterface]
WSfun.cardinal [in CoqFSetInterface]
WSfun.cardinal_1 [in CoqFSetInterface]
WSfun.choose [in CoqFSetInterface]
WSfun.choose_2 [in CoqFSetInterface]
WSfun.choose_1 [in CoqFSetInterface]
WSfun.diff [in CoqFSetInterface]
WSfun.diff_3 [in CoqFSetInterface]
WSfun.diff_2 [in CoqFSetInterface]
WSfun.diff_1 [in CoqFSetInterface]
WSfun.elements [in CoqFSetInterface]
WSfun.elements_3w [in CoqFSetInterface]
WSfun.elements_2 [in CoqFSetInterface]
WSfun.elements_1 [in CoqFSetInterface]
WSfun.empty [in CoqFSetInterface]
WSfun.empty_1 [in CoqFSetInterface]
WSfun.equal [in CoqFSetInterface]
WSfun.equal_2 [in CoqFSetInterface]
WSfun.equal_1 [in CoqFSetInterface]
WSfun.eq_trans [in CoqFSetInterface]
WSfun.eq_sym [in CoqFSetInterface]
WSfun.eq_refl [in CoqFSetInterface]
WSfun.eq_dec [in CoqFSetInterface]
WSfun.exists_2 [in CoqFSetInterface]
WSfun.exists_1 [in CoqFSetInterface]
WSfun.exists_ [in CoqFSetInterface]
WSfun.filter [in CoqFSetInterface]
WSfun.filter_3 [in CoqFSetInterface]
WSfun.filter_2 [in CoqFSetInterface]
WSfun.filter_1 [in CoqFSetInterface]
WSfun.fold [in CoqFSetInterface]
WSfun.fold_1 [in CoqFSetInterface]
WSfun.for_all_2 [in CoqFSetInterface]
WSfun.for_all_1 [in CoqFSetInterface]
WSfun.for_all [in CoqFSetInterface]
WSfun.In [in CoqFSetInterface]
WSfun.inter [in CoqFSetInterface]
WSfun.inter_3 [in CoqFSetInterface]
WSfun.inter_2 [in CoqFSetInterface]
WSfun.inter_1 [in CoqFSetInterface]
WSfun.In_1 [in CoqFSetInterface]
WSfun.is_empty_2 [in CoqFSetInterface]
WSfun.is_empty_1 [in CoqFSetInterface]
WSfun.is_empty [in CoqFSetInterface]
WSfun.mem [in CoqFSetInterface]
WSfun.mem_2 [in CoqFSetInterface]
WSfun.mem_1 [in CoqFSetInterface]
WSfun.partition [in CoqFSetInterface]
WSfun.partition_2 [in CoqFSetInterface]
WSfun.partition_1 [in CoqFSetInterface]
WSfun.remove [in CoqFSetInterface]
WSfun.remove_3 [in CoqFSetInterface]
WSfun.remove_2 [in CoqFSetInterface]
WSfun.remove_1 [in CoqFSetInterface]
WSfun.singleton [in CoqFSetInterface]
WSfun.singleton_2 [in CoqFSetInterface]
WSfun.singleton_1 [in CoqFSetInterface]
WSfun.subset [in CoqFSetInterface]
WSfun.subset_2 [in CoqFSetInterface]
WSfun.subset_1 [in CoqFSetInterface]
WSfun.t [in CoqFSetInterface]
WSfun.union [in CoqFSetInterface]
WSfun.union_3 [in CoqFSetInterface]
WSfun.union_2 [in CoqFSetInterface]
WSfun.union_1 [in CoqFSetInterface]
Lemma Index
A
abs_to_proc [in HoweSound]amapN_parr [in Semantics]
amapN_parl [in Semantics]
amapN_new [in Semantics]
amapN_subset [in Semantics]
amapN_eq_on_fn [in Semantics]
amapN_id [in Semantics]
amapN_amapN [in Semantics]
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_eq_on_fv [in Bisimulation]
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
card_In [in Bisimulation]card_max [in Bisimulation]
clusterfuck [in Struct_congr]
compK_permutK_gt [in Binders]
compK_permutK_leb [in Binders]
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]
D
downfs_empty_rev [in Syntax]downfs_empty [in Syntax]
downfs_0_spec [in Syntax]
downfs_spec [in Syntax]
Down_finite [in Bisimulation]
Down_empty [in Bisimulation]
F
filter_union [in MyFset]filter_subset [in MyFset]
filter_id [in MyFset]
fn_subst [in Syntax]
fn_bind [in Syntax]
fn_bind' [in Syntax]
fn_mapN [in Syntax]
fn_mapV [in Syntax]
fn_parr [in Semantics]
fn_parl [in Semantics]
fn_appr_subset [in Semantics]
fn_C_par [in Semantics]
fn_appr_appl [in Semantics]
fn_agent_new [in Semantics]
fn_agent_amapN [in Semantics]
fn_genNu [in Semantics]
fresh_above_n [in Bisimulation]
fv_finite [in Bisimulation]
G
genNu_fold [in Semantics]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_genNu [in Howe]
howe_mapN [in Howe]
howe_oe [in Howe]
howe_refl [in Howe]
howe_implies_howe' [in Howe]
howe'_mapN [in Howe]
howe'_implies_howe [in Howe]
howe'_ind_size [in Howe]
I
id_bisim_bisim [in Bisimulation]injective_cardinal [in Bisimulation]
invert_f_subs [in Bisimulation]
invert_f_proc [in Bisimulation]
L
late_implies_sim [in Bisimulation]liftN_preserves_injectivity [in Binders]
liftN_0 [in Binders]
liftN_liftN [in Binders]
liftN_S [in Binders]
lts_fn [in Semantics]
lts_conc_wf [in Semantics]
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_mapN [in Syntax]mapN_id' [in Syntax]
mapN_id [in Syntax]
mapN_lts_rev [in Semantics]
mapN_lts [in Semantics]
mapN_appr [in Semantics]
mapN_appl [in Semantics]
mapN_eq_on_fn_rev [in Semantics]
mapN_eq_on_fn [in Semantics]
mapN_concwf [in Semantics]
mapN_genNu [in Semantics]
mapV_mapN [in Syntax]
mapV_mapV [in Syntax]
mapV_id [in Syntax]
map_inter [in MyFset]
map_eq [in MyFset]
map_subset [in MyFset]
map_union [in MyFset]
map_singleton [in MyFset]
map_empty [in MyFset]
map_id [in MyFset]
map_spec [in MyFset]
max_elt_spec_empty [in MyFset]
max_elt_spec [in MyFset]
max_In_S [in Bisimulation]
N
Notin_fun.test_solve_notin_7 [in FSetWeakNotin]Notin_fun.test_solve_notin_6 [in FSetWeakNotin]
Notin_fun.test_solve_notin_5 [in FSetWeakNotin]
Notin_fun.test_solve_notin_4 [in FSetWeakNotin]
Notin_fun.test_solve_notin_3 [in FSetWeakNotin]
Notin_fun.test_solve_notin_2 [in FSetWeakNotin]
Notin_fun.test_solve_notin_1 [in FSetWeakNotin]
Notin_fun.notin_diff_3 [in FSetWeakNotin]
Notin_fun.notin_diff_2 [in FSetWeakNotin]
Notin_fun.notin_diff_1 [in FSetWeakNotin]
Notin_fun.notin_inter_3 [in FSetWeakNotin]
Notin_fun.notin_inter_2 [in FSetWeakNotin]
Notin_fun.notin_inter_1 [in FSetWeakNotin]
Notin_fun.notin_union_3 [in FSetWeakNotin]
Notin_fun.notin_union_2 [in FSetWeakNotin]
Notin_fun.notin_union_1 [in FSetWeakNotin]
Notin_fun.notin_remove_3' [in FSetWeakNotin]
Notin_fun.notin_remove_3 [in FSetWeakNotin]
Notin_fun.notin_remove_2 [in FSetWeakNotin]
Notin_fun.notin_remove_1 [in FSetWeakNotin]
Notin_fun.notin_singleton_2 [in FSetWeakNotin]
Notin_fun.notin_singleton_1' [in FSetWeakNotin]
Notin_fun.notin_singleton_1 [in FSetWeakNotin]
Notin_fun.notin_add_3 [in FSetWeakNotin]
Notin_fun.notin_add_2 [in FSetWeakNotin]
Notin_fun.notin_add_1' [in FSetWeakNotin]
Notin_fun.notin_add_1 [in FSetWeakNotin]
Notin_fun.notin_empty_1 [in FSetWeakNotin]
nu_nu_conc [in Struct_congr]
nu_genNu [in Semantics]
O
oe_sc0 [in Struct_congr]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]
P
permut_shiftN [in Syntax]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
renaming [in Bisimulation]renaming_subs [in Bisimulation]
renaming_proc [in Bisimulation]
renaming_sets [in Bisimulation]
restricted_fn [in Bisimulation]
Rincl_sc0_howe [in HoweSound]
S
sc_nu_nu_permut [in Struct_congr]sc_nuK_permut1 [in Struct_congr]
sc_nuK_compL_permutK [in Struct_congr]
sc_appl_appr [in Struct_congr]
sc_appr_appl [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_genNu [in Struct_congr]
sc_symmetric [in Struct_congr]
sc_refl [in Struct_congr]
set_lift [in Bisimulation]
shiftN_injective [in Binders]
shiftN_mapN [in Semantics]
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]
struct_congr_bisim [in Struct_congr]
struct_congr_sim [in Struct_congr]
struct_congr_sim' [in Struct_congr]
subset_trans [in MyFset]
subst_shift [in Syntax]
subst_mapN [in Syntax]
T
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]
W
WDecide_fun.FSetDecideTestCases.test_sweirich [in CoqFSetDecide]WDecide_fun.FSetDecideTestCases.test_baydemir_4 [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir_3 [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir_2 [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_baydemir [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.function_test_2 [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.function_test_1 [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_too_complex [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.eq_chain_test [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_set_ops_1 [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_iff_conj [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_not_In_conj [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_not_In_disj [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_disjunction [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_Subset_add_remove [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_add_In [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_In_singleton [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_neq_trans_2 [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_neq_trans_1 [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_trans_2 [in CoqFSetDecide]
WDecide_fun.FSetDecideTestCases.test_eq_trans_1 [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.dec_eq [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.dec_In [in CoqFSetDecide]
WDecide_fun.FSetLogicalFacts.test_pull [in CoqFSetDecide]
WDecide_fun.FSetLogicalFacts.test_push [in CoqFSetDecide]
Constructor Index
A
abs_def [in Semantics]ag_conc [in Semantics]
ag_abs [in Semantics]
ag_proc [in Semantics]
C
conc_def [in Semantics]D
Down_def [in Bisimulation]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
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]
st_conc [in Bisimulation]
st_abs [in Bisimulation]
st_proc [in Bisimulation]
T
tau [in Semantics]V
VS [in Binders]VZ [in Binders]
W
WDecide_fun.FSetDecideAuxiliary.Equal_FSet_Prop [in CoqFSetDecide]WDecide_fun.FSetDecideAuxiliary.Subset_FSet_Prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.Empty_FSet_Prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.elt_FSet_Prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.not_elt_prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.impl_elt_prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.disj_elt_prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.conj_elt_prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.False_elt_prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.True_elt_prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.In_elt_prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.eq_elt_prop [in CoqFSetDecide]
WDecide_fun.FSetDecideAuxiliary.eq_Prop [in CoqFSetDecide]
Inductive Index
A
abs [in Semantics]agent [in Semantics]
C
conc [in Semantics]D
Down [in Bisimulation]H
howe [in Howe]howe' [in Howe]
I
incV [in Binders]L
label [in Semantics]lts [in Semantics]
P
proc [in Syntax]R
rel_renamed [in Bisimulation]S
sim_test [in Bisimulation]struct_congr [in Struct_congr]
W
WDecide_fun.FSetDecideAuxiliary.FSet_Prop [in CoqFSetDecide]WDecide_fun.FSetDecideAuxiliary.FSet_elt_Prop [in CoqFSetDecide]
Section Index
N
Notin_fun.Lemmas [in FSetWeakNotin]S
Sfun.Spec [in CoqFSetInterface]W
WSfun.Spec [in CoqFSetInterface]WSfun.Spec.Filter [in CoqFSetInterface]
Abbreviation Index
A
add [in MyFset]C
cardinal [in MyFset]D
diff [in MyFset]E
empty [in MyFset]F
filter [in MyFset]I
indices [in MyFset]inter [in MyFset]
L
lpseudo_sim [in HoweSound]M
max_elt [in MyFset]P
PO [in Syntax]proc0 [in Syntax]
proc1 [in Syntax]
pseudo_sim [in HoweSound]
R
remove [in MyFset]Rincl [in Bisimulation]
S
sc0 [in Struct_congr]shiftN [in Syntax]
shiftV [in Syntax]
shiftV1 [in Syntax]
singleton [in MyFset]
subst [in Syntax]
T
test_conc [in Bisimulation]test_abs [in Bisimulation]
test_proc [in Bisimulation]
U
union [in MyFset]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]
C
cmapN [in Semantics]comp [in Binders]
comp_rel [in Bisimulation]
conc_new [in Semantics]
conc_parr [in Semantics]
conc_parl [in Semantics]
conc_wf [in Semantics]
D
down [in Semantics]downfs [in Syntax]
downV [in Bisimulation]
down_lab [in Semantics]
F
fmapN [in Semantics]fn [in Syntax]
fn_agent [in Semantics]
fn_lab [in Semantics]
fshiftN [in Semantics]
fv [in Bisimulation]
G
genNu [in Semantics]I
id_bisim [in Bisimulation]incV_map [in Binders]
L
liftN [in Binders]liftV [in Syntax]
lmapN [in Semantics]
M
make_In [in Bisimulation]Make.disjoint [in FSetExtra]
Make.fresh_list [in FSetExtra]
Make.notin [in FSetExtra]
map [in MyFset]
mapN [in Syntax]
mapV [in Syntax]
N
name [in Binders]new [in Semantics]
O
open_extension [in Bisimulation]P
parl [in Semantics]parr [in Semantics]
permut [in Binders]
R
rename_compatible [in Bisimulation]S
Sdep.Add [in CoqFSetInterface]Sdep.elt [in CoqFSetInterface]
Sdep.Empty [in CoqFSetInterface]
Sdep.eq [in CoqFSetInterface]
Sdep.Equal [in CoqFSetInterface]
Sdep.Exists [in CoqFSetInterface]
Sdep.For_all [in CoqFSetInterface]
Sdep.Subset [in CoqFSetInterface]
Sfun.disjoint [in FSetExtra]
Sfun.fresh_list [in FSetExtra]
Sfun.notin [in FSetExtra]
simulation [in Bisimulation]
simulation_up_to_sc [in Struct_congr]
simulation_late [in Bisimulation]
subst_func [in Syntax]
s_restr [in Bisimulation]
W
WSfun.elt [in CoqFSetInterface]WSfun.Empty [in CoqFSetInterface]
WSfun.eq [in CoqFSetInterface]
WSfun.Equal [in CoqFSetInterface]
WSfun.Exists [in CoqFSetInterface]
WSfun.For_all [in CoqFSetInterface]
WSfun.Subset [in CoqFSetInterface]
| 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 | (608 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 | (17 entries) |
| Module Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (24 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 | (15 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 | (13 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 | (114 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 | (236 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 | (74 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) |
| 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 | (4 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 | (25 entries) |
| Definition Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (71 entries) |
This page has been generated by coqdoc