notequal.txt -- defining inequality in axiomatic language
uses:
   higher.txt
   finite.txt
   atom.txt
   bit.txt
   length.txt


This file defines inequality in axiomatic language.  To be more precise we
define the negative of the identity relation (== % %) -- that is, distinct
expressions are considered unequal.  Note that inequality is not built-in --
specifically, the inequality of distinct atoms is not built-in.  Instead we
use the "declarations" of atoms given in earlier files in order to define
inequality as needed.  Inequality between atoms and expressions involving
them is defined in section 1.  Section 2 defines some basic predicates
involving inequality.  Section 3 defines the complements of some common
sets.

*** What symbol to use for the inequality relation?:
    /=  Ada "not equals"
    ~=  let ~ be the general "not" symbol
    ~==  "not identical"
Since we use == for the identity relation (== % %), it probably makes sense
to use ~== for this "not identical" relation.  Later, when dealing with
expression representations of objects (instead of expressions that represent
just themselves), we can use = and ~= for equal and not equal objects.


1. Inequality between atoms and expressions

There is no built-in inequality between distinct atoms in axiomatic language
so it must be defined.  The file <atom.txt> shows how a set of distinct
atoms can be "declared" in a single expression.  We can define an inequality
relation between these atoms as follows:

   (~== %atom1 %atom2)<           ! inequality between atoms in set
     (atom_set %set_name ($1 %atom1 $2 %atom2 $3)).

Note that we are assuming that the atoms are distinct.  The file <bit.txt>
defined the two bit atoms `bit0 and `bit1, which are used for character
representation, in an atom set and thus we have an inequality relation
between them:

!  (~== `bit0 `bit1)       -- generated from above axiom and <bit.txt> axiom

We of course also need the inverse relation.  This is obtained by asserting
that the inequality relation is symmetric:

   (Symmetric ~==).        ! from <higher.txt>

This gives us the inverse relation (~== `bit1 `bit0) as well as inverses of
some of the other non-symmetric expressions below.

The above atom_set expression also generates an "atom" predicate which has
two forms:

!  (atom <atom>)
!  (atom <atom> <atom_name>)

We need to define that an atom is not equal to a sequence, which is done
as follows:

   (~== %atom ($))<            ! inequality between atom and sequence
     (atom %atom).

Now let us define inequality between sequences formed from unequal elements.
This is defined as follows:

   (~== () (% $)).               ! null and non-null sequences unequal
   (~== (%x $x) (%y $y))<        ! two sequences are unequal if ...
       (one_valid (~== %x %y)          ! head elements unequal, or ...
                  (~== ($x) ($y))).    ! tail sequences unequal

These axioms define inequality between distinct expressions formed from bit
atoms but they also define inequality between any two expressions where
different bit atoms occur in the same corresponding location.  Thus
two different characters would be unequal (see <char.txt>) and, similarly,
two different symbols (<symbol.txt>) and thus different expressions formed
from symbols would be unequal.  This should handle most of the inequality
needed.

We need to extend our inequality to other atoms that are declared,
either individual or in sets.  See <atom.txt> for a description of how
the "atom" predicate associates a single atom or a set of atoms with
a unique character string name.  We define the inequality between these
additional atoms based on that name as follows:

   (~== %atom1 %atom2)<
     (atom %atom1 %atom1_name),
     (atom %atom2 %atom2_name),
     (~== %atom1_name %atom2_name).

Note that the "atom name" string may refer to a single atom or may be the
set name (string from symbol) for a set of atoms (with inequality between
atoms within the set already defined by the earlier "atom_set" axiom.
This completes the definition of inequality between distinct expressions
formed from any atoms that have been properly declared.


2. Some basic predicates involving inequality

This section defines some basic predicates from inequality between expressions.
The not_member predicate is defined as follows: 

   (not_member %x ()).
   (not_member %x (% $))<
     (not_member %x ($)),
     (~== %x %).

   ! use ~member instead of not_member?   -- maybe
   ! -- Depends on the convention used for negation as failure.

Another similar predicate asserts that a given expression does not occur as
the first element of any sequence in a sequence of sequences:

   (not_first %x ()).
   (not_first %x ((% $) $seqs))<
     (not_first %x ($seqs)),
     (~== %x %).

   *** better name needed here?
       Where is this used?

Not a member of a finite set:

   (not_set_member %set %not_elem)<
     (finite_set %set %elems),
     (not_member %not_elem %elems).

   ! This covers atom sets as well since an atom_set is also a finite_set.

Not a sequence of elements from a finite set:

   (not_set_seq %set %atom)<      ! an atom is not a sequence
     (atom %atom).
   (not_set_seq %set %seq)<       ! sequence has non-set element
     (member %elem %seq),
     (not_set_member %set %elem).

*** many more "not_" predicates to be defined!


3. Non-membership in some common sets

Here we define expressions that are not characters:

   (not_char %atom)<               ! an atom is not a char
     (atom %atom).                 ! (atom must be "declared")
   (not_char ()).                  ! null sequence is not a char
   (not_char (%)).                 ! 1-expr sequence is not a char
   (not_char (%1 %2 %3 $)).        ! >=3-expr sequence is not a char
   (not_char (%not_char_atom $))<  ! 1st expr not char atom
     (char_atom %char_atom),       ! (we avoid explicit mention of char atom)
     (~== %not_char_atom %char_atom).  ! (inequality must be defined for atoms)
   (not_char (%1 %not_char_bit_seq $))<  ! 2nd expr not char bit seq
     (not_char_bit_seq %not_char_bit_seq).

   (not_char_bit_seq %not_bit_seq)<      ! not a bit sequence
     (not_set_seq bit_atom %not_bit_seq).
   (not_char_bit_seq %seq)<              ! or sequence length not correct
     (char_bit_seq_=length %=length),
     (/=length %seq %=length).
     ! We avoid using natural numbers here since they are defined later.
     ! Note that the length of a character bit sequence is hidden from
     ! this file.  (It is only defined once, in <char.txt>.)

   *** not_char_bit_seq probably does not deserve a permanent predicate defn

Note that atoms must be "declared" and inequality must be defined between
them for these axioms to apply.

We can define the set of expressions that are not character strings as
follows:

   (not_charstr %atom)<            ! an atom is not a character string
     (atom %atom).
   (not_charstr %seq)<             ! sequence contains a non-character
     (member %nonchar %seq),
     (not_char %nonchar).

   *** also done in <metaAL.txt>   -- remove it

The set of expressions that are not symbols are defined as follows:

   (not_symbol %atom)<               ! an atom is not a symbol
     (atom %atom).
   (not_symbol ()).                  ! a null sequence is not a symbol
   (not_symbol (%)).                 ! 1-expr sequence is not a char
   (not_symbol (%1 %2 %3 $)).        ! >=3-expr sequence is not a char
   (not_symbol (%not_sym_atom $))<   ! 1st expr not symbol atom
     (symbol_atom %sym_atom),        ! (we avoid mention of symbol atom)
     (~== %not_sym_atom %sym_atom).  ! (inequality must be defined for atoms)
   (not_symbol (%1 %not_charstr $))<  ! 2nd expr not char string
     (not_charstr %not_charstr).

-- Note that this definition has the same pattern as the not_char definition
   above.  Obviously, there is a potential for a higher-order form here.



*****  Explicit negative predicate definition vs. negation as failure

*****  This issue to be discussed later!!

A negation as failure definition that automatically defines negative
predicates from their positive axiom definitions would obviously be a
great simplification over explicit negative predicate definitions as
done here.