| products/Sources/formale Sprachen/PVS/fault_tolerance/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: real_finite_sequences.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(real_finite_sequences
(diameter?_TCC1 0 (diameter?_TCC1-1 nil 3403446511 ("" (skosimp*) (("" (use "min_le_max") (("" (assert) nil nil)) nil)) nil) ((min_le_max formula-decl nil ordered_finite_sequences 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) (ne_seqs type-eq-decl nil seqs "structures/") (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (min_in_consensus name-judgement "in_consensus_function" real_finite_sequences nil) (max_in_consensus name-judgement "in_consensus_function" real_finite_sequences nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil)) nil)) (agreement_propagation 0 (agreement_propagation-1 nil 3403444832 ("" (skosimp*) (("" (assert) nil nil)) nil) ((min_in_consensus name-judgement "in_consensus_function" real_finite_sequences nil) (max_in_consensus name-judgement "in_consensus_function" real_finite_sequences nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (similar?_TCC1 0 (similar?_TCC1-1 nil 3403444810 ("" (subtype-tcc) nil 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) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finite_sequence type-eq-decl nil finite_sequences nil) (ne_seqs type-eq-decl nil seqs "structures/") (below 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 "bool" reals nil)) nil)) (similar_sort_TCC1 0 (similar_sort_TCC1-1 nil 3403475520 ("" (subtype-tcc) nil nil) ((similar? const-decl "bool" real_finite_sequences 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) (sort_length formula-decl nil sort_seq "structures/")) nil)) (similar_sort_TCC2 0 (similar_sort_TCC2-1 nil 3403475520 ("" (subtype-tcc) nil nil) ((similar? const-decl "bool" real_finite_sequences 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) (sort_length formula-decl nil sort_seq "structures/")) nil)) (similar_sort 0 (similar_sort-1 nil 3403482273 ("" (skosimp*) (("" (expand "similar?") (("" (flatten) (("" (assert) (("" (skosimp*) (("" (lemma "sort_overlap") (("" (inst?) (("" (assert) (("" (inst - "s2!1") (("" (inst?) (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) (("2" (typepred "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((similar? const-decl "bool" real_finite_sequences nil) (sort_length formula-decl nil sort_seq "structures/") (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) (sort_overlap formula-decl nil ordered_finite_sequences nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (s2!1 skolem-const-decl "ne_seqs[real]" real_finite_sequences nil) (i!1 skolem-const-decl "below(sort(s1!1)`length)" real_finite_sequences nil) (below type-eq-decl nil naturalnumbers nil) (s1!1 skolem-const-decl "ne_seqs[real]" real_finite_sequences nil) (sort const-decl "{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}" sort_seq "structures/") (increasing? const-decl "bool" sort_seq "structures/") (permutation? const-decl "bool" permutations_seq "structures/") (AND const-decl "[bool, bool -> bool]" booleans nil) (seqs type-eq-decl nil sort_seq "structures/") (< const-decl "bool" reals nil) (NOT const-decl "[bool -> bool]" booleans nil) (ne_seqs type-eq-decl nil seqs "structures/") (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-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) (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_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (sum_TCC1 0 (sum_TCC1-1 nil 3403444810 ("" (subtype-tcc) nil nil) nil nil)) (sum_TCC2 0 (sum_TCC2-1 nil 3403444810 ("" (subtype-tcc) nil nil) nil nil)) (sum_TCC3 0 (sum_TCC3-1 nil 3403449216 ("" (assuming-tcc) nil 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) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finite_sequence type-eq-decl nil finite_sequences nil) (ne_seqs type-eq-decl nil seqs "structures/") (< 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) (below type-eq-decl nil naturalnumbers nil) (integer nonempty-type-from-decl nil integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (sum_lower 0 (sum_lower-1 nil 3403449837 ("" (skosimp* t) (("" (use "max_seq_in?") (("" (expand "in?") (("" (skosimp*) (("" (replace -1 :hide? t) (("" (expand "sum") (("" (lemma "sigma_middle[below(s!1`length)]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (replace -1 :hide? t) (("1" (move-terms 1 r 1) (("1" (assert) (("1" (lemma "sigma_le[below(s!1`length)]") (("1" (inst-cp - "(lambda (i: below(s!1`length)): min(s!1))" "s!1" "ii!1 - 1" 0) (("1" (use "sigma_const[below(s!1`length)]") (("1" (replace -1 :hide? t) (("1" (inst - "(lambda (i: below(s!1`length)): min(s!1))" "s!1" "s!1`length - 1" "ii!1 + 1") (("1" (expand "finseq_appl") (("1" (use "sigma_const[below(s!1`length)]") (("1" (replace -1 :hide? t) (("1" (assert) (("1" (split -1) (("1" (split -2) (("1" (lift-if) (("1" (ground) nil nil)) nil) ("2" (skosimp*) (("2" (use "min_seq_lem") nil nil)) nil)) nil) ("2" (skosimp*) (("2" (use "min_seq_lem") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (inst + "ii!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((<= const-decl "bool" reals nil) (max_seq_in? formula-decl nil max_seq "structures/") (sum const-decl "real" real_finite_sequences nil) (real_plus_real_is_real application-judgement "real" reals nil) (T_low type-eq-decl nil sigma "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (T_high type-eq-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (sigma def-decl "real" sigma "reals/") (min const-decl "{t: T | (FORALL (ii: dom(s)): t <= seq(s)(ii)) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (dom type-eq-decl nil min_seq "structures/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (sigma_le formula-decl nil sigma "reals/") (sigma_const formula-decl nil sigma "reals/") (int_plus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (s!1 skolem-const-decl "ne_seqs[real]" real_finite_sequences nil) (ii!1 skolem-const-decl "below(length(s!1))" real_finite_sequences nil) (sigma_0_neg formula-decl nil sigma_below "reals/") (subrange type-eq-decl nil integers nil) (min_seq_lem formula-decl nil min_seq "structures/") (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (finseq type-eq-decl nil finite_sequences nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (min_in_consensus name-judgement "in_consensus_function" real_finite_sequences nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (integer nonempty-type-from-decl nil integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (sigma_middle formula-decl nil sigma "reals/") (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) (below type-eq-decl nil naturalnumbers nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (in? const-decl "bool" seqs "structures/") (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) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finite_sequence type-eq-decl nil finite_sequences nil) (ne_seqs type-eq-decl nil seqs "structures/")) nil)) (sum_upper 0 (sum_upper-1 nil 3403450918 ("" (skosimp* t) (("" (use "min_seq_in?") (("" (expand "in?") (("" (skosimp*) (("" (replace -1 :hide? t) (("" (expand "sum") (("" (lemma "sigma_middle[below(s!1`length)]") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (replace -1 :hide? t) (("1" (move-terms 1 r 1) (("1" (assert) (("1" (lemma "sigma_le[below(s!1`length)]") (("1" (inst-cp - "s!1`seq" "(lambda (i: below(s!1`length)): max(s!1))" "ii!1 - 1" 0) (("1" (use "sigma_const[below(s!1`length)]") (("1" (replace -1 :hide? t) (("1" (inst - "s!1`seq" "(lambda (i: below(s!1`length)): max(s!1))" "s!1`length - 1" "ii!1 + 1") (("1" (assert) (("1" (use "sigma_const[below(s!1`length)]") (("1" (replace -1 :hide? t) (("1" (assert) (("1" (split -1) (("1" (split -2) (("1" (lift-if) (("1" (ground) nil nil)) nil) ("2" (skosimp*) (("2" (use "max_seq_lem") nil nil)) nil)) nil) ("2" (skosimp*) (("2" (use "max_seq_lem") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (inst + "ii!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((<= const-decl "bool" reals nil) (min_seq_in? formula-decl nil min_seq "structures/") (sum const-decl "real" real_finite_sequences nil) (real_plus_real_is_real application-judgement "real" reals nil) (T_low type-eq-decl nil sigma "reals/") (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (T_high type-eq-decl nil sigma "reals/") (OR const-decl "[bool, bool -> bool]" booleans nil) (max const-decl "{t: T | (FORALL (ii: dom(s)): seq(s)(ii) <= t) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" max_seq "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (dom type-eq-decl nil max_seq "structures/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (sigma def-decl "real" sigma "reals/") (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (sigma_le formula-decl nil sigma "reals/") (sigma_const formula-decl nil sigma "reals/") (int_plus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (s!1 skolem-const-decl "ne_seqs[real]" real_finite_sequences nil) (ii!1 skolem-const-decl "below(length(s!1))" real_finite_sequences nil) (sigma_0_neg formula-decl nil sigma_below "reals/") (subrange type-eq-decl nil integers nil) (max_seq_lem formula-decl nil max_seq "structures/") (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (max_in_consensus name-judgement "in_consensus_function" real_finite_sequences nil) (integer nonempty-type-from-decl nil integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (sigma_middle formula-decl nil sigma "reals/") (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) (below type-eq-decl nil naturalnumbers nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (in? const-decl "bool" seqs "structures/") (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) (> const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finite_sequence type-eq-decl nil finite_sequences nil) (ne_seqs type-eq-decl nil seqs "structures/")) nil)) (mean_TCC1 0 (mean_TCC1-1 nil 3403444810 ("" (subtype-tcc) nil nil) nil nil)) (min_le_mean 0 (min_le_mean-1 nil 3403454558 ("" (skosimp*) (("" (expand "mean") (("" (cross-mult) (("" (use "sum_lower") (("" (use "min_le_max") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((mean const-decl "real" real_finite_sequences nil) (sum_lower formula-decl nil real_finite_sequences nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (max_in_consensus name-judgement "in_consensus_function" real_finite_sequences nil) (min_le_max formula-decl nil ordered_finite_sequences nil) (min_in_consensus name-judgement "in_consensus_function" real_finite_sequences nil) (real_times_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finite_sequence type-eq-decl nil finite_sequences nil) (ne_seqs type-eq-decl nil seqs "structures/") (AND const-decl "[bool, bool -> bool]" booleans 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) (dom type-eq-decl nil min_seq "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (min const-decl "{t: T | (FORALL (ii: dom(s)): t <= seq(s)(ii)) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq "structures/") (sum const-decl "real" real_finite_sequences nil) (div_mult_pos_le2 formula-decl nil real_props nil)) shostak)) (mean_le_max 0 (mean_le_max-1 nil 3403454625 ("" (skosimp*) (("" (expand "mean") (("" (cross-mult) (("" (use "sum_upper") (("" (use "min_le_max") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((mean const-decl "real" real_finite_sequences nil) (sum_upper formula-decl nil real_finite_sequences nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (min_in_consensus name-judgement "in_consensus_function" real_finite_sequences nil) (min_le_max formula-decl nil ordered_finite_sequences nil) (max_in_consensus name-judgement "in_consensus_function" real_finite_sequences nil) (real_times_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (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) (nonneg_real nonempty-type-eq-decl nil real_types nil) (> const-decl "bool" reals nil) (posreal nonempty-type-eq-decl nil real_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finite_sequence type-eq-decl nil finite_sequences nil) (ne_seqs type-eq-decl nil seqs "structures/") (AND const-decl "[bool, bool -> bool]" booleans 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) (dom type-eq-decl nil max_seq "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (max const-decl "{t: T | (FORALL (ii: dom(s)): seq(s)(ii) <= t) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" max_seq "structures/") (sum const-decl "real" real_finite_sequences nil) (div_mult_pos_le1 formula-decl nil real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil)) shostak)) (midpoint_def 0 (midpoint_def-1 nil 3403448305 ("" (auto-rewrite-defs) (("" (skosimp*) (("" (assert) nil nil)) nil)) nil) ((length def-decl "nat" list_props nil) (list2finseq const-decl "finseq[T]" list2finseq 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) (minmax const-decl "ne_seqs" ordered_finite_sequences nil) (nth def-decl "T" list_props nil) (sigma def-decl "real" sigma "reals/") (sum const-decl "real" real_finite_sequences nil) (mean const-decl "real" real_finite_sequences nil) (midpoint const-decl "real" real_finite_sequences nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (max_in_consensus name-judgement "in_consensus_function" real_finite_sequences nil) (min_in_consensus name-judgement "in_consensus_function" real_finite_sequences nil)) shostak)) (mean_lower 0 (mean_lower-1 nil 3403445214 ("" (skosimp* t) (("" (expand "mean") (("" (use "sum_lower") (("" (cross-mult) (("" (mult-by -1 "k!1") (("" (mult-by -4 "max(s!1) - min(s!1)" *) (("" (assert) (("" (prop) (("" (use "min_le_max") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((mean const-decl "real" real_finite_sequences nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (div_mult_pos_le1 formula-decl nil real_props nil) (min const-decl "{t: T | (FORALL (ii: dom(s)): t <= seq(s)(ii)) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq "structures/") (dom type-eq-decl nil min_seq "structures/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (max const-decl "{t: T | (FORALL (ii: dom(s)): seq(s)(ii) <= t) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" max_seq "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (dom type-eq-decl nil max_seq "structures/") (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (sum const-decl "real" real_finite_sequences nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (times_div2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_mult_pos_le2 formula-decl nil real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (max_in_consensus name-judgement "in_consensus_function" real_finite_sequences nil) (min_in_consensus name-judgement "in_consensus_function" real_finite_sequences nil) (both_sides_times_pos_neg_le1_imp formula-decl nil extra_real_props nil) (min_le_max formula-decl nil ordered_finite_sequences nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (sum_lower formula-decl nil real_finite_sequences 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) (> 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) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finite_sequence type-eq-decl nil finite_sequences nil) (ne_seqs type-eq-decl nil seqs "structures/")) nil)) (mean_upper 0 (mean_upper-1 nil 3403445347 ("" (skosimp* t) (("" (expand "mean") (("" (use "sum_upper") (("" (cross-mult) (("" (mult-by -1 "k!1") (("" (mult-by -4 "max(s!1) - min(s!1)" *) (("" (use "min_le_max") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((mean const-decl "real" real_finite_sequences nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (div_mult_pos_le1 formula-decl nil real_props nil) (sum const-decl "real" real_finite_sequences nil) (max const-decl "{t: T | (FORALL (ii: dom(s)): seq(s)(ii) <= t) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" max_seq "structures/") (dom type-eq-decl nil max_seq "structures/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (min const-decl "{t: T | (FORALL (ii: dom(s)): t <= seq(s)(ii)) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (dom type-eq-decl nil min_seq "structures/") (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (numfield nonempty-type-eq-decl nil number_fields nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (min_in_consensus name-judgement "in_consensus_function" real_finite_sequences nil) (max_in_consensus name-judgement "in_consensus_function" real_finite_sequences nil) (times_div2 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_mult_pos_le2 formula-decl nil real_props nil) (both_sides_times_pos_neg_le1_imp formula-decl nil extra_real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (min_le_max formula-decl nil ordered_finite_sequences nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_times_real_is_real application-judgement "real" reals nil) (int_minus_int_is_int application-judgement "int" integers nil) (sum_upper formula-decl nil real_finite_sequences 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) (> 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) (posnat nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finite_sequence type-eq-decl nil finite_sequences nil) (ne_seqs type-eq-decl nil seqs "structures/")) nil)) (mean_consensus 0 (mean_consensus-1 nil 3403955090 ("" (skosimp*) (("" (use "min_le_mean") (("" (use "mean_le_max") (("" (assert) nil nil)) nil)) nil)) nil) ((min_le_mean formula-decl nil real_finite_sequences nil) (ne_seqs type-eq-decl nil seqs "structures/") (> const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (finite_sequence type-eq-decl nil finite_sequences 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) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (min_in_consensus name-judgement "in_consensus_function" real_finite_sequences nil) (max_in_consensus name-judgement "in_consensus_function" real_finite_sequences nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (mean_le_max formula-decl nil real_finite_sequences nil)) nil)) (midpoint_consensus 0 (midpoint_consensus-1 nil 3403955090 ("" (skosimp*) (("" (rewrite "midpoint_def") (("" (assert) (("" (use "min_le_max") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((midpoint_def formula-decl nil real_finite_sequences nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (bool nonempty-type-eq-decl nil booleans nil) (> const-decl "bool" reals nil) (ne_seqs type-eq-decl nil seqs "structures/") (max_in_consensus name-judgement "in_consensus_function" real_finite_sequences nil) (min_in_consensus name-judgement "in_consensus_function" real_finite_sequences nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (<= const-decl "bool" reals nil) (min_le_max formula-decl nil ordered_finite_sequences nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (inexact_min 0 (inexact_min-1 nil 3403466436 ("" (expand "inexact_consensus?") (("" (skosimp*) (("" (forward-chain "similar_sort") (("" (hide -2) (("" (expand "similar?") (("" (flatten) (("" (inst - 0) (("" (rewrite "sort_seq_min") (("" (rewrite "sort_seq_min") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sort_seq_min formula-decl nil sort_seq_lems "structures/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (min_in_consensus name-judgement "in_consensus_function" real_finite_sequences nil) (below type-eq-decl nil naturalnumbers nil) (sort const-decl "{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}" sort_seq "structures/") (increasing? const-decl "bool" sort_seq "structures/") (permutation? const-decl "bool" permutations_seq "structures/") (AND const-decl "[bool, bool -> bool]" booleans nil) (seqs type-eq-decl nil sort_seq "structures/") (<= const-decl "bool" reals 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) (sort_length formula-decl nil sort_seq "structures/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (similar? const-decl "bool" real_finite_sequences nil) (ne_seqs type-eq-decl nil seqs "structures/") (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (similar_sort formula-decl nil real_finite_sequences nil) (inexact_consensus? const-decl "bool" real_finite_sequences nil)) shostak)) (inexact_max 0 (inexact_max-1 nil 3403475661 ("" (expand "inexact_consensus?") (("" (skosimp*) (("" (forward-chain "similar_sort") (("" (expand "similar?") (("" (flatten) (("" (inst - "s1!1`length -1") (("" (rewrite "sort_seq_max") (("" (replace*) (("" (rewrite "sort_seq_max") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((similar? const-decl "bool" real_finite_sequences nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (sort_length formula-decl nil sort_seq "structures/") (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) (seqs type-eq-decl nil sort_seq "structures/") (AND const-decl "[bool, bool -> bool]" booleans nil) (permutation? const-decl "bool" permutations_seq "structures/") (increasing? const-decl "bool" sort_seq "structures/") (sort const-decl "{ss: seqs | permutation?[T, <=](s, ss) AND increasing?(ss)}" sort_seq "structures/") (below type-eq-decl nil naturalnumbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (max_in_consensus name-judgement "in_consensus_function" real_finite_sequences nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (sort_seq_max formula-decl nil sort_seq_lems "structures/") (ne_seqs type-eq-decl nil seqs "structures/") (> const-decl "bool" reals nil) (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (similar_sort formula-decl nil real_finite_sequences nil) (inexact_consensus? const-decl "bool" real_finite_sequences nil)) shostak)) (inexact_choose 0 (inexact_choose-1 nil 3403466574 ("" (expand "inexact_consensus?") (("" (expand "similar?") (("" (expand "choose") (("" (skosimp*) (("" (replace*) (("" (lift-if) (("" (assert) (("" (prop) (("1" (inst?) nil nil) ("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((similar? const-decl "bool" real_finite_sequences 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) (below type-eq-decl nil nat_types nil) (finite_sequence type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (ne_seqs type-eq-decl nil seqs "structures/") (below type-eq-decl nil naturalnumbers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (choose const-decl "T" finite_seqs nil) (inexact_consensus? const-decl "bool" real_finite_sequences nil)) shostak)) (inexact_mean 0 (inexact_mean-1 nil 3403454701 ("" (expand "inexact_consensus?") (("" (skosimp*) (("" (expand "similar?") (("" (flatten) (("" (expand "mean") (("" (replace*) (("" (expand "sum") (("" (replace*) (("" (same-name "sigma[below(s1!1`length)]" "sigma[below(s2!1`length)]") (("1" (replaces -1) (("1" (field 1) (("1" (rewrite "sigma_minus[below(s2!1`length)]") (("1" (lemma "sigma_bound[below(s2!1`length)]") (("1" (inst -1 "eps!1" "LAMBDA(i: below(s2!1`length)): s1!1`seq(i) - s2!1`seq(i)" "s2!1`length-1" "0") (("1" (assert) (("1" (skosimp*) (("1" (inst? -) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace*) (("2" (assert) nil nil)) nil) ("3" (skosimp*) (("3" (assert) nil nil)) nil) ("4" (skosimp*) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((sigma_minus formula-decl nil sigma "reals/") (s1!1 skolem-const-decl "ne_seqs[real]" real_finite_sequences nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma_bound formula-decl nil sigma "reals/") (minus_odd_is_odd application-judgement "odd_int" integers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_times_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (FDX_4 skolem-const-decl "nat" real_finite_sequences nil) (s2!1 skolem-const-decl "ne_seqs[real]" real_finite_sequences nil) (nnreal type-eq-decl nil real_types nil) (sigma def-decl "real" sigma "reals/") (T_high type-eq-decl nil sigma "reals/") (T_low type-eq-decl nil sigma "reals/") (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum 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_times_pos_le1 formula-decl nil real_props nil) (= const-decl "[T, T -> boolean]" equalities nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (/= const-decl "boolean" notequal nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_minus_real_is_real application-judgement "real" reals nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions 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) (IFF const-decl "[bool, bool -> bool]" booleans nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (finite_sequence type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (ne_seqs type-eq-decl nil seqs "structures/") (below type-eq-decl nil naturalnumbers nil) (integer nonempty-type-from-decl nil integers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (sum const-decl "real" real_finite_sequences nil) (mean const-decl "real" real_finite_sequences nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (similar? const-decl "bool" real_finite_sequences nil) (inexact_consensus? const-decl "bool" real_finite_sequences nil)) shostak)) (inexact_midpoint 0 (inexact_midpoint-1 nil 3403455580 ("" (expand "inexact_consensus?") (("" (skosimp*) (("" (rewrite "midpoint_def") (("" (rewrite "midpoint_def") (("" (use "inexact_min") (("" (use "inexact_max") (("" (expand "inexact_consensus?") (("" (inst?) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((inexact_max formula-decl nil real_finite_sequences nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (inexact_min formula-decl nil real_finite_sequences nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (min_in_consensus name-judgement "in_consensus_function" real_finite_sequences nil) (max_in_consensus name-judgement "in_consensus_function" real_finite_sequences nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (ne_seqs type-eq-decl nil seqs "structures/") (> const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (finite_sequence type-eq-decl nil finite_sequences 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) (below type-eq-decl nil nat_types nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (midpoint_def formula-decl nil real_finite_sequences nil) (inexact_consensus? const-decl "bool" real_finite_sequences nil)) shostak)) (mean_convergence 0 (mean_convergence-1 nil 3403448438 ("" (skosimp*) (("" (lemma "mean_upper") (("" (inst - "k!1" "s1!1") (("" (lemma "mean_lower") (("" (inst - "k!1" "s2!1") (("" (assert) (("" (mult-by -5 "(k!1 - 1)") (("" (isolate 1 r 1) (("" (cross-mult) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((mean_upper formula-decl nil real_finite_sequences nil) (mean_lower formula-decl nil real_finite_sequences nil) (nnreal_times_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_times_real_is_real application-judgement "real" reals nil) (real_div_nzreal_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (mean_consensus name-judgement "consensus_function" real_finite_sequences nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (min_in_consensus name-judgement "in_consensus_function" real_finite_sequences nil) (max_in_consensus name-judgement "in_consensus_function" real_finite_sequences nil) (real_minus_real_is_real application-judgement "real" reals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (mean const-decl "real" real_finite_sequences nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (posreal nonempty-type-eq-decl nil real_types nil) (div_mult_pos_le2 formula-decl nil real_props nil) (div_mult_pos_le1 formula-decl nil real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (nnreal type-eq-decl nil real_types nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (min const-decl "{t: T | (FORALL (ii: dom(s)): t <= seq(s)(ii)) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_seq "structures/") (dom type-eq-decl nil min_seq "structures/") (max const-decl "{t: T | (FORALL (ii: dom(s)): seq(s)(ii) <= t) AND (EXISTS (jj: dom(s)): seq(s)(jj) = t)}" max_seq "structures/") (= const-decl "[T, T -> boolean]" equalities nil) (dom type-eq-decl nil max_seq "structures/") (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (ne_seqs type-eq-decl nil seqs "structures/") (finite_sequence type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (nat nonempty-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) (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)) shostak)) (midpoint_convergence 0 (midpoint_convergence-1 nil 3403447904 ("" (skosimp*) (("" (expand "midpoint") (("" (rewrite "max_minmax" :dir rl) (("" (rewrite "min_minmax" :dir rl) (("" (lemma "mean_convergence") (("" (inst?) (("" (inst - 2) (("" (assert) (("" (rewrite "min_minmax") (("" (rewrite "max_minmax") (("" (assert) (("" (hide-all-but 1) (("" (expand "minmax") (("" (expand "list2finseq") (("" (expand "length") (("" (expand "length") (("" (expand "length") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((midpoint const-decl "real" real_finite_sequences nil) (min_minmax formula-decl nil ordered_finite_sequences nil) (min_in_consensus name-judgement "in_consensus_function" real_finite_sequences nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (minmax const-decl "ne_seqs" ordered_finite_sequences nil) (nnreal type-eq-decl nil real_types nil) (>= const-decl "bool" reals nil) (mean_consensus name-judgement "consensus_function" real_finite_sequences nil) (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal" real_types nil) (real_minus_real_is_real application-judgement "real" reals nil) (list2finseq const-decl "finseq[T]" list2finseq nil) (length def-decl "nat" list_props 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (mean_convergence formula-decl nil real_finite_sequences nil) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.45 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
