| products/sources/formale sprachen/PVS/graphs/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: complem.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(complem
(powerset_finite 0 (powerset_finite-2 "from-prelude" 3349377711 ("" (use "finite_sets_of_sets[T].powerset_natfun_inj") (("" (skosimp) (("" (expand "is_finite") (("" (inst 1 "exp2(card(A!1))" "powerset_natfun(A!1)") (("" (expand "injective?") (("" (grind) nil nil)) nil)) nil)) nil)) nil)) 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) (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) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (posnat nonempty-type-eq-decl nil integers nil) (exp2 def-decl "posnat" exp2 nil) (set type-eq-decl nil sets nil) (finite_set type-eq-decl nil finite_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (powerset const-decl "setofsets" sets nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (below type-eq-decl nil naturalnumbers nil) (powerset_natfun const-decl "below(exp2(card(A)))" finite_sets_of_sets nil) (injective? const-decl "bool" functions nil) (is_finite const-decl "bool" finite_sets nil) (T formal-type-decl nil complem nil) (powerset_natfun_inj formula-decl nil finite_sets_of_sets nil)) shostak) (powerset_finite-1 nil 3349377681 ("" (use "powerset_natfun_inj") (("" (skosimp) (("" (expand "is_finite") (("" (inst 1 "exp2(card(A!1))" "powerset_natfun(A!1)") (("" (expand "injective?") (("" (grind) nil)))))))))) nil) nil nil)) (all_edges_power 0 (all_edges_power-1 nil 3349381067 ("" (grind) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil complem 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) (doubleton type-eq-decl nil doubletons nil) (dbl const-decl "set[T]" doubletons nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (nil application-judgement "finite_set[T]" graph_ops nil) (injective? const-decl "bool" functions 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 "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (/= const-decl "boolean" notequal nil) (all_edges const-decl "set[doubleton[T]]" complem nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (powerset const-decl "setofsets" sets nil) (restrict const-decl "R" restrict nil)) shostak)) (all_edges_finite 0 (all_edges_finite-2 "revis all_edge" 3349528703 ("" (skosimp*) (("" (use all_edges_power) (("" (lemma "finite_sets[set[T]].finite_subset") (("" (inst -1 "powerset(V!1)" "all_edges(V!1)") (("" (bddsimp) (("1" (hide -2) (("1" (expand "extend") (("1" (ground) (("1" (expand "is_finite") (("1" (skosimp*) (("1" (inst + "N!1" "f!1") (("1" (expand "injective?") (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide 2) (("2" (expand "restrict") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((all_edges_power formula-decl nil complem 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 complem nil) (powerset_finite application-judgement "finite_set[set[T]]" finite_sets_of_sets nil) (nonempty_powerset application-judgement "(nonempty?[set[T]])" sets_lemmas nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (powerset const-decl "setofsets" 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) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (all_edges const-decl "set[doubleton[T]]" complem nil) (finite_restrict application-judgement "finite_set[S]" restrict_set_props nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (restrict const-decl "R" restrict nil) (NOT const-decl "[bool -> bool]" booleans nil) (nil application-judgement "finite_set[T]" graph_ops nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (injective? const-decl "bool" functions 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) (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) (V!1 skolem-const-decl "finite_set[T]" complem nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (finite_subset formula-decl nil finite_sets nil)) shostak) (all_edges_finite-1 nil 3349381260 ("" (skosimp*) (("" (use all_edges_power) (("" (lemma "finite_sets[set[T]].finite_subset") (("" (inst -1 "powerset(V!1)" "all_edges(V!1)") (("" (bddsimp) (("1" (hide -2) (("1" (expand "extend") (("1" (grind) (("1" (reveal -1) (("1" (inst -1 "dbl[T](x!3, y!3)" "dbl[T](x!4, y!4)") (("1" (assert) nil nil)) nil)) nil) ("2" (reveal -1) (("2" (inst -1 "dbl[T](x!3, y!3)" "dbl[T](x!4, y!4)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (hide 2) (("2" (expand "restrict") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((dbl const-decl "set[T]" doubletons nil) (doubleton type-eq-decl nil doubletons nil)) shostak)) (completion_TCC1 0 (completion_TCC1-1 nil 3349204238 ("" (use "all_edges_finite") (("" (skosimp*) (("" (inst?) nil nil)) nil)) nil) ((T formal-type-decl nil complem 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) (all_edges_finite formula-decl nil complem nil)) nil)) (completion_TCC2 0 (completion_TCC2-1 nil 3349381053 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil complem 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) (nil application-judgement "finite_set[T]" graph_ops nil) (/= const-decl "boolean" notequal nil) (all_edges const-decl "set[doubleton[T]]" complem nil)) nil)) (completion_is_subgraph 0 (completion_is_subgraph-2 "works" 3349205027 ("" (grind) (("1" (lemma "graphs[T].edges_vert_in") (("1" (grind) nil nil)) nil) ("2" (lemma "graphs[T].edges_vert_in") (("2" (grind) nil nil)) nil) ("3" (lemma "graphs[T].edges_vert_in") (("3" (grind) nil nil)) nil) ("4" (lemma "graphs[T].edges_vert_in") (("4" (grind) nil nil)) nil) ("5" (lemma "graphs[T].edges_vert_in") (("5" (grind) nil nil)) nil) ("6" (lemma "graphs[T].edges_vert_in") (("6" (grind) nil nil)) nil)) nil) ((edges_vert_in formula-decl nil graphs nil) (nil application-judgement "finite_set[T]" graph_ops nil) (G!1 skolem-const-decl "graph[T]" complem nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil complem 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) (subgraph? const-decl "bool" subgraphs nil) (all_edges const-decl "set[doubleton[T]]" complem nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (completion const-decl "graph[T]" complem nil) (/= const-decl "boolean" notequal nil)) shostak)) (complement_TCC1 0 (complement_TCC1-1 nil 3349204238 ("" (skosimp*) (("" (case "subset?(difference[doubleton[T]](all_edges(vert(G!1)), edges(G!1)),all_edg (("1" (lemma "finite_sets[doubleton[T]].finite_subset") (("1" (inst -1 "all_edges(vert(G!1))" "difference[doubleton[T]](all_edges(vert(G!1)), edges(G!1))") (("1" (bddsimp) nil nil) ("2" (lemma "all_edges_finite") (("2" (inst -1 "vert(G!1)") nil nil)) nil)) nil)) nil) ("2" (lemma "sets_lemmas[doubleton[T]].difference_subset") (("2" (inst -1 "all_edges(vert(G!1))" "edges(G!1)") 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) (all_edges const-decl "set[doubleton[T]]" complem nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (difference const-decl "set" sets nil) (subset? const-decl "bool" 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 complem nil) (G!1 skolem-const-decl "graph[T]" complem nil) (all_edges_finite formula-decl nil complem nil) (finite_subset formula-decl nil finite_sets nil) (difference_subset formula-decl nil sets_lemmas nil)) nil)) (complement_TCC2 0 (complement_TCC2-1 nil 3349381053 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil complem 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) (nil application-judgement "finite_set[T]" graph_ops nil) (/= const-decl "boolean" notequal nil) (all_edges const-decl "set[doubleton[T]]" complem nil) (member const-decl "bool" sets nil) (difference const-decl "set" sets nil)) nil)) (comp_comp_lem 0 (comp_comp_lem-1 nil 3349285188 ("" (skosimp*) (("" (expand "complement") (("" (apply-extensionality 1 :hide? t) (("" (apply-extensionality 1 :hide? t) (("" (expand "difference") (("" (expand "member") (("" (iff 1) (("" (bddsimp) (("" (expand "all_edges") (("" (typepred "G!1") (("" (typepred "x!1") (("" (skosimp*) (("" (inst 2 "x!2" "y!1") (("" (bddsimp) (("1" (inst -2 "x!1") (("1" (bddsimp) (("1" (grind) nil nil)) nil)) nil) ("2" (inst -2 "x!1") (("2" (bddsimp) (("2" (grind) nil nil)) nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((complement const-decl "graph[T]" complem nil) (member const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (nil application-judgement "finite_set[T]" graph_ops nil) (pregraph type-eq-decl nil graphs nil) (IMPLIES const-decl "[bool, bool -> bool]" booleans nil) (graph type-eq-decl nil graphs nil) (difference const-decl "set" sets nil) (all_edges const-decl "set[doubleton[T]]" complem nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" 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 complem nil)) shostak)) (isol_TCC1 0 (isol_TCC1-1 nil 3349204238 ("" (subtype-tcc) nil nil) ((emptyset const-decl "set" sets nil)) nil)) (path_or_not_path 0 (path_or_not_path-3 "Do not use vert_in" 3358451058 ("" (skosimp*) (("" (expand "path_connected?") (("" (bddsimp) (("1" (expand "empty?") (("1" (expand "empty?") (("1" (hide 2) (("1" (grind) nil nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (case "x!1=y!1") (("1" (inst 2 "gen_seq1(G!1,x!1)") (("1" (hide 3) (("1" (install-rewrites "walks") (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "walks[T].gen_seq1_is_walk") (("2" (inst -1 "G!1" "x!1") (("2" (typepred "x!1") (("2" (bddsimp) nil nil)) nil)) nil)) nil)) nil) ("2" (case "x!2=y!2") (("1" (inst 4 "gen_seq1(complement(G!1),x!2)") (("1" (install-rewrites "walks") (("1" (assert) nil nil)) nil) ("2" (lemma "walks[T].gen_seq1_is_walk") (("2" (inst -1 "complement(G!1)" "x!2") (("2" (typepred "x!2") (("2" (bddsimp) nil nil)) nil)) nil)) nil)) nil) ("2" (case "edge?(G!1)(x!2,y!2)") (("1" (case "x!1=x!2") (("1" (case "y!1=y!2") (("1" (inst 4 "gen_seq2(G!1,x!1,y!1)") (("1" (hide 5) (("1" (install-rewrites "walks") (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "walks[T].edge_to_walk") (("2" (inst -1 "G!1" "x!1" "y!1") (("2" (bddsimp) (("1" (expand "edge?") (("1" (bddsimp) (("1" (assert) (("1" (replace -1 1 lr) (("1" (replace -2 1 lr) (("1" (assert) (("1" (hide-all-but (-4 1)) (("1" (install-rewrites "walks") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (case "edge?(G!1)(x!1, y!1)") (("1" (inst 5 "gen_seq2(G!1,x!1,y!1)") (("1" (hide -3 6) (("1" (install-rewrites "walks") (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "walks[T].edge_to_walk") (("2" (inst? -1) (("2" (assert) (("2" (expand "edge?") (("2" (hide-all-but (-1 1)) (("2" (assert) (("2" (install-rewrites "walks") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "edge?(G!1)(y!2,y!1)") (("1" (inst 6 "add1(gen_seq2(G!1,x!2,y!2),y!1)") (("1" (hide 7) (("1" (install-rewrites "walks") (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "walks[T].walk?_add1") (("2" (inst? -1) (("2" (bddsimp) (("1" (hide (2 8)) (("1" (install-rewrites "walks") (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "graphs[T].edges_vert_in") (("2" (inst -1 "G!1" "dbl[T](y!2,y!1)" "y!2" "y!1") (("1" (expand "edge?") (("1" (assert) nil nil)) nil) ("2" (inst 1 "y!2" "y!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (lemma "walks[T].edge_to_walk") (("3" (inst -1 "G!1" "x!2" "y!2") (("3" (expand "edge?") (("3" (assert) (("3" (hide-all-but (-3 1)) (("3" (install-rewrites "walks") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (lemma "graphs[T].edges_vert_in") (("3" (inst -1 "G!1" "dbl[T](y!2,y!1)" "y!2" "y!1") (("1" (expand "edge?") (("1" (assert) nil nil)) nil) ("2" (inst 1 "y!2" "y!1") (("2" (assert) nil nil)) nil)) nil)) nil) ("4" (lemma "graphs[T].edges_vert_in") (("4" (inst -1 "G!1" "dbl[T](x!2,y!2)" "x!2" "y!2") (("1" (bddsimp) (("1" (expand "edge?") (("1" (assert) nil nil)) nil)) nil) ("2" (inst 1 "x!2" "y!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (inst 8 "add1(gen_seq2(complement(G!1),x!2,y!1),y!2)") (("1" (hide 7) (("1" (install-rewrites "walks") (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "walks[T].walk?_add1") (("2" (hide 8) (("2" (inst -1 "complement(G!1)" "gen_seq2[T](complement(G!1), x!2, y!1)" "y!2") (("2" (assert) (("2" (install-rewrites "walks") (("2" (hide 2) (("2" (bddsimp) (("1" (assert) (("1" (bddsimp) (("1" (assert) (("1" (lemma "graphs[T].edge?_comm") (("1" (inst -1 "G!1" "y!2" "y!1") (("1" (expand "edge?") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (inst 1 "y!1" "y!2") (("2" (assert) (("2" (lemma "graphs[T].edges_vert_in") (("2" (inst -1 "G!1" "dbl[T](x!2,y!2)" "x!2" "y!2") (("2" (bddsimp) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "walks[T].edge_to_walk") (("2" (inst -1 "complement(G!1)" "x!2" "y!1") (("2" (bddsimp) (("1" (hide 2) (("1" (replace -1 * lr) (("1" (hide (-2 2)) (("1" (install-rewrites "walks") (("1" (assert) (("1" (bddsimp) (("1" (inst 1 "x!2" "y!1") (("1" (bddsimp) (("1" (typepred "y!1") (("1" (propax) nil nil)) nil) ("2" (typepred "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "walks[T].edge_to_walk") (("2" (inst -1 "complement(G!1)" "x!2" "y!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (typepred "y!1") (("3" (hide-all-but (-1 1)) (("3" (install-rewrites "walks") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "edge?(G!1)(x!1,y!1)") (("1" (inst 5 "gen_seq2(G!1,x!1,y!1)") (("1" (hide 6) (("1" (install-rewrites "walks") (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "walks[T].edge_to_walk") (("2" (inst? -1) (("2" (assert) (("2" (hide-all-but (-1 1)) (("2" (install-rewrites "walks") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case-replace "edge?(G!1)(x!1,x!2)") (("1" (case-replace "edge?(G!1)(y!2,y!1)") (("1" (case "EXISTS (w: walks[T].prewalk): seq(w)(0) = x!1 AND seq(w)(length(w) - 1) = (("1" (skosimp*) (("1" (hide 7) (("1" (install-rewrites "walks") (("1" (inst 6 "w!1") (("1" (assert) nil nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 7 8) (("2" (install-rewrites "walks") (("2" (inst 1 "walks[T].list2prewalk((:x!1,x!2,y!2,y!1:))") (("1" (install-rewrites "walks") (("1" (assert) (("1" (bddsimp) (("1" (skosimp*) (("1" (bddsimp) (("1" (case "n!1=0") (("1" (replace -1 -3 lr) (("1" (expand "nth") (("1" (propax) nil nil)) nil)) nil) ("2" (case "n!1=1") (("1" (replace -1 -3 lr) (("1" (expand "nth") (("1" (expand "nth") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (case "n!1=2") (("1" (replace -1 -3 lr) (("1" (expand "nth") (("1" (expand "nth") (("1" (expand "nth") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil) ("2" (case "n!1=0") (("1" (expand "nth") (("1" (assert) nil nil)) nil) ("2" (case "n!1=1") (("1" (expand "nth") (("1" (replace -1 2 lr) (("1" (assert) nil nil)) nil)) nil) ("2" (case "n!1=2") (("1" (replace -1 3 lr) (("1" (expand "nth") (("1" (expand "nth") (("1" (expand "nth") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (typepred "i!1") (("2" (lemma "graphs[T].edges_vert_in") (("2" (lemma "graphs[T].edges_vert_in") (("2" (lemma "graphs[T].edges_vert_in") (("2" (inst -1 "G!1" "dbl[T](y!2,y!1)" "y!2" "y!1") (("2" (inst -2 "G!1" "dbl[T](x!1,x!2)" "x!1" "x!2") (("2" (inst -3 "G!1" "dbl[T](x!2,y!2)" "x!2" "y!2") (("2" (bddsimp) (("2" (case "i!1=0") (("1" (expand "nth") (("1" (replace -1 1 lr) (("1" (propax) nil nil)) nil)) nil) ("2" (case "i!1=1") (("1" (replace -1 2 lr) (("1" (expand "nth") (("1" (expand "nth") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (case "i!1=2") (("1" (replace -1 3 lr) (("1" (expand "nth") (("1" (expand "nth") (("1" (expand "nth") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (case "i!1=3") (("1" (replace -1 4 lr) (("1" (expand "nth") (("1" (expand "nth") (("1" (expand "nth") (("1" (expand "nth") (("1" (propax) 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) ("2" (hide (-1 -2 -3 2 7 8)) (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "edge?(G!1)(x!2,y!1)") (("1" (hide 8) (("1" (case "EXISTS (w: walks[T].prewalk): seq(w)(0) = x!1 AND seq(w)(length(w) - 1) = (("1" (skosimp*) (("1" (inst 7 "w!1") (("1" (bddsimp) nil nil)) nil)) nil) ("2" (hide 8) (("2" (inst 1 "walks[T].list2prewalk((:x!1,x!2,y!1:))") (("1" (install-rewrites "walks") (("1" (assert) (("1" (bddsimp) (("1" (skosimp*) (("1" (bddsimp) (("1" (case "n!1=0") (("1" (replace -1 -3 lr) (("1" (expand "nth") (("1" (propax) nil nil)) nil)) nil) ("2" (case "n!1=1") (("1" (replace -1 -3 lr) (("1" (expand "nth") (("1" (expand "nth") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (case "n!1=0") (("1" (expand "nth") (("1" (assert) nil nil)) nil) ("2" (case "n!1=1") (("1" (expand "nth") (("1" (replace -1 2 lr) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (bddsimp) (("1" (case "n!1=0") (("1" (expand "nth") (("1" (assert) nil nil)) nil) ("2" (case "n!1=1") (("1" (expand "nth") (("1" (replace -1 -3 lr) (("1" (assert) nil nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil) ("2" (case "n!1=0") (("1" (expand "nth") (("1" (assert) nil nil)) nil) ("2" (case "n!1=1") (("1" (replace -1 2 lr) (("1" (expand "nth") (("1" (expand "nth") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (typepred "i!1") (("3" (case "i!1=0") (("1" (expand "nth") (("1" (replace -1 1 lr) (("1" (typepred "x!1") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (case "i!1=1") (("1" (replace -1 2 lr) (("1" (expand "nth") (("1" (expand "nth") (("1" (typepred "x!2") (("1" (expand "complement") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "i!1=2") (("1" (replace -1 3 lr) (("1" (expand "nth") (("1" (expand "nth") (("1" (expand "nth") (("1" --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.42 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 |
