|
(factorial_props
(factorial_2n_lb_TCC1 0
(factorial_2n_lb_TCC1-1 nil 3322393244
("" (skosimp*) (("" (assert) nil nil)) nil)
((mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(factorial_2n_lb 0
(factorial_2n_lb-1 nil 3322393266
("" (case "FORALL (n: nat): n^n <= factorial(2 * n)")
(("1" (skosimp)
(("1" (inst - "n!1")
(("1" (rewrite "expt_times")
(("1" (expand "^" 1 1)
(("1" (expand "expt" 1)
(("1" (expand "expt" 1)
(("1" (expand "expt" 1)
(("1" (rewrite "sq_rew") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2"
(case "FORALL (n, N: nat): n <= N => N ^ n <= factorial(n + N)")
(("1" (skosimp)
(("1" (inst - "n!1" "n!1") (("1" (assert) nil nil)) nil))
nil)
("2" (hide 2)
(("2" (skolem 1 ("_" "N"))
(("2" (induct "n")
(("1" (assert)
(("1" (expand "^")
(("1" (expand "expt") (("1" (assert) nil nil)) nil))
nil))
nil)
("2" (skosimp*)
(("2" (assert)
(("2" (rewrite "expt_plus")
(("2" (rewrite "expt_x1")
(("2" (expand "factorial" 1)
(("2" (lemma "le_times_le_pos")
(("2"
(inst - "N^j!1" "N" "N+j!1+1"
"factorial(N+j!1)")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((pred type-eq-decl nil defined_types nil)
(nat_induction formula-decl nil naturalnumbers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(expt_x1 formula-decl nil exponentiation nil)
(le_times_le_pos formula-decl nil real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(expt_plus formula-decl nil exponentiation nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(expt_times formula-decl nil exponentiation nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nat_exp application-judgement "nat" exponentiation nil)
(nnreal_exp application-judgement "nnreal" exponentiation nil)
(expt def-decl "real" exponentiation nil)
(sq_rew formula-decl nil sq nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(sq_sqrt formula-decl nil sqrt nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(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)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(^ const-decl "real" exponentiation nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(factorial def-decl "posnat" factorial "ints/")
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields
nil))
nil))
(factorial_2np1_lb_TCC1 0
(factorial_2np1_lb_TCC1-1 nil 3322393244
("" (skosimp*) (("" (assert) nil nil)) nil)
((mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(even_plus_odd_is_odd application-judgement "odd_int" integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(factorial_2np1_lb 0
(factorial_2np1_lb-2 nil 3322393339
("" (skosimp)
(("" (lemma "factorial_2n_lb" ("n" "n!1"))
(("" (case-replace "n!1=0")
(("1" (expand "factorial")
(("1" (expand "factorial")
(("1" (rewrite "sqrt_0")
(("1" (expand "^")
(("1" (expand "expt") (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (rewrite "expt_plus" 2)
(("2" (expand "factorial" 2)
(("2" (assert)
(("2" (rewrite "expt_x1")
(("2"
(lemma "le_times_le_pos"
("nnx" "sqrt(n!1) ^ (2 * n!1)" "y"
"factorial(2 * n!1)" "nnz" "sqrt(n!1)" "w"
"1+2*n!1"))
(("2" (assert)
(("2" (hide-all-but (1 2))
(("2"
(lemma "sq_le"
("nna" "sqrt(n!1)" "nnb" "1 + 2 * n!1"))
(("2" (rewrite "sq_sqrt")
(("2" (replace -1 1 rl)
(("2" (hide -1)
(("2"
(expand "sq")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(factorial_2n_lb formula-decl nil factorial_props nil)
(expt_plus formula-decl nil exponentiation nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(/= const-decl "boolean" notequal nil)
(nzreal nonempty-type-eq-decl nil reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(nnreal type-eq-decl nil real_types nil)
(sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt nil)
(nnreal_exp application-judgement "nnreal" exponentiation nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(odd_plus_even_is_odd application-judgement "odd_int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(le_times_le_pos formula-decl nil real_props nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(sq_sqrt formula-decl nil sqrt nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(even_plus_even_is_even application-judgement "even_int" integers
nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(sq const-decl "nonneg_real" sq nil)
(sq_le formula-decl nil sq nil)
(expt_x1 formula-decl nil exponentiation nil)
(factorial def-decl "posnat" factorial "ints/")
(sqrt_0 formula-decl nil sqrt nil)
(expt def-decl "real" exponentiation nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nat_expt application-judgement "nat" exponentiation nil)
(^ const-decl "real" exponentiation nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(= const-decl "[T, T -> boolean]" equalities nil))
nil)
(factorial_2np1_lb-1 nil 3322393290
("" (skosimp)
(("" (lemma "exp_series_scaf2" ("n" "n!1"))
(("" (case-replace "n!1=0")
(("1" (expand "factorial")
(("1" (expand "factorial")
(("1" (rewrite "sqrt_0")
(("1" (expand "^")
(("1" (expand "expt") (("1" (assert) nil)))))))))))
("2" (rewrite "expt_plus" 2)
(("2" (expand "factorial" 2)
(("2" (assert)
(("2" (rewrite "expt_x1")
(("2"
(lemma "le_times_le_pos"
("nnx" "sqrt(n!1) ^ (2 * n!1)" "y"
"factorial(2 * n!1)" "nnz" "sqrt(n!1)" "w"
"1+2*n!1"))
(("2" (assert)
(("2" (hide-all-but (1 2))
(("2"
(lemma "sq_le"
("nna" "sqrt(n!1)" "nnb" "1 + 2 * n!1"))
(("2" (rewrite "sq_sqrt")
(("2" (replace -1 1 rl)
(("2" (hide -1)
(("2"
(expand "sq")
(("2"
(assert)
nil))))))))))))))))))))))))))))))
nil)
nil nil)))
¤ Dauer der Verarbeitung: 0.20 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.
|
