Anforderungen  |   Konzepte  |   Entwurf  |   Entwicklung  |   Qualitätssicherung  |   Lebenszyklus  |   Steuerung
 
 
 
 


Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: graph_conn_piece.prf   Sprache: Unknown

(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" (assertnil)))))))
         ("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" (assertnil)))
                                           ("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" (assertnil 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" (assertnil 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" (assertnil 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" (assertnil 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" (assertnil)))))))))))))))))
           ("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" (assertnil))))))))))))))))))))))
    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" (assertnil))))))))))))))
    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" (assertnil)))))
       ("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" (assertnil)))))
                   ("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" (assertnil)))
                             ("2" (skosimp*)
                              (("2"
                                (inst -3 "v!1")
                                (("2" (assertnil)))))))))
                         ("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" (assertnil)))))))
                                 ("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" (assertnil)))
                                         ("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.15 Sekunden  (vorverarbeitet)  ]

                                                                                                                                                                                                                                                                                                                                                                                                     


Neuigkeiten

     Aktuelles
     Motto des Tages

Software

     Produkte
     Quellcodebibliothek

Aktivitäten

     Artikel über Sicherheit
     Anleitung zur Aktivierung von SSL

Muße

     Gedichte
     Musik
     Bilder

Jenseits des Üblichen ....
    

Besucherstatistik

Besucherstatistik