Nuprl Definition : noncelike-signatures
noncelike-signatures(s;es;thr) ==
∀e1,e2:E(Sign). ((signature(e1) = signature(e2) ∈ Atom1) ⇒ e1 ∈ thr ⇒ (e1 = e2 ∈ E))
Definitions occuring in Statement :
ses-thread-member: e ∈ thr,
ses-sig: signature(e),
ses-sign: Sign,
es-E-interface: E(X),
es-E: E,
atom: Atom$n,
all: ∀x:A. B[x],
implies: P ⇒ Q,
equal: s = t ∈ T
FDL editor aliases :
noncelike-signatures
Latex:
noncelike-signatures(s;es;thr) ==
\mforall{}e1,e2:E(Sign). ((signature(e1) = signature(e2)) {}\mRightarrow{} e1 \mmember{} thr {}\mRightarrow{} (e1 = e2))
Date html generated:
2015_07_23-PM-00_12_40
Last ObjectModification:
2012_08_30-PM-04_29_40
Home
Index