Nuprl Lemma : hdf-union-ap

[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:hdataflow(A;C)]. ∀[a:A].
  (X Y(a)
     = <fst(X(a)) fst(Y(a)), bag-map(λx.(inl x);snd(X(a))) bag-map(λx.(inr );snd(Y(a)))>
     ∈ (hdataflow(A;B C) × bag(B C))) supposing 
     (valueall-type(B) and 


Definitions occuring in Statement :  hdf-union: Y hdf-ap: X(a) hdataflow: hdataflow(A;B) valueall-type: valueall-type(T) uimplies: supposing a uall: [x:A]. B[x] pi1: fst(t) pi2: snd(t) lambda: λx.A[x] pair: <a, b> product: x:A × B[x] inr: inr  inl: inl x union: left right universe: Type equal: t ∈ T bag-append: as bs bag-map: bag-map(f;bs) bag: bag(T)
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a hdf-ap: X(a) hdf-union: Y mk-hdf: mk-hdf(s,m.G[s; m];st.H[st];s0) all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q band: p ∧b q ifthenelse: if then else fi  hdf-halt: hdf-halt() top: Top pi1: fst(t) pi2: snd(t) exposed-bfalse: exposed-bfalse callbyvalueall: callbyvalueall evalall: evalall(t) bag-map: bag-map(f;bs) map: map(f;as) list_ind: list_ind empty-bag: {} nil: [] bfalse: ff exists: x:A. B[x] prop: or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b false: False subtype_rel: A ⊆B ext-eq: A ≡ B not: ¬A true: True has-value: (a)↓ has-valueall: has-valueall(a) so_lambda: λ2x.t[x] so_apply: x[s] so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] hdf-halted: hdf-halted(P) isr: isr(x)

\mforall{}[A,B,C:Type].  \mforall{}[X:hdataflow(A;B)].  \mforall{}[Y:hdataflow(A;C)].  \mforall{}[a:A].
    (X  +  Y(a)
          =  <fst(X(a))  +  fst(Y(a))
              ,  bag-map(\mlambda{}x.(inl  x);snd(X(a)))  +  bag-map(\mlambda{}x.(inr  x  );snd(Y(a)))
              >)  supposing 
          (valueall-type(B)  and 

Date html generated: 2016_05_16-AM-10_42_20
Last ObjectModification: 2015_12_28-PM-07_45_52

Theory : halting!dataflow

Home Index