---

Step * 1 2 2 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(last(l_interval(p;j;i))) ∈ Id
BY
{ (RWO "last_l_interval" 0 THEN Auto') }

1
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

---

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(last(l\_interval(p;j;i)))


By

---

Latex:
(RWO  "last\_l\_interval"  0  THEN  Auto')

---

Home Index