Gedichte Musik Bilder Quellcodebibliothek Diashow Normaldarstellung
Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/GAP/grp/   (Algebra von RWTH Aachen Version 4.15.1©)  Datei vom 18.9.2025 mit Größe 354 kB image not shown  

Quelle  atan_values.prf   Sprache: unbekannt

 
(atan_values
 (atan0 0
  (atan0-1 nil 3422179176
   ("" (lemma "atan_tan")
    (("" (inst?)
      (("1" (rewrite "tan_0") nil nil) ("2" (assert) nil nil)) nil))
    nil)
   ((posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
     nil)
    (pi_ub const-decl "posreal" trig_basic nil)
    (pi_lb const-decl "posreal" trig_basic 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 -> numfield]" number_fields 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)
    (< const-decl "bool" reals 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)
    (number nonempty-type-decl nil numbers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
    (tan_0 formula-decl nil trig_basic nil)
    (atan_0 formula-decl nil atan nil)
    (atan_tan formula-decl nil trig_inverses nil))
   shostak))
 (atan1 0
  (atan1-1 nil 3422179016
   ("" (lemma "atan_tan")
    (("" (inst - "pi/4")
      (("1" (expand "tan")
        (("1" (rewrite "sin_pi4")
          (("1" (rewrite "cos_pi4") (("1" (assert) nil nil)) nil))
          nil))
        nil)
       ("2" (assert) nil nil))
      nil))
    nil)
   ((minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
     nil)
    (pi_ub const-decl "posreal" trig_basic nil)
    (pi_lb const-decl "posreal" trig_basic 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 -> numfield]" number_fields 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)
    (< const-decl "bool" reals 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)
    (number nonempty-type-decl nil numbers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
    (sin_pi4 formula-decl nil trig_values nil)
    (sin_range application-judgement "trig_range" trig_basic nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (cos_pi4 formula-decl nil trig_values nil)
    (tan const-decl "real" trig_basic nil)
    (atan_tan formula-decl nil trig_inverses nil))
   shostak))
 (atan_1sqrt3 0
  (atan_1sqrt3-1 nil 3422178472
   ("" (lemma "atan_tan")
    (("" (inst - "pi/6")
      (("1" (expand "tan")
        (("1" (rewrite "sin_pi6")
          (("1" (rewrite "cos_pi6") (("1" (assert) nil nil)) nil))
          nil))
        nil)
       ("2" (assert) nil nil))
      nil))
    nil)
   ((minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
     nil)
    (pi_ub const-decl "posreal" trig_basic nil)
    (pi_lb const-decl "posreal" trig_basic 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 -> numfield]" number_fields 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)
    (< const-decl "bool" reals 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)
    (number nonempty-type-decl nil numbers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
    (sin_pi6 formula-decl nil trig_values nil)
    (sin_range application-judgement "trig_range" trig_basic nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (cos_pi6 formula-decl nil trig_values nil)
    (tan const-decl "real" trig_basic nil)
    (atan_tan formula-decl nil trig_inverses nil))
   nil))
 (atan_sqrt3 0
  (atan_sqrt3-1 nil 3422178501
   ("" (lemma "atan_tan")
    (("" (inst - "pi/3")
      (("1" (expand "tan")
        (("1" (rewrite "sin_pi3")
          (("1" (rewrite "cos_pi3") (("1" (assert) nil nil)) nil))
          nil))
        nil)
       ("2" (assert) nil nil))
      nil))
    nil)
   ((minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
     nil)
    (pi_ub const-decl "posreal" trig_basic nil)
    (pi_lb const-decl "posreal" trig_basic 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 -> numfield]" number_fields 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)
    (< const-decl "bool" reals 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)
    (number nonempty-type-decl nil numbers nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
    (sin_pi3 formula-decl nil trig_values nil)
    (sin_range application-judgement "trig_range" trig_basic nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (cos_pi3 formula-decl nil trig_values nil)
    (tan const-decl "real" trig_basic nil)
    (atan_tan formula-decl nil trig_inverses nil))
   nil))
 (atan_m1sqrt3 0
  (atan_m1sqrt3-1 nil 3422178651
   ("" (lemma "atan_neg")
    (("" (inst - "1/sqrt(3)")
      (("" (rewrite "atan_1sqrt3") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (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)
    (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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (nnreal type-eq-decl nil real_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (atan_1sqrt3 formula-decl nil atan_values nil)
    (atan_neg formula-decl nil atan nil))
   shostak))
 (atan_msqrt3 0
  (atan_msqrt3-1 nil 3422178691
   ("" (lemma "atan_neg")
    (("" (inst?)
      (("" (rewrite "atan_sqrt3") (("" (assert) nil nil)) nil)) nil))
    nil)
   ((minus_nzreal_is_nzreal application-judgement "nzreal" real_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)
    (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)
    (nnreal type-eq-decl nil real_types nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (atan_sqrt3 formula-decl nil atan_values nil)
    (atan_neg formula-decl nil atan nil))
   shostak))
 (atan_gt_0 0
  (atan_gt_0-1 nil 3427470520
   ("" (skeep)
    (("" (lemma "tan_atan")
      (("" (inst?)
        (("" (lemma "tan_gt_0")
          (("" (inst?)
            (("" (lemma "tan_lt_0")
              (("" (inst?)
                (("" (lemma "tan_0") (("" (ground) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((tan_atan formula-decl nil trig_inverses nil)
    (tan_gt_0 formula-decl nil trig_ineq nil)
    (tan_lt_0 formula-decl nil trig_ineq nil)
    (tan_0 formula-decl nil trig_basic nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (atan const-decl "real_abs_lt_pi2" atan nil)
    (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
    (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
     nil)
    (pi_ub const-decl "posreal" trig_basic nil)
    (pi_lb const-decl "posreal" trig_basic 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 -> numfield]" number_fields 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)
    (< 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   shostak)))

100%


[ 0.18Quellennavigators  Projekt   ]