products/sources/formale sprachen/Coq/config/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: players_set.prf   Sprache: Unknown

(players_set)
(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/"))
   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)))

[ Dauer der Verarbeitung: 0.1 Sekunden  (vorverarbeitet)  ]