Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: deriv_domain_def.pvs Sprache: Lisp

Original von: PVS^©

(sigma_countable
(sigma_TCC1 0
  (sigma_TCC1-1 nil 3322368543
   ("" (skosimp)
    (("" (lemma "nonempty_card" ("S" "X!1"))
      (("1" (expand "nonempty?") (("1" (assert) nil nil)) nil)
       ("2" (propax) nil nil))
      nil))
    nil)
   ((T formal-type-decl nil sigma_countable nil)
    (countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (is_countable const-decl "bool" countability "sets_aux/")
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nonempty_card formula-decl nil finite_sets nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nonempty? const-decl "bool" sets nil))
   shostak))
(sigma_TCC2 0
  (sigma_TCC2-1 nil 3322368543
   ("" (skosimp)
    (("" (lemma "nonempty_card" ("S" "X!1"))
      (("1" (expand "nonempty?") (("1" (assert) nil nil)) nil)
       ("2" (propax) nil nil))
      nil))
    nil)
   ((T formal-type-decl nil sigma_countable nil)
    (countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (is_countable const-decl "bool" countability "sets_aux/")
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (nonempty_card formula-decl nil finite_sets nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nonempty? const-decl "bool" sets nil))
   shostak))
(sigma_TCC3 0
  (sigma_TCC3-1 nil 3322368684
   ("" (skosimp)
    (("" (skosimp) (("" (typepred "y!1") (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (< const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (T formal-type-decl nil sigma_countable nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Card const-decl "nat" finite_sets nil)
    (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
    (is_countable const-decl "bool" countability "sets_aux/")
    (countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (below type-eq-decl nil nat_types nil))
   shostak))
(sigma_TCC4 0
  (sigma_TCC4-1 nil 3322368684
   ("" (skosimp) (("" (rewrite "countably_infinite_def") nil nil)) nil)
   ((countably_infinite_def formula-decl nil countable_props
     "sets_aux/")
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (is_countable const-decl "bool" countability "sets_aux/")
    (countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (T formal-type-decl nil sigma_countable nil))
   shostak))
(sigma_TCC5 0
  (sigma_TCC5-1 nil 3405668249
   ("" (skosimp)
    (("" (typepred "f!1")
      (("" (expand "convergent?")
        (("" (assert)
          (("" (expand "o")
            ((""
              (name-replace "FF"
               "LAMBDA (x: nat): f!1(denumerable_enumeration(X!1)(x))")
              (("1" (expand "absconvergent?")
                (("1" (hide 1 2)
                  (("1"
                    (lemma "absconvergent_series_is_convergent"
                     ("x" "FF"))
                    (("1" (expand "convergent?")
                      (("1" (propax) nil nil)) nil)
                     ("2" (expand "absconvergent?")
                      (("2" (propax) nil nil)) nil))
                    nil))
                  nil))
                nil)
               ("2" (assert)
                (("2" (typepred "X!1")
                  (("2" (rewrite "countably_infinite_def") nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((convergent? const-decl "bool" countable_convergence 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)
    (countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (is_countable const-decl "bool" countability "sets_aux/")
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil sigma_countable nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans 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)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (is_countably_infinite const-decl "bool" countability "sets_aux/")
    (countably_infinite_set type-eq-decl nil countability "sets_aux/")
    (denumerable_enumeration const-decl "[nat -> (X)]"
     denumerable_enumeration nil)
    (absconvergent_series nonempty-type-eq-decl nil absconv_series
     "series/")
    (sequence type-eq-decl nil sequences nil)
    (absconvergent_series_is_convergent judgement-tcc nil
     absconv_series "series/")
    (absconvergent? const-decl "bool" absconv_series "series/")
    (countably_infinite_def formula-decl nil countable_props
     "sets_aux/")
    (O const-decl "T3" function_props nil)
    (convergent? const-decl "bool" convergence_sequences "analysis/"))
   nil))
(sigma_empty_TCC1 0
  (sigma_empty_TCC1-1 nil 3322640566 ("" (grind) nil nil)
   ((injective? const-decl "bool" functions nil)
    (surjective? const-decl "bool" functions nil)
    (bijective? const-decl "bool" functions nil)
    (T formal-type-decl nil sigma_countable nil)
    (denumerable_enumeration const-decl "[nat -> (X)]"
     denumerable_enumeration nil)
    (O const-decl "T3" function_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (abs const-decl "sequence[real]" series "series/")
    (sigma def-decl "real" sigma "reals/")
    (series const-decl "sequence[real]" series "series/")
    (convergence const-decl "bool" convergence_sequences "analysis/")
    (convergent? const-decl "bool" convergence_sequences "analysis/")
    (absconvergent? const-decl "bool" absconv_series "series/")
    (convergent? const-decl "bool" countable_convergence nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (finite_emptyset name-judgement "finite_set[T]" sigma_countable
     nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set" finite_sets nil))
   shostak))
(sigma_empty 0
  (sigma_empty-1 nil 3322641284
   ("" (skosimp)
    (("" (expand "sigma") (("" (rewrite "emptyset_is_empty?") nil nil))
      nil))
    nil)
   ((finite_emptyset name-judgement "finite_set" finite_sets nil)
    (finite_emptyset name-judgement "finite_set[T]" countable_props
     "sets_aux/")
    (finite_emptyset name-judgement "finite_set[T]" sigma_countable
     nil)
    (sigma const-decl "real" sigma_countable nil)
    (T formal-type-decl nil sigma_countable nil)
    (emptyset 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)
    (emptyset_is_empty? formula-decl nil sets_lemmas nil))
   shostak))
(sigma_finite_TCC1 0
  (sigma_finite_TCC1-2 nil 3508520761
   ("" (skosimp)
    (("" (typepred "F!1")
      (("" (expand "convergent?") (("" (propax) nil nil)) nil)) nil))
    nil)
   ((non_empty_finite_set type-eq-decl nil finite_sets nil)
    (empty? const-decl "bool" sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil sigma_countable nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (convergent? const-decl "bool" countable_convergence nil))
   nil)
  (sigma_finite_TCC1-1 nil 3322640566
   ("" (skosimp*)
    (("" (typepred "F!1")
      (("" (lemma "finite_countable" ("x" "F!1"))
        (("" (propax) nil nil)) nil))
      nil))
    nil)
   ((non_empty_finite_set type-eq-decl nil finite_sets nil)
    (empty? const-decl "bool" sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (finite_countable judgement-tcc nil countable_props "sets_aux/"))
   shostak))
(sigma_finite_TCC2 0
  (sigma_finite_TCC2-2 nil 3508521550
   ("" (skosimp)
    (("" (assert)
      (("" (typepred "n!1")
        (("" (replace -2)
          (("" (assert)
            (("" (typepred "F!1")
              (("" (lemma "nonempty_card" ("S" "F!1"))
                (("" (expand "nonempty?") (("" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (T formal-type-decl nil sigma_countable nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (empty? const-decl "bool" sets nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (nonempty? const-decl "bool" sets nil)
    (nonempty_card formula-decl nil finite_sets nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans 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))
   nil)
  (sigma_finite_TCC2-1 nil 3322640566
   ("" (skosimp)
    (("" (typepred "F!1")
      (("" (expand "convergent?") (("" (propax) nil nil)) nil)) nil))
    nil)
   ((non_empty_finite_set type-eq-decl nil finite_sets nil)
    (empty? const-decl "bool" sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (convergent? const-decl "bool" countable_convergence nil))
   shostak))
(sigma_finite_TCC3 0
  (sigma_finite_TCC3-1 nil 3322640566
   ("" (skosimp)
    (("" (assert)
      (("" (typepred "n!1")
        (("" (replace -2)
          (("" (assert)
            (("" (typepred "F!1")
              (("" (lemma "nonempty_card" ("S" "F!1"))
                (("" (expand "nonempty?") (("" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (T formal-type-decl nil sigma_countable nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (empty? const-decl "bool" sets nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (nonempty? const-decl "bool" sets nil)
    (nonempty_card 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)
    (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))
   shostak))
(sigma_finite_TCC4 0
  (sigma_finite_TCC4-2 nil 3508520831
   ("" (skosimp*) (("" (replace -1) (("" (assert) nil nil)) nil)) nil)
   ((int_minus_int_is_int application-judgement "int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_plus_int_is_int application-judgement "int" integers nil))
   nil)
  (sigma_finite_TCC4-1 nil 3322640566
   ("" (skosimp)
    (("" (typepred "F!1")
      (("" (rewrite "empty_card") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((non_empty_finite_set type-eq-decl nil finite_sets nil)
    (empty? const-decl "bool" sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (empty_card formula-decl nil finite_sets nil))
   shostak))
(sigma_finite_TCC5 0
  (sigma_finite_TCC5-1 nil 3322640566
   ("" (skosimp*) (("" (replace -1) (("" (assert) nil nil)) nil)) nil)
   ((int_minus_int_is_int application-judgement "int" integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   shostak))
(sigma_finite 0
  (sigma_finite-1 nil 3322641469
   ("" (skosimp)
    (("" (assert)
      (("" (expand "sigma" 1 1) (("" (propax) nil nil)) nil)) nil))
    nil)
   ((int_minus_int_is_int application-judgement "int" integers nil)
    (sigma const-decl "real" sigma_countable nil))
   shostak))
(sigma_singleton_TCC1 0
  (sigma_singleton_TCC1-1 nil 3351597966 ("" (grind) nil nil)
   ((injective? const-decl "bool" functions nil)
    (surjective? const-decl "bool" functions nil)
    (bijective? const-decl "bool" functions nil)
    (T formal-type-decl nil sigma_countable nil)
    (denumerable_enumeration const-decl "[nat -> (X)]"
     denumerable_enumeration nil)
    (O const-decl "T3" function_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (abs const-decl "sequence[real]" series "series/")
    (sigma def-decl "real" sigma "reals/")
    (series const-decl "sequence[real]" series "series/")
    (convergence const-decl "bool" convergence_sequences "analysis/")
    (convergent? const-decl "bool" convergence_sequences "analysis/")
    (absconvergent? const-decl "bool" absconv_series "series/")
    (convergent? const-decl "bool" countable_convergence nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" sigma_countable nil))
   nil))
(sigma_singleton 0
  (sigma_singleton-1 nil 3351597967
   ("" (skosimp)
    (("" (lemma "sigma_finite" ("F" "singleton(t!1)" "g" "g!1"))
      (("" (rewrite "card_singleton")
        (("" (assert)
          (("" (replace -1)
            (("" (hide -1)
              (("" (expand "sigma")
                (("" (expand "o ")
                  ((""
                    (typepred "finite_enumeration(singleton(t!1))(0)")
                    (("" (expand "singleton")
                      (("" (assert)
                        (("" (replace -1)
                          (("" (expand "sigma") (("" (propax) nil nil))
                            nil))
                          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)
    (singleton const-decl "(singleton?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (empty? const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil sigma_countable nil)
    (sigma_finite formula-decl nil sigma_countable nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set[T]" sigma_countable nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (O const-decl "T3" function_props nil)
    (real_plus_real_is_real application-judgement "real" 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)
    (< const-decl "bool" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Card const-decl "nat" finite_sets nil)
    (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
    (below type-eq-decl nil nat_types nil)
    (finite_enumeration const-decl "[below[card(X)] -> (X)]"
     finite_enumeration nil)
    (sigma def-decl "real" sigma "reals/")
    (card_singleton formula-decl nil finite_sets nil))
   shostak))
(sigma_infinite_TCC1 0
  (sigma_infinite_TCC1-1 nil 3322642826
   ("" (skosimp)
    (("" (typepred "f!1")
      (("" (expand "convergent?")
        (("" (typepred "X!1")
          (("" (rewrite "countably_infinite_def")
            (("" (flatten)
              (("" (assert)
                ((""
                  (lemma "absconvergent_series_is_convergent"
                   ("x" "(o[nat, T, real]
                               (f!1, denumerable_enumeration[T](X!1)))"))
                  (("" (assert)
                    (("" (expand "convergent?") (("" (propax) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((countably_infinite_set type-eq-decl nil countability "sets_aux/")
    (is_countably_infinite const-decl "bool" countability "sets_aux/")
    (convergent? const-decl "bool" countable_convergence 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)
    (countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (is_countable const-decl "bool" countability "sets_aux/")
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil sigma_countable nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (denumerable_enumeration const-decl "[nat -> (X)]"
     denumerable_enumeration nil)
    (O const-decl "T3" function_props nil)
    (absconvergent_series nonempty-type-eq-decl nil absconv_series
     "series/")
    (absconvergent? const-decl "bool" absconv_series "series/")
    (sequence type-eq-decl nil sequences 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)
    (absconvergent_series_is_convergent judgement-tcc nil
     absconv_series "series/")
    (countably_infinite_def formula-decl nil countable_props
     "sets_aux/")
    (convergent? const-decl "bool" convergence_sequences "analysis/"))
   shostak))
(sigma_infinite 0
  (sigma_infinite-1 nil 3322642960
   ("" (skosimp)
    (("" (typepred "X!1")
      (("" (expand "sigma" 1 1)
        (("" (lemma "infinite_countably_infinite")
          (("" (inst - "X!1")
            (("" (assert)
              (("" (lift-if 2)
                (("" (case-replace "empty?(X!1)")
                  (("1" (hide 2)
                    (("1" (expand "is_countably_infinite")
                      (("1" (skosimp)
                        (("1" (typepred "f!2")
                          (("1"
                            (lemma
                             "bijective_inverse_exists[(X!1),nat]"
                             ("f" "f!2"))
                            (("1" (expand "exists1")
                              (("1"
                                (flatten)
                                (("1"
                                  (skolem -1 ("gg"))
                                  (("1"
                                    (expand "empty?")
                                    (("1"
                                      (inst - "gg(0)")
                                      (("1"
                                        (expand "member")
                                        (("1" (propax) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((countably_infinite_set type-eq-decl nil countability "sets_aux/")
    (is_countably_infinite const-decl "bool" countability "sets_aux/")
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil sigma_countable nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (infinite_countably_infinite judgement-tcc nil countable_props
     "sets_aux/")
    (empty? const-decl "bool" sets nil)
    (bijective? const-decl "bool" functions 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)
    (exists1 const-decl "bool" exists1 nil)
    (member const-decl "bool" sets nil)
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (sigma const-decl "real" sigma_countable nil))
   shostak))
(nonempty_countable_is_countable 0
  (nonempty_countable_is_countable-1 nil 3323139930
   ("" (skosimp)
    (("" (typepred "x!1")
      (("" (expand "nonempty_countable?") (("" (flatten) nil nil))
        nil))
      nil))
    nil)
   ((nonempty_countable type-eq-decl nil sigma_countable nil)
    (nonempty_countable? const-decl "bool" sigma_countable nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil sigma_countable nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
(nonempty_countable_is_nonempty 0
  (nonempty_countable_is_nonempty-1 nil 3323139930
   ("" (skosimp)
    (("" (typepred "x!1")
      (("" (expand "nonempty_countable?") (("" (flatten) nil nil))
        nil))
      nil))
    nil)
   ((nonempty_countable type-eq-decl nil sigma_countable nil)
    (nonempty_countable? const-decl "bool" sigma_countable nil)
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil sigma_countable nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
(sigma_disjoint_union_TCC1 0
  (sigma_disjoint_union_TCC1-1 nil 3323139931
   ("" (skosimp*)
    (("" (typepred "f!1")
      (("" (lemma "convergent_subset")
        (("" (inst - "X!1" "union(X!1, Y!1)" "f!1")
          (("" (split)
            (("1" (propax) nil nil)
             ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)
             ("3" (propax) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((union const-decl "set" sets nil)
    (convergent? const-decl "bool" countable_convergence 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)
    (countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (is_countable const-decl "bool" countability "sets_aux/")
    (set type-eq-decl nil sets nil)
    (T formal-type-decl nil sigma_countable nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (countable_union application-judgement "countable_set[T]"
     sigma_countable nil)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (convergent_subset formula-decl nil countable_convergence nil))
   shostak))
(sigma_disjoint_union_TCC2 0
  (sigma_disjoint_union_TCC2-1 nil 3323139931
   ("" (skosimp)
    ((""
      (lemma "sigma_disjoint_union_TCC1"
       ("X" "Y!1" "Y" "X!1" "f" "f!1"))
      (("1" (assert)
        (("1" (hide 2)
          (("1" (expand "disjoint?")
            (("1" (rewrite "intersection_commutative") nil nil)) nil))
          nil))
        nil)
       ("2" (typepred "f!1")
        (("2" (hide -2 2) (("2" (rewrite "union_commutative") nil nil))
          nil))
        nil))
      nil))
    nil)
   ((union const-decl "set" sets nil)
    (convergent? const-decl "bool" countable_convergence 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)
    (countable_set nonempty-type-eq-decl nil countability "sets_aux/")
    (is_countable const-decl "bool" countability "sets_aux/")
    (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 sigma_countable nil)
    (sigma_disjoint_union_TCC1 subtype-tcc nil sigma_countable nil)
    (countable_union application-judgement "countable_set[T]"
     sigma_countable nil)
    (intersection_commutative formula-decl nil sets_lemmas nil)
    (disjoint? const-decl "bool" sets nil)
    (countable_intersection1 application-judgement "countable_set[T]"
     sigma_countable nil)
    (union_commutative formula-decl nil sets_lemmas nil)
    (NOT const-decl "[bool -> bool]" booleans nil))
   shostak))
(sigma_disjoint_union 0
  (sigma_disjoint_union-1 nil 3351662957
   (""
    (case "FORALL (X:finite_set[T], Y:countably_infinite_set[T], f:(convergent?(union(X, Y)))):
        disjoint?(X, Y) IMPLIES
         sigma(union(X, Y), f) = sigma(X, f) + sigma(Y, f)")
    (("1" (skosimp)
      (("1" (typepred "X!1")
        (("1" (typepred "Y!1")
          (("1" (case "is_finite(X!1)")
            (("1" (case "is_finite(Y!1)")
              (("1" (hide -5 -3 -4)
                (("1" (name "NX" "card(X!1)")
                  (("1" (name "NY" "card(Y!1)")
                    (("1" (case-replace "X!1=emptyset[T]")
                      (("1" (rewrite "union_commutative" 1)
                        (("1" (rewrite "union_empty")
                          (("1" (rewrite "sigma_empty")
                            (("1" (assert) nil nil)) nil))
                          nil))
                        nil)
                       ("2" (case-replace "Y!1=emptyset[T]")
                        (("1" (rewrite "sigma_empty")
                          (("1" (rewrite "union_empty")
                            (("1" (assert) nil nil)) nil))
                          nil)
                         ("2" (rewrite "emptyset_is_empty?" 1 :dir rl)
                          (("2"
                            (rewrite "emptyset_is_empty?" 2 :dir rl)
                            (("2" (typepred "f!1")
                              (("2"
                                (expand "sigma")
                                (("2"
                                  (assert)
                                  (("2"
                                    (lemma "finite_union[T]")
                                    (("2"
                                      (inst - "X!1" "Y!1")
                                      (("2"
                                        (assert)
                                        (("2"
                                          (case-replace
                                           "empty?(union(X!1, Y!1))")
                                          (("1"
                                            (hide-all-but (1 2 -1))
                                            (("1"
                                              (expand "union")
                                              (("1"
                                                (expand "empty?")
                                                (("1"
                                                  (skosimp*)
                                                  (("1"
                                                    (expand "member")
                                                    (("1"
                                                      (inst - "x!1")
                                                      (("1"
                                                        (flatten)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (assert)
                                            (("2"
                                              (lemma
                                               "card_disj_union"
                                               ("A" "X!1" "B" "Y!1"))
                                              (("2"
                                                (assert)
                                                (("2"
                                                  (replace -1)
                                                  (("2"
                                                    (replace -4)
                                                    (("2"
                                                      (replace -5)
                                                      (("2"
                                                        (lemma
                                                         "series_bijection")
                                                        (("2"
                                                          (name
                                                           "PHI"
                                                           "LAMBDA (n:[below[card(union(X!1,Y!1))]]): IF n < card(X!1) THEN finite_enumeration(X!1)(n) ELSE finite_enumeration(Y!1)(n-card(X!1)) ENDIF")
                                                          (("1"
                                                            (lemma
                                                             "finite_enumeration_bij"
                                                             ("X"
                                                              "union(X!1,Y!1)"))
                                                            (("1"
                                                              (lemma
                                                               "finite_enumeration_bij"
                                                               ("X"
                                                                "X!1"))
                                                              (("1"
                                                                (lemma
                                                                 "finite_enumeration_bij"
                                                                 ("X"
                                                                  "Y!1"))
                                                                (("1"
                                                                  (name-replace
                                                                   "FX"
                                                                   "finite_enumeration(X!1)")
                                                                  (("1"
                                                                    (name-replace
                                                                     "FY"
                                                                     "finite_enumeration(Y!1)")
                                                                    (("1"
                                                                      (name-replace
                                                                       "FXY"
                                                                       "finite_enumeration(union(X!1,Y!1))")
                                                                      (("1"
                                                                        (case
                                                                         "bijective?[below[card[T](union(X!1,Y!1))],(union(X!1,Y!1))](PHI)")
                                                                        (("1"
                                                                          (lemma
                                                                           "bijective_inverse_exists[below[card[T](union(X!1, Y!1))], (union(X!1, Y!1))]"
                                                                           ("f"
                                                                            "FXY"))
                                                                          (("1"
                                                                            (expand
                                                                             "exists1")
                                                                            (("1"
                                                                              (flatten)
                                                                              (("1"
                                                                                (skolem
                                                                                 -
                                                                                 ("CXY"))
                                                                                (("1"
                                                                                  (hide
                                                                                   -2)
                                                                                  (("1"
                                                                                    (expand
                                                                                     "series")
                                                                                    (("1"
                                                                                      (hide
                                                                                       -6
                                                                                       -7)
                                                                                      (("1"
                                                                                        (lemma
                                                                                         "sigma_bijection[below[card(union(X!1, Y!1))]]"
                                                                                         ("low"
                                                                                          "0"
                                                                                          "high"
                                                                                          "NX+NY-1"
                                                                                          "F"
                                                                                          "f!1 o FXY"))
                                                                                        (("1"
                                                                                          (split
                                                                                           -1)
                                                                                          (("1"
                                                                                            (lemma
                                                                                             "bij_inv_is_bij_alt[below[card[T](union(X!1, Y!1))], (union(X!1, Y!1))]"
                                                                                             ("f"
                                                                                              "FXY"
                                                                                              "g"
                                                                                              "CXY"))
                                                                                            (("1"
                                                                                              (lemma
                                                                                               "composition_bijective[below[card[T](union(X!1,Y!1))],(union(X!1,Y!1)),below[card[T](union(X!1, Y!1))]]"
                                                                                               ("f1"
                                                                                                "PHI"
                                                                                                "f2"
                                                                                                "CXY"))
                                                                                              (("1"
                                                                                                (inst
                                                                                                 -
                                                                                                 "CXY o PHI")
                                                                                                (("1"
                                                                                                  (case-replace
                                                                                                   "sigma[subrange_T[below[card(union(X!1, Y!1))]](0, NX - 1 + NY)]
           (0, NX + NY - 1,
            f!1 o FXY o
             restrict
                 [below[card[T](union[T](X!1, Y!1))],
                  subrange_T[below[card[T](union[T](X!1, Y!1))]](0,
                                                                 NX - 1
                                                                 +
                                                                 NY),
                  below[card[T](union[T](X!1, Y!1))]]
                 (CXY o PHI)) = sigma[below[card(union(X!1, Y!1))]](0, NX + NY - 1, f!1 o PHI)")
                                                                                                  (("1"
                                                                                                    (case-replace
                                                                                                     "sigma[subrange_T[below[card(union(X!1, Y!1))]](0, NX - 1 + NY)]
          (0, NX + NY - 1,
           restrict
               [below[card(union(X!1, Y!1))],
                subrange_T[below[card(union(X!1, Y!1))]](0, NX - 1 + NY),
                real]
               (f!1 o FXY)) = sigma[below[card(union(X!1, Y!1))]](0, NX + NY - 1, f!1 o FXY)")
                                                                                                    (("1"
                                                                                                      (replace
                                                                                                       -5
                                                                                                       4)
                                                                                                      (("1"
                                                                                                        (hide-all-but
                                                                                                         (4
                                                                                                          2
                                                                                                          3
                                                                                                          -14
                                                                                                          -15
                                                                                                          -11))
                                                                                                        (("1"
                                                                                                          (lemma
                                                                                                           "nonempty_card"
                                                                                                           ("S"
                                                                                                            "X!1"))
                                                                                                          (("1"
                                                                                                            (lemma
                                                                                                             "nonempty_card"
                                                                                                             ("S"
                                                                                                              "Y!1"))
                                                                                                            (("1"
                                                                                                              (expand
                                                                                                               "nonempty?")
                                                                                                              (("1"
                                                                                                                (assert)
                                                                                                                (("1"
                                                                                                                  (case
                                                                                                                   "forall (n:nat): n <= NY-1 => sigma[below[card(union(X!1, Y!1))]](0, NX + n, f!1 o PHI) =
       sigma[below[card(Y!1)]](0, n, f!1 o FY) +
        sigma[below[card(X!1)]](0, NX - 1, f!1 o FX)")
                                                                                                                  (("1"
                                                                                                                    (inst
                                                                                                                     -
                                                                                                                     "NY-1")
                                                                                                                    (("1"
                                                                                                                      (assert)
                                                                                                                      nil
                                                                                                                      nil))
                                                                                                                    nil)
                                                                                                                   ("2"
                                                                                                                    (hide
                                                                                                                     2
                                                                                                                     3
                                                                                                                     4)
                                                                                                                    (("2"
                                                                                                                      (induct
                                                                                                                       "n")
                                                                                                                      (("1"
                                                                                                                        (assert)
                                                                                                                        (("1"
                                                                                                                          (expand
                                                                                                                           "sigma"
                                                                                                                           1
                                                                                                                           2)
                                                                                                                          (("1"
                                                                                                                            (expand
                                                                                                                             "sigma"
                                                                                                                             1
                                                                                                                             1)
                                                                                                                            (("1"
                                                                                                                              (expand
                                                                                                                               "PHI"
                                                                                                                               1
                                                                                                                               1)
                                                                                                                              (("1"
                                                                                                                                (expand
                                                                                                                                 "FY"
                                                                                                                                 1)
                                                                                                                                (("1"
                                                                                                                                  (expand
                                                                                                                                   "o"
                                                                                                                                   1
                                                                                                                                   3)
                                                                                                                                  (("1"
                                                                                                                                    (expand
                                                                                                                                     "o"
                                                                                                                                     1
                                                                                                                                     1)
                                                                                                                                    (("1"
                                                                                                                                      (assert)
                                                                                                                                      (("1"
                                                                                                                                        (replace
                                                                                                                                         -5
                                                                                                                                         1)
                                                                                                                                        (("1"
                                                                                                                                          (assert)
                                                                                                                                          (("1"
                                                                                                                                            (hide
                                                                                                                                             -1
                                                                                                                                             -3
                                                                                                                                             -4)
                                                                                                                                            (("1"
                                                                                                                                              (case
                                                                                                                                               "forall (n:nat): n<=NX-1 => sigma(0, n, f!1 o PHI) =
       sigma[below[card(X!1)]](0, n, f!1 o FX)")
                                                                                                                                              (("1"
                                                                                                                                                (inst
                                                                                                                                                 -
                                                                                                                                                 "NX-1")
                                                                                                                                                (("1"
                                                                                                                                                  (assert)
                                                                                                                                                  (("1"
                                                                                                                                                    (expand
                                                                                                                                                     "sigma"
                                                                                                                                                     1
                                                                                                                                                     2)
                                                                                                                                                    (("1"
                                                                                                                                                      (propax)
                                                                                                                                                      nil
                                                                                                                                                      nil))
                                                                                                                                                    nil))
                                                                                                                                                  nil))
                                                                                                                                                nil)
                                                                                                                                               ("2"
                                                                                                                                                (hide
                                                                                                                                                 2)
                                                                                                                                                (("2"
                                                                                                                                                  (induct
                                                                                                                                                   "n")
                                                                                                                                                  (("1"
                                                                                                                                                    (expand
                                                                                                                                                     "sigma")
                                                                                                                                                    (("1"
                                                                                                                                                      (expand
                                                                                                                                                       "FX")
                                                                                                                                                      (("1"
                                                                                                                                                        (expand
                                                                                                                                                         "PHI")
                                                                                                                                                        (("1"
                                                                                                                                                          (expand
                                                                                                                                                           "o ")
                                                                                                                                                          (("1"
                                                                                                                                                            (expand
                                                                                                                                                             "sigma")
                                                                                                                                                            (("1"
                                                                                                                                                              (propax)
                                                                                                                                                              nil
                                                                                                                                                              nil))
                                                                                                                                                            nil))
                                                                                                                                                          nil))
                                                                                                                                                        nil))
                                                                                                                                                      nil))
                                                                                                                                                    nil)
                                                                                                                                                   ("2"
                                                                                                                                                    (skosimp*)
                                                                                                                                                    (("2"
                                                                                                                                                      (assert)
                                                                                                                                                      (("2"
                                                                                                                                                        (expand
                                                                                                                                                         "sigma"
                                                                                                                                                         1)
                                                                                                                                                        (("2"
                                                                                                                                                          (assert)
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.109 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.