---

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


1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. path : Path
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. [%10] : 0 < 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 ∈ ℤ)
12. copath-length(pcw-path-coPath(i - 1;path)) = (i - 1) ∈ ℤ
⊢ Barred(pcw-partial(path;i))
BY
{ (RepUR ``pcw-pp-barred`` 0
   THEN MoveToConcl (-2)
   THEN Unfold `pcw-path-coPath` 0
   THEN (SplitOnConclITE THENA Auto)
   THEN Try ((Assert ⌜False⌝⋅ THEN Complete (Auto)))
   THEN RepUR ``let`` 0
   THEN (GenConclTerm ⌜path (i - 1)⌝⋅ THENA Auto)
   THEN RepeatFor 3 (D -2)
   THEN Reduce 0) }

1
1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. path : Path
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. [%10] : 0 < 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 - 1;path)) = (i - 1) ∈ ℤ
12. ¬(i = 0 ∈ ℤ)
13. p : Unit
14. w1 : pco-W p
15. x : B[fst(w1)]
16. (path (i - 1)) = <p, w1, inl x> ∈ pcw-step(Unit;p.A;p,a.B[a];p,a,b.⋅)
⊢ (¬(copath-length(if (copath-length(pcw-path-coPath(i - 1;path)) =z i - 1)
then copath-extend(pcw-path-coPath(i - 1;path);x)
else ()
fi )
= i
∈ ℤ))
⇒ (0 < i ∧ False)

2
1. A : 𝕌'
2. B : A ⟶ Type
3. w : coW(A;a.B[a])
4. path : Path
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. [%10] : 0 < 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 - 1;path)) = (i - 1) ∈ ℤ
12. ¬(i = 0 ∈ ℤ)
13. p : Unit
14. w1 : pco-W p
15. y : Unit
16. (path (i - 1)) = <p, w1, inr y > ∈ pcw-step(Unit;p.A;p,a.B[a];p,a,b.⋅)
⊢ (¬(0 = i ∈ ℤ)) ⇒ (0 < i ∧ True)

---

Latex:

---

Latex:

1.  A  :  \mBbbU{}'
2.  B  :  A  {}\mrightarrow{}  Type
3.  w  :  coW(A;a.B[a])
4.  path  :  Path
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  :  \mBbbZ{}
9.  [\%10]  :  0  <  i
10.  (\mneg{}(copath-length(pcw-path-coPath(i  -  1;path))  =  (i  -  1)))  {}\mRightarrow{}  (\mexists{}n:\mBbbN{}.  Barred(pcw-partial(path;n)))
11.  \mneg{}(copath-length(pcw-path-coPath(i;path))  =  i)
12.  copath-length(pcw-path-coPath(i  -  1;path))  =  (i  -  1)
\mvdash{}  Barred(pcw-partial(path;i))


By

---

Latex:
(RepUR  ``pcw-pp-barred``  0
  THEN  MoveToConcl  (-2)
  THEN  Unfold  `pcw-path-coPath`  0
  THEN  (SplitOnConclITE  THENA  Auto)
  THEN  Try  ((Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Complete  (Auto)))
  THEN  RepUR  ``let``  0
  THEN  (GenConclTerm  \mkleeneopen{}path  (i  -  1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepeatFor  3  (D  -2)
  THEN  Reduce  0)

---

Home Index