Nuprl Definition : es-decl-sets-compatible
dd1 || dd2 ==
let S1,ds1,da1 = dd1 in
let S2,ds2,da2 = dd2 in
∀i:Id. ((i ∈ S1) ⇒ (i ∈ S2) ⇒ (da1 i || da2 i ∧ ds1 i || ds2 i))
Definitions occuring in Statement :
fpf-compatible: f || g,
hasloc: hasloc(k;i),
Kind-deq: KindDeq,
Knd: Knd,
id-deq: IdDeq,
Id: Id,
l_member: (x ∈ l),
assert: ↑b,
spreadn: spread3,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
set: {x:A| B[x]} ,
apply: f a,
universe: Type
FDL editor aliases :
es-decl-sets-compatible
dd1 || dd2 ==
let S1,ds1,da1 = dd1 in
let S2,ds2,da2 = dd2 in
\mforall{}i:Id. ((i \mmember{} S1) {}\mRightarrow{} (i \mmember{} S2) {}\mRightarrow{} (da1 i || da2 i \mwedge{} ds1 i || ds2 i))
Date html generated:
2015_07_17-AM-11_56_41
Last ObjectModification:
2013_03_27-AM-10_38_49
Home
Index