|
(extended_nnreal
(x_inf_TCC1 0
(x_inf_TCC1-1 nil 3396791560
("" (skosimp*)
(("" (split)
(("1" (expand "nonempty?")
(("1" (expand "empty?")
(("1" (expand "member")
(("1" (inst - "x!1`2")
(("1" (inst + "x!1") (("1" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
("2" (expand "bounded_below?")
(("2" (inst + "0")
(("2" (expand "lower_bound?")
(("2" (skosimp)
(("2" (typepred "s!1")
(("2" (skosimp) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((empty? const-decl "bool" sets nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal nil)
(set type-eq-decl nil sets nil) (member const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(lower_bound? const-decl "bool" bounded_real_defs nil)
(bounded_below? const-decl "bool" bounded_real_defs nil))
nil))
(x_inf_TCC2 0
(x_inf_TCC2-1 nil 3396791560
("" (skosimp*)
(("" (lemma "x_inf_TCC1" ("X" "X!1"))
(("" (split -1)
(("1" (flatten)
(("1"
(typepred
"glb({z | EXISTS x: X!1(x) AND x`1 AND x`2 = z})")
(("1"
(name-replace "GLB"
"glb({zz:real | EXISTS y: X!1(y) AND y`1 AND y`2 = zz})")
(("1" (expand "greatest_lower_bound?")
(("1" (flatten)
(("1" (inst - "0")
(("1" (assert)
(("1" (hide 2)
(("1" (expand "lower_bound?")
(("1" (skosimp)
(("1" (typepred "s!1")
(("1"
(skosimp)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2" (inst - "x!1") nil nil))
nil))
nil))
nil)
((set type-eq-decl nil sets nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal nil)
(nnreal type-eq-decl nil real_types 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)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(x_inf_TCC1 subtype-tcc nil extended_nnreal nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(lower_bound? const-decl "bool" bounded_real_defs nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(nonempty? const-decl "bool" sets nil)
(greatest_lower_bound? const-decl "bool" bounded_real_defs nil)
(bounded_below? const-decl "bool" bounded_real_defs nil)
(glb const-decl "{x | greatest_lower_bound?(x, SB)}"
bounded_real_defs nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil))
nil))
(x_sup_TCC1 0
(x_sup_TCC1-1 nil 3431062706
("" (skosimp*)
(("" (expand "empty?")
(("" (skosimp)
(("" (expand "member")
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (expand "member")
(("" (inst - "x!1`2")
(("" (inst + "x!1")
(("" (inst + "x!1") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal nil)
(set type-eq-decl nil sets nil)
(X!1 skolem-const-decl "set[extended_nnreal]" extended_nnreal nil)
(x!1 skolem-const-decl "extended_nnreal" extended_nnreal nil)
(nonempty? const-decl "bool" sets nil))
nil))
(x_sup_TCC2 0
(x_sup_TCC2-1 nil 3431062706
("" (skosimp*)
(("" (replace -1)
(("" (lemma "x_sup_TCC1" ("X" "X!1"))
(("" (replace 3) (("" (replace 2) (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
((x_sup_TCC1 subtype-tcc nil extended_nnreal nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil 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)
(nnreal type-eq-decl nil real_types nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal nil)
(set type-eq-decl nil sets nil))
nil))
(x_sup_TCC3 0
(x_sup_TCC3-1 nil 3431063075
("" (skosimp*)
(("" (lemma "x_sup_TCC2" ("X" "X!1"))
(("" (replace -2)
(("" (replace 1)
(("" (replace 2)
((""
(typepred
"lub({z | EXISTS x: X!1(x) AND x`1 AND x`2 = z})")
(("1" (expand "least_upper_bound?")
(("1"
(name-replace "LUB"
"lub({z | EXISTS x: X!1(x) AND x`1 AND x`2 = z})")
(("1" (flatten)
(("1" (expand "empty?")
(("1" (hide 1 2 -4)
(("1" (expand "nonempty?")
(("1" (expand "empty?")
(("1" (expand "member")
(("1"
(skosimp)
(("1"
(skosimp)
(("1"
(expand "upper_bound?")
(("1"
(hide -2)
(("1"
(inst - "x!1")
(("1" (assert) nil nil)
("2"
(inst + "x!2")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((set type-eq-decl nil sets nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal nil)
(nnreal type-eq-decl nil real_types 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)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(x_sup_TCC2 subtype-tcc nil extended_nnreal nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(lub const-decl "{x | least_upper_bound?(x, SA)}" bounded_real_defs
nil)
(bounded_above? const-decl "bool" bounded_real_defs nil)
(least_upper_bound? const-decl "bool" bounded_real_defs nil)
(nonempty? const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets 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)
(x!1 skolem-const-decl "real" extended_nnreal nil)
(X!1 skolem-const-decl "set[extended_nnreal]" extended_nnreal nil)
(upper_bound? const-decl "bool" bounded_real_defs nil))
nil))
(x_sigma_TCC1 0
(x_sigma_TCC1-1 nil 3396791560 ("" (subtype-tcc) nil nil) nil nil))
(x_sum_TCC1 0
(x_sum_TCC1-1 nil 3396590282
("" (skosimp*)
(("" (lemma "limit_nonneg" ("nna" "series(LAMBDA i: S!1(i)`2)"))
(("1" (assert)
(("1" (expand "series")
(("1" (expand "limit")
(("1" (expand "limit") (("1" (propax) nil nil)) nil)) nil))
nil))
nil)
("2" (expand "series")
(("2" (hide-all-but 1)
(("2" (skosimp)
(("2"
(lemma "sigma_ge_0"
("low" "0" "high" "x1!1" "F" "LAMBDA i: S!1(i)`2"))
(("2" (split -1)
(("1" (propax) nil nil)
("2" (hide 2)
(("2" (skosimp) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((extended_nnreal nonempty-type-eq-decl nil extended_nnreal nil)
(series const-decl "sequence[real]" series "series/")
(sequence type-eq-decl nil sequences nil)
(nnreal type-eq-decl nil real_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)
(limit_nonneg formula-decl nil series_lems "series/")
(limit const-decl "real" convergence_sequences "analysis/")
(limit macro-decl "[(convergent?) -> real]" extended_nnreal nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(T_low type-eq-decl nil sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(<= const-decl "bool" reals nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(sigma_ge_0 formula-decl nil sigma "reals/"))
nil))
(x_sum_TCC2 0
(x_sum_TCC2-1 nil 3454502638
("" (skosimp)
(("" (lemma "limit_nonneg" ("nna" "series(U!1)"))
(("1" (assert)
(("1" (expand "limit" 1) (("1" (propax) nil nil)) nil)) nil)
("2" (hide-all-but 1)
(("2" (skolem + "n!1")
(("2" (expand "series")
(("2"
(lemma "sigma_ge_0" ("low" "0" "high" "n!1" "F" "U!1"))
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((series const-decl "sequence[real]" series "series/")
(sequence type-eq-decl nil sequences nil)
(nnreal type-eq-decl nil real_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)
(limit_nonneg formula-decl nil series_lems "series/")
(limit macro-decl "[(convergent?) -> real]" extended_nnreal nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(T_low type-eq-decl nil sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(<= const-decl "bool" reals nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(sigma_ge_0 formula-decl nil sigma "reals/")
(sigma_nnreal application-judgement "nnreal" sigma_nat "reals/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(x_limit_TCC1 0
(x_limit_TCC1-1 nil 3450168447
("" (skosimp)
(("" (lemma "limit_nonneg" ("nna" "LAMBDA i: S!1(i)`2"))
(("" (assert)
(("" (expand "limit" 1) (("" (propax) nil nil)) nil)) nil))
nil))
nil)
((extended_nnreal nonempty-type-eq-decl nil extended_nnreal nil)
(sequence type-eq-decl nil sequences nil)
(nnreal type-eq-decl nil real_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)
(limit_nonneg formula-decl nil series_lems "series/")
(limit macro-decl "[(convergent?) -> real]" extended_nnreal nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(x_add_commutative 0
(x_add_commutative-1 nil 3396582760
("" (expand "x_add")
(("" (expand "commutative?")
(("" (skosimp*) (("" (grind) nil nil)) nil)) nil))
nil)
((commutative? const-decl "bool" operator_defs nil)
(x_add const-decl "extended_nnreal" extended_nnreal nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil))
shostak))
(x_add_associative 0
(x_add_associative-1 nil 3396582779
("" (expand "x_add")
(("" (expand "associative?") (("" (grind) nil nil)) nil)) nil)
((associative? const-decl "bool" operator_defs nil)
(x_add const-decl "extended_nnreal" extended_nnreal nil)
(nnreal_plus_nnreal_is_nnreal application-judgement "nnreal"
real_types nil))
shostak))
(x_times_commutative 0
(x_times_commutative-1 nil 3457152809
("" (expand "commutative?")
(("" (expand "x_times") (("" (grind) nil nil)) nil)) nil)
((x_times const-decl "extended_nnreal" extended_nnreal nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(x_eq const-decl "bool" extended_nnreal nil)
(commutative? const-decl "bool" operator_defs nil))
shostak))
(x_times_associative 0
(x_times_associative-1 nil 3457152828
("" (expand "associative?")
(("" (grind)
(("1" (rewrite "zero_times3") nil nil)
("2" (rewrite "zero_times3") nil nil))
nil))
nil)
((x_eq const-decl "bool" extended_nnreal nil)
(x_times const-decl "extended_nnreal" extended_nnreal nil)
(nnreal_times_nnreal_is_nnreal application-judgement "nnreal"
real_types nil)
(real_times_real_is_real application-judgement "real" reals nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal nil)
(nnreal type-eq-decl nil real_types nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(zero_times3 formula-decl nil real_props nil)
(associative? const-decl "bool" operator_defs nil))
shostak))
(x_eq_equivalence 0
(x_eq_equivalence-1 nil 3396582792
("" (expand "x_eq")
(("" (expand "equivalence?") (("" (grind) nil nil)) nil)) nil)
((equivalence? const-decl "bool" relations nil)
(reflexive? const-decl "bool" relations nil)
(symmetric? const-decl "bool" relations nil)
(transitive? const-decl "bool" relations nil)
(x_eq const-decl "bool" extended_nnreal nil))
shostak))
(x_le_preorder 0
(x_le_preorder-1 nil 3396582803
("" (expand "x_le")
(("" (expand "preorder?") (("" (grind) nil nil)) nil)) nil)
((preorder? const-decl "bool" orders nil)
(reflexive? const-decl "bool" relations nil)
(transitive? const-decl "bool" relations nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(x_le const-decl "bool" extended_nnreal nil))
shostak))
(x_le_antisymmetric 0
(x_le_antisymmetric-1 nil 3396582814
("" (expand "x_eq")
(("" (expand "x_le") (("" (grind) nil nil)) nil)) nil)
((x_le const-decl "bool" extended_nnreal nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(x_eq const-decl "bool" extended_nnreal nil))
shostak))
(x_sigma_le 0
(x_sigma_le-1 nil 3397794298
("" (skosimp*)
(("" (expand "x_sigma")
(("" (expand "x_le")
((""
(case-replace
"FORALL i: low!1 <= i AND i <= high!1 => T!1(i)`1")
(("1"
(case-replace
"FORALL (i_1: nat): low!1 <= i_1 AND i_1 <= high!1 => S!1(i_1)`1")
(("1"
(lemma "sigma_le"
("low" "low!1" "high" "high!1" "F"
"LAMBDA (i_2: nat): S!1(i_2)`2" "G"
"LAMBDA (i_2: nat): T!1(i_2)`2"))
(("1" (split -1)
(("1" (propax) nil nil)
("2" (hide 2)
(("2" (skosimp)
(("2" (typepred "n!1")
(("2" (inst - "n!1")
(("2" (inst - "n!1")
(("2" (inst - "n!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp)
(("2" (inst - "i!1")
(("2" (inst - "i!1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (replace 1 2) (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
((x_sigma const-decl "extended_nnreal" extended_nnreal nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal nil)
(T_low type-eq-decl nil sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(OR const-decl "[bool, bool -> bool]" booleans nil)
(sigma_le formula-decl nil sigma "reals/")
(NOT const-decl "[bool -> bool]" booleans nil)
(subrange type-eq-decl nil integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(x_le const-decl "bool" extended_nnreal nil))
shostak))
(x_sigma_lt 0
(x_sigma_lt-1 nil 3397794729
("" (skosimp)
(("" (expand "x_sigma")
(("" (expand "x_lt")
((""
(case-replace
"FORALL i: low!1 <= i AND i <= high!1 => T!1(i)`1")
(("1"
(case-replace
"FORALL (i_1: nat): low!1 <= i_1 AND i_1 <= high!1 => S!1(i_1)`1")
(("1"
(lemma "sigma_lt"
("low" "low!1" "high" "high!1" "F"
"LAMBDA (i_1: nat): S!1(i_1)`2" "G"
"LAMBDA (i_1: nat): T!1(i_1)`2"))
(("1" (split -1)
(("1" (propax) nil nil) ("2" (propax) nil nil)
("3" (hide 2)
(("3" (skosimp)
(("3" (typepred "n!1")
(("3" (inst - "n!1")
(("3" (inst - "n!1")
(("3" (inst - "n!1") (("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp)
(("2" (inst - "i!1")
(("2" (inst - "i!1") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (replace 1 2) (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
((x_sigma const-decl "extended_nnreal" extended_nnreal nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(nnreal type-eq-decl nil real_types nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal nil)
(T_low type-eq-decl nil sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(OR const-decl "[bool, bool -> bool]" booleans nil)
(sigma_lt formula-decl nil sigma "reals/")
(NOT const-decl "[bool -> bool]" booleans nil)
(subrange type-eq-decl nil integers 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_lt const-decl "bool" extended_nnreal nil))
shostak))
(x_sum_le 0
(x_sum_le-1 nil 3397795096
("" (skosimp)
(("" (expand "x_le")
(("" (expand "x_sum")
((""
(case-replace "(FORALL i: T!1(i)`1) AND
convergent?(series(LAMBDA i: T!1(i)`2))")
(("1"
(case-replace "(FORALL (i_1: nat): S!1(i_1)`1) AND
convergent?(series(LAMBDA (i_1: nat): S!1(i_1)`2))")
(("1" (flatten)
(("1"
(name "F" "LAMBDA (i_2: nat): T!1(i_2)`2-S!1(i_2)`2")
(("1" (case "forall i: 0<=F(i)")
(("1"
(case "series(F)= series(LAMBDA i: T!1(i)`2)-series(LAMBDA (i_1: nat): S!1(i_1)`2)")
(("1"
(lemma "convergent_diff"
("s1" "series(LAMBDA i: T!1(i)`2)" "s2"
"series(LAMBDA (i_1: nat): S!1(i_1)`2)"))
(("1" (replace -2 -1 rl)
(("1" (assert)
(("1"
(lemma "limit_diff"
("v1" "series(LAMBDA i: T!1(i)`2)" "v2"
"series(LAMBDA (i_1: nat): S!1(i_1)`2)"))
(("1" (replace -3 -1 rl)
(("1"
(name-replace
"L1"
"convergence_sequences.limit(series(LAMBDA (i_2: nat): S!1(i_2)`2))")
(("1"
(name-replace
"L2"
"convergence_sequences.limit(series(LAMBDA (i_1: nat): T!1(i_1)`2))")
(("1"
(lemma
"limit_nonneg"
("nna" "series(F)"))
(("1" (assert) nil nil)
("2"
(skolem + ("n!1"))
(("2"
(hide-all-but (-4 1))
(("2"
(expand "series")
(("2"
(lemma
"sigma_ge_0"
("low"
"0"
"high"
"n!1"
"F"
"F"))
(("2"
(assert)
(("2"
(skosimp)
(("2"
(inst - "n!2")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "F")
(("2" (rewrite "series_diff")
(("2" (expand "-") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (skosimp)
(("2" (expand "F" 1)
(("2" (inst - "i!1")
(("2" (inst - "i!1")
(("2" (inst - "i!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (split)
(("1" (skosimp)
(("1" (inst - "i!1")
(("1" (inst - "i!1") (("1" (assert) nil nil)) nil))
nil))
nil)
("2" (flatten)
(("2"
(lemma "comparison_test"
("b" "LAMBDA i: T!1(i)`2" "a"
"LAMBDA (i_1: nat): S!1(i_1)`2"))
(("2" (replace -3)
(("2" (split)
(("1" (propax) nil nil)
("2" (hide -2 2)
(("2" (skosimp)
(("2" (expand "abs")
(("2"
(assert)
(("2"
(typepred "S!1(n!1)`2")
(("2"
(assert)
(("2"
(inst - "n!1")
(("2"
(inst - "n!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace 1 2) (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
((x_le const-decl "bool" extended_nnreal nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, 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)
(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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(nnreal type-eq-decl nil real_types nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal nil)
(sequence type-eq-decl nil sequences nil)
(convergent? const-decl "bool" convergence_sequences "analysis/")
(series const-decl "sequence[real]" series "series/")
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(comparison_test formula-decl nil series "series/")
(<= const-decl "bool" reals nil)
(series_diff formula-decl nil series "series/")
(F skolem-const-decl "[nat -> real]" extended_nnreal nil)
(convergent_diff formula-decl nil convergence_ops "analysis/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_lt_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)
(subrange type-eq-decl nil integers nil)
(T_low type-eq-decl nil sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(OR const-decl "[bool, bool -> bool]" booleans nil)
(sigma_ge_0 formula-decl nil sigma "reals/")
(limit_nonneg formula-decl nil series_lems "series/")
(limit const-decl "real" convergence_sequences "analysis/")
(limit_diff formula-decl nil convergence_ops "analysis/")
(- const-decl "[T -> real]" real_fun_ops "reals/")
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(x_sum const-decl "extended_nnreal" extended_nnreal nil))
shostak))
(x_sum_eq 0
(x_sum_eq-1 nil 3450459000
("" (skosimp)
(("" (lemma "x_sum_le" ("S" "S!1" "T" "T!1"))
(("" (lemma "x_sum_le" ("S" "T!1" "T" "S!1"))
(("" (split)
(("1" (split)
(("1"
(lemma "x_le_antisymmetric"
("x" "x_sum(S!1)" "y" "x_sum(T!1)"))
(("1" (assert) nil nil)) nil)
("2" (hide-all-but (-2 1))
(("2" (skosimp)
(("2" (inst - "i!1")
(("2" (expand "x_le")
(("2" (expand "x_eq")
(("2" (flatten) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but (-2 1))
(("2" (skosimp)
(("2" (inst - "i!1")
(("2" (expand "x_eq")
(("2" (expand "x_le")
(("2" (flatten) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((extended_nnreal nonempty-type-eq-decl nil extended_nnreal nil)
(nnreal type-eq-decl nil real_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)
(x_sum_le formula-decl nil extended_nnreal nil)
(x_eq const-decl "bool" extended_nnreal nil)
(x_le const-decl "bool" extended_nnreal nil)
(x_sum const-decl "extended_nnreal" extended_nnreal nil)
(x_le_antisymmetric formula-decl nil extended_nnreal nil))
shostak))
(x_sum_lt 0
(x_sum_lt-1 nil 3397796467
("" (skosimp)
(("" (expand "x_sum")
(("" (expand "x_lt")
((""
(case-replace "(FORALL i: T!1(i)`1) AND
convergent?(series(LAMBDA i: T!1(i)`2))")
(("1" (flatten)
(("1"
(case-replace "(FORALL (i_1: nat): S!1(i_1)`1) AND
convergent?(series(LAMBDA (i_1: nat): S!1(i_1)`2))")
(("1" (flatten)
(("1"
(name "F"
"series(LAMBDA (i_2: nat): T!1(i_2)`2-S!1(i_2)`2)")
(("1" (case "forall i: F(i)>0")
(("1"
(case "series(LAMBDA (i_2: nat): T!1(i_2)`2)-series(LAMBDA (i_2: nat): S!1(i_2)`2)=F")
(("1"
(lemma "convergent_diff"
("s1" "series(LAMBDA (i_2: nat): T!1(i_2)`2)"
"s2"
"series(LAMBDA (i_2: nat): S!1(i_2)`2)"))
(("1" (replace -2)
(("1" (assert)
(("1"
(lemma "limit_diff"
("v1"
"series(LAMBDA (i_2: nat): T!1(i_2)`2)"
"v2"
"series(LAMBDA (i_2: nat): S!1(i_2)`2)"))
(("1"
(replace -3 -1)
(("1"
(name-replace
"L1"
"convergence_sequences.limit(series(LAMBDA (i_1: nat): S!1(i_1)`2))")
(("1"
(name-replace
"L2"
"convergence_sequences.limit(series(LAMBDA (i_2: nat): T!1(i_2)`2))")
(("1"
(hide -3 -5 -7 -9)
(("1"
(expand "F")
(("1"
(lemma
"limit_series_shift"
("a"
"LAMBDA (i_2: nat): T!1(i_2)`2 - S!1(i_2)`2"
"pn"
"1"))
(("1"
(assert)
(("1"
(replace -2)
(("1"
(lemma
"conv_series_shift"
("a"
"LAMBDA (i_2: nat): T!1(i_2)`2 - S!1(i_2)`2"
"N"
"1"))
(("1"
(assert)
(("1"
(lemma
"limit_pos"
("a"
"series(LAMBDA i: T!1(1 + i)`2 - S!1(1 + i)`2)"))
(("1"
(replace -2)
(("1"
(name-replace
"L3"
"convergence_sequences.limit(series(LAMBDA i: T!1(1 + i)`2 - S!1(1 + i)`2))")
(("1"
(split -1)
(("1"
(expand
"sigma")
(("1"
(inst
-6
"0")
(("1"
(expand
"series"
-6)
(("1"
(expand
"sigma")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(skosimp)
(("2"
(expand
"series"
(1
-5))
(("2"
(lemma
"sigma_gt_0"
("low"
"0"
"high"
"n!1"
"F"
"LAMBDA (i_1: nat): T!1(1 + i_1)`2 - S!1(1 + i_1)`2"))
(("2"
(assert)
(("2"
(hide
-5
2)
(("2"
(skosimp)
(("2"
(typepred
"n!2")
(("2"
(inst
-
"1+n!2")
(("2"
(inst
-
"1+n!2")
(("2"
(inst
-
"1+n!2")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (rewrite "series_diff")
(("2" (expand "F")
(("2" (expand "-") (("2" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (hide -1 -3 -5 2)
(("2" (expand "F")
(("2" (expand "series")
(("2"
(lemma "sigma_gt_0"
("low"
"0"
"high"
"i!1"
"F"
"LAMBDA (i_2: nat): T!1(i_2)`2 - S!1(i_2)`2"))
(("2"
(assert)
(("2"
(hide 2)
(("2"
(skosimp)
(("2"
(typepred "n!1")
(("2"
(inst - "n!1")
(("2"
(inst - "n!1")
(("2"
(inst - "n!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (split)
(("1" (skosimp)
(("1" (inst - "i!1")
(("1" (inst - "i!1") (("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(lemma "comparison_test"
("a" "LAMBDA (i_1: nat): S!1(i_1)`2" "b"
"LAMBDA i: T!1(i)`2"))
(("2" (assert)
(("2" (hide -2 2)
(("2" (skosimp)
(("2" (typepred "S!1(n!1)`2")
(("2" (expand "abs")
(("2"
(assert)
(("2"
(inst - "n!1")
(("2"
(inst - "n!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace 1 2) (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
((x_sum const-decl "extended_nnreal" extended_nnreal nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, 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)
(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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(nnreal type-eq-decl nil real_types nil)
(extended_nnreal nonempty-type-eq-decl nil extended_nnreal nil)
(sequence type-eq-decl nil sequences nil)
(convergent? const-decl "bool" convergence_sequences "analysis/")
(series const-decl "sequence[real]" series "series/")
(real_minus_real_is_real application-judgement "real" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(limit_diff formula-decl nil convergence_ops "analysis/")
(limit const-decl "real" convergence_sequences "analysis/")
(limit_series_shift formula-decl nil series "series/")
(nonneg_int nonempty-type-eq-decl nil integers nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_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)
(sigma_0_neg formula-decl nil sigma_nat "reals/")
(sigma def-decl "real" sigma "reals/")
(sigma_gt_0 formula-decl nil sigma "reals/")
(OR const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(T_high type-eq-decl nil sigma "reals/")
(T_low type-eq-decl nil sigma "reals/")
(NOT const-decl "[bool -> bool]" booleans nil)
(subrange type-eq-decl nil integers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(limit_pos formula-decl nil series "series/")
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(conv_series_shift formula-decl nil series "series/")
(F skolem-const-decl "sequence[real]" extended_nnreal nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(convergent_diff formula-decl nil convergence_ops "analysis/")
(series_diff formula-decl nil series "series/")
(> const-decl "bool" reals nil)
(abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
nil)
(comparison_test formula-decl nil series "series/")
(x_lt const-decl "bool" extended_nnreal nil))
shostak))
(x_inf_le 0
(x_inf_le-1 nil 3450519245
("" (skosimp)
(("" (expand "x_inf")
(("" (expand "x_le" 1)
(("" (flatten)
(("" (assert)
(("" (expand "fullset")
(("" (expand "image")
(("" (expand "x_inf")
(("" (prop)
(("1" (skosimp)
(("1" (typepred "x!1")
(("1" (skosimp)
(("1" (inst -4 "x!2")
(("1" (expand "x_le")
(("1"
(assert)
(("1"
(flatten)
(("1"
(inst - "S!1(x!2)")
(("1" (inst + "x!2") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace 1 2)
(("2" (skolem! 1)
(("2" (lift-if)
(("2" (assert)
(("2"
(case-replace "FORALL (x:
({y: extended_nnreal |
EXISTS (x_1: ({x: nat | TRUE})): y = S!1(x_1)})):
NOT x`1")
(("1"
(inst - "x!1")
(("1"
(typepred
"glb({z:real |
EXISTS x:
(EXISTS (x_1: ({x: nat | TRUE})): x = T!1(x_1)) AND
x`1 AND x`2 = z})")
(("1"
(name-replace
"RHS"
"glb({z:real |
EXISTS x:
(EXISTS (x_1: ({x: nat | TRUE})): x = T!1(x_1)) AND
x`1 AND x`2 = z})")
(("1"
(expand
"greatest_lower_bound?"
-1)
(("1"
(flatten)
(("1"
(inst -2 "0")
(("1"
(assert)
(("1"
(expand "lower_bound?")
(("1"
(skosimp)
(("1"
(typepred "s!1")
(("1"
(skosimp)
(("1"
(skosimp)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 3)
(("2"
(assert)
(("2"
(split)
(("1"
(expand "nonempty?")
(("1"
(expand "empty?")
(("1"
(expand "member")
(("1"
(typepred "x!1")
(("1"
(skosimp)
(("1"
(inst -2 "x!1`2")
(("1"
(inst + "x!1")
(("1"
(assert)
(("1"
(inst
1
"x!2")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand "bounded_below?")
(("2"
(inst + "0")
(("2"
(expand "lower_bound?")
(("2"
(skosimp)
(("2"
(typepred "s!1")
(("2"
(skosimp)
(("2"
(skosimp)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace 1 2)
(("2"
(skosimp)
(("2"
(typepred
"glb({z:real |
EXISTS x:
(EXISTS (x_1: ({x: nat | TRUE})): x = S!1(x_1)) AND
x`1 AND x`2 = z})")
(("1"
(name-replace
"LHS"
"glb({z:real |
EXISTS x:
(EXISTS (x_1: ({x: nat | TRUE})): x = S!1(x_1)) AND
x`1 AND x`2 = z})")
(("1"
(typepred
"glb({z:real |
EXISTS x:
(EXISTS (x_1: ({x: nat | TRUE})): x = T!1(x_1)) AND
x`1 AND x`2 = z})")
(("1"
(name-replace
"RHS"
"glb({z:real |
EXISTS x:
(EXISTS (x_1: ({x: nat | TRUE})): x = T!1(x_1)) AND
x`1 AND x`2 = z})")
(("1"
(expand
"greatest_lower_bound?")
(("1"
(flatten)
(("1"
(inst -2 "LHS")
(("1"
(assert)
(("1"
(expand
"lower_bound?"
1)
(("1"
(skosimp)
(("1"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.55 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.
|
