---

Step * 1 of Lemma next_wf_bound

.....basecase..... 
1. b : ℤ
⊢ ∀[k:ℤ]. ∀[p:{i:ℤ| k < i}  ⟶ 𝔹].
    (next i > k s.t. ↑p[i]) ∈ {i:ℤ| (k < i ∧ (i ≤ (k + 0))) ∧ (↑p[i]) ∧ (∀j:{k + 1..i-}. (¬↑p[j]))}  
    supposing ∃n:{i:ℤ| k < i ∧ (i ≤ (k + 0))} . (↑p[n])
BY
{ xxx((UnivCD THENA Auto) THEN (D (-1) THEN D -2) THEN Auto)xxx }

---

Latex:

---

Latex:
.....basecase..... 
1.  b  :  \mBbbZ{}
\mvdash{}  \mforall{}[k:\mBbbZ{}].  \mforall{}[p:\{i:\mBbbZ{}|  k  <  i\}    {}\mrightarrow{}  \mBbbB{}].
        (next  i  >  k  s.t.  \muparrow{}p[i])  \mmember{}  \{i:\mBbbZ{}|  (k  <  i  \mwedge{}  (i  \mleq{}  (k  +  0)))  \mwedge{}  (\muparrow{}p[i])  \mwedge{}  (\mforall{}j:\{k  +  1..i\msupminus{}\}.  (\mneg{}\muparrow{}p[j]))\}  \000C 
        supposing  \mexists{}n:\{i:\mBbbZ{}|  k  <  i  \mwedge{}  (i  \mleq{}  (k  +  0))\}  .  (\muparrow{}p[n])


By

---

Latex:
xxx((UnivCD  THENA  Auto)  THEN  (D  (-1)  THEN  D  -2)  THEN  Auto)xxx

---

Home Index