| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/fault_tolerance/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 135 kB |
|
SSL inexact_reduce.prfInteraktion undPortierbarkeitLisp |
|||||||||||||||
|
(inexact_reduce (lower_validity_TCC1 0 (lower_validity_TCC1-1 nil 3397984485 ("" (subtype-tcc) nil nil) ((enabled const-decl "finite_set[below(S)]" fault_assumptions_stage nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (enabled_within? const-decl "bool" fault_assumptions_stage nil) (N formal-const-decl "[nat -> posnat]" inexact_reduce nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil 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) (enabled_within? const-decl "bool" inexact_comm nil) (correct_lower_inaccuracy? const-decl "bool" inexact_comm_stage nil) (empty? const-decl "bool" sets nil) (quorum? const-decl "bool" pigeonhole nil) (quorum? const-decl "bool" fault_assumptions_stage nil) (quorum_lower? const-decl "bool" inexact_comm_stage nil) (quorum_lower? const-decl "bool" inexact_comm nil) (error formal-const-decl "[nat -> real]" inexact_reduce nil) (<= const-decl "bool" reals nil) (reduce_choice const-decl "choice_function" k_ordered nil) (protocol const-decl "bool" protocol nil)) nil)) (lower_validity_TCC2 0 (lower_validity_TCC2-1 nil 3397984485 ("" (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) (enabled const-decl "finite_set[below(S)]" fault_assumptions_stage nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (enabled_within? const-decl "bool" fault_assumptions_stage nil) (N formal-const-decl "[nat -> posnat]" inexact_reduce nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil 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) (enabled_within? const-decl "bool" inexact_comm nil) (correct_lower_inaccuracy? const-decl "bool" inexact_comm_stage nil) (empty? const-decl "bool" sets nil) (quorum? const-decl "bool" pigeonhole nil) (quorum? const-decl "bool" fault_assumptions_stage nil) (quorum_lower? const-decl "bool" inexact_comm_stage nil) (quorum_lower? const-decl "bool" inexact_comm nil) (error formal-const-decl "[nat -> real]" inexact_reduce nil) (<= const-decl "bool" reals nil) (reduce_choice const-decl "choice_function" k_ordered nil) (protocol const-decl "bool" protocol nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil)) nil)) (lower_validity 0 (lower_validity-2 nil 3398099576 ("" (induct "k") (("1" (skosimp*) (("1" (expand "sigma") (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) (("2" (inst?) (("2" (inst?) (("2" (inst - "eps_l!1" _) (("2" (inst?) (("2" (assert) (("2" (prop) (("1" (rewrite "sigma_last" +) (("1" (invoke (then (case "%1 - eps_l!1(j!1+j!2) <= %2") (assert)) (! -1 r) (! 1 r)) (("1" (hide 2 -1) (("1" (expand "enabled_within?") (("1" (expand "protocol") (("1" (expand "quorum_lower?") (("1" (inst - "j!1 + j!2") (("1" (inst - "j!1 + j!2") (("1" (inst - "j!1 + j!2") (("1" (assert) (("1" (expand "v_min") (("1" (expand "reduce_choice") (("1" (replace -1 :hide? t) (("1" (lemma "reduce_min_validity[N(j!2 + j!1), N(1 + j!1 + j!2), error(j!1 + j!2)]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -1)) (("2" (expand "protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (1 -2)) (("3" (expand "quorum_lower?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (1 -3)) (("4" (expand "enabled_within?") (("4" (skosimp*) (("4" (inst?) (("4" (assert) nil 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) ((sigma_last formula-decl nil sigma "reals/") (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (reduce_min_validity formula-decl nil inexact_reduce_stage nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (nat_induction formula-decl nil naturalnumbers nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (v_min const-decl "T" k_ordered 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) (ne_seqs type-eq-decl nil seqs "structures/") (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (finite_sequence type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (< const-decl "bool" reals 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (N formal-const-decl "[nat -> posnat]" inexact_reduce nil) (error formal-const-decl "[nat -> real]" inexact_reduce nil) (k_consensus_function type-eq-decl nil k_ordered nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (check_stage type-eq-decl nil node_functions_stage nil) (check_function type-eq-decl nil node_functions nil) (nonneg_real nonempty-type-eq-decl nil real_types 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) (rcvd_matrix_stage type-eq-decl nil node_functions_stage nil) (rcvd_matrix type-eq-decl nil node_functions nil) (sent_vec_stage type-eq-decl nil node_functions_stage nil) (sent_vec type-eq-decl nil node_functions 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) (result_vec_stage type-eq-decl nil node_functions_stage nil) (choice_stage type-eq-decl nil node_functions_stage nil) (choice_function type-eq-decl nil node_functions nil) (protocol const-decl "bool" protocol nil) (reduce_choice const-decl "choice_function" k_ordered nil) (quorum_lower? const-decl "bool" inexact_comm nil) (enabled_within? const-decl "bool" inexact_comm nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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_minus_real_is_real application-judgement "real" reals nil)) nil) (lower_validity-1 nil 3397985916 ("" (induct "k") (("1" (skosimp*) (("1" (expand "sigma") (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) (("2" (inst?) (("2" (inst?) (("2" (inst - "eps_l!1" _) (("2" (inst?) (("2" (assert) (("2" (prop) (("1" (rewrite "sigma_last" +) (("1" (invoke (then (case "%1 - eps_l!1(j!1+j!2) <= %2") (assert)) (! -1 r) (! 1 r)) (("1" (hide 2 -1) (("1" (expand "enabled_within?") (("1" (expand "protocol") (("1" (expand "generalized_majority_lower?") (("1" (inst - "j!1 + j!2") (("1" (inst - "j!1 + j!2") (("1" (inst - "j!1 + j!2") (("1" (assert) (("1" (expand "v_min") (("1" (expand "reduce_select") (("1" (replace -1 :hide? t) (("1" (lemma "reduce_min_validity[N(j!2 + j!1), N(1 + j!1 + j!2), error(j!1 + j!2)]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -1)) (("2" (expand "protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (1 -2)) (("3" (expand "generalized_majority_lower?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (1 -3)) (("4" (expand "enabled_within?") (("4" (skosimp*) (("4" (inst?) (("4" (assert) nil 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) ((sigma_last formula-decl nil sigma "reals/") (reduce_min_validity formula-decl nil inexact_reduce_stage nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (v_min const-decl "T" k_ordered nil) (check_stage type-eq-decl nil node_functions_stage nil) (check_function type-eq-decl nil node_functions nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (rcvd_matrix_stage type-eq-decl nil node_functions_stage nil) (rcvd_matrix type-eq-decl nil node_functions nil) (sent_vec_stage type-eq-decl nil node_functions_stage nil) (sent_vec type-eq-decl nil node_functions nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (result_vec_stage type-eq-decl nil node_functions_stage nil) (choice_stage type-eq-decl nil node_functions_stage nil) (choice_function type-eq-decl nil node_functions nil)) nil)) (upper_validity_TCC1 0 (upper_validity_TCC1-1 nil 3397984485 ("" (subtype-tcc) nil nil) ((enabled const-decl "finite_set[below(S)]" fault_assumptions_stage nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (enabled_within? const-decl "bool" fault_assumptions_stage nil) (N formal-const-decl "[nat -> posnat]" inexact_reduce nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil 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) (enabled_within? const-decl "bool" inexact_comm nil) (correct_upper_inaccuracy? const-decl "bool" inexact_comm_stage nil) (empty? const-decl "bool" sets nil) (quorum? const-decl "bool" pigeonhole nil) (quorum? const-decl "bool" fault_assumptions_stage nil) (quorum_upper? const-decl "bool" inexact_comm_stage nil) (quorum_upper? const-decl "bool" inexact_comm nil) (error formal-const-decl "[nat -> real]" inexact_reduce nil) (<= const-decl "bool" reals nil) (reduce_choice const-decl "choice_function" k_ordered nil) (protocol const-decl "bool" protocol nil)) nil)) (upper_validity_TCC2 0 (upper_validity_TCC2-1 nil 3397984485 ("" (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) (enabled const-decl "finite_set[below(S)]" fault_assumptions_stage nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (enabled_within? const-decl "bool" fault_assumptions_stage nil) (N formal-const-decl "[nat -> posnat]" inexact_reduce nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil 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) (enabled_within? const-decl "bool" inexact_comm nil) (correct_upper_inaccuracy? const-decl "bool" inexact_comm_stage nil) (empty? const-decl "bool" sets nil) (quorum? const-decl "bool" pigeonhole nil) (quorum? const-decl "bool" fault_assumptions_stage nil) (quorum_upper? const-decl "bool" inexact_comm_stage nil) (quorum_upper? const-decl "bool" inexact_comm nil) (error formal-const-decl "[nat -> real]" inexact_reduce nil) (<= const-decl "bool" reals nil) (reduce_choice const-decl "choice_function" k_ordered nil) (protocol const-decl "bool" protocol nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil)) nil)) (upper_validity 0 (upper_validity-3 nil 3403269169 ("" (induct "k") (("1" (skosimp*) (("1" (expand "sigma") (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) (("2" (inst?) (("2" (inst?) (("2" (inst - "eps_u!1" "rcvd!1") (("2" (assert) (("2" (prop) (("1" (rewrite "sigma_first" 1) (("1" (invoke (then (case "%1 <= %2 + eps_u!1(j!2)") (assert)) (! -1 r 1) (! 1 r 1)) (("1" (hide 2 -1) (("1" (expand "enabled_within?") (("1" (expand "quorum_upper?") (("1" (expand "protocol") (("1" (inst - "j!2") (("1" (inst - "j!2") (("1" (inst - "j!2") (("1" (assert) (("1" (expand "v_max") (("1" (expand "reduce_choice") (("1" (replace -1 :hide? t) (("1" (lemma "reduce_max_validity[N(j!2), N(1 + j!2), error(j!2)]") (("1" (inst?) (("1" (inst?) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -1)) (("2" (expand "protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (1 -2)) (("3" (expand "quorum_upper?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (1 -3)) (("4" (expand "enabled_within?") (("4" (skosimp*) (("4" (inst?) (("4" (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) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (reduce_max_validity formula-decl nil inexact_reduce_stage nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sigma_first formula-decl nil sigma "reals/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (nat_induction formula-decl nil naturalnumbers nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (v_max const-decl "T" k_ordered 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) (ne_seqs type-eq-decl nil seqs "structures/") (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (finite_sequence type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (< const-decl "bool" reals 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (N formal-const-decl "[nat -> posnat]" inexact_reduce nil) (error formal-const-decl "[nat -> real]" inexact_reduce nil) (k_consensus_function type-eq-decl nil k_ordered nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (check_stage type-eq-decl nil node_functions_stage nil) (check_function type-eq-decl nil node_functions nil) (nonneg_real nonempty-type-eq-decl nil real_types 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) (rcvd_matrix_stage type-eq-decl nil node_functions_stage nil) (rcvd_matrix type-eq-decl nil node_functions nil) (sent_vec_stage type-eq-decl nil node_functions_stage nil) (sent_vec type-eq-decl nil node_functions 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) (result_vec_stage type-eq-decl nil node_functions_stage nil) (choice_stage type-eq-decl nil node_functions_stage nil) (choice_function type-eq-decl nil node_functions nil) (protocol const-decl "bool" protocol nil) (reduce_choice const-decl "choice_function" k_ordered nil) (quorum_upper? const-decl "bool" inexact_comm nil) (enabled_within? const-decl "bool" inexact_comm nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (upper_validity-2 nil 3398099607 ("" (induct "k") (("1" (skosimp*) (("1" (expand "sigma") (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) (("2" (inst?) (("2" (inst?) (("2" (inst - "eps_u!1" "rcvd!1") (("2" (assert) (("2" (prop) (("1" (rewrite "sigma_first" 1) (("1" (invoke (then (case "%1 <= %2 + eps_u!1(j!2)") (assert)) (! -1 r 1) (! 1 r 1)) (("1" (hide 2 -1) (("1" (expand "enabled_within?") (("1" (expand "quorum_upper?") (("1" (expand "protocol") (("1" (inst - "j!2") (("1" (inst - "j!2") (("1" (inst - "j!2") (("1" (assert) (("1" (expand "v_max") (("1" (expand "reduce_select") (("1" (replace -1 :hide? t) (("1" (lemma "reduce_max_validity[N(j!2), N(1 + j!2), error(j!2)]") (("1" (inst?) (("1" (inst?) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -1)) (("2" (expand "protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (1 -2)) (("3" (expand "quorum_upper?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (1 -3)) (("4" (expand "enabled_within?") (("4" (skosimp*) (("4" (inst?) (("4" (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) ((enabled_within? const-decl "bool" inexact_comm nil) (quorum_upper? const-decl "bool" inexact_comm nil) (choice_function type-eq-decl nil node_functions nil) (choice_stage type-eq-decl nil node_functions_stage nil) (result_vec_stage type-eq-decl nil node_functions_stage nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (sent_vec type-eq-decl nil node_functions nil) (sent_vec_stage type-eq-decl nil node_functions_stage nil) (rcvd_matrix type-eq-decl nil node_functions nil) (rcvd_matrix_stage type-eq-decl nil node_functions_stage nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (check_function type-eq-decl nil node_functions nil) (check_stage type-eq-decl nil node_functions_stage nil) (v_max const-decl "T" k_ordered nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (sigma_first formula-decl nil sigma "reals/") (reduce_max_validity formula-decl nil inexact_reduce_stage nil)) nil) (upper_validity-1 nil 3397985929 ("" (induct "k") (("1" (skosimp*) (("1" (expand "sigma") (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) (("2" (inst?) (("2" (inst?) (("2" (inst - "eps_u!1" "rcvd!1") (("2" (assert) (("2" (prop) (("1" (rewrite "sigma_first" 1) (("1" (invoke (then (case "%1 <= %2 + eps_u!1(j!2)") (assert)) (! -1 r 1) (! 1 r 1)) (("1" (hide 2 -1) (("1" (expand "enabled_within?") (("1" (expand "generalized_majority_upper?") (("1" (expand "protocol") (("1" (inst - "j!2") (("1" (inst - "j!2") (("1" (inst - "j!2") (("1" (assert) (("1" (expand "v_max") (("1" (expand "reduce_select") (("1" (replace -1 :hide? t) (("1" (lemma "reduce_max_validity[N(j!2), N(1 + j!2), error(j!2)]") (("1" (inst?) (("1" (inst?) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -1)) (("2" (expand "protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (1 -2)) (("3" (expand "generalized_majority_upper?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (1 -3)) (("4" (expand "enabled_within?") (("4" (skosimp*) (("4" (inst?) (("4" (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) ((reduce_max_validity formula-decl nil inexact_reduce_stage nil) (sigma_first formula-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (v_max const-decl "T" k_ordered nil) (check_stage type-eq-decl nil node_functions_stage nil) (check_function type-eq-decl nil node_functions nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (rcvd_matrix_stage type-eq-decl nil node_functions_stage nil) (rcvd_matrix type-eq-decl nil node_functions nil) (sent_vec_stage type-eq-decl nil node_functions_stage nil) (sent_vec type-eq-decl nil node_functions nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (result_vec_stage type-eq-decl nil node_functions_stage nil) (choice_stage type-eq-decl nil node_functions_stage nil) (choice_function type-eq-decl nil node_functions nil)) nil)) (agreement_propagation_TCC1 0 (agreement_propagation_TCC1-1 nil 3397984485 ("" (subtype-tcc) nil nil) ((v_max const-decl "T" select_minmax nil) (error formal-const-decl "[nat -> real]" inexact_reduce nil) (<= const-decl "bool" reals nil) (N formal-const-decl "[nat -> posnat]" inexact_reduce nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil 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) (v_max const-decl "T" k_ordered nil) (v_min const-decl "T" select_minmax nil) (v_min const-decl "T" k_ordered nil) (enabled const-decl "finite_set[below(S)]" fault_assumptions_stage nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (enabled_within? const-decl "bool" fault_assumptions_stage nil) (enabled_within? const-decl "bool" inexact_comm nil) (correct_imprecision? const-decl "bool" inexact_comm_stage nil) (empty? const-decl "bool" sets nil) (quorum? const-decl "bool" pigeonhole nil) (quorum? const-decl "bool" fault_assumptions_stage nil) (quorum_imprecision? const-decl "bool" inexact_comm_stage nil) (quorum_imprecision? const-decl "bool" inexact_comm nil) (reduce_choice const-decl "choice_function" k_ordered nil) (protocol const-decl "bool" protocol nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) nil)) (agreement_propagation_TCC2 0 (agreement_propagation_TCC2-1 nil 3397984485 ("" (subtype-tcc) nil nil) ((nonneg_real nonempty-type-eq-decl nil real_types nil) (NOT const-decl "[bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (finite_image application-judgement "finite_set[R]" function_image_aux nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (v_max const-decl "T" select_minmax nil) (error formal-const-decl "[nat -> real]" inexact_reduce nil) (<= const-decl "bool" reals nil) (N formal-const-decl "[nat -> posnat]" inexact_reduce nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil 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) (v_max const-decl "T" k_ordered nil) (v_min const-decl "T" select_minmax nil) (v_min const-decl "T" k_ordered nil) (enabled const-decl "finite_set[below(S)]" fault_assumptions_stage nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (enabled_within? const-decl "bool" fault_assumptions_stage nil) (enabled_within? const-decl "bool" inexact_comm nil) (correct_imprecision? const-decl "bool" inexact_comm_stage nil) (empty? const-decl "bool" sets nil) (quorum? const-decl "bool" pigeonhole nil) (quorum? const-decl "bool" fault_assumptions_stage nil) (quorum_imprecision? const-decl "bool" inexact_comm_stage nil) (quorum_imprecision? const-decl "bool" inexact_comm nil) (reduce_choice const-decl "choice_function" k_ordered nil) (protocol const-decl "bool" protocol nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil)) nil)) (agreement_propagation 0 (agreement_propagation-4 nil 3403269194 ("" (induct "k") (("1" (skosimp*) (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) (("2" (inst?) (("2" (inst?) (("2" (inst - "epsilon!1" "rcvd!1") (("2" (assert) (("2" (prop) (("1" (hide -5) (("1" (expand "protocol") (("1" (expand "enabled_within?") (("1" (expand "quorum_imprecision?") (("1" (inst - "j!1 + j!2") (("1" (inst - "j!1 + j!2") (("1" (inst - "j!1 + j!2") (("1" (assert) (("1" (expand "v_min") (("1" (expand "v_max") (("1" (expand "reduce_choice") (("1" (replace -2 :hide? t) (("1" (lemma "agreement_propagation[N(j!1 + j!2), N(1 + j!1 + j!2), error(j!1 + j!2)]") (("1" (inst - _ _ _ "delta!1+sigma(j!2,j!1+j!2-1,epsilon!1)" _ "epsilon!1(j!1+j!2)" _ _ _ _) (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (rewrite "sigma_last" 1) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (assert) (("2" (use "sigma_nonneg[nat]") (("1" (skosimp*) (("1" (assert) nil nil)) nil) ("2" (ground) nil nil) ("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -1)) (("2" (expand "protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (1 -2)) (("3" (expand "quorum_imprecision?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (1 -3)) (("4" (expand "enabled_within?") (("4" (skosimp*) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_plus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (j!1 skolem-const-decl "nat" inexact_reduce nil) (j!2 skolem-const-decl "nat" inexact_reduce nil) (sigma_last formula-decl nil sigma "reals/") (sigma_nonneg formula-decl nil sigma "reals/") (agreement_propagation formula-decl nil inexact_reduce_stage nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nat_induction formula-decl nil naturalnumbers nil) (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) (ne_seqs type-eq-decl nil seqs "structures/") (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (finite_sequence type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (< const-decl "bool" reals 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (N formal-const-decl "[nat -> posnat]" inexact_reduce nil) (error formal-const-decl "[nat -> real]" inexact_reduce nil) (k_consensus_function type-eq-decl nil k_ordered nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (below type-eq-decl nil naturalnumbers nil) (check_stage type-eq-decl nil node_functions_stage nil) (check_function type-eq-decl nil node_functions nil) (nonneg_real nonempty-type-eq-decl nil real_types 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) (rcvd_matrix_stage type-eq-decl nil node_functions_stage nil) (rcvd_matrix type-eq-decl nil node_functions nil) (sent_vec_stage type-eq-decl nil node_functions_stage nil) (sent_vec type-eq-decl nil node_functions 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) (result_vec_stage type-eq-decl nil node_functions_stage nil) (choice_stage type-eq-decl nil node_functions_stage nil) (choice_function type-eq-decl nil node_functions nil) (protocol const-decl "bool" protocol nil) (reduce_choice const-decl "choice_function" k_ordered nil) (quorum_imprecision? const-decl "bool" inexact_comm nil) (enabled_within? const-decl "bool" inexact_comm nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (v_max const-decl "T" k_ordered nil) (v_min const-decl "T" k_ordered 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) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil)) nil) (agreement_propagation-3 nil 3398099716 ("" (induct "k") (("1" (skosimp*) (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) (("2" (inst?) (("2" (inst?) (("2" (inst - "epsilon!1" "rcvd!1") (("2" (assert) (("2" (prop) (("1" (hide -5) (("1" (expand "protocol") (("1" (expand "enabled_within?") (("1" (expand "quorum_imprecision?") (("1" (inst - "j!1 + j!2") (("1" (inst - "j!1 + j!2") (("1" (inst - "j!1 + j!2") (("1" (assert) (("1" (expand "v_min") (("1" (expand "v_max") (("1" (expand "reduce_select") (("1" (replace -2 :hide? t) (("1" (lemma "agreement_propagation[N(j!1 + j!2), N(1 + j!1 + j!2), error(j!1 + j!2)]") (("1" (inst - _ "delta!1+sigma(j!2,j!1+j!2-1,epsilon!1)" _ "epsilon!1(j!1+j!2)" _ _ _ _ _ _) (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (rewrite "sigma_last" 1) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -1)) (("2" (expand "protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (1 -2)) (("3" (expand "quorum_imprecision?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (1 -3)) (("4" (expand "enabled_within?") (("4" (skosimp*) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ((v_min const-decl "T" k_ordered nil) (v_max const-decl "T" k_ordered nil) (enabled_within? const-decl "bool" inexact_comm nil) (quorum_imprecision? const-decl "bool" inexact_comm nil) (choice_function type-eq-decl nil node_functions nil) (choice_stage type-eq-decl nil node_functions_stage nil) (result_vec_stage type-eq-decl nil node_functions_stage nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (sent_vec type-eq-decl nil node_functions nil) (sent_vec_stage type-eq-decl nil node_functions_stage nil) (rcvd_matrix type-eq-decl nil node_functions nil) (rcvd_matrix_stage type-eq-decl nil node_functions_stage nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (check_function type-eq-decl nil node_functions nil) (check_stage type-eq-decl nil node_functions_stage nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (agreement_propagation formula-decl nil inexact_reduce_stage nil) (sigma_last formula-decl nil sigma "reals/")) nil) (agreement_propagation-2 nil 3397996105 ("" (induct "k") (("1" (skosimp*) (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) (("2" (inst?) (("2" (inst?) (("2" (inst - "epsilon!1" "rcvd!1") (("2" (assert) (("2" (prop) (("1" (hide -5) (("1" (expand "protocol") (("1" (expand "enabled_within?") (("1" (expand "generalized_majority_imprecision?") (("1" (inst - "j!1 + j!2") (("1" (inst - "j!1 + j!2") (("1" (inst - "j!1 + j!2") (("1" (assert) (("1" (expand "v_min") (("1" (expand "v_max") (("1" (expand "reduce_select") (("1" (replace -2 :hide? t) (("1" (lemma "agreement_propagation[N(j!1 + j!2), N(1 + j!1 + j!2), error(j!1 + j!2)]") (("1" (inst - _ "delta!1+sigma(j!2,j!1+j!2-1,epsilon!1)" _ "epsilon!1(j!1+j!2)" _ _ _ _ _ _) (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (rewrite "sigma_last" 1) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -1)) (("2" (expand "protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (1 -2)) (("3" (expand "generalized_majority_imprecision?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (1 -3)) (("4" (expand "enabled_within?") (("4" (skosimp*) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) ((sigma_last formula-decl nil sigma "reals/") (agreement_propagation formula-decl nil inexact_reduce_stage nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (check_stage type-eq-decl nil node_functions_stage nil) (check_function type-eq-decl nil node_functions nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (rcvd_matrix_stage type-eq-decl nil node_functions_stage nil) (rcvd_matrix type-eq-decl nil node_functions nil) (sent_vec_stage type-eq-decl nil node_functions_stage nil) (sent_vec type-eq-decl nil node_functions nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (result_vec_stage type-eq-decl nil node_functions_stage nil) (choice_stage type-eq-decl nil node_functions_stage nil) (choice_function type-eq-decl nil node_functions nil) (v_max const-decl "T" k_ordered nil) (v_min const-decl "T" k_ordered nil)) nil) (agreement_propagation-1 nil 3397985938 ("" (induct "k") (("1" (skosimp*) (("1" (expand "sigma") (("1" (propax) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) (("2" (inst?) (("2" (inst?) (("2" (inst?) (("2" (assert) (("2" (hide -5) (("2" (expand "protocol") (("2" (expand "enabled_within?") (("2" (assert) (("2" (expand "v_min") (("2" (expand "v_max") (("2" (replace -2 :hide? t) (("2" (inst?) (("2" (assert) (("2" (inst?) (("2" (assert) (("2" (rewrite "sigma_last" 1) (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil) nil nil)) (convergence 0 (convergence-2 "" 3495473970 ("" (expand "convergent_stage?") (("" (skosimp*) (("" (lemma "agreement_propagation") (("" (inst - _ _ _ _ "j!1" "i!1 - j!1" _ _ _ _) (("1" (assert) (("1" (inst?) (("1" (inst?) (("1" (inst?) (("1" (inst?) (("1" (inst?) (("1" (ground) (("1" (hide -9) (("1" (expand "v_max" -) (("1" (expand "v_min" -) (("1" (lemma "convergence[N(i!1), N(i!1 + 1), error(i!1)]") (("1" (inst?) (("1" (invoke (inst - "%1" _ _ _ _) (! -2 r)) (("1" (inst?) (("1" (inst?) (("1" (inst - "node_set!1(i!1 + 1)") (("1" (ground) (("1" (hide -2 -8 -9) (("1" (lemma "agreement_propagation") (("1" (inst - _ _ _ _ "i!1 + 1" "j!1 + k!1 - (i!1 + 1)" _ _ _ _) (("1" (assert) (("1" (inst?) (("1" (inst?) (("1" (inst?) (("1" (invoke (inst - "%1" "epsilon!1" "rcvd!1") (! -2 r)) (("1" (ground) (("1" (hide -2) (("1" (lemma "sigma_middle") (("1" (inst - "epsilon!1" "j!1 - 1 + k!1" "i!1" "j!1") (("1" (assert) (("1" (replace -1 :hide? t) (("1" (invoke (then (case "%1 <= %2") (assert)) (! -1 r 3) (! 1 r 3)) (("1" (hide-all-but 1) (("1" (case "(X!1 - 1)/X!1 <= 1") (("1" (invoke (mult-by -1 "%1") (! 1 r)) (("1" (assert) nil nil)) nil) ("2" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (expand "protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-3 1)) (("3" (expand "quorum_imprecision?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (-4 1)) (("4" (expand "enabled_within?") (("4" (skosimp*) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (expand "v_max" +) (("5" (expand "v_min" +) (("5" (assert) (("5" (expand "protocol") (("5" (inst?) (("5" (expand "reduce_choice" -2) (("5" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (case "(X!1 - 1) / X!1 >= 0") (("1" (case "sigma[nat](j!1, i!1 - 1, epsilon!1) >= 0") (("1" (mult-by -1 "(X!1-1)/X!1") (("1" (assert) (("1" (mult-by -2 "delta!1") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (hide 2) (("2" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (expand "quorum_imprecision?" -) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (hide-all-but (-4 1)) (("3" (expand "enabled_within?" -) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-2 1)) (("3" (expand "quorum_imprecision?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (-3 1)) (("4" (expand "enabled_within?") (("4" (skosimp*) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (j!1 skolem-const-decl "nat" inexact_reduce nil) (i!1 skolem-const-decl "nat" inexact_reduce 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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (nonneg_real nonempty-type-eq-decl nil real_types 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) (N formal-const-decl "[nat -> posnat]" inexact_reduce nil) (below type-eq-decl nil naturalnumbers 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) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (sent_vec_stage type-eq-decl nil node_functions_stage nil) (sent_vec type-eq-decl nil node_functions nil) (int_plus_int_is_int application-judgement "int" integers nil) (check_function type-eq-decl nil node_functions nil) (check_stage type-eq-decl nil node_functions_stage nil) (rcvd_matrix type-eq-decl nil node_functions nil) (rcvd_matrix_stage type-eq-decl nil node_functions_stage nil) (v_min const-decl "T" k_ordered nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (sigma_middle formula-decl nil sigma "reals/") (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (div_mult_pos_le1 formula-decl nil real_props nil) (protocol const-decl "bool" protocol nil) (quorum_imprecision? const-decl "bool" inexact_comm nil) (enabled_within? const-decl "bool" inexact_comm nil) (reduce_choice const-decl "choice_function" k_ordered nil) (epsilon!1 skolem-const-decl "[nat -> nonneg_real]" inexact_reduce nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (X!1 skolem-const-decl "posnat" inexact_reduce nil) (delta!1 skolem-const-decl "nonneg_real" inexact_reduce nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (convergence formula-decl nil inexact_reduce_stage nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (v_max const-decl "T" k_ordered nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (ne_seqs type-eq-decl nil seqs "structures/") (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (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) (error formal-const-decl "[nat -> real]" inexact_reduce nil) (k_consensus_function type-eq-decl nil k_ordered nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (tau_type type-eq-decl nil tau_declaration nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (agreement_propagation formula-decl nil inexact_reduce nil) (convergent_stage? const-decl "bool" inexact_reduce nil) (real_times_real_is_real application-judgement "real" reals nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil)) shostak) (convergence-1 nil 3403709025 ("" (expand "convergent_stage?") (("" (skosimp*) (("" (lemma "agreement_propagation") (("" (inst - _ _ _ _ "j!1" "i!1 - j!1" _ _ _ _) (("1" (assert) (("1" (inst?) (("1" (inst?) (("1" (inst?) (("1" (inst?) (("1" (inst?) (("1" (ground) (("1" (hide -9) (("1" (expand "v_max" -) (("1" (expand "v_min" -) (("1" (lemma "convergence[N(i!1), N(i!1 + 1), error(i!1)]") (("1" (inst?) (("1" (invoke (inst - "%1" _ _ _ _) (! -2 r)) (("1" (inst?) (("1" (inst?) (("1" (inst - "node_set!1(i!1 + 1)") (("1" (ground) (("1" (hide -2 -8 -9) (("1" (lemma "agreement_propagation") (("1" (inst - _ _ _ _ "i!1 + 1" "j!1 + k!1 - (i!1 + 1)" _ _ _ _) (("1" (assert) (("1" (inst?) (("1" (inst?) (("1" (inst?) (("1" (invoke (inst - "%1" "epsilon!1" "rcvd!1") (! -2 r)) (("1" (ground) (("1" (hide -2) (("1" (lemma "sigma_middle") (("1" (inst - "epsilon!1" "j!1 - 1 + k!1" "i!1" "j!1") (("1" (assert) (("1" (replace -1 :hide? t) (("1" (case "(X!1 -1) / X!1 < 1") (("1" (invoke (mult-by -1 "%1") (! 1 r 3)) (("1" (assert) nil nil)) nil) ("2" (cross-mult) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (expand "protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-3 1)) (("3" (expand "quorum_imprecision?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (-4 1)) (("4" (expand "enabled_within?") (("4" (skosimp*) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil) ("5" (hide 2) (("5" (expand "v_max" +) (("5" (expand "v_min" +) (("5" (assert) (("5" (expand "protocol") (("5" (inst?) (("5" (expand "reduce_choice" -2) (("5" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (case "(X!1 - 1) / X!1 > 0") (("1" (mult-by - "delta!1 + sigma[nat](j!1, i!1 - 1, epsilon!1)") (("1" (assert) nil nil)) nil) ("2" (cross-mult) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (expand "quorum_imprecision?" -) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (hide-all-but (-4 1)) (("3" (expand "enabled_within?" -) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-2 1)) (("3" (expand "quorum_imprecision?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (-3 1)) (("4" (expand "enabled_within?") (("4" (skosimp*) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (sent_vec_stage type-eq-decl nil node_functions_stage nil) (sent_vec type-eq-decl nil node_functions nil) (check_function type-eq-decl nil node_functions nil) (check_stage type-eq-decl nil node_functions_stage nil) (rcvd_matrix type-eq-decl nil node_functions nil) (rcvd_matrix_stage type-eq-decl nil node_functions_stage nil) (v_min const-decl "T" k_ordered nil) (sigma_middle formula-decl nil sigma "reals/") (quorum_imprecision? const-decl "bool" inexact_comm nil) (enabled_within? const-decl "bool" inexact_comm nil) (reduce_choice const-decl "choice_function" k_ordered nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (convergence formula-decl nil inexact_reduce_stage nil) (v_max const-decl "T" k_ordered nil) (consensus_function type-eq-decl nil ordered_finite_sequences nil) (k_consensus_function type-eq-decl nil k_ordered nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)) shostak)) (agreement_generation_TCC1 0 (agreement_generation_TCC1-1 nil 3397984485 ("" (subtype-tcc) nil nil) ((enabled const-decl "finite_set[below(S)]" fault_assumptions_stage nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (enabled_within? const-decl "bool" fault_assumptions_stage nil) (N formal-const-decl "[nat -> posnat]" inexact_reduce nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil 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) (enabled_within? const-decl "bool" inexact_comm nil) (similar? const-decl "bool" real_finite_sequences nil) (inexact_consensus? const-decl "bool" real_finite_sequences nil) (single_imprecision? const-decl "bool" inexact_comm_stage nil) (uniformly_enabled? const-decl "bool" fault_assumptions_stage nil) (all_symmetric? const-decl "bool" inexact_comm_stage nil) (correct_imprecision? const-decl "bool" inexact_comm_stage nil) (empty? const-decl "bool" sets nil) (quorum? const-decl "bool" pigeonhole nil) (quorum? const-decl "bool" fault_assumptions_stage nil) (quorum_imprecision? const-decl "bool" inexact_comm_stage nil) (quorum_imprecision? const-decl "bool" inexact_comm nil) (exists_all_symmetric? const-decl "bool" inexact_comm nil) (error formal-const-decl "[nat -> real]" inexact_reduce nil) (<= const-decl "bool" reals nil) (reduce_choice const-decl "choice_function" k_ordered nil) (protocol const-decl "bool" protocol nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (agreement_generation_TCC2 0 (agreement_generation_TCC2-1 nil 3397984485 ("" (subtype-tcc) nil 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) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (injective? const-decl "bool" functions nil) (int_minus_int_is_int application-judgement "int" 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (enabled const-decl "finite_set[below(S)]" fault_assumptions_stage nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (enabled_within? const-decl "bool" fault_assumptions_stage nil) (N formal-const-decl "[nat -> posnat]" inexact_reduce nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil 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) (enabled_within? const-decl "bool" inexact_comm nil) (similar? const-decl "bool" real_finite_sequences nil) (inexact_consensus? const-decl "bool" real_finite_sequences nil) (single_imprecision? const-decl "bool" inexact_comm_stage nil) (uniformly_enabled? const-decl "bool" fault_assumptions_stage nil) (all_symmetric? const-decl "bool" inexact_comm_stage nil) (correct_imprecision? const-decl "bool" inexact_comm_stage nil) (empty? const-decl "bool" sets nil) (quorum? const-decl "bool" pigeonhole nil) (quorum? const-decl "bool" fault_assumptions_stage nil) (quorum_imprecision? const-decl "bool" inexact_comm_stage nil) (quorum_imprecision? const-decl "bool" inexact_comm nil) (exists_all_symmetric? const-decl "bool" inexact_comm nil) (error formal-const-decl "[nat -> real]" inexact_reduce nil) (<= const-decl "bool" reals nil) (reduce_choice const-decl "choice_function" k_ordered nil) (protocol const-decl "bool" protocol nil) (real_minus_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)) (agreement_generation 0 (agreement_generation-1 nil 3397985945 ("" (expand "exists_all_symmetric?") (("" (skosimp*) (("" (lemma "agreement_propagation") (("" (inst - _ _ "sigma(j!1,i!1,epsilon!1)" "epsilon!1" "1 + i!1" "j!1 + k!1 - i!1 - 1" _ _ _ _) (("1" (inst?) (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (prop) (("1" (hide-all-but (1 -1)) (("1" (lemma "sigma_split") (("1" (inst - _ "j!1+k!1-1" "j!1" "i!1") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (1 -1)) (("2" (expand "protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (1 -7)) (("3" (expand "enabled_within?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (expand "protocol") (("4" (inst - "i!1") (("4" (assert) (("4" (expand "v_max") (("4" (expand "v_min") (("4" (expand "reduce_choice") (("4" (replace -1 :hide? t) (("4" (rewrite "sigma_last") (("4" (lemma "agreement_generation[N(i!1), N(1 + i!1), error(i!1)]") (("4" (inst - _ _ _ "epsilon!1(i!1)" _ _) (("4" (inst?) (("4" (assert) (("4" (use "sigma_nonneg") (("4" (assert) (("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (use "sigma_nonneg") (("3" (assert) (("3" (skosimp*) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_plus_int_is_int application-judgement "int" 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) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/") (k!1 skolem-const-decl "nat" inexact_reduce nil) (j!1 skolem-const-decl "nat" inexact_reduce nil) (i!1 skolem-const-decl "nat" inexact_reduce 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) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (T_low type-eq-decl nil sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (sigma def-decl "real" sigma "reals/") (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) (real_minus_real_is_real application-judgement "real" reals 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) (v_min const-decl "T" k_ordered nil) (agreement_generation formula-decl nil inexact_reduce_stage nil) (sigma_last formula-decl nil sigma "reals/") (reduce_choice const-decl "choice_function" k_ordered nil) (v_max const-decl "T" k_ordered nil) (enabled_within? const-decl "bool" inexact_comm nil) (protocol const-decl "bool" protocol nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (sigma_split formula-decl nil sigma "reals/") (ne_seqs type-eq-decl nil seqs "structures/") (AND const-decl "[bool, bool -> bool]" booleans nil) (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) (error formal-const-decl "[nat -> real]" inexact_reduce nil) (k_consensus_function type-eq-decl nil k_ordered 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) (N formal-const-decl "[nat -> posnat]" inexact_reduce nil) (below type-eq-decl nil naturalnumbers nil) (check_stage type-eq-decl nil node_functions_stage nil) (check_function type-eq-decl nil node_functions nil) (rcvd_matrix_stage type-eq-decl nil node_functions_stage nil) (rcvd_matrix type-eq-decl nil node_functions nil) (sent_vec_stage type-eq-decl nil node_functions_stage nil) (sent_vec type-eq-decl nil node_functions nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (tau_type type-eq-decl nil tau_declaration nil) (agreement_propagation formula-decl nil inexact_reduce nil) (exists_all_symmetric? const-decl "bool" inexact_comm nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil)) nil)))
¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.77Bemerkung: (vorverarbeitet am 2026-05-06) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26