---

Step * 1 1 1 of Lemma posint_reduc_dec

.....decidable?..... 
1. a : |<ℤ+,*>|
⊢ Dec(∃b:ℕ+. ((¬(b = 1 ∈ ℤ)) ∧ (b | a) ∧ (¬(a | b))))
BY
{ AbReduce 1 THEN ((RWH (LemmaC `pdivisor_bound`) 0) THENA Auto) }

1
1. a : ℕ+
⊢ Dec(∃b:ℕ+. ((¬(b = 1 ∈ ℤ)) ∧ b < a ∧ (b | a)))

---

Latex:

---

Latex:
.....decidable?..... 
1.  a  :  |<\mBbbZ{}\msupplus{},*>|
\mvdash{}  Dec(\mexists{}b:\mBbbN{}\msupplus{}.  ((\mneg{}(b  =  1))  \mwedge{}  (b  |  a)  \mwedge{}  (\mneg{}(a  |  b))))


By

---

Latex:
AbReduce  1  THEN  ((RWH  (LemmaC  `pdivisor\_bound`)  0)  THENA  Auto)

---

Home Index