|
(step_fun_props
(IMP_step_fun_def_TCC1 0
(IMP_step_fun_def_TCC1-1 nil 3282488571
("" (lemma "connected_domain") (("" (propax) nil nil)) nil)
((connected_domain formula-decl nil step_fun_props nil)) shostak))
(IMP_step_fun_def_TCC2 0
(IMP_step_fun_def_TCC2-1 nil 3282488571
("" (lemma "not_one_element") (("" (propax) nil nil)) nil)
((not_one_element formula-decl nil step_fun_props nil)) shostak))
(is_step_TCC1 0
(is_step_TCC1-1 nil 3273828203
("" (skosimp*)
(("" (lemma "connected_domain")
(("" (inst?) (("" (inst - "y!1") (("" (assert) nil nil)) nil))
nil))
nil))
nil)
((connected_domain formula-decl nil step_fun_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(is_step_TCC2 0
(is_step_TCC2-1 nil 3273828203
("" (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))
shostak))
(is_step 0
(is_step-2 nil 3292077121
("" (skosimp*)
(("" (assert)
(("" (expand "step_function?")
(("" (expand "step_function_on?")
(("" (inst + "P!1")
(("" (skosimp*)
(("" (inst - "ii!1")
(("" (skosimp*)
(("" (inst + "fv!1")
(("" (skosimp*)
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(step_function_on? const-decl "bool" step_fun_def nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(open_interval type-eq-decl nil intervals_real "reals/")
(partition type-eq-decl nil integral_def nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals 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 "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(> const-decl "bool" reals nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(closed_interval type-eq-decl nil intervals_real "reals/")
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-nonempty-subtype-decl nil step_fun_props nil)
(T_pred const-decl "[real -> boolean]" step_fun_props 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)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(step_function? const-decl "bool" step_fun_def nil))
nil)
(is_step-1 nil 3272795795
("" (skosimp*)
(("" (assert)
(("" (expand "step_function?")
(("" (inst + "P!1")
(("" (skosimp*)
(("" (inst - "ii!1")
(("" (skosimp*)
(("" (inst + "fv!1")
(("" (skosimp*)
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((partition type-eq-decl nil integral_def nil)
(step_function? const-decl "bool" step_fun_def nil))
shostak))
(UUPart_TCC1 0
(UUPart_TCC1-1 nil 3281267771
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(UUPart_TCC2 0
(UUPart_TCC2-1 nil 3281267771
("" (skosimp*)
(("" (rewrite "card_union[T]")
(("" (lemma "card_intersection_le[T]")
(("" (inst?)
(("" (assert)
(("" (lemma "card_part2set")
(("" (inst?)
(("" (lemma "card_part2set")
(("" (inst - "b!1" "c!1" "P2!1")
(("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-nonempty-subtype-decl nil step_fun_props nil)
(T_pred const-decl "[real -> boolean]" step_fun_props 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)
(card_intersection_le formula-decl nil finite_sets nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil))
shostak))
(UUPart_TCC3 0
(UUPart_TCC3-1 nil 3281267773
("" (skosimp*)
(("" (prop) (("1" (assert) nil nil) ("2" (assert) nil nil)) nil))
nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil))
shostak))
(UUPart_TCC4 0
(UUPart_TCC4-1 nil 3281271112
("" (skosimp*)
(("" (assert)
(("" (prop)
(("1" (skosimp*)
(("1" (lift-if) (("1" (assert) (("1" (ground) nil nil)) nil))
nil))
nil)
("2" (skosimp*)
(("2" (lift-if)
(("2" (lift-if)
(("2" (ground)
(("1" (typepred "ii!1")
(("1" (assert)
(("1" (typepred "P1!1") (("1" (inst?) nil nil))
nil))
nil))
nil)
("2" (assert)
(("2" (case "ii!1 = length(P1!1)-1")
(("1" (replace -1)
(("1" (typepred "P1!1")
(("1" (replace -3)
(("1" (assert)
(("1" (lemma "parts_order[T]")
(("1"
(inst - "b!1" "c!1" "P2!1" "0" "1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("3" (assert)
(("3" (typepred "P2!1")
(("3" (inst?) (("3" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil))
shostak))
(UUPart_TCC5 0
(UUPart_TCC5-1 nil 3399914704 ("" (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)
(T_pred const-decl "[real -> boolean]" step_fun_props nil)
(T formal-nonempty-subtype-decl nil step_fun_props nil)
(< const-decl "bool" reals 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 "[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)
(int_minus_int_is_int application-judgement "int" integers 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_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)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(UUPart_TCC6 0
(UUPart_TCC6-1 nil 3399914704 ("" (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)
(T_pred const-decl "[real -> boolean]" step_fun_props nil)
(T formal-nonempty-subtype-decl nil step_fun_props nil)
(< const-decl "bool" reals 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 "[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)
(int_minus_int_is_int application-judgement "int" integers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(odd_plus_even_is_odd application-judgement "odd_int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil))
nil))
(UUPart_TCC7 0
(UUPart_TCC7-2 nil 3399972943
("" (skosimp*)
(("" (lift-if)
(("" (lift-if)
(("" (assert)
(("" (skosimp*)
(("" (lift-if)
(("" (lift-if)
(("" (assert)
(("" (typepred "P1!1")
(("" (typepred "ii!1")
(("" (assert)
(("" (ground)
(("1" (inst?) nil nil)
("2" (case "ii!1 = length(P1!1)-1")
(("1" (replace -1)
(("1"
(typepred "P1!1")
(("1"
(replace -3)
(("1"
(assert)
(("1"
(lemma "parts_order[T]")
(("1"
(inst
-
"b!1"
"c!1"
"P2!1"
"0"
"1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil))
nil)
("3" (inst?)
(("3" (typepred "P2!1")
(("3"
(inst?)
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers 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)
(int_plus_int_is_int application-judgement "int" integers nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(minus_odd_is_odd application-judgement "odd_int" integers nil)
(parts_order formula-decl nil integral_def nil)
(real_ge_is_total_order name-judgement "(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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(T_pred const-decl "[real -> boolean]" step_fun_props nil)
(T formal-nonempty-subtype-decl nil step_fun_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals 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 "[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))
nil)
(UUPart_TCC7-1 nil 3399914704 ("" (subtype-tcc) nil nil) nil nil))
(split_step_is_step_TCC1 0
(split_step_is_step_TCC1-1 nil 3280237722
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(split_step_is_step 0
(split_step_is_step-3 nil 3292077159
("" (skosimp*)
(("" (expand "step_function?")
(("" (expand "step_function_on?")
(("" (skosimp*)
(("" (inst + "UUPart(a!1,b!1,c!1,P!1,P!2)")
(("" (skosimp*)
(("" (case "ii!1 < length(P!1)-1")
(("1" (inst -4 "ii!1")
(("1" (skosimp*)
(("1" (inst + "fv!1")
(("1" (skosimp*)
(("1" (hide -5)
(("1" (inst?)
(("1" (lift-if)
(("1"
(typepred "x!1")
(("1"
(expand "UUPart")
(("1"
(lift-if)
(("1" (ground) nil nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2"
(typepred "x!1")
(("2"
(expand "UUPart")
(("2"
(lift-if)
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -3)
(("2" (inst - "ii!1-length(P!1)+1")
(("1" (skosimp*)
(("1" (inst + "fv!1")
(("1" (skosimp*)
(("1" (inst?)
(("1" (typepred "x!1")
(("1"
(expand "UUPart")
(("1"
(lift-if)
(("1" (ground) nil nil))
nil))
nil))
nil)
("2" (hide 3)
(("2"
(typepred "x!1")
(("2"
(expand "UUPart")
(("2"
(lift-if)
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (hide 3)
(("2" (typepred "ii!1")
(("2" (expand "UUPart")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((step_function? const-decl "bool" step_fun_def nil)
(x!1 skolem-const-decl
"open_interval[T](seq(UUPart(a!1, b!1, c!1, P!1, P!2))(ii!1),
seq(UUPart(a!1, b!1, c!1, P!1, P!2))(1 + ii!1))"
step_fun_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(P!1 skolem-const-decl "partition[T](a!1, b!1)" step_fun_props nil)
(P!2 skolem-const-decl "partition[T](b!1, c!1)" step_fun_props nil)
(ii!1 skolem-const-decl
"below(length(UUPart(a!1, b!1, c!1, P!1, P!2)) - 1)"
step_fun_props nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(int_plus_int_is_int application-judgement "int" integers 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)
(NOT const-decl "[bool -> bool]" booleans nil)
(x!1 skolem-const-decl
"open_interval[T](seq(UUPart(a!1, b!1, c!1, P!1, P!2))(ii!1),
seq(UUPart(a!1, b!1, c!1, P!1, P!2))(1 + ii!1))"
step_fun_props nil)
(open_interval type-eq-decl nil intervals_real "reals/")
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(UUPart const-decl "partition[T](a, c)" step_fun_props nil)
(partition type-eq-decl nil integral_def nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(below 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)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(> const-decl "bool" reals nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(closed_interval type-eq-decl nil intervals_real "reals/")
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(c!1 skolem-const-decl "T" step_fun_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)
(bool nonempty-type-eq-decl nil booleans nil)
(< const-decl "bool" reals nil)
(T_pred const-decl "[real -> boolean]" step_fun_props nil)
(T formal-nonempty-subtype-decl nil step_fun_props nil)
(a!1 skolem-const-decl "T" step_fun_props nil)
(b!1 skolem-const-decl "T" step_fun_props nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(step_function_on? const-decl "bool" step_fun_def nil))
nil)
(split_step_is_step-2 nil 3280755186
("" (skosimp*)
(("" (expand "step_function?")
(("" (skosimp*)
(("" (inst + "UUPart(a!1,b!1,c!1,P!1,P!2)")
(("" (skosimp*)
(("" (case "ii!1 < length(P!1)-1")
(("1" (inst -4 "ii!1")
(("1" (skosimp*)
(("1" (inst + "fv!1")
(("1" (skosimp*)
(("1" (hide -5)
(("1" (inst?)
(("1" (lift-if)
(("1" (typepred "x!1")
(("1"
(expand "UUPart")
(("1"
(lift-if)
(("1" (ground) nil nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (typepred "x!1")
(("2"
(expand "UUPart")
(("2"
(lift-if)
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -3)
(("2" (inst - "ii!1-length(P!1)+1")
(("1" (skosimp*)
(("1" (inst + "fv!1")
(("1" (skosimp*)
(("1" (inst?)
(("1" (typepred "x!1")
(("1" (expand "UUPart")
(("1"
(lift-if)
(("1" (ground) nil nil))
nil))
nil))
nil)
("2" (hide 3)
(("2" (typepred "x!1")
(("2"
(expand "UUPart")
(("2"
(lift-if)
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (hide 3)
(("2" (typepred "ii!1")
(("2" (expand "UUPart")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((step_function? const-decl "bool" step_fun_def nil)
(partition type-eq-decl nil integral_def nil))
nil)
(split_step_is_step-1 nil 3280753743
("" (skosimp*)
(("" (rewrite "step_fun_is_sum")
(("" (rewrite "step_fun_is_sum")
(("" (rewrite "step_fun_is_sum")
(("" (skosimp*)
((""
(inst + "nf!1+nf!2"
"(LAMBDA (ii: upto[nf!1+nf!2]): IF ii <= nf!1 THEN
lof!1(ii)
ELSE
lof!2(nf!1+1+ii)
ENDIF)")
(("1" (prop)
(("1" (skosimp*) (("1" (postpone) nil nil)) nil)
("2" (apply-extensionality 1 :hide? t)
(("1" (lift-if)
(("1" (expand "sumof")
(("1" (ground)
(("1"
(case-replace "(LAMBDA (ii_1: nat):
IF ii_1 > nf!1 + nf!2 THEN 0
ELSE IF ii_1 <= nf!1 THEN lof!1(ii_1)(x!1)
ELSE lof!2(1 + ii_1 + nf!1)(x!1)
ENDIF
ENDIF) = (LAMBDA (ii_1: nat): 0)")
(("1" (rewrite "sigma_const[nat]")
(("1" (skosimp*) (("1" (assert) nil nil))
nil))
nil)
("2" (hide 2)
(("2" (apply-extensionality 1 :hide? t)
(("1"
(lift-if)
(("1"
(ground)
(("1"
(inst -5 "x!2")
(("1"
(expand "pulse?")
(("1"
(skosimp*)
(("1"
(expand "zero_except_intv?")
(("1"
(skosimp*)
(("1"
(inst -5 "x!1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst -6 "1 + nf!1 + x!2")
(("1" (postpone) nil nil)
("2" (postpone) nil nil))
nil))
nil))
nil)
("2" (postpone) nil nil))
nil))
nil)
("3" (postpone) nil nil))
nil)
("2" (postpone) nil nil)
("3" (postpone) nil nil)
("4" (postpone) nil nil))
nil))
nil))
nil)
("2" (lemma "connected_domain")
(("2" (propax) nil nil)) nil)
("3" (skosimp*)
(("3" (assert) (("3" (postpone) nil nil)) nil))
nil))
nil))
nil)
("2" (postpone) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
nil shostak))
(ssis_prep 0
(ssis_prep-1 nil 3281187679
("" (skosimp*)
(("" (prop)
(("1" (lemma "Union_lem")
(("1" (inst?)
(("1" (assert)
(("1" (skosimp*)
(("1" (inst + "kk!1") (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (lemma "Union_sym")
(("2" (inst?)
(("2" (replace -1)
(("2" (hide -1)
(("2" (lemma "Union_lem")
(("2" (inst?)
(("1" (assert)
(("1" (skosimp*)
(("1" (inst + "kk!1") (("1" (assert) nil nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (typepred "nn!1")
(("2" (reveal -2) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
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) (> 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)
(closed_interval type-eq-decl nil intervals_real "reals/")
(finite_sequence type-eq-decl nil finite_sequences nil)
(partition type-eq-decl nil integral_def nil)
(UnionPart const-decl "partition[T](a, b)" step_fun_scaf nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
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)
(Union_lem formula-decl nil step_fun_scaf 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]" step_fun_props nil)
(T formal-nonempty-subtype-decl nil step_fun_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nn!1 skolem-const-decl
"below(length(UnionPart(a!1, b!1, P1!1, P2!1)) - 1)"
step_fun_props nil)
(P2!1 skolem-const-decl "partition[T](a!1, b!1)" step_fun_props
nil)
(P1!1 skolem-const-decl "partition[T](a!1, b!1)" step_fun_props
nil)
(b!1 skolem-const-decl "{x: T | a!1 < x}" step_fun_props nil)
(a!1 skolem-const-decl "T" step_fun_props nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(Union_sym formula-decl nil step_fun_scaf nil))
shostak))
(sum_step_is_step 0
(sum_step_is_step-2 nil 3292077198
("" (skosimp*)
(("" (rewrite "step_fun?_lem" +)
(("" (expand "step_function?")
(("" (expand "step_function_on?")
(("" (skosimp*)
(("" (expand "step_fun?")
(("" (inst + "UnionPart(a!1,b!1,P!1,P!2)")
(("" (skosimp*)
(("" (typepred "x!1")
(("" (typepred "y!1")
(("" (lemma "ssis_prep")
((""
(inst - "a!1" "b!1" "P!1" "P!2" "ii!1" "x!1"
"y!1")
(("" (assert)
(("" (skosimp*)
((""
(expand "+ ")
((""
(inst -16 "ii!2")
((""
(inst -17 "jj!1")
((""
(skosimp*)
((""
(inst-cp - "x!1")
(("1"
(inst - "y!1")
(("1"
(inst-cp - "x!1")
(("1"
(inst - "y!1")
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((step_fun?_lem formula-decl nil step_fun_def nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(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]" step_fun_props nil)
(T formal-nonempty-subtype-decl nil step_fun_props nil)
(step_function_on? const-decl "bool" step_fun_def nil)
(step_fun? const-decl "bool" step_fun_def nil)
(y!1 skolem-const-decl
"open_interval[T](seq(UnionPart(a!1, b!1, P!1, P!2))(ii!1),
seq(UnionPart(a!1, b!1, P!1, P!2))(1 + ii!1))"
step_fun_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(jj!1 skolem-const-decl "below(length(P!2) - 1)" step_fun_props
nil)
(x!1 skolem-const-decl
"open_interval[T](seq(UnionPart(a!1, b!1, P!1, P!2))(ii!1),
seq(UnionPart(a!1, b!1, P!1, P!2))(1 + ii!1))"
step_fun_props nil)
(ii!1 skolem-const-decl
"below(length(UnionPart(a!1, b!1, P!1, P!2)) - 1)" step_fun_props
nil)
(P!2 skolem-const-decl "partition[T](a!1, b!1)" step_fun_props nil)
(ii!2 skolem-const-decl "below(length(P!1) - 1)" step_fun_props
nil)
(P!1 skolem-const-decl "partition[T](a!1, b!1)" step_fun_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(ssis_prep formula-decl nil step_fun_props nil)
(open_interval type-eq-decl nil intervals_real "reals/")
(NOT const-decl "[bool -> bool]" booleans nil)
(UnionPart const-decl "partition[T](a, b)" step_fun_scaf nil)
(partition type-eq-decl nil integral_def nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(below 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)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(> const-decl "bool" reals nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(closed_interval type-eq-decl nil intervals_real "reals/")
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(b!1 skolem-const-decl "T" step_fun_props nil)
(a!1 skolem-const-decl "T" step_fun_props nil)
(< const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(step_function? const-decl "bool" step_fun_def nil))
nil)
(sum_step_is_step-1 nil 3281116562
("" (skosimp*)
(("" (rewrite "step_fun?_lem" +)
(("1" (expand "step_function?")
(("1" (skosimp*)
(("1" (expand "step_fun?")
(("1" (inst + "UnionPart(a!1,b!1,P!1,P!2)")
(("1" (skosimp*)
(("1" (typepred "x!1")
(("1" (typepred "y!1")
(("1" (lemma "ssis_prep")
(("1"
(inst - "a!1" "b!1" "P!1" "P!2" "ii!1" "x!1"
"y!1")
(("1" (assert)
(("1" (skosimp*)
(("1" (expand "+ ")
(("1"
(inst -16 "ii!2")
(("1"
(inst -17 "jj!1")
(("1"
(skosimp*)
(("1"
(inst-cp - "x!1")
(("1"
(inst - "y!1")
(("1"
(inst-cp - "x!1")
(("1"
(inst - "y!1")
(("1" (assert) nil nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil)
("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "connected_domain") (("2" (propax) nil nil)) nil))
nil))
nil)
((step_fun?_lem formula-decl nil step_fun_def nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(partition type-eq-decl nil integral_def nil)
(UnionPart const-decl "partition[T](a, b)" step_fun_scaf nil)
(step_fun? const-decl "bool" step_fun_def nil)
(step_function? const-decl "bool" step_fun_def nil))
shostak))
(diff_step_is_step 0
(diff_step_is_step-3 nil 3306073235
("" (skosimp*)
(("" (lemma "sum_step_is_step")
(("" (inst?)
(("" (inst - "-g!1")
(("" (assert)
(("" (expand "+ ")
((""
(case-replace
"(LAMBDA (x: T): (-g!1)(x) + f!1(x)) = f!1 - g!1")
(("1" (split -2)
(("1" (propax) nil nil)
("2" (hide 2)
(("2" (hide -1 -3)
(("2" (expand "step_function?")
(("2" (expand "step_function_on?")
(("2" (skosimp*)
(("2" (inst + "P!1")
(("2"
(skosimp*)
(("2"
(inst - "ii!1")
(("2"
(skosimp*)
(("2"
(inst + "-fv!1")
(("2"
(skosimp*)
(("2"
(inst?)
(("2"
(expand "-")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (apply-extensionality 1 :hide? t)
(("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((sum_step_is_step formula-decl nil step_fun_props nil)
(- const-decl "[T -> real]" real_fun_ops "reals/")
(+ const-decl "[T -> real]" real_fun_ops "reals/")
(real_minus_real_is_real application-judgement "real" reals nil)
(step_function_on? const-decl "bool" step_fun_def 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)
(- 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)
(partition type-eq-decl nil integral_def nil)
(minus_real_is_real application-judgement "real" reals nil)
(- const-decl "[numfield -> numfield]" number_fields nil)
(open_interval type-eq-decl nil intervals_real "reals/")
(step_function? const-decl "bool" step_fun_def nil)
(- 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_plus_real_is_real application-judgement "real" reals nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(T formal-nonempty-subtype-decl nil step_fun_props nil)
(T_pred const-decl "[real -> boolean]" step_fun_props 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)
(diff_step_is_step-2 nil 3292077219
("" (skosimp*)
(("" (lemma "sum_step_is_step[T]")
(("" (inst?)
(("" (inst - "-g!1")
(("" (assert)
(("" (expand "+ ")
((""
(case-replace
"(LAMBDA (x: T): (-g!1)(x) + f!1(x)) = f!1 - g!1")
(("1" (split -2)
(("1" (propax) nil nil)
("2" (hide 2)
(("2" (hide -1 -3)
(("2" (expand "step_function?")
(("2" (expand "step_function_on?")
(("2" (skosimp*)
(("2" (inst + "P!1")
(("2"
(skosimp*)
(("2"
(inst - "ii!1")
(("2"
(skosimp*)
(("2"
(inst + "-fv!1")
(("2"
(skosimp*)
(("2"
(inst?)
(("2"
(expand "-")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (apply-extensionality 1 :hide? t)
(("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((step_function? const-decl "bool" step_fun_def nil)
(partition type-eq-decl nil integral_def nil)
(step_function_on? const-decl "bool" step_fun_def nil)
(+ const-decl "[T -> real]" real_fun_ops "reals/"))
nil)
(diff_step_is_step-1 nil 3280231893
("" (skosimp*)
(("" (lemma "sum_step_is_step[T]")
(("" (inst?)
(("" (inst - "-g!1")
(("" (assert)
(("" (expand "+ ")
((""
(case-replace
"(LAMBDA (x: T): (-g!1)(x) + f!1(x)) = f!1 - g!1")
(("1" (split -2)
(("1" (propax) nil nil)
("2" (hide 2)
(("2" (hide -1 -3)
(("2" (expand "step_function?")
(("2" (skosimp*)
(("2" (inst + "P!1")
(("2" (skosimp*)
(("2"
(inst - "ii!1")
(("2"
(skosimp*)
(("2"
(inst + "-fv!1")
(("2"
(skosimp*)
(("2"
(inst?)
(("2"
(expand "-")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (apply-extensionality 1 :hide? t)
(("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((+ const-decl "[T -> real]" real_fun_ops "reals/")
(partition type-eq-decl nil integral_def nil)
(step_function? const-decl "bool" step_fun_def nil))
nil))
(step_function_subrng_TCC1 0
(step_function_subrng_TCC1-1 nil 3319455497
("" (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)
(T_pred const-decl "[real -> boolean]" step_fun_props nil)
(T formal-nonempty-subtype-decl nil step_fun_props 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))
nil))
(step_function_subrng 0
(step_function_subrng-1 nil 3319455758
("" (skosimp*)
(("" (expand "step_function?")
(("" (expand "step_function_on?")
(("" (skosimp*)
((""
(name "ib"
"min_nat.min({ii: below(length(P!1)) | seq(P!1)(ii) > b!1})")
(("1"
(name "ic"
"max_below[length(P!1)].max({ii: below(length(P!1)) | seq(P!1)(ii) < c!1})")
(("1" (name "SP" "P!1^(ib,ic)")
(("1" (case "ib <= ic")
(("1"
(case "seq(P!1)(ib) > b!1 and seq(P!1)(ic) < c!1")
(("1" (flatten)
(("1"
(case "P!1(ib-1) <= b!1 AND P!1(ic+1) >= c!1")
(("1" (inst + "#(b!1) o SP o #(c!1)")
(("1" (skosimp*)
(("1" (assert)
(("1"
(inst - "ii!1+ib-1")
(("1"
(skosimp*)
(("1"
(inst + "fv!1")
(("1"
(skosimp*)
(("1"
(inst - "x!1")
(("1"
(typepred "x!1")
(("1"
(typepred "ii!1")
(("1"
(replace -10 * rl)
(("1"
(expand "o ")
(("1"
(expand "#")
(("1"
(expand "^")
(("1"
(assert)
(("1"
(lift-if)
(("1"
(hide -6)
(("1"
(hide -9)
(("1"
(lemma
"parts_order[T]")
(("1"
(inst
-
"a!1"
"d!1"
"P!1"
"ib"
"ib+ii!1-1")
(("1"
(assert)
(("1"
(expand
"min")
(("1"
(assert)
(("1"
(ground)
(("1"
(case-replace
"ii!1 = 1 - ib + ic")
(("1"
(assert)
nil
nil)
("2"
(name-replace
"IBB"
"ib")
(("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)
("2"
(assert)
(("2"
(hide 2)
(("2"
(typepred "ii!1")
(("2"
(replace -7 * rl)
(("2"
(hide -7)
(("2"
(expand "#")
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (expand "#")
(("2"
(expand "o")
(("2"
(split +)
(("1"
(skosimp*)
(("1"
(typepred "x1!1")
(("1"
(hide -8 -9 -13)
(("1"
(replace -7 * rl)
(("1"
(hide -7)
(("1"
(expand "#")
(("1"
(grind)
(("1"
(lemma
"parts_order[T]")
(("1"
(inst
-
"a!1"
"d!1"
"P!1"
"x1!1 + ib -1"
"ic")
(("1"
(assert)
nil
nil))
nil))
nil)
("2"
(lemma
"parts_order[T]")
(("2"
(inst
-
"a!1"
"d!1"
"P!1"
"ib"
"x1!1 + ib -1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert) nil nil)
("3"
(ground)
(("3"
(replace -6 * rl)
(("3"
(hide-all-but 1)
(("3" (grind) nil nil))
nil))
nil))
nil)
("4"
(flatten)
(("4"
(skosimp*)
(("4"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.85 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.
|
