---

Step * 2 3 1 1 1 of Lemma proper-divisor_wf


1. n : ℕ+
2. 5 ≤ n
3. 16 ≤ n
4. 81 ≤ n
5. (iroot(4;n)^4 ≤ n) ∧ n < (iroot(4;n) + 1)^4
6. iroot(4;n) ≤ 2
⊢ proper-divisor-aux(n;iroot(4;n) + 1;iroot(4;n) + 1;1;iroot(4;n) + 1) ∈ Dec(∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))])
BY
{ ((Assert (iroot(4;n) = 0 ∈ ℤ) ∨ (iroot(4;n) = 1 ∈ ℤ) ∨ (iroot(4;n) = 2 ∈ ℤ) BY
          (MoveToConcl (-1) THEN GenConclAtAddr [1;1] THEN Auto THEN DVar `v' THEN SplitOrHyps THEN Auto'))
   THEN (SplitOrHyps
         THEN (HypSubst' (-1) (-3)
               THEN RepUR ``exp`` -3
               THEN RepeatFor 3 ((xxx(RWO "primrec-unroll" (-3) THENM Reduce (-3))xxx THENA Auto))
               THEN Auto')⋅
         )⋅
   ) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  5  \mleq{}  n
3.  16  \mleq{}  n
4.  81  \mleq{}  n
5.  (iroot(4;n)\^{}4  \mleq{}  n)  \mwedge{}  n  <  (iroot(4;n)  +  1)\^{}4
6.  iroot(4;n)  \mleq{}  2
\mvdash{}  proper-divisor-aux(n;iroot(4;n)  +  1;iroot(4;n)  +  1;1;iroot(4;n)  +  1)  \mmember{}  Dec(\mexists{}n1:\mBbbZ{}  [(n1  <  n
                                                                                                                                                                      \mwedge{}  (2  \mleq{}  n1)
                                                                                                                                                                      \mwedge{}  (n1  |  n))])


By

---

Latex:
((Assert  (iroot(4;n)  =  0)  \mvee{}  (iroot(4;n)  =  1)  \mvee{}  (iroot(4;n)  =  2)  BY
                (MoveToConcl  (-1)
                  THEN  GenConclAtAddr  [1;1]
                  THEN  Auto
                  THEN  DVar  `v'
                  THEN  SplitOrHyps
                  THEN  Auto'))
  THEN  (SplitOrHyps
              THEN  (HypSubst'  (-1)  (-3)
                          THEN  RepUR  ``exp``  -3
                          THEN  RepeatFor  3  ((xxx(RWO  "primrec-unroll"  (-3)  THENM  Reduce  (-3))xxx  THENA  Auto))
                          THEN  Auto')\mcdot{}
              )\mcdot{}
  )

---

Home Index