Nuprl Definition : hdf-sequence

hdf-sequence(X;Y;Z) ==
  mk-hdf(S,a.case S
   of inl(XY) =>
   let X,Y = XY 
   in let X',bx = X(a) 
      in let Y',by = Y(a) 
         in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = Z(a) in <inr Z' , bz> else <inl <X', Y'>, bx> fi 
   | inr(Z) =>
   let Z',b = Z(a) 
   in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <X, Y>)


Definitions occuring in Statement :  mk-hdf: mk-hdf(s,m.G[s; m];st.H[st];s0),  hdf-halted: hdf-halted(P),  hdf-ap: X(a),  band: p ∧b q,  bnot: ¬bb,  ifthenelse: if b then t else f fi ,  bfalse: ff,  spread: spread def,  pair: <a, b>,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  inr: inr x ,  inl: inl x,  bag-null: bag-null(bs)
FDL editor aliases :  hdf-sequence
hdf-sequence(X;Y;Z)  ==
    mk-hdf(S,a.case  S
      of  inl(XY)  =>
      let  X,Y  =  XY 
      in  let  X',bx  =  X(a) 
            in  let  Y',by  =  Y(a) 
                  in  if  bag-null(bx)  \mwedge{}\msubb{}  (\mneg{}\msubb{}bag-null(by))
                        then  let  Z',bz  =  Z(a) 
                                  in  <inr  Z'  ,  bz>
                        else  <inl  <X',  Y'>,  bx>
                        fi 
      |  inr(Z)  =>
      let  Z',b  =  Z(a) 
      in  <inr  Z'  ,  b>S.case  S  of  inl(XY)  =>  ff  |  inr(Z)  =>  hdf-halted(Z);inl  <X,  Y>)


Date html generated: 2015_07_17-AM-08_06_44
Last ObjectModification: 2012_12_10-AM-11_55_05

Home Index