! natnum.txt - utility predicates for natural numbers in successor notation !/ predicates: (num ) - set of natural numbers in successor notation (plus ) - sum of natural numbers (times ) - product of natural numbers (length ) - length of a sequence as a natural number (ord ) - ordinal number of a finite set element ((< num) ) - < order of natural numbers (see relation.txt: <= > ..) (iota <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). ! -- 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 <0..n>) (iota (`z) ((`z))). (iota (`s \$n) (\$0..n (`s \$n)))< (iota (\$n) (\$0..n)). ! -- see eval.txt for versions where and <0..n> are decimal symbols