|
(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)
(("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)
(("1"
(case
"0)
(("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)
(("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)
(("1"
(case
"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"
(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"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.71 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
