---

Step * of Lemma loc-on-path-decomp

∀[Info:Type]
  ∀es:EO+(Info). ∀Sys:EClass(Top). ∀L:E(Sys) List. ∀j:Id.
    (loc-on-path(es;j;L)
    ⇒ (∃u:E(Sys)
         ∃A,B:E(Sys) List. ((loc(u) = j ∈ Id) ∧ (L = (A @ [u / B]) ∈ (E(Sys) List)) ∧ (¬loc-on-path(es;j;A)))))
BY
{ InductionOnList }

1
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)))))

2
1. [Info] : Type
2. es : EO+(Info)@i'
3. Sys : EClass(Top)@i'
4. u : E(Sys)@i
5. v : E(Sys) List@i
6. ∀j:Id
     (loc-on-path(es;j;v)
     ⇒ (∃u:E(Sys)
          ∃A,B:E(Sys) List. ((loc(u) = j ∈ Id) ∧ (v = (A @ [u / B]) ∈ (E(Sys) List)) ∧ (¬loc-on-path(es;j;A)))))@i
⊢ ∀j:Id
    (loc-on-path(es;j;[u / v])
    ⇒ (∃u@0:E(Sys)
         ∃A,B:E(Sys) List
          ((loc(u@0) = j ∈ Id) ∧ ([u / v] = (A @ [u@0 / B]) ∈ (E(Sys) List)) ∧ (¬loc-on-path(es;j;A)))))

---

Latex:


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


By

InductionOnList

---

Home Index