---

Step * 1 of Lemma 0-dim-complex-polyhedron-decidable

.....decidable?..... 
1. k : ℕ
2. K : 0-dim-complex
3. ∀x:|K|. ∃i:ℕ||K||. req-vec(k;x;λj.rat2real(fst((K[i] j))))
4. x : |K|
5. y : |K|
6. i1 : ℕ||K||
7. req-vec(k;x;λj.rat2real(fst((K[i1] j))))
8. i : ℕ||K||
9. req-vec(k;y;λj.rat2real(fst((K[i] j))))
10. req-vec(k;λj.rat2real(fst((K[i1] j)));λj.rat2real(fst((K[i] j)))) supposing req-vec(k;x;y)
11. req-vec(k;x;y) supposing req-vec(k;λj.rat2real(fst((K[i1] j)));λj.rat2real(fst((K[i] j))))
⊢ Dec(req-vec(k;λj.rat2real(fst((K[i1] j)));λj.rat2real(fst((K[i] j)))))
BY
{ ((Unfold `req-vec` 0 THEN Reduce 0)
   THEN BLemma `decidable__all_int_seg`
   THEN Auto
   THEN RWO "req-rat2real" 0
   THEN Auto) }

---

Latex:

---

Latex:
.....decidable?..... 
1.  k  :  \mBbbN{}
2.  K  :  0-dim-complex
3.  \mforall{}x:|K|.  \mexists{}i:\mBbbN{}||K||.  req-vec(k;x;\mlambda{}j.rat2real(fst((K[i]  j))))
4.  x  :  |K|
5.  y  :  |K|
6.  i1  :  \mBbbN{}||K||
7.  req-vec(k;x;\mlambda{}j.rat2real(fst((K[i1]  j))))
8.  i  :  \mBbbN{}||K||
9.  req-vec(k;y;\mlambda{}j.rat2real(fst((K[i]  j))))
10.  req-vec(k;\mlambda{}j.rat2real(fst((K[i1]  j)));\mlambda{}j.rat2real(fst((K[i]  j))))  supposing  req-vec(k;x;y)
11.  req-vec(k;x;y)  supposing  req-vec(k;\mlambda{}j.rat2real(fst((K[i1]  j)));\mlambda{}j.rat2real(fst((K[i]  j))))
\mvdash{}  Dec(req-vec(k;\mlambda{}j.rat2real(fst((K[i1]  j)));\mlambda{}j.rat2real(fst((K[i]  j)))))


By

---

Latex:
((Unfold  `req-vec`  0  THEN  Reduce  0)
  THEN  BLemma  `decidable\_\_all\_int\_seg`
  THEN  Auto
  THEN  RWO  "req-rat2real"  0
  THEN  Auto)

---

Home Index