|
(real_topology
(IMP_metric_space_TCC1 0
(IMP_metric_space_TCC1-1 nil 3387600277
("" (expand "metric?")
(("" (expand "metric_zero?")
(("" (expand "metric_symmetric?")
(("" (expand "metric_triangle?") (("" (grind) nil nil)) nil))
nil))
nil))
nil)
((real_minus_real_is_real application-judgement "real" reals nil)
(metric_zero? const-decl "bool" metric_def nil)
(metric_triangle? const-decl "bool" metric_def nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(metric_symmetric? const-decl "bool" metric_def nil)
(metric? const-decl "bool" metric_def nil))
nil))
(interval_TCC1 0
(interval_TCC1-1 nil 3454134699 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(set type-eq-decl nil sets nil)
(interval? const-decl "bool" real_topology nil)
(emptyset const-decl "set" sets nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(emptyset_is_compact name-judgement
"compact[T, (metric_induced_topology)]" real_topology nil)
(emptyset_is_clopen name-judgement
"clopen[T, (metric_induced_topology)]" real_topology nil))
nil))
(bounded_interval_TCC1 0
(bounded_interval_TCC1-1 nil 3454134699 ("" (subtype-tcc) nil nil)
((set type-eq-decl nil sets nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(emptyset const-decl "set" sets nil)
(interval? const-decl "bool" real_topology nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil)
(upper_bound const-decl "bool" bound_defs "reals/")
(above_bounded const-decl "bool" bounded_reals "reals/")
(lower_bound const-decl "bool" bound_defs "reals/")
(below_bounded const-decl "bool" bounded_reals "reals/")
(bounded? const-decl "bool" real_topology nil)
(bounded_interval? const-decl "bool" real_topology nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(emptyset_is_compact name-judgement
"compact[T, (metric_induced_topology)]" real_topology nil)
(emptyset_is_clopen name-judgement
"clopen[T, (metric_induced_topology)]" real_topology nil))
nil))
(unbounded_interval_TCC1 0
(unbounded_interval_TCC1-1 nil 3454134699
("" (expand "fullset")
(("" (expand "unbounded_interval?")
(("" (split)
(("1" (grind) nil nil)
("2" (expand "unbounded?")
(("2" (expand "bounded?")
(("2" (expand "nonempty?")
(("2" (split)
(("1" (expand "empty?")
(("1" (inst - "0") (("1" (assert) nil nil)) nil))
nil)
("2" (flatten)
(("2" (hide 1)
(("2" (expand "above_bounded")
(("2" (skosimp)
(("2" (expand "upper_bound")
(("2" (inst - "n!1+1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((unbounded_interval? const-decl "bool" real_topology nil)
(unbounded? const-decl "bool" real_topology nil)
(nonempty? const-decl "bool" sets nil)
(above_bounded const-decl "bool" bounded_reals "reals/")
(upper_bound const-decl "bool" bound_defs "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(TRUE const-decl "bool" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(bounded? const-decl "bool" real_topology nil)
(interval? const-decl "bool" real_topology nil)
(fullset const-decl "set" sets nil))
nil))
(bounded_open_interval_TCC1 0
(bounded_open_interval_TCC1-1 nil 3454134699
("" (expand "bounded_open_interval?")
(("" (split)
(("1" (grind) nil nil)
("2" (lemma "open_emptyset")
(("2" (rewrite "metric_open_def") nil nil)) nil))
nil))
nil)
((set type-eq-decl nil sets nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(emptyset const-decl "set" sets nil)
(interval? const-decl "bool" real_topology nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil)
(upper_bound const-decl "bool" bound_defs "reals/")
(above_bounded const-decl "bool" bounded_reals "reals/")
(lower_bound const-decl "bool" bound_defs "reals/")
(below_bounded const-decl "bool" bounded_reals "reals/")
(bounded? const-decl "bool" real_topology nil)
(bounded_interval? const-decl "bool" real_topology nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(metric_open_def formula-decl nil metric_space nil)
(open_emptyset formula-decl nil topology "topology/")
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
nil)
(bounded_open_interval? const-decl "bool" real_topology nil)
(emptyset_is_clopen name-judgement
"clopen[T, (metric_induced_topology)]" real_topology nil)
(emptyset_is_compact name-judgement
"compact[T, (metric_induced_topology)]" real_topology nil)
(finite_emptyset name-judgement "finite_set[T]" countable_setofsets
"sets_aux/")
(finite_emptyset name-judgement "finite_set[T]" countable_props
"sets_aux/")
(finite_emptyset name-judgement "finite_set" finite_sets nil))
nil))
(open_interval_TCC1 0
(open_interval_TCC1-1 nil 3387600277
("" (inst + "ball(0,1)") (("" (inst + "0" "1") nil nil)) nil)
((ball const-decl "set[T]" metric_space_def nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil) (set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(open_interval_is_bounded_open_interval 0
(open_interval_is_bounded_open_interval-1 nil 3454134699
("" (skolem + "X!1")
(("" (typepred "X!1")
(("" (skosimp)
(("" (replace -1)
(("" (hide -1)
(("" (expand "bounded_open_interval?")
(("" (expand "bounded_interval?")
(("" (split)
(("1" (grind) nil nil)
("2" (expand "bounded?")
(("2" (flatten)
(("2" (hide 1)
(("2" (split)
(("1" (expand "nonempty?")
(("1" (expand "empty?")
(("1"
(inst - "x!1")
(("1" (grind) nil nil))
nil))
nil))
nil)
("2" (expand "above_bounded")
(("2" (inst + "x!1+r!1")
(("2" (grind) nil nil)) nil))
nil)
("3" (expand "below_bounded")
(("3" (inst + "x!1-r!1")
(("3" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("3" (rewrite "metric_open_ball") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((open_interval nonempty-type-eq-decl nil real_topology nil)
(ball const-decl "set[T]" metric_space_def nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(set type-eq-decl nil sets nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(bounded_open_interval? const-decl "bool" real_topology nil)
(minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(interval? const-decl "bool" real_topology nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(upper_bound const-decl "bool" bound_defs "reals/")
(above_bounded const-decl "bool" bounded_reals "reals/")
(lower_bound const-decl "bool" bound_defs "reals/")
(below_bounded const-decl "bool" bounded_reals "reals/")
(bounded? const-decl "bool" real_topology nil)
(metric_open_ball formula-decl nil metric_space nil)
(bounded_interval? const-decl "bool" real_topology nil))
nil))
(open_basis 0
(open_basis-1 nil 3389861684
("" (expand "base?")
(("" (split)
(("1" (expand "subset?")
(("1" (skosimp*)
(("1" (expand "fullset")
(("1" (expand "metric_induced_topology")
(("1" (expand "extend")
(("1" (expand "member")
(("1" (prop)
(("1" (skosimp)
(("1" (replace -1)
(("1" (expand "metric_open?")
(("1" (skosimp)
(("1" (case-replace "ball(x!2, r!1)(x!3)")
(("1"
(assert)
(("1"
(expand "ball")
(("1"
(hide -2)
(("1"
(inst + "r!1-abs(x!2-x!3)")
(("1"
(expand "subset?")
(("1"
(skosimp)
(("1"
(expand "member")
(("1"
(lemma "triangle")
(("1"
(inst
-
"x!2-x!3"
"x!3-x!4")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2"
(replace 1 2)
(("2"
(assert)
(("2"
(hide -1)
(("2"
(skosimp)
(("2"
(expand "subset?")
(("2"
(expand "member")
(("2"
(inst - "x!3")
(("2"
(lemma
"ball_centre"
("x" "x!3" "r" "r!2"))
(("2"
(expand "member")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (typepred "A!1")
(("2" (expand "extend")
(("2" (expand "subset?")
(("2" (expand "member")
(("2" (expand "fullset")
(("2" (expand "metric_induced_topology")
(("2" (expand "metric_open?")
(("2"
(name "VV"
"{X:set[real]| EXISTS (x:real,r:posreal): X=ball(x,r) & subset?[real](X,A!1)}")
(("2" (inst + "VV")
(("2" (split)
(("1" (skosimp)
(("1"
(hide -2)
(("1"
(prop)
(("1"
(expand "VV")
(("1"
(skosimp)
(("1"
(inst + "x!2" "r!1")
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2" (apply-extensionality :hide? t)
(("2"
(hide -1)
(("2"
(expand "Union")
(("2"
(inst - "x!1")
(("2"
(case-replace "A!1(x!1)")
(("1"
(assert)
(("1"
(skosimp)
(("1"
(inst + "ball(x!1,r!1)")
(("1"
(lemma
"ball_centre"
("x" "x!1" "r" "r!1"))
(("1"
(expand "member")
(("1"
(propax)
nil
nil))
nil))
nil)
("2"
(expand "VV")
(("2"
(replace -2)
(("2"
(inst + "x!1" "r!1")
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(assert)
(("2"
(skosimp)
(("2"
(typepred "a!1")
(("2"
(expand "VV")
(("2"
(skosimp)
(("2"
(expand "subset?")
(("2"
(inst - "x!1")
(("2"
(assert)
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)
((metric_induced_topology const-decl "setofsets[T]" metric_space_def
nil)
(member const-decl "bool" sets nil)
(metric_open? const-decl "bool" metric_space_def nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(set type-eq-decl nil sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(ball const-decl "set[T]" metric_space_def nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(r!1 skolem-const-decl "posreal" real_topology nil)
(x!2 skolem-const-decl "real" real_topology nil)
(x!3 skolem-const-decl "real" real_topology nil)
(triangle formula-decl nil real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(ball_centre formula-decl nil metric_space nil)
(extend const-decl "R" extend nil)
(fullset const-decl "set" sets nil)
(subset? const-decl "bool" sets nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(Union const-decl "set" sets nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(r!1 skolem-const-decl "posreal" real_topology nil)
(x!1 skolem-const-decl "real" real_topology nil)
(VV skolem-const-decl "[set[real] -> boolean]" real_topology nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(base? const-decl "bool" basis "topology/"))
shostak))
(rational_open_interval_TCC1 0
(rational_open_interval_TCC1-1 nil 3387600277
("" (inst + "ball(0,1)") (("" (inst + "0" "1") nil nil)) nil)
((ball const-decl "set[T]" metric_space_def nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(posrat nonempty-type-eq-decl nil rationals nil)
(> const-decl "bool" reals nil)
(nonneg_rat nonempty-type-eq-decl nil rationals nil)
(>= const-decl "bool" reals nil)
(rational nonempty-type-from-decl nil rationals nil)
(rat nonempty-type-eq-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_minus_real_is_real application-judgement "real" reals nil))
nil))
(rational_basis 0
(rational_basis-1 nil 3387602054
("" (lemma "open_basis")
(("" (expand "extend")
(("" (expand "base?")
(("" (flatten)
(("" (split)
(("1" (expand "subset?")
(("1" (expand "member")
(("1" (skosimp)
(("1" (prop)
(("1" (skosimp)
(("1" (inst -3 "x!1")
(("1" (prop)
(("1" (expand "fullset")
(("1" (propax) nil nil)) nil)
("2" (inst + "q!1" "pq!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (inst - "A!1")
(("2" (skosimp)
(("2"
(inst +
"{X:set[real] | EXISTS q, pq: X = ball(q, pq) & subset?[real](X,A!1)}")
(("2" (split)
(("1" (expand "subset?")
(("1" (skosimp)
(("1" (expand "member")
(("1" (prop)
(("1"
(expand "fullset")
(("1" (propax) nil nil))
nil)
("2"
(skosimp*)
(("2" (inst + "q!1" "pq!1") nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (apply-extensionality 1 :hide? t)
(("2" (expand "Union")
(("2" (case-replace "A!1(x!1)")
(("1" (replace -4 -1 rl)
(("1"
(assert)
(("1"
(skosimp)
(("1"
(typepred "a!1")
(("1"
(expand "subset?" -4)
(("1"
(expand "member")
(("1"
(inst -4 "a!1")
(("1"
(assert)
(("1"
(prop)
(("1"
(skosimp)
(("1"
(hide -5)
(("1"
(replace -1 -4)
(("1"
(expand
"ball"
-4)
(("1"
(name
"AA"
"ball(x!1,r!1-abs(x!2-x!1))")
(("1"
(case
"subset?[real](AA,a!1)")
(("1"
(name-replace
"R"
"r!1 - abs(x!2 - x!1)")
(("1"
(case
"R>0")
(("1"
(lemma
"density"
("x"
"x!1-R/8"
"y"
"x!1+R/8"))
(("1"
(assert)
(("1"
(skolem
-
("q!1"))
(("1"
(flatten)
(("1"
(lemma
"density"
("x"
"R/4"
"y"
"R/2"))
(("1"
(assert)
(("1"
(skosimp)
(("1"
(case
"ball(q!1,r!2)(x!1)")
(("1"
(case
"subset?[real](ball(q!1, r!2),AA)")
(("1"
(inst
+
"ball(q!1, r!2)")
(("1"
(inst
+
"q!1"
"r!2")
(("1"
(expand
"subset?")
(("1"
(expand
"member")
(("1"
(skosimp)
(("1"
(replace
-15
1
rl)
(("1"
(assert)
(("1"
(hide
-15)
(("1"
(inst
-
"x!3")
(("1"
(assert)
(("1"
(inst
-
"x!3")
(("1"
(inst
+
"a!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil)
("2"
(assert)
nil
nil))
nil)
("2"
(hide
-13
2)
(("2"
(expand
"AA")
(("2"
(expand
"R")
(("2"
(grind)
nil
nil))
nil))
nil))
nil)
("3"
(assert)
nil
nil))
nil)
("2"
(grind)
nil
nil)
("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(expand
"R")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"subset?")
(("2"
(skosimp)
(("2"
(expand
"member")
(("2"
(expand
"AA")
(("2"
(expand
"ball")
(("2"
(replace
-3)
(("2"
(assert)
(("2"
(lemma
"triangle")
(("2"
(inst
-
"x!2-x!1"
"x!1-x!3")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2"
(skosimp)
(("2"
(typepred "a!1")
(("2"
(skosimp)
(("2"
(expand "subset?")
(("2"
(inst - "x!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((extend const-decl "R" extend nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(R skolem-const-decl "real" real_topology nil)
(minus_real_is_real application-judgement "real" reals nil)
(AA skolem-const-decl "set[real]" real_topology nil)
(r!2 skolem-const-decl "rat" real_topology nil)
(q!1 skolem-const-decl "rat" real_topology nil)
(A!1 skolem-const-decl "(metric_induced_topology)" real_topology
nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(density formula-decl nil rational_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(triangle formula-decl nil real_props nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(metric_space_is_hausdorff name-judgement "hausdorff" real_topology
nil)
(metric_space_is_hausdorff? name-judgement "(hausdorff?)"
real_topology nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(Union const-decl "set" sets nil)
(ball const-decl "set[T]" metric_space_def nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(set type-eq-decl nil sets nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(metric_induced_topology const-decl "setofsets[T]" metric_space_def
nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(setofsets type-eq-decl nil sets nil)
(subset? const-decl "bool" sets nil)
(fullset const-decl "set" sets nil)
(posrat nonempty-type-eq-decl nil rationals nil)
(nonneg_rat nonempty-type-eq-decl nil rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(rat nonempty-type-eq-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(member const-decl "bool" sets nil)
(base? const-decl "bool" basis "topology/")
(open_basis formula-decl nil real_topology nil))
shostak))
(countable_rational_open_interval 0
(countable_rational_open_interval-1 nil 3389931575
(""
(lemma "is_countable_cross"
("X" "fullset[rat]" "Y" "fullset[posrat]"))
(("" (lemma "nat_posrat")
(("" (lemma "nat_rational")
(("" (split)
(("1" (hide -2 -3)
(("1" (expand "fullset")
(("1" (expand "cross_product")
(("1" (expand "is_countable")
(("1" (skosimp)
(("1" (typepred "f!1")
(("1"
(name "F"
"lambda (r:rat,pq:posrat): ball(r,pq)")
(("1"
(case "bijective?[[rat, posrat],rational_open_interval](F)")
(("1"
(lemma
"bij_inv_is_bij[[rat, posrat], rational_open_interval]"
("f" "F"))
(("1" (split)
(("1"
(assert)
(("1"
(inst
+
"f!1 o inverse[[rat, posrat], rational_open_interval](F)")
(("1"
(expand "bijective?")
(("1"
(flatten)
(("1"
(hide-all-but (-1 -6 1))
(("1"
(expand "o")
(("1"
(expand "injective?")
(("1"
(skosimp)
(("1"
(inst
-3
"inverse[[rat, posrat], rational_open_interval](F)(x1!1)"
"inverse[[rat, posrat], rational_open_interval](F)(x2!1)")
(("1"
(assert)
(("1"
(inst
-
"x1!1"
"x2!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (propax) nil nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (expand "bijective?")
(("2"
(split)
(("1"
(expand "injective?")
(("1"
(skosimp*)
(("1"
(expand "F")
(("1"
(rewrite
"extensionality_postulate"
-1
:dir
rl)
(("1"
(lemma
"trich_lt"
("x" "x1!1`1" "y" "x2!1`1"))
(("1"
(split)
(("1"
(lemma
"trich_lt"
("x"
"x1!1`2"
"y"
"x2!1`2"))
(("1"
(split)
(("1"
(inst
-
"max(x1!1`1+x1!1`2,x2!1`1)")
(("1"
(expand "ball")
(("1"
(grind)
nil
nil))
nil))
nil)
("2"
(inst
-
"max(x1!1`1+x1!1`2,x2!1`1)")
(("2"
(expand "ball")
(("2"
(grind)
nil
nil))
nil))
nil)
("3"
(expand "ball")
(("3"
(inst
-
"min(x1!1`1-x2!1`2,x1!1`1)")
(("3"
(grind)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(lemma
"trich_lt"
("x"
"x1!1`2"
"y"
"x2!1`2"))
(("2"
(split)
(("1"
(inst
-
"x1!1`1+x1!1`2")
(("1"
(expand "ball")
(("1"
(grind)
nil
nil))
nil))
nil)
("2"
(decompose-equality)
nil
nil)
("3"
(inst
-
"x1!1`1+x2!1`2")
(("3"
(expand "ball")
(("3"
(grind)
nil
nil))
nil))
nil))
nil))
nil)
("3"
(lemma
"trich_lt"
("x"
"x1!1`2"
"y"
"x2!1`2"))
(("3"
(split)
(("1"
(inst
-
"min(x2!1`1-x1!1`2,x2!1`1)")
(("1"
(expand "ball")
(("1"
(grind)
nil
nil))
nil))
nil)
("2"
(inst
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.97 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
