Quelle  fp_round_aux.prf   Sprache: Lisp

(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<b^(i+1)})")
    (("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 < b ^ (i + 1)}"
     fp_round_aux 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)
    (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 < b ^ (i + 1)}"
     fp_round_aux 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)
    (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 < b ^ (i + p)}"
           fp_round_aux nil)
    (< const-decl "bool" reals nil)
    (p formal-const-decl "above(1)" fp_round_aux nil)
    (- const-decl "[numfield, numfield -> 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 < b ^ (i + 1)}"
     fp_round_aux nil)
    (* const-decl "[numfield, numfield -> 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 < b ^ (i + p)}"
           fp_round_aux 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)
    (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)))