Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: gl.xml Sprache: Lisp

Original von: PVS^©

(monoid
(IMP_monad_TCC1 0
  (IMP_monad_TCC1-1 nil 3294078979
   ("" (lemma "fullset_is_monoid")
    (("" (expand "monoid?") (("" (flatten) nil nil)) nil)) nil)
   ((monoid? const-decl "bool" monoid_def nil)
    (fullset_is_monoid formula-decl nil monoid nil))
   shostak))
(IMP_semigroup_TCC1 0
  (IMP_semigroup_TCC1-1 nil 3294079000
   ("" (lemma "fullset_is_monoid")
    (("" (expand "monoid?")
      (("" (expand "monad?")
        (("" (expand "semigroup?")
          (("" (flatten) (("" (assert) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((monoid? const-decl "bool" monoid_def nil)
    (member const-decl "bool" sets nil)
    (monad? const-decl "bool" monad_def nil)
    (fullset_is_monoid formula-decl nil monoid nil))
   shostak))
(monoid_TCC1 0
  (monoid_TCC1-1 nil 3293375371
   ("" (lemma "fullset_is_monoid") (("" (propax) nil nil)) nil)
   ((fullset_is_monoid formula-decl nil monoid nil)) shostak))
(monoid_is_monad 0
  (monoid_is_monad-1 nil 3294079027
   ("" (skosimp)
    (("" (typepred "x!1")
      (("" (expand "monoid?") (("" (flatten) nil nil)) nil)) nil))
    nil)
   ((monoid nonempty-type-eq-decl nil monoid nil)
    (monoid? const-decl "bool" monoid_def nil)
    (one formal-const-decl "T" monoid nil)
    (* formal-const-decl "[T, T -> T]" monoid nil)
    (set type-eq-decl nil sets nil)
    (T formal-nonempty-type-decl nil monoid nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
(monoid_is_semigroup 0
  (monoid_is_semigroup-1 nil 3293375371
   ("" (skosimp)
    (("" (typepred "x!1")
      (("" (expand "monoid?")
        (("" (expand "monad?")
          (("" (expand "semigroup?")
            (("" (flatten) (("" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((monoid nonempty-type-eq-decl nil monoid nil)
    (monoid? const-decl "bool" monoid_def nil)
    (one formal-const-decl "T" monoid nil)
    (* formal-const-decl "[T, T -> T]" monoid nil)
    (set type-eq-decl nil sets nil)
    (T formal-nonempty-type-decl nil monoid 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)
    (one_member formula-decl nil monad nil))
   shostak))
(power_0 0
  (power_0-1 nil 3292925609 ("" (grind) nil nil)
   ((one formal-const-decl "T" monoid nil)
    (* formal-const-decl "[T, T -> T]" monoid nil)
    (T formal-nonempty-type-decl nil monoid nil)
    (power def-decl "T" monoid_def nil))
   shostak))
(power_1 0
  (power_1-1 nil 3292925615
   ("" (grind) (("" (rewrite "right_identity") nil nil)) nil)
   ((one formal-const-decl "T" monoid nil)
    (* formal-const-decl "[T, T -> T]" monoid nil)
    (T formal-nonempty-type-decl nil monoid nil)
    (power def-decl "T" monoid_def nil)
    (right_identity formula-decl nil monad nil))
   shostak))
(one_power 0
  (one_power-1 nil 3292925621
   ("" (induct "n")
    (("1" (grind) nil nil)
     ("2" (skosimp*)
      (("2" (expand "power" 1)
        (("2" (assert) (("2" (rewrite "left_identity") nil nil)) nil))
        nil))
      nil))
    nil)
   ((left_identity formula-decl nil monad nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (power def-decl "T" monoid_def nil)
    (one formal-const-decl "T" monoid nil)
    (* formal-const-decl "[T, T -> T]" monoid nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (T formal-nonempty-type-decl nil monoid nil)
    (pred type-eq-decl nil defined_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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))
   shostak))
(power_def 0
  (power_def-1 nil 3292925779
   ("" (induct "n")
    (("1" (grind)
      (("1" (rewrite "right_identity")
        (("1" (rewrite "left_identity") nil nil)) nil))
      nil)
     ("2" (skosimp*)
      (("2" (inst - "a!1")
        (("2" (expand "power" 1)
          (("2" (rewrite "associative") (("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (associative formula-decl nil semigroup nil)
    (right_identity formula-decl nil monad nil)
    (left_identity formula-decl nil monad nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (power def-decl "T" monoid_def nil)
    (one formal-const-decl "T" monoid nil)
    (* formal-const-decl "[T, T -> T]" monoid nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (T formal-nonempty-type-decl nil monoid nil)
    (pred type-eq-decl nil defined_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil))
   shostak))
(power_mult 0
  (power_mult-1 nil 3292925654
   ("" (induct "m")
    (("1" (skolem!)
      (("1" (rewrite "power_0")
        (("1" (assert) (("1" (rewrite "right_identity") nil nil)) nil))
        nil))
      nil)
     ("2" (skosimp*)
      (("2" (inst - "a!1" "n!1+1")
        (("2" (rewrite "power_def" -1)
          (("2" (expand "power" 1 2)
            (("2" (rewrite "associative" -1) (("2" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((power_def formula-decl nil monoid nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (associative formula-decl nil semigroup nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (right_identity formula-decl nil monad nil)
    (power_0 formula-decl nil monoid nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (power def-decl "T" monoid_def nil)
    (one formal-const-decl "T" monoid nil)
    (* formal-const-decl "[T, T -> T]" monoid nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (T formal-nonempty-type-decl nil monoid nil)
    (pred type-eq-decl nil defined_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil))
   shostak))
(power_power 0
  (power_power-1 nil 3292926190
   ("" (induct "m")
    (("1" (skolem!)
      (("1" (rewrite "power_0") (("1" (rewrite "power_0") nil nil))
        nil))
      nil)
     ("2" (skosimp*)
      (("2" (expand "power" 1 1)
        (("2" (inst - "a!1" "n!1")
          (("2" (replace -1)
            (("2" (rewrite "power_mult") (("2" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((power_mult formula-decl nil monoid nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (power_0 formula-decl nil monoid nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (power def-decl "T" monoid_def nil)
    (one formal-const-decl "T" monoid nil)
    (* formal-const-decl "[T, T -> T]" monoid nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (T formal-nonempty-type-decl nil monoid nil)
    (pred type-eq-decl nil defined_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil))
   shostak))
(power_commutes 0
  (power_commutes-1 nil 3292926297
   ("" (skolem!)
    (("" (rewrite "power_mult") (("" (rewrite "power_mult") nil nil))
      nil))
    nil)
   ((power_mult formula-decl nil monoid nil)
    (T formal-nonempty-type-decl nil monoid 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)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil))
   shostak))
(power_member 0
  (power_member-1 nil 3293204406
   ("" (skolem 1 ("M" "a" "_"))
    (("" (induct "n")
      (("1" (rewrite "power_0")
        (("1" (rewrite "one_member")
          (("1" (typepred "M")
            (("1" (expand "cyclic_monoid?")
              (("1" (expand "monoid?") (("1" (propax) nil nil)) nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (skosimp*)
        (("2" (assert)
          (("2" (expand "power" 1)
            (("2" (typepred "M")
              (("2" (expand "cyclic_monoid?")
                (("2" (expand "monoid?")
                  (("2" (expand "monad?")
                    (("2" (expand "groupoid?")
                      (("2" (flatten)
                        (("2" (expand "star_closed?")
                          (("2" (expand "member")
                            (("2" (inst - "a" "power(a,j!1)") nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (pred type-eq-decl nil defined_types nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (T formal-nonempty-type-decl nil monoid nil)
    (set type-eq-decl nil sets nil) (member const-decl "bool" sets nil)
    (* formal-const-decl "[T, T -> T]" monoid nil)
    (one formal-const-decl "T" monoid nil)
    (monoid? const-decl "bool" monoid_def nil)
    (monoid nonempty-type-eq-decl nil monoid nil)
    (power def-decl "T" monoid_def nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (monad nonempty-type-eq-decl nil monad nil)
    (monad? const-decl "bool" monad_def nil)
    (one_member formula-decl nil monad nil)
    (power_0 formula-decl nil monoid nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (star_closed? const-decl "bool" groupoid_def nil))
   shostak))
(one_is_monoid 0
  (one_is_monoid-1 nil 3426244316
   ("" (expand "monoid?") (("" (assert) (("" (grind) nil nil)) nil))
    nil)
   ((one_is_monad formula-decl nil monad nil)
    (T formal-nonempty-type-decl nil monoid nil)
    (* formal-const-decl "[T, T -> T]" monoid nil)
    (one formal-const-decl "T" monoid 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)
    (singleton const-decl "(singleton?)" sets nil)
    (left_identity formula-decl nil monad nil)
    (associative? const-decl "bool" operator_defs nil)
    (restrict const-decl "R" restrict nil)
    (monoid? const-decl "bool" monoid_def nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil))
   shostak))
(generated_is_submonoid 0
  (generated_is_submonoid-1 nil 3294401810
   ("" (skosimp)
    (("" (expand "submonoid?")
      (("" (split)
        (("1" (expand "generated_set")
          (("1" (expand "subset?")
            (("1" (skosimp)
              (("1" (lemma "power_member" ("a" "a!1" "M" "M!1"))
                (("1" (expand "member")
                  (("1" (skosimp)
                    (("1" (replace -2)
                      (("1" (inst - "n!1") (("1" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (expand "monoid?")
          (("2" (expand "monad?")
            (("2" (expand "groupoid?")
              (("2" (split)
                (("1" (expand "star_closed?")
                  (("1" (expand "generated_set")
                    (("1" (expand "member")
                      (("1" (skosimp)
                        (("1" (typepred "x!1")
                          (("1" (typepred "y!1")
                            (("1" (expand "generated_set")
                              (("1"
                                (skosimp*)
                                (("1"
                                  (inst + "n!2+n!1")
                                  (("1"
                                    (replace -1)
                                    (("1"
                                      (replace -2)
                                      (("1"
                                        (rewrite "power_mult")
                                        nil
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (expand "member")
                  (("2" (expand "generated_set")
                    (("2" (inst + "0")
                      (("2" (rewrite "power_0") nil nil)) nil))
                    nil))
                  nil)
                 ("3" (expand "identity?")
                  (("3" (skosimp)
                    (("3" (expand "restrict")
                      (("3" (rewrite "left_identity")
                        (("3" (rewrite "right_identity") nil nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("4" (expand "associative?")
                  (("4" (lemma "associative")
                    (("4" (expand "restrict")
                      (("4" (skosimp*)
                        (("4" (inst - "x!1" "y!1" "z!1") nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((submonoid? const-decl "bool" monoid nil)
    (power_mult formula-decl nil monoid nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (star_closed? const-decl "bool" groupoid_def nil)
    (power_0 formula-decl nil monoid nil)
    (left_identity formula-decl nil monad nil)
    (right_identity formula-decl nil monad nil)
    (restrict const-decl "R" restrict nil)
    (identity? const-decl "bool" operator_defs nil)
    (associative formula-decl nil semigroup nil)
    (associative? const-decl "bool" operator_defs nil)
    (monad? const-decl "bool" monad_def nil)
    (generated_set const-decl "set[T]" monoid_def nil)
    (member const-decl "bool" sets nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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)
    (number nonempty-type-decl nil numbers nil)
    (power_member formula-decl nil monoid nil)
    (T formal-nonempty-type-decl nil monoid 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]" monoid nil)
    (one formal-const-decl "T" monoid nil)
    (monoid? const-decl "bool" monoid_def nil)
    (monoid nonempty-type-eq-decl nil monoid nil)
    (subset? const-decl "bool" sets nil))
   shostak))
(generated_set_card_1 0
  (generated_set_card_1-1 nil 3396974100
   ("" (skosimp*)
    (("" (lemma "generated_set_lem")
      (("" (inst - "a!1" "0")
        (("" (assert)
          (("" (lemma "card_one[T]")
            (("" (inst?)
              (("" (assert)
                (("" (skosimp*)
                  (("" (replace -1)
                    (("" (expand "singleton")
                      (("" (assert)
                        (("" (replace -2 * rl)
                          (("" (lemma "generated_set_lem")
                            (("" (inst - "a!1" "1")
                              ((""
                                (expand "power")
                                ((""
                                  (expand "power")
                                  ((""
                                    (assert)
                                    ((""
                                      (lemma "right_identity")
                                      ((""
                                        (inst?)
                                        ((""
                                          (assert)
                                          ((""
                                            (replace -1)
                                            ((""
                                              (hide -1)
                                              ((""
                                                (replace -2)
                                                ((""
                                                  (hide -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)
   ((one formal-const-decl "T" monoid nil)
    (* formal-const-decl "[T, T -> T]" monoid nil)
    (T formal-nonempty-type-decl nil monoid nil)
    (generated_set_lem formula-decl nil monoid_def nil)
    (power_0 formula-decl nil monoid nil)
    (member const-decl "bool" sets nil)
    (generated_set const-decl "set[T]" monoid_def 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)
    (singleton const-decl "(singleton?)" sets nil)
    (right_identity formula-decl nil monad nil)
    (power def-decl "T" monoid_def nil)
    (card_one formula-decl nil finite_sets nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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))
   nil))
(finite_monoid_TCC1 0
  (finite_monoid_TCC1-1 nil 3407068285
   ("" (inst + "singleton[T](one)")
    (("" (expand "finite_monoid?")
      (("" (expand "monoid?")
        (("" (expand "monad?")
          (("" (expand "groupoid?")
            (("" (expand "star_closed?")
              (("" (expand "member")
                (("" (prop)
                  (("1" (skosimp*)
                    (("1" (grind)
                      (("1" (typepred "x!1")
                        (("1" (typepred "y!1")
                          (("1" (expand "singleton")
                            (("1" (assert)
                              (("1"
                                (replace -1)
                                (("1"
                                  (hide -1)
                                  (("1"
                                    (replace -1)
                                    (("1"
                                      (hide -1)
                                      (("1"
                                        (rewrite "left_identity")
                                        nil
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (grind) nil nil) ("3" (grind) nil nil)
                   ("4" (grind) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((monad? const-decl "bool" monad_def nil)
    (member const-decl "bool" sets nil)
    (associative? const-decl "bool" operator_defs nil)
    (right_identity formula-decl nil monad nil)
    (restrict const-decl "R" restrict nil)
    (identity? const-decl "bool" operator_defs nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (left_identity formula-decl nil monad nil)
    (star_closed? const-decl "bool" groupoid_def nil)
    (monoid? const-decl "bool" monoid_def nil)
    (singleton const-decl "(singleton?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (finite_monoid? const-decl "bool" monoid_def nil)
    (one formal-const-decl "T" monoid nil)
    (* formal-const-decl "[T, T -> T]" monoid 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 monoid nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil))
   nil))
(finite_monoid_is_monoid 0
  (finite_monoid_is_monoid-1 nil 3407068285
   ("" (skosimp*)
    (("" (typepred "x!1")
      (("" (expand "finite_monoid?") (("" (flatten) nil nil)) nil))
      nil))
    nil)
   ((finite_monoid nonempty-type-eq-decl nil monoid nil)
    (finite_monoid? const-decl "bool" monoid_def nil)
    (one formal-const-decl "T" monoid nil)
    (* formal-const-decl "[T, T -> T]" monoid nil)
    (set type-eq-decl nil sets nil)
    (T formal-nonempty-type-decl nil monoid nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(finite_monoid_is_finite_monad 0
  (finite_monoid_is_finite_monad-1 nil 3407068285
   ("" (judgement-tcc) nil nil)
   ((finite_monoid nonempty-type-eq-decl nil monoid nil)
    (finite_monoid? const-decl "bool" monoid_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)
    (monoid? const-decl "bool" monoid_def nil)
    (associative? const-decl "bool" operator_defs nil)
    (member const-decl "bool" sets nil)
    (star_closed? const-decl "bool" groupoid_def nil)
    (one formal-const-decl "T" monoid nil)
    (* formal-const-decl "[T, T -> T]" monoid nil)
    (T formal-nonempty-type-decl nil monoid nil)
    (one_member formula-decl nil monad 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)
    (finite_monad? const-decl "bool" monad_def nil))
   nil))
(finite_submonoids 0
  (finite_submonoids-1 nil 3407068313
   ("" (skosimp) (("" (typepred "F!1") (("" (propax) nil nil)) nil))
    nil)
   ((finite_monoid nonempty-type-eq-decl nil monoid nil)
    (finite_monoid? const-decl "bool" monoid_def nil)
    (one formal-const-decl "T" monoid nil)
    (* formal-const-decl "[T, T -> T]" monoid nil)
    (set type-eq-decl nil sets nil)
    (T formal-nonempty-type-decl nil monoid nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(commutative_monoid_TCC1 0
  (commutative_monoid_TCC1-1 nil 3407069225
   ("" (inst + "singleton[T](one)")
    (("" (expand "commutative_monoid?")
      (("" (prop)
        (("1" (expand "monoid?")
          (("1" (prop)
            (("1" (expand "monad?")
              (("1" (prop)
                (("1" (expand "groupoid?")
                  (("1" (expand "singleton")
                    (("1" (expand "star_closed?")
                      (("1" (skosimp*)
                        (("1" (expand "member")
                          (("1" (assert)
                            (("1" (typepred "x!1")
                              (("1"
                                (typepred "y!1")
                                (("1"
                                  (replace -1)
                                  (("1"
                                    (hide -1)
                                    (("1"
                                      (replace -1)
                                      (("1"
                                        (hide -1)
                                        (("1"
                                          (rewrite "left_identity")
                                          nil
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (expand "member")
                  (("2" (expand "singleton") (("2" (propax) nil nil))
                    nil))
                  nil)
                 ("3" (expand "identity?")
                  (("3" (skosimp*)
                    (("3" (expand "restrict") (("3" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (expand "associative?")
              (("2" (skosimp*)
                (("2" (grind) (("2" (rewrite "associative") nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (grind) nil nil))
        nil))
      nil))
    nil)
   ((commutative? const-decl "bool" operator_defs nil)
    (monoid? const-decl "bool" monoid_def nil)
    (associative? const-decl "bool" operator_defs nil)
    (associative formula-decl nil semigroup nil)
    (monad? const-decl "bool" monad_def nil)
    (identity? const-decl "bool" operator_defs nil)
    (restrict const-decl "R" restrict nil)
    (right_identity formula-decl nil monad nil)
    (left_identity formula-decl nil monad nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (member const-decl "bool" sets nil)
    (star_closed? const-decl "bool" groupoid_def nil)
    (singleton const-decl "(singleton?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (commutative_monoid? const-decl "bool" monoid_def nil)
    (one formal-const-decl "T" monoid nil)
    (* formal-const-decl "[T, T -> T]" monoid 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 monoid nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil))
   nil))
(commutative_monoid_is_monoid 0
  (commutative_monoid_is_monoid-1 nil 3407069225
   ("" (skosimp*)
    (("" (typepred "x!1")
      (("" (expand "commutative_monoid?") (("" (flatten) nil nil))
        nil))
      nil))
    nil)
   ((commutative_monoid nonempty-type-eq-decl nil monoid nil)
    (commutative_monoid? const-decl "bool" monoid_def nil)
    (one formal-const-decl "T" monoid nil)
    (* formal-const-decl "[T, T -> T]" monoid nil)
    (set type-eq-decl nil sets nil)
    (T formal-nonempty-type-decl nil monoid nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(commutative_monoid_is_commutative_monad 0
  (commutative_monoid_is_commutative_monad-1 nil 3407069225
   ("" (skosimp*)
    (("" (typepred "x!1")
      (("" (expand "commutative_monoid?")
        (("" (flatten)
          (("" (expand "commutative_monad?")
            (("" (assert)
              (("" (expand "monoid?") (("" (propax) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((commutative_monoid nonempty-type-eq-decl nil monoid nil)
    (commutative_monoid? const-decl "bool" monoid_def nil)
    (one formal-const-decl "T" monoid nil)
    (* formal-const-decl "[T, T -> T]" monoid nil)
    (set type-eq-decl nil sets nil)
    (T formal-nonempty-type-decl nil monoid nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (monoid? const-decl "bool" monoid_def nil)
    (commutative_monad? const-decl "bool" monad_def nil))
   nil))
(commutative_submonoids 0
  (commutative_submonoids-1 nil 3407069303
   ("" (skosimp*)
    (("" (typepred "H!1")
      (("" (expand "commutative_monoid?")
        (("" (flatten)
          (("" (expand "commutative?")
            (("" (expand "restrict")
              (("" (assert)
                (("" (expand "submonoid?")
                  (("" (flatten)
                    (("" (assert)
                      (("" (skosimp*)
                        (("" (inst?)
                          (("1" (assert)
                            (("1" (expand "subset?")
                              (("1"
                                (expand "member")
                                (("1"
                                  (inst?)
                                  (("1" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (expand "subset?")
                            (("2" (expand "member")
                              (("2"
                                (inst?)
                                (("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((commutative_monoid nonempty-type-eq-decl nil monoid nil)
    (commutative_monoid? const-decl "bool" monoid_def nil)
    (one formal-const-decl "T" monoid nil)
    (* formal-const-decl "[T, T -> T]" monoid nil)
    (set type-eq-decl nil sets nil)
    (T formal-nonempty-type-decl nil monoid nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (restrict const-decl "R" restrict nil)
    (submonoid? const-decl "bool" monoid nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (H!1 skolem-const-decl "commutative_monoid" monoid nil)
    (S!1 skolem-const-decl "set[T]" monoid nil)
    (x!1 skolem-const-decl "(S!1)" monoid nil)
    (y!1 skolem-const-decl "(S!1)" monoid nil)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (commutative? const-decl "bool" operator_defs nil))
   shostak)))

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