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• ∃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 • 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

privacy policy

Created:

V