---

Step * 1 1 of Lemma pW-sup_wf


1. P : Type
2. A : P ⟶ Type
3. B : p:P ⟶ A[p] ⟶ Type
4. C : p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P
5. pco-W ∈ P ⟶ Type
6. par : P
7. a : A[par]
8. f : b:B[par;a] ⟶ (pW C[par;a;b])
9. pW-sup(a;f) ∈ pco-W par
10. path : Path
11. StepAgree(path 0;par;pW-sup(a;f))
⊢ ↓∃n:ℕ. Barred(pcw-partial(path;n))
BY
{ (MoveToConcl (-1)
   THEN (GenConclTerm ⌜path 0⌝⋅ THENA Auto)
   THEN (D 0 THENA Auto)
   THEN RepeatFor 2 (D (-3))
   THEN RepUR ``pcw-step-agree`` (-1)
   THEN D -1
   THEN pcoWD (-5)
   THEN D -5
   THEN All Reduce
   THEN Unfold `pW-sup` (-1)) }

1
1. P : Type
2. A : P ⟶ Type
3. B : p:P ⟶ A[p] ⟶ Type
4. C : p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P
5. pco-W ∈ P ⟶ Type
6. par : P
7. a : A[par]
8. f : b:B[par;a] ⟶ (pW C[par;a;b])
9. pW-sup(a;f) ∈ pco-W par
10. path : Path
11. p : P
12. a1 : A[p]
13. w1 : b:B[p;a1] ⟶ (pco-W C[p;a1;b])
14. v2 : B[p;a1]?
15. (path 0) = <p, <a1, w1>, v2> ∈ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
16. p = par ∈ P
17. <a1, w1> = <a, f> ∈ (pco-W par)
⊢ ↓∃n:ℕ. Barred(pcw-partial(path;n))

---

Latex:

---

Latex:

1.  P  :  Type
2.  A  :  P  {}\mrightarrow{}  Type
3.  B  :  p:P  {}\mrightarrow{}  A[p]  {}\mrightarrow{}  Type
4.  C  :  p:P  {}\mrightarrow{}  a:A[p]  {}\mrightarrow{}  B[p;a]  {}\mrightarrow{}  P
5.  pco-W  \mmember{}  P  {}\mrightarrow{}  Type
6.  par  :  P
7.  a  :  A[par]
8.  f  :  b:B[par;a]  {}\mrightarrow{}  (pW  C[par;a;b])
9.  pW-sup(a;f)  \mmember{}  pco-W  par
10.  path  :  Path
11.  StepAgree(path  0;par;pW-sup(a;f))
\mvdash{}  \mdownarrow{}\mexists{}n:\mBbbN{}.  Barred(pcw-partial(path;n))


By

---

Latex:
(MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}path  0\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  RepeatFor  2  (D  (-3))
  THEN  RepUR  ``pcw-step-agree``  (-1)
  THEN  D  -1
  THEN  pcoWD  (-5)
  THEN  D  -5
  THEN  All  Reduce
  THEN  Unfold  `pW-sup`  (-1))

---

Home Index