Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: graph_ops.prf Sprache: Lisp

Original von: PVS^©

(graph_ops
(union_TCC1 0
  (union_TCC1-1 nil 3251040627
   ("" (skosimp*)
    (("" (expand "union")
      (("" (expand "member")
        (("" (flatten)
          (("" (prop)
            (("1" (typepred "G1!1")
              (("1" (inst?)
                (("1" (assert)
                  (("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
                nil))
              nil)
             ("2" (typepred "G2!1")
              (("2" (inst?)
                (("2" (assert)
                  (("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((union const-decl "set" sets nil)
    (graph type-eq-decl nil graphs nil)
    (pregraph type-eq-decl nil graphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans 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)
    (T formal-type-decl nil graph_ops nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (member const-decl "bool" sets nil))
   nil))
(del_vert_TCC1 0
  (del_vert_TCC1-1 nil 3251040627
   ("" (skosimp*)
    (("" (lemma "finite_subset[doubleton[T]]")
      (("" (inst?)
        (("" (inst - "edges(G!1)")
          (("" (assert) (("" (hide 2) (("" (grind) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil graph_ops nil)
    (finite_subset formula-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (NOT const-decl "[bool -> bool]" booleans 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))
   nil))
(del_vert_TCC2 0
  (del_vert_TCC2-1 nil 3307708397 ("" (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)
    (T formal-type-decl nil graph_ops nil)
    (set type-eq-decl nil sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dbl const-decl "set[T]" doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (pregraph type-eq-decl nil graphs nil)
    (graph type-eq-decl nil graphs nil)
    (nil application-judgement "finite_set[T]" graph_ops nil)
    (/= const-decl "boolean" notequal nil)
    (member const-decl "bool" sets nil)
    (remove const-decl "set" sets nil))
   nil))
(del_edge_TCC1 0
  (del_edge_TCC1-1 nil 3251040627
   ("" (skosimp*)
    (("" (expand "remove")
      (("" (flatten)
        (("" (expand "member")
          (("" (typepred "G!1")
            (("" (inst?)
              (("" (assert)
                (("" (inst?) (("" (assert) nil))))))))))))))))
    nil)
   ((remove const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil graph_ops nil)
    (set type-eq-decl nil sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dbl const-decl "set[T]" doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (pregraph type-eq-decl nil graphs nil)
    (graph type-eq-decl nil graphs nil))
   nil))
(adjacent_TCC1 0
  (adjacent_TCC1-1 nil 3393146609
   ("" (skosimp*)
    (("" (lemma "finite_subset[T]")
      (("" (inst?)
        (("" (inst -1 "vert(G!1)")
          (("" (assert) (("" (hide 2) (("" (grind) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil graph_ops nil)
    (finite_subset formula-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (nil application-judgement "finite_set[T]" graph_ops nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (edge? const-decl "bool" graphs 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(del_vert_still_in 0
  (del_vert_still_in-1 nil 3251040627
   ("" (skosimp*)
    (("" (expand "del_vert")
      (("" (expand "remove")
        (("" (expand "member") (("" (assert) nil))))))))
    nil)
   ((del_vert const-decl "graph[T]" graph_ops nil)
    (member const-decl "bool" sets nil)
    (remove const-decl "set" sets nil))
   nil))
(size_del_vert 0
  (size_del_vert-1 nil 3251040627
   ("" (skosimp*)
    (("" (typepred "v!1")
      (("" (expand "del_vert")
        (("" (expand "size") (("" (rewrite "card_remove") nil))))))))
    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)
    (T formal-type-decl nil graph_ops nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (size const-decl "nat" graphs nil)
    (card_remove formula-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (del_vert const-decl "graph[T]" graph_ops nil))
   nil))
(del_vert_le 0
  (del_vert_le-1 nil 3251040627
   ("" (skosimp*)
    (("" (expand "size")
      (("" (expand "del_vert")
        (("" (rewrite "card_remove")
          (("" (lift-if) (("" (ground) nil))))))))))
    nil)
   ((size const-decl "nat" graphs nil)
    (card_remove formula-decl nil finite_sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dbl const-decl "set[T]" doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (pregraph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (graph type-eq-decl nil graphs nil)
    (T formal-type-decl nil graph_ops nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (del_vert const-decl "graph[T]" graph_ops nil))
   nil))
(del_vert_ge 0
  (del_vert_ge-1 nil 3251040627
   ("" (skosimp*)
    (("" (expand "size")
      (("" (expand "del_vert")
        (("" (rewrite "card_remove")
          (("" (lift-if) (("" (ground) nil))))))))))
    nil)
   ((size const-decl "nat" graphs nil)
    (card_remove formula-decl nil finite_sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dbl const-decl "set[T]" doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (pregraph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (graph type-eq-decl nil graphs nil)
    (T formal-type-decl nil graph_ops nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (del_vert const-decl "graph[T]" graph_ops nil))
   nil))
(edge_in_del_vert 0
  (edge_in_del_vert-1 nil 3251040627
   ("" (skosimp*) (("" (expand "del_vert") (("" (assert) nil)))) nil)
   ((del_vert const-decl "graph[T]" graph_ops nil)) nil))
(edges_del_vert 0
  (edges_del_vert-1 nil 3251040627
   ("" (skosimp*)
    (("" (expand "del_vert") (("" (flatten) (("" (propax) nil))))))
    nil)
   ((del_vert const-decl "graph[T]" graph_ops nil)) nil))
(del_vert_comm 0
  (del_vert_comm-1 nil 3251040627
   ("" (skosimp*)
    (("" (apply-extensionality 1 :hide? t)
      (("1" (expand "del_vert")
        (("1" (apply-extensionality 1 :hide? t)
          (("1" (iff 1) (("1" (ground) nil)))))))
       ("2" (expand "del_vert")
        (("2" (apply-extensionality 1 :hide? t)
          (("2" (grind) nil))))))))
    nil)
   ((T formal-type-decl nil graph_ops nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dbl const-decl "set[T]" doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (pregraph type-eq-decl nil graphs nil)
    (del_vert const-decl "graph[T]" graph_ops nil)
    (graph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (remove const-decl "set" sets nil)
    (finite_remove application-judgement "finite_set" finite_sets nil)
    (member const-decl "bool" sets nil))
   nil))
(del_vert_empty? 0
  (del_vert_empty?-1 nil 3251040627
   ("" (skosimp*)
    (("" (lemma "card_empty?[T]")
      (("" (inst?)
        (("" (replace -1 * rl)
          (("" (hide -1)
            (("" (expand "singleton?")
              (("" (expand "size")
                (("" (lemma "size_del_vert")
                  (("" (inst?)
                    (("" (expand "size")
                      (("" (assert) nil))))))))))))))))))))
    nil)
   ((T formal-type-decl nil graph_ops nil)
    (card_empty? formula-decl nil finite_sets nil)
    (singleton? const-decl "bool" graphs nil)
    (size_del_vert formula-decl nil graph_ops nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (size const-decl "nat" graphs nil)
    (del_vert const-decl "graph[T]" graph_ops nil)
    (graph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (pregraph type-eq-decl nil graphs 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)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   nil))
(del_edge_lem 0
  (del_edge_lem-1 nil 3251040627
   ("" (skosimp*)
    (("" (expand "member")
      (("" (expand "del_edge")
        (("" (expand "remove") (("" (propax) nil))))))))
    nil)
   ((member const-decl "bool" sets nil)
    (remove const-decl "set" sets nil)
    (del_edge const-decl "graph[T]" graph_ops nil))
   nil))
(del_edge_lem2 0
  (del_edge_lem2-1 nil 3251040627
   ("" (skosimp*) (("" (grind) nil)) nil)
   ((finite_remove application-judgement "finite_set" finite_sets nil)
    (remove const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (/= const-decl "boolean" notequal nil)
    (del_edge const-decl "graph[T]" graph_ops nil))
   nil))
(del_edge_lem3 0
  (del_edge_lem3-1 nil 3251040627
   ("" (skosimp*) (("" (grind) nil)) nil)
   ((finite_remove application-judgement "finite_set" finite_sets nil)
    (remove const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (del_edge const-decl "graph[T]" graph_ops nil))
   nil))
(del_edge_lem5 0
  (del_edge_lem5-1 nil 3251040627
   ("" (skosimp*)
    (("" (apply-extensionality 2 :hide? t)
      (("1" (apply-extensionality 1 :hide? t)
        (("1" (expand "del_edge") (("1" (grind) nil)))))
       ("2" (expand "del_edge") (("2" (propax) nil))))))
    nil)
   ((T formal-type-decl nil graph_ops nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dbl const-decl "set[T]" doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (pregraph type-eq-decl nil graphs nil)
    (del_edge const-decl "graph[T]" graph_ops nil)
    (graph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (finite_remove application-judgement "finite_set" finite_sets nil)
    (member const-decl "bool" sets nil)
    (remove const-decl "set" sets nil))
   nil))
(vert_del_edge 0
  (vert_del_edge-1 nil 3251040627 ("" (grind) nil nil)
   ((del_edge const-decl "graph[T]" graph_ops nil)) nil))
(del_edge_num 0
  (del_edge_num-1 nil 3251040627
   ("" (skosimp*)
    (("" (expand "num_edges")
      ((""
        (case-replace
         "edges(del_edge(G!1,e!1)) = remove(e!1,edges(G!1))")
        (("1" (rewrite "card_remove[doubleton[T]]") nil)
         ("2" (hide 2)
          (("2" (apply-extensionality :hide? t)
            (("2" (iff 1)
              (("2" (prop)
                (("1" (lemma "del_edge_lem2")
                  (("1" (inst?)
                    (("1" (lemma "del_edge_lem")
                      (("1" (inst?)
                        (("1" (expand "member")
                          (("1" (assert)
                            (("1" (grind :exclude ("edges" "del_edge"))
                              nil)))))))))))))
                 ("2" (rewrite "del_edge_lem3")
                  (("1" (hide 2) (("1" (grind :exclude "edges") nil)))
                   ("2" (hide 2)
                    (("2" (grind :exclude "edges")
                      nil))))))))))))))))))
    nil)
   ((num_edges const-decl "nat" graph_ops nil)
    (del_edge_lem3 formula-decl nil graph_ops nil)
    (del_edge_lem2 formula-decl nil graph_ops nil)
    (del_edge_lem formula-decl nil graph_ops nil)
    (member const-decl "bool" sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (card_remove formula-decl nil finite_sets nil)
    (remove const-decl "set" sets nil)
    (del_edge const-decl "graph[T]" graph_ops 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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil graph_ops nil)
    (finite_remove application-judgement "finite_set" finite_sets nil))
   nil))
(del_edge_singleton 0
  (del_edge_singleton-1 nil 3251040627
   ("" (skosimp*)
    (("" (expand "singleton?")
      (("" (expand "size")
        (("" (expand "del_edge") (("" (propax) nil))))))))
    nil)
   ((singleton? const-decl "bool" graphs nil)
    (del_edge const-decl "graph[T]" graph_ops nil)
    (size const-decl "nat" graphs nil))
   nil))
(del_vert_edge_comm 0
  (del_vert_edge_comm-1 nil 3251040627
   ("" (skosimp*)
    (("" (apply-extensionality 1 :hide? t)
      (("1" (apply-extensionality :hide? t) (("1" (grind) nil)))
       ("2" (expand "del_edge")
        (("2" (expand "del_vert") (("2" (propax) nil))))))))
    nil)
   ((T formal-type-decl nil graph_ops nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dbl const-decl "set[T]" doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (pregraph type-eq-decl nil graphs nil)
    (del_edge const-decl "graph[T]" graph_ops nil)
    (del_vert const-decl "graph[T]" graph_ops nil)
    (graph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (finite_remove application-judgement "finite_set" finite_sets nil)
    (member const-decl "bool" sets nil)
    (remove const-decl "set" sets nil))
   nil))
(del_vert_edge 0
  (del_vert_edge-1 nil 3251040627
   ("" (skosimp*)
    (("" (rewrite "del_vert_edge_comm")
      (("" (apply-extensionality 1 :hide? t)
        (("1" (apply-extensionality 1 :hide? t) (("1" (grind) nil)))
         ("2" (expand "del_edge") (("2" (propax) nil))))))))
    nil)
   ((del_vert_edge_comm formula-decl nil graph_ops nil)
    (T formal-type-decl nil graph_ops nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dbl const-decl "set[T]" doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (pregraph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (graph type-eq-decl nil graphs nil)
    (finite_remove application-judgement "finite_set" finite_sets nil)
    (member const-decl "bool" sets nil)
    (remove const-decl "set" sets nil)
    (del_edge const-decl "graph[T]" graph_ops nil)
    (del_vert const-decl "graph[T]" graph_ops nil))
   nil)))

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