Nuprl - Proof: w-match-unique

(12steps 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-match-unique

the_w:World, e:E, t,t':

FairFifo

isrcv(kind(e))

match(lnk(kind(e));t;time(e))

match(lnk(kind(e));t';time(e))

t = t'

By:	Assert (the_w:World, e:E, t,t':. (FairFifo ( (isrcv(kind(e)) ( (t<t' match(lnk(kind(e));t;time(e)) match(lnk(kind(e));t';time(e)))

Generated subgoals:

1   the_w:World, e:E, t,t':.
  FairFifo

  isrcv(kind(e))

  t<t'  match(lnk(kind(e));t;time(e))  match(lnk(kind(e));t';time(e))
7 steps

2 1. the_w:World, e:E, t,t':.
1. FairFifo
1.
1. isrcv(kind(e))
1.
1. t<t'  match(lnk(kind(e));t;time(e))  match(lnk(kind(e));t';time(e))
  the_w:World, e:E, t,t':.
  FairFifo

  isrcv(kind(e))

  match(lnk(kind(e));t;time(e))  match(lnk(kind(e));t';time(e))  t = t'
4 steps

About:

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

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

1	the_w:World, e:E, t,t':. FairFifo isrcv(kind(e)) t<t' match(lnk(kind(e));t;time(e)) match(lnk(kind(e));t';time(e))	7 steps
2	1. the_w:World, e:E, t,t':. 1. FairFifo 1. 1. isrcv(kind(e)) 1. 1. t<t' match(lnk(kind(e));t;time(e)) match(lnk(kind(e));t';time(e)) the_w:World, e:E, t,t':. FairFifo isrcv(kind(e)) match(lnk(kind(e));t;time(e)) match(lnk(kind(e));t';time(e)) t = t'	4 steps