Quelle  jatan2.prf   Sprache: unbekannt

(jatan2
 (jatan2_TCC1 0
  (jatan2_TCC1-1 nil 3422010249 ("" (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)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (/= const-decl "boolean" notequal nil))
   nil))
 (jatan2_TCC2 0
  (jatan2_TCC2-1 nil 3422016445 ("" (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)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (/= const-decl "boolean" notequal nil))
   nil))
 (t1 0
  (t1-1 nil 3422010263
   ("" (expand "jatan2") (("" (rewrite "atan2_11") nil nil)) nil)
   ((atan2_11 formula-decl nil atan2_props nil)
    (jatan2 const-decl "real" jatan2 nil))
   shostak))
 (t2 0
  (t2-1 nil 3422011234
   ("" (expand "jatan2")
    (("" (rewrite "atan2_1m1") (("" (assert) nil nil)) nil)) nil)
   ((atan2_1m1 formula-decl nil atan2_props nil)
    (nil application-judgement "nnreal_lt_2pi" atan2 nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (jatan2 const-decl "real" jatan2 nil))
   nil))
 (t3 0
  (t3-1 nil 3422016836
   ("" (expand "jatan2") (("" (rewrite "atan2_m11") nil nil)) nil)
   ((atan2_m11 formula-decl nil atan2_props nil)
    (jatan2 const-decl "real" jatan2 nil))
   shostak))
 (t4 0
  (t4-1 nil 3422016851
   ("" (expand "jatan2")
    (("" (rewrite "atan2_m1m1") (("" (assert) nil nil)) nil)) nil)
   ((atan2_m1m1 formula-decl nil atan2_props nil)
    (nil application-judgement "nnreal_lt_2pi" atan2 nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (jatan2 const-decl "real" jatan2 nil))
   shostak)))