products/sources/formale Sprachen/PVS/TU_Games/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: tu_game.prf   Sprache: Lisp

Original von: PVS©
(tu_game
 (solution_concept_TCC1 1
  (solution_concept_TCC1-2 "Manually" 3450690788
   ("" (expand "core")
    (("" (expand "solution_concept?")
      (("" (skosimp)
        (("" (expand "subset?")
          (("" (skosimp)
            (("" (expand "member")
              (("" (expand "core")
                (("" (expand "member")
                  (("" (comment "setFP(g!1) vers setFP[ ]")
                    (("" (expand "setFP")
                      (("" (flatten)
                        (("" (hide -2) (("" (grind) nil nil)) nil))
                        nil))
                      ";;; setFP(g!1) vers setFP[ ]"))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((core const-decl "set_vect" imputations nil)
    (setFP const-decl "set_vect" imputations nil)
    (setPI const-decl "set_vect" imputations nil)
    (tot const-decl "real" coalition_fun nil))
   shostak)
  (solution_concept_TCC1-1 nil 3450605344 ("" (subtype-tcc) nil nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (core const-decl "set_vect(g`1)" tu_game nil)
    (setFP const-decl "set_vect(g`1)" tu_game nil)
    (fullN const-decl "powset" coalition_fun nil)
    (tot const-decl "real" coalition_fun nil)
    (setPI const-decl "set_vect" imputations nil)
    (member const-decl "bool" sets nil)
    (core const-decl "set_vect" imputations nil)
    (setFP const-decl "set_vect" imputations nil)
    (subset? const-decl "bool" sets nil)
    (solution_concept? const-decl "bool" tu_game nil))
   shostak))
 (a_test 0
  (a_test-2 "With solution_concept?" 3450606167
   ("" (skosimp)
    (("" (typepred "s!1")
      (("" (expand "solution_concept?") (("" (inst - "g!1") nil nil))
        nil))
      nil))
    nil)
   ((solution_concept nonempty-type-eq-decl nil tu_game nil)
    (solution_concept? const-decl "bool" tu_game nil)
    (set_vect type-eq-decl nil tu_game 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)
    (coalition_fun nonempty-type-eq-decl nil coalition_fun nil)
    (empty? const-decl "bool" sets 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)
    (players_set nonempty-type-eq-decl nil players_set nil)
    (U formal-nonempty-type-decl nil tu_game nil)
    (tu_game type-eq-decl nil tu_game nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak)
  (a_test-1 nil 3450530486
   ("" (skosimp)
    (("" (expand "subset?")
      (("" (skosimp)
        (("" (expand "setFP")
          (("" (expand "member")
            (("" (typepred "s!1")
              (("" (expand "solution_concept?")
                (("" (postpone) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((coalition_fun nonempty-type-eq-decl nil coalition_fun nil)
    (players_set nonempty-type-eq-decl nil players_set nil))
   shostak))
 (test_param 0
  (test_param-1 nil 3450604393
   ("" (skosimp) (("" (assert) nil nil)) nil) nil shostak))
 (tau_v_TCC1 0
  (tau_v_TCC1-2 "OK" 3450611682
   ("" (skosimp)
    (("" (expand "coalition_fun?")
      (("" (expand "o")
        (("" (expand "inverse_image")
          (("" (expand "inverse_image")
            (("" (expand "member")
              (("" (expand "emptyset")
                (("" (typepred "g!1`2")
                  (("" (expand "coalition_fun?")
                    (("" (expand "emptyset") (("" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((coalition_fun? const-decl "bool" coalition_fun nil)
    (inverse_image const-decl "set[D]" function_image nil)
    (member const-decl "bool" sets 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)
    (tu_game type-eq-decl nil tu_game nil)
    (coalition_fun nonempty-type-eq-decl nil coalition_fun nil)
    (empty? const-decl "bool" sets 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)
    (players_set nonempty-type-eq-decl nil players_set nil)
    (U formal-nonempty-type-decl nil tu_game nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (emptyset const-decl "set" sets nil)
    (inverse_image const-decl "set[D]" function_image nil)
    (O const-decl "T3" function_props nil))
   shostak)
  (tau_v_TCC1-1 nil 3450610898 ("" (subtype-tcc) nil nil)
   ((coalition_fun? const-decl "bool" coalition_fun nil)
    (coalition_fun nonempty-type-eq-decl nil coalition_fun nil)
    (players_set nonempty-type-eq-decl nil players_set nil))
   nil))
 (tau_x_TCC1 0
  (tau_x_TCC1-1 nil 3451131861 ("" (existence-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)
    (U formal-nonempty-type-decl nil tu_game 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)
    (empty? const-decl "bool" sets nil)
    (players_set nonempty-type-eq-decl nil players_set nil)
    (coalition_fun nonempty-type-eq-decl nil coalition_fun nil)
    (tu_game type-eq-decl nil tu_game nil)
    (bijective? const-decl "bool" functions nil)
    (tau_type type-eq-decl nil tu_game nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (>= const-decl "bool" reals 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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (i!1 skolem-const-decl "(NN!1)" tu_game nil)
    (NN!1 skolem-const-decl "players_set[U]" tu_game nil)
    (g!1 skolem-const-decl "tu_game" tu_game nil)
    (surjective? const-decl "bool" functions nil)
    (member const-decl "bool" sets nil)
    (injective? const-decl "bool" functions nil))
   nil))
 (bstar_TCC1 0
  (bstar_TCC1-1 nil 3450619785 ("" (tcc))
   ((member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (tot const-decl "real" coalition_fun nil)
    (emptyset const-decl "set" sets nil)
    (sum def-decl "R" finite_sets_sum "finite_sets/")
    (coalition_fun? const-decl "bool" coalition_fun nil))
   nil))
 (affinestar_TCC1 0
  (affinestar_TCC1-1 nil 3450619785 ("" (tcc))
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (U formal-nonempty-type-decl nil tu_game 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)
    (players_set nonempty-type-eq-decl nil players_set 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)
    (powset type-eq-decl nil coalition_fun nil)
    (coalition_fun nonempty-type-eq-decl nil coalition_fun nil)
    (injective? const-decl "bool" functions nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (tot const-decl "real" coalition_fun nil)
    (bstar const-decl "coalition_fun[U, N]" tu_game nil)
    (emptyset const-decl "set" sets nil)
    (sum def-decl "R" finite_sets_sum "finite_sets/")
    (coalition_fun? const-decl "bool" coalition_fun nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
 (interch_impl_desir 0
  (interch_impl_desir-1 nil 3463556569
   ("" (skosimp) (("" (grind) nil nil)) nil)
   ((more_desirable? const-decl "bool" tu_game nil)
    (interchangeable? const-decl "bool" tu_game nil)
    (member const-decl "bool" sets nil)
    (U formal-nonempty-type-decl nil tu_game nil)
    (players_set nonempty-type-eq-decl nil players_set 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)
    (coalition_fun nonempty-type-eq-decl nil coalition_fun nil)
    (tu_game type-eq-decl nil tu_game nil)
    (setof type-eq-decl nil defined_types nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nonempty_add_finite application-judgement
     "non_empty_finite_set[(N)]" coalition_fun nil))
   shostak))
 (interch_is_sym 0
  (interch_is_sym-1 nil 3463556524
   ("" (skosimp)
    (("" (expand "interchangeable?") (("" (grind) nil nil)) nil)) nil)
   ((interchangeable? const-decl "bool" tu_game nil)
    (nonempty_add_finite application-judgement
     "non_empty_finite_set[(N)]" coalition_fun nil)
    (setof type-eq-decl nil defined_types nil)
    (tu_game type-eq-decl nil tu_game nil)
    (coalition_fun nonempty-type-eq-decl nil coalition_fun 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)
    (players_set nonempty-type-eq-decl nil players_set nil)
    (U formal-nonempty-type-decl nil tu_game nil)
    (member const-decl "bool" sets nil))
   shostak))
 (DES_implies_ETP 0
  (DES_implies_ETP-2 "" 3463557186
   ("" (skosimp)
    (("" (expand "ETP")
      (("" (skosimp)
        (("" (expand "DES")
          (("" (inst-cp - "g!1" "x!1" "i!1" "j!1")
            (("" (inst - "g!1" "x!1" "j!1" "i!1")
              ((""
                (lemma "interch_impl_desir"
                 ("g" "g!1" "i" "i!1" "j" "j!1"))
                ((""
                  (lemma "interch_impl_desir"
                   ("g" "g!1" "i" "j!1" "j" "i!1"))
                  ((""
                    (lemma "interch_is_sym"
                     ("g" "g!1" "i" "i!1" "j" "j!1"))
                    (("" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((ETP const-decl "bool" tu_game nil)
    (DES const-decl "bool" tu_game nil)
    (interch_is_sym formula-decl nil tu_game nil)
    (interch_impl_desir formula-decl nil tu_game nil)
    (solution_concept nonempty-type-eq-decl nil tu_game nil)
    (solution_concept? const-decl "bool" tu_game nil)
    (set_vect type-eq-decl nil tu_game 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)
    (tu_game type-eq-decl nil tu_game nil)
    (coalition_fun nonempty-type-eq-decl nil coalition_fun 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)
    (players_set nonempty-type-eq-decl nil players_set nil)
    (U formal-nonempty-type-decl nil tu_game nil))
   shostak)
  (DES_implies_ETP-1 nil 3450619978
   ("" (skosimp)
    (("" (expand "ETP")
      (("" (skosimp)
        (("" (skosimp)
          (("" (expand "DES")
            (("" (inst - "g!1")
              (("" (inst - "x!1")
                (("" (skolem!)
                  (("" (inst-cp - "i!1" "j!1")
                    (("" (inst - "j!1" "i!1")
                      (("" (flatten)
                        (("" (lemma "DES_ETP_lemma2" ("g" "g!1"))
                          (("" (inst - "i!1" "j!1")
                            (("" (grind) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((coalition_fun nonempty-type-eq-decl nil coalition_fun nil)
    (players_set nonempty-type-eq-decl nil players_set nil))
   shostak))
 (SIVA_implies_NE 0
  (SIVA_implies_NE-1 nil 3450530028
   ("" (skosimp)
    (("" (expand "NE")
      (("" (expand "SIVA")
        (("" (skosimp)
          (("" (inst - "g!1")
            (("" (rewrite "nonempty_card") (("" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((NE const-decl "bool" tu_game nil)
    (nonempty_card formula-decl nil finite_sets nil)
    (set_vect type-eq-decl nil tu_game nil)
    (solution_concept? const-decl "bool" tu_game nil)
    (solution_concept nonempty-type-eq-decl nil tu_game 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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (tu_game type-eq-decl nil tu_game nil)
    (coalition_fun nonempty-type-eq-decl nil coalition_fun 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)
    (players_set nonempty-type-eq-decl nil players_set nil)
    (U formal-nonempty-type-decl nil tu_game nil)
    (SIVA const-decl "bool" tu_game nil))
   shostak))
 (PO_core 0
  (PO_core-1 nil 3450692276 ("" (grind) nil nil)
   ((core const-decl "set_vect(g`1)" tu_game nil)
    (setPI const-decl "set_vect(g`1)" tu_game nil)
    (fullN const-decl "powset" coalition_fun nil)
    (fullset const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (tot const-decl "real" coalition_fun nil)
    (setPI const-decl "set_vect" imputations nil)
    (core const-decl "set_vect" imputations nil)
    (subset? const-decl "bool" sets nil)
    (PO const-decl "bool" tu_game nil))
   shostak))
 (affine_bij 0
  (affine_bij-1 nil 3451305234
   ("" (skosimp)
    (("" (expand "affineinv")
      (("" (expand "affine")
        (("" (expand "lin")
          (("" (expand "dif") (("" (apply-extensionality) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((affineinv const-decl "[(N) -> real]" tu_game nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (lin const-decl "real" tu_game nil)
    (+ const-decl "[numfield, numfield -> numfield]" 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 "[numfield, numfield -> numfield]" number_fields nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (U formal-nonempty-type-decl nil tu_game 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)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (dif const-decl "real" tu_game nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (affine const-decl "[(N) -> real]" tu_game nil))
   shostak))
 (COV_core 0
  (COV_core-1 nil 3450701509
   ("" (expand "COV")
    (("" (skosimp)
      (("" (expand "core")
        (("" (apply-extensionality :hide? T)
          (("" (expand "core")
            (("" (expand "image")
              (("" (iff)
                (("" (split)
                  (("1" (skosimp)
                    (("1" (name "y" "affineinv(N!1,a!1,b!1)(x!1)")
                      (("1" (inst + "y")
                        (("1" (replace -1 :dir RL)
                          (("1" (hide -)
                            (("1" (rewrite "affine_bij") nil nil))
                            nil))
                          nil)
                         ("2" (split)
                          (("1" (hide -3)
                            (("1" (expand "member")
                              (("1"
                                (expand "setPI")
                                (("1"
                                  (replace -1 :dir RL)
                                  (("1"
                                    (expand "affineinv")
                                    (("1"
                                      (expand "affinestar")
                                      (("1"
                                        (rewrite-lemma
                                         "tot_div_const"
                                         ("S"
                                          "fullN[U,N!1]"
                                          "a"
                                          "a!1"
                                          "x"
                                          "dif(N!1, x!1, b!1)"))
                                        (("1"
                                          (hide -1)
                                          (("1"
                                            (expand "dif")
                                            (("1"
                                              (rewrite-lemma
                                               "tot_distrib_sub"
                                               ("S"
                                                "fullN[U,N!1]"
                                                "x"
                                                "x!1"
                                                "y"
                                                "b!1"))
                                              (("1" (grind) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (hide -2)
                            (("2" (skosimp)
                              (("2"
                                (inst - "S!1")
                                (("2"
                                  (replace -1 :dir RL)
                                  (("2"
                                    (expand "affineinv")
                                    (("2"
                                      (rewrite-lemma
                                       "tot_div_const"
                                       ("S"
                                        "S!1"
                                        "a"
                                        "a!1"
                                        "x"
                                        "dif(N!1, x!1, b!1)"))
                                      (("2"
                                        (expand "dif")
                                        (("2"
                                          (rewrite-lemma
                                           "tot_distrib_sub"
                                           ("S"
                                            "S!1"
                                            "x"
                                            "x!1"
                                            "y"
                                            "b!1"))
                                          (("2"
                                            (expand "affinestar")
                                            (("2"
                                              (expand "bstar")
                                              (("2"
                                                (expand ">=")
                                                (("2"
                                                  (rewrite
                                                   "div_mult_pos_le2"
                                                   +
                                                   ("py" "a!1"))
                                                  (("2"
                                                    (grind)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (skosimp)
                    (("2" (skosimp)
                      (("2" (split)
                        (("1" (typepred "x!2")
                          (("1" (hide -2)
                            (("1" (expand "member")
                              (("1"
                                (expand "setPI")
                                (("1"
                                  (replace -2)
                                  (("1"
                                    (hide -2)
                                    (("1"
                                      (expand "affinestar")
                                      (("1"
                                        (expand "affine")
                                        (("1"
                                          (expand "bstar")
                                          (("1"
                                            (expand "fullN")
                                            (("1"
                                              (rewrite-lemma
                                               "tot_distrib"
                                               ("S"
                                                "fullset[(N!1)]"
                                                "x"
                                                "lin(N!1,a!1,x!2)"
                                                "y"
                                                "b!1"))
                                              (("1"
                                                (expand "lin")
                                                (("1"
                                                  (expand "tot")
                                                  (("1"
                                                    (rewrite
                                                     "sum_mult")
                                                    (("1"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (skosimp)
                          (("2" (typepred "x!2")
                            (("2" (inst - "S!1")
                              (("2"
                                (expand "affinestar")
                                (("2"
                                  (expand "bstar")
                                  (("2"
                                    (expand "affine")
                                    (("2"
                                      (replace -3)
                                      (("2"
                                        (rewrite-lemma
                                         "tot_distrib"
                                         ("S"
                                          "S!1"
                                          "x"
                                          "lin(N!1,a!1,x!2)"
                                          "y"
                                          "b!1"))
                                        (("2"
                                          (expand "lin")
                                          (("2"
                                            (rewrite
                                             "both_sides_plus_ge2")
                                            (("2"
                                              (hide-all-but (-2) -)
                                              (("2"
                                                (rewrite-lemma
                                                 "tot_mult_const"
                                                 ("S"
                                                  "S!1"
                                                  "c"
                                                  "a!1"
                                                  "x"
                                                  "x!2"))
                                                (("2"
                                                  (rewrite
                                                   "both_sides_times_pos_ge2")
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((U formal-nonempty-type-decl nil tu_game 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)
    (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)
    (affine const-decl "[(N) -> real]" tu_game nil)
    (image const-decl "set[R]" function_image nil)
    (core const-decl "set_vect" imputations nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (affinestar const-decl "coalition_fun[U, N]" tu_game nil)
    (coalition_fun nonempty-type-eq-decl nil coalition_fun nil)
    (coalition_fun? const-decl "bool" coalition_fun nil)
    (powset type-eq-decl nil coalition_fun nil)
    (set_vect type-eq-decl nil coalition_fun nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (/= const-decl "boolean" notequal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (affineinv const-decl "[(N) -> real]" tu_game nil)
    (tot_distrib_sub formula-decl nil coalition_fun nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (bstar const-decl "coalition_fun[U, N]" tu_game nil)
    (fullset const-decl "set" sets nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (tot_div_const formula-decl nil coalition_fun nil)
    (fullN const-decl "powset" coalition_fun nil)
    (dif const-decl "real" tu_game nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (div_mult_pos_le2 formula-decl nil real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (affine_bij formula-decl nil tu_game nil)
    (tot const-decl "real" coalition_fun nil)
    (setPI const-decl "set_vect" imputations nil)
    (v!1 skolem-const-decl "coalition_fun[U, N!1]" tu_game nil)
    (y skolem-const-decl "[(N!1) -> real]" tu_game nil)
    (member const-decl "bool" sets nil)
    (N!1 skolem-const-decl "players_set[U]" tu_game nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (both_sides_times_pos_ge2 formula-decl nil real_props nil)
    (tot_mult_const formula-decl nil coalition_fun nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (both_sides_plus_ge2 formula-decl nil real_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (lin const-decl "real" tu_game nil)
    (tot_distrib formula-decl nil coalition_fun nil)
    (sum_mult formula-decl nil finite_sets_sum_real "finite_sets/")
    (core const-decl "set_vect(g`1)" tu_game nil)
    (COV const-decl "bool" tu_game nil))
   shostak)))


¤ Dauer der Verarbeitung: 0.32 Sekunden  (vorverarbeitet)  ¤



Druckansicht
unsichere Verbindung
Druckansicht
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.


Bot Zugriff