(interval_realsnil 3258223423 3292322828"" (skosimp*)"" (prop)"1" (expand "open_ball?" )"1" (skosimp*)"1" (expand "open_ball" )"1" (expand "subset?" )"1" (expand "member" )"1" (inst + "delta!1" ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (expand "open_ball?" )"2" (skosimp*)"2" (expand "subset?" )"2" (expand "member" )"2" (expand "open_ball" ) (("2" (inst + "r!1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" sets nil )"set[T]" open_sets nil )"bool" open_sets nil ))nil nil ))nil 3258223381 3292322828"" (skosimp*) (("" (expand "open?" ) (("" (inst?) nil nil )) nil ))nil )"bool" open_sets nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" open_sets nil )nil open_sets nil )nil booleans nil )set type-eq-decl nil sets nil ) nil nil )nil 3320064681 3320064682 ("" (skosimp*) nil nil )nil 1331 130 t shostak))nil 3258299476 3292322828"" (skosimp*)"" (expand "open?" )"" (skosimp*)"" (expand "open_ball?" )"" (inst + "min(x!1 -a!1,b!1-x!1)" )"1" (skosimp*) (("1" (grind) nil nil )) nil )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"bool" open_sets nil )"bool" open_sets nil )"{n: nonneg_real | n >= m}" real_defs nil )nil real_types nil )nil real_types nil )nil booleans nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil ) (<= const-decl "bool" reals nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[real -> boolean]" open_sets nil )nil open_sets nil )"bool" reals nil ) nil nil nil "bool" reals nil ))nil 3258299818 3292322829"" (skosimp*)"" (expand "open?" )"" (skosimp*)"" (expand "open_ball?" )"" (inst + "x!1-a!1" )"" (skosimp*) (("" (grind) nil nil )) nil )) nil ))nil ))nil ))nil ))nil )"bool" open_sets nil )"bool" open_sets nil )"{n: nonneg_real | n >= m}" real_defs nil )nil open_sets nil )"[real -> boolean]" open_sets nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil 3258299894 3292322829"" (skosimp*)"" (expand "open?" )"" (skosimp*)"" (expand "open_ball?" )"" (inst + "a!1-x!1" ) (("" (grind) nil nil )) nil )) nil ))nil ))nil ))nil )"bool" open_sets nil )"bool" open_sets nil )"{n: nonneg_real | n >= m}" real_defs nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" reals nil )nil open_sets nil )"[real -> boolean]" open_sets nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil nil ))nil 3258299981 3292322829"" (skosimp*)"" (expand "open?" )"" (skosimp*)"" (expand "open_ball?" )"" (typepred "x!1" )"" (expand "union" )"" (expand "member" )"" (split -2)"1" (hide -4)"1" (inst?)"1" (skosimp*)"1" (inst + "delta!1" )"1" (skosimp*)"1" (inst - "y!1" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (hide -3)"2" (inst?)"2" (skosimp*)"2" (inst + "delta!1" )"2" (skosimp*)"2" (inst - "y!1" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" open_sets nil )"bool" open_sets nil ) nil nil nil nil real_types nil )"bool" reals nil )nil real_types nil )"bool" reals nil )"bool" sets nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" open_sets nil )nil open_sets nil )set type-eq-decl nil sets nil ) (union const-decl "set" sets nil ))nil 3258299631 3292322829"" (skosimp*)"" (expand "closed?" )"" "complement(LAMBDA (x): a!1 <= x AND x <= b!1) = ") "1" (hide -1)"1" (lemma "union_open" )"1" (inst?)"1" (assert )"1" (hide 2)"1" (lemma "above_intv_open " )"1" (inst?)"1" (assert )"1" (lemma "below_intv_open " )"1" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (apply-extensionality 1 :hide? t)"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil )"bool" open_sets nil )"bool" sets nil )nil open_sets nil )nil open_sets nil )nil open_sets nil )"bool" reals nil ) (> const-decl "bool" reals nil )"set" sets nil ) (<= const-decl "bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"set" sets nil )"[T, T -> boolean]" equalities nil )set type-eq-decl nil sets nil )nil booleans nil )nil open_sets nil )"[real -> boolean]" open_sets nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))quality 95%
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
