|
(cross_product
(cross_product_empty1 0
(cross_product_empty1-1 nil 3346222769
("" (skosimp)
(("" (expand "cross_product")
(("" (expand "empty?")
(("" (skosimp)
(("" (expand "member")
(("" (flatten) (("" (inst - "x!1`1") nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((cross_product const-decl "set[[T1, T2]]" cross_product nil)
(T1 formal-type-decl nil cross_product nil)
(T2 formal-type-decl nil cross_product nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil))
shostak))
(cross_product_empty2 0
(cross_product_empty2-1 nil 3346222805
("" (skosimp)
(("" (expand "cross_product")
(("" (expand "empty?")
(("" (skosimp)
(("" (expand "member")
(("" (flatten) (("" (inst - "x!1`2") nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((cross_product const-decl "set[[T1, T2]]" cross_product nil)
(T2 formal-type-decl nil cross_product nil)
(T1 formal-type-decl nil cross_product nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil))
shostak))
(cross_product_emptyset1 0
(cross_product_emptyset1-1 nil 3346223889
("" (skosimp)
(("" (lemma "cross_product_empty1" ("A" "emptyset[T1]" "B" "B!1"))
(("" (lemma "emptyset_is_empty?" ("a" "emptyset[T1]"))
(("" (assert) nil nil)) nil))
nil))
nil)
((T2 formal-type-decl nil cross_product nil)
(emptyset const-decl "set" sets nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T1 formal-type-decl nil cross_product nil)
(cross_product_empty1 formula-decl nil cross_product nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(emptyset_is_empty? formula-decl nil sets_lemmas nil))
shostak))
(cross_product_emptyset2 0
(cross_product_emptyset2-1 nil 3346223969
("" (skosimp)
(("" (lemma "emptyset_is_empty?" ("a" "emptyset[T2]"))
((""
(lemma "cross_product_empty2" ("B" "emptyset[T2]" "A" "A!1"))
(("" (assert) nil nil)) nil))
nil))
nil)
((T2 formal-type-decl nil cross_product nil)
(emptyset const-decl "set" sets nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(emptyset_is_empty? formula-decl nil sets_lemmas nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(cross_product_empty2 formula-decl nil cross_product nil)
(T1 formal-type-decl nil cross_product nil))
shostak))
(cross_product_fullset 0
(cross_product_fullset-1 nil 3346228173
("" (expand "fullset")
(("" (expand "cross_product")
(("" (expand "full?")
(("" (skosimp)
(("" (expand "member") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((cross_product const-decl "set[[T1, T2]]" cross_product nil)
(member const-decl "bool" sets nil)
(full? const-decl "bool" sets nil)
(fullset const-decl "set" sets nil))
shostak))
(projection_product1 0
(projection_product1-1 nil 3346221058
("" (skosimp)
(("" (typepred "NB!1")
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (skosimp)
(("" (expand "member")
(("" (expand "cross_product")
(("" (expand "projection_1")
(("" (apply-extensionality :hide? t)
(("" (case-replace "A!1(x!2)")
(("1" (inst + "(x!2,x!1)")
(("1" (assert) nil nil)) nil)
("2" (assert)
(("2" (skosimp) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(T2 formal-type-decl nil cross_product nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(projection_1 const-decl "set[T1]" cross_product nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(T1 formal-type-decl nil cross_product nil)
(cross_product const-decl "set[[T1, T2]]" cross_product nil))
shostak))
(projection_product2 0
(projection_product2-1 nil 3346222475
("" (skosimp)
(("" (typepred "NA!1")
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (skosimp)
(("" (expand "cross_product")
(("" (expand "projection_2")
(("" (expand "member")
(("" (apply-extensionality :hide? t)
(("" (case-replace "B!1(x!2)")
(("1" (inst + "(x!1,x!2)")
(("1" (assert) nil nil)) nil)
("2" (assert)
(("2" (skosimp) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(T1 formal-type-decl nil cross_product nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(empty? const-decl "bool" sets nil)
(cross_product const-decl "set[[T1, T2]]" cross_product nil)
(member const-decl "bool" sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(T2 formal-type-decl nil cross_product nil)
(projection_2 const-decl "set[T2]" cross_product nil))
shostak))
(projection_1_emptyset 0
(projection_1_emptyset-1 nil 3346223533
("" (expand "emptyset")
(("" (apply-extensionality :hide? t)
(("" (expand "projection_1") (("" (propax) nil nil)) nil)) nil))
nil)
((T1 formal-type-decl nil cross_product nil)
(boolean nonempty-type-decl nil booleans nil)
(FALSE const-decl "bool" booleans nil)
(projection_1 const-decl "set[T1]" cross_product nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T2 formal-type-decl nil cross_product nil)
(emptyset const-decl "set" sets nil))
shostak))
(projection_2_emptyset 0
(projection_2_emptyset-1 nil 3346223560
("" (expand "emptyset")
(("" (apply-extensionality :hide? t)
(("" (expand "projection_2") (("" (propax) nil nil)) nil)) nil))
nil)
((T2 formal-type-decl nil cross_product nil)
(boolean nonempty-type-decl nil booleans nil)
(FALSE const-decl "bool" booleans nil)
(projection_2 const-decl "set[T2]" cross_product nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T1 formal-type-decl nil cross_product nil)
(emptyset const-decl "set" sets nil))
shostak))
(projection_1_fullset 0
(projection_1_fullset-1 nil 3346228390
("" (skosimp*)
(("" (apply-extensionality :hide? t)
(("" (expand "fullset")
(("" (expand "projection_1")
(("" (inst + "(x!1,b!1)") nil nil)) nil))
nil))
nil))
nil)
((T1 formal-type-decl nil cross_product nil)
(boolean nonempty-type-decl nil booleans nil)
(fullset const-decl "set" sets nil)
(projection_1 const-decl "set[T1]" cross_product nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T2 formal-type-decl nil cross_product nil))
shostak))
(projection_2_fullset 0
(projection_2_fullset-1 nil 3346229607
("" (skosimp*)
(("" (apply-extensionality :hide? t)
(("" (expand "fullset")
(("" (expand "projection_2")
(("" (inst + "(a!1,x!1)") nil nil)) nil))
nil))
nil))
nil)
((T2 formal-type-decl nil cross_product nil)
(boolean nonempty-type-decl nil booleans nil)
(fullset const-decl "set" sets nil)
(projection_2 const-decl "set[T2]" cross_product nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T1 formal-type-decl nil cross_product nil))
shostak))
(cross_product_empty1_rew 0
(cross_product_empty1_rew-1 nil 3346229731
("" (skosimp)
(("" (lemma "cross_product_emptyset1" ("B" "B!1"))
((""
(lemma "emptyset_is_empty?"
("a" "cross_product(emptyset[T1], B!1)"))
(("" (assert) nil nil)) nil))
nil))
nil)
((set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T2 formal-type-decl nil cross_product nil)
(cross_product_emptyset1 formula-decl nil cross_product nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(emptyset_is_empty? formula-decl nil sets_lemmas nil)
(cross_product const-decl "set[[T1, T2]]" cross_product nil)
(emptyset const-decl "set" sets nil)
(T1 formal-type-decl nil cross_product nil))
shostak))
(cross_product_empty2_rew 0
(cross_product_empty2_rew-1 nil 3346229792
("" (skosimp)
(("" (lemma "cross_product_emptyset2" ("A" "A!1"))
((""
(lemma "emptyset_is_empty?"
("a" "cross_product(A!1,emptyset[T2])"))
(("" (assert) nil nil)) nil))
nil))
nil)
((set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T1 formal-type-decl nil cross_product nil)
(cross_product_emptyset2 formula-decl nil cross_product nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(emptyset_is_empty? formula-decl nil sets_lemmas nil)
(cross_product const-decl "set[[T1, T2]]" cross_product nil)
(emptyset const-decl "set" sets nil)
(T2 formal-type-decl nil cross_product nil))
shostak))
(cross_product_full_rew 0
(cross_product_full_rew-1 nil 3346245659
("" (apply-extensionality :hide? t)
(("" (expand "fullset")
(("" (expand "cross_product") (("" (propax) nil nil)) nil)) nil))
nil)
((bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(cross_product const-decl "set[[T1, T2]]" cross_product nil)
(fullset const-decl "set" sets nil)
(boolean nonempty-type-decl nil booleans nil)
(T2 formal-type-decl nil cross_product nil)
(T1 formal-type-decl nil cross_product nil))
shostak))
(cross_product_TCC1 0
(cross_product_TCC1-1 nil 3346225743
("" (inst + "emptyset[[T1,T2]]")
(("" (inst + "emptyset[T1]" "emptyset[T2]")
(("" (apply-extensionality :hide? t)
(("" (expand "emptyset")
(("" (expand "cross_product") (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
((emptyset const-decl "set" sets nil)
(cross_product const-decl "set[[T1, T2]]" cross_product nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T2 formal-type-decl nil cross_product nil)
(T1 formal-type-decl nil cross_product nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil))
nil))
(product_projection 0
(product_projection-1 nil 3346221206
("" (skosimp)
(("" (typepred "Y!1")
(("" (skosimp)
(("" (replace -1)
(("" (hide -1)
(("" (case "nonempty?(A!1)")
(("1" (rewrite "projection_product2" 1)
(("1" (case "nonempty?(B!1)")
(("1" (rewrite "projection_product1") nil nil)
("2" (expand "nonempty?" 1)
(("2"
(lemma "cross_product_empty2"
("A" "A!1" "B" "B!1"))
(("2" (assert)
(("2"
(lemma "emptyset_is_empty?"
("a" "cross_product(A!1, B!1)"))
(("2" (assert)
(("2" (replace -1)
(("2"
(lemma "projection_1_emptyset")
(("2"
(replace -1 1)
(("2"
(lemma
"cross_product_emptyset1"
("B" "B!1"))
(("2"
(rewrite "emptyset_is_empty?" -1)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "nonempty?" 1)
(("2"
(lemma "cross_product_empty1" ("A" "A!1" "B" "B!1"))
(("2" (assert)
(("2"
(lemma "emptyset_is_empty?"
("a" "cross_product(A!1, B!1)"))
(("2" (lemma "emptyset_is_empty?" ("a" "A!1"))
(("2" (assert)
(("2" (replace -2)
(("2" (lemma "projection_1_emptyset")
(("2"
(lemma "projection_2_emptyset")
(("2"
(replace -1)
(("2"
(replace -2)
(("2"
(lemma
"cross_product_emptyset1"
("B" "emptyset[T2]"))
(("2"
(lemma
"emptyset_is_empty?"
("a"
"cross_product(emptyset[T1], emptyset[T2])"))
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((cross_product nonempty-type-eq-decl nil cross_product nil)
(cross_product const-decl "set[[T1, T2]]" cross_product nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(T2 formal-type-decl nil cross_product nil)
(set type-eq-decl nil sets nil)
(T1 formal-type-decl nil cross_product nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nonempty? const-decl "bool" sets nil)
(projection_product1 formula-decl nil cross_product nil)
(cross_product_empty2 formula-decl nil cross_product nil)
(emptyset_is_empty? formula-decl nil sets_lemmas nil)
(emptyset const-decl "set" sets nil)
(cross_product_emptyset1 formula-decl nil cross_product nil)
(projection_1_emptyset formula-decl nil cross_product nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(projection_product2 formula-decl nil cross_product nil)
(cross_product_empty1 formula-decl nil cross_product nil)
(projection_2_emptyset formula-decl nil cross_product nil))
shostak)))
¤ Dauer der Verarbeitung: 0.4 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.
|
