---

Step * 1 of Lemma int-problem-dimension_wf


1. x : ⋃n:ℕ.({L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List × ({L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List))
⊢ dim(inl x) ∈ ℕ
BY
{ (D_union 1 THEN RepeatFor 2 (D 2)) }

1
1. n : ℕ
2. {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
⊢ dim(inl <[], %3>) ∈ ℕ

2
1. n : ℕ
2. u : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ} 
3. v : {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
4. {L:ℤ List| ||L|| = (n + 1) ∈ ℤ}  List
⊢ dim(inl <[u / v], %3>) ∈ ℕ

---

Latex:

---

Latex:

1.  x  :  \mcup{}n:\mBbbN{}.(\{L:\mBbbZ{}  List|  ||L||  =  (n  +  1)\}    List  \mtimes{}  (\{L:\mBbbZ{}  List|  ||L||  =  (n  +  1)\}    List))
\mvdash{}  dim(inl  x)  \mmember{}  \mBbbN{}


By

---

Latex:
(D\_union  1  THEN  RepeatFor  2  (D  2))

---

Home Index