|
(fundamental_algebra
(mult_0_l 0
(mult_0_l-1 nil 3595844278
("" (skeep)
(("" (assert)
(("" (lemma " idempotent_rectangular")
(("" (inst-cp - "0*c")
(("" (inst - "0")
(("" (assert)
(("" (replace -2)
(("" (invoke (name "A" "%1") (! 1 1))
(("" (replace -1)
(("" (replace -2 +)
(("" (hide -)
(("" (expand "A")
(("" (expand "rectangular")
(("" (rewrite "Re_times")
((""
(rewrite "Im_times")
((""
(assert)
((""
(rewrite "Im_real")
((""
(rewrite "Re_real")
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((complex_times_complex_is_complex application-judgement "complex"
complex_types 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)
(complex_pred const-decl "[number_field -> boolean]" complex_types
nil)
(complex nonempty-type-from-decl nil complex_types nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(from_rectangular const-decl "complex" polar nil)
(rectangular const-decl "[real, real]" polar nil)
(A skolem-const-decl "complex" fundamental_algebra nil)
(Re_times formula-decl nil arithmetic nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(complex_minus_complex_is_complex application-judgement "complex"
complex_types nil)
(Re_real formula-decl nil arithmetic nil)
(real_times_real_is_real application-judgement "real" reals nil)
(Im_real formula-decl nil arithmetic nil)
(complex_plus_complex_is_complex application-judgement "complex"
complex_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(Im_times formula-decl nil arithmetic nil)
(idempotent_rectangular formula-decl nil polar nil))
shostak))
(mult_commutes 0
(mult_commutes-1 nil 3595844876
("" (skeep)
(("" (lemma "commutative_mult") (("" (inst?) nil nil)) nil)) nil)
((commutative_mult formula-decl nil number_fields nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(complex_pred const-decl "[number_field -> boolean]" complex_types
nil)
(complex nonempty-type-from-decl nil complex_types nil))
shostak))
(cpow_TCC1 0
(cpow_TCC1-1 nil 3595783444 ("" (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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(complex_minus_complex_is_complex application-judgement "complex"
complex_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(cpow_TCC2 0
(cpow_TCC2-1 nil 3595783444 ("" (termination-tcc) nil nil) nil nil))
(cpow_0 0
(cpow_0-1 nil 3595945547
(""
(case " FORALL (c: complex, n: nat): cpow(c)(n+1) = 0 IFF c = 0")
(("1" (skeep)
(("1" (inst - "c" "pn-1") (("1" (assert) nil nil)) nil)) nil)
("2" (hide 2)
(("2" (induct "n")
(("1" (grind) nil nil)
("2" (skeep)
(("2" (skeep)
(("2" (inst - "c")
(("2" (assert)
(("2" (expand "cpow" +)
(("2" (lemma " zero_times3")
(("2" (inst?)
(("2" (replaces -1) (("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((zero_times3 formula-decl nil number_fields_bis nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nat_induction formula-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types nil)
(int_plus_int_is_int application-judgement "int" integers 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)
(complex_minus_complex_is_complex application-judgement "complex"
complex_types nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(complex_plus_complex_is_complex application-judgement "complex"
complex_types nil)
(nnint_plus_posint_is_posint application-judgement "posint"
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)
(complex_pred const-decl "[number_field -> boolean]" complex_types
nil)
(complex nonempty-type-from-decl nil complex_types 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)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(cpow def-decl "complex" fundamental_algebra nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields
nil))
shostak))
(cpow_real_TCC1 0
(cpow_real_TCC1-1 nil 3596554202 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(cpow_real 0
(cpow_real-1 nil 3596554203
("" (induct "n")
(("1" (grind) nil nil)
("2" (skeep)
(("2" (skeep)
(("2" (inst - "r")
(("2" (expand "cpow" +)
(("2" (expand "^")
(("2" (expand "expt" +)
(("2" (assert) (("2" (replaces -1) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_times_real_is_real application-judgement "real" reals nil)
(complex_times_complex_is_complex application-judgement "complex"
complex_types nil)
(expt def-decl "real" exponentiation nil)
(nat_induction formula-decl nil naturalnumbers nil)
(^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(cpow def-decl "complex" fundamental_algebra nil)
(complex nonempty-type-from-decl nil complex_types nil)
(complex_pred const-decl "[number_field -> boolean]" complex_types
nil)
(= const-decl "[T, T -> boolean]" equalities 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))
(abs_rewrite_TCC1 0
(abs_rewrite_TCC1-1 nil 3595939197 ("" (subtype-tcc) nil nil)
((/= const-decl "boolean" notequal nil)) nil))
(abs_rewrite_TCC2 0
(abs_rewrite_TCC2-1 nil 3595939197
("" (skeep)
(("" (case "FORALL (xy:real): xy*xy>=0")
(("1" (inst-cp - "s")
(("1" (inst - "r") (("1" (grind) nil nil)) nil)) nil)
("2" (hide 2)
(("2" (skeep)
(("2" (lemma "nnreal_times_nnreal_is_nnreal")
(("2" (inst - "xy" "xy")
(("2" (lemma "nnreal_times_nnreal_is_nnreal")
(("2" (inst - "-xy" "-xy")
(("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_times_real_is_real application-judgement "real" reals nil)
(complex_times_complex_is_complex application-judgement "complex"
complex_types nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(complex_plus_complex_is_complex application-judgement "complex"
complex_types nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(^ const-decl "real" exponentiation nil)
(expt def-decl "real" exponentiation nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(xy skolem-const-decl "real" fundamental_algebra nil)
(minus_real_is_real application-judgement "real" reals nil)
(minus_complex_is_complex application-judgement "complex"
complex_types nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(nnreal_times_nnreal_is_nnreal judgement-tcc nil real_types nil))
nil))
(abs_rewrite 0
(abs_rewrite-1 nil 3595939199
("" (skeep)
(("" (expand "abs")
(("" (expand "conjugate")
(("" (assert)
(("" (rewrite "Re_plus")
(("" (rewrite "Im_plus")
(("" (rewrite "Re_imag")
(("" (rewrite "Re_real")
(("" (rewrite "Im_imag")
(("" (rewrite "Im_real")
(("" (assert)
(("" (lemma "i_axiom")
(("" (replace -1) (("" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((complex_times_complex_is_complex application-judgement "complex"
complex_types nil)
(abs const-decl "nnreal" polar nil)
(complex_plus_complex_is_complex application-judgement "complex"
complex_types nil)
(Im_plus formula-decl nil arithmetic nil)
(Re_real formula-decl nil arithmetic nil)
(Im_real formula-decl nil arithmetic nil)
(real_times_real_is_real application-judgement "real" reals nil)
(i_axiom formula-decl nil complex_types nil)
(expt def-decl "real" exponentiation nil)
(^ const-decl "real" exponentiation nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(minus_nzcomplex_is_nzcomplex application-judgement "nzcomplex"
complex_types nil)
(Im_imag formula-decl nil arithmetic nil)
(Re_imag formula-decl nil arithmetic nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(i const-decl "complex" complex_types nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(complex nonempty-type-from-decl nil complex_types nil)
(complex_pred const-decl "[number_field -> boolean]" complex_types
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)
(Re_plus formula-decl nil arithmetic nil)
(conjugate const-decl "complex" arithmetic nil)
(complex_minus_complex_is_complex application-judgement "complex"
complex_types nil)
(Re_is_real application-judgement "real" complex_types nil)
(Im_is_real application-judgement "real" complex_types nil))
shostak))
(arg_cpow 0
(arg_cpow-1 nil 3595945241
(""
(case "FORALL (c: complex, n: nat):
-pi < (1+n) * arg(c) AND (1+n) * arg(c) <= pi IMPLIES
arg(cpow(c)((1+n))) = (1+n) * arg(c)")
(("1" (skeep)
(("1" (inst - "c" "pn-1") (("1" (assert) nil nil)) nil)) nil)
("2" (hide 2)
(("2" (induct "n")
(("1" (skeep) (("1" (assert) (("1" (grind) nil nil)) nil)) nil)
("2" (skeep)
(("2" (skeep)
(("2" (inst - "c")
(("2" (assert)
(("2" (split -)
(("1" (expand "cpow" 1)
(("1" (rewrite "arg_mult")
(("1" (assert) nil nil)
("2" (flatten)
(("2" (lemma "cpow_0")
(("2" (inst?)
(("2" (assert)
(("2"
(replaces -1)
(("2"
(assert)
(("2"
(expand "arg" +)
(("2"
(assert)
(("2"
(lift-if)
(("2"
(ground)
(("1"
(rewrite "zero_times1")
nil
nil)
("2"
(rewrite "zero_times1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (flatten)
(("3" (replaces -1)
(("3" (assert)
(("3" (expand "arg" +)
(("3"
(lift-if)
(("3"
(split +)
(("1" (assert) nil nil)
("2"
(flatten)
(("2"
(rewrite "zero_times1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (hide 2)
(("2" (case "arg(c)>=0")
(("1" (copy -1)
(("1" (mult-by -1 "j")
(("1" (assert) nil nil)) nil))
nil)
("2" (copy 1)
(("2" (mult-by 1 "j")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("3" (hide 2)
(("3" (case "arg(c)>=0")
(("1" (copy 1)
(("1" (copy -1)
(("1" (mult-by -1 "j")
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (copy 1)
(("2" (mult-by 1 "j") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nzcomplex nonempty-type-eq-decl nil complex_types nil)
(/= const-decl "boolean" notequal nil)
(arg_mult formula-decl nil polar nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(cpow_0 formula-decl nil fundamental_algebra 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)
(nil application-judgement "nnreal_lt_2pi" atan2 "trig/")
(zero_times1 formula-decl nil number_fields_bis nil)
(both_sides_times_pos_ge1 formula-decl nil real_props nil)
(both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
nil)
(j skolem-const-decl "nat" fundamental_algebra nil)
(atan2 const-decl "real" atan2 "trig/")
(nzcomplex_times_nzcomplex_is_nzcomplex application-judgement
"nzcomplex" complex_types nil)
(nzcomplex_div_nzcomplex_is_nzcomplex application-judgement
"nzcomplex" complex_types nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nat_induction formula-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types 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)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(complex_minus_complex_is_complex application-judgement "complex"
complex_types nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_nzcomplex_is_nzcomplex application-judgement "nzcomplex"
complex_types nil)
(minus_nzreal_is_nzreal application-judgement "nzreal" real_types
nil)
(complex_times_complex_is_complex application-judgement "complex"
complex_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(complex_plus_complex_is_complex application-judgement "complex"
complex_types 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)
(complex_pred const-decl "[number_field -> boolean]" complex_types
nil)
(complex nonempty-type-from-decl nil complex_types 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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(< const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield -> numfield]" number_fields 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)
(pi_lb const-decl "posreal" trig_basic "trig/")
(pi_ub const-decl "posreal" trig_basic "trig/")
(pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
"trig/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(<= const-decl "bool" reals nil)
(argrng nonempty-type-eq-decl nil polar nil)
(arg const-decl "argrng" polar nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(cpow def-decl "complex" fundamental_algebra nil))
shostak))
(abs_cpow_TCC1 0
(abs_cpow_TCC1-1 nil 3595784497 ("" (subtype-tcc) nil nil)
((conjugate const-decl "complex" arithmetic nil)
(abs const-decl "nnreal" polar nil)
(Im_is_real application-judgement "real" complex_types nil)
(complex_times_complex_is_complex application-judgement "complex"
complex_types nil))
nil))
(abs_cpow 0
(abs_cpow-1 nil 3595784503
("" (induct "n")
(("1" (skeep)
(("1" (expand "cpow")
(("1" (expand "^")
(("1" (expand "expt")
(("1" (rewrite "abs_real_rew") nil nil)) nil))
nil))
nil))
nil)
("2" (skeep)
(("2" (skeep)
(("2" (inst - "c")
(("2" (expand "^")
(("2" (expand "expt" +)
(("2" (replaces -1 + :dir rl)
(("2" (rewrite "abs_mult" :dir rl)
(("2" (expand "cpow" 1 1) (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((abs_mult formula-decl nil polar nil)
(complex_times_complex_is_complex application-judgement "complex"
complex_types nil)
(nnreal_expt application-judgement "nnreal" exponentiation nil)
(nzint_abs_is_pos application-judgement "{j: posint | j >= i}"
real_defs nil)
(int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
real_defs nil)
(nzrat_abs_is_pos application-judgement "{r: posrat | r >= q}"
real_defs nil)
(abs_nat formula-decl nil abs_lems "reals/")
(abs_real_rew formula-decl nil polar nil)
(expt def-decl "real" exponentiation nil)
(nat_induction formula-decl nil naturalnumbers nil)
(^ const-decl "real" exponentiation nil)
(/= const-decl "boolean" notequal nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(cpow def-decl "complex" fundamental_algebra nil)
(abs const-decl "nnreal" polar nil)
(nnreal type-eq-decl nil real_types nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(complex nonempty-type-from-decl nil complex_types nil)
(complex_pred const-decl "[number_field -> boolean]" complex_types
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))
(abs_cpow_increasing 0
(abs_cpow_increasing-1 nil 3595784734
("" (skeep)
(("" (rewrite "abs_cpow")
(("" (rewrite "abs_cpow")
(("" (case "abs(y)=0")
(("1" (assert) nil nil)
("2" (case "abs(x)=0")
(("1" (assert)
(("1" (replaces -1)
(("1" (assert)
(("1" (expand "^" 2 1)
(("1" (expand "expt")
(("1" (lift-if)
(("1" (ground)
(("1" (replaces -1) (("1" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "both_sides_expt_pos_ge_aux")
(("2" (case "n = 0")
(("1" (replaces -1)
(("1" (hide -1) (("1" (grind) nil nil)) nil)) nil)
("2" (inst - "n-1" "abs(x)" "abs(y)")
(("1" (assert)
(("1" (expand "^") (("1" (assert) nil nil)) nil))
nil)
("2" (assert) nil nil) ("3" (assert) nil nil)
("4" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((abs_cpow formula-decl nil fundamental_algebra 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)
(complex_pred const-decl "[number_field -> boolean]" complex_types
nil)
(complex nonempty-type-from-decl nil complex_types 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)
(nnreal_exp application-judgement "nnreal" exponentiation nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nnreal type-eq-decl nil real_types nil)
(abs const-decl "nnreal" polar nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(both_sides_expt_pos_ge_aux formula-decl nil exponentiation nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(n skolem-const-decl "nat" fundamental_algebra nil)
(> const-decl "bool" reals nil)
(x skolem-const-decl "complex" fundamental_algebra nil)
(y skolem-const-decl "complex" fundamental_algebra nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(complex_plus_complex_is_complex application-judgement "complex"
complex_types nil)
(nat_exp application-judgement "nat" exponentiation nil)
(expt def-decl "real" exponentiation nil)
(complex_minus_complex_is_complex application-judgement "complex"
complex_types nil)
(nat_expt application-judgement "nat" exponentiation 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)
(complex_times_complex_is_complex application-judgement "complex"
complex_types nil)
(conjugate const-decl "complex" arithmetic nil)
(nnreal_expt application-judgement "nnreal" exponentiation nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(^ const-decl "real" exponentiation nil))
shostak))
(cpow_exp 0
(cpow_exp-1 nil 3595843810
("" (induct "n")
(("1" (skeep)
(("1" (assert)
(("1" (rewrite "mult_0_l")
(("1" (expand "cpow") (("1" (rewrite "exp_0") nil nil)) nil))
nil))
nil))
nil)
("2" (skeep)
(("2" (assert)
(("2" (skeep)
(("2" (inst - "c")
(("2" (assert)
(("2" (rewrite "exp_plus")
(("2" (lemma "mult_commutes")
(("2" (inst?)
(("2" (replace -1)
(("2" (replace -2 :dir rl)
(("2" (expand "cpow" 1 1)
(("2" (lemma "mult_commutes")
(("2" (inst - "exp(c)" _)
(("2" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(complex_plus_complex_is_complex application-judgement "complex"
complex_types nil)
(mult_commutes formula-decl nil fundamental_algebra nil)
(nzcomplex_times_nzcomplex_is_nzcomplex application-judgement
"nzcomplex" complex_types nil)
(exp_plus formula-decl nil exp nil)
(mult_0_l formula-decl nil fundamental_algebra nil)
(exp_0 formula-decl nil exp nil)
(nat_induction formula-decl nil naturalnumbers nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(exp const-decl "nzcomplex" exp nil)
(nzcomplex nonempty-type-eq-decl nil complex_types nil)
(/= const-decl "boolean" notequal nil)
(cpow def-decl "complex" fundamental_algebra nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(complex nonempty-type-from-decl nil complex_types nil)
(complex_pred const-decl "[number_field -> boolean]" complex_types
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)
(complex_times_complex_is_complex application-judgement "complex"
complex_types nil))
shostak))
(cpow_mult 0
(cpow_mult-1 nil 3596548864
("" (induct "n")
(("1" (grind) nil nil)
("2" (skeep)
(("2" (skeep)
(("2" (inst - "x" "y")
(("2" (expand "cpow" +)
(("2" (replace -1 :dir rl) (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((nat_induction formula-decl nil naturalnumbers nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(cpow def-decl "complex" fundamental_algebra nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(complex nonempty-type-from-decl nil complex_types nil)
(complex_pred const-decl "[number_field -> boolean]" complex_types
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)
(complex_times_complex_is_complex application-judgement "complex"
complex_types nil))
shostak))
(complex_continuous_sum 0
(complex_continuous_sum-1 nil 3596302109
("" (skeep)
(("" (expand "complex_continuous?")
(("" (skeep)
(("" (inst - "x" "epsil/4")
(("" (inst - "x" "epsil/4")
(("" (skosimp*)
(("" (inst + "min(delta!1,delta!2)")
(("" (skeep)
(("" (inst - "y")
(("" (inst - "y")
(("" (assert)
(("" (expand "cfunplus")
(("" (lemma "abs_triangle")
(("" (inst - "ff(x)-ff(y)" "gg(x)-gg(y)")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((complex_continuous? const-decl "bool" fundamental_algebra nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nzcomplex_div_nzcomplex_is_nzcomplex application-judgement
"nzcomplex" complex_types 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)
(complex_pred const-decl "[number_field -> boolean]" complex_types
nil)
(complex nonempty-type-from-decl nil complex_types 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)
(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)
(cfunplus const-decl "complex" fundamental_algebra nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(complex_plus_complex_is_complex application-judgement "complex"
complex_types nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(abs_triangle formula-decl nil polar nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(complex_minus_complex_is_complex application-judgement "complex"
complex_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(posreal_min application-judgement
"{z: posreal | z <= x AND z <= y}" real_defs nil))
shostak))
(complex_continuous_mult 0
(complex_continuous_mult-1 nil 3596302712
("" (skeep)
(("" (expand "complex_continuous?")
(("" (skeep)
(("" (name "epf" "min(1/2,epsil/(8*abs(gg(x))+8))")
(("" (name "epg" "epsil/(8*abs(ff(x))+8)")
(("" (inst - "x" "epf")
(("" (inst - "x" "epg")
(("" (skolem - "def")
(("" (skolem - "deg")
(("" (name "delt" "min(def,deg)")
(("" (inst + "delt")
(("" (skeep)
(("" (inst - "y")
(("" (inst - "y")
((""
(assert)
((""
(expand "cfunmult")
((""
(lemma "abs_triangle")
((""
(inst
-
"(ff(x)-ff(y))*gg(x)"
"ff(y)*(gg(x)-gg(y))")
((""
(invoke
(case
"%1 < epsil/2 AND %2<=epsil/2")
(! -1 2 1)
(! -1 2 2))
(("1"
(flatten)
(("1" (assert) nil nil))
nil)
("2"
(hide (-1 2))
(("2"
(split)
(("1"
(rewrite "abs_mult")
(("1"
(mult-by
-4
"abs(gg(x))")
(("1"
(case
"epf*abs(gg(x))<=epsil/2")
(("1"
(assert)
nil
nil)
("2"
(hide (-4 2))
(("2"
(case
"abs(gg(x)) / (8 + 8 * abs(gg(x))) <= 1/2")
(("1"
(mult-by
-1
"epsil")
(("1"
(assert)
(("1"
(expand
"epf")
(("1"
(expand
"min"
1)
(("1"
(lift-if)
(("1"
(ground)
(("1"
(cross-mult
1)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(cross-mult
1)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(rewrite "abs_mult")
(("2"
(case
"(abs(ff(x))+1)*abs((gg(x) - gg(y))) <= epsil / 2")
(("1"
(case
"abs(ff(y))<=abs(ff(x))+1")
(("1"
(mult-by
-1
"abs(gg(x)-gg(y))")
(("1"
(assert)
nil
nil))
nil)
("2"
(hide 2)
(("2"
(case
"NOT abs(ff(x)-ff(y))<=1/2")
(("1"
(expand "min")
(("1"
(lift-if)
(("1"
(ground)
nil
nil))
nil))
nil)
("2"
(hide-all-but
(-1 1))
(("2"
(lemma
"abs_triangle_minus")
(("2"
(inst
-
"ff(y)"
"ff(x)")
(("2"
(case
"ff(y)-ff(x) = -(ff(x)-ff(y))")
(("1"
(replaces
-1)
(("1"
(rewrite
"abs_neg")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(assert)
(("2"
(hide-all-but
1)
(("2"
(lemma
"neg_times_neg")
(("2"
(inst
-
"ff(x)-ff(y)"
"-1")
(("2"
(assert)
(("2"
(rewrite
"mult_commutes")
(("2"
(assert)
(("2"
(lemma
"identity_mult")
(("2"
(inst?)
(("2"
(replaces
-1)
(("2"
(replaces
-1)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(mult-by
-5
"abs(ff(x))+1")
(("2"
(case
"epg*(abs(ff(x))+1)<=epsil/2")
(("1"
(assert)
nil
nil)
("2"
(hide (2 3))
(("2"
(name
"DG"
"abs(ff(x))+1")
(("2"
(replace -1)
(("2"
(expand
"epg"
1
:assert?
none)
(("2"
(case
"DG/(8 * abs(ff(x)) + 8) <= 1/2")
(("1"
(mult-by
-1
"epsil")
(("1"
(assert)
nil
nil))
nil)
("2"
(cross-mult
1)
(("2"
(expand
"DG"
1)
(("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))
nil))
nil))
nil))
nil))
nil))
nil)
((complex_continuous? const-decl "bool" fundamental_algebra nil)
(abs const-decl "nnreal" polar nil)
(nnreal type-eq-decl nil real_types nil)
(complex nonempty-type-from-decl nil complex_types nil)
(complex_pred const-decl "[number_field -> boolean]" complex_types
nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(> const-decl "bool" reals nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(/ 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)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(posreal_min application-judgement
"{z: posreal | z <= x AND z <= y}" real_defs nil)
(posreal_div_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nnreal_plus_posreal_is_posreal application-judgement "posreal"
real_types nil)
(posrat_div_posrat_is_posrat application-judgement "posrat"
rationals nil)
(nzcomplex_div_nzcomplex_is_nzcomplex application-judgement
"nzcomplex" complex_types nil)
(posreal_plus_nnreal_is_posreal application-judgement "posreal"
real_types nil)
(complex_plus_complex_is_complex application-judgement "complex"
complex_types nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(complex_times_complex_is_complex application-judgement "complex"
complex_types nil)
(cfunmult const-decl "complex" fundamental_algebra nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(DG skolem-const-decl "posreal" fundamental_algebra nil)
(epg skolem-const-decl "posreal" fundamental_algebra nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(abs_triangle_minus formula-decl nil polar nil)
(minus_complex_is_complex application-judgement "complex"
complex_types nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(abs_neg formula-decl nil polar nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(minus_nzcomplex_is_nzcomplex application-judgement "nzcomplex"
complex_types nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(mult_commutes formula-decl nil fundamental_algebra nil)
(identity_mult formula-decl nil number_fields nil)
(neg_times_neg formula-decl nil number_fields_bis nil)
(abs_mult formula-decl nil polar nil)
(complex_div_nzcomplex_is_complex application-judgement "complex"
complex_types nil)
(nnreal_div_posreal_is_nnreal application-judgement "nnreal"
real_types nil)
(posreal_times_posreal_is_posreal application-judgement "posreal"
real_types nil)
(nzcomplex_times_nzcomplex_is_nzcomplex application-judgement
"nzcomplex" complex_types nil)
(times_div2 formula-decl nil number_fields_bis nil)
(div_mult_pos_gt1 formula-decl nil extra_real_props nil)
(div_mult_pos_gt2 formula-decl nil extra_real_props nil)
(epf skolem-const-decl
"{z: posreal | z <= 1/2 AND z <= epsil / (8 + 8 * abs(gg(x)))}"
fundamental_algebra nil)
(both_sides_times_pos_le1_imp formula-decl nil extra_real_props
nil)
(div_mult_pos_le1 formula-decl nil real_props nil)
(div_mult_pos_le2 formula-decl nil real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(gg skolem-const-decl "[complex -> complex]" fundamental_algebra
nil)
(x skolem-const-decl "complex" fundamental_algebra nil)
(both_sides_times_pos_lt1 formula-decl nil real_props nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(< const-decl "bool" reals nil)
(abs_triangle formula-decl nil polar nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(complex_minus_complex_is_complex application-judgement "complex"
complex_types nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(complex_continuous_cpow 0
(complex_continuous_cpow-1 nil 3596304212
("" (induct "n")
(("1" (grind) nil nil)
("2" (skeep)
(("2" (skeep)
(("2" (inst - "c")
(("2" (lemma "complex_continuous_mult")
(("2" (inst - "LAMBDA (x): c*cpow(x)(j)" "LAMBDA (x): x")
(("2" (split -)
(("1" (expand "cfunmult")
(("1" (expand "cpow" +)
(("1" (assert)
(("1" (invoke (name "bb" "%1") (! 1 1))
(("1" (replace -1)
(("1" (invoke (name "ggv" "%1") (! -2 1))
(("1" (replace -1)
(("1"
(case "ggv = bb")
(("1" (assert) nil nil)
("2"
(decompose-equality)
(("2"
(expand "ggv" 1)
(("2"
(expand "bb" 1)
(("2"
(assert)
(("2"
(hide-all-but 1)
(("2"
(lemma "mult_commutes")
(("2"
(inst?)
(("2"
(replace -1)
(("2"
(hide -)
(("2"
(lemma
"mult_commutes")
(("2"
(inst
-
"cpow(x!1)(j)"
"x!1")
(("2"
(assert)
(("2"
(replaces
-1
:dir
rl)
(("2"
(assert)
(("2"
(lemma
"associative_mult")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.74 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
