|
(max_bounded_posnat
(bnd_TCC1 0
(bnd_TCC1-1 nil 3507028515
(""
(inst +
"(LAMBDA (S: {A: (nonempty?[posnat]) | EXISTS x: FORALL (y: (A)): y <= x}): choose({ a | FORALL (x: (S)): x <= a}))")
(("" (skosimp*)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (expand "member")
(("" (typepred "S!1")
(("" (skosimp*) (("" (inst -3 "x!1") nil))))))))))))))
nil)
((empty? const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(member const-decl "bool" sets nil)
(choose const-decl "(p)" sets nil) (<= const-decl "bool" reals 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))
(max_rec_TCC1 0
(max_rec_TCC1-1 nil 3507028515
("" (skosimp*) (("" (typepred "i!1") (("" (assert) nil)))) nil)
((<= const-decl "bool" reals nil) (choose const-decl "(p)" sets nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(posnat nonempty-type-eq-decl nil integers 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)
(> const-decl "bool" reals 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(max_rec_TCC2 0
(max_rec_TCC2-1 nil 3507028515
("" (skosimp*) (("" (typepred "i!1") (("" (assert) nil)))) nil)
((<= const-decl "bool" reals nil) (choose const-decl "(p)" sets nil)
(nonempty? const-decl "bool" sets nil)
(set type-eq-decl nil sets nil)
(posnat nonempty-type-eq-decl nil integers 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)
(> const-decl "bool" reals 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(max_rec_TCC3 0
(max_rec_TCC3-1 nil 3507028515
("" (skosimp*) (("" (assert) nil)) nil)
((int_minus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(max_rec_in 0
(max_rec_in-1 nil 3507028515
("" (induct "m")
(("1" (skosimp*)
(("1" (case-replace "n!1 = choose(S!1)")
(("1" (expand "max_rec") (("1" (propax) nil)))
("2" (assert) nil)))))
("2" (skosimp*)
(("2" (expand "max_rec" 1)
(("2" (inst?) (("1" (assert) nil) ("2" (assert) nil)))))))
("3" (hide 2) (("3" (skosimp*) nil))))
nil)
((real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(n!1 skolem-const-decl "posnat" max_bounded_posnat nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(nat_induction formula-decl nil naturalnumbers nil)
(max_rec def-decl "posnat" max_bounded_posnat nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(choose const-decl "(p)" sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals 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)
(pred type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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))
(max_rec_bnd 0
(max_rec_bnd-1 nil 3507028515
("" (induct "m")
(("1" (skosimp*)
(("1" (expand "max_rec")
(("1" (lift-if) (("1" (ground) nil)))))))
("2" (skosimp*)
(("2" (expand "max_rec" 1)
(("2" (lift-if)
(("2" (ground) (("2" (inst?) (("2" (assert) nil)))))))))))
("3" (hide 2) (("3" (skosimp*) nil))))
nil)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nat_induction formula-decl nil naturalnumbers nil)
(max_rec def-decl "posnat" max_bounded_posnat nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(choose const-decl "(p)" sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals 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)
(pred type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(int_minus_int_is_int application-judgement "int" integers nil))
nil))
(max_TCC1 0
(max_TCC1-1 nil 3507028515
(""
(inst +
"(LAMBDA (S: {A: (nonempty?[posnat]) | EXISTS x: FORALL (y: (A)): y <= x}): max_rec(S,bnd(S)))")
(("1" (skosimp*)
(("1" (typepred "bnd(S!1)")
(("1" (inst - "choose[posnat](S!1)")
(("1" (lemma "max_rec_in")
(("1" (inst?)
(("1" (inst -1 "bnd(S!1) - choose(S!1)")
(("1" (assert)
(("1" (skosimp*)
(("1" (lemma "max_rec_bnd")
(("1" (inst?)
(("1" (inst - "bnd(S!1) - x!1")
(("1" (assert)
(("1" (typepred "bnd(S!1)")
(("1"
(inst - "x!1")
(("1" (assert) nil)))))))
("2" (typepred "bnd(S!1)")
(("2" (inst - "x!1")
(("2" (assert) nil)))))))))))))))
("2" (assert) nil)))))))))))))
("2" (skosimp*)
(("2" (typepred "bnd(S!1)")
(("2" (inst - "choose(S!1)") (("2" (assert) nil))))))))
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)
(max_rec_bnd formula-decl nil max_bounded_posnat nil)
(x!1 skolem-const-decl "posnat" max_bounded_posnat nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(S!1 skolem-const-decl
"{A: (nonempty?[posnat]) | EXISTS x: FORALL (y: (A)): y <= x}"
max_bounded_posnat nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(max_rec_in formula-decl nil max_bounded_posnat nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bnd const-decl "{a | FORALL (x: (S)): x <= a}" max_bounded_posnat
nil)
(max_rec def-decl "posnat" max_bounded_posnat nil)
(choose const-decl "(p)" sets nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals 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))
(max_def 0
(max_def-1 nil 3507028515
("" (skosimp*)
(("" (prop)
(("1" (expand "maximum?")
(("1" (assert)
(("1" (skosimp*)
(("1" (assert)
(("1" (replace -1 * rl)
(("1" (hide -1)
(("1" (typepred "max(S!1)")
(("1" (inst?) (("1" (assert) nil)))))))))))))))))
("2" (expand "maximum?")
(("2" (flatten)
(("2" (typepred "max(S!1)")
(("2" (inst -3 "a!1")
(("2" (inst -5 "max(S!1)")
(("2" (assert) nil))))))))))))))
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)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(> const-decl "bool" reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(max const-decl
"{a: posnat | S(a) AND (FORALL x: S(x) IMPLIES x <= a)}"
max_bounded_posnat nil)
(maximum? const-decl "bool" max_bounded_posnat nil))
nil))
(max_lem 0
(max_lem-1 nil 3507028515
("" (skosimp*)
(("" (lemma "max_def") (("" (inst?) (("" (assert) nil)))))) nil)
((max_def formula-decl nil max_bounded_posnat nil)
(max const-decl
"{a: posnat | S(a) AND (FORALL x: S(x) IMPLIES x <= a)}"
max_bounded_posnat nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals 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))
(max_in 0
(max_in-1 nil 3507028515 ("" (skosimp*) (("" (assert) nil)) nil) nil
nil)))
¤ 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.
|
