Nuprl Definition : es-eq
es-eq(es) == λe1,e2. (loc(e1) = loc(e2) ∧b (¬bes-locless(es;e1;e2)) ∧b (¬bes-locless(es;e2;e1)))
Definitions occuring in Statement :
es-locless: es-locless(es;e1;e2),
es-loc: loc(e),
eq_id: a = b,
band: p ∧b q,
bnot: ¬bb,
lambda: λx.A[x]
FDL editor aliases :
es-eq
es-eq
es-eq(es) == \mlambda{}e1,e2. (loc(e1) = loc(e2) \mwedge{}\msubb{} (\mneg{}\msubb{}es-locless(es;e1;e2)) \mwedge{}\msubb{} (\mneg{}\msubb{}es-locless(es;e2;e1)))
Date html generated:
2015_07_17-AM-08_34_41
Last ObjectModification:
2013_03_23-AM-01_21_37
Home
Index