Quelle majority_vote.prf Sprache: Lisp

(majority_vote
(maj_size 0
  (maj_size-1 nil 3286722380
   ("" (skosimp*)
    (("" (use "card_purge_extract")
      (("" (replace - :hide? t)
        (("" (use "card_extract_bag")
          (("" (replace - :hide? t)
            (("" (use "minus_add")
              (("" (replace - :hide? t)
                (("" (use "distributive")
                  (("" (replace - :hide? t)
                    (("" (expand ">")
                      (("" (lemma "both_sides_minus_lt1")
                        ((""
                          (inst - "(2 * card(A!1)) + (2 * -A!1(v!1))"
                           "card(A!1)" "(2 * -A!1(v!1))")
                          (("" (assert) nil))))))))))))))))))))))))
    nil)
   ((card_purge_extract formula-decl nil finite_bags nil)
    (T formal-nonempty-type-decl nil majority_vote nil)
    (finite_bag type-eq-decl nil finite_bags nil)
    (is_finite const-decl "bool" finite_bags nil)
    (bag type-eq-decl nil bags 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)
    (card_extract_bag formula-decl nil finite_bags nil)
    (minus_add formula-decl nil number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (card const-decl "nat" finite_bags nil)
    (distributive formula-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (> const-decl "bool" reals nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (even_plus_even_is_even application-judgement "even_int" integers
     nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (both_sides_minus_lt1 formula-decl nil real_props nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil))
(maj_single_or_empty 0
  (maj_single_or_empty-1 nil 3286722397
   ("" (skosimp*)
    (("" (expand "empty?")
      (("" (skosimp*)
        (("" (expand "member")
          (("" (expand "maj?")
            (("" (expand "singleton?")
              (("" (inst?)
                (("" (skosimp*)
                  (("" (typepred! "y!1")
                    (("" (lemma "card_geq_count_add")
                      (("" (inst - "A!1" "x!1" "y!1")
                        (("" (assert) nil))))))))))))))))))))))
    nil)
   ((empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (singleton? const-decl "bool" sets nil)
    (card_geq_count_add formula-decl nil finite_bags nil)
    (NOT const-decl "[bool -> bool]" booleans 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-nonempty-type-decl nil majority_vote 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)
    (bag type-eq-decl nil bags nil)
    (is_finite const-decl "bool" finite_bags nil)
    (finite_bag type-eq-decl nil finite_bags nil)
    (A!1 skolem-const-decl "finite_bag[T]" majority_vote nil)
    (x!1 skolem-const-decl "T" majority_vote nil)
    (card const-decl "nat" finite_bags nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (maj? const-decl "bool" majority_vote nil))
   nil))
(maj_unique 0
  (maj_unique-1 nil 3286722448
   ("" (skosimp*)
    (("" (expand "maj")
      (("" (lift-if)
        (("" (split)
          (("1" (flatten) (("1" (grind) nil nil)) nil)
           ("2" (flatten)
            (("2" (use "maj_single_or_empty")
              (("2" (split)
                (("1" (case "singleton(v!1) = maj?(A!1)")
                  (("1" (use "choose_singleton")
                    (("1" (lemma "choose_is_epsilon[T]")
                      (("1" (inst?) (("1" (replace*) nil nil)) nil))
                      nil))
                    nil)
                   ("2" (expand "singleton?")
                    (("2" (skosimp*)
                      (("2" (inst-cp - "epsilon(maj?(A!1))")
                        (("1" (inst - "v!1") (("1" (replace*) nil nil))
                          nil)
                         ("2" (use "epsilon_ax[T]")
                          (("2" (split)
                            (("1" (propax) nil nil)
                             ("2" (inst + "v!1") nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (propax) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((maj const-decl "T" majority_vote nil)
    (nil application-judgement "nat" majority_vote nil)
    (nil application-judgement "nonneg_real" majority_vote nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nil application-judgement "finite_set" majority_vote nil)
    (T formal-nonempty-type-decl nil majority_vote nil)
    (bag_to_set const-decl "set[T]" bags_to_sets nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (card const-decl "nat" finite_bags nil)
    (maj? const-decl "bool" majority_vote nil)
    (maj_single_or_empty formula-decl nil majority_vote nil)
    (finite_bag type-eq-decl nil finite_bags nil)
    (is_finite const-decl "bool" finite_bags nil)
    (bag type-eq-decl nil bags 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)
    (singleton const-decl "(singleton?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (set type-eq-decl nil sets nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" majority_vote nil)
    (choose_is_epsilon formula-decl nil sets nil)
    (nonempty? const-decl "bool" sets nil)
    (choose_singleton formula-decl nil sets_lemmas nil)
    (epsilon_ax formula-decl nil epsilons nil)
    (v!1 skolem-const-decl "T" majority_vote nil)
    (epsilon const-decl "T" epsilons nil)
    (pred type-eq-decl nil defined_types nil)
    (A!1 skolem-const-decl "finite_bag[T]" majority_vote nil))
   nil))
(maj_pigeonhole 0
  (maj_pigeonhole-1 nil 3286906485
   ("" (skosimp*)
    (("" (lemma "maj_unique")
      (("" (inst - "A!1" _)
        (("" (inst-cp - "v!1")
          (("" (inst - "i!1") (("" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((maj_unique formula-decl nil majority_vote nil)
    (finite_bag type-eq-decl nil finite_bags nil)
    (is_finite const-decl "bool" finite_bags nil)
    (bag type-eq-decl nil bags 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)
    (T formal-nonempty-type-decl nil majority_vote nil))
   shostak))
(maj_is_extraction 0
  (maj_is_extraction-1 nil 3286722458
   ("" (skosimp*)
    (("" (decompose-equality +)
      (("" (expand "maj?")
        (("" (iff)
          (("" (prop)
            (("1" (expand "bag_to_set")
              (("1" (expand "extract")
                (("1" (lift-if)
                  (("1" (split)
                    (("1" (flatten) (("1" (assert) nil)))
                     ("2" (flatten)
                      (("2" (lemma "card_geq_count_add")
                        (("2" (inst - "A!1" "x!1" "v!1")
                          (("2" (assert) nil)))))))))))))))
             ("2" (expand "bag_to_set")
              (("2" (expand "extract")
                (("2" (lift-if)
                  (("2" (split)
                    (("1" (flatten)
                      (("1" (replace -) (("1" (propax) nil)))))
                     ("2" (flatten)
                      (("2" (assert) nil))))))))))))))))))))
    nil)
   ((nil application-judgement "finite_bag[T]" majority_vote nil)
    (nil application-judgement "finite_set" majority_vote 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (bag type-eq-decl nil bags nil)
    (is_finite const-decl "bool" finite_bags nil)
    (finite_bag type-eq-decl nil finite_bags nil)
    (maj? const-decl "bool" majority_vote nil)
    (set type-eq-decl nil sets nil)
    (bag_to_set const-decl "set[T]" bags_to_sets nil)
    (extract const-decl "bag" bags nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil majority_vote nil)
    (card_geq_count_add formula-decl nil finite_bags nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil))
   nil)))

quality100%

¤ Dauer der Verarbeitung: 0.13 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.