|
(step_fun_scaf
(IMP_partitions_scaf_TCC1 0
(IMP_partitions_scaf_TCC1-1 nil 3281261029
("" (lemma "connected_domain")
(("" (expand "connected?") (("" (propax) nil nil)) nil)) nil)
((connected_domain formula-decl nil step_fun_scaf nil)) shostak))
(IMP_partitions_scaf_TCC2 0
(IMP_partitions_scaf_TCC2-1 nil 3281261029
("" (lemma "not_one_element")
(("" (expand "not_one_element?") (("" (propax) nil nil)) nil)) nil)
((not_one_element formula-decl nil step_fun_scaf nil)) shostak))
(UP_prep 0
(UP_prep-1 nil 3281208248
("" (skosimp*)
(("" (assert)
(("" (lemma "part2set_lem")
(("" (inst?)
(("" (assert)
(("" (flatten)
(("" (prop)
(("1" (rewrite "card_union[T]")
(("1" (lemma "card_intersection_le[T]")
(("1" (inst?)
(("1" (assert)
(("1" (flatten)
(("1" (assert)
(("1" (lemma "card_part2set")
(("1"
(inst?)
(("1"
(lemma "card_part2set")
(("1"
(inst - "a!1" "b!1" "P2!1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "union")
(("2" (expand "member") (("2" (assert) nil nil))
nil))
nil)
("3" (expand "union")
(("3" (expand "member") (("3" (assert) 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)
(nil application-judgement "{s: finite_set[T] | card(s) > 1}"
step_fun_scaf nil)
(finite_union application-judgement "finite_set[T]" step_fun_scaf
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)
(union const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(card_union formula-decl nil finite_sets nil)
(set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(part2set const-decl "finite_set[T]" partitions_scaf nil)
(finite_intersection2 application-judgement "finite_set[T]"
step_fun_scaf nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
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)
(card_intersection_le formula-decl nil finite_sets nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(part2set_lem formula-decl nil partitions_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_scaf nil)
(T formal-nonempty-subtype-decl nil step_fun_scaf nil))
shostak))
(UnionPart_TCC1 0
(UnionPart_TCC1-1 nil 3281186001
("" (skosimp*)
(("" (rewrite "card_union")
(("" (lemma "card_part2set[T]")
(("" (inst?)
(("" (assert)
(("" (lemma "card_part2set[T]")
(("" (inst - "a!1" "b!1" "P2!1")
(("" (assert)
(("" (lemma "card_intersection_le[T]")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((card_union formula-decl nil finite_sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets 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)
(part2set const-decl "finite_set[T]" partitions_scaf 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)
(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_scaf nil)
(T formal-nonempty-subtype-decl nil step_fun_scaf nil)
(finite_intersection2 application-judgement "finite_set[T]"
step_fun_scaf nil)
(nil application-judgement "{s: finite_set[T] | card(s) > 1}"
step_fun_scaf nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(card_intersection_le formula-decl nil finite_sets 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)
(card_part2set formula-decl nil partitions_scaf nil))
shostak))
(UnionPart_TCC2 0
(UnionPart_TCC2-1 nil 3281186001
("" (skosimp*)
((""
(case "seq
(set2part(union[T]
(part2set(a!1, b!1, P1!1),
part2set(a!1, b!1, P2!1))))
(0)
= a!1")
(("1"
(case "seq
(set2part(union[T]
(part2set(a!1, b!1, P1!1),
part2set(a!1, b!1, P2!1))))
(length
(set2part(union[T]
(part2set(a!1, b!1, P1!1),
part2set(a!1, b!1, P2!1))))
- 1)
= b!1")
(("1"
(name "UP" "union[T]
(part2set(a!1, b!1, P1!1),
part2set(a!1, b!1, P2!1))")
(("1" (replace -1)
(("1" (case "seq(set2part(UP))(0) = a!1")
(("1"
(case "seq(set2part(UP))(length(set2part(UP)) - 1) = b!1")
(("1" (assert)
(("1" (prop)
(("1" (skosimp*)
(("1" (lemma "UP_prep")
(("1" (inst?)
(("1" (assert)
(("1" (flatten)
(("1"
(typepred "set2part(UP)")
(("1"
(prop)
(("1"
(hide -3)
(("1"
(lemma "parts_order[T]")
(("1"
(inst
-
"a!1"
"b!1"
"set2part(UP)"
"0"
"x1!1")
(("1" (assert) nil nil)
("2" (assert) nil nil)
("3" (assert) nil nil))
nil))
nil))
nil)
("2"
(lemma "parts_order[T]")
(("2"
(inst
-
"a!1"
"b!1"
"set2part(UP)"
"x1!1"
"length(set2part(UP))-1")
(("1" (assert) nil nil)
("2" (assert) nil nil)
("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (typepred "set2part(UP)")
(("2" (inst - "ii!1") nil nil)) nil))
nil))
nil))
nil)
("2" (propax) nil nil) ("3" (assert) nil nil))
nil)
("2" (propax) nil nil)
("3" (assert)
(("3" (hide 2)
(("3" (lemma "UP_prep")
(("3" (inst?) (("3" (assert) nil nil)) nil)) nil))
nil))
nil)
("4" (assert) nil nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (lemma "max_lem[T,<=]")
(("2" (hide -2)
(("2"
(name "UP" "union[T]
(part2set(a!1, b!1, P1!1),
part2set(a!1, b!1, P2!1))")
(("2" (replace -1)
(("2" (inst - "UP" "b!1")
(("1" (assert)
(("1" (hide 2)
(("1" (lemma "UP_prep")
(("1" (inst?)
(("1" (assert)
(("1"
(flatten)
(("1"
(assert)
(("1"
(skosimp*)
(("1"
(typepred "x!1")
(("1"
(replace -6 - rl)
(("1"
(expand "union")
(("1"
(expand "member")
(("1"
(split -2)
(("1"
(lemma "part2set_lem")
(("1"
(inst?)
(("1"
(flatten)
(("1"
(inst -4 "x!1")
(("1"
(flatten)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(lemma "part2set_lem")
(("2"
(inst
-
"a!1"
"b!1"
"P2!1")
(("2"
(flatten)
(("2"
(inst -4 "x!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "empty?")
(("2" (expand "member")
(("2" (inst - "a!1")
(("2" (lemma "UP_prep")
(("2" (inst?)
(("2"
(assert)
(("2"
(flatten)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 2) (("3" (assert) nil nil)) nil))
nil)
("2" (hide 2)
(("2" (lemma "min_lem[T,<=]")
(("2"
(name "UP" "union[T]
(part2set(a!1, b!1, P1!1),
part2set(a!1, b!1, P2!1))")
(("2" (replace -1)
(("2" (inst - "UP" "a!1")
(("1" (assert)
(("1" (hide 2)
(("1" (lemma "UP_prep")
(("1" (inst?)
(("1" (assert)
(("1" (flatten)
(("1" (assert)
(("1"
(skosimp*)
(("1"
(typepred "x!1")
(("1"
(replace -6 * rl)
(("1"
(expand "union")
(("1"
(expand "member")
(("1"
(split -2)
(("1"
(lemma "part2set_lem")
(("1"
(inst?)
(("1"
(flatten)
(("1"
(inst -4 "x!1")
(("1"
(flatten)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(lemma "part2set_lem")
(("2"
(inst
-
"a!1"
"b!1"
"P2!1")
(("2"
(flatten)
(("2"
(inst -4 "x!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "empty?")
(("2" (expand "member")
(("2" (inst - "a!1")
(("2" (assert)
(("2" (lemma "UP_prep")
(("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (hide 2)
(("3" (assert)
(("3" (lemma "UP_prep")
(("3" (inst?) (("3" (assert) nil nil)) nil)) nil))
nil))
nil)
("4" (hide 2) (("4" (assert) 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/")
(part2set const-decl "finite_set[T]" partitions_scaf nil)
(union const-decl "set" sets nil)
(set2part const-decl
"partition[T](min[T, restrict[[real, real], [T, T], boolean](<=)](S),
max[T, restrict[[real, real], [T, T], boolean](<=)](S))"
partitions_scaf nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(max const-decl
"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}"
finite_sets_minmax "finite_sets/")
(min const-decl
"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES a <= x)}"
finite_sets_minmax "finite_sets/")
(restrict const-decl "R" restrict nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(empty? const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(below type-eq-decl nil nat_types nil)
(card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
(Card const-decl "nat" finite_sets nil)
(nat nonempty-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 "bool" reals nil)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-nonempty-subtype-decl nil step_fun_scaf nil)
(T_pred const-decl "[real -> boolean]" step_fun_scaf 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(finite_union application-judgement "finite_set[T]" step_fun_scaf
nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nil application-judgement "{s: finite_set[T] | card(s) > 1}"
step_fun_scaf nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(P1!1 skolem-const-decl "partition[T](a!1, b!1)" step_fun_scaf nil)
(x!1 skolem-const-decl "(UP)" step_fun_scaf nil)
(part2set_lem formula-decl nil partitions_scaf nil)
(P2!1 skolem-const-decl "partition[T](a!1, b!1)" step_fun_scaf nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(member const-decl "bool" sets nil)
(UP skolem-const-decl "finite_set[T]" step_fun_scaf nil)
(max_lem formula-decl nil finite_sets_minmax "finite_sets/")
(parts_order formula-decl nil integral_def nil)
(b!1 skolem-const-decl "{x: T | a!1 < x}" step_fun_scaf nil)
(a!1 skolem-const-decl "T" step_fun_scaf nil)
(UP skolem-const-decl "finite_set[T]" step_fun_scaf nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(UP_prep formula-decl nil step_fun_scaf nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(min_lem formula-decl nil finite_sets_minmax "finite_sets/")
(x!1 skolem-const-decl "(UP)" step_fun_scaf nil)
(UP skolem-const-decl "finite_set[T]" step_fun_scaf nil))
shostak))
(UnionPart_lem_TCC1 0
(UnionPart_lem_TCC1-1 nil 3293192377
("" (skosimp*) (("" (typepred "kk!1") (("" (assert) nil nil)) nil))
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 "[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)
(T formal-nonempty-subtype-decl nil step_fun_scaf nil)
(T_pred const-decl "[real -> boolean]" step_fun_scaf nil)
(below type-eq-decl nil nat_types nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(nat nonempty-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 "bool" reals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number nonempty-type-decl nil numbers nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil))
shostak))
(UnionPart_lem 0
(UnionPart_lem-1 nil 3293192355
("" (skosimp*)
(("" (expand "UnionPart")
(("" (lemma "part2set_lem[T]")
(("" (inst?)
(("" (flatten)
(("" (assert)
(("" (inst -3 "kk!1")
((""
(case "union(part2set(a!1, b!1, P1!1),
part2set(a!1, b!1, P2!1))(P1!1`seq(kk!1))")
(("1" (lemma "set2part_ix[T]")
(("1" (inst?)
(("1" (assert)
(("1" (split -1)
(("1" (skosimp*)
(("1" (inst + "ii!1")
(("1" (assert) nil nil)
("2"
(typepred "ii!1")
(("2"
(assert)
(("2"
(expand "UnionPart")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (lemma "UP_prep")
(("2"
(inst?)
(("2"
(assert)
(("2" (flatten) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "union")
(("2" (expand "member") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((UnionPart const-decl "partition[T](a, b)" step_fun_scaf 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)
(nil application-judgement "{s: finite_set[T] | card(s) > 1}"
step_fun_scaf nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(part2set const-decl "finite_set[T]" partitions_scaf nil)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(union const-decl "set" sets nil) (set type-eq-decl nil sets nil)
(finite_union application-judgement "finite_set[T]" step_fun_scaf
nil)
(ii!1 skolem-const-decl "below(length
(set2part(union(part2set(a!1, b!1, P1!1),
part2set(a!1, b!1, P2!1)))))" step_fun_scaf
nil)
(P2!1 skolem-const-decl "partition[T](a!1, b!1)" step_fun_scaf nil)
(P1!1 skolem-const-decl "partition[T](a!1, b!1)" step_fun_scaf nil)
(b!1 skolem-const-decl "{x: T | a!1 < x}" step_fun_scaf nil)
(a!1 skolem-const-decl "T" step_fun_scaf nil)
(set2part const-decl
"partition[T](min[T, restrict[[real, real], [T, T], boolean](<=)](S),
max[T, restrict[[real, real], [T, T], boolean](<=)](S))"
partitions_scaf nil)
(max const-decl
"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}"
finite_sets_minmax "finite_sets/")
(min const-decl
"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES a <= x)}"
finite_sets_minmax "finite_sets/")
(restrict const-decl "R" restrict nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(empty? const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
(Card const-decl "nat" finite_sets nil)
(UP_prep formula-decl nil step_fun_scaf nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(set2part_ix formula-decl nil partitions_scaf nil)
(member const-decl "bool" sets nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(part2set_lem formula-decl nil partitions_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_scaf nil)
(T formal-nonempty-subtype-decl nil step_fun_scaf nil))
nil))
(Union_sym 0
(Union_sym-1 nil 3281201902
("" (skosimp*)
(("" (expand "UnionPart")
(("" (lemma "union_commutative[T]")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil)
((UnionPart const-decl "partition[T](a, b)" step_fun_scaf nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets 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)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(part2set const-decl "finite_set[T]" partitions_scaf 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)
(finite_union application-judgement "finite_set[T]" step_fun_scaf
nil)
(nil application-judgement "{s: finite_set[T] | card(s) > 1}"
step_fun_scaf nil)
(union_commutative formula-decl nil sets_lemmas 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_scaf nil)
(T formal-nonempty-subtype-decl nil step_fun_scaf nil))
nil))
(Union_lem_TCC1 0
(Union_lem_TCC1-1 nil 3281201972
("" (skosimp*)
(("" (assert)
(("" (typepred "nn!1") (("" (postpone) nil nil)) 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))
(Union_lem_TCC2 0
(Union_lem_TCC2-1 nil 3281201972
("" (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))
(Union_lem_TCC3 0
(Union_lem_TCC3-1 nil 3281209463
("" (skosimp*) (("" (assert) nil nil)) nil)
((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(real_le_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))
(Union_lem_TCC4 0
(Union_lem_TCC4-1 nil 3281879472 ("" (subtype-tcc) nil nil)
((T formal-nonempty-subtype-decl nil step_fun_scaf nil)
(T_pred const-decl "[real -> boolean]" step_fun_scaf 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)
(set2part const-decl
"partition[T](min[T, restrict[[real, real], [T, T], boolean](<=)](S),
max[T, restrict[[real, real], [T, T], boolean](<=)](S))"
partitions_scaf nil)
(UnionPart const-decl "partition[T](a, b)" step_fun_scaf nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil))
shostak))
(Union_lem 0
(Union_lem-2 nil 3306073304
("" (skosimp*)
(("" (assert)
((""
(case " nonempty?[below[length(P1!1) - 1]]
({kk: below(length(P1!1) - 1) |
seq(P1!1)(kk) <=
UnionPart(a!1, b!1, P1!1, P2!1)`seq(nn!1)})")
(("1"
(inst +
"max[length(P1!1)-1]({kk: below(length(P1!1) - 1) | seq(P1!1)(kk) <= UnionPart(a!1, b!1, P1!1, P2!1)`seq(nn!1)})")
(("1"
(name-replace "MAX" "max[length(P1!1) - 1]
({kk: below(length(P1!1) - 1) |
seq(P1!1)(kk) <=
UnionPart(a!1, b!1, P1!1, P2!1)`seq(nn!1)})")
(("1" (assert)
(("1" (typepred "MAX")
(("1" (assert)
(("1" (ground)
(("1" (inst - "MAX+1")
(("1" (ground)
(("1" (lemma "UnionPart_lem")
(("1" (inst?)
(("1"
(name "UP"
"UnionPart(a!1, b!1, P1!1, P2!1)")
(("1"
(replace -1)
(("1"
(inst -2 "MAX+1")
(("1"
(skosimp*)
(("1"
(assert)
(("1"
(replace -2 * rl)
(("1"
(lemma "parts_order[T]")
(("1"
(inst
-
"a!1"
"b!1"
"UP"
"nn!2"
"nn!1")
(("1"
(lemma "parts_order[T]")
(("1"
(inst
-
"a!1"
"b!1"
"UP"
"nn!1"
"nn!2+1")
(("1"
(lemma
"parts_order[T]")
(("1"
(inst
-
"a!1"
"b!1"
"UP"
"nn!1+1"
"nn!2")
(("1"
(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" (hide 2)
(("2" (expand "nonempty?")
(("2" (expand "empty?")
(("2" (expand "member")
(("2" (inst - "0") (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
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)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
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)
(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_scaf
nil)
(P2!1 skolem-const-decl "partition[T](a!1, b!1)" step_fun_scaf nil)
(P1!1 skolem-const-decl "partition[T](a!1, b!1)" step_fun_scaf nil)
(b!1 skolem-const-decl "{x_1: T | a!1 < x_1}" step_fun_scaf nil)
(a!1 skolem-const-decl "T" step_fun_scaf nil)
(max const-decl
"{a: below[N] | S(a) AND (FORALL x: S(x) IMPLIES a >= x)}"
max_below "ints/")
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(UnionPart_lem formula-decl nil step_fun_scaf nil)
(parts_order formula-decl nil integral_def 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)
(< 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]" step_fun_scaf nil)
(T formal-nonempty-subtype-decl nil step_fun_scaf 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)
(below type-eq-decl nil naturalnumbers nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(partition type-eq-decl nil integral_def nil)
(set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(UnionPart const-decl "partition[T](a, b)" step_fun_scaf nil))
nil)
(Union_lem-1 nil 3281201933
("" (skosimp*)
(("" (assert)
((""
(case " nonempty?[below[length(P1!1) - 1]]
({kk: below(length(P1!1) - 1) |
seq(P1!1)(kk) <=
UnionPart[T](a!1, b!1, P1!1, P2!1)`seq(nn!1)})")
(("1"
(inst +
"max[length(P1!1)-1]({kk: below(length(P1!1) - 1) | seq(P1!1)(kk) <= UnionPart(a!1, b!1, P1!1, P2!1)`seq(nn!1)})")
(("1"
(name-replace "MAX" "max[length(P1!1) - 1]
({kk: below(length(P1!1) - 1) |
seq(P1!1)(kk) <=
UnionPart(a!1, b!1, P1!1, P2!1)`seq(nn!1)})")
(("1" (assert)
(("1" (typepred "MAX")
(("1" (assert)
(("1" (ground)
(("1" (inst - "MAX+1")
(("1" (ground)
(("1" (lemma "UnionPart_lem")
(("1" (inst?)
(("1"
(name "UP"
"UnionPart(a!1, b!1, P1!1, P2!1)")
(("1"
(replace -1)
(("1"
(inst -2 "MAX+1")
(("1"
(skosimp*)
(("1"
(assert)
(("1"
(replace -2 * rl)
(("1"
(lemma "parts_order[T]")
(("1"
(inst
-
"a!1"
"b!1"
"UP"
"nn!2"
"nn!1")
(("1"
(lemma "parts_order[T]")
(("1"
(inst
-
"a!1"
"b!1"
"UP"
"nn!1"
"nn!2+1")
(("1"
(lemma
"parts_order[T]")
(("1"
(inst
-
"a!1"
"b!1"
"UP"
"nn!1+1"
"nn!2")
(("1"
(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" (hide 2)
(("2" (expand "nonempty?")
(("2" (expand "empty?")
(("2" (expand "member")
(("2" (inst - "0") (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((parts_order formula-decl nil integral_def nil)
(partition type-eq-decl nil integral_def nil))
nil)))
¤ Dauer der Verarbeitung: 0.226 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.
|
