Gedichte Musik Bilder Quellcodebibliothek Diashow Normaldarstellung
products/sources/formale sprachen/PVS/lnexp_fnd/  image not shown  

Quellcode-Bibliothek

© Kompilation durch diese Firma

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

Datei: max_array.pvs   Sprache: Lisp

Original von: PVS©
(graph_deg_sum
 (deg_lem0 0
  (deg_lem0-1 nil 3263108640
   ("" (skosimp*)
    (("" (expand "num_edges")
      (("" (rewrite "card_is_0[doubleton[T]]")
        (("" (assert)
          (("" (expand "deg")
            (("" (lemma "finite_emptyset[doubleton[T]]")
              ((""
                (case-replace
                 " (LAMBDA (v: T): card(incident_edges(v, G!1))) =
                       (LAMBDA (v: T): card(emptyset[doubleton[T]]))")
                (("1" (hide -1)
                  (("1" (rewrite "card_emptyset[doubleton[T]]")
                    (("1" (rewrite "sum_const")
                      (("1" (assert) nil nil)) nil))
                    nil))
                  nil)
                 ("2" (hide 2)
                  (("2" (apply-extensionality 1 :hide? t)
                    (("1" (lemma "incident_edges_emptyset")
                      (("1" (inst -1 "G!1" "x!1")
                        (("1" (assert) nil nil)) nil))
                      nil)
                     ("2" (skosimp*)
                      (("2" (rewrite "card_def[doubleton[T]]")
                        (("2" (lemma "incident_edges_emptyset")
                          (("2" (inst?) (("2" (assert) nil nil)) nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((num_edges const-decl "nat" graph_ops nil)
    (nil application-judgement "nat" graph_deg_sum nil)
    (nil application-judgement "int" graph_deg_sum nil)
    (finite_emptyset judgement-tcc nil finite_sets nil)
    (card_def formula-decl nil finite_sets nil)
    (incident_edges_emptyset formula-decl nil graph_deg nil)
    (G!1 skolem-const-decl "graph[T]" graph_deg_sum nil)
    (sum_const formula-decl nil finite_sets_sum_real "finite_sets/")
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (card_emptyset formula-decl nil finite_sets nil)
    (emptyset const-decl "set" sets nil)
    (incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
     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)
    (>= const-decl "bool" reals 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)
    (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)
    (deg const-decl "nat" graph_deg nil)
    (finite_emptyset name-judgement "finite_set" 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_sum 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)
    (card_is_0 formula-decl nil finite_sets nil))
   nil))
 (deg_lem2_TCC1 0
  (deg_lem2_TCC1-1 nil 3263108640
   ("" (skosimp*)
    (("" (replace -4 * rl) (("" (rewrite "finite_remove") nil nil))
      nil))
    nil)
   ((T formal-type-decl nil graph_deg_sum 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)
    (remove const-decl "set" sets 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)
    (finite_remove judgement-tcc nil finite_sets nil)
    (finite_remove application-judgement "finite_set[T]" graph_deg_sum
     nil))
   nil))
 (deg_lem2 0
  (deg_lem2-1 nil 3263108640
   ("" (skosimp*)
    (("" (rewrite "sum_f_g[T,real,0,+]")
      (("" (hide 2)
        (("" (skosimp*)
          (("" (typepred "x!2")
            (("" (replace -2 * rl)
              (("" (hide -2)
                (("" (expand "deg")
                  ((""
                    (case-replace
                     "incident_edges(x!2, del_edge(G!1,e!1)) = incident_edges(x!2, G!1)")
                    (("" (hide 2)
                      (("" (apply-extensionality 1 :hide? t)
                        (("" (expand "incident_edges")
                          (("" (iff 1)
                            (("" (ground)
                              (("1"
                                (lemma "del_edge_lem2[T]")
                                (("1"
                                  (inst?)
                                  (("1" (assert) nil nil))
                                  nil))
                                nil)
                               ("2"
                                (rewrite "del_edge_lem3")
                                (("2"
                                  (hide -5 -6 2)
                                  (("2" (grind) nil nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((sum_f_g formula-decl nil finite_sets_sum "finite_sets/")
    (bool nonempty-type-eq-decl nil booleans nil)
    (set type-eq-decl nil sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (/= const-decl "boolean" notequal nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dbl const-decl "set[T]" doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (pregraph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (graph type-eq-decl nil graphs nil)
    (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)
    (del_edge const-decl "graph[T]" graph_ops nil)
    (T formal-type-decl nil graph_deg_sum nil)
    (number nonempty-type-decl nil numbers nil)
    (boolean nonempty-type-decl nil booleans 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)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (restrict const-decl "R" restrict nil)
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (nil application-judgement "nat" graph_deg_sum nil)
    (nil application-judgement "int" graph_deg_sum nil)
    (nil application-judgement "finite_set[T]" graph_deg_sum nil)
    (finite_remove application-judgement "finite_set[T]" graph_deg_sum
     nil)
    (del_edge_lem2 formula-decl nil graph_ops nil)
    (remove const-decl "set" sets nil)
    (member const-decl "bool" sets nil)
    (del_edge_lem3 formula-decl nil graph_ops nil)
    (incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
     nil)
    (NOT const-decl "[bool -> bool]" booleans nil))
   nil))
 (edge_induction 0
  (edge_induction-1 nil 3263108640
   ("" (skosimp*)
    (("" (prop)
      (("1" (skosimp*) (("1" (inst?) nil nil)) nil)
       ("2" (skosimp*) (("2" (inst?) (("2" (inst?) nil nil)) nil))
        nil))
      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_deg_sum 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)
    (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)
    (num_edges const-decl "nat" graph_ops nil))
   nil))
 (deg_thm 0
  (deg_thm-1 nil 3263108640
   ("" (skosimp*)
    (("" (lemma "edge_induction")
      ((""
        (inst -1
         "(LAMBDA G: sum(vert(G), (LAMBDA (v: T): deg(v, G))) = 2 * num_edges(G))")
        (("" (flatten)
          (("" (hide -1)
            (("" (split -1)
              (("1" (inst -1 "G!1") nil nil)
               ("2" (hide 2)
                (("2" (induct "n")
                  (("1" (skosimp*)
                    (("1" (rewrite "deg_lem0") (("1" (assert) nil nil))
                      nil))
                    nil)
                   ("2" (skosimp*)
                    (("2" (name "Eo" "choose(edges(G!2))")
                      (("1" (inst -2 "del_edge(G!2,Eo)")
                        (("1" (rewrite "del_edge_num")
                          (("1" (assert)
                            (("1" (typepred "Eo")
                              (("1"
                                (skosimp*)
                                (("1"
                                  (case
                                   "member(x!1, remove(y!1, vert(G!2))) AND member(y!1, vert(G!2))
                                       AND is_finite[T](remove(x!1, remove(y!1, vert(G!2))))
                                       AND is_finite[T](remove[T](y!1, vert(G!2)))")
                                  (("1"
                                    (flatten)
                                    (("1"
                                      (name
                                       "V_r"
                                       "remove(x!1,remove(y!1,vert(G!2)))")
                                      (("1"
                                        (replace -1)
                                        (("1"
                                          (case-replace
                                           "sum(vert(G!2), (LAMBDA (v: T): deg(v, G!2))) =
                                          sum(V_r, (LAMBDA (v: T): deg(v, G!2)))
                                      + deg(x!1, G!2)
                                      + deg(y!1, G!2)")
                                          (("1"
                                            (hide -1)
                                            (("1"
                                              (case-replace
                                               "deg(x!1, G!2) = deg(x!1, del_edge(G!2,Eo)) + 1")
                                              (("1"
                                                (case-replace
                                                 "deg(y!1, G!2) = deg(y!1, del_edge(G!2,Eo)) + 1")
                                                (("1"
                                                  (case-replace
                                                   "sum(V_r, (LAMBDA (v: T): deg(v, G!2))) =
                                                      sum(V_r, (LAMBDA (v: T): deg(v, del_edge(G!2,Eo))))")
                                                  (("1"
                                                    (case-replace
                                                     "sum(V_r, (LAMBDA (v: T): deg(v, del_edge(G!2,Eo))))
                                                           = sum(vert(G!2), (LAMBDA (v: T): deg(v, del_edge(G!2,Eo))))
                                                - deg(x!1, del_edge(G!2,Eo))
                                                - deg(y!1, del_edge(G!2,Eo)) ")
                                                    (("1"
                                                      (assert)
                                                      (("1"
                                                        (rewrite
                                                         "vert_del_edge")
                                                        (("1"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil)
                                                     ("2"
                                                      (hide
                                                       -1
                                                       -2
                                                       -3
                                                       -9
                                                       -10
                                                       -11
                                                       -12
                                                       -13
                                                       2
                                                       3)
                                                      (("2"
                                                        (replace
                                                         -1
                                                         +
                                                         rl)
                                                        (("2"
                                                          (rewrite
                                                           "sum_remove_rew")
                                                          (("2"
                                                            (rewrite
                                                             "sum_remove_rew")
                                                            (("2"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil)
                                                   ("2"
                                                    (hide
                                                     -1
                                                     -2
                                                     -11
                                                     -12
                                                     3)
                                                    (("2"
                                                      (lemma
                                                       "deg_lem2")
                                                      (("2"
                                                        (inst?)
                                                        (("2"
                                                          (inst
                                                           -1
                                                           "dbl[T](x!1, y!1)")
                                                          (("1"
                                                            (assert)
                                                            (("1"
                                                              (hide
                                                               -1
                                                               -2
                                                               -3
                                                               -5
                                                               -6
                                                               2
                                                               3)
                                                              (("1"
                                                                (grind
                                                                 :exclude
                                                                 "edges")
                                                                nil
                                                                nil))
                                                              nil))
                                                            nil)
                                                           ("2"
                                                            (inst?)
                                                            (("2"
                                                              (assert)
                                                              nil
                                                              nil))
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil)
                                                 ("2"
                                                  (hide
                                                   -1
                                                   -2
                                                   -3
                                                   -4
                                                   -10
                                                   -11
                                                   2
                                                   3)
                                                  (("2"
                                                    (lemma
                                                     "deg_del_edge")
                                                    (("2"
                                                      (inst?)
                                                      (("2"
                                                        (inst -1 "x!1")
                                                        (("2"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil)
                                               ("2"
                                                (hide
                                                 -1
                                                 -2
                                                 -3
                                                 -8
                                                 -9
                                                 -10
                                                 2
                                                 3)
                                                (("2"
                                                  (lemma
                                                   "deg_del_edge")
                                                  (("2"
                                                    (inst?)
                                                    (("2"
                                                      (inst -1 "y!1")
                                                      (("2"
                                                        (rewrite
                                                         "dbl_comm")
                                                        (("2"
                                                          (assert)
                                                          nil
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil)
                                           ("2"
                                            (hide -4 -5 -8 -9 -10 2 3)
                                            (("2"
                                              (replace -1 + rl)
                                              (("2"
                                                (rewrite
                                                 "sum_remove_rew")
                                                (("2"
                                                  (rewrite
                                                   "sum_remove_rew")
                                                  (("2"
                                                    (assert)
                                                    nil
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil)
                                   ("2"
                                    (rewrite "finite_remove")
                                    (("2"
                                      (rewrite "finite_remove")
                                      (("2"
                                        (assert)
                                        (("2"
                                          (expand "member")
                                          (("2"
                                            (expand "remove")
                                            (("2"
                                              (expand "member")
                                              (("2"
                                                (hide -3 -4 -5 3)
                                                (("2"
                                                  (replace -1)
                                                  (("2"
                                                    (hide -1)
                                                    (("2"
                                                      (typepred "G!2")
                                                      (("2"
                                                        (inst?)
                                                        (("1"
                                                          (assert)
                                                          (("1"
                                                            (inst-cp
                                                             -1
                                                             "x!1")
                                                            (("1"
                                                              (inst
                                                               -1
                                                               "y!1")
                                                              (("1"
                                                                (expand
                                                                 "dbl")
                                                                (("1"
                                                                  (assert)
                                                                  nil
                                                                  nil))
                                                                nil))
                                                              nil))
                                                            nil))
                                                          nil)
                                                         ("2"
                                                          (inst?)
                                                          (("2"
                                                            (assert)
                                                            nil
                                                            nil))
                                                          nil))
                                                        nil))
                                                      nil))
                                                    nil))
                                                  nil))
                                                nil))
                                              nil))
                                            nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil)
                       ("2" (hide -1 2)
                        (("2" (expand "nonempty?")
                          (("2" (lemma "deg_lem0")
                            (("2" (inst?)
                              (("2"
                                (split -1)
                                (("1"
                                  (expand "num_edges")
                                  (("1"
                                    (lemma "card_empty?[doubleton[T]]")
                                    (("1"
                                      (inst?)
                                      (("1"
                                        (assert)
                                        (("1"
                                          (replace -3)
                                          (("1" (assert) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil)
                                 ("2"
                                  (expand "num_edges")
                                  (("2"
                                    (lemma "card_empty?[doubleton[T]]")
                                    (("2"
                                      (inst?)
                                      (("2"
                                        (assert)
                                        (("2"
                                          (replace -2)
                                          (("2" (propax) nil nil))
                                          nil))
                                        nil))
                                      nil))
                                    nil))
                                  nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((edge_induction formula-decl nil graph_deg_sum nil)
    (nat_induction formula-decl nil naturalnumbers nil)
    (deg_lem0 formula-decl nil graph_deg_sum nil)
    (nonempty? const-decl "bool" sets nil)
    (choose const-decl "(p)" sets nil)
    (del_edge_num formula-decl nil graph_ops nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (finite_remove application-judgement "finite_set[T]" graph_deg_sum
     nil)
    (member const-decl "bool" sets nil)
    (remove const-decl "set" sets nil)
    (nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (deg_del_edge formula-decl nil graph_deg nil)
    (odd_plus_odd_is_even application-judgement "even_int" integers
     nil)
    (sum_remove_rew formula-decl nil finite_sets_sum_real
     "finite_sets/")
    (int_plus_int_is_int application-judgement "int" integers nil)
    (even_minus_even_is_even application-judgement "even_int" integers
     nil)
    (nil application-judgement "finite_set[T]" graph_deg_sum nil)
    (vert_del_edge formula-decl nil graph_ops nil)
    (- const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (deg_lem2 formula-decl nil graph_deg_sum nil)
    (x!1 skolem-const-decl "T" graph_deg_sum nil)
    (y!1 skolem-const-decl "T" graph_deg_sum nil)
    (injective? const-decl "bool" functions nil)
    (empty? const-decl "bool" sets nil)
    (posint_plus_nnint_is_posint application-judgement "posint"
     integers nil)
    (dbl_comm formula-decl nil doubletons nil)
    (finite_remove judgement-tcc nil finite_sets nil)
    (nnint_plus_posint_is_posint application-judgement "posint"
     integers nil)
    (del_edge const-decl "graph[T]" graph_ops nil)
    (card_empty? formula-decl nil finite_sets nil)
    (num_edges const-decl "nat" graph_ops nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (deg const-decl "nat" graph_deg nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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)
    (sum def-decl "R" finite_sets_sum "finite_sets/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (restrict const-decl "R" restrict nil)
    (numfield nonempty-type-eq-decl nil number_fields 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)
    (is_finite const-decl "bool" finite_sets nil)
    (number nonempty-type-decl nil numbers 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)
    (T formal-type-decl nil graph_deg_sum nil)
    (nil application-judgement "int" graph_deg_sum nil)
    (nil application-judgement "nat" graph_deg_sum nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (real_plus_real_is_real application-judgement "real" reals nil))
   nil))
 (subgraph_deg 0
  (subgraph_deg-1 nil 3263108640
   ("" (skosimp*)
    (("" (expand "deg")
      (("" (expand "incident_edges")
        (("" (expand "subgraph?")
          (("" (flatten)
            (("" (hide -1 -3)
              (("" (lemma "card_subset[doubletons[T].doubleton]")
                (("" (inst?)
                  (("1" (assert)
                    (("1" (hide 2)
                      (("1" (expand "subset?")
                        (("1" (skosimp*)
                          (("1" (expand "member")
                            (("1" (flatten)
                              (("1"
                                (inst?)
                                (("1" (assert) nil nil))
                                nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("2" (hide -1 2)
                    (("2"
                      (lemma "finite_subset[doubletons[T].doubleton]")
                      (("2" (inst?)
                        (("2" (inst?)
                          (("2" (assert)
                            (("2" (hide -1 2) (("2" (grind) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil)
                   ("3" (hide -1 2)
                    (("3"
                      (lemma "finite_subset[doubletons[T].doubleton]")
                      (("3" (inst?)
                        (("3" (inst?)
                          (("3" (assert)
                            (("3" (hide -1 2) (("3" (grind) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((deg const-decl "nat" graph_deg nil)
    (subgraph? const-decl "bool" subgraphs nil)
    (v!1 skolem-const-decl "T" graph_deg_sum nil)
    (GS!1 skolem-const-decl "graph[T]" graph_deg_sum 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)
    (G!1 skolem-const-decl "graph[T]" graph_deg_sum nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (finite_subset formula-decl nil finite_sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (card_subset formula-decl nil finite_sets nil)
    (T formal-type-decl nil graph_deg_sum 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)
    (incident_edges const-decl "finite_set[doubleton[T]]" graph_deg
     nil))
   nil))
 (sum_gt_bound 0
  (sum_gt_bound-1 nil 3263108683
   ("" (induct "S" 1 "finite_set_induction_rest")
    (("1" (skosimp*)
      (("1" (rewrite "sum_emptyset")
        (("1" (rewrite "card_emptyset")
          (("1" (hide -1) (("1" (assert) nil nil)) nil)) nil))
        nil))
      nil)
     ("2" (skosimp*)
      (("2" (expand "sum" 1)
        (("2" (inst -1 "B!1" "f!1")
          (("2" (split -1)
            (("1" (inst -2 "choose(SS!1)")
              (("1" (rewrite "card_rest") (("1" (assert) nil nil))
                nil))
              nil)
             ("2" (hide 2)
              (("2" (skosimp*)
                (("2" (inst -1 "t!1")
                  (("2" (typepred "t!1")
                    (("2" (grind :exclude "choose") nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((rest const-decl "set" sets nil)
    (SS!1 skolem-const-decl "non_empty_finite_set[T]" graph_deg_sum
     nil)
    (t!1 skolem-const-decl "(rest(SS!1))" graph_deg_sum nil)
    (finite_remove application-judgement "finite_set[T]" graph_deg_sum
     nil)
    (/= const-decl "boolean" notequal nil)
    (member const-decl "bool" sets nil)
    (remove const-decl "set" sets nil)
    (choose const-decl "(p)" sets nil)
    (nonempty? const-decl "bool" sets nil)
    (non_empty_finite_set type-eq-decl nil finite_sets nil)
    (empty? const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (finite_rest application-judgement "finite_set[T]" graph_deg_sum
     nil)
    (int_minus_int_is_int application-judgement "int" integers nil)
    (card_rest formula-decl nil finite_sets nil)
    (card_emptyset formula-decl nil finite_sets nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (sum_emptyset formula-decl nil finite_sets_sum "finite_sets/")
    (finite_set_induction_rest formula-decl nil finite_sets_inductions
     "finite_sets/")
    (T formal-type-decl nil graph_deg_sum nil)
    (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
    (Card const-decl "nat" finite_sets nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (int nonempty-type-eq-decl nil integers nil)
    (integer_pred const-decl "[rational -> boolean]" integers nil)
    (rational nonempty-type-from-decl nil rationals nil)
    (rational_pred const-decl "[real -> boolean]" rationals nil)
    (* const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (sum def-decl "R" finite_sets_sum "finite_sets/")
    (+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
    (restrict const-decl "R" restrict nil)
    (numfield nonempty-type-eq-decl nil number_fields nil)
    (>= const-decl "bool" reals nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans 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)
    (pred type-eq-decl nil defined_types 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)
    (real_plus_real_is_real application-judgement "real" reals nil)
    (real_times_real_is_real application-judgement "real" reals nil))
   nil))
 (deg_gt_one 0
  (deg_gt_one-1 nil 3263108705
   ("" (skosimp*)
    (("" (lemma "sum_gt_bound")
      (("" (inst -1 "2" "vert(G!1)" "LAMBDA (v:T):deg(v,G!1)")
        (("" (bddsimp)
          (("1" (lemma "deg_thm")
            (("1" (inst -1 "G!1")
              (("1" (replace -1 -2)
                (("1" (hide -1 -3) (("1" (grind) nil nil)) nil)) nil))
              nil))
            nil)
           ("2" (assert) nil nil))
          nil))
        nil))
      nil))
    nil)
   ((sum_gt_bound formula-decl nil graph_deg_sum nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (nnint_times_nnint_is_nnint application-judgement "nonneg_int"
     integers nil)
    (even_times_int_is_even application-judgement "even_int" integers
     nil)
    (mult_divides1 application-judgement "(divides(n))" divides nil)
    (mult_divides2 application-judgement "(divides(m))" divides nil)
    (size const-decl "nat" graphs nil)
    (num_edges const-decl "nat" graph_ops nil)
    (deg_thm formula-decl nil graph_deg_sum nil)
    (deg const-decl "nat" graph_deg nil)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (>= const-decl "bool" reals 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)
    (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)
    (T formal-type-decl nil graph_deg_sum 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)
    (boolean nonempty-type-decl nil booleans nil)
    (number nonempty-type-decl nil numbers nil))
   nil)))


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