Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: ind_paths.pvs Sprache: Lisp

Original von: PVS^©

(ind_paths
(independent?_TCC1 0
  (independent?_TCC1-1 nil 3507100931 ("" (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 3507100931 ("" (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 3507100931
   ("" (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 3507100931
   ("" (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 3507100931
   ("" (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)
    (digraph type-eq-decl nil digraphs nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (predigraph type-eq-decl nil digraphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (edgetype type-eq-decl nil digraphs 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)
    (set type-eq-decl nil sets nil))
   nil))
(internal_verts_TCC1 0
  (internal_verts_TCC1-1 nil 3507100931 ("" (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 3507100931
   ("" (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 3507100931
   ("" (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[T]"
     ind_paths 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)))

¤ Dauer der Verarbeitung: 0.46 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
Eigene Datei ansehen

Haftungshinweis

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

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.