spec Nat = sorts Pos < Nat; Pos ops +__ : Nat->Nat; 0 : Nat; 1 : Pos; 1 : Nat; 2 : Nat; 3 : Nat; 4 : Nat; 5 : Nat; 6 : Nat; 7 : Nat; 8 : Nat; 9 : Nat; __! : Nat->Nat; __*__ : Pos*Pos->Pos; __*__ : Nat*Nat->Nat; __+__ : Pos*Nat->Pos; __+__ : Nat*Pos->Pos; __+__ : Nat*Nat->Nat; __-?__ : Nat*Nat->?Nat; __/?__ : Nat*Nat->?Nat; __@@__ : Nat*Nat->Nat; __^__ : Nat*Nat->Nat; __div__ : Nat*Nat->?Nat; __mod__ : Nat*Nat->?Nat; __quot__ : Nat*Nat->?Nat; __rem__ : Nat*Nat->?Nat; abs : Nat->Nat; inf : Nat*Nat->?Nat; max : Nat*Nat->Nat; min : Nat*Nat->Nat; pre : Nat->?Nat; suc : Nat->Nat; sup : Nat*Nat->?Nat preds __<=__ : Nat*Nat; __<__ : Nat*Nat; __>=__ : Nat*Nat; __>__ : Nat*Nat; even : Nat; odd : Nat vars x : Nat;n : Pos . %[SemiGroup_power_1] ( x ^ 1 ) = x vars x : Nat;n : Pos . %[SemiGroup_power_suc] ( x ^ suc(n) as Pos ) = ( x * ( x ^ n ) ) vars x : Nat;n : Pos;m : Pos . %[Power_add] ( x ^ ( n * m ) ) = ( ( x ^ n ) * ( x ^ m ) ) vars x : Nat;n : Pos;m : Pos . %[Power_mult] ( x ^ ( n * m ) ) = ( ( x ^ n ) ^ m ) generated { sorts Nat ops 0 : Nat; suc : Nat->Nat } vars X0 : Nat . %[_selector,pre] X0 = pre(suc(X0)) vars Y0 : Nat . %[_disjoint,0,suc] not 0 = suc(Y0) vars X0 : Nat;Y0 : Nat . %[_injective,suc] suc(X0) = suc(Y0) => X0 = Y0 vars x : Nat;y : Nat . %[SigOrder_geq_def] ( x >= y ) <=> ( y <= x ) vars x : Nat;y : Nat . %[SigOrder_less_def] ( x < y ) <=> ( x <= y ) /\ not x = y vars x : Nat;y : Nat . %[SigOrder_greater_def] ( x > y ) <=> ( y < x ) vars m : Nat;n : Nat . %[Nat_leq_def1] ( 0 <= n ) vars m : Nat;n : Nat . %[Nat_leq_def2] not ( suc(n) <= 0 ) vars m : Nat;n : Nat . %[Nat_leq_def3] ( suc(m) <= suc(n) ) <=> ( m <= n ) vars m : Nat;n : Nat . %[Nat_add__0] ( 0 + m ) = m vars m : Nat;n : Nat . %[Nat_add_suc] ( suc(n) + m ) = suc(( n + m )) vars m : Nat;n : Nat . %[Nat_mult_0] ( 0 * m ) = 0 vars m : Nat;n : Nat . %[Nat_mult_suc] ( suc(n) * m ) = ( ( n * m ) + m ) vars p : Nat . %[_subsort_defn_defn,Pos] p in Pos <=> ( p > 0 ) axiom %[_op_defn,1] 1 = suc(0) as Pos vars x : Nat;y : Nat;z : Nat . %[_assoc,__*__] ( x * ( y * z ) ) = ( ( x * y ) * z ) vars x : Nat . %[Monoid_power_0] ( x ^ 0 ) = 1 vars x : Nat;n : Nat;m : Nat . %[Monoid_power_unit] ( 1 ^ n ) = 1 vars x : Nat;n : Nat;m : Nat . %[Power_add] ( x ^ ( n + m ) ) = ( ( x ^ n ) * ( x ^ m ) ) vars x : Nat;n : Nat;m : Nat . %[Power_mult] ( x ^ ( n * m ) ) = ( ( x ^ n ) ^ m ) vars x : Nat . %[_right_unit,__*__] ( x * 1 ) = x vars x : Nat . %[_left_unit,__*__] ( 1 * x ) = x vars x : Nat;y : Nat;n : Nat . %[Power_basemult] ( ( x ^ n ) * ( y ^ n ) ) = ( ( x * y ) ^ n ) vars x : Nat;n : Pos . %[SemiGroup_power_1] ( x * 1 ) = x vars x : Nat;n : Pos . %[SemiGroup_power_suc] ( x * suc(n) as Pos ) = ( x * ( x * n ) ) vars x : Nat;n : Pos;m : Pos . %[Power_add] ( x * ( n * m ) ) = ( ( x * n ) * ( x * m ) ) vars x : Nat;n : Pos;m : Pos . %[Power_mult] ( x * ( n * m ) ) = ( ( x * n ) * m ) vars x : Nat . %[Monoid_power_0] ( x * 0 ) = 0 vars x : Nat;n : Nat;m : Nat . %[Monoid_power_unit] ( 0 * n ) = 0 vars x : Nat;n : Nat;m : Nat . %[Power_add] ( x * ( n + m ) ) = ( ( x * n ) * ( x * m ) ) vars x : Nat;n : Nat;m : Nat . %[Power_mult] ( x * ( n * m ) ) = ( ( x * n ) * m ) vars x : Nat . %[_right_unit,__*__] ( x * 0 ) = x vars x : Nat . %[_left_unit,__*__] ( 0 * x ) = x vars x : Nat;y : Nat;n : Nat . %[Power_basemult] ( ( x * n ) * ( y * n ) ) = ( ( x * y ) * n ) vars x : Nat;y : Nat;z : Nat . %[inf_def] inf(x,y) = z <=> ( z <= x ) /\ ( z <= y ) /\ forall t : Nat . ( t <= x ) /\ ( t <= y ) => ( t <= z ) vars x : Nat;y : Nat;z : Nat . %[sup_def] sup(x,y) = z <=> ( x <= z ) /\ ( y <= z ) /\ forall t : Nat . ( x <= t ) /\ ( y <= t ) => ( z <= t ) vars x : Nat;y : Nat . %[_comm,inf] inf(x,y) = inf(y,x) vars x : Nat;y : Nat . %[_comm,sup] sup(x,y) = sup(y,x) vars x : Nat . %[refl] ( x <= x ) vars x : Nat;y : Nat;z : Nat . %[trans] ( x <= y ) /\ ( y <= z ) => ( x <= z ) vars x : Nat;y : Nat . %[POrder_antisym] ( x <= y ) /\ ( y <= x ) => x = y vars x : Nat;y : Nat . %[min_def] min(x,y) = x when ( x <= y ) else y vars x : Nat;y : Nat . %[max_def] max(x,y) = y when ( x <= y ) else x vars x : Nat;y : Nat . %[_comm,min] min(x,y) = min(y,x) vars x : Nat;y : Nat . %[_comm,max] max(x,y) = max(y,x) vars x : Nat;y : Nat;z : Nat . %[_assoc,min] min(x,min(y,z)) = min(min(x,y),z) vars x : Nat;y : Nat;z : Nat . %[_assoc,max] max(x,max(y,z)) = max(max(x,y),z) vars x : Nat;y : Nat . %[min_inf_relation] min(x,y) = inf(x,y) vars x : Nat;y : Nat . %[max_sup_relation] max(x,y) = sup(x,y) vars x : Nat . %[plus_def] (+ x ) = x vars m : Nat;n : Nat;r : Nat;s : Nat;p : Pos . %[Nat_abs] abs(n) = n vars m : Nat;n : Nat;r : Nat;s : Nat;p : Pos . %[Nat_odd_def] odd(m) <=> not even(m) vars m : Nat;n : Nat;r : Nat;s : Nat;p : Pos . %[Nat_even_zero] even(0) vars m : Nat;n : Nat;r : Nat;s : Nat;p : Pos . %[Nat_even_suc] even(suc(m)) <=> odd(m) vars m : Nat;n : Nat;r : Nat;s : Nat;p : Pos . %[Nat_factorial_zero] ( 0 !) = 1 vars m : Nat;n : Nat;r : Nat;s : Nat;p : Pos . %[Nat_factorial_suc] ( suc(n) !) = ( suc(n) * ( n !) ) vars m : Nat;n : Nat;r : Nat;s : Nat;p : Pos . %[Nat_sub_def] ( m -? n ) = r <=> m = ( r + n ) vars m : Nat;n : Nat;r : Nat;s : Nat;p : Pos . %[Nat_divide_0] not def ( m /? 0 ) vars m : Nat;n : Nat;r : Nat;s : Nat;p : Pos . %[Nat_divide_Pos] ( n > 0 ) => ( m /? n ) = r <=> m = ( r * n ) vars m : Nat;n : Nat;r : Nat;s : Nat;p : Pos . %[Nat_div] ( m div n ) = r <=> exists s : Nat . m = ( ( n * r ) + s ) /\ ( s < n ) vars m : Nat;n : Nat;r : Nat;s : Nat;p : Pos . %[Nat_mod] ( m mod n ) = s <=> exists r : Nat . m = ( ( n * r ) + s ) /\ ( s < n ) vars m : Nat;n : Nat;r : Nat;s : Nat;p : Pos . %[Nat_quot] ( m quot n ) = ( m div n ) vars m : Nat;n : Nat;r : Nat;s : Nat;p : Pos . %[Nat_rem] ( m rem n ) = ( m mod n ) vars m : Nat;n : Nat . %[Nat_1_def] 1 = suc(0) vars m : Nat;n : Nat . %[Nat_2_def] 2 = suc(1) vars m : Nat;n : Nat . %[Nat_3_def] 3 = suc(2) vars m : Nat;n : Nat . %[Nat_4_def] 4 = suc(3) vars m : Nat;n : Nat . %[Nat_5_def] 5 = suc(4) vars m : Nat;n : Nat . %[Nat_6_def] 6 = suc(5) vars m : Nat;n : Nat . %[Nat_7_def] 7 = suc(6) vars m : Nat;n : Nat . %[Nat_8_def] 8 = suc(7) vars m : Nat;n : Nat . %[Nat_9_def] 9 = suc(8) vars m : Nat;n : Nat . %[Nat_decimal_def] ( m @@ n ) = ( ( m * suc(9) ) + n ) vars m : Nat;n : Nat;r : Nat;s : Nat;t : Nat;p : Pos . %[Nat_sub_dom] def ( m -? n ) <=> ( m >= n ) vars m : Nat;n : Nat;r : Nat;s : Nat;t : Nat;p : Pos . %[Nat_divide_dom] def ( m /? n ) <=> ( m mod n ) = 0 vars m : Nat;n : Nat;r : Nat;s : Nat;t : Nat;p : Pos . %[Nat_div_dom] def ( m div n ) <=> not n = 0 vars m : Nat;n : Nat;r : Nat;s : Nat;t : Nat;p : Pos . %[Nat_mod_dom] def ( m mod n ) <=> not n = 0 vars m : Nat;n : Nat;r : Nat;s : Nat;t : Nat;p : Pos . %[Nat_quot_dom] def ( m quot n ) <=> not n = 0 vars m : Nat;n : Nat;r : Nat;s : Nat;t : Nat;p : Pos . %[Nat_rem_dom] def ( m rem n ) <=> not n = 0 vars m : Nat;n : Nat;r : Nat;s : Nat;t : Nat;p : Pos . %[Nat_max_unit] max(m,0) = m vars m : Nat;n : Nat;r : Nat;s : Nat;t : Nat;p : Pos . %[Nat_distr] ( ( r + s ) * t ) = ( ( r * t ) + ( s * t ) ) end