theorem :: NTALGO_2:11
Nat2BL . 4 = <*0,0,1*>