Nuprl Lemma : lnk-decl-dom-join
∀[l:IdLnk]. ∀[k:Knd]. ∀[dt1,dt2:tg:Id fp-> Type].
(k ∈ dom(lnk-decl(l;dt1 ⊕ dt2)) ~ k ∈ dom(lnk-decl(l;dt1)) ∨bk ∈ dom(lnk-decl(l;dt2)))
Proof
Definitions occuring in Statement :
lnk-decl: lnk-decl(l;dt),
fpf-join: f ⊕ g,
fpf-dom: x ∈ dom(f),
fpf: a:A fp-> B[a],
Kind-deq: KindDeq,
Knd: Knd,
IdLnk: IdLnk,
id-deq: IdDeq,
Id: Id,
bor: p ∨bq,
uall: ∀[x:A]. B[x],
universe: Type,
sqequal: s ~ t
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
uimplies: b supposing a,
so_lambda: λ2x.t[x],
so_apply: x[s],
subtype_rel: A ⊆r B,
lnk-decl: lnk-decl(l;dt),
fpf-dom: x ∈ dom(f),
pi1: fst(t),
sq_type: SQType(T),
all: ∀x:A. B[x],
implies: P ⇒ Q,
guard: {T},
fpf: a:A fp-> B[a],
fpf-join: f ⊕ g,
top: Top,
mapfilter: mapfilter(f;P;L),
iff: P ⇐⇒ Q,
and: P ∧ Q,
prop: ℙ,
cand: A c∧ B,
exists: ∃x:A. B[x],
rev_implies: P ⇐ Q,
or: P ∨ Q,
not: ¬A,
decidable: Dec(P)
Latex:
\mforall{}[l:IdLnk]. \mforall{}[k:Knd]. \mforall{}[dt1,dt2:tg:Id fp-> Type].
(k \mmember{} dom(lnk-decl(l;dt1 \moplus{} dt2)) \msim{} k \mmember{} dom(lnk-decl(l;dt1)) \mvee{}\msubb{}k \mmember{} dom(lnk-decl(l;dt2)))
Date html generated:
2016_05_16-AM-11_35_07
Last ObjectModification:
2015_12_29-AM-09_32_11
Theory : event-ordering
Home
Index