Quelle  gs_bands_2D.prf

(gs_bands_2D
 (gs_band_pos 0
  (gs_band_pos-2 nil 3444146224
   ("" (skeep :preds? t)
    (("" (hide -1) (("" (inst?) (("" (assert) nil nil)) nil)) nil))
    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)
    (ConnectedGt type-eq-decl nil connected_set "reals/")
    (> const-decl "bool" reals nil)
    (Connected type-eq-decl nil connected_set "reals/")
    (<= const-decl "bool" reals nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (set type-eq-decl nil sets 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))
   nil)
  (gs_band_pos-1 nil 3444146224 ("" (judgement-tcc) nil nil) nil nil))
 (gs2v2_continuous 0
  (gs2v2_continuous-2 nil 3459320448
   ("" (skeep)
    (("" (expand "gs2v2")
      (("" (rewrite "scal_cont_rv")
        (("1" (hide 2) (("1" (rewrite "const_cont_rv") nil nil)) nil)
         ("2" (hide 2) (("2" (rewrite "id_cont") nil nil)) nil))
        nil))
      nil))
    nil)
   ((gs2v2 const-decl "Vect2" bands_util nil)
    (id_cont formula-decl nil continuous_lambda "analysis/")
    (const_cont_rv formula-decl nil vect_cont_2D "vect_analysis/")
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (^ const-decl "Normalized" vectors_2D "vectors/")
    (Normalized type-eq-decl nil vectors_2D "vectors/")
    (norm const-decl "nnreal" vectors_2D "vectors/")
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Nz_vector type-eq-decl nil vectors_2D "vectors/")
    (zero const-decl "Vector" vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (continuous_rv? const-decl "bool" cont_real_vect2 "vect_analysis/")
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (continuous_fun nonempty-type-eq-decl nil continuous_functions
     "analysis/")
    (continuous? const-decl "bool" continuous_functions "analysis/")
    (bool nonempty-type-eq-decl nil booleans nil)
    (scal_cont_rv formula-decl nil vect2_cont_dot "vect_analysis/"))
   nil)
  (gs2v2_continuous-1 nil 3459320431 ("" (judgement-tcc) nil nil) nil
   nil))
 (Vgs_continuous 0
  (Vgs_continuous-2 nil 3444142683
   ("" (skeep)
    (("" (expand "Vgs")
      (("" (rewrite "sub_cont_rv")
        (("1" (hide 2) (("1" (rewrite "const_cont_rv") nil nil)) nil)
         ("2" (hide 2)
          (("2"
            (case-replace
             "(LAMBDA (gs:real):gs2v2(vo)(gs)) = gs2v2(vo)")
            (("1" (assert) nil nil)
             ("2" (decompose-equality 1) nil nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Vgs const-decl "Vect2" gs_bands_2D nil)
    (gs2v2_continuous application-judgement "continuous_rv_fun"
     gs_bands_2D nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (const_cont_rv formula-decl nil vect_cont_2D "vect_analysis/")
    (gs2v2 const-decl "Vect2" bands_util nil)
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (zero const-decl "Vector" vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (continuous_rv_fun nonempty-type-eq-decl nil cont_real_vect2
     "vect_analysis/")
    (continuous_rv? const-decl "bool" cont_real_vect2 "vect_analysis/")
    (bool nonempty-type-eq-decl nil booleans nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (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)
    (sub_cont_rv formula-decl nil vect_cont_2D "vect_analysis/"))
   nil)
  (Vgs_continuous-1 nil 3444142661 ("" (judgement-tcc) nil nil) nil
   nil))
 (Omega_gs_TCC1 0
  (Omega_gs_TCC1-2 nil 3444142120
   ("" (skeep)
    (("" (rewrite "comp_vr_rv_cont")
      (("" (hide 2)
        (("" (lemma "omega_v2_continuous")
          (("" (inst?)
            (("" (expand "continuous?")
              (("" (expand "continuous?")
                (("" (expand "continuous_vr?")
                  (("" (expand "continuous_at?")
                    (("" (expand "continuous_vr?")
                      (("" (expand "member")
                        (("" (expand "ball")
                          (("" (expand "real_dist")
                            (("" (skeep)
                              ((""
                                (inst - "x0")
                                (("1"
                                  (skosimp*)
                                  (("1"
                                    (inst - "epsilon!1")
                                    (("1"
                                      (skosimp*)
                                      (("1"
                                        (inst + "delta!1")
                                        (("1"
                                          (skosimp*)
                                          (("1"
                                            (inst - "x!1")
                                            (("1"
                                              (lemma "dist_norm")
                                              (("1"
                                                (inst?)
                                                (("1"
                                                  (case
                                                   "abs(omega_v2[D, B, T](s)(x0) - omega_v2[D, B, T](s)(x!1)) = abs(omega_v2[D,B, T](s)(x!1) - omega_v2[D, B, T](s)(x0)) and norm(x0-x!1) = norm(x!1-x0)")
                                                  (("1"
                                                    (flatten)
                                                    (("1"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (hide-all-but 1)
                                                    (("2"
                                                      (grind
                                                       :exclude
                                                       "omega_v2")
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (expand "fullset")
                                              (("2" (propax) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (expand "fullset")
                                  (("2" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Vgs_continuous application-judgement "continuous_rv_fun"
     gs_bands_2D nil)
    (comp_vr_rv_cont formula-decl nil vect2_cont_comp "vect_analysis/")
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (bool nonempty-type-eq-decl nil booleans nil)
    (continuous_rv? const-decl "bool" cont_real_vect2 "vect_analysis/")
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (Vgs const-decl "Vect2" gs_bands_2D nil)
    (continuous_vr? const-decl "bool" cont_vect2_real "vect_analysis/")
    (>= 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)
    (D formal-const-decl "posreal" gs_bands_2D nil)
    (nnreal type-eq-decl nil real_types nil)
    (B formal-const-decl "nnreal" gs_bands_2D nil)
    (T formal-const-decl "{AB: posreal | AB > B}" gs_bands_2D nil)
    (omega_v2 const-decl "real" omega_v2 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)
    (omega_v2_continuous formula-decl nil omega_v2 nil)
    (continuous? const-decl "bool" continuity_ms_def "analysis/")
    (real_minus_real_is_real application-judgement "real" reals nil)
    (continuous_vr? const-decl "bool" cont_vect2_real "vect_analysis/")
    (ball const-decl "set[T]" metric_spaces "analysis/")
    (dist_norm formula-decl nil distance_2D "vectors/")
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (norm const-decl "nnreal" vectors_2D "vectors/")
    (- const-decl "Vector" vectors_2D "vectors/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (* const-decl "real" vectors_2D "vectors/")
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
     "vect_analysis/")
    (x!1 skolem-const-decl "Vect2" gs_bands_2D nil)
    (x0 skolem-const-decl "Vect2" gs_bands_2D nil)
    (fullset const-decl "set" sets nil) (set type-eq-decl nil sets nil)
    (real_dist const-decl "nnreal" real_metric_space "analysis/")
    (member const-decl "bool" sets nil)
    (continuous_at? const-decl "bool" continuity_ms_def "analysis/")
    (continuous? const-decl "bool" continuity_ms_def "analysis/"))
   nil)
  (Omega_gs_TCC1-1 nil 3444142060 ("" (subtype-tcc) nil nil) nil nil))
 (Omega_gs_critical 0
  (Omega_gs_critical-1 nil 3443205728
   ("" (skeep)
    (("" (expand "Omega_gs")
      (("" (expand "o")
        (("" (expand "Vgs")
          (("" (lemma "omega_v2_critical_points")
            (("" (inst?)
              (("" (assert)
                (("" (expand "gs_critical?")
                  (("" (flatten)
                    (("" (split -1)
                      (("1" (flatten)
                        (("1" (assert)
                          (("1" (lemma "gs_line_complete")
                            (("1" (inst?) (("1" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (lemma "gs_only_circle_complete")
                        (("2"
                          (inst - "Entry" "gs2v2(vo)(gsp)" "s" "T" "vi"
                           "vo")
                          (("2" (assert) nil nil)) nil))
                        nil)
                       ("3" (flatten)
                        (("3" (lemma "gs_only_circle_complete")
                          (("3"
                            (inst - "Exit" "gs2v2(vo)(gsp)" "s" "B"
                             "vi" "vo")
                            (("3" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Omega_gs const-decl "({f | continuous?(f)})" gs_bands_2D nil)
    (Vgs const-decl "Vect2" gs_bands_2D nil)
    (gs2v2 const-decl "Vect2" bands_util nil)
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (zero const-decl "Vector" vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (- const-decl "Vector" vectors_2D "vectors/")
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (gs_critical? const-decl "bool" gs_bands_2D nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (Sp_vect2 type-eq-decl nil horizontal nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (gs_line_complete formula-decl nil gs_line nil)
    (Sign type-eq-decl nil sign "reals/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (nzint nonempty-type-eq-decl nil integers nil)
    (int nonempty-type-eq-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)
    (gs_only_circle_complete formula-decl nil gs_only nil)
    (gs2v2_gs_only application-judgement "(gs_only?(vo2))" bands_util
     nil)
    (gs2v2_continuous application-judgement "continuous_rv_fun"
     gs_bands_2D nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
     "vect_analysis/")
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (omega_v2_critical_points formula-decl nil omega_v2 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)
    (D formal-const-decl "posreal" gs_bands_2D nil)
    (nnreal type-eq-decl nil real_types nil)
    (B formal-const-decl "nnreal" gs_bands_2D nil)
    (T formal-const-decl "{AB: posreal | AB > B}" gs_bands_2D nil)
    (O const-decl "[T -> real]" vect2_cont_comp "vect_analysis/"))
   nil))
 (gs_green_two_parallel 0
  (gs_green_two_parallel-1 nil 3443208598
   ("" (skeep)
    (("" (expand "two_parallel?")
      (("" (flatten)
        (("" (skeep -2)
          (("" (expand "gs_green?")
            (("" (expand "Vgs")
              (("" (expand "gs2v2")
                (("" (skeep 1)
                  ((""
                    (name-replace "cr" "tangent_line(sp,eps)" :hide?
                     nil)
                    (("" (case "det(gso * ^(vo) - vi,cr)=0")
                      (("1" (hide -3 -4)
                        (("1" (rewrite "parallel_det_0" :dir rl)
                          (("1" (expand "parallel?")
                            (("1" (skolem -1 "kk")
                              (("1"
                                (lemma "tangent_line_independence")
                                (("1"
                                  (inst -1 "eps" "sp" "cr")
                                  (("1"
                                    (split -1)
                                    (("1"
                                      (lemma
                                       "horizontal_conflict_ever_scal")
                                      (("1"
                                        (inst -1 "kk" "sp" "cr")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (hide 2)
                                            (("1"
                                              (expand "conflict_2D?")
                                              (("1"
                                                (expand
                                                 "horizontal_conflict_ever?")
                                                (("1"
                                                  (skeep -3)
                                                  (("1"
                                                    (inst 1 "t")
                                                    (("1"
                                                      (replaces
                                                       -1
                                                       :dir
                                                       rl)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (expand "tangent_line?")
                                      (("2"
                                        (inst 1 "1")
                                        (("2" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (flatten)
                            (("2" (replaces -1)
                              (("2"
                                (expand "conflict_2D?")
                                (("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (hide -1 -4)
                        (("2" (rewrite "det_asym")
                          (("2" (rewrite "det_sub_right")
                            (("2" (expand "^")
                              (("2"
                                (rewrite "scal_assoc")
                                (("2"
                                  (rewrite "det_scal_right")
                                  (("2"
                                    (rewrite "det_asym" 1)
                                    (("2"
                                      (replace -2)
                                      (("2"
                                        (assert)
                                        (("2"
                                          (rewrite
                                           "parallel_det_0"
                                           :dir
                                           rl)
                                          (("2"
                                            (rewrite
                                             "parallel_det_0"
                                             :dir
                                             rl)
                                            (("2"
                                              (lemma
                                               "vectors_2D.parallel_trans")
                                              (("2"
                                                (inst
                                                 -1
                                                 "vi"
                                                 "vo"
                                                 "cr")
                                                (("2"
                                                  (assert)
                                                  (("2"
                                                    (hide-all-but
                                                     (-1 1))
                                                    (("2"
                                                      (rewrite
                                                       "parallel_det_0")
                                                      (("2"
                                                        (rewrite
                                                         "det_asym")
                                                        (("2"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((two_parallel? const-decl "bool" gs_line nil)
    (Vgs const-decl "Vect2" gs_bands_2D nil)
    (det const-decl "real" det_2D "vectors/")
    (- const-decl "Vector" vectors_2D "vectors/")
    (* const-decl "Vector" vectors_2D "vectors/")
    (set type-eq-decl nil sets nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (Connected type-eq-decl nil connected_set "reals/")
    (ConnectedGt type-eq-decl nil connected_set "reals/")
    (Nz_vector type-eq-decl nil vectors_2D "vectors/")
    (norm const-decl "nnreal" vectors_2D "vectors/")
    (Normalized type-eq-decl nil vectors_2D "vectors/")
    (^ const-decl "Normalized" vectors_2D "vectors/")
    (nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
    (parallel_det_0 formula-decl nil parallel_2D "vectors/")
    (tangent_line? const-decl "bool" tangent_line nil)
    (scal_1 formula-decl nil vectors_2D "vectors/")
    (horizontal_conflict_ever_scal formula-decl nil horizontal nil)
    (conflict_2D? const-decl "bool" cd2d nil)
    (B formal-const-decl "nnreal" gs_bands_2D nil)
    (T formal-const-decl "{AB: posreal | AB > B}" gs_bands_2D nil)
    (Lookahead type-eq-decl nil Lookahead nil)
    (horizontal_conflict_ever? const-decl "bool" horizontal nil)
    (nzreal nonempty-type-eq-decl nil reals nil)
    (tangent_line_independence formula-decl nil tangent_line nil)
    (parallel? const-decl "bool" vectors_2D "vectors/")
    (scal_zero formula-decl nil vectors_2D "vectors/")
    (add_zero_right formula-decl nil vectors_2D "vectors/")
    (det_asym formula-decl nil det_2D "vectors/")
    (minus_real_is_real application-judgement "real" reals nil)
    (nz_norm_gt_0 application-judgement "posreal" vectors_2D
     "vectors/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (det_scal_right formula-decl nil det_2D "vectors/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (parallel_trans formula-decl nil vectors_2D "vectors/")
    (minus_even_is_even application-judgement "even_int" integers nil)
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (scal_assoc formula-decl nil vectors_2D "vectors/")
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (det_sub_right formula-decl nil det_2D "vectors/")
    (tangent_line const-decl "Nz_vect2" tangent_line nil)
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Sign type-eq-decl nil sign "reals/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (nzint nonempty-type-eq-decl nil integers nil)
    (/= const-decl "boolean" notequal nil)
    (int nonempty-type-eq-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)
    (Sp_vect2 type-eq-decl nil horizontal nil)
    (D formal-const-decl "posreal" gs_bands_2D nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (> const-decl "bool" reals nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans 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)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (gs2v2 const-decl "Vect2" bands_util nil)
    (gs_green? const-decl "bool" gs_bands_2D nil))
   shostak))
 (gs_line_color 0
  (gs_line_color-1 nil 3460208057
   ("" (skeep)
    (("" (expand "Q")
      (("" (rewrite "dot_add_left")
        (("" (lemma "vectors_2D.dot_comm")
          (("" (inst -1 "perpR(ss)" "vo")
            (("" (replaces -1)
              (("" (rewrite "det_perpR" :dir rl)
                (("" (lemma "det_asym")
                  (("" (inst?)
                    (("" (replaces -1)
                      ((""
                        (case-replace
                         "pm*(alpha(ss) * (ss * vo) + beta(ss) * -det(ss, vo) * eps) > 0 = pm*(alpha(ss) * (ss * vo)) > pm*(beta(ss) * det(ss, vo) * eps)")
                        (("1" (hide -1)
                          (("1" (expand "alpha")
                            (("1" (expand "beta")
                              (("1"
                                (case-replace
                                 " pm*(sq(D) / sqv(ss) * (ss * vo)) >
                               pm*(det(ss, vo) * (D * sqrt(sqv(ss) - sq(D)) / sqv(ss)) * eps) = pm*(sq(D)*(ss*vo)) >  pm*(det(ss, vo) * (D * sqrt(sqv(ss) - sq(D))) *eps)")
                                (("1"
                                  (hide -1)
                                  (("1"
                                    (case-replace
                                     "pm*(sq(D) * (ss * vo)) > pm*(det(ss, vo) * (D * sqrt(sqv(ss) - sq(D))) * eps) = pm*(D* (ss * vo)) > pm*(det(ss, vo) * sqrt(sqv(ss) - sq(D)) * eps)")
                                    (("1"
                                      (hide -1)
                                      (("1"
                                        (lift-if)
                                        (("1"
                                          (split 1)
                                          (("1"
                                            (flatten)
                                            (("1"
                                              (split)
                                              (("1"
                                                (flatten)
                                                (("1"
                                                  (split 1)
                                                  (("1"
                                                    (mult-by
                                                     -2
                                                     "sqrt(sqv(ss) - sq(D))")
                                                    (("1"
                                                      (mult-by 1 "D")
                                                      (("1"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (case
                                                     "pm * (det(ss, vo) * sqrt(sqv(ss) - sq(D)) * eps) > 0")
                                                    (("1"
                                                      (both-sides-f
                                                       -2
                                                       "sq")
                                                      (("1"
                                                        (rewrite
                                                         "sq_times")
                                                        (("1"
                                                          (rewrite
                                                           "sq_times")
                                                          (("1"
                                                            (rewrite
                                                             "sq_times")
                                                            (("1"
                                                              (rewrite
                                                               "sq_times")
                                                              (("1"
                                                                (rewrite
                                                                 "sq_times")
                                                                (("1"
                                                                  (lemma
                                                                   "sq_eps")
                                                                  (("1"
                                                                    (inst-cp
                                                                     -1
                                                                     "pm")
                                                                    (("1"
                                                                      (inst
                                                                       -1
                                                                       "eps")
                                                                      (("1"
                                                                        (replaces
                                                                         (-1
                                                                          -2))
                                                                        (("1"
                                                                          (rewrite
                                                                           "sq_det")
                                                                          (("1"
                                                                            (assert)
                                                                            (("1"
                                                                              (move-terms
                                                                               -1
                                                                               r
                                                                               1)
                                                                              (("1"
                                                                                (case-replace
                                                                                 "sq(D) * sq((ss * vo)) - sq(ss * vo) * sq(D) = 0")
                                                                                (("1"
                                                                                  (hide
                                                                                   -1)
                                                                                  (("1"
                                                                                    (mult-by
                                                                                     1
                                                                                     "sqv(ss)")
                                                                                    (("1"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil)
                                                                                 ("2"
                                                                                  (assert)
                                                                                  nil
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (lemma "sq_gt")
                                                        (("2"
                                                          (inst? -1)
                                                          (("1"
                                                            (assert)
                                                            nil
                                                            nil)
                                                           ("2"
                                                            (assert)
                                                            nil
                                                            nil)
                                                           ("3"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (mult-by
                                                       -2
                                                       "sqrt(sqv(ss) - sq(D))")
                                                      (("2"
                                                        (assert)
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (flatten)
                                                (("2"
                                                  (mult-by -1 "D")
                                                  (("2"
                                                    (mult-by
                                                     -3
                                                     "sqrt(sqv(ss)-sq(D))")
                                                    (("2"
                                                      (both-sides-f
                                                       1
                                                       "sq")
                                                      (("1"
                                                        (rewrite
                                                         "sq_times")
                                                        (("1"
                                                          (rewrite
                                                           "sq_times")
                                                          (("1"
                                                            (rewrite
                                                             "sq_times")
                                                            (("1"
                                                              (rewrite
                                                               "sq_times")
                                                              (("1"
                                                                (rewrite
                                                                 "sq_times")
                                                                (("1"
                                                                  (lemma
                                                                   "sq_eps")
                                                                  (("1"
                                                                    (inst-cp
                                                                     -1
                                                                     "pm")
                                                                    (("1"
                                                                      (inst
                                                                       -1
                                                                       "eps")
                                                                      (("1"
                                                                        (replaces
                                                                         (-1
                                                                          -2))
                                                                        (("1"
                                                                          (mult-by
                                                                           -2
                                                                           "sqv(ss)")
                                                                          (("1"
                                                                            (lemma
                                                                             "sq_det")
                                                                            (("1"
                                                                              (inst
                                                                               -1
                                                                               "ss"
                                                                               "vo")
                                                                              (("1"
                                                                                (move-terms
                                                                                 -1
                                                                                 r
                                                                                 2)
                                                                                (("1"
                                                                                  (mult-by
                                                                                   -1
                                                                                   "sq(D)")
                                                                                  (("1"
                                                                                    (replaces
                                                                                     -1
                                                                                     :dir
                                                                                     rl)
                                                                                    (("1"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil)
                                                       ("2"
                                                        (lemma "sq_gt")
                                                        (("2"
                                                          (inst?)
                                                          (("1"
                                                            (assert)
                                                            nil
                                                            nil)
                                                           ("2"
                                                            (assert)
                                                            nil
                                                            nil)
                                                           ("3"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (flatten)
                                            (("2"
                                              (case "pm*(ss*vo) > 0")
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (case
                                                   "pm*(sqrt(sqv(ss) - sq(D)) * det(ss, vo) * eps) <= 0")
                                                  (("1"
                                                    (mult-by -2 "D")
                                                    (("1"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (mult-by
                                                     2
                                                     "sqrt(sqv(ss)-sq(D))")
                                                    (("2"
                                                      (assert)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (split 3)
                                                (("1"
                                                  (flatten)
                                                  (("1"
                                                    (assert)
                                                    (("1"
                                                      (neg-formula -1)
                                                      (("1"
                                                        (both-sides-f
                                                         -1
                                                         "sq")
                                                        (("1"
                                                          (rewrite
                                                           "sq_neg")
                                                          (("1"
                                                            (rewrite
                                                             "sq_times")
                                                            (("1"
                                                              (rewrite
                                                               "sq_times")
                                                              (("1"
                                                                (rewrite
                                                                 "sq_times")
                                                                (("1"
                                                                  (lemma
                                                                   "sq_eps")
                                                                  (("1"
                                                                    (inst-cp
                                                                     -1
                                                                     "pm")
                                                                    (("1"
                                                                      (inst
                                                                       -1
                                                                       "eps")
                                                                      (("1"
                                                                        (rewrite
                                                                         "sq_neg")
                                                                        (("1"
                                                                          (rewrite
                                                                           "sq_times")
                                                                          (("1"
                                                                            (replaces
                                                                             (-1
                                                                              -2))
                                                                            (("1"
                                                                              (mult-by
                                                                               2
                                                                               "sqv(ss)")
                                                                              (("1"
                                                                                (lemma
                                                                                 "sq_det")
                                                                                (("1"
                                                                                  (inst
                                                                                   -1
                                                                                   "ss"
                                                                                   "vo")
                                                                                  (("1"
                                                                                    (move-terms
                                                                                     -1
                                                                                     r
                                                                                     2)
                                                                                    (("1"
                                                                                      (mult-by
                                                                                       -1
                                                                                       "sq(D)")
                                                                                      (("1"
                                                                                        (replaces
                                                                                         -1
                                                                                         :dir
                                                                                         rl)
                                                                                        (("1"
                                                                                          (rewrite
                                                                                           "sq_times")
                                                                                          (("1"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (rewrite
                                                           "sq_gt")
                                                          (("1"
                                                            (mult-by
                                                             5
                                                             "D")
                                                            (("1"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (mult-by
                                                             6
                                                             "sqrt(sqv(ss)-sq(D))")
                                                            (("2"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (flatten)
                                                  (("2"
                                                    (assert)
                                                    (("2"
                                                      (neg-formula 1)
                                                      (("2"
                                                        (mult-by 2 "D")
                                                        (("2"
                                                          (mult-by
                                                           3
                                                           "sqrt(sqv(ss)-sq(D))")
                                                          (("2"
                                                            (both-sides-f
                                                             3
                                                             "sq")
                                                            (("1"
                                                              (rewrite
                                                               "sq_neg")
                                                              (("1"
                                                                (rewrite
                                                                 "sq_neg")
                                                                (("1"
                                                                  (rewrite
                                                                   "sq_times")
                                                                  (("1"
                                                                    (rewrite
                                                                     "sq_times")
                                                                    (("1"
                                                                      (rewrite
                                                                       "sq_times")
                                                                      (("1"
                                                                        (rewrite
                                                                         "sq_times")
                                                                        (("1"
                                                                          (rewrite
                                                                           "sq_times")
                                                                          (("1"
                                                                            (lemma
                                                                             "sq_eps")
                                                                            (("1"
                                                                              (inst-cp
                                                                               -1
                                                                               "pm")
                                                                              (("1"
                                                                                (inst
                                                                                 -1
                                                                                 "eps")
                                                                                (("1"
                                                                                  (replaces
                                                                                   (-1
                                                                                    -2))
                                                                                  (("1"
                                                                                    (assert)
                                                                                    (("1"
                                                                                      (mult-by
                                                                                       -1
                                                                                       "sqv(ss)")
                                                                                      (("1"
                                                                                        (lemma
                                                                                         "sq_det")
                                                                                        (("1"
                                                                                          (inst
                                                                                           -1
                                                                                           "ss"
                                                                                           "vo")
                                                                                          (("1"
                                                                                            (move-terms
                                                                                             -1
                                                                                             r
                                                                                             2)
                                                                                            (("1"
                                                                                              (mult-by
                                                                                               -1
                                                                                               "sq(D)")
                                                                                              (("1"
                                                                                                (replaces
                                                                                                 -1
                                                                                                 :dir
                                                                                                 rl)
                                                                                                (("1"
                                                                                                  (assert)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (rewrite
                                                               "sq_gt")
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (hide 2)
                                      (("2"
                                        (expand "sq" 1 1)
                                        (("2"
                                          (grind-reals)
                                          (("1"
                                            (mult-by 1 "D")
                                            (("1" (assert) nil nil))
                                            nil)
                                           ("2"
                                            (mult-by -1 "D")
                                            (("2" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (hide 2)
                                  (("2"
                                    (assert)
                                    (("2" (grind-reals) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_times_real_is_real application-judgement "real" reals nil)
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (nz_sqv_gt_0 application-judgement "posreal" vectors_2D "vectors/")
    (Q const-decl "Vect2" tangent_line nil)
    (dot_comm formula-decl nil vectors_2D "vectors/")
    (det_asym formula-decl nil det_2D "vectors/")
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (nnreal_div_posreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (both_sides_div_pos_gt1 formula-decl nil real_props nil)
    (times_div1 formula-decl nil real_props nil)
    (times_div2 formula-decl nil real_props nil)
    (both_sides_times_pos_ge1 formula-decl nil real_props nil)
    (both_sides_times_pos_le1 formula-decl nil real_props nil)
    (both_sides_times_pos_le1_imp formula-decl nil extra_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)
    (ss skolem-const-decl "Ss_vect2[D]" gs_bands_2D nil)
    (both_sides_times_pos_gt1 formula-decl nil real_props nil)
    (TRUE const-decl "bool" booleans nil)
    (id const-decl "(bijective?[T, T])" identity nil)
    (bijective? const-decl "bool" functions nil)
    (sq_eps formula-decl nil sign "reals/")
    (sq_det formula-decl nil det_2D "vectors/")
    (posreal_times_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (sq_sqrt formula-decl nil sqrt "reals/")
    (sign_sq_clos application-judgement "Sign" sign "reals/")
    (sq_times formula-decl nil sq "reals/")
    (pm skolem-const-decl "Sign" gs_bands_2D nil)
    (vo skolem-const-decl "Nz_vect2" gs_bands_2D nil)
    (eps skolem-const-decl "Sign" gs_bands_2D nil)
    (sq_gt formula-decl nil sq "reals/")
    (NOT const-decl "[bool -> bool]" booleans nil)
    (both_sides_times1_imp formula-decl nil extra_real_props nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (<= const-decl "bool" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (both_sides_times_neg_le1_imp formula-decl nil extra_real_props
     nil)
    (both_sides_times_pos_lt1 formula-decl nil real_props nil)
    (neg_one_times formula-decl nil extra_tegies nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (both_sides_times_neg_gt1 formula-decl nil real_props nil)
    (nonpos_real nonempty-type-eq-decl nil real_types nil)
    (negreal nonempty-type-eq-decl nil real_types nil)
    (sq_neg formula-decl nil sq "reals/")
    (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
     nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
     "vect_analysis/")
    (posreal_div_posreal_is_posreal application-judgement "posreal"
     real_types nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "real" vectors_2D "vectors/")
    (det const-decl "real" det_2D "vectors/")
    (det_perpR formula-decl nil det_2D "vectors/")
    (dot_scal_left formula-decl nil vectors_2D "vectors/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (nz_nzv application-judgement "Nz_vector" vectors_2D "vectors/")
    (perpR_nz application-judgement "Nz_vect2" perpendicular_2D
     "vectors/")
    (perpR const-decl "Vect2" perpendicular_2D "vectors/")
    (beta const-decl "nnreal" tangent_line nil)
    (Sign type-eq-decl nil sign "reals/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (nzint nonempty-type-eq-decl nil integers nil)
    (int nonempty-type-eq-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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (alpha const-decl "{x: posreal | x < 1}" tangent_line nil)
    (< const-decl "bool" reals nil)
    (Ss_vect2 type-eq-decl nil horizontal nil)
    (D formal-const-decl "posreal" gs_bands_2D nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (nnreal 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)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (* const-decl "Vector" vectors_2D "vectors/")
    (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)
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (zero const-decl "Vector" vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (dot_add_left formula-decl nil vectors_2D "vectors/"))
   nil))
 (gs_green_band 0
  (gs_green_band-3 nil 3476539853
   ("" (skeep)
    (("" (rewrite "cd2d" :dir rl)
      (("" (split)
        (("1" (flatten)
          (("1" (case "sqv(s)>=sq(D) AND two_parallel?(s,vo,vi)")
            (("1" (flatten)
              (("1" (lemma "gs_green_two_parallel")
                (("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
              nil)
             ("2" (expand "gs_green?")
              (("2" (skolem 3 "gs1")
                (("2" (rewrite "omega_v2_conflict" :dir rl)
                  (("2" (rewrite "omega_v2_conflict" :dir rl)
                    (("2" (lemma "IntermediateValue")
                      (("2" (assert)
                        (("2" (inst -1 "band" "Omega_gs(s,vo,vi)")
                          (("2" (assert)
                            (("2" (split -1)
                              (("1"
                                (inst -1 "gso" "gs1")
                                (("1"
                                  (expand "Omega_gs")
                                  (("1"
                                    (expand "o")
                                    (("1" (mult-cases -1) nil nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (skolem 1 "x")
                                (("2"
                                  (lemma "Omega_gs_critical")
                                  (("2"
                                    (inst -1 "x" "s" "vi" "vo")
                                    (("2"
                                      (assert)
                                      (("2"
                                        (expand "gs_band?")
                                        (("2"
                                          (inst -3 "x")
                                          (("2"
                                            (replace 2)
                                            (("2" (propax) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (flatten)
          (("2" (expand "gs_green?") (("2" (inst? -1) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((cd2d formula-decl nil cd2d nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (Vgs const-decl "Vect2" gs_bands_2D nil)
    (set type-eq-decl nil sets nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (Connected type-eq-decl nil connected_set "reals/")
    (ConnectedGt type-eq-decl nil connected_set "reals/")
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (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)
    (D formal-const-decl "posreal" gs_bands_2D nil)
    (nnreal type-eq-decl nil real_types nil)
    (B formal-const-decl "nnreal" gs_bands_2D nil)
    (T formal-const-decl "{AB: posreal | AB > B}" gs_bands_2D nil)
    (Vgs_continuous application-judgement "continuous_rv_fun"
     gs_bands_2D nil)
    (gs_green? const-decl "bool" gs_bands_2D nil)
    (omega_v2_conflict formula-decl nil omega_v2 nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (IntermediateValue formula-decl nil interm_value_thm "analysis/")
    (Omega_gs const-decl "({f | continuous?(f)})" gs_bands_2D nil)
    (continuous? const-decl "bool" continuous_functions "analysis/")
    (pos_times_gt formula-decl nil real_props nil)
    (omega_v2 const-decl "real" omega_v2 nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (O const-decl "[T -> real]" vect2_cont_comp "vect_analysis/")
    (Omega_gs_critical formula-decl nil gs_bands_2D nil)
    (gs_band? const-decl "bool" gs_bands_2D nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
     "vect_analysis/")
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (gs_green_two_parallel formula-decl nil gs_bands_2D nil)
    (two_parallel? const-decl "bool" gs_line nil)
    (Sp_vect2 type-eq-decl nil horizontal nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (sqv const-decl "nnreal" vectors_2D "vectors/"))
   nil)
  (gs_green_band-2 nil 3443226487
   ("" (skeep)
    (("" (rewrite "cd2d" :dir rl)
      (("" (split)
        (("1" (flatten)
          (("1" (lemma "gs_green_two_parallel")
            (("1" (inst?)
              (("1" (assert)
                (("1" (expand "gs_green?")
                  (("1" (skolem 3 "gs1")
                    (("1" (rewrite "omega_vv_conflict" :dir rl)
                      (("1" (rewrite "omega_vv_conflict" :dir rl)
                        (("1" (lemma "IntermediateValue")
                          (("1" (inst -1 "band" "Omega_gs(sp,vo,vi)")
                            (("1" (assert)
                              (("1"
                                (split -1)
                                (("1"
                                  (inst -1 "gso" "gs1")
                                  (("1"
                                    (expand "Omega_gs")
                                    (("1"
                                      (expand "o")
                                      (("1" (mult-cases -1) nil nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (skolem 1 "x")
                                  (("2"
                                    (lemma "Omega_gs_critical")
                                    (("2"
                                      (inst -1 "x" "sp" "vi" "vo")
                                      (("2"
                                        (assert)
                                        (("2"
                                          (expand "gs_band?")
                                          (("2" (inst -3 "x") nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (flatten)
          (("2" (expand "gs_green?") (("2" (inst? -1) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((cd2d formula-decl nil cd2d nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (sq const-decl "nonneg_real" sq "reals/")
    (Sp_vect2 type-eq-decl nil horizontal nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (Connected type-eq-decl nil connected_set "reals/")
    (ConnectedGt type-eq-decl nil connected_set "reals/")
    (IntermediateValue formula-decl nil interm_value_thm "analysis/")
    (O const-decl "[T -> real]" vect2_cont_comp "vect_analysis/"))
   nil)
  (gs_green_band-1 nil 3443196394
   ("" (skeep)
    (("" (lemma "gs_green_two_parallel")
      (("" (inst?)
        (("" (assert)
          (("" (expand "gs_green?")
            (("" (skolem 2 "cc")
              (("" (flatten)
                (("" (case "cc < c")
                  (("1" (lemma "interm_value2")
                    (("1" (inst -1 "cc" "c" "0")
                      (("1" (assert)
                        (("1"
                          (inst -1
                           "LAMBDA (x:closed_interval(cc,c)): omega(ss,vo,vi)(x)")
                          (("1" (assert)
                            (("1" (split -1)
                              (("1"
                                (skeep -1 :preds? t)
                                (("1"
                                  (lemma "Omega_gs_critical")
                                  (("1"
                                    (inst -1 "c_1" "ss" "vi" "vo")
                                    (("1"
                                      (split -1)
                                      (("1"
                                        (expand "gs_band?")
                                        (("1"
                                          (inst -9 "c_1")
                                          (("1" (assert) nil nil))
                                          nil))
                                        nil)
                                       ("2"
                                        (expand "omega" -3)
                                        (("2" (propax) nil nil))
                                        nil)
                                       ("3" (propax) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2"
                                (lemma "omega_continuous")
                                (("2"
                                  (inst? -1)
                                  (("2"
                                    (lemma "cont_intv")
                                    (("2"
                                      (inst
                                       -1
                                       "cc"
                                       "c"
                                       "omega(ss,vo,vi)")
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (case "c < cc")
                    (("1" (lemma "interm_value4")
                      (("1" (inst -1 "c" "cc" "0")
                        (("1" (assert)
                          (("1"
                            (inst -1
                             "LAMBDA (x:closed_interval(c,cc)): omega(ss,vo,vi)(x)")
                            (("1" (assert)
                              (("1"
                                (split -1)
                                (("1"
                                  (skeep -1 :preds? t)
                                  (("1"
                                    (lemma "Omega_gs_critical")
                                    (("1"
                                      (inst -1 "c_1" "ss" "vi" "vo")
                                      (("1"
                                        (split -1)
                                        (("1"
                                          (expand "gs_band?")
                                          (("1"
                                            (inst -9 "c_1")
                                            (("1" (assert) nil nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (expand "omega" -3)
                                          (("2" (propax) nil nil))
                                          nil)
                                         ("3" (propax) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (lemma "omega_continuous")
                                  (("2"
                                    (inst? -1)
                                    (("2"
                                      (lemma "cont_intv")
                                      (("2"
                                        (inst
                                         -1
                                         "c"
                                         "cc"
                                         "omega(ss,vo,vi)")
                                        (("2" (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)
   ((cont_intv formula-decl nil interm_value_thm "analysis/")
    (interm_value2 formula-decl nil interm_value_thm "analysis/")
    (interm_value4 formula-decl nil interm_value_thm "analysis/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Ss_vect2 type-eq-decl nil horizontal nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/"))
   shostak))
 (gs_red_band 0
  (gs_red_band-3 nil 3476539870
   ("" (skeep)
    (("" (rewrite "cd2d" :dir rl)
      (("" (split)
        (("1" (flatten)
          (("1" (case "sqv(s)>=sq(D) AND two_parallel?(s,vo,vi)")
            (("1" (flatten)
              (("1" (lemma "gs_green_two_parallel")
                (("1" (inst - "band" "s" "vi" "vo")
                  (("1" (assert)
                    (("1" (expand "gs_green?")
                      (("1" (inst -1 "gso") nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (expand "gs_red?")
              (("2" (skolem 2 "gs1")
                (("2" (rewrite "omega_v2_conflict" :dir rl)
                  (("2" (rewrite "omega_v2_conflict" :dir rl)
                    (("2" (lemma "IntermediateValue")
                      (("2" (inst -1 "band" "Omega_gs(s,vo,vi)")
                        (("2" (assert)
                          (("2" (split -1)
                            (("1" (inst -1 "gso" "gs1")
                              (("1"
                                (expand "Omega_gs")
                                (("1"
                                  (expand "o")
                                  (("1" (mult-cases -1) nil nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (skolem 1 "x")
                              (("2"
                                (lemma "Omega_gs_critical")
                                (("2"
                                  (inst -1 "x" "s" "vi" "vo")
                                  (("2"
                                    (assert)
                                    (("2"
                                      (expand "gs_band?")
                                      (("2"
                                        (inst -3 "x")
                                        (("2"
                                          (replace 2)
                                          (("2" (propax) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (flatten)
          (("2" (expand "gs_red?") (("2" (inst?) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((cd2d formula-decl nil cd2d nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (/= const-decl "boolean" notequal nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (Vgs const-decl "Vect2" gs_bands_2D nil)
    (set type-eq-decl nil sets nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (Connected type-eq-decl nil connected_set "reals/")
    (ConnectedGt type-eq-decl nil connected_set "reals/")
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (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)
    (D formal-const-decl "posreal" gs_bands_2D nil)
    (nnreal type-eq-decl nil real_types nil)
    (B formal-const-decl "nnreal" gs_bands_2D nil)
    (T formal-const-decl "{AB: posreal | AB > B}" gs_bands_2D nil)
    (Vgs_continuous application-judgement "continuous_rv_fun"
     gs_bands_2D nil)
    (gs_red? const-decl "bool" gs_bands_2D nil)
    (omega_v2_conflict formula-decl nil omega_v2 nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (IntermediateValue formula-decl nil interm_value_thm "analysis/")
    (gs_band? const-decl "bool" gs_bands_2D nil)
    (Omega_gs_critical formula-decl nil gs_bands_2D nil)
    (O const-decl "[T -> real]" vect2_cont_comp "vect_analysis/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (omega_v2 const-decl "real" omega_v2 nil)
    (pos_times_gt formula-decl nil real_props nil)
    (continuous? const-decl "bool" continuous_functions "analysis/")
    (Omega_gs const-decl "({f | continuous?(f)})" gs_bands_2D nil)
    (gs_green? const-decl "bool" gs_bands_2D nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqv_cont name-judgement "continuous_vr_fun" vect_cont_2D
     "vect_analysis/")
    (sq_nz_pos application-judgement "posreal" sq "reals/")
    (gs_green_two_parallel formula-decl nil gs_bands_2D nil)
    (two_parallel? const-decl "bool" gs_line nil)
    (Sp_vect2 type-eq-decl nil horizontal nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (sqv const-decl "nnreal" vectors_2D "vectors/"))
   nil)
  (gs_red_band-2 nil 3443269825
   ("" (skeep)
    (("" (rewrite "cd2d" :dir rl)
      (("" (split)
        (("1" (flatten)
          (("1" (case "two_parallel?(sp,vo,vi)")
            (("1" (lemma "gs_green_two_parallel")
              (("1" (inst - "band" "sp" "vi" "vo")
                (("1" (assert)
                  (("1" (expand "gs_green?")
                    (("1" (inst -1 "gso") nil nil)) nil))
                  nil))
                nil))
              nil)
             ("2" (expand "gs_red?")
              (("2" (skolem 2 "gs1")
                (("2" (rewrite "omega_vv_conflict" :dir rl)
                  (("2" (rewrite "omega_vv_conflict" :dir rl)
                    (("2" (lemma "IntermediateValue")
                      (("2" (inst -1 "band" "Omega_gs(sp,vo,vi)")
                        (("2" (assert)
                          (("2" (split -1)
                            (("1" (inst -1 "gso" "gs1")
                              (("1"
                                (expand "Omega_gs")
                                (("1"
                                  (expand "o")
                                  (("1" (mult-cases -1) nil nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (skolem 1 "x")
                              (("2"
                                (lemma "Omega_gs_critical")
                                (("2"
                                  (inst -1 "x" "sp" "vi" "vo")
                                  (("2"
                                    (assert)
                                    (("2"
                                      (expand "gs_band?")
                                      (("2" (inst -3 "x") nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (flatten)
          (("2" (expand "gs_red?") (("2" (inst?) nil nil)) nil)) nil))
        nil))
      nil))
    nil)
   ((cd2d formula-decl nil cd2d nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (sq const-decl "nonneg_real" sq "reals/")
    (Sp_vect2 type-eq-decl nil horizontal nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/")
    (Connected type-eq-decl nil connected_set "reals/")
    (ConnectedGt type-eq-decl nil connected_set "reals/")
    (IntermediateValue formula-decl nil interm_value_thm "analysis/")
    (O const-decl "[T -> real]" vect2_cont_comp "vect_analysis/")
    (two_parallel? const-decl "bool" gs_line nil))
   nil)
  (gs_red_band-1 nil 3443210630
   ("" (skeep)
    (("" (case "NOT two_parallel?(ss,vo,vi)")
      (("1" (expand "gs_red?")
        (("1" (skolem 2 "cc")
          (("1" (flatten)
            (("1" (case "cc < c")
              (("1" (lemma "interm_value4")
                (("1" (inst -1 "cc" "c" "0")
                  (("1" (assert)
                    (("1"
                      (inst -1
                       "LAMBDA (x:closed_interval(cc,c)): Omega_gs(ss,vo,vi)(x)")
                      (("1" (assert)
                        (("1" (split -1)
                          (("1" (skeep -1 :preds? t)
                            (("1" (lemma "Omega_gs_critical")
                              (("1"
                                (inst -1 "c_1" "ss" "vi" "vo")
                                (("1"
                                  (split -1)
                                  (("1"
                                    (expand "gs_band?")
                                    (("1"
                                      (inst -8 "c_1")
                                      (("1"
                                        (assert)
                                        (("1"
                                          (typepred "ab")
                                          (("1"
                                            (inst -1 "cc" "c" "c_1")
                                            (("1" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (expand "Omega_gs" -3)
                                    (("2" (propax) nil nil))
                                    nil)
                                   ("3" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (lemma "Omega_gs_continuous")
                            (("2" (inst? -1)
                              (("2"
                                (lemma "cont_intv")
                                (("2"
                                  (inst
                                   -1
                                   "cc"
                                   "c"
                                   "Omega_gs(ss,vo,vi)")
                                  (("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (case "c < cc")
                (("1" (lemma "interm_value2")
                  (("1" (inst -1 "c" "cc" "0")
                    (("1" (assert)
                      (("1"
                        (inst -1
                         "LAMBDA (x:closed_interval(c,cc)): Omega_gs(ss,vo,vi)(x)")
                        (("1" (assert)
                          (("1" (split -1)
                            (("1" (skeep -1 :preds? t)
                              (("1"
                                (lemma "Omega_gs_critical")
                                (("1"
                                  (inst -1 "c_1" "ss" "vi" "vo")
                                  (("1"
                                    (split -1)
                                    (("1"
                                      (expand "gs_band?")
                                      (("1"
                                        (inst -8 "c_1")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (typepred "ab")
                                            (("1"
                                              (inst -1 "c" "cc" "c_1")
                                              (("1" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (expand "Omega_gs" -3)
                                      (("2" (propax) nil nil))
                                      nil)
                                     ("3" (propax) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil)
                             ("2" (lemma "Omega_gs_continuous")
                              (("2"
                                (inst? -1)
                                (("2"
                                  (lemma "cont_intv")
                                  (("2"
                                    (inst
                                     -1
                                     "c"
                                     "cc"
                                     "Omega_gs(ss,vo,vi)")
                                    (("2" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (assert) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (lemma "gs_green_two_parallel")
        (("2" (inst?)
          (("2" (inst? -1)
            (("2" (assert)
              (("2" (expand "gs_green?")
                (("2" (inst -1 "c") (("2" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((interm_value2 formula-decl nil interm_value_thm "analysis/")
    (interm_value4 formula-decl nil interm_value_thm "analysis/")
    (cont_intv formula-decl nil interm_value_thm "analysis/")
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (sqv const-decl "nnreal" vectors_2D "vectors/")
    (sq const-decl "nonneg_real" sq "reals/")
    (Ss_vect2 type-eq-decl nil horizontal nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/"))
   nil)))