Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 827


Synopsis:        (assert) crashes PVS with stack overflow
Severity:        serious
Priority:        medium
Responsible:     shankar
State:           open
Class:           sw-bug
Arrival-Date:    Wed Mar 10 10:25:01 2004
Originator:      "Ricky W. Butler"
Organization:    larc.nasa.gov
Release:         PVS 3.1
Environment: 
 System:          
 Architecture: 

Description: 
  
  --=-ssYXAsWuicxIyTo46Ebj
  Content-Type: text/plain
  Content-Transfer-Encoding: 7bit
  
  Rerunning proof of vert_in_circle_correct in theory "vert_only_prop"
  results in:
  
  
  Rerunning step: (assert)
  Error: Stack overflow (signal 1000)
    [condition type: synchronous-operating-system-signal]
  
  Restart actions (select using :continue):
   0: continue computation
   1: Return to Top Level (an "abort" restart).
   2: Abort entirely from this process.
  [1c] pvs(32): 
  
  This did not happen in PVS 2.4
  
  Rick
  
  
  
  --=-ssYXAsWuicxIyTo46Ebj
  Content-Disposition: attachment; filename=bug3.dmp
  Content-Type: text/plain; name=bug3.dmp; charset=UTF-8
  Content-Transfer-Encoding: 7bit
  
  
  %% PVS Version 3.1
  %% 6.2 [Linux (x86)] (Feb 14, 2003 18:46)
  
  
  $$$vert_only_prop.pvs
  vert_only_prop: THEORY
  BEGIN
     
  
    IMPORTING vert_only_algo, 
              common_defs, sign
  
    s   : VAR Vect3 % Relative position
    vo  : VAR Vect3 % Ownship absolute velocity
    vi  : VAR Vect3 % Intruder absolute velocity
    v   : VAR Vect3 % Relative velocity
    vv  : VAR Vect3 % Relative velocity
    ve  : VAR Vect3 % Relative escape velocity
    vr  : VAR Vect3 % Relative recovery velocity
  
    tr  : VAR posreal  % Recovery time
    te  : VAR real  % Escape time
    t   : VAR real  % time
  
    vez : VAR real     % escape velocity in vert axis
    vrz : VAR real     % recovery velocity in vert axis
  
    eps : VAR Sign
    
    m   : VAR solution
  
  
  %
  %
  % ----------------------------------------------------------------
  %              Proofs of Algorithm Components
  % ----------------------------------------------------------------
  %
  %
  
    form_vert_only : LEMMA
        member(m, form_vert_only(v, vez, vrz, tr))
      IMPLIES
        vertical_change?(v,    m`ve) AND
        vertical_change?(v,    m`vr) AND
        vertical_change?(m`ve, m`vr) AND
        s+tr*v = s+m`te*m`ve+(tr-m`te)*m`vr AND
        m`ve`z = vez AND m`vr`z = vrz
  
  
    in_circle_te_def : LEMMA
        member(m, vert_in_circle(s, v, tr))
      IMPLIES
        m`te = THETA(s, v, -1)
  
    vert_in_circle_correct : LEMMA
        hor_sep?(s) AND
        NOT pred_sep?(s,v,tr) AND
        member(m, vert_in_circle(s, v, tr))
      IMPLIES
        separation?(s, m`ve) AND
        separation?(s + m`te * m`ve, m`vr) AND 
        vertical_change?(v,    m`ve) AND
        vertical_change?(v,    m`vr) AND
        vertical_change?(m`ve, m`vr) AND
        s+tr*v = s+m`te*m`ve+(tr-m`te)*m`vr AND
        0 < m`te AND m`te < tr 
  
  END vert_only_prop
  
  $$$vert_only_prop.prf
  (vert_only_prop
   (form_vert_only 0
    (form_vert_only-1 nil 3287854939 3287917171
     ("" (skosimp*)
      (("" (auto-rewrite "restrict")
        (("" (expand "member")
          (("" (expand "form_vert_only")
            (("" (split -1)
              (("1" (flatten)
                (("1" (expand "singleton")
                  (("1" (lemma "vert_timeliness")
                    (("1" (inst?)
                      (("1"
                        (case "vertical_change?(v!1, m!1`ve) AND
                                                    vertical_change?(m!1`ve, m!
 1`vr)")
                        (("1" (flatten)
                          (("1" (assert)
                            (("1" (expand "vertical_change?")
                              (("1" (propax) nil nil)) nil))
                            nil))
                          nil)
                         ("2" (expand "vertical_change?")
                          (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (flatten)
                (("2" (expand "emptyset") (("2" (propax) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved-complete
     ((member const-decl "bool" sets nil)
      (singleton const-decl "(singleton?)" sets nil)
      (real nonempty-type-from-decl nil reals nil)
      (Vect3 type-eq-decl nil Vectors 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)
      (solution type-eq-decl nil common_defs 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)
      (vertical_change? const-decl "bool" common_defs nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (vert_timeliness formula-decl nil one_circle_vert nil)
      (emptyset const-decl "set" sets nil)
      (form_vert_only const-decl "set[solution]" vert_only_algo nil))
     3985 530 t nil))
   (in_circle_te_def_TCC1 0
    (in_circle_te_def_TCC1-1 nil 3287854939 3287917537
     ("" (subtype-tcc) nil nil) proved
     ((vert_in_circle const-decl "set[solution]" vert_only_algo nil)
      (emptyset const-decl "set" sets nil)
      (posreal nonempty-type-eq-decl nil real_types nil)
      (> const-decl "bool" reals nil)
      (nonneg_real nonempty-type-eq-decl nil real_types nil)
      (>= const-decl "bool" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (number nonempty-type-decl nil numbers nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (sq const-decl "nonneg_real" sq "reals/")
      (hor_speed_gt_0? const-decl "bool" criteria nil)
      (disc const-decl "real" common_defs nil)
      (member const-decl "bool" sets nil)
      (THETA_defined? const-decl "bool" common_defs nil))
     1357 1290 nil nil))
   (in_circle_te_def 0
    (in_circle_te_def-1 nil 3287854939 3287922485
     ("" (skosimp*)
      (("" (expand "member")
        (("" (expand "vert_in_circle")
          (("" (split)
            (("1" (flatten)
              (("1" (split)
                (("1" (flatten)
                  (("1" (expand "sign")
                    (("1" (expand "form_vert_only")
                      (("1" (split)
                        (("1" (case "THETA_defined?(s!1,v!1)")
                          (("1" (flatten)
                            (("1" (expand "singleton")
                              (("1" (replace -4)
                                (("1" (hide -4)
                                  (("1" (assert)
                                    (("1" (expand "+")
                                      (("1" (expand "*")
                                        (("1"
                                          (assert)
                                          (("1"
                                            (name
                                             "VO_REC"
                                             "(sign(s!1`z + tr!1 * v!1`z) * H -
  s!1`z - tr!1 * v!1`z) /
                                       (THETA(s!1, v!1, -1) - tr!1)")
                                            (("1"
                                              (expand "sign")
                                              (("1"
                                                (replace -1)
                                                (("1"
                                                  (mult-by
                                                   2
                                                   "((THETA(s!1, v!1, -1) * VO_
 REC - VO_REC * tr!1 + tr!1 * v!1`z) /
                                         THETA(s!1, v!1, -1)
                                         - VO_REC)")
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (real-props 2)
                            (("2" (expand "THETA_defined?")
                              (("2" (assert) nil nil)) nil))
                            nil))
                          nil)
                         ("2" (flatten)
                          (("2" (expand "emptyset") (("2" (propax) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (flatten)
                  (("2" (expand "emptyset") (("2" (propax) nil nil)) nil)) nil)
 )
                nil))
              nil)
             ("2" (flatten)
              (("2" (expand "emptyset") (("2" (propax) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((member const-decl "bool" sets nil) (sign const-decl "Sign" sign nil)
      (* const-decl "Vect3" Vectors nil)
      (THETA const-decl "real" common_defs nil)
      (clash_type type-eq-decl nil common_defs nil)
      (H const-decl "posreal" criteria nil)
      (posreal nonempty-type-eq-decl nil real_types nil)
      (> const-decl "bool" reals nil)
      (nonneg_real nonempty-type-eq-decl nil real_types nil)
      (>= const-decl "bool" reals nil)
      (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (Sign type-eq-decl nil sign nil)
      (- const-decl "[numfield -> numfield]" number_fields nil)
      (OR const-decl "[bool, bool -> bool]" booleans 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)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
      (nznum nonempty-type-eq-decl nil number_fields nil)
      (/= const-decl "boolean" notequal nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (number nonempty-type-decl nil numbers nil)
      (both_sides_times1 formula-decl nil real_props nil)
      (div_cancel2 formula-decl nil real_props nil)
      (nonzero_real nonempty-type-eq-decl nil reals nil)
      (tr!1 skolem-const-decl "posreal" vert_only_prop nil)
      (VO_REC skolem-const-decl "real" vert_only_prop nil)
      (v!1 skolem-const-decl "Vect3" vert_only_prop nil)
      (s!1 skolem-const-decl "Vect3" vert_only_prop nil)
      (+ const-decl "Vect3" Vectors nil)
      (singleton const-decl "(singleton?)" sets nil)
      (real nonempty-type-from-decl nil reals nil)
      (Vect3 type-eq-decl nil Vectors nil)
      (boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (THETA_defined? const-decl "bool" common_defs nil)
      (emptyset const-decl "set" sets nil)
      (form_vert_only const-decl "set[solution]" vert_only_algo nil)
      (vert_in_circle const-decl "set[solution]" vert_only_algo nil))
     139387 9900 t nil))
   (out_circle_te_def_TCC1 0
    (out_circle_te_def_TCC1-1 nil 3287854939 nil ("" (subtype-tcc) nil nil)
     unchecked nil nil nil nil nil))
   (out_circle_te_def 0
    (out_circle_te_def-1 nil 3287854939 nil
     ("" (skosimp*)
      (("" (expand "member")
        (("" (expand "vert_out_circle")
          (("" (split)
            (("1" (flatten)
              (("1" (split)
                (("1" (flatten)
                  (("1" (expand "form_vert_only")
                    (("1" (split)
                      (("1" (case "THETA_defined?(s!1,v!1)")
                        (("1" (flatten)
                          (("1" (expand "singleton")
                            (("1" (replace -4)
                              (("1" (hide -4)
                                (("1" (assert)
                                  (("1"
                                    (name-replace "VO_ESC"
                                     " (-sign(v!1`z) * H - s!1`z) / THETA(s!1, 
 v!1, 1)")
                                    (("1"
                                      (mult-by 2 "(VO_ESC -
                     (tr!1 * v!1`z - THETA(s!1, v!1, 1) * VO_ESC) /
                      (tr!1 - THETA(s!1, v!1, 1)))")
                                      (("1" (field 2) nil nil)) nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (hide -1)
                          (("2" (expand "THETA_defined?")
                            (("2" (assert) nil nil)) nil))
                          nil))
                        nil)
                       ("2" (flatten)
                        (("2" (expand "emptyset") (("2" (propax) nil nil)) nil)
 )
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (flatten)
                  (("2" (expand "emptyset") (("2" (propax) nil nil)) nil)) nil)
 )
                nil))
              nil)
             ("2" (flatten)
              (("2" (expand "emptyset") (("2" (propax) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil)
     unchecked nil nil nil nil nil))
   (vert_in_circle_correct 0
    (vert_in_circle_correct-1 nil 3287854939 nil
     ("" (skosimp*)
      (("" (lemma "in_circle_te_def")
        (("" (inst?)
          (("" (assert)
            (("" (replace -1)
              (("" (expand "member")
                (("" (expand "vert_in_circle")
                  (("" (split)
                    (("1" (flatten)
                      (("1" (split)
                        (("1" (flatten)
                          (("1" (lemma "form_vert_only")
                            (("1" (inst?)
                              (("1" (inst?)
                                (("1" (inst - "s!1")
                                  (("1" (split -1)
                                    (("1" (flatten)
                                      (("1" (assert)
                                        (("1"
                                          (lemma "vert_in_circle")
                                          (("1"
                                            (inst?)
                                            (("1"
                                              (inst?)
                                              (("1"
                                                (inst - "s!1+tr!1*v!1")
                                                (("1"
                                                  (replace -14)
                                                  (("1"
                                                    (expand "vertical_change?")
                                                    (("1"
                                                      (flatten)
                                                      (("1" (assert) nil nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (expand "THETA_defined?")
                                              (("2" (propax) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2" (expand "member")
                                      (("2" (propax) nil nil)) nil))
                                    nil))
                                  nil))
                                nil)
                               ("2" (assert) nil nil) ("3" (assert) nil nil)
                               ("4" (expand "THETA_defined?")
                                (("4" (assert) nil nil)) nil))
                              nil))
                            nil))
                          nil)
                         ("2" (flatten)
                          (("2" (expand "emptyset") (("2" (propax) nil nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (flatten)
                      (("2" (expand "emptyset") (("2" (propax) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     unchecked nil nil nil nil nil))
   (vert_out_circle_correct 0
    (vert_out_circle_correct-1 nil 3287854939 nil
     ("" (skosimp*)
      (("" (lemma "out_circle_te_def")
        (("" (inst?)
          (("" (assert)
            (("" (replace -1)
              (("" (expand "member")
                (("" (expand "vert_out_circle")
                  (("" (split)
                    (("1" (flatten)
                      (("1" (split)
                        (("1" (flatten)
                          (("1" (lemma "form_vert_only")
                            (("1" (inst?)
                              (("1" (inst?)
                                (("1" (inst - "s!1")
                                  (("1" (split -1)
                                    (("1" (flatten)
                                      (("1" (assert)
                                        (("1"
                                          (lemma "vert_out_circle")
                                          (("1"
                                            (inst?)
                                            (("1"
                                              (inst?)
                                              (("1"
                                                (inst - "m!1`vr")
                                                (("1"
                                                  (replace -14)
                                                  (("1"
                                                    (expand "vertical_change?")
                                                    (("1"
                                                      (flatten)
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (expand "at")
                                                          (("1"
                                                            (propax)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (expand "THETA_defined?")
                                              (("2" (propax) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2" (expand "member")
                                      (("2" (propax) nil nil)) nil))
                                    nil))
                                  nil))
                                nil)
                               ("2" (assert) nil nil) ("3" (assert) nil nil)
                               ("4" (expand "THETA_defined?")
                                (("4" (assert) nil nil)) nil))
                              nil))
                            nil))
                          nil)
                         ("2" (flatten)
                          (("2" (expand "emptyset") (("2" (propax) nil nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (flatten)
                      (("2" (expand "emptyset") (("2" (propax) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     unchecked nil nil nil nil nil))
   (vert_one_circle_correct 0
    (vert_one_circle_correct-1 nil 3287854939 nil
     ("" (skosimp*)
      (("" (expand "member")
        (("" (expand "vert_one_circle")
          (("" (split)
            (("1" (flatten)
              (("1" (split)
                (("1" (flatten)
                  (("1" (lemma "form_vert_only")
                    (("1" (inst?)
                      (("1" (inst?)
                        (("1" (expand "member")
                          (("1" (assert)
                            (("1" (lemma "vert_one_circle")
                              (("1" (inst?)
                                (("1" (inst?)
                                  (("1" (expand "vertical_change?")
                                    (("1" (flatten)
                                      (("1" (assert)
                                        (("1"
                                          (expand "form_vert_only")
                                          (("1"
                                            (split -15)
                                            (("1"
                                              (flatten)
                                              (("1"
                                                (assert)
                                                (("1"
                                                  (expand "singleton")
                                                  (("1"
                                                    (replace -3 -4)
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (flatten)
                                                        (("1" (assert) nil nil)
 )
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (flatten)
                                              (("2"
                                                (expand "emptyset")
                                                (("2" (propax) nil nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (assert) nil nil) ("3" (assert) nil nil)
                         ("4" (expand "THETA_defined?") (("4" (assert) nil nil)
 )
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (flatten)
                  (("2" (expand "emptyset") (("2" (propax) nil nil)) nil)) nil)
 )
                nil))
              nil)
             ("2" (flatten)
              (("2" (expand "emptyset") (("2" (propax) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil)
     unchecked nil nil nil nil nil))
   (vert_only_algo_correct_alt 0
    (vert_only_algo_correct_alt-1 nil 3287854939 nil
     ("" (skosimp*)
      (("" (lemma "vert_in_circle_correct")
        (("" (inst?)
          (("" (lemma "vert_out_circle_correct")
            (("" (inst?)
              (("" (lemma "vert_one_circle_correct")
                (("" (inst?)
                  (("" (inst - "1")
                    (("" (lemma "vert_one_circle_correct")
                      (("" (inst - "-1" "_" "_" "_" "_")
                        (("" (inst?)
                          (("" (expand "vertical_change?")
                            (("" (assert)
                              (("" (expand "member")
                                (("" (expand "vert_only_algo")
                                  (("" (expand "union")
                                    (("" (expand "member")
                                      (("" (split -6)
                                        (("1"
                                          (assert)
                                          (("1"
                                            (flatten)
                                            (("1" (assert) nil nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (assert)
                                          (("2"
                                            (flatten)
                                            (("2" (assert) nil nil))
                                            nil))
                                          nil)
                                         ("3"
                                          (assert)
                                          (("3"
                                            (flatten)
                                            (("3" (assert) nil nil))
                                            nil))
                                          nil)
                                         ("4"
                                          (assert)
                                          (("4"
                                            (flatten)
                                            (("4" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     unchecked nil nil nil nil nil))
   (vert_only_algo_correct 0
    (vert_only_algo_correct-1 nil 3287854939 nil
     ("" (skosimp*)
      (("" (lemma "vert_only_algo_correct_alt")
        (("" (inst?)
          (("" (assert)
            (("" (flatten)
              (("" (assert)
                (("" (lemma "sep_connection")
                  (("" (inst - "s!1" "m!1`te" "m!1`ve")
                    (("" (assert)
                      (("" (lemma "sep_connection")
                        (("" (inst - "s!1+m!1`te*m!1`ve" "tr!1-m!1`te" "m!1`vr"
 )
                          (("" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     unchecked nil nil nil nil nil)))
  
  
  $$$sign.pvs
  sign : THEORY
  BEGIN
  
    Sign : TYPE = {i:int|i=1 OR i=-1}
  
    x, y: VAR real
  
    sign(x): Sign = IF x > 0 THEN 1 ELSE -1 ENDIF
  
    abs_plus: LEMMA
      x*y >= 0 IMPLIES abs(x+y) = abs(x) + abs(y)
  
    sign_times: LEMMA
      x*y /= 0 IMPLIES sign(x*y) = sign(x)*sign(y)
  
  END sign
  
  $$$sign.prf
  (|sign|
   (|abs_plus| "" (SKOSIMP*)
    (("" (EXPAND "abs")
      (("" (REWRITE "pos_times_ge" -1)
        (("" (PROP)
          (("1" (ASSERT)
            (("1" (CASE "x!1 = 0 OR y!1 = 0")
              (("1" (SPLIT -)
                (("1" (REPLACE*) (("1" (ASSERT) NIL NIL)) NIL)
                 ("2" (REPLACE*) (("2" (ASSERT) NIL NIL)) NIL))
                NIL)
               ("2" (FLATTEN) (("2" (ASSERT) NIL NIL)) NIL))
              NIL))
            NIL)
           ("2" (ASSERT) NIL NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|sign_times| "" (SKOSIMP*)
    (("" (EXPAND "sign")
      (("" (CASE "x!1 * y!1 > 0")
        (("1" (ASSERT)
          (("1" (REWRITE "pos_times_gt" -1)
            (("1" (PROP) (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL))
              NIL))
            NIL))
          NIL)
         ("2" (ASSERT)
          (("2" (REWRITE "pos_times_gt" 1)
            (("2" (PROP)
              (("1" (ASSERT) NIL NIL) ("2" (ASSERT) NIL NIL)
               ("3" (ASSERT) NIL NIL) ("4" (ASSERT) NIL NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  
  
  $$$Vectors.pvs
  Vectors : THEORY
  BEGIN
    x,y,z : VAR real
  
    Vect3 : TYPE = [#
      x,y,z:real
    #]
  
    vect3 : VAR Vect3
  
  %  Vect2 : TYPE = [#
  %    x,y:real
  %  #]
  
  %  vect2 : VAR Vect2
  
  %  toVect3(vect2) : Vect3 = (#
  %    x := vect2`x,
  %    y := vect2`y,
  %    z := 0
  %  #)
  
  %  toVect2(vect3) : Vect2 = (#
  %    x := vect3`x,
  %    y := vect3`y
  %  #)
  
  %  CONVERSION toVect3
  %  CONVERSION toVect2
    
    v,w : VAR Vect3
    a,b   : VAR real
  
    -(v): Vect3=(# x := -v`x, y := -v`y, z := -v`z #) ;
  
    +(v,w):Vect3=(#
      x:= v`x + w`x,
      y:= v`y + w`y,
      z:= v`z + w`z
    #);
  
  
    -(v,w):Vect3=(#
      x:= v`x - w`x,
      y:= v`y - w`y,
      z:= v`z - w`z
    #);
  
    *(v,w):real =  v`x * w`x + v`y * w`y + v`z * w`z;
  
    *(a,w):Vect3=(#
      x:= a * w`x,
      y:= a * w`y,
      z:= a * w`z
    #)
  
    sq_norm(v):real = v*v
    sq_norm2(v):real = v`x*v`x + v`y*v`y
  
    vect_dist    : LEMMA a*(v+w) = a*v + a*w
  
    vect_dist_sub: LEMMA a*(v-w) = a*v - a*w
  
    vect_split_add: LEMMA (a+b)*v = a*v + b*v
  
    vect_split_sub: LEMMA (a-b)*v = a*v - b*v
  
    
  
  END Vectors
  
  $$$Vectors.prf
  (|Vectors| (|vect_dist| "" (GRIND) NIL NIL)
   (|vect_dist_sub| "" (GRIND) NIL NIL) (|vect_split_add| "" (GRIND) NIL NIL)
   (|vect_split_sub| "" (GRIND) NIL NIL))
  
  
  $$$sqrt_exists.pvs
  sqrt_exists: THEORY
  %----------------------------------------------------------------------------
 ----
  %
  %   This theory provides a non-constructive proof of the existence of the
  %   square root function.  The proof has been adapted from Rosenlicht's
  %   Introduction to Analysis.
  %
  %----------------------------------------------------------------------------
 ----
  
  
  BEGIN
    
    e: VAR posreal
    x, y: VAR real
    nnx, nny: VAR nonneg_real
    i: var posnat
    
    epsilon_delta: LEMMA (FORALL e: abs(x - y) < e) => x = y
  
    expt_0       : LEMMA 0^i = 0
  
    lt1_expt_le  : LEMMA nnx < 1 => nnx^i <= nnx
  
    sqrt_exists  : LEMMA
                     EXISTS (x1: [nnx: nonneg_real -> {nny | nny*nny = nnx}]): 
 TRUE
  
  END sqrt_exists
  
  
  
  $$$sqrt_exists.prf
  (|sqrt_exists|
   (|epsilon_delta| "" (SKOSIMP*)
    (("" (INST - "abs(x!1-y!1)/2")
      (("1" (ASSERT) NIL NIL)
       ("2" (EXPAND "abs") (("2" (LIFT-IF) (("2" (GROUND) NIL NIL)) NIL)) NIL))
      NIL))
    NIL)
   (|expt_0| "" (TCC) NIL NIL) (|lt1_expt_le_TCC1| "" (TCC :DEFS !) NIL NIL)
   (|lt1_expt_le| "" (INDUCT "i" 1 "above_induction[0]")
    (("1" (ASSERT)
      (("1" (SKOSIMP*)
        (("1" (EXPAND "^")
          (("1" (EXPAND "expt")
            (("1" (EXPAND "expt") (("1" (ASSERT) NIL NIL)) NIL)) NIL))
          NIL))
        NIL))
      NIL)
     ("2" (SKOSIMP*)
      (("2" (REWRITE "expt_plus")
        (("1" (REWRITE "expt_x1")
          (("1" (ASSERT)
            (("1" (INST?)
              (("1" (ASSERT)
                (("1" (LEMMA "le_times_le_pos")
                  (("1" (LEMMA "expt_pos")
                    (("1" (INST?)
                      (("1" (INST - "nnx!1^ja!1" "nnx!1" "1" "nnx!1")
                        (("1" (ASSERT) NIL NIL)) NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL)
         ("2" (CASE-REPLACE "nnx!1 = 0")
          (("1" (REWRITE "expt_0") (("1" (ASSERT) NIL NIL)) NIL)
           ("2" (ASSERT) NIL NIL))
          NIL))
        NIL))
      NIL)
     ("3" (SKOSIMP*) (("3" (ASSERT) (("3" (GROUND) NIL NIL)) NIL)) NIL))
    NIL)
   (|sqrt_exists| "" (INST + "lambda nnx: choose({nny|nny*nny=nnx})")
    (("" (SKOSIMP*)
      (("" (REWRITE "nonempty_exists")
        (("" (LEMMA "real_complete")
          (("" (INST - "{nny|nny*nny<=nnx!1}")
            (("1" (PROP)
              (("1" (EXPAND "least_upper_bound?")
                (("1" (SKOSIMP*)
                  (("1" (INST + "y!1")
                    (("1" (EXPAND "upper_bound?")
                      (("1" (ASSERT)
                        (("1" (INST-CP - 0)
                          (("1" (ASSERT)
                            (("1"
                              (CASE "forall (e:posreal|e<y!1): abs(y!1*y!1-nnx!
 1)< 4 * y!1 * e")
                              (("1" (REWRITE "epsilon_delta")
                                (("1" (SKOSIMP*)
                                  (("1" (CASE "e!1 < (4* y!1) *y!1")
                                    (("1" (INST - "e!1/(4*y!1)")
                                      (("1" (ASSERT) NIL NIL)
                                       ("2" (LEMMA "pos_div_gt")
                                        (("2"
                                          (INST - "4*y!1" "e!1")
                                          (("1"
                                            (ASSERT)
                                            (("1"
                                              (ASSERT)
                                              (("1"
                                                (REWRITE "div_mult_pos_lt1")
                                                NIL
                                                NIL))
                                              NIL))
                                            NIL)
                                           ("2" (ASSERT) NIL NIL))
                                          NIL))
                                        NIL)
                                       ("3" (ASSERT) NIL NIL))
                                      NIL)
                                     ("2" (INST - "y!1/4")
                                      (("1" (ASSERT) NIL NIL)
                                       ("2" (ASSERT)
                                        (("2"
                                          (REWRITE "div_mult_pos_lt1")
                                          (("2"
                                            (CASE "y!1=0")
                                            (("1"
                                              (ASSERT)
                                              (("1"
                                                (REPLACE -1)
                                                (("1"
                                                  (ASSERT)
                                                  (("1"
                                                    (CASE "nnx!1<1")
                                                    (("1"
                                                      (INST - "nnx!1")
                                                      (("1" (ASSERT) NIL NIL)
                                                       ("2"
                                                        (EXPAND "extend")
                                                        (("2"
                                                          (LEMMA "lt1_expt_le")
                                                          (("2"
                                                            (INST
                                                             -1
                                                             "2"
                                                             "nnx!1")
                                                            (("2"
                                                              (EXPAND "^" -1)
                                                              (("2"
                                                                (EXPAND
                                                                 "expt"
                                                                 -1)
                                                                (("2"
                                                                  (EXPAND
                                                                   "expt"
                                                                   -1)
                                                                  (("2"
                                                                    (EXPAND
                                                                     "expt"
                                                                     -1)
                                                                    (("2"
                                                                      (ASSERT)
                                                                      NIL
                                                                      NIL))
                                                                    NIL))
                                                                  NIL))
                                                                NIL))
                                                              NIL))
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL)
                                                     ("2"
                                                      (INST - "1")
                                                      (("1" (ASSERT) NIL NIL)
                                                       ("2"
                                                        (EXPAND "extend")
                                                        (("2" (ASSERT) NIL NIL)
 )
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL)
                                             ("2" (ASSERT) NIL NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL)
                               ("2" (SKOSIMP*)
                                (("2"
                                  (CASE-REPLACE
                                   "4*y!1*e!1 = (y!1+e!1)^2 - (y!1-e!1)^2")
                                  (("1" (HIDE -1 2)
                                    (("1"
                                      (CASE "forall (x,y:real): abs(x)<y iff -y
  <x & x <y")
                                      (("1" (INST?)
                                        (("1"
                                          (REPLACE -1)
                                          (("1"
                                            (HIDE -1)
                                            (("1"
                                              (PROP)
                                              (("1"
                                                (LEMMA "lt_minus_lt1")
                                                (("1"
                                                  (INST
                                                   -
                                                   "nnx!1"
                                                   "(y!1-e!1)^2"
                                                   "y!1*y!1"
                                                   "(y!1+e!1)^2")
                                                  (("1"
                                                    (GROUND)
                                                    (("1"
                                                      (ASSERT)
                                                      (("1"
                                                        (HIDE 2)
                                                        (("1"
                                                          (CASE-REPLACE
                                                           "y!1 * y!1 = y!1^2")
                                                          (("1"
                                                            (HIDE -1)
                                                            (("1"
                                                              (REWRITE
                                                               "both_sides_expt
 _pos_le")
                                                              NIL
                                                              NIL))
                                                            NIL)
                                                           ("2"
                                                            (HIDE-ALL-BUT 1)
                                                            (("2"
                                                              (GRIND)
                                                              NIL
                                                              NIL))
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL)
                                                     ("2"
                                                      (INST - "e!1+y!1")
                                                      (("1" (ASSERT) NIL NIL)
                                                       ("2"
                                                        (EXPAND "extend")
                                                        (("2"
                                                          (HIDE -2)
                                                          (("2"
                                                            (GRIND)
                                                            NIL
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL)
                                               ("2"
                                                (REWRITE "lt_minus_lt1")
                                                (("1"
                                                  (CASE-REPLACE
                                                   "y!1 * y!1 = y!1^2")
                                                  (("1"
                                                    (REWRITE
                                                     "both_sides_expt_pos_le")
                                                    NIL
                                                    NIL)
                                                   ("2"
                                                    (HIDE-ALL-BUT 1)
                                                    (("2" (GRIND) NIL NIL))
                                                    NIL))
                                                  NIL)
                                                 ("2"
                                                  (HIDE 2)
                                                  (("2"
                                                    (INST -3 "(y!1-e!1)")
                                                    (("2"
                                                      (ASSERT)
                                                      (("2"
                                                        (SKOLEM-TYPEPRED)
                                                        (("2"
                                                          (EXPAND "extend")
                                                          (("2"
                                                            (LEMMA
                                                             "both_sides_expt_p
 os_le")
                                                            (("2"
                                                              (INST
                                                               -
                                                               "2"
                                                               "s!1"
                                                               "y!1-e!1")
                                                              (("1"
                                                                (ASSERT)
                                                                (("1"
                                                                  (EXPAND "^")
                                                                  (("1"
                                                                    (EXPAND
                                                                     "expt")
                                                                    (("1"
                                                                      (EXPAND
                                                                       "expt")
                                                                      (("1"
                                                                        (EXPAND
                                                                         "expt"
 )
                                                                        (("1"
                                                                          (ASSE
 RT)
                                                                          NIL
                                                                          NIL))
                                                                        NIL))
                                                                      NIL))
                                                                    NIL))
                                                                  NIL))
                                                                NIL)
                                                               ("2"
                                                                (GROUND)
                                                                NIL
                                                                NIL))
                                                              NIL))
                                                            NIL))
                                                          NIL))
                                                        NIL))
                                                      NIL))
                                                    NIL))
                                                  NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL)
                                       ("2" (HIDE -1 -2 -3 2)
                                        (("2" (GRIND) NIL NIL)) NIL))
                                      NIL))
                                    NIL)
                                   ("2" (HIDE -1 -2 -3 2 3)
                                    (("2" (ASSERT) (("2" (GRIND) NIL NIL)) NIL)
 )
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL)
                           ("2" (EXPAND "extend") (("2" (PROPAX) NIL NIL)) NIL)
 )
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL)
               ("2" (INST + "max(nnx!1,1)")
                (("2" (EXPAND "upper_bound?")
                  (("2" (SKOLEM-TYPEPRED)
                    (("2" (EXPAND "extend")
                      (("2" (EXPAND "max")
                        (("2" (LIFT-IF)
                          (("2" (GROUND)
                            (("1" (INST?)
                              (("1" (HIDE 1)
                                (("1" (LEMMA "ge_times_ge_pos")
                                  (("1" (INST -1 "1" "1" "s!1" "s!1")
                                    (("1" (ASSERT) NIL NIL)) NIL))
                                  NIL))
                                NIL))
                              NIL)
                             ("2" (LEMMA "le_times_le_pos")
                              (("2" (INST - "1" "nnx!1" "nnx!1" "nnx!1")
                                (("2" (ASSERT)
                                  (("2" (ASSERT)
                                    (("2" (LEMMA "both_sides_expt_pos_le")
                                      (("2" (INST - "2" "s!1" "nnx!1")
                                        (("2"
                                          (EXPAND "^" -1)
                                          (("2"
                                            (EXPAND "expt")
                                            (("2"
                                              (EXPAND "expt")
                                              (("2"
                                                (EXPAND "expt")
                                                (("2" (ASSERT) NIL NIL))
                                                NIL))
                                              NIL))
                                            NIL))
                                          NIL))
                                        NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL)
             ("2" (REWRITE "nonempty_exists")
              (("2" (INST + "0")
                (("2" (EXPAND "extend") (("2" (PROPAX) NIL NIL)) NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  
  
  $$$sq.pvs
  sq: THEORY
  BEGIN
  
    a,b,d: VAR real
    nna,nnb,nnc : VAR nonneg_real   
    nz          : VAR nzreal 
    n           : VAR nat               
  
    sq(a): nonneg_real = a*a
  
    sq_nz_pos         : JUDGEMENT sq(nz) HAS_TYPE posreal 
  
    sq_rew            : LEMMA a*a = sq(a) 
  
    sq_neg            : LEMMA sq(-a) = sq(a)
        
    sq_pos            : LEMMA sq(a) >= 0
        
    sq_plus_pos       : LEMMA sq(a)+sq(b) >= 0
        
    sq_times          : LEMMA sq(a*b) = sq(a) * sq(b)
  
    sq_plus           : LEMMA sq(a+b) = sq(a) + 2*a*b + sq(b)
  
    sq_minus          : LEMMA sq(a-b) = sq(a) - 2*a*b + sq(b)
  
    sq_neg_minus      : LEMMA sq(a-b) = sq(b-a)
  
    sq_abs            : LEMMA sq(abs(a)) = sq(a)
  
    sq_abs_neg        : LEMMA sq(abs(-a)) = sq(a)
  
    sq_0              : LEMMA sq(0) = 0
  
    sq_1              : LEMMA sq(1) = 1
  
    sq_eq_0           : LEMMA sq(a) = 0 IFF a = 0
  
    sq_gt_0           : LEMMA sq(a) > 0 IFF a /= 0      
  
    sq_div            : LEMMA d /= 0 => sq(a/d) = sq(a)/sq(d)
  
    sq_plus_eq_0      : LEMMA sq(a) + sq(b) = 0 <=> (a = 0 AND b = 0)
  
    AUTO_REWRITE-     sq_neg_minus   
  
  % -------------------- Inequalities --------------------
  
    sq_ge  : LEMMA sq(nna) >= sq(nnb) IFF nna >= nnb 
  
    sq_le  : LEMMA sq(nna) <= sq(nnb) IFF nna <= nnb 
  
    sq_gt  : LEMMA sq(nna) > sq(nnb)  IFF nna > nnb
  
    sq_lt  : LEMMA sq(nna) < sq(nnb)  IFF nna < nnb 
  
    sq_eq  : LEMMA sq(nna) = sq(nnb)  IFF nna = nnb 
    
  
    sq_neg_pos_le : LEMMA sq(a) <= sq(nnc) IFF (-nnc <= a AND a <= nnc)
  
    neg_pos_sq_le : LEMMA (-b <= a AND a <= b) IMPLIES sq(a) <= sq(b)
        
    sq_neg_pos_lt : LEMMA  sq(a) < sq(nnc) IFF (-nnc < a AND a < nnc) 
  
    neg_pos_sq_lt : LEMMA (-b < a AND a < b) IMPLIES sq(a) < sq(b)
  
    sq_le_abs     : LEMMA sq(a) <= sq(b) IFF abs(a) <= abs(b)
        
    sq_lt_abs     : LEMMA sq(a) < sq(b) IFF abs(a) < abs(b)
  
    sq_ge_abs     : LEMMA sq(a) >= sq(b) IFF abs(a) >= abs(b)
        
    sq_gt_abs     : LEMMA sq(a) > sq(b) IFF abs(a) > abs(b)
  
    sq_eq_abs     : LEMMA sq(a) = sq(b) IFF abs(a) = abs(b)
  
  
    %   |\
    %   | \ C <= c
    % A |  \
    %   +----
    %    B 
  
    triangle_rectangle: LEMMA sq(a)+sq(b) <= sq(nnc) IMPLIES
                                -nnc <= a AND a <= nnc AND 
                                -nnc <= b AND b <= nnc   
  
    triangle_ineq_lt  : LEMMA sq(a) + sq(b) < sq(d) IMPLIES  
                                    abs(a) < abs(d) AND
                                    abs(b) < abs(d)   
  
  
    triangle_ineq_le  : LEMMA sq(a) + sq(b) <= sq(d) IMPLIES 
                                    abs(a) <= abs(d) AND
                                    abs(b) <= abs(d)   
  
  
  
    AUTO_REWRITE+ sq_0
    AUTO_REWRITE+ sq_1
    AUTO_REWRITE+ sq_abs
    AUTO_REWRITE+ sq_abs_neg 
  
  
  END sq
  
  
  
  
  $$$sq.prf
  (sq
   (sq_TCC1 0
    (sq_TCC1-1 nil 3255279994 nil ("" (ground) nil nil) proved-complete nil nil
     nil nil nil))
   (sq_nz_pos 0
    (sq_nz_pos-1 nil 3255279994 nil ("" (subtype-tcc) nil nil) proved-complete
     ((boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (/= const-decl "boolean" notequal 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)
      (nzreal nonempty-type-eq-decl nil reals nil)
      (sq const-decl "nonneg_real" sq nil))
     nil nil nil nil))
   (sq_rew 0
    (sq_rew-1 nil 3255279994 3255280142 ("" (grind) nil nil) unchecked
     ((sq const-decl "nonneg_real" sq nil)) 14 20 nil nil))
   (sq_neg 0
    (sq_neg-1 nil 3255279994 3255280142 ("" (grind) nil nil) unchecked
     ((sq const-decl "nonneg_real" sq nil)) 23 30 nil nil))
   (sq_pos 0
    (sq_pos-1 nil 3255279994 3255280142 ("" (grind) nil nil) unchecked
     ((sq const-decl "nonneg_real" sq nil)) 13 20 nil nil))
   (sq_plus_pos 0
    (sq_plus_pos-1 nil 3255279994 3255280142
     ("" (skolem 1 ("a" "b"))
      (("" (case "sq(a)>=0" "sq(b) >= 0")
        (("1" (ground) nil nil) ("2" (rewrite "sq_pos") nil nil)
         ("3" (rewrite "sq_pos") nil nil))
        nil))
      nil)
     unchecked
     ((sq const-decl "nonneg_real" sq nil)
      (nonneg_real nonempty-type-eq-decl nil real_types nil)
      (>= const-decl "bool" reals nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (sq_pos formula-decl nil sq nil))
     121 120 nil nil))
   (sq_times 0
    (sq_times-1 nil 3255279994 3255280142 ("" (grind) nil nil) unchecked
     ((sq const-decl "nonneg_real" sq nil)) 60 60 nil nil))
   (sq_plus 0
    (sq_plus-1 nil 3255279994 3255280142 ("" (grind) nil nil) unchecked
     ((sq const-decl "nonneg_real" sq nil)) 272 230 nil nil))
   (sq_minus 0
    (sq_minus-1 nil 3255279994 3255280142 ("" (grind) nil nil) unchecked
     ((sq const-decl "nonneg_real" sq nil)) 232 230 nil nil))
   (sq_neg_minus 0
    (sq_neg_minus-1 nil 3255279994 3255280143 ("" (grind) nil nil) unchecked
     ((sq const-decl "nonneg_real" sq nil)) 139 130 nil nil))
   (sq_abs 0
    (sq_abs-1 nil 3255280284 3255280287 ("" (grind) nil nil) unchecked
     ((boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil)
      (sq const-decl "nonneg_real" sq nil))
     2889 370 t shostak))
   (sq_abs_neg 0
    (sq_abs_neg-1 nil 3255280291 3255280292 ("" (grind) nil nil) unchecked
     ((boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil)
      (sq const-decl "nonneg_real" sq nil))
     1035 370 t shostak))
   (sq_0 0
    (sq_0-1 nil 3255279994 3255280143 ("" (grind) nil nil) unchecked
     ((sq const-decl "nonneg_real" sq nil)) 159 160 nil nil))
   (sq_1 0
    (sq_1-1 nil 3255279994 3255280143 ("" (grind) nil nil) unchecked
     ((sq const-decl "nonneg_real" sq nil)) 146 150 nil nil))
   (sq_eq_0 0
    (sq_eq_0-1 nil 3255279994 3255280143
     ("" (skosimp*)
      (("" (expand "sq")
        (("" (lemma "zero_times3") (("" (inst?) (("" (ground) nil nil)) nil))
          nil))
        nil))
      nil)
     unchecked
     ((sq const-decl "nonneg_real" sq 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)
      (zero_times3 formula-decl nil real_props nil))
     32 40 nil nil))
   (sq_gt_0 0
    (sq_gt_0-1 nil 3255279994 3255280143
     ("" (skosimp*)
      (("" (expand "sq")
        (("" (lemma "pos_times_gt") (("" (inst?) (("" (ground) nil nil)) nil))
          nil))
        nil))
      nil)
     unchecked
     ((sq const-decl "nonneg_real" sq 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)
      (pos_times_gt formula-decl nil real_props nil))
     164 110 nil nil))
   (sq_div_TCC1 0
    (sq_div_TCC1-1 nil 3255279994 nil
     ("" (skolem 1 "d") (("" (ground) (("" (rewrite "sq_eq_0") nil nil)) nil))
      nil)
     proved-complete
     ((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)
      (sq_eq_0 formula-decl nil sq nil))
     nil nil nil nil))
   (sq_div 0
    (sq_div-1 nil 3255279994 3255280143 ("" (grind) nil nil) unchecked
     ((/= const-decl "boolean" notequal nil)
      (sq const-decl "nonneg_real" sq nil))
     92 90 nil nil))
   (sq_plus_eq_0 0
    (sq_plus_eq_0-1 nil 3255279994 3255280143
     ("" (skolem 1 ("a" "b"))
      (("" (ground)
        (("1" (lemma "sq_pos")
          (("1" (inst -1 "b")
            (("1" (case "sq(a)>0")
              (("1" (ground) nil nil)
               ("2" (delete -)
                (("2" (expand "sq")
                  (("2" (rewrite "pos_times_gt") (("2" (ground) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (lemma "sq_pos")
          (("2" (inst -1 "a")
            (("2" (case "sq(b)>0")
              (("1" (ground) nil nil)
               ("2" (delete -)
                (("2" (expand "sq")
                  (("2" (rewrite "pos_times_gt") (("2" (ground) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("3" (grind) nil nil))
        nil))
      nil)
     unchecked
     ((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)
      (pos_times_gt formula-decl nil real_props nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (> const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
      (nonneg_real nonempty-type-eq-decl nil real_types nil)
      (sq const-decl "nonneg_real" sq nil) (sq_pos formula-decl nil sq nil))
     294 230 nil nil))
   (sq_ge 0
    (sq_ge-1 nil 3255279994 3255280144
     ("" (skosimp*)
      (("" (ground)
        (("1" (case "nna!1 < nnb!1")
          (("1" (case "sq(nna!1) < sq(nnb!1)")
            (("1" (ground) nil nil)
             ("2" (hide -2 2)
              (("2" (lemma "lt_times_lt_pos1")
                (("2" (inst -1 "nna!1" "nna!1" "nnb!1" "nnb!1")
                  (("1" (ground)
                    (("1" (expand "sq") (("1" (propax) nil nil)) nil)) nil)
                   ("2" (ground)
                    (("2" (case "nna!1=0")
                      (("1" (ground)
                        (("1" (replace -1 :hide? t)
                          (("1" (expand "sq")
                            (("1" (ground)
                              (("1" (rewrite "pos_times_lt") nil nil)) nil))
                            nil))
                          nil))
                        nil)
                       ("2" (ground) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (ground) nil nil))
          nil)
         ("2" (lemma "ge_times_ge_pos")
          (("2" (inst?)
            (("2" (inst -1 "nnb!1" "nna!1")
              (("2" (ground) (("2" (expand "sq") (("2" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     unchecked
     ((sq const-decl "nonneg_real" sq nil)
      (lt_times_lt_pos1 formula-decl nil real_props nil)
      (pos_times_lt formula-decl nil real_props nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (posreal nonempty-type-eq-decl nil real_types nil) nil
      (> const-decl "bool" reals 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) (>= const-decl "bool" reals nil)
      (nonneg_real nonempty-type-eq-decl nil real_types nil)
      (ge_times_ge_pos formula-decl nil real_props nil))
     308 280 nil nil))
   (sq_le 0
    (sq_le-1 nil 3255279994 3255280144
     ("" (lemma "sq_ge")
      (("" (skolem 1 ("nna" "nnb"))
        (("" (inst -1 "nnb" "nna") (("" (ground) nil nil)) nil)) nil))
      nil)
     unchecked
     ((nonneg_real nonempty-type-eq-decl nil real_types nil)
      (>= const-decl "bool" reals nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (sq_ge formula-decl nil sq nil))
     84 70 nil nil))
   (sq_gt 0
    (sq_gt-1 nil 3255279994 3255280144
     ("" (skosimp*)
      (("" (ground)
        (("1" (case "nna!1 <= nnb!1")
          (("1" (case "sq(nna!1) <= sq(nnb!1)")
            (("1" (ground) nil nil)
             ("2" (hide -2 2)
              (("2" (lemma "le_times_le_pos")
                (("2" (inst -1 "nna!1" "nna!1" "nnb!1" "nnb!1")
                  (("2" (ground)
                    (("2" (expand "sq") (("2" (propax) nil nil)) nil)) nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (ground) nil nil))
          nil)
         ("2" (lemma "gt_times_gt_pos1")
          (("2" (inst?)
            (("2" (inst -1 "nnb!1" "nna!1")
              (("1" (assert)
                (("1" (hide -2)
                  (("1" (expand "sq") (("1" (propax) nil nil)) nil)) nil))
                nil)
               ("2" (case-replace "nnb!1 = 0")
                (("1" (hide -1 1)
                  (("1" (expand "sq" 1 2)
                    (("1" (lemma "sq_pos")
                      (("1" (inst?)
                        (("1" (assert)
                          (("1" (lemma "sq_eq_0")
                            (("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (assert) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     unchecked
     ((sq const-decl "nonneg_real" sq nil)
      (le_times_le_pos formula-decl nil real_props nil)
      (number nonempty-type-decl nil numbers nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (<= const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
      (nonneg_real nonempty-type-eq-decl nil real_types nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (sq_eq_0 formula-decl nil sq nil) (sq_pos formula-decl nil sq nil)
      (posreal nonempty-type-eq-decl nil real_types nil)
      (> const-decl "bool" reals nil) nil
      (gt_times_gt_pos1 formula-decl nil real_props nil))
     289 270 nil nil))
   (sq_lt 0
    (sq_lt-1 nil 3255279994 3255280144
     ("" (skolem 1 ("nna" "nnb"))
      (("" (lemma "sq_gt")
        (("" (inst -1 "nnb" "nna") (("" (ground) nil nil)) nil)) nil))
      nil)
     unchecked
     ((sq_gt formula-decl nil sq nil)
      (nonneg_real nonempty-type-eq-decl nil real_types nil)
      (>= const-decl "bool" reals nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number nonempty-type-decl nil numbers nil))
     65 70 nil nil))
   (sq_eq 0
    (sq_eq-1 nil 3255279994 3255280144
     ("" (skosimp*)
      (("" (case-replace "nna!1 = 0")
        (("1" (lemma "sq_eq_0")
          (("1" (inst -1 "nnb!1")
            (("1" (expand "sq") (("1" (ground) nil nil)) nil)) nil))
          nil)
         ("2" (case-replace "nnb!1 = 0")
          (("1" (lemma "sq_eq_0")
            (("1" (inst?) (("1" (expand "sq") (("1" (propax) nil nil)) nil))
              nil))
            nil)
           ("2" (ground)
            (("2" (lemma "both_sides_expt2_aux")
              (("2" (inst -1 "2" "nna!1" "nnb!1")
                (("2" (expand "expt")
                  (("2" (expand "expt")
                    (("2" (expand "expt")
                      (("2" (expand "sq") (("2" (propax) nil nil)) nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     unchecked
     ((number nonempty-type-decl nil numbers nil)
      (boolean nonempty-type-decl nil booleans nil)
      (= const-decl "[T, T -> boolean]" equalities 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)
      (sq const-decl "nonneg_real" sq nil) (sq_eq_0 formula-decl nil sq nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (int nonempty-type-eq-decl nil integers nil)
      (nonneg_int nonempty-type-eq-decl nil integers nil)
      (> const-decl "bool" reals nil)
      (posnat nonempty-type-eq-decl nil integers nil)
      (posreal nonempty-type-eq-decl nil real_types nil)
      (expt def-decl "real" exponentiation nil)
      (both_sides_expt2_aux formula-decl nil exponentiation nil))
     239 220 nil nil))
   (sq_neg_pos_le 0
    (sq_neg_pos_le-1 nil 3255279994 3255280145
     ("" (skolem 1 ("a" "c"))
      (("" (case "a >= 0")
        (("1" (lemma "sq_le")
          (("1" (inst -1 "a" "c") (("1" (ground) nil nil)) nil)) nil)
         ("2" (lemma "sq_le")
          (("2" (inst -1 "-a" "c")
            (("1" (case-replace "sq(-a) = sq(a)")
              (("1" (hide -1) (("1" (ground) nil nil)) nil)
               ("2" (hide -1 3)
                (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
              nil)
             ("2" (assert) nil nil))
            nil))
          nil))
        nil))
      nil)
     unchecked
     ((>= const-decl "bool" reals nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number nonempty-type-decl nil numbers nil) nil
      (nonneg_real nonempty-type-eq-decl nil real_types nil)
      (sq_le formula-decl nil sq nil)
      (- const-decl "[numfield -> numfield]" number_fields nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (sq const-decl "nonneg_real" sq nil)
      (= const-decl "[T, T -> boolean]" equalities nil))
     199 180 nil nil))
   (neg_pos_sq_le 0
    (neg_pos_sq_le-1 nil 3255279994 3255280145
     ("" (skolem 1 ("a" "b"))
      (("" (ground)
        (("" (case "a > 0")
          (("1" (lemma "sq_le")
            (("1" (inst -1 "a" "b")
              (("1" (ground) nil nil) ("2" (ground) nil nil)) nil))
            nil)
           ("2" (case "-a <= b")
            (("1" (lemma "sq_le")
              (("1" (inst -1 "-a" "b")
                (("1" (ground) (("1" (rewrite "sq_neg") nil nil)) nil)
                 ("2" (ground) nil nil))
                nil))
              nil)
             ("2" (ground) nil nil))
            nil))
          nil))
        nil))
      nil)
     unchecked
     ((- const-decl "[numfield -> numfield]" number_fields nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (<= const-decl "bool" reals nil) (sq_neg formula-decl nil sq nil)
      (sq_le formula-decl nil sq nil)
      (nonneg_real nonempty-type-eq-decl nil real_types nil)
      (>= const-decl "bool" reals nil) nil
      (number nonempty-type-decl nil numbers nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (> const-decl "bool" reals nil))
     119 120 nil nil))
   (sq_neg_pos_lt 0
    (sq_neg_pos_lt-1 nil 3255279994 3255280145
     ("" (skolem 1 ("a" "c"))
      (("" (case "a >= 0")
        (("1" (lemma "sq_lt")
          (("1" (inst -1 "a" "c") (("1" (ground) nil nil)) nil)) nil)
         ("2" (lemma "sq_lt")
          (("2" (inst -1 "-a" "c")
            (("1" (case-replace "sq(-a) = sq(a)")
              (("1" (ground) nil nil)
               ("2" (hide -1 3)
                (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
              nil)
             ("2" (assert) nil nil))
            nil))
          nil))
        nil))
      nil)
     unchecked
     ((>= const-decl "bool" reals nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number nonempty-type-decl nil numbers nil) nil
      (nonneg_real nonempty-type-eq-decl nil real_types nil)
      (sq_lt formula-decl nil sq nil)
      (- const-decl "[numfield -> numfield]" number_fields nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (sq const-decl "nonneg_real" sq nil)
      (= const-decl "[T, T -> boolean]" equalities nil))
     202 190 nil nil))
   (neg_pos_sq_lt 0
    (neg_pos_sq_lt-1 nil 3255279994 3255280145
     ("" (skolem 1 ("a" "b"))
      (("" (ground)
        (("" (case "a > 0")
          (("1" (lemma "sq_lt")
            (("1" (inst -1 "a" "b")
              (("1" (ground) nil nil) ("2" (ground) nil nil)) nil))
            nil)
           ("2" (case "-a < b")
            (("1" (lemma "sq_lt")
              (("1" (inst -1 "-a" "b")
                (("1" (ground) (("1" (rewrite "sq_neg") nil nil)) nil)
                 ("2" (ground) nil nil))
                nil))
              nil)
             ("2" (ground) nil nil))
            nil))
          nil))
        nil))
      nil)
     unchecked
     ((- const-decl "[numfield -> numfield]" number_fields nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (< const-decl "bool" reals nil) (sq_neg formula-decl nil sq nil)
      (sq_lt formula-decl nil sq nil)
      (nonneg_real nonempty-type-eq-decl nil real_types nil)
      (>= const-decl "bool" reals nil) nil
      (number nonempty-type-decl nil numbers nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (> const-decl "bool" reals nil))
     138 120 nil nil))
   (sq_le_abs 0
    (sq_le_abs-1 nil 3255279994 3255280145
     ("" (skosimp*)
      (("" (case-replace "b!1 >= 0")
        (("1" (lemma "sq_neg_pos_le")
          (("1" (inst?)
            (("1" (expand "abs") (("1" (lift-if) (("1" (ground) nil nil)) nil))
              nil))
            nil))
          nil)
         ("2" (lemma "sq_neg_pos_le")
          (("2" (inst -1 "a!1" "-b!1")
            (("1" (case-replace "sq(-b!1) = sq(b!1)")
              (("1" (hide -1)
                (("1" (expand "abs")
                  (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil))
                nil)
               ("2" (hide -1 3)
                (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
              nil)
             ("2" (assert) nil nil))
            nil))
          nil))
        nil))
      nil)
     unchecked
     ((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) nil
      (nonneg_real nonempty-type-eq-decl nil real_types nil)
      (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil)
      (sq_neg_pos_le formula-decl nil sq nil)
      (- const-decl "[numfield -> numfield]" number_fields nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (sq const-decl "nonneg_real" sq nil)
      (= const-decl "[T, T -> boolean]" equalities nil))
     313 280 nil nil))
   (sq_lt_abs 0
    (sq_lt_abs-1 nil 3255279994 3255280146
     ("" (skosimp*)
      (("" (case-replace "b!1 >= 0")
        (("1" (lemma "sq_neg_pos_lt")
          (("1" (inst?)
            (("1" (expand "abs") (("1" (lift-if) (("1" (ground) nil nil)) nil))
              nil))
            nil))
          nil)
         ("2" (lemma "sq_neg_pos_lt")
          (("2" (inst -1 "a!1" "-b!1")
            (("1" (case-replace "sq(-b!1) = sq(b!1)")
              (("1" (hide -1)
                (("1" (expand "abs")
                  (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil))
                nil)
               ("2" (hide -1 3)
                (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
              nil)
             ("2" (assert) nil nil))
            nil))
          nil))
        nil))
      nil)
     unchecked
     ((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) nil
      (nonneg_real nonempty-type-eq-decl nil real_types nil)
      (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil)
      (sq_neg_pos_lt formula-decl nil sq nil)
      (- const-decl "[numfield -> numfield]" number_fields nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (sq const-decl "nonneg_real" sq nil)
      (= const-decl "[T, T -> boolean]" equalities nil))
     315 280 nil nil))
   (sq_ge_abs 0
    (sq_ge_abs-1 nil 3256039469 3256039538
     ("" (skosimp*)
      (("" (lemma "sq_le_abs")
        (("" (inst -1 "b!1" "a!1") (("" (ground) nil nil)) nil)) nil))
      nil)
     proved
     ((sq_le_abs formula-decl nil sq 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))
     67683 5900 t nil))
   (sq_gt_abs 0
    (sq_gt_abs-1 nil 3256039548 3256039562
     ("" (skosimp*)
      (("" (lemma "sq_lt_abs")
        (("" (inst -1 "b!1" "a!1") (("" (assert) (("" (ground) nil nil)) nil))
          nil))
        nil))
      nil)
     proved
     ((sq_lt_abs formula-decl nil sq 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))
     13739 1600 t shostak))
   (sq_eq_abs 0
    (sq_eq_abs-1 nil 3255279994 3255280146
     ("" (skosimp*)
      (("" (case "a!1 >= 0")
        (("1" (case "b!1 >= 0")
          (("1" (rewrite "sq_eq") (("1" (grind) nil nil)) nil)
           ("2" (case-replace "sq(b!1) = sq(-b!1)")
            (("1" (hide -1)
              (("1" (rewrite "sq_eq") (("1" (grind) nil nil)) nil)) nil)
             ("2" (hide 3) (("2" (expand "sq") (("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil)
         ("2" (case "b!1 >= 0")
          (("1" (case-replace "sq(a!1) = sq(-a!1)")
            (("1" (hide -1)
              (("1" (rewrite "sq_eq") (("1" (grind) nil nil)) nil)) nil)
             ("2" (hide 3) (("2" (expand "sq") (("2" (assert) nil nil)) nil))
              nil))
            nil)
           ("2" (case-replace "sq(a!1) = sq(-a!1)")
            (("1" (case-replace "sq(b!1) = sq(-b!1)")
              (("1" (hide -1 -2)
                (("1" (rewrite "sq_eq") (("1" (grind) nil nil)) nil)) nil)
               ("2" (hide -1 4)
                (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
              nil)
             ("2" (hide 4) (("2" (expand "sq") (("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     unchecked
     ((>= const-decl "bool" reals nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (sq const-decl "nonneg_real" sq nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (- const-decl "[numfield -> numfield]" number_fields nil)
      (sq_eq formula-decl nil sq nil)
      (nonneg_real nonempty-type-eq-decl nil real_types nil)
      (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil))
     361 330 nil nil))
   (triangle_rectangle 0
    (triangle_rectangle-1 nil 3255279994 3255280146
     ("" (skolem 1 ("a" "b" "c"))
      (("" (flatten)
        (("" (case "sq(a)>=0" "sq(b)>=0" "sq(c)>=0")
          (("1" (case "sq(a) <= sq(c)")
            (("1" (case "sq(b) <= sq(c)")
              (("1" (lemma "sq_neg_pos_le")
                (("1" (inst-cp -1 "a" "c")
                  (("1" (inst -1 "b" "c") (("1" (ground) nil nil)) nil)) nil))
                nil)
               ("2" (hide 2 -1) (("2" (ground) nil nil)) nil))
              nil)
             ("2" (hide 2 -1) (("2" (ground) nil nil)) nil))
            nil)
           ("2" (rewrite "sq_pos") nil nil) ("3" (rewrite "sq_pos") nil nil)
           ("4" (rewrite "sq_pos") nil nil))
          nil))
        nil))
      nil)
     unchecked
     ((sq_pos formula-decl nil sq nil) (<= const-decl "bool" reals nil)
      (sq_neg_pos_le formula-decl nil sq 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)
      (sq const-decl "nonneg_real" sq nil))
     214 200 nil nil))
   (triangle_ineq_lt 0
    (triangle_ineq_lt-1 nil 3255279994 3255280147
     ("" (skosimp*)
      (("" (lemma "sq_lt_abs")
        (("" (inst?)
          (("" (assert)
            (("" (lemma "sq_lt_abs")
              (("" (inst -1 "b!1" "d!1") (("" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil)
     unchecked
     ((sq_lt_abs formula-decl nil sq 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))
     179 140 nil nil))
   (triangle_ineq_le 0
    (triangle_ineq_le-1 nil 3255279994 3255280147
     ("" (skosimp*)
      (("" (lemma "sq_le_abs")
        (("" (inst?)
          (("" (assert)
            (("" (lemma "sq_le_abs")
              (("" (inst -1 "b!1" "d!1") (("" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil)
     unchecked
     ((sq_le_abs formula-decl nil sq 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))
     164 140 nil nil)))
  
  
  $$$sqrt.pvs
  sqrt: THEORY
  %------------------------------------------------------------------------
  %
  %  Square root of non-negative real
  %
  %  Supercedes older version: sqrt_ax
  %
  %------------------------------------------------------------------------
  EXPORTING ALL WITH sq
  
  BEGIN
  
    IMPORTING sq,                      % sq(a): nonneg_real = a*a
              sqrt_exists
  
     nnx, nny, nnz: VAR nonneg_real
    x,y,z,xx: VAR real
  
    sqrt(nnx): {nnz | nnz*nnz = nnx}
  
    sqrt_pos            : JUDGEMENT sqrt(px: posreal) HAS_TYPE posreal
  
  % -------------------- Special Arguments --------------------
  
    sqrt_0              : LEMMA  sqrt(0) = 0
    sqrt_1              : LEMMA  sqrt(1) = 1
    sqrt_eq_0           : LEMMA  sqrt(nnx) = 0 IMPLIES nnx = 0
  
  % -------------------- Basic Properties --------------------
  
    sqrt_lem            : LEMMA  sqrt(nny) = nnz IFF nnz * nnz = nny
                                 
    sqrt_def            : LEMMA  sqrt(nnx) * sqrt(nnx) = nnx
  
    sqrt_square         : LEMMA  sqrt(nnx * nnx) = nnx
  
    sqrt_sq             : LEMMA  x >= 0 IMPLIES sqrt(sq(x)) = x
  
    sqrt_sq_neg         : LEMMA  x < 0 IMPLIES sqrt(sq(x)) = -x
  
    sqrt_sq_abs         : LEMMA  sqrt(sq(x)) = abs(x)
  
    sq_sqrt             : LEMMA  x >= 0 IMPLIES sq(sqrt(x))=x
  
    sqrt_times          : LEMMA  sqrt(nny * nnz) = sqrt(nny) * sqrt(nnz)
  
    sqrt_div            : LEMMA  nnz /= 0 IMPLIES 
                                     sqrt(nny / nnz) = sqrt(nny) / sqrt(nnz)
  
  % --------------------- Inequalities --------------------
                                 
    sqrt_lt             : LEMMA  sqrt(nny) < sqrt(nnz) IFF nny < nnz 
  
    sqrt_le             : LEMMA  sqrt(nny) <= sqrt(nnz) IFF nny <= nnz 
  
    sqrt_gt             : LEMMA  sqrt(nny) > sqrt(nnz) IFF nny > nnz 
  
    sqrt_ge             : LEMMA  sqrt(nny) >= sqrt(nnz) IFF nny >= nnz 
  
    sqrt_eq             : LEMMA  sqrt(nny) = sqrt(nnz) IFF nny = nnz  
  
    sqrt_less           : LEMMA  nnx > 1 IMPLIES sqrt(nnx) < nnx
  
    sqrt_more           : LEMMA  nnx > 0 AND nnx < 1 IMPLIES sqrt(nnx) > nnx
  
  
    sqrt_lt1            : LEMMA  nnx < 1 IFF sqrt(nnx) < 1
  
    sqrt_le1            : LEMMA  nnx <= 1 IFF sqrt(nnx) <= 1
  
    sqrt_gt1            : LEMMA  nnx > 1 IFF sqrt(nnx) > 1
  
    sqrt_ge1            : LEMMA  nnx >= 1 IFF sqrt(nnx) >= 1
  
  
    sqrt_plus_le        : LEMMA  sqrt(nnx+nny) <= sqrt(nnx) + sqrt(nny)
  
    sqrt_cauchy         : LEMMA FORALL (a,b,c,d: real):
                             a*c + b*d <= sqrt(sq(a)+sq(b)) *  sqrt(sq(c)+sq(d)
 )
  
  
  
    sqrt_4              : LEMMA  sqrt(4) = 2
    sqrt_9              : LEMMA  sqrt(9) = 3 
    sqrt_16             : LEMMA  sqrt(16) = 4
    sqrt_25             : LEMMA  sqrt(25) = 5
  
    AUTO_REWRITE+   sqrt_4
    AUTO_REWRITE+   sqrt_9
    AUTO_REWRITE+   sqrt_16
    AUTO_REWRITE+   sqrt_25
  
    AUTO_REWRITE+ sqrt_0
    AUTO_REWRITE+ sqrt_1
    AUTO_REWRITE+ sqrt_square
    AUTO_REWRITE+ sqrt_sq
    AUTO_REWRITE+ sqrt_sq_neg
    AUTO_REWRITE+ sq_sqrt
  
  
  END sqrt
  
  
  $$$sqrt.prf
  (sqrt (sqrt_TCC1 0
         (sqrt_TCC1-1 nil 3253527293 nil
          ("" (lemma "sqrt_exists") (("" (propax) nil nil)) nil) proved-complet
 e
          ((sqrt_exists formula-decl nil sqrt_exists nil)) nil nil nil nil))
        (sqrt_pos 0
         (sqrt_pos-1 nil 3253527293 nil
          ("" (skosimp*) (("" (assert) nil nil)) nil) proved-complete nil nil
          nil nil nil))
        (sqrt_0 0
         (sqrt_0-1 nil 3253527293 nil
          ("" (typepred "sqrt(0)")
           (("" (lemma "zero_times3") (("" (inst?) (("" (ground) nil nil)) nil)
 )
             nil))
           nil)
          unchecked
          ((sqrt const-decl "{nnz | nnz * nnz = nnx}" sqrt nil)
           (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
           (numfield nonempty-type-eq-decl nil number_fields nil)
           (= const-decl "[T, T -> boolean]" equalities nil)
           (nonneg_real nonempty-type-eq-decl nil real_types nil)
           (>= const-decl "bool" reals nil)
           (real nonempty-type-from-decl nil reals nil)
           (real_pred const-decl "[number_field -> boolean]" reals nil)
           (number_field nonempty-type-from-decl nil number_fields nil)
           (number_field_pred const-decl "[number -> boolean]" number_fields
            nil)
           (number nonempty-type-decl nil numbers nil)
           (NOT const-decl "[bool -> bool]" booleans nil)
           (bool nonempty-type-eq-decl nil booleans nil)
           (boolean nonempty-type-decl nil booleans nil)
           (zero_times3 formula-decl nil real_props nil))
          nil nil nil nil))
        (sqrt_1 0
         (sqrt_1-1 nil 3253527293 nil
          ("" (typepred "sqrt(1)")
           (("" (lemma "sqrt_1") (("" (inst?) (("" (ground) nil nil)) nil))
             nil))
           nil)
          unchecked
          ((> const-decl "bool" reals nil)
           (sqrt const-decl "{nnz | nnz * nnz = nnx}" sqrt nil)
           (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
           (numfield nonempty-type-eq-decl nil number_fields nil)
           (= const-decl "[T, T -> boolean]" equalities nil)
           (nonneg_real nonempty-type-eq-decl nil real_types nil)
           (>= const-decl "bool" reals nil)
           (real nonempty-type-from-decl nil reals nil)
           (real_pred const-decl "[number_field -> boolean]" reals nil)
           (number_field nonempty-type-from-decl nil number_fields nil)
           (number_field_pred const-decl "[number -> boolean]" number_fields
            nil)
           (number nonempty-type-decl nil numbers nil)
           (NOT const-decl "[bool -> bool]" booleans nil)
           (bool nonempty-type-eq-decl nil booleans nil)
           (boolean nonempty-type-decl nil booleans nil)
           (sqrt_1 formula-decl nil real_props nil))
          nil nil nil nil))
        (sqrt_eq_0 0
         (sqrt_eq_0-1 nil 3253527293 nil
          ("" (skosimp*)
           (("" (typepred "sqrt(nnx!1)")
             (("" (lemma "both_sides_expt2")
               (("" (inst -1 "2" "_" "_")
                 (("" (expand "^")
                   (("" (expand "expt")
                     (("" (expand "expt")
                       (("" (expand "expt")
                         (("" (inst?)
                           (("1" (assert) nil nil) ("2" (assert) nil nil)
                            ("3" (assert) nil nil))
                           nil))
                         nil))
                       nil))
                     nil))
                   nil))
                 nil))
               nil))
             nil))
           nil)
          unchecked
          ((both_sides_expt2 formula-decl nil exponentiation nil)
           (^ const-decl "real" exponentiation nil)
           (> const-decl "bool" reals nil)
           (posreal nonempty-type-eq-decl nil real_types nil)
           (expt def-decl "real" exponentiation nil)
           (rational_pred const-decl "[real -> boolean]" rationals nil)
           (rational nonempty-type-from-decl nil rationals nil)
           (integer_pred const-decl "[rational -> boolean]" integers nil)
           (int nonempty-type-eq-decl nil integers nil)
           (/= const-decl "boolean" notequal nil)
           (nzint nonempty-type-eq-decl nil integers nil)
           (boolean nonempty-type-decl nil booleans nil)
           (bool nonempty-type-eq-decl nil booleans nil)
           (NOT const-decl "[bool -> bool]" booleans nil)
           (number nonempty-type-decl nil numbers nil)
           (number_field_pred const-decl "[number -> boolean]" number_fields
            nil)
           (number_field nonempty-type-from-decl nil number_fields nil)
           (real_pred const-decl "[number_field -> boolean]" reals nil)
           (real nonempty-type-from-decl nil reals nil)
           (>= const-decl "bool" reals nil)
           (nonneg_real nonempty-type-eq-decl nil real_types nil)
           (= const-decl "[T, T -> boolean]" equalities nil)
           (numfield nonempty-type-eq-decl nil number_fields nil)
           (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
           (sqrt const-decl "{nnz | nnz * nnz = nnx}" sqrt nil))
          nil nil nil nil))
        (sqrt_lem 0
         (sqrt_lem-1 nil 3253527293 nil
          ("" (skosimp*)
           (("" (ground)
             (("" (typepred "sqrt(nny!1)")
               (("" (replace -2 - rl)
                 (("" (hide -1 -2)
                   (("" (lemma "both_sides_expt2")
                     (("" (inst -1 "2" "_" "_")
                       (("" (expand "^")
                         (("" (expand "expt")
                           (("" (expand "expt")
                             (("" (expand "expt")
                               (("" (case-replace "nnz!1 = 0")
                                 (("1" (lemma "zero_times3")
                                   (("1" (hide -2 -3)
                                     (("1" (inst -1 "sqrt(nny!1)" "sqrt(nny!1)"
 )
                                       (("1" (ground) nil nil)) nil))
                                     nil))
                                   nil)
                                  ("2" (case-replace "sqrt(nny!1) = 0")
                                   (("1" (hide -1)
                                     (("1" (lemma "zero_times3")
                                       (("1"
                                         (hide -2)
                                         (("1"
                                           (inst?)
                                           (("1" (ground) nil nil))
                                           nil))
                                         nil))
                                       nil))
                                     nil)
                                    ("2" (inst?)
                                     (("1" (ground) nil nil)
                                      ("2" (assert) nil nil)
                                      ("3" (assert) nil nil))
                                     nil))
                                   nil))
                                 nil))
                               nil))
                             nil))
                           nil))
                         nil))
                       nil))
                     nil))
                   nil))
                 nil))
               nil))
             nil))
           nil)
          unchecked
          ((sqrt const-decl "{nnz | nnz * nnz = nnx}" sqrt nil)
           (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
           (numfield nonempty-type-eq-decl nil number_fields nil)
           (= const-decl "[T, T -> boolean]" equalities nil)
           (nonneg_real nonempty-type-eq-decl nil real_types nil)
           (>= const-decl "bool" reals nil)
           (real nonempty-type-from-decl nil reals nil)
           (real_pred const-decl "[number_field -> boolean]" reals nil)
           (number_field nonempty-type-from-decl nil number_fields nil)
           (number_field_pred const-decl "[number -> boolean]" number_fields
            nil)
           (number nonempty-type-decl nil numbers nil)
           (NOT const-decl "[bool -> bool]" booleans nil)
           (bool nonempty-type-eq-decl nil booleans nil)
           (boolean nonempty-type-decl nil booleans nil)
           (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)
           (expt def-decl "real" exponentiation nil)
           (posreal nonempty-type-eq-decl nil real_types nil)
           (> const-decl "bool" reals nil)
           (zero_times3 formula-decl nil real_props nil)
           (^ const-decl "real" exponentiation nil)
           (both_sides_expt2 formula-decl nil exponentiation nil))
          nil nil nil nil))
        (sqrt_def 0
         (sqrt_def-1 nil 3253527293 nil
          ("" (skosimp*)
           (("" (typepred "sqrt(nnx!1)") (("" (propax) nil nil)) nil)) nil)
          unchecked
          ((boolean nonempty-type-decl nil booleans nil)
           (bool nonempty-type-eq-decl nil booleans nil)
           (NOT const-decl "[bool -> bool]" booleans nil)
           (number nonempty-type-decl nil numbers nil)
           (number_field_pred const-decl "[number -> boolean]" number_fields
            nil)
           (number_field nonempty-type-from-decl nil number_fields nil)
           (real_pred const-decl "[number_field -> boolean]" reals nil)
           (real nonempty-type-from-decl nil reals nil)
           (>= const-decl "bool" reals nil)
           (nonneg_real nonempty-type-eq-decl nil real_types nil)
           (= const-decl "[T, T -> boolean]" equalities nil)
           (numfield nonempty-type-eq-decl nil number_fields nil)
           (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
           (sqrt const-decl "{nnz | nnz * nnz = nnx}" sqrt nil))
          nil nil nil nil))
        (sqrt_square 0
         (sqrt_square-1 nil 3253527293 nil
          ("" (skosimp*)
           (("" (typepred "sqrt(nnx!1 * nnx!1)")
             (("" (case-replace "nnx!1 = 0")
               (("1" (assert)
                 (("1" (lemma "zero_times3")
                   (("1" (inst?) (("1" (ground) nil nil)) nil)) nil))
                 nil)
                ("2" (case-replace "sqrt(nnx!1 * nnx!1) = 0")
                 (("1" (lemma "zero_times3")
                   (("1" (inst?) (("1" (ground) nil nil)) nil)) nil)
                  ("2" (lemma "both_sides_expt2")
                   (("2" (inst -1 "2" "_" "_")
                     (("2" (expand "^")
                       (("2" (expand "expt")
                         (("2" (expand "expt")
                           (("2" (expand "expt")
                             (("2" (inst?)
                               (("1" (assert) nil nil) ("2" (assert) nil nil)
                                ("3" (assert) nil nil))
                               nil))
                             nil))
                           nil))
                         nil))
                       nil))
                     nil))
                   nil))
                 nil))
               nil))
             nil))
           nil)
          unchecked
          ((zero_times3 formula-decl nil real_props nil)
           (both_sides_expt2 formula-decl nil exponentiation nil)
           (^ const-decl "real" exponentiation nil)
           (> const-decl "bool" reals nil)
           (posreal nonempty-type-eq-decl nil real_types nil)
           (expt def-decl "real" exponentiation nil)
           (rational_pred const-decl "[real -> boolean]" rationals nil)
           (rational nonempty-type-from-decl nil rationals nil)
           (integer_pred const-decl "[rational -> boolean]" integers nil)
           (int nonempty-type-eq-decl nil integers nil)
           (/= const-decl "boolean" notequal nil)
           (nzint nonempty-type-eq-decl nil integers nil)
           (boolean nonempty-type-decl nil booleans nil)
           (bool nonempty-type-eq-decl nil booleans nil)
           (NOT const-decl "[bool -> bool]" booleans nil)
           (number nonempty-type-decl nil numbers nil)
           (number_field_pred const-decl "[number -> boolean]" number_fields
            nil)
           (number_field nonempty-type-from-decl nil number_fields nil)
           (real_pred const-decl "[number_field -> boolean]" reals nil)
           (real nonempty-type-from-decl nil reals nil)
           (>= const-decl "bool" reals nil)
           (nonneg_real nonempty-type-eq-decl nil real_types nil)
           (= const-decl "[T, T -> boolean]" equalities nil)
           (numfield nonempty-type-eq-decl nil number_fields nil)
           (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
           (sqrt const-decl "{nnz | nnz * nnz = nnx}" sqrt nil))
          nil nil nil nil))
        (sqrt_sq 0
         (sqrt_sq-1 nil 3253527293 nil
          ("" (skosimp*)
           (("" (expand "sq") (("" (rewrite "sqrt_square") nil nil)) nil)) nil)
          unchecked
          ((sqrt_square formula-decl nil sqrt 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)
           (sq const-decl "nonneg_real" sq nil))
          nil nil nil nil))
        (sqrt_sq_neg 0
         (sqrt_sq_neg-1 nil 3254822971 3254822999
          ("" (skosimp*)
           (("" (expand "sq")
             (("" (lemma "sqrt_square")
               (("" (inst -1 "-x!1")
                 (("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
               nil))
             nil))
           nil)
          unchecked
          ((sq const-decl "nonneg_real" sq nil)
           (- const-decl "[numfield -> numfield]" number_fields nil)
           (numfield nonempty-type-eq-decl nil number_fields nil)
           (>= const-decl "bool" reals nil)
           (bool nonempty-type-eq-decl nil booleans nil)
           (real nonempty-type-from-decl nil reals nil)
           (real_pred const-decl "[number_field -> boolean]" reals nil)
           (number_field nonempty-type-from-decl nil number_fields nil)
           (number_field_pred const-decl "[number -> boolean]" number_fields
            nil)
           (boolean nonempty-type-decl nil booleans nil)
           (number nonempty-type-decl nil numbers nil)
           (nonneg_real nonempty-type-eq-decl nil real_types nil)
           (sqrt_square formula-decl nil sqrt nil))
          27977 1780 t shostak))
        (sqrt_sq_abs 0
         (sqrt_sq_abs-1 nil 3253527293 nil
          ("" (skosimp*)
           (("" (case "x!1 >= 0")
             (("1" (expand "sq")
               (("1" (rewrite "sqrt_square")
                 (("1" (expand "abs") (("1" (assert) nil nil)) nil)) nil))
               nil)
              ("2" (lemma "sq_neg")
               (("2" (inst?)
                 (("2" (replace -1 :hide? t :dir rl)
                   (("2" (expand "sq")
                     (("2" (rewrite "sqrt_square")
                       (("2" (expand "abs") (("2" (assert) nil nil)) nil)) nil)
 )
                     nil))
                   nil))
                 nil))
               nil))
             nil))
           nil)
          unchecked
          ((sq_neg formula-decl nil sq nil)
           (numfield nonempty-type-eq-decl nil number_fields nil)
           (- const-decl "[numfield -> numfield]" number_fields nil)
           (sq const-decl "nonneg_real" sq nil)
           (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil)
           (nonneg_real nonempty-type-eq-decl nil real_types nil)
           (sqrt_square formula-decl nil sqrt 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))
          nil nil nil nil))
        (sq_sqrt 0
         (sq_sqrt-1 nil 3253527293 nil
          ("" (skosimp*)
           (("" (expand "sq") (("" (rewrite "sqrt_def") nil nil)) nil)) nil)
          unchecked
          ((sqrt_def formula-decl nil sqrt 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)
           (sq const-decl "nonneg_real" sq nil))
          nil nil nil nil))
        (sqrt_times 0
         (sqrt_times-1 nil 3253527293 nil
          ("" (skosimp*)
           (("" (case "sqrt(nny!1) = 0 OR  sqrt(nnz!1) = 0")
             (("1" (ground) nil nil)
              ("2" (flatten)
               (("2" (lemma "both_sides_expt2")
                 (("2" (inst -1 "2" "_" "_")
                   (("2" (expand "^")
                     (("2" (expand "expt")
                       (("2" (expand "expt")
                         (("2" (expand "expt")
                           (("2"
                             (inst -1 "sqrt(nny!1) * sqrt(nnz!1)"
                              "sqrt(nny!1 * nnz!1)")
                             (("1" (flatten) (("1" (assert) nil nil)) nil)
                              ("2" (assert)
                               (("2" (case-replace "sqrt(nny!1 * nnz!1) = 0")
                                 (("1" (lemma "sqrt_eq_0")
                                   (("1" (inst -1 "nny!1*nnz!1")
                                     (("1" (assert)
                                       (("1"
                                         (lemma "zero_times3")
                                         (("1"
                                           (inst?)
                                           (("1" (assert) nil nil))
                                           nil))
                                         nil))
                                       nil))
                                     nil))
                                   nil)
                                  ("2" (assert)
                                   (("2" (typepred "sqrt(nny!1 * nnz!1)")
                                     (("2" (assert) nil nil)) nil))
                                   nil))
                                 nil))
                               nil)
                              ("3"
                               (case-replace "sqrt(nny!1) * sqrt(nnz!1) = 0")
                               (("1" (lemma "zero_times3")
                                 (("1" (inst?) (("1" (assert) nil nil)) nil))
                                 nil)
                                ("2" (assert) nil nil))
                               nil))
                             nil))
                           nil))
                         nil))
                       nil))
                     nil))
                   nil))
                 nil))
               nil))
             nil))
           nil)
          unchecked
          ((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)
           (expt def-decl "real" exponentiation nil)
           (zero_times3 formula-decl nil real_props nil)
           (posreal nonempty-type-eq-decl nil real_types nil)
           (> const-decl "bool" reals nil)
           (^ const-decl "real" exponentiation nil)
           (both_sides_expt2 formula-decl nil exponentiation nil)
           (boolean nonempty-type-decl nil booleans nil)
           (bool nonempty-type-eq-decl nil booleans nil)
           (OR const-decl "[bool, bool -> bool]" booleans nil)
           (number nonempty-type-decl nil numbers nil)
           (= const-decl "[T, T -> boolean]" equalities nil)
           (number_field_pred const-decl "[number -> boolean]" number_fields
            nil)
           (number_field nonempty-type-from-decl nil number_fields nil)
           (real_pred const-decl "[number_field -> boolean]" reals nil)
           (real nonempty-type-from-decl nil reals nil)
           (>= const-decl "bool" reals nil)
           (nonneg_real nonempty-type-eq-decl nil real_types nil)
           (numfield nonempty-type-eq-decl nil number_fields nil)
           (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
           (sqrt const-decl "{nnz | nnz * nnz = nnx}" sqrt nil))
          nil nil nil nil))
        (sqrt_div_TCC1 0
         (sqrt_div_TCC1-1 nil 3253527293 nil
          ("" (skosimp*) (("" (rewrite "pos_div_ge") nil nil)) nil)
          proved-complete
          ((nonneg_real nonempty-type-eq-decl nil real_types nil)
           (>= const-decl "bool" reals nil)
           (bool nonempty-type-eq-decl nil booleans nil)
           (nonzero_real nonempty-type-eq-decl nil reals nil)
           (/= const-decl "boolean" notequal nil)
           (real nonempty-type-from-decl nil reals nil)
           (real_pred const-decl "[number_field -> boolean]" reals nil)
           (number_field nonempty-type-from-decl nil number_fields nil)
           (number_field_pred const-decl "[number -> boolean]" number_fields
            nil)
           (boolean nonempty-type-decl nil booleans nil)
           (number nonempty-type-decl nil numbers nil)
           (pos_div_ge formula-decl nil real_props nil))
          nil nil nil nil))
        (sqrt_div_TCC2 0
         (sqrt_div_TCC2-1 nil 3253527293 nil ("" (subtype-tcc) nil nil)
          proved-complete
          ((/= const-decl "boolean" notequal nil)
           (nonneg_real nonempty-type-eq-decl nil real_types nil)
           (>= const-decl "bool" reals nil)
           (real nonempty-type-from-decl nil reals nil)
           (real_pred const-decl "[number_field -> boolean]" reals nil)
           (number_field nonempty-type-from-decl nil number_fields nil)
           (number_field_pred const-decl "[number -> boolean]" number_fields
            nil)
           (number nonempty-type-decl nil numbers nil)
           (NOT const-decl "[bool -> bool]" booleans nil)
           (bool nonempty-type-eq-decl nil booleans nil)
           (boolean nonempty-type-decl nil booleans nil))
          nil nil nil nil))
        (sqrt_div 0
         (sqrt_div-1 nil 3253527293 nil
          ("" (skosimp*)
           (("" (lemma "sqrt_sq")
             (("" (inst -1 "sqrt(nny!1)/sqrt(nnz!1)")
               (("1" (ground)
                 (("1" (hide 2 3)
                   (("1" (lemma "sqrt_pos")
                     (("1" (inst -1 "nny!1")
                       (("1" (rewrite "pos_div_ge") nil nil)
                        ("2" (case-replace "nny!1=0")
                         (("1" (rewrite "sqrt_0") (("1" (assert) nil nil)) nil)
                          ("2" (ground) nil nil))
                         nil))
                       nil))
                     nil))
                   nil))
                 nil)
                ("2" (lemma "sqrt_eq_0")
                 (("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
               nil))
             nil))
           nil)
          unchecked
          ((sqrt const-decl "{nnz | nnz * nnz = nnx}" sqrt nil)
           (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
           (numfield nonempty-type-eq-decl nil number_fields nil)
           (= const-decl "[T, T -> boolean]" equalities nil)
           (nonneg_real nonempty-type-eq-decl nil real_types nil)
           (>= const-decl "bool" reals nil)
           (bool nonempty-type-eq-decl nil booleans nil)
           (real nonempty-type-from-decl nil reals nil)
           (real_pred const-decl "[number_field -> boolean]" reals nil)
           (number_field nonempty-type-from-decl nil number_fields nil)
           (number_field_pred const-decl "[number -> boolean]" number_fields
            nil)
           (/= const-decl "boolean" notequal nil)
           (boolean nonempty-type-decl nil booleans nil)
           (number nonempty-type-decl nil numbers nil)
           (nznum nonempty-type-eq-decl nil number_fields nil)
           (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
           (> const-decl "bool" reals nil)
           (posreal nonempty-type-eq-decl nil real_types nil)
           (pos_div_ge formula-decl nil real_props nil)
           (nonzero_real nonempty-type-eq-decl nil reals nil)
           (sqrt_0 formula-decl nil sqrt nil)
           (sqrt_pos judgement-tcc nil sqrt nil)
           (sqrt_eq_0 formula-decl nil sqrt nil)
           (sqrt_sq formula-decl nil sqrt nil))
          nil nil nil nil))
        (sqrt_lt 0
         (sqrt_lt-1 nil 3253527293 nil
          ("" (skosimp*)
           (("" (ground)
             (("1" (lemma "gt_times_gt_pos1")
               (("1"
                 (inst -1 "sqrt(nny!1)" "sqrt(nny!1)" "sqrt(nnz!1)"
                  "sqrt(nnz!1)")
                 (("1" (assert) nil nil)) nil))
               nil)
              ("2" (typepred "sqrt(nny!1)")
               (("2" (replace -2 - rl)
                 (("2" (hide -2)
                   (("2" (typepred "sqrt(nnz!1)")
                     (("2" (replace -2 - rl)
                       (("2" (hide -1 -2 -3)
                         (("2" (lemma "both_sides_expt_pos_lt_aux")
                           (("2" (inst -1 "1" "sqrt(nny!1)" "sqrt(nnz!1)")
                             (("2" (expand "expt")
                               (("2" (expand "expt")
                                 (("2" (expand "expt") (("2" (propax) nil nil))
                                   nil))
                                 nil))
                               nil))
                             nil))
                           nil))
                         nil))
                       nil))
                     nil))
                   nil))
                 nil))
               nil))
             nil))
           nil)
          unchecked
          ((NOT const-decl "[bool -> bool]" booleans nil)
           (both_sides_expt_pos_lt_aux formula-decl nil exponentiation nil)
           (expt def-decl "real" exponentiation nil)
           (nat nonempty-type-eq-decl nil naturalnumbers 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)
           (gt_times_gt_pos1 formula-decl nil real_props nil)
           (posreal nonempty-type-eq-decl nil real_types nil)
           (> const-decl "bool" reals nil)
           (sqrt const-decl "{nnz | nnz * nnz = nnx}" sqrt nil)
           (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
           (numfield nonempty-type-eq-decl nil number_fields nil)
           (= const-decl "[T, T -> boolean]" equalities nil)
           (nonneg_real nonempty-type-eq-decl nil real_types nil)
           (>= const-decl "bool" reals nil)
           (bool nonempty-type-eq-decl nil booleans nil)
           (real nonempty-type-from-decl nil reals nil)
           (real_pred const-decl "[number_field -> boolean]" reals nil)
           (number_field nonempty-type-from-decl nil number_fields nil)
           (number_field_pred const-decl "[number -> boolean]" number_fields
            nil)
           (boolean nonempty-type-decl nil booleans nil)
           (number nonempty-type-decl nil numbers nil))
          nil nil nil nil))
        (sqrt_le 0
         (sqrt_le-1 nil 3253527293 nil
          ("" (skosimp*)
           (("" (lemma "sqrt_lt")
             (("" (inst -1 "nny!1" "nnz!1") (("" (ground) nil nil)) nil)) nil))
           nil)
          unchecked
          ((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)
           (sqrt_lt formula-decl nil sqrt nil))
          nil nil nil nil))
        (sqrt_gt 0
         (sqrt_gt-1 nil 3253527293 nil
          ("" (skosimp*)
           (("" (lemma "sqrt_lt")
             (("" (inst -1 "nny!1" "nnz!1")
               (("" (assert) (("" (ground) nil nil)) nil)) nil))
             nil))
           nil)
          unchecked
          ((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)
           (sqrt_lt formula-decl nil sqrt nil))
          nil nil nil nil))
        (sqrt_ge 0
         (sqrt_ge-1 nil 3253527293 nil
          ("" (skosimp*)
           (("" (lemma "sqrt_le")
             (("" (inst -1 "nny!1" "nnz!1") (("" (ground) nil nil)) nil)) nil))
           nil)
          unchecked
          ((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)
           (sqrt_le formula-decl nil sqrt nil))
          nil nil nil nil))
        (sqrt_eq 0
         (sqrt_eq-1 nil 3253527293 nil
          ("" (skosimp*) (("" (ground) nil nil)) nil) unchecked nil nil nil nil
          nil))
        (sqrt_less 0
         (sqrt_less-1 nil 3253527294 nil
          ("" (skosimp*)
           (("" (typepred "sqrt(nnx!1)")
             (("" (lemma "both_sides_expt_pos_gt_aux")
               (("" (inst -1 "1" "nnx!1" "sqrt(nnx!1)")
                 (("1" (flatten)
                   (("1" (hide -2)
                     (("1" (assert)
                       (("1" (expand "expt")
                         (("1" (expand "expt")
                           (("1" (expand "expt")
                             (("1" (replace -2)
                               (("1" (hide -2 2)
                                 (("1" (lemma "both_sides_times_pos_gt1")
                                   (("1" (inst -1 "nnx!1" "nnx!1" "1")
                                     (("1" (assert) nil nil)) nil))
                                   nil))
                                 nil))
                               nil))
                             nil))
                           nil))
                         nil))
                       nil))
                     nil))
                   nil)
                  ("2" (case-replace "sqrt(nnx!1) = 0")
                   (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)
                  ("3" (assert) nil nil))
                 nil))
               nil))
             nil))
           nil)
          unchecked
          ((both_sides_expt_pos_gt_aux formula-decl nil exponentiation nil)
           (both_sides_times_pos_gt1 formula-decl nil real_props nil)
           (expt def-decl "real" exponentiation nil)
           (posreal nonempty-type-eq-decl nil real_types nil)
           (nat nonempty-type-eq-decl nil naturalnumbers 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 "bool" reals nil)
           (boolean nonempty-type-decl nil booleans nil)
           (bool nonempty-type-eq-decl nil booleans nil)
           (NOT const-decl "[bool -> bool]" booleans nil)
           (number nonempty-type-decl nil numbers nil)
           (number_field_pred const-decl "[number -> boolean]" number_fields
            nil)
           (number_field nonempty-type-from-decl nil number_fields nil)
           (real_pred const-decl "[number_field -> boolean]" reals nil)
           (real nonempty-type-from-decl nil reals nil)
           (>= const-decl "bool" reals nil)
           (nonneg_real nonempty-type-eq-decl nil real_types nil)
           (= const-decl "[T, T -> boolean]" equalities nil)
           (numfield nonempty-type-eq-decl nil number_fields nil)
           (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
           (sqrt const-decl "{nnz | nnz * nnz = nnx}" sqrt nil))
          nil nil nil nil))
        (sqrt_more 0
         (sqrt_more-1 nil 3253527294 nil
          ("" (skosimp*)
           (("" (typepred "sqrt(nnx!1)")
             (("" (lemma "both_sides_expt_pos_gt_aux")
               (("" (inst -1 "1" "sqrt(nnx!1)" "nnx!1")
                 (("1" (flatten)
                   (("1" (hide -2)
                     (("1" (assert)
                       (("1" (expand "expt")
                         (("1" (expand "expt")
                           (("1" (expand "expt")
                             (("1" (replace -2)
                               (("1" (hide -2 2)
                                 (("1" (lemma "both_sides_times_pos_gt1")
                                   (("1" (inst -1 "nnx!1" "1" "nnx!1")
                                     (("1" (assert) nil nil)) nil))
                                   nil))
                                 nil))
                               nil))
                             nil))
                           nil))
                         nil))
                       nil))
                     nil))
                   nil)
                  ("2" (assert) nil nil))
                 nil))
               nil))
             nil))
           nil)
          unchecked
          ((both_sides_expt_pos_gt_aux formula-decl nil exponentiation nil)
           (both_sides_times_pos_gt1 formula-decl nil real_props nil)
           (expt def-decl "real" exponentiation nil)
           (posreal nonempty-type-eq-decl nil real_types nil)
           (nat nonempty-type-eq-decl nil naturalnumbers 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 "bool" reals nil)
           (boolean nonempty-type-decl nil booleans nil)
           (bool nonempty-type-eq-decl nil booleans nil)
           (NOT const-decl "[bool -> bool]" booleans nil)
           (number nonempty-type-decl nil numbers nil)
           (number_field_pred const-decl "[number -> boolean]" number_fields
            nil)
           (number_field nonempty-type-from-decl nil number_fields nil)
           (real_pred const-decl "[number_field -> boolean]" reals nil)
           (real nonempty-type-from-decl nil reals nil)
           (>= const-decl "bool" reals nil)
           (nonneg_real nonempty-type-eq-decl nil real_types nil)
           (= const-decl "[T, T -> boolean]" equalities nil)
           (numfield nonempty-type-eq-decl nil number_fields nil)
           (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
           (sqrt const-decl "{nnz | nnz * nnz = nnx}" sqrt nil))
          nil nil nil nil))
        (sqrt_lt1 0
         (sqrt_lt1-1 nil 3254824033 3254824037
          ("" (skosimp*)
           (("" (lemma "sqrt_gt")
             (("" (inst - "1" "nnx!1")
               (("" (rewrite "sqrt_1")
                 (("" (assert) (("" (ground) nil nil)) nil)) nil))
               nil))
             nil))
           nil)
          unchecked
          ((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)
           (sqrt_1 formula-decl nil sqrt nil)
           (sqrt_gt formula-decl nil sqrt nil))
          3500 110 nil nil))
        (sqrt_le1 0
         (sqrt_le1-1 nil 3254824101 3254824131
          ("" (skosimp*)
           (("" (lemma "sqrt_le")
             (("" (inst - "nnx!1" "1")
               (("" (rewrite "sqrt_1") (("" (grind) nil nil)) nil)) nil))
             nil))
           nil)
          unchecked
          ((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)
           (sqrt_1 formula-decl nil sqrt nil)
           (sqrt_le formula-decl nil sqrt nil))
          29014 2040 t nil))
        (sqrt_gt1 0
         (sqrt_gt1-1 nil 3254823853 3254823969
          ("" (skosimp*)
           (("" (lemma "sqrt_lt")
             (("" (inst - "1" "nnx!1")
               (("" (rewrite "sqrt_1")
                 (("" (assert) (("" (ground) nil nil)) nil)) nil))
               nil))
             nil))
           nil)
          unchecked
          ((sqrt_lt formula-decl nil sqrt nil)
           (sqrt_1 formula-decl nil sqrt nil)
           (nonneg_real nonempty-type-eq-decl nil real_types nil)
           (>= const-decl "bool" reals nil)
           (bool nonempty-type-eq-decl nil booleans nil)
           (real nonempty-type-from-decl nil reals nil)
           (real_pred const-decl "[number_field -> boolean]" reals nil)
           (number_field nonempty-type-from-decl nil number_fields nil)
           (number_field_pred const-decl "[number -> boolean]" number_fields
            nil)
           (boolean nonempty-type-decl nil booleans nil)
           (number nonempty-type-decl nil numbers nil))
          115887 5650 t shostak))
        (sqrt_ge1 0
         (sqrt_ge1-1 nil 3254824148 3254824153
          ("" (skosimp*)
           (("" (lemma "sqrt_ge")
             (("" (inst - "nnx!1" "1")
               (("" (rewrite "sqrt_1") (("" (grind) nil nil)) nil)) nil))
             nil))
           nil)
          unchecked
          ((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)
           (sqrt_1 formula-decl nil sqrt nil)
           (sqrt_ge formula-decl nil sqrt nil))
          3473 60 nil nil))
        (sqrt_plus_le 0
         (sqrt_plus_le-1 nil 3253528174 3253528325
          ("" (skosimp*)
           (("" (lemma "sq_le")
             (("" (inst?)
               (("" (assert)
                 (("" (hide 2)
                   (("" (rewrite "sq_sqrt")
                     (("" (expand "sq")
                       (("" (rewrite "sq_rew")
                         (("" (rewrite "sq_rew")
                           (("" (assert)
                             (("" (assert)
                               (("" (rewrite "sq_sqrt")
                                 (("1" (rewrite "sq_sqrt")
                                   (("1" (assert) nil nil)) nil)
                                  ("2" (typepred "nnx!1")
                                   (("2" (propax) nil nil)) nil))
                                 nil))
                               nil))
                             nil))
                           nil))
                         nil))
                       nil))
                     nil))
                   nil))
                 nil))
               nil))
             nil))
           nil)
          unchecked
          ((sq_le formula-decl nil sq nil) (sq_sqrt formula-decl nil sqrt nil)
           (sq_rew formula-decl nil sq nil)
           (NOT const-decl "[bool -> bool]" booleans nil)
           (sq const-decl "nonneg_real" sq nil)
           (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
           (sqrt const-decl "{nnz | nnz * nnz = nnx}" sqrt nil)
           (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
           (numfield nonempty-type-eq-decl nil number_fields nil)
           (= const-decl "[T, T -> boolean]" equalities nil)
           (nonneg_real nonempty-type-eq-decl nil real_types nil)
           (>= const-decl "bool" reals nil)
           (bool nonempty-type-eq-decl nil booleans nil)
           (real nonempty-type-from-decl nil reals nil)
           (real_pred const-decl "[number_field -> boolean]" reals nil)
           (number_field nonempty-type-from-decl nil number_fields nil)
           (number_field_pred const-decl "[number -> boolean]" number_fields
            nil)
           (boolean nonempty-type-decl nil booleans nil)
           (number nonempty-type-decl nil numbers nil))
          61551 5700 t shostak))
        (sqrt_cauchy 0
         (sqrt_cauchy-1 nil 3253527294 nil
          ("" (skolem 1 ("a" "b" "c" "d"))
           (("" (rewrite "sq_le" :dir rl)
             (("" (rewrite "sq_times")
               (("" (rewrite "sq_sqrt")
                 (("" (rewrite "sq_sqrt")
                   (("" (rewrite "sq_plus")
                     (("" (rewrite "sq_times")
                       (("" (rewrite "sq_times")
                         (("" (ground)
                           (("" (both-sides "-" "sq(a) * sq(c)")
                             (("" (ground)
                               (("" (both-sides "-" " sq(b) * sq(d)")
                                 (("" (ground)
                                   (("" (both-sides "-" " 2 * (a * b * c * d)")
                                     (("" (ground)
                                       ((""
                                         (case
                                          "sq(a) * sq(d) + sq(b) * sq(c) - 2 * 
 (a * b * c * d) = sq(a*d - b*c)")
                                         (("1"
                                           (replace -1 :hide? t)
                                           (("1"
                                             (lemma "sq_pos")
                                             (("1"
                                               (inst?)
                                               (("1" (ground) nil nil))
                                               nil))
                                             nil))
                                           nil)
                                          ("2"
                                           (hide 2)
                                           (("2"
                                             (rewrite "sq_minus")
                                             (("2"
                                               (rewrite "sq_times")
                                               (("2"
                                                 (rewrite "sq_times")
                                                 nil
                                                 nil))
                                               nil))
                                             nil))
                                           nil))
                                         nil))
                                       nil))
                                     nil))
                                   nil))
                                 nil))
                               nil))
                             nil))
                           nil))
                         nil))
                       nil))
                     nil))
                   nil))
                 nil))
               nil))
             nil))
           nil)
          unchecked
          ((sq_times formula-decl nil sq nil) (sq_minus formula-decl nil sq nil
 )
           (sq_pos formula-decl nil sq nil)
           (both_sides_times_pos_le2 formula-decl nil real_props nil)
           (neg_times_gt formula-decl nil real_props nil)
           (neg_times_ge formula-decl nil real_props nil)
           (pos_times_lt formula-decl nil real_props nil)
           (pos_times_le formula-decl nil real_props nil)
           (pos_times_gt formula-decl nil real_props nil)
           (pos_times_ge formula-decl nil real_props nil)
           (neg_times_lt formula-decl nil real_props nil)
           (neg_times_le formula-decl nil real_props nil)
           (both_sides_plus_le2 formula-decl nil real_props nil)
           (both_sides_minus_le1 formula-decl nil real_props nil)
           (NOT const-decl "[bool -> bool]" booleans nil)
           (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
           (<= const-decl "bool" reals nil) (sq_plus formula-decl nil sq nil)
           (sq_sqrt formula-decl nil sqrt nil)
           (sq const-decl "nonneg_real" sq nil)
           (sqrt const-decl "{nnz | nnz * nnz = nnx}" sqrt nil)
           (= const-decl "[T, T -> boolean]" equalities nil)
           (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
           (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
           (numfield nonempty-type-eq-decl nil number_fields nil)
           (nonneg_real nonempty-type-eq-decl nil real_types nil)
           (>= const-decl "bool" reals nil)
           (bool nonempty-type-eq-decl nil booleans nil)
           (real nonempty-type-from-decl nil reals nil)
           (real_pred const-decl "[number_field -> boolean]" reals nil)
           (number_field nonempty-type-from-decl nil number_fields nil)
           (number_field_pred const-decl "[number -> boolean]" number_fields
            nil)
           (boolean nonempty-type-decl nil booleans nil)
           (number nonempty-type-decl nil numbers nil)
           (sq_le formula-decl nil sq nil))
          nil nil nil nil))
        (sqrt_4 0
         (sqrt_4-1 nil 3285686712 3285686755 ("" (rewrite "sqrt_lem") nil nil)
          proved
          ((nonneg_real nonempty-type-eq-decl nil real_types nil)
           (>= const-decl "bool" reals nil)
           (bool nonempty-type-eq-decl nil booleans nil)
           (real nonempty-type-from-decl nil reals nil)
           (real_pred const-decl "[number_field -> boolean]" reals nil)
           (number_field nonempty-type-from-decl nil number_fields nil)
           (number_field_pred const-decl "[number -> boolean]" number_fields
            nil)
           (boolean nonempty-type-decl nil booleans nil)
           (number nonempty-type-decl nil numbers nil)
           (sqrt_lem formula-decl nil sqrt nil))
          42647 910 t shostak))
        (sqrt_9 0
         (sqrt_9-1 nil 3285686759 3285686762 ("" (rewrite "sqrt_lem") nil nil)
          proved
          ((nonneg_real nonempty-type-eq-decl nil real_types nil)
           (>= const-decl "bool" reals nil)
           (bool nonempty-type-eq-decl nil booleans nil)
           (real nonempty-type-from-decl nil reals nil)
           (real_pred const-decl "[number_field -> boolean]" reals nil)
           (number_field nonempty-type-from-decl nil number_fields nil)
           (number_field_pred const-decl "[number -> boolean]" number_fields
            nil)
           (boolean nonempty-type-decl nil booleans nil)
           (number nonempty-type-decl nil numbers nil)
           (sqrt_lem formula-decl nil sqrt nil))
          2580 240 t shostak))
        (sqrt_16 0
         (sqrt_16-1 nil 3285686766 3285686768 ("" (rewrite "sqrt_lem") nil nil)
          proved
          ((nonneg_real nonempty-type-eq-decl nil real_types nil)
           (>= const-decl "bool" reals nil)
           (bool nonempty-type-eq-decl nil booleans nil)
           (real nonempty-type-from-decl nil reals nil)
           (real_pred const-decl "[number_field -> boolean]" reals nil)
           (number_field nonempty-type-from-decl nil number_fields nil)
           (number_field_pred const-decl "[number -> boolean]" number_fields
            nil)
           (boolean nonempty-type-decl nil booleans nil)
           (number nonempty-type-decl nil numbers nil)
           (sqrt_lem formula-decl nil sqrt nil))
          1651 250 t shostak))
        (sqrt_25 0
         (sqrt_25-1 nil 3285686771 3285686772 ("" (rewrite "sqrt_lem") nil nil)
          proved
          ((nonneg_real nonempty-type-eq-decl nil real_types nil)
           (>= const-decl "bool" reals nil)
           (bool nonempty-type-eq-decl nil booleans nil)
           (real nonempty-type-from-decl nil reals nil)
           (real_pred const-decl "[number_field -> boolean]" reals nil)
           (number_field nonempty-type-from-decl nil number_fields nil)
           (number_field_pred const-decl "[number -> boolean]" number_fields
            nil)
           (boolean nonempty-type-decl nil booleans nil)
           (number nonempty-type-decl nil numbers nil)
           (sqrt_lem formula-decl nil sqrt nil))
          1056 250 t shostak)))
  
  
  $$$criteria.pvs
  criteria : THEORY
  BEGIN
  
    IMPORTING sqrt,Vectors
  
    D  : posreal %% Half the diameter
    H  : posreal %% Half the height
  
    s,sr,v,vr: VAR Vect3
    t        : VAR real
    sz       : VAR real
    vz       : VAR nzreal
  
  
    hor_sep?(s) : bool = sq(s`x) + sq(s`y) >= sq(D)   % horizontal separation
  
    vert_sep?(s) : bool = abs(s`z) >= H    % vertical separation
  
    separation?(s,v): bool = (FORALL t: hor_sep?(s+t*v) OR
                                        vert_sep?(s+t*v))
  
  
    %%%% Horizontal Criteria (Lemma 3.2)
  
    hor_speed_gt_0?(v) : bool =            % horizontal speed > 0
      sq(v`x) + sq(v`y) > 0
  
  
  END criteria
  
  $$$criteria.prf
  (criteria
   (vert_pass_criterion 0
    (vert_pass_criterion-1 nil 3287830556 3287831742
     ("" (skosimp*)
      (("" (expand "vert_sep?")
        (("" (expand* "+" "*")
          (("" (expand "vert_pass?")
            (("" (lemma "abs_plus")
              (("" (inst?)
                (("" (split -)
                  (("1" (replace -1 :hide? t) (("1" (assert) nil nil)) nil)
                   ("2" (hide 2)
                    (("2" (lemma "pos_times_ge")
                      (("2" (inst - "z(s!1) * z(v!1) * eps!1" "eps!1 * t!1")
                        (("2" (assert)
                          (("2" (hide -4 -3 -2)
                            (("2" (typepred "eps!1")
                              (("2" (split -)
                                (("1" (assert) nil nil) ("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((vert_sep? const-decl "bool" criteria nil)
      (vert_pass? const-decl "bool" criteria 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)
      (Vect3 type-eq-decl nil Vectors nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (int nonempty-type-eq-decl nil integers nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (OR const-decl "[bool, bool -> bool]" booleans nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (- const-decl "[numfield -> numfield]" number_fields nil)
      (Sign type-eq-decl nil sign nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (pos_times_ge formula-decl nil real_props nil)
      (abs_plus formula-decl nil sign nil) (+ const-decl "Vect3" Vectors nil)
      (* const-decl "Vect3" Vectors nil))
     318 300 nil nil))
   (hor_pass_criterion 0
    (hor_pass_criterion-1 nil 3287830556 3287831743
     ("" (skosimp*)
      (("" (expand "hor_sep?")
        (("" (expand* "+" "*")
          ((""
            (case "sq(s!1`x + t!1 * v!1`x) + sq(s!1`y + t!1 * v!1`y) = sq(s!1`x
 ) + sq(s!1`y) + 2*t!1*(s!1`x * v!1`x + s!1`y * v!1`y) + sq(t!1*v!1`x) + sq(t!1
 *v!1`y)")
            (("1" (replace -1 :hide? t)
              (("1" (case "2 * t!1 * (s!1`x * v!1`x + s!1`y * v!1`y) >= 0")
                (("1" (assert) nil nil)
                 ("2" (hide 2)
                  (("2" (rewrite "pos_times_ge")
                    (("2" (flatten)
                      (("2" (expand "hor_pass?")
                        (("2" (typepred "eps!1")
                          (("2" (split -)
                            (("1" (assert) nil nil) ("2" (assert) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (hide 2)
              (("2" (hide-all-but 1)
                (("2" (expand "sq") (("2" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((hor_sep? const-decl "bool" criteria nil)
      (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (Vect3 type-eq-decl nil Vectors nil) (sq const-decl "nonneg_real" sq nil)
      (nonneg_real nonempty-type-eq-decl nil real_types nil)
      (>= const-decl "bool" reals nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (pos_times_ge formula-decl nil real_props nil)
      (hor_pass? const-decl "bool" criteria nil)
      (Sign type-eq-decl nil sign nil)
      (- const-decl "[numfield -> numfield]" number_fields 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)
      (OR const-decl "[bool, bool -> bool]" booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (+ const-decl "Vect3" Vectors nil) (* const-decl "Vect3" Vectors nil))
     476 470 nil nil))
   (tau_TCC1 0
    (tau_TCC1-1 nil 3287830556 3287831743 ("" (subtype-tcc) nil nil) proved
     ((boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (real nonempty-type-from-decl nil reals nil)
      (Vect3 type-eq-decl nil Vectors nil)
      (hor_speed_gt_0? const-decl "bool" criteria nil)
      (sq const-decl "nonneg_real" sq nil))
     146 140 nil nil))
   (theta_p_lt_theta_pp 0
    (theta_p_lt_theta_pp-1 nil 3287830556 3287831750
     ("" (skosimp*)
      (("" (expand "theta")
        (("" (case "vz!1 > 0")
          (("1" (expand "sign") (("1" (assert) (("1" (field 1) nil nil)) nil))
            nil)
           ("2" (expand "sign") (("2" (assert) (("2" (field 2) nil nil)) nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((theta const-decl "real" criteria nil)
      (both_sides_times_neg_ge1_imp formula-decl nil extra_real_props "Manip/")
      (nonpos_real nonempty-type-eq-decl nil real_types nil)
      (X2__ skolem-const-decl "nzreal" criteria nil)
      (<= const-decl "bool" reals nil) (sign const-decl "Sign" sign nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props "Manip/")
      (H const-decl "posreal" criteria nil)
      (posreal nonempty-type-eq-decl nil real_types nil)
      (- const-decl "[numfield -> numfield]" number_fields nil)
      (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
      (nznum nonempty-type-eq-decl nil number_fields nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (nonneg_real nonempty-type-eq-decl nil real_types nil)
      (X1__ skolem-const-decl "nzreal" criteria nil)
      (>= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
      (div_cancel2 formula-decl nil real_props nil)
      (nonzero_real nonempty-type-eq-decl nil reals 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) (/= const-decl "boolean" notequal nil)
      (nzreal nonempty-type-eq-decl nil reals nil))
     6877 6710 nil nil))
   (theta_translation 0
    (theta_translation-1 nil 3287830556 3287831752
     ("" (skosimp*)
      (("" (expand "theta")
        (("" (field 2)
          (("" (expand "at")
            (("" (assert)
              (("" (expand "+ ") (("" (expand "*") (("" (assert) nil nil)) nil)
 )
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((theta const-decl "real" criteria nil) (+ const-decl "Vect3" Vectors nil)
      (* const-decl "Vect3" Vectors nil)
      (neg_mult formula-decl nil extra_tegies "Field/")
      (one_times formula-decl nil extra_tegies "Field/")
      (div_cancel2 formula-decl nil real_props nil)
      (X3__ skolem-const-decl "real" criteria nil)
      (nonzero_real nonempty-type-eq-decl nil reals nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (nznum nonempty-type-eq-decl nil number_fields nil)
      (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
      (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (int nonempty-type-eq-decl nil integers nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (OR const-decl "[bool, bool -> bool]" booleans nil)
      (- const-decl "[numfield -> numfield]" number_fields nil)
      (Sign type-eq-decl nil sign nil) (sign const-decl "Sign" sign 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)
      (H const-decl "posreal" criteria nil) (at const-decl "Vect3" criteria nil
 )
      (both_sides_times1 formula-decl nil real_props nil)
      (/= const-decl "boolean" notequal nil)
      (number nonempty-type-decl nil numbers nil)
      (boolean nonempty-type-decl nil booleans nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (real nonempty-type-from-decl nil reals nil)
      (Vect3 type-eq-decl nil Vectors 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))
     1875 1760 nil nil))
   (tau_is_tangent_pt 0
    (tau_is_tangent_pt-1 nil 3287830556 3287832526
     ("" (skosimp*)
      (("" (expand "hor_speed_gt_0?")
        (("" (case "sq(x(ve!1)) + sq(y(ve!1)) > 0")
          (("1" (expand "tan_condition?")
            (("1" (factor -3)
              (("1" (div-by -3 "sq(x(ve!1)) + sq(y(ve!1))")
                (("1" (expand "tangent_point?")
                  (("1" (split)
                    (("1" (expand "at")
                      (("1" (expand "tau")
                        (("1" (expand "+")
                          (("1" (expand "*")
                            (("1"
                              (case "s!1`x +
                                                                               
                                                       -(x(s!1) * x(ve!1) + y(s
 !1) * y(ve!1)) /
                                                                               
                                                        (sq(x(ve!1)) + sq(y(ve!
 1)))
                                                                               
                                                        * ve!1`x = ve!1`y*(s!1`
 x*ve!1`y-s!1`y*ve!1`x) /
                                                                               
                                                        (sq(x(ve!1)) + sq(y(ve!
 1)))")
                              (("1" (replace -1 1)
                                (("1" (hide -1)
                                  (("1"
                                    (case "s!1`y +
                                                                               
                                                                               
       -(x(s!1) * x(ve!1) + y(s!1) * y(ve!1)) /
                                                                               
                                                                               
        (sq(x(ve!1)) + sq(y(ve!1)))
                                                                               
                                                                               
        * ve!1`y = -ve!1`x*(s!1`x * ve!1`y - s!1`y * ve!1`x) /
                                                                               
                                                                               
      (sq(x(ve!1)) + sq(y(ve!1)))")
                                    (("1" (replace -1 1)
                                      (("1" (hide -1)
                                        (("1"
                                          (lemma "sq_div")
                                          (("1"
                                            (inst
                                             -
                                             "ve!1`y * (s!1`x * ve!1`y - s!1`y 
 * ve!1`x)"
                                             "(sq(x(ve!1)) + sq(y(ve!1)))")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (replace -1 1)
                                                (("1"
                                                  (hide -1)
                                                  (("1"
                                                    (lemma "sq_div")
                                                    (("1"
                                                      (inst
                                                       -
                                                       "(s!1`x * ve!1`y * -ve!1
 `x - s!1`y * ve!1`x * -ve!1`x)"
                                                       "(sq(x(ve!1)) + sq(y(ve!
 1)))")
                                                      (("1"
                                                        (assert)
                                                        (("1"
                                                          (replace -1 1)
                                                          (("1"
                                                            (hide -1)
                                                            (("1"
                                                              (replace -3 1)
                                                              (("1"
                                                                (hide -2 -3)
                                                                (("1"
                                                                  (field 1)
                                                                  (("1"
                                                                    (grind)
                                                                    nil
                                                                    nil)
                                                                   ("2"
                                                                    (reveal
                                                                     -1
                                                                     -2)
                                                                    (("2"
                                                                      (hide -3)
                                                                      (("2"
                                                                        (replac
 e
  
                                                                         -2)
                                                                        (("2"
                                                                          (hide
                                                                           -2)
                                                                          (("2"
                                                                            (ex
 pand
                                                                             "s
 q")
                                                                            (("
 2"
                                                                              (
 assert)
                                                                              n
 il
                                                                              n
 il))
                                                                            nil
 ))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil)
                                                                   ("3"
                                                                    (name
                                                                     "sqxy"
                                                                     "(sq(x(ve!
 1)) + sq(y(ve!1)))")
                                                                    (("3"
                                                                      (replace
  
                                                                       -1)
                                                                      (("3"
                                                                        (hide
                                                                         -1)
                                                                        (("3"
                                                                          (expa
 nd
                                                                           "sq"
 )
                                                                          (("3"
                                                                            (as
 sert)
                                                                            (("
 3"
                                                                              (
 mult-cases
                                                                               
 -1)
                                                                              n
 il
                                                                              n
 il))
                                                                            nil
 ))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2" (hide-all-but (-1 1))
                                      (("2"
                                        (mult-by
                                         1
                                         "(sq(x(ve!1)) + sq(y(ve!1)))")
                                        (("2"
                                          (field 1)
                                          (("2"
                                            (expand "sq")
                                            (("2" (real-props 1) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("2" (hide-all-but (-1 1))
                                (("2" (mult-by 1 "(sq(x(ve!1)) + sq(y(ve!1)))")
                                  (("2" (field 1)
                                    (("2" (expand "sq") (("2" (propax) nil nil)
 )
                                      nil))
                                    nil))
                                  nil))
                                nil)
                               ("3" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (expand "at")
                      (("2" (expand "+ ")
                        (("2" (expand "*")
                          (("2" (expand "tau")
                            (("2" (factor 1 l (3 4))
                              (("1" (move-terms 1 l (2 3))
                                (("1"
                                  (case "(ve!1`x * x(ve!1) + ve!1`y * y(ve!1)) 
 = (sq(x(ve!1)) + sq(y(ve!1)))")
                                  (("1" (replace -1 1) (("1" (field 1) nil nil)
 )
                                    nil)
                                   ("2" (hide-all-but 1)
                                    (("2" (expand "sq") (("2" (propax) nil nil)
 )
                                      nil))
                                    nil))
                                  nil)
                                 ("2" (assert) nil nil))
                                nil)
                               ("2" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (propax) nil nil))
          nil))
        nil))
      nil)
     proved
     ((hor_speed_gt_0? const-decl "bool" criteria nil)
      (tan_condition? const-decl "bool" criteria nil)
      (both_sides_div1 formula-decl nil real_props nil)
      (nonzero_real nonempty-type-eq-decl nil reals nil)
      (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (ve!1 skolem-const-decl "Vect3" criteria nil)
      (/= const-decl "boolean" notequal nil)
      (times_div_cancel2 formula-decl nil extra_real_props "Manip/")
      (tau const-decl "real" criteria nil) (* const-decl "Vect3" Vectors nil)
      (zero_times3 formula-decl nil real_props nil)
      (mult_neg formula-decl nil extra_tegies "Field/")
      (X33__ skolem-const-decl "nonneg_real" criteria nil)
      (nonzero_times3 formula-decl nil real_props nil)
      (X31__ skolem-const-decl "nnreal" criteria nil)
      (X32__ skolem-const-decl "nonneg_real" criteria nil)
      (both_sides_times1 formula-decl nil real_props nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (nnreal type-eq-decl nil real_types nil) (sq_div formula-decl nil sq nil)
      (div_cancel2 formula-decl nil real_props nil)
      (- const-decl "[numfield -> numfield]" number_fields nil)
      (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
      (nznum nonempty-type-eq-decl nil number_fields nil)
      (+ const-decl "Vect3" Vectors nil) (at const-decl "Vect3" criteria nil)
      (tangent_point? const-decl "bool" criteria nil)
      (D const-decl "posreal" criteria nil)
      (posreal nonempty-type-eq-decl nil real_types nil)
      (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (= const-decl "[T, T -> boolean]" equalities 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)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (>= const-decl "bool" reals nil)
      (nonneg_real nonempty-type-eq-decl nil real_types nil)
      (sq const-decl "nonneg_real" sq nil) (Vect3 type-eq-decl nil Vectors nil)
 )
     605975 75610 t nil))
   (line_case_correctness 0
    (line_case_correctness-1 nil 3287830556 3287831773
     ("" (expand "separation?")
      (("" (skosimp*)
        (("" (hide 2)
          (("" (expand "tangent_point?")
            (("" (flatten)
              (("" (lemma "hor_pass_criterion")
                (("" (inst?)
                  (("" (expand "hor_sep?")
                    (("" (expand "hor_pass?")
                      (("" (case "t!1 >= 0")
                        (("1" (inst - "1") (("1" (assert) nil nil)) nil)
                         ("2" (inst - "-1") (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((tangent_point? const-decl "bool" criteria nil)
      (hor_pass_criterion formula-decl nil criteria nil)
      (hor_sep? const-decl "bool" criteria nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (>= const-decl "bool" reals nil) (Sign type-eq-decl nil sign nil)
      (- 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)
      (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)
      (hor_pass? const-decl "bool" criteria 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)
      (Vect3 type-eq-decl nil Vectors nil)
      (real nonempty-type-from-decl nil reals nil)
      (separation? const-decl "bool" criteria nil))
     381 360 nil nil))
   (circle_case_correctness 0
    (circle_case_correctness-1 nil 3287830556 3287831773
     ("" (expand "separation?")
      (("" (skosimp*)
        (("" (prop)
          (("1" (case "t!1 >= 0")
            (("1" (lemma "vert_pass_criterion")
              (("1" (inst?) (("1" (inst - "1") (("1" (assert) nil nil)) nil))
                nil))
              nil)
             ("2" (lemma "hor_pass_criterion")
              (("2" (inst?) (("2" (inst - "-1") (("2" (assert) nil nil)) nil))
                nil))
              nil))
            nil)
           ("2" (case "t!1 >= 0")
            (("1" (lemma "hor_pass_criterion")
              (("1" (inst?) (("1" (inst - "1") (("1" (assert) nil nil)) nil))
                nil))
              nil)
             ("2" (lemma "vert_pass_criterion")
              (("2" (inst?) (("2" (inst - "-1") (("2" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((>= const-decl "bool" reals nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (Vect3 type-eq-decl nil Vectors nil) (Sign type-eq-decl nil sign nil)
      (- 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)
      (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)
      (vert_pass_criterion formula-decl nil criteria nil)
      (hor_pass_criterion formula-decl nil criteria nil)
      (separation? const-decl "bool" criteria nil))
     332 260 nil nil))
   (separation_lem 0
    (separation_lem-1 nil 3287830556 3287831773
     ("" (skosimp*)
      (("" (prop)
        (("1" (expand "separation?")
          (("1" (skosimp*)
            (("1" (inst -1 "t!1+t!2")
              (("1"
                (case "s!1 + (t!1 + t!2) * v!1 = s!1 + t!1 * v!1 + t!2 * v!1")
                (("1" (replace*) nil nil)
                 ("2" (hide-all-but 1) (("2" (expand* "+" "-" "*") nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (expand "separation?")
          (("2" (skosimp*)
            (("2" (inst -1 "t!2-t!1")
              (("2"
                (case "s!1 + t!1 * v!1 + (t!2 - t!1) * v!1 = s!1 + t!2 * v!1")
                (("1" (replace*) nil nil)
                 ("2" (hide-all-but 1) (("2" (expand* "+" "-" "*") nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((* const-decl "Vect3" Vectors nil) (+ const-decl "Vect3" Vectors nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (Vect3 type-eq-decl nil Vectors nil)
      (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (numfield nonempty-type-eq-decl nil number_fields 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)
      (separation? const-decl "bool" criteria nil)
      (- const-decl "[numfield, numfield -> numfield]" number_fields nil))
     369 340 nil nil))
   (ccc 0
    (ccc-1 nil 3287830556 3287831774
     ("" (skosimp*)
      (("" (lemma "circle_case_correctness")
        (("" (inst?)
          (("" (assert) (("" (hide 2) (("" (grind) nil nil)) nil)) nil)) nil))
        nil))
      nil)
     proved
     ((circle_case_correctness formula-decl nil criteria nil)
      (vert_pass? const-decl "bool" criteria nil)
      (hor_pass? const-decl "bool" criteria nil)
      (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil)
      (sq const-decl "nonneg_real" sq nil)
      (on_cyl? const-decl "bool" criteria nil)
      (entry? const-decl "bool" criteria nil)
      (entry_point? const-decl "bool" criteria nil)
      (exit? const-decl "bool" criteria nil)
      (exit_point? const-decl "bool" criteria nil)
      (vert_sep? const-decl "bool" criteria nil)
      (hor_sep? const-decl "bool" criteria nil)
      (Vect3 type-eq-decl nil Vectors nil)
      (real nonempty-type-from-decl nil reals nil))
     555 550 nil nil))
   (vertical_criterion_sz_vz_ge_0 0
    (vertical_criterion_sz_vz_ge_0-1 nil 3287830556 3287831785
     ("" (skolem 1 ("s" "v"))
      (("" (flatten)
        (("" (skolem 1 "T")
          (("" (typepred "T")
            (("" (expand "vert_sep?")
              (("" (expand* "+" "*")
                (("" (expand "abs")
                  (("" (lift-if)
                    (("" (real-props)
                      (("" (ground)
                        (("1" (replaces -5 :dir rl)
                          (("1" (both-sides "+" "s`z")
                            (("1" (real-props) (("1" (neg-formula 1) nil nil))
                              nil))
                            nil))
                          nil)
                         ("2" (hide 2)
                          (("2" (case " T * v`z <= 0")
                            (("1" (assert) nil nil)
                             ("2" (hide 2) (("2" (real-props) nil nil)) nil))
                            nil))
                          nil)
                         ("3" (replaces -4 :dir rl)
                          (("3" (case " T * v`z >= 0")
                            (("1" (assert) nil nil) ("2" (real-props) nil nil))
                            nil))
                          nil)
                         ("4" (replaces -3 :dir rl)
                          (("4" (both-sides "-" "s`z" 2)
                            (("4" (real-props) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((>= const-decl "bool" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (number nonempty-type-decl nil numbers nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (* const-decl "Vect3" Vectors nil) (+ const-decl "Vect3" Vectors nil)
      (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (Vect3 type-eq-decl nil Vectors nil)
      (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (- const-decl "[numfield -> numfield]" number_fields nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (both_sides_plus_ge1 formula-decl nil real_props nil)
      (negreal nonempty-type-eq-decl nil real_types nil)
      (< const-decl "bool" reals nil)
      (nonpos_real nonempty-type-eq-decl nil real_types nil)
      (<= const-decl "bool" reals nil)
      (both_sides_times_neg_ge1 formula-decl nil real_props nil)
      (neg_times_ge formula-decl nil real_props nil)
      (neg_neg formula-decl nil extra_tegies "Field/")
      (mult_neg formula-decl nil extra_tegies "Field/")
      (zero_is_neg_zero formula-decl nil real_props nil)
      (one_times formula-decl nil extra_tegies "Field/")
      (neg_mult formula-decl nil extra_tegies "Field/")
      (add_neg formula-decl nil extra_tegies "Field/")
      (neg_times_le formula-decl nil real_props nil)
      (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (both_sides_plus_ge2 formula-decl nil real_props nil)
      (both_sides_minus_ge1 formula-decl nil real_props nil)
      (pos_times_ge formula-decl nil real_props nil)
      (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil)
      (vert_sep? const-decl "bool" criteria nil))
     11339 8570 nil nil))
   (vertical_criterion_sz_vz_le_0 0
    (vertical_criterion_sz_vz_le_0-1 nil 3287830556 3287831785
     ("" (skolem 1 ("s" "v"))
      (("" (flatten)
        (("" (lemma "vertical_criterion_sz_vz_ge_0")
          (("" (inst -1 "s" "v WITH [z := -v`z]")
            (("" (split -1)
              (("1" (skolem 1 "T")
                (("1" (inst -1 "-T")
                  (("1" (expand "vert_sep?")
                    (("1" (expand* "+" "*") (("1" (assert) nil nil)) nil)) nil)
 )
                  nil))
                nil)
               ("2" (propax) nil nil)
               ("3" (hide -1 2) (("3" (grind) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((real nonempty-type-from-decl nil reals nil)
      (Vect3 type-eq-decl nil Vectors 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)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (- const-decl "[numfield -> numfield]" number_fields nil)
      (vert_sep? const-decl "bool" criteria nil)
      (+ const-decl "Vect3" Vectors nil) (* const-decl "Vect3" Vectors nil)
      (<= const-decl "bool" reals 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)
      (vertical_criterion_sz_vz_ge_0 formula-decl nil criteria nil))
     206 180 nil nil)))
  
  
  $$$common_defs.pvs
  common_defs: THEORY
  BEGIN
     
  
    IMPORTING criteria, sign
  
    l,r,b,c : VAR real
    a   : VAR nonzero_real
    so  : VAR Vect3 % Ownship position
    vo  : VAR Vect3 % Ownship velocity
    tt  : VAR real    % Target time
    st  : VAR Vect3 % Target position
    si  : VAR Vect3 % Intruder position
    vi  : VAR Vect3 % Intruder velocity
    te  : VAR real  % Escape time
    voe : VAR Vect3 % Escape velocity
    tr  : VAR real  % Recovery time
    vor : VAR Vect3 % Recovery velocity
    s   : VAR Vect3 % Relative ownship position
    v   : VAR Vect3 % Relative ownship velocity
    ve  : VAR Vect3 % Relative escape velocity
    vr  : VAR Vect3 % Relative recovery velocity
  
    sr  : VAR Vect3 % Relative final position
  
  
    eps : VAR Sign
    p: VAR Vect3
    t, t1, t2, t3 : VAR real
    v1, v2 : VAR Vect3
  
  
  
    disc(s,v) : real =   %% FORMULA (4.3) * 4
      4 * sq(D) * (sq(v`x) + sq(v`y)) - 4 * sq(s`x * v`y - s`y * v`x)
  
    pred_sep?(s,v,t2) : bool =          % predicted separation until time t2
      FORALL t: 0 <= t AND t <= t2 => hor_sep?(s+t*v) OR vert_sep?(s+t*v)
  
  
    THETA_defined?(s,v): bool = hor_speed_gt_0?(v) AND disc(s,v) >= 0
  
    clash_type(s): TYPE = {v: Vect3 | THETA_defined?(s,v)}
  
    THETA(s: Vect3, v: clash_type(s), eps) : real =
      (-2*s`x*v`x - 2*s`y*v`y + eps * sqrt(disc(s,v))) / (2*sq(v`x)+2*sq(v`y))
  
  
  % Types of maneuver
  
    vertical_change?(vo,voe) : bool =  voe`x = vo`x AND voe`y = vo`y
  
    scale: VAR real
    ground_speed_only_absolute?(ve, scale, vo, vi): bool =
        scale > 0
        AND ve`x = scale * vo`x - vi`x 
        AND ve`y = scale * vo`y - vi`y 
        AND ve`z = vo`z - vi`z
  
  
    ground_speed_only?(voe, vo, vi): bool = 
       LET ve = voe - vi IN
         (EXISTS scale: 
            ground_speed_only_absolute?(ve, scale, vo, vi))
  
    heading_only?(vo,voe): bool =
        sq(voe`x) + sq(voe`y) = sq(vo`x) + sq(vo`y) AND
        voe`z = vo`z
  
  
    %
    % Algorithm Solution Type
    %
  
    solution : TYPE = [# ve: Vect3, vr:Vect3, te:real #]
  
  
  END common_defs
  
  
  
  $$$common_defs.prf
  (common_defs
   (disc_char_TCC1 0
    (disc_char_TCC1-1 nil 3287832816 3287854642 ("" (subtype-tcc) nil nil)
     proved
     ((sq const-decl "nonneg_real" sq "reals/")
      (hor_speed_gt_0? const-decl "bool" criteria nil))
     101 60 nil nil))
   (disc_char 0
    (disc_char-1 nil 3287832816 3287854643
     ("" (skosimp*)
      (("" (expand "hor_speed_gt_0?")
        (("" (expand "discr")
          (("" (expand "disc") (("" (expand "sq") (("" (propax) nil nil)) nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((hor_speed_gt_0? const-decl "bool" criteria nil)
      (disc const-decl "real" common_defs nil)
      (sq const-decl "nonneg_real" sq "reals/")
      (discr const-decl "real" quadratic "reals/"))
     533 470 nil nil))
   (hor_speed_lem 0
    (hor_speed_lem-1 nil 3287832816 3287854643
     ("" (skosimp*)
      (("" (expand "disc")
        (("" (expand "hor_speed_gt_0?") (("" (assert) nil nil)) nil)) nil))
      nil)
     proved
     ((disc const-decl "real" common_defs nil)
      (hor_speed_gt_0? const-decl "bool" criteria nil))
     314 290 nil nil))
   (THETA_TCC1 0
    (THETA_TCC1-1 nil 3287832816 3287854644 ("" (subtype-tcc) nil nil) proved
     ((hor_speed_gt_0? const-decl "bool" criteria nil)
      (clash_type type-eq-decl nil common_defs nil)
      (THETA_defined? const-decl "bool" common_defs nil)
      (Vect3 type-eq-decl nil Vectors nil) (Sign type-eq-decl nil sign nil)
      (- const-decl "[numfield -> numfield]" number_fields nil)
      (numfield nonempty-type-eq-decl nil number_fields 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)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (number nonempty-type-decl nil numbers nil)
      (OR const-decl "[bool, bool -> bool]" booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (sq const-decl "nonneg_real" sq "reals/")
      (disc const-decl "real" common_defs nil))
     924 880 nil nil))
   (THETA_TCC2 0
    (THETA_TCC2-1 nil 3287832816 3287854645 ("" (subtype-tcc) nil nil) proved
     ((boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (OR const-decl "[bool, bool -> bool]" booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (= const-decl "[T, T -> boolean]" equalities 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)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (int nonempty-type-eq-decl nil integers nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (- const-decl "[numfield -> numfield]" number_fields nil)
      (Sign type-eq-decl nil sign nil) (Vect3 type-eq-decl nil Vectors nil)
      (THETA_defined? const-decl "bool" common_defs nil)
      (clash_type type-eq-decl nil common_defs nil)
      (disc const-decl "real" common_defs nil)
      (hor_speed_gt_0? const-decl "bool" criteria nil)
      (sq const-decl "nonneg_real" sq "reals/"))
     673 660 nil nil))
   (THETA1_char_TCC1 0
    (THETA1_char_TCC1-1 nil 3287832816 3287854645 ("" (subtype-tcc) nil nil)
     proved
     ((sq const-decl "nonneg_real" sq "reals/")
      (disc const-decl "real" common_defs nil)
      (hor_speed_gt_0? const-decl "bool" criteria nil)
      (THETA_defined? const-decl "bool" common_defs nil))
     411 390 nil nil))
   (THETA1_char_TCC2 0
    (THETA1_char_TCC2-1 nil 3287832816 3287854646
     ("" (skosimp*)
      (("" (expand "disc")
        (("" (expand "discr")
          (("" (assert) (("" (expand "sq") (("" (propax) nil nil)) nil)) nil))
          nil))
        nil))
      nil)
     proved
     ((disc const-decl "real" common_defs nil)
      (sq const-decl "nonneg_real" sq "reals/")
      (discr const-decl "real" quadratic "reals/"))
     737 720 t nil))
   (THETA1_char 0
    (THETA1_char-1 nil 3287832816 3287854691
     ("" (skosimp*)
      (("" (expand "THETA")
        (("" (expand "root")
          (("" (rewrite "disc_char")
            (("" (expand "hor_speed_gt_0?") (("" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil)
     proved
     ((THETA const-decl "real" common_defs nil)
      (disc_char formula-decl nil common_defs nil)
      (real nonempty-type-from-decl nil reals nil)
      (Vect3 type-eq-decl nil Vectors nil)
      (hor_speed_gt_0? const-decl "bool" criteria nil)
      (root const-decl "real" quadratic "reals/"))
     7813 1350 t nil))
   (THETA2_char 0
    (THETA2_char-1 nil 3287832816 3287854705
     ("" (skosimp*)
      (("" (expand "THETA")
        (("" (expand "root")
          (("" (rewrite "disc_char")
            (("" (expand "hor_speed_gt_0?") (("" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil)
     proved
     ((THETA const-decl "real" common_defs nil)
      (disc_char formula-decl nil common_defs nil)
      (real nonempty-type-from-decl nil reals nil)
      (Vect3 type-eq-decl nil Vectors nil)
      (hor_speed_gt_0? const-decl "bool" criteria nil)
      (root const-decl "real" quadratic "reals/"))
     9201 1550 t nil))
   (quadr_expr_standard 0
    (quadr_expr_standard-1 nil 3287832816 3287854648
     ("" (skosimp*) (("" (grind :theories "real_props") nil nil)) nil) proved
     ((sq const-decl "nonneg_real" sq "reals/")) 481 450 nil nil))
   (quadr_ineq_standard 0
    (quadr_ineq_standard-1 nil 3287832816 3287854648
     ("" (skosimp*)
      (("" (rewrite "quadr_expr_standard")
        (("" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil))
      nil)
     proved
     ((quadr_expr_standard formula-decl nil common_defs nil)
      (real nonempty-type-from-decl nil reals nil)
      (Vect3 type-eq-decl nil Vectors 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))
     566 550 nil nil))
   (quadr_eq_standard 0
    (quadr_eq_standard-1 nil 3287832816 3287854649
     ("" (skosimp*)
      (("" (rewrite "quadr_expr_standard")
        (("" (grind :theories "real_props") nil nil)) nil))
      nil)
     proved
     ((quadr_expr_standard formula-decl nil common_defs nil)
      (real nonempty-type-from-decl nil reals nil)
      (Vect3 type-eq-decl nil Vectors 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)
      (sq const-decl "nonneg_real" sq "reals/"))
     882 840 nil nil))
   (THETA_main 0
    (THETA_main-1 nil 3287832816 3287854650
     ("" (skosimp*)
      (("" (rewrite "quadr_eq_standard")
        (("" (lemma "quadratic_eq_0")
          ((""
            (inst -1 "(sq(v!1`x) + sq(v!1`y))" "2 * (s!1`x * v!1`x )
                                       + 2 * (s!1`y * v!1`y)"
             "sq(s!1`x) + sq(s!1`y) - sq(D)" "t!1")
            (("1" (case "disc(s!1, v!1) >= 0")
              (("1" (rewrite "THETA1_char")
                (("1" (rewrite "THETA2_char")
                  (("1" (rewrite "disc_char")
                    (("1" (assert)
                      (("1" (replace -2 :hide? t) (("1" (prop) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (hide -1)
                (("2" (assert)
                  (("2" (expand "hor_speed_gt_0?")
                    (("2" (lemma "a_gt_0_discr_ge_0")
                      (("2"
                        (inst - "sq(v!1`x) + sq(v!1`y)"
                         "2 * (s!1`x * v!1`x) + 2 * (s!1`y * v!1`y)"
                         "sq(s!1`x) + sq(s!1`y) - sq(D)" "t!1")
                        (("1" (rewrite "disc_char")
                          (("1" (replace 1 :hide? t) (("1" (assert) nil nil))
                            nil))
                          nil)
                         ("2" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (expand "hor_speed_gt_0?") (("2" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((quadr_eq_standard formula-decl nil common_defs nil)
      (real nonempty-type-from-decl nil reals nil)
      (Vect3 type-eq-decl nil Vectors 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)
      (v!1 skolem-const-decl "Vect3" common_defs nil)
      (sq const-decl "nonneg_real" sq "reals/")
      (nonneg_real nonempty-type-eq-decl nil real_types nil)
      (>= const-decl "bool" reals nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (/= const-decl "boolean" notequal nil)
      (nonzero_real nonempty-type-eq-decl nil reals nil)
      (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (> const-decl "bool" reals nil)
      (posreal nonempty-type-eq-decl nil real_types nil)
      (D const-decl "posreal" criteria nil)
      (hor_speed_gt_0? const-decl "bool" criteria nil)
      (a_gt_0_discr_ge_0 formula-decl nil quadratic "reals/")
      (THETA1_char formula-decl nil common_defs nil)
      (disc_char formula-decl nil common_defs nil)
      (THETA2_char formula-decl nil common_defs nil)
      (disc const-decl "real" common_defs nil)
      (quadratic_eq_0 formula-decl nil quadratic "reals/"))
     1231 1180 nil nil))
   (hor_sep_standard 0
    (hor_sep_standard-1 nil 3287832816 3287854651
     ("" (skosimp*)
      (("" (expand "hor_sep?")
        (("" (expand* "+" "*") (("" (rewrite "quadr_ineq_standard") nil nil))
          nil))
        nil))
      nil)
     proved
     ((hor_sep? const-decl "bool" criteria nil)
      (quadr_ineq_standard formula-decl nil common_defs nil)
      (real nonempty-type-from-decl nil reals nil)
      (Vect3 type-eq-decl nil Vectors 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)
      (+ const-decl "Vect3" Vectors nil) (* const-decl "Vect3" Vectors nil))
     513 470 nil nil))
   (infer_hor_movement 0
    (infer_hor_movement-1 nil 3287832816 3287854651
     ("" (skosimp*)
      (("" (expand "hor_speed_gt_0?")
        (("" (use "sq_plus_eq_0")
          (("" (assert)
            (("" (flatten)
              (("" (expand "hor_sep?")
                (("" (expand* "+" "*") (("" (replace*) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((hor_speed_gt_0? const-decl "bool" criteria nil)
      (hor_sep? const-decl "bool" criteria nil)
      (+ const-decl "Vect3" Vectors nil) (* const-decl "Vect3" Vectors 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)
      (Vect3 type-eq-decl nil Vectors nil)
      (sq_plus_eq_0 formula-decl nil sq "reals/"))
     211 200 nil nil))
   (exploit_hor_conflict 0
    (exploit_hor_conflict-1 nil 3287832816 3287854925
     ("" (skosimp*)
      (("" (use "infer_hor_movement")
        (("" (assert)
          (("" (rewrite "hor_sep_standard")
            (("" (rewrite "disc_char")
              (("" (expand "hor_speed_gt_0?")
                (("" (expand "hor_sep?")
                  (("" (lemma "quadratic_ge_0")
                    (("" (expand "root")
                      ((""
                        (inst - "sq(x(v!1))+sq(y(v!1))"
                         "2*(x(s!1)*x(v!1)+y(s!1)*y(v!1))"
                         "sq(x(s!1)) + sq(y(s!1)) - sq(D)" "t!1")
                        (("1" (replace -1 :hide? t)
                          (("1" (assert)
                            (("1" (lemma "root_eq")
                              (("1" (inst?)
                                (("1"
                                  (case "discr(sq(x(v!1)) + sq(y(v!1)),
                                2 * (x(s!1) * x(v!1)) + 2 * (y(s!1) * y(v!1)),
                                sq(x(s!1)) + sq(y(s!1)) - sq(D)) = 0")
                                  (("1" (replace*)
                                    (("1" (assert)
                                      (("1" (flatten) (("1" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((infer_hor_movement formula-decl nil common_defs 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)
      (Vect3 type-eq-decl nil Vectors nil)
      (real nonempty-type-from-decl nil reals nil)
      (hor_sep_standard formula-decl nil common_defs nil)
      (hor_speed_gt_0? const-decl "bool" criteria nil)
      (quadratic_ge_0 formula-decl nil quadratic "reals/")
      (v!1 skolem-const-decl "Vect3" common_defs nil)
      (sq const-decl "nonneg_real" sq "reals/")
      (nonneg_real nonempty-type-eq-decl nil real_types nil)
      (>= const-decl "bool" reals nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (/= const-decl "boolean" notequal nil)
      (nonzero_real nonempty-type-eq-decl nil reals nil)
      (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (> const-decl "bool" reals nil)
      (posreal nonempty-type-eq-decl nil real_types nil)
      (D const-decl "posreal" criteria nil)
      (sqrt_0 formula-decl nil sqrt "reals/")
      (discr const-decl "real" quadratic "reals/")
      (= const-decl "[T, T -> boolean]" equalities nil)
      (root_eq formula-decl nil quadratic "reals/")
      (root const-decl "real" quadratic "reals/")
      (hor_sep? const-decl "bool" criteria nil)
      (disc_char formula-decl nil common_defs nil))
     201706 5090 t nil))
   (hor_sep_char_TCC1 0
    (hor_sep_char_TCC1-1 nil 3287832816 3287854652
     ("" (skosimp*) (("" (expand "THETA_defined?") (("" (assert) nil nil)) nil)
 )
      nil)
     proved ((THETA_defined? const-decl "bool" common_defs nil)) 16 20 nil nil)
 )
   (hor_sep_char 0
    (hor_sep_char-1 nil 3287832816 3287854653
     ("" (skosimp*)
      (("" (case "hor_speed_gt_0?(v!1) AND disc(s!1,v!1) > 0")
        (("1" (flatten)
          (("1" (assert)
            (("1" (rewrite "THETA1_char")
              (("1" (rewrite "THETA2_char")
                (("1" (rewrite "hor_sep_standard")
                  (("1" (lemma "quadratic_ge_0")
                    (("1"
                      (inst - "sq(x(v!1))+sq(y(v!1))"
                       "2*(x(s!1)*x(v!1)+y(s!1)*y(v!1))"
                       "sq(x(s!1)) + sq(y(s!1)) - sq(D)" "t!1")
                      (("1" (replace -1 :hide? t)
                        (("1" (rewrite "disc_char")
                          (("1" (expand "hor_sep?")
                            (("1" (expand "hor_speed_gt_0?")
                              (("1" (assert) (("1" (prop) nil nil)) nil)) nil))
                            nil))
                          nil))
                        nil)
                       ("2" (expand "hor_speed_gt_0?") (("2" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (case "hor_sep?(s!1 + t!1 * v!1)")
          (("1" (replace -1 :hide? t)
            (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil))
            nil)
           ("2" (hide 3)
            (("2" (use "infer_hor_movement")
              (("2" (prop)
                (("2" (use "exploit_hor_conflict") (("2" (prop) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((disc const-decl "real" common_defs nil) (> const-decl "bool" reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (number nonempty-type-decl nil numbers nil)
      (hor_speed_gt_0? const-decl "bool" criteria nil)
      (Vect3 type-eq-decl nil Vectors nil)
      (real nonempty-type-from-decl nil reals nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (THETA2_char formula-decl nil common_defs nil)
      (quadratic_ge_0 formula-decl nil quadratic "reals/")
      (hor_sep? const-decl "bool" criteria nil)
      (disc_char formula-decl nil common_defs nil)
      (D const-decl "posreal" criteria nil)
      (posreal nonempty-type-eq-decl nil real_types nil)
      (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (nonzero_real nonempty-type-eq-decl nil reals nil)
      (v!1 skolem-const-decl "Vect3" common_defs nil)
      (sq const-decl "nonneg_real" sq "reals/")
      (nonneg_real nonempty-type-eq-decl nil real_types nil)
      (>= const-decl "bool" reals nil)
      (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (/= const-decl "boolean" notequal nil)
      (hor_sep_standard formula-decl nil common_defs nil)
      (THETA1_char formula-decl nil common_defs nil)
      (exploit_hor_conflict formula-decl nil common_defs nil)
      (infer_hor_movement formula-decl nil common_defs nil)
      (* const-decl "Vect3" Vectors nil) (+ const-decl "Vect3" Vectors nil))
     753 690 nil nil))
   (exploit_pred_conflict 0
    (exploit_pred_conflict-1 nil 3287832816 3287854653
     ("" (skosimp*)
      (("" (expand "pred_sep?")
        (("" (skosimp*)
          (("" (hide 2)
            (("" (expand "THETA_defined?")
              (("" (use "infer_hor_movement")
                (("" (use "exploit_hor_conflict") (("" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((pred_sep? const-decl "bool" common_defs nil)
      (infer_hor_movement formula-decl nil common_defs 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)
      (Vect3 type-eq-decl nil Vectors nil)
      (real nonempty-type-from-decl nil reals nil)
      (exploit_hor_conflict formula-decl nil common_defs nil)
      (THETA_defined? const-decl "bool" common_defs nil))
     59 50 nil nil))
   (exploit_pred_conflict2 0
    (exploit_pred_conflict2-1 nil 3287832816 3287854653
     ("" (skosimp*)
      (("" (expand "pred_sep?")
        (("" (skosimp*)
          (("" (hide 2)
            (("" (expand "THETA_defined?")
              (("" (use "infer_hor_movement")
                (("" (use "exploit_hor_conflict") (("" (assert) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((pred_sep? const-decl "bool" common_defs nil)
      (infer_hor_movement formula-decl nil common_defs 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)
      (Vect3 type-eq-decl nil Vectors nil)
      (real nonempty-type-from-decl nil reals nil)
      (exploit_hor_conflict formula-decl nil common_defs nil)
      (THETA_defined? const-decl "bool" common_defs nil))
     54 50 nil nil))
   (sep_connection 0
    (sep_connection-1 nil 3287832816 3287854653
     ("" (skosimp*)
      (("" (expand "pred_sep?")
        (("" (skosimp*)
          (("" (expand "separation?")
            (("" (inst -1 "t!1") (("" (prop) nil nil)) nil)) nil))
          nil))
        nil))
      nil)
     proved
     ((pred_sep? const-decl "bool" common_defs nil)
      (separation? const-decl "bool" criteria 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))
     38 40 nil nil))
   (all_entry_exit 0
    (all_entry_exit-1 nil 3287832816 3287854653
     ("" (skosimp*) (("" (grind) nil nil)) nil) proved
     ((hor_pass? const-decl "bool" criteria nil)) 193 190 nil nil))
   (hor_pass_indeed_TCC1 0
    (hor_pass_indeed_TCC1-1 nil 3287832816 3287854653
     ("" (skosimp*)
      (("" (use "infer_hor_movement")
        (("" (use "exploit_hor_conflict")
          (("" (expand "THETA_defined?") (("" (assert) nil nil)) nil)) nil))
        nil))
      nil)
     proved
     ((infer_hor_movement formula-decl nil common_defs 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)
      (Vect3 type-eq-decl nil Vectors nil)
      (real nonempty-type-from-decl nil reals nil)
      (THETA_defined? const-decl "bool" common_defs nil)
      (exploit_hor_conflict formula-decl nil common_defs nil))
     46 30 nil nil))
   (hor_pass_indeed 0
    (hor_pass_indeed-1 nil 3287832816 3287854655
     ("" (skosimp*)
      (("" (use "infer_hor_movement")
        (("" (use "exploit_hor_conflict")
          (("" (prop)
            (("" (expand "hor_pass?")
              (("" (expand* "+" "*")
                (("" (expand "hor_sep?")
                  ((""
                    (case "s!1`x * v!1`x * eps!1 + s!1`y * v!1`y * eps!1 +
                                                                        v!1`x *
  v!1`x * THETA(s!1, v!1, eps!1) * eps!1
                                                                        + v!1`y
  * v!1`y * THETA(s!1, v!1, eps!1) * eps!1 = s!1`x * v!1`x * eps!1 + s!1`y * v!
 1`y * eps!1 + (2*sq(v!1`x) + 2*sq(v!1`y)) * THETA(s!1, v!1, eps!1) * eps!1/2")
                    (("1" (replace -1 :hide? t)
                      (("1"
                        (case "THETA(s!1, v!1, eps!1) = (-2 * (s!1`x * v!1`x) -
  2 * (s!1`y * v!1`y) +
                          eps!1 * sqrt(disc(s!1, v!1))) / (2 * sq(v!1`x) + 2 * 
 sq(v!1`y))")
                        (("1" (replace -1 :hide? t)
                          (("1" (rewrite "div_cancel1" 2)
                            (("1" (assert)
                              (("1"
                                (case "(-2 * (s!1`x * v!1`x * eps!1) - 2 * (s!1
 `y * v!1`y * eps!1) +
                      sqrt(disc(s!1, v!1)) * eps!1 * eps!1)
                     / 2 = -1 * (s!1`x * v!1`x * eps!1 + s!1`y * v!1`y * eps!1)
  + sqrt(disc(s!1, v!1)) * eps!1 * eps!1 / 2")
                                (("1" (replace -1 :hide? t)
                                  (("1" (assert)
                                    (("1"
                                      (case "sqrt(disc(s!1, v!1)) * eps!1 * eps
 !1 / 2 = sqrt(disc(s!1, v!1)) / 2")
                                      (("1" (replace -1 :hide? t)
                                        (("1" (assert) nil nil)) nil)
                                       ("2" (hide 3)
                                        (("2"
                                          (typepred "eps!1")
                                          (("2"
                                            (split -)
                                            (("1" (assert) nil nil)
                                             ("2" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2" (hide 3) (("2" (mult-by 1 "2") nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (expand "THETA") (("2" (propax) nil nil)) nil)
                         ("3" (assert)
                          (("3" (expand "hor_speed_gt_0?")
                            (("3" (assert) nil nil)) nil))
                          nil)
                         ("4" (assert) nil nil))
                        nil))
                      nil)
                     ("2" (hide 3)
                      (("2" (expand "sq" 1) (("2" (mult-by 1 "2") nil nil))
                        nil))
                      nil)
                     ("3" (expand "THETA_defined?") (("3" (assert) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((infer_hor_movement formula-decl nil common_defs 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)
      (Vect3 type-eq-decl nil Vectors nil)
      (real nonempty-type-from-decl nil reals nil)
      (* const-decl "Vect3" Vectors nil) (+ const-decl "Vect3" Vectors nil)
      (sq const-decl "nonneg_real" sq "reals/")
      (nonneg_real nonempty-type-eq-decl nil real_types nil)
      (>= const-decl "bool" reals nil)
      (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
      (nznum nonempty-type-eq-decl nil number_fields nil)
      (/= const-decl "boolean" notequal nil)
      (THETA const-decl "real" common_defs nil)
      (clash_type type-eq-decl nil common_defs nil)
      (THETA_defined? const-decl "bool" common_defs nil)
      (Sign type-eq-decl nil sign nil)
      (- const-decl "[numfield -> numfield]" number_fields nil)
      (OR const-decl "[bool, bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans 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)
      (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (sqrt const-decl "{nnz | nnz * nnz = nnx}" sqrt "reals/")
      (disc const-decl "real" common_defs nil)
      (nonzero_real nonempty-type-eq-decl nil reals nil)
      (div_cancel1 formula-decl nil real_props nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (div_cancel2 formula-decl nil real_props nil)
      (both_sides_times1 formula-decl nil real_props nil)
      (hor_speed_gt_0? const-decl "bool" criteria nil)
      (v!1 skolem-const-decl "Vect3" common_defs nil)
      (s!1 skolem-const-decl "Vect3" common_defs nil)
      (hor_sep? const-decl "bool" criteria nil)
      (hor_pass? const-decl "bool" criteria nil)
      (exploit_hor_conflict formula-decl nil common_defs nil))
     1865 1750 nil nil))
   (entry_it_is 0
    (entry_it_is-1 nil 3287832816 3287854656
     ("" (skosimp*)
      (("" (lemma "hor_pass_indeed")
        (("" (inst?)
          (("" (assert)
            (("" (expand "entry_point?")
              (("" (expand "entry?")
                (("" (expand "hor_pass?")
                  (("" (assert)
                    (("" (expand "pred_sep?")
                      (("" (skosimp*)
                        (("" (inst?)
                          (("" (assert)
                            (("" (case-replace "t!1 = 0")
                              (("1" (assert)
                                (("1" (hide-all-but (-3 1))
                                  (("1" (grind) nil nil)) nil))
                                nil)
                               ("2" (assert)
                                (("2" (lemma "THETA_main")
                                  (("2" (expand "on_cyl?")
                                    (("2"
                                      (inst -1 "s!1" "THETA(s!1,v!1,-1)" "v!1")
                                      (("2" (assert)
                                        (("2"
                                          (split -1)
                                          (("1"
                                            (assert)
                                            (("1"
                                              (expand "THETA_defined?")
                                              (("1"
                                                (flatten)
                                                (("1"
                                                  (assert)
                                                  (("1"
                                                    (hide -1)
                                                    (("1"
                                                      (hide-all-but (-1 4))
                                                      (("1"
                                                        (grind :exclude "THETA"
 )
                                                        nil
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (expand "THETA_defined?")
                                            (("2" (assert) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((hor_pass_indeed formula-decl nil common_defs nil)
      (entry? const-decl "bool" criteria nil)
      (on_cyl? const-decl "bool" criteria nil)
      (THETA_defined? const-decl "bool" common_defs nil)
      (clash_type type-eq-decl nil common_defs nil)
      (THETA const-decl "real" common_defs nil)
      (THETA_main formula-decl nil common_defs nil)
      (sq const-decl "nonneg_real" sq "reals/")
      (hor_sep? const-decl "bool" criteria nil)
      (* const-decl "Vect3" Vectors nil) (+ const-decl "Vect3" Vectors nil)
      (pred_sep? const-decl "bool" common_defs nil)
      (hor_pass? const-decl "bool" criteria nil)
      (entry_point? const-decl "bool" criteria nil)
      (Vect3 type-eq-decl nil Vectors nil) (Sign type-eq-decl nil sign nil)
      (- 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)
      (bool nonempty-type-eq-decl nil booleans 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)
      (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))
     844 800 nil nil))
   (exit_it_is 0
    (exit_it_is-1 nil 3287832816 3287854657
     ("" (skosimp*)
      (("" (lemma "hor_pass_indeed")
        (("" (inst?)
          (("" (expand "pred_sep?")
            (("" (skosimp*)
              (("" (inst?)
                (("" (assert)
                  (("" (case-replace "t!1 = 0")
                    (("1" (assert)
                      (("1" (hide-all-but (-3 1)) (("1" (grind) nil nil)) nil))
                      nil)
                     ("2" (assert)
                      (("2" (expand "exit_point?")
                        (("2" (expand "exit?")
                          (("2" (expand "hor_pass?")
                            (("2" (assert)
                              (("2" (hide -1)
                                (("2" (lemma "THETA_main")
                                  (("2" (inst?)
                                    (("2" (inst -1 "THETA(s!1, v!1, 1)")
                                      (("2" (expand "THETA_defined?")
                                        (("2"
                                          (flatten)
                                          (("2"
                                            (assert)
                                            (("2"
                                              (hide-all-but (-1 4))
                                              (("2"
                                                (grind :exclude "THETA")
                                                nil
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((hor_pass_indeed formula-decl nil common_defs nil)
      (pred_sep? const-decl "bool" common_defs nil)
      (+ const-decl "Vect3" Vectors nil) (* const-decl "Vect3" Vectors nil)
      (hor_sep? const-decl "bool" criteria nil)
      (sq const-decl "nonneg_real" sq "reals/")
      (exit_point? const-decl "bool" criteria nil)
      (hor_pass? const-decl "bool" criteria nil)
      (on_cyl? const-decl "bool" criteria nil)
      (THETA_defined? const-decl "bool" common_defs nil)
      (clash_type type-eq-decl nil common_defs nil)
      (THETA const-decl "real" common_defs nil)
      (THETA_main formula-decl nil common_defs nil)
      (exit? const-decl "bool" criteria nil)
      (Vect3 type-eq-decl nil Vectors nil) (Sign type-eq-decl nil sign nil)
      (- 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)
      (bool nonempty-type-eq-decl nil booleans 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)
      (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))
     865 810 nil nil))
   (reaching_H 0
    (reaching_H-1 nil 3287832816 3287854657
     ("" (skosimp*) (("" (replaces -2) (("" (field 2) nil nil)) nil)) nil)
     proved nil 263 260 nil nil))
   (vert_ge_H 0
    (vert_ge_H-1 nil 3287832816 3287854659
     ("" (skosimp*)
      (("" (replaces -1)
        (("" (expand* "+" "*")
          (("" (case "v!1`z >= 0")
            (("1" (case "t!1*v!1`z >= 0")
              (("1" (assert) nil nil)
               ("2" (real-props 1) (("2" (ground) nil nil)) nil))
              nil)
             ("2" (case "s!1`z + t!1 * v!1`z >= s!1`z + tr!1 * v!1`z")
              (("1" (assert) nil nil)
               ("2" (hide 3)
                (("2" (real-props) (("2" (cancel-by 1 "v!1`z") nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((Vect3 type-eq-decl nil Vectors nil) (>= const-decl "bool" reals nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (pos_times_ge formula-decl nil real_props nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (> const-decl "bool" reals nil)
      (div_mult_neg_le1 formula-decl nil real_props nil)
      (zero_times1 formula-decl nil real_props nil)
      (div_mult_neg_lt1 formula-decl nil real_props nil)
      (both_sides_times_neg_ge1 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)
      (< const-decl "bool" reals nil)
      (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
      (nznum nonempty-type-eq-decl nil number_fields nil)
      (<= const-decl "bool" reals nil)
      (AND const-decl "[bool, bool -> bool]" booleans nil)
      (CBdiv15__ skolem-const-decl "real" common_defs nil)
      (/= const-decl "boolean" notequal nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (both_sides_plus_ge2 formula-decl nil real_props nil)
      (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (+ const-decl "Vect3" Vectors nil) (* const-decl "Vect3" Vectors nil))
     2204 1930 nil nil))
   (vert_le_neg_H 0
    (vert_le_neg_H-1 nil 3287832816 3287854659
     ("" (skosimp*)
      (("" (lemma "vert_ge_H")
        ((""
          (inst -1 "s!1 WITH [z := -s!1`z]" "sr!1 WITH [z := -sr!1`z]" "t!1"
           "tr!1" "v!1 WITH [z := -v!1`z]")
          (("" (expand* "+" "*")
            (("" (replaces -2)
              (("" (beta)
                (("" (split -1)
                  (("1" (assert) nil nil) ("2" (assert) nil nil)
                   ("3" (assert) nil nil) ("4" (assert) nil nil)
                   ("5" (propax) nil nil) ("6" (propax) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((vert_ge_H formula-decl nil common_defs nil)
      (* const-decl "Vect3" Vectors nil) (+ const-decl "Vect3" Vectors nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (- const-decl "[numfield -> numfield]" number_fields nil)
      (numfield nonempty-type-eq-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)
      (Vect3 type-eq-decl nil Vectors nil)
      (real nonempty-type-from-decl nil reals nil))
     236 210 nil nil))
   (vert_pred 0
    (vert_pred-1 nil 3287832816 3287854660
     ("" (skolem 1 ("s" "sr" "tr" "v"))
      (("" (flatten)
        (("" (expand "pred_sep?")
          (("" (skolem 1 "t")
            (("" (flatten)
              (("" (hide 1)
                (("" (expand "vert_sep?")
                  (("" (split -2)
                    (("1" (flatten)
                      (("1" (lemma "vert_ge_H")
                        (("1" (inst?)
                          (("1" (inst -1 "t")
                            (("1" (expand* "+" "*")
                              (("1" (split -1)
                                (("1" (hide-all-but (-1 1))
                                  (("1" (grind) nil nil)) nil)
                                 ("2" (propax) nil nil) ("3" (propax) nil nil)
                                 ("4" (propax) nil nil) ("5" (propax) nil nil)
                                 ("6" (propax) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (lemma "vert_le_neg_H")
                      (("2" (inst?)
                        (("2" (inst -1 "t")
                          (("2" (split -1)
                            (("1" (hide-all-but (-1 1)) (("1" (grind) nil nil))
                              nil)
                             ("2" (propax) nil nil) ("3" (assert) nil nil)
                             ("4" (assert) nil nil) ("5" (propax) nil nil)
                             ("6" (propax) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((vert_ge_H formula-decl nil common_defs nil)
      (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil)
      (+ const-decl "Vect3" Vectors nil) (* const-decl "Vect3" Vectors 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)
      (Vect3 type-eq-decl nil Vectors nil)
      (real nonempty-type-from-decl nil reals nil)
      (vert_le_neg_H formula-decl nil common_defs nil)
      (vert_sep? const-decl "bool" criteria nil)
      (pred_sep? const-decl "bool" common_defs nil))
     325 260 nil nil))
   (reaching_H_theta 0
    (reaching_H_theta-1 nil 3287832816 3287854660
     ("" (skosimp*)
      (("" (expand "theta")
        (("" (expand "abs")
          (("" (expand "sign")
            (("" (lift-if)
              (("" (lift-if)
                (("" (assert)
                  (("" (lift-if)
                    (("" (assert)
                      (("" (typepred "eps!1")
                        (("" (prop)
                          (("1" (assert) nil nil) ("2" (assert) nil nil)
                           ("3" (assert) nil nil) ("4" (assert) nil nil)
                           ("5" (assert) (("5" (assert) nil nil)) nil)
                           ("6" (assert) nil nil) ("7" (assert) nil nil)
                           ("8" (assert) nil nil) ("9" (assert) nil nil)
                           ("10" (assert) (("10" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((theta const-decl "real" criteria nil) (sign const-decl "Sign" sign nil)
      (Sign type-eq-decl nil sign nil)
      (- const-decl "[numfield -> numfield]" number_fields nil)
      (numfield nonempty-type-eq-decl nil number_fields 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)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (= const-decl "[T, T -> boolean]" equalities nil)
      (number nonempty-type-decl nil numbers nil)
      (OR const-decl "[bool, bool -> bool]" booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil))
     485 460 nil nil))
   (vertical_entry_exit_condition 0
    (vertical_entry_exit_condition-1 nil 3287832816 3287854661
     ("" (skosimp*)
      (("" (typepred "vz!1")
        (("" (flatten)
          (("" (expand "theta")
            ((""
              (case-replace
               "(sign(vz!1) * H * eps!1 - sz!1) / vz!1 * eps!1 * vz!1 * vz!1 = 
 (sign(vz!1) * H * eps!1 - sz!1) * eps!1 * vz!1")
              (("1" (hide -1)
                (("1" (assert)
                  (("1"
                    (case-replace
                     "sign(vz!1) * H * eps!1 * eps!1 * vz!1 = H * abs(vz!1)")
                    (("1" (assert) nil nil)
                     ("2" (hide 2 3)
                      (("2" (typepred "eps!1") (("2" (grind) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (field 1) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((nzreal nonempty-type-eq-decl nil reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (/= const-decl "boolean" notequal nil)
      (number nonempty-type-decl nil numbers nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (boolean nonempty-type-decl nil booleans nil)
      (theta const-decl "real" criteria nil)
      (abs const-decl "{n: nonneg_real | n >= m}" real_defs nil)
      (H const-decl "posreal" criteria nil)
      (posreal nonempty-type-eq-decl nil real_types nil)
      (> const-decl "bool" reals nil)
      (nonneg_real nonempty-type-eq-decl nil real_types nil)
      (>= const-decl "bool" reals nil) (sign const-decl "Sign" sign nil)
      (Sign type-eq-decl nil sign nil)
      (- const-decl "[numfield -> numfield]" number_fields nil)
      (OR const-decl "[bool, bool -> bool]" booleans 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)
      (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
      (nznum nonempty-type-eq-decl nil number_fields nil)
      (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (= const-decl "[T, T -> boolean]" equalities nil))
     515 480 nil nil))
   (timeliness_TCC1 0
    (timeliness_TCC1-1 nil 3287832816 3287854661 ("" (subtype-tcc) nil nil)
     proved
     ((boolean nonempty-type-decl nil booleans nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (NOT const-decl "[bool -> bool]" booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (real nonempty-type-from-decl nil reals nil)
      (/= const-decl "boolean" notequal nil))
     88 70 nil nil))
   (timeliness 0
    (timeliness-1 nil 3287832816 3287854661
     ("" (skosimp*)
      (("" (cross-mult -1) (("" (cross-mult -2) (("" (grind) nil nil)) nil))
        nil))
      nil)
     proved
     ((* const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (Vect3 type-eq-decl nil Vectors nil)
      (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
      (numfield nonempty-type-eq-decl nil number_fields nil)
      (nonzero_real nonempty-type-eq-decl nil reals nil)
      (/= const-decl "boolean" notequal nil)
      (real nonempty-type-from-decl nil reals nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (div_cancel4 formula-decl nil extra_real_props "Manip/")
      (* const-decl "Vect3" Vectors nil) (+ const-decl "Vect3" Vectors nil))
     409 350 nil nil))
   (circle_correctness 0
    (circle_correctness-1 nil 3287832816 3287854662
     ("" (skosimp*)
      (("" (lemma "separation_lem")
        (("" (split)
          (("1" (inst - "s!1" "theta(-1,s!1`z, v!1`z)" "v!1")
            (("1" (assert)
              (("1" (lemma "ccc")
                (("1" (inst - "at(s!1, v!1, theta(-1,s!1`z, v!1`z))" "v!1")
                  (("1" (expand "at")
                    (("1" (expand "+ ")
                      (("1" (expand "*")
                        (("1" (lemma "reaching_H_theta")
                          (("1" (inst - "-1" "s!1`z" "v!1`z")
                            (("1" (assert)
                              (("1" (flatten)
                                (("1" (assert)
                                  (("1" (hide 1)
                                    (("1"
                                      (lemma "vertical_entry_exit_condition")
                                      (("1" (inst?) (("1" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (assert) nil nil))
            nil)
           ("2" (inst - "s!1" "theta(1,s!1`z, v!1`z)" "v!1")
            (("1" (assert)
              (("1" (lemma "ccc")
                (("1" (inst - "at(s!1, v!1, theta(1,s!1`z, v!1`z))" "v!1")
                  (("1" (expand "at")
                    (("1" (expand "+ ")
                      (("1" (expand "*")
                        (("1" (lemma "reaching_H_theta")
                          (("1" (inst - "1" "s!1`z" "v!1`z")
                            (("1" (assert)
                              (("1" (flatten)
                                (("1" (hide 2)
                                  (("1" (hide 2)
                                    (("1"
                                      (lemma "vertical_entry_exit_condition")
                                      (("1" (inst?) (("1" (assert) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil)
             ("2" (assert) nil nil))
            nil))
          nil))
        nil))
      nil)
     proved
     ((separation_lem formula-decl nil criteria nil)
      (v!1 skolem-const-decl "Vect3" common_defs nil)
      (Vect3 type-eq-decl nil Vectors nil)
      (real nonempty-type-from-decl nil reals nil)
      (/= const-decl "boolean" notequal nil)
      (boolean nonempty-type-decl nil booleans nil)
      (number nonempty-type-decl nil numbers nil)
      (number_field_pred const-decl "[number -> boolean]" number_fields nil)
      (number_field nonempty-type-from-decl nil number_fields nil)
      (real_pred const-decl "[number_field -> boolean]" reals nil)
      (rational_pred const-decl "[real -> boolean]" rationals nil)
      (rational nonempty-type-from-decl nil rationals nil)
      (integer_pred const-decl "[rational -> boolean]" integers nil)
      (int nonempty-type-eq-decl nil integers nil)
      (bool nonempty-type-eq-decl nil booleans nil)
      (OR 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)
      (Sign type-eq-decl nil sign nil)
      (nzreal nonempty-type-eq-decl nil reals nil)
      (theta const-decl "real" criteria nil) (ccc formula-decl nil criteria nil
 )
      (* const-decl "Vect3" Vectors nil)
      (vertical_entry_exit_condition formula-decl nil common_defs nil)
      (reaching_H_theta formula-decl nil common_defs nil)
      (+ const-decl "Vect3" Vectors nil) (at const-decl "Vect3" criteria nil))
     861 800 nil nil)))
  
  
  $$$vert_only_algo.pvs
  vert_only_algo: THEORY
  BEGIN
     
  
    IMPORTING 
              common_defs
  
    s   : VAR Vect3 % Relative position
    vo  : VAR Vect3 % Ownship absolute velocity
    vi  : VAR Vect3 % Intruder absolute velocity
    v   : VAR Vect3 % Relative velocity
    ve  : VAR Vect3 % Relative escape velocity
    vr  : VAR Vect3 % Relative recovery velocity
    se  : VAR Vect3 % Relative position at the end of the escape manuver
    sr  : VAR Vect3 % Relative position at the end of the escape manuver,
                    % which is also the final position
  
    tr  : VAR posreal  % Recovery time
    te  : VAR real     % Escape time
    t   : VAR real     % time
  
    vez : VAR real     % escape velocity in vert axis
    vrz : VAR real     % recovery velocity in vert axis
  
    eps : VAR Sign
  
  %
  %
  % ----------------------------------------------------------------
  %                       Algorithm Components
  % ----------------------------------------------------------------
  %
  %
  
  
    form_vert_only(v, vez, vrz, tr) : set[solution] =
      LET
      ve = (# x:= v`x,
              y:= v`y,
              z:= vez #),
      vr = (# x:= v`x,
              y:= v`y,
              z:= vrz #) IN
      IF vez /= vrz AND 0 < tr*(v`z - vrz)/(vez-vrz) 
                    AND tr*(v`z - vrz)/(vez-vrz) < tr
        THEN singleton[solution]((# ve:= ve, vr:= vr, 
                                    te:= tr*(v`z - vrz)/(vez-vrz) #))
        ELSE emptyset[solution]
      ENDIF
  
    vert_in_circle(s, v, tr) : set[solution] =
      LET    
      sr = s + tr*v IN
      IF hor_speed_gt_0?(v) AND disc(s, v) > 0 %AND tr > 0 
        THEN LET
          te = THETA(s, v, -1) IN
          IF 0 < te AND te < tr AND abs(sr`z) >= H
            THEN LET
              vrz = (sign(sr`z)*H - sr`z)/(te-tr),
              vez = (tr*v`z - (tr - te)*vrz)/te IN
              form_vert_only(v, vez, vrz, tr)
            ELSE
              emptyset
          ENDIF
        ELSE 
          emptyset       % should never get here if predicted conflict
      ENDIF
  
  END vert_only_algo
  
  $$$vert_only_algo.prf
  (|vert_only_algo| (|form_vert_only_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|vert_in_circle_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|vert_in_circle_TCC2| "" (SUBTYPE-TCC) NIL NIL)
   (|vert_in_circle_TCC3| "" (SUBTYPE-TCC) NIL NIL)
   (|vert_out_circle_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|vert_out_circle_TCC2| "" (SUBTYPE-TCC) NIL NIL)
   (|vert_out_circle_TCC3| "" (SUBTYPE-TCC) NIL NIL)
   (|vert_one_circle_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|vert_one_circle_TCC2| "" (SUBTYPE-TCC) NIL NIL))
  
  
  --=-ssYXAsWuicxIyTo46Ebj--

How-To-Repeat: 

Fix: 
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools