|
(real_fun_supinf
(nonempty_image 0
(nonempty_image-2 nil 3307806390
("" (grind)
(("" (inst - "f!1(epsilon! x: true)") (("" (inst?) nil nil)) nil))
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)
(T_pred const-decl "[real -> boolean]" real_fun_supinf nil)
(T formal-nonempty-subtype-decl nil real_fun_supinf nil)
(bool nonempty-type-eq-decl nil booleans nil)
(pred type-eq-decl nil defined_types nil)
(epsilon const-decl "T" epsilons nil)
(TRUE const-decl "bool" booleans nil)
(nonempty? const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(Im const-decl "setof[real]" real_fun_props "reals/"))
nil)
(nonempty_image-1 nil 3307697310
("" (grind)
(("" (inst - "f!1(epsilon! x: true)") (("" (inst?) nil nil)) nil))
nil)
nil nil))
(bounded_above_image 0
(bounded_above_image-2 nil 3307806390
("" (grind :if-match nil)
(("" (inst + "a!1")
(("" (reduce :if-match nil) (("" (inst?) nil nil)) nil)) nil))
nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Im const-decl "setof[real]" real_fun_props "reals/")
(setof type-eq-decl nil defined_types 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)
(T_pred const-decl "[real -> boolean]" real_fun_supinf nil)
(T formal-nonempty-subtype-decl nil real_fun_supinf nil)
(bounded_above? const-decl "bool" real_fun_preds "reals/")
(nonempty_image application-judgement "(nonempty?[real])"
real_fun_supinf nil)
(bounded_above? const-decl "bool" bounded_real_defs nil)
(upper_bound? const-decl "bool" bounded_real_defs nil))
nil)
(bounded_above_image-1 nil 3307697310
("" (grind :if-match nil)
(("" (inst + "a!1")
(("" (reduce :if-match nil) (("" (inst?) nil nil)) nil)) nil))
nil)
((bounded_above? const-decl "bool" real_fun_preds "reals/")) nil))
(bounded_below_image 0
(bounded_below_image-2 nil 3307806390
("" (grind :if-match nil)
(("" (inst + "a!1")
(("" (reduce :if-match nil) (("" (inst?) nil nil)) nil)) nil))
nil)
((real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(Im const-decl "setof[real]" real_fun_props "reals/")
(setof type-eq-decl nil defined_types 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)
(T_pred const-decl "[real -> boolean]" real_fun_supinf nil)
(T formal-nonempty-subtype-decl nil real_fun_supinf nil)
(bounded_below? const-decl "bool" real_fun_preds "reals/")
(nonempty_image application-judgement "(nonempty?[real])"
real_fun_supinf nil)
(bounded_below? const-decl "bool" bounded_real_defs nil)
(lower_bound? const-decl "bool" bounded_real_defs nil))
nil)
(bounded_below_image-1 nil 3307697310
("" (grind :if-match nil)
(("" (inst + "a!1")
(("" (reduce :if-match nil) (("" (inst?) nil nil)) nil)) nil))
nil)
((bounded_below? const-decl "bool" real_fun_preds "reals/")) nil))
(supfun_is_bound 0
(supfun_is_bound-2 nil 3307806390
("" (skolem!)
(("" (expand "sup")
(("" (rewrite "lub_is_bound")
(("" (delete 2) (("" (grind) nil nil)) nil)) nil))
nil))
nil)
((sup const-decl "real" real_fun_supinf nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(bounded_above? const-decl "bool" real_fun_preds "reals/")
(Im const-decl "setof[real]" real_fun_props "reals/")
(setof type-eq-decl nil defined_types nil)
(T formal-nonempty-subtype-decl nil real_fun_supinf nil)
(T_pred const-decl "[real -> boolean]" real_fun_supinf nil)
(bounded_above? const-decl "bool" bounded_real_defs 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)
(lub_is_bound formula-decl nil real_facts "reals/")
(bounded_above_image application-judgement "(bounded_above?)"
real_fun_supinf nil))
nil)
(supfun_is_bound-1 nil 3307697310
("" (skolem!)
(("" (expand "sup")
(("" (rewrite "lub_is_bound")
(("" (delete 2) (("" (grind) nil nil)) nil)) nil))
nil))
nil)
((bounded_above? const-decl "bool" real_fun_preds "reals/")
(lub_is_bound formula-decl nil real_facts "reals/"))
nil))
(supfun_is_sup 0
(supfun_is_sup-2 nil 3307806390
("" (skosimp)
(("" (expand "sup")
(("" (use "adherence_sup")
(("" (auto-rewrite "Im")
(("" (apply (then (reduce :if-match nil) (inst?) (assert)))
nil nil))
nil))
nil))
nil))
nil)
((sup const-decl "real" real_fun_supinf nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(bounded_above_image application-judgement "(bounded_above?)"
real_fun_supinf 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)
(set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(bounded_above? const-decl "bool" bounded_real_defs nil)
(T_pred const-decl "[real -> boolean]" real_fun_supinf nil)
(T formal-nonempty-subtype-decl nil real_fun_supinf nil)
(setof type-eq-decl nil defined_types nil)
(Im const-decl "setof[real]" real_fun_props "reals/")
(bounded_above? const-decl "bool" real_fun_preds "reals/")
(>= 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)
(adherence_sup formula-decl nil real_facts "reals/"))
nil)
(supfun_is_sup-1 nil 3307697310
("" (skosimp)
(("" (expand "sup")
(("" (use "adherence_sup")
(("" (auto-rewrite "Im")
(("" (apply (then (reduce :if-match nil) (inst?) (assert)))
nil nil))
nil))
nil))
nil))
nil)
((bounded_above? const-decl "bool" real_fun_preds "reals/")
(adherence_sup formula-decl nil real_facts "reals/"))
nil))
(supfun_is_sup2 0
(supfun_is_sup2-2 nil 3307806390
("" (skolem!)
(("" (expand "sup")
(("" (rewrite "lub_is_lub")
(("" (grind :if-match nil)
(("1" (inst?) (("1" (inst?) nil nil)) nil)
("2" (inst?) nil nil))
nil))
nil))
nil))
nil)
((sup const-decl "real" real_fun_supinf nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(x!1 skolem-const-decl "T" real_fun_supinf nil)
(g!1 skolem-const-decl "{f | bounded_above?(f)}" real_fun_supinf
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(bounded_above? const-decl "bool" real_fun_preds "reals/")
(Im const-decl "setof[real]" real_fun_props "reals/")
(setof type-eq-decl nil defined_types nil)
(T formal-nonempty-subtype-decl nil real_fun_supinf nil)
(T_pred const-decl "[real -> boolean]" real_fun_supinf nil)
(bounded_above? const-decl "bool" bounded_real_defs 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)
(lub_is_lub formula-decl nil real_facts "reals/")
(bounded_above_image application-judgement "(bounded_above?)"
real_fun_supinf nil))
nil)
(supfun_is_sup2-1 nil 3307697310
("" (skolem!)
(("" (expand "sup")
(("" (rewrite "lub_is_lub")
(("" (grind :if-match nil)
(("1" (inst?) (("1" (inst?) nil nil)) nil)
("2" (inst?) nil nil))
nil))
nil))
nil))
nil)
((bounded_above? const-decl "bool" real_fun_preds "reals/")
(lub_is_lub formula-decl nil real_facts "reals/"))
nil))
(inffun_is_bound 0
(inffun_is_bound-2 nil 3307806390
("" (skolem!)
(("" (expand "inf")
(("" (rewrite "glb_is_bound")
(("" (delete 2) (("" (grind) nil nil)) nil)) nil))
nil))
nil)
((inf const-decl "real" real_fun_supinf nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(bounded_below? const-decl "bool" real_fun_preds "reals/")
(Im const-decl "setof[real]" real_fun_props "reals/")
(setof type-eq-decl nil defined_types nil)
(T formal-nonempty-subtype-decl nil real_fun_supinf nil)
(T_pred const-decl "[real -> boolean]" real_fun_supinf nil)
(bounded_below? const-decl "bool" bounded_real_defs 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)
(glb_is_bound formula-decl nil real_facts "reals/")
(bounded_below_image application-judgement "(bounded_below?)"
real_fun_supinf nil))
nil)
(inffun_is_bound-1 nil 3307697310
("" (skolem!)
(("" (expand "inf")
(("" (rewrite "glb_is_bound")
(("" (delete 2) (("" (grind) nil nil)) nil)) nil))
nil))
nil)
((bounded_below? const-decl "bool" real_fun_preds "reals/")
(glb_is_bound formula-decl nil real_facts "reals/"))
nil))
(inffun_is_inf 0
(inffun_is_inf-2 nil 3307806390
("" (skosimp)
(("" (expand "inf")
(("" (use "adherence_inf")
(("" (auto-rewrite "Im")
(("" (apply (then (reduce :if-match nil) (inst?) (assert)))
nil nil))
nil))
nil))
nil))
nil)
((inf const-decl "real" real_fun_supinf nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(bounded_below_image application-judgement "(bounded_below?)"
real_fun_supinf 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)
(set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(bounded_below? const-decl "bool" bounded_real_defs nil)
(T_pred const-decl "[real -> boolean]" real_fun_supinf nil)
(T formal-nonempty-subtype-decl nil real_fun_supinf nil)
(setof type-eq-decl nil defined_types nil)
(Im const-decl "setof[real]" real_fun_props "reals/")
(bounded_below? const-decl "bool" real_fun_preds "reals/")
(>= 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)
(adherence_inf formula-decl nil real_facts "reals/"))
nil)
(inffun_is_inf-1 nil 3307697310
("" (skosimp)
(("" (expand "inf")
(("" (use "adherence_inf")
(("" (auto-rewrite "Im")
(("" (apply (then (reduce :if-match nil) (inst?) (assert)))
nil nil))
nil))
nil))
nil))
nil)
((bounded_below? const-decl "bool" real_fun_preds "reals/")
(adherence_inf formula-decl nil real_facts "reals/"))
nil))
(inffun_is_inf2 0
(inffun_is_inf2-2 nil 3307806390
("" (skolem!)
(("" (expand "inf")
(("" (rewrite "glb_is_glb")
(("" (grind :if-match nil)
(("1" (inst?) (("1" (inst?) nil nil)) nil)
("2" (inst?) nil nil))
nil))
nil))
nil))
nil)
((inf const-decl "real" real_fun_supinf nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(x!1 skolem-const-decl "T" real_fun_supinf nil)
(h!1 skolem-const-decl "{f | bounded_below?(f)}" real_fun_supinf
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(bounded_below? const-decl "bool" real_fun_preds "reals/")
(Im const-decl "setof[real]" real_fun_props "reals/")
(setof type-eq-decl nil defined_types nil)
(T formal-nonempty-subtype-decl nil real_fun_supinf nil)
(T_pred const-decl "[real -> boolean]" real_fun_supinf nil)
(bounded_below? const-decl "bool" bounded_real_defs 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)
(glb_is_glb formula-decl nil real_facts "reals/")
(bounded_below_image application-judgement "(bounded_below?)"
real_fun_supinf nil))
nil)
(inffun_is_inf2-1 nil 3307697310
("" (skolem!)
(("" (expand "inf")
(("" (rewrite "glb_is_glb")
(("" (grind :if-match nil)
(("1" (inst?) (("1" (inst?) nil nil)) nil)
("2" (inst?) nil nil))
nil))
nil))
nil))
nil)
((bounded_below? const-decl "bool" real_fun_preds "reals/")
(glb_is_glb formula-decl nil real_facts "reals/"))
nil))
(supfun_neg_TCC1 0
(supfun_neg_TCC1-2 nil 3307806390
("" (skolem!) (("" (rewrite "bounded_above_neg[T]") nil nil)) nil)
((bounded_above_neg formula-decl nil real_fun_props "reals/")
(bool nonempty-type-eq-decl nil booleans nil)
(bounded_below? const-decl "bool" real_fun_preds "reals/")
(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)
(T_pred const-decl "[real -> boolean]" real_fun_supinf nil)
(T formal-nonempty-subtype-decl nil real_fun_supinf nil))
nil)
(supfun_neg_TCC1-1 nil 3307697310
("" (skolem!) (("" (rewrite "bounded_above_opposite[T]") nil nil))
nil)
((bounded_below? const-decl "bool" real_fun_preds "reals/")) nil))
(supfun_neg 0
(supfun_neg-2 nil 3307806390
("" (skolem!)
(("" (auto-rewrite "supfun_neg_TCC1" "-")
(("" (use "supfun_is_sup2")
(("" (use "inffun_is_inf2" ("a" "- sup(- h!1)"))
(("" (ground)
(("" (case-replace "sup(-h!1) <= -inf(h!1)")
(("1" (assert) nil nil)
("2" (lemma "supfun_is_sup2")
(("2" (inst - "-inf(h!1)" "-h!1")
(("2" (assert)
(("2" (skosimp*)
(("2" (inst?)
(("2" (inst?)
(("2" (assert)
(("2" (use "inffun_is_bound")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((inffun_is_inf2 formula-decl nil real_fun_supinf nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(inf const-decl "real" real_fun_supinf nil)
(<= const-decl "bool" reals nil)
(inffun_is_bound formula-decl nil real_fun_supinf nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sup const-decl "real" real_fun_supinf nil)
(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)
(T_pred const-decl "[real -> boolean]" real_fun_supinf nil)
(T formal-nonempty-subtype-decl nil real_fun_supinf nil)
(bool nonempty-type-eq-decl nil booleans nil)
(bounded_above? const-decl "bool" real_fun_preds "reals/")
(- const-decl "[T -> real]" real_fun_ops "reals/")
(bounded_below? const-decl "bool" real_fun_preds "reals/")
(supfun_is_sup2 formula-decl nil real_fun_supinf nil))
nil)
(supfun_neg-1 nil 3307697310
("" (skolem!)
(("" (auto-rewrite "supfun_neg_TCC1" "-")
(("" (use "supfun_is_sup2")
(("" (use "inffun_is_inf2" ("a" "- sup(- h!1)"))
(("" (ground)
(("1" (skolem!)
(("1" (use "inffun_is_bound") (("1" (assert) nil nil))
nil))
nil)
("2" (skolem!)
(("2" (use "supfun_is_bound" ("g" "-h!1"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
nil nil))
(inffun_neg_TCC1 0
(inffun_neg_TCC1-3 nil 3442582387
("" (skolem!) (("" (rewrite "bounded_below_neg[T]") nil nil)) nil)
((bounded_below_neg formula-decl nil real_fun_props "reals/")
(bool nonempty-type-eq-decl nil booleans nil)
(bounded_above? const-decl "bool" real_fun_preds "reals/")
(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)
(T_pred const-decl "[real -> boolean]" real_fun_supinf nil)
(T formal-nonempty-subtype-decl nil real_fun_supinf nil))
nil)
(inffun_neg_TCC1-2 nil 3307806390
("" (skolem!) (("" (rewrite "bounded_below_opposite[T]") nil nil))
nil)
((bounded_above? const-decl "bool" real_fun_preds "reals/")) nil)
(inffun_neg_TCC1-1 nil 3307697310
("" (skolem!) (("" (rewrite "bounded_below_opposite[T]") nil nil))
nil)
((bounded_above? const-decl "bool" real_fun_preds "reals/")) nil))
(inffun_neg 0
(inffun_neg-2 nil 3307806390
("" (skolem!)
(("" (auto-rewrite "inffun_neg_TCC1" "-")
(("" (use "inffun_is_inf2")
(("" (use "supfun_is_sup2" ("a" "- inf(- g!1)"))
(("" (ground)
(("" (case "inf(-g!1) >= -sup(g!1)")
(("1" (assert) nil nil)
("2" (hide 2)
(("2" (hide -1)
(("2" (lemma "inffun_is_inf2")
(("2" (inst - "-sup(g!1)" "-g!1")
(("2" (assert)
(("2" (skosimp*)
(("2" (inst?)
(("2" (inst?)
(("2"
(assert)
(("2"
(use "supfun_is_bound")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((supfun_is_sup2 formula-decl nil real_fun_supinf nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(>= const-decl "bool" reals nil)
(sup const-decl "real" real_fun_supinf nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(supfun_is_bound formula-decl nil real_fun_supinf nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(inf const-decl "real" real_fun_supinf nil)
(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)
(T_pred const-decl "[real -> boolean]" real_fun_supinf nil)
(T formal-nonempty-subtype-decl nil real_fun_supinf nil)
(bool nonempty-type-eq-decl nil booleans nil)
(bounded_below? const-decl "bool" real_fun_preds "reals/")
(- const-decl "[T -> real]" real_fun_ops "reals/")
(bounded_above? const-decl "bool" real_fun_preds "reals/")
(inffun_is_inf2 formula-decl nil real_fun_supinf nil))
nil)
(inffun_neg-1 nil 3307697310
("" (skolem!)
(("" (auto-rewrite "inffun_neg_TCC1" "-")
(("" (use "inffun_is_inf2")
(("" (use "supfun_is_sup2" ("a" "- inf(- g!1)"))
(("" (ground)
(("1" (skolem!)
(("1" (use "supfun_is_bound") (("1" (assert) nil nil))
nil))
nil)
("2" (skolem!)
(("2" (use "inffun_is_bound" ("h" "-g!1"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
nil nil))
(max_upper_bound 0
(max_upper_bound-2 nil 3307806390
("" (skolem!)
(("" (split)
(("1" (flatten)
(("1" (forward-chain "max_bounded[T]")
(("1" (assert)
(("1" (use "supfun_is_bound")
(("1" (expand "is_maximum?")
(("1" (use "supfun_is_sup2" ("g" "f!1"))
(("1" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (assert)
(("2" (expand "is_maximum?")
(("2" (replace -2 + rl)
(("2" (lemma "supfun_is_bound" ("g" "f!1"))
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((max_bounded formula-decl nil real_fun_props "reals/")
(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)
(T_pred const-decl "[real -> boolean]" real_fun_supinf nil)
(T formal-nonempty-subtype-decl nil real_fun_supinf nil)
(supfun_is_bound formula-decl nil real_fun_supinf nil)
(bounded_above? const-decl "bool" real_fun_preds "reals/")
(bool nonempty-type-eq-decl nil booleans nil)
(supfun_is_sup2 formula-decl nil real_fun_supinf nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(is_maximum? const-decl "bool" real_fun_preds "reals/"))
nil)
(max_upper_bound-1 nil 3307697310
("" (skolem!)
(("" (split)
(("1" (flatten)
(("1" (forward-chain "max_bounded[T]")
(("1" (assert)
(("1" (use "supfun_is_bound")
(("1" (expand "is_maximum?")
(("1" (use "supfun_is_sup2" ("g" "f!1"))
(("1" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (assert)
(("2" (expand "is_maximum?")
(("2" (replace -2 + rl)
(("2" (lemma "supfun_is_bound" ("g" "f!1"))
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((max_bounded formula-decl nil real_fun_props "reals/")
(bounded_above? const-decl "bool" real_fun_preds "reals/")
(is_maximum? const-decl "bool" real_fun_preds "reals/"))
nil))
(min_lower_bound 0
(min_lower_bound-2 nil 3307806390
("" (skolem!)
(("" (split)
(("1" (flatten)
(("1" (forward-chain "min_bounded[T]")
(("1" (assert)
(("1" (use "inffun_is_bound")
(("1" (expand "is_minimum?")
(("1" (use "inffun_is_inf2" ("h" "f!1"))
(("1" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (assert)
(("2" (expand "is_minimum?")
(("2" (replace -2 + rl)
(("2" (lemma "inffun_is_bound" ("h" "f!1"))
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((min_bounded formula-decl nil real_fun_props "reals/")
(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)
(T_pred const-decl "[real -> boolean]" real_fun_supinf nil)
(T formal-nonempty-subtype-decl nil real_fun_supinf nil)
(inffun_is_bound formula-decl nil real_fun_supinf nil)
(bounded_below? const-decl "bool" real_fun_preds "reals/")
(bool nonempty-type-eq-decl nil booleans nil)
(inffun_is_inf2 formula-decl nil real_fun_supinf nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(is_minimum? const-decl "bool" real_fun_preds "reals/"))
nil)
(min_lower_bound-1 nil 3307697310
("" (skolem!)
(("" (split)
(("1" (flatten)
(("1" (forward-chain "min_bounded[T]")
(("1" (assert)
(("1" (use "inffun_is_bound")
(("1" (expand "is_minimum?")
(("1" (use "inffun_is_inf2" ("h" "f!1"))
(("1" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (assert)
(("2" (expand "is_minimum?")
(("2" (replace -2 + rl)
(("2" (lemma "inffun_is_bound" ("h" "f!1"))
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((min_bounded formula-decl nil real_fun_props "reals/")
(bounded_below? const-decl "bool" real_fun_preds "reals/")
(is_minimum? const-decl "bool" real_fun_preds "reals/"))
nil)))
¤ Dauer der Verarbeitung: 0.61 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.
|
