---

Step * 4 1 of Lemma lpath_cons


1. l : IdLnk
2. lpath([])
3. (destination(l) = source(hd([])) ∈ Id) ∧ (¬(hd([]) = lnk-inv(l) ∈ IdLnk)) supposing ¬(||[]|| = 0 ∈ ℤ)
⊢ lpath([l])
BY
{ (Unfold `lpath` 0 THEN Reduce 0 THEN Auto) }

---

Latex:



1.  l  :  IdLnk
2.  lpath([])
3.  (destination(l)  =  source(hd([])))  \mwedge{}  (\mneg{}(hd([])  =  lnk-inv(l)))  supposing  \mneg{}(||[]||  =  0)
\mvdash{}  lpath([l])


By

(Unfold  `lpath`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index