Quelle axpy.prf
Sprache: Lisp
(axpynil 3320508538"" (skeep)"" (typepred "x1" ) (("" (rewrite "FcanonicBounded" ) nil nil ))nil ))nil )"Format" axpy nil )"bool" float nil )nil float nil )nil float nil )"above(1)" axpy nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil integers nil )nil naturalnumbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil float nil ))nil ))nil 3320496512"" (skeep)"" (expand "MinOrMax?" )"" (split)"1" (rewrite "RoundedModeUlp" :subst ("b" "b" "P" "isMin?" ))"1" (rewrite "isMin_RoundedMode" ) nil nil )) nil )"2" (rewrite "RoundedModeUlp" :subst ("b" "b" "P" "isMax?" ))"2" (rewrite "isMax_RoundedMode" ) nil nil )) nil ))nil ))nil ))nil )"bool" axpy nil )"bool" float nil )nil float nil )nil float nil )nil float nil )nil float nil )nil naturalnumbers nil )"bool" float nil )nil float nil )"bool" float nil )"Format" axpy nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"above(1)" axpy nil )"(strict_total_order?[real])" real_props nil )nil float nil )"real" reals nil ))nil 3320496511"" (skeep) (("" (rewrite "FoppBounded" ) nil nil )) nil )nil float nil )nil naturalnumbers nil )nil float nil )"Format" axpy nil )nil float nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"above(1)" axpy nil ))nil ))nil 3320496618"" (skeep)"" (expand "MinOrMax?" )"" (split)"1" (skosimp*) (("1" (rewrite "MinOppMax" ) nil nil )) nil )"2" (skosimp*) (("2" (rewrite "MaxOppMin" ) nil nil )) nil ))nil ))nil ))nil )"bool" axpy nil )nil float nil )"above(1)" axpy nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil float nil )"Format" axpy nil )nil float nil )nil naturalnumbers nil )nil float nil ))nil 3320496511"" (skeep)"" (rewrite "FcanonicBounded" )"" (rewrite "FpredCanonic" ) nil nil )) nil ))nil )nil float nil )nil naturalnumbers nil )nil float nil )"Format" axpy nil )nil float nil )"float" float nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"above(1)" axpy nil )"(strict_total_order?[real])" real_props nil )nil float nil ))nil ))nil 3320504768"" (skeep) (("" (rewrite "FcanonicBounded" ) nil nil )) nil )nil float nil )nil naturalnumbers nil )nil float nil )"Format" axpy nil )nil float nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"above(1)" axpy nil )"real" reals nil ))nil ))nil 3320504301"" (skeep)"" (case "z <= FtoR(f)" )"1" (expand "abs" -4)"1" (grind-reals)"1" (expand "MinOrMax?" )"1" (skosimp*)"1" (hide 1)"1" (expand "isMax?" )"1" (skosimp*)"1" (lemma "FsuccFpred" :subst ("f" "f" "b" "b" ))"1" (split)"1" (replace -1 1 :dir rl)"1" "FtoR(f!1)=FtoR(Fnormalize(b)(f!1))" )"1" (rewrite "FsuccProp" )"1" "z" :strict 1)"1" " FtoR[radix](f)-Fulp(b)(Fpred(b)(f))" "1" rewrite "FpredDiff" :dir rl)"1" (assert ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (rewrite "FpredCanonic" ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flip-ineq 1)"2" (expand "abs" -4)"2" (grind-reals)"2" (expand "MinOrMax?" )"2" (skosimp*)"2" (hide 2)"2" (expand "isMin?" )"2" (skosimp*)"2" "FpredFsucc" :subst ("f" "f" "b" "b" ))"2" (split)"1" (replace -1 1 :dir rl)"1" "FtoR(f!1)=FtoR(Fnormalize(b)(f!1))" )"1" rewrite "FpredProp" )"1" "z" :strict 2)"1" "FtoR(f)+Fulp(b)(Fpred(b)(f))" "1" (assert ) nil nil )"2" "FtoR(f)+Fulp(b)(f)" )"1" assert )"1" rewrite "FulpFpred1" )nil nil ))nil )"2" rewrite "FsuccDiff" :dir rl)"2" (assert ) nil nil ))nil )"3" "3" rewrite "FcanonicBounded" )nil nil ))nil )"4" rewrite "FcanonicBounded" )nil nil ))nil ))nil ))nil )"2" rewrite "FsuccCanonic" )nil nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" float nil )nil float nil )"above(1)" axpy nil )nil integers nil )"bool" reals nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"bool" float nil )nil float nil )nil naturalnumbers nil )nil float nil )"Format" axpy nil )"float" float nil )nil float nil )"real" float nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil float nil )"bool" reals nil )nil float nil )"[T, T -> boolean]" equalities nil )"bool" float nil )"bool" float nil )AND const-decl "[bool, bool -> bool]" booleans nil )"{x: (Fcanonic?(b)) | FtoR(x) = FtoR(f):: real AND Fexp(x) <= Fexp(f)}" nil )"bool" axpy nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil float nil )nil real_props nil )"[bool, bool -> bool]" booleans nil )nil float nil )nil float nil )nil float nil )"real" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil float nil )"float" float nil )nil float nil )"bool" float nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil ))nil 3320505812"" (skeep) (("" (rewrite "FcanonicBounded" ) nil nil )) nil )nil float nil )nil naturalnumbers nil )nil float nil )"Format" axpy nil )nil float nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"above(1)" axpy nil ))nil ))nil 3320505496"" (skeep)"" (expand * "MinOrMax?" "isMin?" )"" (skosimp*)"" (split)"1" (propax) nil nil )"2" (skosimp*)"2" (hide 2)"2" (lemma "FpredFsucc" :subst ("f" "f" "b" "b" ))"2" "FtoR(f!1)=FtoR(Fnormalize(b)(f!1))" )"1" (split)"1" (replace -1 1 :dir rl)"1" (rewrite "FpredProp" )"1" (hide 2 -1 -2)"1" (trans-ineq 1 "z" :strict 2)"1" (expand "abs" -4)"1" "FtoR(f)+Fulp(b)(f)" "1" (assert ) nil nil )"2" rewrite "FsuccDiff" :dir rl)"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "FsuccCanonic" ) nil nil ))nil ))nil )"2" (propax) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" float nil )"bool" axpy nil )"[T, T -> boolean]" equalities nil )"real" float nil )"bool" float nil )"bool" float nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )"{x: (Fcanonic?(b)) | FtoR(x) = FtoR(f):: real AND Fexp(x) <= Fexp(f)}" nil )nil float nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil float nil )"real" reals nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" float nil ) (< const-decl "bool" reals nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil float nil )"float" float nil )nil float nil )nil naturalnumbers nil )nil float nil )"Format" axpy nil )nil float nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"above(1)" axpy nil )"real" reals nil ))nil 3320506118"" (skeep) (("" (rewrite "FcanonicBounded" ) nil nil )) nil )nil float nil )nil naturalnumbers nil )nil float nil )"Format" axpy nil )nil float nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"above(1)" axpy nil ))nil ))nil 3320505840"" (skeep)"" (case "z <= FtoR(f)" )"1" (expand "abs" -4)"1" (grind-reals)"1" (expand * "MinOrMax?" "isMax?" )"1" (skosimp*)"1" (hide 1)"1" (lemma "FsuccFpred" :subst ("f" "f" "b" "b" ))"1" (split)"1" (replace -1 1 :dir rl)"1" "FtoR(f!1)=FtoR(Fnormalize(b)(f!1))" )"1" (rewrite "FsuccProp" )"1" (hide 2 -1 -2)"1" (trans-ineq 1 "z" :strict 1)"1" "FtoR[radix](f) -Fulp(b)(f)" "1" rewrite "FulpCanonic" )"1" "f=(# Fnum:=0, Fexp:=-dExp(b) #)" )"1" "1" expand * "Fpred" "FtoR" )"1" "1" "radix_less_vNum" )"1" "b" )"1" "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "FcanonicUnique" "b" "b" "p" "f" "q" "(# Fnum := 0, Fexp := -dExp(b) #)" ))"1" rewrite -3 :dir rl)"1" expand "FtoR" 1)"1" (assert ) nil nil ))nil ))nil )"2" "2" expand *"Fcanonic?" "Fsubnormal?" "Fbounded?" )"2" "2" expand "abs" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil )"2" (rewrite "FpredCanonic" ) nil nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (flip-ineq 1)"2" (expand * "MinOrMax?" "isMin?" )"2" (skosimp*)"2" (split)"1" (assert ) nil nil )"2" (skosimp*)"2" (expand "abs" -5)"2" (grind-reals)"2" (hide 2)"2" "FpredFsucc" :subst ("f" "f" "b" "b" ))"2" (split)"1" (replace -1 1 :dir rl)"1" "FtoR(f!1)=FtoR(Fnormalize(b)(f!1))" )"1" rewrite "FpredProp" )"1" "1" "z" :strict 2)"1" "FtoR(f)+Fulp(b)(f)" "1" (assert ) nil nil )"2" rewrite "FulpCanonic" )"2" "f=(# Fnum:=0, Fexp:=-dExp(b) #)" )"1" "1" expand * "Fsucc" "FtoR" )"1" "1" "1" "radix_less_vNum" )"1" "1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "FcanonicUnique" "b" "b" "p" "f" "q" "(# Fnum := 0, Fexp := -dExp(b) #)" ))"1" rewrite -4 :dir rl)"1" expand "FtoR" 1)"1" assert )nil nil ))nil ))nil )"2" "2" expand *"Fcanonic?" "Fsubnormal?" "Fbounded?" )"2" expand "abs" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "FsuccCanonic" )nil nil ))nil )"2" (assert ) nil nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" float nil )nil float nil )"above(1)" axpy nil )nil integers nil )"bool" reals nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil integers nil )"bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )nil float nil )nil naturalnumbers nil )nil float nil )"Format" axpy nil )"float" float nil )nil float nil )"bool" reals nil )nil float nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )nil float nil )"nonneg_rat" nil )nil real_props nil )"odd_int" integers nil )"bool" float nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"{j: nonneg_int | j >= i}" nil )nil real_props nil )"nzrat" rationalsnil )"nzint" integers nil )"nzrat" rationalsnil )nil real_props nil )"posrat" nil )"int" integers nil )"(total_order?[real])" nil )nil float nil )"int" integers nil )"int" integers nil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"real" float nil )nil float nil )"[T, T -> boolean]" equalities nil )"bool" float nil )"bool" float nil )AND const-decl "[bool, bool -> bool]" booleans nil )"{x: (Fcanonic?(b)) | FtoR(x) = FtoR(f):: real AND Fexp(x) <= Fexp(f)}" nil )"bool" axpy nil )"bool" float nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"bool" float nil )nil float nil )"[numfield, numfield -> numfield]" number_fields nil )"real" reals nil )nil real_props nil )"posrat" nil )nil float nil )"float" float nil )nil float nil )"real" reals nil )"(strict_total_order?[real])" real_props nil )"real" reals nil ))nil 3320498426"" (skeep) (("" (rewrite "FcanonicBounded" ) nil nil )) nil )nil float nil )nil naturalnumbers nil )nil float nil )"Format" axpy nil )nil float nil )nil numbers nil )nil booleans nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil booleans nil )"bool" reals nil )nil integers nil )"above(1)" axpy nil ))nil ))nil 3320498426"" (skeep)"" (expand * "FtoR" "abs" ) (("" (grind-reals) nil nil )) nil )) nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"real" float nil )nil real_props nil )nil real_props nil )"rat" rationals nil )"nnrat" exponentiation nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"int" integers nil )"(strict_total_order?[real])" real_props nil ))nil ))nil 3320498426"" (skosimp*) (("" (field -3) (("" (grind) nil nil )) nil )) nil )"rat" rationals nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"boolean" notequal nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil integers nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil integers nil )"above(1)" axpy nil )nil float nil )"nzrat" rationalsnil )"{j: nonneg_int | j >= i}" nil )"[T, T -> boolean]" equalities nil )nil extra_real_props nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"bool" functions nil )"(bijective?[T, T])" identity nil )"bool" booleans nil )"rat" rationals nil )"odd_int" integersnil )"int" integers nil )"(strict_total_order?[real])" real_props nil )"real" reals nil ))nil ))nil 3320498427"" (assert )"" (skeep)"" (assert )"" (case "0 < abs(Fnum(f))" )"1" (case "0 < 1 - 1 / (2 * abs(Fnum(f)))" )"1" (mult-by 2 "(1 - 1 / (2 * abs(Fnum(f))))" )"1" " abs(FtoR[radix](f)) * (1 - 1 / (2 * abs(Fnum(f)))) = ") "1" (move-terms 2 l 2)"1" (move-terms 2 r 1)"1" (trans-ineq 2 "abs(FtoR(f)-z)" )"1" (expand "abs" 1)"1" (grind-reals) nil nil )) nil )"2" (rewrite "ClosestUlp" )"2" (rewrite "FcanonicBounded" ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2 3)"2" (field 1)"2" (rewrite "FulpCanonic" )"2" (expand "FtoR" 1)"2" (rewrite "abs_mult" )"2" (expand "abs" 1 2)"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (case "1 <= abs(Fnum(f))" )"1" (field 1) nil nil )"2" (hide-all-but (-1 1)) (("2" (grind) nil nil )) nil ))nil ))nil )"2" (hide-all-but (1 2))"2" (expand * "abs" "FtoR" ) (("2" (grind-reals) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil float nil )"above(1)" axpy nil )nil integers nil )"bool" reals nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil integers nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"odd_int" integersnil )nil extra_real_propsnil )"int" integers nil )nil real_props nil )nil real_types nil )"real" float nil )"float[radix]" axpy nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil reals nil )nil float nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )"real" exponentiation nil )OR const-decl "[bool, bool -> bool]" booleans nil )nil real_props nil )"{r: nonneg_rat | r >= q}" nil )"{r: posrat | r >= q}" nil )"nonneg_rat" nil )"nzint" integers nil )"even_int" integers nil )"rat" rationals nil )"odd_int" integers nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )nil real_props nil )nil rationals nil )NOT const-decl "[bool -> bool]" booleans nil )"[numfield, numfield -> numfield]" number_fields nil )"bool" reals nil )"[bool, bool -> bool]" booleans nil )"real" reals nil )"nnreal" nil )nil real_props nil )nil real_props nil )nil real_props nil )"real" reals nil )nil float nil )nil float nil )"real" reals nil )"real" reals nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )nil float nil )"bool" float nil )"real" float nil )"Format" axpy nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"boolean" notequal nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil )"(total_order?[real])" nil )"real" reals nil )"{j: nonneg_int | j >= i}" nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"nzrat" rationalsnil )"rat" rationals nil ))nil 3320499635"" (skeep) (("" (field -3) nil nil )) nil )"{j: nonneg_int | j >= i}" nil )"nzrat" rationalsnil )"rat" rationals nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"boolean" notequal nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )nil real_types nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[numfield -> numfield]" number_fields nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )nil integers nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )"bool" reals nil )nil integers nil )"above(1)" axpy nil )nil float nil ))nil ))nil 3320499635"" (skeep)"" (case "0 < abs(Fnum(f))" )"1" (case "0 < 1 + 1 / (2 * abs(Fnum(f)))" )"1" (mult-by 2 "(1 + 1 / (2 * abs(Fnum(f))))" )"1" (assert )"1" " abs(FtoR[radix](f)) * (1 / (2 * abs(Fnum(f)))) = ") "1" (move-terms 2 r 1)"1" (trans-ineq 2 "abs(FtoR(f)-z)" )"1" (hide-all-but 1)"1" (expand "abs" ) (("1" (grind-reals) nil nil ))nil ))nil )"2" (rewrite "ClosestUlp" )"2" (rewrite "FcanonicBounded" ) nil nil )) nil ))nil ))nil )"2" (field 1)"2" (rewrite "FulpCanonic" )"2" (hide-all-but 1)"2" (expand * "abs" "FtoR" )"2" (grind-reals) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (field 1) nil nil ))nil )"2" (hide-all-but (1 2))"2" (expand * "abs" "FtoR" ) (("2" (grind-reals) nil nil ))nil ))nil ))nil ))nil )nil float nil )"above(1)" axpy nil )nil integers nil )"bool" reals nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil integers nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil ) (< const-decl "bool" reals nil )nil booleans nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil extra_real_propsnil )"real" reals nil )nil real_props nil )nil real_types nil )"real" float nil )"float[radix]" axpy nil )"(total_order?[real])" nil )"nzrat" rationalsnil )"{j: nonneg_int | j >= i}" nil )"(strict_total_order?[real])" real_props nil )"(strict_total_order?[real])" real_props nil )"(total_order?[real])" nil )nil real_props nil )nil reals nil )"Format" axpy nil )"real" float nil )"bool" float nil )nil float nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )"real" reals nil )nil float nil )nil float nil )"real" reals nil )"real" reals nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )nil float nil )"posrat" exponentiation nil )"nnrat" exponentiation nil )nil real_props nil )"rat" rationals nil )"rat" rationals nil )"int" integers nil )"bool" booleans nil )"(bijective?[T, T])" identity nil )"bool" functions nil )nil real_props nil )NOT const-decl "[bool -> bool]" booleans nil )"real" reals nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"rat" rationals nil )"[numfield, numfield -> numfield]" number_fields nil )"boolean" notequal nil )nil number_fields nil )"[numfield, nznum -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil real_props nil ))nil 3320510642 ("" (subtype-tcc) nil nil )"(strict_total_order?[real])" real_props nil )"{j: nonneg_int | j >= i}" nil )"nat" exponentiation nil )"(total_order?[real])" nil )nil exponent_props "reals/" )"above(1)" axpy nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )"posnat" float nil )"bool" float nil )"real" float nil )"bool" float nil )"boolean" notequal nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"rat" rationals nil )"rat" rationals nil )"real" reals nil ))nil ))nil 3320510940"" (skeep)"" (lemma "errorBoundedPlus" )"" (inst -1 "b" "f" "p" "q" )"" (split)"1" (skosimp*)"1" (case "FtoR(e!1)=0" )"1" (assert ) nil nil )"2" (hide 2)"2" (typepred "e!1" )"2" (expand "Fbounded?" -1)"2" (flatten)"2" (expand "FtoR" 1)"2" (case "abs(Fnum(e!1)) < 1" )"1" (grind-reals) nil nil )"2" (hide 2)"2" (mult-by 1 "radix ^ (-dExp(b))" )"2" "abs(FtoR[radix](f) - (FtoR[radix](p) + FtoR[radix](q)))" "1" "abs(FtoR(e!1))" )"1" expand "FtoR" 1)"1" rewrite "abs_mult" )"1" expand "abs" 1 3)"1" "1" rewrite "Exp_increq_1" )nil nil ))nil ))nil ))nil ))nil )"2" rewrite -3)"2" expand "abs" 1)"2" (grind-reals) nil nil ))nil ))nil ))nil )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (propax) nil nil ) ("3" (propax) nil nil )"4" (propax) nil nil ) ("5" (propax) nil nil ))nil ))nil ))nil ))nil )"above(1)" axpy nil )nil integers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil float nil )"bool" float nil )"real" float nil )"[T, T -> boolean]" equalities nil )"real" reals nil )"{k: int | k <= i AND k <= j}" nil )"(strict_total_order?[real])" real_props nil )"nnrat" exponentiation nil )"posrat" exponentiation nil )"int" integers nil )NOT const-decl "[bool -> bool]" booleans nil )"{n: nonneg_real | n >= m AND n >= -m}" real_defsnil )"[numfield -> numfield]" number_fields nil )nil number_fields nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil real_types nil )"bool" reals nil ) (< const-decl "bool" reals nil )"{j: nonneg_int | j >= i}" nil )"(divides(n))" divides nil )"(total_order?[real])" nil )"rat" rationals nil )nil real_props nil )nil extra_real_propsnil )OR const-decl "[bool, bool -> bool]" booleans nil )"boolean" notequal nil )"real" exponentiation nil )"(total_order?[real])" nil )"[numfield, numfield -> numfield]" number_fields nil )"posrat" nil )"nonneg_rat" nil )nil real_props nil )"{r: posrat | r >= q}" nil )"(strict_total_order?[real])" real_props nil )nil real_props nil )nil float nil )min const-decl "{p: real | p <= m AND p <= n}" real_defs nil )"bool" reals nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil float nil )"Format" axpy nil )nil float nil )nil naturalnumbers nil )quality 100%
¤ Dauer der Verarbeitung: 0.42 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
2026-03-28
