Lines Matching defs:Nat
24 \section*{Numbers.Nat}
26 sorts Nat, Pos
27 sorts Pos < Nat
28 op 0 : Nat
29 op 1 : Nat
31 op 2 : Nat
32 op 3 : Nat
33 op 4 : Nat
34 op 5 : Nat
35 op 6 : Nat
36 op 7 : Nat
37 op 8 : Nat
38 op 9 : Nat
39 op __! : Nat -> Nat
40 op __*__ : Nat * Nat -> Nat
42 op __+__ : Nat * Nat -> Nat
43 op __+__ : Nat * Pos -> Pos
44 op __+__ : Pos * Nat -> Pos
45 op __-!__ : Nat * Nat -> Nat
46 op __-?__ : Nat * Nat ->? Nat
47 op __/?__ : Nat * Nat ->? Nat
48 op __@@__ : Nat * Nat -> Nat
49 op __^__ : Nat * Nat -> Nat
50 op __div__ : Nat * Nat ->? Nat
51 op __mod__ : Nat * Nat ->? Nat
52 op max : Nat * Nat -> Nat
53 op min : Nat * Nat -> Nat
54 op pre : Nat ->? Nat
55 op suc : Nat -> Nat
56 op suc : Nat -> Pos
57 pred __<__ : Nat * Nat
58 pred __<=__ : Nat * Nat
59 pred __>__ : Nat * Nat
60 pred __>=__ : Nat * Nat
61 pred even : Nat
62 pred odd : Nat
65 forall X1:Nat . pre(suc(X1)) = X1 %(ga_selector_pre)%
67 forall X1:Nat; Y1:Nat
70 forall Y1:Nat . not 0 = suc(Y1) %(ga_disjoint_0_suc)%
74 generated{sort Nat; op 0 : Nat;
75 op suc : Nat -> Nat} %(ga_generated_Nat)%
95 forall m:Nat; n:Nat . m @@ n = (m * suc(9)) + n %(decimal_def)%
97 forall x:Nat; y:Nat . x + y = y + x %(ga_comm___+__)%
99 forall x:Nat; y:Nat; z:Nat
102 forall x:Nat . x + 0 = x %(ga_right_unit___+__)%
104 forall x:Nat . 0 + x = x %(ga_left_unit___+__)%
106 forall x:Nat; y:Nat . x * y = y * x %(ga_comm___*__)%
108 forall x:Nat; y:Nat; z:Nat
111 forall x:Nat . x * 1 = x %(ga_right_unit___*__)%
113 forall x:Nat . 1 * x = x %(ga_left_unit___*__)%
115 forall x:Nat; y:Nat . min(x, y) = min(y, x) %(ga_comm_min)%
117 forall x:Nat; y:Nat; z:Nat
120 forall x:Nat; y:Nat . max(x, y) = max(y, x) %(ga_comm_max)%
122 forall x:Nat; y:Nat; z:Nat
125 forall x:Nat . max(x, 0) = x %(ga_right_unit_max)%
127 forall x:Nat . max(0, x) = x %(ga_left_unit_max)%
129 forall m, n, r, s, t:Nat . 0 <= n %(leq_def1_Nat)%
131 forall m, n, r, s, t:Nat . not suc(n) <= 0 %(leq_def2_Nat)%
133 forall m, n, r, s, t:Nat
136 forall m, n, r, s, t:Nat . m >= n <=> n <= m %(geq_def_Nat)%
138 forall m, n, r, s, t:Nat
141 forall m, n, r, s, t:Nat . m > n <=> n < m %(greater_def_Nat)%
143 forall m, n, r, s, t:Nat . even(0) %(even_0_Nat)%
145 forall m, n, r, s, t:Nat . even(suc(m)) <=> odd(m) %(even_suc_Nat)%
147 forall m, n, r, s, t:Nat . odd(m) <=> not even(m) %(odd_def_Nat)%
149 forall m, n, r, s, t:Nat . 0 ! = 1 %(factorial_0)%
151 forall m, n, r, s, t:Nat
154 forall m, n, r, s, t:Nat . 0 + m = m %(add_0_Nat)%
156 forall m, n, r, s, t:Nat . suc(n) + m = suc(n + m) %(add_suc_Nat)%
158 forall m, n, r, s, t:Nat . 0 * m = 0 %(mult_0_Nat)%
160 forall m, n, r, s, t:Nat
163 forall m, n, r, s, t:Nat . m ^ 0 = 1 %(power_0_Nat)%
165 forall m, n, r, s, t:Nat
168 forall m, n, r, s, t:Nat
171 forall m, n, r, s, t:Nat
174 forall m, n, r, s, t:Nat
177 forall m, n, r, s, t:Nat
180 forall m, n, r, s, t:Nat . def m -? n <=> m >= n %(sub_dom_Nat)%
182 forall m, n, r, s, t:Nat . m -? n = r <=> m = r + n %(sub_def_Nat)%
184 forall m, n, r, s, t:Nat
187 forall m, n, r, s, t:Nat . not def m /? 0 %(divide_0_Nat)%
189 forall m, n, r, s, t:Nat
192 forall m, n, r, s, t:Nat
195 forall m, n, r, s, t:Nat
197 exists s:Nat . m = (n * r) + s /\ s < n %(div_Nat)%
199 forall m, n, r, s, t:Nat
202 forall m, n, r, s, t:Nat
204 exists r:Nat . m = (n * r) + s /\ s < n %(mod_Nat)%
206 forall m, n, r, s, t:Nat
209 forall m, n, r, s, t:Nat
212 forall p:Nat . (p in Pos) <=> p > 0
216 forall m, n, r, s:Nat . min(m, 0) = 0 %(min_0)%
218 forall m, n, r, s:Nat
221 forall m, n, r, s:Nat