Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/sets_aux/   (Beweissystem der NASA Version 6.0.9©)  Datei vom 28.9.2014 mit Größe 10 kB image not shown  

Quelle  card_finite.prf   Sprache: Lisp

 
(card_finite
 (card_less_than 0
  (card_less_than-1 nil 3316967388
   ("" (skolem!)
    (("" (expand "card_lt")
      (("" (lemma "injection_n_to_m_var")
        (("" (inst - "card(F1!1)" "card(F2!1)")
          (("" (ground)
            (("1" (use "bij_exists[T2]")
              (("1" (use "card_bij_inv[T1]")
                (("1" (assert)
                  (("1" (expand "bijective?")
                    (("1" (skosimp*)
                      (("1"
                        (use "composition_injective[(F2!1), below(card(F2!1)), below(card(F1!1))]")
                        (("1"
                          (use "composition_injective[(F2!1), below(card(F1!1)), (F1!1)]")
                          (("1" (inst?) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (use "card_bij_inv[T2]" ("N" "card(F2!1)"))
              (("2" (assert)
                (("2" (use "bij_exists[T1]")
                  (("2" (expand "bijective?")
                    (("2" (skosimp*)
                      (("2"
                        (use "composition_injective[below(card(F2!1)), (F2!1), (F1!1)]")
                        (("2"
                          (use "composition_injective[below(card(F2!1)), (F1!1), below(card(F1!1))]")
                          (("2" (inst?) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((card_lt const-decl "bool" card_comp_set nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (T1 formal-type-decl nil card_finite 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)
    (T2 formal-type-decl nil card_finite nil)
    (f!1 skolem-const-decl "[(F1!1) -> below(card(F1!1))]" card_finite
     nil)
    (f!3 skolem-const-decl "[(F2!1) -> (F1!1)]" card_finite nil)
    (f!2 skolem-const-decl "[below[card(F2!1)] -> (F2!1)]" card_finite
     nil)
    (bij_exists formula-decl nil finite_sets nil)
    (O const-decl "T3" function_props nil)
    (f!1 skolem-const-decl "[below[card(F1!1)] -> (F1!1)]" card_finite
     nil)
    (below type-eq-decl nil nat_types nil)
    (F1!1 skolem-const-decl "finite_set[T1]" card_finite nil)
    (f!3 skolem-const-decl "[below(card(F2!1)) -> below(card(F1!1))]"
     card_finite nil)
    (F2!1 skolem-const-decl "finite_set[T2]" card_finite nil)
    (injective? const-decl "bool" functions nil)
    (f!2 skolem-const-decl "[(F2!1) -> below(card(F2!1))]" card_finite
     nil)
    (composition_injective judgement-tcc nil function_props nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (bijective? const-decl "bool" functions nil)
    (card_bij_inv formula-decl nil finite_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)
    (injection_n_to_m_var formula-decl nil nat_fun_props nil))
   shostak))
 (card_less_than_equal 0
  (card_less_than_equal-1 nil 3316967904
   ("" (skolem!)
    (("" (expand "card_le")
      (("" (lemma "injection_n_to_m_var")
        (("" (inst - "card(F2!1)" "card(F1!1)")
          (("" (ground)
            (("1" (use "bij_exists[T1]")
              (("1" (use "card_bij_inv[T2]" ("N" "card(F2!1)"))
                (("1" (assert)
                  (("1" (expand "bijective?")
                    (("1" (skosimp*)
                      (("1"
                        (use "composition_injective[(F1!1), below(card(F1!1)), below(card(F2!1))]")
                        (("1"
                          (use "composition_injective[(F1!1), below(card(F2!1)), (F2!1)]")
                          (("1" (inst?) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (use "card_bij_inv[T1]")
              (("2" (assert)
                (("2" (use "bij_exists[T2]")
                  (("2" (expand "bijective?")
                    (("2" (skosimp*)
                      (("2"
                        (use "composition_injective[below(card(F1!1)), (F1!1), (F2!1)]")
                        (("2"
                          (use "composition_injective[below(card(F1!1)), (F2!1), below(card(F2!1))]")
                          (("2" (inst?) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((card_le const-decl "bool" card_comp_set nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (T2 formal-type-decl nil card_finite 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)
    (T1 formal-type-decl nil card_finite nil)
    (f!1 skolem-const-decl "[(F2!1) -> below(card(F2!1))]" card_finite
     nil)
    (f!3 skolem-const-decl "[(F1!1) -> (F2!1)]" card_finite nil)
    (f!2 skolem-const-decl "[below[card(F1!1)] -> (F1!1)]" card_finite
     nil)
    (bij_exists formula-decl nil finite_sets nil)
    (O const-decl "T3" function_props nil)
    (f!1 skolem-const-decl "[below[card(F2!1)] -> (F2!1)]" card_finite
     nil)
    (below type-eq-decl nil nat_types nil)
    (F2!1 skolem-const-decl "finite_set[T2]" card_finite nil)
    (f!3 skolem-const-decl "[below(card(F1!1)) -> below(card(F2!1))]"
     card_finite nil)
    (F1!1 skolem-const-decl "finite_set[T1]" card_finite nil)
    (injective? const-decl "bool" functions nil)
    (f!2 skolem-const-decl "[(F1!1) -> below(card(F1!1))]" card_finite
     nil)
    (composition_injective judgement-tcc nil function_props nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (bijective? const-decl "bool" functions nil)
    (card_bij_inv formula-decl nil finite_sets nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (injection_n_to_m_var formula-decl nil nat_fun_props nil))
   shostak))
 (card_equal 0
  (card_equal-1 nil 3316968155
   ("" (skolem!)
    (("" (use "card_less_than")
      (("" (use "card_less_than_equal")
        (("" (use "card_le_lt_eq")
          (("" (use "card_lt_neq_ngt") (("" (ground) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((card_less_than formula-decl nil card_finite 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)
    (T1 formal-type-decl nil card_finite nil)
    (T2 formal-type-decl nil card_finite nil)
    (card_le_lt_eq formula-decl nil card_comp_set_props 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)
    (card_lt_neq_ngt formula-decl nil card_comp_set_props nil)
    (card_less_than_equal formula-decl nil card_finite nil))
   shostak))
 (card_greater_than_equal 0
  (card_greater_than_equal-1 nil 3316968194
   ("" (skolem!)
    (("" (use "card_less_than")
      (("" (use "card_lt_ge")
        (("" (expand "XOR") (("" (ground) nil nil)) nil)) nil))
      nil))
    nil)
   ((card_less_than formula-decl nil card_finite 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)
    (T1 formal-type-decl nil card_finite nil)
    (T2 formal-type-decl nil card_finite nil)
    (XOR const-decl "bool" xor_def nil)
    (real_ge_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)
    (card_lt_ge formula-decl nil card_comp_set_props nil))
   shostak))
 (card_greater_than 0
  (card_greater_than-1 nil 3316968211
   ("" (skolem!)
    (("" (use "card_less_than_equal")
      (("" (use "card_le_gt")
        (("" (expand "XOR") (("" (ground) nil nil)) nil)) nil))
      nil))
    nil)
   ((card_less_than_equal formula-decl nil card_finite 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)
    (T1 formal-type-decl nil card_finite nil)
    (T2 formal-type-decl nil card_finite nil)
    (XOR const-decl "bool" xor_def nil)
    (real_gt_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)
    (card_le_gt formula-decl nil card_comp_set_props nil))
   shostak)))

100%


¤ Dauer der Verarbeitung: 0.12 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland




Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.