|
(matroids
(single_TCC1 0
(single_TCC1-1 nil 3322073591
("" (skosimp*)
(("" (lemma "finite_singleton[T]")
(("" (expand "singleton") (("" (inst?) nil))))))
nil)
((T formal-type-decl nil matroids nil)
(finite_singleton judgement-tcc nil finite_sets nil)
(singleton const-decl "(singleton?)" sets nil))
nil))
(double_TCC1 0
(double_TCC1-1 nil 3322073591
("" (skosimp*)
(("" (lemma "finite_add[T]")
(("" (inst -1 "singleton[T](x!1)" "y!1")
(("" (expand "add")
(("" (expand "member")
(("" (expand "singleton")
((""
(case-replace
"{y: T | (y!1 = y OR y = x!1)} = {t: T | t = x!1 OR t = y!1}")
(("" (hide -1 2)
(("" (apply-extensionality 1 :hide? t)
(("" (iff 1) (("" (ground) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil matroids nil)
(finite_add formula-decl nil finite_sets nil)
(add const-decl "(nonempty?)" sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(member const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(singleton? const-decl "bool" sets 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)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets nil))
nil))
(extend_TCC1 0
(extend_TCC1-1 nil 3322073591
("" (skosimp*)
(("" (typepred "a!1")
(("" (typepred "A!1")
(("" (expand "subset?")
(("" (expand "member")
(("" (inst?) (("" (assert) nil))))))))))))
nil)
((Subsets type-eq-decl nil matroids nil)
(Matroid type-eq-decl nil matroids nil)
(indep_card const-decl "bool" matroids nil)
(indep_subset const-decl "bool" matroids nil)
(indep_in_elem const-decl "bool" matroids nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(pre_matroid type-eq-decl nil matroids nil)
(subset? const-decl "bool" sets 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 matroids 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))
(extend_TCC2 0
(extend_TCC2-3 "V3" 3322297301
("" (skosimp*)
(("" (typepred "A!1")
(("" (lemma "finite_sets_eq[T,T].surjection_from_finite_set")
(("" (inst -1 "A!1" "{t: T | EXISTS (a: (A!1)): f!1(a) = t}")
(("1" (bddsimp)
(("1"
(inst 1
"restrict[(elem(M1!1)),(A!1),(elem(M2!1))].restrict(f!1)")
(("1" (expand "surjective?")
(("1" (skosimp*)
(("1" (typepred "y!1")
(("1" (skosimp*)
(("1" (inst 1 "a!1")
(("1" (typepred "a!1")
(("1" (hide -3 -4 2)
(("1" (expand "restrict")
(("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (typepred "x1!1")
(("2" (expand "subset?")
(("2" (expand "member")
(("2" (inst -3 "x1!1")
(("2" (bddsimp)
(("2" (inst 1 "x1!1")
(("2" (expand "restrict")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp*)
(("3" (install-rewrites "finite_sets[T]")
(("3" (typepred "x!1")
(("3" (expand "subset?")
(("3" (expand "member")
(("3" (inst -3 "x!1") (("3" (prop) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (install-rewrites "finite_sets[T]")
(("2" (skosimp*)
(("2" (typepred "a!1")
(("2" (expand "subset?")
(("2" (expand "member")
(("2" (inst -3 "a!1") (("2" (bddsimp) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Subsets type-eq-decl nil matroids nil)
(Matroid type-eq-decl nil matroids nil)
(indep_card const-decl "bool" matroids nil)
(indep_subset const-decl "bool" matroids nil)
(indep_in_elem const-decl "bool" matroids nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(pre_matroid type-eq-decl nil matroids nil)
(subset? const-decl "bool" sets 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 matroids nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(A!1 skolem-const-decl "Subsets(elem(M1!1))" matroids nil)
(M1!1 skolem-const-decl "Matroid" matroids nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(restrict const-decl "R" restrict nil)
(f!1 skolem-const-decl "[(elem(M1!1)) -> (elem(M2!1))]" matroids
nil)
(M2!1 skolem-const-decl "Matroid" matroids nil)
(surjective? const-decl "bool" functions nil)
(member const-decl "bool" sets nil)
(surjection_from_finite_set formula-decl nil finite_sets_eq
"finite_sets/"))
nil)
(extend_TCC2-2 "V3" 3322078043
("" (skosimp*) (("" (typepred "A!1") (("" (postpone) nil nil)) nil))
nil)
nil shostak)
(extend_TCC2-1 nil 3322073591
("" (skosimp*)
(("" (typepred "A!1") (("" (hide -1) (("" (postpone) nil)))))) nil)
nil nil))
(circuit_test 0
(circuit_test-1 nil 3322073591
("" (skolem! 1)
(("" (flatten)
(("" (expand "circuit?")
(("" (flatten)
(("" (bddsimp)
(("" (typepred "M!1")
(("" (expand "indep_subset")
(("" (lemma "finite_sets[T].same_card_subset")
(("" (lemma "finite_sets[T].smaller_card_subset")
(("" (lemma "finite_sets[T].card_subset")
(("" (inst -3 "B!1" "A!1")
(("" (bddsimp)
(("1" (inst -2 "B!1" "A!1")
(("1" (bddsimp)
(("1" (skosimp*) nil nil)
("2"
(inst -1 "B!1" "A!1")
(("2"
(bddsimp)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (inst -2 "B!1" "A!1")
(("2" (inst -1 "B!1" "A!1")
(("2"
(bddsimp)
(("1"
(skosimp*)
(("1"
(case
"subset?(B!1,remove(x!1,A!1))")
(("1"
(inst -6 "remove(x!1,A!1)" "B!1")
(("1"
(bddsimp)
(("1"
(hide -7)
(("1"
(inst -7 "x!1")
(("1"
(assert)
(("1"
(expand "member")
(("1"
(propax)
nil
nil))
nil))
nil)
("2"
(expand "member")
(("2"
(assert)
(("2"
(expand
"indep_in_elem")
(("2"
(inst -5 "A!1")
(("2"
(reveal -3)
(("2"
(assert)
(("2"
(bddsimp)
(("2"
(expand
"subset?")
(("2"
(inst
-1
"x!1")
(("2"
(expand
"member"
-1)
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide [-4 -5 -6 -7 -8])
(("2"
(hide [3 4 5 6])
(("2"
(ground)
(("2"
(hide -4 -5)
(("2"
(hide 3 4)
(("2"
(hide -2)
(("2"
(install-rewrites
t
"finite_sets[T]")
(("2"
(assert)
(("2"
(skosimp*)
(("2"
(bddsimp)
(("1"
(assert)
nil
nil)
("2"
(assert)
(("2"
(inst
-2
"x!2")
(("2"
(bddsimp)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but (-2 1 2))
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((Matroid type-eq-decl nil matroids nil)
(indep_card const-decl "bool" matroids nil)
(indep_subset const-decl "bool" matroids nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(indep_in_elem const-decl "bool" matroids nil)
(pre_matroid type-eq-decl nil matroids nil)
(finite_set type-eq-decl nil finite_sets nil)
(T formal-type-decl nil matroids nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(same_card_subset formula-decl nil finite_sets nil)
(card_subset formula-decl nil finite_sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(/= const-decl "boolean" notequal nil)
(member const-decl "bool" sets nil)
(x!1 skolem-const-decl "T" matroids nil)
(M!1 skolem-const-decl "Matroid" matroids nil)
(remove const-decl "set" sets nil)
(subset? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(smaller_card_subset formula-decl nil finite_sets nil)
(circuit? const-decl "bool" matroids nil)
(finite_remove application-judgement "finite_set" finite_sets nil))
nil))
(circuit_test2 0
(circuit_test2-1 nil 3322073591
("" (skosimp*)
(("" (expand "circuit?")
(("" (bddsimp)
(("" (skosimp*)
(("" (inst -2 "remove(x!1,A!1)")
(("" (bddsimp)
(("1" (hide -1 1 3)
(("1" (install-rewrites "finite_sets[T]")
(("1" (assert)
(("1" (expand "remove")
(("1" (expand "member")
(("1" (replace -1 -2 rl)
(("1" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1 1 3)
(("2" (expand "subset?")
(("2" (skosimp*)
(("2" (expand "member")
(("2" (expand "remove")
(("2" (expand "member") (("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((finite_remove application-judgement "finite_set" finite_sets nil)
(circuit? const-decl "bool" matroids nil)
(member const-decl "bool" sets nil)
(/= const-decl "boolean" notequal nil)
(subset? const-decl "bool" sets nil)
(Matroid type-eq-decl nil matroids nil)
(indep_card const-decl "bool" matroids nil)
(indep_subset const-decl "bool" matroids nil)
(indep_in_elem const-decl "bool" matroids nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(pre_matroid type-eq-decl nil matroids nil)
(remove const-decl "set" sets 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 matroids nil))
nil)))
¤ Dauer der Verarbeitung: 0.24 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.
|
