Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: graph_from_edges.prf Sprache: Lisp

Original von: PVS^©

(graph_from_edges
(finite_lem 0
  (finite_lem-1 nil 3375355954
   ("" (skosimp)
    (("" (lemma "Union_finite[T]")
      (("" (inst -1 "ES!1")
        (("" (typepred "ES!1")
          (("" (prop)
            (("1" (grind) nil nil)
             ("2" (lemma "finite_dbl[T]")
              (("2" (expand "every")
                (("2" (hide (2 3))
                  (("2" (hide -2)
                    (("2" (skosimp)
                      (("2" (typepred "x!1")
                        (("2" (expand "extend")
                          (("2" (prop)
                            (("2" (skosimp)
                              (("2"
                                (inst -3 "x!2" "y!1")
                                (("2" (grind) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil graph_from_edges nil)
    (Union_finite formula-decl nil finite_sets_of_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (finite_dbl formula-decl nil doubletons nil)
    (nil application-judgement "finite_set[T]" graphs nil)
    (injective? const-decl "bool" functions nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (>= const-decl "bool" reals 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)
    (number nonempty-type-decl nil numbers nil)
    (< const-decl "bool" reals nil)
    (below type-eq-decl nil nat_types nil)
    (x!1 skolem-const-decl
     "(extend[setof[T], doubleton[T], bool, FALSE](ES!1))"
     graph_from_edges nil)
    (ES!1 skolem-const-decl "finite_set[doubleton[T]]" graph_from_edges
     nil)
    (y!1 skolem-const-decl "T" graph_from_edges nil)
    (x!2 skolem-const-decl "T" graph_from_edges nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (IFF const-decl "[bool, bool -> bool]" booleans nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (every const-decl "bool" sets nil)
    (finite_extend application-judgement "finite_set[T]"
     extend_set_props nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (extend const-decl "R" extend nil)
    (FALSE const-decl "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)
    (setofsets type-eq-decl nil sets nil)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil))
   shostak))
(Union_to_pred 0
  (Union_to_pred-1 nil 3375356366 ("" (grind) 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_from_edges 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)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (finite_extend application-judgement "finite_set[T]"
     extend_set_props nil)
    (injective? const-decl "bool" functions nil)
    (nat nonempty-type-eq-decl nil naturalnumbers 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)
    (>= const-decl "bool" reals 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)
    (number nonempty-type-decl nil numbers nil)
    (extend const-decl "R" extend nil)
    (FALSE const-decl "bool" booleans nil)
    (setof type-eq-decl nil defined_types nil)
    (Union const-decl "set" sets nil))
   shostak))
(pred_to_Union 0
  (pred_to_Union-1 nil 3375356392
   ("" (skosimp)
    (("" (expand "Union")
      (("" (skolem -1 "d!1")
        (("" (flatten)
          (("" (inst 1 "d!1")
            (("" (expand "extend")
              (("" (prop)
                (("" (typepred "d!1") (("" (propax) nil nil)) nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((Union const-decl "set" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (ES!1 skolem-const-decl "finite_set[doubleton[T]]" graph_from_edges
     nil)
    (d!1 skolem-const-decl "doubleton[T]" graph_from_edges nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (extend const-decl "R" extend nil)
    (FALSE const-decl "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)
    (setof type-eq-decl nil defined_types nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil graph_from_edges nil)
    (finite_extend application-judgement "finite_set[T]"
     extend_set_props nil))
   shostak))
(verts_of_TCC1 0
  (verts_of_TCC1-1 nil 3367125257 ("" (use "finite_lem") nil nil)
   ((finite_lem formula-decl nil graph_from_edges nil)) nil))
(verts_from_TCC1 0
  (verts_from_TCC1-1 nil 3375524256
   ("" (skosimp*)
    (("" (expand "restrict")
      (("" (lemma "verts_of_TCC1")
        (("" (inst - "ES!1")
          ((""
            (case-replace
             "{t: T | EXISTS (d: doubleton[T]): d(t) AND ES!1(d)} = (Union[T](extend[setof[T], doubleton[T], bool, FALSE](ES!1)))")
            (("" (hide -1 2)
              (("" (apply-extensionality 1 :hide? t)
                (("" (iff 1)
                  (("" (prop)
                    (("1" (skosimp*)
                      (("1" (expand "Union")
                        (("1" (inst?)
                          (("1" (expand "extend")
                            (("1" (ground) nil nil)) nil))
                          nil))
                        nil))
                      nil)
                     ("2" (expand "Union")
                      (("2" (skosimp*)
                        (("2" (typepred "a!1")
                          (("2" (expand "extend")
                            (("2" (ground)
                              (("2"
                                (skosimp*)
                                (("2"
                                  (inst?)
                                  (("2" (assert) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((verts_of_TCC1 subtype-tcc nil graph_from_edges nil)
    (setof type-eq-decl nil defined_types nil)
    (setofsets type-eq-decl nil sets nil)
    (Union const-decl "set" sets nil)
    (FALSE const-decl "bool" booleans nil)
    (extend const-decl "R" extend nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (finite_extend application-judgement "finite_set[T]"
     extend_set_props nil)
    (d!1 skolem-const-decl "doubleton[T]" graph_from_edges nil)
    (ES!1 skolem-const-decl "finite_set[doubleton[T]]" graph_from_edges
     nil)
    (nil application-judgement "finite_set[T]" graphs nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" 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_from_edges nil))
   nil))
(verts_from_of 0
  (verts_from_of-1 nil 3375527862
   ("" (skosimp*)
    (("" (apply-extensionality 1 :hide? t)
      (("" (expand "verts_of")
        (("" (expand "verts_from")
          (("" (iff 1)
            (("" (prop)
              (("1" (lemma "Union_to_pred")
                (("1" (inst?)
                  (("1" (assert)
                    (("1" (skosimp*)
                      (("1" (inst?) (("1" (assert) nil nil)) nil))
                      nil))
                    nil))
                  nil))
                nil)
               ("2" (lemma "pred_to_Union")
                (("2" (inst?)
                  (("2" (assert)
                    (("2" (hide 2)
                      (("2" (skosimp*)
                        (("2" (inst?) (("2" (assert) nil nil)) nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil graph_from_edges nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (verts_from const-decl "finite_set[T]" graph_from_edges nil)
    (verts_of const-decl "finite_set[T]" graph_from_edges nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (is_finite const-decl "bool" 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)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (finite_extend application-judgement "finite_set[T]"
     extend_set_props nil)
    (Union_to_pred formula-decl nil graph_from_edges nil)
    (pred_to_Union formula-decl nil graph_from_edges nil))
   shostak))
(graph_from_edgeset_TCC1 0
  (graph_from_edgeset_TCC1-1 nil 3367125257
   ("" (skosimp)
    (("" (split)
      (("1" (use "pred_to_Union") (("1" (grind) nil nil)) nil)
       ("2" (grind) nil nil))
      nil))
    nil)
   ((Union const-decl "set" sets nil)
    (verts_of const-decl "finite_set[T]" graph_from_edges nil)
    (nil application-judgement "finite_set[T]" graphs nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (T formal-type-decl nil graph_from_edges 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)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (pred_to_Union formula-decl nil graph_from_edges nil)
    (Union_surjective name-judgement
     "(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
    (finite_extend application-judgement "finite_set[T]"
     extend_set_props nil)
    (member const-decl "bool" sets nil)
    (isolated_vert? const-decl "bool" graph_from_edges nil))
   nil))
(graph_from_edgeset_rew1 0
  (graph_from_edgeset_rew1-1 nil 3375356563 ("" (grind) nil nil)
   ((verts_of const-decl "finite_set[T]" graph_from_edges nil)
    (graph_from_edgeset const-decl "es_graph" graph_from_edges nil))
   shostak))
(graph_from_edgeset_rew2 0
  (graph_from_edgeset_rew2-1 nil 3375356569 ("" (grind) nil nil)
   ((verts_of const-decl "finite_set[T]" graph_from_edges nil)
    (graph_from_edgeset const-decl "es_graph" graph_from_edges nil))
   shostak))
(no_isolated_verts 0
  (no_isolated_verts-1 nil 3375356574 ("" (grind) 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_from_edges 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)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (verts_of const-decl "finite_set[T]" graph_from_edges nil)
    (graph_from_edgeset const-decl "es_graph" graph_from_edges nil)
    (Union const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (isolated_vert? const-decl "bool" graph_from_edges nil))
   shostak)))

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