products/sources/formale sprachen/PVS/graphs/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: jfc.xsd   Sprache: Lisp

Original von: PVS©
(graph_deg
 (incident_edges_TCC1 0
  (incident_edges_TCC1-1 nil 3507100590
   ("" (skosimp*)
    (("" (lemma "finite_subset[doubleton[T]]")
      (("" (inst?)
        (("" (inst -1 "edges(G!1)")
          (("" (assert) (("" (hide 2) (("" (grind) 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_deg nil)
    (finite_subset formula-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (NOT const-decl "[bool -> bool]" booleans 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)
    (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))
 (incident_edges_subset 0
  (incident_edges_subset-1 nil 3507100590 ("" (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_deg 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)
    (incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
     nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil))
   nil))
 (incident_edges_emptyset 0
  (incident_edges_emptyset-1 nil 3507100590
   ("" (skosimp*)
    (("" (apply-extensionality 1 :hide? t)
      (("" (expand "emptyset")
        (("" (expand "incident_edges") (("" (ground) nil))))))))
    nil)
   ((T formal-type-decl nil graph_deg 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)
    (emptyset const-decl "set" sets nil)
    (incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
     nil)
    (is_finite const-decl "bool" finite_sets 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)
    (finite_emptyset name-judgement "finite_set" finite_sets nil))
   nil))
 (deg_del_edge 0
  (deg_del_edge-1 nil 3507100590
   ("" (skosimp*)
    (("" (expand "deg")
      ((""
        (case-replace "incident_edges(y!1, del_edge(G!1,e!1)) =
                     remove(e!1,incident_edges(y!1, G!1))")
        (("1" (rewrite "card_remove[doubleton[T]]")
          (("1" (lift-if)
            (("1" (ground)
              (("1" (hide -1 2)
                (("1" (hide -2) (("1" (grind) nil)))))))))))
         ("2" (hide 2)
          (("2" (apply-extensionality 1 :hide? t)
            (("2" (iff 1)
              (("2" (prop)
                (("1" (expand "incident_edges")
                  (("1" (ground)
                    (("1" (expand "remove")
                      (("1" (expand "member")
                        (("1" (ground)
                          (("1" (replace -1)
                            (("1" (hide -1)
                              (("1"
                                (lemma "del_edge_lem[T]")
                                (("1"
                                  (inst?)
                                  (("1"
                                    (expand "member")
                                    (("1" (propax) nil)))))))))))
                           ("2" (lemma "del_edge_lem2[T]")
                            (("2" (inst?)
                              (("2" (assert) nil)))))))))))))))
                 ("2" (expand "incident_edges")
                  (("2" (expand "remove")
                    (("2" (flatten)
                      (("2" (expand "member")
                        (("2" (ground)
                          (("2" (rewrite "del_edge_lem3")
                            nil))))))))))))))))))))))))
    nil)
   ((deg const-decl "nat" graph_deg nil)
    (del_edge_lem3 formula-decl nil graph_ops nil)
    (del_edge_lem formula-decl nil graph_ops nil)
    (del_edge_lem2 formula-decl nil graph_ops nil)
    (member const-decl "bool" sets nil)
    (card_remove formula-decl nil finite_sets nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (int_plus_int_is_int application-judgement "int" integers nil)
    (nil application-judgement "finite_set[T]" graph_deg nil)
    (remove const-decl "set" sets nil)
    (del_edge const-decl "graph[T]" graph_ops nil)
    (incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
     nil)
    (is_finite const-decl "bool" finite_sets 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_deg nil)
    (finite_remove application-judgement "finite_set" finite_sets nil))
   nil))
 (deg_del_edge2 0
  (deg_del_edge2-1 nil 3507100590
   ("" (skosimp*)
    (("" (lemma "deg_del_edge")
      (("" (inst?)
        (("" (typepred "e!1")
          (("" (skosimp*)
            (("" (case "x!1=y!1")
              (("1" (replace -1)
                (("1" (hide -1)
                  (("1" (inst -2 "y!2")
                    (("1" (split -2)
                      (("1" (propax) nil)
                       ("2" (replace -1)
                        (("2" (hide -1)
                          (("2" (hide -1 -2 3)
                            (("2" (expand "dbl")
                              (("2"
                                (apply-extensionality :hide? t)
                                (("2"
                                  (iff 1)
                                  (("2" (ground) nil)))))))))))))
                       ("3" (propax) nil)))))))))
               ("2" (case "y!2 = y!1")
                (("1" (replace -1)
                  (("1" (hide -1)
                    (("1" (inst -2 "x!1") (("1" (assert) nil)))))))
                 ("2" (hide -2 -4 4)
                  (("2" (replace -1)
                    (("2" (hide -1)
                      (("2" (expand "dbl")
                        (("2" (ground) nil))))))))))))))))))))))
    nil)
   ((deg_del_edge formula-decl nil graph_deg nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (OR const-decl "[bool, bool -> bool]" booleans nil)
    (nil application-judgement "finite_set[T]" graph_deg nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers 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_deg nil))
   nil))
 (deg_del_edge3 0
  (deg_del_edge3-1 nil 3507100590
   ("" (skosimp*)
    (("" (expand "deg")
      ((""
        (case "incident_edges(y!1, G!1) = incident_edges(y!1, del_edge(G!1, e!1))")
        (("1" (assert) nil)
         ("2" (hide 3)
          (("2" (apply-extensionality 1 :hide? t)
            (("2" (expand "incident_edges")
              (("2" (iff 1)
                (("2" (ground)
                  (("1" (lemma "del_edge_lem3[T]")
                    (("1" (inst?) (("1" (assert) nil)))))
                   ("2" (lemma "del_edge_lem2[T]")
                    (("2" (inst?)
                      (("2" (assert) nil))))))))))))))))))))
    nil)
   ((deg const-decl "nat" graph_deg nil)
    (del_edge_lem3 formula-decl nil graph_ops nil)
    (del_edge_lem2 formula-decl nil graph_ops nil)
    (T formal-type-decl nil graph_deg 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)
    (is_finite const-decl "bool" finite_sets nil)
    (incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
     nil)
    (del_edge const-decl "graph[T]" graph_ops nil))
   nil))
 (deg_del_edge_ge 0
  (deg_del_edge_ge-1 nil 3507100590
   ("" (skosimp*)
    (("" (case "e!1(y!1)")
      (("1" (lemma "deg_del_edge2")
        (("1" (inst?)
          (("1" (assert)
            (("1" (lemma "del_edge_lem5[T]")
              (("1" (inst?) (("1" (assert) nil)))))))))))
       ("2" (lemma "deg_del_edge3")
        (("2" (inst?) (("2" (assert) 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_deg nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (int_minus_int_is_int application-judgement "int" integers 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)
    (del_edge_lem5 formula-decl nil graph_ops nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (deg_del_edge2 formula-decl nil graph_deg nil)
    (deg_del_edge3 formula-decl nil graph_deg nil))
   nil))
 (deg_del_edge_le 0
  (deg_del_edge_le-1 nil 3507100590
   ("" (skosimp*)
    (("" (case "e!1(y!1)")
      (("1" (lemma "deg_del_edge2")
        (("1" (inst?)
          (("1" (assert)
            (("1" (lemma "del_edge_lem5[T]")
              (("1" (inst?) (("1" (assert) nil)))))))))))
       ("2" (lemma "deg_del_edge3")
        (("2" (inst?) (("2" (assert) 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_deg nil)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (int_minus_int_is_int application-judgement "int" integers 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)
    (del_edge_lem5 formula-decl nil graph_ops nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (deg_del_edge2 formula-decl nil graph_deg nil)
    (deg_del_edge3 formula-decl nil graph_deg nil))
   nil))
 (deg_edge_exists 0
  (deg_edge_exists-1 nil 3507100590
   ("" (skosimp*)
    (("" (expand "deg")
      (("" (rewrite "nonempty_card[doubleton[T]]" :dir rl)
        (("" (expand "nonempty?")
          (("" (expand "empty?")
            (("" (expand "incident_edges")
              (("" (skosimp*)
                (("" (expand "member")
                  (("" (inst?)
                    (("" (flatten)
                      (("" (assert) nil))))))))))))))))))))
    nil)
   ((deg const-decl "nat" graph_deg nil)
    (nonempty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" 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_deg nil)
    (incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
     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)
    (is_finite const-decl "bool" finite_sets nil)
    (nonempty_card formula-decl nil finite_sets nil))
   nil))
 (deg_to_card 0
  (deg_to_card-1 nil 3507100590
   ("" (skosimp*)
    (("" (lemma "deg_edge_exists")
      (("" (inst?)
        (("" (assert)
          (("" (skosimp*)
            (("" (hide -1 -3)
              (("" (typepred "G!1")
                (("" (inst?)
                  (("" (assert)
                    (("" (typepred "e!1")
                      (("" (skosimp*)
                        (("" (inst-cp -2 "x!1")
                          (("" (inst -2 "y!1")
                            (("" (replace -1)
                              ((""
                                (hide -1)
                                ((""
                                  (hide -3)
                                  ((""
                                    (expand "dbl")
                                    ((""
                                      (expand "size")
                                      ((""
                                        (case
                                         "subset?(add[T](x!1,singleton(y!1)),vert(G!1))")
                                        (("1"
                                          (lemma "card_subset[T]")
                                          (("1"
                                            (inst?)
                                            (("1"
                                              (assert)
                                              (("1"
                                                (hide -2)
                                                (("1"
                                                  (lemma "card_add[T]")
                                                  (("1"
                                                    (inst?)
                                                    (("1"
                                                      (lemma
                                                       "card_singleton[T]")
                                                      (("1"
                                                        (inst?)
                                                        (("1"
                                                          (replace -1)
                                                          (("1"
                                                            (hide -1)
                                                            (("1"
                                                              (expand
                                                               "singleton")
                                                              (("1"
                                                                (replace
                                                                 -1)
                                                                (("1"
                                                                  (hide
                                                                   -1)
                                                                  (("1"
                                                                    (assert)
                                                                    nil)))))))))))))))))))))))
                                             ("2"
                                              (rewrite "finite_add[T]")
                                              nil)))))
                                         ("2"
                                          (hide 3)
                                          (("2"
                                            (grind)
                                            nil))))))))))))))))))))))))))))))))))))))))
    nil)
   ((deg_edge_exists formula-decl nil graph_deg 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)
    (size const-decl "nat" graphs nil)
    (member const-decl "bool" sets nil)
    (card_subset formula-decl nil finite_sets nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (card_add formula-decl nil finite_sets nil)
    (card_singleton formula-decl nil finite_sets nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (is_finite const-decl "bool" finite_sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (singleton? const-decl "bool" sets nil)
    (add const-decl "(nonempty?)" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (nonempty_add_finite application-judgement "non_empty_finite_set"
     finite_sets 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)
    (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_deg nil))
   nil))
 (del_vert_deg_0 0
  (del_vert_deg_0-1 nil 3507100590
   ("" (skosimp*)
    (("" (expand "deg")
      (("" (lemma "card_empty?[doubleton[T]]")
        (("" (inst?)
          (("" (iff)
            (("" (assert)
              (("" (hide -2)
                (("" (expand "incident_edges")
                  (("" (expand "empty?")
                    (("" (expand "member")
                      (("" (apply-extensionality 1 :hide? t)
                        (("" (expand "del_vert")
                          (("" (inst?)
                            (("" (iff 1)
                              ((""
                                (ground)
                                nil))))))))))))))))))))))))))))
    nil)
   ((deg const-decl "nat" graph_deg nil)
    (is_finite const-decl "bool" finite_sets 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)
    (incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
     nil)
    (member const-decl "bool" sets nil)
    (del_vert const-decl "graph[T]" graph_ops nil)
    (empty? const-decl "bool" sets nil)
    (card_empty? formula-decl nil finite_sets nil)
    (T formal-type-decl nil graph_deg 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))
   nil))
 (deg_del_vert_TCC1 0
  (deg_del_vert_TCC1-1 nil 3507100590 ("" (subtype-tcc) nil nil)
   ((T formal-type-decl nil graph_deg nil)
    (/= const-decl "boolean" notequal nil))
   nil))
 (deg_del_vert 0
  (deg_del_vert-1 nil 3507100590
   ("" (skosimp*)
    (("" (expand "deg")
      ((""
        (case-replace "incident_edges(v!1, del_vert(G!1, x!1)) =
             incident_edges(v!1, del_edge(G!1,dbl[T](x!1,v!1)))")
        (("1" (hide -1)
          (("1" (lemma "deg_del_edge")
            (("1" (inst?)
              (("1" (inst -1 "x!1" "v!1")
                (("1" (prop)
                  (("1" (expand "deg") (("1" (assert) nil)))))))
               ("2" (inst?) (("2" (assert) nil)))))))))
         ("2" (hide 3)
          (("2" (apply-extensionality 1 :hide? t)
            (("1" (expand "incident_edges")
              (("1" (grind)
                (("1" (hide -3)
                  (("1" (replace -2 * rl) (("1" (grind) nil)))))
                 ("2" (hide -1 -4)
                  (("2" (lemma "edge_has_2_verts[T]")
                    (("2" (inst?)
                      (("2" (inst?) (("2" (assert) nil)))))))))))))
             ("2" (inst?) (("2" (assert) nil)))))))
         ("3" (inst?) (("3" (assert) nil))))))))
    nil)
   ((deg const-decl "nat" graph_deg nil)
    (edge_has_2_verts formula-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)
    (odd_minus_odd_is_even application-judgement "even_int" integers
     nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (deg_del_edge formula-decl nil graph_deg nil)
    (del_edge const-decl "graph[T]" graph_ops nil)
    (del_vert const-decl "graph[T]" graph_ops nil)
    (incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
     nil)
    (is_finite const-decl "bool" finite_sets 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_deg nil)
    (nil application-judgement "finite_set[T]" graph_deg nil))
   nil))
 (del_vert_not_incident 0
  (del_vert_not_incident-1 nil 3507100590
   ("" (skosimp*)
    (("" (expand "deg")
      ((""
        (case-replace
         "incident_edges(x!1, G!1) = incident_edges(x!1, del_vert(G!1, v!1))")
        (("" (hide 4)
          (("" (apply-extensionality 1 :hide? t)
            (("" (expand "incident_edges")
              (("" (iff 1)
                (("" (prop)
                  (("1" (lemma "edge_in_del_vert")
                    (("1" (inst?)
                      (("1" (assert)
                        (("1" (lemma "edge_has_2_verts")
                          (("1" (inst?)
                            (("1" (inst?)
                              (("1" (assert) nil)))))))))))))
                   ("2" (expand "del_vert")
                    (("2" (flatten)
                      (("2" (propax) nil))))))))))))))))))))
    nil)
   ((deg const-decl "nat" graph_deg nil)
    (edge_has_2_verts formula-decl nil graphs nil)
    (edge_in_del_vert formula-decl nil graph_ops nil)
    (nil application-judgement "finite_set[T]" graph_deg nil)
    (del_vert const-decl "graph[T]" graph_ops nil)
    (incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
     nil)
    (is_finite const-decl "bool" finite_sets 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_deg nil))
   nil))
 (singleton_deg 0
  (singleton_deg-1 nil 3507100590
   ("" (skosimp*)
    (("" (expand "singleton?")
      (("" (expand "deg")
        (("" (rewrite "card_is_0[doubleton[T]]")
          (("" (apply-extensionality 1 :hide? t)
            (("" (expand "incident_edges")
              (("" (expand "emptyset")
                (("" (flatten)
                  (("" (lemma "edge_in_card_gt_1[T]")
                    (("" (inst?)
                      (("" (split -1)
                        (("1" (assert)
                          (("1" (expand "size") (("1" (assert) nil)))))
                         ("2" (propax) nil))))))))))))))))))))))
    nil)
   ((singleton? const-decl "bool" graphs nil)
    (card_is_0 formula-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets 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)
    (incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
     nil)
    (T formal-type-decl nil graph_deg 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_emptyset name-judgement "finite_set" finite_sets nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (size const-decl "nat" graphs nil)
    (edge_in_card_gt_1 formula-decl nil graphs nil)
    (emptyset const-decl "set" sets nil)
    (deg const-decl "nat" graph_deg nil))
   nil))
 (deg_1_sing 0
  (deg_1_sing-1 nil 3507100590
   ("" (skosimp*)
    (("" (expand "deg")
      (("" (lemma "card_one[Dbl]")
        (("" (inst?)
          (("" (flatten)
            (("" (assert)
              (("" (hide -2)
                (("" (skosimp*)
                  (("" (inst?)
                    (("" (assert)
                      ((""
                        (case-replace
                         "incident_edges(v!1, G!1)(x!1) = singleton(x!1)(x!1)")
                        (("1" (hide -2)
                          (("1" (expand "incident_edges")
                            (("1" (expand "singleton")
                              (("1"
                                (flatten)
                                (("1" (assert) nil)))))))))
                         ("2" (assert) nil))))))))))))))))))))))
    nil)
   ((deg const-decl "nat" graph_deg nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets 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)
    (incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
     nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (card_one formula-decl nil finite_sets nil)
    (T formal-type-decl nil graph_deg 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)
    (Dbl type-eq-decl nil doubletons nil))
   nil)))


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