Nuprl Definition : set-sig
set-sig{i:l}(Item) ==
"set":{s:Type| valueall-type(Item) ⇒ valueall-type(s)}
"member":Item ─→ self."set" ─→ 𝔹
"empty":{s:self."set"| ∀x:Item. (¬↑(self."member" x s))}
"isEmpty":{f:self."set" ─→ 𝔹| ∀s:self."set". (↑(f s) ⇐⇒ ∀x:Item. (¬↑(self."member" x s)))}
"singleton":{f:Item ─→ self."set"| ∀x,y:Item. (↑(self."member" x (f y)) ⇐⇒ x = y ∈ Item)}
"add":{f:Item ─→ self."set" ─→ self."set"|
∀s:self."set". ∀x,y:Item. (↑(self."member" x (f y s)) ⇐⇒ (x = y ∈ Item) ∨ (↑(self."member" x s)))}
"union":{f:self."set" ─→ self."set" ─→ self."set"|
∀s1,s2:self."set". ∀x:Item.
(↑(self."member" x (f s1 s2)) ⇐⇒ (↑(self."member" x s1)) ∨ (↑(self."member" x s2)))}
"remove":{f:Item ─→ self."set" ─→ self."set"|
∀s:self."set". ∀x,y:Item. (↑(self."member" x (f y s)) ⇐⇒ (¬(x = y ∈ Item)) ∧ (↑(self."member" x s)))}
Definitions occuring in Statement :
valueall-type: valueall-type(T),
assert: ↑b,
bool: 𝔹,
top: Top,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
not: ¬A,
implies: P ⇒ Q,
or: P ∨ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ─→ B[x],
token: "$token",
universe: Type,
equal: s = t ∈ T,
record-select: r.x,
record+: record+,
record: record(x.T[x])
FDL editor aliases :
set-sig
set-sig\{i:l\}(Item) ==
"set":\{s:Type| valueall-type(Item) {}\mRightarrow{} valueall-type(s)\}
"member":Item {}\mrightarrow{} self."set" {}\mrightarrow{} \mBbbB{}
"empty":\{s:self."set"| \mforall{}x:Item. (\mneg{}\muparrow{}(self."member" x s))\}
"isEmpty":\{f:self."set" {}\mrightarrow{} \mBbbB{}| \mforall{}s:self."set". (\muparrow{}(f s) \mLeftarrow{}{}\mRightarrow{} \mforall{}x:Item. (\mneg{}\muparrow{}(self."member" x s)))\}
"singleton":\{f:Item {}\mrightarrow{} self."set"| \mforall{}x,y:Item. (\muparrow{}(self."member" x (f y)) \mLeftarrow{}{}\mRightarrow{} x = y)\}
"add":\{f:Item {}\mrightarrow{} self."set" {}\mrightarrow{} self."set"|
\mforall{}s:self."set". \mforall{}x,y:Item.
(\muparrow{}(self."member" x (f y s)) \mLeftarrow{}{}\mRightarrow{} (x = y) \mvee{} (\muparrow{}(self."member" x s)))\}
"union":\{f:self."set" {}\mrightarrow{} self."set" {}\mrightarrow{} self."set"|
\mforall{}s1,s2:self."set". \mforall{}x:Item.
(\muparrow{}(self."member" x (f s1 s2)) \mLeftarrow{}{}\mRightarrow{} (\muparrow{}(self."member" x s1)) \mvee{} (\muparrow{}(self."member" x s2)))\}
"remove":\{f:Item {}\mrightarrow{} self."set" {}\mrightarrow{} self."set"|
\mforall{}s:self."set". \mforall{}x,y:Item.
(\muparrow{}(self."member" x (f y s)) \mLeftarrow{}{}\mRightarrow{} (\mneg{}(x = y)) \mwedge{} (\muparrow{}(self."member" x s)))\}
Date html generated:
2015_07_17-AM-08_21_02
Last ObjectModification:
2013_04_24-AM-01_29_51
Home
Index