|
(well_ordering
(ordered_set_order_TCC1 0
(ordered_set_order_TCC1-1 nil 3315836233 ("" (subtype-tcc) nil nil)
((ordered_set type-eq-decl nil well_ordering nil)
(well_ordered? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil well_ordering nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil))
nil))
(ordered_set_order_TCC2 0
(ordered_set_order_TCC2-1 nil 3315836233 ("" (subtype-tcc) nil nil)
((ordered_set type-eq-decl nil well_ordering nil)
(well_ordered? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil well_ordering nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil))
nil))
(ordered_set_order_TCC3 0
(ordered_set_order_TCC3-1 nil 3315836233 ("" (subtype-tcc) nil nil)
((ordered_set type-eq-decl nil well_ordering nil)
(well_ordered? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(difference const-decl "set" sets nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil well_ordering nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil))
nil))
(partial_ordered_set 0
(partial_ordered_set-1 nil 3315836233
("" (grind :if-match nil)
(("1" (grind-with-ext) nil nil)
("2" (inst - "r!1")
(("2" (assert)
(("2" (inst -9 "t!1")
(("1" (inst -9 "r!1") nil nil)
("2" (inst -7 "t!1")
(("2" (inst -7 "r!1")
(("2" (inst -9 "r!1" "t!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (inst-cp - "r!1")
(("3" (inst - "t!1")
(("3" (assert)
(("3" (inst - "t!1" "r!1")
(("3" (inst -8 "t!1" "r!1") (("3" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("4" (inst-cp - "r!1")
(("4" (inst - "t!1")
(("4" (assert)
(("4" (inst - "t!1" "r!1")
(("4" (inst -8 "t!1" "r!1") (("4" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("5" (inst - "x!2")
(("5" (inst -4 "x!2") (("5" (assert) nil nil)) nil)) nil))
nil)
((y!1 skolem-const-decl "ordered_set" well_ordering nil)
(z!1 skolem-const-decl "ordered_set" well_ordering nil)
(x!1 skolem-const-decl "ordered_set" well_ordering nil)
(t!1 skolem-const-decl "(difference(z!1`1, x!1`1))" well_ordering
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 well_ordering nil)
(set type-eq-decl nil sets nil)
(difference const-decl "set" sets nil)
(pred type-eq-decl nil defined_types nil)
(well_ordered? const-decl "bool" orders nil)
(ordered_set type-eq-decl nil well_ordering nil)
(restrict const-decl "R" restrict nil)
(partial_order? const-decl "bool" orders nil)
(antisymmetric? const-decl "bool" relations nil)
(preorder? const-decl "bool" orders nil)
(transitive? const-decl "bool" relations nil)
(reflexive? const-decl "bool" relations nil)
(ordered_set_order const-decl "bool" well_ordering nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil))
nil))
(ordered_set_union_TCC1 0
(ordered_set_union_TCC1-1 nil 3315836233
("" (skolem-typepred)
((""
(expand* "well_ordered?" "strict_total_order?" "strict_order?")
(("" (split)
(("1" (expand "irreflexive?")
(("1" (skosimp* t)
(("1" (typepred "ord!1`2")
(("1"
(expand* "well_ordered?" "strict_total_order?"
"strict_order?" "irreflexive?")
(("1" (flatten) (("1" (inst - "x!1") nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (expand "transitive?")
(("2" (skosimp* t)
(("2"
(expand* "chain?" "restrict" "total_order?"
"dichotomous?")
(("2" (flatten)
(("2" (inst - "ord!1" "ord!2")
(("2" (split)
(("1" (expand "ordered_set_order" -1)
(("1" (flatten)
(("1" (expand* "subset?" "member")
(("1" (inst - "x!1")
(("1" (assert)
(("1"
(inst + "ord!2")
(("1"
(typepred "ord!2`2")
(("1"
(expand*
"well_ordered?"
"strict_total_order?"
"strict_order?"
"transitive?")
(("1"
(flatten)
(("1"
(inst - "x!1" "y!1" "z!1")
(("1"
(inst - "x!1" "y!1")
(("1" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "ordered_set_order" -1)
(("2" (flatten)
(("2" (expand* "subset?" "member")
(("2" (inst - "z!1")
(("2" (assert)
(("2"
(inst + "ord!1")
(("2"
(typepred "ord!1`2")
(("2"
(expand*
"well_ordered?"
"strict_total_order?"
"strict_order?"
"transitive?")
(("2"
(flatten)
(("2"
(inst - "x!1" "y!1" "z!1")
(("2"
(inst - "y!1" "z!1")
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "trichotomous?")
(("3" (skosimp* t)
(("3"
(expand* "chain?" "restrict" "total_order?"
"dichotomous?")
(("3" (flatten)
(("3" (inst - "S!1" "S!2")
(("3" (split)
(("1" (expand "ordered_set_order" -1)
(("1" (flatten)
(("1" (expand* "subset?" "member")
(("1" (inst - "x!1")
(("1" (assert)
(("1"
(typepred "S!2`2")
(("1"
(expand*
"well_ordered?"
"strict_total_order?"
"trichotomous?")
(("1"
(flatten)
(("1"
(inst - "x!1" "y!1")
(("1"
(inst + "S!2")
(("1"
(inst + "S!2")
(("1" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "ordered_set_order" -1)
(("2" (flatten)
(("2" (expand* "subset?" "member")
(("2" (inst - "y!1")
(("2" (assert)
(("2"
(typepred "S!1`2")
(("2"
(expand*
"well_ordered?"
"strict_total_order?"
"trichotomous?")
(("2"
(flatten)
(("2"
(inst - "x!1" "y!1")
(("2"
(inst + "S!1")
(("2"
(inst + "S!1")
(("2" (ground) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (expand "well_founded?")
(("4" (skosimp* t)
(("4" (typepred "S!1`2")
(("4" (expand* "well_ordered?" "well_founded?")
(("4" (flatten)
(("4" (inst - "{t: (S!1`1) | p!1(t)}")
(("1" (split)
(("1" (skolem-typepred)
(("1" (inst + "y!2")
(("1" (skosimp* t)
(("1"
(expand* "chain?" "restrict"
"total_order?" "dichotomous?")
(("1"
(flatten)
(("1"
(inst - "S!1" "ord!1")
(("1"
(split)
(("1"
(expand "ordered_set_order" -1)
(("1"
(flatten)
(("1"
(inst - "x!1" "y!2")
(("1"
(assert)
(("1"
(inst -10 "x!1")
nil
nil))
nil)
("2"
(inst - "x!1")
(("1"
(expand*
"restrict"
"upper_bound?")
(("1"
(inst - "y!2")
(("1"
(typepred "ord!1`2")
(("1"
(expand*
"well_ordered?"
"strict_total_order?"
"strict_order?"
"irreflexive?"
"transitive?")
(("1"
(flatten)
(("1"
(inst - "x!1")
(("1"
(inst
-
"x!1"
"y!2"
"x!1")
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand*
"difference"
"member")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "ordered_set_order" -1)
(("2"
(flatten)
(("2"
(expand* "subset?" "member")
(("2"
(inst - "x!1")
(("2"
(assert)
(("2"
(inst - "x!1" "y!2")
(("2"
(inst -10 "x!1")
(("2"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst + "y!1") nil nil))
nil)
("2" (skolem-typepred)
(("2" (inst + "S!1") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((strict_total_order? const-decl "bool" orders nil)
(strict_order? const-decl "bool" orders nil)
(well_founded? const-decl "bool" orders nil)
(p!1 skolem-const-decl "pred[({t | EXISTS (S: (C!1)): S`1(t)})]"
well_ordering nil)
(x!1 skolem-const-decl "(p!1)" well_ordering nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(ord!1 skolem-const-decl "(C!1)" well_ordering nil)
(difference const-decl "set" sets nil)
(y!1 skolem-const-decl "({t | EXISTS (S: (C!1)): S`1(t)})"
well_ordering nil)
(S!1 skolem-const-decl "(C!1)" well_ordering nil)
(C!1 skolem-const-decl "chain[ordered_set, ordered_set_order]"
well_ordering nil)
(trichotomous? const-decl "bool" orders nil)
(transitive? const-decl "bool" relations nil)
(restrict const-decl "R" restrict nil)
(dichotomous? const-decl "bool" orders nil)
(total_order? const-decl "bool" orders nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(irreflexive? const-decl "bool" relations nil)
(chain nonempty-type-eq-decl nil chain nil)
(chain? const-decl "bool" chain nil)
(ordered_set_order const-decl "bool" well_ordering nil)
(ordered_set type-eq-decl nil well_ordering nil)
(well_ordered? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil well_ordering nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
nil))
(chain_upper_bound 0
(chain_upper_bound-1 nil 3315837585
("" (skolem-typepred)
(("" (expand* "bounded_above?" "upper_bound?")
(("" (inst + "ordered_set_union(C!1)")
(("" (skolem!)
(("" (expand "ordered_set_order")
(("" (split)
(("1" (expand* "subset?" "member" "ordered_set_union")
(("1" (skosimp) (("1" (inst?) nil nil)) nil)) nil)
("2" (skolem!)
(("2" (prop)
(("1" (expand "ordered_set_union")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil)
("2"
(expand* "ordered_set_union" "chain?"
"total_order?" "dichotomous?" "restrict")
(("2" (skosimp)
(("2" (inst - "r!1" "ord!1")
(("2" (expand "ordered_set_order")
(("2" (prop)
(("1" (inst - "t!1" "r!2")
(("1" (assert) nil nil)) nil)
("2" (inst - "t!1" "r!2")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skolem-typepred)
(("3"
(expand* "restrict" "difference" "member"
"upper_bound?")
(("3" (skosimp :preds? t)
(("3"
(expand* "ordered_set_union" "chain?"
"total_order?" "dichotomous?" "restrict")
(("3" (skosimp*)
(("3" (inst - "S!2" "r!1")
(("3"
(expand* "ordered_set_order" "subset?"
"member")
(("3" (prop)
(("1"
(inst - "t!1")
(("1" (assert) nil nil))
nil)
("2"
(inst - "r!2")
(("2"
(assert)
(("2"
(inst - "t!1")
(("1"
(expand*
"restrict"
"upper_bound?")
(("1"
(inst - "r!2")
(("1"
(inst + "S!2")
(("1" (assert) nil nil))
nil))
nil))
nil)
("2"
(expand* "difference" "member")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((upper_bound? const-decl "bool" bounded_orders nil)
(bounded_above? const-decl "bool" bounded_orders nil)
(subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(total_order? const-decl "bool" orders 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)
(t!1 skolem-const-decl
"(difference(ordered_set_union(C!1)`1, r!1`1))" well_ordering nil)
(r!1 skolem-const-decl "(C!1)" well_ordering nil)
(S!2 skolem-const-decl "(C!1)" well_ordering nil)
(C!1 skolem-const-decl "chain[ordered_set, ordered_set_order]"
well_ordering nil)
(difference const-decl "set" sets nil)
(ordered_set_union const-decl "ordered_set" well_ordering nil)
(chain nonempty-type-eq-decl nil chain nil)
(chain? const-decl "bool" chain nil)
(ordered_set_order const-decl "bool" well_ordering nil)
(ordered_set type-eq-decl nil well_ordering nil)
(well_ordered? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(set type-eq-decl nil sets nil)
(T formal-type-decl nil well_ordering nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(well_ordering 0
(well_ordering-1 nil 3315837896
("" (lemma "chain_upper_bound")
(("" (forward-chain "zorn")
(("" (expand "bounded_above?")
(("" (skolem!)
(("" (expand* "fullset" "maximal?")
(("" (typepred "t!1`2")
(("" (case "full?(t!1`1)")
(("1" (expand* "full?" "member")
(("1"
(inst 2
"LAMBDA (t, r: T): IF t!1`1(t) AND t!1`1(r) THEN t!1`2(t, r) ELSE FALSE ENDIF")
(("1"
(expand* "well_ordered?" "strict_total_order?"
"strict_order?")
(("1" (prop)
(("1" (expand "irreflexive?")
(("1" (skolem!)
(("1" (prop)
(("1" (inst -5 "x!1") nil nil)) nil))
nil))
nil)
("2" (expand "transitive?")
(("2" (skosimp)
(("2" (prop)
(("2"
(inst - "x!1" "y!1" "z!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil)
("3" (expand "trichotomous?")
(("3" (skosimp)
(("3" (inst-cp - "y!1")
(("3"
(inst - "x!1")
(("3"
(inst - "x!1" "y!1")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("4" (expand "well_founded?")
(("4" (skosimp*)
(("4" (inst - "y!1")
(("4"
(inst - "{t: (t!1`1) | p!1(t)}")
(("4"
(split)
(("1"
(skolem-typepred)
(("1"
(inst + "y!2")
(("1"
(skolem-typepred)
(("1"
(prop)
(("1"
(inst - "x!1")
nil
nil))
nil))
nil))
nil))
nil)
("2" (inst + "y!1") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 3)
(("2" (expand* "full?" "member")
(("2" (skolem!)
(("2"
(inst +
"(add(x!1, t!1`1), LAMBDA (t, r: (add(x!1, t!1`1))): IF t = x!1 THEN FALSE ELSIF r = x!1 THEN TRUE ELSE t!1`2(t, r) ENDIF)")
(("1" (expand "ordered_set_order")
(("1" (prop)
(("1" (use "subset_add[T]") nil nil)
("2" (skolem!)
(("2"
(lift-if)
(("2" (ground) nil nil))
nil))
nil)
("3" (expand* "restrict" "upper_bound?")
(("3"
(skosimp* t)
(("3"
(expand* "add" "difference" "member")
(("3" (ground) nil nil))
nil))
nil))
nil)
("4" (replace -1 1)
(("4"
(beta)
(("4"
(expand* "add" "member")
nil
nil))
nil))
nil))
nil))
nil)
("2"
(expand* "well_ordered?"
"strict_total_order?" "strict_order?")
(("2" (prop)
(("1" (expand "irreflexive?")
(("1"
(skolem-typepred)
(("1"
(expand* "add" "member")
(("1"
(ground)
(("1" (inst - "x!2") nil nil))
nil))
nil))
nil))
nil)
("2" (expand "transitive?")
(("2"
(skosimp :preds? t)
(("2"
(expand* "add" "member")
(("2"
(ground)
(("2"
(inst - "x!2" "y!1" "z!1")
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "trichotomous?")
(("3"
(skosimp :preds? t)
(("3"
(expand* "add" "member")
(("3"
(ground)
(("3"
(inst - "x!2" "y!1")
(("3" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("4" (expand "well_founded?")
(("4"
(skosimp* t)
(("4"
(expand* "add" "member")
(("4"
(inst - "{t: (t!1`1) | p!1(t)}")
(("1"
(split)
(("1"
(split)
(("1"
(skolem-typepred)
(("1"
(inst + "y!2")
(("1"
(skolem-typepred)
(("1"
(expand*
"add"
"member")
(("1"
(ground)
(("1"
(inst - "x!2")
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(inst 2 "y!1")
(("2"
(skolem-typepred)
(("2"
(expand* "add" "member")
(("2"
(ground)
(("2"
(inst + "x!2")
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(split)
(("1"
(skolem-typepred)
(("1"
(inst + "y!2")
(("1"
(skolem-typepred)
(("1"
(expand*
"add"
"member")
(("1"
(ground)
(("1"
(inst - "x!2")
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst + "y!1") nil nil))
nil))
nil)
("2"
(skolem-typepred)
(("2"
(expand* "add" "member")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp :preds? t)
(("3" (expand* "add" "member")
(("3" (ground) nil nil)) nil))
nil)
("4" (skosimp :preds? t)
(("4" (expand* "add" "member")
(("4" (ground) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((zorn formula-decl nil zorn nil)
(T formal-type-decl nil well_ordering nil)
(set type-eq-decl nil sets nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(pred type-eq-decl nil defined_types nil)
(well_ordered? const-decl "bool" orders nil)
(ordered_set type-eq-decl nil well_ordering nil)
(ordered_set_order const-decl "bool" well_ordering nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(p!1 skolem-const-decl "pred[(add(x!1, t!1`1))]" well_ordering nil)
(y!1 skolem-const-decl "(add(x!1, t!1`1))" well_ordering nil)
(upper_bound? const-decl "bool" bounded_orders nil)
(restrict const-decl "R" restrict nil)
(difference const-decl "set" sets nil)
(subset_add formula-decl nil sets_lemmas nil)
(TRUE const-decl "bool" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
(x!1 skolem-const-decl "T" well_ordering nil)
(add const-decl "(nonempty?)" sets nil)
(nonempty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(strict_total_order? const-decl "bool" orders nil)
(strict_order? const-decl "bool" orders nil)
(well_founded? const-decl "bool" orders nil)
(y!1 skolem-const-decl "T" well_ordering nil)
(trichotomous? const-decl "bool" orders nil)
(t!1 skolem-const-decl "ordered_set" well_ordering nil)
(x!1 skolem-const-decl "T" well_ordering nil)
(y!1 skolem-const-decl "T" well_ordering nil)
(transitive? const-decl "bool" relations nil)
(irreflexive? const-decl "bool" relations nil)
(IF const-decl "[boolean, T, T -> T]" if_def nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(FALSE const-decl "bool" booleans nil)
(full? const-decl "bool" sets nil)
(fullset const-decl "set" sets nil)
(maximal? const-decl "bool" minmax_orders nil)
(bounded_above? const-decl "bool" bounded_orders nil)
(chain_upper_bound formula-decl nil well_ordering nil))
shostak)))
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.67Angebot
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
|
