---

Step * 1 1 1 1 1 of Lemma list-continuity


1. X : ℕ ⟶ Type
2. d : ℤ
3. x : ⋂n:ℕ. ((X n) List)
4. x ∈ (X 0) List
5. u : X 0
6. v : (X 0) List
7. x = [u / v] ∈ ((X 0) List)
8. (||v|| + 1) ≤ 0
⊢ [u / v] ~ []
BY
{ ((Assert 0 ≤ ||v|| BY Auto) THEN Auto) }

---

Latex:

---

Latex:

1.  X  :  \mBbbN{}  {}\mrightarrow{}  Type
2.  d  :  \mBbbZ{}
3.  x  :  \mcap{}n:\mBbbN{}.  ((X  n)  List)
4.  x  \mmember{}  (X  0)  List
5.  u  :  X  0
6.  v  :  (X  0)  List
7.  x  =  [u  /  v]
8.  (||v||  +  1)  \mleq{}  0
\mvdash{}  [u  /  v]  \msim{}  []


By

---

Latex:
((Assert  0  \mleq{}  ||v||  BY  Auto)  THEN  Auto)

---

Home Index