Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: intersections_2D.prf Sprache: Lisp

Original von: 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)))

¤ Dauer der Verarbeitung: 0.5 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
Eigene Datei ansehen

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.