Nuprl Definition : pa-is-sign-implies
pa-is-sign-implies(a;v.P[v]) == ((fst(a)) = "sign" ∈ Atom) ⇒ P[snd(a)]
Definitions occuring in Statement :
pi1: fst(t),
pi2: snd(t),
implies: P ⇒ Q,
token: "$token",
atom: Atom,
equal: s = t ∈ T
FDL editor aliases :
pa-is-sign-implies
Latex:
pa-is-sign-implies(a;v.P[v]) == ((fst(a)) = "sign") {}\mRightarrow{} P[snd(a)]
Date html generated:
2015_07_23-PM-00_13_39
Last ObjectModification:
2013_10_26-PM-09_29_41
Home
Index