mb event system 7 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def Inj(ABf) == a1,a2:Af(a1) = f(a2 B  a1 = a2

is mentioned by

Thm* R:(Id), uid:(|R|), out,in:(|R|IdLnk).
Thm* ring(R;in;out)
Thm* 
Thm* Inj(|R|; uid)
Thm* 
Thm* loc.(ring-leader1(loc;R;uid;out;in)) 
Thm* realizes es.ldr:|R|. 
Thm* realizes es.e@ldr.kind(e) = locl("leader")
Thm* realizes es.& (i:|R|. e@i.kind(e) = locl("leader")  i = ldr  |R|)
[ring-leader1__realizes]
Thm* R:(Id), uid:(|R|), out,in:(|R|IdLnk).
Thm* ring(R;in;out)
Thm* 
Thm* Inj(|R|; uid d-feasible(loc.(ring-leader1(loc;R;uid;out;in)))
[ring-leader1__feasible]
Thm* loc:Id, R:(Id), uid:(|R|), out,in:(|R|IdLnk).
Thm* ring(R;in;out)
Thm* 
Thm* Inj(|R|; uid ring-leader1(loc;R;uid;out;in MsgA List
[ring-leader1_wf]
Thm* loc:Id, R:(Id), uid:(|R|), out,in:(|R|IdLnk).
Thm* ring(R;in;out)
Thm* 
Thm* Inj(|R|; uid (A,Bring-leader1(loc;R;uid;out;in).A ||+ B)
[ring-leader1__compatible]

In prior sections: mb nat fun 1

Try larger context: EventSystems IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

mb event system 7 Sections EventSystems Doc