---

Step * 1 1 1 1 1 3 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. ¬↑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)
15. y1 : ¬(∃e':{E| ((e' <loc pred(e)) ∧ (↑0 <z #(Y(e'))))})@i
16. (last(λe'.0 <z #(Y(e'))) pred(e))
= (inr y1 )
∈ ((∃e':{E| ((e' <loc pred(e))
            ∧ (↑0 <z #(Y(e')))
            ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc pred(e)) ⇒ (¬↑0 <z #(Y(e''))))))})
  ∨ (¬(∃e':{E| ((e' <loc pred(e)) ∧ (↑0 <z #(Y(e'))))})))@i
17. x1 : Info ⟶ (hdataflow(Info;B) × bag(B))@i
18. x*(map(λx.info(x);before(pred(e)))) = (inl x1) ∈ hdataflow(Info;B)@i
19. z1 : hdataflow(Info;B)@i
20. z2 : bag(B)@i
21. (x1 info(pred(e))) = <z1, z2> ∈ (hdataflow(Info;B) × bag(B))@i
22. y2 : 0 = 0 ∈ ℤ
23. y*(map(λx.info(x);before(pred(e)))) = hdf-halt() ∈ hdataflow(Info;C)@i
24. 0 < #(Y(pred(e)))
⊢ z1 = hdf-halt() ∈ hdataflow(Info;B)
BY
{ ((RWO "13" (-1) THEN Auto) THEN (RWO "-2" (-1) THENA Auto) THEN Reduce (-1) THEN Auto) }

---

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.  \mneg{}\muparrow{}first(e)
11.  \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))))))
12.  \mforall{}e':E.  (e'  \mleq{}loc  e    {}\mRightarrow{}  (X(e')  =  (snd(x*(map(\mlambda{}x.info(x);before(e')))(info(e'))))))@i
13.  \mforall{}e':E.  (e'  \mleq{}loc  e    {}\mRightarrow{}  (Y(e')  =  (snd(y*(map(\mlambda{}x.info(x);before(e')))(info(e'))))))@i
14.  hdf-until(x;y)*(map(\mlambda{}x.info(x);before(pred(e))))
=  hdf-until(if  isl(last(\mlambda{}e'.0  <z  \#(Y(e')))  pred(e))
    then  hdf-halt()
    else  x*(map(\mlambda{}x.info(x);before(pred(e))))
    fi  ;y*(map(\mlambda{}x.info(x);before(pred(e)))))
15.  y1  :  \mneg{}(\mexists{}e':\{E|  ((e'  <loc  pred(e))  \mwedge{}  (\muparrow{}0  <z  \#(Y(e'))))\})@i
16.  (last(\mlambda{}e'.0  <z  \#(Y(e')))  pred(e))  =  (inr  y1  )@i
17.  x1  :  Info  {}\mrightarrow{}  (hdataflow(Info;B)  \mtimes{}  bag(B))@i
18.  x*(map(\mlambda{}x.info(x);before(pred(e))))  =  (inl  x1)@i
19.  z1  :  hdataflow(Info;B)@i
20.  z2  :  bag(B)@i
21.  (x1  info(pred(e)))  =  <z1,  z2>@i
22.  y2  :  0  =  0
23.  y*(map(\mlambda{}x.info(x);before(pred(e))))  =  hdf-halt()@i
24.  0  <  \#(Y(pred(e)))
\mvdash{}  z1  =  hdf-halt()


By

---

Latex:
((RWO  "13"  (-1)  THEN  Auto)  THEN  (RWO  "-2"  (-1)  THENA  Auto)  THEN  Reduce  (-1)  THEN  Auto)

---

Home Index