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)
fill• (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)
fill∧ (∀ x m• x dy_exp (m + 1) = x dy_times x dy_exp m)
dy_less
⊢ ∀ (m, i) (n, j)
fill• (m, i) dy_less (n, j)
fill⇔ (∃ a b
fill• ℕℤ a + i = ℕℤ b + j
fill∧ 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
fill• (x dy_times y) dy_times z = x dy_times y dy_times z
dy_times_order_thm
⊢ ∀ u x y
fill• x dy_times u = u dy_times x
fill∧ (u dy_times x) dy_times y
fill= u dy_times x dy_times y
fill∧ x dy_times u dy_times y
fill= 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
fill• x dy_exp (m + n) = (x dy_exp m) dy_times x dy_exp n
fill∧ x dy_exp 0 = dy_one
fill∧ x dy_exp 1 = x
fill∧ x dy_exp 2 = x dy_times x
fill∧ x dy_exp 3 = x dy_times x dy_times x
dy_times_mono_thm
⊢ ∀ x y z
fill• y dy_less z ⇒ x dy_times y dy_less x dy_times z
dy_times_mono_thm1
⊢ ∀ x y z
fill• y dy_less z ⇒ y dy_times x dy_less z dy_times x
dy_times_mono_thm2
⊢ ∀ x y v w
fill• x dy_less y ∧ v dy_less w
fill⇒ x dy_times v dy_less y dy_times w
dy_times_mono_⇔_thm
⊢ ∀ x y z
fill• 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
fill• x dy_less y
fill⇒ (∃ z
fill• x dy_less x dy_times z
fill∧ 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
fill• x dy_less y
fill⇒ (∃ z
fill• x dy_less y dy_times z
fill∧ y dy_times z dy_less y)

up quick index

privacy policy

Created:

V