---

Step * of Lemma sequence-classrel

∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[Z:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:A].
  uiff(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
{ Auto }

1
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)))

2
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. ↓((∀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)))
⊢ v ∈ sequence-class(X;Y;Z)(e)

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].  \mforall{}[Z:EClass(A)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[v:A].
    uiff(v  \mmember{}  sequence-class(X;Y;Z)(e);\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:
Auto

---

Home Index