---

Step * 2 of Lemma lconnects-transitive


1. u : IdLnk@i
2. v : IdLnk List@i
3. ∀q:IdLnk List. ∀i,j,k:Id.  (∃r:IdLnk List. lconnects(r;i;k)) supposing (lconnects(q;j;k) and lconnects(v;i;j))@i
⊢ ∀q:IdLnk List. ∀i,j,k:Id.  (∃r:IdLnk List. lconnects(r;i;k)) supposing (lconnects(q;j;k) and lconnects([u / v];i;j))
BY
{ (((Auto THEN (Unfold `lconnects` (-2)) THEN (Reduce (-2)) THEN ExRepD THEN (D (-2))) THENA Auto') THEN ExRepD) }

1
1. u : IdLnk@i
2. v : IdLnk List@i
3. ∀q:IdLnk List. ∀i,j,k:Id.  (∃r:IdLnk List. lconnects(r;i;k)) supposing (lconnects(q;j;k) and lconnects(v;i;j))@i
4. q : IdLnk List@i
5. i : Id@i
6. j : Id@i
7. k : Id@i
8. lpath([u / v])
9. ((||v|| + 1) = 0 ∈ ℤ) ⇒ (i = j ∈ Id)
10. lconnects(q;j;k)
11. i = source(u) ∈ Id
12. j = destination(last([u / v])) ∈ Id
⊢ ∃r:IdLnk List. lconnects(r;i;k)

---

Latex:



1.  u  :  IdLnk@i
2.  v  :  IdLnk  List@i
3.  \mforall{}q:IdLnk  List.  \mforall{}i,j,k:Id.
          (\mexists{}r:IdLnk  List.  lconnects(r;i;k))  supposing  (lconnects(q;j;k)  and  lconnects(v;i;j))@i
\mvdash{}  \mforall{}q:IdLnk  List.  \mforall{}i,j,k:Id.
        (\mexists{}r:IdLnk  List.  lconnects(r;i;k))  supposing  (lconnects(q;j;k)  and  lconnects([u  /  v];i;j))


By

(((Auto  THEN  (Unfold  `lconnects`  (-2))  THEN  (Reduce  (-2))  THEN  ExRepD  THEN  (D  (-2)))  THENA  Auto')
  THEN  ExRepD
  )

---

Home Index