Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: card_comp_transitive.prf Sprache: Lisp

Original von: PVS^©

(card_comp_transitive
(card_lt_transitive 0
  (card_lt_transitive-1 nil 3316960965
   ("" (expand "card_lt")
    (("" (lemma "injective_dichotomous")
      (("" (prop)
        (("" (skosimp*)
          (("" (use "composition_injective[T3, T1, T2]")
            (("" (inst? 2) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((T2 formal-type-decl nil card_comp_transitive nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (injective_dichotomous formula-decl nil set_dichotomous "orders/")
    (O const-decl "T3" function_props nil)
    (f!1 skolem-const-decl "[T1 -> T2]" card_comp_transitive nil)
    (f!2 skolem-const-decl "[T3 -> T1]" card_comp_transitive nil)
    (injective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_lt const-decl "bool" card_comp nil))
   shostak))
(card_lt_le_transitive 0
  (card_lt_le_transitive-1 nil 3316961013
   ("" (expand* "card_lt" "card_le")
    (("" (skosimp*)
      (("" (use "composition_injective[T2, T3, T1]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (f!2 skolem-const-decl "[T3 -> T1]" card_comp_transitive nil)
    (f!1 skolem-const-decl "[T2 -> T3]" card_comp_transitive nil)
    (injective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (T2 formal-type-decl nil card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_lt const-decl "bool" card_comp nil)
    (card_le const-decl "bool" card_comp nil))
   shostak))
(card_lt_eq_transitive 0
  (card_lt_eq_transitive-1 nil 3316961037
   ("" (expand* "card_lt" "card_eq" "bijective?")
    (("" (skosimp*)
      (("" (use "composition_injective[T2, T3, T1]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (f!2 skolem-const-decl "[T3 -> T1]" card_comp_transitive nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (injective? const-decl "bool" functions nil)
    (f!1 skolem-const-decl "[T2 -> T3]" card_comp_transitive nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (T2 formal-type-decl nil card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_lt const-decl "bool" card_comp nil)
    (bijective? const-decl "bool" functions nil)
    (card_eq const-decl "bool" card_comp nil))
   shostak))
(card_le_lt_transitive 0
  (card_le_lt_transitive-1 nil 3316961078
   ("" (expand* "card_le" "card_lt")
    (("" (skosimp*)
      (("" (use "composition_injective[T3, T1, T2]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (f!1 skolem-const-decl "[T1 -> T2]" card_comp_transitive nil)
    (f!2 skolem-const-decl "[T3 -> T1]" card_comp_transitive nil)
    (injective? 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_transitive nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_le const-decl "bool" card_comp nil)
    (card_lt const-decl "bool" card_comp nil))
   shostak))
(card_eq_lt_transitive 0
  (card_eq_lt_transitive-1 nil 3316961096
   ("" (expand* "card_eq" "card_lt" "bijective?")
    (("" (skosimp*)
      (("" (use "composition_injective[T3, T1, T2]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (f!1 skolem-const-decl "[T1 -> T2]" card_comp_transitive nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (injective? const-decl "bool" functions nil)
    (f!2 skolem-const-decl "[T3 -> T1]" card_comp_transitive nil)
    (T2 formal-type-decl nil card_comp_transitive nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_eq const-decl "bool" card_comp nil)
    (bijective? const-decl "bool" functions nil)
    (card_lt const-decl "bool" card_comp nil))
   shostak))
(card_le_transitive 0
  (card_le_transitive-1 nil 3316961118
   ("" (expand "card_le")
    (("" (skosimp*)
      (("" (use "composition_injective[T1, T2, T3]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (f!2 skolem-const-decl "[T2 -> T3]" card_comp_transitive nil)
    (f!1 skolem-const-decl "[T1 -> T2]" card_comp_transitive nil)
    (injective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (T2 formal-type-decl nil card_comp_transitive nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_le const-decl "bool" card_comp nil))
   shostak))
(card_le_eq_transitive 0
  (card_le_eq_transitive-1 nil 3316961145
   ("" (expand* "card_le" "card_eq" "bijective?")
    (("" (skosimp*)
      (("" (use "composition_injective[T1, T2, T3]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (f!2 skolem-const-decl "[T2 -> T3]" card_comp_transitive nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (injective? const-decl "bool" functions nil)
    (f!1 skolem-const-decl "[T1 -> T2]" card_comp_transitive nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (T2 formal-type-decl nil card_comp_transitive nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_le const-decl "bool" card_comp nil)
    (bijective? const-decl "bool" functions nil)
    (card_eq const-decl "bool" card_comp nil))
   shostak))
(card_eq_le_transitive 0
  (card_eq_le_transitive-1 nil 3316961166
   ("" (expand* "card_eq" "card_le" "bijective?")
    (("" (skosimp*)
      (("" (use "composition_injective[T1, T2, T3]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (f!2 skolem-const-decl "[T2 -> T3]" card_comp_transitive nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (injective? const-decl "bool" functions nil)
    (f!1 skolem-const-decl "[T1 -> T2]" card_comp_transitive nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (T2 formal-type-decl nil card_comp_transitive nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_eq const-decl "bool" card_comp nil)
    (bijective? const-decl "bool" functions nil)
    (card_le const-decl "bool" card_comp nil))
   shostak))
(card_eq_transitive 0
  (card_eq_transitive-1 nil 3316961183
   ("" (expand "card_eq")
    (("" (skosimp*)
      (("" (use "composition_bijective[T1, T2, T3]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (f!2 skolem-const-decl "[T2 -> T3]" card_comp_transitive nil)
    (f!1 skolem-const-decl "[T1 -> T2]" card_comp_transitive nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (T2 formal-type-decl nil card_comp_transitive nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (composition_bijective judgement-tcc nil function_props nil)
    (card_eq const-decl "bool" card_comp nil))
   shostak))
(card_eq_ge_transitive 0
  (card_eq_ge_transitive-1 nil 3316961212
   ("" (expand* "card_eq" "card_ge")
    (("" (skosimp*)
      (("" (use "bijective_inverse_exists[T1, T2]")
        (("" (expand "exists1")
          (("" (skosimp*)
            (("" (use "bij_inv_is_bij_alt[T1, T2]")
              (("" (expand "bijective?" -1)
                (("" (flatten)
                  (("" (use "composition_injective[T3, T2, T1]")
                    (("" (inst?) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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_transitive nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (O const-decl "T3" function_props nil)
    (injective? const-decl "bool" functions nil)
    (f!2 skolem-const-decl "[T3 -> T2]" card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (f!1 skolem-const-decl "[T1 -> T2]" card_comp_transitive 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_transitive nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (card_eq const-decl "bool" card_comp nil)
    (card_ge const-decl "bool" card_comp nil))
   shostak))
(card_ge_eq_transitive 0
  (card_ge_eq_transitive-1 nil 3316961287
   ("" (expand* "card_ge" "card_eq")
    (("" (skosimp*)
      (("" (use "bijective_inverse_exists[T2, T3]")
        (("" (expand "exists1")
          (("" (skosimp*)
            (("" (use "bij_inv_is_bij_alt[T2, T3]")
              (("" (expand "bijective?" -1)
                (("" (flatten)
                  (("" (use "composition_injective[T3, T2, T1]")
                    (("" (inst?) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((exists1 const-decl "bool" exists1 nil)
    (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
    (x!1 skolem-const-decl "[T3 -> T2]" card_comp_transitive nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (O const-decl "T3" function_props nil)
    (f!1 skolem-const-decl "[T2 -> T1]" card_comp_transitive nil)
    (injective? const-decl "bool" functions nil)
    (composition_injective judgement-tcc nil function_props nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (f!2 skolem-const-decl "[T2 -> T3]" card_comp_transitive nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (T2 formal-type-decl nil card_comp_transitive nil)
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (card_ge const-decl "bool" card_comp nil)
    (card_eq const-decl "bool" card_comp nil))
   shostak))
(card_ge_transitive 0
  (card_ge_transitive-1 nil 3316961349
   ("" (expand "card_ge")
    (("" (skosimp*)
      (("" (use "composition_injective[T3, T2, T1]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (f!1 skolem-const-decl "[T2 -> T1]" card_comp_transitive nil)
    (f!2 skolem-const-decl "[T3 -> T2]" card_comp_transitive nil)
    (injective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (T2 formal-type-decl nil card_comp_transitive nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_ge const-decl "bool" card_comp nil))
   shostak))
(card_eq_gt_transitive 0
  (card_eq_gt_transitive-1 nil 3316961376
   ("" (expand* "card_eq" "card_gt")
    (("" (skosimp*)
      (("" (use "bijective_inverse_exists[T1, T2]")
        (("" (expand "exists1")
          (("" (skosimp*)
            (("" (use "bij_inv_is_bij_alt[T1, T2]")
              (("" (expand "bijective?" -1)
                (("" (flatten)
                  (("" (use "composition_injective[T2, T1, T3]")
                    (("" (inst?) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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_transitive nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (O const-decl "T3" function_props nil)
    (f!2 skolem-const-decl "[T1 -> T3]" card_comp_transitive nil)
    (injective? const-decl "bool" functions nil)
    (composition_injective judgement-tcc nil function_props nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (f!1 skolem-const-decl "[T1 -> T2]" card_comp_transitive 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_transitive nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (card_eq const-decl "bool" card_comp nil)
    (card_gt const-decl "bool" card_comp nil))
   shostak))
(card_ge_gt_transitive 0
  (card_ge_gt_transitive-1 nil 3316961423
   ("" (expand* "card_ge" "card_gt")
    (("" (skosimp*)
      (("" (use "composition_injective[T2, T1, T3]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (f!2 skolem-const-decl "[T1 -> T3]" card_comp_transitive nil)
    (f!1 skolem-const-decl "[T2 -> T1]" card_comp_transitive nil)
    (injective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (T2 formal-type-decl nil card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_ge const-decl "bool" card_comp nil)
    (card_gt const-decl "bool" card_comp nil))
   shostak))
(card_gt_eq_transitive 0
  (card_gt_eq_transitive-1 nil 3316961447
   ("" (expand* "card_gt" "card_eq")
    (("" (skosimp*)
      (("" (use "bijective_inverse_exists[T2, T3]")
        (("" (expand "exists1")
          (("" (skosimp*)
            (("" (use "bij_inv_is_bij_alt[T2, T3]")
              (("" (expand "bijective?" -1)
                (("" (flatten)
                  (("" (use "composition_injective[T1, T3, T2]")
                    (("" (inst?) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((exists1 const-decl "bool" exists1 nil)
    (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil)
    (x!1 skolem-const-decl "[T3 -> T2]" card_comp_transitive nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (O const-decl "T3" function_props nil)
    (injective? const-decl "bool" functions nil)
    (f!2 skolem-const-decl "[T1 -> T3]" card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (f!1 skolem-const-decl "[T2 -> T3]" card_comp_transitive nil)
    (bijective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (T2 formal-type-decl nil card_comp_transitive nil)
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (card_gt const-decl "bool" card_comp nil)
    (card_eq const-decl "bool" card_comp nil))
   shostak))
(card_gt_ge_transitive 0
  (card_gt_ge_transitive-1 nil 3316961503
   ("" (expand* "card_gt" "card_ge")
    (("" (skosimp*)
      (("" (use "composition_injective[T1, T3, T2]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (f!1 skolem-const-decl "[T3 -> T2]" card_comp_transitive nil)
    (f!2 skolem-const-decl "[T1 -> T3]" card_comp_transitive nil)
    (injective? 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_transitive nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_gt const-decl "bool" card_comp nil)
    (card_ge const-decl "bool" card_comp nil))
   shostak))
(card_gt_transitive 0
  (card_gt_transitive-1 nil 3316961525
   ("" (expand "card_gt")
    (("" (lemma "injective_dichotomous")
      (("" (prop)
        (("" (skosimp*)
          (("" (use "composition_injective[T2, T1, T3]")
            (("" (inst? 2) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((T2 formal-type-decl nil card_comp_transitive nil)
    (T1 formal-type-decl nil card_comp_transitive nil)
    (injective_dichotomous formula-decl nil set_dichotomous "orders/")
    (O const-decl "T3" function_props nil)
    (f!2 skolem-const-decl "[T1 -> T3]" card_comp_transitive nil)
    (f!1 skolem-const-decl "[T2 -> T1]" card_comp_transitive nil)
    (injective? const-decl "bool" functions nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T3 formal-type-decl nil card_comp_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_gt const-decl "bool" card_comp nil))
   shostak)))

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