Step * 2 of Lemma lpath_cons


1. IdLnk
2. IdLnk List
3. lpath([l p])
4. ¬(||p|| 0 ∈ ℤ)
⊢ destination(l) source(hd(p)) ∈ Id
BY
((((Unfold `lpath` (-2)) THEN (InstHyp [⌈0⌉(-2))⋅THENA Auto')
   THEN (Reduce (-1))
   THEN Auto
   THEN (NthHypEq (-2))
   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{}  destination(l)  =  source(hd(p))


By

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




Home Index