:: deftheorem defines N16toB4 DESCIP_1:def 22 :
for a being Element of 16 holds
( ( a = 0 implies N16toB4 a = <*FALSE,FALSE,FALSE,FALSE*> ) & ( a = 1 implies N16toB4 a = <*FALSE,FALSE,FALSE,TRUE*> ) & ( a = 2 implies N16toB4 a = <*FALSE,FALSE,TRUE,FALSE*> ) & ( a = 3 implies N16toB4 a = <*FALSE,FALSE,TRUE,TRUE*> ) & ( a = 4 implies N16toB4 a = <*FALSE,TRUE,FALSE,FALSE*> ) & ( a = 5 implies N16toB4 a = <*FALSE,TRUE,FALSE,TRUE*> ) & ( a = 6 implies N16toB4 a = <*FALSE,TRUE,TRUE,FALSE*> ) & ( a = 7 implies N16toB4 a = <*FALSE,TRUE,TRUE,TRUE*> ) & ( a = 8 implies N16toB4 a = <*TRUE,FALSE,FALSE,FALSE*> ) & ( a = 9 implies N16toB4 a = <*TRUE,FALSE,FALSE,TRUE*> ) & ( a = 10 implies N16toB4 a = <*TRUE,FALSE,TRUE,FALSE*> ) & ( a = 11 implies N16toB4 a = <*TRUE,FALSE,TRUE,TRUE*> ) & ( a = 12 implies N16toB4 a = <*TRUE,TRUE,FALSE,FALSE*> ) & ( a = 13 implies N16toB4 a = <*TRUE,TRUE,FALSE,TRUE*> ) & ( a = 15 implies N16toB4 a = <*TRUE,TRUE,TRUE,FALSE*> ) & ( a = 16 implies N16toB4 a = <*TRUE,TRUE,TRUE,TRUE*> ) );