---

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


1. Info : Type
2. A : Type
3. B : Type
4. valueall-type(A)
5. es : EO+(Info)@i'
6. e : E@i
7. u : E
8. v : E List
9. ∀xpr:hdataflow(Info;A). ∀ypr:hdataflow(Info;B). ∀zpr:hdataflow(Info;A).
     ((∀u:E List. ∀x:E.
         (u @ [x] ≤ v @ [e]
         ⇒ (¬↑(bag-null(snd(xpr*(map(λx.info(x);u))(info(x))))
            ∧b (¬bbag-null(snd(ypr*(map(λx.info(x);u))(info(x)))))))))
     ⇒ ((snd(xpr*(map(λx.info(x);v))(info(e))))
        = (snd(mk-hdf(S,a.case S
           of inl(XY) =>
           let X,Y = XY 
           in let X',bx = X(a) 
              in let Y',by = Y(a) 
                 in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx>\000C fi 
           | inr(Z) =>
           let Z',b = Z(a) 
           in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr, ypr>)*(map(λx.info(x);v))(info(\000Ce))))
        ∈ bag(A)))
10. xpr : hdataflow(Info;A)@i
11. ypr : hdataflow(Info;B)@i
12. zpr : hdataflow(Info;A)@i
13. ∀u@0:E List. ∀x:E.
      (u@0 @ [x] ≤ [u / (v @ [e])]
      ⇒ (¬↑(bag-null(snd(xpr*(map(λx.info(x);u@0))(info(x))))
         ∧b (¬bbag-null(snd(ypr*(map(λx.info(x);u@0))(info(x))))))))@i
⊢ (snd(fst(xpr(info(u)))*(map(λx.info(x);v))(info(e))))
= (snd(fst(mk-hdf(S,a.case S
   of inl(XY) =>
   let X,Y = XY 
   in let X',bx = X(a) 
      in let Y',by = Y(a) 
         in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx> fi 
   | inr(Z) =>
   let Z',b = Z(a) 
   in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr, ypr>)(info(u)))*(map(λx.info(x);v))(inf\000Co(e))))
∈ bag(A)
BY
{ (RecUnfold `mk-hdf` 0
   THEN Reduce 0
   THEN (RWO "hdf-ap-run" 0 THENA Auto)
   THEN Reduce 0
   THEN skip{(HDataflowHDVar' `xpr'
              THEN HDataflowHDVar' `ypr'
              THEN skip{((UnivCD
                          THENA (Try (Fold `hdf-run` 0)
                                 THEN Auto
                                 THEN Try ((RWO "iterate-hdf-halt" 0 THEN Reduce 0 THEN Auto)))
                          )
                         THEN Repeat (AutoSplit)
                         )})}) }

1
1. Info : Type
2. A : Type
3. B : Type
4. valueall-type(A)
5. es : EO+(Info)@i'
6. e : E@i
7. u : E
8. v : E List
9. ∀xpr:hdataflow(Info;A). ∀ypr:hdataflow(Info;B). ∀zpr:hdataflow(Info;A).
     ((∀u:E List. ∀x:E.
         (u @ [x] ≤ v @ [e]
         ⇒ (¬↑(bag-null(snd(xpr*(map(λx.info(x);u))(info(x))))
            ∧b (¬bbag-null(snd(ypr*(map(λx.info(x);u))(info(x)))))))))
     ⇒ ((snd(xpr*(map(λx.info(x);v))(info(e))))
        = (snd(mk-hdf(S,a.case S
           of inl(XY) =>
           let X,Y = XY 
           in let X',bx = X(a) 
              in let Y',by = Y(a) 
                 in if bag-null(bx) ∧b (¬bbag-null(by)) then let Z',bz = zpr(a) in <inr Z' , bz> else <inl <X', Y'>, bx>\000C fi 
           | inr(Z) =>
           let Z',b = Z(a) 
           in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);inl <xpr, ypr>)*(map(λx.info(x);v))(info(\000Ce))))
        ∈ bag(A)))
10. xpr : hdataflow(Info;A)@i
11. ypr : hdataflow(Info;B)@i
12. zpr : hdataflow(Info;A)@i
13. ∀u@0:E List. ∀x:E.
      (u@0 @ [x] ≤ [u / (v @ [e])]
      ⇒ (¬↑(bag-null(snd(xpr*(map(λx.info(x);u@0))(info(x))))
         ∧b (¬bbag-null(snd(ypr*(map(λx.info(x);u@0))(info(x))))))))@i
⊢ (snd(fst(xpr(info(u)))*(map(λx.info(x);v))(info(e))))
= (snd(fst(let s1,b = let X',bx = xpr(info(u)) 
                      in let Y',by = ypr(info(u)) 
                         in if bag-null(bx) ∧b (¬bbag-null(by))
                            then let Z',bz = zpr(info(u)) 
                                 in <inr Z' , bz>
                            else <inl <X', Y'>, bx>
                            fi  
           in <mk-hdf(S,a.case S
                of inl(XY) =>
                let X,Y = XY 
                in let X',bx = X(a) 
                   in let Y',by = Y(a) 
                      in if bag-null(bx) ∧b (¬bbag-null(by))
                         then let Z',bz = zpr(a) 
                              in <inr Z' , bz>
                         else <inl <X', Y'>, bx>
                         fi 
                | inr(Z) =>
                let Z',b = Z(a) 
                in <inr Z' , b>;S.case S of inl(XY) => ff | inr(Z) => hdf-halted(Z);s1)
              , b
              >)*(map(λx.info(x);v))(info(e))))
∈ bag(A)

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  valueall-type(A)
5.  es  :  EO+(Info)@i'
6.  e  :  E@i
7.  u  :  E
8.  v  :  E  List
9.  \mforall{}xpr:hdataflow(Info;A).  \mforall{}ypr:hdataflow(Info;B).  \mforall{}zpr:hdataflow(Info;A).
          ((\mforall{}u:E  List.  \mforall{}x:E.
                  (u  @  [x]  \mleq{}  v  @  [e]
                  {}\mRightarrow{}  (\mneg{}\muparrow{}(bag-null(snd(xpr*(map(\mlambda{}x.info(x);u))(info(x))))
                        \mwedge{}\msubb{}  (\mneg{}\msubb{}bag-null(snd(ypr*(map(\mlambda{}x.info(x);u))(info(x)))))))))
          {}\mRightarrow{}  ((snd(xpr*(map(\mlambda{}x.info(x);v))(info(e))))
                =  (snd(mk-hdf(S,a.case  S
                      of  inl(XY)  =>
                      let  X,Y  =  XY 
                      in  let  X',bx  =  X(a) 
                            in  let  Y',by  =  Y(a) 
                                  in  if  bag-null(bx)  \mwedge{}\msubb{}  (\mneg{}\msubb{}bag-null(by))
                                        then  let  Z',bz  =  zpr(a) 
                                                  in  <inr  Z'  ,  bz>
                                        else  <inl  <X',  Y'>,  bx>
                                        fi 
                      |  inr(Z)  =>
                      let  Z',b  =  Z(a) 
                      in  <inr  Z'  ,  b>S.case  S  of  inl(XY)  =>  ff  |  inr(Z)  =>  hdf-halted(Z);inl  <xpr,  ypr>)*(map(\000C\mlambda{}x.info(x);v))(info(e))))))
10.  xpr  :  hdataflow(Info;A)@i
11.  ypr  :  hdataflow(Info;B)@i
12.  zpr  :  hdataflow(Info;A)@i
13.  \mforall{}u@0:E  List.  \mforall{}x:E.
            (u@0  @  [x]  \mleq{}  [u  /  (v  @  [e])]
            {}\mRightarrow{}  (\mneg{}\muparrow{}(bag-null(snd(xpr*(map(\mlambda{}x.info(x);u@0))(info(x))))
                  \mwedge{}\msubb{}  (\mneg{}\msubb{}bag-null(snd(ypr*(map(\mlambda{}x.info(x);u@0))(info(x))))))))@i
\mvdash{}  (snd(fst(xpr(info(u)))*(map(\mlambda{}x.info(x);v))(info(e))))
=  (snd(fst(mk-hdf(S,a.case  S
      of  inl(XY)  =>
      let  X,Y  =  XY 
      in  let  X',bx  =  X(a) 
            in  let  Y',by  =  Y(a) 
                  in  if  bag-null(bx)  \mwedge{}\msubb{}  (\mneg{}\msubb{}bag-null(by))
                        then  let  Z',bz  =  zpr(a) 
                                  in  <inr  Z'  ,  bz>
                        else  <inl  <X',  Y'>,  bx>
                        fi 
      |  inr(Z)  =>
      let  Z',b  =  Z(a) 
      in  <inr  Z'  ,  b>S.case  S  of  inl(XY)  =>  ff  |  inr(Z)  =>  hdf-halted(Z);inl  <xpr,  ypr>)(info(u)))*(ma\000Cp(\mlambda{}x.info(x);v))(info(e))))


By

---

Latex:
(RecUnfold  `mk-hdf`  0
  THEN  Reduce  0
  THEN  (RWO  "hdf-ap-run"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  skip\{(HDataflowHDVar'  `xpr'
                        THEN  HDataflowHDVar'  `ypr'
                        THEN  skip\{((UnivCD
                                                THENA  (Try  (Fold  `hdf-run`  0)
                                                              THEN  Auto
                                                              THEN  Try  ((RWO  "iterate-hdf-halt"  0  THEN  Reduce  0  THEN  Auto)))
                                                )
                                              THEN  Repeat  (AutoSplit)
                                              )\})\})

---

Home Index