The Theory %nat%

Parents

pair

Children

list

Constants

Is__Rep	IND BOOL
Suc
Zero
$+
$	BOOL
$	BOOL
$<	BOOL
$>	BOOL
$*
$Mod
$Div
$-

Types

Fixity

Left Infix 305:

-

Left Infix 315:

Div

Mod

Right Infix 210:

<

>

Right Infix 300:

+

Right Infix 310:

*

Definitions

Is__Rep is__rep_def	zero suc (Is__Rep zero ( n Is__Rep n Is__Rep (suc n))) ( n Is__Rep n suc n = zero) OneOne suc ( p p zero ( m p m p (suc m)) ( n Is__Rep n p n))
_def	f TypeDefn Is__Rep f
Zero Suc zero_suc_def	( n Suc n = Zero) OneOne Suc ( p p Zero ( m p m p (Suc m)) ( n p n))
+ plus_def	m n 0 + n = n (m + 1) + n = (m + n) + 1 Suc m = m + 1
_def	m n m n ( i m + i = n)
_def	m n m n n m
< less_def	m n m < n m + 1 n
> greater_def	m n m > n n < m
* times_def	m n 0 * n = 0 (m + 1) * n = m * n + n
Mod mod_def	m n 0 < n 0 Mod n = 0 (m + 1) Mod n = (if m Mod n + 1 < n then m Mod n + 1 else 0)
Div div_def	m n 0 < n 0 Div n = 0 (m + 1) Div n = (if m Mod n + 1 < n then m Div n else m Div n + 1)
- minus_def	m n (m + n) - n = m

Theorems

induction_thm	p p 0 ( m p m p (m + 1)) ( n p n)
_plus1_thm	n n + 1 = 0
one_one_plus1_thm	x1 x2 x1 + 1 = x2 + 1 x1 = x2
prim_rec_thm	z s ₁ f f 0 = z ( n f (n + 1) = s (f n) n)
plus_assoc_thm	i m n (i + m) + n = i + m + n
plus_assoc_thm1	i m n i + m + n = (i + m) + n
plus_comm_thm	m n m + n = n + m
plus_order_thm	i m n m + i = i + m (i + m) + n = i + m + n m + i + n = i + m + n
plus_clauses	m n i (m + i = n + i m = n) (i + m = n + i m = n) (m + i = i + n m = n) (i + m = i + n m = n) (m + i = i m = 0) (i + m = i m = 0) (i = i + n n = 0) (i = n + i n = 0) (m + i = 0 m = 0 i = 0) (0 = m + i m = 0 i = 0) (m + 0 = m 0 + m = m) 1 = 0 0 = 1
_trans_thm	m i n m i i n m n
less_trans_thm	m i n m < i i < n m < n
_clauses	m n i (m + i n + i m n) (i + m n + i m n) (m + i i + n m n) (i + m i + n m n) (m + i i m = 0) (i + m i m = 0) (m + i 0 m = 0 i = 0) (m 0 m = 0) m m + i m i + m m m 0 m 1 0
less_clauses	m n i (m + i < n + i m < n) (i + m < n + i m < n) (m + i < i + n m < n) (i + m < i + n m < n) (m < m + i 0 < i) (m < i + m 0 < i) m + i < m m + i < i m < 0 m < m 0 < m + 1 0 < 1 + m 0 < 1
_cases_thm	m m = 0 ( i m = i + 1)
_cases_thm	m n m n n m
_plus1_thm	m n m n + 1 m = n + 1 m n
plus1__thm	m n m + 1 n m n m = n
_plus1__thm	m n m + 1 n n m
less_cases_thm	m n m < n m = n n < m
_less_plus1_thm	m n m < n + 1 n < m
less_plus1_thm	m n m < n + 1 m = n m < n
plus1_less_thm	m n m + 1 < n m < n m + 1 = n
_antisym_thm	m n m n n m m = n
less_irrefl_thm	m n (m < n n < m)
cov_induction_thm	p ( n ( m m < n p m) p n) ( n p n)
less_well_order_thm	p ( i p i) ( m p m ( i p i i < m))
_less_thm	m n m < n n m
__thm	m n m n n < m
_well_order_thm	p ( i p i) ( m p m ( i p i m i))
_least_upper_bound_thm	p ( i p i) ( n j p j j n) ( m p m ( j p j j m))
minimum__thm	p b p 0 p b ( m ( n n m p n) p (m + 1))
times_comm_thm	m n m * n = n * m
times_assoc_thm	i m n (i * m) * n = i * m * n
times_plus_distrib_thm	i m n (i + m) * n = i * n + m * n i * (m + n) = i * m + i * n
times_clauses	m m * 0 = 0 0 * m = 0 m * 1 = m 1 * m = m
mod_less_thm	m n 0 < n m Mod n < n
div_mod_thm	m n 0 < n m = m Div n * n + m Mod n
div_mod_unique_thm	m n d r r < n m = d * n + r d = m Div n r = m Mod n
minus_clauses	m n m - m = 0 m - 0 = m (m + n) - n = m (m + n) - m = n

V