%% PVS Version 3.1 %% 6.2 [Linux (x86)] (Feb 14, 2003 18:46) $$$FTRTFT_top.pvs FTRTFT_top[N: [nat -> posnat]]: THEORY BEGIN IMPORTING unified_order[real, <=], k_exact[N, unified_msg[real], unified_order.<=, source_error], k_inexact END FTRTFT_top $$$delta_bound.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % File Name : delta_bound.pvs % % Purpose : % % Assumptions : % % Guarantees : % % Design : SPIDER Version 0 % % Dependencies : % % Comments : Rougly the analog for good_vote_for % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% delta_bound [ S: posnat % Number of sources ]: THEORY BEGIN s, s1, s2: VAR below(S) good: VAR finite_set[below(S)] delta: VAR nonneg_real ideal: VAR [below(S) -> real] % The separation of values from good sources may be bounded. This is % captured in bounded_skew. bounded_delta?(good, ideal, delta): bool = FORALL s1, s2: good(s1) AND good(s2) IMPLIES abs(ideal(s1) - ideal(s2)) <= delta END delta_bound $$$inexact_sampling.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % File Name : inexact_sampling.pvs % % Purpose : % % Assumptions : % % Guarantees : % % Design : SPIDER Version 0 % % Dependencies : % % Comments : % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% inexact_sampling [ S : posnat, % Number of sources D : posnat % Number of receivers, ] : THEORY BEGIN IMPORTING delta_bound, exact_sampling[S, D, real] epsilon, eps_u, eps_l, skew: VAR nonneg_real v: VAR real s, s1, s2: VAR below(S) d, d1, d2: VAR below(D) good, benign, nonasym: VAR finite_set[below(S)] select: VAR [below(D) -> finite_set[below(S)]] good_select: VAR [below(D) -> finite_set[below(S)]] good_select_nonempty: VAR [below(D) -> non_empty_finite_set[below(S)]] eligible: var finite_set[below(S)] sent: VAR [below(S) -> real] rcvd: VAR [below(D) -> [below(S) -> real]] sampling_lower_bound?(good_select, sent, rcvd, eps_l): bool = FORALL d: FORALL s: good_select(d)(s) => sent(s) - eps_l <= rcvd(d)(s) sampling_upper_bound?(good_select, sent, rcvd, eps_u): bool = FORALL d: FORALL s: good_select(d)(s) => rcvd(d)(s) <= sent(s) + eps_u sampling_bound?(good_select, sent, rcvd, eps_l, eps_u): bool = sampling_upper_bound?(good_select, sent, rcvd, eps_l) AND sampling_lower_bound?(good_select, sent, rcvd, eps_u) inexact_agreement?(good_select, rcvd, skew): bool = FORALL d1, d2, s1, s2: good_select(d1)(s1) AND good_select(d2)(s2) IMPLIES abs(rcvd(d1)(s1) - rcvd(d2)(s2)) <= skew relative_sampling_bound?(good_select, sent, rcvd, epsilon): bool = FORALL d1, d2, s1, s2: good_select(d1)(s1) AND good_select(d2)(s2) IMPLIES abs((rcvd(d1)(s1) - rcvd(d2)(s2)) - (sent(s1) - sent(s2))) <= epsilon inexact_sampling: LEMMA sampling_upper_bound?(good_select, sent, rcvd, eps_l) AND sampling_lower_bound?(good_select, sent, rcvd, eps_u) IMPLIES relative_sampling_bound?(good_select, sent, rcvd, eps_l + eps_u) inexact_symmetry?(eligible, rcvd, epsilon): bool = FORALL d1, d2, s: eligible(s) IMPLIES abs(rcvd(d1)(s) - rcvd(d2)(s)) <= epsilon sampling_correspondence: LEMMA sampling_exact?(good_select, sent, rcvd) = sampling_bound?(good_select, sent, rcvd, 0, 0) agreement_correspondence: LEMMA exact_agreement?(good_select_nonempty, rcvd) = inexact_agreement?(good_select_nonempty, rcvd, 0) symmetry_correspondence: LEMMA exact_symmetry?(eligible, rcvd) = inexact_symmetry?(eligible, rcvd, 0) END inexact_sampling $$$inexact_sampling.prf (inexact_sampling (inexact_sampling 0 (inexact_sampling-1 nil 3292276217 3292276363 ("" (skosimp*) (("" (expand "relative_sampling_bound?") (("" (expand "sampling_lower_bound?") (("" (expand "sampling_upper_bound?") (("" (skosimp*) (("" (inst-cp - "d2!1") (("" (inst - "d1!1") (("" (inst - "s1!1") (("" (inst - "s2!1") (("" (inst-cp - "d2!1") (("" (inst - "d1!1") (("" (inst - "s1!1") (("" (inst - "s2!1") (("" (assert) (("" (assert) (("" (expand "abs") (("" (lift-if) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((relative_sampling_bound? const-decl "bool" inexact_sampling nil) (sampling_upper_bound? const-decl "bool" inexact_sampling 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) (D formal-const-decl "posnat" inexact_sampling nil) (below type-eq-decl nil naturalnumbers nil) (S formal-const-decl "posnat" inexact_sampling nil) (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil) (sampling_lower_bound? const-decl "bool" inexact_sampling nil)) 145811 5300 t shostak)) (sampling_correspondence 0 (sampling_correspondence-1 nil 3276532698 3276532700 ("" (skosimp*) (("" (expand "sampling_bound?") (("" (expand "sampling_exact?") (("" (expand "sampling_upper_bound?") (("" (expand "sampling_lower_bound?") (("" (iff) (("" (split) (("1" (flatten) (("1" (split) (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (skosimp*) (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((sampling_exact? const-decl "bool" exact_sampling nil) (sampling_lower_bound? const-decl "bool" inexact_sampling 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) (D formal-const-decl "posnat" inexact_sampling nil) (below type-eq-decl nil naturalnumbers nil) (S formal-const-decl "posnat" inexact_sampling nil) (sampling_upper_bound? const-decl "bool" inexact_sampling nil) (sampling_bound? const-decl "bool" inexact_sampling nil)) 2124 310 t nil)) (agreement_correspondence 0 (agreement_correspondence-1 nil 3276532709 3276532712 ("" (skosimp*) (("" (expand "inexact_agreement?") (("" (expand "exact_agreement?") (("" (expand "good_vote_for?") (("" (iff) (("" (split) (("1" (flatten) (("1" (skosimp*) (("1" (inst?) (("1" (inst - "d2!1") (("1" (flatten) (("1" (inst?) (("1" (inst - "s2!1") (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (typepred "good_select_nonempty!1(0)") (("1" (hide -1) (("1" (expand "empty?") (("1" (skosimp*) (("1" (expand "member") (("1" (inst + "rcvd!1(0)(x!1)") (("1" (skosimp*) (("1" (split) (("1" (skosimp*) (("1" (inst?) (("1" (inst - "0" "x!1") (("1" (assert) (("1" (expand "abs") (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) (("2" (inst - "0" "x!1") (("2" (assert) (("2" (expand "abs") (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((exact_agreement? const-decl "bool" exact_sampling nil) (member const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans 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) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets 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) (D formal-const-decl "posnat" inexact_sampling nil) (below type-eq-decl nil naturalnumbers nil) (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil) (S formal-const-decl "posnat" inexact_sampling nil) (good_vote_for? const-decl "bool" good_vote_for nil) (inexact_agreement? const-decl "bool" inexact_sampling nil)) 2907 580 t nil)) (symmetry_correspondence 0 (symmetry_correspondence-1 nil 3276532721 3276532725 ("" (skosimp*) (("" (expand "inexact_symmetry?") (("" (expand "exact_symmetry?") (("" (iff) (("" (split) (("1" (flatten) (("1" (skosimp*) (("1" (inst?) (("1" (inst - "d2!1") (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (skosimp*) (("2" (inst?) (("2" (inst - "d2!1") (("2" (assert) (("2" (assert) (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((exact_symmetry? const-decl "bool" exact_sampling nil) (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil) (S formal-const-decl "posnat" inexact_sampling nil) (below type-eq-decl nil naturalnumbers nil) (D formal-const-decl "posnat" inexact_sampling 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) (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) (inexact_symmetry? const-decl "bool" inexact_sampling nil)) 2669 270 t nil))) $$$k_inexact.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % File Name : k_inexact.pvs % % Purpose : validity and agreement properties for all destination % nodes of a k-stage exchange. % % Assumptions : Bounded error introduced during communication. % % Guarantees : % % Design : SPIDER Version 2 % % Dependencies : % % Comments : % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% k_inexact [ N : [nat -> posnat], % Number of source nodes at each stage default: [nat -> real] ] : THEORY BEGIN IMPORTING inexact_sampling, k_stage_shared[N, real, <=, default] %+ Workaround problem with finite_sets_minmax overloading min and max (via select_minmax) x, y : VAR real min(x,y): MACRO real = real_defs.min(x,y) max(x,y): MACRO real = real_defs.max(x,y) %- eps_l, eps_u : VAR nonneg_real epsilon, delta : VAR nonneg_real i, j, k: VAR nat good: VAR [j : nat -> non_empty_finite_set[below(N(j))]] nonasym: VAR [j : nat -> non_empty_finite_set[below(N(j))]] eligible: VAR [j : nat -> [below(N(j+1)) -> finite_set[below(N(j))]]] good_eligible: VAR [j : nat -> [below(N(j+1)) -> finite_set[below(N(j))]]] sent: VAR [j : nat -> [below(N(j)) -> real]] rcvd: VAR [j : nat -> [below(N(j+1)) -> [below(N(j)) -> real]]] % Abstracted model of communication sampling_lower_bound?(good_eligible, sent, rcvd, eps_l, j, k): bool = FORALL i : j <= i AND i < k IMPLIES sampling_lower_bound?[N(i), N(i + 1)](good_eligible(i), sent(i), rcvd(i), eps_l) sampling_upper_bound?(good_eligible, sent, rcvd, eps_u, j, k): bool = FORALL i : j <= i AND i < k IMPLIES sampling_upper_bound?[N(i), N(i + 1)](good_eligible(i), sent(i), rcvd(i), eps_u) relative_sampling_bound?(good_eligible, sent, rcvd, epsilon, j, k): bool = FORALL i : j <= i AND i < k IMPLIES relative_sampling_bound?[N(i), N(i + 1)](good_eligible(i), sent(i), rcvd(i), epsilon) inexact_symmetry?(nonasym, rcvd, epsilon, j, k): bool = FORALL i : j <= i AND i < k IMPLIES inexact_symmetry?[N(i), N(i + 1)](nonasym(i), rcvd(i), epsilon) % Main results lower_validity: THEOREM protocol(sent, rcvd, eligible, j, j + k) AND majority_subsets?(good_filter(good, eligible), eligible, j, j + k) AND sampling_lower_bound?(good_filter(good, eligible), sent, rcvd, eps_l, j, j + k) IMPLIES v_min(sent, good)(j) - k * eps_l <= v_min(sent, good)(j + k) upper_validity: THEOREM protocol(sent, rcvd, eligible, j, j + k) AND majority_subsets?(good_filter(good, eligible), eligible, j, j + k) AND sampling_upper_bound?(good_filter(good, eligible), sent, rcvd, eps_u, j, j + k) IMPLIES v_max(sent, good)(j + k) <= v_max(sent, good)(j) + k * eps_u master_slave: COROLLARY protocol(sent, rcvd, eligible, j, j + k) AND majority_subsets?(good_filter(good, eligible), eligible, j, j + k) AND sampling_lower_bound?(good_filter(good, eligible), sent, rcvd, eps_l, j, j + k) AND sampling_upper_bound?(good_filter(good, eligible), sent, rcvd, eps_u, j, j + k) AND v_max(sent, good)(j) - v_min(sent, good)(j) <= delta IMPLIES FORALL (s : (good(j))), (d : (good(j + k))): abs(sent(j)(s) - sent(j + k)(d)) <= delta + k * max(eps_l, eps_u) agreement_propagation: THEOREM protocol(sent, rcvd, eligible, j, j + k) AND majority_subsets?(good_filter(good, eligible), eligible, j, j + k) AND relative_sampling_bound?(good_filter(good, eligible), sent, rcvd, epsilon, j, j + k) AND v_max(sent, good)(j) - v_min(sent, good)(j) <= delta IMPLIES v_max(sent, good)(j + k) - v_min(sent, good)(j + k) <= delta + k * epsilon agreement_generation: THEOREM protocol(sent, rcvd, eligible, j, j + k) AND eligible_nonasymmetric?(good_filter(good, eligible), eligible, nonasym, j, j + k) AND relative_sampling_bound?(good_filter(good, eligible), sent, rcvd, epsilon, j, j + k) AND inexact_symmetry?(nonasym, rcvd, epsilon, j, j + k) IMPLIES v_max(sent, good)(j + k) - v_min(sent, good)(j + k) <= k * epsilon END k_inexact $$$k_inexact.prf (k_inexact (lower_validity 0 (lower_validity-1 nil 3292172538 3292354434 ("" (induct "k") (("1" (skosimp*) (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (inst?) (("2" (inst?) (("2" (inst - "eps_l!1" _) (("2" (inst?) (("2" (prop) (("1" (lemma "v_min_witness[N(1 + j!2 + j!1), real, <=]") (("1" (inst?) (("1" (skosimp*) (("1" (expand "protocol") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (replace*) (("1" (expand "majority_subsets?") (("1" (inst?) (("1" (assert) (("1" (expand "majority_subsets?") (("1" (inst - "n!1") (("1" (hide -2 -4) (("1" (forward-chain "majority_subset_nonempty[below(N(j!1+j!2))]") (("1" (expand "voter") (("1" (assert) (("1" (use "middle_value_lower_validity[N(j!1 + j!2), real, <=]") (("1" (assert) (("1" (skosimp*) (("1" (expand "sampling_lower_bound?") (("1" (inst?) (("1" (assert) (("1" (expand "sampling_lower_bound?") (("1" (inst?) (("1" (assert) (("1" (expand "good_filter") (("1" (expand "intersection") (("1" (expand "member") (("1" (flatten) (("1" (assert) (("1" (lemma "v_min_is_min[N(j!2 + j!1), real, <=]") (("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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("3" (expand "majority_subsets?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (expand "sampling_lower_bound?") (("4" (skosimp*) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((v_min_witness formula-decl nil select_minmax nil) (majority_subset_nonempty formula-decl nil pigeonhole nil) (member const-decl "bool" sets nil) (v_min_is_min formula-decl nil select_minmax nil) (intersection const-decl "set" sets nil) (sampling_lower_bound? const-decl "bool" inexact_sampling nil) (middle_value_lower_validity formula-decl nil middle_value_index nil) (voter const-decl "T" voter nil) (majority_subsets? const-decl "bool" eligibility nil) (nat_induction formula-decl nil naturalnumbers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (v_min const-decl "T" select_minmax nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (sampling_lower_bound? const-decl "bool" k_inexact nil) (good_filter const-decl "[below(N(j + 1)) -> finite_set[below(N(j))]]" k_inexact nil) (majority_subsets? const-decl "bool" k_inexact nil) (protocol const-decl "bool" k_inexact nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (nonneg_real nonempty-type-eq-decl nil real_types 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 "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (N formal-const-decl "[nat -> posnat]" k_inexact 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) (pred type-eq-decl nil defined_types 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)) 5883 4450 t shostak)) (upper_validity 0 (upper_validity-1 nil 3292188822 3292354439 ("" (induct "k") (("1" (skosimp*) (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (inst - _ "eps_u!1" _ "j!2" _ _) (("2" (inst?) (("2" (inst?) (("2" (inst?) (("2" (prop) (("1" (lemma "v_max_witness[N(1 + j!2 + j!1), real, <=]") (("1" (inst?) (("1" (skosimp*) (("1" (expand "protocol") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (replace*) (("1" (hide -2 -4) (("1" (expand "majority_subsets?") (("1" (inst?) (("1" (assert) (("1" (expand "majority_subsets?") (("1" (inst - "n!1") (("1" (forward-chain "majority_subset_nonempty[below(N(j!1+j!2))]") (("1" (expand "voter") (("1" (assert) (("1" (use "middle_value_upper_validity[N(j!1 + j!2), real, <=]") (("1" (assert) (("1" (skosimp*) (("1" (expand "sampling_upper_bound?") (("1" (inst?) (("1" (assert) (("1" (expand "sampling_upper_bound?") (("1" (inst?) (("1" (assert) (("1" (expand "good_filter") (("1" (expand "intersection") (("1" (expand "member") (("1" (flatten) (("1" (assert) (("1" (lemma "v_max_is_max[N(j!2 + j!1), real, <=]") (("1" (inst - _ _ "sent!1(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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("3" (expand "majority_subsets?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil) ("4" (expand "sampling_upper_bound?") (("4" (skosimp*) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((v_max_witness formula-decl nil select_minmax nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (majority_subsets? const-decl "bool" eligibility nil) (majority_subset_nonempty formula-decl nil pigeonhole nil) (member const-decl "bool" sets nil) (v_max_is_max formula-decl nil select_minmax nil) (intersection const-decl "set" sets nil) (sampling_upper_bound? const-decl "bool" inexact_sampling nil) (middle_value_upper_validity formula-decl nil middle_value_index nil) (voter const-decl "T" voter nil) (nat_induction formula-decl nil naturalnumbers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (v_max const-decl "T" select_minmax nil) (<= const-decl "bool" reals nil) (sampling_upper_bound? const-decl "bool" k_inexact nil) (good_filter const-decl "[below(N(j + 1)) -> finite_set[below(N(j))]]" k_inexact nil) (majority_subsets? const-decl "bool" k_inexact nil) (protocol const-decl "bool" k_inexact nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (nonneg_real nonempty-type-eq-decl nil real_types 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 "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (N formal-const-decl "[nat -> posnat]" k_inexact 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) (pred type-eq-decl nil defined_types 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)) 5100 3980 t nil)) (master_slave 0 (master_slave-1 nil 3292193659 3292354442 ("" (skosimp*) (("" (case-replace "k!1 * real_defs.max(eps_l!1, eps_u!1) = max(k!1 * eps_l!1, k!1 * eps_u!1)") (("1" (hide -1) (("1" (forward-chain "lower_validity") (("1" (forward-chain "upper_validity") (("1" (lemma "v_min_is_min[N(j!1), real, <=]") (("1" (lemma "v_min_is_min[N(j!1 + k!1), real, <=]") (("1" (inst?) (("1" (inst?) (("1" (inst?) (("1" (inst?) (("1" (lemma "v_max_is_max[N(j!1), real, <=]") (("1" (lemma "v_max_is_max[N(j!1 + k!1), real, <=]") (("1" (assert) (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (inst - "s!1" _ _) (("1" (inst?) (("1" (assert) (("1" (expand "abs") (("1" (lift-if) (("1" (assert) 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 1) (("2" (rewrite "max") (("2" (lift-if) (("2" (expand "max") (("2" (lift-if) (("2" (assert) (("2" (ground) (("1" (mult-by 1 "k!1") (("1" (assert) nil nil)) nil) ("2" (mult-by -1 "k!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (max const-decl "{p: real | p >= m AND p >= n}" real_defs nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (lower_validity formula-decl nil k_inexact 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]" k_inexact nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields 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) (v_min_is_min formula-decl nil select_minmax nil) (<= const-decl "bool" reals nil) (v_max_is_max formula-decl nil select_minmax nil) (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil) (upper_validity formula-decl nil k_inexact nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props "Manip/")) 3001 2070 t shostak)) (agreement_propagation 0 (agreement_propagation-1 nil 3292264504 3292355246 ("" (induct "k") (("1" (assert) (("1" (skosimp*) nil nil)) nil) ("2" (skosimp*) (("2" (inst?) (("2" (inst?) (("2" (inst - "epsilon!1" _) (("2" (inst?) (("2" (assert) (("2" (prop) (("1" (hide -5) (("1" (expand "relative_sampling_bound?") (("1" (inst - "j!1 + j!2") (("1" (assert) (("1" (expand "majority_subsets?") (("1" (inst?) (("1" (assert) (("1" (lemma "v_min_witness[N(1 + j!2 + j!1), real, <=]") (("1" (inst?) (("1" (lemma "v_max_witness[N(1 + j!2 + j!1), real, <=]") (("1" (inst?) (("1" (skosimp*) (("1" (replace*) (("1" (hide -2 -4) (("1" (expand "protocol") (("1" (inst?) (("1" (assert) (("1" (inst-cp - "n!1") (("1" (inst - "n!2") (("1" (replace*) (("1" (hide -4 -5) (("1" (lemma "majority_subsets_nonempty[N(j!1 + j!2), N(1 + j!1 + j!2)]") (("1" (inst - _ "good_filter(good!1, eligible!1)(j!1 + j!2)" "eligible!1(j!1 + j!2)") (("1" (inst-cp - "n!2") (("1" (inst - "n!1") (("1" (assert) (("1" (expand "voter") (("1" (expand "majority_subsets?") (("1" (inst-cp - "n!2") (("1" (inst - "n!1") (("1" (lemma "middle_value_upper_validity[N(j!1 + j!2), real, <=]") (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (hide -6) (("1" (lemma "middle_value_lower_validity[N(j!1 + j!2), real, <=]") (("1" (inst - "eligible!1(j!1 + j!2)(n!2)" "rcvd!1(j!1 + j!2)(n!2)" _) (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (expand "relative_sampling_bound?") (("1" (inst - "n!1" "n!2" "i!1" "i!2") (("1" (assert) (("1" (lemma "v_min_is_min[N(j!2 + j!1), real, <=]") (("1" (inst?) (("1" (inst - "i!2") (("1" (lemma "v_max_is_max[N(j!2 + j!1), real, <=]") (("1" (inst - "i!1" _ _) (("1" (inst?) (("1" (expand* "good_filter" "intersection" "member") (("1" (flatten) (("1" (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)) 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)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-2 1)) (("3" (expand "majority_subsets?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil) ("4" (hide-all-but (-3 1)) (("4" (assert) (("4" (expand "relative_sampling_bound?") (("4" (skosimp*) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((v_min_witness formula-decl nil select_minmax nil) (v_max_witness formula-decl nil select_minmax nil) (majority_subsets_nonempty formula-decl nil eligibility nil) (majority_subsets? const-decl "bool" eligibility nil) (relative_sampling_bound? const-decl "bool" inexact_sampling nil) (v_max_is_max formula-decl nil select_minmax nil) (member const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (v_min_is_min formula-decl nil select_minmax nil) (middle_value_lower_validity formula-decl nil middle_value_index nil) (middle_value_upper_validity formula-decl nil middle_value_index nil) (voter const-decl "T" voter nil) (nat_induction formula-decl nil naturalnumbers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (v_min const-decl "T" select_minmax nil) (v_max const-decl "T" select_minmax nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (relative_sampling_bound? const-decl "bool" k_inexact nil) (good_filter const-decl "[below(N(j + 1)) -> finite_set[below(N(j))]]" k_inexact nil) (majority_subsets? const-decl "bool" k_inexact nil) (protocol const-decl "bool" k_inexact nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (N formal-const-decl "[nat -> posnat]" k_inexact 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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (pred type-eq-decl nil defined_types 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)) 155980 51180 t nil)) (agreement_generation 0 (agreement_generation-2 nil 3292264574 3292461250 ("" (skosimp*) (("" (expand "eligible_nonasymmetric?") (("" (skosimp*) (("" (case "v_max(sent!1, good!1)(i!1+1) - v_min(sent!1, good!1)(i!1+1) <= epsilon!1") (("1" (lemma "agreement_propagation") (("1" (inst - "epsilon!1" "eligible!1" "epsilon!1" "good!1" "i!1+1" " j!1 + k!1 - (i!1 + 1)" "rcvd!1" "sent!1") (("1" (assert) (("1" (prop) (("1" (assert) (("1" (mult-by -4 "epsilon!1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (expand "protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-8 1)) (("3" (expand "relative_sampling_bound?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (hide -6 -7 2) (("2" (expand "inexact_symmetry?") (("2" (inst?) (("2" (assert) (("2" (lemma "v_max_witness[N(1 + i!1), real, <=]") (("2" (inst?) (("2" (skosimp*) (("2" (lemma "v_min_witness[N(1 + i!1), real, <=]") (("2" (inst?) (("2" (skosimp*) (("2" (replace*) (("2" (expand "protocol") (("2" (inst?) (("2" (assert) (("2" (hide -2 -4) (("2" (inst-cp - "n!2") (("2" (inst - "n!1") (("2" (replace*) (("2" (hide -3 -4) (("2" (expand "voter") (("2" (lemma "eligible_agree[N(i!1), N(i!1 + 1)]") (("2" (inst - "n!1" "n!2" "nonasym!1(i!1)" "eligible!1(i!1)") (("2" (assert) (("2" (lift-if) (("2" (assert) (("2" (prop) (("2" (lemma "middle_value_overlap[N(i!1), real, <=]") (("2" (inst - "eligible!1(i!1)(n!2)" "rcvd!1(i!1)(n!2)" "rcvd!1(i!1)(n!1)") (("1" (skosimp*) (("1" (expand "inexact_symmetry?") (("1" (inst - "n!1" "n!2" "j!2") (("1" (expand* "subsets?" "subset?" "member") (("1" (inst?) (("1" (assert) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((eligible_nonasymmetric? const-decl "bool" k_inexact nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (v_min const-decl "T" select_minmax nil) (v_max const-decl "T" select_minmax 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) (below type-eq-decl nil naturalnumbers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (N formal-const-decl "[nat -> posnat]" k_inexact 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals 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) (- const-decl "[numfield -> numfield]" number_fields nil) (i!1 skolem-const-decl "nat" k_inexact nil) (j!1 skolem-const-decl "nat" k_inexact nil) (k!1 skolem-const-decl "nat" k_inexact nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props "Manip/") (protocol const-decl "bool" k_inexact nil) (relative_sampling_bound? const-decl "bool" k_inexact nil) (agreement_propagation formula-decl nil k_inexact nil) (inexact_symmetry? const-decl "bool" k_inexact nil) (v_min_witness formula-decl nil select_minmax nil) (voter const-decl "T" voter nil) (eligible!1 skolem-const-decl "[j: nat -> [below(N(1 + j)) -> finite_set[below(N(j))]]]" k_inexact nil) (n!2 skolem-const-decl "below(N(1 + i!1))" k_inexact nil) (inexact_symmetry? const-decl "bool" inexact_sampling nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (subsets? const-decl "bool" eligibility nil) (middle_value_overlap formula-decl nil middle_value_index nil) (eligible_agree formula-decl nil eligibility nil) (v_max_witness formula-decl nil select_minmax nil)) 228048 18350 t nil) (agreement_generation-1 nil 3292264405 3292264419 ("" (skosimp*) (("" (expand "nonasymmetric_filtered") (("" (skosimp*) (("" (case "max_good(sent!1, good!1)(i!1+1) - min_good(sent!1, good!1)(i!1+1) <= epsilon!1") (("1" (lemma "agreement_propagation_alt_alt") (("1" (inst - "epsilon!1" "epsilon!1" "filtered!1" "good!1" "i!1+1" " j!1 + k!1 - (i!1 + 1)" "rcvd!1" "sent!1") (("1" (assert) (("1" (prop) (("1" (assert) (("1" (mult-by -5 "epsilon!1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but (-2 1)) (("2" (expand "protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but (-8 1)) (("3" (expand "inexact_agreement_alt?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (hide -6 -7 2) (("2" (expand "eligible_sources_invariant") (("2" (inst?) (("2" (assert) (("2" (expand "inexact_symmetry?") (("2" (inst?) (("2" (assert) (("2" (lemma "max_good_witness") (("2" (inst?) (("2" (skosimp*) (("2" (lemma "min_good_witness") (("2" (inst?) (("2" (skosimp*) (("2" (replace*) (("2" (expand "protocol") (("2" (inst?) (("2" (assert) (("2" (hide -2 -4) (("2" (inst-cp - "d!2") (("2" (inst - "d!1") (("2" (replace*) (("2" (hide -3 -4) (("2" (expand "voter") (("2" (case-replace "filtered!1(i!1)(d!1) = filtered!1(i!1)(d!2)") (("1" (lift-if) (("1" (assert) (("1" (prop) (("1" (lemma "middle_value_overlap[N(i!1), real, <=]") (("1" (inst - "filtered!1(i!1)(d!2)" "rcvd!1(i!1)(d!2)" "rcvd!1(i!1)(d!1)") (("1" (skosimp*) (("1" (expand "inexact_symmetry?") (("1" (inst?) (("1" (inst - "d!1") (("1" (expand "subsets?") (("1" (expand "subset?") (("1" (expand "member") (("1" (inst?) (("1" (assert) (("1" (assert) (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 -4 -5 -7 2) (("2" (apply-extensionality :hide? t) (("2" (expand "eligible_sources_invariant") (("2" (iff) (("2" (inst?) (("2" (expand "subsets?") (("2" (prop) (("1" (hide 1) (("1" (inst?) (("1" (expand "subset?") (("1" (expand "member") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 1) (("2" (expand "subset?") (("2" (expand "member") (("2" (inst?) (("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)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((inexact_symmetry? const-decl "bool" k_inexact nil) (voter const-decl "T" voter nil) (inexact_symmetry? const-decl "bool" inexact_sampling nil) (subset? const-decl "bool" sets nil) (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil) (member const-decl "bool" sets nil) (subsets? const-decl "bool" eligibility nil) (middle_value_overlap formula-decl nil middle_value_index nil) (= const-decl "[T, T -> boolean]" equalities nil) (protocol const-decl "bool" k_inexact nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props "Manip/") (- const-decl "[numfield -> numfield]" number_fields 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) (bool nonempty-type-eq-decl nil booleans nil) (<= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (< 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]" k_inexact 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) (nonneg_real nonempty-type-eq-decl nil real_types nil)) 12698 1610 t nil))) $$$exact_sampling.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % File Name : exact_sampling.pvs % % Purpose : % % Assumptions : % % Guarantees : % % Design : SPIDER Version 0 % % Dependencies : % % Comments : % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% exact_sampling [ S : posnat, % Number of sources D : posnat, % Number of receivers, T : TYPE ] : THEORY BEGIN IMPORTING good_vote_for[S, T] t: VAR T s, s1, s2: VAR below(S) d, d1, d2: VAR below(D) good_eligible: VAR [below(D) -> finite_set[below(S)]] eligible: VAR finite_set[below(S)] est: VAR [below(D) -> [below(S) -> T]] ideal: VAR [below(S) -> T] sampling_exact?(good_eligible, ideal, est): bool = FORALL d, s: good_eligible(d)(s) => ideal(s) = est(d)(s) exact_agreement?(good_eligible, est): bool = EXISTS t: FORALL d1, d2: good_vote_for?(good_eligible(d1), est(d1), t) AND good_vote_for?(good_eligible(d2), est(d2), t) exact_symmetry?(eligible, est): bool = FORALL d1, d2, s: eligible(s) IMPLIES est(d1)(s) = est(d2)(s) END exact_sampling $$$voter.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % File Name : voter.pvs % % Design : SPIDER Version 0 % % PVS : Version 3.1 % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% voter [ S : posnat, D : posnat, T : TYPE+ ]: THEORY BEGIN default: VAR T d: VAR below(D) eligible: VAR [below(D) -> finite_set[below(S)]] rcvd: VAR [below(D) -> [below(S) -> T]] vote_function: VAR [[non_empty_finite_set[below(S)], [below(S) -> T]] -> T] voter(vote_function, eligible, rcvd, default)(d): T = IF NOT empty?[below(S)](eligible(d)) THEN vote_function(eligible(d), rcvd(d)) ELSE default ENDIF END voter $$$eligibility.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % File Name : eligibility.pvs % % Purpose : Properties of eligibility. This theory is to % contain only predicates that are requirements of % eligible vote sets. % % Design : SPIDER Version 2 % % PVS : Version 3.1 % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% eligibility[ S : posnat, % Number of sources D : posnat % Number of destinations ] : THEORY BEGIN IMPORTING pigeonhole s: VAR below(S) d, d1, d2: VAR below(D) good_select: VAR [below(D) -> finite_set[below(S)]] good: VAR finite_set[below(S)] nonasym: VAR finite_set[below(S)] agreed: VAR non_empty_finite_set[below(S)] eligible: VAR finite_set[below(S)] select_nonempty: VAR [below(D) -> non_empty_finite_set[below(S)]] select: VAR [below(D) -> finite_set[below(S)]] % Abstracted single stage fault assumptions majority_subsets?(good_select, select): bool = FORALL d: majority_subset?(good_select(d), select(d)) majority_subsets_nonempty: LEMMA majority_subsets?(good_select, select) IMPLIES NOT empty?[below(S)](select(d)) byzantine_majority_subsets?(good_select, select): bool = FORALL d: byzantine_majority_subset?(good_select(d), select(d)) subsets?(select, good): bool = FORALL d: subset?(select(d), good) %------------------------------------------------ eligible_sources_property?(select, nonasym): bool = FORALL s, d1, d2: nonasym(s) IMPLIES select(d1)(s) IFF select(d2)(s) eligible_agree: LEMMA subsets?(select, nonasym) AND eligible_sources_property?(select, nonasym) IMPLIES select(d1) = select(d2) eligible_agree?(select, eligible) : bool = FORALL d: select(d) = eligible eligible_non_empty: LEMMA eligible_agree?(select_nonempty, eligible) IMPLIES NOT empty?(eligible) END eligibility $$$eligibility.prf (eligibility (majority_subsets_nonempty 0 (majority_subsets_nonempty-1 nil 3276528224 3292266872 ("" (skosimp*) (("" (expand "majority_subsets?") (("" (inst?) (("" (forward-chain "majority_subset_nonempty") nil nil)) nil)) nil)) nil) proved ((majority_subsets? const-decl "bool" eligibility nil) (majority_subset_nonempty formula-decl nil pigeonhole nil) (S formal-const-decl "posnat" eligibility 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) (below type-eq-decl nil naturalnumbers nil) (D formal-const-decl "posnat" eligibility 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) (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)) 58 40 t shostak)) (eligible_agree 0 (eligible_agree-1 nil 3292266913 3292267014 ("" (skosimp*) (("" (apply-extensionality :hide? t) (("" (iff) (("" (expand "eligible_sources_property?") (("" (inst?) (("" (inst - "d2!1") (("" (expand "subsets?") (("" (prop) (("" (expand "subset?") (("" (expand "member") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((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) (S formal-const-decl "posnat" eligibility nil) (below type-eq-decl nil naturalnumbers nil) (set type-eq-decl nil sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (D formal-const-decl "posnat" eligibility nil) (eligible_sources_property? const-decl "bool" eligibility nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (subsets? const-decl "bool" eligibility nil)) 100978 4470 t shostak)) (eligible_non_empty 0 (eligible_non_empty-1 nil 3276433771 3292266872 ("" (skosimp*) (("" (expand "eligible_agree?") (("" (inst - "0") (("1" (typepred! "select_nonempty!1(0)") (("1" (expand "empty?") (("1" (skosimp*) (("1" (inst - "x!1") (("1" (replace -3 :dir rl) (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) proved ((eligible_agree? const-decl "bool" eligibility nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets 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) (S formal-const-decl "posnat" eligibility nil) (NOT const-decl "[bool -> bool]" booleans nil) (below type-eq-decl nil naturalnumbers nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (bool nonempty-type-eq-decl nil booleans nil) (< const-decl "bool" 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (D formal-const-decl "posnat" eligibility nil)) 86 60 t shostak))) $$$pigeonhole.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Design : SPIDER Version 2 % % PVS : Version 3.1 % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% pigeonhole[T: TYPE]: THEORY BEGIN A, A1, A2, B, C, S, S1, S2: VAR finite_set[T] x: VAR T pigeonhole: THEOREM card(A) + card(B) > card(union(A,B)) IMPLIES EXISTS x: A(x) AND B(x) majority_subset?(A,S): bool = 2*card(A) > card(S) AND subset?(A,S) majority_subset_nonempty: LEMMA majority_subset?(A,S) IMPLIES NOT empty?(S) majority_nonempty: LEMMA majority_subset?(A,S) IMPLIES NOT empty?(A) majority_pigeonhole: THEOREM 2*card(A) > card(S) AND subset?(A,S) AND 2*card(B) >= card(S) AND subset?(B,S) IMPLIES EXISTS x: A(x) AND B(x) byzantine_majority_subset?(A,S): bool = 3*card(A) > 2*card(S) AND subset?(A,S) byzantine_majority_subset_nonempty: LEMMA byzantine_majority_subset?(A,S) IMPLIES NOT empty?(S) byzantine_majority_nonempty: LEMMA byzantine_majority_subset?(A,S) IMPLIES NOT empty?(A) byzantine_majority_pigeonhole: THEOREM 3*card(A) > 2*card(S) AND subset?(A,S) AND 3*card(B) >= card(S) AND subset?(B,S) IMPLIES EXISTS x: A(x) AND B(x) byzantine_majority_pigeonhole2: THEOREM 3*card(A) >= 2*card(S) AND subset?(A,S) AND 3*card(B) > card(S) AND subset?(B,S) IMPLIES EXISTS x: A(x) AND B(x) byzantine_overlap_pigeonhole_sym: THEOREM card(S1) >= card(S2) AND byzantine_majority_subset?(A,S1) AND byzantine_majority_subset?(A,S2) AND 3*card(B) >= 2*card(S1) AND subset?(B,S1) AND 3*card(C) >= 2*card(S2) AND subset?(C,S2) IMPLIES EXISTS x: A(x) AND B(x) AND C(x) byzantine_overlap_pigeonhole: THEOREM byzantine_majority_subset?(A,S1) AND byzantine_majority_subset?(A,S2) AND 3*card(B) >= 2*card(S1) AND subset?(B,S1) AND 3*card(C) >= 2*card(S2) AND subset?(C,S2) IMPLIES EXISTS x: A(x) AND B(x) AND C(x) END pigeonhole $$$pigeonhole.prf (pigeonhole (pigeonhole 0 (pigeonhole-1 nil 3266842135 3266842233 ("" (skosimp*) (("" (case "card(intersection(A!1, B!1)) >= 1") (("1" (hide -2) (("1" (forward-chain "card_1_has_1") (("1" (hide -2) (("1" (skosimp*) (("1" (expand* "intersection" "member") (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "card_plus[T]") (("2" (assert) nil nil)) nil)) nil)) nil) unchecked ((intersection const-decl "set" sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (= const-decl "[T, T -> boolean]" equalities 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) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil pigeonhole 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) (card_1_has_1 formula-decl nil finite_sets nil) (member const-decl "bool" sets nil) (card_plus formula-decl nil finite_sets nil)) 54744 5690 t nil)) (majority_subset_nonempty 0 (majority_subset_nonempty-1 nil 3267459600 3267459694 ("" (skosimp*) (("" (expand "majority_subset?") (("" (flatten) (("" (use "nonempty_card[T]") (("" (assert) (("" (expand* "nonempty?" "empty?" "subset?" "member") (("" (skosimp*) (("" (inst?) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((majority_subset? const-decl "bool" pigeonhole nil) (nonempty_card formula-decl nil finite_sets nil) (T formal-type-decl nil pigeonhole 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) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil)) 93831 7330 t shostak)) (majority_nonempty 0 (majority_nonempty-1 nil 3276456345 3276456628 ("" (skosimp*) (("" (lemma "majority_subset_nonempty") (("" (inst?) (("" (assert) (("" (expand "majority_subset?") (("" (flatten) (("" (lemma "card_empty?[T]") (("" (inst-cp - "S!1") (("" (inst - "A!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((majority_subset_nonempty formula-decl nil pigeonhole nil) (card_empty? formula-decl nil finite_sets nil) (majority_subset? const-decl "bool" pigeonhole 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) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil pigeonhole nil)) 282760 11350 t shostak)) (majority_pigeonhole 0 (majority_pigeonhole-1 nil 3266842135 3266842142 ("" (skosimp*) (("" (case "card(union(A!1,B!1)) <= card(S!1)") (("1" (use "pigeonhole") (("1" (assert) nil nil)) nil) ("2" (hide -1 -3 2) (("2" (rewrite "card_subset") (("2" (rewrite "union_upper_bound") nil nil)) nil)) nil)) nil)) nil) unchecked ((union const-decl "set" sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals 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) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil pigeonhole 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) (pigeonhole formula-decl nil pigeonhole nil) (card_subset formula-decl nil finite_sets nil) (union_upper_bound formula-decl nil sets_lemmas nil)) 905 830 nil nil)) (byzantine_majority_subset_nonempty 0 (byzantine_majority_subset_nonempty-1 nil 3278759253 3278759397 ("" (skosimp*) (("" (lemma "majority_subset_nonempty") (("" (expand "majority_subset?") (("" (expand "byzantine_majority_subset?") (("" (inst?) (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((majority_subset_nonempty formula-decl nil pigeonhole nil) (byzantine_majority_subset? const-decl "bool" pigeonhole 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) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil pigeonhole nil) (majority_subset? const-decl "bool" pigeonhole nil)) 25874 2130 t nil)) (byzantine_majority_nonempty 0 (byzantine_majority_nonempty-1 nil 3278773608 3278773656 ("" (skosimp*) (("" (lemma "byzantine_majority_subset_nonempty") (("" (inst?) (("" (assert) (("" (expand "byzantine_majority_subset?") (("" (flatten) (("" (lemma "card_empty?[T]") (("" (inst-cp - "S!1") (("" (inst - "A!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((byzantine_majority_subset_nonempty formula-decl nil pigeonhole nil) (card_empty? formula-decl nil finite_sets nil) (byzantine_majority_subset? const-decl "bool" pigeonhole 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) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil pigeonhole nil)) 44826 3040 t nil)) (byzantine_majority_pigeonhole 0 (byzantine_majority_pigeonhole-1 nil 3266842135 3266842143 ("" (skosimp*) (("" (case "card(union(A!1,B!1)) <= card(S!1)") (("1" (hide -3 -5) (("1" (use "pigeonhole") (("1" (assert) nil nil)) nil)) nil) ("2" (hide -1 -3 2) (("2" (rewrite "card_subset") (("2" (rewrite "union_upper_bound") nil nil)) nil)) nil)) nil)) nil) unchecked ((union const-decl "set" sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals 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) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil pigeonhole 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) (pigeonhole formula-decl nil pigeonhole nil) (card_subset formula-decl nil finite_sets nil) (union_upper_bound formula-decl nil sets_lemmas nil)) 917 830 nil nil)) (byzantine_majority_pigeonhole2 0 (byzantine_majority_pigeonhole2-1 nil 3266842135 3266842144 ("" (skosimp*) (("" (case "card(union(A!1,B!1)) <= card(S!1)") (("1" (hide -3 -5) (("1" (use "pigeonhole") (("1" (assert) nil nil)) nil)) nil) ("2" (hide -1 -3 2) (("2" (rewrite "card_subset") (("2" (rewrite "union_upper_bound") nil nil)) nil)) nil)) nil)) nil) unchecked ((union const-decl "set" sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals 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) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil pigeonhole 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) (pigeonhole formula-decl nil pigeonhole nil) (card_subset formula-decl nil finite_sets nil) (union_upper_bound formula-decl nil sets_lemmas nil)) 1002 910 nil nil)) (byzantine_overlap_pigeonhole_sym 0 (byzantine_overlap_pigeonhole_sym-1 nil 3266842135 3266842333 ("" (expand "byzantine_majority_subset?") (("" (skosimp*) (("" (case "3*card(intersection(A!1,B!1)) > card(S1!1)") (("1" (hide -3 -4 -5 -7 -8) (("1" (use "byzantine_majority_pigeonhole2") (("1" (assert) (("1" (prop) (("1" (hide-all-but (-1 1)) (("1" (expand* "intersection" "member") (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 1)) (("2" (use "intersection_subset1[T]") (("2" (forward-chain "subset_transitive[T]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -4 -5 -8 -9 2) (("2" (lemma "card_plus[T]") (("2" (inst?) (("2" (lemma "union_upper_bound[T]") (("2" (inst - "A!1" "B!1" "S1!1") (("2" (assert) (("2" (forward-chain "card_subset") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((union const-decl "set" sets nil) (card_subset formula-decl nil finite_sets nil) (union_upper_bound formula-decl nil sets_lemmas nil) (card_plus formula-decl nil finite_sets nil) (subset_transitive formula-decl nil sets_lemmas nil) (intersection_subset1 formula-decl nil sets_lemmas nil) (member const-decl "bool" sets nil) (byzantine_majority_pigeonhole2 formula-decl nil pigeonhole 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) (bool nonempty-type-eq-decl nil booleans nil) (> const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (T formal-type-decl nil pigeonhole 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) (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) (= const-decl "[T, T -> boolean]" equalities nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (intersection const-decl "set" sets nil) (byzantine_majority_subset? const-decl "bool" pigeonhole nil)) 70689 12620 t nil)) (byzantine_overlap_pigeonhole 0 (byzantine_overlap_pigeonhole-1 nil 3266842135 3266842147 ("" (skosimp*) (("" (case "card(S1!1) >= card(S2!1)") (("1" (use "byzantine_overlap_pigeonhole_sym") (("1" (prop) nil nil)) nil) ("2" (lemma "byzantine_overlap_pigeonhole_sym") (("2" (inst - "A!1" "C!1" "B!1" "S2!1" "S1!1") (("2" (assert) (("2" (skosimp*) (("2" (inst?) (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (= const-decl "[T, T -> boolean]" equalities 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) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil pigeonhole 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) (byzantine_overlap_pigeonhole_sym formula-decl nil pigeonhole nil)) 862 820 nil nil))) $$$index_filters.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Design : SPIDER Version 2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% index_filters[N: posnat, T: TYPE]: THEORY BEGIN IMPORTING finite_sets@finite_sets_below[N] good, select: var finite_set[below(N)] f: var [below(N) -> T] i, j: var below(N) rel: VAR [T,T -> bool] filter(rel)(select)(f)(i)(j): bool = select(j) AND rel(f(j),f(i)) filter_finite: JUDGEMENT filter(rel)(select)(f)(i) HAS_TYPE finite_set[below(N)] subset_filter: LEMMA subset?(filter(rel)(select)(f)(i),select) filter_remove: LEMMA filter(rel)(remove(j,select))(f)(i) = remove(j,filter(rel)(select)(f)(i)) END index_filters $$$index_filters.prf (index_filters (filter_finite 0 (filter_finite-1 nil 3265035253 nil ("" (skosimp*) (("" (rewrite "finite_below") nil nil)) nil) proved-complete ((finite_below formula-decl nil finite_sets_below "finite_sets/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals 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) (filter const-decl "bool" index_filters 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (M formal-const-decl "posnat" index_filters nil)) nil nil nil nil)) (subset_filter 0 (subset_filter-1 nil 3265035253 3265035274 ("" (skosimp*) (("" (expand* "subset?" "filter" "member") (("" (skosimp*) nil nil)) nil)) nil) proved ((filter const-decl "bool" index_filters nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil)) 355 90 nil nil)) (filter_remove 0 (filter_remove-1 nil 3265035285 3265035343 ("" (auto-rewrite-defs) (("" (skosimp*) (("" (apply-extensionality :hide? t) nil nil)) nil)) nil) proved ((below type-eq-decl nil naturalnumbers nil) (M formal-const-decl "posnat" index_filters 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) (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) (/= const-decl "boolean" notequal nil) (member const-decl "bool" sets nil) (remove const-decl "set" sets nil) (filter const-decl "bool" index_filters 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)) 30005 139