|
(ordered_message
(valid_iff_ord1 0
(valid_iff_ord1-1 nil 3394812915
("" (skosimp*) (("" (expand "ord") (("" (ground) nil nil)) nil))
nil)
((ord const-decl "upto(1)" message_adt nil)) shostak))
(eq_iff 0
(eq_iff-1 nil 3394814913
("" (skosimp*)
(("" (split)
(("1" (flatten)
(("1" (replace -1)
(("1" (rewrite "valid_iff_ord1") (("1" (assert) nil nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (prop)
(("1" (use "message_valid_extensionality")
(("1" (assert) nil nil)) nil)
("2" (expand "ord")
(("2" (lift-if) (("2" (ground) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
((message type-decl nil message_adt nil)
(T formal-nonempty-type-decl nil ordered_message nil)
(valid_iff_ord1 formula-decl nil ordered_message nil)
(boolean nonempty-type-decl nil booleans nil)
(valid? adt-recognizer-decl "[message -> boolean]" message_adt nil)
(message_valid_extensionality formula-decl nil message_adt nil)
(ord const-decl "upto(1)" message_adt nil))
shostak))
(message_total_order 0
(message_total_order-1 nil 3394808860
("" (typepred "leq")
(("" (expand "total_order?")
(("" (expand "partial_order?")
(("" (expand "preorder?")
(("" (expand "<=")
(("" (prop)
(("1" (expand "reflexive?")
(("1" (skosimp*)
(("1" (inst?)
(("1" (assert) nil nil) ("2" (assert) nil nil))
nil))
nil))
nil)
("2" (expand "transitive?")
(("2" (skosimp*)
(("2"
(case "valid?(x!1) & valid?(y!1) & valid?(z!1)")
(("1" (flatten)
(("1" (assert)
(("1"
(inst - "value(x!1)" "value(y!1)"
"value(z!1)")
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (rewrite "valid_iff_ord1")
(("2" (rewrite "valid_iff_ord1")
(("2" (rewrite "valid_iff_ord1")
(("2" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "antisymmetric?")
(("3" (skosimp*)
(("3" (case " valid?(x!1)")
(("1" (case " valid?(y!1)")
(("1" (assert)
(("1" (inst?)
(("1" (apply-extensionality) nil nil)) nil))
nil)
("2" (rewrite "eq_iff")
(("2" (flatten)
(("2" (assert)
(("2" (expand "ord")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (rewrite "eq_iff")
(("2" (assert)
(("2" (expand "ord") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (expand "dichotomous?")
(("4" (skosimp*)
(("4" (inst?)
(("1" (ground) nil nil) ("2" (assert) nil nil)
("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((preorder? const-decl "bool" orders nil)
(value adt-accessor-decl "[(valid?) -> T]" message_adt nil)
(x!1 skolem-const-decl "message[T]" ordered_message nil)
(valid? adt-recognizer-decl "[message -> boolean]" message_adt nil)
(message type-decl nil message_adt nil)
(reflexive? const-decl "bool" relations nil)
(valid_iff_ord1 formula-decl nil ordered_message nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(transitive? const-decl "bool" relations nil)
(message_valid_extensionality formula-decl nil message_adt nil)
(ord const-decl "upto(1)" message_adt nil)
(eq_iff formula-decl nil ordered_message nil)
(antisymmetric? const-decl "bool" relations nil)
(y!1 skolem-const-decl "message[T]" ordered_message nil)
(x!1 skolem-const-decl "message[T]" ordered_message nil)
(dichotomous? const-decl "bool" orders nil)
(<= const-decl "bool" ordered_message nil)
(partial_order? const-decl "bool" orders 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-nonempty-type-decl nil ordered_message nil)
(pred type-eq-decl nil defined_types nil)
(total_order? const-decl "bool" orders nil)
(leq formal-const-decl "(total_order?[T])" ordered_message nil))
nil)))
¤ Dauer der Verarbeitung: 0.16 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.
|
