|
(pigeonhole_int
(disjoint1 0
(disjoint1-1 nil 3362385158
("" (expand "disjoint?")
(("" (expand "empty?")
(("" (expand "intersection")
(("" (expand "member")
(("" (skosimp* t)
(("" (inst?) (("" (inst?) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((empty? const-decl "bool" sets nil)
(member const-decl "bool" sets 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)
(set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(>= const-decl "bool" reals nil)
(nat_set type-eq-decl nil pigeonhole_int nil)
(< const-decl "bool" reals nil)
(negint_set type-eq-decl nil pigeonhole_int nil)
(intersection const-decl "set" sets nil)
(disjoint? const-decl "bool" sets nil)
(finite_intersection1 application-judgement "finite_set"
finite_sets nil))
shostak))
(disjoint2 0
(disjoint2-1 nil 3362385222
("" (expand "disjoint?")
(("" (expand "empty?")
(("" (expand "intersection")
(("" (expand "member")
(("" (skosimp* t)
(("" (inst?) (("" (inst?) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((empty? const-decl "bool" sets nil)
(member const-decl "bool" sets 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)
(set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(>= const-decl "bool" reals nil)
(nat_set type-eq-decl nil pigeonhole_int nil)
(< const-decl "bool" reals nil)
(negint_set type-eq-decl nil pigeonhole_int nil)
(intersection const-decl "set" sets nil)
(disjoint? const-decl "bool" sets nil)
(finite_intersection1 application-judgement "finite_set"
finite_sets nil))
nil))
(complement_complement 0
(complement_complement-1 nil 3362381515
("" (expand "complement") (("" (propax) nil nil)) nil)
((complement const-decl "int" pigeonhole_int nil)) shostak))
(mirror_TCC1 0
(mirror_TCC1-1 nil 3362381514 ("" (subtype-tcc) nil nil)
((image const-decl "set[R]" function_image nil)
(finite_image application-judgement "finite_set[R]"
function_image_aux nil))
nil))
(mirror_mirror 0
(mirror_mirror-1 nil 3362381576
("" (expand "mirror")
(("" (expand "image")
(("" (expand "image")
(("" (expand "complement")
(("" (skosimp*)
(("" (decompose-equality)
(("" (iff)
(("" (prop)
(("1" (skosimp* t)
(("1" (expand "complement")
(("1" (assert) nil nil)) nil))
nil)
("2" (inst + "complement(x!1)")
(("1" (expand "complement")
(("1" (propax) nil nil)) nil)
("2" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((image const-decl "set[R]" function_image nil)
(complement const-decl "int" pigeonhole_int nil)
(int_minus_int_is_int application-judgement "int" integers 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)
(= const-decl "[T, T -> boolean]" equalities nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields 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)
(NOT const-decl "[bool -> bool]" booleans nil)
(x!1 skolem-const-decl "int" pigeonhole_int nil)
(X!1 skolem-const-decl "finite_set[int]" pigeonhole_int nil)
(image const-decl "set[R]" function_image nil)
(mirror const-decl "finite_set[int]" pigeonhole_int nil))
shostak))
(card_mirror 0
(card_mirror-1 nil 3362383344
("" (skosimp*)
(("" (use "mirror_mirror")
(("" (expand "mirror")
(("" (expand "image")
(("" (lemma "card_image[int, int]")
(("" (inst-cp - "complement" "image(complement, X!1)")
(("" (inst - "complement" "X!1") (("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((mirror_mirror formula-decl nil pigeonhole_int 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)
(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)
(image const-decl "set[R]" function_image nil)
(finite_image application-judgement "finite_set[R]"
function_image_aux nil)
(image const-decl "set[R]" function_image nil)
(complement const-decl "int" pigeonhole_int nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(card_image formula-decl nil function_image_aux nil)
(mirror const-decl "finite_set[int]" pigeonhole_int nil))
shostak))
(subset_mirror 0
(subset_mirror-1 nil 3362383733
("" (skosimp*)
(("" (expand "mirror")
(("" (expand "image") (("" (rewrite "image_subset") nil nil))
nil))
nil))
nil)
((mirror const-decl "finite_set[int]" pigeonhole_int nil)
(image_subset formula-decl nil function_image 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)
(complement const-decl "int" pigeonhole_int 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)
(image const-decl "set[R]" function_image nil))
shostak))
(mirror_nat 0
(mirror_nat-1 nil 3362381514 ("" (judgement-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)
(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)
(set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(>= const-decl "bool" reals nil)
(nat_set type-eq-decl nil pigeonhole_int nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(injective? const-decl "bool" functions 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)
(image const-decl "set[R]" function_image nil)
(mirror const-decl "finite_set[int]" pigeonhole_int nil)
(complement const-decl "int" pigeonhole_int nil)
(image const-decl "set[R]" function_image nil))
nil))
(mirror_negint 0
(mirror_negint-1 nil 3362381514 ("" (judgement-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)
(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)
(set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(< const-decl "bool" reals nil)
(negint_set type-eq-decl nil pigeonhole_int nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(injective? const-decl "bool" functions nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(image const-decl "set[R]" function_image nil)
(mirror const-decl "finite_set[int]" pigeonhole_int nil)
(complement const-decl "int" pigeonhole_int nil)
(image const-decl "set[R]" function_image nil))
nil))
(subset_split 0
(subset_split-1 nil 3362384514
("" (skosimp*)
(("" (expand "subset?")
(("" (expand "split")
(("" (expand "intersection")
(("" (expand "union")
(("" (expand "mirror")
(("" (expand "difference")
(("" (expand "member")
(("" (skosimp*)
(("" (split -)
(("1" (inst?)
(("1" (flatten) (("1" (assert) nil nil)) nil))
nil)
("2" (expand "image")
(("2" (expand "image")
(("2" (skosimp* t)
(("2" (inst? +)
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((subset? const-decl "bool" sets nil)
(intersection const-decl "set" sets nil)
(mirror const-decl "finite_set[int]" pigeonhole_int nil)
(member const-decl "bool" sets 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)
(image const-decl "set[R]" function_image nil)
(Y!1 skolem-const-decl "finite_set[int]" pigeonhole_int nil)
(X!1 skolem-const-decl "finite_set[int]" pigeonhole_int nil)
(Z!1 skolem-const-decl "finite_set[int]" pigeonhole_int nil)
(x!2 skolem-const-decl "({x | X!1(x) AND NOT Z!1(x)})"
pigeonhole_int 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)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(image const-decl "set[R]" function_image nil)
(difference const-decl "set" sets nil)
(union const-decl "set" sets nil)
(split const-decl "finite_set[int]" pigeonhole_int nil))
shostak))
(card_split 0
(card_split-1 nil 3362386173
("" (skosimp*)
(("" (expand "split")
(("" (rewrite "card_disj_union")
(("1" (rewrite "card_mirror")
(("1" (lemma "card_disj_union[int]")
(("1" (invoke (inst - "%1" "%2") (! 1 l 2 1) (! 1 l 1 1))
(("1" (assert)
(("1" (prop)
(("1" (replace -1 :dir rl)
(("1" (hide -1)
(("1" (rewrite "congruence")
(("1" (hide 2)
(("1" (decompose-equality)
(("1" (iff) (("1" (grind) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "disjoint?")
(("2" (expand "empty?")
(("2" (expand "intersection")
(("2" (expand "difference")
(("2" (expand "member")
(("2" (skosimp*) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (rewrite "disjoint1")
(("1" (hide 2)
(("1" (expand "mirror")
(("1" (expand "difference")
(("1" (expand "member")
(("1" (expand "image")
(("1" (expand "image")
(("1" (skosimp* t)
(("1" (typepred "A!1")
(("1" (inst?)
(("1"
(expand "complement")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "intersection")
(("2" (expand "member")
(("2" (skosimp*)
(("2" (assert)
(("2" (typepred " A!1")
(("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((split const-decl "finite_set[int]" pigeonhole_int nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(image const-decl "set[R]" function_image nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(complement const-decl "int" pigeonhole_int nil)
(image const-decl "set[R]" function_image nil)
(disjoint1 formula-decl nil pigeonhole_int nil)
(< const-decl "bool" reals nil)
(negint_set type-eq-decl nil pigeonhole_int nil)
(card_mirror formula-decl nil pigeonhole_int nil)
(member const-decl "bool" sets nil)
(congruence formula-decl nil functions 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)
(disjoint? const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(finite_union application-judgement "finite_set" finite_sets nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers 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)
(difference const-decl "set" sets nil)
(mirror const-decl "finite_set[int]" pigeonhole_int nil)
(nat_set type-eq-decl nil pigeonhole_int nil)
(>= const-decl "bool" reals nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans 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)
(card_disj_union formula-decl nil finite_sets nil)
(finite_difference application-judgement "finite_set" finite_sets
nil)
(finite_intersection1 application-judgement "finite_set"
finite_sets nil))
shostak))
(two_thirds_split 0
(two_thirds_split-1 nil 3362385320
("" (expand "two_thirds_majority_subset?")
(("" (skosimp*)
(("" (use "subset_split")
(("" (assert)
(("" (hide -1 -3)
(("" (rewrite "card_split")
(("" (rewrite "card_split") nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(even_times_int_is_even application-judgement "even_int" integers
nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(card_split formula-decl nil pigeonhole_int 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)
(set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(>= const-decl "bool" reals nil)
(nat_set type-eq-decl nil pigeonhole_int nil)
(subset_split formula-decl nil pigeonhole_int nil)
(two_thirds_majority_subset? const-decl "bool" pigeonhole nil))
shostak))
(two_thirds_overlap_lem 0
(two_thirds_overlap_lem-1 nil 3362392710
("" (skosimp*)
(("" (forward-chain "two_thirds_overlap_pigeonhole")
(("" (hide -2 -3 -4)
(("" (skosimp*)
(("" (expand "split")
(("" (expand "union")
(("" (expand "intersection")
(("" (expand "member")
(("" (prop)
(("1" (inst?) (("1" (assert) nil nil)) nil)
("2" (hide 1)
(("2" (expand "mirror")
(("2" (expand "image")
(("2" (expand "image")
(("2" (skosimp* t)
(("2"
(expand "difference")
(("2"
(expand "member")
(("2"
(flatten)
(("2"
(typepred "A!1")
(("2"
(inst?)
(("2"
(typepred "B!1")
(("2"
(inst - "x!2")
(("2"
(assert)
(("2"
(expand "complement")
(("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)
((two_thirds_overlap_pigeonhole formula-decl nil pigeonhole 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)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(>= const-decl "bool" reals nil)
(nat_set type-eq-decl nil pigeonhole_int nil)
(split const-decl "finite_set[int]" pigeonhole_int 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)
(union const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(image const-decl "set[R]" function_image nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(difference const-decl "set" sets nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(complement const-decl "int" pigeonhole_int nil)
(image const-decl "set[R]" function_image nil)
(mirror const-decl "finite_set[int]" pigeonhole_int nil)
(intersection const-decl "set" sets nil))
nil))
(fta_overlap_pigeonhole 0
(fta_overlap_pigeonhole-1 nil 3362390999
("" (skosimp*)
(("" (lemma "two_thirds_overlap_lem")
(("" (inst?)
(("" (inst - "S1!1" "S2!1")
(("" (assert)
(("" (rewrite "two_thirds_split")
(("" (prop)
(("" (hide -1 -2 2)
(("" (expand "byzantine_intersection_majority?")
(("" (expand "intersection_majority?")
(("" (expand "split")
(("" (rewrite "distribute_intersection_union")
(("" (rewrite "card_disj_union")
(("1" (lemma "disjoint1")
(("1"
(expand "disjoint?")
(("1"
(inst?)
(("1"
(use "empty_card[int]")
(("1"
(assert)
(("1"
(replace -1)
(("1"
(assert)
(("1"
(hide -1 -2)
(("1"
(invoke
(then
(case "%1 <= %2")
(assert)
(hide -1 2))
(! 1 r)
(! -1 r))
(("1"
(rewrite
"union_associative"
:dir
rl)
(("1"
(rewrite
"card_disj_union")
(("1"
(rewrite
"card_mirror")
(("1"
(isolate 1 l 2)
(("1"
(assert)
(("1"
(rewrite
"card_subset")
(("1"
(hide 2)
(("1"
(expand
"subset?")
(("1"
(expand
"intersection")
(("1"
(expand
"union")
(("1"
(expand
"member")
(("1"
(skosimp*)
(("1"
(prop)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(rewrite
"disjoint1")
(("1"
(hide 2)
(("1"
(expand
"difference")
(("1"
(expand
"member")
(("1"
(expand
"mirror")
(("1"
(expand
"image")
(("1"
(expand
"image")
(("1"
(expand
"complement")
(("1"
(skosimp*
t)
(("1"
(typepred
"S2!1")
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide 2)
(("2"
(expand
"intersection")
(("2"
(expand
"union")
(("2"
(expand
"member")
(("2"
(skosimp*)
(("2"
(typepred
"S1!1")
(("2"
(inst?)
(("2"
(typepred
"S2!1")
(("2"
(inst?)
(("2"
(prop)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -1 2)
(("2"
(expand "difference")
(("2"
(expand "member")
(("2"
(expand "mirror")
(("2"
(expand "image")
(("2"
(expand "image")
(("2"
(expand "complement")
(("2"
(skosimp* t)
(("2"
(assert)
(("2"
(typepred "S2!1")
(("2"
(inst?)
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -1 2)
(("2"
(expand "disjoint?")
(("2"
(expand "intersection")
(("2"
(expand "empty?")
(("2"
(expand "difference")
(("2"
(expand "mirror")
(("2"
(expand "member")
(("2"
(expand "image")
(("2"
(expand "image")
(("2"
(expand "complement")
(("2"
(skosimp* t)
(("2"
(assert)
(("2"
(typepred "S2!1")
(("2"
(inst-cp
-
"x!2")
(("2"
(inst
-
"x!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))
nil))
nil)
((two_thirds_overlap_lem formula-decl nil pigeonhole_int nil)
(two_thirds_split formula-decl nil pigeonhole_int nil)
(intersection_majority? const-decl "bool" pigeonhole nil)
(difference const-decl "set" sets nil)
(mirror const-decl "finite_set[int]" pigeonhole_int nil)
(intersection const-decl "set" sets nil)
(distribute_intersection_union formula-decl nil sets_lemmas nil)
(finite_difference application-judgement "finite_set" finite_sets
nil)
(finite_intersection1 application-judgement "finite_set"
finite_sets nil)
(finite_union application-judgement "finite_set" finite_sets nil)
(empty? const-decl "bool" sets nil)
(disjoint1 formula-decl nil pigeonhole_int nil)
(S2!1 skolem-const-decl "nat_set" pigeonhole_int nil)
(C!1 skolem-const-decl "nat_set" pigeonhole_int nil)
(< const-decl "bool" reals nil)
(negint_set type-eq-decl nil pigeonhole_int nil)
(even_plus_even_is_even application-judgement "even_int" integers
nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields 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)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(- const-decl "[numfield, numfield -> numfield]" number_fields nil)
(IFF const-decl "[bool, bool -> bool]" booleans nil)
(int_minus_int_is_int application-judgement "int" integers 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)
(member const-decl "bool" sets nil)
(card_mirror formula-decl nil pigeonhole_int nil)
(image const-decl "set[R]" function_image nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(complement const-decl "int" pigeonhole_int nil)
(image const-decl "set[R]" function_image nil)
(union_associative formula-decl nil sets_lemmas nil)
(empty_card formula-decl nil finite_sets nil)
(disjoint? 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)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(card_disj_union formula-decl nil finite_sets nil)
(split const-decl "finite_set[int]" pigeonhole_int nil)
(byzantine_intersection_majority? const-decl "bool" pigeonhole nil)
(nat_set type-eq-decl nil pigeonhole_int nil)
(>= const-decl "bool" reals nil)
(IMPLIES const-decl "[bool, 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)
(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)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.58Angebot
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
|
