|
(finite_seqs
(choose_TCC1 0
(choose_TCC1-1 nil 3403442054 ("" (subtype-tcc) nil nil) nil nil))
(choose_in? 0
(choose_in?-2 nil 3403442450
("" (skosimp*)
(("" (expand "choose")
(("" (lift-if)
(("" (assert)
(("" (ground)
(("1" (expand "in?") (("1" (inst?) nil nil)) nil)
("2" (expand "in?") (("2" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((choose const-decl "T" finite_seqs nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(in? const-decl "bool" seqs "structures/")
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil nat_types nil)
(T formal-nonempty-type-decl nil finite_seqs nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(> const-decl "bool" reals nil)
(ne_seqs type-eq-decl nil seqs "structures/")
(below type-eq-decl nil naturalnumbers nil))
nil)
(choose_in?-1 nil 3403362398
("" (skosimp*)
(("" (expand "in?")
(("" (expand "choose")
(("" (lift-if)
(("" (prop)
(("1" (inst?) nil nil)
("2" (use "max_seq_in?")
(("2" (expand "in?") (("2" (propax) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
nil shostak))
(choose_consensus 0
(choose_consensus-1 nil 3403361092
("" (skosimp*) (("" (use "choose_in?") (("" (assert) nil nil)) nil))
nil)
((ne_seqs type-eq-decl nil seqs "structures/")
(> const-decl "bool" reals nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(T formal-nonempty-type-decl nil finite_seqs nil)
(below type-eq-decl nil nat_types 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)
(choose_in? formula-decl nil finite_seqs nil))
nil))
(maj_exists_same 0
(maj_exists_same-1 nil 3495198007
("" (skosimp* t)
(("" (typepred "mf!1(fs!1)")
(("" (typepred "maj(fs!1)")
(("" (prop)
(("" (use "is_majority_unique") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
((majority_function type-eq-decl nil finite_seqs nil)
(is_majority const-decl "bool" majority_seq "structures/")
(maj_exists const-decl "bool" majority_seq "structures/")
(finite_sequence type-eq-decl nil finite_sequences nil)
(T formal-nonempty-type-decl nil finite_seqs nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(is_majority_unique formula-decl nil majority_seq "structures/")
(maj const-decl "{mv | maj_exists(fs) => is_majority(mv, fs)}"
majority_seq "structures/"))
shostak))
(mf_lem 0
(mf_lem-1 nil 3495202609
("" (skosimp*)
(("" (rewrite "maj_exists_same")
(("1" (use "maj_lem") (("1" (prop) nil nil)) nil)
("2" (expand "maj_exists") (("2" (inst?) nil nil)) nil))
nil))
nil)
((maj_exists_same formula-decl nil finite_seqs nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(T formal-nonempty-type-decl nil finite_seqs nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(maj_exists const-decl "bool" majority_seq "structures/")
(is_majority const-decl "bool" majority_seq "structures/")
(majority_function type-eq-decl nil finite_seqs nil)
(maj_lem formula-decl nil majority_seq "structures/"))
shostak))
(majority_choose_consensus 0
(majority_choose_consensus-1 nil 3495209869
("" (skosimp*)
(("" (expand "majority_choose")
(("" (lift-if)
(("" (assert)
(("" (prop)
(("1" (typepred "maj(x1!1)")
(("1" (prop)
(("1" (use "maj_in_seq")
(("1" (assert)
(("1" (expand "in_seq")
(("1" (expand "in?")
(("1" (skosimp*)
(("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (assert)
(("2" (expand "choose")
(("2" (assert)
(("2" (expand "in?") (("2" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((majority_choose const-decl "T" finite_seqs nil)
(in? const-decl "bool" seqs "structures/")
(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)
(in_seq const-decl "bool" majority_seq "structures/")
(maj_in_seq formula-decl nil majority_seq "structures/")
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(T formal-nonempty-type-decl nil finite_seqs nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(maj_exists const-decl "bool" majority_seq "structures/")
(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)
(ne_seqs type-eq-decl nil seqs "structures/")
(is_majority const-decl "bool" majority_seq "structures/")
(maj const-decl "{mv | maj_exists(fs) => is_majority(mv, fs)}"
majority_seq "structures/")
(choose const-decl "T" finite_seqs nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(choose_consensus application-judgement "in_consensus_function"
finite_seqs nil))
nil))
(majority_choose2_TCC1 0
(majority_choose2_TCC1-1 nil 3495213184 ("" (subtype-tcc) nil nil)
((member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil))
nil))
(majority_choose2_TCC2 0
(majority_choose2_TCC2-1 nil 3495213184 ("" (subtype-tcc) nil nil)
((real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(majority2_choose_majority 0
(majority2_choose_majority-1 nil 3495213184
("" (skosimp*)
(("" (expand "majority_choose2")
(("" (expand "majority_choose")
(("" (lift-if)
(("" (assert)
(("" (prop)
(("1" (expand "maj_exists")
(("1" (expand "is_majority")
(("1" (skosimp*)
(("1" (use "empty_card[below(length(x1!1))]")
(("1" (assert)
(("1" (expand "empty?")
(("1" (expand "member")
(("1" (skosimp*) nil nil)) nil))
nil))
nil)
("2" (rewrite "finite_below") nil nil))
nil))
nil))
nil))
nil)
("2" (typepred "maj(x1!1)") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((majority_choose2 const-decl "T" finite_seqs nil)
(is_majority const-decl "bool" majority_seq "structures/")
(empty_card formula-decl nil finite_sets nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil nat_types nil)
(T formal-nonempty-type-decl nil finite_seqs nil)
(finite_sequence type-eq-decl nil finite_sequences nil)
(below type-eq-decl nil naturalnumbers nil)
(finite_set type-eq-decl nil finite_sets nil)
(x1!1 skolem-const-decl "finite_sequence[T]" finite_seqs nil)
(set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(mv!1 skolem-const-decl "T" finite_seqs nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(finite_below formula-decl nil finite_sets_below "finite_sets/")
(maj_exists const-decl "bool" majority_seq "structures/")
(NOT const-decl "[bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(maj const-decl "{mv | maj_exists(fs) => is_majority(mv, fs)}"
majority_seq "structures/")
(majority_choose const-decl "T" finite_seqs nil))
nil))
(uniform_TCC1 0
(uniform_TCC1-1 nil 3494953503 ("" (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)
(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)
(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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil))
nil))
(uniform_TCC2 0
(uniform_TCC2-1 nil 3494953503
("" (skosimp*)
(("" (rewrite "finite_below")
(("" (skosimp*) (("" (assert) nil nil)) nil)) nil))
nil)
((IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(finite_below formula-decl nil finite_sets_below "finite_sets/")
(< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(set type-eq-decl nil sets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(below type-eq-decl nil nat_types nil)
(T formal-nonempty-type-decl nil finite_seqs nil)
(finite_sequence 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)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil))
nil))
(majority_same 0
(majority_same-1 nil 3494953576
("" (skosimp*)
(("" (prop)
(("1" (expand "is_majority")
(("1" (expand "is_majority?")
(("1" (expand "uniform") (("1" (propax) nil nil)) nil)) nil))
nil)
("2" (expand "is_majority?")
(("2" (expand "is_majority")
(("2" (assert)
(("2" (expand "uniform") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((is_majority? const-decl "bool" finite_seqs nil)
(uniform const-decl "finite_set[below(k)]" finite_seqs nil)
(is_majority const-decl "bool" majority_seq "structures/")
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil))
shostak)))
¤ Dauer der Verarbeitung: 0.20 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.
|
