is mentioned by
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* ring(R;in;out) Thm* ![]() ![]() Thm* Inj(|R|; ![]() Thm* ![]() ![]() Thm* ![]() ![]() Thm* realizes es. ![]() Thm* realizes es. ![]() Thm* realizes es.& ( ![]() ![]() ![]() ![]() ![]() | [ring-leader1__realizes] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* ring(R;in;out) Thm* ![]() ![]() Thm* Inj(|R|; ![]() ![]() ![]() ![]() ![]() | [ring-leader1__feasible] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* ring(R;in;out) Thm* ![]() ![]() Thm* Inj(|R|; ![]() ![]() ![]() ![]() | [ring-leader1_wf] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* ring(R;in;out) Thm* ![]() ![]() Thm* Inj(|R|; ![]() ![]() ![]() ![]() ![]() | [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