---

Step * of Lemma loc-on-path-append

∀es:EO. ∀L1,L2:E List. ∀i:Id.  (loc-on-path(es;i;L1 @ L2) ⇐⇒ loc-on-path(es;i;L1) ∨ loc-on-path(es;i;L2))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `loc-on-path` 0
   THEN (RWO "map_append_sq" 0 THENA Auto)
   THEN (RWO "member_append" 0 THENA Auto)
   THEN Fold `loc-on-path` 0
   THEN Auto) }

---

Latex:


\mforall{}es:EO.  \mforall{}L1,L2:E  List.  \mforall{}i:Id.
    (loc-on-path(es;i;L1  @  L2)  \mLeftarrow{}{}\mRightarrow{}  loc-on-path(es;i;L1)  \mvee{}  loc-on-path(es;i;L2))


By

((UnivCD  THENA  Auto)
  THEN  Unfold  `loc-on-path`  0
  THEN  (RWO  "map\_append\_sq"  0  THENA  Auto)
  THEN  (RWO  "member\_append"  0  THENA  Auto)
  THEN  Fold  `loc-on-path`  0
  THEN  Auto)

---

Home Index