Nuprl Lemma : mk-set-nat-missing_wf
mk-set-nat-missing() ∈ set-sig{i:l}(ℕ)
Proof
Definitions occuring in Statement :
mk-set-nat-missing: mk-set-nat-missing(),
set-sig: set-sig{i:l}(Item),
nat: ℕ,
member: t ∈ T
Definitions unfolded in proof :
mk-set-nat-missing: mk-set-nat-missing(),
member: t ∈ T,
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
nat-missing-type: nat-missing-type(),
prop: ℙ,
so_lambda: λ2x.t[x],
so_lambda: λ2x y.t[x; y],
nat: ℕ,
so_apply: x[s1;s2],
so_apply: x[s],
and: P ∧ Q,
uimplies: b supposing a,
all: ∀x:A. B[x],
not: ¬A,
false: False,
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
or: P ∨ Q,
cand: A c∧ B
Latex:
mk-set-nat-missing() \mmember{} set-sig\{i:l\}(\mBbbN{})
Date html generated:
2016_05_17-PM-01_46_30
Last ObjectModification:
2015_12_28-PM-08_51_49
Theory : datatype-signatures
Home
Index