| products/sources/formale Sprachen/PVS/fault_tolerance/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Sprache: LispUntersuchung PVS© |
|
||||||
|
(reduce_synch
(Delay_TCC1 0 (Delay_TCC1-2 nil 3397908417 ("" (skosimp* t) (("" (expand "feasible?") (("" (assert) (("" (inst - "i!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (integer nonempty-type-from-decl nil integers nil) (feasible? const-decl "bool" reduce_synch nil)) nil) (Delay_TCC1-1 nil 3397907770 ("" (subtype-tcc) nil nil) nil nil)) (Del_TCC1 0 (Del_TCC1-2 nil 3397908432 ("" (expand "pred") (("" (skosimp*) (("" (lift-if) (("" (assert) (("" (typepred "Sched!1") (("" (expand "feasible?") (("" (expand "W") (("" (inst - "i!1-1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (i!1 skolem-const-decl "nat" reduce_synch nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (W const-decl "nat" reduce_synch nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (integer nonempty-type-from-decl nil integers nil) (feasible? const-decl "bool" reduce_synch nil) (pred const-decl "nat" naturalnumbers nil)) nil) (Del_TCC1-1 nil 3397907770 ("" (subtype-tcc) nil nil) nil nil)) (Del_Delay 0 (Del_Delay-1 nil 3397908176 ("" (expand "Del") (("" (expand "pred") (("" (expand "Delay") (("" (propax) nil nil)) nil)) nil)) nil) ((pred const-decl "nat" naturalnumbers nil) (Delay const-decl "nat" reduce_synch nil) (Del const-decl "nat" reduce_synch nil)) nil)) (Lag_TCC1 0 (Lag_TCC1-2 nil 3397908450 ("" (skosimp* t) (("" (expand "Delay") (("" (expand "feasible?") (("" (inst - "i!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((Delay const-decl "nat" reduce_synch nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (integer nonempty-type-from-decl nil integers nil) (feasible? const-decl "bool" reduce_synch nil)) nil) (Lag_TCC1-1 nil 3397907770 ("" (subtype-tcc) nil nil) nil nil)) (Delay_Lag 0 (Delay_Lag-2 nil 3397908241 ("" (expand "Lag") (("" (propax) nil nil)) nil) ((Lag const-decl "nat" reduce_synch nil)) nil) (Delay_Lag-1 nil 3397908197 (";;; Proof for formula k_synch.Del_Delay" (expand "Del") ((";;; Proof for formula k_synch.Del_Delay" (expand "pred") ((";;; Proof for formula k_synch.Del_Delay" (expand "Delay") ((";;; Proof for formula k_synch.Del_Delay" (propax) nil)))))) "") nil nil)) (offset_sent_nominal 0 (offset_sent_nominal-1 nil 3397908260 ("" (skosimp*) (("" (apply-extensionality :hide? t) (("" (expand "nominal") (("" (expand "W") (("" (expand "nominal") (("" (expand "offset") (("" (expand "sent") (("" (expand "sent") (("" (rewrite "Clock_rewrite") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (stage formal-const-decl "[nat -> posnat]" reduce_synch nil) (below type-eq-decl nil naturalnumbers nil) (sent const-decl "[below(stage(i)) -> real]" timing_integration nil) (W const-decl "nat" reduce_synch nil) (offset const-decl "real" clock_shift nil) (nominal const-decl "[below(stage(i)) -> real]" timing_integration nil) (var_latency formal-const-decl "[nat -> nonneg_real]" reduce_synch nil) (min_latency formal-const-decl "[nat -> nonneg_real]" reduce_synch nil) (integer nonempty-type-from-decl nil integers nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rate const-decl "posreal" physical_clocks nil) (rho formal-const-decl "nonneg_real" reduce_synch nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (sent const-decl "real" timing_integration_stage nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (Clock_rewrite formula-decl nil inverse_clocks nil) (posint nonempty-type-eq-decl nil integers nil) (W const-decl "posint" timing_imprecision nil) (nominal const-decl "real" timing_integration_stage nil)) nil)) (synch_protocol_sent 0 (synch_protocol_sent-1 nil 3397908283 ("" (skosimp*) (("" (expand "synch_protocol") (("" (inst - "i!1") (("" (assert) (("" (expand "same_clock?") (("" (inst - "i!1") (("" (assert) (("" (rewrite "offset_sent_nominal") (("" (rewrite "Delay_Lag") (("" (lemma "synch_stage_offset[rho, min_latency(i!1), var_latency(i!1), stage(i!1), stage(1 (("" (inst - "W(i!1+1)" _ _ _ _ _ _ _ _ _) (("" (assert) (("" (inst?) (("" (replace -1 :hide? t) (("" (lemma "offset_same2[rho, stage(i!1+1)]") (("" (inst?) (("" (assert) (("" (hide-all-but 1) (("" (split) (("1" (expand "all_clock_edge?") (("1" (skosimp*) (("1" (expand "clock_edge?") (("1" (expand "sent") (("1" (expand "sent") (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "all_clock_edge?") (("2" (skosimp*) (("2" (expand "clock_edge?") (("2" (expand "synch_stage") (("2" (expand "offset") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((synch_protocol const-decl "bool" reduce_synch nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (offset_sent_nominal formula-decl nil reduce_synch nil) (integer nonempty-type-from-decl nil integers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (stage formal-const-decl "[nat -> posnat]" reduce_synch nil) (below type-eq-decl nil naturalnumbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (rho formal-const-decl "nonneg_real" reduce_synch nil) (rate const-decl "posreal" physical_clocks nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (synch_stage_offset formula-decl nil reduce_synch_stage nil) (min_latency formal-const-decl "[nat -> nonneg_real]" reduce_synch nil) (var_latency formal-const-decl "[nat -> nonneg_real]" reduce_synch nil) (int_minus_int_is_int application-judgement "int" integers nil) (synch_stage const-decl "real" reduce_synch_stage nil) (sent const-decl "[below(stage(i)) -> real]" timing_integration nil) (offset const-decl "real" clock_shift nil) (int_plus_int_is_int application-judgement "int" integers nil) (check const-decl "bool" timing_integration_stage nil) (received const-decl "real" timing_integration_stage nil) (reduce_choice const-decl "T" reduce_choice nil) (check_stage type-eq-decl nil node_functions_stage nil) (rcvd_matrix_stage type-eq-decl nil node_functions_stage nil) (C const-decl "int" inverse_clocks nil) (all_clock_edge? const-decl "bool" clock_shift nil) (clock_edge? const-decl "bool" physical_clocks nil) (sent const-decl "real" timing_integration_stage nil) (W const-decl "posint" timing_imprecision nil) (posint nonempty-type-eq-decl nil integers nil) (offset_same2 formula-decl nil clock_shift nil) (tau_type type-eq-decl nil tau_declaration nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (node_status type-eq-decl nil integration_fault_model nil) (fault_class type-decl nil integration_fault_model nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (k_consensus_function type-eq-decl nil k_ordered nil) (consensus_function type-eq-decl nil ordered_finite_sequences nil) (max const-decl "{t: T | (FORALL (ii: dom(s)): seq(s)(ii) <= t) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" max_seq "structures/") (dom type-eq-decl nil max_seq "structures/") (min const-decl "{t: T | (FORALL (ii: dom(s)): t <= seq(s)(ii)) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (dom type-eq-decl nil min_seq "structures/") (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (ne_seqs type-eq-decl nil seqs "structures/") (Lag const-decl "nat" reduce_synch nil) (W const-decl "nat" reduce_synch nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (Delay_Lag formula-decl nil reduce_synch nil) (feasible? const-decl "bool" reduce_synch nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (same_clock? const-decl "bool" reduce_synch nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) nil)) (k_stage_synch 0 (k_stage_synch-1 nil 3397908305 ("" (skosimp*) (("" (expand "protocol_synch") (("" (expand "protocol") (("" (expand "synch_protocol") (("" (expand "reduce_choice") (("" (expand "synch_stage") (("" (expand "offset") (("" (expand "offset") (("" (expand "check" 1 1) (("" (expand "received" 1 1) (("" (prop) (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (replace -1 :hide? t) (("1" (apply-extensionality :hide? t) (("1" (rewrite "Del_Delay") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) (("2" (assert) (("2" (replace -1 :hide? t) (("2" (apply-extensionality :hide? t) (("2" (rewrite "Del_Delay") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((protocol_synch const-decl "bool" reduce_synch nil) (synch_protocol const-decl "bool" reduce_synch nil) (synch_stage const-decl "real" reduce_synch_stage nil) (received const-decl "[below(stage(i + 1)) -> [below(stage(i)) -> real]]" timing_integration nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (stage formal-const-decl "[nat -> posnat]" reduce_synch nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals nil) (Delay const-decl "nat" reduce_synch nil) (Del const-decl "nat" reduce_synch nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (check const-decl "bool" timing_integration_stage nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (feasible? const-decl "bool" reduce_synch nil) (received const-decl "real" timing_integration_stage nil) (var_latency formal-const-decl "[nat -> nonneg_real]" reduce_synch nil) (min_latency formal-const-decl "[nat -> nonneg_real]" reduce_synch nil) (node_status type-eq-decl nil integration_fault_model nil) (fault_class type-decl nil integration_fault_model nil) (integer nonempty-type-from-decl nil integers nil) (k_consensus_function type-eq-decl nil k_ordered nil) (reduce_choice const-decl "T" reduce_choice nil) (check_stage type-eq-decl nil node_functions_stage nil) (rcvd_matrix_stage type-eq-decl nil node_functions_stage nil) (consensus_function type-eq-decl nil ordered_finite_sequences nil) (max const-decl "{t: T | (FORALL (ii: dom(s)): seq(s)(ii) <= t) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" max_seq "structures/") (dom type-eq-decl nil max_seq "structures/") (min const-decl "{t: T | (FORALL (ii: dom(s)): t <= seq(s)(ii)) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (dom type-eq-decl nil min_seq "structures/") (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (ne_seqs type-eq-decl nil seqs "structures/") (tau_type type-eq-decl nil tau_declaration nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (C const-decl "int" inverse_clocks nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (rate const-decl "posreal" physical_clocks nil) (rho formal-const-decl "nonneg_real" reduce_synch nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (int_plus_int_is_int application-judgement "int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (Del_Delay formula-decl nil reduce_synch nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (check const-decl "[below(stage(i + 1)) -> [below(stage(i)) -> [real -> bool]]]" timing_integration nil) (offset const-decl "compute_stage[stage(i), real]" reduce_synch nil) (offset const-decl "real" clock_shift nil) (reduce_choice const-decl "choice_function" k_ordered nil) (protocol const-decl "bool" protocol nil)) nil)) (lower_validity_TCC1 0 (lower_validity_TCC1-1 nil 3397907770 ("" (subtype-tcc) nil nil) ((NOT const-decl "[bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (clock_relation? const-decl "bool" timing_integration_stage nil) (stage formal-const-decl "[nat -> posnat]" reduce_synch nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (var_latency formal-const-decl "[nat -> nonneg_real]" reduce_synch nil) (min_latency formal-const-decl "[nat -> nonneg_real]" reduce_synch nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rho formal-const-decl "nonneg_real" reduce_synch nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (clock_relation? const-decl "bool" timing_integration nil) (max const-decl "T" bounded_reals "reals/") (C const-decl "int" inverse_clocks nil) (Timestamp const-decl "integer" timing_imprecision nil) (received const-decl "real" timing_integration_stage nil) (rate const-decl "posreal" physical_clocks nil) (epsilon const-decl "posreal" timing_imprecision nil) (mid_latency const-decl "posreal" timing_imprecision nil) (fractional const-decl "{x | 0 <= x & x < 1}" floor_ceil nil) (epsilon_l const-decl "posreal" timing_imprecision nil) (max_latency const-decl "posreal" timing_imprecision nil) (epsilon_u const-decl "nnreal" timing_imprecision nil) (max_error const-decl "posreal" timing_imprecision nil) (Delta_max const-decl "nat" timing_window nil) (timing_conforms? const-decl "bool" timing_window nil) (check const-decl "bool" timing_integration_stage nil) (enabled const-decl "finite_set[below(S)]" fault_assumptions_stage nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (quorum? const-decl "bool" pigeonhole nil) (quorum? const-decl "bool" fault_assumptions_stage nil) (quorum_synch? const-decl "bool" timing_integration_stage nil) (quorum_synch? const-decl "bool" timing_integration nil) (nominal const-decl "[below(stage(i)) -> real]" timing_integration nil) (Delay const-decl "nat" reduce_synch nil) (synch_protocol const-decl "bool" reduce_synch nil) (W const-decl "nat" reduce_synch nil) (feasible? const-decl "bool" reduce_synch nil) (real_minus_real_is_real application-judgement "real" reals nil) (sup_int_is_in_set application-judgement "(SS)" bounded_ints nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (posreal_times_posreal_is_posreal application-judgement "posreal" real_types nil) (posreal_plus_nnreal_is_posreal application-judgement "posreal" real_types nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil)) nil)) (lower_validity 0 (lower_validity-1 nil 3397908619 ("" (induct "k") (("1" (skosimp*) (("1" (expand "sigma") (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (rewrite "sigma_last") (("2" (inst?) (("2" (inst - "c_dst!1" "cf!1" "pi!1" _ "tau!1") (("2" (inst?) (("2" (prop) (("1" (rewrite "-") (("1" (move-terms 1 l (2 3)) (("1" (invoke (then (case "%1 <= %2") (assert) (hide -1 2)) (! -1 r) (! 1 r)) (("1" (expand* "*" "synch_protocol" "v_min") (("1" (inst?) (("1" (assert) (("1" (replace -2 :hide? t) (("1" (isolate 1 r 2) (("1" (expand* "clock_relation?" "nominal" "epsilon_lower") (("1" (inst?) (("1" (expand* "quorum_synch?" "check" "received") (("1" (inst?) (("1" (assert) (("1" (use "lower_synch_validity[rho, min_latency(j!1 + j!2), var_latency(j!1 + j!2), stage (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (expand "synch_protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-3 1)) (("3" (expand "quorum_synch?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (-4 1)) (("4" (expand "clock_relation?") (("4" (skosimp*) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil) ((nnreal_div_posreal_is_nnreal application-judgement "nnreal" real_types nil) (lower_synch_validity formula-decl nil reduce_synch_stage nil) (vec type-eq-decl nil node nil) (v_min const-decl "T" select_minmax nil) (synch_stage const-decl "real" reduce_synch_stage nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (sigma_last formula-decl nil sigma "reals/") (nat_induction formula-decl nil naturalnumbers nil) (Delay const-decl "nat" reduce_synch nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (epsilon_lower const-decl "nonneg_real" timing_integration nil) (- const-decl "[T -> real]" real_fun_ops "reals/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (nominal const-decl "[below(stage(i)) -> real]" timing_integration nil) (v_min const-decl "T" k_ordered nil) (sent_vec type-eq-decl nil node_functions nil) (sent_vec_stage type-eq-decl nil node_functions_stage nil) (pred type-eq-decl nil defined_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (integer nonempty-type-from-decl nil integers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (stage formal-const-decl "[nat -> posnat]" reduce_synch nil) (below type-eq-decl nil naturalnumbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (rho formal-const-decl "nonneg_real" reduce_synch nil) (rate const-decl "posreal" physical_clocks nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (ne_seqs type-eq-decl nil seqs "structures/") (below type-eq-decl nil nat_types nil) (finite_sequence type-eq-decl nil finite_sequences nil) (dom type-eq-decl nil min_seq "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (min const-decl "{t: T | (FORALL (ii: dom(s)): t <= seq(s)(ii)) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq "structures/") (dom type-eq-decl nil max_seq "structures/") (max const-decl "{t: T | (FORALL (ii: dom(s)): seq(s)(ii) <= t) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" max_seq "structures/") (consensus_function type-eq-decl nil ordered_finite_sequences nil) (k_consensus_function type-eq-decl nil k_ordered nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (fault_class type-decl nil integration_fault_model nil) (node_status type-eq-decl nil integration_fault_model nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (tau_type type-eq-decl nil tau_declaration nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (feasible? const-decl "bool" reduce_synch nil) (synch_protocol const-decl "bool" reduce_synch nil) (min_latency formal-const-decl "[nat -> nonneg_real]" reduce_synch nil) (var_latency formal-const-decl "[nat -> nonneg_real]" reduce_synch nil) (quorum_synch? const-decl "bool" timing_integration nil) (clock_relation? const-decl "bool" timing_integration nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (posreal_div_posreal_is_posreal application-judgement "posreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (upper_validity 1 (upper_validity-2 nil 3397909247 (";;; Proof lower_validity-1 for formula reduce_synch.lower_validity" (induct "k") (("1" (skosimp*) (("1" (expand "sigma") (("1" (assert) nil))))) ("2" (skosimp*) (("2" (rewrite "sigma_last") (("2" (inst?) (("2" (inst - "c_dst!1" "pi!1" _) (("2" (inst?) (("2" (prop) (("1" (rewrite "-") (("1" (move-terms 1 l (2 3)) (("1" (invoke (then (case "%1 <= %2") (assert) (hide -1 2)) (! -1 r) (! 1 r)) (("1" (expand* "*" "synch_protocol" "v_min") (("1" (inst?) (("1" (assert) (("1" (replace -2 :hide? t) (("1" (isolate 1 r 2) (("1" (expand* "clock_relation?" "nominal" "epsilon_lower") (("1" (inst?) (("1" (expand* "quorum_synch?" "check" "received") (("1" (inst?) (("1" (assert) (("1" (use "lower_synch_validity[rho, min_latency(j!1 + j!2), var_latency(j!1 + j!2), stage (("1" (assert) nil))))))))))))))))))))))))))))) ("2" (hide-all-but (-2 1)) (("2" (expand "synch_protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil))))))))) ("3" (hide-all-but (-3 1)) (("3" (expand "quorum_synch?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil))))))))) ("4" (hide-all-but (-4 1)) (("4" (expand "clock_relation?") (("4" (skosimp*) (("4" (inst?) (("4" (assert) nil))))))))))))))))))))) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil)))))) ";;; developed with shostak decision procedures") nil nil) (upper_validity-1 nil 3397908629 ("" (induct "k") (("1" (skosimp*) (("1" (expand "sigma") (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (rewrite "sigma_last") (("2" (inst - _ "c_dst!1" _ "cf!1" "j!2" "pi!1" _ _ "tau!1") (("2" (inst?) (("2" (inst?) (("2" (prop) (("1" (rewrite "+") (("1" (rewrite "*") (("1" (move-terms 1 r (2 3)) (("1" (invoke (then (case "%1 <= %2") (assert) (hide -1 2)) (! 1 l) (! -1 l)) (("1" (expand* "synch_protocol" "v_max") (("1" (inst?) (("1" (assert) (("1" (replace -2 :hide? t) (("1" (isolate 1 l 1) (("1" (expand* "clock_relation?" "nominal" "epsilon_upper") (("1" (inst?) (("1" (expand* "quorum_synch?" "check" "received") (("1" (inst?) (("1" (assert) (("1" (use "upper_synch_validity[rho, min_latency(j!1 + j!2), var_latency(j!1 + j!2), stage (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (expand "synch_protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-3 1)) (("3" (expand "quorum_synch?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (-4 1)) (("4" (expand "clock_relation?") (("4" (skosimp*) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ((IFF const-decl "[bool, bool -> bool]" booleans nil) (real_minus_real_is_real application-judgement "real" reals nil) (int_plus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (synch_stage const-decl "real" reduce_synch_stage nil) (v_max const-decl "T" select_minmax nil) (vec type-eq-decl nil node nil) (upper_synch_validity formula-decl nil reduce_synch_stage nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (sigma_last formula-decl nil sigma "reals/") (nat_induction formula-decl nil naturalnumbers nil) (Delay const-decl "nat" reduce_synch nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (epsilon_upper const-decl "nonneg_real" timing_integration nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (nominal const-decl "[below(stage(i)) -> real]" timing_integration nil) (v_max const-decl "T" k_ordered nil) (sent_vec type-eq-decl nil node_functions nil) (sent_vec_stage type-eq-decl nil node_functions_stage nil) (pred type-eq-decl nil defined_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (integer nonempty-type-from-decl nil integers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (stage formal-const-decl "[nat -> posnat]" reduce_synch nil) (below type-eq-decl nil naturalnumbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (rho formal-const-decl "nonneg_real" reduce_synch nil) (rate const-decl "posreal" physical_clocks nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (ne_seqs type-eq-decl nil seqs "structures/") (below type-eq-decl nil nat_types nil) (finite_sequence type-eq-decl nil finite_sequences nil) (dom type-eq-decl nil min_seq "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (min const-decl "{t: T | (FORALL (ii: dom(s)): t <= seq(s)(ii)) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq "structures/") (dom type-eq-decl nil max_seq "structures/") (max const-decl "{t: T | (FORALL (ii: dom(s)): seq(s)(ii) <= t) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" max_seq "structures/") (consensus_function type-eq-decl nil ordered_finite_sequences nil) (k_consensus_function type-eq-decl nil k_ordered nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (fault_class type-decl nil integration_fault_model nil) (node_status type-eq-decl nil integration_fault_model nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (tau_type type-eq-decl nil tau_declaration nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (feasible? const-decl "bool" reduce_synch nil) (synch_protocol const-decl "bool" reduce_synch nil) (min_latency formal-const-decl "[nat -> nonneg_real]" reduce_synch nil) (var_latency formal-const-decl "[nat -> nonneg_real]" reduce_synch nil) (quorum_synch? const-decl "bool" timing_integration nil) (clock_relation? const-decl "bool" timing_integration nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (agreement_propagation 0 (agreement_propagation-1 nil 3397908638 ("" (induct "k") (("1" (skosimp*) (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (rewrite "sigma_last") (("2" (inst?) (("2" (inst - "c_dst!1" "cf!1" "pi!1" _ _) (("2" (inst?) (("2" (inst?) (("2" (prop) (("1" (hide -6) (("1" (forward-chain "synch_protocol_sent") (("1" (expand* "v_max" "v_min" "quorum_synch?") (("1" (inst - "j!1+j!2") (("1" (assert) (("1" (replace -1 :hide? t) (("1" (expand* "clock_relation?" "sent" "check" "received") (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (rewrite "+") (("1" (rewrite "*") (("1" (rewrite "epsilon_total") (("1" (use "synch_agreement_propagation[rho, min_latency(j!1 + j!2), var_latency(j!1 + j!2) stage(1 + j!1 + j!2)]") (("1" (assert) nil nil) ("2" (expand "quorum_synch?") (("2" (hide-all-but 1) (("2" (use "sigma_nonneg[nat]") (("2" (assert) (("2" (skosimp*) (("2" (hide 2) (("2" (rewrite "+") (("2" (rewrite "*") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (expand "synch_protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-3 1)) (("3" (expand "quorum_synch?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (-4 1)) (("4" (expand "clock_relation?") (("4" (skosimp*) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("5" (hide-all-but (-6 1)) (("5" (expand "same_clock?") (("5" (skosimp*) (("5" (inst?) (("5" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (synch_protocol_sent formula-decl nil reduce_synch nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (synch_agreement_propagation formula-decl nil reduce_synch_stage nil) (delta!1 skolem-const-decl "nonneg_real" reduce_synch nil) (Schedule!1 skolem-const-decl "[nat -> integer]" reduce_synch nil) (j!1 skolem-const-decl "nat" reduce_synch nil) (j!2 skolem-const-decl "nat" reduce_synch nil) (nnreal_plus_posreal_is_posreal application-judgement "posreal" real_types nil) (sigma_nonneg formula-decl nil sigma "reals/") (quorum_synch? const-decl "bool" timing_integration_stage nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (sigma_last formula-decl nil sigma "reals/") (nat_induction formula-decl nil naturalnumbers nil) (Lag const-decl "nat" reduce_synch nil) (drift const-decl "nonneg_real" physical_clocks nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (epsilon_total const-decl "nonneg_real" timing_integration nil) (+ const-decl "[T -> real]" real_fun_ops "reals/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (pred type-eq-decl nil defined_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (integer nonempty-type-from-decl nil integers nil) (< const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (stage formal-const-decl "[nat -> posnat]" reduce_synch nil) (below type-eq-decl nil naturalnumbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (rho formal-const-decl "nonneg_real" reduce_synch nil) (rate const-decl "posreal" physical_clocks nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (good_clock nonempty-type-eq-decl nil physical_clocks nil) (ne_seqs type-eq-decl nil seqs "structures/") (below type-eq-decl nil nat_types nil) (finite_sequence type-eq-decl nil finite_sequences nil) (dom type-eq-decl nil min_seq "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (min const-decl "{t: T | (FORALL (ii: dom(s)): t <= seq(s)(ii)) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq "structures/") (dom type-eq-decl nil max_seq "structures/") (max const-decl "{t: T | (FORALL (ii: dom(s)): seq(s)(ii) <= t) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" max_seq "structures/") (consensus_function type-eq-decl nil ordered_finite_sequences nil) (k_consensus_function type-eq-decl nil k_ordered nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (fault_class type-decl nil integration_fault_model nil) (node_status type-eq-decl nil integration_fault_model nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (tau_type type-eq-decl nil tau_declaration nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (feasible? const-decl "bool" reduce_synch nil) (synch_protocol const-decl "bool" reduce_synch nil) (min_latency formal-const-decl "[nat -> nonneg_real]" reduce_synch nil) (var_latency formal-const-decl "[nat -> nonneg_real]" reduce_synch nil) (quorum_synch? const-decl "bool" timing_integration nil) (clock_relation? const-decl "bool" timing_integration nil) (sent_vec_stage type-eq-decl nil node_functions_stage nil) (sent_vec type-eq-decl nil node_functions nil) (v_max const-decl "T" k_ordered nil) (sent const-decl "[below(stage(i)) -> real]" timing_integration nil) (v_min const-decl "T" k_ordered nil) (same_clock? const-decl "bool" reduce_synch nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (convergence 0 (convergence-2 nil 3403887754 ("" (expand "convergent_stage?") (("" (skosimp*) (("" (lemma "agreement_propagation") (("" (inst - _ _ _ _ _ "j!1" "i!1 - j!1" _ _ _ _) (("1" (assert) (("1" (inst?) (("1" (inst - "c_dst!1" "cf!1" "pi!1" "status!1" "tau!1") (("1" (ground) (("1" (hide -10) (("1" (lemma "synch_convergence[rho, min_latency(i!1), var_latency(i!1), stage(i!1), stage(1 (("1" (expand "v_max" -2) (("1" (expand "v_min" -2) (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (invoke (inst - "Lag(Schedule!1)(i!1)" "%1" "src_set!1(i!1 + 1)") (! -2 r)) (("1" (assert) (("1" (ground) (("1" (hide -2 -9 -10) (("1" (lemma "sigma_middle") (("1" (invoke (inst - "%1" "j!1 + k!1 - 1" "i!1" "j!1") (! 1 r 1 3)) (("1" (assert) (("1" (replace -1 :hide? t) (("1" (assert) (("1" (rewrite "+") (("1" (rewrite "*") --> -------------------- --> maximum size reached --> -------------------- ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.89Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Entwicklung einer Software für die statische QuellcodeanalyseBot Zugriff |
