Nuprl Lemma : assert-has-src
∀[i:Id]. ∀[k:Knd]. uiff(↑has-src(i;k);(↑isrcv(k)) c∧ (source(lnk(k)) = i ∈ Id))
Proof
Definitions occuring in Statement :
has-src: has-src(i;k),
lsrc: source(l),
lnk: lnk(k),
isrcv: isrcv(k),
Knd: Knd,
Id: Id,
assert: ↑b,
uiff: uiff(P;Q),
uall: ∀[x:A]. B[x],
cand: A c∧ B,
equal: s = t ∈ T
Lemmas :
assert_witness,
isrcv_wf,
assert_wf,
has-src_wf,
Id_wf,
lsrc_wf,
lnk_wf,
Knd_wf,
assert-eq-id
\mforall{}[i:Id]. \mforall{}[k:Knd]. uiff(\muparrow{}has-src(i;k);(\muparrow{}isrcv(k)) c\mwedge{} (source(lnk(k)) = i))
Date html generated:
2015_07_17-AM-09_13_53
Last ObjectModification:
2015_01_28-AM-07_54_54
Home
Index