---

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


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

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

---

Latex:

---

Latex:

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


By

---

Latex:
(RenameVar  `x'  (-2)
  THEN  RenameVar  `y'  (-1)
  THEN  (RepUR  ``class-pred``  0
              THEN  Fold  `class-ap`  0
              THEN  MoveToConcl  (-3)
              THEN  CausalInd'
              THEN  Auto)\mcdot{})

---

Home Index