|
(doubletons
(dbl_comm 0
(dbl_comm-1 nil 3507100930
("" (skosimp*)
(("" (expand "dbl")
(("" (apply-extensionality 1 :hide? t)
(("" (iff) (("" (ground) nil))))))))
nil)
((dbl const-decl "set[T]" doubletons nil)
(bool nonempty-type-eq-decl nil booleans nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil doubletons nil))
nil))
(doubleton_irreflexive 0
(doubleton_irreflexive-1 nil 3507100930
("" (skosimp*)
(("" (expand "doubleton?")
(("" (skosimp*)
((""
(case "(FORALL (z:T): member(z,dbl(x!1, x!1)) = member(z,dbl(x!2, y!1)))")
(("1" (inst-cp -1 "x!2")
(("1" (inst -1 "y!1")
(("1" (expand "member")
(("1" (expand "dbl")
(("1" (hide -3) (("1" (ground) nil)))))))))))
("2" (skosimp*)
(("2" (expand "member")
(("2" (replace -1) (("2" (propax) nil))))))))))))))
nil)
((doubleton? const-decl "bool" doubletons nil)
(dbl const-decl "set[T]" doubletons nil)
(member const-decl "bool" sets nil) (set type-eq-decl nil sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil doubletons nil))
nil))
(doubleton_nonempty 0
(doubleton_nonempty-1 nil 3507100930 ("" (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 doubletons nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(/= const-decl "boolean" notequal nil)
(set type-eq-decl nil sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(dbl const-decl "set[T]" doubletons nil)
(doubleton type-eq-decl nil doubletons nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil))
nil))
(doubleton_rest_nonempty 0
(doubleton_rest_nonempty-1 nil 3507100930
("" (skolem-typepred)
(("" (skosimp*)
(("" (expand "rest")
(("" (rewrite "doubleton_nonempty")
(("" (expand "nonempty?")
(("" (assert)
(("" (prop)
(("" (expand "empty?")
(("" (expand "remove")
(("" (expand "member")
(("" (inst-cp - "x!1")
(("" (inst - "y!1")
(("" (replace -1)
(("" (expand "dbl")
((""
(assert)
nil))))))))))))))))))))))))))))
nil)
((doubleton_nonempty formula-decl nil doubletons nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(remove const-decl "set" sets nil)
(nonempty? const-decl "bool" sets nil)
(rest const-decl "set" sets nil)
(doubleton type-eq-decl nil doubletons nil)
(dbl const-decl "set[T]" doubletons nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(set type-eq-decl nil sets nil)
(/= const-decl "boolean" notequal nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(T formal-type-decl nil doubletons nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(dbl_choose_TCC1 0
(dbl_choose_TCC1-1 nil 3507100930 ("" (subtype-tcc) nil nil)
((T formal-type-decl nil doubletons nil)
(dbl const-decl "set[T]" doubletons nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil))
nil))
(dbl_choose 0
(dbl_choose-1 nil 3507100930
("" (skosimp*)
(("" (expand "dbl")
(("" (lemma "choose_is_epsilon[T]")
(("" (inst?)
(("1" (lemma "epsilon_ax[T]")
(("1" (inst?)
(("1" (assert) (("1" (inst + "x!1") nil nil)) nil)) nil)
("2" (assert) (("2" (inst + "x!1") nil nil)) nil))
nil)
("2" (expand "nonempty?")
(("2" (expand "empty?")
(("2" (expand "member") (("2" (inst - "x!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((dbl const-decl "set[T]" doubletons nil)
(y!1 skolem-const-decl "T" doubletons nil)
(x!1 skolem-const-decl "T" doubletons nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(pred type-eq-decl nil defined_types nil)
(TRUE const-decl "bool" booleans nil)
(epsilon_ax formula-decl nil epsilons nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(choose_is_epsilon formula-decl nil sets nil)
(T formal-type-decl nil doubletons nil))
nil))
(dbl_rest_choose_TCC1 0
(dbl_rest_choose_TCC1-1 nil 3507100930
("" (skosimp*)
(("" (use "doubleton_rest_nonempty")
(("" (inst?) (("" (assert) nil))))))
nil)
((doubleton_rest_nonempty formula-decl nil doubletons nil)
(x!1 skolem-const-decl "T" doubletons nil)
(y!1 skolem-const-decl "T" doubletons 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 doubletons nil))
nil))
(dbl_rest_choose 0
(dbl_rest_choose-1 nil 3507100930
("" (skosimp*)
(("" (expand "rest")
(("" (lemma "doubleton_nonempty")
(("" (inst - "dbl(x!1, y!1)")
(("1" (expand "nonempty?")
(("1" (assert)
(("1" (use "dbl_choose")
(("1" (ground)
(("1" (replace -2)
(("1" (expand "remove")
(("1" (expand "member") (("1" (assert) nil nil))
nil))
nil))
nil)
("2" (replace -1)
(("2" (expand "remove")
(("2" (expand "member")
(("2" (assert)
(("2" (expand "dbl")
(("2" (hide -1 3)
(("2"
(lemma "choose_is_epsilon[T]")
(("2"
(inst?)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(lemma "epsilon_ax[T]")
(("1"
(inst?)
(("1"
(assert)
(("1"
(inst + "y!1")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2" (inst + "y!1") nil nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(hide 3)
(("2"
(lemma "epsilon_ax[T]")
(("1"
(inst?)
(("1"
(hide 3)
(("1"
(expand "nonempty?")
(("1"
(expand "empty?")
(("1"
(expand "member")
(("1"
(assert)
(("1"
(inst -2 "y!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst + "x!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (replace -2)
(("3" (expand "remove") (("3" (assert) nil nil))
nil))
nil)
("4" (replace -1)
(("4" (expand "remove")
(("4" (expand "member")
(("4" (expand "dbl")
(("4" (assert)
(("4" (hide -1)
(("4"
(hide 3)
(("4"
(lemma "choose_is_epsilon[T]")
(("4"
(inst?)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(lemma "epsilon_ax[T]")
(("1"
(inst?)
(("1"
(assert)
(("1"
(inst + "x!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(inst + "x!1")
nil
nil))
nil))
nil))
nil)
("2"
(expand "nonempty?")
(("2"
(expand "empty?")
(("2"
(expand "member")
(("2"
(inst - "x!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((rest const-decl "set" sets nil)
(y!1 skolem-const-decl "T" doubletons nil)
(x!1 skolem-const-decl "T" doubletons nil)
(dbl const-decl "set[T]" doubletons nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(set type-eq-decl nil sets nil)
(/= const-decl "boolean" notequal nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil doubletons nil)
(doubleton type-eq-decl nil doubletons nil)
(remove const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(pred type-eq-decl nil defined_types nil)
(TRUE const-decl "bool" booleans nil)
(epsilon_ax formula-decl nil epsilons nil)
(empty? const-decl "bool" sets nil)
(choose_is_epsilon formula-decl nil sets nil)
(dbl_choose formula-decl nil doubletons nil)
(nonempty? const-decl "bool" sets nil)
(doubleton_nonempty formula-decl nil doubletons nil))
nil))
(dbl_to_pair_TCC1 0
(dbl_to_pair_TCC1-1 nil 3507100930
("" (inst 1 " (LAMBDA D: (choose(D),choose(rest(D))))")
(("1" (skosimp*)
(("1" (typepred "D!1")
(("1" (skosimp*)
(("1" (replace -1)
(("1" (lemma "dbl_choose")
(("1" (inst?)
(("1" (lemma "dbl_rest_choose")
(("1" (inst?)
(("1" (assert)
(("1" (flatten)
(("1" (assert)
(("1" (prop)
(("1" (replace*) nil)
("2" (replace*)
(("2" (rewrite "dbl_comm") nil)))
("3" (replace*) nil)
("4" (replace*)
nil)))))))))))))))))))))))))
("2" (lemma "doubleton_rest_nonempty") (("2" (propax) nil)))
("3" (lemma "doubleton_nonempty") (("3" (propax) nil))))
nil)
((doubleton_nonempty formula-decl nil doubletons nil)
(doubleton_rest_nonempty formula-decl nil doubletons nil)
(dbl_choose formula-decl nil doubletons nil)
(dbl_rest_choose formula-decl nil doubletons nil)
(dbl_comm formula-decl nil doubletons nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(rest const-decl "set" sets nil) (choose const-decl "(p)" sets nil)
(nonempty? 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 doubletons nil))
nil))
(dbl_def 0
(dbl_def-1 nil 3507100930 ("" (skosimp*) (("" (assert) nil)) nil) nil
nil))
(dbl_in 0
(dbl_in-1 nil 3507100930
("" (skosimp*)
(("" (replace -1) (("" (hide -1) (("" (grind) nil)))))) nil)
((dbl const-decl "set[T]" doubletons nil)) nil))
(dbl_not_in 0
(dbl_not_in-1 nil 3507100930
("" (skosimp*)
(("" (replace -1) (("" (hide -1) (("" (grind) nil)))))) nil)
((dbl const-decl "set[T]" doubletons nil)) nil))
(dbl_to_pair_lem_TCC1 0
(dbl_to_pair_lem_TCC1-1 nil 3507100930 ("" (subtype-tcc) nil nil)
((T formal-type-decl nil doubletons nil)
(/= const-decl "boolean" notequal nil))
nil))
(dbl_to_pair_lem 0
(dbl_to_pair_lem-1 nil 3507100930
("" (skosimp*)
(("" (typepred "dbl_to_pair(dbl(x!1, y!1))")
(("1"
(case "dbl(x!1, y!1)(x!1)
=
dbl(PROJ_1(dbl_to_pair(dbl(x!1, y!1))),
PROJ_2(dbl_to_pair(dbl(x!1, y!1))))(x!1)")
(("1"
(case "dbl(x!1, y!1)(y!1)
=
dbl(PROJ_1(dbl_to_pair(dbl(x!1, y!1))),
PROJ_2(dbl_to_pair(dbl(x!1, y!1))))(y!1)")
(("1" (hide -3)
(("1" (expand "dbl")
(("1" (apply-extensionality 2 :hide? t)
(("1" (apply-extensionality 3 :hide? t)
(("1" (expand "dbl")
(("1" (inst?) (("1" (assert) nil)))))))
("2" (apply-extensionality 3 :hide? t)
(("2" (expand "dbl")
(("2" (inst?) (("2" (assert) nil)))))))
("3" (expand "dbl")
(("3" (inst?) (("3" (assert) nil)))))))))))
("2" (assert) nil)))
("2" (assert) nil)))
("2" (inst?) (("2" (assert) nil))))))
nil)
((dbl_to_pair const-decl "{x, y | D = dbl(x, y)}" doubletons nil)
(doubleton type-eq-decl nil doubletons nil)
(/= const-decl "boolean" notequal nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(dbl const-decl "set[T]" doubletons nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil doubletons nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(y!1 skolem-const-decl "T" doubletons nil)
(x!1 skolem-const-decl "T" doubletons nil)
(OR const-decl "[bool, bool -> bool]" booleans nil))
nil))
(dbl_to_pair_inverse_l 0
(dbl_to_pair_inverse_l-1 nil 3507100930
("" (skolem-typepred)
(("" (skosimp*)
(("" (replace -1)
(("" (use "dbl_to_pair_lem")
(("" (assert)
(("" (ground)
(("1" (replace -1) (("1" (propax) nil)))
("2" (replace -1)
(("2" (rewrite "dbl_comm") nil))))))))))))))
nil)
((dbl_to_pair_lem formula-decl nil doubletons nil)
(dbl_comm formula-decl nil doubletons nil)
(doubleton type-eq-decl nil doubletons nil)
(dbl const-decl "set[T]" doubletons nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(set type-eq-decl nil sets nil)
(/= const-decl "boolean" notequal nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(T formal-type-decl nil doubletons nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(dbl_proj 0
(dbl_proj-1 nil 3507100930
("" (skosimp*)
(("" (lemma "dbl_to_pair_inverse_l")
(("" (inst?)
(("" (expand "dbl")
(("" (replace -1 + rl) (("" (assert) nil))))))))))
nil)
((dbl_to_pair_inverse_l formula-decl nil doubletons 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 doubletons nil))
nil))
(proj_dbl 0
(proj_dbl-1 nil 3507100930
("" (skosimp*)
(("" (typepred "D!1")
(("" (skosimp*)
(("" (replace -1)
(("" (hide -1)
(("" (lemma "dbl_to_pair_lem")
(("" (inst?)
(("" (assert) (("" (grind) nil))))))))))))))))
nil)
((doubleton type-eq-decl nil doubletons nil)
(dbl const-decl "set[T]" doubletons nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(set type-eq-decl nil sets nil)
(/= const-decl "boolean" notequal nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(T formal-type-decl nil doubletons nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(dbl_to_pair_lem formula-decl nil doubletons nil))
nil))
(dbl_eq 0
(dbl_eq-1 nil 3507100930
("" (skosimp*)
(("" (case "dbl(x!1, y!1)(x!1) = dbl(v!1, z!1)(x!1)")
(("1" (case "dbl(x!1, y!1)(y!1) = dbl(v!1, z!1)(y!1)")
(("1" (case "dbl(x!1, y!1)(z!1) = dbl(v!1, z!1)(z!1)")
(("1" (case "dbl(x!1, y!1)(v!1) = dbl(v!1, z!1)(v!1)")
(("1" (expand "dbl") (("1" (ground) nil)))
("2" (assert) nil)))
("2" (assert) nil)))
("2" (assert) nil)))
("2" (assert) nil))))
nil)
((dbl const-decl "set[T]" doubletons nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil doubletons nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(finite_dbl 0
(finite_dbl-1 nil 3507100930
("" (skosimp*)
(("" (case-replace "dbl(x!1, y!1) = add(x!1,singleton(y!1))")
(("1" (rewrite "finite_add")
(("1" (rewrite "finite_singleton") nil)))
("2" (hide 2)
(("2" (apply-extensionality 1 :hide? t)
(("2" (grind) nil))))))))
nil)
((nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets nil)
(nonempty_add_finite application-judgement "non_empty_finite_set"
finite_sets nil)
(T formal-type-decl nil doubletons nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(dbl const-decl "set[T]" doubletons nil)
(nonempty? const-decl "bool" sets nil)
(add const-decl "(nonempty?)" sets nil)
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(finite_add formula-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(member const-decl "bool" sets nil))
nil)))
¤ Dauer der Verarbeitung: 0.11 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.
|
