---

Step * 4 2 of Lemma lpath_cons


1. l : IdLnk
2. u : IdLnk
3. v : IdLnk List
4. lpath([u / v])
5. (destination(l) = source(hd([u / v])) ∈ Id) ∧ (¬(hd([u / v]) = lnk-inv(l) ∈ IdLnk)) supposing ¬(||[u / v]|| = 0 ∈ ℤ)
⊢ lpath([l; [u / v]])
BY
{ (((D (-1)) THENA Auto') THEN (Reduce (-1)) THEN Auto) }

1
1. l : IdLnk
2. u : IdLnk
3. v : IdLnk List
4. lpath([u / v])
5. destination(l) = source(u) ∈ Id
6. ¬(u = lnk-inv(l) ∈ IdLnk)
⊢ lpath([l; [u / v]])

---

Latex:



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


By

(((D  (-1))  THENA  Auto')  THEN  (Reduce  (-1))  THEN  Auto)

---

Home Index