Nuprl Definition : pv11_p1_in_domain
pv11_p1_in_domain(Cmd) == λx,xys. x ∈b map(λx.(fst(x));xys)
Definitions occuring in Statement :
deq-member: x ∈b L,
map: map(f;as),
int-deq: IntDeq,
pi1: fst(t),
lambda: λx.A[x]
FDL editor aliases :
pv11_p1_in_domain
Latex:
pv11\_p1\_in\_domain(Cmd) == \mlambda{}x,xys. x \mmember{}\msubb{} map(\mlambda{}x.(fst(x));xys)
Date html generated:
2016_05_17-PM-02_48_10
Last ObjectModification:
2014_11_26-AM-11_22_48
Theory : paxos!synod
Home
Index