spec Nat =

  free type Nat ::= 0 | suc(pre:? Nat)
 
  preds   __ <= __, __ < __,
          __ >= __, __ > __: Nat * Nat;
          odd, even: Nat

  ops   __ + __, __ * __: Nat * Nat -> Nat;
        __ ^ __: Nat * Nat -> Nat;
        min, max: Nat * Nat ->  Nat;
        +__: Nat -> Nat;
        abs: Nat -> Nat;
        __! :    Nat -> Nat;
        __ -?__: Nat * Nat ->? Nat;
        __ /? __: Nat * Nat ->? Nat;
        __ div __, __ mod __ , __ quot __, __ rem __ :Nat * Nat ->? Nat;

%%   Operations to represent natural numbers with digits:
           1,2,3,4,5,6,7,8,9: Nat;
           __ @@ __ :         Nat * Nat -> Nat 
     
     forall m,n,r,s: Nat

     . 0 <= n                           %(Nat_leq_def1)%
     . not (suc(n) <= 0)                %(Nat_leq_def2)%
     . suc(m) <= suc(n) <=> m <= n      %(Nat_leq_def3)%

     . m >= n <=> n <= m                %(Nat_geq_def)%
     . m < n <=> (m <= n /\ not (m=n))  %(Nat_less_def)%
     . m > n <=> m < n                  %(Nat_greater_def)%
   
     . 0 + m = m                        %(Nat_add_0)%
     . suc(n) + m = suc(n + m)          %(Nat_add_suc)%

     . 0 * m = 0                        %(Nat_mult_0)%
     . suc(n) * m = (n * m) + m         %(Nat_mult_suc)%

     . m ^ 0 = 1                        %(Nat_power_0)%
     . m ^ suc(n)  = m * m ^ n          %(Nat_power_suc)%

     . min(m,n) = m when m <= n else n  %(Nat_min_def)%
     . max(m,n) = n when m <= n else m  %(Nat_max_def)%

     . + m = m                          %(plus_def)%

     . abs(n) = n                       %(Nat_abs)%

     . odd(m) <=> not even(m)           %(Nat_odd_def)%
     . even(0)                          %(Nat_even_0)%
     . even(suc(m)) <=> odd(m)          %(Nat_even_suc)%

     . 0! = 1                           %(Nat_factorial_0)%
     . suc(n)! =suc(n)*n!               %(Nat_factorial_suc)%

     . m -? n = r <=> m = r + n         %(Nat_sub_def)%

     . not def(m /? 0)                      %(Nat_divide_0)%
     . ( m /? n = r <=> m = r * n ) if n>0  %(Nat_divide_Pos)%

     . m div n = r <=> 
       (exists s: Nat . m = n*r + s /\ s < n)  %(Nat_div)%
     . m mod n = s <=> 
       (exists r: Nat . m = n*r + s /\ s < n)  %(Nat_mod)%
     . m quot n = m div n                      %(Nat_quot)%
     . m rem n = m mod n                       %(Nat_rem)%

     . 1 = suc (0)                      %(Nat_1_def)%
     . 2 = suc (1)                      %(Nat_2_def)%
     . 3 = suc (2)                      %(Nat_3_def)%
     . 4 = suc (3)                      %(Nat_4_def)%
     . 5 = suc (4)                      %(Nat_5_def)%
     . 6 = suc (5)                      %(Nat_6_def)%
     . 7 = suc (6)                      %(Nat_7_def)%
     . 8 = suc (7)                      %(Nat_8_def)%
     . 9 = suc (8)                      %(Nat_9_def)%
     . m @@ n = (m * suc(9)) + n        %(Nat_decimal_def)%

then %def
     sort Pos = { p: Nat . p > 0 }
     op    1: Pos = suc(0) as Pos;      %(Nat_1_as_Pos_def)%
           __*__: Pos * Pos -> Pos;
           __+__: Pos * Nat -> Pos;
           __+__: Nat * Pos -> Pos;
	   suc: Nat -> Pos

then %implies

     ops min, max: Nat * Nat -> Nat, comm, assoc

     forall x,m,n,r,s,t: Nat; p: Pos
     . def(m-?n) <=> m >= n             %(Nat_sub_dom)%
     . def(m /? n) <=> m mod n = 0      %(Nat_divide_dom)%
     . def ( m div n ) <=> not (n=0)    %(Nat_div_dom)%
     . def ( m mod n ) <=> not (n=0)    %(Nat_mod_dom)%
     . def ( m quot n ) <=> not (n=0)   %(Nat_quot_dom)%
     . def ( m rem n ) <=> not (n=0)    %(Nat_rem_dom)%
     . (r + s) * t = (r * t) + (s * t)  %(Nat_distr)%
     . max(m,0)=m                       %(Nat_max_unit)%      
     . min(m,0)=0                       %(Nat_min_0)% 
end