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: s = 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