---

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:

---

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

---

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

---

Home Index