SSL divergence.prf Sprache: Lisp

(divergence
(divergence_crit_oriented 0
  (divergence_crit_oriented-1 nil 3488708232 3488708254
   ("" (grind) nil nil) unchecked
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (/= const-decl "boolean" notequal nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (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)
    (nzint nonempty-type-eq-decl nil integers nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (Sign type-eq-decl nil sign "reals/")
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (* const-decl "real" vectors_2D "vectors/")
    (divergence_crit? const-decl "Criterion_2D" divergence nil)
    (symmetric_oriented_2D? const-decl "bool" predicate_coordination_2D
     nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (minus_real_is_real application-judgement "real" reals nil))
   3000 110 t shostak))
(divergence_crit_sum_indep 0
  (divergence_crit_sum_indep-1 nil 3488708264 3488708365
   ("" (expand "sum_independent_2D?")
    (("" (skeep)
      (("" (case "divergence_crit?(s,v,eps)(nv+nw)")
        (("1" (hide -2)
          (("1" (hide -2)
            (("1" (hide -2)
              (("1" (expand "divergence_pred?")
                (("1" (lemma "dot_pos_divergent")
                  (("1" (inst?)
                    (("1" (assert)
                      (("1" (expand "divergence_crit?")
                        (("1" (propax) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (hide -3) (("2" (hide -3) (("2" (grind) nil nil)) nil))
          nil))
        nil))
      nil))
    nil)
   unchecked
   ((sum_independent_2D? const-decl "bool" predicate_coordination_2D
     nil)
    (+ const-decl "Vector" vectors_2D "vectors/")
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (divergence_crit? const-decl "Criterion_2D" divergence nil)
    (Criterion_2D nonempty-type-eq-decl nil predicate_coordination_2D
     nil)
    (Sign type-eq-decl nil sign "reals/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (nzint nonempty-type-eq-decl nil integers nil)
    (/= const-decl "boolean" notequal nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (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)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (divergence_pred? const-decl "Vector_Predicate_2D" divergence nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (dot_pos_divergent formula-decl nil definitions nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil)
    (* const-decl "real" vectors_2D "vectors/"))
   30871 160 t shostak))
(divergence_pred_sum_closed 0
  (divergence_pred_sum_closed-1 nil 3488708903 3488709049
   ("" (expand "sum_closed_2D?")
    (("" (expand "divergence_pred?")
      (("" (skeep)
        (("" (case "nw = zero")
          (("1" (replace -1) (("1" (assert) nil nil)) nil)
           ("2" (case "nv = zero")
            (("1" (replace -1) (("1" (assert) nil nil)) nil)
             ("2" (lemma "dot_nneg_divergent")
              (("2" (inst-cp - "nv" "s")
                (("1" (inst-cp - "nw" "s")
                  (("1" (inst - "nv + nw" "s")
                    (("1" (assert)
                      (("1" (hide-all-but (-1 1 2))
                        (("1" (grind) nil nil)) nil))
                      nil)
                     ("2" (flatten)
                      (("2" (replace -1)
                        (("2" (assert)
                          (("2" (hide-all-but (-1 1 2))
                            (("2" (expand "zero")
                              (("2" (grind) nil nil)) nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (assert) nil nil))
                  nil)
                 ("2" (assert) nil nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   unchecked
   ((divergence_pred? const-decl "Vector_Predicate_2D" divergence nil)
    (zero const-decl "Vector" vectors_2D "vectors/")
    (Vector type-eq-decl nil vectors_2D "vectors/")
    (= const-decl "[T, T -> boolean]" equalities nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (real nonempty-type-from-decl nil reals nil)
    (add_zero_right formula-decl nil vectors_2D "vectors/")
    (dot_nneg_divergent formula-decl nil definitions nil) nil
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (* const-decl "real" vectors_2D "vectors/")
    (real_times_real_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (+ const-decl "Vector" vectors_2D "vectors/")
    (Nz_vect2 type-eq-decl nil vectors_2D "vectors/") nil
    (/= const-decl "boolean" notequal nil)
    (add_zero_left formula-decl nil vectors_2D "vectors/") nil)
   146458 220 t shostak))
(divergence_crit_coordinated 0
  (divergence_crit_coordinated-1 nil 3488708050 3488708213
   ("" (lemma "sum_indep_coordinated_oriented_2D")
    (("" (inst?)
      (("" (assert)
        (("" (hide 2)
          (("" (lemma "divergence_crit_oriented")
            (("" (assert)
              (("" (lemma "divergence_crit_sum_indep")
                (("" (assert)
                  (("" (lemma "divergence_pred_sum_closed")
                    (("" (propax) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   unfinished
   ((sum_indep_coordinated_oriented_2D formula-decl nil
     predicate_coordination_2D nil)
    (divergence_crit_oriented formula-decl nil divergence nil)
    (divergence_crit_sum_indep formula-decl nil divergence nil)
    (divergence_pred_sum_closed formula-decl nil divergence nil)
    (divergence_crit? const-decl "Criterion_2D" divergence nil)
    (Criterion_2D nonempty-type-eq-decl nil predicate_coordination_2D
     nil)
    (Sign type-eq-decl nil sign "reals/")
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (nzint nonempty-type-eq-decl nil integers nil)
    (/= const-decl "boolean" notequal nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (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)
    (divergence_pred? const-decl "Vector_Predicate_2D" divergence nil)
    (Vector_Predicate_2D nonempty-type-eq-decl nil
     predicate_coordination_2D nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (real nonempty-type-from-decl nil reals nil))
   44005 20 t shostak))
(divergence_crit_coordinated2 0
  (divergence_crit_coordinated2-1 nil 3488709154 3488709190
   ("" (lemma "divergence_crit_coordinated")
    (("" (expand "coordinated_oriented_2D?")
      (("" (expand "divergence_pred?")
        (("" (assert)
          (("" (skeep)
            (("" (inst - "vo" "vi" "nvo" "nvi" "s" "eps")
              (("" (assert) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   proved
   ((coordinated_oriented_2D? const-decl "bool"
     predicate_coordination_2D nil)
    (real nonempty-type-from-decl nil reals nil)
    (Vect2 type-eq-decl nil vectors_2D_def "vectors/")
    (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)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (/= const-decl "boolean" notequal nil)
    (nzint nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (- const-decl "[numfield -> numfield]" number_fields nil)
    (Sign type-eq-decl nil sign "reals/")
    (divergence_pred? const-decl "Vector_Predicate_2D" divergence nil)
    (divergence_crit_coordinated formula-decl nil divergence nil))
   36838 50 t shostak)))

quality100%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.