Nuprl Lemma : hdf-state1-single-val_wf

[A,B,C:Type]. ∀[f:B ⟶ C ⟶ C]. ∀[X:hdataflow(A;B)]. ∀[b:C].
  (hdf-state1-single-val(f;X;b) ∈ hdataflow(A;C)) supposing (hdf-single-valued(X;A;B) and valueall-type(C))


Definitions occuring in Statement :  hdf-state1-single-val: hdf-state1-single-val(f;X;b) hdf-single-valued: hdf-single-valued(X;A;B) hdataflow: hdataflow(A;B) valueall-type: valueall-type(T) uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a hdf-state1-single-val: hdf-state1-single-val(f;X;b) prop: hdf-ap: X(a) subtype_rel: A ⊆B ext-eq: A ≡ B and: P ∧ Q all: x:A. B[x] implies:  Q ifthenelse: if then else fi  btrue: tt so_lambda: λ2x.t[x] so_apply: x[s] so_lambda: λ2y.t[x; y] so_apply: x[s1;s2] hdf-run: hdf-run(P) hdf-single-valued: hdf-single-valued(X;A;B) iterate-hdataflow: P*(inputs) list_accum: list_accum nil: [] it: bool: 𝔹 unit: Unit uiff: uiff(P;Q) bfalse: ff exists: x:A. B[x] or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b false: False not: ¬A callbyvalueall: callbyvalueall has-value: (a)↓ has-valueall: has-valueall(a) pi1: fst(t) top: Top nat: decidable: Dec(P) ge: i ≥  satisfiable_int_formula: satisfiable_int_formula(fmla) hdf-halt: hdf-halt()

\mforall{}[A,B,C:Type].  \mforall{}[f:B  {}\mrightarrow{}  C  {}\mrightarrow{}  C].  \mforall{}[X:hdataflow(A;B)].  \mforall{}[b:C].
    (hdf-state1-single-val(f;X;b)  \mmember{}  hdataflow(A;C))  supposing 
          (hdf-single-valued(X;A;B)  and 

Date html generated: 2016_05_16-AM-10_40_38
Last ObjectModification: 2016_01_17-AM-11_13_22

Theory : halting!dataflow

Home Index