Nuprl Definition : tree-tensor

tree-tensor(n;p;q) ==
fix((λtree-tensor,n,p,q. let pzero,f = p

                           in if (n =_z 0) then if pzero then q else Wsup(ff;λx.(tree-tensor 0 (f x) q)) fi

                              if pzero then p
                              else let qzero,g = q
                                   in if qzero
                                      then q

                                      else Wsup(ff;λx.(tree-tensor (n - 1) (tree-tensor n (f x) q)

                                                       (tree-tensor n p (g x))))

                                      fi
                              fi ))
  n
  p
  q

Definitions occuring in Statement : Wsup: Wsup(a;b), ifthenelse: if b then t else f fi , eq_int: (i =_z j), bfalse: ff, apply: f a, fix: fix(F), lambda: λx.A[x], spread: spread def, subtract: n - m, natural_number: $n
Definitions occuring in definition : fix: fix(F), eq_int: (i =_z j), spread: spread def, ifthenelse: if b then t else f fi , Wsup: Wsup(a;b), bfalse: ff, lambda: λx.A[x], subtract: n - m, natural_number: $n, apply: f a
FDL editor aliases : tree-tensor

Latex:
tree-tensor(n;p;q) == fix((\mlambda{}tree-tensor,n,p,q. let pzero,f = p in if (n =\msubz{} 0) then if pzero then q else Wsup(ff;\mlambda{}x.(tree-tensor 0 (f x) q)) fi if pzero then p else let qzero,g = q in if qzero then q else Wsup(ff;\mlambda{}x.(tree-tensor (n - 1) (tree-tensor n (f x) q) (tree-tensor n p (g x)))) fi fi )) n p q Date html generated: 2016_05_14-PM-04_07_29 Last ObjectModification: 2015_09_22-PM-06_02_07 Theory : fan-theorem Home Index