|
(lift_props
(down_up 0
(down_up-1 nil 3353045582 ("" (grind) nil nil) nil shostak))
(up_down 0
(up_down-1 nil 3353049060
("" (skosimp) (("" (grind) (("" (decompose-equality) nil nil)) nil))
nil)
((up adt-constructor-decl "[T -> (up?)]" lift_adt nil)
(down adt-accessor-decl "[(up?) -> T]" lift_adt nil)
(lift_up_extensionality formula-decl nil lift_adt nil)
(T formal-type-decl nil lift_props nil)
(lift type-decl nil lift_adt nil)
(boolean nonempty-type-decl nil booleans nil)
(up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil))
shostak))
(down_equal 0
(down_equal-1 nil 3353768866
("" (skosimp)
(("" (case-replace "y1!1=y2!1")
(("1" (assert) nil nil)
("2" (assert)
(("2" (lemma "up_down" ("y" "y1!1"))
(("2" (lemma "up_down" ("y" "y2!1")) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((T formal-type-decl nil lift_props nil)
(lift type-decl nil lift_adt nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(up_down formula-decl nil lift_props nil))
shostak))
(up_equal 0
(up_equal-1 nil 3353045918
("" (skosimp)
(("" (case-replace "x1!1=x2!1")
(("1" (assert) nil nil)
("2" (assert)
(("2" (lemma "down_equal" ("y1" "up(x1!1)" "y2" "up(x2!1)"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil)
((T formal-type-decl nil lift_props nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(up adt-constructor-decl "[T -> (up?)]" lift_adt nil)
(up? adt-recognizer-decl "[lift -> boolean]" lift_adt nil)
(lift type-decl nil lift_adt nil)
(down_equal formula-decl nil lift_props nil))
shostak)))
¤ Dauer der Verarbeitung: 0.26 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.
|
