---

Step * 2 of Lemma hdataflow-valueall-type


1. A : Type
2. B : Type
3. ↓A
⊢ ∃n:ℕ. valueall-type(λ2P.A ─→ (P × bag(B))?^n Top)
BY
{ ((RepUR ``so_lambda`` 0 THEN With ⌈1⌉ (D 0)⋅ THEN Auto) THEN Reduce 0) }

1
1. A : Type
2. B : Type
3. ↓A
⊢ valueall-type(A ─→ (Top × bag(B))?)

2
1. A : Type
2. B : Type
3. A
4. n : ℕ
⊢ λP.(A ─→ (P × bag(B))?)^n Top ∈ Type

---

Latex:



1.  A  :  Type
2.  B  :  Type
3.  \mdownarrow{}A
\mvdash{}  \mexists{}n:\mBbbN{}.  valueall-type(\mlambda{}\msubtwo{}P.A  {}\mrightarrow{}  (P  \mtimes{}  bag(B))?\^{}n  Top)


By

((RepUR  ``so\_lambda``  0  THEN  With  \mkleeneopen{}1\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)  THEN  Reduce  0)

---

Home Index