! sort.ax - axioms for sorting program
!
!   (Program <input_file> <output_file>)
!
!   lines of input file are sorted and written to output file

! defining the sorting program

   (Program %infile %outfile)<
     (charstr_seq %infile),       ! only applies to sequence of char strings
     (sort %infile %outfile).
 
! sort function - sort a sequence of character strings

   (sort %seq %sorted_seq)<       ! sorted sequence is an ordered permutation
     (permutation %seq %sorted_seq),
     (ordered %sorted_seq).

! permutation - permutation relation on sequences

   (permutation () ()).
   (permutation (% $) ($1 % $2))< (permutation ($) ($1 $2)).

! ordered - sequence is ordered (based on a default ordering relation)

   (ordered ()).        ! empty sequence is ordered
   (ordered (%)).       ! single element sequence is ordered
   (ordered (% %1 $))<   ! adding element to ordered sequence
     (ordered (%1 $)),
     (<= % %1).

! < - ordering relation on bits, characters, & character sequences

   (< `0 `1).             ! ordering of bit atoms

   (< ($) ($ %x $x)).      ! lexicographic ordering of sequences
   (< ($ %1 $1) ($ %2 $2))< (< %1 %2).

! <= relation

   (<= % %).                ! identical elements are ordered
   (<= %1 %2)< (< %1 %2).

! charstr_seq - sequence of character strings

   (charstr_seq ()).
   (charstr_seq (%chstr $chstrs))< (charstr %chstr), (charstr_seq ($chstrs)).

! charstr - string (sequence) of characters

   (charstr ()).
   (charstr (%char $chars))< (char %char), (charstr ($chars)).

! char - definition of characters
! example:  'A'  ==  (`char (`0 `1 `0 `0 `0 `0 `0 `1))   (syntactic shorthand)

   (char (`char %8bitseq))<            ! 8-bit characters
     (bit_seq %8bitseq),
     (=len %8bitseq (* * * *  * * * *)).

! bit_seq - sequence of bit atoms

   (bit_seq ()).
   (bit_seq (%bit $bits))< (bit %bit), (bit_seq ($bits)).

! bit - definition of bit atoms

   (bit `0).
   (bit `1).

! =len - sequences of equal length

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