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 (578 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 (29 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 (6 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 (21 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 (375 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 (48 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 (18 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 (7 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 (3 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 (70 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 (1 entry)

Global Index

A

all_rounds_inhabited [lemma, in Round]
ancestor [definition, in Hashgraph]
ancestor_sees [lemma, in Sees]
ancestor_impl_spawn_le [lemma, in Consensus]
ancestor_realtime [lemma, in Hashgraph]
ancestor_witness [lemma, in Round]
ancestor_decide [lemma, in HashgraphFacts]
ancestor_finite [lemma, in HashgraphFacts]
ancestor_initial [lemma, in HashgraphFacts]
arbitrary_peer [lemma, in HashgraphFacts]
atleasthalf [definition, in Majority]
atleasthalf_le_all [lemma, in Calculate]
average_range [lemma, in Calculate]


C

Calculate [library]
car [definition, in Tact]
cardinality [definition, in Cardinality]
Cardinality [library]
cardinality_lt_by_contradiction [lemma, in Cardinality]
cardinality_lt_impl_lt [lemma, in Cardinality]
cardinality_lt_increase [lemma, in Cardinality]
cardinality_impl_cardinality_lt [lemma, in Cardinality]
cardinality_lt [definition, in Cardinality]
cardinality_gt_decide [lemma, in Cardinality]
cardinality_finite [lemma, in Cardinality]
cardinality_tabulate [lemma, in Cardinality]
cardinality_image [lemma, in Cardinality]
cardinality_incl [lemma, in Cardinality]
cardinality_map_surj [lemma, in Cardinality]
cardinality_map_inj [lemma, in Cardinality]
cardinality_corr_eq [lemma, in Cardinality]
cardinality_corr_le [lemma, in Cardinality]
cardinality_difference [lemma, in Cardinality]
cardinality_partition [lemma, in Cardinality]
cardinality_sum [lemma, in Cardinality]
cardinality_subset [lemma, in Cardinality]
cardinality_nonempty [lemma, in Cardinality]
cardinality_empty' [lemma, in Cardinality]
cardinality_iff [lemma, in Cardinality]
cardinality_fun [lemma, in Cardinality]
cardinality_In [lemma, in Cardinality]
cardinality_singleton [lemma, in Cardinality]
cardinality_empty [lemma, in Cardinality]
cdr [definition, in Tact]
coin [axiom, in Hashgraph]
coin_freq_min [axiom, in Hashgraph]
coin_freq [axiom, in Hashgraph]
compose [definition, in Relation]
Consensus [library]
corder [definition, in Order]
corder_support_finite [lemma, in Order]
corder_support [lemma, in Order]
corder_stable [lemma, in Order]
corder_refl [lemma, in Order]
corder_total [lemma, in Order]
corder_trans [lemma, in Order]
corder_antisym [lemma, in Order]
creator [axiom, in Hashgraph]
creatorstake [definition, in Vote]
cumulative_decisions_support [lemma, in Received]


D

Decide [library]
decision [definition, in Decision]
Decision [library]
decisions_propagate_round [lemma, in Decision]
decisions_propagate [lemma, in Decision]
decisions_support [lemma, in Received]
decision_consistent [lemma, in Decision]
decision_vote_consistent [lemma, in Decision]
decision_decide [lemma, in Decision]
decision_fun [lemma, in Decision]
decision_ancestor [lemma, in Famous]
dec_forall_imp_finite [lemma, in Decide]
dec_exists_finite [lemma, in Decide]
dec_equiv [lemma, in Decide]
dec_and_dep [lemma, in Decide]
dec_In [lemma, in Decide]
deduplicate [lemma, in Cardinality]
deduplicate [lemma, in Weight]
destruct_election' [lemma, in Decision]
destruct_election [lemma, in Decision]
distinct_honest_peers [axiom, in Hashgraph]
distinct_peer [lemma, in HashgraphFacts]
div3_one_third [lemma, in Calculate]


E

earlier [definition, in Round]
earlier_trans [lemma, in Round]
earlier_rounds [lemma, in Round]
earliest_observer_impl_self_ancestor [lemma, in Order]
earliest_observer [definition, in Order]
earliest_observer_defined [lemma, in Timestamp]
earliest_observer_fun [lemma, in Timestamp]
election [definition, in Vote]
election_fun [lemma, in Decision]
election_defined' [lemma, in Vote]
election_defined [lemma, in Vote]
election_fun_gen [lemma, in Vote]
elector [definition, in Vote]
elector_vote_peer [lemma, in Decision]
elector_minimum [lemma, in Decision]
elector_unique [lemma, in Decision]
elector_rwitness [lemma, in Decision]
elector_weight [lemma, in Vote]
elector_decide [lemma, in Vote]
elector_cardinality [lemma, in Famous]
eligible_voter_maximum [lemma, in Consensus]
enumerate_subset [lemma, in Cardinality]
enumerate_subset [lemma, in Weight]
eq_fn_apply [lemma, in Tact]
eq_event_decide [lemma, in HashgraphFacts]
eq_peer_decide [lemma, in HashgraphFacts]
event [axiom, in Hashgraph]
EventMedian [module, in Median]
events_reach_every_world [lemma, in Progress]
events_are_received [lemma, in Progress]
eventual_agreement [axiom, in Hashgraph]
EventWeightAndValue [module, in Median]
EventWeightAndValue.eqT_decide [definition, in Median]
EventWeightAndValue.inh [definition, in Median]
EventWeightAndValue.lebU [definition, in Median]
EventWeightAndValue.lebU_total [definition, in Median]
EventWeightAndValue.lebU_order [lemma, in Median]
EventWeightAndValue.T [definition, in Median]
EventWeightAndValue.U [definition, in Median]
EventWeightAndValue.vl [definition, in Median]
EventWeightAndValue.wt [definition, in Median]
EventWeightAndValue.wt_pos [lemma, in Median]
event_broadcast [lemma, in Progress]
event_transmit [lemma, in Progress]
event_eq_dec [axiom, in Hashgraph]
event_world [lemma, in HashgraphFacts]
every [definition, in Majority]
extends [definition, in Hashgraph]
extends_famous [lemma, in Famous]
extends_ufwitness [lemma, in Received]
extends_fwitness [lemma, in Received]


F

fairness [lemma, in Fairness]
Fairness [library]
fame_reaches_every_world [lemma, in Famous]
fame_consensus [lemma, in Consensus]
famous [definition, in Famous]
Famous [library]
famous_member [lemma, in Famous]
famous_decide_nonterm [lemma, in Famous]
famous_decide_finite [lemma, in Famous]
famous_witness_exists [lemma, in Fairness]
filter_to_finite [lemma, in Decide]
finite [definition, in Decide]
finite_cardinality [lemma, in Cardinality]
finite_weight [lemma, in Weight]
finite_exists [lemma, in Decide]
finite_star [lemma, in Decide]
finite_plus [lemma, in Decide]
finite_subset' [lemma, in Decide]
finite_subset [lemma, in Decide]
finite_equiv [lemma, in Decide]
finite_decide [lemma, in Decide]
first_witness_exists [lemma, in Consensus]
first_witness_realtime [lemma, in Consensus]
first_witness_fun [lemma, in Consensus]
first_witness [definition, in Consensus]
first_regular_min [axiom, in Hashgraph]
first_regular [axiom, in Hashgraph]
fold_right_ext_in [lemma, in Weight]
fold_right_map [lemma, in Weight]
Forall_app [lemma, in Median]
fork [definition, in Hashgraph]
fork_decide [lemma, in HashgraphFacts]
fork_creator [lemma, in HashgraphFacts]
fork_symm [lemma, in HashgraphFacts]
four_thirds_le [lemma, in Calculate]
fwitness [definition, in Famous]
fwitness_stable [lemma, in Order]
fwitness_finite_global [lemma, in Received]
fwitness_finite_finite [lemma, in Received]
fwitness_ufwitness_finite [lemma, in Received]
fwitness_finite_global_if [lemma, in Fairness]
fwitness_finite_nonterm_if [lemma, in Fairness]


G

global [definition, in Hashgraph]
global_nonterminating [lemma, in Progress]
good_coins [lemma, in Consensus]


H

half_supermajority [lemma, in Calculate]
Hashgraph [library]
HashgraphFacts [library]
honest [axiom, in Hashgraph]
honest_event_exists [lemma, in Progress]
honest_peers_sync [axiom, in Hashgraph]
honest_timestamp [lemma, in Timestamp]
honest_witness_unique [lemma, in Round]
honest_decide [lemma, in HashgraphFacts]


I

incl [definition, in Decide]
inclusion_exclusion [lemma, in Cardinality]
inclusion_exclusion [lemma, in Weight]
incl_weight [lemma, in Weight]
incl_every [lemma, in Majority]
initial [definition, in Hashgraph]
initial_decide [axiom, in Hashgraph]
initial_no_self_parent [lemma, in HashgraphFacts]
initial_no_parent [lemma, in HashgraphFacts]
inj_pair2_UIP [lemma, in Tact]
Is_true_decide [lemma, in Decide]


L

list_minimum [lemma, in Timestamp]


M

majority [definition, in Majority]
Majority [library]
majority_complement [lemma, in Calculate]
majority_atleasthalf_intersect_calculation [lemma, in Calculate]
majority_intersect_calculation [lemma, in Calculate]
majority_inhabitant [lemma, in Majority]
majority_decide [lemma, in Majority]
majority_atleasthalf_intersect [lemma, in Majority]
majority_intersect [lemma, in Majority]
majority_enlarge [lemma, in Majority]
majority_impl_superminority [lemma, in Majority]
majority_incl [lemma, in Majority]
map_sorted [lemma, in Median]
Marker_invert [definition, in Tact]
maximum_votes [lemma, in Vote]
Median [library]
MedianFun [module, in Median]
MedianFun.eqU_decide [lemma, in Median]
MedianFun.leT [definition, in Median]
MedianFun.leU [definition, in Median]
MedianFun.leU_decide [lemma, in Median]
MedianFun.leU_total [lemma, in Median]
MedianFun.leU_order [lemma, in Median]
MedianFun.majority_median [lemma, in Median]
MedianFun.median [definition, in Median]
MedianFun.median_spec [lemma, in Median]
MedianFun.median_unique [lemma, in Median]
MedianFun.select [definition, in Median]
MedianFun.select_spec [lemma, in Median]
MedianFun.select_unique [lemma, in Median]
MedianFun.sselect [definition, in Median]
MedianFun.sselect_eq_select [lemma, in Median]
MedianFun.sselect_unique [lemma, in Median]
MedianFun.sselect_lift [lemma, in Median]
MedianFun.sselect_app_r [lemma, in Median]
MedianFun.sselect_cons_r [lemma, in Median]
MedianFun.sselect_prefix [lemma, in Median]
MedianFun.TOrder [module, in Median]
MedianFun.TOrder.leb [definition, in Median]
MedianFun.TOrder.leb_total [lemma, in Median]
MedianFun.TOrder.t [definition, in Median]
MedianFun.Transitive_leT [lemma, in Median]
MedianFun.TSort [module, in Median]
MedianFun.tsort_sorted [lemma, in Median]
member [projection, in Hashgraph]
minimal_witness' [lemma, in Fairness]
minimal_witness [lemma, in Fairness]
mk_world [constructor, in Hashgraph]
mod3_2 [lemma, in Calculate]
mod3_1 [lemma, in Calculate]
mod3_0 [lemma, in Calculate]


N

neq_negb [lemma, in Consensus]
NoDup_app [lemma, in Cardinality]
NoDup_weight_incl [lemma, in Weight]
NoDup_app [lemma, in Weight]
NoDup_app_invert [lemma, in Median]
nonempty [definition, in Received]
nonterminating [definition, in Round]
nonterminating_nonempty [lemma, in Received]
not_supermajority_every [lemma, in Majority]
not_supermajority [lemma, in Majority]
no_late_fame_world [lemma, in Famous]
no_late_fame [lemma, in Famous]
no_true_votes_election [lemma, in Famous]
no_orphans [axiom, in Hashgraph]
no_majority_stake [axiom, in Hashgraph]
number_of_peers [axiom, in Hashgraph]
number_peers_minimum [axiom, in Hashgraph]
number_peers [axiom, in Hashgraph]


O

obtain_ufwitness [lemma, in Timestamp]
offer [definition, in Decision]
one_half_plus_two [lemma, in Calculate]
one_third_mono [lemma, in Calculate]
one_third [definition, in Calculate]
one_half [definition, in Calculate]
Order [library]


P

parent [inductive, in Hashgraph]
parents [axiom, in Hashgraph]
parents_creator [axiom, in Hashgraph]
parents_fun [axiom, in Hashgraph]
parents_self_parent [lemma, in HashgraphFacts]
parent_well_founded [axiom, in Hashgraph]
parent_finite [lemma, in HashgraphFacts]
parent_decide [lemma, in HashgraphFacts]
parent1 [constructor, in Hashgraph]
parent2 [constructor, in Hashgraph]
peer [axiom, in Hashgraph]
peer_vote_offer [lemma, in Decision]
peer_vote_elector [lemma, in Decision]
peer_vote [definition, in Decision]
peer_eq_dec [axiom, in Hashgraph]
permutation_length [lemma, in Cardinality]
permutation_weight' [lemma, in Weight]
permutation_weight [lemma, in Weight]
pigeonhole [lemma, in Cardinality]
plus [definition, in Relation]
plusi [inductive, in Relation]
plusi_plus [lemma, in Relation]
plusi_step [constructor, in Relation]
plusi_one [constructor, in Relation]
plusr [definition, in Relation]
plusri [inductive, in Relation]
plusri_plus [lemma, in Relation]
plusri_step [constructor, in Relation]
plusri_one [constructor, in Relation]
plusr_plus [lemma, in Relation]
plus_two_no_coin [lemma, in Consensus]
plus_ind_r [lemma, in Relation]
plus_ind [lemma, in Relation]
plus_well_founded [lemma, in Relation]
plus_of_transitive [lemma, in Relation]
plus_idem [lemma, in Relation]
plus_mono_map [lemma, in Relation]
plus_map' [lemma, in Relation]
plus_mono [lemma, in Relation]
plus_step [lemma, in Relation]
plus_plusri [lemma, in Relation]
plus_plusi [lemma, in Relation]
plus_star_trans [lemma, in Relation]
plus_transitive [lemma, in Relation]
plus_trans [lemma, in Relation]
plus_plusr [lemma, in Relation]
plus_one [lemma, in Relation]
plus_star [lemma, in Relation]
Progress [library]


R

realtime [definition, in Hashgraph]
realtime_impl_self_ancestor [lemma, in Progress]
realtime_spawn_impl_leq [lemma, in Consensus]
realtime_refl_spawn [lemma, in Consensus]
realtime_parent [lemma, in Hashgraph]
realtime_antisym [lemma, in Hashgraph]
realtime_trans [lemma, in Hashgraph]
realtime_member [lemma, in Hashgraph]
realtime_before [definition, in HashgraphFacts]
received [definition, in Received]
Received [library]
received_impl_time_received [lemma, in Order]
received_support [lemma, in Received]
received_by_support [lemma, in Received]
received_cumulative [lemma, in Received]
received_consistent [lemma, in Received]
received_by_consistent [lemma, in Received]
received_defined [lemma, in Received]
received_by_exists [lemma, in Received]
received_by_decide [lemma, in Received]
received_by_global [lemma, in Received]
received_fun [lemma, in Received]
received_by_inhabited [lemma, in Received]
received_by [definition, in Received]
Relation [library]
round [inductive, in Round]
Round [library]
rounds_earlier [lemma, in Round]
round_advanced [lemma, in Progress]
round_decide [lemma, in Round]
round_defined [lemma, in Round]
round_mono [lemma, in Round]
round_fun [lemma, in Round]
round_advance [constructor, in Round]
round_nadvance [constructor, in Round]
round_initial [constructor, in Round]
rwitness [definition, in Round]
rwitness_decide [lemma, in Round]
rwitness_earlier [lemma, in Round]
rwitness_fun [lemma, in Round]
rwitness_witness [lemma, in Round]


S

sample [axiom, in Hashgraph]
sees [definition, in Sees]
Sees [library]
sees_decide [lemma, in Sees]
sees_impl_ancestor [lemma, in Sees]
self_ancestor_stsees_trans [lemma, in Sees]
self_ancestor_sees_trans [lemma, in Sees]
self_ancestor [definition, in Hashgraph]
self_parent [definition, in Hashgraph]
self_ancestor_witness [lemma, in Round]
self_ancestor_total' [lemma, in HashgraphFacts]
self_ancestor_total [lemma, in HashgraphFacts]
self_ancestor_decide [lemma, in HashgraphFacts]
self_ancestor_creator [lemma, in HashgraphFacts]
self_parent_well_founded [lemma, in HashgraphFacts]
self_ancestor_impl_ancestor [lemma, in HashgraphFacts]
self_parent_decide [lemma, in HashgraphFacts]
self_parent_creator [lemma, in HashgraphFacts]
self_parent_fun [lemma, in HashgraphFacts]
self_parent_impl_parent [lemma, in HashgraphFacts]
similar [definition, in Hashgraph]
similar_first_witness [lemma, in Consensus]
similar_vote [lemma, in Consensus]
similar_election [lemma, in Consensus]
similar_symm [lemma, in Consensus]
similar_weaken [lemma, in Consensus]
sorted_impl [lemma, in Median]
sorted_unique [lemma, in Median]
spawn [axiom, in Hashgraph]
spawn_forks [axiom, in Hashgraph]
spawn_parent [axiom, in Hashgraph]
spawn_inj [axiom, in Hashgraph]
stake [axiom, in Hashgraph]
stake_positive [axiom, in Hashgraph]
star [inductive, in Relation]
starr [inductive, in Relation]
starr_star [lemma, in Relation]
starr_step [constructor, in Relation]
starr_refl [constructor, in Relation]
star_mono_map [lemma, in Relation]
star_map' [lemma, in Relation]
star_plus_trans [lemma, in Relation]
star_neq_plus [lemma, in Relation]
star_plus [lemma, in Relation]
star_starr [lemma, in Relation]
star_map [lemma, in Relation]
star_mono [lemma, in Relation]
star_stepr [lemma, in Relation]
star_one [lemma, in Relation]
star_transitive [lemma, in Relation]
star_trans [lemma, in Relation]
star_step [constructor, in Relation]
star_refl [constructor, in Relation]
strict_ancestor_impl_spawn_lt [lemma, in Consensus]
strict_self_ancestor [definition, in Hashgraph]
strict_ancestor [definition, in Hashgraph]
strict_self_ancestor_witness [lemma, in Round]
strict_ancestor_decide [lemma, in HashgraphFacts]
strict_ancestor_finite [lemma, in HashgraphFacts]
strict_ancestor_irreflex [lemma, in HashgraphFacts]
strict_ancestor_initial [lemma, in HashgraphFacts]
strict_self_ancestor_parent [lemma, in HashgraphFacts]
strict_ancestor_parents [lemma, in HashgraphFacts]
strict_ancestor_well_founded [lemma, in HashgraphFacts]
strict_self_ancestor_impl_strict_ancestor [lemma, in HashgraphFacts]
strongly_sorted_remove_middle [lemma, in Median]
strongly_sorted_app_inv [lemma, in Median]
strongly_seeing [lemma, in Sees]
stseen_witness_unique [lemma, in Round]
stsees [definition, in Sees]
stsees_ancestor_trans [lemma, in Sees]
stsees_decide [lemma, in Sees]
stsees_impl_ancestor [lemma, in Sees]
stsees_impl_strict_ancestor [lemma, in Sees]
stsees_many_witnesses [lemma, in Round]
stsees_impl_famous [lemma, in Fairness]
stsees_impl_famous_pre [lemma, in Fairness]
succ_no_coin [lemma, in Decision]
sumweight [definition, in Weight]
sumweight_app [lemma, in Weight]
sumweight_cons [lemma, in Weight]
supermajority [definition, in Majority]
supermajority_intersect_3_calculation [lemma, in Calculate]
supermajority_intersect_2_calculation [lemma, in Calculate]
supermajority_honest [axiom, in Hashgraph]
supermajority_inhabitant [lemma, in Majority]
supermajority_decide [lemma, in Majority]
supermajority_intersect_3 [lemma, in Majority]
supermajority_intersect_2' [lemma, in Majority]
supermajority_intersect_2 [lemma, in Majority]
supermajority_iff [lemma, in Majority]
supermajority_enlarge [lemma, in Majority]
supermajority_impl_majority [lemma, in Majority]
superminority [definition, in Majority]
superminority_supermajority_intersect_calculation [lemma, in Calculate]
superminority_supermajority_intersect [lemma, in Majority]


T

Tact [library]
textorder [axiom, in Hashgraph]
textorder_total [axiom, in Hashgraph]
textorder_order [axiom, in Hashgraph]
textorder_decide [lemma, in HashgraphFacts]
the_total_stake [axiom, in Hashgraph]
timestamp [axiom, in Hashgraph]
Timestamp [library]
time_received_consistent [lemma, in Order]
time_received_defined [lemma, in Order]
time_received_fun [lemma, in Order]
time_received [definition, in Order]
too_many_voters_honest [lemma, in Consensus]
too_many_voters_elector [lemma, in Consensus]
too_many_voters [lemma, in Consensus]
total_stake [axiom, in Hashgraph]
two_thirds_of_three [lemma, in Calculate]
two_thirds_shift [lemma, in Calculate]
two_thirds_mono [lemma, in Calculate]
two_thirds_lt [lemma, in Calculate]
two_thirds [definition, in Calculate]


U

ufwitness [definition, in Received]
ufwitness_stable [lemma, in Order]
ufwitness_fun [lemma, in Timestamp]
ufwitness_finite_global [lemma, in Received]
ufwitness_finite_finite [lemma, in Received]
unanimity [lemma, in Decision]
unanimity_impl_decision [lemma, in Decision]
unanimity_persists [lemma, in Decision]
unanimous_election [lemma, in Decision]
unanimous_supermajority [lemma, in Majority]
under_half_complement [lemma, in Calculate]
unknown_event_vote [lemma, in Famous]


V

vote [inductive, in Vote]
Vote [library]
vote_defined [lemma, in Vote]
vote_consistent [lemma, in Vote]
vote_fun [lemma, in Vote]
vote_round [lemma, in Vote]
vote_witness [lemma, in Vote]
vote_coin [constructor, in Vote]
vote_coin_super [constructor, in Vote]
vote_regular [constructor, in Vote]
vote_first [constructor, in Vote]


W

weight [definition, in Weight]
Weight [library]
weight_lt_by_contradiction [lemma, in Weight]
weight_lt_impl_lt [lemma, in Weight]
weight_lt_increase [lemma, in Weight]
weight_impl_weight_lt [lemma, in Weight]
weight_lt [definition, in Weight]
weight_gt_decide [lemma, in Weight]
weight_finite [lemma, in Weight]
weight_image [lemma, in Weight]
weight_incl [lemma, in Weight]
weight_map_surj [lemma, in Weight]
weight_map_inj [lemma, in Weight]
weight_corr_eq [lemma, in Weight]
weight_corr_le [lemma, in Weight]
weight_difference [lemma, in Weight]
weight_partition [lemma, in Weight]
weight_sum [lemma, in Weight]
weight_subset' [lemma, in Weight]
weight_subset [lemma, in Weight]
weight_nonempty [lemma, in Weight]
weight_empty' [lemma, in Weight]
weight_iff [lemma, in Weight]
weight_fun [lemma, in Weight]
weight_In [lemma, in Weight]
weight_singleton [lemma, in Weight]
weight_empty [lemma, in Weight]
WEIGHT_AND_VALUE.inh [axiom, in Median]
WEIGHT_AND_VALUE.lebU_total [axiom, in Median]
WEIGHT_AND_VALUE.lebU_order [axiom, in Median]
WEIGHT_AND_VALUE.lebU [axiom, in Median]
WEIGHT_AND_VALUE.wt_pos [axiom, in Median]
WEIGHT_AND_VALUE.vl [axiom, in Median]
WEIGHT_AND_VALUE.wt [axiom, in Median]
WEIGHT_AND_VALUE.eqT_decide [axiom, in Median]
WEIGHT_AND_VALUE.U [axiom, in Median]
WEIGHT_AND_VALUE.T [axiom, in Median]
WEIGHT_AND_VALUE [module, in Median]
well_founded_impl_irrefl [lemma, in Relation]
witness [definition, in Round]
witness_decide [lemma, in Round]
world [record, in Hashgraph]
world_forks [projection, in Hashgraph]
world_closed [projection, in Hashgraph]


other

_ $= _ (event_scope) [notation, in Hashgraph]
_ $ _ (event_scope) [notation, in Hashgraph]
_ @= _ (event_scope) [notation, in Hashgraph]
_ @ _ (event_scope) [notation, in Hashgraph]
_ << _ (event_scope) [notation, in Round]
_ _#20 (tactics_scope) [notation, in Tact]
_ _#19 (tactics_scope) [notation, in Tact]
_ _#18 (tactics_scope) [notation, in Tact]
_ _#17 (tactics_scope) [notation, in Tact]
_ _#16 (tactics_scope) [notation, in Tact]
_ _#15 (tactics_scope) [notation, in Tact]
_ _#14 (tactics_scope) [notation, in Tact]
_ _#13 (tactics_scope) [notation, in Tact]
_ _#12 (tactics_scope) [notation, in Tact]
_ _#11 (tactics_scope) [notation, in Tact]
_ _#10 (tactics_scope) [notation, in Tact]
_ _#9 (tactics_scope) [notation, in Tact]
_ _#8 (tactics_scope) [notation, in Tact]
_ _#7 (tactics_scope) [notation, in Tact]
_ _#6 (tactics_scope) [notation, in Tact]
_ _#5 (tactics_scope) [notation, in Tact]
_ _#4 (tactics_scope) [notation, in Tact]
_ _#3 (tactics_scope) [notation, in Tact]
_ _#2 (tactics_scope) [notation, in Tact]
_ anderrl (tactics_scope) [notation, in Tact]
_ anderr (tactics_scope) [notation, in Tact]
_ anderl (tactics_scope) [notation, in Tact]
_ ander (tactics_scope) [notation, in Tact]
_ andel (tactics_scope) [notation, in Tact]



Notation Index

other

_ $= _ (event_scope) [in Hashgraph]
_ $ _ (event_scope) [in Hashgraph]
_ @= _ (event_scope) [in Hashgraph]
_ @ _ (event_scope) [in Hashgraph]
_ << _ (event_scope) [in Round]
_ _#20 (tactics_scope) [in Tact]
_ _#19 (tactics_scope) [in Tact]
_ _#18 (tactics_scope) [in Tact]
_ _#17 (tactics_scope) [in Tact]
_ _#16 (tactics_scope) [in Tact]
_ _#15 (tactics_scope) [in Tact]
_ _#14 (tactics_scope) [in Tact]
_ _#13 (tactics_scope) [in Tact]
_ _#12 (tactics_scope) [in Tact]
_ _#11 (tactics_scope) [in Tact]
_ _#10 (tactics_scope) [in Tact]
_ _#9 (tactics_scope) [in Tact]
_ _#8 (tactics_scope) [in Tact]
_ _#7 (tactics_scope) [in Tact]
_ _#6 (tactics_scope) [in Tact]
_ _#5 (tactics_scope) [in Tact]
_ _#4 (tactics_scope) [in Tact]
_ _#3 (tactics_scope) [in Tact]
_ _#2 (tactics_scope) [in Tact]
_ anderrl (tactics_scope) [in Tact]
_ anderr (tactics_scope) [in Tact]
_ anderl (tactics_scope) [in Tact]
_ ander (tactics_scope) [in Tact]
_ andel (tactics_scope) [in Tact]



Module Index

E

EventMedian [in Median]
EventWeightAndValue [in Median]


M

MedianFun [in Median]
MedianFun.TOrder [in Median]
MedianFun.TSort [in Median]


W

WEIGHT_AND_VALUE [in Median]



Library Index

C

Calculate
Cardinality
Consensus


D

Decide
Decision


F

Fairness
Famous


H

Hashgraph
HashgraphFacts


M

Majority
Median


O

Order


P

Progress


R

Received
Relation
Round


S

Sees


T

Tact
Timestamp


V

Vote


W

Weight



Lemma Index

A

all_rounds_inhabited [in Round]
ancestor_sees [in Sees]
ancestor_impl_spawn_le [in Consensus]
ancestor_realtime [in Hashgraph]
ancestor_witness [in Round]
ancestor_decide [in HashgraphFacts]
ancestor_finite [in HashgraphFacts]
ancestor_initial [in HashgraphFacts]
arbitrary_peer [in HashgraphFacts]
atleasthalf_le_all [in Calculate]
average_range [in Calculate]


C

cardinality_lt_by_contradiction [in Cardinality]
cardinality_lt_impl_lt [in Cardinality]
cardinality_lt_increase [in Cardinality]
cardinality_impl_cardinality_lt [in Cardinality]
cardinality_gt_decide [in Cardinality]
cardinality_finite [in Cardinality]
cardinality_tabulate [in Cardinality]
cardinality_image [in Cardinality]
cardinality_incl [in Cardinality]
cardinality_map_surj [in Cardinality]
cardinality_map_inj [in Cardinality]
cardinality_corr_eq [in Cardinality]
cardinality_corr_le [in Cardinality]
cardinality_difference [in Cardinality]
cardinality_partition [in Cardinality]
cardinality_sum [in Cardinality]
cardinality_subset [in Cardinality]
cardinality_nonempty [in Cardinality]
cardinality_empty' [in Cardinality]
cardinality_iff [in Cardinality]
cardinality_fun [in Cardinality]
cardinality_In [in Cardinality]
cardinality_singleton [in Cardinality]
cardinality_empty [in Cardinality]
corder_support_finite [in Order]
corder_support [in Order]
corder_stable [in Order]
corder_refl [in Order]
corder_total [in Order]
corder_trans [in Order]
corder_antisym [in Order]
cumulative_decisions_support [in Received]


D

decisions_propagate_round [in Decision]
decisions_propagate [in Decision]
decisions_support [in Received]
decision_consistent [in Decision]
decision_vote_consistent [in Decision]
decision_decide [in Decision]
decision_fun [in Decision]
decision_ancestor [in Famous]
dec_forall_imp_finite [in Decide]
dec_exists_finite [in Decide]
dec_equiv [in Decide]
dec_and_dep [in Decide]
dec_In [in Decide]
deduplicate [in Cardinality]
deduplicate [in Weight]
destruct_election' [in Decision]
destruct_election [in Decision]
distinct_peer [in HashgraphFacts]
div3_one_third [in Calculate]


E

earlier_trans [in Round]
earlier_rounds [in Round]
earliest_observer_impl_self_ancestor [in Order]
earliest_observer_defined [in Timestamp]
earliest_observer_fun [in Timestamp]
election_fun [in Decision]
election_defined' [in Vote]
election_defined [in Vote]
election_fun_gen [in Vote]
elector_vote_peer [in Decision]
elector_minimum [in Decision]
elector_unique [in Decision]
elector_rwitness [in Decision]
elector_weight [in Vote]
elector_decide [in Vote]
elector_cardinality [in Famous]
eligible_voter_maximum [in Consensus]
enumerate_subset [in Cardinality]
enumerate_subset [in Weight]
eq_fn_apply [in Tact]
eq_event_decide [in HashgraphFacts]
eq_peer_decide [in HashgraphFacts]
events_reach_every_world [in Progress]
events_are_received [in Progress]
EventWeightAndValue.lebU_order [in Median]
EventWeightAndValue.wt_pos [in Median]
event_broadcast [in Progress]
event_transmit [in Progress]
event_world [in HashgraphFacts]
extends_famous [in Famous]
extends_ufwitness [in Received]
extends_fwitness [in Received]


F

fairness [in Fairness]
fame_reaches_every_world [in Famous]
fame_consensus [in Consensus]
famous_member [in Famous]
famous_decide_nonterm [in Famous]
famous_decide_finite [in Famous]
famous_witness_exists [in Fairness]
filter_to_finite [in Decide]
finite_cardinality [in Cardinality]
finite_weight [in Weight]
finite_exists [in Decide]
finite_star [in Decide]
finite_plus [in Decide]
finite_subset' [in Decide]
finite_subset [in Decide]
finite_equiv [in Decide]
finite_decide [in Decide]
first_witness_exists [in Consensus]
first_witness_realtime [in Consensus]
first_witness_fun [in Consensus]
fold_right_ext_in [in Weight]
fold_right_map [in Weight]
Forall_app [in Median]
fork_decide [in HashgraphFacts]
fork_creator [in HashgraphFacts]
fork_symm [in HashgraphFacts]
four_thirds_le [in Calculate]
fwitness_stable [in Order]
fwitness_finite_global [in Received]
fwitness_finite_finite [in Received]
fwitness_ufwitness_finite [in Received]
fwitness_finite_global_if [in Fairness]
fwitness_finite_nonterm_if [in Fairness]


G

global_nonterminating [in Progress]
good_coins [in Consensus]


H

half_supermajority [in Calculate]
honest_event_exists [in Progress]
honest_timestamp [in Timestamp]
honest_witness_unique [in Round]
honest_decide [in HashgraphFacts]


I

inclusion_exclusion [in Cardinality]
inclusion_exclusion [in Weight]
incl_weight [in Weight]
incl_every [in Majority]
initial_no_self_parent [in HashgraphFacts]
initial_no_parent [in HashgraphFacts]
inj_pair2_UIP [in Tact]
Is_true_decide [in Decide]


L

list_minimum [in Timestamp]


M

majority_complement [in Calculate]
majority_atleasthalf_intersect_calculation [in Calculate]
majority_intersect_calculation [in Calculate]
majority_inhabitant [in Majority]
majority_decide [in Majority]
majority_atleasthalf_intersect [in Majority]
majority_intersect [in Majority]
majority_enlarge [in Majority]
majority_impl_superminority [in Majority]
majority_incl [in Majority]
map_sorted [in Median]
maximum_votes [in Vote]
MedianFun.eqU_decide [in Median]
MedianFun.leU_decide [in Median]
MedianFun.leU_total [in Median]
MedianFun.leU_order [in Median]
MedianFun.majority_median [in Median]
MedianFun.median_spec [in Median]
MedianFun.median_unique [in Median]
MedianFun.select_spec [in Median]
MedianFun.select_unique [in Median]
MedianFun.sselect_eq_select [in Median]
MedianFun.sselect_unique [in Median]
MedianFun.sselect_lift [in Median]
MedianFun.sselect_app_r [in Median]
MedianFun.sselect_cons_r [in Median]
MedianFun.sselect_prefix [in Median]
MedianFun.TOrder.leb_total [in Median]
MedianFun.Transitive_leT [in Median]
MedianFun.tsort_sorted [in Median]
minimal_witness' [in Fairness]
minimal_witness [in Fairness]
mod3_2 [in Calculate]
mod3_1 [in Calculate]
mod3_0 [in Calculate]


N

neq_negb [in Consensus]
NoDup_app [in Cardinality]
NoDup_weight_incl [in Weight]
NoDup_app [in Weight]
NoDup_app_invert [in Median]
nonterminating_nonempty [in Received]
not_supermajority_every [in Majority]
not_supermajority [in Majority]
no_late_fame_world [in Famous]
no_late_fame [in Famous]
no_true_votes_election [in Famous]


O

obtain_ufwitness [in Timestamp]
one_half_plus_two [in Calculate]
one_third_mono [in Calculate]


P

parents_self_parent [in HashgraphFacts]
parent_finite [in HashgraphFacts]
parent_decide [in HashgraphFacts]
peer_vote_offer [in Decision]
peer_vote_elector [in Decision]
permutation_length [in Cardinality]
permutation_weight' [in Weight]
permutation_weight [in Weight]
pigeonhole [in Cardinality]
plusi_plus [in Relation]
plusri_plus [in Relation]
plusr_plus [in Relation]
plus_two_no_coin [in Consensus]
plus_ind_r [in Relation]
plus_ind [in Relation]
plus_well_founded [in Relation]
plus_of_transitive [in Relation]
plus_idem [in Relation]
plus_mono_map [in Relation]
plus_map' [in Relation]
plus_mono [in Relation]
plus_step [in Relation]
plus_plusri [in Relation]
plus_plusi [in Relation]
plus_star_trans [in Relation]
plus_transitive [in Relation]
plus_trans [in Relation]
plus_plusr [in Relation]
plus_one [in Relation]
plus_star [in Relation]


R

realtime_impl_self_ancestor [in Progress]
realtime_spawn_impl_leq [in Consensus]
realtime_refl_spawn [in Consensus]
realtime_parent [in Hashgraph]
realtime_antisym [in Hashgraph]
realtime_trans [in Hashgraph]
realtime_member [in Hashgraph]
received_impl_time_received [in Order]
received_support [in Received]
received_by_support [in Received]
received_cumulative [in Received]
received_consistent [in Received]
received_by_consistent [in Received]
received_defined [in Received]
received_by_exists [in Received]
received_by_decide [in Received]
received_by_global [in Received]
received_fun [in Received]
received_by_inhabited [in Received]
rounds_earlier [in Round]
round_advanced [in Progress]
round_decide [in Round]
round_defined [in Round]
round_mono [in Round]
round_fun [in Round]
rwitness_decide [in Round]
rwitness_earlier [in Round]
rwitness_fun [in Round]
rwitness_witness [in Round]


S

sees_decide [in Sees]
sees_impl_ancestor [in Sees]
self_ancestor_stsees_trans [in Sees]
self_ancestor_sees_trans [in Sees]
self_ancestor_witness [in Round]
self_ancestor_total' [in HashgraphFacts]
self_ancestor_total [in HashgraphFacts]
self_ancestor_decide [in HashgraphFacts]
self_ancestor_creator [in HashgraphFacts]
self_parent_well_founded [in HashgraphFacts]
self_ancestor_impl_ancestor [in HashgraphFacts]
self_parent_decide [in HashgraphFacts]
self_parent_creator [in HashgraphFacts]
self_parent_fun [in HashgraphFacts]
self_parent_impl_parent [in HashgraphFacts]
similar_first_witness [in Consensus]
similar_vote [in Consensus]
similar_election [in Consensus]
similar_symm [in Consensus]
similar_weaken [in Consensus]
sorted_impl [in Median]
sorted_unique [in Median]
starr_star [in Relation]
star_mono_map [in Relation]
star_map' [in Relation]
star_plus_trans [in Relation]
star_neq_plus [in Relation]
star_plus [in Relation]
star_starr [in Relation]
star_map [in Relation]
star_mono [in Relation]
star_stepr [in Relation]
star_one [in Relation]
star_transitive [in Relation]
star_trans [in Relation]
strict_ancestor_impl_spawn_lt [in Consensus]
strict_self_ancestor_witness [in Round]
strict_ancestor_decide [in HashgraphFacts]
strict_ancestor_finite [in HashgraphFacts]
strict_ancestor_irreflex [in HashgraphFacts]
strict_ancestor_initial [in HashgraphFacts]
strict_self_ancestor_parent [in HashgraphFacts]
strict_ancestor_parents [in HashgraphFacts]
strict_ancestor_well_founded [in HashgraphFacts]
strict_self_ancestor_impl_strict_ancestor [in HashgraphFacts]
strongly_sorted_remove_middle [in Median]
strongly_sorted_app_inv [in Median]
strongly_seeing [in Sees]
stseen_witness_unique [in Round]
stsees_ancestor_trans [in Sees]
stsees_decide [in Sees]
stsees_impl_ancestor [in Sees]
stsees_impl_strict_ancestor [in Sees]
stsees_many_witnesses [in Round]
stsees_impl_famous [in Fairness]
stsees_impl_famous_pre [in Fairness]
succ_no_coin [in Decision]
sumweight_app [in Weight]
sumweight_cons [in Weight]
supermajority_intersect_3_calculation [in Calculate]
supermajority_intersect_2_calculation [in Calculate]
supermajority_inhabitant [in Majority]
supermajority_decide [in Majority]
supermajority_intersect_3 [in Majority]
supermajority_intersect_2' [in Majority]
supermajority_intersect_2 [in Majority]
supermajority_iff [in Majority]
supermajority_enlarge [in Majority]
supermajority_impl_majority [in Majority]
superminority_supermajority_intersect_calculation [in Calculate]
superminority_supermajority_intersect [in Majority]


T

textorder_decide [in HashgraphFacts]
time_received_consistent [in Order]
time_received_defined [in Order]
time_received_fun [in Order]
too_many_voters_honest [in Consensus]
too_many_voters_elector [in Consensus]
too_many_voters [in Consensus]
two_thirds_of_three [in Calculate]
two_thirds_shift [in Calculate]
two_thirds_mono [in Calculate]
two_thirds_lt [in Calculate]


U

ufwitness_stable [in Order]
ufwitness_fun [in Timestamp]
ufwitness_finite_global [in Received]
ufwitness_finite_finite [in Received]
unanimity [in Decision]
unanimity_impl_decision [in Decision]
unanimity_persists [in Decision]
unanimous_election [in Decision]
unanimous_supermajority [in Majority]
under_half_complement [in Calculate]
unknown_event_vote [in Famous]


V

vote_defined [in Vote]
vote_consistent [in Vote]
vote_fun [in Vote]
vote_round [in Vote]
vote_witness [in Vote]


W

weight_lt_by_contradiction [in Weight]
weight_lt_impl_lt [in Weight]
weight_lt_increase [in Weight]
weight_impl_weight_lt [in Weight]
weight_gt_decide [in Weight]
weight_finite [in Weight]
weight_image [in Weight]
weight_incl [in Weight]
weight_map_surj [in Weight]
weight_map_inj [in Weight]
weight_corr_eq [in Weight]
weight_corr_le [in Weight]
weight_difference [in Weight]
weight_partition [in Weight]
weight_sum [in Weight]
weight_subset' [in Weight]
weight_subset [in Weight]
weight_nonempty [in Weight]
weight_empty' [in Weight]
weight_iff [in Weight]
weight_fun [in Weight]
weight_In [in Weight]
weight_singleton [in Weight]
weight_empty [in Weight]
well_founded_impl_irrefl [in Relation]
witness_decide [in Round]



Axiom Index

C

coin [in Hashgraph]
coin_freq_min [in Hashgraph]
coin_freq [in Hashgraph]
creator [in Hashgraph]


D

distinct_honest_peers [in Hashgraph]


E

event [in Hashgraph]
eventual_agreement [in Hashgraph]
event_eq_dec [in Hashgraph]


F

first_regular_min [in Hashgraph]
first_regular [in Hashgraph]


H

honest [in Hashgraph]
honest_peers_sync [in Hashgraph]


I

initial_decide [in Hashgraph]


N

no_orphans [in Hashgraph]
no_majority_stake [in Hashgraph]
number_of_peers [in Hashgraph]
number_peers_minimum [in Hashgraph]
number_peers [in Hashgraph]


P

parents [in Hashgraph]
parents_creator [in Hashgraph]
parents_fun [in Hashgraph]
parent_well_founded [in Hashgraph]
peer [in Hashgraph]
peer_eq_dec [in Hashgraph]


S

sample [in Hashgraph]
spawn [in Hashgraph]
spawn_forks [in Hashgraph]
spawn_parent [in Hashgraph]
spawn_inj [in Hashgraph]
stake [in Hashgraph]
stake_positive [in Hashgraph]
supermajority_honest [in Hashgraph]


T

textorder [in Hashgraph]
textorder_total [in Hashgraph]
textorder_order [in Hashgraph]
the_total_stake [in Hashgraph]
timestamp [in Hashgraph]
total_stake [in Hashgraph]


W

WEIGHT_AND_VALUE.inh [in Median]
WEIGHT_AND_VALUE.lebU_total [in Median]
WEIGHT_AND_VALUE.lebU_order [in Median]
WEIGHT_AND_VALUE.lebU [in Median]
WEIGHT_AND_VALUE.wt_pos [in Median]
WEIGHT_AND_VALUE.vl [in Median]
WEIGHT_AND_VALUE.wt [in Median]
WEIGHT_AND_VALUE.eqT_decide [in Median]
WEIGHT_AND_VALUE.U [in Median]
WEIGHT_AND_VALUE.T [in Median]



Constructor Index

M

mk_world [in Hashgraph]


P

parent1 [in Hashgraph]
parent2 [in Hashgraph]
plusi_step [in Relation]
plusi_one [in Relation]
plusri_step [in Relation]
plusri_one [in Relation]


R

round_advance [in Round]
round_nadvance [in Round]
round_initial [in Round]


S

starr_step [in Relation]
starr_refl [in Relation]
star_step [in Relation]
star_refl [in Relation]


V

vote_coin [in Vote]
vote_coin_super [in Vote]
vote_regular [in Vote]
vote_first [in Vote]



Inductive Index

P

parent [in Hashgraph]
plusi [in Relation]
plusri [in Relation]


R

round [in Round]


S

star [in Relation]
starr [in Relation]


V

vote [in Vote]



Projection Index

M

member [in Hashgraph]


W

world_forks [in Hashgraph]
world_closed [in Hashgraph]



Definition Index

A

ancestor [in Hashgraph]
atleasthalf [in Majority]


C

car [in Tact]
cardinality [in Cardinality]
cardinality_lt [in Cardinality]
cdr [in Tact]
compose [in Relation]
corder [in Order]
creatorstake [in Vote]


D

decision [in Decision]


E

earlier [in Round]
earliest_observer [in Order]
election [in Vote]
elector [in Vote]
EventWeightAndValue.eqT_decide [in Median]
EventWeightAndValue.inh [in Median]
EventWeightAndValue.lebU [in Median]
EventWeightAndValue.lebU_total [in Median]
EventWeightAndValue.T [in Median]
EventWeightAndValue.U [in Median]
EventWeightAndValue.vl [in Median]
EventWeightAndValue.wt [in Median]
every [in Majority]
extends [in Hashgraph]


F

famous [in Famous]
finite [in Decide]
first_witness [in Consensus]
fork [in Hashgraph]
fwitness [in Famous]


G

global [in Hashgraph]


I

incl [in Decide]
initial [in Hashgraph]


M

majority [in Majority]
Marker_invert [in Tact]
MedianFun.leT [in Median]
MedianFun.leU [in Median]
MedianFun.median [in Median]
MedianFun.select [in Median]
MedianFun.sselect [in Median]
MedianFun.TOrder.leb [in Median]
MedianFun.TOrder.t [in Median]


N

nonempty [in Received]
nonterminating [in Round]


O

offer [in Decision]
one_third [in Calculate]
one_half [in Calculate]


P

peer_vote [in Decision]
plus [in Relation]
plusr [in Relation]


R

realtime [in Hashgraph]
realtime_before [in HashgraphFacts]
received [in Received]
received_by [in Received]
rwitness [in Round]


S

sees [in Sees]
self_ancestor [in Hashgraph]
self_parent [in Hashgraph]
similar [in Hashgraph]
strict_self_ancestor [in Hashgraph]
strict_ancestor [in Hashgraph]
stsees [in Sees]
sumweight [in Weight]
supermajority [in Majority]
superminority [in Majority]


T

time_received [in Order]
two_thirds [in Calculate]


U

ufwitness [in Received]


W

weight [in Weight]
weight_lt [in Weight]
witness [in Round]



Record Index

W

world [in Hashgraph]



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 (578 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 (29 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 (6 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 (21 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 (375 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 (48 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 (18 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 (7 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 (3 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 (70 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 (1 entry)

This page has been generated by coqdoc