---

Step * 1 of Lemma loc-on-path-decomp


1. [Info] : Type
2. es : EO+(Info)@i'
3. Sys : EClass(Top)@i'
⊢ ∀j:Id
    (loc-on-path(es;j;[])
    ⇒ (∃u:E(Sys)
         ∃A,B:E(Sys) List. ((loc(u) = j ∈ Id) ∧ ([] = (A @ [u / B]) ∈ (E(Sys) List)) ∧ (¬loc-on-path(es;j;A)))))
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN FLemma `loc-on-path-nil` [-1] THEN Auto) }

---

Latex:



1.  [Info]  :  Type
2.  es  :  EO+(Info)@i'
3.  Sys  :  EClass(Top)@i'
\mvdash{}  \mforall{}j:Id
        (loc-on-path(es;j;[])
        {}\mRightarrow{}  (\mexists{}u:E(Sys)
                  \mexists{}A,B:E(Sys)  List.  ((loc(u)  =  j)  \mwedge{}  ([]  =  (A  @  [u  /  B]))  \mwedge{}  (\mneg{}loc-on-path(es;j;A)))))


By

(RepeatFor  2  ((D  0  THENA  Auto))  THEN  FLemma  `loc-on-path-nil`  [-1]  THEN  Auto)

---

Home Index