| products/sources/formale sprachen/PVS/trig_fnd/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: atan.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(atan (IMP_nth_derivatives_TCC1 0
(IMP_nth_derivatives_TCC1-1 nil 3514558647 ("" (lemma "deriv_domain[real]") (("1" (propax) nil nil) ("2" (lemma "connected_real") (("2" (propax) nil nil)) nil)) nil) ((connected_real formula-decl nil deriv_domain "analysis/") (bool nonempty-type-eq-decl nil booleans nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (connected? const-decl "bool" deriv_domain_def "analysis/") (deriv_domain formula-decl nil fundamental_theorem "analysis/") (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)) nil)) (IMP_nth_derivatives_TCC2 0 (IMP_nth_derivatives_TCC2-1 nil 3514558647 ("" (expand "not_one_element?") (("" (skosimp*) (("" (inst + "x!1+1") (("" (assert) nil nil)) nil)) nil)) nil) ((+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields 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_plus_real_is_real application-judgement "real" reals nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/")) nil)) (IMP_taylors_TCC1 0 (IMP_taylors_TCC1-1 nil 3514558647 ("" (assuming-tcc) nil nil) ((connected? const-decl "bool" deriv_domain_def "analysis/")) nil)) (atan_deriv_fn_TCC1 0 (atan_deriv_fn_TCC1-1 nil 3255851189 ("" (skosimp*) (("" (lemma "sq_pos" ("a" "x!1")) (("" (grind) nil nil)) nil)) 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) (sq_pos formula-decl nil sq "reals/") (sq const-decl "nonneg_real" sq "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil)) shostak)) (atan_deriv_fn_TCC2 0 (atan_deriv_fn_TCC2-1 nil 3255875082 ("" (skosimp*) (("" (lemma "sq_pos" ("a" "x!1")) (("" (expand "sq") (("" (lemma "posreal_div_posreal_is_posreal" ("px" "1" "py" "1+x!1*x!1")) (("" (assert) nil nil)) nil)) nil)) nil)) 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) (sq_pos formula-decl nil sq "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil 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) (bool nonempty-type-eq-decl nil booleans nil) (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil) (real_plus_real_is_real application-judgement "real" reals nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_times_real_is_real application-judgement "real" reals nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (sq const-decl "nonneg_real" sq "reals/")) shostak)) (one_over_one_plus_t_sq_cont 0 (one_over_one_plus_t_sq_cont-2 nil 3352177935 ("" (expand "atan_deriv_fn") (("" (expand "continuous?") (("" (skolem 1 ("x")) (("" (lemma "identity_continuous[real]" ("x0" "x")) (("" (expand "I") (("" (lemma "prod_continuous[real]" ("f1" "LAMBDA (x: real): x" "f2" "LAMBDA (x: real): x" "x0" "x")) (("" (assert) (("" (lemma "const_continuous[real]" ("u" "1" "x0" "x")) (("" (expand "const_fun") (("" (expand "*") (("" (lemma "sum_continuous[real]" ("f1" "LAMBDA (x: real): 1" "f2" "LAMBDA (x: real): x*x" "x0" "x")) (("" (assert) (("" (expand "+") (("" (lemma "inv_continuous[real]" ("g" "LAMBDA (x: real): 1 + x * x" "x0" "x")) (("1" (assert) (("1" (expand "/") (("1" (propax) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (lemma "sq_pos" ("a" "x!1")) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((real_times_real_is_real application-judgement "real" reals nil) (real_plus_real_is_real application-judgement "real" reals nil) (continuous? const-decl "bool" continuous_functions "analysis/") (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) (identity_continuous formula-decl nil continuous_functions "analysis/") (prod_continuous formula-decl nil continuous_functions "analysis/") (const_continuous formula-decl nil continuous_functions "analysis/") (* const-decl "[T -> real]" real_fun_ops "reals/") (inv_continuous formula-decl nil continuous_functions "analysis/") (/= const-decl "boolean" notequal nil) (nzreal nonempty-type-eq-decl nil reals nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (/ const-decl "[T -> real]" real_fun_ops "reals/") (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (sq const-decl "nonneg_real" sq "reals/") (sq_pos formula-decl nil sq "reals/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (sum_continuous formula-decl nil continuous_functions "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (I const-decl "(bijective?[T, T])" identity nil) (atan_deriv_fn const-decl "posreal" atan nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil)) nil) (one_over_one_plus_t_sq_cont-1 nil 3255875106 ("" (expand "atan_deriv_fn") (("" (expand "continuous?") (("" (skolem 1 ("x")) (("" (lemma "identity_continuous" ("x0" "x")) (("" (expand "I") (("" (lemma "prod_continuous" ("f1" "LAMBDA (x: real): x" "f2" "LAMBDA (x: real): x" "x0" "x")) (("" (assert) (("" (lemma "const_continuous" ("u" "1" "x0" "x")) (("" (expand "const_fun") (("" (expand "*") (("" (lemma "sum_continuous" ("f1" "LAMBDA (x: real): 1" "f2" "LAMBDA (x: real): x*x" "x0" "x")) (("" (assert) (("" (expand "+") (("" (lemma "inv_continuous" ("g" "LAMBDA (x: real): 1 + x * x" "x0" "x")) (("1" (assert) (("1" (expand "/") (("1" (propax) nil nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (skosimp*) (("2" (lemma "sq_pos" ("a" "x!1")) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((identity_continuous formula-decl nil continuous_functions "analysis/") (prod_continuous formula-decl nil continuous_functions "analysis/") (const_continuous formula-decl nil continuous_functions "analysis/") (inv_continuous formula-decl nil continuous_functions "analysis/") (sq const-decl "nonneg_real" sq "reals/") (sq_pos formula-decl nil sq "reals/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (sum_continuous formula-decl nil continuous_functions "analysis/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/")) shostak)) (atan_value_TCC1 0 (atan_value_TCC1-2 nil 3352178025 ("" (skolem 1 ("x")) (("" (lemma "one_over_one_plus_t_sq_cont") (("" (lemma "continuous_Integrable?[real]" ("f" "atan_deriv_fn" "a" "0" "b" "x")) (("1" (expand "continuous?" -2) (("1" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skosimp*) (("2" (inst - "x!1") nil nil)) nil)) nil)) nil)) nil) ("2" (expand "connected?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ((one_over_one_plus_t_sq_cont formula-decl nil atan nil) (continuous? const-decl "bool" continuous_functions "analysis/") (Closed_interval type-eq-decl nil intervals_real "reals/") (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (connected? const-decl "bool" deriv_domain_def "analysis/") (continuous_Integrable? formula-decl nil integral "analysis/") (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) (atan_deriv_fn const-decl "posreal" atan 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)) nil) (atan_value_TCC1-1 nil 3255851329 ("" (skolem 1 ("x")) (("" (lemma "one_over_one_plus_t_sq_cont") (("" (lemma "continuous_Integrable?" ("f" "atan_deriv_fn" "a" "0" "b" "x")) (("" (expand "continuous?" -2) (("" (split -1) (("1" (propax) nil nil) ("2" (hide 2) (("2" (skosimp*) (("2" (inst - "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((continuous_Integrable? formula-decl nil integral "analysis/")) shostak)) (atan_value_0 0 (atan_value_0-2 nil 3352180534 ("" (expand "atan_value") (("" (lemma "Integral_a_to_a[real]" ("a" "0" "f" "atan_deriv_fn")) (("1" (propax) nil nil) ("2" (assert) (("2" (expand "connected?") (("2" (propax) nil nil)) nil)) nil)) nil)) 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) (atan_deriv_fn const-decl "posreal" atan 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) (bool nonempty-type-eq-decl nil booleans nil) (Integral_a_to_a formula-decl nil integral "analysis/") (connected? const-decl "bool" deriv_domain_def "analysis/") (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (atan_value const-decl "real" atan nil)) nil) (atan_value_0-1 nil 3255979393 ("" (expand "atan_value") (("" (lemma "Integral_a_to_a" ("a" "0" "f" "atan_deriv_fn")) (("" (propax) nil nil)) nil)) nil) ((Integral_a_to_a formula-decl nil integral "analysis/")) shostak)) (atan_neg_value 0 (atan_neg_value-3 "fixit" 3394184058 ("" (lemma "derivs_eq[real]" ("F" "LAMBDA (z:real): atan_value(-z)" "G" "LAMBDA (z:real): -atan_value(z)")) (("1" (skolem 1 ("x")) (("1" (lemma "identity_derivable_fun[real]") (("1" (lemma "deriv_id_fun[real]") (("1" (lemma "neg_derivable_fun[real]" ("f" "LAMBDA (x:real): x")) (("1" (lemma "deriv_neg_fun[real]" ("ff" "LAMBDA (x: real): x")) (("1" (expand "I") (("1" (lemma "one_over_one_plus_t_sq_cont") (("1" (lemma "fundamental[real]" ("f" "atan_deriv_fn" "a" "0" "F" "atan_value")) (("1" (split -1) (("1" (flatten -1) (("1" (lemma "composition_derivable_fun[real,real]" ("f" "-(LAMBDA (x: real): x)" "g" "atan_value")) (("1" (lemma "composition_derivable_fun[real,real]" ("g" "-(LAMBDA (x: real): x)" "f" "atan_value")) (("1" (assert) (("1" (assert) (("1" (lemma "deriv_comp_fun[real,real]" ("ff" "-(LAMBDA (x: real): x)" "gg" "atan_value")) (("1" (lemma "deriv_comp_fun[real,real]" ("gg" "-(LAMBDA (x: real): x)" "ff" "atan_value")) (("1" (expand "o") (("1" (expand "-") (("1" (expand "*") (("1" (assert) (("1" (replace -6) (("1" (expand "const_fun") (("1" (replace -10) (("1" (simplify -8) (("1" (replace -8) (("1" (simplify -2) (("1" (simplify -1) (("1" (replace -1) (("1" (replace -2) (("1" (lemma "extensionality_postulate" ("f" "LAMBDA (x: real): atan_deriv_fn(-x) * -1" "g" "LAMBDA (x: real): -1 * atan_deriv_fn(x)")) (("1" (split -13) (("1" (skosimp*) (("1" (lemma "extensionality_postulate" ("f" "(LAMBDA (z: real): atan_value(-z))" "g" "(LAMBDA (z: real): -atan_value(z)) + (LAMBDA (x: real): c!1)")) (("1" (replace -1 -2 rl) (("1" (inst-cp -2 "0") (("1" (expand "+") (("1" (rewrite "atan_value_0") (("1" (inst -2 "x") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "atan_deriv_fn") (("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) ("2" (propax) nil nil) ("3" (expand "atan_value" 1) (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "I") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (assert) (("2" (lemma "not_one_element") (("2" (expand "not_one_element?") (("2" (expand "connected?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((not_one_element formula-decl nil taylors "analysis/") (deriv_id_fun formula-decl nil derivatives "analysis/") (deriv_neg_fun formula-decl nil derivatives "analysis/") (derivable? const-decl "bool" derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (one_over_one_plus_t_sq_cont formula-decl nil atan nil) (composition_derivable_fun formula-decl nil chain_rule "analysis/") (- const-decl "[T -> real]" real_fun_ops "reals/") (deriv_domain? const-decl "bool" deriv_domain_def "analysis/") (deriv_comp_fun formula-decl nil chain_rule "analysis/") (O const-decl "T3" function_props nil) (* const-decl "[T -> real]" real_fun_ops "reals/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (atan_value_0 formula-decl nil atan nil) (minus_even_is_even application-judgement "even_int" integers nil) (real_plus_real_is_real application-judgement "real" reals nil) (nzreal_div_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (extensionality_postulate formula-decl nil functions nil) (nzreal_times_nzreal_is_nzreal application-judgement "nzreal" real_types nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (real_times_real_is_real application-judgement "real" reals nil) (atan_deriv_fn const-decl "posreal" atan 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) (fundamental formula-decl nil fundamental_theorem "analysis/") (I const-decl "(bijective?[T, T])" identity nil) (derivable_id name-judgement "deriv_fun" derivatives "analysis/") (id_fun_continuous name-judgement "continuous_fun" continuous_functions "analysis/") (id_fun_continuous name-judgement "continuous_fun[T2]" lim_of_composition "analysis/") (id_fun_continuous name-judgement "continuous_fun[T]" unif_cont_fun "analysis/") (id_fun_continuous name-judgement "continuous_fun[T]" integral_step "analysis/") (id_fun_continuous name-judgement "continuous_fun[T]" integral_split_scaf "analysis/") (id_fun_continuous name-judgement "continuous_fun[T]" integral "analysis/") (id_fun_continuous name-judgement "continuous_fun[T]" indefinite_integral "analysis/") (neg_derivable_fun formula-decl nil derivatives "analysis/") (identity_derivable_fun formula-decl nil derivatives "analysis/") (bool nonempty-type-eq-decl nil booleans nil) (not_one_element? const-decl "bool" deriv_domain_def "analysis/") (connected? const-decl "bool" deriv_domain_def "analysis/") (minus_real_is_real application-judgement "real" reals nil) (derivs_eq formula-decl nil indefinite_integral "analysis/") (atan_value const-decl "real" atan nil) (numfield nonempty-type-eq-decl nil number_fields nil) (- const-decl "[numfield -> numfield]" 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) (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)) nil) (atan_neg_value-2 nil 3352180601 ("" (lemma "derivs_eq[real]" ("F" "LAMBDA (z:real): atan_value(-z)" "G" "LAMBDA (z:real): -atan_value(z)")) (("1" (skolem 1 ("x")) (("1" (lemma "identity_derivable_fun[real]") (("1" (lemma "deriv_id_fun[real]") (("1" (lemma "neg_derivable_fun[real]" ("f" "LAMBDA (x:real): x")) (("1" (lemma "deriv_neg_fun[real]" ("ff" "LAMBDA (x: real): x")) (("1" (expand "I") (("1" (lemma "one_over_one_plus_t_sq_cont") (("1" (lemma "fundamental[real]" ("f" "atan_deriv_fn" "a" "0" "F" "atan_value")) (("1" (split -1) (("1" (flatten -1) (("1" (lemma "composition_derivable_fun[real,real]" ("f" "-(LAMBDA (x: real): x)" "g" "atan_value")) (("1" (lemma "composition_derivable_fun[real,real]" ("g" "-(LAMBDA (x: real): x)" "f" "atan_value")) (("1" (assert) (("1" (assert) (("1" (lemma "deriv_comp_fun[real,real]" ("ff" "-(LAMBDA (x: real): x)" "gg" "atan_value")) (("1" (lemma "deriv_comp_fun[real,real]" ("gg" "-(LAMBDA (x: real): x)" "ff" "atan_value")) (("1" (expand "o") (("1" (expand "-") (("1" (expand "*") (("1" (assert) (("1" (replace -6) (("1" (expand "const_fun") (("1" (replace -10) (("1" (simplify -8) (("1" (replace -8) (("1" (simplify -2) (("1" (simplify -1) (("1" (replace -1) (("1" (replace -2) (("1" (assert) (("1" (lemma "extensionality_postulate" ("f" "LAMBDA (x: real): atan_deriv_fn(-x) * -1" "g" "LAMBDA (x: real): -1 * atan_deriv_fn(x)")) (("1" (replace -1 -13 rl) (("1" (split -13) (("1" (skosimp*) (("1" (lemma "extensionality_postulate" ("f" "(LAMBDA (z: real): atan_value(-z))" "g" "(LAMBDA (z: real): -atan_value(z)) + (LAMBDA (x: real): c!1)")) (("1" (replace -1 -2 rl) (("1" (inst-cp -2 "0") (("1" (expand "+") (("1" (rewrite "atan_value_0") (("1" (inst -2 "x") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "atan_deriv_fn") (("2" (lemma "sq_neg" ("a" "x!1")) (("2" (expand "sq") (("2" (replace -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) ("2" (propax) nil nil) ("3" (expand "atan_value" 1) (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (expand "I") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil)) nil)) nil) ((deriv_id_fun formula-decl nil derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (composition_derivable_fun formula-decl nil chain_rule "analysis/") (constant_seq2 application-judgement "(convergent_nz?)" convergence_ops "analysis/") (const_fun_continuous application-judgement "continuous_fun[T]" integral "analysis/") (deriv_comp_fun formula-decl nil chain_rule "analysis/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (sq const-decl "nonneg_real" sq "reals/") (sq_neg formula-decl nil sq "reals/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (fundamental formula-decl nil fundamental_theorem "analysis/") (derivable_id name-judgement "deriv_fun" derivatives "analysis/") (id_fun_continuous name-judgement "continuous_fun" continuous_functions "analysis/") (id_fun_continuous name-judgement "continuous_fun[T2]" lim_of_composition "analysis/") (id_fun_continuous name-judgement "continuous_fun[T]" unif_cont_fun "analysis/") (id_fun_continuous name-judgement "continuous_fun[T]" integral_step "analysis/") (id_fun_continuous name-judgement "continuous_fun[T]" integral_split_scaf "analysis/") (id_fun_continuous name-judgement "continuous_fun[T]" integral "analysis/") (neg_derivable_fun formula-decl nil derivatives "analysis/") (identity_derivable_fun formula-decl nil derivatives "analysis/")) nil) (atan_neg_value-1 nil 3255979648 ("" (lemma "derivs_eq" ("F" "LAMBDA (z:real): atan_value(-z)" "G" "LAMBDA (z:real): -atan_value(z)")) (("" (skolem 1 ("x")) (("" (lemma "identity_derivable_fun[real]") (("" (lemma "deriv_id_fun[real]") (("" (lemma "neg_derivable_fun[real]" ("f" "LAMBDA (x:real): x")) (("" (lemma "deriv_neg_fun" ("ff" "LAMBDA (x: real): x")) (("1" (expand "I") (("1" (lemma "one_over_one_plus_t_sq_cont") (("1" (lemma "fundamental[real]" ("f" "atan_deriv_fn" "a" "0" "F" "atan_value")) (("1" (split -1) (("1" (flatten -1) (("1" (lemma "composition_derivable_fun" ("f" "-(LAMBDA (x: real): x)" "g" "atan_value")) (("1" (lemma "composition_derivable_fun" ("g" "-(LAMBDA (x: real): x)" "f" "atan_value")) (("1" (assert) (("1" (assert) (("1" (lemma "deriv_comp_fun" ("ff" "-(LAMBDA (x: real): x)" "gg" "atan_value")) (("1" (lemma "deriv_comp_fun" ("gg" "-(LAMBDA (x: real): x)" "ff" "atan_value")) (("1" (expand "o") (("1" (expand "-") (("1" (expand "*") (("1" (assert) (("1" (replace -6) (("1" (expand "const_fun") (("1" (replace -10) (("1" (simplify -8) (("1" (replace -8) (("1" (simplify -2) (("1" (simplify -1) (("1" (replace -1) (("1" (replace -2) (("1" (assert) (("1" (lemma "extensionality_postulate" ("f" "LAMBDA (x: real): atan_deriv_fn(-x) * -1" "g" "LAMBDA (x: real): -1 * atan_deriv_fn(x)")) (("1" (replace -1 -13 rl) (("1" (split -13) (("1" (skosimp*) (("1" (lemma "extensionality_postulate" ("f" "(LAMBDA (z: real): atan_value(-z))" "g" "(LAMBDA (z: real): -atan_value(z)) + (LAMBDA (x: real): c!1)")) (("1" (replace -1 -2 rl) (("1" (inst-cp -2 "0") (("1" (expand "+") (("1" (rewrite "atan_value_0") (("1" (inst -2 "x") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "atan_deriv_fn") (("2" (lemma "sq_neg" ("a" "x!1")) (("2" (expand "sq") (("2" (replace -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) ("2" (propax) nil nil) ("3" (expand "atan_value" 1) (("3" (propax) nil nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "x!1+1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "I") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((deriv_id_fun formula-decl nil derivatives "analysis/") (deriv_fun type-eq-decl nil derivatives "analysis/") (composition_derivable_fun formula-decl nil chain_rule "analysis/") (deriv_comp_fun formula-decl nil chain_rule "analysis/") (+ const-decl "[T -> real]" real_fun_ops "reals/") (sq const-decl "nonneg_real" sq "reals/") (sq_neg formula-decl nil sq "reals/") (const_fun const-decl "[T -> real]" real_fun_ops "reals/") (fundamental formula-decl nil fundamental_theorem "analysis/") (neg_derivable_fun formula-decl nil derivatives "analysis/") (identity_derivable_fun formula-decl nil derivatives "analysis/")) shostak)) (atan_inv_value 0 (atan_inv_value-2 nil 3352181608 ("" (lemma "derivs_eq[posreal]" ("F" "LAMBDA (x:posreal): atan_value(x)" "G" "LAMBDA (x:posreal): atan_value(-1/x)")) (("1" (skolem 1 ("x")) (("1" (lemma "fundamental[real]" ("f" "atan_deriv_fn" "F" "atan_value" "a" "0")) (("1" (split -1) (("1" (flatten -1) (("1" (lemma "restrict2_derivable[posreal,real]" ("f" "atan_value")) (("1" (lemma "restrict2_deriv[posreal,real]" ("f" "atan_value")) (("1" (expand "restrict2") (("1" (replace -2) (("1" (lemma "composition_derivable_fun[posreal,real]" ("f" "LAMBDA (x: posreal): -(1 / x)" "g" "atan_value")) (("1" (lemma "identity_derivable_fun[posreal]") (("1" (lemma "deriv_id_fun[posreal]") (("1" (expand "I") (("1" (expand "const_fun") (("1" (lemma "inv_derivable_fun[posreal]" ("g" "(LAMBDA (x: posreal): x)")) (("1" (assert) (("1" (expand "/") (("1" (lemma "deriv_inv_fun[posreal]" ("gg" "(LAMBDA (x: posreal): x)")) (("1" (replace -3) (("1" (expand "-") (("1" (expand "/") --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.93 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.Bot Zugriff |
