---

Step * 1 of Lemma bar-diverges-iff


1. T : Type
2. x : bar-base(T)
3. ∀[a:T]. (¬x↓a)
⊢ x↑
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN InstHyp [⌜outl(bar-val(n;x))⌝] 3⋅
   THEN Auto
   THEN D -1
   THEN With ⌜n⌝ (D 0)⋅
   THEN Auto) }

1
1. T : Type
2. x : bar-base(T)
3. ∀[a:T]. (¬x↓a)
4. n : ℕ
5. ↑isl(bar-val(n;x))
⊢ bar-val(n;x) = (inl outl(bar-val(n;x))) ∈ (T?)

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  bar-base(T)
3.  \mforall{}[a:T].  (\mneg{}x\mdownarrow{}a)
\mvdash{}  x\muparrow{}


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  InstHyp  [\mkleeneopen{}outl(bar-val(n;x))\mkleeneclose{}]  3\mcdot{}
  THEN  Auto
  THEN  D  -1
  THEN  With  \mkleeneopen{}n\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto)

---

Home Index