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