Nuprl Lemma : ldst_mk_lnk_lemma

n,j,i:Top.  (destination((link(n) from to j)) j)


Proof




Definitions occuring in Statement :  ldst: destination(l) mk_lnk: (link(n) from to j) top: Top all: x:A. B[x] sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T mk_lnk: (link(n) from to j) ldst: destination(l) pi2: snd(t) pi1: fst(t)

Latex:
\mforall{}n,j,i:Top.    (destination((link(n)  from  i  to  j))  \msim{}  j)



Date html generated: 2016_05_16-AM-10_56_00
Last ObjectModification: 2015_12_29-AM-09_08_32

Theory : event-ordering


Home Index