Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: ordered_int.pvs Sprache: Lisp

Original von: PVS^©

(fp_round_aux
(Exp_of_TCC1 0
 (Exp_of_TCC1-1 nil 3321197030 ("" (tcc :defs !) 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))
(Exp_of_TCC2 0
 (Exp_of_TCC2-1 nil 3321197030 ("" (tcc :defs !) 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)
 (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)
 (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)
 (real_minus_real_is_real application-judgement "real" reals nil)
 (int_minus_int_is_int application-judgement "int" integers nil)
 (posnat_expt application-judgement "posnat" exponentiation nil)
 (posint_times_posint_is_posint application-judgement "posint"
 integers nil)
 (mult_divides1 application-judgement "(divides(n))" divides nil)
 (mult_divides2 application-judgement "(divides(m))" divides nil)
 (expt def-decl "real" exponentiation nil)
 (^ const-decl "real" exponentiation nil)
 (/= const-decl "boolean" notequal nil)
 (minus_int_is_int application-judgement "int" integers nil))
 nil))
(Exp_of_TCC3 0
 (Exp_of_TCC3-1 nil 3321197030
 (""
 (inst +
 "lambda (px:posreal): choose({i:int|b^i<=px & px)
 (("1" (skosimp*)
 (("1" (rewrite "nonempty_member")
 (("1" (expand "member")
 (("1" (lemma "exp_of_exists")
 (("1" (inst - "b" "px!1") (("1" (assert) nil)))))))
 ("2" (skosimp*) (("2" (assert) nil)))
 ("3" (skosimp*) (("3" (assert) nil)))))))
 ("2" (skosimp*) (("2" (assert) nil)))
 ("3" (skosimp*) (("3" (assert) nil))))
 nil)
 ((real_le_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (nnrat_exp application-judgement "nnrat" exponentiation nil)
 (posrat_exp application-judgement "posrat" exponentiation nil)
 (member const-decl "bool" sets nil)
 (exp_of_exists formula-decl nil exponentiation nil)
 (nonempty_member formula-decl nil sets_lemmas nil)
 (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
 (choose const-decl "(p)" sets nil)
 (nonempty? const-decl "bool" sets nil)
 (set type-eq-decl nil sets nil)
 (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (numfield nonempty-type-eq-decl nil number_fields nil)
 (< const-decl "bool" reals nil)
 (b formal-const-decl "above(1)" fp_round_aux nil)
 (above nonempty-type-eq-decl nil integers nil)
 (^ const-decl "real" exponentiation nil)
 (/= const-decl "boolean" notequal nil)
 (OR const-decl "[bool, bool -> bool]" booleans nil)
 (<= const-decl "bool" reals nil)
 (AND const-decl "[bool, bool -> bool]" 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)
 (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_plus_int_is_int application-judgement "int" integers nil))
 nil))
(Exp_of_correct_TCC1 0
 (Exp_of_correct_TCC1-1 nil 3321197030 ("" (tcc :defs !) 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_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)
 (/= const-decl "boolean" notequal nil))
 nil))
(Exp_of_correct 0
 (Exp_of_correct-1 nil 3321197030
 ("" (skosimp*)
 (("" (typepred "Exp_of(x!1)")
 (("1" (rewrite "expt_inverse")
 (("1" (assert)
 (("1" (lemma "expt_pos")
 (("1" (inst?)
 (("1" (rewrite "times_div1")
 (("1" (ground)
 (("1" (rewrite "div_mult_pos_le2") nil)
 ("2" (rewrite "div_mult_pos_lt1")
 (("2" (rewrite "expt_plus")
 (("2" (rewrite "expt_x1") nil)))))))))))))))))
 ("2" (skosimp*) (("2" (assert) nil)))
 ("3" (skosimp*) (("3" (assert) nil))))))
 nil)
 ((Exp_of const-decl "{i: int | b ^ i <= x & x numfield]" number_fields nil)
 (numfield nonempty-type-eq-decl nil number_fields nil)
 (< const-decl "bool" reals nil)
 (AND const-decl "[bool, bool -> bool]" booleans nil)
 (posreal nonempty-type-eq-decl nil real_types nil)
 (nonneg_real nonempty-type-eq-decl nil real_types nil)
 (b formal-const-decl "above(1)" fp_round_aux nil)
 (above nonempty-type-eq-decl nil integers nil)
 (> const-decl "bool" reals nil)
 (^ const-decl "real" exponentiation nil)
 (>= const-decl "bool" reals nil)
 (/= const-decl "boolean" notequal nil)
 (OR const-decl "[bool, bool -> bool]" 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)
 (<= const-decl "bool" reals 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)
 (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)
 (posreal_times_posreal_is_posreal application-judgement "posreal"
 real_types nil)
 (int_plus_int_is_int application-judgement "int" integers nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (real_le_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)
 (div_mult_pos_le2 formula-decl nil real_props nil)
 (posrat_times_posrat_is_posrat application-judgement "posrat"
 rationals nil)
 (expt_plus formula-decl nil exponentiation nil)
 (int_minus_int_is_int application-judgement "int" integers nil)
 (posint_exp application-judgement "posint" exponentiation nil)
 (expt_x1 formula-decl nil exponentiation nil)
 (div_mult_pos_lt1 formula-decl nil real_props nil)
 (posreal_div_posreal_is_posreal application-judgement "posreal"
 real_types nil)
 (times_div1 formula-decl nil real_props nil)
 (nonzero_real nonempty-type-eq-decl nil reals nil)
 (expt_pos formula-decl nil exponentiation nil)
 (posrat_div_posrat_is_posrat application-judgement "posrat"
 rationals nil)
 (nnrat_exp application-judgement "nnrat" exponentiation nil)
 (posrat_exp application-judgement "posrat" exponentiation nil)
 (nzreal nonempty-type-eq-decl nil reals nil)
 (expt_inverse formula-decl nil exponentiation nil))
 nil))
(significand_TCC1 0
 (significand_TCC1-1 nil 3321197030 ("" (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)
 (nzreal nonempty-type-eq-decl nil reals nil)
 (/= const-decl "boolean" notequal nil))
 nil))
(significand_TCC2 0
 (significand_TCC2-1 nil 3321197030
 ("" (skosimp*)
 (("" (assert)
 (("" (use "pos_times_gt")
 (("" (use "expt_pos")
 (("" (assert)
 (("" (assert)
 (("" (rewrite "Exp_of_correct") nil))))))))))))
 nil)
 ((minus_int_is_int application-judgement "int" integers nil)
 (nnrat_exp application-judgement "nnrat" exponentiation nil)
 (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
 real_defs nil)
 (posreal_times_posreal_is_posreal application-judgement "posreal"
 real_types nil)
 (real_le_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (expt_pos formula-decl nil exponentiation nil)
 (Exp_of_correct formula-decl nil fp_round_aux 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)
 (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)
 (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)
 (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
 nil)
 (/= const-decl "boolean" notequal nil)
 (nzreal nonempty-type-eq-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)
 (OR const-decl "[bool, bool -> bool]" booleans nil)
 (^ const-decl "real" exponentiation nil)
 (> const-decl "bool" reals nil)
 (above nonempty-type-eq-decl nil integers nil)
 (b formal-const-decl "above(1)" fp_round_aux nil)
 (posreal nonempty-type-eq-decl nil real_types nil)
 (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
 (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (Exp_of const-decl "{i: int | b ^ i <= x & x < b ^ (i + 1)}"
 fp_round_aux nil)
 (pos_times_gt formula-decl nil real_props nil))
 nil))
(real_components_TCC1 0
 (real_components_TCC1-1 nil 3321197030 ("" (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)
 (nzreal nonempty-type-eq-decl nil reals nil)
 (/= const-decl "boolean" notequal nil)
 (E const-decl "integer" fp_round_aux nil))
 nil))
(real_components 0
 (real_components-1 nil 3321197030
 ("" (skosimp*)
 (("" (expand "significand")
 (("" (expand "E")
 (("" (rewrite "associative_mult" :dir rl)
 (("" (rewrite "associative_mult" :dir rl)
 (("" (rewrite "associative_mult" :dir rl)
 (("" (rewrite "expt_plus" :dir rl)
 (("" (rewrite "expt_x0")
 (("" (grind) nil))))))))))))))))
 nil)
 ((significand const-decl "norm_fp_range" fp_round_aux nil)
 (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
 real_defs nil)
 (associative_mult formula-decl nil number_fields 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)
 (numfield nonempty-type-eq-decl nil 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)
 (sgn const-decl "int" real_defs nil)
 (/= const-decl "boolean" notequal nil)
 (nzreal nonempty-type-eq-decl nil reals nil)
 (bool nonempty-type-eq-decl nil booleans nil)
 (>= const-decl "bool" reals 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)
 (OR const-decl "[bool, bool -> bool]" booleans nil)
 (^ const-decl "real" exponentiation nil)
 (> const-decl "bool" reals nil)
 (above nonempty-type-eq-decl nil integers nil)
 (b formal-const-decl "above(1)" fp_round_aux nil)
 (posreal nonempty-type-eq-decl nil real_types nil)
 (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
 (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (Exp_of const-decl "{i: int | b ^ i <= x & x < b ^ (i + 1)}"
 fp_round_aux nil)
 (posrat_exp application-judgement "posrat" exponentiation nil)
 (nnrat_exp application-judgement "nnrat" exponentiation nil)
 (posreal_times_posreal_is_posreal application-judgement "posreal"
 real_types nil)
 (real_times_real_is_real application-judgement "real" reals nil)
 (posrat_times_posrat_is_posrat application-judgement "posrat"
 rationals nil)
 (expt_x0 formula-decl nil exponentiation nil)
 (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
 real_types nil)
 (minus_odd_is_odd application-judgement "odd_int" integers nil)
 (real_ge_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
 nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (int_plus_int_is_int application-judgement "int" integers nil)
 (expt_plus formula-decl nil exponentiation nil)
 (minus_int_is_int application-judgement "int" integers nil)
 (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (E const-decl "integer" fp_round_aux nil))
 nil))
(abs_real_components 0
 (abs_real_components-1 nil 3321197030
 ("" (skosimp*)
 (("" (use "real_components")
 (("" (expand "abs")
 (("" (expand "sgn")
 (("" (lift-if) (("" (assert) (("" (ground) nil))))))))))))
 nil)
 ((real_components formula-decl nil fp_round_aux nil)
 (nzreal nonempty-type-eq-decl nil reals nil)
 (/= const-decl "boolean" notequal 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)
 (nnrat_exp application-judgement "nnrat" exponentiation nil)
 (posrat_exp application-judgement "posrat" exponentiation nil)
 (rat_times_rat_is_rat application-judgement "rat" rationals nil)
 (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
 real_defs nil)
 (posreal_times_posreal_is_posreal application-judgement "posreal"
 real_types nil)
 (sgn const-decl "int" real_defs 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)
 (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
 nil)
 (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
 real_types nil)
 (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
 nil))
 nil))
(Exp_of_unique_TCC1 0
 (Exp_of_unique_TCC1-1 nil 3321197030 ("" (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)
 (integer nonempty-type-from-decl nil integers 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)
 (real_le_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (nat_exp application-judgement "nat" exponentiation nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (int_plus_int_is_int application-judgement "int" integers nil)
 (/= const-decl "boolean" notequal nil))
 nil))
(Exp_of_unique_TCC2 0
 (Exp_of_unique_TCC2-1 nil 3321197030 ("" (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)
 (integer nonempty-type-from-decl nil integers 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_minus_real_is_real application-judgement "real" reals 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)
 (real_le_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (nat_exp application-judgement "nat" exponentiation nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (int_plus_int_is_int application-judgement "int" integers nil)
 (/= const-decl "boolean" notequal nil))
 nil))
(Exp_of_unique 0
 (Exp_of_unique-1 nil 3321197030
 ("" (skosimp*)
 (("" (case "b^i!1 < b^(1+j!1) & b^j!1 < b^(1+i!1)")
 (("1" (hide -2 -3 -4 -5)
 (("1" (flatten)
 (("1" (rewrite "both_sides_expt_gt1_lt")
 (("1" (rewrite "both_sides_expt_gt1_lt")
 (("1" (assert) nil)))))))))
 ("2" (assert) nil) ("3" (assert) nil) ("4" (assert) nil)
 ("5" (assert) nil) ("6" (assert) nil))))
 nil)
 ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (numfield nonempty-type-eq-decl nil number_fields nil)
 (integer nonempty-type-from-decl nil integers nil)
 (b formal-const-decl "above(1)" fp_round_aux nil)
 (above nonempty-type-eq-decl nil integers nil)
 (> const-decl "bool" reals nil)
 (^ const-decl "real" exponentiation nil)
 (>= const-decl "bool" reals nil)
 (/= const-decl "boolean" notequal nil)
 (OR const-decl "[bool, bool -> bool]" 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)
 (< const-decl "bool" reals 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)
 (number nonempty-type-decl nil numbers nil)
 (AND const-decl "[bool, bool -> bool]" booleans nil)
 (bool nonempty-type-eq-decl nil booleans nil)
 (boolean nonempty-type-decl nil booleans nil)
 (int_plus_int_is_int application-judgement "int" integers nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (nnrat_exp application-judgement "nnrat" exponentiation nil)
 (posrat_exp application-judgement "posrat" exponentiation nil)
 (real_ge_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
 (both_sides_expt_gt1_lt formula-decl nil exponentiation nil)
 (nonneg_real nonempty-type-eq-decl nil real_types nil)
 (posreal nonempty-type-eq-decl nil real_types nil)
 (real_gt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (real_le_is_total_order name-judgement "(total_order?[real])"
 real_props nil))
 nil))
(posreal_exponent 0
 (posreal_exponent-1 nil 3321197030
 ("" (skosimp*)
 (("" (expand "E")
 (("" (expand "abs")
 (("" (lemma "Exp_of_unique")
 (("" (inst - "Exp_of(x!1)" "i!1" "x!1")
 (("" (assert)
 (("" (hide 2)
 (("" (replace -1)
 (("" (hide -1)
 (("" (split)
 (("1" (assert) nil nil) ("2" (assert) nil nil)
 ("3" (rewrite "commutative_mult")
 (("3" (rewrite "div_mult_pos_le1" :dir rl) nil
 nil))
 nil)
 ("4" (rewrite "commutative_mult")
 (("4" (rewrite "div_mult_pos_lt2" :dir rl)
 (("4" (rewrite "expt_div")
 (("4" (rewrite "expt_x1")
 (("4" (assert) nil nil)) nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil))
 nil)
 ((E const-decl "integer" fp_round_aux nil)
 (Exp_of_unique formula-decl nil fp_round_aux nil)
 (int_plus_int_is_int application-judgement "int" integers nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (posrat_exp application-judgement "posrat" exponentiation nil)
 (real_le_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (nnrat_exp application-judgement "nnrat" exponentiation nil)
 (posreal_times_posreal_is_posreal application-judgement "posreal"
 real_types nil)
 (posrat_div_posrat_is_posrat application-judgement "posrat"
 rationals nil)
 (div_mult_pos_le1 formula-decl nil real_props nil)
 (commutative_mult formula-decl nil number_fields nil)
 (norm_fp_range type-eq-decl nil fp_round_aux nil)
 (div_mult_pos_lt2 formula-decl nil real_props nil)
 (expt_x1 formula-decl nil exponentiation nil)
 (int_minus_int_is_int application-judgement "int" integers nil)
 (expt_div formula-decl nil exponentiation nil)
 (nzreal nonempty-type-eq-decl nil reals nil)
 (Exp_of const-decl "{i: int | b ^ i <= x & x numfield]" number_fields nil)
 (numfield nonempty-type-eq-decl nil number_fields nil)
 (< const-decl "bool" reals nil)
 (b formal-const-decl "above(1)" fp_round_aux nil)
 (above nonempty-type-eq-decl nil integers nil)
 (^ const-decl "real" exponentiation nil)
 (/= const-decl "boolean" notequal nil)
 (OR const-decl "[bool, bool -> bool]" booleans nil)
 (<= const-decl "bool" reals nil)
 (AND const-decl "[bool, bool -> bool]" booleans nil)
 (int 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)
 (>= const-decl "bool" reals nil)
 (bool nonempty-type-eq-decl nil booleans nil)
 (integer nonempty-type-from-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)
 (boolean nonempty-type-decl nil booleans nil)
 (number nonempty-type-decl nil numbers nil)
 (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
 nil))
 nil))
(real_exponent 0
 (real_exponent-1 nil 3321197030
 ("" (skosimp*)
 (("" (lemma "posreal_exponent")
 (("" (inst - "i!1" "n1!1" "abs(z!1)")
 (("" (expand "E")
 (("" (expand "sgn")
 (("" (expand "abs")
 (("" (lift-if)
 (("" (lift-if)
 (("" (assert) (("" (ground) nil))))))))))))))))))
 nil)
 ((posreal_exponent formula-decl nil fp_round_aux nil)
 (nnrat_exp application-judgement "nnrat" exponentiation nil)
 (posrat_exp application-judgement "posrat" exponentiation nil)
 (E const-decl "integer" fp_round_aux nil)
 (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
 nil)
 (posreal_times_posreal_is_posreal application-judgement "posreal"
 real_types nil)
 (real_ge_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
 real_types nil)
 (sgn const-decl "int" real_defs nil)
 (nzreal nonempty-type-eq-decl nil reals nil)
 (/= const-decl "boolean" notequal 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)
 (norm_fp_range type-eq-decl nil fp_round_aux nil)
 (b formal-const-decl "above(1)" fp_round_aux nil)
 (above nonempty-type-eq-decl nil integers nil)
 (int nonempty-type-eq-decl nil integers nil)
 (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
 (AND const-decl "[bool, bool -> bool]" booleans 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)
 (integer nonempty-type-from-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)
 (boolean nonempty-type-decl nil booleans nil)
 (number nonempty-type-decl nil numbers nil)
 (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
 real_defs nil))
 nil))
(scale_TCC1 0
 (scale_TCC1-1 nil 3321197030 ("" (tcc :defs !) 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)
 (int_minus_int_is_int application-judgement "int" integers nil))
 nil))
(scale_TCC2 0
 (scale_TCC2-1 nil 3321197030 ("" (tcc :defs !) 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)
 (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)
 (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)
 (posnat_expt application-judgement "posnat" exponentiation nil)
 (posint_times_posint_is_posint application-judgement "posint"
 integers nil)
 (mult_divides1 application-judgement "(divides(n))" divides nil)
 (mult_divides2 application-judgement "(divides(m))" divides nil)
 (expt def-decl "real" exponentiation nil)
 (^ const-decl "real" exponentiation nil)
 (/= const-decl "boolean" notequal nil)
 (int_minus_int_is_int application-judgement "int" integers nil)
 (int_plus_int_is_int application-judgement "int" integers nil)
 (minus_int_is_int application-judgement "int" integers nil))
 nil))
(scale_TCC3 0
 (scale_TCC3-1 nil 3321197030
 ("" (skosimp*)
 (("" (assert) (("" (typepred "Exp_of(x!1)") (("" (assert) nil))))))
 nil)
 ((int_minus_int_is_int application-judgement "int" integers 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)
 (real_le_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props 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)
 (OR const-decl "[bool, bool -> bool]" booleans nil)
 (/= const-decl "boolean" notequal nil)
 (>= const-decl "bool" reals nil)
 (^ const-decl "real" exponentiation nil)
 (> const-decl "bool" reals nil)
 (above nonempty-type-eq-decl nil integers nil)
 (b formal-const-decl "above(1)" fp_round_aux nil)
 (nonneg_real nonempty-type-eq-decl nil real_types nil)
 (posreal nonempty-type-eq-decl nil real_types nil)
 (AND const-decl "[bool, bool -> bool]" booleans nil)
 (< const-decl "bool" reals nil)
 (numfield nonempty-type-eq-decl nil number_fields nil)
 (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (Exp_of const-decl "{i: int | b ^ i <= x & x < b ^ (i + 1)}"
 fp_round_aux nil))
 nil))
(scale_correct_TCC1 0
 (scale_correct_TCC1-1 nil 3321197030 ("" (tcc :defs !) nil nil)
 ((/= const-decl "boolean" notequal nil)) nil))
(scale_correct_TCC2 0
 (scale_correct_TCC2-1 nil 3321197030 ("" (tcc :defs !) 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_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)
 (/= const-decl "boolean" notequal nil)
 (scale const-decl
 "{i: int | b ^ (i + p - 1) <= x & x < b ^ (i + p)}"
 fp_round_aux nil)
 (int_plus_int_is_int application-judgement "int" integers nil))
 nil))
(scale_correct_TCC3 0
 (scale_correct_TCC3-1 nil 3321197030
 ("" (skosimp*) (("" (assert) nil nil)) nil)
 ((posreal_div_posreal_is_posreal application-judgement "posreal"
 real_types nil)
 (posrat_exp application-judgement "posrat" exponentiation nil)
 (nnrat_exp application-judgement "nnrat" 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))
 nil))
(scale_correct 0
 (scale_correct-1 nil 3321197030
 ("" (skosimp*)
 (("" (prop)
 (("1" (rewrite "div_mult_pos_le2")
 (("1" (expand "scale")
 (("1" (lemma "expt_plus")
 (("1" (inst - "p-1" "1+Exp_of(x!1)-p" "b")
 (("1" (assert) nil)))))))
 ("2" (lemma "expt_pos")
 (("2" (inst?) (("2" (assert) nil)))))))
 ("2" (rewrite "div_mult_pos_lt1")
 (("1" (rewrite "expt_plus" :dir rl)
 (("1" (expand "scale") (("1" (assert) nil)))))
 ("2" (lemma "expt_pos")
 (("2" (inst?) (("2" (assert) nil))))))))))
 nil)
 ((nzreal nonempty-type-eq-decl nil reals nil)
 (Exp_of const-decl "{i: int | b ^ i <= x & x < b ^ (i + 1)}"
 fp_round_aux nil)
 (int_plus_int_is_int application-judgement "int" integers nil)
 (expt_plus formula-decl nil exponentiation nil)
 (real_le_is_total_order name-judgement "(total_order?[real])"
 real_props nil)
 (posrat_times_posrat_is_posrat application-judgement "posrat"
 rationals nil)
 (scale const-decl
 "{i: int | b ^ (i + p - 1) <= x & x numfield]" number_fields nil)
 (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (numfield nonempty-type-eq-decl nil number_fields nil)
 (<= const-decl "bool" reals nil)
 (AND const-decl "[bool, bool -> bool]" booleans nil)
 (b formal-const-decl "above(1)" fp_round_aux nil)
 (above nonempty-type-eq-decl nil integers nil)
 (^ const-decl "real" exponentiation nil)
 (/= const-decl "boolean" notequal nil)
 (OR const-decl "[bool, bool -> bool]" 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)
 (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)
 (div_mult_pos_le2 formula-decl nil real_props nil)
 (posrat_exp application-judgement "posrat" exponentiation nil)
 (nnrat_exp application-judgement "nnrat" exponentiation nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (posint_exp application-judgement "posint" exponentiation nil)
 (div_mult_pos_lt1 formula-decl nil real_props nil)
 (int_minus_int_is_int application-judgement "int" integers nil))
 nil))
(round_scaled_TCC1 0
 (round_scaled_TCC1-1 nil 3321197030 ("" (tcc :defs !) 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)
 (nzreal nonempty-type-eq-decl nil reals nil)
 (/= const-decl "boolean" notequal nil)
 (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
 nil)
 (scale const-decl
 "{i: int | b ^ (i + p - 1) <= x & x < b ^ (i + p)}"
 fp_round_aux nil)
 (int_minus_int_is_int application-judgement "int" integers nil))
 nil))
(round_scaled_TCC2 0
 (round_scaled_TCC2-1 nil 3321197030 ("" (tcc :defs !) 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)
 (nzreal nonempty-type-eq-decl nil reals nil)
 (/= const-decl "boolean" notequal nil)
 (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
 nil)
 (scale const-decl
 "{i: int | b ^ (i + p - 1) <= x & x < b ^ (i + p)}"
 fp_round_aux nil)
 (int_minus_int_is_int application-judgement "int" integers nil))
 nil))
(truncate_TCC1 0
 (truncate_TCC1-1 nil 3321197030 ("" (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)
 (integer nonempty-type-from-decl nil integers nil)
 (< const-decl "bool" reals nil)
 (int nonempty-type-eq-decl nil integers nil)
 (>= const-decl "bool" reals nil)
 (nat nonempty-type-eq-decl nil naturalnumbers nil)
 (> const-decl "bool" reals nil)
 (above nonempty-type-eq-decl nil integers nil)
 (p formal-const-decl "above(1)" fp_round_aux nil)
 (below type-eq-decl nil naturalnumbers nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (/= const-decl "boolean" notequal nil))
 nil))
(truncate_shift 0
 (truncate_shift-1 nil 3321197030
 ("" (skosimp*)
 (("" (apply-extensionality)
 (("1" (hide 2)
 (("1" (expand "truncate")
 (("1" (rewrite "associative_mult")
 (("1" (rewrite "expt_plus" :dir rl) nil)))))))
 ("2" (hide 2)
 (("2" (use "expt_pos")
 (("2" (rewrite "pos_times_ge") (("2" (assert) 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)
 (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)
 (< const-decl "bool" reals nil) (> const-decl "bool" reals nil)
 (above nonempty-type-eq-decl nil integers nil)
 (p formal-const-decl "above(1)" fp_round_aux nil)
 (below type-eq-decl nil naturalnumbers nil)
 (b formal-const-decl "above(1)" fp_round_aux nil)
 (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (posreal nonempty-type-eq-decl nil real_types nil)
 (^ const-decl "real" exponentiation nil)
 (/= const-decl "boolean" notequal nil)
 (OR const-decl "[bool, bool -> bool]" booleans nil)
 (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (numfield nonempty-type-eq-decl nil number_fields nil)
 (truncate const-decl "[below(p) -> below(b)]" fp_round_aux nil)
 (nonneg_real nonempty-type-eq-decl nil real_types nil)
 (integer nonempty-type-from-decl nil integers nil)
 (posreal_times_posreal_is_posreal application-judgement "posreal"
 real_types nil)
 (int_minus_int_is_int application-judgement "int" integers nil)
 (nnrat_exp application-judgement "nnrat" exponentiation nil)
 (posrat_exp application-judgement "posrat" exponentiation nil)
 (int_plus_int_is_int application-judgement "int" integers nil)
 (nzreal nonempty-type-eq-decl nil reals nil)
 (expt_plus formula-decl nil exponentiation nil)
 (posrat_times_posrat_is_posrat application-judgement "posrat"
 rationals nil)
 (associative_mult formula-decl nil number_fields nil))
 nil))
(Exp_of_shift 0
 (Exp_of_shift-1 nil 3321197030
 ("" (skosimp*)
 (("" (lemma "Exp_of_unique")
 (("" (use "expt_pos")
 (("1" (inst?)
 (("1" (inst - "b^j!1*px!1")
 (("1" (assert)
 (("1" (hide 2)
 (("1" (rewrite "commutative_mult")
 (("1" (rewrite "div_mult_pos_le1" :dir rl)
 (("1" (rewrite "div_mult_pos_lt2" :dir rl)
 (("1" (rewrite "expt_div")
 (("1" (rewrite "expt_div")
 (("1" (assert) nil)))))))))))))))
 ("2" (use "pos_times_gt")
 (("1" (assert) (("1" (assert) nil))) ("2" (assert) nil)))
 ("3" (assert) nil)))
 ("2" (use "pos_times_gt")
 (("1" (assert) (("1" (assert) nil))) ("2" (assert) nil)))
 ("3" (assert) nil)))
 ("2" (assert) nil))))))
 nil)
 ((Exp_of_unique formula-decl nil fp_round_aux nil)
 (int_plus_int_is_int application-judgement "int" integers nil)
 (posreal_times_posreal_is_posreal application-judgement "posreal"
 real_types nil)
 (AND const-decl "[bool, bool -> bool]" booleans nil)
 (<= const-decl "bool" reals nil)
 (OR const-decl "[bool, bool -> bool]" booleans nil)
 (/= const-decl "boolean" notequal nil)
 (^ const-decl "real" exponentiation nil)
 (< const-decl "bool" reals nil)
 (numfield nonempty-type-eq-decl nil number_fields nil)
 (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
 (Exp_of const-decl "{i: int | b ^ i <= x & x numfield]" number_fields nil)
 (real_lt_is_strict_total_order name-judgement
 "(strict_total_order?[real])" real_props nil)
 (real_le_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)
 (commutative_mult formula-decl nil number_fields nil)
 (div_mult_pos_lt2 formula-decl nil real_props nil)
 (int_minus_int_is_int application-judgement "int" integers nil)
 (expt_div formula-decl nil exponentiation nil)
 (nzreal nonempty-type-eq-decl nil reals nil)
 (posrat_div_posrat_is_posrat application-judgement "posrat"
 rationals nil)
 (div_mult_pos_le1 formula-decl nil real_props nil)
 (real_ge_is_total_order name-judgement "(total_order?[real])"
 real_props 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)
 (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)
 (integer nonempty-type-from-decl nil integers nil)
 (bool nonempty-type-eq-decl nil booleans 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)
 (above nonempty-type-eq-decl nil integers nil)
 (b formal-const-decl "above(1)" fp_round_aux nil)
 (expt_pos formula-decl nil exponentiation nil)
 (posrat_exp application-judgement "posrat" exponentiation nil)
 (nnrat_exp application-judgement "nnrat" exponentiation nil))
 nil))
(scale_shift 0
 (scale_shift-1 nil 3321197030
 ("" (skosimp*)
 (("" (expand "scale") (("" (rewrite "Exp_of_shift") nil)))) nil)
 ((scale const-decl
 "{i: int | b ^ (i + p - 1) <= x & x 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)
 (integer nonempty-type-from-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)
 (boolean nonempty-type-decl nil booleans nil)
 (number nonempty-type-decl nil numbers nil)
 (Exp_of_shift formula-decl nil fp_round_aux 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)
 (int_minus_int_is_int application-judgement "int" integers nil))
 nil)))

¤ Dauer der Verarbeitung: 0.97 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

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.