Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: finite_bags_minmax.prf Sprache: Lisp

Original von: PVS^©

(sets_complete_lattices
(subset_equals_pointwise_implies 0
  (subset_equals_pointwise_implies-1 nil 3318704900
   ("" (expand* "subset?" "member" "pointwise") nil nil)
   ((pointwise const-decl "bool" pointwise_orders nil)
    (member const-decl "bool" sets nil)
    (subset? const-decl "bool" sets nil))
   shostak))
(subset_is_a_complete_lattice 0
  (subset_is_a_complete_lattice-1 nil 3318704881
   ("" (rewrite "subset_equals_pointwise_implies")
    (("" (rewrite "pointwise_preserves_complete_lattices") nil nil))
    nil)
   ((bool nonempty-type-eq-decl nil booleans nil)
    (boolean nonempty-type-decl nil booleans nil)
    (T formal-type-decl nil sets_complete_lattices nil)
    (IMPLIES const-decl "[bool, bool -> bool]" booleans nil)
    (complete_lattice? const-decl "bool" bounded_orders nil)
    (pred type-eq-decl nil defined_types nil)
    (pointwise_preserves_complete_lattices judgement-tcc nil
     pointwise_orders nil)
    (pointwise_preserves_reflexive application-judgement
     "(reflexive?[[D -> R]])" sets_complete_lattices nil)
    (pointwise_preserves_transitive application-judgement
     "(transitive?[[D -> R]])" sets_complete_lattices nil)
    (pointwise_preserves_preorder application-judgement
     "(preorder?[[D -> R]])" sets_complete_lattices nil)
    (pointwise_preserves_antisymmetric application-judgement
     "(antisymmetric?[[D -> R]])" sets_complete_lattices nil)
    (pointwise_preserves_partial_order application-judgement
     "(partial_order?[[D -> R]])" sets_complete_lattices nil)
    (pointwise_preserves_lower_semilattices application-judgement
     "(lower_semilattice?[[D -> R]])" sets_complete_lattices nil)
    (pointwise_preserves_complete_lower_semilattices
     application-judgement "(complete_lower_semilattice?[[D -> R]])"
     sets_complete_lattices nil)
    (pointwise_preserves_upper_semilattices application-judgement
     "(upper_semilattice?[[D -> R]])" sets_complete_lattices nil)
    (pointwise_preserves_lattices application-judgement
     "(lattice?[[D -> R]])" sets_complete_lattices nil)
    (pointwise_preserves_complete_upper_semilattices
     application-judgement "(complete_upper_semilattice?[[D -> R]])"
     sets_complete_lattices nil)
    (pointwise_preserves_complete_lattices application-judgement
     "(complete_lattice?[[T -> bool]])" sets_complete_lattices nil)
    (implies_is_total_order name-judgement "(total_order?[bool])"
     booleans_are_finite nil)
    (subset_equals_pointwise_implies formula-decl nil
     sets_complete_lattices nil))
   nil)))

¤ Dauer der Verarbeitung: 0.19 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

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.