|
(min_posnat
(min_TCC1 0
(min_TCC1-1 nil 3507028515
(""
(inst +
"lambda S : choose({a : posnat | S(a) AND (FORALL (x : posnat) : S(x) IMPLIES a <= x)})")
(("" (skosimp*)
(("" (typepred "S!1")
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (expand "member")
(("" (skosimp*)
(("" (lemma "wf_nat")
(("" (expand "well_founded?")
(("" (inst - "S!1")
(("" (split -1)
(("1" (assert)
(("1" (skosimp*)
(("1" (typepred "y!1")
(("1"
(expand "extend")
(("1"
(inst -4 "y!1")
(("1"
(ground)
(("1"
(skosimp*)
(("1"
(inst - "x!2")
(("1" (assert) nil)
("2"
(expand "extend")
(("2" (propax) nil)))))))))
("2" (ground) nil)))))))))))
("2" (inst?)
(("2" (assert)
(("2" (grind) nil))))))))))))))))))))))))))
nil)
((member const-decl "bool" sets nil)
(wf_nat formula-decl nil naturalnumbers nil)
(extend const-decl "R" extend nil)
(FALSE const-decl "bool" booleans nil)
(pred type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(S!1 skolem-const-decl "(nonempty?[posnat])" min_posnat nil)
(y!1 skolem-const-decl "(extend[nat, posnat, bool, FALSE](S!1))"
min_posnat nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(x!2 skolem-const-decl "posnat" min_posnat nil)
(nonempty_extend application-judgement "(nonempty?[T])"
extend_set_props nil)
(well_founded? const-decl "bool" orders nil)
(empty? const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(choose const-decl "(p)" sets nil) (<= const-decl "bool" reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil))
(min_def 0
(min_def-1 nil 3507028515
("" (skolem-typepred)
(("" (typepred "min(S!1)")
(("" (prop)
(("1" (expand "minimum?")
(("1" (assert)
(("1" (skosimp*) (("1" (inst?) (("1" (assert) nil)))))))))
("2" (expand "minimum?")
(("2" (flatten)
(("2" (inst -5 "a!1")
(("2" (assert)
(("2" (inst -2 "min(S!1)")
(("2" (assert) nil))))))))))))))))
nil)
((min const-decl
"{a: posnat | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}"
min_posnat nil)
(<= const-decl "bool" reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(minimum? const-decl "bool" min_posnat nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers 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))
nil))
(min_lem 0
(min_lem-1 nil 3507028515
("" (skosimp*)
(("" (lemma "min_def") (("" (inst?) (("" (assert) nil)))))) nil)
((min_def formula-decl nil min_posnat nil)
(min const-decl
"{a: posnat | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}"
min_posnat nil)
(<= const-decl "bool" reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers 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.
|
