Nuprl Lemma : hdf-union-eq-disju

[A,B,C:Type]. ∀[X:hdataflow(A;B)]. ∀[Y:hdataflow(A;C)].
  (X x.(inl x)) || x.(inr )) Y ∈ hdataflow(A;B C)) supposing 
     (valueall-type(B) and 


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

\mforall{}[A,B,C:Type].  \mforall{}[X:hdataflow(A;B)].  \mforall{}[Y:hdataflow(A;C)].
    (X  +  Y  =  (\mlambda{}x.(inl  x))  o  X  ||  (\mlambda{}x.(inr  x  ))  o  Y)  supposing 
          (valueall-type(B)  and 

Date html generated: 2016_05_16-AM-10_42_27
Last ObjectModification: 2016_01_17-AM-11_13_16

Theory : halting!dataflow

Home Index