---

Step * 1 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
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)
BY
{ ((RWW "map_append_sq iterate-hdf-append" 0 THENA Auto) THEN Reduce 0) }

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)
⊢ (fst(hdf-once(z)*(map(λx.info(x);before(pred(e))))(info(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 fst(z*(map(λx.info(x);before(pred(e))))(info(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
9.  \mneg{}\muparrow{}first(e)
\mvdash{}  hdf-once(z)*(map(\mlambda{}x.info(x);before(pred(e))  @  [pred(e)]))
=  hdf-once(if  isl(if  0  <z  \#(X(pred(e)))  then  inl  pred(e)  else  last(\mlambda{}e'.0  <z  \#(X(e')))  pred(e)  fi  )
    then  hdf-halt()
    else  z*(map(\mlambda{}x.info(x);before(pred(e))  @  [pred(e)]))
    fi  )


By

---

Latex:
((RWW  "map\_append\_sq  iterate-hdf-append"  0  THENA  Auto)  THEN  Reduce  0)

---

Home Index