|
(seq2set
(seq2set_TCC1 0
(seq2set_TCC1-1 nil 3282912778
("" (skosimp*)
(("" (assert)
(("" (lemma "is_finite_surj[T]")
(("" (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)
(below type-eq-decl nil nat_types nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(below type-eq-decl nil naturalnumbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(finseq type-eq-decl nil finite_sequences nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(surjective? const-decl "bool" functions nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(fs!1 skolem-const-decl "finite_sequence[T]" seq2set nil)
(is_finite_surj formula-decl nil finite_sets nil)
(T formal-type-decl nil seq2set 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)
((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(seq2set const-decl "finite_set[T]" seq2set nil)
(below type-eq-decl nil naturalnumbers nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(T formal-type-decl nil seq2set nil)
(below type-eq-decl nil nat_types 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))
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[T]")
(("" (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]" seq2set nil)
(finite_set type-eq-decl nil finite_sets nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(below type-eq-decl nil nat_types 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-type-decl nil seq2set 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 seq2set nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(injective? const-decl "bool" functions nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets 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 "finite_sequence[T]" seq2set 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 "[T, T -> boolean]" equalities nil)
(Card_injection formula-decl nil finite_sets nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
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))
(seq2set_TCC2 0
(seq2set_TCC2-2 nil 3559517457
("" (skosimp*)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (expand "member")
(("" (expand "seq2set")
(("" (inst - "ss!1(0)") (("" (inst + "0") nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((nonempty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(T formal-type-decl nil seq2set nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(finseq type-eq-decl nil finite_sequences 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) (< const-decl "bool" reals nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(> const-decl "bool" reals nil) (ne_seqs type-eq-decl nil seqs nil)
(below type-eq-decl nil naturalnumbers nil)
(seq2set const-decl "finite_set[T]" seq2set nil)
(empty? const-decl "bool" sets nil))
nil)
(seq2set_TCC2-1 nil 3282912778
("" (skosimp*)
(("" (expand "nonempty?")
(("" (lemma "minmax_seq2set_TCC1")
(("" (inst?) (("" (assert) (("" (postpone) nil nil)) nil))
nil))
nil))
nil))
nil)
((ne_seqs type-eq-decl nil seqs nil)) shostak)))
(minmax_seq2set
(minmax_seq2set_TCC1 0
(minmax_seq2set_TCC1-2 nil 3559516730
("" (skosimp*)
(("" (expand "empty?")
(("" (expand "member")
(("" (expand "seq2set")
(("" (inst - "ne_fs!1(0)") (("" (inst + "0") nil nil)) nil))
nil))
nil))
nil))
nil)
((empty? const-decl "bool" sets nil)
(seq2set const-decl "finite_set[T]" seq2set nil)
(below type-eq-decl nil naturalnumbers nil)
(ne_seqs type-eq-decl nil seqs nil) (> const-decl "bool" reals nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(< const-decl "bool" reals 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)
(finseq type-eq-decl nil finite_sequences nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(T formal-nonempty-type-decl nil minmax_seq2set nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(member const-decl "bool" sets nil))
nil)
(minmax_seq2set_TCC1-1 nil 3559516643 ("" (subtype-tcc) nil nil) nil
nil))
(minmax_seq2set 0
(minmax_seq2set-1 nil 3559516692
("" (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)
((nonempty? const-decl "bool" sets nil)
(ne_seqs type-eq-decl nil seqs 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]" seq2set nil)
(finite_set type-eq-decl nil finite_sets nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(below type-eq-decl nil nat_types 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 minmax_seq2set nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(nil application-judgement "(nonempty?[T])" minmax_seq2set nil)
(min_seq_lem formula-decl nil min_seq nil)
(member const-decl "bool" sets nil)
(dichotomous? const-decl "bool" orders nil)
(antisymmetric? const-decl "bool" relations nil)
(partial_order? const-decl "bool" orders nil)
(min const-decl
"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES a <= x)}"
finite_sets_minmax "finite_sets/")
(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)
(below type-eq-decl nil naturalnumbers nil)
(seq2set_lem formula-decl nil seq2set nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
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])" minmax_seq2set nil)
(dom type-eq-decl nil min_seq 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_seq nil)
(max_seq_lem formula-decl nil max_seq nil)
(reflexive? const-decl "bool" relations nil)
(ne_fs!1 skolem-const-decl "ne_seqs[T]" minmax_seq2set nil)
(max_lem formula-decl nil finite_sets_minmax "finite_sets/")
(transitive? const-decl "bool" relations nil)
(preorder? const-decl "bool" orders nil)
(max const-decl
"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}"
finite_sets_minmax "finite_sets/")
(dom type-eq-decl nil max_seq nil)
(max const-decl "{t: T |
(FORALL (ii: dom(s)): seq(s)(ii) <= t) AND
(EXISTS (jj: dom(s)): seq(s)(jj) = t)}" max_seq nil))
nil)))
¤ Dauer der Verarbeitung: 0.50 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.
|
