|
(subset_chain
(subset_chain_min 0
(subset_chain_min-1 nil 3314727715 ("" (grind) 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 subset_chain nil)
(set type-eq-decl nil sets nil)
(chain? const-decl "bool" chain nil)
(chain nonempty-type-eq-decl nil chain nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
subset_chain nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(reflexive_restrict application-judgement "(reflexive?[S])"
restrict_order_props nil)
(antisymmetric_restrict application-judgement "(antisymmetric?[S])"
restrict_order_props nil)
(transitive_restrict application-judgement "(transitive?[S])"
restrict_order_props nil)
(preorder_restrict application-judgement "(preorder?[S])"
restrict_order_props nil)
(partial_order_restrict application-judgement "(partial_order?[S])"
restrict_order_props nil)
(restrict const-decl "R" restrict nil)
(dichotomous? const-decl "bool" orders nil)
(total_order? const-decl "bool" orders nil)
(Intersection const-decl "set" sets nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil))
shostak))
(subset_chain_intersection 0
(subset_chain_intersection-1 nil 3314727727
("" (skosimp :preds? t)
(("" (expand "maximal_chain?")
(("" (lemma "subset_chain_min" ("C" "C!1"))
(("" (inst + "add(Intersection(C!1), C!1)")
(("1" (expand "strict_subset?")
(("1" (use "subset_add[set[T]]")
(("1" (assert)
(("1" (decompose-equality)
(("1" (inst - "Intersection(C!1)")
(("1" (expand* "add" "member") nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (grind :if-match nil)
(("1" (expand "Intersection")
(("1" (decompose-equality)
(("1" (inst - "x!2")
(("1" (assert) (("1" (inst - "y!1") nil nil)) nil))
nil))
nil))
nil)
("2" (inst - "x!1")
(("2" (inst - "x!3")
(("2" (assert)
(("2" (expand "Intersection")
(("2" (decompose-equality)
(("2" (inst - "x!3") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (inst -6 "x!1" "y!1")
(("3" (split)
(("1" (inst - "x!2") (("1" (assert) nil nil)) nil)
("2" (inst - "x!3") (("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((maximal_chain? const-decl "bool" chain nil)
(Intersection_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" subset_chain nil)
(Intersection_surjective name-judgement
"(surjective?[setofsets[T], set[T]])" sets_lemmas nil)
(C!1 skolem-const-decl "chain[set[T], subset?]" subset_chain nil)
(Intersection const-decl "set" sets nil)
(setofsets type-eq-decl nil sets nil)
(setof type-eq-decl nil defined_types nil)
(add const-decl "(nonempty?)" sets nil)
(nonempty? const-decl "bool" sets nil)
(subset_add formula-decl nil sets_lemmas nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(member const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(strict_subset? const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
subset_chain nil)
(reflexive_restrict application-judgement "(reflexive?[S])"
restrict_order_props nil)
(antisymmetric_restrict application-judgement "(antisymmetric?[S])"
restrict_order_props nil)
(transitive_restrict application-judgement "(transitive?[S])"
restrict_order_props nil)
(preorder_restrict application-judgement "(preorder?[S])"
restrict_order_props nil)
(partial_order_restrict application-judgement "(partial_order?[S])"
restrict_order_props nil)
(restrict const-decl "R" restrict nil)
(dichotomous? const-decl "bool" orders nil)
(total_order? const-decl "bool" orders nil)
(subset_chain_min formula-decl nil subset_chain 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 subset_chain nil)
(set type-eq-decl nil sets nil)
(subset? const-decl "bool" sets nil)
(chain? const-decl "bool" chain nil)
(chain nonempty-type-eq-decl nil chain nil))
shostak)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.25Angebot
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
|
