|
(integral_step
(IMP_step_fun_def_TCC1 0
(IMP_step_fun_def_TCC1-1 nil 3282481239
("" (lemma "connected_domain") (("" (propax) nil nil)) nil)
((connected_domain formula-decl nil integral_step nil)) shostak))
(IMP_step_fun_def_TCC2 0
(IMP_step_fun_def_TCC2-1 nil 3282481239
("" (lemma "not_one_element") (("" (propax) nil nil)) nil)
((not_one_element formula-decl nil integral_step nil)) shostak))
(sigma_0_m1_TCC1 0
(sigma_0_m1_TCC1-1 nil 3403457729 ("" (subtype-tcc) nil nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(sigma_0_m1_TCC2 0
(sigma_0_m1_TCC2-1 nil 3403457729 ("" (subtype-tcc) nil nil)
((minus_odd_is_odd application-judgement "odd_int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(sigma_0_m1_TCC3 0
(sigma_0_m1_TCC3-1 nil 3403457729 ("" (subtype-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)
(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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(integer nonempty-type-from-decl nil integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
nil))
(sigma_0_m1 0
(sigma_0_m1-1 nil 3403457735
("" (skosimp*) (("" (expand "sigma") (("" (propax) nil nil)) nil))
nil)
((sigma def-decl "real" sigma "reals/")) shostak))
(pick_TCC1 0
(pick_TCC1-1 nil 3281791727 ("" (subtype-tcc) nil nil) nil shostak))
(pick_TCC2 0
(pick_TCC2-1 nil 3281791727 ("" (subtype-tcc) nil nil) nil shostak))
(pick_TCC3 0
(pick_TCC3-1 nil 3281791727 ("" (subtype-tcc) nil nil) nil shostak))
(pick_TCC4 0
(pick_TCC4-2 nil 3281793131
("" (skosimp*)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (expand "member")
(("" (inst - "(seq(P!1)(j!1) + seq(P!1)(1 + j!1))/2")
(("1" (typepred "P!1")
(("1" (inst - "j!1")
(("1" (split)
(("1" (cross-mult 1) (("1" (assert) nil nil)) nil)
("2" (cross-mult 1) (("2" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (lemma "connected_domain")
(("2" (expand "connected?")
(("2"
(inst - "seq(P!1)(j!1)" "seq(P!1)(1 + j!1)"
"(seq(P!1)(j!1) + seq(P!1)(1 + j!1))/2")
(("2" (assert)
(("2" (hide 2)
(("2" (typepred "P!1")
(("2" (inst - "j!1")
(("2" (split)
(("1" (cross-mult 1)
(("1" (assert) nil nil)) nil)
("2" (cross-mult 1)
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((nonempty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(connected_domain formula-decl nil integral_step nil)
(div_mult_pos_le1 formula-decl nil real_props nil)
(div_mult_pos_le2 formula-decl nil real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(connected? const-decl "bool" deriv_domain_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_times_real_is_real application-judgement "real" reals nil)
(posreal nonempty-type-eq-decl nil real_types nil)
(nonneg_real nonempty-type-eq-decl nil real_types nil)
(div_mult_pos_lt2 formula-decl nil real_props nil)
(div_mult_pos_lt1 formula-decl nil real_props 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)
(T_pred const-decl "[real -> boolean]" integral_step nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(/= const-decl "boolean" notequal nil)
(nznum nonempty-type-eq-decl nil number_fields nil)
(/ const-decl "[numfield, nznum -> numfield]" number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(T formal-subtype-decl nil integral_step nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(a!1 skolem-const-decl "T" integral_step nil)
(< const-decl "bool" reals nil)
(b!1 skolem-const-decl "{x: T | a!1 < x}" integral_step nil)
(closed_interval type-eq-decl nil intervals_real "reals/")
(finite_sequence type-eq-decl nil finite_sequences nil)
(> const-decl "bool" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields 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)
(below type-eq-decl nil naturalnumbers nil)
(partition type-eq-decl nil integral_def nil)
(P!1 skolem-const-decl "partition[T](a!1, b!1)" integral_step nil)
(j!1 skolem-const-decl "below(length(P!1) - 1)" integral_step nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_div_nzreal_is_real application-judgement "real" reals nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(empty? const-decl "bool" sets nil))
nil)
(pick_TCC4-1 nil 3281791727
("" (subtype-tcc)
(("1" (postpone) nil nil) ("2" (postpone) nil nil)) nil)
nil shostak))
(stp_sect_TCC1 0
(stp_sect_TCC1-1 nil 3262529911
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(stp_sect_TCC2 0
(stp_sect_TCC2-1 nil 3262529911
("" (skosimp*) (("" (assert) nil nil)) 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)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(stp_sect_TCC3 0
(stp_sect_TCC3-1 nil 3262529911
("" (skosimp*) (("" (assert) nil nil)) nil)
((int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(stp_sect_lem_TCC1 0
(stp_sect_lem_TCC1-1 nil 3262529911
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(stp_sect_lem 0
(stp_sect_lem-1 nil 3262529850
("" (skosimp*)
(("" (expand "stp_sect")
(("" (case "x!1 = seq(P!1)(ii!1)")
(("1" (assert)
(("1" (lemma "parts_order")
(("1" (inst - "a!1" "b!1" "P!1" "ii!1" "jj!1")
(("1" (assert) nil nil)) nil))
nil))
nil)
("2" (assert)
(("2" (lift-if)
(("2" (lemma "parts_order")
(("2" (inst - "a!1" "b!1" "P!1" "ii!1" "jj!1")
(("2" (assert)
(("2" (lemma "parts_order")
(("2" (inst - "a!1" "b!1" "P!1" "ii!1+1" "jj!1")
(("2" (assert) (("2" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((stp_sect const-decl "real" integral_step nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers 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)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(parts_order formula-decl nil integral_def nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(T_pred const-decl "[real -> boolean]" integral_step nil)
(T formal-subtype-decl nil integral_step nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(closed_interval type-eq-decl nil intervals_real "reals/")
(finite_sequence type-eq-decl nil finite_sequences nil)
(> const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields 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) (< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(partition type-eq-decl nil integral_def nil)
(upto nonempty-type-eq-decl nil naturalnumbers nil))
nil))
(sigma_stp_sect_TCC1 0
(sigma_stp_sect_TCC1-1 nil 3262529911
("" (skosimp*) (("" (assert) nil nil)) nil)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(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))
shostak))
(sigma_stp_sect_TCC2 0
(sigma_stp_sect_TCC2-1 nil 3262529911
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(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))
shostak))
(sigma_stp_sect 0
(sigma_stp_sect-1 nil 3262529900
("" (skolem!)
(("" (assert)
(("" (flatten)
(("" (skolem!)
(("" (induct "j")
(("1" (assert)
(("1" (flatten)
(("1" (expand "sigma")
(("1" (lemma "stp_sect_lem")
(("1" (inst?)
(("1" (inst -1 "f!1" "x!1")
(("1" (assert)
(("1" (inst?)
(("1" (inst -1 "1")
(("1"
(assert)
(("1"
(expand "sigma")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "sigma" 1)
(("2" (assert)
(("2"
(case-replace " sigma(0, j!1,
LAMBDA (ii: nat):
IF ii >= 2 + j!1 THEN 0
ELSE stp_sect(a!1, b!1, P!1, ii, f!1)(x!1)
ENDIF) = sigma(0, j!1,
LAMBDA (ii: nat):
IF ii >= 1 + j!1 THEN 0
ELSE stp_sect(a!1, b!1, P!1, ii, f!1)(x!1)
ENDIF)")
(("1" (hide -1)
(("1" (case "x!1 > seq(P!1)(1 + j!1)")
(("1" (assert)
(("1" (replace -2)
(("1" (lemma "stp_sect_lem")
(("1"
(inst?)
(("1"
(inst -1 "f!1" "x!1")
(("1"
(assert)
(("1"
(inst?)
(("1"
(inst - "j!1+2")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "parts_order")
(("2"
(inst - "a!1" "b!1" "P!1" "j!1+1" "j!1+2")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (rewrite "sigma_restrict_eq[nat]")
(("2" (hide 2)
(("2" (expand "restrict")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp*) nil nil)
("4" (skosimp*) (("4" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(restrict const-decl "[T -> real]" sigma "reals/")
(sigma_restrict_eq formula-decl nil sigma "reals/")
(parts_order formula-decl nil integral_def nil)
(odd_plus_even_is_odd application-judgement "odd_int" integers nil)
(real_gt_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)
(real_plus_real_is_real application-judgement "real" reals nil)
(upto nonempty-type-eq-decl nil naturalnumbers nil)
(stp_sect_lem formula-decl nil integral_step nil)
(nat_induction formula-decl nil naturalnumbers nil)
(stp_sect const-decl "real" integral_step nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(sigma def-decl "real" sigma "reals/")
(T_high type-eq-decl nil sigma "reals/")
(T_low type-eq-decl nil sigma "reals/")
(OR const-decl "[bool, bool -> bool]" booleans nil)
(pred type-eq-decl nil defined_types nil)
(x!1 skolem-const-decl "T" integral_step nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(<= const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(below type-eq-decl nil nat_types nil)
(T_pred const-decl "[real -> boolean]" integral_step nil)
(T formal-subtype-decl nil integral_step nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(a!1 skolem-const-decl "T" integral_step nil)
(b!1 skolem-const-decl "T" integral_step nil)
(closed_interval type-eq-decl nil intervals_real "reals/")
(finite_sequence type-eq-decl nil finite_sequences nil)
(> const-decl "bool" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(partition type-eq-decl nil integral_def nil)
(P!1 skolem-const-decl "partition[T](a!1, b!1)" integral_step nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(integral_stp_sect_TCC1 0
(integral_stp_sect_TCC1-1 nil 3281868373 ("" (subtype-tcc) nil nil)
nil shostak))
(integral_stp_sect_TCC2 0
(integral_stp_sect_TCC2-1 nil 3281868373 ("" (subtype-tcc) nil nil)
nil shostak))
(integral_stp_sect 0
(integral_stp_sect-1 nil 3281796581
("" (skosimp*)
(("" (rewrite "integral_def" :dir rl)
(("1" (lemma "zero_except_intv?_integrable")
(("1" (inst?)
(("1" (assert)
(("1" (assert)
(("1"
(inst - "val_in(a!1, b!1, P!1, j!1, f!1)"
"seq(P!1)(1 + j!1)" "seq(P!1)(j!1)")
(("1" (assert)
(("1" (split -1)
(("1" (flatten) (("1" (assert) nil nil)) nil)
("2" (typepred "P!1")
(("2" (inst - "j!1") nil nil)) nil)
("3" (assert)
(("3" (hide 2)
(("3" (expand "zero_except_intv?")
(("3" (skosimp*)
(("3" (assert)
(("3"
(expand "stp_sect")
(("3"
(assert)
(("3"
(lift-if)
(("3"
(expand "val_in")
(("3"
(ground)
(("3"
(typepred "P!1")
(("3"
(inst - "j!1")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (lemma "parts_order[T]")
(("2" (inst - "a!1" "b!1" "P!1" "0" "1+j!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_times_real_is_real application-judgement "real" reals nil)
(integral_def formula-decl nil integral_def nil)
(bool nonempty-type-eq-decl nil booleans nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(closed_interval type-eq-decl nil intervals_real "reals/")
(finite_sequence type-eq-decl nil finite_sequences nil)
(> const-decl "bool" 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)
(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)
(below type-eq-decl nil naturalnumbers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(partition type-eq-decl nil integral_def nil)
(stp_sect const-decl "real" integral_step nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(val_in const-decl "real" integral_step 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)
(T_pred const-decl "[real -> boolean]" integral_step nil)
(T formal-subtype-decl nil integral_step nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(zero_except_intv? const-decl "bool" integral_pulse nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(zero_except_intv?_integrable formula-decl nil integral_pulse nil))
shostak))
(sumof_TCC1 0
(sumof_TCC1-1 nil 3281876432 ("" (subtype-tcc) nil nil) nil shostak))
(sumof_TCC2 0
(sumof_TCC2-1 nil 3281876432 ("" (assuming-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)
(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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(T_pred const-decl "[real -> boolean]" integral_step nil)
(T formal-subtype-decl nil integral_step 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)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(sigma_sumof_TCC1 0
(sigma_sumof_TCC1-1 nil 3261756014
("" (skosimp*) (("" (assert) nil nil)) nil)
((nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(sigma_sumof 0
(sigma_sumof-3 nil 3306073359
("" (auto-rewrite "sigma_0_m1")
(("" (skolem!)
(("" (flatten)
(("" (expand "step_function_on?")
(("" (induct "n")
(("1" (assert)
(("1" (skosimp*)
(("1" (expand "sumof")
(("1" (expand "sigma")
(("1" (inst - "0")
(("1" (skosimp*)
(("1" (expand "stp_sect")
(("1" (assert)
(("1" (lift-if)
(("1"
(lift-if)
(("1"
(typepred "P!1")
(("1"
(inst - "0")
(("1"
(ground)
(("1"
(expand "val_in")
(("1"
(inst-cp
-
"pick(a!1, b!1, P!1, 0)")
(("1"
(inst - "x!1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "P!1")
(("2" (assert)
(("2" (skosimp*)
(("2" (split -5)
(("1" (inst?)
(("1" (assert)
(("1" (case "x!1 <= seq(P!1)(1 + j!1)")
(("1" (assert)
(("1" (expand "sumof")
(("1"
(expand "sigma" 1)
(("1"
(case-replace
" sigma(0, j!1,
LAMBDA (ii: nat):
IF ii > 1 + j!1 THEN 0
ELSE stp_sect(a!1, b!1, P!1, ii, f!1)(x!1)
ENDIF) = sigma(0, j!1,
LAMBDA (ii: nat):
IF ii > j!1 THEN 0
ELSE stp_sect(a!1, b!1, P!1, ii, f!1)(x!1)
ENDIF)")
(("1"
(hide -1)
(("1"
(move-terms -2 l 2)
(("1"
(replace -2)
(("1"
(hide -2)
(("1"
(expand "stp_sect")
(("1"
(lift-if)
(("1"
(typepred "P!1")
(("1"
(inst - "j!1+1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(rewrite
"sigma_restrict_eq[nat]")
(("2"
(hide 2)
(("2"
(expand "restrict")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (hide -1)
(("2"
(expand "sumof")
(("2"
(assert)
(("2"
(inst - "j!1+1")
(("2"
(assert)
(("2"
(lift-if)
(("2"
(case-replace
"x!1 = seq(P!1)(2 + j!1)")
(("1"
(assert)
(("1"
(case-replace
"(LAMBDA (ii: nat):
IF ii > 1 + j!1 THEN 0
ELSE stp_sect(a!1, b!1, P!1, ii, f!1)(seq(P!1)(2 + j!1))
ENDIF) = (LAMBDA (ii: nat): 0)")
(("1"
(rewrite
"sigma_const[nat]")
nil
nil)
("2"
(hide 3)
(("2"
(apply-extensionality
1
:hide?
t)
(("2"
(lift-if)
(("2"
(ground)
(("2"
(expand
"stp_sect")
(("2"
(lift-if)
(("2"
(ground)
(("1"
(lemma
"parts_order[T]")
(("1"
(inst
-1
"a!1"
"b!1"
"P!1"
"x!2"
"2+j!1")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(expand
"val_in")
(("2"
(lemma
"parts_order[T]")
(("2"
(inst
-1
"a!1"
"b!1"
"P!1"
"x!2+1"
"2+j!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(lemma "sigma_stp_sect")
(("2"
(inst
-
"a!1"
"b!1"
"f!1"
"x!1")
(("2"
(assert)
(("2"
(inst -1 "P!1")
(("2"
(expand
"sigma"
3)
(("2"
(inst -1 "j!1")
(("2"
(assert)
(("2"
(assert)
(("2"
(case-replace
" sigma(0, j!1,
LAMBDA (ii: nat):
IF ii > 1 + j!1 THEN 0
ELSE stp_sect(a!1, b!1, P!1, ii, f!1)(x!1)
ENDIF) = sigma(0, j!1,
LAMBDA (ii: nat):
IF ii >= 1 + j!1 THEN 0
ELSE stp_sect(a!1, b!1, P!1, ii, f!1)(x!1)
ENDIF)")
(("1"
(hide
-1)
(("1"
(replace
-1)
(("1"
(expand
"stp_sect")
(("1"
(inst
-
"j!1+1")
(("1"
(skosimp*)
(("1"
(inst-cp
-
"x!1")
(("1"
(expand
"val_in")
(("1"
(inst
-
"pick(a!1, b!1, P!1, 1 + j!1)")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(hide
4)
(("2"
(rewrite
"sigma_restrict_eq[nat]")
(("2"
(hide
2)
(("2"
(expand
"restrict")
(("2"
(propax)
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" (assert) nil nil))
nil))
nil))
nil))
nil)
("3" (skosimp*) (("3" (assert) nil nil)) nil)
("4" (assert) nil nil)
("5" (skosimp*) (("5" (assert) nil nil)) nil)
("6" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
((step_function_on? const-decl "bool" step_fun_def nil)
(T_high type-eq-decl nil sigma "reals/")
(T_low type-eq-decl nil sigma "reals/")
(OR const-decl "[bool, bool -> bool]" booleans nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(real_minus_real_is_real application-judgement "real" reals nil)
(sigma_restrict_eq formula-decl nil sigma "reals/")
(restrict const-decl "[T -> real]" sigma "reals/")
(sigma_const formula-decl nil sigma "reals/")
(int_plus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_times_even_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(parts_order formula-decl nil integral_def nil)
(sigma_stp_sect formula-decl nil integral_step nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(odd_plus_even_is_odd application-judgement "odd_int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(pick const-decl "{t: T | seq(P)(j) < t AND t < seq(P)(j + 1)}"
integral_step nil)
(open_interval type-eq-decl nil intervals_real "reals/")
(val_in const-decl "real" integral_step nil)
(sigma_0_m1 formula-decl nil integral_step nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(sigma def-decl "real" sigma "reals/")
(n!1 skolem-const-decl "nat" integral_step nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(n!1 skolem-const-decl "nat" integral_step nil)
(nat_induction formula-decl nil naturalnumbers nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(stp_sect const-decl "real" integral_step nil)
(sumof const-decl "real" integral_step nil)
(list_of_funs type-eq-decl nil integral_step nil)
(upto nonempty-type-eq-decl nil naturalnumbers nil)
(pred type-eq-decl nil defined_types 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)
(<= const-decl "bool" reals nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(below type-eq-decl nil nat_types nil)
(T_pred const-decl "[real -> boolean]" integral_step nil)
(T formal-subtype-decl nil integral_step nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(a!1 skolem-const-decl "T" integral_step nil)
(< const-decl "bool" reals nil)
(b!1 skolem-const-decl "{x: T | a!1 < x}" integral_step nil)
(closed_interval type-eq-decl nil intervals_real "reals/")
(finite_sequence type-eq-decl nil finite_sequences nil)
(> const-decl "bool" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(below type-eq-decl nil naturalnumbers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(partition type-eq-decl nil integral_def nil)
(P!1 skolem-const-decl "partition[T](a!1, b!1)" integral_step nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil))
nil)
(sigma_sumof-2 nil 3281792634
("" (skolem!)
(("" (flatten)
(("" (expand "step_function_on?")
(("" (induct "n")
(("1" (assert)
(("1" (skosimp*)
(("1" (expand "sumof")
(("1" (expand "sigma")
(("1" (inst - "0")
(("1" (skosimp*)
(("1" (expand "stp_sect")
(("1" (assert)
(("1" (lift-if)
(("1" (lift-if)
(("1"
(typepred "P!1")
(("1"
(inst - "0")
(("1"
(ground)
(("1"
(expand "val_in")
(("1"
(inst-cp
-
"pick(a!1, b!1, P!1, 0)")
(("1"
(inst - "x!1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "P!1")
(("2" (assert)
(("2" (skosimp*)
(("2" (split -5)
(("1" (inst?)
(("1" (assert)
(("1" (case "x!1 <= seq(P!1)(1 + j!1)")
(("1" (assert)
(("1" (expand "sumof")
(("1" (expand "sigma" 1)
(("1"
(case-replace
" sigma(0, j!1,
LAMBDA (ii: nat):
IF ii > 1 + j!1 THEN 0
ELSE stp_sect(a!1, b!1, P!1, ii, f!1)(x!1)
ENDIF) = sigma(0, j!1,
LAMBDA (ii: nat):
IF ii > j!1 THEN 0
ELSE stp_sect(a!1, b!1, P!1, ii, f!1)(x!1)
ENDIF)")
(("1"
(hide -1)
(("1"
(move-terms -2 l 2)
(("1"
(replace -2)
(("1"
(hide -2)
(("1"
(expand "stp_sect")
(("1"
(lift-if)
(("1"
(typepred "P!1")
(("1"
(inst - "j!1+1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2" (assert) nil nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(rewrite "sigma_restrict_eq[nat]")
(("1"
(hide 2)
(("1"
(expand "restrict")
(("1" (propax) nil nil))
nil))
nil)
("2"
(lemma "connected_domain")
(("2"
(assert)
(("2"
(skosimp*)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("3"
(lemma "connected_domain")
(("3"
(skosimp*)
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (hide -1)
(("2" (expand "sumof")
(("2"
(assert)
(("2"
(inst - "j!1+1")
(("2"
(assert)
(("2"
(lift-if)
(("2"
(case-replace
"x!1 = seq(P!1)(2 + j!1)")
(("1"
(assert)
(("1"
(case-replace
"(LAMBDA (ii: nat):
IF ii > 1 + j!1 THEN 0
ELSE stp_sect(a!1, b!1, P!1, ii, f!1)(seq(P!1)(2 + j!1))
ENDIF) = (LAMBDA (ii: nat): 0)")
(("1"
(rewrite
"sigma_const[nat]")
(("1"
(skosimp*)
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(hide 3)
(("2"
(apply-extensionality
1
:hide?
t)
(("2"
(lift-if)
(("2"
(ground)
(("2"
(expand
"stp_sect")
(("2"
(lift-if)
(("2"
(ground)
(("1"
(lemma
"parts_order[T]")
(("1"
(inst
-1
"a!1"
"b!1"
"P!1"
"x!2"
"2+j!1")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(expand
"val_in")
(("2"
(lemma
"parts_order[T]")
(("2"
(inst
-1
"a!1"
"b!1"
"P!1"
"x!2+1"
"2+j!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(lemma "sigma_stp_sect[T]")
(("2"
(inst
-
"a!1"
"b!1"
"f!1"
"x!1")
(("2"
(assert)
(("2"
(inst -1 "P!1")
(("2"
(expand "sigma" 3)
(("2"
(inst -1 "j!1")
(("2"
(assert)
(("2"
(assert)
(("2"
(case-replace
" sigma(0, j!1,
LAMBDA (ii: nat):
IF ii > 1 + j!1 THEN 0
ELSE stp_sect(a!1, b!1, P!1, ii, f!1)(x!1)
ENDIF) = sigma(0, j!1,
LAMBDA (ii: nat):
IF ii >= 1 + j!1 THEN 0
ELSE stp_sect(a!1, b!1, P!1, ii, f!1)(x!1)
ENDIF)")
(("1"
(hide -1)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.76 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.
|
