---

Step * of Lemma lpath_cons

∀[l:IdLnk]. ∀[p:IdLnk List].
  uiff(lpath([l / p]);lpath(p)
  ∧ (destination(l) = source(hd(p)) ∈ Id) ∧ (¬(hd(p) = lnk-inv(l) ∈ IdLnk)) supposing ¬(||p|| = 0 ∈ ℤ))
BY
{ Auto' }

1
1. l : IdLnk
2. p : IdLnk List
3. lpath([l / p])
⊢ lpath(p)

2
1. l : IdLnk
2. p : IdLnk List
3. lpath([l / p])
4. ¬(||p|| = 0 ∈ ℤ)
⊢ destination(l) = source(hd(p)) ∈ Id

3
1. l : IdLnk
2. p : IdLnk List
3. lpath([l / p])
4. ¬(||p|| = 0 ∈ ℤ)
⊢ ¬(hd(p) = lnk-inv(l) ∈ IdLnk)

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

---

Latex:


\mforall{}[l:IdLnk].  \mforall{}[p:IdLnk  List].
    uiff(lpath([l  /  p]);lpath(p)
    \mwedge{}  (destination(l)  =  source(hd(p)))  \mwedge{}  (\mneg{}(hd(p)  =  lnk-inv(l)))  supposing  \mneg{}(||p||  =  0))


By

Auto'

---

Home Index