Nuprl Definition : W-bars
W-bars(w;p) == ↓∃n:ℕ. (↑isr(W-select(w;map(p;upto(n)))))
Definitions occuring in Statement :
W-select: W-select(w;s),
upto: upto(n),
map: map(f;as),
nat: ℕ,
assert: ↑b,
isr: isr(x),
exists: ∃x:A. B[x],
squash: ↓T
Definitions occuring in definition :
squash: ↓T,
exists: ∃x:A. B[x],
nat: ℕ,
assert: ↑b,
isr: isr(x),
W-select: 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{}isr(W-select(w;map(p;upto(n)))))
Date html generated:
2016_05_15-PM-10_06_41
Last ObjectModification:
2015_09_23-AM-08_22_17
Theory : bar!induction
Home
Index