---

Step * 2 of Lemma hdf-state1-single-val_wf


1. A : Type
2. B : Type
3. C : Type
4. f : B ─→ C ─→ C
5. X : hdataflow(A;B)
6. b : C
7. valueall-type(C)
8. hdf-single-valued(X;A;B)
9. X2 : C@i
10. a : A@i
11. y : Unit@i
⊢ hdf-single-valued(inr y ;A;B) ⇒ (let b' ←─ X2 in <<inr ⋅ , b'>, {b'}> ∈ {X:hdataflow(A;B)| hdf-single-valued(X;A;B)} \000C × C × bag(C))
BY
{ (DVar `y'
   THEN ThinVar `y'
   THEN Fold `it` 0
   THEN Fold `hdf-halt` 0
   THEN Auto
   THEN CallByValueReduce 0
   THEN RepeatFor 2 ((MemCD THEN Try (Complete (Auto))))
   THEN At ⌈Type⌉ MemTypeCD⋅
   THEN Auto)⋅ }

---

Latex:



1.  A  :  Type
2.  B  :  Type
3.  C  :  Type
4.  f  :  B  {}\mrightarrow{}  C  {}\mrightarrow{}  C
5.  X  :  hdataflow(A;B)
6.  b  :  C
7.  valueall-type(C)
8.  hdf-single-valued(X;A;B)
9.  X2  :  C@i
10.  a  :  A@i
11.  y  :  Unit@i
\mvdash{}  hdf-single-valued(inr  y  ;A;B)
{}\mRightarrow{}  (let  b'  \mleftarrow{}{}  X2
        in  <<inr  \mcdot{}  ,  b'>,  \{b'\}>  \mmember{}  \{X:hdataflow(A;B)|  hdf-single-valued(X;A;B)\}    \mtimes{}  C  \mtimes{}  bag(C))


By

(DVar  `y'
  THEN  ThinVar  `y'
  THEN  Fold  `it`  0
  THEN  Fold  `hdf-halt`  0
  THEN  Auto
  THEN  CallByValueReduce  0
  THEN  RepeatFor  2  ((MemCD  THEN  Try  (Complete  (Auto))))
  THEN  At  \mkleeneopen{}Type\mkleeneclose{}  MemTypeCD\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index