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
fill• (Is_ℕ_Rep zero
fill∧ (∀ n• Is_ℕ_Rep n ⇒ Is_ℕ_Rep (suc n)))
fill∧ (∀ n• Is_ℕ_Rep n ⇒ ¬ suc n = zero)
fill∧ OneOne suc
fill∧ (∀ p
fill• p zero ∧ (∀ m• p m ⇒ p (suc m))
fill⇒ (∀ n• Is_ℕ_Rep n ⇒ p n))
ℕ_def
⊢ ∃ f• TypeDefn Is_ℕ_Rep f
Zero
Suc
zero_suc_def
⊢ (∀ n• ¬ Suc n = Zero)
fill∧ OneOne Suc
fill∧ (∀ p
fill• p Zero ∧ (∀ m• p m ⇒ p (Suc m)) ⇒ (∀ n• p n))
+
plus_def
⊢ ∀ m n
fill• 0 + n = n
fill∧ (m + 1) + n = (m + n) + 1
fill∧ 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
fill• 0 < n
fill⇒ 0 Mod n = 0
fill∧ (m + 1) Mod n
fill= (if m Mod n + 1 < n
fillthen m Mod n + 1
fillelse 0)
Div
div_def
⊢ ∀ m n
fill• 0 < n
fill⇒ 0 Div n = 0
fill∧ (m + 1) Div n
fill= (if m Mod n + 1 < n
fillthen m Div n
fillelse 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• ∃1 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
fill• m + i = i + m
fill∧ (i + m) + n = i + m + n
fill∧ m + i + n = i + m + n
plus_clauses
⊢ ∀ m n i
fill• (m + i = n + i ⇔ m = n)
fill∧ (i + m = n + i ⇔ m = n)
fill∧ (m + i = i + n ⇔ m = n)
fill∧ (i + m = i + n ⇔ m = n)
fill∧ (m + i = i ⇔ m = 0)
fill∧ (i + m = i ⇔ m = 0)
fill∧ (i = i + n ⇔ n = 0)
fill∧ (i = n + i ⇔ n = 0)
fill∧ (m + i = 0 ⇔ m = 0 ∧ i = 0)
fill∧ (0 = m + i ⇔ m = 0 ∧ i = 0)
fill∧ (m + 0 = m ∧ 0 + m = m)
fill∧ ¬ 1 = 0
fill∧ ¬ 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
fill• (m + i ≤ n + i ⇔ m ≤ n)
fill∧ (i + m ≤ n + i ⇔ m ≤ n)
fill∧ (m + i ≤ i + n ⇔ m ≤ n)
fill∧ (i + m ≤ i + n ⇔ m ≤ n)
fill∧ (m + i ≤ i ⇔ m = 0)
fill∧ (i + m ≤ i ⇔ m = 0)
fill∧ (m + i ≤ 0 ⇔ m = 0 ∧ i = 0)
fill∧ (m ≤ 0 ⇔ m = 0)
fill∧ m ≤ m + i
fill∧ m ≤ i + m
fill∧ m ≤ m
fill∧ 0 ≤ m
fill∧ ¬ 1 ≤ 0
less_clauses
⊢ ∀ m n i
fill• (m + i < n + i ⇔ m < n)
fill∧ (i + m < n + i ⇔ m < n)
fill∧ (m + i < i + n ⇔ m < n)
fill∧ (i + m < i + n ⇔ m < n)
fill∧ (m < m + i ⇔ 0 < i)
fill∧ (m < i + m ⇔ 0 < i)
fill∧ ¬ m + i < m
fill∧ ¬ m + i < i
fill∧ ¬ m < 0
fill∧ ¬ m < m
fill∧ 0 < m + 1
fill∧ 0 < 1 + m
fill∧ 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
fill• (∃ i• p i) ∧ (∃ n• ∀ j• p j ⇒ j ≤ n)
fill⇔ (∃ m• p m ∧ (∀ j• p j ⇒ j ≤ m))
minimum_¬_thm
⊢ ∀ p b
fill• p 0 ∧ ¬ p b
fill⇒ (∃ 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
fill• (i + m) * n = i * n + m * n
fill∧ 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
fill• r < n ⇒ m = d * n + r ⇒ d = m Div n ∧ r = m Mod n
minus_clauses
⊢ ∀ m n
fill• m - m = 0
fill∧ m - 0 = m
fill∧ (m + n) - n = m
fill∧ (m + n) - m = n

up quick index

privacy policy

Created:

V