---

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


1. Info : Type
2. A : Type
3. B : Type
4. xpr : Id ─→ hdataflow(Info;A)
5. ypr : Id ─→ hdataflow(Info;B)
6. zpr : Id ─→ hdataflow(Info;A)
7. valueall-type(A)
8. es : EO+(Info)@i'
9. e : E@i
10. v : hdataflow(Info;A)@i
11. (xpr loc(e)) = v ∈ hdataflow(Info;A)@i
12. v1 : hdataflow(Info;B)@i
13. (ypr loc(e)) = v1 ∈ hdataflow(Info;B)@i
14. v2 : hdataflow(Info;A)@i
15. (zpr loc(e)) = v2 ∈ hdataflow(Info;A)@i
16. x : E@i
17. x ≤loc e @i
18. ↑(bag-null(snd(v*(map(λx.info(x);before(x)))(info(x))))
∧b (¬bbag-null(snd(v1*(map(λx.info(x);before(x)))(info(x))))))
19. ∀e'':E
      ((e'' <loc x)
      ⇒ (¬↑(bag-null(snd(xpr loc(e'')*(map(λx.info(x);before(e'')))(info(e''))))
         ∧b (¬bbag-null(snd(ypr loc(e'')*(map(λx.info(x);before(e'')))(info(e''))))))))@i
⊢ (snd(v2*(map(λx@0.info(x@0);before(e)))(info(e))))
= (snd(hdf-sequence(v;v1;v2)*(map(λx.info(x);before(e)))(info(e))))
∈ bag(A)
BY
{ ((Assert ∀e'':E
             ((e'' <loc x)
             ⇒ (¬↑(bag-null(snd(v*(map(λx.info(x);before(e'')))(info(e''))))
                ∧b (¬bbag-null(snd(v1*(map(λx.info(x);before(e'')))(info(e'')))))))) BY
          (RepeatFor 2 (ParallelLast) THEN NthHypEq (-1) THEN EqCD THEN Auto))
   THEN ThinVar `xpr'
   THEN ThinVar `ypr'
   THEN ThinVar `zpr'
   THEN (RenameVar `xpr' (-7) THEN RenameVar `ypr' (-6) THEN RenameVar `zpr' (-5))
   THEN RepUR ``hdf-sequence`` 0) }

1
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. x : E@i
11. x ≤loc e @i
12. ↑(bag-null(snd(xpr*(map(λx.info(x);before(x)))(info(x))))
∧b (¬bbag-null(snd(ypr*(map(λx.info(x);before(x)))(info(x))))))
13. ∀e'':E
      ((e'' <loc x)
      ⇒ (¬↑(bag-null(snd(xpr*(map(λx.info(x);before(e'')))(info(e''))))
         ∧b (¬bbag-null(snd(ypr*(map(λx.info(x);before(e'')))(info(e''))))))))
⊢ (snd(zpr*(map(λx@0.info(x@0);before(e)))(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>)*(map(λx.info(x);before(e)))(info(\000Ce))))
∈ bag(A)

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  xpr  :  Id  {}\mrightarrow{}  hdataflow(Info;A)
5.  ypr  :  Id  {}\mrightarrow{}  hdataflow(Info;B)
6.  zpr  :  Id  {}\mrightarrow{}  hdataflow(Info;A)
7.  valueall-type(A)
8.  es  :  EO+(Info)@i'
9.  e  :  E@i
10.  v  :  hdataflow(Info;A)@i
11.  (xpr  loc(e))  =  v@i
12.  v1  :  hdataflow(Info;B)@i
13.  (ypr  loc(e))  =  v1@i
14.  v2  :  hdataflow(Info;A)@i
15.  (zpr  loc(e))  =  v2@i
16.  x  :  E@i
17.  x  \mleq{}loc  e  @i
18.  \muparrow{}(bag-null(snd(v*(map(\mlambda{}x.info(x);before(x)))(info(x))))
\mwedge{}\msubb{}  (\mneg{}\msubb{}bag-null(snd(v1*(map(\mlambda{}x.info(x);before(x)))(info(x))))))
19.  \mforall{}e'':E
            ((e''  <loc  x)
            {}\mRightarrow{}  (\mneg{}\muparrow{}(bag-null(snd(xpr  loc(e'')*(map(\mlambda{}x.info(x);before(e'')))(info(e''))))
                  \mwedge{}\msubb{}  (\mneg{}\msubb{}bag-null(snd(ypr  loc(e'')*(map(\mlambda{}x.info(x);before(e'')))(info(e''))))))))@i
\mvdash{}  (snd(v2*(map(\mlambda{}x@0.info(x@0);before(e)))(info(e))))
=  (snd(hdf-sequence(v;v1;v2)*(map(\mlambda{}x.info(x);before(e)))(info(e))))


By

---

Latex:
((Assert  \mforall{}e'':E
                      ((e''  <loc  x)
                      {}\mRightarrow{}  (\mneg{}\muparrow{}(bag-null(snd(v*(map(\mlambda{}x.info(x);before(e'')))(info(e''))))
                            \mwedge{}\msubb{}  (\mneg{}\msubb{}bag-null(snd(v1*(map(\mlambda{}x.info(x);before(e'')))(info(e''))))))))  BY
                (RepeatFor  2  (ParallelLast)  THEN  NthHypEq  (-1)  THEN  EqCD  THEN  Auto))
  THEN  ThinVar  `xpr'
  THEN  ThinVar  `ypr'
  THEN  ThinVar  `zpr'
  THEN  (RenameVar  `xpr'  (-7)  THEN  RenameVar  `ypr'  (-6)  THEN  RenameVar  `zpr'  (-5))
  THEN  RepUR  ``hdf-sequence``  0)

---

Home Index