|
(reals_complete_more
(real_complete2 0
(real_complete2-1 nil 3506273121
("" (skosimp*)
(("" (lemma "real_complete")
(("" (inst -1 "S!1")
(("1" (assert)
(("1" (split -1)
(("1" (skosimp*)
(("1" (inst 1 "y!2")
(("1" (hide -2)
(("1" (expand "extend")
(("1" (expand "least_upper_bound")
(("1" (expand "least_upper_bound?")
(("1" (prop)
(("1" (hide -2)
(("1" (expand "upper_bound")
(("1"
(expand "upper_bound?")
(("1"
(skosimp*)
(("1" (inst?) nil nil))
nil))
nil))
nil))
nil)
("2" (hide -1)
(("2" (skosimp*)
(("2"
(inst -2 "y!3")
(("2"
(assert)
(("2"
(hide 1 2)
(("2"
(expand "upper_bound")
(("2"
(expand "upper_bound?")
(("2"
(skosimp*)
(("2"
(typepred "s!1")
(("2"
(assert)
(("2" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst 1 "y!1")
(("2" (hide 2)
(("2" (expand "upper_bound?")
(("2" (expand "upper_bound")
(("2" (skosimp*)
(("2" (inst?)
(("2" (typepred "s!1")
(("2" (expand "extend")
(("2" (assert) (("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "S!1")
(("2" (hide -2 2) (("2" (grind) nil nil)) nil)) nil))
nil))
nil))
nil)
((real_complete formula-decl nil bounded_real_defs nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(s!1 skolem-const-decl "(extend[real, T, bool, FALSE](S!1))"
reals_complete_more nil)
(S!1 skolem-const-decl "(nonempty?[T])" reals_complete_more nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(least_upper_bound const-decl "bool" bound_defs nil)
(upper_bound const-decl "bool" bound_defs nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(upper_bound? const-decl "bool" bounded_real_defs nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(least_upper_bound? const-decl "bool" bounded_real_defs nil)
(extend const-decl "R" extend nil)
(FALSE const-decl "bool" booleans nil)
(T formal-subtype-decl nil reals_complete_more nil)
(T_pred const-decl "[real -> boolean]" reals_complete_more nil)
(nonempty? const-decl "bool" sets 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)
(nonempty_extend application-judgement "(nonempty?[T])"
extend_set_props nil))
nil))
(real_lower_complete2 0
(real_lower_complete2-1 nil 3506273121
("" (skosimp*)
(("" (lemma "real_lower_complete")
(("" (inst -1 "S!1")
(("1" (split -1)
(("1" (skosimp*)
(("1" (inst 1 "x!1")
(("1" (hide -2)
(("1" (expand "greatest_lower_bound")
(("1" (expand "greatest_lower_bound?")
(("1" (prop)
(("1" (hide -2)
(("1" (expand "lower_bound")
(("1" (expand "lower_bound?")
(("1" (skosimp*)
(("1"
(inst?)
(("1"
(expand "extend")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1)
(("2" (skosimp*)
(("2" (inst -2 "y!2")
(("2" (assert)
(("2"
(hide 1 2)
(("2"
(expand "lower_bound")
(("2"
(expand "lower_bound?")
(("2"
(skosimp*)
(("2"
(inst?)
(("2"
(typepred "s!1")
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (inst?)
(("2" (expand "lower_bound?")
(("2" (expand "lower_bound")
(("2" (skosimp*)
(("2" (inst?)
(("2" (typepred "s!1") (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (typepred "S!1")
(("2" (hide -2) (("2" (grind) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((real_lower_complete formula-decl nil bounded_real_defs nil)
(greatest_lower_bound const-decl "bool" bound_defs nil)
(lower_bound const-decl "bool" bound_defs nil)
(z!1 skolem-const-decl "{x: T | S!1(x)}" reals_complete_more nil)
(S!1 skolem-const-decl "(nonempty?[T])" reals_complete_more nil)
(lower_bound? const-decl "bool" bounded_real_defs nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(s!1 skolem-const-decl "(extend[real, T, bool, FALSE](S!1))"
reals_complete_more nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(greatest_lower_bound? const-decl "bool" bounded_real_defs nil)
(s!1 skolem-const-decl "(extend[real, T, bool, FALSE](S!1))"
reals_complete_more nil)
(extend const-decl "R" extend nil)
(FALSE const-decl "bool" booleans nil)
(T formal-subtype-decl nil reals_complete_more nil)
(T_pred const-decl "[real -> boolean]" reals_complete_more nil)
(nonempty? const-decl "bool" sets 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)
(nonempty_extend application-judgement "(nonempty?[T])"
extend_set_props nil))
nil)))
¤ Dauer der Verarbeitung: 0.33 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.
|
