---

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


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
7. j : Id@i
8. loc-on-path(es;j;v)
9. ¬(loc(u) = j ∈ Id)
10. u1 : E(Sys)
11. ∃A,B:E(Sys) List. ((loc(u1) = j ∈ Id) ∧ (v = (A @ [u1 / B]) ∈ (E(Sys) List)) ∧ (¬loc-on-path(es;j;A)))
⊢ ∃A,B:E(Sys) List. ((loc(u1) = j ∈ Id) ∧ ([u / v] = (A @ [u1 / B]) ∈ (E(Sys) List)) ∧ (¬loc-on-path(es;j;A)))
BY
{ ExRepD }

1
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
7. j : Id@i
8. loc-on-path(es;j;v)
9. ¬(loc(u) = j ∈ Id)
10. u1 : E(Sys)
11. A : E(Sys) List
12. B : E(Sys) List
13. loc(u1) = j ∈ Id
14. v = (A @ [u1 / B]) ∈ (E(Sys) List)
15. ¬loc-on-path(es;j;A)
⊢ ∃A,B:E(Sys) List. ((loc(u1) = j ∈ Id) ∧ ([u / v] = (A @ [u1 / B]) ∈ (E(Sys) List)) ∧ (¬loc-on-path(es;j;A)))

---

Latex:



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.  \mforall{}j:Id
          (loc-on-path(es;j;v)
          {}\mRightarrow{}  (\mexists{}u:E(Sys)
                    \mexists{}A,B:E(Sys)  List.  ((loc(u)  =  j)  \mwedge{}  (v  =  (A  @  [u  /  B]))  \mwedge{}  (\mneg{}loc-on-path(es;j;A)))))@i
7.  j  :  Id@i
8.  loc-on-path(es;j;v)
9.  \mneg{}(loc(u)  =  j)
10.  u1  :  E(Sys)
11.  \mexists{}A,B:E(Sys)  List.  ((loc(u1)  =  j)  \mwedge{}  (v  =  (A  @  [u1  /  B]))  \mwedge{}  (\mneg{}loc-on-path(es;j;A)))
\mvdash{}  \mexists{}A,B:E(Sys)  List.  ((loc(u1)  =  j)  \mwedge{}  ([u  /  v]  =  (A  @  [u1  /  B]))  \mwedge{}  (\mneg{}loc-on-path(es;j;A)))


By

ExRepD

---

Home Index