|
(well_foundedness
(no_infinite_descending_sequence 0
(no_infinite_descending_sequence-1 nil 3318615614
("" (skolem!)
(("" (expand* "empty?" "member" "descending?" "well_founded?")
(("" (prop)
(("1" (skolem!)
(("1" (inst - "LAMBDA x: EXISTS n: x = x!1(n)")
(("1" (split)
(("1" (skosimp* t)
(("1" (replace -2 :hide? t)
(("1" (inst - "x!1(1 + n!1)")
(("1" (inst?) nil nil) ("2" (inst?) nil nil)) nil))
nil))
nil)
("2" (inst + "x!1(0)") (("2" (inst?) nil nil)) nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (rewrite "skolemize_forall[(p!1), (p!1)]")
(("2" (skolem!)
(("2" (inst - "LAMBDA n: iterate(f!1, n)(y!1)")
(("2" (skolem!)
(("2" (expand "iterate" 1 1) (("2" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((member const-decl "bool" sets nil)
(well_founded? const-decl "bool" orders nil)
(descending? const-decl "bool" monotone_sequences nil)
(empty? const-decl "bool" sets nil)
(iterate def-decl "T" function_iterate nil)
(y!1 skolem-const-decl "T" well_foundedness nil)
(p!1 skolem-const-decl "pred[T]" well_foundedness nil)
(skolemize_forall formula-decl nil skolemization nil)
(n!1 skolem-const-decl "nat" well_foundedness nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(x!1 skolem-const-decl "sequence[T]" well_foundedness nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(sequence type-eq-decl nil sequences nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil well_foundedness nil))
shostak))
(well_founded_is_irreflexive 0
(well_founded_is_irreflexive-1 nil 3318615593
("" (skolem-typepred)
(("" (rewrite "no_infinite_descending_sequence")
(("" (expand* "empty?" "member" "descending?" "irreflexive?")
(("" (skolem!)
(("" (inst - "LAMBDA n: x!2") (("" (skolem!) nil nil)) nil))
nil))
nil))
nil))
nil)
((no_infinite_descending_sequence formula-decl nil well_foundedness
nil)
(sequence type-eq-decl nil sequences nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(empty? const-decl "bool" sets nil)
(descending? const-decl "bool" monotone_sequences nil)
(irreflexive? const-decl "bool" relations nil)
(member const-decl "bool" sets nil)
(well_founded? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil well_foundedness nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(well_order_is_well_founded_order 0
(well_order_is_well_founded_order-1 nil 3318615593
("" (judgement-tcc) 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 well_foundedness nil)
(pred type-eq-decl nil defined_types nil)
(well_ordered? const-decl "bool" orders nil)
(strict_total_order? const-decl "bool" orders nil)
(trichotomous? const-decl "bool" orders nil)
(strict_order? const-decl "bool" orders nil)
(irreflexive? const-decl "bool" relations nil)
(well_founded? const-decl "bool" orders nil)
(transitive? const-decl "bool" relations nil)
(well_founded_order? const-decl "bool" well_foundedness nil))
nil))
(well_founded_order_is_well_founded 0
(well_founded_order_is_well_founded-1 nil 3318615593
("" (judgement-tcc) 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 well_foundedness nil)
(pred type-eq-decl nil defined_types nil)
(well_founded_order? const-decl "bool" well_foundedness nil)
(transitive? const-decl "bool" relations nil)
(well_founded? const-decl "bool" orders nil))
nil))
(well_founded_order_is_strict_order 0
(well_founded_order_is_strict_order-1 nil 3318615593
("" (skolem-typepred)
(("" (expand* "strict_order?" "well_founded_order?")
(("" (prop)
(("" (rewrite "well_founded_is_irreflexive") nil nil)) nil))
nil))
nil)
((strict_order? const-decl "bool" orders nil)
(well_founded_is_irreflexive judgement-tcc nil well_foundedness
nil)
(well_founded? const-decl "bool" orders nil)
(well_founded_order? const-decl "bool" well_foundedness nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil well_foundedness nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(transitive_closure_preserves_well_foundedness 0
(transitive_closure_preserves_well_foundedness-1 nil 3318615593
("" (skolem-typepred)
(("" (expand* "well_founded_order?" "well_founded?")
(("" (skosimp*)
((""
(inst -
"LAMBDA (y: T): EXISTS (x: T): preorder_closure[T](rel!1)(x, y) & p!1(x)")
(("" (prop)
(("1" (skosimp* t)
(("1" (rewrite "preorder_closure_reflexive_transitive")
(("1" (expand* "reflexive_closure" "union" "member")
(("1" (split)
(("1" (hide 1)
(("1" (rewrite "transitive_closure_step_r")
(("1" (expand "o")
(("1" (skosimp)
(("1" (inst - "y!3")
(("1"
(inst + "x!1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst + "x!1")
(("2" (skolem!)
(("2" (rewrite "transitive_closure_step_r")
(("2" (expand "o")
(("2" (skosimp)
(("2"
(inst - "y!3")
(("1" (assert) nil nil)
("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst? 2)
(("2" (skolem!)
(("2" (inst + "y!1")
(("2" (inst + "x!1")
(("2"
(expand* "preorder_closure" "transitive_closure"
"IUnion")
(("2" (skolem!) (("2" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((well_founded_order? const-decl "bool" well_foundedness nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(preorder? const-decl "bool" orders nil)
(preorder_closure const-decl "(preorder?)" closure_ops nil)
(y!1 skolem-const-decl "T" well_foundedness nil)
(transitive_closure const-decl "(transitive?)" closure_ops nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(union const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(x!1 skolem-const-decl "T" well_foundedness nil)
(y!3 skolem-const-decl "T" well_foundedness nil)
(O const-decl "bool" relation_props nil)
(rel!1 skolem-const-decl "(well_founded?[T])" well_foundedness nil)
(y!3 skolem-const-decl "T" well_foundedness nil)
(p!1 skolem-const-decl "pred[T]" well_foundedness nil)
(transitive_closure_step_r formula-decl nil closure_ops nil)
(reflexive_closure_preserves_transitive application-judgement
"(preorder?)" well_foundedness nil)
(preorder_closure_reflexive_transitive formula-decl nil closure_ops
nil)
(well_founded? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil well_foundedness nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil)))
¤ Dauer der Verarbeitung: 0.17 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.
|
