Nuprl Definition : bdd-val
bdd-val(v0;x;n) ==
{f:{a:formula()| a ⊆ x ∧ prank(a) < n} ⟶ 𝔹| ∀a:{a:formula()| a ⊆ x ∧ prank(a) < n} . f a = extend-val(v0;f;a)}
Definitions occuring in Statement :
extend-val: extend-val(v0;g;x),
psub: a ⊆ b,
prank: prank(x),
formula: formula(),
bool: 𝔹,
less_than: a < b,
all: ∀x:A. B[x],
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ⟶ B[x],
equal: s = t ∈ T
Definitions occuring in definition :
function: x:A ⟶ B[x],
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
formula: formula(),
and: P ∧ Q,
psub: a ⊆ b,
less_than: a < b,
prank: prank(x),
equal: s = t ∈ T,
bool: 𝔹,
apply: f a,
extend-val: extend-val(v0;g;x)
FDL editor aliases :
bdd-val
Latex:
bdd-val(v0;x;n) ==
\{f:\{a:formula()| a \msubseteq{} x \mwedge{} prank(a) < n\} {}\mrightarrow{} \mBbbB{}|
\mforall{}a:\{a:formula()| a \msubseteq{} x \mwedge{} prank(a) < n\} . f a = extend-val(v0;f;a)\}
Date html generated:
2016_05_15-PM-07_16_03
Last ObjectModification:
2015_09_23-AM-08_13_49
Theory : general
Home
Index