Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: card_comp_set_props.prf Sprache: Lisp

Original von: PVS^©

(card_comp_set_props
(card_lt_surj 0
  (card_lt_surj-1 nil 3316959740
   ("" (skolem!)
    (("" (expand "card_lt")
      (("" (prop)
        (("1" (lemma "fun_exists[(S2!1), (S1!1)]")
          (("1" (prop)
            (("1" (skolem!)
              (("1" (inst 2 "f!1") (("1" (grind) nil nil)) nil)) nil))
            nil))
          nil)
         ("2" (skolem!)
          (("2" (use "surjective_inverse_exists[(S1!1), (S2!1)]")
            (("2" (skolem!)
              (("2" (use "inj_inv_alt[(S1!1), (S2!1)]")
                (("2" (inst?) nil nil)) nil))
              nil))
            nil))
          nil)
         ("3" (skolem! -2)
          (("3" (use "inv_inj_is_surj[(S2!1), (S1!1)]")
            (("3" (inst?) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((card_lt const-decl "bool" card_comp_set nil)
    (inverse const-decl "D" function_inverse nil)
    (f!1 skolem-const-decl "[(S2!1) -> (S1!1)]" card_comp_set_props
     nil)
    (inv_inj_is_surj judgement-tcc nil function_inverse nil)
    (TRUE const-decl "bool" booleans nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (g!1 skolem-const-decl "[(S2!1) -> (S1!1)]" card_comp_set_props
     nil)
    (inj_inv_alt formula-decl nil function_inverse_def nil)
    (f!1 skolem-const-decl "[(S1!1) -> (S2!1)]" card_comp_set_props
     nil)
    (surjective? const-decl "bool" functions nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_props nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_props nil)
    (surjective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (T1 formal-type-decl nil card_comp_set_props nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T2 formal-type-decl nil card_comp_set_props nil)
    (fun_exists formula-decl nil function_image nil)
    (injective? const-decl "bool" functions nil)
    (NOT const-decl "[bool -> bool]" booleans nil))
   shostak))
(card_ge_surj 0
  (card_ge_surj-1 nil 3316959991
   ("" (skolem!)
    (("" (expand "card_ge")
      (("" (split)
        (("1" (flatten)
          (("1" (skolem!)
            (("1" (case "EXISTS (x: (S2!1)): TRUE")
              (("1" (use "inv_inj_is_surj[(S2!1), (S1!1)]")
                (("1" (inst? 2) nil nil)) nil)
               ("2" (split)
                (("1" (lemma "fun_exists[(S1!1), (S2!1)]")
                  (("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: (S2!1)): t!1")
              (("1" (grind) nil nil)) nil))
            nil)
           ("2" (skolem!)
            (("2" (use "surjective_inverse_exists[(S1!1), (S2!1)]")
              (("2" (skolem!)
                (("2" (use "inj_inv_alt[(S1!1), (S2!1)]")
                  (("2" (inst?) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((card_ge const-decl "bool" card_comp_set nil)
    (surjective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (f!1 skolem-const-decl "[(S1!1) -> (S2!1)]" card_comp_set_props
     nil)
    (inj_inv_alt formula-decl nil function_inverse_def nil)
    (g!1 skolem-const-decl "[(S2!1) -> (S1!1)]" card_comp_set_props
     nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (TRUE const-decl "bool" booleans nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T2 formal-type-decl nil card_comp_set_props nil)
    (inverse const-decl "D" function_inverse nil)
    (f!1 skolem-const-decl "[(S2!1) -> (S1!1)]" card_comp_set_props
     nil)
    (injective? const-decl "bool" functions nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_props nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_props nil)
    (T1 formal-type-decl nil card_comp_set_props nil)
    (inv_inj_is_surj judgement-tcc nil function_inverse nil)
    (fun_exists formula-decl nil function_image nil)
    (surjective? const-decl "bool" functions nil)
    (NOT const-decl "[bool -> bool]" booleans nil))
   shostak))
(card_lt_le 0
  (card_lt_le-1 nil 3316960095
   ("" (expand* "card_lt" "card_le")
    (("" (skosimp)
      (("" (lemma "injective_dichotomous[(S1!1), (S2!1)]")
        (("" (prop) nil nil)) nil))
      nil))
    nil)
   ((injective_dichotomous formula-decl nil set_dichotomous "orders/")
    (T1 formal-type-decl nil card_comp_set_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (T2 formal-type-decl nil card_comp_set_props nil)
    (card_lt const-decl "bool" card_comp_set nil)
    (card_le const-decl "bool" card_comp_set nil))
   shostak))
(card_gt_ge 0
  (card_gt_ge-1 nil 3316960131
   ("" (expand* "card_gt" "card_ge")
    (("" (skosimp)
      (("" (lemma "injective_dichotomous[(S1!1), (S2!1)]")
        (("" (prop) nil nil)) nil))
      nil))
    nil)
   ((injective_dichotomous formula-decl nil set_dichotomous "orders/")
    (T1 formal-type-decl nil card_comp_set_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (T2 formal-type-decl nil card_comp_set_props nil)
    (card_gt const-decl "bool" card_comp_set nil)
    (card_ge const-decl "bool" card_comp_set nil))
   shostak))
(card_lt_gt 0
  (card_lt_gt-1 nil 3316960154
   ("" (expand* "card_lt" "card_gt") nil nil)
   ((card_gt const-decl "bool" card_comp_set nil)
    (card_lt const-decl "bool" card_comp_set nil))
   shostak))
(card_le_ge 0
  (card_le_ge-1 nil 3316960172
   ("" (expand* "card_le" "card_ge") nil nil)
   ((card_ge const-decl "bool" card_comp_set nil)
    (card_le const-decl "bool" card_comp_set nil))
   shostak))
(card_gt_lt 0
  (card_gt_lt-1 nil 3316960178
   ("" (expand* "card_gt" "card_lt") nil nil)
   ((card_lt const-decl "bool" card_comp_set nil)
    (card_gt const-decl "bool" card_comp_set nil))
   shostak))
(card_ge_le 0
  (card_ge_le-1 nil 3316960186
   ("" (expand* "card_ge" "card_le") nil nil)
   ((card_le const-decl "bool" card_comp_set nil)
    (card_ge const-decl "bool" card_comp_set nil))
   shostak))
(card_lt_ge 0
  (card_lt_ge-1 nil 3316960193
   ("" (expand* "card_lt" "card_ge" "XOR") (("" (reduce) nil nil)) nil)
   ((card_lt const-decl "bool" card_comp_set nil)
    (XOR const-decl "bool" xor_def nil)
    (card_ge const-decl "bool" card_comp_set nil))
   shostak))
(card_le_gt 0
  (card_le_gt-1 nil 3316960243
   ("" (expand* "card_le" "card_gt" "XOR") (("" (reduce) nil nil)) nil)
   ((card_le const-decl "bool" card_comp_set nil)
    (XOR const-decl "bool" xor_def nil)
    (card_gt const-decl "bool" card_comp_set nil))
   shostak))
(card_eq_le_ge 0
  (card_eq_le_ge-1 nil 3316960256
   ("" (expand* "card_eq" "card_le" "card_ge")
    (("" (skolem!)
      (("" (prop)
        (("1" (expand "bijective?")
          (("1" (skosimp) (("1" (inst?) nil nil)) nil)) nil)
         ("2" (skolem!)
          (("2" (use "bijective_inverse_exists[(S1!1), (S2!1)]")
            (("2" (expand "exists1")
              (("2" (skosimp*)
                (("2" (use "bij_inv_is_bij_alt[(S1!1), (S2!1)]")
                  (("2" (expand "bijective?" -1)
                    (("2" (flatten) (("2" (inst?) nil nil)) nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("3" (forward-chain "inj_inj_bij[(S1!1), (S2!1)]") nil nil))
        nil))
      nil))
    nil)
   ((inj_inj_bij formula-decl nil set_antisymmetric "orders/")
    (exists1 const-decl "bool" exists1 nil)
    (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
    (x!1 skolem-const-decl "[(S2!1) -> (S1!1)]" card_comp_set_props
     nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (f!1 skolem-const-decl "[(S1!1) -> (S2!1)]" card_comp_set_props
     nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_props nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_props nil)
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (bijective? const-decl "bool" functions nil)
    (T2 formal-type-decl nil card_comp_set_props 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_comp_set_props nil)
    (card_eq const-decl "bool" card_comp_set nil)
    (card_ge const-decl "bool" card_comp_set nil)
    (card_le const-decl "bool" card_comp_set nil))
   shostak))
(card_le_lt_eq 0
  (card_le_lt_eq-1 nil 3316960340
   ("" (expand* "card_le" "card_lt" "card_eq")
    (("" (skolem!)
      (("" (prop)
        (("1" (forward-chain "inj_inj_bij[(S1!1), (S2!1)]") nil nil)
         ("2" (lemma "injective_dichotomous[(S1!1), (S2!1)]")
          (("2" (prop) nil nil)) nil)
         ("3" (expand "bijective?")
          (("3" (skosimp) (("3" (inst?) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((bijective? const-decl "bool" functions nil)
    (injective_dichotomous formula-decl nil set_dichotomous "orders/")
    (inj_inj_bij formula-decl nil set_antisymmetric "orders/")
    (T1 formal-type-decl nil card_comp_set_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (T2 formal-type-decl nil card_comp_set_props nil)
    (card_le const-decl "bool" card_comp_set nil)
    (card_eq const-decl "bool" card_comp_set nil)
    (card_lt const-decl "bool" card_comp_set nil))
   shostak))
(card_ge_gt_eq 0
  (card_ge_gt_eq-1 nil 3316960405
   ("" (skolem!)
    (("" (use "card_eq_le_ge")
      (("" (expand* "card_eq" "card_le" "card_ge" "card_gt")
        (("" (lemma "injective_dichotomous[(S1!1), (S2!1)]")
          (("" (ground) nil nil)) nil))
        nil))
      nil))
    nil)
   ((card_eq_le_ge formula-decl nil card_comp_set_props nil)
    (T2 formal-type-decl nil card_comp_set_props 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_comp_set_props nil)
    (injective_dichotomous formula-decl nil set_dichotomous "orders/")
    (card_eq const-decl "bool" card_comp_set nil)
    (card_ge const-decl "bool" card_comp_set nil)
    (card_gt const-decl "bool" card_comp_set nil)
    (card_le const-decl "bool" card_comp_set nil))
   shostak))
(card_lt_neq_ngt 0
  (card_lt_neq_ngt-1 nil 3316960435
   ("" (skosimp)
    (("" (use "card_ge_gt_eq")
      (("" (use "card_lt_ge")
        (("" (expand "XOR") (("" (ground) nil nil)) nil)) nil))
      nil))
    nil)
   ((card_ge_gt_eq formula-decl nil card_comp_set_props nil)
    (T2 formal-type-decl nil card_comp_set_props 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_comp_set_props nil)
    (XOR const-decl "bool" xor_def nil)
    (card_lt_ge formula-decl nil card_comp_set_props nil))
   shostak))
(card_gt_neq_nlt 0
  (card_gt_neq_nlt-1 nil 3316960535
   ("" (expand* "card_gt" "card_eq" "card_lt")
    (("" (skosimp)
      (("" (lemma "injective_dichotomous[(S1!1), (S2!1)]")
        (("" (prop)
          (("" (expand "bijective?")
            (("" (skosimp) (("" (inst?) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((bijective? const-decl "bool" functions nil)
    (injective_dichotomous formula-decl nil set_dichotomous "orders/")
    (T1 formal-type-decl nil card_comp_set_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (T2 formal-type-decl nil card_comp_set_props nil)
    (card_gt const-decl "bool" card_comp_set nil)
    (card_lt const-decl "bool" card_comp_set nil)
    (card_eq const-decl "bool" card_comp_set nil))
   shostak))
(card_lt_anticommutative 0
  (card_lt_anticommutative-1 nil 3316960578
   ("" (expand "card_lt")
    (("" (skosimp)
      (("" (lemma "injective_dichotomous[(S1!1), (S2!1)]")
        (("" (prop) nil nil)) nil))
      nil))
    nil)
   ((injective_dichotomous formula-decl nil set_dichotomous "orders/")
    (T1 formal-type-decl nil card_comp_set_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (T2 formal-type-decl nil card_comp_set_props nil)
    (card_lt const-decl "bool" card_comp_set nil))
   shostak))
(card_le_antisymmetric 0
  (card_le_antisymmetric-1 nil 3316960590
   ("" (expand* "card_le" "card_eq")
    (("" (skosimp)
      (("" (forward-chain "inj_inj_bij[(S1!1), (S2!1)]") nil nil))
      nil))
    nil)
   ((T2 formal-type-decl nil card_comp_set_props 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_comp_set_props nil)
    (inj_inj_bij formula-decl nil set_antisymmetric "orders/")
    (card_le const-decl "bool" card_comp_set nil)
    (card_eq const-decl "bool" card_comp_set nil))
   shostak))
(card_eq_symmetric 0
  (card_eq_symmetric-1 nil 3316960616
   ("" (expand "card_eq")
    (("" (skolem!)
      (("" (iff)
        (("" (prop)
          (("1" (skolem!)
            (("1" (use "bijective_inverse_exists[(S1!1), (S2!1)]")
              (("1" (expand "exists1")
                (("1" (skosimp*)
                  (("1" (use "bij_inv_is_bij_alt[(S1!1), (S2!1)]")
                    (("1" (inst?) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (skolem!)
            (("2" (use "bijective_inverse_exists[(S2!1), (S1!1)]")
              (("2" (expand "exists1")
                (("2" (skosimp*)
                  (("2" (use "bij_inv_is_bij_alt[(S2!1), (S1!1)]")
                    (("2" (inst?) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (T1 formal-type-decl nil card_comp_set_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (T2 formal-type-decl nil card_comp_set_props nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_props nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_props nil)
    (bijective? const-decl "bool" functions nil)
    (f!1 skolem-const-decl "[(S1!1) -> (S2!1)]" card_comp_set_props
     nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (x!1 skolem-const-decl "[(S2!1) -> (S1!1)]" card_comp_set_props
     nil)
    (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
    (exists1 const-decl "bool" exists1 nil)
    (f!1 skolem-const-decl "[(S2!1) -> (S1!1)]" card_comp_set_props
     nil)
    (x!1 skolem-const-decl "[(S1!1) -> (S2!1)]" card_comp_set_props
     nil)
    (card_eq const-decl "bool" card_comp_set nil))
   shostak))
(card_ge_antisymmetric 0
  (card_ge_antisymmetric-1 nil 3316960683
   ("" (expand* "card_ge" "card_eq")
    (("" (skosimp)
      (("" (forward-chain "inj_inj_bij[(S1!1), (S2!1)]") nil nil))
      nil))
    nil)
   ((T2 formal-type-decl nil card_comp_set_props 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_comp_set_props nil)
    (inj_inj_bij formula-decl nil set_antisymmetric "orders/")
    (card_ge const-decl "bool" card_comp_set nil)
    (card_eq const-decl "bool" card_comp_set nil))
   shostak))
(card_gt_anticommutative 0
  (card_gt_anticommutative-1 nil 3316960742
   ("" (expand "card_gt")
    (("" (skosimp)
      (("" (lemma "injective_dichotomous[(S1!1), (S2!1)]")
        (("" (prop) nil nil)) nil))
      nil))
    nil)
   ((injective_dichotomous formula-decl nil set_dichotomous "orders/")
    (T1 formal-type-decl nil card_comp_set_props nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (T2 formal-type-decl nil card_comp_set_props nil)
    (card_gt const-decl "bool" card_comp_set nil))
   shostak))
(card_lt_trichotomous 0
  (card_lt_trichotomous-1 nil 3316960758
   ("" (skosimp)
    (("" (use "card_lt_ge")
      (("" (use "card_gt_lt")
        (("" (use "card_ge_gt_eq")
          (("" (expand "XOR") (("" (ground) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((card_lt_ge formula-decl nil card_comp_set_props nil)
    (T2 formal-type-decl nil card_comp_set_props 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_comp_set_props nil)
    (card_ge_gt_eq formula-decl nil card_comp_set_props nil)
    (XOR const-decl "bool" xor_def nil)
    (card_gt_lt formula-decl nil card_comp_set_props nil))
   shostak))
(card_le_dichotomous 0
  (card_le_dichotomous-1 nil 3316960784
   ("" (skosimp)
    (("" (use "card_le_gt")
      (("" (use "card_ge_le")
        (("" (use "card_gt_ge")
          (("" (expand "XOR") (("" (ground) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((card_le_gt formula-decl nil card_comp_set_props nil)
    (T2 formal-type-decl nil card_comp_set_props 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_comp_set_props nil)
    (card_gt_ge formula-decl nil card_comp_set_props nil)
    (XOR const-decl "bool" xor_def nil)
    (card_ge_le formula-decl nil card_comp_set_props nil))
   shostak))
(card_ge_dichotomous 0
  (card_ge_dichotomous-1 nil 3316960815
   ("" (skosimp)
    (("" (use "card_le_dichotomous")
      (("" (use "card_le_ge")
        (("" (use "card_ge_le") (("" (ground) nil nil)) nil)) nil))
      nil))
    nil)
   ((card_le_dichotomous formula-decl nil card_comp_set_props 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_comp_set_props nil)
    (T2 formal-type-decl nil card_comp_set_props nil)
    (card_ge_le formula-decl nil card_comp_set_props nil)
    (card_le_ge formula-decl nil card_comp_set_props nil))
   shostak))
(card_gt_trichotomous 0
  (card_gt_trichotomous-1 nil 3316960841
   ("" (skosimp)
    (("" (use "card_lt_trichotomous")
      (("" (use "card_lt_gt")
        (("" (use "card_gt_lt") (("" (ground) nil nil)) nil)) nil))
      nil))
    nil)
   ((card_lt_trichotomous formula-decl nil card_comp_set_props nil)
    (T2 formal-type-decl nil card_comp_set_props 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_comp_set_props nil)
    (card_gt_lt formula-decl nil card_comp_set_props nil)
    (card_lt_gt formula-decl nil card_comp_set_props nil))
   shostak)))

¤ Dauer der Verarbeitung: 0.32 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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.