Quelle  sincos.prf   Sprache: Lisp

(sincos
 (noa_nnreal_lt_pi2 0
  (noa_nnreal_lt_pi2-1 nil 3477822201
   ("" (expand "not_one_element?")
    (("" (skosimp*)
      (("" (inst-cp + "pi/4")
        (("" (inst + "pi/8") (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((pi 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 "[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)
    (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)
    (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)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil))
   shostak))
 (noa_real_lt_pi2 0
  (noa_real_lt_pi2-1 nil 3477822300
   ("" (expand "not_one_element?")
    (("" (skosimp*)
      (("" (inst-cp + "pi/4")
        (("" (inst + "pi/8") (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
    (pi 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)
    (- 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)
    (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)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil))
   nil))
 (noa_posreal_lt_pi 0
  (noa_posreal_lt_pi-1 nil 3477822312
   ("" (expand "not_one_element?")
    (("" (skosimp*)
      (("" (inst-cp + "pi/4")
        (("" (inst + "pi/8") (("" (assert) nil nil)) nil)) nil))
      nil))
    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)
    (posreal_lt_pi nonempty-type-eq-decl nil sincos_quad nil)
    (pi const-decl "posreal" atan nil) (< const-decl "bool" 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)
    (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)
    (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)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/"))
   nil))
 (noa_nnreal_pi4_to_pi 0
  (noa_nnreal_pi4_to_pi-1 nil 3477822324
   ("" (expand "not_one_element?")
    (("" (skosimp*)
      (("" (inst-cp + "3*pi/4")
        (("" (inst-cp + "pi/2") (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (< const-decl "bool" reals nil) (pi 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 "[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)
    (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)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil))
   nil))
 (noa_posreal_pi2_to_pi 0
  (noa_posreal_pi2_to_pi-1 nil 3477822372
   ("" (expand "not_one_element?")
    (("" (skosimp*)
      (("" (inst-cp + "3*pi/4")
        (("" (inst + "pi/2") (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (< const-decl "bool" reals nil) (pi const-decl "posreal" atan 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)
    (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)
    (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)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil))
   nil))
 (noa_nnreal_lt_pi4 0
  (noa_nnreal_lt_pi4-1 nil 3477822408
   ("" (expand "not_one_element?")
    (("" (skosimp*)
      (("" (inst-cp + "pi/8")
        (("" (inst + "pi/10") (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((pi 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 "[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)
    (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)
    (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)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil))
   nil))
 (noa_mpi4_to_pi4 0
  (noa_mpi4_to_pi4-1 nil 3477822445
   ("" (expand "not_one_element?")
    (("" (skosimp*)
      (("" (inst-cp + "pi/8")
        (("" (inst + "0") (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((pi 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)
    (- 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)
    (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)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil))
   nil))
 (conn_nnreal_lt_p2 0
  (conn_nnreal_lt_p2-1 nil 3477822472
   ("" (expand "connected?")
    (("" (skosimp*) (("" (assert) nil nil)) nil)) nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (connected? const-decl "bool" deriv_domain_def "analysis/")
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil))
   shostak))
 (conn_nnreal_pi4_to_pi 0
  (conn_nnreal_pi4_to_pi-1 nil 3477822481
   ("" (expand "connected?")
    (("" (skosimp*) (("" (assert) nil nil)) nil)) nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (connected? const-decl "bool" deriv_domain_def "analysis/")
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil))
   shostak))
 (conn_posreal_pi2_to_pi 0
  (conn_posreal_pi2_to_pi-1 nil 3477822492
   ("" (expand "connected?")
    (("" (skosimp*) (("" (assert) nil nil)) nil)) nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (connected? const-decl "bool" deriv_domain_def "analysis/")
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil))
   shostak))
 (conn_nnreal_lt_pi4 0
  (conn_nnreal_lt_pi4-1 nil 3477822502
   ("" (expand "connected?")
    (("" (skosimp*) (("" (assert) nil nil)) nil)) nil)
   ((real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (connected? const-decl "bool" deriv_domain_def "analysis/")
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil))
   shostak))
 (deriv_domain_nnreal_lt_pi2 0
  (deriv_domain_nnreal_lt_pi2-1 nil 3477822510
   ("" (lemma "deriv_domain_co")
    (("" (inst - "0" "pi/2")
      (("" (assert)
        (("" (expand "deriv_domain?")
          (("" (skosimp*)
            (("" (inst - "e!1" "x!1")
              (("" (skosimp*) (("" (inst?) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     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)
    (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)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (pi const-decl "posreal" atan nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnreal type-eq-decl nil real_types nil)
    (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (deriv_domain_co formula-decl nil deriv_domain "analysis/"))
   shostak))
 (deriv_domain_real_abs_lt_pi2 0
  (deriv_domain_real_abs_lt_pi2-1 nil 3477822569
   ("" (lemma "deriv_domain_open")
    (("" (inst - "-pi/2" "pi/2") nil nil)) nil)
   ((nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx 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)
    (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)
    (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)
    (pi const-decl "posreal" atan nil)
    (deriv_domain_open formula-decl nil deriv_domain "analysis/"))
   shostak))
 (deriv_domain_posreal_pi2_to_pi 0
  (deriv_domain_posreal_pi2_to_pi-1 nil 3477822648
   ("" (lemma "deriv_domain_co")
    (("" (inst - "pi/2" "pi")
      (("" (assert)
        (("" (expand "deriv_domain?")
          (("" (skosimp*)
            (("" (inst - "e!1" "x!1")
              (("" (skosimp*) (("" (inst?) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     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)
    (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)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (pi const-decl "posreal" atan nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (< const-decl "bool" reals nil) (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_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)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (deriv_domain_co formula-decl nil deriv_domain "analysis/"))
   shostak))
 (deriv_domain_posreal_lt_pi 0
  (deriv_domain_posreal_lt_pi-1 nil 3477822724
   ("" (lemma "deriv_domain_open")
    (("" (inst - "0" "pi")
      (("" (assert)
        (("" (expand "deriv_domain?")
          (("" (skosimp*)
            (("" (inst - "e!1" "x!1")
              (("" (skosimp*) (("" (inst?) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (pi const-decl "posreal" atan nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (deriv_domain_posreal_lt_pi formula-decl nil sincos_quad nil)
    (deriv_domain_open formula-decl nil deriv_domain "analysis/"))
   shostak))
 (deriv_domain_nnreal_pi4_to_pi 0
  (deriv_domain_nnreal_pi4_to_pi-1 nil 3477822763
   ("" (lemma "deriv_domain_co")
    (("" (inst - "pi/4" "pi")
      (("" (expand "deriv_domain?")
        (("" (skosimp*)
          (("" (inst - "e!1" "x!1")
            (("" (skosimp*) (("" (inst?) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     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)
    (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)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (pi const-decl "posreal" atan 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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (deriv_domain_co formula-decl nil deriv_domain "analysis/"))
   shostak))
 (deriv_domain_nnreal_lt_pi4 0
  (deriv_domain_nnreal_lt_pi4-1 nil 3477822797
   ("" (lemma "deriv_domain_co")
    (("" (inst - "0" "pi/4")
      (("" (expand "deriv_domain?")
        (("" (skosimp*)
          (("" (inst - "e!1" "x!1")
            (("" (skosimp*) (("" (inst?) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     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)
    (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)
    (> const-decl "bool" reals nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (pi const-decl "posreal" atan nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (real_le_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)
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (deriv_domain_co formula-decl nil deriv_domain "analysis/"))
   shostak))
 (deriv_domain_mpi4_to_pi4 0
  (deriv_domain_mpi4_to_pi4-1 nil 3477822834
   ("" (lemma "deriv_domain_open")
    (("" (inst - "-pi/4" "pi/4") nil nil)) nil)
   ((nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx 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)
    (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)
    (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)
    (pi const-decl "posreal" atan nil)
    (deriv_domain_open formula-decl nil deriv_domain "analysis/"))
   shostak))
 (cos_ub 0
         (cos_ub-1 nil 3265619589
          ("" (skosimp*)
           (("" (typepred "cos(x!1)") (("" (propax) nil nil)) nil))
           nil)
          ((cos const-decl "real" sincos_def nil)
           (- const-decl "[numfield -> numfield]" number_fields 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)
           (NOT const-decl "[bool -> bool]" booleans nil)
           (bool nonempty-type-eq-decl nil booleans nil)
           (boolean nonempty-type-decl nil booleans nil)
           (cos_range application-judgement "trig_range" sincos_def
            nil))
          shostak))
 (sin_ub 0
  (sin_ub-4 nil 3425655889
   ("" (skolem 1 ("px"))
    (("" (case "px<=1")
      (("1" (expand "sin")
        (("1" (lemma "floor_def" ("x" "px/(2*pi)"))
          (("1" (rewrite "div_mult_pos_lt1")
            (("1" (rewrite "div_mult_pos_le2")
              (("1" (flatten)
                (("1" (lemma "trichotomy" ("x" "floor(px / (2 * pi))"))
                  (("1" (split -1)
                    (("1" (case "floor(px / (2 * pi)) =1")
                      (("1" (lemma "pi_bnds")
                        (("1" (flatten) (("1" (assert) nil nil)) nil))
                        nil)
                       ("2" (case "floor(px / (2 * pi))>1")
                        (("1" (lemma "pi_bnds")
                          (("1" (flatten)
                            (("1" (assert)
                              (("1"
                                (lemma
                                 "both_sides_times_pos_lt1"
                                 ("x"
                                  "1"
                                  "y"
                                  "floor(px / (2 * pi))"
                                  "pz"
                                  "2*pi"))
                                (("1" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (assert) nil nil))
                        nil))
                      nil)
                     ("2" (replace -1)
                      (("2" (hide -1 -2 -3)
                        (("2" (simplify 1)
                          (("2" (lemma "pi_bnds")
                            (("2" (flatten)
                              (("2"
                                (lemma "phases_sin" ("x" "px"))
                                (("2"
                                  (split -1)
                                  (("1"
                                    (rewrite "sin_q1")
                                    (("1"
                                      (hide -1)
                                      (("1"
                                        (lemma
                                         "sin_value_derivable_fun")
                                        (("1"
                                          (lemma "deriv_sin_value")
                                          (("1"
                                            (lemma
                                             "identity_derivable_fun[real_abs_lt_pi2]")
                                            (("1"
                                              (lemma
                                               "deriv_id_fun[real_abs_lt_pi2]")
                                              (("1"
                                                (expand "I")
                                                (("1"
                                                  (expand "const_fun")
                                                  (("1"
                                                    (lemma
                                                     "diff_derivable_fun[real_abs_lt_pi2]"
                                                     ("f1"
                                                      "LAMBDA (x: real_abs_lt_pi2): x"
                                                      "f2"
                                                      "LAMBDA (x: real_abs_lt_pi2): sin_value(x)"))
                                                    (("1"
                                                      (lemma
                                                       "deriv_diff_fun[real_abs_lt_pi2]"
                                                       ("ff1"
                                                        "LAMBDA (x: real_abs_lt_pi2): x"
                                                        "ff2"
                                                        "LAMBDA (x: real_abs_lt_pi2): sin_value(x)"))
                                                      (("1"
                                                        (replace -3 -1)
                                                        (("1"
                                                          (replace
                                                           -5
                                                           -1)
                                                          (("1"
                                                            (expand
                                                             "-")
                                                            (("1"
                                                              (assert)
                                                              (("1"
                                                                (lemma
                                                                 "identity_derivable_fun[{x:nnreal|x)
                                                                (("1"
                                                                  (lemma
                                                                   "deriv_id_fun[{x:nnreal|x)
                                                                  (("1"
                                                                    (expand
                                                                     "I")
                                                                    (("1"
                                                                      (expand
                                                                       "const_fun")
                                                                      (("1"
                                                                        (lemma
                                                                         "composition_derivable_fun[{x: nnreal | x < pi / 2},real_abs_lt_pi2]"
                                                                         ("f"
                                                                          "LAMBDA (x: {x: nnreal | x < pi / 2}): x"
                                                                          "g"
                                                                          "LAMBDA (x_1: real_abs_lt_pi2): x_1 - sin_value(x_1)"))
                                                                        (("1"
                                                                          (replace
                                                                           -3)
                                                                          (("1"
                                                                            (replace
                                                                             -5)
                                                                            (("1"
                                                                              (expand
                                                                               "o")
                                                                              (("1"
                                                                                (lemma
                                                                                 "deriv_comp_fun[{x: nnreal | x < pi / 2},real_abs_lt_pi2]"
                                                                                 ("ff"
                                                                                  "LAMBDA (x: {x: nnreal | x < pi / 2}): x"
                                                                                  "gg"
                                                                                  "LAMBDA (x_1: real_abs_lt_pi2): x_1 - sin_value(x_1)"))
                                                                                (("1"
                                                                                  (expand
                                                                                   "o")
                                                                                  (("1"
                                                                                    (replace
                                                                                     -3
                                                                                     -1)
                                                                                    (("1"
                                                                                      (replace
                                                                                       -5
                                                                                       -1)
                                                                                      (("1"
                                                                                        (expand
                                                                                         "*"
                                                                                         -1)
                                                                                        (("1"
                                                                                          (lemma
                                                                                           "minimum_derivative[{x: nnreal | x < pi / 2}]"
                                                                                           ("g"
                                                                                            "LAMBDA (x_1: {x: nnreal | x < pi / 2}): x_1 - sin_value(x_1)"
                                                                                            "x"
                                                                                            "0"
                                                                                            "y1"
                                                                                            "px"))
                                                                                          (("1"
                                                                                            (split
                                                                                             -1)
                                                                                            (("1"
                                                                                              (simplify
                                                                                               -1)
                                                                                              (("1"
                                                                                                (rewrite
                                                                                                 "sin_value_0")
                                                                                                (("1"
                                                                                                  (assert)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil)
                                                                                             ("2"
                                                                                              (replace
                                                                                               -1
                                                                                               1)
                                                                                              (("2"
                                                                                                (assert)
                                                                                                (("2"
                                                                                                  (expand
                                                                                                   "abs")
                                                                                                  (("2"
                                                                                                    (rewrite
                                                                                                     "cos_value_0")
                                                                                                    (("2"
                                                                                                      (assert)
                                                                                                      nil
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil)
                                                                                             ("3"
                                                                                              (assert)
                                                                                              nil
                                                                                              nil)
                                                                                             ("4"
                                                                                              (replace
                                                                                               -1
                                                                                               1)
                                                                                              (("4"
                                                                                                (hide-all-but
                                                                                                 1)
                                                                                                (("4"
                                                                                                  (skosimp*)
                                                                                                  (("4"
                                                                                                    (expand
                                                                                                     "abs")
                                                                                                    (("4"
                                                                                                      (lemma
                                                                                                       "cos_value_strict_decreasing")
                                                                                                      (("4"
                                                                                                        (expand
                                                                                                         "strict_decreasing?")
                                                                                                        (("4"
                                                                                                          (inst
                                                                                                           -
                                                                                                           "0"
                                                                                                           "y!1")
                                                                                                          (("4"
                                                                                                            (rewrite
                                                                                                             "cos_value_0")
                                                                                                            (("4"
                                                                                                              (assert)
                                                                                                              (("4"
                                                                                                                (lemma
                                                                                                                 "posreal_times_posreal_is_posreal"
                                                                                                                 ("px"
                                                                                                                  "1-cos_value(y!1)"
                                                                                                                  "py"
                                                                                                                  "y!1"))
                                                                                                                (("4"
                                                                                                                  (assert)
                                                                                                                  nil
                                                                                                                  nil))
                                                                                                                nil))
                                                                                                              nil))
                                                                                                            nil))
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil)
                                                                                           ("2"
                                                                                            (propax)
                                                                                            nil
                                                                                            nil)
                                                                                           ("3"
                                                                                            (skosimp*)
                                                                                            (("3"
                                                                                              (assert)
                                                                                              nil
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("2"
                                                                                  (propax)
                                                                                  nil
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (hide-all-but
                                                                   1)
                                                                  (("2"
                                                                    (skosimp*)
                                                                    (("2"
                                                                      (case
                                                                       "x!1=0")
                                                                      (("1"
                                                                        (inst
                                                                         +
                                                                         "pi/4")
                                                                        (("1"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil)
                                                                       ("2"
                                                                        (inst
                                                                         +
                                                                         "0")
                                                                        (("2"
                                                                          (assert)
                                                                          nil
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("3"
                                                                  (hide-all-but
                                                                   1)
                                                                  (("3"
                                                                    (lemma
                                                                     deriv_domain_nnreal_lt)
                                                                    (("3"
                                                                      (inst
                                                                       -
                                                                       pi/2)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (propax)
                                                        nil
                                                        nil)
                                                       ("3"
                                                        (propax)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (hide-all-but 1)
                                              (("2"
                                                (skosimp*)
                                                (("2"
                                                  (case "x!1=0")
                                                  (("1"
                                                    (inst + "pi/4")
                                                    (("1"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (inst + "0")
                                                    (("2"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("3"
                                              (hide-all-but 1)
                                              (("3"
                                                (lemma
                                                 deriv_domain_open)
                                                (("3"
                                                  (inst - -pi/2 pi/2)
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (rewrite "phase_sin_q2")
                                    (("2"
                                      (flatten)
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil)
                                   ("3"
                                    (rewrite "phase_sin_q3")
                                    (("3"
                                      (flatten)
                                      (("3" (assert) nil nil))
                                      nil))
                                    nil)
                                   ("4"
                                    (rewrite "phase_sin_q4")
                                    (("4"
                                      (flatten)
                                      (("4" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("3" (assert) nil nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (typepred "sin(px)") (("2" (assert) nil nil)) nil))
      nil))
    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 "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)
    (pi const-decl "posreal" atan nil)
    (* const-decl "[numfield, 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)
    (floor_def formula-decl nil floor_ceil nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (div_mult_pos_le2 formula-decl nil real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (trichotomy formula-decl nil real_axioms nil)
    (deriv_sin_value formula-decl nil sincos_quad nil)
    (deriv_id_fun formula-decl nil derivatives "analysis/")
    (diff_derivable_fun formula-decl nil derivatives "analysis/")
    (real_abs_le_pi2 nonempty-type-eq-decl nil asin nil)
    (real_abs_le1 nonempty-type-eq-decl nil asin nil)
    (sin_value const-decl "[real_abs_le_pi2 -> real_abs_le1]"
     sincos_quad nil)
    (- const-decl "[T -> real]" real_fun_ops "reals/")
    (O const-decl "T3" function_props nil)
    (minimum_derivative formula-decl nil derivative_props "analysis/")
    (connected? const-decl "bool" deriv_domain_def "analysis/")
    (cos_value_strict_decreasing formula-decl nil sincos_quad nil)
    (nnreal_le_pi nonempty-type-eq-decl nil acos nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (cos_value const-decl "[nnreal_le_pi -> real_abs_le1]" sincos_quad
     nil)
    (posreal_times_posreal_is_posreal judgement-tcc nil real_types nil)
    (strict_decreasing? const-decl "bool" real_fun_preds "reals/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (cos_value_0 formula-decl nil sincos_quad nil)
    (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
     real_defs nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (int_times_even_is_even application-judgement "even_int" integers
     nil)
    (sin_value_0 formula-decl nil sincos_quad nil)
    (* const-decl "[T -> real]" real_fun_ops "reals/")
    (deriv_comp_fun formula-decl nil chain_rule "analysis/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (composition_derivable_fun formula-decl nil chain_rule "analysis/")
    (deriv_fun type-eq-decl nil derivatives "analysis/")
    (derivable? const-decl "bool" derivatives "analysis/")
    (deriv_diff_fun formula-decl nil derivatives "analysis/")
    (I const-decl "(bijective?[T, T])" identity nil)
    (not_one_element? const-decl "bool" deriv_domain_def "analysis/")
    (deriv_domain? const-decl "bool" deriv_domain_def "analysis/")
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (real_abs_lt_pi2 nonempty-type-eq-decl nil atan nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (identity_derivable_fun formula-decl nil derivatives "analysis/")
    (sin_value_derivable_fun formula-decl nil sincos_quad nil)
    (sin_q1 formula-decl nil sincos_phase nil)
    (phase_sin_q2 formula-decl nil sincos_phase nil)
    (phase_sin_q3 formula-decl nil sincos_phase nil)
    (phase_sin_q4 formula-decl nil sincos_phase nil)
    (trig_phase nonempty-type-eq-decl nil sincos_phase nil)
    (nnreal type-eq-decl nil real_types nil)
    (phases_sin formula-decl nil sincos_phase nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnreal_plus_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (pi_bnds formula-decl nil atan nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (both_sides_times_pos_lt1 formula-decl nil real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (floor const-decl "{i | i <= x & x < i + 1}" floor_ceil nil)
    (< const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (integer nonempty-type-from-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (div_mult_pos_lt1 formula-decl nil real_props nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (sin const-decl "real" sincos_def nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (pi_bound name-judgement "{r: posreal | pi_lb < r AND r < pi_ub}"
     atan_approx nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (sin_range application-judgement "trig_range" sincos_def nil)
    (NOT const-decl "[bool -> bool]" booleans nil))
   nil)
  (sin_ub-3 nil 3408979329
   ("" (skolem 1 ("px"))
    (("" (case "px<=1")
      (("1" (expand "sin")
        (("1" (lemma "floor_def" ("x" "px/(2*pi)"))
          (("1" (rewrite "div_mult_pos_lt1")
            (("1" (rewrite "div_mult_pos_le2")
              (("1" (flatten)
                (("1" (lemma "trichotomy" ("x" "floor(px / (2 * pi))"))
                  (("1" (split -1)
                    (("1" (case "floor(px / (2 * pi)) =1")
                      (("1" (lemma "pi_bnds")
                        (("1" (flatten) (("1" (assert) nil nil)) nil))
                        nil)
                       ("2" (case "floor(px / (2 * pi))>1")
                        (("1" (lemma "pi_bnds")
                          (("1" (flatten)
                            (("1" (assert)
                              (("1"
                                (lemma
--> --------------------

--> maximum size reached

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