Nuprl Definition : non-zero-component

non-zero-component(r;eq;k;a) ==
  (λr,eq,k,a. eval j' = k in
              case letrec G(x)=if (x) < (j')
                                  then if eq (a x) 0 then G (x + 1) else inl <x, λ_.Ax> fi 
                                  else (inr (λx.Ax) ) in
                    G(0)
               of inl(p) =>
               let i,_ = p 
               in i
               | inr(_) =>
               ⊥) 
  r 
  eq 
  k 
  a


Definitions occuring in Statement :  genrec-ap: genrec-ap,  bottom: ⊥,  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  less: if (a) < (b)  then c  else d,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  inl: inl x,  add: n + m,  natural_number: $n,  axiom: Ax,  rng_zero: 0
Definitions occuring in definition :  callbyvalue: callbyvalue,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  genrec-ap: genrec-ap,  less: if (a) < (b)  then c  else d,  ifthenelse: if b then t else f fi ,  rng_zero: 0,  apply: f a,  add: n + m,  inl: inl x,  pair: <a, b>,  inr: inr x ,  lambda: λx.A[x],  axiom: Ax,  natural_number: $n,  spread: spread def,  bottom: ⊥
FDL editor aliases :  non-zero-component
Latex:
non-zero-component(r;eq;k;a)  ==
    (\mlambda{}r,eq,k,a.  eval  j'  =  k  in
                            case  letrec  G(x)=if  (x)  <  (j')
                                                                    then  if  eq  (a  x)  0  then  G  (x  +  1)  else  inl  <x,  \mlambda{}$_{\mbackslash{}ff\000C7d$.Ax>  fi 
                                                                    else  (inr  (\mlambda{}x.Ax)  )  in
                                        G(0)
                              of  inl(p)  =>
                              let  i,$_{}$  =  p 
                              in  i
                              |  inr($_{}$)  =>
                              \mbot{}) 
    r 
    eq 
    k 
    a


Date html generated: 2018_05_21-PM-09_42_35
Last ObjectModification: 2018_01_12-AM-10_42_42

Theory : matrices


Home Index