---

Step * 1 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. 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)
BY
{ (RecUnfold `es-before` 0
   THEN RecUnfold `es-local-pred` 0
   THEN Reduce 0
   THEN AutoSplit
   THEN (RWW "map_append_sq iterate-hdf-append" 0 THENA Auto)
   THEN Reduce 0
   THEN (InstHyp [⌜pred(e)⌝] (-3)⋅ THENA Auto)
   THEN (HypSubst (-1) 0 THENA AutoSplit)) }

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. ¬↑first(e)
11. ∀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)))
12. ∀e':E. (e' ≤loc e  ⇒ (X(e') = (snd(x*(map(λx.info(x);before(e')))(info(e')))) ∈ bag(B)))@i
13. ∀e':E. (e' ≤loc e  ⇒ (Y(e') = (snd(y*(map(λx.info(x);before(e')))(info(e')))) ∈ bag(C)))@i
14. hdf-until(x;y)*(map(λx.info(x);before(pred(e))))
= hdf-until(if isl(last(λe'.0 <z #(Y(e'))) pred(e))
  then hdf-halt()
  else x*(map(λx.info(x);before(pred(e))))
  fi ;y*(map(λx.info(x);before(pred(e)))))
∈ hdataflow(Info;B)
⊢ (fst(hdf-until(if isl(last(λe'.0 <z #(Y(e'))) pred(e))
then hdf-halt()
else x*(map(λx.info(x);before(pred(e))))
fi ;y*(map(λx.info(x);before(pred(e)))))(info(pred(e)))))
= hdf-until(if isl(if 0 <z #(Y(pred(e))) then inl pred(e) else last(λe'.0 <z #(Y(e'))) pred(e) fi )
  then hdf-halt()
  else fst(x*(map(λx.info(x);before(pred(e))))(info(pred(e))))
  fi ;fst(y*(map(λx.info(x);before(pred(e))))(info(pred(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.  x  :  hdataflow(Info;B)@i
8.  y  :  hdataflow(Info;C)@i
9.  e  :  E@i
10.  \mforall{}e1:E
            ((e1  <  e)
            {}\mRightarrow{}  (\mforall{}e':E.  (e'  \mleq{}loc  e1    {}\mRightarrow{}  (X(e')  =  (snd(x*(map(\mlambda{}x.info(x);before(e')))(info(e')))))))
            {}\mRightarrow{}  (\mforall{}e':E.  (e'  \mleq{}loc  e1    {}\mRightarrow{}  (Y(e')  =  (snd(y*(map(\mlambda{}x.info(x);before(e')))(info(e')))))))
            {}\mRightarrow{}  (hdf-until(x;y)*(map(\mlambda{}x.info(x);before(e1)))
                  =  hdf-until(if  isl(last(\mlambda{}e'.0  <z  \#(Y(e')))  e1)
                      then  hdf-halt()
                      else  x*(map(\mlambda{}x.info(x);before(e1)))
                      fi  ;y*(map(\mlambda{}x.info(x);before(e1))))))
11.  \mforall{}e':E.  (e'  \mleq{}loc  e    {}\mRightarrow{}  (X(e')  =  (snd(x*(map(\mlambda{}x.info(x);before(e')))(info(e'))))))@i
12.  \mforall{}e':E.  (e'  \mleq{}loc  e    {}\mRightarrow{}  (Y(e')  =  (snd(y*(map(\mlambda{}x.info(x);before(e')))(info(e'))))))@i
\mvdash{}  hdf-until(x;y)*(map(\mlambda{}x.info(x);before(e)))
=  hdf-until(if  isl(last(\mlambda{}e'.0  <z  \#(Y(e')))  e)
    then  hdf-halt()
    else  x*(map(\mlambda{}x.info(x);before(e)))
    fi  ;y*(map(\mlambda{}x.info(x);before(e))))


By

---

Latex:
(RecUnfold  `es-before`  0
  THEN  RecUnfold  `es-local-pred`  0
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  (RWW  "map\_append\_sq  iterate-hdf-append"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (InstHyp  [\mkleeneopen{}pred(e)\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
  THEN  (HypSubst  (-1)  0  THENA  AutoSplit))

---

Home Index