|
(constant_continuity
(const_continuous_at 0
(const_continuous_at-1 nil 3301542630
("" (expand "continuous_at?")
(("" (expand "neighbourhood?")
(("" (expand "interior_point?")
(("" (skosimp*)
(("" (typepred "U!2")
(("" (assert)
(("" (inst + "inverse_image(const_fun(a!1), U!2)")
(("1"
(lemma "inverse_image_subset[T1,T2]"
("Y1" "U!2" "Y2" "U!1" "f" "const_fun[T1,T2](a!1)"))
(("1" (assert)
(("1" (lemma "topology1")
(("1" (lemma "open_fullset[T1,S]")
(("1" (expand "inverse_image")
(("1" (assert) nil nil)) nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (expand "inverse_image")
(("2" (expand "const_fun")
(("2" (expand "member")
(("2" (replace -3)
(("2" (lemma "open_fullset[T1,S]")
(("1" (expand "fullset")
(("1" (propax) nil nil)) nil)
("2" (lemma "topology1")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((neighbourhood? const-decl "bool" topology nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(member const-decl "bool" sets nil)
(fullset const-decl "set" sets nil)
(inverse_image_subset formula-decl nil function_image nil)
(open_fullset formula-decl nil topology nil)
(fullset_is_clopen name-judgement "clopen" constant_continuity nil)
(T1 formal-type-decl nil constant_continuity nil)
(S formal-const-decl "topology[T1]" constant_continuity nil)
(inverse_image const-decl "set[D]" function_image nil)
(const_fun const-decl "[S -> T]" const_fun_def "structures/")
(a!1 skolem-const-decl "T2" constant_continuity nil)
(U!2 skolem-const-decl "open[T2, T]" constant_continuity nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T2 formal-type-decl nil constant_continuity nil)
(set type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(topology? const-decl "bool" topology_prelim nil)
(topology nonempty-type-eq-decl nil topology_prelim nil)
(T formal-const-decl "topology[T2]" constant_continuity nil)
(open? const-decl "bool" topology nil)
(open nonempty-type-eq-decl nil topology nil)
(interior_point? const-decl "bool" topology nil)
(continuous_at? const-decl "bool" continuity_def nil))
shostak))
(const_continuous 0
(const_continuous-1 nil 3301542853
("" (expand "continuous?")
(("" (skosimp*)
(("" (lemma "const_continuous_at" ("a" "a!1" "x" "x!1"))
(("" (propax) nil nil)) nil))
nil))
nil)
((const_continuous_at formula-decl nil constant_continuity nil)
(T2 formal-type-decl nil constant_continuity nil)
(T1 formal-type-decl nil constant_continuity nil)
(continuous? const-decl "bool" continuity_def nil))
shostak))
(const_is_continuous 0
(const_is_continuous-1 nil 3358747663
("" (skosimp)
(("" (lemma "const_continuous" ("a" "a!1")) (("" (propax) nil nil))
nil))
nil)
((T2 formal-type-decl nil constant_continuity nil)
(const_continuous formula-decl nil constant_continuity nil))
nil)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.1Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Entwicklung einer Software für die statische Quellcodeanalyse
|
