Quelle log_nat.prf Sprache: Lisp

(log_nat
(log_nat_TCC1 0
  (log_nat_TCC1-1 nil 3321008812 ("" (subtype-tcc) nil nil) nil nil))
(log_nat_TCC2 0
  (log_nat_TCC2-1 nil 3321008812 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
(log_nat_TCC3 0
  (log_nat_TCC3-1 nil 3321008812
   ("" (skeep) (("" (rewrite "expt_x0") (("" (assert) nil nil)) nil))
    nil)
   ((expt_x0 formula-decl nil exponentiation 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)
    (above nonempty-type-eq-decl nil integers nil)
    (posint_exp application-judgement "posint" exponentiation nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
(log_nat_TCC4 0
  (log_nat_TCC4-1 nil 3321008812
   ("" (skeep)
    (("" (skosimp*)
      (("" (typepred "y!1")
        (("" (assert)
          (("" (cross-mult -3)
            (("" (rewrite "expt_plus")
              (("" (assert)
                (("" (rewrite "expt_x1") (("" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals 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)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (expt_plus formula-decl nil exponentiation nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (expt_x1 formula-decl nil exponentiation nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (div_cancel3 formula-decl nil 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (above nonempty-type-eq-decl nil integers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (^ const-decl "real" exponentiation nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (posint_exp application-judgement "posint" exponentiation nil))
   nil))
(log_nat_TCC5 0
  (log_nat_TCC5-1 nil 3321008812
   ("" (skosimp :preds? t)
    (("" (typepred "floor(x!1/p!1)")
      (("" (case "x!1/p!1 < floor(x!1)")
        (("1" (assert) (("1" (cross-mult 2) nil nil)) nil)
         ("2" (typepred "floor(x!1)")
          (("2" (cross-mult 1)
            (("2" (case "1 + floor(x!1) < floor(x!1) * p!1")
              (("1" (assert) nil nil)
               ("2" (move-terms 1 l 2)
                (("2" (factor 1)
                  (("2" (div-by 1 "(p!1 - 1)")
                    (("2" (case "1 / (p!1 - 1) < 1")
                      (("1" (case "1 <= floor(x!1)")
                        (("1" (assert) nil nil) ("2" (assert) nil nil))
                        nil)
                       ("2" (cross-mult 1) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil 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)
    (integer nonempty-type-from-decl nil integers nil)
    (<= const-decl "bool" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals
     nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (times_div_cancel2 formula-decl nil extra_real_props nil)
    (both_sides_div_pos_lt1 formula-decl nil real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (div_mult_pos_lt1 formula-decl nil real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_plus_int_is_int application-judgement "int" integers 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)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (div_mult_pos_ge1 formula-decl nil 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) (> 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)
    (above nonempty-type-eq-decl nil integers nil))
   nil))
(log_nat_TCC6 0
  (log_nat_TCC6-2 nil 3399807171
   ("" (skosimp :preds? t)
    (("" (lemma "floor_lt_floor_int")
      (("" (inst?) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((floor_lt_floor_int formula-decl nil prelude_aux nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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)
    (nat nonempty-type-eq-decl nil naturalnumbers 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) (> 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)
    (above nonempty-type-eq-decl nil integers nil))
   nil)
  (log_nat_TCC6-1 nil 3321008812
   ("" (skosimp :preds? t)
    (("" (split)
      (("1" (beta)
        (("1" (typepred "v!1(x!1 / p!1, p!1)`2")
          (("1" (propax) nil nil)
           ("2" (cross-mult) (("2" (assert) nil nil)) nil))
          nil))
        nil)
       ("2" (beta)
        (("2" (typepred "v!1(x!1 / p!1, p!1)`2")
          (("1" (cross-mult -3)
            (("1" (rewrite "expt_plus")
              (("1" (rewrite "expt_x1") (("1" (assert) nil nil)) nil))
              nil))
            nil)
           ("2" (cross-mult) (("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   nil nil))
(log_nat_bounds_TCC1 0
  (log_nat_bounds_TCC1-1 nil 3321012239 ("" (subtype-tcc) nil nil)
   ((posint_exp application-judgement "posint" exponentiation nil))
   nil))
(log_nat_bounds_TCC2 0
  (log_nat_bounds_TCC2-1 nil 3321012239 ("" (subtype-tcc) nil nil)
   ((^ const-decl "real" exponentiation nil)
    (posint_exp application-judgement "posint" exponentiation nil))
   nil))
(log_nat_bounds 0
  (log_nat_bounds-1 nil 3321012239
   ("" (skeep)
    (("" (beta)
      (("" (typepred "log_nat(x, p)`2")
        (("" (name-replace "yy" "log_nat(x, p)`2")
          (("" (name-replace "nn" " log_nat(x, p)`1")
            (("" (replace -3)
              (("" (split)
                (("1" (cancel-by 1 "p ^ nn") nil nil)
                 ("2" (rewrite "expt_plus")
                  (("2" (rewrite "expt_x1")
                    (("2" (cancel-by 1 "p ^ nn") nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nzreal nonempty-type-eq-decl nil reals nil)
    (expt_plus formula-decl nil exponentiation nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (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)
    (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
     nil)
    (expt_x1 formula-decl nil exponentiation 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)
    (posrat_times_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (both_sides_times_pos_le1 formula-decl nil real_props nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (posint nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (real_times_real_is_real application-judgement "real" reals 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)
    (> const-decl "bool" reals nil)
    (above nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (log_nat def-decl "[n: nat, {y | y < p AND x = p ^ n * y}]" log_nat
     nil)
    (posint_exp application-judgement "posint" exponentiation nil))
   shostak))
(log_nat_incr 0
  (log_nat_incr-1 nil 3321011017
   ("" (skeep :preds? t)
    (("" (lemma "log_nat_bounds")
      (("" (inst-cp -1 "p" "x")
        (("" (inst -1 "p" "y")
          (("" (beta)
            (("" (flatten)
              (("" (name-replace "xx" "log_nat(x, p)`1")
                (("" (name-replace "yy" "log_nat(y, p)`1")
                  (("" (lemma "both_sides_expt_gt1_lt")
                    (("" (inst -1 "p" "xx" "yy")
                      (("" (assert)
                        (("" (hide 2)
                          (("" (mult-by -3 "p")
                            (("" (rewrite "expt_plus" -3)
                              ((""
                                (rewrite "expt_x1" -3)
                                ((""
                                  (mult-by 1 "p")
                                  (("" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((log_nat_bounds formula-decl nil log_nat nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (expt_plus formula-decl nil exponentiation nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
     nil)
    (expt_x1 formula-decl nil exponentiation nil)
    (both_sides_times_pos_le1_imp formula-decl nil extra_real_props
     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)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (both_sides_expt_gt1_lt formula-decl nil exponentiation nil)
    (log_nat def-decl "[n: nat, {y | y < p AND x = p ^ n * y}]" log_nat
     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)
    (< const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (>= const-decl "bool" reals nil)
    (above nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (posint_exp application-judgement "posint" exponentiation nil))
   shostak))
(log_nat_itaux_TCC1 0
  (log_nat_itaux_TCC1-1 nil 3544887262 ("" (subtype-tcc) nil nil) nil
   nil))
(log_nat_itaux_TCC2 0
  (log_nat_itaux_TCC2-1 nil 3544887262 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil) (> 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)
    (above nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posnat_expt application-judgement "posnat" exponentiation nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posint_exp application-judgement "posint" exponentiation nil))
   nil))
(log_nat_itaux_TCC3 0
  (log_nat_itaux_TCC3-1 nil 3544887262
   ("" (skeep :preds? t) (("" (assert) nil nil)) nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_times_real_is_real application-judgement "real" reals 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)
    (posint_exp application-judgement "posint" exponentiation nil))
   nil))
(log_nat_itaux_TCC4 0
  (log_nat_itaux_TCC4-1 nil 3544887262
   ("" (skeep :preds? t)
    (("" (grind-reals)
      (("" (rewrite "expt_plus")
        (("" (rewrite "expt_x1") (("" (assert) nil nil)) nil)) nil))
      nil))
    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_times_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props 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)
    (div_mult_pos_ge1 formula-decl nil real_props nil)
    (div_cancel4 formula-decl nil real_props nil)
    (times_div1 formula-decl nil real_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (both_sides_times1 formula-decl nil real_props nil)
    (expt_x1 formula-decl nil exponentiation nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (above nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (expt_plus formula-decl nil exponentiation nil)
    (posint_exp application-judgement "posint" exponentiation nil))
   nil))
(log_nat_itaux_TCC5 0
  (log_nat_itaux_TCC5-1 nil 3544887262
   ("" (skeep :preds? t)
    (("" (lemma "log_nat_TCC6")
      (("" (inst?) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((log_nat_TCC6 termination-tcc nil log_nat nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_times_real_is_real application-judgement "real" reals 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (above nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals 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)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (posint_exp application-judgement "posint" exponentiation nil))
   nil))
(log_nat_it_TCC1 0
  (log_nat_it_TCC1-1 nil 3544887262
   ("" (skeep) (("" (rewrite "expt_x0") (("" (assert) nil nil)) nil))
    nil)
   ((expt_x0 formula-decl nil exponentiation 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)
    (above nonempty-type-eq-decl nil integers nil)
    (posint_exp application-judgement "posint" exponentiation nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
(log_nat_id 0
  (log_nat_id-1 nil 3544887270
   ("" (skeep)
    (("" (expand "log_nat_it")
      (("" (typepred "log_nat_itaux(x, p, 0, x)`2")
        (("" (typepred "log_nat(x,p)`2")
          (("" (name-replace "log1" "log_nat(x,p)")
            (("" (name-replace "log2" "log_nat_itaux(x,p,0,x)")
              (("" (replaces -3)
                ((""
                  (case "FORALL (A,C:nat,B,D:real): B>=1 AND B

=1 AND D

=C AND (p^A)*B = (p^C)*D IMPLIES A = C AND B = D")
                  (("1" (inst-cp - "log1`1" "log2`1" "log1`2" "log2`2")
                    (("1" (inst - "log2`1" "log1`1" "log2`2" "log1`2")
                      (("1" (assert)
                        (("1" (decompose-equality +) nil nil)) nil))
                      nil))
                    nil)
                   ("2" (hide-all-but 1)
                    (("2" (skeep)
                      (("2" (case "p^(A-C)*B = D")
                        (("1" (case "A = C")
                          (("1" (replace -1)
                            (("1" (assert)
                              (("1"
                                (mult-by 1 "p^C")
                                (("1" (assert) nil nil))
                                nil))
                              nil))
                            nil)
                           ("2" (assert)
                            (("2" (hide 2)
                              (("2"
                                (expand "^" -1)
                                (("2"
                                  (expand "expt")
                                  (("2"
                                    (case "expt(p, A - 1 - C) * B>=1")
                                    (("1"
                                      (mult-by -1 "p")
                                      (("1" (assert) nil nil))
                                      nil)
                                     ("2"
                                      (hide -1)
                                      (("2"
                                        (case "expt(p,A-1-C)>=1")
                                        (("1"
                                          (mult-by -1 "B")
                                          (("1" (assert) nil nil))
                                          nil)
                                         ("2"
                                          (hide 2)
                                          (("2"
                                            (lemma "expt_ge1")
                                            (("2"
                                              (inst - "p" "A-1-C")
                                              (("2"
                                                (expand "^")
                                                (("2"
                                                  (propax)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (mult-by 1 "p^C")
                          (("2" (lemma "expt_plus")
                            (("2" (inst - "A-C" "C" "p")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((log_nat_it const-decl "[n: nat, {y | y < p AND x = p ^ n * y}]"
     log_nat nil)
    (log_nat def-decl "[n: nat, {y | y < p AND x = p ^ n * y}]" log_nat
     nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans 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 nonempty-type-eq-decl nil reals nil)
    (posrat_exp application-judgement "posrat" exponentiation nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (posrat_times_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (expt_plus formula-decl nil exponentiation nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (both_sides_times1 formula-decl nil real_props nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (nnrat_exp application-judgement "nnrat" exponentiation nil)
    (expt def-decl "real" exponentiation nil)
    (expt_ge1 formula-decl nil exponentiation nil)
    (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
     nil)
    (nonneg_real nonempty-type-eq-decl nil real_types 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)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (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)
    (> const-decl "bool" reals nil)
    (above nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (log_nat_itaux def-decl "[n: nat, {y | y < p AND x = p ^ n * y}]"
     log_nat nil)
    (posint_exp application-judgement "posint" exponentiation nil))
   shostak))
(least_pow_2_ge_TCC1 0
  (least_pow_2_ge_TCC1-1 nil 3609934857
   ("" (skeep)
    (("" (skeep)
      (("" (typepred "y")
        (("" (rewrite "log_nat_id")
          (("" (splash +)
            (("1" (replace -6)
              (("1" (assert)
                (("1" (replace -4)
                  (("1" (hide -)
                    (("1" (skeep)
                      (("1" (case "FORALL (k:nat): 2^i < 2^(i+1+k)")
                        (("1" (inst - "n-i-1")
                          (("1" (assert) nil nil)
                           ("2" (assert) nil nil))
                          nil)
                         ("2" (hide-all-but 1)
                          (("2" (induct "k")
                            (("1" (assert)
                              (("1"
                                (expand "^")
                                (("1"
                                  (lift-if)
                                  (("1"
                                    (lift-if)
                                    (("1"
                                      (lift-if)
                                      (("1"
                                        (assert)
                                        (("1"
                                          (ground)
                                          (("1"
                                            (expand "expt" + 2)
                                            (("1" (assert) nil nil))
                                            nil)
                                           ("2"
                                            (case "NOT i = -1")
                                            (("1" (assert) nil nil)
                                             ("2"
                                              (replaces -1)
                                              (("2"
                                                (assert)
                                                (("2"
                                                  (case "NOT --1 = 1")
                                                  (("1"
                                                    (assert)
                                                    nil
                                                    nil)
                                                   ("2"
                                                    (replace -1)
                                                    (("2"
                                                      (assert)
                                                      (("2"
                                                        (expand
                                                         "expt"
                                                         1)
                                                        (("2"
                                                          (expand
                                                           "expt"
                                                           1)
                                                          (("2"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("3"
                                            (expand "expt" + 1)
                                            (("3" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (skeep)
                              (("2"
                                (assert)
                                (("2"
                                  (expand "^")
                                  (("2"
                                    (lift-if)
                                    (("2"
                                      (lift-if)
                                      (("2"
                                        (lift-if)
                                        (("2"
                                          (assert)
                                          (("2"
                                            (ground)
                                            (("1"
                                              (expand "expt" + 2)
                                              (("1" (assert) nil nil))
                                              nil)
                                             ("2"
                                              (expand "expt" + 2)
                                              (("2" (assert) nil nil))
                                              nil)
                                             ("3"
                                              (cross-mult -2)
                                              (("3"
                                                (expand "expt" + 2)
                                                (("3"
                                                  (assert)
                                                  (("3"
                                                    (cross-mult 1)
                                                    (("3"
                                                      (case
                                                       "FORALL (ki:nat): expt(2,(ki+1))>1")
                                                      (("1"
                                                        (inst - "-i-1")
                                                        (("1"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (induct "ki")
                                                        (("1"
                                                          (hide-all-but
                                                           1)
                                                          (("1"
                                                            (grind)
                                                            nil
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (skosimp*)
                                                          (("2"
                                                            (expand
                                                             "expt"
                                                             1)
                                                            (("2"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("4"
                                              (cross-mult -1)
                                              (("4"
                                                (cross-mult 2)
                                                (("4"
                                                  (expand "expt" - 1)
                                                  (("4"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (assert) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((above nonempty-type-eq-decl nil integers nil)
    (log_nat_id formula-decl nil log_nat nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (div_mult_pos_lt1 formula-decl nil real_props nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (times_div2 formula-decl nil real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (div_mult_pos_lt2 formula-decl nil real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (even_plus_odd_is_odd application-judgement "odd_int" integers nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (minus_int_is_int application-judgement "int" integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (expt def-decl "real" exponentiation nil)
    (odd_plus_odd_is_even application-judgement "even_int" integers
     nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (posnat_expt application-judgement "posnat" exponentiation nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (pred type-eq-decl nil defined_types nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (i skolem-const-decl "int" log_nat nil)
    (n skolem-const-decl "nat" log_nat nil)
    (nnrat_exp application-judgement "nnrat" exponentiation nil)
    (posrat_exp application-judgement "posrat" exponentiation nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (int_plus_int_is_int application-judgement "int" integers 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)
    (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)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (posint_exp application-judgement "posint" exponentiation nil))
   nil))
(least_pow_2_ge_TCC2 0
  (least_pow_2_ge_TCC2-1 nil 3609934857
   ("" (skeep)
    (("" (skeep)
      (("" (typepred "y")
        (("" (case "NOT y>1")
          (("1" (assert) nil nil)
           ("2" (hide (-2 1))
            (("2" (splash 1)
              (("1" (rewrite "log_nat_id")
                (("1" (lemma "log_nat_bounds")
                  (("1" (inst?)
                    (("1" (assert)
                      (("1" (replace -8 :dir rl)
                        (("1" (flatten)
                          (("1" (skeep)
                            (("1" (case "xp = 2^n")
                              (("1"
                                (assert)
                                (("1"
                                  (replaces -1 :dir rl)
                                  (("1"
                                    (div-by -7 "xp")
                                    (("1" (assert) nil nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (case "i = n")
                                (("1" (assert) nil nil)
                                 ("2"
                                  (lemma "both_sides_expt_gt1_lt")
                                  (("2"
                                    (case "xp = 1")
                                    (("1"
                                      (replaces -1)
                                      (("1"
                                        (assert)
                                        (("1"
                                          (lemma "expt_gt1_bound2")
                                          (("1"
                                            (case "n = 0")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (replaces -1)
                                                (("1"
                                                  (hide-all-but 2)
                                                  (("1"
                                                    (grind)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (inst - "2" "n")
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (expand "^" -3)
                                                  (("1"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (assert)
                                      (("2"
                                        (inst - "2" "i" "n")
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (assert)
                (("2" (replace -3 1)
                  (("2" (expand "^" +)
                    (("2" (expand "expt" + 2)
                      (("2" (mult-by -2 "expt(2,n)")
                        (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (<= const-decl "bool" reals nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (log_nat_bounds formula-decl nil log_nat nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (times_div_cancel1 formula-decl nil extra_real_props nil)
    (div_simp formula-decl nil real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (both_sides_div1 formula-decl nil real_props nil)
    (nnrat_exp application-judgement "nnrat" exponentiation nil)
    (posrat_exp application-judgement "posrat" exponentiation nil)
    (both_sides_expt_gt1_lt formula-decl nil exponentiation nil)
    (expt_gt1_bound2 formula-decl nil exponentiation nil)
    (n skolem-const-decl "nat" log_nat nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat_expt application-judgement "posnat" exponentiation nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (expt def-decl "real" exponentiation nil)
    (log_nat_id formula-decl nil log_nat nil)
    (above nonempty-type-eq-decl nil integers nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (both_sides_times_pos_lt1 formula-decl nil 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (= const-decl "[T, T -> boolean]" equalities 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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (^ const-decl "real" exponentiation nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (posint_exp application-judgement "posint" exponentiation nil))
   nil))
(least_pow_2_ge_TCC3 0
  (least_pow_2_ge_TCC3-1 nil 3609934857
   ("" (skeep)
    (("" (assert)
      (("" (split +)
        (("1" (grind) nil nil)
         ("2" (skeep)
          (("2" (case "i = -1")
            (("1" (replaces -1) (("1" (grind) nil nil)) nil)
             ("2" (lemma "both_sides_expt_gt1_lt")
              (("2" (inst - "2" "i" "-1")
                (("2" (assert)
                  (("2" (expand "^" -1 2)
                    (("2" (expand "expt" -1)
                      (("2" (expand "expt" -1) (("2" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((posint_exp application-judgement "posint" exponentiation nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (both_sides_expt_gt1_lt formula-decl nil exponentiation 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)
    (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)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (expt def-decl "real" exponentiation nil)
    (^ const-decl "real" exponentiation nil)
    (posnat_expt application-judgement "posnat" exponentiation nil))
   nil))
(least_pow_2_ge_TCC4 0
  (least_pow_2_ge_TCC4-1 nil 3609934857
   ("" (skeep) (("" (cross-mult 3) (("" (assert) nil nil)) nil)) nil)
   ((posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types 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_ge1 formula-decl nil real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil))
   nil))
(least_pow_2_ge_TCC5 0
  (least_pow_2_ge_TCC5-1 nil 3609934857
   ("" (skeep)
    (("" (skeep)
      (("" (rewrite "log_nat_id")
        (("" (assert)
          (("" (splash)
            (("1" (skeep)
              (("1" (lemma "log_nat_bounds")
                (("1" (inst?)
                  (("1" (assert)
                    (("1" (replace -4 :dir rl)
                      (("1" (flatten)
                        (("1" (case "NOT xp > 2^(-n-1)")
                          (("1" (lemma "expt_inverse")
                            (("1" (inst - "n+1" "2")
                              (("1"
                                (replaces -1)
                                (("1"
                                  (cross-mult -2)
                                  (("1" (cross-mult 1) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (assert)
                            (("2" (case "2^(-n-1)>2^i")
                              (("1" (assert) nil nil)
                               ("2"
                                (assert)
                                (("2"
                                  (lemma "both_sides_expt_gt1_lt")
                                  (("2"
                                    (inst - "2" "i" "-n-1")
                                    (("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (assert)
              (("2" (lemma "log_nat_bounds")
                (("2" (inst?)
                  (("2" (assert)
                    (("2" (replace -2 :dir rl)
                      (("2" (assert)
                        (("2" (flatten)
                          (("2" (lemma "expt_inverse")
                            (("2" (inst - "n" "2")
                              (("2"
                                (replaces -1)
                                (("2"
                                  (cross-mult -1)
                                  (("2" (cross-mult 1) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((minus_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_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals 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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (div_mult_pos_lt1 formula-decl nil real_props nil)
    (div_mult_pos_gt2 formula-decl nil extra_real_props nil)
    (expt_inverse formula-decl nil exponentiation nil)
    (both_sides_expt_gt1_lt formula-decl nil exponentiation nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (log_nat_bounds formula-decl nil log_nat nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (^ const-decl "real" exponentiation nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (>= const-decl "bool" reals nil)
    (above nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
--> --------------------

--> maximum size reached

--> --------------------

Messung V0.5

¤ Dauer der Verarbeitung: 0.31 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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 und die Messung sind noch experimentell.