Nuprl Lemma : mk-set_wf
∀[Item:Type]. ∀[set:{s:Type| valueall-type(Item) 
⇒ valueall-type(s)} ]. ∀[member:Item ⟶ set ⟶ 𝔹].
∀[empty:{s:set| ∀x:Item. (¬↑(member x s))} ]. ∀[isEmpty:{f:set ⟶ 𝔹| ∀s:set. (↑(f s) 
⇐⇒ ∀x:Item. (¬↑(member x s)))} ].
∀[singleton:{f:Item ⟶ set| ∀x,y:Item.  (↑(member x (f y)) 
⇐⇒ x = y ∈ Item)} ]. ∀[add:{f:Item ⟶ set ⟶ set| 
                                                                                       ∀s:set. ∀x,y:Item.
                                                                                         (↑(member x (f y s))
                                                                                         
⇐⇒ (x = y ∈ Item)
                                                                                             ∨ (↑(member x s)))} ].
∀[union:{f:set ⟶ set ⟶ set| ∀s1,s2:set. ∀x:Item.  (↑(member x (f s1 s2)) 
⇐⇒ (↑(member x s1)) ∨ (↑(member x s2)))} ].
∀[remove:{f:Item ⟶ set ⟶ set| ∀s:set. ∀x,y:Item.  (↑(member x (f y s)) 
⇐⇒ (¬(x = y ∈ Item)) ∧ (↑(member x s)))} ].
  (mk-set(Item;set;member;empty;isEmpty;singleton;add;union;remove) ∈ set-sig{i:l}(Item))
Proof
Definitions occuring in Statement : 
mk-set: mk-set(Item;set;member;empty;isEmpty;singleton;add;union;remove)
, 
set-sig: set-sig{i:l}(Item)
, 
valueall-type: valueall-type(T)
, 
assert: ↑b
, 
bool: 𝔹
, 
uall: ∀[x:A]. B[x]
, 
all: ∀x:A. B[x]
, 
iff: P 
⇐⇒ Q
, 
not: ¬A
, 
implies: P 
⇒ Q
, 
or: P ∨ Q
, 
and: P ∧ Q
, 
member: t ∈ T
, 
set: {x:A| B[x]} 
, 
apply: f a
, 
function: x:A ⟶ B[x]
, 
universe: Type
, 
equal: s = t ∈ T
Definitions unfolded in proof : 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
mk-set: mk-set(Item;set;member;empty;isEmpty;singleton;add;union;remove)
, 
set-sig: set-sig{i:l}(Item)
, 
record+: record+, 
record-update: r[x := v]
, 
record: record(x.T[x])
, 
top: Top
, 
all: ∀x:A. B[x]
, 
implies: P 
⇒ Q
, 
bool: 𝔹
, 
unit: Unit
, 
it: ⋅
, 
btrue: tt
, 
uiff: uiff(P;Q)
, 
and: P ∧ Q
, 
uimplies: b supposing a
, 
ifthenelse: if b then t else f fi 
, 
sq_type: SQType(T)
, 
guard: {T}
, 
record-select: r.x
, 
eq_atom: x =a y
, 
bfalse: ff
, 
iff: P 
⇐⇒ Q
, 
not: ¬A
, 
prop: ℙ
, 
rev_implies: P 
⇐ Q
, 
so_lambda: λ2x.t[x]
, 
so_apply: x[s]
, 
or: P ∨ Q
Latex:
\mforall{}[Item:Type].  \mforall{}[set:\{s:Type|  valueall-type(Item)  {}\mRightarrow{}  valueall-type(s)\}  ].  \mforall{}[member:Item  {}\mrightarrow{}  set  {}\mrightarrow{}  \mBbbB{}].
\mforall{}[empty:\{s:set|  \mforall{}x:Item.  (\mneg{}\muparrow{}(member  x  s))\}  ].  \mforall{}[isEmpty:\{f:set  {}\mrightarrow{}  \mBbbB{}| 
                                                                                                                \mforall{}s:set
                                                                                                                    (\muparrow{}(f  s)  \mLeftarrow{}{}\mRightarrow{}  \mforall{}x:Item.  (\mneg{}\muparrow{}(member  x  s)))\}  ].
\mforall{}[singleton:\{f:Item  {}\mrightarrow{}  set|  \mforall{}x,y:Item.    (\muparrow{}(member  x  (f  y))  \mLeftarrow{}{}\mRightarrow{}  x  =  y)\}  ].
\mforall{}[add:\{f:Item  {}\mrightarrow{}  set  {}\mrightarrow{}  set| 
              \mforall{}s:set.  \mforall{}x,y:Item.    (\muparrow{}(member  x  (f  y  s))  \mLeftarrow{}{}\mRightarrow{}  (x  =  y)  \mvee{}  (\muparrow{}(member  x  s)))\}  ].
\mforall{}[union:\{f:set  {}\mrightarrow{}  set  {}\mrightarrow{}  set| 
                  \mforall{}s1,s2:set.  \mforall{}x:Item.    (\muparrow{}(member  x  (f  s1  s2))  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}(member  x  s1))  \mvee{}  (\muparrow{}(member  x  s2)))\}  ].
\mforall{}[remove:\{f:Item  {}\mrightarrow{}  set  {}\mrightarrow{}  set| 
                    \mforall{}s:set.  \mforall{}x,y:Item.    (\muparrow{}(member  x  (f  y  s))  \mLeftarrow{}{}\mRightarrow{}  (\mneg{}(x  =  y))  \mwedge{}  (\muparrow{}(member  x  s)))\}  ].
    (mk-set(Item;set;member;empty;isEmpty;singleton;add;union;remove)  \mmember{}  set-sig\{i:l\}(Item))
Date html generated:
2016_05_17-PM-01_44_07
Last ObjectModification:
2015_12_28-PM-08_52_54
Theory : datatype-signatures
Home
Index