---

Step * 4 2 1 of Lemma lpath_cons


1. l : IdLnk
2. u : IdLnk
3. v : IdLnk List
4. lpath([u / v])
5. destination(l) = source(u) ∈ Id
6. ¬(u = lnk-inv(l) ∈ IdLnk)
⊢ lpath([l; [u / v]])
BY
{ ((((((ParallelOp (-3)) THEN D 0) THENA Auto) THEN CaseNat 0 `i' THEN Reduce 0 THEN Auto THEN RWO "select_cons_tl" 0)
    THENA Auto'
    )
   THEN (InstHyp [⌈i - 1⌉] 4)⋅
   THEN Auto') }

---

Latex:



1.  l  :  IdLnk
2.  u  :  IdLnk
3.  v  :  IdLnk  List
4.  lpath([u  /  v])
5.  destination(l)  =  source(u)
6.  \mneg{}(u  =  lnk-inv(l))
\mvdash{}  lpath([l;  [u  /  v]])


By

((((((ParallelOp  (-3))  THEN  D  0)  THENA  Auto)
      THEN  CaseNat  0  `i'
      THEN  Reduce  0
      THEN  Auto
      THEN  RWO  "select\_cons\_tl"  0)
    THENA  Auto'
    )
  THEN  (InstHyp  [\mkleeneopen{}i  -  1\mkleeneclose{}]  4)\mcdot{}
  THEN  Auto')

---

Home Index