Nuprl Definition : howard-bar-rec

howard-bar-rec(M;mon;base;ind;n;s)
==r case M n s
     of inl(x) =>
     let k,p = x 
     in base n s (mon n k s p)
     | inr(x) =>
     ind n s (λt.howard-bar-rec(M;mon;base;ind;n + 1;s.t@n))
howard-bar-rec(M;mon;base;ind;n;s) ==
  fix((λhoward-bar-rec,n,s. case M n s
                            of inl(x) =>
                            let k,p = x 
                            in base n s (mon n k s p)
                            | inr(x) =>
                            ind n s (λt.(howard-bar-rec (n + 1) s.t@n)))) 
  n 
  s


Definitions occuring in Statement :  seq-add: s.x@n,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  add: n + m,  natural_number: $n
Definitions occuring in definition :  seq-add: s.x@n,  natural_number: $n,  add: n + m,  apply: f a,  lambda: λx.A[x],  spread: spread def,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  fix: fix(F)
FDL editor aliases :  howard-bar-rec
Latex:
howard-bar-rec(M;mon;base;ind;n;s)
==r  case  M  n  s
          of  inl(x)  =>
          let  k,p  =  x 
          in  base  n  s  (mon  n  k  s  p)
          |  inr(x)  =>
          ind  n  s  (\mlambda{}t.howard-bar-rec(M;mon;base;ind;n  +  1;s.t@n))
Latex:
howard-bar-rec(M;mon;base;ind;n;s)  ==
    fix((\mlambda{}howard-bar-rec,n,s.  case  M  n  s
                                                        of  inl(x)  =>
                                                        let  k,p  =  x 
                                                        in  base  n  s  (mon  n  k  s  p)
                                                        |  inr(x)  =>
                                                        ind  n  s  (\mlambda{}t.(howard-bar-rec  (n  +  1)  s.t@n)))) 
    n 
    s


Date html generated: 2016_05_19-PM-00_05_11
Last ObjectModification: 2016_05_18-AM-09_44_34

Theory : continuity


Home Index