[0]
[1]
[2]
[3]
[4]
[5]
[6]
[9]
[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]
2
top next
Paasche-alg-2
Paasche-alg-2_wf
Rice-theorem-for-Type_2
Theorem 6.2 in Bezem,Coquand,Huber
add-one-mod-2
add-plus-1-div-2-implies-lt
assert-bl-all-2
assert-es-eq-E-2
bag-member-lifting-2
bag-member-lifting-loc-2
bag-member-subtype-2
basic-seq-1-2
basic-seq-1-2_wf
callbyvalueall-seq-extend-2
callbyvalueall-seq-extend0-2
cbv_sqle_2
concat-lifting-2
concat-lifting-2-strict
concat-lifting-2_wf
concat-lifting-loc-2
concat-lifting-loc-2-strict
concat-lifting-loc-2_wf
cu_filler_2
decidable__atom_equal_2
div_2_to_1
div_bounds_2
divides_invar_2
divisibility-by-2-rule
eqff_assert_2
eqtt_assert_2
exp-2-3-fact
filter_wf4_2
gcd_is_divisor_2
gcd_p_neg_arg_2
grp_lt_transitivity_2
has-value-implies-dec-isatom-2
has-value-implies-dec-isatom2-2
has-value-implies-dec-isaxiom-2
has-value-implies-dec-isinl-2
has-value-implies-dec-isinr-2
has-value-implies-dec-isint-2
has-value-implies-dec-islambda-2
has-value-implies-dec-ispair-2
hdf-compose1-transformation0-2
hdf-compose1-transformation1-2
hdf-compose2-transformation1-2-0
hdf-compose2-transformation1-2-1
hdf-compose2-transformation1-2-2
hdf-compose2-transformation1-2-3
hdf-memory-base2-2
hdf-memory-base3-2
hdf-memory-base4-2
hdf-parallel-transformation1-2-0
hdf-parallel-transformation1-2-1
hdf-parallel-transformation2-2
hdf-sqequal6-2
hdf-sqequal8-2
hdf-state-base2-2
hdf-state-base3-2
hdf-state-base4-2
int_mod_2_isect_int_mod_3
int_mod_2_union_int_mod_3
interleaving_as_filter_2
isect-subtype-2
ite-bool-2
lifting-2
lifting-2-strict
lifting-2_wf
lifting-add-isaxiom-2
lifting-add-ispair-2
lifting-add-spread-2
lifting-loc-2
lifting-loc-2_wf
list_2_decomp
lt_transitivity_2
map_functionality_2
member-eclass-simple-comb-2-iff
member-eclass-simple-loc-comb-2-iff
member-of-tagged+2
member_filter_2
nat_op_mon_hom_2
not-equal-2
not-ge-2
not-gt-2
not-le-2
oal_lk_merge_2
prob2.2
rec-combined-class-2
rec-combined-class-2-classrel
rec-combined-class-2_wf
rec-combined-class-opt-2
rec-combined-class-opt-2-classrel
rec-combined-class-opt-2_wf
rec-combined-loc-class-2
rec-combined-loc-class-2-classrel
rec-combined-loc-class-2_wf
rec-combined-loc-class-opt-2
rec-combined-loc-class-opt-2-classrel
rec-combined-loc-class-opt-2_wf
regularize-2-regular
rel_star_symmetric_2
rem_2_to_1
rem_bounds_2
rem_sym_2
rev_permf_order_2
rroot-odd-2-regular
rsqrt-rnexp-2
rsqrt_2-irrational
set_lt_transitivity_2
simple-cbva-seq-extend-2
simple-comb-2
simple-comb-2-classrel
simple-comb-2-classrel-weak
simple-comb-2-concat-classrel
simple-comb-2-concat-classrel-weak
simple-comb-2-es-sv
simple-comb-2_wf
simple-loc-comb-2
simple-loc-comb-2-classrel
simple-loc-comb-2-classrel-weak
simple-loc-comb-2-concat-classrel
simple-loc-comb-2-concat-classrel-weak
simple-loc-comb-2-concat-es-sv
simple-loc-comb-2-concat-loc-bounded
simple-loc-comb-2-concat-loc-bounded2
simple-loc-comb-2-concat-loc-bounded3
simple-loc-comb-2-concat-single-val
simple-loc-comb-2-loc-bounded
simple-loc-comb-2-loc-bounded2
simple-loc-comb-2-loc-bounded3
simple-loc-comb-2_wf
sublist_filter_2
subtype_rel_isect-2
swap_eval_2
swap_order_2
trivial_ite_2
tswap_eval_2
txpose_perm_order_2
23
prev top next
------ new_23_sig - extra ------
------ new_23_sig - headers ------
------ new_23_sig - specification ------
new_23_sig-decided
new_23_sig-ilf
new_23_sig-notify
new_23_sig-retry
new_23_sig-vote
new_23_sig_NewRounds
new_23_sig_NewRounds-program
new_23_sig_NewRounds-program_wf
new_23_sig_NewRoundsState
new_23_sig_NewRoundsState-classrel
new_23_sig_NewRoundsState-functional
new_23_sig_NewRoundsState-program
new_23_sig_NewRoundsState-program_wf
new_23_sig_NewRoundsStateFun
new_23_sig_NewRoundsStateFun_wf
new_23_sig_NewRoundsState_wf
new_23_sig_NewRounds_wf
new_23_sig_NewVoters
new_23_sig_NewVoters-program
new_23_sig_NewVoters-program_wf
new_23_sig_NewVoters_wf
new_23_sig_Notify
new_23_sig_Notify-program
new_23_sig_Notify-program_wf
new_23_sig_Notify_wf
new_23_sig_Proposal
new_23_sig_Proposal-program
new_23_sig_Proposal-program_wf
new_23_sig_Proposal_wf
new_23_sig_Quorum
new_23_sig_Quorum-program
new_23_sig_Quorum-program_wf
new_23_sig_QuorumState
new_23_sig_QuorumState-classrel
new_23_sig_QuorumState-functional
new_23_sig_QuorumState-program
new_23_sig_QuorumState-program_wf
new_23_sig_QuorumStateFun
new_23_sig_QuorumStateFun_wf
new_23_sig_QuorumState_wf
new_23_sig_Quorum_wf
new_23_sig_Replica
new_23_sig_Replica-program
new_23_sig_Replica-program_wf
new_23_sig_ReplicaState
new_23_sig_ReplicaState-classrel
new_23_sig_ReplicaState-functional
new_23_sig_ReplicaState-program
new_23_sig_ReplicaState-program_wf
new_23_sig_ReplicaStateFun
new_23_sig_ReplicaStateFun_wf
new_23_sig_ReplicaState_wf
new_23_sig_Replica_wf
new_23_sig_Round
new_23_sig_Round-program
new_23_sig_Round-program_wf
new_23_sig_RoundInfo
new_23_sig_RoundInfo-program
new_23_sig_RoundInfo-program_wf
new_23_sig_RoundInfo-single-val
new_23_sig_RoundInfo_wf
new_23_sig_Round_wf
new_23_sig_Rounds
new_23_sig_Rounds-program
new_23_sig_Rounds-program_wf
new_23_sig_Rounds_wf
new_23_sig_Voter
new_23_sig_Voter-program
new_23_sig_Voter-program_wf
new_23_sig_Voter_wf
new_23_sig_add_to_quorum
new_23_sig_add_to_quorum_wf
new_23_sig_addvote
new_23_sig_addvote_wf
new_23_sig_agreement
new_23_sig_assert_newvote
new_23_sig_commands_from_votes
new_23_sig_commands_from_votes_wf
new_23_sig_decided'base
new_23_sig_decided'base-program
new_23_sig_decided'base-program_wf
new_23_sig_decided'base_wf
new_23_sig_decided'broadcast
new_23_sig_decided'broadcast_wf
new_23_sig_decided_property
new_23_sig_decided_with_id
new_23_sig_decided_with_id-assert-classrel
new_23_sig_decided_with_id-assert-type
new_23_sig_decided_with_id_wf
new_23_sig_decision
new_23_sig_decision_wf
new_23_sig_headers
new_23_sig_headers_fun
new_23_sig_headers_fun_wf
new_23_sig_headers_internal
new_23_sig_headers_internal_wf
new_23_sig_headers_no_inputs
new_23_sig_headers_no_inputs_types
new_23_sig_headers_no_inputs_types_wf
new_23_sig_headers_no_inputs_wf
new_23_sig_headers_no_rep
new_23_sig_headers_no_rep_wf
new_23_sig_headers_type
new_23_sig_headers_type_wf
new_23_sig_headers_wf
new_23_sig_increasing_max
new_23_sig_main
new_23_sig_main-program
new_23_sig_main-program_wf
new_23_sig_main_wf
new_23_sig_message-constraint
new_23_sig_message-constraint_wf
new_23_sig_messages-delivered
new_23_sig_messages-delivered_wf
new_23_sig_newvote
new_23_sig_newvote_wf
new_23_sig_notify'broadcast
new_23_sig_notify'broadcast_wf
new_23_sig_progress-step1
new_23_sig_progress-step10
new_23_sig_progress-step2
new_23_sig_progress-step3
new_23_sig_progress-step4
new_23_sig_progress-step5
new_23_sig_progress-step6
new_23_sig_progress-step7
new_23_sig_progress-step8
new_23_sig_progress-step8-v2
new_23_sig_progress-step8-v3
new_23_sig_progress-step9
new_23_sig_progress-step9-v2
new_23_sig_progress-step9-v3
new_23_sig_progress1
new_23_sig_progress2-step1
new_23_sig_progress2-step2
new_23_sig_proposal_classrel
new_23_sig_proposal_classrel2
new_23_sig_proposal_has_header
new_23_sig_proposal_if_vote
new_23_sig_propose'base
new_23_sig_propose'base-program
new_23_sig_propose'base-program_wf
new_23_sig_propose'base_wf
new_23_sig_quorum_fseg
new_23_sig_quorum_inv_vote
new_23_sig_quorum_inv_vote2
new_23_sig_quorum_inv_vote2_fun
new_23_sig_quorum_inv_vote_fun
new_23_sig_quorum_invariant
new_23_sig_quorum_invariant_fun
new_23_sig_quorum_mem
new_23_sig_quorum_state_eq1
new_23_sig_quorum_state_eq1-forward
new_23_sig_quorum_state_fun_eq
new_23_sig_replica_state_from_proposal
new_23_sig_replica_state_from_proposal_fun
new_23_sig_replica_state_mem
new_23_sig_replica_state_mem_fun
new_23_sig_retry'base
new_23_sig_retry'base-program
new_23_sig_retry'base-program_wf
new_23_sig_retry'base_wf
new_23_sig_retry'send
new_23_sig_retry'send_wf
new_23_sig_retry_property
new_23_sig_round_info_classrel2
new_23_sig_roundout
new_23_sig_roundout_wf
new_23_sig_rounds_inc
new_23_sig_rounds_mem
new_23_sig_rounds_mem_fun
new_23_sig_rounds_pos
new_23_sig_rounds_pos_fun
new_23_sig_rounds_strict_inc
new_23_sig_update_replica
new_23_sig_update_replica_wf
new_23_sig_update_round
new_23_sig_update_round_wf
new_23_sig_validity
new_23_sig_vote'base
new_23_sig_vote'base-program
new_23_sig_vote'base-program_wf
new_23_sig_vote'base_wf
new_23_sig_vote'broadcast
new_23_sig_vote'broadcast_wf
new_23_sig_vote2prop
new_23_sig_vote2prop_wf
new_23_sig_vote2retry
new_23_sig_vote2retry_wf
new_23_sig_vote_with_ballot
new_23_sig_vote_with_ballot-assert-classrel
new_23_sig_vote_with_ballot-assert-type
new_23_sig_vote_with_ballot-forward
new_23_sig_vote_with_ballot-header
new_23_sig_vote_with_ballot-if-classrel
new_23_sig_vote_with_ballot_and_id
new_23_sig_vote_with_ballot_and_id-assert-classrel
new_23_sig_vote_with_ballot_and_id-assert-type
new_23_sig_vote_with_ballot_and_id-forward
new_23_sig_vote_with_ballot_and_id-if-classrel
new_23_sig_vote_with_ballot_and_id-if-snd
new_23_sig_vote_with_ballot_and_id-implies
new_23_sig_vote_with_ballot_and_id-snd
new_23_sig_vote_with_ballot_and_id_wf
new_23_sig_vote_with_ballot_first
new_23_sig_vote_with_ballot_first-assert
new_23_sig_vote_with_ballot_first-assert-forward
new_23_sig_vote_with_ballot_first-assert-forward2
new_23_sig_vote_with_ballot_first-assert-type
new_23_sig_vote_with_ballot_first-forward
new_23_sig_vote_with_ballot_first-not
new_23_sig_vote_with_ballot_first-not2
new_23_sig_vote_with_ballot_first_alt
new_23_sig_vote_with_ballot_first_alt_wf
new_23_sig_vote_with_ballot_first_wf
new_23_sig_vote_with_ballot_wf
new_23_sig_voter_start
new_23_sig_voter_start_unique
new_23_sig_votes_consistent
new_23_sig_when_new_proposal
new_23_sig_when_new_proposal_wf
new_23_sig_when_new_round
new_23_sig_when_new_round_wf
new_23_sig_when_quorum
new_23_sig_when_quorum_wf
25
prev top next
first-25-rationals
2OP
prev top
dist_1op_2op_lr
dist_1op_2op_lr_wf
fun_thru_2op
fun_thru_2op_wf
sq_stable__dist_1op_2op_lr
sq_stable__fun_thru_2op