---

Step * 1 of Lemma isqrt_newton_wf

.....assertion..... 
∀d:ℕ. ∀n,x:ℕ+.
  (((((x + 1) * (x + 1)) - n) ≤ d)
  ⇒ n < (x + 1) * (x + 1)
  ⇒ (isqrt_newton(n;x) ∈ ∃r:ℕ [(((r * r) ≤ n) ∧ n < (r + 1) * (r + 1))]))
BY
{ TACTIC:((CompleteInductionOnNat THEN Auto)
          THEN RecUnfold `isqrt_newton` 0
          THEN (GenConclTerm ⌜x + (n ÷ x)⌝⋅ THENA Auto)
          THEN (CallByValueReduce 0 THENA Auto)
          THEN Mul ⌜x⌝ (-1)⋅
          THEN (RW IntNormC (-1) THENA Auto)
          THEN (RWO "div_rem_sum2" (-1) THENA Auto)
          THEN (InstLemma `rem_bounds_1` [⌜n⌝;⌜x⌝]⋅ THENA Auto)
          THEN (InstLemma `div_bounds_1` [⌜n⌝;⌜x⌝]⋅ THENA Auto)
          THEN (GenConclTerm ⌜v ÷ 2⌝⋅ THENA Auto)
          THEN (Mul ⌜2⌝ (-1)⋅ THENA Auto)
          THEN TACTIC:(RWO "div_rem_sum2" (-1) THENA Auto)
          THEN (InstLemma `rem_bounds_1` [⌜v⌝;⌜2⌝]⋅ THENA Auto)
          THEN (CallByValueReduce 0 THENA Auto)
          THEN ExRepD) }

1
1. d : ℕ
2. ∀d:ℕd. ∀n,x:ℕ+.
     (((((x + 1) * (x + 1)) - n) ≤ d)
     ⇒ n < (x + 1) * (x + 1)
     ⇒ (isqrt_newton(n;x) ∈ ∃r:ℕ [(((r * r) ≤ n) ∧ n < (r + 1) * (r + 1))]))
3. n : ℕ+@i
4. x : ℕ+@i
5. (((x + 1) * (x + 1)) - n) ≤ d
6. n < (x + 1) * (x + 1)
7. v : ℤ@i
8. (x + (n ÷ x)) = v ∈ ℤ
9. ((n - n rem x) + (x * x)) = (v * x) ∈ ℤ
10. 0 ≤ (n rem x)
11. n rem x < x
12. 0 ≤ (n ÷ x)
13. v1 : ℤ@i
14. (v ÷ 2) = v1 ∈ ℤ
15. (v - v rem 2) = (2 * v1) ∈ ℤ
16. 0 ≤ (v rem 2)
17. v rem 2 < 2
⊢ if v1=x then v1 else if (x) < (v1)  then x  else isqrt_newton(n;v1) ∈ ∃r:ℕ [(((r * r) ≤ n) ∧ n < (r + 1) * (r + 1))]

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}d:\mBbbN{}.  \mforall{}n,x:\mBbbN{}\msupplus{}.
    (((((x  +  1)  *  (x  +  1))  -  n)  \mleq{}  d)
    {}\mRightarrow{}  n  <  (x  +  1)  *  (x  +  1)
    {}\mRightarrow{}  (isqrt\_newton(n;x)  \mmember{}  \mexists{}r:\mBbbN{}  [(((r  *  r)  \mleq{}  n)  \mwedge{}  n  <  (r  +  1)  *  (r  +  1))]))


By

---

Latex:
TACTIC:((CompleteInductionOnNat  THEN  Auto)
                THEN  RecUnfold  `isqrt\_newton`  0
                THEN  (GenConclTerm  \mkleeneopen{}x  +  (n  \mdiv{}  x)\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  (CallByValueReduce  0  THENA  Auto)
                THEN  Mul  \mkleeneopen{}x\mkleeneclose{}  (-1)\mcdot{}
                THEN  (RW  IntNormC  (-1)  THENA  Auto)
                THEN  (RWO  "div\_rem\_sum2"  (-1)  THENA  Auto)
                THEN  (InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  (InstLemma  `div\_bounds\_1`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  (GenConclTerm  \mkleeneopen{}v  \mdiv{}  2\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  (Mul  \mkleeneopen{}2\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
                THEN  TACTIC:(RWO  "div\_rem\_sum2"  (-1)  THENA  Auto)
                THEN  (InstLemma  `rem\_bounds\_1`  [\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  (CallByValueReduce  0  THENA  Auto)
                THEN  ExRepD)

---

Home Index