---

Step * 1 2 1 1 2 1 1 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. xpr : hdataflow(Info;A)@i
8. ypr : hdataflow(Info;B)@i
9. zpr : hdataflow(Info;A)@i
10. ∀u:E List. ∀x:E.
      (u @ [x] ≤ [e]
      ⇒ (¬↑(bag-null(snd(xpr*(map(λx.info(x);u))(info(x)))) ∧b (¬bbag-null(snd(ypr*(map(λx.info(x);u))(info(x))))))))@i
⊢ (snd(xpr(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> 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(e))))
∈ bag(A)
BY
{ ((InstHyp [⌜[]⌝;⌜e⌝] (-1)⋅ THENA (Reduce 0 THEN Auto THEN GenListD 0))
   THEN Reduce (-1)
   THEN Thin (-2)
   THEN RecUnfold `mk-hdf` 0
   THEN Reduce 0
   THEN (RWO "hdf-ap-run" 0 THENA Auto)
   THEN Reduce 0
   THEN HDataflowHDAll
   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. x : Info ⟶ (hdataflow(Info;A) × bag(A))@i
8. z1 : hdataflow(Info;A)@i
9. z2 : bag(A)@i
10. (x info(e)) = <z1, z2> ∈ (hdataflow(Info;A) × bag(A))@i
11. x1 : Info ⟶ (hdataflow(Info;B) × bag(B))@i
12. ¬↑(bag-null(snd(inl x(info(e)))) ∧b (¬bbag-null(snd(inl x1(info(e))))))@i
13. z3 : hdataflow(Info;B)@i
14. z4 : bag(B)@i
15. ¬(z4 = {} ∈ bag(B))
16. (x1 info(e)) = <z3, z4> ∈ (hdataflow(Info;B) × bag(B))@i
17. x2 : Info ⟶ (hdataflow(Info;A) × bag(A))@i
18. z5 : hdataflow(Info;A)@i
19. z6 : bag(A)@i
20. (x2 info(e)) = <z5, z6> ∈ (hdataflow(Info;A) × bag(A))@i
21. z2 = {} ∈ bag(A)
⊢ z2 = z6 ∈ bag(A)

2
1. Info : Type
2. A : Type
3. B : Type
4. valueall-type(A)
5. es : EO+(Info)@i'
6. e : E@i
7. y : 0 = 0 ∈ ℤ
8. x : Info ⟶ (hdataflow(Info;B) × bag(B))@i
9. ¬↑¬bbag-null(snd(inl x(info(e))))@i
10. z1 : hdataflow(Info;B)@i
11. z2 : bag(B)@i
12. ¬(z2 = {} ∈ bag(B))
13. (x info(e)) = <z1, z2> ∈ (hdataflow(Info;B) × bag(B))@i
14. x1 : Info ⟶ (hdataflow(Info;A) × bag(A))@i
15. z3 : hdataflow(Info;A)@i
16. z4 : bag(A)@i
17. (x1 info(e)) = <z3, z4> ∈ (hdataflow(Info;A) × bag(A))@i
⊢ {} = z4 ∈ 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.  xpr  :  hdataflow(Info;A)@i
8.  ypr  :  hdataflow(Info;B)@i
9.  zpr  :  hdataflow(Info;A)@i
10.  \mforall{}u:E  List.  \mforall{}x:E.
            (u  @  [x]  \mleq{}  [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))))))))@i
\mvdash{}  (snd(xpr(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>)(info(e))))


By

---

Latex:
((InstHyp  [\mkleeneopen{}[]\mkleeneclose{};\mkleeneopen{}e\mkleeneclose{}]  (-1)\mcdot{}  THENA  (Reduce  0  THEN  Auto  THEN  GenListD  0))
  THEN  Reduce  (-1)
  THEN  Thin  (-2)
  THEN  RecUnfold  `mk-hdf`  0
  THEN  Reduce  0
  THEN  (RWO  "hdf-ap-run"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  HDataflowHDAll
  THEN  Repeat  (AutoSplit))

---

Home Index