Nuprl Lemma : hdataflow-ext
∀[A,B:Type]. hdataflow(A;B) ≡ A ─→ (hdataflow(A;B) × bag(B))?
Proof
Definitions occuring in Statement :
hdataflow: hdataflow(A;B),
ext-eq: A ≡ B,
uall: ∀[x:A]. B[x],
unit: Unit,
function: x:A ─→ B[x],
product: x:A × B[x],
union: left + right,
universe: Type,
bag: bag(T)
Lemmas :
corec-ext,
bag_wf,
unit_wf2,
continuous-monotone-union,
continuous-monotone-function,
continuous-monotone-product,
continuous-monotone-id,
continuous-monotone-constant
\mforall{}[A,B:Type]. hdataflow(A;B) \mequiv{} A {}\mrightarrow{} (hdataflow(A;B) \mtimes{} bag(B))?
Date html generated:
2015_07_17-AM-08_04_37
Last ObjectModification:
2015_01_27-PM-00_16_46
Home
Index