length.txt -- definition of predicates based on length
uses
   higher.txt

These notes define predicates involving lengths of sequences.  In effect,
we treat sequence lengths as a natural number, without using actual natural
numbers and their operations.  Note that many of these functions and relations
have a natural number counterpart (where a real natural number n is used
instead of a sequence of length n).

Two sequences of equal length:

   (=length () ()).
   (=length (%1 $1) (%2 $2))<
     (=length ($1) ($2)).

This binary relation can be generalized using the following higher-order form:

   (generalize_binrel =length).

This generates the following versions of =length:

!  (=length seq1 ... seqn)     -- n >= 2 sequences of equal length
!  (=length (seq1 ... seqn))   -- seq of sequences of equal length  (n>=0)

two sequences of unequal length:

   (valid (/=length ($1) ($2 % $))
          (/=length ($1 % $) ($2)))<
     (=length ($1) ($2)). 

ordering relation based on sequence length:

   (<length ($1) ($2 % $))<
     (=length ($1) ($2)).

   (<=length %1 %2)<
     (one_valid
       (<length %1 %2)
       (=length %1 %2)).

   (>length %1 %2)<
     (<length %2 %1).

   (>=length %1 %2)<
     (<=length %2 %1).

-- better definition of unequal length?:

   (/=length %1 %2)<
     (one_valid
       (<length %1 %2)
       (>length %1 %2)).

selecting nth element (n>=0) (counting from front):

   (len_select ($1 %elem $2) %nseq %elem)<
     (=length ($1) %nseq).

     ! -- somewhat analogous to the member relation

selecting nth element counting from end:

   (len_select\ ($1 %elem $2) %nseq %elem)<
     (=length ($2) %nseq).

prefix ending before nth element:

   (len_prefix ($1 $2) %nseq ($1))<
     (=length ($1) %nseq).

prefix ending with nth element from end:

   (len_prefix\ ($1 $2) %nseq ($1))<
     (=length ($2) %nseq). 

suffix beginning with nth element:

   (len_suffix ($1 $2) %nseq ($2))<
     (=length ($1) %nseq).

suffix beginning after nth element from end:

   (len_suffix\ ($1 $2) %nseq ($2))<
     (=length ($2) %nseq).

-- Note that the patterns here would allow combining these axioms.

*** substr variations  -- to be done

search  (for an element -- return index as seq of some length)