| products/Sources/formale Sprachen/PVS/graphs/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: sep_sets.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(sep_sets
(del_verts_TCC1 0 (del_verts_TCC1-1 nil 3251040627 ("" (skosimp*) (("" (lemma "finite_subset[doubleton[T]]") (("" (inst?) (("" (inst - "edges(G!1)") (("" (assert) (("" (hide 2) (("" (grind) 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 sep_sets nil) (finite_subset formula-decl nil 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) (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)) (del_verts_TCC2 0 (del_verts_TCC2-1 nil 3307708403 ("" (skosimp*) (("" (expand "difference") (("" (expand "member") (("" (inst?) (("" (assert) (("" (typepred "G!1") (("" (inst?) (("" (assert) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((difference const-decl "set" sets nil) (T formal-type-decl nil sep_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) (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)) nil)) (sep_set_exists 0 (sep_set_exists-1 nil 3251040627 ("" (skosimp*) (("" (case "s!1 = t!1 OR edge?(G!1)(s!1,t!1)") (("1" (inst 1 "vert(G!1)") (("1" (ground) nil nil)) nil) ("2" (inst 2 "{t: T | vert(G!1)(t) AND t /= s!1 AND t /= t!1}") (("2" (prop) (("1" (lemma "finite_subset[T]") (("1" (inst?) (("1" (inst?) (("1" (assert) (("1" (hide 2 3 4) (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 4 5) (("2" (expand "separates") (("2" (skosimp*) (("2" (expand "walk_from?") (("2" (flatten) (("2" (case "length(w!1) = 1") (("1" (replace -1) (("1" (hide -1) (("1" (assert) nil nil)) nil)) nil) ("2" (case-replace "length(w!1) = 2") (("1" (assert) (("1" (expand "walk?") (("1" (flatten) (("1" (inst -5 "0") (("1" (assert) (("1" (expand "del_verts") (("1" (expand "edge?") (("1" (expand "finseq_appl") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "FORALL (i: below(length(w!1))): seq(w!1)(i) = s!1 OR seq(w!1)(i) = t!1") (("1" (expand "walk?") (("1" (flatten) (("1" (inst -5 "0") (("1" (assert) (("1" (expand "finseq_appl") (("1" (expand "edge?") (("1" (expand "del_verts") (("1" (flatten) (("1" (inst -1 "1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "walk_verts_in") (("2" (inst?) (("1" (split -1) (("1" (hide -4) (("1" (expand "verts_in?") (("1" (expand "del_verts") (("1" (expand "difference") (("1" (expand "member") (("1" (skosimp*) (("1" (inst?) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (hide -1 -2 -3 2 3 4 5 6) (("2" (lemma "finite_subset[T]") (("2" (inst?) (("2" (inst -1 "vert(G!1)") (("2" (assert) (("2" (hide 2) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((edge? const-decl "bool" graphs 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 "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (T formal-type-decl nil sep_sets nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (s!1 skolem-const-decl "T" sep_sets nil) (t!1 skolem-const-decl "T" sep_sets nil) (G!1 skolem-const-decl "graph[T]" sep_sets nil) (TRUE const-decl "bool" booleans nil) (seps type-eq-decl nil sep_sets nil) (separates const-decl "bool" sep_sets nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (is_finite const-decl "bool" 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) (finite_subset formula-decl nil finite_sets nil) (walk_from? const-decl "bool" walks nil) (number nonempty-type-decl nil numbers nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences 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) (prewalk type-eq-decl nil walks nil) (odd_minus_odd_is_even application-judgement "even_int" integers nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (difference const-decl "set" sets nil) (verts_in? const-decl "bool" walks nil) (walk_verts_in formula-decl nil walks nil) (even_minus_odd_is_odd application-judgement "odd_int" integers nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nil application-judgement "finite_set[T]" sep_sets nil) (finite_difference application-judgement "finite_set" finite_sets nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (del_verts const-decl "graph[T]" sep_sets 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) (walk? const-decl "bool" walks nil)) nil)) (min_sep_set_TCC1 0 (min_sep_set_TCC1-1 nil 3251040627 ("" (skosimp*) (("" (lemma "sep_set_exists") (("" (inst?) nil nil)) nil)) nil) ((sep_set_exists formula-decl nil sep_sets nil) (T formal-type-decl nil sep_sets 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)) (min_sep_set_edge 0 (min_sep_set_edge-1 nil 3251040627 ("" (skosimp*) (("" (expand "separable?") (("" (expand "min_sep_set") (("" (lemma "min_in[seps(G!1, s!1, t!1), (LAMBDA (v: seps(G!1, s!1, t!1)): card(v)), (LAMBDA (v: seps(G!1, s!1, t!1)): TRUE)]") (("1" (typepred "min[seps(G!1, s!1, t!1), (LAMBDA (v: seps(G!1, s!1, t!1)): card(v)), (LAMBDA (v: seps(G!1, s!1, t!1)): TRUE)]") (("1" (expand "minimal?") (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "sep_set_exists") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ((separable? const-decl "bool" sep_sets nil) (TRUE const-decl "bool" booleans 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) (seps type-eq-decl nil sep_sets nil) (separates const-decl "bool" sep_sets nil) (edge? const-decl "bool" graphs 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 "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def 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) (T formal-type-decl nil sep_sets nil) (min_in formula-decl nil abstract_min nil) (NOT const-decl "[bool -> bool]" booleans nil) (minimal? const-decl "bool" abstract_min nil) (min const-decl "{S: T | minimal?(S)}" abstract_min nil) (sep_set_exists formula-decl nil sep_sets nil) (min_sep_set const-decl "finite_set[T]" sep_sets nil)) nil)) (min_sep_set_card 0 (min_sep_set_card-1 nil 3251040627 ("" (skosimp*) (("" (expand "min_sep_set") (("" (lemma "min_is_min[seps(G!1, s!1, t!1), (LAMBDA (v: seps(G!1, s!1, t!1)): card(v)), (LAMBDA (v: seps(G!1, s!1, t!1)): TRUE)]") (("1" (inst -1 "V!1") (("1" (beta) (("1" (propax) nil nil)) nil) ("2" (hide 2) (("2" (ground) (("1" (expand "separates") (("1" (flatten) (("1" (inst 4 "gen_seq1(G!1,s!1)") (("1" (expand "walk_from?") (("1" (expand "gen_seq1") (("1" (expand "walk?") (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (expand "del_verts") (("1" (expand "difference") (("1" (expand "member") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "separates") (("2" (flatten) (("2" (inst 4 "gen_seq2(G!1,s!1,t!1)") (("2" (expand "walk_from?") (("2" (expand "gen_seq2") (("2" (expand "del_verts") (("2" (expand "walk?") (("2" (split 4) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (expand "difference") (("1" (expand "member") (("1" (ground) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "finseq_appl") (("2" (expand "edge?") (("2" (flatten) (("2" (assert) (("2" (skosimp*) (("2" (expand "dbl") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sep_set_exists") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ((min_sep_set const-decl "finite_set[T]" sep_sets nil) (sep_set_exists formula-decl nil sep_sets nil) (G!1 skolem-const-decl "graph[T]" sep_sets nil) (s!1 skolem-const-decl "(vert(G!1))" sep_sets nil) (t!1 skolem-const-decl "(vert(G!1))" sep_sets nil) (V!1 skolem-const-decl "finite_set[T]" sep_sets nil) (walk_from? const-decl "bool" walks nil) (walk? const-decl "bool" walks nil) (difference const-decl "set" sets nil) (member const-decl "bool" sets nil) (del_verts const-decl "graph[T]" sep_sets nil) (below type-eq-decl nil nat_types nil) (finseq type-eq-decl nil finite_sequences nil) (> const-decl "bool" reals nil) (prewalk type-eq-decl nil walks nil) (verts_in? const-decl "bool" walks nil) (Seq type-eq-decl nil walks nil) (gen_seq1 const-decl "Seq(G)" walks nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nil application-judgement "finite_set[T]" sep_sets nil) (gen_seq2 const-decl "Seq(G)" walks nil) (min_is_min formula-decl nil abstract_min nil) (T formal-type-decl nil sep_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) (IF const-decl "[boolean, T, T -> T]" if_def nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal 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) (edge? const-decl "bool" graphs nil) (separates const-decl "bool" sep_sets nil) (seps type-eq-decl nil sep_sets 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) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (TRUE const-decl "bool" booleans nil)) nil)) (min_sep_set_seps 0 (min_sep_set_seps-1 nil 3251040627 ("" (skosimp*) (("" (expand "separable?") (("" (flatten) (("" (lemma "min_in[seps(G!1, s!1, t!1), (LAMBDA (v: seps(G!1, s!1, t!1)): card(v)), (LAMBDA (v: seps(G!1, s!1, t!1)): TRUE)]") (("1" (typepred "min[seps(G!1, s!1, t!1), (LAMBDA (v: seps(G!1, s!1, t!1)): card(v)), (LAMBDA (v: seps(G!1, s!1, t!1)): TRUE)]") (("1" (assert) (("1" (expand "min_sep_set") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (lemma "sep_set_exists") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ((separable? const-decl "bool" sep_sets nil) (TRUE const-decl "bool" booleans 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) (seps type-eq-decl nil sep_sets nil) (separates const-decl "bool" sep_sets nil) (edge? const-decl "bool" graphs 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 "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def 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) (T formal-type-decl nil sep_sets nil) (min_in formula-decl nil abstract_min nil) (min_sep_set const-decl "finite_set[T]" sep_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (minimal? const-decl "bool" abstract_min nil) (min const-decl "{S: T | minimal?(S)}" abstract_min nil) (sep_set_exists formula-decl nil sep_sets nil)) nil)) (min_sep_set_vert 0 (min_sep_set_vert-1 nil 3251040627 ("" (skosimp*) (("" (typepred "min[seps(G!1, s!1, t!1), (LAMBDA (v: seps(G!1, s!1, t!1)): card(v)), (LAMBDA (v: seps(G!1, s!1, t!1)): TRUE)]") (("1" (hide -1 -2 -3) (("1" (expand "minimal?") (("1" (inst -1 "remove(v!1,(min_sep_set(G!1, s!1, t!1)))") (("1" (rewrite "card_remove[T]") (("1" (assert) (("1" (expand "min_sep_set" -1) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (split 1) (("1" (flatten) (("1" (lemma "min_sep_set_edge") (("1" (inst?) (("1" (split -1) (("1" (replace -1) (("1" (propax) nil nil)) nil) ("2" (hide -1) (("2" (expand "separable?") (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (flatten) (("2" (ground) (("2" (lemma "min_sep_set_seps") (("2" (inst?) (("2" (assert) (("2" (expand "separates") (("2" (flatten) (("2" (expand "remove") (("2" (expand "member") (("2" (assert) (("2" (skosimp*) (("2" (inst 3 "w!1") (("2" (expand "walk_from?") (("2" (flatten) (("2" (expand "walk?") (("2" (flatten) (("2" (assert) (("2" (split 3) (("1" (hide -4) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (expand "del_verts") (("1" (expand "difference") (("1" (expand "member") (("1" (inst -3 "i!1") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -3) (("2" (skosimp*) (("2" (inst?) (("2" (assert) (("2" (expand "edge?") (("2" (flatten) (("2" (expand "finseq_appl") (("2" (expand "del_verts") (("2" (flatten) (("2" (assert) (("2" (skosimp*) (("2" (expand "dbl") (("2" (inst -7 "v!2") (("2" (assert) (("2" (split -7) (("1" (propax) nil nil) ("2" (case-replace "v!1 = v!2") (("1" (hide -1 -3 -5 -6 -7 -8 -9 1 2 3 4 5) (("1" (reveal -9) (("1" (expand "verts_in?") (("1" (expand "del_verts") (("1" (expand "difference") (("1" (expand "member") (("1" (split -3) (("1" (inst?) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil) ("2" (inst?) (("2" (flatten) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "sep_set_exists") (("2" (inst?) nil nil)) nil)) nil)) nil) ((min const-decl "{S: T | minimal?(S)}" abstract_min nil) (minimal? const-decl "bool" abstract_min nil) (TRUE const-decl "bool" booleans 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) (seps type-eq-decl nil sep_sets nil) (separates const-decl "bool" sep_sets nil) (edge? const-decl "bool" graphs 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 "boolean" notequal nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (IF const-decl "[boolean, T, T -> T]" if_def 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) (T formal-type-decl nil sep_sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (min_sep_set_edge formula-decl nil sep_sets nil) (separable? const-decl "bool" sep_sets nil) (prewalk type-eq-decl nil walks nil) (> const-decl "bool" reals nil) (finseq type-eq-decl nil finite_sequences nil) (below type-eq-decl nil nat_types nil) (verts_in? const-decl "bool" walks nil) (del_verts const-decl "graph[T]" sep_sets nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (difference const-decl "set" sets nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (nil application-judgement "finite_set[T]" sep_sets nil) (walk? const-decl "bool" walks nil) (walk_from? const-decl "bool" walks nil) (member const-decl "bool" sets nil) (min_sep_set_seps formula-decl nil sep_sets nil) (card_remove formula-decl nil finite_sets nil) (int_minus_int_is_int application-judgement "int" integers nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (min_sep_set const-decl "finite_set[T]" sep_sets nil) (v!1 skolem-const-decl "T" sep_sets nil) (remove const-decl "set" sets nil) (G!1 skolem-const-decl "graph[T]" sep_sets nil) (t!1 skolem-const-decl "T" sep_sets nil) (s!1 skolem-const-decl "T" sep_sets nil) (finite_remove application-judgement "finite_set" finite_sets nil) (sep_set_exists formula-decl nil sep_sets nil)) nil)) (ends_not_in_min_sep_set 0 (ends_not_in_min_sep_set-1 nil 3251040627 ("" (skosimp*) (("" (lemma "min_sep_set_seps") (("" (inst?) (("" (assert) (("" (expand "separates") (("" (flatten) (("" (hide 3) (("" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((min_sep_set_seps formula-decl nil sep_sets nil) (separates const-decl "bool" sep_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) (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 sep_sets nil)) nil)) (walk?_del_verts_not 0 (walk?_del_verts_not-1 nil 3251040627 ("" (skosimp*) (("" (expand "walk?") (("" (split +) (("1" (flatten) (("1" (hide -2) (("1" (expand "verts_in?") (("1" (skosimp*) (("1" (expand "del_verts") (("1" (expand "intersection") (("1" (expand "empty?") (("1" (expand "difference") (("1" (expand "member") (("1" (inst?) (("1" (assert) (("1" (inst?) (("1" (assert) (("1" (expand "verts_of") (("1" (inst?) (("1" (expand "finseq_appl") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "edge?") (("2" (inst?) (("2" (assert) (("2" (flatten) (("2" (assert) (("2" (expand "del_verts") (("2" (expand "empty?") (("2" (expand "intersection") (("2" (expand "member") (("2" (skosimp*) (("2" (inst?) (("2" (expand "verts_of") (("2" (assert) (("2" (expand "dbl") (("2" (split -3) (("1" (inst?) (("1" (assert) 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)) nil)) nil) ((walk? const-decl "bool" walks nil) (dbl const-decl "set[T]" doubletons nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (finite_intersection1 application-judgement "finite_set" finite_sets nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (edge? const-decl "bool" graphs nil) (nil application-judgement "finite_set[T]" sep_sets nil) (verts_in? const-decl "bool" walks nil) (del_verts const-decl "graph[T]" sep_sets nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences nil) (verts_of const-decl "finite_set[T]" walks nil) (below type-eq-decl nil naturalnumbers nil) (prewalk type-eq-decl nil walks nil) (> const-decl "bool" reals nil) (finseq type-eq-decl nil finite_sequences nil) (T formal-type-decl nil sep_sets nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans 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) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (difference const-decl "set" sets nil) (intersection const-decl "set" sets nil)) nil)) (adj_verts_TCC1 0 (adj_verts_TCC1-1 nil 3251040627 ("" (skosimp*) (("" (lemma "finite_subset[T]") (("" (inst?) (("" (inst -1 "vert(G!1)") (("" (assert) (("" (hide 2) (("" (grind) (("1" (typepred "G!1") (("1" (inst?) (("1" (assert) (("1" (inst?) nil nil)) nil) ("2" (inst 1 "x!2" "y!1") nil nil)) nil)) nil) ("2" (typepred "G!1") (("2" (inst?) (("1" (assert) (("1" (inst?) nil nil)) nil) ("2" (inst 1 "x!2" "y!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil sep_sets nil) (finite_subset formula-decl nil finite_sets nil) (nil application-judgement "finite_set[T]" sep_sets 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) (NOT const-decl "[bool -> bool]" booleans nil) (incident_edges const-decl "finite_set[doubleton[T]]" graph_deg 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) (doubleton type-eq-decl nil doubletons nil) (Dbl 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)) (adj_verts_lem 0 (adj_verts_lem-1 nil 3251040627 ("" (skosimp*) (("" (lemma "card_eq_bij[T,Dbl]") (("" (expand "deg") (("" (inst?) (("" (assert) (("" (hide 2) (("" (inst 1 "(LAMBDA (vv: (adj_verts(G!1, s!1))): dbl[T](s!1,vv))") (("1" (expand "bijective?") (("1" (prop) (("1" (expand "injective?") (("1" (skosimp*) (("1" (case "dbl[T](s!1, x1!1)(x1!1) = dbl[T](s!1, x2!1)(x1!1)") (("1" (case "dbl[T](s!1, x1!1)(x2!1) = dbl[T](s!1, x2!1)(x2!1)") (("1" (hide -3) (("1" (expand "dbl") (("1" (ground) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (expand "surjective?") (("2" (skosimp*) (("2" (typepred "y!1") (("2" (skosimp*) (("2" (replace -1) (("2" (case "s!1 = x!1 OR s!1 = y!2") (("1" (split -1) (("1" (replace -1) (("1" (inst 2 "y!2") (("1" (expand "adj_verts") (("1" (inst + "dbl[T](x!1, y!2)") (("1" (assert) (("1" (expand "dbl") (("1" (propax) nil nil)) nil)) nil) ("2" (inst?) (("2" (expand "dbl") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst 2 "x!1") (("1" (apply-extensionality 2 :hide? t) (("1" (expand "dbl") (("1" (iff 1) (("1" (ground) nil nil)) nil)) nil)) nil) ("2" (expand "adj_verts") (("2" (inst?) (("1" (assert) (("1" (expand "dbl") (("1" (propax) nil nil)) nil)) nil) ("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 3) (("2" (expand "incident_edges") (("2" (flatten) (("2" (hide -1) (("2" (expand "dbl") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (prop) (("1" (inst?) (("1" (typepred "vv!1") (("1" (expand "adj_verts") (("1" (skosimp*) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (typepred "vv!1") (("2" (expand "adj_verts") (("2" (skosimp*) (("2" (expand "incident_edges") (("2" (flatten) (("2" (lemma "edge_has_2_verts") (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Dbl 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 sep_sets nil) (card_eq_bij formula-decl nil finite_sets_card_eq "finite_sets/") (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets 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) (adj_verts const-decl "finite_set[T]" sep_sets nil) (incident_edges const-decl "finite_set[doubleton[T]]" graph_deg nil) (edge_has_2_verts formula-decl nil graphs nil) (bijective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (NOT const-decl "[bool -> bool]" booleans nil) (y!2 skolem-const-decl "T" sep_sets nil) (x!1 skolem-const-decl "T" sep_sets nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (injective? const-decl "bool" functions nil) (s!1 skolem-const-decl "T" sep_sets nil) (G!1 skolem-const-decl "graph[T]" sep_sets nil) (nil application-judgement "finite_set[T]" sep_sets nil) (deg const-decl "nat" graph_deg nil)) nil)) (sep_num_min 0 (sep_num_min-1 nil 3251040627 ("" (skosimp*) (("" (expand "separable?") (("" (flatten) (("" (lemma "min_sep_set_card") (("" (inst -1 "G!1" "_" "s!1" "t!1") (("" (copy -1) (("" (inst -1 "adj_verts(G!1,s!1)") (("" (inst -2 "adj_verts(G!1,t!1)") (("" (split -1) (("1" (split -2) (("1" (expand "sep_num") (("1" (lemma "adj_verts_lem") (("1" (inst?) (("1" (replace -1) (("1" (hide -1) (("1" (lemma "adj_verts_lem") (("1" (inst?) (("1" (replace -1) (("1" (hide -1) (("1" (expand "min") (("1" (lift-if) (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 4) (("2" (expand "separates") (("2" (expand "adj_verts") (("2" (prop) (("1" (skosimp*) (("1" (expand "incident_edges") (("1" (flatten) (("1" (expand "edge?") (("1" (lemma "edge_has_2_verts") (("1" (inst?) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "walk_from?") (("2" (flatten) (("2" (expand "walk?") (("2" (expand "del_verts") (("2" (expand "edge?") (("2" (flatten) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.63 Sekunden (vorverarbeitet) ¤ |
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 |
