---

Step * 1 2 1 1 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. ∀e'':E
      (e'' ≤loc e 
      ⇒ (¬↑(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''))))))))
11. v : E List@i
12. before(e) = v ∈ (E List)@i
13. u : E List@i
14. x : E@i
15. u @ [x] ≤ v @ [e]@i
16. ¬↑(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))))))
⊢ ¬↑(bag-null(snd(xpr*(map(λx.info(x);u))(info(x)))) ∧b (¬bbag-null(snd(ypr*(map(λx.info(x);u))(info(x))))))
BY
{ (Assert ⌜u = before(x) ∈ (E List)⌝⋅
   THEN Auto
   THEN (RevHypSubst' (-5) (-2) THENA Auto)
   THEN Fold `es-le-before` (-2)
   THEN FLemma `iseg-es-le-before-is-before` [-2]
   THEN Auto) }

---

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{}e'':E
            (e''  \mleq{}loc  e 
            {}\mRightarrow{}  (\mneg{}\muparrow{}(bag-null(snd(xpr*(map(\mlambda{}x.info(x);before(e'')))(info(e''))))
                  \mwedge{}\msubb{}  (\mneg{}\msubb{}bag-null(snd(ypr*(map(\mlambda{}x.info(x);before(e'')))(info(e''))))))))
11.  v  :  E  List@i
12.  before(e)  =  v@i
13.  u  :  E  List@i
14.  x  :  E@i
15.  u  @  [x]  \mleq{}  v  @  [e]@i
16.  \mneg{}\muparrow{}(bag-null(snd(xpr*(map(\mlambda{}x.info(x);before(x)))(info(x))))
\mwedge{}\msubb{}  (\mneg{}\msubb{}bag-null(snd(ypr*(map(\mlambda{}x.info(x);before(x)))(info(x))))))
\mvdash{}  \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))))))


By

---

Latex:
(Assert  \mkleeneopen{}u  =  before(x)\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (RevHypSubst'  (-5)  (-2)  THENA  Auto)
  THEN  Fold  `es-le-before`  (-2)
  THEN  FLemma  `iseg-es-le-before-is-before`  [-2]
  THEN  Auto)

---

Home Index