The Theory dyadic
 Parents
 ℤ
 Children
 ℝ
 Constants
 \$^ ℕ → ℕ → ℕ \$dy_times DYADIC → DYADIC → DYADIC dy_one DYADIC \$dy_exp DYADIC → ℕ → DYADIC \$dy_less DYADIC → DYADIC → BOOL
 Type_Abbreviations
 DYADIC DYADIC
 Fixity
 Right Infix 210: dy_less Right Infix 310: dy_exp dy_times Right Infix 320: ^
 Definitions
 ^ ⊢ (∀ i• i ^ 0 = 1) ∧ (∀ i m• i ^ (m + 1) = i * i ^ m) dy_times ⊢ ∀ (m, i) (n, j) • (m, i) dy_times (n, j) = (2 * m * n + m + n, i + j) dy_one ⊢ dy_one = (0, ℕℤ 0) dy_exp ⊢ (∀ x• x dy_exp 0 = dy_one) ∧ (∀ x m• x dy_exp (m + 1) = x dy_times x dy_exp m) dy_less ⊢ ∀ (m, i) (n, j) • (m, i) dy_less (n, j) ⇔ (∃ a b • ℕℤ a + i = ℕℤ b + j ∧ 2 ^ a * (2 * m + 1) < 2 ^ b * (2 * n + 1))
 Theorems
 dy_less_irrefl_thm ⊢ ∀ x• ¬ x dy_less x dy_less_antisym_thm ⊢ ∀ x y• ¬ (x dy_less y ∧ y dy_less x) dy_less_trans_thm ⊢ ∀ x y z• x dy_less y ∧ y dy_less z ⇒ x dy_less z dy_less_trich_thm ⊢ ∀ x y• ¬ x = y ⇒ x dy_less y ∨ y dy_less x dy_times_comm_thm ⊢ ∀ x y• x dy_times y = y dy_times x dy_times_assoc_thm ⊢ ∀ x y z • (x dy_times y) dy_times z = x dy_times y dy_times z dy_times_order_thm ⊢ ∀ u x y • x dy_times u = u dy_times x ∧ (u dy_times x) dy_times y = u dy_times x dy_times y ∧ x dy_times u dy_times y = u dy_times x dy_times y dy_times_unit_thm ⊢ ∀ x• x dy_times dy_one = x dy_times_unit_clauses ⊢ ∀ x• x dy_times dy_one = x ∧ dy_one dy_times x = x dy_exp_clauses ⊢ ∀ x m n • x dy_exp (m + n) = (x dy_exp m) dy_times x dy_exp n ∧ x dy_exp 0 = dy_one ∧ x dy_exp 1 = x ∧ x dy_exp 2 = x dy_times x ∧ x dy_exp 3 = x dy_times x dy_times x dy_times_mono_thm ⊢ ∀ x y z • y dy_less z ⇒ x dy_times y dy_less x dy_times z dy_times_mono_thm1 ⊢ ∀ x y z • y dy_less z ⇒ y dy_times x dy_less z dy_times x dy_times_mono_thm2 ⊢ ∀ x y v w • x dy_less y ∧ v dy_less w ⇒ x dy_times v dy_less y dy_times w dy_times_mono_⇔_thm ⊢ ∀ x y z • x dy_times y dy_less x dy_times z ⇔ y dy_less z dy_arch_thm ⊢ ∀ x y• dy_one dy_less x ⇒ (∃ t• y dy_less x dy_exp t) dy_balance_thm1 ⊢ ∀ x• ∃ y• dy_one dy_less x dy_times y dy_balance_thm2 ⊢ ∀ x• ∃ y• x dy_times y dy_less dy_one dy_right_dense_thm ⊢ ∀ x y • x dy_less y ⇒ (∃ z • x dy_less x dy_times z ∧ x dy_times z dy_less y) dy_less_dense_thm ⊢ ∀ x y• x dy_less y ⇒ (∃ z• x dy_less z ∧ z dy_less y) dy_left_dense_thm ⊢ ∀ x y • x dy_less y ⇒ (∃ z • x dy_less y dy_times z ∧ y dy_times z dy_less y)

privacy policy

Created:

V