---

Step * 1 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
BY
{ (Subst' ⌈i = j ∈ ℤ⌉ 0⋅ THEN Auto')⋅ }

---

Latex:



1.  p  :  IdLnk  List
2.  i  :  \mBbbN{}||p||
3.  j  :  \mBbbN{}i  +  1
4.  lpath(p)
5.  (i  -  j)  =  0
\mvdash{}  source(p[j])  =  source(p[i])


By

(Subst'  \mkleeneopen{}i  =  j\mkleeneclose{}  0\mcdot{}  THEN  Auto')\mcdot{}

---

Home Index