Gedichte Musik Bilder Quellcodebibliothek Diashow Normaldarstellung
Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/ints/   (Beweissystem der NASA Version 6.0.9©)  Datei vom 28.9.2014 mit Größe 1 kB image not shown  

Quelle  finite_seqs.prf   Sprache: Lisp

 
(finite_seqs
 (choose_TCC1 0
  (choose_TCC1-1 nil 3403442054 ("" (subtype-tcc) nil nil) nil nil))
 (choose_in? 0
  (choose_in?-2 nil 3403442450
   ("" (skosimp*)
    (("" (expand "choose")
      (("" (lift-if)
        (("" (assert)
          (("" (ground)
            (("1" (expand "in?") (("1" (inst?) nil nil)) nil)
             ("2" (expand "in?") (("2" (inst?) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((choose const-decl "T" finite_seqs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (in? const-decl "bool" seqs "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)
    (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 finite_seqs 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))
   nil)
  (choose_in?-1 nil 3403362398
   ("" (skosimp*)
    (("" (expand "in?")
      (("" (expand "choose")
        (("" (lift-if)
          (("" (prop)
            (("1" (inst?) nil nil)
             ("2" (use "max_seq_in?")
              (("2" (expand "in?") (("2" (propax) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil shostak))
 (choose_consensus 0
  (choose_consensus-1 nil 3403361092
   ("" (skosimp*) (("" (use "choose_in?") (("" (assert) nil nil)) nil))
    nil)
   ((ne_seqs type-eq-decl nil seqs "structures/")
    (> const-decl "bool" reals nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (T formal-nonempty-type-decl nil finite_seqs nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (choose_in? formula-decl nil finite_seqs nil))
   nil))
 (maj_exists_same 0
  (maj_exists_same-1 nil 3495198007
   ("" (skosimp* t)
    (("" (typepred "mf!1(fs!1)")
      (("" (typepred "maj(fs!1)")
        (("" (prop)
          (("" (use "is_majority_unique") (("" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((majority_function type-eq-decl nil finite_seqs nil)
    (is_majority const-decl "bool" majority_seq "structures/")
    (maj_exists const-decl "bool" majority_seq "structures/")
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (T formal-nonempty-type-decl nil finite_seqs nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (is_majority_unique formula-decl nil majority_seq "structures/")
    (maj const-decl "{mv | maj_exists(fs) => is_majority(mv, fs)}"
     majority_seq "structures/"))
   shostak))
 (mf_lem 0
  (mf_lem-1 nil 3495202609
   ("" (skosimp*)
    (("" (rewrite "maj_exists_same")
      (("1" (use "maj_lem") (("1" (prop) nil nil)) nil)
       ("2" (expand "maj_exists") (("2" (inst?) nil nil)) nil))
      nil))
    nil)
   ((maj_exists_same formula-decl nil finite_seqs nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (T formal-nonempty-type-decl nil finite_seqs nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (maj_exists const-decl "bool" majority_seq "structures/")
    (is_majority const-decl "bool" majority_seq "structures/")
    (majority_function type-eq-decl nil finite_seqs nil)
    (maj_lem formula-decl nil majority_seq "structures/"))
   shostak))
 (majority_choose_consensus 0
  (majority_choose_consensus-1 nil 3495209869
   ("" (skosimp*)
    (("" (expand "majority_choose")
      (("" (lift-if)
        (("" (assert)
          (("" (prop)
            (("1" (typepred "maj(x1!1)")
              (("1" (prop)
                (("1" (use "maj_in_seq")
                  (("1" (assert)
                    (("1" (expand "in_seq")
                      (("1" (expand "in?")
                        (("1" (skosimp*)
                          (("1" (inst?) (("1" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (assert)
              (("2" (expand "choose")
                (("2" (assert)
                  (("2" (expand "in?") (("2" (inst?) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((majority_choose const-decl "T" finite_seqs nil)
    (in? const-decl "bool" seqs "structures/")
    (below type-eq-decl nil naturalnumbers nil)
    (< 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)
    (in_seq const-decl "bool" majority_seq "structures/")
    (maj_in_seq formula-decl nil majority_seq "structures/")
    (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)
    (T formal-nonempty-type-decl nil finite_seqs nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (maj_exists const-decl "bool" majority_seq "structures/")
    (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)
    (ne_seqs type-eq-decl nil seqs "structures/")
    (is_majority const-decl "bool" majority_seq "structures/")
    (maj const-decl "{mv | maj_exists(fs) => is_majority(mv, fs)}"
     majority_seq "structures/")
    (choose const-decl "T" finite_seqs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (choose_consensus application-judgement "in_consensus_function"
     finite_seqs nil))
   nil))
 (majority_choose2_TCC1 0
  (majority_choose2_TCC1-1 nil 3495213184 ("" (subtype-tcc) nil nil)
   ((member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (nonempty? const-decl "bool" sets nil))
   nil))
 (majority_choose2_TCC2 0
  (majority_choose2_TCC2-1 nil 3495213184 ("" (subtype-tcc) nil nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (majority2_choose_majority 0
  (majority2_choose_majority-1 nil 3495213184
   ("" (skosimp*)
    (("" (expand "majority_choose2")
      (("" (expand "majority_choose")
        (("" (lift-if)
          (("" (assert)
            (("" (prop)
              (("1" (expand "maj_exists")
                (("1" (expand "is_majority")
                  (("1" (skosimp*)
                    (("1" (use "empty_card[below(length(x1!1))]")
                      (("1" (assert)
                        (("1" (expand "empty?")
                          (("1" (expand "member")
                            (("1" (skosimp*) nil nil)) nil))
                          nil))
                        nil)
                       ("2" (rewrite "finite_below") nil nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (typepred "maj(x1!1)") (("2" (assert) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((majority_choose2 const-decl "T" finite_seqs nil)
    (is_majority const-decl "bool" majority_seq "structures/")
    (empty_card 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)
    (below type-eq-decl nil nat_types nil)
    (T formal-nonempty-type-decl nil finite_seqs nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (below type-eq-decl nil naturalnumbers nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (x1!1 skolem-const-decl "finite_sequence[T]" finite_seqs 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" finite_seqs nil)
    (empty? const-decl "bool" sets nil)
    (member 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)
    (finite_below formula-decl nil finite_sets_below "finite_sets/")
    (maj_exists const-decl "bool" majority_seq "structures/")
    (NOT const-decl "[bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (maj const-decl "{mv | maj_exists(fs) => is_majority(mv, fs)}"
     majority_seq "structures/")
    (majority_choose const-decl "T" finite_seqs nil))
   nil))
 (uniform_TCC1 0
  (uniform_TCC1-1 nil 3494953503 ("" (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)
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil))
   nil))
 (uniform_TCC2 0
  (uniform_TCC2-1 nil 3494953503
   ("" (skosimp*)
    (("" (rewrite "finite_below")
      (("" (skosimp*) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (finite_below formula-decl nil finite_sets_below "finite_sets/")
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (set type-eq-decl nil sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (below type-eq-decl nil nat_types nil)
    (T formal-nonempty-type-decl nil finite_seqs nil)
    (finite_sequence type-eq-decl nil 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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (majority_same 0
  (majority_same-1 nil 3494953576
   ("" (skosimp*)
    (("" (prop)
      (("1" (expand "is_majority")
        (("1" (expand "is_majority?")
          (("1" (expand "uniform") (("1" (propax) nil nil)) nil)) nil))
        nil)
       ("2" (expand "is_majority?")
        (("2" (expand "is_majority")
          (("2" (assert)
            (("2" (expand "uniform") (("2" (propax) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((is_majority? const-decl "bool" finite_seqs nil)
    (uniform const-decl "finite_set[below(k)]" finite_seqs nil)
    (is_majority const-decl "bool" majority_seq "structures/")
    (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))
   shostak)))

100%


¤ Dauer der Verarbeitung: 0.15 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland




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.