Nuprl Definition : b-exists
(∃i<n.P[i])_b == primrec(n;ff;λi,x. (P[i] ∨bx))
Definitions occuring in Statement :
bor: p ∨bq,
primrec: primrec(n;b;c),
bfalse: ff,
lambda: λx.A[x]
Definitions occuring in definition :
primrec: primrec(n;b;c),
bfalse: ff,
lambda: λx.A[x],
bor: p ∨bq
FDL editor aliases :
b-exists
Latex:
(\mexists{}i<n.P[i])\_b == primrec(n;ff;\mlambda{}i,x. (P[i] \mvee{}\msubb{}x))
Date html generated:
2016_05_13-PM-04_00_35
Last ObjectModification:
2015_09_22-PM-05_45_41
Theory : bool_1
Home
Index