---

Step * 2 of Lemma altW-item_wf

.....set predicate..... 
1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. coW-wfdd(a.B[a];w)
5. b : coW-dom(a.B[a];w)
⊢ coW-wfdd(a.B[a];altW-item(w;b))
BY
{ (Unfold `altW-item` 0 THEN ParallelOp -2 THEN (D 0 THENA Auto) THEN D -1) }

1
1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. ∀p:{p:n:ℕ ⟶ copath(a.B[a];w)| 
       ∀i:ℕ
         ((copath-length(p i) = i ∈ ℤ)
         ⇒ (copath-length(p (i + 1)) = (i + 1) ∈ ℤ)
         ⇒ copathAgree(a.B[a];w;p i;p (i + 1)))} 
     (↓∃i:ℕ. (¬(copath-length(p i) = i ∈ ℤ)))
5. b : coW-dom(a.B[a];w)
6. p : n:ℕ ⟶ copath(a.B[a];coW-item(w;b))@i
7. ∀i:ℕ
     ((copath-length(p i) = i ∈ ℤ)
     ⇒ (copath-length(p (i + 1)) = (i + 1) ∈ ℤ)
     ⇒ copathAgree(a.B[a];coW-item(w;b);p i;p (i + 1)))
⊢ ↓∃i:ℕ. (¬(copath-length(p i) = i ∈ ℤ))

---

Latex:

---

Latex:
.....set  predicate..... 
1.  A  :  \mBbbU{}'
2.  B  :  A  {}\mrightarrow{}  Type
3.  w  :  coW(A;a.B[a])
4.  coW-wfdd(a.B[a];w)
5.  b  :  coW-dom(a.B[a];w)
\mvdash{}  coW-wfdd(a.B[a];altW-item(w;b))


By

---

Latex:
(Unfold  `altW-item`  0  THEN  ParallelOp  -2  THEN  (D  0  THENA  Auto)  THEN  D  -1)

---

Home Index