Step
*
2
of Lemma
lpath_cons
1. l : IdLnk
2. p : 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