---

Step * 1 2 1 1 1 1 of Lemma bind-class-program_wf

.....assertion..... 
1. Info : Type
2. A : Type
3. B : Type
4. valueall-type(B)
5. es : EO+(Info)@i'
6. e : E@i
7. X : hdataflow(Info;A)@i
8. Y : A ⟶ hdataflow(Info;B)@i
⊢ ∀e:E
    (simple-hdf-bind(X;λx.(Y x))*(map(λx.info(x);before(e)))
    = mk-hdf(p,a.simple-bind-nxt(λx.(Y x); p; a);p.let X,ys = p 
                                                   in ff;<X*(map(λx.info(x);before(e)))
                                                         , ⋃e'∈before(e).
                                                           bag-map(λa.Y a*(map(λx.info(x);filter(λa.e' ≤loc a;
                                                                                                 before(e))));
                                                           snd(X*(map(λx.info(x);before(e')))(info(e'))))
                                                         >)
    ∈ hdataflow(Info;B))
BY
{ (Thin (-3)
   THEN CausalInd'
   THEN Subst ⌜before(e) ~ if first(e) then [] else before(pred(e)) @ [pred(e)] fi ⌝ 0⋅
   THEN Try ((RW (AddrC [1] RecUnfoldTopAbC) 0 THEN Trivial))
   THEN OldAutoSplit
   THEN Try ((Fold `empty-bag` 0 THEN Reduce 0 THEN Fold `simple-hdf-bind` 0 THEN Auto)⋅)
   THEN (RWW "map_append_sq iterate-hdf-append" 0 THENA MaAuto)
   THEN (RWO "-2" 0
         THENA (Try (Complete (Auto))
                THEN Try ((RepeatFor 2 ((MemCD THEN Try (Complete (Auto)))) THEN GenConclAtAddr [2;1] THEN Auto))
                THEN MaAuto)
         )
   THEN Reduce 0
   THEN GenConclAtAddr [2;1;1;3;1]) }

1
1. Info : Type
2. A : Type
3. B : Type
4. valueall-type(B)
5. es : EO+(Info)@i'
6. X : hdataflow(Info;A)@i
7. Y : A ⟶ hdataflow(Info;B)@i
8. e : E@i
9. ∀e1:E
     ((e1 < e)
     ⇒ (simple-hdf-bind(X;λx.(Y x))*(map(λx.info(x);before(e1)))
        = mk-hdf(p,a.simple-bind-nxt(λx.(Y x); p; a);p.let X,ys = p 
                                                       in ff;<X*(map(λx.info(x);before(e1)))
                                                             , ⋃e'∈before(e1).
                                                               bag-map(λa.Y a*(map(λx.info(x);filter(λa.e' ≤loc a;
                                                                                                     before(e1))));
                                                               snd(X*(map(λx.info(x);before(e')))(info(e'))))
                                                             >)
        ∈ hdataflow(Info;B)))
10. ¬↑first(e)
11. v : hdataflow(Info;A)@i
12. X*(map(λx.info(x);before(pred(e)))) = v ∈ hdataflow(Info;A)@i
⊢ (fst(mk-hdf(p,a.simple-bind-nxt(λx.(Y x); p; a);p.let X,ys = p 
                                                    in ff;<v
                                                          , ⋃e'∈before(pred(e)).
                                                            bag-map(λa.Y a*(map(λx.info(x);filter(λa.e' ≤loc a;
                                                                                                  before(pred(e)))));
                                                            snd(X*(map(λx.info(x);before(e')))(info(e'))))
                                                          >)(info(pred(e)))))
= mk-hdf(p,a.simple-bind-nxt(λx.(Y x); p; a
                             );p.let X,ys = p 
                                 in ff;<fst(v(info(pred(e))))
                                       , ⋃e'∈before(pred(e)) @ [pred(e)].
                                         bag-map(λa.Y a*(map(λx.info(x);filter(λa.e' ≤loc a;
                                                                               before(pred(e)) @ [pred(e)])));
                                         snd(X*(map(λx.info(x);before(e')))(info(e'))))
                                       >)
∈ hdataflow(Info;B)

---

Latex:

---

Latex:
.....assertion..... 
1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  valueall-type(B)
5.  es  :  EO+(Info)@i'
6.  e  :  E@i
7.  X  :  hdataflow(Info;A)@i
8.  Y  :  A  {}\mrightarrow{}  hdataflow(Info;B)@i
\mvdash{}  \mforall{}e:E
        (simple-hdf-bind(X;\mlambda{}x.(Y  x))*(map(\mlambda{}x.info(x);before(e)))
        =  mk-hdf(p,a.simple-bind-nxt(\mlambda{}x.(Y  x);  p;  a);p.let  X,ys  =  p 
                                                                                                      in  ff;<X*(map(\mlambda{}x.info(x);before(e)))
                                                                                                                  ,  \mcup{}e'\mmember{}before(e).
                                                                                                                      bag-map(\mlambda{}a.Y  a*(map(\mlambda{}x.info(x);
                                                                                                                                                              filter(\mlambda{}a.e'  \mleq{}loc  a;
                                                                                                                                                                            before(e))));
                                                                                                                      snd(X*(map(\mlambda{}x.info(x);
                                                                                                                                            before(e')))(info(e'))))
                                                                                                                  >))


By

---

Latex:
(Thin  (-3)
  THEN  CausalInd'
  THEN  Subst  \mkleeneopen{}before(e)  \msim{}  if  first(e)  then  []  else  before(pred(e))  @  [pred(e)]  fi  \mkleeneclose{}  0\mcdot{}
  THEN  Try  ((RW  (AddrC  [1]  RecUnfoldTopAbC)  0  THEN  Trivial))
  THEN  OldAutoSplit
  THEN  Try  ((Fold  `empty-bag`  0  THEN  Reduce  0  THEN  Fold  `simple-hdf-bind`  0  THEN  Auto)\mcdot{})
  THEN  (RWW  "map\_append\_sq  iterate-hdf-append"  0  THENA  MaAuto)
  THEN  (RWO  "-2"  0
              THENA  (Try  (Complete  (Auto))
                            THEN  Try  ((RepeatFor  2  ((MemCD  THEN  Try  (Complete  (Auto))))
                                                  THEN  GenConclAtAddr  [2;1]
                                                  THEN  Auto))
                            THEN  MaAuto)
              )
  THEN  Reduce  0
  THEN  GenConclAtAddr  [2;1;1;3;1])

---

Home Index