Nuprl Definition : pv11_p1_update_proposals

pv11_p1_update_proposals(Cmd) ==
  λproposals1,proposals2. (filter(λprp.(¬b(∃prp'∈proposals2.(fst(prp) =z fst(prp')))_b);proposals1) @ proposals2)


Definitions occuring in Statement :  bl-exists: (∃x∈L.P[x])_b,  filter: filter(P;l),  append: as @ bs,  bnot: ¬bb,  eq_int: (i =z j),  pi1: fst(t),  lambda: λx.A[x]
FDL editor aliases :  pv11_p1_update_proposals
Latex:
pv11\_p1\_update\_proposals(Cmd)  ==
    \mlambda{}proposals1,proposals2.  (filter(\mlambda{}prp.(\mneg{}\msubb{}(\mexists{}prp'\mmember{}proposals2.(fst(prp)  =\msubz{}  fst(prp')))\_b);proposals1)
                                                  @  proposals2)


Date html generated: 2016_05_17-PM-02_48_05
Last ObjectModification: 2014_11_26-AM-11_22_44

Theory : paxos!synod


Home Index