Nuprl Definition : bl-exists
(∃x∈L.P[x])_b == reduce(λx,p. (P[x] ∨bp);ff;L)
Definitions occuring in Statement :
reduce: reduce(f;k;as),
bor: p ∨bq,
bfalse: ff,
lambda: λx.A[x]
Definitions occuring in definition :
reduce: reduce(f;k;as),
lambda: λx.A[x],
bor: p ∨bq,
bfalse: ff
FDL editor aliases :
bl-exists
Latex:
(\mexists{}x\mmember{}L.P[x])\_b == reduce(\mlambda{}x,p. (P[x] \mvee{}\msubb{}p);ff;L)
Date html generated:
2016_05_14-PM-02_09_48
Last ObjectModification:
2015_09_22-PM-05_55_27
Theory : list_1
Home
Index