|
(float (vNum_TCC1 0
(vNum_TCC1-1 nil 3321636413 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(radix_div_vNum 0
(radix_div_vNum-1 nil 3319366647
("" (judgement-tcc)
((""
(case-replace
"expt(radix, Prec(b!1)) / radix=expt(radix, Prec(b!1)-1)")
(("1" (grind-reals) nil nil)
("2" (hide 2)
(("2" (rewrite "expt_minus_aux")
(("2" (rewrite "expt_x1_aux") nil nil)) nil))
nil))
nil))
nil)
((int_minus_int_is_int application-judgement "int" integers
nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields
nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers
nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(expt def-decl "real" exponentiation nil)
(> const-decl "bool" reals nil)
(above nonempty-type-eq-decl nil integers nil)
(radix formal-const-decl "above(1)" float nil)
(Format type-eq-decl nil float nil)
(- const-decl "[numfield, numfield -> numfield]"
number_fields nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(expt_minus_aux formula-decl nil exponentiation nil)
(expt_x1_aux formula-decl nil exponentiation nil)
(posnat_expt application-judgement "posnat" exponentiation
nil)
(^ const-decl "real" exponentiation nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(posint_exp application-judgement "posint" exponentiation
nil)
(vNum const-decl "posnat" float nil))
nil))
(radix_less_vNum 0
(radix_less_vNum-1 nil 3319366647
("" (judgement-tcc)
(("" (lemma "both_sides_expt_gt1_ge_aux")
(("" (inst -1 "radix" "Prec(b!1)-1" "0")
(("" (grind-reals)
(("" (rewrite "expt_x1_aux" -1) (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((both_sides_expt_gt1_ge_aux formula-decl nil exponentiation
nil)
(int_plus_int_is_int application-judgement "int" integers
nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(even_plus_odd_is_odd application-judgement "odd_int"
integers nil)
(expt_x1_aux formula-decl nil exponentiation nil)
(Format type-eq-decl nil float nil)
(- const-decl "[numfield, numfield -> numfield]"
number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(radix formal-const-decl "above(1)" float nil)
(above nonempty-type-eq-decl nil integers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers
nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" 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)
(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)
(int_minus_int_is_int application-judgement "int" integers
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posnat_expt application-judgement "posnat" exponentiation
nil)
(^ const-decl "real" exponentiation nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posint_exp application-judgement "posint" exponentiation
nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(vNum const-decl "posnat" float nil))
nil))
(FtoR_TCC1 0
(FtoR_TCC1-1 nil 3318615387 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(float_int_def 0
(float_int_def-1 nil 3544780855 ("" (grind) nil nil)
((float_int const-decl "float" float nil)
(expt def-decl "real" exponentiation nil)
(^ const-decl "real" exponentiation nil)
(FtoR const-decl "real" float nil))
shostak))
(Fplus_TCC1 0
(Fplus_TCC1-1 nil 3319889173 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)
(int_min application-judgement "{k: int | k <= i AND k <= j}"
real_defs nil))
nil))
(Fplus_TCC2 0
(Fplus_TCC2-1 nil 3319889173 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)
(int_min application-judgement "{k: int | k <= i AND k <= j}"
real_defs nil))
nil))
(Fplus_TCC3 0
(Fplus_TCC3-1 nil 3319889173 ("" (subtype-tcc) nil nil)
((^ const-decl "real" exponentiation nil)
(int_plus_int_is_int application-judgement "int" integers
nil)
(posnat_expt application-judgement "posnat" exponentiation
nil)
(int_minus_int_is_int application-judgement "int" integers
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)
(int_min application-judgement "{k: int | k <= i AND k <= j}"
real_defs nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(posrat_exp application-judgement "posrat" exponentiation
nil)
(rat_times_rat_is_rat application-judgement "rat" rationals
nil)
(rat_plus_rat_is_rat application-judgement "rat" rationals
nil))
nil))
(Fminus_TCC1 0
(Fminus_TCC1-1 nil 3319889173 ("" (subtype-tcc) nil nil)
((^ const-decl "real" exponentiation nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(posnat_expt application-judgement "posnat" exponentiation
nil)
(int_minus_int_is_int application-judgement "int" integers
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)
(int_min application-judgement "{k: int | k <= i AND k <= j}"
real_defs nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(posrat_exp application-judgement "posrat" exponentiation
nil)
(rat_times_rat_is_rat application-judgement "rat" rationals
nil)
(rat_minus_rat_is_rat application-judgement "rat" rationals
nil))
nil))
(sum_float_commutes 0
(sum_float_commutes-1 nil 3545039871 ("" (grind) nil nil)
((mult_divides2 application-judgement "(divides(m))" divides
nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(posint_times_posint_is_posint application-judgement "posint"
integers nil)
(posnat_expt application-judgement "posnat" exponentiation
nil)
(int_minus_int_is_int application-judgement "int" integers
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(expt def-decl "real" exponentiation nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs
nil)
(^ const-decl "real" exponentiation nil)
(Fplus const-decl "float" float nil)
(+ const-decl "float" float nil))
shostak))
(mult_float_commutes 0
(mult_float_commutes-1 nil 3545039902 ("" (grind) nil nil)
((Fmult const-decl "float" float nil)
(* const-decl "float" float nil))
shostak))
(FexptCorrect_TCC1 0
(FexptCorrect_TCC1-1 nil 3545396627 ("" (subtype-tcc) nil nil)
((nnrat_exp application-judgement "nnrat" exponentiation nil)
(posrat_exp application-judgement "posrat" exponentiation
nil)
(FtoR const-decl "real" float nil))
nil))
(FexptCorrect 0
(FexptCorrect-1 nil 3545396632
("" (skeep)
(("" (expand "^")
(("" (expand "Fexpt")
(("" (expand "FtoR")
(("" (lemma "mult_expt")
(("" (case "n = 0")
(("1" (replace -1)
(("1" (hide -) (("1" (grind) nil nil)) nil)) nil)
("2" (inst - "n" _ _)
(("2" (expand "^" - 1)
(("2" (rewrite -1)
(("1" (lemma "expt_times")
(("1" (inst - "Fexp(f)" "n" "radix")
(("1"
(replace -1 :dir rl)
(("1"
(hide -)
(("1"
(expand "^" + 2)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (replace -1)
(("2"
(expand "expt")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((^ const-decl "real" exponentiation nil)
(^ const-decl "float" float nil)
(FtoR const-decl "real" float nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers
nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(rat_times_rat_is_rat application-judgement "rat" rationals
nil)
(even_times_int_is_even application-judgement "even_int"
integers nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(posnat_expt application-judgement "posnat" exponentiation
nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(rat_expt application-judgement "rat" exponentiation nil)
(minus_int_is_int application-judgement "int" integers nil)
(expt def-decl "real" exponentiation nil)
(posrat_exp application-judgement "posrat" exponentiation
nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(int_expt application-judgement "int" exponentiation nil)
(nzreal_exp application-judgement "nzreal" exponentiation
nil)
(nnrat_times_nnrat_is_nnrat application-judgement
"nonneg_rat" rationals nil)
(nnint_times_nnint_is_nnint application-judgement
"nonneg_int" integers nil)
(nat_expt application-judgement "nat" exponentiation nil)
(int_minus_int_is_int application-judgement "int" integers
nil)
(expt_times formula-decl nil exponentiation nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(> const-decl "bool" reals nil)
(above nonempty-type-eq-decl nil integers nil)
(radix formal-const-decl "above(1)" float nil)
(f skolem-const-decl "float" float nil)
(float type-eq-decl nil float nil)
(/= const-decl "boolean" notequal nil)
(int_exp application-judgement "int" exponentiation nil)
(mult_expt formula-decl nil exponentiation nil)
(Fexpt const-decl "float" float nil))
nil))
(sigma_TCC1 0
(sigma_TCC1-1 nil 3544869888 ("" (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)
(>= const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers
nil)
(int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int_minus_int_is_int application-judgement "int" integers
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))
nil))
(sigma_TCC2 0
(sigma_TCC2-1 nil 3544869888 ("" (termination-tcc) nil nil) nil
nil))
(FDivInt_TCC1 0
(FDivInt_TCC1-1 nil 3544783712
("" (skeep)
(("" (typepred "i")
(("" (case "radix = mod(radix,i) + i * floor(radix / i)")
(("1" (replace -3)
(("1" (assert)
(("1" (replace -1)
(("1" (assert)
(("1"
(case "FORALL (ii,jj:int): integer_pred(ii*jj)")
(("1" (inst - "Fnum(f)" "floor(radix/i)")
(("1" (assert)
(("1" (hide-all-but (-1 1))
(("1" (grind :exclude "floor") nil nil))
nil))
nil))
nil)
("2" (hide-all-but 1) (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "mod") (("2" (propax) nil nil)) nil))
nil))
nil))
nil)
((radix formal-const-decl "above(1)" float nil)
(above nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(mod const-decl "{k | abs(k) < abs(j)}" mod 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)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(< const-decl "bool" reals nil)
(nonzero_integer nonempty-type-eq-decl nil integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nzint nonempty-type-eq-decl nil integers nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers
nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals 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)
(/= const-decl "boolean" notequal 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)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(float type-eq-decl nil float nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals
nil)
(rat_times_rat_is_rat application-judgement "rat" rationals
nil)
(int_plus_int_is_int application-judgement "int" integers
nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat"
rationals nil)
(+ const-decl "[numfield, numfield -> numfield]"
number_fields nil)
(* const-decl "[numfield, numfield -> numfield]"
number_fields nil)
(integer nonempty-type-from-decl nil integers nil)
(<= const-decl "bool" reals nil)
(floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields
nil))
nil))
(FDivInt_def 0
(FDivInt_def-1 nil 3544783715
("" (skeep)
(("" (expand "mod")
(("" (name "k" "floor(radix/i)")
(("" (case "k = radix/i")
(("1" (expand "FDivInt")
(("1" (replace -1 :dir rl)
(("1" (expand "FtoR")
(("1" (lemma "expt_plus")
(("1" (inst - "Fexp(f)-1" "1" "radix")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (replace -1) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((mult_divides1 application-judgement "(divides(n))" divides
nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(mod const-decl "{k | abs(k) < abs(j)}" mod nil)
(expt_plus formula-decl nil exponentiation nil)
(expt_x1 formula-decl nil exponentiation nil)
(rat_div_nzrat_is_rat application-judgement "rat" rationals
nil)
(rat_times_rat_is_rat application-judgement "rat" rationals
nil)
(posint_exp application-judgement "posint" exponentiation
nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(int_plus_int_is_int application-judgement "int" integers
nil)
(posrat_exp application-judgement "posrat" exponentiation
nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(- const-decl "[numfield, numfield -> numfield]"
number_fields nil)
(float type-eq-decl nil float nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(int_minus_int_is_int application-judgement "int" integers
nil)
(FtoR const-decl "real" float nil)
(FDivInt const-decl "float" float nil)
(real_div_nzreal_is_real application-judgement "real" reals
nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat"
rationals nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers
nil)
(integer nonempty-type-from-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(< const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]"
number_fields nil)
(floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields
nil)
(int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(above nonempty-type-eq-decl nil integers nil)
(radix formal-const-decl "above(1)" float nil)
(nzint nonempty-type-eq-decl nil integers nil))
shostak))
(hathatln_TCC1 0
(hathatln_TCC1-1 nil 3318954543
("" (grind-reals)
(("" (wrap-formula -1 "exp")
(("1" (rewrite "exp_ln" -1) (("1" (grind-reals) nil nil))
nil)
("2" (grind-reals) nil nil))
nil))
nil)
((number nonempty-type-decl nil numbers nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(>= 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)
(ln const-decl "real" ln_exp "lnexp_fnd/")
(exp const-decl "{py | x = ln(py)}" ln_exp "lnexp_fnd/")
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers
nil)
(int nonempty-type-eq-decl nil integers nil)
(above nonempty-type-eq-decl nil integers nil)
(radix formal-const-decl "above(1)" float nil)
(TRUE const-decl "bool" booleans nil)
(id const-decl "(bijective?[T, T])" identity nil)
(bijective? const-decl "bool" functions nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(exp_0 formula-decl nil ln_exp "lnexp_fnd/")
(exp_ln formula-decl nil ln_exp "lnexp_fnd/"))
nil))
(hathatln_TCC2 0
(hathatln_TCC2-1 nil 3318954543 ("" (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)
(>= 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)
(real_ge_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)
(/= const-decl "boolean" notequal nil)
(ln const-decl "real" ln_exp "lnexp_fnd/")
(real_div_nzreal_is_real application-judgement "real" reals
nil))
nil))
(hathatln 0
(hathatln-1 nil 3318954554
("" (skeep)
(("" (expand "^^")
(("" (case "radix=0")
(("1" (assert) nil nil)
("2" (assert)
(("2"
(case-replace
"-(ln(r) / ln(radix)) * ln(radix) = -ln(r)")
(("1" (hide -1)
(("1" (rewrite "exp_neg")
(("1" (rewrite "exp_ln") nil nil)) nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((real_div_nzreal_is_real application-judgement "real" reals
nil)
(minus_real_is_real application-judgement "real" reals nil)
(^^ const-decl "nnreal" expt "lnexp_fnd/")
(posreal_div_posreal_is_posreal application-judgement
"posreal" real_types nil)
(real_times_real_is_real application-judgement "real" reals
nil)
(exp_ln formula-decl nil ln_exp "lnexp_fnd/")
(exp_neg formula-decl nil ln_exp "lnexp_fnd/")
(ln const-decl "real" ln_exp "lnexp_fnd/")
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields
nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(* const-decl "[numfield, numfield -> numfield]"
number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers
nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(> const-decl "bool" reals nil)
(above nonempty-type-eq-decl nil integers nil)
(radix formal-const-decl "above(1)" float nil))
shostak))
(hathat_int_TCC1 0
(hathat_int_TCC1-1 nil 3319195930 ("" (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)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers
nil)
(int nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil))
nil))
(hathat_int_TCC2 0
(hathat_int_TCC2-1 nil 3545651010 ("" (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)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers
nil)
(int nonempty-type-eq-decl nil integers nil)
(/= const-decl "boolean" notequal nil))
nil))
(hathat_int 0
(hathat_int-1 nil 3319197088
("" (skeep)
(("" (expand "^")
(("" (case "e1 >= 0")
(("1" (grind-reals)
(("1" (rewrite "hathat_nat")
(("1" (expand "^") (("1" (propax) nil nil)) nil))
nil))
nil)
("2" (grind-reals)
(("2" (lemma "hathat_diff")
(("2" (inst -1 "radix" "-e1" "0")
(("2" (case-replace "0--e1=e1")
(("1" (rewrite -2)
(("1" (rewrite "hathat_nat")
(("1" (expand "^")
(("1" (grind-reals) nil nil)) nil))
nil))
nil)
("2" (hide -1 2 3) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((^ const-decl "real" exponentiation nil)
(div_cancel4 formula-decl nil real_props nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(minus_int_is_int application-judgement "int" integers nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(hathat_to_0 formula-decl nil expt "lnexp_fnd/")
(real_div_nzreal_is_real application-judgement "real" reals
nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posrat_times_posrat_is_posrat application-judgement "posrat"
rationals nil)
(div_cancel2 formula-decl nil real_props nil)
(nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
real_types nil)
(int_minus_int_is_int application-judgement "int" integers
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(- const-decl "[numfield, numfield -> numfield]"
number_fields nil)
(hathat_diff formula-decl nil expt "lnexp_fnd/")
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posnat_expt application-judgement "posnat" exponentiation
nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(posrat_exp application-judgement "posrat" exponentiation
nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(radix formal-const-decl "above(1)" float nil)
(above nonempty-type-eq-decl nil integers 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)
(hathat_nat formula-decl nil expt "lnexp_fnd/")
(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)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers
nil)
(int nonempty-type-eq-decl nil integers nil))
shostak))
(Fsucc_TCC1 0
(Fsucc_TCC1-1 nil 3321636413
("" (skeep)
(("" (lemma "radix_div_vNum") (("" (inst?) nil nil)) nil))
nil)
((radix_div_vNum formula-decl nil float nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(above nonempty-type-eq-decl nil integers nil)
(Format type-eq-decl nil float nil))
nil))
(Fpred_TCC1 0
(Fpred_TCC1-1 nil 3319211903
("" (skeep)
(("" (case-replace "-vNum(b) / radix = -(vNum(b)/radix)")
(("1" (hide -1)
(("1" (lemma "integers.closed_neg")
(("1" (inst?)
(("1" (hide 2)
(("1" (lemma "radix_div_vNum")
(("1" (inst -1 "b") nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (hide 2) (("2" (assert) nil nil)) nil))
nil))
nil)
((nzrat_div_nzrat_is_nzrat application-judgement "nzrat"
rationals nil)
(minus_nzrat_is_nzrat application-judgement "nzrat" rationals
nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number_field_pred const-decl "[number -> boolean]"
number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields
nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(above nonempty-type-eq-decl nil integers nil)
(Format type-eq-decl nil float nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers
nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(vNum const-decl "posnat" float nil)
(radix formal-const-decl "above(1)" float nil)
(int_minus_int_is_int application-judgement "int" integers
nil)
(minus_nzint_is_nzint application-judgement "nzint" integers
nil)
(closed_neg formula-decl nil integers nil)
(radix_div_vNum formula-decl nil float nil)
(b skolem-const-decl "Format" float nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil))
nil))
(Fnormalize_TCC1 0
(Fnormalize_TCC1-1 nil 3318871237 ("" (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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(above nonempty-type-eq-decl nil integers nil)
(Format type-eq-decl nil float nil)
(int nonempty-type-eq-decl nil integers nil)
(float type-eq-decl nil float nil)
(Fbounded? const-decl "bool" float nil)
(^ const-decl "real" exponentiation nil)
(real_lt_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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_int_is_int application-judgement "int" integers nil)
(int_minus_int_is_int application-judgement "int" integers
nil)
(posnat_expt application-judgement "posnat" exponentiation
nil)
(vNum const-decl "posnat" float nil)
(int_abs_is_nonneg application-judgement
"{j: nonneg_int | j >= i}" real_defs nil)
(posint_exp application-judgement "posint" exponentiation
nil))
nil))
(Fnormalize_TCC2 0
(Fnormalize_TCC2-1 nil 3318871237 ("" (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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(above nonempty-type-eq-decl nil integers nil)
(Format type-eq-decl nil float nil)
(int nonempty-type-eq-decl nil integers nil)
(float type-eq-decl nil float nil)
(^ const-decl "real" exponentiation nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_abs_is_nonneg application-judgement
"{j: nonneg_int | j >= i}" real_defs nil)
(posint_exp application-judgement "posint" exponentiation
nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_int_is_int application-judgement "int" integers nil)
(posnat_expt application-judgement "posnat" exponentiation
nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil)
(vNum const-decl "posnat" float nil)
(Fbounded? const-decl "bool" float nil)
(Fnormal? const-decl "bool" float nil)
(Fsubnormal? const-decl "bool" float nil)
(Fcanonic? const-decl "bool" float nil)
(FtoR const-decl "real" float nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(posrat_exp application-judgement "posrat" exponentiation
nil))
nil))
(Fnormalize_TCC3 0
(Fnormalize_TCC3-1 nil 3318871237 ("" (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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(above nonempty-type-eq-decl nil integers nil)
(Format type-eq-decl nil float nil)
(int nonempty-type-eq-decl nil integers nil)
(float type-eq-decl nil float nil)
(Fbounded? const-decl "bool" float nil)
(^ const-decl "real" exponentiation nil)
(posnat_expt application-judgement "posnat" exponentiation
nil)
(minus_int_is_int application-judgement "int" integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posint_exp application-judgement "posint" exponentiation
nil)
(int_abs_is_nonneg application-judgement
"{j: nonneg_int | j >= i}" real_defs nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(vNum const-decl "posnat" float nil)
(Fnormal? const-decl "bool" float nil)
(Fsubnormal? const-decl "bool" float nil)
(Fcanonic? const-decl "bool" float nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil))
nil))
(Fnormalize_TCC4 0
(Fnormalize_TCC4-1 nil 3318871237 ("" (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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(above nonempty-type-eq-decl nil integers nil)
(Format type-eq-decl nil float nil)
(int nonempty-type-eq-decl nil integers nil)
(float type-eq-decl nil float nil)
(posnat_expt application-judgement "posnat" exponentiation
nil)
(minus_int_is_int application-judgement "int" integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posint_exp application-judgement "posint" exponentiation
nil)
(int_abs_is_nonneg application-judgement
"{j: nonneg_int | j >= i}" real_defs nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(^ const-decl "real" exponentiation nil)
(vNum const-decl "posnat" float nil)
(Fbounded? const-decl "bool" float nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil))
nil))
(Fnormalize_TCC5 0
(Fnormalize_TCC5-1 nil 3318871660
("" (skosimp)
(("" (grind-reals)
(("" (expand "abs" 4 2)
(("" (wrap-formula 2 "abs")
(("" (expand "abs" 1 2)
(("" (cancel-by 4 "abs(Fnum(f!1))")
(("" (hide-all-but (-1 3)) (("" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((both_sides_minus_lt2 formula-decl nil real_props nil)
(abs_mult formula-decl nil real_props nil)
(minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_abs_is_nonneg application-judgement
"{j: nonneg_int | j >= i}" real_defs nil)
(nnint_times_nnint_is_nnint application-judgement
"nonneg_int" integers nil)
(nzint_abs_is_pos application-judgement
"{j: posint | j >= i}" real_defs nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers
nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props 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)
(>= 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)
(* const-decl "[numfield, numfield -> numfield]"
number_fields nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers
nil)
(int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(above nonempty-type-eq-decl nil integers nil)
(radix formal-const-decl "above(1)" float nil)
(float type-eq-decl nil float nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(Format type-eq-decl nil float nil)
(Fbounded? const-decl "bool" float nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(vNum const-decl "posnat" float nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(abs_abs formula-decl nil real_props nil)
(div_cancel1 formula-decl nil real_props nil)
(rat_times_rat_is_rat application-judgement "rat" rationals
nil)
(< const-decl "bool" reals nil)
(pos_div_ge formula-decl nil real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(/= const-decl "boolean" notequal nil)
(b!1 skolem-const-decl "Format" float nil)
(f!1 skolem-const-decl "(Fbounded?(b!1))" float nil)
(CBD_1 skolem-const-decl
"{n: nonneg_real | n >= Fnum(f!1) AND n >= -Fnum(f!1)}"
float nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields
nil)
(both_sides_times_pos_ge1_imp formula-decl nil
extra_real_props nil)
(nzrat_div_nzrat_is_nzrat application-judgement "nzrat"
rationals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil))
nil))
(Fnormalize_TCC6 0
(Fnormalize_TCC6-1 nil 3319287157
("" (skosimp)
(("" (split)
(("1"
(typepred
"v!1(b!1)((# Fnum := radix * Fnum(f!1), Fexp := Fexp(f!1) - 1 #))")
(("1" (replaces -2)
(("1" (expand "FtoR")
(("1" (rewrite "expt_div" :dir rl)
(("1" (rewrite "expt_x1") (("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(typepred
"v!1(b!1)((# Fnum := radix * Fnum(f!1), Fexp := Fexp(f!1) - 1 #))")
(("2" (assert) nil nil)) nil))
nil))
nil)
((nzreal nonempty-type-eq-decl nil reals nil)
(/= const-decl "boolean" notequal nil)
(expt_div formula-decl nil exponentiation nil)
(posrat_exp application-judgement "posrat" exponentiation
nil)
(rat_times_rat_is_rat application-judgement "rat" rationals
nil)
(posint_exp application-judgement "posint" exponentiation
nil)
(nnrat_exp application-judgement "nnrat" exponentiation nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(expt_x1 formula-decl nil exponentiation nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers
nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(above nonempty-type-eq-decl nil integers nil)
(Format type-eq-decl nil float nil)
(int nonempty-type-eq-decl nil integers nil)
(float type-eq-decl nil float nil)
(Fcanonic? const-decl "bool" float nil)
(Fbounded? const-decl "bool" float 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)
(< const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]"
number_fields nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers
nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(vNum const-decl "posnat" float nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}"
real_defs nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(FtoR const-decl "real" float nil)
(<= const-decl "bool" reals nil)
(* const-decl "[numfield, numfield -> numfield]"
number_fields nil)
(radix formal-const-decl "above(1)" float nil)
(mult_divides2 application-judgement "(divides(m))" divides
nil)
(mult_divides1 application-judgement "(divides(n))" divides
nil)
(int_abs_is_nonneg application-judgement
"{j: nonneg_int | j >= i}" real_defs nil))
nil))
(Fulp_TCC1 0
(Fulp_TCC1-1 nil 3318887371 ("" (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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(above nonempty-type-eq-decl nil integers nil)
(Format type-eq-decl nil float nil)
(int nonempty-type-eq-decl nil integers nil)
(float type-eq-decl nil float nil)
(Fbounded? const-decl "bool" float nil)
(vNum const-decl "posnat" float nil)
(minus_int_is_int application-judgement "int" integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posint_exp application-judgement "posint" exponentiation
nil)
(int_abs_is_nonneg application-judgement
"{j: nonneg_int | j >= i}" real_defs nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(/= const-decl "boolean" notequal nil))
nil))
(FcanonicOpp 0
(FcanonicOpp-1 nil 3319221457
("" (skeep)
(("" (split)
(("1" (skosimp*)
(("1" (expand "Fcanonic?")
(("1" (split)
(("1" (case "Fnormal?(b)(Fopp(f))")
(("1" (assert) nil nil)
("2" (hide 2)
(("2" (expand* "Fnormal?" "Fbounded?" "Fopp")
(("2" (flatten)
(("2" (split)
(("1"
(case-replace
"abs(-(Fnum(f)))=abs(Fnum(f))")
(("1"
(hide -1 -2 -3 2)
(("1"
(expand "abs")
(("1" (grind-reals) nil nil))
nil))
nil))
nil)
("2" (propax) nil nil)
("3"
(case-replace
"abs(radix * -(Fnum(f)))=abs(radix * Fnum(f))")
(("3"
(hide -1 -2 -3 2)
(("3"
(expand "abs")
(("3"
(grind-reals)
(("1"
(case "-(radix * (Fnum(f))) > 0")
(("1" (grind-reals) nil nil)
("2"
(hide -1)
(("2"
(cancel-by 1 "radix")
nil
nil))
nil))
nil)
("2"
(flip-ineq 2)
(("2"
(hide 2)
(("2"
(cancel-by 1 "radix")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (case "Fsubnormal?(b)(Fopp(f))")
(("1" (assert) nil nil)
("2" (hide 2)
(("2" (expand* "Fopp" "Fsubnormal?" "Fbounded?")
(("2" (flatten)
(("2" (split)
(("1"
(case-replace
"abs(-(Fnum(f)))=abs(Fnum(f))")
(("1"
(hide -1 -2 -3 -4 2)
(("1"
(expand "abs")
(("1" (grind-reals) nil nil))
nil))
nil))
nil)
("2" (propax) nil nil)
("3" (propax) nil nil)
("4"
(case-replace
"abs(radix * -(Fnum(f)))=abs(radix * Fnum(f))")
(("4"
(hide -1 -2 -3 -4 2)
(("4"
(expand "abs")
(("4"
(grind-reals)
(("1"
(flip-ineq -1)
(("1"
(cancel-by 1 "radix")
nil
nil))
nil)
("2"
(flip-ineq 2)
(("2"
(hide 2)
(("2"
(cancel-by 1 "radix")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "Fcanonic?")
(("2" (split)
(("1" (case "Fnormal?(b)(f)")
(("1" (assert) nil nil)
("2" (hide 2)
(("2" (expand* "Fnormal?" "Fopp" "Fbounded?")
(("2" (flatten)
(("2" (split)
(("1"
(case-replace
"abs(Fnum(f))=abs(-(Fnum(f)))")
(("1"
(hide -1 -2 -3 2)
(("1"
(expand "abs")
(("1" (grind-reals) nil nil))
nil))
nil))
nil)
("2" (propax) nil nil)
("3"
(case-replace
"abs(radix * (Fnum(f)))=abs(radix * -(Fnum(f)))")
(("3"
(hide -1 -2 -3 2)
(("3"
(expand "abs")
(("3"
(grind-reals)
(("1"
(flip-ineq -2)
(("1"
(cancel-by 1 "radix")
nil
nil))
nil)
("2"
(flip-ineq 1)
(("2"
(cancel-by 1 "radix")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (case " Fsubnormal?(b)(f)")
(("1" (assert) nil nil)
("2" (hide 2)
(("2" (expand* "Fsubnormal?" "Fopp" "Fbounded?")
(("2" (flatten)
(("2" (split)
(("1"
(case-replace
"abs(Fnum(f))=abs(-(Fnum(f)))")
(("1"
(hide -1 -2 -3 -4 2)
(("1"
(expand "abs")
(("1" (grind-reals) nil nil))
nil))
nil))
nil)
("2" (propax) nil nil)
("3" (propax) nil nil)
("4"
(case-replace
"abs(radix * (Fnum(f)))=abs(radix * -(Fnum(f)))")
(("4"
(hide -1 -2 -3 -4 2)
(("4"
(expand "abs")
(("4"
(grind-reals)
(("1"
(flip-ineq -2)
(("1"
(cancel-by 1 "radix")
nil
nil))
nil)
("2"
(flip-ineq 1)
(("2"
(cancel-by 1 "radix")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Fcanonic? const-decl "bool" float nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.102 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.
|
