%% 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 1390 t shostak))) $$$index_select.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Design : SPIDER Version 2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% index_select[N: posnat, T: TYPE, leq: (total_order?[T])]: THEORY BEGIN IMPORTING index_filters[N, T], pigeonhole[below(N)] t1, t2: VAR T geq(t1,t2): bool = leq(t2, t1) good, eligible: var finite_set[below(N)] % subsets of indices f, f1, f2 : var [below(N) -> T] i, j, k, l : var below(N) n: var subrange(1,N) index_value(eligible, k ,f)(i): bool = eligible(i) AND card(filter(leq)(eligible)(f)(i)) > k AND card(filter(geq)(eligible)(f)(i)) >= card(eligible) - k index_min: LEMMA index_value(eligible, 0, f)(i) AND eligible(j) IMPLIES leq(f(i), f(j)) index_max: LEMMA eligible(j) AND index_value(eligible, card(eligible) - 1, f)(i) IMPLIES leq(f(j), f(i)) least_index_exists: LEMMA card(eligible) = n IMPLIES EXISTS i: index_value(eligible, 0, f)(i) index_exists_induct: LEMMA card(eligible) = n AND k < card(eligible) IMPLIES EXISTS i : index_value(eligible, k, f)(i) index_exists: LEMMA k < card(eligible) IMPLIES EXISTS i: index_value(eligible, k, f)(i) index_order: LEMMA k < l AND index_value(eligible, k, f)(i) AND index_value(eligible, l, f)(j) IMPLIES leq(f(i), f(j)) index_value_overlap: LEMMA index_value(eligible, k, f1)(i) AND index_value(eligible, k, f2)(l) IMPLIES EXISTS j: eligible(j) AND leq(f1(j), f1(i)) AND leq(f2(l), f2(j)) END index_select $$$index_select.prf (index_select (index_min_TCC1 0 (index_min_TCC1-1 nil 3264854173 3276349873 ("" (subtype-tcc) nil nil) proved nil 88 90 nil shostak)) (index_min 0 (index_min-4 nil 3276341041 3276349873 ("" (skosimp*) (("" (expand "index_value") (("" (flatten) (("" (hide -2) (("" (use "subset_filter") (("" (forward-chain "card_subset") (("" (use "same_card_subset[below(N)]") (("" (assert) (("" (replace -1 :dir rl) (("" (hide-all-but (-6 1)) (("" (expand "filter") (("" (expand "geq") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((index_value const-decl "bool" index_select nil) (card_subset formula-decl nil finite_sets nil) (filter const-decl "bool" index_filters nil) (same_card_subset formula-decl nil finite_sets nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (geq const-decl "bool" index_select 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) (T formal-type-decl nil index_select nil) (N formal-const-decl "posnat" index_select 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) (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) (subset_filter formula-decl nil index_filters nil)) 425 330 t nil) (index_min-3 nil 3275837333 3276339186 ("" (skosimp*) (("" (expand "index_value") (("" (flatten) (("" (hide -2) (("" (use "subset_filter") (("" (forward-chain "card_subset") (("" (use "same_card_subset[below(M)]") (("" (assert) (("" (replace -1 :dir rl) (("" (hide-all-but (-6 1)) (("" (expand "filter") (("" (expand "geq") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished ((subset_filter formula-decl nil 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) (T formal-type-decl nil index_select 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) (geq const-decl "bool" index_select nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (same_card_subset formula-decl nil finite_sets nil) (filter const-decl "bool" index_filters nil) (card_subset formula-decl nil finite_sets nil) (index_value const-decl "bool" index_select nil)) 140 100 t nil) (index_min-2 nil 3264930592 3275837307 ("" (skosimp*) (("" (expand "index_value") (("" (flatten) (("" (hide -2) (("" (use "subset_filter") (("" (forward-chain "card_subset") (("" (use "same_card_subset[below(M)]") (("" (assert) (("" (replace -1 :dir rl) (("" (hide-all-but (-6 1)) (("" (expand "filter") (("" (expand ">=") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished ((index_value const-decl "bool" index_select nil) (card_subset formula-decl nil finite_sets nil) (filter const-decl "bool" index_filters nil) (same_card_subset formula-decl nil finite_sets nil) (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) (T formal-type-decl nil index_select 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) (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) (subset_filter formula-decl nil index_filters nil)) 195 170 t nil) (index_min-1 nil 3264930563 3264930570 ("" (postpone) nil nil) unfinished nil 6645 410 t shostak)) (index_max_TCC1 0 (index_max_TCC1-1 nil 3264854173 3276352560 ("" (skosimp*) (("" (use "card_below") (("" (assert) (("" (use "nonempty_card[below(N)]") (("" (assert) (("" (expand "nonempty?") (("" (expand "empty?") (("" (expand "member") (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((card_below formula-decl nil finite_sets_below "finite_sets/") (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) (N formal-const-decl "posnat" index_select 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (nonempty_card formula-decl nil finite_sets nil) (nonempty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil)) 23653 4610 t shostak)) (index_max 0 (index_max-2 nil 3276341063 3276349874 ("" (skosimp*) (("" (expand "index_value") (("" (flatten) (("" (hide -4) (("" (use "subset_filter") (("" (forward-chain "card_subset") (("" (use "same_card_subset[below(N)]") (("" (assert) (("" (replace -1 :dir rl) (("" (rewrite "filter") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((index_value const-decl "bool" index_select nil) (card_subset formula-decl nil finite_sets nil) (filter const-decl "bool" index_filters nil) (same_card_subset formula-decl nil finite_sets nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (leq formal-const-decl "(total_order?[T])" index_select 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) (T formal-type-decl nil index_select nil) (N formal-const-decl "posnat" index_select 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) (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) (subset_filter formula-decl nil index_filters nil)) 490 390 t nil) (index_max-1 nil 3264852248 3276339187 ("" (skosimp*) (("" (expand "index_value") (("" (flatten) (("" (hide -4) (("" (use "subset_filter") (("" (forward-chain "card_subset") (("" (use "same_card_subset[below(M)]") (("" (assert) (("" (replace -1 :dir rl) (("" (rewrite "filter") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished ((index_value const-decl "bool" index_select nil) (card_subset formula-decl nil finite_sets nil) (filter const-decl "bool" index_filters nil) (same_card_subset formula-decl nil finite_sets nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (leq formal-const-decl "(total_order?[T])" index_select 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) (T formal-type-decl nil index_select 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) (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) (subset_filter formula-decl nil index_filters nil)) 182 130 t shostak)) (least_index_exists 0 (least_index_exists-6 nil 3276345315 3276349878 ("" (induct "n") (("1" (skosimp*) (("1" (rewrite "card_one") (("1" (skosimp*) (("1" (replace -1) (("1" (expand "index_value") (("1" (inst + "x!1") (("1" (rewrite "singleton") (("1" (prop) (("1" (use "nonempty_card[below(N)]") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (expand "filter") (("1" (inst?) (("1" (assert) (("1" (expand "singleton") (("1" (typepred! "leq") (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "reflexive?") (("1" (flatten) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (swap-rel 1) (("2" (rewrite "card_subset") (("2" (hide 2) (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) (("2" (expand "filter") (("2" (assert) (("2" (expand "singleton") (("2" (expand "geq") (("2" (replace -1) (("2" (typepred! "leq") (("2" (expand "total_order?") (("2" (expand "partial_order?") (("2" (expand "preorder?") (("2" (expand "reflexive?") (("2" (flatten) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (use "nonempty_card[below(N)]") (("2" (assert) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp*) (("2" (inst - "remove(x!1,eligible!1)" "f!1") (("2" (rewrite "card_remove") (("2" (assert) (("2" (skosimp*) (("2" (case "leq(f!1(x!1), f!1(i!1))") (("1" (inst + "x!1") (("1" (rewrite "index_value" +) (("1" (prop) (("1" (use "nonempty_card[below(N)]") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "x!1") (("1" (rewrite "filter") (("1" (typepred! "leq") (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "reflexive?") (("1" (flatten) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (swap-rel +) (("2" (rewrite "card_subset") (("2" (expand "subset?") (("2" (skosimp*) (("2" (expand "member") (("2" (rewrite "filter") (("2" (assert) (("2" (lemma "index_min") (("2" (inst - "remove(x!1,eligible!1)" "f!1" "i!1" "x!2") (("2" (assert) (("2" (rewrite "remove") (("2" (expand "member") (("2" (expand "geq") (("2" (typepred! "leq") (("2" (case "x!1 /= x!2") (("1" (assert) (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "transitive?") (("1" (flatten) (("1" (inst -2 "f!1(x!1)" "f!1(i!1)" "f!1(x!2)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (prop) (("1" (replace -2) (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "reflexive?") (("1" (flatten) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (expand "total_order?") (("2" (expand "partial_order?") (("2" (expand "preorder?") (("2" (expand "reflexive?") (("2" (flatten) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "i!1") (("2" (rewrite "index_value" +) (("2" (prop) (("1" (rewrite "index_value") (("1" (flatten) (("1" (rewrite "remove") (("1" (expand "member") (("1" (flatten) nil nil)) nil)) nil)) nil)) nil) ("2" (use "nonempty_card[below(N)]") (("2" (assert) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "i!1") (("2" (expand "filter") (("2" (expand "index_value") (("2" (flatten) (("2" (expand "remove") (("2" (expand "member") (("2" (flatten) (("2" (split 1) (("1" (propax) nil nil) ("2" (typepred! "leq") (("2" (expand "total_order?") (("2" (expand "partial_order?") (("2" (expand "preorder?") (("2" (expand "reflexive?") (("2" (flatten) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (swap-rel 1) (("3" (rewrite "card_subset") (("3" (expand "subset?") (("3" (expand "member") (("3" (skosimp*) (("3" (rewrite "filter") (("3" (expand "geq") (("3" (assert) (("3" (use "index_min") (("3" (assert) (("3" (rewrite "remove") (("3" (rewrite "member") (("3" (prop) (("3" (replace -1) (("3" (typepred! "leq") (("3" (expand "total_order?") (("3" (expand "dichotomous?") (("3" (flatten) (("3" (inst?) (("3" (split -2) (("1" (propax) nil nil) ("2" (propax) 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) ("3" (skosimp*) (("3" (expand "index_value") (("3" (rewrite "filter") (("3" (grind) nil nil)) nil)) nil)) nil)) nil) proved ((card_remove formula-decl nil finite_sets nil) (dichotomous? const-decl "bool" orders nil) (index_min formula-decl nil index_select nil) (transitive? const-decl "bool" relations nil) (/= const-decl "boolean" notequal nil) (remove const-decl "set" sets nil) (singleton const-decl "(singleton?)" sets nil) (geq const-decl "bool" index_select nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (subset? const-decl "bool" sets nil) (card_subset formula-decl nil finite_sets nil) (nonempty_card formula-decl nil finite_sets nil) (filter const-decl "bool" index_filters nil) (total_order? const-decl "bool" orders nil) (leq formal-const-decl "(total_order?[T])" index_select nil) (singleton? const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (preorder? const-decl "bool" orders nil) (reflexive? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (card_one formula-decl nil finite_sets nil) (subrange_induction formula-decl nil subrange_inductions 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) (N formal-const-decl "posnat" index_select nil) (index_value const-decl "bool" index_select 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (T formal-type-decl nil index_select 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (subrange type-eq-decl nil integers nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil)) 4184 3240 t nil) (least_index_exists-5 nil 3276341220 3276345265 ("" (induct "n") (("1" (skosimp*) (("1" (rewrite "card_one") (("1" (skosimp*) (("1" (replace -1) (("1" (expand "index_value") (("1" (inst + "x!1") (("1" (rewrite "singleton") (("1" (prop) (("1" (use "nonempty_card[below(N)]") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (expand "filter") (("1" (inst?) (("1" (assert) (("1" (expand "singleton") (("1" (typepred! "leq") (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "reflexive?") (("1" (flatten) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (swap-rel 1) (("2" (rewrite "card_subset") (("2" (hide 2) (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) (("2" (expand "filter") (("2" (assert) (("2" (expand "singleton") (("2" (expand "geq") (("2" (replace -1) (("2" (typepred! "leq") (("2" (expand "total_order?") (("2" (expand "partial_order?") (("2" (expand "preorder?") (("2" (expand "reflexive?") (("2" (flatten) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (use "nonempty_card[below(N)]") (("2" (assert) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp*) (("2" (inst - "remove(x!1,eligible!1)" "f!1") (("2" (rewrite "card_remove") (("2" (assert) (("2" (skosimp*) (("2" (case "leq(f!1(x!1), f!1(n1!1))") (("1" (inst + "x!1") (("1" (rewrite "index_value" +) (("1" (prop) (("1" (use "nonempty_card[below(N)]") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "x!1") (("1" (rewrite "filter") (("1" (typepred! "leq") (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "reflexive?") (("1" (flatten) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (swap-rel +) (("2" (rewrite "card_subset") (("2" (expand "subset?") (("2" (skosimp*) (("2" (expand "member") (("2" (rewrite "filter") (("2" (assert) (("2" (lemma "index_min") (("2" (inst - "remove(x!1,eligible!1)" "f!1" "n1!1" "x!2") (("2" (assert) (("2" (rewrite "remove") (("2" (expand "member") (("2" (expand "geq") (("2" (typepred! "leq") (("2" (case "x!1 /= x!2") (("1" (assert) (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "transitive?") (("1" (flatten) (("1" (inst -2 "f!1(x!1)" "f!1(n1!1)" "f!1(x!2)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (prop) (("1" (replace -2) (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "reflexive?") (("1" (flatten) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (expand "total_order?") (("2" (expand "partial_order?") (("2" (expand "preorder?") (("2" (expand "reflexive?") (("2" (flatten) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "n1!1") (("2" (rewrite "index_value" +) (("2" (prop) (("1" (rewrite "index_value") (("1" (flatten) (("1" (rewrite "remove") (("1" (expand "member") (("1" (flatten) nil nil)) nil)) nil)) nil)) nil) ("2" (use "nonempty_card[below(N)]") (("2" (assert) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "n1!1") (("2" (expand "filter") (("2" (expand "index_value") (("2" (flatten) (("2" (expand "remove") (("2" (expand "member") (("2" (flatten) (("2" (split 1) (("1" (propax) nil nil) ("2" (typepred! "leq") (("2" (expand "total_order?") (("2" (expand "partial_order?") (("2" (expand "preorder?") (("2" (expand "reflexive?") (("2" (flatten) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (swap-rel 1) (("3" (rewrite "card_subset") (("3" (expand "subset?") (("3" (expand "member") (("3" (skosimp*) (("3" (rewrite "filter") (("3" (expand "geq") (("3" (assert) (("3" (use "index_min") (("3" (assert) (("3" (rewrite "remove") (("3" (rewrite "member") (("3" (prop) (("3" (replace -1) (("3" (typepred! "leq") (("3" (expand "total_order?") (("3" (expand "dichotomous?") (("3" (flatten) (("3" (inst?) (("3" (split -2) (("1" (propax) nil nil) ("2" (propax) 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) ("3" (skosimp*) (("3" (expand "index_value") (("3" (rewrite "filter") (("3" (grind) nil nil)) nil)) nil)) nil)) nil) unfinished ((AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (subrange type-eq-decl nil integers nil) (pred type-eq-decl nil defined_types nil) (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) (T formal-type-decl nil index_select nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans 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) (index_value const-decl "bool" index_select nil) (N formal-const-decl "posnat" index_select 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) (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) (subrange_induction formula-decl nil subrange_inductions nil) (card_one formula-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (partial_order? const-decl "bool" orders nil) (reflexive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (member const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil) (singleton? const-decl "bool" sets nil) (leq formal-const-decl "(total_order?[T])" index_select nil) (total_order? const-decl "bool" orders nil) (filter const-decl "bool" index_filters nil) (nonempty_card formula-decl nil finite_sets nil) (card_subset formula-decl nil finite_sets nil) (subset? const-decl "bool" sets nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (geq const-decl "bool" index_select nil) (singleton const-decl "(singleton?)" sets nil) (remove const-decl "set" sets nil) (/= const-decl "boolean" notequal nil) (transitive? const-decl "bool" relations nil) (index_min formula-decl nil index_select nil) (dichotomous? const-decl "bool" orders nil) (card_remove formula-decl nil finite_sets nil)) 4418 840 nil nil) (least_index_exists-4 nil 3276341161 3276341185 ("" (induct "n") (("1" (skosimp*) (("1" (rewrite "card_one") (("1" (skosimp*) (("1" (replace -1) (("1" (expand "index_value") (("1" (inst + "x!1") (("1" (rewrite "singleton") (("1" (prop) (("1" (use "nonempty_card[below(N)]") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (expand "filter") (("1" (inst?) (("1" (assert) (("1" (expand "singleton") (("1" (typepred! "leq") (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "reflexive?") (("1" (flatten) (("1" (inst?) nil))))))))))))))))))))))))))))))) ("2" (swap-rel 1) (("2" (rewrite "card_subset") (("2" (hide 2) (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) (("2" (expand "filter") (("2" (assert) (("2" (expand "singleton") (("2" (expand "geq") (("2" (replace -1) (("2" (typepred! "leq") (("2" (expand "total_order?") (("2" (expand "partial_order?") (("2" (expand "preorder?") (("2" (expand "reflexive?") (("2" (flatten) (("2" (inst?) nil))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (skosimp*) (("2" (use "nonempty_card[below(N)]") (("2" (assert) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp*) (("2" (inst - "remove(x!1,eligible!1)" "f!1") (("2" (rewrite "card_remove") (("2" (assert) (("2" (skosimp*) (("2" (case "leq(f!1(x!1), f!1(n1!1))") (("1" (inst + "x!1") (("1" (rewrite "index_value" +) (("1" (prop) (("1" (use "nonempty_card[below(N)]") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "x!1") (("1" (rewrite "filter") (("1" (typepred! "leq") (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "reflexive?") (("1" (flatten) (("1" (inst?) nil))))))))))))))))))))))))))) ("2" (swap-rel +) (("2" (rewrite "card_subset") (("2" (expand "subset?") (("2" (skosimp*) (("2" (expand "member") (("2" (rewrite "filter") (("2" (assert) (("2" (lemma "index_min") (("2" (inst - "remove(x!1,eligible!1)" "f!1" "n1!1" "x!2") (("2" (assert) (("2" (rewrite "remove") (("2" (expand "member") (("2" (expand "geq") (("2" (typepred! "leq") (("2" (case "x!1 /= x!2") (("1" (assert) (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "transitive?") (("1" (flatten) (("1" (inst -2 "f!1(x!1)" "f!1(i!1)" "f!1(x!2)") (("1" (assert) nil))))))))))))))) ("2" (prop) (("1" (replace -2) (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "reflexive?") (("1" (flatten) (("1" (inst?) nil))))))))))))) ("2" (replace -1) (("2" (expand "total_order?") (("2" (expand "partial_order?") (("2" (expand "preorder?") (("2" (expand "reflexive?") (("2" (flatten) (("2" (inst?) nil))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (inst + "n1!1") (("2" (rewrite "index_value" +) (("2" (prop) (("1" (rewrite "index_value") (("1" (flatten) (("1" (rewrite "remove") (("1" (expand "member") (("1" (flatten) nil))))))))) ("2" (use "nonempty_card[below(N)]") (("2" (assert) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "n1!1") (("2" (expand "filter") (("2" (expand "index_value") (("2" (flatten) (("2" (expand "remove") (("2" (expand "member") (("2" (flatten) (("2" (split 1) (("1" (propax) nil) ("2" (typepred! "leq") (("2" (expand "total_order?") (("2" (expand "partial_order?") (("2" (expand "preorder?") (("2" (expand "reflexive?") (("2" (flatten) (("2" (inst?) nil))))))))))))))))))))))))))))))))))))))) ("3" (swap-rel 1) (("3" (rewrite "card_subset") (("3" (expand "subset?") (("3" (expand "member") (("3" (skosimp*) (("3" (rewrite "filter") (("3" (expand "geq") (("3" (assert) (("3" (use "index_min") (("3" (assert) (("3" (rewrite "remove") (("3" (rewrite "member") (("3" (prop) (("3" (replace -1) (("3" (typepred! "leq") (("3" (expand "total_order?") (("3" (expand "dichotomous?") (("3" (flatten) (("3" (inst?) (("3" (split -2) (("1" (propax) nil) ("2" (propax) nil))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ("3" (skosimp*) (("3" (expand "index_value") (("3" (rewrite "filter") (("3" (grind) nil)))))))) nil) unfinished nil 20779 2690 t nil) (least_index_exists-3 nil 3276341130 3276341145 ("" (induct "n") (("1" (skosimp*) (("1" (rewrite "card_one") (("1" (skosimp*) (("1" (replace -1) (("1" (expand "index_value") (("1" (inst + "x!1") (("1" (rewrite "singleton") (("1" (prop) (("1" (use "nonempty_card[below(N)]") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (expand "filter") (("1" (inst?) (("1" (assert) (("1" (expand "singleton") (("1" (typepred! "leq") (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "reflexive?") (("1" (flatten) (("1" (inst?) nil))))))))))))))))))))))))))))))) ("2" (swap-rel 1) (("2" (rewrite "card_subset") (("2" (hide 2) (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) (("2" (expand "filter") (("2" (assert) (("2" (expand "singleton") (("2" (expand "geq") (("2" (replace -1) (("2" (typepred! "leq") (("2" (expand "total_order?") (("2" (expand "partial_order?") (("2" (expand "preorder?") (("2" (expand "reflexive?") (("2" (flatten) (("2" (inst?) nil))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (skosimp*) (("2" (use "nonempty_card[below(M)]") (("2" (assert) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp*) (("2" (inst - "remove(x!1,eligible!1)" "f!1") (("2" (rewrite "card_remove") (("2" (assert) (("2" (skosimp*) (("2" (case "leq(f!1(x!1), f!1(n1!1))") (("1" (inst + "x!1") (("1" (rewrite "index_value" +) (("1" (prop) (("1" (use "nonempty_card[below(N)]") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "x!1") (("1" (rewrite "filter") (("1" (typepred! "leq") (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "reflexive?") (("1" (flatten) (("1" (inst?) nil))))))))))))))))))))))))))) ("2" (swap-rel +) (("2" (rewrite "card_subset") (("2" (expand "subset?") (("2" (skosimp*) (("2" (expand "member") (("2" (rewrite "filter") (("2" (assert) (("2" (lemma "index_min") (("2" (inst - "remove(x!1,eligible!1)" "f!1" "n1!1" "x!2") (("2" (assert) (("2" (rewrite "remove") (("2" (expand "member") (("2" (expand "geq") (("2" (typepred! "leq") (("2" (case "x!1 /= x!2") (("1" (assert) (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "transitive?") (("1" (flatten) (("1" (inst -2 "f!1(x!1)" "f!1(i!1)" "f!1(x!2)") (("1" (assert) nil))))))))))))))) ("2" (prop) (("1" (replace -2) (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "reflexive?") (("1" (flatten) (("1" (inst?) nil))))))))))))) ("2" (replace -1) (("2" (expand "total_order?") (("2" (expand "partial_order?") (("2" (expand "preorder?") (("2" (expand "reflexive?") (("2" (flatten) (("2" (inst?) nil))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (inst + "n1!1") (("2" (rewrite "index_value" +) (("2" (prop) (("1" (rewrite "index_value") (("1" (flatten) (("1" (rewrite "remove") (("1" (expand "member") (("1" (flatten) nil))))))))) ("2" (use "nonempty_card[below(N)]") (("2" (assert) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "n1!1") (("2" (expand "filter") (("2" (expand "index_value") (("2" (flatten) (("2" (expand "remove") (("2" (expand "member") (("2" (flatten) (("2" (split 1) (("1" (propax) nil) ("2" (typepred! "leq") (("2" (expand "total_order?") (("2" (expand "partial_order?") (("2" (expand "preorder?") (("2" (expand "reflexive?") (("2" (flatten) (("2" (inst?) nil))))))))))))))))))))))))))))))))))))))) ("3" (swap-rel 1) (("3" (rewrite "card_subset") (("3" (expand "subset?") (("3" (expand "member") (("3" (skosimp*) (("3" (rewrite "filter") (("3" (expand "geq") (("3" (assert) (("3" (use "index_min") (("3" (assert) (("3" (rewrite "remove") (("3" (rewrite "member") (("3" (prop) (("3" (replace -1) (("3" (typepred! "leq") (("3" (expand "total_order?") (("3" (expand "dichotomous?") (("3" (flatten) (("3" (inst?) (("3" (split -2) (("1" (propax) nil) ("2" (propax) nil))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ("3" (skosimp*) (("3" (expand "index_value") (("3" (rewrite "filter") (("3" (grind) nil)))))))) nil) unfinished nil 14241 870 t nil) (least_index_exists-2 nil 3275837439 3276339187 ("" (induct "n") (("1" (skosimp*) (("1" (rewrite "card_one") (("1" (skosimp*) (("1" (replace -1) (("1" (expand "index_value") (("1" (inst + "x!1") (("1" (rewrite "singleton") (("1" (prop) (("1" (use "nonempty_card[below(M)]") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (expand "filter") (("1" (inst?) (("1" (assert) (("1" (expand "singleton") (("1" (typepred! "leq") (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "reflexive?") (("1" (flatten) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (swap-rel 1) (("2" (rewrite "card_subset") (("2" (hide 2) (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) (("2" (expand "filter") (("2" (assert) (("2" (expand "singleton") (("2" (expand "geq") (("2" (replace -1) (("2" (typepred! "leq") (("2" (expand "total_order?") (("2" (expand "partial_order?") (("2" (expand "preorder?") (("2" (expand "reflexive?") (("2" (flatten) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (use "nonempty_card[below(M)]") (("2" (assert) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp*) (("2" (inst - "remove(x!1,eligible!1)" "f!1") (("2" (rewrite "card_remove") (("2" (assert) (("2" (skosimp*) (("2" (case "leq(f!1(x!1), f!1(i!1))") (("1" (inst + "x!1") (("1" (rewrite "index_value" +) (("1" (prop) (("1" (use "nonempty_card[below(M)]") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "x!1") (("1" (rewrite "filter") (("1" (typepred! "leq") (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "reflexive?") (("1" (flatten) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (swap-rel +) (("2" (rewrite "card_subset") (("2" (expand "subset?") (("2" (skosimp*) (("2" (expand "member") (("2" (rewrite "filter") (("2" (assert) (("2" (lemma "index_min") (("2" (inst - "remove(x!1,eligible!1)" "f!1" "i!1" "x!2") (("2" (assert) (("2" (rewrite "remove") (("2" (expand "member") (("2" (expand "geq") (("2" (typepred! "leq") (("2" (case "x!1 /= x!2") (("1" (assert) (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "transitive?") (("1" (flatten) (("1" (inst -2 "f!1(x!1)" "f!1(i!1)" "f!1(x!2)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (prop) (("1" (replace -2) (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "reflexive?") (("1" (flatten) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (expand "total_order?") (("2" (expand "partial_order?") (("2" (expand "preorder?") (("2" (expand "reflexive?") (("2" (flatten) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "i!1") (("2" (rewrite "index_value" +) (("2" (prop) (("1" (rewrite "index_value") (("1" (flatten) (("1" (rewrite "remove") (("1" (expand "member") (("1" (flatten) nil nil)) nil)) nil)) nil)) nil) ("2" (use "nonempty_card[below(M)]") (("2" (assert) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "i!1") (("2" (expand "filter") (("2" (expand "index_value") (("2" (flatten) (("2" (expand "remove") (("2" (expand "member") (("2" (flatten) (("2" (split 1) (("1" (propax) nil nil) ("2" (typepred! "leq") (("2" (expand "total_order?") (("2" (expand "partial_order?") (("2" (expand "preorder?") (("2" (expand "reflexive?") (("2" (flatten) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (swap-rel 1) (("3" (rewrite "card_subset") (("3" (expand "subset?") (("3" (expand "member") (("3" (skosimp*) (("3" (rewrite "filter") (("3" (expand "geq") (("3" (assert) (("3" (use "index_min") (("3" (assert) (("3" (rewrite "remove") (("3" (rewrite "member") (("3" (prop) (("3" (replace -1) (("3" (typepred! "leq") (("3" (expand "total_order?") (("3" (expand "dichotomous?") (("3" (flatten) (("3" (inst?) (("3" (split -2) (("1" (propax) nil nil) ("2" (propax) 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) ("3" (skosimp*) (("3" (expand "index_value") (("3" (rewrite "filter") (("3" (grind) nil nil)) nil)) nil)) nil)) nil) unfinished ((card_remove formula-decl nil finite_sets nil) (dichotomous? const-decl "bool" orders nil) (index_min formula-decl nil index_select nil) (transitive? const-decl "bool" relations nil) (/= const-decl "boolean" notequal nil) (remove const-decl "set" sets nil) (singleton const-decl "(singleton?)" sets nil) (geq const-decl "bool" index_select nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (subset? const-decl "bool" sets nil) (card_subset formula-decl nil finite_sets nil) (nonempty_card formula-decl nil finite_sets nil) (filter const-decl "bool" index_filters nil) (total_order? const-decl "bool" orders nil) (leq formal-const-decl "(total_order?[T])" index_select nil) (singleton? const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (preorder? const-decl "bool" orders nil) (reflexive? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (card_one formula-decl nil finite_sets nil) (subrange_induction formula-decl nil subrange_inductions 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) (index_value const-decl "bool" index_select 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (T formal-type-decl nil index_select 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (subrange type-eq-decl nil integers nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil)) 266 200 t nil) (least_index_exists-1 nil 3264854096 3275837308 ("" (induct "n") (("1" (skosimp*) (("1" (rewrite "card_one") (("1" (skosimp*) (("1" (replace -1) (("1" (expand "index_value") (("1" (inst + "x!1") (("1" (rewrite "singleton") (("1" (prop) (("1" (use "nonempty_card[below(M)]") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (expand "filter") (("1" (inst?) (("1" (assert) (("1" (expand "singleton") (("1" (typepred! "<=") (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "reflexive?") (("1" (flatten) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (swap-rel 1) (("2" (rewrite "card_subset") (("2" (hide 2) (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) (("2" (expand "filter") (("2" (assert) (("2" (expand "singleton") (("2" (expand ">=") (("2" (replace -1) (("2" (typepred! "<=") (("2" (expand "total_order?") (("2" (expand "partial_order?") (("2" (expand "preorder?") (("2" (expand "reflexive?") (("2" (flatten) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (use "nonempty_card[below(M)]") (("2" (assert) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (skosimp*) (("2" (inst - "remove(x!1,eligible!1)" "f!1") (("2" (rewrite "card_remove") (("2" (assert) (("2" (skosimp*) (("2" (case "f!1(x!1) <= f!1(i!1)") (("1" (inst + "x!1") (("1" (rewrite "index_value" +) (("1" (prop) (("1" (use "nonempty_card[below(M)]") (("1" (assert) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "x!1") (("1" (rewrite "filter") (("1" (typepred! "<=") (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "reflexive?") (("1" (flatten) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (swap-rel +) (("2" (rewrite "card_subset") (("2" (expand "subset?") (("2" (skosimp*) (("2" (expand "member") (("2" (rewrite "filter") (("2" (assert) (("2" (lemma "index_min") (("2" (inst - "remove(x!1,eligible!1)" "f!1" "i!1" "x!2") (("2" (assert) (("2" (rewrite "remove") (("2" (expand "member") (("2" (expand ">=") (("2" (typepred! "<=") (("2" (case "x!1 /= x!2") (("1" (assert) (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "transitive?") (("1" (flatten) (("1" (inst -2 "f!1(x!1)" "f!1(i!1)" "f!1(x!2)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (prop) (("1" (replace -2) (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "reflexive?") (("1" (flatten) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (expand "total_order?") (("2" (expand "partial_order?") (("2" (expand "preorder?") (("2" (expand "reflexive?") (("2" (flatten) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "i!1") (("2" (rewrite "index_value" +) (("2" (prop) (("1" (rewrite "index_value") (("1" (flatten) (("1" (rewrite "remove") (("1" (expand "member") (("1" (flatten) nil nil)) nil)) nil)) nil)) nil) ("2" (use "nonempty_card[below(M)]") (("2" (assert) (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (expand "member") (("2" (inst - "i!1") (("2" (expand "filter") (("2" (expand "index_value") (("2" (flatten) (("2" (expand "remove") (("2" (expand "member") (("2" (flatten) (("2" (split 1) (("1" (propax) nil nil) ("2" (typepred! "<=") (("2" (expand "total_order?") (("2" (expand "partial_order?") (("2" (expand "preorder?") (("2" (expand "reflexive?") (("2" (flatten) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (swap-rel 1) (("3" (rewrite "card_subset") (("3" (expand "subset?") (("3" (expand "member") (("3" (skosimp*) (("3" (rewrite "filter") (("3" (assert) (("3" (swap-rel 1) (("1" (use "index_min") (("1" (assert) (("1" (rewrite "remove") (("1" (rewrite "member") (("1" (prop) (("1" (replace -1) (("1" (typepred! "<=") (("1" (expand "total_order?") (("1" (expand "dichotomous?") (("1" (flatten) (("1" (inst?) (("1" (split -2) (("1" (propax) nil nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand ">=") (("2" (propax) 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) ("3" (skosimp*) (("3" (expand "index_value") (("3" (rewrite "filter") (("3" (grind) nil nil)) nil)) nil)) nil)) nil) unfinished ((card_remove formula-decl nil finite_sets nil) (dichotomous? const-decl "bool" orders nil) (index_min formula-decl nil index_select nil) (transitive? const-decl "bool" relations nil) (/= const-decl "boolean" notequal nil) (remove const-decl "set" sets nil) (singleton const-decl "(singleton?)" sets nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (subset? const-decl "bool" sets nil) (card_subset formula-decl nil finite_sets nil) (nonempty_card formula-decl nil finite_sets nil) (filter const-decl "bool" index_filters nil) (total_order? const-decl "bool" orders nil) (singleton? const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (preorder? const-decl "bool" orders nil) (reflexive? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (card_one formula-decl nil finite_sets nil) (subrange_induction formula-decl nil subrange_inductions 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) (index_value const-decl "bool" index_select 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (T formal-type-decl nil index_select 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (subrange type-eq-decl nil integers nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil)) 376 320 t shostak)) (index_exists_induct 0 (index_exists_induct-6 nil 3276346167 3276349881 ("" (induct "n") (("1" (skosimp*) (("1" (use "least_index_exists") (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (use "least_index_exists") (("1" (assert) (("1" (skosimp*) (("1" (inst - "remove(i!1, eligible!1)" "f!1" "k!2-1") (("1" (rewrite "card_remove") (("1" (assert) (("1" (lift-if) (("1" (assert) (("1" (prop) (("1" (skosimp*) (("1" (inst + "i!2") (("1" (lemma "index_min") (("1" (inst?) (("1" (inst - "i!2") (("1" (assert) (("1" (hide -4) (("1" (expand "index_value") (("1" (flatten) (("1" (rewrite "remove") (("1" (expand "member") (("1" (flatten) (("1" (assert) (("1" (rewrite "filter_remove") (("1" (rewrite "card_remove") (("1" (rewrite "filter") (("1" (assert) (("1" (rewrite "card_remove") (("1" (assert) (("1" (hide -4) (("1" (invoke (then (case "%1 <= %2") (assert)) (! -4 l) (! 2 l)) (("1" (rewrite "card_subset") (("1" (expand "subset?") (("1" (expand "member") (("1" (skosimp*) (("1" (rewrite "filter") (("1" (rewrite "filter") (("1" (rewrite "remove") (("1" (expand "member") (("1" (prop) 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" (rewrite "index_value") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("3" (assert) nil nil)) nil) proved ((- const-decl "[numfield, numfield -> numfield]" number_fields nil) (remove const-decl "set" sets nil) (index_min formula-decl nil index_select nil) (member const-decl "bool" sets nil) (filter const-decl "bool" index_filters nil) (geq const-decl "bool" index_select nil) (subset? const-decl "bool" sets nil) (card_subset formula-decl nil finite_sets nil) (filter_remove formula-decl nil index_filters nil) (total_order? const-decl "bool" orders nil) (leq formal-const-decl "(total_order?[T])" index_select nil) (card_remove formula-decl nil finite_sets nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (k!1 skolem-const-decl "subrange(1, N)" index_select nil) (least_index_exists formula-decl nil index_select nil) (subrange_induction formula-decl nil subrange_inductions 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) (N formal-const-decl "posnat" index_select nil) (index_value const-decl "bool" index_select 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (T formal-type-decl nil index_select 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (subrange type-eq-decl nil integers nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil)) 2776 2200 t nil) (index_exists_induct-5 nil 3276345378 3276346054 ("" (induct "n") (("1" (skosimp*) (("1" (use "least_index_exists") (("1" (assert) nil))))) ("2" (skosimp*) (("2" (use "least_index_exists") (("1" (assert) (("1" (skosimp*) (("1" (inst - "remove(i!1, eligible!1)" "f!1" "k!1-1") (("1" (rewrite "card_remove") (("1" (assert) (("1" (lift-if) (("1" (assert) (("1" (prop) (("1" (skosimp*) (("1" (inst + "i!2") (("1" (lemma "index_min") (("1" (inst?) (("1" (inst - "i!2") (("1" (assert) (("1" (hide -4) (("1" (expand "index_value") (("1" (flatten) (("1" (rewrite "remove") (("1" (expand "member") (("1" (flatten) (("1" (assert) (("1" (rewrite "filter_remove") (("1" (rewrite "card_remove") (("1" (rewrite "filter") (("1" (assert) (("1" (rewrite "card_remove") (("1" (assert) (("1" (hide -4) (("1" (invoke (then (case "%1 <= %2") (assert)) (! -4 l) (! 2 l)) (("1" (rewrite "card_subset") (("1" (expand "subset?") (("1" (expand "member") (("1" (skosimp*) (("1" (rewrite "filter") (("1" (rewrite "filter") (("1" (rewrite "remove") (("1" (expand "member") (("1" (prop) nil))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (rewrite "index_value") (("2" (flatten) nil))))))))))))))))))) ("2" (assert) nil))))) ("3" (assert) nil)) nil) unfinished nil 638124 26090 t nil) (index_exists_induct-4 nil 3276339961 3276345266 ("" (induct "n") (("1" (skosimp*) (("1" (use "least_index_exists") (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (use "least_index_exists") (("1" (assert) (("1" (skosimp*) (("1" (inst - "remove(n1!1, eligible!1)" "f!1" "n3!1-1") (("1" (rewrite "card_remove") (("1" (assert) (("1" (lift-if) (("1" (assert) (("1" (prop) (("1" (skosimp*) (("1" (inst + "n1!2") (("1" (lemma "index_min") (("1" (inst?) (("1" (inst - "n1!2") (("1" (assert) (("1" (hide -4) (("1" (expand "index_value") (("1" (flatten) (("1" (rewrite "remove") (("1" (expand "member") (("1" (flatten) (("1" (assert) (("1" (rewrite "filter_remove") (("1" (rewrite "card_remove") (("1" (rewrite "filter") (("1" (assert) (("1" (rewrite "card_remove") (("1" (assert) (("1" (hide -4) (("1" (invoke (then (case "%1 <= %2") (assert)) (! -4 l) (! 2 l)) (("1" (rewrite "card_subset") (("1" (expand "subset?") (("1" (expand "member") (("1" (skosimp*) (("1" (rewrite "filter") (("1" (rewrite "filter") (("1" (rewrite "remove") (("1" (expand "member") (("1" (prop) 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" (rewrite "index_value") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("3" (assert) nil nil)) nil) unfinished ((- const-decl "[numfield, numfield -> numfield]" number_fields nil) (remove const-decl "set" sets nil) (index_min formula-decl nil index_select nil) (member const-decl "bool" sets nil) (filter const-decl "bool" index_filters nil) (geq const-decl "bool" index_select nil) (subset? const-decl "bool" sets nil) (card_subset formula-decl nil finite_sets nil) (filter_remove formula-decl nil index_filters nil) (total_order? const-decl "bool" orders nil) (leq formal-const-decl "(total_order?[T])" index_select nil) (card_remove formula-decl nil finite_sets nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (least_index_exists formula-decl nil index_select nil) (subrange_induction formula-decl nil subrange_inductions 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) (N formal-const-decl "posnat" index_select nil) (index_value const-decl "bool" index_select 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (T formal-type-decl nil index_select 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (subrange type-eq-decl nil integers nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil)) 934 800 t nil) (index_exists_induct-3 nil 3276339416 3276339844 ("" (induct "n") (("1" (skosimp*) (("1" (use "least_index_exists") (("1" (assert) nil))))) ("2" (skosimp*) (("2" (use "least_index_exists") (("1" (assert) (("1" (skosimp*) (("1" (inst - "remove(n1!1, eligible!1)" "f!1" "n2!2-1") (("1" (rewrite "card_remove") (("1" (assert) (("1" (lift-if) (("1" (assert) (("1" (prop) (("1" (skosimp*) (("1" (inst + "n1!2") (("1" (lemma "index_min") (("1" (inst?) (("1" (inst - "n1!2") (("1" (assert) (("1" (hide -4) (("1" (expand "index_value") (("1" (flatten) (("1" (rewrite "remove") (("1" (expand "member") (("1" (flatten) (("1" (assert) (("1" (rewrite "filter_remove") (("1" (rewrite "card_remove") (("1" (rewrite "filter") (("1" (assert) (("1" (rewrite "card_remove") (("1" (assert) (("1" (hide -4) (("1" (invoke (then (case "%1 <= %2") (assert)) (! -4 l) (! 2 l)) (("1" (rewrite "card_subset") (("1" (expand "subset?") (("1" (expand "member") (("1" (skosimp*) (("1" (rewrite "filter") (("1" (rewrite "filter") (("1" (rewrite "remove") (("1" (expand "member") (("1" (prop) nil))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (rewrite "index_value") (("2" (flatten) nil))))))))))))))))))) ("2" (assert) nil))))) ("3" (assert) nil)) nil) unfinished nil 417243 21650 t nil) (index_exists_induct-2 nil 3276339260 3276339272 ("" (induct "n") (("1" (skosimp*) (("1" (use "least_index_exists") (("1" (assert) nil))))) ("2" (skosimp*) (("2" (use "least_index_exists") (("1" (assert) (("1" (skosimp*) (("1" (inst - "remove(i!1, eligible!1)" "f!1" "n2!2-1") (("1" (rewrite "card_remove") (("1" (assert) (("1" (lift-if) (("1" (assert) (("1" (prop) (("1" (skosimp*) (("1" (inst + "n1!2") (("1" (lemma "index_min") (("1" (inst?) (("1" (inst - "n1!2") (("1" (assert) (("1" (hide -4) (("1" (expand "index_value") (("1" (flatten) (("1" (rewrite "remove") (("1" (expand "member") (("1" (flatten) (("1" (assert) (("1" (rewrite "filter_remove") (("1" (rewrite "card_remove") (("1" (rewrite "filter") (("1" (assert) (("1" (rewrite "card_remove") (("1" (assert) (("1" (hide -4) (("1" (invoke (then (case "%1 <= %2") (assert)) (! -4 l) (! 2 l)) (("1" (rewrite "card_subset") (("1" (expand "subset?") (("1" (expand "member") (("1" (skosimp*) (("1" (rewrite "filter") (("1" (rewrite "filter") (("1" (rewrite "remove") (("1" (expand "member") (("1" (prop) nil))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (rewrite "index_value") (("2" (flatten) nil))))))))))))))))))) ("2" (assert) nil))))) ("3" (assert) nil)) nil) unfinished nil 9251 1160 t nil) (index_exists_induct-1 nil 3265033464 3276339188 ("" (induct "n") (("1" (skosimp*) (("1" (use "least_index_exists") (("1" (assert) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (use "least_index_exists") (("1" (assert) (("1" (skosimp*) (("1" (inst - "remove(i!1, eligible!1)" "f!1" "k!2-1") (("1" (rewrite "card_remove") (("1" (assert) (("1" (lift-if) (("1" (assert) (("1" (prop) (("1" (skosimp*) (("1" (inst + "i!2") (("1" (lemma "index_min") (("1" (inst?) (("1" (inst - "i!2") (("1" (assert) (("1" (hide -4) (("1" (expand "index_value") (("1" (flatten) (("1" (rewrite "remove") (("1" (expand "member") (("1" (flatten) (("1" (assert) (("1" (rewrite "filter_remove") (("1" (rewrite "card_remove") (("1" (rewrite "filter") (("1" (assert) (("1" (rewrite "card_remove") (("1" (assert) (("1" (hide -4) (("1" (invoke (then (case "%1 <= %2") (assert)) (! -4 l) (! 2 l)) (("1" (rewrite "card_subset") (("1" (expand "subset?") (("1" (expand "member") (("1" (skosimp*) (("1" (rewrite "filter") (("1" (rewrite "filter") (("1" (rewrite "remove") (("1" (expand "member") (("1" (prop) 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" (rewrite "index_value") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("3" (assert) nil nil)) nil) unfinished ((- const-decl "[numfield, numfield -> numfield]" number_fields nil) (remove const-decl "set" sets nil) (index_min formula-decl nil index_select nil) (member const-decl "bool" sets nil) (filter const-decl "bool" index_filters nil) (geq const-decl "bool" index_select nil) (subset? const-decl "bool" sets nil) (card_subset formula-decl nil finite_sets nil) (filter_remove formula-decl nil index_filters nil) (total_order? const-decl "bool" orders nil) (leq formal-const-decl "(total_order?[T])" index_select nil) (card_remove formula-decl nil finite_sets nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (least_index_exists formula-decl nil index_select nil) (subrange_induction formula-decl nil subrange_inductions 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) (index_value const-decl "bool" index_select 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (T formal-type-decl nil index_select 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (pred type-eq-decl nil defined_types nil) (subrange type-eq-decl nil integers nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil)) 907 820 t nil)) (index_exists 0 (index_exists-1 nil 3265033521 3276349881 ("" (skosimp*) (("" (lemma "index_exists_induct") (("" (inst?) (("" (assert) (("" (assert) (("" (rewrite "card_below") nil nil)) nil)) nil)) nil)) nil)) nil) proved ((index_exists_induct formula-decl nil index_select nil) (card_below formula-decl nil finite_sets_below "finite_sets/") (T formal-type-decl nil index_select 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) (N formal-const-decl "posnat" index_select 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)) 251 210 t shostak)) (index_order 0 (index_order-4 nil 3276346205 3276349883 ("" (skosimp*) (("" (expand "index_value") (("" (flatten) (("" (hide -3 -7) (("" (lemma "pigeonhole[below(N)]") (("" (inst?) (("" (invoke (inst - "%1") (! -6 l 1)) (("" (assert) (("" (prop) (("1" (skosimp*) (("1" (rewrite "filter") (("1" (rewrite "filter") (("1" (flatten) (("1" (expand "geq" -2) (("1" (typepred! "leq") (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "transitive?") (("1" (flatten) (("1" (inst -2 "f!1(i!1)" "f!1(x!1)" "f!1(j!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (invoke (then (case "%1 <= %2") (assert)) (! 1 r) (! -3 r 1)) (("2" (hide-all-but 1) (("2" (rewrite "card_subset") (("2" (expand "subset?") (("2" (expand "union") (("2" (expand "filter") (("2" (expand "member") (("2" (skosimp*) (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((index_value const-decl "bool" index_select 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) (T formal-type-decl nil index_select nil) (filter const-decl "bool" index_filters nil) (geq const-decl "bool" index_select nil) (<= const-decl "bool" reals 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) (union const-decl "set" sets nil) (card_subset formula-decl nil finite_sets nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (preorder? const-decl "bool" orders nil) (transitive? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (leq formal-const-decl "(total_order?[T])" index_select nil) (pigeonhole 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) (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) (N formal-const-decl "posnat" index_select nil) (below type-eq-decl nil naturalnumbers nil)) 1502 1240 nil nil) (index_order-3 nil 3276338797 3276345267 ("" (skosimp*) (("" (expand "index_value") (("" (flatten) (("" (hide -3 -7) (("" (lemma "pigeonhole[below(N)]") (("" (inst?) (("" (invoke (inst - "%1") (! -6 l 1)) (("" (assert) (("" (prop) (("1" (skosimp*) (("1" (rewrite "filter") (("1" (rewrite "filter") (("1" (flatten) (("1" (expand "geq" -2) (("1" (typepred! "leq") (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "transitive?") (("1" (flatten) (("1" (inst -2 "f!1(n1!1)" "f!1(x!1)" "f!1(n2!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (invoke (then (case "%1 <= %2") (assert)) (! 1 r) (! -3 r 1)) (("2" (hide-all-but 1) (("2" (rewrite "card_subset") (("2" (expand "subset?") (("2" (expand "union") (("2" (expand "filter") (("2" (expand "member") (("2" (skosimp*) (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished ((index_value const-decl "bool" index_select 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) (T formal-type-decl nil index_select nil) (filter const-decl "bool" index_filters nil) (geq const-decl "bool" index_select nil) (<= const-decl "bool" reals 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) (union const-decl "set" sets nil) (card_subset formula-decl nil finite_sets nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (preorder? const-decl "bool" orders nil) (transitive? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (leq formal-const-decl "(total_order?[T])" index_select nil) (pigeonhole 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) (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) (N formal-const-decl "posnat" index_select nil) (below type-eq-decl nil naturalnumbers nil)) 839 730 nil nil) (index_order-2 nil 3275839130 3275840381 ("" (skosimp*) (("" (expand "index_value") (("" (flatten) (("" (hide -3 -7) (("" (lemma "pigeonhole[below(M)]") (("" (inst?) (("" (invoke (inst - "%1") (! -6 l 1)) (("" (assert) (("" (prop) (("1" (skosimp*) (("1" (rewrite "filter") (("1" (rewrite "filter") (("1" (flatten) (("1" (expand "geq" -2) (("1" (typepred! "leq") (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "transitive?") (("1" (flatten) (("1" (inst -2 "f!1(i1!1)" "f!1(x!1)" "f!1(i2!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (invoke (then (case "%1 <= %2") (assert)) (! 1 r) (! -3 r 1)) (("2" (hide-all-but 1) (("2" (rewrite "card_subset") (("2" (expand "subset?") (("2" (expand "union") (("2" (expand "filter") (("2" (expand "member") (("2" (skosimp*) (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((index_value const-decl "bool" index_select 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) (T formal-type-decl nil index_select nil) (filter const-decl "bool" index_filters nil) (geq const-decl "bool" index_select nil) (<= const-decl "bool" reals 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) (union const-decl "set" sets nil) (card_subset formula-decl nil finite_sets nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (preorder? const-decl "bool" orders nil) (transitive? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (leq formal-const-decl "(total_order?[T])" index_select nil) (pigeonhole 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) (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) (below type-eq-decl nil naturalnumbers nil)) 1235052 37960 t nil) (index_order-1 nil 3265095833 3275837310 ("" (skosimp*) (("" (expand "index_value") (("" (flatten) (("" (hide -3 -7) (("" (lemma "pigeonhole[below(M)]") (("" (inst?) (("" (invoke (inst - "%1") (! -6 l 1)) (("" (assert) (("" (prop) (("1" (skosimp*) (("1" (rewrite "filter") (("1" (rewrite "filter") (("1" (flatten) (("1" (expand ">=" -2) (("1" (typepred! "<=") (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "transitive?") (("1" (flatten) (("1" (inst -2 "f!1(i1!1)" "f!1(x!1)" "f!1(i2!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (invoke (then (case "%1 <= %2") (assert)) (! 1 r) (! -3 r 1)) (("2" (hide-all-but 1) (("2" (rewrite "card_subset") (("2" (expand "subset?") (("2" (expand "union") (("2" (expand "filter") (("2" (expand "member") (("2" (skosimp*) (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished ((index_value const-decl "bool" index_select 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) (T formal-type-decl nil index_select nil) (filter const-decl "bool" index_filters nil) (<= const-decl "bool" reals 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) (union const-decl "set" sets nil) (card_subset formula-decl nil finite_sets nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (preorder? const-decl "bool" orders nil) (transitive? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (pigeonhole 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) (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) (below type-eq-decl nil naturalnumbers nil)) 719 500 t shostak)) (index_value_overlap 0 (index_value_overlap-3 nil 3276339150 3276349884 ("" (expand "index_value") (("" (skosimp*) (("" (hide -3 -5) (("" (lemma "pigeonhole") (("" (invoke (inst - "%1" "%2") (! -3 l 1) (! -5 l 1)) (("" (prop) (("1" (skosimp*) (("1" (rewrite "filter") (("1" (rewrite "filter") (("1" (flatten) (("1" (inst?) (("1" (expand "geq") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -3 2) (("2" (invoke (then (case "%1 <= %2") (assert)) (! 1 r) (! -2 r 1)) (("2" (hide-all-but 1) (("2" (rewrite "card_subset") (("2" (hide 2) (("2" (auto-rewrite-defs) (("2" (assert) (("2" (skosimp*) (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((below type-eq-decl nil naturalnumbers nil) (N formal-const-decl "posnat" index_select 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) (pigeonhole formula-decl nil pigeonhole nil) (<= const-decl "bool" reals 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) (union const-decl "set" sets nil) (card_subset formula-decl nil finite_sets nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets 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) (T formal-type-decl nil index_select nil) (filter const-decl "bool" index_filters nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (leq formal-const-decl "(total_order?[T])" index_select nil) (geq const-decl "bool" index_select nil) (index_value const-decl "bool" index_select nil)) 1356 1160 nil nil) (index_value_overlap-2 nil 3275840404 3275840414 ("" (expand "index_value") (("" (skosimp*) (("" (hide -3 -5) (("" (lemma "pigeonhole") (("" (invoke (inst - "%1" "%2") (! -3 l 1) (! -5 l 1)) (("" (prop) (("1" (skosimp*) (("1" (rewrite "filter") (("1" (rewrite "filter") (("1" (flatten) (("1" (inst?) (("1" (expand "geq") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -3 2) (("2" (invoke (then (case "%1 <= %2") (assert)) (! 1 r) (! -2 r 1)) (("2" (hide-all-but 1) (("2" (rewrite "card_subset") (("2" (hide 2) (("2" (auto-rewrite-defs) (("2" (assert) (("2" (skosimp*) (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((index_value const-decl "bool" index_select nil) (geq const-decl "bool" index_select nil) (leq formal-const-decl "(total_order?[T])" index_select nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (filter const-decl "bool" index_filters nil) (T formal-type-decl nil index_select 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) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (card_subset formula-decl nil finite_sets nil) (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) (<= const-decl "bool" reals nil) (pigeonhole 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) (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) (below type-eq-decl nil naturalnumbers nil)) 8389 810 nil nil) (index_value_overlap-1 nil 3267461668 3275837311 ("" (expand "index_value") (("" (skosimp*) (("" (hide -3 -5) (("" (lemma "pigeonhole") (("" (invoke (inst - "%1" "%2") (! -3 l 1) (! -5 l 1)) (("" (prop) (("1" (skosimp*) (("1" (rewrite "filter") (("1" (rewrite "filter") (("1" (flatten) (("1" (inst?) (("1" (expand ">=") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -3 2) (("2" (invoke (then (case "%1 <= %2") (assert)) (! 1 r) (! -2 r 1)) (("2" (hide-all-but 1) (("2" (rewrite "card_subset") (("2" (hide 2) (("2" (auto-rewrite-defs) (("2" (assert) (("2" (skosimp*) (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished ((below type-eq-decl nil naturalnumbers 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) (pigeonhole formula-decl nil pigeonhole nil) (<= const-decl "bool" reals 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) (union const-decl "set" sets nil) (card_subset formula-decl nil finite_sets nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets 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) (T formal-type-decl nil index_select nil) (filter const-decl "bool" index_filters nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (index_value const-decl "bool" index_select nil)) 714 680 t nil))) $$$middle_value_index.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Design : SPIDER Version 2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% middle_value_index[N: posnat, T: TYPE, leq: (total_order?[T])]: THEORY BEGIN IMPORTING index_select[N, T, leq], good_vote_for[N, T] good, select: var finite_set[below(N)] f, f1, f2 : var [below(N) -> T] t: VAR T i, j: VAR below(N) rel: VAR [T,T -> bool] middle_value(select)(f)(i): bool = % returns true if f(i) is a middle value select(i) AND 2*card(filter(leq)(select)(f)(i)) > card(select) AND 2*card(filter(geq)(select)(f)(i)) >= card(select) eligible: var non_empty_finite_set[below(N)] middle_value_exists: LEMMA EXISTS i: middle_value(eligible)(f)(i) middle_index(eligible, f): below(N) = choose({i | middle_value(eligible)(f)(i)}) middle_index_value: LEMMA index_value(eligible, floor(card(eligible)/2),f)(middle_index(eligible, f)) middle_value(eligible, f): T = f(middle_index(eligible, f)) middle_good_bounded: LEMMA majority_subset?(good,select) AND 2*card(filter(rel)(select)(f)(i)) >= card(select) IMPLIES EXISTS j: good(j) AND rel(f(j),f(i)) middle_value_lower_validity: LEMMA majority_subset?(good, eligible) IMPLIES EXISTS i : good(i) AND leq(f(i), middle_value(eligible, f)) middle_value_upper_validity: LEMMA majority_subset?(good, eligible) IMPLIES EXISTS i : good(i) AND leq(middle_value(eligible, f), f(i)) middle_value_exact_validity: LEMMA majority_subset?(good, eligible) AND good_vote_for?(good, f, t) IMPLIES middle_value(eligible, f) = t middle_value_overlap: LEMMA EXISTS j: eligible(j) AND leq(f1(j), middle_value(eligible,f1)) AND leq(middle_value(eligible,f2), f2(j)) END middle_value_index $$$middle_value_index.prf (middle_value_index (middle_value_exists 0 (middle_value_exists-3 nil 3276346291 3276346299 ("" (skosimp*) (("" (lemma "index_exists") (("" (inst?) (("" (inst?) (("" (inst - "floor(card(eligible!1)/2)") (("1" (assert) (("1" (prop) (("1" (skosimp*) (("1" (inst + "i!1") (("1" (expand "index_value") (("1" (flatten) (("1" (expand "middle_value") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (use "nonempty_card[below(N)]") (("2" (assert) (("2" (expand "nonempty?") (("2" (typepred "eligible!1") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "card_below") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((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) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) 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) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (middle_value const-decl "bool" middle_value_index nil) (index_value const-decl "bool" index_select nil) (nonempty_card formula-decl nil finite_sets nil) (nonempty? const-decl "bool" sets nil) (card_below formula-decl nil finite_sets_below "finite_sets/") (index_exists formula-decl nil index_select 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) (N formal-const-decl "posnat" middle_value_index nil) (T formal-type-decl nil middle_value_index nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (leq formal-const-decl "(total_order?[T])" middle_value_index nil)) 7154 440 nil nil) (middle_value_exists-2 nil 3276341498 3276346271 ("" (skosimp*) (("" (lemma "index_exists") (("" (inst?) (("" (inst?) (("" (inst - "floor(card(eligible!1)/2)") (("1" (assert) (("1" (prop) (("1" (skosimp*) (("1" (inst + "n1!1") (("1" (expand "index_value") (("1" (flatten) (("1" (expand "middle_value") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (use "nonempty_card[below(N)]") (("2" (assert) (("2" (expand "nonempty?") (("2" (typepred "eligible!1") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "card_below") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished ((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) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_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) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (middle_value const-decl "bool" middle_value_index nil) (index_value const-decl "bool" index_select nil) (nonempty_card formula-decl nil finite_sets nil) (nonempty? const-decl "bool" sets nil) (card_below formula-decl nil finite_sets_below "finite_sets/") (index_exists formula-decl nil index_select 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) (N formal-const-decl "posnat" middle_value_index nil) (T formal-type-decl nil middle_value_index nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (leq formal-const-decl "(total_order?[T])" middle_value_index nil)) 546 470 nil nil) (middle_value_exists-1 nil 3265458918 3276341464 ("" (skosimp*) (("" (lemma "index_exists") (("" (inst?) (("" (inst?) (("" (inst - "floor(card(eligible!1)/2)") (("1" (assert) (("1" (prop) (("1" (skosimp*) (("1" (inst + "i!1") (("1" (expand "index_value") (("1" (flatten) (("1" (expand "middle_value") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (use "nonempty_card[below(N)]") (("2" (assert) (("2" (expand "nonempty?") (("2" (typepred "eligible!1") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "card_below") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished ((leq formal-const-decl "(total_order?[T])" middle_value_index nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (T formal-type-decl nil middle_value_index nil) (N formal-const-decl "posnat" middle_value_index 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) (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) (index_exists formula-decl nil index_select nil) (card_below formula-decl nil finite_sets_below "finite_sets/") (nonempty? const-decl "bool" sets nil) (nonempty_card formula-decl nil finite_sets nil) (index_value const-decl "bool" index_select nil) (middle_value const-decl "bool" middle_value_index nil) (integer nonempty-type-from-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (/= const-decl "boolean" notequal nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields 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) (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 "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) 497 460 t shostak)) (middle_index_TCC1 0 (middle_index_TCC1-1 nil 3265469831 3276277571 ("" (skosimp*) (("" (expand "nonempty?") (("" (expand "empty?") (("" (expand "member") (("" (use "middle_value_exists") (("" (skosimp*) (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) proved-complete ((nonempty? const-decl "bool" sets nil) (member const-decl "bool" 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) (N formal-const-decl "posnat" middle_value_index 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) (non_empty_finite_set type-eq-decl nil finite_sets nil) (T formal-type-decl nil middle_value_index nil) (middle_value_exists formula-decl nil middle_value_index nil) (empty? const-decl "bool" sets nil)) 128 100 t shostak)) (middle_index_value_TCC1 0 (middle_index_value_TCC1-1 nil 3267464088 3276277571 ("" (skosimp*) (("" (use "card_below") (("" (assert) nil nil)) nil)) nil) proved-complete ((card_below formula-decl nil finite_sets_below "finite_sets/") (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) (N formal-const-decl "posnat" middle_value_index 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 "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil)) 243 230 t shostak)) (middle_index_value 0 (middle_index_value-1 nil 3267463215 3276346273 ("" (skosimp*) (("" (expand "index_value") (("" (expand "middle_index") (("" (expand "choose") (("" (use "epsilon_ax[below(N)]") (("1" (split -1) (("1" (rewrite "middle_value") (("1" (flatten) (("1" (assert) (("1" (div-by (-2 -3) "2") (("1" (assert) (("1" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil) ("2" (inst + 0) nil nil) ("3" (inst + 0) nil nil) ("4" (inst + 0) nil nil) ("5" (inst + 0) nil nil)) nil)) nil)) nil) ("2" (inst + 0) nil nil)) nil) ("2" (use "middle_value_exists") nil nil)) nil) ("2" (assert) (("2" (inst + 0) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((index_value const-decl "bool" index_select nil) (choose const-decl "(p)" sets nil) (both_sides_div_pos_gt1 formula-decl nil real_props nil) (leq formal-const-decl "(total_order?[T])" middle_value_index nil) (total_order? const-decl "bool" orders nil) (filter const-decl "bool" index_filters 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) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (both_sides_div_pos_ge1 formula-decl nil real_props nil) (times_div_cancel1 formula-decl nil extra_real_props "Manip/") (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (geq const-decl "bool" index_select nil) (epsilon const-decl "T" epsilons nil) (middle_value_exists formula-decl nil middle_value_index nil) (pred type-eq-decl nil defined_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) (T formal-type-decl nil middle_value_index nil) (middle_value const-decl "bool" middle_value_index 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) (below type-eq-decl nil naturalnumbers nil) (N formal-const-decl "posnat" middle_value_index 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) (epsilon_ax formula-decl nil epsilons nil) (TRUE const-decl "bool" booleans nil) (middle_index const-decl "below(N)" middle_value_index nil)) 1420 1230 t shostak)) (middle_good_bounded 0 (middle_good_bounded-1 nil 3265458917 3276346273 ("" (skosimp*) (("" (expand "majority_subset?") (("" (flatten) (("" (use "majority_pigeonhole") (("" (expand "filter") (("" (assert) (("" (prop) (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "subset?") (("2" (expand "member") (("2" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((majority_subset? const-decl "bool" pigeonhole nil) (majority_pigeonhole 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) (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) (N formal-const-decl "posnat" middle_value_index nil) (below type-eq-decl nil naturalnumbers 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) (filter const-decl "bool" index_filters nil) (T formal-type-decl nil middle_value_index nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil)) 687 490 nil nil)) (middle_value_lower_validity 0 (middle_value_lower_validity-2 nil 3276277974 3276346274 ("" (skosimp*) (("" (expand "middle_value") (("" (use "middle_good_bounded") (("" (assert) (("" (ground) (("" (hide-all-but 1) (("" (expand "middle_index") (("" (assert) (("" (expand "choose") (("" (use "epsilon_ax[below(N)]") (("1" (assert) (("1" (prop) (("1" (expand "middle_value") (("1" (assert) nil nil)) nil) ("2" (use "middle_value_exists") nil nil)) nil)) nil) ("2" (assert) (("2" (inst + 0) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((middle_value const-decl "T" middle_value_index nil) (TRUE const-decl "bool" booleans nil) (epsilon_ax formula-decl nil epsilons nil) (middle_value const-decl "bool" middle_value_index nil) (middle_value_exists formula-decl nil middle_value_index nil) (choose const-decl "(p)" 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) (N formal-const-decl "posnat" middle_value_index nil) (below type-eq-decl nil naturalnumbers nil) (T formal-type-decl nil middle_value_index 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) (middle_index const-decl "below(N)" middle_value_index nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (leq formal-const-decl "(total_order?[T])" middle_value_index nil) (middle_good_bounded formula-decl nil middle_value_index nil)) 958 900 t nil) (middle_value_lower_validity-1 nil 3266841587 3276277573 ("" (skosimp*) (("" (expand "middle_value") (("" (use "middle_good_bounded") (("" (assert) (("" (ground) (("" (hide-all-but 1) (("" (expand "middle_index") (("" (assert) (("" (expand "choose") (("" (use "epsilon_ax[below(M)]") (("1" (assert) (("1" (prop) (("1" (expand "middle_value") (("1" (assert) nil nil)) nil) ("2" (use "middle_value_exists") nil nil)) nil)) nil) ("2" (assert) (("2" (inst + 0) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished ((middle_value const-decl "T" middle_value_index nil) (TRUE const-decl "bool" booleans nil) (epsilon_ax formula-decl nil epsilons nil) (middle_value const-decl "bool" middle_value_index nil) (middle_value_exists formula-decl nil middle_value_index nil) (choose const-decl "(p)" 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) (below type-eq-decl nil naturalnumbers nil) (T formal-type-decl nil middle_value_index 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) (middle_index const-decl "below(N)" middle_value_index nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (leq formal-const-decl "(total_order?[T])" middle_value_index nil) (middle_good_bounded formula-decl nil middle_value_index nil)) 525 490 t shostak)) (middle_value_upper_validity 0 (middle_value_upper_validity-4 nil 3276278002 3276346275 ("" (skosimp*) (("" (expand "middle_value") (("" (lemma "middle_good_bounded") (("" (inst?) (("" (inst?) (("" (inst - "geq") (("" (assert) (("" (ground) (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (expand "geq") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (expand "middle_index") (("2" (expand "choose") (("2" (use "epsilon_ax[below(N)]") (("1" (assert) (("1" (ground) (("1" (rewrite "middle_value") (("1" (inst + 0) nil nil)) nil) ("2" (use "middle_value_exists") nil nil)) nil)) nil) ("2" (inst + 0) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((middle_value const-decl "T" middle_value_index 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) (N formal-const-decl "posnat" middle_value_index nil) (below type-eq-decl nil naturalnumbers nil) (T formal-type-decl nil middle_value_index 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) (middle_index const-decl "below(N)" middle_value_index nil) (geq const-decl "bool" index_select nil) (leq formal-const-decl "(total_order?[T])" middle_value_index nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (TRUE const-decl "bool" booleans nil) (epsilon_ax formula-decl nil epsilons nil) (middle_value const-decl "bool" middle_value_index nil) (epsilon const-decl "T" epsilons nil) (middle_value_exists formula-decl nil middle_value_index nil) (choose const-decl "(p)" sets nil) (middle_good_bounded formula-decl nil middle_value_index nil)) 755 680 nil nil) (middle_value_upper_validity-3 nil 3275840687 3276277573 ("" (skosimp*) (("" (expand "middle_value") (("" (lemma "middle_good_bounded") (("" (inst?) (("" (inst?) (("" (inst - "geq") (("" (assert) (("" (ground) (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (expand "geq") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (expand "middle_index") (("2" (expand "choose") (("2" (use "epsilon_ax[below(M)]") (("1" (assert) (("1" (ground) (("1" (rewrite "middle_value") (("1" (inst + 0) nil nil)) nil) ("2" (use "middle_value_exists") nil nil)) nil)) nil) ("2" (inst + 0) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished ((middle_good_bounded formula-decl nil middle_value_index nil) (choose const-decl "(p)" sets nil) (middle_value_exists formula-decl nil middle_value_index nil) (epsilon const-decl "T" epsilons nil) (middle_value const-decl "bool" middle_value_index nil) (epsilon_ax formula-decl nil epsilons nil) (TRUE const-decl "bool" booleans nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (leq formal-const-decl "(total_order?[T])" middle_value_index nil) (geq const-decl "bool" index_select nil) (middle_index const-decl "below(N)" middle_value_index 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) (T formal-type-decl nil middle_value_index nil) (below type-eq-decl nil naturalnumbers 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) (middle_value const-decl "T" middle_value_index nil)) 528 400 nil nil) (middle_value_upper_validity-2 nil 3275840651 3275840663 ("" (skosimp*) (("" (expand "middle_value") (("" (lemma "middle_good_bounded") (("" (inst?) (("" (inst?) (("" (inst - ">=") (("" (assert) (("" (ground) (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (expand "geq") (("1" (propax) nil))))))))) ("2" (hide -1 2) (("2" (expand "middle_index") (("2" (expand "choose") (("2" (use "epsilon_ax[below(M)]") (("1" (assert) (("1" (ground) (("1" (rewrite "middle_value") (("1" (inst + 0) nil))) ("2" (use "middle_value_exists") nil))))) ("2" (inst + 0) nil)))))))))))))))))))))))) nil) unfinished nil 11775 690 t nil) (middle_value_upper_validity-1 nil 3266845095 3275840618 ("" (skosimp*) (("" (expand "middle_value") (("" (lemma "middle_good_bounded") (("" (inst?) (("" (inst?) (("" (inst - ">=") (("" (assert) (("" (ground) (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (expand ">=") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -1 2) (("2" (expand "middle_index") (("2" (expand "choose") (("2" (use "epsilon_ax[below(M)]") (("1" (assert) (("1" (ground) (("1" (rewrite "middle_value") (("1" (inst + 0) nil nil)) nil) ("2" (use "middle_value_exists") nil nil)) nil)) nil) ("2" (inst + 0) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unfinished ((middle_value const-decl "T" middle_value_index 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) (below type-eq-decl nil naturalnumbers nil) (T formal-type-decl nil middle_value_index 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) (middle_index const-decl "below(N)" middle_value_index nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (TRUE const-decl "bool" booleans nil) (epsilon_ax formula-decl nil epsilons nil) (middle_value const-decl "bool" middle_value_index nil) (epsilon const-decl "T" epsilons nil) (middle_value_exists formula-decl nil middle_value_index nil) (choose const-decl "(p)" sets nil) (middle_good_bounded formula-decl nil middle_value_index nil)) 389 370 t shostak)) (middle_value_exact_validity 0 (middle_value_exact_validity-1 nil 3276519967 3276520204 ("" (skosimp*) (("" (expand "good_vote_for?") (("" (use "middle_value_lower_validity") (("" (use "middle_value_upper_validity") (("" (assert) (("" (skosimp*) (("" (inst-cp - "i!1") (("" (inst - "i!2") (("" (assert) (("" (typepred! "leq") (("" (expand "total_order?") (("" (expand "partial_order?") (("" (expand "antisymmetric?") (("" (flatten) (("" (replace*) (("" (hide -9 -10) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((good_vote_for? const-decl "bool" good_vote_for nil) (middle_value_upper_validity formula-decl nil middle_value_index nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (leq formal-const-decl "(total_order?[T])" middle_value_index nil) (partial_order? const-decl "bool" orders nil) (middle_value const-decl "T" middle_value_index nil) (antisymmetric? const-decl "bool" relations 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) (N formal-const-decl "posnat" middle_value_index 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) (T formal-type-decl nil middle_value_index nil) (middle_value_lower_validity formula-decl nil middle_value_index nil)) 236929 7320 t shostak)) (middle_value_overlap 0 (middle_value_overlap-1 nil 3265458917 3276346276 ("" (skosimp*) (("" (expand "middle_value") (("" (lemma "index_value_overlap") (("" (inst?) (("" (assert) (("" (inst - "floor(card(eligible!1)/2)") (("1" (rewrite "middle_index_value") (("1" (rewrite "middle_index_value") nil nil)) nil) ("2" (assert) (("2" (hide 2) (("2" (use "card_below") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((middle_value const-decl "T" middle_value_index nil) (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) (NOT const-decl "[bool -> bool]" booleans nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (middle_index const-decl "below(N)" middle_value_index nil) 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) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (<= const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (integer nonempty-type-from-decl nil integers nil) (middle_index_value formula-decl nil middle_value_index nil) (card_below formula-decl nil finite_sets_below "finite_sets/") (index_value_overlap formula-decl nil index_select 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) (N formal-const-decl "posnat" middle_value_index nil) (T formal-type-decl nil middle_value_index nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (leq formal-const-decl "(total_order?[T])" middle_value_index nil)) 317 310 t nil))) $$$good_vote_for.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Design : SPIDER Version 2 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% good_vote_for[N: posnat, T: TYPE]: THEORY BEGIN IMPORTING finite_sets@finite_sets_below[N] n: VAR below(N) t: VAR T f, f1, f2: VAR [below(N) -> T] good, eligible: VAR finite_set[below(N)] good_vote_for?(good, f, t) : bool = FORALL n: good(n) IMPLIES f(n) = t eligible_symmetric?(eligible, f1, f2): bool = FORALL n: eligible(n) IMPLIES f1(n) = f2(n) votes_for(eligible, f, t): finite_set[below(N)] = {n | eligible(n) AND f(n) = t} votes_for_subset: LEMMA subset?(votes_for(eligible, f, t), eligible) eligible_symmetric_vote_same: LEMMA eligible_symmetric?(eligible, f1, f2) IMPLIES votes_for(eligible, f1, t) = votes_for(eligible, f2, t) END good_vote_for $$$good_vote_for.prf (good_vote_for (votes_for_TCC1 0 (votes_for_TCC1-1 nil 3276528241 3276530105 ("" (skosimp*) (("" (rewrite "finite_below[N]") nil nil)) nil) proved ((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) (AND const-decl "[bool, bool -> bool]" booleans nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (T formal-type-decl nil good_vote_for nil) (= const-decl "[T, T -> boolean]" equalities 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) (N formal-const-decl "posnat" good_vote_for nil)) 8248 1010 t shostak)) (votes_for_subset 0 (votes_for_subset-1 nil 3276528629 3276529994 ("" (skosimp*) (("" (auto-rewrite-defs) (("" (assert) (("" (skosimp*) nil nil)) nil)) nil)) nil) proved ((votes_for const-decl "finite_set[below(N)]" good_vote_for nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil)) 9534 1990 t nil)) (eligible_symmetric_vote_same 0 (eligible_symmetric_vote_same-1 nil 3276530010 3276530051 ("" (skosimp*) (("" (apply-extensionality :hide? t) (("" (expand "votes_for") (("" (expand "eligible_symmetric?") (("" (inst?) (("" (iff) (("" (ground) 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) (N formal-const-decl "posnat" good_vote_for nil) (below type-eq-decl nil naturalnumbers nil) (set type-eq-decl nil sets nil) (votes_for const-decl "finite_set[below(N)]" good_vote_for nil) (T formal-type-decl nil good_vote_for nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (eligible_symmetric? const-decl "bool" good_vote_for nil)) 41454 4010 t shostak))) $$$select_minmax.pvs select_minmax[N: posnat, T: TYPE, <=: (total_order?[T])]: THEORY BEGIN IMPORTING finite_sets@finite_sets_minmax[T, <=], good_vote_for[N, T] select: VAR non_empty_finite_set[below(N)] v: VAR [below(N) -> T] n: VAR below(N) t: VAR T v_min(v, select): T = min(image(v, select)) v_max(v, select): T = max(image(v, select)) v_min_witness: LEMMA EXISTS n: select(n) AND v_min(v, select) = v(n) v_max_witness: LEMMA EXISTS n: select(n) AND v_max(v, select) = v(n) v_min_is_min: LEMMA select(n) IMPLIES v_min(v, select) <= v(n) v_max_is_max: LEMMA select(n) IMPLIES v(n) <= v_max(v, select) v_minmax_vote_for: LEMMA good_vote_for?(select, v, t) IFF (v_max(v, select) = v_min(v, select) AND v_min(v, select) = t) END select_minmax $$$select_minmax.prf (select_minmax (v_min_TCC1 0 (v_min_TCC1-1 nil 3292345986 3292346145 ("" (skosimp*) (("" (typepred "select!1") (("" (expand "empty?") (("" (expand "image") (("" (expand "member") (("" (skosimp*) (("" (inst - "v!1(x!1)") (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved-complete ((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) (below type-eq-decl nil naturalnumbers nil) (N formal-const-decl "posnat" select_minmax 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) (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) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil select_minmax nil) (member const-decl "bool" sets nil)) 59131 2880 t shostak)) (v_min_witness 0 (v_min_witness-1 nil 3292346160 3292346624 ("" (skosimp*) (("" (expand "v_min") (("" (typepred "min(image(v!1, select!1))") (("1" (hide -2) (("1" (rewrite "image" -1) (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (use "v_min_TCC1") nil nil)) nil)) nil)) nil) unchecked ((v_min const-decl "T" select_minmax nil) (v_min_TCC1 subtype-tcc nil select_minmax nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< 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 "posnat" select_minmax nil) (below type-eq-decl nil naturalnumbers nil) (T formal-type-decl nil select_minmax nil) (set type-eq-decl nil sets nil) 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" select_minmax nil) (min const-decl "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES a <= x)}" finite_sets_minmax "finite_sets/")) 138 140 t shostak)) (v_max_witness 0 (v_max_witness-1 nil 3292346450 3292346624 ("" (skosimp*) (("" (expand "v_max") (("" (typepred "max(image(v!1, select!1))") (("1" (hide -2) (("1" (rewrite "image" -1) (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (use "v_min_TCC1") nil nil)) nil)) nil)) nil) unchecked ((v_max const-decl "T" select_minmax nil) (v_min_TCC1 subtype-tcc nil select_minmax nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< 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 "posnat" select_minmax nil) (below type-eq-decl nil naturalnumbers nil) (T formal-type-decl nil select_minmax nil) (set type-eq-decl nil sets nil) 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" select_minmax nil) (max const-decl "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" finite_sets_minmax "finite_sets/")) 227 140 t shostak)) (v_min_is_min 0 (v_min_is_min-1 nil 3292346679 3292346765 ("" (skosimp*) (("" (expand "v_min") (("" (typepred "min(image(v!1, select!1))") (("1" (inst?) (("1" (assert) (("1" (rewrite "image" +) (("1" (inst?) nil nil)) nil)) nil)) nil) ("2" (use "v_min_TCC1") nil nil)) nil)) nil)) nil) unchecked ((v_min const-decl "T" select_minmax nil) (v_min_TCC1 subtype-tcc nil select_minmax nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< 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 "posnat" select_minmax nil) (below type-eq-decl nil naturalnumbers nil) (T formal-type-decl nil select_minmax nil) (set type-eq-decl nil sets nil) 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" select_minmax nil) (min const-decl "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES a <= x)}" finite_sets_minmax "finite_sets/")) 86736 3230 t shostak)) (v_max_is_max 0 (v_max_is_max-1 nil 3292346777 3292346807 ("" (skosimp*) (("" (expand "v_max") (("" (typepred "max(image(v!1, select!1))") (("1" (inst?) (("1" (assert) (("1" (rewrite "image" +) (("1" (inst?) nil nil)) nil)) nil)) nil) ("2" (use "v_min_TCC1") nil nil)) nil)) nil)) nil) unchecked ((v_max const-decl "T" select_minmax nil) (v_min_TCC1 subtype-tcc nil select_minmax nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< 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 "posnat" select_minmax nil) (below type-eq-decl nil naturalnumbers nil) (T formal-type-decl nil select_minmax nil) (set type-eq-decl nil sets nil) 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" select_minmax nil) (max const-decl "{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" finite_sets_minmax "finite_sets/")) 29331 2580 t shostak)) (v_minmax_vote_for 0 (v_minmax_vote_for-1 nil 3292582177 3292582945 ("" (skosimp*) (("" (prop) (("1" (lemma "v_min_witness") (("1" (inst?) (("1" (lemma "v_max_witness") (("1" (inst?) (("1" (expand "good_vote_for?") (("1" (skosimp*) (("1" (inst-cp - "n!2") (("1" (inst - "n!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "v_min_witness") (("2" (inst?) (("2" (skosimp*) (("2" (expand "good_vote_for?") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "good_vote_for?") (("3" (skosimp*) (("3" (lemma "v_min_is_min") (("3" (inst?) (("3" (inst?) (("3" (assert) (("3" (lemma "v_max_is_max") (("3" (inst?) (("3" (inst?) (("3" (assert) (("3" (replace*) (("3" (hide -3 -4 -5) (("3" (typepred "<=") (("3" (expand "total_order?") (("3" (expand "partial_order?") (("3" (expand "antisymmetric?") (("3" (flatten) (("3" (inst?) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (N formal-const-decl "posnat" select_minmax 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) (T formal-type-decl nil select_minmax nil) (good_vote_for? const-decl "bool" good_vote_for nil) (v_max_witness formula-decl nil select_minmax nil) (v_min_witness formula-decl nil select_minmax nil) (antisymmetric? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" select_minmax nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (v_max_is_max formula-decl nil select_minmax nil) (v_min_is_min formula-decl nil select_minmax nil)) 767076 26440 t shostak))) $$$k_stage_shared.pvs k_stage_shared [ N : [nat -> posnat], T : TYPE+, <= : (total_order?[T]), error: [nat -> T] ]: THEORY BEGIN IMPORTING select_minmax, middle_value_index, eligibility, voter 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)) -> T]] rcvd: VAR [j : nat -> [below(N(j+1)) -> [below(N(j)) -> T]]] good_filter(good, eligible)(j): [below(N(j+1)) -> finite_set[below(N(j))]] = LAMBDA (d : below(N(j+1))): intersection(good(j), eligible(j)(d)) v_min(sent, good)(j) : MACRO T = v_min[N(j), T, <=](sent(j), good(j)) v_max(sent, good)(j) : MACRO T = v_max[N(j), T, <=](sent(j), good(j)) % Model of multi-stage protocol (simplified) protocol(sent, rcvd, eligible, j, k) : bool = FORALL i : j <= i AND i < k IMPLIES FORALL (d: below(N(i + 1))): sent(i + 1)(d) = voter[N(i), N(i + 1), T](middle_value[N(i), T, <=], eligible(i), rcvd(i), error(i))(d) % Abstracted fault assumptions majority_subsets?(good_eligible, eligible, j, k): bool = %implied by VPFA FORALL i : j <= i AND i < k IMPLIES majority_subsets?[N(i), N(i + 1)](good_eligible(i), eligible(i)) eligible_nonasymmetric?(good_eligible, eligible, nonasym, j, k): bool = % implied by AGFA EXISTS i: j <= i AND i < k AND eligible_sources_property?[N(i), N(i + 1)](eligible(i), nonasym(i)) AND subsets?[N(i), N(i + 1)](eligible(i), nonasym(i)) AND majority_subsets?(good_eligible, eligible, i + 1, k) END k_stage_shared $$$k_exact.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % File Name : k_exact.pvs % % Purpose : validity and agreement properties for all destination % nodes of a k-stage exchange. % % Assumptions : No error is introduced during communication. % % Guarantees : % % Design : SPIDER Version 2 % % Dependencies : % % Comments : % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% k_exact [ N : [nat -> posnat], % Number of source nodes at each stage T : TYPE+, <= : (total_order?[T]), error: [nat -> T] ] : THEORY BEGIN IMPORTING k_stage_shared[N, T, <=, error], exact_sampling i, j, k: VAR nat v: VAR T 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)) -> T]] rcvd: VAR [j : nat -> [below(N(j+1)) -> [below(N(j)) -> T]]] % Abstracted model of communication sampling_exact?(good_eligible, sent, rcvd, j, k): bool = FORALL i : j <= i AND i < k IMPLIES sampling_exact?[N(i), N(i + 1), T](good_eligible(i), sent(i), rcvd(i)) exact_symmetry?(nonasym, rcvd, j, k): bool = FORALL i : j <= i AND i < k IMPLIES exact_symmetry?[N(i), N(i + 1), T](nonasym(i), rcvd(i)) % 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_exact?(good_filter(good, eligible), sent, rcvd, j, j + k) IMPLIES v_min(sent, good)(j) <= 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_exact?(good_filter(good, eligible), sent, rcvd, j, j + k) IMPLIES v_max(sent, good)(j + k) <= v_max(sent, good)(j) consensus_validity: COROLLARY protocol(sent, rcvd, eligible, j, j + k) AND majority_subsets?(good_filter(good, eligible), eligible, j, j + k) AND sampling_exact?(good_filter(good, eligible), sent, rcvd, j, j + k) AND good_vote_for?[N(j), T](good(j), sent(j), v) IMPLIES good_vote_for?[N(j + k), T](good(j + k), sent(j + k), v) agreement_generation: THEOREM protocol(sent, rcvd, eligible, j, j + k) AND eligible_nonasymmetric?(good_filter(good, eligible), eligible, nonasym, j, j + k) AND sampling_exact?(good_filter(good, eligible), sent, rcvd, j, j + k) AND exact_symmetry?(nonasym, rcvd, j, j + k) IMPLIES v_max(sent, good)(j + k) = v_min(sent, good)(j + k) END k_exact $$$k_exact.prf (k_exact (lower_validity 0 (lower_validity-1 nil 3292509781 3292584747 ("" (induct "k") (("1" (skosimp*) (("1" (assert) (("1" (typepred "<=") (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "reflexive?") (("1" (flatten) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst?) (("2" (inst?) (("2" (inst?) (("2" (assert) (("2" (prop) (("1" (typepred "<=") (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "transitive?") (("1" (flatten) (("1" (inst - "v_min[N(j!2), T, <=](sent!1(j!2), good!1(j!2))" "v_min[N(j!2 + j!1), T, <=](sent!1(j!1 + j!2), good!1(j!1 + j!2))" "v_min[N(1 + j!2 + j!1), T, <=] (sent!1(1 + j!1 + j!2), good!1(1 + j!1 + j!2))") (("1" (assert) (("1" (hide -4 2) (("1" (lemma "v_min_witness[N(1 + j!2 + j!1), T, <=]") (("1" (inst?) (("1" (skosimp*) (("1" (replace -2 :hide? t) (("1" (expand "protocol") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (replace -5 :hide? t) (("1" (expand "majority_subsets?") (("1" (inst?) (("1" (assert) (("1" (expand "voter") (("1" (lemma "majority_subsets_nonempty[N(j!1 + j!2), N(1 + j!1 + j!2)]") (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (expand "majority_subsets?") (("1" (inst?) (("1" (lemma "middle_value_lower_validity[N(j!1 + j!2), T, <=]") (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (expand "sampling_exact?") (("1" (inst?) (("1" (assert) (("1" (expand "sampling_exact?") (("1" (inst?) (("1" (assert) (("1" (lemma "v_min_is_min[N(j!2 + j!1), T, <=]") (("1" (inst?) (("1" (inst?) (("1" (expand* "good_filter" "intersection" "member") (("1" (flatten) (("1" (assert) (("1" (replace -10) (("1" (hide-all-but (-1 -4 2)) (("1" (typepred "<=") (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "transitive?") (("1" (inst - "v_min[N(j!2 + j!1), T, <=](sent!1(j!1 + j!2), good!1(j!1 + j!2))" "rcvd!1(j!1 + j!2)(n!1)(i!1)" "middle_value[N(j!1 + j!2), T, <=](eligible!1(j!1 + j!2)(n!1), rcvd!1(j!1 + j!2)(n!1))") (("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)) 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_exact?") (("4" (skosimp*) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((transitive? const-decl "bool" relations nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (majority_subsets_nonempty formula-decl nil eligibility nil) (majority_subsets? const-decl "bool" eligibility nil) (middle_value_lower_validity formula-decl nil middle_value_index nil) (sampling_exact? const-decl "bool" exact_sampling nil) (intersection const-decl "set" sets nil) (member const-decl "bool" sets nil) (middle_value const-decl "T" middle_value_index nil) (v_min_is_min formula-decl nil select_minmax nil) (voter const-decl "T" voter nil) (v_min_witness formula-decl nil select_minmax nil) (partial_order? const-decl "bool" orders nil) (reflexive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (nat_induction formula-decl nil naturalnumbers nil) (v_min const-decl "T" select_minmax nil) (sampling_exact? const-decl "bool" k_exact nil) (good_filter const-decl "[below(N(j + 1)) -> finite_set[below(N(j))]]" k_stage_shared nil) (majority_subsets? const-decl "bool" k_stage_shared nil) (protocol const-decl "bool" k_stage_shared nil) (error formal-const-decl "[nat -> T]" k_exact nil) (<= formal-const-decl "(total_order?[T])" k_exact nil) (total_order? const-decl "bool" orders nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (T formal-nonempty-type-decl nil k_exact 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_exact 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)) 2106 1800 t shostak)) (upper_validity 0 (upper_validity-2 nil 3292523172 3292584754 ("" (induct "k") (("1" (skosimp*) (("1" (assert) (("1" (typepred "<=") (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "reflexive?") (("1" (flatten) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "eligible!1" "good!1" "j!2" "rcvd!1" "sent!1") (("2" (prop) (("1" (typepred "<=") (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "transitive?") (("1" (flatten) (("1" (inst - "v_max[N(1 + j!2 + j!1), T, <=](sent!1(1 + j!1 + j!2), good!1(1 + j!1 + j!2))" "v_max[N(j!2 + j!1), T, <=](sent!1(j!1 + j!2), good!1(j!1 + j!2))" "v_max[N(j!2), T, <=](sent!1(j!2), good!1(j!2))") (("1" (assert) (("1" (hide -4 2) (("1" (lemma "v_max_witness[N(1 + j!2 + j!1), T, <=]") (("1" (inst?) (("1" (skosimp*) (("1" (replace -2 :hide? t) (("1" (expand "protocol") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (replace -5 :hide? t) (("1" (expand "majority_subsets?") (("1" (inst?) (("1" (assert) (("1" (expand "voter") (("1" (lemma "majority_subsets_nonempty[N(j!1 + j!2), N(1 + j!1 + j!2)]") (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (expand "majority_subsets?") (("1" (inst?) (("1" (lemma "middle_value_upper_validity[N(j!1 + j!2), T, <=]") (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (expand "sampling_exact?") (("1" (inst?) (("1" (assert) (("1" (expand "sampling_exact?") (("1" (inst?) (("1" (assert) (("1" (lemma "v_max_is_max[N(j!2 + j!1), T, <=]") (("1" (inst - "i!1" "good!1(j!1+j!2)" "sent!1(j!1+j!2)") (("1" (expand* "good_filter" "intersection" "member") (("1" (flatten) (("1" (assert) (("1" (replace -10) (("1" (hide-all-but (-1 -4 2)) (("1" (typepred "<=") (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "transitive?") (("1" (inst - "middle_value[N(j!1 + j!2), T, <=](eligible!1(j!1 + j!2)(n!1), rcvd!1(j!1 + j!2)(n!1))" "rcvd!1(j!1 + j!2)(n!1)(i!1)" "v_max[N(j!2 + j!1), T, <=](sent!1(j!1 + j!2), good!1(j!1 + j!2))") (("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" (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_exact?") (("4" (skosimp*) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((v_max_witness formula-decl nil select_minmax nil) (voter const-decl "T" voter nil) (v_max_is_max formula-decl nil select_minmax nil) (intersection const-decl "set" sets nil) (member const-decl "bool" sets nil) (middle_value const-decl "T" middle_value_index nil) (sampling_exact? const-decl "bool" exact_sampling nil) (middle_value_upper_validity formula-decl nil middle_value_index nil) (majority_subsets? const-decl "bool" eligibility nil) (majority_subsets_nonempty formula-decl nil eligibility nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (transitive? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (reflexive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (nat_induction formula-decl nil naturalnumbers nil) (v_max const-decl "T" select_minmax nil) (sampling_exact? const-decl "bool" k_exact nil) (good_filter const-decl "[below(N(j + 1)) -> finite_set[below(N(j))]]" k_stage_shared nil) (majority_subsets? const-decl "bool" k_stage_shared nil) (protocol const-decl "bool" k_stage_shared nil) (error formal-const-decl "[nat -> T]" k_exact nil) (<= formal-const-decl "(total_order?[T])" k_exact nil) (total_order? const-decl "bool" orders nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (T formal-nonempty-type-decl nil k_exact 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_exact 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)) 6764 1750 t nil) (upper_validity-1 nil 3292523101 nil ("" (induct "k") (("1" (skosimp*) (("1" (assert) (("1" (typepred "<=") (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "reflexive?") (("1" (flatten) (("1" (inst?) nil))))))))))))))))) ("2" (skosimp*) (("2" (inst?) (("2" (inst?) (("2" (inst?) (("2" (assert) (("2" (prop) (("1" (typepred "<=") (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "transitive?") (("1" (flatten) (("1" (inst - "v_min[N(j!2), T, <=](sent!1(j!2), good!1(j!2))" "v_min[N(j!2 + j!1), T, <=](sent!1(j!1 + j!2), good!1(j!1 + j!2))" "v_min[N(1 + j!2 + j!1), T, <=] (sent!1(1 + j!1 + j!2), good!1(1 + j!1 + j!2))") (("1" (assert) (("1" (hide -4 2) (("1" (lemma "v_min_witness[N(1 + j!2 + j!1), T, <=]") (("1" (inst?) (("1" (skosimp*) (("1" (replace -2 :hide? t) (("1" (expand "protocol") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (replace -5 :hide? t) (("1" (expand "majority_subsets?") (("1" (inst?) (("1" (assert) (("1" (expand "voter") (("1" (lemma "majority_subsets_nonempty[N(j!1 + j!2), N(1 + j!1 + j!2)]") (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (expand "majority_subsets?") (("1" (inst?) (("1" (lemma "middle_value_lower_validity[N(j!1 + j!2), T, <=]") (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (skosimp*) (("1" (expand "sampling_exact?") (("1" (inst?) (("1" (assert) (("1" (expand "sampling_exact?") (("1" (inst?) (("1" (assert) (("1" (lemma "v_min_is_min[N(j!2 + j!1), T, <=]") (("1" (inst?) (("1" (inst?) (("1" (expand* "good_filter" "intersection" "member") (("1" (flatten) (("1" (assert) (("1" (replace -10) (("1" (hide-all-but (-1 -4 2)) (("1" (typepred "<=") (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "transitive?") (("1" (inst - "v_min[N(j!2 + j!1), T, <=](sent!1(j!1 + j!2), good!1(j!1 + j!2))" "rcvd!1(j!1 + j!2)(n!1)(i!1)" "middle_value[N(j!1 + j!2), T, <=](eligible!1(j!1 + j!2)(n!1), rcvd!1(j!1 + j!2)(n!1))") (("1" (assert) nil))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ("2" (expand "protocol") (("2" (skosimp*) (("2" (inst?) (("2" (assert) (("2" (inst?) nil))))))))) ("3" (expand "majority_subsets?") (("3" (skosimp*) (("3" (inst?) (("3" (assert) nil))))))) ("4" (expand "sampling_exact?") (("4" (skosimp*) (("4" (inst?) (("4" (assert) nil)))))))))))))))))))) nil) unchecked nil nil nil nil nil)) (consensus_validity 0 (consensus_validity-2 nil 3292584122 3292584756 ("" (induct "k") (("1" (skosimp*) (("1" (assert) nil nil)) nil) ("2" (skosimp*) (("2" (inst - "eligible!1" "good!1" "j!2" "rcvd!1" "sent!1" "v!1") (("2" (assert) (("2" (prop) (("1" (hide -5) (("1" (rewrite "good_vote_for?" +) (("1" (skosimp*) (("1" (expand "sampling_exact?") (("1" (inst?) (("1" (assert) (("1" (expand "majority_subsets?") (("1" (inst?) (("1" (assert) (("1" (expand "protocol") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (replace*) (("1" (hide -2) (("1" (lemma "majority_subsets_nonempty[N(j!1 + j!2), N(1 + j!1 + j!2)]") (("1" (expand "voter") (("1" (lift-if) (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (expand "majority_subsets?") (("1" (inst?) (("1" (lemma "middle_value_exact_validity[N(j!1 + j!2), T, <=]") (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (expand "good_vote_for?") (("1" (skosimp*) (("1" (inst - "n!2") (("1" (expand "sampling_exact?") (("1" (inst?) (("1" (assert) (("1" (expand "good_filter") (("1" (expand "intersection") (("1" (expand "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) ("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_exact?") (("4" (skosimp*) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((- const-decl "[numfield, numfield -> numfield]" number_fields nil) (voter const-decl "T" voter nil) (sampling_exact? const-decl "bool" exact_sampling nil) (intersection const-decl "set" sets nil) (member const-decl "bool" sets nil) (middle_value_exact_validity formula-decl nil middle_value_index nil) (majority_subsets? const-decl "bool" eligibility nil) (majority_subsets_nonempty formula-decl nil eligibility nil) (nat_induction formula-decl nil naturalnumbers nil) (good_vote_for? const-decl "bool" good_vote_for nil) (sampling_exact? const-decl "bool" k_exact nil) (good_filter const-decl "[below(N(j + 1)) -> finite_set[below(N(j))]]" k_stage_shared nil) (majority_subsets? const-decl "bool" k_stage_shared nil) (protocol const-decl "bool" k_stage_shared nil) (error formal-const-decl "[nat -> T]" k_exact nil) (<= formal-const-decl "(total_order?[T])" k_exact nil) (total_order? const-decl "bool" orders nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (T formal-nonempty-type-decl nil k_exact 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_exact 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)) 1797 1510 t nil) (consensus_validity-1 nil 3292526257 3292575623 ("" (skosimp*) (("" (forward-chain "upper_validity") (("" (forward-chain "lower_validity") (("" (assert) (("" (replace*) (("" (hide -3 -4 -5 -6) (("" (typepred "<=") (("" (expand "total_order?") (("" (expand "partial_order?") (("" (expand "antisymmetric?") (("" (flatten) (("" (inst?) (("" (assert) (("" (prop) (("1" (hide -2 2) (("1" (expand "preorder?") (("1" (expand "transitive?") (("1" (flatten) (("1" (inst?) (("1" (inst - "v_min[N(j!1), T, <=](sent!1(j!1), good!1(j!1))") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (use "v_max_witness[N(j!1 + k!1), T, <=]") (("2" (skosimp*) (("2" (replace -2 :hide? t) (("2" (use "v_min_is_min[N(j!1 + k!1), T, <=]") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) unchecked ((upper_validity formula-decl nil k_exact 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) (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) (< 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_exact 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) (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) (T formal-nonempty-type-decl nil k_exact nil) (antisymmetric? const-decl "bool" relations nil) (v_min const-decl "T" select_minmax nil) (v_max const-decl "T" select_minmax nil) (preorder? const-decl "bool" orders nil) (transitive? const-decl "bool" relations nil) (v_max_witness formula-decl nil select_minmax nil) (v_min_is_min formula-decl nil select_minmax nil) (partial_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" k_exact nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (lower_validity formula-decl nil k_exact nil)) 645 470 t shostak)) (agreement_generation 0 (agreement_generation-1 nil 3292529966 3292585885 ("" (skosimp*) (("" (expand "eligible_nonasymmetric?") (("" (skosimp*) (("" (lemma "consensus_validity") (("" (assert) (("" (inst - _ _ "i!1+1" "j!1+k!1-(i!1+1)" _ _ _) (("" (assert) (("" (inst?) (("" (inst?) (("" (inst?) (("" (inst - "v_min[N(1+i!1), T, <=] (sent!1(1 + i!1), good!1(1 + i!1))") (("" (rewrite "v_minmax_vote_for[N(j!1 + k!1), T, <=]") (("" (assert) (("" (prop) (("1" (hide-all-but (-1 1)) (("1" (expand "protocol") (("1" (skosimp*) (("1" (inst?) (("1" (assert) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-7 1)) (("2" (expand "sampling_exact?") (("2" (skosimp*) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (hide -6 -7 2) (("3" (rewrite "v_minmax_vote_for[N(1 + i!1), T, <=]") (("3" (use "v_max_witness[N(1 + i!1), T, <=]") (("3" (use "v_min_witness[N(1 + i!1), T, <=]") (("3" (skosimp*) (("3" (replace*) (("3" (hide -2 -4) (("3" (expand "protocol") (("3" (inst?) (("3" (assert) (("3" (inst-cp - "n!2") (("3" (inst - "n!1") (("3" (replace*) (("3" (hide -3 -4) (("3" (lemma "eligible_agree[N(i!1), N(i!1 + 1)]") (("3" (inst - "n!1" "n!2" "nonasym!1(i!1)" "eligible!1(i!1)") (("3" (assert) (("3" (expand "voter") (("3" (lift-if) (("3" (assert) (("3" (prop) (("3" (lemma "middle_value_overlap[N(i!1), T, <=]") (("3" (inst-cp - "eligible!1(i!1)(n!1)" "rcvd!1(i!1)(n!1)" "rcvd!1(i!1)(n!2)") (("1" (inst - "eligible!1(i!1)(n!1)" "rcvd!1(i!1)(n!2)" "rcvd!1(i!1)(n!1)") (("1" (skosimp*) (("1" (expand "exact_symmetry?") (("1" (inst?) (("1" (assert) (("1" (expand "exact_symmetry?") (("1" (inst-cp - "n!1" "n!2" "j!2") (("1" (inst - "n!1" "n!2" "j!3") (("1" (expand "subsets?") (("1" (inst?) (("1" (assert) (("1" (expand "subset?") (("1" (expand "member") (("1" (inst-cp - "j!2") (("1" (inst - "j!3") (("1" (assert) (("1" (replace*) (("1" (hide -1 -4 -7 -8 -9 -10 -11 -12 -13 -14 -15 -16 1) (("1" (typepred "<=") (("1" (expand "total_order?") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (expand "transitive?") (("1" (flatten) (("1" (inst-cp - "middle_value[N(i!1), T, <=](eligible!1(i!1)(n!2), rcvd!1(i!1)(n!1))" "rcvd!1(i!1)(n!2)(j!2)" "middle_value[N(i!1), T, <=](eligible!1(i!1)(n!2), rcvd!1(i!1)(n!2))") (("1" (inst - "middle_value[N(i!1), T, <=](eligible!1(i!1)(n!2), rcvd!1(i!1)(n!2))" "rcvd!1(i!1)(n!2)(j!3)" "middle_value[N(i!1), T, <=](eligible!1(i!1)(n!2), rcvd!1(i!1)(n!1))") (("1" (assert) (("1" (hide-all-but (-2 -3 -4 1)) (("1" (expand "antisymmetric?") (("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) ("2" (assert) 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)) nil)) nil)) nil)) nil)) nil) proved ((eligible_nonasymmetric? const-decl "bool" k_stage_shared nil) (consensus_validity formula-decl nil k_exact 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) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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_exact 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_minmax_vote_for formula-decl nil select_minmax nil) (protocol const-decl "bool" k_stage_shared nil) (sampling_exact? const-decl "bool" k_exact nil) (v_min_witness formula-decl nil select_minmax nil) (voter const-decl "T" voter nil) (middle_value_overlap formula-decl nil middle_value_index nil) (exact_symmetry? const-decl "bool" k_exact nil) (subsets? const-decl "bool" eligibility nil) (member const-decl "bool" sets nil) (partial_order? const-decl "bool" orders nil) (transitive? const-decl "bool" relations nil) (middle_value const-decl "T" middle_value_index nil) (antisymmetric? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (subset? const-decl "bool" sets nil) (exact_symmetry? const-decl "bool" exact_sampling nil) (n!1 skolem-const-decl "below(N(1 + i!1))" k_exact nil) (eligible!1 skolem-const-decl "[j: nat -> [below(N(1 + j)) -> finite_set[below(N(j))]]]" k_exact nil) (i!1 skolem-const-decl "nat" k_exact nil) (eligible_agree formula-decl nil eligibility nil) (v_max_witness formula-decl nil select_minmax nil) (v_min const-decl "T" select_minmax nil) (<= formal-const-decl "(total_order?[T])" k_exact nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (T formal-nonempty-type-decl nil k_exact nil)) 1020052 46930 t shostak))) $$$unified_msg_adt.pvs %%% ADT file generated from unified_msg unified_msg_adt[T: TYPE+]: THEORY BEGIN ASSUMING T_TCC1: ASSUMPTION EXISTS (x: T): TRUE; ENDASSUMING unified_msg: TYPE receive_error?, no_majority?, source_error?, payload?: [unified_msg -> boolean] receive_error: (receive_error?) no_majority: (no_majority?) source_error: [nat -> (source_error?)] payload: [T -> (payload?)] stage: [(source_error?) -> nat] value: [(payload?) -> T] unified_msg_ord: [unified_msg -> upto(3)] unified_msg_ord_defaxiom: AXIOM unified_msg_ord(receive_error) = 0 AND unified_msg_ord(no_majority) = 1 AND (FORALL (stage: nat): unified_msg_ord(source_error(stage)) = 2) AND (FORALL (value: T): unified_msg_ord(payload(value)) = 3); ord(x: unified_msg): upto(3) = CASES x OF receive_error: 0, no_majority: 1, source_error(source_error1_var): 2, payload(payload1_var): 3 ENDCASES unified_msg_receive_error_extensionality: AXIOM FORALL (receive_error?_var: (receive_error?), receive_error?_var2: (receive_error?)): receive_error?_var = receive_error?_var2; unified_msg_no_majority_extensionality: AXIOM FORALL (no_majority?_var: (no_majority?), no_majority?_var2: (no_majority?)): no_majority?_var = no_majority?_var2; unified_msg_source_error_extensionality: AXIOM FORALL (source_error?_var: (source_error?), source_error?_var2: (source_error?)): stage(source_error?_var) = stage(source_error?_var2) IMPLIES source_error?_var = source_error?_var2; unified_msg_source_error_eta: AXIOM FORALL (source_error?_var: (source_error?)): source_error(stage(source_error?_var)) = source_error?_var; unified_msg_payload_extensionality: AXIOM FORALL (payload?_var: (payload?), payload?_var2: (payload?)): value(payload?_var) = value(payload?_var2) IMPLIES payload?_var = payload?_var2; unified_msg_payload_eta: AXIOM FORALL (payload?_var: (payload?)): payload(value(payload?_var)) = payload?_var; unified_msg_stage_source_error: AXIOM FORALL (source_error1_var: nat): stage(source_error(source_error1_var)) = source_error1_var; unified_msg_value_payload: AXIOM FORALL (payload1_var: T): value(payload(payload1_var)) = payload1_var; unified_msg_inclusive: AXIOM FORALL (unified_msg_var: unified_msg): receive_error?(unified_msg_var) OR no_majority?(unified_msg_var) OR source_error?(unified_msg_var) OR payload?(unified_msg_var); unified_msg_induction: AXIOM FORALL (p: [unified_msg -> boolean]): (p(receive_error) AND p(no_majority) AND (FORALL (source_error1_var: nat): p(source_error(source_error1_var))) AND (FORALL (payload1_var: T): p(payload(payload1_var)))) IMPLIES (FORALL (unified_msg_var: unified_msg): p(unified_msg_var)); every(p: PRED[T])(a: unified_msg): boolean = CASES a OF receive_error: TRUE, no_majority: TRUE, source_error(source_error1_var): TRUE, payload(payload1_var): p(payload1_var) ENDCASES; every(p: PRED[T], a: unified_msg): boolean = CASES a OF receive_error: TRUE, no_majority: TRUE, source_error(source_error1_var): TRUE, payload(payload1_var): p(payload1_var) ENDCASES; some(p: PRED[T])(a: unified_msg): boolean = CASES a OF receive_error: FALSE, no_majority: FALSE, source_error(source_error1_var): FALSE, payload(payload1_var): p(payload1_var) ENDCASES; some(p: PRED[T], a: unified_msg): boolean = CASES a OF receive_error: FALSE, no_majority: FALSE, source_error(source_error1_var): FALSE, payload(payload1_var): p(payload1_var) ENDCASES; subterm(x, y: unified_msg): boolean = x = y; <<: (well_founded?[unified_msg]) = LAMBDA (x, y: unified_msg): FALSE; unified_msg_well_founded: AXIOM well_founded?[unified_msg](<<); reduce_nat(receive_error?_fun, no_majority?_fun: nat, source_error?_fun: [nat -> nat], payload?_fun: [T -> nat]): [unified_msg -> nat] = LAMBDA (unified_msg_adtvar: unified_msg): LET red: [unified_msg -> nat] = reduce_nat(receive_error?_fun, no_majority?_fun, source_error?_fun, payload?_fun) IN CASES unified_msg_adtvar OF receive_error: receive_error?_fun, no_majority: no_majority?_fun, source_error(source_error1_var): source_error?_fun(source_error1_var), payload(payload1_var): payload?_fun(payload1_var) ENDCASES; REDUCE_nat(receive_error?_fun, no_majority?_fun: [unified_msg -> nat], source_error?_fun: [[nat, unified_msg] -> nat], payload?_fun: [[T, unified_msg] -> nat]): [unified_msg -> nat] = LAMBDA (unified_msg_adtvar: unified_msg): LET red: [unified_msg -> nat] = REDUCE_nat(receive_error?_fun, no_majority?_fun, source_error?_fun, payload?_fun) IN CASES unified_msg_adtvar OF receive_error: receive_error?_fun(unified_msg_adtvar), no_majority: no_majority?_fun(unified_msg_adtvar), source_error(source_error1_var): source_error?_fun(source_error1_var, unified_msg_adtvar), payload(payload1_var): payload?_fun(payload1_var, unified_msg_adtvar) ENDCASES; reduce_ordinal(receive_error?_fun, no_majority?_fun: ordinal, source_error?_fun: [nat -> ordinal], payload?_fun: [T -> ordinal]): [unified_msg -> ordinal] = LAMBDA (unified_msg_adtvar: unified_msg): LET red: [unified_msg -> ordinal] = reduce_ordinal(receive_error?_fun, no_majority?_fun, source_error?_fun, payload?_fun) IN CASES unified_msg_adtvar OF receive_error: receive_error?_fun, no_majority: no_majority?_fun, source_error(source_error1_var): source_error?_fun(source_error1_var), payload(payload1_var): payload?_fun(payload1_var) ENDCASES; REDUCE_ordinal(receive_error?_fun, no_majority?_fun: [unified_msg -> ordinal], source_error?_fun: [[nat, unified_msg] -> ordinal], payload?_fun: [[T, unified_msg] -> ordinal]): [unified_msg -> ordinal] = LAMBDA (unified_msg_adtvar: unified_msg): LET red: [unified_msg -> ordinal] = REDUCE_ordinal(receive_error?_fun, no_majority?_fun, source_error?_fun, payload?_fun) IN CASES unified_msg_adtvar OF receive_error: receive_error?_fun(unified_msg_adtvar), no_majority: no_majority?_fun(unified_msg_adtvar), source_error(source_error1_var): source_error?_fun(source_error1_var, unified_msg_adtvar), payload(payload1_var): payload?_fun(payload1_var, unified_msg_adtvar) ENDCASES; END unified_msg_adt unified_msg_adt_map[T: TYPE+, T1: TYPE+]: THEORY BEGIN ASSUMING T_TCC1: ASSUMPTION EXISTS (x: T): TRUE; T1_TCC1: ASSUMPTION EXISTS (x: T1): TRUE; ENDASSUMING IMPORTING unified_msg_adt map(f: [T -> T1])(a: unified_msg[T]): unified_msg[T1] = CASES a OF receive_error: receive_error, no_majority: no_majority, source_error(source_error1_var): source_error(source_error1_var), payload(payload1_var): payload(f(payload1_var)) ENDCASES; map(f: [T -> T1], a: unified_msg[T]): unified_msg[T1] = CASES a OF receive_error: receive_error, no_majority: no_majority, source_error(source_error1_var): source_error(source_error1_var), payload(payload1_var): payload(f(payload1_var)) ENDCASES; every(R: [[T, T1] -> boolean])(x: unified_msg[T], y: unified_msg[T1]): boolean = receive_error?(x) AND receive_error?(y) OR no_majority?(x) AND no_majority?(y) OR source_error?(x) AND source_error?(y) AND stage(x) = stage(y) OR payload?(x) AND payload?(y) AND R(value(x), value(y)); END unified_msg_adt_map unified_msg_adt_reduce[T: TYPE+, range: TYPE]: THEORY BEGIN ASSUMING T_TCC1: ASSUMPTION EXISTS (x: T): TRUE; ENDASSUMING IMPORTING unified_msg_adt[T] reduce(receive_error?_fun, no_majority?_fun: range, source_error?_fun: [nat -> range], payload?_fun: [T -> range]): [unified_msg -> range] = LAMBDA (unified_msg_adtvar: unified_msg): LET red: [unified_msg -> range] = reduce(receive_error?_fun, no_majority?_fun, source_error?_fun, payload?_fun) IN CASES unified_msg_adtvar OF receive_error: receive_error?_fun, no_majority: no_majority?_fun, source_error(source_error1_var): source_error?_fun(source_error1_var), payload(payload1_var): payload?_fun(payload1_var) ENDCASES; REDUCE(receive_error?_fun, no_majority?_fun: [unified_msg -> range], source_error?_fun: [[nat, unified_msg] -> range], payload?_fun: [[T, unified_msg] -> range]): [unified_msg -> range] = LAMBDA (unified_msg_adtvar: unified_msg): LET red: [unified_msg -> range] = REDUCE(receive_error?_fun, no_majority?_fun, source_error?_fun, payload?_fun) IN CASES unified_msg_adtvar OF receive_error: receive_error?_fun(unified_msg_adtvar), no_majority: no_majority?_fun(unified_msg_adtvar), source_error(source_error1_var): source_error?_fun(source_error1_var, unified_msg_adtvar), payload(payload1_var): payload?_fun(payload1_var, unified_msg_adtvar) ENDCASES; END unified_msg_adt_reduce $$$unified_msg.pvs %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % SPIDER version 2 % % PVS : Version 3.1 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% unified_msg[T:NONEMPTY_TYPE]: DATATYPE BEGIN receive_error : receive_error? no_majority : no_majority? source_error(stage: nat): source_error? payload(value: T) : payload? END unified_msg $$$unified_order.pvs unified_order[T: TYPE+, leq: (total_order?[T])]: THEORY BEGIN IMPORTING unified_msg[T] msg1, msg2: VAR unified_msg <=(msg1, msg2): bool = CASES msg1 OF receive_error : TRUE, no_majority: NOT receive_error?(msg2), source_error(i): CASES msg2 OF receive_error : FALSE, no_majority : FALSE, source_error(j): i <= j, payload(v) : TRUE ENDCASES, payload(v1) : CASES msg2 OF payload(v2): leq(v1, v2) ELSE FALSE ENDCASES ENDCASES le_total: JUDGEMENT <= HAS_TYPE (total_order?[unified_msg[T]]) END unified_order $$$unified_order.prf (unified_order (le_total 0 (le_total-1 nil 3292250856 3292255249 ("" (expand "total_order?") (("" (split) (("1" (expand "partial_order?") (("1" (split) (("1" (expand "preorder?") (("1" (split) (("1" (expand "reflexive?") (("1" (induct "x") (("1" (expand "<=") (("1" (propax) nil nil)) nil) ("2" (expand "<=") (("2" (propax) nil nil)) nil) ("3" (expand "<=") (("3" (propax) nil nil)) nil) ("4" (expand "<=") (("4" (skosimp*) (("4" (typepred "leq") (("4" (expand "total_order?") (("4" (expand "partial_order?") (("4" (expand "preorder?") (("4" (expand "reflexive?") (("4" (flatten) (("4" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "transitive?") (("2" (induct "x") (("1" (expand "<=") (("1" (propax) nil nil)) nil) ("2" (skosimp*) (("2" (expand "<=") (("2" (lift-if) (("2" (assert) (("2" (lift-if) (("2" (assert) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (expand "<=") (("3" (assert) (("3" (lift-if) (("3" (lift-if) (("3" (assert) (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (expand "<=") (("4" (lift-if) (("4" (assert) (("4" (lift-if) (("4" (assert) (("4" (ground) (("4" (typepred "leq") (("4" (expand "total_order?") (("4" (expand "partial_order?") (("4" (expand "preorder?") (("4" (expand "transitive?") (("4" (flatten) (("4" (inst?) (("4" (assert) (("4" (inst - "value(y!1)") (("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" (expand "antisymmetric?") (("2" (induct "x") (("1" (skosimp*) (("1" (expand "<=") (("1" (lift-if) (("1" (assert) (("1" (lift-if) (("1" (assert) (("1" (lift-if) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "<=") (("2" (lift-if) (("2" (assert) (("2" (lift-if) (("2" (assert) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (expand "<=") (("3" (lift-if) (("3" (lift-if) (("3" (assert) (("3" (lift-if) (("3" (assert) (("3" (ground) (("3" (use "unified_msg_source_error_extensionality") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (expand "<=") (("4" (lift-if) (("4" (assert) (("4" (lift-if) (("4" (assert) (("4" (lift-if) (("4" (assert) (("4" (ground) (("4" (typepred "leq") (("4" (expand "total_order?") (("4" (use "unified_msg_payload_extensionality") (("4" (assert) (("4" (expand "partial_order?") (("4" (expand "antisymmetric?") (("4" (flatten) (("4" (inst?) (("4" (assert) 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 "dichotomous?") (("2" (induct "x") (("1" (expand "<=") (("1" (propax) nil nil)) nil) ("2" (expand "<=") (("2" (skosimp*) (("2" (lift-if) (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (expand "<=") (("3" (lift-if) (("3" (assert) (("3" (lift-if) (("3" (assert) (("3" (lift-if) (("3" (assert) (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (skosimp*) (("4" (expand "<=") (("4" (assert) (("4" (lift-if) (("4" (assert) (("4" (lift-if) (("4" (assert) (("4" (lift-if) (("4" (assert) (("4" (ground) (("4" (typepred "leq") (("4" (expand "total_order?") (("4" (expand "dichotomous?") (("4" (flatten) (("4" (inst?) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) proved ((<= const-decl "bool" unified_order nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (unified_msg type-decl nil unified_msg_adt nil) (unified_msg_induction formula-decl nil unified_msg_adt nil) (T formal-nonempty-type-decl nil unified_order nil) (leq formal-const-decl "(total_order?[T])" unified_order nil) (pred type-eq-decl nil defined_types nil) (NOT const-decl "[bool -> bool]" booleans nil) (reflexive? const-decl "bool" relations nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (value adt-accessor-decl "[(payload?) -> T]" unified_msg_adt nil) (payload? adt-recognizer-decl "[unified_msg -> boolean]" unified_msg_adt nil) (transitive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (= const-decl "[T, T -> boolean]" equalities nil) (source_error? adt-recognizer-decl "[unified_msg -> boolean]" unified_msg_adt nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (source_error adt-constructor-decl "[nat -> (source_error?)]" unified_msg_adt nil) (unified_msg_source_error_extensionality formula-decl nil unified_msg_adt nil) (unified_msg_payload_extensionality formula-decl nil unified_msg_adt nil) (payload adt-constructor-decl "[T -> (payload?)]" unified_msg_adt nil) (antisymmetric? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (dichotomous? const-decl "bool" orders nil) (total_order? const-decl "bool" orders nil)) 493475 28640 t shostak)))