|
(integral_split
(partition_join_TCC1 0
(partition_join_TCC1-1 nil 3281885132
("" (lemma "connected_domain") (("" (skosimp*) nil nil)) nil)
((connected_domain formula-decl nil integral_split nil)) shostak))
(partition_join_TCC2 0
(partition_join_TCC2-1 nil 3282313772
("" (lemma "not_one_element") (("" (assert) nil nil)) nil)
((not_one_element formula-decl nil integral_split nil)) shostak))
(partition_join_TCC3 0
(partition_join_TCC3-1 nil 3282313772
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(partition_join 0
(partition_join-3 nil 3399973962
("" (auto-rewrite "xis?")
(("" (auto-rewrite "xis_lem")
(("" (skosimp*)
(("" (typepred "xisa!1")
(("" (typepred "xisb!1")
(("" (expand "xis?")
(("" (assert)
((""
(inst + "UUPart(a!1,b!1,c!1,Pa!1,Pb!1)"
"xisa!1 o xisb!1")
(("1" (split +)
(("1" (hide -1 -2)
(("1" (expand "width")
(("1" (lemma "connected_domain")
(("1"
(name "LUU" "{l: real |
EXISTS (ii: below(length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) - 1)):
l = seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(1 + ii)
- seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(ii)}")
(("1" (replace -1)
(("1"
(case
"is_finite[real](LUU) AND NOT empty?[real](LUU)")
(("1"
(name
"LA"
"{l: real | EXISTS (ii: below(length(Pa!1) - 1)):
l = seq(Pa!1)(1 + ii) - seq(Pa!1)(ii)}")
(("1"
(replace -1)
(("1"
(name
"LB"
"{l: real | EXISTS (ii: below(length(Pb!1) - 1)):
l = seq(Pb!1)(1 + ii) - seq(Pb!1)(ii)}")
(("1"
(replace -1)
(("1"
(case
"is_finite[real](LA) AND NOT empty?[real](LA)")
(("1"
(case
"is_finite[real](LB) AND NOT empty?[real](LB)")
(("1"
(typepred "max(LUU)")
(("1"
(replace -8 -1 rl)
(("1"
(assert)
(("1"
(skosimp*)
(("1"
(replace -8)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(expand
"UUPart")
(("1"
(ground)
(("1"
(lift-if)
(("1"
(case
"1 + ii!1 < length(Pa!1)")
(("1"
(assert)
(("1"
(typepred
"max(LA)")
(("1"
(inst
-2
"Pa!1`seq(1 + ii!1) - Pa!1`seq(ii!1)")
(("1"
(assert)
(("1"
(replace
-7
+
rl)
(("1"
(assert)
(("1"
(inst?)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(lift-if)
(("2"
(case-replace
"ii!1 = length(Pa!1) - 1")
(("1"
(case-replace
"Pa!1`seq(length(Pa!1) - 1) = Pb!1`seq(0)")
(("1"
(assert)
(("1"
(typepred
"max(LB)")
(("1"
(replace
-8
-1
rl)
(("1"
(assert)
(("1"
(skosimp*)
(("1"
(replace
-8)
(("1"
(inst
-2
"Pb!1`seq(1) - Pb!1`seq(0)")
(("1"
(assert)
(("1"
(replace
-7
+
rl)
(("1"
(assert)
(("1"
(inst
1
"0")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
nil
nil))
nil)
("2"
(assert)
(("2"
(typepred
"max(LB)")
(("2"
(replace
-6
-1
rl)
(("2"
(assert)
(("2"
(skosimp*)
(("2"
(replace
-6)
(("2"
(inst
-2
"Pb!1`seq(2 - length(Pa!1) + ii!1) - Pb!1`seq(1 - length(Pa!1) + ii!1)")
(("2"
(assert)
(("2"
(replace
-5
1
rl)
(("2"
(assert)
(("2"
(inst
1
"1-length(Pa!1)+ii!1")
(("1"
(assert)
nil
nil)
("2"
(assert)
(("2"
(hide
-5
-6
-8)
(("2"
(hide
-2
-3
-4
-5
-6)
(("2"
(typepred
"ii!1")
(("2"
(assert)
(("2"
(expand
"UUPart")
(("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))
nil))
nil)
("2"
(replace -2 * rl)
(("2"
(hide-all-but 1)
(("2"
(split +)
(("1"
(lemma
"is_finite_surj")
(("1"
(inst?)
(("1"
(assert)
(("1"
(hide 2)
(("1"
(inst
+
"length(Pb!1)-1"
"(LAMBDA (ii: below(length(Pb!1) - 1)):
seq(Pb!1)(1 + ii) - seq(Pb!1)(ii))")
(("1"
(expand
"surjective?")
(("1"
(skosimp*)
(("1"
(typepred
"y!1")
(("1"
(skosimp*)
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(inst?)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "empty?")
(("2"
(expand "member")
(("2"
(inst
-
"seq(Pb!1)(1) - seq(Pb!1)(0)")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace -2 * rl)
(("2"
(hide-all-but 1)
(("2"
(split +)
(("1"
(lemma
"is_finite_surj")
(("1"
(inst?)
(("1"
(assert)
(("1"
(hide 2)
(("1"
(inst
+
"length(Pa!1)-1"
"(LAMBDA (ii: below(length(Pa!1) - 1)):
seq(Pa!1)(1 + ii) - seq(Pa!1)(ii))")
(("1"
(expand
"surjective?")
(("1"
(skosimp*)
(("1"
(typepred
"y!1")
(("1"
(skosimp*)
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(inst?)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "empty?")
(("2"
(inst
-
"seq(Pa!1)(1) - seq(Pa!1)(0)")
(("2"
(expand "member")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(replace -1 * rl)
(("2"
(hide-all-but 1)
(("2"
(split +)
(("1"
(lemma "is_finite_surj")
(("1"
(inst?)
(("1"
(assert)
(("1"
(hide 2)
(("1"
(inst
+
"length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))-1"
"(LAMBDA (ii: below(length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) - 1)):
seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(1 + ii)
- seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(ii))")
(("1"
(expand
"surjective?")
(("1"
(skosimp*)
(("1"
(typepred "y!1")
(("1"
(skosimp*)
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(inst?)
nil
nil))
nil)
("3"
(lemma
"connected_domain")
(("3"
(skosimp*)
nil
nil))
nil)
("4"
(expand "UUPart")
(("4"
(assert)
nil
nil))
nil)
("5"
(lemma
"connected_domain")
(("5"
(propax)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(lemma
"connected_domain")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil)
("2"
(expand "empty?")
(("2"
(expand "member")
(("2"
(inst
-
"seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(1) -
seq(UUPart(a!1, b!1, c!1, Pa!1, Pb!1))(0)")
(("1"
(assert)
(("1"
(inst + "0")
(("1" (assert) nil nil)
("2"
(expand "UUPart")
(("2"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(expand "UUPart")
(("2" (assert) nil nil))
nil)
("3"
(lemma
"connected_domain")
(("3" (propax) nil nil))
nil)
("4"
(expand "UUPart")
(("4" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*) nil nil))
nil))
nil))
nil))
nil)
("2" (hide -1 -2)
(("2" (expand "Rie_sum")
(("2" (assert)
(("1"
(case " length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) = length(Pa!1) + length(Pb!1) - 1")
(("1"
(same-name "sigma[below(length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) - 1)]"
"sigma[below(length(Pa!1) + length(Pb!1) - 2)]")
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(assert)
(("1"
(lemma
"sigma_split[below(length(Pa!1) + length(Pb!1) - 2)]")
(("1"
(inst?)
(("1"
(assert)
(("1"
(inst - "length(Pa!1) - 2")
(("1"
(assert)
(("1"
(replace -2)
(("1"
(assert)
(("1"
(replace -1)
(("1"
(hide -1)
(("1"
(case-replace
"sigma[below(length(Pa!1) + length(Pb!1) - 2)].sigma(0, length(Pa!1) - 2,
LAMBDA (n: below(length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) - 1)):
UUPart(a!1, b!1, c!1, Pa!1, Pb!1)`seq(1 + n) *
f!1((concat_arrays.o(xisa!1, xisb!1))(n))
- UUPart(a!1, b!1, c!1, Pa!1, Pb!1)`seq(n) *
f!1((concat_arrays.o(xisa!1, xisb!1))(n)))
= sigma[below(length(Pa!1) - 1)]
(0, length(Pa!1) - 2,
LAMBDA (n: below(length(Pa!1) - 1)):
Pa!1`seq(1 + n) * f!1(xisa!1(n)) -
Pa!1`seq(n) * f!1(xisa!1(n)))")
(("1"
(assert)
(("1"
(hide -1)
(("1"
(lemma
"sigma_diff_shift[length(Pb!1) - 1,length(Pa!1) + length(Pb!1) - 2
]")
(("1"
(inst
-
"(LAMBDA (n: below(length(Pb!1) - 1)):
Pb!1`seq(1 + n) * f!1(xisb!1(n)) -
Pb!1`seq(n) * f!1(xisb!1(n)))"
"(LAMBDA (n:
below(length(UUPart(a!1, b!1, c!1, Pa!1, Pb!1)) -
1)):
UUPart(a!1, b!1, c!1, Pa!1, Pb!1)`seq(1 + n) *
f!1((concat_arrays.o(xisa!1, xisb!1))(n))
-
UUPart(a!1, b!1, c!1, Pa!1, Pb!1)`seq(n) *
f!1((concat_arrays.o(xisa!1, xisb!1))(n)))"
"length(Pa!1) - 1"
"length(Pb!1) - 2"
"0")
(("1"
(assert)
(("1"
(hide
2)
(("1"
(skosimp*)
(("1"
(expand
"UUPart")
(("1"
(assert)
(("1"
(expand
"o ")
(("1"
(lift-if)
(("1"
(ground)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(skosimp*)
(("2"
(assert)
(("2"
(ground)
nil
nil))
nil))
nil))
nil)
("3"
(hide
2)
(("3"
(lemma
"connected_domain")
(("3"
(skosimp*)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(lemma
"sigma_diff_eq[length(Pa!1) + length(Pb!1) - 2
,length(Pa!1) - 1]")
(("2"
(lemma
"connected_domain")
(("2"
(lemma
"sigma_diff_eq[length(Pa!1) + length(Pb!1) - 2
,length(Pa!1) - 1]")
(("2"
(inst?)
(("1"
(assert)
(("1"
(hide
2)
(("1"
(skosimp*)
(("1"
(expand
"UUPart")
(("1"
(assert)
(("1"
(expand
"o ")
(("1"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide
2)
(("2"
(skosimp*)
(("2"
(assert)
(("2"
(ground)
nil
nil))
nil))
nil))
nil)
("3"
(hide
2)
(("3"
(skosimp*)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(hide 2)
(("3"
(skosimp*)
(("3"
(assert)
nil
nil))
nil))
nil)
("4"
(hide 2)
(("4"
(lemma
"connected_domain")
(("4"
(skosimp*)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(lemma "connected_domain")
(("2" (propax) nil nil))
nil))
nil)
("3"
(assert)
(("3"
(hide 2)
(("3"
(skosimp*)
(("3" (ground) nil nil))
nil))
nil))
nil)
("4"
(hide 2)
(("4"
(lemma "connected_domain")
(("4" (skosimp*) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(skosimp*)
(("2"
(expand "UUPart")
(("2" (propax) nil nil))
nil))
nil))
nil)
("3"
(hide 2)
(("3"
(skosimp*)
(("3" (assert) nil nil))
nil))
nil)
("4"
(hide 2)
(("4"
(skosimp*)
(("4" (assert) nil nil))
nil))
nil))
nil)
("2" (expand "UUPart")
(("2" (propax) nil nil)) nil)
("3" (lemma "connected_domain")
(("3" (propax) nil nil)) nil))
nil)
("2" (hide 2)
(("2" (assert) (("2" (assert) nil nil))
nil))
nil)
("3" (lemma "connected_domain")
(("3" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (split +)
(("1" (skosimp*)
(("1" (expand "UUPart") (("1" (propax) nil nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "o")
(("2" (assert)
(("2" (lift-if) (("2" (ground) nil nil))
nil))
nil))
nil))
nil)
("3" (skosimp*)
(("3" (typepred "ii!1")
(("3" (expand "UUPart")
(("3" (expand "o")
(("3"
(case-replace "ii!1 < length(Pa!1) - 1")
(("1"
(inst -4 "ii!1")
(("1" (assert) nil nil))
nil)
("2"
(assert)
(("2"
(inst -2 "1 - length(Pa!1) + ii!1")
(("2"
(assert)
(("2"
(flatten)
(("2"
(lift-if)
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (lemma "connected_domain")
(("3" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((partition type-eq-decl nil integral_def nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(closed_interval type-eq-decl nil intervals_real "reals/")
(xis? const-decl "bool" 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) (<= 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)
(< const-decl "bool" reals nil)
(T formal-nonempty-subtype-decl nil integral_split nil)
(T_pred const-decl "[real -> boolean]" integral_split nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(connected? const-decl "bool" deriv_domain_def nil)
(xisb!1 skolem-const-decl "(xis?(b!1, c!1, Pb!1))" integral_split
nil)
(xisa!1 skolem-const-decl "(xis?(a!1, b!1, Pa!1))" integral_split
nil)
(O const-decl "below_array[n + m, T]" concat_arrays "structures/")
(below_array type-eq-decl nil below_arrays "structures/")
(UUPart const-decl "partition[T](a, c)" step_fun_props nil)
(Pb!1 skolem-const-decl "partition[T](b!1, c!1)" integral_split
nil)
(c!1 skolem-const-decl "T" integral_split nil)
(Pa!1 skolem-const-decl "partition[T](a!1, b!1)" integral_split
nil)
(b!1 skolem-const-decl "T" integral_split nil)
(a!1 skolem-const-decl "T" integral_split nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(not_one_element formula-decl nil integral_split nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(real_plus_real_is_real application-judgement "real" reals nil)
(integer nonempty-type-from-decl nil integers nil)
(sigma_split formula-decl nil sigma "reals/")
(sigma_diff_eq formula-decl nil sigma_below_sub "reals/")
(sigma_diff_shift formula-decl nil sigma_below_sub "reals/")
(sigma def-decl "real" sigma "reals/")
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(OR const-decl "[bool, bool -> bool]" booleans nil)
(T_high type-eq-decl nil sigma "reals/")
(T_low type-eq-decl nil sigma "reals/")
(Rie_sum const-decl "real" integral_def nil)
(real_times_real_is_real application-judgement "real" reals nil)
(connected_domain formula-decl nil integral_split nil)
(surjective? const-decl "bool" functions nil)
(is_finite_surj formula-decl nil finite_sets nil)
(member const-decl "bool" sets nil)
(odd_minus_odd_is_even application-judgement "even_int" integers
nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(finite_set type-eq-decl nil finite_sets nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(max const-decl
"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.53 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.
|
