Theory logroot

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

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

⊢ ∀n. SQRTd n = (SQRT n,n − SQRT n * SQRT n)

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

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

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

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

⊢ ∀n m. 0 < m ⇒ (n ** m = n ⇔ m = 1 ∨ n = 0 ∨ n = 1)

⊢ ∀a b c n m.
    0 < a ∧ n < m ∧ a ** n * b = a ** m * c ⇒ ∃d. 0 < d ∧ b = a ** d * c

⊢ ∀n b. 0 < n ⇒ b ≤ b ** n

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

⊢ (<..num comp'n..> ** e ≤ <..num comp'n..> ⇔
   <..num comp'n..> < 2 ∨ e ≤ LOG <..num comp'n..> <..num comp'n..> ) ∧
  (<..num comp'n..> ** e ≤ <..num comp'n..> ⇔
   <..num comp'n..> < 2 ∨ e ≤ LOG <..num comp'n..> <..num comp'n..> )

⊢ ∀n b. 1 < b ∧ 1 < n ⇒ b < b ** n

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

⊢ (<..num comp'n..> ** e < <..num comp'n..> ⇔
   <..num comp'n..> < 2 ∨ e ≤ LOG <..num comp'n..> (<..num comp'n..> − 1)) ∧
  (<..num comp'n..> ** e < <..num comp'n..> ⇔
   <..num comp'n..> < 2 ∨ e ≤ LOG <..num comp'n..> (<..num comp'n..> − 1)) ∧
  (<..num comp'n..> ** e < <..num comp'n..> ⇔
   <..num comp'n..> < 2 ∨ e ≤ LOG <..num comp'n..> (<..num comp'n..> − 1))

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

⊢ ∀a b c n m.
    0 < a ∧ n < m ∧ b * a ** n = c * a ** m ⇒ ∃d. 0 < d ∧ b = c * a ** d

⊢ ∀a b n. 1 < a ∧ 0 < b ∧ b ≤ a ** n ⇒ LOG a b ≤ n

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

⊢ (<..num comp'n..> ≤ <..num comp'n..> ** e ⇔
   2 ≤ <..num comp'n..> ∧ LOG <..num comp'n..> (<..num comp'n..> − 1) < e) ∧
  (<..num comp'n..> ≤ <..num comp'n..> ** e ⇔
   2 ≤ <..num comp'n..> ∧ LOG <..num comp'n..> (<..num comp'n..> − 1) < e) ∧
  (<..num comp'n..> ≤ <..num comp'n..> ** e ⇔
   2 ≤ <..num comp'n..> ∧ LOG <..num comp'n..> (<..num comp'n..> − 1) < e)

⊢ LOG2 1 = 0

⊢ LOG2 2 = 1

⊢ ∀n. LOG2 (2 ** n) = n

⊢ ∀n. 0 < n ⇒ (LOG2 n = 0 ⇔ n = 1)

⊢ ∀n. 0 < n ⇒ (LOG2 n = 1 ⇔ n = 2 ∨ n = 3)

⊢ ∀n. LOG2 n = n ⇒ n = 0

⊢ ∀n. 2 ** LOG2 n = n ⇔ ∃k. n = 2 ** k

⊢ ∀n m. 0 < n ∧ n ≤ m ⇒ LOG2 n ≤ LOG2 m

⊢ ∀n m. 0 < n ⇒ n ≤ m ⇒ LOG2 n ≤ LOG2 m

⊢ ∀n m. 0 < n ∧ n < m ⇒ LOG2 n ≤ LOG2 m

⊢ ∀n. 0 < n ⇒ LOG2 n < n

⊢ ∀n m. 0 < n ⇒ LOG2 (n * 2 ** m) = LOG2 n + m

⊢ ∀n. 0 < n ⇒ LOG2 n ≠ n

⊢ ∀n. 1 < n ⇒ 0 < LOG2 n

⊢ ∀n. 0 < n ⇒ 2 ** LOG2 n ≤ n ∧ n < 2 ** SUC (LOG2 n)

⊢ ∀n. 1 < n ⇒ 1 < (SUC (LOG2 n))²

⊢ ∀n. 0 < n ⇒ 4 ≤ (2 * SUC (LOG2 n))²

⊢ ∀n. 0 < n ⇒ ∀p. LOG2 n = p ⇔ 2 ** p ≤ n ∧ n < 2 ** SUC p

⊢ ∀n. 0 < n ⇒ LOG2 (2 * n) = 1 + LOG2 n

⊢ ∀n. 1 < n ⇒ 1 < 2 * LOG2 n

⊢ ∀n. 1 < n ⇒ 4 ≤ (2 * LOG2 n)²

⊢ ∀n m. 2 ** m ≤ n ∧ n < 2 ** SUC m ⇒ LOG2 n = m

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

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

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

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

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

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

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

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

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

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

⊢ ∀a b n. 1 < a ∧ 0 < n ∧ a ≤ b ⇒ LOG b n ≤ LOG a n

⊢ ∀n. 0 < n ⇒ n = 2 ** LOG2 n + n MOD 2 ** LOG2 n

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

⊢ LOG <..num comp'n..> <..num comp'n..> =
  (if <..num comp'n..> < <..num comp'n..> then 0
   else LOG <..num comp'n..> (<..num comp'n..> DIV <..num comp'n..> ) + 1) ∧
  LOG <..num comp'n..> <..num comp'n..> =
  (if <..num comp'n..> < <..num comp'n..> then 0
   else LOG <..num comp'n..> (<..num comp'n..> DIV <..num comp'n..> ) + 1) ∧
  LOG <..num comp'n..> <..num comp'n..> =
  (if <..num comp'n..> < <..num comp'n..> then 0
   else LOG <..num comp'n..> (<..num comp'n..> DIV <..num comp'n..> ) + 1) ∧
  LOG <..num comp'n..> <..num comp'n..> =
  (if <..num comp'n..> < <..num comp'n..> then 0
   else LOG <..num comp'n..> (<..num comp'n..> DIV <..num comp'n..> ) + 1) ∧
  LOG <..num comp'n..> <..num comp'n..> =
  (if <..num comp'n..> < <..num comp'n..> then 0
   else LOG <..num comp'n..> (<..num comp'n..> DIV <..num comp'n..> ) + 1) ∧
  LOG <..num comp'n..> <..num comp'n..> =
  if <..num comp'n..> < <..num comp'n..> then 0
  else LOG <..num comp'n..> (<..num comp'n..> DIV <..num comp'n..> ) + 1

⊢ ∀b n. 1 < b ⇒ LOG b (b ** n) = n

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

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

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

⊢ ∀a n.
    1 < a ∧ 0 < n ⇒
    ∀p. LOG a n = p ⇔ SUC n ≤ a ** SUC p ∧ a ** SUC p ≤ a * n

⊢ ∀a n. 1 < a ∧ 0 < n ⇒ ∀p. LOG a n = p ⇔ a ** p ≤ n ∧ n < a ** SUC p

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

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

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

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

⊢ x < b ** e ⇔
  b = 0 ∧ e = 0 ∧ x = 0 ∨ b = 1 ∧ x = 0 ∨ 2 ≤ b ∧ (LOG b x < e ∨ x = 0)

⊢ (<..num comp'n..> < <..num comp'n..> ** e ⇔
   2 ≤ <..num comp'n..> ∧ LOG <..num comp'n..> <..num comp'n..> < e) ∧
  (<..num comp'n..> < <..num comp'n..> ** e ⇔
   2 ≤ <..num comp'n..> ∧ LOG <..num comp'n..> <..num comp'n..> < e)

⊢ ∀n m. n < SQRT m ⇒ n² < m

⊢ ∀m n. 0 < m ⇒ 1 ≤ m ** n

⊢ ∀n. ROOT 1 n = n

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

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

⊢ ∀m. 0 < m ⇒ ∀n. ROOT m n = 0 ⇔ n = 0

⊢ ∀m. 0 < m ⇒ ∀n. ROOT m n = 1 ⇔ 0 < n ∧ n < 2 ** m

⊢ ∀m n. 0 < m ⇒ (ROOT m n = n ⇔ m = 1 ∨ n = 0 ∨ n = 1)

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

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

⊢ ∀m n b. 0 < m ∧ b ** m = n ⇒ b = ROOT m n

⊢ ∀m n. 0 < m ⇒ (n ≤ ROOT m n ⇔ m = 1 ∨ n = 0 ∨ n = 1)

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

⊢ ∀a b n. 0 < a ∧ a ≤ b ⇒ ROOT b n ≤ ROOT a n

⊢ ∀m n. 0 < m ⇒ ROOT m n ≤ n

⊢ ∀m. 0 < m ⇒ ROOT m 0 = 0

⊢ ∀m. 0 < m ⇒ ROOT m 1 = 1

⊢ ∀a n. 1 < a ∧ 0 < n ⇒ ROOT n (a ** n) = a

⊢ ∀r n.
    0 < r ⇒
    ROOT r (SUC n) =
    ROOT r n + if SUC n = SUC (ROOT r n) ** r then 1 else 0

⊢ ∀r. 0 < r ⇒ ∀n p. ROOT r n = p ⇔ p ** r ≤ n ∧ n < SUC p ** r

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

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

⊢ SQRT 0 = 0

⊢ SQRT 1 = 1

⊢ ∀n. SQRT n = 0 ⇔ n = 0

⊢ ∀n. SQRT n = 1 ⇔ n = 1 ∨ n = 2 ∨ n = 3

⊢ ∀n. SQRT n = n ⇔ n = 0 ∨ n = 1

⊢ ∀n. SQRT n² = n

⊢ ∀n. n ≤ SQRT n ⇔ n = 0 ∨ n = 1

⊢ ∀n m. n ≤ m ⇒ SQRT n ≤ SQRT m

⊢ ∀n m. n < m ⇒ SQRT n ≤ SQRT m

⊢ ∀n m. SQRT n < m ⇒ n < m²

⊢ ∀n m. SQRT n < SQRT m ⇒ n < m

⊢ ∀n. SQRT n² = n

⊢ ∀n. (SQRT n)² ≤ n ∧ n < (SUC (SQRT n))²

⊢ ∀n p. SQRT n = p ⇔ p² ≤ n ∧ n < (SUC p)²

⊢ ∀n p. p² ≤ n ∧ n < (SUC p)² ⇒ SQRT n = p

⊢ ∀n. 0 < n ⇒ 2 ** LOG2 n ≤ n

⊢ SQRT <..num comp'n..> = FST (SQRTd n)

⊢ SQRTd ZERO = (0,0) ∧ SQRTd <..num comp'n..> = (1,0) ∧
  SQRTd <..num comp'n..> = (1,1) ∧ SQRTd <..num comp'n..> = iSQRT3 n ∧
  SQRTd <..num comp'n..> = iSQRT0 (SUC n) ∧
  SQRTd <..num comp'n..> = iSQRT1 (SUC n) ∧
  SQRTd <..num comp'n..> = iSQRT2 (SUC n) ∧
  SQRTd (SUC <..num comp'n..> ) = iSQRT0 (SUC n) ∧
  SQRTd (SUC <..num comp'n..> ) = iSQRT1 (SUC n) ∧
  SQRTd (SUC <..num comp'n..> ) = iSQRT2 (SUC n) ∧
  SQRTd (SUC <..num comp'n..> ) = iSQRT3 (SUC n)