---

Step * 2 1 1 1 1 of Lemma lconnects-transitive


1. u : IdLnk@i
2. ∀q:IdLnk List. ∀i,j,k:Id.  (∃r:IdLnk List. lconnects(r;i;k)) supposing (lconnects(q;j;k) and lconnects([];i;j))@i
3. q : IdLnk List@i
4. i : Id@i
5. j : Id@i
6. k : Id@i
7. lpath([]) ∧ (destination(u) = source(hd([])) ∈ Id) ∧ (¬(hd([]) = lnk-inv(u) ∈ IdLnk)) supposing ¬(0 = 0 ∈ ℤ)
8. (1 = 0 ∈ ℤ) ⇒ (i = j ∈ Id)
9. lconnects(q;j;k)
10. i = source(u) ∈ Id
11. j = destination(last([u])) ∈ Id
⊢ lconnects([];destination(u);j)
BY
{ ((Unfold `last` (-1)) THEN (Reduce (-1)) THEN Unfold `lconnects` 0 THEN Reduce 0 THEN Auto) }

---

Latex:



1.  u  :  IdLnk@i
2.  \mforall{}q:IdLnk  List.  \mforall{}i,j,k:Id.
          (\mexists{}r:IdLnk  List.  lconnects(r;i;k))  supposing  (lconnects(q;j;k)  and  lconnects([];i;j))@i
3.  q  :  IdLnk  List@i
4.  i  :  Id@i
5.  j  :  Id@i
6.  k  :  Id@i
7.  lpath([])  \mwedge{}  (destination(u)  =  source(hd([])))  \mwedge{}  (\mneg{}(hd([])  =  lnk-inv(u)))  supposing  \mneg{}(0  =  0)
8.  (1  =  0)  {}\mRightarrow{}  (i  =  j)
9.  lconnects(q;j;k)
10.  i  =  source(u)
11.  j  =  destination(last([u]))
\mvdash{}  lconnects([];destination(u);j)


By

((Unfold  `last`  (-1))  THEN  (Reduce  (-1))  THEN  Unfold  `lconnects`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index