---

Step * of Lemma iseg-local-property

∀[Info:Type]
  ∀L1,L2:(Id × Info) List.
    (L1 ≤ L2
    ⇒ (∀[P:Id ⟶ Info List+ ⟶ ℙ]
          ∀e:E. (es-local-property(i,L.P[i;L];global-eo(L1);e) ⇐⇒ es-local-property(i,L.P[i;L];global-eo(L2);e))))
BY
{ (InstLemma `iseg-es-embedding` []
   THEN (RepeatFor 4 (ParallelLast') THENA Auto)
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN (InstLemma `embedding-preserves-local-property` [⌜Info⌝;⌜P⌝;⌜global-eo(L1)⌝;⌜global-eo(L2)⌝]⋅ THENA Auto)
   THEN InstHyp [⌜λx.x⌝] (-1)⋅
   THEN Try ((Reduce (-1) THEN InstHyp [⌜e⌝] (-1)⋅ THEN Trivial))
   THEN Try (Trivial)) }

1
.....wf..... 
1. Info : Type
2. L1 : (Id × Info) List@i
3. L2 : (Id × Info) List@i
4. L1 ≤ L2@i
5. (λx.x embeds global-eo(L1) into global-eo(L2))
6. P : Id ⟶ Info List+ ⟶ ℙ
7. e : E@i
8. ∀f:E ⟶ E
     (es-local-embedding(Info;global-eo(L1);global-eo(L2);f)
     ⇒ (∀[e:E]. (es-local-property(i,L.P[i;L];global-eo(L1);e) ⇐⇒ es-local-property(i,L.P[i;L];global-eo(L2);f e))))
⊢ λx.x ∈ E ⟶ E

2
.....antecedent..... 
1. [Info] : Type
2. L1 : (Id × Info) List@i
3. L2 : (Id × Info) List@i
4. L1 ≤ L2@i
5. (λx.x embeds global-eo(L1) into global-eo(L2))
6. [P] : Id ⟶ Info List+ ⟶ ℙ
7. e : E@i
8. ∀f:E ⟶ E
     (es-local-embedding(Info;global-eo(L1);global-eo(L2);f)
     ⇒ (∀[e:E]. (es-local-property(i,L.P[i;L];global-eo(L1);e) ⇐⇒ es-local-property(i,L.P[i;L];global-eo(L2);f e))))
⊢ es-local-embedding(Info;global-eo(L1);global-eo(L2);λx.x)

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}L1,L2:(Id  \mtimes{}  Info)  List.
        (L1  \mleq{}  L2
        {}\mRightarrow{}  (\mforall{}[P:Id  {}\mrightarrow{}  Info  List\msupplus{}  {}\mrightarrow{}  \mBbbP{}]
                    \mforall{}e:E
                        (es-local-property(i,L.P[i;L];global-eo(L1);e)
                        \mLeftarrow{}{}\mRightarrow{}  es-local-property(i,L.P[i;L];global-eo(L2);e))))


By

---

Latex:
(InstLemma  `iseg-es-embedding`  []
  THEN  (RepeatFor  4  (ParallelLast')  THENA  Auto)
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (InstLemma  `embedding-preserves-local-property`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}global-eo(L1)\mkleeneclose{};\mkleeneopen{}global-eo(L2)\mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  InstHyp  [\mkleeneopen{}\mlambda{}x.x\mkleeneclose{}]  (-1)\mcdot{}
  THEN  Try  ((Reduce  (-1)  THEN  InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  (-1)\mcdot{}  THEN  Trivial))
  THEN  Try  (Trivial))

---

Home Index