---

Step * 1 of Lemma lpath-members-connected


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]))
BY
{ (Unfold `lconnects` 0 THEN D 0) }

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

2
1. p : IdLnk List
2. i : ℕ||p||
3. j : ℕi + 1
4. lpath(p)
⊢ ((||l_interval(p;j;i)|| = 0 ∈ ℤ) ⇒ (source(p[j]) = source(p[i]) ∈ Id))
∧ ((¬(||l_interval(p;j;i)|| = 0 ∈ ℤ))
  ⇒ ((source(p[j]) = source(hd(l_interval(p;j;i))) ∈ Id) ∧ (source(p[i]) = destination(last(l_interval(p;j;i))) ∈ Id)))

---

Latex:



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


By

(Unfold  `lconnects`  0  THEN  D  0)

---

Home Index