---

Step * 1 1 of Lemma until-class-program_wf

.....assertion..... 
1. Info : Type
2. B : Type
3. C : Type
4. X : EClass(B)
5. Y : EClass(C)
6. xpr : Id ⟶ hdataflow(Info;B)
7. ∀es:EO+(Info). ∀e:E.  (X(e) = (snd(xpr loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(B))
8. ypr : Id ⟶ hdataflow(Info;C)
9. ∀es:EO+(Info). ∀e:E.  (Y(e) = (snd(ypr loc(e)*(map(λx.info(x);before(e)))(info(e)))) ∈ bag(C))
10. es : EO+(Info)@i'
11. e : E@i
⊢ hdf-until(xpr loc(e);ypr loc(e))*(map(λx.info(x);before(e)))
= hdf-until(if isl(class-pred(Y;es;e))
  then hdf-halt()
  else xpr loc(e)*(map(λx.info(x);before(e)))
  fi ;ypr loc(e)*(map(λx.info(x);before(e))))
∈ hdataflow(Info;B)
BY
{ ((Assert ∀e':E. (e' ≤loc e  ⇒ (X(e') = (snd(xpr loc(e)*(map(λx.info(x);before(e')))(info(e')))) ∈ bag(B))) BY
          Auto)
   THEN Thin (-6)
   THEN (Assert ∀e':E. (e' ≤loc e  ⇒ (Y(e') = (snd(ypr loc(e)*(map(λx.info(x);before(e')))(info(e')))) ∈ bag(C))) BY
               Auto)
   THEN Thin (-5)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN (GenApply 6 THENA Auto)
   THEN ThinVar `xpr'
   THEN (GenApply 6 THENA Auto)
   THEN ThinVar `ypr') }

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

---

Latex:

---

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


By

---

Latex:
((Assert  \mforall{}e':E
                      (e'  \mleq{}loc  e    {}\mRightarrow{}  (X(e')  =  (snd(xpr  loc(e)*(map(\mlambda{}x.info(x);before(e')))(info(e'))))))  BY
                Auto)
  THEN  Thin  (-6)
  THEN  (Assert  \mforall{}e':E
                                (e'  \mleq{}loc  e 
                                {}\mRightarrow{}  (Y(e')  =  (snd(ypr  loc(e)*(map(\mlambda{}x.info(x);before(e')))(info(e'))))))  BY
                          Auto)
  THEN  Thin  (-5)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  (GenApply  6  THENA  Auto)
  THEN  ThinVar  `xpr'
  THEN  (GenApply  6  THENA  Auto)
  THEN  ThinVar  `ypr')

---

Home Index