---

Step * 1 1 of Lemma lpath-members-connected


1. p : IdLnk List
2. i : ℕ||p||
3. j : ℕi + 1
4. lpath(p)
⊢ lpath(l_interval(p;j;i))
BY
{ ((((ParallelOp (-1)) THEN Auto' THEN (InstLemma `length_l_interval` [⌈IdLnk⌉; ⌈p⌉; ⌈i⌉; ⌈j⌉])⋅) THENA Auto')
   THEN RWO "select_l_interval" 0
   THEN Auto'
   THEN Reduce 0
   THEN OnMaybeHyp 4 (\h. ((InstHyp [⌈j + i@0⌉] h)⋅ THEN Auto' THEN All ArithSimp THEN Complete (Auto')))) }

---

Latex:



1.  p  :  IdLnk  List
2.  i  :  \mBbbN{}||p||
3.  j  :  \mBbbN{}i  +  1
4.  lpath(p)
\mvdash{}  lpath(l\_interval(p;j;i))


By

((((ParallelOp  (-1))  THEN  Auto'  THEN  (InstLemma  `length\_l\_interval`  [\mkleeneopen{}IdLnk\mkleeneclose{};  \mkleeneopen{}p\mkleeneclose{};  \mkleeneopen{}i\mkleeneclose{};  \mkleeneopen{}j\mkleeneclose{}])\mcdot{})
    THENA  Auto'
    )
  THEN  RWO  "select\_l\_interval"  0
  THEN  Auto'
  THEN  Reduce  0
  THEN  OnMaybeHyp  4  (\mbackslash{}h.  ((InstHyp  [\mkleeneopen{}j  +  i@0\mkleeneclose{}]  h)\mcdot{}
                                                  THEN  Auto'
                                                  THEN  All  ArithSimp
                                                  THEN  Complete  (Auto'))))

---

Home Index