---

Step * of Lemma embedding-preserves-local-relation

∀[Info:Type]. ∀[R:Id ─→ Id ─→ Info List+ ─→ Info List+ ─→ ℙ]. ∀[eo1:EO+(Info)].
  ∀eo2:EO+(Info). ∀f:E ─→ E.
    (es-local-embedding(Info;eo1;eo2;f)
    ⇒ (∀[e1,e2:E].
          (es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo1;e1;e2)
          ⇐⇒ es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo2;f e1;f e2))))
BY
{ (Auto
   THEN ParallelLast
   THEN NthHypEq (-1)
   THEN EqCD
   THEN Auto
   THEN RepeatFor 3 (((EqTypeCD ORELSE EqCD)
                      THEN Auto
                      THEN Try ((Symmetry THEN Complete (Auto)))
                      THEN Try ((Unfold `es-le-before` 0 THEN RWO "length-append" 0 THEN Auto'))))) }

---

Latex:


\mforall{}[Info:Type].  \mforall{}[R:Id  {}\mrightarrow{}  Id  {}\mrightarrow{}  Info  List\msupplus{}  {}\mrightarrow{}  Info  List\msupplus{}  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[eo1:EO+(Info)].
    \mforall{}eo2:EO+(Info).  \mforall{}f:E  {}\mrightarrow{}  E.
        (es-local-embedding(Info;eo1;eo2;f)
        {}\mRightarrow{}  (\mforall{}[e1,e2:E].
                    (es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo1;e1;e2)
                    \mLeftarrow{}{}\mRightarrow{}  es-local-relation(i,j,L1,L2.R[i;j;L1;L2];eo2;f  e1;f  e2))))


By

(Auto
  THEN  ParallelLast
  THEN  NthHypEq  (-1)
  THEN  EqCD
  THEN  Auto
  THEN  RepeatFor  3  (((EqTypeCD  ORELSE  EqCD)
                                        THEN  Auto
                                        THEN  Try  ((Symmetry  THEN  Complete  (Auto)))
                                        THEN  Try  ((Unfold  `es-le-before`  0  THEN  RWO  "length-append"  0  THEN  Auto')))))

---

Home Index