Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 

products/sources/formale Sprachen/Java/openjdk-20-36_src/test/jdk/sun/tools/jrunscript/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: common.sh   Sprache: PVS

Untersuchung PVS©
(card_comp_props
 (card_lt_surj 0
  (card_lt_surj-1 nil 3316958745
   ("" (expand "card_lt")
    (("" (prop)
      (("1" (lemma "fun_exists[T2, T1]")
        (("1" (prop)
          (("1" (skolem!)
            (("1" (inst 2 "f!1") (("1" (grind) nil nil)) nil)) nil))
          nil))
        nil)
       ("2" (skolem!)
        (("2" (use "surjective_inverse_exists[T1, T2]")
          (("2" (skolem!)
            (("2" (use "inj_inv_alt[T1, T2]") (("2" (inst?) nil nil))
              nil))
            nil))
          nil))
        nil)
       ("3" (skolem! -2)
        (("3" (use "inv_inj_is_surj[T2, T1]") (("3" (inst?) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((injective? const-decl "bool" functions nil)
    (fun_exists formula-decl nil function_image nil)
    (T2 formal-type-decl nil card_comp_props nil)
    (T1 formal-type-decl nil card_comp_props nil)
    (surjective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (surjective? const-decl "bool" functions nil)
    (f!1 skolem-const-decl "[T1 -> T2]" card_comp_props nil)
    (inj_inv_alt formula-decl nil function_inverse_def nil)
    (g!1 skolem-const-decl "[T2 -> T1]" card_comp_props nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (TRUE const-decl "bool" booleans nil)
    (inv_inj_is_surj judgement-tcc nil function_inverse nil)
    (f!1 skolem-const-decl "[T2 -> T1]" card_comp_props nil)
    (inverse const-decl "D" function_inverse nil)
    (card_lt const-decl "bool" card_comp nil))
   shostak))
 (card_ge_surj 0
  (card_ge_surj-1 nil 3316958898
   ("" (expand "card_ge")
    (("" (split)
      (("1" (flatten)
        (("1" (skolem!)
          (("1" (case "EXISTS (t: T2): TRUE")
            (("1" (use "inv_inj_is_surj[T2, T1]")
              (("1" (inst?) nil nil)) nil)
             ("2" (split)
              (("1" (lemma "fun_exists[T1, T2]")
                (("1" (prop)
                  (("1" (skolem!)
                    (("1" (inst 3 "f!2") (("1" (grind) nil nil)) nil))
                    nil))
                  nil))
                nil)
               ("2" (skolem!) (("2" (inst + "t!1") nil nil)) nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (prop)
        (("1" (skolem!)
          (("1" (inst + "LAMBDA (x: T2): t!1") (("1" (grind) nil nil))
            nil))
          nil)
         ("2" (skolem!)
          (("2" (use "surjective_inverse_exists[T1, T2]")
            (("2" (skolem!)
              (("2" (use "inj_inv_alt[T1, T2]") (("2" (inst?) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((surjective? const-decl "bool" functions nil)
    (fun_exists formula-decl nil function_image nil)
    (T1 formal-type-decl nil card_comp_props nil)
    (inv_inj_is_surj judgement-tcc nil function_inverse nil)
    (f!1 skolem-const-decl "[T2 -> T1]" card_comp_props nil)
    (injective? const-decl "bool" functions nil)
    (inverse const-decl "D" function_inverse nil)
    (T2 formal-type-decl nil card_comp_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (TRUE const-decl "bool" booleans nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (g!1 skolem-const-decl "[T2 -> T1]" card_comp_props nil)
    (inj_inv_alt formula-decl nil function_inverse_def nil)
    (f!1 skolem-const-decl "[T1 -> T2]" card_comp_props nil)
    (surjective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (card_ge const-decl "bool" card_comp nil))
   shostak))
 (card_lt_le 0
  (card_lt_le-1 nil 3316959024
   ("" (expand* "card_lt" "card_le")
    (("" (lemma "injective_dichotomous") (("" (prop) nil nil)) nil))
    nil)
   ((T2 formal-type-decl nil card_comp_props nil)
    (T1 formal-type-decl nil card_comp_props nil)
    (injective_dichotomous formula-decl nil set_dichotomous "orders/")
    (card_lt const-decl "bool" card_comp nil)
    (card_le const-decl "bool" card_comp nil))
   shostak))
 (card_gt_ge 0
  (card_gt_ge-1 nil 3316959049
   ("" (expand* "card_gt" "card_ge")
    (("" (lemma "injective_dichotomous") (("" (prop) nil nil)) nil))
    nil)
   ((T2 formal-type-decl nil card_comp_props nil)
    (T1 formal-type-decl nil card_comp_props nil)
    (injective_dichotomous formula-decl nil set_dichotomous "orders/")
    (card_gt const-decl "bool" card_comp nil)
    (card_ge const-decl "bool" card_comp nil))
   shostak))
 (card_lt_gt 0
  (card_lt_gt-1 nil 3316959093
   ("" (expand* "card_lt" "card_gt") nil nil)
   ((card_gt const-decl "bool" card_comp nil)
    (card_lt const-decl "bool" card_comp nil))
   shostak))
 (card_le_ge 0
  (card_le_ge-1 nil 3316959107
   ("" (expand* "card_le" "card_ge") nil nil)
   ((card_ge const-decl "bool" card_comp nil)
    (card_le const-decl "bool" card_comp nil))
   shostak))
 (card_gt_lt 0
  (card_gt_lt-1 nil 3316959121
   ("" (expand* "card_gt" "card_lt") nil nil)
   ((card_lt const-decl "bool" card_comp nil)
    (card_gt const-decl "bool" card_comp nil))
   shostak))
 (card_ge_le 0
  (card_ge_le-1 nil 3316959130
   ("" (expand* "card_ge" "card_le") nil nil)
   ((card_le const-decl "bool" card_comp nil)
    (card_ge const-decl "bool" card_comp nil))
   shostak))
 (card_lt_ge 0
  (card_lt_ge-1 nil 3316959138
   ("" (expand* "XOR" "card_lt" "card_ge") (("" (reduce) nil nil)) nil)
   ((XOR const-decl "bool" xor_def nil)
    (card_ge const-decl "bool" card_comp nil)
    (card_lt const-decl "bool" card_comp nil))
   shostak))
 (card_le_gt 0
  (card_le_gt-1 nil 3316959172
   ("" (expand* "XOR" "card_le" "card_gt") (("" (reduce) nil nil)) nil)
   ((XOR const-decl "bool" xor_def nil)
    (card_gt const-decl "bool" card_comp nil)
    (card_le const-decl "bool" card_comp nil))
   shostak))
 (card_eq_le_ge 0
  (card_eq_le_ge-1 nil 3316959186
   ("" (expand* "card_eq" "card_le" "card_ge")
    (("" (lemma "inj_inj_bij")
      (("" (reduce)
        (("1" (use "bijective_inverse_exists[T1, T2]")
          (("1" (expand "exists1")
            (("1" (skosimp*)
              (("1" (use "bij_inv_is_bij_alt[T1, T2]")
                (("1" (expand "bijective?" -1)
                  (("1" (flatten) (("1" (inst?) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (expand "bijective?") (("2" (propax) nil nil)) nil))
        nil))
      nil))
    nil)
   ((T2 formal-type-decl nil card_comp_props nil)
    (T1 formal-type-decl nil card_comp_props nil)
    (inj_inj_bij formula-decl nil set_antisymmetric "orders/")
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (bijective? const-decl "bool" functions nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (x!1 skolem-const-decl "[T2 -> T1]" card_comp_props nil)
    (f!1 skolem-const-decl "[T1 -> T2]" card_comp_props nil)
    (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
    (exists1 const-decl "bool" exists1 nil)
    (card_eq const-decl "bool" card_comp nil)
    (card_ge const-decl "bool" card_comp nil)
    (card_le const-decl "bool" card_comp nil))
   shostak))
 (card_le_lt_eq 0
  (card_le_lt_eq-1 nil 3316959272
   ("" (expand* "card_le" "card_lt" "card_eq")
    (("" (lemma "inj_inj_bij")
      (("" (lemma "injective_dichotomous")
        (("" (reduce)
          (("" (expand "bijective?") (("" (propax) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((T2 formal-type-decl nil card_comp_props nil)
    (T1 formal-type-decl nil card_comp_props nil)
    (inj_inj_bij formula-decl nil set_antisymmetric "orders/")
    (bijective? const-decl "bool" functions nil)
    (injective_dichotomous formula-decl nil set_dichotomous "orders/")
    (card_le const-decl "bool" card_comp nil)
    (card_eq const-decl "bool" card_comp nil)
    (card_lt const-decl "bool" card_comp nil))
   shostak))
 (card_ge_gt_eq 0
  (card_ge_gt_eq-1 nil 3316959313
   ("" (lemma "card_eq_le_ge")
    (("" (lemma "injective_dichotomous")
      (("" (expand* "card_ge" "card_le" "card_gt" "card_eq")
        (("" (prop) nil nil)) nil))
      nil))
    nil)
   ((T2 formal-type-decl nil card_comp_props nil)
    (T1 formal-type-decl nil card_comp_props nil)
    (injective_dichotomous formula-decl nil set_dichotomous "orders/")
    (card_ge const-decl "bool" card_comp nil)
    (card_gt const-decl "bool" card_comp nil)
    (card_eq const-decl "bool" card_comp nil)
    (card_le const-decl "bool" card_comp nil)
    (card_eq_le_ge formula-decl nil card_comp_props nil))
   shostak))
 (card_lt_neq_ngt 0
  (card_lt_neq_ngt-1 nil 3316959372
   ("" (lemma "card_ge_gt_eq")
    (("" (lemma "card_lt_ge")
      (("" (expand "XOR") (("" (ground) nil nil)) nil)) nil))
    nil)
   ((card_lt_ge formula-decl nil card_comp_props nil)
    (XOR const-decl "bool" xor_def nil)
    (card_ge_gt_eq formula-decl nil card_comp_props nil))
   shostak))
 (card_gt_neq_nlt 0
  (card_gt_neq_nlt-1 nil 3316959390
   ("" (expand* "card_gt" "card_eq" "card_lt")
    (("" (lemma "injective_dichotomous")
      (("" (expand "bijective?") (("" (reduce) nil nil)) nil)) nil))
    nil)
   ((T2 formal-type-decl nil card_comp_props nil)
    (T1 formal-type-decl nil card_comp_props nil)
    (injective_dichotomous formula-decl nil set_dichotomous "orders/")
    (bijective? const-decl "bool" functions nil)
    (card_gt const-decl "bool" card_comp nil)
    (card_lt const-decl "bool" card_comp nil)
    (card_eq const-decl "bool" card_comp nil))
   shostak))
 (card_lt_anticommutative 0
  (card_lt_anticommutative-1 nil 3316959443
   ("" (expand "card_lt")
    (("" (lemma "injective_dichotomous") (("" (prop) nil nil)) nil))
    nil)
   ((T2 formal-type-decl nil card_comp_props nil)
    (T1 formal-type-decl nil card_comp_props nil)
    (injective_dichotomous formula-decl nil set_dichotomous "orders/")
    (card_lt const-decl "bool" card_comp nil))
   shostak))
 (card_le_antisymmetric 0
  (card_le_antisymmetric-1 nil 3316959455
   ("" (lemma "inj_inj_bij")
    (("" (expand* "card_le" "card_eq") nil nil)) nil)
   ((card_le const-decl "bool" card_comp nil)
    (card_eq const-decl "bool" card_comp nil)
    (inj_inj_bij formula-decl nil set_antisymmetric "orders/")
    (T1 formal-type-decl nil card_comp_props nil)
    (T2 formal-type-decl nil card_comp_props nil))
   shostak))
 (card_eq_symmetric 0
  (card_eq_symmetric-1 nil 3316959482
   ("" (expand "card_eq")
    (("" (iff)
      (("" (prop)
        (("1" (skolem!)
          (("1" (use "bijective_inverse_exists[T1, T2]")
            (("1" (expand "exists1")
              (("1" (skosimp*)
                (("1" (use "bij_inv_is_bij_alt[T1, T2]")
                  (("1" (inst?) nil nil)) nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (skolem!)
          (("2" (use "bijective_inverse_exists[T2, T1]")
            (("2" (expand "exists1")
              (("2" (skosimp*)
                (("2" (use "bij_inv_is_bij_alt[T2, T1]")
                  (("2" (inst?) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((x!1 skolem-const-decl "[T1 -> T2]" card_comp_props nil)
    (f!1 skolem-const-decl "[T2 -> T1]" card_comp_props nil)
    (exists1 const-decl "bool" exists1 nil)
    (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
    (x!1 skolem-const-decl "[T2 -> T1]" card_comp_props nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (f!1 skolem-const-decl "[T1 -> T2]" card_comp_props nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T2 formal-type-decl nil card_comp_props nil)
    (T1 formal-type-decl nil card_comp_props nil)
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (card_eq const-decl "bool" card_comp nil))
   shostak))
 (card_ge_antisymmetric 0
  (card_ge_antisymmetric-1 nil 3316959532
   ("" (expand* "card_ge" "card_eq")
    (("" (lemma "inj_inj_bij") (("" (prop) nil nil)) nil)) nil)
   ((T2 formal-type-decl nil card_comp_props nil)
    (T1 formal-type-decl nil card_comp_props nil)
    (inj_inj_bij formula-decl nil set_antisymmetric "orders/")
    (card_ge const-decl "bool" card_comp nil)
    (card_eq const-decl "bool" card_comp nil))
   shostak))
 (card_gt_anticommutative 0
  (card_gt_anticommutative-1 nil 3316959552
   ("" (expand "card_gt")
    (("" (lemma "injective_dichotomous") (("" (prop) nil nil)) nil))
    nil)
   ((T2 formal-type-decl nil card_comp_props nil)
    (T1 formal-type-decl nil card_comp_props nil)
    (injective_dichotomous formula-decl nil set_dichotomous "orders/")
    (card_gt const-decl "bool" card_comp nil))
   shostak))
 (card_lt_trichotomous 0
  (card_lt_trichotomous-1 nil 3316959567
   ("" (lemma "card_lt_ge")
    (("" (lemma "card_gt_lt")
      (("" (lemma "card_ge_gt_eq")
        (("" (expand "XOR") (("" (ground) nil nil)) nil)) nil))
      nil))
    nil)
   ((card_gt_lt formula-decl nil card_comp_props nil)
    (XOR const-decl "bool" xor_def nil)
    (card_ge_gt_eq formula-decl nil card_comp_props nil)
    (card_lt_ge formula-decl nil card_comp_props nil))
   shostak))
 (card_le_dichotomous 0
  (card_le_dichotomous-1 nil 3316959601
   ("" (lemma "card_le_gt")
    (("" (lemma "card_ge_le")
      (("" (lemma "card_gt_ge")
        (("" (expand "XOR") (("" (ground) nil nil)) nil)) nil))
      nil))
    nil)
   ((card_ge_le formula-decl nil card_comp_props nil)
    (XOR const-decl "bool" xor_def nil)
    (card_gt_ge formula-decl nil card_comp_props nil)
    (card_le_gt formula-decl nil card_comp_props nil))
   shostak))
 (card_ge_dichotomous 0
  (card_ge_dichotomous-1 nil 3316959625
   ("" (lemma "card_le_dichotomous")
    (("" (lemma "card_le_ge")
      (("" (lemma "card_ge_le") (("" (ground) nil nil)) nil)) nil))
    nil)
   ((card_le_ge formula-decl nil card_comp_props nil)
    (card_ge_le formula-decl nil card_comp_props nil)
    (card_le_dichotomous formula-decl nil card_comp_props nil))
   shostak))
 (card_gt_trichotomous 0
  (card_gt_trichotomous-1 nil 3316959647
   ("" (lemma "card_lt_trichotomous")
    (("" (lemma "card_lt_gt")
      (("" (lemma "card_gt_lt") (("" (ground) nil nil)) nil)) nil))
    nil)
   ((card_lt_gt formula-decl nil card_comp_props nil)
    (card_gt_lt formula-decl nil card_comp_props nil)
    (card_lt_trichotomous formula-decl nil card_comp_props nil))
   shostak)))


¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.82Angebot  Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können  ¤



Kontakt
Drucken
Kontakt
Hier finden Sie eine Liste der Produkte des Unternehmens

Eigene Datei ansehen




schauen Sie vor die Tür

Fenster


Die Firma ist wie angegeben erreichbar.

Entwicklung einer Software für die statische Quellcodeanalyse


Bot Zugriff

                                                                                                                                                                                                                                                                                                                                                                                                     

Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder
Jenseits des Üblichen ....

Besucherstatistik

Besucherstatistik