(relation_implication
(rel_impl_extensionality 0
(rel_impl_extensionality-1 nil 3570350716
("" (skosimp*)
(("" (expand "|-" ) (("" (inst?) (("" (prop) nil nil )) nil )) nil ))
nil )
((\|- const-decl "bool" relation_implication nil )
(U formal-nonempty-type-decl nil relation_implication nil )
(T formal-nonempty-type-decl nil relation_implication nil ))
shostak))
(lemma_double_impl 0
(lemma_double_impl-1 nil 3570774110
("" (skolem-typepred)
(("" (flatten)
(("" (expand "|=" )
(("" (prop)
(("" (expand "|-" )
(("" (skolem!)
(("" (inst?) (("" (inst?) (("" (prop) nil nil )) nil ))
nil ))
nil ))
nil ))
nil ))
nil ))
nil ))
nil )
((U formal-nonempty-type-decl nil relation_implication nil )
(T formal-nonempty-type-decl nil relation_implication nil )
(\|- const-decl "bool" relation_implication nil )
(\|= const-decl "bool" relation_implication nil ))
shostak))
(rel_impl_is_partial_order 0
(rel_impl_is_partial_order-1 nil 3570351379
("" (expand "partial_order?" )
(("" (prop)
(("1" (expand "preorder?" )
(("1" (prop)
(("1" (expand "reflexive?" )
(("1" (skolem-typepred)
(("1" (expand "|-" )
(("1" (skolem!) (("1" (flatten) nil nil )) nil )) nil ))
nil ))
nil )
("2" (expand "transitive?" )
(("2" (skolem!)
(("2" (flatten)
(("2" (expand "|-" )
(("2" (skolem!)
(("2" (inst?)
(("2" (inst?) (("2" (prop) nil nil )) nil )) nil ))
nil ))
nil ))
nil ))
nil ))
nil ))
nil ))
nil )
("2" (expand "antisymmetric?" )
(("2" (skolem!)
(("2" (flatten)
(("2" (expand "|-" )
(("2" (apply-extensionality :hide? t)
(("2" (inst?)
(("2" (inst?)
(("2" (iff) (("2" (prop) nil nil )) nil )) nil ))
nil ))
nil ))
nil ))
nil ))
nil ))
nil ))
nil ))
nil )
((\|- const-decl "bool" relation_implication nil )
(reflexive? const-decl "bool" relations nil )
(U formal-nonempty-type-decl nil relation_implication nil )
(T formal-nonempty-type-decl nil relation_implication nil )
(transitive? const-decl "bool" relations nil )
(preorder? const-decl "bool" orders nil )
(pred type-eq-decl nil defined_types nil )
(bool nonempty-type-eq-decl nil booleans nil )
(boolean nonempty-type-decl nil booleans nil )
(antisymmetric? const-decl "bool" relations nil )
(partial_order? const-decl "bool" orders nil ))
shostak))
(double_impl_is_equivalence 0
(double_impl_is_equivalence-1 nil 3570774215
("" (expand "equivalence?" )
(("" (prop)
(("1" (expand "reflexive?" )
(("1" (skolem!)
(("1" (expand "|=" )
(("1" (prop)
(("1" (expand "|-" )
(("1" (skolem!) (("1" (prop) nil nil )) nil )) nil )
("2" (expand "|-" )
(("2" (skolem!) (("2" (prop) nil nil )) nil )) nil ))
nil ))
nil ))
nil ))
nil )
("2" (expand "symmetric?" )
(("2" (skolem!)
(("2" (prop) (("2" (expand "|=" ) (("2" (prop) nil nil )) nil ))
nil ))
nil ))
nil )
("3" (expand "transitive?" )
(("3" (skolem!)
(("3" (flatten)
(("3" (expand "|=" )
(("3" (expand "|-" )
(("3" (prop)
(("1" (skolem!)
(("1" (inst?)
(("1" (inst?)
(("1" (inst?)
(("1" (inst?) (("1" (prop) nil nil )) nil ))
nil ))
nil ))
nil ))
nil )
("2" (skolem!)
(("2" (inst?)
(("2" (inst?)
(("2" (inst?)
(("2" (inst?) (("2" (prop) nil nil )) nil ))
nil ))
nil ))
nil ))
nil ))
nil ))
nil ))
nil ))
nil ))
nil ))
nil ))
nil ))
nil )
((\|- const-decl "bool" relation_implication nil )
(\|= const-decl "bool" relation_implication nil )
(reflexive? const-decl "bool" relations nil )
(symmetric? const-decl "bool" relations nil )
(U formal-nonempty-type-decl nil relation_implication nil )
(T formal-nonempty-type-decl nil relation_implication nil )
(transitive? const-decl "bool" relations nil )
(equivalence? const-decl "bool" relations nil ))
shostak))
(turnstile_TCC1 0
(turnstile_TCC1-1 nil 3570774066
("" (judgement-tcc)
(("" (apply-extensionality :hide? t)
(("" (inst?)
(("" (inst?) (("" (iff) (("" (prop) nil nil )) nil )) nil )) nil ))
nil ))
nil )
((boolean nonempty-type-decl nil booleans nil )
(bool nonempty-type-eq-decl nil booleans nil )
(pred type-eq-decl nil defined_types nil )
(U formal-nonempty-type-decl nil relation_implication nil )
(T formal-nonempty-type-decl nil relation_implication nil )
(partial_order? const-decl "bool" orders nil )
(antisymmetric? const-decl "bool" relations nil )
(preorder? const-decl "bool" orders nil )
(transitive? const-decl "bool" relations nil )
(reflexive? const-decl "bool" relations nil )
(\|- const-decl "bool" relation_implication nil ))
nil ))
(models_TCC1 0
(models_TCC1-1 nil 3570774066 ("" (judgement-tcc) nil nil )
((U formal-nonempty-type-decl nil relation_implication nil )
(T formal-nonempty-type-decl nil relation_implication nil )
(\|- const-decl "bool" relation_implication nil )
(\|= const-decl "bool" relation_implication nil )
(reflexive? const-decl "bool" relations nil )
(symmetric? const-decl "bool" relations nil )
(transitive? const-decl "bool" relations nil )
(equivalence? const-decl "bool" relations nil ))
nil )))
quality 100%
¤ 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.0.18Bemerkung:
(vorverarbeitet)
¤
*© Formatika GbR, Deutschland