---

Step * of Lemma iseg-local-relation

∀[Info:Type]
  ∀L1,L2:(Id × Info) List.
    (L1 ≤ L2
    ⇒ (∀[R:Id ⟶ Id ⟶ Info List+ ⟶ Info List+ ⟶ ℙ]
          ∀e1,e2:E.
            (es-local-relation(i,j,L1,L2.R[i;j;L1;L2];global-eo(L1);e1;e2)
            ⇐⇒ es-local-relation(i,j,L1,L2.R[i;j;L1;L2];global-eo(L2);e1;e2))))
BY
{ (InstLemma `iseg-es-embedding` []
   THEN (RepeatFor 4 (ParallelLast') THENA Auto)
   THEN RepeatFor 3 ((D 0 THENA Auto))
   THEN (InstLemma `embedding-preserves-local-relation` [⌜Info⌝;⌜R⌝;⌜global-eo(L1)⌝;⌜global-eo(L2)⌝]⋅ THENA Auto)
   THEN InstHyp [⌜λx.x⌝] (-1)⋅
   THEN Try ((Reduce (-1) THEN InstHyp [⌜e1⌝;⌜e2⌝] (-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. R : Id ⟶ Id ⟶ Info List+ ⟶ Info List+ ⟶ ℙ
7. e1 : E@i
8. e2 : E@i
9. ∀f:E ⟶ E
     (es-local-embedding(Info;global-eo(L1);global-eo(L2);f)
     ⇒ (∀[e1,e2:E].
           (es-local-relation(i,j,L1,L2.R[i;j;L1;L2];global-eo(L1);e1;e2)
           ⇐⇒ es-local-relation(i,j,L1,L2.R[i;j;L1;L2];global-eo(L2);f e1;f e2))))
⊢ λ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. [R] : Id ⟶ Id ⟶ Info List+ ⟶ Info List+ ⟶ ℙ
7. e1 : E@i
8. e2 : E@i
9. ∀f:E ⟶ E
     (es-local-embedding(Info;global-eo(L1);global-eo(L2);f)
     ⇒ (∀[e1,e2:E].
           (es-local-relation(i,j,L1,L2.R[i;j;L1;L2];global-eo(L1);e1;e2)
           ⇐⇒ es-local-relation(i,j,L1,L2.R[i;j;L1;L2];global-eo(L2);f e1;f e2))))
⊢ 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{}[R:Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  Info  List\msupplus{}  {}\mrightarrow{}  Info  List\msupplus{}  {}\mrightarrow{}  \mBbbP{}]
                    \mforall{}e1,e2:E.
                        (es-local-relation(i,j,L1,L2.R[i;j;L1;L2];global-eo(L1);e1;e2)
                        \mLeftarrow{}{}\mRightarrow{}  es-local-relation(i,j,L1,L2.R[i;j;L1;L2];global-eo(L2);e1;e2))))


By

---

Latex:
(InstLemma  `iseg-es-embedding`  []
  THEN  (RepeatFor  4  (ParallelLast')  THENA  Auto)
  THEN  RepeatFor  3  ((D  0  THENA  Auto))
  THEN  (InstLemma  `embedding-preserves-local-relation`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}R\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{}e1\mkleeneclose{};\mkleeneopen{}e2\mkleeneclose{}]  (-1)\mcdot{}  THEN  Trivial))
  THEN  Try  (Trivial))

---

Home Index