|
***
*** top (19:10:17 11/7/2014)
*** Generated by proveit - ProofLite-6.0.9 (3/14/14)
***
Proof summary for theory top
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory core_top
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory majority_integration
consensus_validity....................proved - incomplete [shostak](0.55 s)
agreement_generation..................proved - incomplete [shostak](0.49 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (1.04 s)
Proof summary for theory protocol_integration
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory comm_integration
quorum_correct_integration............proved - incomplete [shostak](0.13 s)
majority_correct_rw...................proved - incomplete [shostak](0.12 s)
all_symmetric_integration.............proved - incomplete [shostak](0.12 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.37 s)
Proof summary for theory comm_integration_stage
msg_checker_TCC1......................proved - complete [shostak](0.03 s)
osym_rcvd_TCC1........................proved - complete [shostak](0.03 s)
oasym_rcvd_TCC1.......................proved - complete [shostak](0.03 s)
sv_rcvd_TCC1..........................proved - complete [shostak](0.03 s)
correct_denotation_send...............proved - complete [shostak](0.09 s)
conforms_type.........................proved - complete [shostak](0.05 s)
scheduled_conform.....................proved - incomplete [shostak](0.05 s)
exact_correct_denotation..............proved - incomplete [shostak](0.05 s)
quorum_correct_integration............proved - incomplete [shostak](0.04 s)
majority_correct_rw...................proved - incomplete [shostak](0.04 s)
exact_single_denotation...............proved - incomplete [shostak](0.21 s)
uniformly_enabled.....................proved - incomplete [shostak](0.18 s)
exact_symmetric_single................proved - incomplete [shostak](0.14 s)
all_symmetric_integration.............proved - incomplete [shostak](0.04 s)
good_conforms.........................proved - incomplete [shostak](0.05 s)
Theory totals: 15 formulas, 15 attempted, 15 succeeded (1.04 s)
Proof summary for theory integration_fault_model
symmetric_single_denotation...........proved - complete [shostak](0.04 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.04 s)
Proof summary for theory finite_sets_below_extra
below_is_finite_type..................proved - complete [shostak](0.04 s)
set_below_is_finite...................proved - incomplete [shostak](0.03 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.07 s)
Proof summary for theory exact_comm_stage
correct_uniform.......................proved - incomplete [shostak](0.08 s)
correct_uniform_alt...................proved - incomplete [shostak](0.09 s)
majority_correct_rw...................proved - incomplete [shostak](0.05 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.22 s)
Proof summary for theory fault_assumptions_stage
enabled_TCC1..........................proved - incomplete [shostak](0.05 s)
enabled?_TCC1.........................proved - incomplete [shostak](0.04 s)
enabled_within........................proved - incomplete [shostak](0.04 s)
quorum_implies_majority...............proved - incomplete [shostak](0.13 s)
majority..............................proved - incomplete [shostak](0.14 s)
enabled_within_quorum.................proved - incomplete [shostak](0.09 s)
enabled_within_quorum_nada............proved - incomplete [shostak](0.12 s)
quorum_nonempty.......................proved - incomplete [shostak](0.05 s)
max_TCC1..............................proved - incomplete [shostak](0.11 s)
intersection_majority_nonempty........proved - incomplete [shostak](0.09 s)
byzantine_intersection_nonempty.......proved - incomplete [shostak](0.19 s)
intersection_majority.................proved - incomplete [shostak](0.14 s)
enabled_agree.........................proved - incomplete [shostak](0.07 s)
Theory totals: 13 formulas, 13 attempted, 13 succeeded (1.25 s)
Proof summary for theory pigeonhole
pigeonhole............................proved - complete [shostak](0.12 s)
card_difference_alt...................proved - complete [shostak](0.15 s)
pigeonhole_difference.................proved - complete [shostak](0.12 s)
simple_majority_subset................proved - complete [shostak](0.08 s)
majority_subset_nonempty..............proved - complete [shostak](0.08 s)
simple_majority_nonempty..............proved - complete [shostak](0.03 s)
majority_nonempty.....................proved - complete [shostak](0.07 s)
majority_pigeonhole...................proved - complete [shostak](0.12 s)
simple_majority_pigeonhole............proved - complete [shostak](0.19 s)
median_pigeonhole.....................proved - complete [shostak](0.34 s)
intersection_nonempty.................proved - complete [shostak](0.09 s)
two_thirds_overlap_pigeonhole.........proved - complete [shostak](0.25 s)
quorum?_TCC1..........................proved - complete [shostak](0.04 s)
M_TCC1................................proved - complete [shostak](0.04 s)
M_TCC2................................proved - complete [shostak](0.11 s)
nada_reduce...........................proved - complete [shostak](0.06 s)
mid_reduce............................proved - complete [shostak](0.08 s)
byz_reduce............................proved - complete [shostak](0.06 s)
Theory totals: 18 formulas, 18 attempted, 18 succeeded (2.01 s)
Proof summary for theory tau_declaration
nada_TCC1.............................proved - complete [shostak](0.03 s)
mid_TCC1..............................proved - complete [shostak](0.08 s)
byz_TCC1..............................proved - complete [shostak](0.07 s)
weber_TCC1............................proved - complete [shostak](0.10 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.28 s)
Proof summary for theory node_functions_stage
nominal_filter_TCC1...................proved - complete [shostak](0.09 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.09 s)
Proof summary for theory node
uniform_char..........................proved - complete [shostak](0.04 s)
enabled_symmetric_uniform.............proved - complete [shostak](0.05 s)
m_TCC1................................proved - complete [shostak](0.09 s)
vec2seq_TCC1..........................proved - complete [shostak](0.04 s)
vec2seq_agreement.....................proved - complete [shostak](0.08 s)
vec2seq_type..........................proved - complete [shostak](0.05 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.35 s)
Proof summary for theory local
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory exact_comm
majority_correct_rw...................proved - incomplete [shostak](0.10 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.10 s)
Proof summary for theory node_functions
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory protocol
protocol_rw...........................proved - complete [shostak](0.05 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.05 s)
Proof summary for theory majority
consensus_validity....................proved - incomplete [shostak](0.54 s)
agreement_generation..................proved - incomplete [shostak](0.48 s)
faulty_source.........................proved - incomplete [shostak](0.25 s)
faulty_stage..........................proved - incomplete [shostak](0.12 s)
asymmetric_source.....................proved - incomplete [shostak](0.32 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (1.71 s)
Proof summary for theory majority_stage
majority_at_destination...............proved - incomplete [shostak](0.10 s)
majority_validity.....................proved - incomplete [shostak](0.07 s)
consensus_validity....................proved - incomplete [shostak](0.07 s)
agreement_generation_alt..............proved - incomplete [shostak](0.10 s)
agreement_generation..................proved - incomplete [shostak](0.05 s)
faulty_source.........................proved - incomplete [shostak](0.10 s)
sources_disagree......................proved - incomplete [shostak](0.06 s)
asymmetric_source.....................proved - incomplete [shostak](0.07 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.62 s)
Proof summary for theory majority_properties
is_majority...........................proved - incomplete [shostak](0.49 s)
majority_value_subset.................proved - complete [shostak](0.09 s)
uniform_majority......................proved - complete [shostak](0.14 s)
majority_validity.....................proved - incomplete [shostak](0.05 s)
agreement_generation..................proved - incomplete [shostak](0.05 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.81 s)
Proof summary for theory finite_seqs
choose_TCC1...........................proved - complete [shostak](0.03 s)
choose_in?............................proved - complete [shostak](0.05 s)
choose_consensus......................proved - complete [shostak](0.04 s)
maj_exists_same.......................proved - incomplete [shostak](0.05 s)
mf_lem................................proved - incomplete [shostak](0.04 s)
majority_choose_consensus.............proved - incomplete [shostak](0.06 s)
majority_choose2_TCC1.................proved - complete [shostak](0.04 s)
majority_choose2_TCC2.................proved - complete [shostak](0.03 s)
majority2_choose_majority.............proved - incomplete [shostak](0.21 s)
uniform_TCC1..........................proved - complete [shostak](0.04 s)
uniform_TCC2..........................proved - incomplete [shostak](0.05 s)
majority_same.........................proved - incomplete [shostak](0.17 s)
Theory totals: 12 formulas, 12 attempted, 12 succeeded (0.81 s)
Proof summary for theory exact_reduce_integration
lower_validity........................proved - incomplete [shostak](0.55 s)
upper_validity........................proved - incomplete [shostak](0.54 s)
agreement_generation..................proved - incomplete [shostak](0.55 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (1.63 s)
Proof summary for theory ordered_message
valid_iff_ord1........................proved - complete [shostak](0.03 s)
eq_iff................................proved - complete [shostak](0.06 s)
message_total_order...................proved - complete [shostak](0.34 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.43 s)
Proof summary for theory exact_reduce
lower_validity........................proved - incomplete [shostak](1.00 s)
upper_validity........................proved - incomplete [shostak](0.99 s)
consensus_validity....................proved - incomplete [shostak](0.44 s)
exact_agreement_propagation...........proved - incomplete [shostak](0.41 s)
agreement_generation..................proved - incomplete [shostak](0.77 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (3.61 s)
Proof summary for theory k_ordered
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory reduce_choice
in_rcvd...............................proved - incomplete [shostak](0.27 s)
min_reduce_choice.....................proved - incomplete [shostak](0.17 s)
max_reduce_choice.....................proved - incomplete [shostak](0.17 s)
reduce_overlap?_TCC1..................proved - incomplete [shostak](0.13 s)
reduce_overlap?_TCC2..................proved - incomplete [shostak](0.41 s)
max_length_TCC1.......................proved - incomplete [shostak](0.07 s)
max_length_bound......................proved - incomplete [shostak](0.21 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (1.44 s)
Proof summary for theory reduce_properties
lowset_TCC1...........................proved - incomplete [shostak](0.15 s)
card_lower_leq_lowset_TCC1............proved - complete [shostak](0.04 s)
card_lower_leq_lowset.................proved - incomplete [shostak](0.26 s)
card_lowset...........................proved - incomplete [shostak](0.16 s)
card_upper_leq_highset................proved - incomplete [shostak](0.26 s)
card_highset..........................proved - incomplete [shostak](0.15 s)
reduce_TCC1...........................proved - complete [shostak](0.10 s)
reduce_TCC2...........................proved - complete [shostak](0.10 s)
reduce_TCC3...........................proved - incomplete [shostak](0.25 s)
min_reduce_TCC1.......................proved - complete [shostak](0.08 s)
min_reduce_TCC2.......................proved - incomplete [shostak](0.17 s)
min_reduce............................proved - incomplete [shostak](0.19 s)
max_reduce_TCC1.......................proved - incomplete [shostak](0.20 s)
max_reduce............................proved - incomplete [shostak](0.19 s)
reduce_length.........................proved - incomplete [shostak](0.30 s)
reduce_rewrite_TCC1...................proved - incomplete [shostak](0.35 s)
reduce_rewrite_TCC2...................proved - incomplete [shostak](0.25 s)
reduce_rewrite........................proved - incomplete [shostak](0.26 s)
reduce_overlap_TCC1...................proved - incomplete [shostak](0.46 s)
reduce_overlap........................proved - incomplete [shostak](0.25 s)
reduce_agreement......................proved - incomplete [shostak](0.06 s)
min_validity..........................proved - incomplete [shostak](0.15 s)
max_validity..........................proved - incomplete [shostak](0.15 s)
choice_lower_validity.................proved - incomplete [shostak](0.16 s)
choice_upper_validity.................proved - incomplete [shostak](0.16 s)
choice_agreement_generation...........proved - incomplete [shostak](0.09 s)
Theory totals: 26 formulas, 26 attempted, 26 succeeded (4.91 s)
Proof summary for theory ordered_finite_sequences
extract_one_TCC1......................proved - complete [shostak](0.16 s)
extract_one_TCC2......................proved - complete [shostak](0.08 s)
extract_one...........................proved - complete [shostak](0.11 s)
extract_upper_TCC1....................proved - complete [shostak](0.17 s)
extract_upper.........................proved - complete [shostak](0.14 s)
min_extract_TCC1......................proved - incomplete [shostak](0.13 s)
min_extract_TCC2......................proved - incomplete [shostak](0.09 s)
min_extract...........................proved - incomplete [shostak](0.28 s)
max_extract_TCC1......................proved - incomplete [shostak](0.10 s)
max_extract...........................proved - incomplete [shostak](0.31 s)
minmax_TCC1...........................proved - complete [shostak](0.09 s)
min_le_max............................proved - complete [shostak](0.13 s)
min_minmax............................proved - complete [shostak](0.20 s)
max_minmax............................proved - complete [shostak](0.22 s)
min_in_consensus......................proved - complete [shostak](0.09 s)
max_in_consensus......................proved - complete [shostak](0.08 s)
in_consensus..........................proved - complete [shostak](0.11 s)
lower_TCC1............................proved - complete [shostak](0.06 s)
lower_TCC2............................proved - incomplete [shostak](0.04 s)
lower_TCC3............................proved - incomplete [shostak](0.10 s)
upper_TCC1............................proved - incomplete [shostak](0.10 s)
map_set_TCC1..........................proved - complete [shostak](0.04 s)
map_set_TCC2..........................proved - incomplete [shostak](0.05 s)
map_set_TCC3..........................proved - incomplete [shostak](0.06 s)
map_subset_lower_TCC1.................proved - incomplete [shostak](0.04 s)
map_subset_lower......................proved - incomplete [shostak](0.12 s)
map_subset_upper_TCC1.................proved - incomplete [shostak](0.04 s)
map_subset_upper......................proved - incomplete [shostak](0.13 s)
mapper_TCC1...........................proved - incomplete [shostak](0.13 s)
mapper_TCC2...........................proved - incomplete [shostak](0.14 s)
map_card_eq...........................proved - incomplete [shostak](0.14 s)
card_below_set_TCC1...................proved - incomplete [shostak](0.04 s)
card_below_set........................proved - incomplete [shostak](0.29 s)
card_above_set_TCC1...................proved - incomplete [shostak](0.04 s)
card_above_set........................proved - incomplete [shostak](0.25 s)
card_lower............................proved - incomplete [shostak](0.16 s)
card_upper............................proved - incomplete [shostak](0.14 s)
sort_overlap_TCC1.....................proved - complete [shostak](0.06 s)
sort_overlap_TCC2.....................proved - incomplete [shostak](0.10 s)
sort_overlap..........................proved - incomplete [shostak](0.22 s)
leq_validity..........................proved - incomplete [shostak](0.09 s)
Theory totals: 41 formulas, 41 attempted, 41 succeeded (5.06 s)
Proof summary for theory relations_extra
strict_order_is_asymmetric............proved - complete [shostak](0.04 s)
asymmetric_is_antisymmetric...........proved - complete [shostak](0.03 s)
asymmetric_is_irreflexive.............proved - complete [shostak](0.03 s)
reflexive.............................proved - complete [shostak](0.03 s)
irreflexive...........................proved - complete [shostak](0.03 s)
symmetric.............................proved - complete [shostak](0.03 s)
antisymmetric.........................proved - complete [shostak](0.02 s)
asymmetric............................proved - complete [shostak](0.03 s)
transitive............................proved - complete [shostak](0.03 s)
dichotomous...........................proved - complete [shostak](0.03 s)
trichotomous..........................proved - complete [shostak](0.03 s)
dichotomous_is_trichotomous...........proved - complete [shostak](0.04 s)
well_founded..........................proved - complete [shostak](0.03 s)
reflexive_closure_TCC1................proved - complete [shostak](0.04 s)
irreflexive_kernel_TCC1...............proved - complete [shostak](0.04 s)
symmetric_closure_TCC1................proved - complete [shostak](0.05 s)
symmetric_kernel_TCC1.................proved - complete [shostak](0.05 s)
reflexive_closure_preserves_transitive...proved - complete [shostak](0.05 s)
strict_order_to_partial_order.........proved - complete [shostak](0.05 s)
reflexive_closure_dichotomous.........proved - complete [shostak](0.05 s)
strict_total_order_to_total_order.....proved - complete [shostak](0.06 s)
partial_order_to_strict_order.........proved - complete [shostak](0.10 s)
irreflexive_kernel_trichotomous.......proved - complete [shostak](0.09 s)
total_order_to_strict_total_order.....proved - complete [shostak](0.10 s)
symmetric_kernel_of_preorder..........proved - complete [shostak](0.14 s)
Theory totals: 25 formulas, 25 attempted, 25 succeeded (1.22 s)
Proof summary for theory select_minmax
v_min_TCC1............................proved - complete [shostak](0.09 s)
v_min_witness.........................proved - incomplete [shostak](0.10 s)
v_max_witness.........................proved - incomplete [shostak](0.09 s)
v_min_is_min..........................proved - incomplete [shostak](0.10 s)
v_max_is_max..........................proved - incomplete [shostak](0.09 s)
min_le_max............................proved - incomplete [shostak](0.18 s)
min_le_max_alt........................proved - incomplete [shostak](0.19 s)
v_minmax_choose.......................proved - incomplete [shostak](0.12 s)
v_minmax_choose_alt...................proved - incomplete [shostak](0.35 s)
Theory totals: 9 formulas, 9 attempted, 9 succeeded (1.31 s)
Proof summary for theory exact_reduce_stage
reduce_lower_validity.................proved - incomplete [shostak](0.26 s)
reduce_upper_validity.................proved - incomplete [shostak](0.25 s)
reduce_agreement_generation...........proved - incomplete [shostak](0.13 s)
reduce_min_validity...................proved - incomplete [shostak](0.38 s)
reduce_max_validity...................proved - incomplete [shostak](0.23 s)
reduce_consensus......................proved - incomplete [shostak](1.31 s)
reduce_min_eq_max.....................proved - incomplete [shostak](0.07 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (2.63 s)
Proof summary for theory reduce_synch
Delay_TCC1............................proved - complete [shostak](0.09 s)
Del_TCC1..............................proved - complete [shostak](0.09 s)
Del_Delay.............................proved - complete [shostak](0.03 s)
Lag_TCC1..............................proved - complete [shostak](0.08 s)
Delay_Lag.............................proved - complete [shostak](0.03 s)
offset_sent_nominal...................proved - complete [shostak](0.09 s)
synch_protocol_sent...................proved - incomplete [shostak](0.29 s)
k_stage_synch.........................proved - incomplete [shostak](1.24 s)
lower_validity_TCC1...................proved - incomplete [shostak](3.85 s)
lower_validity........................proved - incomplete [shostak](0.44 s)
upper_validity........................proved - incomplete [shostak](1.46 s)
agreement_propagation.................proved - incomplete [shostak](1.73 s)
convergence...........................proved - incomplete [shostak](2.94 s)
agreement_generation_TCC1.............proved - incomplete [shostak](5.74 s)
agreement_generation..................proved - incomplete [shostak](1.16 s)
agreement_generation_edge_TCC1........proved - incomplete [shostak](0.08 s)
agreement_generation_edge.............proved - incomplete [shostak](1.01 s)
Theory totals: 17 formulas, 17 attempted, 17 succeeded (20.34 s)
Proof summary for theory timing_integration
enabled_within_timing.................proved - incomplete [shostak](0.14 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.14 s)
Proof summary for theory timing_integration_stage
t_min_TCC1............................proved - incomplete [shostak](0.06 s)
uniformly_outer_exists................proved - incomplete [shostak](0.17 s)
symmetric_timing_uniform..............proved - complete [shostak](0.09 s)
uniformly_outer_single_denotation.....proved - complete [shostak](0.07 s)
good_send_TCC1........................proved - complete [shostak](0.09 s)
osym_send_TCC1........................proved - complete [shostak](0.10 s)
oasym_send_TCC1.......................proved - complete [shostak](0.11 s)
tsym_send_TCC1........................proved - incomplete [shostak](0.07 s)
sv_send_TCC1..........................proved - incomplete [shostak](0.08 s)
tsym_single_denotation................proved - incomplete [shostak](0.07 s)
received_clock_edge...................proved - incomplete [shostak](0.05 s)
enabled_within_stage..................proved - incomplete [shostak](0.06 s)
correct_denotation_send...............proved - incomplete [shostak](0.11 s)
conforming_correct_denotation_send....proved - incomplete [shostak](0.09 s)
single_denotation_send................proved - incomplete [shostak](0.45 s)
symmetric_send........................proved - incomplete [shostak](0.06 s)
symmetric_timing_conforms.............proved - incomplete [shostak](0.63 s)
correct_lower_timing..................proved - incomplete [shostak](0.07 s)
correct_quorum_lower..................proved - incomplete [shostak](0.05 s)
correct_majority_lower................proved - incomplete [shostak](0.05 s)
correct_upper_timing..................proved - incomplete [shostak](0.06 s)
correct_majority_upper................proved - incomplete [shostak](0.21 s)
correct_quorum_upper..................proved - incomplete [shostak](0.05 s)
correct_accuracy_timing...............proved - incomplete [shostak](0.06 s)
correct_imprecision_timing............proved - incomplete [shostak](0.67 s)
quorum_imprecision....................proved - incomplete [shostak](0.05 s)
majority_imprecision..................proved - incomplete [shostak](0.05 s)
single_imprecision_timing.............proved - incomplete [shostak](0.18 s)
uniformly_enabled.....................proved - incomplete [shostak](0.09 s)
symmetric_imprecision_timing..........proved - incomplete [shostak](0.27 s)
all_symmetric_timing..................proved - incomplete [shostak](0.06 s)
Theory totals: 31 formulas, 31 attempted, 31 succeeded (4.26 s)
Proof summary for theory timing_window
timing_conforms_def...................proved - complete [shostak](0.11 s)
good_range_always_conforms............proved - complete [shostak](0.46 s)
good_range_inner_window...............proved - complete [shostak](0.04 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.60 s)
Proof summary for theory timing_imprecision
mid_latency_ge_one_half...............proved - complete [shostak](0.07 s)
W_TCC1................................proved - complete [shostak](0.09 s)
W_TCC2................................proved - complete [shostak](0.09 s)
drift_relation_alt....................proved - complete [shostak](0.13 s)
W_bound...............................proved - complete [shostak](0.22 s)
W_bound_alt...........................proved - complete [shostak](0.10 s)
epsilon_l_TCC1........................proved - complete [shostak](0.08 s)
epsilon_u_TCC1........................proved - complete [shostak](0.09 s)
max_error_TCC1........................proved - complete [shostak](0.20 s)
epsilon_relation......................proved - complete [shostak](0.10 s)
event_observation_error...............proved - complete [shostak](0.12 s)
link_lower_range......................proved - complete [shostak](0.21 s)
link_upper_range......................proved - complete [shostak](0.25 s)
link_abs_bound........................proved - complete [shostak](0.15 s)
link_relative_range...................proved - complete [shostak](0.16 s)
link_relative_symmetry................proved - complete [shostak](0.23 s)
good_range_bounded....................proved - complete [shostak](0.07 s)
link_symmetry.........................proved - complete [shostak](0.12 s)
Theory totals: 18 formulas, 18 attempted, 18 succeeded (2.46 s)
Proof summary for theory inverse_clocks
lower_Clocktime_exists................proved - complete [shostak](0.16 s)
upper_Clocktime_exists................proved - complete [shostak](0.13 s)
past_ticks_max_set....................proved - complete [shostak](0.11 s)
Clock_rewrite.........................proved - complete [shostak](0.06 s)
Clock_lower...........................proved - complete [shostak](0.06 s)
Clock_upper...........................proved - complete [shostak](0.08 s)
Clock_nondecreasing...................proved - complete [shostak](0.10 s)
alt_clock_edge........................proved - complete [shostak](0.04 s)
conversion_left.......................proved - complete [shostak](0.04 s)
conversion_left_alt...................proved - complete [shostak](0.09 s)
conversion_right......................proved - complete [shostak](0.09 s)
obs_bound.............................proved - complete [shostak](0.09 s)
precision_conversion_sym..............proved - complete [shostak](0.39 s)
precision_conversion..................proved - complete [shostak](0.33 s)
lower_accuracy_conversion.............proved - complete [shostak](0.26 s)
upper_accuracy_conversion.............proved - complete [shostak](0.19 s)
Theory totals: 16 formulas, 16 attempted, 16 succeeded (2.20 s)
Proof summary for theory physical_clocks
drift_TCC1............................proved - complete [shostak](0.13 s)
drift_def.............................proved - complete [shostak](0.08 s)
drift_bound...........................proved - complete [shostak](0.54 s)
good_clock_TCC1.......................proved - complete [shostak](0.07 s)
drift_left_nat........................proved - complete [shostak](0.19 s)
drift_right_nat.......................proved - complete [shostak](0.22 s)
drift_left............................proved - complete [shostak](0.19 s)
drift_right...........................proved - complete [shostak](0.19 s)
abs_drift_lb..........................proved - complete [shostak](0.12 s)
clock_nondecreasing...................proved - complete [shostak](0.08 s)
clock_increasing......................proved - complete [shostak](0.08 s)
clock_nondecreasing_alt...............proved - complete [shostak](0.03 s)
clock_eq_arg..........................proved - complete [shostak](0.03 s)
relative_drift........................proved - complete [shostak](0.15 s)
nonoverlap_basis......................proved - complete [shostak](0.15 s)
skew_basis_0..........................proved - complete [shostak](0.16 s)
skew_bound_1..........................proved - complete [shostak](0.28 s)
skew_bound_2..........................proved - complete [shostak](0.27 s)
skew_bound............................proved - complete [shostak](0.20 s)
lower_offset..........................proved - complete [shostak](0.19 s)
upper_offset..........................proved - complete [shostak](0.23 s)
Theory totals: 21 formulas, 21 attempted, 21 succeeded (3.56 s)
Proof summary for theory abs_props
abs_max...............................proved - complete [shostak](0.04 s)
abs_add...............................proved - complete [shostak](0.10 s)
abs_le_nonneg.........................proved - complete [shostak](0.05 s)
abs_diff_commutes.....................proved - complete [shostak](0.05 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.24 s)
Proof summary for theory minmax_ineq
min_le................................proved - complete [shostak](0.04 s)
min_lt................................proved - complete [shostak](0.04 s)
min_ge................................proved - complete [shostak](0.04 s)
min_gt................................proved - complete [shostak](0.05 s)
le_min................................proved - complete [shostak](0.05 s)
lt_min................................proved - complete [shostak](0.04 s)
ge_min................................proved - complete [shostak](0.04 s)
gt_min................................proved - complete [shostak](0.05 s)
max_le................................proved - complete [shostak](0.04 s)
max_lt................................proved - complete [shostak](0.03 s)
max_ge................................proved - complete [shostak](0.04 s)
max_gt................................proved - complete [shostak](0.03 s)
le_max................................proved - complete [shostak](0.04 s)
lt_max................................proved - complete [shostak](0.04 s)
ge_max................................proved - complete [shostak](0.03 s)
gt_max................................proved - complete [shostak](0.04 s)
max_triangle..........................proved - complete [shostak](0.07 s)
min_commutative.......................proved - complete [shostak](0.04 s)
max_commutative.......................proved - complete [shostak](0.03 s)
Theory totals: 19 formulas, 19 attempted, 19 succeeded (0.78 s)
Proof summary for theory floor_ceiling_ineq
ge_floor_l............................proved - complete [shostak](0.05 s)
ge_floor_r............................proved - complete [shostak](0.07 s)
gt_floor_l............................proved - complete [shostak](0.06 s)
gt_floor_r............................proved - complete [shostak](0.05 s)
le_floor_l............................proved - complete [shostak](0.06 s)
le_floor_r............................proved - complete [shostak](0.06 s)
lt_floor_l............................proved - complete [shostak](0.06 s)
lt_floor_r............................proved - complete [shostak](0.06 s)
floor_monotone........................proved - complete [shostak](0.03 s)
ge_ceiling_l..........................proved - complete [shostak](0.06 s)
ge_ceiling_r..........................proved - complete [shostak](0.05 s)
gt_ceiling_l..........................proved - complete [shostak](0.05 s)
gt_ceiling_r..........................proved - complete [shostak](0.05 s)
le_ceiling_l..........................proved - complete [shostak](0.05 s)
le_ceiling_r..........................proved - complete [shostak](0.06 s)
lt_ceiling_l..........................proved - complete [shostak](0.05 s)
lt_ceiling_r..........................proved - complete [shostak](0.05 s)
ceiling_monotone......................proved - complete [shostak](0.03 s)
Theory totals: 18 formulas, 18 attempted, 18 succeeded (0.95 s)
Proof summary for theory bounded_ints
sup_int_int...........................proved - complete [shostak](0.06 s)
sup_int_in_set........................proved - complete [shostak](0.07 s)
sup_int_is_in_set.....................proved - complete [shostak](0.04 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.17 s)
Proof summary for theory inexact_comm_stage
majority_lower_rw.....................proved - incomplete [shostak](0.04 s)
majority_upper_rw.....................proved - incomplete [shostak](0.04 s)
quorum_accuracy.......................proved - incomplete [shostak](0.04 s)
majority_accuracy.....................proved - incomplete [shostak](0.05 s)
majority_accuracy_rw..................proved - incomplete [shostak](0.04 s)
quorum_imprecision_nonempty...........proved - incomplete [shostak](0.04 s)
majority_imprecision_rw...............proved - incomplete [shostak](0.04 s)
correct_imprecision...................proved - incomplete [shostak](0.19 s)
rcvd_diameter.........................proved - incomplete [shostak](0.40 s)
Theory totals: 9 formulas, 9 attempted, 9 succeeded (0.88 s)
Proof summary for theory real_finite_sequences
diameter?_TCC1........................proved - complete [shostak](0.12 s)
agreement_propagation.................proved - complete [shostak](0.07 s)
similar?_TCC1.........................proved - complete [shostak](0.05 s)
similar_sort_TCC1.....................proved - incomplete [shostak](0.09 s)
similar_sort_TCC2.....................proved - incomplete [shostak](0.08 s)
similar_sort..........................proved - incomplete [shostak](0.12 s)
sum_TCC1..............................proved - complete [shostak](0.03 s)
sum_TCC2..............................proved - complete [shostak](0.04 s)
sum_TCC3..............................proved - complete [shostak](0.05 s)
sum_lower.............................proved - complete [shostak](0.76 s)
sum_upper.............................proved - complete [shostak](0.69 s)
mean_TCC1.............................proved - complete [shostak](0.03 s)
min_le_mean...........................proved - complete [shostak](0.29 s)
mean_le_max...........................proved - complete [shostak](0.30 s)
midpoint_def..........................proved - complete [shostak](1.81 s)
mean_lower............................proved - complete [shostak](0.52 s)
mean_upper............................proved - complete [shostak](0.53 s)
mean_consensus........................proved - complete [shostak](0.13 s)
midpoint_consensus....................proved - complete [shostak](0.19 s)
inexact_min...........................proved - incomplete [shostak](0.11 s)
inexact_max...........................proved - incomplete [shostak](0.13 s)
inexact_choose........................proved - complete [shostak](0.08 s)
inexact_mean..........................proved - complete [shostak](6.87 s)
inexact_midpoint......................proved - incomplete [shostak](0.23 s)
mean_convergence......................proved - complete [shostak](0.40 s)
midpoint_convergence..................proved - complete [shostak](1.17 s)
convergent_mean.......................proved - complete [shostak](0.62 s)
convergent_midpoint...................proved - complete [shostak](0.12 s)
Theory totals: 28 formulas, 28 attempted, 28 succeeded (15.62 s)
Proof summary for theory inexact_comm
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory reduce_synch_stage
synch_stage_offset....................proved - incomplete [shostak](0.12 s)
lower_synch_validity..................proved - incomplete [shostak](1.22 s)
upper_synch_validity..................proved - incomplete [shostak](1.59 s)
synch_master_slave....................proved - incomplete [shostak](1.47 s)
synch_agreement_propagation...........proved - incomplete [shostak](2.13 s)
overlap_imprecision...................proved - incomplete [shostak](0.23 s)
synch_convergence.....................proved - incomplete [shostak](2.38 s)
synch_agreement_generation............proved - incomplete [shostak](1.13 s)
synch_agreement_generation_edge.......proved - incomplete [shostak](1.22 s)
Theory totals: 9 formulas, 9 attempted, 9 succeeded (11.48 s)
Proof summary for theory clock_shift
offset_left_edge......................proved - complete [shostak](0.09 s)
offset_left...........................proved - complete [shostak](0.18 s)
offset_right_edge.....................proved - complete [shostak](0.10 s)
offset_right..........................proved - complete [shostak](0.11 s)
offset_zero...........................proved - complete [shostak](0.05 s)
offset_drift..........................proved - complete [shostak](0.28 s)
offset_nondecreasing..................proved - complete [shostak](0.09 s)
offset_drift_edge.....................proved - complete [shostak](0.14 s)
double_offset.........................proved - complete [shostak](0.10 s)
offset_same...........................proved - complete [shostak](0.35 s)
offset_same2..........................proved - complete [shostak](0.04 s)
Theory totals: 11 formulas, 11 attempted, 11 succeeded (1.53 s)
Proof summary for theory inexact_reduce_stage
reduce_lower_validity.................proved - incomplete [shostak](0.31 s)
reduce_upper_validity.................proved - incomplete [shostak](0.29 s)
reduce_master_slave...................proved - incomplete [shostak](0.23 s)
reduce_agreement_propagation..........proved - incomplete [shostak](0.33 s)
convergence_overlap...................proved - incomplete [shostak](0.29 s)
reduce_convergence....................proved - incomplete [shostak](0.41 s)
reduce_agreement_generation...........proved - incomplete [shostak](0.32 s)
reduce_min_validity...................proved - incomplete [shostak](0.29 s)
reduce_max_validity...................proved - incomplete [shostak](0.13 s)
minmax_diameter.......................proved - incomplete [shostak](0.11 s)
agreement_propagation.................proved - incomplete [shostak](0.59 s)
agreement_generation..................proved - incomplete [shostak](0.08 s)
convergence...........................proved - incomplete [shostak](0.61 s)
Theory totals: 13 formulas, 13 attempted, 13 succeeded (3.98 s)
Proof summary for theory inexact_reduce
lower_validity_TCC1...................proved - incomplete [shostak](2.34 s)
lower_validity_TCC2...................proved - incomplete [shostak](2.43 s)
lower_validity........................proved - incomplete [shostak](1.15 s)
upper_validity_TCC1...................proved - incomplete [shostak](2.35 s)
upper_validity_TCC2...................proved - incomplete [shostak](2.45 s)
upper_validity........................proved - incomplete [shostak](1.03 s)
agreement_propagation_TCC1............proved - incomplete [shostak](6.17 s)
agreement_propagation_TCC2............proved - incomplete [shostak](5.40 s)
agreement_propagation.................proved - incomplete [shostak](2.18 s)
convergence...........................proved - incomplete [shostak](2.32 s)
agreement_generation_TCC1.............proved - incomplete [shostak](3.99 s)
agreement_generation_TCC2.............proved - incomplete [shostak](4.23 s)
agreement_generation..................proved - incomplete [shostak](0.78 s)
Theory totals: 13 formulas, 13 attempted, 13 succeeded (36.81 s)
Proof summary for theory convergence_top
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory median_stage
one_asymmetric_overlap................proved - incomplete [shostak](0.28 s)
median_convergence....................proved - incomplete [shostak](0.20 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.48 s)
Proof summary for theory median_overlap
median_overlap........................proved - incomplete [shostak](0.42 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.42 s)
Proof summary for theory middle_third_stage
byzantine_overlap.....................proved - incomplete [shostak](0.45 s)
middle_third_convergence..............proved - incomplete [shostak](0.16 s)
mean_convergence......................proved - incomplete [shostak](0.18 s)
midpoint_convergence..................proved - incomplete [shostak](0.17 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.95 s)
Proof summary for theory middle_third_overlap
middle_third_overlap..................proved - incomplete [shostak](0.42 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.42 s)
Proof summary for theory middle_third_pigeonhole
middle_third_pigeonhole...............proved - complete [shostak](0.45 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.45 s)
Proof summary for theory pigeonhole_int
disjoint1.............................proved - complete [shostak](0.04 s)
disjoint2.............................proved - complete [shostak](0.05 s)
complement_complement.................proved - complete [shostak](0.02 s)
mirror_TCC1...........................proved - complete [shostak](0.03 s)
mirror_mirror.........................proved - complete [shostak](0.07 s)
card_mirror...........................proved - complete [shostak](0.05 s)
subset_mirror.........................proved - complete [shostak](0.04 s)
mirror_nat............................proved - complete [shostak](0.07 s)
mirror_negint.........................proved - complete [shostak](0.07 s)
subset_split..........................proved - complete [shostak](0.08 s)
card_split............................proved - complete [shostak](0.19 s)
two_thirds_split......................proved - complete [shostak](0.12 s)
two_thirds_overlap_lem................proved - complete [shostak](0.07 s)
fta_overlap_pigeonhole................proved - complete [shostak](0.52 s)
Theory totals: 14 formulas, 14 attempted, 14 succeeded (1.42 s)
Proof summary for theory weber_stage
overlap_imprecision...................proved - incomplete [shostak](0.28 s)
weber_convergence.....................proved - incomplete [shostak](0.09 s)
weber_mean_convergence................proved - incomplete [shostak](0.30 s)
weber_midpoint_convergence............proved - incomplete [shostak](0.16 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.83 s)
Proof summary for theory weber_overlap
weber_overlap.........................proved - incomplete [shostak](0.69 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.69 s)
Proof summary for theory virtual_clock_top
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory virtual_clock_1
turns_TCC1............................proved - complete [shostak](0.25 s)
turns_increasing......................proved - complete [shostak](0.40 s)
turns_unbounded.......................proved - complete [shostak](0.30 s)
turns_event_sequence..................proved - complete [shostak](0.03 s)
turns_nonoverlap......................proved - complete [shostak](0.52 s)
turns_early...........................proved - complete [shostak](0.37 s)
turns_self............................proved - complete [shostak](0.09 s)
turns_cross...........................proved - complete [shostak](0.51 s)
VC1_j_TCC1............................proved - complete [shostak](0.03 s)
VC1_j.................................proved - complete [shostak](0.03 s)
VC1_precision_TCC1....................proved - incomplete [shostak](0.05 s)
VC1_precision_TCC2....................proved - incomplete [shostak](0.04 s)
VC1_precision.........................proved - incomplete [shostak](0.62 s)
VC1_accuracy_lower_TCC1...............proved - incomplete [shostak](0.04 s)
VC1_accuracy_lower....................proved - incomplete [shostak](1.57 s)
VC1_optimal_accuracy_lower............proved - incomplete [shostak](0.87 s)
VC1_accuracy_upper....................proved - incomplete [shostak](1.13 s)
VC1_optimal_accuracy_upper............proved - incomplete [shostak](0.65 s)
Theory totals: 18 formulas, 18 attempted, 18 succeeded (7.49 s)
Proof summary for theory synch_protocol_invariants
all_periodic_precision_iff_peer_precision...proved - incomplete [shostak](0.04 s)
all_periodic_precision................proved - incomplete [shostak](0.09 s)
minmax_adjustment_lower_bound.........proved - incomplete [shostak](0.10 s)
minmax_adjustment_upper_bound.........proved - incomplete [shostak](0.10 s)
min_le_trace..........................proved - incomplete [shostak](0.04 s)
trace_le_max..........................proved - incomplete [shostak](0.04 s)
trace_diff............................proved - incomplete [shostak](0.05 s)
traces_peer_precision.................proved - incomplete [shostak](0.42 s)
traces_lower..........................proved - incomplete [shostak](0.14 s)
traces_upper..........................proved - incomplete [shostak](0.48 s)
traces_compatible.....................proved - incomplete [shostak](0.29 s)
trace_lower_accuracy..................proved - incomplete [shostak](0.22 s)
trace_upper_accuracy..................proved - incomplete [shostak](0.11 s)
trace_weakly_accurate.................proved - incomplete [shostak](0.34 s)
Theory totals: 14 formulas, 14 attempted, 14 succeeded (2.45 s)
Proof summary for theory synch_constant_definitions
P_bound...............................proved - complete [shostak](0.21 s)
rho_bound.............................proved - complete [shostak](3.29 s)
ADJ_ineq..............................proved - complete [shostak](0.17 s)
ADJ_ineq_l............................proved - complete [shostak](0.45 s)
ADJ_ineq_h............................proved - complete [shostak](0.45 s)
ADJ_bound.............................proved - complete [shostak](0.17 s)
P_min_TCC1............................proved - complete [shostak](0.03 s)
p_min_bound...........................proved - complete [shostak](0.16 s)
p_lower_TCC1..........................proved - complete [shostak](0.22 s)
p_min_TCC1............................proved - complete [shostak](0.23 s)
p_min_lower...........................proved - complete [shostak](0.03 s)
p_max_upper...........................proved - complete [shostak](0.03 s)
drift_P_bound.........................proved - complete [shostak](0.30 s)
Pi_TCC1...............................proved - complete [shostak](0.19 s)
Theory totals: 14 formulas, 14 attempted, 14 succeeded (5.91 s)
Proof summary for theory synch_parameter_constraints
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory clock_minmax
clock_min_witness.....................proved - incomplete [shostak](0.07 s)
clock_max_witness.....................proved - incomplete [shostak](0.06 s)
clock_min_is_min......................proved - incomplete [shostak](0.06 s)
clock_max_is_max......................proved - incomplete [shostak](0.05 s)
clock_min_clock.......................proved - incomplete [shostak](0.32 s)
clock_max_clock.......................proved - incomplete [shostak](0.11 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.66 s)
Proof summary for theory function_image_nonempty
nonempty_image........................proved - complete [shostak](0.05 s)
nonempty_finite_image.................proved - complete [shostak](0.03 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.08 s)
Proof summary for theory interval_clocks
T_def.................................proved - complete [shostak](0.09 s)
T_rounds..............................proved - complete [shostak](0.09 s)
handover_precision_lower..............proved - complete [shostak](0.22 s)
handover_precision_upper..............proved - complete [shostak](0.21 s)
handover_precision....................proved - complete [shostak](0.31 s)
nonoverlap_peers......................proved - complete [shostak](0.18 s)
nonoverlap_lower......................proved - complete [shostak](0.34 s)
nonoverlap_upper......................proved - complete [shostak](0.34 s)
nonoverlap_round......................proved - complete [shostak](0.43 s)
lower_interval_accuracy...............proved - complete [shostak](0.20 s)
upper_interval_accuracy...............proved - complete [shostak](0.20 s)
Theory totals: 11 formulas, 11 attempted, 11 succeeded (2.59 s)
Proof summary for theory virtual_clocks
VC_j..................................proved - complete [shostak](0.03 s)
observable_peers......................proved - complete [shostak](0.19 s)
observable_master.....................proved - complete [shostak](0.13 s)
observable_slave......................proved - complete [shostak](0.14 s)
adjustment_nonoverlap.................proved - complete [shostak](0.17 s)
VC_precision_0........................proved - complete [shostak](0.40 s)
VC_precision_1........................proved - complete [shostak](0.56 s)
VC_precision_sym......................proved - complete [shostak](0.31 s)
VC_precision..........................proved - complete [shostak](0.11 s)
index_upper_bound.....................proved - complete [shostak](0.26 s)
VC_lower_accuracy.....................proved - complete [shostak](1.60 s)
VC_upper_accuracy.....................proved - complete [shostak](0.93 s)
Theory totals: 12 formulas, 12 attempted, 12 succeeded (4.82 s)
Proof summary for theory event_sequences
increasing_ind........................proved - complete [shostak](0.10 s)
nondecreasing.........................proved - complete [shostak](0.07 s)
future_events_nonempty................proved - complete [shostak](0.06 s)
index_le..............................proved - complete [shostak](0.07 s)
lt_index..............................proved - complete [shostak](0.06 s)
index_le_alt..........................proved - complete [shostak](0.07 s)
index_rewrite.........................proved - complete [shostak](0.08 s)
index_conversion_left.................proved - complete [shostak](0.06 s)
index_conversion_right................proved - complete [shostak](0.06 s)
index_ordered.........................proved - complete [shostak](0.04 s)
cross_nondecreasing...................proved - complete [shostak](0.06 s)
nonoverlap_index_bound................proved - complete [shostak](0.10 s)
Theory totals: 12 formulas, 12 attempted, 12 succeeded (0.83 s)
Proof summary for theory virtual_clock_2
t_increasing..........................proved - complete [shostak](0.07 s)
t_unbounded...........................proved - complete [shostak](0.29 s)
t_event_sequence......................proved - complete [shostak](0.03 s)
t_nonoverlap..........................proved - complete [shostak](0.19 s)
t_early...............................proved - complete [shostak](0.04 s)
t_self................................proved - complete [shostak](0.29 s)
t_cross...............................proved - complete [shostak](0.36 s)
VC_j..................................proved - complete [shostak](0.05 s)
VC2_precision_TCC1....................proved - incomplete [shostak](0.05 s)
VC2_precision_TCC2....................proved - incomplete [shostak](0.05 s)
VC2_precision.........................proved - incomplete [shostak](0.60 s)
VC2_accuracy_lower_TCC1...............proved - incomplete [shostak](0.04 s)
VC2_accuracy_lower....................proved - incomplete [shostak](1.12 s)
VC2_optimal_accuracy_lower............proved - incomplete [shostak](0.52 s)
VC2_accuracy_upper....................proved - incomplete [shostak](0.83 s)
VC2_optimal_accuracy_upper............proved - incomplete [shostak](0.44 s)
Theory totals: 16 formulas, 16 attempted, 16 succeeded (4.96 s)
Grand Totals: 593 proofs, 593 attempted, 593 succeeded (174.57 s)
[ Verzeichnis aufwärts0.28unsichere Verbindung
Übersetzung europäischer Sprachen durch Browser
]
|
