Impressum nvectors.prf

(nvectors
 (difference_TCC1 0
  (difference_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil) nil
   nil))
 (difference_TCC2 0
  (difference_TCC2-1 nil 3500755723
   ("" (skosimp*)
    (("" (typepred "v!1`seq")
      (("" (inst?) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((= const-decl "[T, T -> boolean]" equalities nil)
    (Vector type-eq-decl nil nvectors nil)
    (> const-decl "bool" reals nil)
    (fseq type-eq-decl nil fseqs_def "structures/")
    (barray type-eq-decl nil fseqs_def "structures/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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)
    (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)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (plus_TCC1 0
  (plus_TCC1-1 nil 3500755723
   ("" (skosimp*)
    (("" (typepred "u!1`seq")
      (("" (inst?)
        (("" (assert)
          (("" (typepred "v!1`seq")
            (("" (inst?) (("" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((= const-decl "[T, T -> boolean]" equalities nil)
    (Vector type-eq-decl nil nvectors nil)
    (> const-decl "bool" reals nil)
    (fseq type-eq-decl nil fseqs_def "structures/")
    (barray type-eq-decl nil fseqs_def "structures/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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)
    (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)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Vect type-eq-decl nil nvectors nil))
   nil))
 (plus_TCC2 0
  (plus_TCC2-1 nil 3500755723 ("" (subtype-tcc) nil nil) nil nil))
 (difference_TCC3 0
  (difference_TCC3-1 nil 3501234730 ("" (subtype-tcc) nil nil)
   ((- const-decl "Vect(v`length)" nvectors nil)) nil))
 (times_TCC1 0
  (times_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil) nil nil))
 (times_TCC2 0
  (times_TCC2-1 nil 3500755723
   ("" (skosimp*)
    (("" (typepred "v!1`seq")
      (("" (inst?) (("" (assert) nil nil)) nil)) nil))
    nil)
   ((= const-decl "[T, T -> boolean]" equalities nil)
    (Vector type-eq-decl nil nvectors nil)
    (> const-decl "bool" reals nil)
    (fseq type-eq-decl nil fseqs_def "structures/")
    (barray type-eq-decl nil fseqs_def "structures/")
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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)
    (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)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   nil))
 (sqv_TCC1 0
  (sqv_TCC1-1 nil 3500755723
   ("" (skosimp*)
    (("" (expand "*")
      (("" (lemma "sigma_ge_0[nat]")
        (("" (inst?) (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((* const-decl "real" nvectors nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (> const-decl "bool" reals nil)
    (Vector type-eq-decl nil nvectors nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T_low type-eq-decl nil sigma "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sigma_ge_0 formula-decl nil sigma "reals/")
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (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)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   nil))
 (sq_TCC1 0
  (sq_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil) nil nil))
 (zero_TCC1 0
  (zero_TCC1-1 nil 3500755723
   ("" (skosimp*)
    (("" (expand "const_seq")
      (("" (expand "norm")
        (("" (expand "sqv")
          (("" (expand "*")
            (("" (lemma "sigma_const")
              (("" (inst?)
                (("" (assert)
                  (("" (replace -1) (("" (assert) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   nil nil))
 (zero_TCC2 0
  (zero_TCC2-1 nil 3501326694
   ("" (skosimp*)
    (("" (assert)
      (("" (expand "norm")
        (("" (expand "sqv")
          (("" (expand "*")
            (("" (rewrite "sqrt_eq_0")
              (("" (lemma "sigma_const")
                (("" (inst?)
                  (("" (assert)
                    (("" (replace -1) (("" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sqv const-decl "nnreal" nvectors nil)
    (sqrt_eq_0 formula-decl nil sqrt "reals/")
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sqrt_0 formula-decl nil sqrt "reals/")
    (int_minus_int_is_int application-judgement "int" integers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma "reals/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (> const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (T_low type-eq-decl nil sigma "reals/")
    (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (int_times_even_is_even application-judgement "even_int" integers
     nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_plus_int_is_int application-judgement "int" integers 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)
    (sigma_const formula-decl nil sigma "reals/")
    (* const-decl "real" nvectors nil)
    (norm const-decl "nnreal" nvectors nil))
   nil))
 (unity_TCC1 0
  (unity_TCC1-1 nil 3500755723
   ("" (skosimp*)
    (("" (expand "zero")
      (("" (expand "norm")
        ((""
          (case "sqv((# length := n!1,
                   seq := (LAMBDA (i: nat): 0) WITH [(i!1) := 1] #)) = 1")
          (("1" (assert)
            (("1" (replace -1) (("1" (assert) nil nil)) nil)) nil)
           ("2" (hide 2)
            (("2" (expand "sqv")
              (("2"
                (case-replace
                 "(# length := n!1, seq := (LAMBDA (i: nat): 0) WITH [(i!1) := 1] #) *
       (# length := n!1, seq := (LAMBDA (i: nat): 0) WITH [(i!1) := 1] #) =
         sigma(0, n!1 - 1,
            LAMBDA (j: nat): (LAMBDA (i: nat): 0) WITH [(i!1) := 1](j))")
                (("1" (hide -1)
                  (("1" (assert)
                    (("1"
                      (case-replace
                       "(LAMBDA (j: nat): (LAMBDA (i: nat): 0) WITH [(i!1) := 1](j)) =
                     (LAMBDA (j: nat): if (j = i!1) then 1 else 0 endif)")
                      (("1" (hide -1)
                        (("1" (lemma "sigma_middle")
                          (("1" (inst?)
                            (("1" (inst - "i!1")
                              (("1"
                                (assert)
                                (("1"
                                  (replace -1)
                                  (("1"
                                    (hide -1)
                                    (("1"
                                      (lemma "sigma_restrict_eq")
                                      (("1"
                                        (inst?)
                                        (("1"
                                          (assert)
                                          (("1"
                                            (inst
                                             -
                                             "(LAMBDA (j: nat): 0)")
                                            (("1"
                                              (assert)
                                              (("1"
                                                (split -1)
                                                (("1"
                                                  (replace -1)
                                                  (("1"
                                                    (rewrite
                                                     "sigma_const")
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (hide -1)
                                                        (("1"
                                                          (lemma
                                                           "sigma_restrict_eq")
                                                          (("1"
                                                            (inst?)
                                                            (("1"
                                                              (inst
                                                               -
                                                               "(LAMBDA (j: nat): 0)")
                                                              (("1"
                                                                (split
                                                                 -1)
                                                                (("1"
                                                                  (assert)
                                                                  (("1"
                                                                    (replace
                                                                     -1)
                                                                    (("1"
                                                                      (hide
                                                                       -1)
                                                                      (("1"
                                                                        (rewrite
                                                                         "sigma_const")
                                                                        nil
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil)
                                                                 ("2"
                                                                  (hide
                                                                   2)
                                                                  (("2"
                                                                    (expand
                                                                     "restrict")
                                                                    (("2"
                                                                      (propax)
                                                                      nil
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (hide 2)
                                                  (("2"
                                                    (expand "restrict")
                                                    (("2"
                                                      (propax)
                                                      nil
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (hide 2)
                        (("2" (apply-extensionality 1 :hide? t)
                          (("2" (lift-if) (("2" (propax) nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide 2)
                  (("2" (expand "*")
                    (("2" (lemma "sigma_restrict_eq")
                      (("2" (inst?)
                        (("2" (assert)
                          (("2" (hide 2)
                            (("2" (expand "restrict")
                              (("2"
                                (apply-extensionality 1 :hide? t)
                                (("2"
                                  (lift-if)
                                  (("2" (ground) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("3" (skosimp*)
            (("3" (hide 2) (("3" (assert) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((zero const-decl "Zero_vect(n)" nvectors nil)
    (below type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (sqv const-decl "nnreal" nvectors nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (Vector type-eq-decl nil nvectors nil)
    (> const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (fseq type-eq-decl nil fseqs_def "structures/")
    (barray type-eq-decl nil fseqs_def "structures/")
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (sqrt_pos application-judgement "posreal" sqrt "reals/")
    (sqrt_1 formula-decl nil sqrt "reals/")
    (odd_times_odd_is_odd application-judgement "odd_int" integers nil)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (sigma_middle formula-decl nil sigma "reals/")
    (sigma_restrict_eq formula-decl nil sigma "reals/")
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (restrict const-decl "[T -> real]" sigma "reals/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (int_times_even_is_even application-judgement "even_int" integers
     nil)
    (sigma_const formula-decl nil sigma "reals/")
    (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/")
    (sigma_nat application-judgement "nat" sigma_nat "reals/")
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (sigma def-decl "real" sigma "reals/")
    (T_high type-eq-decl nil sigma "reals/")
    (T_low type-eq-decl nil sigma "reals/")
    (<= const-decl "bool" reals nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (* const-decl "real" nvectors nil)
    (Vect type-eq-decl nil nvectors nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (norm const-decl "nnreal" nvectors nil))
   nil))
 (const_vec_TCC1 0
  (const_vec_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (const_seq const-decl "fseq" fseqs_def "structures/"))
   nil))
 (comp_distr_add 0
  (comp_distr_add-1 nil 3500783129 ("" (grind) nil nil)
   ((+ const-decl "Vect(u`length)" nvectors nil)) shostak))
 (comp_distr_sub 0
  (comp_distr_sub-1 nil 3500783135 ("" (grind) nil nil)
   ((- const-decl "Vect(v`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
 (comp_distr_scal 0
  (comp_distr_scal-1 nil 3500783142 ("" (grind) nil nil)
   ((* const-decl "Vect(v`length)" nvectors nil)) shostak))
 (comp_zero 0
  (comp_zero-1 nil 3500783145 ("" (grind) nil nil)
   ((zero const-decl "Zero_vect(n)" nvectors nil)) shostak))
 (comp_eq 0
  (comp_eq-1 nil 3500783149
   ("" (skosimp*)
    (("" (prop)
      (("1" (assert) nil nil)
       ("2" (apply-extensionality 1 :hide? t)
        (("2" (apply-extensionality :hide? t)
          (("2" (inst?)
            (("2" (assert)
              (("2" (typepred "w!1`seq")
                (("2" (typepred "u!1`seq")
                  (("2" (inst?)
                    (("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((>= const-decl "bool" reals 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_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (x!1 skolem-const-decl "nat" nvectors nil)
    (u!1 skolem-const-decl "Vector" nvectors nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil naturalnumbers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (> const-decl "bool" reals nil)
    (Vector type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors nil)
    (fseq type-eq-decl nil fseqs_def "structures/")
    (barray type-eq-decl nil fseqs_def "structures/")
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   shostak))
 (add_zero_left_TCC1 0
  (add_zero_left_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((zero const-decl "Zero_vect(n)" nvectors nil)) nil))
 (add_zero_left 0
  (add_zero_left-1 nil 3500783169
   ("" (grind-with-ext :exclude "default")
    (("" (typepred "v!1`seq(x1!1)") (("" (propax) nil nil)) nil)) nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" 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)
    (>= const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (zero const-decl "Zero_vect(n)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil))
   shostak))
 (add_zero_right_TCC1 0
  (add_zero_right_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((zero const-decl "Zero_vect(n)" nvectors nil)) nil))
 (add_zero_right 0
  (add_zero_right-1 nil 3500783182
   ("" (grind-with-ext :exclude "default")
    (("" (typepred "v!1`seq(x1!1)") (("" (propax) nil nil)) nil)) nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" 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)
    (>= const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (zero const-decl "Zero_vect(n)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil))
   shostak))
 (add_comm_TCC1 0
  (add_comm_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil) nil nil))
 (add_comm 0
  (add_comm-1 nil 3500783188 ("" (grind-with-ext) nil nil)
   ((+ const-decl "Vect(u`length)" nvectors nil)) shostak))
 (add_assoc_TCC1 0
  (add_assoc_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil) nil nil))
 (add_assoc_TCC2 0
  (add_assoc_TCC2-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((+ const-decl "Vect(u`length)" nvectors nil)) nil))
 (add_assoc_TCC3 0
  (add_assoc_TCC3-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((+ const-decl "Vect(u`length)" nvectors nil)) nil))
 (add_assoc 0
  (add_assoc-1 nil 3500783193 ("" (grind-with-ext) nil nil)
   ((+ const-decl "Vect(u`length)" nvectors nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   shostak))
 (add_move_right 0
  (add_move_right-1 nil 3500783197
   ("" (skosimp*)
    (("" (prop)
      (("1" (replace -1 * rl)
        (("1" (assert)
          (("1" (hide -1)
            (("1" (apply-extensionality 1 :hide? t)
              (("1" (apply-extensionality 1 :hide? t)
                (("1" (grind)
                  (("1" (typepred "u!1`seq")
                    (("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (replace -1)
        (("2" (assert)
          (("2" (hide -1)
            (("2" (apply-extensionality 1 :hide? t)
              (("2" (apply-extensionality 1 :hide? t)
                (("2" (grind)
                  (("2" (typepred "v!1`seq")
                    (("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nat nonempty-type-eq-decl nil naturalnumbers 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)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (+ const-decl "Vect(u`length)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil)
    (Vect type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vector type-eq-decl nil nvectors nil)
    (> const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (- const-decl "Vect(v`length)" nvectors nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" 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)
    (>= const-decl "bool" reals nil))
   shostak))
 (add_move_both 0
  (add_move_both-1 nil 3500783287
   ("" (skosimp*)
    (("" (prop)
      (("1" (apply-extensionality 1 :hide? t)
        (("1" (apply-extensionality 1 :hide? t)
          (("1" (grind)
            (("1" (typepred "u!1`seq")
              (("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil)
       ("2" (apply-extensionality 1 :hide? t)
        (("2" (apply-extensionality 1 :hide? t)
          (("2" (grind)
            (("2" (typepred "v!1`seq")
              (("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((>= const-decl "bool" reals 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 "Vect(u`length)" nvectors nil)
    (- const-decl "Vect(v`length)" nvectors nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (> const-decl "bool" reals nil)
    (Vector type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil)
    (fseq type-eq-decl nil fseqs_def "structures/")
    (barray type-eq-decl nil fseqs_def "structures/")
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   shostak))
 (add_neg_sub_TCC1 0
  (add_neg_sub_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((- const-decl "Vect(v`length)" nvectors nil)) nil))
 (add_neg_sub 0
  (add_neg_sub-1 nil 3500783295
   ("" (grind-with-ext :exclude "default") nil nil)
   ((- const-decl "Vect(v`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
 (add_cancel_TCC1 0
  (add_cancel_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((+ const-decl "Vect(u`length)" nvectors nil)) nil))
 (add_cancel 0
  (add_cancel-1 nil 3500783299
   ("" (skosimp*)
    (("" (apply-extensionality 1 :hide? t)
      (("" (grind :exclude "default")
        (("" (apply-extensionality 1 :hide? t)
          (("" (lift-if)
            (("" (ground)
              (("" (typepred "w!1`seq")
                (("" (inst?) (("" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nat nonempty-type-eq-decl nil naturalnumbers 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)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (+ const-decl "Vect(u`length)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil)
    (Vect type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (> const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (Vector type-eq-decl nil nvectors nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (>= const-decl "bool" reals 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)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (- const-decl "Vect(v`length)" nvectors nil))
   shostak))
 (add_cancel_neg_TCC1 0
  (add_cancel_neg_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((- const-decl "Vect(v`length)" nvectors nil)) nil))
 (add_cancel_neg_TCC2 0
  (add_cancel_neg_TCC2-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((- const-decl "Vect(v`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil))
   nil))
 (add_cancel_neg 0
  (add_cancel_neg-1 nil 3500783303
   ("" (grind-with-ext :exclude "default")
    (("1" (typepred "w!1`seq")
      (("1" (inst?)
        (("1" (assert)
          (("1" (replace -1) (("1" (propax) nil nil)) nil)) nil))
        nil))
      nil)
     ("2" (typepred "w!1`seq(x1!1)") (("2" (propax) nil nil)) nil))
    nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors 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 "bool" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (- const-decl "Vect(v`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
 (add_cancel2_TCC1 0
  (add_cancel2_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((- const-decl "Vect(v`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil))
   nil))
 (add_cancel2 0
  (add_cancel2-1 nil 3500783307
   ("" (grind-with-ext :exclude "default")
    (("1" (typepred "w!1`seq(x!1)")
      (("1" (typepred "w!1`seq")
        (("1" (inst?)
          (("1" (assert)
            (("1" (replace -1) (("1" (propax) nil nil)) nil)) nil))
          nil))
        nil))
      nil)
     ("2" (typepred "w!1`seq(x1!1)") (("2" (propax) nil nil)) nil))
    nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors 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 "bool" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (- const-decl "Vect(v`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
 (add_cancel_neg2_TCC1 0
  (add_cancel_neg2_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((+ const-decl "Vect(u`length)" nvectors nil)) nil))
 (add_cancel_neg2 0
  (add_cancel_neg2-1 nil 3500783311
   ("" (grind-with-ext :exclude "default")
    (("1" (typepred "w!1`seq")
      (("1" (inst?)
        (("1" (assert)
          (("1" (replace -1) (("1" (propax) nil nil)) nil)) nil))
        nil))
      nil)
     ("2" (typepred "w!1`seq(x1!1)") (("2" (propax) nil nil)) nil))
    nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors 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 "bool" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (- const-decl "Vect(v`length)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
 (sub_zero_left 0
  (sub_zero_left-1 nil 3500783315
   ("" (skosimp*)
    (("" (expand "zero")
      (("" (expand "const_seq")
        (("" (assert)
          (("" (expand "-")
            (("" (expand "+ ")
              (("" (apply-extensionality 1 :hide? t)
                (("" (grind) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((zero const-decl "Zero_vect(n)" nvectors nil)
    (- const-decl "Vect(v`length)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors 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)
    (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)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (Vect type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vector type-eq-decl nil nvectors nil)
    (> const-decl "bool" reals nil)
    (fseq type-eq-decl nil fseqs_def "structures/")
    (barray type-eq-decl nil fseqs_def "structures/")
    (minus_real_is_real application-judgement "real" reals nil)
    (+ const-decl "Vect(u`length)" nvectors nil))
   shostak))
 (sub_zero_right 0
  (sub_zero_right-1 nil 3500783319
   ("" (grind-with-ext :exclude "default")
    (("" (typepred "v!1`seq(x1!1)") (("" (propax) nil nil)) nil)) nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" 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)
    (>= const-decl "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (zero const-decl "Zero_vect(n)" nvectors nil)
    (- const-decl "Vect(v`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil))
   shostak))
 (sub_eq_args 0
  (sub_eq_args-1 nil 3500783323
   ("" (grind-with-ext :exclude "default") nil nil)
   ((- const-decl "Vect(v`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil)
    (zero const-decl "Zero_vect(n)" nvectors nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
 (sub_eq_zero_TCC1 0
  (sub_eq_zero_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil) nil
   nil))
 (sub_eq_zero 0
  (sub_eq_zero-1 nil 3500783328
   ("" (grind-with-ext :exclude "default")
    (("" (decompose-equality)
      (("" (inst?)
        (("" (ground)
          (("" (lift-if)
            (("" (ground)
              (("" (typepred "u!1`seq")
                (("" (typepred "v!1`seq")
                  (("" (inst?)
                    (("" (inst?) (("" (assert) nil nil)) nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((- const-decl "[numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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)
    (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 "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (zero const-decl "Zero_vect(n)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (- const-decl "Vect(v`length)" nvectors nil))
   shostak))
 (sub_cancel_TCC1 0
  (sub_cancel_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((- const-decl "Vect(v`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil))
   nil))
 (sub_cancel 0
  (sub_cancel-1 nil 3500783354
   ("" (grind-with-ext :exclude "default") nil nil)
   ((- const-decl "Vect(v`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
 (sub_cancel_neg_TCC1 0
  (sub_cancel_neg_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((- const-decl "Vect(v`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil))
   nil))
 (sub_cancel_neg 0
  (sub_cancel_neg-1 nil 3500783361
   ("" (grind-with-ext :exclude "default") nil nil)
   ((- const-decl "Vect(v`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
 (neg_add_left_TCC1 0
  (neg_add_left_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((- const-decl "Vect(v`length)" nvectors nil)) nil))
 (neg_add_left 0
  (neg_add_left-1 nil 3500783364
   ("" (grind-with-ext :exclude "default") nil nil)
   ((- const-decl "Vect(v`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (zero const-decl "Zero_vect(n)" nvectors nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
 (neg_add_right 0
  (neg_add_right-1 nil 3500783370
   ("" (grind-with-ext :exclude "default") nil nil)
   ((- const-decl "Vect(v`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (zero const-decl "Zero_vect(n)" nvectors nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
 (neg_distr_sub 0
  (neg_distr_sub-1 nil 3500783373
   ("" (grind-with-ext :exclude "default") nil nil)
   ((- const-decl "Vect(v`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
 (neg_neg 0
  (neg_neg-1 nil 3500783377
   ("" (skosimp*)
    (("" (apply-extensionality 1 :hide? t)
      (("" (apply-extensionality 1 :hide? t)
        (("" (expand "-") (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((nat nonempty-type-eq-decl nil naturalnumbers 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)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (- const-decl "Vect(v`length)" nvectors nil)
    (Vect type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vector type-eq-decl nil nvectors nil)
    (> const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (minus_real_is_real application-judgement "real" 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)
    (>= const-decl "bool" reals nil))
   shostak))
 (neg_distr_add_TCC1 0
  (neg_distr_add_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((- const-decl "Vect(v`length)" nvectors nil)) nil))
 (neg_distr_add 0
  (neg_distr_add-1 nil 3500783381
   ("" (grind-with-ext :exclude "default") nil nil)
   ((+ const-decl "Vect(u`length)" nvectors nil)
    (- const-decl "Vect(v`length)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   shostak))
 (dot_neg_left 0
  (dot_neg_left-1 nil 3500783385
   ("" (skosimp :preds? t)
    (("" (expand "-")
      (("" (expand "*")
        (("" (lemma "sigma_scal[nat]")
          ((""
            (inst -1 "LAMBDA (i_1: nat): -u!1`seq(i_1) * w!1`seq(i_1)"
             "-1" "u!1`length-1" "0")
            (("" (replace -1)
              (("" (assert)
                (("" (hide -1)
                  (("" (lemma "sigma_restrict_eq")
                    (("" (inst?)
                      (("" (assert)
                        ((""
                          (inst -
                           "LAMBDA (i_1: nat): -u!1`seq(i_1) * w!1`seq(i_1)")
                          (("" (assert)
                            (("" (expand "restrict")
                              (("" (propax) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((- const-decl "Vect(v`length)" nvectors nil)
    (sigma_scal formula-decl nil sigma "reals/")
    (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 "bool" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (T_low type-eq-decl nil sigma "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T_high type-eq-decl nil sigma "reals/")
    (<= const-decl "bool" reals nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (* const-decl "real" nvectors 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors nil))
   shostak))
 (dot_neg_right 0
  (dot_neg_right-2 nil 3501260680
   ("" (skosimp :preds? t)
    (("" (expand "-")
      (("" (expand "*")
        (("" (lemma "sigma_scal[nat]")
          ((""
            (inst -1 "LAMBDA (i_1: nat): -u!1`seq(i_1) * w!1`seq(i_1)"
             "-1" "u!1`length-1" "0")
            (("" (replace -1)
              (("" (assert)
                (("" (hide -1)
                  (("" (lemma "sigma_restrict_eq")
                    (("" (inst?)
                      (("" (assert)
                        ((""
                          (inst -
                           "LAMBDA (i_1: nat): -u!1`seq(i_1) * w!1`seq(i_1)")
                          (("" (assert)
                            (("" (expand "restrict")
                              ((""
                                (apply-extensionality 1 :hide? t)
                                ((""
                                  (lift-if)
                                  (("" (ground) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((- const-decl "Vect(v`length)" nvectors nil)
    (sigma_scal formula-decl nil sigma "reals/")
    (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 "bool" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (T_low type-eq-decl nil sigma "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T_high type-eq-decl nil sigma "reals/")
    (<= const-decl "bool" reals nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (* const-decl "real" nvectors 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors nil))
   nil)
  (dot_neg_right-1 nil 3500784674
   ("" (skosimp :preds? t)
    (("" (expand "-")
      (("" (expand "*")
        (("" (expand "fseq_appl")
          (("" (lemma "sigma_scal[nat]")
            ((""
              (inst -1
               "LAMBDA (i_1: nat): u!1`seq(i_1) * -w!1`seq(i_1)" "-1"
               "u!1`length-1" "0")
              (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T_high type-eq-decl nil sigma "reals/")
    (T_low type-eq-decl nil sigma "reals/")
    (sigma_scal formula-decl nil sigma "reals/"))
   shostak))
 (dot_neg_sq 0
  (dot_neg_sq-1 nil 3500784794
   ("" (grind-with-ext :exclude "default")
    (("" (lemma "sigma_restrict_eq")
      (("" (inst?)
        (("" (inst - "(LAMBDA (i: nat): v!1`seq(i) * v!1`seq(i))")
          (("" (assert)
            (("" (expand "restrict")
              (("" (apply-extensionality 1 :hide? t)
                (("" (lift-if)
                  (("" (hide 2) (("" (ground) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((- const-decl "Vect(v`length)" nvectors nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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)
    (sigma def-decl "real" sigma "reals/")
    (* const-decl "real" nvectors nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   shostak))
 (dot_zero_left_TCC1 0
  (dot_zero_left_TCC1-1 nil 3500785044 ("" (subtype-tcc) nil nil)
   ((zero const-decl "Zero_vect(n)" nvectors nil)) nil))
 (dot_zero_left 0
  (dot_zero_left-1 nil 3500784801
   ("" (grind-with-ext :exclude "default")
    (("" (lemma "sigma_restrict_eq")
      (("" (inst?)
        (("" (lemma "sigma_zero[nat]")
          (("" (inst - "v!1`length - 2" "0")
            (("" (inst?)
              (("" (assert)
                (("" (expand "restrict")
                  (("" (apply-extensionality 1 :hide? t)
                    (("" (lift-if) (("" (ground) nil nil)) nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sigma_restrict_eq formula-decl nil sigma "reals/")
    (sigma_zero formula-decl nil sigma "reals/")
    (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/")
    (sigma_nat application-judgement "nat" sigma_nat "reals/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T_low type-eq-decl nil sigma "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Vector type-eq-decl nil nvectors nil)
    (fseq type-eq-decl nil fseqs_def "structures/")
    (barray type-eq-decl nil fseqs_def "structures/")
    (> const-decl "bool" reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (* const-decl "real" nvectors nil)
    (sigma def-decl "real" sigma "reals/")
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (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)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (zero const-decl "Zero_vect(n)" nvectors nil))
   shostak))
 (dot_zero_right 0
  (dot_zero_right-2 nil 3501260122
   ("" (grind-with-ext :exclude "default")
    (("" (lemma "sigma_restrict_eq")
      (("" (inst?)
        (("" (lemma "sigma_zero[nat]")
          (("" (inst - "v!1`length - 2" "0")
            (("" (inst?)
              (("" (assert)
                (("" (expand "restrict") (("" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sigma_restrict_eq formula-decl nil sigma "reals/")
    (sigma_zero formula-decl nil sigma "reals/")
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma "reals/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T_low type-eq-decl nil sigma "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sigma_nat application-judgement "nat" sigma_nat "reals/")
    (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Vector type-eq-decl nil nvectors nil)
    (fseq type-eq-decl nil fseqs_def "structures/")
    (barray type-eq-decl nil fseqs_def "structures/")
    (> const-decl "bool" reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (* const-decl "real" nvectors nil)
    (sigma def-decl "real" sigma "reals/")
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (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)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (zero const-decl "Zero_vect(n)" nvectors nil))
   nil)
  (dot_zero_right-1 nil 3500785150
   ("" (grind-with-ext :exclude "default")
    (("" (use "sigma_zero[nat]") nil nil)) nil)
   ((T_high type-eq-decl nil sigma "reals/")
    (T_low type-eq-decl nil sigma "reals/")
    (sigma_zero formula-decl nil sigma "reals/")
    (sigma def-decl "real" sigma "reals/"))
   shostak))
 (dot_comm 0
  (dot_comm-1 nil 3500785167
   ("" (grind-with-ext :exclude "default")
    (("" (lemma "sigma_eq[nat]")
      ((""
        (inst -1 "LAMBDA (i: nat): u!1`seq(i) * v!1`seq(i)"
         "LAMBDA (i: nat): v!1`seq(i) * u!1`seq(i)" "u!1`length - 2"
         "0")
        (("1" (assert)
          (("1" (assert)
            (("1" (replace -1 :hide? t)
              (("1" (assert)
                (("1" (replace -2 :actuals? t) (("1" (assert) nil nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil))
        nil))
      nil))
    nil)
   ((nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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)
    (sigma def-decl "real" sigma "reals/")
    (* const-decl "real" nvectors nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   shostak))
 (dot_assoc_TCC1 0
  (dot_assoc_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((* const-decl "Vect(v`length)" nvectors nil)) nil))
 (dot_assoc 0
  (dot_assoc-1 nil 3500785460
   ("" (grind-with-ext :exclude "default")
    (("" (use "sigma_scal[nat]") (("" (assert) nil nil)) nil)) nil)
   ((sigma_scal formula-decl nil sigma "reals/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T_low type-eq-decl nil sigma "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Vect type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vector type-eq-decl nil nvectors nil)
    (fseq type-eq-decl nil fseqs_def "structures/")
    (barray type-eq-decl nil fseqs_def "structures/")
    (> const-decl "bool" reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (* const-decl "Vect(v`length)" nvectors nil)
    (* const-decl "real" nvectors nil)
    (sigma def-decl "real" sigma "reals/")
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (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)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   shostak))
 (dot_eq_args_ge 0
  (dot_eq_args_ge-1 nil 3500785551
   ("" (grind-with-ext :exclude "default")
    (("" (use "sigma_ge_0[nat]")
      (("" (prop)
        (("1" (assert) nil nil)
         ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil))
        nil))
      nil))
    nil)
   ((sigma_ge_0 formula-decl nil sigma "reals/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T_low type-eq-decl nil sigma "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Vector type-eq-decl nil nvectors nil)
    (fseq type-eq-decl nil fseqs_def "structures/")
    (barray type-eq-decl nil fseqs_def "structures/")
    (> const-decl "bool" reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (* const-decl "real" nvectors nil)
    (sigma def-decl "real" sigma "reals/")
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (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)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   shostak))
 (dot_distr_add_left 0
  (dot_distr_add_left-1 nil 3500785603
   ("" (grind-with-ext :exclude "default")
    (("" (use "sigma_sum[nat]") (("" (assert) nil nil)) nil)) nil)
   ((sigma_sum formula-decl nil sigma "reals/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T_low type-eq-decl nil sigma "reals/")
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (Vect type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vector type-eq-decl nil nvectors nil)
    (fseq type-eq-decl nil fseqs_def "structures/")
    (barray type-eq-decl nil fseqs_def "structures/")
    (> const-decl "bool" reals nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (* const-decl "real" nvectors nil)
    (sigma def-decl "real" sigma "reals/")
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (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)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (+ const-decl "Vect(u`length)" nvectors nil))
   shostak))
 (dot_distr_add_right_TCC1 0
  (dot_distr_add_right_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((+ const-decl "Vect(u`length)" nvectors nil)) nil))
 (dot_distr_add_right_TCC2 0
  (dot_distr_add_right_TCC2-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   nil nil))
 (dot_distr_add_right 0
  (dot_distr_add_right-1 nil 3500785664
   ("" (skosimp :preds? t)
    (("" (expand "+")
      (("" (expand "*")
        (("" (expand "fseq_appl")
          (("" (replace -3 :actuals? t)
            (("" (replace -5 :actuals? t)
              (("" (use "sigma_sum[nat]")
                (("1" (assert)
                  (("1" (replace -1 :hide? t)
                    (("1" (use "sigma_eq[nat]")
                      (("1" (prop)
                        (("1" (hide-all-but 1) (("1" (grind) nil nil))
                          nil))
                        nil)
                       ("2" (hide-all-but 1) (("2" (grind) nil nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)
                 ("3" (hide-all-but 1) (("3" (grind) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((+ const-decl "Vect(u`length)" nvectors nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (>= const-decl "bool" reals 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)
    (sigma_sum formula-decl nil sigma "reals/")
    (T_low type-eq-decl nil sigma "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T_high type-eq-decl nil sigma "reals/")
    (<= const-decl "bool" reals nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (* const-decl "real" nvectors 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors nil))
   shostak))
 (dot_distr_sub_left_TCC1 0
  (dot_distr_sub_left_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((- const-decl "Vect(v`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil))
   nil))
 (dot_distr_sub_left 0
  (dot_distr_sub_left-1 nil 3500785912
   ("" (skosimp :preds? t)
    (("" (expand "-")
      (("" (expand "*")
        (("" (replace -3 :actuals? t)
          (("" (replace -5 :actuals? t)
            (("" (hide-all-but 1)
              (("" (expand "fseq_appl")
                (("" (use "sigma_minus[nat]")
                  (("" (replace -1 :hide? t)
                    (("" (use "sigma_eq[nat]")
                      (("1" (prop)
                        (("1" (hide-all-but 1) (("1" (grind) nil nil))
                          nil))
                        nil)
                       ("2" (hide-all-but 1) (("2" (grind) nil nil))
                        nil)
                       ("3" (hide-all-but 1) (("3" (grind) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((- const-decl "Vect(u`length)" nvectors nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "Vect(v`length)" nvectors nil)
    (u!1 skolem-const-decl "Vector" nvectors nil)
    (w!1 skolem-const-decl "Vect(u!1`length)" nvectors nil)
    (v!1 skolem-const-decl "Vect(u!1`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (sigma_eq formula-decl nil sigma "reals/")
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T_low type-eq-decl nil sigma "reals/")
    (sigma_minus formula-decl nil sigma "reals/")
    (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 "bool" reals nil) (* const-decl "real" nvectors 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors nil))
   shostak))
 (dot_distr_sub_right_TCC1 0
  (dot_distr_sub_right_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((- const-decl "Vect(v`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil))
   nil))
 (dot_distr_sub_right 0
  (dot_distr_sub_right-1 nil 3500786067
   ("" (skosimp :preds? t)
    (("" (expand "-")
      (("" (expand "-")
        (("" (expand "+")
          (("" (expand "*")
            (("" (expand "fseq_appl")
              (("" (replace -3 :actuals? t)
                (("" (replace -5 :actuals? t)
                  (("" (hide-all-but 1)
                    (("" (use "sigma_minus[nat]")
                      (("1" (replace -1 :hide? t)
                        (("1" (use "sigma_eq[nat]")
                          (("1" (prop)
                            (("1" (hide-all-but 1)
                              (("1" (grind) nil nil)) nil))
                            nil)
                           ("2" (hide-all-but 1)
                            (("2" (grind) nil nil)) nil))
                          nil))
                        nil)
                       ("2" (hide-all-but 1) (("2" (grind) nil nil))
                        nil)
                       ("3" (hide-all-but 1) (("3" (grind) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((- const-decl "Vect(u`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sigma_eq formula-decl nil sigma "reals/")
    (int_minus_int_is_int application-judgement "int" integers nil)
    (T_low type-eq-decl nil sigma "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T_high type-eq-decl nil sigma "reals/")
    (<= const-decl "bool" reals nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (sigma_minus formula-decl nil sigma "reals/")
    (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 "bool" reals nil) (* const-decl "real" nvectors nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "Vect(v`length)" nvectors 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors nil))
   shostak))
 (dot_divby 0
  (dot_divby-1 nil 3500786326
   ("" (skosimp :preds? t)
    (("" (apply-extensionality 2 :hide? t)
      (("" (expand "*")
        (("" (decompose-equality)
          (("" (decompose-equality)
            (("" (expand "fseq_appl")
              (("" (inst?) (("" (assert) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_times_real_is_real application-judgement "real" 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)
    (>= const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "Vect(v`length)" nvectors 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)
    (/= 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)
    (> const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors nil))
   shostak))
 (dot_scal_left_TCC1 0
  (dot_scal_left_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((* const-decl "Vect(v`length)" nvectors nil)) nil))
 (dot_scal_left 0
  (dot_scal_left-1 nil 3500786422
   ("" (skosimp :preds? t)
    (("" (expand "*")
      (("" (expand "fseq_appl")
        (("" (use "sigma_scal[nat]")
          (("" (replace -1 :dir rl :hide? t)
            (("" (use "sigma_eq[nat]") (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((* const-decl "Vect(v`length)" nvectors nil)
    (* const-decl "real" nvectors nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sigma_eq formula-decl nil sigma "reals/")
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T_low type-eq-decl nil sigma "reals/")
    (sigma_scal formula-decl nil sigma "reals/")
    (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 "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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors nil))
   shostak))
 (dot_scal_right_TCC1 0
  (dot_scal_right_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((* const-decl "Vect(v`length)" nvectors nil)) nil))
 (dot_scal_right 0
  (dot_scal_right-1 nil 3500786537
   ("" (skosimp :preds? t)
    (("" (expand "*")
      (("" (expand "fseq_appl")
        (("" (use "sigma_scal[nat]")
          (("" (replace -1 :dir rl :hide? t)
            (("" (use "sigma_eq[nat]") (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((* const-decl "Vect(v`length)" nvectors nil)
    (* const-decl "real" nvectors nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sigma_eq formula-decl nil sigma "reals/")
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T_low type-eq-decl nil sigma "reals/")
    (sigma_scal formula-decl nil sigma "reals/")
    (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 "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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors nil))
   shostak))
 (dot_scal_assoc 0
  (dot_scal_assoc-1 nil 3500786577
   ("" (grind-with-ext :exclude "default") nil nil)
   ((* const-decl "Vect(v`length)" nvectors nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
 (dot_scal_canon_TCC1 0
  (dot_scal_canon_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((* const-decl "Vect(v`length)" nvectors nil)) nil))
 (dot_scal_canon 0
  (dot_scal_canon-1 nil 3500786586
   ("" (skosimp :preds? t)
    (("" (expand "*")
      (("" (expand "fseq_appl")
        (("" (lemma "sigma_scal[nat]")
          ((""
            (inst -1 "LAMBDA (i: nat): u!1`seq(i) * v!1`seq(i)" "a!1 *
b!1" "u!1`length - 1" "0")
            (("" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((* const-decl "Vect(v`length)" nvectors nil)
    (* const-decl "real" nvectors nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T_low type-eq-decl nil sigma "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (>= const-decl "bool" reals 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)
    (sigma_scal formula-decl nil sigma "reals/")
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors nil))
   shostak))
 (dot_scal_distr_add_TCC1 0
  (dot_scal_distr_add_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((* const-decl "Vect(v`length)" nvectors nil)) nil))
 (dot_scal_distr_add 0
  (dot_scal_distr_add-1 nil 3500786724
   ("" (grind-with-ext :exclude "default") nil nil)
   ((* const-decl "Vect(v`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
 (dot_scal_distr_sub 0
  (dot_scal_distr_sub-1 nil 3500786730
   ("" (grind-with-ext :exclude "default") nil nil)
   ((* const-decl "Vect(v`length)" nvectors nil)
    (- const-decl "Vect(v`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
 (scal_add_distr_TCC1 0
  (scal_add_distr_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((* const-decl "Vect(v`length)" nvectors nil)) nil))
 (scal_add_distr 0
  (scal_add_distr-1 nil 3500786734
   ("" (grind-with-ext :exclude "default") nil nil)
   ((+ const-decl "Vect(u`length)" nvectors nil)
    (* const-decl "Vect(v`length)" nvectors nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
 (scal_sub_distr 0
  (scal_sub_distr-1 nil 3500786738
   ("" (grind-with-ext :exclude "default") nil nil)
   ((- const-decl "Vect(v`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil)
    (* const-decl "Vect(v`length)" nvectors nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil))
   shostak))
 (scal_zero 0
  (scal_zero-1 nil 3500786742
   ("" (grind-with-ext :exclude "default") nil nil)
   ((zero const-decl "Zero_vect(n)" nvectors nil)
    (* const-decl "Vect(v`length)" nvectors nil))
   shostak))
 (scal_0 0
  (scal_0-1 nil 3500786750
   ("" (grind-with-ext :exclude "default") nil nil)
   ((* const-decl "Vect(v`length)" nvectors nil)
    (zero const-decl "Zero_vect(n)" nvectors nil))
   shostak))
 (scal_1 0
  (scal_1-1 nil 3501329009
   ("" (skosimp*)
    (("" (apply-extensionality 1 :hide? t)
      (("" (apply-extensionality 1 :hide? t)
        (("" (expand "*") (("" (assert) nil nil)) nil)) nil))
      nil))
    nil)
   ((nat nonempty-type-eq-decl nil naturalnumbers 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)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (* const-decl "Vect(v`length)" nvectors nil)
    (Vect type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vector type-eq-decl nil nvectors nil)
    (> const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real_times_real_is_real application-judgement "real" 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)
    (>= const-decl "bool" reals nil))
   shostak))
 (scal_cancel 0
  (scal_cancel-1 nil 3500826110
   ("" (skosimp*)
    (("" (expand "*")
      (("" (assert)
        (("" (typepred "nzv!1")
          (("" (flatten)
            (("" (expand "norm")
              (("" (case "sqv(nzv!1) = 0")
                (("1" (assert)
                  (("1" (replace -1) (("1" (assert) nil nil)) nil))
                  nil)
                 ("2" (hide 2)
                  (("2" (expand "sqv")
                    (("2" (decompose-equality)
                      (("2" (expand "*")
                        (("2"
                          (case "FORALL (x: nat): nzv!1`seq(x) = 0")
                          (("1" (hide -2)
                            (("1"
                              (case-replace
                               "(LAMBDA (i: nat): nzv!1`seq(i) * nzv!1`seq(i)) = (LAMBDA (i:nat): 0)")
                              (("1"
                                (lemma "sigma_const")
                                (("1"
                                  (inst?)
                                  (("1" (assert) nil nil))
                                  nil))
                                nil)
                               ("2"
                                (apply-extensionality 1 :hide? t)
                                (("2"
                                  (inst?)
                                  (("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil)
                           ("2" (hide 2)
                            (("2" (skosimp*)
                              (("2"
                                (inst?)
                                (("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((* const-decl "Vect(v`length)" nvectors nil)
    (Nz_vector type-eq-decl nil nvectors nil)
    (norm const-decl "nnreal" nvectors nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (/= const-decl "boolean" notequal nil)
    (Vector type-eq-decl nil nvectors nil)
    (fseq type-eq-decl nil fseqs_def "structures/")
    (barray type-eq-decl nil fseqs_def "structures/")
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (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 -> numfield]" number_fields nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (T_low type-eq-decl nil sigma "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T_high type-eq-decl nil sigma "reals/")
    (<= const-decl "bool" reals nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/")
    (sigma_nat application-judgement "nat" sigma_nat "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (int_times_even_is_even application-judgement "even_int" integers
     nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (sigma_const formula-decl nil sigma "reals/")
    (* const-decl "real" nvectors nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sqrt_0 formula-decl nil sqrt "reals/")
    (sqv const-decl "nnreal" nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   shostak))
 (scal_dot_eq_0 0
  (scal_dot_eq_0-1 nil 3500786759
   ("" (skosimp :preds? t)
    (("" (expand "*")
      (("" (expand "zero")
        (("" (decompose-equality)
          (("" (apply-extensionality 2 :hide? t)
            (("" (apply-extensionality :hide? t)
              (("1" (inst?)
                (("1" (assert)
                  (("1" (expand "fseq_appl") (("1" (assert) nil nil))
                    nil))
                  nil))
                nil)
               ("2" (hide-all-but (1 -5)) (("2" (grind) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((* const-decl "Vect(v`length)" nvectors nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (zero const-decl "Zero_vect(n)" nvectors 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)
    (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 "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors nil))
   shostak))
 (dot_ge_dist_TCC1 0
  (dot_ge_dist_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil) nil
   nil))
 (dot_ge_dist_TCC2 0
  (dot_ge_dist_TCC2-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((* const-decl "real" nvectors nil)
    (- const-decl "Vect(v`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil))
 (dot_ge_dist 0
  (dot_ge_dist-1 nil 3500786888
   ("" (skosimp :preds? t)
    (("" (expand "*")
      (("" (expand "-")
        (("" (expand "fseq_appl")
          (("" (lemma "sigma_minus[nat]")
            ((""
              (inst -1 "LAMBDA (i: nat): w!1`seq(i) * u!1`seq(i)"
               "LAMBDA (i: nat): w!1`seq(i) * v!1`seq(i)" "w!1`length -
      1" "0")
              (("" (assert)
                ((""
                  (name-replace "s1" "sigma(0, w!1`length - 1,
            LAMBDA (i: nat): w!1`seq(i) * u!1`seq(i))" :hide? t)
                  ((""
                    (name-replace "s2" "sigma(0, w!1`length - 1,
             LAMBDA (i: nat): w!1`seq(i) * v!1`seq(i))" :hide? t)
                    (("" (lemma "sigma_eq[nat]")
                      ((""
                        (inst -1 "LAMBDA (i_1: nat):
               w!1`seq(i_1) * u!1`seq(i_1) - w!1`seq(i_1) * v!1`seq(i_1)"
                         "LAMBDA (i: nat):
              w!1`seq(i) * (u!1 + -v!1)`seq(i)" "w!1`length - 1" "0")
                        (("1" (assert)
                          (("1" (hide-all-but 1)
                            (("1" (grind) nil nil)) nil))
                          nil)
                         ("2" (hide-all-but 1) (("2" (grind) nil nil))
                          nil)
                         ("3" (hide-all-but 1) (("3" (grind) nil nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((* const-decl "real" nvectors nil)
    (sigma_minus formula-decl nil sigma "reals/")
    (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 "bool" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "Vect(v`length)" nvectors nil)
    (u!1 skolem-const-decl "Vector" nvectors nil)
    (v!1 skolem-const-decl "Vect(u!1`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (sigma_eq formula-decl nil sigma "reals/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (sigma def-decl "real" sigma "reals/")
    (T_low type-eq-decl nil sigma "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T_high type-eq-decl nil sigma "reals/")
    (<= const-decl "bool" reals nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (- const-decl "Vect(u`length)" nvectors 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors nil))
   shostak))
 (dot_gt_dist_TCC1 0
  (dot_gt_dist_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((* const-decl "real" nvectors nil)
    (- const-decl "Vect(v`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil))
 (dot_gt_dist 0
  (dot_gt_dist-1 nil 3500787454
   ("" (skosimp :preds? t)
    (("" (expand "-")
      (("" (expand "-")
        (("" (expand "+")
          (("" (expand "*")
            (("" (expand "fseq_appl")
              (("" (lemma "sigma_minus[nat]")
                ((""
                  (inst -1 "LAMBDA (i: nat): w!1`seq(i) * u!1`seq(i)"
                   "LAMBDA (i: nat): w!1`seq(i) * v!1`seq(i)"
                   "w!1`length - 1" "0")
                  ((""
                    (name-replace "s1" "sigma(0, w!1`length - 1,
            LAMBDA (i: nat): w!1`seq(i) * u!1`seq(i))" :hide? t)
                    ((""
                      (name-replace "s2" "sigma(0, w!1`length - 1,
             LAMBDA (i: nat): w!1`seq(i) * v!1`seq(i))" :hide? t)
                      (("" (lemma "sigma_eq[nat]")
                        ((""
                          (inst -1 "LAMBDA (i_1: nat):
               w!1`seq(i_1) * u!1`seq(i_1) - w!1`seq(i_1) * v!1`seq(i_1)"
                           "LAMBDA (i: nat):
              w!1`seq(i) * (u!1 + -v!1)`seq(i)" "w!1`length - 1" "0")
                          (("1" (assert) nil nil)
                           ("2" (hide-all-but 1)
                            (("2" (grind) nil nil)) nil)
                           ("3" (hide-all-but 1)
                            (("3" (grind) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((- const-decl "Vect(u`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (sigma_minus formula-decl nil sigma "reals/")
    (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 "bool" reals nil)
    (sigma def-decl "real" sigma "reals/")
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (sigma_eq formula-decl nil sigma "reals/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (v!1 skolem-const-decl "Vect(u!1`length)" nvectors nil)
    (u!1 skolem-const-decl "Vector" nvectors nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T_low type-eq-decl nil sigma "reals/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (* const-decl "real" nvectors nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (- const-decl "Vect(v`length)" nvectors 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors nil))
   shostak))
 (sq_dot_eq 0
  (sq_dot_eq-1 nil 3500788721
   ("" (skosimp :preds? t)
    (("" (expand "*")
      (("" (expand "zero")
        (("" (prop)
          (("1" (apply-extensionality :hide? t)
            (("1" (lemma "sigma_nonneg_eq_0")
              (("1" (inst?)
                (("1" (assert)
                  (("1" (apply-extensionality 1 :hide? t)
                    (("1" (inst?)
                      (("1" (typepred "x!1")
                        (("1" (split -2)
                          (("1" (assert)
                            (("1" (mult-cases -1) nil nil)) nil)
                           ("2" (typepred "v!1`seq")
                            (("2" (inst?) (("2" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (replace -1)
            (("2" (assert) (("2" (use "sigma_zero[nat]") nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((* const-decl "real" nvectors nil)
    (sigma_nonneg_eq_0 formula-decl nil sigma "reals/")
    (zero_times3 formula-decl nil real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans 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)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T_low type-eq-decl nil sigma "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers 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 "bool" reals nil)
    (sigma_zero formula-decl nil sigma "reals/")
    (zero const-decl "Zero_vect(n)" nvectors 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil))
   shostak))
 (sqv_sq 0
  (sqv_sq-1 nil 3500789105
   ("" (grind-with-ext :exclude "default") nil nil)
   ((nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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)
    (sigma def-decl "real" sigma "reals/")
    (* const-decl "real" nvectors nil)
    (sqv const-decl "nnreal" nvectors nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (sq const-decl "nnreal" nvectors nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   shostak))
 (sq_sqv 0
  (sq_sqv-1 nil 3500789110
   ("" (grind-with-ext :exclude "default") nil nil)
   ((sq const-decl "nonneg_real" sq "reals/")
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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)
    (sigma def-decl "real" sigma "reals/")
    (sq const-decl "nnreal" nvectors nil)
    (* const-decl "real" nvectors nil)
    (sqv const-decl "nnreal" nvectors nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/")
    (int_minus_int_is_int application-judgement "int" integers nil))
   shostak))
 (sq_lem 0
  (sq_lem-1 nil 3500789113
   ("" (grind-with-ext :exclude "default") nil nil)
   ((sq const-decl "nonneg_real" sq "reals/")
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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)
    (sigma def-decl "real" sigma "reals/")
    (sq const-decl "nnreal" nvectors nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/")
    (int_minus_int_is_int application-judgement "int" integers nil))
   shostak))
 (sqv_lem 0
  (sqv_lem-1 nil 3500789120
   ("" (grind-with-ext :exclude "default") nil nil)
   ((nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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)
    (sigma def-decl "real" sigma "reals/")
    (* const-decl "real" nvectors nil)
    (sqv const-decl "nnreal" nvectors nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   shostak))
 (sqv_zero 0
  (sqv_zero-1 nil 3500789123
   ("" (skosimp :preds? t)
    (("" (expand "zero")
      (("" (expand "sqv")
        (("" (expand "*") (("" (use "sigma_zero[nat]") nil nil)) nil))
        nil))
      nil))
    nil)
   ((zero const-decl "Zero_vect(n)" nvectors nil)
    (* const-decl "real" nvectors nil)
    (sigma_zero formula-decl nil sigma "reals/")
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma "reals/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T_low type-eq-decl nil sigma "reals/")
    (sqv const-decl "nnreal" nvectors 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)
    (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 "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil))
   shostak))
 (sqv_eq_0 0
  (sqv_eq_0-1 nil 3500789189
   ("" (skosimp :preds? t)
    (("" (expand "sqv") (("" (use "sq_dot_eq") nil nil)) nil)) nil)
   ((sqv const-decl "nnreal" nvectors nil)
    (sq_dot_eq formula-decl nil nvectors 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil))
   shostak))
 (sqv_neg 0
  (sqv_neg-1 nil 3500789338
   ("" (skosimp :preds? t)
    (("" (expand "sqv") (("" (use "dot_neg_sq") nil nil)) nil)) nil)
   ((sqv const-decl "nnreal" nvectors nil)
    (dot_neg_sq formula-decl nil nvectors 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil))
   shostak))
 (sqv_add_TCC1 0
  (sqv_add_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((* const-decl "Vect(v`length)" nvectors nil)) nil))
 (sqv_add 0
  (sqv_add-1 nil 3500789436
   ("" (skosimp :preds? t)
    (("" (expand "sqv")
      (("" (lemma "dot_distr_add_right")
        (("" (inst -1 "(u!1 + v!1)" "u!1" "v!1")
          (("1" (replace -1 :hide? t)
            (("1" (rewrite "dot_distr_add_left")
              (("1" (rewrite "dot_distr_add_left")
                (("1" (lemma "dot_comm")
                  (("1" (inst -1 "v!1" "u!1")
                    (("1" (replace -1 :hide? t)
                      (("1" (lemma "add_comm")
                        (("1" (assert)
                          (("1" (assert)
                            (("1" (rewrite "dot_scal_left") nil nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (assert) nil nil) ("3" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((sqv const-decl "nnreal" nvectors nil)
    (v!1 skolem-const-decl "Vect(u!1`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (u!1 skolem-const-decl "Vector" nvectors nil)
    (dot_distr_add_left formula-decl nil nvectors nil)
    (dot_comm formula-decl nil nvectors nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (dot_scal_left formula-decl nil nvectors nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (add_comm formula-decl nil nvectors nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (dot_distr_add_right formula-decl nil nvectors 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors nil))
   shostak))
 (sqv_sub 0
  (sqv_sub-1 nil 3500791344
   ("" (skosimp*)
    (("" (expand "sqv")
      (("" (lemma "dot_distr_sub_right")
        (("" (inst -1 "(u!1 - v!1)" "u!1" "v!1")
          (("1" (replace -1 :hide? t)
            (("1" (rewrite "dot_distr_sub_left")
              (("1" (rewrite "dot_distr_sub_left")
                (("1" (assert)
                  (("1" (rewrite "dot_comm")
                    (("1" (assert)
                      (("1" (rewrite "dot_assoc" :dir rl)
                        (("1" (assert)
                          (("1" (rewrite "dot_comm") nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (assert) nil nil) ("3" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((sqv const-decl "nnreal" nvectors nil)
    (v!1 skolem-const-decl "Vect(u!1`length)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil)
    (Vect type-eq-decl nil nvectors nil)
    (u!1 skolem-const-decl "Vector" nvectors nil)
    (Vector type-eq-decl nil nvectors nil)
    (> const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (fseq type-eq-decl nil fseqs_def "structures/")
    (barray type-eq-decl nil fseqs_def "structures/")
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (dot_distr_sub_left formula-decl nil nvectors nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (dot_assoc formula-decl nil nvectors nil)
    (dot_comm formula-decl nil nvectors nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (dot_distr_sub_right formula-decl nil nvectors nil))
   shostak))
 (sqv_sym 0
  (sqv_sym-1 nil 3500791556
   ("" (skosimp :preds? t)
    (("" (expand "sqv")
      (("" (expand "-")
        (("" (expand "-")
          (("" (expand "+")
            (("" (expand "*")
              (("" (expand "fseq_appl")
                (("" (replace -3 :actuals? t)
                  (("" (use "sigma_eq[nat]")
                    (("1" (assert) nil nil)
                     ("2" (hide-all-but 1) (("2" (grind) nil nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sqv const-decl "nnreal" nvectors nil)
    (- const-decl "Vect(v`length)" nvectors nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (* const-decl "real" nvectors nil) (>= const-decl "bool" reals 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)
    (sigma_eq formula-decl nil sigma "reals/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T_low type-eq-decl nil sigma "reals/")
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors nil))
   shostak))
 (sqv_scal 0
  (sqv_scal-1 nil 3500791721
   ("" (skosimp :preds? t)
    (("" (expand "sqv")
      (("" (expand "sq")
        (("" (assert) (("" (rewrite "dot_scal_canon") nil nil)) nil))
        nil))
      nil))
    nil)
   ((sqv const-decl "nnreal" nvectors nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (dot_scal_canon formula-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil))
   shostak))
 (sqrt_sqv_sq 0
  (sqrt_sqv_sq-1 nil 3500791898
   ("" (skosimp :preds? t)
    (("" (expand "sqv")
      (("" (typepred "sqrt(v!1 * v!1)")
        (("1" (propax) nil nil) ("2" (assert) nil nil)) nil))
      nil))
    nil)
   ((sqv const-decl "nnreal" nvectors nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (nnreal 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: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (Vect type-eq-decl nil nvectors nil)
    (* const-decl "real" nvectors 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil))
   shostak))
 (norm_sym 0
  (norm_sym-1 nil 3500791987
   ("" (skosimp :preds? t)
    (("" (expand "norm") (("" (rewrite "sqv_sym") nil nil)) nil)) nil)
   ((norm const-decl "nnreal" nvectors nil)
    (sqv_sym formula-decl nil nvectors 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors nil))
   shostak))
 (norm_neg 0
  (norm_neg-1 nil 3500792117
   ("" (skosimp :preds? t)
    (("" (expand "norm")
      (("" (lemma "norm_sym")
        (("" (inst -1 "zero(u!1`length)" "u!1")
          (("1" (rewrite "sub_zero_left")
            (("1" (rewrite "sub_zero_right")
              (("1" (expand "norm") (("1" (propax) nil nil)) nil))
              nil))
            nil)
           ("2" (expand "zero") (("2" (propax) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((norm const-decl "nnreal" nvectors nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (zero const-decl "Zero_vect(n)" nvectors nil)
    (Zero_vect type-eq-decl nil nvectors nil)
    (nnreal type-eq-decl nil real_types nil)
    (Vect type-eq-decl nil nvectors nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals 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)
    (u!1 skolem-const-decl "Vector" nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sub_zero_right formula-decl nil nvectors nil)
    (sub_zero_left formula-decl nil nvectors nil)
    (norm_sym formula-decl nil nvectors 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil))
   shostak))
 (dot_sq_norm 0
  (dot_sq_norm-1 nil 3500792266
   ("" (skosimp :preds? t)
    (("" (expand "norm")
      (("" (expand "sq")
        (("" (rewrite "sqrt_sqv_sq")
          (("" (assert)
            (("" (expand "sqv") (("" (propax) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((norm const-decl "nnreal" nvectors nil)
    (sqrt_sqv_sq formula-decl nil nvectors nil)
    (sqv const-decl "nnreal" nvectors nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil))
   shostak))
 (sq_norm 0
  (sq_norm-1 nil 3500792329
   ("" (skosimp :preds? t) (("" (rewrite "dot_sq_norm") nil nil)) nil)
   ((dot_sq_norm formula-decl nil nvectors 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil))
   shostak))
 (sqrt_sqv_norm 0
  (sqrt_sqv_norm-1 nil 3500792356
   ("" (skosimp :preds? t)
    (("" (expand "norm") (("" (propax) nil nil)) nil)) nil)
   ((norm const-decl "nnreal" nvectors 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil))
   shostak))
 (norm_eq_0 0
  (norm_eq_0-1 nil 3500792378
   ("" (skosimp :preds? t)
    (("" (expand "norm")
      (("" (expand "sqv")
        (("" (prop)
          (("1" (lemma "sqrt_eq_0")
            (("1" (inst - v!1*v!1)
              (("1" (split -1)
                (("1" (hide -2)
                  (("1" (lemma "sq_dot_eq")
                    (("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
                  nil)
                 ("2" (propax) nil nil))
                nil)
               ("2" (assert) nil nil))
              nil))
            nil)
           ("2" (replace -1)
            (("2" (expand "zero")
              (("2" (expand "*")
                (("2" (lemma "sigma_zero")
                  (("2" (inst?)
                    (("2" (assert)
                      (("2" (replace -1) (("2" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((norm const-decl "nnreal" nvectors nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (v!1 skolem-const-decl "Vector" nvectors nil)
    (* const-decl "real" nvectors nil)
    (Vect type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sq_dot_eq formula-decl nil nvectors nil)
    (sqrt_eq_0 formula-decl nil sqrt "reals/")
    (zero const-decl "Zero_vect(n)" nvectors nil)
    (sigma_zero formula-decl nil sigma "reals/")
    (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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sigma_nat application-judgement "nat" sigma_nat "reals/")
    (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/")
    (sqrt_0 formula-decl nil sqrt "reals/")
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma "reals/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T_low type-eq-decl nil sigma "reals/")
    (int_minus_int_is_int application-judgement "int" integers nil)
    (sqv const-decl "nnreal" nvectors 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil))
   shostak))
 (norms_eq_sqv 0
  (norms_eq_sqv-1 nil 3500792831
   ("" (skosimp :preds? t)
    (("" (expand "norm")
      (("" (prop)
        (("1" (typepred "sqrt(sqv(u!1))")
          (("1" (typepred "sqrt(sqv(v!1))") (("1" (assert) nil nil))
            nil))
          nil)
         ("2" (assert) nil nil))
        nil))
      nil))
    nil)
   ((norm const-decl "nnreal" nvectors nil)
    (sqv const-decl "nnreal" nvectors nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (nnreal type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors nil))
   shostak))
 (norm_scal 0
  (norm_scal-1 nil 3500793051
   ("" (skosimp*)
    (("" (expand "norm")
      (("" (rewrite "sqv_scal")
        (("" (rewrite "sqrt_times")
          (("" (rewrite "sqrt_sq_abs") nil nil)) nil))
        nil))
      nil))
    nil)
   ((norm const-decl "nnreal" nvectors nil)
    (sqrt_times formula-decl nil sqrt "reals/")
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (nnreal type-eq-decl nil real_types nil)
    (sqv const-decl "nnreal" nvectors nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqrt_sq_abs formula-decl nil sqrt "reals/")
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (Vector type-eq-decl nil nvectors nil)
    (> const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (fseq type-eq-decl nil fseqs_def "structures/")
    (barray type-eq-decl nil fseqs_def "structures/")
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (sqv_scal formula-decl nil nvectors nil))
   shostak))
 (idem_right 0
  (idem_right-1 nil 3500788316
   ("" (skosimp :preds? t)
    (("" (prop)
      (("1" (apply-extensionality 2 :hide? t)
        (("1" (apply-extensionality 1 :hide? t)
          (("1" (expand "zero")
            (("1" (lemma "scal_cancel")
              (("1" (inst -1 "a!1" "1" "v!1")
                (("1" (assert)
                  (("1" (replace -1) (("1" (rewrite "scal_1") nil nil))
                    nil))
                  nil)
                 ("2" (flatten)
                  (("2" (lemma "norm_eq_0")
                    (("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (assert)
        (("2" (replace -1)
          (("2" (assert)
            (("2" (apply-extensionality 1 :hide? t)
              (("2" (expand "*")
                (("2" (apply-extensionality 1 :hide? t) nil nil)) nil))
              nil))
            nil))
          nil))
        nil)
       ("3" (replace -1)
        (("3" (expand "zero")
          (("3" (assert)
            (("3" (expand "*") (("3" (propax) nil nil)) nil)) nil))
          nil))
        nil))
      nil))
    nil)
   ((scal_cancel formula-decl nil nvectors nil)
    (norm_eq_0 formula-decl nil nvectors nil)
    (scal_1 formula-decl nil nvectors nil)
    (Nz_vector type-eq-decl nil nvectors nil)
    (v!1 skolem-const-decl "Vector" nvectors nil)
    (/= const-decl "boolean" notequal nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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 "bool" reals nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors nil)
    (nnreal type-eq-decl nil real_types nil)
    (norm const-decl "nnreal" nvectors nil)
    (Zero_vect type-eq-decl nil nvectors nil)
    (zero const-decl "Zero_vect(n)" nvectors nil)
    (* const-decl "Vect(v`length)" nvectors nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil))
   shostak))
 (caret_TCC1 0
  (caret_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (/= const-decl "boolean" notequal nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (Nz_vector type-eq-decl nil nvectors nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (* const-decl "real" nvectors nil)
    (sqv const-decl "nnreal" nvectors nil)
    (norm const-decl "nnreal" nvectors nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
 (caret_TCC2 0
  (caret_TCC2-1 nil 3500755723
   ("" (skosimp :preds? t)
    (("" (use "norm_scal")
      (("" (replace -1 :hide? t)
        (("" (expand "abs")
          (("" (lift-if)
            (("" (assert)
              (("" (prop)
                (("" (hide -2)
                  (("" (expand "norm")
                    (("" (expand "sqv")
                      (("" (expand "*")
                        (("" (use "sigma_ge_0[nat]")
                          (("" (prop)
                            (("1"
                              (name-replace "ss"
                               "sigma(0, nzv!1`length - 1,
                LAMBDA (i: nat): nzv!1`seq(i) * nzv!1`seq(i))" :hide?
                               t)
                              (("1"
                                (typepred "sqrt(ss)")
                                (("1"
                                  (assert)
                                  (("1"
                                    (rewrite "quotient_neg_lt")
                                    nil
                                    nil))
                                  nil)
                                 ("2" (propax) nil nil))
                                nil))
                              nil)
                             ("2" (hide-all-but 1)
                              (("2" (grind) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((norm_scal formula-decl nil nvectors 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)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
     real_defs nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (minus_nzreal_is_nzreal application-judgement "nzreal" real_types
     nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sqv const-decl "nnreal" nvectors 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)
    (sigma_ge_0 formula-decl nil sigma "reals/")
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T_low type-eq-decl nil sigma "reals/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (sigma def-decl "real" sigma "reals/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (quotient_neg_lt formula-decl nil real_props nil)
    (nonzero_real nonempty-type-eq-decl nil reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (* const-decl "real" nvectors 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (/= const-decl "boolean" notequal nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (norm const-decl "nnreal" nvectors nil)
    (Nz_vector type-eq-decl nil nvectors nil))
   nil))
 (dot_normalize_TCC1 0
  (dot_normalize_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((* const-decl "real" nvectors nil)
    (sqv const-decl "nnreal" nvectors nil)
    (norm const-decl "nnreal" nvectors nil)
    (* const-decl "Vect(v`length)" nvectors nil)
    (^ const-decl "Normalized" nvectors nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil))
 (dot_normalize_TCC2 0
  (dot_normalize_TCC2-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (/= const-decl "boolean" notequal nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (Nz_vector type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors nil)
    (Nz_vect type-eq-decl nil nvectors nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (* const-decl "real" nvectors nil)
    (sqv const-decl "nnreal" nvectors nil)
    (norm const-decl "nnreal" nvectors nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
 (dot_normalize 0
  (dot_normalize-1 nil 3500793449
   ("" (skosimp*)
    (("" (expand "^")
      (("" (assert)
        (("" (rewrite "dot_scal_right")
          (("" (assert)
            (("" (rewrite "dot_scal_left") (("" (assert) nil nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((^ const-decl "Normalized" nvectors nil)
    (dot_scal_right formula-decl nil nvectors nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (bool nonempty-type-eq-decl nil booleans nil)
    (> const-decl "bool" reals nil)
    (Vector type-eq-decl nil nvectors nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (norm const-decl "nnreal" nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Nz_vector type-eq-decl nil nvectors nil)
    (Vect type-eq-decl nil nvectors nil)
    (Nz_vect type-eq-decl nil nvectors nil)
    (* const-decl "Vect(v`length)" nvectors nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (dot_scal_left formula-decl nil nvectors nil)
    (nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil))
   shostak))
 (normalize_normalize_TCC1 0
  (normalize_normalize_TCC1-1 nil 3500755723
   ("" (skosimp :preds? t)
    (("" (rewrite "norm_eq_0")
      (("" (expand "zero")
        (("" (apply-extensionality :hide? t) nil nil)) nil))
      nil))
    nil)
   ((norm_eq_0 formula-decl nil nvectors 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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (zero const-decl "Zero_vect(n)" nvectors 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (/= const-decl "boolean" notequal nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (norm const-decl "nnreal" nvectors nil)
    (Nz_vector type-eq-decl nil nvectors nil))
   nil))
 (normalize_normalize 0
  (normalize_normalize-1 nil 3500793485
   ("" (skosimp*)
    (("" (assert)
      (("" (expand "^")
        (("" (rewrite "norm_scal")
          (("" (expand "abs")
            (("" (lift-if)
              (("" (split +)
                (("1" (flatten)
                  (("1" (cross-mult -1) (("1" (assert) nil nil)) nil))
                  nil)
                 ("2" (flatten)
                  (("2" (expand "*")
                    (("2" (assert)
                      (("2" (apply-extensionality 2 :hide? t)
                        (("2" (lift-if) (("2" (ground) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nzreal_div_nzreal_is_nzreal application-judgement "nzreal"
     real_types nil)
    (norm_scal formula-decl nil nvectors nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (bool nonempty-type-eq-decl nil booleans nil)
    (> const-decl "bool" reals nil)
    (Vector type-eq-decl nil nvectors nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (norm const-decl "nnreal" nvectors nil)
    (Nz_vector type-eq-decl nil nvectors nil)
    (nonzero_abs_is_pos application-judgement "{y: posreal | y >= x}"
     real_defs nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (* const-decl "Vect(v`length)" nvectors nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (posreal nonempty-type-eq-decl nil real_types nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (div_mult_pos_lt1 formula-decl nil real_props nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (^ const-decl "Normalized" nvectors nil))
   shostak))
 (sqv_minus_dot_TCC1 0
  (sqv_minus_dot_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((* const-decl "Vect(v`length)" nvectors nil)) nil))
 (sqv_minus_dot 0
  (sqv_minus_dot-1 nil 3500793554
   ("" (skosimp*)
    (("" (expand "sqv" 1 1)
      (("" (lemma "dot_distr_sub_left")
        (("" (inst -1 "(u!1 - a!1 * v!1)" "u!1" "a!1*v!1")
          (("1" (replace -1 :hide? t)
            (("1" (lemma "dot_distr_sub_right")
              (("1" (inst -1 "u!1" "u!1" "a!1 * v!1")
                (("1" (replace -1 :hide? t)
                  (("1" (lemma "dot_distr_sub_right")
                    (("1" (inst -1 "a!1 * v!1" "u!1" "a!1 * v!1")
                      (("1" (replace -1 :hide? t)
                        (("1" (expand "sqv")
                          (("1" (expand "sq")
                            (("1" (assert)
                              (("1"
                                (rewrite "dot_scal_right")
                                (("1"
                                  (rewrite "dot_scal_right")
                                  (("1"
                                    (case-replace
                                     "a!1 * v!1 * u!1 = a!1 * u!1 * v!1")
                                    (("1"
                                      (hide -1)
                                      (("1"
                                        (case-replace
                                         "v!1 * v!1 * a!1 * a!1 = a!1*a!1*v!1 * v!1")
                                        (("1"
                                          (hide -1)
                                          (("1"
                                            (case-replace
                                             "a!1 * u!1 * v!1 = a!1 * ( u!1 * v!1)")
                                            (("1"
                                              (case-replace
                                               "2 * a!1 * u!1 * v!1 = 2 * a!1 * ( u!1 * v!1)")
                                              (("1"
                                                (name-replace
                                                 udotv
                                                 "u!1 * v!1")
                                                (("1"
                                                  (case-replace
                                                   "a!1 * a!1 * v!1 * v!1 = a!1 *( a!1 * v!1 * v!1)")
                                                  (("1"
                                                    (assert)
                                                    nil
                                                    nil)
                                                   ("2"
                                                    (hide -1 -2 2)
                                                    (("2"
                                                      (lemma
                                                       "dot_scal_assoc")
                                                      (("2"
                                                        (inst
                                                         -1
                                                         "a!1"
                                                         "a!1"
                                                         "v!1")
                                                        (("2"
                                                          (replace
                                                           -1
                                                           *
                                                           rl)
                                                          (("2"
                                                            (rewrite
                                                             "dot_scal_left")
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (hide -1 2)
                                                (("2"
                                                  (assert)
                                                  (("2"
                                                    (rewrite
                                                     "dot_scal_left")
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil)
                                             ("2"
                                              (hide 2)
                                              (("2"
                                                (assert)
                                                (("2"
                                                  (rewrite
                                                   "dot_scal_left")
                                                  nil
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil)
                                         ("2"
                                          (hide 2)
                                          (("2"
                                            (assert)
                                            (("2"
                                              (rewrite "dot_scal_left")
                                              nil
                                              nil))
                                            nil))
                                          nil)
                                         ("3"
                                          (hide 2)
                                          (("3" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("2"
                                      (hide 2)
                                      (("2"
                                        (rewrite "dot_scal_left")
                                        (("2"
                                          (assert)
                                          (("2"
                                            (rewrite "dot_comm")
                                            (("2"
                                              (assert)
                                              (("2"
                                                (rewrite
                                                 "dot_scal_left"
                                                 :dir
                                                 rl)
                                                nil
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil)
                                     ("3" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (assert) nil nil) ("3" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((sqv const-decl "nnreal" nvectors nil)
    (v!1 skolem-const-decl "Vect(u!1`length)" nvectors nil)
    (a!1 skolem-const-decl "real" nvectors nil)
    (* const-decl "Vect(v`length)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil)
    (Vect type-eq-decl nil nvectors nil)
    (u!1 skolem-const-decl "Vector" nvectors nil)
    (Vector type-eq-decl nil nvectors nil)
    (> const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (fseq type-eq-decl nil fseqs_def "structures/")
    (barray type-eq-decl nil fseqs_def "structures/")
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (dot_distr_sub_right formula-decl nil nvectors nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (dot_comm formula-decl nil nvectors nil)
    (dot_scal_assoc formula-decl nil nvectors nil)
    (dot_scal_left formula-decl nil nvectors nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "real" nvectors nil)
    (dot_scal_right formula-decl nil nvectors nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (dot_distr_sub_left formula-decl nil nvectors nil))
   shostak))
 (cauchy_schwarz 0
  (cauchy_schwarz-1 nil 3500794264
   ("" (skosimp :preds? t)
    (("" (case "sqv(v!1) = 0")
      (("1" (rewrite "sqv_eq_0")
        (("1" (replace -4)
          (("1" (replace -1 :hide? t)
            (("1" (rewrite "dot_zero_right")
              (("1" (rewrite "sq_0") (("1" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (case "(FORALL (t:real): sqv(u!1-t*v!1) >= 0)")
        (("1" (inst -1 "(u!1*v!1)/sqv(v!1)")
          (("1" (rewrite "sqv_minus_dot")
            (("1" (name-replace "UDOTV" "u!1 * v!1")
              (("1"
                (case-replace
                 "2 * (UDOTV / sqv(v!1)) * u!1 * v!1 = 2 * sq(UDOTV) / sqv(v!1) ")
                (("1" (hide -1)
                  (("1"
                    (case-replace
                     "sq(UDOTV / sqv(v!1)) * sqv(v!1) = sq(UDOTV) / sqv(v!1) ")
                    (("1" (hide -1)
                      (("1" (assert)
                        (("1"
                          (case-replace
                           "sqv(u!1) + sq(UDOTV) / sqv(v!1) - 2 * sq(UDOTV) / sqv(v!1) = sqv(u!1) - sq(UDOTV) / sqv(v!1)")
                          (("1" (hide -1)
                            (("1" (assert)
                              (("1"
                                (mult-by -1 "sqv(v!1)")
                                (("1" (assert) nil nil))
                                nil))
                              nil))
                            nil)
                           ("2" (lemma "sqv_eq_0")
                            (("2" (inst?) (("2" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (rewrite "sq_div")
                      (("2" (expand "sq" 1) (("2" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (assert)
                  (("2" (reveal -1)
                    (("2"
                      (case-replace
                       "2 * (UDOTV / sqv(v!1)) * u!1 * v!1 = 2 * (UDOTV / sqv(v!1)) * (u!1 * v!1)")
                      (("1" (hide -1)
                        (("1" (replace -1)
                          (("1" (hide -1)
                            (("1" (expand "sq")
                              (("1" (assert) nil nil)) nil))
                            nil))
                          nil))
                        nil)
                       ("2" (hide -1 2 3)
                        (("2" (rewrite "dot_scal_left") nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (assert) nil nil))
          nil)
         ("2" (assert) (("2" (skosimp*) (("2" (assert) nil nil)) nil))
          nil)
         ("3" (skosimp*) (("3" (assert) nil nil)) nil))
        nil))
      nil))
    nil)
   ((sqv const-decl "nnreal" nvectors nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (dot_zero_right formula-decl nil nvectors nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (sq_0 formula-decl nil sq "reals/")
    (sqv_eq_0 formula-decl nil nvectors nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (/= const-decl "boolean" notequal nil)
    (u!1 skolem-const-decl "Vector" nvectors nil)
    (v!1 skolem-const-decl "Vect(u!1`length)" nvectors 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 "real" nvectors nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (dot_scal_left formula-decl nil nvectors nil)
    (sq_div formula-decl nil sq "reals/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (both_sides_times_pos_ge1_imp formula-decl nil extra_real_props
     nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (sqv_minus_dot formula-decl nil nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil)
    (* const-decl "Vect(v`length)" nvectors 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (Vector type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors nil))
   shostak))
 (dot_norm 0
  (dot_norm-1 nil 3500823230
   ("" (skosimp*)
    (("" (lemma "cauchy_schwarz")
      (("" (inst?)
        (("" (lemma "sqrt_le")
          (("" (inst?)
            (("" (assert)
              (("" (hide -2)
                (("" (lemma "sqrt_sq_abs")
                  (("" (inst?)
                    (("" (assert)
                      (("" (replace -1)
                        (("" (hide -1)
                          (("" (rewrite "sqrt_times")
                            (("" (expand "norm")
                              ((""
                                (expand "abs")
                                ((""
                                  (lift-if)
                                  (("" (ground) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((cauchy_schwarz formula-decl nil nvectors nil)
    (sqrt_le formula-decl nil sqrt "reals/")
    (minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqrt_sq_abs formula-decl nil sqrt "reals/")
    (norm const-decl "nnreal" nvectors nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (sqrt_times formula-decl nil sqrt "reals/")
    (sqv const-decl "nnreal" nvectors nil)
    (nnreal type-eq-decl nil real_types nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (* const-decl "real" nvectors nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (Vect type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vector type-eq-decl nil nvectors nil)
    (> const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (fseq type-eq-decl nil fseqs_def "structures/")
    (barray type-eq-decl nil fseqs_def "structures/")
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   shostak))
 (norm_add_le 0
  (norm_add_le-1 nil 3500823296
   ("" (skosimp*)
    (("" (expand "norm")
      (("" (lemma "sqrt_le")
        ((""
          (inst -1 "sqv(u!1 + v!1)"
           "sq(sqrt(sqv(u!1)) + sqrt(sqv(v!1)))")
          (("" (rewrite "sqrt_sq")
            (("" (assert)
              (("" (hide 2)
                (("" (rewrite "sqv_add")
                  (("" (expand "sq")
                    (("" (rewrite "sqrt_sqv_sq")
                      (("" (rewrite "sqrt_sqv_sq")
                        (("" (rewrite "sqrt_sqv_norm")
                          (("" (rewrite "sqrt_sqv_norm")
                            (("" (lemma "dot_norm")
                              ((""
                                (inst -1 "u!1" "v!1")
                                ((""
                                  (flatten)
                                  ((""
                                    (rewrite "dot_scal_left")
                                    (("" (assert) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((norm const-decl "nnreal" nvectors nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (> const-decl "bool" reals nil)
    (Vector type-eq-decl nil nvectors nil)
    (nnreal type-eq-decl nil real_types nil)
    (sqv const-decl "nnreal" nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (Vect type-eq-decl nil nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sqrt const-decl "{nnz: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqv_add formula-decl nil nvectors nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (sqrt_sqv_sq formula-decl nil nvectors nil)
    (sqrt_sqv_norm formula-decl nil nvectors nil)
    (dot_norm formula-decl nil nvectors nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (dot_scal_left formula-decl nil nvectors nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sqrt_sq formula-decl nil sqrt "reals/")
    (sqrt_le formula-decl nil sqrt "reals/"))
   shostak))
 (norm_sub_le 0
  (norm_sub_le-1 nil 3500823344
   ("" (skosimp*)
    (("" (expand "norm")
      (("" (lemma "sq_le")
        (("" (inst?)
          (("" (assert)
            (("" (hide 2)
              (("" (expand "sq")
                (("" (rewrite "sq_rew")
                  (("" (rewrite "sq_rew")
                    (("" (rewrite "sqv_sub")
                      (("" (assert)
                        (("" (rewrite "sqrt_sqv_norm")
                          (("" (rewrite "sqrt_sqv_norm")
                            (("" (assert)
                              ((""
                                (lemma "dot_norm")
                                ((""
                                  (inst -1 "-u!1" "v!1")
                                  (("1"
                                    (flatten)
                                    (("1"
                                      (assert)
                                      (("1"
                                        (rewrite "norm_neg")
                                        (("1"
                                          (rewrite "dot_neg_left")
                                          (("1"
                                            (assert)
                                            (("1"
                                              (rewrite "dot_scal_left")
                                              (("1" (assert) nil nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((norm const-decl "nnreal" nvectors nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (nnreal 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: nnreal | nnz * nnz = nnx}" sqrt "reals/")
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (> const-decl "bool" reals nil)
    (Vector type-eq-decl nil nvectors nil)
    (sqv const-decl "nnreal" nvectors nil)
    (Vect type-eq-decl nil nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sq_rew formula-decl nil sq "reals/")
    (sqv_sub formula-decl nil nvectors nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (sqrt_sqv_norm formula-decl nil nvectors nil)
    (u!1 skolem-const-decl "Vector" nvectors nil)
    (v!1 skolem-const-decl "Vect(u!1`length)" nvectors nil)
    (- const-decl "Vect(v`length)" nvectors nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (dot_neg_left formula-decl nil nvectors nil)
    (dot_scal_left formula-decl nil nvectors nil)
    (norm_neg formula-decl nil nvectors nil)
    (dot_norm formula-decl nil nvectors nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (sq_sqrt formula-decl nil sqrt "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sq_le formula-decl nil sq "reals/"))
   shostak))
 (norm_sub_ge 0
  (norm_sub_ge-1 nil 3500823649
   ("" (skosimp*)
    (("" (lemma "norm_add_le")
      (("" (inst -1 "u!1-v!1" "v!1")
        (("1" (assert)
          (("1" (rewrite "add_cancel2") (("1" (assert) nil nil)) nil))
          nil)
         ("2" (assert) nil nil))
        nil))
      nil))
    nil)
   ((norm_add_le formula-decl nil nvectors nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (add_cancel2 formula-decl nil nvectors nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (barray type-eq-decl nil fseqs_def "structures/")
    (fseq type-eq-decl nil fseqs_def "structures/")
    (bool nonempty-type-eq-decl nil booleans nil)
    (> const-decl "bool" reals nil)
    (Vector type-eq-decl nil nvectors nil)
    (u!1 skolem-const-decl "Vector" nvectors nil)
    (Vect type-eq-decl nil nvectors nil)
    (v!1 skolem-const-decl "Vect(u!1`length)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil))
   shostak))
 (norm_ge_comps 0
  (norm_ge_comps-1 nil 3500823676
   ("" (skosimp*)
    (("" (expand "norm")
      (("" (expand "sqv")
        (("" (expand "*")
          (("" (rewrite "sqrt_sq_abs" :dir rl)
            ((""
              (case-replace
               "(LAMBDA (i: nat): u!1`seq(i) * u!1`seq(i)) =
                             (LAMBDA (i: nat): sq(u!1`seq(i)))")
              (("1" (hide -1)
                (("1" (lemma "sqrt_ge")
                  (("1" (inst?)
                    (("1" (assert)
                      (("1" (hide 2)
                        (("1" (lemma "sigma_nn_ge_comps")
                          (("1" (inst?)
                            (("1" (inst - "i!1")
                              (("1"
                                (assert)
                                (("1"
                                  (typepred "u!1`seq")
                                  (("1"
                                    (inst?)
                                    (("1"
                                      (assert)
                                      (("1"
                                        (replace -1)
                                        (("1"
                                          (assert)
                                          (("1"
                                            (lemma "sigma_Fnnr")
                                            (("1" (inst?) nil nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("2" (lemma "sigma_Fnnr") (("2" (inst?) nil nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (hide 2)
                (("2" (apply-extensionality 1 :hide? t)
                  (("2" (expand "sq") (("2" (propax) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((norm const-decl "nnreal" nvectors nil)
    (* const-decl "real" nvectors nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (nonneg_real nonempty-type-eq-decl nil real_types nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (sqrt_ge formula-decl nil sqrt "reals/")
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sigma_nn_ge_comps formula-decl nil sigma "reals/")
    (NOT const-decl "[bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (sq_0 formula-decl nil sq "reals/")
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (T_low type-eq-decl nil sigma "reals/")
    (T_high type-eq-decl nil sigma "reals/")
    (sigma def-decl "real" sigma "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/")
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (>= const-decl "bool" reals 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)
    (Vector type-eq-decl nil nvectors nil)
    (> const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (fseq type-eq-decl nil fseqs_def "structures/")
    (barray type-eq-decl nil fseqs_def "structures/")
    (nat nonempty-type-eq-decl nil naturalnumbers 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_sq_abs formula-decl nil sqrt "reals/")
    (sqv const-decl "nnreal" nvectors nil))
   shostak))
 (norm_triangle_TCC1 0
  (norm_triangle_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil)
   ((- const-decl "Vect(v`length)" nvectors nil)
    (+ const-decl "Vect(u`length)" nvectors nil)
    (- const-decl "Vect(u`length)" nvectors nil)
    (* const-decl "Vect(v`length)" nvectors nil)
    (minus_real_is_real application-judgement "real" reals nil))
   nil))
 (norm_triangle 0
  (norm_triangle-1 nil 3500825007
   ("" (skosimp*)
    (("" (expand "norm")
      (("" (rewrite "sq_sqrt")
        (("" (rewrite "sq_sqrt")
          (("" (rewrite "sq_sqrt")
            (("" (auto-rewrite "sqv_sub")
              (("" (auto-rewrite "scal_sub_distr")
                (("" (auto-rewrite "dot_distr_sub_left")
                  (("" (auto-rewrite "dot_distr_sub_right")
                    (("" (auto-rewrite "sub_cancel")
                      (("" (assert)
                        (("" (expand "sqv")
                          (("" (auto-rewrite "dot_scal_assoc")
                            (("" (auto-rewrite "dot_scal_right")
                              ((""
                                (auto-rewrite "dot_scal_left")
                                ((""
                                  (assert)
                                  ((""
                                    (lemma "dot_comm")
                                    ((""
                                      (inst -1 "v0!1" "v1!1")
                                      ((""
                                        (replace -1)
                                        ((""
                                          (hide -1)
                                          ((""
                                            (lemma "dot_comm")
                                            ((""
                                              (inst?)
                                              ((""
                                                (assert)
                                                ((""
                                                  (rewrite
                                                   "scal_sub_distr"
                                                   :dir
                                                   rl)
                                                  ((""
                                                    (lemma
                                                     "dot_distr_sub_right")
                                                    ((""
                                                      (inst
                                                       -1
                                                       "v2!1"
                                                       "2 * v1!1"
                                                       "2 * v0!1")
                                                      ((""
                                                        (replace -1)
                                                        ((""
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (norm const-decl "nnreal" nvectors nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (dot_scal_left formula-decl nil nvectors nil)
    (dot_distr_sub_right formula-decl nil nvectors nil)
    (dot_distr_sub_left formula-decl nil nvectors nil)
    (* const-decl "Vect(v`length)" nvectors nil)
    (minus_even_is_even application-judgement "even_int" integers nil)
    (minus_nzint_is_nzint application-judgement "nzint" integers nil)
    (dot_comm formula-decl nil nvectors nil)
    (scal_sub_distr formula-decl nil nvectors nil)
    (sqv_sub formula-decl nil nvectors nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
     real_types nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (- const-decl "Vect(u`length)" nvectors nil)
    (Vect type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sqv const-decl "nnreal" nvectors nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (Vector type-eq-decl nil nvectors nil)
    (> const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (fseq type-eq-decl nil fseqs_def "structures/")
    (barray type-eq-decl nil fseqs_def "structures/")
    (nat nonempty-type-eq-decl nil naturalnumbers 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_sqrt formula-decl nil sqrt "reals/"))
   shostak))
 (nzvec_has_nz 0
  (nzvec_has_nz-1 nil 3500825996
   ("" (skosimp*)
    (("" (typepred "nzv!1")
      (("" (flatten)
        (("" (lemma "norm_eq_0")
          (("" (inst?)
            (("" (assert)
              (("" (hide 2)
                (("" (apply-extensionality 1 :hide? t)
                  (("" (apply-extensionality 1 :hide? t)
                    (("" (inst?)
                      (("1" (assert)
                        (("1" (flatten)
                          (("1" (replace -2)
                            (("1" (expand "zero")
                              (("1"
                                (expand "const_seq")
                                (("1" (propax) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (typepred "nzv!1`seq")
                        (("2" (inst?)
                          (("2" (assert)
                            (("2" (replace -1)
                              (("2"
                                (expand "zero")
                                (("2"
                                  (expand "const_seq")
                                  (("2" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Nz_vector type-eq-decl nil nvectors nil)
    (norm const-decl "nnreal" nvectors nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (/= const-decl "boolean" notequal nil)
    (Vector type-eq-decl nil nvectors nil)
    (fseq type-eq-decl nil fseqs_def "structures/")
    (barray type-eq-decl nil fseqs_def "structures/")
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (norm_eq_0 formula-decl nil nvectors nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (zero const-decl "Zero_vect(n)" nvectors nil)
    (Zero_vect type-eq-decl nil nvectors nil)
    (Vect type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (posnat nonempty-type-eq-decl nil integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (< const-decl "bool" reals nil)
    (x!1 skolem-const-decl "nat" nvectors nil)
    (nzv!1 skolem-const-decl "Nz_vector" nvectors nil)
    (below type-eq-decl nil naturalnumbers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil))
   shostak))
 (nzvec_neq_zero_TCC1 0
  (nzvec_neq_zero_TCC1-1 nil 3500755723 ("" (subtype-tcc) nil nil) nil
   nil))
 (nzvec_neq_zero 0
  (nzvec_neq_zero-1 nil 3500826085
   ("" (skosimp*)
    (("" (lemma "nzvec_has_nz")
      (("" (inst?)
        (("" (skosimp*)
          (("" (replace -1)
            (("" (expand "zero")
              (("" (expand "const_seq") (("" (propax) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((nzvec_has_nz formula-decl nil nvectors nil)
    (zero const-decl "Zero_vect(n)" nvectors nil)
    (Nz_vector type-eq-decl nil nvectors nil)
    (norm const-decl "nnreal" nvectors nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (/= const-decl "boolean" notequal nil)
    (Vector type-eq-decl nil nvectors nil)
    (> const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (fseq type-eq-decl nil fseqs_def "structures/")
    (barray type-eq-decl nil fseqs_def "structures/")
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   shostak))
 (v_neq_0 0
  (v_neq_0-1 nil 3500826283
   ("" (skeep)
    (("" (lemma "norm_eq_0")
      (("" (inst?)
        (("" (assert)
          (("" (expand "norm")
            (("" (flatten)
              (("" (split +)
                (("1" (flatten)
                  (("1" (expand "sqv")
                    (("1" (case-replace "v*v = 0")
                      (("1" (assert) nil nil)
                       ("2" (hide 2)
                        (("2" (assert)
                          (("2" (expand "*")
                            (("2" (expand "fseq_appl")
                              (("2"
                                (lemma "sigma_Fnnr[nat]")
                                (("2"
                                  (inst?)
                                  (("2"
                                    (assert)
                                    (("2"
                                      (expand "sq")
                                      (("2" (assert) nil nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil)
                 ("2" (flatten)
                  (("2" (replace -2)
                    (("2" (expand "zero")
                      (("2" (expand "sq")
                        (("2" (lemma "sigma_zero[nat]")
                          (("2" (expand "fseq_appl")
                            (("2" (inst?) (("2" (assert) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((norm_eq_0 formula-decl nil nvectors nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (sigma_nnreal application-judgement "nnreal" sigma_nat "reals/")
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (zero const-decl "Zero_vect(n)" nvectors nil)
    (sigma_zero formula-decl nil sigma "reals/")
    (sigma_nat application-judgement "nat" sigma_nat "reals/")
    (* const-decl "real" nvectors nil)
    (Vect type-eq-decl nil nvectors nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (sqrt_0 formula-decl nil sqrt "reals/")
    (sigma_Fnnr formula-decl nil sigma "reals/")
    (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 "bool" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sq const-decl "nonneg_real" sq "reals/")
    (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)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (T_high type-eq-decl nil sigma "reals/")
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (T_low type-eq-decl nil sigma "reals/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (sqv const-decl "nnreal" nvectors nil)
    (norm const-decl "nnreal" nvectors nil)
    (Vector type-eq-decl nil nvectors nil)
    (> const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (fseq type-eq-decl nil fseqs_def "structures/")
    (barray type-eq-decl nil fseqs_def "structures/")
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil))
   shostak)))