---

Step * 1 2 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
⊢ ¬↑(bag-null(snd(xpr*(map(λx.info(x);u))(info(x)))) ∧b (¬bbag-null(snd(ypr*(map(λx.info(x);u))(info(x))))))
BY
{ (InstHyp [⌜x⌝] (-6)⋅
   THENA (Auto
          THEN Using [`x',⌜x⌝] (FLemma `iseg_member` [-1])⋅
          THEN Auto
          THEN Try (Complete ((GenListD 0 THEN (OrRight THENA Auto) THEN GenListD 0)))
          THEN (RevHypSubst' (-5) (-1) THENA Auto)
          THEN Fold `es-le-before` (-1)
          THEN GenListD (-1))
   ) }

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. ∀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))))))

---

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
\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:
(InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-6)\mcdot{}
  THENA  (Auto
                THEN  Using  [`x',\mkleeneopen{}x\mkleeneclose{}]  (FLemma  `iseg\_member`  [-1])\mcdot{}
                THEN  Auto
                THEN  Try  (Complete  ((GenListD  0  THEN  (OrRight  THENA  Auto)  THEN  GenListD  0)))
                THEN  (RevHypSubst'  (-5)  (-1)  THENA  Auto)
                THEN  Fold  `es-le-before`  (-1)
                THEN  GenListD  (-1))
  )

---

Home Index