Impressum real_intervals_aux.prf
Sprache: Lisp
(real_intervals_auxnil 3471584778"" (skosimp)"" (split)"1" (flatten)"1" (expand "bounded_open_interval?" )"1" (expand "bounded_interval?" )"1" (expand "bounded?" )"1" (flatten)"1" (split -2)"1" (propax) nil nil )"2" (flatten)"2" (expand "empty?" )"2" (skosimp)"2" (expand "member" )"2" (name "LO" "inf(A!1)" )"1" (name "HI" "sup(A!1)" )"1" "sup(A!1)" )"1" "inf(A!1)" )"1" replace -3)"1" replace -4)"1" expand "least_upper_bound" )"1" expand "greatest_lower_bound" )"1" "1" expand "lower_bound" )"1" expand "upper_bound" )"1" "1" case "LO<HI" )"1" "(HI+LO)/2" "(HI-LO)/2" )"1" "1" "A!1(x!2)" )"1" "1" expand "metric_open?" )"1" "x!2" )"1" assert )"1" "1" expand "subset?" )"1" "x!2-r!1/2" )"1" "x!2+r!1/2" )"1" assert )"1" "1" "1" "x!2 - r!1 / 2" )"1" "r!1 / 2 + x!2" )"1" "1" nil nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "ball" )"2" case "LO<x!2 & x!2<HI" )"1" "1" "1" "x!2" )"1" assert )"1" "1" "z!1" )"1" case "z!1<x!2" )"1" "1" "x!2" )"1" assert )"1" "1" case "x!2<z!2" )"1" "1" "z!2" )"1" expand "interval?" )"1" "z!1" "z!2" "x!2" )"1" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" "2" expand "metric_open?" )"2" "x!1" )"2" assert )"2" "2" expand "subset?" )"2" "x!1+r!1/2" )"2" assert )"2" "1" "x!1" )"1" "x!1+r!1/2" )"1" assert )nil nil ))nil ))nil )"2" "2" 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 ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (expand "bounded_open_interval?" )"2" (expand "bounded_interval?" )"2" (expand "bounded?" )"2" (split -1)"1" (assert )"1" (rewrite "emptyset_is_empty?" )"1" (replace -1)"1" (hide -1)"1" (split)"1" (grind) nil nil )"2" (expand "metric_open?" )"2" (expand "emptyset" )"2" expand "subset?" )"2" expand "member" )"2" "2" "2" "x!1" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (split)"1" (replace -1)"1" (hide -1) (("1" (grind) nil nil )) nil ))nil )"2" (replace -1)"2" (hide -1)"2" (flatten)"2" (expand "nonempty?" )"2" (assert )"2" "1" expand "above_bounded" )"1" "x!1+r!1" )"1" (grind) nil nil ))nil ))nil )"2" expand "below_bounded" )"2" "x!1-r!1" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (replace -1)"3" (hide -1)"3" "metric_open_ball" "x" "x!1" "r" "r!1" ))"3" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" real_topology"metric_space/" )"bool" real_topology "metric_space/" )"bool" sets nil )"bool" sets nil )"bool" bounded_reals "reals/" )nil bounded_reals "reals/" )"bool" bound_defs "reals/" )"{x | least_upper_bound(<=)(x, Su)}" bounded_reals"reals/" )"bool" bound_defs "reals/" )"posreal" real_intervals_aux nil )"real" real_intervals_aux nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"(total_order?[real])" nil )"real" reals nil )"bool" reals nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"set[real]" real_intervals_aux nil )"{x | least_upper_bound[real, real](<=)(x, A!1)}" nil )"{x | greatest_lower_bound[real, real](<=)(x, A!1)}" nil )"bool" reals nil )nil real_types nil )nil real_types nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" metric_space_def "metric_space/" )"bool" sets nil )"real" real_intervals_aux nil )"posreal" real_intervals_aux nil )"(total_order?[real])" nil )"nzreal" real_typesnil )"nzreal" nil )"posreal" nil )"real" reals nil )"bool" real_topology "metric_space/" )"real" reals nil )"(strict_total_order?[real])" real_props nil )"set[T]" metric_space_def "metric_space/" )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )"bool" reals nil )"bool" bound_defs "reals/" )NOT const-decl "[bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil numbers nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" sets nil )nil defined_types nil )"bool" bounded_reals "reals/" )nil bounded_reals "reals/" )nil defined_types nil )"bool" bound_defs "reals/" )"bool" reals nil )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )"bool" real_topology "metric_space/" )nil metric_space "metric_space/" )"set" sets nil )"finite_set" finite_sets nil )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set[T]" countable_props"sets_aux/" )"clopen[real, (metric_induced_topology)]" real_topology"metric_space/" )"compact[real, (metric_induced_topology)]" real_topology"metric_space/" )nil sets_lemmas nil ))nil 3471587044"" (skosimp)"" (expand "unbounded?" )"" (split)"1" (flatten)"1" (expand "bounded?" )"1" (flatten)"1" (expand "nonempty?" )"1" (assert )"1" (case-replace "above_bounded[real](A!1)" )"1" (hide 4 3)"1" (typepred "sup(A!1)" )"1" (name-replace "HI" "sup(A!1)" )"1" (expand "least_upper_bound" )"1" (flatten)"1" expand "upper_bound" )"1" "HI" )"1" "1" expand "inf_open" )"1" "A!1(x!1)" )"1" expand "open_interval?" )"1" "1" expand "metric_open?" )"1" "x!1" )"1" assert )"1" "1" expand "subset?" )"1" "x!1+r!1/2" )"1" "1" assert )"1" "r!1 / 2 + x!1" )"1" assert )nil nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "x!1" )"2" assert )"2" "2" case "x!1<z!1" )"1" "z!1" )"1" "1" expand "below_bounded" )"1" "x!1" )"1" expand "lower_bound" )"1" "1" case "z!2<x!1" )"1" "1" expand "open_interval?" )"1" "1" expand "interval?" )"1" "z!2" "z!1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )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 )"2" (expand "nonempty?" )"2" (propax) nil nil )) nil ))nil ))nil )"2" (case-replace "below_bounded[real](A!1)" )"1" (hide 3 6 4)"1" (typepred "inf(A!1)" )"1" (name-replace "LO" "inf(A!1)" )"1" (inst + "LO" )"1" expand "open_inf" )"1" expand "greatest_lower_bound" )"1" expand "lower_bound" )"1" "1" "A!1(x!1)" )"1" "1" expand "open_interval?" )"1" "1" expand "metric_open?" )"1" "x!1" )"1" assert )"1" "1" expand "subset?" )"1" "x!1-r!1/2" )"1" "1" expand "member" )"1" "x!1 - r!1 / 2" )"1" assert )"1" "1" "r!1" )"1" expand "<=" "1" "1" assert )"1" "reals.<" )"1" expand "strict_total_order?" )"1" expand "strict_order?" )"1" "1" expand "transitive?" )"1" "LO" "x!1 - r!1 / 2" "x!1" )"1" "1" nil nil )"2" nil nil )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" "x!1" )"2" assert )"2" "2" "z!1" )"2" case "z!1<x!1" )"1" "1" expand "above_bounded" )"1" "x!1" )"1" expand "upper_bound" )"1" "1" case "x!1<z!2" )"1" "z!2" )"1" expand "open_interval?" )"1" "1" expand "interval?" )"1" "z!1" "z!2" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )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" (expand "nonempty?" )"2" (propax) nil nil )) nil ))nil ))nil )"2" (hide 4 6 7)"2" (apply-extensionality 4 :hide? t)"2" (expand "fullset" )"2" (expand "open_interval?" )"2" "2" expand "below_bounded" )"2" "x!1" )"2" expand "above_bounded" )"2" "x!1" )"2" expand "upper_bound" )"2" expand "lower_bound" )"2" "2" case "z!1<x!1" )"1" case "x!1<z!2" )"1" expand "interval?" )"1" "z!1" "z!2" "x!1" )"1" assert )nil nil ))nil ))nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (split)"1" (replace -1)"1" (hide -1)"1" (split)"1" (expand "bounded?" )"1" (split)"1" (grind) nil nil )"2" (flatten)"2" (expand "above_bounded" )"2" (skosimp)"2" (expand "upper_bound" )"2" "n!1+1" )"1" (assert ) nil nil )"2" expand "fullset" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "open_interval?" )"2" (split)"1" (grind) nil nil )"2" (expand "metric_open?" )"2" (expand "fullset" )"2" (expand "subset?" )"2" (expand "member" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp)"2" (replace -1)"2" (hide -1)"2" (split)"1" (expand "bounded?" )"1" (split)"1" (expand "open_inf" )"1" (expand "empty?" )"1" (expand "member" )"1" "a!1+1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil )"2" (flatten)"2" (expand "open_inf" )"2" (expand "above_bounded" )"2" "2" expand "upper_bound" )"2" "max(a!1+1,n!1+1)" )"1" (grind) nil nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "open_inf" )"2" (expand "open_interval?" )"2" (split)"1" (grind) nil nil )"2" (expand "metric_open?" )"2" (skosimp)"2" expand "subset?" )"2" expand "member" )"2" "a!1<x!1" )"1" assert )"1" "x!1-a!1" )"1" "1" (grind) nil nil ))nil ))nil ))nil )"2" assert )"2" "2" "x!1" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (skosimp)"3" (replace -1)"3" (hide -1)"3" (assert )"3" (split)"1" (expand "inf_open" )"1" (expand "bounded?" )"1" (split)"1" (expand "empty?" )"1" expand "member" )"1" "a!1-1" )"1" (assert ) nil nil ))nil ))nil ))nil )"2" (flatten)"2" expand "below_bounded" )"2" "2" expand "lower_bound" )"2" "min(n!1-1,a!1-1)" )"1" (grind) nil nil )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "open_interval?" )"2" (split)"1" (grind) nil nil )"2" (expand "inf_open" )"2" (expand "metric_open?" )"2" "2" "x!1 < a!1" )"1" assert )"1" expand "subset?" )"1" expand "member" )"1" "a!1-x!1" )"1" "1" (grind) nil nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" "2" expand "subset?" )"2" expand "member" )"2" "x!1" )"2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" real_topology "metric_space/" )"real" real_intervals_aux nil )"real" real_intervals_aux nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"real" reals nil )"real" real_intervals_aux nil )max const-decl "{p: real | p >= m AND p >= n}" real_defs nil )"real" real_intervals_aux nil )"bool" sets nil )"real" real_intervals_aux nil )"metric_complete" real_topology"metric_space/" )"clopen[real, (metric_induced_topology)]" real_topology"metric_space/" )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )nil bounded_reals "reals/" )"bool" bound_defs "reals/" )"bool" orders nil )"bool" orders nil )"bool" relations nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"posreal" real_intervals_aux nil )"real" real_intervals_aux nil )"set[real]" real_intervals_aux nil )"open" real_topology "metric_space/" )"set" sets nil )"[T, T -> boolean]" equalities nil )"bool" reals nil )"bool" real_topology "metric_space/" )"bool" bound_defs "reals/" )"bool" bounded_reals "reals/" )"bool" real_intervals_aux nil )"bool" metric_space_def "metric_space/" )"(strict_total_order?[real])" real_props nil )"bool" sets nil )"(total_order?[real])" nil )"bool" sets nil )"posreal" nil )"real" reals nil )"set[T]" metric_space_def "metric_space/" )"nzreal" real_typesnil )"nzreal" nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"bool" reals nil )nil real_types nil )"real" reals nil )nil sets nil )"bool" reals nil )nil real_types nil )nil number_fields nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield, numfield -> numfield]" number_fields nil )"setofsets[T]" metric_space_def"metric_space/" )"bool" topology "topology/" )nil topology "topology/" )"open" real_topology "metric_space/" )"bool" bound_defs "reals/" )AND const-decl "[bool, bool -> bool]" booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil defined_types nil )"bool" bound_defs "reals/" )"bool" reals nil )nil bounded_reals "reals/" )"{x | least_upper_bound(<=)(x, Su)}" bounded_reals"reals/" )set type-eq-decl nil sets nil )"bool" bounded_reals "reals/" )nil defined_types 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 )"bool" sets nil )"bool" real_topology "metric_space/" ))nil 3453781861 ("" (subtype-tcc) nil 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 )set type-eq-decl nil sets nil )"bool" real_topology "metric_space/" )nil real_topology"metric_space/" )"bool" real_topology "metric_space/" )"bool" bound_defs "reals/" )"bool" bounded_reals "reals/" )"bool" real_topology "metric_space/" )"bool" sets nil )"bool" sets nil )"bool" sets nil )"bool" bound_defs "reals/" )"bool" bounded_reals "reals/" ))nil ))nil 3453781861 ("" (subtype-tcc) nil 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 )set type-eq-decl nil sets nil )"bool" real_topology "metric_space/" )nil real_topology"metric_space/" )"bool" real_topology "metric_space/" )"bool" bound_defs "reals/" )"bool" bounded_reals "reals/" )"bool" real_topology "metric_space/" )"bool" sets nil )"bool" sets nil )"bool" sets nil )"bool" bound_defs "reals/" )"bool" bounded_reals "reals/" ))nil ))nil 3453781861"" (skosimp)"" (typepred "b!1" )"" (expand "bounded_interval?" )"" (flatten)"" (expand "bounded?" )"" (replace 1 -2)"" (flatten)"" (expand "empty?" )"" (skosimp)"" (expand "member" )"" (typepred "inf[real](b!1)" )"" (typepred "sup[real](b!1)" )"" (name-replace "INF" "inf[real](b!1)" )"" (name-replace "SUP" "sup[real](b!1)" )"" expand "least_upper_bound" )"" expand "greatest_lower_bound" )"" expand "upper_bound" )"" expand "lower_bound" )"" "" "x!1" )"" "x!1" )"" "" (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 real_topology"metric_space/" )"bool" real_topology "metric_space/" )set type-eq-decl nil sets nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" sets nil )"bool" sets nil )"bool" bound_defs "reals/" )"bool" bounded_reals "reals/" )nil bounded_reals "reals/" )"{x | least_upper_bound(<=)(x, Su)}" bounded_reals"reals/" )"odd_int" integers nil )"bool" bound_defs "reals/" )"bounded_interval" real_intervals_aux nil )"real" real_intervals_aux nil )"(total_order?[real])" nil )"(total_order?[real])" nil )"real" reals nil )"bool" bound_defs "reals/" )"[T, T -> boolean]" equalities nil )nil defined_types nil )"bool" bound_defs "reals/" )"bool" reals nil )"bool" sets nil )nil defined_types nil )"bool" bounded_reals "reals/" )nil bounded_reals "reals/" )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )"bool" real_topology "metric_space/" ))nil ))nil 3453781861 ("" (subtype-tcc) nil 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 )set type-eq-decl nil sets nil )"bool" real_topology "metric_space/" )nil real_topology"metric_space/" )"bool" real_topology "metric_space/" )"bool" bound_defs "reals/" )"bool" bounded_reals "reals/" )"bool" real_topology "metric_space/" )"bool" sets nil )"bool" sets nil )"bool" sets nil )"bool" bound_defs "reals/" )"bool" bounded_reals "reals/" ))nil ))nil 3453781861 ("" (subtype-tcc) nil 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 )set type-eq-decl nil sets nil )"bool" real_topology "metric_space/" )nil real_topology"metric_space/" )"real" real_intervals_aux nil )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )"bool" reals nil )"bool" bound_defs "reals/" )nil defined_types nil )nil bounded_reals "reals/" )nil defined_types nil )"bounded_interval" real_intervals_aux nil )"bool" real_topology "metric_space/" )"bool" bounded_reals "reals/" )"bool" bound_defs "reals/" )"bool" real_topology "metric_space/" )"(total_order?[real])" nil )"bool" sets nil )"bool" sets nil )"bool" sets nil )"bool" bound_defs "reals/" )"bool" bounded_reals "reals/" ))nil ))nil 3453781861"" (skosimp)"" (expand "bounded_interval?" )"" (expand "bounded?" )"" (split)"1" (grind) nil nil )"2" (flatten)"2" (expand "nonempty?" )"2" (typepred "b!1" )"2" (expand "bounded_interval?" )"2" (expand "bounded?" )"2" (replace 3)"2" (flatten)"2" (replace 1)"2" (hide 1 3)"2" (split)"1" "sup(b!1)" )"1" expand "least_upper_bound" )"1" "1" expand "above_bounded" )"1" "sup(b!1)" )"1" expand "upper_bound" )"1" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" "inf(b!1)" )"1" expand "greatest_lower_bound" )"1" "1" expand "below_bounded" )"1" "inf(b!1)" )"1" expand "lower_bound" )"1" (propax) 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 ))nil )"bool" real_topology "metric_space/" )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 )"bool" reals nil ) (set type-eq-decl nil sets nil )nil defined_types nil )"bool" bounded_reals "reals/" )nil bounded_reals "reals/" )nil defined_types nil )"bool" bound_defs "reals/" )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )nil real_topology"metric_space/" )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" bounded_reals "reals/" )nil bounded_reals "reals/" )"bool" bound_defs "reals/" )"{x | least_upper_bound(<=)(x, Su)}" bounded_reals"reals/" )"(total_order?[real])" nil )"bool" real_topology "metric_space/" )"bool" sets nil )"bool" sets nil )"bool" sets nil )"bool" bound_defs "reals/" )"bool" bound_defs "reals/" )"bool" real_topology "metric_space/" ))nil ))nil 3453784437"" (skosimp)"" (expand "length" 1 1)"" (copy -1)"" (expand "nonempty?" -1)"" (replace 1)"" (typepred "b!1" )"" (expand "bounded_interval?" )"" (flatten)"" (expand "bounded?" )"" (replace 1)"" (flatten)"" (hide -5)"" (typepred "inf(b!1)" )"" (name-replace "INF" "inf(b!1)" )"" "sup(b!1)" )"" "SUP" "sup(b!1)" )"" expand "length" )"" "empty?[real]({x | INF <= x AND x <= SUP})" )"1" expand "empty?" )"1" "INF" )"1" expand "member" )"1" expand "least_upper_bound" )"1" expand "greatest_lower_bound" )"1" "1" expand "lower_bound" )"1" expand "upper_bound" )"1" "1" "x!1" )"1" "x!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace 1)"2" "sup({x | INF <= x AND x <= SUP})" )"1" "SUP2" "sup({x | INF <= x AND x <= SUP})" )"1" "inf({x | INF <= x AND x <= SUP})" )"1" "INF2" "inf({x | INF <= x AND x <= SUP})" )"1" "1" expand "greatest_lower_bound" )"1" expand "least_upper_bound" )"1" "1" expand "lower_bound" )"1" expand "upper_bound" )"1" "INF2=INF" )"1" "SUP2=SUP" )"1" "SUP" )"1" "SUP" )"1" assert )nil nil ))nil )"2" expand "empty?" "2" "2" expand "member" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "INF" )"1" "INF" )"1" assert )nil nil ))nil )"2" expand "empty?" "2" "2" expand "member" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" assert )"2" expand "below_bounded" )"2" "INF" )"2" expand "lower_bound" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" assert )"2" expand "above_bounded" )"2" "SUP" )"2" expand "upper_bound" )"2" 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 )"nnreal" real_intervals_aux nil )"bool" sets nil )nil real_topology"metric_space/" )"bool" real_topology "metric_space/" )set type-eq-decl nil sets nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"[T, T -> boolean]" equalities nil )"odd_int" integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" sets nil )"bool" bound_defs "reals/" )"bounded_interval" real_intervals_aux nil )"real" real_intervals_aux nil )"(total_order?[real])" nil )"bool" bound_defs "reals/" )"bool" sets nil )"{x | greatest_lower_bound[real, real](<=)(x, b!1)}" nil )"{x | least_upper_bound[real, real](<=)(x, b!1)}" nil )"real" reals nil )"{x | least_upper_bound(<=)(x, Su)}" bounded_reals"reals/" )nil bounded_reals "reals/" )"bool" bounded_reals "reals/" )"bool" bound_defs "reals/" )nil defined_types nil )"bool" bound_defs "reals/" )"bool" reals nil )nil defined_types nil )"bool" bounded_reals "reals/" )nil bounded_reals "reals/" )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )"bool" real_topology "metric_space/" ))nil 3453781861 ("" (subtype-tcc) nil 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 )set type-eq-decl nil sets nil )"bool" real_topology "metric_space/" )nil real_topology"metric_space/" )"bounded_interval" real_intervals_aux nil )"real" real_intervals_aux nil )"bool" real_topology "metric_space/" )"bool" bounded_reals "reals/" )"bool" bound_defs "reals/" )"bool" real_topology "metric_space/" )"(strict_total_order?[real])" real_props nil )"bool" sets nil )"bool" sets nil )"bool" sets nil )"bool" bound_defs "reals/" )"bool" bounded_reals "reals/" ))nil ))nil 3453781861"" (skosimp)"" (typepred "b!1" )"" (expand "bounded_interval?" )"" (flatten)"" (split)"1" (expand "interval?" )"1" (skosimp)"1" (typepred "x!1" )"1" (typepred "y!1" ) (("1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (expand "bounded?" )"2" (flatten)"2" (expand "nonempty?" 2)"2" (assert )"2" (expand "empty?" 1)"2" (skosimp)"2" (expand "member" )"2" (flatten)"2" (split -4)"1" expand "nonempty?" )"1" (propax) nil nil ))nil )"2" "2" "inf[real](b!1)" )"2" "sup[real](b!1)" )"2" "INF" "inf[real](b!1)" )"2" "SUP" "sup[real](b!1)" )"2" expand "least_upper_bound" )"2" expand "greatest_lower_bound" )"2" "2" expand "upper_bound" )"2" expand "lower_bound" )"2" "x!1" )"2" assert )"2" "2" case "z!1<x!1" )"1" "1" "z!1" )"1" "x!1" )"1" assert )"1" "1" case "x!1<z!2" )"1" "z!2" )"1" "1" "1" "1" expand "above_bounded" )"1" "SUP" )"1" expand "upper_bound" )"1" nil nil ))nil ))nil ))nil )"2" expand "below_bounded" )"2" "INF" )"2" expand "lower_bound" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil real_topology"metric_space/" )"bool" real_topology "metric_space/" )set type-eq-decl nil sets nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" real_topology "metric_space/" )"bool" sets nil )"bool" sets nil )"[T, T -> boolean]" equalities nil )"bool" bound_defs "reals/" )"bool" bound_defs "reals/" )"bool" real_topology "metric_space/" )"{x | least_upper_bound(<=)(x, Su)}" bounded_reals"reals/" )"bool" bound_defs "reals/" )nil bounded_reals "reals/" )"bool" bounded_reals "reals/" )AND const-decl "[bool, bool -> bool]" booleans nil )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )"bool" reals nil )"bool" bound_defs "reals/" )nil defined_types nil )nil bounded_reals "reals/" )"bool" bounded_reals "reals/" )nil defined_types nil )"bool" sets nil )"bool" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3453786603"" (skosimp)"" (expand "length" )"" (typepred "b!1" )"" (expand "bounded_interval?" )"" (expand "bounded?" )"" (flatten)"" (replace -3)"" (split -2)"1" (expand "nonempty?" ) (("1" (propax) nil nil ))nil )"2" (flatten)"2" (case-replace "empty?[real](b!1)" )"1" (expand "nonempty?" )"1" (propax) nil nil )) nil )"2" (replace 1)"2" (hide 1)"2" (typepred "sup(b!1)" )"2" (name-replace "BB" "sup(b!1)" )"2" "inf(b!1)" )"2" "AA" "inf(b!1)" )"2" case "AA<=BB" )"1" expand "<=" -1)"1" "1" case "nonempty?[real]({x | AA < x AND x < BB})" )"1" "1" expand "nonempty?" -1)"1" replace 1)"1" "1" case "below_bounded[real]({x | AA < x AND x < BB})" )"1" case "above_bounded[real]({x | AA < x AND x < BB})" )"1" "inf({x | AA < x AND x < BB})" )"1" "INF" "inf({x | AA < x AND x < BB})" )"1" "INF=AA" )"1" "1" "sup({x | AA < x AND x < BB})" )"1" "SUP" "sup({x | AA < x AND x < BB})" )"1" expand "least_upper_bound" )"1" expand "upper_bound" )"1" "1" "SUP=BB" )"1" "1" "BB" )"1" "1" expand "<=" "1" "1" "(AA+BB)/2" )"1" "(SUP+BB)/2" )"1" assert )nil nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil )"2" nil nil ))nil ))nil )"2" nil nil )"3" "3" "z!1" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil )"2" "2" expand "greatest_lower_bound" )"2" expand "lower_bound" )"2" "2" "(AA+BB)/2" )"1" "AA" )"1" "1" expand "<=" "1" "1" "(INF+AA)/2" )"1" assert )nil nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil ))nil )"2" nil nil )"3" "3" "z!1" )"3" assert )nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil )"2" expand "above_bounded" )"2" "BB" )"2" expand "upper_bound" )"2" nil nil ))nil ))nil ))nil ))nil )"2" expand "below_bounded" )"2" "AA" )"2" expand "lower_bound" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" replace -1)"2" expand "empty?" )"2" "(AA+BB)/2" )"2" assert )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "empty?[real]({x | AA < x AND x < BB})" )"1" (assert ) nil nil )"2" replace 1)"2" "2" expand "empty?" )"2" "2" expand "member" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "nonempty?" )"2" expand "empty?" )"2" "2" expand "member" )"2" expand "greatest_lower_bound" )"2" expand "least_upper_bound" )"2" expand "lower_bound" )"2" expand "upper_bound" )"2" "2" "x!1" )"2" "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 ))nil ))nil ))nil )"nnreal" real_intervals_aux nil )"bool" sets nil )"bool" sets nil )"[T, T -> boolean]" equalities nil )"odd_int" integers nil )"real" real_intervals_aux nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"bool" bound_defs "reals/" )"{x_1 | greatest_lower_bound[real, real](<=)(x_1, {x | AA < x AND x < BB})}" nil )"real" reals nil )"bool" bound_defs "reals/" )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"bounded_interval" real_intervals_aux nil )"{x | greatest_lower_bound[real, real](<=)(x, b!1)}" nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"{x | least_upper_bound[real, real](<=)(x, b!1)}" nil )"(total_order?[real])" nil )"{x_1 | least_upper_bound[real, real](<=)(x_1, {x | AA < x AND x < BB})}" nil )"bool" sets nil )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )nil bounded_reals "reals/" )"bool" bounded_reals "reals/" )"bool" bound_defs "reals/" )nil defined_types nil )"bool" bound_defs "reals/" )"bool" reals nil )nil defined_types nil )"bool" bounded_reals "reals/" )nil bounded_reals "reals/" )"{x | least_upper_bound(<=)(x, Su)}" bounded_reals"reals/" )"bool" real_topology "metric_space/" )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 )set type-eq-decl nil sets nil )"bool" real_topology "metric_space/" )nil real_topology"metric_space/" ))nil 3471444041 ("" (subtype-tcc) nil nil )set type-eq-decl nil sets nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"set" sets nil )"bool" real_topology "metric_space/" )"bool" sets nil )"bool" sets nil )"bool" sets nil )"bool" bound_defs "reals/" )"bool" bounded_reals "reals/" )"bool" bound_defs "reals/" )"bool" bounded_reals "reals/" )"bool" real_topology "metric_space/" )"bool" real_topology "metric_space/" )"finite_set" finite_sets nil )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set[T]" countable_props"sets_aux/" )"clopen[real, (metric_induced_topology)]" real_topology"metric_space/" )"compact[real, (metric_induced_topology)]" real_topology"metric_space/" ))nil ))nil 3453783100"" (expand "length" ) (("" (rewrite "emptyset_is_empty?" ) nil nil ))nil )nil sets_lemmas nil )nil booleans nil )set type-eq-decl nil sets nil )"set" sets nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"nnreal" real_intervals_aux nil )"compact[real, (metric_induced_topology)]" real_topology"metric_space/" )"clopen[real, (metric_induced_topology)]" real_topology"metric_space/" )"finite_set[T]" countable_props"sets_aux/" )"finite_set[T]" countable_setofsets"sets_aux/" )"finite_set" finite_sets nil ))nil 3453781861"" (skosimp)"" (expand "bounded_interval?" )"" (split)"1" (grind) nil nil )"2" (expand "bounded?" )"2" (flatten)"2" (expand "nonempty?" )"2" (assert )"2" (hide 1)"2" (split)"1" (expand "above_bounded" )"1" (inst + "b!1" ) (("1" (grind) nil nil ))nil ))nil )"2" (expand "below_bounded" )"2" (inst + "a!1" ) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" real_topology "metric_space/" )"bool" real_topology "metric_space/" )"bool" sets nil )"bool" bounded_reals "reals/" )"bool" bound_defs "reals/" )"bool" bounded_reals "reals/" )"bool" bound_defs "reals/" )"bool" real_topology "metric_space/" )"(total_order?[real])" nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3453783130"" (skosimp)"" (typepred "b!1" )"" (expand "length" )"" (case "nonempty?[real]({x | a!1 <= x AND x <= b!1})" )"1" (copy -1)"1" (expand "nonempty?" -1)"1" (replace 1 2)"1" case "above_bounded[real]({x | a!1 <= x AND x <= b!1})" )"1" case "below_bounded[real]({x | a!1 <= x AND x <= b!1})" )"1" (typepred "inf({x | a!1 <= x AND x <= b!1})" )"1" "INF" "inf({x | a!1 <= x AND x <= b!1})" )"1" (case-replace "INF=a!1" )"1" "sup({x | a!1 <= x AND x <= b!1})" )"1" "SUP" "sup({x | a!1 <= x AND x <= b!1})" )"1" "SUP=b!1" )"1" expand "least_upper_bound" )"1" "1" expand "upper_bound" )"1" "1" "b!1" )"1" "b!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (hide-all-but (-1 -5 2 1))"2" (expand "greatest_lower_bound" )"2" expand "lower_bound" )"2" "2" "a!1" )"2" "a!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (expand "below_bounded" )"2" (inst + "a!1" )"2" (expand "lower_bound" )"2" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (expand "above_bounded" )"2" (inst + "b!1" )"2" (expand "upper_bound" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (inst - "a!1" ) (("2" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" sets nil )set type-eq-decl nil sets nil )nil defined_types nil )"bool" bounded_reals "reals/" )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )nil bounded_reals "reals/" )"bool" bound_defs "reals/" )nil defined_types nil )"real" reals nil )"odd_int" integers nil )"bool" bound_defs "reals/" )"(total_order?[real])" nil )"{x | least_upper_bound(<=)(x, Su)}" bounded_reals"reals/" )nil bounded_reals "reals/" )"bool" bound_defs "reals/" )"bool" bound_defs "reals/" )"[T, T -> boolean]" equalities nil )"bool" bounded_reals "reals/" )"bool" sets nil )"bool" sets nil )"nnreal" real_intervals_aux nil ))nil 3453781861"" (skosimp)"" (expand "bounded_interval?" )"" (split)"1" (grind) nil nil )"2" (expand "bounded?" )"2" (expand "nonempty?" )"2" (flatten)"2" (assert )"2" (hide 1)"2" (split)"1" (expand "above_bounded" )"1" (inst + "b!1" )"1" (expand "upper_bound" )"1" (propax) nil nil )) nil ))nil ))nil )"2" (expand "below_bounded" )"2" (inst + "a!1" ) (("2" (grind) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" real_topology "metric_space/" )"bool" real_topology "metric_space/" )"bool" bounded_reals "reals/" )"bool" bound_defs "reals/" )"bool" bounded_reals "reals/" )"bool" bound_defs "reals/" )"bool" sets nil )"bool" real_topology "metric_space/" )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3453785868"" (skosimp)"" (typepred "b!1" )"" (expand "<=" -1)"" (split)"1" (expand "length" )"1" (case "nonempty?[real]({x | a!1 < x AND x < b!1})" )"1" (copy -1)"1" (expand "nonempty?" -1)"1" (replace 1 2)"1" case "above_bounded({x | a!1 < x AND x < b!1})" )"1" case "below_bounded({x | a!1 < x AND x < b!1})" )"1" "inf({x | a!1 < x AND x < b!1})" )"1" "INF" "inf({x | a!1 < x AND x < b!1})" )"1" (case-replace "INF=a!1" )"1" "1" "sup({x | a!1 < x AND x < b!1})" )"1" "SUP" "sup({x | a!1 < x AND x < b!1})" )"1" "SUP=b!1" )"1" "1" expand "least_upper_bound" )"1" "1" expand "upper_bound" )"1" "b!1" )"1" "1" expand "<=" -1)"1" "1" "(a!1+b!1)/2" )"1" "(SUP+b!1)/2" )"1" assert )nil nil )"2" assert )nil nil ))nil )"2" assert )nil nil ))nil )"2" nil nil ))nil ))nil )"2" nil nil )"3" "3" "z!1" )"3" "z!1" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" expand "greatest_lower_bound" )"2" "2" expand "lower_bound" )"2" "a!1" )"2" replace 1 -2)"2" "1" expand "<=" -1)"1" "1" "(min(INF,b!1)+a!1)/2" )"1" (assert ) nil nil )"2" assert )"2" expand "min" )"2" "2" assert )nil nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" "2" "z!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" (expand "below_bounded" )"2" (inst + "a!1" )"2" (expand "lower_bound" )"2" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (expand "above_bounded" )"2" (inst + "b!1" )"2" (expand "upper_bound" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (inst - "(a!1+b!1)/2" )"2" (grind) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "length" )"2" "empty?[real]({x | a!1 < x AND x < b!1})" )"1" (assert ) nil nil )"2" (hide 2)"2" (expand "empty?" )"2" (skosimp)"2" (expand "member" )"2" (flatten) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" reals nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" sets nil )set type-eq-decl nil sets nil )nil defined_types nil )"bool" bounded_reals "reals/" )"{x | greatest_lower_bound(<=)(x, Sl)}" "reals/" )nil bounded_reals "reals/" )"bool" bound_defs "reals/" )nil defined_types nil )"bool" bound_defs "reals/" )nil bounded_reals "reals/" )"{x | least_upper_bound(<=)(x, Su)}" bounded_reals"reals/" )"bool" bound_defs "reals/" )"{x_1 | least_upper_bound[real, real](<=)(x_1, {x | a!1 < x AND x < b!1})}" nil )"(total_order?[real])" nil )"{x | a!1 <= x}" real_intervals_aux nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )nil number_fields nil )"real" real_intervals_aux nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil )"odd_int" integers nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"{x_1 | greatest_lower_bound[real, real](<=)(x_1, {x | a!1 < x AND x < b!1})}" nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"bool" bound_defs "reals/" )"[T, T -> boolean]" equalities nil )"bool" bounded_reals "reals/" )"bool" sets nil )"bool" sets nil )"nnreal" real_intervals_aux nil ))nil 3472290274"" (expand "left_closed_right_open_interval?" )"" (expand "fullset" )"" (split)"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (inst - "0" ) (("1" (assert ) nil nil )) nil )) nil ))nil )"2" (expand "interval?" ) (("2" (propax) nil nil )) nil )"3" (expand "above_bounded" )"3" (skosimp)"3" (expand "upper_bound" )"3" (inst - "n!1+1" ) (("3" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"set" sets nil )"bool" bounded_reals "reals/" )"bool" bound_defs "reals/" )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"bool" booleans nil )nil booleans nil )"real" reals nil )"bool" real_topology "metric_space/" )"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 )"bool" sets nil )"bool" sets nil )"bool" nil )"metric_complete" real_topology"metric_space/" )"clopen[real, (metric_induced_topology)]" real_topology"metric_space/" ))nil ))nil 3472290132"" (expand "fullset" )"" (expand "nonempty_interval?" )"" (split)"1" (expand "nonempty?" )"1" (expand "empty?" )"1" (inst - "0" ) (("1" (assert ) nil nil )) nil )) nil ))nil )"2" (expand "interval?" ) (("2" (propax) nil nil )) nil ))nil ))nil ))nil )"bool" real_intervals_aux nil )"bool" real_topology "metric_space/" )"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 )"bool" sets nil )"bool" sets nil )"set" sets nil ))nil )))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ 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.0.207Bemerkung:
(vorverarbeitet am 2026-04-28)
¤ *Bot Zugriff
2026-05-26
