|
(graph_piece_path
(union_edge_disj_TCC1 0
(union_edge_disj_TCC1-1 nil 3251113235 ("" (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 graph_piece_path 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)
(/= const-decl "boolean" notequal nil))
nil))
(union_edge_disj 0
(union_edge_disj-1 nil 3251113235
("" (skosimp*)
(("" (apply-extensionality 2 :hide? t)
(("1" (apply-extensionality 1 :hide? t)
(("1" (iff 1)
(("1" (prop)
(("1" (replace -2)
(("1" (hide -2)
(("1" (replace -2)
(("1" (hide -2)
(("1" (expand "union")
(("1" (expand "union")
(("1" (expand "member")
(("1" (expand "subgraph")
(("1" (assert)
(("1"
(expand "difference")
(("1"
(expand "member")
(("1"
(skosimp*)
(("1"
(typepred "G!1")
(("1"
(inst?)
(("1"
(assert)
(("1"
(inst-cp -1 "x!2")
(("1"
(inst -1 "x!3")
(("1"
(assert)
(("1"
(case-replace
"x!2 = x!3")
(("1"
(lemma
"edge_has_2_verts")
(("1"
(inst
-1
"x!1"
"x!2"
"x!3")
(("1"
(assert)
(("1"
(inst
3
"x!3"
"x!2")
(("1"
(ground)
(("1"
(expand
"edg")
(("1"
(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)
("2" (expand "union")
(("2" (expand "union")
(("2" (expand "member")
(("2" (prop)
(("1" (replace -2)
(("1" (expand "subgraph")
(("1" (assert) nil nil)) nil))
nil)
("2" (replace -3)
(("2" (expand "subgraph")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (replace -1)
(("2" (hide -1)
(("2" (replace -1)
(("2" (hide -1)
(("2" (apply-extensionality 1 :hide? t)
(("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil graph_piece_path 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)
(union const-decl "graph[T]" graph_ops nil)
(graph type-eq-decl nil graphs nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(finite_difference application-judgement "finite_set" finite_sets
nil)
(member const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(edg const-decl "doubleton[T]" graphs nil)
(nil application-judgement "finite_set[T]" graph_piece_path nil)
(edge_has_2_verts formula-decl nil graphs nil)
(difference const-decl "set" sets nil)
(subgraph const-decl "Subgraph(G)" subgraphs nil)
(union const-decl "set" sets nil)
(Subgraph type-eq-decl nil subgraphs nil)
(subgraph? const-decl "bool" subgraphs nil)
(finite_union application-judgement "finite_set" finite_sets nil))
nil))
(piece_implies_path 0
(piece_implies_path-1 nil 3251113235
("" (skosimp*)
(("" (case "empty?(G!1)")
(("1" (expand "piece_connected?") (("1" (flatten) nil nil)) nil)
("2" (expand "empty?")
(("2" (expand "empty?")
(("2" (expand "member")
(("2" (skosimp*)
(("2"
(name "V"
"{u: T | (EXISTS (w: Walk(G!1)): w(0) = u AND w(length(w)-1) = x!1) OR u = x!1}")
(("2" (ground)
(("2" (expand "finseq_appl")
(("2" (name "H" "subgraph(G!1,V)")
(("2" (name "W" "difference(vert(G!1),V)")
(("2" (name "K" "subgraph(G!1,W)")
(("2"
(case "(EXISTS (u,w:T): vert(H)(u) AND vert(K)(w) AND u /= w AND edges(G!1)(edg[T](u,w)))")
(("1" (skosimp*)
(("1"
(hide 1)
(("1"
(expand "piece_connected?")
(("1"
(flatten)
(("1"
(inst -9 "K" "H")
(("1"
(assert)
(("1"
(split -9)
(("1"
(expand "intersection")
(("1"
(expand "empty?")
(("1"
(skosimp*)
(("1"
(expand "member")
(("1"
(flatten)
(("1"
(hide
-3
-4
-5
-9
-10
1)
(("1"
(replace
-3
*
rl)
(("1"
(hide -3)
(("1"
(replace
-3
*
rl)
(("1"
(hide -3)
(("1"
(replace
-3
*
rl)
(("1"
(hide
-3)
(("1"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -8 1 2)
(("2"
(case "V(u!1)")
(("1"
(case "V(w!1)")
(("1"
(hide -5 -8 -9)
(("1"
(expand
"difference")
(("1"
(replace -6 * rl)
(("1"
(expand
"subgraph")
(("1"
(replace
-5
*
rl)
(("1"
(assert)
(("1"
(hide
-5
-6)
(("1"
(expand
"member")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -2 -6 -7)
(("2"
(replace -4 * rl)
(("2"
(hide -4)
(("2"
(expand
"subgraph")
(("2"
(flatten)
(("2"
(replace
-5
*
rl)
(("2"
(hide -5)
(("2"
(beta)
(("2"
(flatten)
(("2"
(split
-1)
(("1"
(skosimp*)
(("1"
(case-replace
"u!1 = w!1")
(("1"
(inst
1
"w!2")
(("1"
(assert)
nil
nil))
nil)
("2"
(inst
+
"gen_seq1(G!1,w!1) o w!2")
(("1"
(expand
"o ")
(("1"
(expand
"gen_seq1")
(("1"
(propax)
nil
nil))
nil))
nil)
("2"
(lemma
"walk_concat_edge")
(("2"
(inst
-
"G!1"
"w!1"
"u!1"
"w!1"
"x!1"
"gen_seq1[T](G!1, w!1)"
"w!2")
(("2"
(expand
"walk_from?")
(("2"
(assert)
(("2"
(split
+)
(("1"
(assert)
(("1"
(hide
-1)
(("1"
(expand
"o ")
(("1"
(expand
"gen_seq1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(hide
1)
(("2"
(expand
"edg")
(("2"
(expand
"edge?")
(("2"
(rewrite
"dbl_comm")
(("2"
(assert)
(("2"
(rewrite
"gen_seq1_is_walk")
(("2"
(expand
"gen_seq1")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace
-1)
(("2"
(hide
-1)
(("2"
(inst
+
"gen_seq2(G!1,w!1,x!1)")
(("1"
(expand
"gen_seq2")
(("1"
(propax)
nil
nil))
nil)
("2"
(lemma
"edge_to_walk")
(("2"
(inst?)
(("2"
(assert)
(("2"
(expand
"edg")
(("2"
(rewrite
"dbl_comm")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -2 -3 -4 -5 -7)
(("2"
(expand "subgraph")
(("2"
(replace -2 * rl)
(("2"
(hide -2)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(expand "empty?")
(("3"
(expand "empty?")
(("3"
(inst -1 "w!1")
(("3"
(expand "member")
(("3"
(propax)
nil
nil))
nil))
nil))
nil))
nil)
("4"
(expand "empty?")
(("4"
(expand "empty?")
(("4"
(inst -1 "u!1")
(("4"
(expand "member")
(("4"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2"
(lemma "union_edge_disj")
(("2"
(inst
-1
"G!1"
"subgraph(G!1, V)"
"subgraph(G!1, W)"
"V")
(("2"
(assert)
(("2"
(replace -2)
(("2"
(replace -4)
(("2"
(split -1)
(("1"
(hide 1)
(("1"
(expand
"piece_connected?")
(("1"
(prop)
(("1"
(inst -7 "H" "K")
(("1"
(assert)
(("1"
(split -7)
(("1"
(hide -1 -6 2)
(("1"
(replace
-1
*
rl)
(("1"
(hide -1)
(("1"
(replace
-1
*
rl)
(("1"
(hide
-1)
(("1"
(replace
-1
*
rl)
(("1"
(hide
-1)
(("1"
(replace
-1
*
rl)
(("1"
(hide
-1)
(("1"
(grind)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace
-5
*
rl)
(("2"
(expand
"empty?")
(("2"
(hide
-2
-3
-4
-5)
(("2"
(replace
-2
*
rl)
(("2"
(hide
-2)
(("2"
(expand
"subgraph")
(("2"
(expand
"empty?")
(("2"
(inst
-1
"x!1")
(("2"
(expand
"member")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(hide -7)
(("3"
(reveal 2)
(("3"
(expand
"path_connected?")
(("3"
(skosimp*)
(("3"
(case
"vert(K)(x!2) OR vert(K)(y!1)")
(("1"
(hide
-3
-4
-5
-6
-7
1
2
3)
(("1"
(grind)
nil
nil))
nil)
("2"
(case
"vert(H)(x!2) AND vert(H)(y!1)")
(("1"
(flatten)
(("1"
(hide
-3
-4
-5
-6
1
2)
(("1"
(replace
-4
*
rl)
(("1"
(hide
-4)
(("1"
(replace
-3
*
rl)
(("1"
(hide
-3)
(("1"
(expand
"subgraph")
(("1"
(case-replace
"x!2 = x!1")
(("1"
(case-replace
"y!1 = x!1")
(("1"
(inst
1
"gen_seq1(G!1,x!1)")
(("1"
(expand
"gen_seq1")
(("1"
(propax)
nil
nil))
nil)
("2"
(lemma
"gen_seq1_is_walk")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(skosimp*)
(("2"
(assert)
(("2"
(inst
+
"rev(w!1)")
(("1"
(expand
"rev")
(("1"
(propax)
nil
nil))
nil)
("2"
(rewrite
"walk?_rev")
(("2"
(expand
"rev")
(("2"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(ground)
(("1"
(skosimp*)
(("1"
(case
"y!1 = x!2")
(("1"
(replace
-1)
(("1"
(hide
-1)
(("1"
(inst
+
"gen_seq1(G!1,x!2)")
(("1"
(expand
"gen_seq1")
(("1"
(propax)
nil
nil))
nil)
("2"
(rewrite
"gen_seq1_is_walk")
nil
nil))
nil))
nil))
nil)
("2"
(lemma
"walk_merge")
(("2"
(inst
-1
"G!1"
"w!1"
"w!2"
"x!2"
"y!1"
"x!1")
(("2"
(expand
"walk_from?")
(("2"
(assert)
(("2"
(skosimp*)
(("2"
(inst
+
"p!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace
-1)
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
3
4)
(("2"
(case
"disjoint?(vert(H),vert(K))")
(("1"
(hide
-2
-3
-4
-5
-6)
(("1"
(expand
"disjoint?")
(("1"
(expand
"intersection")
(("1"
(expand
"empty?")
(("1"
(expand
"member")
(("1"
(inst-cp
-1
"x!2")
(("1"
(inst
-1
"y!1")
(("1"
(case
"vert(G!1) = union(vert(H),vert(K))")
(("1"
(typepred
"y!1")
(("1"
(typepred
"x!2")
(("1"
(expand
"union")
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.94 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.
|
