---

Step * 2 of Lemma proper-divisor_wf


1. n : ℕ+
2. y : Top
⊢ if n <z 5 then if (n =z 4) then inl 2 else inr (λx.any x)  fi 
  if n <z 16 then proper-divisor-aux(n;2;2;1;2)
  if n <z 81 then proper-divisor-aux(n;3;3;1;3)
  else eval m = iroot(4;n) + 1 in
       proper-divisor-aux(n;m;m;1;m)
  fi  ∈ Dec(∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))])
BY
{ RepeatFor 2 (OldAutoSplit)⋅ }

1
1. n : ℕ+
2. y : Top
3. n < 5
4. n = 4 ∈ ℤ
⊢ inl 2 ∈ Dec(∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))])

2
1. n : ℕ+
2. y : Top
3. n < 5
4. ¬(n = 4 ∈ ℤ)
⊢ inr (λx.any x)  ∈ Dec(∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))])

3
1. n : ℕ+
2. y : Top
3. 5 ≤ n
4. 16 ≤ n
⊢ if n <z 81 then proper-divisor-aux(n;3;3;1;3) else eval m = iroot(4;n) + 1 in proper-divisor-aux(n;m;m;1;m) fi 
  ∈ Dec(∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))])

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}\msupplus{}
2.  y  :  Top
\mvdash{}  if  n  <z  5  then  if  (n  =\msubz{}  4)  then  inl  2  else  inr  (\mlambda{}x.any  x)    fi 
    if  n  <z  16  then  proper-divisor-aux(n;2;2;1;2)
    if  n  <z  81  then  proper-divisor-aux(n;3;3;1;3)
    else  eval  m  =  iroot(4;n)  +  1  in
              proper-divisor-aux(n;m;m;1;m)
    fi    \mmember{}  Dec(\mexists{}n1:\mBbbZ{}  [(n1  <  n  \mwedge{}  (2  \mleq{}  n1)  \mwedge{}  (n1  |  n))])


By

---

Latex:
RepeatFor  2  (OldAutoSplit)\mcdot{}

---

Home Index