Nuprl Lemma : locknd_functionality_isrcv
∀[i,j:Id]. ∀[k1,k2:Knd]. (locknd(i;k1) = locknd(j;k2) ∈ LocKnd) supposing ((k1 = k2 ∈ Knd) and (↑isrcv(k1)))
Proof
Definitions occuring in Statement :
locknd: locknd(i;k),
LocKnd: LocKnd,
isrcv: isrcv(k),
Knd: Knd,
Id: Id,
assert: ↑b,
uimplies: b supposing a,
uall: ∀[x:A]. B[x],
equal: s = t ∈ T
Lemmas :
subtype_base_sq,
Knd_wf,
union_subtype_base,
IdLnk_wf,
product_subtype_base,
atom2_subtype_base,
isrcv-implies,
equal_wf,
assert_wf,
isrcv_wf,
Id_wf,
ldst_wf,
lnk_wf,
spread_wf,
hasloc_wf,
iff_weakening_uiff,
isect_wf,
assert-hasloc,
squash_wf,
true_wf,
iff_weakening_equal
\mforall{}[i,j:Id]. \mforall{}[k1,k2:Knd]. (locknd(i;k1) = locknd(j;k2)) supposing ((k1 = k2) and (\muparrow{}isrcv(k1)))
Date html generated:
2015_07_17-AM-09_14_42
Last ObjectModification:
2015_02_04-PM-05_06_56
Home
Index