|
(meng_scaff_defs
(H_TCC1 0
(H_TCC1-1 nil 3507100603
("" (skosimp*)
(("" (expand "subgraph?")
(("" (split 1)
(("1" (expand "subset?")
(("1" (skosimp*)
(("1" (expand "path_comp")
(("1" (expand "subgraph")
(("1" (expand "del_vert")
(("1" (expand "member")
(("1" (flatten)
(("1" (hide -2)
(("1" (expand "remove")
(("1" (expand "member")
(("1" (flatten)
(("1" (propax) nil)))))))))))))))))))))))
("2" (expand "subset?")
(("2" (skosimp*)
(("2" (expand "member")
(("2" (expand "path_comp")
(("2" (expand "subgraph")
(("2" (flatten)
(("2" (hide -2)
(("2" (expand "del_vert")
(("2" (flatten)
(("2" (propax) nil))))))))))))))))))))))))
nil)
((subgraph? const-decl "bool" subgraphs nil)
(subset? const-decl "bool" sets nil)
(path_comp const-decl "Subgraph(G)" meng_scaff_defs nil)
(del_vert const-decl "graph[T]" graph_ops nil)
(remove const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(subgraph const-decl "Subgraph(G)" subgraphs nil))
nil))
(incident_TCC1 0
(incident_TCC1-1 nil 3507100603
("" (skosimp*)
(("" (lemma "finite_subset[Dbl]")
(("" (inst?)
(("" (inst -1 "edges(G!1)")
(("" (assert)
(("" (hide 2)
(("" (expand "subset?")
(("" (skosimp*)
(("" (expand "member")
(("" (skosimp*) 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 meng_scaff_defs nil)
(finite_subset formula-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_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)
(H const-decl "Subgraph(G)" meng_scaff_defs nil)
(Subgraph type-eq-decl nil subgraphs nil)
(subgraph? const-decl "bool" subgraphs 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))
nil))
(meng_TCC1 0
(meng_TCC1-1 nil 3507100603
("" (skosimp*) (("" (inst?) (("" (assert) nil)))) nil)
((T formal-type-decl nil meng_scaff_defs nil)
(boolean nonempty-type-decl nil booleans 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))
nil))
(meng_TCC2 0
(meng_TCC2-1 nil 3507100603
("" (skosimp*) (("" (inst?) (("" (assert) nil)))) nil)
((T formal-type-decl nil meng_scaff_defs nil)
(boolean nonempty-type-decl nil booleans 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))
nil))
(meng_TCC3 0
(meng_TCC3-1 nil 3507100603
("" (skosimp*)
(("" (expand "add")
(("" (flatten)
(("" (expand "member")
(("" (flatten)
(("" (split -1)
(("1" (replace -1 * rl)
(("1" (hide -1)
(("1" (expand "dbl") (("1" (ground) nil)))))))
("2" (replace -1 * rl)
(("2" (hide -1)
(("2" (expand "dbl") (("2" (ground) nil)))))))
("3" (expand "union")
(("3" (expand "member")
(("3" (split -1)
(("1" (typepred "H(G!1, x!1, w1!1, w2!1)")
(("1" (inst?)
(("1" (assert)
(("1" (inst?) (("1" (assert) nil)))))))))
("2" (expand "incident")
(("2" (skosimp*)
(("2" (replace -2)
(("2" (hide -2)
(("2" (expand "dbl")
(("2"
(split -)
(("1"
(replace -1)
(("1" (propax) nil)))
("2"
(replace -1)
(("2" (propax) nil)))))))))))))))
("3" (expand "incident")
(("3" (skosimp*)
(("3" (replace -2)
(("3" (hide -2)
(("3" (expand "dbl" -3)
(("3"
(split -3)
(("1"
(replace -1)
(("1" (propax) nil)))
("2"
(assert)
nil))))))))))))))))))))))))))))))
nil)
((add const-decl "(nonempty?)" sets nil)
(member const-decl "bool" sets nil)
(dbl const-decl "set[T]" doubletons nil)
(nil application-judgement "finite_set[T]" meng_scaff_defs nil)
(incident const-decl "finite_set[doubleton[T]]" meng_scaff_defs
nil)
(H const-decl "Subgraph(G)" meng_scaff_defs nil)
(Subgraph type-eq-decl nil subgraphs nil)
(subgraph? const-decl "bool" subgraphs 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)
(= 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 meng_scaff_defs nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(union const-decl "set" sets nil))
nil))
(vert_H_s 0
(vert_H_s-1 nil 3507100603
("" (skosimp*)
(("" (assert)
(("" (expand "H")
(("" (expand "path_comp")
(("" (expand "subgraph")
(("" (expand "del_vert")
(("" (expand "remove")
(("" (expand "member")
(("" (expand "path_verts")
(("" (expand "walk_from?")
(("" (inst + "gen_seq1(G!1,s!1)")
(("" (expand "gen_seq1")
(("" (expand "walk?")
(("" (expand "verts_in?")
((""
(propax)
nil))))))))))))))))))))))))))))
nil)
((path_comp const-decl "Subgraph(G)" meng_scaff_defs nil)
(del_vert const-decl "graph[T]" graph_ops nil)
(member const-decl "bool" sets nil)
(walk_from? const-decl "bool" walks nil)
(walk? const-decl "bool" walks nil)
(gen_seq1 const-decl "Seq(G)" walks nil)
(Seq type-eq-decl nil walks nil)
(verts_in? const-decl "bool" walks 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)
(prewalk type-eq-decl nil walks nil)
(> const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(finseq type-eq-decl nil finite_sequences nil)
(T formal-type-decl nil meng_scaff_defs nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(path_verts const-decl "set[T]" paths nil)
(remove const-decl "set" sets nil)
(subgraph const-decl "Subgraph(G)" subgraphs nil)
(H const-decl "Subgraph(G)" meng_scaff_defs nil))
nil))
(path_H_W 0
(path_H_W-1 nil 3507100603
("" (skosimp*)
(("" (expand "path?")
(("" (flatten)
(("" (hide -2)
(("" (expand "walk?")
(("" (flatten)
(("" (hide -2)
(("" (expand "verts_in?")
(("" (expand "H")
(("" (expand "path_comp")
(("" (expand "subgraph")
(("" (expand "del_vert")
(("" (expand "remove")
(("" (expand "member")
((""
(expand "verts_of")
((""
(expand "finseq_appl")
((""
(split 1)
(("1"
(skosimp*)
(("1"
(inst?)
(("1" (assert) nil)))))
("2"
(assert)
(("2"
(skosimp*)
(("2"
(inst?)
(("2"
(assert)
nil))))))))))))))))))))))))))))))))))))))))
nil)
((path? const-decl "bool" paths nil)
(verts_in? const-decl "bool" walks nil)
(path_comp const-decl "Subgraph(G)" meng_scaff_defs nil)
(del_vert const-decl "graph[T]" graph_ops nil)
(member const-decl "bool" sets nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
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 meng_scaff_defs 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)
(verts_of const-decl "finite_set[T]" walks nil)
(remove const-decl "set" sets nil)
(subgraph const-decl "Subgraph(G)" subgraphs nil)
(H const-decl "Subgraph(G)" meng_scaff_defs nil)
(walk? const-decl "bool" walks nil))
nil))
(path_comp_in 0
(path_comp_in-1 nil 3507100603
("" (skosimp*)
(("" (expand "path?")
(("" (split 1)
(("1" (flatten)
(("1" (typepred "H(G!1, s!1, w1!1, w2!1)")
(("1" (hide -1 -4)
(("1" (lemma "walk?_subgraph")
(("1" (inst?)
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
("2" (flatten) nil nil))
nil))
nil))
nil)
((path? const-decl "bool" paths 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 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)
(prewalk type-eq-decl nil walks nil)
(walk?_subgraph formula-decl nil subgraph_paths 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 meng_scaff_defs 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)
(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)
(Subgraph type-eq-decl nil subgraphs nil)
(H const-decl "Subgraph(G)" meng_scaff_defs nil))
nil))
(walk?_H_TCC1 0
(walk?_H_TCC1-1 nil 3507100603 ("" (subtype-tcc) nil nil)
((T formal-type-decl nil meng_scaff_defs nil)
(verts_in? const-decl "bool" walks nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(/= const-decl "boolean" notequal nil)
(edge? const-decl "bool" graphs nil)
(walk? const-decl "bool" walks nil)
(nil application-judgement "finite_set[T]" meng_scaff_defs nil))
nil))
(walk?_H 0
(walk?_H-1 nil 3507100603
("" (skosimp*)
(("" (expand "H")
(("" (expand "path_comp")
(("" (expand "walk?")
(("" (flatten)
(("" (split +)
(("1" (hide -2)
(("1" (expand "verts_in?")
(("1" (skosimp*)
(("1" (inst?)
(("1" (expand "subgraph")
(("1" (expand "del_vert")
(("1" (expand "remove")
(("1" (expand "member")
(("1"
(assert)
(("1"
(expand "verts_of")
(("1"
(inst?)
(("1"
(expand "finseq_appl")
(("1"
(inst?)
(("1"
(assert)
(("1"
(expand "path_verts")
(("1"
(expand "walk_from?")
(("1"
(inst 1 "p!1^(0,i!1)")
(("1"
(expand*
"^"
min
empty_seq)
(("1"
(expand "walk?")
(("1"
(split +)
(("1"
(expand
"verts_in?")
(("1"
(skosimp*)
(("1"
(reveal -1)
(("1"
(inst?)
(("1"
(assert)
(("1"
(reveal
2
3)
(("1"
(expand
"finseq_appl")
(("1"
(hide
4
5
-2)
(("1"
(inst?)
(("1"
(inst?)
(("1"
(assert)
nil)))))))))))))))))))))
("2"
(expand
"finseq_appl")
(("2"
(skosimp*)
(("2"
(expand
"edge?")
(("2"
(hide
-2
2
3)
(("2"
(reveal
-3)
(("2"
(inst
-
"n!1")
(("2"
(assert)
(("2"
(expand
"finseq_appl")
(("2"
(expand
"edge?")
(("2"
(flatten)
(("2"
(assert)
(("2"
(hide
-1
-3)
(("2"
(reveal
4
5)
(("2"
(expand
"finseq_appl")
(("2"
(inst-cp
+
"n!1")
(("2"
(inst
+
"n!1+1")
(("2"
(inst-cp
+
"n!1")
(("2"
(inst
+
"n!1+1")
(("2"
(expand
"dbl")
(("2"
(ground)
nil)))))))))))))))))))))))))))))))))))))))))))))
("2"
(expand*
"^"
min
empty_seq)
(("2"
(assert)
nil)))))))))))))))))))))))))))))))))))))
("2" (skosimp*)
(("2" (expand "finseq_appl")
(("2" (expand "edge?")
(("2" (inst?)
(("2" (assert)
(("2" (flatten)
(("2" (assert)
(("2" (expand "subgraph")
(("2"
(expand "del_vert")
(("2"
(split +)
(("1"
(expand "verts_of" 2)
(("1"
(inst-cp + "n!1")
(("1"
(inst + "n!1+1")
(("1"
(expand "finseq_appl")
(("1"
(expand "dbl")
(("1"
(ground)
nil)))))))))))
("2"
(expand "verts_of" 3)
(("2"
(inst-cp + "n!1")
(("2"
(inst + "n!1+1")
(("2"
(expand "finseq_appl")
(("2"
(expand "dbl")
(("2"
(ground)
nil)))))))))))
("3"
(skosimp*)
(("3"
(expand "path_verts")
(("3"
(expand "walk_from?")
(("3"
(expand "dbl")
(("3"
(split -1)
(("1"
(inst 1 "p!1^(0,n!1)")
(("1"
(expand*
"^"
min
empty_seq)
(("1"
(assert)
(("1"
(expand "walk?")
(("1"
(split +)
(("1"
(expand
"verts_in?")
(("1"
(skosimp*)
(("1"
(expand
"remove")
(("1"
(expand
"member")
(("1"
(inst?)
(("1"
(assert)
(("1"
(expand
"verts_of")
(("1"
(inst
+
"i!1")
(("1"
(inst
+
"i!1")
(("1"
(expand
"finseq_appl")
(("1"
(ground)
nil)))))))))))))))))))))
("2"
(skosimp*)
(("2"
(expand
"finseq_appl")
(("2"
(expand
"edge?")
(("2"
(assert)
(("2"
(reveal
-1)
(("2"
(inst?)
(("2"
(assert)
(("2"
(flatten)
(("2"
(assert)
(("2"
(expand
"dbl")
(("2"
(expand
"verts_of")
(("2"
(inst-cp
+
"n!2")
(("2"
(inst
+
"n!2+1")
(("2"
(inst-cp
+
"n!2")
(("2"
(inst
+
"n!2+1")
(("2"
(expand
"finseq_appl")
(("2"
(ground)
nil)))))))))))))))))))))))))))))))))))))))))
("2"
(expand*
"^"
min
empty_seq)
(("2" (assert) nil)))))
("2"
(inst 1 "p!1^(0,n!1+1)")
(("1"
(expand*
"^"
min
empty_seq)
(("1"
(assert)
(("1"
(expand "walk?")
(("1"
(split +)
(("1"
(expand
"verts_in?")
(("1"
(skosimp*)
(("1"
(expand
"remove")
(("1"
(expand
"member")
(("1"
(inst?)
(("1"
(assert)
(("1"
(expand
"verts_of")
(("1"
(inst-cp
+
"i!1")
(("1"
(inst
+
"i!1+1")
(("1"
(inst-cp
+
"i!1")
(("1"
(inst
+
"i!1+1")
(("1"
(expand
"finseq_appl")
(("1"
(assert)
nil)))
("2"
(assert)
(("2"
(typepred
"i!1")
(("2"
(expand
"finseq_appl")
(("2"
(assert)
nil)))))))))))
("2"
(expand
"finseq_appl")
(("2"
(assert)
(("2"
(typepred
"i!1")
(("2"
(inst?)
(("2"
(assert)
nil)))))))))))))))))))))))))))
("2"
(skosimp*)
(("2"
(expand
"edge?")
(("2"
(expand
"finseq_appl")
(("2"
(reveal
-1)
(("2"
(inst?)
(("2"
(assert)
(("2"
(flatten)
(("2"
(assert)
(("2"
(expand
"verts_of")
(("2"
(expand
"finseq_appl")
(("2"
(inst-cp
+
"n!2")
(("2"
(inst
+
"n!2+1")
(("2"
(inst-cp
+
"n!2")
(("2"
(inst
+
"n!2+1")
(("2"
(expand
"dbl")
(("2"
(ground)
nil)))))))))))))))))))))))))))))))))))))))
("2"
(expand*
"^"
min
empty_seq)
(("2"
(assert)
nil))))))))))))))))))))))))))))))))))))))))))))))
nil)
((H const-decl "Subgraph(G)" meng_scaff_defs nil)
(walk? const-decl "bool" walks nil)
(verts_in? const-decl "bool" walks 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)
(< const-decl "bool" reals nil)
(below type-eq-decl nil nat_types nil)
(T formal-type-decl nil meng_scaff_defs nil)
(finseq type-eq-decl nil finite_sequences nil)
(> const-decl "bool" reals nil)
(prewalk type-eq-decl nil walks nil)
(below type-eq-decl nil naturalnumbers nil)
(del_vert const-decl "graph[T]" graph_ops nil)
(member const-decl "bool" sets nil)
(verts_of const-decl "finite_set[T]" walks nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(walk_from? const-decl "bool" walks nil)
(min const-decl "{p: real | p <= m AND p <= n}" real_defs nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nat_min application-judgement "{k: nat | k <= i AND k <= j}"
real_defs 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)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(dbl const-decl "set[T]" doubletons nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(edge? const-decl "bool" graphs nil)
(nil application-judgement "finite_set[T]" meng_scaff_defs nil)
(i!1 skolem-const-decl "below(length(p!1))" meng_scaff_defs nil)
(p!1 skolem-const-decl "prewalk[T]" meng_scaff_defs nil)
(^ const-decl "finseq" finite_sequences nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(path_verts const-decl "set[T]" paths nil)
(remove const-decl "set" sets nil)
(subgraph const-decl "Subgraph(G)" subgraphs nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(i!1 skolem-const-decl "below(2 + n!1)" meng_scaff_defs nil)
(n!1 skolem-const-decl "nat" meng_scaff_defs nil)
(path_comp const-decl "Subgraph(G)" meng_scaff_defs nil))
nil))
(vert_meng_sub_TCC1 0
(vert_meng_sub_TCC1-1 nil 3507100603 ("" (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 meng_scaff_defs 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)
(disjoint? const-decl "bool" meng_scaff_defs nil)
(in? const-decl "bool" meng_scaff_defs nil))
nil))
(vert_meng_sub_TCC2 0
(vert_meng_sub_TCC2-1 nil 3507100603 ("" (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 meng_scaff_defs 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)
(disjoint? const-decl "bool" meng_scaff_defs nil)
(in? const-decl "bool" meng_scaff_defs nil))
nil))
(vert_meng_sub_TCC3 0
(vert_meng_sub_TCC3-1 nil 3507100603 ("" (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 meng_scaff_defs 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)
(disjoint? const-decl "bool" meng_scaff_defs nil)
(in? const-decl "bool" meng_scaff_defs nil))
nil))
(vert_meng_sub_TCC4 0
(vert_meng_sub_TCC4-1 nil 3507100603 ("" (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 meng_scaff_defs 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)
(disjoint? const-decl "bool" meng_scaff_defs nil)
(in? const-decl "bool" meng_scaff_defs nil))
nil))
(vert_meng_sub 0
(vert_meng_sub-1 nil 3507100603
("" (skosimp*)
(("" (expand "subset?")
(("" (expand "member")
(("" (skosimp*)
(("" (expand "meng")
(("" (expand "add")
(("" (expand "member")
(("" (assert)
(("" (expand "H")
(("" (expand "path_comp")
(("" (expand "subgraph")
(("" (expand "del_vert")
(("" (expand "remove")
(("" (expand "member")
((""
(expand "in?")
((""
(flatten)
((""
(expand "disjoint?")
((""
(flatten)
((""
(assert)
nil))))))))))))))))))))))))))))))))))))
nil)
((subset? const-decl "bool" sets nil)
(add const-decl "(nonempty?)" sets nil)
(path_comp const-decl "Subgraph(G)" meng_scaff_defs nil)
(del_vert const-decl "graph[T]" graph_ops nil)
(disjoint? const-decl "bool" meng_scaff_defs nil)
(in? const-decl "bool" meng_scaff_defs nil)
(remove const-decl "set" sets nil)
(subgraph const-decl "Subgraph(G)" subgraphs nil)
(H const-decl "Subgraph(G)" meng_scaff_defs nil)
(meng const-decl "graph[T]" meng_scaff_defs nil)
(member const-decl "bool" sets nil))
nil))
(del_vert_comm 0
(del_vert_comm-1 nil 3507100603
("" (skosimp*)
(("" (apply-extensionality 1 :hide? t)
(("1" (apply-extensionality 1 :hide? t)
(("1" (expand "del_vert")
(("1" (iff 1) (("1" (ground) nil)))))))
("2" (apply-extensionality 1 :hide? t)
(("2" (expand "del_vert")
(("2" (expand "remove")
(("2" (expand "member")
(("2" (iff 1) (("2" (ground) nil))))))))))))))
nil)
((T formal-type-decl nil meng_scaff_defs 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)
(del_vert const-decl "graph[T]" graph_ops nil)
(graph type-eq-decl nil graphs nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(member const-decl "bool" sets nil)
(remove const-decl "set" sets nil))
nil))
(H_comm 0
(H_comm-1 nil 3507100603
("" (skosimp*)
(("" (expand "H")
(("" (expand "path_comp")
(("" (rewrite "del_vert_comm") nil))))))
nil)
((H const-decl "Subgraph(G)" meng_scaff_defs nil)
(del_vert_comm formula-decl nil meng_scaff_defs nil)
(T formal-type-decl nil meng_scaff_defs 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)
(path_comp const-decl "Subgraph(G)" meng_scaff_defs nil))
nil))
(incident_comm 0
(incident_comm-1 nil 3507100603
("" (skosimp*)
(("" (expand "incident") (("" (rewrite "H_comm") nil)))) nil)
((incident const-decl "finite_set[doubleton[T]]" meng_scaff_defs
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 meng_scaff_defs nil)
(H_comm formula-decl nil meng_scaff_defs nil))
nil))
(meng_comm_TCC1 0
(meng_comm_TCC1-1 nil 3507100603 ("" (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 meng_scaff_defs 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))
(meng_comm_TCC2 0
(meng_comm_TCC2-1 nil 3507100603 ("" (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 meng_scaff_defs 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))
(meng_comm 0
(meng_comm-1 nil 3507100603
("" (skosimp*)
(("" (hide -1)
(("" (expand "meng")
((""
(case-replace
"H(G!1, t!1, w2!1, w1!1) = H(G!1, t!1, w1!1, w2!1)")
(("1" (split 3)
(("1" (hide -1)
(("1" (apply-extensionality 1 :hide? t)
(("1" (expand "add")
(("1" (expand "member")
(("1" (iff) (("1" (ground) nil)))))))))))
("2" (apply-extensionality 1 :hide? t)
(("1" (expand "union")
(("1" (expand "add")
(("1" (expand "member")
(("1" (iff)
(("1" (lemma "incident_comm")
(("1" (inst?)
(("1" (lemma "incident_comm")
(("1"
(inst -1 "G!1" "t!1" "w2!1" "w1!1"
"w2!1")
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(ground)
nil)))))))))))))))))))))))))
("2" (inst?) (("2" (assert) nil)))
("3" (inst?) (("3" (assert) nil)))))))
("2" (hide 4)
(("2" (lemma "H_comm") (("2" (inst?) nil))))))))))))
nil)
((T formal-type-decl nil meng_scaff_defs 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)
(subgraph? const-decl "bool" subgraphs nil)
(Subgraph type-eq-decl nil subgraphs nil)
(H const-decl "Subgraph(G)" meng_scaff_defs nil)
(incident const-decl "finite_set[doubleton[T]]" meng_scaff_defs
nil)
(is_finite const-decl "bool" finite_sets nil)
(union const-decl "set" sets nil)
(nil application-judgement "finite_set[T]" meng_scaff_defs nil)
(finite_union application-judgement "finite_set" finite_sets nil)
(incident_comm formula-decl nil meng_scaff_defs nil)
(member const-decl "bool" sets nil)
(nonempty_add_finite application-judgement "non_empty_finite_set"
finite_sets nil)
(nonempty? const-decl "bool" sets nil)
(add const-decl "(nonempty?)" sets nil)
(H_comm formula-decl nil meng_scaff_defs nil)
(meng const-decl "graph[T]" meng_scaff_defs nil))
nil)))
[ Dauer der Verarbeitung: 0.38 Sekunden
(vorverarbeitet)
]
|
