| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/reals/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 242 kB |
|
Impressum base_repr.prfSprache: Lisp |
|||||||||||||||
|
(base_repr (base_n_TCC1 0 (base_n_TCC1-1 nil 3617026679 ("" (subtype-tcc) nil nil) nil nil)) (base_n_TCC2 0 (base_n_TCC2-1 nil 3617026679 ("" (skeep) (("" (skeep) (("" (lemma "mod_pos") (("" (inst?) (("" (flatten) nil nil)) nil)) nil)) nil)) nil) ((mod_pos formula-decl nil mod nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (base_n_TCC3 0 (base_n_TCC3-1 nil 3617026679 ("" (subtype-tcc) nil nil) nil nil)) (base_n_TCC4 0 (base_n_TCC4-1 nil 3617026679 ("" (skeep) (("" (skeep) (("" (split) (("1" (expand "mod") (("1" (ground) nil nil)) nil) ("2" (ground) (("2" (lemma "mod_pos") (("2" (inst?) (("2" (flatten) (("2" (cross-mult) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((mod const-decl "{k | abs(k) < abs(j)}" mod nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mod_pos formula-decl nil mod nil) (nonneg_real nonempty-type-eq-decl nil real_types 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) (/= const-decl "boolean" notequal nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals 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) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) nil)) (base_n_TCC5 0 (base_n_TCC5-1 nil 3617026679 ("" (skeep) (("" (skeep) (("" (lemma "mod_pos") (("" (inst?) (("" (flatten) (("" (cross-mult) (("" (both-sides "-" "k" 3) (("" (simplify) (("" (case-replace "k*n-k= k*(n-1)") (("1" (case "n-1>0") (("1" (case "k>0") (("1" (mult-ineq -1 -2) (("1" (ground) nil nil)) nil) ("2" (ground) nil nil)) nil) ("2" (ground) nil nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((mod_pos formula-decl nil mod nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (both_sides_minus_lt1 formula-decl nil real_props nil) (gt_times_gt_any1 formula-decl nil extra_real_props nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" 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) (int_minus_int_is_int application-judgement "int" integers nil) (nonneg_real nonempty-type-eq-decl nil real_types 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) (/= const-decl "boolean" notequal nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals 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) (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (base_n_TCC6 0 (base_n_TCC6-1 nil 3617026679 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (> const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (int_minus_int_is_int application-judgement "int" 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) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (upper_index_TCC1 0 (upper_index_TCC1-1 nil 3617354263 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (> const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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)) nil)) (base_n_lt_n 0 (base_n_lt_n-1 nil 3620120286 ("" (skolem 1 ("n" "_" "_")) (("" (induct "i" 1 NAT_induction) (("" (skeep) (("" (skeep) (("" (expand "base_n" 1) (("" (lift-if 1) (("" (split 1) (("1" (flatten) (("1" (split 1) (("1" (flatten) (("1" (ground) nil nil)) nil) ("2" (flatten) (("2" (ground) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split 2) (("1" (flatten) (("1" (lemma "mod_pos") (("1" (inst?) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (inst -1 "j-1") (("1" (split -1) (("1" (inst -1 "(k-mod(k,n))/n") (("1" (hide-all-but 1) (("1" (split 1) (("1" (grind) nil nil) ("2" (cross-mult) (("2" (expand "mod") (("2" (cancel-by 1 "n") (("2" (ground) (("2" (grind) (("2" (typepred (k)) (("2" (div-by -1 "n") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (pred type-eq-decl nil defined_types nil) (< const-decl "bool" reals nil) (> const-decl "bool" reals nil) (base_n def-decl "nat" base_repr nil) (NAT_induction formula-decl nil naturalnumbers nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (NOT const-decl "[bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (CBD_20 skolem-const-decl "{x: nat | x > 1}" base_repr nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (<= const-decl "bool" reals nil) (integer nonempty-type-from-decl nil integers nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (both_sides_times_pos_ge1 formula-decl nil real_props nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (pos_div_gt formula-decl nil real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (zero_times1 formula-decl nil real_props nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (both_sides_div_pos_ge1 formula-decl nil real_props nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (k skolem-const-decl "nat" base_repr nil) (n skolem-const-decl "{x: nat | x > 1}" base_repr nil) (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/= const-decl "boolean" notequal nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (j skolem-const-decl "nat" base_repr nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (int_minus_int_is_int application-judgement "int" integers 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) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (mod_pos formula-decl nil mod nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) shostak)) (upper_is_bound 0 (upper_is_bound-6 nil 3617357240 ("" (skolem 1 ("n" "_" "_")) (("" (induct "k" 1 NAT_induction) (("" (skeep) (("" (skeep) (("" (case "j<n") (("1" (expand "base_n" 1) (("1" (lift-if 1) (("1" (split 1) (("1" (flatten) (("1" (split) (("1" (flatten) (("1" (expand "upper_index") (("1" (lift-if -5) (("1" (split -5) (("1" (flatten) nil nil) ("2" (flatten) (("2" (typepred ("log_nat(j, n)`1")) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (flatten) nil nil)) nil)) nil)) nil) ("2" (expand "upper_index" -2) (("2" (lift-if -2) (("2" (split -2) (("1" (flatten) (("1" (ground) nil nil)) nil) ("2" (flatten) (("2" (flip-ineq 2) (("2" (expand "base_n" 2) (("2" (lift-if 2) (("2" (split 2) (("1" (flatten) (("1" (ground) nil nil)) nil) ("2" (flatten) (("2" (hide 1) (("2" (split 1) (("1" (flatten) (("1" (ground) nil nil)) nil) ("2" (flatten) (("2" (hide 1) (("2" (inst -3 "(j-mod(j,n))/n") (("1" (split -3) (("1" (inst -1 "m-1") (("1" (lemma "log_nat_incr") (("1" (case "(j-mod(j,n))/n = 0") (("1" (replace -1) (("1" (expand "base_n") (("1" (propax) nil nil)) nil)) nil) ("2" (lemma "base_n_TCC4") (("2" (inst -1 "n" "j" "1") (("2" (split -1) (("1" (case "(j-mod(j,n))/n<1") (("1" (flatten) (("1" (ground) (("1" (assert) (("1" (name-replace "N" "(j-mod(j,n))/n") (("1" (hide-all-but (-1 -2 -3 2)) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flip-ineq 1) (("2" (lemma "log_nat_incr") (("2" (inst -1 "n" "(j-mod(j,n))/n" "j") (("2" (split -1) (("1" (case "m-1>log_nat((j - mod(j, n)) / n, n)`1") (("1" (split -6) (("1" (propax) nil nil) ("2" (expand "upper_index") (("2" (lift-if 1) (("2" (split 1) (("1" (flatten) nil nil) ("2" (flatten) nil nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil) ("2" (simplify 1) (("2" (case-replace "n * ((j - mod(j, n)) / n) = j-mod(j,n)") (("1" (both-sides "-" "j" 1) (("1" (simplify 1) (("1" (lemma "mod_pos") (("1" (inst?) (("1" (flatten) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil) ("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred ("log_nat(j, n)`1")) (("2" (ground) nil nil)) nil)) nil) ("2" (lemma "mod_pos") (("2" (inst -1 "j" "n") (("2" (flatten) (("2" (cross-mult 1) (("2" (ground) (("2" (both-sides "-" "j" 1) (("2" (simplify 1) (("2" (case "0<j") (("1" (case "0<n-1") (("1" (mult-ineq -1 -2) (("1" (ground) nil nil)) nil) ("2" (ground) nil nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "base_n_TCC4") (("2" (inst -1 "n" "j" "1") (("2" (split -1) (("1" (propax) nil nil) ("2" (ground) nil nil) ("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (pred type-eq-decl nil defined_types nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (> const-decl "bool" reals nil) (upper_index const-decl "nat" base_repr nil) (= const-decl "[T, T -> boolean]" equalities nil) (base_n def-decl "nat" base_repr nil) (NAT_induction formula-decl nil naturalnumbers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (log_nat_incr formula-decl nil log_nat nil) (base_n_TCC4 subtype-tcc nil base_repr nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (<= const-decl "bool" reals nil) (both_sides_minus_le1 formula-decl nil real_props nil) (mod_pos formula-decl nil mod nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (rat nonempty-type-eq-decl nil rationals nil) (m skolem-const-decl "nat" base_repr nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (both_sides_minus_lt1 formula-decl nil real_props nil) (even_times_int_is_even application-judgement "even_int" integers nil) (lt_times_lt_any1 formula-decl nil extra_real_props 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) (j skolem-const-decl "nat" base_repr nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (n skolem-const-decl "{x: nat | x > 1}" base_repr nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (int_minus_int_is_int application-judgement "int" integers nil) (nat_exp application-judgement "nat" 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) (AND const-decl "[bool, bool -> bool]" booleans nil) (above nonempty-type-eq-decl nil integers nil) (NOT const-decl "[bool -> bool]" booleans 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 "bool" reals nil)) nil) (upper_is_bound-5 nil 3617357192 ("" (induct "k" NAT_induction) (("1" (skeep) (("1" (typepred (n)) (("1" (expand "base_n") (("1" (ground) nil))))))) ("2" (skeep) (("2" (skeep) (("2" (expand "base_n" 1) (("2" (lift-if 1) (("2" (split 1) (("1" (flatten) (("1" (split 1) (("1" (flatten) (("1" (expand "upper_index") (("1" (typepred ("log_nat(1+j, n)`1")) (("1" (ground) nil))))))) ("2" (propax) nil))))) ("2" (flatten) (("2" (split) (("1" (flatten) (("1" (expand "upper_index") (("1" (typepred ("log_nat(1+j, n)`1")) (("1" (ground) nil))))))) ("2" (flatten) (("2" (postpone) nil)))))))))))))))))) nil) nil nil) (upper_is_bound-4 nil 3617357053 ("" (induct "k") (("1" (skeep) (("1" (typepred (n)) (("1" (expand "base_n") (("1" (ground) nil))))))) ("2" (skeep) (("2" (skeep) (("2" (expand "base_n" 1) (("2" (lift-if 1) (("2" (split 1) (("1" (flatten) (("1" (split 1) (("1" (flatten) (("1" (expand "upper_index") (("1" (typepred ("log_nat(1+j, n)`1")) (("1" (ground) nil))))))) ("2" (propax) nil))))) ("2" (flatten) (("2" (split) (("1" (flatten) (("1" (expand "upper_index") (("1" (typepred ("log_nat(1+j, n)`1")) (("1" (ground) nil))))))) ("2" (flatten) (("2" (postpone) nil)))))))))))))))))) nil) nil nil) (upper_is_bound-3 nil 3617356979 ("" (induct "k" "NAT_induction") (("1" (skeep) (("1" (typepred (n)) (("1" (expand "base_n") (("1" (ground) nil))))))) ("2" (skeep) (("2" (skeep) (("2" (expand "base_n" 1) (("2" (lift-if 1) (("2" (split 1) (("1" (flatten) (("1" (split 1) (("1" (flatten) (("1" (expand "upper_index") (("1" (typepred ("log_nat(1+j, n)`1")) (("1" (ground) nil))))))) ("2" (propax) nil))))) ("2" (flatten) (("2" (split) (("1" (flatten) (("1" (expand "upper_index") (("1" (typepred ("log_nat(1+j, n)`1")) (("1" (ground) nil))))))) ("2" (flatten) (("2" (postpone) nil)))))))))))))))))) nil) nil nil) (upper_is_bound-2 nil 3617356437 ("" (induct "k") (("1" (skeep) (("1" (typepred (n)) (("1" (expand "base_n") (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (skeep) (("2" (skeep) (("2" (expand "base_n" 1) (("2" (lift-if 1) (("2" (split 1) (("1" (flatten) (("1" (split 1) (("1" (flatten) (("1" (expand "upper_index") (("1" (typepred ("log_nat(1+j, n)`1")) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (flatten) (("2" (split) (("1" (flatten) (("1" (expand "upper_index") (("1" (typepred ("log_nat(1+j, n)`1")) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil nil) (upper_is_bound-1 nil 3617354266 ("" (induct "k") (("1" (skeep) (("1" (typepred (n)) (("1" (expand "base_n") (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (skeep) (("2" (skeep) (("2" (expand "base_n") (("2" (lift-if 1) (("2" (split 1) (("1" (flatten) (("1" (split 1) (("1" (flatten) (("1" (expand "upper_index") (("1" (typepred ("log_nat(1+j, n)`1")) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil) ("2" (flatten) (("2" (split) (("1" (flatten) (("1" (expand "upper_index") (("1" (typepred ("log_nat(1+j, n)`1")) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (expand "upper_index") (("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (base_n_is_n_TCC1 0 (base_n_is_n_TCC1-1 nil 3617354263 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (> const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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)) nil)) (base_n_is_n_TCC2 0 (base_n_is_n_TCC2-1 nil 3617354263 ("" (subtype-tcc) nil nil) nil nil)) (base_n_is_n 0 (base_n_is_n-1 nil 3617365860 ("" (skolem 1 ("n" "_")) (("" (induct "k" 1 NAT_induction) (("1" (skolem 1 "k") (("1" (case "k<n") (("1" (flatten) (("1" (case-replace "upper_index(n,k) = 0") (("1" (lemma "sigma_eq_arg[nat]") (("1" (inst?) (("1" (replace -1) (("1" (hide (-1 -4)) (("1" (expand "base_n") (("1" (expand "^") (("1" (expand "expt") (("1" (lift-if 1) (("1" (split) (("1" (flatten) (("1" (ground) nil nil)) nil) ("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "upper_index") (("2" (lift-if 1) (("2" (split 1) (("1" (propax) nil nil) ("2" (flatten) (("2" (expand "log_nat") (("2" (lift-if 2) (("2" (split 2) (("1" (propax) nil nil) ("2" (flatten) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flip-ineq 1) (("2" (flatten) (("2" (rewrite "sigma_first_ge") (("2" (case-replace "n^0*base_n(n,k)(0) = mod(k,n)") (("1" (both-sides "-" "mod(k,n)" 1) (("1" (simplify 1) (("1" (rewrite "sigma_shift_to_zero") (("1" (both-sides "*" "1/n" 1) (("1" (lemma "sigma_scal_right") (("1" (inst?) (("1" (replace -1 :dir rl) (("1" (case-replace "(LAMBDA (i_1: nat): (n ^ (1 + i_1)) * base_n(n, k)(1 + i_1) * (1 / n)) = LAMBDA (i: nat): n ^ i * base_n(n, k)(1 + i)") (("1" (expand "base_n" 1) (("1" (lemma "base_n_TCC4") (("1" (inst -1 "n" "k" "1") (("1" (split -1) (("1" (case-replace "(LAMBDA(i:nat): n^i*IF k < n THEN 0 ELSE base_n(n, (k - mod(k, n)) / n)(i) ENDIF) = LAMBDA(i:nat): n^i*base_n(n, (k - mod(k, n)) / n)(i)") (("1" (name "K" "(k-mod(k,n))/n") (("1" (case-replace "upper_index(n,K) = upper_index(n,k)-1") (("1" (hide (-5 -6)) (("1" (inst -7 "K") (("1" (split -7) (("1" (replace -3 :dir rl) (("1" (ground) nil nil)) nil) ("2" (expand "K") (("2" (cross-mult 1) (("2" (both-sides "-" "k" 1) (("2" (simplify 1) (("2" (case "0<k") (("1" (case "0<n-1") (("1" (mult-ineq -1 -2) (("1" (lemma "mod_pos") (("1" (inst?) (("1" (flatten) (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "K") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "upper_index") (("2" (lift-if 1) (("2" (split 1) (("1" (flatten) (("1" (case "k=n") (("1" (replace -1) (("1" (lift-if 1) (("1" (split 1) (("1" (flatten) (("1" (ground) nil nil)) nil) ("2" (flatten) (("2" (expand "log_nat") (("2" (expand "log_nat") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (replace -1) (("2" (cross-mult -2) (("2" (case "k=mod(k,n)") (("1" (lemma "mod_pos") (("1" (inst?) (("1" (flatten) (("1" (replace -3 :dir rl) (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (lift-if 2) (("2" (split 2) (("1" (flatten) (("1" (ground) nil nil)) nil) ("2" (flatten) (("2" (hide (-2 -5 -6 -7 -9 4)) (("2" (lemma "log_nat_incr") (("2" (inst -1 "n" "K" "k") (("2" (split -1) (("1" (case "log_nat(K,n)`1<=log_nat(k,n)`1-1") (("1" (both-sides "+" "1" -1) (("1" (simplify -1) (("1" (both-sides "+" "1" 2) (("1" (simplify 2) (("1" (case-replace "1+log_nat(K, n)`1 = log_nat(n*K, n)`1") (("1" (lemma "log_nat_incr") (("1" (case "log_nat(n*K, n)`1< log_nat(k,n)`1") (("1" (case "log_nat(n*K, n)`1+1 <= log_nat(k,n)`1") (("1" (case-replace "log_nat(n*K, n)`1+1 = log_nat(n*n*K, n)`1") (("1" (lemma "log_nat_bounds") (("1" (inst-cp -1 "n" "n*K") (("1" (case "n*K<n^(log_nat(n*K,n)`1+1)") (("1" (inst -2 "n" "k") (("1" (case "n^log_nat(k,n)`1<=k") (("1" (replace -5 -2) (("1" (div-by -1 "n") (("1" (case-replace "n ^ log_nat(k, n)`1 / n = n^(log_nat(k,n)`1-1)") (("1" (case "n^(log_nat(k,n)`1-1)<=floor(k/n)") (("1" (mult-by -1 "n") (("1" (cross-mult -2) (("1" (replace -2 -1 :dir rl) (("1" (case-replace "floor(k/n)*n = k-mod(k,n)") (("1" (case-replace "k-mod(k,n) = n*K") (("1" (case "n^log_nat(k,n)`1<n^log_nat(n*n*K, n)`1") (("1" (lemma "both_sides_expt_gt1_lt") (("1" (inst -1 "n" "log_nat(k, n)`1 " " log_nat(n * n * K, n)`1") (("1" (flatten) (("1" (split -1) (("1" (ground) (("1" (hide-all-but (-2 -13)) (("1" (ground) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (ground) (("2" (split-ineq -3) nil nil)) nil)) nil) ("2" (expand "K") (("2" (ground) nil nil)) nil)) nil) ("2" (expand "mod") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "FORALL (nn1:nat,xx1:nnreal): nn1<=xx1 IMPLIES nn1<=floor(xx1)") (("1" (inst?) (("1" (assert) nil nil) ("2" (assert) nil nil) ("3" (assert) (("3" (expand "^") (("3" (propax) nil nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skeep) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (cross-mult 1) (("2" (expand "^") (("2" (lift-if 1) (("2" (split) (("1" (flatten) (("1" (expand "expt" 1 1) (("1" (lift-if 1) (("1" (split 1) (("1" (flatten) (("1" (ground) nil nil)) nil) ("2" (flatten) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil) ("2" (name-replace "lgnK" "log_nat(n*K, n)`1") (("2" (hide (-1 -2 -3 -4 -5 -6 3)) (("2" (expand "log_nat") (("2" (lift-if 1) (("2" (split 1) (("1" (flatten) (("1" (ground) (("1" (cancel-by -1 "n") (("1" (case "K>=1") (("1" (typepred (n)) (("1" (mult-ineq -1 -2) (("1" (ground) nil nil)) nil)) nil) ("2" (expand "K") (("2" (ground) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case-replace "K * n * n / n = K*n") (("1" (expand "lgnK") (("1" (ground) nil nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (case "K>=1") (("1" (typepred (n)) (("1" (mult-ineq -1 -2) (("1" (ground) (("1" (mult-ineq -1 -2) (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-8 -9 1 5)) (("2" (expand "K") (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil) ("2" (ground) nil nil)) nil)) nil) ("2" (name-replace "lgK" "log_nat(K,n)`1") (("2" (expand "log_nat") (("2" (lift-if 1) (("2" (split 1) (("1" (flatten) (("1" (cancel-by -1 "n") (("1" (expand "K") (("1" (ground) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (case-replace "n*K/n = K") (("1" (expand "lgK") (("1" (propax) nil nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (case "K>=1") (("1" (typepred (n)) (("1" (mult-ineq -1 -2) (("1" (ground) nil nil)) nil)) nil) ("2" (replace -3) (("2" (ground) (("2" (split-ineq -5) (("2" (hide-all-but (-3 -4 -5 1 2)) (("2" (expand "K") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil) ("2" (expand "K") (("2" (case-replace "n * ((k - mod(k, n)) / n) = k-mod(k,n)") (("1" (both-sides "-" "k" 1) (("1" (simplify 1) (("1" (lemma "mod_pos") (("1" (inst?) (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "K") (("3" (propax) nil nil)) nil)) nil)) nil) ("2" (decompose-equality 1) nil nil) ("3" (flatten) (("3" (ground) nil nil)) nil)) nil) ("2" (ground) nil nil) ("3" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (decompose-equality 1) (("2" (expand "^") (("2" (name-replace "EN" "expt(n, x!1)") (("2" (expand "expt") (("2" (ground) (("2" (case-replace " base_n(n, k)(1 + x!1) * expt(n, x!1) * (1 / n) * n = base_n(n, k)(1 + x!1) * expt(n, x!1)") (("1" (expand "EN") (("1" (ground) nil nil)) nil) ("2" (expand "EN") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred (n)) (("2" (ground) (("2" (assert) (("2" (cancel-by -2 "n") nil nil)) nil)) nil)) nil)) nil) ("2" (hide (-3 2)) (("2" (expand "upper_index") (("2" (expand "log_nat") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil) ("2" (hide (2 -2)) (("2" (expand "^") (("2" (expand "expt") (("2" (expand "base_n") (("2" (lift-if 1) (("2" (split) (("1" (flatten) (("1" (ground) nil nil)) nil) ("2" (flatten) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep 1) (("2" (expand "upper_index") (("2" (lift-if 1) (("2" (split 1) (("1" (flatten) (("1" (ground) nil nil)) nil) ("2" (flatten) (("2" (typepred ("log_nat(k, n)`1")) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (<= const-decl "bool" reals nil) (n skolem-const-decl "{x: nat | x > 1}" base_repr nil) (upper_index const-decl "nat" base_repr nil) (> const-decl "bool" reals nil) (OR const-decl "[bool, bool -> bool]" booleans 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) (pred type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (T_low type-eq-decl nil sigma nil) (T_high type-eq-decl nil sigma nil) (sigma def-decl "real" sigma nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (base_n def-decl "nat" base_repr nil) (NAT_induction formula-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (nat_exp application-judgement "nat" exponentiation nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (expt def-decl "real" exponentiation nil) (sigma_eq_arg formula-decl nil sigma nil) (log_nat def-decl "[n: nat, {y | y < p AND x = p ^ n * y}]" log_nat nil) (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (sigma_nat application-judgement "nat" sigma_nat nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (cross_mult formula-decl nil real_props nil) (times_div1 formula-decl nil real_props nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (base_n_TCC4 subtype-tcc nil base_repr nil) (rat nonempty-type-eq-decl nil rationals nil) (div_cancel3 formula-decl nil real_props nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (log_nat_incr formula-decl nil log_nat nil) (odd? const-decl "bool" integers nil) (both_sides_plus_le1 formula-decl nil real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (real_minus_real_is_real application-judgement "real" reals nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (nnreal type-eq-decl nil real_types nil) (nat_expt application-judgement "nat" exponentiation nil) (k skolem-const-decl "nat" base_repr nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (both_sides_expt_gt1_lt formula-decl nil exponentiation nil) (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (integer nonempty-type-from-decl nil integers nil) (minus_int_is_int application-judgement "int" integers nil) (both_sides_div_pos_le1 formula-decl nil real_props nil) (log_nat_bounds formula-decl nil log_nat nil) (lgnK skolem-const-decl "nat" base_repr nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (CBD_21 skolem-const-decl "{x: nat | x > 1}" base_repr nil) (both_sides_times_pos_lt1 formula-decl nil real_props nil) (pos_div_gt formula-decl nil real_props nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (zero_times1 formula-decl nil real_props nil) (gt_times_gt_any1 formula-decl nil extra_real_props nil) (posint_times_posint_is_posint application-judgement "posint" integers nil) (odd_times_odd_is_odd application-judgement "odd_int" integers nil) (CBD_22 skolem-const-decl "{x: nat | x > 1}" base_repr nil) (lgK skolem-const-decl "nat" base_repr nil) (both_sides_minus_le1 formula-decl nil real_props nil) (above nonempty-type-eq-decl nil integers nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (rat_minus_rat_is_rat application-judgement "rat" rationals nil) (div_mult_pos_lt1 formula-decl nil real_props 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) (mod_pos formula-decl nil mod nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (lt_times_lt_any1 formula-decl nil extra_real_props nil) (even_times_int_is_even application-judgement "even_int" integers nil) (both_sides_minus_lt1 formula-decl nil real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (K skolem-const-decl "rat" base_repr nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (EN skolem-const-decl "nat" base_repr nil) (sigma_scal_right formula-decl nil sigma nil) (both_sides_times1_imp formula-decl nil extra_real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_shift_to_zero formula-decl nil sigma_nat nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (NOT const-decl "[bool -> bool]" booleans nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (sigma_nnreal application-judgement "nnreal" sigma_nat nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (sigma_first_ge formula-decl nil sigma_nat nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil)) shostak)) (base_n_to_nat_TCC1 0 (base_n_to_nat_TCC1-1 nil 3620393225 ("" (subtype-tcc) nil nil) nil nil)) (base_n_is_n_alt_TCC1 0 (base_n_is_n_alt_TCC1-1 nil 3621094617 ("" (subtype-tcc) nil nil) nil nil)) (base_n_is_n_alt 0 (base_n_is_n_alt-1 nil 3620393240 ("" (skeep) (("" (expand "base_n_to_nat") (("" (lemma "base_n_is_n") (("" (inst?) (("" (lemma "upper_is_bound") (("" (lemma "log_nat_bounds") (("" (case "upper_index(n,k)<=m") (("1" (case-replace "upper_index(n,k) = m") (("1" (lemma "sigma_split") (("1" (inst -1 "LAMBDA (s: nat): n ^ s * base_n(n, k)(s)" "m" "0" "upper_index(n,k)") (("1" (split -1) (("1" (ground) (("1" (replace -1) (("1" (hide -1) (("1" (replace -4 :dir rl) (("1" (simplify 2) (("1" (lemma "sigma_const_restrict_eq_0") (("1" (inst -1 "LAMBDA (s: nat): n ^ s * base_n(n, k)(s)" "m" "1+upper_index(n,k)" "1") (("1" (split -1) (("1" (ground) nil nil) ("2" (skeep) (("2" (inst -3 "n" "k" "i") (("2" (split -3) (("1" (ground) nil nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "upper_index") (("2" (lift-if 1) (("2" (split 1) (("1" (flatten) (("1" (ground) nil nil)) nil) ("2" (flatten) (("2" (hide (-3 3)) (("2" (inst -1 "n" "k") (("2" (flip-ineq -3) (("2" (flip-ineq 3) (("2" (case "log_nat(k,n)`1>=m+1") (("1" (lemma "both_sides_expt_gt1_le") (("1" (inst -1 "n" "m+1" "log_nat(k,n)`1") (("1" (flatten) (("1" (hide -1) (("1" (split -1) (("1" (ground) nil nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((base_n_to_nat const-decl "nat" base_repr nil) (nat_exp application-judgement "nat" 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (log_nat_bounds formula-decl nil log_nat nil) (posreal nonempty-type-eq-decl nil real_types nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (both_sides_expt_gt1_le formula-decl nil exponentiation nil) (< const-decl "bool" reals nil) (log_nat def-decl "[n: nat, {y | y < p AND x = p ^ n * y}]" log_nat nil) (above nonempty-type-eq-decl nil integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (T_low type-eq-decl nil sigma nil) (T_high type-eq-decl nil sigma nil) (base_n def-decl "nat" base_repr 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) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (sigma_nnreal application-judgement "nnreal" sigma_nat nil) (sigma_nat application-judgement "nat" sigma_nat 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_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_exp application-judgement "posint" exponentiation nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_const_restrict_eq_0 formula-decl nil sigma nil) (sigma_split formula-decl nil sigma nil) (upper_index const-decl "nat" base_repr nil) (<= const-decl "bool" reals nil) (upper_is_bound formula-decl nil base_repr nil) (base_n_is_n formula-decl nil base_repr nil)) shostak)) (base_n_to_nat_lt 0 (base_n_to_nat_lt-1 nil 3620468885 ("" (skeep) (("" (expand "base_n_to_nat") (("" (lemma "sigma_le") (("" (name "kz" "n-1") (("" (inst - "LAMBDA (s: nat): n ^ s * F(s)" "LAMBDA (s:nat): (n-1)*n^s" "m" "0") (("" (replace -1) (("" (assert) (("" (split) (("1" (rewrite "sigma_scal") (("1" (lemma "sigma_geometric") (("1" (inst - "m" "0" "n") (("1" (assert) (("1" (rewrite "expt_x0") (("1" (replaces -1) (("1" (assert) (("1" (invoke (case "%1 = n^(1+m)-1") (! -1 2)) (("1" (assert) nil nil) ("2" (assert) (("2" (cross-mult 1) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst - "n!1") (("2" (case "NOT F(n!1)<=kz") (("1" (assert) nil nil) ("2" (mult-by -1 "n^n!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((base_n_to_nat const-decl "nat" base_repr nil) (> const-decl "bool" reals 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) (int_minus_int_is_int application-judgement "int" integers nil) (nat_exp application-judgement "nat" exponentiation nil) (sigma_nnreal application-judgement "nnreal" sigma_nat nil) (sigma_nat application-judgement "nat" sigma_nat nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (sigma_geometric formula-decl nil sigma_nat nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (times_div1 formula-decl nil real_props nil) (div_cancel3 formula-decl nil real_props nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (expt_x0 formula-decl nil exponentiation nil) (sigma_scal formula-decl nil sigma nil) (subrange type-eq-decl nil integers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (NOT const-decl "[bool -> bool]" booleans 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) (T_low type-eq-decl nil sigma nil) (T_high type-eq-decl nil sigma nil) (<= const-decl "bool" reals 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) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (sigma_le formula-decl nil sigma 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)) shostak)) (base_n_0 0 (base_n_0-1 nil 3621093915 ("" (skeep) (("" (lemma "upper_is_bound") (("" (inst?) (("" (assert) (("" (lemma "base_n_is_n") (("" (inst?) (("" (lemma "sigma_split") (("" (inst?) (("" (inst - "m") (("" (assert) (("" (replaces -1) (("" (expand "sigma" - 1) (("" (case "base_n(n,k)(m)>=1") (("1" (mult-by -1 "n^(m)") (("1" (lemma "sigma_ge_0") (("1" (inst-cp - _ "upper_index(n,k)" "1+m") (("1" (inst-cp - _ "m-1" "0") (("1" (hide -1) (("1" (inst?) (("1" (inst?) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((upper_is_bound formula-decl nil base_repr nil) (real_gt_is_strict_total_order name-judgement "(strict_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) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers 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) (base_n def-decl "nat" base_repr nil) (<= const-decl "bool" reals nil) (T_high type-eq-decl nil sigma nil) (upper_index const-decl "nat" base_repr nil) (T_low type-eq-decl nil sigma nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (sigma_nat application-judgement "nat" sigma_nat nil) (sigma_nnreal application-judgement "nnreal" sigma_nat nil) (sigma def-decl "real" sigma nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (int_minus_int_is_int application-judgement "int" integers nil) (sigma_ge_0 formula-decl nil sigma nil) (sigma_split formula-decl nil sigma nil) (base_n_is_n formula-decl nil base_repr nil) (> const-decl "bool" reals 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)) shostak)) (base_n_unique 0 (base_n_unique-1 nil 3620035552 ("" (skeep) (("" (skoletin 1) (("" (skeep) (("" (case "NOT upper_index(n,k)<=d") (("1" (expand "upper_index") (("1" (assert) (("1" (lift-if) (("1" (ground) (("1" (lemma "log_nat_bounds") (("1" (inst?) (("1" (assert) (("1" (flatten) (("1" (case "k < n^(d+1)") (("1" (lemma "both_sides_expt_gt1_lt_aux") (("1" (inst - "n" "log_nat(k,n)`1-1" "d") (("1" (assert) (("1" (expand "^") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "sigma_le") (("2" (inst - "LAMBDA (s: nat): n ^ s * numseq(s)" "LAMBDA (s: nat): n ^ s * (n-1)" "d" "0") (("2" (split -) (("1" (invoke (case "%1 < n^(d+1)") (! -1 2)) (("1" (assert) nil nil) ("2" (hide -1) (("2" (lemma "sigma_scal") (("2" (inst - "LAMBDA (s:nat): n^s" "n-1" "d" "0") (("2" (replace -1) (("2" (lemma "sigma_geometric") (("2" (inst?) (("2" (split -1) (("1" (replace -1) (("1" (rewrite "expt_x0") (("1" (hide-all-but 1) (("1" (grind-reals) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (case "numseq(n!1)<=n-1") (("1" (mult-by -1 "n^n!1") (("1" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "base_n_is_n") (("2" (inst?) (("2" (case "NOT k = sigma(0, d, LAMBDA (s: nat): n ^ s * base_n(n, k)(s))") (("1" (lemma "sigma_split") (("1" (inst?) (("1" (inst - "upper_index(n,k)") (("1" (assert) (("1" (replaces -1) (("1" (invoke (case "%1 = 0") (! 1 2 2)) (("1" (assert) nil nil) ("2" (hide 2) (("2" (rewrite "sigma_restrict_eq_0") (("2" (skosimp*) (("2" (lemma "upper_is_bound") (("2" (inst - "n" "k" "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2) (("2" (name "F" "LAMBDA (z:nat): numseq(z)-base_n(n,k)(z)") (("2" (case "F = (LAMBDA (i:nat): 0)") (("1" (decompose-equality -1) (("1" (inst - "j") (("1" (expand "F" -1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (case "NOT sigma(0,d,LAMBDA (s:nat): n^s*F(s))=0") (("1" (expand "F" 1) (("1" (rewrite "sigma_minus" :dir rl) (("1" (assert) nil nil)) nil)) nil) ("2" (case "NOT FORALL (s:nat): abs(F(s))<n") (("1" (skeep) (("1" (expand "F" 1) (("1" (case "abs(numseq(s))<n AND abs(base_n(n,k)(s))<n") (("1" (flatten) (("1" (hide-all-but (-1 -2 1)) (("1" (grind :exclude "base_n") nil nil)) nil)) nil) ("2" (expand "abs" 1) (("2" (assert) (("2" (lemma "base_n_lt_n") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "EXISTS (dd:nat): dd<=d AND F(dd)/=0 AND (FORALL (s:nat): s>dd AND s<=d IMPLIES F(s)=0)") (("1" (skeep -1) (("1" (case "sigma(0, d, LAMBDA (s: nat): n ^ s * F(s)) = sigma(0, dd, LAMBDA (s: nat): n ^ s * F(s))") (("1" (assert) (("1" (replace -1) (("1" (expand "sigma" -5) (("1" (case "abs(n^dd*F(dd)) >= n^dd AND abs(sigma(0, dd - 1, LAMBDA (s: nat): n ^ s * F(s)))<n^dd") (("1" (flatten) (("1" (expand "abs") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (split 1) (("1" (rewrite "abs_mult") (("1" (expand "abs" + 1) (("1" (case "NOT abs(F(dd))>=1") (("1" (expand "abs" 1) (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil) ("2" (mult-by -1 "n^dd") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "sigma_triangle") (("2" (inst?) (("2" (invoke (case "%1<n^dd") (! -1 2)) (("1" (assert) nil nil) ("2" (lemma "sigma_le") (("2" (inst - "LAMBDA (n_1: nat): abs(n ^ n_1 * F(n_1))" "LAMBDA (n_1: nat): n ^ n_1 * (n-1)" "dd-1" "0") (("2" (split -1) (("1" (invoke (case "%1<n^dd") (! -1 2)) (("1" (assert) nil nil) ("2" (case "NOT dd-1>=0") (("1" (assert) (("1" (expand "abs" +) (("1" (assert) (("1" (expand "^" +) (("1" (lemma "posnat_expt") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sigma_scal") (("2" (inst - "LAMBDA (s:nat): n^s" "n-1" "dd-1" "0") (("2" (replaces -1) (("2" (lemma "sigma_geometric") (("2" (inst?) (("2" (split -1) (("1" (replaces -1) (("1" (rewrite "expt_x0") (("1" (grind-reals) nil nil)) nil)) nil) ("2" (assert) nil nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (rewrite "abs_mult") (("2" (expand "abs" + 1) (("2" (inst -5 "n!1") (("2" (case "abs(F(n!1))<=n-1") (("1" (mult-by -1 "n^n!1") (("1" (assert) nil nil)) nil) ("2" (assert) (("2" (expand "abs") (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sigma_split") (("2" (inst?) (("2" (inst - "dd") (("2" (assert) (("2" (replaces -1) (("2" (assert) (("2" (rewrite "sigma_restrict_eq_0" 1) (("2" (skosimp*) (("2" (inst - "i!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "FORALL (kz:nat): (EXISTS (j:nat): j<=kz AND F(j)/=0) IMPLIES EXISTS (dd: nat): dd <= kz AN F(dd) /= 0 AND (FORALL (s: nat): s > dd AND s <= kz IMPLIES F(s) = 0)") (("1" (inst - "d") (("1" (replace 1) (("1" (inst + "j") (("1" (assert) (("1" (expand "F" 1) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (induct "kz") (("1" (grind) nil nil) ("2" (skolem 1 "kz") (("2" (flatten) (("2" (assert) (("2" (case "(EXISTS (j: nat): j <= kz AND F(j) /= 0)") (("1" (assert) (("1" (replace -1) (("1" (case "F(1+kz)=0") (("1" (skeep -3) (("1" (inst + "dd") (("1" (assert) (("1" (skeep) (("1" (inst -4 "s") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "1+kz") (("2" (assert) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep -2) (("2" (inst + "j!1") (("2" (assert) (("2" (inst + "1+kz") (("2" (assert) (("2" (skosimp*) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((<= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (OR const-decl "[bool, bool -> bool]" booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (sigma_nat application-judgement "nat" sigma_nat nil) (sigma_nnreal application-judgement "nnreal" sigma_nat nil) (TRUE const-decl "bool" booleans nil) (id const-decl "(bijective?[T, T])" identity nil) (bijective? const-decl "bool" functions nil) (> const-decl "bool" reals nil) (/= const-decl "boolean" notequal nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_exp application-judgement "nat" exponentiation nil) (= const-decl "[T, T -> boolean]" equalities nil) (T_low type-eq-decl nil sigma nil) (T_high type-eq-decl nil sigma nil) (sigma def-decl "real" sigma nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (^ const-decl "real" exponentiation nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (base_n def-decl "nat" base_repr nil) (upper_index const-decl "nat" base_repr nil) (above nonempty-type-eq-decl nil integers nil) (sigma_le formula-decl nil sigma nil) (sigma_geometric formula-decl nil sigma_nat nil) (expt_x0 formula-decl nil exponentiation nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (rat_minus_rat_is_rat application-judgement "rat" rationals nil) (div_mult_neg_lt1 formula-decl nil real_props nil) (div_distributes_minus formula-decl nil real_props nil) (times_div2 formula-decl nil real_props nil) (sigma_scal formula-decl nil sigma nil) (both_sides_times_pos_le1_imp formula-decl nil extra_real_props nil) (subrange type-eq-decl nil integers nil) (both_sides_expt_gt1_lt_aux formula-decl nil exponentiation nil) (int_plus_int_is_int application-judgement "int" integers nil) (nat_expt application-judgement "nat" exponentiation nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (log_nat def-decl "[n: nat, {y | y < p AND x = p ^ n * y}]" log_nat nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (log_nat_bounds formula-decl nil log_nat nil) (F skolem-const-decl "[nat -> int]" base_repr nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (base_n_lt_n formula-decl nil base_repr nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (minus_int_is_int application-judgement "int" integers nil) (pred type-eq-decl nil defined_types nil) (nat_induction formula-decl nil naturalnumbers nil) (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props nil) (abs_mult formula-decl nil real_props nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat_expt judgement-tcc nil exponentiation nil) (sigma_0_neg formula-decl nil sigma_nat nil) (dd skolem-const-decl "nat" base_repr nil) (rat_abs_is_nonneg application-judgement "{r: nonneg_rat | r >= q}" real_defs nil) (sigma_triangle formula-decl nil sigma nil) (real_plus_real_is_real application-judgement "real" reals nil) (minus_real_is_real application-judgement "real" reals nil) (sigma_minus formula-decl nil sigma nil) (sigma_split formula-decl nil sigma nil) (nnrat_times_nnrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (upper_is_bound formula-decl nil base_repr nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (sigma_restrict_eq_0 formula-decl nil sigma nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (base_n_is_n formula-decl nil base_repr nil)) shostak)) (base_n_base_n_to_nat 0 (base_n_base_n_to_nat-1 nil 3620554653 ("" (skeep) (("" (skeep) (("" (typepred "i") (("" (lemma "base_n_unique") (("" (name "numseq" "LAMBDA (i:nat): IF i<=m THEN F(i) ELSE 0 ENDIF") (("" (inst - "m" "n" "numseq") (("1" (assert) (("1" (inst - "i") (("1" (assert) (("1" (expand "numseq" -2) (("1" (expand "base_n_to_nat" +) (("1" (case "sigma(0, m, LAMBDA (s: nat): n ^ s * F(s)) = sigma(0, m, LAMBDA (s: nat): n ^ s * IF s <= m THEN F(s) ELSE 0 ENDIF)") (("1" (assert) nil nil) ("2" (rewrite "sigma_eq") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "numseq") (("2" (lift-if) (("2" (ground) (("2" (inst - "x1!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((base_n_unique formula-decl nil base_repr nil) (< const-decl "bool" reals nil) (numseq skolem-const-decl "[nat -> nat]" base_repr nil) (> const-decl "bool" reals nil) (n skolem-const-decl "{x: nat | x > 1}" base_repr nil) (below type-eq-decl nil naturalnumbers nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (T_low type-eq-decl nil sigma nil) (T_high type-eq-decl nil sigma nil) (sigma def-decl "real" sigma nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (sigma_eq formula-decl nil sigma nil) (base_n_to_nat const-decl "nat" base_repr nil) (sigma_nnreal application-judgement "nnreal" sigma_nat nil) (sigma_nat application-judgement "nat" sigma_nat nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" 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) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_exp application-judgement "nat" exponentiation nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (upto nonempty-type-eq-decl nil naturalnumbers nil)) shostak)) (base_n_to_nat_eq 0 (base_n_to_nat_eq-1 nil 3620747774 ("" (skeep) (("" (expand "base_n_to_nat") (("" (rewrite "sigma_eq") (("" (skosimp*) (("" (inst - "n!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((base_n_to_nat const-decl "nat" base_repr nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (subrange type-eq-decl nil integers nil) (sigma_nnreal application-judgement "nnreal" sigma_nat nil) (sigma_nat application-judgement "nat" sigma_nat 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) (nat_exp application-judgement "nat" exponentiation 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) (T_low type-eq-decl nil sigma nil) (T_high type-eq-decl nil sigma nil) (<= const-decl "bool" reals nil) (> const-decl "bool" reals 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) (sigma_eq formula-decl nil sigma nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil)) shostak)) (base_n_to_nat_unique 0 (base_n_to_nat_unique-1 nil 3620749981 ("" (skeep) (("" (expand "base_n_to_nat" - 2) (("" (lemma "base_n_unique") (("" (expand "base_n_to_nat") (("" (inst - "m" "n" "LAMBDA (i:nat): IF i<=m THEN G(i) ELSE 0 ENDIF") (("1" (lemma "base_n_unique") (("1" (inst - "m" "n" "LAMBDA (i:nat): IF i<=m THEN F(i) ELSE 0 ENDIF") (("1" (assert) (("1" (skeep) (("1" (inst - "i") (("1" (inst - "i") (("1" (assert) (("1" (case "sigma(0, m, LAMBDA (s: nat): n ^ s * IF s <= m THEN F(s) ELSE 0 ENDIF) = sigma(0, m, LAMBDA (s: nat): n ^ s * F(s))") (("1" (case "sigma(0, m, LAMBDA (s: nat): n ^ s * IF s <= m THEN G(s) ELSE 0 ENDIF) = sigma(0, m, LAMBDA (s: nat): n ^ s * G(s))") (("1" (assert) nil nil) ("2" (rewrite "sigma_eq") nil nil)) nil) ("2" (rewrite "sigma_eq") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (inst - "i") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (inst - "i") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((base_n_to_nat const-decl "nat" base_repr nil) (i skolem-const-decl "nat" base_repr nil) (i skolem-const-decl "nat" base_repr nil) (nat_exp application-judgement "nat" exponentiation 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) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (sigma_nat application-judgement "nat" sigma_nat nil) (sigma_nnreal application-judgement "nnreal" sigma_nat nil) (upto nonempty-type-eq-decl nil naturalnumbers nil) (sigma_eq formula-decl nil sigma nil) (^ const-decl "real" exponentiation nil) (/= const-decl "boolean" notequal nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sigma def-decl "real" sigma nil) (T_high type-eq-decl nil sigma nil) (T_low type-eq-decl nil sigma nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (F skolem-const-decl "[nat -> nat]" base_repr nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (below type-eq-decl nil naturalnumbers 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) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (<= const-decl "bool" reals nil) (m skolem-const-decl "nat" base_repr nil) (< const-decl "bool" reals nil) (G skolem-const-decl "[nat -> nat]" base_repr nil) (> const-decl "bool" reals nil) (n skolem-const-decl "{x: nat | x > 1}" base_repr nil) (base_n_unique formula-decl nil base_repr nil)) shostak)) (base_list_TCC1 0 (base_list_TCC1-1 nil 3617546684 ("" (skolem 1 ("n" "_")) (("" (induct "k" 1 NAT_induction) (("" (skeep) (("" (skeep) (("" (expand "base_n" 1) (("" (lift-if 1) (("" (split 1) (("1" (flatten) (("1" (split 1) (("1" (propax) nil nil) ("2" (flatten) (("2" (ground) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split 2) (("1" (flatten) (("1" (lemma "mod_pos") (("1" (inst?) (("1" (flatten) nil nil)) nil)) nil)) nil) ("2" (flatten) (("2" (inst -1 "(j-mod(j, n))/n") (("1" (split -1) (("1" (inst -1 "x1-1") (("1" (ground) nil nil)) nil) ("2" (ground) (("2" (cross-mult) (("2" (both-sides "-" "j" 1) (("2" (simplify 1) (("2" (case-replace "j*n-j = (n-1)*j") (("1" (typepred (j)) (("1" (typepred (n)) (("1" (case "j>0") (("1" (case "n-1>0") (("1" (mult-ineq -1 -2) (("1" (lemma "mod_pos") (("1" (inst?) (("1" (flatten) (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil) ("2" (case-replace "j=0") (("1" (ground) nil nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split) (("1" (ground) (("1" (expand "mod") (("1" (ground) nil nil)) nil)) nil) ("2" (cross-mult) (("2" (grind) (("2" (grind) (("2" (cancel-by 1 "n") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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) (pred type-eq-decl nil defined_types nil) (< const-decl "bool" reals nil) (> const-decl "bool" reals nil) (base_n def-decl "nat" base_repr nil) (NAT_induction formula-decl nil naturalnumbers nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (x1 skolem-const-decl "nat" base_repr nil) (div_mult_pos_lt1 formula-decl nil real_props nil) (posreal nonempty-type-eq-decl nil real_types nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (gt_times_gt_any1 formula-decl nil extra_real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (both_sides_minus_lt1 formula-decl nil real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (= const-decl "[T, T -> boolean]" equalities nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (AND const-decl "[bool, bool -> bool]" booleans 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) (j skolem-const-decl "nat" base_repr nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (- const-decl "[numfield -> numfield]" number_fields nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (n skolem-const-decl "{x: nat | x > 1}" base_repr nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (int_minus_int_is_int application-judgement "int" integers 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) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (mod_pos formula-decl nil mod nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (base_list_TCC2 0 (base_list_TCC2-1 nil 3618061812 ("" (skeep) (("" (inst 1 "0") nil nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_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) (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) (below type-eq-decl nil naturalnumbers nil)) nil)) (base_list_cdr_TCC1 0 (base_list_cdr_TCC1-1 nil 3618133482 ("" (skeep) (("" (ground) (("" (ground) (("" (expand "base_list") (("" (ground) (("" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ((posint_plus_nnint_is_posint application-judgement "posint" integers nil) (base_list const-decl "listn[below(n)](digits)" base_repr nil) (array2list_it def-decl "{l: listn(n - i) | FORALL (j: subrange(i, n - 1)): a(j) = nth(l, j - i)}" array2list "structures/") (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (base_list_cdr_TCC2 0 (base_list_cdr_TCC2-1 nil 3618133482 ("" (subtype-tcc) nil nil) nil nil)) (base_list_cdr_TCC3 0 (base_list_cdr_TCC3-1 nil 3618133482 ("" (skeep) (("" (split) (("1" (expand "mod") (("1" (grind) nil nil)) nil) ("2" (cross-mult) (("2" (expand "mod") (("2" (cancel-by 1 "n") (("2" (ground) (("2" (grind) (("2" (typepred (k)) (("2" (div-by -1 "n") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((mod const-decl "{k | abs(k) < abs(j)}" mod nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (both_sides_div_pos_ge1 formula-decl nil real_props nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (zero_times1 formula-decl nil real_props 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) (pos_div_gt formula-decl nil real_props nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (both_sides_times_pos_ge1 formula-decl nil real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (integer nonempty-type-from-decl nil integers nil) (<= const-decl "bool" reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (CBD_25 skolem-const-decl "{x: nat | x > 1}" base_repr nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (nznum nonempty-type-eq-decl nil number_fields nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (NOT const-decl "[bool -> bool]" booleans nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers 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) (int_minus_int_is_int application-judgement "int" integers 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) (> 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (/= const-decl "boolean" notequal nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (< const-decl "bool" reals 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) (div_mult_pos_ge1 formula-decl nil real_props nil)) nil)) (base_list_cdr 0 (base_list_cdr-1 nil 3618133505 ("" (skeep) (("" (case "integer_pred((k-mod(k,n))/n) AND (k-mod(k,n))/n>=0") (("1" (lemma "more_list_props[below(n)].list_extensionality") (("1" (inst?) (("1" (flatten -1) (("1" (hide -1) (("1" (split -1) (("1" (propax) nil nil) ("2" (grind) nil nil) ("3" (skeep) (("3" (hide 2) (("3" (expand "base_list") (("3" (typepred "array2list[below(n)](j)(base_n(n, (k - mod(k, n)) / n))") (("1" (inst -3 "n_1") (("1" (replace -3 :dir rl) (("1" (hide (-1 -2 -3)) (("1" (case-replace "nth(cdr(array2list[below(n)](1 + j)(base_n(n, k))), n_1) = nth( array2list[below(n)](1 (("1" (typepred "array2list[below(n)](1 + j)(base_n(n, k))") (("1" (inst -3 "n_1+1") (("1" (replace -3 :dir rl) (("1" (name-replace "bnk_mod" "base_n(n, (k - mod(k, n)) / n)(n_1)") (("1" (hide (-1 -2 -3 -4)) (("1" (expand "base_n") (("1" (lift-if 1) (("1" (split 1) (("1" (flatten) (("1" (case-replace "mod(k,n)=k") (("1" (expand "bnk_mod") (("1" (replace -1) (("1" (expand "base_n") (("1" (lift-if 1) (("1" (split) (("1" (flatten) (("1" (ground) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "mod") (("2" (div-by -1 "n") (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (ground) (("2" (expand "bnk_mod") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred (n_1)) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (name-replace "CDL" "nth(cdr(array2list[below(n)](1 + j)(base_n(n, k))), n_1)") (("2" (expand "nth") (("2" (expand "CDL") (("2" (propax) nil nil)) nil)) nil)) nil) ("3" (typepred (n_1)) (("3" (ground) (("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) (("2" (typepred (n_1)) (("2" (ground) (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (split 1) (("1" (expand "mod") (("1" (ground) nil nil)) nil) ("2" (cross-mult) (("2" (expand "mod") (("2" (cancel-by 1 "n") (("2" (typepred (k)) (("2" (div-by -1 "n") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((> const-decl "bool" reals nil) (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (< const-decl "bool" reals nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (- const-decl "[numfield, numfield -> numfield]" number_fields 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) (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) (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) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (k skolem-const-decl "nat" base_repr nil) (n skolem-const-decl "{x: nat | x > 1}" base_repr nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (cdr adt-accessor-decl "[(cons?) -> list]" list_adt nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (length def-decl "nat" list_props nil) (listn type-eq-decl nil listn "structures/") (base_list const-decl "listn[below(n)](digits)" base_repr nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (j skolem-const-decl "posnat" base_repr nil) (n_1 skolem-const-decl "below(length(cdr(base_list(n, k, 1 + j))))" base_repr nil) (CDL skolem-const-decl "below(n)" base_repr nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (div_simp formula-decl nil real_props 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) (both_sides_div_pos_lt1 formula-decl nil real_props nil) (bnk_mod skolem-const-decl "nat" base_repr nil) (base_n def-decl "nat" base_repr nil) (nth def-decl "T" list_props nil) (below type-eq-decl nil nat_types nil) (NOT const-decl "[bool -> bool]" booleans 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) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (array2list_it def-decl "{l: listn(n - i) | FORALL (j: subrange(i, n - 1)): a(j) = nth(l, j - i)}" array2list "structures/") (below type-eq-decl nil naturalnumbers nil) (list_extensionality formula-decl nil more_list_props "structures/") (both_sides_div_pos_ge1 formula-decl nil real_props nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (zero_times1 formula-decl nil real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (pos_div_gt formula-decl nil real_props nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (both_sides_times_pos_ge1 formula-decl nil real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (integer nonempty-type-from-decl nil integers nil) (<= const-decl "bool" reals nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (CBD_26 skolem-const-decl "{x: nat | x > 1}" base_repr nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (div_mult_pos_ge1 formula-decl nil real_props nil)) shostak)) (base_list_faster_TCC1 0 (base_list_faster_TCC1-1 nil 3621612652 ("" (skeep) (("" (rewrite "mod_pos") nil nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (mod_pos formula-decl nil mod 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil)) nil)) (base_list_faster_TCC2 0 (base_list_faster_TCC2-1 nil 3621612652 ("" (skeep) (("" (ground) (("" (grind) nil nil)) nil)) nil) ((every adt-def-decl "boolean" list_adt nil)) nil)) (base_list_faster_TCC3 0 (base_list_faster_TCC3-1 nil 3621612652 ("" (skeep) (("" (ground) (("" (grind) nil nil)) nil)) nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (length def-decl "nat" list_props nil) (mod const-decl "{k | abs(k) < abs(j)}" mod nil)) nil)) (base_list_faster_TCC4 0 (base_list_faster_TCC4-1 nil 3621612652 ("" (skeep) (("" (rewrite "mod_pos") nil nil)) nil) ((real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (mod_pos formula-decl nil mod 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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil)) nil)) (base_list_faster_TCC5 0 (base_list_faster_TCC5-1 nil 3621612652 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (number nonempty-type-decl nil numbers nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (> const-decl "bool" reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (posnat nonempty-type-eq-decl nil integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (base_list_faster_TCC6 0 (base_list_faster_TCC6-1 nil 3621612652 ("" (termination-tcc) nil nil) nil nil)) (base_list_faster_TCC7 0 (base_list_faster_TCC7-1 nil 3621612652 ("" (skeep) (("" (grind) nil nil)) nil) ((mod const-decl "{k | abs(k) < abs(j)}" mod nil) (length def-decl "nat" list_props nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (int_minus_int_is_int application-judgement "int" integers nil)) nil)) (base_list_same 0 (base_list_same-1 nil 3621612875 ("" (induct "digits") (("1" (ground) nil nil) ("2" (ground) nil nil) ("3" (skeep) (("3" (skeep) (("3" (expand "base_list_faster" 1) (("3" (lift-if 1) (("3" (split 1) (("1" (flatten) (("1" (expand "base_list") (("1" (expand "base_n") (("1" (replace -1) (("1" (ground) (("1" (hide -1) (("1" (grind) (("1" (div-by -2 "n") (("1" (ground) (("1" (case "floor(k/n) = 0") (("1" (replace -1) (("1" (ground) nil nil)) nil) ("2" (typepred (k)) (("2" (ground) (("2" (grind) (("2" (div-by -1 "n") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) (("2" (grind) (("2" (typepred (k)) (("2" (div-by -1 "n") (("2" (div-by -3 "n") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (split -1) (("1" (inst -1 "n" "(k-mod(k,n))/n") (("1" (rewrite "base_list_cdr" :dir rl) (("1" (replace -1) (("1" (ground) (("1" (case-replace "mod(k,n)= car(base_list(n,k,1+j))") (("1" (ground) (("1" (grind) nil nil)) nil) ("2" (hide (-1 3)) (("2" (expand "base_list") (("2" (expand "base_n") (("2" (grind) (("2" (div-by -1 "n") (("2" (typepred (k)) (("2" (div-by -1 "n") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (split 1) (("1" (expand "mod") (("1" (grind) nil nil)) nil) ("2" (cross-mult 1) (("2" (lemma "mod_pos") (("2" (inst?) (("2" (grind) (("2" (cancel-by 1 "n") (("2" (typepred (k)) (("2" (grind) (("2" (grind) (("2" (grind) (("2" (div-by -1 "n") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (both_sides_div_pos_lt1 formula-decl nil real_props nil) (nonneg_real nonempty-type-eq-decl nil real_types nil) (posreal nonempty-type-eq-decl nil real_types nil) (div_simp formula-decl nil real_props nil) (/= const-decl "boolean" notequal nil) (nonzero_real nonempty-type-eq-decl nil reals nil) (integer nonempty-type-from-decl nil integers nil) (<= const-decl "bool" reals nil) (numfield nonempty-type-eq-decl nil number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil) (nznum nonempty-type-eq-decl nil number_fields nil) (/ const-decl "[numfield, nznum -> numfield]" number_fields nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (both_sides_div_pos_ge1 formula-decl nil real_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mod const-decl "{k | abs(k) < abs(j)}" mod nil) (array2list_it def-decl "{l: listn(n - i) | FORALL (j: subrange(i, n - 1)): a(j) = nth(l, j - i)}" array2list "structures/") (array2list const-decl "{l: listn(n) | FORALL (i: below(n)): a(i) = nth(l, i)}" array2list "structures/") (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (base_n def-decl "nat" base_repr nil) (mod_pos formula-decl nil mod nil) (rat_times_rat_is_rat application-judgement "rat" rationals nil) (zero_times1 formula-decl nil real_props nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (pos_div_gt formula-decl nil real_props nil) (nzrat_div_nzrat_is_nzrat application-judgement "nzrat" rationals nil) (both_sides_times_pos_ge1 formula-decl nil real_props nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (CBD_27 skolem-const-decl "{x: nat | x > 1}" base_repr nil) (bijective? const-decl "bool" functions nil) (id const-decl "(bijective?[T, T])" identity nil) (TRUE const-decl "bool" booleans nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (div_mult_pos_ge1 formula-decl nil real_props nil) (base_list_cdr formula-decl nil base_repr nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (car adt-accessor-decl "[(cons?) -> T]" list_adt nil) (n skolem-const-decl "{x: nat | x > 1}" base_repr nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (- const-decl "[numfield -> numfield]" number_fields nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (k skolem-const-decl "nat" base_repr nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nat_induction formula-decl nil naturalnumbers nil) (base_list const-decl "listn[below(n)](digits)" base_repr nil) (base_list_faster def-decl "listn[below(n)](digits)" base_repr nil) (listn type-eq-decl nil listn "structures/") (length def-decl "nat" list_props nil) (below type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (every adt-def-decl "boolean" list_adt nil) (PRED type-eq-decl nil defined_types nil) (posnat nonempty-type-eq-decl nil integers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (= const-decl "[T, T -> boolean]" equalities nil) (list type-decl nil list_adt nil) (> const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (pred type-eq-decl nil defined_types 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)) shostak)) (base_to_array_TCC1 0 (base_to_array_TCC1-1 nil 3621588317 ("" (subtype-tcc) nil nil) nil nil)) (base_to_array_TCC2 0 (base_to_array_TCC2-1 nil 3621588317 ("" (skeep) (("" (inst 1 "0") nil nil)) nil) ((real_lt_is_strict_total_order name-judgement "(strict_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) (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) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil)) nil)) (base_to_array_sound_TCC1 0 (base_to_array_sound_TCC1-1 nil 3621588317 ("" (subtype-tcc) nil nil) nil nil)) (base_to_array_sound 0 (base_to_array_sound-1 nil 3621588391 ("" (skeep) (("" (decompose-equality 1) (("1" (case "x!1<j") (("1" (expand "base_to_array") (("1" (expand "base_list") (("1" (lemma "array2list_inv[below(n)]") (("1" (inst -1 "base_n(n, k)" "0" "j" "x!1") nil nil)) nil)) nil)) nil) ("2" (flip-ineq 1) (("2" (typepred (j)) (("2" (expand "base_to_array") (("2" (rewrite "upper_is_bound") (("2" (ground) (("2" (rewrite "list2array_sound[below(n)]") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skeep) (("2" (rewrite "base_n_lt_n") nil nil)) nil)) nil)) nil) ((k skolem-const-decl "nat" base_repr nil) (n skolem-const-decl "{x: nat | x > 1}" base_repr nil) (base_n def-decl "nat" base_repr nil) (posnat nonempty-type-eq-decl nil integers nil) (list type-decl nil list_adt nil) (PRED type-eq-decl nil defined_types nil) (every adt-def-decl "boolean" list_adt nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (base_to_array const-decl "[nat -> below(n)]" base_repr nil) (= const-decl "[T, T -> boolean]" equalities nil) (length def-decl "nat" list_props nil) (listn type-eq-decl nil listn "structures/") (base_list const-decl "listn[below(n)](digits)" base_repr nil) (upper_index const-decl "nat" base_repr nil) (above nonempty-type-eq-decl nil integers nil) (below type-eq-decl nil naturalnumbers nil) (> const-decl "bool" reals nil) (< const-decl "bool" reals 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (list2array_sound formula-decl nil array2list "structures/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (upper_is_bound formula-decl nil base_repr nil) (NOT const-decl "[bool -> bool]" booleans nil) (array2list_inv formula-decl nil array2list "structures/") (j skolem-const-decl "above(upper_index(n, k))" base_repr nil) (x!1 skolem-const-decl "nat" base_repr nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (base_n_lt_n formula-decl nil base_repr nil)) shostak)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.237Angebot (Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können 2026-04-26) ¤*Eine klare Vorstellung vom Zielzustand |
|
||||||||||||||
2026-05-26