---

Step * 3 of Lemma lpath_cons


1. l : IdLnk
2. p : IdLnk List
3. lpath([l / p])
4. ¬(||p|| = 0 ∈ ℤ)
⊢ ¬(hd(p) = lnk-inv(l) ∈ IdLnk)
BY
{ ((((Unfold `lpath` (-2)) THEN (InstHyp [⌈0⌉] (-2))⋅) THENA Auto')
   THEN (Reduce (-1))
   THEN Auto
   THEN (NthHypEq (-1))
   THEN EqCD
   THEN Auto
   THEN EqCD
   THEN Auto
   THEN DVar `p'
   THEN All Reduce
   THEN Auto') }

---

Latex:



1.  l  :  IdLnk
2.  p  :  IdLnk  List
3.  lpath([l  /  p])
4.  \mneg{}(||p||  =  0)
\mvdash{}  \mneg{}(hd(p)  =  lnk-inv(l))


By

((((Unfold  `lpath`  (-2))  THEN  (InstHyp  [\mkleeneopen{}0\mkleeneclose{}]  (-2))\mcdot{})  THENA  Auto')
  THEN  (Reduce  (-1))
  THEN  Auto
  THEN  (NthHypEq  (-1))
  THEN  EqCD
  THEN  Auto
  THEN  EqCD
  THEN  Auto
  THEN  DVar  `p'
  THEN  All  Reduce
  THEN  Auto')

---

Home Index