---

Step * 1 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. 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)
BY
{ (RecUnfold `es-before` 0 THEN RecUnfold `es-local-pred` 0 THEN Reduce 0 THEN OldAutoSplit) }

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
9. ¬↑first(e)
⊢ hdf-once(z)*(map(λx.info(x);before(pred(e)) @ [pred(e)]))
= hdf-once(if isl(if 0 <z #(X(pred(e))) then inl pred(e) else last(λe'.0 <z #(X(e'))) pred(e) fi )
  then hdf-halt()
  else z*(map(λx.info(x);before(pred(e)) @ [pred(e)]))
  fi )
∈ hdataflow(Info;B)

---

Latex:

---

Latex:

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.  \mforall{}e1:E
          ((e1  <  e)
          {}\mRightarrow{}  (\mforall{}e':E.  (e'  \mleq{}loc  e1    {}\mRightarrow{}  (X(e')  =  (snd(z*(map(\mlambda{}x.info(x);before(e')))(info(e')))))))
          {}\mRightarrow{}  (hdf-once(z)*(map(\mlambda{}x.info(x);before(e1)))
                =  hdf-once(if  isl(last(\mlambda{}e'.0  <z  \#(X(e')))  e1)
                    then  hdf-halt()
                    else  z*(map(\mlambda{}x.info(x);before(e1)))
                    fi  )))
8.  \mforall{}e':E.  (e'  \mleq{}loc  e    {}\mRightarrow{}  (X(e')  =  (snd(z*(map(\mlambda{}x.info(x);before(e')))(info(e'))))))@i
\mvdash{}  hdf-once(z)*(map(\mlambda{}x.info(x);before(e)))
=  hdf-once(if  isl(last(\mlambda{}e'.0  <z  \#(X(e')))  e)  then  hdf-halt()  else  z*(map(\mlambda{}x.info(x);before(e)))  fi  )


By

---

Latex:
(RecUnfold  `es-before`  0  THEN  RecUnfold  `es-local-pred`  0  THEN  Reduce  0  THEN  OldAutoSplit)

---

Home Index