Gedichte Musik Bilder Quellcodebibliothek Diashow Normaldarstellung
Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/graphs/   (Beweissystem der NASA Version 6.0.9©)  Datei vom 28.9.2014 mit Größe 14 kB image not shown  

Quelle  ind_paths.prf   Sprache: Lisp

 
(ind_paths
 (independent?_TCC1 0
  (independent?_TCC1-1 nil 3507100597 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (T formal-type-decl nil ind_paths nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (prewalk type-eq-decl nil walks 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)
    (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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (independent?_TCC2 0
  (independent?_TCC2-1 nil 3507100597 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (T formal-type-decl nil ind_paths nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (prewalk type-eq-decl nil walks 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)
    (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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (independent?_comm 0
  (independent?_comm-1 nil 3507100597
   ("" (skosimp*)
    (("" (expand "independent?")
      (("" (skosimp*)
        (("" (inst -1 "j!1" "i!1") (("" (assert) nil))))))))
    nil)
   ((independent? const-decl "bool" ind_paths 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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil))
 (independent_ne 0
  (independent_ne-1 nil 3507100597
   ("" (skosimp*)
    (("" (expand "independent?")
      (("" (replace -3)
        (("" (hide -3)
          (("" (inst - "1" "1") (("" (assert) nil))))))))))
    nil)
   ((independent? const-decl "bool" ind_paths 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_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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))
   nil))
 (ind_path_set_2 0
  (ind_path_set_2-1 nil 3507100597
   ("" (skosimp*)
    (("" (lemma "card_2_has_2[Path_from(G!1,s!1,t!1)]")
      (("" (inst?)
        (("" (assert)
          (("" (skosimp*)
            (("" (inst 2 "x!1" "y!1")
              (("" (expand "ind_path_set?")
                (("" (inst?)
                  (("" (assert)
                    (("" (expand "path_from?")
                      (("" (propax) nil))))))))))))))))))))
    nil)
   ((Path_from type-eq-decl nil paths nil)
    (path_from? const-decl "bool" paths nil)
    (graph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (pregraph type-eq-decl nil graphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (doubleton type-eq-decl nil doubletons nil)
    (dbl const-decl "set[T]" doubletons nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (/= const-decl "boolean" notequal nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (prewalk type-eq-decl nil walks 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)
    (finseq type-eq-decl nil finite_sequences nil)
    (T formal-type-decl nil ind_paths nil)
    (below type-eq-decl nil nat_types nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (card_2_has_2 formula-decl nil finite_sets nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (ind_path_set? const-decl "bool" ind_paths nil)
    (set_of_paths type-eq-decl nil ind_paths nil)
    (is_finite const-decl "bool" finite_sets nil))
   nil))
 (internal_verts_TCC1 0
  (internal_verts_TCC1-1 nil 3507100597 ("" (subtype-tcc) nil nil)
   ((boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (number nonempty-type-decl nil numbers nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (> const-decl "bool" reals nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (T formal-type-decl nil ind_paths nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (prewalk type-eq-decl nil walks 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)
    (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)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil))
   nil))
 (internal_verts_TCC2 0
  (internal_verts_TCC2-1 nil 3507100597
   ("" (skosimp*)
    (("" (lemma "finite_subset[T]")
      (("" (inst?)
        (("1" (assert)
          (("1" (inst - "verts_of(w!1)")
            (("1" (assert) (("1" (hide 2) (("1" (grind) nil)))))))))
         ("2" (hide 2) (("2" (skosimp*) (("2" (assert) nil))))))))))
    nil)
   ((T formal-type-decl nil ind_paths nil)
    (finite_subset formula-decl nil finite_sets nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (below type-eq-decl nil naturalnumbers nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (verts_of const-decl "finite_set[T]" walks nil)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (set type-eq-decl nil sets 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)
    (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)
    (below type-eq-decl nil nat_types nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (> const-decl "bool" reals nil)
    (prewalk type-eq-decl nil walks nil)
    (w!1 skolem-const-decl "prewalk[T]" ind_paths nil)
    (int_minus_int_is_int application-judgement "int" integers nil))
   nil))
 (indep?_lem 0
  (indep?_lem-1 nil 3507100597
   ("" (skosimp*)
    (("" (expand "indep?")
      (("" (expand "independent?")
        (("" (prop)
          (("1" (skosimp*)
            (("1" (expand "empty?")
              (("1" (expand "member")
                (("1" (expand "intersection")
                  (("1" (expand "internal_verts")
                    (("1" (expand "member")
                      (("1" (expand "finseq_appl")
                        (("1" (inst - "seq(w1!1)(i!1)")
                          (("1" (prop)
                            (("1" (inst?) (("1" (assert) nil)))
                             ("2" (inst + "j!1")
                              (("2" (assert) nil)))))
                           ("2" (assert) nil)))))))))))))))))
           ("2" (expand "empty?")
            (("2" (expand "intersection")
              (("2" (expand "internal_verts")
                (("2" (expand "member")
                  (("2" (expand "finseq_appl")
                    (("2" (skosimp*)
                      (("2" (inst - "i!1" "i!2")
                        (("2" (assert) nil))))))))))))))))))))))
    nil)
   ((finite_intersection1 application-judgement "finite_set"
     finite_sets nil)
    (indep? const-decl "bool" ind_paths nil)
    (empty? const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil)
    (T formal-type-decl nil ind_paths nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (below type-eq-decl nil nat_types nil)
    (finseq type-eq-decl nil finite_sequences nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans nil)
    (number_field_pred const-decl "[number -> boolean]" number_fields
     nil)
    (number_field nonempty-type-from-decl nil number_fields nil)
    (real_pred const-decl "[number_field -> boolean]" reals nil)
    (real nonempty-type-from-decl nil reals nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (> const-decl "bool" reals nil)
    (prewalk type-eq-decl nil walks nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (>= const-decl "bool" reals nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (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)
    (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
     nil)
    (internal_verts const-decl "finite_set[T]" ind_paths nil)
    (member const-decl "bool" sets nil)
    (independent? const-decl "bool" ind_paths nil))
   nil)))

100%


¤ Dauer der Verarbeitung: 0.22 Sekunden  (vorverarbeitet)  ¤

*© Formatika GbR, Deutschland




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.