Description: Obsolete version of nnsdomg as of 7-Jan-2025. (Contributed by NM, 15-Jun-1998) (Proof modification is discouraged.) (New usage is discouraged.)