Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: set_as_list_props.pvs Sprache: PVS

Original von: PVS^©

% Computable finite sets by Pierre Neron (Ecole Polytechnique)

set_as_list_props[T:TYPE] : THEORY
BEGIN

  IMPORTING set_as_list[T]

  strict_subset_card_lt : LEMMA FORALL (s1,s2 : finite_set) : strict_subset?(s1,s2) IMPLIES card(s1) < card(s2)

  x, y: VAR T

  l, l1, l2: VAR list[T]

  empty_l2s : LEMMA empty_sl?(l) IFF empty?(list2set(l))

  emptyset_l2s : LEMMA list2set(emptyset_sl) = emptyset

  nonempty_l2s : LEMMA nonempty_sl?(l) IFF nonempty?(list2set(l))

  subset_l2s : LEMMA subset_sl?(l1,l2) IFF subset?(list2set(l1),list2set(l2))

  remove_l2s : LEMMA list2set(remove_sl(x,l)) = remove(x,list2set(l))

  equal_l2s : LEMMA equal_sl(l1,l2) IFF list2set(l1) = list2set(l2)

  strict_subset_l2s : LEMMA strict_subset_sl?(l1,l2) IFF strict_subset?(list2set(l1),list2set(l2))

  union_l2s : LEMMA list2set(union_sl(l1,l2)) = union(list2set(l1),list2set(l2))

  intersection_l2s : LEMMA list2set(intersection_sl(l1,l2)) = intersection(list2set(l1),list2set(l2))

  disjoint_l2s : LEMMA disjoint_sl?(l1,l2) IFF disjoint?(list2set(l1),list2set(l2))

  difference_l2s : LEMMA list2set(difference_sl(l1,l2)) = difference(list2set(l1),list2set(l2))

  symmetric_difference_l2s : LEMMA
    list2set(symmetric_difference_sl(l1,l2)) = symmetric_difference(list2set(l1),list2set(l2))

  subset_sl_emptyset_sl: LEMMA subset_sl?(emptyset_sl, l)

  subset_sl_reflexive: LEMMA subset_sl?(l, l)

  subset_sl_transitive: LEMMA
    subset_sl?(l1, l) AND subset_sl?(l,l2) IMPLIES subset_sl?(l1,l2)

  subset_sl_preorder: LEMMA preorder?(subset_sl?[T])

  subset_sl_is_preorder: JUDGEMENT
    subset_sl?[T] HAS_TYPE (preorder?[list[T]])

  equal_sl_reflexive: LEMMA equal_sl(l,l)

  equal_sl_transitive: LEMMA equal_sl(l1,l) AND equal_sl(l,l2) => equal_sl(l1,l2)

  equal_sl_symmetric: LEMMA equal_sl(l1,l2) IFF equal_sl(l2,l1)

  strict_subset_sl_irreflexive: LEMMA NOT strict_subset_sl?(l, l)

  strict_subset_sl_transitive: LEMMA
    strict_subset_sl?(l1, l) AND strict_subset_sl?(l, l2) IMPLIES
     strict_subset_sl?(l1, l2)

  strict_subset_sl_strict_order: LEMMA strict_order?(strict_subset_sl?[T])

  strict_subset_sl_is_strict_order: JUDGEMENT
    strict_subset_sl?[T] HAS_TYPE (strict_order?[list[T]])

  strict_subset_sl_wf: LEMMA well_founded?(strict_subset_sl?)

  strict_subset_sl_is_wf : JUDGEMENT
    strict_subset_sl?[T] HAS_TYPE (well_founded?[list[T]])




END set_as_list_props

¤ Dauer der Verarbeitung: 0.0 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des 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.