|
(monotone_sequences
(reflexive_closure_ascending 0
(reflexive_closure_ascending-1 nil 3314543892
("" (skolem-typepred)
(("" (expand* "ascending?" "reflexive_closure" "union" "member")
(("" (skosimp) (("" (inst?) nil nil)) nil)) nil))
nil)
((reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(member const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(ascending? const-decl "bool" monotone_sequences 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)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil monotone_sequences nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(reflexive_closure_descending 0
(reflexive_closure_descending-1 nil 3314543932
("" (skolem-typepred)
(("" (expand* "descending?" "reflexive_closure" "union" "member")
(("" (skosimp) (("" (inst?) nil nil)) nil)) nil))
nil)
((reflexive_closure const-decl "(reflexive?)" closure_ops nil)
(member const-decl "bool" sets nil)
(union const-decl "set" sets nil)
(descending? const-decl "bool" monotone_sequences 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)
(pred type-eq-decl nil defined_types nil)
(T formal-type-decl nil monotone_sequences nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(ascending_lem 0
(ascending_lem-1 nil 3314543958
("" (skolem-typepred)
(("" (expand* "preserves" "restrict")
(("" (induct "x2")
(("1" (skosimp) (("1" (assert) nil nil)) nil)
("2" (skosimp*)
(("2" (case-replace "x1!1 = j!1")
(("1" (hide -2)
(("1" (expand "ascending?")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
nil)
("2" (inst?)
(("2" (assert)
(("2" (expand "transitive?")
(("2"
(inst - "seq!1(x1!1)" "seq!1(j!1)"
"seq!1(1 + j!1)")
(("2" (assert)
(("2" (hide 2 -1)
(("2" (expand "ascending?")
(("2" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((restrict const-decl "R" restrict nil)
(preserves const-decl "bool" functions nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nat_induction formula-decl nil naturalnumbers nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(< const-decl "bool" reals nil)
(ascending? const-decl "bool" monotone_sequences 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)
(pred type-eq-decl nil defined_types nil)
(transitive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(T formal-type-decl nil monotone_sequences nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(descending_lem 0
(descending_lem-1 nil 3314544287
("" (skolem-typepred)
(("" (rewrite "ascending_lem")
(("" (expand* "ascending?" "converse" "descending?") nil nil))
nil))
nil)
((transitive_converse application-judgement "(transitive?[T])"
relation_converse_props nil)
(ascending_lem formula-decl nil monotone_sequences nil)
(converse const-decl "pred[[T2, T1]]" relation_defs nil)
(ascending? const-decl "bool" monotone_sequences nil)
(strict_total_order_restrict application-judgement
"(strict_total_order?[S])" restrict_order_props nil)
(trichotomous_restrict application-judgement "(trichotomous?[S])"
restrict_order_props nil)
(strict_order_restrict application-judgement "(strict_order?[S])"
restrict_order_props nil)
(transitive_restrict application-judgement "(transitive?[S])"
restrict_order_props nil)
(antisymmetric_restrict application-judgement "(antisymmetric?[S])"
restrict_order_props nil)
(irreflexive_restrict application-judgement "(irreflexive?[S])"
restrict_order_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(descending? const-decl "bool" monotone_sequences 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)
(pred type-eq-decl nil defined_types nil)
(transitive? const-decl "bool" relations nil)
(PRED type-eq-decl nil defined_types nil)
(T formal-type-decl nil monotone_sequences nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(ascending_subsequence 0
(ascending_subsequence-1 nil 3314544355
("" (skolem-typepred)
(("" (lemma "preserves_composition[nat, nat, T]")
(("" (inst?)
(("" (invoke (inst - "%1" "%1" "lt!1") (! -2 0 1))
(("" (expand "preserves" -2)
(("" (assert)
(("" (hide -2)
(("" (split)
(("1" (hide -3)
(("1" (expand* "ascending?" "preserves" "restrict")
(("1" (skolem!)
(("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (rewrite "ascending_lem") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((preserves_composition formula-decl nil function_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(irreflexive_restrict application-judgement "(irreflexive?[S])"
restrict_order_props nil)
(antisymmetric_restrict application-judgement "(antisymmetric?[S])"
restrict_order_props nil)
(transitive_restrict application-judgement "(transitive?[S])"
restrict_order_props nil)
(strict_order_restrict application-judgement "(strict_order?[S])"
restrict_order_props nil)
(trichotomous_restrict application-judgement "(trichotomous?[S])"
restrict_order_props nil)
(strict_total_order_restrict application-judgement
"(strict_total_order?[S])" restrict_order_props nil)
(preserves const-decl "bool" functions nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(ascending_lem formula-decl nil monotone_sequences nil)
(ascending? const-decl "bool" monotone_sequences nil)
(sequence type-eq-decl nil sequences nil)
(pred type-eq-decl nil defined_types nil)
(transitive? const-decl "bool" relations nil)
(T formal-type-decl nil monotone_sequences nil)
(< const-decl "bool" reals nil)
(restrict const-decl "R" restrict nil)
(preserves const-decl "bool" functions nil)
(PRED type-eq-decl nil defined_types 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)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(descending_subsequence 0
(descending_subsequence-1 nil 3314544571
("" (skolem-typepred)
(("" (use "ascending_subsequence" ("lt" "converse(lt!1)"))
(("1" (expand* "ascending?" "converse" "descending?") nil nil)
("2" (expand* "ascending?" "converse" "descending?") nil nil))
nil))
nil)
((converse const-decl "pred[[T2, T1]]" relation_defs nil)
(ascending_subsequence formula-decl nil monotone_sequences nil)
(transitive_converse application-judgement "(transitive?[T])"
relation_converse_props nil)
(seq!1 skolem-const-decl "(descending?(lt!1))" monotone_sequences
nil)
(lt!1 skolem-const-decl "(transitive?[T])" monotone_sequences nil)
(ascending? const-decl "bool" monotone_sequences nil)
(descending? const-decl "bool" monotone_sequences nil)
(sequence type-eq-decl nil sequences nil)
(pred type-eq-decl nil defined_types nil)
(transitive? const-decl "bool" relations nil)
(T formal-type-decl nil monotone_sequences nil)
(< const-decl "bool" reals nil)
(restrict const-decl "R" restrict nil)
(preserves const-decl "bool" functions nil)
(PRED type-eq-decl nil defined_types 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)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak)))
¤ Dauer der Verarbeitung: 0.23 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.
|
