The Theory %nat%

Parents

pair

Children

list

Constants

Is_ℕ_Rep	IND → BOOL
Zero	ℕ
Suc	ℕ → ℕ
$+	ℕ → ℕ → ℕ
$≤	ℕ → ℕ → 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

Created: