---

Step * 1 2 2 1 of Lemma lpath-members-connected


1. p : IdLnk List
2. i : ℕ||p||
3. j : ℕi + 1
4. lpath(p)
5. ((i - j) = 0 ∈ ℤ) ⇒ (source(p[j]) = source(p[i]) ∈ Id)
6. ¬((i - j) = 0 ∈ ℤ)
7. source(p[j]) = source(hd(l_interval(p;j;i))) ∈ Id
⊢ source(p[i]) = destination(p[i - 1]) ∈ Id
BY
{ ((Unfold `lpath` 4) THEN (InstHyp [⌜i - 1⌝] 4)⋅ THEN Auto')⋅ }

---

Latex:

---

Latex:

1.  p  :  IdLnk  List
2.  i  :  \mBbbN{}||p||
3.  j  :  \mBbbN{}i  +  1
4.  lpath(p)
5.  ((i  -  j)  =  0)  {}\mRightarrow{}  (source(p[j])  =  source(p[i]))
6.  \mneg{}((i  -  j)  =  0)
7.  source(p[j])  =  source(hd(l\_interval(p;j;i)))
\mvdash{}  source(p[i])  =  destination(p[i  -  1])


By

---

Latex:
((Unfold  `lpath`  4)  THEN  (InstHyp  [\mkleeneopen{}i  -  1\mkleeneclose{}]  4)\mcdot{}  THEN  Auto')\mcdot{}

---

Home Index