stabilization_admits.txt

adopting_succs_decreases_succs_error
at_most_one_request_timeout_invariant
better_pred_eventually_improves_succ
Classical_Prop:classic
constrained_Request_not_cleared_by_recv_handler
dead_node_channel_empties_out
dead_nodes_go_quiet
error_decreases_when_succs_right
error_means_merge_point_or_wrong_pred
first_succ_error_nonincreasing
first_succ_same_until_improvement
has_first_succ_stable
has_succ_has_pred_inv
incoming_GotPredAndSuccs_with_a_after_p_causes_improvement
in_concat
initial_esl_is_sorted_nodes_chopped
join2_target_joined
joins_stop
live_node_in_succs_best_succ
merge_points_preserved_until_error_drops
notify_when_pred_None_eventually_improves
not_skipped_means_incoming_succs_not_skipped
open_stabilize_request_until_response
phase_one_error_continuously_nonincreasing
phase_two_zero_error_locally_correct
pred_bound_pred_not_worse
pred_error_nonincreasing
pred_same_until_improvement
queries_eventually_stop
query_message_ok_invariant
RecvMsg_enabled_until_occurred
sorted_list_elements_not_between
stabilize2_target_joined
stabilize_target_joined
succ_between_improves_error
successor_nodes_always_valid
successors_are_live_nodes
succ_list_len_lower_bound
succs_error_helper_invar
succs_error_nonincreasing
valid_ptrs_global_inductive
wf_ptr_succ_list_invariant'