---

Step * 1 2 1 1 2 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. v : E List@i
⊢ ∀xpr:hdataflow(Info;A). ∀ypr:hdataflow(Info;B). ∀zpr:hdataflow(Info;A).
    ((∀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)))))))))
    ⇒ ((snd(xpr*(map(λx.info(x);v))(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> \000Cfi 
          | 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);v))(info(e\000C))))
       ∈ bag(A)))
BY
{ ListInd (-1) }

1
1. Info : Type
2. A : Type
3. B : Type
4. valueall-type(A)
5. es : EO+(Info)@i'
6. e : E@i
⊢ ∀xpr:hdataflow(Info;A). ∀ypr:hdataflow(Info;B). ∀zpr:hdataflow(Info;A).
    ((∀u:E List. ∀x:E.
        (u @ [x] ≤ [] @ [e]
        ⇒ (¬↑(bag-null(snd(xpr*(map(λx.info(x);u))(info(x))))
           ∧b (¬bbag-null(snd(ypr*(map(λx.info(x);u))(info(x)))))))))
    ⇒ ((snd(xpr*(map(λx.info(x);[]))(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> \000Cfi 
          | 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);[]))(info(\000Ce))))
       ∈ bag(A)))

2
1. Info : Type
2. A : Type
3. B : Type
4. valueall-type(A)
5. es : EO+(Info)@i'
6. e : E@i
7. u : E
8. v : E List
9. ∀xpr:hdataflow(Info;A). ∀ypr:hdataflow(Info;B). ∀zpr:hdataflow(Info;A).
     ((∀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)))))))))
     ⇒ ((snd(xpr*(map(λx.info(x);v))(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>\000C 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);v))(info(\000Ce))))
        ∈ bag(A)))
⊢ ∀xpr:hdataflow(Info;A). ∀ypr:hdataflow(Info;B). ∀zpr:hdataflow(Info;A).
    ((∀u@0:E List. ∀x:E.
        (u@0 @ [x] ≤ [u / v] @ [e]
        ⇒ (¬↑(bag-null(snd(xpr*(map(λx.info(x);u@0))(info(x))))
           ∧b (¬bbag-null(snd(ypr*(map(λx.info(x);u@0))(info(x)))))))))
    ⇒ ((snd(xpr*(map(λx.info(x);[u / v]))(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> \000Cfi 
          | 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);[u / v]))(\000Cinfo(e))))
       ∈ bag(A)))

---

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.  v  :  E  List@i
\mvdash{}  \mforall{}xpr:hdataflow(Info;A).  \mforall{}ypr:hdataflow(Info;B).  \mforall{}zpr:hdataflow(Info;A).
        ((\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)))))))))
        {}\mRightarrow{}  ((snd(xpr*(map(\mlambda{}x.info(x);v))(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)  \mwedge{}\msubb{}  (\mneg{}\msubb{}bag-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(\mlambda{}\000Cx.info(x);v))(info(e))))))


By

---

Latex:
ListInd  (-1)

---

Home Index