---

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

.....assertion..... 
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
⊢ ∀u:E List. ∀x:E.
    (u @ [x] ≤ v @ [e]
    ⇒ (¬↑(bag-null(snd(xpr*(map(λx.info(x);u))(info(x)))) ∧b (¬bbag-null(snd(ypr*(map(λx.info(x);u))(info(x))))))))
BY
{ (UnivCD THENA Auto) }

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
⊢ ¬↑(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:
.....assertion..... 
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
\mvdash{}  \mforall{}u:E  List.  \mforall{}x:E.
        (u  @  [x]  \mleq{}  v  @  [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))))))))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index