Quelle coalition_fun.prf Sprache: Lisp

(coalition_fun
(coalition_fun_TCC1 0
  (coalition_fun_TCC1-1 nil 3450526146 ("" (subtype-tcc) nil nil)
   ((zero_fun const-decl "real" coalition_fun nil)
    (coalition_fun? const-decl "bool" coalition_fun nil)
    (finite_emptyset name-judgement "finite_set" finite_sets nil))
   nil))
(subsets_are_finite 0
  (subsets_are_finite-1 nil 3450526146
   ("" (skosimp)
    (("" (rewrite-lemma "finite_subset" ("s" "x!1" "A" "fullN"))
      (("1" (hide 2) (("1" (grind) nil nil)) nil)
       ("2" (hide 2)
        (("2" (typepred "N")
          (("2" (hide 1) (("2" (grind) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((finite_subset formula-decl nil finite_sets nil)
    (powset type-eq-decl nil coalition_fun nil)
    (fullN const-decl "powset" coalition_fun nil)
    (setof type-eq-decl nil defined_types nil)
    (U formal-nonempty-type-decl nil coalition_fun nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (empty? const-decl "bool" sets nil)
    (players_set nonempty-type-eq-decl nil players_set nil)
    (N formal-const-decl "players_set" coalition_fun nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (member const-decl "bool" sets nil)
    (fullset const-decl "set" sets nil)
    (subset? const-decl "bool" sets nil)
    (injective? const-decl "bool" functions nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil nat_types 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))
   nil))
(tot_S_0 0
  (tot_S_0-1 nil 3450687506
   ("" (skosimp)
    (("" (expand "tot")
      (("" (rewrite "sum_const") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((tot const-decl "real" coalition_fun 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)
    (N formal-const-decl "players_set" coalition_fun nil)
    (players_set nonempty-type-eq-decl nil players_set nil)
    (empty? const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (U formal-nonempty-type-decl nil coalition_fun 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)
    (number nonempty-type-decl nil numbers nil)
    (powset type-eq-decl nil coalition_fun nil)
    (sum_const formula-decl nil finite_sets_sum_real "finite_sets/"))
   shostak))
(tot_distrib 0
  (tot_distrib-1 nil 3451301777
   ("" (skosimp)
    (("" (expand "tot") (("" (rewrite "sum_distributive") nil nil))
      nil))
    nil)
   ((tot const-decl "real" coalition_fun nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (restrict const-decl "R" restrict nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (number nonempty-type-decl nil numbers nil)
    (N formal-const-decl "players_set" coalition_fun nil)
    (players_set nonempty-type-eq-decl nil players_set nil)
    (empty? const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (U formal-nonempty-type-decl nil coalition_fun nil)
    (powset type-eq-decl nil coalition_fun nil)
    (sum_distributive formula-decl nil finite_sets_sum "finite_sets/")
    (real_plus_real_is_real application-judgement "real" reals nil))
   shostak))
(tot_mult_const 0
  (tot_mult_const-1 nil 3451304002
   ("" (skosimp)
    (("" (expand "tot") (("" (rewrite "sum_mult") nil nil)) nil)) nil)
   ((tot const-decl "real" coalition_fun nil)
    (N formal-const-decl "players_set" coalition_fun nil)
    (players_set nonempty-type-eq-decl nil players_set nil)
    (empty? const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (U formal-nonempty-type-decl nil coalition_fun 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)
    (number nonempty-type-decl nil numbers nil)
    (powset type-eq-decl nil coalition_fun nil)
    (sum_mult formula-decl nil finite_sets_sum_real "finite_sets/"))
   shostak))
(tot_distrib_sub 0
  (tot_distrib_sub-1 nil 3451307834
   ("" (skosimp)
    ((""
      (rewrite-lemma "tot_distrib"
       ("S" "S!1" "x" "x!1" "y" "LAMBDA i: -y!1(i)"))
      ((""
        (rewrite-lemma "tot_mult_const" ("S" "S!1" "c" "-1" "x" "y!1"))
        (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((minus_real_is_real application-judgement "real" reals nil)
    (tot_distrib formula-decl nil coalition_fun nil)
    (U formal-nonempty-type-decl nil coalition_fun nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (empty? const-decl "bool" sets nil)
    (players_set nonempty-type-eq-decl nil players_set nil)
    (N formal-const-decl "players_set" coalition_fun nil)
    (powset type-eq-decl nil coalition_fun 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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (tot_mult_const formula-decl nil coalition_fun nil))
   shostak))
(tot_div_const 0
  (tot_div_const-1 nil 3451306279
   ("" (skosimp)
    (("" (lemma "tot_mult_const" ("S" "S!1" "x" "x!1" "c" "1/a!1"))
      (("" (assert) nil nil)) nil))
    nil)
   ((nzreal nonempty-type-eq-decl nil reals nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (number nonempty-type-decl nil numbers nil)
    (powset type-eq-decl nil coalition_fun nil)
    (N formal-const-decl "players_set" coalition_fun nil)
    (players_set nonempty-type-eq-decl nil players_set nil)
    (empty? const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (U formal-nonempty-type-decl nil coalition_fun nil)
    (tot_mult_const formula-decl nil coalition_fun nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil))
   shostak)))

quality93%

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