| products/sources/formale Sprachen/PVS/Sturm/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: product_orders.pvs Sprache: IsabelleOriginal von: PVS© |
|
||||||
|
(total_lattices
(singleton_has_greatest 0 (singleton_has_greatest-1 nil 3316873516 ("" (skolem!) (("" (use "non_empty_finite_has_greatest") nil nil)) nil) ((<= formal-const-decl "(total_order?[T])" total_lattices nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[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) (boolean nonempty-type-decl nil booleans nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" total_lattices nil) (non_empty_finite_has_greatest formula-decl nil minmax_orders nil) (T formal-type-decl nil total_lattices nil)) nil)) (union_preserves_has_greatest 0 (union_preserves_has_greatest-1 nil 3316872843 ("" (skolem-typepred) (("" (expand* "has_greatest?" "greatest?" "upper_bound?" "union" "member") (("" (skosimp*) (("" (case "t!1 <= t!2") (("1" (inst + "t!2") (("1" (assert) (("1" (skolem-typepred) (("1" (expand* "union" "member") (("1" (split) (("1" (inst - "r!1") (("1" (typepred "<=") (("1" (expand* "total_order?" "partial_order?" "preorder?" "transitive?") (("1" (flatten) (("1" (inst - "r!1" "t!1" "t!2") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst -6 "r!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "<=") (("2" (expand* "total_order?" "dichotomous?" "partial_order?" "preorder?" "transitive?") (("2" (flatten) (("2" (inst - "t!1" "t!2") (("2" (inst + "t!1") (("2" (assert) (("2" (skolem-typepred) (("2" (expand* "union" "member") (("2" (split) (("1" (inst - "r!1") nil nil) ("2" (inst -9 "r!1") (("2" (inst - "r!1" "t!2" "t!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((greatest? const-decl "bool" minmax_orders nil) (union const-decl "set" sets nil) (member const-decl "bool" sets nil) (upper_bound? const-decl "bool" bounded_orders nil) (G1!1 skolem-const-decl "(LAMBDA (S: set[T]): has_greatest?(S, <=))" total_lattices nil) (G2!1 skolem-const-decl "(LAMBDA (S: set[T]): has_greatest?(S, <=))" total_lattices nil) (r!1 skolem-const-decl "(union[T](G1!1, G2!1))" total_lattices nil) (partial_order? const-decl "bool" orders nil) (transitive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (dichotomous? const-decl "bool" orders nil) (r!1 skolem-const-decl "(union[T](G1!1, G2!1))" total_lattices nil) (<= formal-const-decl "(total_order?[T])" total_lattices nil) (total_order? const-decl "bool" orders nil) (has_greatest? const-decl "bool" minmax_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil total_lattices nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (add_preserves_has_greatest 0 (add_preserves_has_greatest-1 nil 3316872843 ("" (skolem!) (("" (rewrite "add_as_union[T]") (("" (assert) nil nil)) nil)) nil) ((add_as_union formula-decl nil sets_lemmas nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (has_greatest? const-decl "bool" minmax_orders nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" total_lattices nil) (T formal-type-decl nil total_lattices nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" total_lattices nil) (singleton_has_greatest application-judgement "(LAMBDA (S: set[T]): has_greatest?(S, <=))" total_lattices nil) (nonempty_union2 application-judgement "(nonempty?)" total_lattices nil) (union_preserves_has_greatest application-judgement "(LAMBDA (S: set[T]): has_greatest?(S, <=))" total_lattices nil)) nil)) (greatest_singleton 0 (greatest_singleton-1 nil 3316873630 ("" (skolem!) (("" (rewrite "greatest_def") (("" (grind) (("" (typepred "<=") (("" (expand* "total_order?" "partial_order?" "preorder?" "reflexive?") (("" (flatten) (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((singleton_has_greatest application-judgement "(LAMBDA (S: set[T]): has_greatest?(S, <=))" total_lattices nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" total_lattices nil) (greatest_def formula-decl nil minmax_orders nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (antisymmetric? const-decl "bool" relations nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" total_lattices nil) (set type-eq-decl nil sets nil) (has_greatest? const-decl "bool" minmax_orders nil) (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (T formal-type-decl nil total_lattices nil) (preorder? const-decl "bool" orders nil) (reflexive? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (upper_bound? const-decl "bool" bounded_orders nil) (greatest? const-decl "bool" minmax_orders nil)) shostak)) (greatest_union 0 (greatest_union-1 nil 3316873738 ("" (skolem!) (("" (lift-if) (("" (ground) (("1" (rewrite "greatest_def") (("1" (typepred "greatest(<=)(G2!1)") (("1" (typepred "greatest(<=)(G1!1)") (("1" (typepred "<=") (("1" (grind :if-match nil) (("1" (inst -7 "r!1") (("1" (inst - "r!1" "greatest(<=)(G1!1)" "greatest(<=)(G2!1)") (("1" (assert) nil nil)) nil)) nil) ("2" (inst -9 "r!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "<=") (("2" (expand* "total_order?" "dichotomous?") (("2" (flatten) (("2" (inst - "greatest(<=)(G1!1)" "greatest(<=)(G2!1)") (("2" (assert) (("2" (typepred "greatest(<=)(G2!1)") (("2" (typepred "greatest(<=)(G1!1)") (("2" (rewrite "greatest_def") (("2" (grind :if-match nil) (("1" (inst - "r!1") nil nil) ("2" (inst -5 "r!1") (("2" (inst - "r!1" "greatest(<=)(G2!1)" "greatest(<=)(G1!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((greatest_def formula-decl nil minmax_orders nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (antisymmetric? const-decl "bool" relations nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" total_lattices nil) (set type-eq-decl nil sets nil) (has_greatest? const-decl "bool" minmax_orders nil) (greatest? const-decl "bool" minmax_orders nil) (greatest const-decl "{t: (S) | greatest?(t, S, <=)}" minmax_orders nil) (union const-decl "set" sets nil) (T formal-type-decl nil total_lattices nil) (member const-decl "bool" sets nil) (upper_bound? const-decl "bool" bounded_orders nil) (dichotomous? const-decl "bool" orders nil) (partial_order? const-decl "bool" orders nil) (preorder? const-decl "bool" orders nil) (transitive? const-decl "bool" relations nil) (reflexive? const-decl "bool" relations nil) (NOT const-decl "[bool -> bool]" booleans nil) (union_preserves_has_greatest application-judgement "(LAMBDA (S: set[T]): has_greatest?(S, <=))" total_lattices nil)) shostak)) (greatest_add 0 (greatest_add-1 nil 3316873976 ("" (skolem!) (("" (rewrite "add_as_union[T]") (("" (use "greatest_union") (("" (rewrite "greatest_singleton") nil nil)) nil)) nil)) nil) ((add_as_union formula-decl nil sets_lemmas nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (has_greatest? const-decl "bool" minmax_orders nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" total_lattices nil) (T formal-type-decl nil total_lattices nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" total_lattices nil) (singleton_has_greatest application-judgement "(LAMBDA (S: set[T]): has_greatest?(S, <=))" total_lattices nil) (nonempty_union2 application-judgement "(nonempty?)" total_lattices nil) (union_preserves_has_greatest application-judgement "(LAMBDA (S: set[T]): has_greatest?(S, <=))" total_lattices nil) (greatest_singleton formula-decl nil total_lattices nil) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (greatest_union formula-decl nil total_lattices nil)) shostak)) (singleton_has_least 0 (singleton_has_least-1 nil 3316873516 ("" (skolem!) (("" (use "non_empty_finite_has_least") nil nil)) nil) ((<= formal-const-decl "(total_order?[T])" total_lattices nil) (total_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (NOT const-decl "[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) (boolean nonempty-type-decl nil booleans nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" total_lattices nil) (singleton_has_greatest application-judgement "(LAMBDA (S: set[T]): has_greatest?(S, <=))" total_lattices nil) (non_empty_finite_has_least formula-decl nil minmax_orders nil) (T formal-type-decl nil total_lattices nil)) nil)) (union_preserves_has_least 0 (union_preserves_has_least-1 nil 3316872843 ("" (skolem-typepred) (("" (expand* "has_least?" "least?" "lower_bound?" "union" "member") (("" (skosimp*) (("" (case "t!1 <= t!2") (("1" (inst + "t!1") (("1" (assert) (("1" (skolem-typepred) (("1" (expand* "union" "member") (("1" (split) (("1" (inst - "r!1") nil nil) ("2" (inst -6 "r!1") (("2" (typepred "<=") (("2" (expand* "total_order?" "partial_order?" "preorder?" "transitive?") (("2" (flatten) (("2" (inst - "t!1" "t!2" "r!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "<=") (("2" (expand* "total_order?" "dichotomous?" "partial_order?" "preorder?" "transitive?") (("2" (flatten) (("2" (inst - "t!1" "t!2") (("2" (inst + "t!2") (("2" (assert) (("2" (skolem-typepred) (("2" (expand* "union" "member") (("2" (split) (("1" (inst - "r!1") (("1" (inst - "t!2" "t!1" "r!1") (("1" (assert) nil nil)) nil)) nil) ("2" (inst -9 "r!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((least? const-decl "bool" minmax_orders nil) (union const-decl "set" sets nil) (member const-decl "bool" sets nil) (lower_bound? const-decl "bool" bounded_orders nil) (partial_order? const-decl "bool" orders nil) (transitive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (L1!1 skolem-const-decl "(LAMBDA (S: set[T]): has_least?(S, <=))" total_lattices nil) (L2!1 skolem-const-decl "(LAMBDA (S: set[T]): has_least?(S, <=))" total_lattices nil) (r!1 skolem-const-decl "(union[T](L1!1, L2!1))" total_lattices nil) (dichotomous? const-decl "bool" orders nil) (r!1 skolem-const-decl "(union[T](L1!1, L2!1))" total_lattices nil) (<= formal-const-decl "(total_order?[T])" total_lattices nil) (total_order? const-decl "bool" orders nil) (has_least? const-decl "bool" minmax_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil total_lattices nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (add_preserves_has_least 0 (add_preserves_has_least-1 nil 3316872843 ("" (skolem!) (("" (rewrite "add_as_union[T]") (("" (assert) nil nil)) nil)) nil) ((add_as_union formula-decl nil sets_lemmas nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (has_least? const-decl "bool" minmax_orders nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" total_lattices nil) (T formal-type-decl nil total_lattices nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" total_lattices nil) (singleton_has_greatest application-judgement "(LAMBDA (S: set[T]): has_greatest?(S, <=))" total_lattices nil) (singleton_has_least application-judgement "(LAMBDA (S: set[T]): has_least?(S, <=))" total_lattices nil) (nonempty_union2 application-judgement "(nonempty?)" total_lattices nil) (union_preserves_has_least application-judgement "(LAMBDA (S: set[T]): has_least?(S, <=))" total_lattices nil)) nil)) (least_singleton 0 (least_singleton-1 nil 3316874553 ("" (skolem!) (("" (rewrite "least_def") (("" (grind) (("" (typepred "<=") (("" (expand* "total_order?" "partial_order?" "preorder?" "reflexive?") (("" (flatten) (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((singleton_has_least application-judgement "(LAMBDA (S: set[T]): has_least?(S, <=))" total_lattices nil) (singleton_has_greatest application-judgement "(LAMBDA (S: set[T]): has_greatest?(S, <=))" total_lattices nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" total_lattices nil) (least_def formula-decl nil minmax_orders nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (antisymmetric? const-decl "bool" relations nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" total_lattices nil) (set type-eq-decl nil sets nil) (has_least? const-decl "bool" minmax_orders nil) (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (T formal-type-decl nil total_lattices nil) (preorder? const-decl "bool" orders nil) (reflexive? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (lower_bound? const-decl "bool" bounded_orders nil) (least? const-decl "bool" minmax_orders nil)) shostak)) (least_union 0 (least_union-1 nil 3316874582 ("" (skolem!) (("" (lift-if) (("" (ground) (("1" (rewrite "least_def") (("1" (typepred "least(<=)(L2!1)") (("1" (typepred "least(<=)(L1!1)") (("1" (typepred "<=") (("1" (grind :if-match nil) (("1" (inst -7 "r!1") nil nil) ("2" (inst -9 "r!1") (("2" (inst - "least(<=)(L1!1)" "least(<=)(L2!1)" "r!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "<=") (("2" (expand* "total_order?" "dichotomous?") (("2" (flatten) (("2" (inst - "least(<=)(L1!1)" "least(<=)(L2!1)") (("2" (assert) (("2" (typepred "least(<=)(L2!1)") (("2" (typepred "least(<=)(L1!1)") (("2" (rewrite "least_def") (("2" (grind :if-match nil) (("1" (inst - "r!1") (("1" (inst - "least(<=)(L2!1)" "least(<=)(L1!1)" "r!1") (("1" (assert) nil nil)) nil)) nil) ("2" (inst -5 "r!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((least_def formula-decl nil minmax_orders nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (antisymmetric? const-decl "bool" relations nil) (pred type-eq-decl nil defined_types nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" total_lattices nil) (set type-eq-decl nil sets nil) (has_least? const-decl "bool" minmax_orders nil) (least? const-decl "bool" minmax_orders nil) (least const-decl "{t: (S) | least?(t, S, <=)}" minmax_orders nil) (union const-decl "set" sets nil) (T formal-type-decl nil total_lattices nil) (member const-decl "bool" sets nil) (lower_bound? const-decl "bool" bounded_orders nil) (dichotomous? const-decl "bool" orders nil) (partial_order? const-decl "bool" orders nil) (preorder? const-decl "bool" orders nil) (transitive? const-decl "bool" relations nil) (reflexive? const-decl "bool" relations nil) (NOT const-decl "[bool -> bool]" booleans nil) (union_preserves_has_least application-judgement "(LAMBDA (S: set[T]): has_least?(S, <=))" total_lattices nil)) shostak)) (least_add 0 (least_add-1 nil 3316874740 ("" (skolem!) (("" (rewrite "add_as_union[T]") (("" (use "least_union") (("" (rewrite "least_singleton") nil nil)) nil)) nil)) nil) ((add_as_union formula-decl nil sets_lemmas nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (has_least? const-decl "bool" minmax_orders nil) (total_order? const-decl "bool" orders nil) (<= formal-const-decl "(total_order?[T])" total_lattices nil) (T formal-type-decl nil total_lattices nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" total_lattices nil) (singleton_has_greatest application-judgement "(LAMBDA (S: set[T]): has_greatest?(S, <=))" total_lattices nil) (singleton_has_least application-judgement "(LAMBDA (S: set[T]): has_least?(S, <=))" total_lattices nil) (nonempty_union2 application-judgement "(nonempty?)" total_lattices nil) (union_preserves_has_least application-judgement "(LAMBDA (S: set[T]): has_least?(S, <=))" total_lattices nil) (least_singleton formula-decl nil total_lattices nil) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (least_union formula-decl nil total_lattices nil)) shostak))) ¤ Dauer der Verarbeitung: 0.47 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
