Quelle  graph_inductions.prf   Sprache: unbekannt

(graph_inductions
 (size_prep 0
  (size_prep-1 nil 3307708422 ("" (grind) nil nil)
   ((G!1 skolem-const-decl "graph[T]" graph_inductions nil)
    (card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
    (Card const-decl "nat" finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (NOT const-decl "[bool -> bool]" booleans 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)
    (nat nonempty-type-eq-decl nil naturalnumbers nil)
    (set type-eq-decl nil sets nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (dbl const-decl "set[T]" doubletons nil)
    (doubleton type-eq-decl nil doubletons nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (pregraph type-eq-decl nil graphs nil)
    (graph type-eq-decl nil graphs nil)
    (real_ge_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (G!1 skolem-const-decl "graph[T]" graph_inductions nil)
    (T formal-type-decl nil graph_inductions nil)
    (size const-decl "nat" graphs nil)
    (/= const-decl "boolean" notequal nil))
   nil))
 (graph_induction_vert 0
  (graph_induction_vert-1 nil 3307708422
   ("" (skosimp)
    (("" (lemma "size_prep")
      (("" (inst -1 "P!1")
        (("" (flatten)
          (("" (hide -1)
            (("" (split -1)
              (("1" (propax) nil nil)
               ("2" (hide 2)
                (("2" (induct "n" 1 "NAT_induction")
                  (("2" (skosimp*)
                    (("2" (inst -3 "G!1")
                      (("2" (split -3)
                        (("1" (propax) nil nil)
                         ("2" (skosimp*)
                          (("2" (inst -2 "size(GG!1)")
                            (("2" (assert) (("2" (inst?) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((size_prep formula-decl nil graph_inductions 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)
    (size const-decl "nat" graphs nil)
    (NAT_induction formula-decl nil naturalnumbers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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_inductions nil))
   nil))
 (graph_induction_vert_not 0
  (graph_induction_vert_not-1 nil 3307708422
   ("" (skosimp*)
    (("" (lemma "graph_induction_vert")
      (("" (inst -1 "(LAMBDA (GG: graph[T]): NOT P!1(GG))")
        (("" (prop)
          (("1" (inst?) nil nil)
           ("2" (skosimp*)
            (("2" (inst -3 "G!2")
              (("2" (assert)
                (("2" (skosimp*)
                  (("2" (inst -1 "GG!1") (("2" (assert) nil nil)) nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((graph_induction_vert formula-decl nil graph_inductions nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props nil)
    (NOT const-decl "[bool -> bool]" booleans 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_inductions nil))
   nil))
 (num_edges_prep 0
  (num_edges_prep-1 nil 3307708422
   ("" (skosimp*)
    (("" (prop)
      (("1" (skosimp*) (("1" (inst?) nil nil)) nil)
       ("2" (skosimp*)
        (("2" (inst?) (("2" (assert) (("2" (inst?) nil 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_inductions nil)
    (num_edges const-decl "nat" graph_ops 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))
   nil))
 (graph_induction_edge 0
  (graph_induction_edge-1 nil 3307708422
   ("" (skosimp)
    (("" (lemma "num_edges_prep")
      (("" (inst -1 "P!1")
        (("" (flatten)
          (("" (hide -1)
            (("" (split -1)
              (("1" (propax) nil nil)
               ("2" (hide 2)
                (("2" (induct "n" 1 "NAT_induction")
                  (("2" (skosimp*)
                    (("2" (inst -3 "G!1")
                      (("2" (split -3)
                        (("1" (propax) nil nil)
                         ("2" (skosimp*)
                          (("2" (inst -2 "num_edges(GG!1)")
                            (("2" (assert) (("2" (inst?) nil nil))
                              nil))
                            nil))
                          nil))
                        nil))
                      nil))
                    nil))
                  nil))
                nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((num_edges_prep formula-decl nil graph_inductions 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)
    (NAT_induction formula-decl nil naturalnumbers nil)
    (real_lt_is_strict_total_order name-judgement
     "(strict_total_order?[real])" real_props 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_inductions nil))
   nil)))

quality100%

[ zur Elbe Produktseite wechseln0.18Quellennavigators  Analyse erneut starten  ]