| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/topology/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 7 kB |
|
Quelle homeomorphic_transitive.prf Sprache: Lisp |
|||||||||
|
(homeomorphic_transitive
(homeomorphic_transitive 0 (homeomorphic_transitive-1 nil 3301538739 ("" (expand "homeomorphic?") (("" (skosimp*) (("" (expand "homeomorphism?") (("" (flatten) (("" (inst + "f!2 o f!1") (("" (lemma "composition_bijective[T1,T2,T3]" ("f1" "f!1" "f2" "f!2")) (("1" (assert) (("1" (lemma "composition_continuous[T1,S,T2,T,T3,U]" ("f" "f!2" "g" "f!1")) (("1" (assert) (("1" (rewrite "composition_inverse_alt" 1) (("1" (lemma "composition_continuous[T3,U,T2,T,T1,S]") (("1" (case "nonempty?(fullset[T1])") (("1" (case "EXISTS (x:T1): TRUE") (("1" (case "EXISTS (y:T2): TRUE") (("1" (case "EXISTS (z:T3): TRUE") (("1" (inst - "inverse_alt(f!1)" "inverse_alt(f!2)") (("1" (assert) nil nil) ("2" (flatten) nil nil) ("3" (flatten) nil nil)) nil) ("2" (skolem! -) (("2" (inst + "f!2(y!1)") nil nil)) nil)) nil) ("2" (skolem! -) (("2" (inst + "f!1(x!1)") nil nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "fullset") (("2" (expand "nonempty?") (("2" (expand "empty?") (("2" (skosimp) (("2" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (rewrite "emptyset_is_empty?" -1) (("2" (hide -2 -3 -4 -6 -7 -9 -10) (("2" (expand "bijective?") (("2" (flatten) (("2" (expand "continuous?") (("2" (skosimp) (("2" (expand "surjective?") (("2" (inst -5 "x!1") (("2" (skosimp) (("2" (inst - "x!2") (("2" (skosimp) (("2" (rewrite "extensionality_postulate" -1 :dir rl) (("2" (inst - "x!3") (("2" (expand "emptyset") (("2" (expand "fullset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((bijective? const-decl "bool" functions nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (composition_bijective judgement-tcc nil function_props nil) (U formal-const-decl "topology[T3]" homeomorphic_transitive nil) (T formal-const-decl "topology[T2]" homeomorphic_transitive nil) (S formal-const-decl "topology[T1]" homeomorphic_transitive nil) (topology nonempty-type-eq-decl nil topology_prelim nil) (topology? const-decl "bool" topology_prelim nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (composition_continuous formula-decl nil composition_continuity nil) (composition_inverse_alt formula-decl nil function_props_aux "structures/") (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (fullset const-decl "set" sets nil) (empty? const-decl "bool" sets nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (FALSE const-decl "bool" booleans nil) (inverse_alt const-decl "inverses(f)" function_inverse_alt nil) (inverses nonempty-type-eq-decl nil function_inverse_alt nil) (inverse? const-decl "bool" function_inverse_def nil) (TRUE const-decl "bool" booleans nil) (emptyset_is_empty? formula-decl nil sets_lemmas nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (continuous? const-decl "bool" continuity_def nil) (surjective? const-decl "bool" functions nil) (extensionality_postulate formula-decl nil functions nil) (emptyset const-decl "set" sets nil) (O const-decl "T3" function_props nil) (T2 formal-type-decl nil homeomorphic_transitive nil) (T3 formal-type-decl nil homeomorphic_transitive nil) (T1 formal-type-decl nil homeomorphic_transitive nil) (homeomorphism? const-decl "bool" homeomorphism_def nil) (homeomorphic? const-decl "bool" homeomorphism_def nil)) shostak))) ¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28