Quelle  atan2.prf   Sprache: Lisp

(atan2
 (atan2_TCC1 0
  (atan2_TCC1-1 nil 3269553691 ("" (grind) 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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (/= const-decl "boolean" notequal nil))
   shostak))
 (atan2_TCC2 0
  (atan2_TCC2-1 nil 3269553735 ("" (grind) 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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (/= const-decl "boolean" notequal nil))
   shostak))
 (atan2_TCC3 0
  (atan2_TCC3-1 nil 3269553749 ("" (grind) 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))
   shostak))
 (atan2_0_2pi_TCC1 0
  (atan2_0_2pi_TCC1-1 nil 3269553757 ("" (grind) 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 "boolean" notequal nil))
   shostak))
 (atan2_0_2pi_TCC2 0
  (atan2_0_2pi_TCC2-1 nil 3269553764 ("" (grind) 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)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (/= const-decl "boolean" notequal nil)
    (atan2 const-decl "real" atan2 nil))
   shostak))
 (atan2_0_2pi_TCC3 0
  (atan2_0_2pi_TCC3-1 nil 3269553778
   ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   shostak))
 (atan2_0_2pi_TCC4 0
  (atan2_0_2pi_TCC4-1 nil 3269554070
   ("" (skosimp*) (("" (assert) nil nil)) nil)
   ((real_ge_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))
   shostak))
 (atan2_0_2pi 0
  (atan2_0_2pi-2 nil 3322496352
   ("" (skosimp*)
    (("" (lemma "trichotomy" ("x" "x!1"))
      (("" (expand "atan2")
        (("" (split -1)
          (("1" (assert)
            (("1" (lemma "trichotomy" ("x" "y!1"))
              (("1" (split -1)
                (("1" (assert)
                  (("1" (typepred "atan(y!1 / x!1)")
                    (("1" (rewrite "pi_value")
                      (("1" (lemma "atan_strict_increasing")
                        (("1" (expand "strict_increasing?")
                          (("1" (inst - "0" "y!1/x!1")
                            (("1"
                              (lemma "posreal_div_posreal_is_posreal"
                               ("px" "y!1" "py" "x!1"))
                              (("1"
                                (assert)
                                (("1"
                                  (rewrite "atan_0")
                                  (("1"
                                    (expand "abs")
                                    (("1"
                                      (assert)
                                      (("1"
                                        (expand "atan")
                                        (("1" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (replace -1)
                  (("2" (assert)
                    (("2" (rewrite "atan_0") (("2" (assert) nil nil))
                      nil))
                    nil))
                  nil)
                 ("3" (assert)
                  (("3" (lemma "atan_strict_increasing")
                    (("3" (expand "strict_increasing?")
                      (("3" (typepred "atan(y!1 / x!1)")
                        (("3" (inst - "y!1/x!1" "0")
                          (("3"
                            (lemma "both_sides_div_pos_gt1"
                             ("x" "0" "y" "y!1" "pz" "x!1"))
                            (("3" (assert)
                              (("3"
                                (rewrite "atan_0")
                                (("3"
                                  (expand "abs")
                                  (("3"
                                    (assert)
                                    (("3"
                                      (rewrite "pi_value")
                                      (("3"
                                        (expand "atan")
                                        (("3" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (replace -1)
            (("2" (assert)
              (("2" (lemma "trichotomy" ("x" "y!1"))
                (("2" (split -1)
                  (("1" (assert) nil nil) ("2" (assert) nil nil)
                   ("3" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil)
           ("3" (assert)
            (("3" (hide -2)
              (("3" (lemma "trichotomy" ("x" "y!1"))
                (("3" (split -1)
                  (("1" (assert)
                    (("1" (lemma "both_sides_div_neg_gt1")
                      (("1" (inst - "x!1" "0" "y!1")
                        (("1" (assert)
                          (("1" (lemma "atan_strict_increasing")
                            (("1" (expand "strict_increasing?")
                              (("1"
                                (inst - "y!1/x!1" "0")
                                (("1"
                                  (rewrite "atan_0")
                                  (("1"
                                    (typepred "atan(y!1/x!1)")
                                    (("1"
                                      (expand "abs")
                                      (("1"
                                        (assert)
                                        (("1"
                                          (assert)
                                          (("1"
                                            (rewrite "pi_value")
                                            (("1"
                                              (expand "atan")
                                              (("1" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (assert)
                    (("2" (replace -1)
                      (("2" (rewrite "atan_0") (("2" (assert) nil nil))
                        nil))
                      nil))
                    nil)
                   ("3"
                    (lemma "negreal_div_negreal_is_posreal"
                     ("nx" "y!1" "ny" "x!1"))
                    (("1" (lemma "atan_strict_increasing")
                      (("1" (expand "strict_increasing?")
                        (("1" (inst - "0" "y!1/x!1")
                          (("1" (rewrite "atan_0")
                            (("1" (assert)
                              (("1"
                                (typepred "atan(y!1/x!1)")
                                (("1"
                                  (expand "abs")
                                  (("1"
                                    (rewrite "pi_value")
                                    (("1"
                                      (expand "atan")
                                      (("1" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              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)
    (trichotomy formula-decl nil real_axioms nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (both_sides_div_pos_gt1 formula-decl nil real_props nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (pi_value formula-decl nil atan nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (strict_increasing? const-decl "bool" real_fun_preds "reals/")
    (posreal_div_posreal_is_posreal judgement-tcc nil real_types nil)
    (atan_0 formula-decl nil atan nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (atan_strict_increasing formula-decl nil atan nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (< const-decl "bool" 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)
    (- const-decl "[numfield -> numfield]" number_fields 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)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (pi_lb const-decl "posreal" trig_basic nil)
    (pi_ub const-decl "posreal" trig_basic nil)
    (pi const-decl "{r: posreal | r > pi_lb AND r < pi_ub}" trig_basic
     nil)
    (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
    (atan const-decl "real_abs_lt_pi2" atan nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (both_sides_div_neg_gt1 formula-decl nil real_props nil)
    (<= const-decl "bool" reals nil)
    (nonpos_real nonempty-type-eq-decl nil real_types nil)
    (negreal nonempty-type-eq-decl nil real_types nil)
    (nnreal_plus_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (negreal_div_negreal_is_posreal judgement-tcc nil real_types nil)
    (atan2 const-decl "real" atan2 nil))
   nil)
  (atan2_0_2pi-1 nil 3269554130
   ("" (skosimp*)
    (("" (lemma "trichotomy" ("x" "x!1"))
      (("" (expand "atan2")
        (("" (split -1)
          (("1" (assert)
            (("1" (lemma "trichotomy" ("x" "y!1"))
              (("1" (split -1)
                (("1" (assert)
                  (("1" (typepred "atan(y!1 / x!1)")
                    (("1" (expand "pi")
                      (("1" (expand "pi")
                        (("1" (lemma "atan_strict_increasing")
                          (("1" (expand "strict_increasing?")
                            (("1" (inst - "0" "y!1/x!1")
                              (("1"
                                (lemma
                                 "posreal_div_posreal_is_posreal"
                                 ("px" "y!1" "py" "x!1"))
                                (("1"
                                  (assert)
                                  (("1"
                                    (rewrite "atan_0")
                                    (("1"
                                      (expand "abs")
                                      (("1"
                                        (assert)
                                        (("1"
                                          (expand "atan")
                                          (("1" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (replace -1)
                  (("2" (assert)
                    (("2" (rewrite "atan_0") (("2" (assert) nil nil))
                      nil))
                    nil))
                  nil)
                 ("3" (assert)
                  (("3" (lemma "atan_strict_increasing")
                    (("3" (expand "strict_increasing?")
                      (("3" (typepred "atan(y!1 / x!1)")
                        (("3" (inst - "y!1/x!1" "0")
                          (("3"
                            (lemma "both_sides_div_pos_gt1"
                             ("x" "0" "y" "y!1" "pz" "x!1"))
                            (("3" (assert)
                              (("3"
                                (rewrite "atan_0")
                                (("3"
                                  (expand "abs")
                                  (("3"
                                    (assert)
                                    (("3"
                                      (expand "pi")
                                      (("3"
                                        (expand "pi")
                                        (("3"
                                          (expand "atan")
                                          (("3" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (replace -1)
            (("2" (assert)
              (("2" (lemma "trichotomy" ("x" "y!1"))
                (("2" (split -1)
                  (("1" (assert) nil nil) ("2" (assert) nil nil)
                   ("3" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil)
           ("3" (assert)
            (("3" (hide -2)
              (("3" (lemma "trichotomy" ("x" "y!1"))
                (("3" (split -1)
                  (("1" (assert)
                    (("1" (lemma "both_sides_div_neg_gt1")
                      (("1" (inst - "x!1" "0" "y!1")
                        (("1" (assert)
                          (("1" (lemma "atan_strict_increasing")
                            (("1" (expand "strict_increasing?")
                              (("1"
                                (inst - "y!1/x!1" "0")
                                (("1"
                                  (rewrite "atan_0")
                                  (("1"
                                    (typepred "atan(y!1/x!1)")
                                    (("1"
                                      (expand "abs")
                                      (("1"
                                        (assert)
                                        (("1"
                                          (assert)
                                          (("1"
                                            (expand "pi")
                                            (("1"
                                              (expand "pi")
                                              (("1"
                                                (expand "atan")
                                                (("1"
                                                  (assert)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (assert)
                    (("2" (replace -1)
                      (("2" (rewrite "atan_0") (("2" (assert) nil nil))
                        nil))
                      nil))
                    nil)
                   ("3"
                    (lemma "negreal_div_negreal_is_posreal"
                     ("nx" "y!1" "ny" "x!1"))
                    (("1" (lemma "atan_strict_increasing")
                      (("1" (expand "strict_increasing?")
                        (("1" (inst - "0" "y!1/x!1")
                          (("1" (rewrite "atan_0")
                            (("1" (assert)
                              (("1"
                                (typepred "atan(y!1/x!1)")
                                (("1"
                                  (expand "abs")
                                  (("1"
                                    (expand "pi")
                                    (("1"
                                      (expand "pi")
                                      (("1"
                                        (expand "atan")
                                        (("1" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((strict_increasing? const-decl "bool" real_fun_preds "reals/")
    (atan_0 formula-decl nil atan nil)
    (atan_strict_increasing formula-decl nil atan nil)
    (atan const-decl "real_abs_lt_pi2" atan nil))
   shostak))
 (atan2_ge_0_lt_2pi_TCC1 0
  (atan2_ge_0_lt_2pi_TCC1-1 nil 3269553812 ("" (grind) 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 "boolean" notequal nil))
   shostak))
 (atan2_ge_0_lt_2pi 0
  (atan2_ge_0_lt_2pi-1 nil 3269552776
   ("" (skosimp*)
    (("" (lemma "atan2_0_2pi" ("x" "x!1" "y" "y!1"))
      (("" (replace -2 -1)
        (("" (flatten -1)
          (("" (lemma "trichotomy" ("x" "x!1"))
            (("" (split -1)
              (("1" (assert)
                (("1" (hide -3 -4 -6)
                  (("1" (case "y!1>=0")
                    (("1" (assert)
                      (("1" (flatten -3) (("1" (assert) nil nil)) nil))
                      nil)
                     ("2" (assert)
                      (("2" (flatten -3) (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (assert)
                (("2" (lemma "trichotomy" ("x" "y!1"))
                  (("2" (split -1)
                    (("1" (assert)
                      (("1" (flatten (-3 -4)) (("1" (assert) nil nil))
                        nil))
                      nil)
                     ("2" (assert) nil nil)
                     ("3" (assert)
                      (("3" (flatten (-5 -6)) (("3" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("3" (assert)
                (("3" (hide -2 -5 -6)
                  (("3" (case "y!1>=0")
                    (("1" (assert)
                      (("1" (flatten -3) (("1" (assert) nil nil)) nil))
                      nil)
                     ("2" (assert)
                      (("2" (flatten -3) (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              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)
    (atan2_0_2pi formula-decl nil atan2 nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_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)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (trichotomy formula-decl nil real_axioms nil))
   nil))
 (nnreal_lt_2pi_TCC1 0
  (nnreal_lt_2pi_TCC1-1 nil 3414421709
   ("" (inst + "0") (("" (assert) nil nil)) 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)
    (AND const-decl "[bool, bool -> bool]" booleans 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 "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types 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_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil))
   nil))
 (atan2_TCC4 0
  (atan2_TCC4-1 nil 3414421709
   ("" (skosimp*)
    (("" (typepred "y!1")
      (("" (rewrite "atan2_ge_0_lt_2pi") (("" (grind) nil nil)) nil))
      nil))
    nil)
   ((/= const-decl "boolean" notequal 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)
    (number nonempty-type-decl nil numbers nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (atan2_ge_0_lt_2pi formula-decl nil atan2 nil))
   nil))
 (atan2_cancel_pos_TCC1 0
  (atan2_cancel_pos_TCC1-1 nil 3269628375
   ("" (skosimp*)
    (("" (assert)
      (("" (split -1)
        (("1"
          (lemma "both_sides_times1" ("x" "x!1" "y" "0" "n0z" "pz!1"))
          (("1" (assert) nil nil)) nil)
         ("2"
          (lemma "both_sides_times1" ("x" "y!1" "y" "0" "n0z" "pz!1"))
          (("2" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((real_times_real_is_real application-judgement "real" reals 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)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal 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)
    (both_sides_times1 formula-decl nil real_props nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil))
   shostak))
 (atan2_cancel_pos 0
  (atan2_cancel_pos-1 nil 3269616367
   ("" (skosimp*)
    (("" (expand "atan2")
      ((""
        (lemma "both_sides_times_pos_gt1"
         ("x" "x!1" "y" "0" "pz" "pz!1"))
        (("" (replace -1)
          (("" (case "x!1>0")
            (("1" (assert)
              (("1"
                (lemma "both_sides_times_pos_ge1"
                 ("x" "y!1" "y" "0" "pz" "pz!1"))
                (("1" (replace -1)
                  (("1" (case "y!1>=0")
                    (("1" (assert) nil nil) ("2" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (assert)
              (("2" (case "x!1=0")
                (("1" (assert)
                  (("1"
                    (lemma "both_sides_times_pos_gt1"
                     ("x" "y!1" "y" "0" "pz" "pz!1"))
                    (("1" (replace -1) (("1" (propax) nil nil)) nil))
                    nil))
                  nil)
                 ("2" (assert) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (atan2 const-decl "real" atan2 nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (both_sides_times_pos_ge1 formula-decl nil real_props nil)
    (both_sides_times_pos_gt1 formula-decl nil real_props 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)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil))
   shostak))
 (atan2_cancel_neg_TCC1 0
  (atan2_cancel_neg_TCC1-1 nil 3269628375
   ("" (skosimp*)
    (("" (lemma "both_sides_times1" ("x" "y!1" "y" "0" "n0z" "nz!1"))
      (("" (lemma "both_sides_times1" ("x" "x!1" "y" "0" "n0z" "nz!1"))
        (("" (assert) nil nil)) nil))
      nil))
    nil)
   ((negreal nonempty-type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (nonpos_real nonempty-type-eq-decl nil real_types nil)
    (<= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (/= const-decl "boolean" notequal 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)
    (both_sides_times1 formula-decl nil real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
 (atan2_cancel_neg 0
  (atan2_cancel_neg-1 nil 3269628659
   ("" (skosimp*)
    (("" (expand "atan2")
      (("" (lemma "both_sides_times1" ("x" "x!1" "y" "0" "n0z" "nz!1"))
        (("" (replace -1)
          (("" (case "y!1=0")
            (("1" (replace -1)
              (("1" (rewrite "atan_0")
                (("1" (simplify 1)
                  (("1" (case "x!1>0")
                    (("1" (assert)
                      (("1"
                        (lemma "both_sides_times_neg_lt1"
                         ("x" "x!1" "y" "0" "nz" "nz!1"))
                        (("1" (assert) nil nil)) nil))
                      nil)
                     ("2" (assert)
                      (("2"
                        (lemma "both_sides_times_neg_lt1"
                         ("x" "x!1" "y" "0" "nz" "nz!1"))
                        (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (assert)
              (("2" (case "y!1>0")
                (("1" (hide -2)
                  (("1" (assert)
                    (("1"
                      (lemma "both_sides_times_neg_gt1"
                       ("x" "0" "y" "y!1" "nz" "nz!1"))
                      (("1" (assert)
                        (("1" (case "x!1>0")
                          (("1" (assert)
                            (("1"
                              (lemma "both_sides_times_neg_gt1"
                               ("x" "0" "y" "x!1" "nz" "nz!1"))
                              (("1" (assert) nil nil)) nil))
                            nil)
                           ("2"
                            (lemma "both_sides_times_neg_gt1"
                             ("x" "0" "y" "x!1" "nz" "nz!1"))
                            (("2" (assert)
                              (("2"
                                (case "x!1=0")
                                (("1" (assert) nil nil)
                                 ("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (assert)
                  (("2" (case "x!1=0")
                    (("1" (assert)
                      (("1"
                        (lemma "both_sides_times_neg_gt1"
                         ("x" "0" "y" "y!1" "nz" "nz!1"))
                        (("1" (assert) nil nil)) nil))
                      nil)
                     ("2" (assert)
                      (("2" (case "x!1>0")
                        (("1" (assert)
                          (("1"
                            (lemma "both_sides_times_neg_gt1"
                             ("x" "0" "y" "x!1" "nz" "nz!1"))
                            (("1" (assert) nil nil)) nil))
                          nil)
                         ("2" (assert)
                          (("2"
                            (lemma "both_sides_times_neg_gt1"
                             ("y" "0" "x" "x!1" "nz" "nz!1"))
                            (("2" (assert)
                              (("2"
                                (lemma
                                 "both_sides_times_neg_gt1"
                                 ("y" "0" "x" "y!1" "nz" "nz!1"))
                                (("2" (assert) 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)
    (atan2 const-decl "real" atan2 nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (both_sides_times_neg_gt1 formula-decl nil real_props nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (both_sides_times_neg_lt1 formula-decl nil real_props nil)
    (> const-decl "bool" reals nil) (atan_0 formula-decl nil atan nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (both_sides_times1 formula-decl nil real_props 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)
    (/= const-decl "boolean" notequal nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (<= const-decl "bool" reals nil)
    (nonpos_real nonempty-type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil)
    (negreal nonempty-type-eq-decl nil real_types nil))
   shostak))
 (atan2_swap_pos_TCC1 0
  (atan2_swap_pos_TCC1-1 nil 3514306188 ("" (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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (/= const-decl "boolean" notequal nil))
   nil))
 (atan2_swap_pos_TCC2 0
  (atan2_swap_pos_TCC2-1 nil 3514306188 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (atan2_swap_pos_TCC3 0
  (atan2_swap_pos_TCC3-1 nil 3514306188 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (atan2_swap_pos_TCC4 0
  (atan2_swap_pos_TCC4-1 nil 3514306188 ("" (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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (/= const-decl "boolean" notequal nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
 (atan2_swap_pos 0
  (atan2_swap_pos-1 nil 3514306188
   ("" (skeep)
    (("" (case "x > 0 AND y > 0")
      (("1" (flatten)
        (("1" (hide -3)
          (("1" (expand "atan2")
            (("1" (assert)
              (("1" (lemma "atan_sub_swap")
                (("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (case "x < 0 AND y < 0")
        (("1" (flatten)
          (("1" (hide -3 1)
            (("1" (expand "atan2")
              (("1" (assert)
                (("1" (lemma "atan_sub_swap")
                  (("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (hide 3) (("2" (grind-reals) nil nil)) nil))
        nil))
      nil))
    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)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (atan_sub_swap formula-decl nil atan nil)
    (atan2 const-decl "real" atan2 nil)
    (pos_times_gt formula-decl nil real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (< const-decl "bool" reals nil))
   nil))
 (atan2_swap_neg_TCC1 0
  (atan2_swap_neg_TCC1-1 nil 3514306386 ("" (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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (/= const-decl "boolean" notequal nil))
   nil))
 (atan2_swap_neg_TCC2 0
  (atan2_swap_neg_TCC2-1 nil 3514306386 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (atan2_swap_neg_TCC3 0
  (atan2_swap_neg_TCC3-1 nil 3514306386 ("" (subtype-tcc) nil nil)
   ((/= const-decl "boolean" notequal nil)) nil))
 (atan2_swap_neg_TCC4 0
  (atan2_swap_neg_TCC4-1 nil 3514306386 ("" (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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (/= const-decl "boolean" notequal nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
 (atan2_swap_neg 0
  (atan2_swap_neg-1 nil 3514306386
   ("" (skeep)
    (("" (case "x > 0 AND y < 0")
      (("1" (hide -2)
        (("1" (flatten)
          (("1" (expand "atan2")
            (("1" (assert)
              (("1" (expand "sign")
                (("1" (lemma "atan_sub_swap")
                  (("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (case "x < 0 AND y > 0")
        (("1" (hide -2 1)
          (("1" (flatten)
            (("1" (expand "sign")
              (("1" (assert)
                (("1" (expand "atan2")
                  (("1" (lemma "atan_sub_swap")
                    (("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (hide 3) (("2" (grind-reals) nil nil)) nil))
        nil))
      nil))
    nil)
   ((< const-decl "bool" reals 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)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (nzreal_times_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals 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_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)
    (atan_sub_swap formula-decl nil atan nil)
    (sign const-decl "Sign" sign "reals/")
    (atan2 const-decl "real" atan2 nil)
    (neg_times_lt formula-decl nil real_props nil)
    (nil application-judgement "nnreal_lt_2pi" atan2 nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil))
   nil))
 (atan2_swap_zero_TCC1 0
  (atan2_swap_zero_TCC1-1 nil 3514306403 ("" (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 "boolean" notequal nil))
   nil))
 (atan2_swap_zero_TCC2 0
  (atan2_swap_zero_TCC2-1 nil 3514306403 ("" (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 "boolean" notequal nil)
    (nil application-judgement "nnreal_lt_2pi" atan2 nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil))
   nil))
 (atan2_swap_zero 0
  (atan2_swap_zero-1 nil 3514306403
   ("" (skeep)
    (("" (lemma "atan_0")
      (("" (split)
        (("1" (flatten)
          (("1" (replaces -1)
            (("1" (case "y > 0")
              (("1" (expand "atan2") (("1" (assert) nil nil)) nil)
               ("2" (expand "atan2") (("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil)
         ("2" (flatten)
          (("2" (replaces -1)
            (("2" (case "x > 0")
              (("1" (expand "atan2") (("1" (assert) nil nil)) nil)
               ("2" (expand "atan2") (("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((atan_0 formula-decl nil atan nil)
    (real_minus_real_is_real application-judgement "real" reals 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_div_nzreal_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (atan2 const-decl "real" atan2 nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (nil application-judgement "nnreal_lt_2pi" atan2 nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil))
   nil))
 (atan2_cos_sin_TCC1 0
  (atan2_cos_sin_TCC1-1 nil 3269553823
   ("" (skosimp*)
    (("" (typepred "a!1")
      (("" (lemma "sin_eq_0_2pi" ("a" "a!1"))
        (("" (lemma "cos_eq_0_2pi" ("a" "a!1"))
          (("" (assert)
            (("" (split -1)
              (("1" (split -2)
                (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)
               ("2" (split -2)
                (("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (AND const-decl "[bool, bool -> bool]" booleans 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 "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (< const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types 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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (cos_eq_0_2pi formula-decl nil trig_basic nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_ge_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)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (cos_range application-judgement "trig_range" trig_basic nil)
    (sin_range application-judgement "trig_range" trig_basic nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sin_eq_0_2pi formula-decl nil trig_basic nil))
   shostak))
 (atan2_cos_sin 0
  (atan2_cos_sin-2 nil 3279154016
   ("" (case "FORALL (x:posreal): x < pi => sin(x) > 0")
    (("1"
      (case "FORALL (x: nnreal): x < pi => atan2(cos(x), sin(x)) = x")
      (("1" (skolem 1 ("a"))
        (("1" (case "a < pi")
          (("1" (inst -2 "a") (("1" (assert) nil nil)) nil)
           ("2" (inst -1 "a-pi")
            (("1" (assert)
              (("1" (rewrite "cos_minus")
                (("1" (rewrite "sin_minus")
                  (("1" (rewrite "sin_pi")
                    (("1" (rewrite "cos_pi")
                      (("1" (assert)
                        (("1"
                          (lemma "atan2_cancel_neg"
                           ("x" "cos(a)" "y" "sin(a)" "nz" "-1"))
                          (("1" (case-replace "a=pi")
                            (("1" (rewrite "sin_pi")
                              (("1"
                                (rewrite "cos_pi")
                                (("1" (assert) nil nil))
                                nil))
                              nil)
                             ("2" (lemma "sin_eq_0_2pi" ("a" "a"))
                              (("2"
                                (assert)
                                (("2"
                                  (inst - "a-pi")
                                  (("2"
                                    (assert)
                                    (("2"
                                      (rewrite "sin_minus" -3)
                                      (("2"
                                        (rewrite "cos_pi")
                                        (("2"
                                          (rewrite "sin_pi")
                                          (("2" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (assert) nil nil))
            nil))
          nil))
        nil)
       ("2" (hide 2)
        (("2" (skolem 1 ("a"))
          (("2" (flatten)
            (("2" (inst - "a")
              (("1" (assert)
                (("1" (expand "atan2")
                  (("1" (lemma "trichotomy" ("x" "cos(a)"))
                    (("1" (split)
                      (("1" (assert)
                        (("1" (case "a)
                          (("1" (rewrite "tan_rew")
                            (("1" (rewrite "atan_tan")
                              (("1"
                                (expand "abs")
                                (("1" (propax) nil nil))
                                nil))
                              nil)
                             ("2" (expand "Tan?")
                              (("2" (assert) nil nil)) nil))
                            nil)
                           ("2" (lemma "cos_value_strict_decreasing")
                            (("2" (case-replace "a=pi/2")
                              (("1"
                                (rewrite "cos_pi2")
                                (("1" (assert) nil nil))
                                nil)
                               ("2"
                                (expand "strict_decreasing?")
                                (("2"
                                  (inst - "pi/2" "a")
                                  (("2"
                                    (rewrite "cos_value_pi2")
                                    (("2"
                                      (assert)
                                      (("2"
                                        (lemma
                                         "cos_cos_value"
                                         ("a" "a"))
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (replace -1)
                        (("2" (lemma "cos_eq_0_2pi" ("a" "a"))
                          (("2" (assert) nil nil)) nil))
                        nil)
                       ("3" (assert)
                        (("3" (lemma "cos_value_strict_decreasing")
                          (("3" (expand "strict_decreasing?")
                            (("3"
                              (lemma "trich_lt" ("x" "a" "y" "pi/2"))
                              (("3"
                                (split)
                                (("1"
                                  (inst - "a" "pi/2")
                                  (("1"
                                    (rewrite "cos_value_pi2")
                                    (("1"
                                      (assert)
                                      (("1"
                                        (rewrite "cos_cos_value" -3)
                                        (("1" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (replace -1)
                                  (("2"
                                    (rewrite "cos_pi2")
                                    (("2" (assert) nil nil))
                                    nil))
                                  nil)
                                 ("3"
                                  (hide -2)
                                  (("3"
                                    (name "b" "a-pi/2")
                                    (("3"
                                      (lemma "sin_plus")
                                      (("3"
                                        (lemma "cos_plus")
                                        (("3"
                                          (inst - "b" "pi/2")
                                          (("3"
                                            (inst - "b" "pi/2")
                                            (("3"
                                              (rewrite "cos_pi2")
                                              (("3"
                                                (rewrite "sin_pi2")
                                                (("3"
                                                  (assert)
                                                  (("3"
                                                    (replace -3 -1 rl)
                                                    (("3"
                                                      (replace
                                                       -3
                                                       -2
                                                       rl)
                                                      (("3"
                                                        (assert)
                                                        (("3"
                                                          (replace -3)
                                                          (("3"
                                                            (replace
                                                             -1)
                                                            (("3"
                                                              (replace
                                                               -2)
                                                              (("3"
                                                                (hide
                                                                 -1
                                                                 -2)
                                                                (("3"
                                                                  (lemma
                                                                   "atan_neg"
                                                                   ("x"
                                                                    "cos(b)/sin(b)"))
                                                                  (("3"
                                                                    (replace
                                                                     -1
                                                                     1)
                                                                    (("3"
                                                                      (lemma
                                                                       "posreal_div_posreal_is_posreal"
                                                                       ("px"
                                                                        "cos(b)"
                                                                        "py"
                                                                        "sin(b)"))
                                                                      (("3"
                                                                        (lemma
                                                                         "atan_inv"
                                                                         ("px"
                                                                          "cos(b) / sin(b)"))
                                                                        (("1"
                                                                          (rewrite
                                                                           "div_div1"
                                                                           -1)
                                                                          (("1"
                                                                            (assert)
                                                                            (("1"
                                                                              (case-replace
                                                                               "((1 * sin(b)) / cos(b))=tan(b)")
                                                                              (("1"
                                                                                (rewrite
                                                                                 "atan_tan"
                                                                                 -2)
                                                                                (("1"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil)
                                                                                 ("2"
                                                                                  (expand
                                                                                   "abs")
                                                                                  (("2"
                                                                                    (assert)
                                                                                    nil
                                                                                    nil))
                                                                                  nil))
--> --------------------

--> maximum size reached

--> --------------------