---

Step * of Lemma is-latest-pair

∀[Info,A,B:Type].
  ∀X:EClass(A). ∀Y:EClass(B). ∀es:EO+(Info). ∀e:E.
    (↑e ∈b (X&Y) ⇐⇒ ((↑e ∈b X) ∧ ((↑e ∈b Y) ∨ (↑e ∈b Prior(Y)))) ∨ ((↑e ∈b Y) ∧ ((↑e ∈b X) ∨ (↑e ∈b Prior(X)))))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``latest-pair eclass-compose4 in-eclass`` 0
   THEN Try (Fold `in-eclass` 0)
   THEN Repeat (AutoSplit)
   THEN Auto
   THEN RepeatFor 2 ((SplitOrHyps THEN Auto))⋅) }

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].
    \mforall{}X:EClass(A).  \mforall{}Y:EClass(B).  \mforall{}es:EO+(Info).  \mforall{}e:E.
        (\muparrow{}e  \mmember{}\msubb{}  (X\&Y)
        \mLeftarrow{}{}\mRightarrow{}  ((\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  ((\muparrow{}e  \mmember{}\msubb{}  Y)  \mvee{}  (\muparrow{}e  \mmember{}\msubb{}  Prior(Y))))  \mvee{}  ((\muparrow{}e  \mmember{}\msubb{}  Y)  \mwedge{}  ((\muparrow{}e  \mmember{}\msubb{}  X)  \mvee{}  (\muparrow{}e  \mmember{}\msubb{}  Prior(X)))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  RepUR  ``latest-pair  eclass-compose4  in-eclass``  0
  THEN  Try  (Fold  `in-eclass`  0)
  THEN  Repeat  (AutoSplit)
  THEN  Auto
  THEN  RepeatFor  2  ((SplitOrHyps  THEN  Auto))\mcdot{})

---

Home Index