|
(scott
(down_is_closed 0
(down_is_closed-1 nil 3330142088
("" (skosimp)
(("" (expand "member")
(("" (expand "scott_closed_sets")
(("" (expand "extend")
(("" (skosimp)
(("" (expand "member")
(("" (expand "subset?")
(("" (expand "member")
(("" (typepred "lub(D!1)")
(("1" (expand "least_upper_bound?")
(("1" (flatten)
(("1" (expand "down")
(("1" (inst - "x!1")
(("1" (split -2)
(("1" (propax) nil nil)
("2"
(hide 2)
(("2"
(expand "upper_bound?")
(("2"
(skosimp)
(("2"
(typepred "r!1")
(("2"
(inst -3 "r!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "<=")
(("2" (expand "directed_complete_partial_order?")
(("2" (flatten) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((member const-decl "bool" sets nil)
(extend const-decl "R" extend nil)
(down const-decl "lower_set" partial_order_props "orders/")
(upper_bound? const-decl "bool" bounded_orders "orders/")
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil scott nil) (set type-eq-decl nil sets nil)
(pred type-eq-decl nil defined_types nil)
(least_upper_bound? const-decl "bool" bounded_orders "orders/")
(directed_complete_partial_order? const-decl "bool" directed_orders
"orders/")
(<= formal-const-decl "(directed_complete_partial_order?[T])" scott
nil)
(lub_set? const-decl "bool" bounded_order_props "orders/")
(lub const-decl
"{x | bounded_orders[T].least_upper_bound?(x, SA, <=)}"
bounded_order_props "orders/")
(nonempty? const-decl "bool" sets nil)
(directed? const-decl "bool" directed_order_props "orders/")
(directed type-eq-decl nil directed_order_props "orders/")
(subset? const-decl "bool" sets nil)
(scott_closed_sets const-decl "setofsets[T]" scott nil))
shostak))
(scott_empty 0
(scott_empty-1 nil 3329467322
("" (expand "scott_closed_sets")
(("" (expand "member")
(("" (expand "extend") (("" (grind) nil nil)) nil)) nil))
nil)
((finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" scott nil)
(member const-decl "bool" sets nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil scott nil) (set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(pred type-eq-decl nil defined_types nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
"orders/")
(<= formal-const-decl "(directed_complete_partial_order?[T])" scott
nil)
(directed? const-decl "bool" directed_order_props "orders/")
(directed type-eq-decl nil directed_order_props "orders/")
(directed? const-decl "bool" directed_orders "orders/")
(empty? const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(emptyset const-decl "set" sets nil)
(lower_set? const-decl "bool" partial_order_props "orders/")
(extend const-decl "R" extend nil)
(scott_closed_sets const-decl "setofsets[T]" scott nil))
shostak))
(scott_full 0
(scott_full-1 nil 3329488152 ("" (grind) nil nil)
((member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(scott_closed_sets const-decl "setofsets[T]" scott nil)
(fullset const-decl "set" sets nil)
(<= formal-const-decl "(directed_complete_partial_order?[T])" scott
nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
"orders/")
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil scott nil)
(lower_set? const-decl "bool" partial_order_props "orders/")
(extend const-decl "R" extend nil))
shostak))
(scott_union 0
(scott_union-1 nil 3329489659
("" (skosimp)
(("" (typepred "A!1")
(("" (typepred "B!1")
(("" (expand "union")
(("" (expand "member")
(("" (expand "scott_closed_sets")
(("" (expand "extend")
(("" (prop)
(("1" (skosimp*)
(("1" (typepred "D!1")
(("1"
(lemma "directed_union_lower"
("D" "D!1" "L1" "A!1" "L2" "B!1"))
(("1" (expand "union")
(("1" (expand "member")
(("1" (assert)
(("1"
(flatten)
(("1"
(split -1)
(("1"
(inst -7 "D!1")
(("1" (assert) nil nil))
nil)
("2"
(inst -9 "D!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil) ("3" (propax) nil nil))
nil))
nil))
nil)
("2" (hide -2 -4)
(("2" (expand "lower_set?")
(("2" (expand "member")
(("2" (skosimp*)
(("2" (inst - "x!1" "y!1")
(("2" (inst - "x!1" "y!1")
(("2"
(split -1)
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((scott_closed_sets const-decl "setofsets[T]" scott nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(T formal-type-decl nil scott nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(union const-decl "set" sets nil)
(directed type-eq-decl nil directed_order_props "orders/")
(directed? const-decl "bool" directed_order_props "orders/")
(<= formal-const-decl "(directed_complete_partial_order?[T])" scott
nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
"orders/")
(pred type-eq-decl nil defined_types nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(lower_set nonempty-type-eq-decl nil partial_order_props "orders/")
(lower_set? const-decl "bool" partial_order_props "orders/")
(directed_union_lower formula-decl nil directed_order_props
"orders/")
(extend const-decl "R" extend nil)
(member const-decl "bool" sets nil))
shostak))
(scott_Intersection 0
(scott_Intersection-1 nil 3329541686
("" (expand "scott_closed_sets")
(("" (expand "Intersection")
(("" (expand "subset?")
(("" (expand "extend")
(("" (expand "member")
(("" (skosimp*)
(("" (typepred "LS!1")
(("" (prop)
(("1" (skosimp*)
(("1" (typepred "D!1")
(("1" (typepred "lub(D!1)")
(("1" (typepred "a!1")
(("1" (inst -8 "a!1")
(("1" (replace -1)
(("1"
(assert)
(("1"
(prop)
(("1"
(inst -2 "D!1")
(("1"
(split -2)
(("1" (propax) nil nil)
("2"
(hide 2)
(("2"
(skosimp)
(("2"
(inst -8 "x!1")
(("2"
(assert)
(("2"
(inst -8 "a!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "<=")
(("2"
(expand "directed_complete_partial_order?")
(("2" (flatten) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (expand "lower_sets?")
(("2" (expand "every")
(("2" (expand "lower_set?")
(("2" (skosimp)
(("2" (expand "member")
(("2" (skosimp)
(("2"
(typepred "a!1")
(("2"
(inst - "a!1")
(("2"
(inst - "a!1")
(("2"
(inst - "x!1" "y!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Intersection const-decl "set" sets nil)
(extend const-decl "R" extend nil) (set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(directed? const-decl "bool" directed_order_props "orders/")
(directed type-eq-decl nil directed_order_props "orders/")
(lub const-decl
"{x | bounded_orders[T].least_upper_bound?(x, SA, <=)}"
bounded_order_props "orders/")
(lub_set? const-decl "bool" bounded_order_props "orders/")
(least_upper_bound? const-decl "bool" bounded_orders "orders/")
(every const-decl "bool" sets nil)
(lower_set? const-decl "bool" partial_order_props "orders/")
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil scott nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(pred type-eq-decl nil defined_types nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
"orders/")
(<= formal-const-decl "(directed_complete_partial_order?[T])" scott
nil)
(lower_sets? const-decl "bool" partial_order_props "orders/")
(lower_sets nonempty-type-eq-decl nil partial_order_props
"orders/")
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(scott_closed_sets const-decl "setofsets[T]" scott nil))
shostak))
(scott_topology 0
(scott_topology-1 nil 3327377085
("" (expand "scott_open_sets")
(("" (expand "Complement")
(("" (expand "topology?")
(("" (split)
(("1" (expand "topology_empty?")
(("1" (lemma "scott_full")
(("1" (expand "member")
(("1" (inst + "fullset[T]")
(("1" (rewrite "complement_fullset") nil nil)) nil))
nil))
nil))
nil)
("2" (lemma "scott_empty")
(("2" (expand "topology_full?")
(("2" (expand "member")
(("2" (inst + "emptyset[T]")
(("2" (rewrite "complement_emptyset") nil nil)) nil))
nil))
nil))
nil)
("3" (expand "topology_Union?")
(("3" (skosimp)
(("3" (expand "member")
(("3"
(lemma "scott_Intersection" ("LS" "Complement(U!1)"))
(("1" (split -1)
(("1" (expand "member")
(("1" (inst + "Intersection(Complement(U!1))")
(("1" (rewrite "Demorgan2")
(("1" (rewrite "Complement_Complement") nil
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "Complement")
(("2" (expand "subset?")
(("2" (expand "member")
(("2" (skosimp)
(("2"
(skosimp)
(("2"
(typepred "b!1")
(("2"
(inst - "b!1")
(("2"
(assert)
(("2"
(skosimp)
(("2"
(typepred "b!2")
(("2"
(replace -4)
(("2"
(rewrite
"complement_complement")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "lower_sets?")
(("2" (expand "every")
(("2" (skosimp)
(("2" (typepred "x!1")
(("2" (expand "Complement")
(("2"
(skosimp)
(("2"
(typepred "b!1")
(("2"
(expand "subset?")
(("2"
(expand "member")
(("2"
(inst - "b!1")
(("2"
(assert)
(("2"
(skosimp)
(("2"
(replace -3)
(("2"
(typepred "b!2")
(("2"
(rewrite
"complement_complement")
(("2"
(assert)
(("2"
(replace -3 * rl)
(("2"
(hide-all-but
(-1 1))
(("2"
(expand
"lower_set?")
(("2"
(expand
"member")
(("2"
(skosimp)
(("2"
(expand
"scott_closed_sets")
(("2"
(expand
"extend")
(("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))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (expand "topology_intersection?")
(("4" (skosimp*)
(("4" (typepred "A!1")
(("4" (typepred "B!1")
(("4" (skosimp*)
(("4" (lemma "scott_union")
(("4" (typepred "b!1")
(("4" (typepred "b!2")
(("4" (inst - "b!2" "b!1")
(("4" (expand "member")
(("4"
(inst + "union(b!2, b!1)")
(("4"
(replace -4)
(("4"
(replace -5)
(("4"
(rewrite "demorgan1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Complement const-decl "setofsets[T]" sets_lemmas nil)
(scott_full formula-decl nil scott nil)
(fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(scott_closed_sets const-decl "setofsets[T]" scott nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil scott nil)
(complement_fullset formula-decl nil sets_lemmas nil)
(finite_emptyset name-judgement "finite_set[T]" scott nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(member const-decl "bool" sets nil)
(topology_empty? const-decl "bool" topology_prelim "topology/")
(topology_full? const-decl "bool" topology_prelim "topology/")
(emptyset const-decl "set" sets nil)
(complement_emptyset formula-decl nil sets_lemmas nil)
(scott_empty formula-decl nil scott nil)
(lower_sets nonempty-type-eq-decl nil partial_order_props
"orders/")
(lower_sets? const-decl "bool" partial_order_props "orders/")
(<= formal-const-decl "(directed_complete_partial_order?[T])" scott
nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
"orders/")
(pred type-eq-decl nil defined_types nil)
(scott_Intersection formula-decl nil scott nil)
(Complement_bijective name-judgement
"(bijective?[setofsets[T], setofsets[T]])" sets_lemmas nil)
(subset? const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(complement_complement formula-decl nil sets_lemmas nil)
(Demorgan2 formula-decl nil sets_lemmas nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(Complement_Complement formula-decl nil sets_lemmas nil)
(U!1 skolem-const-decl "setofsets[T]" scott nil)
(Intersection const-decl "set" sets nil)
(Intersection_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(lower_set? const-decl "bool" partial_order_props "orders/")
(extend const-decl "R" extend nil)
(every const-decl "bool" sets nil)
(topology_Union? const-decl "bool" topology_prelim "topology/")
(scott_union formula-decl nil scott nil)
(demorgan1 formula-decl nil sets_lemmas nil)
(b!1 skolem-const-decl "(scott_closed_sets)" scott nil)
(b!2 skolem-const-decl "(scott_closed_sets)" scott nil)
(union const-decl "set" sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(complement const-decl "set" sets nil)
(topology_intersection? const-decl "bool" topology_prelim
"topology/")
(topology? const-decl "bool" topology_prelim "topology/")
(scott_open_sets const-decl "setofsets[T]" scott nil))
shostak))
(scott_open_sets_is_topology 0
(scott_open_sets_is_topology-1 nil 3353640969
("" (lemma "scott_topology") (("" (propax) nil nil)) nil)
((scott_topology formula-decl nil scott nil)) nil))
(closed_is_lower 0
(closed_is_lower-1 nil 3330135344
("" (skosimp)
(("" (typepred "x!1")
(("" (lemma "lt_order")
(("" (expand "closed?")
(("" (expand "member")
(("" (expand "scott_open_sets")
(("" (expand "Complement")
(("" (skosimp)
(("" (typepred "b!1")
(("" (expand "scott_closed_sets")
(("" (expand "extend")
(("" (rewrite "complement_equal")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((closed? const-decl "bool" topology "topology/")
(scott_open_sets const-decl "setofsets[T]" scott nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil) (T formal-type-decl nil scott nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(member const-decl "bool" sets nil)
(Complement const-decl "setofsets[T]" sets_lemmas nil)
(scott_closed_sets const-decl "setofsets[T]" scott nil)
(extend const-decl "R" extend nil)
(complement_equal formula-decl nil sets_lemmas nil))
shostak))
(open_is_upper 0
(open_is_upper-1 nil 3330134932
("" (skosimp)
(("" (typepred "x!1")
(("" (lemma "closed_complement" ("A" "x!1"))
(("" (assert)
(("" (lemma "closed_is_lower" ("x" "complement(x!1)"))
(("" (lemma "complement_lower_set" ("L" "complement(x!1)"))
(("1" (rewrite "complement_complement") nil nil)
("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((open? const-decl "bool" topology "topology/")
(scott_open_sets const-decl "setofsets[T]" scott nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil) (T formal-type-decl nil scott nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(complement_open_is_closed application-judgement
"closed[T, scott_open_sets]" scott nil)
(<= formal-const-decl "(directed_complete_partial_order?[T])" scott
nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
"orders/")
(pred type-eq-decl nil defined_types nil)
(lower_set nonempty-type-eq-decl nil partial_order_props "orders/")
(lower_set? const-decl "bool" partial_order_props "orders/")
(complement_lower_set judgement-tcc nil partial_order_props
"orders/")
(complement_complement formula-decl nil sets_lemmas nil)
(closed_is_lower judgement-tcc nil scott nil)
(closed? const-decl "bool" topology "topology/")
(complement const-decl "set" sets nil)
(closed_complement formula-decl nil topology "topology/"))
shostak))
(closure_is_down 0
(closure_is_down-1 nil 3352264609
("" (skolem 1 ("y"))
(("" (apply-extensionality 1 :hide? t)
(("1" (lemma "down_is_closed" ("x" "y"))
(("1" (expand "member")
(("1" (expand "Cl")
(("1" (expand "adherent_point?")
(("1" (lemma "open_complement" ("A" "down(y)"))
(("1" (expand "closed?")
(("1" (expand "member")
(("1" (expand "scott_open_sets")
(("1" (expand "Complement")
(("1" (flatten -1)
(("1" (hide -1)
(("1" (split -1)
(("1"
(case-replace "down(y)(x!1)")
(("1"
(skosimp)
(("1"
(expand "singleton")
(("1"
(expand "intersection")
(("1"
(expand "nonempty?")
(("1"
(expand "empty?")
(("1"
(expand "member")
(("1"
(typepred "U!1")
(("1"
(expand
"neighbourhood?")
(("1"
(expand
"interior_point?")
(("1"
(skosimp)
(("1"
(expand "member")
(("1"
(inst - "y")
(("1"
(expand
"down")
(("1"
(typepred
"U!2")
(("1"
(lemma
"open_is_upper"
("x"
"U!2"))
(("1"
(expand
"upper_set?")
(("1"
(expand
"member")
(("1"
(inst
-
"x!1"
"y")
(("1"
(assert)
(("1"
(expand
"subset?")
(("1"
(inst
-
"y")
(("1"
(expand
"member")
(("1"
(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"
(assert)
(("2"
(expand "singleton")
(("2"
(expand "intersection")
(("2"
(expand "nonempty?")
(("2"
(expand "empty?")
(("2"
(expand "member")
(("2"
(inst
-
"complement(down(y))")
(("1"
(split -3)
(("1"
(skosimp)
(("1"
(replace -2)
(("1"
(expand
"complement")
(("1"
(expand
"member")
(("1"
(expand
"down")
(("1"
(rewrite
"partial_order_reflexive")
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"neighbourhood?")
(("2"
(expand
"interior_point?")
(("2"
(inst
+
"complement(down(y))")
(("1"
(rewrite
"subset_reflexive")
(("1"
(expand
"member")
(("1"
(expand
"complement")
(("1"
(expand
"member")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(typepred "<=")
(("2"
(expand
"directed_complete_partial_order?")
(("2"
(flatten)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(typepred "<=")
(("2"
(expand
"directed_complete_partial_order?")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst + "down(y)")
(("2"
(typepred "<=")
(("2"
(expand
"directed_complete_partial_order?")
(("2" (flatten) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "<=")
(("2" (expand "directed_complete_partial_order?")
(("2" (flatten) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "<=")
(("2" (expand "directed_complete_partial_order?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil)
((T formal-type-decl nil scott nil)
(boolean nonempty-type-decl nil booleans nil)
(down const-decl "lower_set" partial_order_props "orders/")
(lower_set nonempty-type-eq-decl nil partial_order_props "orders/")
(lower_set? const-decl "bool" partial_order_props "orders/")
(<= formal-const-decl "(directed_complete_partial_order?[T])" scott
nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
"orders/")
(pred type-eq-decl nil defined_types nil)
(singleton const-decl "(singleton?)" sets nil)
(singleton? const-decl "bool" sets nil)
(Cl const-decl "set[T]" topology "topology/")
(scott_open_sets const-decl "setofsets[T]" scott nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(scott_open_sets_is_topology name-judgement "topology" scott nil)
(Cl_is_closed application-judgement "closed[T, scott_open_sets]"
scott nil)
(singleton_is_compact application-judgement
"compact[T, scott_open_sets]" scott nil)
(directed_singleton application-judgement "directed[T, <=]" scott
nil)
(member const-decl "bool" sets nil)
(finite_intersection1 application-judgement "finite_set[T]" scott
nil)
(adherent_point? const-decl "bool" topology "topology/")
(complement_lower_set application-judgement "upper_set[T, <=]"
scott nil)
(closed? const-decl "bool" topology "topology/")
(complement const-decl "set" sets nil)
(subset_reflexive formula-decl nil sets_lemmas nil)
(partial_order_reflexive formula-decl nil partial_order_props
"orders/")
(intersection const-decl "set" sets nil)
(empty? const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(open? const-decl "bool" topology "topology/")
(open nonempty-type-eq-decl nil topology "topology/")
(interior_point? const-decl "bool" topology "topology/")
(open_is_upper judgement-tcc nil scott nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(subset? const-decl "bool" sets nil)
(upper_set? const-decl "bool" partial_order_props "orders/")
(neighbourhood? const-decl "bool" topology "topology/")
(nonempty? const-decl "bool" sets nil)
(y skolem-const-decl "T" scott nil)
(scott_closed_sets const-decl "setofsets[T]" scott nil)
(Complement const-decl "setofsets[T]" sets_lemmas nil)
(open_complement formula-decl nil topology "topology/")
(down_is_closed formula-decl nil scott nil))
shostak))
(order_iff_closure 0
(order_iff_closure-1 nil 3330140630
("" (skosimp)
(("" (rewrite "closure_is_down")
(("" (expand "down")
(("" (expand "member") (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((closure_is_down formula-decl nil scott nil)
(T formal-type-decl nil scott nil)
(member const-decl "bool" sets nil)
(down const-decl "lower_set" partial_order_props "orders/"))
shostak))
(order_iff_subset 0
(order_iff_subset-1 nil 3330144953
("" (skosimp)
(("" (split)
(("1" (flatten)
(("1" (skosimp)
(("1" (typepred "A!1")
(("1" (lemma "open_is_upper" ("x" "A!1"))
(("1" (expand "upper_set?")
(("1" (expand "member")
(("1" (inst - "x!1" "y!1") (("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (expand "member")
(("2" (rewrite "order_iff_closure")
(("2"
(case "FORALL (A: (closed?)): member(y!1, A) IMPLIES member(x!1, A)")
(("1" (hide -2)
(("1" (lemma "Cl_closed" ("A" "singleton(y!1)"))
(("1" (expand "member")
(("1" (inst - "Cl(singleton(y!1))")
(("1" (split -2)
(("1" (propax) nil nil)
("2" (hide-all-but 1)
(("2"
(lemma "subset_of_Cl"
("A" "singleton(y!1)"))
(("2" (expand "subset?")
(("2"
(inst - "y!1")
(("2"
(expand "member")
(("2"
(expand "singleton" -1 1)
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp)
(("2" (expand "member")
(("2" (typepred "A!1")
(("2" (lemma "open_complement" ("A" "A!1"))
(("2" (assert)
(("2" (inst - "complement(A!1)")
(("2" (expand "complement")
(("2"
(expand "member")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((open_is_upper judgement-tcc nil scott nil)
(member const-decl "bool" sets nil)
(upper_set? const-decl "bool" partial_order_props "orders/")
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(T formal-type-decl nil scott nil) (set type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(scott_open_sets const-decl "setofsets[T]" scott nil)
(open? const-decl "bool" topology "topology/")
(open_set nonempty-type-eq-decl nil topology "topology/")
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(closed? const-decl "bool" topology "topology/")
(Cl_closed formula-decl nil topology "topology/")
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(scott_open_sets_is_topology name-judgement "topology" scott nil)
(Cl const-decl "set[T]" topology "topology/")
(subset? const-decl "bool" sets nil)
(subset_of_Cl formula-decl nil topology "topology/")
(complement_closed_is_open application-judgement
"open[T, scott_open_sets]" scott nil)
(complement const-decl "set" sets nil)
(open_complement formula-decl nil topology "topology/")
(Cl_is_closed application-judgement "closed[T, scott_open_sets]"
scott nil)
(singleton_is_compact application-judgement
"compact[T, scott_open_sets]" scott nil)
(directed_singleton application-judgement "directed[T, <=]" scott
nil)
(order_iff_closure formula-decl nil scott nil))
shostak))
(scott_is_T0 0
(scott_is_T0-1 nil 3352703320
("" (expand "T0_space?")
(("" (expand "is_T0?")
(("" (expand "member")
(("" (skosimp*)
(("" (lemma "closure_is_down")
(("" (lemma "Cl_closed")
(("" (inst-cp - "singleton(x!1)")
(("" (inst - "singleton(y!1)")
(("" (inst-cp - "x!1")
(("" (inst - "y!1")
(("" (replace -3)
(("" (replace -4)
(("" (hide -3 -4)
(("" (inst-cp + "complement(down(x!1))")
(("1"
(inst + "complement(down(y!1))")
(("1"
(flatten)
(("1"
(expand "complement")
(("1"
(expand "member")
(("1"
(expand "down")
(("1"
(lemma
"partial_order_antisymmetric")
(("1"
(inst - "x!1" "y!1")
(("1"
(rewrite
"partial_order_reflexive")
(("1"
(rewrite
"partial_order_reflexive")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "scott_open_sets")
(("2"
(expand "Complement")
(("2"
(inst + "down(y!1)")
(("1"
(assert)
(("1"
(expand "closed?")
(("1"
(expand "member")
(("1"
(expand
"scott_open_sets")
(("1"
(expand "Complement")
(("1"
(skosimp)
(("1"
(typepred "b!1")
(("1"
(rewrite
"complement_equal"
-2)
(("1"
(typepred "<=")
(("1"
(expand
"directed_complete_partial_order?")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(typepred "<=")
(("2"
(expand
"directed_complete_partial_order?")
(("2" (flatten) nil nil))
nil))
nil))
nil))
nil))
nil)
("3"
(typepred "<=")
(("3"
(expand
"directed_complete_partial_order?")
(("3" (flatten) nil nil))
nil))
nil))
nil)
("2"
(hide -1 2)
(("2"
(expand "closed?")
(("2"
(expand "scott_open_sets")
(("2"
(expand "Complement")
(("2"
(expand "member")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("3"
(typepred "<=")
(("3"
(expand
"directed_complete_partial_order?")
(("3" (flatten) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((is_T0? const-decl "bool" topology_prelim "topology/")
(scott_open_sets const-decl "setofsets[T]" scott nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil scott nil)
(Cl_closed formula-decl nil topology "topology/")
(complement_lower_set application-judgement "upper_set[T, <=]"
scott nil)
(complement const-decl "set" sets nil)
(pred type-eq-decl nil defined_types nil)
(directed_complete_partial_order? const-decl "bool" directed_orders
"orders/")
(<= formal-const-decl "(directed_complete_partial_order?[T])" scott
nil)
(lower_set? const-decl "bool" partial_order_props "orders/")
(lower_set nonempty-type-eq-decl nil partial_order_props "orders/")
(down const-decl "lower_set" partial_order_props "orders/")
(x!1 skolem-const-decl "T" scott nil)
(scott_closed_sets const-decl "setofsets[T]" scott nil)
(closed? const-decl "bool" topology "topology/")
(complement_equal formula-decl nil sets_lemmas nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(Complement const-decl "setofsets[T]" sets_lemmas nil)
(partial_order_antisymmetric formula-decl nil partial_order_props
"orders/")
(partial_order_reflexive formula-decl nil partial_order_props
"orders/")
(y!1 skolem-const-decl "T" scott nil)
(set type-eq-decl nil sets nil)
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(closure_is_down formula-decl nil scott nil)
(member const-decl "bool" sets nil)
(T0_space? const-decl "bool" topology_prelim "topology/")
(scott_open_sets_is_topology name-judgement "topology" scott nil))
shostak))
(scott_hausdorff 0
(scott_hausdorff-1 nil 3352743221
("" (expand "hausdorff_space?")
(("" (lemma "scott_topology")
(("" (assert)
(("" (expand "hausdorff?")
(("" (expand "is_T2?")
(("" (expand "trivial_partial_order?")
(("" (split)
(("1" (skosimp*)
(("1" (split)
(("1" (flatten)
(("1" (inst - "x!1" "y!1")
(("1" (assert)
(("1" (skosimp)
(("1" (typepred "U!1")
(("1"
(typepred "V!1")
(("1"
(expand "scott_open_sets")
(("1"
(expand "Complement")
(("1"
(skosimp*)
(("1"
(typepred "b!1")
(("1"
(typepred "b!2")
(("1"
(expand
"scott_closed_sets")
(("1"
(expand "extend")
(("1"
(prop)
(("1"
(lemma
"complement_lower_set"
("L" "b!1"))
(("1"
(lemma
"complement_lower_set"
("L" "b!2"))
(("1"
(replace -7 * rl)
(("1"
(replace
-8
*
rl)
(("1"
(hide-all-but
(1
-1
-2
-9
-11
-12
-10))
(("1"
(expand
"upper_set?")
(("1"
(expand
"member")
(("1"
(inst
-
"x!1"
"y!1")
(("1"
(assert)
(("1"
(expand
"disjoint?")
(("1"
(expand
"empty?")
(("1"
(inst
-
"y!1")
(("1"
(expand
"intersection")
(("1"
(expand
"member")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.77 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
