---

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


1. A : Type
2. B : Type
3. X : hdataflow(A;B ─→ B)
4. b : B
5. valueall-type(B)
6. hdf-single-valued(X;A;B ─→ B)
7. X2 : B@i
8. a : A@i
9. y : Unit@i
⊢ hdf-single-valued(inr y ;A;B ─→ B) ⇒ (let b' ←─ X2 in <<inr ⋅ , b'>, {b'}> ∈ {X:hdataflow(A;B ─→ B)| hdf-single-value\000Cd(X;A;B ─→ B)}  × B × bag(B))
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.  X  :  hdataflow(A;B  {}\mrightarrow{}  B)
4.  b  :  B
5.  valueall-type(B)
6.  hdf-single-valued(X;A;B  {}\mrightarrow{}  B)
7.  X2  :  B@i
8.  a  :  A@i
9.  y  :  Unit@i
\mvdash{}  hdf-single-valued(inr  y  ;A;B  {}\mrightarrow{}  B)
{}\mRightarrow{}  (let  b'  \mleftarrow{}{}  X2
        in  <<inr  \mcdot{}  ,  b'>,  \{b'\}>  \mmember{}  \{X:hdataflow(A;B  {}\mrightarrow{}  B)|  hdf-single-valued(X;A;B  {}\mrightarrow{}  B)\}    \mtimes{}  B  \mtimes{}  bag(B))


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)

---

Home Index