| products/sources/formale Sprachen/PVS/fault_tolerance/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: pigeonhole.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(pigeonhole
(pigeonhole 0 (pigeonhole-1 nil 3266842135 ("" (skosimp*) (("" (case "card(intersection(A!1, B!1)) >= 1") (("1" (hide -2) (("1" (forward-chain "card_1_has_1") (("1" (hide -2) (("1" (skosimp*) (("1" (expand* "intersection" "member") (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (use "card_plus[T]") (("2" (assert) nil nil)) nil)) nil)) nil) ((intersection const-decl "set" sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (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-type-decl nil pigeonhole 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) (finite_intersection1 application-judgement "finite_set" finite_sets nil) (card_1_has_1 formula-decl nil finite_sets nil) (member const-decl "bool" sets nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (finite_union application-judgement "finite_set" finite_sets nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (card_plus formula-decl nil finite_sets nil)) nil)) (card_difference_alt 0 (card_difference_alt-1 nil 3363507964 ("" (skosimp*) (("" (rewrite "difference_intersection") (("" (lemma "card_disj_union[T]") (("" (inst?) (("" (invoke (inst - "%1") (! 1 r 1 1)) (("" (split -) (("1" (rewrite "distribute_intersection_union" :dir rl) (("1" (invoke (case-replace "%1 = %2") (! -1 l 1) (! -1 l 1 1)) (("1" (ground) nil nil) ("2" (hide-all-but 1) (("2" (apply-extensionality :hide? t) (("2" (iff) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((difference_intersection formula-decl nil sets_lemmas 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 pigeonhole nil) (finite_intersection2 application-judgement "finite_set" finite_sets nil) (complement const-decl "set" sets nil) (intersection const-decl "set" sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (union const-decl "set" sets nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_minus_int_is_int application-judgement "int" integers 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) (member const-decl "bool" sets nil) (distribute_intersection_union formula-decl nil sets_lemmas nil) (empty? const-decl "bool" sets nil) (disjoint? const-decl "bool" sets nil) (finite_intersection1 application-judgement "finite_set" finite_sets nil) (card_disj_union formula-decl nil finite_sets nil)) shostak)) (pigeonhole_difference 0 (pigeonhole_difference-1 nil 3363458043 ("" (skosimp*) (("" (lemma "pigeonhole") (("" (inst - "A!1" "intersection(S!1, B!1)") (("" (prop) (("1" (skosimp*) (("1" (expand "intersection") (("1" (expand "member") (("1" (flatten) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "subset?(union(A!1, intersection(S!1, B!1)), S!1)") (("1" (forward-chain "card_subset") (("1" (rewrite "card_difference_alt") (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "union_upper_bound") (("2" (rewrite "intersection_subset1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((pigeonhole formula-decl nil pigeonhole nil) (finite_difference application-judgement "finite_set" finite_sets nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (member const-decl "bool" sets nil) (union_upper_bound formula-decl nil sets_lemmas nil) (intersection_subset1 formula-decl nil sets_lemmas nil) (card_subset formula-decl nil finite_sets nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers 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) (card_difference_alt formula-decl nil pigeonhole nil) (union const-decl "set" sets nil) (subset? const-decl "bool" sets nil) (finite_union application-judgement "finite_set" finite_sets nil) (intersection const-decl "set" sets 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-type-decl nil pigeonhole nil) (finite_intersection1 application-judgement "finite_set" finite_sets nil)) shostak)) (simple_majority_subset 0 (simple_majority_subset-1 nil 3397651319 ("" (skosimp*) (("" (prop) (("1" (expand "majority_subset?") (("1" (expand "simple_majority?") (("1" (assert) (("1" (hide -1) (("1" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "simple_majority?") (("2" (expand "majority_subset?") (("2" (flatten) nil nil)) nil)) nil)) nil)) nil) ((simple_majority? const-decl "bool" pigeonhole nil) (subset? const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (member const-decl "bool" sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas 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_intersection1 application-judgement "finite_set" finite_sets nil) (majority_subset? const-decl "bool" pigeonhole nil)) shostak)) (majority_subset_nonempty 0 (majority_subset_nonempty-1 nil 3267459600 ("" (skosimp*) (("" (expand "majority_subset?") (("" (flatten) (("" (use "nonempty_card[T]") (("" (assert) (("" (expand* "nonempty?" "empty?" "subset?" "member") (("" (skosimp*) (("" (inst?) (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((majority_subset? const-decl "bool" pigeonhole nil) (nonempty_card formula-decl nil finite_sets nil) (T formal-type-decl nil 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) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (nonempty? 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) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil)) shostak)) (simple_majority_nonempty 0 (simple_majority_nonempty-1 nil 3397654037 ("" (skosimp*) (("" (rewrite "simple_majority_subset") (("" (forward-chain "majority_subset_nonempty") nil nil)) nil)) nil) ((simple_majority_subset formula-decl nil pigeonhole nil) (T formal-type-decl nil pigeonhole 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) (finite_intersection1 application-judgement "finite_set" finite_sets nil) (intersection const-decl "set" sets nil) (majority_subset_nonempty formula-decl nil pigeonhole nil)) shostak)) (majority_nonempty 0 (majority_nonempty-1 nil 3276456345 ("" (skosimp*) (("" (lemma "majority_subset_nonempty") (("" (inst?) (("" (assert) (("" (expand "majority_subset?") (("" (flatten) (("" (lemma "card_empty?[T]") (("" (inst-cp - "S!1") (("" (inst - "A!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((majority_subset_nonempty formula-decl nil pigeonhole 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) (card_empty? formula-decl nil finite_sets nil) (majority_subset? const-decl "bool" 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) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil pigeonhole nil)) shostak)) (majority_pigeonhole 0 (majority_pigeonhole-1 nil 3266842135 ("" (skosimp*) (("" (case "card(union(A!1,B!1)) <= card(S!1)") (("1" (use "pigeonhole") (("1" (assert) nil nil)) nil) ("2" (hide -1 -3 2) (("2" (rewrite "card_subset") (("2" (rewrite "union_upper_bound") nil nil)) nil)) nil)) nil)) nil) ((union const-decl "set" sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (= const-decl "[T, T -> boolean]" equalities 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) (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-type-decl nil pigeonhole 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) (finite_union application-judgement "finite_set" finite_sets nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (pigeonhole formula-decl nil pigeonhole nil) (card_subset formula-decl nil finite_sets nil) (union_upper_bound formula-decl nil sets_lemmas nil)) nil)) (simple_majority_pigeonhole 0 (simple_majority_pigeonhole-1 nil 3400434247 ("" (skosimp*) (("" (expand "simple_majority?") (("" (case "card(union(intersection(A!1,S!1),intersection(B!1,S!1))) <= card(S!1)") (("1" (lemma "pigeonhole") (("1" (inst - "intersection(A!1, S!1)" "intersection(B!1, S!1)") (("1" (assert) (("1" (skosimp*) (("1" (inst?) (("1" (expand "intersection") (("1" (expand "member") (("1" (flatten) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "card_subset") (("2" (hide -1 -2 2 3) (("2" (auto-rewrite-defs) (("2" (assert) (("2" (skosimp*) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((simple_majority? const-decl "bool" pigeonhole nil) (card_subset formula-decl nil finite_sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (subset? const-decl "bool" sets nil) (pigeonhole formula-decl nil pigeonhole nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers 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) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (member const-decl "bool" sets nil) (finite_intersection1 application-judgement "finite_set" finite_sets nil) (finite_union application-judgement "finite_set" 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) (bool nonempty-type-eq-decl nil booleans nil) (<= const-decl "bool" reals nil) (T formal-type-decl nil pigeonhole 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) (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 "[T, T -> boolean]" equalities nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (union const-decl "set" sets nil) (intersection const-decl "set" sets nil)) nil)) (median_pigeonhole 0 (median_pigeonhole-1 nil 3363648177 ("" (skosimp*) (("" (case "subset?(S1!1, S2!1)") (("1" (lemma "majority_pigeonhole") (("1" (inst - "B!1" "A!1" "S2!1") (("1" (assert) (("1" (expand "majority_subset?") (("1" (flatten) (("1" (assert) (("1" (forward-chain "card_subset") (("1" (assert) (("1" (prop) (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "union_subset2") (("2" (rewrite "intersection_subset2") (("2" (assert) nil nil)) nil)) nil) ("3" (hide -1 -3 -5 -6 -7 2) (("3" (lemma "subset_transitive[T]") (("3" (inst?) (("3" (inst - "S1!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (case "subset?(S2!1, S1!1)") (("1" (rewrite "union_commutative") (("1" (rewrite "intersection_commutative") (("1" (rewrite "union_subset2") (("1" (rewrite "intersection_subset2") (("1" (expand "majority_subset?") (("1" (flatten) (("1" (lemma "majority_pigeonhole") (("1" (inst - "A!1" "B!1" "S1!1") (("1" (assert) (("1" (prop) (("1" (hide -2 -3 -4 -6 2 3) (("1" (lemma "subset_transitive[T]") (("1" (inst?) (("1" (inst - "S2!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1 -2 3) (("2" (case "card(difference(union(S1!1, S2!1), intersection(S1!1, S2!1))) >= 2") (("1" (use "card_diff_subset[T]") (("1" (assert) (("1" (hide-all-but 1) (("1" (expand "subset?") (("1" (expand "intersection") (("1" (expand "union") (("1" (expand "member") (("1" (skosimp*) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (expand "subset?") (("2" (skosimp*) (("2" (case "subset?((: x!1, x!2 :), difference(union(S1!1, S2!1), intersection(S1!1, S (("1" (forward-chain "card_subset") (("1" (hide -2) (("1" (expand "list2set") (("1" (expand "list2set") (("1" (expand "list2set") (("1" (rewrite "card_add") (("1" (rewrite "card_add") (("1" (rewrite "card_emptyset") (("1" (assert) (("1" (expand "emptyset") (("1" (expand "add") (("1" (expand "member") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "list2set") (("2" (expand "list2set") (("2" (expand "list2set") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "list2set") (("2" (expand "list2set") (("2" (expand "list2set") (("2" (expand "add") (("2" (expand "subset?") (("2" (expand "intersection") (("2" (expand "union") (("2" (expand "difference") (("2" (expand "emptyset") (("2" (expand "member") (("2" (skosimp*) (("2" (assert) (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (subset? const-decl "bool" 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-type-decl nil pigeonhole nil) (majority_subset? const-decl "bool" pigeonhole nil) (subset_transitive formula-decl nil sets_lemmas nil) (union_subset2 formula-decl nil sets_lemmas nil) (intersection_subset2 formula-decl nil sets_lemmas nil) (card_subset formula-decl nil finite_sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers nil) (finite_union application-judgement "finite_set" finite_sets nil) (finite_intersection1 application-judgement "finite_set" finite_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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (majority_pigeonhole formula-decl nil pigeonhole nil) (card_emptyset formula-decl nil finite_sets nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (nonempty_add_finite application-judgement "non_empty_finite_set" finite_sets nil) (card_add formula-decl nil finite_sets nil) (nonempty? const-decl "bool" sets nil) (add const-decl "(nonempty?)" sets nil) (emptyset const-decl "set" sets nil) (null adt-constructor-decl "(null?)" list_adt nil) (null? adt-recognizer-decl "[list -> boolean]" list_adt nil) (cons adt-constructor-decl "[[T, list] -> (cons?)]" list_adt nil) (cons? adt-recognizer-decl "[list -> boolean]" list_adt nil) (list2set def-decl "set[T]" list2set nil) (list type-decl nil list_adt nil) (card_diff_subset formula-decl nil finite_sets nil) (member const-decl "bool" sets nil) (finite_difference application-judgement "finite_set" finite_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) (>= 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 "[T, T -> boolean]" equalities nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (difference const-decl "set" sets nil) (union const-decl "set" sets nil) (intersection const-decl "set" sets nil) (union_commutative formula-decl nil sets_lemmas nil) (intersection_commutative formula-decl nil sets_lemmas nil)) shostak)) (intersection_nonempty 0 (intersection_nonempty-1 nil 3395056471 ("" (skosimp*) (("" (expand "intersection_majority?") (("" (use "nonempty_card[T]") (("" (assert) (("" (expand "nonempty?") (("" (expand "empty?") (("" (expand "member") (("" (expand "intersection") (("" (expand "member") (("" (skosimp*) (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((intersection_majority? const-decl "bool" pigeonhole 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) (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil) (finite_union application-judgement "finite_set" finite_sets nil) (finite_intersection1 application-judgement "finite_set" 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) (intersection const-decl "set" sets nil) (T formal-type-decl nil pigeonhole nil) (nonempty_card formula-decl nil finite_sets nil)) shostak)) (two_thirds_overlap_pigeonhole 0 (two_thirds_overlap_pigeonhole-1 nil 3361957346 ("" (expand "intersection_majority?") (("" (skosimp*) (("" (rewrite "pigeonhole") (("" (hide 2) (("" (expand "two_thirds_majority_subset?") (("" (flatten) (("" (invoke (case "%1 <= %2") (! 1 r) (! -5 r)) (("1" (invoke (then (case "%1 > %2") (assert)) (! 1 l) (! -1 r)) (("1" (hide -1 -3 -5 2) (("1" (rewrite "card_union") (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (rewrite "card_subset") (("2" (hide-all-but (-2 -4 1)) (("2" (expand "subset?") (("2" (expand "union") (("2" (expand "member") (("2" (skosimp*) (("2" (inst?) (("2" (inst?) (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((card_subset formula-decl nil finite_sets nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (+ const-decl "[numfield, numfield -> numfield]" number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (> const-decl "bool" reals 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) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (card_union formula-decl nil finite_sets nil) (int_minus_int_is_int application-judgement "int" integers nil) (union const-decl "set" sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (= const-decl "[T, T -> boolean]" equalities 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) (<= 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) (two_thirds_majority_subset? const-decl "bool" pigeonhole nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (finite_union application-judgement "finite_set" finite_sets 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_intersection1 application-judgement "finite_set" finite_sets 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-type-decl nil pigeonhole nil) (pigeonhole formula-decl nil pigeonhole nil) (intersection_majority? const-decl "bool" pigeonhole nil)) shostak)) (quorum?_TCC1 0 (quorum?_TCC1-1 nil 3408976160 ("" (skosimp*) (("" (use "nonempty_card[T]") (("" (expand "nonempty?") (("" (assert) nil nil)) nil)) nil)) nil) ((nonempty_card formula-decl nil finite_sets nil) (T formal-type-decl nil 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) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonempty? const-decl "bool" sets nil)) nil)) (M_TCC1 0 (M_TCC1-1 nil 3398087512 ("" (skosimp*) (("" (use "nonempty_card[T]") (("" (assert) (("" (typepred "e!1") (("" (expand "nonempty?") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((nonempty_card formula-decl nil finite_sets nil) (T formal-type-decl nil pigeonhole 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) (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) (nonempty? const-decl "bool" sets nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil)) nil)) (M_TCC2 0 (M_TCC2-1 nil 3408976160 ("" (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) (T formal-type-decl nil pigeonhole 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) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props 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) (member const-decl "bool" sets nil) (injective? const-decl "bool" functions nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (int_minus_int_is_int application-judgement "int" integers 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)) nil)) (nada_reduce 0 (nada_reduce-1 nil 3398087779 ("" (expand "M") (("" (expand "nada") (("" (propax) nil nil)) nil)) nil) ((nada const-decl "tau_type" tau_declaration nil) (M const-decl "posnat" pigeonhole 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)) nil)) (mid_reduce 0 (mid_reduce-1 nil 3398087793 ("" (expand "M") (("" (expand "mid") (("" (skosimp*) (("" (assert) nil nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (mid const-decl "tau_type" tau_declaration nil) (rat_div_nzrat_is_rat application-judgement "rat" rationals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (M const-decl "posnat" pigeonhole 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)) nil)) (byz_reduce 0 (byz_reduce-1 nil 3398087809 ("" (skosimp*) (("" (expand "M") (("" (expand "byz") (("" (assert) nil nil)) nil)) nil)) nil) ((M const-decl "posnat" pigeonhole nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals 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) (int_minus_int_is_int application-judgement "int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (byz const-decl "tau_type" tau_declaration nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)) nil))) ¤ Dauer der Verarbeitung: 0.47 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.Bot Zugriff |
