|
(fseq2set
(bij_TCC1 0
(bij_TCC1-1 nil 3440769713 3440772507
("" (lemma "bij_exists")
((""
(inst + "(LAMBDA (S: finite_set[T]):
choose({f: [(S) -> below(card[T](S))] |
bijective?(f)}))")
(("" (skosimp*)
(("" (inst?)
(("" (skosimp*)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (expand "member") (("" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
unchecked
((boolean nonempty-type-decl nil booleans 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)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Card const-decl "nat" finite_sets nil)
(card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
(below type-eq-decl nil naturalnumbers nil)
(bijective? const-decl "bool" functions nil)
(nonempty? const-decl "bool" sets nil)
(choose const-decl "(p)" sets nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(bij_exists formula-decl nil finite_sets nil)
(T formal-type-decl nil fseq2set nil))
132 140 t nil))
(ibij_TCC1 0
(ibij_TCC1-1 nil 3440770452 3440772507
(""
(inst + "(LAMBDA (S: non_empty_finite_set[T]): inverse(bij(S)))")
(("" (skosimp*)
(("" (typepred "S!1")
(("" (expand "empty?")
(("" (expand "member")
(("" (hide -1) (("" (skosimp*) (("" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
unchecked
((non_empty_finite_set type-eq-decl nil finite_sets nil)
(empty? const-decl "bool" sets 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)
(T formal-type-decl nil fseq2set nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(member const-decl "bool" sets nil))
132 110 t nil))
(bij_ibij 0
(bij_ibij-1 nil 3440771597 3440772897
("" (skosimp*)
(("" (expand "ibij")
(("" (lemma "comp_inverse_right[(S!1),below(card(S!1))]")
(("" (inst?) nil nil)) nil))
nil))
nil)
unchecked
((ibij const-decl "{f: [below(card(S)) -> (S)] | bijective?(f)}"
fseq2set nil)
(bij const-decl "{f: [(S) -> below(card(S))] | bijective?(f)}"
fseq2set nil)
(bijective? const-decl "bool" functions nil)
(comp_inverse_right formula-decl nil function_inverse nil)
(T formal-type-decl nil fseq2set nil)
(boolean nonempty-type-decl nil booleans 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)
(NOT const-decl "[bool -> bool]" booleans nil)
(empty? const-decl "bool" sets nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Card const-decl "nat" finite_sets nil)
(card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
(below type-eq-decl nil naturalnumbers nil))
24 20 t shostak))
(ibij_bij 0
(ibij_bij-1 nil 3440771016 3440772897
("" (skosimp*)
(("" (assert)
(("" (expand "ibij")
(("" (assert)
(("" (lemma "bijective_inverse[(S!1),below(card(S!1))]")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
unchecked
((bijective_inverse_is_bijective application-judgement
"(bijective?[R, D])" function_inverse nil)
(unique_bijective_inverse application-judgement "{x: D | f(x) = y}"
function_inverse nil)
(bij const-decl "{f: [(S) -> below(card(S))] | bijective?(f)}"
fseq2set nil)
(bijective? const-decl "bool" functions nil)
(bijective_inverse formula-decl nil function_inverse nil)
(T formal-type-decl nil fseq2set nil)
(boolean nonempty-type-decl nil booleans 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)
(NOT const-decl "[bool -> bool]" booleans nil)
(empty? const-decl "bool" sets nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(Card const-decl "nat" finite_sets nil)
(card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
(below type-eq-decl nil naturalnumbers nil)
(ibij const-decl "{f: [below(card(S)) -> (S)] | bijective?(f)}"
fseq2set nil))
31 30 t shostak))
(seq2set_TCC1 0
(seq2set_TCC1-1 nil 3282912778 3440772507
("" (skosimp*)
(("" (assert)
(("" (lemma "is_finite_surj")
(("" (inst?)
(("" (assert)
(("" (hide 2)
((""
(inst + "length(fs!1)"
"(LAMBDA (ii: below(length(fs!1))):
seq(fs!1)(ii))")
(("1" (expand "surjective?")
(("1" (skosimp*)
(("1" (typepred "y!1")
(("1" (skosimp*)
(("1" (assert)
(("1" (inst?)
(("1" (assert)
(("1"
(expand "finseq_appl")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (assert)
(("2" (expand "finseq_appl")
(("2" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
unchecked
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(barray type-eq-decl nil fseqs "structures/")
(fseq type-eq-decl nil fseqs "structures/")
(below type-eq-decl nil naturalnumbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(surjective? const-decl "bool" functions nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(below type-eq-decl nil nat_types nil)
(is_finite_surj formula-decl nil finite_sets nil)
(T formal-type-decl nil fseq2set nil))
59 40 t shostak))
(seq2set_lem 0
(seq2set_lem-1 nil 3282915134 3440772897
("" (skosimp*)
(("" (expand "finseq_appl")
(("" (assert)
(("" (expand "seq2set")
(("" (expand "finseq_appl") (("" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil)
unchecked
((below type-eq-decl nil naturalnumbers nil)
(fseq type-eq-decl nil fseqs "structures/")
(barray type-eq-decl nil fseqs "structures/")
(T formal-type-decl nil fseq2set nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(seq2set const-decl "finite_set[T]" fseq2set nil))
35 20 t shostak))
(card_seq2set 0
(card_seq2set-2 "" 3283086594 3440772898
("" (skosimp*)
(("" (typepred "seq2set(fs!1)")
(("" (typepred "length(fs!1)")
(("" (expand "seq2set")
(("" (expand "finseq_appl")
(("" (lemma "seq2set_lem")
(("" (inst?)
(("" (assert)
(("" (expand "seq2set")
(("" (expand "finseq_appl")
(("" (lemma "Card_injection")
(("" (expand "injective?")
((""
(inst -1
"{s: T | EXISTS (kk: below(length(fs!1))): fs!1`seq(kk) = s}"
"length(fs!1)")
(("" (assert)
((""
(inst
+
"LAMBDA (f: {s: T | EXISTS (kk: below(length(fs!1))): fs!1`seq(kk) = s}): min( {kk: below(length(fs!1)) | fs!1`seq(kk) = f})")
(("1"
(skosimp*)
(("1" (assert) nil nil))
nil)
("2"
(skosimp*)
(("2"
(expand "nonempty?")
(("2"
(typepred "f!1")
(("2"
(skosimp*)
(("2"
(expand "empty?")
(("2"
(expand "member")
(("2"
(inst -2 "kk!1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
unchecked
((seq2set const-decl "finite_set[T]" fseq2set nil)
(finite_set type-eq-decl nil finite_sets nil)
(fseq type-eq-decl nil fseqs "structures/")
(barray type-eq-decl nil fseqs "structures/")
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(is_finite const-decl "bool" finite_sets nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil fseq2set nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(injective? const-decl "bool" functions nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(below type-eq-decl nil nat_types nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(<= const-decl "bool" reals nil)
(min const-decl "{a | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}"
min_nat nil)
(nonempty? const-decl "bool" sets nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(Card_injection formula-decl nil finite_sets nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(seq2set_lem formula-decl nil fseq2set 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))
231 190 t shostak)
(card_seq2set-1 nil 3282918983 3283085680
("" (skosimp*)
(("" (expand "seq2set")
(("" (expand "finseq_appl")
(("" (lemma "seq2set_lem")
(("" (inst?)
(("" (assert)
(("" (expand "seq2set")
(("" (expand "finseq_appl")
(("" (lemma "Card_injection")
(("" (expand "injective?")
((""
(inst -1
"{s: T | EXISTS (kk: below(length(fs!1))): fs!1`seq(kk) = s}"
"length(fs!1)")
(("1" (assert)
(("1" (hide 2)
(("1"
(inst +
"LAMBDA (s: {s: T | EXISTS (kk: below(length(fs!1))): fs!1`seq(kk) = s}): min( {kk: below(length(fs!1)) | fs!1`seq(kk) = s})")
(("1"
(skosimp*)
(("1"
(inst-cp
-2
"min({kk: below(length(fs!1)) | fs!1`seq(kk) = x1!1})")
(("1"
(inst
-2
"min({kk: below(length(fs!1)) | fs!1`seq(kk) = x2!1})")
(("1"
(skosimp*)
(("1" (assert) nil nil))
nil)
("2"
(skosimp*)
(("2" (assert) nil nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(reduce)
(("2"
(grind)
(("2" (postpone) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (postpone) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
unfinished nil 5068986 8940 t shostak))
(minmax_seq2set_TCC1 0
(minmax_seq2set_TCC1-1 nil 3282912778 3440772507
("" (skosimp*)
(("" (expand "empty?")
(("" (expand "member")
(("" (expand "seq2set")
(("" (inst - "ne_fs!1`seq(0)")
(("" (inst + "0")
(("" (assert)
(("" (expand "finseq_appl") (("" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
unchecked
((empty? const-decl "bool" sets nil)
(seq2set const-decl "finite_set[T]" fseq2set nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(ne_fseq type-eq-decl nil fseqs "structures/")
(> const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(fseq type-eq-decl nil fseqs "structures/")
(barray type-eq-decl nil fseqs "structures/")
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(T formal-type-decl nil fseq2set nil)
(member const-decl "bool" sets nil))
19 20 t shostak))
(minmax_seq2set 0
(minmax_seq2set-2 "" 3283271310 3440772898
("" (skosimp*)
(("" (typepred "seq2set(ne_fs!1)")
(("" (typepred "ne_fs!1")
(("" (split)
(("1" (typepred "min(ne_fs!1)")
(("1" (expand "seq2set")
(("1" (assert)
(("1" (skosimp*)
(("1" (expand "finseq_appl")
(("1" (inst?)
(("1" (lemma "seq2set_lem")
(("1" (inst?)
(("1" (expand "seq2set")
(("1" (expand "finseq_appl")
(("1"
(inst?)
(("1"
(lemma "min_seq_lem")
(("1"
(name
mm
"min[T, <=]({s: T | EXISTS (kk: below(length(ne_fs!1))): ne_fs!1`seq(kk) = s})")
(("1"
(replace -1)
(("1"
(typepred "mm")
(("1"
(skosimp*)
(("1"
(case "mm <= min(ne_fs!1)")
(("1"
(assert)
(("1"
(case
"min(ne_fs!1) <= mm")
(("1"
(assert)
(("1"
(typepred "<=")
(("1"
(expand
"total_order?")
(("1"
(flatten)
(("1"
(expand
"dichotomous?")
(("1"
(expand
"partial_order?")
(("1"
(expand
"antisymmetric?")
(("1"
(flatten)
(("1"
(inst
-2
"mm"
"min(ne_fs!1)")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(typepred "<=")
(("2"
(expand
"total_order?")
(("2"
(expand
"dichotomous?")
(("2"
(expand
"partial_order?")
(("2"
(flatten)
(("2"
(expand
"antisymmetric?")
(("2"
(inst
-8
"ne_fs!1"
"kk!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst? -2)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(skosimp*)
(("2"
(expand "empty?")
(("2"
(expand "member")
(("2"
(inst?)
(("2" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "max(ne_fs!1)")
(("2" (expand "seq2set")
(("2" (assert)
(("2" (skosimp*)
(("2" (expand "finseq_appl")
(("2" (inst?)
(("2" (lemma "seq2set_lem")
(("2" (inst?)
(("2" (expand "seq2set")
(("2" (expand "finseq_appl")
(("2"
(inst?)
(("2"
(lemma "max_seq_lem")
(("2"
(name
mm
" max[T, <=]
({s: T |
EXISTS (kk: below(length(ne_fs!1))): ne_fs!1`seq(kk) = s})")
(("1"
(replace -1)
(("1"
(typepred "mm")
(("1"
(skosimp*)
(("1"
(case "mm <= max(ne_fs!1)")
(("1"
(assert)
(("1"
(case
"max(ne_fs!1) <= mm")
(("1"
(assert)
(("1"
(typepred "<=")
(("1"
(expand
"total_order?")
(("1"
(flatten)
(("1"
(expand
"dichotomous?")
(("1"
(expand
"partial_order?")
(("1"
(expand
"antisymmetric?")
(("1"
(flatten)
(("1"
(inst
-2
"mm"
"max(ne_fs!1)")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(assert)
(("2"
(typepred "<=")
(("2"
(expand
"total_order?")
(("2"
(expand
"dichotomous?")
(("2"
(expand
"partial_order?")
(("2"
(flatten)
(("2"
(expand
"antisymmetric?")
(("2"
(expand
"preorder?")
(("2"
(expand
"reflexive?")
(("2"
(expand
"transitive?")
(("2"
(flatten)
(("2"
(lemma
"max_lem")
(("2"
(inst?
-1)
(("1"
(replace
-9)
(("1"
(assert)
(("1"
(flatten)
(("1"
(skosimp*)
(("1"
(inst?)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(expand
"empty?")
(("2"
(inst?)
(("2"
(expand
"member")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst?)
(("2"
(inst
-4
"ne_fs!1"
"kk!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(assert)
(("2"
(expand "empty?")
(("2"
(inst?)
(("2"
(expand "member")
(("2"
(inst 1 "jj!1")
(("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)
unchecked
((ne_fseq type-eq-decl nil fseqs "structures/")
(> 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)
(seq2set const-decl "finite_set[T]" fseq2set nil)
(finite_set type-eq-decl nil finite_sets nil)
(fseq type-eq-decl nil fseqs "structures/")
(barray type-eq-decl nil fseqs "structures/")
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(is_finite const-decl "bool" finite_sets nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil fseq2set nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(seq2set_lem formula-decl nil fseq2set nil)
(empty? const-decl "bool" sets nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(min const-decl
"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES a <= x)}"
finite_sets_minmax "finite_sets/")
(partial_order? const-decl "bool" orders nil)
(antisymmetric? const-decl "bool" relations nil)
(dichotomous? const-decl "bool" orders nil)
(member const-decl "bool" sets nil)
(min_seq_lem formula-decl nil min_fseq "structures/")
(below type-eq-decl nil naturalnumbers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(pred type-eq-decl nil defined_types nil)
(total_order? const-decl "bool" orders nil)
(<= formal-const-decl "(total_order?[T])" fseq2set nil)
(dom type-eq-decl nil min_fseq "structures/")
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(min const-decl "{t: T |
(FORALL (ii: dom(s)): t <= seq(s)(ii)) AND
(EXISTS (jj: dom(s)): seq(s)(jj) = t)}" min_fseq
"structures/")
(max const-decl
"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}"
finite_sets_minmax "finite_sets/")
(preorder? const-decl "bool" orders nil)
(transitive? const-decl "bool" relations nil)
(max_lem formula-decl nil finite_sets_minmax "finite_sets/")
(reflexive? const-decl "bool" relations nil)
(max_seq_lem formula-decl nil max_fseq "structures/")
(dom type-eq-decl nil max_fseq "structures/")
(max const-decl "{t: T |
(FORALL (ii: dom(s)): seq(s)(ii) <= t) AND
(EXISTS (jj: dom(s)): seq(s)(jj) = t)}" max_fseq
"structures/"))
861 760 t shostak)
(minmax_seq2set-1 nil 3283098598 3283255060
("" (skosimp*)
(("" (typepred "seq2set(ne_fs!1)")
(("" (typepred "ne_fs!1")
(("" (split)
(("1" (typepred "min(ne_fs!1)")
(("1" (expand "seq2set")
(("1" (assert)
(("1" (skosimp*)
(("1" (expand "finseq_appl")
(("1" (inst?)
(("1" (lemma "seq2set_lem")
(("1" (inst?)
(("1" (expand "seq2set")
(("1" (expand "finseq_appl")
(("1"
(inst?)
(("1"
(lemma "min_seq_lem")
(("1"
(skosimp*)
(("1"
(name
mm
"min[T, <=]({s: T | EXISTS (kk: below(length(ne_fs!1))): ne_fs!1`seq(kk) = s})")
(("1"
(replace -1)
(("1"
(typepred "mm")
(("1"
(skosimp*)
(("1"
(case
"mm <= min(ne_fs!1)")
(("1"
(assert)
(("1"
(case
"min(ne_fs!1) <= mm")
(("1"
(assert)
(("1"
(typepred "<=")
(("1"
(expand
"total_order?")
(("1"
(flatten)
(("1"
(expand
"dichotomous?")
(("1"
(expand
"partial_order?")
(("1"
(expand
"antisymmetric?")
(("1"
(flatten)
(("1"
(inst
-2
"mm"
"min(ne_fs!1)")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst? -5)
(("2"
(inst?)
(("2"
(postpone)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(postpone)
nil
nil))
nil))
nil))
nil))
nil)
("2" (postpone) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (postpone) nil nil))
nil))
nil))
nil))
nil)
unfinished nil 3562301 6490 t shostak))
(seq2set_TCC2 0
(seq2set_TCC2-1 nil 3282912778 3440772507
("" (skosimp*)
(("" (expand "nonempty?")
(("" (lemma "minmax_seq2set_TCC1")
(("" (inst?) (("" (assert) (("" (postpone) nil nil)) nil))
nil))
nil))
nil))
nil)
unchecked
((nonempty? const-decl "bool" sets nil)
(ne_fseq type-eq-decl nil fseqs "structures/")
(> const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(fseq type-eq-decl nil fseqs "structures/")
(barray type-eq-decl nil fseqs "structures/")
(T formal-type-decl nil fseq2set nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(minmax_seq2set_TCC1 subtype-tcc nil fseq2set nil))
30 10 t shostak))
(set2seq_TCC1 0
(set2seq_TCC1-2 nil 3440770694 3440772890
(""
(inst + "(LAMBDA (S: finite_set[T]):
choose({fs: fseq[T] |
length(fs) = card[T](S) AND
(FORALL (ii: below(length(fs))):
S(fs`seq(ii))) AND
(FORALL (x: T):
S(x)
IMPLIES
(EXISTS
(ii: below(length(fs))):
fs`seq(ii) = x))
AND
(FORALL (ii, jj: below(length(fs))):
ii /= jj
IMPLIES
fs`seq(ii) /= fs`seq(jj))}))")
(("" (skosimp*)
(("" (name "F" "ibij(S!1)")
(("1" (typepred "ibij(S!1)")
(("1" (replace -2 * lr)
(("1" (hide -2)
(("1" (expand "nonempty?")
(("1" (expand "empty?")
(("1" (expand "member")
(("1"
(inst -2 "(# length := card(S!1),
seq := (LAMBDA (i: nat): IF i < card(S!1) THEN F(i)
ELSE default
ENDIF)
#)")
(("1" (prop)
(("1" (ground) nil nil)
("2" (skosimp*)
(("2" (inst + "bij(S!1)(x!1)")
(("2" (lift-if)
(("2"
(ground)
(("2"
(expand "F")
(("2" (rewrite "ibij_bij") nil nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp*)
(("3" (lift-if)
(("3" (ground)
(("3"
(expand "bijective?")
(("3"
(flatten)
(("3"
(expand "injective?")
(("3"
(inst?)
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (lift-if) (("2" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "nonempty?")
(("2" (lemma "empty_card")
(("2" (inst?)
(("2" (assert)
(("2" (replace -1 * lr)
(("2" (hide -1)
(("2" (hide -1)
(("2" (expand "empty?")
(("2" (expand "member")
(("2"
(inst -
"(# length := 0, seq := (LAMBDA (i: nat): default) #)")
(("2" (prop)
(("1" (skosimp*) nil nil)
("2"
(skosimp*)
(("2"
(assert)
(("2"
(reveal -2)
(("2"
(expand "empty?")
(("2"
(expand "member")
(("2" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp*) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
unchecked
((empty_card formula-decl nil finite_sets nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(default const-decl "T" fseqs "structures/")
(injective? const-decl "bool" functions nil)
(ibij_bij formula-decl nil fseq2set nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(bij const-decl "{f: [(S) -> below(card(S))] | bijective?(f)}"
fseq2set nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(member const-decl "bool" sets nil)
(ibij const-decl "{f: [below(card(S)) -> (S)] | bijective?(f)}"
fseq2set nil)
(bijective? const-decl "bool" functions 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)
(choose const-decl "(p)" sets nil)
(nonempty? const-decl "bool" sets nil)
(/= const-decl "boolean" notequal nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
(Card const-decl "nat" finite_sets 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)
(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)
(number nonempty-type-decl nil numbers nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(fseq type-eq-decl nil fseqs "structures/")
(barray type-eq-decl nil fseqs "structures/")
(nat nonempty-type-eq-decl nil naturalnumbers 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)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil fseq2set nil))
365426 390 t nil)
(set2seq_TCC1-1 nil 3280842302 3440770670
(""
(inst + "(LAMBDA (S: finite_set[T]):
choose({fs: fseq[T] |
length(fs) = card[T](S) AND
(FORALL (ii: below(length(fs))):
S(fs`seq(ii)) AND
(FORALL (x: T):
S(x)
IMPLIES
(EXISTS
(ii: below(length(fs))):
fs`seq(ii) = x))
AND
(FORALL (ii, jj: below(length(fs))):
ii /= jj
IMPLIES
fs`seq(ii) /= fs`seq(jj)))}))")
(("" (skosimp*)
(("" (name "F" "bij(S!1)")
(("" (typepred "bij(S!1)")
(("" (replace -2 * lr)
(("" (hide -2)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (expand "member") (("" (postpone) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
unfinished ((nonempty? const-decl "bool" sets nil)) 116 80 t
shostak))
(set2seq_length 0
(set2seq_length-1 nil 3281098906 3440772898
("" (induct "S" 1 "finite_set_induction_rest[T]")
(("1" (expand "set2seq")
(("1" (expand "fseq1")
(("1" (expand "o ")
(("1" (ground)
(("1" (case "empty?[T](emptyset[T])")
(("1" (assert)
(("1" (rewrite "card_emptyset[T]")
(("1" (assert)
(("1" (expand "empty_seq") (("1" (propax) nil nil))
nil))
nil))
nil))
nil)
("2" (hide 2) (("2" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "set2seq" 1)
(("2" (expand "o ")
(("2" (expand "fseq1")
(("2" (assert)
(("2" (rewrite "card_rest") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
unchecked
((finite_rest application-judgement "finite_set[T]" fseq2set nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" fseq2set nil)
(finite_set_induction_rest formula-decl nil finite_sets_inductions
"finite_sets/")
(T formal-type-decl nil fseq2set nil)
(set2seq const-decl "{fs: fseq[T] |
length(fs) = card(S) AND
(FORALL (ii: below(length(fs))): S(fs`seq(ii))) AND
(FORALL (x: T):
S(x) IMPLIES
(EXISTS (ii: below(length(fs))): fs`seq(ii) = x))
AND
(FORALL (ii, jj: below(length(fs))):
ii /= jj IMPLIES fs`seq(ii) /= fs`seq(jj))}" fseq2set
nil)
(/= const-decl "boolean" notequal nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
(Card const-decl "nat" finite_sets 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)
(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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(fseq type-eq-decl nil fseqs "structures/")
(barray type-eq-decl nil fseqs "structures/")
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(number nonempty-type-decl nil numbers nil)
(pred type-eq-decl nil defined_types 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)
(boolean nonempty-type-decl nil booleans nil))
84 70 t shostak))
(set2seq_lem 0
(set2seq_lem-1 nil 3280846807 3440772898
("" (skosimp*)
(("" (assert)
(("" (skosimp*)
(("" (typepred "set2seq(S!1)")
(("" (inst?) (("" (flatten) nil nil)) nil)) nil))
nil))
nil))
nil)
unchecked nil 28 20 t shostak))
(set2seq_exists 0
(set2seq_exists-2 nil 3410632995 3440772939
("" (skosimp*)
(("" (assert)
(("" (flatten)
(("" (typepred "set2seq(S!1)")
(("" (inst -3 "x!1") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
unchecked
((set2seq const-decl "{fs: fseq[T] |
length(fs) = card(S) AND
(FORALL (ii: below(length(fs))): S(fs`seq(ii))) AND
(FORALL (x: T):
S(x) IMPLIES
(EXISTS (ii: below(length(fs))): fs`seq(ii) = x))
AND
(FORALL (ii, jj: below(length(fs))):
ii /= jj IMPLIES fs`seq(ii) /= fs`seq(jj))}" fseq2set
nil)
(/= const-decl "boolean" notequal nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
(Card const-decl "nat" finite_sets 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)
(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)
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.70 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.
|
