| products/Sources/formale Sprachen/PVS/orders/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: bounded_order_props.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(bounded_order_props
(singleton_is_lub_set 0 (singleton_is_lub_set-1 nil 3330924431 ("" (skosimp) (("" (typepred "x!1") (("" (expand "lub_set?") (("" (expand "singleton?") (("" (expand "least_bounded_above?") (("" (skosimp) (("" (typepred "x!2") (("" (inst + "x!2") (("" (expand "least_upper_bound?") (("" (split) (("1" (expand "upper_bound?") (("1" (skosimp) (("1" (inst - "r!1") (("1" (assert) (("1" (typepred "<=") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (flatten) (("1" (expand "reflexive?") (("1" (inst - "r!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "upper_bound?") (("2" (inst - "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((singleton? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil bounded_order_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (reflexive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (<= formal-const-decl "(partial_order?[T])" bounded_order_props nil) (partial_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (upper_bound? const-decl "bool" bounded_orders nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (least_bounded_above? const-decl "bool" bounded_orders nil) (lub_set? const-decl "bool" bounded_order_props nil)) shostak)) (lub_TCC1 0 (lub_TCC1-1 nil 3330403776 ("" (inst + "LAMBDA (S:(lub_set?)):epsilon!(x:T):bounded_orders[T].least_upper_bound?(x,S,<=)") (("1" (skosimp) (("1" (typepred "S!1") (("1" (expand "lub_set?") (("1" (use "epsilon_ax[T]") (("1" (split -1) (("1" (propax) nil nil) ("2" (expand "least_bounded_above?") (("2" (propax) nil nil)) nil)) nil) ("2" (expand "least_bounded_above?") (("2" (skosimp) (("2" (inst + "t!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "S!1") (("2" (expand "lub_set?") (("2" (expand "least_bounded_above?") (("2" (skosimp) (("2" (inst + "t!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((least_bounded_above? const-decl "bool" bounded_orders nil) (epsilon_ax formula-decl nil epsilons nil) (NOT const-decl "[bool -> bool]" booleans nil) (epsilon const-decl "T" epsilons nil) (<= formal-const-decl "(partial_order?[T])" bounded_order_props nil) (partial_order? const-decl "bool" orders nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (lub_set? const-decl "bool" bounded_order_props 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 bounded_order_props nil)) shostak)) (lub_rew_TCC1 0 (lub_rew_TCC1-1 nil 3353512817 ("" (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) (set type-eq-decl nil sets nil) (lub_set? const-decl "bool" bounded_order_props nil) (T formal-type-decl nil bounded_order_props nil) (upper_bound? const-decl "bool" bounded_orders nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (least_bounded_above? const-decl "bool" bounded_orders nil)) nil)) (lub_rew 0 (lub_rew-1 nil 3353512818 ("" (skosimp) (("" (typepred "SA!1") (("" (typepred "lub(SA!1)") (("" (typepred "lub(<=)(SA!1)") (("" (expand "least_upper_bound?") (("" (flatten) (("" (typepred "<=") (("" (expand "partial_order?") (("" (flatten) (("" (inst - "lub(SA!1)") (("" (inst - "lub(<=)(SA!1)") (("" (split -4) (("1" (split -6) (("1" (expand "antisymmetric?") (("1" (inst - "lub(SA!1)" "lub(<=)(SA!1)") (("1" (assert) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((lub_set? const-decl "bool" bounded_order_props nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil bounded_order_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (lub const-decl "(LAMBDA (t): least_upper_bound?(t, S, <=))" bounded_orders nil) (least_bounded_above? const-decl "bool" bounded_orders nil) (antisymmetric? const-decl "bool" relations nil) (pred type-eq-decl nil defined_types nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (partial_order? const-decl "bool" orders nil) (<= formal-const-decl "(partial_order?[T])" bounded_order_props nil) (lub const-decl "{x | bounded_orders[T].least_upper_bound?(x, SA, <=)}" bounded_order_props nil)) shostak)) (lub_singleton 0 (lub_singleton-1 nil 3330924634 ("" (skosimp) (("" (typepred "lub(singleton(x!1))") (("" (expand "least_upper_bound?") (("" (flatten) (("" (inst - "x!1") (("" (expand "upper_bound?") (("" (inst - "x!1") (("1" (split -2) (("1" (typepred "<=") (("1" (expand "partial_order?") (("1" (flatten) (("1" (expand "antisymmetric?") (("1" (inst - "lub(singleton(x!1))" "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "r!1") (("2" (expand "singleton") (("2" (typepred "<=") (("2" (expand "partial_order?") (("2" (expand "preorder?") (("2" (flatten) (("2" (expand "reflexive?") (("2" (inst - "r!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "singleton") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (lub const-decl "{x | bounded_orders[T].least_upper_bound?(x, SA, <=)}" bounded_order_props nil) (<= formal-const-decl "(partial_order?[T])" bounded_order_props nil) (partial_order? const-decl "bool" orders nil) (lub_set? const-decl "bool" bounded_order_props nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil bounded_order_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (upper_bound? const-decl "bool" bounded_orders nil) (antisymmetric? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (reflexive? const-decl "bool" relations nil) (x!1 skolem-const-decl "T" bounded_order_props nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" bounded_order_props nil)) shostak)) (lub_lem 0 (lub_lem-1 nil 3330483947 ("" (skosimp) (("" (typepred "lub(SA!1)") (("" (case-replace "lub(SA!1)=x!1") (("1" (assert) nil nil) ("2" (assert) (("2" (name-replace "LUB" "lub(SA!1)") (("2" (lemma "unique_least_upper_bound[T]") (("2" (inst - "SA!1" "<=" "_" "_") (("2" (inst - "LUB" "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((lub const-decl "{x | bounded_orders[T].least_upper_bound?(x, SA, <=)}" bounded_order_props nil) (<= formal-const-decl "(partial_order?[T])" bounded_order_props nil) (partial_order? const-decl "bool" orders nil) (lub_set? const-decl "bool" bounded_order_props nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil bounded_order_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (unique_least_upper_bound formula-decl nil bounded_orders nil) (PRED type-eq-decl nil defined_types nil) (antisymmetric? const-decl "bool" relations nil) (= const-decl "[T, T -> boolean]" equalities nil)) shostak)) (above_lub 0 (above_lub-1 nil 3330751210 ("" (skosimp) (("" (typepred "lub(YA!1)") (("" (typepred "lub(XA!1)") (("" (expand "least_upper_bound?") (("" (flatten) (("" (inst -4 "lub(XA!1)") (("" (split -4) (("1" (propax) nil nil) ("2" (expand "upper_bound?") (("2" (skosimp) (("2" (typepred "r!1") (("2" (expand "above?") (("2" (inst -5 "r!1") (("2" (skosimp) (("2" (typepred "y!1") (("2" (inst -3 "y!1") (("2" (assert) (("2" (typepred "<=") (("2" (expand "partial_order?") (("2" (expand "preorder?") (("2" (flatten) (("2" (expand "transitive?") (("2" (inst - "r!1" "y!1" "lub(XA!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) ((lub const-decl "{x | bounded_orders[T].least_upper_bound?(x, SA, <=)}" bounded_order_props nil) (<= formal-const-decl "(partial_order?[T])" bounded_order_props nil) (partial_order? const-decl "bool" orders nil) (lub_set? const-decl "bool" bounded_order_props nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil bounded_order_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (upper_bound? const-decl "bool" bounded_orders nil) (transitive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (above? const-decl "bool" bounded_order_props nil)) shostak)) (singleton_is_glb_set 0 (singleton_is_glb_set-1 nil 3330924431 ("" (skosimp) (("" (typepred "x!1") (("" (expand "singleton?") (("" (skosimp) (("" (expand "glb_set?") (("" (expand "greatest_bounded_below?") (("" (inst + "x!2") (("" (expand "greatest_lower_bound?") (("" (split) (("1" (expand "lower_bound?") (("1" (skosimp) (("1" (typepred "<=") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (flatten) (("1" (expand "reflexive?") (("1" (inst - "x!2") (("1" (typepred "r!1") (("1" (inst - "r!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "lower_bound?") (("2" (inst - "x!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((singleton? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil bounded_order_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (greatest_bounded_below? const-decl "bool" bounded_orders nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (lower_bound? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (partial_order? const-decl "bool" orders nil) (<= formal-const-decl "(partial_order?[T])" bounded_order_props nil) (preorder? const-decl "bool" orders nil) (reflexive? const-decl "bool" relations nil) (glb_set? const-decl "bool" bounded_order_props nil)) shostak)) (glb_TCC1 0 (glb_TCC1-1 nil 3330403776 ("" (inst + "LAMBDA (S:(glb_set?)):epsilon!(x:T):bounded_orders[T].greatest_lower_bound?(x,S (("1" (skosimp) (("1" (typepred "S!1") (("1" (use "epsilon_ax[T]") (("1" (split -1) (("1" (propax) nil nil) ("2" (expand "glb_set?") (("2" (expand "greatest_bounded_below?") (("2" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "glb_set?") (("2" (expand "greatest_bounded_below?") (("2" (skosimp) (("2" (inst + "t!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "S!1") (("2" (expand "glb_set?") (("2" (expand "greatest_bounded_below?") (("2" (skosimp) (("2" (inst + "t!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((epsilon_ax formula-decl nil epsilons nil) (greatest_bounded_below? const-decl "bool" bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (epsilon const-decl "T" epsilons nil) (<= formal-const-decl "(partial_order?[T])" bounded_order_props nil) (partial_order? const-decl "bool" orders nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (glb_set? const-decl "bool" bounded_order_props 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 bounded_order_props nil)) shostak)) (glb_rew_TCC1 0 (glb_rew_TCC1-1 nil 3353512817 ("" (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) (set type-eq-decl nil sets nil) (glb_set? const-decl "bool" bounded_order_props nil) (T formal-type-decl nil bounded_order_props nil) (lower_bound? const-decl "bool" bounded_orders nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (greatest_bounded_below? const-decl "bool" bounded_orders nil)) nil)) (glb_rew 0 (glb_rew-1 nil 3353512945 ("" (skosimp) (("" (typepred "SB!1") (("" (typepred "glb(<=)(SB!1)") (("" (typepred "glb(SB!1)") (("" (typepred "<=") (("" (expand "partial_order?") (("" (expand "greatest_lower_bound?") (("" (flatten) (("" (inst - "glb(<=)(SB!1)") (("" (inst - "glb(SB!1)") (("" (split -4) (("1" (split -6) (("1" (expand "antisymmetric?") (("1" (inst - "glb(SB!1)" "glb(<=)(SB!1)") (("1" (assert) nil nil)) nil)) nil) ("2" (propax) nil nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((glb_set? const-decl "bool" bounded_order_props nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil bounded_order_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (glb const-decl "{x | bounded_orders[T].greatest_lower_bound?(x, SB, <=)}" bounded_order_props nil) (antisymmetric? const-decl "bool" relations nil) (pred type-eq-decl nil defined_types nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (greatest_bounded_below? const-decl "bool" bounded_orders nil) (glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))" bounded_orders nil) (partial_order? const-decl "bool" orders nil) (<= formal-const-decl "(partial_order?[T])" bounded_order_props nil)) shostak)) (glb_singleton 0 (glb_singleton-1 nil 3330924838 ("" (skosimp) (("" (typepred "glb(singleton(x!1))") (("" (expand "greatest_lower_bound?") (("" (flatten) (("" (expand "lower_bound?") (("" (case "singleton(x!1)(x!1)") (("1" (inst - "x!1") (("1" (inst - "x!1") (("1" (split -3) (("1" (typepred "<=") (("1" (expand "partial_order?") (("1" (flatten) (("1" (expand "antisymmetric?") (("1" (inst - "glb(singleton(x!1))" "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (typepred "r!1") (("2" (expand "singleton") (("2" (typepred "<=") (("2" (expand "partial_order?") (("2" (expand "preorder?") (("2" (flatten) (("2" (expand "reflexive?") (("2" (inst - "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "singleton") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (glb const-decl "{x | bounded_orders[T].greatest_lower_bound?(x, SB, <=)}" bounded_order_props nil) (<= formal-const-decl "(partial_order?[T])" bounded_order_props nil) (partial_order? const-decl "bool" orders nil) (glb_set? const-decl "bool" bounded_order_props nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil bounded_order_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (reflexive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (antisymmetric? const-decl "bool" relations nil) (x!1 skolem-const-decl "T" bounded_order_props nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" bounded_order_props nil) (lower_bound? const-decl "bool" bounded_orders nil)) shostak)) (glb_lem 0 (glb_lem-1 nil 3330484050 ("" (skosimp) (("" (typepred "glb(SB!1)") (("" (case-replace "glb(SB!1) = x!1") (("1" (assert) nil nil) ("2" (assert) (("2" (lemma "unique_greatest_lower_bound" ("<=" "<=" "S" "SB!1" "t" "glb(SB!1)" "r" "x!1")) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((glb const-decl "{x | bounded_orders[T].greatest_lower_bound?(x, SB, <=)}" bounded_order_props nil) (<= formal-const-decl "(partial_order?[T])" bounded_order_props nil) (partial_order? const-decl "bool" orders nil) (glb_set? const-decl "bool" bounded_order_props nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil bounded_order_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (unique_greatest_lower_bound formula-decl nil bounded_orders nil) (PRED type-eq-decl nil defined_types nil) (antisymmetric? const-decl "bool" relations nil) (= const-decl "[T, T -> boolean]" equalities nil)) shostak)) (below_glb 0 (below_glb-1 nil 3330750355 ("" (skosimp) (("" (typepred "glb(XB!1)") (("" (typepred "glb(YB!1)") (("" (expand "greatest_lower_bound?") (("" (flatten) (("" (inst - "glb(XB!1)") (("" (split -2) (("1" (propax) nil nil) ("2" (hide 2) (("2" (expand "lower_bound?") (("2" (skosimp) (("2" (typepred "r!1") (("2" (expand "below?") (("2" (inst -5 "r!1") (("2" (skosimp) (("2" (inst -3 "y!1") (("2" (typepred "<=") (("2" (expand "partial_order?") (("2" (expand "preorder?") (("2" (flatten) (("2" (expand "transitive?") (("2" (inst - "glb(XB!1)" "y!1" "r!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) ((glb const-decl "{x | bounded_orders[T].greatest_lower_bound?(x, SB, <=)}" bounded_order_props nil) (<= formal-const-decl "(partial_order?[T])" bounded_order_props nil) (partial_order? const-decl "bool" orders nil) (glb_set? const-decl "bool" bounded_order_props nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil bounded_order_props nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (below? const-decl "bool" bounded_order_props nil) (preorder? const-decl "bool" orders nil) (transitive? const-decl "bool" relations nil) (lower_bound? const-decl "bool" bounded_orders nil)) shostak))) ¤ Dauer der Verarbeitung: 0.12 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 |
