Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Thinking Intellekt

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/sources/formale sprachen/PVS/sets_aux/

Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: card_finite.prf Sprache: Lisp

Original von: PVS^©

(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)))

¤ Dauer der Verarbeitung: 0.24 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

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