:: deftheorem Def1 defines NumberOnLevel BINTREE2:def 1 :
for T being binary Tree
for n being non zero Nat
for b₃ being Function of (T -level n),NAT holds
( b₃ = NumberOnLevel (n,T) iff for t being Element of T st t in T -level n holds
for F being Element of n -tuples_on BOOLEAN st F = Rev t holds
b₃ . t = (Absval F) + 1 );