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

products/sources/formale sprachen/PVS/sets_aux/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: riesz_linear_functionals.prf   Sprache: Lisp

Untersuchung PVS©
(card_comp_set_transitive
 (card_lt_transitive 0
  (card_lt_transitive-1 nil 3316966275
   ("" (expand "card_lt")
    (("" (skosimp)
      (("" (lemma "injective_dichotomous[(S1!1), (S2!1)]")
        (("" (prop)
          (("" (skosimp*)
            (("" (use "composition_injective[(S3!1), (S1!1), (S2!1)]")
              (("" (inst? 2) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((composition_injective judgement-tcc nil function_props nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (f!2 skolem-const-decl "[(S3!1) -> (S1!1)]"
     card_comp_set_transitive nil)
    (f!1 skolem-const-decl "[(S1!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (O const-decl "T3" function_props nil)
    (injective_dichotomous formula-decl nil set_dichotomous "orders/")
    (T1 formal-type-decl nil card_comp_set_transitive 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_transitive nil)
    (card_lt const-decl "bool" card_comp_set nil))
   shostak))
 (card_lt_le_transitive 0
  (card_lt_le_transitive-1 nil 3316966326
   ("" (expand* "card_lt" "card_le")
    (("" (skosimp*)
      (("" (use "composition_injective[(S2!1), (S3!1), (S1!1)]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (f!2 skolem-const-decl "[(S3!1) -> (S1!1)]"
     card_comp_set_transitive nil)
    (f!1 skolem-const-decl "[(S2!1) -> (S3!1)]"
     card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (T1 formal-type-decl nil card_comp_set_transitive nil)
    (T3 formal-type-decl nil card_comp_set_transitive 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_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_lt const-decl "bool" card_comp_set nil)
    (card_le const-decl "bool" card_comp_set nil))
   shostak))
 (card_lt_eq_transitive 0
  (card_lt_eq_transitive-1 nil 3316966361
   ("" (expand* "card_lt" "card_eq" "bijective?")
    (("" (skosimp*)
      (("" (use "composition_injective[(S2!1), (S3!1), (S1!1)]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (f!2 skolem-const-decl "[(S3!1) -> (S1!1)]"
     card_comp_set_transitive nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (f!1 skolem-const-decl "[(S2!1) -> (S3!1)]"
     card_comp_set_transitive nil)
    (T1 formal-type-decl nil card_comp_set_transitive nil)
    (T3 formal-type-decl nil card_comp_set_transitive 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_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_lt const-decl "bool" card_comp_set nil)
    (bijective? const-decl "bool" functions nil)
    (card_eq const-decl "bool" card_comp_set nil))
   shostak))
 (card_le_lt_transitive 0
  (card_le_lt_transitive-1 nil 3316966385
   ("" (expand* "card_le" "card_lt")
    (("" (skosimp*)
      (("" (use "composition_injective[(S3!1), (S1!1), (S2!1)]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (f!1 skolem-const-decl "[(S1!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (f!2 skolem-const-decl "[(S3!1) -> (S1!1)]"
     card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (T2 formal-type-decl nil card_comp_set_transitive nil)
    (T1 formal-type-decl nil card_comp_set_transitive nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_le const-decl "bool" card_comp_set nil)
    (card_lt const-decl "bool" card_comp_set nil))
   shostak))
 (card_eq_lt_transitive 0
  (card_eq_lt_transitive-1 nil 3316966409
   ("" (expand* "card_eq" "card_lt" "bijective?")
    (("" (skosimp*)
      (("" (use "composition_injective[(S3!1), (S1!1), (S2!1)]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (f!1 skolem-const-decl "[(S1!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (f!2 skolem-const-decl "[(S3!1) -> (S1!1)]"
     card_comp_set_transitive nil)
    (T2 formal-type-decl nil card_comp_set_transitive nil)
    (T1 formal-type-decl nil card_comp_set_transitive nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_eq const-decl "bool" card_comp_set nil)
    (bijective? const-decl "bool" functions nil)
    (card_lt const-decl "bool" card_comp_set nil))
   shostak))
 (card_le_transitive 0
  (card_le_transitive-1 nil 3316966440
   ("" (expand "card_le")
    (("" (skosimp*)
      (("" (use "composition_injective[(S1!1), (S2!1), (S3!1)]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (f!2 skolem-const-decl "[(S2!1) -> (S3!1)]"
     card_comp_set_transitive nil)
    (f!1 skolem-const-decl "[(S1!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (T2 formal-type-decl nil card_comp_set_transitive 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_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_le const-decl "bool" card_comp_set nil))
   shostak))
 (card_le_eq_transitive 0
  (card_le_eq_transitive-1 nil 3316966458
   ("" (expand* "card_le" "card_eq" "bijective?")
    (("" (skosimp*)
      (("" (use "composition_injective[(S1!1), (S2!1), (S3!1)]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (f!2 skolem-const-decl "[(S2!1) -> (S3!1)]"
     card_comp_set_transitive nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (f!1 skolem-const-decl "[(S1!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (T2 formal-type-decl nil card_comp_set_transitive 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_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_le const-decl "bool" card_comp_set nil)
    (bijective? const-decl "bool" functions nil)
    (card_eq const-decl "bool" card_comp_set nil))
   shostak))
 (card_eq_le_transitive 0
  (card_eq_le_transitive-1 nil 3316966499
   ("" (expand* "card_eq" "card_le" "bijective?")
    (("" (skosimp*)
      (("" (use "composition_injective[(S1!1), (S2!1), (S3!1)]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (f!2 skolem-const-decl "[(S2!1) -> (S3!1)]"
     card_comp_set_transitive nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (f!1 skolem-const-decl "[(S1!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (T2 formal-type-decl nil card_comp_set_transitive 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_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_eq const-decl "bool" card_comp_set nil)
    (bijective? const-decl "bool" functions nil)
    (card_le const-decl "bool" card_comp_set nil))
   shostak))
 (card_eq_transitive 0
  (card_eq_transitive-1 nil 3316966568
   ("" (expand "card_eq")
    (("" (skosimp*)
      (("" (use "composition_bijective[(S1!1), (S2!1), (S3!1)]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (f!2 skolem-const-decl "[(S2!1) -> (S3!1)]"
     card_comp_set_transitive nil)
    (f!1 skolem-const-decl "[(S1!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (bijective? const-decl "bool" functions nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (T2 formal-type-decl nil card_comp_set_transitive 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_transitive nil)
    (composition_bijective judgement-tcc nil function_props nil)
    (card_eq const-decl "bool" card_comp_set nil))
   shostak))
 (card_eq_ge_transitive 0
  (card_eq_ge_transitive-1 nil 3316966605
   ("" (expand* "card_eq" "card_ge")
    (("" (skosimp*)
      (("" (use "bijective_inverse_exists[(S1!1), (S2!1)]")
        (("" (expand "exists1")
          (("" (skosimp*)
            (("" (use "bij_inv_is_bij_alt[(S1!1), (S2!1)]")
              (("" (expand "bijective?" -1)
                (("" (flatten)
                  ((""
                    (use "composition_injective[(S3!1), (S2!1), (S1!1)]")
                    (("" (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 "[(S2!1) -> (S1!1)]"
     card_comp_set_transitive nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (O const-decl "T3" function_props nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (f!2 skolem-const-decl "[(S3!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (f!1 skolem-const-decl "[(S1!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (bijective? const-decl "bool" functions nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (T2 formal-type-decl nil card_comp_set_transitive 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_transitive nil)
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (card_eq const-decl "bool" card_comp_set nil)
    (card_ge const-decl "bool" card_comp_set nil))
   shostak))
 (card_ge_eq_transitive 0
  (card_ge_eq_transitive-1 nil 3316966787
   ("" (expand* "card_ge" "card_eq")
    (("" (skosimp*)
      (("" (use "bijective_inverse_exists[(S2!1), (S3!1)]")
        (("" (expand "exists1")
          (("" (skosimp*)
            (("" (use "bij_inv_is_bij_alt[(S2!1), (S3!1)]")
              (("" (expand "bijective?" -1)
                (("" (flatten)
                  ((""
                    (use "composition_injective[(S3!1), (S2!1), (S1!1)]")
                    (("" (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 "[(S3!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (O const-decl "T3" function_props nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (f!1 skolem-const-decl "[(S2!1) -> (S1!1)]"
     card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (composition_injective judgement-tcc nil function_props nil)
    (T1 formal-type-decl nil card_comp_set_transitive nil)
    (f!2 skolem-const-decl "[(S2!1) -> (S3!1)]"
     card_comp_set_transitive nil)
    (bijective? const-decl "bool" functions nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (T3 formal-type-decl nil card_comp_set_transitive 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_transitive nil)
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (card_ge const-decl "bool" card_comp_set nil)
    (card_eq const-decl "bool" card_comp_set nil))
   shostak))
 (card_ge_transitive 0
  (card_ge_transitive-1 nil 3316966978
   ("" (expand "card_ge")
    (("" (skosimp*)
      (("" (use "composition_injective[(S3!1), (S2!1), (S1!1)]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (f!1 skolem-const-decl "[(S2!1) -> (S1!1)]"
     card_comp_set_transitive nil)
    (f!2 skolem-const-decl "[(S3!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (T1 formal-type-decl nil card_comp_set_transitive nil)
    (T2 formal-type-decl nil card_comp_set_transitive nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_ge const-decl "bool" card_comp_set nil))
   shostak))
 (card_eq_gt_transitive 0
  (card_eq_gt_transitive-1 nil 3316967003
   ("" (expand* "card_eq" "card_gt")
    (("" (skosimp*)
      (("" (use "bijective_inverse_exists[(S1!1), (S2!1)]")
        (("" (expand "exists1")
          (("" (skosimp*)
            (("" (use "bij_inv_is_bij_alt[(S1!1), (S2!1)]")
              (("" (expand "bijective?" -1)
                (("" (flatten)
                  ((""
                    (use "composition_injective[(S2!1), (S1!1), (S3!1)]")
                    (("" (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 "[(S2!1) -> (S1!1)]"
     card_comp_set_transitive nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (O const-decl "T3" function_props nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (f!2 skolem-const-decl "[(S1!1) -> (S3!1)]"
     card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (composition_injective judgement-tcc nil function_props nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (f!1 skolem-const-decl "[(S1!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (bijective? const-decl "bool" functions nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (T2 formal-type-decl nil card_comp_set_transitive 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_transitive nil)
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (card_eq const-decl "bool" card_comp_set nil)
    (card_gt const-decl "bool" card_comp_set nil))
   shostak))
 (card_ge_gt_transitive 0
  (card_ge_gt_transitive-1 nil 3316967051
   ("" (expand* "card_ge" "card_gt")
    (("" (skosimp*)
      (("" (use "composition_injective[(S2!1), (S1!1), (S3!1)]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (f!2 skolem-const-decl "[(S1!1) -> (S3!1)]"
     card_comp_set_transitive nil)
    (f!1 skolem-const-decl "[(S2!1) -> (S1!1)]"
     card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (T1 formal-type-decl nil card_comp_set_transitive 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_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_ge const-decl "bool" card_comp_set nil)
    (card_gt const-decl "bool" card_comp_set nil))
   shostak))
 (card_gt_eq_transitive 0
  (card_gt_eq_transitive-1 nil 3316967073
   ("" (expand* "card_gt" "card_eq")
    (("" (skosimp*)
      (("" (use "bijective_inverse_exists[(S2!1), (S3!1)]")
        (("" (expand "exists1")
          (("" (skosimp*)
            (("" (use "bij_inv_is_bij_alt[(S2!1), (S3!1)]")
              (("" (expand "bijective?" -1)
                (("" (flatten)
                  ((""
                    (use "composition_injective[(S1!1), (S3!1), (S2!1)]")
                    (("" (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 "[(S3!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (inverse? const-decl "bool" function_inverse_def nil)
    (O const-decl "T3" function_props nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (f!2 skolem-const-decl "[(S1!1) -> (S3!1)]"
     card_comp_set_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (T1 formal-type-decl nil card_comp_set_transitive nil)
    (f!1 skolem-const-decl "[(S2!1) -> (S3!1)]"
     card_comp_set_transitive nil)
    (bijective? const-decl "bool" functions nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (T3 formal-type-decl nil card_comp_set_transitive 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_transitive nil)
    (bijective_inverse_exists formula-decl nil function_inverse_def
     nil)
    (card_gt const-decl "bool" card_comp_set nil)
    (card_eq const-decl "bool" card_comp_set nil))
   shostak))
 (card_gt_ge_transitive 0
  (card_gt_ge_transitive-1 nil 3316967127
   ("" (expand* "card_gt" "card_ge")
    (("" (skosimp*)
      (("" (use "composition_injective[(S1!1), (S3!1), (S2!1)]")
        (("" (inst?) nil nil)) nil))
      nil))
    nil)
   ((O const-decl "T3" function_props nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (f!1 skolem-const-decl "[(S3!1) -> (S2!1)]"
     card_comp_set_transitive nil)
    (f!2 skolem-const-decl "[(S1!1) -> (S3!1)]"
     card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (T2 formal-type-decl nil card_comp_set_transitive nil)
    (T3 formal-type-decl nil card_comp_set_transitive 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_transitive nil)
    (composition_injective judgement-tcc nil function_props nil)
    (card_gt const-decl "bool" card_comp_set nil)
    (card_ge const-decl "bool" card_comp_set nil))
   shostak))
 (card_gt_transitive 0
  (card_gt_transitive-1 nil 3316967160
   ("" (expand "card_gt")
    (("" (skosimp)
      (("" (lemma "injective_dichotomous[(S1!1), (S2!1)]")
        (("" (prop)
          (("" (skosimp*)
            (("" (use "composition_injective[(S2!1), (S1!1), (S3!1)]")
              (("" (inst?) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((composition_injective judgement-tcc nil function_props nil)
    (T3 formal-type-decl nil card_comp_set_transitive nil)
    (S2!1 skolem-const-decl "set[T2]" card_comp_set_transitive nil)
    (S1!1 skolem-const-decl "set[T1]" card_comp_set_transitive nil)
    (injective? const-decl "bool" functions nil)
    (f!1 skolem-const-decl "[(S2!1) -> (S1!1)]"
     card_comp_set_transitive nil)
    (f!2 skolem-const-decl "[(S1!1) -> (S3!1)]"
     card_comp_set_transitive nil)
    (S3!1 skolem-const-decl "set[T3]" card_comp_set_transitive nil)
    (O const-decl "T3" function_props nil)
    (injective_dichotomous formula-decl nil set_dichotomous "orders/")
    (T1 formal-type-decl nil card_comp_set_transitive 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_transitive nil)
    (card_gt const-decl "bool" card_comp_set nil))
   shostak)))


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



Druckansicht
unsichere Verbindung
Druckansicht
Hier finden Sie eine Liste der Produkte des Unternehmens

Mittel




Lebenszyklus

Die hierunter aufgelisteten Ziele sind für diese Firma wichtig


Ziele

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