Nuprl - Proof: d-realizes wf 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: d-realizes wf 1 1 1

1. D : Dsys
2. {es:ES| es is an event system of D }

Prop
3. D' : Dsys
4. D

D'
5. w : World
6. FairFifo
7. PossibleWorld(D';w)

PossibleWorld(D;w)

By:	Inst Thm* A,B:Dsys. A B (w:World. PossibleWorld(B;w) PossibleWorld(A;w)) [D;D';w]

Generated subgoals:

None

About:

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