---

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


1. u : IdLnk@i
2. u1 : IdLnk
3. v : IdLnk List
4. ∀q:IdLnk List. ∀i,j,k:Id.  (∃r:IdLnk List. lconnects(r;i;k)) supposing (lconnects(q;j;k) and lconnects([u1 / v];i;j))\000C@i
5. q : IdLnk List@i
6. i : Id@i
7. j : Id@i
8. k : Id@i
9. lpath([u1 / v]) ∧ (destination(u) = source(u1) ∈ Id) ∧ (¬(u1 = lnk-inv(u) ∈ IdLnk)) supposing ¬((||v|| + 1) = 0 ∈ ℤ)
10. (((||v|| + 1) + 1) = 0 ∈ ℤ) ⇒ (i = j ∈ Id)
11. lconnects(q;j;k)
12. i = source(u) ∈ Id
13. j = destination(last([u; [u1 / v]])) ∈ Id
⊢ lconnects([u1 / v];destination(u);j)
BY
{ (((Auto THEN (D (-5))) THENA Auto') THEN Auto) }

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

---

Latex:



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


By

(((Auto  THEN  (D  (-5)))  THENA  Auto')  THEN  Auto)

---

Home Index