products/sources/formale Sprachen/PVS/vectors/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: univMinim.ml   Sprache: SML

Original von: PVS©
(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)
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.86 Sekunden  (vorverarbeitet)  ¤



Download des
Quellennavigators
Download des
sprechenden Kalenders

Eigene Datei ansehen




Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.


Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.


Bot Zugriff