---

Step * of Lemma pcw-pp-tail_wf

∀[P:Type]. ∀[A:P ⟶ Type]. ∀[B:p:P ⟶ A[p] ⟶ Type]. ∀[C:p:P ⟶ a:A[p] ⟶ B[p;a] ⟶ P]. ∀[pp:PartialPath].
  pcw-pp-tail(pp) ∈ PartialPath supposing ¬↑pcw-pp-null(pp)
BY
{ (Auto THEN D -2 THEN D -3 THEN RepUR ``pcw-pp-null`` -1 THEN (SimplifyAssert (-1) THENA Auto) THEN Reduce (-2)) }

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. 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

---

Latex:

---

Latex:
\mforall{}[P:Type].  \mforall{}[A:P  {}\mrightarrow{}  Type].  \mforall{}[B:p:P  {}\mrightarrow{}  A[p]  {}\mrightarrow{}  Type].  \mforall{}[C:p:P  {}\mrightarrow{}  a:A[p]  {}\mrightarrow{}  B[p;a]  {}\mrightarrow{}  P].
\mforall{}[pp:PartialPath].
    pcw-pp-tail(pp)  \mmember{}  PartialPath  supposing  \mneg{}\muparrow{}pcw-pp-null(pp)


By

---

Latex:
(Auto
  THEN  D  -2
  THEN  D  -3
  THEN  RepUR  ``pcw-pp-null``  -1
  THEN  (SimplifyAssert  (-1)  THENA  Auto)
  THEN  Reduce  (-2))

---

Home Index