---

Step * of Lemma sequence-class-program_wf

∀[Info,A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[Z:EClass(A)]. ∀[xpr:LocalClass(X)]. ∀[ypr:LocalClass(Y)].
∀[zpr:LocalClass(Z)].
  sequence-class-program(xpr;ypr;zpr) ∈ LocalClass(sequence-class(X;Y;Z)) supposing valueall-type(A)
BY
{ (Auto
   THEN (D (-4) THEN D (-3) THEN D (-2))
   THEN RepUR ``sequence-class-program`` 0
   THEN MemTypeCD
   THEN Auto
   THEN RepUR ``sequence-class class-ap member-eclass`` 0
   THEN (Fold `class-ap` 0
         THEN (Subst ⌜(λe.((¬b¬b(#(X(e)) =z 0)) ∧b (¬b(#(Y(e)) =z 0))))
                      = (λe.(bag-null(X(e)) ∧b (¬bbag-null(Y(e)))))
                      ∈ (E ⟶ 𝔹)⌝ 0⋅
               THENA (Try (Complete (Auto)) THEN RepeatFor 2 ((MemCD THEN Try (Complete (Auto)))) THEN D -2 THEN Auto)
               )
         )
   THEN (RWO "-4" 0 THENA (Try (Complete (Auto)) THEN D -2 THEN Auto))
   THEN (RWO "-8" 0 THENA (Try (Complete (Auto)) THEN D -2 THEN Auto))
   THEN (RWO "-6" 0 THENA (Try (Complete (Auto)) THEN D -2 THEN Auto))) }

1
1. Info : Type
2. A : Type
3. B : Type
4. X : EClass(A)
5. Y : EClass(B)
6. Z : EClass(A)
7. xpr : Id ⟶ hdataflow(Info;A)
8. ∀es:EO+(Info). ∀e:E.  (X(e) = (snd(xpr loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(A))
9. ypr : Id ⟶ hdataflow(Info;B)
10. ∀es:EO+(Info). ∀e:E.  (Y(e) = (snd(ypr loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(B))
11. zpr : Id ⟶ hdataflow(Info;A)
12. ∀es:EO+(Info). ∀e:E.  (Z(e) = (snd(zpr loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(A))
13. valueall-type(A)
14. es : EO+(Info)@i'
15. e : E@i
⊢ case es-first-event(es;λe.(bag-null(snd(xpr loc(e)*(map(λx.info(x);before(e)))(info(e))))
                            ∧b (¬bbag-null(snd(ypr loc(e)*(map(λx.info(x);before(e)))(info(e))))));e)
 of inl(e') =>
 snd(zpr loc(e)*(map(λx.info(x);before(e)))(info(e)))
 | inr(x) =>
 snd(xpr loc(e)*(map(λx.info(x);before(e)))(info(e)))
= (snd(hdf-sequence(xpr loc(e);ypr loc(e);zpr loc(e))*(map(λx.info(x);before(e)))(info(e))))
∈ bag(A)

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].  \mforall{}[Z:EClass(A)].  \mforall{}[xpr:LocalClass(X)].
\mforall{}[ypr:LocalClass(Y)].  \mforall{}[zpr:LocalClass(Z)].
    sequence-class-program(xpr;ypr;zpr)  \mmember{}  LocalClass(sequence-class(X;Y;Z))  supposing  valueall-type(A)


By

---

Latex:
(Auto
  THEN  (D  (-4)  THEN  D  (-3)  THEN  D  (-2))
  THEN  RepUR  ``sequence-class-program``  0
  THEN  MemTypeCD
  THEN  Auto
  THEN  RepUR  ``sequence-class  class-ap  member-eclass``  0
  THEN  (Fold  `class-ap`  0
              THEN  (Subst  \mkleeneopen{}(\mlambda{}e.((\mneg{}\msubb{}\mneg{}\msubb{}(\#(X(e))  =\msubz{}  0))  \mwedge{}\msubb{}  (\mneg{}\msubb{}(\#(Y(e))  =\msubz{}  0))))
                                        =  (\mlambda{}e.(bag-null(X(e))  \mwedge{}\msubb{}  (\mneg{}\msubb{}bag-null(Y(e)))))\mkleeneclose{}  0\mcdot{}
                          THENA  (Try  (Complete  (Auto))
                                        THEN  RepeatFor  2  ((MemCD  THEN  Try  (Complete  (Auto))))
                                        THEN  D  -2
                                        THEN  Auto)
                          )
              )
  THEN  (RWO  "-4"  0  THENA  (Try  (Complete  (Auto))  THEN  D  -2  THEN  Auto))
  THEN  (RWO  "-8"  0  THENA  (Try  (Complete  (Auto))  THEN  D  -2  THEN  Auto))
  THEN  (RWO  "-6"  0  THENA  (Try  (Complete  (Auto))  THEN  D  -2  THEN  Auto)))

---

Home Index