---

Step * 4 of Lemma lpath_cons


1. l : IdLnk
2. p : IdLnk List
3. lpath(p)
4. (destination(l) = source(hd(p)) ∈ Id) ∧ (¬(hd(p) = lnk-inv(l) ∈ IdLnk)) supposing ¬(||p|| = 0 ∈ ℤ)
⊢ lpath([l / p])
BY
{ DVar `p' }

1
1. l : IdLnk
2. lpath([])
3. (destination(l) = source(hd([])) ∈ Id) ∧ (¬(hd([]) = lnk-inv(l) ∈ IdLnk)) supposing ¬(||[]|| = 0 ∈ ℤ)
⊢ lpath([l])

2
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]])

---

Latex:



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


By

DVar  `p'

---

Home Index