Nuprl Definition : pa-is-new-and

pa-is-new-and(a;v.P[v]) ==  ((fst(a)) "new" ∈ Atom) ∧ P[snd(a)]



Definitions occuring in Statement :  pi1: fst(t) pi2: snd(t) and: P ∧ Q token: "$token" atom: Atom equal: t ∈ T
FDL editor aliases :  pa-is-new-and

Latex:
pa-is-new-and(a;v.P[v])  ==    ((fst(a))  =  "new")  \mwedge{}  P[snd(a)]



Date html generated: 2015_07_23-PM-00_13_47
Last ObjectModification: 2013_10_26-PM-09_42_17

Home Index