| 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 | (1094 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 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 | (488 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 | (2 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 | (85 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 | (120 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 | (60 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 | (279 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 | (11 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 | (3 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 | (7 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (30 entries) |
Global Index
A
act [definition, in act]action [inductive, in action]
Action [constructor, in Action]
Actions [projection, in Actions]
actions [definition, in actions]
acts [definition, in acts]
adding_binding_unaffect_bindings [lemma, in adding_binding_unaffect_bindings]
adding_comp_unaffect_bindings [lemma, in adding_comp_unaffect_bindings]
adding_interface_keeps_components_ids_unique [lemma, in adding_interface_keeps_components_ids_unique]
adding_comp_keeps_bindings_well_formed [lemma, in adding_comp_keeps_bindings_well_formed]
adding_interface_keeps_bindings_well_formed [lemma, in adding_interface_keeps_bindings_well_formed]
adding_interface_maintains_component_id [lemma, in adding_interface_maintains_component_id]
adding_binding_auxiliary [lemma, in adding_binding_auxiliary]
adding_3_lights [lemma, in adding_3_lights]
adding_comp_maintains_valid_bindings [lemma, in adding_comp_maintains_valid_bindings]
adding_interface_unaffect_bindings [lemma, in adding_interface_unaffect_bindings]
add_binding_fact [lemma, in add_binding_fact]
add_binding [definition, in add_binding]
add_interface_may_entail_false [lemma, in add_interface_may_entail_false]
add_binding_fact_nil_comps [lemma, in add_binding_fact_nil_comps]
add_3_lights [lemma, in add_3_lights]
add_comp_may_entail_false [lemma, in add_comp_may_entail_false]
add_interface [definition, in add_interface]
AllEmpty [constructor, in AllEmpty]
allowed_actions_from_sv_elements_coffee_fact [lemma, in allowed_actions_from_sv_elements_coffee_fact]
allowed_actions_from_q1q1_coffee [inductive, in allowed_actions_from_q1q1_coffee]
allowed_actions_from_q1q1_sandwich_fact [lemma, in allowed_actions_from_q1q1_sandwich_fact]
AllStep [constructor, in AllStep]
all_the_same_fact [lemma, in all_the_same_fact]
all_the_same [inductive, in all_the_same]
alter [definition, in alter]
alter2 [definition, in alter2]
Always [inductive, in Always]
Always_LCons [constructor, in Always_LCons]
always_a [lemma, in always_a]
Always_Infinite [lemma, in Always_Infinite]
annotation_example [definition, in annotation_example]
AnotherSimpleArchitecture [definition, in AnotherSimpleArchitecture]
AnotherSimpleArchitecture' [definition, in AnotherSimpleArchitecture']
appending_binding_keeps_component_well_formed [lemma, in appending_binding_keeps_component_well_formed]
appending_interface_keeps_bindings_well_formed [lemma, in appending_interface_keeps_bindings_well_formed]
app_str_yield_different_str [lemma, in app_str_yield_different_str]
Arch_is_Sound [definition, in Arch_is_Sound]
Arch_is_Sound_After_Removal' [definition, in Arch_is_Sound_After_Removal']
Arch_is_Sound' [definition, in Arch_is_Sound']
Arch_is_Sound_After_Removal [definition, in Arch_is_Sound_After_Removal]
ArrayList [record, in ArrayList]
arraylist_length [projection, in arraylist_length]
ascii_eq_reflection [lemma, in ascii_eq_reflection]
asgns [definition, in asgns]
Assignment [constructor, in Assignment]
assignment [inductive, in assignment]
assignments [definition, in assignments]
AssignmentVar [constructor, in AssignmentVar]
Atomic [inductive, in Atomic]
Atomic_intro [constructor, in Atomic_intro]
attainable [inductive, in attainable]
AttainN [constructor, in AttainN]
Attain0 [constructor, in Attain0]
AutonomicUseCase [library]
awesome_definition [inductive, in awesome_definition]
B
Base [library]Batteries [library]
beq_string_reflection [lemma, in beq_string_reflection]
beq_comp_id_fact [lemma, in beq_comp_id_fact]
beq_opt_comp [definition, in beq_opt_comp]
beq_visibility_symmetry [lemma, in beq_visibility_symmetry]
beq_ident_symmetry' [lemma, in beq_ident_symmetry']
beq_bool_refl [lemma, in beq_bool_refl]
beq_comp [definition, in beq_comp]
beq_ident_symmetry [lemma, in beq_ident_symmetry]
beq_string_reflection_in_prop [lemma, in beq_string_reflection_in_prop]
beq_string_reflection_in_bool [lemma, in beq_string_reflection_in_bool]
beq_component [definition, in beq_component]
beq_message [definition, in beq_message]
beq_signature [definition, in beq_signature]
beq_acc_fact [lemma, in beq_acc_fact]
beq_visibility_reflexivity [lemma, in beq_visibility_reflexivity]
binding [inductive, in binding]
Binding [library]
BindingExists_Step [constructor, in BindingExists_Step]
BindingExists_Root [constructor, in BindingExists_Root]
bindings_still_valid_removing_unbinded_component [lemma, in bindings_still_valid_removing_unbinded_component]
bindings_lookup_fact [lemma, in bindings_lookup_fact]
bindings_unaffected [lemma, in bindings_unaffected]
binding_type_dec [axiom, in binding_type_dec]
binding_exists [definition, in binding_exists]
binding_is_not_a_duplicate [definition, in binding_is_not_a_duplicate]
binding_eq_reflection [lemma, in binding_eq_reflection]
binding_exists' [inductive, in binding_exists']
binding_equality_bool2Prop [lemma, in binding_equality_bool2Prop]
binding_dec [lemma, in binding_dec]
binding_is_not_a_duplicate_bool_correctness [lemma, in binding_is_not_a_duplicate_bool_correctness]
binding_equality_Prop2bool [lemma, in binding_equality_Prop2bool]
binding_cannot_be_crossing_if_valid [lemma, in binding_cannot_be_crossing_if_valid]
binding_exists_correctness [lemma, in binding_exists_correctness]
bind_system [definition, in bind_system]
bisimilar [inductive, in bisimilar]
bisimilar_LNth [lemma, in bisimilar_LNth]
bisimilar_sym [lemma, in bisimilar_sym]
bisimilar_trans [lemma, in bisimilar_trans]
bisimilar_of_Finite_is_eq [lemma, in bisimilar_of_Finite_is_eq]
bisimilar_inv_1 [lemma, in bisimilar_inv_1]
bisimilar_inv_2 [lemma, in bisimilar_inv_2]
bisimilar_refl [lemma, in bisimilar_refl]
bisimilar_of_Finite_is_Finite [lemma, in bisimilar_of_Finite_is_Finite]
bisimilar_of_Infinite_is_Infinite [lemma, in bisimilar_of_Infinite_is_Infinite]
bisimilar_equiv [lemma, in bisimilar_equiv]
bisimulation [definition, in bisimulation]
bisim0 [constructor, in bisim0]
bisim1 [constructor, in bisim1]
ble_nat_reflection [lemma, in ble_nat_reflection]
bneq_ident [definition, in bneq_ident]
bneq_false_entails_beq_true [lemma, in bneq_false_entails_beq_true]
bneq_true_entails_beq_false [lemma, in bneq_true_entails_beq_false]
body [definition, in body]
body_transitions [definition, in body_transitions]
body_init [definition, in body_init]
body_states [definition, in body_states]
body_actions [definition, in body_actions]
body_mem [definition, in body_mem]
boolean_function_fact [lemma, in boolean_function_fact]
bool_dec_fact [lemma, in bool_dec_fact]
bool_conjunction_acc [lemma, in bool_conjunction_acc]
bool_dec [definition, in bool_dec]
bool_symmetry_fact [lemma, in bool_symmetry_fact]
bool_conjunction_fact [lemma, in bool_conjunction_fact]
bool_conjunction_fact' [lemma, in bool_conjunction_fact']
bool_fact [lemma, in bool_fact]
BrightComp [definition, in BrightComp]
BRINFOCOLL [definition, in BRINFOCOLL]
build_state_fact' [lemma, in build_state_fact']
build_state_fact [lemma, in build_state_fact]
build_state_reduction_fact [lemma, in build_state_reduction_fact]
build_running_example [definition, in build_running_example]
build_state_soundness [lemma, in build_state_soundness]
build_state_correctness [lemma, in build_state_correctness]
build_state_completeness [lemma, in build_state_completeness]
build_C [definition, in build_C]
build_N [definition, in build_N]
build_S [definition, in build_S]
b1 [definition, in b1]
b2 [definition, in b2]
b3 [definition, in b3]
b4 [definition, in b4]
b5 [definition, in b5]
b6 [definition, in b6]
b7 [definition, in b7]
C
C [definition, in C]cardinality [inductive, in cardinality]
CardinalityDecidability [library]
cardinality_eq_reflection [lemma, in cardinality_eq_reflection]
CEMI_Bound [constructor, in CEMI_Bound]
check_if_recipients_are_mandatory'_fact [lemma, in check_if_recipients_are_mandatory'_fact]
check_if_recipients_are_mandatory_fact [lemma, in check_if_recipients_are_mandatory_fact]
check_if_recipients_are_mandatory_spec [lemma, in check_if_recipients_are_mandatory_spec]
check_if_mandatory_fact' [lemma, in check_if_mandatory_fact']
check_if_singleton_requirement_is_met_fact [lemma, in check_if_singleton_requirement_is_met_fact]
check_if_mandatory_fact [lemma, in check_if_mandatory_fact]
check_if_singleton_requirement_is_met_fact' [lemma, in check_if_singleton_requirement_is_met_fact']
CIMI_Bound [constructor, in CIMI_Bound]
cim_itfs_bound_correctness [definition, in cim_itfs_bound_correctness]
Client [constructor, in Client]
client_singleton_are_bound_once_at_most [definition, in client_singleton_are_bound_once_at_most]
client_internal_mandatory_interfaces_are_bound [inductive, in client_internal_mandatory_interfaces_are_bound]
client_singleton_are_bound_once_at_most_normal_import_bindings [inductive, in client_singleton_are_bound_once_at_most_normal_import_bindings]
client_internal_mandatory_interfaces_are_bound_bool_one_rev_spec [lemma, in client_internal_mandatory_interfaces_are_bound_bool_one_rev_spec]
client_singleton_are_bound_once_at_most_export_bindings_bool [definition, in client_singleton_are_bound_once_at_most_export_bindings_bool]
client_internal_mandatory_itfs_are_bound [definition, in client_internal_mandatory_itfs_are_bound]
client_singleton_are_bound_once_at_most_normal_import_bindings_bool_fact [lemma, in client_singleton_are_bound_once_at_most_normal_import_bindings_bool_fact]
client_singleton_are_bound_once_at_most_export_bindings [inductive, in client_singleton_are_bound_once_at_most_export_bindings]
client_singleton_are_bound_once_at_most_normal_import_bindings_bool [definition, in client_singleton_are_bound_once_at_most_normal_import_bindings_bool]
client_internal_mandatory_interfaces_are_bound_bool_one_rev_spec_proof_nr_2 [lemma, in client_internal_mandatory_interfaces_are_bound_bool_one_rev_spec_proof_nr_2]
client_singleton_are_bound_once_at_most_export_bindings_bool_one_fact [lemma, in client_singleton_are_bound_once_at_most_export_bindings_bool_one_fact]
client_internal_mandatory_interfaces_are_bound_bool [definition, in client_internal_mandatory_interfaces_are_bound_bool]
client_singleton_are_bound_once_at_most_normal_import_bindings_bool_one_rev_spec' [lemma, in client_singleton_are_bound_once_at_most_normal_import_bindings_bool_one_rev_spec']
client_singleton_are_bound_once_at_most_normal_import_bindings_bool_one_rev_spec [lemma, in client_singleton_are_bound_once_at_most_normal_import_bindings_bool_one_rev_spec]
client_internal_mandatory_interfaces_are_bound_bool_one_spec [lemma, in client_internal_mandatory_interfaces_are_bound_bool_one_spec]
client_singleton_are_bound_once_at_most_export_bindings_bool_fact [lemma, in client_singleton_are_bound_once_at_most_export_bindings_bool_fact]
client_internal_mandatory_interfaces_are_bound_bool_fact [lemma, in client_internal_mandatory_interfaces_are_bound_bool_fact]
client_internal_mandatory_itfs_are_bound_bool [definition, in client_internal_mandatory_itfs_are_bound_bool]
CoffeeN [constructor, in CoffeeN]
Coffee0 [constructor, in Coffee0]
CoInductionLib [library]
Collection [constructor, in Collection]
combineN_coffee_orders_fact [lemma, in combineN_coffee_orders_fact]
communication_type [inductive, in communication_type]
Compliance [library]
component [inductive, in component]
Component [constructor, in Component]
Component [library]
component_dec [lemma, in component_dec]
component_is_not_connected' [inductive, in component_is_not_connected']
component_eq_dec [definition, in component_eq_dec]
component_is_not_connected_bool_soundness [lemma, in component_is_not_connected_bool_soundness]
component_query_fact [lemma, in component_query_fact]
component_is_not_connected [definition, in component_is_not_connected]
component_is_not_connected_bool_completeness [lemma, in component_is_not_connected_bool_completeness]
Composite [definition, in Composite]
CompositePath [definition, in CompositePath]
Configuration [constructor, in Configuration]
Constructor1 [constructor, in Constructor1]
Constructor2 [constructor, in Constructor2]
cons_eqServerSingleton [lemma, in cons_eqServerSingleton]
cons_eqSingleton_export [lemma, in cons_eqSingleton_export]
cons_eq [lemma, in cons_eq]
cons_eqType [lemma, in cons_eqType]
cons_eqSingleton_normal_import [lemma, in cons_eqSingleton_normal_import]
cons_eqType' [lemma, in cons_eqType']
contents [projection, in contents]
contingency [inductive, in contingency]
ContingencyDecidability [library]
contingency_eq_reflection [lemma, in contingency_eq_reflection]
Control [constructor, in Control]
controlLevel [inductive, in controlLevel]
controlLevel_eq_reflection [lemma, in controlLevel_eq_reflection]
controlLevel_dec [lemma, in controlLevel_dec]
controlLevel_equality_bool2Prop [lemma, in controlLevel_equality_bool2Prop]
control_level_dec [lemma, in control_level_dec]
CoreElementsFacts [library]
cpath [definition, in cpath]
CrossBinding_Base [constructor, in CrossBinding_Base]
CrossBinding_Step [constructor, in CrossBinding_Step]
cross_binding_cannot_happen [lemma, in cross_binding_cannot_happen]
cross_normal [definition, in cross_normal]
cross_binding' [inductive, in cross_binding']
cross_export [definition, in cross_export]
cross_binding [definition, in cross_binding]
cross_import [definition, in cross_import]
C_is_well_formed [lemma, in C_is_well_formed]
D
dec [definition, in dec]dec_unique_ids_correctness [lemma, in dec_unique_ids_correctness]
dec_component [definition, in dec_component]
dec_state [definition, in dec_state]
dec_interfaces_correctness [lemma, in dec_interfaces_correctness]
dec_state_correctness [lemma, in dec_state_correctness]
dec_component_correctness [lemma, in dec_component_correctness]
dec_bindings_correctness [lemma, in dec_bindings_correctness]
default_class [definition, in default_class]
digit_of_nat [definition, in digit_of_nat]
Done [constructor, in Done]
done_is_quiet [lemma, in done_is_quiet]
done_is_quiet' [lemma, in done_is_quiet']
E
element_type [projection, in element_type]element_in_removed_set_is_in_original [lemma, in element_in_removed_set_is_in_original]
Emit [constructor, in Emit]
empty_state_is_well_formed [lemma, in empty_state_is_well_formed]
empty_components_entail_no_bindings [lemma, in empty_components_entail_no_bindings]
empty_state [definition, in empty_state]
eq [definition, in eq]
eqServerSingleton [definition, in eqServerSingleton]
eqServerSingleton_correctness [lemma, in eqServerSingleton_correctness]
eqSingleton_normal_import_correctness [lemma, in eqSingleton_normal_import_correctness]
eqSingleton_export [definition, in eqSingleton_export]
eqSingleton_normal_import [definition, in eqSingleton_normal_import]
eqSingleton_export_correctness [lemma, in eqSingleton_export_correctness]
eqType [definition, in eqType]
eqType_correctness [lemma, in eqType_correctness]
eqType' [definition, in eqType']
eqType'_correctness [lemma, in eqType'_correctness]
eq_action [definition, in eq_action]
ErrorIdent [definition, in ErrorIdent]
errorState_means_stuck_reduction [lemma, in errorState_means_stuck_reduction]
errorState_means_stuck_reduction' [lemma, in errorState_means_stuck_reduction']
eval [definition, in eval]
Eval [library]
eval_reduction_fact [lemma, in eval_reduction_fact]
Eventually [inductive, in Eventually]
Eventually_further [constructor, in Eventually_further]
Eventually_of_LAppend [lemma, in Eventually_of_LAppend]
Eventually_here [constructor, in Eventually_here]
Examples [library]
execute_computes_the_semantics [lemma, in execute_computes_the_semantics]
Export [constructor, in Export]
External [constructor, in External]
ext_client_mand_mapping_fact [lemma, in ext_client_mand_mapping_fact]
ext_client_mand_mapping [inductive, in ext_client_mand_mapping]
F
final [lemma, in final]Finite [inductive, in Finite]
Finite_LNil [constructor, in Finite_LNil]
Finite_not_Infinite [lemma, in Finite_not_Infinite]
Finite_of_LCons [lemma, in Finite_of_LCons]
Finite_LCons [constructor, in Finite_LCons]
first_well_typedness_proof [lemma, in first_well_typedness_proof]
first_well_formedness_proof [lemma, in first_well_formedness_proof]
fold_left2 [definition, in fold_left2]
forever [definition, in forever]
forever_infinite [lemma, in forever_infinite]
forever_unfold [lemma, in forever_unfold]
from [definition, in from]
from_q1q1_target_states [lemma, in from_q1q1_target_states]
from_q1q1_target_states_interleaving' [lemma, in from_q1q1_target_states_interleaving']
from_unfold [lemma, in from_unfold]
from_Infinite_V0 [lemma, in from_Infinite_V0]
from_q0q0_target_states_interleaving' [lemma, in from_q0q0_target_states_interleaving']
from_q0q0_target_states [lemma, in from_q0q0_target_states]
from_Infinite [lemma, in from_Infinite]
from_q0q0_target_states_interleaving [lemma, in from_q0q0_target_states_interleaving]
from_q1q1_target_states_interleaving [lemma, in from_q1q1_target_states_interleaving]
Functional [constructor, in Functional]
functionality [inductive, in functionality]
functionality_eq_reflection [lemma, in functionality_eq_reflection]
FunctionalSpec [library]
F_Infinite [definition, in F_Infinite]
F_Infinite_2_Eventually [definition, in F_Infinite_2_Eventually]
F_Infinite_cons [lemma, in F_Infinite_cons]
F_from [definition, in F_from]
f_aux [definition, in f_aux]
F_Infinite_consR [lemma, in F_Infinite_consR]
G
Gathercast [constructor, in Gathercast]GCMExample [library]
GCMSpec [library]
GCMTyping [library]
GCMWellFormedness [library]
gcm_component [definition, in gcm_component]
general_omega [definition, in general_omega]
general_omega_LNil [lemma, in general_omega_LNil]
general_omega_LNil_LCons [lemma, in general_omega_LNil_LCons]
general_omega_LCons [lemma, in general_omega_LCons]
general_omega_lappend [lemma, in general_omega_lappend]
general_omega_infinite [lemma, in general_omega_infinite]
general_omega_shoots_again [lemma, in general_omega_shoots_again]
general_omega_of_Finite [lemma, in general_omega_of_Finite]
generate_0 [lemma, in generate_0]
generate_1 [lemma, in generate_1]
generate_from_template_fact [lemma, in generate_from_template_fact]
generate_n_states_len [lemma, in generate_n_states_len]
generate_from_template_spec [lemma, in generate_from_template_spec]
generation_has_unique_ids [lemma, in generation_has_unique_ids]
get_parent_eq [lemma, in get_parent_eq]
get_parent_step [lemma, in get_parent_step]
get_binding_server_id [definition, in get_binding_server_id]
get_normal_binding_recipients_fact [lemma, in get_normal_binding_recipients_fact]
get_normal_binding_recipients_aux2_trivial_fact [lemma, in get_normal_binding_recipients_aux2_trivial_fact]
get_subComponent [definition, in get_subComponent]
get_export_bindings_not_nil [lemma, in get_export_bindings_not_nil]
get_normal_import_bindings_fact [lemma, in get_normal_import_bindings_fact]
get_component_fact' [lemma, in get_component_fact']
get_interfaces_vis_role_cont_fact [lemma, in get_interfaces_vis_role_cont_fact]
get_component_commutes_on_l [lemma, in get_component_commutes_on_l]
get_component_path_eq [lemma, in get_component_path_eq]
get_component_fact'' [lemma, in get_component_fact'']
get_component_on_empty_components_entails_false [lemma, in get_component_on_empty_components_entails_false]
get_component_fact_same_interfaces' [lemma, in get_component_fact_same_interfaces']
get_component_fact [lemma, in get_component_fact]
get_interface_fact_id [lemma, in get_interface_fact_id]
get_binding_client_id [definition, in get_binding_client_id]
get_interface_fact_acc [lemma, in get_interface_fact_acc]
get_interface_fact [lemma, in get_interface_fact]
get_component_correct [lemma, in get_component_correct]
get_interfaces_vis_role_cont_spec [lemma, in get_interfaces_vis_role_cont_spec]
get_component_fact_same_interfaces [lemma, in get_component_fact_same_interfaces]
get_component_with_path [definition, in get_component_with_path]
get_component_with_path_dec [lemma, in get_component_with_path_dec]
get_left_most_fact1 [lemma, in get_left_most_fact1]
get_left_most_fact2 [lemma, in get_left_most_fact2]
get_parent [definition, in get_parent]
get_interface_post [lemma, in get_interface_post]
get_comp_fact [lemma, in get_comp_fact]
get_interface_membership_fact [lemma, in get_interface_membership_fact]
get_component_dec [lemma, in get_component_dec]
GlobalAction [constructor, in GlobalAction]
G_Infinite [definition, in G_Infinite]
H
HeavyLifting [library]I
iclC [axiom, in iclC]iclS [axiom, in iclS]
Ident [constructor, in Ident]
ident [inductive, in ident]
IdentDefinitionExample [module, in IdentDefinitionExample]
IdentDefinitionExample.BarVariable [definition, in BarVariable]
IdentDefinitionExample.FooVariable [definition, in FooVariable]
IdentDefinitionExample.XyzVariable [definition, in XyzVariable]
IdentProofExamples [module, in IdentProofExamples]
IdentProofExamples.warm_up_proof' [definition, in warm_up_proof']
IdentProofExamples.warm_up_proof [definition, in warm_up_proof]
IdentProofExamples.x [definition, in x]
IdentProofExamples.y [definition, in y]
ident_equality_Prop2bool [lemma, in ident_equality_Prop2bool]
ident_equality_bool2Prop' [lemma, in ident_equality_bool2Prop']
ident_dec [lemma, in ident_dec]
ident_equality_Prop2bool' [lemma, in ident_equality_Prop2bool']
ident_equality_bool2Prop [lemma, in ident_equality_bool2Prop]
ident_eq_reflection [lemma, in ident_eq_reflection]
ids_unicity_kept_removing_component [lemma, in ids_unicity_kept_removing_component]
IMn [constructor, in IMn]
implementationClass [definition, in implementationClass]
implementationClass_eq_reflection [lemma, in implementationClass_eq_reflection]
implementationClass_dec [lemma, in implementationClass_dec]
Import [constructor, in Import]
IM0 [constructor, in IM0]
indexed_membership [inductive, in indexed_membership]
induction_example [definition, in induction_example]
Infinite [inductive, in Infinite]
Infinite_ready_interleaving [lemma, in Infinite_ready_interleaving]
Infinite_act [lemma, in Infinite_act]
Infinite_of_LCons [lemma, in Infinite_of_LCons]
Infinite_not_Finite [lemma, in Infinite_not_Finite]
Infinite_LCons [constructor, in Infinite_LCons]
Infinite_act' [lemma, in Infinite_act']
Init [projection, in Init]
init_net_state [definition, in init_net_state]
inner_symmetry [lemma, in inner_symmetry]
InstantiatedExample [module, in InstantiatedExample]
InstantiatedExample.Infinite_ready_interleaving [lemma, in Infinite_ready_interleaving]
interelaving_test' [definition, in interelaving_test']
interelaving_test [definition, in interelaving_test]
interface [inductive, in interface]
Interface [constructor, in Interface]
Interface [library]
interfaces_BRINFOCOLL [definition, in interfaces_BRINFOCOLL]
interfaces_fact [lemma, in interfaces_fact]
interfaces_LightControlComp [definition, in interfaces_LightControlComp]
interfaces_are_well_formed [lemma, in interfaces_are_well_formed]
interfaces_in_example_are_bound [definition, in interfaces_in_example_are_bound]
interfaces_are_the_same [lemma, in interfaces_are_the_same]
interfaces_SwonLights [definition, in interfaces_SwonLights]
interfaces_dec [lemma, in interfaces_dec]
interfaces_LightComp [definition, in interfaces_LightComp]
interfaces_LCC [definition, in interfaces_LCC]
interfaces_BrightComp [definition, in interfaces_BrightComp]
interfaces_SensedBrInfo [definition, in interfaces_SensedBrInfo]
interface_dec [lemma, in interface_dec]
interface_dec [lemma, in interface_dec]
interface_eq_reflection [lemma, in interface_eq_reflection]
interleaving [inductive, in interleaving]
InterleavingOne [constructor, in InterleavingOne]
InterleavingTwo [constructor, in InterleavingTwo]
Internal [constructor, in Internal]
internal_or_external [lemma, in internal_or_external]
Introspection [constructor, in Introspection]
in_app_cons_fact [lemma, in in_app_cons_fact]
in_entailment [lemma, in in_entailment]
in_get_component_fact [lemma, in in_get_component_fact]
isEmpty [definition, in isEmpty]
IsNF [constructor, in IsNF]
IsSeq [constructor, in IsSeq]
isServerExternalSingleton [definition, in isServerExternalSingleton]
isServerInternalSingleton [definition, in isServerInternalSingleton]
is_normal_form [definition, in is_normal_form]
is_seq [definition, in is_seq]
is_one_step_from_normal_form [definition, in is_one_step_from_normal_form]
J
jmx [definition, in jmx]jmx_actions [definition, in jmx_actions]
jmx_states [definition, in jmx_states]
jmx_transitions [definition, in jmx_transitions]
jmx_init [definition, in jmx_init]
L
LAppend [definition, in LAppend]LAppend_of_Finite [lemma, in LAppend_of_Finite]
LAppend_G_Infinite [lemma, in LAppend_G_Infinite]
LAppend_assoc [lemma, in LAppend_assoc]
LAppend_of_Infinite_eq [lemma, in LAppend_of_Infinite_eq]
LAppend_LNil [lemma, in LAppend_LNil]
LAppend_LCons [lemma, in LAppend_LCons]
LAppend_G_Infinite_R [lemma, in LAppend_G_Infinite_R]
LAppend_of_Infinite [lemma, in LAppend_of_Infinite]
LCC [definition, in LCC]
LCons [constructor, in LCons]
lc_eqServerSingleton [lemma, in lc_eqServerSingleton]
lc_eqType [lemma, in lc_eqType]
lc_eqType' [lemma, in lc_eqType']
lc_eq [lemma, in lc_eq]
lc_eqSingleton_normal_import [lemma, in lc_eqSingleton_normal_import]
lc_eqSingleton_export [lemma, in lc_eqSingleton_export]
LHead [definition, in LHead]
LightComp [definition, in LightComp]
LightControlComp [definition, in LightControlComp]
LightsControlUseCaseArchitecture [definition, in LightsControlUseCaseArchitecture]
LightsControlUseCase_is_well_formed [lemma, in LightsControlUseCase_is_well_formed]
lists_with_same_elements_yield_same_component [lemma, in lists_with_same_elements_yield_same_component]
list_interface_eq_reflection [lemma, in list_interface_eq_reflection]
list_binding_eq_reflection [lemma, in list_binding_eq_reflection]
list_dec [definition, in list_dec]
list_interface_equality_bool2Prop [lemma, in list_interface_equality_bool2Prop]
LList [inductive, in LList]
LList_decomposition_n [lemma, in LList_decomposition_n]
LList_decompose_n [definition, in LList_decompose_n]
LList_decompose [definition, in LList_decompose]
LList_decomposition [lemma, in LList_decomposition]
LNil [constructor, in LNil]
LNil_not_Infinite [lemma, in LNil_not_Infinite]
LNth [definition, in LNth]
LNth_bisimilar [lemma, in LNth_bisimilar]
lookup_get_fact' [lemma, in lookup_get_fact']
lookup_get_comp_fact [lemma, in lookup_get_comp_fact]
lookup_get_fact [lemma, in lookup_get_fact]
lookup_get_fact_gen' [lemma, in lookup_get_fact_gen']
lookup_get_fact_gen'2 [lemma, in lookup_get_fact_gen'2]
lookup_unique_ids_gen' [lemma, in lookup_unique_ids_gen']
lookup_unique_ids_gen2 [lemma, in lookup_unique_ids_gen2]
lookup_id_fact [lemma, in lookup_id_fact]
lookup_query_fact [lemma, in lookup_query_fact]
lookup_get_comp [lemma, in lookup_get_comp]
lookup_unique_ids_gen [lemma, in lookup_unique_ids_gen]
lookup_backup_fact [lemma, in lookup_backup_fact]
lookup_solution_fact [lemma, in lookup_solution_fact]
lookup_mem_fact' [lemma, in lookup_mem_fact']
lookup_none_comp_fact [lemma, in lookup_none_comp_fact]
lookup_congruence_fact [lemma, in lookup_congruence_fact]
lookup_comp_fact [lemma, in lookup_comp_fact]
lookup_mem_fact [lemma, in lookup_mem_fact]
lookup_unique_ids [lemma, in lookup_unique_ids]
lookup_unique_ids_backup [lemma, in lookup_unique_ids_backup]
lookup'_id_fact [lemma, in lookup'_id_fact]
Lowest [constructor, in Lowest]
LTail [definition, in LTail]
LTL [section, in LTL]
LTL [library]
LTL.A_Proof_with_F_Infinite.A [variable, in A]
LTL.A_Proof_with_F_Infinite.P [variable, in P]
LTL.A_Proof_with_F_Infinite.a [variable, in a]
LTL.A_Proof_with_F_Infinite.b [variable, in b]
LTL.A_Proof_with_F_Infinite.c [variable, in c]
LTL.A_Proof_with_F_Infinite.w [variable, in w]
LTL.A_Proof_with_F_Infinite [section, in A_Proof_with_F_Infinite]
LTL.A_Proof_with_F_Infinite.w_omega [variable, in w_omega]
_ |= _ [notation, in ::x_'|='_x]
LTS [record, in LTS]
LTS [library]
lts_empty_trace [constructor, in lts_empty_trace]
lts_state [inductive, in lts_state]
lts_target_state [definition, in lts_target_state]
LTS_State [constructor, in LTS_State]
lts_trace [constructor, in lts_trace]
LTS_Trace [inductive, in LTS_Trace]
lts_lcons_trace [constructor, in lts_lcons_trace]
lts_states [definition, in lts_states]
M
makeCoffeeOrder [definition, in makeCoffeeOrder]makeSandwichOrder [definition, in makeSandwichOrder]
Mandatory [constructor, in Mandatory]
mandatory_interfaces_are_bound_reflection [lemma, in mandatory_interfaces_are_bound_reflection]
mandatory_interfaces_are_bound [definition, in mandatory_interfaces_are_bound]
mandatory_interfaces_are_bound_bool [definition, in mandatory_interfaces_are_bound_bool]
mandatory_interfaces_are_bound_dec [lemma, in mandatory_interfaces_are_bound_dec]
MapNil [constructor, in MapNil]
MapStep [constructor, in MapStep]
masterlts [definition, in masterlts]
MasterSlaveCoffee [library]
MasterSlaveCoffeeNet [definition, in MasterSlaveCoffeeNet]
MasterSlaveCoffeeNet_allowed_actions_from_q1q1_n_ready_fact [lemma, in MasterSlaveCoffeeNet_allowed_actions_from_q1q1_n_ready_fact]
master_ready_act [definition, in master_ready_act]
master_sts [definition, in master_sts]
master_acts [definition, in master_acts]
master_order_acts [definition, in master_order_acts]
mem [definition, in mem]
mem [definition, in mem]
membership_fact [lemma, in membership_fact]
Message [constructor, in Message]
message [inductive, in message]
Mk_binding [constructor, in Mk_binding]
Mk_symmetric_interface [definition, in Mk_symmetric_interface]
Mk_interface [constructor, in Mk_interface]
mk_arraylist [constructor, in mk_arraylist]
Mk_component [constructor, in Mk_component]
mk_Net [constructor, in mk_Net]
mk_LTS [constructor, in mk_LTS]
mk_SingletonNet [constructor, in mk_SingletonNet]
mst0 [definition, in mst0]
mst1 [definition, in mst1]
Multicast [constructor, in Multicast]
N
N [definition, in N]Nats [definition, in Nats]
nat_to_string_fact [axiom, in nat_to_string_fact]
nat_to_string [definition, in nat_to_string]
Net [inductive, in Net]
Net [library]
NetSingleton_State [constructor, in NetSingleton_State]
net_lcons_trace [constructor, in net_lcons_trace]
net_target_states [definition, in net_target_states]
net_empty_trace [constructor, in net_empty_trace]
net_state [inductive, in net_state]
net_target_states_from_q0q0' [lemma, in net_target_states_from_q0q0']
Net_State [constructor, in Net_State]
net_target_states_from_q0q0 [lemma, in net_target_states_from_q0q0]
Net_Trace [inductive, in Net_Trace]
net_target_states_from_q1q1' [lemma, in net_target_states_from_q1q1']
net_target_states_from_q1q1 [lemma, in net_target_states_from_q1q1]
net_target_states_fromq0q0_output [lemma, in net_target_states_fromq0q0_output]
Next [inductive, in Next]
Next_example [lemma, in Next_example]
Next_intro [constructor, in Next_intro]
nil_eq [lemma, in nil_eq]
nil_eqSingleton_export [lemma, in nil_eqSingleton_export]
nil_eqSingleton_normal_import [lemma, in nil_eqSingleton_normal_import]
nil_is_valid_path' [lemma, in nil_is_valid_path']
nil_is_valid_path [lemma, in nil_is_valid_path]
nil_eqType [lemma, in nil_eqType]
nil_eqType' [lemma, in nil_eqType']
nil_eqServerSingleton [lemma, in nil_eqServerSingleton]
Normal [constructor, in Normal]
NotConnected_Step [constructor, in NotConnected_Step]
NotInNil [constructor, in NotInNil]
NotInPairStep [constructor, in NotInPairStep]
NotInPair_Nil [constructor, in NotInPair_Nil]
NotInStep [constructor, in NotInStep]
not_in_congruence [lemma, in not_in_congruence]
not_in_list_pairs [definition, in not_in_list_pairs]
not_in_dec [lemma, in not_in_dec]
not_in_l_pairs [inductive, in not_in_l_pairs]
not_sequence [inductive, in not_sequence]
not_attainable_q0q0_q0q1 [lemma, in not_attainable_q0q0_q0q1]
not_in_preserved_by_removing_component [lemma, in not_in_preserved_by_removing_component]
not_in_l [inductive, in not_in_l]
not_attainable_q0q0_q1q0 [lemma, in not_attainable_q0q0_q1q0]
not_in_bool_correctness [lemma, in not_in_bool_correctness]
not_in_l_pairs_dec' [lemma, in not_in_l_pairs_dec']
not_in_l_pairs_bool_correctness [lemma, in not_in_l_pairs_bool_correctness]
not_in_list [definition, in not_in_list]
not_nil [definition, in not_nil]
not_in_l_nil [lemma, in not_in_l_nil]
not_binded [definition, in not_binded]
not_binded_bool_correctness [lemma, in not_binded_bool_correctness]
Not_Finite_Infinite [lemma, in Not_Finite_Infinite]
not_in_l_pairs_dec [lemma, in not_in_l_pairs_dec]
no_id_acc_clash_bool_completeness [lemma, in no_id_acc_clash_bool_completeness]
no_id_clash_bool_correctness [lemma, in no_id_clash_bool_correctness]
no_id_acc_clash [definition, in no_id_acc_clash]
no_clash_on_generation [definition, in no_clash_on_generation]
no_id_clash [definition, in no_id_clash]
no_id_acc_clash_bool_soundness [lemma, in no_id_acc_clash_bool_soundness]
no_interference_bool_correctness [lemma, in no_interference_bool_correctness]
no_id_clash_step [lemma, in no_id_clash_step]
no_id_clash' [definition, in no_id_clash']
no_id_acc_clash' [definition, in no_id_acc_clash']
N_has_sound_cardinality [lemma, in N_has_sound_cardinality]
N_has_sound_contingency [lemma, in N_has_sound_contingency]
O
omega [definition, in omega]omega_LNil [lemma, in omega_LNil]
omega_of_Finite [lemma, in omega_of_Finite]
omega_lappend [lemma, in omega_lappend]
omega_F_Infinite [lemma, in omega_F_Infinite]
omega_infinite [lemma, in omega_infinite]
one_step_entails_n_steps [lemma, in one_step_entails_n_steps]
one_two_three [lemma, in one_two_three]
operation [inductive, in operation]
operation_dec [lemma, in operation_dec]
Optional [constructor, in Optional]
op_sequence_reduction [lemma, in op_sequence_reduction]
P
p [axiom, in p]parameter [inductive, in parameter]
parameters [definition, in parameters]
ParamSpec [library]
park_principle [lemma, in park_principle]
path [definition, in path]
path_refl [lemma, in path_refl]
path_equality_bool2Prop [lemma, in path_equality_bool2Prop]
path_eq_reflection [lemma, in path_eq_reflection]
path_dec [lemma, in path_dec]
path_equality_Prop2bool [lemma, in path_equality_Prop2bool]
pN [definition, in pN]
prime_list_lookup [lemma, in prime_list_lookup]
Primitive [definition, in Primitive]
primitive [definition, in primitive]
PrimitiveA [definition, in PrimitiveA]
PrimitiveAPath [definition, in PrimitiveAPath]
PrimitiveB [definition, in PrimitiveB]
PrimitivePath [definition, in PrimitivePath]
primitive_are_internally_bounded [lemma, in primitive_are_internally_bounded]
process_assignment [definition, in process_assignment]
projectionBindingClientPath [definition, in projectionBindingClientPath]
projectionBindingIntId [definition, in projectionBindingIntId]
projectionBindingIntId2 [definition, in projectionBindingIntId2]
projectionBindingSubComponent [definition, in projectionBindingSubComponent]
projectionComponentBindings [definition, in projectionComponentBindings]
projectionComponentControlLevel [definition, in projectionComponentControlLevel]
projectionComponentId [definition, in projectionComponentId]
projectionComponentImplementationClass [definition, in projectionComponentImplementationClass]
projectionComponentInterfaces [definition, in projectionComponentInterfaces]
projectionComponentPath [definition, in projectionComponentPath]
projectionComponentSubComponents [definition, in projectionComponentSubComponents]
projectionInterfaceCardinality [definition, in projectionInterfaceCardinality]
projectionInterfaceContingency [definition, in projectionInterfaceContingency]
projectionInterfaceFunctionality [definition, in projectionInterfaceFunctionality]
projectionInterfaceId [definition, in projectionInterfaceId]
projectionInterfaceOwner [definition, in projectionInterfaceOwner]
projectionInterfaceRole [definition, in projectionInterfaceRole]
projectionInterfaceSignature [definition, in projectionInterfaceSignature]
projectionInterfaceVisibility [definition, in projectionInterfaceVisibility]
projectionNormalBindingComp1Id [definition, in projectionNormalBindingComp1Id]
projectionNormalBindingComp2Id [definition, in projectionNormalBindingComp2Id]
projectionNormalBindingInt1Id [definition, in projectionNormalBindingInt1Id]
projectionNormalBindingInt2Id [definition, in projectionNormalBindingInt2Id]
projStateBindings [definition, in projStateBindings]
projStateComponents [definition, in projStateComponents]
P_F_Infinite [lemma, in P_F_Infinite]
p1 [definition, in p1]
p2 [definition, in p2]
Q
query_interface_entail_false [lemma, in query_interface_entail_false]query_is_equal_for_well_formed_interfaces [lemma, in query_is_equal_for_well_formed_interfaces]
queue [definition, in queue]
queue_mem [definition, in queue_mem]
queue_transitions [definition, in queue_transitions]
queue_actions [definition, in queue_actions]
queue_states [definition, in queue_states]
queue_init [definition, in queue_init]
q0 [definition, in q0]
q1 [definition, in q1]
R
R [definition, in R]Read [constructor, in Read]
ready_to_start_fact [lemma, in ready_to_start_fact]
ready_to_start [definition, in ready_to_start]
receiveCoffeeOrder [definition, in receiveCoffeeOrder]
receiveSandwichOrder [definition, in receiveSandwichOrder]
Reductions [library]
reduction_example [lemma, in reduction_example]
reduction_example' [lemma, in reduction_example']
refl_step_closure [inductive, in refl_step_closure]
relation [definition, in relation]
RemoveBinding [definition, in RemoveBinding]
RemoveComponent [definition, in RemoveComponent]
remove_binding [definition, in remove_binding]
remove_component_nil_specification [lemma, in remove_component_nil_specification]
remove_id_and_search_for_it_yields_none [lemma, in remove_id_and_search_for_it_yields_none]
remove_component_fact [lemma, in remove_component_fact]
removing_binding_yields_a_subset_of_original [lemma, in removing_binding_yields_a_subset_of_original]
removing_a_binding_keeps_component_well_formed [lemma, in removing_a_binding_keeps_component_well_formed]
removing_binding_unaffect_bindings [lemma, in removing_binding_unaffect_bindings]
removing_binding_keeps_components_ids_unique [lemma, in removing_binding_keeps_components_ids_unique]
removing_component_from_non_empty_path_cannot_yield_empty_components [lemma, in removing_component_from_non_empty_path_cannot_yield_empty_components]
removing_from_empty_list_yields_empty_list [lemma, in removing_from_empty_list_yields_empty_list]
removing_binding_auxiliary [lemma, in removing_binding_auxiliary]
removing_component_keeps_bindings_well_formed [lemma, in removing_component_keeps_bindings_well_formed]
removing_comp_unaffect_bindings [lemma, in removing_comp_unaffect_bindings]
removing_binding_from_list_keeps_bindings_well_formed [lemma, in removing_binding_from_list_keeps_bindings_well_formed]
removing_components_fact [lemma, in removing_components_fact]
Rma [definition, in Rma]
Rm_component [constructor, in Rm_component]
Rm_binding [constructor, in Rm_binding]
role [inductive, in role]
role_eq_reflection [lemma, in role_eq_reflection]
role_bool_prop [lemma, in role_bool_prop]
root [definition, in root]
root [definition, in root]
root_config_is_unaffected_by_remove_comp [lemma, in root_config_is_unaffected_by_remove_comp]
root_config_is_unaffected_by_add_interface [lemma, in root_config_is_unaffected_by_add_interface]
root_config_is_unaffected_by_add_comp [lemma, in root_config_is_unaffected_by_add_comp]
root_config_is_unaffected_by_remove_binding [lemma, in root_config_is_unaffected_by_remove_binding]
root_config_is_unaffected_by_add_binding [lemma, in root_config_is_unaffected_by_add_binding]
rsc_trans [lemma, in rsc_trans]
rsc_step [constructor, in rsc_step]
rsc_base [constructor, in rsc_base]
R_useful [lemma, in R_useful]
R_bisim [lemma, in R_bisim]
S
S [definition, in S]same_nots [lemma, in same_nots]
same_well_formed_interfaces [lemma, in same_well_formed_interfaces]
same_unique_ids [lemma, in same_unique_ids]
same_by_ids [lemma, in same_by_ids]
same_nots' [lemma, in same_nots']
same_nots_pair [lemma, in same_nots_pair]
satisfies [definition, in satisfies]
SDoneRefl [constructor, in SDoneRefl]
Semantics [library]
SensedBrInfo [definition, in SensedBrInfo]
Seq [constructor, in Seq]
sequence_completion_gen [lemma, in sequence_completion_gen]
seq_lemma [lemma, in seq_lemma]
seq_fact' [lemma, in seq_fact']
seq_validity [lemma, in seq_validity]
seq_fact [lemma, in seq_fact]
seq_reduction_aux [lemma, in seq_reduction_aux]
Server [constructor, in Server]
ServerSingleton [constructor, in ServerSingleton]
server_singleton_are_bound_once_at_most_bool_one1_spec [lemma, in server_singleton_are_bound_once_at_most_bool_one1_spec]
server_singleton_are_bound_once_at_most [inductive, in server_singleton_are_bound_once_at_most]
server_singleton_are_bound_once_at_most_bool_one2_spec [lemma, in server_singleton_are_bound_once_at_most_bool_one2_spec]
server_singleton_are_bound_once_at_most_bool_fact [lemma, in server_singleton_are_bound_once_at_most_bool_fact]
server_singleton_are_bound_once_at_most_bool_one_rev_spec [lemma, in server_singleton_are_bound_once_at_most_bool_one_rev_spec]
server_singleton_are_bound_once_at_most_bool [definition, in server_singleton_are_bound_once_at_most_bool]
server_singleton_are_bound_once_at_most_bool_one [definition, in server_singleton_are_bound_once_at_most_bool_one]
sigC1 [axiom, in sigC1]
sigC2 [axiom, in sigC2]
sigC3 [axiom, in sigC3]
signature [definition, in signature]
signature_eq_reflection [lemma, in signature_eq_reflection]
signature_dec [lemma, in signature_dec]
sigS1 [axiom, in sigS1]
sigS2 [axiom, in sigS2]
sigS3 [axiom, in sigS3]
SimpleArchitecture [definition, in SimpleArchitecture]
simplelts [definition, in simplelts]
simplenet [definition, in simplenet]
simpleProof [lemma, in simpleProof]
simpleProof_Revisited [definition, in simpleProof_Revisited]
Singleton [constructor, in Singleton]
SingletonExport [constructor, in SingletonExport]
SingletonNormalImport [constructor, in SingletonNormalImport]
slavelts [definition, in slavelts]
slave_acts [definition, in slave_acts]
slave_sts [definition, in slave_sts]
slave_ready_act [definition, in slave_ready_act]
slave_order_acts [definition, in slave_order_acts]
slv0 [definition, in slv0]
slv1 [definition, in slv1]
SMakeBinding [constructor, in SMakeBinding]
SMakeComponent [constructor, in SMakeComponent]
SMakeInterface [constructor, in SMakeInterface]
sound_contingency_bool [definition, in sound_contingency_bool]
sound_contigency_correctness [definition, in sound_contigency_correctness]
sound_cardinality_dec [lemma, in sound_cardinality_dec]
sound_cardinality_reflection [lemma, in sound_cardinality_reflection]
sound_contingency_dec [lemma, in sound_contingency_dec]
sound_cardinality_correctness [definition, in sound_cardinality_correctness]
sound_cardinality [definition, in sound_cardinality]
sound_contingency [definition, in sound_contingency]
sound_contigency_reflection [lemma, in sound_contigency_reflection]
sound_cardinality_bool [definition, in sound_cardinality_bool]
spath [definition, in spath]
Squares_from [definition, in Squares_from]
SRemoveBinding [constructor, in SRemoveBinding]
SRemoveComponent [constructor, in SRemoveComponent]
SSeqFinish [constructor, in SSeqFinish]
SSeq1 [constructor, in SSeq1]
SSeq2 [constructor, in SSeq2]
state [definition, in state]
States [projection, in States]
state_mem [definition, in state_mem]
stay_in_state [definition, in stay_in_state]
step [inductive, in step]
string_of_nat [definition, in string_of_nat]
string_append_fact' [lemma, in string_append_fact']
string_append_fact [lemma, in string_append_fact]
stronger_inheritance [lemma, in stronger_inheritance]
str_symmetry [lemma, in str_symmetry]
sts [definition, in sts]
subcomponents_client_external_mandatory_interfaces_are_bound [inductive, in subcomponents_client_external_mandatory_interfaces_are_bound]
subcomponents_client_external_mandatory_interfaces_spec' [lemma, in subcomponents_client_external_mandatory_interfaces_spec']
subcomponents_client_external_mandatory_interfaces_fact [lemma, in subcomponents_client_external_mandatory_interfaces_fact]
subcomponents_client_external_mandatory_interfaces_are_bound_bool_one_rev_spec' [lemma, in subcomponents_client_external_mandatory_interfaces_are_bound_bool_one_rev_spec']
subcomponents_client_external_mandatory_interfaces_are_bound_bool [definition, in subcomponents_client_external_mandatory_interfaces_are_bound_bool]
subcomponents_client_external_mandatory_interfaces_nil_fact [lemma, in subcomponents_client_external_mandatory_interfaces_nil_fact]
subcomponents_client_external_mandatory_interfaces_spec [lemma, in subcomponents_client_external_mandatory_interfaces_spec]
subcomponents_client_external_mandatory_interfaces_are_bound_dec [lemma, in subcomponents_client_external_mandatory_interfaces_are_bound_dec]
subcomponents_client_external_mandatory_interfaces_are_bound_bool_one_spec [lemma, in subcomponents_client_external_mandatory_interfaces_are_bound_bool_one_spec]
subcomponents_client_external_mandatory_interfaces_are_bound_bool_one_rev_spec [lemma, in subcomponents_client_external_mandatory_interfaces_are_bound_bool_one_rev_spec]
subcomponents_client_external_mandatory_interfaces_are_bound_bool_fact [lemma, in subcomponents_client_external_mandatory_interfaces_are_bound_bool_fact]
subcomponents_client_external_singleton_interfaces_spec' [lemma, in subcomponents_client_external_singleton_interfaces_spec']
suffix_ident_spec [lemma, in suffix_ident_spec]
SwonLights [definition, in SwonLights]
symmetric_visibility [definition, in symmetric_visibility]
symmetric_role [definition, in symmetric_role]
SyncElement [constructor, in SyncElement]
SynchronizationVector [inductive, in SynchronizationVector]
synch_vectors [definition, in synch_vectors]
synch_vectors [definition, in synch_vectors]
SyncronizationElement [inductive, in SyncronizationElement]
SyncronizationOutput [inductive, in SyncronizationOutput]
SyncVector [constructor, in SyncVector]
sync_vectors [definition, in sync_vectors]
sync_notation [definition, in sync_notation]
system_binding [definition, in system_binding]
S_is_well_formed [lemma, in S_is_well_formed]
s0 [definition, in s0]
T
template_generation_produces_well_formed_components [lemma, in template_generation_produces_well_formed_components]test [lemma, in test]
ThesisRunningExample [library]
TraceExamples [library]
transitions [definition, in transitions]
Transitions [projection, in Transitions]
transitive_inheritance [lemma, in transitive_inheritance]
transitive_inheritance' [lemma, in transitive_inheritance']
trs [definition, in trs]
two_simplenet [definition, in two_simplenet]
two_simplelts [definition, in two_simplelts]
U
UniquePairs_Base [constructor, in UniquePairs_Base]UniquePairs_Step [constructor, in UniquePairs_Step]
unique_ids' [definition, in unique_ids']
unique_ids_is_preserved_by_adding_comp [lemma, in unique_ids_is_preserved_by_adding_comp]
unique_ids_fact' [lemma, in unique_ids_fact']
unique_ids_fact' [lemma, in unique_ids_fact']
unique_ids_dec [lemma, in unique_ids_dec]
unique_ids [inductive, in unique_ids]
unique_ids_fact [lemma, in unique_ids_fact]
unique_subset [lemma, in unique_subset]
Unique_Step [constructor, in Unique_Step]
unique_ids_nil [lemma, in unique_ids_nil]
unique_ids_sublist [lemma, in unique_ids_sublist]
unique_pairs_dec [lemma, in unique_pairs_dec]
unique_subset_gen [lemma, in unique_subset_gen]
unique_ids_one [lemma, in unique_ids_one]
unique_pairs [inductive, in unique_pairs]
unique_subset' [lemma, in unique_subset']
Unique_Base [constructor, in Unique_Base]
update_w_bindings_reduction_fact'' [lemma, in update_w_bindings_reduction_fact'']
update_sub_comp_red'' [lemma, in update_sub_comp_red'']
update_sub_comp_red [lemma, in update_sub_comp_red]
update_w_bindings_reduction_fact [lemma, in update_w_bindings_reduction_fact]
update_w_valid_bindings_reduction_fact [lemma, in update_w_valid_bindings_reduction_fact]
update_sub_comp_maitains_id [lemma, in update_sub_comp_maitains_id]
update_sub_comp_red' [lemma, in update_sub_comp_red']
update_sub_comps_keep_ids [lemma, in update_sub_comps_keep_ids]
updating_comps_unaffect_bindings [lemma, in updating_comps_unaffect_bindings]
updating_interfaces_is_well_formed [lemma, in updating_interfaces_is_well_formed]
updating_comps_bindings [lemma, in updating_comps_bindings]
V
Val [constructor, in Val]ValidComponentBinding_Base [constructor, in ValidComponentBinding_Base]
ValidComponentBinding_Step [constructor, in ValidComponentBinding_Step]
ValidInterfacePath_Step [constructor, in ValidInterfacePath_Step]
ValidInterfacePath_Base [constructor, in ValidInterfacePath_Base]
validity [lemma, in validity]
ValidN [constructor, in ValidN]
valid_mk_interfaces [lemma, in valid_mk_interfaces]
valid_removing_binding_fact' [lemma, in valid_removing_binding_fact']
valid_path_step [lemma, in valid_path_step]
valid_binding_lookup_fact [lemma, in valid_binding_lookup_fact]
valid_interface_path [definition, in valid_interface_path]
valid_no_id_acc_step [lemma, in valid_no_id_acc_step]
valid_interface_path_fact [lemma, in valid_interface_path_fact]
valid_binding [definition, in valid_binding]
valid_interface_path' [inductive, in valid_interface_path']
valid_path [inductive, in valid_path]
valid_binding_dec [lemma, in valid_binding_dec]
valid_binding_interface_fact [lemma, in valid_binding_interface_fact]
valid_binding_on_same_element_lists [lemma, in valid_binding_on_same_element_lists]
valid_rm_comp [lemma, in valid_rm_comp]
valid_bindings_correctness [lemma, in valid_bindings_correctness]
valid_adding_binding_fact [lemma, in valid_adding_binding_fact]
valid_component_binding' [inductive, in valid_component_binding']
valid_seq_aux [lemma, in valid_seq_aux]
valid_component_path_bool_correctness [lemma, in valid_component_path_bool_correctness]
valid_removing_binding_fact [lemma, in valid_removing_binding_fact]
valid_seq [lemma, in valid_seq]
valid_rm_bindings [lemma, in valid_rm_bindings]
valid_component_binding [definition, in valid_component_binding]
valid_interface_path_step [lemma, in valid_interface_path_step]
valid_coffee_combination [inductive, in valid_coffee_combination]
valid_component_binding_bool_correctness [lemma, in valid_component_binding_bool_correctness]
valid_path_fact' [lemma, in valid_path_fact']
valid_mk_comp [lemma, in valid_mk_comp]
valid_mk_bindings [lemma, in valid_mk_bindings]
valid_binding_fact [lemma, in valid_binding_fact]
valid_component_binding_has_valid_component_path [lemma, in valid_component_binding_has_valid_component_path]
valid_cross_binding [definition, in valid_cross_binding]
valid_path_fact [lemma, in valid_path_fact]
valid_path_on_non_empty_path_entails_non_empty_components [lemma, in valid_path_on_non_empty_path_entails_non_empty_components]
valid_binding_may_entail_false [lemma, in valid_binding_may_entail_false]
valid_interface_path_bool_correctness [lemma, in valid_interface_path_bool_correctness]
valid_component_path [definition, in valid_component_path]
Valid0 [constructor, in Valid0]
Var [constructor, in Var]
VCN [constructor, in VCN]
VC0 [constructor, in VC0]
visibility [inductive, in visibility]
visibility_eq_reflection [lemma, in visibility_eq_reflection]
visibility_dec [lemma, in visibility_dec]
vis_equality_Prop2bool [lemma, in vis_equality_Prop2bool]
vis_equality_bool2Prop' [lemma, in vis_equality_bool2Prop']
vis_equality_Prop2bool' [lemma, in vis_equality_Prop2bool']
vis_equality_bool2Prop [lemma, in vis_equality_bool2Prop]
vis_bool_conjunction_fact [lemma, in vis_bool_conjunction_fact]
W
WellFormedComponent [constructor, in WellFormedComponent]WellFormedInterfaces_Step [constructor, in WellFormedInterfaces_Step]
WellFormedInterfaces_Base [constructor, in WellFormedInterfaces_Base]
WellFormednessDecidability [library]
WellTypedDecidability [library]
well_formed_empty_component [lemma, in well_formed_empty_component]
well_formed_components [definition, in well_formed_components]
well_formed_removing_component_from_list [lemma, in well_formed_removing_component_from_list]
well_formed_interfaces [inductive, in well_formed_interfaces]
well_formed_component_has_well_formed_interfaces [lemma, in well_formed_component_has_well_formed_interfaces]
well_formed_bindings_in_nil [lemma, in well_formed_bindings_in_nil]
well_formed_interfaces_dec [lemma, in well_formed_interfaces_dec]
well_formed_nil_bindings' [lemma, in well_formed_nil_bindings']
well_formed_adding_interface [lemma, in well_formed_adding_interface]
well_formed_bindings [definition, in well_formed_bindings]
well_formed_empty_component' [lemma, in well_formed_empty_component']
well_formed_components_have_unique_ids [lemma, in well_formed_components_have_unique_ids]
well_formed_subset' [lemma, in well_formed_subset']
well_typed_correctness [lemma, in well_typed_correctness]
well_formed_component_minus_one_binding [lemma, in well_formed_component_minus_one_binding]
well_formed_lookup_split [lemma, in well_formed_lookup_split]
well_formed_subset [lemma, in well_formed_subset]
well_formed_dec [lemma, in well_formed_dec]
well_formed [definition, in well_formed]
well_formed_entail_unique_ids [lemma, in well_formed_entail_unique_ids]
well_formed_inheritance [lemma, in well_formed_inheritance]
well_formed_component_lc_dec [lemma, in well_formed_component_lc_dec]
well_formed_component [inductive, in well_formed_component]
well_formed_bool [definition, in well_formed_bool]
well_formed_component_dec [lemma, in well_formed_component_dec]
well_formed_nil_components [lemma, in well_formed_nil_components]
well_formed_adding_bindings [lemma, in well_formed_adding_bindings]
well_formed_bindings_dec [lemma, in well_formed_bindings_dec]
well_formed_nil_interfaces [lemma, in well_formed_nil_interfaces]
well_typed [definition, in well_typed]
well_formed_append' [lemma, in well_formed_append']
well_formed_subcomponents_update [lemma, in well_formed_subcomponents_update]
well_typed_bool [definition, in well_typed_bool]
well_formed_interfaces' [definition, in well_formed_interfaces']
well_formed_component_has_subcomponents_w_unique_ids [lemma, in well_formed_component_has_subcomponents_w_unique_ids]
well_formed_bindings_w_lookup [lemma, in well_formed_bindings_w_lookup]
well_formed_adding_component [lemma, in well_formed_adding_component]
well_formed_update_w_add_interface [lemma, in well_formed_update_w_add_interface]
well_formed_removing_component [lemma, in well_formed_removing_component]
well_formed_update_remove_sub_comps [lemma, in well_formed_update_remove_sub_comps]
well_formed_adding_component_interface [lemma, in well_formed_adding_component_interface]
well_formed_nil_bindings [lemma, in well_formed_nil_bindings]
well_formed_component_cons_dec [lemma, in well_formed_component_cons_dec]
well_formed_interface_append [lemma, in well_formed_interface_append]
well_formed_component_individuals [lemma, in well_formed_component_individuals]
well_formed_bindings_may_entail_false [lemma, in well_formed_bindings_may_entail_false]
well_formed_removing_binding_from_list [lemma, in well_formed_removing_binding_from_list]
well_formed_bindings_entailment [lemma, in well_formed_bindings_entailment]
well_formed_component_nil_dec [lemma, in well_formed_component_nil_dec]
well_formed_removing_binding_from_component [lemma, in well_formed_removing_binding_from_component]
well_formed_append [lemma, in well_formed_append]
well_formed_component_has_well_formed_sub_components [lemma, in well_formed_component_has_well_formed_sub_components]
well_formed_tail [lemma, in well_formed_tail]
well_formed_removing_bindings [lemma, in well_formed_removing_bindings]
well_typed_dec [lemma, in well_typed_dec]
WildCard [constructor, in WildCard]
other
_ ->idcs (binding_scope) [notation, in :binding_scope:x_'->idcs']_ [ _ ] (binding_scope) [notation, in :binding_scope:x_'['_x_']']
_ == _ (binding_scope) [notation, in :binding_scope:x_'=='_x]
_ ~~ _ (binding_scope) [notation, in :binding_scope:x_'~~'_x]
_ != _ (binding_scope) [notation, in :binding_scope:x_'!='_x]
_ ->idcc (binding_scope) [notation, in :binding_scope:x_'->idcc']
_ ->path (binding_scope) [notation, in :binding_scope:x_'->path']
_ == _ (card_scope) [notation, in :card_scope:x_'=='_x]
_ != _ (card_scope) [notation, in :card_scope:x_'!='_x]
_ ->id (component_scope) [notation, in :component_scope:x_'->id']
_ ->iclass (component_scope) [notation, in :component_scope:x_'->iclass']
_ ->controlLevel (component_scope) [notation, in :component_scope:x_'->controlLevel']
_ == _ (component_scope) [notation, in :component_scope:x_'=='_x]
_ ->itfs (component_scope) [notation, in :component_scope:x_'->itfs']
_ ->subComponents (component_scope) [notation, in :component_scope:x_'->subComponents']
_ ->path (component_scope) [notation, in :component_scope:x_'->path']
_ ->bnds (component_scope) [notation, in :component_scope:x_'->bnds']
_ ->interfaces (component_scope) [notation, in :component_scope:x_'->interfaces']
_ ->bindings (component_scope) [notation, in :component_scope:x_'->bindings']
_ ->subcomps (component_scope) [notation, in :component_scope:x_'->subcomps']
_ != _ (controlLevel_scope) [notation, in :controlLevel_scope:x_'!='_x]
_ == _ (controlLevel_scope) [notation, in :controlLevel_scope:x_'=='_x]
_ == _ (cont_scope) [notation, in :cont_scope:x_'=='_x]
_ != _ (cont_scope) [notation, in :cont_scope:x_'!='_x]
_ == _ (func_scope) [notation, in :func_scope:x_'=='_x]
_ != _ (func_scope) [notation, in :func_scope:x_'!='_x]
_ == _ (implementationClass_scope) [notation, in :implementationClass_scope:x_'=='_x]
_ != _ (implementationClass_scope) [notation, in :implementationClass_scope:x_'!='_x]
_ ->owner (interface_scope) [notation, in :interface_scope:x_'->owner']
_ [ _ ] (interface_scope) [notation, in :interface_scope:x_'['_x_']']
_ ->cardinality (interface_scope) [notation, in :interface_scope:x_'->cardinality']
_ [ _ , _ ] (interface_scope) [notation, in :interface_scope:x_'['_x_','_x_']']
_ ->id (interface_scope) [notation, in :interface_scope:x_'->id']
_ [ _ , _ , _ , _ ] (interface_scope) [notation, in :interface_scope:x_'['_x_','_x_','_x_','_x_']']
_ ->sig (interface_scope) [notation, in :interface_scope:x_'->sig']
_ ->contingency (interface_scope) [notation, in :interface_scope:x_'->contingency']
_ == _ (interface_scope) [notation, in :interface_scope:x_'=='_x]
_ ->visibility (interface_scope) [notation, in :interface_scope:x_'->visibility']
_ ->functionality (interface_scope) [notation, in :interface_scope:x_'->functionality']
_ != _ (interface_scope) [notation, in :interface_scope:x_'!='_x]
_ ->role (interface_scope) [notation, in :interface_scope:x_'->role']
_ [ _ ; _ ] (interface_scope) [notation, in :interface_scope:x_'['_x_';'_x_']']
_ [ _ , _ , _ ] (interface_scope) [notation, in :interface_scope:x_'['_x_','_x_','_x_']']
_ [ _ , _ , _ ] (interface_scope) [notation, in :interface_scope:x_'['_x_','_x_','_x_']']
[ _ ; .. ; _ ] (list_scope) [notation, in :list_scope:'['_x_';'_'..'_';'_x_']']
[ _ ] (list_scope) [notation, in :list_scope:'['_x_']']
_ == _ (list_interface_scope) [notation, in :list_interface_scope:x_'=='_x]
_ == _ (list_binding_scope) [notation, in :list_binding_scope:x_'=='_x]
[ ] (list_scope) [notation, in :list_scope:'['_']']
_ == _ (opt_comp_scope) [notation, in :opt_comp_scope:x_'=='_x]
_ != _ (opt_comp_scope) [notation, in :opt_comp_scope:x_'!='_x]
_ == _ (path_scope) [notation, in :path_scope:x_'=='_x]
_ != _ (path_scope) [notation, in :path_scope:x_'!='_x]
_ != _ (role_scope) [notation, in :role_scope:x_'!='_x]
sym- _ (role_scope) [notation, in :role_scope:'sym-'_x]
_ == _ (role_scope) [notation, in :role_scope:x_'=='_x]
_ != _ (signature_scope) [notation, in :signature_scope:x_'!='_x]
_ == _ (signature_scope) [notation, in :signature_scope:x_'=='_x]
_ ->components (state_scope) [notation, in :state_scope:x_'->components']
_ ->bindings (state_scope) [notation, in :state_scope:x_'->bindings']
sym- _ (vis_scope) [notation, in :vis_scope:'sym-'_x]
_ != _ (vis_scope) [notation, in :vis_scope:x_'!='_x]
_ == _ (vis_scope) [notation, in :vis_scope:x_'=='_x]
_ == _ [notation, in ::x_'=='_x]
_ / _ ~~~> _ / _ [notation, in ::x_'/'_x_'~~~>'_x_'/'_x]
_ [| _ |] [notation, in ::x_'[|'_x_'|]']
_ / _ ~~~>* _ / _ [notation, in ::x_'/'_x_'~~~>*'_x_'/'_x]
_ != _ [notation, in ::x_'!='_x]
_ ; _ [notation, in ::x_';'_x]
_ |= _ [notation, in ::x_'|='_x]
_ |= _ [notation, in ::x_'|='_x]
_ * ( _ , _ ) [notation, in ::x_'*'_'('_x_','_x_')']
_ === _ [notation, in ::x_'==='_x]
_ ->> _ [notation, in ::x_'->>'_x]
_ [| _ |] <- _ [notation, in ::x_'[|'_x_'|]'_'<-'_x]
_ [ _ ] [notation, in ::x_'['_x_']']
new ArrayList
new ArrayList
<< _ , .. , _ >> -> _ [notation, in ::'<<'_x_','_'..'_','_x_'>>'_'->'_x]
[ _ ; .. ; _ ] [notation, in ::'['_x_';'_'..'_';'_x_']']
[ _ / _ ] [notation, in ::'['_x_'/'_x_']']
[ _ ] [notation, in ::'['_x_']']
[ _ \ _ ] [notation, in ::'['_x_'\'_x_']']
[ ] [notation, in ::'['_']']
Projection Index
A
Actions [in Actions]arraylist_length [in arraylist_length]
C
contents [in contents]E
element_type [in element_type]I
Init [in Init]S
States [in States]T
Transitions [in Transitions]Record Index
A
ArrayList [in ArrayList]L
LTS [in LTS]Lemma Index
A
adding_binding_unaffect_bindings [in adding_binding_unaffect_bindings]adding_comp_unaffect_bindings [in adding_comp_unaffect_bindings]
adding_interface_keeps_components_ids_unique [in adding_interface_keeps_components_ids_unique]
adding_comp_keeps_bindings_well_formed [in adding_comp_keeps_bindings_well_formed]
adding_interface_keeps_bindings_well_formed [in adding_interface_keeps_bindings_well_formed]
adding_interface_maintains_component_id [in adding_interface_maintains_component_id]
adding_binding_auxiliary [in adding_binding_auxiliary]
adding_3_lights [in adding_3_lights]
adding_comp_maintains_valid_bindings [in adding_comp_maintains_valid_bindings]
adding_interface_unaffect_bindings [in adding_interface_unaffect_bindings]
add_binding_fact [in add_binding_fact]
add_interface_may_entail_false [in add_interface_may_entail_false]
add_binding_fact_nil_comps [in add_binding_fact_nil_comps]
add_3_lights [in add_3_lights]
add_comp_may_entail_false [in add_comp_may_entail_false]
allowed_actions_from_sv_elements_coffee_fact [in allowed_actions_from_sv_elements_coffee_fact]
allowed_actions_from_q1q1_sandwich_fact [in allowed_actions_from_q1q1_sandwich_fact]
all_the_same_fact [in all_the_same_fact]
always_a [in always_a]
Always_Infinite [in Always_Infinite]
appending_binding_keeps_component_well_formed [in appending_binding_keeps_component_well_formed]
appending_interface_keeps_bindings_well_formed [in appending_interface_keeps_bindings_well_formed]
app_str_yield_different_str [in app_str_yield_different_str]
ascii_eq_reflection [in ascii_eq_reflection]
B
beq_string_reflection [in beq_string_reflection]beq_comp_id_fact [in beq_comp_id_fact]
beq_visibility_symmetry [in beq_visibility_symmetry]
beq_ident_symmetry' [in beq_ident_symmetry']
beq_bool_refl [in beq_bool_refl]
beq_ident_symmetry [in beq_ident_symmetry]
beq_string_reflection_in_prop [in beq_string_reflection_in_prop]
beq_string_reflection_in_bool [in beq_string_reflection_in_bool]
beq_acc_fact [in beq_acc_fact]
beq_visibility_reflexivity [in beq_visibility_reflexivity]
bindings_still_valid_removing_unbinded_component [in bindings_still_valid_removing_unbinded_component]
bindings_lookup_fact [in bindings_lookup_fact]
bindings_unaffected [in bindings_unaffected]
binding_eq_reflection [in binding_eq_reflection]
binding_equality_bool2Prop [in binding_equality_bool2Prop]
binding_dec [in binding_dec]
binding_is_not_a_duplicate_bool_correctness [in binding_is_not_a_duplicate_bool_correctness]
binding_equality_Prop2bool [in binding_equality_Prop2bool]
binding_cannot_be_crossing_if_valid [in binding_cannot_be_crossing_if_valid]
binding_exists_correctness [in binding_exists_correctness]
bisimilar_LNth [in bisimilar_LNth]
bisimilar_sym [in bisimilar_sym]
bisimilar_trans [in bisimilar_trans]
bisimilar_of_Finite_is_eq [in bisimilar_of_Finite_is_eq]
bisimilar_inv_1 [in bisimilar_inv_1]
bisimilar_inv_2 [in bisimilar_inv_2]
bisimilar_refl [in bisimilar_refl]
bisimilar_of_Finite_is_Finite [in bisimilar_of_Finite_is_Finite]
bisimilar_of_Infinite_is_Infinite [in bisimilar_of_Infinite_is_Infinite]
bisimilar_equiv [in bisimilar_equiv]
ble_nat_reflection [in ble_nat_reflection]
bneq_false_entails_beq_true [in bneq_false_entails_beq_true]
bneq_true_entails_beq_false [in bneq_true_entails_beq_false]
boolean_function_fact [in boolean_function_fact]
bool_dec_fact [in bool_dec_fact]
bool_conjunction_acc [in bool_conjunction_acc]
bool_symmetry_fact [in bool_symmetry_fact]
bool_conjunction_fact [in bool_conjunction_fact]
bool_conjunction_fact' [in bool_conjunction_fact']
bool_fact [in bool_fact]
build_state_fact' [in build_state_fact']
build_state_fact [in build_state_fact]
build_state_reduction_fact [in build_state_reduction_fact]
build_state_soundness [in build_state_soundness]
build_state_correctness [in build_state_correctness]
build_state_completeness [in build_state_completeness]
C
cardinality_eq_reflection [in cardinality_eq_reflection]check_if_recipients_are_mandatory'_fact [in check_if_recipients_are_mandatory'_fact]
check_if_recipients_are_mandatory_fact [in check_if_recipients_are_mandatory_fact]
check_if_recipients_are_mandatory_spec [in check_if_recipients_are_mandatory_spec]
check_if_mandatory_fact' [in check_if_mandatory_fact']
check_if_singleton_requirement_is_met_fact [in check_if_singleton_requirement_is_met_fact]
check_if_mandatory_fact [in check_if_mandatory_fact]
check_if_singleton_requirement_is_met_fact' [in check_if_singleton_requirement_is_met_fact']
client_internal_mandatory_interfaces_are_bound_bool_one_rev_spec [in client_internal_mandatory_interfaces_are_bound_bool_one_rev_spec]
client_singleton_are_bound_once_at_most_normal_import_bindings_bool_fact [in client_singleton_are_bound_once_at_most_normal_import_bindings_bool_fact]
client_internal_mandatory_interfaces_are_bound_bool_one_rev_spec_proof_nr_2 [in client_internal_mandatory_interfaces_are_bound_bool_one_rev_spec_proof_nr_2]
client_singleton_are_bound_once_at_most_export_bindings_bool_one_fact [in client_singleton_are_bound_once_at_most_export_bindings_bool_one_fact]
client_singleton_are_bound_once_at_most_normal_import_bindings_bool_one_rev_spec' [in client_singleton_are_bound_once_at_most_normal_import_bindings_bool_one_rev_spec']
client_singleton_are_bound_once_at_most_normal_import_bindings_bool_one_rev_spec [in client_singleton_are_bound_once_at_most_normal_import_bindings_bool_one_rev_spec]
client_internal_mandatory_interfaces_are_bound_bool_one_spec [in client_internal_mandatory_interfaces_are_bound_bool_one_spec]
client_singleton_are_bound_once_at_most_export_bindings_bool_fact [in client_singleton_are_bound_once_at_most_export_bindings_bool_fact]
client_internal_mandatory_interfaces_are_bound_bool_fact [in client_internal_mandatory_interfaces_are_bound_bool_fact]
combineN_coffee_orders_fact [in combineN_coffee_orders_fact]
component_dec [in component_dec]
component_is_not_connected_bool_soundness [in component_is_not_connected_bool_soundness]
component_query_fact [in component_query_fact]
component_is_not_connected_bool_completeness [in component_is_not_connected_bool_completeness]
cons_eqServerSingleton [in cons_eqServerSingleton]
cons_eqSingleton_export [in cons_eqSingleton_export]
cons_eq [in cons_eq]
cons_eqType [in cons_eqType]
cons_eqSingleton_normal_import [in cons_eqSingleton_normal_import]
cons_eqType' [in cons_eqType']
contingency_eq_reflection [in contingency_eq_reflection]
controlLevel_eq_reflection [in controlLevel_eq_reflection]
controlLevel_dec [in controlLevel_dec]
controlLevel_equality_bool2Prop [in controlLevel_equality_bool2Prop]
control_level_dec [in control_level_dec]
cross_binding_cannot_happen [in cross_binding_cannot_happen]
C_is_well_formed [in C_is_well_formed]
D
dec_unique_ids_correctness [in dec_unique_ids_correctness]dec_interfaces_correctness [in dec_interfaces_correctness]
dec_state_correctness [in dec_state_correctness]
dec_component_correctness [in dec_component_correctness]
dec_bindings_correctness [in dec_bindings_correctness]
done_is_quiet [in done_is_quiet]
done_is_quiet' [in done_is_quiet']
E
element_in_removed_set_is_in_original [in element_in_removed_set_is_in_original]empty_state_is_well_formed [in empty_state_is_well_formed]
empty_components_entail_no_bindings [in empty_components_entail_no_bindings]
eqServerSingleton_correctness [in eqServerSingleton_correctness]
eqSingleton_normal_import_correctness [in eqSingleton_normal_import_correctness]
eqSingleton_export_correctness [in eqSingleton_export_correctness]
eqType_correctness [in eqType_correctness]
eqType'_correctness [in eqType'_correctness]
errorState_means_stuck_reduction [in errorState_means_stuck_reduction]
errorState_means_stuck_reduction' [in errorState_means_stuck_reduction']
eval_reduction_fact [in eval_reduction_fact]
Eventually_of_LAppend [in Eventually_of_LAppend]
execute_computes_the_semantics [in execute_computes_the_semantics]
ext_client_mand_mapping_fact [in ext_client_mand_mapping_fact]
F
final [in final]Finite_not_Infinite [in Finite_not_Infinite]
Finite_of_LCons [in Finite_of_LCons]
first_well_typedness_proof [in first_well_typedness_proof]
first_well_formedness_proof [in first_well_formedness_proof]
forever_infinite [in forever_infinite]
forever_unfold [in forever_unfold]
from_q1q1_target_states [in from_q1q1_target_states]
from_q1q1_target_states_interleaving' [in from_q1q1_target_states_interleaving']
from_unfold [in from_unfold]
from_Infinite_V0 [in from_Infinite_V0]
from_q0q0_target_states_interleaving' [in from_q0q0_target_states_interleaving']
from_q0q0_target_states [in from_q0q0_target_states]
from_Infinite [in from_Infinite]
from_q0q0_target_states_interleaving [in from_q0q0_target_states_interleaving]
from_q1q1_target_states_interleaving [in from_q1q1_target_states_interleaving]
functionality_eq_reflection [in functionality_eq_reflection]
F_Infinite_cons [in F_Infinite_cons]
F_Infinite_consR [in F_Infinite_consR]
G
general_omega_LNil [in general_omega_LNil]general_omega_LNil_LCons [in general_omega_LNil_LCons]
general_omega_LCons [in general_omega_LCons]
general_omega_lappend [in general_omega_lappend]
general_omega_infinite [in general_omega_infinite]
general_omega_shoots_again [in general_omega_shoots_again]
general_omega_of_Finite [in general_omega_of_Finite]
generate_0 [in generate_0]
generate_1 [in generate_1]
generate_from_template_fact [in generate_from_template_fact]
generate_n_states_len [in generate_n_states_len]
generate_from_template_spec [in generate_from_template_spec]
generation_has_unique_ids [in generation_has_unique_ids]
get_parent_eq [in get_parent_eq]
get_parent_step [in get_parent_step]
get_normal_binding_recipients_fact [in get_normal_binding_recipients_fact]
get_normal_binding_recipients_aux2_trivial_fact [in get_normal_binding_recipients_aux2_trivial_fact]
get_export_bindings_not_nil [in get_export_bindings_not_nil]
get_normal_import_bindings_fact [in get_normal_import_bindings_fact]
get_component_fact' [in get_component_fact']
get_interfaces_vis_role_cont_fact [in get_interfaces_vis_role_cont_fact]
get_component_commutes_on_l [in get_component_commutes_on_l]
get_component_path_eq [in get_component_path_eq]
get_component_fact'' [in get_component_fact'']
get_component_on_empty_components_entails_false [in get_component_on_empty_components_entails_false]
get_component_fact_same_interfaces' [in get_component_fact_same_interfaces']
get_component_fact [in get_component_fact]
get_interface_fact_id [in get_interface_fact_id]
get_interface_fact_acc [in get_interface_fact_acc]
get_interface_fact [in get_interface_fact]
get_component_correct [in get_component_correct]
get_interfaces_vis_role_cont_spec [in get_interfaces_vis_role_cont_spec]
get_component_fact_same_interfaces [in get_component_fact_same_interfaces]
get_component_with_path_dec [in get_component_with_path_dec]
get_left_most_fact1 [in get_left_most_fact1]
get_left_most_fact2 [in get_left_most_fact2]
get_interface_post [in get_interface_post]
get_comp_fact [in get_comp_fact]
get_interface_membership_fact [in get_interface_membership_fact]
get_component_dec [in get_component_dec]
I
ident_equality_Prop2bool [in ident_equality_Prop2bool]ident_equality_bool2Prop' [in ident_equality_bool2Prop']
ident_dec [in ident_dec]
ident_equality_Prop2bool' [in ident_equality_Prop2bool']
ident_equality_bool2Prop [in ident_equality_bool2Prop]
ident_eq_reflection [in ident_eq_reflection]
ids_unicity_kept_removing_component [in ids_unicity_kept_removing_component]
implementationClass_eq_reflection [in implementationClass_eq_reflection]
implementationClass_dec [in implementationClass_dec]
Infinite_ready_interleaving [in Infinite_ready_interleaving]
Infinite_act [in Infinite_act]
Infinite_of_LCons [in Infinite_of_LCons]
Infinite_not_Finite [in Infinite_not_Finite]
Infinite_act' [in Infinite_act']
inner_symmetry [in inner_symmetry]
InstantiatedExample.Infinite_ready_interleaving [in Infinite_ready_interleaving]
interfaces_fact [in interfaces_fact]
interfaces_are_well_formed [in interfaces_are_well_formed]
interfaces_are_the_same [in interfaces_are_the_same]
interfaces_dec [in interfaces_dec]
interface_dec [in interface_dec]
interface_dec [in interface_dec]
interface_eq_reflection [in interface_eq_reflection]
internal_or_external [in internal_or_external]
in_app_cons_fact [in in_app_cons_fact]
in_entailment [in in_entailment]
in_get_component_fact [in in_get_component_fact]
L
LAppend_of_Finite [in LAppend_of_Finite]LAppend_G_Infinite [in LAppend_G_Infinite]
LAppend_assoc [in LAppend_assoc]
LAppend_of_Infinite_eq [in LAppend_of_Infinite_eq]
LAppend_LNil [in LAppend_LNil]
LAppend_LCons [in LAppend_LCons]
LAppend_G_Infinite_R [in LAppend_G_Infinite_R]
LAppend_of_Infinite [in LAppend_of_Infinite]
lc_eqServerSingleton [in lc_eqServerSingleton]
lc_eqType [in lc_eqType]
lc_eqType' [in lc_eqType']
lc_eq [in lc_eq]
lc_eqSingleton_normal_import [in lc_eqSingleton_normal_import]
lc_eqSingleton_export [in lc_eqSingleton_export]
LightsControlUseCase_is_well_formed [in LightsControlUseCase_is_well_formed]
lists_with_same_elements_yield_same_component [in lists_with_same_elements_yield_same_component]
list_interface_eq_reflection [in list_interface_eq_reflection]
list_binding_eq_reflection [in list_binding_eq_reflection]
list_interface_equality_bool2Prop [in list_interface_equality_bool2Prop]
LList_decomposition_n [in LList_decomposition_n]
LList_decomposition [in LList_decomposition]
LNil_not_Infinite [in LNil_not_Infinite]
LNth_bisimilar [in LNth_bisimilar]
lookup_get_fact' [in lookup_get_fact']
lookup_get_comp_fact [in lookup_get_comp_fact]
lookup_get_fact [in lookup_get_fact]
lookup_get_fact_gen' [in lookup_get_fact_gen']
lookup_get_fact_gen'2 [in lookup_get_fact_gen'2]
lookup_unique_ids_gen' [in lookup_unique_ids_gen']
lookup_unique_ids_gen2 [in lookup_unique_ids_gen2]
lookup_id_fact [in lookup_id_fact]
lookup_query_fact [in lookup_query_fact]
lookup_get_comp [in lookup_get_comp]
lookup_unique_ids_gen [in lookup_unique_ids_gen]
lookup_backup_fact [in lookup_backup_fact]
lookup_solution_fact [in lookup_solution_fact]
lookup_mem_fact' [in lookup_mem_fact']
lookup_none_comp_fact [in lookup_none_comp_fact]
lookup_congruence_fact [in lookup_congruence_fact]
lookup_comp_fact [in lookup_comp_fact]
lookup_mem_fact [in lookup_mem_fact]
lookup_unique_ids [in lookup_unique_ids]
lookup_unique_ids_backup [in lookup_unique_ids_backup]
lookup'_id_fact [in lookup'_id_fact]
M
mandatory_interfaces_are_bound_reflection [in mandatory_interfaces_are_bound_reflection]mandatory_interfaces_are_bound_dec [in mandatory_interfaces_are_bound_dec]
MasterSlaveCoffeeNet_allowed_actions_from_q1q1_n_ready_fact [in MasterSlaveCoffeeNet_allowed_actions_from_q1q1_n_ready_fact]
membership_fact [in membership_fact]
N
net_target_states_from_q0q0' [in net_target_states_from_q0q0']net_target_states_from_q0q0 [in net_target_states_from_q0q0]
net_target_states_from_q1q1' [in net_target_states_from_q1q1']
net_target_states_from_q1q1 [in net_target_states_from_q1q1]
net_target_states_fromq0q0_output [in net_target_states_fromq0q0_output]
Next_example [in Next_example]
nil_eq [in nil_eq]
nil_eqSingleton_export [in nil_eqSingleton_export]
nil_eqSingleton_normal_import [in nil_eqSingleton_normal_import]
nil_is_valid_path' [in nil_is_valid_path']
nil_is_valid_path [in nil_is_valid_path]
nil_eqType [in nil_eqType]
nil_eqType' [in nil_eqType']
nil_eqServerSingleton [in nil_eqServerSingleton]
not_in_congruence [in not_in_congruence]
not_in_dec [in not_in_dec]
not_attainable_q0q0_q0q1 [in not_attainable_q0q0_q0q1]
not_in_preserved_by_removing_component [in not_in_preserved_by_removing_component]
not_attainable_q0q0_q1q0 [in not_attainable_q0q0_q1q0]
not_in_bool_correctness [in not_in_bool_correctness]
not_in_l_pairs_dec' [in not_in_l_pairs_dec']
not_in_l_pairs_bool_correctness [in not_in_l_pairs_bool_correctness]
not_in_l_nil [in not_in_l_nil]
not_binded_bool_correctness [in not_binded_bool_correctness]
Not_Finite_Infinite [in Not_Finite_Infinite]
not_in_l_pairs_dec [in not_in_l_pairs_dec]
no_id_acc_clash_bool_completeness [in no_id_acc_clash_bool_completeness]
no_id_clash_bool_correctness [in no_id_clash_bool_correctness]
no_id_acc_clash_bool_soundness [in no_id_acc_clash_bool_soundness]
no_interference_bool_correctness [in no_interference_bool_correctness]
no_id_clash_step [in no_id_clash_step]
N_has_sound_cardinality [in N_has_sound_cardinality]
N_has_sound_contingency [in N_has_sound_contingency]
O
omega_LNil [in omega_LNil]omega_of_Finite [in omega_of_Finite]
omega_lappend [in omega_lappend]
omega_F_Infinite [in omega_F_Infinite]
omega_infinite [in omega_infinite]
one_step_entails_n_steps [in one_step_entails_n_steps]
one_two_three [in one_two_three]
operation_dec [in operation_dec]
op_sequence_reduction [in op_sequence_reduction]
P
park_principle [in park_principle]path_refl [in path_refl]
path_equality_bool2Prop [in path_equality_bool2Prop]
path_eq_reflection [in path_eq_reflection]
path_dec [in path_dec]
path_equality_Prop2bool [in path_equality_Prop2bool]
prime_list_lookup [in prime_list_lookup]
primitive_are_internally_bounded [in primitive_are_internally_bounded]
P_F_Infinite [in P_F_Infinite]
Q
query_interface_entail_false [in query_interface_entail_false]query_is_equal_for_well_formed_interfaces [in query_is_equal_for_well_formed_interfaces]
R
ready_to_start_fact [in ready_to_start_fact]reduction_example [in reduction_example]
reduction_example' [in reduction_example']
remove_component_nil_specification [in remove_component_nil_specification]
remove_id_and_search_for_it_yields_none [in remove_id_and_search_for_it_yields_none]
remove_component_fact [in remove_component_fact]
removing_binding_yields_a_subset_of_original [in removing_binding_yields_a_subset_of_original]
removing_a_binding_keeps_component_well_formed [in removing_a_binding_keeps_component_well_formed]
removing_binding_unaffect_bindings [in removing_binding_unaffect_bindings]
removing_binding_keeps_components_ids_unique [in removing_binding_keeps_components_ids_unique]
removing_component_from_non_empty_path_cannot_yield_empty_components [in removing_component_from_non_empty_path_cannot_yield_empty_components]
removing_from_empty_list_yields_empty_list [in removing_from_empty_list_yields_empty_list]
removing_binding_auxiliary [in removing_binding_auxiliary]
removing_component_keeps_bindings_well_formed [in removing_component_keeps_bindings_well_formed]
removing_comp_unaffect_bindings [in removing_comp_unaffect_bindings]
removing_binding_from_list_keeps_bindings_well_formed [in removing_binding_from_list_keeps_bindings_well_formed]
removing_components_fact [in removing_components_fact]
role_eq_reflection [in role_eq_reflection]
role_bool_prop [in role_bool_prop]
root_config_is_unaffected_by_remove_comp [in root_config_is_unaffected_by_remove_comp]
root_config_is_unaffected_by_add_interface [in root_config_is_unaffected_by_add_interface]
root_config_is_unaffected_by_add_comp [in root_config_is_unaffected_by_add_comp]
root_config_is_unaffected_by_remove_binding [in root_config_is_unaffected_by_remove_binding]
root_config_is_unaffected_by_add_binding [in root_config_is_unaffected_by_add_binding]
rsc_trans [in rsc_trans]
R_useful [in R_useful]
R_bisim [in R_bisim]
S
same_nots [in same_nots]same_well_formed_interfaces [in same_well_formed_interfaces]
same_unique_ids [in same_unique_ids]
same_by_ids [in same_by_ids]
same_nots' [in same_nots']
same_nots_pair [in same_nots_pair]
sequence_completion_gen [in sequence_completion_gen]
seq_lemma [in seq_lemma]
seq_fact' [in seq_fact']
seq_validity [in seq_validity]
seq_fact [in seq_fact]
seq_reduction_aux [in seq_reduction_aux]
server_singleton_are_bound_once_at_most_bool_one1_spec [in server_singleton_are_bound_once_at_most_bool_one1_spec]
server_singleton_are_bound_once_at_most_bool_one2_spec [in server_singleton_are_bound_once_at_most_bool_one2_spec]
server_singleton_are_bound_once_at_most_bool_fact [in server_singleton_are_bound_once_at_most_bool_fact]
server_singleton_are_bound_once_at_most_bool_one_rev_spec [in server_singleton_are_bound_once_at_most_bool_one_rev_spec]
signature_eq_reflection [in signature_eq_reflection]
signature_dec [in signature_dec]
simpleProof [in simpleProof]
sound_cardinality_dec [in sound_cardinality_dec]
sound_cardinality_reflection [in sound_cardinality_reflection]
sound_contingency_dec [in sound_contingency_dec]
sound_contigency_reflection [in sound_contigency_reflection]
string_append_fact' [in string_append_fact']
string_append_fact [in string_append_fact]
stronger_inheritance [in stronger_inheritance]
str_symmetry [in str_symmetry]
subcomponents_client_external_mandatory_interfaces_spec' [in subcomponents_client_external_mandatory_interfaces_spec']
subcomponents_client_external_mandatory_interfaces_fact [in subcomponents_client_external_mandatory_interfaces_fact]
subcomponents_client_external_mandatory_interfaces_are_bound_bool_one_rev_spec' [in subcomponents_client_external_mandatory_interfaces_are_bound_bool_one_rev_spec']
subcomponents_client_external_mandatory_interfaces_nil_fact [in subcomponents_client_external_mandatory_interfaces_nil_fact]
subcomponents_client_external_mandatory_interfaces_spec [in subcomponents_client_external_mandatory_interfaces_spec]
subcomponents_client_external_mandatory_interfaces_are_bound_dec [in subcomponents_client_external_mandatory_interfaces_are_bound_dec]
subcomponents_client_external_mandatory_interfaces_are_bound_bool_one_spec [in subcomponents_client_external_mandatory_interfaces_are_bound_bool_one_spec]
subcomponents_client_external_mandatory_interfaces_are_bound_bool_one_rev_spec [in subcomponents_client_external_mandatory_interfaces_are_bound_bool_one_rev_spec]
subcomponents_client_external_mandatory_interfaces_are_bound_bool_fact [in subcomponents_client_external_mandatory_interfaces_are_bound_bool_fact]
subcomponents_client_external_singleton_interfaces_spec' [in subcomponents_client_external_singleton_interfaces_spec']
suffix_ident_spec [in suffix_ident_spec]
S_is_well_formed [in S_is_well_formed]
T
template_generation_produces_well_formed_components [in template_generation_produces_well_formed_components]test [in test]
transitive_inheritance [in transitive_inheritance]
transitive_inheritance' [in transitive_inheritance']
U
unique_ids_is_preserved_by_adding_comp [in unique_ids_is_preserved_by_adding_comp]unique_ids_fact' [in unique_ids_fact']
unique_ids_fact' [in unique_ids_fact']
unique_ids_dec [in unique_ids_dec]
unique_ids_fact [in unique_ids_fact]
unique_subset [in unique_subset]
unique_ids_nil [in unique_ids_nil]
unique_ids_sublist [in unique_ids_sublist]
unique_pairs_dec [in unique_pairs_dec]
unique_subset_gen [in unique_subset_gen]
unique_ids_one [in unique_ids_one]
unique_subset' [in unique_subset']
update_w_bindings_reduction_fact'' [in update_w_bindings_reduction_fact'']
update_sub_comp_red'' [in update_sub_comp_red'']
update_sub_comp_red [in update_sub_comp_red]
update_w_bindings_reduction_fact [in update_w_bindings_reduction_fact]
update_w_valid_bindings_reduction_fact [in update_w_valid_bindings_reduction_fact]
update_sub_comp_maitains_id [in update_sub_comp_maitains_id]
update_sub_comp_red' [in update_sub_comp_red']
update_sub_comps_keep_ids [in update_sub_comps_keep_ids]
updating_comps_unaffect_bindings [in updating_comps_unaffect_bindings]
updating_interfaces_is_well_formed [in updating_interfaces_is_well_formed]
updating_comps_bindings [in updating_comps_bindings]
V
validity [in validity]valid_mk_interfaces [in valid_mk_interfaces]
valid_removing_binding_fact' [in valid_removing_binding_fact']
valid_path_step [in valid_path_step]
valid_binding_lookup_fact [in valid_binding_lookup_fact]
valid_no_id_acc_step [in valid_no_id_acc_step]
valid_interface_path_fact [in valid_interface_path_fact]
valid_binding_dec [in valid_binding_dec]
valid_binding_interface_fact [in valid_binding_interface_fact]
valid_binding_on_same_element_lists [in valid_binding_on_same_element_lists]
valid_rm_comp [in valid_rm_comp]
valid_bindings_correctness [in valid_bindings_correctness]
valid_adding_binding_fact [in valid_adding_binding_fact]
valid_seq_aux [in valid_seq_aux]
valid_component_path_bool_correctness [in valid_component_path_bool_correctness]
valid_removing_binding_fact [in valid_removing_binding_fact]
valid_seq [in valid_seq]
valid_rm_bindings [in valid_rm_bindings]
valid_interface_path_step [in valid_interface_path_step]
valid_component_binding_bool_correctness [in valid_component_binding_bool_correctness]
valid_path_fact' [in valid_path_fact']
valid_mk_comp [in valid_mk_comp]
valid_mk_bindings [in valid_mk_bindings]
valid_binding_fact [in valid_binding_fact]
valid_component_binding_has_valid_component_path [in valid_component_binding_has_valid_component_path]
valid_path_fact [in valid_path_fact]
valid_path_on_non_empty_path_entails_non_empty_components [in valid_path_on_non_empty_path_entails_non_empty_components]
valid_binding_may_entail_false [in valid_binding_may_entail_false]
valid_interface_path_bool_correctness [in valid_interface_path_bool_correctness]
visibility_eq_reflection [in visibility_eq_reflection]
visibility_dec [in visibility_dec]
vis_equality_Prop2bool [in vis_equality_Prop2bool]
vis_equality_bool2Prop' [in vis_equality_bool2Prop']
vis_equality_Prop2bool' [in vis_equality_Prop2bool']
vis_equality_bool2Prop [in vis_equality_bool2Prop]
vis_bool_conjunction_fact [in vis_bool_conjunction_fact]
W
well_formed_empty_component [in well_formed_empty_component]well_formed_removing_component_from_list [in well_formed_removing_component_from_list]
well_formed_component_has_well_formed_interfaces [in well_formed_component_has_well_formed_interfaces]
well_formed_bindings_in_nil [in well_formed_bindings_in_nil]
well_formed_interfaces_dec [in well_formed_interfaces_dec]
well_formed_nil_bindings' [in well_formed_nil_bindings']
well_formed_adding_interface [in well_formed_adding_interface]
well_formed_empty_component' [in well_formed_empty_component']
well_formed_components_have_unique_ids [in well_formed_components_have_unique_ids]
well_formed_subset' [in well_formed_subset']
well_typed_correctness [in well_typed_correctness]
well_formed_component_minus_one_binding [in well_formed_component_minus_one_binding]
well_formed_lookup_split [in well_formed_lookup_split]
well_formed_subset [in well_formed_subset]
well_formed_dec [in well_formed_dec]
well_formed_entail_unique_ids [in well_formed_entail_unique_ids]
well_formed_inheritance [in well_formed_inheritance]
well_formed_component_lc_dec [in well_formed_component_lc_dec]
well_formed_component_dec [in well_formed_component_dec]
well_formed_nil_components [in well_formed_nil_components]
well_formed_adding_bindings [in well_formed_adding_bindings]
well_formed_bindings_dec [in well_formed_bindings_dec]
well_formed_nil_interfaces [in well_formed_nil_interfaces]
well_formed_append' [in well_formed_append']
well_formed_subcomponents_update [in well_formed_subcomponents_update]
well_formed_component_has_subcomponents_w_unique_ids [in well_formed_component_has_subcomponents_w_unique_ids]
well_formed_bindings_w_lookup [in well_formed_bindings_w_lookup]
well_formed_adding_component [in well_formed_adding_component]
well_formed_update_w_add_interface [in well_formed_update_w_add_interface]
well_formed_removing_component [in well_formed_removing_component]
well_formed_update_remove_sub_comps [in well_formed_update_remove_sub_comps]
well_formed_adding_component_interface [in well_formed_adding_component_interface]
well_formed_nil_bindings [in well_formed_nil_bindings]
well_formed_component_cons_dec [in well_formed_component_cons_dec]
well_formed_interface_append [in well_formed_interface_append]
well_formed_component_individuals [in well_formed_component_individuals]
well_formed_bindings_may_entail_false [in well_formed_bindings_may_entail_false]
well_formed_removing_binding_from_list [in well_formed_removing_binding_from_list]
well_formed_bindings_entailment [in well_formed_bindings_entailment]
well_formed_component_nil_dec [in well_formed_component_nil_dec]
well_formed_removing_binding_from_component [in well_formed_removing_binding_from_component]
well_formed_append [in well_formed_append]
well_formed_component_has_well_formed_sub_components [in well_formed_component_has_well_formed_sub_components]
well_formed_tail [in well_formed_tail]
well_formed_removing_bindings [in well_formed_removing_bindings]
well_typed_dec [in well_typed_dec]
Section Index
L
LTL [in LTL]LTL.A_Proof_with_F_Infinite [in A_Proof_with_F_Infinite]
Notation Index
L
_ |= _ [in ::x_'|='_x]other
_ ->idcs (binding_scope) [in :binding_scope:x_'->idcs']_ [ _ ] (binding_scope) [in :binding_scope:x_'['_x_']']
_ == _ (binding_scope) [in :binding_scope:x_'=='_x]
_ ~~ _ (binding_scope) [in :binding_scope:x_'~~'_x]
_ != _ (binding_scope) [in :binding_scope:x_'!='_x]
_ ->idcc (binding_scope) [in :binding_scope:x_'->idcc']
_ ->path (binding_scope) [in :binding_scope:x_'->path']
_ == _ (card_scope) [in :card_scope:x_'=='_x]
_ != _ (card_scope) [in :card_scope:x_'!='_x]
_ ->id (component_scope) [in :component_scope:x_'->id']
_ ->iclass (component_scope) [in :component_scope:x_'->iclass']
_ ->controlLevel (component_scope) [in :component_scope:x_'->controlLevel']
_ == _ (component_scope) [in :component_scope:x_'=='_x]
_ ->itfs (component_scope) [in :component_scope:x_'->itfs']
_ ->subComponents (component_scope) [in :component_scope:x_'->subComponents']
_ ->path (component_scope) [in :component_scope:x_'->path']
_ ->bnds (component_scope) [in :component_scope:x_'->bnds']
_ ->interfaces (component_scope) [in :component_scope:x_'->interfaces']
_ ->bindings (component_scope) [in :component_scope:x_'->bindings']
_ ->subcomps (component_scope) [in :component_scope:x_'->subcomps']
_ != _ (controlLevel_scope) [in :controlLevel_scope:x_'!='_x]
_ == _ (controlLevel_scope) [in :controlLevel_scope:x_'=='_x]
_ == _ (cont_scope) [in :cont_scope:x_'=='_x]
_ != _ (cont_scope) [in :cont_scope:x_'!='_x]
_ == _ (func_scope) [in :func_scope:x_'=='_x]
_ != _ (func_scope) [in :func_scope:x_'!='_x]
_ == _ (implementationClass_scope) [in :implementationClass_scope:x_'=='_x]
_ != _ (implementationClass_scope) [in :implementationClass_scope:x_'!='_x]
_ ->owner (interface_scope) [in :interface_scope:x_'->owner']
_ [ _ ] (interface_scope) [in :interface_scope:x_'['_x_']']
_ ->cardinality (interface_scope) [in :interface_scope:x_'->cardinality']
_ [ _ , _ ] (interface_scope) [in :interface_scope:x_'['_x_','_x_']']
_ ->id (interface_scope) [in :interface_scope:x_'->id']
_ [ _ , _ , _ , _ ] (interface_scope) [in :interface_scope:x_'['_x_','_x_','_x_','_x_']']
_ ->sig (interface_scope) [in :interface_scope:x_'->sig']
_ ->contingency (interface_scope) [in :interface_scope:x_'->contingency']
_ == _ (interface_scope) [in :interface_scope:x_'=='_x]
_ ->visibility (interface_scope) [in :interface_scope:x_'->visibility']
_ ->functionality (interface_scope) [in :interface_scope:x_'->functionality']
_ != _ (interface_scope) [in :interface_scope:x_'!='_x]
_ ->role (interface_scope) [in :interface_scope:x_'->role']
_ [ _ ; _ ] (interface_scope) [in :interface_scope:x_'['_x_';'_x_']']
_ [ _ , _ , _ ] (interface_scope) [in :interface_scope:x_'['_x_','_x_','_x_']']
_ [ _ , _ , _ ] (interface_scope) [in :interface_scope:x_'['_x_','_x_','_x_']']
[ _ ; .. ; _ ] (list_scope) [in :list_scope:'['_x_';'_'..'_';'_x_']']
[ _ ] (list_scope) [in :list_scope:'['_x_']']
_ == _ (list_interface_scope) [in :list_interface_scope:x_'=='_x]
_ == _ (list_binding_scope) [in :list_binding_scope:x_'=='_x]
[ ] (list_scope) [in :list_scope:'['_']']
_ == _ (opt_comp_scope) [in :opt_comp_scope:x_'=='_x]
_ != _ (opt_comp_scope) [in :opt_comp_scope:x_'!='_x]
_ == _ (path_scope) [in :path_scope:x_'=='_x]
_ != _ (path_scope) [in :path_scope:x_'!='_x]
_ != _ (role_scope) [in :role_scope:x_'!='_x]
sym- _ (role_scope) [in :role_scope:'sym-'_x]
_ == _ (role_scope) [in :role_scope:x_'=='_x]
_ != _ (signature_scope) [in :signature_scope:x_'!='_x]
_ == _ (signature_scope) [in :signature_scope:x_'=='_x]
_ ->components (state_scope) [in :state_scope:x_'->components']
_ ->bindings (state_scope) [in :state_scope:x_'->bindings']
sym- _ (vis_scope) [in :vis_scope:'sym-'_x]
_ != _ (vis_scope) [in :vis_scope:x_'!='_x]
_ == _ (vis_scope) [in :vis_scope:x_'=='_x]
_ == _ [in ::x_'=='_x]
_ / _ ~~~> _ / _ [in ::x_'/'_x_'~~~>'_x_'/'_x]
_ [| _ |] [in ::x_'[|'_x_'|]']
_ / _ ~~~>* _ / _ [in ::x_'/'_x_'~~~>*'_x_'/'_x]
_ != _ [in ::x_'!='_x]
_ ; _ [in ::x_';'_x]
_ |= _ [in ::x_'|='_x]
_ |= _ [in ::x_'|='_x]
_ * ( _ , _ ) [in ::x_'*'_'('_x_','_x_')']
_ === _ [in ::x_'==='_x]
_ ->> _ [in ::x_'->>'_x]
_ [| _ |] <- _ [in ::x_'[|'_x_'|]'_'<-'_x]
_ [ _ ] [in ::x_'['_x_']']
new ArrayList
new ArrayList
<< _ , .. , _ >> -> _ [in ::'<<'_x_','_'..'_','_x_'>>'_'->'_x]
[ _ ; .. ; _ ] [in ::'['_x_';'_'..'_';'_x_']']
[ _ / _ ] [in ::'['_x_'/'_x_']']
[ _ ] [in ::'['_x_']']
[ _ \ _ ] [in ::'['_x_'\'_x_']']
[ ] [in ::'['_']']
Constructor Index
A
Action [in Action]AllEmpty [in AllEmpty]
AllStep [in AllStep]
Always_LCons [in Always_LCons]
Assignment [in Assignment]
AssignmentVar [in AssignmentVar]
Atomic_intro [in Atomic_intro]
AttainN [in AttainN]
Attain0 [in Attain0]
B
BindingExists_Step [in BindingExists_Step]BindingExists_Root [in BindingExists_Root]
bisim0 [in bisim0]
bisim1 [in bisim1]
C
CEMI_Bound [in CEMI_Bound]CIMI_Bound [in CIMI_Bound]
Client [in Client]
CoffeeN [in CoffeeN]
Coffee0 [in Coffee0]
Collection [in Collection]
Component [in Component]
Configuration [in Configuration]
Constructor1 [in Constructor1]
Constructor2 [in Constructor2]
Control [in Control]
CrossBinding_Base [in CrossBinding_Base]
CrossBinding_Step [in CrossBinding_Step]
D
Done [in Done]E
Emit [in Emit]Eventually_further [in Eventually_further]
Eventually_here [in Eventually_here]
Export [in Export]
External [in External]
F
Finite_LNil [in Finite_LNil]Finite_LCons [in Finite_LCons]
Functional [in Functional]
G
Gathercast [in Gathercast]GlobalAction [in GlobalAction]
I
Ident [in Ident]IMn [in IMn]
Import [in Import]
IM0 [in IM0]
Infinite_LCons [in Infinite_LCons]
Interface [in Interface]
InterleavingOne [in InterleavingOne]
InterleavingTwo [in InterleavingTwo]
Internal [in Internal]
Introspection [in Introspection]
IsNF [in IsNF]
IsSeq [in IsSeq]
L
LCons [in LCons]LNil [in LNil]
Lowest [in Lowest]
lts_empty_trace [in lts_empty_trace]
LTS_State [in LTS_State]
lts_trace [in lts_trace]
lts_lcons_trace [in lts_lcons_trace]
M
Mandatory [in Mandatory]MapNil [in MapNil]
MapStep [in MapStep]
Message [in Message]
Mk_binding [in Mk_binding]
Mk_interface [in Mk_interface]
mk_arraylist [in mk_arraylist]
Mk_component [in Mk_component]
mk_Net [in mk_Net]
mk_LTS [in mk_LTS]
mk_SingletonNet [in mk_SingletonNet]
Multicast [in Multicast]
N
NetSingleton_State [in NetSingleton_State]net_lcons_trace [in net_lcons_trace]
net_empty_trace [in net_empty_trace]
Net_State [in Net_State]
Next_intro [in Next_intro]
Normal [in Normal]
NotConnected_Step [in NotConnected_Step]
NotInNil [in NotInNil]
NotInPairStep [in NotInPairStep]
NotInPair_Nil [in NotInPair_Nil]
NotInStep [in NotInStep]
O
Optional [in Optional]R
Read [in Read]Rm_component [in Rm_component]
Rm_binding [in Rm_binding]
rsc_step [in rsc_step]
rsc_base [in rsc_base]
S
SDoneRefl [in SDoneRefl]Seq [in Seq]
Server [in Server]
ServerSingleton [in ServerSingleton]
Singleton [in Singleton]
SingletonExport [in SingletonExport]
SingletonNormalImport [in SingletonNormalImport]
SMakeBinding [in SMakeBinding]
SMakeComponent [in SMakeComponent]
SMakeInterface [in SMakeInterface]
SRemoveBinding [in SRemoveBinding]
SRemoveComponent [in SRemoveComponent]
SSeqFinish [in SSeqFinish]
SSeq1 [in SSeq1]
SSeq2 [in SSeq2]
SyncElement [in SyncElement]
SyncVector [in SyncVector]
U
UniquePairs_Base [in UniquePairs_Base]UniquePairs_Step [in UniquePairs_Step]
Unique_Step [in Unique_Step]
Unique_Base [in Unique_Base]
V
Val [in Val]ValidComponentBinding_Base [in ValidComponentBinding_Base]
ValidComponentBinding_Step [in ValidComponentBinding_Step]
ValidInterfacePath_Step [in ValidInterfacePath_Step]
ValidInterfacePath_Base [in ValidInterfacePath_Base]
ValidN [in ValidN]
Valid0 [in Valid0]
Var [in Var]
VCN [in VCN]
VC0 [in VC0]
W
WellFormedComponent [in WellFormedComponent]WellFormedInterfaces_Step [in WellFormedInterfaces_Step]
WellFormedInterfaces_Base [in WellFormedInterfaces_Base]
WildCard [in WildCard]
Inductive Index
A
action [in action]allowed_actions_from_q1q1_coffee [in allowed_actions_from_q1q1_coffee]
all_the_same [in all_the_same]
Always [in Always]
assignment [in assignment]
Atomic [in Atomic]
attainable [in attainable]
awesome_definition [in awesome_definition]
B
binding [in binding]binding_exists' [in binding_exists']
bisimilar [in bisimilar]
C
cardinality [in cardinality]client_internal_mandatory_interfaces_are_bound [in client_internal_mandatory_interfaces_are_bound]
client_singleton_are_bound_once_at_most_normal_import_bindings [in client_singleton_are_bound_once_at_most_normal_import_bindings]
client_singleton_are_bound_once_at_most_export_bindings [in client_singleton_are_bound_once_at_most_export_bindings]
communication_type [in communication_type]
component [in component]
component_is_not_connected' [in component_is_not_connected']
contingency [in contingency]
controlLevel [in controlLevel]
cross_binding' [in cross_binding']
E
Eventually [in Eventually]ext_client_mand_mapping [in ext_client_mand_mapping]
F
Finite [in Finite]functionality [in functionality]
I
ident [in ident]indexed_membership [in indexed_membership]
Infinite [in Infinite]
interface [in interface]
interleaving [in interleaving]
L
LList [in LList]lts_state [in lts_state]
LTS_Trace [in LTS_Trace]
M
message [in message]N
Net [in Net]net_state [in net_state]
Net_Trace [in Net_Trace]
Next [in Next]
not_in_l_pairs [in not_in_l_pairs]
not_sequence [in not_sequence]
not_in_l [in not_in_l]
O
operation [in operation]P
parameter [in parameter]R
refl_step_closure [in refl_step_closure]role [in role]
S
server_singleton_are_bound_once_at_most [in server_singleton_are_bound_once_at_most]step [in step]
subcomponents_client_external_mandatory_interfaces_are_bound [in subcomponents_client_external_mandatory_interfaces_are_bound]
SynchronizationVector [in SynchronizationVector]
SyncronizationElement [in SyncronizationElement]
SyncronizationOutput [in SyncronizationOutput]
U
unique_ids [in unique_ids]unique_pairs [in unique_pairs]
V
valid_interface_path' [in valid_interface_path']valid_path [in valid_path]
valid_component_binding' [in valid_component_binding']
valid_coffee_combination [in valid_coffee_combination]
visibility [in visibility]
W
well_formed_interfaces [in well_formed_interfaces]well_formed_component [in well_formed_component]
Definition Index
A
act [in act]actions [in actions]
acts [in acts]
add_binding [in add_binding]
add_interface [in add_interface]
alter [in alter]
alter2 [in alter2]
annotation_example [in annotation_example]
AnotherSimpleArchitecture [in AnotherSimpleArchitecture]
AnotherSimpleArchitecture' [in AnotherSimpleArchitecture']
Arch_is_Sound [in Arch_is_Sound]
Arch_is_Sound_After_Removal' [in Arch_is_Sound_After_Removal']
Arch_is_Sound' [in Arch_is_Sound']
Arch_is_Sound_After_Removal [in Arch_is_Sound_After_Removal]
asgns [in asgns]
assignments [in assignments]
B
beq_opt_comp [in beq_opt_comp]beq_comp [in beq_comp]
beq_component [in beq_component]
beq_message [in beq_message]
beq_signature [in beq_signature]
binding_exists [in binding_exists]
binding_is_not_a_duplicate [in binding_is_not_a_duplicate]
bind_system [in bind_system]
bisimulation [in bisimulation]
bneq_ident [in bneq_ident]
body [in body]
body_transitions [in body_transitions]
body_init [in body_init]
body_states [in body_states]
body_actions [in body_actions]
body_mem [in body_mem]
bool_dec [in bool_dec]
BrightComp [in BrightComp]
BRINFOCOLL [in BRINFOCOLL]
build_running_example [in build_running_example]
build_C [in build_C]
build_N [in build_N]
build_S [in build_S]
b1 [in b1]
b2 [in b2]
b3 [in b3]
b4 [in b4]
b5 [in b5]
b6 [in b6]
b7 [in b7]
C
C [in C]cim_itfs_bound_correctness [in cim_itfs_bound_correctness]
client_singleton_are_bound_once_at_most [in client_singleton_are_bound_once_at_most]
client_singleton_are_bound_once_at_most_export_bindings_bool [in client_singleton_are_bound_once_at_most_export_bindings_bool]
client_internal_mandatory_itfs_are_bound [in client_internal_mandatory_itfs_are_bound]
client_singleton_are_bound_once_at_most_normal_import_bindings_bool [in client_singleton_are_bound_once_at_most_normal_import_bindings_bool]
client_internal_mandatory_interfaces_are_bound_bool [in client_internal_mandatory_interfaces_are_bound_bool]
client_internal_mandatory_itfs_are_bound_bool [in client_internal_mandatory_itfs_are_bound_bool]
component_eq_dec [in component_eq_dec]
component_is_not_connected [in component_is_not_connected]
Composite [in Composite]
CompositePath [in CompositePath]
cpath [in cpath]
cross_normal [in cross_normal]
cross_export [in cross_export]
cross_binding [in cross_binding]
cross_import [in cross_import]
D
dec [in dec]dec_component [in dec_component]
dec_state [in dec_state]
default_class [in default_class]
digit_of_nat [in digit_of_nat]
E
empty_state [in empty_state]eq [in eq]
eqServerSingleton [in eqServerSingleton]
eqSingleton_export [in eqSingleton_export]
eqSingleton_normal_import [in eqSingleton_normal_import]
eqType [in eqType]
eqType' [in eqType']
eq_action [in eq_action]
ErrorIdent [in ErrorIdent]
eval [in eval]
F
fold_left2 [in fold_left2]forever [in forever]
from [in from]
F_Infinite [in F_Infinite]
F_Infinite_2_Eventually [in F_Infinite_2_Eventually]
F_from [in F_from]
f_aux [in f_aux]
G
gcm_component [in gcm_component]general_omega [in general_omega]
get_binding_server_id [in get_binding_server_id]
get_subComponent [in get_subComponent]
get_binding_client_id [in get_binding_client_id]
get_component_with_path [in get_component_with_path]
get_parent [in get_parent]
G_Infinite [in G_Infinite]
I
IdentDefinitionExample.BarVariable [in BarVariable]IdentDefinitionExample.FooVariable [in FooVariable]
IdentDefinitionExample.XyzVariable [in XyzVariable]
IdentProofExamples.warm_up_proof' [in warm_up_proof']
IdentProofExamples.warm_up_proof [in warm_up_proof]
IdentProofExamples.x [in x]
IdentProofExamples.y [in y]
implementationClass [in implementationClass]
induction_example [in induction_example]
init_net_state [in init_net_state]
interelaving_test' [in interelaving_test']
interelaving_test [in interelaving_test]
interfaces_BRINFOCOLL [in interfaces_BRINFOCOLL]
interfaces_LightControlComp [in interfaces_LightControlComp]
interfaces_in_example_are_bound [in interfaces_in_example_are_bound]
interfaces_SwonLights [in interfaces_SwonLights]
interfaces_LightComp [in interfaces_LightComp]
interfaces_LCC [in interfaces_LCC]
interfaces_BrightComp [in interfaces_BrightComp]
interfaces_SensedBrInfo [in interfaces_SensedBrInfo]
isEmpty [in isEmpty]
isServerExternalSingleton [in isServerExternalSingleton]
isServerInternalSingleton [in isServerInternalSingleton]
is_normal_form [in is_normal_form]
is_seq [in is_seq]
is_one_step_from_normal_form [in is_one_step_from_normal_form]
J
jmx [in jmx]jmx_actions [in jmx_actions]
jmx_states [in jmx_states]
jmx_transitions [in jmx_transitions]
jmx_init [in jmx_init]
L
LAppend [in LAppend]LCC [in LCC]
LHead [in LHead]
LightComp [in LightComp]
LightControlComp [in LightControlComp]
LightsControlUseCaseArchitecture [in LightsControlUseCaseArchitecture]
list_dec [in list_dec]
LList_decompose_n [in LList_decompose_n]
LList_decompose [in LList_decompose]
LNth [in LNth]
LTail [in LTail]
lts_target_state [in lts_target_state]
lts_states [in lts_states]
M
makeCoffeeOrder [in makeCoffeeOrder]makeSandwichOrder [in makeSandwichOrder]
mandatory_interfaces_are_bound [in mandatory_interfaces_are_bound]
mandatory_interfaces_are_bound_bool [in mandatory_interfaces_are_bound_bool]
masterlts [in masterlts]
MasterSlaveCoffeeNet [in MasterSlaveCoffeeNet]
master_ready_act [in master_ready_act]
master_sts [in master_sts]
master_acts [in master_acts]
master_order_acts [in master_order_acts]
mem [in mem]
mem [in mem]
Mk_symmetric_interface [in Mk_symmetric_interface]
mst0 [in mst0]
mst1 [in mst1]
N
N [in N]Nats [in Nats]
nat_to_string [in nat_to_string]
net_target_states [in net_target_states]
not_in_list_pairs [in not_in_list_pairs]
not_in_list [in not_in_list]
not_nil [in not_nil]
not_binded [in not_binded]
no_id_acc_clash [in no_id_acc_clash]
no_clash_on_generation [in no_clash_on_generation]
no_id_clash [in no_id_clash]
no_id_clash' [in no_id_clash']
no_id_acc_clash' [in no_id_acc_clash']
O
omega [in omega]P
parameters [in parameters]path [in path]
pN [in pN]
Primitive [in Primitive]
primitive [in primitive]
PrimitiveA [in PrimitiveA]
PrimitiveAPath [in PrimitiveAPath]
PrimitiveB [in PrimitiveB]
PrimitivePath [in PrimitivePath]
process_assignment [in process_assignment]
projectionBindingClientPath [in projectionBindingClientPath]
projectionBindingIntId [in projectionBindingIntId]
projectionBindingIntId2 [in projectionBindingIntId2]
projectionBindingSubComponent [in projectionBindingSubComponent]
projectionComponentBindings [in projectionComponentBindings]
projectionComponentControlLevel [in projectionComponentControlLevel]
projectionComponentId [in projectionComponentId]
projectionComponentImplementationClass [in projectionComponentImplementationClass]
projectionComponentInterfaces [in projectionComponentInterfaces]
projectionComponentPath [in projectionComponentPath]
projectionComponentSubComponents [in projectionComponentSubComponents]
projectionInterfaceCardinality [in projectionInterfaceCardinality]
projectionInterfaceContingency [in projectionInterfaceContingency]
projectionInterfaceFunctionality [in projectionInterfaceFunctionality]
projectionInterfaceId [in projectionInterfaceId]
projectionInterfaceOwner [in projectionInterfaceOwner]
projectionInterfaceRole [in projectionInterfaceRole]
projectionInterfaceSignature [in projectionInterfaceSignature]
projectionInterfaceVisibility [in projectionInterfaceVisibility]
projectionNormalBindingComp1Id [in projectionNormalBindingComp1Id]
projectionNormalBindingComp2Id [in projectionNormalBindingComp2Id]
projectionNormalBindingInt1Id [in projectionNormalBindingInt1Id]
projectionNormalBindingInt2Id [in projectionNormalBindingInt2Id]
projStateBindings [in projStateBindings]
projStateComponents [in projStateComponents]
p1 [in p1]
p2 [in p2]
Q
queue [in queue]queue_mem [in queue_mem]
queue_transitions [in queue_transitions]
queue_actions [in queue_actions]
queue_states [in queue_states]
queue_init [in queue_init]
q0 [in q0]
q1 [in q1]
R
R [in R]ready_to_start [in ready_to_start]
receiveCoffeeOrder [in receiveCoffeeOrder]
receiveSandwichOrder [in receiveSandwichOrder]
relation [in relation]
RemoveBinding [in RemoveBinding]
RemoveComponent [in RemoveComponent]
remove_binding [in remove_binding]
Rma [in Rma]
root [in root]
root [in root]
S
S [in S]satisfies [in satisfies]
SensedBrInfo [in SensedBrInfo]
server_singleton_are_bound_once_at_most_bool [in server_singleton_are_bound_once_at_most_bool]
server_singleton_are_bound_once_at_most_bool_one [in server_singleton_are_bound_once_at_most_bool_one]
signature [in signature]
SimpleArchitecture [in SimpleArchitecture]
simplelts [in simplelts]
simplenet [in simplenet]
simpleProof_Revisited [in simpleProof_Revisited]
slavelts [in slavelts]
slave_acts [in slave_acts]
slave_sts [in slave_sts]
slave_ready_act [in slave_ready_act]
slave_order_acts [in slave_order_acts]
slv0 [in slv0]
slv1 [in slv1]
sound_contingency_bool [in sound_contingency_bool]
sound_contigency_correctness [in sound_contigency_correctness]
sound_cardinality_correctness [in sound_cardinality_correctness]
sound_cardinality [in sound_cardinality]
sound_contingency [in sound_contingency]
sound_cardinality_bool [in sound_cardinality_bool]
spath [in spath]
Squares_from [in Squares_from]
state [in state]
state_mem [in state_mem]
stay_in_state [in stay_in_state]
string_of_nat [in string_of_nat]
sts [in sts]
subcomponents_client_external_mandatory_interfaces_are_bound_bool [in subcomponents_client_external_mandatory_interfaces_are_bound_bool]
SwonLights [in SwonLights]
symmetric_visibility [in symmetric_visibility]
symmetric_role [in symmetric_role]
synch_vectors [in synch_vectors]
synch_vectors [in synch_vectors]
sync_vectors [in sync_vectors]
sync_notation [in sync_notation]
system_binding [in system_binding]
s0 [in s0]
T
transitions [in transitions]trs [in trs]
two_simplenet [in two_simplenet]
two_simplelts [in two_simplelts]
U
unique_ids' [in unique_ids']V
valid_interface_path [in valid_interface_path]valid_binding [in valid_binding]
valid_component_binding [in valid_component_binding]
valid_cross_binding [in valid_cross_binding]
valid_component_path [in valid_component_path]
W
well_formed_components [in well_formed_components]well_formed_bindings [in well_formed_bindings]
well_formed [in well_formed]
well_formed_bool [in well_formed_bool]
well_typed [in well_typed]
well_typed_bool [in well_typed_bool]
well_formed_interfaces' [in well_formed_interfaces']
Axiom Index
B
binding_type_dec [in binding_type_dec]I
iclC [in iclC]iclS [in iclS]
N
nat_to_string_fact [in nat_to_string_fact]P
p [in p]S
sigC1 [in sigC1]sigC2 [in sigC2]
sigC3 [in sigC3]
sigS1 [in sigS1]
sigS2 [in sigS2]
sigS3 [in sigS3]
Module Index
I
IdentDefinitionExample [in IdentDefinitionExample]IdentProofExamples [in IdentProofExamples]
InstantiatedExample [in InstantiatedExample]
Variable Index
L
LTL.A_Proof_with_F_Infinite.A [in A]LTL.A_Proof_with_F_Infinite.P [in P]
LTL.A_Proof_with_F_Infinite.a [in a]
LTL.A_Proof_with_F_Infinite.b [in b]
LTL.A_Proof_with_F_Infinite.c [in c]
LTL.A_Proof_with_F_Infinite.w [in w]
LTL.A_Proof_with_F_Infinite.w_omega [in w_omega]
Library Index
A
AutonomicUseCaseB
BaseBatteries
Binding
C
CardinalityDecidabilityCoInductionLib
Compliance
Component
ContingencyDecidability
CoreElementsFacts
E
EvalExamples
F
FunctionalSpecG
GCMExampleGCMSpec
GCMTyping
GCMWellFormedness
H
HeavyLiftingI
InterfaceL
LTLLTS
M
MasterSlaveCoffeeN
NetP
ParamSpecR
ReductionsS
SemanticsT
ThesisRunningExampleTraceExamples
W
WellFormednessDecidabilityWellTypedDecidability
| 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 | (1094 entries) |
| Projection Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (7 entries) |
| Record Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (2 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 | (488 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 | (2 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 | (85 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 | (120 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 | (60 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 | (279 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 | (11 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 | (3 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 | (7 entries) |
| Library Index | A | B | C | D | E | F | G | H | I | J | K | L | M | N | O | P | Q | R | S | T | U | V | W | X | Y | Z | _ | other | (30 entries) |
This page has been generated by coqdoc