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

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei:   Sprache: Lisp

Original von: PVS©
(convergence_set
 (convergent_zero 0
  (convergent_zero-1 nil 3406348940
   ("" (skosimp)
    (("" (expand "convergent?")
      (("" (case-replace "nonzero_elts(LAMBDA t: 0, X!1)= emptyset[T]")
        (("1" (rewrite "countable_emptyset")
          (("1" (rewrite "convergent_empty") nil nil)) nil)
         ("2" (hide 2)
          (("2" (apply-extensionality :hide? t)
            (("2" (expand "emptyset")
              (("2" (expand "nonzero_elts") (("2" (propax) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((convergent? const-decl "bool" convergence_set nil)
    (countable_emptyset formula-decl nil countable_props "sets_aux/")
    (convergent_empty formula-decl nil countable_convergence nil)
    (emptyset const-decl "set" sets nil)
    (nonzero_elts const-decl "set[T]" convergence_set 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)
    (= const-decl "[T, T -> boolean]" equalities 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-type-decl nil convergence_set nil)
    (finite_emptyset name-judgement "finite_set[T]" convergence_set
     nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set" finite_sets nil))
   shostak))
 (convergent_plus 0
  (convergent_plus-1 nil 3406349137
   ("" (skosimp)
    (("" (expand "convergent?")
      (("" (flatten)
        (("" (split)
          (("1"
            (lemma "countable_subset"
             ("S" "nonzero_elts(f!1 + g!1, X!1)" "Count"
              "union(nonzero_elts(f!1, X!1),nonzero_elts(g!1, X!1))"))
            (("1" (split -1)
              (("1" (propax) nil nil)
               ("2" (hide-all-but 1)
                (("2" (expand "subset?")
                  (("2" (expand "nonzero_elts")
                    (("2" (expand "union")
                      (("2" (expand "member")
                        (("2" (skosimp)
                          (("2" (expand "+") (("2" (assert) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2"
              (lemma "countable_union"
               ("Count1" "nonzero_elts(f!1, X!1)" "Count2"
                "nonzero_elts(g!1, X!1)"))
              (("2" (propax) nil nil)) nil))
            nil)
           ("2"
            (case "subset?(nonzero_elts(f!1 + g!1, X!1),union(nonzero_elts(f!1, X!1),nonzero_elts(g!1, X!1)))")
            (("1" (name-replace "FX" "nonzero_elts(f!1, X!1)")
              (("1" (name-replace "GX" "nonzero_elts(g!1, X!1)")
                (("1" (name-replace "FGX" "nonzero_elts(f!1+g!1, X!1)")
                  (("1"
                    (lemma "countable_union"
                     ("Count1" "FX" "Count2" "GX"))
                    (("1"
                      (lemma "convergent_disjoint_union"
                       ("g" "f!1" "X" "FX" "Y"
                        "difference(union(FX, GX),FX)"))
                      (("1"
                        (lemma "convergent_disjoint_union"
                         ("g" "g!1" "X" "GX" "Y"
                          "difference(union(FX, GX),GX)"))
                        (("1" (replace -6)
                          (("1" (replace -8)
                            (("1"
                              (case-replace
                               "union(GX, difference(union(FX, GX), GX))=union(FX, GX)")
                              (("1"
                                (hide -1)
                                (("1"
                                  (case-replace
                                   "union(FX, difference(union(FX, GX), FX))=union(FX, GX)")
                                  (("1"
                                    (hide -1)
                                    (("1"
                                      (split -1)
                                      (("1"
                                        (split -2)
                                        (("1"
                                          (lemma
                                           "convergent_plus"
                                           ("X"
                                            "union(FX,GX)"
                                            "f"
                                            "f!1"
                                            "g"
                                            "g!1"))
                                          (("1"
                                            (assert)
                                            (("1"
                                              (lemma
                                               "convergent_subset"
                                               ("X"
                                                "FGX"
                                                "Y"
                                                "union(FX, GX)"
                                                "g"
                                                "f!1+g!1"))
                                              (("1" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (hide-all-but 1)
                                          (("2" (grind) nil nil))
                                          nil)
                                         ("3"
                                          (hide 2)
                                          (("3"
                                            (lemma
                                             "convergent_zeros"
                                             ("g"
                                              "f!1"
                                              "X"
                                              "difference(union(FX, GX), FX)"))
                                            (("3"
                                              (assert)
                                              (("3"
                                                (hide 2)
                                                (("3"
                                                  (skosimp)
                                                  (("3"
                                                    (typepred "t!1")
                                                    (("3"
                                                      (hide-all-but
                                                       (-1 1))
                                                      (("3"
                                                        (expand "FX")
                                                        (("3"
                                                          (expand
                                                           "nonzero_elts")
                                                          (("3"
                                                            (expand
                                                             "union")
                                                            (("3"
                                                              (expand
                                                               "difference")
                                                              (("3"
                                                                (expand
                                                                 "member")
                                                                (("3"
                                                                  (flatten)
                                                                  (("3"
                                                                    (expand
                                                                     "GX")
                                                                    (("3"
                                                                      (expand
                                                                       "nonzero_elts")
                                                                      (("3"
                                                                        (grind)
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (hide-all-but 1)
                                        (("2" (grind) nil nil))
                                        nil)
                                       ("3"
                                        (hide -1 2)
                                        (("3"
                                          (lemma
                                           "convergent_zeros"
                                           ("g"
                                            "g!1"
                                            "X"
                                            "difference(union(FX, GX), GX)"))
                                          (("3"
                                            (assert)
                                            (("3"
                                              (hide-all-but 1)
                                              (("3"
                                                (skosimp)
                                                (("3"
                                                  (typepred "t!1")
                                                  (("3"
                                                    (expand "GX")
                                                    (("3"
                                                      (expand "FX")
                                                      (("3"
                                                        (grind)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (hide-all-but 1)
                                    (("2"
                                      (apply-extensionality :hide? t)
                                      (("2" (grind) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (hide-all-but 1)
                                (("2"
                                  (apply-extensionality :hide? t)
                                  (("2" (grind) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (rewrite "countable_difference") nil
                          nil))
                        nil)
                       ("2" (rewrite "countable_difference") nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (hide-all-but 1)
              (("2" (expand "nonzero_elts")
                (("2" (expand "union")
                  (("2" (expand "subset?")
                    (("2" (expand "member")
                      (("2" (skosimp)
                        (("2" (expand "+ ") (("2" (assert) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((convergent? const-decl "bool" convergence_set nil)
    (countable_union judgement-tcc nil countable_props "sets_aux/")
    (subset? const-decl "bool" sets nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (member const-decl "bool" sets nil)
    (countable_subset formula-decl nil countability "sets_aux/")
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil 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)
    (nonzero_elts const-decl "set[T]" convergence_set nil)
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (is_countable const-decl "bool" countability "sets_aux/")
    (countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (union const-decl "set" sets nil)
    (T formal-type-decl nil convergence_set nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (convergent_disjoint_union formula-decl nil countable_convergence
     nil)
    (difference const-decl "set" sets nil)
    (countable_difference judgement-tcc nil countable_props
     "sets_aux/")
    (/= const-decl "boolean" notequal nil)
    (GX skolem-const-decl "set[T]" convergence_set nil)
    (FX skolem-const-decl "set[T]" convergence_set nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (convergent_zeros formula-decl nil countable_convergence nil)
    (disjoint? const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil)
    (convergent_plus formula-decl nil countable_convergence nil)
    (convergent_subset formula-decl nil countable_convergence nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil))
   shostak))
 (convergent_scal 0
  (convergent_scal-1 nil 3406349233
   ("" (skosimp)
    (("" (expand "convergent?")
      (("" (flatten)
        (("" (case-replace "a!1=0")
          (("1" (case-replace "nonzero_elts(0 * f!1, X!1)=emptyset[T]")
            (("1" (rewrite "countable_emptyset")
              (("1" (rewrite "convergent_empty") nil nil)) nil)
             ("2" (hide-all-but 1)
              (("2" (apply-extensionality :hide? t)
                (("2" (expand "emptyset")
                  (("2" (expand "nonzero_elts")
                    (("2" (flatten)
                      (("2" (expand "*") (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2"
            (case-replace
             "nonzero_elts(a!1 * f!1, X!1)=nonzero_elts(f!1, X!1)")
            (("1" (assert)
              (("1" (hide -1 -2)
                (("1"
                  (lemma "convergent_scal"
                   ("X" "nonzero_elts(f!1, X!1)" "a" "a!1" "f" "f!1"))
                  (("1" (assert) nil nil)) nil))
                nil))
              nil)
             ("2" (hide-all-but (1 2))
              (("2" (apply-extensionality :hide? t)
                (("2" (expand "nonzero_elts")
                  (("2" (expand "*")
                    (("2" (assert)
                      (("2" (case-replace "f!1(x!1)=0")
                        (("1" (assert) nil nil) ("2" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((convergent? const-decl "bool" convergence_set nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities 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_times_real_is_real application-judgement "real" reals nil)
    (countable_emptyset formula-decl nil countable_props "sets_aux/")
    (convergent_empty formula-decl nil countable_convergence nil)
    (emptyset const-decl "set" sets nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (nonzero_elts const-decl "set[T]" convergence_set nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (T formal-type-decl nil convergence_set nil)
    (finite_emptyset name-judgement "finite_set[T]" convergence_set
     nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (is_countable const-decl "bool" countability "sets_aux/")
    (convergent_scal formula-decl nil countable_convergence nil))
   shostak))
 (convergent_opp 0
  (convergent_opp-1 nil 3406350311
   ("" (skosimp)
    (("" (lemma "convergent_scal" ("X" "X!1" "f" "f!1" "a" "-1"))
      (("" (assert)
        (("" (case-replace "-1*f!1=-f!1")
          (("" (hide-all-but 1)
            (("" (apply-extensionality :hide? t)
              (("" (expand "*")
                (("" (expand "-") (("" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number nonempty-type-decl nil numbers nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil convergence_set nil)
    (convergent_scal formula-decl nil convergence_set nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
 (convergent_diff 0
  (convergent_diff-1 nil 3406350375
   ("" (skosimp)
    (("" (lemma "convergent_opp" ("X" "X!1" "f" "g!1"))
      (("" (assert)
        (("" (lemma "convergent_plus" ("X" "X!1" "f" "f!1" "g" "-g!1"))
          (("" (assert)
            (("" (case-replace "f!1 + -g!1=f!1 - g!1")
              (("" (hide-all-but 1)
                (("" (apply-extensionality :hide? t)
                  (("" (expand "+")
                    (("" (expand "-") (("" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil convergence_set nil)
    (convergent_opp formula-decl nil convergence_set nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (convergent_plus formula-decl nil convergence_set nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (+ const-decl "[T -> real]" real_fun_ops "reals/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
 (convergent_le 0
  (convergent_le-1 nil 3406357616
   ("" (skosimp)
    (("" (expand "convergent?")
      (("" (flatten)
        ((""
          (case "subset?(nonzero_elts(g!1, X!1),nonzero_elts(f!1, X!1))")
          (("1"
            (lemma "countable_subset"
             ("S" "nonzero_elts(g!1, X!1)" "Count"
              "nonzero_elts(f!1, X!1)"))
            (("1" (assert)
              (("1"
                (lemma "convergent_subset"
                 ("X" "nonzero_elts(g!1, X!1)" "Y"
                  "nonzero_elts(f!1, X!1)" "g" "f!1"))
                (("1" (assert)
                  (("1"
                    (lemma "convergent_le"
                     ("g" "g!1" "f" "f!1" "X"
                      "nonzero_elts(g!1, X!1)"))
                    (("1" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide-all-but (-1 1))
            (("2" (expand "subset?")
              (("2" (expand "nonzero_elts")
                (("2" (expand "member")
                  (("2" (skosimp)
                    (("2" (inst - "x!1") (("2" (grind) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((convergent? const-decl "bool" convergence_set nil)
    (nonzero_elts const-decl "set[T]" convergence_set 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)
    (subset? const-decl "bool" 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-type-decl nil convergence_set nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (convergent_le formula-decl nil countable_convergence nil)
    (convergent_subset formula-decl nil countable_convergence nil)
    (countable_subset formula-decl nil countability "sets_aux/")
    (is_countable const-decl "bool" countability "sets_aux/")
    (countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (member const-decl "bool" sets nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (/= const-decl "boolean" notequal nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil))
   shostak))
 (convergent_empty 0
  (convergent_empty-1 nil 3406350597
   ("" (skosimp)
    (("" (expand "convergent?")
      (("" (case-replace "nonzero_elts(g!1, emptyset[T])=emptyset[T]")
        (("1" (rewrite "countable_emptyset")
          (("1" (rewrite "convergent_empty") nil nil)) nil)
         ("2" (hide 2)
          (("2" (apply-extensionality :hide? t)
            (("2" (expand "emptyset")
              (("2" (expand "nonzero_elts") (("2" (propax) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((convergent? const-decl "bool" convergence_set nil)
    (countable_emptyset formula-decl nil countable_props "sets_aux/")
    (convergent_empty formula-decl nil countable_convergence nil)
    (emptyset const-decl "set" sets nil)
    (nonzero_elts const-decl "set[T]" convergence_set 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)
    (= const-decl "[T, T -> boolean]" equalities 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-type-decl nil convergence_set nil)
    (finite_emptyset name-judgement "finite_set[T]" convergence_set
     nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set" finite_sets nil))
   shostak))
 (convergent_singleton 0
  (convergent_singleton-1 nil 3406350738
   ("" (skosimp)
    (("" (expand "convergent?")
      (("" (expand "absconvergent?")
        (("" (case "g!1(t!1)=0")
          (("1"
            (case-replace
             "nonzeros(g!1, singleton(t!1))=emptyset[real]")
            (("1" (assert)
              (("1" (rewrite "countable_emptyset") nil nil)) nil)
             ("2" (hide 2)
              (("2" (apply-extensionality :hide? t)
                (("2" (expand "emptyset")
                  (("2" (expand "nonzeros")
                    (("2" (expand "extend")
                      (("2" (prop)
                        (("2" (skosimp)
                          (("2" (expand "singleton")
                            (("2" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2"
            (case-replace
             "nonzeros(g!1, singleton(t!1)) = singleton(g!1(t!1))")
            (("1" (hide -1)
              (("1" (rewrite "countable_singleton")
                (("1" (flatten)
                  (("1" (rewrite "finite_singleton") nil nil)) nil))
                nil))
              nil)
             ("2" (hide 3)
              (("2" (apply-extensionality :hide? t)
                (("2" (expand "singleton")
                  (("2" (expand "nonzeros")
                    (("2" (expand "extend")
                      (("2" (case-replace "x!1=g!1(t!1)")
                        (("1" (assert) (("1" (inst + "t!1") nil nil))
                          nil)
                         ("2" (assert)
                          (("2" (prop)
                            (("2" (skosimp) (("2" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" convergence_set nil)
    (convergent? const-decl "bool" countable_convergence nil))
   shostak))
 (convergent_subset 0
  (convergent_subset-1 nil 3406356738
   ("" (skosimp)
    (("" (expand "convergent?")
      (("" (flatten)
        ((""
          (case "subset?(nonzero_elts(g!1, X!1),nonzero_elts(g!1, Y!1))")
          (("1"
            (lemma "countable_subset"
             ("S" "nonzero_elts(g!1, X!1)" "Count"
              "nonzero_elts(g!1, Y!1)"))
            (("1" (assert)
              (("1"
                (lemma "convergent_subset"
                 ("X" "nonzero_elts(g!1, X!1)" "Y"
                  "nonzero_elts(g!1, Y!1)" "g" "g!1"))
                (("1" (assert) nil nil)) nil))
              nil))
            nil)
           ("2" (hide-all-but (-1 1))
            (("2" (expand "subset?")
              (("2" (expand "nonzero_elts")
                (("2" (expand "member")
                  (("2" (skosimp)
                    (("2" (inst - "x!1") (("2" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((convergent? const-decl "bool" convergence_set nil)
    (nonzero_elts const-decl "set[T]" convergence_set 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)
    (subset? const-decl "bool" 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-type-decl nil convergence_set nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (convergent_subset formula-decl nil countable_convergence nil)
    (countable_subset formula-decl nil countability "sets_aux/")
    (is_countable const-decl "bool" countability "sets_aux/")
    (countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (member const-decl "bool" sets nil))
   shostak))
 (convergent_intersection 0
  (convergent_intersection-1 nil 3406353573
   ("" (skosimp)
    (("" (split)
      (("1"
        (lemma "convergent_subset"
         ("X" "intersection(X!1, Y!1)" "Y" "X!1" "g" "g!1"))
        (("1" (rewrite "intersection_subset1") (("1" (assert) nil nil))
          nil))
        nil)
       ("2"
        (lemma "convergent_subset"
         ("X" "intersection(X!1, Y!1)" "Y" "Y!1" "g" "g!1"))
        (("2" (rewrite "intersection_commutative")
          (("2" (rewrite "intersection_subset1")
            (("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((intersection_subset1 formula-decl nil sets_lemmas nil)
    (convergent_subset formula-decl nil convergence_set nil)
    (T formal-type-decl nil convergence_set nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (intersection const-decl "set" 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)
    (intersection_commutative formula-decl nil sets_lemmas nil))
   shostak))
 (convergent_difference 0
  (convergent_difference-1 nil 3406353696
   ("" (skosimp)
    ((""
      (lemma "convergent_subset"
       ("X" "difference(X!1, Y!1)" "Y" "X!1" "g" "g!1"))
      (("" (rewrite "difference_subset") (("" (assert) nil nil)) nil))
      nil))
    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)
    (difference 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-type-decl nil convergence_set nil)
    (convergent_subset formula-decl nil convergence_set nil)
    (difference_subset formula-decl nil sets_lemmas nil))
   shostak))
 (convergent_disjoint_union 0
  (convergent_disjoint_union-1 nil 3406356330
   ("" (skosimp)
    (("" (expand "convergent?")
      (("" (flatten)
        ((""
          (case-replace
           "nonzero_elts(g!1, union(X!1, Y!1))=union(nonzero_elts(g!1, X!1),nonzero_elts(g!1, Y!1))")
          (("1" (hide -1)
            (("1" (rewrite "countable_union")
              (("1"
                (lemma "convergent_disjoint_union"
                 ("X" "nonzero_elts(g!1, X!1)" "Y"
                  "nonzero_elts(g!1, Y!1)" "g" "g!1"))
                (("1" (assert)
                  (("1" (hide-all-but (-1 1))
                    (("1" (expand "disjoint?")
                      (("1" (expand "intersection")
                        (("1" (expand "empty?")
                          (("1" (expand "member")
                            (("1" (expand "nonzero_elts")
                              (("1"
                                (skosimp)
                                (("1"
                                  (inst - "x!1")
                                  (("1" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (hide-all-but 1)
            (("2" (apply-extensionality :hide? t)
              (("2" (expand "nonzero_elts")
                (("2" (expand "union")
                  (("2" (expand "member")
                    (("2" (case-replace "g!1(x!1)=0")
                      (("1" (assert) nil nil) ("2" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((convergent? const-decl "bool" convergence_set nil)
    (T formal-type-decl nil convergence_set nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (nonzero_elts const-decl "set[T]" convergence_set nil)
    (union const-decl "set" sets nil)
    (countable_union judgement-tcc nil countable_props "sets_aux/")
    (is_countable const-decl "bool" countability "sets_aux/")
    (countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (disjoint? const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil)
    (convergent_disjoint_union formula-decl nil countable_convergence
     nil))
   shostak))
 (convergent_union 0
  (convergent_union-1 nil 3406355915
   ("" (skosimp)
    ((""
      (lemma "convergent_difference" ("X" "X!1" "Y" "Y!1" "g" "g!1"))
      (("" (assert)
        (("" (lemma "difference_disjoint" ("a" "Y!1" "b" "X!1"))
          ((""
            (lemma "convergent_disjoint_union"
             ("X" "Y!1" "Y" "difference(X!1, Y!1)" "g" "g!1"))
            (("" (assert)
              (("" (rewrite "union_difference" -1 :dir rl)
                (("" (rewrite "union_commutative") nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil convergence_set nil)
    (convergent_difference formula-decl nil convergence_set nil)
    (difference_disjoint formula-decl nil sets_lemmas nil)
    (union_commutative formula-decl nil sets_lemmas nil)
    (union_difference formula-decl nil sets_lemmas nil)
    (convergent_disjoint_union formula-decl nil convergence_set nil)
    (difference const-decl "set" sets nil))
   shostak))
 (convergent_add 0
  (convergent_add-1 nil 3406355712
   ("" (skosimp)
    (("" (rewrite "add_as_union")
      ((""
        (lemma "convergent_union"
         ("g" "g!1" "X" "X!1" "Y" "singleton(t!1)"))
        (("" (assert)
          (("" (hide-all-but 1)
            (("" (expand "convergent?")
              (("" (case-replace "g!1(t!1)=0")
                (("1"
                  (case-replace
                   "nonzero_elts(g!1, singleton(t!1))=emptyset[T]")
                  (("1" (rewrite "countable_emptyset")
                    (("1"
                      (rewrite
                       "countable_convergence.convergent_empty")
                      nil nil))
                    nil)
                   ("2" (hide 2)
                    (("2" (apply-extensionality :hide? t)
                      (("2" (grind) nil nil)) nil))
                    nil))
                  nil)
                 ("2"
                  (case-replace
                   "nonzero_elts(g!1, singleton(t!1))=singleton(t!1)")
                  (("1" (rewrite "countable_singleton")
                    (("1"
                      (rewrite
                       "countable_convergence.convergent_singleton")
                      nil nil))
                    nil)
                   ("2" (hide 3)
                    (("2" (apply-extensionality :hide? t)
                      (("2" (grind) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((add_as_union formula-decl nil sets_lemmas nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil convergence_set nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" convergence_set nil)
    (nonempty_union2 application-judgement "(nonempty?)" sets nil)
    (convergent? const-decl "bool" convergence_set nil)
    (convergent_singleton formula-decl nil countable_convergence nil)
    (countable_singleton formula-decl nil countable_props "sets_aux/")
    (emptyset const-decl "set" sets nil)
    (nonzero_elts const-decl "set[T]" convergence_set nil)
    (finite_emptyset name-judgement "finite_set[T]" convergence_set
     nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set" finite_sets nil)
    (convergent_empty formula-decl nil countable_convergence nil)
    (countable_emptyset formula-decl nil countable_props "sets_aux/")
    (/= const-decl "boolean" notequal nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (convergent_union formula-decl nil convergence_set nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" 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))
   shostak))
 (convergent_remove 0
  (convergent_remove-1 nil 3406355843
   ("" (skosimp)
    ((""
      (lemma "convergent_subset"
       ("X" "remove(t!1, X!1)" "Y" "X!1" "g" "g!1"))
      (("" (rewrite "subset_remove") (("" (assert) nil nil)) nil))
      nil))
    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)
    (remove 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-type-decl nil convergence_set nil)
    (convergent_subset formula-decl nil convergence_set nil)
    (subset_remove formula-decl nil sets_lemmas nil))
   shostak))
 (convergent_abs 0
  (convergent_abs-1 nil 3406355601
   ("" (skosimp)
    (("" (expand "convergent?")
      ((""
        (case-replace
         "nonzero_elts(abs(g!1), X!1)=nonzero_elts(g!1, X!1)")
        (("1" (hide -1)
          (("1" (rewrite "convergent_abs")
            (("1" (split)
              (("1" (flatten) (("1" (assert) nil nil)) nil)
               ("2" (flatten) (("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil)
         ("2" (hide 2)
          (("2" (apply-extensionality :hide? t)
            (("2" (expand "nonzero_elts") (("2" (grind) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((convergent? const-decl "bool" convergence_set nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (/= const-decl "boolean" notequal nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (convergent_abs formula-decl nil countable_convergence nil)
    (is_countable const-decl "bool" countability "sets_aux/")
    (countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (abs const-decl "[T -> nonneg_real]" real_fun_ops "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (nonzero_elts const-decl "set[T]" convergence_set 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)
    (= const-decl "[T, T -> boolean]" equalities 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-type-decl nil convergence_set nil))
   shostak)))


¤ Dauer der Verarbeitung: 0.70 Sekunden  (vorverarbeitet)  ¤



zum Wurzelverzeichnis wechseln
Diese Quellcodebibliothek enthält Beispiele in vielen Programmiersprachen. Man kann per Verzeichnistruktur darin navigieren. Der Code wird farblich markiert angezeigt.
zum Wurzelverzeichnis wechseln
sprechenden Kalenders

in der Quellcodebibliothek suchen




Laden

Fehler beim Verzeichnis:


in der Quellcodebibliothek suchen

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff