---

Step * of Lemma next_wf

∀[k:ℤ]. ∀[p:{i:ℤ| k < i}  ⟶ 𝔹].  (next i > k s.t. ↑p[i]) ∈ {i:ℤ| k < i ∧ (↑p[i]) ∧ (∀j:{k + 1..i-}. (¬↑p[j]))}  supposi\000Cng ∃n:{i:ℤ| k < i} . (↑p[n])
BY
{ ((UnivCD THENA Auto) THEN D -1) }

1
1. k : ℤ
2. p : {i:ℤ| k < i}  ⟶ 𝔹
3. n : {i:ℤ| k < i} 
4. ↑p[n]
⊢ (next i > k s.t. ↑p[i]) ∈ {i:ℤ| k < i ∧ (↑p[i]) ∧ (∀j:{k + 1..i-}. (¬↑p[j]))} 

---

Latex:

---

Latex:
\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{}  (\muparrow{}p[i])  \mwedge{}  (\mforall{}j:\{k  +  1..i\msupminus{}\}.  (\mneg{}\muparrow{}p[j]))\}    supposing  \mexists{}n:\{i:\mBbbZ{}|  \000Ck  <  i\}  .  (\muparrow{}p[n])


By

---

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

---

Home Index