|
(cauchy_scaf
(set_seq_TCC1 0
(set_seq_TCC1-1 nil 3529325333 ("" (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)
(below type-eq-decl nil nat_types nil)
(< const-decl "bool" reals nil))
nil))
(emptyset_gives_emptyset 0
(emptyset_gives_emptyset-1 nil 3529250300
("" (skosimp)
(("" (expand "empty?")
(("" (skosimp)
(("" (expand "member")
(("" (expand "add_element")
(("" (skosimp)
(("" (inst -1 "s!1") (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((empty? const-decl "bool" sets nil)
(member const-decl "bool" 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)
(finseq type-eq-decl nil finite_sequences nil)
(T formal-type-decl nil cauchy_scaf nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(add_element const-decl "set[finseq]" cauchy_scaf nil))
shostak))
(emptyset_gives_emptyset1 0
(emptyset_gives_emptyset1-1 nil 3529255354
("" (skosimp)
(("" (expand* "empty?" "member")
(("" (skosimp)
(("" (expand "add_set")
(("" (skosimp) (("" (inst?) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(add_set const-decl "setofsets[finseq]" cauchy_scaf nil)
(T formal-type-decl nil cauchy_scaf 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))
shostak))
(set_seq_singleton 0
(set_seq_singleton-1 nil 3529322733
("" (skosimp)
(("" (decompose-equality 1)
(("" (iff)
(("" (prop)
(("1" (expand* "set_seq" "singleton")
(("1" (rewrite "empty_0") (("1" (assert) nil nil)) nil))
nil)
("2" (expand* "set_seq" "singleton")
(("2" (rewrite "empty_0")
(("2" (assert) (("2" (skosimp) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets 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)
(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)
(set_seq const-decl "set[finseq]" cauchy_scaf nil)
(singleton? const-decl "bool" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(empty_seq const-decl "finseq" finite_sequences nil)
(boolean nonempty-type-decl nil booleans nil)
(finseq type-eq-decl nil finite_sequences nil)
(T formal-type-decl nil cauchy_scaf nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(empty_0 formula-decl nil seq_extras "structures/"))
shostak))
(set_seq_empty 0
(set_seq_empty-1 nil 3529331756
("" (skosimp)
(("" (expand* "empty?" "member")
(("" (skosimp)
(("" (expand "set_seq")
(("" (flatten)
(("" (inst -3 "0")
(("" (expand "member") (("" (inst?) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(set_seq const-decl "set[finseq]" cauchy_scaf nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props 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)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(> const-decl "bool" reals nil)
(posnat nonempty-type-eq-decl nil integers nil)
(below type-eq-decl nil nat_types nil)
(T formal-type-decl nil cauchy_scaf nil)
(finseq type-eq-decl nil finite_sequences nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil))
shostak))
(add_element_add_set 0
(add_element_add_set-1 nil 3529269674
("" (skosimp)
(("" (skoletin* 1)
(("" (skoletin* 2)
(("" (decompose-equality 1)
(("" (iff)
(("" (prop)
(("1" (expand* "Union" "union" "member")
(("1" (skosimp)
(("1" (typepred "a!2")
(("1" (expand "add_set" -1)
(("1" (skosimp)
(("1" (replaces -1)
(("1" (replaces -2)
(("1" (case-replace "a!3 = a!1")
(("1"
(hide 3)
(("1"
(inst?)
(("1"
(replaces -2)
(("1"
(expand "add_set")
(("1"
(inst?)
(("1"
(typepred "a!3")
(("1"
(expand "add")
(("1"
(expand "member")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand* "Union" "union" "member")
(("2" (prop)
(("1" (skosimp)
(("1" (typepred "a!2")
(("1" (replaces -4)
(("1" (inst?)
(("1" (expand "add_set")
(("1" (skosimp)
(("1"
(inst?)
(("1"
(expand "add")
(("1"
(expand "member")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (replaces -2)
(("2" (inst?)
(("2" (expand "add_set")
(("2" (inst?)
(("2" (expand "add") (("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((IFF 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-type-decl nil cauchy_scaf nil)
(finseq type-eq-decl nil finite_sequences nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(add_set const-decl "setofsets[finseq]" cauchy_scaf nil)
(add_element const-decl "set[finseq]" cauchy_scaf nil)
(union const-decl "set" sets nil)
(add const-decl "(nonempty?)" sets nil)
(nonempty? const-decl "bool" sets nil)
(Union const-decl "set" sets nil)
(nonempty_add_finite application-judgement
"non_empty_finite_set[T]" cauchy_scaf nil)
(a!3 skolem-const-decl "(M!1)" cauchy_scaf nil)
(a!2 skolem-const-decl "(B)" cauchy_scaf nil)
(member const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(a!3 skolem-const-decl "(add(a!1, M!1))" cauchy_scaf nil)
(M!1 skolem-const-decl "finite_set[T]" cauchy_scaf nil)
(a!1 skolem-const-decl "T" cauchy_scaf nil)
(S!1 skolem-const-decl "finite_set[finseq]" cauchy_scaf nil)
(B skolem-const-decl "setofsets[finseq]" cauchy_scaf nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil))
shostak))
(card_add_element_aux 0
(card_add_element_aux-1 nil 3529246650
("" (skosimp)
(("" (skoletin 1)
(("" (inst 1 "LAMBDA (x: (A)): rest(x)")
(("1" (expand "bijective?")
(("1" (prop)
(("1" (expand "injective?")
(("1" (skosimp)
(("1" (typepred "x1!1" "x2!1")
(("1" (replaces -4)
(("1" (expand "add_element")
(("1" (skosimp*)
(("1" (replace -1 -3)
(("1" (replace -2 -3)
(("1" (rewrite "rest_add_first")
(("1"
(rewrite "rest_add_first")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "surjective?")
(("2" (skosimp)
(("2" (inst 1 "add_first(a!1, y!1)")
(("1" (rewrite "rest_add_first") nil nil)
("2" (replaces -1)
(("2" (expand "add_element")
(("2" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (typepred "x!1")
(("2" (replaces -2)
(("2" (expand "add_element")
(("2" (skosimp)
(("2" (replaces -1)
(("2" (rewrite "rest_add_first")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((IFF 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-type-decl nil cauchy_scaf nil)
(finseq type-eq-decl nil finite_sequences nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(add_element const-decl "set[finseq]" cauchy_scaf nil)
(bijective? const-decl "bool" functions nil)
(surjective? const-decl "bool" functions nil)
(add_first const-decl "finseq" seq_extras "structures/")
(a!1 skolem-const-decl "T" cauchy_scaf nil)
(y!1 skolem-const-decl "(S!1)" cauchy_scaf nil)
(injective? const-decl "bool" functions nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(rest_add_first formula-decl nil seq_extras "structures/")
(rest const-decl "finseq" seq_extras "structures/")
(S!1 skolem-const-decl "finite_set[finseq]" cauchy_scaf nil)
(A skolem-const-decl "set[finseq]" cauchy_scaf nil))
shostak))
(card_add_element_TCC1 0
(card_add_element_TCC1-1 nil 3529239379
("" (skosimp)
(("" (lemma "card_add_element_aux")
(("" (inst?)
(("" (replace -2 -1 rl)
(("" (assert)
(("" (lemma "bijection_finite_set1[finseq,finseq]")
(("" (inst -1 "S!1" "A!1") (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((card_add_element_aux formula-decl nil cauchy_scaf nil)
(bijection_finite_set1 formula-decl nil finite_sets_eq
"finite_sets/")
(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)
(finseq type-eq-decl nil finite_sequences nil)
(T formal-type-decl nil cauchy_scaf nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
nil))
(card_add_element 0
(card_add_element-1 nil 3529247197
("" (skosimp)
(("" (skoletin 1)
(("1" (lemma "card_add_element_aux")
(("1" (inst?)
(("1" (replace -2 -1 rl)
(("1" (assert)
(("1" (lemma "card_eq_bij[finseq,finseq]")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (lemma "card_add_element_TCC1")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil)
((boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(bijective? const-decl "bool" functions nil)
(id const-decl "(bijective?[T, T])" identity nil)
(TRUE const-decl "bool" booleans nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(below type-eq-decl nil nat_types nil)
(T formal-type-decl nil cauchy_scaf nil)
(finseq type-eq-decl nil finite_sequences nil)
(set type-eq-decl nil sets nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(is_finite const-decl "bool" finite_sets nil)
(finite_set type-eq-decl nil finite_sets nil)
(add_element const-decl "set[finseq]" cauchy_scaf nil)
(IFF const-decl "[bool, bool -> bool]" booleans 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)
(number nonempty-type-decl nil numbers nil)
(card_eq_bij formula-decl nil finite_sets_card_eq "finite_sets/")
(card_add_element_aux formula-decl nil cauchy_scaf nil))
shostak))
(disjoint_add_set 0
(disjoint_add_set-1 nil 3529247423
("" (skosimp)
(("" (skoletin* 1)
(("" (prop)
(("" (expand "disjoint?")
(("" (expand* "empty?" "intersection")
(("" (skosimp)
(("" (expand "member")
(("" (flatten)
(("" (expand "Union")
(("" (skosimp)
(("" (typepred "a!2")
(("" (replaces -5)
(("" (replaces -4)
(("" (expand* "add_set" "add_element")
((""
(skosimp*)
((""
(replaces -1)
((""
(assert)
((""
(skosimp)
((""
(replaces -1)
((""
(lemma "first_equal")
((""
(inst?)
(("" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((IFF 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-type-decl nil cauchy_scaf nil)
(finseq type-eq-decl nil finite_sequences nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(add_set const-decl "setofsets[finseq]" cauchy_scaf nil)
(add_element const-decl "set[finseq]" cauchy_scaf nil)
(Union const-decl "set" sets nil)
(disjoint? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(first_equal formula-decl nil seq_extras "structures/")
(empty? const-decl "bool" sets nil)
(intersection const-decl "set" sets nil))
shostak))
(add_set_is_add_ele 0
(add_set_is_add_ele-1 nil 3529238634
("" (skosimp)
(("" (skoletin* 1)
(("" (prop)
(("" (decompose-equality 1)
(("" (iff)
(("" (prop)
(("1" (expand "Union")
(("1" (skosimp)
(("1" (typepred "a!2")
(("1" (expand "B" -1)
(("1" (expand "add_set" -1)
(("1" (skosimp)
(("1" (replaces -1)
(("1" (typepred "a!3")
(("1"
(decompose-equality -3)
(("1"
(inst?)
(("1"
(iff)
(("1"
(prop)
(("1"
(expand "singleton")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "Union")
(("2" (inst?)
(("2" (replaces -4)
(("2" (expand "add_set")
(("2" (inst?)
(("2" (decompose-equality -2)
(("2" (inst?)
(("2" (iff)
(("2"
(prop)
(("2"
(expand "singleton")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((IFF 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-type-decl nil cauchy_scaf nil)
(finseq type-eq-decl nil finite_sequences nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(add_set const-decl "setofsets[finseq]" cauchy_scaf nil)
(add_element const-decl "set[finseq]" cauchy_scaf nil)
(Union const-decl "set" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(singleton? const-decl "bool" sets nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set[T]" cauchy_scaf nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(B skolem-const-decl "setofsets[finseq]" cauchy_scaf nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(A skolem-const-decl "set[finseq]" cauchy_scaf nil)
(a!1 skolem-const-decl "T" cauchy_scaf nil)
(M!1 skolem-const-decl "finite_set[T]" cauchy_scaf nil))
shostak))
(add_set_is_finite_aux 0
(add_set_is_finite_aux-1 nil 3529248399
("" (skosimp)
(("" (skoletin 1)
(("" (inst 1 "LAMBDA (x: (M!1)): add_element(S!1)(x)")
(("1" (expand "bijective?")
(("1" (prop)
(("1" (expand "injective?")
(("1" (skosimp)
(("1" (decompose-equality -1)
(("1" (inst -1 "add_first(x1!1, choose(S!1))")
(("1" (iff)
(("1" (prop)
(("1" (expand "add_element")
(("1" (skosimp*)
(("1" (replaces -1)
(("1"
(lemma "first_equal")
(("1"
(inst?)
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide (1 3))
(("2" (expand "add_element")
(("2" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "surjective?")
(("2" (skosimp)
(("2" (typepred "y!1")
(("2" (replaces -2)
(("2" (expand "add_set")
(("2" (skosimp)
(("2" (inst?) (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp)
(("2" (replaces -1)
(("2" (expand "add_set") (("2" (inst?) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((IFF 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-type-decl nil cauchy_scaf nil)
(finseq type-eq-decl nil finite_sequences nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(add_set const-decl "setofsets[finseq]" cauchy_scaf nil)
(bijective? const-decl "bool" functions nil)
(surjective? const-decl "bool" functions nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(injective? const-decl "bool" functions nil)
(first_equal formula-decl nil seq_extras "structures/")
(add_first const-decl "finseq" seq_extras "structures/")
(choose const-decl "(p)" sets nil)
(nonempty? const-decl "bool" sets nil)
(M!1 skolem-const-decl "finite_set[T]" cauchy_scaf nil)
(B skolem-const-decl "setofsets[finseq]" cauchy_scaf nil)
(add_element const-decl "set[finseq]" cauchy_scaf nil)
(S!1 skolem-const-decl "finite_set[finseq]" cauchy_scaf nil))
shostak))
(add_set_is_finite 0
(add_set_is_finite-1 nil 3529247905
("" (skosimp)
(("" (skoletin 1)
(("" (case "empty?(S!1)")
(("1" (case "empty?(M!1)")
(("1" (lemma "emptyset_gives_emptyset1")
(("1" (inst?)
(("1" (assert)
(("1" (replace -4 -1 rl)
(("1" (hide (-2 -3 -4))
(("1" (rewrite "emptyset_is_empty?")
(("1" (lemma "finite_emptyset[finseq]")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (case "B = singleton(emptyset)")
(("1" (hide (-2 -3 1))
(("1" (replaces -1)
(("1" (rewrite "finite_singleton") nil nil)) nil))
nil)
("2" (hide 3)
(("2" (decompose-equality 1)
(("2" (iff)
(("2" (prop)
(("1" (expand "singleton")
(("1" (replaces -3)
(("1" (expand "add_set")
(("1" (skosimp)
(("1" (lemma "emptyset_gives_emptyset")
(("1"
(inst?)
(("1"
(assert)
(("1"
(replace -2 -1 rl)
(("1"
(hide (-2 -3))
(("1"
(rewrite "emptyset_is_empty?")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "singleton")
(("2" (replaces -3)
(("2" (expand "add_set")
(("2" (inst 1 "choose(M!1)")
(("1" (lemma "emptyset_gives_emptyset")
(("1"
(inst?)
(("1"
(assert)
(("1"
(rewrite "emptyset_is_empty?")
nil
nil))
nil))
nil))
nil)
("2" (expand "nonempty?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "add_set_is_finite_aux")
(("2" (inst?)
(("2" (expand "nonempty?")
(("2" (assert)
(("2" (replaces -2)
(("2" (lemma "bijection_finite_set2[T,set[finseq]]")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((IFF 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-type-decl nil cauchy_scaf nil)
(finseq type-eq-decl nil finite_sequences nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(add_set const-decl "setofsets[finseq]" cauchy_scaf nil)
(add_set_is_finite_aux formula-decl nil cauchy_scaf nil)
(bijection_finite_set2 formula-decl nil finite_sets_eq
"finite_sets/")
(emptyset_is_empty? formula-decl nil sets_lemmas nil)
(finite_emptyset name-judgement "finite_set" finite_sets nil)
(finite_emptyset judgement-tcc nil finite_sets nil)
(emptyset_gives_emptyset1 formula-decl nil cauchy_scaf nil)
(add_element const-decl "set[finseq]" cauchy_scaf nil)
(choose const-decl "(p)" sets nil)
(M!1 skolem-const-decl "finite_set[T]" cauchy_scaf nil)
(nonempty? const-decl "bool" sets nil)
(emptyset_gives_emptyset formula-decl nil cauchy_scaf nil)
(finite_singleton judgement-tcc nil finite_sets nil)
(emptyset const-decl "set" sets nil)
(singleton const-decl "(singleton?)" sets nil)
(singleton? const-decl "bool" sets nil)
(nonempty_singleton_finite application-judgement
"non_empty_finite_set" finite_sets nil)
(empty? const-decl "bool" sets nil))
shostak))
(card_add_set_TCC1 0
(card_add_set_TCC1-1 nil 3529240214
("" (skosimp)
(("" (lemma "Union_finite[finseq]")
(("" (inst -1 "B!1")
(("" (assert)
(("" (hide 2)
(("" (prop)
(("1" (lemma "add_set_is_finite")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
("2" (expand "every")
(("2" (skosimp)
(("2" (typepred "x!1")
(("2" (replaces -2)
(("2" (expand "add_set")
(("2" (skosimp)
(("2" (lemma "card_add_element_TCC1")
(("2" (inst?) (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((finseq type-eq-decl nil finite_sequences nil)
(T formal-type-decl nil cauchy_scaf nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(Union_finite formula-decl nil finite_sets_of_sets nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas 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)
(add_set_is_finite formula-decl nil cauchy_scaf nil)
(card_add_element_TCC1 subtype-tcc nil cauchy_scaf nil)
(add_set const-decl "setofsets[finseq]" cauchy_scaf nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(every const-decl "bool" sets nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(card_add_set 0
(card_add_set-1 nil 3529256829
("" (measure-induct+ "card(M)" "M")
(("1" (skosimp)
(("1" (case "empty?(x!1)")
(("1" (hide -2)
(("1" (lemma "empty_card[T]")
(("1" (inst?)
(("1" (assert)
(("1" (replace -1 1)
(("1" (assert)
(("1" (case "empty?(Union(add_set(S!1)(x!1)))")
(("1" (rewrite "empty_card" -1) nil nil)
("2" (hide (-1 2))
(("2" (lemma "Union_empty[finseq]")
(("2" (inst?)
(("2" (assert)
(("2"
(hide 2)
(("2"
(flatten)
(("2"
(hide 2)
(("2"
(lemma
"emptyset_gives_emptyset1")
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst -1 "rest(x!1)" "S!1")
(("2" (prop)
(("1" (lemma "choose_rest[T]")
(("1" (inst?)
(("1" (assert)
(("1" (replace -1 2 rl)
(("1" (lemma "add_element_add_set")
(("1" (inst -1 "rest(x!1)" "S!1" "choose(x!1)")
(("1" (prop)
(("1" (assert)
(("1" (replaces -1)
(("1"
(replaces -1)
(("1"
(lemma "choose_not_member[T]")
(("1"
(inst?)
(("1"
(assert)
(("1"
(lemma "disjoint_add_set")
(("1"
(inst
-1
"rest(x!1)"
"S!1"
"choose(x!1)")
(("1"
(assert)
(("1"
(lemma
"card_disj_union[finseq]")
(("1"
(inst?)
(("1"
(assert)
(("1"
(replaces -1)
(("1"
(replaces -2)
(("1"
(hide (-1 1 2))
(("1"
(lemma
"card_add_element")
(("1"
(inst?)
(("1"
(assert)
(("1"
(replaces
-1)
(("1"
(lemma
"card_rest[T]")
(("1"
(inst?)
(("1"
(assert)
(("1"
(replaces
-1)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but 1)
(("2"
(lemma
"card_add_element_aux")
(("2"
(inst?)
(("2"
(assert)
(("2"
(lemma
"bijection_finite_set1[finseq, finseq]")
(("2"
(inst
-1
"S!1"
"add_element(S!1)(choose[T](x!1))")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide (-2 -3 2))
(("2" (lemma "choose_not_member[T]")
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 3)
(("2" (lemma "card_rest[T]")
(("2" (inst?) (("2" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide-all-but 1)
(("2" (lemma "card_add_set_TCC1")
(("2" (inst -1 "y!1" "S!1" "add_set(S!1)(y!1)") nil nil)) nil))
nil)
("3" (hide 2)
(("3" (lemma "card_add_set_TCC1")
(("3" (inst?) (("3" (assert) nil nil)) nil)) nil))
nil))
nil)
((card_add_set_TCC1 subtype-tcc nil cauchy_scaf nil)
(finite_rest application-judgement "finite_set[T]" cauchy_scaf nil)
(rest const-decl "set" sets nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(choose_rest formula-decl nil sets_lemmas nil)
(add_element_add_set formula-decl nil cauchy_scaf nil)
(choose_not_member formula-decl nil sets_lemmas nil)
(card_disj_union formula-decl nil finite_sets nil)
(bijection_finite_set1 formula-decl nil finite_sets_eq
"finite_sets/")
(card_add_element_aux formula-decl nil cauchy_scaf nil)
(card_add_element formula-decl nil cauchy_scaf nil)
(nnint_plus_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(card_rest formula-decl nil finite_sets nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(int_plus_int_is_int application-judgement "int" integers nil)
(x!1 skolem-const-decl "finite_set[T]" cauchy_scaf nil)
(S!1 skolem-const-decl "finite_set[finseq]" cauchy_scaf nil)
(add_element const-decl "set[finseq]" cauchy_scaf nil)
(disjoint_add_set formula-decl nil cauchy_scaf nil)
(nonempty_add_finite application-judgement
"non_empty_finite_set[T]" cauchy_scaf nil)
(nonempty? const-decl "bool" sets nil)
(choose const-decl "(p)" sets nil)
(Union_empty formula-decl nil sets_lemmas nil)
(emptyset_gives_emptyset1 formula-decl nil cauchy_scaf nil)
(int_times_even_is_even application-judgement "even_int" integers
nil)
(Union_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(nnint_times_nnint_is_nnint application-judgement "nonneg_int"
integers nil)
(mult_divides1 application-judgement "(divides(n))" divides nil)
(mult_divides2 application-judgement "(divides(m))" divides nil)
(empty_card formula-decl nil finite_sets nil)
(empty? const-decl "bool" sets nil)
(* const-decl "[numfield, numfield -> numfield]" number_fields nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(Union const-decl "set" sets nil)
(add_set const-decl "setofsets[finseq]" cauchy_scaf nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(finseq type-eq-decl nil finite_sequences nil)
(below type-eq-decl nil nat_types nil)
(wf_nat formula-decl nil naturalnumbers nil)
(< const-decl "bool" reals 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)
(naturalnumber 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)
(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 cauchy_scaf nil)
(measure_induction formula-decl nil measure_induction nil)
(well_founded? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil))
shostak))
(set_seq_is_finite 0
(set_seq_is_finite-1 nil 3529321863
("" (induct "n")
(("1" (skosimp)
(("1" (skoletin 1) (("1" (inst?) (("1" (assert) nil nil)) nil))
nil))
nil)
("2" (skosimp)
(("2" (lemma "set_seq_singleton")
(("2" (inst?)
(("2" (replaces -1)
(("2" (rewrite "finite_singleton") nil nil)) nil))
nil))
nil))
nil)
("3" (skosimp*)
(("3" (inst?)
(("3" (name-replace "C!1" "set_seq(M!1)(1 + j!1)" :hide? nil)
(("3" (name-replace "S!1" "set_seq(M!1)(j!1)" :hide? nil)
(("3" (case "C!1 = Union(add_set(S!1)(M!1))")
(("1" (replace -1 1)
(("1" (lemma "card_add_set_TCC1")
(("1" (inst -1 "M!1" "S!1" "add_set(S!1)(M!1)") nil
nil))
nil))
nil)
("2" (hide 2)
(("2" (decompose-equality 1)
(("2" (iff)
(("2" (prop)
(("1" (expand "Union")
(("1" (replace -3 -1 rl)
(("1" (expand "set_seq" -1)
(("1" (flatten)
(("1"
(inst 1 "add_element(S!1)(x!1(0))")
(("1"
(expand "add_element")
(("1"
(inst 1 "rest(x!1)")
(("1"
(lemma "seq_first_rest")
(("1"
(inst?)
(("1"
(assert)
(("1"
(expand "first")
(("1" (propax) nil nil))
nil))
nil))
nil))
nil)
("2"
(replace -3 1 rl)
(("2"
(expand "set_seq" 1)
(("2"
(prop)
(("1"
(hide-all-but (-1 1))
(("1" (grind) nil nil))
nil)
("2"
(skosimp)
(("2"
(expand*
"member"
"finseq_appl")
(("2"
(case
"rest(x!1)`length = 0")
(("1"
(hide-all-but
(-1 -2 1))
(("1"
(grind)
nil
nil))
nil)
("2"
(inst -2 "i!1 + 1")
(("2"
(lemma "rest_pos")
(("2"
(inst?)
(("2"
(assert)
(("2"
(inst
-1
"i!1")
(("2"
(expand
"finseq_appl")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "add_set" 1)
(("2"
(inst 1 "x!1(0)")
(("1"
(inst -2 "0")
(("1"
(expand " member")
(("1" (propax) nil nil))
nil))
nil)
("2" (assert) nil nil))
nil))
nil)
("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (replace -3 1 rl)
(("2" (expand "Union")
(("2" (skosimp)
(("2" (typepred "a!1")
(("2"
(expand "add_set")
(("2"
(skosimp)
(("2"
(replaces -1)
(("2"
(expand "add_element")
(("2"
(skosimp)
(("2"
(typepred "s!1")
(("2"
(replace -3 -1 rl)
(("2"
(expand "set_seq" (-1 1))
(("2"
(flatten)
(("2"
(prop)
(("1"
(hide-all-but
(-1 -3 1))
(("1"
(grind)
nil
nil))
nil)
("2"
(skosimp)
(("2"
(expand "member")
(("2"
(case-replace
"i!1 = 0")
(("1"
(hide-all-but
(-4 1))
(("1"
(lemma
"first_add")
(("1"
(inst?)
(("1"
(replace
-2
-1
rl)
(("1"
(expand
"first")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst
-2
"i!1 - 1")
(("1"
(lemma
"rest_pos")
(("1"
(inst?)
(("1"
(prop)
(("1"
(inst
-1
"i!1 - 1")
(("1"
(assert)
(("1"
(lemma
"rest_add_first")
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(-1
-3
1
2))
(("2"
(grind)
nil
nil))
nil))
nil)
("2"
(hide-all-but
(-1
-2
-4
1))
(("2"
(grind)
nil
nil))
nil))
nil))
nil))
nil)
("2"
(hide-all-but
(1 2))
(("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)
("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((posint_plus_nnint_is_posint application-judgement "posint"
integers nil)
(numfield nonempty-type-eq-decl nil number_fields nil)
(+ const-decl "[numfield, numfield -> numfield]" number_fields nil)
(nnint_plus_posint_is_posint application-judgement "posint"
integers nil)
(int_minus_int_is_int application-judgement "int" integers nil)
(setof type-eq-decl nil defined_types nil)
(setofsets type-eq-decl nil sets nil)
(Union const-decl "set" sets nil)
(add_set const-decl "setofsets[finseq]" cauchy_scaf nil)
--> --------------------
--> maximum size reached
--> --------------------
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.84Angebot
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
|
