bit.txt -- definition of bits
uses:
   atom.txt -- definition of atoms
   higher.txt -- higher-order definitions  (one_valid, mapped_pred)
   uncbasic.txt -- unconditional basic predicates  (member)

This file defines (declares) the bit atoms that are used in the expression
representation of characters.  These bit atoms are declared using the
following axiom:

   (atom_set bit_atom (`bit0 `bit1)).

From this we get following "bit_atom" predicate (see <atom.txt> file):

!  (bit_atom <bit_atom>)

An alternative definition is to declare the bit atoms separately:

!  (atom_defn `bit0 "bit0" bit0_atom).
!  (atom_defn `bit1 "bit1" bit1_atom).

 ! (atom_defn <atom> <atom_name> <atom_pred>)   -- see <atom.txt> file

This gives us the "bit0_atom" and "bit1_atom" predicates for referring to
the specific atoms.  But we need the following additional axiom to define
the set of bit atoms:

!  (bit_atom %bit_atom)<
!    (one_valid
!        (bit0_atom %bit_atom)
!        (bit1_atom %bit_atom)).

Here we are using the "atom predicates" to "hide" the representation of the
bit atoms.  But perhaps it would be just as well to write:

!  (bit_atom %bit_atom)<
!    (member %bit_atom (`bit0 `bit1)). 

For now we will use the above atom_set definition and assume that we will
not need the bitx_atom predicates.

We can define the set of sequences of bit atoms as follows:

   (mapped_pred bit_atom_seq bit_atom).

The "bit_atom_seq" predicate is perhaps unnecessary since (map bit_atom) is
equivalent and symbolic forms of the map function, such as bit_atom* or
*:bit_atom will also be defined later.  But for now we will make use of
this explicit definition.
 
See <char.txt> for a description of how characters are defined from bit atoms,
and see <notequal.txt> for a definition of inequality between bit atoms.