---

Step * 2 1 2 2 1 1 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
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
13. u1 : IdLnk
14. v1 : IdLnk List
15. lconnects([u1 / v1];destination(u);k)
16. u1 = lnk-inv(u) ∈ IdLnk
17. destination(u1) = source(u) ∈ Id
⊢ lconnects(v1;i;k)
BY
{ ((((((ParallelOp (-3)) THEN ExRepD THEN (RWO "lpath_cons" (-5))) THENA Auto') THEN ExRepD THEN (D (-3))) THENA Auto')
   THEN ExRepD
   THEN All Reduce
   THEN D 0
   THEN Try (Trivial)
   THEN D 0) }

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
13. u1 : IdLnk
14. v1 : IdLnk List
15. lpath(v1)
16. (destination(u1) = source(hd(v1)) ∈ Id) ∧ (¬(hd(v1) = lnk-inv(u1) ∈ IdLnk)) supposing ¬(||v1|| = 0 ∈ ℤ)
17. ((||v1|| + 1) = 0 ∈ ℤ) ⇒ (destination(u) = k ∈ Id)
18. u1 = lnk-inv(u) ∈ IdLnk
19. destination(u1) = source(u) ∈ Id
20. destination(u) = source(u1) ∈ Id
21. k = destination(last([u1 / v1])) ∈ Id
⊢ (||v1|| = 0 ∈ ℤ) ⇒ (i = k ∈ Id)

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
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
13. u1 : IdLnk
14. v1 : IdLnk List
15. lpath(v1)
16. (destination(u1) = source(hd(v1)) ∈ Id) ∧ (¬(hd(v1) = lnk-inv(u1) ∈ IdLnk)) supposing ¬(||v1|| = 0 ∈ ℤ)
17. ((||v1|| + 1) = 0 ∈ ℤ) ⇒ (destination(u) = k ∈ Id)
18. u1 = lnk-inv(u) ∈ IdLnk
19. destination(u1) = source(u) ∈ Id
20. destination(u) = source(u1) ∈ Id
21. k = destination(last([u1 / v1])) ∈ Id
⊢ (¬(||v1|| = 0 ∈ ℤ)) ⇒ ((i = source(hd(v1)) ∈ Id) ∧ (k = destination(last(v1)) ∈ Id))

---

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
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)  {}\mRightarrow{}  (i  =  j)
10.  lconnects(q;j;k)
11.  i  =  source(u)
12.  j  =  destination(last([u  /  v]))
13.  u1  :  IdLnk
14.  v1  :  IdLnk  List
15.  lconnects([u1  /  v1];destination(u);k)
16.  u1  =  lnk-inv(u)
17.  destination(u1)  =  source(u)
\mvdash{}  lconnects(v1;i;k)


By

((((((ParallelOp  (-3))  THEN  ExRepD  THEN  (RWO  "lpath\_cons"  (-5)))  THENA  Auto')
      THEN  ExRepD
      THEN  (D  (-3)))
    THENA  Auto'
    )
  THEN  ExRepD
  THEN  All  Reduce
  THEN  D  0
  THEN  Try  (Trivial)
  THEN  D  0)

---

Home Index