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

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: TestSuite.vdmrt   Sprache: Lisp

Untersuchung PVS©
(real_metric_space
 (real_metric_space 0
  (real_metric_space-1 nil 3460456811 ("" (grind) nil nil)
   ((minus_odd_is_odd application-judgement "odd_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)
    (set type-eq-decl nil sets nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (minus_real_is_real application-judgement "real" reals nil)
    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
         nil)
    (real_dist const-decl "nnreal" real_metric_space nil)
    (space_zero? const-decl "bool" metric_spaces_def nil)
    (space_symmetric? const-decl "bool" metric_spaces_def nil)
    (space_triangle? const-decl "bool" metric_spaces_def nil)
    (metric_space? const-decl "bool" metric_spaces_def nil)
    (real_minus_real_is_real application-judgement "real" reals nil))
   shostak))
 (IMP_compactness_TCC1 0
  (IMP_compactness_TCC1-1 nil 3460718977
   ("" (lemma "real_metric_space")
    (("" (inst - "fullset[real]") nil nil)) nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil) (fullset const-decl "set" sets nil)
    (real_metric_space formula-decl nil real_metric_space nil))
   nil))
 (compact_induction 0
  (compact_induction-1 nil 3460795815
   ("" (skosimp*)
    (("" (label "compact_first" -1)
      (("" (label "compact_second" -2)
        (("" (label "compact_final" 1)
          (("" (expand "compact?")
            (("" (skosimp*)
              (("" (label "tot_oc" -3)
                (("" (inst - "XS!1")
                  (("" (inst - "XS!1")
                    (("" (expand "open_cover?")
                      (("" (prop)
                        (("1" (label "sets_open" -4)
                          (("1" (copy "compact_first")
                            (("1" (hide "compact_first")
                              (("1"
                                (skosimp -1)
                                (("1"
                                  (expand "finite_cover?")
                                  (("1"
                                    (prop)
                                    (("1"
                                      (label "first_ss" -1)
                                      (("1"
                                        (label "first_fin" -2)
                                        (("1"
                                          (expand "open_cover?" -3)
                                          (("1"
                                            (prop)
                                            (("1"
                                              (expand "subset?" -3)
                                              (("1"
                                                (expand "member")
                                                (("1"
                                                  (label
                                                   "first_is_cov"
                                                   -3)
                                                  (("1"
                                                    (label
                                                     "first_is_op"
                                                     -4)
                                                    (("1"
                                                      (expand
                                                       "Union"
                                                       "first_is_cov")
                                                      (("1"
                                                        (copy
                                                         "compact_second")
                                                        (("1"
                                                          (hide
                                                           "compact_second")
                                                          (("1"
                                                            (skosimp
                                                             -1)
                                                            (("1"
                                                              (expand
                                                               "open_cover?"
                                                               -3)
                                                              (("1"
                                                                (prop)
                                                                (("1"
                                                                  (label
                                                                   "second_ss"
                                                                   -1)
                                                                  (("1"
                                                                    (label
                                                                     "second_fin"
                                                                     -2)
                                                                    (("1"
                                                                      (label
                                                                       "second_cov"
                                                                       -3)
                                                                      (("1"
                                                                        (label
                                                                         "second_op"
                                                                         -4)
                                                                        (("1"
                                                                          (expand
                                                                           "Union"
                                                                           "second_cov")
                                                                          (("1"
                                                                            (inst
                                                                             +
                                                                             "union[set[real]](YS!1,YS!2)")
                                                                            (("1"
                                                                              (expand
                                                                               "open_cover?")
                                                                              (("1"
                                                                                (expand
                                                                                 "subset?")
                                                                                (("1"
                                                                                  (expand
                                                                                   "member")
                                                                                  (("1"
                                                                                    (prop)
                                                                                    (("1"
                                                                                      (skosimp*)
                                                                                      (("1"
                                                                                        (expand
                                                                                         "union")
                                                                                        (("1"
                                                                                          (expand
                                                                                           "member")
                                                                                          (("1"
                                                                                            (prop)
                                                                                            (("1"
                                                                                              (label
                                                                                               "in_first"
                                                                                               -1)
                                                                                              (("1"
                                                                                                (inst
                                                                                                 "first_ss"
                                                                                                 "x!1")
                                                                                                (("1"
                                                                                                  (prop)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil)
                                                                                             ("2"
                                                                                              (label
                                                                                               "in_second"
                                                                                               -1)
                                                                                              (("2"
                                                                                                (inst
                                                                                                 "second_ss"
                                                                                                 "x!1")
                                                                                                (("2"
                                                                                                  (prop)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil)
                                                                                     ("2"
                                                                                      (lemma
                                                                                       "infinite_union[set[real]]")
                                                                                      (("2"
                                                                                        (label
                                                                                         "inf_un"
                                                                                         -1)
                                                                                        (("2"
                                                                                          (inst
                                                                                           "inf_un"
                                                                                           "YS!1"
                                                                                           "YS!2")
                                                                                          (("2"
                                                                                            (assert)
                                                                                            nil
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil)
                                                                                     ("3"
                                                                                      (skosimp*)
                                                                                      (("3"
                                                                                        (case
                                                                                         "x!1 <= (c!1 + d!1)/2")
                                                                                        (("1"
                                                                                          (label
                                                                                           "caseonx1"
                                                                                           -1)
                                                                                          (("1"
                                                                                            (inst
                                                                                             "first_is_cov"
                                                                                             "x!1")
                                                                                            (("1"
                                                                                              (expand
                                                                                               "Union")
                                                                                              (("1"
                                                                                                (assert)
                                                                                                (("1"
                                                                                                  (skosimp
                                                                                                   "first_is_cov")
                                                                                                  (("1"
                                                                                                    (inst
                                                                                                     +
                                                                                                     "a!1")
                                                                                                    (("1"
                                                                                                      (expand
                                                                                                       "union")
                                                                                                      (("1"
                                                                                                        (expand
                                                                                                         "member")
                                                                                                        (("1"
                                                                                                          (propax)
                                                                                                          nil
                                                                                                          nil))
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil)
                                                                                         ("2"
                                                                                          (inst
                                                                                           "second_cov"
                                                                                           "x!1")
                                                                                          (("2"
                                                                                            (assert)
                                                                                            (("2"
                                                                                              (skosimp
                                                                                               "second_cov")
                                                                                              (("2"
                                                                                                (expand
                                                                                                 "Union")
                                                                                                (("2"
                                                                                                  (inst
                                                                                                   "compact_final"
                                                                                                   "a!1")
                                                                                                  (("2"
                                                                                                    (expand
                                                                                                     "union")
                                                                                                    (("2"
                                                                                                      (expand
                                                                                                       "member")
                                                                                                      (("2"
                                                                                                        (propax)
                                                                                                        nil
                                                                                                        nil))
                                                                                                      nil))
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil)
                                                                                     ("4"
                                                                                      (skosimp*)
                                                                                      (("4"
                                                                                        (expand
                                                                                         "union")
                                                                                        (("4"
                                                                                          (expand
                                                                                           "member")
                                                                                          (("4"
                                                                                            (prop)
                                                                                            (("1"
                                                                                              (inst
                                                                                               "first_ss"
                                                                                               "C!1")
                                                                                              (("1"
                                                                                                (assert)
                                                                                                (("1"
                                                                                                  (inst
                                                                                                   "sets_open"
                                                                                                   "C!1")
                                                                                                  (("1"
                                                                                                    (assert)
                                                                                                    nil
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil)
                                                                                             ("2"
                                                                                              (inst
                                                                                               "second_ss"
                                                                                               "C!1")
                                                                                              (("2"
                                                                                                (inst
                                                                                                 "sets_open"
                                                                                                 "C!1")
                                                                                                (("2"
                                                                                                  (assert)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
                                                                      nil))
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("2" (expand "subset?")
                          (("2" (expand "member")
                            (("2" (skosimp*)
                              (("2"
                                (inst "tot_oc" "x!1")
                                (("2"
                                  (expand "Union")
                                  (("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("3" (expand "subset?")
                          (("3" (expand "member")
                            (("3" (skosimp*)
                              (("3"
                                (inst "tot_oc" "x!1")
                                (("3"
                                  (expand "Union")
                                  (("3" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil)
                         ("4" (expand "subset?")
                          (("4" (expand "member")
                            (("4" (skosimp*)
                              (("4"
                                (inst "tot_oc" "x!1")
                                (("4"
                                  (expand "Union")
                                  (("4" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (open_cover? const-decl "bool" compactness nil)
    (finite_cover? const-decl "bool" compactness nil)
    (subset? const-decl "bool" sets nil)
    (Union const-decl "set" sets nil)
    (a!1 skolem-const-decl "(YS!2)" real_metric_space nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (a!1 skolem-const-decl "(YS!1)" real_metric_space nil)
    (YS!2 skolem-const-decl "set[set[real]]" real_metric_space nil)
    (YS!1 skolem-const-decl "set[set[real]]" real_metric_space nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (< const-decl "bool" reals nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (<= const-decl "bool" reals nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (infinite_union formula-decl nil infinite_sets_def nil)
    (union const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (compact? const-decl "bool" compactness nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   shostak))
 (seq_intv_scaf_TCC1 0
  (seq_intv_scaf_TCC1-1 nil 3460814665 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (< const-decl "bool" reals nil) (set type-eq-decl nil sets nil)
    (>= const-decl "bool" reals nil)
    (nnreal type-eq-decl nil real_types nil)
    (real_dist const-decl "nnreal" real_metric_space nil)
    (open_cover? const-decl "bool" compactness nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (open? const-decl "bool" metric_spaces nil)
    (Union const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil))
   nil))
 (seq_intv_scaf_TCC2 0
  (seq_intv_scaf_TCC2-1 nil 3460814665 ("" (termination-tcc) nil nil)
   ((member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil))
   nil))
 (seq_intv_scaf_TCC3 0
  (seq_intv_scaf_TCC3-1 nil 3460814665 ("" (subtype-tcc) nil nil)
   ((NOT const-decl "[bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil) (set type-eq-decl nil sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (injective? const-decl "bool" functions nil)
    (is_finite const-decl "bool" finite_sets nil)
    (Union const-decl "set" sets nil)
    (real_dist const-decl "nnreal" real_metric_space nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (open? const-decl "bool" metric_spaces nil)
    (open_cover? const-decl "bool" compactness nil)
    (finite_cover? const-decl "bool" compactness nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
 (seq_intv_scaf_TCC4 0
  (seq_intv_scaf_TCC4-1 nil 3460814665 ("" (termination-tcc) nil nil)
   ((member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (injective? const-decl "bool" functions nil)
    (is_finite const-decl "bool" finite_sets nil)
    (Union const-decl "set" sets nil)
    (real_dist const-decl "nnreal" real_metric_space nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (open? const-decl "bool" metric_spaces nil)
    (open_cover? const-decl "bool" compactness nil)
    (finite_cover? const-decl "bool" compactness nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
 (seq_intv_scaf_TCC5 0
  (seq_intv_scaf_TCC5-1 nil 3460814665 ("" (subtype-tcc) nil nil)
   ((NOT const-decl "[bool -> bool]" booleans nil)
    (< const-decl "bool" reals nil) (set type-eq-decl nil sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans 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)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (injective? const-decl "bool" functions nil)
    (is_finite const-decl "bool" finite_sets nil)
    (Union const-decl "set" sets nil)
    (real_dist const-decl "nnreal" real_metric_space nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (open? const-decl "bool" metric_spaces nil)
    (open_cover? const-decl "bool" compactness nil)
    (finite_cover? const-decl "bool" compactness nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
 (seq_intv_scaf_TCC6 0
  (seq_intv_scaf_TCC6-1 nil 3460814665 ("" (termination-tcc) nil nil)
   ((member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (injective? const-decl "bool" functions nil)
    (is_finite const-decl "bool" finite_sets nil)
    (Union const-decl "set" sets nil)
    (real_dist const-decl "nnreal" real_metric_space nil)
    (nnreal type-eq-decl nil real_types nil)
    (>= const-decl "bool" reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (real nonempty-type-from-decl nil reals nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (open? const-decl "bool" metric_spaces nil)
    (open_cover? const-decl "bool" compactness nil)
    (finite_cover? const-decl "bool" compactness nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
 (seq_inv_scaf_decreasing 0
  (seq_inv_scaf_decreasing-1 nil 3460811042
   ("" (skolem 1 ("c" "d" "YS"))
    (("" (skeep)
      (("" (split)
        (("1" (generalize "n" "m")
          (("1" (induct "m")
            (("1" (grind) nil nil)
             ("2" (skosimp*)
              (("2" (expand "seq_intv_scaf" 1)
                (("2" (name "W" "seq_intv_scaf(c,d,YS)(j!1)")
                  (("2" (replace -1)
                    (("2" (hide -1)
                      (("2"
                        (name "P" "NOT (EXISTS (XS: set[set[real]]):
                subset?(XS, YS) AND
                 open_cover?(XS,
                             LAMBDA (x: real):
                               W`1 <= x AND x <= (W`1 + W`2) / 2))")
                        (("2" (hide -1) (("2" (grind) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("2" (expand "subset?")
          (("2" (skosimp*)
            (("2" (expand "member")
              (("2" (expand "seq_intv_scaf" -1)
                (("2" (name "W" "seq_intv_scaf(c,d,YS)(n)")
                  (("2" (replace -1)
                    (("2" (hide -1)
                      (("2"
                        (name "P" "NOT (EXISTS (XS: set[set[real]]):
                subset?(XS, YS) AND
                 open_cover?(XS,
                             LAMBDA (x: real):
                               W`1 <= x AND x <= (W`1 + W`2) / 2))")
                        (("2" (hide -1) (("2" (grind) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil)
         ("3" (generalize "n" "m")
          (("3" (induct "m")
            (("1" (expand "seq_intv_scaf")
              (("1" (expand "^")
                (("1" (expand "expt") (("1" (assert) nil nil)) nil))
                nil))
              nil)
             ("2" (skosimp*)
              (("2" (name "W" "seq_intv_scaf(c,d,YS)(j!1)")
                (("2" (replace -1)
                  (("2" (label "name_w" -1)
                    (("2" (hide -1)
                      (("2" (expand "seq_intv_scaf")
                        (("2" (reveal "name_w")
                          (("2" (replace "name_w")
                            (("2" (hide "name_w")
                              (("2"
                                (name
                                 "P"
                                 "NOT (EXISTS (XS: set[set[real]]):
                subset?(XS, YS) AND
                 finite_cover?(XS,
                               LAMBDA (x: real):
                                 W`1 <= x AND x <= (W`1 + W`2) / 2))")
                                (("2"
                                  (replace -1)
                                  (("2"
                                    (hide -1)
                                    (("2" (grind) nil nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((posint_exp application-judgement "posint" exponentiation nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (^ const-decl "real" exponentiation 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)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (posint_times_posint_is_posint application-judgement "posint"
     integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (posrat_div_posrat_is_posrat application-judgement "posrat"
     rationals nil)
    (posnat_expt application-judgement "posnat" exponentiation nil)
    (expt def-decl "real" exponentiation nil)
    (real_minus_real_is_real application-judgement "real" reals nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (>= const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (< const-decl "bool" reals nil) (set type-eq-decl nil sets nil)
    (nnreal type-eq-decl nil real_types nil)
    (real_dist const-decl "nnreal" real_metric_space nil)
    (open_cover? const-decl "bool" compactness nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (<= const-decl "bool" reals nil)
    (seq_intv_scaf def-decl "[real, real]" real_metric_space nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (finite_cover? const-decl "bool" compactness nil)
    (open? const-decl "bool" metric_spaces nil)
    (Union const-decl "set" sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (injective? const-decl "bool" functions nil)
    (member const-decl "bool" sets nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
    (nznum nonempty-type-eq-decl nil number_fields nil)
    (/= const-decl "boolean" notequal nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (subset? const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_div_nzreal_is_real application-judgement "real" reals nil)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (pred type-eq-decl nil defined_types nil))
   shostak))
 (compact_seq_induction 0
  (compact_seq_induction-1 nil 3460812837
   ("" (skolem 1 ("c" "d"))
    (("" (prop)
      (("" (expand "compact?")
        (("" (skosimp*)
          (("" (label "big_open_cov" -1)
            (("" (label "exists_fs" 1)
              (("" (label "smaller_sc" 2)
                (("" (inst "smaller_sc" "XS!1")
                  (("" (assert)
                    (("" (induct "n" "smaller_sc")
                      (("1" (skosimp*)
                        (("1" (expand "seq_intv_scaf")
                          (("1" (inst "exists_fs" "XS!2")
                            (("1" (assert) nil nil)) nil))
                          nil))
                        nil)
                       ("2" (skosimp*)
                        (("2" (name "W" "seq_intv_scaf(c,d,XS!1)(j!1)")
                          (("2" (replace -1)
                            (("2" (label "name_w" -1)
                              (("2"
                                (hide "name_w")
                                (("2"
                                  (expand "seq_intv_scaf")
                                  (("2"
                                    (reveal "name_w")
                                    (("2"
                                      (replace "name_w")
                                      (("2"
                                        (hide "name_w")
                                        (("2"
                                          (case
                                           "(EXISTS (XS: set[set[real]]):
                                subset?(XS, XS!1) AND
                                 finite_cover?(XS,
                                               LAMBDA
                                               (x: real):
                                               W`1 <= x
                                               AND
                                               x <= (W`1 + W`2) / 2))")
                                          (("1"
                                            (assert)
                                            (("1"
                                              (replace -1)
                                              (("1"
                                                (skosimp*)
                                                (("1"
                                                  (inst
                                                   +
                                                   "union[set[real]](XS!2,XS!3)")
                                                  (("1"
                                                    (expand "subset?")
                                                    (("1"
                                                      (expand "member")
                                                      (("1"
                                                        (prop)
                                                        (("1"
                                                          (expand
                                                           "union")
                                                          (("1"
                                                            (expand
                                                             "member")
                                                            (("1"
                                                              (skolem
                                                               1
                                                               ("x"))
                                                              (("1"
                                                                (inst
                                                                 -
                                                                 "x")
                                                                (("1"
                                                                  (inst
                                                                   -
                                                                   "x")
                                                                  (("1"
                                                                    (prop)
                                                                    nil
                                                                    nil))
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (expand
                                                           "finite_cover?")
                                                          (("2"
                                                            (prop)
                                                            (("1"
                                                              (lemma
                                                               "infinite_union[set[real]]")
                                                              (("1"
                                                                (inst
                                                                 -
                                                                 "XS!2"
                                                                 "XS!3")
                                                                (("1"
                                                                  (prop)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil)
                                                             ("2"
                                                              (label
                                                               "XS3_ss"
                                                               -1)
                                                              (("2"
                                                                (label
                                                                 "XS2_ss"
                                                                 -6)
                                                                (("2"
                                                                  (label
                                                                   "XS3_oc"
                                                                   -3)
                                                                  (("2"
                                                                    (label
                                                                     "XS2_oc"
                                                                     -5)
                                                                    (("2"
                                                                      (expand
                                                                       "open_cover?")
                                                                      (("2"
                                                                        (prop)
                                                                        (("1"
                                                                          (expand
                                                                           "Union")
                                                                          (("1"
                                                                            (expand
                                                                             "subset?")
                                                                            (("1"
                                                                              (expand
                                                                               "member")
                                                                              (("1"
                                                                                (assert)
                                                                                (("1"
                                                                                  (skosimp*)
                                                                                  (("1"
                                                                                    (case
                                                                                     "x!1 <= (W`1 + W`2)/2")
                                                                                    (("1"
                                                                                      (inst
                                                                                       "XS3_oc"
                                                                                       "x!1")
                                                                                      (("1"
                                                                                        (assert)
                                                                                        (("1"
                                                                                          (skosimp*)
                                                                                          (("1"
                                                                                            (inst
                                                                                             "XS3_ss"
                                                                                             "a!1")
                                                                                            (("1"
                                                                                              (inst
                                                                                               +
                                                                                               "a!1")
                                                                                              (("1"
                                                                                                (expand
                                                                                                 "union")
                                                                                                (("1"
                                                                                                  (expand
                                                                                                   "member")
                                                                                                  (("1"
                                                                                                    (propax)
                                                                                                    nil
                                                                                                    nil))
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil)
                                                                                     ("2"
                                                                                      (inst
                                                                                       -9
                                                                                       "x!1")
                                                                                      (("2"
                                                                                        (assert)
                                                                                        (("2"
                                                                                          (skosimp*)
                                                                                          (("2"
                                                                                            (inst
                                                                                             +
                                                                                             "a!1")
                                                                                            (("2"
                                                                                              (expand
                                                                                               "union")
                                                                                              (("2"
                                                                                                (expand
                                                                                                 "member")
                                                                                                (("2"
                                                                                                  (propax)
                                                                                                  nil
                                                                                                  nil))
                                                                                                nil))
                                                                                              nil))
                                                                                            nil))
                                                                                          nil))
                                                                                        nil))
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil)
                                                                         ("2"
                                                                          (skosimp*)
                                                                          (("2"
                                                                            (expand
                                                                             "union")
                                                                            (("2"
                                                                              (expand
                                                                               "member")
                                                                              (("2"
                                                                                (inst
                                                                                 -5
                                                                                 "C!1")
                                                                                (("2"
                                                                                  (inst
                                                                                   -9
                                                                                   "C!1")
                                                                                  (("2"
                                                                                    (assert)
                                                                                    (("2"
                                                                                      (assert)
                                                                                      nil
                                                                                      nil))
                                                                                    nil))
                                                                                  nil))
                                                                                nil))
                                                                              nil))
                                                                            nil))
                                                                          nil))
                                                                        nil))
--> --------------------

--> maximum size reached

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

¤ Dauer der Verarbeitung: 0.82 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.


Bot Zugriff