Nuprl - Proof: w-causl-time 1 1 1 2 1

(17steps 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: w-causl-time 1 1 1 2 1

1. the_w : World
2. FairFifo
3. e : E
4. e' : E
5. isrcv(kind(e'))
6. e = sender(e')

time(sender(e'))<time(e')

By:

AssertBY (

n:

time(e'). match(lnk(kind(e'));n;time(e')))
(BackThru
(Thm*

the_w:World, e:E.
(Thm* FairFifo
(Thm*

(Thm* isrcv(kind(e))

(

t:

time(e). match(lnk(kind(e));t;time(e))))
THEN
Inst Thm*

f:(

). (

n:

. f(n))

f(mu(f)) & (

i:

. i<mu(f)

f(i))
[

t.match(lnk(kind(e'));t;time(e'))]
THENA
(Reduce 0 THEN ParallelOp -1)
THEN
Reduce -1
THEN
ExRepD

Generated subgoal:

1 7. n : time(e')
8. match(lnk(kind(e'));n;time(e'))
9. match(lnk(kind(e'));mu(t.match(lnk(kind(e'));t;time(e')));time(e'))
10. i:.
10. i<mu(t.match(lnk(kind(e'));t;time(e'))) match(lnk(kind(e'));i;time(e'))
time(sender(e'))<time(e')
4 steps

About:

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

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