Nuprl Definition : request-buffer

request-buffer(Req) ==
  smr-class(<1, []>;s,reqst.let c = fst(reqst) in
                                let num,pending = s 
                                in if c <z num then <s, []>
                                   if num <z c
                                     then <<num
                                           , insert-by(r1,r2.(fst(r1) = fst(r2));r1,r2.fst(r1) <z fst(r2);reqst;
                                                       pending)
                                           >
                                          , []
                                          >
                                   else let p1,p2 = split-gap(x.(fst(x));pending) 
                                        in <<(num + 1) + ||p1||, p2>, map(x.(snd(x));[reqst / p1])>
                                   fi ;Req)


Proof not projected



Definitions occuring in Statement :  smr-class: smr-class(init;s,x.F[s; x];X),  map: map(f;as),  length: ||as||,  eq_int: (i = j),  lt_int: i <z j,  ifthenelse: if b then t else f fi ,  let: let,  pi1: fst(t),  pi2: snd(t),  lambda: x.A[x],  spread: spread def,  pair: <a, b>,  cons: [car / cdr],  nil: [],  add: n + m,  natural_number: $n,  split-gap: split-gap(f;L),  insert-by: insert-by(eq;r;x;l)
Definitions :  smr-class: smr-class(init;s,x.F[s; x];X),  let: let,  ifthenelse: if b then t else f fi ,  insert-by: insert-by(eq;r;x;l),  eq_int: (i = j),  lt_int: i <z j,  nil: [],  spread: spread def,  split-gap: split-gap(f;L),  pi1: fst(t),  pair: <a, b>,  add: n + m,  natural_number: $n,  length: ||as||,  map: map(f;as),  lambda: x.A[x],  pi2: snd(t),  cons: [car / cdr]
FDL editor aliases :  request-buffer
request-buffer(Req)  ==
    smr-class(ə,  []>s,reqst.let  c  =  fst(reqst)  in
                                                                let  num,pending  =  s 
                                                                in  if  c  <z  num  then  <s,  []>
                                                                      if  num  <z  c
                                                                          then  <<num
                                                                                      ,  insert-by(\mlambda{}r1,r2.(fst(r1)  =\msubz{}  fst(r2));
                                                                                                              \mlambda{}r1,r2.fst(r1)  <z  fst(r2);reqst;pending)
                                                                                      >
                                                                                    ,  []
                                                                                    >
                                                                      else  let  p1,p2  =  split-gap(\mlambda{}x.(fst(x));pending) 
                                                                                in  <<(num  +  1)  +  ||p1||,  p2>,  map(\mlambda{}x.(snd(x));[reqst  /  p1])>
                                                                      fi  ;Req)


Date html generated: 2011_10_20-PM-04_09_50
Last ObjectModification: 2011_01_25-AM-00_06_47

Home Index