Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: monad.prf Sprache: Lisp

Original von: PVS^©

(monad
(fullset_is_monad 0
  (fullset_is_monad-1 nil 3294071593 ("" (grind) nil nil)
   ((star_closed? const-decl "bool" groupoid_def nil)
    (monad? const-decl "bool" monad_def nil))
   shostak))
(monad_TCC1 0
  (monad_TCC1-1 nil 3294071529
   ("" (lemma "fullset_is_monad") (("" (propax) nil nil)) nil)
   ((fullset_is_monad formula-decl nil monad nil)) shostak))
(one_member 0
  (one_member-1 nil 3294071569 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-nonempty-type-decl nil monad nil)
    (set type-eq-decl nil sets nil)
    (* formal-const-decl "[T, T -> T]" monad nil)
    (one formal-const-decl "T" monad nil)
    (monad? const-decl "bool" monad_def nil)
    (monad nonempty-type-eq-decl nil monad nil)
    (identity? const-decl "bool" operator_defs nil)
    (restrict const-decl "R" restrict nil)
    (star_closed? const-decl "bool" groupoid_def nil)
    (member const-decl "bool" sets nil))
   shostak))
(one_in 0
  (one_in-1 nil 3405941233
   ("" (skosimp*)
    (("" (assert)
      (("" (grind)
        (("" (typepred "M!1")
          (("" (expand "monad?")
            (("" (flatten)
              (("" (expand "member") (("" (propax) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((monad nonempty-type-eq-decl nil monad nil)
    (monad? const-decl "bool" monad_def nil)
    (one formal-const-decl "T" monad nil)
    (* formal-const-decl "[T, T -> T]" monad nil)
    (set type-eq-decl nil sets nil)
    (T formal-nonempty-type-decl nil monad nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (member const-decl "bool" sets nil))
   shostak))
(left_identity 0
  (left_identity-1 nil 3294076909
   ("" (skosimp)
    (("" (lemma "fullset_is_monad")
      (("" (expand "monad?")
        (("" (flatten)
          (("" (hide -1 -2)
            (("" (expand "identity?")
              (("" (inst - "x!1")
                (("1" (flatten)
                  (("1" (expand "restrict") (("1" (propax) nil nil))
                    nil))
                  nil)
                 ("2" (expand "fullset") (("2" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((fullset_is_monad formula-decl nil monad nil)
    (identity? const-decl "bool" operator_defs nil)
    (restrict const-decl "R" restrict nil)
    (T formal-nonempty-type-decl nil monad nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil)
    (x!1 skolem-const-decl "T" monad nil)
    (monad? const-decl "bool" monad_def nil))
   shostak))
(right_identity 0
  (right_identity-1 nil 3294076954
   ("" (skosimp)
    (("" (lemma "fullset_is_monad")
      (("" (expand "monad?")
        (("" (flatten)
          (("" (expand "identity?")
            (("" (inst - "x!1")
              (("1" (flatten)
                (("1" (expand "restrict") (("1" (propax) nil nil))
                  nil))
                nil)
               ("2" (expand "fullset") (("2" (propax) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((fullset_is_monad formula-decl nil monad nil)
    (x!1 skolem-const-decl "T" monad nil)
    (fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil monad nil)
    (restrict const-decl "R" restrict nil)
    (identity? const-decl "bool" operator_defs nil)
    (monad? const-decl "bool" monad_def nil))
   shostak))
(unique_left_identity 0
  (unique_left_identity-1 nil 3294076981
   ("" (skosimp)
    (("" (prop)
      (("1" (lemma "one_member" ("M" "M!1"))
        (("1" (expand "member")
          (("1" (inst - "one")
            (("1" (rewrite "right_identity") nil nil)) nil))
          nil))
        nil)
       ("2" (replace -1)
        (("2" (skosimp) (("2" (rewrite "left_identity") nil nil)) nil))
        nil))
      nil))
    nil)
   ((member const-decl "bool" sets nil)
    (right_identity formula-decl nil monad nil)
    (M!1 skolem-const-decl "monad" monad nil)
    (one_member formula-decl nil monad nil)
    (T formal-nonempty-type-decl nil monad nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (* formal-const-decl "[T, T -> T]" monad nil)
    (one formal-const-decl "T" monad nil)
    (monad? const-decl "bool" monad_def nil)
    (monad nonempty-type-eq-decl nil monad nil)
    (left_identity formula-decl nil monad nil))
   shostak))
(unique_right_identity 0
  (unique_right_identity-1 nil 3294077083
   ("" (skosimp)
    (("" (prop)
      (("1" (lemma "one_member" ("M" "M!1"))
        (("1" (expand "member")
          (("1" (inst - "one")
            (("1" (rewrite "left_identity") nil nil)) nil))
          nil))
        nil)
       ("2" (replace -1)
        (("2" (skosimp) (("2" (rewrite "right_identity") nil nil))
          nil))
        nil))
      nil))
    nil)
   ((member const-decl "bool" sets nil)
    (left_identity formula-decl nil monad nil)
    (M!1 skolem-const-decl "monad" monad nil)
    (one_member formula-decl nil monad nil)
    (T formal-nonempty-type-decl nil monad nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (* formal-const-decl "[T, T -> T]" monad nil)
    (one formal-const-decl "T" monad nil)
    (monad? const-decl "bool" monad_def nil)
    (monad nonempty-type-eq-decl nil monad nil)
    (right_identity formula-decl nil monad nil))
   shostak))
(one_is_monad 0
  (one_is_monad-1 nil 3426244396
   ("" (expand "monad?")
    (("" (expand "singleton")
      (("" (grind)
        (("1" (rewrite "left_identity") nil nil)
         ("2" (rewrite "left_identity") nil nil)
         ("3" (rewrite "left_identity") nil nil))
        nil))
      nil))
    nil)
   ((singleton const-decl "(singleton?)" sets nil)
    (left_identity formula-decl nil monad nil)
    (set type-eq-decl nil sets nil)
    (singleton? const-decl "bool" sets nil)
    (restrict const-decl "R" restrict nil)
    (identity? const-decl "bool" operator_defs nil)
    (one formal-const-decl "T" monad nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (star_closed? const-decl "bool" groupoid_def nil)
    (T formal-nonempty-type-decl nil monad nil)
    (* formal-const-decl "[T, T -> T]" monad nil)
    (member const-decl "bool" sets nil)
    (monad? const-decl "bool" monad_def nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil))
   shostak))
(trivial_monad_TCC1 0
  (trivial_monad_TCC1-1 nil 3294077151
   ("" (expand "monad?")
    (("" (split)
      (("1" (grind) (("1" (rewrite "left_identity") nil nil)) nil)
       ("2" (grind) nil nil)
       ("3" (expand "identity?")
        (("3" (skosimp)
          (("3" (expand "restrict")
            (("3" (rewrite "left_identity")
              (("3" (rewrite "right_identity") nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((left_identity formula-decl nil monad nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (singleton? const-decl "bool" sets nil)
    (one formal-const-decl "T" monad nil)
    (star_closed? const-decl "bool" groupoid_def nil)
    (T formal-nonempty-type-decl nil monad nil)
    (* formal-const-decl "[T, T -> T]" monad nil)
    (member const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (right_identity formula-decl nil monad nil)
    (restrict const-decl "R" restrict nil)
    (identity? const-decl "bool" operator_defs nil)
    (monad? const-decl "bool" monad_def nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil))
   shostak))
(monad_is_groupoid 0
  (monad_is_groupoid-1 nil 3294071529 ("" (grind) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (one formal-const-decl "T" monad nil)
    (monad? const-decl "bool" monad_def nil)
    (monad nonempty-type-eq-decl nil monad nil)
    (identity? const-decl "bool" operator_defs nil)
    (restrict const-decl "R" restrict nil)
    (member const-decl "bool" sets nil)
    (* formal-const-decl "[T, T -> T]" monad nil)
    (T formal-nonempty-type-decl nil monad nil)
    (star_closed? const-decl "bool" groupoid_def nil))
   shostak))
(sing_one_finite_monad 0
  (sing_one_finite_monad-1 nil 3407064383 ("" (grind) nil nil)
   ((singleton? const-decl "bool" sets nil)
    (set type-eq-decl nil sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (singleton const-decl "(singleton?)" sets nil)
    (member const-decl "bool" sets nil)
    (* formal-const-decl "[T, T -> T]" monad nil)
    (T formal-nonempty-type-decl nil monad nil)
    (star_closed? const-decl "bool" groupoid_def nil)
    (right_identity formula-decl nil monad nil)
    (restrict const-decl "R" restrict nil)
    (left_identity formula-decl nil monad nil)
    (identity? const-decl "bool" operator_defs nil)
    (one formal-const-decl "T" monad nil)
    (monad? const-decl "bool" monad_def nil)
    (finite_monad? const-decl "bool" monad_def nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil))
   shostak))
(finite_monad_TCC1 0
  (finite_monad_TCC1-1 nil 3407064251
   ("" (inst + "singleton[T](one)") (("" (grind) nil nil)) nil)
   ((monad? const-decl "bool" monad_def nil)
    (identity? const-decl "bool" operator_defs nil)
    (left_identity formula-decl nil monad nil)
    (restrict const-decl "R" restrict nil)
    (right_identity formula-decl nil monad nil)
    (star_closed? const-decl "bool" groupoid_def nil)
    (member const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (singleton const-decl "(singleton?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (finite_monad? const-decl "bool" monad_def nil)
    (one formal-const-decl "T" monad nil)
    (* formal-const-decl "[T, T -> T]" monad nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil monad nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil))
   nil))
(commutative_monad_TCC1 0
  (commutative_monad_TCC1-1 nil 3407068743
   ("" (inst + "singleton[T](one)")
    (("" (expand "commutative_monad?")
      (("" (prop) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil))
      nil))
    nil)
   ((commutative? const-decl "bool" operator_defs nil)
    (monad? const-decl "bool" monad_def nil)
    (identity? const-decl "bool" operator_defs nil)
    (left_identity formula-decl nil monad nil)
    (restrict const-decl "R" restrict nil)
    (right_identity formula-decl nil monad nil)
    (star_closed? const-decl "bool" groupoid_def nil)
    (member const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (singleton const-decl "(singleton?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (commutative_monad? const-decl "bool" monad_def nil)
    (one formal-const-decl "T" monad nil)
    (* formal-const-decl "[T, T -> T]" monad nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil monad nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil))
   nil))
(finite_commutative_monad_TCC1 0
  (finite_commutative_monad_TCC1-1 nil 3407068743
   ("" (inst + "singleton[T](one)") (("" (grind) nil nil)) nil)
   ((commutative? const-decl "bool" operator_defs nil)
    (finite_monad? const-decl "bool" monad_def nil)
    (monad? const-decl "bool" monad_def nil)
    (identity? const-decl "bool" operator_defs nil)
    (left_identity formula-decl nil monad nil)
    (restrict const-decl "R" restrict nil)
    (right_identity formula-decl nil monad nil)
    (star_closed? const-decl "bool" groupoid_def nil)
    (member const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (singleton const-decl "(singleton?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (finite_commutative_monad? const-decl "bool" monad_def nil)
    (one formal-const-decl "T" monad nil)
    (* formal-const-decl "[T, T -> T]" monad nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-nonempty-type-decl nil monad nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil))
   nil))
(order_TCC1 0
  (order_TCC1-1 nil 3407064251 ("" (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)
    (T formal-nonempty-type-decl nil monad nil)
    (set type-eq-decl nil sets nil)
    (* formal-const-decl "[T, T -> T]" monad nil)
    (one formal-const-decl "T" monad nil)
    (finite_monad? const-decl "bool" monad_def nil)
    (finite_monad nonempty-type-eq-decl nil monad nil)
    (member const-decl "bool" sets nil)
    (star_closed? const-decl "bool" groupoid_def nil)
    (right_identity formula-decl nil monad nil)
    (restrict const-decl "R" restrict nil)
    (left_identity formula-decl nil monad nil)
    (identity? const-decl "bool" operator_defs nil)
    (monad? const-decl "bool" monad_def nil)
    (injective? const-decl "bool" functions nil)
    (is_finite const-decl "bool" finite_sets nil))
   nil))
(order_TCC2 0
  (order_TCC2-1 nil 3407064251
   ("" (skosimp)
    (("" (typepred "F!1")
      (("" (expand "finite_monad?")
        (("" (expand "monad?")
          (("" (flatten)
            (("" (expand "member")
              (("" (lemma "nonempty_card" ("S" "F!1"))
                (("" (replace -1 1 rl)
                  (("" (hide-all-but (-3 1)) (("" (grind) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((finite_monad nonempty-type-eq-decl nil monad nil)
    (finite_monad? const-decl "bool" monad_def nil)
    (one formal-const-decl "T" monad nil)
    (* formal-const-decl "[T, T -> T]" monad nil)
    (set type-eq-decl nil sets nil)
    (T formal-nonempty-type-decl nil monad nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (monad? const-decl "bool" monad_def nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (nonempty_card formula-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil))
   nil))
(order_is_1 0
  (order_is_1-1 nil 3407064442
   ("" (skosimp*)
    (("" (expand "order")
      (("" (typepred "F!1")
        (("" (expand "finite_monad?")
          (("" (flatten)
            (("" (expand "monad?")
              (("" (flatten)
                (("" (hide -1 -3)
                  (("" (lemma "same_card_subset[T]")
                    (("" (inst?)
                      (("" (assert)
                        (("" (hide 2)
                          (("" (rewrite "card_singleton[T]")
                            (("" (assert)
                              ((""
                                (expand "subset?")
                                ((""
                                  (skosimp*)
                                  ((""
                                    (expand "member")
                                    ((""
                                      (expand "singleton")
                                      ((""
                                        (assert)
                                        ((""
                                          (name
                                           "S"
                                           "add(x!1, singleton[T](one))")
                                          ((""
                                            (case "subset?(S,F!1)")
                                            (("1"
                                              (lemma "card_subset[T]")
                                              (("1"
                                                (inst?)
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (case-replace
                                                     "card(S) = 2")
                                                    (("1"
                                                      (assert)
                                                      nil
                                                      nil)
                                                     ("2"
                                                      (hide-all-but
                                                       (-3 1 2))
                                                      (("2"
                                                        (lemma
                                                         "card_add[T]")
                                                        (("2"
                                                          (inst?)
                                                          (("2"
                                                            (assert)
                                                            (("2"
                                                              (lemma
                                                               "card_singleton[T]")
                                                              (("2"
                                                                (inst?)
                                                                (("2"
                                                                  (replace
                                                                   -1)
                                                                  (("2"
                                                                    (assert)
                                                                    (("2"
                                                                      (lift-if)
                                                                      (("2"
                                                                        (ground)
                                                                        (("2"
                                                                          (expand
                                                                           "singleton")
                                                                          (("2"
                                                                            (propax)
                                                                            nil
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (expand "subset?")
                                              (("2"
                                                (skosimp*)
                                                (("2"
                                                  (expand "member")
                                                  (("2"
                                                    (assert)
                                                    (("2"
                                                      (replace -2 * rl)
                                                      (("2"
                                                        (expand "add")
                                                        (("2"
                                                          (expand
                                                           "member")
                                                          (("2"
                                                            (expand
                                                             "singleton")
                                                            (("2"
                                                              (assert)
                                                              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))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((order const-decl "posnat" monad nil)
    (monad? const-decl "bool" monad_def nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (nonempty_add_finite application-judgement "non_empty_finite_set"
     finite_sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nonempty? const-decl "bool" sets nil)
    (add const-decl "(nonempty?)" sets nil)
    (empty? const-decl "bool" sets nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (card_subset formula-decl nil finite_sets nil)
    (odd_plus_even_is_odd application-judgement "odd_int" integers nil)
    (odd_plus_odd_is_even application-judgement "even_int" integers
     nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (card_add formula-decl nil finite_sets 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)
    (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)
    (Card const-decl "nat" finite_sets nil)
    (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
    (subset? const-decl "bool" sets nil)
    (card_singleton formula-decl nil finite_sets nil)
    (member const-decl "bool" sets nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (same_card_subset formula-decl nil finite_sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-nonempty-type-decl nil monad nil)
    (set type-eq-decl nil sets nil)
    (* formal-const-decl "[T, T -> T]" monad nil)
    (one formal-const-decl "T" monad nil)
    (finite_monad? const-decl "bool" monad_def nil)
    (finite_monad nonempty-type-eq-decl nil monad nil))
   nil))
(finite_monad_is_monad 0
  (finite_monad_is_monad-1 nil 3407064251 ("" (judgement-tcc) nil nil)
   ((finite_monad nonempty-type-eq-decl nil monad nil)
    (finite_monad? const-decl "bool" monad_def nil)
    (set type-eq-decl nil sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (is_finite const-decl "bool" finite_sets nil)
    (injective? const-decl "bool" functions nil)
    (member const-decl "bool" sets nil)
    (* formal-const-decl "[T, T -> T]" monad nil)
    (T formal-nonempty-type-decl nil monad nil)
    (star_closed? const-decl "bool" groupoid_def nil)
    (right_identity formula-decl nil monad nil)
    (restrict const-decl "R" restrict nil)
    (left_identity formula-decl nil monad nil)
    (identity? const-decl "bool" operator_defs nil)
    (one formal-const-decl "T" monad nil)
    (monad? const-decl "bool" monad_def nil))
   nil))
(commutative_monad_is_monad 0
  (commutative_monad_is_monad-1 nil 3407068743
   ("" (judgement-tcc) nil nil)
   ((commutative_monad nonempty-type-eq-decl nil monad nil)
    (commutative_monad? const-decl "bool" monad_def nil)
    (set type-eq-decl nil sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (commutative? const-decl "bool" operator_defs nil)
    (member const-decl "bool" sets nil)
    (* formal-const-decl "[T, T -> T]" monad nil)
    (T formal-nonempty-type-decl nil monad nil)
    (star_closed? const-decl "bool" groupoid_def nil)
    (right_identity formula-decl nil monad nil)
    (restrict const-decl "R" restrict nil)
    (left_identity formula-decl nil monad nil)
    (identity? const-decl "bool" operator_defs nil)
    (one formal-const-decl "T" monad nil)
    (monad? const-decl "bool" monad_def nil))
   nil))
(finite_commutative_monad_is_commutative_monad 0
  (finite_commutative_monad_is_commutative_monad-1 nil 3407068743
   ("" (judgement-tcc) nil nil)
   ((finite_commutative_monad nonempty-type-eq-decl nil monad nil)
    (finite_commutative_monad? const-decl "bool" monad_def nil)
    (set type-eq-decl nil sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (finite_monad? const-decl "bool" monad_def nil)
    (is_finite const-decl "bool" finite_sets nil)
    (injective? const-decl "bool" functions nil)
    (member const-decl "bool" sets nil)
    (* formal-const-decl "[T, T -> T]" monad nil)
    (T formal-nonempty-type-decl nil monad nil)
    (star_closed? const-decl "bool" groupoid_def nil)
    (right_identity formula-decl nil monad nil)
    (restrict const-decl "R" restrict nil)
    (left_identity formula-decl nil monad nil)
    (identity? const-decl "bool" operator_defs nil)
    (one formal-const-decl "T" monad nil)
    (monad? const-decl "bool" monad_def nil)
    (commutative? const-decl "bool" operator_defs nil)
    (commutative_monad? const-decl "bool" monad_def nil))
   nil))
(finite_commutative_monad_is_finite_monad 0
  (finite_commutative_monad_is_finite_monad-1 nil 3407068743
   ("" (judgement-tcc) nil nil)
   ((finite_commutative_monad nonempty-type-eq-decl nil monad nil)
    (finite_commutative_monad? const-decl "bool" monad_def nil)
    (set type-eq-decl nil sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (commutative? const-decl "bool" operator_defs nil)
    (member const-decl "bool" sets nil)
    (* formal-const-decl "[T, T -> T]" monad nil)
    (T formal-nonempty-type-decl nil monad nil)
    (star_closed? const-decl "bool" groupoid_def nil)
    (right_identity formula-decl nil monad nil)
    (restrict const-decl "R" restrict nil)
    (left_identity formula-decl nil monad nil)
    (identity? const-decl "bool" operator_defs nil)
    (one formal-const-decl "T" monad nil)
    (monad? const-decl "bool" monad_def nil)
    (injective? const-decl "bool" functions nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_monad? const-decl "bool" monad_def nil))
   nil)))

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des 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.