---

Step * 1 of Lemma pcw-pp-tail_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. n : ℕ
6. p1 : ℕn ⟶ pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
7. ∀i:ℕn - 1. StepRel(p1 i;p1 (i + 1))
8. ¬(n ≤ 0)
⊢ pcw-pp-tail(<n, p1>) ∈ PartialPath
BY
{ (RepUR ``pcw-pp-tail pcw-pp`` 0 THEN MemTypeCD THEN Reduce 0 THEN Auto) }

---

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.  n  :  \mBbbN{}
6.  p1  :  \mBbbN{}n  {}\mrightarrow{}  pcw-step(P;p.A[p];p,a.B[p;a];p,a,b.C[p;a;b])
7.  \mforall{}i:\mBbbN{}n  -  1.  StepRel(p1  i;p1  (i  +  1))
8.  \mneg{}(n  \mleq{}  0)
\mvdash{}  pcw-pp-tail(<n,  p1>)  \mmember{}  PartialPath


By

---

Latex:
(RepUR  ``pcw-pp-tail  pcw-pp``  0  THEN  MemTypeCD  THEN  Reduce  0  THEN  Auto)

---

Home Index