Quelle majority_properties.prf Sprache: Lisp

(majority_properties
(is_majority 0
  (is_majority-1 nil 3494947025
   ("" (skosimp*)
    (("" (rewrite "majority_same")
      (("" (expand "vec2seq" + 2)
        (("" (expand "majority_value_set")
          (("" (expand "is_majority?")
            (("" (case "empty?(e!1)")
              (("1" (prop)
                (("1" (invoke (case "empty?(%1)") (! -1 l 2 1))
                  (("1" (use "empty_card[below(N)]")
                    (("1" (assert) nil nil)) nil)
                   ("2" (expand "empty?")
                    (("2" (skosimp*)
                      (("2" (expand "member")
                        (("2" (expand "uniform_nodes")
                          (("2" (flatten) (("2" (inst?) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (use "empty_card[below(card(e!1))]")
                  (("2" (assert)
                    (("2" (use "empty_card[below(N)]")
                      (("2" (assert)
                        (("2" (expand "empty?")
                          (("2" (skosimp*) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2"
                (invoke (case-replace "%1 = %2") (! 2 r 1 2)
                 (! 2 l 1 2))
                (("1" (prop) nil nil)
                 ("2" (hide 3)
                  (("2" (rewrite "card_eq_bij")
                    (("2" (inst + "m(e!1)")
                      (("1" (expand "restrict")
                        (("1" (expand "bijective?")
                          (("1" (prop)
                            (("1" (expand "injective?")
                              (("1"
                                (skosimp* t)
                                (("1"
                                  (expand "uniform")
                                  (("1"
                                    (expand "vec2seq")
                                    (("1"
                                      (assert)
                                      (("1"
                                        (typepred "m(e!1)")
                                        (("1"
                                          (expand "bijective?")
                                          (("1"
                                            (expand "injective?")
                                            (("1"
                                              (flatten)
                                              (("1"
                                                (inst - "x1!1" "x2!1")
                                                (("1"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (expand "surjective?")
                              (("2"
                                (skosimp* t)
                                (("2"
                                  (expand "uniform_nodes")
                                  (("2"
                                    (flatten)
                                    (("2"
                                      (typepred "m(e!1)")
                                      (("1"
                                        (expand "bijective?")
                                        (("1"
                                          (flatten)
                                          (("1"
                                            (expand "surjective?")
                                            (("1"
                                              (inst?)
                                              (("1"
                                                (skosimp*)
                                                (("1"
                                                  (inst?)
                                                  (("1"
                                                    (expand "uniform")
                                                    (("1"
                                                      (expand
                                                       "vec2seq")
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2" (propax) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (skosimp* t)
                        (("2" (expand "uniform")
                          (("2" (expand "uniform_nodes")
                            (("2" (expand "vec2seq")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((majority_same formula-decl nil finite_seqs 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)
    (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)
    (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_properties nil)
    (below type-eq-decl nil naturalnumbers nil)
    (vec type-eq-decl nil node nil) (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (nodeid_set type-eq-decl nil node nil)
    (vec2seq const-decl "finite_sequence[T]" node nil)
    (T formal-nonempty-type-decl nil majority_properties nil)
    (majority_value_set const-decl "bool" majority_properties nil)
    (empty? const-decl "bool" sets nil)
    (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
    (Card const-decl "nat" finite_sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (uniform const-decl "finite_set[below(k)]" finite_seqs nil)
    (uniform_nodes const-decl "nodeid_set" node 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)
    (finite_set type-eq-decl nil finite_sets nil)
    (empty_card formula-decl nil finite_sets nil)
    (member const-decl "bool" sets nil)
    (restrict_of_inj_is_inj application-judgement "(injective?[S, R])"
     restrict nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (e!1 skolem-const-decl "nodeid_set[N, T]" majority_properties nil)
    (m const-decl "(bijective?[below(card(enabled)), (enabled)])" node
     nil)
    (bijective? const-decl "bool" functions nil)
    (nodeid_nonempty type-eq-decl nil node nil)
    (t!1 skolem-const-decl "T" majority_properties nil)
    (v!1 skolem-const-decl "vec[N, T]" majority_properties nil)
    (restrict const-decl "R" restrict nil)
    (surjective? const-decl "bool" functions nil)
    (y!1 skolem-const-decl "(uniform_nodes(e!1, v!1, t!1))"
     majority_properties nil)
    (x!1 skolem-const-decl "below(card(e!1))" majority_properties nil)
    (injective? const-decl "bool" functions nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (card_eq_bij formula-decl nil finite_sets_card_eq "finite_sets/")
    (is_majority? const-decl "bool" finite_seqs nil))
   shostak))
(majority_value_subset 0
  (majority_value_subset-1 nil 3494954016
   ("" (skosimp*)
    (("" (expand "majority_value_set")
      (("" (expand "majority_subset?")
        (("" (prop) (("" (grind) nil nil)) nil)) nil))
      nil))
    nil)
   ((majority_value_set const-decl "bool" majority_properties nil)
    (below type-eq-decl nil naturalnumbers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-nonempty-type-decl nil majority_properties nil)
    (N formal-const-decl "posnat" majority_properties 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)
    (uniform_nodes const-decl "nodeid_set" node nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas 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)
    (majority_subset? const-decl "bool" pigeonhole nil))
   shostak))
(uniform_majority 0
  (uniform_majority-1 nil 3398785724
   ("" (skosimp*)
    (("" (expand* "majority_value_set" "majority_subset?")
      (("" (prop)
        ((""
          (invoke (then (case "%1 <= %2") (assert)) (! -1 l 2)
           (! 1 l 2))
          (("" (rewrite "card_subset[below(N)]")
            (("" (hide 3 2 -1)
              (("" (auto-rewrite-defs)
                (("" (assert)
                  (("" (skosimp*)
                    (("" (inst?)
                      (("" (inst?) (("" (prop) nil nil)) nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((majority_subset? const-decl "bool" pigeonhole nil)
    (majority_value_set const-decl "bool" majority_properties 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)
    (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_properties nil)
    (below type-eq-decl nil naturalnumbers nil)
    (set type-eq-decl nil 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)
    (Card const-decl "nat" finite_sets nil)
    (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
    (T formal-nonempty-type-decl nil majority_properties nil)
    (nodeid_set type-eq-decl nil node nil)
    (vec type-eq-decl nil node nil)
    (uniform_nodes const-decl "nodeid_set" node 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)
    (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)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (uniform? const-decl "bool" node nil)
    (card_subset formula-decl nil finite_sets nil))
   nil))
(majority_validity 0
  (majority_validity-2 nil 3495214986
   ("" (skosimp*)
    (("" (rewrite "is_majority")
      (("" (expand "majority") (("" (rewrite "mf_lem") nil nil)) nil))
      nil))
    nil)
   ((is_majority formula-decl nil majority_properties 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_properties nil)
    (below type-eq-decl nil naturalnumbers nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (T formal-nonempty-type-decl nil majority_properties nil)
    (nodeid_set type-eq-decl nil node nil)
    (vec type-eq-decl nil node nil)
    (mf_lem formula-decl nil finite_seqs nil)
    (below type-eq-decl nil nat_types nil)
    (finite_sequence type-eq-decl nil finite_sequences nil)
    (vec2seq const-decl "finite_sequence[T]" node 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)
    (majority const-decl "T" majority_properties nil))
   nil)
  (majority_validity-1 nil 3495188586
   ("" (skosimp*)
    (("" (rewrite "is_majority")
      (("" (expand "majority")
        (("" (rewrite "maj_lem") (("" (flatten) nil nil)) nil)) nil))
      nil))
    nil)
   ((nodeid_set type-eq-decl nil node nil)
    (vec type-eq-decl nil node nil)
    (maj_lem formula-decl nil majority_seq "structures/")
    (vec2seq const-decl "finite_sequence[T]" node nil))
   nil))
(agreement_generation 0
  (agreement_generation-2 nil 3495215005
   ("" (skosimp*)
    (("" (expand "majority")
      (("" (use "vec2seq_agreement") (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((majority const-decl "T" majority_properties nil)
    (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)
    (is_finite const-decl "bool" finite_sets nil)
    (nodeid_set type-eq-decl nil node nil)
    (vec type-eq-decl nil node nil)
    (T formal-nonempty-type-decl nil majority_properties nil)
    (N formal-const-decl "posnat" majority_properties 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)
    (vec2seq_agreement formula-decl nil node nil))
   nil)
  (agreement_generation-1 nil 3495188664
   ("" (skosimp*)
    (("" (expand "majority")
      (("" (use "vec2seq_agreement") (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((nodeid_set type-eq-decl nil node nil)
    (vec type-eq-decl nil node nil)
    (vec2seq_agreement formula-decl nil node nil))
   shostak)))

quality100%

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