---

Step * of Lemma lconnects-transitive

∀p,q:IdLnk List. ∀i,j,k:Id.  (∃r:IdLnk List. lconnects(r;i;k)) supposing (lconnects(q;j;k) and lconnects(p;i;j))
BY
{ InductionOnList }

1
∀q:IdLnk List. ∀i,j,k:Id.  (∃r:IdLnk List. lconnects(r;i;k)) supposing (lconnects(q;j;k) and lconnects([];i;j))

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

---

Latex:


\mforall{}p,q:IdLnk  List.  \mforall{}i,j,k:Id.
    (\mexists{}r:IdLnk  List.  lconnects(r;i;k))  supposing  (lconnects(q;j;k)  and  lconnects(p;i;j))


By

InductionOnList

---

Home Index