---

Step * 1 1 1 1 of Lemma coW-is-W


1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. path : Path@i'
5. StepAgree(path 0;⋅;w)
6. ∀[n:ℕ]
     ((pcw-path-coPath(n;path) ∈ copath(a.B[a];w))
     ∧ ((copath-length(pcw-path-coPath(n;path)) = n ∈ ℤ)
       ⇒ (copath-at(w;pcw-path-coPath(n;path)) = (fst(snd((path n)))) ∈ coW(A;a.B[a]))))
7. ∀n:ℕ. (pcw-path-coPath(n;path) ∈ copath(a.B[a];w))
8. i : ℕ
9. ¬(copath-length(pcw-path-coPath(i;path)) = i ∈ ℤ)
⊢ ∃n:ℕ. Barred(pcw-partial(path;n))
BY
{ ((NatInd (-2) THENM D 0) THENW Auto) }

1
1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. path : Path@i'
5. StepAgree(path 0;⋅;w)
6. ∀[n:ℕ]
     ((pcw-path-coPath(n;path) ∈ copath(a.B[a];w))
     ∧ ((copath-length(pcw-path-coPath(n;path)) = n ∈ ℤ)
       ⇒ (copath-at(w;pcw-path-coPath(n;path)) = (fst(snd((path n)))) ∈ coW(A;a.B[a]))))
7. ∀n:ℕ. (pcw-path-coPath(n;path) ∈ copath(a.B[a];w))
8. ¬(copath-length(pcw-path-coPath(0;path)) = 0 ∈ ℤ)
⊢ ∃n:ℕ. Barred(pcw-partial(path;n))

2
1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. path : Path@i'
5. StepAgree(path 0;⋅;w)
6. ∀[n:ℕ]
     ((pcw-path-coPath(n;path) ∈ copath(a.B[a];w))
     ∧ ((copath-length(pcw-path-coPath(n;path)) = n ∈ ℤ)
       ⇒ (copath-at(w;pcw-path-coPath(n;path)) = (fst(snd((path n)))) ∈ coW(A;a.B[a]))))
7. ∀n:ℕ. (pcw-path-coPath(n;path) ∈ copath(a.B[a];w))
⊢ copath-length(pcw-path-coPath(0;path)) ∈ ℤ

3
1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. path : Path@i'
5. StepAgree(path 0;⋅;w)
6. ∀[n:ℕ]
     ((pcw-path-coPath(n;path) ∈ copath(a.B[a];w))
     ∧ ((copath-length(pcw-path-coPath(n;path)) = n ∈ ℤ)
       ⇒ (copath-at(w;pcw-path-coPath(n;path)) = (fst(snd((path n)))) ∈ coW(A;a.B[a]))))
7. ∀n:ℕ. (pcw-path-coPath(n;path) ∈ copath(a.B[a];w))
8. i : ℤ@i
9. [%10] : 0 < i@i
10. (¬(copath-length(pcw-path-coPath(i - 1;path)) = (i - 1) ∈ ℤ)) ⇒ (∃n:ℕ. Barred(pcw-partial(path;n)))
11. ¬(copath-length(pcw-path-coPath(i;path)) = i ∈ ℤ)
⊢ ∃n:ℕ. Barred(pcw-partial(path;n))

4
1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. path : Path@i'
5. StepAgree(path 0;⋅;w)
6. ∀[n:ℕ]
     ((pcw-path-coPath(n;path) ∈ copath(a.B[a];w))
     ∧ ((copath-length(pcw-path-coPath(n;path)) = n ∈ ℤ)
       ⇒ (copath-at(w;pcw-path-coPath(n;path)) = (fst(snd((path n)))) ∈ coW(A;a.B[a]))))
7. ∀n:ℕ. (pcw-path-coPath(n;path) ∈ copath(a.B[a];w))
8. i : ℤ@i
9. 0 < i
10. (¬(copath-length(pcw-path-coPath(i - 1;path)) = (i - 1) ∈ ℤ)) ⇒ (∃n:ℕ. Barred(pcw-partial(path;n)))
⊢ copath-length(pcw-path-coPath(i;path)) ∈ ℤ

5
1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. path : Path@i'
5. StepAgree(path 0;⋅;w)
6. ∀[n:ℕ]
     ((pcw-path-coPath(n;path) ∈ copath(a.B[a];w))
     ∧ ((copath-length(pcw-path-coPath(n;path)) = n ∈ ℤ)
       ⇒ (copath-at(w;pcw-path-coPath(n;path)) = (fst(snd((path n)))) ∈ coW(A;a.B[a]))))
7. ∀n:ℕ. (pcw-path-coPath(n;path) ∈ copath(a.B[a];w))
8. i : ℤ@i
9. 0 < i
⊢ copath-length(pcw-path-coPath(i - 1;path)) ∈ ℤ

6
1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. path : Path@i'
5. StepAgree(path 0;⋅;w)
6. ∀[n:ℕ]
     ((pcw-path-coPath(n;path) ∈ copath(a.B[a];w))
     ∧ ((copath-length(pcw-path-coPath(n;path)) = n ∈ ℤ)
       ⇒ (copath-at(w;pcw-path-coPath(n;path)) = (fst(snd((path n)))) ∈ coW(A;a.B[a]))))
7. ∀n:ℕ. (pcw-path-coPath(n;path) ∈ copath(a.B[a];w))
8. i : ℕ
9. (¬(copath-length(pcw-path-coPath(0;path)) = 0 ∈ ℤ)) ⇒ (∃n:ℕ. Barred(pcw-partial(path;n)))
10. ∀i:{n:ℤ| 0 < n} 
      (((¬(copath-length(pcw-path-coPath(i - 1;path)) = (i - 1) ∈ ℤ)) ⇒ (∃n:ℕ. Barred(pcw-partial(path;n))))
      ⇒ (¬(copath-length(pcw-path-coPath(i;path)) = i ∈ ℤ))
      ⇒ (∃n:ℕ. Barred(pcw-partial(path;n))))
11. i1 : ℕ@i
⊢ copath-length(pcw-path-coPath(i1;path)) ∈ ℤ

---

Latex:

---

Latex:

1.  A  :  \mBbbU{}'
2.  B  :  A  {}\mrightarrow{}  Type
3.  w  :  coW(A;a.B[a])
4.  path  :  Path@i'
5.  StepAgree(path  0;\mcdot{};w)
6.  \mforall{}[n:\mBbbN{}]
          ((pcw-path-coPath(n;path)  \mmember{}  copath(a.B[a];w))
          \mwedge{}  ((copath-length(pcw-path-coPath(n;path))  =  n)
              {}\mRightarrow{}  (copath-at(w;pcw-path-coPath(n;path))  =  (fst(snd((path  n)))))))
7.  \mforall{}n:\mBbbN{}.  (pcw-path-coPath(n;path)  \mmember{}  copath(a.B[a];w))
8.  i  :  \mBbbN{}
9.  \mneg{}(copath-length(pcw-path-coPath(i;path))  =  i)
\mvdash{}  \mexists{}n:\mBbbN{}.  Barred(pcw-partial(path;n))


By

---

Latex:
((NatInd  (-2)  THENM  D  0)  THENW  Auto)

---

Home Index