Theory "logroot"

Signature

Definitions

LOG

⊢ ∀a n. 1 < a ∧ 0 < n ⇒ a ** LOG a n ≤ n ∧ n < a ** SUC (LOG a n)

ROOT

⊢ ∀r n. 0 < r ⇒ ROOT r n ** r ≤ n ∧ n < SUC (ROOT r n) ** r

SQRTd_def

⊢ ∀n. SQRTd n = (ROOT 2 n,n − ROOT 2 n * ROOT 2 n)

iSQRT0_def

⊢ ∀n. iSQRT0 n =
      (let
         p = SQRTd n;
         d = SND p − FST p
       in
         if d = 0 then (2 * FST p,4 * SND p) else (SUC (2 * FST p),4 * d − 1))

iSQRT1_def

⊢ ∀n. iSQRT1 n =
      (let
         p = SQRTd n;
         d = SUC (SND p) − FST p
       in
         if d = 0 then (2 * FST p,SUC (4 * SND p))
         else (SUC (2 * FST p),4 * (d − 1)))

iSQRT2_def

⊢ ∀n. iSQRT2 n =
      (let
         p = SQRTd n;
         d = 2 * FST p;
         c = SUC (2 * SND p);
         e = c − d
       in
         if e = 0 then (d,2 * c) else (SUC d,2 * e − 1))

iSQRT3_def

⊢ ∀n. iSQRT3 n =
      (let
         p = SQRTd n;
         d = 2 * FST p;
         c = SUC (2 * SND p);
         e = SUC c − d
       in
         if e = 0 then (d,SUC (2 * c)) else (SUC d,2 * (e − 1)))

Theorems

EXP_LE_ISO

⊢ ∀a b r. 0 < r ⇒ (a ≤ b ⇔ a ** r ≤ b ** r)

EXP_LT_ISO

⊢ ∀a b r. 0 < r ⇒ (a < b ⇔ a ** r < b ** r)

EXP_MUL

⊢ ∀a b c. (a ** b) ** c = a ** (b * c)

LE_EXP_ISO

⊢ ∀e a b. 1 < e ⇒ (a ≤ b ⇔ e ** a ≤ e ** b)

LOG_1

⊢ ∀a. 1 < a ⇒ (LOG a 1 = 0)

LOG_ADD

⊢ ∀a b c. 1 < a ∧ b < a ** c ⇒ (LOG a (b + a ** c) = c)

LOG_ADD1

⊢ ∀n a b.
    0 < n ∧ 1 < a ∧ 0 < b ⇒
    (LOG a (a ** SUC n * b) = SUC (LOG a (a ** n * b)))

LOG_BASE

⊢ ∀a. 1 < a ⇒ (LOG a a = 1)

LOG_DIV

⊢ ∀a x. 1 < a ∧ a ≤ x ⇒ (LOG a x = 1 + LOG a (x DIV a))

LOG_EQ_0

⊢ ∀a b. 1 < a ∧ 0 < b ⇒ ((LOG a b = 0) ⇔ b < a)

LOG_EXP

⊢ ∀n a b. 1 < a ∧ 0 < b ⇒ (LOG a (a ** n * b) = n + LOG a b)

LOG_LE_MONO

⊢ ∀a x y. 1 < a ∧ 0 < x ⇒ x ≤ y ⇒ LOG a x ≤ LOG a y

LOG_MOD

⊢ ∀n. 0 < n ⇒ (n = 2 ** LOG 2 n + n MOD 2 ** LOG 2 n)

LOG_MULT

⊢ ∀b x. 1 < b ∧ 0 < x ⇒ (LOG b (b * x) = SUC (LOG b x))

LOG_ROOT

⊢ ∀a x r. 1 < a ∧ 0 < x ∧ 0 < r ⇒ (LOG a (ROOT r x) = LOG a x DIV r)

LOG_RWT

⊢ ∀m n. 1 < m ∧ 0 < n ⇒ (LOG m n = if n < m then 0 else SUC (LOG m (n DIV m)))

LOG_UNIQUE

⊢ ∀a n p. a ** p ≤ n ∧ n < a ** SUC p ⇒ (LOG a n = p)

LOG_add_digit

⊢ ∀b x y. 1 < b ∧ 0 < y ∧ x < b ⇒ (LOG b (b * y + x) = SUC (LOG b y))

LOG_exists

⊢ ∃f. ∀a n. 1 < a ∧ 0 < n ⇒ a ** f a n ≤ n ∧ n < a ** SUC (f a n)

LT_EXP_ISO

⊢ ∀e a b. 1 < e ⇒ (a < b ⇔ e ** a < e ** b)

ROOT_COMPUTE

⊢ ∀r n.
    0 < r ⇒
    (ROOT r 0 = 0) ∧
    (ROOT r n =
     (let
        x = 2 * ROOT r (n DIV 2 ** r)
      in
        if n < SUC x ** r then x else SUC x))

ROOT_DIV

⊢ ∀r x y. 0 < r ∧ 0 < y ⇒ (ROOT r x DIV y = ROOT r (x DIV y ** r))

ROOT_EVAL

⊢ ∀r n.
    ROOT r n =
    if r = 0 then ROOT 0 n
    else if n = 0 then 0
    else
      (let
         m = 2 * ROOT r (n DIV 2 ** r)
       in
         m + if SUC m ** r ≤ n then 1 else 0)

ROOT_EXP

⊢ ∀n r. 0 < r ⇒ (ROOT r (n ** r) = n)

ROOT_LE_MONO

⊢ ∀r x y. 0 < r ⇒ x ≤ y ⇒ ROOT r x ≤ ROOT r y

ROOT_UNIQUE

⊢ ∀r n p. p ** r ≤ n ∧ n < SUC p ** r ⇒ (ROOT r n = p)

ROOT_exists

⊢ ∀r n. 0 < r ⇒ ∃rt. rt ** r ≤ n ∧ n < SUC rt ** r

numeral_root2

⊢ ROOT 2 (NUMERAL n) = FST (SQRTd n)

numeral_sqrt

⊢ (SQRTd ZERO = (0,0)) ∧ (SQRTd (BIT1 ZERO) = (1,0)) ∧
  (SQRTd (BIT2 ZERO) = (1,1)) ∧ (SQRTd (BIT1 (BIT1 n)) = iSQRT3 n) ∧
  (SQRTd (BIT2 (BIT1 n)) = iSQRT0 (SUC n)) ∧
  (SQRTd (BIT1 (BIT2 n)) = iSQRT1 (SUC n)) ∧
  (SQRTd (BIT2 (BIT2 n)) = iSQRT2 (SUC n)) ∧
  (SQRTd (SUC (BIT1 (BIT1 n))) = iSQRT0 (SUC n)) ∧
  (SQRTd (SUC (BIT2 (BIT1 n))) = iSQRT1 (SUC n)) ∧
  (SQRTd (SUC (BIT1 (BIT2 n))) = iSQRT2 (SUC n)) ∧
  (SQRTd (SUC (BIT2 (BIT2 n))) = iSQRT3 (SUC n))