is mentioned by
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* T1 = T2 Thm* ![]() ![]() Thm* ( ![]() ![]() ![]() Thm* ![]() ![]() Thm* (WellFnd{i}(T1;x,y.r1(x,y)) ![]() ![]() | [wellfounded_functionality_wrt_iff] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* T1 = T2 Thm* ![]() ![]() Thm* ( ![]() ![]() ![]() Thm* ![]() ![]() Thm* WellFnd{i}(T1;x,y.r1(x,y)) ![]() ![]() | [wellfounded_functionality_wrt_implies] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* WellFnd{i}(A;x,y.r(x,y)) ![]() ![]() | [inv_image_ind] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* WellFnd{i}(T;x,y.r(x,y)) ![]() ![]() | [inv_image_ind_tp] |
![]() ![]() ![]() ![]() ![]() ![]() ![]() Thm* WellFnd{i}(T;x,y.r(x,y)) ![]() ![]() | [inv_image_ind_a] |
Def == ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | [wellfounded] |
In prior sections: core
Try larger context:
StandardLIB
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html