! natnum.txt - utility predicates for natural numbers in successor notation
!/ predicates:
  (num <num>) - set of natural numbers in successor notation
  (plus <n1> <n2> <sum>) - sum of natural numbers
  (times <n1> <n2> <prod>) - product of natural numbers
  (length <seq> <len>) - length of a sequence as a natural number
  (ord <set> <elem> <n>) - ordinal number of a finite set element
  ((< num) <n1> <n2>) - < order of natural numbers (see relation.txt: <= > ..)
  (iota <n> <0..n>) - sequence of numbers from 0-n

  We represent natural numbers 0,1,2,... as (`z), (`s `z), (`s `s `z), ....
  (We use `z instead of `0 to make distinct from bit-atom `0.)
!\

! num - set of natural numbers in successor notation

  (num (`z)).           ! zero is a natural number
  (num (`s $n))<        ! successor of n is a natural number,
    (num ($n)).         ! if n is a natural number

! plus - addition of natural numbers

  (plus %n (`z) %n)< (num %n).       ! n + 0 = n
  (plus %1 (`s $2) (`s $3))<         ! n1 + n2+1 = n3+1
    (plus %1 ($2) ($3)).             ! if n1 + n2 = n3

! times - multiplication of natural numbers

  (times %n (`z) (`z))< (num %n).    ! n * 0 = 0
  (times %1 (`s $2) %3')<            ! n1 * n2+1 = n3'
    (times %1 ($2) %3),              ! if n1 * n2 = n3
    (plus %3 %1 %3').                ! and n3 + n1 = n3'

! length - length of a sequence

  (length () (`z)).           ! empty sequence has length zero
  (length (% $) (`s $l))<     ! adding element increments length
    (length ($) ($l)).

! select - select the ith element of a sequence (indexed from 0)

  (select %k ($1 % $2) %)<
    (length ($1) %k).

! ord - ordinal number of a finite set element

  (ord %setname %elem %n)<
    (finite_set %setname ($1 %elem $2)),   ! (set elems must be unique)
    (length ($1) %n).
  ! -- <setname> may not be needed in some cases?

! (< num) - < on natural numbers

  ((< num) (`z) (`s $n))< (num ($n)).
  ((< num) (`s $n1) (`s $n2))< ((< num) ($n1) ($n2)).

  ! see relation.txt for other relational operations <= > >= /= =

! iota - sequence of natural numbers from 0 thru n (APL function name)
! (iota <n> <0..n>)

  (iota (`z) ((`z))).
  (iota (`s $n) ($0..n (`s $n)))<
    (iota ($n) ($0..n)).

  ! -- see eval.txt for versions where <n> and <0..n> are decimal symbols