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: default_bindings_src.ml   Sprache: Lisp

Original von: PVS©
(graph_conn_piece
 (singleton_piece 0
  (singleton_piece-1 nil 3251050559
   ("" (skosimp*)
    (("" (expand "piece_connected?")
      (("" (prop)
        (("1" (rewrite "empty?_rew")
          (("1" (expand "singleton?")
            (("1" (expand "size") (("1" (assert) nil)))))))
         ("2" (skosimp*)
          (("2" (expand "singleton?")
            (("2" (replace -1)
              (("2" (hide -1)
                (("2" (expand "empty?")
                  (("2" (expand "empty?")
                    (("2" (expand "member")
                      (("2" (skosimp*)
                        (("2" (expand "intersection")
                          (("2" (expand "member")
                            (("2" (inst-cp -3 "x!1")
                              (("2"
                                (inst -3 "x!2")
                                (("2"
                                  (ground)
                                  (("2"
                                    (expand "size")
                                    (("2"
                                      (rewrite "card_one[T]")
                                      (("2"
                                        (skosimp*)
                                        (("2"
                                          (case
                                           "vert(union(H1!1, H2!1))(x!1) = singleton(x!3)(x!1)")
                                          (("1"
                                            (case
                                             "vert(union(H1!1, H2!1))(x!2) = singleton(x!3)(x!2)")
                                            (("1"
                                              (hide -5)
                                              (("1" (grind) nil)))
                                             ("2" (assert) nil)))
                                           ("2"
                                            (assert)
                                            nil))))))))))))))))))))))))))))))))))))))))
    nil)
   ((finite_intersection1 application-judgement "finite_set"
     finite_sets nil)
    (piece_connected? const-decl "bool" graph_conn_defs nil)
    (empty? const-decl "bool" sets nil)
    (empty? const-decl "bool" graphs nil)
    (member const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil)
    (card_one formula-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (union const-decl "graph[T]" graph_ops nil)
    (singleton? const-decl "bool" sets nil)
    (singleton const-decl "(singleton?)" sets nil)
    (union const-decl "set" sets nil)
    (nonempty_singleton_finite application-judgement
     "non_empty_finite_set" finite_sets nil)
    (finite_union application-judgement "finite_set" finite_sets nil)
    (empty?_rew formula-decl nil graphs 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)
    (T formal-type-decl nil graph_conn_piece nil)
    (size const-decl "nat" graphs nil)
    (singleton? const-decl "bool" graphs nil))
   nil))
 (not_piece_has_2 0
  (not_piece_has_2-2 nil 3251107139
   ("" (skosimp*)
    (("" (expand "piece_connected?")
      (("" (prop)
        (("" (skosimp*)
          (("" (rewrite "empty?_rew")
            (("" (rewrite "empty?_rew")
              (("" (rewrite "empty?_rew")
                (("" (expand "empty?")
                  (("" (expand "size")
                    ((""
                      (case "card(vert(G!1)) >= card(vert(H1!1)) + card(vert(H2!1))")
                      (("1" (assert) nil nil)
                       ("2" (hide 2 3 4)
                        (("2" (replace -1)
                          (("2" (hide -1)
                            (("2" (expand "union")
                              (("2"
                                (rewrite "card_union[T]")
                                (("2"
                                  (case
                                   "card(intersection(vert(H1!1), vert(H2!1))) = 0")
                                  (("1" (assert) nil nil)
                                   ("2"
                                    (hide 2)
                                    (("2"
                                      (rewrite "card_empty?[T]")
                                      (("2"
                                        (expand "empty?")
                                        (("2" (propax) nil nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((finite_intersection1 application-judgement "finite_set"
     finite_sets nil)
    (piece_connected? const-decl "bool" graph_conn_defs nil)
    (empty? const-decl "bool" sets nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
    (Card const-decl "nat" finite_sets 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)
    (is_finite const-decl "bool" finite_sets 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)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers 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)
    (union const-decl "graph[T]" graph_ops nil)
    (intersection const-decl "set" sets nil)
    (card_empty? formula-decl nil finite_sets nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (card_union formula-decl nil finite_sets nil)
    (size const-decl "nat" graphs nil)
    (T formal-type-decl nil graph_conn_piece 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)
    (empty?_rew formula-decl nil graphs nil))
   nil)
  (not_piece_has_2-1 nil 3251050559
   ("" (skosimp*)
    (("" (expand "piece_connected?")
      (("" (prop)
        (("" (skosimp*)
          (("" (rewrite "empty?_rew")
            (("" (rewrite "empty?_rew")
              (("" (rewrite "empty?_rew")
                (("" (expand "empty?")
                  (("" (expand "size")
                    ((""
                      (case "card(vert(G!1)) >= card(vert(H1!1)) + card(vert(H2!1))")
                      (("1" (assert) nil nil)
                       ("2" (hide 2 3 4)
                        (("2" (replace -1)
                          (("2" (hide -1)
                            (("2" (expand "union")
                              (("2"
                                (rewrite "card_union[T]")
                                (("2"
                                  (case
                                   "card(intersection(vert(H1!1), vert(H2!1))) = 0")
                                  (("1" (assert) nil nil)
                                   ("2"
                                    (hide 2)
                                    (("2"
                                      (rewrite "card_empty?[T]")
                                      (("2"
                                        (expand "empty?")
                                        (("2" (propax) nil nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("3"
                                    (rewrite "finite_intersection")
                                    nil
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((piece_connected? const-decl "bool" graph_conn_defs nil)
    (union const-decl "graph[T]" graph_ops nil)
    (size const-decl "nat" graphs nil)
    (graph type-eq-decl nil graphs nil)
    (pregraph type-eq-decl nil graphs nil)
    (doubleton type-eq-decl nil doubletons nil)
    (dbl const-decl "set[T]" doubletons nil)
    (empty?_rew formula-decl nil graphs nil))
   nil))
 (edge_not_across 0
  (edge_not_across-1 nil 3251050559
   ("" (skosimp*)
    (("" (expand "union")
      (("" (expand "union")
        (("" (expand "member")
          (("" (assert)
            (("" (typepred "H2!1")
              (("" (inst?)
                (("" (assert)
                  (("" (inst -1 "vo!1")
                    (("" (assert)
                      (("" (hide -2 -4 1)
                        (("" (grind) nil))))))))))))))))))))))
    nil)
   ((union const-decl "graph[T]" graph_ops nil)
    (member const-decl "bool" 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_conn_piece nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (intersection const-decl "set" sets nil)
    (empty? const-decl "bool" sets nil)
    (finite_intersection1 application-judgement "finite_set"
     finite_sets nil)
    (union const-decl "set" sets nil))
   nil))
 (lem1 0
  (lem1-1 nil 3251050559
   ("" (skosimp*)
    (("" (case "NOT vert(H2!1)(vo!1)")
      (("1" (hide -2)
        (("1" (apply-extensionality 4 :hide? t)
          (("1" (hide 3 4)
            (("1" (apply-extensionality 1 :hide? t)
              (("1" (grind)
                (("1" (hide -3)
                  (("1" (typepred "H2!1")
                    (("1" (inst?)
                      (("1" (assert)
                        (("1" (inst?)
                          (("1" (assert) nil)))))))))))))))))
           ("2" (hide 3 4)
            (("2" (apply-extensionality 1 :hide? t)
              (("2" (grind) nil)))))))))
       ("2" (hide 1 2 3) (("2" (grind) 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_conn_piece nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (union const-decl "graph[T]" graph_ops nil)
    (del_vert const-decl "graph[T]" graph_ops nil)
    (finite_remove application-judgement "finite_set" finite_sets nil)
    (finite_union application-judgement "finite_set" finite_sets nil)
    (member const-decl "bool" sets nil)
    (union const-decl "set" sets nil)
    (remove const-decl "set" sets nil)
    (finite_intersection1 application-judgement "finite_set"
     finite_sets nil)
    (intersection const-decl "set" sets nil)
    (empty? const-decl "bool" sets nil))
   nil))
 (H1P_not_empty 0
  (H1P_not_empty-1 nil 3251050559
   ("" (skosimp*)
    (("" (hide -3 3)
      (("" (lemma "deg_edge_exists")
        (("" (inst?)
          (("" (assert)
            (("" (skosimp*)
              (("" (case "edges(H1!1)(e!1)")
                (("1" (hide -3)
                  (("1" (typepred "H1!1")
                    (("1" (inst?)
                      (("1" (assert)
                        (("1" (typepred "e!1")
                          (("1" (skosimp*)
                            (("1" (hide -3 -4 -6)
                              (("1"
                                (replace -1)
                                (("1"
                                  (hide -1)
                                  (("1"
                                    (inst-cp -1 "x!1")
                                    (("1"
                                      (inst -1 "y!1")
                                      (("1"
                                        (expand "dbl")
                                        (("1"
                                          (case "vo!1 = x!1")
                                          (("1"
                                            (replace -1 * rl)
                                            (("1"
                                              (hide -1)
                                              (("1"
                                                (hide -4 2 3)
                                                (("1"
                                                  (expand "empty?")
                                                  (("1"
                                                    (expand "empty?")
                                                    (("1"
                                                      (expand "member")
                                                      (("1"
                                                        (inst -4 "y!1")
                                                        (("1"
                                                          (grind)
                                                          nil)))))))))))))))
                                           ("2"
                                            (hide -4 3 4)
                                            (("2"
                                              (expand "empty?")
                                              (("2"
                                                (expand "empty?")
                                                (("2"
                                                  (inst -4 "x!1")
                                                  (("2"
                                                    (expand "member")
                                                    (("2"
                                                      (grind)
                                                      nil)))))))))))))))))))))))))))))))))))))
                 ("2" (hide -4 -6 2 3)
                  (("2" (lemma "edge_not_across")
                    (("2" (inst?)
                      (("2" (inst?)
                        (("2" (assert) nil))))))))))))))))))))))
    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)
    (union const-decl "graph[T]" graph_ops nil)
    (edge_not_across formula-decl nil graph_conn_piece nil)
    (empty? const-decl "bool" graphs nil)
    (member const-decl "bool" sets nil)
    (finite_remove application-judgement "finite_set" finite_sets nil)
    (remove const-decl "set" sets nil)
    (del_vert const-decl "graph[T]" graph_ops nil)
    (empty? const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (finite_intersection1 application-judgement "finite_set"
     finite_sets nil)
    (deg_edge_exists formula-decl nil graph_deg nil)
    (T formal-type-decl nil graph_conn_piece nil))
   nil))
 (cip0 0
  (cip0-1 nil 3251050559
   ("" (skosimp*)
    (("" (name "GP" "del_vert(G!1,vo!1)")
      (("" (name "H1P" "del_vert(H1!1, vo!1)")
        (("" (case "GP = union(H1P,H2!1)")
          (("1" (case "NOT piece_connected?(GP)")
            (("1" (inst?)
              (("1" (assert)
                (("1" (hide -1 -2 -5 -6 -8 -9 1 3 4)
                  (("1" (replace -1 * rl)
                    (("1" (hide -1)
                      (("1" (expand "size")
                        (("1" (expand "del_vert")
                          (("1" (rewrite "card_remove")
                            (("1" (lift-if)
                              (("1"
                                (ground)
                                (("1"
                                  (hide 2)
                                  (("1"
                                    (replace -2)
                                    (("1"
                                      (hide -2)
                                      (("1"
                                        (grind)
                                        nil)))))))))))))))))))))))))))
             ("2" (hide -5 -6 -7 -8)
              (("2" (expand "piece_connected?")
                (("2" (flatten)
                  (("2" (inst -1 "H1P" "H2!1")
                    (("2" (assert)
                      (("2" (split -1)
                        (("1" (hide -3 -4 2)
                          (("1" (hide -1)
                            (("1" (replace -1 * rl)
                              (("1"
                                (hide -1)
                                (("1"
                                  (hide -1 2 3)
                                  (("1"
                                    (expand "empty?")
                                    (("1"
                                      (skosimp*)
                                      (("1"
                                        (inst?)
                                        (("1"
                                          (grind)
                                          nil)))))))))))))))))
                         ("2" (reveal -3 -4)
                          (("2" (lemma "H1P_not_empty")
                            (("2" (inst?)
                              (("2"
                                (inst -1 "G!1" "H2!1")
                                (("2"
                                  (assert)
                                  nil)))))))))))))))))))))))
           ("2" (hide -5 -6 -8)
            (("2" (lemma "lem1")
              (("2" (inst -1 "H1!1" "H2!1" "vo!1")
                (("2" (assert) nil))))))))))))))
    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)
    (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_conn_piece nil)
    (union const-decl "graph[T]" graph_ops nil)
    (H1P_not_empty formula-decl nil graph_conn_piece nil)
    (finite_remove application-judgement "finite_set" finite_sets nil)
    (remove const-decl "set" sets nil)
    (intersection const-decl "set" sets nil)
    (empty? const-decl "bool" sets nil)
    (finite_union application-judgement "finite_set" finite_sets nil)
    (union const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (card_remove formula-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (size const-decl "nat" graphs nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (finite_intersection1 application-judgement "finite_set"
     finite_sets nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (piece_connected? const-decl "bool" graph_conn_defs nil)
    (lem1 formula-decl nil graph_conn_piece nil))
   nil))
 (cip3 0
  (cip3-1 nil 3251050559
   ("" (skosimp*)
    (("" (case "vert(H1!1)(vo!1)")
      (("1" (lemma "cip0")
        (("1" (inst -1 "G!1" "H1!1" "H2!1" "vo!1")
          (("1" (assert) nil)))))
       ("2" (lemma "cip0")
        (("2" (inst -1 "G!1" "H2!1" "H1!1" "vo!1")
          (("2" (rewrite "intersection_commutative")
            (("2"
              (case-replace "union(H2!1, H1!1) = union(H1!1, H2!1)")
              (("1" (assert)
                (("1" (prop)
                  (("1" (hide -1 -2 -3 -4 -7)
                    (("1" (replace -1)
                      (("1" (hide -1) (("1" (grind) nil)))))))))))
               ("2" (hide -1 -2 -3 -4 -5 -6 -7 -8 -9 2 3 4)
                (("2" (expand "union")
                  (("2" (prop)
                    (("1" (rewrite "union_commutative") nil)
                     ("2" (rewrite "union_commutative")
                      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)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil graph_conn_piece nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (finite_intersection1 application-judgement "finite_set"
     finite_sets nil)
    (cip0 formula-decl nil graph_conn_piece nil)
    (union const-decl "graph[T]" graph_ops nil)
    (member const-decl "bool" sets nil)
    (empty? const-decl "bool" sets nil)
    (empty? const-decl "bool" graphs nil)
    (union const-decl "set" sets nil)
    (finite_union application-judgement "finite_set" finite_sets nil)
    (union_commutative formula-decl nil sets_lemmas nil)
    (intersection_commutative formula-decl nil sets_lemmas nil))
   nil))
 (connected_not_empty 0
  (connected_not_empty-1 nil 3251050559
   ("" (skosimp*)
    (("" (expand "empty?")
      (("" (expand "connected?")
        (("" (lemma " card_empty?[T]")
          (("" (inst?)
            (("" (iff)
              (("" (assert)
                (("" (prop)
                  (("1" (expand "singleton?")
                    (("1" (expand "size") (("1" (assert) nil)))))
                   ("2" (skosimp*)
                    (("2" (expand "empty?")
                      (("2" (inst -4 "v!1")
                        (("2" (expand "member")
                          (("2" (propax) nil))))))))))))))))))))))))
    nil)
   ((empty? const-decl "bool" graphs nil)
    (T formal-type-decl nil graph_conn_piece nil)
    (card_empty? formula-decl nil finite_sets nil)
    (size const-decl "nat" graphs nil)
    (singleton? const-decl "bool" graphs nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets 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)
    (connected? def-decl "bool" graph_conn_defs nil))
   nil))
 (conn_implies_piece 0
  (conn_implies_piece-1 nil 3251050559
   ("" (induct "G" 1 "graph_induction_vert")
    (("" (skosimp*)
      (("" (hide -1)
        (("" (lemma "not_piece_has_2")
          (("" (inst?)
            (("" (assert)
              (("" (expand "piece_connected?")
                (("" (rewrite "connected_not_empty")
                  (("" (assert)
                    (("" (skosimp*)
                      ((""
                        (case "(FORALL (vo: (vert(G!1))): deg(vo,G!1) > 0 IMPLIES NOT connected?(del_vert(G!1,vo)))")
                        (("1" (expand "connected?" -3)
                          (("1" (prop)
                            (("1" (use "singleton_piece")
                              (("1" (assert) nil)))
                             ("2" (skosimp*)
                              (("2"
                                (inst -3 "v!1")
                                (("2" (assert) nil)))))))))
                         ("2" (skosimp*)
                          (("2" (assert)
                            (("2" (reveal -2)
                              (("2"
                                (case "vert(H1!1)(vo!1)")
                                (("1"
                                  (lemma "cip3")
                                  (("1"
                                    (inst?)
                                    (("1"
                                      (inst -1 "vo!1")
                                      (("1" (assert) nil)))))))
                                 ("2"
                                  (lemma "cip3")
                                  (("2"
                                    (inst
                                     -1
                                     "G!1"
                                     "H2!1"
                                     "H1!1"
                                     "vo!1")
                                    (("2"
                                      (case-replace
                                       "union(H2!1, H1!1) = union(H1!1, H2!1)")
                                      (("1"
                                        (case-replace
                                         "intersection(vert(H2!1), vert(H1!1)) = intersection(vert(H1!1), vert(H2!1))")
                                        (("1"
                                          (hide -1 -2)
                                          (("1" (assert) nil)))
                                         ("2"
                                          (prop)
                                          (("1"
                                            (hide
                                             -1
                                             -2
                                             -3
                                             -4
                                             -5
                                             -7
                                             3
                                             4)
                                            (("1"
                                              (typepred "vo!1")
                                              (("1"
                                                (hide -2)
                                                (("1"
                                                  (grind)
                                                  (("1"
                                                    (hide
                                                     -1
                                                     -2
                                                     -3
                                                     -4
                                                     -5
                                                     -6
                                                     -7
                                                     -8
                                                     -9
                                                     2
                                                     3
                                                     4)
                                                    (("1"
                                                      (apply-extensionality
                                                       1
                                                       :hide?
                                                       t)
                                                      (("1"
                                                        (grind)
                                                        nil)))))
                                                   ("2"
                                                    (hide
                                                     -1
                                                     -2
                                                     -3
                                                     -4
                                                     -5
                                                     -6
                                                     -7
                                                     -8
                                                     2
                                                     3
                                                     4)
                                                    (("2"
                                                      (apply-extensionality
                                                       1
                                                       :hide?
                                                       t)
                                                      (("2"
                                                        (grind)
                                                        nil)))))))))))))
                                           ("2"
                                            (hide
                                             -1
                                             -2
                                             -3
                                             -4
                                             -5
                                             -6
                                             -7
                                             -8
                                             1
                                             3
                                             4
                                             5)
                                            (("2"
                                              (apply-extensionality
                                               1
                                               :hide?
                                               t)
                                              (("2"
                                                (grind)
                                                nil)))))))))
                                       ("2"
                                        (hide
                                         -1
                                         -2
                                         -3
                                         -4
                                         -5
                                         -6
                                         -7
                                         -8
                                         2
                                         3
                                         4)
                                        (("2"
                                          (apply-extensionality
                                           1
                                           :hide?
                                           t)
                                          (("1"
                                            (apply-extensionality
                                             1
                                             :hide?
                                             t)
                                            (("1" (grind) nil)))
                                           ("2"
                                            (apply-extensionality
                                             1
                                             :hide?
                                             t)
                                            (("2"
                                              (grind)
                                              nil))))))))))))))))))))))))))))))))))))))))))
    nil)
   ((not_piece_has_2 formula-decl nil graph_conn_piece nil)
    (connected_not_empty formula-decl nil graph_conn_piece nil)
    (union const-decl "graph[T]" graph_ops nil)
    (empty? const-decl "bool" graphs nil)
    (empty? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (intersection const-decl "set" sets nil)
    (union const-decl "set" sets nil)
    (finite_union application-judgement "finite_set" finite_sets nil)
    (cip3 formula-decl nil graph_conn_piece nil)
    (singleton_piece formula-decl nil graph_conn_piece 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)
    (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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (deg const-decl "nat" graph_deg nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (del_vert const-decl "graph[T]" graph_ops nil)
    (real_gt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (finite_intersection1 application-judgement "finite_set"
     finite_sets nil)
    (graph_induction_vert formula-decl nil graph_inductions nil)
    (T formal-type-decl nil graph_conn_piece nil)
    (piece_connected? const-decl "bool" graph_conn_defs nil)
    (connected? def-decl "bool" graph_conn_defs nil)
    (pred type-eq-decl nil defined_types 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)))


¤ Dauer der Verarbeitung: 0.39 Sekunden  (vorverarbeitet)  ¤



Druckansicht
unsichere Verbindung
Druckansicht
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