Nuprl - Proof: better-w-match-exists 1

(43steps total) PrintForm Definitions Lemmas mb event system 3 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: better-w-match-exists 1

1. the_w : World
2. e : E
3.

i:Id, t:

, l:IdLnk.

source(l) = i

onlnk(l;m(i;t)) = nil
4.

i:Id, t:

. isnull(a(i;t))

(

x:Id. s(i;t+1).x = s(i;t).x) & m(i;t) = nil
5.

i:Id, t:

, l:IdLnk.
5. isrcv(l;a(i;t))
5.

5. destination(l) = i & ||queue(l;t)||

1 & hd(queue(l;t)) = msg(a(i;t))
6.

l:IdLnk, t:

.
6.

t':

. t

t' & isrcv(l;a(destination(l);t'))

queue(l;t') = nil
7. isrcv(kind(e))

isrcv(lnk(kind(e));a(loc(e);time(e)))

By:	RepeatFor 4 (Thin 3) THEN Unfold `w-isrcvl` 0 THEN Analyze 2 THEN Analyze 2 THEN All (Unfolds [`w-loc`;`w-time`;`w-ekind`]) THEN All Reduce THEN All (Unfolds [`w-act`]) THEN All Reduce

Generated subgoal:

1 2. e1 : Id
3. e2 :
4. isnull(a(e1;e2))  [not for witness]
5. isrcv(kind(a(e1;e2)))
  isnull(a(e1;e2))isrcv(kind(a(e1;e2)))
  lnk(kind(a(e1;e2))) = lnk(kind(a(e1;e2)))
2 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(43steps total) PrintForm Definitions Lemmas mb event system 3 Sections EventSystems Doc