| 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)
|
