---

Step * of Lemma proper-divisor_wf

∀[n:ℕ+]. (proper-divisor(n) ∈ Dec(∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))]))
BY
{ (Auto THEN Unfold `proper-divisor` 0 THEN GenConclAtAddr [2;1] THEN Thin (-1) THEN D -1 THEN Reduce 0) }

1
1. n : ℕ+
2. x : ∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))]
⊢ inl x ∈ Dec(∃n1:ℤ [(n1 < n ∧ (2 ≤ n1) ∧ (n1 | n))])

2
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))])

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}\msupplus{}].  (proper-divisor(n)  \mmember{}  Dec(\mexists{}n1:\mBbbZ{}  [(n1  <  n  \mwedge{}  (2  \mleq{}  n1)  \mwedge{}  (n1  |  n))]))


By

---

Latex:
(Auto
  THEN  Unfold  `proper-divisor`  0
  THEN  GenConclAtAddr  [2;1]
  THEN  Thin  (-1)
  THEN  D  -1
  THEN  Reduce  0)

---

Home Index