Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: majority_array.prf Sprache: Lisp

Original von: PVS^©

(majority_array
(is_majority_TCC1 0
  (is_majority_TCC1-1 nil 3506271671
   ("" (skosimp*) (("" (rewrite "finite_below") nil)) nil)
   ((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)
    (below type-eq-decl nil nat_types nil)
    (T formal-nonempty-type-decl nil majority_array 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" majority_array nil))
   nil))
(maj_TCC1 0
  (maj_TCC1-1 nil 3506271671
   (""
    (inst 1 "(LAMBDA A:
             IF maj_exists(A) THEN
                choose({mv: T | is_majority(mv, A)})
             ELSE
                epsilon({mv: T | TRUE})
             ENDIF)")
    (("1" (skosimp*) nil) ("2" (skosimp*) (("2" (assert) nil)))
     ("3" (grind) nil))
    nil)
   ((member const-decl "bool" sets nil)
    (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)
    (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_array nil)
    (maj_exists const-decl "bool" majority_array nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (T formal-nonempty-type-decl nil majority_array nil)
    (below type-eq-decl nil nat_types nil)
    (N formal-const-decl "posnat" majority_array 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))
   nil))
(is_majority_unique 0
  (is_majority_unique-1 nil 3506271671
   ("" (skosimp*)
    (("" (expand "is_majority")
      ((""
        (case "disjoint?({ii | A!1(ii) = mv1!1},{ii | A!1(ii) = mv2!1})")
        (("1" (lemma "card_disj_union[below(N)]")
          (("1" (inst?)
            (("1" (assert)
              (("1" (hide -2)
                (("1"
                  (case "card(union({ii | A!1(ii) = mv1!1}, {ii | A!1(ii) = mv2!1})) <= N")
                  (("1" (replace -2)
                    (("1" (hide -2 -3 -4 1) (("1" (assert) nil)))))
                   ("2" (hide -1 -2 -3)
                    (("2" (rewrite "card_below") nil)))
                   ("3" (rewrite "finite_below") nil)))))))
             ("2" (rewrite "finite_below") nil)
             ("3" (rewrite "finite_below") nil)))))
         ("2" (expand "disjoint?")
          (("2" (expand "intersection")
            (("2" (expand "empty?")
              (("2" (expand "member")
                (("2" (skosimp*) (("2" (assert) nil))))))))))))))))
    nil)
   ((is_majority const-decl "bool" majority_array 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)
    (below type-eq-decl nil naturalnumbers 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)
    (<= 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/")
    (finite_set type-eq-decl nil finite_sets nil)
    (mv2!1 skolem-const-decl "T" majority_array nil)
    (is_finite const-decl "bool" finite_sets nil)
    (A!1 skolem-const-decl "[below[N] -> T]" majority_array nil)
    (mv1!1 skolem-const-decl "T" majority_array 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" majority_array nil)
    (below type-eq-decl nil nat_types nil)
    (set type-eq-decl nil sets nil)
    (disjoint? const-decl "bool" sets nil)
    (T formal-nonempty-type-decl nil majority_array nil)
    (= const-decl "[T, T -> boolean]" equalities nil))
   nil))
(maj_lem 0
  (maj_lem-1 nil 3506271671
   ("" (skosimp*)
    (("" (prop)
      (("1" (expand "maj_exists") (("1" (inst?) nil)))
       ("2" (typepred "maj(A!1)")
        (("2" (split -1)
          (("1" (lemma "is_majority_unique")
            (("1" (inst -1 "A!1" "mv!1" "maj(A!1)")
              (("1" (assert) nil)))))
           ("2" (expand "maj_exists") (("2" (inst?) nil)))))))
       ("3" (typepred "maj(A!1)") (("3" (assert) nil))))))
    nil)
   ((T formal-nonempty-type-decl nil majority_array nil)
    (maj_exists const-decl "bool" majority_array nil)
    (is_majority_unique formula-decl nil majority_array 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)
    (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" majority_array nil)
    (below type-eq-decl nil nat_types nil)
    (is_majority const-decl "bool" majority_array nil)
    (maj const-decl "{mv | maj_exists(A) => is_majority(mv, A)}"
     majority_array nil))
   nil))
(maj_subset 0
  (maj_subset-1 nil 3506271671
   ("" (skosimp*)
    (("" (expand "is_majority")
      (("" (case "subset?(IDS!1,{ii | A!1(ii) = mv!1})")
        (("1" (lemma "card_subset[below(N)]")
          (("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_array 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_array nil)
    (A!1 skolem-const-decl "[below[N] -> T]" majority_array 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" majority_array 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)
    (below type-eq-decl nil nat_types nil)
    (T formal-nonempty-type-decl nil majority_array nil)
    (= const-decl "[T, T -> boolean]" equalities nil))
   nil))
(maj_in_array 0
  (maj_in_array-1 nil 3506271671
   ("" (skosimp*)
    (("" (expand "is_majority")
      (("" (lemma "card_empty?[below(N)]")
        (("" (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?) nil)))))))))))))))
           ("2" (rewrite "finite_below") nil))))))))
    nil)
   ((is_majority const-decl "bool" majority_array nil)
    (mv!1 skolem-const-decl "T" majority_array nil)
    (A!1 skolem-const-decl "[below[N] -> T]" majority_array nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (T formal-nonempty-type-decl nil majority_array nil)
    (below type-eq-decl nil nat_types nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (member const-decl "bool" 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)
    (empty? const-decl "bool" sets nil)
    (finite_below formula-decl nil finite_sets_below "finite_sets/")
    (card_empty? formula-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)
    (N formal-const-decl "posnat" majority_array nil)
    (below type-eq-decl nil naturalnumbers nil))
   nil))
(is_majority_const 0
  (is_majority_const-1 nil 3506271671
   ("" (skosimp*)
    (("" (lemma "card_below_fullset")
      (("" (expand "constant_array")
        (("" (expand "is_majority")
          (("" (expand "fullset") (("" (assert) nil))))))))))
    nil)
   ((N formal-const-decl "posnat" majority_array 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)
    (card_below_fullset formula-decl nil finite_sets_below
     "finite_sets/")
    (is_majority const-decl "bool" majority_array 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)
    (fullset const-decl "set" sets nil)
    (constant_array const-decl "below_array" majority_array nil))
   nil))
(maj_const 0
  (maj_const-1 nil 3506271671
   ("" (skosimp*)
    (("" (lemma "is_majority_const")
      (("" (inst?)
        (("" (lemma "maj_lem") (("" (inst?) (("" (ground) nil))))))))))
    nil)
   ((is_majority_const formula-decl nil majority_array nil)
    (maj_lem formula-decl nil majority_array nil)
    (constant_array const-decl "below_array" majority_array nil)
    (below_array type-eq-decl nil below_arrays nil)
    (below type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (N formal-const-decl "posnat" majority_array 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)
    (T formal-nonempty-type-decl nil majority_array nil))
   nil)))

¤ Dauer der Verarbeitung: 0.4 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.