Nuprl Definition : bdd-all
bdd-all(n;i.P[i]) ==  primrec(n;tt;λi,x. (P[i] ∧b x))
Definitions occuring in Statement : 
band: p ∧b q
, 
primrec: primrec(n;b;c)
, 
btrue: tt
, 
lambda: λx.A[x]
Definitions occuring in definition : 
primrec: primrec(n;b;c)
, 
btrue: tt
, 
lambda: λx.A[x]
, 
band: p ∧b q
FDL editor aliases : 
bdd-all
Latex:
bdd-all(n;i.P[i])  ==    primrec(n;tt;\mlambda{}i,x.  (P[i]  \mwedge{}\msubb{}  x))
Date html generated:
2016_05_13-PM-04_00_48
Last ObjectModification:
2015_09_22-PM-05_45_43
Theory : bool_1
Home
Index