---

Step * 1 1 1 1 1 2 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. x : E@i
11. x ≤loc e @i
12. ↑(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))))))
13. ∀e'':E
      ((e'' <loc x)
      ⇒ (¬↑(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''))))))))
14. v : E List@i
15. before(e) = v ∈ (E List)@i
16. before(e) = (before(x) @ v) ∈ (E List)
17. v ∈ E List
18. 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> 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);before(x)))
= 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> 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*(map(λx.info(x);before(x)))
                                                                           , ypr*(map(λx.info(x);before(x)))
                                                                           >)
∈ hdataflow(Info;A)
⊢ (snd(zpr*(map(λx@0.info(x@0);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> 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);before(x)))*(map(\000Cλx.info(x);v))(info(e))))
∈ bag(A)
BY
{ ((RWO "-1" 0 THENA Auto)
   THEN Thin (-1)
   THEN Thin (-5)
   THEN GenConclAtAddr [3;1;1;1;3;1;1]
   THEN GenConclAtAddr [3;1;1;1;3;1;2]
   THEN (HypSubst' (-3) (-9) THENA Auto)
   THEN (HypSubst' (-2) (-1) THENA Auto)
   THEN (Assert ⌜v = before(e) ∈ (E List)⌝⋅ THENA (RWO "-8<" 0 THEN Auto))
   THEN (RWO "es-closed-open-interval-eq-before<" (-1) THENA Auto)
   THEN D (-11)) }

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. x : E@i
11. (x <loc e)@i
12. v : E List@i
13. before(e) = v ∈ (E List)@i
14. before(e) = (before(x) @ v) ∈ (E List)
15. v ∈ E List
16. v1 : hdataflow(Info;A)@i
17. xpr*(map(λx.info(x);before(x))) = v1 ∈ hdataflow(Info;A)@i
18. v2 : hdataflow(Info;B)@i
19. ypr*(map(λx.info(x);before(x))) = v2 ∈ hdataflow(Info;B)@i
20. ↑(bag-null(snd(v1(info(x)))) ∧b (¬bbag-null(snd(v2(info(x))))))
21. v = [x;e) ∈ (E List)
⊢ (snd(zpr*(map(λx@0.info(x@0);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> 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 <v1, v2>)*(map(λx.info(x);v))(info(e))))
∈ 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. xpr : hdataflow(Info;A)@i
8. ypr : hdataflow(Info;B)@i
9. zpr : hdataflow(Info;A)@i
10. x : E@i
11. x = e ∈ E@i
12. v : E List@i
13. before(e) = v ∈ (E List)@i
14. before(e) = (before(x) @ v) ∈ (E List)
15. v ∈ E List
16. v1 : hdataflow(Info;A)@i
17. xpr*(map(λx.info(x);before(x))) = v1 ∈ hdataflow(Info;A)@i
18. v2 : hdataflow(Info;B)@i
19. ypr*(map(λx.info(x);before(x))) = v2 ∈ hdataflow(Info;B)@i
20. ↑(bag-null(snd(v1(info(x)))) ∧b (¬bbag-null(snd(v2(info(x))))))
21. v = [x;e) ∈ (E List)
⊢ (snd(zpr*(map(λx@0.info(x@0);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> 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 <v1, v2>)*(map(λx.info(x);v))(info(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.  xpr  :  hdataflow(Info;A)@i
8.  ypr  :  hdataflow(Info;B)@i
9.  zpr  :  hdataflow(Info;A)@i
10.  x  :  E@i
11.  x  \mleq{}loc  e  @i
12.  \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))))))
13.  \mforall{}e'':E
            ((e''  <loc  x)
            {}\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''))))))))
14.  v  :  E  List@i
15.  before(e)  =  v@i
16.  before(e)  =  (before(x)  @  v)
17.  v  \mmember{}  E  List
18.  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{}x.info(x)\000C;before(x)))
=  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*(map(\mlambda{}x.info(x);before(x))),  ypr*(map(\mlambda{}x.info(x);before(x)))>)
\mvdash{}  (snd(zpr*(map(\mlambda{}x@0.info(x@0);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{}x.info(\000Cx);before(x)))*(map(\mlambda{}x.info(x);v))(info(e))))


By

---

Latex:
((RWO  "-1"  0  THENA  Auto)
  THEN  Thin  (-1)
  THEN  Thin  (-5)
  THEN  GenConclAtAddr  [3;1;1;1;3;1;1]
  THEN  GenConclAtAddr  [3;1;1;1;3;1;2]
  THEN  (HypSubst'  (-3)  (-9)  THENA  Auto)
  THEN  (HypSubst'  (-2)  (-1)  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}v  =  before(e)\mkleeneclose{}\mcdot{}  THENA  (RWO  "-8<"  0  THEN  Auto))
  THEN  (RWO  "es-closed-open-interval-eq-before<"  (-1)  THENA  Auto)
  THEN  D  (-11))

---

Home Index