Quelle  subgraphs.prf   Sprache: unbekannt

(subgraphs
 (finite_vert_subset 0
  (finite_vert_subset-1 nil 3251040622
   ("" (skosimp*)
    (("" (lemma "finite_subset[T]")
      (("" (inst?)
        (("" (inst -1 "vert(G!1)")
          (("" (assert) (("" (hide 2) (("" (grind) nil nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((T formal-type-decl nil subgraphs nil)
    (finite_subset formula-decl nil finite_sets nil)
    (is_finite const-decl "bool" finite_sets nil)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (graph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (pregraph type-eq-decl nil graphs nil)
    (finite_set type-eq-decl nil finite_sets nil)
    (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))
 (subgraph_TCC1 0
  (subgraph_TCC1-1 nil 3251040622
   ("" (skosimp*)
    (("" (lemma "finite_subset[doubleton[T]]")
      (("" (inst?)
        (("" (assert)
          (("" (inst - "edges(G!1)")
            (("" (assert) (("" (hide 2) (("" (grind) nil nil)) nil))
              nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((doubleton type-eq-decl nil doubletons nil)
    (dbl const-decl "set[T]" doubletons nil)
    (= const-decl "[T, T -> boolean]" equalities nil)
    (/= const-decl "boolean" notequal nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (set type-eq-decl nil sets nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil subgraphs nil)
    (finite_subset formula-decl nil finite_sets nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (is_finite const-decl "bool" finite_sets nil)
    (graph type-eq-decl nil graphs nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (pregraph type-eq-decl nil graphs nil)
    (finite_set type-eq-decl nil finite_sets nil))
   nil))
 (subgraph_TCC2 0
  (subgraph_TCC2-1 nil 3307708398
   ("" (skosimp*)
    (("" (lemma "finite_vert_subset") (("" (inst?) nil nil)) nil)) nil)
   ((finite_vert_subset formula-decl nil subgraphs nil)
    (T formal-type-decl nil subgraphs 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))
   nil))
 (subgraph_TCC3 0
  (subgraph_TCC3-2 nil 3307713815
   ("" (skosimp*)
    (("" (split +)
      (("1" (skosimp*)
        (("1" (typepred "G!1")
          (("1" (inst?)
            (("1" (assert)
              (("1" (inst?)
                (("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
              nil))
            nil))
          nil))
        nil)
       ("2" (grind) nil nil))
      nil))
    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 subgraphs nil)
    (NOT const-decl "[bool -> bool]" booleans nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil)
    (subgraph? const-decl "bool" subgraphs nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil))
   nil)
  (subgraph_TCC3-1 nil 3307708398 ("" (subtype-tcc) nil nil) nil nil))
 (subgraph_vert_sub 0
  (subgraph_vert_sub-1 nil 3251040622
   ("" (skosimp*)
    (("" (expand "subgraph")
      (("" (apply-extensionality 1 :hide? t)
        (("" (expand "subset?")
          (("" (inst?)
            (("" (expand "member")
              (("" (iff 1) (("" (ground) nil nil)) nil)) nil))
            nil))
          nil))
        nil))
      nil))
    nil)
   ((subgraph const-decl "Subgraph(G)" subgraphs nil)
    (subset? const-decl "bool" sets nil)
    (member const-decl "bool" sets nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (bool nonempty-type-eq-decl nil booleans nil)
    (AND const-decl "[bool, bool -> bool]" booleans nil)
    (set type-eq-decl nil sets 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)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil subgraphs nil))
   nil))
 (subgraph_lem 0
  (subgraph_lem-1 nil 3251040622
   ("" (skosimp*) (("" (assert) nil nil)) nil) nil nil))
 (subgraph_smaller 0
  (subgraph_smaller-1 nil 3251040622
   ("" (skosimp*)
    (("" (expand "size")
      (("" (expand "subgraph?")
        (("" (rewrite "card_subset[T]") nil nil)) nil))
      nil))
    nil)
   ((size const-decl "nat" graphs nil)
    (real_le_is_total_order name-judgement "(total_order?[real])"
     real_props nil)
    (subset_is_partial_order name-judgement "(partial_order?[set[T]])"
     sets_lemmas nil)
    (card_subset formula-decl nil finite_sets nil)
    (boolean nonempty-type-decl nil booleans nil)
    (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)
    (T formal-type-decl nil subgraphs nil)
    (subgraph? const-decl "bool" subgraphs nil))
   nil)))