|
% 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
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.1Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Entwicklung einer Software für die statische Quellcodeanalyse
|
