---

Step * 1 of Lemma sequence-classrel


1. Info : Type
2. A : Type
3. B : Type
4. X : EClass(A)
5. Y : EClass(B)
6. Z : EClass(A)
7. es : EO+(Info)
8. e : E
9. v : A
10. v ∈ sequence-class(X;Y;Z)(e)
⊢ ↓((∀e':E. (e' ≤loc e  ⇒ (↑e' ∈b Y) ⇒ (↑e' ∈b X))) ∧ v ∈ X(e))
   ∨ (∃e':E
       (e' ≤loc e  ∧ (↑e' ∈b Y) ∧ (¬↑e' ∈b X) ∧ (∀e'':E. ((e'' <loc e') ⇒ (↑e'' ∈b Y) ⇒ (↑e'' ∈b X))) ∧ v ∈ Z(e)))
BY
{ (RepUR ``sequence-class classrel`` (-1)
   THEN GenHypAtAddr (-1) [3;1]
   THEN DProdsAndUnions
   THEN AllReduce
   THEN Try (Complete (Auto))
   THEN RepUR ``class-ap`` (-1)
   THEN Fold `classrel` (-1)
   THEN Repeat (AllPushDown)
   THEN Try ((D 0
              THEN (OrRight THENA Auto)
              THEN (InstConcl [⌜x⌝]⋅ THEN Auto)
              THEN OnMaybeHyp 14 (\h. Complete (((InstHyp [⌜e''⌝] h⋅ THEN Auto)
                                                 THEN (RWO "not_over_and" (-1) THENA Auto)
                                                 THEN D (-1)
                                                 THEN Auto
                                                 THEN SupposeNot)))))
   THEN D 0
   THEN OrLeft
   THEN Auto
   THEN Try (OnMaybeHyp 14 (\h. Complete (((InstHyp [⌜e'⌝] h⋅ THEN Auto)
                                           THEN (RWO "not_over_and" (-1) THENA Auto)
                                           THEN D (-1)
                                           THEN Auto
                                           THEN SupposeNot))))) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  X  :  EClass(A)
5.  Y  :  EClass(B)
6.  Z  :  EClass(A)
7.  es  :  EO+(Info)
8.  e  :  E
9.  v  :  A
10.  v  \mmember{}  sequence-class(X;Y;Z)(e)
\mvdash{}  \mdownarrow{}((\mforall{}e':E.  (e'  \mleq{}loc  e    {}\mRightarrow{}  (\muparrow{}e'  \mmember{}\msubb{}  Y)  {}\mRightarrow{}  (\muparrow{}e'  \mmember{}\msubb{}  X)))  \mwedge{}  v  \mmember{}  X(e))
      \mvee{}  (\mexists{}e':E
              (e'  \mleq{}loc  e 
              \mwedge{}  (\muparrow{}e'  \mmember{}\msubb{}  Y)
              \mwedge{}  (\mneg{}\muparrow{}e'  \mmember{}\msubb{}  X)
              \mwedge{}  (\mforall{}e'':E.  ((e''  <loc  e')  {}\mRightarrow{}  (\muparrow{}e''  \mmember{}\msubb{}  Y)  {}\mRightarrow{}  (\muparrow{}e''  \mmember{}\msubb{}  X)))
              \mwedge{}  v  \mmember{}  Z(e)))


By

---

Latex:
(RepUR  ``sequence-class  classrel``  (-1)
  THEN  GenHypAtAddr  (-1)  [3;1]
  THEN  DProdsAndUnions
  THEN  AllReduce
  THEN  Try  (Complete  (Auto))
  THEN  RepUR  ``class-ap``  (-1)
  THEN  Fold  `classrel`  (-1)
  THEN  Repeat  (AllPushDown)
  THEN  Try  ((D  0
                        THEN  (OrRight  THENA  Auto)
                        THEN  (InstConcl  [\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)
                        THEN  OnMaybeHyp  14  (\mbackslash{}h.  Complete  (((InstHyp  [\mkleeneopen{}e''\mkleeneclose{}]  h\mcdot{}  THEN  Auto)
                                                                                              THEN  (RWO  "not\_over\_and"  (-1)  THENA  Auto)
                                                                                              THEN  D  (-1)
                                                                                              THEN  Auto
                                                                                              THEN  SupposeNot)))))
  THEN  D  0
  THEN  OrLeft
  THEN  Auto
  THEN  Try  (OnMaybeHyp  14  (\mbackslash{}h.  Complete  (((InstHyp  [\mkleeneopen{}e'\mkleeneclose{}]  h\mcdot{}  THEN  Auto)
                                                                                  THEN  (RWO  "not\_over\_and"  (-1)  THENA  Auto)
                                                                                  THEN  D  (-1)
                                                                                  THEN  Auto
                                                                                  THEN  SupposeNot)))))

---

Home Index