---

Step * of Lemma lpath-members-connected

∀[p:IdLnk List]. ∀[i:ℕ||p||]. ∀[j:ℕi + 1].  lconnects(l_interval(p;j;i);source(p[j]);source(p[i])) supposing lpath(p)
BY
{ Auto 
⋅ }

1
1. p : IdLnk List
2. i : ℕ||p||
3. j : ℕi + 1
4. lpath(p)
⊢ lconnects(l_interval(p;j;i);source(p[j]);source(p[i]))

---

Latex:


\mforall{}[p:IdLnk  List].  \mforall{}[i:\mBbbN{}||p||].  \mforall{}[j:\mBbbN{}i  +  1].
    lconnects(l\_interval(p;j;i);source(p[j]);source(p[i]))  supposing  lpath(p)


By

Auto 
\mcdot{}

---

Home Index