Nuprl Definition : tree-secures

tree-secures(T;A;p)==r let iszero,f = p in if iszero then ∀s:ℕ0 ⟶ T. (A 0 s) else ∀x:T. tree-secures(T;A[x];f x) fi 
tree-secures(T;A;p) ==
  fix((λtree-secures,A,p. let iszero,f = p 
                          in if iszero then ∀s:ℕ0 ⟶ T. (A 0 s) else ∀x:T. (tree-secures A[x] (f x)) fi )) 
  A 
  p


Definitions occuring in Statement :  predicate-or-shift: A[x],  int_seg: {i..j-},  ifthenelse: if b then t else f fi ,  all: ∀x:A. B[x],  apply: f a,  fix: fix(F),  lambda: λx.A[x],  function: x:A ⟶ B[x],  spread: spread def,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  ifthenelse: if b then t else f fi ,  function: x:A ⟶ B[x],  int_seg: {i..j-},  natural_number: $n,  all: ∀x:A. B[x],  predicate-or-shift: A[x],  apply: f a
FDL editor aliases :  tree-secures
Latex:
tree-secures(T;A;p)
==r  let  iszero,f  =  p 
        in  if  iszero  then  \mforall{}s:\mBbbN{}0  {}\mrightarrow{}  T.  (A  0  s)  else  \mforall{}x:T.  tree-secures(T;A[x];f  x)  fi 

Latex:
tree-secures(T;A;p)  ==
    fix((\mlambda{}tree-secures,A,p.  let  iszero,f  =  p 
                                                    in  if  iszero
                                                          then  \mforall{}s:\mBbbN{}0  {}\mrightarrow{}  T.  (A  0  s)
                                                          else  \mforall{}x:T.  (tree-secures  A[x]  (f  x))
                                                          fi  )) 
    A 
    p


Date html generated: 2016_05_14-PM-04_07_20
Last ObjectModification: 2015_09_22-PM-06_02_07

Theory : fan-theorem


Home Index