### Nuprl Lemma : set-sig-add_wf

`∀[Item:Type]. ∀[s:set-sig{i:l}(Item)].  (set-sig-add(s) ∈ Item ⟶ set-sig-set(s) ⟶ set-sig-set(s))`

Proof

Definitions occuring in Statement :  set-sig-add: `set-sig-add(s)` set-sig-set: `set-sig-set(s)` set-sig: `set-sig{i:l}(Item)` uall: `∀[x:A]. B[x]` member: `t ∈ T` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` set-sig-add: `set-sig-add(s)` set-sig-set: `set-sig-set(s)` set-sig: `set-sig{i:l}(Item)` record+: record+ record-select: `r.x` subtype_rel: `A ⊆r B` eq_atom: `x =a y` ifthenelse: `if b then t else f fi ` btrue: `tt` implies: `P `` Q` guard: `{T}` so_lambda: `λ2x.t[x]` so_apply: `x[s]` all: `∀x:A. B[x]` prop: `ℙ` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` and: `P ∧ Q` or: `P ∨ Q`

Latex:
\mforall{}[Item:Type].  \mforall{}[s:set-sig\{i:l\}(Item)].    (set-sig-add(s)  \mmember{}  Item  {}\mrightarrow{}  set-sig-set(s)  {}\mrightarrow{}  set-sig-set(s))

Date html generated: 2016_05_17-PM-01_44_29
Last ObjectModification: 2015_12_28-PM-08_52_39

Theory : datatype-signatures

Home Index