Nuprl Definition : tree-bars
(p|A) == fix((λtree-bars,A,p. let iszero,f = p in if iszero then A 0 (λx.x) else ∀x:T. (tree-bars A_x (f x)) fi )) A p
Definitions occuring in Statement :
predicate-shift: A_x,
ifthenelse: if b then t else f fi ,
all: ∀x:A. B[x],
apply: f a,
fix: fix(F),
lambda: λx.A[x],
spread: spread def,
natural_number: $n
Definitions occuring in definition :
fix: fix(F),
spread: spread def,
ifthenelse: if b then t else f fi ,
natural_number: $n,
lambda: λx.A[x],
all: ∀x:A. B[x],
predicate-shift: A_x,
apply: f a
FDL editor aliases :
tree-bars
Latex:
(p|A) ==
fix((\mlambda{}tree-bars,A,p. let iszero,f = p
in if iszero then A 0 (\mlambda{}x.x) else \mforall{}x:T. (tree-bars A\_x (f x)) fi ))
A
p
Date html generated:
2016_05_14-PM-04_12_08
Last ObjectModification:
2015_09_22-PM-06_02_21
Theory : fan-theorem
Home
Index