Nuprl Definition : w-bars
w-bars(w;p) == ↓∃n:ℕ. (↑co-w-null(w@map(p;upto(n))))
Definitions occuring in Statement :
co-w-select: w@s,
co-w-null: co-w-null(w),
upto: upto(n),
map: map(f;as),
nat: ℕ,
assert: ↑b,
exists: ∃x:A. B[x],
squash: ↓T
Definitions occuring in definition :
squash: ↓T,
exists: ∃x:A. B[x],
nat: ℕ,
assert: ↑b,
co-w-null: co-w-null(w),
co-w-select: w@s,
map: map(f;as),
upto: upto(n)
FDL editor aliases :
w-bars
Latex:
w-bars(w;p) == \mdownarrow{}\mexists{}n:\mBbbN{}. (\muparrow{}co-w-null(w@map(p;upto(n))))
Date html generated:
2016_05_15-PM-10_05_46
Last ObjectModification:
2015_09_23-AM-08_22_11
Theory : bar!induction
Home
Index