Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: fsq.prf Sprache: Lisp

Original von: PVS^©

(fsq
(default_TCC1 0
  (default_TCC1-1 nil 3410527823 3410692589 ("" (subtype-tcc) nil nil)
   unchecked
   ((member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (nonempty? const-decl "bool" sets nil))
   8 10 nil nil))
(doubleplus_TCC1 0
  (doubleplus_TCC1-1 nil 3410528601 3410692589
   ("" (subtype-tcc) nil nil) unchecked
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nonneg_int nonempty-type-eq-decl nil integers nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil))
   77 80 nil nil))
(doublecaret_TCC1 0
  (doublecaret_TCC1-1 nil 3410528601 3410692589
   ("" (skosimp*) (("" (grind) nil nil)) nil) unchecked
   ((int_plus_int_is_int application-judgement "int" integers nil)
    (int_min application-judgement "{k: int | k <= i AND k <= j}"
     real_defs 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)
    (min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil))
   161 140 t nil))
(doublecaret_TCC2 0
  (doublecaret_TCC2-1 nil 3411463305 3411463311
   ("" (subtype-tcc) nil nil) unchecked
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil))
   221 140 nil nil))
(plus_assoc_TCC1 0
  (plus_assoc_TCC1-1 nil 3410601808 3410692590
   ("" (subtype-tcc) nil nil) unchecked
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (int_minus_int_is_int application-judgement "int" integers 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)
    (minus_odd_is_odd application-judgement "odd_int" integers nil))
   61 30 nil nil))
(plus_assoc_TCC2 0
  (plus_assoc_TCC2-1 nil 3410601808 3410692590
   ("" (subtype-tcc) nil nil) unchecked
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides 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)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   75 70 nil nil))
(plus_assoc_TCC3 0
  (plus_assoc_TCC3-1 nil 3410601808 3410692590
   ("" (subtype-tcc) nil nil) unchecked
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers 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)
    (minus_odd_is_odd application-judgement "odd_int" integers nil))
   85 70 nil nil))
(plus_assoc_TCC4 0
  (plus_assoc_TCC4-1 nil 3410601808 3410692590
   ("" (subtype-tcc) nil nil) unchecked
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers 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)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   93 90 nil nil))
(plus_assoc 0
  (plus_assoc-1 nil 3410527843 3411463312
   ("" (skeep)
    (("" (apply-extensionality 1 :hide? t)
      (("1" (grind)
        (("1" (apply-extensionality 1 :hide? t)
          (("1" (grind) nil nil) ("2" (grind) nil nil)
           ("3" (skosimp*) (("3" (assert) nil nil)) nil)
           ("4" (skosimp*) (("4" (assert) nil nil)) nil)
           ("5" (skosimp*) (("5" (assert) nil nil)) nil))
          nil))
        nil)
       ("2" (skosimp*) (("2" (assert) nil nil)) nil)
       ("3" (skosimp*) (("3" (assert) nil nil)) nil)
       ("4" (skosimp*) (("4" (assert) nil nil)) nil)
       ("5" (skosimp*) (("5" (assert) nil nil)) nil))
      nil))
    nil)
   unchecked
   ((nat nonempty-type-eq-decl nil naturalnumbers nil)
    (T formal-type-decl nil fseqs nil) (fsq type-eq-decl nil fseqs nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields 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)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil))
   886 700 t shostak))
(empty_seq_fseq 0
  (empty_seq_fseq-1 nil 3410528601 3410692591
   ("" (judgement-tcc) nil nil) unchecked
   ((choose const-decl "(p)" sets nil)
    (default const-decl "T" fseqs nil)
    (empty_seq const-decl "fsq" fseqs nil))
   10 10 nil nil))
(emptyseq_fseq 0
  (emptyseq_fseq-1 nil 3411463305 3411463312
   ("" (judgement-tcc) nil nil) unchecked
   ((choose const-decl "(p)" sets nil)
    (default const-decl "T" fseqs nil)
    (empty_seq const-decl "fsq" fseqs nil))
   34 10 nil nil))
(singleton_TCC1 0
  (singleton_TCC1-1 nil 3473180360 nil ("" (subtype-tcc) nil nil)
   unchecked nil nil nil nil nil))
(deflt_TCC1 0
  (deflt_TCC1-1 nil 3410527823 3410692591 ("" (subtype-tcc) nil nil)
   unchecked
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (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)
    (choose const-decl "(p)" sets nil)
    (default const-decl "T" fseqs nil))
   27 30 nil nil))
(fseqs_eq 0
  (fseqs_eq-1 nil 3481896970 3481897145
   ("" (skeep)
    (("" (ground)
      (("" (decompose-equality)
        (("" (decompose-equality)
          (("" (typepred "fs1`seq")
            (("" (typepred "fs2`seq")
              (("" (case "x!1 >= fs1`length")
                (("1" (inst - "x!1")
                  (("1" (inst - "x!1") (("1" (assert) nil nil)) nil))
                  nil)
                 ("2" (hide -1)
                  (("2" (hide -1)
                    (("2" (inst - "x!1") (("2" (assert) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   unchecked
   ((T formal-type-decl nil fseqs 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)
    (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)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (default const-decl "T" fseqs nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs nil)
    (fseq type-eq-decl nil fseqs nil))
   174779 90 t shostak))
(fseq_length_zero 0
  (fseq_length_zero-1 nil 3481897245 3481897299
   ("" (skeep)
    (("" (lemma "fseqs_eq")
      (("" (inst - "fs" "emptyseq")
        (("1" (assert)
          (("1" (expand "empty_seq") (("1" (propax) nil nil)) nil))
          nil)
         ("2" (skeep)
          (("2" (expand "empty_seq") (("2" (propax) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   unchecked
   ((fseqs_eq formula-decl nil fseqs nil)
    (empty_seq_fseq name-judgement "fseq" fseqs nil)
    (fseq type-eq-decl nil fseqs nil)
    (barray type-eq-decl nil fseqs 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)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (T formal-type-decl nil fseqs nil) (fsq type-eq-decl nil fseqs nil)
    (empty_seq const-decl "fsq" fseqs nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (default const-decl "T" fseqs nil))
   54081 30 t shostak))
(singleton_length 0
  (singleton_length-1 nil 3473181682 3473182216
   (""
    (case "NOT FORALL (fsqz: fseq): fsqz = singleton(fsqz`seq(0)) IFF fsqz`length = 1")
    (("1" (hide 2)
      (("1" (skeep)
        (("1" (expand "singleton")
          (("1" (ground)
            (("1" (decompose-equality)
              (("1" (decompose-equality)
                (("1" (lift-if)
                  (("1" (ground)
                    (("1" (typepred "fsqz`seq")
                      (("1" (inst - "x!1") (("1" (assert) nil nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (skosimp*)
                (("2" (lift-if) (("2" (ground) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil)
     ("2" (skeep)
      (("2" (inst - "fs")
        (("2" (replace -1 :dir rl)
          (("2" (hide -1)
            (("2" (expand "singleton")
              (("2" (expand "singleton?")
                (("2" (ground)
                  (("1" (decompose-equality)
                    (("1" (skosimp*)
                      (("1" (expand "singleton")
                        (("1" (assert) nil nil)) nil))
                      nil)
                     ("2" (skosimp*)
                      (("2" (decompose-equality)
                        (("2" (lift-if)
                          (("2" (ground)
                            (("2" (expand "singleton")
                              (("2"
                                (replace -1)
                                (("2" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil)
                     ("3" (skeep)
                      (("3" (lift-if) (("3" (ground) nil nil)) nil))
                      nil))
                    nil)
                   ("2" (inst + "fs`seq(0)")
                    (("2" (replace -1)
                      (("2" (hide -1)
                        (("2" (decompose-equality)
                          (("1" (expand "singleton")
                            (("1" (propax) nil nil)) nil)
                           ("2" (decompose-equality)
                            (("2" (lift-if)
                              (("2"
                                (ground)
                                (("1"
                                  (replace -1)
                                  (("1"
                                    (expand "singleton")
                                    (("1" (propax) nil nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (expand "singleton")
                                  (("2" (propax) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   unchecked
   ((singleton const-decl "ne_fseq" fseqs nil)
    (ne_fseq type-eq-decl nil fseqs 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)
    (T formal-type-decl nil fseqs nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (fseq type-eq-decl nil fseqs nil)
    (barray type-eq-decl nil fseqs nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (real_ge_is_total_order name-judgement "(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)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (default const-decl "T" fseqs nil)
    (singleton? const-decl "bool" fseqs nil))
   219317 210 t shostak))
(oh_TCC1 0
  (oh_TCC1-1 nil 3410601808 3410692591 ("" (subtype-tcc) nil nil)
   unchecked
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (T formal-type-decl nil fseqs nil) (fsq type-eq-decl nil fseqs nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (default const-decl "T" fseqs nil)
    (fseq type-eq-decl nil fseqs nil)
    (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)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil))
   115 90 nil nil))
(oh_TCC2 0
  (oh_TCC2-1 nil 3410601808 3410692591 ("" (subtype-tcc) nil nil)
   unchecked
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (T formal-type-decl nil fseqs nil) (fsq type-eq-decl nil fseqs nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (fseq type-eq-decl nil fseqs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (choose const-decl "(p)" sets nil)
    (default const-decl "T" fseqs nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil))
   125 110 nil nil))
(concat_length_add 0
  (concat_length_add-1 nil 3481897577 3481897583
   ("" (skeep) (("" (expand "o") (("" (propax) nil nil)) nil)) nil)
   proved
   ((minus_odd_is_odd application-judgement "odd_int" integers nil)
    (O const-decl "fseq" fseqs nil))
   6188 20 t shostak))
(concat_rew_TCC1 0
  (concat_rew_TCC1-1 nil 3410601808 3410692591
   ("" (subtype-tcc) nil nil) unchecked
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (T formal-type-decl nil fseqs nil) (fsq type-eq-decl nil fseqs nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (default const-decl "T" fseqs nil)
    (fseq type-eq-decl nil fseqs nil)
    (int_minus_int_is_int application-judgement "int" integers 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)
    (minus_odd_is_odd application-judgement "odd_int" integers nil))
   33 30 nil nil))
(concat_rew 0
  (concat_rew-1 nil 3410602191 3411463312
   ("" (skeep)
    (("" (apply-extensionality 1 :hide? t)
      (("1" (grind) nil nil)
       ("2" (apply-extensionality 1 :hide? t)
        (("1" (grind) nil nil)
         ("2" (skosimp*) (("2" (assert) nil nil)) nil))
        nil)
       ("3" (skosimp*) (("3" (assert) nil nil)) nil))
      nil))
    nil)
   unchecked
   ((nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs nil)
    (fseq type-eq-decl nil fseqs nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (deflt const-decl "fseq" fseqs nil)
    (fsq type-eq-decl nil fseqs nil) (T formal-type-decl nil fseqs nil)
    (O const-decl "fseq" fseqs 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)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (default const-decl "T" fseqs nil)
    (choose const-decl "(p)" sets nil)
    (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))
   351 290 t shostak))
(member_composition 0
  (member_composition-1 nil 3473180360 3473181130
   ("" (skeep)
    (("" (expand "member")
      (("" (expand "o")
        (("" (ground)
          (("1" (skosimp*)
            (("1" (lift-if)
              (("1" (ground)
                (("1" (inst + "i!1") nil nil)
                 ("2" (inst 3 "i!1 - fs1`length") nil nil)
                 ("3" (typepred "i!1")
                  (("3" (hide-all-but (-1 1))
                    (("3" (expand "o") (("3" (propax) nil nil)) nil))
                    nil))
                  nil))
                nil))
              nil))
            nil)
           ("2" (skosimp*)
            (("2" (inst + "i!1")
              (("1" (typepred "i!1") (("1" (assert) nil nil)) nil)
               ("2" (typepred "i!1")
                (("2" (expand "o") (("2" (assert) nil nil)) nil)) nil))
              nil))
            nil)
           ("3" (skosimp*)
            (("3" (inst + "fs1`length + i!1")
              (("1" (assert) nil nil)
               ("2" (expand "o") (("2" (assert) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   unchecked
   ((minus_odd_is_odd application-judgement "odd_int" integers nil)
    (O const-decl "fseq" fseqs nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (below type-eq-decl nil naturalnumbers nil)
    (fseq type-eq-decl nil fseqs nil)
    (barray type-eq-decl nil fseqs nil) (< const-decl "bool" reals 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)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (member const-decl "bool" fseqs nil))
   296891 170 t shostak))
(concat_right_emptyseq 0
  (concat_right_emptyseq-1 nil 3481897352 3481897400
   ("" (skeep)
    (("" (lemma "fseqs_eq")
      (("" (inst?)
        (("" (assert)
          (("" (hide 2)
            (("" (ground)
              (("1" (expand "empty_seq")
                (("1" (expand "o") (("1" (propax) nil nil)) nil)) nil)
               ("2" (skeep)
                (("2" (expand "empty_seq")
                  (("2" (expand "o") (("2" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   unchecked
   ((fseqs_eq formula-decl nil fseqs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (empty_seq const-decl "fsq" fseqs nil)
    (fsq type-eq-decl nil fseqs nil) (T formal-type-decl nil fseqs nil)
    (O const-decl "fseq" fseqs nil) (fseq type-eq-decl nil fseqs nil)
    (barray type-eq-decl nil fseqs nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (empty_seq_fseq name-judgement "fseq" fseqs nil))
   47730 50 t shostak))
(concat_left_emptyseq 0
  (concat_left_emptyseq-1 nil 3481897405 3481897435
   ("" (skeep)
    (("" (lemma "fseqs_eq")
      (("" (inst?)
        (("" (assert)
          (("" (hide 2)
            (("" (ground)
              (("1" (expand "empty_seq")
                (("1" (expand "o") (("1" (propax) nil nil)) nil)) nil)
               ("2" (skeep)
                (("2" (expand "empty_seq")
                  (("2" (expand "o") (("2" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   unchecked
   ((fseqs_eq formula-decl nil fseqs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (empty_seq const-decl "fsq" fseqs nil)
    (fsq type-eq-decl nil fseqs nil) (T formal-type-decl nil fseqs nil)
    (O const-decl "fseq" fseqs nil) (fseq type-eq-decl nil fseqs nil)
    (barray type-eq-decl nil fseqs nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (empty_seq_fseq name-judgement "fseq" fseqs nil))
   30280 30 t shostak))
(member_singleton 0
  (member_singleton-1 nil 3473181181 3473181268
   ("" (skeep)
    (("" (expand "member")
      (("" (expand "singleton")
        (("" (ground)
          (("1" (skosimp*)
            (("1" (typepred "i!1")
              (("1" (expand "singleton") (("1" (assert) nil nil)) nil))
              nil))
            nil)
           ("2" (inst + "0") (("2" (assert) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   unchecked
   ((member const-decl "bool" fseqs nil)
    (below type-eq-decl nil naturalnumbers nil)
    (ne_fseq type-eq-decl nil fseqs nil)
    (> const-decl "bool" reals nil) (fseq type-eq-decl nil fseqs nil)
    (barray type-eq-decl nil fseqs nil)
    (T formal-type-decl nil fseqs 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)
    (< 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)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (singleton const-decl "ne_fseq" fseqs nil))
   86825 40 t shostak))
(caret_TCC1 0
  (caret_TCC1-1 nil 3410601808 3410692591
   ("" (skosimp*)
    (("" (expand "min") (("" (lift-if) (("" (ground) nil nil)) nil))
      nil))
    nil)
   unchecked
   ((min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil))
   89 60 t nil))
(caret_TCC2 0
  (caret_TCC2-1 nil 3410601808 3410692592 ("" (subtype-tcc) nil nil)
   unchecked
   ((int_minus_int_is_int application-judgement "int" integers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (T formal-type-decl nil fseqs nil) (fsq type-eq-decl nil fseqs nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (fseq type-eq-decl nil fseqs nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_min application-judgement "{k: int | k <= i AND k <= j}"
     real_defs nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil) (choose const-decl "(p)" sets nil)
    (default const-decl "T" fseqs nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil))
   221 200 nil nil))
(caret_TCC3 0
  (caret_TCC3-1 nil 3411463305 3411463312 ("" (subtype-tcc) nil nil)
   unchecked
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (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_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (choose const-decl "(p)" sets nil)
    (default const-decl "T" fseqs nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil))
   170 130 nil nil))
(hat_rewrite_TCC1 0
  (hat_rewrite_TCC1-1 nil 3410601808 3410692592
   ("" (skosimp*)
    (("" (expand "min") (("" (lift-if) (("" (ground) nil nil)) nil))
      nil))
    nil)
   unchecked
   ((min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil))
   48 40 t nil))
(hat_rewrite_TCC2 0
  (hat_rewrite_TCC2-1 nil 3411463305 3411463312
   ("" (subtype-tcc) nil nil) unchecked
   ((int_plus_int_is_int application-judgement "int" integers 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)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   52 50 nil nil))
(hat_rewrite 0
  (hat_rewrite-1 nil 3410602219 3411463381
   ("" (skeep)
    (("" (apply-extensionality 1 :hide? t)
      (("1" (grind) nil nil)
       ("2" (apply-extensionality 1 :hide? t)
        (("1" (grind) nil nil)
         ("2" (flatten) (("2" (ground) nil nil)) nil)
         ("3" (flatten) (("3" (ground) nil nil)) nil))
        nil)
       ("3" (hide 2) (("3" (flatten) (("3" (grind) nil nil)) nil)) nil)
       ("4" (hide 2) (("4" (flatten) (("4" (ground) nil nil)) nil))
        nil))
      nil))
    nil)
   unchecked
   ((nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs nil)
    (fseq type-eq-decl nil fseqs nil)
    (empty_seq const-decl "fsq" fseqs nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (IF const-decl "[boolean, T, T -> T]" if_def nil)
    (deflt const-decl "fseq" fseqs nil)
    (fsq type-eq-decl nil fseqs nil) (T formal-type-decl nil fseqs nil)
    (^ const-decl "fseq" fseqs nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (AND const-decl "[bool, bool -> bool]" 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)
    (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)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (minus_odd_is_odd application-judgement "odd_int" integers 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)
    (empty_seq_fseq name-judgement "fseq" fseqs nil)
    (default const-decl "T" fseqs nil)
    (choose const-decl "(p)" sets nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   46005 430 t shostak))
(o_assoc 0
  (o_assoc-1 nil 3410258465 3411463313
   ("" (skeep)
    (("" (apply-extensionality 1 :hide? t)
      (("1" (grind) nil nil)
       ("2" (apply-extensionality 1 :hide? t) (("2" (grind) nil nil))
        nil))
      nil))
    nil)
   unchecked
   ((nat nonempty-type-eq-decl nil naturalnumbers nil)
    (barray type-eq-decl nil fseqs nil)
    (fseq type-eq-decl nil fseqs nil) (O const-decl "fseq" fseqs nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (default const-decl "T" fseqs nil)
    (choose const-decl "(p)" sets nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (T formal-type-decl nil fseqs 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))
   500 430 t shostak))
(fseq1_TCC1 0
  (fseq1_TCC1-1 nil 3410692586 3410692592 ("" (subtype-tcc) nil nil)
   unchecked
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (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)
    (choose const-decl "(p)" sets nil)
    (default const-decl "T" fseqs nil))
   23 20 nil nil))
(fseq2_TCC1 0
  (fseq2_TCC1-1 nil 3411463305 3411463313 ("" (subtype-tcc) nil nil)
   unchecked
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (choose const-decl "(p)" sets nil)
    (default const-decl "T" fseqs nil))
   43 20 nil nil))
(fseq1_def 0
  (fseq1_def-1 nil 3410692610 3411463313 ("" (grind) nil nil) unchecked
   ((choose const-decl "(p)" sets nil)
    (default const-decl "T" fseqs nil)
    (fseq1 const-decl "fseq" fseqs nil))
   9 10 t shostak))
(rev_TCC1 0
  (rev_TCC1-1 nil 3411463305 3411463313 ("" (subtype-tcc) nil nil)
   unchecked
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (minus_odd_is_odd application-judgement "odd_int" integers nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   29 30 nil nil))
(rev_TCC2 0
  (rev_TCC2-1 nil 3411463305 3411463313 ("" (subtype-tcc) nil nil)
   unchecked
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (>= const-decl "bool" reals nil)
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (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)
    (choose const-decl "(p)" sets nil)
    (default const-decl "T" fseqs nil)
    (minus_odd_is_odd application-judgement "odd_int" integers nil))
   51 30 nil nil)))

¤ Dauer der Verarbeitung: 0.64 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.