|
(middle_third_pigeonhole
(middle_third_pigeonhole 0
(middle_third_pigeonhole-1 nil 3395067970
("" (auto-rewrite-theory "extend_set_props[int, below(N)]")
(("" (skosimp*)
(("" (lemma "fta_overlap_pigeonhole")
(("" (inst - "A!1" "B!1" "C!1" "S1!1" "S2!1")
(("1" (expand "two_thirds_majority_subset?")
(("1" (expand "byzantine_intersection_majority?")
(("1" (ground)
(("1" (skosimp*)
(("1" (expand "extend")
(("1" (inst?)
(("1" (ground) nil nil) ("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil)
("3" (skosimp*)
(("3" (expand "extend") (("3" (assert) nil nil)) nil)) nil)
("4" (skosimp*)
(("4" (expand "extend") (("4" (assert) nil nil)) nil)) nil)
("5" (skosimp*)
(("5" (expand "extend") (("5" (assert) nil nil)) nil)) nil)
("6" (skosimp*)
(("6" (expand "extend") (("6" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((finite_extend application-judgement "finite_set[T]"
extend_set_props nil)
(A!1 skolem-const-decl "finite_set[below(N)]"
middle_third_pigeonhole 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) (extend const-decl "R" extend nil)
(FALSE const-decl "bool" booleans nil)
(below type-eq-decl nil naturalnumbers nil)
(N formal-const-decl "posnat" middle_third_pigeonhole nil)
(posnat nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(nonneg_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)
(IMPLIES const-decl "[bool, bool -> bool]" booleans 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)
(B!1 skolem-const-decl "finite_set[below(N)]"
middle_third_pigeonhole nil)
(C!1 skolem-const-decl "finite_set[below(N)]"
middle_third_pigeonhole nil)
(S1!1 skolem-const-decl "finite_set[below(N)]"
middle_third_pigeonhole nil)
(S2!1 skolem-const-decl "finite_set[below(N)]"
middle_third_pigeonhole nil)
(nat_set type-eq-decl nil pigeonhole_int nil)
(byzantine_intersection_majority? const-decl "bool" pigeonhole nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(x!1 skolem-const-decl "int" middle_third_pigeonhole nil)
(subset_extend formula-decl nil extend_set_props nil)
(intersection_extend formula-decl nil extend_set_props nil)
(card_extend formula-decl nil extend_set_props nil)
(difference_extend formula-decl nil extend_set_props nil)
(union_extend formula-decl nil extend_set_props nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(finite_union application-judgement "finite_set" finite_sets nil)
(finite_difference application-judgement "finite_set" finite_sets
nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(finite_intersection1 application-judgement "finite_set"
finite_sets nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(two_thirds_majority_subset? const-decl "bool" pigeonhole nil)
(fta_overlap_pigeonhole formula-decl nil pigeonhole_int nil))
shostak)))
¤ Dauer der Verarbeitung: 0.28 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.
|
