Quelle majority_seq.prf Sprache: Lisp

(majority_seq
(is_majority_TCC1 0
  (is_majority_TCC1-1 nil 3410692309
   ("" (skosimp*) (("" (rewrite "finite_below") nil)) nil)
   ((finite_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) (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (set type-eq-decl nil sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (T formal-nonempty-type-decl nil majority_seq nil)
    (finite_sequence type-eq-decl nil finite_sequences nil))
   nil))
(maj_TCC1 0
  (maj_TCC1-1 nil 3410692309
   (""
    (inst 1 "(LAMBDA (fs: finite_sequence[T]):
             IF maj_exists(fs) THEN
                choose({mv: T | is_majority(mv, fs)})
             ELSE
                epsilon({mv: T | TRUE})
             ENDIF)")
    (("1" (skosimp*) nil) ("2" (skosimp*) (("2" (assert) nil)))
     ("3" (skosimp*)
      (("3" (assert)
        (("3" (expand "nonempty?")
          (("3" (expand "empty?")
            (("3" (expand "maj_exists")
              (("3" (skosimp*)
                (("3" (inst -2 "mv!1")
                  (("3" (expand "member")
                    (("3" (propax) nil))))))))))))))))))
    nil)
   ((member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (TRUE const-decl "bool" booleans nil)
    (epsilon const-decl "T" epsilons nil)
    (pred type-eq-decl nil defined_types nil)
    (choose const-decl "(p)" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (is_majority const-decl "bool" majority_seq nil)
    (maj_exists const-decl "bool" majority_seq nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (T formal-nonempty-type-decl nil majority_seq nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   nil))
(is_majority_unique 0
  (is_majority_unique-1 nil 3410692309
   ("" (skosimp*)
    (("" (expand "is_majority")
      (("" (name "A" "{i: below(length(fs!1)) | seq(fs!1)(i) = mv1!1}")
        ((""
          (name "B" "{i: below(length(fs!1)) | seq(fs!1)(i) = mv2!1}")
          (("" (replace -1)
            (("" (hide -1)
              (("" (replace -1)
                (("" (hide -1)
                  (("" (case "disjoint?(A,B)")
                    (("1"
                      (lemma "card_disj_union[below(length(fs!1))]")
                      (("1" (inst?)
                        (("1" (assert)
                          (("1" (hide -2)
                            (("1"
                              (case "card(union(A, B)) <= length(fs!1)")
                              (("1"
                                (replace -2)
                                (("1"
                                  (hide -2 -3 -4 1)
                                  (("1" (assert) nil)))))
                               ("2"
                                (hide -1 -2 -3)
                                (("2" (rewrite "card_below") nil)))
                               ("3"
                                (lemma
                                 "finite_subset[below(length(fs!1))]")
                                (("3"
                                  (inst
                                   -1
                                   "{x: below(length(fs!1)) | TRUE}"
                                   "union[below(length(fs!1))](A, B)")
                                  (("1"
                                    (assert)
                                    (("1"
                                      (hide -1 -2 -3 -4 2 3)
                                      (("1"
                                        (expand "subset?")
                                        (("1"
                                          (expand "union")
                                          (("1"
                                            (expand "member")
                                            (("1"
                                              (propax)
                                              nil)))))))))))
                                   ("2"
                                    (rewrite "finite_below")
                                    nil)))))))))))
                         ("2" (reveal -3)
                          (("2" (hide -2 -3 -4 2)
                            (("2" (replace -1 1 rl)
                              (("2"
                                (hide -1)
                                (("2"
                                  (rewrite "finite_below")
                                  nil)))))))))
                         ("3" (rewrite "finite_below") nil)))))
                     ("2" (reveal -1 -2)
                      (("2" (hide -3 -4)
                        (("2" (replace -1 + rl)
                          (("2" (hide -1)
                            (("2" (replace -1 + rl)
                              (("2"
                                (hide -1)
                                (("2"
                                  (expand "disjoint?")
                                  (("2"
                                    (expand "intersection")
                                    (("2"
                                      (expand "empty?")
                                      (("2"
                                        (expand "member")
                                        (("2"
                                          (skosimp*)
                                          (("2"
                                            (assert)
                                            nil))))))))))))))))))))))))))))))))))))))))
    nil)
   ((is_majority const-decl "bool" majority_seq nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil)
    (card_disj_union formula-decl nil finite_sets 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)
    (<= const-decl "bool" reals 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)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (card_below formula-decl nil finite_sets_below "finite_sets/")
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (set type-eq-decl nil sets nil)
    (disjoint? 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)
    (below type-eq-decl nil nat_types nil)
    (T formal-nonempty-type-decl nil majority_seq nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (below type-eq-decl nil naturalnumbers nil)
    (= const-decl "[T, T -> boolean]" equalities nil))
   nil))
(maj_lem 0
  (maj_lem-1 nil 3410692309
   ("" (skosimp*)
    (("" (prop)
      (("1" (expand "maj_exists") (("1" (inst?) nil)))
       ("2" (typepred "maj(fs!1)")
        (("2" (split -1)
          (("1" (lemma "is_majority_unique")
            (("1" (inst -1 "fs!1" "mv!1" "maj(fs!1)")
              (("1" (assert) nil)))))
           ("2" (expand "maj_exists") (("2" (inst?) nil)))))))
       ("3" (typepred "maj(fs!1)") (("3" (assert) nil))))))
    nil)
   ((T formal-nonempty-type-decl nil majority_seq nil)
    (maj_exists const-decl "bool" majority_seq nil)
    (is_majority_unique formula-decl nil majority_seq nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans 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)
    (is_majority const-decl "bool" majority_seq nil)
    (maj const-decl "{mv | maj_exists(fs) => is_majority(mv, fs)}"
     majority_seq nil))
   nil))
(maj_subset 0
  (maj_subset-1 nil 3410692309
   ("" (skosimp*)
    (("" (expand "is_majority")
      ((""
        (case "subset?(A!1,{i: below(length(fs!1)) | seq(fs!1)(i) = mv!1})")
        (("1" (lemma "card_subset[below(length(fs!1))]")
          (("1" (inst?)
            (("1" (assert) nil) ("2" (rewrite "finite_below") nil)))))
         ("2" (hide -1 2)
          (("2" (expand "subset?")
            (("2" (skosimp*)
              (("2" (expand "member")
                (("2" (inst -2 "x!1")
                  (("2" (assert) nil))))))))))))))))
    nil)
   ((is_majority const-decl "bool" majority_seq nil)
    (member const-decl "bool" sets nil)
    (card_subset formula-decl nil finite_sets nil)
    (finite_below formula-decl nil finite_sets_below "finite_sets/")
    (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)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (mv!1 skolem-const-decl "T" majority_seq nil)
    (fs!1 skolem-const-decl "finite_sequence[T]" majority_seq 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)
    (T formal-nonempty-type-decl nil majority_seq nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (below type-eq-decl nil naturalnumbers nil)
    (set type-eq-decl nil sets nil)
    (subset? const-decl "bool" sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil))
   nil))
(maj_in_seq 0
  (maj_in_seq-1 nil 3410692309
   ("" (skosimp*)
    (("" (expand "in_seq")
      (("" (expand "is_majority")
        (("" (lemma "card_empty?[below(length(fs!1))]")
          (("" (inst?)
            (("1" (expand "empty?")
              (("1" (expand "member")
                (("1" (iff -1)
                  (("1" (flatten)
                    (("1" (split -1)
                      (("1" (assert) nil)
                       ("2" (split -1)
                        (("1" (propax) nil)
                         ("2" (skosimp*)
                          (("2" (inst 2 "x!1") nil)))))))))))))))
             ("2" (rewrite "finite_below") nil))))))))))
    nil)
   ((in_seq const-decl "bool" majority_seq nil)
    (below type-eq-decl nil naturalnumbers nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (T formal-nonempty-type-decl nil majority_seq nil)
    (below type-eq-decl nil nat_types 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)
    (card_empty? formula-decl nil finite_sets nil)
    (finite_below formula-decl nil finite_sets_below "finite_sets/")
    (empty? const-decl "bool" sets 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)
    (member const-decl "bool" sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (fs!1 skolem-const-decl "finite_sequence[T]" majority_seq nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (mv!1 skolem-const-decl "T" majority_seq nil)
    (is_majority const-decl "bool" majority_seq nil))
   nil))
(length_eq_1 0
  (length_eq_1-1 nil 3410692309
   ("" (skosimp*)
    (("" (lemma "maj_lem")
      (("" (inst -1 "(# length := 1, seq := f1!1 #)" "f1!1(0)")
        (("" (flatten)
          (("" (hide -2)
            (("" (assert)
              (("" (lemma "maj_lem")
                (("" (inst?)
                  (("" (flatten)
                    (("" (hide -2)
                      (("" (assert)
                        (("" (hide 2)
                          ((""
                            (case "length((# length := 1, seq := f1!1 #)) = 1")
                            (("1" (expand "is_majority")
                              (("1"
                                (lemma
                                 "card_below_fullset[length((# length := 1, seq := f1!1 #))]")
                                (("1"
                                  (expand "fullset")
                                  (("1"
                                    (replace -1)
                                    (("1" (assert) nil)))))))))
                             ("2" (assert)
                              nil))))))))))))))))))))))))))
    nil)
   ((maj_lem formula-decl nil majority_seq nil)
    (is_majority const-decl "bool" majority_seq nil)
    (fullset const-decl "set" sets 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)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (card_below_fullset formula-decl nil finite_sets_below
     "finite_sets/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (< const-decl "bool" reals 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)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (T formal-nonempty-type-decl nil majority_seq nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   nil))
(is_majority_const 0
  (is_majority_const-2 nil 3410692328
   ("" (skosimp*)
    (("" (expand "is_majority")
      (("" (expand "const_seq")
        (("" (lemma "card_below_fullset[length(const_seq(n!1, c!1))]")
          (("" (expand "fullset")
            (("" (expand "const_seq") (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((is_majority const-decl "bool" majority_seq nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (below type-eq-decl nil nat_types nil)
    (T formal-nonempty-type-decl nil majority_seq 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_below_fullset formula-decl nil finite_sets_below
     "finite_sets/")
    (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)
    (fullset const-decl "set" sets nil)
    (const_seq const-decl "finite_sequence[T]" seqs nil))
   nil)
  (is_majority_const-1 nil 3410692309
   ("" (skosimp*)
    (("" (expand "is_majority")
      (("" (expand "constant_seq")
        ((""
          (lemma "card_below_fullset[length(constant_seq(n!1, c!1))]")
          (("" (expand "fullset")
            (("" (expand "constant_seq") (("" (assert) nil))))))))))))
    nil)
   nil nil))
(maj_const 0
  (maj_const-1 nil 3410692309
   ("" (skosimp*)
    (("" (lemma "is_majority_const")
      (("" (inst?)
        (("" (lemma "maj_lem") (("" (inst?) (("" (ground) nil))))))))))
    nil)
   ((is_majority_const formula-decl nil majority_seq nil)
    (maj_lem formula-decl nil majority_seq nil)
    (const_seq const-decl "finite_sequence[T]" seqs 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)
    (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)
    (T formal-nonempty-type-decl nil majority_seq nil))
   nil)))

quality100%

¤ Dauer der Verarbeitung: 0.12 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.