Quelle trigx.prf
Sprache: Lisp
(trigxnil 3394178341"" (rewrite "sin_pi2" ) (("" (assert ) nil nil )) nil )nil trig_basic "trig_fnd/" )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" ))nil ))nil 3394178341"" (rewrite "cos_0" ) (("" (assert ) nil nil )) nil )nil trig_basic "trig_fnd/" )) nil ))nil 3394178341"" (expand "cauchy_sin_nz?" )"" (lemma "lemma_div2n" ("x" "pi" "cx" "cauchy_pi" "n" "1" ))"" (rewrite "pi_lemma" )"" (expand "div2n" )"" (rewrite "expt_x1" )"" (inst + "pi / 2" )"" (rewrite "sin_pi2" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"posreal" atan "trig_fnd/" )nil real_types nil )"bool" reals nil )nil real_types nil )"cauchy_real" atanx nil )nil cauchy nil )"bool" cauchy nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil shift nil )"real" shift nil )"trig_range" sincos_def"trig_fnd/" )"posreal" nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )nil number_fields nil )nil trigx nil )"real" sincos_def "trig_fnd/" )"boolean" notequal nil )nil trig_basic "trig_fnd/" )"posint" exponentiation nil )"{r: posreal | pi_lb < r AND r < pi_ub}" "trig_fnd/" )nil exponentiation nil )nil atanx nil )"bool" trigx nil ))nil ))nil 3394178341"" (expand "cauchy_cos_nz?" )"" (inst + "0" )"1" (expand "cauchy_prop" )"1" (skosimp)"1" (assert )"1" (expand "cauchy_zero" ) (("1" (propax) nil nil )) nil ))nil ))nil ))nil )"2" (rewrite "cos_0" ) (("2" (assert ) nil nil )) nil ))nil ))nil )"trig_range" sincos_def"trig_fnd/" )"real" sincos_def "trig_fnd/" )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"boolean" notequal nil )nil booleans nil )nil numbers nil )nil trigx nil )"cauchy_nnreal" cauchy nil )"(strict_total_order?[real])" real_props nil )"int" integers nil )"int" integers nil )"nonneg_int" nil )"even_int" integersnil )"(divides(n))" divides nil )"(divides(m))" divides nil )"bool" cauchy nil )"posint" exponentiation nil )nil trig_basic "trig_fnd/" )"bool" trigx nil ))nil ))nil 3394178341"" (skosimp)"" (typepred "x!1" )"" (expand "cauchy_sin_nz?" )"" (skosimp)"" (expand "cauchy_real?" ) (("" (inst + "nsx!1" ) nil nil ))nil ))nil ))nil ))nil ))nil )nil trigx nil )"bool" trigx nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil trigx nil )"real" sincos_def "trig_fnd/" )"boolean" notequal nil )"bool" cauchy nil ))nil ))nil 3394178341"" (skosimp)"" (typepred "x!1" )"" (expand "cauchy_cos_nz?" )"" (skosimp)"" (expand "cauchy_real?" ) (("" (inst + "ncx!1" ) nil nil ))nil ))nil ))nil ))nil ))nil )nil trigx nil )"bool" trigx nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )nil trigx nil )"real" sincos_def "trig_fnd/" )"boolean" notequal nil )"bool" cauchy nil ))nil ))nil 3394179601"" (skosimp)"" (typepred "cncx!1" )"" (expand "cauchy_cos_nz?" )"" (skosimp)"" (typepred "ncx!1" )"" (expand "cauchy_nzreal?" )"" (inst + "cos(ncx!1)" )"" (lemma "cos_lemma" ("x" "ncx!1" "cx" "cncx!1" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil trigx nil )"bool" trigx nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" cauchy nil )nil sincosx nil )"bool" cauchy nil )nil cauchy nil )nil reals nil )"trig_range" sincos_def"trig_fnd/" )nil trigx nil )"real" sincos_def "trig_fnd/" )"boolean" notequal nil ))nil ))nil 3394179601"" (skosimp)"" (typepred "cnsx!1" )"" (expand "cauchy_sin_nz?" )"" (skosimp)"" (typepred "nsx!1" )"" (expand "cauchy_nzreal?" )"" (lemma "sin_lemma" ("x" "nsx!1" "cx" "cnsx!1" ))"" (inst + "sin(nsx!1)" ) (("" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil trigx nil )"bool" trigx nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" cauchy nil )"trig_range" sincos_def"trig_fnd/" )nil reals nil )nil sincosx nil )"bool" cauchy nil )nil cauchy nil )nil trigx nil )"real" sincos_def "trig_fnd/" )"boolean" notequal nil ))nil ))nil 3394179601"" (skosimp) (("" (typepred "ncx!1" ) (("" (assert ) nil nil )) nil ))nil )nil trigx nil )"real" sincos_def "trig_fnd/" )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"boolean" notequal nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"trig_range" sincos_def"trig_fnd/" ))nil ))nil 3394179601"" (skosimp) (("" (typepred "nsx!1" ) (("" (assert ) nil nil )) nil ))nil )nil trigx nil )"real" sincos_def "trig_fnd/" )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"boolean" notequal nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"trig_range" sincos_def"trig_fnd/" ))nil ))nil 3394180068"" (skosimp)"" (expand "sec" )"" (expand "cauchy_sec" )"" (lemma "cos_lemma" ("x" "ncx!1" "cx" "cncx!1" ))"" (assert )"" "inv_lemma" "nzx" "cos(ncx!1)" "nzcx" "cauchy_cos(cncx!1)" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"nzreal" trigx nil )nil trigx nil )"real" sincos_def "trig_fnd/" )"boolean" notequal nil )nil trigx nil )"bool" trigx nil )nil cauchy nil )"bool" cauchy nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sincosx nil )nil reals nil )"cauchy_real" sincosx nil )nil cauchy nil )"bool" cauchy nil )nil inv nil )"nzreal" nil )"trig_range" sincos_def"trig_fnd/" )"cauchy_nzreal" trigx nil ))nil 3394180131"" (skosimp)"" (expand "cosec" )"" (expand "cauchy_cosec" )"" (lemma "sin_lemma" ("x" "nsx!1" "cx" "cnsx!1" ))"" (assert )"" "inv_lemma" "nzx" "sin(nsx!1)" "nzcx" "cauchy_sin(cnsx!1)" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"nzreal" trigx nil )nil trigx nil )"real" sincos_def "trig_fnd/" )"boolean" notequal nil )nil trigx nil )"bool" trigx nil )nil cauchy nil )"bool" cauchy nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sincosx nil )nil reals nil )"cauchy_real" sincosx nil )nil cauchy nil )"bool" cauchy nil )nil inv nil )"nzreal" nil )"trig_range" sincos_def"trig_fnd/" )"cauchy_nzreal" trigx nil ))nil 3394179601"" (skosimp)"" (typepred "ncx!1" )"" (expand "Tan?" ) (("" (propax) nil nil )) nil )) nil ))nil )nil trigx nil )"real" sincos_def "trig_fnd/" )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"boolean" notequal nil )nil numbers nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" sincos_def "trig_fnd/" ))nil ))nil 3394180209"" (skosimp)"" (expand "tan" )"" (expand "cauchy_tan" )"" (lemma "sin_lemma" ("x" "ncx!1" "cx" "cncx!1" ))"" (lemma "cos_lemma" ("x" "ncx!1" "cx" "cncx!1" ))"" (assert )"" "div_lemma" "x" "sin(ncx!1)" "cx" "cauchy_sin(cncx!1)" "nzy" "cos(ncx!1)" "nzcy" "cauchy_cos(cncx!1)" ))"" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"real" sincos_def "trig_fnd/" )nil trigx nil )"real" sincos_def "trig_fnd/" )"boolean" notequal nil )nil trigx nil )"bool" trigx nil )nil cauchy nil )"bool" cauchy nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sincosx nil )"trig_range" sincos_def"trig_fnd/" )"trig_range" sincos_def"trig_fnd/" )"real" reals nil )nil div nil )"cauchy_real" sincosx nil )"bool" cauchy nil )nil cauchy nil )"cauchy_real" sincosx nil )nil reals nil )"real" sincos_def "trig_fnd/" )nil sincosx nil )"cauchy_real" trigx nil ))nil 3394180301"" (skosimp)"" (lemma "sin_lemma" ("x" "nsx!1" "cx" "cnsx!1" ))"" (lemma "cos_lemma" ("x" "nsx!1" "cx" "cnsx!1" ))"" (assert )"" "div_lemma" "nzy" "sin(nsx!1)" "nzcy" "cauchy_sin(cnsx!1)" "x" "cos(nsx!1)" "cx" "cauchy_cos(cnsx!1)" ))"1" (expand "cot" )"1" (expand "cauchy_cot" ) (("1" (assert ) nil nil ))nil ))nil )"2" (expand "cauchy_nzreal?" )"2" (inst + "sin(nsx!1)" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil trigx nil )"real" sincos_def "trig_fnd/" )"boolean" notequal nil )nil trigx nil )"bool" trigx nil )nil cauchy nil )"bool" cauchy nil )nil naturalnumbers nil )"bool" reals nil )nil booleans nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil )nil sincosx nil )nil reals nil )"real" trigx nil )"real" reals nil )"trig_range" sincos_def"trig_fnd/" )"cauchy_real" trigx nil )"trig_range" sincos_def"trig_fnd/" )nil div nil )"cauchy_real" sincosx nil )"bool" cauchy nil )nil cauchy nil )"cauchy_real" sincosx nil )nil reals nil )"real" sincos_def "trig_fnd/" )nil sincosx nil ))quality 100%
¤ 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.0.2Bemerkung:
(vorverarbeitet)
¤ *Bot Zugriff
2026-03-28
