|
(set2seq
(gen_seq_lem_TCC1 0
(gen_seq_lem_TCC1-1 nil 3280594050 ("" (subtype-tcc) nil nil)
((|#| const-decl "finite_sequence[T]" set2seq nil)) shostak))
(gen_seq_lem 0
(gen_seq_lem-1 nil 3280833619
("" (skosimp*)
(("" (assert)
(("" (expand "finseq_appl")
(("" (assert) (("" (expand "#") (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil)
((|#| const-decl "finite_sequence[T]" set2seq nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil))
shostak))
(set2seq_TCC1 0
(set2seq_TCC1-1 nil 3280842302
("" (skosimp*)
(("" (expand "nonempty?") (("" (propax) nil nil)) nil)) nil)
((nonempty? const-decl "bool" sets nil)) shostak))
(set2seq_TCC2 0
(set2seq_TCC2-1 nil 3280842320
("" (skosimp*)
(("" (rewrite "card_rest[T]") (("" (assert) nil nil)) nil)) nil)
((card_rest formula-decl nil finite_sets 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)
(T formal-type-decl nil set2seq nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
shostak))
(set2seq_length 0
(set2seq_length-1 nil 3281098906
("" (induct "S" 1 "finite_set_induction_rest[T]")
(("1" (expand "set2seq")
(("1" (expand "#")
(("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 "#")
(("2" (assert)
(("2" (rewrite "card_rest") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(finite_rest application-judgement "finite_set[T]" set2seq nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(card_rest formula-decl nil finite_sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" set2seq nil)
(O const-decl "finseq" finite_sequences nil)
(empty? const-decl "bool" sets nil)
(emptyset const-decl "set" sets nil)
(card_emptyset formula-decl nil finite_sets nil)
(empty_seq const-decl "finseq" finite_sequences nil)
(member const-decl "bool" sets nil)
(|#| const-decl "finite_sequence[T]" set2seq nil)
(finite_set_induction_rest formula-decl nil finite_sets_inductions
"finite_sets/")
(T formal-type-decl nil set2seq 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)
(set2seq def-decl "finite_sequence[T]" set2seq 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)
(= 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
("" (auto-rewrite!! "finseq_appl")
(("" (induct "S" 1 "finite_set_induction_rest[T]")
(("1" (assert) nil nil)
("2" (skosimp*)
(("2" (expand "set2seq")
(("2" (case "empty?[T](emptyset[T])")
(("1" (assert)
(("1" (typepred "ii!1")
(("1" (expand "set2seq")
(("1" (expand "empty_seq") (("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (assert) (("2" (grind) nil nil)) nil))
nil))
nil))
nil)
("3" (skosimp*)
(("3" (expand "finseq_appl")
(("3" (expand "set2seq" 1)
(("3" (expand "o ")
(("3" (assert)
(("3" (expand "#")
(("3" (ground)
(("3" (inst?)
(("1" (assert)
(("1" (lemma "rest_member[T]")
(("1" (expand "member")
(("1" (inst?)
(("1" (assert) nil nil)
("2"
(assert)
(("2"
(hide 3)
(("2"
(typepred "ii!1")
(("2"
(assert)
(("2"
(expand "set2seq")
(("2"
(expand "o ")
(("2"
(assert)
(("2"
(expand "#")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 3)
(("2" (typepred "ii!1")
(("2" (expand "set2seq")
(("2" (expand "#")
(("2"
(expand "o")
(("2"
(assert)
(("2"
(lift-if)
(("2"
(ground)
(("1"
(expand "set2seq")
(("1" (assert) nil nil))
nil)
("2"
(expand "set2seq")
(("2"
(assert)
(("2"
(expand "o")
(("2"
(expand "#")
(("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)
((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)
(pred type-eq-decl nil defined_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(finite_sequence type-eq-decl nil 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)
(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)
(finseq type-eq-decl nil finite_sequences nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(set2seq def-decl "finite_sequence[T]" set2seq nil)
(T formal-type-decl nil set2seq nil)
(finite_set_induction_rest formula-decl nil finite_sets_inductions
"finite_sets/")
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" set2seq nil)
(finite_rest application-judgement "finite_set[T]" set2seq nil)
(member const-decl "bool" sets nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(empty_seq const-decl "finseq" finite_sequences nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(emptyset const-decl "set" sets nil)
(empty? const-decl "bool" sets nil)
(O const-decl "finseq" finite_sequences nil)
(|#| const-decl "finite_sequence[T]" set2seq nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(rest const-decl "set" sets nil)
(rest_member formula-decl nil sets_lemmas nil)
(int_minus_int_is_int application-judgement "int" integers nil))
shostak))
(set2seq_exists 0
(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)
((finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(O const-decl "finseq" finite_sequences nil)
(finite_rest application-judgement "finite_set[T]" set2seq 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)
(member const-decl "bool" sets nil)
(rest const-decl "set" sets nil)
(/= const-decl "boolean" notequal nil)
(remove const-decl "set" sets nil)
(finite_remove application-judgement "finite_set[T]" set2seq nil)
(posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(ii!1 skolem-const-decl "below(length(set2seq(rest(SS!1))))"
set2seq nil)
(SS!1 skolem-const-decl "non_empty_finite_set[T]" set2seq nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(choose_rest_or formula-decl nil sets_lemmas nil)
(|#| const-decl "finite_sequence[T]" set2seq nil)
(emptyset const-decl "set" sets nil)
(finite_set_induction_rest formula-decl nil finite_sets_inductions
"finite_sets/")
(T formal-type-decl nil set2seq nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(below type-eq-decl nil naturalnumbers nil)
(set2seq def-decl "finite_sequence[T]" set2seq nil)
(finite_sequence type-eq-decl nil finite_sequences 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)
(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)
(number nonempty-type-decl nil numbers nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans 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_neq 0
(set2seq_neq-1 nil 3281100425
("" (induct "S" 1 "finite_set_induction_rest[T]")
(("1" (assert) nil nil)
("2" (skosimp*)
(("2" (expand "finseq_appl")
(("2" (auto-rewrite!! "finseq_appl")
(("2" (typepred "ii!1")
(("2" (typepred "jj!1")
(("2" (assert)
(("2" (rewrite "card_emptyset")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp*)
(("3" (expand "finseq_appl")
(("3" (typepred "ii!1")
(("3" (typepred "jj!1")
(("3" (assert)
(("3" (expand "set2seq" -4)
(("3" (expand "#")
(("3" (expand "o")
(("3" (case "ii!1 < 1")
(("1" (assert)
(("1" (lemma "set2seq_lem")
(("1" (inst?)
(("1" (assert)
(("1"
(inst - "jj!1-1")
(("1"
(expand "finseq_appl")
(("1"
(assert)
(("1"
(lemma "choose_not_member[T]")
(("1"
(expand "member")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (case "jj!1 < 1")
(("1" (assert)
(("1" (lemma "set2seq_lem")
(("1"
(inst?)
(("1"
(assert)
(("1"
(inst - "ii!1-1")
(("1"
(expand "finseq_appl")
(("1"
(lemma "choose_not_member[T]")
(("1"
(expand "member")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (inst -3 "ii!1-1" "jj!1-1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((empty? const-decl "bool" sets nil)
(non_empty_finite_set type-eq-decl nil finite_sets nil)
(|#| const-decl "finite_sequence[T]" set2seq nil)
(set2seq_lem formula-decl nil set2seq nil)
(choose_not_member formula-decl nil sets_lemmas nil)
(member const-decl "bool" sets nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(rest const-decl "set" sets nil)
(finite_rest application-judgement "finite_set[T]" set2seq nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(O const-decl "finseq" finite_sequences nil)
(card_emptyset formula-decl nil finite_sets nil)
(set2seq_length formula-decl nil set2seq nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset name-judgement "finite_set[T]" set2seq nil)
(emptyset const-decl "set" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(finite_set_induction_rest formula-decl nil finite_sets_inductions
"finite_sets/")
(T formal-type-decl nil set2seq nil)
(set2seq def-decl "finite_sequence[T]" set2seq nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(finseq type-eq-decl nil finite_sequences 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) (>= 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)
(number nonempty-type-decl nil numbers 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)
(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)))
(minmax_set2seq
(minmax_set2seq_TCC1 0
(minmax_set2seq_TCC1-1 nil 3559516105 ("" (subtype-tcc) nil nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" 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)
(T formal-nonempty-type-decl nil minmax_set2seq nil)
(set2seq_length formula-decl nil set2seq nil))
nil))
(minmax_set2seq_TCC2 0
(minmax_set2seq_TCC2-2 nil 3559516392
("" (skosimp*)
(("" (lemma "card_empty?[T]")
(("" (inst?) (("" (assert) (("" (ground) nil nil)) nil)) nil))
nil))
nil)
((T formal-nonempty-type-decl nil minmax_set2seq 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))
nil)
(minmax_set2seq_TCC2-1 nil 3559516105 ("" (subtype-tcc) nil nil) nil
nil))
(minmax_set2seq 0
(minmax_set2seq-1 nil 3559516260
("" (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" (expand "finseq_appl")
(("1" (inst?)
(("1" (assert)
(("1" (inst - "set2seq(S!1)`seq(jj!1)")
(("1" (assert)
(("1" (lemma "set2seq_exists")
(("1" (expand "finseq_appl")
(("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))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "max(set2seq(S!1))")
(("2" (skosimp*)
(("2" (typepred " max[T, <=](S!1)")
(("2" (lemma "set2seq_lem")
(("2" (inst?)
(("2" (assert)
(("2" (inst?)
(("2" (expand "finseq_appl")
(("2" (inst -3 "set2seq(S!1)`seq(jj!1)")
(("2" (assert)
(("2" (lemma "set2seq_exists")
(("2" (inst - "S!1" "max[T, <=](S!1)")
(("2"
(assert)
(("2"
(skosimp*)
(("2"
(expand "finseq_appl")
(("2"
(inst -5 "ii!1")
(("2"
(assert)
(("2"
(typepred "<=")
(("2"
(expand "total_order?")
(("2"
(expand "partial_order?")
(("2"
(expand
"antisymmetric?")
(("2"
(expand "preorder?")
(("2"
(flatten)
(("2"
(inst
-3
"max[T, <=](S!1)"
"set2seq(S!1)`seq(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))
nil))
nil))
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/")
(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)
(partial_order? const-decl "bool" orders nil)
(transitive? const-decl "bool" relations nil)
(reflexive? const-decl "bool" relations nil)
(antisymmetric? const-decl "bool" relations nil)
(preorder? const-decl "bool" orders nil)
(set2seq_exists formula-decl nil set2seq nil)
(below type-eq-decl nil naturalnumbers nil)
(set2seq_lem formula-decl nil set2seq nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans 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)
(T formal-nonempty-type-decl nil minmax_set2seq 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)
(below type-eq-decl nil nat_types nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(set2seq def-decl "finite_sequence[T]" set2seq nil)
(pred type-eq-decl nil defined_types nil)
(total_order? const-decl "bool" orders nil)
(<= formal-const-decl "(total_order?[T])" minmax_set2seq nil)
(dom type-eq-decl nil min_seq nil) (> const-decl "bool" reals nil)
(ne_seqs type-eq-decl nil seqs 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 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)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.38Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
