|
(fseq2set
(seq2set_TCC1 0
(seq2set_TCC1-1 nil 3282912778
("" (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)
((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 nil)
(fseq type-eq-decl nil fseqs nil)
(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)
(fs!1 skolem-const-decl "fseq[T]" fseq2set nil)
(is_finite_surj formula-decl nil finite_sets nil)
(T formal-nonempty-type-decl nil fseq2set nil))
shostak))
(seq2set_lem 0
(seq2set_lem-1 nil 3282915134
("" (skosimp*)
(("" (expand "finseq_appl")
(("" (assert)
(("" (expand "seq2set")
(("" (expand "finseq_appl") (("" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil)
((below type-eq-decl nil naturalnumbers nil)
(fseq type-eq-decl nil fseqs nil)
(barray type-eq-decl nil fseqs nil)
(T formal-nonempty-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))
shostak))
(card_seq2set 0
(card_seq2set-2 "" 3283086594
("" (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)
((seq2set const-decl "finite_set[T]" fseq2set nil)
(finite_set type-eq-decl nil finite_sets nil)
(fseq type-eq-decl nil fseqs nil)
(barray type-eq-decl nil fseqs nil)
(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-nonempty-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)
(fs!1 skolem-const-decl "fseq[T]" fseq2set 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))
shostak)
(card_seq2set-1 nil 3282918983
("" (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)
nil shostak))
(minmax_seq2set_TCC1 0
(minmax_seq2set_TCC1-1 nil 3282912778
("" (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)
((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 nil)
(> 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 nil)
(barray type-eq-decl nil fseqs nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(T formal-nonempty-type-decl nil fseq2set nil)
(member const-decl "bool" sets nil))
shostak))
(minmax_seq2set 0
(minmax_seq2set-2 "" 3283271310
("" (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)
((ne_fseq type-eq-decl nil fseqs 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)
(seq2set const-decl "finite_set[T]" fseq2set nil)
(finite_set type-eq-decl nil finite_sets nil)
(fseq type-eq-decl nil fseqs nil)
(barray type-eq-decl nil fseqs nil)
(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-nonempty-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 nil)
(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 nil)
(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 nil)
(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/")
(ne_fs!1 skolem-const-decl "ne_fseq[T]" fseq2set nil)
(reflexive? const-decl "bool" relations nil)
(max_seq_lem formula-decl nil max_fseq nil)
(dom type-eq-decl nil max_fseq nil)
(max const-decl "{t: T |
(FORALL (ii: dom(s)): seq(s)(ii) <= t) AND
(EXISTS (jj: dom(s)): seq(s)(jj) = t)}" max_fseq nil))
shostak)
(minmax_seq2set-1 nil 3283098598
("" (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)
nil shostak))
(seq2set_TCC2 0
(seq2set_TCC2-1 nil 3282912778
("" (skosimp*)
(("" (expand "nonempty?")
(("" (lemma "minmax_seq2set_TCC1")
(("" (inst?) (("" (assert) (("" (postpone) nil nil)) nil))
nil))
nil))
nil))
nil)
((nonempty? const-decl "bool" sets nil)
(ne_fseq type-eq-decl nil fseqs nil)
(> 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 nil)
(barray type-eq-decl nil fseqs nil)
(T formal-nonempty-type-decl nil fseq2set nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(minmax_seq2set_TCC1 subtype-tcc nil fseq2set nil))
shostak))
(set2seq_TCC1 0
(set2seq_TCC1-2 nil 3440770694
(""
(inst + "(LAMBDA (S: finite_set[T]):
choose({fs: fseq |
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)
((empty_card formula-decl nil finite_sets nil)
(S!1 skolem-const-decl "finite_set[T]" fseq2set nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(F skolem-const-decl
"{f: [below(card(S!1)) -> (S!1)] | bijective?(f)}" fseq2set nil)
(default const-decl "T" fseqs nil)
(injective? const-decl "bool" functions nil)
(ibij_bij formula-decl nil finite_sets 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)}"
finite_sets nil)
(x!1 skolem-const-decl "T" 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)}"
finite_sets 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 nil)
(barray type-eq-decl nil fseqs nil)
(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-nonempty-type-decl nil fseq2set nil))
nil)
(set2seq_TCC1-1 nil 3280842302
(""
(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)
nil shostak))
(set2seq_length 0
(set2seq_length-1 nil 3281098906
("" (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)
((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-nonempty-type-decl nil fseq2set nil)
(set2seq const-decl "{fs: fseq |
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 nil)
(barray type-eq-decl nil fseqs nil)
(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))
shostak))
(set2seq_lem 0
(set2seq_lem-1 nil 3280846807
("" (skosimp*)
(("" (assert)
(("" (skosimp*)
(("" (typepred "set2seq(S!1)")
(("" (inst?) (("" (flatten) nil nil)) nil)) nil))
nil))
nil))
nil)
nil shostak))
(set2seq_exists 0
(set2seq_exists-2 nil 3410632995
("" (skosimp*)
(("" (assert)
(("" (flatten)
(("" (typepred "set2seq(S!1)")
(("" (inst -3 "x!1") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((set2seq const-decl "{fs: fseq |
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 nil)
(barray type-eq-decl nil fseqs nil)
(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)
(T formal-nonempty-type-decl nil fseq2set nil)
(= const-decl "[T, T -> boolean]" equalities 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))
nil)
(set2seq_exists-1 nil 3281099741
("" (auto-rewrite!! "finseq_appl")
(("" (expand "finseq_appl")
(("" (induct "S" 1 "finite_set_induction_rest[T]")
(("1" (skosimp*)
(("1" (hide 1)
(("1" (expand "emptyset") (("1" (propax) nil nil)) nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "set2seq" 1)
(("2" (expand "o " 1)
(("2" (expand "#")
(("2" (assert)
(("2" (inst?)
(("2" (assert)
(("2" (lemma "choose_rest_or[T]")
(("2" (inst?)
(("2" (inst?)
(("2" (expand "member")
(("2"
(split -1)
(("1"
(assert)
(("1"
(skosimp*)
(("1"
(typepred "ii!1")
(("1"
(inst + "ii!1+1")
(("1" (assert) nil nil)
("2" (grind) nil nil))
nil))
nil))
nil))
nil)
("2"
(inst + "0")
(("1" (assert) nil nil)
("2"
(expand "set2seq")
(("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((finite_set_induction_rest formula-decl nil finite_sets_inductions
"finite_sets/"))
shostak))
(minmax_set2seq_TCC1 0
(minmax_set2seq_TCC1-1 nil 3281118238
("" (skosimp*) (("" (assert) nil nil)) nil)
((real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(set2seq_length formula-decl nil fseq2set nil))
shostak))
(minmax_set2seq_TCC2 0
(minmax_set2seq_TCC2-1 nil 3281118238
("" (skosimp*)
(("" (lemma "card_empty?[T]")
(("" (inst?) (("" (assert) (("" (ground) nil nil)) nil)) nil))
nil))
nil)
((T formal-nonempty-type-decl nil fseq2set nil)
(card_empty? formula-decl nil finite_sets nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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))
shostak))
(minmax_set2seq 0
(minmax_set2seq-1 nil 3281118135
("" (assert)
(("" (skosimp*)
(("" (prop)
(("1" (typepred "min(set2seq(S!1))")
(("1" (skosimp*)
(("1" (replace -2 * rl)
(("1" (typepred "min[T, <=](S!1)")
(("1" (lemma "set2seq_lem")
(("1" (inst?)
(("1" (assert)
(("1" (inst - "jj!1")
(("1" (inst - "set2seq(S!1)`seq(jj!1)")
(("1" (assert)
(("1" (assert)
(("1"
(lemma "set2seq_exists")
(("1"
(inst - "S!1" "min[T, <=](S!1)")
(("1"
(assert)
(("1"
(skosimp*)
(("1"
(inst - "ii!1")
(("1"
(assert)
(("1"
(typepred "<=")
(("1"
(expand "total_order?")
(("1"
(expand
"partial_order?")
(("1"
(expand "preorder?")
(("1"
(expand
"transitive?")
(("1"
(flatten)
(("1"
(expand
"reflexive?")
(("1"
(expand
"antisymmetric?")
(("1"
(inst
-3
"min[T, <=](S!1)"
"set2seq(S!1)`seq(jj!1)")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.135 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.
|
