---

Step * 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(xpr loc(x)*(map(λx.info(x);before(x)))(info(x))))
∧b (¬bbag-null(snd(ypr loc(x)*(map(λx.info(x);before(x)))(info(x))))))@i
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
{ ((Subst' loc(x) ~ loc(e) -2 THENA Auto) THEN (RWO "11 13" (-2) THENA Auto)) }

1
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)

---

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(xpr  loc(x)*(map(\mlambda{}x.info(x);before(x)))(info(x))))
\mwedge{}\msubb{}  (\mneg{}\msubb{}bag-null(snd(ypr  loc(x)*(map(\mlambda{}x.info(x);before(x)))(info(x))))))@i
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:
((Subst'  loc(x)  \msim{}  loc(e)  -2  THENA  Auto)  THEN  (RWO  "11  13"  (-2)  THENA  Auto))

---

Home Index