data specification
using nat
data types ebaentry := unmapped
| ⌜ . ⌝(. .pnum : nat)
;
variables ebae : ebaentry;
ebae0 : ebaentry;
ebae1 : ebaentry;
ebae2 : ebaentry;
end data specification