Nuprl Definition : wfd-tree
wfd-tree(A) == {w:co-w(A)| ∀p:ℕ ⟶ A. w-bars(w;p)}
Wellformedness Lemmas :
wfd-tree_wf
Definitions occuring in Statement :
w-bars: w-bars(w;p),
co-w: co-w(A),
nat: ℕ,
all: ∀x:A. B[x],
set: {x:A| B[x]} ,
function: x:A ⟶ B[x]
Definitions occuring in definition :
set: {x:A| B[x]} ,
co-w: co-w(A),
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
nat: ℕ,
w-bars: w-bars(w;p)
FDL editor aliases :
wfd-tree2
Latex:
wfd-tree(A) == \{w:co-w(A)| \mforall{}p:\mBbbN{} {}\mrightarrow{} A. w-bars(w;p)\}
Date html generated:
2016_05_15-PM-10_05_49
Last ObjectModification:
2015_09_23-AM-08_22_12
Theory : bar!induction
Home
Index