---

Step * 1 of Lemma lpath_cons


1. l : IdLnk
2. p : IdLnk List
3. lpath([l / p])
⊢ lpath(p)
BY
{ ((((((((((ParallelOp (-1)) THEN D 0) THENA Auto) THEN (InstHyp [⌈i + 1⌉] (-2))⋅) THENA Auto')
       THEN (RWO "select_cons_tl" (-1))
       )
      THENA Auto'
      )
     THEN (Subst ⌈(i + 1) - 1 ~ i⌉ (-1))⋅
     )
    THENL [Auto; Id]
   )
   THEN (Subst ⌈((i + 1) + 1) - 1 ~ i + 1⌉ (-1))⋅
   THEN Auto) }

---

Latex:



1.  l  :  IdLnk
2.  p  :  IdLnk  List
3.  lpath([l  /  p])
\mvdash{}  lpath(p)


By

((((((((((ParallelOp  (-1))  THEN  D  0)  THENA  Auto)  THEN  (InstHyp  [\mkleeneopen{}i  +  1\mkleeneclose{}]  (-2))\mcdot{})  THENA  Auto')
          THEN  (RWO  "select\_cons\_tl"  (-1))
          )
        THENA  Auto'
        )
      THEN  (Subst  \mkleeneopen{}(i  +  1)  -  1  \msim{}  i\mkleeneclose{}  (-1))\mcdot{}
      )
    THENL  [Auto;  Id]
  )
  THEN  (Subst  \mkleeneopen{}((i  +  1)  +  1)  -  1  \msim{}  i  +  1\mkleeneclose{}  (-1))\mcdot{}
  THEN  Auto)

---

Home Index