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)))


Definitions occuring in Statement :  locknd: locknd(i;k) LocKnd: LocKnd isrcv: isrcv(k) Knd: Knd Id: Id assert: b uimplies: supposing a uall: [x:A]. B[x] equal: 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