| products/sources/formale sprachen/Coq/doc/plugin_tutorial/tuto2/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: IO.vdmrt Sprache: LispUntersuchung PVS© |
|
||||||
|
(finite_sets_card_from
(card_extension 0 (card_extension-2 "How diff" 3389097530 ("" (skosimp*) (("" (expand "extend") (("" (lemma "finite_sets_card_eq[T1,T2].card_eq_bij") (("" (inst?) (("1" (prop) (("1" (hide 2 3) (("1" (inst 1 "lambda (t:(F!1)):t") (("1" (expand "bijective?") (("1" (prop) (("1" (expand "injective?") (("1" (grind) nil nil)) nil) ("2" (expand "surjective?") (("2" (skosimp*) (("2" (typepred "y!1") (("2" (inst 1 "y!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (prop) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "extend_set_props[T1,T2].finite_extension") (("2" (inst -1 "F!1") (("2" (typepred "F!1") (("2" (prop) (("2" (hide -2 -3) (("2" (expand "extend") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((extend const-decl "R" extend nil) (FALSE const-decl "bool" booleans nil) (F!1 skolem-const-decl "finite_set[T2]" finite_sets_card_from nil) (finite_set type-eq-decl nil finite_sets nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (is_finite const-decl "bool" finite_sets nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (bijective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (injective? const-decl "bool" functions nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (finite_extension formula-decl nil extend_set_props nil) (card_eq_bij formula-decl nil finite_sets_card_eq "finite_sets/") (T1 formal-type-decl nil finite_sets_card_from nil) (boolean nonempty-type-decl nil booleans nil) (T2_pred const-decl "[T1 -> boolean]" finite_sets_card_from nil) (T2 formal-subtype-decl nil finite_sets_card_from nil)) shostak) (card_extension-1 nil 3389097499 ("" (skosimp*) (("" (expand "extend") (("" (lemma "finite_sets_card_eq[T1,T2].card_eq_bij") (("" (inst?) (("1" (prop) (("1" (hide 2 3) (("1" (inst 1 "lambda (t:(F!1)):t") (("1" (expand "bijective?") (("1" (prop) (("1" (expand "injective?") (("1" (grind) nil))) ("2" (expand "surjective?") (("2" (skosimp*) (("2" (typepred "y!1") (("2" (inst 1 "y!1") nil))))))))))) ("2" (skosimp*) (("2" (prop) nil))))))))) ("2" (hide 2) (("2" (lemma "extend_set_props[T1,T2].finite_extension") (("2" (inst -1 "F!1") (("2" (typepred "F!1") (("2" (prop) (("2" (hide -2 -3) (("2" (expand "extend") (("2" (propax) nil)))))))))))))))))))))) nil) ((card_eq_bij formula-decl nil finite_sets_card_eq "finite_sets/")) nil))) ¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.22Angebot Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können ¤ |
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
ZieleEntwicklung einer Software für die statische QuellcodeanalyseBot Zugriff |
