---

Step * 1 1 1 of Lemma once-class-program_wf


1. Info : Type
2. B : Type
3. X : EClass(B)
4. es : EO+(Info)@i'
5. e : E@i
6. z : hdataflow(Info;B)@i
⊢ (∀e':E. (e' ≤loc e  ⇒ (X(e') = (snd(z*(map(λx.info(x);before(e')))(info(e')))) ∈ bag(B))))
⇒ (hdf-once(z)*(map(λx.info(x);before(e)))
   = hdf-once(if isl(class-pred(X;es;e)) then hdf-halt() else z*(map(λx.info(x);before(e))) fi )
   ∈ hdataflow(Info;B))
BY
{ (RepUR ``class-pred`` 0 THEN Fold `class-ap` 0 THEN MoveToConcl (-2) THEN CausalInd' THEN Auto) }

1
1. Info : Type
2. B : Type
3. X : EClass(B)
4. es : EO+(Info)@i'
5. z : hdataflow(Info;B)@i
6. e : E@i
7. ∀e1:E
     ((e1 < e)
     ⇒ (∀e':E. (e' ≤loc e1  ⇒ (X(e') = (snd(z*(map(λx.info(x);before(e')))(info(e')))) ∈ bag(B))))
     ⇒ (hdf-once(z)*(map(λx.info(x);before(e1)))
        = hdf-once(if isl(last(λe'.0 <z #(X(e'))) e1) then hdf-halt() else z*(map(λx.info(x);before(e1))) fi )
        ∈ hdataflow(Info;B)))
8. ∀e':E. (e' ≤loc e  ⇒ (X(e') = (snd(z*(map(λx.info(x);before(e')))(info(e')))) ∈ bag(B)))@i
⊢ hdf-once(z)*(map(λx.info(x);before(e)))
= hdf-once(if isl(last(λe'.0 <z #(X(e'))) e) then hdf-halt() else z*(map(λx.info(x);before(e))) fi )
∈ hdataflow(Info;B)

---

Latex:

---

Latex:

1.  Info  :  Type
2.  B  :  Type
3.  X  :  EClass(B)
4.  es  :  EO+(Info)@i'
5.  e  :  E@i
6.  z  :  hdataflow(Info;B)@i
\mvdash{}  (\mforall{}e':E.  (e'  \mleq{}loc  e    {}\mRightarrow{}  (X(e')  =  (snd(z*(map(\mlambda{}x.info(x);before(e')))(info(e')))))))
{}\mRightarrow{}  (hdf-once(z)*(map(\mlambda{}x.info(x);before(e)))
      =  hdf-once(if  isl(class-pred(X;es;e))  then  hdf-halt()  else  z*(map(\mlambda{}x.info(x);before(e)))  fi  ))


By

---

Latex:
(RepUR  ``class-pred``  0  THEN  Fold  `class-ap`  0  THEN  MoveToConcl  (-2)  THEN  CausalInd'  THEN  Auto)

---

Home Index