Structure logrootTheory

signature logrootTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val LOG : thm
    val ROOT : thm
    val SQRTd_def : thm
    val iSQRT0_def : thm
    val iSQRT1_def : thm
    val iSQRT2_def : thm
    val iSQRT3_def : thm
  
  (*  Theorems  *)
    val EXP_EQ_SELF : thm
    val EXP_LCANCEL : thm
    val EXP_LE : thm
    val EXP_LE_ISO : thm
    val EXP_LE_LOG_SIMP : thm
    val EXP_LT : thm
    val EXP_LT_ISO : thm
    val EXP_LT_LOG_SIMP : thm
    val EXP_MUL : thm
    val EXP_RCANCEL : thm
    val EXP_TO_LOG : thm
    val LE_EXP_ISO : thm
    val LE_EXP_LOG_SIMP : thm
    val LOG2_1 : thm
    val LOG2_2 : thm
    val LOG2_2_EXP : thm
    val LOG2_EQ_0 : thm
    val LOG2_EQ_1 : thm
    val LOG2_EQ_SELF : thm
    val LOG2_EXACT_EXP : thm
    val LOG2_LE : thm
    val LOG2_LE_MONO : thm
    val LOG2_LT : thm
    val LOG2_LT_SELF : thm
    val LOG2_MULT_EXP : thm
    val LOG2_NEQ_SELF : thm
    val LOG2_POS : thm
    val LOG2_PROPERTY : thm
    val LOG2_SUC_SQ : thm
    val LOG2_SUC_TWICE_SQ : thm
    val LOG2_THM : thm
    val LOG2_TWICE : thm
    val LOG2_TWICE_LT : thm
    val LOG2_TWICE_SQ : thm
    val LOG2_UNIQUE : thm
    val LOG_1 : thm
    val LOG_ADD : thm
    val LOG_ADD1 : thm
    val LOG_BASE : thm
    val LOG_DIV : thm
    val LOG_EQ_0 : thm
    val LOG_EVAL : thm
    val LOG_EXACT_EXP : thm
    val LOG_EXP : thm
    val LOG_LE_MONO : thm
    val LOG_LE_REVERSE : thm
    val LOG_MOD : thm
    val LOG_MULT : thm
    val LOG_NUMERAL : thm
    val LOG_POW : thm
    val LOG_POWER : thm
    val LOG_ROOT : thm
    val LOG_RWT : thm
    val LOG_TEST : thm
    val LOG_THM : thm
    val LOG_UNIQUE : thm
    val LOG_add_digit : thm
    val LOG_exists : thm
    val LT_EXP_ISO : thm
    val LT_EXP_LOG : thm
    val LT_EXP_LOG_SIMP : thm
    val LT_SQRT_IMP : thm
    val ONE_LE_EXP : thm
    val ROOT_1 : thm
    val ROOT_COMPUTE : thm
    val ROOT_DIV : thm
    val ROOT_EQ_0 : thm
    val ROOT_EQ_1 : thm
    val ROOT_EQ_SELF : thm
    val ROOT_EVAL : thm
    val ROOT_EXP : thm
    val ROOT_FROM_POWER : thm
    val ROOT_GE_SELF : thm
    val ROOT_LE_MONO : thm
    val ROOT_LE_REVERSE : thm
    val ROOT_LE_SELF : thm
    val ROOT_OF_0 : thm
    val ROOT_OF_1 : thm
    val ROOT_POWER : thm
    val ROOT_SUC : thm
    val ROOT_THM : thm
    val ROOT_UNIQUE : thm
    val ROOT_exists : thm
    val SQRT_0 : thm
    val SQRT_1 : thm
    val SQRT_EQ_0 : thm
    val SQRT_EQ_1 : thm
    val SQRT_EQ_SELF : thm
    val SQRT_EXP_2 : thm
    val SQRT_GE_SELF : thm
    val SQRT_LE : thm
    val SQRT_LT : thm
    val SQRT_LT_IMP : thm
    val SQRT_LT_SQRT : thm
    val SQRT_OF_SQ : thm
    val SQRT_PROPERTY : thm
    val SQRT_THM : thm
    val SQRT_UNIQUE : thm
    val TWO_EXP_LOG2_LE : thm
    val numeral_root2 : thm
    val numeral_sqrt : thm
(*
   [basicSize] Parent theory of "logroot"
   
   [cv] Parent theory of "logroot"
   
   [reduce] Parent theory of "logroot"
   
   [while] Parent theory of "logroot"
   
   [LOG]  Definition
      
      ⊢ ∀a n. 1 < a ∧ 0 < n ⇒ a ** LOG a n ≤ n ∧ n < a ** SUC (LOG a n)
   
   [ROOT]  Definition
      
      ⊢ ∀r n. 0 < r ⇒ ROOT r n ** r ≤ n ∧ n < SUC (ROOT r n) ** r
   
   [SQRTd_def]  Definition
      
      ⊢ ∀n. SQRTd n = (SQRT n,n − SQRT n * SQRT n)
   
   [iSQRT0_def]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀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]  Definition
      
      ⊢ ∀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)))
   
   [EXP_EQ_SELF]  Theorem
      
      ⊢ ∀n m. 0 < m ⇒ (n ** m = n ⇔ m = 1 ∨ n = 0 ∨ n = 1)
   
   [EXP_LCANCEL]  Theorem
      
      ⊢ ∀a b c n m.
          0 < a ∧ n < m ∧ a ** n * b = a ** m * c ⇒
          ∃d. 0 < d ∧ b = a ** d * c
   
   [EXP_LE]  Theorem
      
      ⊢ ∀n b. 0 < n ⇒ b ≤ b ** n
   
   [EXP_LE_ISO]  Theorem
      
      ⊢ ∀a b r. 0 < r ⇒ (a ≤ b ⇔ a ** r ≤ b ** r)
   
   [EXP_LE_LOG_SIMP]  Theorem
      
      ⊢ (<..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..> )
   
   [EXP_LT]  Theorem
      
      ⊢ ∀n b. 1 < b ∧ 1 < n ⇒ b < b ** n
   
   [EXP_LT_ISO]  Theorem
      
      ⊢ ∀a b r. 0 < r ⇒ (a < b ⇔ a ** r < b ** r)
   
   [EXP_LT_LOG_SIMP]  Theorem
      
      ⊢ (<..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))
   
   [EXP_MUL]  Theorem
      
      ⊢ ∀a b c. (a ** b) ** c = a ** (b * c)
   
   [EXP_RCANCEL]  Theorem
      
      ⊢ ∀a b c n m.
          0 < a ∧ n < m ∧ b * a ** n = c * a ** m ⇒
          ∃d. 0 < d ∧ b = c * a ** d
   
   [EXP_TO_LOG]  Theorem
      
      ⊢ ∀a b n. 1 < a ∧ 0 < b ∧ b ≤ a ** n ⇒ LOG a b ≤ n
   
   [LE_EXP_ISO]  Theorem
      
      ⊢ ∀e a b. 1 < e ⇒ (a ≤ b ⇔ e ** a ≤ e ** b)
   
   [LE_EXP_LOG_SIMP]  Theorem
      
      ⊢ (<..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]  Theorem
      
      ⊢ LOG2 1 = 0
   
   [LOG2_2]  Theorem
      
      ⊢ LOG2 2 = 1
   
   [LOG2_2_EXP]  Theorem
      
      ⊢ ∀n. LOG2 (2 ** n) = n
   
   [LOG2_EQ_0]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ (LOG2 n = 0 ⇔ n = 1)
   
   [LOG2_EQ_1]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ (LOG2 n = 1 ⇔ n = 2 ∨ n = 3)
   
   [LOG2_EQ_SELF]  Theorem
      
      ⊢ ∀n. LOG2 n = n ⇒ n = 0
   
   [LOG2_EXACT_EXP]  Theorem
      
      ⊢ ∀n. 2 ** LOG2 n = n ⇔ ∃k. n = 2 ** k
   
   [LOG2_LE]  Theorem
      
      ⊢ ∀n m. 0 < n ∧ n ≤ m ⇒ LOG2 n ≤ LOG2 m
   
   [LOG2_LE_MONO]  Theorem
      
      ⊢ ∀n m. 0 < n ⇒ n ≤ m ⇒ LOG2 n ≤ LOG2 m
   
   [LOG2_LT]  Theorem
      
      ⊢ ∀n m. 0 < n ∧ n < m ⇒ LOG2 n ≤ LOG2 m
   
   [LOG2_LT_SELF]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ LOG2 n < n
   
   [LOG2_MULT_EXP]  Theorem
      
      ⊢ ∀n m. 0 < n ⇒ LOG2 (n * 2 ** m) = LOG2 n + m
   
   [LOG2_NEQ_SELF]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ LOG2 n ≠ n
   
   [LOG2_POS]  Theorem
      
      ⊢ ∀n. 1 < n ⇒ 0 < LOG2 n
   
   [LOG2_PROPERTY]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ 2 ** LOG2 n ≤ n ∧ n < 2 ** SUC (LOG2 n)
   
   [LOG2_SUC_SQ]  Theorem
      
      ⊢ ∀n. 1 < n ⇒ 1 < (SUC (LOG2 n))²
   
   [LOG2_SUC_TWICE_SQ]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ 4 ≤ (2 * SUC (LOG2 n))²
   
   [LOG2_THM]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ ∀p. LOG2 n = p ⇔ 2 ** p ≤ n ∧ n < 2 ** SUC p
   
   [LOG2_TWICE]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ LOG2 (2 * n) = 1 + LOG2 n
   
   [LOG2_TWICE_LT]  Theorem
      
      ⊢ ∀n. 1 < n ⇒ 1 < 2 * LOG2 n
   
   [LOG2_TWICE_SQ]  Theorem
      
      ⊢ ∀n. 1 < n ⇒ 4 ≤ (2 * LOG2 n)²
   
   [LOG2_UNIQUE]  Theorem
      
      ⊢ ∀n m. 2 ** m ≤ n ∧ n < 2 ** SUC m ⇒ LOG2 n = m
   
   [LOG_1]  Theorem
      
      ⊢ ∀a. 1 < a ⇒ LOG a 1 = 0
   
   [LOG_ADD]  Theorem
      
      ⊢ ∀a b c. 1 < a ∧ b < a ** c ⇒ LOG a (b + a ** c) = c
   
   [LOG_ADD1]  Theorem
      
      ⊢ ∀n a b.
          0 < n ∧ 1 < a ∧ 0 < b ⇒
          LOG a (a ** SUC n * b) = SUC (LOG a (a ** n * b))
   
   [LOG_BASE]  Theorem
      
      ⊢ ∀a. 1 < a ⇒ LOG a a = 1
   
   [LOG_DIV]  Theorem
      
      ⊢ ∀a x. 1 < a ∧ a ≤ x ⇒ LOG a x = 1 + LOG a (x DIV a)
   
   [LOG_EQ_0]  Theorem
      
      ⊢ ∀a b. 1 < a ∧ 0 < b ⇒ (LOG a b = 0 ⇔ b < a)
   
   [LOG_EVAL]  Theorem
      
      ⊢ ∀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))
   
   [LOG_EXACT_EXP]  Theorem
      
      ⊢ ∀a. 1 < a ⇒ ∀n. LOG a (a ** n) = n
   
   [LOG_EXP]  Theorem
      
      ⊢ ∀n a b. 1 < a ∧ 0 < b ⇒ LOG a (a ** n * b) = n + LOG a b
   
   [LOG_LE_MONO]  Theorem
      
      ⊢ ∀a x y. 1 < a ∧ 0 < x ⇒ x ≤ y ⇒ LOG a x ≤ LOG a y
   
   [LOG_LE_REVERSE]  Theorem
      
      ⊢ ∀a b n. 1 < a ∧ 0 < n ∧ a ≤ b ⇒ LOG b n ≤ LOG a n
   
   [LOG_MOD]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ n = 2 ** LOG2 n + n MOD 2 ** LOG2 n
   
   [LOG_MULT]  Theorem
      
      ⊢ ∀b x. 1 < b ∧ 0 < x ⇒ LOG b (b * x) = SUC (LOG b x)
   
   [LOG_NUMERAL]  Theorem
      
      ⊢ 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
   
   [LOG_POW]  Theorem
      
      ⊢ ∀b n. 1 < b ⇒ LOG b (b ** n) = n
   
   [LOG_POWER]  Theorem
      
      ⊢ ∀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)
   
   [LOG_ROOT]  Theorem
      
      ⊢ ∀a x r. 1 < a ∧ 0 < x ∧ 0 < r ⇒ LOG a (ROOT r x) = LOG a x DIV r
   
   [LOG_RWT]  Theorem
      
      ⊢ ∀m n.
          1 < m ∧ 0 < n ⇒
          LOG m n = if n < m then 0 else SUC (LOG m (n DIV m))
   
   [LOG_TEST]  Theorem
      
      ⊢ ∀a n.
          1 < a ∧ 0 < n ⇒
          ∀p. LOG a n = p ⇔ SUC n ≤ a ** SUC p ∧ a ** SUC p ≤ a * n
   
   [LOG_THM]  Theorem
      
      ⊢ ∀a n. 1 < a ∧ 0 < n ⇒ ∀p. LOG a n = p ⇔ a ** p ≤ n ∧ n < a ** SUC p
   
   [LOG_UNIQUE]  Theorem
      
      ⊢ ∀a n p. a ** p ≤ n ∧ n < a ** SUC p ⇒ LOG a n = p
   
   [LOG_add_digit]  Theorem
      
      ⊢ ∀b x y. 1 < b ∧ 0 < y ∧ x < b ⇒ LOG b (b * y + x) = SUC (LOG b y)
   
   [LOG_exists]  Theorem
      
      ⊢ ∃f. ∀a n. 1 < a ∧ 0 < n ⇒ a ** f a n ≤ n ∧ n < a ** SUC (f a n)
   
   [LT_EXP_ISO]  Theorem
      
      ⊢ ∀e a b. 1 < e ⇒ (a < b ⇔ e ** a < e ** b)
   
   [LT_EXP_LOG]  Theorem
      
      ⊢ x < b ** e ⇔
        b = 0 ∧ e = 0 ∧ x = 0 ∨ b = 1 ∧ x = 0 ∨
        2 ≤ b ∧ (LOG b x < e ∨ x = 0)
   
   [LT_EXP_LOG_SIMP]  Theorem
      
      ⊢ (<..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)
   
   [LT_SQRT_IMP]  Theorem
      
      ⊢ ∀n m. n < SQRT m ⇒ n² < m
   
   [ONE_LE_EXP]  Theorem
      
      ⊢ ∀m n. 0 < m ⇒ 1 ≤ m ** n
   
   [ROOT_1]  Theorem
      
      ⊢ ∀n. ROOT 1 n = n
   
   [ROOT_COMPUTE]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀r x y. 0 < r ∧ 0 < y ⇒ ROOT r x DIV y = ROOT r (x DIV y ** r)
   
   [ROOT_EQ_0]  Theorem
      
      ⊢ ∀m. 0 < m ⇒ ∀n. ROOT m n = 0 ⇔ n = 0
   
   [ROOT_EQ_1]  Theorem
      
      ⊢ ∀m. 0 < m ⇒ ∀n. ROOT m n = 1 ⇔ 0 < n ∧ n < 2 ** m
   
   [ROOT_EQ_SELF]  Theorem
      
      ⊢ ∀m n. 0 < m ⇒ (ROOT m n = n ⇔ m = 1 ∨ n = 0 ∨ n = 1)
   
   [ROOT_EVAL]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀n r. 0 < r ⇒ ROOT r (n ** r) = n
   
   [ROOT_FROM_POWER]  Theorem
      
      ⊢ ∀m n b. 0 < m ∧ b ** m = n ⇒ b = ROOT m n
   
   [ROOT_GE_SELF]  Theorem
      
      ⊢ ∀m n. 0 < m ⇒ (n ≤ ROOT m n ⇔ m = 1 ∨ n = 0 ∨ n = 1)
   
   [ROOT_LE_MONO]  Theorem
      
      ⊢ ∀r x y. 0 < r ⇒ x ≤ y ⇒ ROOT r x ≤ ROOT r y
   
   [ROOT_LE_REVERSE]  Theorem
      
      ⊢ ∀a b n. 0 < a ∧ a ≤ b ⇒ ROOT b n ≤ ROOT a n
   
   [ROOT_LE_SELF]  Theorem
      
      ⊢ ∀m n. 0 < m ⇒ ROOT m n ≤ n
   
   [ROOT_OF_0]  Theorem
      
      ⊢ ∀m. 0 < m ⇒ ROOT m 0 = 0
   
   [ROOT_OF_1]  Theorem
      
      ⊢ ∀m. 0 < m ⇒ ROOT m 1 = 1
   
   [ROOT_POWER]  Theorem
      
      ⊢ ∀a n. 1 < a ∧ 0 < n ⇒ ROOT n (a ** n) = a
   
   [ROOT_SUC]  Theorem
      
      ⊢ ∀r n.
          0 < r ⇒
          ROOT r (SUC n) =
          ROOT r n + if SUC n = SUC (ROOT r n) ** r then 1 else 0
   
   [ROOT_THM]  Theorem
      
      ⊢ ∀r. 0 < r ⇒ ∀n p. ROOT r n = p ⇔ p ** r ≤ n ∧ n < SUC p ** r
   
   [ROOT_UNIQUE]  Theorem
      
      ⊢ ∀r n p. p ** r ≤ n ∧ n < SUC p ** r ⇒ ROOT r n = p
   
   [ROOT_exists]  Theorem
      
      ⊢ ∀r n. 0 < r ⇒ ∃rt. rt ** r ≤ n ∧ n < SUC rt ** r
   
   [SQRT_0]  Theorem
      
      ⊢ SQRT 0 = 0
   
   [SQRT_1]  Theorem
      
      ⊢ SQRT 1 = 1
   
   [SQRT_EQ_0]  Theorem
      
      ⊢ ∀n. SQRT n = 0 ⇔ n = 0
   
   [SQRT_EQ_1]  Theorem
      
      ⊢ ∀n. SQRT n = 1 ⇔ n = 1 ∨ n = 2 ∨ n = 3
   
   [SQRT_EQ_SELF]  Theorem
      
      ⊢ ∀n. SQRT n = n ⇔ n = 0 ∨ n = 1
   
   [SQRT_EXP_2]  Theorem
      
      ⊢ ∀n. SQRT n² = n
   
   [SQRT_GE_SELF]  Theorem
      
      ⊢ ∀n. n ≤ SQRT n ⇔ n = 0 ∨ n = 1
   
   [SQRT_LE]  Theorem
      
      ⊢ ∀n m. n ≤ m ⇒ SQRT n ≤ SQRT m
   
   [SQRT_LT]  Theorem
      
      ⊢ ∀n m. n < m ⇒ SQRT n ≤ SQRT m
   
   [SQRT_LT_IMP]  Theorem
      
      ⊢ ∀n m. SQRT n < m ⇒ n < m²
   
   [SQRT_LT_SQRT]  Theorem
      
      ⊢ ∀n m. SQRT n < SQRT m ⇒ n < m
   
   [SQRT_OF_SQ]  Theorem
      
      ⊢ ∀n. SQRT n² = n
   
   [SQRT_PROPERTY]  Theorem
      
      ⊢ ∀n. (SQRT n)² ≤ n ∧ n < (SUC (SQRT n))²
   
   [SQRT_THM]  Theorem
      
      ⊢ ∀n p. SQRT n = p ⇔ p² ≤ n ∧ n < (SUC p)²
   
   [SQRT_UNIQUE]  Theorem
      
      ⊢ ∀n p. p² ≤ n ∧ n < (SUC p)² ⇒ SQRT n = p
   
   [TWO_EXP_LOG2_LE]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ 2 ** LOG2 n ≤ n
   
   [numeral_root2]  Theorem
      
      ⊢ SQRT <..num comp'n..> = FST (SQRTd n)
   
   [numeral_sqrt]  Theorem
      
      ⊢ 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)
   
   
*)
end

HOL 4, Trindemossen-2