---

Step * of Lemma es-pstar-q_functionality_wrt_implies

∀es:EO. ∀e1:E. ∀e2:{e:E| loc(e) = loc(e1) ∈ Id} .
  ∀[p,q,p',q':{e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ].
    ((∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ {p[a;b] ⇒ p'[a;b]}))
    ⇒ (∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ {q[a;b] ⇒ q'[a;b]}))
    ⇒ {[e1;e2]~([a,b].p[a;b])*[a,b].q[a;b] ⇒ [e1;e2]~([a,b].p'[a;b])*[a,b].q'[a;b]})
BY
{ (((((Unfold `guard` 0 THEN UnivCD) THENA Auto) THEN (InstLemma `es-pstar-q_wf` [⌜es⌝; ⌜e1⌝; ⌜e2⌝; ⌜p⌝; ⌜q⌝])⋅)
    THENA Auto
    )
   THEN (InstLemma `es-pstar-q_wf` [⌜es⌝; ⌜e1⌝; ⌜e2⌝; ⌜p'⌝; ⌜q'⌝])⋅
   THEN Auto
   THEN let T = Try (OnMember (∀h:hyp. (((InstHyp [⌜i⌝] h)⋅ THENA Auto)
                                        THEN (MoveToConcl (-1) THEN GenConclAtAddr [1;3])
                                        THEN Complete (Auto)) )⋅) in
         ((MoveToHyp 0 (-3))
          THEN (Unfold `es-pstar-q` (-1))
          THEN (Reduce (-1))
          THEN Unfold `es-pstar-q` 0
          THEN Reduce 0
          THEN RepeatFor 2 ((ParallelLast THEN T))
          THEN ExRepD
          THEN Auto
          THEN BackThruSomeHyp
          THEN Auto
          THEN T)) }

1
1. es : EO@i'
2. e1 : E@i
3. e2 : {e:E| loc(e) = loc(e1) ∈ Id} @i
4. [p] : {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ
5. [q] : {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ
6. [p'] : {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ
7. [q'] : {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ
8. ∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ p[a;b] ⇒ p'[a;b])@i
9. ∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ q[a;b] ⇒ q'[a;b])@i
10. [e1;e2]~([a,b].p[a;b])*[a,b].q[a;b] ∈ ℙ
11. [e1;e2]~([a,b].p'[a;b])*[a,b].q'[a;b] ∈ ℙ
12. m : ℕ+
13. f : ℕm ⟶ {e:E| loc(e) = loc(e1) ∈ Id} 
14. (f 0) = e1 ∈ E
15. f (m - 1) ≤loc e2 
16. ∀i:ℕm - 1. (f i <loc f (i + 1))
17. ∀i:ℕm - 1. p[f i;pred(f (i + 1))]
18. q[f (m - 1);e2]
19. (f 0) = e1 ∈ E
20. f (m - 1) ≤loc e2 
21. ∀i:ℕm - 1. (f i <loc f (i + 1))
22. i : ℕm - 1@i
⊢ (f i ∈ [e1, e2])

2
1. es : EO@i'
2. e1 : E@i
3. e2 : {e:E| loc(e) = loc(e1) ∈ Id} @i
4. [p] : {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ
5. [q] : {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ
6. [p'] : {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ
7. [q'] : {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ
8. ∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ p[a;b] ⇒ p'[a;b])@i
9. ∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ q[a;b] ⇒ q'[a;b])@i
10. [e1;e2]~([a,b].p[a;b])*[a,b].q[a;b] ∈ ℙ
11. [e1;e2]~([a,b].p'[a;b])*[a,b].q'[a;b] ∈ ℙ
12. m : ℕ+
13. f : ℕm ⟶ {e:E| loc(e) = loc(e1) ∈ Id} 
14. (f 0) = e1 ∈ E
15. f (m - 1) ≤loc e2 
16. ∀i:ℕm - 1. (f i <loc f (i + 1))
17. ∀i:ℕm - 1. p[f i;pred(f (i + 1))]
18. q[f (m - 1);e2]
19. (f 0) = e1 ∈ E
20. f (m - 1) ≤loc e2 
21. ∀i:ℕm - 1. (f i <loc f (i + 1))
22. i : ℕm - 1@i
⊢ (pred(f (i + 1)) ∈ [e1, e2])

3
1. es : EO@i'
2. e1 : E@i
3. e2 : {e:E| loc(e) = loc(e1) ∈ Id} @i
4. [p] : {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ
5. [q] : {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ
6. [p'] : {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ
7. [q'] : {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ
8. ∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ p[a;b] ⇒ p'[a;b])@i
9. ∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ q[a;b] ⇒ q'[a;b])@i
10. [e1;e2]~([a,b].p[a;b])*[a,b].q[a;b] ∈ ℙ
11. [e1;e2]~([a,b].p'[a;b])*[a,b].q'[a;b] ∈ ℙ
12. m : ℕ+
13. f : ℕm ⟶ {e:E| loc(e) = loc(e1) ∈ Id} 
14. (f 0) = e1 ∈ E
15. f (m - 1) ≤loc e2 
16. ∀i:ℕm - 1. (f i <loc f (i + 1))
17. ∀i:ℕm - 1. p[f i;pred(f (i + 1))]
18. q[f (m - 1);e2]
19. (f 0) = e1 ∈ E
20. f (m - 1) ≤loc e2 
21. ∀i:ℕm - 1. (f i <loc f (i + 1))
22. ∀i:ℕm - 1. p'[f i;pred(f (i + 1))]
⊢ (f (m - 1) ∈ [e1, e2])

4
1. es : EO@i'
2. e1 : E@i
3. e2 : {e:E| loc(e) = loc(e1) ∈ Id} @i
4. [p] : {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ
5. [q] : {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ
6. [p'] : {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ
7. [q'] : {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ {e:E| loc(e) = loc(e1) ∈ Id}  ⟶ ℙ
8. ∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ p[a;b] ⇒ p'[a;b])@i
9. ∀a,b:{e:E| loc(e) = loc(e1) ∈ Id} .  ((a ∈ [e1, e2]) ⇒ (b ∈ [e1, e2]) ⇒ q[a;b] ⇒ q'[a;b])@i
10. [e1;e2]~([a,b].p[a;b])*[a,b].q[a;b] ∈ ℙ
11. [e1;e2]~([a,b].p'[a;b])*[a,b].q'[a;b] ∈ ℙ
12. m : ℕ+
13. f : ℕm ⟶ {e:E| loc(e) = loc(e1) ∈ Id} 
14. (f 0) = e1 ∈ E
15. f (m - 1) ≤loc e2 
16. ∀i:ℕm - 1. (f i <loc f (i + 1))
17. ∀i:ℕm - 1. p[f i;pred(f (i + 1))]
18. q[f (m - 1);e2]
19. (f 0) = e1 ∈ E
20. f (m - 1) ≤loc e2 
21. ∀i:ℕm - 1. (f i <loc f (i + 1))
22. ∀i:ℕm - 1. p'[f i;pred(f (i + 1))]
⊢ (e2 ∈ [e1, e2])

---

Latex:

---

Latex:
\mforall{}es:EO.  \mforall{}e1:E.  \mforall{}e2:\{e:E|  loc(e)  =  loc(e1)\}  .
    \mforall{}[p,q,p',q':\{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \{e:E|  loc(e)  =  loc(e1)\}    {}\mrightarrow{}  \mBbbP{}].
        ((\mforall{}a,b:\{e:E|  loc(e)  =  loc(e1)\}  .    ((a  \mmember{}  [e1,  e2])  {}\mRightarrow{}  (b  \mmember{}  [e1,  e2])  {}\mRightarrow{}  \{p[a;b]  {}\mRightarrow{}  p'[a;b]\}))
        {}\mRightarrow{}  (\mforall{}a,b:\{e:E|  loc(e)  =  loc(e1)\}  .    ((a  \mmember{}  [e1,  e2])  {}\mRightarrow{}  (b  \mmember{}  [e1,  e2])  {}\mRightarrow{}  \{q[a;b]  {}\mRightarrow{}  q'[a;b]\}))
        {}\mRightarrow{}  \{[e1;e2]\msim{}([a,b].p[a;b])*[a,b].q[a;b]  {}\mRightarrow{}  [e1;e2]\msim{}([a,b].p'[a;b])*[a,b].q'[a;b]\})


By

---

Latex:
(((((Unfold  `guard`  0  THEN  UnivCD)  THENA  Auto)
      THEN  (InstLemma  `es-pstar-q\_wf`  [\mkleeneopen{}es\mkleeneclose{};  \mkleeneopen{}e1\mkleeneclose{};  \mkleeneopen{}e2\mkleeneclose{};  \mkleeneopen{}p\mkleeneclose{};  \mkleeneopen{}q\mkleeneclose{}])\mcdot{}
      )
    THENA  Auto
    )
  THEN  (InstLemma  `es-pstar-q\_wf`  [\mkleeneopen{}es\mkleeneclose{};  \mkleeneopen{}e1\mkleeneclose{};  \mkleeneopen{}e2\mkleeneclose{};  \mkleeneopen{}p'\mkleeneclose{};  \mkleeneopen{}q'\mkleeneclose{}])\mcdot{}
  THEN  Auto
  THEN  let  T  =  Try  (OnMember  (\mforall{}h:hyp.  (((InstHyp  [\mkleeneopen{}i\mkleeneclose{}]  h)\mcdot{}  THENA  Auto)
                                                                            THEN  (MoveToConcl  (-1)  THEN  GenConclAtAddr  [1;3])
                                                                            THEN  Complete  (Auto))  )\mcdot{})  in
              ((MoveToHyp  0  (-3))
                THEN  (Unfold  `es-pstar-q`  (-1))
                THEN  (Reduce  (-1))
                THEN  Unfold  `es-pstar-q`  0
                THEN  Reduce  0
                THEN  RepeatFor  2  ((ParallelLast  THEN  T))
                THEN  ExRepD
                THEN  Auto
                THEN  BackThruSomeHyp
                THEN  Auto
                THEN  T))

---

Home Index