---

Step * 1 of Lemma decidable__all-unit-ball-approx

.....decidable?..... 
1. k : ℕ
2. [P] : unit-ball-approx(0;k) ⟶ ℙ
3. ∀p:unit-ball-approx(0;k). Dec(P[p])
⊢ Dec(∀p:unit-ball-approx(0;k). P[p])
BY
{ ((InstLemma `unit-ball-approx0` [⌜k⌝]⋅ THENA Auto)
   THEN D -1
   THEN (D 3 With ⌜⋅⌝  THENA (SubsumeC ⌜Top⌝⋅ THEN Auto))
   THEN RepeatFor 2 (ParallelLast)
   THEN Try (ParallelLast)) }

1
1. k : ℕ
2. [P] : unit-ball-approx(0;k) ⟶ ℙ
3. unit-ball-approx(0;k) ⊆r Top
4. Top ⊆r unit-ball-approx(0;k)
5. P[⋅]
⊢ ∀p:unit-ball-approx(0;k). P[p]

2
1. k : ℕ
2. P : unit-ball-approx(0;k) ⟶ ℙ
3. unit-ball-approx(0;k) ⊆r Top
4. Top ⊆r unit-ball-approx(0;k)
5. ∀p:unit-ball-approx(0;k). P[p]
⊢ P[⋅]

---

Latex:

---

Latex:
.....decidable?..... 
1.  k  :  \mBbbN{}
2.  [P]  :  unit-ball-approx(0;k)  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}p:unit-ball-approx(0;k).  Dec(P[p])
\mvdash{}  Dec(\mforall{}p:unit-ball-approx(0;k).  P[p])


By

---

Latex:
((InstLemma  `unit-ball-approx0`  [\mkleeneopen{}k\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  (D  3  With  \mkleeneopen{}\mcdot{}\mkleeneclose{}    THENA  (SubsumeC  \mkleeneopen{}Top\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  RepeatFor  2  (ParallelLast)
  THEN  Try  (ParallelLast))

---

Home Index