---

Step * 1 of Lemma locl-pre-preserving-compose


1. es : EO@i'
2. [P] : E ─→ ℙ
3. [Q] : E ─→ ℙ
4. f1 : {e:E| P e}  ─→ {e:E| Q e} @i
5. f2 : {e:E| Q e}  ─→ E@i
6. f1 is locl-pre-preserving on P@i
7. f2 is locl-pre-preserving on Q@i
⊢ f2 o f1 is locl-pre-preserving on P
BY
{ ((InstLemma `rel-pre-preserving-compose` [⌈es⌉;⌈P⌉;⌈Q⌉;⌈λe,e'. e ≤loc e' ⌉; ⌈f1⌉;⌈f2⌉]⋅ THENA Auto)
   THEN skip{(Fold `locl-pre-preserving` (-1) THEN Trivial)}
   ) }

1
1. es : EO@i'
2. [P] : E ─→ ℙ
3. [Q] : E ─→ ℙ
4. f1 : {e:E| P e}  ─→ {e:E| Q e} @i
5. f2 : {e:E| Q e}  ─→ E@i
6. f1 is locl-pre-preserving on P@i
7. f2 is locl-pre-preserving on Q@i
8. f2 o f1 is λe,e'. e ≤loc e' -pre-preserving on P
⊢ f2 o f1 is locl-pre-preserving on P

---

Latex:



1.  es  :  EO@i'
2.  [P]  :  E  {}\mrightarrow{}  \mBbbP{}
3.  [Q]  :  E  {}\mrightarrow{}  \mBbbP{}
4.  f1  :  \{e:E|  P  e\}    {}\mrightarrow{}  \{e:E|  Q  e\}  @i
5.  f2  :  \{e:E|  Q  e\}    {}\mrightarrow{}  E@i
6.  f1  is  locl-pre-preserving  on  P@i
7.  f2  is  locl-pre-preserving  on  Q@i
\mvdash{}  f2  o  f1  is  locl-pre-preserving  on  P


By

((InstLemma  `rel-pre-preserving-compose`  [\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}Q\mkleeneclose{};\mkleeneopen{}\mlambda{}e,e'.  e  \mleq{}loc  e'  \mkleeneclose{};  \mkleeneopen{}f1\mkleeneclose{};\mkleeneopen{}f2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  skip\{(Fold  `locl-pre-preserving`  (-1)  THEN  Trivial)\}
  )

---

Home Index